Theorem: PowerSeries.isExponential_scale (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
a : A
f : R⟦X⟧
hf : f.IsExponential
⊢ (constantCoeff R) (scale a f) = 1
Tactic:
rw [← coeff_zero_eq_constantCoeff, coeff_scale]
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
a : A
f : R⟦X⟧
hf : f.IsExponential
⊢ a ^ 0 • (coeff R 0) f = 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
a : A
f : R⟦X⟧
hf : f.IsExponential
⊢ a ^ 0 • (coeff R 0) f = 1
Tactic:
simp only [pow_zero, coeff_zero_eq_constantCoeff, one_smul,
  hf.constantCoeff]
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
a : A
f : R⟦X⟧
hf : f.IsExponential
⊢ subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) (scale a f) =
    subst (MvPowerSeries.X 0) (scale a f) * subst (MvPowerSeries.X 1) (scale a f)
Tactic:
rw [subst_linear_subst_scalar_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
a : A
f : R⟦X⟧
hf : f.IsExponential
⊢ MvPowerSeries.scale (Function.const (Fin 2) a) (subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f) =
    subst (MvPowerSeries.X 0) (scale a f) * subst (MvPowerSeries.X 1) (scale a f)

case hp_lin
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
a : A
f : R⟦X⟧
hf : f.IsExponential
⊢ ∀ (d : Fin 2 →₀ ℕ), (d.sum fun x n => n) ≠ 1 → (MvPowerSeries.coeff R d) (MvPowerSeries.X 0 + MvPowerSeries.X 1) = 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
a : A
f : R⟦X⟧
hf : f.IsExponential
⊢ MvPowerSeries.scale (Function.const (Fin 2) a) (subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f) =
    subst (MvPowerSeries.X 0) (scale a f) * subst (MvPowerSeries.X 1) (scale a f)

case hp_lin
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
a : A
f : R⟦X⟧
hf : f.IsExponential
⊢ ∀ (d : Fin 2 →₀ ℕ), (d.sum fun x n => n) ≠ 1 → (MvPowerSeries.coeff R d) (MvPowerSeries.X 0 + MvPowerSeries.X 1) = 0
Tactic:
rw [subst_linear_subst_scalar_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
a : A
f : R⟦X⟧
hf : f.IsExponential
⊢ MvPowerSeries.scale (Function.const (Fin 2) a) (subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f) =
    MvPowerSeries.scale (Function.const (Fin 2) a) (subst (MvPowerSeries.X 0) f) * subst (MvPowerSeries.X 1) (scale a f)

case hp_lin
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
a : A
f : R⟦X⟧
hf : f.IsExponential
⊢ ∀ (d : Fin 2 →₀ ℕ), (d.sum fun x n => n) ≠ 1 → (MvPowerSeries.coeff R d) (MvPowerSeries.X 0) = 0

case hp_lin
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
a : A
f : R⟦X⟧
hf : f.IsExponential
⊢ ∀ (d : Fin 2 →₀ ℕ), (d.sum fun x n => n) ≠ 1 → (MvPowerSeries.coeff R d) (MvPowerSeries.X 0 + MvPowerSeries.X 1) = 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
a : A
f : R⟦X⟧
hf : f.IsExponential
⊢ MvPowerSeries.scale (Function.const (Fin 2) a) (subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f) =
    MvPowerSeries.scale (Function.const (Fin 2) a) (subst (MvPowerSeries.X 0) f) * subst (MvPowerSeries.X 1) (scale a f)

case hp_lin
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
a : A
f : R⟦X⟧
hf : f.IsExponential
⊢ ∀ (d : Fin 2 →₀ ℕ), (d.sum fun x n => n) ≠ 1 → (MvPowerSeries.coeff R d) (MvPowerSeries.X 0) = 0

case hp_lin
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
a : A
f : R⟦X⟧
hf : f.IsExponential
⊢ ∀ (d : Fin 2 →₀ ℕ), (d.sum fun x n => n) ≠ 1 → (MvPowerSeries.coeff R d) (MvPowerSeries.X 0 + MvPowerSeries.X 1) = 0
Tactic:
rw [subst_linear_subst_scalar_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
a : A
f : R⟦X⟧
hf : f.IsExponential
⊢ MvPowerSeries.scale (Function.const (Fin 2) a) (subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f) =
    MvPowerSeries.scale (Function.const (Fin 2) a) (subst (MvPowerSeries.X 0) f) *
      MvPowerSeries.scale (Function.const (Fin 2) a) (subst (MvPowerSeries.X 1) f)

case hp_lin
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
a : A
f : R⟦X⟧
hf : f.IsExponential
⊢ ∀ (d : Fin 2 →₀ ℕ), (d.sum fun x n => n) ≠ 1 → (MvPowerSeries.coeff R d) (MvPowerSeries.X 1) = 0

case hp_lin
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
a : A
f : R⟦X⟧
hf : f.IsExponential
⊢ ∀ (d : Fin 2 →₀ ℕ), (d.sum fun x n => n) ≠ 1 → (MvPowerSeries.coeff R d) (MvPowerSeries.X 0) = 0

case hp_lin
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
a : A
f : R⟦X⟧
hf : f.IsExponential
⊢ ∀ (d : Fin 2 →₀ ℕ), (d.sum fun x n => n) ≠ 1 → (MvPowerSeries.coeff R d) (MvPowerSeries.X 0 + MvPowerSeries.X 1) = 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
a : A
f : R⟦X⟧
hf : f.IsExponential
⊢ MvPowerSeries.scale (Function.const (Fin 2) a) (subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f) =
    MvPowerSeries.scale (Function.const (Fin 2) a) (subst (MvPowerSeries.X 0) f) *
      MvPowerSeries.scale (Function.const (Fin 2) a) (subst (MvPowerSeries.X 1) f)

case hp_lin
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
a : A
f : R⟦X⟧
hf : f.IsExponential
⊢ ∀ (d : Fin 2 →₀ ℕ), (d.sum fun x n => n) ≠ 1 → (MvPowerSeries.coeff R d) (MvPowerSeries.X 1) = 0

case hp_lin
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
a : A
f : R⟦X⟧
hf : f.IsExponential
⊢ ∀ (d : Fin 2 →₀ ℕ), (d.sum fun x n => n) ≠ 1 → (MvPowerSeries.coeff R d) (MvPowerSeries.X 0) = 0

case hp_lin
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
a : A
f : R⟦X⟧
hf : f.IsExponential
⊢ ∀ (d : Fin 2 →₀ ℕ), (d.sum fun x n => n) ≠ 1 → (MvPowerSeries.coeff R d) (MvPowerSeries.X 0 + MvPowerSeries.X 1) = 0
Tactic:
simp only [← MvPowerSeries.coe_scale_algHom, ← map_mul, hf.add_mul]
State after:
case hp_lin
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
a : A
f : R⟦X⟧
hf : f.IsExponential
⊢ ∀ (d : Fin 2 →₀ ℕ), (d.sum fun x n => n) ≠ 1 → (MvPowerSeries.coeff R d) (MvPowerSeries.X 1) = 0

case hp_lin
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
a : A
f : R⟦X⟧
hf : f.IsExponential
⊢ ∀ (d : Fin 2 →₀ ℕ), (d.sum fun x n => n) ≠ 1 → (MvPowerSeries.coeff R d) (MvPowerSeries.X 0) = 0

case hp_lin
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
a : A
f : R⟦X⟧
hf : f.IsExponential
⊢ ∀ (d : Fin 2 →₀ ℕ), (d.sum fun x n => n) ≠ 1 → (MvPowerSeries.coeff R d) (MvPowerSeries.X 0 + MvPowerSeries.X 1) = 0

State before:
case hp_lin
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
a : A
f : R⟦X⟧
hf : f.IsExponential
⊢ ∀ (d : Fin 2 →₀ ℕ), (d.sum fun x n => n) ≠ 1 → (MvPowerSeries.coeff R d) (MvPowerSeries.X 1) = 0

case hp_lin
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
a : A
f : R⟦X⟧
hf : f.IsExponential
⊢ ∀ (d : Fin 2 →₀ ℕ), (d.sum fun x n => n) ≠ 1 → (MvPowerSeries.coeff R d) (MvPowerSeries.X 0) = 0

case hp_lin
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
a : A
f : R⟦X⟧
hf : f.IsExponential
⊢ ∀ (d : Fin 2 →₀ ℕ), (d.sum fun x n => n) ≠ 1 → (MvPowerSeries.coeff R d) (MvPowerSeries.X 0 + MvPowerSeries.X 1) = 0
Tactic:
repeat
  intro d hd
  simp only [Fin.isValue, map_add, MvPowerSeries.coeff_X]
  rw [if_neg]
  intro hd'
  apply hd
  rw [hd']
  simp only [Fin.isValue, Finsupp.sum_single_index]
State after:
case hp_lin
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
a : A
f : R⟦X⟧
hf : f.IsExponential
⊢ ∀ (d : Fin 2 →₀ ℕ), (d.sum fun x n => n) ≠ 1 → (MvPowerSeries.coeff R d) (MvPowerSeries.X 0 + MvPowerSeries.X 1) = 0

State before:
case hp_lin
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
a : A
f : R⟦X⟧
hf : f.IsExponential
⊢ ∀ (d : Fin 2 →₀ ℕ), (d.sum fun x n => n) ≠ 1 → (MvPowerSeries.coeff R d) (MvPowerSeries.X 0 + MvPowerSeries.X 1) = 0
Tactic:
intro d hd
State after:
case hp_lin
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
a : A
f : R⟦X⟧
hf : f.IsExponential
d : Fin 2 →₀ ℕ
hd : (d.sum fun x n => n) ≠ 1
⊢ (MvPowerSeries.coeff R d) (MvPowerSeries.X 0 + MvPowerSeries.X 1) = 0

State before:
case hp_lin
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
a : A
f : R⟦X⟧
hf : f.IsExponential
d : Fin 2 →₀ ℕ
hd : (d.sum fun x n => n) ≠ 1
⊢ (MvPowerSeries.coeff R d) (MvPowerSeries.X 0 + MvPowerSeries.X 1) = 0
Tactic:
simp only [Fin.isValue, map_add, MvPowerSeries.coeff_X]
State after:
case hp_lin
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
a : A
f : R⟦X⟧
hf : f.IsExponential
d : Fin 2 →₀ ℕ
hd : (d.sum fun x n => n) ≠ 1
⊢ ((if d = Finsupp.single 0 1 then 1 else 0) + if d = Finsupp.single 1 1 then 1 else 0) = 0

State before:
case hp_lin
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
a : A
f : R⟦X⟧
hf : f.IsExponential
d : Fin 2 →₀ ℕ
hd : (d.sum fun x n => n) ≠ 1
⊢ ((if d = Finsupp.single 0 1 then 1 else 0) + if d = Finsupp.single 1 1 then 1 else 0) = 0
Tactic:
rw [if_neg]
State after:
case hp_lin
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
a : A
f : R⟦X⟧
hf : f.IsExponential
d : Fin 2 →₀ ℕ
hd : (d.sum fun x n => n) ≠ 1
⊢ (0 + if d = Finsupp.single 1 1 then 1 else 0) = 0

case hp_lin.hnc
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
a : A
f : R⟦X⟧
hf : f.IsExponential
d : Fin 2 →₀ ℕ
hd : (d.sum fun x n => n) ≠ 1
⊢ ¬d = Finsupp.single 0 1

State before:
case hp_lin.hnc
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
a : A
f : R⟦X⟧
hf : f.IsExponential
d : Fin 2 →₀ ℕ
hd : (d.sum fun x n => n) ≠ 1
⊢ ¬d = Finsupp.single 0 1

case hp_lin
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
a : A
f : R⟦X⟧
hf : f.IsExponential
⊢ ∀ (d : Fin 2 →₀ ℕ), (d.sum fun x n => n) ≠ 1 → (MvPowerSeries.coeff R d) (MvPowerSeries.X 0 + MvPowerSeries.X 1) = 0
Tactic:
intro hd'
State after:
case hp_lin.hnc
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
a : A
f : R⟦X⟧
hf : f.IsExponential
d : Fin 2 →₀ ℕ
hd : (d.sum fun x n => n) ≠ 1
hd' : d = Finsupp.single 0 1
⊢ False

case hp_lin
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
a : A
f : R⟦X⟧
hf : f.IsExponential
⊢ ∀ (d : Fin 2 →₀ ℕ), (d.sum fun x n => n) ≠ 1 → (MvPowerSeries.coeff R d) (MvPowerSeries.X 0 + MvPowerSeries.X 1) = 0

State before:
case hp_lin.hnc
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
a : A
f : R⟦X⟧
hf : f.IsExponential
d : Fin 2 →₀ ℕ
hd : (d.sum fun x n => n) ≠ 1
hd' : d = Finsupp.single 0 1
⊢ False

case hp_lin
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
a : A
f : R⟦X⟧
hf : f.IsExponential
⊢ ∀ (d : Fin 2 →₀ ℕ), (d.sum fun x n => n) ≠ 1 → (MvPowerSeries.coeff R d) (MvPowerSeries.X 0 + MvPowerSeries.X 1) = 0
Tactic:
apply hd
State after:
case hp_lin.hnc
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
a : A
f : R⟦X⟧
hf : f.IsExponential
d : Fin 2 →₀ ℕ
hd : (d.sum fun x n => n) ≠ 1
hd' : d = Finsupp.single 0 1
⊢ (d.sum fun x n => n) = 1

case hp_lin
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
a : A
f : R⟦X⟧
hf : f.IsExponential
⊢ ∀ (d : Fin 2 →₀ ℕ), (d.sum fun x n => n) ≠ 1 → (MvPowerSeries.coeff R d) (MvPowerSeries.X 0 + MvPowerSeries.X 1) = 0

State before:
case hp_lin.hnc
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
a : A
f : R⟦X⟧
hf : f.IsExponential
d : Fin 2 →₀ ℕ
hd : (d.sum fun x n => n) ≠ 1
hd' : d = Finsupp.single 0 1
⊢ (d.sum fun x n => n) = 1

case hp_lin
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
a : A
f : R⟦X⟧
hf : f.IsExponential
⊢ ∀ (d : Fin 2 →₀ ℕ), (d.sum fun x n => n) ≠ 1 → (MvPowerSeries.coeff R d) (MvPowerSeries.X 0 + MvPowerSeries.X 1) = 0
Tactic:
rw [hd']
State after:
case hp_lin.hnc
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
a : A
f : R⟦X⟧
hf : f.IsExponential
d : Fin 2 →₀ ℕ
hd : (d.sum fun x n => n) ≠ 1
hd' : d = Finsupp.single 0 1
⊢ ((Finsupp.single 0 1).sum fun x n => n) = 1

case hp_lin
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
a : A
f : R⟦X⟧
hf : f.IsExponential
⊢ ∀ (d : Fin 2 →₀ ℕ), (d.sum fun x n => n) ≠ 1 → (MvPowerSeries.coeff R d) (MvPowerSeries.X 0 + MvPowerSeries.X 1) = 0

State before:
case hp_lin.hnc
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
a : A
f : R⟦X⟧
hf : f.IsExponential
d : Fin 2 →₀ ℕ
hd : (d.sum fun x n => n) ≠ 1
hd' : d = Finsupp.single 0 1
⊢ ((Finsupp.single 0 1).sum fun x n => n) = 1

case hp_lin
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
a : A
f : R⟦X⟧
hf : f.IsExponential
⊢ ∀ (d : Fin 2 →₀ ℕ), (d.sum fun x n => n) ≠ 1 → (MvPowerSeries.coeff R d) (MvPowerSeries.X 0 + MvPowerSeries.X 1) = 0
Tactic:
simp only [Fin.isValue, Finsupp.sum_single_index]
State after:
case hp_lin
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
a : A
f : R⟦X⟧
hf : f.IsExponential
⊢ ∀ (d : Fin 2 →₀ ℕ), (d.sum fun x n => n) ≠ 1 → (MvPowerSeries.coeff R d) (MvPowerSeries.X 0 + MvPowerSeries.X 1) = 0

State before:
case hp_lin
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
a : A
f : R⟦X⟧
hf : f.IsExponential
d : Fin 2 →₀ ℕ
hd : (d.sum fun x n => n) ≠ 1
⊢ ((if d = Finsupp.single 0 1 then 1 else 0) + if d = Finsupp.single 1 1 then 1 else 0) = 0
Tactic:
split_ifs with h0 h1 h1
State after:
case pos
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
a : A
f : R⟦X⟧
hf : f.IsExponential
d : Fin 2 →₀ ℕ
hd : (d.sum fun x n => n) ≠ 1
h0 : d = Finsupp.single 0 1
h1 : d = Finsupp.single 1 1
⊢ 1 + 1 = 0

case neg
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
a : A
f : R⟦X⟧
hf : f.IsExponential
d : Fin 2 →₀ ℕ
hd : (d.sum fun x n => n) ≠ 1
h0 : d = Finsupp.single 0 1
h1 : ¬d = Finsupp.single 1 1
⊢ 1 + 0 = 0

case pos
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
a : A
f : R⟦X⟧
hf : f.IsExponential
d : Fin 2 →₀ ℕ
hd : (d.sum fun x n => n) ≠ 1
h0 : ¬d = Finsupp.single 0 1
h1 : d = Finsupp.single 1 1
⊢ 0 + 1 = 0

case neg
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
a : A
f : R⟦X⟧
hf : f.IsExponential
d : Fin 2 →₀ ℕ
hd : (d.sum fun x n => n) ≠ 1
h0 : ¬d = Finsupp.single 0 1
h1 : ¬d = Finsupp.single 1 1
⊢ 0 + 0 = 0

State before:
case pos
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
a : A
f : R⟦X⟧
hf : f.IsExponential
d : Fin 2 →₀ ℕ
hd : (d.sum fun x n => n) ≠ 1
h0 : d = Finsupp.single 0 1
h1 : d = Finsupp.single 1 1
⊢ 1 + 1 = 0
Tactic:
rw [h1, Finsupp.single_left_inj (by norm_num)] at h0
State after:
case pos
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
a : A
f : R⟦X⟧
hf : f.IsExponential
d : Fin 2 →₀ ℕ
hd : (d.sum fun x n => n) ≠ 1
h0 : 1 = 0
h1 : d = Finsupp.single 1 1
⊢ 1 + 1 = 0

State before:
case pos
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
a : A
f : R⟦X⟧
hf : f.IsExponential
d : Fin 2 →₀ ℕ
hd : (d.sum fun x n => n) ≠ 1
h0 : 1 = 0
h1 : d = Finsupp.single 1 1
⊢ 1 + 1 = 0
Tactic:
exfalso
State after:
case pos
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
a : A
f : R⟦X⟧
hf : f.IsExponential
d : Fin 2 →₀ ℕ
hd : (d.sum fun x n => n) ≠ 1
h0 : 1 = 0
h1 : d = Finsupp.single 1 1
⊢ False

State before:
case pos
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
a : A
f : R⟦X⟧
hf : f.IsExponential
d : Fin 2 →₀ ℕ
hd : (d.sum fun x n => n) ≠ 1
h0 : 1 = 0
h1 : d = Finsupp.single 1 1
⊢ False
Tactic:
exact one_ne_zero h0
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
a : A
f : R⟦X⟧
hf : f.IsExponential
d : Fin 2 →₀ ℕ
hd : (d.sum fun x n => n) ≠ 1
h0 : Finsupp.single 1 1 = Finsupp.single 0 1
h1 : d = Finsupp.single 1 1
⊢ 1 ≠ 0
Tactic:
norm_num
State after:
no goals

State before:
case neg
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
a : A
f : R⟦X⟧
hf : f.IsExponential
d : Fin 2 →₀ ℕ
hd : (d.sum fun x n => n) ≠ 1
h0 : d = Finsupp.single 0 1
h1 : ¬d = Finsupp.single 1 1
⊢ 1 + 0 = 0
Tactic:
exfalso
State after:
case neg
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
a : A
f : R⟦X⟧
hf : f.IsExponential
d : Fin 2 →₀ ℕ
hd : (d.sum fun x n => n) ≠ 1
h0 : d = Finsupp.single 0 1
h1 : ¬d = Finsupp.single 1 1
⊢ False

State before:
case neg
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
a : A
f : R⟦X⟧
hf : f.IsExponential
d : Fin 2 →₀ ℕ
hd : (d.sum fun x n => n) ≠ 1
h0 : d = Finsupp.single 0 1
h1 : ¬d = Finsupp.single 1 1
⊢ False
Tactic:
apply hd
State after:
case neg
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
a : A
f : R⟦X⟧
hf : f.IsExponential
d : Fin 2 →₀ ℕ
hd : (d.sum fun x n => n) ≠ 1
h0 : d = Finsupp.single 0 1
h1 : ¬d = Finsupp.single 1 1
⊢ (d.sum fun x n => n) = 1

State before:
case neg
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
a : A
f : R⟦X⟧
hf : f.IsExponential
d : Fin 2 →₀ ℕ
hd : (d.sum fun x n => n) ≠ 1
h0 : d = Finsupp.single 0 1
h1 : ¬d = Finsupp.single 1 1
⊢ (d.sum fun x n => n) = 1
Tactic:
simp only [h0, Fin.isValue, Finsupp.sum_single_index]
State after:
no goals

State before:
case pos
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
a : A
f : R⟦X⟧
hf : f.IsExponential
d : Fin 2 →₀ ℕ
hd : (d.sum fun x n => n) ≠ 1
h0 : ¬d = Finsupp.single 0 1
h1 : d = Finsupp.single 1 1
⊢ 0 + 1 = 0
Tactic:
exfalso
State after:
case pos
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
a : A
f : R⟦X⟧
hf : f.IsExponential
d : Fin 2 →₀ ℕ
hd : (d.sum fun x n => n) ≠ 1
h0 : ¬d = Finsupp.single 0 1
h1 : d = Finsupp.single 1 1
⊢ False

State before:
case pos
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
a : A
f : R⟦X⟧
hf : f.IsExponential
d : Fin 2 →₀ ℕ
hd : (d.sum fun x n => n) ≠ 1
h0 : ¬d = Finsupp.single 0 1
h1 : d = Finsupp.single 1 1
⊢ False
Tactic:
apply hd
State after:
case pos
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
a : A
f : R⟦X⟧
hf : f.IsExponential
d : Fin 2 →₀ ℕ
hd : (d.sum fun x n => n) ≠ 1
h0 : ¬d = Finsupp.single 0 1
h1 : d = Finsupp.single 1 1
⊢ (d.sum fun x n => n) = 1

State before:
case pos
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
a : A
f : R⟦X⟧
hf : f.IsExponential
d : Fin 2 →₀ ℕ
hd : (d.sum fun x n => n) ≠ 1
h0 : ¬d = Finsupp.single 0 1
h1 : d = Finsupp.single 1 1
⊢ (d.sum fun x n => n) = 1
Tactic:
simp only [h1, Fin.isValue, Finsupp.sum_single_index]
State after:
no goals

State before:
case neg
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
a : A
f : R⟦X⟧
hf : f.IsExponential
d : Fin 2 →₀ ℕ
hd : (d.sum fun x n => n) ≠ 1
h0 : ¬d = Finsupp.single 0 1
h1 : ¬d = Finsupp.single 1 1
⊢ 0 + 0 = 0
Tactic:
simp only [add_zero]
State after:
no goals