[GOAL]
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
⊢ ↑(hasseDeriv k) f = sum f fun i r => ↑(monomial (i - k)) (↑(choose i k) * r)
[PROOFSTEP]
dsimp [hasseDeriv]
[GOAL]
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
⊢ (sum f fun x x_1 => ↑(monomial (x - k)) (choose x k • x_1)) = sum f fun i r => ↑(monomial (i - k)) (↑(choose i k) * r)
[PROOFSTEP]
congr
[GOAL]
case e_f
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
⊢ (fun x x_1 => ↑(monomial (x - k)) (choose x k • x_1)) = fun i r => ↑(monomial (i - k)) (↑(choose i k) * r)
[PROOFSTEP]
ext
[GOAL]
case e_f.h.h.a
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
x✝¹ : ℕ
x✝ : R
n✝ : ℕ
⊢ coeff (↑(monomial (x✝¹ - k)) (choose x✝¹ k • x✝)) n✝ = coeff (↑(monomial (x✝¹ - k)) (↑(choose x✝¹ k) * x✝)) n✝
[PROOFSTEP]
congr
[GOAL]
case e_f.h.h.a.e_a.h.e_6.h
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
x✝¹ : ℕ
x✝ : R
n✝ : ℕ
⊢ choose x✝¹ k • x✝ = ↑(choose x✝¹ k) * x✝
[PROOFSTEP]
apply nsmul_eq_mul
[GOAL]
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n : ℕ
⊢ coeff (↑(hasseDeriv k) f) n = ↑(choose (n + k) k) * coeff f (n + k)
[PROOFSTEP]
rw [hasseDeriv_apply, coeff_sum, sum_def, Finset.sum_eq_single (n + k), coeff_monomial]
[GOAL]
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n : ℕ
⊢ (if n + k - k = n then ↑(choose (n + k) k) * coeff f (n + k) else 0) = ↑(choose (n + k) k) * coeff f (n + k)
[PROOFSTEP]
simp only [if_true, add_tsub_cancel_right, eq_self_iff_true]
[GOAL]
case h₀
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n : ℕ
⊢ ∀ (b : ℕ), b ∈ support f → b ≠ n + k → coeff (↑(monomial (b - k)) (↑(choose b k) * coeff f b)) n = 0
[PROOFSTEP]
intro i _hi hink
[GOAL]
case h₀
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n i : ℕ
_hi : i ∈ support f
hink : i ≠ n + k
⊢ coeff (↑(monomial (i - k)) (↑(choose i k) * coeff f i)) n = 0
[PROOFSTEP]
rw [coeff_monomial]
[GOAL]
case h₀
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n i : ℕ
_hi : i ∈ support f
hink : i ≠ n + k
⊢ (if i - k = n then ↑(choose i k) * coeff f i else 0) = 0
[PROOFSTEP]
by_cases hik : i < k
[GOAL]
case pos
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n i : ℕ
_hi : i ∈ support f
hink : i ≠ n + k
hik : i < k
⊢ (if i - k = n then ↑(choose i k) * coeff f i else 0) = 0
[PROOFSTEP]
simp only [Nat.choose_eq_zero_of_lt hik, ite_self, Nat.cast_zero, zero_mul]
[GOAL]
case neg
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n i : ℕ
_hi : i ∈ support f
hink : i ≠ n + k
hik : ¬i < k
⊢ (if i - k = n then ↑(choose i k) * coeff f i else 0) = 0
[PROOFSTEP]
push_neg at hik
[GOAL]
case neg
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n i : ℕ
_hi : i ∈ support f
hink : i ≠ n + k
hik : k ≤ i
⊢ (if i - k = n then ↑(choose i k) * coeff f i else 0) = 0
[PROOFSTEP]
rw [if_neg]
[GOAL]
case neg.hnc
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n i : ℕ
_hi : i ∈ support f
hink : i ≠ n + k
hik : k ≤ i
⊢ ¬i - k = n
[PROOFSTEP]
contrapose! hink
[GOAL]
case neg.hnc
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n i : ℕ
_hi : i ∈ support f
hik : k ≤ i
hink : i - k = n
⊢ i = n + k
[PROOFSTEP]
exact (tsub_eq_iff_eq_add_of_le hik).mp hink
[GOAL]
case h₁
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n : ℕ
⊢ ¬n + k ∈ support f → coeff (↑(monomial (n + k - k)) (↑(choose (n + k) k) * coeff f (n + k))) n = 0
[PROOFSTEP]
intro h
[GOAL]
case h₁
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n : ℕ
h : ¬n + k ∈ support f
⊢ coeff (↑(monomial (n + k - k)) (↑(choose (n + k) k) * coeff f (n + k))) n = 0
[PROOFSTEP]
simp only [not_mem_support_iff.mp h, monomial_zero_right, mul_zero, coeff_zero]
[GOAL]
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
⊢ ↑(hasseDeriv 0) f = f
[PROOFSTEP]
simp only [hasseDeriv_apply, tsub_zero, Nat.choose_zero_right, Nat.cast_one, one_mul, sum_monomial_eq]
[GOAL]
R : Type u_1
inst✝ : Semiring R
k : ℕ
f p : R[X]
n : ℕ
h : natDegree p < n
⊢ ↑(hasseDeriv n) p = 0
[PROOFSTEP]
rw [hasseDeriv_apply, sum_def]
[GOAL]
R : Type u_1
inst✝ : Semiring R
k : ℕ
f p : R[X]
n : ℕ
h : natDegree p < n
⊢ ∑ n_1 in support p, ↑(monomial (n_1 - n)) (↑(choose n_1 n) * coeff p n_1) = 0
[PROOFSTEP]
refine' Finset.sum_eq_zero fun x hx => _
[GOAL]
R : Type u_1
inst✝ : Semiring R
k : ℕ
f p : R[X]
n : ℕ
h : natDegree p < n
x : ℕ
hx : x ∈ support p
⊢ ↑(monomial (x - n)) (↑(choose x n) * coeff p x) = 0
[PROOFSTEP]
simp [Nat.choose_eq_zero_of_lt ((le_natDegree_of_mem_supp _ hx).trans_lt h)]
[GOAL]
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
⊢ ↑(hasseDeriv 1) f = ↑derivative f
[PROOFSTEP]
simp only [hasseDeriv_apply, derivative_apply, ← C_mul_X_pow_eq_monomial, Nat.choose_one_right,
  (Nat.cast_commute _ _).eq]
[GOAL]
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n : ℕ
r : R
⊢ ↑(hasseDeriv k) (↑(monomial n) r) = ↑(monomial (n - k)) (↑(choose n k) * r)
[PROOFSTEP]
ext i
[GOAL]
case a
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n : ℕ
r : R
i : ℕ
⊢ coeff (↑(hasseDeriv k) (↑(monomial n) r)) i = coeff (↑(monomial (n - k)) (↑(choose n k) * r)) i
[PROOFSTEP]
simp only [hasseDeriv_coeff, coeff_monomial]
[GOAL]
case a
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n : ℕ
r : R
i : ℕ
⊢ (↑(choose (i + k) k) * if n = i + k then r else 0) = if n - k = i then ↑(choose n k) * r else 0
[PROOFSTEP]
by_cases hnik : n = i + k
[GOAL]
case pos
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n : ℕ
r : R
i : ℕ
hnik : n = i + k
⊢ (↑(choose (i + k) k) * if n = i + k then r else 0) = if n - k = i then ↑(choose n k) * r else 0
[PROOFSTEP]
rw [if_pos hnik, if_pos, ← hnik]
[GOAL]
case pos.hc
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n : ℕ
r : R
i : ℕ
hnik : n = i + k
⊢ n - k = i
[PROOFSTEP]
apply tsub_eq_of_eq_add_rev
[GOAL]
case pos.hc.h
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n : ℕ
r : R
i : ℕ
hnik : n = i + k
⊢ n = k + i
[PROOFSTEP]
rwa [add_comm]
[GOAL]
case neg
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n : ℕ
r : R
i : ℕ
hnik : ¬n = i + k
⊢ (↑(choose (i + k) k) * if n = i + k then r else 0) = if n - k = i then ↑(choose n k) * r else 0
[PROOFSTEP]
rw [if_neg hnik, mul_zero]
[GOAL]
case neg
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n : ℕ
r : R
i : ℕ
hnik : ¬n = i + k
⊢ 0 = if n - k = i then ↑(choose n k) * r else 0
[PROOFSTEP]
by_cases hkn : k ≤ n
[GOAL]
case pos
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n : ℕ
r : R
i : ℕ
hnik : ¬n = i + k
hkn : k ≤ n
⊢ 0 = if n - k = i then ↑(choose n k) * r else 0
[PROOFSTEP]
rw [← tsub_eq_iff_eq_add_of_le hkn] at hnik
[GOAL]
case pos
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n : ℕ
r : R
i : ℕ
hnik : ¬n - k = i
hkn : k ≤ n
⊢ 0 = if n - k = i then ↑(choose n k) * r else 0
[PROOFSTEP]
rw [if_neg hnik]
[GOAL]
case neg
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n : ℕ
r : R
i : ℕ
hnik : ¬n = i + k
hkn : ¬k ≤ n
⊢ 0 = if n - k = i then ↑(choose n k) * r else 0
[PROOFSTEP]
push_neg at hkn
[GOAL]
case neg
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n : ℕ
r : R
i : ℕ
hnik : ¬n = i + k
hkn : n < k
⊢ 0 = if n - k = i then ↑(choose n k) * r else 0
[PROOFSTEP]
rw [Nat.choose_eq_zero_of_lt hkn, Nat.cast_zero, zero_mul, ite_self]
[GOAL]
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
r : R
hk : 0 < k
⊢ ↑(hasseDeriv k) (↑C r) = 0
[PROOFSTEP]
rw [← monomial_zero_left, hasseDeriv_monomial, Nat.choose_eq_zero_of_lt hk, Nat.cast_zero, zero_mul,
  monomial_zero_right]
[GOAL]
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
hk : 0 < k
⊢ ↑(hasseDeriv k) 1 = 0
[PROOFSTEP]
rw [← C_1, hasseDeriv_C k _ hk]
[GOAL]
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
hk : 1 < k
⊢ ↑(hasseDeriv k) X = 0
[PROOFSTEP]
rw [← monomial_one_one_eq_X, hasseDeriv_monomial, Nat.choose_eq_zero_of_lt hk, Nat.cast_zero, zero_mul,
  monomial_zero_right]
