mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
⊢ sinh (x * I ^ 2) = -sinh x

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: case a
x : ℂ
h : I * sin (x * I) = -sinh x
⊢ (sin (x * I)).re = (-(I * sin (x * I)) * I).re

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: case a
x : ℂ
h : I * sin (x * I) = -sinh x
⊢ (sin (x * I)).im = (-(I * sin (x * I)) * I).im

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: 𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
m n : ℕ
h : m < n
⊢ (fun x ↦ x ^ n) =o[𝓝 0] fun x ↦ x ^ m

Tactic:
rcases lt_iff_exists_add.1 h with ⟨p, hp0 : 0 < p, rfl⟩

Goal state after:
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
m p : ℕ
hp0 : 0 < p
h : m < m + p
⊢ (fun x ↦ x ^ (m + p)) =o[𝓝 0] fun x ↦ x ^ m
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℂ
hx : ‖x‖ ≤ 1
⊢ ‖cexp x - 1‖ = ‖cexp x - ∑ m ∈ range 1, x ^ m / ↑m.factorial‖

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℝ
hx : ‖x‖ ≤ 1
⊢ ‖↑(Real.exp x) - 1 - ↑x‖ = ‖cexp ↑x - 1 - ↑x‖

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℝ
hx : ‖x‖ ≤ 1
⊢ ‖↑x‖ ≤ 1

Tactic:
exact_mod_cast hx

Goal state after:
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℝ
hx : ‖x‖ ≤ 1
⊢ ‖↑x‖ ^ 2 = ‖x‖ ^ 2

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
hx : ‖x‖ ≤ 1
⊢ ‖(cexp (-x * I) - ∑ m ∈ range 4, (-x * I) ^ m / ↑m.factorial) / 2‖ +
      ‖(cexp (x * I) - ∑ m ∈ range 4, (x * I) ^ m / ↑m.factorial) / 2‖ ≤
    ‖cexp (-x * I) - ∑ m ∈ range 4, (-x * I) ^ m / ↑m.factorial‖ / 2 +
      ‖cexp (x * I) - ∑ m ∈ range 4, (x * I) ^ m / ↑m.factorial‖ / 2

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
hx : ‖x‖ ≤ 1
⊢ 0 < 4

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: case e'_3
x : ℂ
⊢ cexp x = cexp x - ∑ m ∈ range 0, x ^ m / ↑m.factorial

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: case e'_4
x : ℂ
⊢ Real.exp ‖x‖ = Real.exp ‖x‖ - ∑ m ∈ range 0, ‖x‖ ^ m / ↑m.factorial

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
hx : ‖x‖ ≤ 1
⊢ ‖(cexp (-x * I) - ∑ m ∈ range 5, (-x * I) ^ m / ↑m.factorial) * I / 2‖ +
      ‖(cexp (x * I) - ∑ m ∈ range 5, (x * I) ^ m / ↑m.factorial) * I / 2‖ ≤
    ‖cexp (-x * I) - ∑ m ∈ range 5, (-x * I) ^ m / ↑m.factorial‖ / 2 +
      ‖cexp (x * I) - ∑ m ∈ range 5, (x * I) ^ m / ↑m.factorial‖ / 2

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
hx : ‖x‖ ≤ 1
⊢ 0 < 5

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: case h
x : ℂ
n j : ℕ
hj : j ≥ n
i : ℕ
hi : i ∈ Ico n j
⊢ i - n ≤ i

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ ↑(tan x)⁻¹ = ↑x.cot

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ ↑x.cot⁻¹ = ↑(tan x)

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ ↑(cosh (-x)) = ↑(cosh x)

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ ↑(cosh x + sinh x) = ↑(rexp x)

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ ↑(cosh x - sinh x) = ↑(rexp (-x))

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ ↑(cosh x ^ 2 - sinh x ^ 2) = ↑1

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
hx0 : 0 < x
hx : x ≤ 2
⊢ 0 < 2

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
hx0 : 0 < x
hx : x ≤ 2
this : x / 2 ≤ 1
⊢ 0 < 2

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: ⊢ |1| ≤ 1

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ ‖cexp (↑x * I)‖₊ = 1

Tactic:
← nnnorm_norm,

Goal state after:
x : ℝ
⊢ ‖‖cexp (↑x * I)‖‖₊ = 1
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ ↑‖1‖₊ = 1

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ ‖cexp (I * ↑x)‖₊ = 1

Tactic:
← nnnorm_norm,

Goal state after:
x : ℝ
⊢ ‖‖cexp (I * ↑x)‖‖₊ = 1
Module: Mathlib.Algebra.Order.Field.Power

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
p : ℤ
⊢ |(-1) ^ p| = 1

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: n : ℕ
a₁ b₁ : ℝ
m : ℕ
en : n + 1 = m
h : |rexp 1 - expNear m 1 ((a₁ - 1) * ↑m)| ≤ |1| ^ m / ↑m.factorial * (b₁ * ↑m)
⊢ |1 + 1 / ↑m * ((a₁ - 1) * ↑m) - a₁| ≤ b₁ - |1| / ↑m * (b₁ * ↑m)

Tactic:
simp

Goal state after:
n : ℕ
a₁ b₁ : ℝ
m : ℕ
en : n + 1 = m
h : |rexp 1 - expNear m 1 ((a₁ - 1) * ↑m)| ≤ |1| ^ m / ↑m.factorial * (b₁ * ↑m)
⊢ |1 + (↑m)⁻¹ * ((a₁ - 1) * ↑m) - a₁| ≤ b₁ - (↑m)⁻¹ * (b₁ * ↑m)
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: n : ℕ
a₁ b₁ : ℝ
m : ℕ
en : n + 1 = m
h : |rexp 1 - expNear m 1 ((a₁ - 1) * ↑m)| ≤ |1| ^ m / ↑m.factorial * (b₁ * ↑m)
⊢ |1 + (a₁ - 1) - a₁| ≤ b₁ * (1 - 1)

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: case inl
h1 : 0 ≤ 0
h2 : 0 < 1
⊢ rexp 0 ≤ 1 / (1 - 0)

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: case inl
⊢ 0 + 1 ≤ rexp 0

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: case inl
t : ℝ
ht' : t ≤ ↑0
⊢ (1 - t / ↑0) ^ 0 ≤ rexp (-t)

Tactic:
simp

Goal state after:
case inl
t : ℝ
ht' : t ≤ ↑0
⊢ t ≤ 0
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: case e'_4
n : ℕ
⊢ rexp 1 = rexp (- -1)

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℝ
hx : 0 < x
hx' : x < 2
⊢ 0 < 3

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: case inl
hx : 0 ≤ 0
hx' : 0 < 2
⊢ rexp 0 ≤ (2 + 0) / (2 - 0)

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: F : Type u_1
ι : Type u_2
inst✝³ : NormedRing F
inst✝² : NormMulClass F
inst✝¹ : NormOneClass F
inst✝ : CompleteSpace F
f g : ι → F
hf : Summable fun n ↦ ‖f n‖
c : F
hg : Tendsto g cofinite (𝓝 c)
⊢ Summable fun n ↦ f n * g n

Tactic:
by
  apply summable_of_isBigO hf
  simpa using (isBigO_const_mul_self 1 f _).mul (hg.isBigO_one F)

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.BigOperators

Goal state before:
pp: α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : Archimedean α
f : ℕ → α
a : α
m : ℕ
ham : ∀ n ≥ m, |f n| ≤ a
hnm : ∀ n ≥ m, f n.succ ≤ f n
ε : α
ε0 : ε > 0
k : ℕ
hk : a ≤ k • ε
h : ∃ l, ∀ n ≥ m, a - l • ε < f n
l : ℕ := Nat.find h
hl : ∀ n ≥ m, f n > a - l • ε
hl0 : l ≠ 0
i : ℕ
hi : i ≥ m ∧ f i ≤ a - (Nat.find h).pred • ε
⊢ ∀ j ≥ i, |f j - f i| < ε

Tactic:
intro j

Goal state after:
α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : Archimedean α
f : ℕ → α
a : α
m : ℕ
ham : ∀ n ≥ m, |f n| ≤ a
hnm : ∀ n ≥ m, f n.succ ≤ f n
ε : α
ε0 : ε > 0
k : ℕ
hk : a ≤ k • ε
h : ∃ l, ∀ n ≥ m, a - l • ε < f n
l : ℕ := Nat.find h
hl : ∀ n ≥ m, f n > a - l • ε
hl0 : l ≠ 0
i : ℕ
hi : i ≥ m ∧ f i ≤ a - (Nat.find h).pred • ε
j : ℕ
⊢ j ≥ i → |f j - f i| < ε
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: a : ℝ
this : Continuous (cexp - 1)
⊢ UniformContinuousOn cexp {x | x.re ≤ a}

Tactic:
rw [Metric.uniformContinuousOn_iff, Metric.continuous_iff'] at *

Goal state after:
a : ℝ
this : ∀ (a : ℂ), ∀ ε > 0, ∀ᶠ (x : ℂ) in 𝓝 a, dist ((cexp - 1) x) ((cexp - 1) a) < ε
⊢ ∀ ε > 0, ∃ δ > 0, ∀ x ∈ {x | x.re ≤ a}, ∀ y ∈ {x | x.re ≤ a}, dist x y < δ → dist (cexp x) (cexp y) < ε
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: a ε : ℝ
hε : ε > 0
this✝ : ∀ (a : ℂ) (ε : ℝ), 0 < ε → ∀ᶠ (x : ℂ) in 𝓝 a, dist (cexp x) (cexp a) < ε
ha : 0 < ε / (2 * Real.exp a)
δ : ℝ
hδ : δ > 0 ∧ ∀ ⦃y : ℂ⦄, dist y 0 < δ → dist (cexp y) 1 < ε / (2 * Real.exp a)
x : ℂ
a✝ : x ∈ {x | x.re ≤ a}
y : ℂ
hy : y ∈ {x | x.re ≤ a}
hxy : ‖x - y‖ < δ
h3 : ‖cexp (x - y) - 1‖ < ε / (2 * Real.exp a)
this : cexp x - cexp y = cexp y * (cexp (x - y) - 1)
⊢ ‖(cexp (x - y) - 1) * cexp y‖ < ε

Tactic:
have hya : ‖cexp y‖ ≤ Real.exp a := by simpa only [norm_exp, Real.exp_le_exp]

Goal state after:
a ε : ℝ
hε : ε > 0
this✝ : ∀ (a : ℂ) (ε : ℝ), 0 < ε → ∀ᶠ (x : ℂ) in 𝓝 a, dist (cexp x) (cexp a) < ε
ha : 0 < ε / (2 * Real.exp a)
δ : ℝ
hδ : δ > 0 ∧ ∀ ⦃y : ℂ⦄, dist y 0 < δ → dist (cexp y) 1 < ε / (2 * Real.exp a)
x : ℂ
a✝ : x ∈ {x | x.re ≤ a}
y : ℂ
hy : y ∈ {x | x.re ≤ a}
hxy : ‖x - y‖ < δ
h3 : ‖cexp (x - y) - 1‖ < ε / (2 * Real.exp a)
this : cexp x - cexp y = cexp y * (cexp (x - y) - 1)
hya : ‖cexp y‖ ≤ Real.exp a
⊢ ‖(cexp (x - y) - 1) * cexp y‖ < ε
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: ⊢ 1 = rexp 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.BigOperators

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : Field α
inst✝⁴ : LinearOrder α
inst✝³ : IsStrictOrderedRing α
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : Archimedean α
f : ℕ → β
r : α
hr0 : 0 ≤ r
hr1 : r < 1
har1 : |r| < 1
hr : 0 < r
k : ℕ
ih :
  ∀ (n : ℕ),
    (∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)) →
      ∀ (m : ℕ), n.succ ≤ m → m = k + n.succ → abv (f m) ≤ abv (f n.succ) * r⁻¹ ^ n.succ * r ^ m
