Theorem: PowerSeries.isExponential_add_mul_iff (DividedPowers/ExponentialModule/Basic.lean)

State before:
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
he :
  ∀ (e : Fin 2 →₀ ℕ),
    (MvPowerSeries.coeff R e) (subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f) =
      ↑((e 0 + e 1).choose (e 0)) * (coeff R (e 0 + e 1)) f
he' :
  ∀ (e : Fin 2 →₀ ℕ),
    (MvPowerSeries.coeff R e) (subst (MvPowerSeries.X 0) f * subst (MvPowerSeries.X 1) f) =
      (coeff R (e 0)) f * (coeff R (e 1)) f
⊢ subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f = subst (MvPowerSeries.X 0) f * subst (MvPowerSeries.X 1) f ↔
    ∀ (p q : ℕ), ↑((p + q).choose p) * (coeff R (p + q)) f = (coeff R p) f * (coeff R q) f
Tactic:
rw [MvPowerSeries.ext_iff]
State after:
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
he :
  ∀ (e : Fin 2 →₀ ℕ),
    (MvPowerSeries.coeff R e) (subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f) =
      ↑((e 0 + e 1).choose (e 0)) * (coeff R (e 0 + e 1)) f
he' :
  ∀ (e : Fin 2 →₀ ℕ),
    (MvPowerSeries.coeff R e) (subst (MvPowerSeries.X 0) f * subst (MvPowerSeries.X 1) f) =
      (coeff R (e 0)) f * (coeff R (e 1)) f
⊢ (∀ (n : Fin 2 →₀ ℕ),
      (MvPowerSeries.coeff R n) (subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f) =
        (MvPowerSeries.coeff R n) (subst (MvPowerSeries.X 0) f * subst (MvPowerSeries.X 1) f)) ↔
    ∀ (p q : ℕ), ↑((p + q).choose p) * (coeff R (p + q)) f = (coeff R p) f * (coeff R q) f

State before:
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
he :
  ∀ (e : Fin 2 →₀ ℕ),
    (MvPowerSeries.coeff R e) (subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f) =
      ↑((e 0 + e 1).choose (e 0)) * (coeff R (e 0 + e 1)) f
he' :
  ∀ (e : Fin 2 →₀ ℕ),
    (MvPowerSeries.coeff R e) (subst (MvPowerSeries.X 0) f * subst (MvPowerSeries.X 1) f) =
      (coeff R (e 0)) f * (coeff R (e 1)) f
⊢ (∀ (n : Fin 2 →₀ ℕ),
      (MvPowerSeries.coeff R n) (subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f) =
        (MvPowerSeries.coeff R n) (subst (MvPowerSeries.X 0) f * subst (MvPowerSeries.X 1) f)) ↔
    ∀ (p q : ℕ), ↑((p + q).choose p) * (coeff R (p + q)) f = (coeff R p) f * (coeff R q) f
Tactic:
convert forall_congr_curry₀ _
State after:
case convert_5
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
he :
  ∀ (e : Fin 2 →₀ ℕ),
    (MvPowerSeries.coeff R e) (subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f) =
      ↑((e 0 + e 1).choose (e 0)) * (coeff R (e 0 + e 1)) f
he' :
  ∀ (e : Fin 2 →₀ ℕ),
    (MvPowerSeries.coeff R e) (subst (MvPowerSeries.X 0) f * subst (MvPowerSeries.X 1) f) =
      (coeff R (e 0)) f * (coeff R (e 1)) f
⊢ ∀ (e : Fin 2 →₀ ℕ),
    (MvPowerSeries.coeff R e) (subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f) =
        (MvPowerSeries.coeff R e) (subst (MvPowerSeries.X 0) f * subst (MvPowerSeries.X 1) f) ↔
      ↑((e 0 + e 1).choose (e 0)) * (coeff R (e 0 + e 1)) f = (coeff R (e 0)) f * (coeff R (e 1)) f

State before:
case convert_5
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
he :
  ∀ (e : Fin 2 →₀ ℕ),
    (MvPowerSeries.coeff R e) (subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f) =
      ↑((e 0 + e 1).choose (e 0)) * (coeff R (e 0 + e 1)) f
he' :
  ∀ (e : Fin 2 →₀ ℕ),
    (MvPowerSeries.coeff R e) (subst (MvPowerSeries.X 0) f * subst (MvPowerSeries.X 1) f) =
      (coeff R (e 0)) f * (coeff R (e 1)) f
⊢ ∀ (e : Fin 2 →₀ ℕ),
    (MvPowerSeries.coeff R e) (subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f) =
        (MvPowerSeries.coeff R e) (subst (MvPowerSeries.X 0) f * subst (MvPowerSeries.X 1) f) ↔
      ↑((e 0 + e 1).choose (e 0)) * (coeff R (e 0 + e 1)) f = (coeff R (e 0)) f * (coeff R (e 1)) f
Tactic:
intro e
State after:
case convert_5
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
he :
  ∀ (e : Fin 2 →₀ ℕ),
    (MvPowerSeries.coeff R e) (subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f) =
      ↑((e 0 + e 1).choose (e 0)) * (coeff R (e 0 + e 1)) f
he' :
  ∀ (e : Fin 2 →₀ ℕ),
    (MvPowerSeries.coeff R e) (subst (MvPowerSeries.X 0) f * subst (MvPowerSeries.X 1) f) =
      (coeff R (e 0)) f * (coeff R (e 1)) f
e : Fin 2 →₀ ℕ
⊢ (MvPowerSeries.coeff R e) (subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f) =
      (MvPowerSeries.coeff R e) (subst (MvPowerSeries.X 0) f * subst (MvPowerSeries.X 1) f) ↔
    ↑((e 0 + e 1).choose (e 0)) * (coeff R (e 0 + e 1)) f = (coeff R (e 0)) f * (coeff R (e 1)) f

State before:
case convert_5
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
he :
  ∀ (e : Fin 2 →₀ ℕ),
    (MvPowerSeries.coeff R e) (subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f) =
      ↑((e 0 + e 1).choose (e 0)) * (coeff R (e 0 + e 1)) f
he' :
  ∀ (e : Fin 2 →₀ ℕ),
    (MvPowerSeries.coeff R e) (subst (MvPowerSeries.X 0) f * subst (MvPowerSeries.X 1) f) =
      (coeff R (e 0)) f * (coeff R (e 1)) f
e : Fin 2 →₀ ℕ
⊢ (MvPowerSeries.coeff R e) (subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f) =
      (MvPowerSeries.coeff R e) (subst (MvPowerSeries.X 0) f * subst (MvPowerSeries.X 1) f) ↔
    ↑((e 0 + e 1).choose (e 0)) * (coeff R (e 0 + e 1)) f = (coeff R (e 0)) f * (coeff R (e 1)) f
Tactic:
rw [he, he']
State after:
no goals

State before:
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
⊢ ∀ (e : Fin 2 →₀ ℕ),
    (MvPowerSeries.coeff R e) (subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f) =
      ↑((e 0 + e 1).choose (e 0)) * (coeff R (e 0 + e 1)) f
Tactic:
intro e
State after:
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
e : Fin 2 →₀ ℕ
⊢ (MvPowerSeries.coeff R e) (subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f) =
    ↑((e 0 + e 1).choose (e 0)) * (coeff R (e 0 + e 1)) f

State before:
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
e : Fin 2 →₀ ℕ
⊢ (MvPowerSeries.coeff R e) (subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f) =
    ↑((e 0 + e 1).choose (e 0)) * (coeff R (e 0 + e 1)) f
Tactic:
rw [PowerSeries.subst, MvPowerSeries.coeff_subst _]
State after:
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
e : Fin 2 →₀ ℕ
⊢ ∑ᶠ (d : Unit →₀ ℕ),
      (MvPowerSeries.coeff R d) f •
        (MvPowerSeries.coeff R e) (d.prod fun s e => (MvPowerSeries.X 0 + MvPowerSeries.X 1) ^ e) =
    ↑((e 0 + e 1).choose (e 0)) * (coeff R (e 0 + e 1)) f

A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
e : Fin 2 →₀ ℕ
⊢ MvPowerSeries.SubstDomain fun x => MvPowerSeries.X 0 + MvPowerSeries.X 1

State before:
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
e : Fin 2 →₀ ℕ
⊢ ∑ᶠ (d : Unit →₀ ℕ),
      (MvPowerSeries.coeff R d) f •
        (MvPowerSeries.coeff R e) (d.prod fun s e => (MvPowerSeries.X 0 + MvPowerSeries.X 1) ^ e) =
    ↑((e 0 + e 1).choose (e 0)) * (coeff R (e 0 + e 1)) f

A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
e : Fin 2 →₀ ℕ
⊢ MvPowerSeries.SubstDomain fun x => MvPowerSeries.X 0 + MvPowerSeries.X 1
Tactic:
simp only [Fin.isValue, Finsupp.prod_pow, Finset.univ_unique,
  PUnit.default_eq_unit, Finset.prod_singleton, smul_eq_mul]
State after:
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
e : Fin 2 →₀ ℕ
⊢ ∑ᶠ (d : Unit →₀ ℕ),
      (MvPowerSeries.coeff R d) f * (MvPowerSeries.coeff R e) ((MvPowerSeries.X 0 + MvPowerSeries.X 1) ^ d PUnit.unit) =
    ↑((e 0 + e 1).choose (e 0)) * (coeff R (e 0 + e 1)) f

A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
e : Fin 2 →₀ ℕ
⊢ MvPowerSeries.SubstDomain fun x => MvPowerSeries.X 0 + MvPowerSeries.X 1

State before:
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
e : Fin 2 →₀ ℕ
⊢ ∑ᶠ (d : Unit →₀ ℕ),
      (MvPowerSeries.coeff R d) f * (MvPowerSeries.coeff R e) ((MvPowerSeries.X 0 + MvPowerSeries.X 1) ^ d PUnit.unit) =
    ↑((e 0 + e 1).choose (e 0)) * (coeff R (e 0 + e 1)) f

A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
e : Fin 2 →₀ ℕ
⊢ MvPowerSeries.SubstDomain fun x => MvPowerSeries.X 0 + MvPowerSeries.X 1
Tactic:
simp only [← MvPolynomial.coe_X, ← MvPolynomial.coe_add, ← MvPolynomial.coe_pow, MvPolynomial.coeff_coe]
State after:
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
e : Fin 2 →₀ ℕ
⊢ ∑ᶠ (d : Unit →₀ ℕ),
      (MvPowerSeries.coeff R d) f * MvPolynomial.coeff e ((MvPolynomial.X 0 + MvPolynomial.X 1) ^ d PUnit.unit) =
    ↑((e 0 + e 1).choose (e 0)) * (coeff R (e 0 + e 1)) f

A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
e : Fin 2 →₀ ℕ
⊢ MvPowerSeries.SubstDomain fun x => MvPowerSeries.X 0 + MvPowerSeries.X 1

State before:
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
e : Fin 2 →₀ ℕ
⊢ ∑ᶠ (d : Unit →₀ ℕ),
      (MvPowerSeries.coeff R d) f * MvPolynomial.coeff e ((MvPolynomial.X 0 + MvPolynomial.X 1) ^ d PUnit.unit) =
    ↑((e 0 + e 1).choose (e 0)) * (coeff R (e 0 + e 1)) f

A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
e : Fin 2 →₀ ℕ
⊢ MvPowerSeries.SubstDomain fun x => MvPowerSeries.X 0 + MvPowerSeries.X 1
Tactic:
rw [finsum_eq_single _ (Finsupp.single () (e 0 + e 1)), mul_comm]
State after:
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
e : Fin 2 →₀ ℕ
⊢ MvPolynomial.coeff e ((MvPolynomial.X 0 + MvPolynomial.X 1) ^ (Finsupp.single () (e 0 + e 1)) PUnit.unit) *
      (MvPowerSeries.coeff R (Finsupp.single () (e 0 + e 1))) f =
    ↑((e 0 + e 1).choose (e 0)) * (coeff R (e 0 + e 1)) f

A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
e : Fin 2 →₀ ℕ
⊢ ∀ (x : Unit →₀ ℕ),
    x ≠ Finsupp.single () (e 0 + e 1) →
      (MvPowerSeries.coeff R x) f * MvPolynomial.coeff e ((MvPolynomial.X 0 + MvPolynomial.X 1) ^ x PUnit.unit) = 0

A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
e : Fin 2 →₀ ℕ
⊢ MvPowerSeries.SubstDomain fun x => MvPowerSeries.X 0 + MvPowerSeries.X 1

State before:
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
e : Fin 2 →₀ ℕ
⊢ MvPolynomial.coeff e ((MvPolynomial.X 0 + MvPolynomial.X 1) ^ (Finsupp.single () (e 0 + e 1)) PUnit.unit) *
      (MvPowerSeries.coeff R (Finsupp.single () (e 0 + e 1))) f =
    ↑((e 0 + e 1).choose (e 0)) * (coeff R (e 0 + e 1)) f
Tactic:
apply congr_arg₂
State after:
case hx
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
e : Fin 2 →₀ ℕ
⊢ MvPolynomial.coeff e ((MvPolynomial.X 0 + MvPolynomial.X 1) ^ (Finsupp.single () (e 0 + e 1)) PUnit.unit) =
    ↑((e 0 + e 1).choose (e 0))

case hy
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
e : Fin 2 →₀ ℕ
⊢ (MvPowerSeries.coeff R (Finsupp.single () (e 0 + e 1))) f = (coeff R (e 0 + e 1)) f

State before:
case hx
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
e : Fin 2 →₀ ℕ
⊢ MvPolynomial.coeff e ((MvPolynomial.X 0 + MvPolynomial.X 1) ^ (Finsupp.single () (e 0 + e 1)) PUnit.unit) =
    ↑((e 0 + e 1).choose (e 0))

case hy
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
e : Fin 2 →₀ ℕ
⊢ (MvPowerSeries.coeff R (Finsupp.single () (e 0 + e 1))) f = (coeff R (e 0 + e 1)) f
Tactic:
simp only [Finsupp.single_add, Finsupp.coe_add, Pi.add_apply, Finsupp.single_eq_same]
State after:
case hx
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
e : Fin 2 →₀ ℕ
⊢ MvPolynomial.coeff e ((MvPolynomial.X 0 + MvPolynomial.X 1) ^ (e 0 + e 1)) = ↑((e 0 + e 1).choose (e 0))

case hy
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
e : Fin 2 →₀ ℕ
⊢ (MvPowerSeries.coeff R (Finsupp.single () (e 0 + e 1))) f = (coeff R (e 0 + e 1)) f

State before:
case hx
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
e : Fin 2 →₀ ℕ
⊢ MvPolynomial.coeff e ((MvPolynomial.X 0 + MvPolynomial.X 1) ^ (e 0 + e 1)) = ↑((e 0 + e 1).choose (e 0))

case hy
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
e : Fin 2 →₀ ℕ
⊢ (MvPowerSeries.coeff R (Finsupp.single () (e 0 + e 1))) f = (coeff R (e 0 + e 1)) f
Tactic:
simp only [Fin.isValue, coeff_add_pow e _, Finset.mem_antidiagonal, ↓reduceIte, coeff]
State after:
case hy
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
e : Fin 2 →₀ ℕ
⊢ (MvPowerSeries.coeff R (Finsupp.single () (e 0 + e 1))) f = (coeff R (e 0 + e 1)) f

State before:
case hy
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
e : Fin 2 →₀ ℕ
⊢ (MvPowerSeries.coeff R (Finsupp.single () (e 0 + e 1))) f = (coeff R (e 0 + e 1)) f
Tactic:
rfl
State after:
no goals

State before:
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
e : Fin 2 →₀ ℕ
⊢ ∀ (x : Unit →₀ ℕ),
    x ≠ Finsupp.single () (e 0 + e 1) →
      (MvPowerSeries.coeff R x) f * MvPolynomial.coeff e ((MvPolynomial.X 0 + MvPolynomial.X 1) ^ x PUnit.unit) = 0
Tactic:
intro d hd'
State after:
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
e : Fin 2 →₀ ℕ
d : Unit →₀ ℕ
hd' : d ≠ Finsupp.single () (e 0 + e 1)
⊢ (MvPowerSeries.coeff R d) f * MvPolynomial.coeff e ((MvPolynomial.X 0 + MvPolynomial.X 1) ^ d PUnit.unit) = 0

State before:
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
e : Fin 2 →₀ ℕ
d : Unit →₀ ℕ
hd' : d ≠ Finsupp.single () (e 0 + e 1)
⊢ (MvPowerSeries.coeff R d) f * MvPolynomial.coeff e ((MvPolynomial.X 0 + MvPolynomial.X 1) ^ d PUnit.unit) = 0
Tactic:
simp [coeff_add_pow]
State after:
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
e : Fin 2 →₀ ℕ
d : Unit →₀ ℕ
hd' : d ≠ Finsupp.single () (e 0 + e 1)
⊢ e 0 + e 1 = d PUnit.unit → (MvPowerSeries.coeff R d) f * ↑((d PUnit.unit).choose (e 0)) = 0

State before:
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
e : Fin 2 →₀ ℕ
d : Unit →₀ ℕ
hd' : d ≠ Finsupp.single () (e 0 + e 1)
⊢ e 0 + e 1 = d PUnit.unit → (MvPowerSeries.coeff R d) f * ↑((d PUnit.unit).choose (e 0)) = 0
Tactic:
intro hd
State after:
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
e : Fin 2 →₀ ℕ
d : Unit →₀ ℕ
hd' : d ≠ Finsupp.single () (e 0 + e 1)
hd : e 0 + e 1 = d PUnit.unit
⊢ (MvPowerSeries.coeff R d) f * ↑((d PUnit.unit).choose (e 0)) = 0

State before:
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
e : Fin 2 →₀ ℕ
d : Unit →₀ ℕ
hd' : d ≠ Finsupp.single () (e 0 + e 1)
hd : e 0 + e 1 = d PUnit.unit
⊢ (MvPowerSeries.coeff R d) f * ↑((d PUnit.unit).choose (e 0)) = 0
Tactic:
exfalso
State after:
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
e : Fin 2 →₀ ℕ
d : Unit →₀ ℕ
hd' : d ≠ Finsupp.single () (e 0 + e 1)
hd : e 0 + e 1 = d PUnit.unit
⊢ False

State before:
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
e : Fin 2 →₀ ℕ
d : Unit →₀ ℕ
hd' : d ≠ Finsupp.single () (e 0 + e 1)
hd : e 0 + e 1 = d PUnit.unit
⊢ False
Tactic:
apply hd'
State after:
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
e : Fin 2 →₀ ℕ
d : Unit →₀ ℕ
hd' : d ≠ Finsupp.single () (e 0 + e 1)
hd : e 0 + e 1 = d PUnit.unit
⊢ d = Finsupp.single () (e 0 + e 1)

State before:
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
e : Fin 2 →₀ ℕ
d : Unit →₀ ℕ
hd' : d ≠ Finsupp.single () (e 0 + e 1)
hd : e 0 + e 1 = d PUnit.unit
⊢ d = Finsupp.single () (e 0 + e 1)
Tactic:
ext
State after:
case h
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
e : Fin 2 →₀ ℕ
d : Unit →₀ ℕ
hd' : d ≠ Finsupp.single () (e 0 + e 1)
hd : e 0 + e 1 = d PUnit.unit
⊢ d default = (Finsupp.single () (e 0 + e 1)) default

State before:
case h
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
e : Fin 2 →₀ ℕ
d : Unit →₀ ℕ
hd' : d ≠ Finsupp.single () (e 0 + e 1)
hd : e 0 + e 1 = d PUnit.unit
⊢ d default = (Finsupp.single () (e 0 + e 1)) default
Tactic:
simp only [PUnit.default_eq_unit, hd, Finsupp.single_eq_same]
State after:
no goals

State before:
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
e : Fin 2 →₀ ℕ
⊢ MvPowerSeries.SubstDomain fun x => MvPowerSeries.X 0 + MvPowerSeries.X 1
Tactic:
exact MvPowerSeries.substDomain_of_constantCoeff_zero
      (fun _ ↦ by simp)
State after:
no goals

State before:
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
e : Fin 2 →₀ ℕ
x✝ : Unit
⊢ (MvPowerSeries.constantCoeff (Fin 2) R) (MvPowerSeries.X 0 + MvPowerSeries.X 1) = 0
Tactic:
simp
State after:
no goals

State before:
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
he :
  ∀ (e : Fin 2 →₀ ℕ),
    (MvPowerSeries.coeff R e) (subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f) =
      ↑((e 0 + e 1).choose (e 0)) * (coeff R (e 0 + e 1)) f
⊢ ∀ (e : Fin 2 →₀ ℕ),
    (MvPowerSeries.coeff R e) (subst (MvPowerSeries.X 0) f * subst (MvPowerSeries.X 1) f) =
      (coeff R (e 0)) f * (coeff R (e 1)) f
Tactic:
intro e
State after:
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
he :
  ∀ (e : Fin 2 →₀ ℕ),
    (MvPowerSeries.coeff R e) (subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f) =
      ↑((e 0 + e 1).choose (e 0)) * (coeff R (e 0 + e 1)) f
e : Fin 2 →₀ ℕ
⊢ (MvPowerSeries.coeff R e) (subst (MvPowerSeries.X 0) f * subst (MvPowerSeries.X 1) f) =
    (coeff R (e 0)) f * (coeff R (e 1)) f

State before:
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
he :
  ∀ (e : Fin 2 →₀ ℕ),
    (MvPowerSeries.coeff R e) (subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f) =
      ↑((e 0 + e 1).choose (e 0)) * (coeff R (e 0 + e 1)) f
e : Fin 2 →₀ ℕ
⊢ (MvPowerSeries.coeff R e) (subst (MvPowerSeries.X 0) f * subst (MvPowerSeries.X 1) f) =
    (coeff R (e 0)) f * (coeff R (e 1)) f
Tactic:
rw [MvPowerSeries.coeff_mul]
State after:
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
he :
  ∀ (e : Fin 2 →₀ ℕ),
    (MvPowerSeries.coeff R e) (subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f) =
      ↑((e 0 + e 1).choose (e 0)) * (coeff R (e 0 + e 1)) f
e : Fin 2 →₀ ℕ
⊢ ∑ p ∈ Finset.antidiagonal e,
      (MvPowerSeries.coeff R p.1) (subst (MvPowerSeries.X 0) f) *
        (MvPowerSeries.coeff R p.2) (subst (MvPowerSeries.X 1) f) =
    (coeff R (e 0)) f * (coeff R (e 1)) f

State before:
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
he :
  ∀ (e : Fin 2 →₀ ℕ),
    (MvPowerSeries.coeff R e) (subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f) =
      ↑((e 0 + e 1).choose (e 0)) * (coeff R (e 0 + e 1)) f
e : Fin 2 →₀ ℕ
⊢ ∑ p ∈ Finset.antidiagonal e,
      (MvPowerSeries.coeff R p.1) (subst (MvPowerSeries.X 0) f) *
        (MvPowerSeries.coeff R p.2) (subst (MvPowerSeries.X 1) f) =
    (coeff R (e 0)) f * (coeff R (e 1)) f
Tactic:
rw [Finset.sum_eq_single (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1))]
State after:
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
he :
  ∀ (e : Fin 2 →₀ ℕ),
    (MvPowerSeries.coeff R e) (subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f) =
      ↑((e 0 + e 1).choose (e 0)) * (coeff R (e 0 + e 1)) f
e : Fin 2 →₀ ℕ
⊢ (MvPowerSeries.coeff R (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1)).1) (subst (MvPowerSeries.X 0) f) *
      (MvPowerSeries.coeff R (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1)).2) (subst (MvPowerSeries.X 1) f) =
    (coeff R (e 0)) f * (coeff R (e 1)) f

case h₀
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
he :
  ∀ (e : Fin 2 →₀ ℕ),
    (MvPowerSeries.coeff R e) (subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f) =
      ↑((e 0 + e 1).choose (e 0)) * (coeff R (e 0 + e 1)) f
e : Fin 2 →₀ ℕ
⊢ ∀ b ∈ Finset.antidiagonal e,
    b ≠ (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1)) →
      (MvPowerSeries.coeff R b.1) (subst (MvPowerSeries.X 0) f) *
          (MvPowerSeries.coeff R b.2) (subst (MvPowerSeries.X 1) f) =
        0

case h₁
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
he :
  ∀ (e : Fin 2 →₀ ℕ),
    (MvPowerSeries.coeff R e) (subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f) =
      ↑((e 0 + e 1).choose (e 0)) * (coeff R (e 0 + e 1)) f
e : Fin 2 →₀ ℕ
⊢ (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1)) ∉ Finset.antidiagonal e →
    (MvPowerSeries.coeff R (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1)).1) (subst (MvPowerSeries.X 0) f) *
        (MvPowerSeries.coeff R (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1)).2) (subst (MvPowerSeries.X 1) f) =
      0