[GOAL]
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
⊢ ↑(k ! • hasseDeriv k) = (↑derivative)^[k]
[PROOFSTEP]
induction' k with k ih
[GOAL]
case zero
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
⊢ ↑(Nat.zero ! • hasseDeriv Nat.zero) = (↑derivative)^[Nat.zero]
[PROOFSTEP]
rw [hasseDeriv_zero, factorial_zero, iterate_zero, one_smul, LinearMap.id_coe]
[GOAL]
case succ
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k : ℕ
ih : ↑(k ! • hasseDeriv k) = (↑derivative)^[k]
⊢ ↑((succ k)! • hasseDeriv (succ k)) = (↑derivative)^[succ k]
[PROOFSTEP]
ext f n : 2
[GOAL]
case succ.h.a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f✝ : R[X]
k : ℕ
ih : ↑(k ! • hasseDeriv k) = (↑derivative)^[k]
f : R[X]
n : ℕ
⊢ coeff (↑((succ k)! • hasseDeriv (succ k)) f) n = coeff ((↑derivative)^[succ k] f) n
[PROOFSTEP]
rw [iterate_succ_apply', ← ih]
[GOAL]
case succ.h.a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f✝ : R[X]
k : ℕ
ih : ↑(k ! • hasseDeriv k) = (↑derivative)^[k]
f : R[X]
n : ℕ
⊢ coeff (↑((succ k)! • hasseDeriv (succ k)) f) n = coeff (↑derivative (↑(k ! • hasseDeriv k) f)) n
[PROOFSTEP]
simp only [LinearMap.smul_apply, coeff_smul, LinearMap.map_smul_of_tower, coeff_derivative, hasseDeriv_coeff, ←
  @choose_symm_add _ k]
[GOAL]
case succ.h.a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f✝ : R[X]
k : ℕ
ih : ↑(k ! • hasseDeriv k) = (↑derivative)^[k]
f : R[X]
n : ℕ
⊢ (succ k)! • (↑(choose (n + succ k) (succ k)) * coeff f (n + succ k)) =
    k ! • (↑(choose (n + 1 + k) (n + 1)) * coeff f (n + 1 + k) * (↑n + 1))
[PROOFSTEP]
simp only [nsmul_eq_mul, factorial_succ, mul_assoc, succ_eq_add_one, ← add_assoc, add_right_comm n 1 k, ← cast_succ]
[GOAL]
case succ.h.a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f✝ : R[X]
k : ℕ
ih : ↑(k ! • hasseDeriv k) = (↑derivative)^[k]
f : R[X]
n : ℕ
⊢ ↑((k + 1) * k !) * (↑(choose (n + k + 1) (k + 1)) * coeff f (n + k + 1)) =
    ↑k ! * (↑(choose (n + k + 1) (n + 1)) * (coeff f (n + k + 1) * ↑(n + 1)))
[PROOFSTEP]
rw [← (cast_commute (n + 1) (f.coeff (n + k + 1))).eq]
[GOAL]
case succ.h.a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f✝ : R[X]
k : ℕ
ih : ↑(k ! • hasseDeriv k) = (↑derivative)^[k]
f : R[X]
n : ℕ
⊢ ↑((k + 1) * k !) * (↑(choose (n + k + 1) (k + 1)) * coeff f (n + k + 1)) =
    ↑k ! * (↑(choose (n + k + 1) (n + 1)) * (↑(n + 1) * coeff f (n + k + 1)))
[PROOFSTEP]
simp only [← mul_assoc]
[GOAL]
case succ.h.a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f✝ : R[X]
k : ℕ
ih : ↑(k ! • hasseDeriv k) = (↑derivative)^[k]
f : R[X]
n : ℕ
⊢ ↑((k + 1) * k !) * ↑(choose (n + k + 1) (k + 1)) * coeff f (n + k + 1) =
    ↑k ! * ↑(choose (n + k + 1) (n + 1)) * ↑(n + 1) * coeff f (n + k + 1)
[PROOFSTEP]
norm_cast
[GOAL]
case succ.h.a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f✝ : R[X]
k : ℕ
ih : ↑(k ! • hasseDeriv k) = (↑derivative)^[k]
f : R[X]
n : ℕ
⊢ ↑((k + 1) * k ! * choose (n + k + 1) (k + 1)) * coeff f (n + k + 1) =
    ↑(k ! * choose (n + k + 1) (n + 1) * (n + 1)) * coeff f (n + k + 1)
[PROOFSTEP]
congr 2
[GOAL]
case succ.h.a.e_a.e_a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f✝ : R[X]
k : ℕ
ih : ↑(k ! • hasseDeriv k) = (↑derivative)^[k]
f : R[X]
n : ℕ
⊢ (k + 1) * k ! * choose (n + k + 1) (k + 1) = k ! * choose (n + k + 1) (n + 1) * (n + 1)
[PROOFSTEP]
rw [mul_comm (k + 1) _, mul_assoc, mul_assoc]
[GOAL]
case succ.h.a.e_a.e_a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f✝ : R[X]
k : ℕ
ih : ↑(k ! • hasseDeriv k) = (↑derivative)^[k]
f : R[X]
n : ℕ
⊢ k ! * ((k + 1) * choose (n + k + 1) (k + 1)) = k ! * (choose (n + k + 1) (n + 1) * (n + 1))
[PROOFSTEP]
congr 1
[GOAL]
case succ.h.a.e_a.e_a.e_a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f✝ : R[X]
k : ℕ
ih : ↑(k ! • hasseDeriv k) = (↑derivative)^[k]
f : R[X]
n : ℕ
⊢ (k + 1) * choose (n + k + 1) (k + 1) = choose (n + k + 1) (n + 1) * (n + 1)
[PROOFSTEP]
have : n + k + 1 = n + (k + 1) := by apply add_assoc
[GOAL]
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f✝ : R[X]
k : ℕ
ih : ↑(k ! • hasseDeriv k) = (↑derivative)^[k]
f : R[X]
n : ℕ
⊢ n + k + 1 = n + (k + 1)
[PROOFSTEP]
apply add_assoc
[GOAL]
case succ.h.a.e_a.e_a.e_a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f✝ : R[X]
k : ℕ
ih : ↑(k ! • hasseDeriv k) = (↑derivative)^[k]
f : R[X]
n : ℕ
this : n + k + 1 = n + (k + 1)
⊢ (k + 1) * choose (n + k + 1) (k + 1) = choose (n + k + 1) (n + 1) * (n + 1)
[PROOFSTEP]
rw [← choose_symm_of_eq_add this, choose_succ_right_eq, mul_comm]
[GOAL]
case succ.h.a.e_a.e_a.e_a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f✝ : R[X]
k : ℕ
ih : ↑(k ! • hasseDeriv k) = (↑derivative)^[k]
f : R[X]
n : ℕ
this : n + k + 1 = n + (k + 1)
⊢ choose (n + k + 1) n * (k + 1) = choose (n + k + 1) n * (n + k + 1 - n)
[PROOFSTEP]
congr
[GOAL]
case succ.h.a.e_a.e_a.e_a.e_a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f✝ : R[X]
k : ℕ
ih : ↑(k ! • hasseDeriv k) = (↑derivative)^[k]
f : R[X]
n : ℕ
this : n + k + 1 = n + (k + 1)
⊢ k + 1 = n + k + 1 - n
[PROOFSTEP]
rw [add_assoc, add_tsub_cancel_left]
[GOAL]
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l : ℕ
⊢ LinearMap.comp (hasseDeriv k) (hasseDeriv l) = choose (k + l) k • hasseDeriv (k + l)
[PROOFSTEP]
ext i : 2
[GOAL]
case h.h
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
⊢ ↑(LinearMap.comp (LinearMap.comp (hasseDeriv k) (hasseDeriv l)) (monomial i)) 1 =
    ↑(LinearMap.comp (choose (k + l) k • hasseDeriv (k + l)) (monomial i)) 1
[PROOFSTEP]
simp only [LinearMap.smul_apply, comp_apply, LinearMap.coe_comp, smul_monomial, hasseDeriv_apply, mul_one,
  monomial_eq_zero_iff, sum_monomial_index, mul_zero, ← tsub_add_eq_tsub_tsub, add_comm l k]
[GOAL]
case h.h
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
⊢ ↑(monomial (i - (k + l))) (↑(choose (i - l) k) * ↑(choose i l)) =
    ↑(monomial (i - (k + l))) (choose (k + l) k • ↑(choose i (k + l)))
[PROOFSTEP]
rw_mod_cast [nsmul_eq_mul]
[GOAL]
case h.h
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
⊢ ↑(monomial (i - (k + l))) ↑(choose (i - l) k * choose i l) =
    ↑(monomial (i - (k + l))) (↑(choose (k + l) k) * ↑(choose i (k + l)))
[PROOFSTEP]
rw [← Nat.cast_mul]
[GOAL]
case h.h
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
⊢ ↑(monomial (i - (k + l))) ↑(choose (i - l) k * choose i l) =
    ↑(monomial (i - (k + l))) ↑(choose (k + l) k * choose i (k + l))
[PROOFSTEP]
congr 2
[GOAL]
case h.h.h.e_6.h.e_a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
⊢ choose (i - l) k * choose i l = choose (k + l) k * choose i (k + l)
[PROOFSTEP]
by_cases hikl : i < k + l
[GOAL]
case pos
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
hikl : i < k + l
⊢ choose (i - l) k * choose i l = choose (k + l) k * choose i (k + l)
[PROOFSTEP]
rw [choose_eq_zero_of_lt hikl, mul_zero]
[GOAL]
case pos
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
hikl : i < k + l
⊢ choose (i - l) k * choose i l = 0
[PROOFSTEP]
by_cases hil : i < l
[GOAL]
case pos
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
hikl : i < k + l
hil : i < l
⊢ choose (i - l) k * choose i l = 0
[PROOFSTEP]
rw [choose_eq_zero_of_lt hil, mul_zero]
[GOAL]
case neg
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
hikl : i < k + l
hil : ¬i < l
⊢ choose (i - l) k * choose i l = 0
[PROOFSTEP]
push_neg at hil
[GOAL]
case neg
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
hikl : i < k + l
hil : l ≤ i
⊢ choose (i - l) k * choose i l = 0
[PROOFSTEP]
rw [← tsub_lt_iff_right hil] at hikl
[GOAL]
case neg
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
hikl : i - l < k
hil : l ≤ i
⊢ choose (i - l) k * choose i l = 0
[PROOFSTEP]
rw [choose_eq_zero_of_lt hikl, zero_mul]
[GOAL]
case neg
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
hikl : ¬i < k + l
⊢ choose (i - l) k * choose i l = choose (k + l) k * choose i (k + l)
[PROOFSTEP]
push_neg at hikl
[GOAL]
case neg
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
hikl : k + l ≤ i
⊢ choose (i - l) k * choose i l = choose (k + l) k * choose i (k + l)
[PROOFSTEP]
apply @cast_injective ℚ
[GOAL]
case neg.a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
hikl : k + l ≤ i
⊢ ↑(choose (i - l) k * choose i l) = ↑(choose (k + l) k * choose i (k + l))
[PROOFSTEP]
have h1 : l ≤ i := le_of_add_le_right hikl
[GOAL]
case neg.a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
hikl : k + l ≤ i
h1 : l ≤ i
⊢ ↑(choose (i - l) k * choose i l) = ↑(choose (k + l) k * choose i (k + l))
[PROOFSTEP]
have h2 : k ≤ i - l := le_tsub_of_add_le_right hikl
[GOAL]
case neg.a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
hikl : k + l ≤ i
h1 : l ≤ i
h2 : k ≤ i - l
⊢ ↑(choose (i - l) k * choose i l) = ↑(choose (k + l) k * choose i (k + l))
[PROOFSTEP]
have h3 : k ≤ k + l := le_self_add
[GOAL]
case neg.a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
hikl : k + l ≤ i
h1 : l ≤ i
h2 : k ≤ i - l
h3 : k ≤ k + l
⊢ ↑(choose (i - l) k * choose i l) = ↑(choose (k + l) k * choose i (k + l))
[PROOFSTEP]
push_cast
[GOAL]
case neg.a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
hikl : k + l ≤ i
h1 : l ≤ i
h2 : k ≤ i - l
h3 : k ≤ k + l
⊢ ↑(choose (i - l) k) * ↑(choose i l) = ↑(choose (k + l) k) * ↑(choose i (k + l))
[PROOFSTEP]
rw [cast_choose ℚ h1, cast_choose ℚ h2, cast_choose ℚ h3, cast_choose ℚ hikl]
[GOAL]
case neg.a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
hikl : k + l ≤ i
h1 : l ≤ i
h2 : k ≤ i - l
h3 : k ≤ k + l
⊢ ↑(i - l)! / (↑k ! * ↑(i - l - k)!) * (↑i ! / (↑l ! * ↑(i - l)!)) =
    ↑(k + l)! / (↑k ! * ↑(k + l - k)!) * (↑i ! / (↑(k + l)! * ↑(i - (k + l))!))
[PROOFSTEP]
rw [show i - (k + l) = i - l - k by rw [add_comm]; apply tsub_add_eq_tsub_tsub]
[GOAL]
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
hikl : k + l ≤ i
h1 : l ≤ i
h2 : k ≤ i - l
h3 : k ≤ k + l
⊢ i - (k + l) = i - l - k
[PROOFSTEP]
rw [add_comm]
[GOAL]
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
hikl : k + l ≤ i
h1 : l ≤ i
h2 : k ≤ i - l
h3 : k ≤ k + l
⊢ i - (l + k) = i - l - k
[PROOFSTEP]
apply tsub_add_eq_tsub_tsub
[GOAL]
case neg.a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
hikl : k + l ≤ i
h1 : l ≤ i
h2 : k ≤ i - l
h3 : k ≤ k + l
⊢ ↑(i - l)! / (↑k ! * ↑(i - l - k)!) * (↑i ! / (↑l ! * ↑(i - l)!)) =
    ↑(k + l)! / (↑k ! * ↑(k + l - k)!) * (↑i ! / (↑(k + l)! * ↑(i - l - k)!))
[PROOFSTEP]
simp only [add_tsub_cancel_left]
[GOAL]
case neg.a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
hikl : k + l ≤ i
h1 : l ≤ i
h2 : k ≤ i - l
h3 : k ≤ k + l
⊢ ↑(i - l)! / (↑k ! * ↑(i - l - k)!) * (↑i ! / (↑l ! * ↑(i - l)!)) =
    ↑(k + l)! / (↑k ! * ↑l !) * (↑i ! / (↑(k + l)! * ↑(i - l - k)!))
[PROOFSTEP]
have H : ∀ n : ℕ, (n ! : ℚ) ≠ 0 := by exact_mod_cast factorial_ne_zero
[GOAL]
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
hikl : k + l ≤ i
h1 : l ≤ i
h2 : k ≤ i - l
h3 : k ≤ k + l
⊢ ∀ (n : ℕ), ↑n ! ≠ 0
[PROOFSTEP]
exact_mod_cast factorial_ne_zero
[GOAL]
case neg.a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
hikl : k + l ≤ i
h1 : l ≤ i
h2 : k ≤ i - l
h3 : k ≤ k + l
H : ∀ (n : ℕ), ↑n ! ≠ 0
⊢ ↑(i - l)! / (↑k ! * ↑(i - l - k)!) * (↑i ! / (↑l ! * ↑(i - l)!)) =
    ↑(k + l)! / (↑k ! * ↑l !) * (↑i ! / (↑(k + l)! * ↑(i - l - k)!))
[PROOFSTEP]
field_simp [H]
[GOAL]
case neg.a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
hikl : k + l ≤ i
h1 : l ≤ i
h2 : k ≤ i - l
h3 : k ≤ k + l
H : ∀ (n : ℕ), ↑n ! ≠ 0
⊢ ↑(i - l)! * ↑i ! * (↑k ! * ↑l ! * (↑(k + l)! * ↑(i - l - k)!)) =
    ↑(k + l)! * ↑i ! * (↑k ! * ↑(i - l - k)! * (↑l ! * ↑(i - l)!))
[PROOFSTEP]
ring
[GOAL]
R : Type u_1
inst✝ : Semiring R
k : ℕ
f p : R[X]
n : ℕ
⊢ natDegree (↑(hasseDeriv n) p) ≤ natDegree p - n
[PROOFSTEP]
classical
rw [hasseDeriv_apply, sum_def]
refine' (natDegree_sum_le _ _).trans _
simp_rw [Function.comp, natDegree_monomial]
rw [Finset.fold_ite, Finset.fold_const]
· simp only [ite_self, max_eq_right, zero_le', Finset.fold_max_le, true_and_iff, and_imp, tsub_le_iff_right,
    mem_support_iff, Ne.def, Finset.mem_filter]
  intro x hx hx'
  have hxp : x ≤ p.natDegree := le_natDegree_of_ne_zero hx
  have hxn : n ≤ x := by
    contrapose! hx'
    simp [Nat.choose_eq_zero_of_lt hx']
  rwa [tsub_add_cancel_of_le (hxn.trans hxp)]
· simp
[GOAL]
R : Type u_1
inst✝ : Semiring R
k : ℕ
f p : R[X]
n : ℕ
⊢ natDegree (↑(hasseDeriv n) p) ≤ natDegree p - n
[PROOFSTEP]
rw [hasseDeriv_apply, sum_def]
[GOAL]
R : Type u_1
inst✝ : Semiring R
k : ℕ
f p : R[X]
n : ℕ
⊢ natDegree (∑ n_1 in support p, ↑(monomial (n_1 - n)) (↑(choose n_1 n) * coeff p n_1)) ≤ natDegree p - n
[PROOFSTEP]
refine' (natDegree_sum_le _ _).trans _
[GOAL]
R : Type u_1
inst✝ : Semiring R
k : ℕ
f p : R[X]
n : ℕ
⊢ Finset.fold max 0 (natDegree ∘ fun n_1 => ↑(monomial (n_1 - n)) (↑(choose n_1 n) * coeff p n_1)) (support p) ≤
    natDegree p - n
[PROOFSTEP]
simp_rw [Function.comp, natDegree_monomial]
[GOAL]
R : Type u_1
inst✝ : Semiring R
k : ℕ
f p : R[X]
n : ℕ
⊢ Finset.fold max 0 (fun x => if ↑(choose x n) * coeff p x = 0 then 0 else x - n) (support p) ≤ natDegree p - n
[PROOFSTEP]
rw [Finset.fold_ite, Finset.fold_const]
[GOAL]
R : Type u_1
inst✝ : Semiring R
k : ℕ
f p : R[X]
n : ℕ
⊢ max (if Finset.filter (fun x => ↑(choose x n) * coeff p x = 0) (support p) = ∅ then 0 else max 0 0)
      (Finset.fold max 0 (fun x => x - n) (Finset.filter (fun i => ¬↑(choose i n) * coeff p i = 0) (support p))) ≤
    natDegree p - n
[PROOFSTEP]
simp only [ite_self, max_eq_right, zero_le', Finset.fold_max_le, true_and_iff, and_imp, tsub_le_iff_right,
  mem_support_iff, Ne.def, Finset.mem_filter]
[GOAL]
R : Type u_1
inst✝ : Semiring R
k : ℕ
f p : R[X]
n : ℕ
⊢ ∀ (x : ℕ), ¬coeff p x = 0 → ¬↑(choose x n) * coeff p x = 0 → x ≤ natDegree p - n + n
[PROOFSTEP]
intro x hx hx'
[GOAL]
R : Type u_1
inst✝ : Semiring R
k : ℕ
f p : R[X]
n x : ℕ
hx : ¬coeff p x = 0
hx' : ¬↑(choose x n) * coeff p x = 0
⊢ x ≤ natDegree p - n + n
[PROOFSTEP]
have hxp : x ≤ p.natDegree := le_natDegree_of_ne_zero hx
[GOAL]
R : Type u_1
inst✝ : Semiring R
k : ℕ
f p : R[X]
n x : ℕ
hx : ¬coeff p x = 0
hx' : ¬↑(choose x n) * coeff p x = 0
hxp : x ≤ natDegree p
⊢ x ≤ natDegree p - n + n
[PROOFSTEP]
have hxn : n ≤ x := by
  contrapose! hx'
  simp [Nat.choose_eq_zero_of_lt hx']
[GOAL]
R : Type u_1
inst✝ : Semiring R
k : ℕ
f p : R[X]
n x : ℕ
hx : ¬coeff p x = 0
hx' : ¬↑(choose x n) * coeff p x = 0
hxp : x ≤ natDegree p
⊢ n ≤ x
[PROOFSTEP]
contrapose! hx'
[GOAL]
R : Type u_1
inst✝ : Semiring R
k : ℕ
f p : R[X]
n x : ℕ
hx : ¬coeff p x = 0
hxp : x ≤ natDegree p
hx' : x < n
⊢ ↑(choose x n) * coeff p x = 0
[PROOFSTEP]
simp [Nat.choose_eq_zero_of_lt hx']
[GOAL]
R : Type u_1
inst✝ : Semiring R
k : ℕ
f p : R[X]
n x : ℕ
hx : ¬coeff p x = 0
hx' : ¬↑(choose x n) * coeff p x = 0
hxp : x ≤ natDegree p
hxn : n ≤ x
⊢ x ≤ natDegree p - n + n
[PROOFSTEP]
rwa [tsub_add_cancel_of_le (hxn.trans hxp)]
[GOAL]
case h
R : Type u_1
inst✝ : Semiring R
k : ℕ
f p : R[X]
n : ℕ
⊢ max 0 (max 0 0) = max 0 0
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝¹ : Semiring R
k : ℕ
f : R[X]
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
n : ℕ
⊢ natDegree (↑(hasseDeriv n) p) = natDegree p - n
[PROOFSTEP]
cases' lt_or_le p.natDegree n with hn hn
[GOAL]
case inl
R : Type u_1
inst✝¹ : Semiring R
k : ℕ
f : R[X]
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
n : ℕ
hn : natDegree p < n
⊢ natDegree (↑(hasseDeriv n) p) = natDegree p - n
[PROOFSTEP]
simpa [hasseDeriv_eq_zero_of_lt_natDegree, hn] using (tsub_eq_zero_of_le hn.le).symm
[GOAL]
case inr
R : Type u_1
inst✝¹ : Semiring R
k : ℕ
f : R[X]
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
n : ℕ
hn : n ≤ natDegree p
⊢ natDegree (↑(hasseDeriv n) p) = natDegree p - n
[PROOFSTEP]
refine' map_natDegree_eq_sub _ _
[GOAL]
case inr.refine'_1
R : Type u_1
inst✝¹ : Semiring R
k : ℕ
f : R[X]
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
n : ℕ
hn : n ≤ natDegree p
⊢ ∀ (f : R[X]), natDegree f < n → ↑(hasseDeriv n) f = 0
[PROOFSTEP]
exact fun h => hasseDeriv_eq_zero_of_lt_natDegree _ _
[GOAL]
case inr.refine'_2
R : Type u_1
inst✝¹ : Semiring R
k : ℕ
f : R[X]
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
n : ℕ
hn : n ≤ natDegree p
⊢ ∀ (n_1 : ℕ) (c : R), c ≠ 0 → natDegree (↑(hasseDeriv n) (↑(monomial n_1) c)) = n_1 - n
[PROOFSTEP]
classical
simp only [ite_eq_right_iff, Ne.def, natDegree_monomial, hasseDeriv_monomial]
intro k c c0 hh
rw [← nsmul_eq_mul, smul_eq_zero, Nat.choose_eq_zero_iff] at hh
exact (tsub_eq_zero_of_le (Or.resolve_right hh c0).le).symm
[GOAL]
case inr.refine'_2
R : Type u_1
inst✝¹ : Semiring R
k : ℕ
f : R[X]
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
n : ℕ
hn : n ≤ natDegree p
⊢ ∀ (n_1 : ℕ) (c : R), c ≠ 0 → natDegree (↑(hasseDeriv n) (↑(monomial n_1) c)) = n_1 - n
[PROOFSTEP]
simp only [ite_eq_right_iff, Ne.def, natDegree_monomial, hasseDeriv_monomial]
[GOAL]
case inr.refine'_2
R : Type u_1
inst✝¹ : Semiring R
k : ℕ
f : R[X]
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
n : ℕ
hn : n ≤ natDegree p
⊢ ∀ (n_1 : ℕ) (c : R), ¬c = 0 → ↑(choose n_1 n) * c = 0 → 0 = n_1 - n
[PROOFSTEP]
intro k c c0 hh
[GOAL]
case inr.refine'_2
R : Type u_1
inst✝¹ : Semiring R
k✝ : ℕ
f : R[X]
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
n : ℕ
hn : n ≤ natDegree p
k : ℕ
c : R
c0 : ¬c = 0
hh : ↑(choose k n) * c = 0
⊢ 0 = k - n
[PROOFSTEP]
rw [← nsmul_eq_mul, smul_eq_zero, Nat.choose_eq_zero_iff] at hh
[GOAL]
case inr.refine'_2
R : Type u_1
inst✝¹ : Semiring R
k✝ : ℕ
f : R[X]
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
n : ℕ
hn : n ≤ natDegree p
k : ℕ
c : R
c0 : ¬c = 0
hh : k < n ∨ c = 0
⊢ 0 = k - n
[PROOFSTEP]
exact (tsub_eq_zero_of_le (Or.resolve_right hh c0).le).symm
[GOAL]
R : Type u_1
inst✝ : Semiring R
k : ℕ
f✝ f g : R[X]
⊢ ↑(hasseDeriv k) (f * g) = ∑ ij in antidiagonal k, ↑(hasseDeriv ij.fst) f * ↑(hasseDeriv ij.snd) g
[PROOFSTEP]
let D k := (@hasseDeriv R _ k).toAddMonoidHom
[GOAL]
R : Type u_1
inst✝ : Semiring R
k : ℕ
f✝ f g : R[X]
D : ℕ → R[X] →+ R[X] := fun k => LinearMap.toAddMonoidHom (hasseDeriv k)
⊢ ↑(hasseDeriv k) (f * g) = ∑ ij in antidiagonal k, ↑(hasseDeriv ij.fst) f * ↑(hasseDeriv ij.snd) g
[PROOFSTEP]
let Φ := @AddMonoidHom.mul R[X] _
[GOAL]
R : Type u_1
inst✝ : Semiring R
k : ℕ
f✝ f g : R[X]
D : ℕ → R[X] →+ R[X] := fun k => LinearMap.toAddMonoidHom (hasseDeriv k)
Φ : R[X] →+ R[X] →+ R[X] := mul
⊢ ↑(hasseDeriv k) (f * g) = ∑ ij in antidiagonal k, ↑(hasseDeriv ij.fst) f * ↑(hasseDeriv ij.snd) g
[PROOFSTEP]
show
  (compHom (D k)).comp Φ f g = ∑ ij : ℕ × ℕ in antidiagonal k, ((compHom.comp ((compHom Φ) (D ij.1))).flip (D ij.2) f) g
[GOAL]
R : Type u_1
inst✝ : Semiring R
k : ℕ
f✝ f g : R[X]
D : ℕ → R[X] →+ R[X] := fun k => LinearMap.toAddMonoidHom (hasseDeriv k)
Φ : R[X] →+ R[X] →+ R[X] := mul
⊢ ↑(↑(AddMonoidHom.comp (↑compHom (D k)) Φ) f) g =
    ∑ ij in antidiagonal k,
      ↑(↑(↑(AddMonoidHom.flip (AddMonoidHom.comp compHom (↑(↑compHom Φ) (D ij.fst)))) (D ij.snd)) f) g
[PROOFSTEP]
simp only [← finset_sum_apply]
[GOAL]
R : Type u_1
inst✝ : Semiring R
k : ℕ
f✝ f g : R[X]
D : ℕ → R[X] →+ R[X] := fun k => LinearMap.toAddMonoidHom (hasseDeriv k)
Φ : R[X] →+ R[X] →+ R[X] := mul
⊢ ↑(↑(AddMonoidHom.comp (↑compHom (LinearMap.toAddMonoidHom (hasseDeriv k))) mul) f) g =
    ↑(↑(∑ x in antidiagonal k,
              ↑(AddMonoidHom.flip
                    (AddMonoidHom.comp compHom (↑(↑compHom mul) (LinearMap.toAddMonoidHom (hasseDeriv x.fst)))))
                (LinearMap.toAddMonoidHom (hasseDeriv x.snd)))
          f)
      g
[PROOFSTEP]
congr 2
[GOAL]
case e_a.e_a
R : Type u_1
inst✝ : Semiring R
k : ℕ
f✝ f g : R[X]
D : ℕ → R[X] →+ R[X] := fun k => LinearMap.toAddMonoidHom (hasseDeriv k)
Φ : R[X] →+ R[X] →+ R[X] := mul
⊢ AddMonoidHom.comp (↑compHom (LinearMap.toAddMonoidHom (hasseDeriv k))) mul =
    ∑ x in antidiagonal k,
      ↑(AddMonoidHom.flip (AddMonoidHom.comp compHom (↑(↑compHom mul) (LinearMap.toAddMonoidHom (hasseDeriv x.fst)))))
        (LinearMap.toAddMonoidHom (hasseDeriv x.snd))
[PROOFSTEP]
clear f g
[GOAL]
case e_a.e_a
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
D : ℕ → R[X] →+ R[X] := fun k => LinearMap.toAddMonoidHom (hasseDeriv k)
Φ : R[X] →+ R[X] →+ R[X] := mul
⊢ AddMonoidHom.comp (↑compHom (LinearMap.toAddMonoidHom (hasseDeriv k))) mul =
    ∑ x in antidiagonal k,
      ↑(AddMonoidHom.flip (AddMonoidHom.comp compHom (↑(↑compHom mul) (LinearMap.toAddMonoidHom (hasseDeriv x.fst)))))
        (LinearMap.toAddMonoidHom (hasseDeriv x.snd))
[PROOFSTEP]
ext m r n s : 4
[GOAL]
case e_a.e_a.h.h.h.h
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
D : ℕ → R[X] →+ R[X] := fun k => LinearMap.toAddMonoidHom (hasseDeriv k)
Φ : R[X] →+ R[X] →+ R[X] := mul
m : ℕ
r : R
n : ℕ
s : R
⊢ ↑(AddMonoidHom.comp
          (↑(AddMonoidHom.comp (AddMonoidHom.comp (↑compHom (LinearMap.toAddMonoidHom (hasseDeriv k))) mul)
                (LinearMap.toAddMonoidHom (monomial m)))
            r)
          (LinearMap.toAddMonoidHom (monomial n)))
      s =
    ↑(AddMonoidHom.comp
          (↑(AddMonoidHom.comp
                (∑ x in antidiagonal k,
                  ↑(AddMonoidHom.flip
                        (AddMonoidHom.comp compHom (↑(↑compHom mul) (LinearMap.toAddMonoidHom (hasseDeriv x.fst)))))
                    (LinearMap.toAddMonoidHom (hasseDeriv x.snd)))
                (LinearMap.toAddMonoidHom (monomial m)))
            r)
          (LinearMap.toAddMonoidHom (monomial n)))
      s
[PROOFSTEP]
simp only [finset_sum_apply, coe_mulLeft, coe_comp, flip_apply, Function.comp_apply, hasseDeriv_monomial,
  LinearMap.toAddMonoidHom_coe, compHom_apply_apply, coe_mul, monomial_mul_monomial]
[GOAL]
case e_a.e_a.h.h.h.h
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
D : ℕ → R[X] →+ R[X] := fun k => LinearMap.toAddMonoidHom (hasseDeriv k)
Φ : R[X] →+ R[X] →+ R[X] := mul
m : ℕ
r : R
n : ℕ
s : R
⊢ ↑(monomial (m + n - k)) (↑(choose (m + n) k) * (r * s)) =
    ∑ x in antidiagonal k, ↑(monomial (m - x.fst + (n - x.snd))) (↑(choose m x.fst) * r * (↑(choose n x.snd) * s))
[PROOFSTEP]
have aux :
  ∀ x : ℕ × ℕ,
    x ∈ antidiagonal k →
      monomial (m - x.1 + (n - x.2)) (↑(m.choose x.1) * r * (↑(n.choose x.2) * s)) =
        monomial (m + n - k) (↑(m.choose x.1) * ↑(n.choose x.2) * (r * s)) :=
  by
  intro x hx
  rw [Finset.Nat.mem_antidiagonal] at hx
  subst hx
  by_cases hm : m < x.1
  · simp only [Nat.choose_eq_zero_of_lt hm, Nat.cast_zero, zero_mul, monomial_zero_right]
  by_cases hn : n < x.2
  · simp only [Nat.choose_eq_zero_of_lt hn, Nat.cast_zero, zero_mul, mul_zero, monomial_zero_right]
  push_neg at hm hn
  rw [tsub_add_eq_add_tsub hm, ← add_tsub_assoc_of_le hn, ← tsub_add_eq_tsub_tsub, add_comm x.2 x.1, mul_assoc, ←
    mul_assoc r, ← (Nat.cast_commute _ r).eq, mul_assoc, mul_assoc]
[GOAL]
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
D : ℕ → R[X] →+ R[X] := fun k => LinearMap.toAddMonoidHom (hasseDeriv k)
Φ : R[X] →+ R[X] →+ R[X] := mul
m : ℕ
r : R
n : ℕ
s : R
⊢ ∀ (x : ℕ × ℕ),
    x ∈ antidiagonal k →
      ↑(monomial (m - x.fst + (n - x.snd))) (↑(choose m x.fst) * r * (↑(choose n x.snd) * s)) =
        ↑(monomial (m + n - k)) (↑(choose m x.fst) * ↑(choose n x.snd) * (r * s))
[PROOFSTEP]
intro x hx
[GOAL]
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
D : ℕ → R[X] →+ R[X] := fun k => LinearMap.toAddMonoidHom (hasseDeriv k)
Φ : R[X] →+ R[X] →+ R[X] := mul
m : ℕ
r : R
n : ℕ
s : R
x : ℕ × ℕ
hx : x ∈ antidiagonal k
⊢ ↑(monomial (m - x.fst + (n - x.snd))) (↑(choose m x.fst) * r * (↑(choose n x.snd) * s)) =
    ↑(monomial (m + n - k)) (↑(choose m x.fst) * ↑(choose n x.snd) * (r * s))
[PROOFSTEP]
rw [Finset.Nat.mem_antidiagonal] at hx
[GOAL]
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
D : ℕ → R[X] →+ R[X] := fun k => LinearMap.toAddMonoidHom (hasseDeriv k)
Φ : R[X] →+ R[X] →+ R[X] := mul
m : ℕ
r : R
n : ℕ
s : R
x : ℕ × ℕ
hx : x.fst + x.snd = k
⊢ ↑(monomial (m - x.fst + (n - x.snd))) (↑(choose m x.fst) * r * (↑(choose n x.snd) * s)) =
    ↑(monomial (m + n - k)) (↑(choose m x.fst) * ↑(choose n x.snd) * (r * s))
[PROOFSTEP]
subst hx
[GOAL]
R : Type u_1
inst✝ : Semiring R
f : R[X]
D : ℕ → R[X] →+ R[X] := fun k => LinearMap.toAddMonoidHom (hasseDeriv k)
Φ : R[X] →+ R[X] →+ R[X] := mul
m : ℕ
r : R
n : ℕ
s : R
x : ℕ × ℕ
⊢ ↑(monomial (m - x.fst + (n - x.snd))) (↑(choose m x.fst) * r * (↑(choose n x.snd) * s)) =
    ↑(monomial (m + n - (x.fst + x.snd))) (↑(choose m x.fst) * ↑(choose n x.snd) * (r * s))
[PROOFSTEP]
by_cases hm : m < x.1
[GOAL]
case pos
R : Type u_1
inst✝ : Semiring R
f : R[X]
D : ℕ → R[X] →+ R[X] := fun k => LinearMap.toAddMonoidHom (hasseDeriv k)
Φ : R[X] →+ R[X] →+ R[X] := mul
m : ℕ
r : R
n : ℕ
s : R
x : ℕ × ℕ
hm : m < x.fst
⊢ ↑(monomial (m - x.fst + (n - x.snd))) (↑(choose m x.fst) * r * (↑(choose n x.snd) * s)) =
    ↑(monomial (m + n - (x.fst + x.snd))) (↑(choose m x.fst) * ↑(choose n x.snd) * (r * s))
[PROOFSTEP]
simp only [Nat.choose_eq_zero_of_lt hm, Nat.cast_zero, zero_mul, monomial_zero_right]
[GOAL]
case neg
R : Type u_1
inst✝ : Semiring R
f : R[X]
D : ℕ → R[X] →+ R[X] := fun k => LinearMap.toAddMonoidHom (hasseDeriv k)
Φ : R[X] →+ R[X] →+ R[X] := mul
m : ℕ
r : R
n : ℕ
s : R
x : ℕ × ℕ
hm : ¬m < x.fst
⊢ ↑(monomial (m - x.fst + (n - x.snd))) (↑(choose m x.fst) * r * (↑(choose n x.snd) * s)) =
    ↑(monomial (m + n - (x.fst + x.snd))) (↑(choose m x.fst) * ↑(choose n x.snd) * (r * s))
[PROOFSTEP]
by_cases hn : n < x.2
[GOAL]
case pos
R : Type u_1
inst✝ : Semiring R
f : R[X]
D : ℕ → R[X] →+ R[X] := fun k => LinearMap.toAddMonoidHom (hasseDeriv k)
Φ : R[X] →+ R[X] →+ R[X] := mul
m : ℕ
r : R
n : ℕ
s : R
x : ℕ × ℕ
hm : ¬m < x.fst
hn : n < x.snd
⊢ ↑(monomial (m - x.fst + (n - x.snd))) (↑(choose m x.fst) * r * (↑(choose n x.snd) * s)) =
    ↑(monomial (m + n - (x.fst + x.snd))) (↑(choose m x.fst) * ↑(choose n x.snd) * (r * s))
[PROOFSTEP]
simp only [Nat.choose_eq_zero_of_lt hn, Nat.cast_zero, zero_mul, mul_zero, monomial_zero_right]
[GOAL]
case neg
R : Type u_1
inst✝ : Semiring R
f : R[X]
D : ℕ → R[X] →+ R[X] := fun k => LinearMap.toAddMonoidHom (hasseDeriv k)
Φ : R[X] →+ R[X] →+ R[X] := mul
m : ℕ
r : R
n : ℕ
s : R
x : ℕ × ℕ
hm : ¬m < x.fst
hn : ¬n < x.snd
⊢ ↑(monomial (m - x.fst + (n - x.snd))) (↑(choose m x.fst) * r * (↑(choose n x.snd) * s)) =
    ↑(monomial (m + n - (x.fst + x.snd))) (↑(choose m x.fst) * ↑(choose n x.snd) * (r * s))
[PROOFSTEP]
push_neg at hm hn
[GOAL]
case neg
R : Type u_1
inst✝ : Semiring R
f : R[X]
D : ℕ → R[X] →+ R[X] := fun k => LinearMap.toAddMonoidHom (hasseDeriv k)
Φ : R[X] →+ R[X] →+ R[X] := mul
m : ℕ
r : R
n : ℕ
s : R
x : ℕ × ℕ
hm : x.fst ≤ m
hn : x.snd ≤ n
⊢ ↑(monomial (m - x.fst + (n - x.snd))) (↑(choose m x.fst) * r * (↑(choose n x.snd) * s)) =
    ↑(monomial (m + n - (x.fst + x.snd))) (↑(choose m x.fst) * ↑(choose n x.snd) * (r * s))
[PROOFSTEP]
rw [tsub_add_eq_add_tsub hm, ← add_tsub_assoc_of_le hn, ← tsub_add_eq_tsub_tsub, add_comm x.2 x.1, mul_assoc, ←
  mul_assoc r, ← (Nat.cast_commute _ r).eq, mul_assoc, mul_assoc]
[GOAL]
case e_a.e_a.h.h.h.h
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
D : ℕ → R[X] →+ R[X] := fun k => LinearMap.toAddMonoidHom (hasseDeriv k)
Φ : R[X] →+ R[X] →+ R[X] := mul
m : ℕ
r : R
n : ℕ
s : R
aux :
  ∀ (x : ℕ × ℕ),
    x ∈ antidiagonal k →
      ↑(monomial (m - x.fst + (n - x.snd))) (↑(choose m x.fst) * r * (↑(choose n x.snd) * s)) =
        ↑(monomial (m + n - k)) (↑(choose m x.fst) * ↑(choose n x.snd) * (r * s))
⊢ ↑(monomial (m + n - k)) (↑(choose (m + n) k) * (r * s)) =
    ∑ x in antidiagonal k, ↑(monomial (m - x.fst + (n - x.snd))) (↑(choose m x.fst) * r * (↑(choose n x.snd) * s))
[PROOFSTEP]
rw [Finset.sum_congr rfl aux]
[GOAL]
case e_a.e_a.h.h.h.h
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
D : ℕ → R[X] →+ R[X] := fun k => LinearMap.toAddMonoidHom (hasseDeriv k)
Φ : R[X] →+ R[X] →+ R[X] := mul
m : ℕ
r : R
n : ℕ
s : R
aux :
  ∀ (x : ℕ × ℕ),
    x ∈ antidiagonal k →
      ↑(monomial (m - x.fst + (n - x.snd))) (↑(choose m x.fst) * r * (↑(choose n x.snd) * s)) =
        ↑(monomial (m + n - k)) (↑(choose m x.fst) * ↑(choose n x.snd) * (r * s))
⊢ ↑(monomial (m + n - k)) (↑(choose (m + n) k) * (r * s)) =
    ∑ x in antidiagonal k, ↑(monomial (m + n - k)) (↑(choose m x.fst) * ↑(choose n x.snd) * (r * s))
[PROOFSTEP]
rw [← LinearMap.map_sum, ← Finset.sum_mul]
[GOAL]
case e_a.e_a.h.h.h.h
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
D : ℕ → R[X] →+ R[X] := fun k => LinearMap.toAddMonoidHom (hasseDeriv k)
Φ : R[X] →+ R[X] →+ R[X] := mul
m : ℕ
r : R
n : ℕ
s : R
aux :
  ∀ (x : ℕ × ℕ),
    x ∈ antidiagonal k →
      ↑(monomial (m - x.fst + (n - x.snd))) (↑(choose m x.fst) * r * (↑(choose n x.snd) * s)) =
        ↑(monomial (m + n - k)) (↑(choose m x.fst) * ↑(choose n x.snd) * (r * s))
⊢ ↑(monomial (m + n - k)) (↑(choose (m + n) k) * (r * s)) =
    ↑(monomial (m + n - k)) ((∑ x in antidiagonal k, ↑(choose m x.fst) * ↑(choose n x.snd)) * (r * s))
[PROOFSTEP]
congr
[GOAL]
case e_a.e_a.h.h.h.h.h.e_6.h.e_a
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
D : ℕ → R[X] →+ R[X] := fun k => LinearMap.toAddMonoidHom (hasseDeriv k)
Φ : R[X] →+ R[X] →+ R[X] := mul
m : ℕ
r : R
n : ℕ
s : R
aux :
  ∀ (x : ℕ × ℕ),
    x ∈ antidiagonal k →
      ↑(monomial (m - x.fst + (n - x.snd))) (↑(choose m x.fst) * r * (↑(choose n x.snd) * s)) =
        ↑(monomial (m + n - k)) (↑(choose m x.fst) * ↑(choose n x.snd) * (r * s))
⊢ ↑(choose (m + n) k) = ∑ x in antidiagonal k, ↑(choose m x.fst) * ↑(choose n x.snd)
[PROOFSTEP]
rw_mod_cast [← Nat.add_choose_eq]


[GOAL]
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
p q : Fq[X]
⊢ (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) (p * q) =
    (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) p *
      (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) q
[PROOFSTEP]
by_cases hp : p = 0
[GOAL]
case pos
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
p q : Fq[X]
hp : p = 0
⊢ (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) (p * q) =
    (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) p *
      (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) q
[PROOFSTEP]
simp [hp]
[GOAL]
case neg
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
p q : Fq[X]
hp : ¬p = 0
⊢ (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) (p * q) =
    (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) p *
      (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) q
[PROOFSTEP]
by_cases hq : q = 0
[GOAL]
case pos
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
p q : Fq[X]
hp : ¬p = 0
hq : q = 0
⊢ (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) (p * q) =
    (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) p *
      (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) q
[PROOFSTEP]
simp [hq]
[GOAL]
case neg
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
p q : Fq[X]
hp : ¬p = 0
hq : ¬q = 0
⊢ (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) (p * q) =
    (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) p *
      (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) q
[PROOFSTEP]
have hpq : p * q ≠ 0 := mul_ne_zero hp hq
[GOAL]
case neg
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
p q : Fq[X]
hp : ¬p = 0
hq : ¬q = 0
hpq : p * q ≠ 0
⊢ (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) (p * q) =
    (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) p *
      (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) q
[PROOFSTEP]
simp only [hpq, hp, hq, eq_self_iff_true, if_true, if_false, Polynomial.natDegree_mul hp hq, pow_add]
[GOAL]
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
p : Fq[X]
⊢ 0 ≤
    MulHom.toFun
      { toFun := fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p,
        map_mul' :=
          (_ :
            ∀ (p q : Fq[X]),
              (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) (p * q) =
                (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) p *
                  (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) q) }
      p
[PROOFSTEP]
dsimp
[GOAL]
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
p : Fq[X]
⊢ 0 ≤ if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p
[PROOFSTEP]
split_ifs
[GOAL]
case pos
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
p : Fq[X]
h✝ : p = 0
⊢ 0 ≤ 0
[PROOFSTEP]
rfl
[GOAL]
case neg
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
p : Fq[X]
h✝ : ¬p = 0
⊢ 0 ≤ ↑(Fintype.card Fq) ^ natDegree p
[PROOFSTEP]
exact pow_nonneg (Int.ofNat_zero_le _) _
[GOAL]
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
p : Fq[X]
h : ¬p = 0 → ↑(Fintype.card Fq) ^ natDegree p = 0
⊢ p = 0
[PROOFSTEP]
contrapose! h
[GOAL]
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
p : Fq[X]
h : p ≠ 0
⊢ p ≠ 0 ∧ ↑(Fintype.card Fq) ^ natDegree p ≠ 0
[PROOFSTEP]
exact ⟨h, (pow_pos _).ne'⟩
[GOAL]
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
p q : Fq[X]
⊢ MulHom.toFun
      { toFun := fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p,
        map_mul' :=
          (_ :
            ∀ (p q : Fq[X]),
              (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) (p * q) =
                (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) p *
                  (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) q) }
      (p + q) ≤
    MulHom.toFun
        { toFun := fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p,
          map_mul' :=
            (_ :
              ∀ (p q : Fq[X]),
                (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) (p * q) =
                  (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) p *
                    (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) q) }
        p +
      MulHom.toFun
        { toFun := fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p,
          map_mul' :=
            (_ :
              ∀ (p q : Fq[X]),
                (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) (p * q) =
                  (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) p *
                    (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) q) }
        q
[PROOFSTEP]
by_cases hp : p = 0
[GOAL]
case pos
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
p q : Fq[X]
hp : p = 0
⊢ MulHom.toFun
      { toFun := fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p,
        map_mul' :=
          (_ :
            ∀ (p q : Fq[X]),
              (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) (p * q) =
                (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) p *
                  (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) q) }
      (p + q) ≤
    MulHom.toFun
        { toFun := fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p,
          map_mul' :=
            (_ :
              ∀ (p q : Fq[X]),
                (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) (p * q) =
                  (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) p *
                    (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) q) }
        p +
      MulHom.toFun
        { toFun := fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p,
          map_mul' :=
            (_ :
              ∀ (p q : Fq[X]),
                (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) (p * q) =
                  (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) p *
                    (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) q) }
        q
[PROOFSTEP]
simp [hp]
[GOAL]
case neg
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
p q : Fq[X]
hp : ¬p = 0
⊢ MulHom.toFun
      { toFun := fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p,
        map_mul' :=
          (_ :
            ∀ (p q : Fq[X]),
              (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) (p * q) =
                (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) p *
                  (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) q) }
      (p + q) ≤
    MulHom.toFun
        { toFun := fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p,
          map_mul' :=
            (_ :
              ∀ (p q : Fq[X]),
                (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) (p * q) =
                  (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) p *
                    (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) q) }
        p +
      MulHom.toFun
        { toFun := fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p,
          map_mul' :=
            (_ :
              ∀ (p q : Fq[X]),
                (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) (p * q) =
                  (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) p *
                    (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) q) }
        q
[PROOFSTEP]
by_cases hq : q = 0
[GOAL]
case pos
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
p q : Fq[X]
hp : ¬p = 0
hq : q = 0
⊢ MulHom.toFun
      { toFun := fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p,
        map_mul' :=
          (_ :
            ∀ (p q : Fq[X]),
              (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) (p * q) =
                (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) p *
                  (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) q) }
      (p + q) ≤
    MulHom.toFun
        { toFun := fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p,
          map_mul' :=
            (_ :
              ∀ (p q : Fq[X]),
                (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) (p * q) =
                  (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) p *
                    (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) q) }
        p +
      MulHom.toFun
        { toFun := fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p,
          map_mul' :=
            (_ :
              ∀ (p q : Fq[X]),
                (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) (p * q) =
                  (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) p *
                    (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) q) }
        q
[PROOFSTEP]
simp [hq]
[GOAL]
case neg
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
p q : Fq[X]
hp : ¬p = 0
hq : ¬q = 0
⊢ MulHom.toFun
      { toFun := fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p,
        map_mul' :=
          (_ :
            ∀ (p q : Fq[X]),
              (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) (p * q) =
                (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) p *
                  (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) q) }
      (p + q) ≤
    MulHom.toFun
        { toFun := fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p,
          map_mul' :=
            (_ :
              ∀ (p q : Fq[X]),
                (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) (p * q) =
                  (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) p *
                    (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) q) }
        p +
      MulHom.toFun
        { toFun := fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p,
          map_mul' :=
            (_ :
              ∀ (p q : Fq[X]),
                (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) (p * q) =
                  (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) p *
                    (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) q) }
        q
[PROOFSTEP]
by_cases hpq : p + q = 0
[GOAL]
case pos
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
p q : Fq[X]
hp : ¬p = 0
hq : ¬q = 0
hpq : p + q = 0
⊢ MulHom.toFun
      { toFun := fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p,
        map_mul' :=
          (_ :
            ∀ (p q : Fq[X]),
              (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) (p * q) =
                (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) p *
                  (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) q) }
      (p + q) ≤
    MulHom.toFun
        { toFun := fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p,
          map_mul' :=
            (_ :
              ∀ (p q : Fq[X]),
                (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) (p * q) =
                  (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) p *
                    (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) q) }
        p +
      MulHom.toFun
        { toFun := fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p,
          map_mul' :=
            (_ :
              ∀ (p q : Fq[X]),
                (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) (p * q) =
                  (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) p *
                    (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) q) }
        q
[PROOFSTEP]
simp only [hpq, hp, hq, eq_self_iff_true, if_true, if_false]
[GOAL]
case pos
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
p q : Fq[X]
hp : ¬p = 0
hq : ¬q = 0
hpq : p + q = 0
⊢ 0 ≤ ↑(Fintype.card Fq) ^ natDegree p + ↑(Fintype.card Fq) ^ natDegree q
[PROOFSTEP]
exact add_nonneg (pow_pos _).le (pow_pos _).le
[GOAL]
case neg
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
p q : Fq[X]
hp : ¬p = 0
hq : ¬q = 0
hpq : ¬p + q = 0
⊢ MulHom.toFun
      { toFun := fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p,
        map_mul' :=
          (_ :
            ∀ (p q : Fq[X]),
              (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) (p * q) =
                (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) p *
                  (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) q) }
      (p + q) ≤
    MulHom.toFun
        { toFun := fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p,
          map_mul' :=
            (_ :
              ∀ (p q : Fq[X]),
                (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) (p * q) =
                  (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) p *
                    (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) q) }
        p +
      MulHom.toFun
        { toFun := fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p,
          map_mul' :=
            (_ :
              ∀ (p q : Fq[X]),
                (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) (p * q) =
                  (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) p *
                    (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) q) }
        q
[PROOFSTEP]
simp only [hpq, hp, hq, if_false]
[GOAL]
case neg
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
p q : Fq[X]
hp : ¬p = 0
hq : ¬q = 0
hpq : ¬p + q = 0
⊢ ↑(Fintype.card Fq) ^ natDegree (p + q) ≤ ↑(Fintype.card Fq) ^ natDegree p + ↑(Fintype.card Fq) ^ natDegree q
[PROOFSTEP]
refine' le_trans (pow_le_pow (by linarith) (Polynomial.natDegree_add_le _ _)) _
[GOAL]
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
p q : Fq[X]
hp : ¬p = 0
hq : ¬q = 0
hpq : ¬p + q = 0
⊢ 1 ≤ ↑(Fintype.card Fq)
[PROOFSTEP]
linarith
[GOAL]
case neg
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
p q : Fq[X]
hp : ¬p = 0
hq : ¬q = 0
hpq : ¬p + q = 0
⊢ ↑(Fintype.card Fq) ^ max (natDegree p) (natDegree q) ≤
    ↑(Fintype.card Fq) ^ natDegree p + ↑(Fintype.card Fq) ^ natDegree q
[PROOFSTEP]
refine' le_trans (le_max_iff.mpr _) (max_le_add_of_nonneg (pow_nonneg (by linarith) _) (pow_nonneg (by linarith) _))
[GOAL]
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
p q : Fq[X]
hp : ¬p = 0
hq : ¬q = 0
hpq : ¬p + q = 0
⊢ 0 ≤ ↑(Fintype.card Fq)
[PROOFSTEP]
linarith
[GOAL]
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
p q : Fq[X]
hp : ¬p = 0
hq : ¬q = 0
hpq : ¬p + q = 0
⊢ 0 ≤ ↑(Fintype.card Fq)
[PROOFSTEP]
linarith
[GOAL]
case neg
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
p q : Fq[X]
hp : ¬p = 0
hq : ¬q = 0
hpq : ¬p + q = 0
⊢ ↑(Fintype.card Fq) ^ max (natDegree p) (natDegree q) ≤ ↑(Fintype.card Fq) ^ natDegree p ∨
    ↑(Fintype.card Fq) ^ max (natDegree p) (natDegree q) ≤ ↑(Fintype.card Fq) ^ natDegree q
[PROOFSTEP]
exact (max_choice p.natDegree q.natDegree).imp (fun h => by rw [h]) fun h => by rw [h]
[GOAL]
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
p q : Fq[X]
hp : ¬p = 0
hq : ¬q = 0
hpq : ¬p + q = 0
h : max (natDegree p) (natDegree q) = natDegree p
⊢ ↑(Fintype.card Fq) ^ max (natDegree p) (natDegree q) ≤ ↑(Fintype.card Fq) ^ natDegree p
[PROOFSTEP]
rw [h]
[GOAL]
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
p q : Fq[X]
hp : ¬p = 0
hq : ¬q = 0
hpq : ¬p + q = 0
h : max (natDegree p) (natDegree q) = natDegree q
⊢ ↑(Fintype.card Fq) ^ max (natDegree p) (natDegree q) ≤ ↑(Fintype.card Fq) ^ natDegree q
[PROOFSTEP]
rw [h]
[GOAL]
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
p q : Fq[X]
⊢ ↑cardPowDegree p < ↑cardPowDegree q ↔ EuclideanDomain.r p q
[PROOFSTEP]
show cardPowDegree p < cardPowDegree q ↔ degree p < degree q
[GOAL]
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
p q : Fq[X]
⊢ ↑cardPowDegree p < ↑cardPowDegree q ↔ degree p < degree q
[PROOFSTEP]
simp only [cardPowDegree_apply]
[GOAL]
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
p q : Fq[X]
⊢ ((if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) < if q = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree q) ↔
    degree p < degree q
[PROOFSTEP]
split_ifs with hp hq hq
[GOAL]
case pos
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
p q : Fq[X]
hp : p = 0
hq : q = 0
⊢ 0 < 0 ↔ degree p < degree q
[PROOFSTEP]
simp only [hp, hq, lt_self_iff_false]
[GOAL]
case neg
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
p q : Fq[X]
hp : p = 0
hq : ¬q = 0
⊢ 0 < ↑(Fintype.card Fq) ^ natDegree q ↔ degree p < degree q
[PROOFSTEP]
simp only [hp, hq, degree_zero, Ne.def, bot_lt_iff_ne_bot, degree_eq_bot, pow_pos, not_false_iff]
[GOAL]
case pos
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
p q : Fq[X]
hp : ¬p = 0
hq : q = 0
⊢ ↑(Fintype.card Fq) ^ natDegree p < 0 ↔ degree p < degree q
[PROOFSTEP]
simp only [hp, hq, degree_zero, not_lt_bot, (pow_pos _).not_lt]
[GOAL]
case neg
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
p q : Fq[X]
hp : ¬p = 0
hq : ¬q = 0
⊢ ↑(Fintype.card Fq) ^ natDegree p < ↑(Fintype.card Fq) ^ natDegree q ↔ degree p < degree q
[PROOFSTEP]
rw [degree_eq_natDegree hp, degree_eq_natDegree hq, Nat.cast_withBot, Nat.cast_withBot, WithBot.coe_lt_coe,
  pow_lt_pow_iff]
[GOAL]
case neg
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
p q : Fq[X]
hp : ¬p = 0
hq : ¬q = 0
⊢ 1 < ↑(Fintype.card Fq)
[PROOFSTEP]
exact_mod_cast @Fintype.one_lt_card Fq _ _


[GOAL]
f : Natβ Natα.zero → WType Natβ
⊢ ofNat (toNat (mk Natα.zero f)) = mk Natα.zero f
[PROOFSTEP]
rw [toNat, ofNat]
[GOAL]
f : Natβ Natα.zero → WType Natβ
⊢ mk Natα.zero Empty.elim = mk Natα.zero f
[PROOFSTEP]
congr
[GOAL]
case e_f
f : Natβ Natα.zero → WType Natβ
⊢ Empty.elim = f
[PROOFSTEP]
ext x
[GOAL]
case e_f.h
f : Natβ Natα.zero → WType Natβ
x : Empty
⊢ Empty.elim x = f x
[PROOFSTEP]
cases x
[GOAL]
f : Natβ Natα.succ → WType Natβ
⊢ ofNat (toNat (mk Natα.succ f)) = mk Natα.succ f
[PROOFSTEP]
simp only [toNat, ofNat, leftInverse_nat (f ()), mk.injEq, heq_eq_eq, true_and]
[GOAL]
f : Natβ Natα.succ → WType Natβ
⊢ (fun x => f ()) = f
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
⊢ toNat (ofNat (Nat.succ n)) = Nat.succ n
[PROOFSTEP]
rw [ofNat, toNat, rightInverse_nat n]
[GOAL]
γ : Type u
f : Listβ γ Listα.nil → WType (Listβ γ)
⊢ ofList γ (toList γ (mk Listα.nil f)) = mk Listα.nil f
[PROOFSTEP]
simp only [toList, ofList, mk.injEq, heq_eq_eq, true_and]
[GOAL]
γ : Type u
f : Listβ γ Listα.nil → WType (Listβ γ)
⊢ PEmpty.elim = f
[PROOFSTEP]
ext x
[GOAL]
case h
γ : Type u
f : Listβ γ Listα.nil → WType (Listβ γ)
x : PEmpty
⊢ PEmpty.elim x = f x
[PROOFSTEP]
cases x
[GOAL]
γ : Type u
x : γ
f : Listβ γ (Listα.cons x) → WType (Listβ γ)
⊢ ofList γ (toList γ (mk (Listα.cons x) f)) = mk (Listα.cons x) f
[PROOFSTEP]
simp only [ofList, leftInverse_list (f PUnit.unit), mk.injEq, heq_eq_eq, true_and]
[GOAL]
γ : Type u
x : γ
f : Listβ γ (Listα.cons x) → WType (Listβ γ)
⊢ (fun x => f PUnit.unit) = f
[PROOFSTEP]
rfl
[GOAL]
γ : Type u
hd : γ
tl : List γ
⊢ toList γ (ofList γ (hd :: tl)) = hd :: tl
[PROOFSTEP]
simp only [toList, rightInverse_list tl]


[GOAL]
α : Type u
β : α → Type u
⊢ #(WType β) = sum fun a => #(WType β) ^ #(β a)
[PROOFSTEP]
simp only [Cardinal.power_def, ← Cardinal.mk_sigma]
[GOAL]
α : Type u
β : α → Type u
⊢ #(WType β) = #((i : α) × (β i → WType β))
[PROOFSTEP]
exact mk_congr (equivSigma β)
[GOAL]
α : Type u
β : α → Type u
κ : Cardinal.{u}
hκ : (sum fun a => κ ^ #(β a)) ≤ κ
⊢ #(WType β) ≤ κ
[PROOFSTEP]
induction' κ using Cardinal.inductionOn with γ
[GOAL]
case h
α : Type u
β : α → Type u
κ : Cardinal.{u}
hκ✝ : (sum fun a => κ ^ #(β a)) ≤ κ
γ : Type u
hκ : (sum fun a => #γ ^ #(β a)) ≤ #γ
⊢ #(WType β) ≤ #γ
[PROOFSTEP]
simp only [Cardinal.power_def, ← Cardinal.mk_sigma, Cardinal.le_def] at hκ
[GOAL]
case h
α : Type u
β : α → Type u
κ : Cardinal.{u}
hκ✝ : (sum fun a => κ ^ #(β a)) ≤ κ
γ : Type u
hκ : Nonempty ((i : α) × (β i → γ) ↪ γ)
⊢ #(WType β) ≤ #γ
[PROOFSTEP]
cases' hκ with hκ
[GOAL]
case h.intro
α : Type u
β : α → Type u
κ : Cardinal.{u}
hκ✝ : (sum fun a => κ ^ #(β a)) ≤ κ
γ : Type u
hκ : (i : α) × (β i → γ) ↪ γ
⊢ #(WType β) ≤ #γ
[PROOFSTEP]
exact Cardinal.mk_le_of_injective (elim_injective _ hκ.1 hκ.2)
[GOAL]
α : Type u
β : α → Type u
inst✝ : ∀ (a : α), Finite (β a)
⊢ IsEmpty α → #(WType β) ≤ max #α ℵ₀
[PROOFSTEP]
intro h
[GOAL]
α : Type u
β : α → Type u
inst✝ : ∀ (a : α), Finite (β a)
h : IsEmpty α
⊢ #(WType β) ≤ max #α ℵ₀
[PROOFSTEP]
rw [Cardinal.mk_eq_zero (WType β)]
[GOAL]
α : Type u
β : α → Type u
inst✝ : ∀ (a : α), Finite (β a)
h : IsEmpty α
⊢ 0 ≤ max #α ℵ₀
[PROOFSTEP]
exact zero_le _
[GOAL]
α : Type u
β : α → Type u
inst✝ : ∀ (a : α), Finite (β a)
hn : Nonempty α
m : Cardinal.{u} := max #α ℵ₀
⊢ Order.succ 0 ≤ ⨆ (a : α), m ^ #(β a)
[PROOFSTEP]
rw [succ_zero]
[GOAL]
α : Type u
β : α → Type u
inst✝ : ∀ (a : α), Finite (β a)
hn : Nonempty α
m : Cardinal.{u} := max #α ℵ₀
⊢ 1 ≤ ⨆ (a : α), m ^ #(β a)
[PROOFSTEP]
obtain ⟨a⟩ : Nonempty α := hn
[GOAL]
case intro
α : Type u
β : α → Type u
inst✝ : ∀ (a : α), Finite (β a)
m : Cardinal.{u} := max #α ℵ₀
a : α
⊢ 1 ≤ ⨆ (a : α), m ^ #(β a)
[PROOFSTEP]
refine' le_trans _ (le_ciSup (bddAbove_range.{u, u} _) a)
[GOAL]
case intro
α : Type u
β : α → Type u
inst✝ : ∀ (a : α), Finite (β a)
m : Cardinal.{u} := max #α ℵ₀
a : α
⊢ 1 ≤ m ^ #(β a)
[PROOFSTEP]
rw [← power_zero]
[GOAL]
case intro
α : Type u
β : α → Type u
inst✝ : ∀ (a : α), Finite (β a)
m : Cardinal.{u} := max #α ℵ₀
a : α
⊢ ?m.2506 ^ 0 ≤ m ^ #(β a)
α : Type u β : α → Type u inst✝ : ∀ (a : α), Finite (β a) m : Cardinal.{u} := max #α ℵ₀ a : α ⊢ Cardinal.{u}
[PROOFSTEP]
exact power_le_power_left (pos_iff_ne_zero.1 (aleph0_pos.trans_le (le_max_right _ _))) (zero_le _)


[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : One α
s : Finset α
a : α
inst✝² : DecidableEq β
inst✝¹ : One β
inst✝ : OneHomClass F α β
f : F
⊢ image (↑f) 1 = 1
[PROOFSTEP]
rw [image_one, map_one, singleton_one]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : DecidableEq α
inst✝ : InvolutiveInv α
s : Finset α
⊢ ↑(preimage s Inv.inv (_ : Set.InjOn Inv.inv (Inv.inv ⁻¹' ↑s))) = ↑s⁻¹
[PROOFSTEP]
rw [coe_preimage, Set.inv_preimage, coe_inv]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : Monoid α
s✝ t : Finset α
a : α
m n✝ : ℕ
s : Finset α
n : ℕ
⊢ ↑(s ^ n) = ↑s ^ n
[PROOFSTEP]
change ↑(npowRec n s) = (s : Set α) ^ n
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : Monoid α
s✝ t : Finset α
a : α
m n✝ : ℕ
s : Finset α
n : ℕ
⊢ ↑(npowRec n s) = ↑s ^ n
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : Monoid α
s✝ t : Finset α
a : α
m n : ℕ
s : Finset α
⊢ ↑(npowRec Nat.zero s) = ↑s ^ Nat.zero
[PROOFSTEP]
rw [npowRec, pow_zero, coe_one]
[GOAL]
case succ
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : Monoid α
s✝ t : Finset α
a : α
m n✝ : ℕ
s : Finset α
n : ℕ
ih : ↑(npowRec n s) = ↑s ^ n
⊢ ↑(npowRec (Nat.succ n) s) = ↑s ^ Nat.succ n
[PROOFSTEP]
rw [npowRec, pow_succ, coe_mul, ih]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : Monoid α
s t : Finset α
a : α
m n : ℕ
ha : a ∈ s
⊢ a ^ 0 ∈ s ^ 0
[PROOFSTEP]
rw [pow_zero]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : Monoid α
s t : Finset α
a : α
m n : ℕ
ha : a ∈ s
⊢ 1 ∈ s ^ 0
[PROOFSTEP]
exact one_mem_one
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : Monoid α
s t : Finset α
a : α
m n✝ : ℕ
ha : a ∈ s
n : ℕ
⊢ a ^ (n + 1) ∈ s ^ (n + 1)
[PROOFSTEP]
rw [pow_succ]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : Monoid α
s t : Finset α
a : α
m n✝ : ℕ
ha : a ∈ s
n : ℕ
⊢ a * a ^ n ∈ s ^ (n + 1)
[PROOFSTEP]
exact mul_mem_mul ha (pow_mem_pow ha n)
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : Monoid α
s t : Finset α
a : α
m n : ℕ
hst : s ⊆ t
⊢ s ^ 0 ⊆ t ^ 0
[PROOFSTEP]
simp [pow_zero]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : Monoid α
s t : Finset α
a : α
m n✝ : ℕ
hst : s ⊆ t
n : ℕ
⊢ s ^ (n + 1) ⊆ t ^ (n + 1)
[PROOFSTEP]
rw [pow_succ]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : Monoid α
s t : Finset α
a : α
m n✝ : ℕ
hst : s ⊆ t
n : ℕ
⊢ s * s ^ n ⊆ t ^ (n + 1)
[PROOFSTEP]
exact mul_subset_mul hst (pow_subset_pow hst n)
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : Monoid α
s t : Finset α
a : α
m n : ℕ
hs : 1 ∈ s
⊢ m ≤ n → s ^ m ⊆ s ^ n
[PROOFSTEP]
apply Nat.le_induction
[GOAL]
case base
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : Monoid α
s t : Finset α
a : α
m n : ℕ
hs : 1 ∈ s
⊢ s ^ m ⊆ s ^ m
[PROOFSTEP]
exact fun _ hn => hn
[GOAL]
case succ
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : Monoid α
s t : Finset α
a : α
m n : ℕ
hs : 1 ∈ s
⊢ ∀ (n : ℕ), m ≤ n → s ^ m ⊆ s ^ n → s ^ m ⊆ s ^ (n + 1)
[PROOFSTEP]
intro n _ hmn
[GOAL]
case succ
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : Monoid α
s t : Finset α
a : α
m n✝ : ℕ
hs : 1 ∈ s
n : ℕ
hn✝ : m ≤ n
hmn : s ^ m ⊆ s ^ n
⊢ s ^ m ⊆ s ^ (n + 1)
[PROOFSTEP]
rw [pow_succ]
[GOAL]
case succ
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : Monoid α
s t : Finset α
a : α
m n✝ : ℕ
hs : 1 ∈ s
n : ℕ
hn✝ : m ≤ n
hmn : s ^ m ⊆ s ^ n
⊢ s ^ m ⊆ s * s ^ n
[PROOFSTEP]
exact hmn.trans (subset_mul_right (s ^ n) hs)
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : Monoid α
s✝ t : Finset α
a✝ : α
m n : ℕ
a : α
s : Fin n → Finset α
⊢ a ∈ List.prod (List.ofFn s) ↔ ∃ f, List.prod (List.ofFn fun i => ↑(f i)) = a
[PROOFSTEP]
rw [← mem_coe, coe_list_prod, List.map_ofFn, Set.mem_prod_list_ofFn]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : Monoid α
s✝ t : Finset α
a✝ : α
m n : ℕ
a : α
s : Fin n → Finset α
⊢ (∃ f, List.prod (List.ofFn fun i => ↑(f i)) = a) ↔ ∃ f, List.prod (List.ofFn fun i => ↑(f i)) = a
[PROOFSTEP]
rfl
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : Monoid α
s t : Finset α
a✝ : α
m n✝ : ℕ
a : α
n : ℕ
⊢ a ∈ s ^ n ↔ ∃ f, List.prod (List.ofFn fun i => ↑(f i)) = a
[PROOFSTEP]
simp [← mem_coe, coe_pow, Set.mem_pow]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : Monoid α
s t : Finset α
a : α
m n : ℕ
hn : n ≠ 0
⊢ ∅ ^ n = ∅
[PROOFSTEP]
rw [← tsub_add_cancel_of_le (Nat.succ_le_of_lt <| Nat.pos_of_ne_zero hn), pow_succ, empty_mul]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : Monoid α
s t : Finset α
a : α
m n : ℕ
inst✝ : Fintype α
hn : n ≠ 0
⊢ ↑(univ ^ n) = ↑univ
[PROOFSTEP]
rw [coe_pow, coe_univ, Set.univ_pow hn]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DivisionMonoid α
s✝ t s : Finset α
n : ℕ
⊢ ↑(s ^ Int.negSucc n) = ↑s ^ Int.negSucc n
[PROOFSTEP]
refine' (coe_inv _).trans _
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DivisionMonoid α
s✝ t s : Finset α
n : ℕ
⊢ (↑(npowRec (Nat.succ n) s))⁻¹ = ↑s ^ Int.negSucc n
[PROOFSTEP]
exact congr_arg Inv.inv (coe_pow _ _)
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DivisionMonoid α
s t : Finset α
⊢ s * t = 1 ↔ ∃ a b, s = {a} ∧ t = {b} ∧ a * b = 1
[PROOFSTEP]
simp_rw [← coe_inj, coe_mul, coe_one, Set.mul_eq_one_iff, coe_singleton]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DivisionMonoid α
s t : Finset α
⊢ IsUnit s ↔ ∃ a, s = {a} ∧ IsUnit a
[PROOFSTEP]
constructor
[GOAL]
case mp
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DivisionMonoid α
s t : Finset α
⊢ IsUnit s → ∃ a, s = {a} ∧ IsUnit a
[PROOFSTEP]
rintro ⟨u, rfl⟩
[GOAL]
case mp.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DivisionMonoid α
t : Finset α
u : (Finset α)ˣ
⊢ ∃ a, ↑u = {a} ∧ IsUnit a
[PROOFSTEP]
obtain ⟨a, b, ha, hb, h⟩ := Finset.mul_eq_one_iff.1 u.mul_inv
[GOAL]
case mp.intro.intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DivisionMonoid α
t : Finset α
u : (Finset α)ˣ
a b : α
ha : ↑u = {a}
hb : ↑u⁻¹ = {b}
h : a * b = 1
⊢ ∃ a, ↑u = {a} ∧ IsUnit a
[PROOFSTEP]
refine' ⟨a, ha, ⟨a, b, h, singleton_injective _⟩, rfl⟩
[GOAL]
case mp.intro.intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DivisionMonoid α
t : Finset α
u : (Finset α)ˣ
a b : α
ha : ↑u = {a}
hb : ↑u⁻¹ = {b}
h : a * b = 1
⊢ {b * a} = {1}
[PROOFSTEP]
rw [← singleton_mul_singleton, ← ha, ← hb]
[GOAL]
case mp.intro.intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DivisionMonoid α
t : Finset α
u : (Finset α)ˣ
a b : α
ha : ↑u = {a}
hb : ↑u⁻¹ = {b}
h : a * b = 1
⊢ ↑u⁻¹ * ↑u = {1}
[PROOFSTEP]
exact u.inv_mul
[GOAL]
case mpr
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DivisionMonoid α
s t : Finset α
⊢ (∃ a, s = {a} ∧ IsUnit a) → IsUnit s
[PROOFSTEP]
rintro ⟨a, rfl, ha⟩
[GOAL]
case mpr.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DivisionMonoid α
t : Finset α
a : α
ha : IsUnit a
⊢ IsUnit {a}
[PROOFSTEP]
exact ha.finset
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DivisionMonoid α
s t : Finset α
⊢ IsUnit ↑s ↔ IsUnit s
[PROOFSTEP]
simp_rw [isUnit_iff, Set.isUnit_iff, coe_eq_singleton]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : MulZeroClass α
s✝ t s : Finset α
⊢ s * 0 ⊆ 0
[PROOFSTEP]
simp [subset_iff, mem_mul]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : MulZeroClass α
s✝ t s : Finset α
⊢ 0 * s ⊆ 0
[PROOFSTEP]
simp [subset_iff, mem_mul]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : MulZeroClass α
s t : Finset α
hs : Finset.Nonempty s
⊢ 0 ⊆ s * 0
[PROOFSTEP]
simpa [mem_mul] using hs
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : MulZeroClass α
s t : Finset α
hs : Finset.Nonempty s
⊢ 0 ⊆ 0 * s
[PROOFSTEP]
simpa [mem_mul] using hs
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : DecidableEq α
inst✝³ : DecidableEq β
inst✝² : Group α
inst✝¹ : DivisionMonoid β
inst✝ : MonoidHomClass F α β
f : F
s t : Finset α
a b : α
⊢ 1 ∈ s / t ↔ ¬Disjoint s t
[PROOFSTEP]
rw [← mem_coe, ← disjoint_coe, coe_div, Set.one_mem_div_iff]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : DecidableEq α
inst✝³ : DecidableEq β
inst✝² : Group α
inst✝¹ : DivisionMonoid β
inst✝ : MonoidHomClass F α β
f : F
s t : Finset α
a b : α
⊢ IsUnit s ↔ ∃ a, s = {a}
[PROOFSTEP]
simp only [isUnit_iff, Group.isUnit, and_true_iff]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : DecidableEq α
inst✝³ : DecidableEq β
inst✝² : Group α
inst✝¹ : DivisionMonoid β
inst✝ : MonoidHomClass F α β
f : F
s t : Finset α
a b : α
⊢ (∃ a, s = {a} ∧ IsUnit a) ↔ ∃ a, s = {a}
[PROOFSTEP]
simp only [Group.isUnit, and_true_iff]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : DecidableEq α
inst✝³ : DecidableEq β
inst✝² : Group α
inst✝¹ : DivisionMonoid β
inst✝ : MonoidHomClass F α β
f : F
s t : Finset α
a b : α
⊢ ↑(image (fun b => a * b) t) =
    ↑(preimage t (fun b => a⁻¹ * b) (_ : Set.InjOn ((fun x x_1 => x * x_1) a⁻¹) ((fun b => a⁻¹ * b) ⁻¹' ↑t)))
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : DecidableEq α
inst✝³ : DecidableEq β
inst✝² : Group α
inst✝¹ : DivisionMonoid β
inst✝ : MonoidHomClass F α β
f : F
s t : Finset α
a b : α
⊢ ↑(image (fun x => x * b) t) =
    ↑(preimage t (fun x => x * b⁻¹) (_ : Set.InjOn (fun x => x * b⁻¹) ((fun x => x * b⁻¹) ⁻¹' ↑t)))
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : DecidableEq α
inst✝³ : DecidableEq β
inst✝² : Group α
inst✝¹ : DivisionMonoid β
inst✝ : MonoidHomClass F α β
f : F
s t : Finset α
a b : α
⊢ image (fun b => a⁻¹ * b) t =
    preimage t (fun b => a * b) (_ : Set.InjOn ((fun x x_1 => x * x_1) a) ((fun b => a * b) ⁻¹' ↑t))
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : DecidableEq α
inst✝³ : DecidableEq β
inst✝² : Group α
inst✝¹ : DivisionMonoid β
inst✝ : MonoidHomClass F α β
f : F
s t : Finset α
a b : α
⊢ image (fun x => x * b⁻¹) t = preimage t (fun x => x * b) (_ : Set.InjOn (fun x => x * b) ((fun x => x * b) ⁻¹' ↑t))
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : GroupWithZero α
s✝ t s : Finset α
⊢ s / 0 ⊆ 0
[PROOFSTEP]
simp [subset_iff, mem_div]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : GroupWithZero α
s✝ t s : Finset α
⊢ 0 / s ⊆ 0
[PROOFSTEP]
simp [subset_iff, mem_div]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : GroupWithZero α
s t : Finset α
hs : Finset.Nonempty s
⊢ 0 ⊆ s / 0
[PROOFSTEP]
simpa [mem_div] using hs
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : GroupWithZero α
s t : Finset α
hs : Finset.Nonempty s
⊢ 0 ⊆ 0 / s
[PROOFSTEP]
simpa [mem_div] using hs
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : Group α
s t : Finset α
a b : α
⊢ preimage {b} ((fun x x_1 => x * x_1) a)
      (_ : Set.InjOn ((fun x x_1 => x * x_1) a) ((fun x x_1 => x * x_1) a ⁻¹' ↑{b})) =
    {a⁻¹ * b}
[PROOFSTEP]
classical rw [← image_mul_left', image_singleton]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : Group α
s t : Finset α
a b : α
⊢ preimage {b} ((fun x x_1 => x * x_1) a)
      (_ : Set.InjOn ((fun x x_1 => x * x_1) a) ((fun x x_1 => x * x_1) a ⁻¹' ↑{b})) =
    {a⁻¹ * b}
[PROOFSTEP]
rw [← image_mul_left', image_singleton]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : Group α
s t : Finset α
a b : α
⊢ preimage {b} (fun x => x * a) (_ : Set.InjOn (fun x => x * a) ((fun x => x * a) ⁻¹' ↑{b})) = {b * a⁻¹}
[PROOFSTEP]
classical rw [← image_mul_right', image_singleton]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : Group α
s t : Finset α
a b : α
⊢ preimage {b} (fun x => x * a) (_ : Set.InjOn (fun x => x * a) ((fun x => x * a) ⁻¹' ↑{b})) = {b * a⁻¹}
[PROOFSTEP]
rw [← image_mul_right', image_singleton]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : Group α
s t : Finset α
a b : α
⊢ preimage 1 ((fun x x_1 => x * x_1) a) (_ : Set.InjOn ((fun x x_1 => x * x_1) a) ((fun x x_1 => x * x_1) a ⁻¹' ↑1)) =
    {a⁻¹}
[PROOFSTEP]
classical rw [← image_mul_left', image_one, mul_one]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : Group α
s t : Finset α
a b : α
⊢ preimage 1 ((fun x x_1 => x * x_1) a) (_ : Set.InjOn ((fun x x_1 => x * x_1) a) ((fun x x_1 => x * x_1) a ⁻¹' ↑1)) =
    {a⁻¹}
[PROOFSTEP]
rw [← image_mul_left', image_one, mul_one]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : Group α
s t : Finset α
a b : α
⊢ preimage 1 (fun x => x * b) (_ : Set.InjOn (fun x => x * b) ((fun x => x * b) ⁻¹' ↑1)) = {b⁻¹}
[PROOFSTEP]
classical rw [← image_mul_right', image_one, one_mul]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : Group α
s t : Finset α
a b : α
⊢ preimage 1 (fun x => x * b) (_ : Set.InjOn (fun x => x * b) ((fun x => x * b) ⁻¹' ↑1)) = {b⁻¹}
[PROOFSTEP]
rw [← image_mul_right', image_one, one_mul]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : Group α
s t : Finset α
a b : α
⊢ preimage 1 ((fun x x_1 => x * x_1) a⁻¹)
      (_ : Set.InjOn ((fun x x_1 => x * x_1) a⁻¹) ((fun x x_1 => x * x_1) a⁻¹ ⁻¹' ↑1)) =
    {a}
[PROOFSTEP]
rw [preimage_mul_left_one, inv_inv]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : Group α
s t : Finset α
a b : α
⊢ preimage 1 (fun x => x * b⁻¹) (_ : Set.InjOn (fun x => x * b⁻¹) ((fun x => x * b⁻¹) ⁻¹' ↑1)) = {b}
[PROOFSTEP]
rw [preimage_mul_right_one, inv_inv]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : DecidableEq β
inst✝ : SMul α β
s s₁ s₂ t u : Finset β
a : α
b x : β
⊢ x ∈ a • s ↔ ∃ y, y ∈ s ∧ a • y = x
[PROOFSTEP]
simp only [Finset.smul_finset_def, and_assoc, mem_image, exists_prop, Prod.exists, mem_product]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : DecidableEq γ
inst✝² : SMul α γ
inst✝¹ : SMul β γ
inst✝ : SMulCommClass α β γ
a : α
s : Finset β
t : Finset γ
⊢ ↑(a • s • t) = ↑(s • a • t)
[PROOFSTEP]
simp only [coe_smul_finset, coe_smul, smul_comm]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : DecidableEq γ
inst✝² : SMul α γ
inst✝¹ : SMul β γ
inst✝ : SMulCommClass α β γ
s : Finset α
t : Finset β
u : Finset γ
⊢ ↑(s • t • u) = ↑(t • s • u)
[PROOFSTEP]
simp_rw [coe_smul, smul_comm]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : DecidableEq γ
inst✝³ : SMul α β
inst✝² : SMul α γ
inst✝¹ : SMul β γ
inst✝ : IsScalarTower α β γ
a : α
b : β
s : Finset γ
⊢ (a • b) • s = a • b • s
[PROOFSTEP]
simp only [← image_smul, image_image, smul_assoc, Function.comp]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : DecidableEq γ
inst✝⁴ : DecidableEq β
inst✝³ : SMul α β
inst✝² : SMul α γ
inst✝¹ : SMul β γ
inst✝ : IsScalarTower α β γ
a : α
s : Finset β
t : Finset γ
⊢ ↑((a • s) • t) = ↑(a • s • t)
[PROOFSTEP]
simp only [coe_smul_finset, coe_smul, smul_assoc]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : DecidableEq γ
inst✝⁴ : DecidableEq β
inst✝³ : SMul α β
inst✝² : SMul α γ
inst✝¹ : SMul β γ
inst✝ : IsScalarTower α β γ
a : Finset α
s : Finset β
t : Finset γ
⊢ ↑((a • s) • t) = ↑(a • s • t)
[PROOFSTEP]
simp only [coe_smul_finset, coe_smul, smul_assoc]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : DecidableEq γ
inst✝³ : DecidableEq β
inst✝² : SMul α β
inst✝¹ : SMul αᵐᵒᵖ β
inst✝ : IsCentralScalar α β
a : α
s : Finset β
⊢ ↑(op a • s) = ↑(a • s)
[PROOFSTEP]
simp only [coe_smul_finset, coe_smul, op_smul_eq_smul]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : DecidableEq γ
inst✝³ : DecidableEq β
inst✝² : DecidableEq α
inst✝¹ : Monoid α
inst✝ : MulAction α β
s : Finset β
⊢ image (fun b => 1 • b) s = s
[PROOFSTEP]
simp_rw [one_smul, image_id']
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : DecidableEq γ
inst✝⁴ : DecidableEq β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : NoZeroSMulDivisors α β
⊢ ∀ {c : Finset α} {x : Finset β}, c • x = 0 → c = 0 ∨ x = 0
[PROOFSTEP]
intro s t h
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : DecidableEq γ
inst✝⁴ : DecidableEq β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : NoZeroSMulDivisors α β
s : Finset α
t : Finset β
h : s • t = 0
⊢ s = 0 ∨ t = 0
[PROOFSTEP]
by_contra H
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : DecidableEq γ
inst✝⁴ : DecidableEq β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : NoZeroSMulDivisors α β
s : Finset α
t : Finset β
h : s • t = 0
H : ¬(s = 0 ∨ t = 0)
⊢ False
[PROOFSTEP]
have hst : (s • t).Nonempty := h.symm.subst zero_nonempty
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : DecidableEq γ
inst✝⁴ : DecidableEq β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : NoZeroSMulDivisors α β
s : Finset α
t : Finset β
h : s • t = 0
H : ¬(s = 0 ∨ t = 0)
hst : Finset.Nonempty (s • t)
⊢ False
[PROOFSTEP]
rw [← hst.of_smul_left.subset_zero_iff, ← hst.of_smul_right.subset_zero_iff] at H
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : DecidableEq γ
inst✝⁴ : DecidableEq β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : NoZeroSMulDivisors α β
s : Finset α
t : Finset β
h : s • t = 0
H : ¬(s ⊆ 0 ∨ t ⊆ 0)
hst : Finset.Nonempty (s • t)
⊢ False
[PROOFSTEP]
push_neg at H
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : DecidableEq γ
inst✝⁴ : DecidableEq β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : NoZeroSMulDivisors α β
s : Finset α
t : Finset β
h : s • t = 0
hst : Finset.Nonempty (s • t)
H : ¬s ⊆ 0 ∧ ¬t ⊆ 0
⊢ False
[PROOFSTEP]
simp_rw [not_subset, mem_zero] at H
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : DecidableEq γ
inst✝⁴ : DecidableEq β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : NoZeroSMulDivisors α β
s : Finset α
t : Finset β
h : s • t = 0
hst : Finset.Nonempty (s • t)
H : (∃ x, x ∈ s ∧ ¬x = 0) ∧ ∃ x, x ∈ t ∧ ¬x = 0
⊢ False
[PROOFSTEP]
obtain ⟨⟨a, hs, ha⟩, b, ht, hb⟩ := H
[GOAL]
case intro.intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : DecidableEq γ
inst✝⁴ : DecidableEq β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : NoZeroSMulDivisors α β
s : Finset α
t : Finset β
h : s • t = 0
hst : Finset.Nonempty (s • t)
a : α
hs : a ∈ s
ha : ¬a = 0
b : β
ht : b ∈ t
hb : ¬b = 0
⊢ False
[PROOFSTEP]
exact (eq_zero_or_eq_zero_of_smul_eq_zero <| mem_zero.1 <| subset_of_eq h <| smul_mem_smul hs ht).elim ha hb
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : DecidableEq β
inst✝³ : DecidableEq γ
inst✝² : SMul αᵐᵒᵖ β
inst✝¹ : SMul β γ
inst✝ : SMul α γ
a : α
s : Finset β
t : Finset γ
h : ∀ (a : α) (b : β) (c : γ), (op a • b) • c = b • a • c
⊢ (op a • s) • t = s • a • t
[PROOFSTEP]
ext
[GOAL]
case a
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : DecidableEq β
inst✝³ : DecidableEq γ
inst✝² : SMul αᵐᵒᵖ β
inst✝¹ : SMul β γ
inst✝ : SMul α γ
a : α
s : Finset β
t : Finset γ
h : ∀ (a : α) (b : β) (c : γ), (op a • b) • c = b • a • c
a✝ : γ
⊢ a✝ ∈ (op a • s) • t ↔ a✝ ∈ s • a • t
[PROOFSTEP]
simp [mem_smul, mem_smul_finset, h]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : LeftCancelSemigroup α
inst✝ : DecidableEq α
s✝ t✝ : Finset α
a : α
s : Set α
t : Finset α
⊢ (Set.PairwiseDisjoint s fun x => x • t) ↔ Set.InjOn (fun p => p.fst * p.snd) (s ×ˢ ↑t)
[PROOFSTEP]
simp_rw [← pairwiseDisjoint_coe, coe_smul_finset, Set.pairwiseDisjoint_smul_iff]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : DecidableEq β
inst✝¹ : Group α
inst✝ : MulAction α β
s t : Finset β
a : α
b : β
⊢ a⁻¹ • b ∈ s ↔ b ∈ a • s
[PROOFSTEP]
rw [← smul_mem_smul_finset_iff a, smul_inv_smul]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : DecidableEq β
inst✝¹ : Group α
inst✝ : MulAction α β
s t : Finset β
a : α
b : β
⊢ b ∈ a⁻¹ • s ↔ a • b ∈ s
[PROOFSTEP]
rw [← smul_mem_smul_finset_iff a, smul_inv_smul]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : DecidableEq β
inst✝¹ : Group α
inst✝ : MulAction α β
s t : Finset β
a : α
b : β
⊢ a • s ⊆ t ↔ s ⊆ a⁻¹ • t
[PROOFSTEP]
simp_rw [← coe_subset]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : DecidableEq β
inst✝¹ : Group α
inst✝ : MulAction α β
s t : Finset β
a : α
b : β
⊢ ↑(a • s) ⊆ ↑t ↔ ↑s ⊆ ↑(a⁻¹ • t)
[PROOFSTEP]
push_cast
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : DecidableEq β
inst✝¹ : Group α
inst✝ : MulAction α β
s t : Finset β
a : α
b : β
⊢ a • ↑s ⊆ ↑t ↔ ↑s ⊆ a⁻¹ • ↑t
[PROOFSTEP]
exact Set.set_smul_subset_iff
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : DecidableEq β
inst✝¹ : Group α
inst✝ : MulAction α β
s t : Finset β
a : α
b : β
⊢ s ⊆ a • t ↔ a⁻¹ • s ⊆ t
[PROOFSTEP]
simp_rw [← coe_subset]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : DecidableEq β
inst✝¹ : Group α
inst✝ : MulAction α β
s t : Finset β
a : α
b : β
⊢ ↑s ⊆ ↑(a • t) ↔ ↑(a⁻¹ • s) ⊆ ↑t
[PROOFSTEP]
push_cast
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : DecidableEq β
inst✝¹ : Group α
inst✝ : MulAction α β
s t : Finset β
a : α
b : β
⊢ ↑s ⊆ a • ↑t ↔ a⁻¹ • ↑s ⊆ ↑t
[PROOFSTEP]
exact Set.subset_set_smul_iff
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : DecidableEq β
inst✝² : Group α
inst✝¹ : MulAction α β
s✝ t : Finset β
a : α
b : β
inst✝ : Fintype β
s : Finset α
hs : Finset.Nonempty s
⊢ ↑(s • univ) = ↑univ
[PROOFSTEP]
push_cast
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : DecidableEq β
inst✝² : Group α
inst✝¹ : MulAction α β
s✝ t : Finset β
a : α
b : β
inst✝ : Fintype β
s : Finset α
hs : Finset.Nonempty s
⊢ ↑s • Set.univ = Set.univ
[PROOFSTEP]
exact Set.smul_univ hs
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : DecidableEq β
inst✝² : GroupWithZero α
inst✝¹ : MulAction α β
s✝ t : Finset β
a : α
b : β
inst✝ : Fintype β
s : Finset α
hs : ¬s ⊆ 0
⊢ ↑(s • univ) = ↑univ
[PROOFSTEP]
rw [← coe_subset] at hs
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : DecidableEq β
inst✝² : GroupWithZero α
inst✝¹ : MulAction α β
s✝ t : Finset β
a : α
b : β
inst✝ : Fintype β
s : Finset α
hs : ¬↑s ⊆ ↑0
⊢ ↑(s • univ) = ↑univ
[PROOFSTEP]
push_cast at hs ⊢
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : DecidableEq β
inst✝² : GroupWithZero α
inst✝¹ : MulAction α β
s✝ t : Finset β
a : α
b : β
inst✝ : Fintype β
s : Finset α
hs : ¬↑s ⊆ 0
⊢ ↑s • Set.univ = Set.univ
[PROOFSTEP]
exact Set.smul_univ₀ hs
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : DecidableEq β
inst✝² : GroupWithZero α
inst✝¹ : MulAction α β
s t : Finset β
a : α
b : β
inst✝ : Fintype β
ha : a ≠ 0
⊢ ↑(a • univ) = ↑univ
[PROOFSTEP]
push_cast
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : DecidableEq β
inst✝² : GroupWithZero α
inst✝¹ : MulAction α β
s t : Finset β
a : α
b : β
inst✝ : Fintype β
ha : a ≠ 0
⊢ a • Set.univ = Set.univ
[PROOFSTEP]
exact Set.smul_set_univ₀ ha
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMulWithZero α β
inst✝ : DecidableEq β
s✝ : Finset α
t : Finset β
s : Finset α
⊢ s • 0 ⊆ 0
[PROOFSTEP]
simp [subset_iff, mem_smul]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMulWithZero α β
inst✝ : DecidableEq β
s : Finset α
t✝ t : Finset β
⊢ 0 • t ⊆ 0
[PROOFSTEP]
simp [subset_iff, mem_smul]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMulWithZero α β
inst✝ : DecidableEq β
s : Finset α
t : Finset β
hs : Finset.Nonempty s
⊢ 0 ⊆ s • 0
[PROOFSTEP]
simpa [mem_smul] using hs
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMulWithZero α β
inst✝ : DecidableEq β
s : Finset α
t : Finset β
ht : Finset.Nonempty t
⊢ 0 ⊆ 0 • t
[PROOFSTEP]
simpa [mem_smul] using ht
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMulWithZero α β
inst✝ : DecidableEq β
s✝ : Finset α
t s : Finset β
h : Finset.Nonempty s
⊢ ↑(0 • s) = ↑0
[PROOFSTEP]
simpa using @Set.zero_smul_set α _ _ _ _ _ h
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : SMulWithZero α β
inst✝¹ : DecidableEq β
s : Finset α
t : Finset β
inst✝ : NoZeroSMulDivisors α β
a : α
⊢ 0 ∈ s • t ↔ 0 ∈ s ∧ Finset.Nonempty t ∨ 0 ∈ t ∧ Finset.Nonempty s
[PROOFSTEP]
rw [← mem_coe, coe_smul, Set.zero_mem_smul_iff]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : SMulWithZero α β
inst✝¹ : DecidableEq β
s : Finset α
t : Finset β
inst✝ : NoZeroSMulDivisors α β
a : α
⊢ 0 ∈ ↑s ∧ Set.Nonempty ↑t ∨ 0 ∈ ↑t ∧ Set.Nonempty ↑s ↔ 0 ∈ s ∧ Finset.Nonempty t ∨ 0 ∈ t ∧ Finset.Nonempty s
[PROOFSTEP]
rfl
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : SMulWithZero α β
inst✝¹ : DecidableEq β
s : Finset α
t : Finset β
inst✝ : NoZeroSMulDivisors α β
a : α
ha : a ≠ 0
⊢ 0 ∈ a • t ↔ 0 ∈ t
[PROOFSTEP]
rw [← mem_coe, coe_smul_finset, Set.zero_mem_smul_set_iff ha, mem_coe]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : Monoid α
inst✝² : AddGroup β
inst✝¹ : DistribMulAction α β
inst✝ : DecidableEq β
a : α
s : Finset α
t : Finset β
⊢ a • -t = -(a • t)
[PROOFSTEP]
simp only [← image_smul, ← image_neg, Function.comp, image_image, smul_neg]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : Monoid α
inst✝² : AddGroup β
inst✝¹ : DistribMulAction α β
inst✝ : DecidableEq β
a : α
s : Finset α
t : Finset β
⊢ s • -t = -(s • t)
[PROOFSTEP]
simp_rw [← image_neg]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : Monoid α
inst✝² : AddGroup β
inst✝¹ : DistribMulAction α β
inst✝ : DecidableEq β
a : α
s : Finset α
t : Finset β
⊢ s • image (fun x => -x) t = image (fun x => -x) (s • t)
[PROOFSTEP]
exact image_image₂_right_comm smul_neg
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : Ring α
inst✝² : AddCommGroup β
inst✝¹ : Module α β
inst✝ : DecidableEq β
s : Finset α
t : Finset β
a : α
⊢ -a • t = -(a • t)
[PROOFSTEP]
simp only [← image_smul, ← image_neg, image_image, neg_smul, Function.comp]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : Ring α
inst✝³ : AddCommGroup β
inst✝² : Module α β
inst✝¹ : DecidableEq β
s : Finset α
t : Finset β
a : α
inst✝ : DecidableEq α
⊢ -s • t = -(s • t)
[PROOFSTEP]
simp_rw [← image_neg]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : Ring α
inst✝³ : AddCommGroup β
inst✝² : Module α β
inst✝¹ : DecidableEq β
s : Finset α
t : Finset β
a : α
inst✝ : DecidableEq α
⊢ image (fun x => -x) s • t = image (fun x => -x) (s • t)
[PROOFSTEP]
exact image₂_image_left_comm neg_smul