awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
Goal:
R : Type u_1
inst : Semiring R
k : ℕ
D : (k : ℕ) → R[X] →+ R[X] := fun (k : ℕ) ↦ LinearMap.toAddMonoidHom (hasseDeriv k)
Φ : R[X] →+ R[X] →+ R[X] := mul
m : ℕ
r : R
n : ℕ
s : R
aux :
  ∀ x ∈ @antidiagonal _ instAddMonoid _ k,
    Eq (α := R[X])
      ((monomial (m - x.1 + (n - x.2)) : (a : R) → R[X]) ((↑(m.choose x.1) : R) * r * ((↑(n.choose x.2) : R) * s)) :
        R[X])
      ((monomial (m + n - k) : (a : R) → R[X])
          (HMul.hMul (α := R) (↑(m.choose x.1) : R) (↑(n.choose x.2) : R) * (r * s)) :
        R[X])
⊢ Eq.{u_1 + 1} (α := R) (↑((m + n).choose k) : R)
    (∑ i ∈ @antidiagonal _ instAddMonoid _ k, HMul.hMul (α := R) (↑(m.choose i.1) : R) (↑(n.choose i.2) : R))
have e_a : ∀
  (aux :
    ∀ x ∈ @antidiagonal _ instAddMonoid _ k,
      Eq (α := R[X])
        ((monomial (m - x.1 + (n - x.2)) : (a : R) → R[X]) ((↑(m.choose x.1) : R) * r * ((↑(n.choose x.2) : R) * s)) :
          R[X])
        ((monomial (m + n - k) : (a : R) → R[X]) ((↑(m.choose x.1 * n.choose x.2) : R) * (r * s)) : R[X])),
  Eq.{u_1 + 1} (α := R) (↑((m + n).choose k) : R)
    (↑(∑ x ∈ @antidiagonal _ instAddMonoid _ k, m.choose x.1 * n.choose x.2) : R)
Tactic: rw_mod_cast [← Nat.add_choose_eq]
Cleared hypotheses: aux
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Homogenize (goal)
Goal:
R : Type u_1
inst : CommSemiring R
m n : ℕ
h : m ≤ n
r : R
⊢ Eq.{u_1 + 1} (α := MvPolynomial (Fin 2) R) (homogenize ((monomial m : (a : R) → R[X]) r) n)
    ((MvPolynomial.monomial fun₀ | 0 => m | 1 => n - m : (a : R) → MvPolynomial (Fin 2) R) r)
have rw : Eq (α := MvPolynomial (Fin 2) R)
  ((MvPolynomial.monomial fun₀ | 0 => (m, n - m).1 | 1 => (m, n - m).2 : (a : R) → MvPolynomial (Fin 2) R)
      (coeff ((monomial m : (a : R) → R[X]) r) (m, n - m).1) :
    MvPolynomial (Fin 2) R)
  ((MvPolynomial.monomial fun₀ | 0 => m | 1 => n - m : (a : R) → MvPolynomial (Fin 2) R) r : MvPolynomial (Fin 2) R)
Tactic: rw [homogenize, Finset.sum_eq_single (a := (m, n - m))]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Homogenize (goal)
Goal:
R : Type u_1
inst : CommSemiring R
m n : ℕ
h : m ≤ n
r : R
rw :
  Eq (α := MvPolynomial (Fin 2) R)
    ((MvPolynomial.monomial fun₀ | 0 => (m, n - m).1 | 1 => (m, n - m).2 : (a : R) → MvPolynomial (Fin 2) R)
        (coeff ((monomial m : (a : R) → R[X]) r) (m, n - m).1) :
      MvPolynomial (Fin 2) R)
    ((MvPolynomial.monomial fun₀ | 0 => m | 1 => n - m : (a : R) → MvPolynomial (Fin 2) R) r : MvPolynomial (Fin 2) R)
⊢ Eq.{u_1 + 1} (α := MvPolynomial (Fin 2) R) (homogenize ((monomial m : (a : R) → R[X]) r) n)
    ((MvPolynomial.monomial fun₀ | 0 => m | 1 => n - m : (a : R) → MvPolynomial (Fin 2) R) r)
have h₀ : ∀ b ∈ @antidiagonal _ Nat.instAddMonoid _ n,
  b ≠ (m, n - m) →
    Eq.{u_1 + 1} (α := MvPolynomial (Fin 2) R)
      ((MvPolynomial.monomial fun₀ | 0 => b.1 | 1 => b.2 : (a : R) → MvPolynomial (Fin 2) R)
        (coeff ((monomial m : (a : R) → R[X]) r) b.1))
      0
Tactic: rw [homogenize, Finset.sum_eq_single (a := (m, n - m))]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Homogenize (goal)
Goal:
R : Type u_1
inst : CommSemiring R
m n : ℕ
h : m ≤ n
r : R
rw :
  Eq (α := MvPolynomial (Fin 2) R)
    ((MvPolynomial.monomial fun₀ | 0 => (m, n - m).1 | 1 => (m, n - m).2 : (a : R) → MvPolynomial (Fin 2) R)
        (coeff ((monomial m : (a : R) → R[X]) r) (m, n - m).1) :
      MvPolynomial (Fin 2) R)
    ((MvPolynomial.monomial fun₀ | 0 => m | 1 => n - m : (a : R) → MvPolynomial (Fin 2) R) r : MvPolynomial (Fin 2) R)
h₀ :
  ∀ b ∈ @antidiagonal _ Nat.instAddMonoid _ n,
    b ≠ (m, n - m) →
      Eq.{u_1 + 1} (α := MvPolynomial (Fin 2) R)
        ((MvPolynomial.monomial fun₀ | 0 => b.1 | 1 => b.2 : (a : R) → MvPolynomial (Fin 2) R)
          (coeff ((monomial m : (a : R) → R[X]) r) b.1))
        0
⊢ Eq.{u_1 + 1} (α := MvPolynomial (Fin 2) R) (homogenize ((monomial m : (a : R) → R[X]) r) n)
    ((MvPolynomial.monomial fun₀ | 0 => m | 1 => n - m : (a : R) → MvPolynomial (Fin 2) R) r)
have h₁ : (m, n - m) ∉ @antidiagonal _ Nat.instAddMonoid _ n →
  Eq.{u_1 + 1} (α := MvPolynomial (Fin 2) R)
    ((MvPolynomial.monomial fun₀ | 0 => (m, n - m).1 | 1 => (m, n - m).2 : (a : R) → MvPolynomial (Fin 2) R)
      (coeff ((monomial m : (a : R) → R[X]) r) (m, n - m).1))
    0
Tactic: rw [homogenize, Finset.sum_eq_single (a := (m, n - m))]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Homogenize (goal)
Goal:
R : Type u_1
inst : CommSemiring R
m n : ℕ
h : n < m
r : R
⊢ Eq.{u_1 + 1} (α := MvPolynomial (Fin 2) R)
    (∑ kl ∈ @antidiagonal _ Nat.instAddMonoid _ n,
      (MvPolynomial.monomial fun₀ | 0 => kl.1 | 1 => kl.2 : (a : R) → MvPolynomial (Fin 2) R)
        (coeff ((monomial m : (a : R) → R[X]) r) kl.1))
    0
have h₁ : ∀ x ∈ @antidiagonal _ Nat.instAddMonoid _ n,
  Eq.{u_1 + 1} (α := MvPolynomial (Fin 2) R)
    ((MvPolynomial.monomial fun₀ | 0 => x.1 | 1 => x.2 : (a : R) → MvPolynomial (Fin 2) R)
      (coeff ((monomial m : (a : R) → R[X]) r) x.1))
    0
Tactic: apply Finset.sum_eq_zero
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Homogenize (goal)
Goal:
R : Type u_1
inst : CommSemiring R
m n : ℕ
h : m ≤ n
⊢ (HPow.hPow (α := R[X]) X m).homogenize n =
    HPow.hPow (α := MvPolynomial (Fin 2) R) (MvPolynomial.X 0) m *
      HPow.hPow (α := MvPolynomial (Fin 2) R) (MvPolynomial.X 1) (n - m)
have rw : homogenize ((monomial m : (a : R) → R[X]) 1) n =
  HPow.hPow (α := MvPolynomial (Fin 2) R) (MvPolynomial.X 0) m *
    HPow.hPow (α := MvPolynomial (Fin 2) R) (MvPolynomial.X 1) (n - m)
Tactic: rw [X_pow_eq_monomial, homogenize_monomial h, Finsupp.update_eq_add_single (by simp),
    MvPolynomial.monomial_single_add, ← MvPolynomial.X_pow_eq_monomial]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Homogenize (goal)
Goal:
R : Type u_1
inst : CommSemiring R
m n : ℕ
h : m ≤ n
rw :
  homogenize ((monomial m : (a : R) → R[X]) 1) n =
    HPow.hPow (α := MvPolynomial (Fin 2) R) (MvPolynomial.X 0) m *
      HPow.hPow (α := MvPolynomial (Fin 2) R) (MvPolynomial.X 1) (n - m)
⊢ (HPow.hPow (α := R[X]) X m).homogenize n =
    HPow.hPow (α := MvPolynomial (Fin 2) R) (MvPolynomial.X 0) m *
      HPow.hPow (α := MvPolynomial (Fin 2) R) (MvPolynomial.X 1) (n - m)
have rw₁ : (MvPolynomial.monomial fun₀ | 0 => m | 1 => n - m : (a : R) → MvPolynomial (Fin 2) R) 1 =
  HPow.hPow (α := MvPolynomial (Fin 2) R) (MvPolynomial.X 0) m *
    HPow.hPow (α := MvPolynomial (Fin 2) R) (MvPolynomial.X 1) (n - m)
Tactic: rw [X_pow_eq_monomial, homogenize_monomial h, Finsupp.update_eq_add_single (by simp),
    MvPolynomial.monomial_single_add, ← MvPolynomial.X_pow_eq_monomial]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Homogenize (goal)
Goal:
R : Type u_1
inst : CommSemiring R
m n : ℕ
h : m ≤ n
rw :
  homogenize ((monomial m : (a : R) → R[X]) 1) n =
    HPow.hPow (α := MvPolynomial (Fin 2) R) (MvPolynomial.X 0) m *
      HPow.hPow (α := MvPolynomial (Fin 2) R) (MvPolynomial.X 1) (n - m)
rw₁ :
  (MvPolynomial.monomial fun₀ | 0 => m | 1 => n - m : (a : R) → MvPolynomial (Fin 2) R) 1 =
    HPow.hPow (α := MvPolynomial (Fin 2) R) (MvPolynomial.X 0) m *
      HPow.hPow (α := MvPolynomial (Fin 2) R) (MvPolynomial.X 1) (n - m)
⊢ (HPow.hPow (α := R[X]) X m).homogenize n =
    HPow.hPow (α := MvPolynomial (Fin 2) R) (MvPolynomial.X 0) m *
      HPow.hPow (α := MvPolynomial (Fin 2) R) (MvPolynomial.X 1) (n - m)
have rw₂ : (MvPolynomial.monomial (HAdd.hAdd (α := Fin 2 →₀ ℕ) (fun₀ | 0 => m) fun₀ | 1 => n - m) :
      (a : R) → MvPolynomial (Fin 2) R)
    1 =
  HPow.hPow (α := MvPolynomial (Fin 2) R) (MvPolynomial.X 0) m *
    HPow.hPow (α := MvPolynomial (Fin 2) R) (MvPolynomial.X 1) (n - m)
Tactic: rw [X_pow_eq_monomial, homogenize_monomial h, Finsupp.update_eq_add_single (by simp),
    MvPolynomial.monomial_single_add, ← MvPolynomial.X_pow_eq_monomial]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Homogenize (goal)
Goal:
R : Type u_1
inst : CommSemiring R
m n : ℕ
h : m ≤ n
rw :
  homogenize ((monomial m : (a : R) → R[X]) 1) n =
    HPow.hPow (α := MvPolynomial (Fin 2) R) (MvPolynomial.X 0) m *
      HPow.hPow (α := MvPolynomial (Fin 2) R) (MvPolynomial.X 1) (n - m)
rw₁ :
  (MvPolynomial.monomial fun₀ | 0 => m | 1 => n - m : (a : R) → MvPolynomial (Fin 2) R) 1 =
    HPow.hPow (α := MvPolynomial (Fin 2) R) (MvPolynomial.X 0) m *
      HPow.hPow (α := MvPolynomial (Fin 2) R) (MvPolynomial.X 1) (n - m)
