awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
hφ : φ.IsHomogeneous n
d : σ →₀ ℕ
hd : d ∈ φ.support
⊢ coeff d φ ≠ 0

Tactic:
rw [mem_support_iff] at hd

Premises used: MvPolynomial.mem_support_iff
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
hφ : φ.IsHomogeneous n
d : σ →₀ ℕ
hd : coeff d φ ≠ 0
a : ∑ x ∈ d.support, (d : (a : σ) → ℕ) x ≤ n
a₁ : LE.le (α := ℕ) (∑ x ∈ d.support, (d : (a : σ) → ℕ) x : ℕ) ((weight 1 : (a : σ →₀ ℕ) → ℕ) d : ℕ)
a₂ : LE.le (α := ℕ) (∑ x ∈ d.support, (d : (a : σ) → ℕ) x) (d.sum fun (i : σ) (c : ℕ) ↦ HSMul.hSMul (β := ℕ) c (1 i))
a₃ : LE.le (α := ℕ) (∑ x ∈ d.support, (d : (a : σ) → ℕ) x) (d.sum fun (i : σ) (c : ℕ) ↦ HSMul.hSMul (β := ℕ) c 1)
a₄ : LE.le (α := ℕ) (∑ x ∈ d.support, (d : (a : σ) → ℕ) x) (d.sum fun (i : σ) (c : ℕ) ↦ c * 1)
a₅ : LE.le (α := ℕ) (∑ x ∈ d.support, (d : (a : σ) → ℕ) x) (d.sum fun (i : σ) (c : ℕ) ↦ c)
a₆ : LE.le (α := ℕ) (∑ x ∈ d.support, (d : (a : σ) → ℕ) x) (∑ x ∈ d.support, (d : (a : σ) → ℕ) x)
⊢ (d.sum fun (x : σ) (e : ℕ) ↦ e) ≤ n

Tactic:
simp_rw [Finsupp.sum, ← hφ hd, weight_apply, Pi.one_apply, smul_eq_mul, mul_one, Finsupp.sum,
    le_rfl]

Premises used: le_rfl, Pi.one_apply, Finsupp.sum, smul_eq_mul, mul_one, Finsupp.weight_apply
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
hφ : φ.IsHomogeneous n
h : φ ≠ 0
apply : n ≤ φ.totalDegree
⊢ φ.totalDegree = n

Tactic:
apply le_antisymm hφ.totalDegree_le

Premises used: MvPolynomial.IsHomogeneous.totalDegree_le, le_antisymm
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
hφ : φ.IsHomogeneous n
h : φ ≠ 0
⊢ ∃ (d : σ →₀ ℕ), coeff d φ ≠ 0

Tactic:
exists_coeff_ne_zero h

Premises used: MvPolynomial.exists_coeff_ne_zero
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
hφ : φ.IsHomogeneous n
h : φ ≠ 0
obtain : ∀ (d : σ →₀ ℕ) (hd : coeff d φ ≠ 0), n ≤ φ.totalDegree
⊢ n ≤ φ.totalDegree

Tactic:
obtain ⟨d, hd⟩ : ∃ d, coeff d φ ≠ 0 := exists_coeff_ne_zero h

Premises used: MvPolynomial.exists_coeff_ne_zero
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
hφ : φ.IsHomogeneous n
h : φ ≠ 0
d : σ →₀ ℕ
hd : coeff d φ ≠ 0
simp :
  LE.le (α := ℕ) ((weight 1 : (a : σ →₀ ℕ) → ℕ) d : ℕ)
    (φ.support.sup fun (s : σ →₀ ℕ) ↦ ∑ x ∈ s.support, (s : (a : σ) → ℕ) x : ℕ)
⊢ n ≤ φ.totalDegree

Tactic:
simp only [← hφ hd, MvPolynomial.totalDegree, Finsupp.sum]

Premises used: Finsupp.sum, MvPolynomial.totalDegree
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
hφ : φ.IsHomogeneous n
h : φ ≠ 0
d : σ →₀ ℕ
hd : coeff d φ ≠ 0
⊢ d ∈ φ.support

Tactic:
replace hd := Finsupp.mem_support_iff.mpr hd
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
hφ : φ.IsHomogeneous n
h : φ ≠ 0
d : σ →₀ ℕ
hd : d ∈ φ.support
simp :
  LE.le (α := ℕ) (d.sum fun (i : σ) (c : ℕ) ↦ c) (φ.support.sup fun (s : σ →₀ ℕ) ↦ ∑ x ∈ s.support, (s : (a : σ) → ℕ) x)
⊢ LE.le (α := ℕ) ((weight 1 : (a : σ →₀ ℕ) → ℕ) d : ℕ)
    (φ.support.sup fun (s : σ →₀ ℕ) ↦ ∑ x ∈ s.support, (s : (a : σ) → ℕ) x : ℕ)

Tactic:
simp only [weight_apply, Pi.one_apply, smul_eq_mul, mul_one]

Premises used: Pi.one_apply, smul_eq_mul, mul_one, Finsupp.weight_apply
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
hφ : φ.IsHomogeneous n
h : φ ≠ 0
d : σ →₀ ℕ
hd : d ∈ φ.support
⊢ LE.le (α := ℕ) (d.sum fun (i : σ) (c : ℕ) ↦ c) (φ.support.sup fun (s : σ →₀ ℕ) ↦ ∑ x ∈ s.support, (s : (a : σ) → ℕ) x)

Tactic:
Finset.le_sup (f := fun s ↦ ∑ x ∈ s.support, s x) hd

Premises used: Finsupp.sum, MvPolynomial.support, Finset.le_sup
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
hφ : φ.IsHomogeneous n
h : φ ≠ 0
d : σ →₀ ℕ
hd : d ∈ φ.support
⊢ LE.le (α := ℕ) (d.sum fun (i : σ) (c : ℕ) ↦ c) (φ.support.sup fun (s : σ →₀ ℕ) ↦ ∑ x ∈ s.support, (s : (a : σ) → ℕ) x)

Tactic:
exact Finset.le_sup (f := fun s ↦ ∑ x ∈ s.support, s x) hd

Premises used: Finset.le_sup
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
hφ : φ.IsHomogeneous n
s : σ →₀ ℕ
hs : s ∈ φ.support
⊢ n = ∑ i ∈ s.support, (s : (a : σ) → ℕ) i

Tactic:
simp [← hφ <| mem_support_iff.mp hs, ← degree_apply, degree_eq_weight_one, Pi.one_def]

Premises used: MvPolynomial.mem_support_iff, Finsupp.degree_apply, Finsupp.degree_eq_weight_one, Pi.one_def, Iff.mp
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
f : σ → τ
h : φ.IsHomogeneous n
rw :
  IsHomogeneous.{u_2, u_3} (σ := τ) (R := R)
    (∑ x ∈ φ.support,
      (rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) ((monomial x : (a : R) → MvPolynomial σ R) (coeff x φ)))
    n
⊢ IsHomogeneous.{u_2, u_3} (σ := τ) (R := R) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ) n

Tactic:
rw [← φ.support_sum_monomial_coeff, map_sum]

Premises used: map_sum, MvPolynomial.support_sum_monomial_coeff
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
f : σ → τ
h : φ.IsHomogeneous n
simp_rw :
  IsHomogeneous.{u_2, u_3} (σ := τ) (R := R)
    (∑ x ∈ φ.support, (monomial (mapDomain f x) : (a : R) → MvPolynomial τ R) (coeff x φ)) n
⊢ IsHomogeneous.{u_2, u_3} (σ := τ) (R := R)
    (∑ x ∈ φ.support,
      (rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) ((monomial x : (a : R) → MvPolynomial σ R) (coeff x φ)))
    n

Tactic:
simp_rw [rename_monomial]

Premises used: MvPolynomial.rename_monomial
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
f : σ → τ
h : φ.IsHomogeneous n
apply : ∀ (d : σ →₀ ℕ) (hd : d ∈ φ.support), (degree : (a : τ →₀ ℕ) → ℕ) (mapDomain f d) = n
⊢ IsHomogeneous.{u_2, u_3} (σ := τ) (R := R)
    (∑ x ∈ φ.support, (monomial (mapDomain f x) : (a : R) → MvPolynomial τ R) (coeff x φ)) n

Tactic:
apply IsHomogeneous.sum _ _ _ fun d hd ↦ isHomogeneous_monomial _ _

Premises used: MvPolynomial.isHomogeneous_monomial, MvPolynomial.IsHomogeneous.sum
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
f : σ → τ
h : φ.IsHomogeneous n
d : σ →₀ ℕ
hd : d ∈ φ.support
apply : (d.sum fun (a : σ) (m : ℕ) ↦ (AddMonoidHom.id ℕ : (a : ℕ) → ℕ) m) = n
⊢ (degree : (a : τ →₀ ℕ) → ℕ) (mapDomain f d) = n

Tactic:
apply (Finsupp.sum_mapDomain_index_addMonoidHom fun _ ↦ .id ℕ).trans

Premises used: AddMonoidHom.id, Nat, Finsupp.sum_mapDomain_index_addMonoidHom, Eq.trans
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
f : σ → τ
h : φ.IsHomogeneous n
d : σ →₀ ℕ
hd : d ∈ φ.support
⊢ (weight 1 : (a : σ →₀ ℕ) → ℕ) d = n

Tactic:
h (mem_support_iff.mp hd)

Premises used: MvPolynomial.mem_support_iff, Iff.mp
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
f : σ → τ
h : φ.IsHomogeneous n
d : σ →₀ ℕ
hd : d ∈ φ.support
h₁ :
  Eq (α := ℕ) (d.sum fun (a : σ) (m : ℕ) ↦ (AddMonoidHom.id ℕ : (a : ℕ) → ℕ) m : ℕ)
    ((weight 1 : (a : σ →₀ ℕ) → ℕ) d : ℕ)
⊢ (d.sum fun (a : σ) (m : ℕ) ↦ (AddMonoidHom.id ℕ : (a : ℕ) → ℕ) m) = n

Tactic:
convert! h (mem_support_iff.mp hd)

Premises used: MvPolynomial.mem_support_iff, Iff.mp
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
f : σ → τ
h : φ.IsHomogeneous n
d : σ →₀ ℕ
hd : d ∈ φ.support
⊢ Eq (α := ℕ) (d.sum fun (a : σ) (m : ℕ) ↦ (AddMonoidHom.id ℕ : (a : ℕ) → ℕ) m : ℕ)
    ((weight 1 : (a : σ →₀ ℕ) → ℕ) d : ℕ)

Tactic:
simp only [weight_apply, AddMonoidHom.id_apply, Pi.one_apply, smul_eq_mul, mul_one]

Premises used: AddMonoidHom.id_apply, Pi.one_apply, smul_eq_mul, mul_one, Finsupp.weight_apply
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
f : σ → τ
hf : Function.Injective f
⊢ IsHomogeneous.{u_2, u_3} (σ := τ) (R := R) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ) n ↔
    φ.IsHomogeneous n

Tactic:
⟨fun h d hd ↦ ?_, rename_isHomogeneous⟩

Premises used: Iff.intro, MvPolynomial.IsHomogeneous.rename_isHomogeneous
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
f : σ → τ
hf : Function.Injective f
refine :
  ∀ (h : IsHomogeneous.{u_2, u_3} (σ := τ) (R := R) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ) n)
    (d : σ →₀ ℕ) (hd : coeff d φ ≠ 0), (weight 1 : (a : σ →₀ ℕ) → ℕ) d = n
⊢ IsHomogeneous.{u_2, u_3} (σ := τ) (R := R) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ) n ↔
    φ.IsHomogeneous n

Tactic:
refine ⟨fun h d hd ↦ ?_, rename_isHomogeneous⟩
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
f : σ → τ
hf : Function.Injective f
h : IsHomogeneous.{u_2, u_3} (σ := τ) (R := R) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ) n
d : σ →₀ ℕ
hd : coeff d φ ≠ 0
⊢ (weight 1 : (a : τ →₀ ℕ) → ℕ) (mapDomain f d) = n

Tactic:
@h (d.mapDomain f) _
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
f : σ → τ
hf : Function.Injective f
h : IsHomogeneous.{u_2, u_3} (σ := τ) (R := R) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ) n
d : σ →₀ ℕ
hd : coeff d φ ≠ 0
h₁ : Eq (α := ℕ) ((weight 1 : (a : τ →₀ ℕ) → ℕ) (mapDomain f d) : ℕ) ((weight 1 : (a : σ →₀ ℕ) → ℕ) d : ℕ)
convert! : Ne.{u_3 + 1} (α := R) (coeff (mapDomain f d) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) 0
⊢ (weight 1 : (a : σ →₀ ℕ) → ℕ) d = n