State before:
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
he :
  ∀ (e : Fin 2 →₀ ℕ),
    (MvPowerSeries.coeff R e) (subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f) =
      ↑((e 0 + e 1).choose (e 0)) * (coeff R (e 0 + e 1)) f
e : Fin 2 →₀ ℕ
⊢ (MvPowerSeries.coeff R (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1)).1) (subst (MvPowerSeries.X 0) f) *
      (MvPowerSeries.coeff R (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1)).2) (subst (MvPowerSeries.X 1) f) =
    (coeff R (e 0)) f * (coeff R (e 1)) f
Tactic:
apply congr_arg₂
State after:
case hx
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
he :
  ∀ (e : Fin 2 →₀ ℕ),
    (MvPowerSeries.coeff R e) (subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f) =
      ↑((e 0 + e 1).choose (e 0)) * (coeff R (e 0 + e 1)) f
e : Fin 2 →₀ ℕ
⊢ (MvPowerSeries.coeff R (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1)).1) (subst (MvPowerSeries.X 0) f) =
    (coeff R (e 0)) f

case hy
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
he :
  ∀ (e : Fin 2 →₀ ℕ),
    (MvPowerSeries.coeff R e) (subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f) =
      ↑((e 0 + e 1).choose (e 0)) * (coeff R (e 0 + e 1)) f
e : Fin 2 →₀ ℕ
⊢ (MvPowerSeries.coeff R (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1)).2) (subst (MvPowerSeries.X 1) f) =
    (coeff R (e 1)) f

State before:
case hx
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
he :
  ∀ (e : Fin 2 →₀ ℕ),
    (MvPowerSeries.coeff R e) (subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f) =
      ↑((e 0 + e 1).choose (e 0)) * (coeff R (e 0 + e 1)) f
e : Fin 2 →₀ ℕ
⊢ (MvPowerSeries.coeff R (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1)).1) (subst (MvPowerSeries.X 0) f) =
    (coeff R (e 0)) f
Tactic:
simp only [coeff_subst_single, Finsupp.single_eq_same, if_pos]
State after:
no goals

State before:
case hy
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
he :
  ∀ (e : Fin 2 →₀ ℕ),
    (MvPowerSeries.coeff R e) (subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f) =
      ↑((e 0 + e 1).choose (e 0)) * (coeff R (e 0 + e 1)) f
e : Fin 2 →₀ ℕ
⊢ (MvPowerSeries.coeff R (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1)).2) (subst (MvPowerSeries.X 1) f) =
    (coeff R (e 1)) f
Tactic:
simp only [coeff_subst_single, Finsupp.single_eq_same, if_pos]
State after:
no goals

State before:
case h₀
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
he :
  ∀ (e : Fin 2 →₀ ℕ),
    (MvPowerSeries.coeff R e) (subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f) =
      ↑((e 0 + e 1).choose (e 0)) * (coeff R (e 0 + e 1)) f
e : Fin 2 →₀ ℕ
⊢ ∀ b ∈ Finset.antidiagonal e,
    b ≠ (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1)) →
      (MvPowerSeries.coeff R b.1) (subst (MvPowerSeries.X 0) f) *
          (MvPowerSeries.coeff R b.2) (subst (MvPowerSeries.X 1) f) =
        0
Tactic:
intro b hb hb'
State after:
case h₀
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
he :
  ∀ (e : Fin 2 →₀ ℕ),
    (MvPowerSeries.coeff R e) (subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f) =
      ↑((e 0 + e 1).choose (e 0)) * (coeff R (e 0 + e 1)) f
e : Fin 2 →₀ ℕ
b : (Fin 2 →₀ ℕ) × (Fin 2 →₀ ℕ)
hb : b ∈ Finset.antidiagonal e
hb' : b ≠ (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1))
⊢ (MvPowerSeries.coeff R b.1) (subst (MvPowerSeries.X 0) f) *
      (MvPowerSeries.coeff R b.2) (subst (MvPowerSeries.X 1) f) =
    0

State before:
case h₀
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
he :
  ∀ (e : Fin 2 →₀ ℕ),
    (MvPowerSeries.coeff R e) (subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f) =
      ↑((e 0 + e 1).choose (e 0)) * (coeff R (e 0 + e 1)) f
e : Fin 2 →₀ ℕ
b : (Fin 2 →₀ ℕ) × (Fin 2 →₀ ℕ)
hb : b ∈ Finset.antidiagonal e
hb' : b ≠ (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1))
⊢ (MvPowerSeries.coeff R b.1) (subst (MvPowerSeries.X 0) f) *
      (MvPowerSeries.coeff R b.2) (subst (MvPowerSeries.X 1) f) =
    0
Tactic:
rw [Finset.mem_antidiagonal] at hb
State after:
case h₀
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
he :
  ∀ (e : Fin 2 →₀ ℕ),
    (MvPowerSeries.coeff R e) (subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f) =
      ↑((e 0 + e 1).choose (e 0)) * (coeff R (e 0 + e 1)) f
e : Fin 2 →₀ ℕ
b : (Fin 2 →₀ ℕ) × (Fin 2 →₀ ℕ)
hb : b.1 + b.2 = e
hb' : b ≠ (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1))
⊢ (MvPowerSeries.coeff R b.1) (subst (MvPowerSeries.X 0) f) *
      (MvPowerSeries.coeff R b.2) (subst (MvPowerSeries.X 1) f) =
    0

State before:
case h₀
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
he :
  ∀ (e : Fin 2 →₀ ℕ),
    (MvPowerSeries.coeff R e) (subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f) =
      ↑((e 0 + e 1).choose (e 0)) * (coeff R (e 0 + e 1)) f
e : Fin 2 →₀ ℕ
b : (Fin 2 →₀ ℕ) × (Fin 2 →₀ ℕ)
hb : b.1 + b.2 = e
hb' : b ≠ (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1))
⊢ (MvPowerSeries.coeff R b.1) (subst (MvPowerSeries.X 0) f) *
      (MvPowerSeries.coeff R b.2) (subst (MvPowerSeries.X 1) f) =
    0
Tactic:
by_contra hmul_ne_zero
State after:
case h₀
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
he :
  ∀ (e : Fin 2 →₀ ℕ),
    (MvPowerSeries.coeff R e) (subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f) =
      ↑((e 0 + e 1).choose (e 0)) * (coeff R (e 0 + e 1)) f
e : Fin 2 →₀ ℕ
b : (Fin 2 →₀ ℕ) × (Fin 2 →₀ ℕ)
hb : b.1 + b.2 = e
hb' : b ≠ (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1))
hmul_ne_zero :
  ¬(MvPowerSeries.coeff R b.1) (subst (MvPowerSeries.X 0) f) *
        (MvPowerSeries.coeff R b.2) (subst (MvPowerSeries.X 1) f) =
      0
⊢ False

State before:
case h₀
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
he :
  ∀ (e : Fin 2 →₀ ℕ),
    (MvPowerSeries.coeff R e) (subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f) =
      ↑((e 0 + e 1).choose (e 0)) * (coeff R (e 0 + e 1)) f
e : Fin 2 →₀ ℕ
b : (Fin 2 →₀ ℕ) × (Fin 2 →₀ ℕ)
hb : b.1 + b.2 = e
hb' : b ≠ (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1))
hmul_ne_zero :
  ¬(MvPowerSeries.coeff R b.1) (subst (MvPowerSeries.X 0) f) *
        (MvPowerSeries.coeff R b.2) (subst (MvPowerSeries.X 1) f) =
      0
⊢ False
Tactic:
rcases ne_zero_of_mul_ne_zero hmul_ne_zero with ⟨h0, h1⟩
State after:
case h₀.intro
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
he :
  ∀ (e : Fin 2 →₀ ℕ),
    (MvPowerSeries.coeff R e) (subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f) =
      ↑((e 0 + e 1).choose (e 0)) * (coeff R (e 0 + e 1)) f
e : Fin 2 →₀ ℕ
b : (Fin 2 →₀ ℕ) × (Fin 2 →₀ ℕ)
hb : b.1 + b.2 = e
hb' : b ≠ (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1))
hmul_ne_zero :
  ¬(MvPowerSeries.coeff R b.1) (subst (MvPowerSeries.X 0) f) *
        (MvPowerSeries.coeff R b.2) (subst (MvPowerSeries.X 1) f) =
      0
h0 : (MvPowerSeries.coeff R b.1) (subst (MvPowerSeries.X 0) f) ≠ 0
h1 : (MvPowerSeries.coeff R b.2) (subst (MvPowerSeries.X 1) f) ≠ 0
⊢ False

State before:
case h₀.intro
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
he :
  ∀ (e : Fin 2 →₀ ℕ),
    (MvPowerSeries.coeff R e) (subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f) =
      ↑((e 0 + e 1).choose (e 0)) * (coeff R (e 0 + e 1)) f
e : Fin 2 →₀ ℕ
b : (Fin 2 →₀ ℕ) × (Fin 2 →₀ ℕ)
hb : b.1 + b.2 = e
hb' : b ≠ (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1))
hmul_ne_zero :
  ¬(MvPowerSeries.coeff R b.1) (subst (MvPowerSeries.X 0) f) *
        (MvPowerSeries.coeff R b.2) (subst (MvPowerSeries.X 1) f) =
      0
h0 : (MvPowerSeries.coeff R b.1) (subst (MvPowerSeries.X 0) f) ≠ 0
h1 : (MvPowerSeries.coeff R b.2) (subst (MvPowerSeries.X 1) f) ≠ 0
⊢ False
Tactic:
simp only [Fin.isValue, coeff_subst_single, ne_eq, ite_eq_right_iff,
  not_forall, exists_prop] at h0 h1
State after:
case h₀.intro
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
he :
  ∀ (e : Fin 2 →₀ ℕ),
    (MvPowerSeries.coeff R e) (subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f) =
      ↑((e 0 + e 1).choose (e 0)) * (coeff R (e 0 + e 1)) f
e : Fin 2 →₀ ℕ
b : (Fin 2 →₀ ℕ) × (Fin 2 →₀ ℕ)
hb : b.1 + b.2 = e
hb' : b ≠ (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1))
hmul_ne_zero :
  ¬(MvPowerSeries.coeff R b.1) (subst (MvPowerSeries.X 0) f) *
        (MvPowerSeries.coeff R b.2) (subst (MvPowerSeries.X 1) f) =
      0
h0 : b.1 = Finsupp.single 0 (b.1 0) ∧ ¬(coeff R (b.1 0)) f = 0
h1 : b.2 = Finsupp.single 1 (b.2 1) ∧ ¬(coeff R (b.2 1)) f = 0
⊢ False

State before:
case h₀.intro
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
he :
  ∀ (e : Fin 2 →₀ ℕ),
    (MvPowerSeries.coeff R e) (subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f) =
      ↑((e 0 + e 1).choose (e 0)) * (coeff R (e 0 + e 1)) f
e : Fin 2 →₀ ℕ
b : (Fin 2 →₀ ℕ) × (Fin 2 →₀ ℕ)
hb : b.1 + b.2 = e
hb' : b ≠ (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1))
hmul_ne_zero :
  ¬(MvPowerSeries.coeff R b.1) (subst (MvPowerSeries.X 0) f) *
        (MvPowerSeries.coeff R b.2) (subst (MvPowerSeries.X 1) f) =
      0
h0 : b.1 = Finsupp.single 0 (b.1 0) ∧ ¬(coeff R (b.1 0)) f = 0
h1 : b.2 = Finsupp.single 1 (b.2 1) ∧ ¬(coeff R (b.2 1)) f = 0
⊢ False
Tactic:
apply hb'
State after:
case h₀.intro
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
he :
  ∀ (e : Fin 2 →₀ ℕ),
    (MvPowerSeries.coeff R e) (subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f) =
      ↑((e 0 + e 1).choose (e 0)) * (coeff R (e 0 + e 1)) f
e : Fin 2 →₀ ℕ
b : (Fin 2 →₀ ℕ) × (Fin 2 →₀ ℕ)
hb : b.1 + b.2 = e
hb' : b ≠ (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1))
hmul_ne_zero :
  ¬(MvPowerSeries.coeff R b.1) (subst (MvPowerSeries.X 0) f) *
        (MvPowerSeries.coeff R b.2) (subst (MvPowerSeries.X 1) f) =
      0
h0 : b.1 = Finsupp.single 0 (b.1 0) ∧ ¬(coeff R (b.1 0)) f = 0
h1 : b.2 = Finsupp.single 1 (b.2 1) ∧ ¬(coeff R (b.2 1)) f = 0
⊢ b = (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1))

State before:
case h₀.intro
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
he :
  ∀ (e : Fin 2 →₀ ℕ),
    (MvPowerSeries.coeff R e) (subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f) =
      ↑((e 0 + e 1).choose (e 0)) * (coeff R (e 0 + e 1)) f
e : Fin 2 →₀ ℕ
b : (Fin 2 →₀ ℕ) × (Fin 2 →₀ ℕ)
hb : b.1 + b.2 = e
hb' : b ≠ (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1))
hmul_ne_zero :
  ¬(MvPowerSeries.coeff R b.1) (subst (MvPowerSeries.X 0) f) *
        (MvPowerSeries.coeff R b.2) (subst (MvPowerSeries.X 1) f) =
      0
h0 : b.1 = Finsupp.single 0 (b.1 0) ∧ ¬(coeff R (b.1 0)) f = 0
h1 : b.2 = Finsupp.single 1 (b.2 1) ∧ ¬(coeff R (b.2 1)) f = 0
⊢ b = (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1))
Tactic:
rw [Prod.ext_iff, ← hb, h0.1, h1.1]
State after:
case h₀.intro
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
he :
  ∀ (e : Fin 2 →₀ ℕ),
    (MvPowerSeries.coeff R e) (subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f) =
      ↑((e 0 + e 1).choose (e 0)) * (coeff R (e 0 + e 1)) f
e : Fin 2 →₀ ℕ
b : (Fin 2 →₀ ℕ) × (Fin 2 →₀ ℕ)
hb : b.1 + b.2 = e
hb' : b ≠ (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1))
hmul_ne_zero :
  ¬(MvPowerSeries.coeff R b.1) (subst (MvPowerSeries.X 0) f) *
        (MvPowerSeries.coeff R b.2) (subst (MvPowerSeries.X 1) f) =
      0
h0 : b.1 = Finsupp.single 0 (b.1 0) ∧ ¬(coeff R (b.1 0)) f = 0
h1 : b.2 = Finsupp.single 1 (b.2 1) ∧ ¬(coeff R (b.2 1)) f = 0
⊢ Finsupp.single 0 (b.1 0) =
      (Finsupp.single 0 ((Finsupp.single 0 (b.1 0) + Finsupp.single 1 (b.2 1)) 0),
          Finsupp.single 1 ((Finsupp.single 0 (b.1 0) + Finsupp.single 1 (b.2 1)) 1)).1 ∧
    Finsupp.single 1 (b.2 1) =
      (Finsupp.single 0 ((Finsupp.single 0 (b.1 0) + Finsupp.single 1 (b.2 1)) 0),
          Finsupp.single 1 ((Finsupp.single 0 (b.1 0) + Finsupp.single 1 (b.2 1)) 1)).2

State before:
case h₀.intro
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
he :
  ∀ (e : Fin 2 →₀ ℕ),
    (MvPowerSeries.coeff R e) (subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f) =
      ↑((e 0 + e 1).choose (e 0)) * (coeff R (e 0 + e 1)) f
e : Fin 2 →₀ ℕ
b : (Fin 2 →₀ ℕ) × (Fin 2 →₀ ℕ)
hb : b.1 + b.2 = e
hb' : b ≠ (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1))
hmul_ne_zero :
  ¬(MvPowerSeries.coeff R b.1) (subst (MvPowerSeries.X 0) f) *
        (MvPowerSeries.coeff R b.2) (subst (MvPowerSeries.X 1) f) =
      0
h0 : b.1 = Finsupp.single 0 (b.1 0) ∧ ¬(coeff R (b.1 0)) f = 0
h1 : b.2 = Finsupp.single 1 (b.2 1) ∧ ¬(coeff R (b.2 1)) f = 0
⊢ Finsupp.single 0 (b.1 0) =
      (Finsupp.single 0 ((Finsupp.single 0 (b.1 0) + Finsupp.single 1 (b.2 1)) 0),
          Finsupp.single 1 ((Finsupp.single 0 (b.1 0) + Finsupp.single 1 (b.2 1)) 1)).1 ∧
    Finsupp.single 1 (b.2 1) =
      (Finsupp.single 0 ((Finsupp.single 0 (b.1 0) + Finsupp.single 1 (b.2 1)) 0),
          Finsupp.single 1 ((Finsupp.single 0 (b.1 0) + Finsupp.single 1 (b.2 1)) 1)).2
Tactic:
simp
State after:
no goals

State before:
case h₁
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
he :
  ∀ (e : Fin 2 →₀ ℕ),
    (MvPowerSeries.coeff R e) (subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f) =
      ↑((e 0 + e 1).choose (e 0)) * (coeff R (e 0 + e 1)) f
e : Fin 2 →₀ ℕ
⊢ (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1)) ∉ Finset.antidiagonal e →
    (MvPowerSeries.coeff R (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1)).1) (subst (MvPowerSeries.X 0) f) *
        (MvPowerSeries.coeff R (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1)).2) (subst (MvPowerSeries.X 1) f) =
      0
Tactic:
intro he
State after:
case h₁
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
he✝ :
  ∀ (e : Fin 2 →₀ ℕ),
    (MvPowerSeries.coeff R e) (subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f) =
      ↑((e 0 + e 1).choose (e 0)) * (coeff R (e 0 + e 1)) f
e : Fin 2 →₀ ℕ
he : (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1)) ∉ Finset.antidiagonal e
⊢ (MvPowerSeries.coeff R (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1)).1) (subst (MvPowerSeries.X 0) f) *
      (MvPowerSeries.coeff R (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1)).2) (subst (MvPowerSeries.X 1) f) =
    0

State before:
case h₁
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
he✝ :
  ∀ (e : Fin 2 →₀ ℕ),
    (MvPowerSeries.coeff R e) (subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f) =
      ↑((e 0 + e 1).choose (e 0)) * (coeff R (e 0 + e 1)) f
e : Fin 2 →₀ ℕ
he : (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1)) ∉ Finset.antidiagonal e
⊢ (MvPowerSeries.coeff R (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1)).1) (subst (MvPowerSeries.X 0) f) *
      (MvPowerSeries.coeff R (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1)).2) (subst (MvPowerSeries.X 1) f) =
    0
Tactic:
exfalso
State after:
case h₁
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
he✝ :
  ∀ (e : Fin 2 →₀ ℕ),
    (MvPowerSeries.coeff R e) (subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f) =
      ↑((e 0 + e 1).choose (e 0)) * (coeff R (e 0 + e 1)) f
e : Fin 2 →₀ ℕ
he : (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1)) ∉ Finset.antidiagonal e
⊢ False

State before:
case h₁
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
he✝ :
  ∀ (e : Fin 2 →₀ ℕ),
    (MvPowerSeries.coeff R e) (subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f) =
      ↑((e 0 + e 1).choose (e 0)) * (coeff R (e 0 + e 1)) f
e : Fin 2 →₀ ℕ
he : (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1)) ∉ Finset.antidiagonal e
⊢ False
Tactic:
apply he
State after:
case h₁
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
he✝ :
  ∀ (e : Fin 2 →₀ ℕ),
    (MvPowerSeries.coeff R e) (subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f) =
      ↑((e 0 + e 1).choose (e 0)) * (coeff R (e 0 + e 1)) f
e : Fin 2 →₀ ℕ
he : (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1)) ∉ Finset.antidiagonal e
⊢ (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1)) ∈ Finset.antidiagonal e

State before:
case h₁
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
he✝ :
  ∀ (e : Fin 2 →₀ ℕ),
    (MvPowerSeries.coeff R e) (subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f) =
      ↑((e 0 + e 1).choose (e 0)) * (coeff R (e 0 + e 1)) f
e : Fin 2 →₀ ℕ
he : (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1)) ∉ Finset.antidiagonal e
⊢ (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1)) ∈ Finset.antidiagonal e
Tactic:
simp only [Finset.mem_antidiagonal]
State after:
case h₁
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
he✝ :
  ∀ (e : Fin 2 →₀ ℕ),
    (MvPowerSeries.coeff R e) (subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f) =
      ↑((e 0 + e 1).choose (e 0)) * (coeff R (e 0 + e 1)) f
e : Fin 2 →₀ ℕ
he : (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1)) ∉ Finset.antidiagonal e
⊢ Finsupp.single 0 (e 0) + Finsupp.single 1 (e 1) = e

State before:
case h₁
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
he✝ :
  ∀ (e : Fin 2 →₀ ℕ),
    (MvPowerSeries.coeff R e) (subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f) =
      ↑((e 0 + e 1).choose (e 0)) * (coeff R (e 0 + e 1)) f
e : Fin 2 →₀ ℕ
he : (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1)) ∉ Finset.antidiagonal e
⊢ Finsupp.single 0 (e 0) + Finsupp.single 1 (e 1) = e
Tactic:
ext i
State after:
case h₁.h
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
he✝ :
  ∀ (e : Fin 2 →₀ ℕ),
    (MvPowerSeries.coeff R e) (subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f) =
      ↑((e 0 + e 1).choose (e 0)) * (coeff R (e 0 + e 1)) f
e : Fin 2 →₀ ℕ
he : (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1)) ∉ Finset.antidiagonal e
i : Fin 2
⊢ (Finsupp.single 0 (e 0) + Finsupp.single 1 (e 1)) i = e i

State before:
case h₁.h
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
he✝ :
  ∀ (e : Fin 2 →₀ ℕ),
    (MvPowerSeries.coeff R e) (subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f) =
      ↑((e 0 + e 1).choose (e 0)) * (coeff R (e 0 + e 1)) f
e : Fin 2 →₀ ℕ
he : (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1)) ∉ Finset.antidiagonal e
i : Fin 2
⊢ (Finsupp.single 0 (e 0) + Finsupp.single 1 (e 1)) i = e i
Tactic:
match i with
| 0 => simp
| 1 => simp
State after:
no goals

State before:
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
he✝ :
  ∀ (e : Fin 2 →₀ ℕ),
    (MvPowerSeries.coeff R e) (subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f) =
      ↑((e 0 + e 1).choose (e 0)) * (coeff R (e 0 + e 1)) f
e : Fin 2 →₀ ℕ
he : (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1)) ∉ Finset.antidiagonal e
i : Fin 2
⊢ (Finsupp.single 0 (e 0) + Finsupp.single 1 (e 1)) 0 = e 0
Tactic:
simp
State after:
no goals

State before:
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
he✝ :
  ∀ (e : Fin 2 →₀ ℕ),
    (MvPowerSeries.coeff R e) (subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f) =
      ↑((e 0 + e 1).choose (e 0)) * (coeff R (e 0 + e 1)) f
e : Fin 2 →₀ ℕ
he : (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1)) ∉ Finset.antidiagonal e
i : Fin 2
⊢ (Finsupp.single 0 (e 0) + Finsupp.single 1 (e 1)) 1 = e 1
Tactic:
simp
State after:
no goals