mathlib-initiative/mathlib-tactics huggingface dataset:
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 g : NormedAddGroupHom V₁ V₂
h : f.toAddMonoidHom = g.toAddMonoidHom
⊢ ⇑f = ⇑g

Tactic:
← coe_toAddMonoidHom f,

Goal state after:
V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
f g : NormedAddGroupHom V₁ V₂
h : f.toAddMonoidHom = g.toAddMonoidHom
⊢ ⇑f.toAddMonoidHom = ⇑g
Module: Mathlib.Analysis.CStarAlgebra.Basic

Goal state before:
pp: E : Type u_2
inst✝¹ : NonUnitalNormedRing E
inst✝ : StarRing E
h : ∀ (x : E), ‖x‖ * ‖x‖ ≤ ‖x * x⋆‖
x : E
⊢ ‖x⋆‖ ≤ ‖x‖

Tactic:
obtain (hx | hx) := eq_zero_or_norm_pos x⋆

Goal state after:
case inl
E : Type u_2
inst✝¹ : NonUnitalNormedRing E
inst✝ : StarRing E
h : ∀ (x : E), ‖x‖ * ‖x‖ ≤ ‖x * x⋆‖
x : E
hx : x⋆ = 0
⊢ ‖x⋆‖ ≤ ‖x‖

case inr
E : Type u_2
inst✝¹ : NonUnitalNormedRing E
inst✝ : StarRing E
h : ∀ (x : E), ‖x‖ * ‖x‖ ≤ ‖x * x⋆‖
x : E
hx : 0 < ‖x⋆‖
⊢ ‖x⋆‖ ≤ ‖x‖
Module: Mathlib.Analysis.CStarAlgebra.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
α : Type u_3
inst✝² : NonUnitalNormedRing E
inst✝¹ : StarRing E
inst✝ : CStarRing E
x : E
⊢ ‖x⋆‖ ≤ ‖x‖

Tactic:
obtain (hx | hx) := eq_zero_or_norm_pos x⋆

Goal state after:
case inl
𝕜 : Type u_1
E : Type u_2
α : Type u_3
inst✝² : NonUnitalNormedRing E
inst✝¹ : StarRing E
inst✝ : CStarRing E
x : E
hx : x⋆ = 0
⊢ ‖x⋆‖ ≤ ‖x‖

case inr
𝕜 : Type u_1
E : Type u_2
α : Type u_3
inst✝² : NonUnitalNormedRing E
inst✝¹ : StarRing E
inst✝ : CStarRing E
x : E
hx : 0 < ‖x⋆‖
⊢ ‖x⋆‖ ≤ ‖x‖
Module: Mathlib.Algebra.Star.Unitary

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarMul R
U B : R
x✝¹ : U ∈ {U | star U * U = 1 ∧ U * star U = 1}
x✝ : B ∈ {U | star U * U = 1 ∧ U * star U = 1}
hA₁ : star U * U = 1
hA₂ : U * star U = 1
hB₁ : star B * B = 1
hB₂ : B * star B = 1
⊢ U * B * (star B * star U) = U * (B * star B) * star U

Tactic:
simp_rw [← mul_assoc]

Goal state after:
Module: Mathlib.Algebra.Star.Unitary

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarMul R
u : ↥(unitary R)
⊢ Commute u (star u)

Tactic:
by simp [commute_iff_eq]

Goal state after:
Module: Mathlib.Algebra.Star.Unitary

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarMul R
u : ↥(unitary R)
⊢ Commute (star u) u

Tactic:
by simp [commute_iff_eq]

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.ContinuousLinearMap

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : SeminormedRing 𝕜
inst✝³ : Ring 𝕜₂
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : IsBoundedSMul 𝕜 E
f : 𝕜 →ₗ[𝕜] E
x : 𝕜
⊢ ‖x • f 1‖ ≤ ‖f 1‖ * ‖x‖

Tactic:
mul_comm

