awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Evaluation (goal)
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
⊢ ε (↑p : MvPowerSeries Unit R) = MvPolynomial.eval₂ φ (fun (x : Unit) ↦ a) p
have rw₁ : Polynomial.eval₂ φ a ((MvPolynomial.uniqueAlgEquiv R PUnit.{1} : (a : MvPolynomial PUnit.{1} R) → Polynomial R) p) =
  MvPolynomial.eval₂ φ (fun (x : Unit) ↦ a) p
Tactic: rw [MvPolynomial.toMvPowerSeries_pUnitAlgEquiv, h, ← MvPolynomial.eval₂_uniqueAlgEquiv]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Evaluation (goal)
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
⊢ ε (↑p : MvPowerSeries Unit R) = MvPolynomial.eval₂ φ (fun (x : Unit) ↦ a) p
have 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)
Tactic: rw [MvPolynomial.toMvPowerSeries_pUnitAlgEquiv, h, ← MvPolynomial.eval₂_uniqueAlgEquiv]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Evaluation (goal)
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)
⊢ (⇑ε : (a : S) → T) ∘ eval₂ φ a = eval₂ (ε.comp φ) ((ε : (a : S) → T) a)
have refine : ∀ (p : Polynomial R), ((⇑ε : (a : S) → T) ∘ eval₂ φ a) (↑p : R⟦X⟧) = Polynomial.eval₂ (ε.comp φ) ((ε : (a : S) → T) a) p
Tactic: refine eval₂_unique (by simp only [RingHom.coe_comp, hε.comp hφ]) (ha.map hε)
    (hε.comp (continuous_eval₂ hφ ha)) (fun p ↦ ?_)
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Evaluation (goal)
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
⊢ Eq.{u_2 + 1} (α := S) ((aeval ha : (a : R⟦X⟧) → S) (↑p : R⟦X⟧) : S)
    ((Polynomial.aeval a : (a : Polynomial R) → S) p : S)
have rw : eval₂ (algebraMap R S) a (↑p : R⟦X⟧) = (Polynomial.aeval a : (a : Polynomial R) → S) p
Tactic: rw [coe_aeval, Polynomial.aeval_def, eval₂_coe]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Evaluation (goal)
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
⊢ Eq.{u_2 + 1} (α := S) ((aeval ha : (a : R⟦X⟧) → S) (↑p : R⟦X⟧) : S)
    ((Polynomial.aeval a : (a : Polynomial R) → S) p : S)
have rw₁ : eval₂ (algebraMap R S) a (↑p : R⟦X⟧) = Polynomial.eval₂ (algebraMap R S) a p
Tactic: rw [coe_aeval, Polynomial.aeval_def, eval₂_coe]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Evaluation (goal)
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
⊢ Eq.{u_2 + 1} (α := S) ((aeval ha : (a : R⟦X⟧) → S) (↑p : R⟦X⟧) : S)
    ((Polynomial.aeval a : (a : Polynomial R) → S) p : S)
have rw₂ : Polynomial.eval₂ (algebraMap R S) a p = Polynomial.eval₂ (algebraMap R S) a p
Tactic: rw [coe_aeval, Polynomial.aeval_def, eval₂_coe]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Evaluation (goal)
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.{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)
have 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)
Tactic: simp_rw [coe_aeval, ← algebraMap_smul (R := R) S, smul_eq_mul]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Exp (goal)
Goal:
A : Type u_1
inst : Ring A
inst_1 : Algebra ℚ A
⊢ Eq (α := A) ((constantCoeff : (a : A⟦X⟧) → A) (exp A) : A) (1 : A)
have rw : Eq (α := A) ((algebraMap ℚ A : (a : ℚ) → A) (HDiv.hDiv (α := ℚ) 1 (↑0! : ℚ)) : A) (1 : A)
Tactic: rw [← coeff_zero_eq_constantCoeff_apply, coeff_exp]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Exp (goal)
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'
⊢ (map f : (a : A⟦X⟧) → A'⟦X⟧) (exp A) = exp A'
have 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')
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Exp (goal)
Goal:
A : Type u_3
inst : CommRing A
inst_1 : Algebra ℚ A
⊢ (d⁄dX A : (a : A⟦X⟧) → A⟦X⟧) (exp A) = exp A
have 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)
Tactic: ext n
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Exp (goal)
Goal:
A : Type u_3
inst : CommRing A
inst_1 : Algebra ℚ A
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)
have 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 ! : ℚ))
Tactic: rw [coeff_derivative, coeff_exp, coeff_exp]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Exp (goal)
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)
have rw : HAdd.hAdd (α := A) (↑n : A) 1 =
  HAdd.hAdd (α := A) (β := A) ((algebraMap ℚ A : (a : ℚ) → A) (↑n : ℚ) : A) ((algebraMap ℚ A : (a : ℚ) → A) 1 : A)
Tactic: rw [map_add, map_natCast, map_one]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Exp (goal)
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)
⊢ HAdd.hAdd (α := A) (↑n : A) 1 = (algebraMap ℚ A : (a : ℚ) → A) (HAdd.hAdd (α := ℚ) (↑n : ℚ) 1)
have rw₁ : HAdd.hAdd (α := A) (↑n : A) 1 = HAdd.hAdd (α := A) (β := A) ((↑n : A) : A) ((algebraMap ℚ A : (a : ℚ) → A) 1 : A)
Tactic: rw [map_add, map_natCast, map_one]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Exp (goal)
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)
⊢ HAdd.hAdd (α := A) (↑n : A) 1 = (algebraMap ℚ A : (a : ℚ) → A) (HAdd.hAdd (α := ℚ) (↑n : ℚ) 1)
have rw₂ : HAdd.hAdd (α := A) (↑n : A) 1 = HAdd.hAdd (α := A) (↑n : A) 1
Tactic: rw [map_add, map_natCast, map_one]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Exp (hypothesis)
Goal:
A : Type u_3
inst : CommRing A
inst_1 : Algebra ℚ A
n : ℕ
⊢ 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 ! : ℚ))
have key : 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]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Exp (goal)
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)
⊢ 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 ! : ℚ))
have 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)
Tactic: rw [key, ← map_mul, factorial_succ, Nat.cast_mul, Nat.cast_add_one]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Exp (goal)
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)
⊢ 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)
have h : 1 / (HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 * (↑n ! : ℚ)) * HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 = HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Exp (goal)
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)
⊢ f = exp A
have h : ∀ (n : ℕ), Eq (α := A) ((coeff n : (a : A⟦X⟧) → A) f : A) ((coeff n : (a : A⟦X⟧) → A) (exp A) : A)
Tactic: ext n
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Exp (goal)
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)
⊢ Eq (α := A) ((coeff 0 : (a : A⟦X⟧) → A) f : A) ((coeff 0 : (a : A⟦X⟧) → A) (exp A) : A)
have h : Eq (α := A) ((constantCoeff : (a : A⟦X⟧) → A) f : A) ((constantCoeff : (a : A⟦X⟧) → A) (exp A) : A)
Tactic: rw [coeff_zero_eq_constantCoeff, hc, constantCoeff_exp]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Exp (goal)
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)
⊢ Eq (α := A) ((coeff 0 : (a : A⟦X⟧) → A) f : A) ((coeff 0 : (a : A⟦X⟧) → A) (exp A) : A)
have h₁ : Eq (α := A) (1 : A) ((constantCoeff : (a : A⟦X⟧) → A) (exp A) : A)
Tactic: rw [coeff_zero_eq_constantCoeff, hc, constantCoeff_exp]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Exp (goal)
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)
⊢ Eq (α := A) ((coeff 0 : (a : A⟦X⟧) → A) f : A) ((coeff 0 : (a : A⟦X⟧) → A) (exp A) : A)
have h₂ : Eq.{u_3 + 1} (α := A) 1 1
Tactic: rw [coeff_zero_eq_constantCoeff, hc, constantCoeff_exp]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Exp (hypothesis)
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 + 1) : (a : A⟦X⟧) → A) f : A) ((coeff (n + 1) : (a : A⟦X⟧) → A) (exp A) : A)
have 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)
Tactic: have eq1 : coeff n (d⁄dX A f) = coeff n f := congrArg (coeff n) hd
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Exp (hypothesis)
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)
⊢ Eq (α := A) ((coeff (n + 1) : (a : A⟦X⟧) → A) f : A) ((coeff (n + 1) : (a : A⟦X⟧) → A) (exp A) : A)
have eq1₁ : 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
Cleared hypotheses: eq1
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Exp (hypothesis)
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 :
  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
⊢ Eq (α := A) ((coeff (n + 1) : (a : A⟦X⟧) → A) f : A) ((coeff (n + 1) : (a : A⟦X⟧) → A) (exp A) : A)
have eq2 : 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: have eq2 : coeff n (d⁄dX A (exp A)) = coeff n (exp A) := congrArg (coeff n) (derivative_exp A)
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Exp (hypothesis)
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 :
  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
eq2 :
  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)
⊢ Eq (α := A) ((coeff (n + 1) : (a : A⟦X⟧) → A) f : A) ((coeff (n + 1) : (a : A⟦X⟧) → A) (exp A) : A)
have eq2₁ : HMul.hMul (α := A) ((coeff (n + 1) : (a : A⟦X⟧) → A) (exp A) : A) (HAdd.hAdd (α := A) (↑n : A) 1) =
  (coeff n : (a : A⟦X⟧) → A) (exp A)
Tactic: rw [coeff_derivative] at eq2
Cleared hypotheses: eq2
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Exp (hypothesis)
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 :
  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
eq2 :
  HMul.hMul (α := A) ((coeff (n + 1) : (a : A⟦X⟧) → A) (exp A) : A) (HAdd.hAdd (α := A) (↑n : A) 1) =
    (coeff n : (a : A⟦X⟧) → A) (exp A)
⊢ Eq (α := A) ((coeff (n + 1) : (a : A⟦X⟧) → A) f : A) ((coeff (n + 1) : (a : A⟦X⟧) → A) (exp A) : A)
have eq1₁ : HMul.hMul (α := A) ((coeff (n + 1) : (a : A⟦X⟧) → A) f : A) (HAdd.hAdd (α := A) (↑n : A) 1) =
  (coeff n : (a : A⟦X⟧) → A) (exp A)
Tactic: rw [ih] at eq1
Cleared hypotheses: eq1, eq2
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Exp (goal)
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 :
  HMul.hMul (α := A) ((coeff (n + 1) : (a : A⟦X⟧) → A) f : A) (HAdd.hAdd (α := A) (↑n : A) 1) =
    (coeff n : (a : A⟦X⟧) → A) (exp A)
eq2 :
  HMul.hMul (α := A) ((coeff (n + 1) : (a : A⟦X⟧) → A) (exp A) : A) (HAdd.hAdd (α := A) (↑n : A) 1) =
    (coeff n : (a : A⟦X⟧) → A) (exp A)
⊢ HMul.hMul (α := A) ((coeff (n + 1) : (a : A⟦X⟧) → A) f : A) (HAdd.hAdd (α := A) (↑n : A) 1) =
    HMul.hMul (α := A) ((coeff (n + 1) : (a : A⟦X⟧) → A) (exp A) : A) (HAdd.hAdd (α := A) (↑n : A) 1)
have rw : (coeff n : (a : A⟦X⟧) → A) (exp A) =
  HMul.hMul (α := A) ((coeff (n + 1) : (a : A⟦X⟧) → A) (exp A) : A) (HAdd.hAdd (α := A) (↑n : A) 1)
Tactic: rw [eq1, eq2]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Exp (goal)
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 :
  HMul.hMul (α := A) ((coeff (n + 1) : (a : A⟦X⟧) → A) f : A) (HAdd.hAdd (α := A) (↑n : A) 1) =
    (coeff n : (a : A⟦X⟧) → A) (exp A)
eq2 :
  HMul.hMul (α := A) ((coeff (n + 1) : (a : A⟦X⟧) → A) (exp A) : A) (HAdd.hAdd (α := A) (↑n : A) 1) =
    (coeff n : (a : A⟦X⟧) → A) (exp A)
rw :
  (coeff n : (a : A⟦X⟧) → A) (exp A) =
    HMul.hMul (α := A) ((coeff (n + 1) : (a : A⟦X⟧) → A) (exp A) : A) (HAdd.hAdd (α := A) (↑n : A) 1)
⊢ HMul.hMul (α := A) ((coeff (n + 1) : (a : A⟦X⟧) → A) f : A) (HAdd.hAdd (α := A) (↑n : A) 1) =
    HMul.hMul (α := A) ((coeff (n + 1) : (a : A⟦X⟧) → A) (exp A) : A) (HAdd.hAdd (α := A) (↑n : A) 1)
have rw₁ : Eq (α := A) ((coeff n : (a : A⟦X⟧) → A) (exp A) : A) ((coeff n : (a : A⟦X⟧) → A) (exp A) : A)
Tactic: rw [eq1, eq2]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Exp (hypothesis)
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 :
  HMul.hMul (α := A) ((coeff (n + 1) : (a : A⟦X⟧) → A) f : A) (HAdd.hAdd (α := A) (↑n : A) 1) =
    (coeff n : (a : A⟦X⟧) → A) (exp A)
eq2 :
  HMul.hMul (α := A) ((coeff (n + 1) : (a : A⟦X⟧) → A) (exp A) : A) (HAdd.hAdd (α := A) (↑n : A) 1) =
    (coeff n : (a : A⟦X⟧) → A) (exp A)
⊢ Eq (α := A) ((coeff (n + 1) : (a : A⟦X⟧) → A) f : A) ((coeff (n + 1) : (a : A⟦X⟧) → A) (exp A) : A)
have h : HMul.hMul (α := A) ((coeff (n + 1) : (a : A⟦X⟧) → A) f : A) (HAdd.hAdd (α := A) (↑n : A) 1) =
  HMul.hMul (α := A) ((coeff (n + 1) : (a : A⟦X⟧) → A) (exp A) : A) (HAdd.hAdd (α := A) (↑n : A) 1)
Tactic: have h : coeff (n + 1) f * (n + 1) = coeff (n + 1) (exp A) * (n + 1) := by
      rw [eq1, eq2]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Exp (hypothesis)
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 :
  HMul.hMul (α := A) ((coeff (n + 1) : (a : A⟦X⟧) → A) f : A) (HAdd.hAdd (α := A) (↑n : A) 1) =
    (coeff n : (a : A⟦X⟧) → A) (exp A)
eq2 :
  HMul.hMul (α := A) ((coeff (n + 1) : (a : A⟦X⟧) → A) (exp A) : A) (HAdd.hAdd (α := A) (↑n : A) 1) =
    (coeff n : (a : A⟦X⟧) → A) (exp A)
h :
  HMul.hMul (α := A) ((coeff (n + 1) : (a : A⟦X⟧) → A) f : A) (HAdd.hAdd (α := A) (↑n : A) 1) =
    HMul.hMul (α := A) ((coeff (n + 1) : (a : A⟦X⟧) → A) (exp A) : A) (HAdd.hAdd (α := A) (↑n : A) 1)
⊢ Eq (α := A) ((coeff (n + 1) : (a : A⟦X⟧) → A) f : A) ((coeff (n + 1) : (a : A⟦X⟧) → A) (exp A) : A)
have h₁ : HSMul.hSMul (β := A) n.succ ((coeff (n + 1) : (a : A⟦X⟧) → A) f : A) =
  HSMul.hSMul (β := A) n.succ ((coeff (n + 1) : (a : A⟦X⟧) → A) (exp A) : A)
Tactic: rw [← Nat.cast_succ, mul_comm, ← nsmul_eq_mul, mul_comm, ← nsmul_eq_mul] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Exp (goal)
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 : ℕ
⊢ Eq (α := A) ((coeff n : (a : A⟦X⟧) → A) f : A) ((coeff n : (a : A⟦X⟧) → A) (exp A) : A)
have h : Eq (α := A) ((coeff 0 : (a : A⟦X⟧) → A) f : A) ((coeff 0 : (a : A⟦X⟧) → A) (exp A) : A)
Tactic: induction n with
  | zero =>
    rw [coeff_zero_eq_constantCoeff, hc, constantCoeff_exp]
  | succ n ih =>
    have eq1 : coeff n (d⁄dX A f) = coeff n f := congrArg (coeff n) hd
    rw [coeff_derivative] at eq1
    have eq2 : coeff n (d⁄dX A (exp A)) = coeff n (exp A) := congrArg (coeff n) (derivative_exp A)
    rw [coeff_derivative] at eq2
    rw [ih] at eq1
    have h : coeff (n + 1) f * (n + 1) = coeff (n + 1) (exp A) * (n + 1) := by
      rw [eq1, eq2]
    rw [← Nat.cast_succ, mul_comm, ← nsmul_eq_mul, mul_comm, ← nsmul_eq_mul] at h
    exact (smul_right_inj (Nat.succ_ne_zero n)).mp h
Cleared hypotheses: n