mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝² : SFinite ν
R : Type u_3
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
c : R
s : Set (α × β)
hs : MeasurableSet s
A : ∀ (s : Set β), c • ν s = c • 1 * ν s
⊢ ∫⁻ (x : α), c • ν (Prod.mk x ⁻¹' s) ∂μ = c • ∫⁻ (x : α), ν (Prod.mk x ⁻¹' s) ∂μ

Tactic:
A

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝² : SFinite ν
R : Type u_3
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
c : R
s : Set (α × β)
hs : MeasurableSet s
A : ∀ (s : Set β), c • ν s = c • 1 * ν s
⊢ ∫⁻ (x : α), c • 1 * ν (Prod.mk x ⁻¹' s) ∂μ = c • ∫⁻ (x : α), ν (Prod.mk x ⁻¹' s) ∂μ
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
x y : V₁
⊢ dist (f x) (f y) ≤ ↑⟨‖f‖, ⋯⟩ * dist x y

Tactic:
rw [dist_eq_norm, dist_eq_norm, ← map_sub]
    apply le_opNorm

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Basic

Goal state before:
pp: E : Type u_2
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CStarRing E
x : E
hx : IsSelfAdjoint x
n : ℕ
⊢ ‖x ^ 2 ^ n‖₊ = ‖x‖₊ ^ 2 ^ n

Tactic:
induction n with

Goal state after:
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ ↑(re z) + ↑(im z) * I + (↑(re z) - ↑(im z) * I) = 2 * ↑(re z)

Tactic:
by rw [add_add_sub_cancel, two_mul]

Goal state after:
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
x y : ℝ
⊢ ↑x < ↑y ↔ x < y

Tactic:
lt_iff_re_im

Goal state after:
K : Type u_1
inst✝ : RCLike K
x y : ℝ
⊢ re ↑x < re ↑y ∧ im ↑x = im ↑y ↔ x < y
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
x : K
hx : 0 ≤ x
⊢ ↑‖x‖ = x

Tactic:
rw [eq_comm, ← norm_le_re_iff_eq_norm, ← sqrt_normSq_eq_norm, normSq_apply]

Goal state after:
K : Type u_1
inst✝ : RCLike K
x : K
hx : 0 ≤ x
⊢ √(re x * re x + im x * im x) ≤ re x
Module: Mathlib.Topology.OpenPartialHomeomorph.Continuity

Goal state before:
pp: X : Type u_1
Y : Type u_3
Z : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
e : OpenPartialHomeomorph X Y
s : Set X
t : Set Z
x : X
f : X → Z
hf : ContinuousWithinAt f s x
hxe : x ∈ e.source
ht : t ∈ 𝓝 (f x)
⊢ ↑e.symm ⁻¹' s =ᶠ[𝓝 (↑e x)] e.target ∩ ↑e.symm ⁻¹' (s ∩ f ⁻¹' t)

Tactic:
rw [eventuallyEq_set, e.eventually_nhds _ hxe]

Goal state after:
X : Type u_1
Y : Type u_3
Z : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
e : OpenPartialHomeomorph X Y
s : Set X
t : Set Z
x : X
f : X → Z
hf : ContinuousWithinAt f s x
hxe : x ∈ e.source
ht : t ∈ 𝓝 (f x)
⊢ ∀ᶠ (x : X) in 𝓝 x, ↑e x ∈ ↑e.symm ⁻¹' s ↔ ↑e x ∈ e.target ∩ ↑e.symm ⁻¹' (s ∩ f ⁻¹' t)
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
x✝ : K
⊢ (map K ℝ) x✝ = reCLM x✝

Tactic:
simp only [map_apply, I, mul_zero, add_zero]

Goal state after:
K : Type u_1
inst✝ : RCLike K
x✝ : K
⊢ ↑(re x✝) = reCLM x✝
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ im z ≤ -‖z‖ ↔ z = -(I * ↑‖z‖)

Tactic:
by
  simpa [neg_eq_iff_eq_neg, le_neg] using norm_le_im_iff_eq_I_mul_norm (z := -z)

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

Goal state before:
pp: α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
l : Filter α
h : f =o[l] g
hg : ∀ᶠ (x : α) in l, 0 < ‖g x‖
x : α
x✝ : ‖f x‖ ≤ 2⁻¹ * ‖g x‖ ∧ 0 < ‖g x‖
hx₁ : ‖f x‖ ≤ 2⁻¹ * ‖g x‖
hx₂ : 0 < ‖g x‖
⊢ 2⁻¹ * ‖g x‖ < ‖g x‖

Tactic:
mul_lt_iff_lt_one_left hx₂

Goal state after:
α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
l : Filter α
h : f =o[l] g
hg : ∀ᶠ (x : α) in l, 0 < ‖g x‖
x : α
x✝ : ‖f x‖ ≤ 2⁻¹ * ‖g x‖ ∧ 0 < ‖g x‖
hx₁ : ‖f x‖ ≤ 2⁻¹ * ‖g x‖
hx₂ : 0 < ‖g x‖
⊢ 2⁻¹ < 1
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 : α
hx₁ : ‖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‖
hx₂ : ‖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 : α
hx₁ : ‖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‖
hx₂ : ‖f₂ x‖ ≤ c₂ * ‖g₂ x‖
⊢ ‖f₁ x + f₂ x‖ ≤ max c₁ c₂ * ‖‖g₁ x‖ + ‖g₂ x‖‖
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✝ : α
hx₁ : ‖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✝‖
hx₂ : ‖f₂ a✝‖ ≤ c₂ * ‖g₂ a✝‖
⊢ ‖f₁ a✝ * f₂ a✝‖ ≤ c₁ * c₂ * ‖g₁ a✝ * g₂ a✝‖
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 : α → R
g : α → S
h : f =o[l] g
n : ℕ
⊢ (fun x ↦ f x ^ n.succ) =o[l] fun x ↦ g x ^ n.succ

Tactic:
induction n with

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
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
⊢ ∃ i,
    ∀ j ≥ i, abv ((∑ k ∈ range j, f k) * ∑ k ∈ range j, g k - ∑ n ∈ range j, ∑ m ∈ range (n + 1), f m * g (n - m)) < ε

Tactic:
let ⟨Q, hQ⟩ := hb.bounded

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
⊢ ∃ i,
    ∀ j ≥ i, abv ((∑ k ∈ range j, f k) * ∑ k ∈ range j, g k - ∑ n ∈ range j, ∑ m ∈ range (n + 1), f m * g (n - m)) < ε
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✝ : α
hx₁ : ‖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✝‖
hx₂ : ‖f' a✝‖ ≤ c' * ‖g' a✝‖
⊢ ‖k₁ a✝ • f' a✝‖ ≤ c * c' * ‖k₂ a✝ • g' a✝‖
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
⊢ ∑ i ∈ range K, f i * ∑ k ∈ range (K - i), g k =
    ∑ x ∈ range K, (f x * (∑ k ∈ range (K - x), g k - ∑ k ∈ range K, g k) + f x * ∑ k ∈ range K, g k)

Tactic:
simp [(mul_add _ _ _).symm]

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

Goal state before:
pp: x : ℂ
h : cexp x = 0
⊢ 0 = 1

Tactic:
by rw [← exp_zero, ← add_neg_cancel x, exp_add, h]; simp

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

Goal state before:
pp: case mpr
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
u v φ : α → 𝕜
hφ : Tendsto φ l (𝓝 0)
huvφ : u =ᶠ[l] φ * v
c : ℝ
hpos : 0 < c
⊢ IsBigOWith c l u v

Tactic:
rw [NormedAddGroup.tendsto_nhds_zero] at hφ

Goal state after:
case mpr
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
u v φ : α → 𝕜
hφ : ∀ ε > 0, ∀ᶠ (x : α) in l, ‖φ x‖ < ε
huvφ : u =ᶠ[l] φ * v
c : ℝ
hpos : 0 < c
⊢ IsBigOWith c l u v
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
⊢ tanh ((starRingEnd ℂ) x) = (starRingEnd ℂ) (tanh x)

Tactic:
tanh,

Goal state after:
x : ℂ
⊢ sinh ((starRingEnd ℂ) x) / cosh ((starRingEnd ℂ) x) = (starRingEnd ℂ) (tanh x)
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
c : ℝ
l : Filter α
f₁ f₂ : α → E'
h : IsBigOWith c l f₁ f₂
hc : c < 1
x : α
⊢ -(-f₂ x - f₁ x) = f₁ x + f₂ x

Tactic:
rw [neg_sub, sub_neg_eq_add]

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

Goal state before:
pp: case hab
⊢ cos 1 ≤ 5 / 9

Tactic:
· apply cos_one_le

Goal state after:
Module: Mathlib.Analysis.Normed.Ring.InfiniteSum

Goal state before:
pp: R : Type u_1
inst✝ : NormedRing R
f g : ℕ → R
hf : Summable fun x ↦ ‖f x‖
h'f : Summable f
hg : Summable fun x ↦ ‖g x‖
h'g : Summable g
⊢ HasSum (fun n ↦ ∑ k ∈ range (n + 1), f k * g (n - k)) ((∑' (n : ℕ), f n) * ∑' (n : ℕ), g n)

Tactic:
convert! (summable_sum_mul_range_of_summable_norm' hf h'f hg h'g).hasSum

Goal state after:
R : Type u_1
inst✝ : NormedRing R
f g : ℕ → R
hf : Summable fun x ↦ ‖f x‖
h'f : Summable f
hg : Summable fun x ↦ ‖g x‖
h'g : Summable g
⊢ (∑' (n : ℕ), f n) * ∑' (n : ℕ), g n = ∑' (b : ℕ), ∑ k ∈ range (b + 1), f k * g (b - k)
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
⊢ ∑ i ∈ range K with max N M + 1 ≤ i, abv (f i) * abv (∑ k ∈ range (K - i), g k - ∑ k ∈ range K, g k) ≤
    ∑ i ∈ range K with max N M + 1 ≤ i, abv (f i) * (2 * Q)

Tactic:
by
        gcongr
        rw [sub_eq_add_neg]
        grw [abv_add abv]
        rw [two_mul, abv_neg abv]
        gcongr <;> exact le_of_lt (hQ _)

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

Goal state before:
pp: n : ℕ
C : ℝ
hC₁ : 1 ≤ C
hC₀ : 0 < C
this : 0 < (rexp 1 * C)⁻¹
N : ℕ
hN : ∀ k ≥ N, ↑k ^ n < rexp ↑k / (rexp 1 * C)
x : ℝ
hx : ↑N < x
hx₀ : 0 < x
⊢ x ^ n ≤ ↑⌈x⌉₊ ^ n

Tactic:
gcongr; exact Nat.le_ceil _

Goal state after:
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
⊢ f = 0

Tactic:
ext n

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 n
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: ⊢ Set.range rexp = Set.Ioi 0

Tactic:
by
  rw [← coe_comp_expOrderIso, range_comp, expOrderIso.range_eq, image_univ, Subtype.range_coe]

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

Goal state before:
pp: ⊢ comap re (comap Real.exp atTop) = comap re atTop

Tactic:
rw [Real.comap_exp_atTop]

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

Goal state before:
pp: ⊢ comap cexp (𝓝 0) = comap re (comap Real.exp (𝓝 0))

Tactic:
by
      rw [← comap_norm_nhds_zero, comap_comap, Function.comp_def]
      simp_rw [norm_exp, comap_comap, Function.comp_def]

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‖ = 0 ↔ m ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑S

Tactic:
rw [norm_mk, ← mem_closure_iff_infDist_zero]
  exact ⟨1, S.one_mem⟩

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

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
s : Set E
⊢ (cthickening δ s)⁻¹ = cthickening δ s⁻¹

Tactic:
simp_rw [cthickening, ← infEDist_inv]

Goal state after:
E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
s : Set E
⊢ {x | infEDist x s ≤ ENNReal.ofReal δ}⁻¹ = {x | infEDist x⁻¹ s ≤ ENNReal.ofReal δ}
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
tfae_5_to_3 :
  (∃ a < R, ∃ C, (0 < C ∨ 0 < R) ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n) → ∃ 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
n : ℕ
hn : |f n| ≤ |a ^ n|
⊢ |f n| ≤ a ^ n

Tactic:
abs_pow,

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
tfae_5_to_3 :
  (∃ a < R, ∃ C, (0 < C ∨ 0 < R) ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n) → ∃ 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
n : ℕ
hn : |f n| ≤ |a| ^ n
⊢ |f n| ≤ a ^ n
Module: Mathlib.Analysis.Normed.Module.RCLike.Real

Goal state before:
pp: case convert_3
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
y : E
hy : ‖y - x‖ ≤ r
this : ContinuousWithinAt (fun c ↦ c • (y - x) + x) (Ico 0 1) 1
c : ℝ
hc0 : 0 ≤ c
hc1 : c < 1
hr : 0 < r
⊢ ‖y - x‖ * c < r * 1

Tactic:
apply mul_lt_mul'

Goal state after:
case convert_3.h₁
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
y : E
hy : ‖y - x‖ ≤ r
this : ContinuousWithinAt (fun c ↦ c • (y - x) + x) (Ico 0 1) 1
c : ℝ
hc0 : 0 ≤ c
hc1 : c < 1
hr : 0 < r
⊢ ‖y - x‖ ≤ r

case h₂
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
y : E
hy : ‖y - x‖ ≤ r
this : ContinuousWithinAt (fun c ↦ c • (y - x) + x) (Ico 0 1) 1
c : ℝ
hc0 : 0 ≤ c
hc1 : c < 1
hr : 0 < r
⊢ c < 1

case c0
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
y : E
hy : ‖y - x‖ ≤ r
this : ContinuousWithinAt (fun c ↦ c • (y - x) + x) (Ico 0 1) 1
c : ℝ
hc0 : 0 ≤ c
hc1 : c < 1
hr : 0 < r
⊢ 0 ≤ c

case b0
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
y : E
hy : ‖y - x‖ ≤ r
this : ContinuousWithinAt (fun c ↦ c • (y - x) + x) (Ico 0 1) 1
c : ℝ
hc0 : 0 ≤ c
hc1 : c < 1
hr : 0 < r
⊢ 0 < r
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : NormSMulClass 𝕜 E
c : 𝕜
x : Set E
⊢ (‖c‖₊ • ediam x).toReal = ‖c‖ * (ediam x).toReal

Tactic:
ENNReal.toReal_smul,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : NormSMulClass 𝕜 E
c : 𝕜
x : Set E
⊢ ‖c‖₊ • (ediam x).toReal = ‖c‖ * (ediam x).toReal
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: n : ℕ
⊢ 1 - (2 / 2 ^ 2 + sqrtTwoAddSeries 0 n / 2 ^ 2) = 1 / 2 - sqrtTwoAddSeries 0 n / 4

pp: n : ℕ
⊢ 0 ≤ 2 + sqrtTwoAddSeries 0 n

Tactic:
← sub_sub

Goal state after:
n : ℕ
⊢ 1 - 2 / 2 ^ 2 - sqrtTwoAddSeries 0 n / 2 ^ 2 = 1 / 2 - sqrtTwoAddSeries 0 n / 4

n : ℕ
⊢ 0 ≤ 2 + sqrtTwoAddSeries 0 n
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

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

Tactic:
trans cos (π / 2 ^ 2)

Goal state after:
⊢ cos (π / 4) = cos (π / 2 ^ 2)

⊢ cos (π / 2 ^ 2) = √2 / 2
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : NormSMulClass 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
⊢ (‖c‖₊ • infEDist x s).toReal = ‖c‖ * (infEDist x s).toReal

Tactic:
ENNReal.toReal_smul,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : NormSMulClass 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
⊢ ‖c‖₊ • (infEDist x s).toReal = ‖c‖ * (infEDist x s).toReal
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: R : Type u_4
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
k✝ : ℕ
r : R
hr : ‖r‖ < 1
k : ℕ
hk : ∀ m < k, Summable fun n ↦ ↑n ^ m * r ^ n
a : ℕ → ℕ
ha : ∀ (n : ℕ), (n + k).descFactorial k = n ^ k + ∑ i ∈ Finset.range k, a i * n ^ i
this : Summable fun n ↦ ↑((n + k).descFactorial k) * r ^ n - ∑ i ∈ Finset.range k, ↑(a i) * ↑n ^ i * r ^ n
⊢ (fun n ↦ ↑n ^ k * r ^ n) = fun n ↦ ↑((n + k).descFactorial k) * r ^ n - ∑ i ∈ Finset.range k, ↑(a i) * ↑n ^ i * r ^ n

Tactic:
ext n

Goal state after:
R : Type u_4
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
k✝ : ℕ
r : R
hr : ‖r‖ < 1
k : ℕ
hk : ∀ m < k, Summable fun n ↦ ↑n ^ m * r ^ n
a : ℕ → ℕ
ha : ∀ (n : ℕ), (n + k).descFactorial k = n ^ k + ∑ i ∈ Finset.range k, a i * n ^ i
this : Summable fun n ↦ ↑((n + k).descFactorial k) * r ^ n - ∑ i ∈ Finset.range k, ↑(a i) * ↑n ^ i * r ^ n
n : ℕ
⊢ ↑n ^ k * r ^ n = ↑((n + k).descFactorial k) * r ^ n - ∑ i ∈ Finset.range k, ↑(a i) * ↑n ^ i * r ^ n