rw₂ :
  (MvPolynomial.monomial (HAdd.hAdd (α := Fin 2 →₀ ℕ) (fun₀ | 0 => m) fun₀ | 1 => n - m) :
        (a : R) → MvPolynomial (Fin 2) R)
      1 =
    HPow.hPow (α := MvPolynomial (Fin 2) R) (MvPolynomial.X 0) m *
      HPow.hPow (α := MvPolynomial (Fin 2) R) (MvPolynomial.X 1) (n - m)
⊢ (HPow.hPow (α := R[X]) X m).homogenize n =
    HPow.hPow (α := MvPolynomial (Fin 2) R) (MvPolynomial.X 0) m *
      HPow.hPow (α := MvPolynomial (Fin 2) R) (MvPolynomial.X 1) (n - m)
have rw₃ : HPow.hPow (α := MvPolynomial (Fin 2) R) (MvPolynomial.X 0) m *
    (MvPolynomial.monomial fun₀ | 1 => n - m : (a : R) → MvPolynomial (Fin 2) R) 1 =
  HPow.hPow (α := MvPolynomial (Fin 2) R) (MvPolynomial.X 0) m *
    HPow.hPow (α := MvPolynomial (Fin 2) R) (MvPolynomial.X 1) (n - m)
Tactic: rw [X_pow_eq_monomial, homogenize_monomial h, Finsupp.update_eq_add_single (by simp),
    MvPolynomial.monomial_single_add, ← MvPolynomial.X_pow_eq_monomial]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Homogenize (goal)
Goal:
R : Type u_1
inst : CommSemiring R
m n : ℕ
h : m ≤ n
rw :
  homogenize ((monomial m : (a : R) → R[X]) 1) n =
    HPow.hPow (α := MvPolynomial (Fin 2) R) (MvPolynomial.X 0) m *
      HPow.hPow (α := MvPolynomial (Fin 2) R) (MvPolynomial.X 1) (n - m)
rw₁ :
  (MvPolynomial.monomial fun₀ | 0 => m | 1 => n - m : (a : R) → MvPolynomial (Fin 2) R) 1 =
    HPow.hPow (α := MvPolynomial (Fin 2) R) (MvPolynomial.X 0) m *
      HPow.hPow (α := MvPolynomial (Fin 2) R) (MvPolynomial.X 1) (n - m)
rw₂ :
  (MvPolynomial.monomial (HAdd.hAdd (α := Fin 2 →₀ ℕ) (fun₀ | 0 => m) fun₀ | 1 => n - m) :
        (a : R) → MvPolynomial (Fin 2) R)
      1 =
    HPow.hPow (α := MvPolynomial (Fin 2) R) (MvPolynomial.X 0) m *
      HPow.hPow (α := MvPolynomial (Fin 2) R) (MvPolynomial.X 1) (n - m)
rw₃ :
  HPow.hPow (α := MvPolynomial (Fin 2) R) (MvPolynomial.X 0) m *
      (MvPolynomial.monomial fun₀ | 1 => n - m : (a : R) → MvPolynomial (Fin 2) R) 1 =
    HPow.hPow (α := MvPolynomial (Fin 2) R) (MvPolynomial.X 0) m *
      HPow.hPow (α := MvPolynomial (Fin 2) R) (MvPolynomial.X 1) (n - m)
⊢ (HPow.hPow (α := R[X]) X m).homogenize n =
    HPow.hPow (α := MvPolynomial (Fin 2) R) (MvPolynomial.X 0) m *
      HPow.hPow (α := MvPolynomial (Fin 2) R) (MvPolynomial.X 1) (n - m)
have rw₄ : HPow.hPow (α := MvPolynomial (Fin 2) R) (MvPolynomial.X 0) m *
    HPow.hPow (α := MvPolynomial (Fin 2) R) (MvPolynomial.X 1) (n - m) =
  HPow.hPow (α := MvPolynomial (Fin 2) R) (MvPolynomial.X 0) m *
    HPow.hPow (α := MvPolynomial (Fin 2) R) (MvPolynomial.X 1) (n - m)
Tactic: rw [X_pow_eq_monomial, homogenize_monomial h, Finsupp.update_eq_add_single (by simp),
    MvPolynomial.monomial_single_add, ← MvPolynomial.X_pow_eq_monomial]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Homogenize (goal)
