awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
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)
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
⊢ ∑ᶠ (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)

Tactic:
rw [finsum_eq_single _ (single () (e 0 + e 1)), mul_comm]

Premises used: Unit.unit, HAdd.hAdd, mul_comm, OfNat.ofNat, DFunLike.coe, finsum_eq_single, Finsupp.single
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
R : Type u_2
inst : CommRing R
f : R⟦X⟧
e : Fin 2 →₀ ℕ
⊢ 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)

Tactic:
simp [MvPolynomial.coeff_add_pow, coeff]

Premises used: PowerSeries.coeff, MvPolynomial.coeff_add_pow
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
R : Type u_2
inst : CommRing R
f : R⟦X⟧
e : Fin 2 →₀ ℕ
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
⊢ ∀ (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:
simp only [MvPolynomial.coeff_add_pow, mem_antidiagonal, cast_ite]

Premises used: Finset.HasAntidiagonal.mem_antidiagonal, Nat.cast_ite, MvPolynomial.coeff_add_pow
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
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) (β := 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:
grind
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
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
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
⊢ (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)

Tactic:
rw [MvPowerSeries.coeff_mul, Finset.sum_eq_single (single 0 (e 0), single 1 (e 1)) ?_ ?_]

Premises used: Prod.mk, Finset.sum_eq_single, OfNat.ofNat, DFunLike.coe, MvPowerSeries.coeff_mul, Finsupp.single
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
R : Type u_2
inst : CommRing R
f : R⟦X⟧
e : Fin 2 →₀ ℕ
⊢ 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:
grind [coeff_subst_single]

Premises used: PowerSeries.coeff_subst_single
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
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))
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
⊢ 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:
by_contra hmul_ne_zero
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
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
⊢ 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⟩

Premises used: ne_zero_and_ne_zero_of_mul
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
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)
⊢ 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⟩

Premises used: ne_zero_and_ne_zero_of_mul
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
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)
⊢ 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

Premises used: PowerSeries.coeff_subst_single, exists_prop, ne_eq, Fin.isValue, ite_eq_right_iff, Classical.not_forall
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
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)
⊢ 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

Premises used: PowerSeries.coeff_subst_single, exists_prop, ne_eq, Fin.isValue, ite_eq_right_iff, Classical.not_forall
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
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)
apply : b = (single 0 ((e : (a : Fin 2) → ℕ) 0), single 1 ((e : (a : Fin 2) → ℕ) 1))
⊢ False

Tactic:
apply hb'
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
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)
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 →₀ ℕ)
⊢ b = (single 0 ((e : (a : Fin 2) → ℕ) 0), single 1 ((e : (a : Fin 2) → ℕ) 1))

Tactic:
rw [Prod.ext_iff, ← mem_antidiagonal.mp hb, h0.1, h1.1]

Premises used: Prod.ext_iff, Finset.HasAntidiagonal.mem_antidiagonal, And.left, Iff.mp
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
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)
⊢ 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:
simp
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
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
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 : ℕ)
⊢ 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:
ext i
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
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, ⋯⟩) : ℕ)
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, ⋯⟩) :
      ℕ)
    ((e : (a : Fin 2) → ℕ) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) : ℕ)
⊢ 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:
fin_cases i
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
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
⊢ 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, ⋯⟩) : ℕ)

Tactic:
simp
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
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
⊢ 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, ⋯⟩) :
      ℕ)
    ((e : (a : Fin 2) → ℕ) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) : ℕ)

Tactic:
simp
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
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

Tactic:
have he' : single 0 (e 0) + single 1 (e 1) = e := by
      ext i
      fin_cases i <;> simp
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
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
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
⊢ 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:
absurd (mem_antidiagonal.mpr he') he

Premises used: Iff.mpr, absurd, Finset.HasAntidiagonal.mem_antidiagonal
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
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
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
⊢ 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:
exact absurd (mem_antidiagonal.mpr he') he

Premises used: Iff.mpr, absurd, Finset.HasAntidiagonal.mem_antidiagonal
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
Goal:
R : Type u_1
inst : Semiring R
m n : ℕ
φ : R⟦X⟧
⊢ Polynomial.coeff (trunc_aux n φ) m = if m < n then (coeff m : (a : R⟦X⟧) → R) φ else 0

Tactic:
simp [trunc_aux, Polynomial.coeff_monomial]

Premises used: Polynomial.coeff_monomial, _private.0.PowerSeries.trunc_aux