awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
f : R →+* S
g : Fin 2 → S
hg : g 1 = 1
⊢ ∀ (n_1 : ℕ) (r : R),
    r ≠ 0 →
      n_1 ≤ n →
        MvPolynomial.eval₂ f g
            ((HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n_1)).homogenize n) =
          eval₂ f (g 0) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n_1))

Tactic:
simp +contextual [hg]
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
f : R →+* S
g : Fin 2 → S
hg : g 1 = 1
⊢ ∀ (f_1 g_1 : R[X]),
    f_1.natDegree < g_1.natDegree →
      g_1.natDegree ≤ n →
        MvPolynomial.eval₂ f g (f_1.homogenize n) = eval₂ f (g 0) f_1 →
          MvPolynomial.eval₂ f g (g_1.homogenize n) = eval₂ f (g 0) g_1 →
            MvPolynomial.eval₂ f g ((f_1 + g_1).homogenize n) = eval₂ f (g 0) (f_1 + g_1)

Tactic:
simp +contextual
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
f : R →+* S
g : Fin 2 → S
hg : g 1 = 1
⊢ p.natDegree ≤ n

Tactic:
assumption
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
g : Fin 2 → A
hg : g 1 = 1
hn₁ : p.natDegree ≤ n
hg₁ : g 1 = 1
⊢ Eq.{u_2 + 1} (α := A) ((MvPolynomial.aeval g : (a : MvPolynomial (Fin 2) R) → A) (p.homogenize n) : A)
    ((aeval (g 0) : (a : R[X]) → A) p : A)

Tactic:
apply eval₂_homogenize_of_eq_one

Premises used: Polynomial.eval₂_homogenize_of_eq_one
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
g : Fin 2 → A
hg : g 1 = 1
⊢ p.natDegree ≤ n

Tactic:
assumption
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
g : Fin 2 → A
hg : g 1 = 1
⊢ g 1 = 1

Tactic:
assumption
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
rw : (aeval (![X, 1] 0) : (a : R[X]) → R[X]) p = p
hn₁ : p.natDegree ≤ n
hg : Eq.{u_1 + 1} (α := R[X]) (![X, 1] 1) 1
⊢ (MvPolynomial.aeval ![X, 1] : (a : MvPolynomial (Fin (Nat.succ 0).succ) R) → R[X]) (p.homogenize n) = p

Tactic:
rw [aeval_homogenize_of_eq_one]

Premises used: Polynomial.aeval_homogenize_of_eq_one
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
⊢ (aeval (![X, 1] 0) : (a : R[X]) → R[X]) p = p

Tactic:
simp [*]
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
⊢ p.natDegree ≤ n

Tactic:
simp [*]
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
⊢ Eq.{u_1 + 1} (α := R[X]) (![X, 1] 1) 1

Tactic:
simp [*]
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
R : Type u_1
inst : CommSemiring R
n : ℕ
p : R[X]
⊢ (p.homogenize n).IsHomogeneous n

Tactic:
MvPolynomial.IsHomogeneous.sum _ _ _ ?_

Premises used: Polynomial.homogenize, MvPolynomial.IsHomogeneous.sum
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
R : Type u_1
inst : CommSemiring R
n : ℕ
p : R[X]
refine :
  ∀ i ∈ @antidiagonal _ Nat.instAddMonoid _ n,
    MvPolynomial.IsHomogeneous.{0, u_1} (σ := Fin 2) (R := R)
      ((MvPolynomial.monomial fun₀ | 0 => i.1 | 1 => i.2 : (a : R) → MvPolynomial (Fin 2) R) (p.coeff i.1)) n
⊢ (p.homogenize n).IsHomogeneous n

Tactic:
refine MvPolynomial.IsHomogeneous.sum _ _ _ ?_

Premises used: MvPolynomial.IsHomogeneous.sum
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
R : Type u_1
inst : CommSemiring R
n : ℕ
p : R[X]
simp :
  ∀ (a b : ℕ),
    a + b = n →
      MvPolynomial.IsHomogeneous.{0, u_1} (σ := Fin 2) (R := R)
        ((MvPolynomial.monomial fun₀ | 0 => a | 1 => b : (a : R) → MvPolynomial (Fin 2) R) (p.coeff a)) n
