mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.InfiniteSum.Module

Goal state before:
pp: ι : Type u_5
R : Type u_7
R₂ : Type u_8
M : Type u_9
M₂ : Type u_10
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring R₂
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R₂ M₂
inst✝⁵ : TopologicalSpace M
inst✝⁴ : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst✝³ : RingHomInvPair σ σ'
inst✝² : RingHomInvPair σ' σ
L : SummationFilter ι
inst✝¹ : T2Space M
inst✝ : T2Space M₂
f : ι → M
e : M ≃SL[σ] M₂
⊢ e (∑'[L] (z : ι), f z) = ∑'[L] (z : ι), e (f z)

Tactic:
by
  refine symm (e.tsum_eq_iff.mpr ?_)
  rw [e.symm_apply_apply _]

Goal state after:
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: case e_a
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
I' : A
hf : I' * I' = -1
x₁ y₁ x₂ y₂ : ℝ
⊢ (algebraMap ℝ A) (x₁ * y₂ + y₁ * x₂) * I' = ((algebraMap ℝ A) (x₁ * y₂) + (algebraMap ℝ A) (y₁ * x₂)) * I'

Tactic:
← map_add

Goal state after:
case e_a
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
I' : A
hf : I' * I' = -1
x₁ y₁ x₂ y₂ : ℝ
⊢ (algebraMap ℝ A) (x₁ * y₂ + y₁ * x₂) * I' = (algebraMap ℝ A) (x₁ * y₂ + y₁ * x₂) * I'
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
x✝ : (starRingEnd K) z = z
h : (starRingEnd K) z = z := x✝
⊢ I * (z - z) / 2 = ↑0

Tactic:
sub_self,

Goal state after:
K : Type u_1
inst✝ : RCLike K
z : K
x✝ : (starRingEnd K) z = z
h : (starRingEnd K) z = z := x✝
⊢ I * 0 / 2 = ↑0
Module: Mathlib.Analysis.Complex.Basic

Goal state before:
pp: A : Type u_1
inst✝⁴ : SeminormedAddCommGroup A
inst✝³ : StarAddMonoid A
inst✝² : NormedSpace ℂ A
inst✝¹ : StarModule ℂ A
inst✝ : NormedStarGroup A
x : A
⊢ ‖2⁻¹‖ * ‖x + star x‖ ≤ 2⁻¹ * (2 * ‖x‖)

Tactic:
norm_inv,

Goal state after:
A : Type u_1
inst✝⁴ : SeminormedAddCommGroup A
inst✝³ : StarAddMonoid A
inst✝² : NormedSpace ℂ A
inst✝¹ : StarModule ℂ A
inst✝ : NormedStarGroup A
x : A
⊢ ‖2‖⁻¹ * ‖x + star x‖ ≤ 2⁻¹ * (2 * ‖x‖)
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
E : Type u_3
E''' : Type u_12
inst✝¹ : Norm E
inst✝ : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
h : f =O[l] g
⊢ ∃ c > 0, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖

Tactic:
isBigO_iff

Goal state after:
α : Type u_1
E : Type u_3
E''' : Type u_12
inst✝¹ : Norm E
inst✝ : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
h : ∃ c, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
⊢ ∃ c > 0, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
E : Type u_3
E''' : Type u_12
inst✝¹ : Norm E
inst✝ : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
h : ∃ c > 0, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
⊢ f =O[l] g

Tactic:
isBigO_iff

Goal state after:
α : Type u_1
E : Type u_3
E''' : Type u_12
inst✝¹ : Norm E
inst✝ : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
h : ∃ c > 0, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
⊢ ∃ c, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
F : Type u_4
E' : Type u_6
inst✝¹ : Norm F
inst✝ : SeminormedAddCommGroup E'
c₁ c₂ : ℝ
g : α → F
l : Filter α
f₁ f₂ : α → E'
h₁ : ∀ᶠ (x : α) in l, ‖f₁ x‖ ≤ c₁ * ‖g x‖
h₂ : ∀ᶠ (x : α) in l, ‖f₂ x‖ ≤ c₂ * ‖g x‖
x : α
⊢ ‖f₁ x‖ ≤ c₁ * ‖g x‖ → ‖f₂ x‖ ≤ c₂ * ‖g x‖ → ‖f₁ x + f₂ x‖ ≤ (c₁ + c₂) * ‖g x‖

Tactic:
hx₁

Goal state after:
α : Type u_1
F : Type u_4
E' : Type u_6
inst✝¹ : Norm F
inst✝ : SeminormedAddCommGroup E'
c₁ c₂ : ℝ
g : α → F
l : Filter α
f₁ f₂ : α → E'
h₁ : ∀ᶠ (x : α) in l, ‖f₁ x‖ ≤ c₁ * ‖g x‖
h₂ : ∀ᶠ (x : α) in l, ‖f₂ x‖ ≤ c₂ * ‖g x‖
x : α
hx₁ : ‖f₁ x‖ ≤ c₁ * ‖g x‖
⊢ ‖f₂ x‖ ≤ c₂ * ‖g x‖ → ‖f₁ x + f₂ x‖ ≤ (c₁ + c₂) * ‖g x‖
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
c₁ c₂ : ℝ
l : Filter α
f₁ f₂ : α → E'
g₁ g₂ : α → ℝ
h₁ : ∀ᶠ (x : α) in l, ‖f₁ x‖ ≤ c₁ * ‖g₁ x‖
h₂ : ∀ᶠ (x : α) in l, ‖f₂ x‖ ≤ c₂ * ‖g₂ x‖
x : α
⊢ ‖f₁ x‖ ≤ c₁ * ‖g₁ x‖ → ‖f₂ x‖ ≤ c₂ * ‖g₂ x‖ → ‖f₁ x + f₂ x‖ ≤ max c₁ c₂ * ‖‖g₁ x‖ + ‖g₂ x‖‖

Tactic:
hx₁

Goal state after:
α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
c₁ c₂ : ℝ
l : Filter α
f₁ f₂ : α → E'
g₁ g₂ : α → ℝ
h₁ : ∀ᶠ (x : α) in l, ‖f₁ x‖ ≤ c₁ * ‖g₁ x‖
h₂ : ∀ᶠ (x : α) in l, ‖f₂ x‖ ≤ c₂ * ‖g₂ x‖
x : α
hx₁ : ‖f₁ x‖ ≤ c₁ * ‖g₁ x‖
⊢ ‖f₂ x‖ ≤ c₂ * ‖g₂ x‖ → ‖f₁ x + f₂ x‖ ≤ max c₁ c₂ * ‖‖g₁ x‖ + ‖g₂ x‖‖
Module: Mathlib.Tactic.NormNum.BigOperators

Goal state before:
pp: n : ℕ
pn : NormNum.IsNat n 0
⊢ Finset.range 0 = ∅

Tactic:
Finset.range_zero

Goal state after:
n : ℕ
pn : NormNum.IsNat n 0
⊢ ∅ = ∅
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
R : Type u_13
inst✝² : SeminormedRing R
S : Type u_17
inst✝¹ : NormedRing S
inst✝ : NormMulClass S
l : Filter α
f₁ f₂ : α → R
g₁ g₂ : α → S
c₁ c₂ : ℝ
h₁ : ∀ᶠ (x : α) in l, ‖f₁ x‖ ≤ c₁ * ‖g₁ x‖
h₂ : ∀ᶠ (x : α) in l, ‖f₂ x‖ ≤ c₂ * ‖g₂ x‖
a✝ : α
⊢ ‖f₁ a✝‖ ≤ c₁ * ‖g₁ a✝‖ → ‖f₂ a✝‖ ≤ c₂ * ‖g₂ a✝‖ → ‖f₁ a✝ * f₂ a✝‖ ≤ c₁ * c₂ * ‖g₁ a✝ * g₂ a✝‖

Tactic:
hx₁

Goal state after:
α : Type u_1
R : Type u_13
inst✝² : SeminormedRing R
S : Type u_17
inst✝¹ : NormedRing S
inst✝ : NormMulClass S
l : Filter α
f₁ f₂ : α → R
g₁ g₂ : α → S
c₁ c₂ : ℝ
h₁ : ∀ᶠ (x : α) in l, ‖f₁ x‖ ≤ c₁ * ‖g₁ x‖
h₂ : ∀ᶠ (x : α) in l, ‖f₂ x‖ ≤ c₂ * ‖g₂ x‖
a✝ : α
hx₁ : ‖f₁ a✝‖ ≤ c₁ * ‖g₁ a✝‖
⊢ ‖f₂ a✝‖ ≤ c₂ * ‖g₂ a✝‖ → ‖f₁ a✝ * f₂ a✝‖ ≤ c₁ * c₂ * ‖g₁ a✝ * g₂ a✝‖
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
E' : Type u_6
F' : Type u_7
R : Type u_13
𝕜' : Type u_16
inst✝⁷ : SeminormedAddCommGroup E'
inst✝⁶ : SeminormedAddCommGroup F'
inst✝⁵ : SeminormedRing R
inst✝⁴ : NormedDivisionRing 𝕜'
c c' : ℝ
f' : α → E'
g' : α → F'
l : Filter α
inst✝³ : Module R E'
inst✝² : IsBoundedSMul R E'
inst✝¹ : Module 𝕜' F'
inst✝ : NormSMulClass 𝕜' F'
k₁ : α → R
k₂ : α → 𝕜'
h₁ : ∀ᶠ (x : α) in l, ‖k₁ x‖ ≤ c * ‖k₂ x‖
h₂ : ∀ᶠ (x : α) in l, ‖f' x‖ ≤ c' * ‖g' x‖
a✝ : α
⊢ ‖k₁ a✝‖ ≤ c * ‖k₂ a✝‖ → ‖f' a✝‖ ≤ c' * ‖g' a✝‖ → ‖k₁ a✝ • f' a✝‖ ≤ c * c' * ‖k₂ a✝ • g' a✝‖

Tactic:
hx₁

Goal state after:
α : Type u_1
E' : Type u_6
F' : Type u_7
R : Type u_13
𝕜' : Type u_16
inst✝⁷ : SeminormedAddCommGroup E'
inst✝⁶ : SeminormedAddCommGroup F'
inst✝⁵ : SeminormedRing R
inst✝⁴ : NormedDivisionRing 𝕜'
c c' : ℝ
f' : α → E'
g' : α → F'
l : Filter α
inst✝³ : Module R E'
inst✝² : IsBoundedSMul R E'
inst✝¹ : Module 𝕜' F'
inst✝ : NormSMulClass 𝕜' F'
k₁ : α → R
k₂ : α → 𝕜'
h₁ : ∀ᶠ (x : α) in l, ‖k₁ x‖ ≤ c * ‖k₂ x‖
h₂ : ∀ᶠ (x : α) in l, ‖f' x‖ ≤ c' * ‖g' x‖
a✝ : α
hx₁ : ‖k₁ a✝‖ ≤ c * ‖k₂ a✝‖
⊢ ‖f' a✝‖ ≤ c' * ‖g' a✝‖ → ‖k₁ a✝ • f' a✝‖ ≤ c * c' * ‖k₂ a✝ • g' a✝‖
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: case hgf
α : Type u_1
𝕜 : Type u_17
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
h✝ : Tendsto (fun x ↦ g x / f x) l atTop
x : α
h : 1 ≤ g x / f x
⊢ g x = 0 → f x = 0

Tactic:
h0

Goal state after:
case hgf
α : Type u_1
𝕜 : Type u_17
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
h✝ : Tendsto (fun x ↦ g x / f x) l atTop
x : α
h : 1 ≤ g x / f x
h0 : g x = 0
⊢ f x = 0
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: E'' : Type u_9
F'' : Type u_10
inst✝¹ : NormedAddCommGroup E''
inst✝ : NormedAddCommGroup F''
f : E'' → F''
s : Set E''
x₀ : E''
n : ℕ
h : f =O[𝓝[s] x₀] fun x ↦ ‖x - x₀‖ ^ n
hx₀ : x₀ ∈ s
hn : n ≠ 0
⊢ ‖x₀ - x₀‖ ^ n = 0

Tactic:
sub_self,

Goal state after:
E'' : Type u_9
F'' : Type u_10
inst✝¹ : NormedAddCommGroup E''
inst✝ : NormedAddCommGroup F''
f : E'' → F''
s : Set E''
x₀ : E''
n : ℕ
h : f =O[𝓝[s] x₀] fun x ↦ ‖x - x₀‖ ^ n
hx₀ : x₀ ∈ s
hn : n ≠ 0
⊢ ‖0‖ ^ n = 0
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
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
⊢ abv
      (∑ i ∈ range K, f i * ∑ k ∈ range K, g k - ∑ i ∈ range K, f i * ∑ k ∈ range K, g k -
        ∑ i ∈ range K, f i * (∑ k ∈ range (K - i), g k - ∑ k ∈ range K, g k)) <
    ε

Tactic:
sub_self,

Goal state after:
α : 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
⊢ abv (0 - ∑ i ∈ range K, f i * (∑ k ∈ range (K - i), g k - ∑ k ∈ range K, g k)) < ε
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: case hbc
x : ℂ
n : ℕ
hx : ‖x‖ / ↑n.succ ≤ 1 / 2
j : ℕ
hj✝ : j ≥ n
k : ℕ := j - n
hj : j = n + k
⊢ 2 * (‖x‖ / ↑n.succ - 1) ≤ (‖x‖ / ↑n.succ) ^ k - 1

pp: case hbc
x : ℂ
n : ℕ
hx : ‖x‖ / ↑n.succ ≤ 1 / 2
j : ℕ
hj✝ : j ≥ n
k : ℕ := j - n
hj : j = n + k
⊢ ‖x‖ / ↑n.succ - 1 < 0

pp: case hbc.h
x : ℂ
n : ℕ
hx : ‖x‖ / ↑n.succ ≤ 1 / 2
j : ℕ
hj✝ : j ≥ n
k : ℕ := j - n
hj : j = n + k
⊢ ‖x‖ / ↑n.succ ≠ 1

Tactic:
· trans (-1 : ℝ)
      · linarith
      · simp only [neg_le_sub_iff_le_add, div_pow, Nat.cast_succ, le_add_iff_nonneg_left]
        positivity

Goal state after:
case hbc
x : ℂ
n : ℕ
hx : ‖x‖ / ↑n.succ ≤ 1 / 2
j : ℕ
hj✝ : j ≥ n
k : ℕ := j - n
hj : j = n + k
⊢ ‖x‖ / ↑n.succ - 1 < 0

case hbc.h
x : ℂ
n : ℕ
hx : ‖x‖ / ↑n.succ ≤ 1 / 2
j : ℕ
hj✝ : j ≥ n
k : ℕ := j - n
hj : j = n + k
⊢ ‖x‖ / ↑n.succ ≠ 1
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ sin x * sin x ≤ 1

Tactic:
simp only [← sq, sin_sq_le_one]

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

Goal state before:
pp: E'' : Type u_9
F'' : Type u_10
inst✝¹ : NormedAddCommGroup E''
inst✝ : NormedAddCommGroup F''
f : ℕ → E''
g : ℕ → F''
h✝ : ∀ᶠ (x : ℕ) in atTop, ∀ (y : ℕ), x ≤ y → g y = 0 → f y = 0
hrec✝ :
  ∀ᶠ (n₀ : ℕ) in atTop,
    ∃ C₀, ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, ‖f m‖ ≤ C * ‖g m‖) → ‖f n‖ ≤ C * ‖g n‖
n₀ : ℕ
h : ∀ (y : ℕ), n₀ ≤ y → g y = 0 → f y = 0
C₀ : ℝ
hrec : ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, ‖f m‖ ≤ C * ‖g m‖) → ‖f n‖ ≤ C * ‖g n‖
⊢ f =O[atTop] g

Tactic:
isBigO_iff

Goal state after:
E'' : Type u_9
F'' : Type u_10
inst✝¹ : NormedAddCommGroup E''
inst✝ : NormedAddCommGroup F''
f : ℕ → E''
g : ℕ → F''
h✝ : ∀ᶠ (x : ℕ) in atTop, ∀ (y : ℕ), x ≤ y → g y = 0 → f y = 0
hrec✝ :
  ∀ᶠ (n₀ : ℕ) in atTop,
    ∃ C₀, ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, ‖f m‖ ≤ C * ‖g m‖) → ‖f n‖ ≤ C * ‖g n‖
n₀ : ℕ
h : ∀ (y : ℕ), n₀ ≤ y → g y = 0 → f y = 0
C₀ : ℝ
hrec : ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, ‖f m‖ ≤ C * ‖g m‖) → ‖f n‖ ≤ C * ‖g n‖
⊢ ∃ c, ∀ᶠ (x : ℕ) in atTop, ‖f x‖ ≤ c * ‖g x‖
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ tanh x < 1

