internlm/Lean-Github huggingface dataset:
Theorem: PowerSeries.isExponential_scale_add
Proof 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'
Proof 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
Theorem: PowerSeries.isExponential_scale_add
Proof 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'
Proof 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
Theorem: PowerSeries.isExponential_scale_add
Proof 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'
Proof 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
Theorem: PowerSeries.isExponential_scale_add
Proof 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'
Proof 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
Theorem: PowerSeries.isExponential_scale_add
Proof 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'
Proof 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
Theorem: PowerSeries.isExponential_scale_add
Proof 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]
Proof 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
Theorem: PowerSeries.isExponential_scale_add
Proof 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'
Proof 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)
Theorem: PowerSeries.isExponential_scale_add
Proof 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]
Proof state after:
no goals
Theorem: PowerSeries.isExponential_scale_add
Proof 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
Proof 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
Theorem: PowerSeries.isExponential_scale_add
Proof 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
Proof 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
Theorem: PowerSeries.isExponential_scale_add
Proof 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]
Proof 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
Theorem: PowerSeries.isExponential_scale_add
Proof 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]
Proof state after:
no goals
Theorem: PowerSeries.isExponential_scale_add
Proof 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]
Proof state after:
no goals
Theorem: PowerSeries.isExponential_scale_add
Proof 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]
Proof state after:
no goals
Theorem: PowerSeries.isExponential_scale_add
Proof 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
Proof state after:
no goals
Theorem: PowerSeries.isExponential_scale_add
Proof 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
Proof state after:
no goals
Theorem: PowerSeries.isExponential_scale_add
Proof 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
Proof state after:
no goals
Theorem: PowerSeries.isExponential_scale_add
Proof 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]
Proof 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)
Theorem: PowerSeries.isExponential_scale_add
Proof 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]
Proof state after:
no goals
Theorem: PowerSeries.isExponential_self_mul_neg_eq_one
Proof 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⟧
hf : f.IsExponential
⊢ f * scale (-1) f = 1
Tactic:
convert (isExponential_scale_add (1 : A) (-1 : A) hf).symm
Proof state after:
case h.e'_2.h.e'_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⟧
hf : f.IsExponential
⊢ f = scale 1 f

case h.e'_3
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⟧
hf : f.IsExponential
⊢ 1 = scale (1 + -1) f
Theorem: PowerSeries.isExponential_self_mul_neg_eq_one
Proof state before:
case h.e'_2.h.e'_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⟧
hf : f.IsExponential
⊢ f = scale 1 f
Tactic:
rw [scale_one, id_eq]
Proof state after:
no goals
Theorem: PowerSeries.isExponential_self_mul_neg_eq_one
Proof state before:
case h.e'_3
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⟧
hf : f.IsExponential
⊢ 1 = scale (1 + -1) f
Tactic:
simp only [add_right_neg, scale_zero_apply, hf.constantCoeff, map_one]
Proof state after:
no goals
Theorem: PowerSeries.isExponential_neg_mul_self_eq_one
Proof 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⟧
hf : f.IsExponential
⊢ scale (-1) f * f = 1
Tactic:
rw [mul_comm, isExponential_self_mul_neg_eq_one hf]
Proof state after:
no goals
Theorem: PowerSeries.isExponential_map
Proof 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
f : R⟦X⟧
hf : f.IsExponential
⊢ ((map φ) f).IsExponential
Tactic:
rw [isExponential_iff]
Proof 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
f : R⟦X⟧
hf : f.IsExponential
⊢ (constantCoeff S) ((map φ) f) = 1 ∧
    ∀ (p q : ℕ), ↑((p + q).choose p) * (coeff S (p + q)) ((map φ) f) = (coeff S p) ((map φ) f) * (coeff S q) ((map φ) f)