⊢ ∀ i ∈ @antidiagonal _ Nat.instAddMonoid _ n,
    MvPolynomial.IsHomogeneous.{0, u_1} (σ := Fin 2) (R := R)
      ((MvPolynomial.monomial fun₀ | 0 => i.1 | 1 => i.2 : (a : R) → MvPolynomial (Fin 2) R) (p.coeff i.1)) n

Tactic:
simp only [Prod.forall, mem_antidiagonal]

Premises used: Finset.HasAntidiagonal.mem_antidiagonal, Prod.forall
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
a b : ℕ
hn : ((Finsupp.degree : (a : Fin 2 →₀ ℕ) → ℕ) fun₀ | 0 => a | 1 => b) = a + b
⊢ MvPolynomial.IsHomogeneous.{0, u_1} (σ := Fin 2) (R := R)
    ((MvPolynomial.monomial fun₀ | 0 => a | 1 => b : (a : R) → MvPolynomial (Fin 2) R) (p.coeff a)) (a + b)

Tactic:
apply MvPolynomial.isHomogeneous_monomial

Premises used: MvPolynomial.isHomogeneous_monomial
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
a b : ℕ
⊢ ((Finsupp.degree : (a : Fin 2 →₀ ℕ) → ℕ) fun₀ | 0 => a | 1 => b) = a + b

Tactic:
simp [Finsupp.update_eq_add_single]

Premises used: Finsupp.update_eq_add_single
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
n : ℕ
q : MvPolynomial (Fin 2) R
hq : q.IsHomogeneous n
hpq : (MvPolynomial.aeval ![X, 1] : (a : MvPolynomial (Fin (Nat.succ 0).succ) R) → R[X]) q = p
subst : homogenize ((MvPolynomial.aeval ![X, 1] : (a : MvPolynomial (Fin (Nat.succ 0).succ) R) → R[X]) q) n = q
⊢ p.homogenize n = q

Tactic:
subst p
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
R : Type u_1
inst : CommSemiring R
n : ℕ
q : MvPolynomial (Fin 2) R
hq : q.IsHomogeneous n
rw :
  Eq.{u_1 + 1} (α := MvPolynomial (Fin 2) R)
    (homogenize
      ((MvPolynomial.aeval ![X, 1] : (a : MvPolynomial (Fin (Nat.succ 0).succ) R) → R[X])
        (∑ v ∈ q.support, (MvPolynomial.monomial v : (a : R) → MvPolynomial (Fin 2) R) (MvPolynomial.coeff v q)))
      n)
    (∑ v ∈ q.support, (MvPolynomial.monomial v : (a : R) → MvPolynomial (Fin 2) R) (MvPolynomial.coeff v q))
⊢ homogenize ((MvPolynomial.aeval ![X, 1] : (a : MvPolynomial (Fin (Nat.succ 0).succ) R) → R[X]) q) n = q

Tactic:
rw [q.as_sum]

Premises used: MvPolynomial.as_sum
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
R : Type u_1
inst : CommSemiring R
n : ℕ
q : MvPolynomial (Fin 2) R
hq : q.IsHomogeneous n
simp :
  Eq.{u_1 + 1} (α := MvPolynomial (Fin 2) R)
    (∑ x ∈ q.support,
      HMul.hMul (α := MvPolynomial (Fin 2) R) (β := MvPolynomial (Fin 2) R)
        ((MvPolynomial.C : (a : R) → MvPolynomial (Fin 2) R) (MvPolynomial.coeff x q) : MvPolynomial (Fin 2) R)
        (homogenize (x.prod fun (i : Fin (Nat.succ 0).succ) (k : ℕ) ↦ HPow.hPow (α := R[X]) (![X, 1] i) k) n))
    (∑ v ∈ q.support, (MvPolynomial.monomial v : (a : R) → MvPolynomial (Fin 2) R) (MvPolynomial.coeff v q))