Tactic:
rw [tanh_eq]

Goal state after:
x : ℝ
⊢ (rexp x - rexp (-x)) / (rexp x + rexp (-x)) < 1
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ -1 < tanh x

Tactic:
rw [tanh_eq]

Goal state after:
x : ℝ
⊢ -1 < (rexp x - rexp (-x)) / (rexp x + rexp (-x))
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: f g : ℕ → ℝ
hf : ∀ᶠ (n : ℕ) in atTop, 0 ≤ f n
hg : ∀ᶠ (n : ℕ) in atTop, 0 < g n
hrec : ∀ᶠ (n₀ : ℕ) in atTop, ∃ C₀, ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, f m ≤ C * g m) → f n ≤ C * g n
n₀ : ℕ
hn₀ : ∀ (y : ℕ), n₀ ≤ y → 0 < g y
hn₀' : ∀ (y : ℕ), n₀ ≤ y → 0 ≤ f y
C₀ : ℝ
hnrec : ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, f m ≤ C * g m) → f n ≤ C * g n
⊢ ∃ C₀, ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, ‖f m‖ ≤ C * ‖g m‖) → ‖f n‖ ≤ C * ‖g n‖

Tactic:
refine ⟨C₀, ?_⟩

Goal state after:
f g : ℕ → ℝ
hf : ∀ᶠ (n : ℕ) in atTop, 0 ≤ f n
hg : ∀ᶠ (n : ℕ) in atTop, 0 < g n
hrec : ∀ᶠ (n₀ : ℕ) in atTop, ∃ C₀, ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, f m ≤ C * g m) → f n ≤ C * g n
n₀ : ℕ
hn₀ : ∀ (y : ℕ), n₀ ≤ y → 0 < g y
hn₀' : ∀ (y : ℕ), n₀ ≤ y → 0 ≤ f y
C₀ : ℝ
hnrec : ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, f m ≤ C * g m) → f n ≤ C * g n
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, ‖f m‖ ≤ C * ‖g m‖) → ‖f n‖ ≤ C * ‖g n‖
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 : ℕ
hj : j ≥ i
hfij : f j ≤ f i
⊢ a - l • ε + ε < f j + ε

