mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.CStarAlgebra.Basic

Goal state before:
pp: E : Type u_2
inst✝² : NonUnitalNormedRing E
inst✝¹ : StarRing E
inst✝ : CStarRing E
x : E
⊢ ‖x * x⋆‖ = ‖x‖ * ‖x‖

Tactic:
nth_rw 1 [← star_star x]
  simp only [norm_star_mul_self, norm_star]

Goal state after:
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:
by 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 : R
hu : IsUnit u
⊢ u ∈ unitary R ↔ u * star u = 1

Tactic:
← star_mem_iff,

Goal state after:
R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarMul R
u : R
hu : IsUnit u
⊢ star u ∈ unitary R ↔ u * star u = 1
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: x : ℂ
⊢ ↑x.re + ↑x.im • I ∈ ℝ[I]

Tactic:
← Complex.coe_algebraMap

Goal state after:
x : ℂ
⊢ (algebraMap ℝ ℂ) x.re + (algebraMap ℝ ℂ) x.im • I ∈ ℝ[I]
Module: Mathlib.Analysis.Complex.Basic

Goal state before:
pp: z : ℂ
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
𝕜 : Type u_2
inst✝ : RCLike 𝕜
h : RCLike.im RCLike.I = 1
x✝ : 𝕜
⊢ ‖{ toFun := (RCLike.complexRingEquiv h).toFun, map_add' := ⋯, map_smul' := ⋯,
          invFun := (RCLike.complexRingEquiv h).invFun, left_inv := ⋯, right_inv := ⋯ }
        x✝‖ =
    ‖x✝‖

Tactic:
rw [← sq_eq_sq₀ (by positivity) (by positivity), ← normSq_eq_norm_sq, ← RCLike.normSq_eq_def',
      RCLike.normSq_apply]

Goal state after:
z : ℂ
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
𝕜 : Type u_2
inst✝ : RCLike 𝕜
h : RCLike.im RCLike.I = 1
x✝ : 𝕜
⊢ normSq
      ({ toFun := (RCLike.complexRingEquiv h).toFun, map_add' := ⋯, map_smul' := ⋯,
          invFun := (RCLike.complexRingEquiv h).invFun, left_inv := ⋯, right_inv := ⋯ }
        x✝) =
    RCLike.re x✝ * RCLike.re x✝ + RCLike.im x✝ * RCLike.im x✝
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
m : ℕ
s : Bool
e : ℕ
⊢ re (ofScientific m s e) = ofScientific m s e

Tactic:
← ofReal_ofScientific,

Goal state after:
K : Type u_1
inst✝ : RCLike K
m : ℕ
s : Bool
e : ℕ
⊢ re ↑(ofScientific m s e) = ofScientific m s e
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
m : ℕ
s : Bool
e : ℕ
⊢ im (ofScientific m s e) = 0

Tactic:
← ofReal_ofScientific,

Goal state after:
K : Type u_1
inst✝ : RCLike K
m : ℕ
s : Bool
e : ℕ
⊢ im ↑(ofScientific m s e) = 0
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
x : K
⊢ re (↑‖x‖ ^ 2) = ‖↑‖x‖ ^ 2‖

Tactic:
← ofReal_pow

Goal state after:
K : Type u_1
inst✝ : RCLike K
x : K
⊢ re ↑(‖x‖ ^ 2) = ‖↑(‖x‖ ^ 2)‖
Module: Mathlib.Topology.OpenPartialHomeomorph.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
h : IsOpenEmbedding f
inst✝ : Nonempty X
x : X
⊢ ↑(toOpenPartialHomeomorph f h).symm (f x) = x

Tactic:
← congr_fun (h.toOpenPartialHomeomorph_apply f),

Goal state after:
X : Type u_1
Y : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
h : IsOpenEmbedding f
inst✝ : Nonempty X
x : X
⊢ ↑(toOpenPartialHomeomorph f h).symm (↑(toOpenPartialHomeomorph f h) x) = x
Module: Mathlib.Topology.OpenPartialHomeomorph.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
h : IsOpenEmbedding f
inst✝ : Nonempty X
x : Y
hx : x ∈ range f
⊢ f (↑(toOpenPartialHomeomorph f h).symm x) = x

Tactic:
← congr_fun (h.toOpenPartialHomeomorph_apply f),

Goal state after:
X : Type u_1
Y : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
h : IsOpenEmbedding f
inst✝ : Nonempty X
x : Y
hx : x ∈ range f
⊢ ↑(toOpenPartialHomeomorph f h) (↑(toOpenPartialHomeomorph f h).symm x) = x
Module: Mathlib.Analysis.RCLike.Basic

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

Tactic:
← sqrt_normSq_eq_norm,

Goal state after:
K : Type u_1
inst✝ : RCLike K
x : K
hx : 0 ≤ x
⊢ √(normSq x) ≤ re x
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
c₁ : ℝ
l : Filter α
f₁ f₂ : α → E
g₁ g₂ : α → F
hf : f₁ =ᶠ[l] f₂
hg : g₁ =ᶠ[l] g₂
a✝ : α
⊢ f₁ a✝ = f₂ a✝ → g₁ a✝ = g₂ a✝ → (‖f₁ a✝‖ ≤ c₁ * ‖g₁ a✝‖ ↔ ‖f₂ a✝‖ ≤ c₁ * ‖g₂ a✝‖)

Tactic:
e₁

Goal state after:
α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
c₁ : ℝ
l : Filter α
f₁ f₂ : α → E
g₁ g₂ : α → F
hf : f₁ =ᶠ[l] f₂
hg : g₁ =ᶠ[l] g₂
a✝ : α
e₁ : f₁ a✝ = f₂ a✝
⊢ g₁ a✝ = g₂ a✝ → (‖f₁ a✝‖ ≤ c₁ * ‖g₁ a✝‖ ↔ ‖f₂ a✝‖ ≤ c₁ * ‖g₂ a✝‖)
Module: Mathlib.Tactic.NormNum.NatFactorial

Goal state before:
pp: n l m a b : ℕ
h₁ : n.ascFactorial l = a
h₂ : (n + l).ascFactorial m = b
⊢ n.ascFactorial l * (n + l).ascFactorial m = n.ascFactorial (l + m)

Tactic:
apply ascFactorial_mul_ascFactorial

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

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
n : ℕ
⊢ lim ⟨fun n ↦ (↑(exp' ↑x) n).re, ⋯⟩ = (exp' ↑x).lim.re

Tactic:
← cauSeqRe,

Goal state after:
x : ℝ
hx : 0 ≤ x
n : ℕ
⊢ (cauSeqRe (exp' ↑x)).lim = (exp' ↑x).lim.re
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x y : ℂ
⊢ cos (x + y * I) = cos x * cosh y - sin x * sinh y * I

Tactic:
cos_add,

Goal state after:
x y : ℂ
⊢ cos x * cos (y * I) - sin x * sin (y * I) = cos x * cosh y - sin x * sinh y * I
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 - f₁ x‖ * (1 - c)⁻¹

Tactic:
← div_eq_mul_inv,

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‖ ≤ ‖f₂ x - f₁ x‖ / (1 - c)
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: case calc_2
x y : ℂ
⊢ cos ((x + y) / 2 + (x - y) / 2) + cos ((x + y) / 2 - (x - y) / 2) =
    cos ((x + y) / 2) * cos ((x - y) / 2) - sin ((x + y) / 2) * sin ((x - y) / 2) +
      (cos ((x + y) / 2) * cos ((x - y) / 2) + sin ((x + y) / 2) * sin ((x - y) / 2))

Tactic:
cos_add,

Goal state after:
case calc_2
x y : ℂ
⊢ cos ((x + y) / 2) * cos ((x - y) / 2) - sin ((x + y) / 2) * sin ((x - y) / 2) + cos ((x + y) / 2 - (x - y) / 2) =
    cos ((x + y) / 2) * cos ((x - y) / 2) - sin ((x + y) / 2) * sin ((x - y) / 2) +
      (cos ((x + y) / 2) * cos ((x - y) / 2) + sin ((x + y) / 2) * sin ((x - y) / 2))
Module: Mathlib.Analysis.Complex.Trigonometric

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

Tactic:
by rw [tan, sin_conj, cos_conj, ← map_div₀, tan]

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

Goal state before:
pp: x : ℂ
⊢ cos (x + x) = cos x ^ 2 - sin x ^ 2

Tactic:
cos_add,

Goal state after:
x : ℂ
⊢ cos x * cos x - sin x * sin x = cos x ^ 2 - sin x ^ 2
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ cos (3 * x) = 4 * cos x ^ 3 - 3 * cos x

Tactic:
by
  rw [← ofReal_inj]; simp [cos_three_mul]

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

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

Tactic:
rw [← nnnorm_norm, norm_exp_ofReal_mul_I, ← NNReal.coe_eq_one]; simp

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

Goal state before:
pp: x : ℝ
⊢ ‖cexp (I * ↑x) - 1‖ = ‖2 * Real.sin (x / 2)‖

Tactic:
by
  rw [show ‖2 * Real.sin (x / 2)‖ = ‖2 * sin (x / 2)‖ by norm_cast, two_sin]
  nth_rw 2 [← one_mul (_ - _), ← exp_zero]
  rw [← neg_add_cancel (x / 2 * I), exp_add, mul_assoc _ _ (_ - _), mul_sub, ← exp_add, ← exp_add,
    ← add_mul, ← add_mul]; norm_cast
  rw [add_neg_cancel, ofReal_zero, zero_mul, exp_zero, add_halves, ← neg_mul, Complex.norm_mul,
    norm_I, mul_one, Complex.norm_mul,
    show -(ofReal (x / 2)) = ofReal (-x / 2) by norm_cast; exact neg_div' 2 x,
    norm_exp_ofReal_mul_I, one_mul, ← norm_neg, neg_sub, mul_comm]

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

Goal state before:
pp: case inr
x : ℝ
hx : x ≠ 0
⊢ x + 1 ≤ rexp x

Tactic:
exact (add_one_lt_exp hx).le

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
E : Type u_3
inst✝¹ : Norm E
F : Type u_4
inst✝ : Norm F
e : OpenPartialHomeomorph α β
b : β
hb : b ∈ e.target
f : β → E
g : β → F
⊢ f =o[𝓝 b] g ↔ (f ∘ ↑e) =o[𝓝 (↑e.symm b)] (g ∘ ↑e)

Tactic:
simp only [IsLittleO_def]
  exact forall₂_congr fun c _hc => e.isBigOWith_congr hb

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

Goal state before:
pp: f : ℕ → ℝ
R : ℝ
A : Set.Ico 0 R ⊆ Set.Ioo (-R) R
⊢ [∃ 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:
have B : Ioo 0 R ⊆ Ioo (-R) R := Subset.trans Ioo_subset_Ico_self A

Goal state after:
f : ℕ → ℝ
R : ℝ
A : Set.Ico 0 R ⊆ Set.Ioo (-R) R
B : Set.Ioo 0 R ⊆ Set.Ioo (-R) R
⊢ [∃ 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.Algebra.Order.CauSeq.BigOperators

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

Tactic:
← div_eq_mul_inv,

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

Goal state before:
pp: ⊢ Subtype.val '' Set.range ⇑expOrderIso = Set.Ioi 0

Tactic:
expOrderIso.range_eq,

Goal state after:
⊢ Subtype.val '' Set.univ = Set.Ioi 0
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: ⊢ comap rexp (Filter.map rexp atTop) = Filter.map rexp atTop

Tactic:
comap_map exp_injective,

Goal state after:
⊢ atTop = Filter.map rexp atTop
Module: Mathlib.Analysis.Normed.Group.Pointwise

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
x y : E
⊢ {x} / closedBall y δ = closedBall (x / y) δ

Tactic:
simp_rw [div_eq_mul_inv, inv_closedBall, singleton_mul_closedBall]

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
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_of_pos ha.1

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.SpecificLimits.Normed

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

Tactic:
| base =>

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

Goal state before:
pp: x : ℝ
hx : x ∈ Ioo (-(π / 2)) (π / 2)
y : ℝ
hy : y ∈ Ioo (-(π / 2)) (π / 2)
hlt : x < y
⊢ y - x < π

Tactic:
by linarith [hx.1, hy.2]

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

Goal state before:
pp: ⊢ tan π = 0

Tactic:
tan_periodic.eq,

Goal state after:
⊢ tan 0 = 0
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
F : Set X
⊢ IsPathConnected F ↔ PathConnectedSpace ↑F

Tactic:
rw [pathConnectedSpace_iff_univ, IsInducing.subtypeVal.isPathConnected_iff, image_univ,
    Subtype.range_val_subtype, ofPred_mem_eq]

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

Goal state before:
pp: x : ℝ
this : {y | ↑y = ↑x} = {x}
⊢ ‖↑x‖ = |x|

Tactic:
simp [norm_eq_infDist, this]

Goal state after:
Module: Mathlib.Topology.Path

Goal state before:
pp: case pos
X✝ : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type u_3
γ✝ : Path x y
X : Type u_4
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ : ℝ
h₁ : t₀ ≤ ↑1
h₂ : ↑1 ≤ t₁
⊢ γ.extend ↑1 = γ.extend t₁

pp: case neg
X✝ : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type u_3
γ✝ : Path x y
X : Type u_4
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ : ℝ
h₁ : t₀ ≤ ↑1
h₂ : ¬↑1 ≤ t₁
⊢ γ.extend t₁ = γ.extend t₁

pp: case pos
X✝ : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type u_3
γ✝ : Path x y
X : Type u_4
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ : ℝ
h₁ : ¬t₀ ≤ ↑1
h₃ : t₀ ≤ t₁
⊢ γ.extend t₀ = γ.extend t₁

pp: case neg
X✝ : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type u_3
γ✝ : Path x y
X : Type u_4
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ : ℝ
h₁ : ¬t₀ ≤ ↑1
h₃ : ¬t₀ ≤ t₁
⊢ γ.extend t₁ = γ.extend t₁

Tactic:
· simp [γ.extend_of_one_le h₂]

Goal state after:
case neg
X✝ : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type u_3
γ✝ : Path x y
X : Type u_4
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ : ℝ
h₁ : t₀ ≤ ↑1
h₂ : ¬↑1 ≤ t₁
⊢ γ.extend t₁ = γ.extend t₁

case pos
X✝ : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type u_3
γ✝ : Path x y
X : Type u_4
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ : ℝ
h₁ : ¬t₀ ≤ ↑1
h₃ : t₀ ≤ t₁
⊢ γ.extend t₀ = γ.extend t₁

case neg
X✝ : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type u_3
γ✝ : Path x y
X : Type u_4
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ : ℝ
h₁ : ¬t₀ ≤ ↑1
h₃ : ¬t₀ ≤ t₁
⊢ γ.extend t₁ = γ.extend t₁
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: x y : ℂ
⊢ |x.arg - y.arg| < 2 * π

Tactic:
grind [arg_lt_arg_add_two_pi x y, arg_lt_arg_add_two_pi y x]

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

Goal state before:
pp: x y : ℝ
hx : 0 < x
hy : 0 < y
⊢ x < rexp (log y) ↔ x < y

Tactic:
exp_log hy

Goal state after:
x y : ℝ
hx : 0 < x
hy : 0 < y
⊢ x < y ↔ x < y
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: x y : ℝ
hy : 0 < y
⊢ rexp x ≤ rexp (log y) ↔ rexp x ≤ y

Tactic:
exp_log hy

Goal state after:
x y : ℝ
hy : 0 < y
⊢ rexp x ≤ y ↔ rexp x ≤ y
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: x y : ℝ
hy : 0 < y
⊢ rexp x < rexp (log y) ↔ rexp x < y

Tactic:
exp_log hy

Goal state after:
x y : ℝ
hy : 0 < y
⊢ rexp x < y ↔ rexp x < y
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: x : ℂ
hx : x ≠ 0
⊢ ↑‖x‖ * ↑(x.re / ‖x‖) + ↑‖x‖ * (↑(x.im / ‖x‖) * I) = x

Tactic:
ofReal_div,

Goal state after:
x : ℂ
hx : x ≠ 0
⊢ ↑‖x‖ * (↑x.re / ↑‖x‖) + ↑‖x‖ * (↑(x.im / ‖x‖) * I) = x
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: x : ℂ
hx : x ≠ 0
⊢ ↑‖x‖ * (↑x.re / ↑‖x‖) + ↑‖x‖ * (↑(x.im / ‖x‖) * I) = x

Tactic:
ofReal_div,

Goal state after:
x : ℂ
hx : x ≠ 0
⊢ ↑‖x‖ * (↑x.re / ↑‖x‖) + ↑‖x‖ * (↑x.im / ↑‖x‖ * I) = x
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: case mp.inl
x : ℝ
h : log x = 0
x_lt_zero : x < 0
⊢ -x = 1

Tactic:
← log_neg_eq_log x

Goal state after:
case mp.inl
x : ℝ
h : log (-x) = 0
x_lt_zero : x < 0
⊢ -x = 1
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: case convert_1
z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ ‖z‖ ≠ 0

Tactic:
lift z to ℝ using him
    simpa using hre.ne

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: z : ℂ
⊢ z.arg ≤ π / 2 ∧ z.arg ≠ π / 2 ↔ 0 < z.re ∨ z.im < 0 ∨ z = 0

Tactic:
arg_le_pi_div_two_iff,

Goal state after:
z : ℂ
⊢ (0 ≤ z.re ∨ z.im < 0) ∧ z.arg ≠ π / 2 ↔ 0 < z.re ∨ z.im < 0 ∨ z = 0
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: z : ℂ
⊢ -(π / 2) ≤ z.arg ∧ z.arg ≤ π / 2 ↔ 0 ≤ z.re

Tactic:
arg_le_pi_div_two_iff,

Goal state after:
z : ℂ
⊢ -(π / 2) ≤ z.arg ∧ (0 ≤ z.re ∨ z.im < 0) ↔ 0 ≤ z.re
Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex

Goal state before:
pp: x n : ℂ
⊢ x⁻¹ ^ n = if x.arg = π then (starRingEnd ℂ) (x ^ (starRingEnd ℂ) n)⁻¹ else (x ^ n)⁻¹

Tactic:
simp_rw [Complex.cpow_def, log_inv_eq_ite, inv_eq_zero, map_eq_zero, ite_mul, neg_mul,
    RCLike.conj_inv, apply_ite conj, apply_ite exp, apply_ite Inv.inv, map_zero, map_one, exp_neg,
    inv_one, inv_zero, ← exp_conj, map_mul, conj_conj]
  split_ifs with hx hn ha ha <;> rfl

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

Goal state before:
pp: ⊢ (↑π).toReal = π

Tactic:
rw [toReal_coe_eq_self_iff]

Goal state after:
⊢ -π < π ∧ π ≤ π
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : Angle
this✝ : 0 < π / 2
this : θ.toReal ∈ Set.Ioc (-π) π
⊢ 0 ≤ θ.cos ↔ |θ.toReal| ≤ π / 2

Tactic:
rw [← cos_toReal, ← cos_abs]

Goal state after:
θ : Angle
this✝ : 0 < π / 2
this : θ.toReal ∈ Set.Ioc (-π) π
⊢ 0 ≤ Real.cos |θ.toReal| ↔ |θ.toReal| ≤ π / 2
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: x : ℂ
n : ℤ
m : ℕ
⊢ ↑(x ^ Int.ofNat m).arg = Int.ofNat m • ↑x.arg

Tactic:
simp [arg_pow_coe_angle]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: x : ℂ
n : ℤ
m : ℕ
⊢ ↑(x ^ Int.negSucc m).arg = Int.negSucc m • ↑x.arg

Tactic:
simp [arg_pow_coe_angle]

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

Goal state before:
pp: case h.h
x✝¹ x✝ : ℝ
k : ℤ
h : x✝ = π * ↑k + 2⁻¹ * π - x✝¹
⊢ (↑x✝).tan = (↑x✝¹).tan⁻¹

Tactic:
inv_mul_eq_div,

Goal state after:
case h.h
x✝¹ x✝ : ℝ
k : ℤ
h : x✝ = π * ↑k + π / 2 - x✝¹
⊢ (↑x✝).tan = (↑x✝¹).tan⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case convert_3
z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ ‖z‖ ≠ 0

Tactic:
lift z to ℝ using him
    simpa using hre.ne

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

Goal state before:
pp: θ : Angle
h : θ.sign ≤ 0
⊢ -↑|θ.toReal| = θ

Tactic:
SignType.nonpos_iff

Goal state after:
θ : Angle
h : θ.sign = -1 ∨ θ.sign = 0
⊢ -↑|θ.toReal| = θ
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
⊢ Tendsto (fun x ↦ b ^ x) atTop (𝓝 0)

Tactic:
simp_rw [Real.rpow_def_of_nonpos hb.le, hb.ne, ite_false]

Goal state after:
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
⊢ Tendsto (fun x ↦ rexp (log b * x) * cos (x * π)) atTop (𝓝 0)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x a : ℝ
⊢ 0 ^ x = a ↔ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1

Tactic:
constructor
  · intro hyp
    simp only [rpow_def, Complex.ofReal_zero] at hyp
    by_cases h : x = 0
    · subst h
      simp only [Complex.one_re, Complex.ofReal_zero, Complex.cpow_zero] at hyp
      exact Or.inr ⟨rfl, hyp.symm⟩
    · rw [Complex.zero_cpow (Complex.ofReal_ne_zero.mpr h)] at hyp
      exact Or.inl ⟨h, hyp.symm⟩
  · rintro (⟨h, rfl⟩ | ⟨rfl, rfl⟩)
    · exact zero_rpow h
    · exact rpow_zero _

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℝ
⊢ 0 ^ x ≤ 1

Tactic:
by
  by_cases h : x = 0 <;> simp [h, zero_le_one]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℝ
⊢ 0 ≤ 0 ^ x

Tactic:
by
  by_cases h : x = 0 <;> simp [h, zero_le_one]

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

Goal state before:
pp: θ ψ : Angle
hθ : θ.sign = 1
hψ : ψ.sign = -1
⊢ (↑(θ.toReal + ψ.toReal)).toReal = θ.toReal + ψ.toReal

Tactic:
rw [toReal_coe_eq_self_iff]

Goal state after:
θ ψ : Angle
hθ : θ.sign = 1
hψ : ψ.sign = -1
⊢ -π < θ.toReal + ψ.toReal ∧ θ.toReal + ψ.toReal ≤ π
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ ψ : Angle
hθs : θ.toReal ∈ Set.Ioo 0 π
hψs : ψ.toReal ∈ Set.Ioo 0 π
hsa : (θ + ψ).sign ≠ 1
this : ↑(θ + ψ).toReal = ↑(θ.toReal + ψ.toReal)
⊢ |(θ + ψ).toReal| = 2 * π - (|θ.toReal| + |ψ.toReal|)

Tactic:
obtain ⟨k, hk⟩ := angle_eq_iff_two_pi_dvd_sub.mp this

Goal state after:
θ ψ : Angle
hθs : θ.toReal ∈ Set.Ioo 0 π
hψs : ψ.toReal ∈ Set.Ioo 0 π
hsa : (θ + ψ).sign ≠ 1
this : ↑(θ + ψ).toReal = ↑(θ.toReal + ψ.toReal)
k : ℤ
hk : (θ + ψ).toReal - (θ.toReal + ψ.toReal) = 2 * π * ↑k
⊢ |(θ + ψ).toReal| = 2 * π - (|θ.toReal| + |ψ.toReal|)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case inl
z w : ℂ
h : z = 0 → w.re = 0 → w = 0
hz : z ≠ 0
⊢ ‖z ^ w‖ = ‖z‖ ^ w.re / rexp (z.arg * w.im)

Tactic:
exact norm_cpow_of_ne_zero hz w

Goal state after: