awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℕ
h : Eq (α := A) ((coeff 0 : (a : A⟦X⟧) → A) f : A) ((coeff 0 : (a : A⟦X⟧) → A) (exp A) : A)
⊢ Eq (α := A) ((coeff n : (a : A⟦X⟧) → A) f : A) ((coeff n : (a : A⟦X⟧) → A) (exp A) : A)
have h₁ : ∀ (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)
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
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Exp (goal)
Goal:
A : Type u_4
inst : CommRing A
inst_1 : Algebra ℚ A
a b : A
⊢ HMul.hMul (α := A⟦X⟧) (β := A⟦X⟧) ((rescale a : (a : A⟦X⟧) → A⟦X⟧) (exp A) : A⟦X⟧)
      ((rescale b : (a : A⟦X⟧) → A⟦X⟧) (exp A) : A⟦X⟧) =
    (rescale (a + b) : (a : A⟦X⟧) → A⟦X⟧) (exp A)
have h : ∀ (n : ℕ),
  Eq (α := A)
    ((coeff n : (a : A⟦X⟧) → A)
        (HMul.hMul (α := A⟦X⟧) (β := A⟦X⟧) ((rescale a : (a : A⟦X⟧) → A⟦X⟧) (exp A) : A⟦X⟧)
          ((rescale b : (a : A⟦X⟧) → A⟦X⟧) (exp A) : A⟦X⟧)) :
      A)
    ((coeff n : (a : A⟦X⟧) → A) ((rescale (a + b) : (a : A⟦X⟧) → A⟦X⟧) (exp A) : A⟦X⟧) : A)
Tactic: ext n
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Exp (goal)
Goal:
A : Type u_4
inst : CommRing A
inst_1 : Algebra ℚ A
a b : A
n : ℕ
⊢ Eq (α := A)
    ((coeff n : (a : A⟦X⟧) → A)
        (HMul.hMul (α := A⟦X⟧) (β := A⟦X⟧) ((rescale a : (a : A⟦X⟧) → A⟦X⟧) (exp A) : A⟦X⟧)
          ((rescale b : (a : A⟦X⟧) → A⟦X⟧) (exp A) : A⟦X⟧)) :
      A)
    ((coeff n : (a : A⟦X⟧) → A) ((rescale (a + b) : (a : A⟦X⟧) → A⟦X⟧) (exp A) : A⟦X⟧) : A)
have h : Eq.{u_4 + 1} (α := A)
  (∑ x ∈ Finset.range n.succ,
    HMul.hMul (β := A) (a ^ x) ((algebraMap ℚ A : (a : ℚ) → A) (HDiv.hDiv (α := ℚ) 1 (↑x ! : ℚ)) : A) *
      HMul.hMul (β := A) (b ^ (n - x)) ((algebraMap ℚ A : (a : ℚ) → A) (HDiv.hDiv (α := ℚ) 1 (↑(n - x)! : ℚ)) : A))
  (∑ x ∈ Finset.range (n + 1),
    HMul.hMul (β := A) (a ^ x * b ^ (n - x) * (↑(n.choose x) : A))
      ((algebraMap ℚ A : (a : ℚ) → A) (HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ)) : A))
Tactic: simp only [coeff_mul, exp, rescale, coeff_mk, MonoidHom.coe_mk, OneHom.coe_mk, coe_mk,
    Nat.sum_antidiagonal_eq_sum_range_succ_mk, add_pow, sum_mul]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Exp (goal)
Goal:
A : Type u_4
inst : CommRing A
inst_1 : Algebra ℚ A
a b : A
n : ℕ
⊢ Eq.{u_4 + 1} (α := A)
    (∑ x ∈ Finset.range n.succ,
      HMul.hMul (β := A) (a ^ x) ((algebraMap ℚ A : (a : ℚ) → A) (HDiv.hDiv (α := ℚ) 1 (↑x ! : ℚ)) : A) *
        HMul.hMul (β := A) (b ^ (n - x)) ((algebraMap ℚ A : (a : ℚ) → A) (HDiv.hDiv (α := ℚ) 1 (↑(n - x)! : ℚ)) : A))
    (∑ x ∈ Finset.range (n + 1),
      HMul.hMul (β := A) (a ^ x * b ^ (n - x) * (↑(n.choose x) : A))
        ((algebraMap ℚ A : (a : ℚ) → A) (HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ)) : A))
have h : ∀ x ∈ Finset.range n.succ,
  HMul.hMul (β := A) (a ^ x) ((algebraMap ℚ A : (a : ℚ) → A) (HDiv.hDiv (α := ℚ) 1 (↑x ! : ℚ)) : A) *
      HMul.hMul (β := A) (b ^ (n - x)) ((algebraMap ℚ A : (a : ℚ) → A) (HDiv.hDiv (α := ℚ) 1 (↑(n - x)! : ℚ)) : A) =
    HMul.hMul (β := A) (a ^ x * b ^ (n - x) * (↑(n.choose x) : A))
      ((algebraMap ℚ A : (a : ℚ) → A) (HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ)) : A)
Tactic: apply sum_congr rfl
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Exp (goal)
Goal:
A : Type u_4
inst : CommRing A
inst_1 : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range n.succ
this :
  a ^ x * b ^ (n - x) *
      HMul.hMul (α := A) (β := A) ((algebraMap ℚ A : (a : ℚ) → A) (HDiv.hDiv (α := ℚ) 1 (↑x ! : ℚ)) : A)
        ((algebraMap ℚ A : (a : ℚ) → A) (HDiv.hDiv (α := ℚ) 1 (↑(n - x)! : ℚ)) : A) =
    a ^ x * b ^ (n - x) *
      HMul.hMul (α := A) (β := A) ((↑(n.choose x) : A) : A)
        ((algebraMap ℚ A : (a : ℚ) → A) (HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ)) : A)
⊢ HMul.hMul (β := A) (a ^ x) ((algebraMap ℚ A : (a : ℚ) → A) (HDiv.hDiv (α := ℚ) 1 (↑x ! : ℚ)) : A) *
      HMul.hMul (β := A) (b ^ (n - x)) ((algebraMap ℚ A : (a : ℚ) → A) (HDiv.hDiv (α := ℚ) 1 (↑(n - x)! : ℚ)) : A) =
    HMul.hMul (β := A) (a ^ x * b ^ (n - x) * (↑(n.choose x) : A))
      ((algebraMap ℚ A : (a : ℚ) → A) (HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ)) : A)
have h : HMul.hMul (β := A) (a ^ x) ((algebraMap ℚ A : (a : ℚ) → A) (HDiv.hDiv (α := ℚ) 1 (↑x ! : ℚ)) : A) *
    HMul.hMul (β := A) (b ^ (n - x)) ((algebraMap ℚ A : (a : ℚ) → A) (HDiv.hDiv (α := ℚ) 1 (↑(n - x)! : ℚ)) : A) =
  a ^ x * b ^ (n - x) *
    HMul.hMul (α := A) (β := A) ((algebraMap ℚ A : (a : ℚ) → A) (HDiv.hDiv (α := ℚ) 1 (↑x ! : ℚ)) : A)
      ((algebraMap ℚ A : (a : ℚ) → A) (HDiv.hDiv (α := ℚ) 1 (↑(n - x)! : ℚ)) : A)
Tactic: convert! this using 1
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Exp (goal)
Goal:
A : Type u_4
inst : CommRing A
inst_1 : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range n.succ
this :
  a ^ x * b ^ (n - x) *
      HMul.hMul (α := A) (β := A) ((algebraMap ℚ A : (a : ℚ) → A) (HDiv.hDiv (α := ℚ) 1 (↑x ! : ℚ)) : A)
        ((algebraMap ℚ A : (a : ℚ) → A) (HDiv.hDiv (α := ℚ) 1 (↑(n - x)! : ℚ)) : A) =
    a ^ x * b ^ (n - x) *
      HMul.hMul (α := A) (β := A) ((↑(n.choose x) : A) : A)
        ((algebraMap ℚ A : (a : ℚ) → A) (HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ)) : A)
h :
  HMul.hMul (β := A) (a ^ x) ((algebraMap ℚ A : (a : ℚ) → A) (HDiv.hDiv (α := ℚ) 1 (↑x ! : ℚ)) : A) *
      HMul.hMul (β := A) (b ^ (n - x)) ((algebraMap ℚ A : (a : ℚ) → A) (HDiv.hDiv (α := ℚ) 1 (↑(n - x)! : ℚ)) : A) =
    a ^ x * b ^ (n - x) *
      HMul.hMul (α := A) (β := A) ((algebraMap ℚ A : (a : ℚ) → A) (HDiv.hDiv (α := ℚ) 1 (↑x ! : ℚ)) : A)
        ((algebraMap ℚ A : (a : ℚ) → A) (HDiv.hDiv (α := ℚ) 1 (↑(n - x)! : ℚ)) : A)
⊢ HMul.hMul (β := A) (a ^ x) ((algebraMap ℚ A : (a : ℚ) → A) (HDiv.hDiv (α := ℚ) 1 (↑x ! : ℚ)) : A) *
      HMul.hMul (β := A) (b ^ (n - x)) ((algebraMap ℚ A : (a : ℚ) → A) (HDiv.hDiv (α := ℚ) 1 (↑(n - x)! : ℚ)) : A) =
    HMul.hMul (β := A) (a ^ x * b ^ (n - x) * (↑(n.choose x) : A))
      ((algebraMap ℚ A : (a : ℚ) → A) (HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ)) : A)
have h₁ : HMul.hMul (β := A) (a ^ x * b ^ (n - x) * (↑(n.choose x) : A))
    ((algebraMap ℚ A : (a : ℚ) → A) (HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ)) : A) =
  a ^ x * b ^ (n - x) *
    HMul.hMul (α := A) (β := A) ((↑(n.choose x) : A) : A)
      ((algebraMap ℚ A : (a : ℚ) → A) (HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ)) : A)
Tactic: convert! this using 1
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Exp (goal)
Goal:
A : Type u_4
inst : CommRing A
inst_1 : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range n.succ
⊢ HMul.hMul (β := A) (a ^ x) ((algebraMap ℚ A : (a : ℚ) → A) (HDiv.hDiv (α := ℚ) 1 (↑x ! : ℚ)) : A) *
      HMul.hMul (β := A) (b ^ (n - x)) ((algebraMap ℚ A : (a : ℚ) → A) (HDiv.hDiv (α := ℚ) 1 (↑(n - x)! : ℚ)) : A) =
    HMul.hMul (β := A) (a ^ x * b ^ (n - x) * (↑(n.choose x) : A))
      ((algebraMap ℚ A : (a : ℚ) → A) (HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ)) : A)
have h : a ^ x * b ^ (n - x) *
    HMul.hMul (α := A) (β := A) ((algebraMap ℚ A : (a : ℚ) → A) (HDiv.hDiv (α := ℚ) 1 (↑x ! : ℚ)) : A)
      ((algebraMap ℚ A : (a : ℚ) → A) (HDiv.hDiv (α := ℚ) 1 (↑(n - x)! : ℚ)) : A) =
  a ^ x * b ^ (n - x) *
    HMul.hMul (α := A) (β := A) ((↑(n.choose x) : A) : A)
      ((algebraMap ℚ A : (a : ℚ) → A) (HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ)) : A)
Tactic: suffices
    a ^ x * b ^ (n - x) *
        (algebraMap ℚ A (1 / ↑x.factorial) * algebraMap ℚ A (1 / ↑(n - x).factorial)) =
      a ^ x * b ^ (n - x) * (↑(n.choose x) * (algebraMap ℚ A) (1 / ↑n.factorial))
    by convert! this using 1 <;> ring
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Exp (goal)
Goal:
A : Type u_4
inst : CommRing A
inst_1 : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range n.succ
⊢ a ^ x * b ^ (n - x) *
      HMul.hMul (α := A) (β := A) ((algebraMap ℚ A : (a : ℚ) → A) (HDiv.hDiv (α := ℚ) 1 (↑x ! : ℚ)) : A)
        ((algebraMap ℚ A : (a : ℚ) → A) (HDiv.hDiv (α := ℚ) 1 (↑(n - x)! : ℚ)) : A) =
    a ^ x * b ^ (n - x) *
      HMul.hMul (α := A) (β := A) ((↑(n.choose x) : A) : A)
        ((algebraMap ℚ A : (a : ℚ) → A) (HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ)) : A)
have h : HMul.hMul (α := A) (β := A) ((algebraMap ℚ A : (a : ℚ) → A) (HDiv.hDiv (α := ℚ) 1 (↑x ! : ℚ)) : A)
    ((algebraMap ℚ A : (a : ℚ) → A) (HDiv.hDiv (α := ℚ) 1 (↑(n - x)! : ℚ)) : A) =
  HMul.hMul (α := A) (β := A) ((↑(n.choose x) : A) : A)
    ((algebraMap ℚ A : (a : ℚ) → A) (HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ)) : A)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Exp (goal)
Goal:
A : Type u_4
inst : CommRing A
inst_1 : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range n.succ
⊢ HMul.hMul (α := A) (β := A) ((algebraMap ℚ A : (a : ℚ) → A) (HDiv.hDiv (α := ℚ) 1 (↑x ! : ℚ)) : A)
      ((algebraMap ℚ A : (a : ℚ) → A) (HDiv.hDiv (α := ℚ) 1 (↑(n - x)! : ℚ)) : A) =
    HMul.hMul (α := A) (β := A) ((↑(n.choose x) : A) : A)
      ((algebraMap ℚ A : (a : ℚ) → A) (HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ)) : A)
have h : Eq (α := A)
  ((algebraMap ℚ A : (a : ℚ) → A) (HDiv.hDiv (α := ℚ) 1 (↑x ! : ℚ) * HDiv.hDiv (α := ℚ) 1 (↑(n - x)! : ℚ)) : A)
  ((algebraMap ℚ A : (a : ℚ) → A) ((↑(n.choose x) : ℚ) * HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ)) : A)
Tactic: rw [← map_natCast (algebraMap ℚ A) (n.choose x), ← map_mul, ← map_mul]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Exp (goal)
Goal:
A : Type u_4
inst : CommRing A
inst_1 : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range n.succ
⊢ Eq (α := A)
    ((algebraMap ℚ A : (a : ℚ) → A) (HDiv.hDiv (α := ℚ) 1 (↑x ! : ℚ) * HDiv.hDiv (α := ℚ) 1 (↑(n - x)! : ℚ)) : A)
    ((algebraMap ℚ A : (a : ℚ) → A) ((↑(n.choose x) : ℚ) * HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ)) : A)
have h : HDiv.hDiv (α := ℚ) 1 (↑x ! : ℚ) * HDiv.hDiv (α := ℚ) 1 (↑(n - x)! : ℚ) =
  (↑(n.choose x) : ℚ) * HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ)
Tactic: refine RingHom.congr_arg _ ?_
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Exp (goal)
Goal:
A : Type u_4
inst : CommRing A
inst_1 : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range n.succ
⊢ HDiv.hDiv (α := ℚ) 1 (↑x ! : ℚ) * HDiv.hDiv (α := ℚ) 1 (↑(n - x)! : ℚ) =
    (↑(n.choose x) : ℚ) * HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ)
have h : 1 / HMul.hMul (α := ℚ) (↑x ! : ℚ) (↑(n - x)! : ℚ) = HDiv.hDiv (α := ℚ) (↑(n.choose x) : ℚ) (↑n ! : ℚ)
Tactic: rw [mul_one_div (↑(n.choose x) : ℚ), one_div_mul_one_div]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Exp (goal)
Goal:
A : Type u_4
inst : CommRing A
inst_1 : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range n.succ
⊢ 1 / HMul.hMul (α := ℚ) (↑x ! : ℚ) (↑(n - x)! : ℚ) = HDiv.hDiv (α := ℚ) (↑(n.choose x) : ℚ) (↑n ! : ℚ)
have h : HDiv.hDiv (α := ℚ) (↑(n.choose x) : ℚ) (↑n ! : ℚ) = 1 / HMul.hMul (α := ℚ) (↑x ! : ℚ) (↑(n - x)! : ℚ)
Tactic: symm
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Exp (goal)
Goal:
A : Type u_4
inst : CommRing A
inst_1 : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range n.succ
⊢ HDiv.hDiv (α := ℚ) (↑(n.choose x) : ℚ) (↑n ! : ℚ) = 1 / HMul.hMul (α := ℚ) (↑x ! : ℚ) (↑(n - x)! : ℚ)
have h : (↑(n ! / (x ! * (n - x)!)) : ℚ) = (↑n ! : ℚ) / HMul.hMul (α := ℚ) (↑x ! : ℚ) (↑(n - x)! : ℚ)
Tactic: rw [div_eq_iff, div_mul_eq_mul_div, one_mul, choose_eq_factorial_div_factorial]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Exp (goal)
Goal:
A : Type u_4
inst : CommRing A
inst_1 : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range n.succ
h : (↑(n ! / (x ! * (n - x)!)) : ℚ) = (↑n ! : ℚ) / HMul.hMul (α := ℚ) (↑x ! : ℚ) (↑(n - x)! : ℚ)
⊢ HDiv.hDiv (α := ℚ) (↑(n.choose x) : ℚ) (↑n ! : ℚ) = 1 / HMul.hMul (α := ℚ) (↑x ! : ℚ) (↑(n - x)! : ℚ)
have h₁ : x ≤ n
Tactic: rw [div_eq_iff, div_mul_eq_mul_div, one_mul, choose_eq_factorial_div_factorial]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Exp (goal)
Goal:
A : Type u_4
inst : CommRing A
inst_1 : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range n.succ
h : (↑(n ! / (x ! * (n - x)!)) : ℚ) = (↑n ! : ℚ) / HMul.hMul (α := ℚ) (↑x ! : ℚ) (↑(n - x)! : ℚ)
h₁ : x ≤ n
⊢ HDiv.hDiv (α := ℚ) (↑(n.choose x) : ℚ) (↑n ! : ℚ) = 1 / HMul.hMul (α := ℚ) (↑x ! : ℚ) (↑(n - x)! : ℚ)
have h₂ : Ne (α := ℚ) (↑n ! : ℚ) 0
Tactic: rw [div_eq_iff, div_mul_eq_mul_div, one_mul, choose_eq_factorial_div_factorial]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Exp (goal)
Goal:
A : Type u_4
inst : CommRing A
inst_1 : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range n.succ
⊢ (↑(n ! / (x ! * (n - x)!)) : ℚ) = (↑n ! : ℚ) / HMul.hMul (α := ℚ) (↑x ! : ℚ) (↑(n - x)! : ℚ)
have h : (↑(n ! / (x ! * (n - x)!)) : ℚ) = HDiv.hDiv (α := ℚ) (↑n ! : ℚ) (↑(x ! * (n - x)!) : ℚ)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Exp (goal)
Goal:
A : Type u_4
inst : CommRing A
inst_1 : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range n.succ
⊢ (↑(n ! / (x ! * (n - x)!)) : ℚ) = HDiv.hDiv (α := ℚ) (↑n ! : ℚ) (↑(x ! * (n - x)!) : ℚ)
have h : x ! * (n - x)! ∣ n !
Tactic: rw [cast_div_charZero]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Exp (goal)
Goal:
A : Type u_4
inst : CommRing A
inst_1 : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range n.succ
h : Eq (α := ℚ) (↑n ! : ℚ) 0
⊢ False
have h₁ : n ! = 0
Tactic: apply factorial_ne_zero n
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Exp (goal)
Goal:
A : Type u_4
inst : CommRing A
inst_1 : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range n.succ
h : Eq (α := ℚ) (↑n ! : ℚ) 0
⊢ n ! = 0
have h₁ : Eq (α := ℕ) 0 0
Tactic: rw [cast_eq_zero.1 h]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Exp (goal)
Goal:
A : Type u_4
inst : CommRing A
inst_1 : Algebra ℚ A
⊢ HMul.hMul (β := A⟦X⟧) (exp A) ((evalNegHom : (a : A⟦X⟧) → A⟦X⟧) (exp A) : A⟦X⟧) = 1
have h : exp A = (rescale 1 : (a : A⟦X⟧) → A⟦X⟧) (exp A)
Tactic: convert! exp_mul_exp_eq_exp_add (1 : A) (-1)
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Exp (goal)
Goal:
A : Type u_4
inst : CommRing A
inst_1 : Algebra ℚ A
h : exp A = (rescale 1 : (a : A⟦X⟧) → A⟦X⟧) (exp A)
⊢ HMul.hMul (β := A⟦X⟧) (exp A) ((evalNegHom : (a : A⟦X⟧) → A⟦X⟧) (exp A) : A⟦X⟧) = 1
have h₁ : Eq (α := A⟦X⟧) (1 : A⟦X⟧) ((rescale (HAdd.hAdd (α := A) 1 (-1)) : (a : A⟦X⟧) → A⟦X⟧) (exp A) : A⟦X⟧)
Tactic: convert! exp_mul_exp_eq_exp_add (1 : A) (-1)
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Exp (goal)
Goal:
A : Type u_4
inst : CommRing A
inst_1 : Algebra ℚ A
k : ℕ
⊢ exp A ^ k = (rescale (↑k : A) : (a : A⟦X⟧) → A⟦X⟧) (exp A)
have zero : HPow.hPow (β := ℕ) (exp A) 0 = (rescale (↑0 : A) : (a : A⟦X⟧) → A⟦X⟧) (exp A)
Tactic: induction k with
  | zero =>
    simp only [rescale_zero, constantCoeff_exp, Function.comp_apply, map_one, cast_zero,
      pow_zero (exp A), coe_comp]
  | succ k h =>
    simpa only [succ_eq_add_one, cast_add, ← exp_mul_exp_eq_exp_add (k : A), ← h, cast_one,
      id_apply, rescale_one] using pow_succ (exp A) k
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Exp (goal)
Goal:
A : Type u_4
inst : CommRing A
inst_1 : Algebra ℚ A
k : ℕ
zero : HPow.hPow (β := ℕ) (exp A) 0 = (rescale (↑0 : A) : (a : A⟦X⟧) → A⟦X⟧) (exp A)
⊢ exp A ^ k = (rescale (↑k : A) : (a : A⟦X⟧) → A⟦X⟧) (exp A)
have succ : ∀ (k : ℕ) (h : exp A ^ k = (rescale (↑k : A) : (a : A⟦X⟧) → A⟦X⟧) (exp A)),
  exp A ^ (k + 1) = (rescale (↑(k + 1) : A) : (a : A⟦X⟧) → A⟦X⟧) (exp A)
Tactic: induction k with
  | zero =>
    simp only [rescale_zero, constantCoeff_exp, Function.comp_apply, map_one, cast_zero,
      pow_zero (exp A), coe_comp]
  | succ k h =>
    simpa only [succ_eq_add_one, cast_add, ← exp_mul_exp_eq_exp_add (k : A), ← h, cast_one,
      id_apply, rescale_one] using pow_succ (exp A) k
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Exp (goal)
Goal:
A : Type u_4
inst : CommRing A
inst_1 : Algebra ℚ A
n : ℕ
⊢ Eq.{u_4 + 1} (α := A⟦X⟧) (∑ k ∈ Finset.range n, exp A ^ k)
    (mk fun (p : ℕ) ↦
      ∑ k ∈ Finset.range n,
        HMul.hMul (β := A) (HPow.hPow (α := A) (↑k : A) p) ((algebraMap ℚ A : (a : ℚ) → A) (↑p ! : ℚ)⁻¹ : A))
have simp : Eq.{u_4 + 1} (α := A⟦X⟧)
  (∑ x ∈ Finset.range n,
    ({
          toFun := fun (f : A⟦X⟧) ↦
            mk fun (n : ℕ) ↦ HMul.hMul (β := A) (HPow.hPow (α := A) (↑x : A) n) ((coeff n : (a : A⟦X⟧) → A) f : A),
          map_one' := sorry, map_mul' := sorry, map_zero' := sorry, map_add' := sorry } :
        (a : A⟦X⟧) → A⟦X⟧)
      (exp A))
  (mk fun (p : ℕ) ↦
    ∑ k ∈ Finset.range n,
      HMul.hMul (β := A) (HPow.hPow (α := A) (↑k : A) p) ((algebraMap ℚ A : (a : ℚ) → A) (↑p ! : ℚ)⁻¹ : A))
Tactic: simp only [exp_pow_eq_rescale_exp, rescale]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Exp (goal)
Goal:
A : Type u_4
inst : CommRing A
inst_1 : Algebra ℚ A
n : ℕ
⊢ Eq.{u_4 + 1} (α := A⟦X⟧)
    (∑ x ∈ Finset.range n,
      ({
            toFun := fun (f : A⟦X⟧) ↦
              mk fun (n : ℕ) ↦ HMul.hMul (β := A) (HPow.hPow (α := A) (↑x : A) n) ((coeff n : (a : A⟦X⟧) → A) f : A),
            map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } :
          (a : A⟦X⟧) → A⟦X⟧)
        (exp A))
    (mk fun (p : ℕ) ↦
      ∑ k ∈ Finset.range n,
        HMul.hMul (β := A) (HPow.hPow (α := A) (↑k : A) p) ((algebraMap ℚ A : (a : ℚ) → A) (↑p ! : ℚ)⁻¹ : A))
have h : ∀ (n_1 : ℕ),
  Eq.{u_4 + 1} (α := A)
    ((coeff n_1 : (a : A⟦X⟧) → A)
        (∑ x ∈ Finset.range n,
          ({
                toFun := fun (f : A⟦X⟧) ↦
                  mk fun (n : ℕ) ↦
                    HMul.hMul (β := A) (HPow.hPow (α := A) (↑x : A) n) ((coeff n : (a : A⟦X⟧) → A) f : A),
                map_one' := sorry, map_mul' := sorry, map_zero' := sorry, map_add' := sorry } :
              (a : A⟦X⟧) → A⟦X⟧)
            (exp A)) :
      A)
    ((coeff n_1 : (a : A⟦X⟧) → A)
        (mk fun (p : ℕ) ↦
          ∑ k ∈ Finset.range n,
            HMul.hMul (β := A) (HPow.hPow (α := A) (↑k : A) p) ((algebraMap ℚ A : (a : ℚ) → A) (↑p ! : ℚ)⁻¹ : A)) :
      A)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Expand (goal)
Goal:
R : Type u_2
inst : CommRing R
p : ℕ
hp : p ≠ 0
r : R
| ((expand p hp : (a : R⟦X⟧) → R⟦X⟧) ((C : (a : R) → R⟦X⟧) r : R⟦X⟧) : R⟦X⟧)
have rw : ((C : (a : R) → R⟦X⟧) r : R⟦X⟧)
Tactic: rw [← mul_one (C r), ← smul_eq_C_mul, expand, AlgHom.map_smul_of_tower,
    map_one, smul_eq_C_mul, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Expand (goal)
Goal:
R : Type u_2
inst : CommRing R
p : ℕ
hp : p ≠ 0
r : R
⊢ Eq (α := R⟦X⟧) ((expand p hp : (a : R⟦X⟧) → R⟦X⟧) ((C : (a : R) → R⟦X⟧) r : R⟦X⟧) : R⟦X⟧)
    ((C : (a : R) → R⟦X⟧) r : R⟦X⟧)
have conv_lhs : Eq (α := R⟦X⟧) ((expand p hp : (a : R⟦X⟧) → R⟦X⟧) ((C : (a : R) → R⟦X⟧) r : R⟦X⟧) : R⟦X⟧)
  ((C : (a : R) → R⟦X⟧) r : R⟦X⟧)
Tactic: conv_lhs => rw [← mul_one (C r), ← smul_eq_C_mul, expand, AlgHom.map_smul_of_tower,
    map_one, smul_eq_C_mul, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Expand (goal)
Goal:
R : Type u_2
inst : CommRing R
p : ℕ
hp : p ≠ 0
r : R
conv_lhs :
  Eq (α := R⟦X⟧) ((expand p hp : (a : R⟦X⟧) → R⟦X⟧) ((C : (a : R) → R⟦X⟧) r : R⟦X⟧) : R⟦X⟧)
    ((C : (a : R) → R⟦X⟧) r : R⟦X⟧)
⊢ Eq (α := R⟦X⟧) ((expand p hp : (a : R⟦X⟧) → R⟦X⟧) ((C : (a : R) → R⟦X⟧) r : R⟦X⟧) : R⟦X⟧)
    ((C : (a : R) → R⟦X⟧) r : R⟦X⟧)
have conv_lhs₁ : Eq (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) r : R⟦X⟧) ((C : (a : R) → R⟦X⟧) r : R⟦X⟧)
Tactic: conv_lhs => rw [← mul_one (C r), ← smul_eq_C_mul, expand, AlgHom.map_smul_of_tower,
    map_one, smul_eq_C_mul, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Expand (goal)
Goal:
R : Type u_2
inst : CommRing R
p : ℕ
hp : p ≠ 0
q : ℕ
hq : q ≠ 0
⊢ Eq.{u_2 + 1} (α := R⟦X⟧ →ₐ[R] R⟦X⟧) (expand (p * q) ⋯) (AlgHom.comp (expand p hp) (expand q hq))
have H : ∀ (i : R⟦X⟧),
  Eq (α := R⟦X⟧) ((expand (p * q) sorry : (a : R⟦X⟧) → R⟦X⟧) i : R⟦X⟧)
    ((AlgHom.comp (expand p hp) (expand q hq) : (a : R⟦X⟧) → R⟦X⟧) i : R⟦X⟧)
Tactic: ext1 i
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Expand (goal)
Goal:
τ : Type u_1
S : Type u_3
inst : CommRing S
p : ℕ
hp : p ≠ 0
f : MvPowerSeries τ S
hf : HasSubst f
φ : S⟦X⟧
⊢ Eq (α := MvPowerSeries τ S)
    ((MvPowerSeries.expand p hp : (a : MvPowerSeries τ S) → MvPowerSeries τ S) (subst f φ) : MvPowerSeries τ S)
    (subst ((MvPowerSeries.expand p hp : (a : MvPowerSeries τ S) → MvPowerSeries τ S) f) φ : MvPowerSeries τ S)
have rw : Eq (α := MvPowerSeries τ S)
  ((MvPowerSeries.expand p hp : (a : MvPowerSeries τ S) → MvPowerSeries τ S)
      (MvPowerSeries.subst (fun (x : Unit) ↦ f) φ) :
    MvPowerSeries τ S)
  (subst ((MvPowerSeries.expand p hp : (a : MvPowerSeries τ S) → MvPowerSeries τ S) f) φ : MvPowerSeries τ S)
Tactic: rw [PowerSeries.subst, MvPowerSeries.expand_subst _ hp (HasSubst.const hf) (φ := φ),
    PowerSeries.subst]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Expand (goal)
Goal:
τ : Type u_1
S : Type u_3
inst : CommRing S
p : ℕ
hp : p ≠ 0
f : MvPowerSeries τ S
hf : HasSubst f
φ : S⟦X⟧
rw :
  Eq (α := MvPowerSeries τ S)
    ((MvPowerSeries.expand p hp : (a : MvPowerSeries τ S) → MvPowerSeries τ S)
        (MvPowerSeries.subst (fun (x : Unit) ↦ f) φ) :
      MvPowerSeries τ S)
    (subst ((MvPowerSeries.expand p hp : (a : MvPowerSeries τ S) → MvPowerSeries τ S) f) φ : MvPowerSeries τ S)
⊢ Eq (α := MvPowerSeries τ S)
    ((MvPowerSeries.expand p hp : (a : MvPowerSeries τ S) → MvPowerSeries τ S) (subst f φ) : MvPowerSeries τ S)
    (subst ((MvPowerSeries.expand p hp : (a : MvPowerSeries τ S) → MvPowerSeries τ S) f) φ : MvPowerSeries τ S)
have rw₁ : Eq (α := MvPowerSeries τ S)
  (MvPowerSeries.subst (fun (i : Unit) ↦ (MvPowerSeries.expand p hp : (a : MvPowerSeries τ S) → MvPowerSeries τ S) f) φ)
  (subst ((MvPowerSeries.expand p hp : (a : MvPowerSeries τ S) → MvPowerSeries τ S) f) φ)
Tactic: rw [PowerSeries.subst, MvPowerSeries.expand_subst _ hp (HasSubst.const hf) (φ := φ),
    PowerSeries.subst]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Expand (goal)
Goal:
τ : Type u_1
S : Type u_3
inst : CommRing S
p : ℕ
hp : p ≠ 0
f : MvPowerSeries τ S
hf : HasSubst f
φ : S⟦X⟧
rw :
  Eq (α := MvPowerSeries τ S)
    ((MvPowerSeries.expand p hp : (a : MvPowerSeries τ S) → MvPowerSeries τ S)
        (MvPowerSeries.subst (fun (x : Unit) ↦ f) φ) :
      MvPowerSeries τ S)
    (subst ((MvPowerSeries.expand p hp : (a : MvPowerSeries τ S) → MvPowerSeries τ S) f) φ : MvPowerSeries τ S)
rw₁ :
  Eq (α := MvPowerSeries τ S)
    (MvPowerSeries.subst (fun (i : Unit) ↦ (MvPowerSeries.expand p hp : (a : MvPowerSeries τ S) → MvPowerSeries τ S) f)
      φ)
    (subst ((MvPowerSeries.expand p hp : (a : MvPowerSeries τ S) → MvPowerSeries τ S) f) φ)
⊢ Eq (α := MvPowerSeries τ S)
    ((MvPowerSeries.expand p hp : (a : MvPowerSeries τ S) → MvPowerSeries τ S) (subst f φ) : MvPowerSeries τ S)
    (subst ((MvPowerSeries.expand p hp : (a : MvPowerSeries τ S) → MvPowerSeries τ S) f) φ : MvPowerSeries τ S)
have rw₂ : Eq (α := MvPowerSeries τ S)
  (MvPowerSeries.subst (fun (i : Unit) ↦ (MvPowerSeries.expand p hp : (a : MvPowerSeries τ S) → MvPowerSeries τ S) f) φ)
  (MvPowerSeries.subst (fun (x : Unit) ↦ (MvPowerSeries.expand p hp : (a : MvPowerSeries τ S) → MvPowerSeries τ S) f) φ)
Tactic: rw [PowerSeries.subst, MvPowerSeries.expand_subst _ hp (HasSubst.const hf) (φ := φ),
    PowerSeries.subst]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Expand (goal)
Goal:
R : Type u_2
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : R⟦X⟧
m : ℕ
⊢ Eq (α := R) ((coeff (p * m) : (a : R⟦X⟧) → R) ((expand p hp : (a : R⟦X⟧) → R⟦X⟧) φ : R⟦X⟧) : R)
    ((coeff m : (a : R⟦X⟧) → R) φ : R)
have rw : Eq (α := R)
  ((MvPowerSeries.coeff (Finsupp.single () (p * m)) : (a : R⟦X⟧) → R) ((expand p hp : (a : R⟦X⟧) → R⟦X⟧) φ : R⟦X⟧) : R)
  ((coeff m : (a : R⟦X⟧) → R) φ : R)
Tactic: rw [coeff, coeff, expand, ← smul_eq_mul, ← Finsupp.smul_single, MvPowerSeries.coeff_expand_smul]