n : ℕ
h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)
m : ℕ
hmn : n.succ ≤ m
hk : m = k + 1 + n.succ
⊢ n.succ ≤ 0 + n.succ

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: b c : ℝ
n : ℕ
hb : 0 ≠ b
b' c' : ℝ
h : 0 < b'
x : ℝ
⊢ x ^ n / (b' * rexp x + c') = (fun x ↦ (b' * rexp x + c') / x ^ n)⁻¹ x

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.BigOperators

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : Field α
inst✝⁴ : LinearOrder α
inst✝³ : IsStrictOrderedRing α
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : Archimedean α
f : ℕ → β
r : α
hr0 : 0 ≤ r
hr1 : r < 1
har1 : |r| < 1
hr : 0 < r
k : ℕ
ih :
  ∀ (n : ℕ),
    (∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)) →
      ∀ (m : ℕ), n.succ ≤ m → m = k + n.succ → abv (f m) ≤ abv (f n.succ) * r⁻¹ ^ n.succ * r ^ m
n : ℕ
h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)
m : ℕ
hmn : n.succ ≤ m
hk : m = k + 1 + n.succ
kn : k + n.succ ≥ n.succ
⊢ n.succ ≤ k + n.succ

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ 1 ≤ 2

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ 0 < 2

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ sin (π / 2) * 0 + 0 * sin (π / 2) = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: ⊢ comap rexp (𝓝[Set.range rexp] 0) = atBot

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: this : sin (π / 2) = 1 ∨ sin (π / 2) = -1
h : sin (π / 2) = -1
⊢ ¬0 < -1

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Quotient

Goal state before:
pp: M : Type u_1
inst✝ : SeminormedCommGroup M
S T : Subgroup M
x : M ⧸ S
m : M
r ε : ℝ
⊢ 1 ∈ {m | ↑m = 1}

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: c : ℝ
hc : c < 0
f : ℕ → ℝ
hf : ∀ (i : ℕ), ↑i ≤ f i
⊢ Summable fun i ↦ rexp (c * f i)

Tactic:
refine (Real.summable_exp_nat_mul_iff.mpr hc).of_nonneg_of_le (fun _ ↦ by positivity) fun i ↦ ?_

Goal state after:
c : ℝ
hc : c < 0
f : ℕ → ℝ
hf : ∀ (i : ℕ), ↑i ≤ f i
i : ℕ
⊢ rexp (c * f i) ≤ rexp (↑i * c)
Module: Mathlib.Analysis.Normed.Group.Quotient