Tactic:
convert! ← @h (d.mapDomain f) _
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
f : σ → τ
hf : Function.Injective f
h : IsHomogeneous.{u_2, u_3} (σ := τ) (R := R) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ) n
d : σ →₀ ℕ
hd : coeff d φ ≠ 0
h₁ : Eq (α := ℕ) ((mapDomain f d).sum fun (i : τ) (c : ℕ) ↦ c) (d.sum fun (i : σ) (c : ℕ) ↦ c)
⊢ Eq (α := ℕ) ((weight 1 : (a : τ →₀ ℕ) → ℕ) (mapDomain f d) : ℕ) ((weight 1 : (a : σ →₀ ℕ) → ℕ) d : ℕ)

Tactic:
simp only [weight_apply, Pi.one_apply, smul_eq_mul, mul_one]

Premises used: Pi.one_apply, smul_eq_mul, mul_one, Finsupp.weight_apply
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
f : σ → τ
hf : Function.Injective f
h : IsHomogeneous.{u_2, u_3} (σ := τ) (R := R) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ) n
d : σ →₀ ℕ
hd : coeff d φ ≠ 0
⊢ Eq (α := ℕ) ((mapDomain f d).sum fun (i : τ) (c : ℕ) ↦ c) (d.sum fun (i : σ) (c : ℕ) ↦ c)

Tactic:
Finsupp.sum_mapDomain_index_inj (h := fun _ ↦ id) hf

Premises used: Finsupp.sum_mapDomain_index_inj
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
f : σ → τ
hf : Function.Injective f
h : IsHomogeneous.{u_2, u_3} (σ := τ) (R := R) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ) n
d : σ →₀ ℕ
hd : coeff d φ ≠ 0
⊢ Eq (α := ℕ) ((mapDomain f d).sum fun (i : τ) (c : ℕ) ↦ c) (d.sum fun (i : σ) (c : ℕ) ↦ c)

Tactic:
exact Finsupp.sum_mapDomain_index_inj (h := fun _ ↦ id) hf

Premises used: Finsupp.sum_mapDomain_index_inj
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
f : σ → τ
hf : Function.Injective f
h : IsHomogeneous.{u_2, u_3} (σ := τ) (R := R) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ) n
d : σ →₀ ℕ
hd rwa rwa₁ rwa₂ rwa₃ : coeff d φ ≠ 0
⊢ Ne.{u_3 + 1} (α := R) (coeff (mapDomain f d) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) 0

Tactic:
rwa [coeff_rename_mapDomain f hf]

Premises used: MvPolynomial.coeff_rename_mapDomain
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
R : Type u_3
inst : CommSemiring R
N : ℕ
φ : MvPolynomial (Fin (N + 1)) R
n : ℕ
hφ : φ.IsHomogeneous n
i j : ℕ
h : i + j = n
d : Fin N →₀ ℕ
hd :
  Ne.{u_3 + 1} (α := R)
    (coeff d
      (Polynomial.coeff
        ((finSuccEquiv R N : (a : MvPolynomial (Fin (N + 1)) R) → Polynomial (MvPolynomial (Fin N) R)) φ) i))
    0
⊢ coeff (cons i d) φ ≠ 0

Tactic:
rw [finSuccEquiv_coeff_coeff] at hd

Premises used: MvPolynomial.finSuccEquiv_coeff_coeff
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
R : Type u_3
inst : CommSemiring R
N : ℕ
φ : MvPolynomial (Fin (N + 1)) R
n : ℕ
hφ : φ.IsHomogeneous n
i j : ℕ
h : i + j = n
d : Fin N →₀ ℕ
hd : coeff (cons i d) φ ≠ 0
⊢ ∀ x ∈ insert 0 (Finset.map (Fin.succEmb N) d.support) \ (cons i d).support,
    Eq (α := ℕ) ((cons i d : (a : Fin (N + 1)) → ℕ) x : ℕ) 0

Tactic:
simp
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
R : Type u_3
inst : CommSemiring R
N : ℕ
φ : MvPolynomial (Fin (N + 1)) R
n : ℕ
hφ : φ.IsHomogeneous n
i j : ℕ
h : i + j = n
d : Fin N →₀ ℕ
hd : coeff (cons i d) φ ≠ 0
⊢ (weight 1 : (a : Fin (N + 1) →₀ ℕ) → ℕ) (cons i d) = i + j

Tactic:
simpa [Finset.sum_subset_zero_on_sdiff (g := d.cons i)
     (d.cons_support (y := i)) (by simp) (fun _ _ ↦ rfl), ← h] using hφ hd

Premises used: Finsupp.cons_support, rfl, Finset.sum_subset_zero_on_sdiff
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
R : Type u_3
inst : CommSemiring R
N : ℕ
φ : MvPolynomial (Fin (N + 1)) R
n : ℕ
hφ : φ.IsHomogeneous n
i j : ℕ
h : i + j = n
d : Fin N →₀ ℕ
hd : coeff (cons i d) φ ≠ 0
⊢ (weight 1 : (a : Fin (N + 1) →₀ ℕ) → ℕ) (cons i d) = i + j

Tactic:
have h' : (weight 1) (Finsupp.cons i d) = i + j := by
    simpa [Finset.sum_subset_zero_on_sdiff (g := d.cons i)
     (d.cons_support (y := i)) (by simp) (fun _ _ ↦ rfl), ← h] using hφ hd
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
R : Type u_3
inst : CommSemiring R
N : ℕ
φ : MvPolynomial (Fin (N + 1)) R
n : ℕ
hφ : φ.IsHomogeneous n
i j : ℕ
h : i + j = n
d : Fin N →₀ ℕ
hd : coeff (cons i d) φ ≠ 0
h' : (weight 1 : (a : Fin (N + 1) →₀ ℕ) → ℕ) (cons i d) = i + j
simp : ∀ (h' : (d.sum fun (x : Fin N) (e : ℕ) ↦ e) = j), (d.sum fun (i : Fin N) (c : ℕ) ↦ c) = j
⊢ (weight 1 : (a : Fin N →₀ ℕ) → ℕ) d = j

Tactic:
simp only [weight_apply, Pi.one_apply, smul_eq_mul, mul_one, Finsupp.sum_cons,
    add_right_inj] at h' ⊢

Premises used: Pi.one_apply, Finsupp.sum_cons, smul_eq_mul, mul_one, add_right_inj, Finsupp.weight_apply
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
R : Type u_3
inst : CommSemiring R
N : ℕ
φ : MvPolynomial (Fin (N + 1)) R
n : ℕ
hφ : φ.IsHomogeneous n
i j : ℕ
h : i + j = n
d : Fin N →₀ ℕ
hd : coeff (cons i d) φ ≠ 0
h' : (d.sum fun (x : Fin N) (e : ℕ) ↦ e) = j
⊢ (d.sum fun (i : Fin N) (c : ℕ) ↦ c) = j

Tactic:
h'
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
R : Type u_3
inst : CommSemiring R
N : ℕ
φ : MvPolynomial (Fin (N + 1)) R
n : ℕ
hφ : φ.IsHomogeneous n
i j : ℕ
h : i + j = n
d : Fin N →₀ ℕ
hd : coeff (cons i d) φ ≠ 0
h' : (d.sum fun (x : Fin N) (e : ℕ) ↦ e) = j
⊢ (d.sum fun (i : Fin N) (c : ℕ) ↦ c) = j

Tactic:
exact h'
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
n : ℕ
hσ : Finite σ
p : Polynomial (MvPolynomial σ R)
hp :
  IsHomogeneous.{u_1, u_3} (σ := Option σ) (R := R)
    ((AlgEquiv.symm (optionEquivLeft R σ) : (a : Polynomial (MvPolynomial σ R)) → MvPolynomial (Option σ) R) p) n
i j : ℕ
h : i + j = n
obtain : ∀ (k : ℕ) (e : σ ≃ Fin k), (p.coeff i).IsHomogeneous j
⊢ (p.coeff i).IsHomogeneous j

Tactic:
obtain ⟨k, ⟨e⟩⟩ := Finite.exists_equiv_fin σ

Premises used: Finite.exists_equiv_fin
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
n : ℕ
hσ : Finite σ
p : Polynomial (MvPolynomial σ R)
hp :
  IsHomogeneous.{u_1, u_3} (σ := Option σ) (R := R)
    ((AlgEquiv.symm (optionEquivLeft R σ) : (a : Polynomial (MvPolynomial σ R)) → MvPolynomial (Option σ) R) p) n
i j : ℕ
h : i + j = n
k : ℕ
e : σ ≃ Fin k
e' : Option σ ≃ Fin (k + 1) := e.optionCongr.trans (_root_.finSuccEquiv k).symm
F : MvPolynomial σ R ≃ₐ[R] MvPolynomial (Fin k) R := renameEquiv R e
F' : MvPolynomial.{u_1, u_3} (Option σ) R ≃ₐ[R] MvPolynomial (Fin (k + 1)) R := renameEquiv R e'
φ : MvPolynomial (Fin (k + 1)) R :=
  (F' : (a : MvPolynomial (Option σ) R) → MvPolynomial (Fin (k + 1)) R)
    ((AlgEquiv.symm (optionEquivLeft R σ) : (a : Polynomial (MvPolynomial σ R)) → MvPolynomial (Option σ) R) p)
⊢ φ.IsHomogeneous n

Tactic:
have hφ : φ.IsHomogeneous n := hp.rename_isHomogeneous
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
n : ℕ
hσ : Finite σ
p : Polynomial (MvPolynomial σ R)
hp :
  IsHomogeneous.{u_1, u_3} (σ := Option σ) (R := R)
    ((AlgEquiv.symm (optionEquivLeft R σ) : (a : Polynomial (MvPolynomial σ R)) → MvPolynomial (Option σ) R) p) n
i j : ℕ
h : i + j = n
k : ℕ
e : σ ≃ Fin k
e' : Option σ ≃ Fin (k + 1) := e.optionCongr.trans (_root_.finSuccEquiv k).symm
F : MvPolynomial σ R ≃ₐ[R] MvPolynomial (Fin k) R := renameEquiv R e
F' : MvPolynomial.{u_1, u_3} (Option σ) R ≃ₐ[R] MvPolynomial (Fin (k + 1)) R := renameEquiv R e'
φ : MvPolynomial (Fin (k + 1)) R :=
  (F' : (a : MvPolynomial (Option σ) R) → MvPolynomial (Fin (k + 1)) R)
    ((AlgEquiv.symm (optionEquivLeft R σ) : (a : Polynomial (MvPolynomial σ R)) → MvPolynomial (Option σ) R) p)
hφ : φ.IsHomogeneous n
this :
  IsHomogeneous.{0, u_3} (σ := Fin k) (R := R) ((F : (a : MvPolynomial σ R) → MvPolynomial (Fin k) R) (p.coeff i)) j
rwa rwa₁ rwa₂ rwa₃ :
  IsHomogeneous.{0, u_3} (σ := Fin k) (R := R)
    ((rename (⇑e : (a : σ) → Fin k) : (a : MvPolynomial σ R) → MvPolynomial (Fin k) R) (p.coeff i)) j
⊢ (p.coeff i).IsHomogeneous j

Tactic:
rwa [← (IsHomogeneous.rename_isHomogeneous_iff e.injective)]

Premises used: MvPolynomial.IsHomogeneous.rename_isHomogeneous_iff, Equiv.injective
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
n : ℕ
hσ : Finite σ
p : Polynomial (MvPolynomial σ R)
hp :
  IsHomogeneous.{u_1, u_3} (σ := Option σ) (R := R)
    ((AlgEquiv.symm (optionEquivLeft R σ) : (a : Polynomial (MvPolynomial σ R)) → MvPolynomial (Option σ) R) p) n
i j : ℕ
h : i + j = n
k : ℕ
e : σ ≃ Fin k
e' : Option σ ≃ Fin (k + 1) := e.optionCongr.trans (_root_.finSuccEquiv k).symm
F : MvPolynomial σ R ≃ₐ[R] MvPolynomial (Fin k) R := renameEquiv R e
F' : MvPolynomial.{u_1, u_3} (Option σ) R ≃ₐ[R] MvPolynomial (Fin (k + 1)) R := renameEquiv R e'
φ : MvPolynomial (Fin (k + 1)) R :=
  (F' : (a : MvPolynomial (Option σ) R) → MvPolynomial (Fin (k + 1)) R)
    ((AlgEquiv.symm (optionEquivLeft R σ) : (a : Polynomial (MvPolynomial σ R)) → MvPolynomial (Option σ) R) p)
hφ : φ.IsHomogeneous n
suffices :
  IsHomogeneous.{0, u_3} (σ := Fin k) (R := R) ((F : (a : MvPolynomial σ R) → MvPolynomial (Fin k) R) (p.coeff i)) j
⊢ (p.coeff i).IsHomogeneous j

Tactic:
suffices IsHomogeneous (F (p.coeff i)) j by
    rwa [← (IsHomogeneous.rename_isHomogeneous_iff e.injective)]
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
n : ℕ
hσ : Finite σ
p : Polynomial (MvPolynomial σ R)
hp :
  IsHomogeneous.{u_1, u_3} (σ := Option σ) (R := R)
    ((AlgEquiv.symm (optionEquivLeft R σ) : (a : Polynomial (MvPolynomial σ R)) → MvPolynomial (Option σ) R) p) n
i j : ℕ
h : i + j = n
k : ℕ
e : σ ≃ Fin k
e' : Option σ ≃ Fin (k + 1) := e.optionCongr.trans (_root_.finSuccEquiv k).symm
F : MvPolynomial σ R ≃ₐ[R] MvPolynomial (Fin k) R := renameEquiv R e
F' : MvPolynomial.{u_1, u_3} (Option σ) R ≃ₐ[R] MvPolynomial (Fin (k + 1)) R := renameEquiv R e'
φ : MvPolynomial (Fin (k + 1)) R :=
  (F' : (a : MvPolynomial (Option σ) R) → MvPolynomial (Fin (k + 1)) R)
    ((AlgEquiv.symm (optionEquivLeft R σ) : (a : Polynomial (MvPolynomial σ R)) → MvPolynomial (Option σ) R) p)
hφ : φ.IsHomogeneous n
⊢ IsHomogeneous.{0, u_3} (σ := Fin k) (R := R)
    (Polynomial.coeff ((finSuccEquiv R k : (a : MvPolynomial (Fin (k + 1)) R) → Polynomial (MvPolynomial (Fin k) R)) φ)
      i)
    j

Tactic:
hφ.finSuccEquiv_coeff_isHomogeneous i j h

Premises used: MvPolynomial.IsHomogeneous.finSuccEquiv_coeff_isHomogeneous
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
n : ℕ
hσ : Finite σ
p : Polynomial (MvPolynomial σ R)
hp :
  IsHomogeneous.{u_1, u_3} (σ := Option σ) (R := R)
    ((AlgEquiv.symm (optionEquivLeft R σ) : (a : Polynomial (MvPolynomial σ R)) → MvPolynomial (Option σ) R) p) n
i j : ℕ
h : i + j = n
k : ℕ
e : σ ≃ Fin k
e' : Option σ ≃ Fin (k + 1) := e.optionCongr.trans (_root_.finSuccEquiv k).symm
F : MvPolynomial σ R ≃ₐ[R] MvPolynomial (Fin k) R := renameEquiv R e
F' : MvPolynomial.{u_1, u_3} (Option σ) R ≃ₐ[R] MvPolynomial (Fin (k + 1)) R := renameEquiv R e'
φ : MvPolynomial (Fin (k + 1)) R :=
  (F' : (a : MvPolynomial (Option σ) R) → MvPolynomial (Fin (k + 1)) R)
    ((AlgEquiv.symm (optionEquivLeft R σ) : (a : Polynomial (MvPolynomial σ R)) → MvPolynomial (Option σ) R) p)
hφ : φ.IsHomogeneous n
h₁ :
  Eq.{u_3 + 1} (α := MvPolynomial (Fin k) R)
    ((F : (a : MvPolynomial σ R) → MvPolynomial (Fin k) R) (p.coeff i) : MvPolynomial (Fin k) R)
    (Polynomial.coeff ((finSuccEquiv R k : (a : MvPolynomial (Fin (k + 1)) R) → Polynomial (MvPolynomial (Fin k) R)) φ)
        i :
      MvPolynomial (Fin k) R)
⊢ IsHomogeneous.{0, u_3} (σ := Fin k) (R := R) ((F : (a : MvPolynomial σ R) → MvPolynomial (Fin k) R) (p.coeff i)) j

Tactic:
convert! hφ.finSuccEquiv_coeff_isHomogeneous i j h using 1

Premises used: MvPolynomial.IsHomogeneous.finSuccEquiv_coeff_isHomogeneous