Goal:
R : Type u_1
inst : CommSemiring R
n : ℕ
hn : n ≠ 0
⊢ homogenize X n = MvPolynomial.X 0 * HPow.hPow (α := MvPolynomial (Fin 2) R) (MvPolynomial.X 1) (n - 1)
have rw : 1 ≤ n
Tactic: rw [← pow_one X, homogenize_X_pow, pow_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Homogenize (goal)
Goal:
R : Type u_1
inst : CommSemiring R
n : ℕ
m : Fin 2 →₀ ℕ
k : ℕ
c : R
⊢ Eq.{u_1 + 1} (α := R) (MvPolynomial.coeff m (homogenize ((monomial k : (a : R) → R[X]) c) n))
    (if HAdd.hAdd (α := ℕ) (β := ℕ) ((m : (a : Fin 2) → ℕ) 0 : ℕ) ((m : (a : Fin 2) → ℕ) 1 : ℕ) = n then
      coeff ((monomial k : (a : R) → R[X]) c) ((m : (a : Fin 2) → ℕ) 0)
    else 0)
have monomial : ∀ (hkn : k ≤ n),
  Eq.{u_1 + 1} (α := R) (MvPolynomial.coeff m (homogenize ((monomial k : (a : R) → R[X]) c) n))
    (if HAdd.hAdd (α := ℕ) (β := ℕ) ((m : (a : Fin 2) → ℕ) 0 : ℕ) ((m : (a : Fin 2) → ℕ) 1 : ℕ) = n then
      coeff ((monomial k : (a : R) → R[X]) c) ((m : (a : Fin 2) → ℕ) 0)
    else 0)
Tactic: rcases le_or_gt k n with hkn | hnk
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Homogenize (goal)
Goal:
R : Type u_1
inst : CommSemiring R
n : ℕ
m : Fin 2 →₀ ℕ
k : ℕ
c : R
monomial :
  ∀ (hkn : k ≤ n),
    Eq.{u_1 + 1} (α := R) (MvPolynomial.coeff m (homogenize ((Polynomial.monomial k : (a : R) → R[X]) c) n))
      (if HAdd.hAdd (α := ℕ) (β := ℕ) ((m : (a : Fin 2) → ℕ) 0 : ℕ) ((m : (a : Fin 2) → ℕ) 1 : ℕ) = n then
        coeff ((Polynomial.monomial k : (a : R) → R[X]) c) ((m : (a : Fin 2) → ℕ) 0)
      else 0)
⊢ Eq.{u_1 + 1} (α := R) (MvPolynomial.coeff m (homogenize ((Polynomial.monomial k : (a : R) → R[X]) c) n))
    (if HAdd.hAdd (α := ℕ) (β := ℕ) ((m : (a : Fin 2) → ℕ) 0 : ℕ) ((m : (a : Fin 2) → ℕ) 1 : ℕ) = n then
      coeff ((Polynomial.monomial k : (a : R) → R[X]) c) ((m : (a : Fin 2) → ℕ) 0)
    else 0)
have monomial₁ : ∀ (hnk : n < k),
  Eq.{u_1 + 1} (α := R) (MvPolynomial.coeff m (homogenize ((Polynomial.monomial k : (a : R) → R[X]) c) n))
    (if HAdd.hAdd (α := ℕ) (β := ℕ) ((m : (a : Fin 2) → ℕ) 0 : ℕ) ((m : (a : Fin 2) → ℕ) 1 : ℕ) = n then
      coeff ((Polynomial.monomial k : (a : R) → R[X]) c) ((m : (a : Fin 2) → ℕ) 0)
    else 0)
Tactic: rcases le_or_gt k n with hkn | hnk
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Homogenize (goal)
Goal:
R : Type u_1
inst : CommSemiring R
n : ℕ
m : Fin 2 →₀ ℕ
k : ℕ
c : R
hkn : k ≤ n
⊢ Eq.{u_1 + 1} (α := R) (MvPolynomial.coeff m (homogenize ((monomial k : (a : R) → R[X]) c) n))
    (if HAdd.hAdd (α := ℕ) (β := ℕ) ((m : (a : Fin 2) → ℕ) 0 : ℕ) ((m : (a : Fin 2) → ℕ) 1 : ℕ) = n then
      coeff ((monomial k : (a : R) → R[X]) c) ((m : (a : Fin 2) → ℕ) 0)
    else 0)
have monomial : (if (fun₀ | 0 => k | 1 => n - k) = m then c else 0) =
  if HAdd.hAdd (α := ℕ) (β := ℕ) ((m : (a : Fin 2) → ℕ) 0 : ℕ) ((m : (a : Fin 2) → ℕ) 1 : ℕ) = n then
    if k = (m : (a : Fin 2) → ℕ) 0 then c else 0
  else 0
Tactic: rw [homogenize_monomial hkn, coeff_monomial, MvPolynomial.coeff_monomial]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Homogenize (goal)
Goal:
R : Type u_1
inst : CommSemiring R
n : ℕ
m : Fin 2 →₀ ℕ
k : ℕ
c : R
hkn : k ≤ n
⊢ (fun₀ | 0 => (m : (a : Fin 2) → ℕ) 0 | 1 => (m : (a : Fin 2) → ℕ) 1) = m
have h : ∀ (i : Fin 2),
  Eq (α := ℕ)
    (((fun₀ | 0 => (m : (a : Fin 2) → ℕ) 0 | 1 => (m : (a : Fin 2) → ℕ) 1 : Fin 2 →₀ ℕ) : (a : Fin 2) → ℕ) i : ℕ)
    ((m : (a : Fin 2) → ℕ) i : ℕ)
Tactic: ext i
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Homogenize (goal)
Goal:
R : Type u_1
inst : CommSemiring R
n : ℕ
m : Fin 2 →₀ ℕ
k : ℕ
c : R
hkn : k ≤ n
i : Fin 2
⊢ Eq (α := ℕ)
    (((fun₀ | 0 => (m : (a : Fin 2) → ℕ) 0 | 1 => (m : (a : Fin 2) → ℕ) 1 : Fin 2 →₀ ℕ) : (a : Fin 2) → ℕ) i : ℕ)
    ((m : (a : Fin 2) → ℕ) i : ℕ)
have h : Eq (α := ℕ)
  (((fun₀ | 0 => (m : (a : Fin 2) → ℕ) 0 | 1 => (m : (a : Fin 2) → ℕ) 1 : Fin 2 →₀ ℕ) : (a : Fin 2) → ℕ)
      ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) :
    ℕ)
  ((m : (a : Fin 2) → ℕ) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) : ℕ)
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
n : ℕ
m : Fin 2 →₀ ℕ
k : ℕ
c : R
hkn : k ≤ n
i : Fin 2
h :
  Eq (α := ℕ)
    (((fun₀ | 0 => (m : (a : Fin 2) → ℕ) 0 | 1 => (m : (a : Fin 2) → ℕ) 1 : Fin 2 →₀ ℕ) : (a : Fin 2) → ℕ)
        ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) :
      ℕ)
    ((m : (a : Fin 2) → ℕ) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) : ℕ)
⊢ Eq (α := ℕ)
    (((fun₀ | 0 => (m : (a : Fin 2) → ℕ) 0 | 1 => (m : (a : Fin 2) → ℕ) 1 : Fin 2 →₀ ℕ) : (a : Fin 2) → ℕ) i : ℕ)
    ((m : (a : Fin 2) → ℕ) i : ℕ)
have h₁ : Eq (α := ℕ)
  (((fun₀ | 0 => (m : (a : Fin 2) → ℕ) 0 | 1 => (m : (a : Fin 2) → ℕ) 1 : Fin 2 →₀ ℕ) : (a : Fin 2) → ℕ)
      ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) :
    ℕ)
  ((m : (a : Fin 2) → ℕ) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) : ℕ)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Homogenize (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
n : ℕ
m : Fin 2 →₀ ℕ
k : ℕ
c : R
hkn : k ≤ n
⊢ (if (fun₀ | 0 => k | 1 => n - k) = m then c else 0) =
    if HAdd.hAdd (α := ℕ) (β := ℕ) ((m : (a : Fin 2) → ℕ) 0 : ℕ) ((m : (a : Fin 2) → ℕ) 1 : ℕ) = n then
      if k = (m : (a : Fin 2) → ℕ) 0 then c else 0
    else 0
have this : (fun₀ | 0 => (m : (a : Fin 2) → ℕ) 0 | 1 => (m : (a : Fin 2) → ℕ) 1) = m
Tactic: have : (fun₀ | 0 => m 0 | 1 => m 1) = m := by ext i; fin_cases i <;> simp
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Homogenize (goal)
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
n : ℕ
m : Fin 2 →₀ ℕ
⊢ MvPolynomial.coeff m (p.homogenize n) =
    if HAdd.hAdd (α := ℕ) (β := ℕ) ((m : (a : Fin 2) → ℕ) 0 : ℕ) ((m : (a : Fin 2) → ℕ) 1 : ℕ) = n then
      p.coeff ((m : (a : Fin 2) → ℕ) 0)
    else 0
have add : ∀ (p q : R[X])
  (ihp :
    MvPolynomial.coeff m (p.homogenize n) =
      if HAdd.hAdd (α := ℕ) (β := ℕ) ((m : (a : Fin 2) → ℕ) 0 : ℕ) ((m : (a : Fin 2) → ℕ) 1 : ℕ) = n then
        p.coeff ((m : (a : Fin 2) → ℕ) 0)
      else 0)
  (ihq :
    MvPolynomial.coeff m (q.homogenize n) =
      if HAdd.hAdd (α := ℕ) (β := ℕ) ((m : (a : Fin 2) → ℕ) 0 : ℕ) ((m : (a : Fin 2) → ℕ) 1 : ℕ) = n then
        q.coeff ((m : (a : Fin 2) → ℕ) 0)
      else 0),
  MvPolynomial.coeff m ((p + q).homogenize n) =
    if HAdd.hAdd (α := ℕ) (β := ℕ) ((m : (a : Fin 2) → ℕ) 0 : ℕ) ((m : (a : Fin 2) → ℕ) 1 : ℕ) = n then
      (p + q).coeff ((m : (a : Fin 2) → ℕ) 0)
    else 0
Tactic: induction p using Polynomial.induction_on' with
  | add p q ihp ihq =>
    simp [*, ite_add_ite]
  | monomial k c =>
    rcases le_or_gt k n with hkn | hnk
    · rw [homogenize_monomial hkn, coeff_monomial, MvPolynomial.coeff_monomial]
      have : (fun₀ | 0 => m 0 | 1 => m 1) = m := by ext i; fin_cases i <;> simp
      aesop
    · aesop (add simp homogenize_monomial_of_lt) (add simp coeff_monomial)
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Homogenize (goal)
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
n : ℕ
m : Fin 2 →₀ ℕ
add :
  ∀ (p q : R[X])
    (ihp :
      MvPolynomial.coeff m (p.homogenize n) =
        if HAdd.hAdd (α := ℕ) (β := ℕ) ((m : (a : Fin 2) → ℕ) 0 : ℕ) ((m : (a : Fin 2) → ℕ) 1 : ℕ) = n then
          p.coeff ((m : (a : Fin 2) → ℕ) 0)
        else 0)
    (ihq :
      MvPolynomial.coeff m (q.homogenize n) =
        if HAdd.hAdd (α := ℕ) (β := ℕ) ((m : (a : Fin 2) → ℕ) 0 : ℕ) ((m : (a : Fin 2) → ℕ) 1 : ℕ) = n then
          q.coeff ((m : (a : Fin 2) → ℕ) 0)
        else 0),
    MvPolynomial.coeff m ((p + q).homogenize n) =
      if HAdd.hAdd (α := ℕ) (β := ℕ) ((m : (a : Fin 2) → ℕ) 0 : ℕ) ((m : (a : Fin 2) → ℕ) 1 : ℕ) = n then
        (p + q).coeff ((m : (a : Fin 2) → ℕ) 0)
      else 0
⊢ MvPolynomial.coeff m (p.homogenize n) =
    if HAdd.hAdd (α := ℕ) (β := ℕ) ((m : (a : Fin 2) → ℕ) 0 : ℕ) ((m : (a : Fin 2) → ℕ) 1 : ℕ) = n then
      p.coeff ((m : (a : Fin 2) → ℕ) 0)
    else 0
have monomial : ∀ (k : ℕ) (c : R),
  Eq.{u_1 + 1} (α := R) (MvPolynomial.coeff m (homogenize ((monomial k : (a : R) → R[X]) c) n))
    (if HAdd.hAdd (α := ℕ) (β := ℕ) ((m : (a : Fin 2) → ℕ) 0 : ℕ) ((m : (a : Fin 2) → ℕ) 1 : ℕ) = n then
      coeff ((monomial k : (a : R) → R[X]) c) ((m : (a : Fin 2) → ℕ) 0)
    else 0)
Tactic: induction p using Polynomial.induction_on' with
  | add p q ihp ihq =>
    simp [*, ite_add_ite]
  | monomial k c =>
    rcases le_or_gt k n with hkn | hnk
    · rw [homogenize_monomial hkn, coeff_monomial, MvPolynomial.coeff_monomial]
      have : (fun₀ | 0 => m 0 | 1 => m 1) = m := by ext i; fin_cases i <;> simp
      aesop
    · aesop (add simp homogenize_monomial_of_lt) (add simp coeff_monomial)
Cleared hypotheses: p
-- 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
h : p.homogenize n = 0
⊢ p = 0
have a : ∀ (i : ℕ), p.coeff i = coeff 0 i
Tactic: ext i
-- 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
h : p.homogenize n = 0
i : ℕ
⊢ p.coeff i = coeff 0 i
have a : p.coeff i = 0
Tactic: simp only [coeff_zero]
-- 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
h : p.homogenize n = 0
i : ℕ
⊢ p.coeff i = 0
have a : ∀ (H : i ≤ p.natDegree), p.coeff i = 0
Tactic: rcases le_or_gt i p.natDegree with H | H
-- 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
h : p.homogenize n = 0
i : ℕ
a : ∀ (H : i ≤ p.natDegree), p.coeff i = 0
⊢ p.coeff i = 0
have a₁ : ∀ (H : p.natDegree < i), p.coeff i = 0
Tactic: rcases le_or_gt i p.natDegree with H | H
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Homogenize (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
h : p.homogenize n = 0
i : ℕ
H : i ≤ p.natDegree
⊢ p.coeff i = 0
have this : p.coeff i = MvPolynomial.coeff (fun₀ | 0 => i | 1 => n - i) (p.homogenize n)
Tactic: have : p.coeff i = (p.homogenize n).coeff fun₀ | 0 => i | 1 => n - i := by
      simp [coeff_homogenize, Nat.add_sub_of_le (H.trans hn)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Homogenize (goal)
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
⊢ MvPolynomial.eval₂ f g (p.homogenize n) = eval₂ f (g 0) p
have zero : MvPolynomial.eval₂ f g (homogenize 0 n) = eval₂ f (g 0) 0
Tactic: apply Polynomial.induction_with_natDegree_le
    (fun p ↦ MvPolynomial.eval₂ f g (p.homogenize n) = p.eval₂ f (g 0)) (N := n)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Homogenize (goal)
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
zero : MvPolynomial.eval₂ f g (homogenize 0 n) = eval₂ f (g 0) 0
⊢ MvPolynomial.eval₂ f g (p.homogenize n) = eval₂ f (g 0) p
have C_mul_pow : ∀ (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: apply Polynomial.induction_with_natDegree_le
    (fun p ↦ MvPolynomial.eval₂ f g (p.homogenize n) = p.eval₂ f (g 0)) (N := n)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Homogenize (goal)
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
zero : MvPolynomial.eval₂ f g (homogenize 0 n) = eval₂ f (g 0) 0
C_mul_pow :
  ∀ (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))
⊢ MvPolynomial.eval₂ f g (p.homogenize n) = eval₂ f (g 0) p
have add : ∀ (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: apply Polynomial.induction_with_natDegree_le
    (fun p ↦ MvPolynomial.eval₂ f g (p.homogenize n) = p.eval₂ f (g 0)) (N := n)
-- 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
⊢ (MvPolynomial.aeval ![X, 1] : (a : MvPolynomial (Fin (Nat.succ 0).succ) R) → R[X]) (p.homogenize n) = p
have rw : (aeval (![X, 1] 0) : (a : R[X]) → R[X]) p = p
Tactic: rw [aeval_homogenize_of_eq_one]