awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.PowerSeries.Evaluation
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
φ : R →+* S
a : S
inst_2 : UniformSpace R
inst_3 : UniformSpace S
inst_4 : IsUniformAddGroup R
inst_5 : IsTopologicalSemiring R
inst_6 : IsUniformAddGroup S
inst_7 : T2Space S
inst_8 : CompleteSpace S
inst_9 : IsTopologicalRing S
inst_10 : IsLinearTopology S S
hφ : Continuous.{u_1, u_2} (X := R) (Y := S) (⇑φ : (a : R) → S)
ha : HasEval a
f : R⟦X⟧
this :
  HasSum
    (fun (d : Unit →₀ ℕ) ↦
      HMul.hMul (α := S) (β := S)
        ((φ : (a : R) → S) ((MvPowerSeries.coeff d : (a : MvPowerSeries Unit R) → R) f : R) : S)
        (d.prod fun (s : Unit) (e : ℕ) ↦ a ^ e : S))
    (MvPowerSeries.eval₂ φ (fun (x : Unit) ↦ a) f)
d : Unit →₀ ℕ
hd : d ∉ Set.range (Finsupp.single ())
h :
  Eq (α := ℕ) (((Finsupp.single () ((d : (a : Unit) → ℕ) ()) : Unit →₀ ℕ) : (a : Unit) → ℕ) default : ℕ)
    ((d : (a : Unit) → ℕ) default : ℕ)
⊢ Finsupp.single () ((d : (a : Unit) → ℕ) ()) = d

Tactic:
ext
-- Module: Mathlib.RingTheory.PowerSeries.Evaluation
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
φ : R →+* S
a : S
inst_2 : UniformSpace R
inst_3 : UniformSpace S
inst_4 : IsUniformAddGroup R
inst_5 : IsTopologicalSemiring R
inst_6 : IsUniformAddGroup S
inst_7 : T2Space S
inst_8 : CompleteSpace S
inst_9 : IsTopologicalRing S
inst_10 : IsLinearTopology S S
hφ : Continuous.{u_1, u_2} (X := R) (Y := S) (⇑φ : (a : R) → S)
ha : HasEval a
f : R⟦X⟧
this :
  HasSum
    (fun (d : Unit →₀ ℕ) ↦
      HMul.hMul (α := S) (β := S)
        ((φ : (a : R) → S) ((MvPowerSeries.coeff d : (a : MvPowerSeries Unit R) → R) f : R) : S)
        (d.prod fun (s : Unit) (e : ℕ) ↦ a ^ e : S))
    (MvPowerSeries.eval₂ φ (fun (x : Unit) ↦ a) f)
d : Unit →₀ ℕ
hd : d ∉ Set.range (Finsupp.single ())
⊢ Eq (α := ℕ) (((Finsupp.single () ((d : (a : Unit) → ℕ) ()) : Unit →₀ ℕ) : (a : Unit) → ℕ) default : ℕ)
    ((d : (a : Unit) → ℕ) default : ℕ)

Tactic:
simp
-- Module: Mathlib.RingTheory.PowerSeries.Evaluation
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
φ : R →+* S
a : S
inst_2 : UniformSpace R
inst_3 : UniformSpace S
inst_4 : IsUniformAddGroup R
inst_5 : IsTopologicalSemiring R
inst_6 : IsUniformAddGroup S
inst_7 : T2Space S
inst_8 : CompleteSpace S
inst_9 : IsTopologicalRing S
inst_10 : IsLinearTopology S S
hφ : Continuous.{u_1, u_2} (X := R) (Y := S) (⇑φ : (a : R) → S)
ha : HasEval a
f : R⟦X⟧
this :
  HasSum
    (fun (d : Unit →₀ ℕ) ↦
      HMul.hMul (α := S) (β := S)
        ((φ : (a : R) → S) ((MvPowerSeries.coeff d : (a : MvPowerSeries Unit R) → R) f : R) : S)
        (d.prod fun (s : Unit) (e : ℕ) ↦ a ^ e : S))
    (MvPowerSeries.eval₂ φ (fun (x : Unit) ↦ a) f)
d : Unit →₀ ℕ
hd : d ∉ Set.range (Finsupp.single ())
⊢ HMul.hMul (α := S) (β := S) ((φ : (a : R) → S) ((MvPowerSeries.coeff d : (a : MvPowerSeries Unit R) → R) f : R) : S)
      (d.prod fun (s : Unit) (e : ℕ) ↦ a ^ e : S) =
    0

Tactic:
exact False.elim (hd ⟨d (), by ext; simp⟩)

Premises used: Unit.unit, False.elim, Exists.intro, DFunLike.coe
-- Module: Mathlib.RingTheory.PowerSeries.Evaluation
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
φ : R →+* S
a : S
inst_2 : UniformSpace R
inst_3 : UniformSpace S
inst_4 : IsUniformAddGroup R
inst_5 : IsTopologicalSemiring R
inst_6 : IsUniformAddGroup S
inst_7 : T2Space S
inst_8 : CompleteSpace S
inst_9 : IsTopologicalRing S
inst_10 : IsLinearTopology S S
hφ : Continuous.{u_1, u_2} (X := R) (Y := S) (⇑φ : (a : R) → S)
ha : HasEval a
f : R⟦X⟧
⊢ eval₂ φ a f = ∑' (d : ℕ), HMul.hMul (α := S) ((φ : (a : R) → S) ((coeff d : (a : R⟦X⟧) → R) f : R) : S) (a ^ d)

Tactic:
(hasSum_eval₂ hφ ha f).tsum_eq.symm

Premises used: HasSum.tsum_eq, Eq.symm, PowerSeries.hasSum_eval₂
-- Module: Mathlib.RingTheory.PowerSeries.Evaluation
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
φ : R →+* S
a : S
inst_2 : UniformSpace R
inst_3 : UniformSpace S
inst_4 : IsUniformAddGroup R
inst_5 : IsTopologicalSemiring R
inst_6 : IsUniformAddGroup S
inst_7 : T2Space S
inst_8 : CompleteSpace S
inst_9 : IsTopologicalRing S
inst_10 : IsLinearTopology S S
hφ : Continuous.{u_1, u_2} (X := R) (Y := S) (⇑φ : (a : R) → S)
ha : HasEval a
ε : R⟦X⟧ → S
hε : Continuous ε
h : ∀ (p : Polynomial R), ε (↑p : R⟦X⟧) = Polynomial.eval₂ φ a p
⊢ ε = eval₂ φ a

Tactic:
MvPowerSeries.eval₂_unique hφ (hasEval ha) hε (fun p ↦ ?_)

Premises used: PowerSeries.eval₂, MvPowerSeries.eval₂_unique, PowerSeries.hasEval
-- Module: Mathlib.RingTheory.PowerSeries.Evaluation
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
φ : R →+* S
a : S
inst_2 : UniformSpace R
inst_3 : UniformSpace S
inst_4 : IsUniformAddGroup R
inst_5 : IsTopologicalSemiring R
inst_6 : IsUniformAddGroup S
inst_7 : T2Space S
inst_8 : CompleteSpace S
inst_9 : IsTopologicalRing S
inst_10 : IsLinearTopology S S
hφ : Continuous.{u_1, u_2} (X := R) (Y := S) (⇑φ : (a : R) → S)
ha : HasEval a
ε : R⟦X⟧ → S
hε : Continuous ε
h : ∀ (p : Polynomial R), ε (↑p : R⟦X⟧) = Polynomial.eval₂ φ a p
refine : ∀ (p : MvPolynomial Unit R), ε (↑p : MvPowerSeries Unit R) = MvPolynomial.eval₂ φ (fun (x : Unit) ↦ a) p
⊢ ε = eval₂ φ a

Tactic:
refine MvPowerSeries.eval₂_unique hφ (hasEval ha) hε (fun p ↦ ?_)

Premises used: MvPowerSeries.eval₂_unique, PowerSeries.hasEval
-- Module: Mathlib.RingTheory.PowerSeries.Evaluation
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
φ : R →+* S
a : S
inst_2 : UniformSpace R
inst_3 : UniformSpace S
inst_4 : IsUniformAddGroup R
inst_5 : IsTopologicalSemiring R
inst_6 : IsUniformAddGroup S
inst_7 : T2Space S
inst_8 : CompleteSpace S
inst_9 : IsTopologicalRing S
inst_10 : IsLinearTopology S S
hφ : Continuous.{u_1, u_2} (X := R) (Y := S) (⇑φ : (a : R) → S)
ha : HasEval a
ε : R⟦X⟧ → S
hε : Continuous ε
h : ∀ (p : Polynomial R), ε (↑p : R⟦X⟧) = Polynomial.eval₂ φ a p
p : MvPolynomial Unit R
rw :
  ε (↑((MvPolynomial.uniqueAlgEquiv R PUnit.{1} : (a : MvPolynomial PUnit.{1} R) → Polynomial R) p) : R⟦X⟧) =
    MvPolynomial.eval₂ φ (fun (x : Unit) ↦ a) p
rw₁ :
  Polynomial.eval₂ φ a ((MvPolynomial.uniqueAlgEquiv R PUnit.{1} : (a : MvPolynomial PUnit.{1} R) → Polynomial R) p) =
    MvPolynomial.eval₂ φ (fun (x : Unit) ↦ a) p
rw₂ rw₃ :
  Polynomial.eval₂ φ a ((MvPolynomial.uniqueAlgEquiv R PUnit.{1} : (a : MvPolynomial PUnit.{1} R) → Polynomial R) p) =
    Polynomial.eval₂ φ a ((MvPolynomial.uniqueAlgEquiv R Unit : (a : MvPolynomial Unit R) → Polynomial R) p)
⊢ ε (↑p : MvPowerSeries Unit R) = MvPolynomial.eval₂ φ (fun (x : Unit) ↦ a) p

Tactic:
rw [MvPolynomial.toMvPowerSeries_pUnitAlgEquiv, h, ← MvPolynomial.eval₂_uniqueAlgEquiv]

Premises used: MvPolynomial.eval₂_uniqueAlgEquiv, MvPolynomial.toMvPowerSeries_pUnitAlgEquiv
-- Module: Mathlib.RingTheory.PowerSeries.Evaluation
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
φ : R →+* S
a : S
inst_2 : UniformSpace R
inst_3 : UniformSpace S
inst_4 : IsUniformAddGroup R
inst_5 : IsTopologicalSemiring R
inst_6 : IsUniformAddGroup S
inst_7 : T2Space S
inst_8 : CompleteSpace S
inst_9 : IsTopologicalRing S
inst_10 : IsLinearTopology S S
hφ : Continuous.{u_1, u_2} (X := R) (Y := S) (⇑φ : (a : R) → S)
ha : HasEval a
T : Type u_3
inst_11 : UniformSpace T
inst_12 : CompleteSpace T
inst_13 : T2Space T
inst_14 : CommRing T
inst_15 : IsTopologicalRing T
inst_16 : IsLinearTopology T T
inst_17 : IsUniformAddGroup T
ε : S →+* T
hε : Continuous.{u_2, u_3} (X := S) (Y := T) (⇑ε : (a : S) → T)
⊢ Continuous.{u_1, u_3} (X := R) (Y := T) (⇑(ε.comp φ) : (a : R) → T)

Tactic:
simp only [RingHom.coe_comp, hε.comp hφ]

Premises used: Continuous.comp, RingHom.coe_comp
-- Module: Mathlib.RingTheory.PowerSeries.Evaluation
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
φ : R →+* S
a : S
inst_2 : UniformSpace R
inst_3 : UniformSpace S
inst_4 : IsUniformAddGroup R
inst_5 : IsTopologicalSemiring R
inst_6 : IsUniformAddGroup S
inst_7 : T2Space S
inst_8 : CompleteSpace S
inst_9 : IsTopologicalRing S
inst_10 : IsLinearTopology S S
hφ : Continuous.{u_1, u_2} (X := R) (Y := S) (⇑φ : (a : R) → S)
ha : HasEval a
T : Type u_3
inst_11 : UniformSpace T
inst_12 : CompleteSpace T
inst_13 : T2Space T
inst_14 : CommRing T
inst_15 : IsTopologicalRing T
inst_16 : IsLinearTopology T T
inst_17 : IsUniformAddGroup T
ε : S →+* T
hε : Continuous.{u_2, u_3} (X := S) (Y := T) (⇑ε : (a : S) → T)
refine :
  ∀ (p : Polynomial R),
    ((⇑ε : (a : S) → T) ∘ eval₂ φ a) (↑p : R⟦X⟧) = Polynomial.eval₂ (ε.comp φ) ((ε : (a : S) → T) a) p
⊢ (⇑ε : (a : S) → T) ∘ eval₂ φ a = eval₂ (ε.comp φ) ((ε : (a : S) → T) a)

Tactic:
refine eval₂_unique (by simp only [RingHom.coe_comp, hε.comp hφ]) (ha.map hε)
    (hε.comp (continuous_eval₂ hφ ha)) (fun p ↦ ?_)

Premises used: Continuous.comp, PowerSeries.continuous_eval₂, PowerSeries.HasEval.map, PowerSeries.eval₂_unique
-- Module: Mathlib.RingTheory.PowerSeries.Evaluation
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
φ : R →+* S
a : S
inst_2 : UniformSpace R
inst_3 : UniformSpace S
inst_4 : IsUniformAddGroup R
inst_5 : IsTopologicalSemiring R
inst_6 : IsUniformAddGroup S
inst_7 : T2Space S
inst_8 : CompleteSpace S
inst_9 : IsTopologicalRing S
inst_10 : IsLinearTopology S S
hφ : Continuous.{u_1, u_2} (X := R) (Y := S) (⇑φ : (a : R) → S)
ha : HasEval a
T : Type u_3
inst_11 : UniformSpace T
inst_12 : CompleteSpace T
inst_13 : T2Space T
inst_14 : CommRing T
inst_15 : IsTopologicalRing T
inst_16 : IsLinearTopology T T
inst_17 : IsUniformAddGroup T
ε : S →+* T
hε : Continuous.{u_2, u_3} (X := S) (Y := T) (⇑ε : (a : S) → T)
p : Polynomial R
⊢ ((⇑ε : (a : S) → T) ∘ eval₂ φ a) (↑p : R⟦X⟧) = Polynomial.eval₂ (ε.comp φ) ((ε : (a : S) → T) a) p

Tactic:
simpa [Function.comp_apply, eval₂_coe] using p.hom_eval₂ φ ε a

Premises used: PowerSeries.eval₂_coe, Polynomial.hom_eval₂, Function.comp_apply
-- Module: Mathlib.RingTheory.PowerSeries.Evaluation
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
a : S
inst_2 : UniformSpace R
inst_3 : UniformSpace S
inst_4 : IsUniformAddGroup R
inst_5 : IsTopologicalSemiring R
inst_6 : IsUniformAddGroup S
inst_7 : T2Space S
inst_8 : CompleteSpace S
inst_9 : IsTopologicalRing S
inst_10 : IsLinearTopology S S
inst_11 : Algebra R S
inst_12 : ContinuousSMul R S
ha : HasEval a
⊢ (⇑(aeval ha) : (a : R⟦X⟧) → S) = eval₂ (algebraMap R S) a

Tactic:
MvPowerSeries.coe_aeval (hasEval ha)

Premises used: PowerSeries.eval₂, MvPowerSeries.coe_aeval, PowerSeries.hasEval
-- Module: Mathlib.RingTheory.PowerSeries.Evaluation
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
a : S
inst_2 : UniformSpace R
inst_3 : UniformSpace S
inst_4 : IsUniformAddGroup R
inst_5 : IsTopologicalSemiring R
inst_6 : IsUniformAddGroup S
inst_7 : T2Space S
inst_8 : CompleteSpace S
inst_9 : IsTopologicalRing S
inst_10 : IsLinearTopology S S
inst_11 : Algebra R S
inst_12 : ContinuousSMul R S
ha : HasEval a
⊢ Continuous.{u_1, u_2} (X := R⟦X⟧) (Y := S) (⇑(aeval ha) : (a : R⟦X⟧) → S)

Tactic:
MvPowerSeries.continuous_aeval (hasEval ha)

Premises used: MvPowerSeries.continuous_aeval, PowerSeries.hasEval
-- Module: Mathlib.RingTheory.PowerSeries.Evaluation
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
a : S
inst_2 : UniformSpace R
inst_3 : UniformSpace S
inst_4 : IsUniformAddGroup R
inst_5 : IsTopologicalSemiring R
inst_6 : IsUniformAddGroup S
inst_7 : T2Space S
inst_8 : CompleteSpace S
inst_9 : IsTopologicalRing S
inst_10 : IsLinearTopology S S
inst_11 : Algebra R S
inst_12 : ContinuousSMul R S
ha : HasEval a
p : Polynomial R
rw : eval₂ (algebraMap R S) a (↑p : R⟦X⟧) = (Polynomial.aeval a : (a : Polynomial R) → S) p
rw₁ : eval₂ (algebraMap R S) a (↑p : R⟦X⟧) = Polynomial.eval₂ (algebraMap R S) a p
rw₂ rw₃ : Polynomial.eval₂ (algebraMap R S) a p = Polynomial.eval₂ (algebraMap R S) a p
⊢ Eq.{u_2 + 1} (α := S) ((aeval ha : (a : R⟦X⟧) → S) (↑p : R⟦X⟧) : S)
    ((Polynomial.aeval a : (a : Polynomial R) → S) p : S)

Tactic:
rw [coe_aeval, Polynomial.aeval_def, eval₂_coe]

Premises used: PowerSeries.eval₂_coe, Polynomial.aeval_def, PowerSeries.coe_aeval
-- Module: Mathlib.RingTheory.PowerSeries.Evaluation
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : UniformSpace R
inst_3 : UniformSpace S
inst_4 : IsUniformAddGroup R
inst_5 : IsTopologicalSemiring R
inst_6 : IsUniformAddGroup S
inst_7 : T2Space S
inst_8 : CompleteSpace S
inst_9 : IsTopologicalRing S
inst_10 : IsLinearTopology S S
inst_11 : Algebra R S
inst_12 : ContinuousSMul R S
ε : R⟦X⟧ →ₐ[R] S
hε : Continuous.{u_1, u_2} (X := R⟦X⟧) (Y := S) (⇑ε : (a : R⟦X⟧) → S)
⊢ aeval (a := (ε.toRingHom : (a : R⟦X⟧) → S) X) ⋯ = ε

Tactic:
MvPowerSeries.aeval_unique hε

Premises used: PowerSeries.X, PowerSeries.aeval, MvPowerSeries.aeval_unique
-- Module: Mathlib.RingTheory.PowerSeries.Evaluation
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
a : S
inst_2 : UniformSpace R
inst_3 : UniformSpace S
inst_4 : IsUniformAddGroup R
inst_5 : IsTopologicalSemiring R
inst_6 : IsUniformAddGroup S
inst_7 : T2Space S
inst_8 : CompleteSpace S
inst_9 : IsTopologicalRing S
inst_10 : IsLinearTopology S S
inst_11 : Algebra R S
inst_12 : ContinuousSMul R S
ha : HasEval a
f : R⟦X⟧
simp_rw :
  HasSum
    (fun (d : ℕ) ↦ HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) ((coeff d : (a : R⟦X⟧) → R) f : R) : S) (a ^ d))
    (eval₂ (algebraMap R S) a f)
⊢ HasSum.{u_2, 0} (α := S) (fun (d : ℕ) ↦ HSMul.hSMul (α := R) ((coeff d : (a : R⟦X⟧) → R) f : R) (a ^ d))
    ((aeval ha : (a : R⟦X⟧) → S) f : S)

Tactic:
simp_rw [coe_aeval, ← algebraMap_smul (R := R) S, smul_eq_mul]

Premises used: algebraMap_smul, PowerSeries.coe_aeval, smul_eq_mul
-- Module: Mathlib.RingTheory.PowerSeries.Evaluation
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
a : S
inst_2 : UniformSpace R
inst_3 : UniformSpace S
inst_4 : IsUniformAddGroup R
inst_5 : IsTopologicalSemiring R
inst_6 : IsUniformAddGroup S
inst_7 : T2Space S
inst_8 : CompleteSpace S
inst_9 : IsTopologicalRing S
inst_10 : IsLinearTopology S S
inst_11 : Algebra R S
inst_12 : ContinuousSMul R S
ha : HasEval a
f : R⟦X⟧
⊢ HasSum
    (fun (d : ℕ) ↦ HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) ((coeff d : (a : R⟦X⟧) → R) f : R) : S) (a ^ d))
    (eval₂ (algebraMap R S) a f)

Tactic:
hasSum_eval₂ (continuous_algebraMap R S) ha f

Premises used: continuous_algebraMap, PowerSeries.hasSum_eval₂
-- Module: Mathlib.RingTheory.PowerSeries.Evaluation
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
a : S
inst_2 : UniformSpace R
inst_3 : UniformSpace S
inst_4 : IsUniformAddGroup R
inst_5 : IsTopologicalSemiring R
inst_6 : IsUniformAddGroup S
inst_7 : T2Space S
inst_8 : CompleteSpace S
inst_9 : IsTopologicalRing S
inst_10 : IsLinearTopology S S
inst_11 : Algebra R S
inst_12 : ContinuousSMul R S
ha : HasEval a
f : R⟦X⟧
⊢ HasSum
    (fun (d : ℕ) ↦ HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) ((coeff d : (a : R⟦X⟧) → R) f : R) : S) (a ^ d))
    (eval₂ (algebraMap R S) a f)

Tactic:
exact hasSum_eval₂ (continuous_algebraMap R S) ha f

Premises used: continuous_algebraMap, PowerSeries.hasSum_eval₂
-- Module: Mathlib.RingTheory.PowerSeries.Evaluation
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
a : S
inst_2 : UniformSpace R
inst_3 : UniformSpace S
inst_4 : IsUniformAddGroup R
inst_5 : IsTopologicalSemiring R
inst_6 : IsUniformAddGroup S
inst_7 : T2Space S
inst_8 : CompleteSpace S
inst_9 : IsTopologicalRing S
inst_10 : IsLinearTopology S S
inst_11 : Algebra R S
inst_12 : ContinuousSMul R S
ha : HasEval a
f : R⟦X⟧
⊢ Eq.{u_2 + 1} (α := S) ((aeval ha : (a : R⟦X⟧) → S) f : S)
    (∑' (d : ℕ), HSMul.hSMul (α := R) ((coeff d : (a : R⟦X⟧) → R) f : R) (a ^ d) : S)

Tactic:
(hasSum_aeval ha f).tsum_eq.symm

Premises used: PowerSeries.hasSum_aeval, HasSum.tsum_eq, Eq.symm
-- Module: Mathlib.RingTheory.PowerSeries.Evaluation
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
a : S
inst_2 : UniformSpace R
inst_3 : UniformSpace S
inst_4 : IsUniformAddGroup R
inst_5 : IsTopologicalSemiring R
inst_6 : IsUniformAddGroup S
inst_7 : T2Space S
inst_8 : CompleteSpace S
inst_9 : IsTopologicalRing S
inst_10 : IsLinearTopology S S
inst_11 : Algebra R S
inst_12 : ContinuousSMul R S
ha : HasEval a
T : Type u_3
inst_13 : CommRing T
inst_14 : UniformSpace T
inst_15 : IsUniformAddGroup T
inst_16 : IsTopologicalRing T
inst_17 : IsLinearTopology T T
inst_18 : T2Space T
inst_19 : Algebra R T
inst_20 : ContinuousSMul R T
inst_21 : CompleteSpace T
ε : S →ₐ[R] T
hε : Continuous.{u_2, u_3} (X := S) (Y := T) (⇑ε : (a : S) → T)
⊢ ε.comp (aeval ha) = aeval ⋯

Tactic:
MvPowerSeries.comp_aeval (hasEval ha) hε

Premises used: MvPowerSeries.comp_aeval, PowerSeries.aeval, PowerSeries.hasEval
-- Module: Mathlib.RingTheory.PowerSeries.Exp
Goal:
A : Type u_1
inst : Ring A
inst_1 : Algebra ℚ A
n : ℕ
⊢ Eq (α := A) ((coeff n : (a : A⟦X⟧) → A) (exp A) : A)
    ((algebraMap ℚ A : (a : ℚ) → A) (HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ)) : A)

Tactic:
coeff_mk _ _

Premises used: PowerSeries.coeff_mk, PowerSeries.exp
-- Module: Mathlib.RingTheory.PowerSeries.Exp
Goal:
A : Type u_1
inst : Ring A
inst_1 : Algebra ℚ A
rw : Eq (α := A) ((algebraMap ℚ A : (a : ℚ) → A) (HDiv.hDiv (α := ℚ) 1 (↑0! : ℚ)) : A) (1 : A)
⊢ Eq (α := A) ((constantCoeff : (a : A⟦X⟧) → A) (exp A) : A) (1 : A)

Tactic:
rw [← coeff_zero_eq_constantCoeff_apply, coeff_exp]

Premises used: PowerSeries.coeff_exp, PowerSeries.coeff_zero_eq_constantCoeff_apply
-- Module: Mathlib.RingTheory.PowerSeries.Exp
Goal:
A : Type u_1
inst : Ring A
inst_1 : Algebra ℚ A
⊢ Eq (α := A) ((algebraMap ℚ A : (a : ℚ) → A) (HDiv.hDiv (α := ℚ) 1 (↑0! : ℚ)) : A) (1 : A)

Tactic:
simp
-- Module: Mathlib.RingTheory.PowerSeries.Exp
Goal:
A : Type u_1
A' : Type u_2
inst : Ring A
inst_1 : Ring A'
inst_2 : Algebra ℚ A
inst_3 : Algebra ℚ A'
f : A →+* A'
h :
  ∀ (n : ℕ),
    Eq.{u_2 + 1} (α := A') ((coeff n : (a : A'⟦X⟧) → A') ((map f : (a : A⟦X⟧) → A'⟦X⟧) (exp A) : A'⟦X⟧) : A')
      ((coeff n : (a : A'⟦X⟧) → A') (exp A') : A')
⊢ (map f : (a : A⟦X⟧) → A'⟦X⟧) (exp A) = exp A'

Tactic:
ext
-- Module: Mathlib.RingTheory.PowerSeries.Exp
Goal:
A : Type u_1
A' : Type u_2
inst : Ring A
inst_1 : Ring A'
inst_2 : Algebra ℚ A
inst_3 : Algebra ℚ A'
f : A →+* A'
n : ℕ
⊢ Eq.{u_2 + 1} (α := A') ((coeff n : (a : A'⟦X⟧) → A') ((map f : (a : A⟦X⟧) → A'⟦X⟧) (exp A) : A'⟦X⟧) : A')
    ((coeff n : (a : A'⟦X⟧) → A') (exp A') : A')

Tactic:
simp
-- Module: Mathlib.RingTheory.PowerSeries.Exp
Goal:
A : Type u_3
inst : CommRing A
inst_1 : Algebra ℚ A
h :
  ∀ (n : ℕ),
    Eq (α := A) ((coeff n : (a : A⟦X⟧) → A) ((d⁄dX A : (a : A⟦X⟧) → A⟦X⟧) (exp A) : A⟦X⟧) : A)
      ((coeff n : (a : A⟦X⟧) → A) (exp A) : A)
⊢ (d⁄dX A : (a : A⟦X⟧) → A⟦X⟧) (exp A) = exp A

Tactic:
ext n
-- Module: Mathlib.RingTheory.PowerSeries.Exp
Goal:
A : Type u_3
inst : CommRing A
inst_1 : Algebra ℚ A
n : ℕ
h :
  HMul.hMul (α := A) ((algebraMap ℚ A : (a : ℚ) → A) (HDiv.hDiv (α := ℚ) 1 (↑(n + 1)! : ℚ)) : A)
      (HAdd.hAdd (α := A) (↑n : A) 1) =
    (algebraMap ℚ A : (a : ℚ) → A) (HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ))
⊢ Eq (α := A) ((coeff n : (a : A⟦X⟧) → A) ((d⁄dX A : (a : A⟦X⟧) → A⟦X⟧) (exp A) : A⟦X⟧) : A)
    ((coeff n : (a : A⟦X⟧) → A) (exp A) : A)

Tactic:
rw [coeff_derivative, coeff_exp, coeff_exp]

Premises used: PowerSeries.coeff_exp, PowerSeries.coeff_derivative
-- Module: Mathlib.RingTheory.PowerSeries.Exp
Goal:
A : Type u_3
inst : CommRing A
inst_1 : Algebra ℚ A
n : ℕ
rw :
  HAdd.hAdd (α := A) (↑n : A) 1 =
    HAdd.hAdd (α := A) (β := A) ((algebraMap ℚ A : (a : ℚ) → A) (↑n : ℚ) : A) ((algebraMap ℚ A : (a : ℚ) → A) 1 : A)
rw₁ : HAdd.hAdd (α := A) (↑n : A) 1 = HAdd.hAdd (α := A) (β := A) ((↑n : A) : A) ((algebraMap ℚ A : (a : ℚ) → A) 1 : A)
rw₂ rw₃ : HAdd.hAdd (α := A) (↑n : A) 1 = HAdd.hAdd (α := A) (↑n : A) 1
⊢ HAdd.hAdd (α := A) (↑n : A) 1 = (algebraMap ℚ A : (a : ℚ) → A) (HAdd.hAdd (α := ℚ) (↑n : ℚ) 1)

Tactic:
rw [map_add, map_natCast, map_one]

Premises used: map_add, map_natCast, map_one
-- Module: Mathlib.RingTheory.PowerSeries.Exp
Goal:
A : Type u_3
inst : CommRing A
inst_1 : Algebra ℚ A
n : ℕ
⊢ HAdd.hAdd (α := A) (↑n : A) 1 = (algebraMap ℚ A : (a : ℚ) → A) (HAdd.hAdd (α := ℚ) (↑n : ℚ) 1)

Tactic:
have key : (n + 1 : A) = algebraMap ℚ A (n + 1) := by
    rw [map_add, map_natCast, map_one]
-- Module: Mathlib.RingTheory.PowerSeries.Exp
Goal:
A : Type u_3
inst : CommRing A
inst_1 : Algebra ℚ A
n : ℕ
key : HAdd.hAdd (α := A) (↑n : A) 1 = (algebraMap ℚ A : (a : ℚ) → A) (HAdd.hAdd (α := ℚ) (↑n : ℚ) 1)
h :
  Eq (α := A)
    ((algebraMap ℚ A : (a : ℚ) → A) (1 / (HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 * (↑n ! : ℚ)) * HAdd.hAdd (α := ℚ) (↑n : ℚ) 1) :
      A)
    ((algebraMap ℚ A : (a : ℚ) → A) (HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ)) : A)
⊢ HMul.hMul (α := A) ((algebraMap ℚ A : (a : ℚ) → A) (HDiv.hDiv (α := ℚ) 1 (↑(n + 1)! : ℚ)) : A)
      (HAdd.hAdd (α := A) (↑n : A) 1) =
    (algebraMap ℚ A : (a : ℚ) → A) (HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ))

Tactic:
rw [key, ← map_mul, factorial_succ, Nat.cast_mul, Nat.cast_add_one]

Premises used: Nat.factorial_succ, map_mul, Nat.cast_mul, Nat.cast_add_one
-- Module: Mathlib.RingTheory.PowerSeries.Exp
Goal:
A : Type u_3
inst : CommRing A
inst_1 : Algebra ℚ A
n : ℕ
key : HAdd.hAdd (α := A) (↑n : A) 1 = (algebraMap ℚ A : (a : ℚ) → A) (HAdd.hAdd (α := ℚ) (↑n : ℚ) 1)
h : 1 / (HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 * (↑n ! : ℚ)) * HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 = HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ)
⊢ Eq (α := A)
    ((algebraMap ℚ A : (a : ℚ) → A) (1 / (HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 * (↑n ! : ℚ)) * HAdd.hAdd (α := ℚ) (↑n : ℚ) 1) :
      A)
    ((algebraMap ℚ A : (a : ℚ) → A) (HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ)) : A)

Tactic:
congr 1
-- Module: Mathlib.RingTheory.PowerSeries.Exp
Goal:
A : Type u_3
inst : CommRing A
inst_1 : Algebra ℚ A
n : ℕ
key : HAdd.hAdd (α := A) (↑n : A) 1 = (algebraMap ℚ A : (a : ℚ) → A) (HAdd.hAdd (α := ℚ) (↑n : ℚ) 1)
⊢ 1 / (HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 * (↑n ! : ℚ)) * HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 = HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ)

Tactic:
field_simp
-- Module: Mathlib.RingTheory.PowerSeries.Exp
Goal:
A : Type u_3
inst : CommRing A
inst_1 : Algebra ℚ A
inst_2 : IsAddTorsionFree A
f : A⟦X⟧
hd : (d⁄dX A : (a : A⟦X⟧) → A⟦X⟧) f = f
hc : Eq (α := A) ((constantCoeff : (a : A⟦X⟧) → A) f : A) (1 : A)
h : ∀ (n : ℕ), Eq (α := A) ((coeff n : (a : A⟦X⟧) → A) f : A) ((coeff n : (a : A⟦X⟧) → A) (exp A) : A)
⊢ f = exp A

Tactic:
ext n
-- Module: Mathlib.RingTheory.PowerSeries.Exp
Goal:
A : Type u_3
inst : CommRing A
inst_1 : Algebra ℚ A
inst_2 : IsAddTorsionFree A
f : A⟦X⟧
hd : (d⁄dX A : (a : A⟦X⟧) → A⟦X⟧) f = f
hc : Eq (α := A) ((constantCoeff : (a : A⟦X⟧) → A) f : A) (1 : A)
h : Eq (α := A) ((constantCoeff : (a : A⟦X⟧) → A) f : A) ((constantCoeff : (a : A⟦X⟧) → A) (exp A) : A)
h₁ : Eq (α := A) (1 : A) ((constantCoeff : (a : A⟦X⟧) → A) (exp A) : A)
h₂ h₃ : Eq.{u_3 + 1} (α := A) 1 1
⊢ Eq (α := A) ((coeff 0 : (a : A⟦X⟧) → A) f : A) ((coeff 0 : (a : A⟦X⟧) → A) (exp A) : A)

Tactic:
rw [coeff_zero_eq_constantCoeff, hc, constantCoeff_exp]

Premises used: PowerSeries.coeff_zero_eq_constantCoeff, PowerSeries.constantCoeff_exp
-- Module: Mathlib.RingTheory.PowerSeries.Exp
Goal:
A : Type u_3
inst : CommRing A
inst_1 : Algebra ℚ A
inst_2 : IsAddTorsionFree A
f : A⟦X⟧
hd : (d⁄dX A : (a : A⟦X⟧) → A⟦X⟧) f = f
hc : Eq (α := A) ((constantCoeff : (a : A⟦X⟧) → A) f : A) (1 : A)
n : ℕ
ih : Eq (α := A) ((coeff n : (a : A⟦X⟧) → A) f : A) ((coeff n : (a : A⟦X⟧) → A) (exp A) : A)
⊢ Eq (α := A) ((coeff n : (a : A⟦X⟧) → A) ((d⁄dX A : (a : A⟦X⟧) → A⟦X⟧) f : A⟦X⟧) : A)
    ((coeff n : (a : A⟦X⟧) → A) f : A)

Tactic:
have eq1 : coeff n (d⁄dX A f) = coeff n f := congrArg (coeff n) hd
-- Module: Mathlib.RingTheory.PowerSeries.Exp
Goal:
A : Type u_3
inst : CommRing A
inst_1 : Algebra ℚ A
inst_2 : IsAddTorsionFree A
f : A⟦X⟧
hd : (d⁄dX A : (a : A⟦X⟧) → A⟦X⟧) f = f
hc : Eq (α := A) ((constantCoeff : (a : A⟦X⟧) → A) f : A) (1 : A)
n : ℕ
ih : Eq (α := A) ((coeff n : (a : A⟦X⟧) → A) f : A) ((coeff n : (a : A⟦X⟧) → A) (exp A) : A)
eq1 :
  Eq (α := A) ((coeff n : (a : A⟦X⟧) → A) ((d⁄dX A : (a : A⟦X⟧) → A⟦X⟧) f : A⟦X⟧) : A)
    ((coeff n : (a : A⟦X⟧) → A) f : A)
⊢ HMul.hMul (α := A) ((coeff (n + 1) : (a : A⟦X⟧) → A) f : A) (HAdd.hAdd (α := A) (↑n : A) 1) =
    (coeff n : (a : A⟦X⟧) → A) f

Tactic:
rw [coeff_derivative] at eq1

Premises used: PowerSeries.coeff_derivative