Goal state after:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : SeminormedRing 𝕜
inst✝³ : Ring 𝕜₂
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : IsBoundedSMul 𝕜 E
f : 𝕜 →ₗ[𝕜] E
x : 𝕜
⊢ ‖x • f 1‖ ≤ ‖x‖ * ‖f 1‖
Module: Mathlib.Analysis.CStarAlgebra.Basic

Goal state before:
pp: 𝕜✝ : Type u_1
E : Type u_2
α : Type u_3
𝕜 : Type u_4
A : Type u_5
inst✝⁵ : NormedField 𝕜
inst✝⁴ : StarRing 𝕜
inst✝³ : SeminormedRing A
inst✝² : StarRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : StarModule 𝕜 A
S : StarSubalgebra 𝕜 A
⊢ NormedAlgebra 𝕜 ↥S

Tactic:
infer_instance

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : SMul R ℝ
inst✝¹ : SMul S ℝ
inst✝ : SMulCommClass R S ℝ
r : R
s : S
x : ℂ
⊢ r • s • x = s • r • x

Tactic:
ext <;> simp [smul_re, smul_im, smul_comm]

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
r : ℝ
⊢ r * re z = re z * r

Tactic:
mul_comm

Goal state after:
K : Type u_1
inst✝ : RCLike K
z : K
r : ℝ
⊢ re z * r = re z * r
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
r : ℝ
⊢ r * im z = im z * r

Tactic:
mul_comm

Goal state after:
K : Type u_1
inst✝ : RCLike K
z : K
r : ℝ
⊢ im z * r = im z * r
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: A : Type u_1
inst✝⁵ : NonUnitalNonAssocRing A
inst✝⁴ : StarRing A
inst✝³ : Module ℂ A
inst✝² : IsScalarTower ℂ A A
inst✝¹ : SMulCommClass ℂ A A
inst✝ : StarModule ℂ A
x : A
⊢ IsStarNormal x ↔ Commute ↑(ℜ x) ↑(ℑ x)

Tactic:
isStarNormal_iff,

Goal state after:
A : Type u_1
inst✝⁵ : NonUnitalNonAssocRing A
inst✝⁴ : StarRing A
inst✝³ : Module ℂ A
inst✝² : IsScalarTower ℂ A A
inst✝¹ : SMulCommClass ℂ A A
inst✝ : StarModule ℂ A
x : A
⊢ Commute (star x) x ↔ Commute ↑(ℜ x) ↑(ℑ x)
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
f : CauSeq K norm
x✝ : ℝ
ε0 : x✝ > 0
i : ℕ
H : ∀ j ≥ i, ‖↑f j - ↑f i‖ < x✝
j : ℕ
ij : j ≥ i
⊢ |(fun n ↦ im (↑f n)) j - (fun n ↦ im (↑f n)) i| ≤ ‖↑f j - ↑f i‖

Tactic:
simpa only [map_sub] using abs_im_le_norm (f j - f i)

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
x y : K
⊢ ‖re (x - y)‖ ≤ ‖x - y‖

Tactic:
exact norm_re_le_norm (x - y)

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

Goal state before:
pp: α : Type u_1
E : Type u_3
F : Type u_4
G : Type u_5
inst✝² : Norm E
inst✝¹ : Norm F
inst✝ : Norm G
c : ℝ
f : α → E
g : α → F
k : α → G
l : Filter α
hgk : IsBigOWith c l g k
hc : 0 < c
hfg : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f g
⊢ ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f k

Tactic:
intro c'

Goal state after:
α : Type u_1
E : Type u_3
F : Type u_4
G : Type u_5
inst✝² : Norm E
inst✝¹ : Norm F
inst✝ : Norm G
c : ℝ
f : α → E
g : α → F
k : α → G
l : Filter α
hgk : IsBigOWith c l g k
hc : 0 < c
hfg : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f g
c' : ℝ
⊢ 0 < c' → IsBigOWith c' l f k
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
E : Type u_3
F : Type u_4
G : Type u_5
inst✝² : Norm E
inst✝¹ : Norm F
inst✝ : Norm G
c : ℝ
f : α → E
g : α → F
k : α → G
l : Filter α
hfg : IsBigOWith c l f g
hc : 0 < c
hgk : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l g k
⊢ ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f k

Tactic:
intro c'

Goal state after:
α : Type u_1
E : Type u_3
F : Type u_4
G : Type u_5
inst✝² : Norm E
inst✝¹ : Norm F
inst✝ : Norm G
c : ℝ
f : α → E
g : α → F
k : α → G
l : Filter α
hfg : IsBigOWith c l f g
hc : 0 < c
hgk : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l g k
c' : ℝ
⊢ 0 < c' → IsBigOWith c' l f 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 : ℕ → β
a : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ a m
⊢ (IsCauSeq abs fun n ↦ ∑ i ∈ range n, a i) → IsCauSeq abv fun n ↦ ∑ i ∈ range n, f i

Tactic:
intro hg ε ε0

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
a : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ a m
hg : IsCauSeq abs fun n ↦ ∑ i ∈ range n, a i
ε : α
ε0 : ε > 0
⊢ ∃ i, ∀ j ≥ i, abv ((fun n ↦ ∑ i ∈ range n, f i) j - (fun n ↦ ∑ i ∈ range n, f i) i) < ε
Module: Mathlib.Analysis.Normed.Operator.LinearIsometry

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R₄ : Type u_4
E : Type u_5
E₂ : Type u_6
E₃ : Type u_7
E₄ : Type u_8
F : Type u_9
𝓕 : Type u_10
inst✝³⁵ : Semiring R
inst✝³⁴ : Semiring R₂
inst✝³³ : Semiring R₃
inst✝³² : Semiring R₄
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
σ₁₃ : R →+* R₃
σ₃₁ : R₃ →+* R
σ₁₄ : R →+* R₄
σ₄₁ : R₄ →+* R
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
σ₂₄ : R₂ →+* R₄
σ₄₂ : R₄ →+* R₂
σ₃₄ : R₃ →+* R₄
σ₄₃ : R₄ →+* R₃
inst✝³¹ : RingHomInvPair σ₁₂ σ₂₁
inst✝³⁰ : RingHomInvPair σ₂₁ σ₁₂
inst✝²⁹ : RingHomInvPair σ₁₃ σ₃₁
inst✝²⁸ : RingHomInvPair σ₃₁ σ₁₃
inst✝²⁷ : RingHomInvPair σ₂₃ σ₃₂
inst✝²⁶ : RingHomInvPair σ₃₂ σ₂₃
inst✝²⁵ : RingHomInvPair σ₁₄ σ₄₁
inst✝²⁴ : RingHomInvPair σ₄₁ σ₁₄
inst✝²³ : RingHomInvPair σ₂₄ σ₄₂
inst✝²² : RingHomInvPair σ₄₂ σ₂₄
inst✝²¹ : RingHomInvPair σ₃₄ σ₄₃
inst✝²⁰ : RingHomInvPair σ₄₃ σ₃₄
inst✝¹⁹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹⁸ : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄
inst✝¹⁷ : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst✝¹⁶ : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst✝¹⁵ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
inst✝¹⁴ : RingHomCompTriple σ₄₂ σ₂₁ σ₄₁
inst✝¹³ : RingHomCompTriple σ₄₃ σ₃₂ σ₄₂
inst✝¹² : RingHomCompTriple σ₄₃ σ₃₁ σ₄₁
inst✝¹¹ : SeminormedAddCommGroup E
inst✝¹⁰ : SeminormedAddCommGroup E₂
inst✝⁹ : SeminormedAddCommGroup E₃
inst✝⁸ : SeminormedAddCommGroup E₄
inst✝⁷ : Module R E
inst✝⁶ : Module R₂ E₂
inst✝⁵ : Module R₃ E₃
inst✝⁴ : Module R₄ E₄
inst✝³ : NormedAddCommGroup F
inst✝² : Module R F
e : E ≃ₛₗᵢ[σ₁₂] E₂
α : Type u_11
inst✝¹ : TopologicalSpace α
inst✝ : Module R E₂
⊢ ∀ (x : E × E₂), ‖(LinearEquiv.prodComm R E E₂) x‖ = ‖x‖

Tactic:
intro

Goal state after:
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R₄ : Type u_4
E : Type u_5
E₂ : Type u_6
E₃ : Type u_7
E₄ : Type u_8
F : Type u_9
𝓕 : Type u_10
inst✝³⁵ : Semiring R
inst✝³⁴ : Semiring R₂
inst✝³³ : Semiring R₃
inst✝³² : Semiring R₄
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
σ₁₃ : R →+* R₃
σ₃₁ : R₃ →+* R
σ₁₄ : R →+* R₄
σ₄₁ : R₄ →+* R
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
σ₂₄ : R₂ →+* R₄
σ₄₂ : R₄ →+* R₂
σ₃₄ : R₃ →+* R₄
σ₄₃ : R₄ →+* R₃
inst✝³¹ : RingHomInvPair σ₁₂ σ₂₁
inst✝³⁰ : RingHomInvPair σ₂₁ σ₁₂
inst✝²⁹ : RingHomInvPair σ₁₃ σ₃₁
inst✝²⁸ : RingHomInvPair σ₃₁ σ₁₃
inst✝²⁷ : RingHomInvPair σ₂₃ σ₃₂
inst✝²⁶ : RingHomInvPair σ₃₂ σ₂₃
inst✝²⁵ : RingHomInvPair σ₁₄ σ₄₁
inst✝²⁴ : RingHomInvPair σ₄₁ σ₁₄
inst✝²³ : RingHomInvPair σ₂₄ σ₄₂
inst✝²² : RingHomInvPair σ₄₂ σ₂₄
inst✝²¹ : RingHomInvPair σ₃₄ σ₄₃
inst✝²⁰ : RingHomInvPair σ₄₃ σ₃₄
inst✝¹⁹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹⁸ : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄
inst✝¹⁷ : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst✝¹⁶ : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst✝¹⁵ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
inst✝¹⁴ : RingHomCompTriple σ₄₂ σ₂₁ σ₄₁
inst✝¹³ : RingHomCompTriple σ₄₃ σ₃₂ σ₄₂
inst✝¹² : RingHomCompTriple σ₄₃ σ₃₁ σ₄₁
inst✝¹¹ : SeminormedAddCommGroup E
inst✝¹⁰ : SeminormedAddCommGroup E₂
inst✝⁹ : SeminormedAddCommGroup E₃
inst✝⁸ : SeminormedAddCommGroup E₄
inst✝⁷ : Module R E
inst✝⁶ : Module R₂ E₂
inst✝⁵ : Module R₃ E₃
inst✝⁴ : Module R₄ E₄
inst✝³ : NormedAddCommGroup F
inst✝² : Module R F
e : E ≃ₛₗᵢ[σ₁₂] E₂
α : Type u_11
inst✝¹ : TopologicalSpace α
inst✝ : Module R E₂
x✝ : E × E₂
⊢ ‖(LinearEquiv.prodComm R E E₂) x✝‖ = ‖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
h₁ : f₁ =O[l] g₁
h₂ : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f₂ g₂
c : ℝ
cpos : 0 < c
⊢ IsBigOWith c l (fun x ↦ f₁ x * f₂ x) fun x ↦ g₁ x * g₂ x

Tactic:
rcases h₁.exists_pos with ⟨c', c'pos, hc'⟩

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
h₁ : f₁ =O[l] g₁
h₂ : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f₂ g₂
c : ℝ
cpos : 0 < c
c' : ℝ
c'pos : c' > 0
hc' : IsBigOWith c' l f₁ g₁
⊢ IsBigOWith c l (fun x ↦ f₁ x * f₂ x) fun x ↦ 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 : α → R
g : α → S
h : f =o[l] g
n : ℕ
hn : 0 < n
⊢ (fun x ↦ f x ^ n) =o[l] fun x ↦ g x ^ n

Tactic:
obtain ⟨n, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hn.ne'; clear hn
  induction n with
  | zero => simpa only [pow_one]
  | succ n ihn => convert! ihn.mul h <;> simp [pow_succ]

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

Goal state before:
pp: α : Type u_1
R : Type u_13
𝕜 : Type u_15
inst✝¹ : SeminormedRing R
inst✝ : NormedDivisionRing 𝕜
l : Filter α
f : α → 𝕜
g : α → R
n : ℕ
hn : n ≠ 0
h : (f ^ n) =O[l] (g ^ n)
C : ℝ
_hC₀ : C > 0
hC : IsBigOWith C l (f ^ n) (g ^ n)
c : ℝ
hc₀ : 0 ≤ c
hc : C ≤ c ^ n
⊢ f =O[l] g

Tactic:
exact (hC.of_pow hn hc hc₀).isBigO

Goal state after:
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 𝕜'
f' : α → E'
g' : α → F'
l : Filter α
inst✝³ : Module R E'
inst✝² : IsBoundedSMul R E'
inst✝¹ : Module 𝕜' F'
inst✝ : NormSMulClass 𝕜' F'
k₁ : α → R
k₂ : α → 𝕜'
h₁ : k₁ =O[l] k₂
h₂ : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f' g'
c : ℝ
cpos : 0 < c
⊢ IsBigOWith c l (fun x ↦ k₁ x • f' x) fun x ↦ k₂ x • g' x

Tactic:
rcases h₁.exists_pos with ⟨c', c'pos, hc'⟩

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 𝕜'
f' : α → E'
g' : α → F'
l : Filter α
inst✝³ : Module R E'
inst✝² : IsBoundedSMul R E'
inst✝¹ : Module 𝕜' F'
inst✝ : NormSMulClass 𝕜' F'
k₁ : α → R
k₂ : α → 𝕜'
h₁ : k₁ =O[l] k₂
h₂ : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f' g'
c : ℝ
cpos : 0 < c
c' : ℝ
c'pos : c' > 0
hc' : IsBigOWith c' l k₁ k₂
⊢ IsBigOWith c l (fun x ↦ k₁ x • f' x) fun x ↦ k₂ x • g' x
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: case inl
α : Type u_1
E'' : Type u_9
F'' : Type u_10
inst✝¹ : NormedAddCommGroup E''
inst✝ : NormedAddCommGroup F''
g'' : α → F''
l : Filter α
⊢ (fun _x ↦ 0) =o[l] g'' ↔ 0 = 0 ∨ Tendsto (norm ∘ g'') l atTop

Tactic:
simp only [isLittleO_zero, true_or]

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

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n j : ℕ
hn : 0 < n
h₁ : ↑n.succ ≠ 1
h₂ : ↑n.succ ≠ 0
h₃ : ↑n.factorial * ↑n ≠ 0
h₄ : ↑n.succ - 1 = ↑n
⊢ ↑n.succ - (↑n.succ)⁻¹ ^ (j - n) * ↑n.succ = ↑n.succ - ↑n.succ * (↑n.succ)⁻¹ ^ (j - n)

Tactic:
mul_comm

Goal state after:
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n j : ℕ
hn : 0 < n
h₁ : ↑n.succ ≠ 1
h₂ : ↑n.succ ≠ 0
h₃ : ↑n.factorial * ↑n ≠ 0
h₄ : ↑n.succ - 1 = ↑n
⊢ ↑n.succ - ↑n.succ * (↑n.succ)⁻¹ ^ (j - n) = ↑n.succ - ↑n.succ * (↑n.succ)⁻¹ ^ (j - n)
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 : α
hx : ‖f₁ x‖ ≤ c * ‖f₂ x‖
⊢ ‖f₂ x‖ - ‖f₂ x‖ * c ≤ ‖f₂ x - f₁ x‖

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 : α
hx : ‖f₁ x‖ ≤ c * ‖f₂ x‖
⊢ 0 < 1 - c

Tactic:
mul_comm

Goal state after:
α : 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 : α
hx : ‖f₁ x‖ ≤ c * ‖f₂ x‖
⊢ ‖f₂ x‖ - c * ‖f₂ x‖ ≤ ‖f₂ x - f₁ x‖

α : 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 : α
hx : ‖f₁ x‖ ≤ c * ‖f₂ x‖
⊢ 0 < 1 - c
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
⊢ sin x * cos x + cos x * sin x = sin x * cos x + sin x * cos x

Tactic:
mul_comm

Goal state after:
x : ℂ
⊢ cos x * sin x + cos x * sin x = cos x * sin x + cos x * sin x
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 (max N M + 1), abv (f i)) * (ε / (2 * P)) < ε / (2 * P) * P

Tactic:
mul_comm

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
⊢ ε / (2 * P) * ∑ i ∈ range (max N M + 1), abv (f i) < ε / (2 * P) * P
Module: Mathlib.Analysis.Complex.Trigonometric

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

Tactic:
rw [mul_comm, norm_exp_ofReal_mul_I]

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

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

Tactic:
mul_comm

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

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n : ℤ
hn : Even n
a : α
⊢ 0 ≤ a ^ n

Tactic:
obtain ⟨k, rfl⟩ := hn; rw [zpow_add' (by simp [em'])]; exact mul_self_nonneg _

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

Goal state before:
pp: case refine_2
f : ℕ → ℝ
r : ℝ
hr : Tendsto (fun n ↦ ∑ i ∈ range n, |f i|) atTop (𝓝 r)
⊢ Tendsto (fun n ↦ ∑ i ∈ range n, ‖f i‖) atTop (𝓝 r)

Tactic:
· simpa only using! hr

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
⊢ [∃ a ∈ Set.Ioo (-R) R, f =o[atTop] fun x ↦ a ^ x, ∃ 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 ∈ Set.Ioo 0 R, f =O[atTop] fun x ↦ a ^ x,
      ∃ a < R, ∃ C, (0 < C ∨ 0 < R) ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n,
      ∃ a ∈ Set.Ioo 0 R, ∃ C > 0, ∀ (n : ℕ), |f n| ≤ C * a ^ n, ∃ a < R, ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n,
      ∃ a ∈ Set.Ioo 0 R, ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n].TFAE

Tactic:
tfae_have 2 → 4 := fun ⟨a, ha, H⟩ ↦ ⟨a, ha, H.isBigO⟩

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
⊢ [∃ a ∈ Set.Ioo (-R) R, f =o[atTop] fun x ↦ a ^ x, ∃ 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 ∈ Set.Ioo 0 R, f =O[atTop] fun x ↦ a ^ x,
      ∃ a < R, ∃ C, (0 < C ∨ 0 < R) ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n,
      ∃ a ∈ Set.Ioo 0 R, ∃ C > 0, ∀ (n : ℕ), |f n| ≤ C * a ^ n, ∃ a < R, ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n,
      ∃ a ∈ Set.Ioo 0 R, ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n].TFAE
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 y * (cexp (x - y) - 1)‖ < ε

Tactic:
mul_comm

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)
⊢ ‖(cexp (x - y) - 1) * cexp y‖ < ε
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
⊢ rexp x / x ^ n ∈ Set.Ici C

Tactic:
rw [Set.mem_Ici, le_div_iff₀ (pow_pos hx₀ _), ← le_div_iff₀' hC₀]

Goal state after:
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 ≤ rexp x / C