awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Series
Goal:
z : ℂ
h :
  Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * z ^ (2 * n) / (↑(2 * n)! : ℂ)) fun (n : ℕ) ↦
    (z * I) ^ (2 * n) / (↑(2 * n)! : ℂ)
⊢ HasSum (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * z ^ (2 * n) / (↑(2 * n)! : ℂ)) (cos z)

Tactic:
convert! Complex.hasSum_cos' z using 1

Premises used: Complex.hasSum_cos'
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Series
Goal:
z : ℂ
h :
  Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * z ^ (2 * n) / (↑(2 * n)! : ℂ)) fun (n : ℕ) ↦
    z ^ (2 * n) * I ^ (2 * n) / (↑(2 * n)! : ℂ)
h₁ :
  Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * HPow.hPow (β := ℕ) z 2 ^ n / (↑(2 * n)! : ℂ)) fun (n : ℕ) ↦
    HPow.hPow (β := ℕ) z 2 ^ n * HPow.hPow (β := ℕ) I 2 ^ n / (↑(2 * n)! : ℂ)
h₂ :
  Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * HPow.hPow (β := ℕ) z 2 ^ n / (↑(2 * n)! : ℂ)) fun (n : ℕ) ↦
    HPow.hPow (β := ℕ) z 2 ^ n * HPow.hPow (α := ℂ) (-1) n / (↑(2 * n)! : ℂ)
⊢ Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * z ^ (2 * n) / (↑(2 * n)! : ℂ)) fun (n : ℕ) ↦
    (z * I) ^ (2 * n) / (↑(2 * n)! : ℂ)

Tactic:
simp_rw [mul_pow, pow_mul, Complex.I_sq, mul_comm]

Premises used: pow_mul, Complex.I_sq, mul_comm, mul_pow
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Series
Goal:
z : ℂ
⊢ HasSum (fun (n : ℕ) ↦ (z * I) ^ (2 * n + 1) / (↑(2 * n + 1)! : ℂ) / I) (sin z)

Tactic:
Complex.hasSum_sin' z

Premises used: Complex.hasSum_sin'
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Series
Goal:
z : ℂ
h :
  Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * z ^ (2 * n + 1) / (↑(2 * n + 1)! : ℂ)) fun (n : ℕ) ↦
    (z * I) ^ (2 * n + 1) / (↑(2 * n + 1)! : ℂ) / I
⊢ HasSum (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * z ^ (2 * n + 1) / (↑(2 * n + 1)! : ℂ)) (sin z)

Tactic:
convert! Complex.hasSum_sin' z using 1

Premises used: Complex.hasSum_sin'
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Series
Goal:
z : ℂ
h :
  Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * z ^ (2 * n + 1) / (↑(2 * n + 1)! : ℂ)) fun (n : ℕ) ↦
    z ^ (2 * n + 1) * I ^ (2 * n + 1) / (↑(2 * n + 1)! : ℂ) / I
h₁ :
  Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * (z ^ (2 * n) * z) / (↑(2 * n + 1)! : ℂ)) fun (n : ℕ) ↦
    z ^ (2 * n) * z * (I ^ (2 * n) * I) / (↑(2 * n + 1)! : ℂ) / I
h₂ :
  Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * (HPow.hPow (β := ℕ) z 2 ^ n * z) / (↑(2 * n + 1)! : ℂ))
    fun (n : ℕ) ↦ HPow.hPow (β := ℕ) z 2 ^ n * z * (HPow.hPow (β := ℕ) I 2 ^ n * I) / (↑(2 * n + 1)! : ℂ) / I
h₃ :
  Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * (HPow.hPow (β := ℕ) z 2 ^ n * z) / (↑(2 * n + 1)! : ℂ))
    fun (n : ℕ) ↦ HPow.hPow (β := ℕ) z 2 ^ n * z * (HPow.hPow (α := ℂ) (-1) n * I) / (↑(2 * n + 1)! : ℂ) / I
h₄ :
  Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * HPow.hPow (β := ℕ) z 2 ^ n * z / (↑(2 * n + 1)! : ℂ))
    fun (n : ℕ) ↦ HPow.hPow (β := ℕ) z 2 ^ n * z * HPow.hPow (α := ℂ) (-1) n * I / (↑(2 * n + 1)! : ℂ) / I
h₅ :
  Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * HPow.hPow (β := ℕ) z 2 ^ n * (z / (↑(2 * n + 1)! : ℂ)))
    fun (n : ℕ) ↦ HPow.hPow (β := ℕ) z 2 ^ n * z * HPow.hPow (α := ℂ) (-1) n * (I / (↑(2 * n + 1)! : ℂ) / I)
h₆ :
  Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * HPow.hPow (β := ℕ) z 2 ^ n * (z / (↑(2 * n + 1)! : ℂ)))
    fun (n : ℕ) ↦ HPow.hPow (β := ℕ) z 2 ^ n * z * HPow.hPow (α := ℂ) (-1) n * (I / I / (↑(2 * n + 1)! : ℂ))
h₇ :
  Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * HPow.hPow (β := ℕ) z 2 ^ n * (z / (↑(2 * n + 1)! : ℂ)))
    fun (n : ℕ) ↦ HPow.hPow (β := ℕ) z 2 ^ n * z * HPow.hPow (α := ℂ) (-1) n * HDiv.hDiv (α := ℂ) 1 (↑(2 * n + 1)! : ℂ)
h₈ :
  Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * HPow.hPow (β := ℕ) z 2 ^ n * (z / (↑(2 * n + 1)! : ℂ)))
    fun (n : ℕ) ↦
    HPow.hPow (α := ℂ) (-1) n * (HPow.hPow (β := ℕ) z 2 ^ n * z) * HDiv.hDiv (α := ℂ) 1 (↑(2 * n + 1)! : ℂ)
h₉ :
  Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * HPow.hPow (β := ℕ) z 2 ^ n * (z / (↑(2 * n + 1)! : ℂ)))
    fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * (HPow.hPow (β := ℕ) z 2 ^ n * z) / (↑(2 * n + 1)! : ℂ)
h₁₀ :
  Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * HPow.hPow (β := ℕ) z 2 ^ n * (z / (↑(2 * n + 1)! : ℂ)))
    fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * (HPow.hPow (β := ℕ) z 2 ^ n * (z / (↑(2 * n + 1)! : ℂ)))
⊢ Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * z ^ (2 * n + 1) / (↑(2 * n + 1)! : ℂ)) fun (n : ℕ) ↦
    (z * I) ^ (2 * n + 1) / (↑(2 * n + 1)! : ℂ) / I

Tactic:
simp_rw [mul_pow, pow_succ, pow_mul, Complex.I_sq, ← mul_assoc, mul_div_assoc, div_right_comm,
    div_self Complex.I_ne_zero, mul_comm _ ((-1 : ℂ) ^ _), mul_one_div, mul_div_assoc, mul_assoc]

Premises used: div_right_comm, pow_succ, mul_assoc, mul_div_assoc, Complex.I_ne_zero, pow_mul, HPow.hPow, mul_one_div, Complex.I_sq, mul_comm, OfNat.ofNat, mul_pow, Neg.neg, div_self
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Series
Goal:
z : ℂ
⊢ cos z = ∑' (n : ℕ), (z * I) ^ (2 * n) / (↑(2 * n)! : ℂ)

Tactic:
(Complex.hasSum_cos' z).tsum_eq.symm

Premises used: Complex.hasSum_cos', HasSum.tsum_eq, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Series
Goal:
z : ℂ
⊢ sin z = ∑' (n : ℕ), (z * I) ^ (2 * n + 1) / (↑(2 * n + 1)! : ℂ) / I

Tactic:
(Complex.hasSum_sin' z).tsum_eq.symm

Premises used: HasSum.tsum_eq, Complex.hasSum_sin', Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Series
Goal:
z : ℂ
⊢ cos z = ∑' (n : ℕ), HPow.hPow (α := ℂ) (-1) n * z ^ (2 * n) / (↑(2 * n)! : ℂ)

Tactic:
(Complex.hasSum_cos z).tsum_eq.symm

Premises used: HasSum.tsum_eq, Eq.symm, Complex.hasSum_cos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Series
Goal:
z : ℂ
⊢ sin z = ∑' (n : ℕ), HPow.hPow (α := ℂ) (-1) n * z ^ (2 * n + 1) / (↑(2 * n + 1)! : ℂ)

Tactic:
(Complex.hasSum_sin z).tsum_eq.symm

Premises used: Complex.hasSum_sin, HasSum.tsum_eq, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Series
Goal:
r : ℝ
⊢ HasSum (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (-1) n * r ^ (2 * n) / (↑(2 * n)! : ℝ)) (cos r)

Tactic:
mod_cast Complex.hasSum_cos r

Premises used: Int.cast_neg, Int.cast, HMul.hMul, Complex.cos, Real.cos, congrArg, Complex.hasSum_ofReal._simp_1, Int.cast_negSucc._simp_1, Complex.ofReal_div._simp_1, Int.cast_pow, Complex.ofReal_neg, cast, HDiv.hDiv, Complex.ofReal_pow._simp_1, Complex.ofReal, Nat.cast, Complex.ofReal_mul._simp_1, funext, HPow.hPow, Complex.ofReal_cos._simp_1, Nat.factorial, HasSum, Nat, congr, Int.cast_pow._simp_1, congrFun', Int.negSucc, OfNat.ofNat, Eq.symm, Complex.ofReal_pow, Complex.hasSum_cos, Nat.cast_one, Neg.neg, Int.cast_one, SummationFilter.unconditional, Eq.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Series
Goal:
r : ℝ
⊢ HasSum (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (-1) n * r ^ (2 * n + 1) / (↑(2 * n + 1)! : ℝ)) (sin r)

Tactic:
mod_cast Complex.hasSum_sin r

Premises used: Int.cast_neg, Int.cast, HMul.hMul, congrArg, Complex.hasSum_ofReal._simp_1, Int.cast_negSucc._simp_1, Complex.sin, Complex.ofReal_div._simp_1, Int.cast_pow, Complex.ofReal_neg, cast, Complex.hasSum_sin, HDiv.hDiv, Complex.ofReal_pow._simp_1, Complex.ofReal, Nat.cast, Complex.ofReal_mul._simp_1, funext, HPow.hPow, HAdd.hAdd, Nat.factorial, HasSum, Nat, congr, Int.cast_pow._simp_1, Complex.ofReal_sin._simp_1, congrFun', Int.negSucc, OfNat.ofNat, Eq.symm, Complex.ofReal_pow, Nat.cast_one, Real.sin, Neg.neg, Int.cast_one, SummationFilter.unconditional, Eq.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Series
Goal:
r : ℝ
⊢ cos r = ∑' (n : ℕ), HPow.hPow (α := ℝ) (-1) n * r ^ (2 * n) / (↑(2 * n)! : ℝ)

Tactic:
(Real.hasSum_cos r).tsum_eq.symm

Premises used: Real.hasSum_cos, HasSum.tsum_eq, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Series
Goal:
r : ℝ
⊢ sin r = ∑' (n : ℕ), HPow.hPow (α := ℝ) (-1) n * r ^ (2 * n + 1) / (↑(2 * n + 1)! : ℝ)

Tactic:
(Real.hasSum_sin r).tsum_eq.symm

Premises used: HasSum.tsum_eq, Real.hasSum_sin, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Series
Goal:
z : ℂ
⊢ HasSum (fun (n : ℕ) ↦ z ^ (2 * n) / (↑(2 * n)! : ℂ)) (cosh z)

Tactic:
simpa [mul_assoc, cos_mul_I] using hasSum_cos' (z * I)

Premises used: Complex.cos_mul_I, HMul.hMul, mul_assoc, Complex.hasSum_cos', Complex.I
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Series
Goal:
z : ℂ
⊢ HasSum (fun (n : ℕ) ↦ z ^ (2 * n + 1) / (↑(2 * n + 1)! : ℂ)) (sinh z)

Tactic:
simpa [mul_assoc, sin_mul_I, neg_pow z, pow_add, pow_mul, neg_mul, neg_div]
    using (hasSum_sin' (z * I)).mul_right (-I)

Premises used: neg_div, HMul.hMul, mul_assoc, pow_add, pow_mul, neg_pow, Complex.sin_mul_I, neg_mul, Complex.hasSum_sin', HasSum.mul_right, Neg.neg, Complex.I
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Series
Goal:
z : ℂ
⊢ cosh z = ∑' (n : ℕ), z ^ (2 * n) / (↑(2 * n)! : ℂ)

Tactic:
z.hasSum_cosh.tsum_eq.symm

Premises used: HasSum.tsum_eq, Eq.symm, Complex.hasSum_cosh
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Series
Goal:
z : ℂ
⊢ sinh z = ∑' (n : ℕ), z ^ (2 * n + 1) / (↑(2 * n + 1)! : ℂ)

Tactic:
z.hasSum_sinh.tsum_eq.symm

Premises used: HasSum.tsum_eq, Complex.hasSum_sinh, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Series
Goal:
r : ℝ
⊢ HasSum (fun (n : ℕ) ↦ r ^ (2 * n) / (↑(2 * n)! : ℝ)) (cosh r)

Tactic:
mod_cast Complex.hasSum_cosh r

Premises used: HMul.hMul, congrArg, Complex.hasSum_ofReal._simp_1, Complex.ofReal_div._simp_1, cast, HDiv.hDiv, Complex.ofReal_pow._simp_1, Complex.ofReal, Nat.cast, funext, HPow.hPow, Nat.factorial, HasSum, Nat, congr, Complex.ofReal_cosh._simp_1, congrFun', OfNat.ofNat, Complex.hasSum_cosh, SummationFilter.unconditional, Eq.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Series
Goal:
r : ℝ
⊢ HasSum (fun (n : ℕ) ↦ r ^ (2 * n + 1) / (↑(2 * n + 1)! : ℝ)) (sinh r)

Tactic:
mod_cast Complex.hasSum_sinh r

Premises used: HMul.hMul, congrArg, Complex.hasSum_ofReal._simp_1, Complex.ofReal_div._simp_1, Complex.ofReal_sinh._simp_1, cast, HDiv.hDiv, Complex.ofReal_pow._simp_1, Complex.ofReal, Nat.cast, funext, HPow.hPow, HAdd.hAdd, Nat.factorial, HasSum, Nat, congr, congrFun', Complex.hasSum_sinh, OfNat.ofNat, SummationFilter.unconditional, Eq.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Series
Goal:
r : ℝ
⊢ cosh r = ∑' (n : ℕ), r ^ (2 * n) / (↑(2 * n)! : ℝ)

Tactic:
r.hasSum_cosh.tsum_eq.symm

Premises used: Real.hasSum_cosh, HasSum.tsum_eq, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Series
Goal:
r : ℝ
⊢ sinh r = ∑' (n : ℕ), r ^ (2 * n + 1) / (↑(2 * n + 1)! : ℝ)

Tactic:
r.hasSum_sinh.tsum_eq.symm

Premises used: Real.hasSum_sinh, HasSum.tsum_eq, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Series
Goal:
x : ℝ
rw :
  LE.le (α := ℝ) (∑' (n : ℕ), x ^ (2 * n) / (↑(2 * n)! : ℝ))
    ((fun (x : ℝ) ↦ (∑' (n : ℕ), HSMul.hSMul (α := ℝ) (↑n ! : ℝ)⁻¹ (x ^ n) : ℝ)) (HPow.hPow (β := ℕ) x 2 / 2))
⊢ cosh x ≤ rexp (HPow.hPow (β := ℕ) x 2 / 2)

Tactic:
rw [cosh_eq_tsum, exp_eq_exp_ℝ, exp_eq_tsum ℝ]

Premises used: Real, NormedSpace.exp_eq_tsum, Real.exp_eq_exp_ℝ, Real.cosh_eq_tsum
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Series
Goal:
x : ℝ
⊢ LE.le (α := ℝ) (∑' (n : ℕ), x ^ (2 * n) / (↑(2 * n)! : ℝ))
    ((fun (x : ℝ) ↦ (∑' (n : ℕ), HSMul.hSMul (α := ℝ) (↑n ! : ℝ)⁻¹ (x ^ n) : ℝ)) (HPow.hPow (β := ℕ) x 2 / 2))

Tactic:
x.hasSum_cosh.summable.tsum_le_tsum (fun i ↦ ?_) <| expSeries_summable' (x ^ 2 / 2)

Premises used: Real.hasSum_cosh, HDiv.hDiv, NormedSpace.expSeries_summable', Summable.tsum_le_tsum, HasSum.summable, HPow.hPow, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Series
Goal:
x : ℝ
refine : ∀ (i : ℕ), x ^ (2 * i) / (↑(2 * i)! : ℝ) ≤ HSMul.hSMul (α := ℝ) (↑i ! : ℝ)⁻¹ ((HPow.hPow (β := ℕ) x 2 / 2) ^ i)
⊢ LE.le (α := ℝ) (∑' (n : ℕ), x ^ (2 * n) / (↑(2 * n)! : ℝ))
    ((fun (x : ℝ) ↦ (∑' (n : ℕ), HSMul.hSMul (α := ℝ) (↑n ! : ℝ)⁻¹ (x ^ n) : ℝ)) (HPow.hPow (β := ℕ) x 2 / 2))

Tactic:
refine x.hasSum_cosh.summable.tsum_le_tsum (fun i ↦ ?_) <| expSeries_summable' (x ^ 2 / 2)

Premises used: Real.hasSum_cosh, HDiv.hDiv, NormedSpace.expSeries_summable', Summable.tsum_le_tsum, HasSum.summable, HPow.hPow, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Series
Goal:
x : ℝ
i : ℕ
simp : HPow.hPow (β := ℕ) x 2 ^ i / (↑(2 * i)! : ℝ) ≤ HPow.hPow (β := ℕ) x 2 ^ i / (HPow.hPow (α := ℝ) 2 i * (↑i ! : ℝ))
⊢ x ^ (2 * i) / (↑(2 * i)! : ℝ) ≤ HSMul.hSMul (α := ℝ) (↑i ! : ℝ)⁻¹ ((HPow.hPow (β := ℕ) x 2 / 2) ^ i)

Tactic:
simp only [div_pow, pow_mul, smul_eq_mul, inv_mul_eq_div, div_div]

Premises used: inv_mul_eq_div, pow_mul, div_pow, smul_eq_mul, div_div
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Series
Goal:
x : ℝ
i : ℕ
hdb : HPow.hPow (α := ℝ) 2 i * (↑i ! : ℝ) ≤ (↑(2 * i)! : ℝ)
⊢ HPow.hPow (β := ℕ) x 2 ^ i / (↑(2 * i)! : ℝ) ≤ HPow.hPow (β := ℕ) x 2 ^ i / (HPow.hPow (α := ℝ) 2 i * (↑i ! : ℝ))

Tactic:
gcongr
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Series
Goal:
x : ℝ
i : ℕ
hdb : HPow.hPow (α := ℕ) 2 i * i ! ≤ (2 * i)!
⊢ HPow.hPow (α := ℝ) 2 i * (↑i ! : ℝ) ≤ (↑(2 * i)! : ℝ)

Tactic:
norm_cast
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Series
Goal:
x : ℝ
i : ℕ
⊢ HPow.hPow (α := ℕ) 2 i * i ! ≤ (2 * i)!

Tactic:
Nat.two_pow_mul_factorial_le_factorial_two_mul _

Premises used: Nat.two_pow_mul_factorial_le_factorial_two_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Series
Goal:
x : ℝ
i : ℕ
⊢ HPow.hPow (α := ℕ) 2 i * i ! ≤ (2 * i)!

Tactic:
exact Nat.two_pow_mul_factorial_le_factorial_two_mul _

Premises used: Nat.two_pow_mul_factorial_le_factorial_two_mul
-- Module: Mathlib.Analysis.SpecificLimits.ArithmeticGeometric
Goal:
R : Type u_1
a b u₀ : R
inst : Mul R
inst_1 : Add R
⊢ arithGeom a b u₀ 0 = u₀

Tactic:
rfl

Premises used: arithGeom, rfl
-- Module: Mathlib.Analysis.SpecificLimits.ArithmeticGeometric
Goal:
R : Type u_1
a b u₀ : R
inst : Mul R
inst_1 : Add R
n : ℕ
⊢ arithGeom a b u₀ (n + 1) = a * arithGeom a b u₀ n + b

Tactic:
rfl

Premises used: arithGeom, rfl
-- Module: Mathlib.Analysis.SpecificLimits.ArithmeticGeometric
Goal:
R : Type u_1
a b u₀ : R
inst : CommSemiring R
⊢ arithGeom a b u₀ 0 = HPow.hPow (β := ℕ) a 0 * u₀ + b * ∑ k ∈ Finset.range 0, a ^ k

Tactic:
simp
-- Module: Mathlib.Analysis.SpecificLimits.ArithmeticGeometric
Goal:
R : Type u_1
a b u₀ : R
inst : CommSemiring R
n : ℕ
hn : arithGeom a b u₀ n = a ^ n * u₀ + b * ∑ k ∈ Finset.range n, a ^ k
succ :
  a * a ^ n * u₀ + (a * (b * ∑ k ∈ Finset.range n, a ^ k) + b) = a * a ^ n * u₀ + b * ∑ k ∈ Finset.range (1 + n), a ^ k
⊢ arithGeom a b u₀ (n + 1) = a ^ (n + 1) * u₀ + b * ∑ k ∈ Finset.range (n + 1), a ^ k

Tactic:
rw [arithGeom_succ, hn, mul_add, ← mul_assoc, add_comm n, pow_add, pow_one, add_assoc]

Premises used: arithGeom_succ, add_assoc, mul_assoc, pow_add, add_comm, pow_one, mul_add
-- Module: Mathlib.Analysis.SpecificLimits.ArithmeticGeometric
Goal:
R : Type u_1
a b u₀ : R
inst : CommSemiring R
n : ℕ
hn : arithGeom a b u₀ n = a ^ n * u₀ + b * ∑ k ∈ Finset.range n, a ^ k
succ : a * (b * ∑ k ∈ Finset.range n, a ^ k) + b = b * ∑ k ∈ Finset.range (1 + n), a ^ k
⊢ a * a ^ n * u₀ + (a * (b * ∑ k ∈ Finset.range n, a ^ k) + b) = a * a ^ n * u₀ + b * ∑ k ∈ Finset.range (1 + n), a ^ k

Tactic:
congr
-- Module: Mathlib.Analysis.SpecificLimits.ArithmeticGeometric
Goal:
R : Type u_1
a b u₀ : R
inst : CommSemiring R
n : ℕ
hn : arithGeom a b u₀ n = a ^ n * u₀ + b * ∑ k ∈ Finset.range n, a ^ k
succ : ∑ i ∈ Finset.range n, a * (b * a ^ i) + b = ∑ i ∈ Finset.range n, b * a ^ (i + 1) + b
⊢ a * (b * ∑ k ∈ Finset.range n, a ^ k) + b = b * ∑ k ∈ Finset.range (1 + n), a ^ k

Tactic:
rw [add_comm _ n, Finset.sum_range_succ', Finset.mul_sum, pow_zero, mul_add, mul_one,
      Finset.mul_sum, Finset.mul_sum]

Premises used: Finset.mul_sum, add_comm, pow_zero, mul_add, mul_one, Finset.sum_range_succ'
-- Module: Mathlib.Analysis.SpecificLimits.ArithmeticGeometric
Goal:
R : Type u_1
a b u₀ : R
inst : CommSemiring R
n : ℕ
hn : arithGeom a b u₀ n = a ^ n * u₀ + b * ∑ k ∈ Finset.range n, a ^ k
succ : ∀ (k : ℕ), a * (b * a ^ k) = b * a ^ (k + 1)
⊢ ∑ i ∈ Finset.range n, a * (b * a ^ i) + b = ∑ i ∈ Finset.range n, b * a ^ (i + 1) + b

Tactic:
congr with k
-- Module: Mathlib.Analysis.SpecificLimits.ArithmeticGeometric
Goal:
R : Type u_1
a b u₀ : R
inst : CommSemiring R
n : ℕ
hn : arithGeom a b u₀ n = a ^ n * u₀ + b * ∑ k ∈ Finset.range n, a ^ k
k : ℕ
⊢ a * (b * a ^ k) = b * a ^ (k + 1)

Tactic:
ring
-- Module: Mathlib.Analysis.SpecificLimits.ArithmeticGeometric
Goal:
R : Type u_1
a b u₀ : R
inst : CommSemiring R
n : ℕ
zero : arithGeom a b u₀ 0 = HPow.hPow (β := ℕ) a 0 * u₀ + b * ∑ k ∈ Finset.range 0, a ^ k
succ :
  ∀ (n : ℕ) (hn : arithGeom a b u₀ n = a ^ n * u₀ + b * ∑ k ∈ Finset.range n, a ^ k),
    arithGeom a b u₀ (n + 1) = a ^ (n + 1) * u₀ + b * ∑ k ∈ Finset.range (n + 1), a ^ k
⊢ arithGeom a b u₀ n = a ^ n * u₀ + b * ∑ k ∈ Finset.range n, a ^ k

Tactic:
induction n with
  | zero => simp
  | succ n hn =>
    rw [arithGeom_succ, hn, mul_add, ← mul_assoc, add_comm n, pow_add, pow_one, add_assoc]
    congr
    rw [add_comm _ n, Finset.sum_range_succ', Finset.mul_sum, pow_zero, mul_add, mul_one,
      Finset.mul_sum, Finset.mul_sum]
    congr with k
    ring

Premises used: arithGeom_succ, Finset.mul_sum, add_assoc, mul_assoc, pow_add, add_comm, pow_zero, pow_one, mul_add, mul_one, Finset.sum_range_succ'
-- Module: Mathlib.Analysis.SpecificLimits.ArithmeticGeometric
Goal:
R : Type u_1
a b : R
inst : CommSemiring R
n : ℕ
rw : a ^ n * b + b * ∑ k ∈ Finset.range n, a ^ k = b * ∑ k ∈ Finset.range (n + 1), a ^ k
rw₁ : a ^ n * b + b * ∑ k ∈ Finset.range n, a ^ k = b * (∑ x ∈ Finset.range n, a ^ x + a ^ n)
rw₂ : a ^ n * b + b * ∑ k ∈ Finset.range n, a ^ k = b * ∑ x ∈ Finset.range n, a ^ x + b * a ^ n
rw₃ : b * ∑ k ∈ Finset.range n, a ^ k + a ^ n * b = b * ∑ x ∈ Finset.range n, a ^ x + b * a ^ n
rw₄ rw₅ : b * ∑ k ∈ Finset.range n, a ^ k + b * a ^ n = b * ∑ x ∈ Finset.range n, a ^ x + b * a ^ n
⊢ arithGeom a b b n = b * ∑ k ∈ Finset.range (n + 1), a ^ k

Tactic:
rw [arithGeom_eq_add_sum, Finset.sum_range_succ, mul_add, add_comm, mul_comm _ b]

Premises used: arithGeom_eq_add_sum, add_comm, mul_comm, mul_add, Finset.sum_range_succ
-- Module: Mathlib.Analysis.SpecificLimits.ArithmeticGeometric
Goal:
R : Type u_1
a b : R
inst : CommSemiring R
n : ℕ
⊢ arithGeom a b 0 n = b * ∑ k ∈ Finset.range n, a ^ k

Tactic:
simp [arithGeom_eq_add_sum]

Premises used: arithGeom_eq_add_sum
-- Module: Mathlib.Analysis.SpecificLimits.ArithmeticGeometric
Goal:
R : Type u_1
a b u₀ : R
inst : Field R
ha : a ≠ 1
⊢ arithGeom a b u₀ 0 = HPow.hPow (β := ℕ) a 0 * (u₀ - b / (1 - a)) + b / (1 - a)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecificLimits.ArithmeticGeometric
Goal:
R : Type u_1
a b u₀ : R
inst : Field R
ha : a ≠ 1
n : ℕ
hn : arithGeom a b u₀ n = a ^ n * (u₀ - b / (1 - a)) + b / (1 - a)
succ : a * arithGeom a b u₀ n + b = a ^ (n + 1) * (u₀ - b / (1 - a)) + b / (1 - a)
⊢ arithGeom a b u₀ (n + 1) = a ^ (n + 1) * (u₀ - b / (1 - a)) + b / (1 - a)

Tactic:
unfold arithGeom

Premises used: arithGeom
-- Module: Mathlib.Analysis.SpecificLimits.ArithmeticGeometric
Goal:
R : Type u_1
a b u₀ : R
inst : Field R
ha : a ≠ 1
n : ℕ
hn : arithGeom a b u₀ n = a ^ n * (u₀ - b / (1 - a)) + b / (1 - a)
⊢ a * arithGeom a b u₀ n + b = a ^ (n + 1) * (u₀ - b / (1 - a)) + b / (1 - a)

Tactic:
grind
-- Module: Mathlib.Analysis.SpecificLimits.ArithmeticGeometric
Goal:
R : Type u_1
a b u₀ : R
inst : Field R
ha : a ≠ 1
n : ℕ
zero : arithGeom a b u₀ 0 = HPow.hPow (β := ℕ) a 0 * (u₀ - b / (1 - a)) + b / (1 - a)
succ :
  ∀ (n : ℕ) (hn : arithGeom a b u₀ n = a ^ n * (u₀ - b / (1 - a)) + b / (1 - a)),
    arithGeom a b u₀ (n + 1) = a ^ (n + 1) * (u₀ - b / (1 - a)) + b / (1 - a)
⊢ arithGeom a b u₀ n = a ^ n * (u₀ - b / (1 - a)) + b / (1 - a)

Tactic:
induction n with
  | zero => simp
  | succ n hn => unfold arithGeom; grind

Premises used: arithGeom
-- Module: Mathlib.Analysis.SpecificLimits.ArithmeticGeometric
Goal:
R : Type u_1
a b u₀ : R
inst : Field R
ha : a ≠ 1
h : ∀ (x : ℕ), arithGeom a b u₀ x = a ^ x * (u₀ - b / (1 - a)) + b / (1 - a)
⊢ arithGeom a b u₀ = fun (n : ℕ) ↦ a ^ n * (u₀ - b / (1 - a)) + b / (1 - a)

Tactic:
ext
-- Module: Mathlib.Analysis.SpecificLimits.ArithmeticGeometric
Goal:
R : Type u_1
a b u₀ : R
inst : Field R
ha : a ≠ 1
x : ℕ
⊢ arithGeom a b u₀ x = a ^ x * (u₀ - b / (1 - a)) + b / (1 - a)

Tactic:
arithGeom_eq ha _

Premises used: arithGeom_eq
-- Module: Mathlib.Analysis.SpecificLimits.ArithmeticGeometric
Goal:
R : Type u_1
a b u₀ : R
inst : Field R
ha : a ≠ 1
x : ℕ
⊢ arithGeom a b u₀ x = a ^ x * (u₀ - b / (1 - a)) + b / (1 - a)

Tactic:
exact arithGeom_eq ha _

Premises used: arithGeom_eq
-- Module: Mathlib.Analysis.SpecificLimits.ArithmeticGeometric
Goal:
R : Type u_1
a b : R
inst : Field R
ha : a ≠ 1
n : ℕ
rw : a ^ n * (b - b / (1 - a)) + b / (1 - a) = b * (1 - a ^ (n + 1)) / (1 - a)
⊢ arithGeom a b b n = b * (1 - a ^ (n + 1)) / (1 - a)

Tactic:
rw [arithGeom_eq ha n]

Premises used: arithGeom_eq
-- Module: Mathlib.Analysis.SpecificLimits.ArithmeticGeometric
Goal:
R : Type u_1
a b : R
inst : Field R
ha : a ≠ 1
n : ℕ
⊢ a ^ n * (b - b / (1 - a)) + b / (1 - a) = b * (1 - a ^ (n + 1)) / (1 - a)

Tactic:
field [sub_ne_zero.mpr ha.symm]

Premises used: Iff.mpr, sub_ne_zero, Ne.symm
-- Module: Mathlib.Analysis.SpecificLimits.ArithmeticGeometric
Goal:
R : Type u_1
a b : R
inst : Field R
ha : a ≠ 1
n : ℕ
rw : b * (1 - a ^ (n + 1)) / (1 - a) = b * (a ^ (n + 1) - 1) / (a - 1)
rw₁ : b * (1 - a ^ (n + 1)) / (1 - a) = b * (a ^ (n + 1) - 1) / -(1 - a)
rw₂ : b * (1 - a ^ (n + 1)) / (1 - a) = -(b * (a ^ (n + 1) - 1) / (1 - a))
rw₃ : b * (1 - a ^ (n + 1)) / (1 - a) = -(b * -(1 - a ^ (n + 1)) / (1 - a))
rw₄ : b * (1 - a ^ (n + 1)) / (1 - a) = -(-(b * (1 - a ^ (n + 1))) / (1 - a))
rw₅ : b * (1 - a ^ (n + 1)) / (1 - a) = - -(b * (1 - a ^ (n + 1)) / (1 - a))
rw₆ rw₇ : b * (1 - a ^ (n + 1)) / (1 - a) = b * (1 - a ^ (n + 1)) / (1 - a)
⊢ arithGeom a b b n = b * (a ^ (n + 1) - 1) / (a - 1)

Tactic:
rw [arithGeom_same_eq_mul_div' ha n, ← neg_sub _ a, div_neg,
    ← neg_sub _ (a ^ (n + 1)), mul_neg, neg_div, neg_neg]

Premises used: neg_sub, neg_div, arithGeom_same_eq_mul_div', neg_neg, HPow.hPow, HAdd.hAdd, div_neg, OfNat.ofNat, mul_neg
-- Module: Mathlib.Analysis.SpecificLimits.ArithmeticGeometric
Goal:
R : Type u_1
a b : R
inst : Field R
ha : a ≠ 1
n : ℕ
rw : a ^ n * (0 - b / (1 - a)) + b / (1 - a) = b * (1 - a ^ n) / (1 - a)
⊢ arithGeom a b 0 n = b * (1 - a ^ n) / (1 - a)

Tactic:
rw [arithGeom_eq ha n]

Premises used: arithGeom_eq
-- Module: Mathlib.Analysis.SpecificLimits.ArithmeticGeometric
Goal:
R : Type u_1
a b : R
inst : Field R
ha : a ≠ 1
n : ℕ
⊢ a ^ n * (0 - b / (1 - a)) + b / (1 - a) = b * (1 - a ^ n) / (1 - a)

Tactic:
ring
-- Module: Mathlib.Analysis.SpecificLimits.ArithmeticGeometric
Goal:
R : Type u_1
a b : R
inst : Field R
ha : a ≠ 1
n : ℕ
rw : b * (1 - a ^ n) / (1 - a) = b * (a ^ n - 1) / (a - 1)
rw₁ : b * (1 - a ^ n) / (1 - a) = b * (a ^ n - 1) / -(1 - a)
rw₂ : b * (1 - a ^ n) / (1 - a) = -(b * (a ^ n - 1) / (1 - a))
rw₃ : b * (1 - a ^ n) / (1 - a) = -(b * -(1 - a ^ n) / (1 - a))
rw₄ : b * (1 - a ^ n) / (1 - a) = -(-(b * (1 - a ^ n)) / (1 - a))
rw₅ : b * (1 - a ^ n) / (1 - a) = - -(b * (1 - a ^ n) / (1 - a))
rw₆ rw₇ : b * (1 - a ^ n) / (1 - a) = b * (1 - a ^ n) / (1 - a)
⊢ arithGeom a b 0 n = b * (a ^ n - 1) / (a - 1)

Tactic:
rw [arithGeom_zero_eq_mul_div' ha n, ← neg_sub _ a, div_neg, ← neg_sub _ (a ^ n), mul_neg,
    neg_div, neg_neg]

Premises used: neg_sub, neg_div, arithGeom_zero_eq_mul_div', neg_neg, HPow.hPow, div_neg, mul_neg
-- Module: Mathlib.Analysis.SpecificLimits.ArithmeticGeometric
Goal:
R : Type u_1
a b u₀ : R
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
ha_pos : 0 < a
ha_ne : a ≠ 1
h0 : b / (1 - a) < u₀
⊢ b / (1 - a) < arithGeom a b u₀ 0

Tactic:
h0

Premises used: arithGeom
-- Module: Mathlib.Analysis.SpecificLimits.ArithmeticGeometric
Goal:
R : Type u_1
a b u₀ : R
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
ha_pos : 0 < a
ha_ne : a ≠ 1
h0 : b / (1 - a) < u₀
⊢ b / (1 - a) < arithGeom a b u₀ 0

Tactic:
exact h0