Goal state before:
pp: M : Type u_1
inst✝ : SeminormedCommGroup M
S : Subgroup M
x : M
⊢ infDist ((IsometryEquiv.divLeft x) 1) (⇑(IsometryEquiv.divLeft x).symm ⁻¹' {m | ↑m = ↑x}) = infDist x ↑S

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Quotient

Goal state before:
pp: M : Type u_1
inst✝ : SeminormedCommGroup M
S : Subgroup M
m : M
⊢ m ∈ {m_1 | ↑m_1 = ↑m}

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: h : cos (↑0 * (2 * π)) = 1
hx₁ : -0 < 1
hx₂ : 0 < 1
⊢ ↑0 * (2 * π) = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Pointwise

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
x : E
⊢ {x} * ball 1 δ = ball x δ

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Pointwise

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
x : E
⊢ ball 1 δ * {x} = ball x δ

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Quotient

Goal state before:
pp: M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
m : M
⊢ infDist m ↑S = ⨅ a, ‖m + ↑a‖

Tactic:
← infDist_image isometry_neg,

Goal state after:
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
m : M
⊢ infDist (-m) (Neg.neg '' ↑S) = ⨅ a, ‖m + ↑a‖
Module: Mathlib.Analysis.Normed.Group.Pointwise

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
x : E
⊢ {x} * closedBall 1 δ = closedBall x δ

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Pointwise

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
x : E
⊢ closedBall 1 δ * {x} = closedBall x δ

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Pointwise

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
x : E
⊢ closedBall 1 δ / {x} = closedBall x⁻¹ δ

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Pointwise

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
x : E
⊢ x • closedBall 1 δ = closedBall x δ

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Pointwise

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
x : E
⊢ {x} * sphere 1 δ = sphere x δ

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Pointwise

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
x : E
⊢ sphere 1 δ * {x} = sphere x δ

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Pointwise

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
x : E
⊢ sphere 1 δ / {x} = sphere x⁻¹ δ

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Pointwise

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
x : E
⊢ x • sphere 1 δ = sphere x δ

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Quotient

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : f.IsQuotient
m : M
⊢ (fun m_1 ↦ ‖m + m_1‖) 0 = ‖m‖

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ -1 < 1

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: x : ℝ
⊢ x.sqrtTwoAddSeries 0 = x

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ sqrtTwoAddSeries 0 1 = √2

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ sqrtTwoAddSeries 0 2 = √(2 + √2)

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ sqrtTwoAddSeries 0 0 < 2

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Quotient

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝³ : SeminormedAddCommGroup M
inst✝² : SeminormedAddCommGroup N
R : Type u_3
inst✝¹ : Ring R
inst✝ : Module R M
S T : Submodule R M
⊢ map S.mkQ T = map S.mkQ (S ⊔ T)

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ cos (π / 2 ^ (0 + 1)) = sqrtTwoAddSeries 0 0 / 2

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: case inl.inl
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : NormSMulClass 𝕜 E
⊢ ‖0‖₊ • ediam ∅ ≤ ediam (0 • ∅)

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: n : ℕ
A : 1 < 2 ^ (n + 1)
B : π / 2 ^ (n + 1) < π
C : 0 < π / 2 ^ (n + 1)
⊢ cos (π / 2 ^ (n + 1 + 1)) = sqrtTwoAddSeries 0 (n + 1) / 2

Tactic:
rw [pow_succ, div_mul_eq_div_div, cos_half, cos_pi_over_two_pow n, sqrtTwoAddSeries,
      add_div_eq_mul_add_div, one_mul, ← div_mul_eq_div_div, sqrt_div, sqrt_mul_self] <;>
      linarith [sqrtTwoAddSeries_nonneg le_rfl n]

Goal state after:
Module: Mathlib.Analysis.Normed.Module.RCLike.Real

Goal state before:
pp: case inr.inr
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x y : E
hr✝ : dist y x ≠ 0
hr : 0 < dist y x
hy : y ∈ interior (closedBall x (dist y x))
f : ℝ → E := fun c ↦ c • (y - x) + x
c : ℝ
hc : c ∈ f ⁻¹' closedBall x (dist y x)
⊢ c ∈ Icc (-1) 1

Tactic:
rw [mem_Icc, ← abs_le, ← Real.norm_eq_abs, ← mul_le_mul_iff_left₀ hr]

Goal state after:
case inr.inr
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x y : E
hr✝ : dist y x ≠ 0
hr : 0 < dist y x
hy : y ∈ interior (closedBall x (dist y x))
f : ℝ → E := fun c ↦ c • (y - x) + x
c : ℝ
hc : c ∈ f ⁻¹' closedBall x (dist y x)
⊢ ‖c‖ * dist y x ≤ 1 * dist y x
Module: Mathlib.Analysis.Normed.Module.RCLike.Real

Goal state before:
pp: case inl
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
⊢ interior (closedBall x 0) = ball x 0

Tactic:
closedBall_zero,

Goal state after:
case inl
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
⊢ interior {x} = ball x 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ cos (π / 2 ^ 2) = √2 / 2

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ sin (π / 2 ^ 2) = √2 / 2

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ cos (π / 2 ^ 3) = √(2 + √2) / 2

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: k : ℕ
r : ℝ
hr : |r| < 1
⊢ Tendsto (fun n ↦ ↑n ^ k * r ^ n) atTop (𝓝 0)

Tactic:
by_cases h0 : r = 0
  · exact tendsto_const_nhds.congr'
      (mem_atTop_sets.2 ⟨1, fun n hn ↦ by simp [zero_lt_one.trans_le hn |>.ne', h0]⟩)
  have hr' : 1 < |r|⁻¹ := (one_lt_inv₀ (abs_pos.2 h0)).2 hr
  rw [tendsto_zero_iff_norm_tendsto_zero]
  simpa [div_eq_mul_inv] using tendsto_pow_const_div_const_pow_of_one_lt k hr'

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ sin (π / 2 ^ 3) = √(2 - √2) / 2

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ cos (π / 2 ^ 4) = √(2 + √(2 + √2)) / 2

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ sin (π / 2 ^ 4) = √(2 - √(2 + √2)) / 2

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ cos (π / 2 ^ 5) = √(2 + √(2 + √(2 + √2))) / 2

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ sin (π / 2 ^ 5) = √(2 - √(2 + √(2 + √2))) / 2

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: case base
R : Type u_2
inst✝¹ : SeminormedRing R
inst✝ : NormMulClass R
x : R
n : ℕ
⊢ ‖x ^ 1‖ = ‖x‖ ^ 1

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: R : Type u_2
S : Type u_3
inst✝⁵ : Field R
inst✝⁴ : Field S
inst✝³ : LinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : IsStrictOrderedRing S
inst✝ : Archimedean S
_i : OrderTopology S
v : AbsoluteValue R S
a : R
ha : v a < 1
h_add : Tendsto (fun x ↦ 1 + v a ^ x) atTop (𝓝 (1 + 0))
h_sub : Tendsto (fun x ↦ 1 - v a ^ x) atTop (𝓝 (1 - 0))
n : ℕ
⊢ 1 - v a ^ n ≤ v 1 - v (a ^ n)

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: R : Type u_2
S : Type u_3
inst✝⁵ : Field R
inst✝⁴ : Field S
inst✝³ : LinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : IsStrictOrderedRing S
inst✝ : Archimedean S
_i : OrderTopology S
v : AbsoluteValue R S
a : R
ha : v a < 1
h_add : Tendsto (fun x ↦ 1 + v a ^ x) atTop (𝓝 (1 + 0))
h_sub : Tendsto (fun x ↦ 1 - v a ^ x) atTop (𝓝 (1 - 0))
n : ℕ
⊢ v 1 + v (a ^ n) ≤ 1 + v a ^ n

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x z : E
δ ε : ℝ
hδ : 0 ≤ δ
hε : 0 ≤ ε
h : dist x z ≤ ε + δ
hε' : 0 < ε
hεδ : 0 < ε + δ
⊢ ε / (ε + δ) + δ / (ε + δ) = 1

Tactic:
by
      rw [← add_div, div_self hεδ.ne']

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: case e'_6
R : Type u_4
inst✝ : NormedRing R
x : R
h : ‖x‖ < 1
hx : Summable fun n ↦ x ^ n
⊢ 1 = ∑ i ∈ Finset.range 1, ‖x‖ ^ i

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: c : ℝ := cos (π / 5)
this : 4 * (c * c) + -2 * c + -1 = 0
hd : discrim 4 (-2) (-1) = 2 * √5 * (2 * √5)
⊢ 4 ≠ 0

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: case e'_5
⊢ 1 = sin (π / 2)

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: case e'_5
⊢ 0 = cos (π / 2)

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: case inr.coe
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ : ℝ
hδ : 0 < δ
s : Set E
x : E
hs : ENNReal.ofReal δ ≤ infEDist x s
z : E
hz : z ∈ s
r : NNReal
h : dist x z < δ + (↑r - δ)
hr : 0 < ↑r - δ
y : E
hxy : dist x y < ↑r - δ
hyz : dist y z < δ
⊢ infEDist x (thickening δ s) + ENNReal.ofReal δ < ↑r

Tactic:
refine (ENNReal.add_lt_add_right ofReal_ne_top <|
      infEDist_lt_iff.2 ⟨_, mem_thickening_iff.2 ⟨_, hz, hyz⟩, edist_lt_ofReal.2 hxy⟩).trans_le ?_

Goal state after:
case inr.coe
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ : ℝ
hδ : 0 < δ
s : Set E
x : E
hs : ENNReal.ofReal δ ≤ infEDist x s
z : E
hz : z ∈ s
r : NNReal
h : dist x z < δ + (↑r - δ)
hr : 0 < ↑r - δ
y : E
hxy : dist x y < ↑r - δ
hyz : dist y z < δ
⊢ ENNReal.ofReal (↑r - δ) + ENNReal.ofReal δ ≤ ↑r
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: case e'_5
⊢ -1 = sin (-(π / 2))

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: case e'_5
⊢ 0 = cos (-(π / 2))

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ -1 < 0

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ cos (↑π / 2) = cos ↑(π / 2)

Tactic:
simp

Goal state after: