mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: case refine_2
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
f g h✝ : α → 𝕜
c : ℝ
hf : ∀ᶠ (x : α) in l, f x ≠ 0
h : ∀ᶠ (x : α) in l, ‖g x‖ ≤ c * ‖h✝ x / f x‖
⊢ ∀ᶠ (x : α) in l, ‖f x * g x‖ ≤ c * ‖h✝ x‖

Tactic:
· refine h.congr <| Eventually.mp hf <| Eventually.of_forall fun x hx ↦ ?_
    rw [norm_mul, norm_div, ← mul_div_assoc, le_div_iff₀' (norm_pos_iff.mpr hx)]

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

Goal state before:
pp: x : ℝ
hx : cos x ≠ 0
this : Complex.cos ↑x ≠ 0
⊢ ↑(1 + tan x ^ 2)⁻¹ = ↑(cos x ^ 2)

Tactic:
simpa using

Goal state after:
x : ℝ
hx : cos x ≠ 0
this : Complex.cos ↑x ≠ 0
⊢ (1 + Complex.tan ↑x ^ 2)⁻¹ = Complex.cos ↑x ^ 2
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℝ
h1 : 0 ≤ x
h2 : x ≤ 1
n : ℕ
hn : 0 < n
h3 : |x| = x
h4 : |x| ≤ 1
h' : |rexp x - ∑ m ∈ range n, x ^ m / ↑m.factorial| ≤ x ^ n * (↑n.succ / (↑n.factorial * ↑n))
h'' : rexp x - ∑ m ∈ range n, x ^ m / ↑m.factorial ≤ x ^ n * (↑n.succ / (↑n.factorial * ↑n))
t : rexp x ≤ ∑ m ∈ range n, x ^ m / ↑m.factorial + x ^ n * (↑n.succ / (↑n.factorial * ↑n))
⊢ rexp x ≤ ∑ m ∈ range n, x ^ m / ↑m.factorial + x ^ n * (↑n + 1) / (↑n.factorial * ↑n)

Tactic:
simpa using

Goal state after:
x : ℝ
h1 : 0 ≤ x
h2 : x ≤ 1
n : ℕ
hn : 0 < n
h3 : |x| = x
h4 : |x| ≤ 1
h' : |rexp x - ∑ m ∈ range n, x ^ m / ↑m.factorial| ≤ x ^ n * (↑n.succ / (↑n.factorial * ↑n))
h'' : rexp x - ∑ m ∈ range n, x ^ m / ↑m.factorial ≤ x ^ n * (↑n.succ / (↑n.factorial * ↑n))
t : rexp x ≤ ∑ m ∈ range n, x ^ m / ↑m.factorial + x ^ n * (↑n.succ / (↑n.factorial * ↑n))
⊢ rexp x ≤ ∑ m ∈ range n, x ^ m / ↑m.factorial + x ^ n * ((↑n + 1) / (↑n.factorial * ↑n))
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
hx : |x| ≤ 1
⊢ |cos x - (1 - x ^ 2 / 2)| ≤ |x| ^ 4 * (5 / 96)

Tactic:
simpa using

Goal state after:
x : ℝ
hx : |x| ≤ 1
⊢ ‖↑(cos x) - (1 - ↑x ^ 2 / 2)‖ ≤ ‖↑x‖ ^ 4 * (5 / 96)
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
hx : |x| ≤ 1
⊢ |sin x - (x - x ^ 3 / 6)| ≤ |x| ^ 5 / 100

Tactic:
simpa using

Goal state after:
x : ℝ
hx : |x| ≤ 1
⊢ ‖↑(sin x) - (↑x - ↑x ^ 3 / 6)‖ ≤ ‖↑x‖ ^ 5 / 100
Module: Mathlib.Algebra.Order.Field.Power

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
k : ℤ
h : k + k ≠ 0
⊢ k ≠ 0

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
k : ℤ
h : k + k ≠ 0
⊢ ¬k = 0
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: n : ℕ
x a b : ℝ
m : ℕ
e₁ : n + 1 = m
h : |x| ≤ 1
e : |1 - a| ≤ b - |x| / ↑m * ((↑m + 1) / ↑m)
⊢ |1 + x / ↑m * 0 - a| ≤ b - |x| / ↑m * ((↑m + 1) / ↑m)

Tactic:
simpa using

Goal state after:
n : ℕ
x a b : ℝ
m : ℕ
e₁ : n + 1 = m
h : |x| ≤ 1
e : |1 - a| ≤ b - |x| / ↑m * ((↑m + 1) / ↑m)
⊢ |1 - a| ≤ b - |x| / ↑m * ((↑m + 1) / ↑m)
Module: Mathlib.Algebra.Order.Field.Power

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
n : ℤ
⊢ a ^ n = -1 ↔ a = -1 ∧ Odd n

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
n : ℤ
⊢ a ^ n = -1 ↔ a = -1 ∧ Odd n
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x a b : ℝ
h : |rexp x - expNear 0 x a| ≤ |x| ^ 0 / ↑(Nat.factorial 0) * b
⊢ |rexp x - a| ≤ b

Tactic:
simpa using

Goal state after:
x a b : ℝ
h : |rexp x - expNear 0 x a| ≤ |x| ^ 0 / ↑(Nat.factorial 0) * b
⊢ |rexp x - a| ≤ b
Module: Mathlib.Analysis.Normed.Ring.InfiniteSum

Goal state before:
pp: ι : Type u_2
ι' : Type u_3
f : ι → ℝ
g : ι' → ℝ
hf : Summable f
hg : Summable g
hf' : 0 ≤ f
hg' : 0 ≤ g
⊢ Summable fun x ↦ ∑' (y : ι'), f (x, y).1 * g (x, y).2

