Theorem: PowerSeries.isExponential_scale_add (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
r s : A
f : R⟦X⟧
hf : f.IsExponential
⊢ scale (r + s) f = scale r f * scale s f
Tactic:
let a : Fin 2 → PowerSeries R
| 0 => r • X
| 1 => s • X
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
r s : A
f : R⟦X⟧
hf : f.IsExponential
a : Fin 2 → R⟦X⟧ :=
  fun x =>
    match x with
    | 0 => r • X
    | 1 => s • X
⊢ scale (r + s) f = scale r f * scale s 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
r s : A
f : R⟦X⟧
hf : f.IsExponential
a : Fin 2 → R⟦X⟧ :=
  fun x =>
    match x with
    | 0 => r • X
    | 1 => s • X
⊢ scale (r + s) f = scale r f * scale s f
Tactic:
have ha : MvPowerSeries.SubstDomain a := by
  apply MvPowerSeries.substDomain_of_constantCoeff_zero
  intro i
  simp only [X, a]
  match i with
  | 0 =>
    rw [MvPowerSeries.constantCoeff_smul, MvPowerSeries.constantCoeff_X, smul_zero]
  | 1 =>
    rw [MvPowerSeries.constantCoeff_smul, MvPowerSeries.constantCoeff_X, smul_zero]
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
r s : A
f : R⟦X⟧
hf : f.IsExponential
a : Fin 2 → R⟦X⟧ :=
  fun x =>
    match x with
    | 0 => r • X
    | 1 => s • X
ha : MvPowerSeries.SubstDomain a
⊢ scale (r + s) f = scale r f * scale s 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
r s : A
f : R⟦X⟧
hf : f.IsExponential
a : Fin 2 → R⟦X⟧ :=
  fun x =>
    match x with
    | 0 => r • X
    | 1 => s • X
ha : MvPowerSeries.SubstDomain a
⊢ scale (r + s) f = scale r f * scale s f
Tactic:
have hf' := congr_arg (MvPowerSeries.subst a) hf.add_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
r s : A
f : R⟦X⟧
hf : f.IsExponential
a : Fin 2 → R⟦X⟧ :=
  fun x =>
    match x with
    | 0 => r • X
    | 1 => s • X
ha : MvPowerSeries.SubstDomain a
hf' :
  MvPowerSeries.subst a (subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f) =
    MvPowerSeries.subst a (subst (MvPowerSeries.X 0) f * subst (MvPowerSeries.X 1) f)
⊢ scale (r + s) f = scale r f * scale s 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
r s : A
f : R⟦X⟧
hf : f.IsExponential
a : Fin 2 → R⟦X⟧ :=
  fun x =>
    match x with
    | 0 => r • X
    | 1 => s • X
ha : MvPowerSeries.SubstDomain a
hf' :
  MvPowerSeries.subst a (subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f) =
    MvPowerSeries.subst a (subst (MvPowerSeries.X 0) f * subst (MvPowerSeries.X 1) f)
⊢ scale (r + s) f = scale r f * scale s f
Tactic:
simp only [PowerSeries.subst] at hf'
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
r s : A
f : R⟦X⟧
hf : f.IsExponential
a : Fin 2 → R⟦X⟧ :=
  fun x =>
    match x with
    | 0 => r • X
    | 1 => s • X
ha : MvPowerSeries.SubstDomain a
hf' :
  MvPowerSeries.subst a (MvPowerSeries.subst (fun x => MvPowerSeries.X 0 + MvPowerSeries.X 1) f) =
    MvPowerSeries.subst a
      (MvPowerSeries.subst (fun x => MvPowerSeries.X 0) f * MvPowerSeries.subst (fun x => MvPowerSeries.X 1) f)
⊢ scale (r + s) f = scale r f * scale s 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
r s : A
f : R⟦X⟧
hf : f.IsExponential
a : Fin 2 → R⟦X⟧ :=
  fun x =>
    match x with
    | 0 => r • X
    | 1 => s • X
ha : MvPowerSeries.SubstDomain a
hf' :
  MvPowerSeries.subst a (MvPowerSeries.subst (fun x => MvPowerSeries.X 0 + MvPowerSeries.X 1) f) =
    MvPowerSeries.subst a
      (MvPowerSeries.subst (fun x => MvPowerSeries.X 0) f * MvPowerSeries.subst (fun x => MvPowerSeries.X 1) f)
⊢ scale (r + s) f = scale r f * scale s f
Tactic:
rw [← MvPowerSeries.coe_substAlgHom ha] at hf'
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
r s : A
f : R⟦X⟧
hf : f.IsExponential
a : Fin 2 → R⟦X⟧ :=
  fun x =>
    match x with
    | 0 => r • X
    | 1 => s • X
ha : MvPowerSeries.SubstDomain a
hf' :
  (MvPowerSeries.substAlgHom ha) (MvPowerSeries.subst (fun x => MvPowerSeries.X 0 + MvPowerSeries.X 1) f) =
    (MvPowerSeries.substAlgHom ha)
      (MvPowerSeries.subst (fun x => MvPowerSeries.X 0) f * MvPowerSeries.subst (fun x => MvPowerSeries.X 1) f)
⊢ scale (r + s) f = scale r f * scale s 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
r s : A
f : R⟦X⟧
hf : f.IsExponential
a : Fin 2 → R⟦X⟧ :=
  fun x =>
    match x with
    | 0 => r • X
    | 1 => s • X
ha : MvPowerSeries.SubstDomain a
hf' :
  (MvPowerSeries.substAlgHom ha) (MvPowerSeries.subst (fun x => MvPowerSeries.X 0 + MvPowerSeries.X 1) f) =
    (MvPowerSeries.substAlgHom ha)
      (MvPowerSeries.subst (fun x => MvPowerSeries.X 0) f * MvPowerSeries.subst (fun x => MvPowerSeries.X 1) f)
⊢ scale (r + s) f = scale r f * scale s f
Tactic:
rw [← MvPowerSeries.coe_substAlgHom (MvPowerSeries.substDomain_of_constantCoeff_zero (by simp))] at hf'
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
r s : A
f : R⟦X⟧
hf : f.IsExponential
a : Fin 2 → R⟦X⟧ :=
  fun x =>
    match x with
    | 0 => r • X
    | 1 => s • X
ha : MvPowerSeries.SubstDomain a
hf' :
  (MvPowerSeries.substAlgHom ha) ((MvPowerSeries.substAlgHom ⋯) f) =
    (MvPowerSeries.substAlgHom ha)
      (MvPowerSeries.subst (fun x => MvPowerSeries.X 0) f * MvPowerSeries.subst (fun x => MvPowerSeries.X 1) f)
⊢ scale (r + s) f = scale r f * scale s 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
r s : A
f : R⟦X⟧
hf : f.IsExponential
a : Fin 2 → R⟦X⟧ :=
  fun x =>
    match x with
    | 0 => r • X
    | 1 => s • X
ha : MvPowerSeries.SubstDomain a
hf' :
  (MvPowerSeries.substAlgHom ha) ((MvPowerSeries.substAlgHom ⋯) f) =
    (MvPowerSeries.substAlgHom ha)
      (MvPowerSeries.subst (fun x => MvPowerSeries.X 0) f * MvPowerSeries.subst (fun x => MvPowerSeries.X 1) f)
⊢ scale (r + s) f = scale r f * scale s f
Tactic:
rw [← MvPowerSeries.coe_substAlgHom (MvPowerSeries.substDomain_of_constantCoeff_zero (by simp))] at hf'
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
r s : A
f : R⟦X⟧
hf : f.IsExponential
a : Fin 2 → R⟦X⟧ :=
  fun x =>
    match x with
    | 0 => r • X
    | 1 => s • X
ha : MvPowerSeries.SubstDomain a
hf' :
  (MvPowerSeries.substAlgHom ha) ((MvPowerSeries.substAlgHom ⋯) f) =
    (MvPowerSeries.substAlgHom ha)
      ((MvPowerSeries.substAlgHom ⋯) f * MvPowerSeries.subst (fun x => MvPowerSeries.X 1) f)
⊢ scale (r + s) f = scale r f * scale s 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
r s : A
f : R⟦X⟧
hf : f.IsExponential
a : Fin 2 → R⟦X⟧ :=
  fun x =>
    match x with
    | 0 => r • X
    | 1 => s • X
ha : MvPowerSeries.SubstDomain a
hf' :
  (MvPowerSeries.substAlgHom ha) ((MvPowerSeries.substAlgHom ⋯) f) =
    (MvPowerSeries.substAlgHom ha)
      ((MvPowerSeries.substAlgHom ⋯) f * MvPowerSeries.subst (fun x => MvPowerSeries.X 1) f)
⊢ scale (r + s) f = scale r f * scale s f
Tactic:
rw [← MvPowerSeries.coe_substAlgHom (MvPowerSeries.substDomain_of_constantCoeff_zero (by simp))] at hf'
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
r s : A
f : R⟦X⟧
hf : f.IsExponential
a : Fin 2 → R⟦X⟧ :=
  fun x =>
    match x with
    | 0 => r • X
    | 1 => s • X
ha : MvPowerSeries.SubstDomain a
hf' :
  (MvPowerSeries.substAlgHom ha) ((MvPowerSeries.substAlgHom ⋯) f) =
    (MvPowerSeries.substAlgHom ha) ((MvPowerSeries.substAlgHom ⋯) f * (MvPowerSeries.substAlgHom ⋯) f)
⊢ scale (r + s) f = scale r f * scale s 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
r s : A
f : R⟦X⟧
hf : f.IsExponential
a : Fin 2 → R⟦X⟧ :=
  fun x =>
    match x with
    | 0 => r • X
    | 1 => s • X
ha : MvPowerSeries.SubstDomain a
hf' :
  (MvPowerSeries.substAlgHom ha) ((MvPowerSeries.substAlgHom ⋯) f) =
    (MvPowerSeries.substAlgHom ha) ((MvPowerSeries.substAlgHom ⋯) f * (MvPowerSeries.substAlgHom ⋯) f)
⊢ scale (r + s) f = scale r f * scale s f
Tactic:
simp only [MvPowerSeries.substAlgHom_comp_substAlgHom_apply, map_mul] at hf'
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
r s : A
f : R⟦X⟧
hf : f.IsExponential
a : Fin 2 → R⟦X⟧ :=
  fun x =>
    match x with
    | 0 => r • X
    | 1 => s • X
ha : MvPowerSeries.SubstDomain a
hf' : (MvPowerSeries.substAlgHom ⋯) f = (MvPowerSeries.substAlgHom ⋯) f * (MvPowerSeries.substAlgHom ⋯) f
⊢ scale (r + s) f = scale r f * scale s 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
r s : A
f : R⟦X⟧
hf : f.IsExponential
a : Fin 2 → R⟦X⟧ :=
  fun x =>
    match x with
    | 0 => r • X
    | 1 => s • X
ha : MvPowerSeries.SubstDomain a
hf' : (MvPowerSeries.substAlgHom ⋯) f = (MvPowerSeries.substAlgHom ⋯) f * (MvPowerSeries.substAlgHom ⋯) f
⊢ scale (r + s) f = scale r f * scale s f
Tactic:
simp only [MvPowerSeries.coe_substAlgHom] at hf'
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
r s : A
f : R⟦X⟧
hf : f.IsExponential
a : Fin 2 → R⟦X⟧ :=
  fun x =>
    match x with
    | 0 => r • X
    | 1 => s • X
ha : MvPowerSeries.SubstDomain a
hf' :
  MvPowerSeries.subst (fun s => MvPowerSeries.subst a (MvPowerSeries.X 0 + MvPowerSeries.X 1)) f =
    MvPowerSeries.subst (fun s => MvPowerSeries.subst a (MvPowerSeries.X 0)) f *
      MvPowerSeries.subst (fun s => MvPowerSeries.subst a (MvPowerSeries.X 1)) f
⊢ scale (r + s) f = scale r f * scale s 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
r s : A
f : R⟦X⟧
hf : f.IsExponential
a : Fin 2 → R⟦X⟧ :=
  fun x =>
    match x with
    | 0 => r • X
    | 1 => s • X
ha : MvPowerSeries.SubstDomain a
hf' :
  MvPowerSeries.subst (fun s => MvPowerSeries.subst a (MvPowerSeries.X 0 + MvPowerSeries.X 1)) f =
    MvPowerSeries.subst (fun s => MvPowerSeries.subst a (MvPowerSeries.X 0)) f *
      MvPowerSeries.subst (fun s => MvPowerSeries.subst a (MvPowerSeries.X 1)) f
⊢ scale (r + s) f = scale r f * scale s f
Tactic:
simp only [scale_eq_subst, 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
r s : A
f : R⟦X⟧
hf : f.IsExponential
a : Fin 2 → R⟦X⟧ :=
  fun x =>
    match x with
    | 0 => r • X
    | 1 => s • X
ha : MvPowerSeries.SubstDomain a
hf' :
  MvPowerSeries.subst (fun s => MvPowerSeries.subst a (MvPowerSeries.X 0 + MvPowerSeries.X 1)) f =
    MvPowerSeries.subst (fun s => MvPowerSeries.subst a (MvPowerSeries.X 0)) f *
      MvPowerSeries.subst (fun s => MvPowerSeries.subst a (MvPowerSeries.X 1)) f
⊢ MvPowerSeries.subst (fun x => (r + s) • X) f =
    MvPowerSeries.subst (fun x => r • X) f * MvPowerSeries.subst (fun x => s • X) 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
r s : A
f : R⟦X⟧
hf : f.IsExponential
a : Fin 2 → R⟦X⟧ :=
  fun x =>
    match x with
    | 0 => r • X
    | 1 => s • X
ha : MvPowerSeries.SubstDomain a
hf' :
  MvPowerSeries.subst (fun s => MvPowerSeries.subst a (MvPowerSeries.X 0 + MvPowerSeries.X 1)) f =
    MvPowerSeries.subst (fun s => MvPowerSeries.subst a (MvPowerSeries.X 0)) f *
      MvPowerSeries.subst (fun s => MvPowerSeries.subst a (MvPowerSeries.X 1)) f
⊢ MvPowerSeries.subst (fun x => (r + s) • X) f =
    MvPowerSeries.subst (fun x => r • X) f * MvPowerSeries.subst (fun x => s • X) f
Tactic:
convert hf'
State after:
case h.e'_2.h.h.e'_8.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
r s : A
f : R⟦X⟧
hf : f.IsExponential
a : Fin 2 → R⟦X⟧ :=
  fun x =>
    match x with
    | 0 => r • X
    | 1 => s • X
ha : MvPowerSeries.SubstDomain a
hf' :
  MvPowerSeries.subst (fun s => MvPowerSeries.subst a (MvPowerSeries.X 0 + MvPowerSeries.X 1)) f =
    MvPowerSeries.subst (fun s => MvPowerSeries.subst a (MvPowerSeries.X 0)) f *
      MvPowerSeries.subst (fun s => MvPowerSeries.subst a (MvPowerSeries.X 1)) f
e_1✝ : R⟦X⟧ = MvPowerSeries Unit R
x✝ : Unit
⊢ (r + s) • X = MvPowerSeries.subst a (MvPowerSeries.X 0 + MvPowerSeries.X 1)

case h.e'_3.h.h.e'_5.h.h.e'_8.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
r s : A
f : R⟦X⟧
hf : f.IsExponential
a : Fin 2 → R⟦X⟧ :=
  fun x =>
    match x with
    | 0 => r • X
    | 1 => s • X
ha : MvPowerSeries.SubstDomain a
hf' :
  MvPowerSeries.subst (fun s => MvPowerSeries.subst a (MvPowerSeries.X 0 + MvPowerSeries.X 1)) f =
    MvPowerSeries.subst (fun s => MvPowerSeries.subst a (MvPowerSeries.X 0)) f *
      MvPowerSeries.subst (fun s => MvPowerSeries.subst a (MvPowerSeries.X 1)) f
e_1✝ : R⟦X⟧ = MvPowerSeries Unit R
x✝ : Unit
⊢ r • X = MvPowerSeries.subst a (MvPowerSeries.X 0)

case h.e'_3.h.h.e'_6.h.h.e'_8.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
r s : A
f : R⟦X⟧
hf : f.IsExponential
a : Fin 2 → R⟦X⟧ :=
  fun x =>
    match x with
    | 0 => r • X
    | 1 => s • X
ha : MvPowerSeries.SubstDomain a
hf' :
  MvPowerSeries.subst (fun s => MvPowerSeries.subst a (MvPowerSeries.X 0 + MvPowerSeries.X 1)) f =
    MvPowerSeries.subst (fun s => MvPowerSeries.subst a (MvPowerSeries.X 0)) f *
      MvPowerSeries.subst (fun s => MvPowerSeries.subst a (MvPowerSeries.X 1)) f
e_1✝ : R⟦X⟧ = MvPowerSeries Unit R
x✝ : Unit
⊢ s • X = MvPowerSeries.subst a (MvPowerSeries.X 1)

State before:
case h.e'_2.h.h.e'_8.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
r s : A
f : R⟦X⟧
hf : f.IsExponential
a : Fin 2 → R⟦X⟧ :=
  fun x =>
    match x with
    | 0 => r • X
    | 1 => s • X
ha : MvPowerSeries.SubstDomain a
hf' :
  MvPowerSeries.subst (fun s => MvPowerSeries.subst a (MvPowerSeries.X 0 + MvPowerSeries.X 1)) f =
    MvPowerSeries.subst (fun s => MvPowerSeries.subst a (MvPowerSeries.X 0)) f *
      MvPowerSeries.subst (fun s => MvPowerSeries.subst a (MvPowerSeries.X 1)) f
e_1✝ : R⟦X⟧ = MvPowerSeries Unit R
x✝ : Unit
⊢ (r + s) • X = MvPowerSeries.subst a (MvPowerSeries.X 0 + MvPowerSeries.X 1)

case h.e'_3.h.h.e'_5.h.h.e'_8.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
r s : A
f : R⟦X⟧
hf : f.IsExponential
a : Fin 2 → R⟦X⟧ :=
  fun x =>
    match x with
    | 0 => r • X
    | 1 => s • X
ha : MvPowerSeries.SubstDomain a
hf' :
  MvPowerSeries.subst (fun s => MvPowerSeries.subst a (MvPowerSeries.X 0 + MvPowerSeries.X 1)) f =
    MvPowerSeries.subst (fun s => MvPowerSeries.subst a (MvPowerSeries.X 0)) f *
      MvPowerSeries.subst (fun s => MvPowerSeries.subst a (MvPowerSeries.X 1)) f
e_1✝ : R⟦X⟧ = MvPowerSeries Unit R
x✝ : Unit
⊢ r • X = MvPowerSeries.subst a (MvPowerSeries.X 0)

case h.e'_3.h.h.e'_6.h.h.e'_8.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
r s : A
f : R⟦X⟧
hf : f.IsExponential
a : Fin 2 → R⟦X⟧ :=
  fun x =>
    match x with
    | 0 => r • X
    | 1 => s • X
ha : MvPowerSeries.SubstDomain a
hf' :
  MvPowerSeries.subst (fun s => MvPowerSeries.subst a (MvPowerSeries.X 0 + MvPowerSeries.X 1)) f =
    MvPowerSeries.subst (fun s => MvPowerSeries.subst a (MvPowerSeries.X 0)) f *
      MvPowerSeries.subst (fun s => MvPowerSeries.subst a (MvPowerSeries.X 1)) f
e_1✝ : R⟦X⟧ = MvPowerSeries Unit R
x✝ : Unit
⊢ s • X = MvPowerSeries.subst a (MvPowerSeries.X 1)
Tactic:
repeat
  simp only [← MvPolynomial.coe_X, ← MvPolynomial.coe_add,
    MvPowerSeries.subst_coe ha]
  simp only [Fin.isValue, map_add, MvPolynomial.aeval_X, add_smul]
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
r s : A
f : R⟦X⟧
hf : f.IsExponential
a : Fin 2 → R⟦X⟧ :=
  fun x =>
    match x with
    | 0 => r • X
    | 1 => s • X
⊢ MvPowerSeries.SubstDomain a
Tactic:
apply MvPowerSeries.substDomain_of_constantCoeff_zero
State after:
case ha
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
r s : A
f : R⟦X⟧
hf : f.IsExponential
a : Fin 2 → R⟦X⟧ :=
  fun x =>
    match x with
    | 0 => r • X
    | 1 => s • X
⊢ ∀ (s : Fin 2), (MvPowerSeries.constantCoeff Unit R) (a s) = 0

State before:
case ha
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
r s : A
f : R⟦X⟧
hf : f.IsExponential
a : Fin 2 → R⟦X⟧ :=
  fun x =>
    match x with
    | 0 => r • X
    | 1 => s • X
⊢ ∀ (s : Fin 2), (MvPowerSeries.constantCoeff Unit R) (a s) = 0
Tactic:
intro i
State after:
case ha
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
r s : A
f : R⟦X⟧
hf : f.IsExponential
a : Fin 2 → R⟦X⟧ :=
  fun x =>
    match x with
    | 0 => r • X
    | 1 => s • X
i : Fin 2
⊢ (MvPowerSeries.constantCoeff Unit R) (a i) = 0

State before:
case ha
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
r s : A
f : R⟦X⟧
hf : f.IsExponential
a : Fin 2 → R⟦X⟧ :=
  fun x =>
    match x with
    | 0 => r • X
    | 1 => s • X
i : Fin 2
⊢ (MvPowerSeries.constantCoeff Unit R) (a i) = 0
Tactic:
simp only [X, a]
State after:
case ha
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
r s : A
f : R⟦X⟧
hf : f.IsExponential
a : Fin 2 → R⟦X⟧ :=
  fun x =>
    match x with
    | 0 => r • X
    | 1 => s • X
i : Fin 2
⊢ (MvPowerSeries.constantCoeff Unit R)
      (match i with
      | 0 => r • MvPowerSeries.X ()
      | 1 => s • MvPowerSeries.X ()) =
    0

State before:
case ha
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
r s : A
f : R⟦X⟧
hf : f.IsExponential
a : Fin 2 → R⟦X⟧ :=
  fun x =>
    match x with
    | 0 => r • X
    | 1 => s • X
i : Fin 2
⊢ (MvPowerSeries.constantCoeff Unit R)
      (match i with
      | 0 => r • MvPowerSeries.X ()
      | 1 => s • MvPowerSeries.X ()) =
    0
Tactic:
match i with
| 0 =>
  rw [MvPowerSeries.constantCoeff_smul, MvPowerSeries.constantCoeff_X, smul_zero]
| 1 =>
  rw [MvPowerSeries.constantCoeff_smul, MvPowerSeries.constantCoeff_X, smul_zero]
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
r s : A
f : R⟦X⟧
hf : f.IsExponential
a : Fin 2 → R⟦X⟧ :=
  fun x =>
    match x with
    | 0 => r • X
    | 1 => s • X
i : Fin 2
⊢ (MvPowerSeries.constantCoeff Unit R)
      (match 0 with
      | 0 => r • MvPowerSeries.X ()
      | 1 => s • MvPowerSeries.X ()) =
    0
Tactic:
rw [MvPowerSeries.constantCoeff_smul, MvPowerSeries.constantCoeff_X, smul_zero]
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
r s : A
f : R⟦X⟧
hf : f.IsExponential
a : Fin 2 → R⟦X⟧ :=
  fun x =>
    match x with
    | 0 => r • X
    | 1 => s • X
i : Fin 2
⊢ (MvPowerSeries.constantCoeff Unit R)
      (match 1 with
      | 0 => r • MvPowerSeries.X ()
      | 1 => s • MvPowerSeries.X ()) =
    0
Tactic:
rw [MvPowerSeries.constantCoeff_smul, MvPowerSeries.constantCoeff_X, smul_zero]
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
r s : A
f : R⟦X⟧
hf : f.IsExponential
a : Fin 2 → R⟦X⟧ :=
  fun x =>
    match x with
    | 0 => r • X
    | 1 => s • X
ha : MvPowerSeries.SubstDomain a
hf' :
  (MvPowerSeries.substAlgHom ha) (MvPowerSeries.subst (fun x => MvPowerSeries.X 0 + MvPowerSeries.X 1) f) =
    (MvPowerSeries.substAlgHom ha)
      (MvPowerSeries.subst (fun x => MvPowerSeries.X 0) f * MvPowerSeries.subst (fun x => MvPowerSeries.X 1) f)
⊢ 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
r s : A
f : R⟦X⟧
hf : f.IsExponential
a : Fin 2 → R⟦X⟧ :=
  fun x =>
    match x with
    | 0 => r • X
    | 1 => s • X
ha : MvPowerSeries.SubstDomain a
hf' :
  (MvPowerSeries.substAlgHom ha) ((MvPowerSeries.substAlgHom ⋯) f) =
    (MvPowerSeries.substAlgHom ha)
      (MvPowerSeries.subst (fun x => MvPowerSeries.X 0) f * MvPowerSeries.subst (fun x => MvPowerSeries.X 1) f)
⊢ Unit → (MvPowerSeries.constantCoeff (Fin 2) R) (MvPowerSeries.X 0) = 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
r s : A
f : R⟦X⟧
hf : f.IsExponential
a : Fin 2 → R⟦X⟧ :=
  fun x =>
    match x with
    | 0 => r • X
    | 1 => s • X
ha : MvPowerSeries.SubstDomain a
hf' :
  (MvPowerSeries.substAlgHom ha) ((MvPowerSeries.substAlgHom ⋯) f) =
    (MvPowerSeries.substAlgHom ha)
      ((MvPowerSeries.substAlgHom ⋯) f * MvPowerSeries.subst (fun x => MvPowerSeries.X 1) f)
⊢ Unit → (MvPowerSeries.constantCoeff (Fin 2) R) (MvPowerSeries.X 1) = 0
Tactic:
simp
State after:
no goals

State before:
case h.e'_3.h.h.e'_6.h.h.e'_8.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
r s : A
f : R⟦X⟧
hf : f.IsExponential
a : Fin 2 → R⟦X⟧ :=
  fun x =>
    match x with
    | 0 => r • X
    | 1 => s • X
ha : MvPowerSeries.SubstDomain a
hf' :
  MvPowerSeries.subst (fun s => MvPowerSeries.subst a (MvPowerSeries.X 0 + MvPowerSeries.X 1)) f =
    MvPowerSeries.subst (fun s => MvPowerSeries.subst a (MvPowerSeries.X 0)) f *
      MvPowerSeries.subst (fun s => MvPowerSeries.subst a (MvPowerSeries.X 1)) f
e_1✝ : R⟦X⟧ = MvPowerSeries Unit R
x✝ : Unit
⊢ s • X = MvPowerSeries.subst a (MvPowerSeries.X 1)
Tactic:
simp only [← MvPolynomial.coe_X, ← MvPolynomial.coe_add,
  MvPowerSeries.subst_coe ha]
State after:
case h.e'_3.h.h.e'_6.h.h.e'_8.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
r s : A
f : R⟦X⟧
hf : f.IsExponential
a : Fin 2 → R⟦X⟧ :=
  fun x =>
    match x with
    | 0 => r • X
    | 1 => s • X
ha : MvPowerSeries.SubstDomain a
hf' :
  MvPowerSeries.subst (fun s => MvPowerSeries.subst a (MvPowerSeries.X 0 + MvPowerSeries.X 1)) f =
    MvPowerSeries.subst (fun s => MvPowerSeries.subst a (MvPowerSeries.X 0)) f *
      MvPowerSeries.subst (fun s => MvPowerSeries.subst a (MvPowerSeries.X 1)) f
e_1✝ : R⟦X⟧ = MvPowerSeries Unit R
x✝ : Unit
⊢ s • X = (MvPolynomial.aeval a) (MvPolynomial.X 1)

State before:
case h.e'_3.h.h.e'_6.h.h.e'_8.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
r s : A
f : R⟦X⟧
hf : f.IsExponential
a : Fin 2 → R⟦X⟧ :=
  fun x =>
    match x with
    | 0 => r • X
    | 1 => s • X
ha : MvPowerSeries.SubstDomain a
hf' :
  MvPowerSeries.subst (fun s => MvPowerSeries.subst a (MvPowerSeries.X 0 + MvPowerSeries.X 1)) f =
    MvPowerSeries.subst (fun s => MvPowerSeries.subst a (MvPowerSeries.X 0)) f *
      MvPowerSeries.subst (fun s => MvPowerSeries.subst a (MvPowerSeries.X 1)) f
e_1✝ : R⟦X⟧ = MvPowerSeries Unit R
x✝ : Unit
⊢ s • X = (MvPolynomial.aeval a) (MvPolynomial.X 1)
Tactic:
simp only [Fin.isValue, map_add, MvPolynomial.aeval_X, add_smul]
State after:
no goals