awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
Goal:
R : Type u_2
inst : CommRing R
f : R⟦X⟧
e : Fin 2 →₀ ℕ
rw :
  HMul.hMul (β := R)
      (MvPolynomial.coeff e
        (HPow.hPow (β := ℕ) (HAdd.hAdd (α := MvPolynomial (Fin 2) R) (MvPolynomial.X 0) (MvPolynomial.X 1))
          ((single () (HAdd.hAdd (α := ℕ) (β := ℕ) ((e : (a : Fin 2) → ℕ) 0 : ℕ) ((e : (a : Fin 2) → ℕ) 1 : ℕ)) :
                (a : Unit) → ℕ)
              PUnit.unit :
            ℕ)))
      ((MvPowerSeries.coeff
              (single () (HAdd.hAdd (α := ℕ) (β := ℕ) ((e : (a : Fin 2) → ℕ) 0 : ℕ) ((e : (a : Fin 2) → ℕ) 1 : ℕ))) :
            (a : MvPowerSeries Unit R) → R)
          f :
        R) =
    HMul.hMul (α := R) (β := R)
      ((↑((HAdd.hAdd (α := ℕ) (β := ℕ) ((e : (a : Fin 2) → ℕ) 0 : ℕ) ((e : (a : Fin 2) → ℕ) 1 : ℕ)).choose
              ((e : (a : Fin 2) → ℕ) 0)) :
          R) :
        R)
      ((coeff (HAdd.hAdd (α := ℕ) (β := ℕ) ((e : (a : Fin 2) → ℕ) 0 : ℕ) ((e : (a : Fin 2) → ℕ) 1 : ℕ)) :
            (a : R⟦X⟧) → R)
          f :
        R)
⊢ ∑ᶠ (d : Unit →₀ ℕ),
      HMul.hMul (α := R) ((MvPowerSeries.coeff d : (a : MvPowerSeries Unit R) → R) f : R)
        (MvPolynomial.coeff e
          (HPow.hPow (β := ℕ) (HAdd.hAdd (α := MvPolynomial (Fin 2) R) (MvPolynomial.X 0) (MvPolynomial.X 1))
            ((d : (a : Unit) → ℕ) PUnit.unit : ℕ))) =
    HMul.hMul (α := R) (β := R)
      ((↑((HAdd.hAdd (α := ℕ) (β := ℕ) ((e : (a : Fin 2) → ℕ) 0 : ℕ) ((e : (a : Fin 2) → ℕ) 1 : ℕ)).choose
              ((e : (a : Fin 2) → ℕ) 0)) :
          R) :
        R)
      ((coeff (HAdd.hAdd (α := ℕ) (β := ℕ) ((e : (a : Fin 2) → ℕ) 0 : ℕ) ((e : (a : Fin 2) → ℕ) 1 : ℕ)) :
            (a : R⟦X⟧) → R)
          f :
        R)
have rw₁ : ∀ (x : Unit →₀ ℕ),
  x ≠ single () (HAdd.hAdd (α := ℕ) (β := ℕ) ((e : (a : Fin 2) → ℕ) 0 : ℕ) ((e : (a : Fin 2) → ℕ) 1 : ℕ)) →
    HMul.hMul (α := R) ((MvPowerSeries.coeff x : (a : MvPowerSeries Unit R) → R) f : R)
        (MvPolynomial.coeff e
          (HPow.hPow (β := ℕ) (HAdd.hAdd (α := MvPolynomial (Fin 2) R) (MvPolynomial.X 0) (MvPolynomial.X 1))
            ((x : (a : Unit) → ℕ) PUnit.unit : ℕ))) =
      0
Tactic: rw [finsum_eq_single _ (single () (e 0 + e 1)), mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
Goal:
R : Type u_2
inst : CommRing R
f : R⟦X⟧
e : Fin 2 →₀ ℕ
⊢ ∀ (x : Unit →₀ ℕ),
    x ≠ single () (HAdd.hAdd (α := ℕ) (β := ℕ) ((e : (a : Fin 2) → ℕ) 0 : ℕ) ((e : (a : Fin 2) → ℕ) 1 : ℕ)) →
      HMul.hMul (α := R) ((MvPowerSeries.coeff x : (a : MvPowerSeries Unit R) → R) f : R)
          (MvPolynomial.coeff e
            (HPow.hPow (β := ℕ) (HAdd.hAdd (α := MvPolynomial (Fin 2) R) (MvPolynomial.X 0) (MvPolynomial.X 1))
              ((x : (a : Unit) → ℕ) PUnit.unit : ℕ))) =
        0
have simp : ∀ (x : Unit →₀ ℕ),
  x ≠ single () (HAdd.hAdd (α := ℕ) (β := ℕ) ((e : (a : Fin 2) → ℕ) 0 : ℕ) ((e : (a : Fin 2) → ℕ) 1 : ℕ)) →
    HMul.hMul (α := R) (β := R) ((MvPowerSeries.coeff x : (a : MvPowerSeries Unit R) → R) f : R)
        (if
              HAdd.hAdd (α := ℕ) (β := ℕ) ((e : (a : Fin 2) → ℕ) 0 : ℕ) ((e : (a : Fin 2) → ℕ) 1 : ℕ) =
                (x : (a : Unit) → ℕ) PUnit.unit then
            (↑(Nat.choose ((x : (a : Unit) → ℕ) PUnit.unit) ((e : (a : Fin 2) → ℕ) 0)) : R)
          else (↑0 : R) :
          R) =
      0
Tactic: simp only [MvPolynomial.coeff_add_pow, mem_antidiagonal, cast_ite]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
Goal:
R : Type u_2
inst : CommRing R
f : R⟦X⟧
e : Fin 2 →₀ ℕ
⊢ (MvPowerSeries.coeff e : (a : MvPowerSeries (Fin 2) R) → R)
      (HMul.hMul (α := MvPowerSeries (Fin 2) R) (subst X₀ f) (subst X₁ f)) =
    HMul.hMul (α := R) (β := R) ((coeff ((e : (a : Fin 2) → ℕ) 0) : (a : R⟦X⟧) → R) f : R)
      ((coeff ((e : (a : Fin 2) → ℕ) 1) : (a : R⟦X⟧) → R) f : R)
have rw : HMul.hMul (α := R) (β := R)
    ((MvPowerSeries.coeff (single 0 ((e : (a : Fin 2) → ℕ) 0), single 1 ((e : (a : Fin 2) → ℕ) 1)).1 :
          (a : MvPowerSeries (Fin 2) R) → R)
        (subst X₀ f) :
      R)
    ((MvPowerSeries.coeff (single 0 ((e : (a : Fin 2) → ℕ) 0), single 1 ((e : (a : Fin 2) → ℕ) 1)).2 :
          (a : MvPowerSeries (Fin 2) R) → R)
        (subst X₁ f) :
      R) =
  HMul.hMul (α := R) (β := R) ((coeff ((e : (a : Fin 2) → ℕ) 0) : (a : R⟦X⟧) → R) f : R)
    ((coeff ((e : (a : Fin 2) → ℕ) 1) : (a : R⟦X⟧) → R) f : R)
Tactic: rw [MvPowerSeries.coeff_mul, Finset.sum_eq_single (single 0 (e 0), single 1 (e 1)) ?_ ?_]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
Goal:
R : Type u_2
inst : CommRing R
f : R⟦X⟧
e : Fin 2 →₀ ℕ
rw :
  HMul.hMul (α := R) (β := R)
      ((MvPowerSeries.coeff (single 0 ((e : (a : Fin 2) → ℕ) 0), single 1 ((e : (a : Fin 2) → ℕ) 1)).1 :
            (a : MvPowerSeries (Fin 2) R) → R)
          (subst X₀ f) :
        R)
      ((MvPowerSeries.coeff (single 0 ((e : (a : Fin 2) → ℕ) 0), single 1 ((e : (a : Fin 2) → ℕ) 1)).2 :
            (a : MvPowerSeries (Fin 2) R) → R)
          (subst X₁ f) :
        R) =
    HMul.hMul (α := R) (β := R) ((coeff ((e : (a : Fin 2) → ℕ) 0) : (a : R⟦X⟧) → R) f : R)
      ((coeff ((e : (a : Fin 2) → ℕ) 1) : (a : R⟦X⟧) → R) f : R)
⊢ (MvPowerSeries.coeff e : (a : MvPowerSeries (Fin 2) R) → R)
      (HMul.hMul (α := MvPowerSeries (Fin 2) R) (subst X₀ f) (subst X₁ f)) =
    HMul.hMul (α := R) (β := R) ((coeff ((e : (a : Fin 2) → ℕ) 0) : (a : R⟦X⟧) → R) f : R)
      ((coeff ((e : (a : Fin 2) → ℕ) 1) : (a : R⟦X⟧) → R) f : R)
have rw₁ : ∀ b ∈ @antidiagonal _ Finsupp.instAddMonoid _ e,
  b ≠ (single 0 ((e : (a : Fin 2) → ℕ) 0), single 1 ((e : (a : Fin 2) → ℕ) 1)) →
    HMul.hMul (α := R) (β := R) ((MvPowerSeries.coeff b.1 : (a : MvPowerSeries (Fin 2) R) → R) (subst X₀ f) : R)
        ((MvPowerSeries.coeff b.2 : (a : MvPowerSeries (Fin 2) R) → R) (subst X₁ f) : R) =
      0
Tactic: rw [MvPowerSeries.coeff_mul, Finset.sum_eq_single (single 0 (e 0), single 1 (e 1)) ?_ ?_]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
Goal:
R : Type u_2
inst : CommRing R
f : R⟦X⟧
e : Fin 2 →₀ ℕ
rw :
  HMul.hMul (α := R) (β := R)
      ((MvPowerSeries.coeff (single 0 ((e : (a : Fin 2) → ℕ) 0), single 1 ((e : (a : Fin 2) → ℕ) 1)).1 :
            (a : MvPowerSeries (Fin 2) R) → R)
          (subst X₀ f) :
        R)
      ((MvPowerSeries.coeff (single 0 ((e : (a : Fin 2) → ℕ) 0), single 1 ((e : (a : Fin 2) → ℕ) 1)).2 :
            (a : MvPowerSeries (Fin 2) R) → R)
          (subst X₁ f) :
        R) =
    HMul.hMul (α := R) (β := R) ((coeff ((e : (a : Fin 2) → ℕ) 0) : (a : R⟦X⟧) → R) f : R)
      ((coeff ((e : (a : Fin 2) → ℕ) 1) : (a : R⟦X⟧) → R) f : R)
rw₁ :
  ∀ b ∈ @antidiagonal _ Finsupp.instAddMonoid _ e,
    b ≠ (single 0 ((e : (a : Fin 2) → ℕ) 0), single 1 ((e : (a : Fin 2) → ℕ) 1)) →
      HMul.hMul (α := R) (β := R) ((MvPowerSeries.coeff b.1 : (a : MvPowerSeries (Fin 2) R) → R) (subst X₀ f) : R)
          ((MvPowerSeries.coeff b.2 : (a : MvPowerSeries (Fin 2) R) → R) (subst X₁ f) : R) =
        0
⊢ (MvPowerSeries.coeff e : (a : MvPowerSeries (Fin 2) R) → R)
      (HMul.hMul (α := MvPowerSeries (Fin 2) R) (subst X₀ f) (subst X₁ f)) =
    HMul.hMul (α := R) (β := R) ((coeff ((e : (a : Fin 2) → ℕ) 0) : (a : R⟦X⟧) → R) f : R)
      ((coeff ((e : (a : Fin 2) → ℕ) 1) : (a : R⟦X⟧) → R) f : R)
have rw₂ : ((single 0 ((e : (a : Fin 2) → ℕ) 0), single 1 ((e : (a : Fin 2) → ℕ) 1)) : (Fin 2 →₀ ℕ) × (Fin 2 →₀ ℕ)) ∉
    @antidiagonal _ Finsupp.instAddMonoid _ e →
  HMul.hMul (α := R) (β := R)
      ((MvPowerSeries.coeff (single 0 ((e : (a : Fin 2) → ℕ) 0), single 1 ((e : (a : Fin 2) → ℕ) 1)).1 :
            (a : MvPowerSeries (Fin 2) R) → R)
          (subst X₀ f) :
        R)
      ((MvPowerSeries.coeff (single 0 ((e : (a : Fin 2) → ℕ) 0), single 1 ((e : (a : Fin 2) → ℕ) 1)).2 :
            (a : MvPowerSeries (Fin 2) R) → R)
          (subst X₁ f) :
        R) =
    0
Tactic: rw [MvPowerSeries.coeff_mul, Finset.sum_eq_single (single 0 (e 0), single 1 (e 1)) ?_ ?_]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
Goal:
R : Type u_2
inst : CommRing R
f : R⟦X⟧
e : Fin 2 →₀ ℕ
b : (Fin 2 →₀ ℕ) × (Fin 2 →₀ ℕ)
hb : b ∈ @antidiagonal _ Finsupp.instAddMonoid _ e
hb' : b ≠ (single 0 ((e : (a : Fin 2) → ℕ) 0), single 1 ((e : (a : Fin 2) → ℕ) 1))
⊢ HMul.hMul (α := R) (β := R) ((MvPowerSeries.coeff b.1 : (a : MvPowerSeries (Fin 2) R) → R) (subst X₀ f) : R)
      ((MvPowerSeries.coeff b.2 : (a : MvPowerSeries (Fin 2) R) → R) (subst X₁ f) : R) =
    0
have by_contra : ∀
  (hmul_ne_zero :
    ¬HMul.hMul (α := R) (β := R) ((MvPowerSeries.coeff b.1 : (a : MvPowerSeries (Fin 2) R) → R) (subst X₀ f) : R)
          ((MvPowerSeries.coeff b.2 : (a : MvPowerSeries (Fin 2) R) → R) (subst X₁ f) : R) =
        0),
  False
Tactic: by_contra hmul_ne_zero
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (hypothesis)
Goal:
R : Type u_2
inst : CommRing R
f : R⟦X⟧
e : Fin 2 →₀ ℕ
b : (Fin 2 →₀ ℕ) × (Fin 2 →₀ ℕ)
hb : b ∈ @antidiagonal _ Finsupp.instAddMonoid _ e
hb' : b ≠ (single 0 ((e : (a : Fin 2) → ℕ) 0), single 1 ((e : (a : Fin 2) → ℕ) 1))
hmul_ne_zero :
  ¬HMul.hMul (α := R) (β := R) ((MvPowerSeries.coeff b.1 : (a : MvPowerSeries (Fin 2) R) → R) (subst X₀ f) : R)
        ((MvPowerSeries.coeff b.2 : (a : MvPowerSeries (Fin 2) R) → R) (subst X₁ f) : R) =
      0
⊢ False
have h0 : Ne (α := R) ((MvPowerSeries.coeff b.1 : (a : MvPowerSeries (Fin 2) R) → R) (subst X₀ f) : R) (0 : R)
Tactic: rcases ne_zero_and_ne_zero_of_mul hmul_ne_zero with ⟨h0, h1⟩
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (hypothesis)
Goal:
R : Type u_2
inst : CommRing R
f : R⟦X⟧
e : Fin 2 →₀ ℕ
b : (Fin 2 →₀ ℕ) × (Fin 2 →₀ ℕ)
hb : b ∈ @antidiagonal _ Finsupp.instAddMonoid _ e
hb' : b ≠ (single 0 ((e : (a : Fin 2) → ℕ) 0), single 1 ((e : (a : Fin 2) → ℕ) 1))
hmul_ne_zero :
  ¬HMul.hMul (α := R) (β := R) ((MvPowerSeries.coeff b.1 : (a : MvPowerSeries (Fin 2) R) → R) (subst X₀ f) : R)
        ((MvPowerSeries.coeff b.2 : (a : MvPowerSeries (Fin 2) R) → R) (subst X₁ f) : R) =
      0
h0 : Ne (α := R) ((MvPowerSeries.coeff b.1 : (a : MvPowerSeries (Fin 2) R) → R) (subst X₀ f) : R) (0 : R)
⊢ False
have h1 : Ne (α := R) ((MvPowerSeries.coeff b.2 : (a : MvPowerSeries (Fin 2) R) → R) (subst X₁ f) : R) (0 : R)
Tactic: rcases ne_zero_and_ne_zero_of_mul hmul_ne_zero with ⟨h0, h1⟩
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (hypothesis)
Goal:
R : Type u_2
inst : CommRing R
f : R⟦X⟧
e : Fin 2 →₀ ℕ
b : (Fin 2 →₀ ℕ) × (Fin 2 →₀ ℕ)
hb : b ∈ @antidiagonal _ Finsupp.instAddMonoid _ e
hb' : b ≠ (single 0 ((e : (a : Fin 2) → ℕ) 0), single 1 ((e : (a : Fin 2) → ℕ) 1))
hmul_ne_zero :
  ¬HMul.hMul (α := R) (β := R) ((MvPowerSeries.coeff b.1 : (a : MvPowerSeries (Fin 2) R) → R) (subst X₀ f) : R)
        ((MvPowerSeries.coeff b.2 : (a : MvPowerSeries (Fin 2) R) → R) (subst X₁ f) : R) =
      0
h0 : Ne (α := R) ((MvPowerSeries.coeff b.1 : (a : MvPowerSeries (Fin 2) R) → R) (subst X₀ f) : R) (0 : R)
h1 : Ne (α := R) ((MvPowerSeries.coeff b.2 : (a : MvPowerSeries (Fin 2) R) → R) (subst X₁ f) : R) (0 : R)
⊢ False
have h0₁ : b.1 = single 0 ((b.1 : (a : Fin 2) → ℕ) 0) ∧
  ¬Eq (α := R) ((coeff ((b.1 : (a : Fin 2) → ℕ) 0) : (a : R⟦X⟧) → R) f : R) (0 : R)
Tactic: simp only [Fin.isValue, coeff_subst_single, ne_eq, ite_eq_right_iff,
      not_forall, exists_prop] at h0 h1
Cleared hypotheses: h0, h1
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (hypothesis)
Goal:
R : Type u_2
inst : CommRing R
f : R⟦X⟧
e : Fin 2 →₀ ℕ
b : (Fin 2 →₀ ℕ) × (Fin 2 →₀ ℕ)
hb : b ∈ @antidiagonal _ Finsupp.instAddMonoid _ e
hb' : b ≠ (single 0 ((e : (a : Fin 2) → ℕ) 0), single 1 ((e : (a : Fin 2) → ℕ) 1))
hmul_ne_zero :
  ¬HMul.hMul (α := R) (β := R) ((MvPowerSeries.coeff b.1 : (a : MvPowerSeries (Fin 2) R) → R) (subst X₀ f) : R)
        ((MvPowerSeries.coeff b.2 : (a : MvPowerSeries (Fin 2) R) → R) (subst X₁ f) : R) =
      0
h0 : Ne (α := R) ((MvPowerSeries.coeff b.1 : (a : MvPowerSeries (Fin 2) R) → R) (subst X₀ f) : R) (0 : R)
h1 : Ne (α := R) ((MvPowerSeries.coeff b.2 : (a : MvPowerSeries (Fin 2) R) → R) (subst X₁ f) : R) (0 : R)
h0₁ :
  b.1 = single 0 ((b.1 : (a : Fin 2) → ℕ) 0) ∧
    ¬Eq (α := R) ((coeff ((b.1 : (a : Fin 2) → ℕ) 0) : (a : R⟦X⟧) → R) f : R) (0 : R)
⊢ False
have h1₁ : b.2 = single 1 ((b.2 : (a : Fin 2) → ℕ) 1) ∧
  ¬Eq (α := R) ((coeff ((b.2 : (a : Fin 2) → ℕ) 1) : (a : R⟦X⟧) → R) f : R) (0 : R)
Tactic: simp only [Fin.isValue, coeff_subst_single, ne_eq, ite_eq_right_iff,
      not_forall, exists_prop] at h0 h1
Cleared hypotheses: h0, h1
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
Goal:
R : Type u_2
inst : CommRing R
f : R⟦X⟧
e : Fin 2 →₀ ℕ
b : (Fin 2 →₀ ℕ) × (Fin 2 →₀ ℕ)
hb : b ∈ @antidiagonal _ Finsupp.instAddMonoid _ e
hb' : b ≠ (single 0 ((e : (a : Fin 2) → ℕ) 0), single 1 ((e : (a : Fin 2) → ℕ) 1))
hmul_ne_zero :
  ¬HMul.hMul (α := R) (β := R) ((MvPowerSeries.coeff b.1 : (a : MvPowerSeries (Fin 2) R) → R) (subst X₀ f) : R)
        ((MvPowerSeries.coeff b.2 : (a : MvPowerSeries (Fin 2) R) → R) (subst X₁ f) : R) =
      0
h0 :
  b.1 = single 0 ((b.1 : (a : Fin 2) → ℕ) 0) ∧
    ¬Eq (α := R) ((coeff ((b.1 : (a : Fin 2) → ℕ) 0) : (a : R⟦X⟧) → R) f : R) (0 : R)
h1 :
  b.2 = single 1 ((b.2 : (a : Fin 2) → ℕ) 1) ∧
    ¬Eq (α := R) ((coeff ((b.2 : (a : Fin 2) → ℕ) 1) : (a : R⟦X⟧) → R) f : R) (0 : R)
⊢ False
have apply : b = (single 0 ((e : (a : Fin 2) → ℕ) 0), single 1 ((e : (a : Fin 2) → ℕ) 1))
Tactic: apply hb'
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
Goal:
R : Type u_2
inst : CommRing R
f : R⟦X⟧
e : Fin 2 →₀ ℕ
b : (Fin 2 →₀ ℕ) × (Fin 2 →₀ ℕ)
hb : b ∈ @antidiagonal _ Finsupp.instAddMonoid _ e
hb' : b ≠ (single 0 ((e : (a : Fin 2) → ℕ) 0), single 1 ((e : (a : Fin 2) → ℕ) 1))
hmul_ne_zero :
  ¬HMul.hMul (α := R) (β := R) ((MvPowerSeries.coeff b.1 : (a : MvPowerSeries (Fin 2) R) → R) (subst X₀ f) : R)
        ((MvPowerSeries.coeff b.2 : (a : MvPowerSeries (Fin 2) R) → R) (subst X₁ f) : R) =
      0
h0 :
  b.1 = single 0 ((b.1 : (a : Fin 2) → ℕ) 0) ∧
    ¬Eq (α := R) ((coeff ((b.1 : (a : Fin 2) → ℕ) 0) : (a : R⟦X⟧) → R) f : R) (0 : R)
h1 :
  b.2 = single 1 ((b.2 : (a : Fin 2) → ℕ) 1) ∧
    ¬Eq (α := R) ((coeff ((b.2 : (a : Fin 2) → ℕ) 1) : (a : R⟦X⟧) → R) f : R) (0 : R)
⊢ b = (single 0 ((e : (a : Fin 2) → ℕ) 0), single 1 ((e : (a : Fin 2) → ℕ) 1))
have rw : Eq (α := Fin 2 →₀ ℕ) (single 0 ((b.1 : (a : Fin 2) → ℕ) 0) : Fin 2 →₀ ℕ)
    ((single 0
            ((HAdd.hAdd (α := Fin 2 →₀ ℕ) (β := Fin 2 →₀ ℕ) (single 0 ((b.1 : (a : Fin 2) → ℕ) 0) : Fin 2 →₀ ℕ)
                  (single 1 ((b.2 : (a : Fin 2) → ℕ) 1) : Fin 2 →₀ ℕ) :
                (a : Fin 2) → ℕ)
              0),
          single 1
            ((HAdd.hAdd (α := Fin 2 →₀ ℕ) (β := Fin 2 →₀ ℕ) (single 0 ((b.1 : (a : Fin 2) → ℕ) 0) : Fin 2 →₀ ℕ)
                  (single 1 ((b.2 : (a : Fin 2) → ℕ) 1) : Fin 2 →₀ ℕ) :
                (a : Fin 2) → ℕ)
              1)).1 :
      Fin 2 →₀ ℕ) ∧
  Eq (α := Fin 2 →₀ ℕ) (single 1 ((b.2 : (a : Fin 2) → ℕ) 1) : Fin 2 →₀ ℕ)
    ((single 0
            ((HAdd.hAdd (α := Fin 2 →₀ ℕ) (β := Fin 2 →₀ ℕ) (single 0 ((b.1 : (a : Fin 2) → ℕ) 0) : Fin 2 →₀ ℕ)
                  (single 1 ((b.2 : (a : Fin 2) → ℕ) 1) : Fin 2 →₀ ℕ) :
                (a : Fin 2) → ℕ)
              0),
          single 1
            ((HAdd.hAdd (α := Fin 2 →₀ ℕ) (β := Fin 2 →₀ ℕ) (single 0 ((b.1 : (a : Fin 2) → ℕ) 0) : Fin 2 →₀ ℕ)
                  (single 1 ((b.2 : (a : Fin 2) → ℕ) 1) : Fin 2 →₀ ℕ) :
                (a : Fin 2) → ℕ)
              1)).2 :
      Fin 2 →₀ ℕ)
Tactic: rw [Prod.ext_iff, ← mem_antidiagonal.mp hb, h0.1, h1.1]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
Goal:
R : Type u_2
inst : CommRing R
f : R⟦X⟧
e : Fin 2 →₀ ℕ
he :
  ((single 0 ((e : (a : Fin 2) → ℕ) 0), single 1 ((e : (a : Fin 2) → ℕ) 1)) : (Fin 2 →₀ ℕ) × (Fin 2 →₀ ℕ)) ∉
    @antidiagonal _ Finsupp.instAddMonoid _ e
⊢ HAdd.hAdd (α := Fin 2 →₀ ℕ) (β := Fin 2 →₀ ℕ) (single 0 ((e : (a : Fin 2) → ℕ) 0) : Fin 2 →₀ ℕ)
      (single 1 ((e : (a : Fin 2) → ℕ) 1) : Fin 2 →₀ ℕ) =
    e
have h : ∀ (i : Fin 2),
  Eq (α := ℕ)
    ((HAdd.hAdd (α := Fin 2 →₀ ℕ) (β := Fin 2 →₀ ℕ) (single 0 ((e : (a : Fin 2) → ℕ) 0) : Fin 2 →₀ ℕ)
            (single 1 ((e : (a : Fin 2) → ℕ) 1) : Fin 2 →₀ ℕ) :
          (a : Fin 2) → ℕ)
        i :
      ℕ)
    ((e : (a : Fin 2) → ℕ) i : ℕ)
Tactic: ext i
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
Goal:
R : Type u_2
inst : CommRing R
f : R⟦X⟧
e : Fin 2 →₀ ℕ
he :
  ((single 0 ((e : (a : Fin 2) → ℕ) 0), single 1 ((e : (a : Fin 2) → ℕ) 1)) : (Fin 2 →₀ ℕ) × (Fin 2 →₀ ℕ)) ∉
    @antidiagonal _ Finsupp.instAddMonoid _ e
i : Fin 2
⊢ Eq (α := ℕ)
    ((HAdd.hAdd (α := Fin 2 →₀ ℕ) (β := Fin 2 →₀ ℕ) (single 0 ((e : (a : Fin 2) → ℕ) 0) : Fin 2 →₀ ℕ)
            (single 1 ((e : (a : Fin 2) → ℕ) 1) : Fin 2 →₀ ℕ) :
          (a : Fin 2) → ℕ)
        i :
      ℕ)
    ((e : (a : Fin 2) → ℕ) i : ℕ)
have h : Eq (α := ℕ)
  ((HAdd.hAdd (α := Fin 2 →₀ ℕ) (β := Fin 2 →₀ ℕ) (single 0 ((e : (a : Fin 2) → ℕ) 0) : Fin 2 →₀ ℕ)
          (single 1 ((e : (a : Fin 2) → ℕ) 1) : Fin 2 →₀ ℕ) :
        (a : Fin 2) → ℕ)
      ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) :
    ℕ)
  ((e : (a : Fin 2) → ℕ) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) : ℕ)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