Tactic:
gcongr; exact hl _ <| hi.1.trans hj

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

Goal state before:
pp: α : Type u_1
l : Filter α
f : α → ℝ
⊢ Tendsto (fun x ↦ rexp (f x)) l (𝓝 0) ↔ Tendsto f l atBot

Tactic:
simp_rw [← comp_apply (f := exp), ← tendsto_comap_iff, comap_exp_nhds_zero]

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

Goal state before:
pp: x : ℝ
hl : 0 ≤ x
hu : x ≤ π
⊢ sin x = √(1 - cos x ^ 2)

Tactic:
← abs_sin_eq_sqrt_one_sub_cos_sq,

Goal state after:
x : ℝ
hl : 0 ≤ x
hu : x ≤ π
⊢ sin x = |sin x|
Module: Mathlib.Analysis.Normed.Module.RCLike.Real

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
r : ℝ
⊢ frontier (sphere x r) = sphere x r

Tactic:
rw [isClosed_sphere.frontier_eq, interior_sphere' x, sdiff_empty]

Goal state after:
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
U W : Set X
hW : IsPathConnected W
hWU : W ⊆ U
⊢ IsPathConnected (Subtype.val ⁻¹' W)

Tactic:
by
  rwa [IsInducing.subtypeVal.isPathConnected_iff, Subtype.image_preimage_val, inter_eq_right.2 hWU]

Goal state after:
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: X : Type u_2
Y : Type u_3
T : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace T
t : Set X
f : T → X → Y
g : C(↑t, Y)
f_cont : ContinuousOn (Function.uncurry f) (univ ×ˢ t)
this : ∀ (x : T), ContinuousOn (f x) t
⊢ Continuous[instTopologicalSpaceProd, inst✝¹] (Function.uncurry fun x y ↦ (mkD (t.domRestrict (f x)) g) y)

Tactic:
conv in mkD _ _ => rw [mkD_of_continuousOn (this x)]

Goal state after:
X : Type u_2
Y : Type u_3
T : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace T
t : Set X
f : T → X → Y
g : C(↑t, Y)
f_cont : ContinuousOn (Function.uncurry f) (univ ×ˢ t)
this : ∀ (x : T), ContinuousOn (f x) t
⊢ Continuous[instTopologicalSpaceProd, inst✝¹]
    (Function.uncurry fun x y ↦ { toFun := t.domRestrict (f x), continuous_toFun := ⋯ } y)
Module: Mathlib.Topology.Path

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
a b c : X
γ₁ : Path a b
γ₂ : Path b c
⊢ range ⇑(γ₁.trans γ₂) = range ⇑γ₁ ∪ range ⇑γ₂

Tactic:
rw [← extend_range, ← image_univ, ← Iic_union_Ici (a := 1 / 2), image_union,
    EqOn.image_eq fun t ht ↦ extend_trans_of_le_half _ _ (mem_Iic.1 ht),
    EqOn.image_eq fun t ht ↦ extend_trans_of_half_le _ _ (mem_Ici.1 ht),
    ← image_image γ₁.extend, ← image_image (γ₂.extend <| · - 1), ← image_image γ₂.extend]

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
a b c : X
γ₁ : Path a b
γ₂ : Path b c
⊢ ⇑γ₁.extend '' HMul.hMul 2 '' Iic (1 / 2) ∪ ⇑γ₂.extend '' (fun x ↦ x - 1) '' HMul.hMul 2 '' Ici (1 / 2) =
    range ⇑γ₁ ∪ range ⇑γ₂
Module: Mathlib.Topology.Path

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
a b c : X
γ₁ : Path a b
γ₂ : Path b c
⊢ ⇑γ₁.extend '' HMul.hMul 2 '' Iic (1 / 2) ∪ ⇑γ₂.extend '' (fun x ↦ x - 1) '' HMul.hMul 2 '' Ici (1 / 2) =
    range ⇑γ₁ ∪ range ⇑γ₂

Tactic:
norm_num [image_mul_left_Ici, image_mul_left_Iic,
    image_extend_of_subset, Icc_subset_Iic_self, Icc_subset_Ici_self]

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

Goal state before:
pp: p x : ℝ
⊢ ‖↑x‖ = ‖↑x‖

Tactic:
by
  suffices ‖(↑(-1 * x) : AddCircle (-1 * p))‖ = ‖(x : AddCircle p)‖ by
    rw [← this, neg_one_mul]
    simp
  simp only [norm_coe_mul, abs_neg, abs_one, one_mul]

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

Goal state before:
pp: case refine_2
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Monotone f
hf0 : Tendsto f atTop (𝓝 0)
hgb : ∀ (n : ℕ), ‖∑ i ∈ Finset.range n, z i‖ ≤ b
n : ℕ
⊢ ‖(f (n + 1) + -f n) • (Finset.range (n + 1)).sum z‖ ≤ b * |f (n + 1) - f n|

Tactic:
· rw [norm_smul, mul_comm]
    exact mul_le_mul_of_nonneg_right (hgb _) (abs_nonneg _)

Goal state after:
Module: Mathlib.Topology.Path

Goal state before:
pp: case refine_3
X : Type u_1
inst✝¹ : TopologicalSpace X
ι : Type u_4
inst✝ : TopologicalSpace ι
a b c : ι → X
γ₁ : (t : ι) → Path (a t) (b t)
h₁ : Continuous[instTopologicalSpaceProd, inst✝¹] ↿γ₁
γ₂ : (t : ι) → Path (b t) (c t)
h₂ : Continuous[instTopologicalSpaceProd, inst✝¹] ↿γ₂
h₁' : Continuous[instTopologicalSpaceProd, inst✝¹] ↿fun t ↦ ⇑(γ₁ t).extend
h₂' : Continuous[instTopologicalSpaceProd, inst✝¹] ↿fun t ↦ ⇑(γ₂ t).extend
⊢ ∀ (x : ι × ↑I), ↑x.2 = 1 / 2 → (γ₁ x.1).extend (2 * ↑x.2) = (γ₂ x.1).extend (2 * ↑x.2 - 1)

Tactic:
rintro st hst

Goal state after:
case refine_3
X : Type u_1
inst✝¹ : TopologicalSpace X
ι : Type u_4
inst✝ : TopologicalSpace ι
a b c : ι → X
γ₁ : (t : ι) → Path (a t) (b t)
h₁ : Continuous[instTopologicalSpaceProd, inst✝¹] ↿γ₁
γ₂ : (t : ι) → Path (b t) (c t)
h₂ : Continuous[instTopologicalSpaceProd, inst✝¹] ↿γ₂
h₁' : Continuous[instTopologicalSpaceProd, inst✝¹] ↿fun t ↦ ⇑(γ₁ t).extend
h₂' : Continuous[instTopologicalSpaceProd, inst✝¹] ↿fun t ↦ ⇑(γ₂ t).extend
st : ι × ↑I
hst : ↑st.2 = 1 / 2
⊢ (γ₁ st.1).extend (2 * ↑st.2) = (γ₂ st.1).extend (2 * ↑st.2 - 1)
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: E : Type u_4
inst✝⁴ : Ring E
inst✝³ : PartialOrder E
inst✝² : IsOrderedRing E
inst✝¹ : TopologicalSpace E
inst✝ : OrderClosedTopology E
l : E
f : ℕ → E
hfl : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 l)
hfm : Monotone f
k n : ℕ
⊢ ∑ i ∈ Finset.range (2 * (n + 1)), (-1) ^ i * f i ≤ ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i

Tactic:
rw [show 2 * (n + 1) = 2 * n + 1 + 1 by ring, sum_range_succ, sum_range_succ]

Goal state after:
E : Type u_4
inst✝⁴ : Ring E
inst✝³ : PartialOrder E
inst✝² : IsOrderedRing E
inst✝¹ : TopologicalSpace E
inst✝ : OrderClosedTopology E
l : E
f : ℕ → E
hfl : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 l)
hfm : Monotone f
k n : ℕ
⊢ ∑ x ∈ Finset.range (2 * n), (-1) ^ x * f x + (-1) ^ (2 * n) * f (2 * n) + (-1) ^ (2 * n + 1) * f (2 * n + 1) ≤
    ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i
Module: Mathlib.Topology.Path

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
f : ↑I → ↑I
hfcont : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
t : ↑I
h₁ : Continuous (IccExtend ⋯ f)
⊢ ∃ a, f a = t

Tactic:
have := intermediate_value_Icc (zero_le_one' ℝ) h₁.continuousOn

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
f : ↑I → ↑I
hfcont : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
t : ↑I
h₁ : Continuous (IccExtend ⋯ f)
this : Icc (IccExtend ⋯ f 0) (IccExtend ⋯ f 1) ⊆ IccExtend ⋯ f '' Icc 0 1
⊢ ∃ a, f a = t
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: E : Type u_4
inst✝⁴ : Ring E
inst✝³ : PartialOrder E
inst✝² : IsOrderedRing E
inst✝¹ : TopologicalSpace E
inst✝ : OrderClosedTopology E
l : E
f : ℕ → E
hfl : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 l)
hfa : Antitone f
k n : ℕ
⊢ ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i ≤ ∑ i ∈ Finset.range (2 * (n + 1)), (-1) ^ i * f i

Tactic:
rw [show 2 * (n + 1) = 2 * n + 1 + 1 by ring, sum_range_succ, sum_range_succ]

Goal state after:
E : Type u_4
inst✝⁴ : Ring E
inst✝³ : PartialOrder E
inst✝² : IsOrderedRing E
inst✝¹ : TopologicalSpace E
inst✝ : OrderClosedTopology E
l : E
f : ℕ → E
hfl : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 l)
hfa : Antitone f
k n : ℕ
⊢ ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i ≤
    ∑ x ∈ Finset.range (2 * n), (-1) ^ x * f x + (-1) ^ (2 * n) * f (2 * n) + (-1) ^ (2 * n + 1) * f (2 * n + 1)
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: E : Type u_4
inst✝⁴ : Ring E
inst✝³ : PartialOrder E
inst✝² : IsOrderedRing E
inst✝¹ : TopologicalSpace E
inst✝ : OrderClosedTopology E
l : E
f : ℕ → E
hfl : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 l)
hfa : Antitone f
k n : ℕ
⊢ ∑ i ∈ Finset.range (2 * (n + 1) + 1), (-1) ^ i * f i ≤ ∑ i ∈ Finset.range (2 * n + 1), (-1) ^ i * f i

