awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 :
  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 : (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)
-- 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 :
  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)
⊢ 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

Premises used: PowerSeries.coeff_derivative
-- 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 :
  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)
⊢ 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
-- 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 :
  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)
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)
⊢ 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 [ih] at eq1
-- 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 :
  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)
rw₁ rw₂ : Eq (α := A) ((coeff n : (a : A⟦X⟧) → A) (exp A) : A) ((coeff n : (a : A⟦X⟧) → A) (exp A) : 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)

Tactic:
rw [eq1, eq2]
-- 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 :
  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)

Tactic:
have h : coeff (n + 1) f * (n + 1) = coeff (n + 1) (exp A) * (n + 1) := by
      rw [eq1, eq2]
-- 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 :
  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)
⊢ 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

Premises used: Nat.cast_succ, mul_comm, nsmul_eq_mul
-- 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 :
  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 :
  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)
⊢ Eq (α := A) ((coeff (n + 1) : (a : A⟦X⟧) → A) f : A) ((coeff (n + 1) : (a : A⟦X⟧) → A) (exp A) : A)

Tactic:
(smul_right_inj (Nat.succ_ne_zero n)).mp h

Premises used: Nat.succ_ne_zero, Iff.mp, smul_right_inj
-- 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 :
  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 :
  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)
⊢ Eq (α := A) ((coeff (n + 1) : (a : A⟦X⟧) → A) f : A) ((coeff (n + 1) : (a : A⟦X⟧) → A) (exp A) : A)

Tactic:
exact (smul_right_inj (Nat.succ_ne_zero n)).mp h

Premises used: Nat.succ_ne_zero, Iff.mp, smul_right_inj
-- 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 : ℕ
h : Eq (α := A) ((coeff 0 : (a : A⟦X⟧) → A) f : A) ((coeff 0 : (a : A⟦X⟧) → A) (exp A) : A)
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)
⊢ Eq (α := A) ((coeff n : (a : A⟦X⟧) → A) f : A) ((coeff n : (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

Premises used: Nat.cast_succ, PowerSeries.coeff_zero_eq_constantCoeff, mul_comm, nsmul_eq_mul, PowerSeries.constantCoeff_exp, PowerSeries.coeff_derivative, Nat.zero, Nat.succ
-- Module: Mathlib.RingTheory.PowerSeries.Exp
Goal:
A : Type u_4
inst : Ring A
inst_1 : Algebra ℚ A
⊢ IsUnit (M := A) ((constantCoeff : (a : A⟦X⟧) → A) (exp A) : A)

Tactic:
simp
-- Module: Mathlib.RingTheory.PowerSeries.Exp
Goal:
A : Type u_4
inst : Ring A
inst_1 : Algebra ℚ A
inst_2 : Nontrivial A
⊢ (exp A).order = 0

Tactic:
order_zero_of_unit (isUnit_exp A)

Premises used: PowerSeries.isUnit_exp, PowerSeries.order_zero_of_unit
-- Module: Mathlib.RingTheory.PowerSeries.Exp
Goal:
A : Type u_4
inst : CommRing A
inst_1 : Algebra ℚ A
a b : A
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)
⊢ 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)

Tactic:
ext n
-- Module: Mathlib.RingTheory.PowerSeries.Exp
Goal:
A : Type u_4
inst : CommRing A
inst_1 : Algebra ℚ A
a b : A
n : ℕ
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))
⊢ 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:
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]

Premises used: Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mk, OneHom.coe_mk, PowerSeries.coeff_mk, PowerSeries.coeff_mul, MonoidHom.coe_mk, RingHom.coe_mk, add_pow, PowerSeries.exp, PowerSeries.rescale, Finset.sum_mul
-- Module: Mathlib.RingTheory.PowerSeries.Exp
Goal:
A : Type u_4
inst : CommRing A
inst_1 : Algebra ℚ A
a b : A
n : ℕ
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)
⊢ 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:
apply sum_congr rfl

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.RingTheory.PowerSeries.Exp
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)
⊢ 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:
this
-- Module: Mathlib.RingTheory.PowerSeries.Exp
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)
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)
⊢ 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:
convert! this using 1
-- Module: Mathlib.RingTheory.PowerSeries.Exp
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) =
    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:
ring
-- Module: Mathlib.RingTheory.PowerSeries.Exp
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 * 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:
ring
-- Module: Mathlib.RingTheory.PowerSeries.Exp
Goal:
A : Type u_4
inst : CommRing A
inst_1 : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range n.succ
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)
⊢ 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:
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
-- Module: Mathlib.RingTheory.PowerSeries.Exp
Goal:
A : Type u_4
inst : CommRing A
inst_1 : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range n.succ
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)
⊢ 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:
congr 1
-- Module: Mathlib.RingTheory.PowerSeries.Exp
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 (α := 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)
⊢ 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:
rw [← map_natCast (algebraMap ℚ A) (n.choose x), ← map_mul, ← map_mul]

Premises used: Nat.choose, Algebra.algebraMap, Rat, map_mul, map_natCast
-- Module: Mathlib.RingTheory.PowerSeries.Exp
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)

Tactic:
RingHom.congr_arg _ ?_

Premises used: RingHom.congr_arg
-- Module: Mathlib.RingTheory.PowerSeries.Exp
Goal:
A : Type u_4
inst : CommRing A
inst_1 : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range n.succ
h :
  HDiv.hDiv (α := ℚ) 1 (↑x ! : ℚ) * HDiv.hDiv (α := ℚ) 1 (↑(n - x)! : ℚ) =
    (↑(n.choose x) : ℚ) * HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ)
⊢ 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:
refine RingHom.congr_arg _ ?_

Premises used: RingHom.congr_arg
-- Module: Mathlib.RingTheory.PowerSeries.Exp
Goal:
A : Type u_4
inst : CommRing A
inst_1 : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range n.succ
h : 1 / HMul.hMul (α := ℚ) (↑x ! : ℚ) (↑(n - x)! : ℚ) = HDiv.hDiv (α := ℚ) (↑(n.choose x) : ℚ) (↑n ! : ℚ)
⊢ HDiv.hDiv (α := ℚ) 1 (↑x ! : ℚ) * HDiv.hDiv (α := ℚ) 1 (↑(n - x)! : ℚ) =
    (↑(n.choose x) : ℚ) * HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ)

Tactic:
rw [mul_one_div (↑(n.choose x) : ℚ), one_div_mul_one_div]

Premises used: Nat.choose, Nat.cast, mul_one_div, one_div_mul_one_div
-- Module: Mathlib.RingTheory.PowerSeries.Exp
Goal:
A : Type u_4
inst : CommRing A
inst_1 : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range n.succ
h : HDiv.hDiv (α := ℚ) (↑(n.choose x) : ℚ) (↑n ! : ℚ) = 1 / HMul.hMul (α := ℚ) (↑x ! : ℚ) (↑(n - x)! : ℚ)
⊢ 1 / HMul.hMul (α := ℚ) (↑x ! : ℚ) (↑(n - x)! : ℚ) = HDiv.hDiv (α := ℚ) (↑(n.choose x) : ℚ) (↑n ! : ℚ)

Tactic:
symm
-- Module: Mathlib.RingTheory.PowerSeries.Exp
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
h₂ : Ne (α := ℚ) (↑n ! : ℚ) 0
⊢ HDiv.hDiv (α := ℚ) (↑(n.choose x) : ℚ) (↑n ! : ℚ) = 1 / HMul.hMul (α := ℚ) (↑x ! : ℚ) (↑(n - x)! : ℚ)

Tactic:
rw [div_eq_iff, div_mul_eq_mul_div, one_mul, choose_eq_factorial_div_factorial]

Premises used: div_mul_eq_mul_div, div_eq_iff, one_mul, Nat.choose_eq_factorial_div_factorial
-- Module: Mathlib.RingTheory.PowerSeries.Exp
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)!)) : ℚ) = HDiv.hDiv (α := ℚ) (↑n ! : ℚ) (↑(x ! * (n - x)!) : ℚ)
⊢ (↑(n ! / (x ! * (n - x)!)) : ℚ) = (↑n ! : ℚ) / HMul.hMul (α := ℚ) (↑x ! : ℚ) (↑(n - x)! : ℚ)

Tactic:
norm_cast
-- Module: Mathlib.RingTheory.PowerSeries.Exp
Goal:
A : Type u_4
inst : CommRing A
inst_1 : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range n.succ
h : x ! * (n - x)! ∣ n !
⊢ (↑(n ! / (x ! * (n - x)!)) : ℚ) = HDiv.hDiv (α := ℚ) (↑n ! : ℚ) (↑(x ! * (n - x)!) : ℚ)

Tactic:
rw [cast_div_charZero]

Premises used: Nat.cast_div_charZero
-- Module: Mathlib.RingTheory.PowerSeries.Exp
Goal:
A : Type u_4
inst : CommRing A
inst_1 : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range n.succ
⊢ x ! * (n - x)! ∣ n !

Tactic:
apply factorial_mul_factorial_dvd_factorial (mem_range_succ_iff.1 hx)

Premises used: Finset.mem_range_succ_iff, Nat.factorial_mul_factorial_dvd_factorial, Iff.mp
-- Module: Mathlib.RingTheory.PowerSeries.Exp
Goal:
A : Type u_4
inst : CommRing A
inst_1 : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range n.succ
⊢ x ≤ n

Tactic:
apply mem_range_succ_iff.1 hx

Premises used: Finset.mem_range_succ_iff, Iff.mp