Goal:
R : Type u_2
inst : CommRing R
f : R⟦X⟧
e : Fin 2 →₀ ℕ
he :
  ((single 0 ((e : (a : Fin 2) → ℕ) 0), single 1 ((e : (a : Fin 2) → ℕ) 1)) : (Fin 2 →₀ ℕ) × (Fin 2 →₀ ℕ)) ∉
    @antidiagonal _ Finsupp.instAddMonoid _ e
i : Fin 2
h :
  Eq (α := ℕ)
    ((HAdd.hAdd (α := Fin 2 →₀ ℕ) (β := Fin 2 →₀ ℕ) (single 0 ((e : (a : Fin 2) → ℕ) 0) : Fin 2 →₀ ℕ)
            (single 1 ((e : (a : Fin 2) → ℕ) 1) : Fin 2 →₀ ℕ) :
          (a : Fin 2) → ℕ)
        ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) :
      ℕ)
    ((e : (a : Fin 2) → ℕ) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) : ℕ)
⊢ Eq (α := ℕ)
    ((HAdd.hAdd (α := Fin 2 →₀ ℕ) (β := Fin 2 →₀ ℕ) (single 0 ((e : (a : Fin 2) → ℕ) 0) : Fin 2 →₀ ℕ)
            (single 1 ((e : (a : Fin 2) → ℕ) 1) : Fin 2 →₀ ℕ) :
          (a : Fin 2) → ℕ)
        i :
      ℕ)
    ((e : (a : Fin 2) → ℕ) i : ℕ)
have h₁ : Eq (α := ℕ)
  ((HAdd.hAdd (α := Fin 2 →₀ ℕ) (β := Fin 2 →₀ ℕ) (single 0 ((e : (a : Fin 2) → ℕ) 0) : Fin 2 →₀ ℕ)
          (single 1 ((e : (a : Fin 2) → ℕ) 1) : Fin 2 →₀ ℕ) :
        (a : Fin 2) → ℕ)
      ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) :
    ℕ)
  ((e : (a : Fin 2) → ℕ) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) : ℕ)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (hypothesis)
Goal:
R : Type u_2
inst : CommRing R
f : R⟦X⟧
e : Fin 2 →₀ ℕ
he :
  ((single 0 ((e : (a : Fin 2) → ℕ) 0), single 1 ((e : (a : Fin 2) → ℕ) 1)) : (Fin 2 →₀ ℕ) × (Fin 2 →₀ ℕ)) ∉
    @antidiagonal _ Finsupp.instAddMonoid _ e
⊢ HMul.hMul (α := R) (β := R)
      ((MvPowerSeries.coeff (single 0 ((e : (a : Fin 2) → ℕ) 0), single 1 ((e : (a : Fin 2) → ℕ) 1)).1 :
            (a : MvPowerSeries (Fin 2) R) → R)
          (subst X₀ f) :
        R)
      ((MvPowerSeries.coeff (single 0 ((e : (a : Fin 2) → ℕ) 0), single 1 ((e : (a : Fin 2) → ℕ) 1)).2 :
            (a : MvPowerSeries (Fin 2) R) → R)
          (subst X₁ f) :
        R) =
    0
have he' : HAdd.hAdd (α := Fin 2 →₀ ℕ) (β := Fin 2 →₀ ℕ) (single 0 ((e : (a : Fin 2) → ℕ) 0) : Fin 2 →₀ ℕ)
    (single 1 ((e : (a : Fin 2) → ℕ) 1) : Fin 2 →₀ ℕ) =
  e
Tactic: have he' : single 0 (e 0) + single 1 (e 1) = e := by
      ext i
      fin_cases i <;> simp
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
φ ψ : R⟦X⟧
m : ℕ
⊢ Polynomial.coeff (trunc_aux n (φ + ψ)) m = (HAdd.hAdd (α := R[X]) (trunc_aux n φ) (trunc_aux n ψ)).coeff m
have simp : (if m < n then (coeff m : (a : R⟦X⟧) → R) (φ + ψ) else 0) =
  HAdd.hAdd (α := R) (β := R) (if m < n then (coeff m : (a : R⟦X⟧) → R) φ else 0 : R)
    (if m < n then (coeff m : (a : R⟦X⟧) → R) ψ else 0 : R)
Tactic: simp only [coeff_trunc_aux, Polynomial.coeff_add]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
φ ψ : R⟦X⟧
m : ℕ
⊢ (if m < n then (coeff m : (a : R⟦X⟧) → R) (φ + ψ) else 0) =
    HAdd.hAdd (α := R) (β := R) (if m < n then (coeff m : (a : R⟦X⟧) → R) φ else 0 : R)
      (if m < n then (coeff m : (a : R⟦X⟧) → R) ψ else 0 : R)
have pos : ∀ (H : m < n),
  (coeff m : (a : R⟦X⟧) → R) (φ + ψ) =
    HAdd.hAdd (α := R) (β := R) ((coeff m : (a : R⟦X⟧) → R) φ : R) ((coeff m : (a : R⟦X⟧) → R) ψ : R)
Tactic: split_ifs with H
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
φ ψ : R⟦X⟧
m : ℕ
pos :
  ∀ (H : m < n),
    (coeff m : (a : R⟦X⟧) → R) (φ + ψ) =
      HAdd.hAdd (α := R) (β := R) ((coeff m : (a : R⟦X⟧) → R) φ : R) ((coeff m : (a : R⟦X⟧) → R) ψ : R)
⊢ (if m < n then (coeff m : (a : R⟦X⟧) → R) (φ + ψ) else 0) =
    HAdd.hAdd (α := R) (β := R) (if m < n then (coeff m : (a : R⟦X⟧) → R) φ else 0 : R)
      (if m < n then (coeff m : (a : R⟦X⟧) → R) ψ else 0 : R)
have neg : ∀ (H : ¬m < n), 0 = HAdd.hAdd (α := R) 0 0
Tactic: split_ifs with H
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
φ ψ : R⟦X⟧
m : ℕ
H : ¬m < n
⊢ 0 = HAdd.hAdd (α := R) 0 0
have neg : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [zero_add]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
t : R
φ : R⟦X⟧
⊢ trunc_aux n (t • φ) = HSMul.hSMul (α := R) (β := R[X]) ((RingHom.id R : (a : R) → R) t : R) (trunc_aux n φ)
have a : ∀ (n_1 : ℕ),
  Polynomial.coeff (trunc_aux n (t • φ)) n_1 =
    (HSMul.hSMul (α := R) (β := R[X]) ((RingHom.id R : (a : R) → R) t : R) (trunc_aux n φ)).coeff n_1
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
a : R
m : ℕ
⊢ Eq.{u_1 + 1} (α := R) (Polynomial.coeff ((trunc (n + 1) : (a : R⟦X⟧) → R[X]) ((C : (a : R) → R⟦X⟧) a)) m)
    (Polynomial.coeff ((Polynomial.C : (a : R) → R[X]) a) m)
have rw : (if m < n + 1 then if m = 0 then a else 0 else 0) = if m = 0 then a else 0
Tactic: rw [coeff_trunc, coeff_C, Polynomial.coeff_C]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
a : R
m : ℕ
⊢ (if m < n + 1 then if m = 0 then a else 0 else 0) = if m = 0 then a else 0
have pos : ∀ (H : m < n + 1), m = 0 → a = a
Tactic: split_ifs with H
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
a : R
m : ℕ
pos : ∀ (H : m < n + 1), m = 0 → a = a
⊢ (if m < n + 1 then if m = 0 then a else 0 else 0) = if m = 0 then a else 0
have neg : ∀ (H : m < n + 1), ¬m = 0 → Eq.{u_1 + 1} (α := R) 0 0
Tactic: split_ifs with H
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
a : R
m : ℕ
pos : ∀ (H : m < n + 1), m = 0 → a = a
neg : ∀ (H : m < n + 1), ¬m = 0 → Eq.{u_1 + 1} (α := R) 0 0
⊢ (if m < n + 1 then if m = 0 then a else 0 else 0) = if m = 0 then a else 0
have pos₁ : ∀ (H : ¬m < n + 1), m = 0 → 0 = a
Tactic: split_ifs with H
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
a : R
m : ℕ
pos : ∀ (H : m < n + 1), m = 0 → a = a
neg : ∀ (H : m < n + 1), ¬m = 0 → Eq.{u_1 + 1} (α := R) 0 0
pos₁ : ∀ (H : ¬m < n + 1), m = 0 → 0 = a
⊢ (if m < n + 1 then if m = 0 then a else 0 else 0) = if m = 0 then a else 0
have neg₁ : ∀ (H : ¬m < n + 1), ¬m = 0 → Eq.{u_1 + 1} (α := R) 0 0
Tactic: split_ifs with H
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R⟦X⟧
n : ℕ
⊢ (trunc n.succ : (a : R⟦X⟧) → R[X]) f =
    HAdd.hAdd (α := R[X]) (β := R[X]) ((trunc n : (a : R⟦X⟧) → R[X]) f : R[X])
      ((Polynomial.monomial n : (a : R) → R[X]) ((coeff n : (a : R⟦X⟧) → R) f) : R[X])
have rw : ∑ m ∈ Ico 0 n.succ, (Polynomial.monomial m : (a : R) → R[X]) ((coeff m : (a : R⟦X⟧) → R) f) =
  HAdd.hAdd (α := R[X]) (β := R[X]) ((trunc n : (a : R⟦X⟧) → R[X]) f : R[X])
    ((Polynomial.monomial n : (a : R) → R[X]) ((coeff n : (a : R⟦X⟧) → R) f) : R[X])
Tactic: rw [trunc_apply, Ico_zero_eq_range, sum_range_succ, trunc_apply, Ico_zero_eq_range]