Tactic:
rw [show 2 * (n + 1) = 2 * n + 1 + 1 by ring, sum_range_succ, sum_range_succ]

Goal state after:
E : Type u_4
inst✝⁴ : Ring E
inst✝³ : PartialOrder E
inst✝² : IsOrderedRing E
inst✝¹ : TopologicalSpace E
inst✝ : OrderClosedTopology E
l : E
f : ℕ → E
hfl : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 l)
hfa : Antitone f
k n : ℕ
⊢ ∑ x ∈ Finset.range (2 * n + 1), (-1) ^ x * f x + (-1) ^ (2 * n + 1) * f (2 * n + 1) +
      (-1) ^ (2 * n + 2) * f (2 * n + 2) ≤
    ∑ i ∈ Finset.range (2 * n + 1), (-1) ^ i * f i
Module: Mathlib.Analysis.Normed.Group.AddCircle

Goal state before:
pp: p : ℝ
hp : Fact (0 < p)
u : AddCircle p
hu : IsOfFinAddOrder u
n : ℕ := addOrderOf u
⊢ ∃ k, ‖u‖ = p * (↑k / ↑(addOrderOf u))

Tactic:
change ∃ k : ℕ, ‖u‖ = p * (k / n)

Goal state after:
p : ℝ
hp : Fact (0 < p)
u : AddCircle p
hu : IsOfFinAddOrder u
n : ℕ := addOrderOf u
⊢ ∃ k, ‖u‖ = p * (↑k / ↑n)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: x : ℝ
⊢ tan (arcsin x) = x / √(1 - x ^ 2)

Tactic:
rw [tan_eq_sin_div_cos, cos_arcsin]
  by_cases hx₁ : -1 ≤ x; swap
  · have h : √(1 - x ^ 2) = 0 := sqrt_eq_zero_of_nonpos (by nlinarith)
    rw [h]
    simp
  by_cases hx₂ : x ≤ 1; swap
  · have h : √(1 - x ^ 2) = 0 := sqrt_eq_zero_of_nonpos (by nlinarith)
    rw [h]
    simp
  rw [sin_arcsin hx₁ hx₂]

Goal state after: