awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Homogenize (goal)
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
⊢ (MvPolynomial.aeval ![X, 1] : (a : MvPolynomial (Fin (Nat.succ 0).succ) R) → R[X]) (p.homogenize n) = p
have hg : Eq.{u_1 + 1} (α := R[X]) (![X, 1] 1) 1
Tactic: rw [aeval_homogenize_of_eq_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Homogenize (goal)
Goal:
R : Type u_1
inst : CommSemiring R
n : ℕ
p : R[X]
⊢ (p.homogenize n).IsHomogeneous n
have 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
Tactic: refine MvPolynomial.IsHomogeneous.sum _ _ _ ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Homogenize (goal)
Goal:
R : Type u_1
inst : CommSemiring R
n : ℕ
p : R[X]
⊢ ∀ 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
have 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
Tactic: simp only [Prod.forall, mem_antidiagonal]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Homogenize (goal)
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
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)
have hn : ((Finsupp.degree : (a : Fin 2 →₀ ℕ) → ℕ) fun₀ | 0 => a | 1 => b) = a + b
Tactic: apply MvPolynomial.isHomogeneous_monomial
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Homogenize (goal)
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
⊢ p.homogenize n = q
have subst : homogenize ((MvPolynomial.aeval ![X, 1] : (a : MvPolynomial (Fin (Nat.succ 0).succ) R) → R[X]) q) n = q
Tactic: subst p
Cleared hypotheses: p, hpq
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Homogenize (goal)
Goal:
R : Type u_1
inst : CommSemiring R
n : ℕ
q : MvPolynomial (Fin 2) R
hq : q.IsHomogeneous n
⊢ homogenize ((MvPolynomial.aeval ![X, 1] : (a : MvPolynomial (Fin (Nat.succ 0).succ) R) → R[X]) q) n = q
have 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))
Tactic: rw [q.as_sum]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Homogenize (goal)
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)
    (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))
have 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))
Tactic: simp only [MvPolynomial.aeval_sum, MvPolynomial.aeval_monomial, ← C_eq_algebraMap,
    homogenize_finsetSum, homogenize_C_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Homogenize (goal)
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))
have 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)
Tactic: refine Finset.sum_congr rfl fun m hm ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Homogenize (goal)
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
⊢ 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)
have 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)
Tactic: rw [MvPolynomial.monomial_eq]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Homogenize (goal)
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
⊢ 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)
have 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)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Homogenize (goal)
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
⊢ 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)
have 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)
Tactic: obtain rfl : m.weight 1 = n := hq <| by simpa using hm
Cleared hypotheses: n, hq
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Homogenize (goal)
Goal:
R : Type u_1
inst : CommSemiring R
p q : R[X]
m n : ℕ
hm : p.natDegree ≤ m
hn : q.natDegree ≤ n
⊢ (p * q).homogenize (m + n) = p.homogenize m * q.homogenize n
have hq : (p.homogenize m * q.homogenize n).IsHomogeneous (m + n)
Tactic: apply homogenize_eq_of_isHomogeneous
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Homogenize (goal)
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)
⊢ (p * q).homogenize (m + n) = p.homogenize m * q.homogenize n
have hpq : (MvPolynomial.aeval ![X, 1] : (a : MvPolynomial (Fin (Nat.succ 0).succ) R) → R[X]) (p.homogenize m * q.homogenize n) =
  p * q
Tactic: apply homogenize_eq_of_isHomogeneous
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Homogenize (goal)
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 ∈ cons i s hi, (p i_1).natDegree ≤ n i_1
⊢ Eq.{u_1 + 1} (α := MvPolynomial (Fin 2) R) (homogenize (∏ i ∈ cons i s hi, p i) (∑ i ∈ cons i s hi, n i))
    (∏ i ∈ cons i s hi, (p i).homogenize (n i))
have 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)
Tactic: simp only [prod_cons, sum_cons, forall_mem_cons] at *
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Homogenize (goal)
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
⊢ (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)
have cons : natDegree.{u_1} (R := R) (∏ i ∈ s, p i) ≤ ∑ i ∈ s, n i
Tactic: rw [homogenize_mul _ _ h.1, ihs h.2]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Homogenize (goal)
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
⊢ Eq.{u_1 + 1} (α := MvPolynomial (Fin 2) R) (homogenize (∏ i ∈ s, p i) (∑ i ∈ s, n i))
    (∏ i ∈ s, (p i).homogenize (n i))
have 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))
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)
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Homogenize (goal)
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))
⊢ Eq.{u_1 + 1} (α := MvPolynomial (Fin 2) R) (homogenize (∏ i ∈ s, p i) (∑ i ∈ s, n i))
    (∏ i ∈ s, (p i).homogenize (n i))
have 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 ∈ cons i s hi, (p i_1).natDegree ≤ n i_1),
  Eq.{u_1 + 1} (α := MvPolynomial (Fin 2) R) (homogenize (∏ i ∈ cons i s hi, p i) (∑ i ∈ cons i s hi, n i))
    (∏ i ∈ cons i s hi, (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)
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Homogenize (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : NoZeroDivisors R
p q : R[X]
h : p ∣ q
⊢ p.homogenize p.natDegree ∣ q.homogenize q.natDegree
have rcases : ∀ (r : R[X]), p.homogenize p.natDegree ∣ (p * r).homogenize (p * r).natDegree
Tactic: rcases h with ⟨r, rfl⟩
Cleared hypotheses: q, h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Homogenize (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : NoZeroDivisors R
p r : R[X]
⊢ p = 0 ∨ r = 0 ∨ p ≠ 0 ∧ r ≠ 0
have tauto : ¬p = 0 → r = 0 ∨ p ≠ 0 ∧ r ≠ 0
Tactic: tauto
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Homogenize (goal)
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
⊢ p = 0 ∨ r = 0 ∨ p ≠ 0 ∧ r ≠ 0
have left : ¬p = 0 → ¬r = 0 → p ≠ 0
Tactic: tauto
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Homogenize (goal)
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
⊢ p = 0 ∨ r = 0 ∨ p ≠ 0 ∧ r ≠ 0
have right : ¬p = 0 → ¬r = 0 → r ≠ 0
Tactic: tauto
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Homogenize (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : NoZeroDivisors R
p r : R[X]
⊢ p.homogenize p.natDegree ∣ (p * r).homogenize (p * r).natDegree
have inl : homogenize 0 (natDegree.{u_1} (R := R) 0) ∣ (0 * r).homogenize (0 * r).natDegree
Tactic: obtain rfl | rfl | ⟨hp₀, hr₀⟩ : p = 0 ∨ r = 0 ∨ p ≠ 0 ∧ r ≠ 0 := by tauto
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Homogenize (goal)
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
⊢ p.homogenize p.natDegree ∣ (p * r).homogenize (p * r).natDegree
have inr : p.homogenize p.natDegree ∣ (p * 0).homogenize (p * 0).natDegree
Tactic: obtain rfl | rfl | ⟨hp₀, hr₀⟩ : p = 0 ∨ r = 0 ∨ p ≠ 0 ∧ r ≠ 0 := by tauto
Cleared hypotheses: r
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Homogenize (goal)
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
⊢ p.homogenize p.natDegree ∣ (p * r).homogenize (p * r).natDegree
have inr₁ : ∀ (hp₀ : p ≠ 0) (hr₀ : r ≠ 0), 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
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Homogenize (goal)
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 * r).homogenize (p * r).natDegree
have inr : p.homogenize p.natDegree ∣ p.homogenize p.natDegree * r.homogenize r.natDegree
Tactic: rw [natDegree_mul hp₀ hr₀, homogenize_mul _ _ le_rfl le_rfl]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Homogenize (goal)
Goal:
K : Type u_1
inst : Semifield K
p : K[X]
n : ℕ
hn : p.natDegree ≤ n
x : Fin 2 → K
hx : x 1 ≠ 0
⊢ (MvPolynomial.eval x : (a : MvPolynomial (Fin 2) K) → K) (p.homogenize n) = eval (x 0 / x 1) p * x 1 ^ n
have 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)
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]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Homogenize (goal)
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)
have refine : ∀ (k : ℕ) (hk : k ∈ range n.succ),
  (MvPolynomial.eval x : (a : MvPolynomial (Fin 2) K) → K)
      ((MvPolynomial.monomial fun₀ | 0 => k | 1 => n - k : (a : K) → MvPolynomial (Fin 2) K) (p.coeff k) :
        MvPolynomial (Fin 2) K) =
    p.coeff k * (x 0 / x 1) ^ k * x 1 ^ n
Tactic: refine Finset.sum_congr rfl fun k hk ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Homogenize (goal)
Goal:
K : Type u_1
inst : Semifield K
p : K[X]
n : ℕ
hn : p.natDegree ≤ n
x : Fin 2 → K
hx : x 1 ≠ 0
k : ℕ
hk : k ∈ range n.succ
⊢ (MvPolynomial.eval x : (a : MvPolynomial (Fin 2) K) → K)
      ((MvPolynomial.monomial fun₀ | 0 => k | 1 => n - k : (a : K) → MvPolynomial (Fin 2) K) (p.coeff k) :
        MvPolynomial (Fin 2) K) =
    p.coeff k * (x 0 / x 1) ^ k * x 1 ^ n
have rw : p.coeff k * (x 0 ^ k * (x 1 ^ n * (x 1 ^ k)⁻¹)) = p.coeff k * (x 0 / x 1) ^ k * x 1 ^ n
Tactic: rw [MvPolynomial.eval_monomial, Finsupp.update_eq_add_single, Finsupp.prod_add_index',
    Finsupp.prod_single_index, Finsupp.prod_single_index, pow_sub₀]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Homogenize (goal)
Goal:
K : Type u_1
inst : Semifield K
p : K[X]
n : ℕ
hn : p.natDegree ≤ n
x : Fin 2 → K
hx : x 1 ≠ 0
k : ℕ
hk : k ∈ range n.succ
rw : p.coeff k * (x 0 ^ k * (x 1 ^ n * (x 1 ^ k)⁻¹)) = p.coeff k * (x 0 / x 1) ^ k * x 1 ^ n
ha : x 1 ≠ 0
⊢ (MvPolynomial.eval x : (a : MvPolynomial (Fin 2) K) → K)
      ((MvPolynomial.monomial fun₀ | 0 => k | 1 => n - k : (a : K) → MvPolynomial (Fin 2) K) (p.coeff k) :
        MvPolynomial (Fin 2) K) =
    p.coeff k * (x 0 / x 1) ^ k * x 1 ^ n
have h : k ≤ n
Tactic: rw [MvPolynomial.eval_monomial, Finsupp.update_eq_add_single, Finsupp.prod_add_index',
    Finsupp.prod_single_index, Finsupp.prod_single_index, pow_sub₀]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Homogenize (goal)
Goal:
K : Type u_1
inst : Semifield K
p : K[X]
n : ℕ
hn : p.natDegree ≤ n
x : Fin 2 → K
hx : x 1 ≠ 0
k : ℕ
hk : k ∈ range n.succ
rw : p.coeff k * (x 0 ^ k * (x 1 ^ n * (x 1 ^ k)⁻¹)) = p.coeff k * (x 0 / x 1) ^ k * x 1 ^ n
ha : x 1 ≠ 0
h : k ≤ n
⊢ (MvPolynomial.eval x : (a : MvPolynomial (Fin 2) K) → K)
      ((MvPolynomial.monomial fun₀ | 0 => k | 1 => n - k : (a : K) → MvPolynomial (Fin 2) K) (p.coeff k) :
        MvPolynomial (Fin 2) K) =
    p.coeff k * (x 0 / x 1) ^ k * x 1 ^ n
have rw₁ : HPow.hPow (β := ℕ) (x 1) 0 = 1
Tactic: rw [MvPolynomial.eval_monomial, Finsupp.update_eq_add_single, Finsupp.prod_add_index',
    Finsupp.prod_single_index, Finsupp.prod_single_index, pow_sub₀]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Homogenize (goal)
Goal:
K : Type u_1
inst : Semifield K
p : K[X]
n : ℕ
hn : p.natDegree ≤ n
x : Fin 2 → K
hx : x 1 ≠ 0
k : ℕ
hk : k ∈ range n.succ
rw : p.coeff k * (x 0 ^ k * (x 1 ^ n * (x 1 ^ k)⁻¹)) = p.coeff k * (x 0 / x 1) ^ k * x 1 ^ n
ha : x 1 ≠ 0
h : k ≤ n
rw₁ : HPow.hPow (β := ℕ) (x 1) 0 = 1
⊢ (MvPolynomial.eval x : (a : MvPolynomial (Fin 2) K) → K)
      ((MvPolynomial.monomial fun₀ | 0 => k | 1 => n - k : (a : K) → MvPolynomial (Fin 2) K) (p.coeff k) :
        MvPolynomial (Fin 2) K) =
    p.coeff k * (x 0 / x 1) ^ k * x 1 ^ n
have rw₂ : HPow.hPow (β := ℕ) (x 0) 0 = 1
Tactic: rw [MvPolynomial.eval_monomial, Finsupp.update_eq_add_single, Finsupp.prod_add_index',
    Finsupp.prod_single_index, Finsupp.prod_single_index, pow_sub₀]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Homogenize (goal)
Goal:
K : Type u_1
inst : Semifield K
p : K[X]
n : ℕ
hn : p.natDegree ≤ n
x : Fin 2 → K
hx : x 1 ≠ 0
k : ℕ
hk : k ∈ range n.succ
rw : p.coeff k * (x 0 ^ k * (x 1 ^ n * (x 1 ^ k)⁻¹)) = p.coeff k * (x 0 / x 1) ^ k * x 1 ^ n
ha : x 1 ≠ 0
h : k ≤ n
rw₁ : HPow.hPow (β := ℕ) (x 1) 0 = 1
rw₂ : HPow.hPow (β := ℕ) (x 0) 0 = 1
⊢ (MvPolynomial.eval x : (a : MvPolynomial (Fin 2) K) → K)
      ((MvPolynomial.monomial fun₀ | 0 => k | 1 => n - k : (a : K) → MvPolynomial (Fin 2) K) (p.coeff k) :
        MvPolynomial (Fin 2) K) =
    p.coeff k * (x 0 / x 1) ^ k * x 1 ^ n
have h_zero : ∀ (a : Fin 2), HPow.hPow (β := ℕ) (x a) 0 = 1
Tactic: rw [MvPolynomial.eval_monomial, Finsupp.update_eq_add_single, Finsupp.prod_add_index',
    Finsupp.prod_single_index, Finsupp.prod_single_index, pow_sub₀]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Homogenize (goal)
Goal:
K : Type u_1
inst : Semifield K
p : K[X]
n : ℕ
hn : p.natDegree ≤ n
x : Fin 2 → K
hx : x 1 ≠ 0
k : ℕ
hk : k ∈ range n.succ
rw : p.coeff k * (x 0 ^ k * (x 1 ^ n * (x 1 ^ k)⁻¹)) = p.coeff k * (x 0 / x 1) ^ k * x 1 ^ n
ha : x 1 ≠ 0
h : k ≤ n
rw₁ : HPow.hPow (β := ℕ) (x 1) 0 = 1
rw₂ : HPow.hPow (β := ℕ) (x 0) 0 = 1
h_zero : ∀ (a : Fin 2), HPow.hPow (β := ℕ) (x a) 0 = 1
⊢ (MvPolynomial.eval x : (a : MvPolynomial (Fin 2) K) → K)
      ((MvPolynomial.monomial fun₀ | 0 => k | 1 => n - k : (a : K) → MvPolynomial (Fin 2) K) (p.coeff k) :
        MvPolynomial (Fin 2) K) =
    p.coeff k * (x 0 / x 1) ^ k * x 1 ^ n
have h_add : ∀ (a : Fin 2) (b₁ b₂ : ℕ), x a ^ (b₁ + b₂) = x a ^ b₁ * x a ^ b₂
Tactic: rw [MvPolynomial.eval_monomial, Finsupp.update_eq_add_single, Finsupp.prod_add_index',
    Finsupp.prod_single_index, Finsupp.prod_single_index, pow_sub₀]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Homogenize (goal)
Goal:
K : Type u_1
inst : Semifield K
p : K[X]
n : ℕ
hn : p.natDegree ≤ n
x : Fin 2 → K
hx : x 1 ≠ 0
k : ℕ
hk : k ∈ range n.succ
rw : p.coeff k * (x 0 ^ k * (x 1 ^ n * (x 1 ^ k)⁻¹)) = p.coeff k * (x 0 / x 1) ^ k * x 1 ^ n
ha : x 1 ≠ 0
h : k ≤ n
rw₁ : HPow.hPow (β := ℕ) (x 1) 0 = 1
rw₂ : HPow.hPow (β := ℕ) (x 0) 0 = 1
h_zero : ∀ (a : Fin 2), HPow.hPow (β := ℕ) (x a) 0 = 1
h_add : ∀ (a : Fin 2) (b₁ b₂ : ℕ), x a ^ (b₁ + b₂) = x a ^ b₁ * x a ^ b₂
⊢ (MvPolynomial.eval x : (a : MvPolynomial (Fin 2) K) → K)
      ((MvPolynomial.monomial fun₀ | 0 => k | 1 => n - k : (a : K) → MvPolynomial (Fin 2) K) (p.coeff k) :
        MvPolynomial (Fin 2) K) =
    p.coeff k * (x 0 / x 1) ^ k * x 1 ^ n
have h₁ : Eq (α := ℕ) ((fun₀ | 0 => k : (a : Fin 2) → ℕ) 1 : ℕ) (0 : ℕ)
Tactic: rw [MvPolynomial.eval_monomial, Finsupp.update_eq_add_single, Finsupp.prod_add_index',
    Finsupp.prod_single_index, Finsupp.prod_single_index, pow_sub₀]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Homogenize (goal)
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
i : Fin 2
⊢ (p.toTupleMvPolynomial i).IsHomogeneous p.natDegree
have 0 : (p.toTupleMvPolynomial ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2))).IsHomogeneous p.natDegree
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Homogenize (goal)
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
i : Fin 2
0 : (p.toTupleMvPolynomial ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))).IsHomogeneous p.natDegree
⊢ (p.toTupleMvPolynomial i).IsHomogeneous p.natDegree
have 1 : (p.toTupleMvPolynomial ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2))).IsHomogeneous p.natDegree
Tactic: fin_cases i
Cleared hypotheses: i