Tactic:
simpa using

Goal state after:
ι : Type u_2
ι' : Type u_3
f : ι → ℝ
g : ι' → ℝ
hf : Summable f
hg : Summable g
hf' : 0 ≤ f
hg' : 0 ≤ g
⊢ Summable fun x ↦ f x * ∑' (i : ι'), g i
Module: Mathlib.Order.Filter.AtTopBot.ModEq

Goal state before:
pp: d n : ℕ
h : d < n
⊢ ∃ᶠ (m : ℕ) in atTop, m % n = d

Tactic:
simpa using

Goal state after:
d n : ℕ
h : d < n
⊢ ∃ᶠ (m : ℕ) in atTop, m % n = d
Module: Mathlib.Order.Filter.AtTopBot.ModEq

Goal state before:
pp: ⊢ ∃ᶠ (m : ℕ) in atTop, Even m

Tactic:
simpa using

Goal state after:
⊢ ∃ᶠ (m : ℕ) in atTop, m % 2 = 0
Module: Mathlib.Order.Filter.AtTopBot.ModEq

Goal state before:
pp: ⊢ ∃ᶠ (m : ℕ) in atTop, Odd m

Tactic:
simpa using

Goal state after:
⊢ ∃ᶠ (m : ℕ) in atTop, m % 2 = 1
Module: Mathlib.Algebra.Order.CauSeq.BigOperators

Goal state before:
pp: case h₁
α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : ℕ → β
ha : IsCauSeq abs fun m ↦ ∑ n ∈ range m, abv (f n)
hb : IsCauSeq abv fun m ↦ ∑ n ∈ range m, g n
ε : α
ε0 : 0 < ε
P : α
hP : ∀ (i : ℕ), |∑ n ∈ range i, abv (f n)| < P
Q : α
hQ : ∀ (i : ℕ), abv (∑ n ∈ range i, g n) < Q
hP0 : 0 < P
hPε0 : 0 < ε / (2 * P)
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, abv (∑ n ∈ range j, g n - ∑ n ∈ range k, g n) < ε / (2 * P)
hQε0 : 0 < ε / (4 * Q)
M : ℕ
hM : ∀ j ≥ M, ∀ k ≥ M, |∑ n ∈ range j, abv (f n) - ∑ n ∈ range k, abv (f n)| < ε / (4 * Q)
K : ℕ
hK : K ≥ 2 * (max N M + 1)
h₁ : ∑ m ∈ range K, ∑ k ∈ range (m + 1), f k * g (m - k) = ∑ m ∈ range K, ∑ n ∈ range (K - m), f m * g n
h₂ : (fun i ↦ ∑ k ∈ range (K - i), f i * g k) = fun i ↦ f i * ∑ k ∈ range (K - i), g k
h₃ :
  ∑ i ∈ range K, f i * ∑ k ∈ range (K - i), g k =
    ∑ i ∈ range K, f i * (∑ k ∈ range (K - i), g k - ∑ k ∈ range K, g k) + ∑ i ∈ range K, f i * ∑ k ∈ range K, g k
two_mul_two : 4 = 2 * 2
hQ0 : Q ≠ 0
h2Q0 : 2 * Q ≠ 0
hε : ε / (2 * P) * P + ε / (4 * Q) * (2 * Q) = ε
hNMK : max N M + 1 < K
hKN : N < K
hsumlesum :
  ∑ i ∈ range (max N M + 1), abv (f i) * abv (∑ k ∈ range (K - i), g k - ∑ k ∈ range K, g k) ≤
    ∑ i ∈ range (max N M + 1), abv (f i) * (ε / (2 * P))
hsumltP : ∑ n ∈ range (max N M + 1), abv (f n) < P
i : ℕ
a✝ : i ∈ {i ∈ range K | max N M + 1 ≤ i}
⊢ abv (∑ k ∈ range (K - i), g k) ≤ Q

Tactic:
exact le_of_lt (hQ _)

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

Goal state before:
pp: case inr.inr
x : ℝ
hx✝ : x ≠ 0
hx : x < 0
h' : -x < 1
hx' : 0 < x + 1
⊢ x + 1 < rexp x

Tactic:
simpa using

Goal state after:
case inr.inr
x : ℝ
hx✝ : x ≠ 0
hx : x < 0
h' : -x < 1
hx' : 0 < x + 1
⊢ x + 1 < rexp x
Module: Mathlib.Algebra.Order.CauSeq.BigOperators

Goal state before:
pp: case h₂
α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : ℕ → β
ha : IsCauSeq abs fun m ↦ ∑ n ∈ range m, abv (f n)
hb : IsCauSeq abv fun m ↦ ∑ n ∈ range m, g n
ε : α
ε0 : 0 < ε
P : α
hP : ∀ (i : ℕ), |∑ n ∈ range i, abv (f n)| < P
Q : α
hQ : ∀ (i : ℕ), abv (∑ n ∈ range i, g n) < Q
hP0 : 0 < P
hPε0 : 0 < ε / (2 * P)
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, abv (∑ n ∈ range j, g n - ∑ n ∈ range k, g n) < ε / (2 * P)
hQε0 : 0 < ε / (4 * Q)
M : ℕ
hM : ∀ j ≥ M, ∀ k ≥ M, |∑ n ∈ range j, abv (f n) - ∑ n ∈ range k, abv (f n)| < ε / (4 * Q)
K : ℕ
hK : K ≥ 2 * (max N M + 1)
h₁ : ∑ m ∈ range K, ∑ k ∈ range (m + 1), f k * g (m - k) = ∑ m ∈ range K, ∑ n ∈ range (K - m), f m * g n
h₂ : (fun i ↦ ∑ k ∈ range (K - i), f i * g k) = fun i ↦ f i * ∑ k ∈ range (K - i), g k
h₃ :
  ∑ i ∈ range K, f i * ∑ k ∈ range (K - i), g k =
    ∑ i ∈ range K, f i * (∑ k ∈ range (K - i), g k - ∑ k ∈ range K, g k) + ∑ i ∈ range K, f i * ∑ k ∈ range K, g k
two_mul_two : 4 = 2 * 2
hQ0 : Q ≠ 0
h2Q0 : 2 * Q ≠ 0
hε : ε / (2 * P) * P + ε / (4 * Q) * (2 * Q) = ε
hNMK : max N M + 1 < K
hKN : N < K
hsumlesum :
  ∑ i ∈ range (max N M + 1), abv (f i) * abv (∑ k ∈ range (K - i), g k - ∑ k ∈ range K, g k) ≤
    ∑ i ∈ range (max N M + 1), abv (f i) * (ε / (2 * P))
hsumltP : ∑ n ∈ range (max N M + 1), abv (f n) < P
i : ℕ
a✝ : i ∈ {i ∈ range K | max N M + 1 ≤ i}
⊢ abv (∑ k ∈ range K, g k) ≤ Q

Tactic:
exact le_of_lt (hQ _)

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

Goal state before:
pp: n : ℕ
t : ℝ
ht' : t ≤ ↑n
hn : n ≠ 0
⊢ rexp (-(t / ↑n)) ^ n = rexp (-t)

Tactic:
← Real.exp_nat_mul,

Goal state after:
n : ℕ
t : ℝ
ht' : t ≤ ↑n
hn : n ≠ 0
⊢ rexp (↑n * -(t / ↑n)) = rexp (-t)
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)
⊢ (fun n ↦ f n * g n) =O[cofinite] fun n ↦ ‖f n‖

Tactic:
simpa using

Goal state after:
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)
⊢ (fun n ↦ f n * g n) =O[cofinite] f
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
this : f m > a - l • ε
⊢ a < f m

Tactic:
simpa using

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
this : f m > a - l • ε
⊢ a < f m
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: α : Type u_1
inst✝² : NormedRing α
inst✝¹ : NormSMulClass ℤ α
inst✝ : Nontrivial α
⊢ Tendsto (fun x ↦ ‖↑x‖) atTop atTop

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝² : NormedRing α
inst✝¹ : NormSMulClass ℤ α
inst✝ : Nontrivial α
⊢ Tendsto (fun x ↦ ↑x * ‖1‖) atTop atTop
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: α : Type u_1
inst✝² : NormedRing α
inst✝¹ : NormSMulClass ℤ α
inst✝ : Nontrivial α
⊢ Tendsto (fun x ↦ ‖↑x‖) (atBot ⊔ atTop) atTop

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝² : NormedRing α
inst✝¹ : NormSMulClass ℤ α
inst✝ : Nontrivial α
⊢ Tendsto (fun x ↦ |↑x| * ‖1‖) atBot atTop ∧ Tendsto (fun x ↦ |↑x| * ‖1‖) atTop atTop
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: x y : ℂ
⊢ dist y x < 1 → dist (cexp y) (cexp x) ≤ 2 * ‖cexp x‖ * dist y x

Tactic:
simpa using

Goal state after:
x y : ℂ
⊢ ‖y - x‖ < 1 → ‖cexp y - cexp x‖ ≤ 2 * ‖cexp x‖ * ‖y - x‖
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: case inl
⊢ (fun x ↦ cexp x - ∑ i ∈ Finset.range 0, x ^ i / ↑i !) =O[𝓝 0] fun x ↦ x ^ 0

Tactic:
simpa using

Goal state after:
case inl
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝 0) fun x ↦ ‖cexp x‖
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 ≤ f n.succ
⊢ ∀ n ≥ m, |(-f) n| ≤ a

Tactic:
simpa using

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 ≤ f n.succ
⊢ ∀ (n : ℕ), m ≤ n → |f n| ≤ a
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) (cexp 0) < ε / (2 * Real.exp a)
x : ℂ
a✝ : x ∈ {x | x.re ≤ a}
y : ℂ
hy : y ∈ {x | x.re ≤ a}
hxy : dist x y < δ
⊢ dist (x - y) 0 < δ

Tactic:
simpa using

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) (cexp 0) < ε / (2 * Real.exp a)
x : ℂ
a✝ : x ∈ {x | x.re ≤ a}
y : ℂ
hy : y ∈ {x | x.re ≤ a}
hxy : dist x y < δ
⊢ ‖x - y‖ < δ
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 ≤ f n.succ
⊢ ∀ n ≥ m, (-f) n.succ ≤ (-f) n

Tactic:
simpa using

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 ≤ f n.succ
⊢ ∀ (n : ℕ), m ≤ n → f n ≤ f (n + 1)
Module: Mathlib.Algebra.Order.CauSeq.BigOperators

Goal state before:
pp: α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : Archimedean α
a x : α
hx1 : |x| < 1
⊢ IsCauSeq abs fun m ↦ ∑ n ∈ range m, a * x ^ n

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : Archimedean α
a x : α
hx1 : |x| < 1
⊢ IsCauSeq abs fun m ↦ ∑ n ∈ range m, a * x ^ n
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: f : ℕ → ℝ
R : ℝ
A : Set.Ico 0 R ⊆ Set.Ioo (-R) R
B : Set.Ioo 0 R ⊆ Set.Ioo (-R) R
tfae_1_to_3 : (∃ a ∈ Set.Ioo (-R) R, f =o[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo (-R) R, f =O[atTop] fun x ↦ a ^ x
tfae_2_to_1 : (∃ a ∈ Set.Ioo 0 R, f =o[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo (-R) R, f =o[atTop] fun x ↦ a ^ x
tfae_3_to_2 : (∃ a ∈ Set.Ioo (-R) R, f =O[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo 0 R, f =o[atTop] fun x ↦ a ^ x
tfae_2_to_4 : (∃ a ∈ Set.Ioo 0 R, f =o[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo 0 R, f =O[atTop] fun x ↦ a ^ x
tfae_4_to_3 : (∃ a ∈ Set.Ioo 0 R, f =O[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo (-R) R, f =O[atTop] fun x ↦ a ^ x
a : ℝ
ha : a ∈ Set.Ioo 0 R
H : f =O[atTop] fun x ↦ a ^ x
C : ℝ
hC₀ : C > 0
hC : ∀ ⦃x : ℕ⦄, a ^ x ≠ 0 → ‖f x‖ ≤ C * ‖a ^ x‖
n : ℕ
⊢ |f n| ≤ C * a ^ n

Tactic:
simpa using

Goal state after:
f : ℕ → ℝ
R : ℝ
A : Set.Ico 0 R ⊆ Set.Ioo (-R) R
B : Set.Ioo 0 R ⊆ Set.Ioo (-R) R
tfae_1_to_3 : (∃ a ∈ Set.Ioo (-R) R, f =o[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo (-R) R, f =O[atTop] fun x ↦ a ^ x
tfae_2_to_1 : (∃ a ∈ Set.Ioo 0 R, f =o[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo (-R) R, f =o[atTop] fun x ↦ a ^ x
tfae_3_to_2 : (∃ a ∈ Set.Ioo (-R) R, f =O[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo 0 R, f =o[atTop] fun x ↦ a ^ x
tfae_2_to_4 : (∃ a ∈ Set.Ioo 0 R, f =o[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo 0 R, f =O[atTop] fun x ↦ a ^ x
tfae_4_to_3 : (∃ a ∈ Set.Ioo 0 R, f =O[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo (-R) R, f =O[atTop] fun x ↦ a ^ x
a : ℝ
ha : a ∈ Set.Ioo 0 R
H : f =O[atTop] fun x ↦ a ^ x
C : ℝ
hC₀ : C > 0
hC : ∀ ⦃x : ℕ⦄, a ^ x ≠ 0 → ‖f x‖ ≤ C * ‖a ^ x‖
n : ℕ
⊢ |f n| ≤ C * a ^ n
Module: Mathlib.Algebra.Order.CauSeq.BigOperators

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

Tactic:
simpa using

Goal state after:
case inl
α : Type u_1
β : Type u_2
inst✝⁵ : Field α
inst✝⁴ : LinearOrder α
inst✝³ : IsStrictOrderedRing α
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : Archimedean α
f : ℕ → β
n m : ℕ
hmn : n.succ ≤ m
hr0 : 0 ≤ 0
hr1 : 0 < 1
h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ 0 * abv (f m)
har1 : |0| < 1
m_pos : 0 < m
this : abv (f m.pred.succ) ≤ 0 * abv (f m.pred)
⊢ abv (f m) ≤ 0
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: y : ℝ
⊢ y ≤ rexp (y - 1)

Tactic:
simpa using

Goal state after:
y : ℝ
⊢ y ≤ rexp (y - 1)
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: y : ℝ
h_le : y ≤ rexp (y - 1)
h_mul_le : y * rexp (-y) ≤ rexp (y - 1) * rexp (-y)
⊢ y * rexp (-y) ≤ rexp (-1)

Tactic:
simpa using

Goal state after:
y : ℝ
h_le : y ≤ rexp (y - 1)
h_mul_le : y * rexp (-y) ≤ rexp (y - 1) * rexp (-y)
⊢ y * rexp (-y) ≤ rexp (-1)
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: f : ℕ → ℝ
R : ℝ
A : Set.Ico 0 R ⊆ Set.Ioo (-R) R
B : Set.Ioo 0 R ⊆ Set.Ioo (-R) R
tfae_1_to_3 : (∃ a ∈ Set.Ioo (-R) R, f =o[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo (-R) R, f =O[atTop] fun x ↦ a ^ x
tfae_2_to_1 : (∃ a ∈ Set.Ioo 0 R, f =o[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo (-R) R, f =o[atTop] fun x ↦ a ^ x
tfae_3_to_2 : (∃ a ∈ Set.Ioo (-R) R, f =O[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo 0 R, f =o[atTop] fun x ↦ a ^ x
tfae_2_to_4 : (∃ a ∈ Set.Ioo 0 R, f =o[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo 0 R, f =O[atTop] fun x ↦ a ^ x
tfae_4_to_3 : (∃ a ∈ Set.Ioo 0 R, f =O[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo (-R) R, f =O[atTop] fun x ↦ a ^ x
tfae_4_to_6 : (∃ a ∈ Set.Ioo 0 R, f =O[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo 0 R, ∃ C > 0, ∀ (n : ℕ), |f n| ≤ C * a ^ n
tfae_6_to_5 :
  (∃ a ∈ Set.Ioo 0 R, ∃ C > 0, ∀ (n : ℕ), |f n| ≤ C * a ^ n) →
    ∃ a < R, ∃ C, (0 < C ∨ 0 < R) ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n
a : ℝ
ha : a < R
h₀ : 0 < 0 ∨ 0 < R
H : ∀ (n : ℕ), |f n| ≤ 0 * a ^ n
n : ℕ
⊢ f n = 0 n

Tactic:
simpa using

Goal state after:
f : ℕ → ℝ
R : ℝ
A : Set.Ico 0 R ⊆ Set.Ioo (-R) R
B : Set.Ioo 0 R ⊆ Set.Ioo (-R) R
tfae_1_to_3 : (∃ a ∈ Set.Ioo (-R) R, f =o[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo (-R) R, f =O[atTop] fun x ↦ a ^ x
tfae_2_to_1 : (∃ a ∈ Set.Ioo 0 R, f =o[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo (-R) R, f =o[atTop] fun x ↦ a ^ x
tfae_3_to_2 : (∃ a ∈ Set.Ioo (-R) R, f =O[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo 0 R, f =o[atTop] fun x ↦ a ^ x
tfae_2_to_4 : (∃ a ∈ Set.Ioo 0 R, f =o[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo 0 R, f =O[atTop] fun x ↦ a ^ x
tfae_4_to_3 : (∃ a ∈ Set.Ioo 0 R, f =O[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo (-R) R, f =O[atTop] fun x ↦ a ^ x
tfae_4_to_6 : (∃ a ∈ Set.Ioo 0 R, f =O[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo 0 R, ∃ C > 0, ∀ (n : ℕ), |f n| ≤ C * a ^ n
tfae_6_to_5 :
  (∃ a ∈ Set.Ioo 0 R, ∃ C > 0, ∀ (n : ℕ), |f n| ≤ C * a ^ n) →
    ∃ a < R, ∃ C, (0 < C ∨ 0 < R) ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n
a : ℝ
ha : a < R
h₀ : 0 < 0 ∨ 0 < R
H : ∀ (n : ℕ), |f n| ≤ 0 * a ^ n
n : ℕ
⊢ f n = 0
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: case inl
b c : ℝ
hb : 0 < b
⊢ Tendsto (fun x ↦ (b * rexp x + c) / x ^ 0) atTop atTop

Tactic:
simp only [pow_zero, div_one]

Goal state after:
case inl
b c : ℝ
hb : 0 < b
⊢ Tendsto (fun x ↦ b * rexp x + c) atTop atTop
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: x : ℝ
n : ℤ
⊢ sin (↑n * π - x) = -((-1) ^ n * sin x)

Tactic:
simpa using

Goal state after:
x : ℝ
n : ℤ
⊢ sin (↑n * π - x) = -((-1) ^ n * sin x)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: x : ℝ
n : ℕ
⊢ sin (↑n * π - x) = -((-1) ^ n * sin x)

Tactic:
simpa using

Goal state after:
x : ℝ
n : ℕ
⊢ sin (↑n * π - x) = -((-1) ^ n * sin x)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: n : ℤ
⊢ cos (↑n * π) = (-1) ^ n

Tactic:
simpa using

Goal state after:
n : ℤ
⊢ cos (↑n * π) = (-1) ^ n
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: n : ℕ
⊢ cos (↑n * π) = (-1) ^ n

Tactic:
simpa using

Goal state after:
n : ℕ
⊢ cos (↑n * π) = (-1) ^ n
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: n : ℕ
⊢ cos (↑n * (2 * π) + π) = -1

Tactic:
simpa using

Goal state after:
n : ℕ
⊢ cos (↑n * (2 * π) + π) = -1
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: n : ℤ
⊢ cos (↑n * (2 * π) + π) = -1

Tactic:
simpa using

Goal state after:
n : ℤ
⊢ cos (↑n * (2 * π) + π) = -1
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: n : ℕ
⊢ cos (↑n * (2 * π) - π) = -1

Tactic:
simpa using

Goal state after:
n : ℕ
⊢ cos (↑n * (2 * π) - π) = -1
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: n : ℤ
⊢ cos (↑n * (2 * π) - π) = -1

Tactic:
simpa using

Goal state after:
n : ℤ
⊢ cos (↑n * (2 * π) - π) = -1
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: n : ℕ
⊢ (fun x ↦ x ^ n) =o[atTop] rexp

Tactic:
simpa using

Goal state after:
n : ℕ
⊢ Tendsto (fun x ↦ x ^ n / rexp x) atTop (𝓝 0)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ sin (π / 2) = 1 ∨ sin (π / 2) = -1

Tactic:
simpa using

Goal state after:
⊢ sin (π / 2) = 1 ∨ sin (π / 2) = -1
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: ⊢ Summable fun n ↦ rexp (-↑n)

Tactic:
simpa using

Goal state after:
⊢ Summable fun n ↦ rexp (-↑n)
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 ε : ℝ
a : M
this✝ : Nonempty ↑{m | ↑m = ↑a}
b : M
this : Nonempty ↑{m | ↑m = ↑b}
⊢ dist 1 ↑⟨a * b, ⋯⟩ ≤ dist 1 ↑⟨a, ⋯⟩ + dist 1 ↑⟨b, ⋯⟩

Tactic:
simpa using

Goal state after:
M : Type u_1
inst✝ : SeminormedCommGroup M
S T : Subgroup M
x : M ⧸ S
m : M
r ε : ℝ
a : M
this✝ : Nonempty ↑{m | ↑m = ↑a}
b : M
this : Nonempty ↑{m | ↑m = ↑b}
⊢ ‖a * b‖ ≤ ‖a‖ + ‖b‖
Module: Mathlib.Analysis.Normed.Group.Quotient

Goal state before:
pp: M : Type u_1
inst✝ : SeminormedCommGroup M
S : Subgroup M
m : M
ε : ℝ
hε : 0 < ε
n : M
hn : ↑n = (mk' S) m
hn' : ‖n‖ < ‖(mk' S) m‖ + ε
⊢ m⁻¹ * n ∈ S

Tactic:
simpa using

Goal state after:
M : Type u_1
inst✝ : SeminormedCommGroup M
S : Subgroup M
m : M
ε : ℝ
hε : 0 < ε
n : M
hn : ↑n = (mk' S) m
hn' : ‖n‖ < ‖(mk' S) m‖ + ε
⊢ m⁻¹ * n ∈ S
Module: Mathlib.Analysis.Normed.Group.Quotient

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
m : M
⊢ ‖(↑(mk' S)).toFun m‖ ≤ 1 * ‖m‖

Tactic:
simpa using

Goal state after:
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
m : M
⊢ ‖↑m‖ ≤ ‖m‖
Module: Mathlib.Analysis.Normed.Group.Quotient

Goal state before:
pp: case inl
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ x ∈ S, f x = 0
h : ‖f‖ = 0
x : M
⊢ ‖(lift S f.toAddMonoidHom hf) ↑x‖ ≤ ‖f‖ * ‖↑x‖

Tactic:
simpa using

Goal state after:
case inl
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ x ∈ S, f x = 0
h : ‖f‖ = 0
x : M
⊢ ‖f x‖ ≤ 0
Module: Mathlib.Analysis.Normed.Group.Quotient

Goal state before:
pp: M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
h : ↑S.topologicalClosure = univ
x : M
⊢ ‖S.normedMk x‖ ≤ 0 * ‖x‖

Tactic:
have hker : x ∈ S.normedMk.ker.topologicalClosure := by
    rw [S.ker_normedMk, ← SetLike.mem_coe, h]
    trivial

Goal state after:
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
h : ↑S.topologicalClosure = univ
x : M
hker : x ∈ S.normedMk.ker.topologicalClosure
⊢ ‖S.normedMk x‖ ≤ 0 * ‖x‖
Module: Mathlib.Analysis.Normed.Group.Quotient

Goal state before:
pp: M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
m : M
⊢ ‖S.normedMk m‖ = sInf ((fun m_1 ↦ ‖m + m_1‖) '' ↑S.normedMk.ker)

Tactic:
simpa using

Goal state after:
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
m : M
⊢ ‖↑m‖ = sInf ((fun m_1 ↦ ‖m + m_1‖) '' ↑S)
Module: Mathlib.Analysis.Normed.Group.Quotient

Goal state before:
pp: M : Type u_1
inst✝¹ : SeminormedAddCommGroup M
N : Type u_3
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ s ∈ S, f s = 0
fb : f.NormNoninc
x : M ⧸ S
fb' : ‖f‖ ≤ ↑1
⊢ ‖(lift S f hf) x‖ ≤ ‖x‖

Tactic:
simpa using

Goal state after:
M : Type u_1
inst✝¹ : SeminormedAddCommGroup M
N : Type u_3
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ s ∈ S, f s = 0
fb : f.NormNoninc
x : M ⧸ S
fb' : ‖f‖ ≤ ↑1
⊢ ‖(lift S f hf) x‖ ≤ ‖x‖