⊢ Eq.{u_1 + 1} (α := MvPolynomial (Fin 2) R)
    (homogenize
      ((MvPolynomial.aeval ![X, 1] : (a : MvPolynomial (Fin (Nat.succ 0).succ) R) → R[X])
        (∑ v ∈ q.support, (MvPolynomial.monomial v : (a : R) → MvPolynomial (Fin 2) R) (MvPolynomial.coeff v q)))
      n)
    (∑ v ∈ q.support, (MvPolynomial.monomial v : (a : R) → MvPolynomial (Fin 2) R) (MvPolynomial.coeff v q))

Tactic:
simp only [MvPolynomial.aeval_sum, MvPolynomial.aeval_monomial, ← C_eq_algebraMap,
    homogenize_finsetSum, homogenize_C_mul]

Premises used: MvPolynomial.aeval_sum, Polynomial.C_eq_algebraMap, Polynomial.homogenize_finsetSum, Polynomial.homogenize_C_mul, MvPolynomial.aeval_monomial
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
R : Type u_1
inst : CommSemiring R
n : ℕ
q : MvPolynomial (Fin 2) R
hq : q.IsHomogeneous n
⊢ Eq.{u_1 + 1} (α := MvPolynomial (Fin 2) R)
    (∑ x ∈ q.support,
      HMul.hMul (α := MvPolynomial (Fin 2) R) (β := MvPolynomial (Fin 2) R)
        ((MvPolynomial.C : (a : R) → MvPolynomial (Fin 2) R) (MvPolynomial.coeff x q) : MvPolynomial (Fin 2) R)
        (homogenize (x.prod fun (i : Fin (Nat.succ 0).succ) (k : ℕ) ↦ HPow.hPow (α := R[X]) (![X, 1] i) k) n))
    (∑ v ∈ q.support, (MvPolynomial.monomial v : (a : R) → MvPolynomial (Fin 2) R) (MvPolynomial.coeff v q))

Tactic:
Finset.sum_congr rfl fun m hm ↦ ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
R : Type u_1
inst : CommSemiring R
n : ℕ
q : MvPolynomial (Fin 2) R
hq : q.IsHomogeneous n
refine :
  ∀ (m : Fin 2 →₀ ℕ) (hm : m ∈ q.support),
    HMul.hMul (α := MvPolynomial (Fin 2) R) (β := MvPolynomial (Fin 2) R)
        ((MvPolynomial.C : (a : R) → MvPolynomial (Fin 2) R) (MvPolynomial.coeff m q) : MvPolynomial (Fin 2) R)
        (homogenize (m.prod fun (i : Fin (Nat.succ 0).succ) (k : ℕ) ↦ HPow.hPow (α := R[X]) (![X, 1] i) k) n) =
      (MvPolynomial.monomial m : (a : R) → MvPolynomial (Fin 2) R) (MvPolynomial.coeff m q)
⊢ Eq.{u_1 + 1} (α := MvPolynomial (Fin 2) R)
    (∑ x ∈ q.support,
      HMul.hMul (α := MvPolynomial (Fin 2) R) (β := MvPolynomial (Fin 2) R)
        ((MvPolynomial.C : (a : R) → MvPolynomial (Fin 2) R) (MvPolynomial.coeff x q) : MvPolynomial (Fin 2) R)
        (homogenize (x.prod fun (i : Fin (Nat.succ 0).succ) (k : ℕ) ↦ HPow.hPow (α := R[X]) (![X, 1] i) k) n))
    (∑ v ∈ q.support, (MvPolynomial.monomial v : (a : R) → MvPolynomial (Fin 2) R) (MvPolynomial.coeff v q))

Tactic:
refine Finset.sum_congr rfl fun m hm ↦ ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
R : Type u_1
inst : CommSemiring R
n : ℕ
q : MvPolynomial (Fin 2) R
hq : q.IsHomogeneous n
m : Fin 2 →₀ ℕ
hm : m ∈ q.support
rw :
  HMul.hMul (α := MvPolynomial (Fin 2) R) (β := MvPolynomial (Fin 2) R)
      ((MvPolynomial.C : (a : R) → MvPolynomial (Fin 2) R) (MvPolynomial.coeff m q) : MvPolynomial (Fin 2) R)
      (homogenize (m.prod fun (i : Fin (Nat.succ 0).succ) (k : ℕ) ↦ HPow.hPow (α := R[X]) (![X, 1] i) k) n) =
    HMul.hMul (α := MvPolynomial (Fin 2) R) (β := MvPolynomial (Fin 2) R)
      ((MvPolynomial.C : (a : R) → MvPolynomial (Fin 2) R) (MvPolynomial.coeff m q) : MvPolynomial (Fin 2) R)
      (m.prod fun (n : Fin 2) (e : ℕ) ↦ HPow.hPow (α := MvPolynomial (Fin 2) R) (MvPolynomial.X n) e :
        MvPolynomial (Fin 2) R)
⊢ HMul.hMul (α := MvPolynomial (Fin 2) R) (β := MvPolynomial (Fin 2) R)
      ((MvPolynomial.C : (a : R) → MvPolynomial (Fin 2) R) (MvPolynomial.coeff m q) : MvPolynomial (Fin 2) R)
      (homogenize (m.prod fun (i : Fin (Nat.succ 0).succ) (k : ℕ) ↦ HPow.hPow (α := R[X]) (![X, 1] i) k) n) =
    (MvPolynomial.monomial m : (a : R) → MvPolynomial (Fin 2) R) (MvPolynomial.coeff m q)

Tactic:
rw [MvPolynomial.monomial_eq]

Premises used: MvPolynomial.monomial_eq
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
R : Type u_1
inst : CommSemiring R
n : ℕ
q : MvPolynomial (Fin 2) R
hq : q.IsHomogeneous n
m : Fin 2 →₀ ℕ
hm : m ∈ q.support
e_a :
  Eq.{u_1 + 1} (α := MvPolynomial (Fin 2) R)
    (homogenize (m.prod fun (i : Fin (Nat.succ 0).succ) (k : ℕ) ↦ HPow.hPow (α := R[X]) (![X, 1] i) k) n)
    (m.prod fun (n : Fin 2) (e : ℕ) ↦ HPow.hPow (α := MvPolynomial (Fin 2) R) (MvPolynomial.X n) e)
⊢ HMul.hMul (α := MvPolynomial (Fin 2) R) (β := MvPolynomial (Fin 2) R)
      ((MvPolynomial.C : (a : R) → MvPolynomial (Fin 2) R) (MvPolynomial.coeff m q) : MvPolynomial (Fin 2) R)
      (homogenize (m.prod fun (i : Fin (Nat.succ 0).succ) (k : ℕ) ↦ HPow.hPow (α := R[X]) (![X, 1] i) k) n) =
    HMul.hMul (α := MvPolynomial (Fin 2) R) (β := MvPolynomial (Fin 2) R)
      ((MvPolynomial.C : (a : R) → MvPolynomial (Fin 2) R) (MvPolynomial.coeff m q) : MvPolynomial (Fin 2) R)
      (m.prod fun (n : Fin 2) (e : ℕ) ↦ HPow.hPow (α := MvPolynomial (Fin 2) R) (MvPolynomial.X n) e :
        MvPolynomial (Fin 2) R)

Tactic:
congr 1
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
R : Type u_1
inst : CommSemiring R
n : ℕ
q : MvPolynomial (Fin 2) R
hq : q.IsHomogeneous n
m : Fin 2 →₀ ℕ
hm : m ∈ q.support
⊢ MvPolynomial.coeff m q ≠ 0

Tactic:
simpa using hm
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
R : Type u_1
inst : CommSemiring R
n : ℕ
q : MvPolynomial (Fin 2) R
hq : q.IsHomogeneous n
m : Fin 2 →₀ ℕ
hm : m ∈ q.support
e_a :
  ∀ (hq : q.IsHomogeneous ((Finsupp.weight 1 : (a : Fin 2 →₀ ℕ) → ℕ) m)),
    Eq.{u_1 + 1} (α := MvPolynomial (Fin 2) R)
      (homogenize (m.prod fun (i : Fin (Nat.succ 0).succ) (k : ℕ) ↦ HPow.hPow (α := R[X]) (![X, 1] i) k)
        ((Finsupp.weight 1 : (a : Fin 2 →₀ ℕ) → ℕ) m))
      (m.prod fun (n : Fin 2) (e : ℕ) ↦ HPow.hPow (α := MvPolynomial (Fin 2) R) (MvPolynomial.X n) e)
⊢ Eq.{u_1 + 1} (α := MvPolynomial (Fin 2) R)
    (homogenize (m.prod fun (i : Fin (Nat.succ 0).succ) (k : ℕ) ↦ HPow.hPow (α := R[X]) (![X, 1] i) k) n)
    (m.prod fun (n : Fin 2) (e : ℕ) ↦ HPow.hPow (α := MvPolynomial (Fin 2) R) (MvPolynomial.X n) e)

Tactic:
obtain rfl : m.weight 1 = n := hq <| by simpa using hm

Premises used: Finsupp.weight, OfNat.ofNat, DFunLike.coe, rfl
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
R : Type u_1
inst : CommSemiring R
q : MvPolynomial (Fin 2) R
m : Fin 2 →₀ ℕ
hm : m ∈ q.support
hq : q.IsHomogeneous ((Finsupp.weight 1 : (a : Fin 2 →₀ ℕ) → ℕ) m)
⊢ Eq.{u_1 + 1} (α := MvPolynomial (Fin 2) R)
    (homogenize (m.prod fun (i : Fin (Nat.succ 0).succ) (k : ℕ) ↦ HPow.hPow (α := R[X]) (![X, 1] i) k)
      ((Finsupp.weight 1 : (a : Fin 2 →₀ ℕ) → ℕ) m))
    (m.prod fun (n : Fin 2) (e : ℕ) ↦ HPow.hPow (α := MvPolynomial (Fin 2) R) (MvPolynomial.X n) e)

Tactic:
simp [Finsupp.prod_fintype, Finsupp.weight_apply, Finsupp.sum_fintype, Fin.prod_univ_two,
    Fin.sum_univ_two]

Premises used: Finsupp.sum_fintype, Fin.prod_univ_two, Finsupp.prod_fintype, Fin.sum_univ_two, Finsupp.weight_apply
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
R : Type u_1
inst : CommSemiring R
p q : R[X]
m n : ℕ
hm : p.natDegree ≤ m
hn : q.natDegree ≤ n
hq : (p.homogenize m * q.homogenize n).IsHomogeneous (m + n)
hpq :
  (MvPolynomial.aeval ![X, 1] : (a : MvPolynomial (Fin (Nat.succ 0).succ) R) → R[X]) (p.homogenize m * q.homogenize n) =
    p * q
⊢ (p * q).homogenize (m + n) = p.homogenize m * q.homogenize n

Tactic:
apply homogenize_eq_of_isHomogeneous

Premises used: Polynomial.homogenize_eq_of_isHomogeneous
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
R : Type u_1
inst : CommSemiring R
p q : R[X]
m n : ℕ
hm : p.natDegree ≤ m
hn : q.natDegree ≤ n
⊢ (p.homogenize m * q.homogenize n).IsHomogeneous (m + n)

Tactic:
apply_rules [MvPolynomial.IsHomogeneous.mul, isHomogeneous_homogenize]

Premises used: Polynomial.isHomogeneous_homogenize, MvPolynomial.IsHomogeneous.mul
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
R : Type u_1
inst : CommSemiring R
p q : R[X]
m n : ℕ
hm : p.natDegree ≤ m
hn : q.natDegree ≤ n
⊢ (MvPolynomial.aeval ![X, 1] : (a : MvPolynomial (Fin (Nat.succ 0).succ) R) → R[X]) (p.homogenize m * q.homogenize n) =
    p * q

Tactic:
simp [*]
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
R : Type u_1
inst : CommSemiring R
ι : Type u_2
p : ι → R[X]
n : ι → ℕ
h : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → (p i).natDegree ≤ n i
⊢ Eq.{u_1 + 1} (α := MvPolynomial (Fin 2) R) (homogenize (∏ i ∈ ∅, p i) (∑ i ∈ ∅, n i))
    (∏ i ∈ ∅, (p i).homogenize (n i))

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
R : Type u_1
inst : CommSemiring R
ι : Type u_2
p : ι → R[X]
n : ι → ℕ
i : ι
s : Finset ι
hi : i ∉ s
ihs :
  ∀ (h : ∀ i ∈ s, (p i).natDegree ≤ n i),
    Eq.{u_1 + 1} (α := MvPolynomial (Fin 2) R) (homogenize (∏ i ∈ s, p i) (∑ i ∈ s, n i))
      (∏ i ∈ s, (p i).homogenize (n i))
h : ∀ i_1 ∈ Finset.cons i s hi, (p i_1).natDegree ≤ n i_1
cons :
  ∀ (h : (p i).natDegree ≤ n i ∧ ∀ x ∈ s, (p x).natDegree ≤ n x),
    (p i * ∏ i ∈ s, p i).homogenize (n i + ∑ i ∈ s, n i) = (p i).homogenize (n i) * ∏ i ∈ s, (p i).homogenize (n i)
⊢ Eq.{u_1 + 1} (α := MvPolynomial (Fin 2) R)
    (homogenize (∏ i ∈ Finset.cons i s hi, p i) (∑ i ∈ Finset.cons i s hi, n i))
    (∏ i ∈ Finset.cons i s hi, (p i).homogenize (n i))

Tactic:
simp only [prod_cons, sum_cons, forall_mem_cons] at *

Premises used: Finset.sum_cons, Finset.forall_mem_cons, Finset.prod_cons
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
R : Type u_1
inst : CommSemiring R
ι : Type u_2
p : ι → R[X]
n : ι → ℕ
i : ι
s : Finset ι
hi : i ∉ s
ihs :
  ∀ (h : ∀ i ∈ s, (p i).natDegree ≤ n i),
    Eq.{u_1 + 1} (α := MvPolynomial (Fin 2) R) (homogenize (∏ i ∈ s, p i) (∑ i ∈ s, n i))
      (∏ i ∈ s, (p i).homogenize (n i))
h : (p i).natDegree ≤ n i ∧ ∀ x ∈ s, (p x).natDegree ≤ n x
cons : natDegree.{u_1} (R := R) (∏ i ∈ s, p i) ≤ ∑ i ∈ s, n i
⊢ (p i * ∏ i ∈ s, p i).homogenize (n i + ∑ i ∈ s, n i) = (p i).homogenize (n i) * ∏ i ∈ s, (p i).homogenize (n i)

Tactic:
rw [homogenize_mul _ _ h.1, ihs h.2]

Premises used: And.right, And.left, Polynomial.homogenize_mul
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
R : Type u_1
inst : CommSemiring R
ι : Type u_2
p : ι → R[X]
n : ι → ℕ
i : ι
s : Finset ι
hi : i ∉ s
ihs :
  ∀ (h : ∀ i ∈ s, (p i).natDegree ≤ n i),
    Eq.{u_1 + 1} (α := MvPolynomial (Fin 2) R) (homogenize (∏ i ∈ s, p i) (∑ i ∈ s, n i))
      (∏ i ∈ s, (p i).homogenize (n i))
h : (p i).natDegree ≤ n i ∧ ∀ x ∈ s, (p x).natDegree ≤ n x
⊢ natDegree.{u_1} (R := R) (∏ i ∈ s, p i) ≤ ∑ i ∈ s, n i

Tactic:
(natDegree_prod_le _ _).trans (sum_le_sum h.2)

Premises used: Polynomial.natDegree_prod_le, And.right, Finset.sum_le_sum, LE.le.trans
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
R : Type u_1
inst : CommSemiring R
ι : Type u_2
p : ι → R[X]
n : ι → ℕ
i : ι
s : Finset ι
hi : i ∉ s
ihs :
  ∀ (h : ∀ i ∈ s, (p i).natDegree ≤ n i),
    Eq.{u_1 + 1} (α := MvPolynomial (Fin 2) R) (homogenize (∏ i ∈ s, p i) (∑ i ∈ s, n i))
      (∏ i ∈ s, (p i).homogenize (n i))
h : (p i).natDegree ≤ n i ∧ ∀ x ∈ s, (p x).natDegree ≤ n x
⊢ natDegree.{u_1} (R := R) (∏ i ∈ s, p i) ≤ ∑ i ∈ s, n i

Tactic:
exact (natDegree_prod_le _ _).trans (sum_le_sum h.2)

Premises used: Polynomial.natDegree_prod_le, And.right, Finset.sum_le_sum, LE.le.trans
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
R : Type u_1
inst : CommSemiring R
ι : Type u_2
s : Finset ι
p : ι → R[X]
n : ι → ℕ
h : ∀ i ∈ s, (p i).natDegree ≤ n i
empty :
  ∀ (h : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → (p i).natDegree ≤ n i),
    Eq.{u_1 + 1} (α := MvPolynomial (Fin 2) R) (homogenize (∏ i ∈ ∅, p i) (∑ i ∈ ∅, n i))
      (∏ i ∈ ∅, (p i).homogenize (n i))
cons :
  ∀ (i : ι) (s : Finset ι) (hi : i ∉ s)
    (ihs :
      ∀ (h : ∀ i ∈ s, (p i).natDegree ≤ n i),
        Eq.{u_1 + 1} (α := MvPolynomial (Fin 2) R) (homogenize (∏ i ∈ s, p i) (∑ i ∈ s, n i))
          (∏ i ∈ s, (p i).homogenize (n i)))
    (h : ∀ i_1 ∈ Finset.cons i s hi, (p i_1).natDegree ≤ n i_1),
    Eq.{u_1 + 1} (α := MvPolynomial (Fin 2) R)
      (homogenize (∏ i ∈ Finset.cons i s hi, p i) (∑ i ∈ Finset.cons i s hi, n i))
      (∏ i ∈ Finset.cons i s hi, (p i).homogenize (n i))
⊢ Eq.{u_1 + 1} (α := MvPolynomial (Fin 2) R) (homogenize (∏ i ∈ s, p i) (∑ i ∈ s, n i))
    (∏ i ∈ s, (p i).homogenize (n i))

Tactic:
induction s using Finset.cons_induction with
  | empty => simp
  | cons i s hi ihs =>
    simp only [prod_cons, sum_cons, forall_mem_cons] at *
    rw [homogenize_mul _ _ h.1, ihs h.2]
    exact (natDegree_prod_le _ _).trans (sum_le_sum h.2)

Premises used: Finset.sum_cons, Finset.cons, Finset.forall_mem_cons, Finset.prod_cons
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : NoZeroDivisors R
p q : R[X]
h : p ∣ q
rcases : ∀ (r : R[X]), p.homogenize p.natDegree ∣ (p * r).homogenize (p * r).natDegree
⊢ p.homogenize p.natDegree ∣ q.homogenize q.natDegree

Tactic:
rcases h with ⟨r, rfl⟩

Premises used: rfl
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : NoZeroDivisors R
p r : R[X]
tauto tauto₁ tauto₂ : ¬p = 0 → r = 0 ∨ p ≠ 0 ∧ r ≠ 0
left : ¬p = 0 → ¬r = 0 → p ≠ 0
right : ¬p = 0 → ¬r = 0 → r ≠ 0
⊢ p = 0 ∨ r = 0 ∨ p ≠ 0 ∧ r ≠ 0

Tactic:
tauto
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : NoZeroDivisors R
p r : R[X]
inl : homogenize 0 (natDegree.{u_1} (R := R) 0) ∣ (0 * r).homogenize (0 * r).natDegree
inr : p.homogenize p.natDegree ∣ (p * 0).homogenize (p * 0).natDegree
inr₁ : ∀ (hp₀ : p ≠ 0) (hr₀ : r ≠ 0), p.homogenize p.natDegree ∣ (p * r).homogenize (p * r).natDegree
⊢ p.homogenize p.natDegree ∣ (p * r).homogenize (p * r).natDegree

Tactic:
obtain rfl | rfl | ⟨hp₀, hr₀⟩ : p = 0 ∨ r = 0 ∨ p ≠ 0 ∧ r ≠ 0 := by tauto

Premises used: rfl
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : NoZeroDivisors R
r : R[X]
⊢ homogenize 0 (natDegree.{u_1} (R := R) 0) ∣ (0 * r).homogenize (0 * r).natDegree

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : NoZeroDivisors R
p : R[X]
⊢ p.homogenize p.natDegree ∣ (p * 0).homogenize (p * 0).natDegree

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : NoZeroDivisors R
p r : R[X]
hp₀ : p ≠ 0
hr₀ : r ≠ 0
inr : p.homogenize p.natDegree ∣ p.homogenize p.natDegree * r.homogenize r.natDegree
⊢ p.homogenize p.natDegree ∣ (p * r).homogenize (p * r).natDegree

Tactic:
rw [natDegree_mul hp₀ hr₀, homogenize_mul _ _ le_rfl le_rfl]

Premises used: le_rfl, Polynomial.natDegree_mul, Polynomial.homogenize_mul
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : NoZeroDivisors R
p r : R[X]
hp₀ : p ≠ 0
hr₀ : r ≠ 0
⊢ p.homogenize p.natDegree ∣ p.homogenize p.natDegree * r.homogenize r.natDegree

Tactic:
apply dvd_mul_right

Premises used: dvd_mul_right
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
R : Type u_1
inst : CommRing R
p : R[X]
n : ℕ
⊢ (-p).homogenize n = -p.homogenize n

Tactic:
map_neg (homogenizeLM n) p

Premises used: Multiset.sum, Multiset.foldr, Polynomial.homogenize, map_neg, Polynomial.homogenizeLM, Finset.sum
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
R : Type u_1
inst : CommRing R
p q : R[X]
n : ℕ
⊢ (p - q).homogenize n = p.homogenize n - q.homogenize n

Tactic:
map_sub (homogenizeLM n) p q

Premises used: Multiset.sum, Multiset.foldr, map_sub, Polynomial.homogenize, Polynomial.homogenizeLM, Finset.sum
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
K : Type u_1
inst : Semifield K
p : K[X]
n : ℕ
hn : p.natDegree ≤ n
x : Fin 2 → K
hx : x 1 ≠ 0
simp :
  Eq.{u_1 + 1} (α := K)
    (∑ i ∈ range n.succ,
      (MvPolynomial.eval x : (a : MvPolynomial (Fin 2) K) → K)
        ((MvPolynomial.monomial fun₀ | 0 => i | 1 => n - i : (a : K) → MvPolynomial (Fin 2) K) (p.coeff i) :
          MvPolynomial (Fin 2) K))
    (∑ i ∈ range n.succ, p.coeff i * (x 0 / x 1) ^ i * x 1 ^ n)
⊢ (MvPolynomial.eval x : (a : MvPolynomial (Fin 2) K) → K) (p.homogenize n) = eval (x 0 / x 1) p * x 1 ^ n

Tactic:
simp only [homogenize, Polynomial.eval_eq_sum_range' (Nat.lt_succ_iff.mpr hn),
    Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mk, Finset.sum_mul, MvPolynomial.eval_sum]

Premises used: Iff.mpr, Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mk, Polynomial.homogenize, Nat.lt_succ_iff, Polynomial.eval_eq_sum_range', MvPolynomial.eval_sum, Finset.sum_mul
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
K : Type u_1
inst : Semifield K
p : K[X]
n : ℕ
hn : p.natDegree ≤ n
x : Fin 2 → K
hx : x 1 ≠ 0
⊢ Eq.{u_1 + 1} (α := K)
    (∑ i ∈ range n.succ,
      (MvPolynomial.eval x : (a : MvPolynomial (Fin 2) K) → K)
        ((MvPolynomial.monomial fun₀ | 0 => i | 1 => n - i : (a : K) → MvPolynomial (Fin 2) K) (p.coeff i) :
          MvPolynomial (Fin 2) K))
    (∑ i ∈ range n.succ, p.coeff i * (x 0 / x 1) ^ i * x 1 ^ n)

Tactic:
Finset.sum_congr rfl fun k hk ↦ ?_

Premises used: Finset.sum_congr, rfl