awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
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])
e_a :
  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))
⊢ Eq (α := R[X]) ((monomial (m + n - k) : (a : R) → R[X]) ((↑((m + n).choose k) : R) * (r * s)) : R[X])
    ((monomial (m + n - k) : (a : R) → R[X])
        ((∑ i ∈ @antidiagonal _ instAddMonoid _ k, HMul.hMul (α := R) (↑(m.choose i.1) : R) (↑(n.choose i.2) : R)) *
          (r * s)) :
      R[X])

Tactic:
congr
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
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])
e_a e_a₁ e_a₂ e_a₃ e_a₄ 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)
⊢ 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))

Tactic:
rw_mod_cast [← Nat.add_choose_eq]

Premises used: Nat.add_choose_eq
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
R : Type u_1
inst : CommSemiring R
n : ℕ
⊢ Eq.{u_1 + 1} (α := MvPolynomial (Fin 2) R) (homogenize 0 n) 0

Tactic:
simp [homogenize]

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

Tactic:
simp [homogenize, Finset.sum_add_distrib]

Premises used: Finset.sum_add_distrib, Polynomial.homogenize
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : Semiring S
inst_2 : Module S R
c : S
p : R[X]
n : ℕ
⊢ (c • p).homogenize n = c • p.homogenize n

Tactic:
simp [homogenize, Finset.smul_sum, MvPolynomial.smul_monomial]

Premises used: MvPolynomial.smul_monomial, Polynomial.homogenize, Finset.smul_sum
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
R : Type u_1
inst : CommSemiring R
ι : Type u_2
s : Finset ι
p : ι → R[X]
n : ℕ
⊢ Eq.{u_1 + 1} (α := MvPolynomial (Fin 2) R) (homogenize (∑ i ∈ s, p i) n) (∑ i ∈ s, (p i).homogenize n)

Tactic:
_root_.map_sum (homogenizeLM n) p s

Premises used: Multiset.sum, Multiset.foldr, Polynomial.homogenize, map_sum, Polynomial.homogenizeLM, Finset.sum
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
f : R →+* S
p : R[X]
n : ℕ
⊢ (map f p).homogenize n =
    ((MvPolynomial.map f : RingHom.{u_1, u_2} (MvPolynomial (Fin 2) R) (MvPolynomial (Fin 2) S)) :
        (a : MvPolynomial (Fin 2) R) → MvPolynomial (Fin 2) S)
      (p.homogenize n)

Tactic:
simp [homogenize]

Premises used: Polynomial.homogenize
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
R : Type u_1
inst : CommSemiring R
c : R
p : R[X]
n : ℕ
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) c : R[X]) p).homogenize n =
    HMul.hMul (α := MvPolynomial (Fin 2) R)
      ((MvPolynomial.C : (a : R) → MvPolynomial (Fin 2) R) c : MvPolynomial (Fin 2) R) (p.homogenize n)

Tactic:
simp only [C_mul', homogenize_smul, MvPolynomial.C_mul']

Premises used: Polynomial.homogenize_smul, Polynomial.C_mul', MvPolynomial.C_mul'
-- Module: Mathlib.Algebra.Polynomial.Homogenize
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
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
⊢ 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)

Tactic:
rw [homogenize, Finset.sum_eq_single (a := (m, n - m))]

Premises used: HSub.hSub, Polynomial.homogenize, Prod.mk, Finset.sum_eq_single
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
R : Type u_1
inst : CommSemiring R
m n : ℕ
h : m ≤ n
r : R
⊢ 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:
simp
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
R : Type u_1
inst : CommSemiring R
m n : ℕ
h : m ≤ n
r : R
⊢ ∀ 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:
aesop (add simp coeff_monomial)

Premises used: Polynomial.coeff_monomial
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
R : Type u_1
inst : CommSemiring R
m n : ℕ
h : m ≤ n
r : R
⊢ (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:
simp [h]
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
R : Type u_1
inst : CommSemiring R
m n : ℕ
h : n < m
r : R
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
⊢ 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

Tactic:
apply Finset.sum_eq_zero

Premises used: Finset.sum_eq_zero
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
R : Type u_1
inst : CommSemiring R
m n : ℕ
h : n < m
r : R
⊢ ∀ 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:
aesop (add simp coeff_monomial)

Premises used: Polynomial.coeff_monomial
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
R : Type u_1
inst : CommSemiring R
m n : ℕ
h : m ≤ n
⊢ Eq (α := ℕ) ((fun₀ | 0 => m : (a : Fin 2) → ℕ) 1 : ℕ) (0 : ℕ)

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Homogenize
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)
rw₄ 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)
⊢ (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)

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]

Premises used: MvPolynomial.X_pow_eq_monomial, Finsupp.update_eq_add_single, Polynomial.X_pow_eq_monomial, MvPolynomial.monomial_single_add, Polynomial.homogenize_monomial
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
R : Type u_1
inst : CommSemiring R
n : ℕ
hn : n ≠ 0
rw : 1 ≤ n
⊢ homogenize X n = MvPolynomial.X 0 * HPow.hPow (α := MvPolynomial (Fin 2) R) (MvPolynomial.X 1) (n - 1)

Tactic:
rw [← pow_one X, homogenize_X_pow, pow_one]

Premises used: Polynomial.homogenize_X_pow, pow_one, Polynomial.X
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
R : Type u_1
inst : CommSemiring R
n : ℕ
hn rwa rwa₁ rwa₂ rwa₃ : n ≠ 0
⊢ 1 ≤ n

Tactic:
rwa [Nat.one_le_iff_ne_zero]

Premises used: Nat.one_le_iff_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
R : Type u_1
inst : CommSemiring R
c : R
n : ℕ
⊢ homogenize ((C : (a : R) → R[X]) c) n =
    HMul.hMul (α := MvPolynomial (Fin 2) R)
      ((MvPolynomial.C : (a : R) → MvPolynomial (Fin 2) R) c : MvPolynomial (Fin 2) R)
      (HPow.hPow (α := MvPolynomial (Fin 2) R) (MvPolynomial.X 1) n)

Tactic:
simpa [MvPolynomial.C_mul_X_pow_eq_monomial] using homogenize_monomial (Nat.zero_le n) c

Premises used: Nat.zero_le, MvPolynomial.C_mul_X_pow_eq_monomial, Polynomial.homogenize_monomial
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
R : Type u_1
inst : CommSemiring R
n : ℕ
⊢ homogenize 1 n = HPow.hPow (α := MvPolynomial (Fin 2) R) (MvPolynomial.X 1) n

Tactic:
simpa using homogenize_C (1 : R) n

Premises used: Polynomial.homogenize_C, OfNat.ofNat
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
R : Type u_1
inst : CommSemiring R
n : ℕ
m : Fin 2 →₀ ℕ
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:
simp [*, ite_add_ite]

Premises used: ite_add_ite
-- Module: Mathlib.Algebra.Polynomial.Homogenize
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)
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)
⊢ 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

Premises used: le_or_gt
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
R : Type u_1
inst : CommSemiring R
n : ℕ
m : Fin 2 →₀ ℕ
k : ℕ
c : R
hkn : k ≤ n
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
⊢ 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:
rw [homogenize_monomial hkn, coeff_monomial, MvPolynomial.coeff_monomial]

Premises used: Polynomial.coeff_monomial, MvPolynomial.coeff_monomial, Polynomial.homogenize_monomial
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
R : Type u_1
inst : CommSemiring R
n : ℕ
m : Fin 2 →₀ ℕ
k : ℕ
c : R
hkn : k ≤ n
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 : ℕ)
⊢ (fun₀ | 0 => (m : (a : Fin 2) → ℕ) 0 | 1 => (m : (a : Fin 2) → ℕ) 1) = m

Tactic:
ext i
-- Module: Mathlib.Algebra.Polynomial.Homogenize
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, ⋯⟩) : ℕ)
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, ⋯⟩) :
      ℕ)
    ((m : (a : Fin 2) → ℕ) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) : ℕ)
⊢ 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:
fin_cases i
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
R : Type u_1
inst : CommSemiring R
n : ℕ
m : Fin 2 →₀ ℕ
k : ℕ
c : R
hkn : k ≤ n
⊢ 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, ⋯⟩) : ℕ)

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
R : Type u_1
inst : CommSemiring R
n : ℕ
m : Fin 2 →₀ ℕ
k : ℕ
c : R
hkn : k ≤ n
⊢ 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, ⋯⟩) :
      ℕ)
    ((m : (a : Fin 2) → ℕ) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) : ℕ)

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Homogenize
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

Tactic:
have : (fun₀ | 0 => m 0 | 1 => m 1) = m := by ext i; fin_cases i <;> simp
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
R : Type u_1
inst : CommSemiring R
n : ℕ
m : Fin 2 →₀ ℕ
k : ℕ
c : R
hkn : k ≤ n
this : (fun₀ | 0 => (m : (a : Fin 2) → ℕ) 0 | 1 => (m : (a : Fin 2) → ℕ) 1) = m
⊢ (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:
aesop
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
R : Type u_1
inst : CommSemiring R
n : ℕ
m : Fin 2 →₀ ℕ
k : ℕ
c : R
hnk : n < k
⊢ 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:
aesop (add simp homogenize_monomial_of_lt) (add simp coeff_monomial)

Premises used: Polynomial.coeff_monomial, Polynomial.homogenize_monomial_of_lt
-- Module: Mathlib.Algebra.Polynomial.Homogenize
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
monomial :
  ∀ (k : ℕ) (c : R),
    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)
⊢ 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

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)

Premises used: Polynomial.monomial, Polynomial.coeff_monomial, Polynomial.homogenize_monomial_of_lt, MvPolynomial.coeff_monomial, ite_add_ite
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
h : p.homogenize n = 0
a : ∀ (i : ℕ), p.coeff i = coeff 0 i
⊢ p = 0

Tactic:
ext i
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
h : p.homogenize n = 0
i : ℕ
a : p.coeff i = 0
⊢ p.coeff i = coeff 0 i

Tactic:
simp only [coeff_zero]

Premises used: Polynomial.coeff_zero
-- Module: Mathlib.Algebra.Polynomial.Homogenize
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
a₁ : ∀ (H : p.natDegree < i), p.coeff i = 0
⊢ p.coeff i = 0

Tactic:
rcases le_or_gt i p.natDegree with H | H

Premises used: le_or_gt, Polynomial.natDegree
-- Module: Mathlib.Algebra.Polynomial.Homogenize
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 = MvPolynomial.coeff (fun₀ | 0 => i | 1 => n - i) (p.homogenize n)

Tactic:
simp [coeff_homogenize, Nat.add_sub_of_le (H.trans hn)]

Premises used: Nat.add_sub_of_le, Polynomial.coeff_homogenize, LE.le.trans
-- Module: Mathlib.Algebra.Polynomial.Homogenize
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 = 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)]
-- Module: Mathlib.Algebra.Polynomial.Homogenize
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
this : p.coeff i = MvPolynomial.coeff (fun₀ | 0 => i | 1 => n - i) (p.homogenize n)
⊢ p.coeff i = 0

Tactic:
simp [this, h]
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
h : p.homogenize n = 0
i : ℕ
H : p.natDegree < i
⊢ p.coeff i = 0

Tactic:
coeff_eq_zero_of_natDegree_lt H

Premises used: Polynomial.coeff_eq_zero_of_natDegree_lt
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
h : p.homogenize n = 0
i : ℕ
H : p.natDegree < i
⊢ p.coeff i = 0

Tactic:
exact coeff_eq_zero_of_natDegree_lt H

Premises used: Polynomial.coeff_eq_zero_of_natDegree_lt
-- Module: Mathlib.Algebra.Polynomial.Homogenize
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
⊢ p = 0 → p.homogenize n = 0

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
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))
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)
df : p.natDegree ≤ n
⊢ MvPolynomial.eval₂ f g (p.homogenize n) = eval₂ f (g 0) p

Tactic:
apply Polynomial.induction_with_natDegree_le
    (fun p ↦ MvPolynomial.eval₂ f g (p.homogenize n) = p.eval₂ f (g 0)) (N := n)

Premises used: Polynomial.homogenize, MvPolynomial.eval₂, Polynomial.induction_with_natDegree_le, Polynomial.eval₂, OfNat.ofNat, Eq
-- 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
⊢ MvPolynomial.eval₂ f g (homogenize 0 n) = eval₂ f (g 0) 0

Tactic:
simp