awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Expand (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
n : ℕ
hn : 0 < n
g g' : MvPolynomial σ R
H :
  Eq (α := MvPolynomial σ R) ((expand n : (a : MvPolynomial σ R) → MvPolynomial σ R) g : MvPolynomial σ R)
    ((expand n : (a : MvPolynomial σ R) → MvPolynomial σ R) g' : MvPolynomial σ R)
⊢ g = g'
have a : ∀ (d : σ →₀ ℕ), coeff d g = coeff d g'
Tactic: ext d
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Expand (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
n : ℕ
hn : 0 < n
g g' : MvPolynomial σ R
H :
  Eq (α := MvPolynomial σ R) ((expand n : (a : MvPolynomial σ R) → MvPolynomial σ R) g : MvPolynomial σ R)
    ((expand n : (a : MvPolynomial σ R) → MvPolynomial σ R) g' : MvPolynomial σ R)
d : σ →₀ ℕ
⊢ coeff d g = coeff d g'
have a : coeff (n • d) ((expand n : (a : MvPolynomial σ R) → MvPolynomial σ R) g) = coeff d g'
Tactic: rw [← coeff_expand_smul _ (n.ne_zero_iff_zero_lt.mpr hn), H, coeff_expand_smul _
      (n.ne_zero_iff_zero_lt.mpr hn)]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Expand (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
n : ℕ
hn : 0 < n
g g' : MvPolynomial σ R
H :
  Eq (α := MvPolynomial σ R) ((expand n : (a : MvPolynomial σ R) → MvPolynomial σ R) g : MvPolynomial σ R)
    ((expand n : (a : MvPolynomial σ R) → MvPolynomial σ R) g' : MvPolynomial σ R)
d : σ →₀ ℕ
a : coeff (n • d) ((expand n : (a : MvPolynomial σ R) → MvPolynomial σ R) g) = coeff d g'
⊢ coeff d g = coeff d g'
have a₁ : coeff (n • d) ((expand n : (a : MvPolynomial σ R) → MvPolynomial σ R) g') = coeff d g'
Tactic: rw [← coeff_expand_smul _ (n.ne_zero_iff_zero_lt.mpr hn), H, coeff_expand_smul _
      (n.ne_zero_iff_zero_lt.mpr hn)]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Expand (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
n : ℕ
hn : 0 < n
g g' : MvPolynomial σ R
H :
  Eq (α := MvPolynomial σ R) ((expand n : (a : MvPolynomial σ R) → MvPolynomial σ R) g : MvPolynomial σ R)
    ((expand n : (a : MvPolynomial σ R) → MvPolynomial σ R) g' : MvPolynomial σ R)
d : σ →₀ ℕ
a : coeff (n • d) ((expand n : (a : MvPolynomial σ R) → MvPolynomial σ R) g) = coeff d g'
a₁ : coeff (n • d) ((expand n : (a : MvPolynomial σ R) → MvPolynomial σ R) g') = coeff d g'
⊢ coeff d g = coeff d g'
have a₂ : coeff d g' = coeff d g'
Tactic: rw [← coeff_expand_smul _ (n.ne_zero_iff_zero_lt.mpr hn), H, coeff_expand_smul _
      (n.ne_zero_iff_zero_lt.mpr hn)]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Expand (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
p : ℕ
hp : 0 < p
f : MvPolynomial σ R
r : R
⊢ Eq (α := MvPolynomial σ R) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) f : MvPolynomial σ R)
      ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) ↔
    f = (C : (a : R) → MvPolynomial σ R) r
have rw : Eq (α := MvPolynomial σ R) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) f : MvPolynomial σ R)
    ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) r) : MvPolynomial σ R) ↔
  f = (expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) r)
Tactic: rw [← expand_C, expand_inj hp, expand_C]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Expand (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
p : ℕ
hp : 0 < p
f : MvPolynomial σ R
r : R
rw :
  Eq (α := MvPolynomial σ R) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) f : MvPolynomial σ R)
      ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) r) : MvPolynomial σ R) ↔
    f = (expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) r)
p₁ : ℕ
⊢ Eq (α := MvPolynomial σ R) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) f : MvPolynomial σ R)
      ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) ↔
    f = (C : (a : R) → MvPolynomial σ R) r
have rw₁ : f = (C : (a : R) → MvPolynomial σ R) r ↔
  f = (expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) r)
Tactic: rw [← expand_C, expand_inj hp, expand_C]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Expand (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
p : ℕ
hp : 0 < p
f : MvPolynomial σ R
r : R
rw :
  Eq (α := MvPolynomial σ R) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) f : MvPolynomial σ R)
      ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) r) : MvPolynomial σ R) ↔
    f = (expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) r)
p₁ : ℕ
rw₁ :
  f = (C : (a : R) → MvPolynomial σ R) r ↔
    f = (expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) r)
⊢ Eq (α := MvPolynomial σ R) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) f : MvPolynomial σ R)
      ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) ↔
    f = (C : (a : R) → MvPolynomial σ R) r
have rw₂ : f = (C : (a : R) → MvPolynomial σ R) r ↔ f = (C : (a : R) → MvPolynomial σ R) r
Tactic: rw [← expand_C, expand_inj hp, expand_C]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Expand (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst : CommSemiring R
p : ℕ
f : σ → MvPolynomial τ R
⊢ AlgHom.comp (expand p) (bind₁ f) = bind₁ fun (i : σ) ↦ (expand p : (a : MvPolynomial τ R) → MvPolynomial τ R) (f i)
have hf : ∀ (i : σ),
  Eq (α := MvPolynomial τ R)
    ((AlgHom.comp (expand p) (bind₁ f) : (a : MvPolynomial σ R) → MvPolynomial τ R) (X i) : MvPolynomial τ R)
    ((bind₁ fun (i : σ) ↦ (expand p : (a : MvPolynomial τ R) → MvPolynomial τ R) (f i) :
          (a : MvPolynomial σ R) → MvPolynomial τ R)
        (X i) :
      MvPolynomial τ R)
Tactic: ext1 i
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Expand (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst : CommSemiring R
p : ℕ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
⊢ Eq (α := MvPolynomial τ R)
    ((expand p : (a : MvPolynomial τ R) → MvPolynomial τ R) ((bind₁ f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ) :
      MvPolynomial τ R)
    ((bind₁ fun (i : σ) ↦ (expand p : (a : MvPolynomial τ R) → MvPolynomial τ R) (f i) :
          (a : MvPolynomial σ R) → MvPolynomial τ R)
        φ :
      MvPolynomial τ R)
have rw : Eq (α := MvPolynomial τ R)
  ((AlgHom.comp (expand p) (bind₁ f) : (a : MvPolynomial σ R) → MvPolynomial τ R) φ : MvPolynomial τ R)
  ((bind₁ fun (i : σ) ↦ (expand p : (a : MvPolynomial τ R) → MvPolynomial τ R) (f i) :
        (a : MvPolynomial σ R) → MvPolynomial τ R)
      φ :
    MvPolynomial τ R)
Tactic: rw [← AlgHom.comp_apply, expand_comp_bind₁]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Expand (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst : CommSemiring R
p : ℕ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
rw :
  Eq (α := MvPolynomial τ R)
    ((AlgHom.comp (expand p) (bind₁ f) : (a : MvPolynomial σ R) → MvPolynomial τ R) φ : MvPolynomial τ R)
    ((bind₁ fun (i : σ) ↦ (expand p : (a : MvPolynomial τ R) → MvPolynomial τ R) (f i) :
          (a : MvPolynomial σ R) → MvPolynomial τ R)
        φ :
      MvPolynomial τ R)
⊢ Eq (α := MvPolynomial τ R)
    ((expand p : (a : MvPolynomial τ R) → MvPolynomial τ R) ((bind₁ f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ) :
      MvPolynomial τ R)
    ((bind₁ fun (i : σ) ↦ (expand p : (a : MvPolynomial τ R) → MvPolynomial τ R) (f i) :
          (a : MvPolynomial σ R) → MvPolynomial τ R)
        φ :
      MvPolynomial τ R)
have rw₁ : Eq (α := MvPolynomial τ R)
  ((bind₁ fun (i : σ) ↦ (expand p : (a : MvPolynomial τ R) → MvPolynomial τ R) (f i) :
        (a : MvPolynomial σ R) → MvPolynomial τ R)
      φ :
    MvPolynomial τ R)
  ((bind₁ fun (i : σ) ↦ (expand p : (a : MvPolynomial τ R) → MvPolynomial τ R) (f i) :
        (a : MvPolynomial σ R) → MvPolynomial τ R)
      φ :
    MvPolynomial τ R)
Tactic: rw [← AlgHom.comp_apply, expand_comp_bind₁]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Expand (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst : CommSemiring R
p : ℕ
f : σ → τ
⊢ Eq (α := MvPolynomial σ R →ₐ[R] MvPolynomial τ R) (AlgHom.comp (rename f) (expand p))
    (AlgHom.comp (expand p) (rename f))
have hf : ∀ (i : σ),
  Eq (α := MvPolynomial τ R)
    ((AlgHom.comp (rename f) (expand p) : (a : MvPolynomial σ R) → MvPolynomial τ R) (X i) : MvPolynomial τ R)
    ((AlgHom.comp (expand p) (rename f) : (a : MvPolynomial σ R) → MvPolynomial τ R) (X i) : MvPolynomial τ R)
Tactic: ext1 i
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Expand (goal)
Goal:
σ : Type u_1
R : Type u_3
S : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
p : ℕ
f : R →+* S
g : σ → S
⊢ (eval₂Hom f g).comp (↑(expand p) : MvPolynomial σ R →+* MvPolynomial σ R) = eval₂Hom f (g ^ p)
have hC : ∀ (x : R),
  Eq.{u_4 + 1} (α := S)
    ((RingHom.comp ((eval₂Hom f g).comp (↑(expand p) : MvPolynomial σ R →+* MvPolynomial σ R)) C : (a : R) → S) x : S)
    (((eval₂Hom f (g ^ p)).comp C : (a : R) → S) x : S)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Expand (goal)
Goal:
σ : Type u_1
R : Type u_3
S : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
p : ℕ
f : R →+* S
g : σ → S
hC :
  ∀ (x : R),
    Eq.{u_4 + 1} (α := S)
      ((RingHom.comp ((eval₂Hom f g).comp (↑(expand p) : MvPolynomial σ R →+* MvPolynomial σ R)) C : (a : R) → S) x : S)
      (((eval₂Hom f (g ^ p)).comp C : (a : R) → S) x : S)
⊢ (eval₂Hom f g).comp (↑(expand p) : MvPolynomial σ R →+* MvPolynomial σ R) = eval₂Hom f (g ^ p)
have hX : ∀ (i : σ),
  Eq.{u_4 + 1} (α := S)
    (((eval₂Hom f g).comp (↑(expand p) : MvPolynomial σ R →+* MvPolynomial σ R) : (a : MvPolynomial σ R) → S) (X i) : S)
    ((eval₂Hom f (g ^ p) : (a : MvPolynomial σ R) → S) (X i) : S)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Expand (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
p : ℕ
A : Type u_5
inst_1 : CommSemiring A
inst_2 : Algebra R A
f : σ → A
⊢ Eq (α := MvPolynomial σ R →ₐ[R] A) (AlgHom.comp (aeval f) (expand p)) (aeval (f ^ p))
have hf : ∀ (i : σ),
  Eq.{u_5 + 1} (α := A) ((AlgHom.comp (aeval f) (expand p) : (a : MvPolynomial σ R) → A) (X i) : A)
    ((aeval (f ^ p) : (a : MvPolynomial σ R) → A) (X i) : A)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Expand (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
p : ℕ
φ : MvPolynomial σ R
inst_1 : DecidableEq σ
| support.{u_3, u_1} (R := R) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) φ)
have rw : support.{u_3, u_1} (R := R)
  ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R)
    (∑ v ∈ φ.support, (monomial v : (a : R) → MvPolynomial σ R) (coeff v φ)))
Tactic: rw [φ.as_sum]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Expand (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
p : ℕ
φ : MvPolynomial σ R
inst_1 : DecidableEq σ
⊢ Subset (α := Finset (σ →₀ ℕ)) (support.{u_3, u_1} (R := R) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) φ))
    (Finset.image (fun (x : σ →₀ ℕ) ↦ p • x) φ.support)
have conv_lhs : Subset (α := Finset (σ →₀ ℕ))
  (support.{u_3, u_1} (R := R)
    ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R)
      (∑ v ∈ φ.support, (monomial v : (a : R) → MvPolynomial σ R) (coeff v φ))))
  (Finset.image (fun (x : σ →₀ ℕ) ↦ p • x) φ.support)
Tactic: conv_lhs => rw [φ.as_sum]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Expand (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
p : ℕ
φ : MvPolynomial σ R
inst_1 : DecidableEq σ
⊢ Subset (α := Finset (σ →₀ ℕ))
    (support.{u_3, u_1} (R := R)
      ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R)
        (∑ v ∈ φ.support, (monomial v : (a : R) → MvPolynomial σ R) (coeff v φ))))
    (Finset.image (fun (x : σ →₀ ℕ) ↦ p • x) φ.support)
have simp : Subset (α := Finset (σ →₀ ℕ))
  (support.{u_3, u_1} (R := R) (∑ x ∈ φ.support, (monomial (p • x) : (a : R) → MvPolynomial σ R) (coeff x φ)))
  (Finset.image (fun (x : σ →₀ ℕ) ↦ p • x) φ.support)
Tactic: simp only [map_sum, expand_monomial]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Expand (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
p : ℕ
φ : MvPolynomial σ R
inst_1 : DecidableEq σ
⊢ Subset (α := Finset (σ →₀ ℕ))
    (support.{u_3, u_1} (R := R) (∑ x ∈ φ.support, (monomial (p • x) : (a : R) → MvPolynomial σ R) (coeff x φ)))
    (Finset.image (fun (x : σ →₀ ℕ) ↦ p • x) φ.support)
have refine : Subset (α := Finset (σ →₀ ℕ))
  (φ.support.biUnion fun (x : σ →₀ ℕ) ↦
    support.{u_3, u_1} (R := R) ((monomial (p • x) : (a : R) → MvPolynomial σ R) (coeff x φ)))
  (Finset.image (fun (x : σ →₀ ℕ) ↦ p • x) φ.support)
Tactic: refine MvPolynomial.support_sum.trans ?_
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Expand (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
p : ℕ
φ : MvPolynomial σ R
m : σ →₀ ℕ
i : σ
h : ¬p ∣ (m : (a : σ) → ℕ) i
⊢ Eq.{u_3 + 1} (α := R) (coeff m ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) φ)) 0
have contrapose! : ∀ (h : Ne.{u_3 + 1} (α := R) (coeff m ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) φ)) 0),
  p ∣ (m : (a : σ) → ℕ) i
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Expand (hypothesis)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
p : ℕ
φ : MvPolynomial σ R
m : σ →₀ ℕ
i : σ
h : Ne.{u_3 + 1} (α := R) (coeff m ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) φ)) 0
⊢ p ∣ (m : (a : σ) → ℕ) i
have h₁ : ∃ a ∈ φ.support, p • a = m
Tactic: grw [← mem_support_iff, support_expand_subset, Finset.mem_image] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Expand (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
p : ℕ
φ : MvPolynomial σ R
m : σ →₀ ℕ
i : σ
h : ∃ a ∈ φ.support, p • a = m
⊢ p ∣ (m : (a : σ) → ℕ) i
have rcases : ∀ (a : σ →₀ ℕ), p ∣ (p • a : (a : σ) → ℕ) i
Tactic: rcases h with ⟨a, -, rfl⟩
Cleared hypotheses: m, h
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Expand (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
p : ℕ
φ : MvPolynomial σ R
m : σ →₀ ℕ
i : σ
h : ¬p ∣ (m : (a : σ) → ℕ) i
⊢ Eq.{u_3 + 1} (α := R) (coeff m ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) φ)) 0
have contrapose! : ∀ (h : ¬p ∣ (m : (a : σ) → ℕ) i),
  Eq.{u_3 + 1} (α := R) (coeff m ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) φ)) 0
Tactic: classical
  contrapose! h
  grw [← mem_support_iff, support_expand_subset, Finset.mem_image] at h
  rcases h with ⟨a, -, rfl⟩
  exact ⟨a i, by simp⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Expand (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
p : ℕ
φ : MvPolynomial σ R
m : σ →₀ ℕ
i : σ
h : ¬p ∣ (m : (a : σ) → ℕ) i
contrapose! contrapose!₁ :
  ∀ (h : ¬p ∣ (m : (a : σ) → ℕ) i),
    Eq.{u_3 + 1} (α := R) (coeff m ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) φ)) 0
⊢ Eq.{u_3 + 1} (α := R) (coeff m ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) φ)) 0
have contrapose!₂ : Ne.{u_3 + 1} (α := R) (coeff m ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) φ)) 0 → p ∣ (m : (a : σ) → ℕ) i
Tactic: classical
  contrapose! h
  grw [← mem_support_iff, support_expand_subset, Finset.mem_image] at h
  rcases h with ⟨a, -, rfl⟩
  exact ⟨a i, by simp⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Expand (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
p : ℕ
φ : MvPolynomial σ R
m : σ →₀ ℕ
i : σ
h : ¬p ∣ (m : (a : σ) → ℕ) i
contrapose! contrapose!₁ :
  ∀ (h : ¬p ∣ (m : (a : σ) → ℕ) i),
    Eq.{u_3 + 1} (α := R) (coeff m ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) φ)) 0
contrapose!₂ contrapose!₃ contrapose!₄ :
  ∀ (h : Ne.{u_3 + 1} (α := R) (coeff m ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) φ)) 0),
    p ∣ (m : (a : σ) → ℕ) i
⊢ Eq.{u_3 + 1} (α := R) (coeff m ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) φ)) 0
have contrapose!₅ : ∀ (h : ∃ a ∈ φ.support, p • a = m), p ∣ (m : (a : σ) → ℕ) i
Tactic: classical
  contrapose! h
  grw [← mem_support_iff, support_expand_subset, Finset.mem_image] at h
  rcases h with ⟨a, -, rfl⟩
  exact ⟨a i, by simp⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Expand (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
p : ℕ
φ : MvPolynomial σ R
m : σ →₀ ℕ
i : σ
h : ¬p ∣ (m : (a : σ) → ℕ) i
contrapose! contrapose!₁ :
  ∀ (h : ¬p ∣ (m : (a : σ) → ℕ) i),
    Eq.{u_3 + 1} (α := R) (coeff m ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) φ)) 0
contrapose!₂ contrapose!₃ contrapose!₄ :
  ∀ (h : Ne.{u_3 + 1} (α := R) (coeff m ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) φ)) 0),
    p ∣ (m : (a : σ) → ℕ) i
contrapose!₅ : ∀ (h : ∃ a ∈ φ.support, p • a = m), p ∣ (m : (a : σ) → ℕ) i
⊢ Eq.{u_3 + 1} (α := R) (coeff m ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) φ)) 0
have contrapose!₆ : ∀ (a : σ →₀ ℕ), p ∣ (p • a : (a : σ) → ℕ) i
Tactic: classical
  contrapose! h
  grw [← mem_support_iff, support_expand_subset, Finset.mem_image] at h
  rcases h with ⟨a, -, rfl⟩
  exact ⟨a i, by simp⟩
Cleared hypotheses: m, h
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Expand (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
p : ℕ
φ : MvPolynomial σ R
inst_1 : DecidableEq σ
hp : p ≠ 0
⊢ Eq (α := Finset (σ →₀ ℕ)) (support.{u_3, u_1} (R := R) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) φ))
    (Finset.image (fun (x : σ →₀ ℕ) ↦ p • x) φ.support)
have refine : Subset (α := Finset (σ →₀ ℕ)) (Finset.image (fun (x : σ →₀ ℕ) ↦ p • x) φ.support)
  (support.{u_3, u_1} (R := R) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) φ))
Tactic: refine (support_expand_subset φ).antisymm ?_
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Expand (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
p : ℕ
f : MvPolynomial σ R
⊢ totalDegree.{u_3, u_1} (R := R) (σ := σ) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) f) =
    f.totalDegree * p
have inl : ∀ (hp : p = 0),
  totalDegree.{u_3, u_1} (R := R) (σ := σ) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) f) =
    f.totalDegree * p
Tactic: rcases p.eq_zero_or_pos with hp | hp
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Expand (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
p : ℕ
f : MvPolynomial σ R
inl :
  ∀ (hp : p = 0),
    totalDegree.{u_3, u_1} (R := R) (σ := σ) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) f) =
      f.totalDegree * p
⊢ totalDegree.{u_3, u_1} (R := R) (σ := σ) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) f) =
    f.totalDegree * p
have inr : ∀ (hp : p > 0),
  totalDegree.{u_3, u_1} (R := R) (σ := σ) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) f) =
    f.totalDegree * p
Tactic: rcases p.eq_zero_or_pos with hp | hp
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Expand (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
p : ℕ
f : MvPolynomial σ R
hp : p > 0
⊢ totalDegree.{u_3, u_1} (R := R) (σ := σ) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) f) =
    f.totalDegree * p
have pos : ∀ (hf : f = 0),
  totalDegree.{u_3, u_1} (R := R) (σ := σ) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) f) =
    f.totalDegree * p
Tactic: by_cases hf : f = 0
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Expand (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
p : ℕ
f : MvPolynomial σ R
hp : p > 0
pos :
  ∀ (hf : f = 0),
    totalDegree.{u_3, u_1} (R := R) (σ := σ) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) f) =
      f.totalDegree * p
⊢ totalDegree.{u_3, u_1} (R := R) (σ := σ) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) f) =
    f.totalDegree * p
have neg : ∀ (hf : ¬f = 0),
  totalDegree.{u_3, u_1} (R := R) (σ := σ) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) f) =
    f.totalDegree * p
Tactic: by_cases hf : f = 0
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Expand (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
p : ℕ
f : MvPolynomial σ R
hp : p > 0
hf : f = 0
⊢ totalDegree.{u_3, u_1} (R := R) (σ := σ) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) f) =
    f.totalDegree * p
have pos : totalDegree.{u_3, u_1} (R := R) (σ := σ) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) 0) =
  totalDegree.{u_3, u_1} (R := R) (σ := σ) 0 * p
Tactic: rw [hf, map_zero, totalDegree_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Expand (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
p : ℕ
f : MvPolynomial σ R
hp : p > 0
hf : f = 0
pos :
  totalDegree.{u_3, u_1} (R := R) (σ := σ) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) 0) =
    totalDegree.{u_3, u_1} (R := R) (σ := σ) 0 * p
⊢ totalDegree.{u_3, u_1} (R := R) (σ := σ) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) f) =
    f.totalDegree * p
have pos₁ : totalDegree.{u_3, u_1} (R := R) (σ := σ) 0 = totalDegree.{u_3, u_1} (R := R) (σ := σ) 0 * p
Tactic: rw [hf, map_zero, totalDegree_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Expand (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
p : ℕ
f : MvPolynomial σ R
hp : p > 0
hf : f = 0
pos :
  totalDegree.{u_3, u_1} (R := R) (σ := σ) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) 0) =
    totalDegree.{u_3, u_1} (R := R) (σ := σ) 0 * p
pos₁ : totalDegree.{u_3, u_1} (R := R) (σ := σ) 0 = totalDegree.{u_3, u_1} (R := R) (σ := σ) 0 * p
⊢ totalDegree.{u_3, u_1} (R := R) (σ := σ) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) f) =
    f.totalDegree * p
have pos₂ : 0 = 0 * p
Tactic: rw [hf, map_zero, totalDegree_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Expand (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
p : ℕ
f : MvPolynomial σ R
hp : p > 0
hf : f = 0
pos :
  totalDegree.{u_3, u_1} (R := R) (σ := σ) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) 0) =
    totalDegree.{u_3, u_1} (R := R) (σ := σ) 0 * p
pos₁ : totalDegree.{u_3, u_1} (R := R) (σ := σ) 0 = totalDegree.{u_3, u_1} (R := R) (σ := σ) 0 * p
pos₂ : 0 = 0 * p
⊢ totalDegree.{u_3, u_1} (R := R) (σ := σ) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) f) =
    f.totalDegree * p
have pos₃ : Eq (α := ℕ) 0 0
Tactic: rw [hf, map_zero, totalDegree_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Expand (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
p : ℕ
f : MvPolynomial σ R
hp : p > 0
hf : ¬f = 0
⊢ totalDegree.{u_3, u_1} (R := R) (σ := σ) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) f) =
    f.totalDegree * p
have neg : (Finset.sup (Finset.image (fun (x : σ →₀ ℕ) ↦ p • x) f.support) fun (m : σ →₀ ℕ) ↦
    Multiset.card.{u_1} (α := σ) ((Finsupp.toMultiset : (a : σ →₀ ℕ) → Multiset σ) m)) =
  (f.support.sup fun (m : σ →₀ ℕ) ↦ Multiset.card.{u_1} (α := σ) ((Finsupp.toMultiset : (a : σ →₀ ℕ) → Multiset σ) m)) *
    p
Tactic: simp_rw [totalDegree_eq, support_expand _ (p.ne_zero_iff_zero_lt.mpr hp)]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Expand (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
p : ℕ
f : MvPolynomial σ R
hp : p > 0
hf : ¬f = 0
⊢ (Finset.sup (Finset.image (fun (x : σ →₀ ℕ) ↦ p • x) f.support) fun (m : σ →₀ ℕ) ↦
      Multiset.card.{u_1} (α := σ) ((Finsupp.toMultiset : (a : σ →₀ ℕ) → Multiset σ) m)) =
    (f.support.sup fun (m : σ →₀ ℕ) ↦
        Multiset.card.{u_1} (α := σ) ((Finsupp.toMultiset : (a : σ →₀ ℕ) → Multiset σ) m)) *
      p
have neg : Eq (α := ℕ) (f.support.sup fun (x : σ →₀ ℕ) ↦ (p • x).sum fun (x : σ) ↦ id)
  (f.support.sup fun (x : σ →₀ ℕ) ↦ (x.sum fun (x : σ) ↦ id) * p)
Tactic: simp only [Finsupp.card_toMultiset, Finset.sup_image, Finset.sup_mul₀, Function.comp_def]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Expand (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
p : ℕ
f : MvPolynomial σ R
hp : p > 0
hf : ¬f = 0
⊢ Eq (α := ℕ) (f.support.sup fun (x : σ →₀ ℕ) ↦ (p • x).sum fun (x : σ) ↦ id)
    (f.support.sup fun (x : σ →₀ ℕ) ↦ (x.sum fun (x : σ) ↦ id) * p)
have neg : ∀ (d : σ →₀ ℕ), ((p • d).sum fun (x : σ) ↦ id) = (d.sum fun (x : σ) ↦ id) * p
Tactic: congr! 2 with d