mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: case inr.right
E : Type u_5
inst✝⁶ : Ring E
inst✝⁵ : LinearOrder E
inst✝⁴ : IsOrderedRing E
inst✝³ : UniformSpace E
inst✝² : IsUniformAddGroup E
inst✝¹ : CompleteSpace E
inst✝ : OrderClosedTopology E
f : ℕ → E
hfa : Antitone f
hfs : Summable f
h✝ : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 (∑' (i : ℕ), (-1) ^ i * f i))
I : ∀ (n : ℕ), 0 ≤ f n
n : ℕ
lower : ∑' (i : ℕ), (-1) ^ i * f i ≤ ∑ i ∈ Finset.range (2 * n + 1), (-1) ^ i * f i
upper : ∑ x ∈ Finset.range (2 * n + 1), (-1) ^ x * f x + (-1) ^ (2 * n + 1) * f (2 * n + 1) ≤ ∑' (i : ℕ), (-1) ^ i * f i
h : Odd (2 * n + 1)
⊢ ∑ i ∈ Finset.range (2 * n + 1), (-1) ^ i * f i - ∑' (i : ℕ), (-1) ^ i * f i ≤ f (2 * n + 1)

Tactic:
simpa using

Goal state after:
case inr.right
E : Type u_5
inst✝⁶ : Ring E
inst✝⁵ : LinearOrder E
inst✝⁴ : IsOrderedRing E
inst✝³ : UniformSpace E
inst✝² : IsUniformAddGroup E
inst✝¹ : CompleteSpace E
inst✝ : OrderClosedTopology E
f : ℕ → E
hfa : Antitone f
hfs : Summable f
h✝ : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 (∑' (i : ℕ), (-1) ^ i * f i))
I : ∀ (n : ℕ), 0 ≤ f n
n : ℕ
lower : ∑' (i : ℕ), (-1) ^ i * f i ≤ ∑ i ∈ Finset.range (2 * n + 1), (-1) ^ i * f i
upper : ∑ x ∈ Finset.range (2 * n + 1), (-1) ^ x * f x + (-1) ^ (2 * n + 1) * f (2 * n + 1) ≤ ∑' (i : ℕ), (-1) ^ i * f i
h : Odd (2 * n + 1)
⊢ ∑ x ∈ Finset.range (1 + 2 * n), (-1) ^ x * f x ≤ f (1 + 2 * n) + ∑' (x : ℕ), (-1) ^ x * f x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: x✝ y x : ℝ
hx : x ∈ Icc (-(π / 2)) (π / 2)
⊢ sin x ∈ Icc (-1) 1

Tactic:
simpa using

Goal state after:
x✝ y x : ℝ
hx : x ∈ Icc (-(π / 2)) (π / 2)
⊢ |sin x| ≤ 1
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: ⊢ arcsin '' Icc (-1) 1 = Icc (-(π / 2)) (π / 2)

Tactic:
simpa using

Goal state after:
⊢ arcsin '' Icc (-1) 1 = Icc (-(π / 2)) (π / 2)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: x✝ y x : ℝ
hx : x ∈ Icc 0 π
⊢ cos x ∈ Icc (-1) 1

Tactic:
simpa using

Goal state after:
x✝ y x : ℝ
hx : x ∈ Icc 0 π
⊢ |cos x| ≤ 1
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: ⊢ arccos '' Icc (-1) 1 = Icc 0 π

Tactic:
simpa using

Goal state after:
⊢ arccos '' Icc (-1) 1 = Icc 0 π
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: case inl
α : Type u_1
R : Type u_4
K : Type u_5
inst✝⁵ : NormedRing K
inst✝⁴ : IsDomain K
inst✝³ : NormedAddCommGroup R
inst✝² : Module K R
inst✝¹ : IsTorsionFree K R
inst✝ : NormSMulClass K R
f : α → K
g : α → R
l : Filter α
hmul : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun x ↦ ‖f x • g x‖
hf : Tendsto f l (cobounded K)
ε : ℝ
hε0 : 0 < ε
x : α
hf0 : f x ≠ 0
hc : ∀ᶠ (x : α) in l, ‖f x • g x‖ ≤ 0
hfgc : ‖f x • g x‖ ≤ 0
hεf : 0 / ε ≤ ‖f x‖
⊢ g x ∈ closedBall 0 ε

Tactic:
simpa using

Goal state after:
case inl
α : Type u_1
R : Type u_4
K : Type u_5
inst✝⁵ : NormedRing K
inst✝⁴ : IsDomain K
inst✝³ : NormedAddCommGroup R
inst✝² : Module K R
inst✝¹ : IsTorsionFree K R
inst✝ : NormSMulClass K R
f : α → K
g : α → R
l : Filter α
hmul : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun x ↦ ‖f x • g x‖
hf : Tendsto f l (cobounded K)
ε : ℝ
hε0 : 0 < ε
x : α
hf0 : f x ≠ 0
hc : ∀ᶠ (x : α) in l, ‖f x • g x‖ ≤ 0
hfgc : ‖f x • g x‖ ≤ 0
hεf : 0 / ε ≤ ‖f x‖
⊢ 0 ≤ ε
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: z : ℂ
⊢ toIocMod Real.two_pi_pos (-π) z.arg = z.arg

Tactic:
simpa using

Goal state after:
z : ℂ
⊢ -π < z.arg ∧ z.arg ≤ π
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: case hf
α : Type u_1
R : Type u_4
K : Type u_5
inst✝⁵ : NormedRing K
inst✝⁴ : IsDomain K
inst✝³ : NormedAddCommGroup R
inst✝² : Module K R
inst✝¹ : IsTorsionFree K R
inst✝ : NormSMulClass K R
f₁ f₂ : α → K
g : α → R
t : R
l : Filter α
hmul : Tendsto (fun x ↦ f₁ x • g x) l (𝓝 t)
hf₁ : Tendsto f₁ l (cobounded K)
hbdd : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun x ↦ ‖f₁ x - f₂ x‖
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun x ↦ (norm ∘ fun x ↦ ‖f₁ x - f₂ x‖) x

Tactic:
simpa using

Goal state after:
case hf
α : Type u_1
R : Type u_4
K : Type u_5
inst✝⁵ : NormedRing K
inst✝⁴ : IsDomain K
inst✝³ : NormedAddCommGroup R
inst✝² : Module K R
inst✝¹ : IsTorsionFree K R
inst✝ : NormSMulClass K R
f₁ f₂ : α → K
g : α → R
t : R
l : Filter α
hmul : Tendsto (fun x ↦ f₁ x • g x) l (𝓝 t)
hf₁ : Tendsto f₁ l (cobounded K)
hbdd : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun x ↦ ‖f₁ x - f₂ x‖
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun x ↦ ‖f₁ x - f₂ x‖
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: R : Type u_4
K : Type u_5
inst✝¹⁰ : NormedRing K
inst✝⁹ : IsDomain K
inst✝⁸ : NormedAddCommGroup R
inst✝⁷ : Module K R
inst✝⁶ : IsTorsionFree K R
inst✝⁵ : NormSMulClass K R
inst✝⁴ : NormSMulClass ℤ K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : FloorSemiring K
inst✝ : HasSolidNorm K
g : ℕ → R
t : R
hg : Tendsto (fun n ↦ ↑n • g n) atTop (𝓝 t)
⊢ ∀ᶠ (x : K) in atTop, |↑⌊x⌋₊ - x| ≤ |1|

Tactic:
simpa using

Goal state after:
R : Type u_4
K : Type u_5
inst✝¹⁰ : NormedRing K
inst✝⁹ : IsDomain K
inst✝⁸ : NormedAddCommGroup R
inst✝⁷ : Module K R
inst✝⁶ : IsTorsionFree K R
inst✝⁵ : NormSMulClass K R
inst✝⁴ : NormSMulClass ℤ K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : FloorSemiring K
inst✝ : HasSolidNorm K
g : ℕ → R
t : R
hg : Tendsto (fun n ↦ ↑n • g n) atTop (𝓝 t)
⊢ ∃ a, ∀ (b : K), a ≤ b → |↑⌊b⌋₊ - b| ≤ 1
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: R : Type u_4
K : Type u_5
inst✝⁹ : NormedRing K
inst✝⁸ : NormedRing R
inst✝⁷ : Module K R
inst✝⁶ : IsTorsionFree K R
inst✝⁵ : NormSMulClass K R
inst✝⁴ : NormSMulClass ℤ K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : FloorSemiring K
inst✝ : HasSolidNorm K
g : ℕ → R
t : R
hg : Tendsto (fun n ↦ ↑n * g n) atTop (𝓝 t)
⊢ Tendsto (fun n ↦ n • g n) atTop (𝓝 t)

Tactic:
simpa using

Goal state after:
R : Type u_4
K : Type u_5
inst✝⁹ : NormedRing K
inst✝⁸ : NormedRing R
inst✝⁷ : Module K R
inst✝⁶ : IsTorsionFree K R
inst✝⁵ : NormSMulClass K R
inst✝⁴ : NormSMulClass ℤ K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : FloorSemiring K
inst✝ : HasSolidNorm K
g : ℕ → R
t : R
hg : Tendsto (fun n ↦ ↑n * g n) atTop (𝓝 t)
⊢ Tendsto (fun n ↦ ↑n * g n) atTop (𝓝 t)
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: x : ℝ
⊢ log x ≠ 0 ↔ x ≠ 0 ∧ x ≠ 1 ∧ x ≠ -1

Tactic:
simpa using

Goal state after:
x : ℝ
⊢ log x ≠ 0 ↔ x ≠ 0 ∧ x ≠ 1 ∧ x ≠ -1
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: x : ℝ
hx : 0 < x
⊢ 1 - x⁻¹ ≤ log x

Tactic:
simpa using

Goal state after:
x : ℝ
hx : 0 < x
⊢ 1 ≤ x⁻¹ + log x
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: x : ℝ
h1 : 0 < x
h2 : x ≤ 1
⊢ 0 < 1 / x

Tactic:
simpa using

Goal state after:
x : ℝ
h1 : 0 < x
h2 : x ≤ 1
⊢ 0 < x
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: ⊢ Tendsto log (𝓝[≠] 0) atBot

Tactic:
simpa using

Goal state after:
⊢ Tendsto log (𝓝[≠] 0) atBot
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: ψ θ : Angle
this : Int.natAbs 2 = 2
⊢ ψ = θ ∨ ψ = θ + ↑(2 * π / 2) ↔ ψ = θ ∨ ψ = θ + ↑π

Tactic:
mul_div_cancel_left₀ (_ : ℝ) two_ne_zero

Goal state after:
ψ θ : Angle
this : Int.natAbs 2 = 2
⊢ ψ = θ ∨ ψ = θ + ↑π ↔ ψ = θ ∨ ψ = θ + ↑π
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: x : ℂ
h : cexp x = 1
n : ℤ
hn : x.im + n • (2 * π) ∈ Ioc (-π) (-π + 2 * π)
⊢ (x + ↑n * (2 * ↑π * I)).im ∈ Ioc (-π) π

Tactic:
simpa using

Goal state after:
x : ℂ
h : cexp x = 1
n : ℤ
hn : x.im + n • (2 * π) ∈ Ioc (-π) (-π + 2 * π)
⊢ -π < x.im + (↑n * π + ↑n * π) ∧ x.im + (↑n * π + ↑n * π) ≤ π
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : Angle
⊢ θ = -θ ↔ θ = 0 ∨ θ = ↑π

Tactic:
by
  rw [← add_eq_zero_iff_eq_neg, ← two_nsmul, two_nsmul_eq_zero_iff]

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

Goal state before:
pp: x : ℂ
hx : 0 ≤ x.im
x✝ : ∃ n, x = ↑n * (2 * ↑π * I)
n : ℤ
hn : x = ↑n * (2 * ↑π * I)
⊢ 0 ≤ ↑n * (2 * π)

Tactic:
simpa using

Goal state after:
x : ℂ
hx : 0 ≤ x.im
x✝ : ∃ n, x = ↑n * (2 * ↑π * I)
n : ℤ
hn : x = ↑n * (2 * ↑π * I)
⊢ 0 ≤ ↑n * (2 * π)
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: n : ℕ
⊢ Tendsto (fun x ↦ log x ^ n / id x) atTop (𝓝 0)

Tactic:
simpa using

Goal state after:
n : ℕ
⊢ Tendsto (fun x ↦ log x ^ n / x) atTop (𝓝 0)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: case convert_1
z : ℝ
hre : (↑z).re < 0
⊢ ‖↑z‖ ≠ 0

Tactic:
simpa using

Goal state after:
case convert_1
z : ℝ
hre : (↑z).re < 0
⊢ ¬z = 0
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ Tendsto log (𝓝[{z | 0 ≤ z.im}] z) (𝓝 (↑(Real.log ‖z‖) + ↑π * I))

Tactic:
simpa using

Goal state after:
z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ Tendsto log (𝓝[{z | 0 ≤ z.im}] z) (𝓝 (↑(Real.log ‖z‖) + ↑π * I))
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: x y : ℝ
h₁ : -π < y
h₂ : y < π
⊢ y ≤ -π + 2 * π

Tactic:
simpa using

Goal state after:
x y : ℝ
h₁ : -π < y
h₂ : y < π
⊢ y ≤ π
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: e : ℝ
n : ℕ
h : NormNum.IsNat e n
w : Nat.blt 1 n = true
⊢ 1 < ↑n

Tactic:
simpa using

Goal state after:
e : ℝ
n : ℕ
h : NormNum.IsNat e n
w : Nat.blt 1 n = true
⊢ 1 < n
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: e : ℝ
n : ℕ
h : NormNum.IsInt e (Int.negOfNat n)
w : Nat.blt 1 n = true
⊢ 1 < ↑n

Tactic:
simpa using

Goal state after:
e : ℝ
n : ℕ
h : NormNum.IsInt e (Int.negOfNat n)
w : Nat.blt 1 n = true
⊢ 1 < n
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: e : ℝ
d n : ℕ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (1 < ↑n / ↑d) = true
⊢ 1 < ↑n / ↑d

Tactic:
simpa using

Goal state after:
e : ℝ
d n : ℕ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (1 < ↑n / ↑d) = true
⊢ 1 < ↑n / ↑d
Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex

Goal state before:
pp: x : ℂ
⊢ x ^ (-1) = x⁻¹

Tactic:
simpa using

Goal state after:
x : ℂ
⊢ x ^ (-1) = x⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex

Goal state before:
pp: x : ℂ
n : ℕ
⊢ x ^ ↑n = x ^ n

Tactic:
simpa using

Goal state after:
x : ℂ
n : ℕ
⊢ x ^ ↑n = x ^ n
Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex

Goal state before:
pp: x : ℂ
n : ℤ
⊢ x ^ ↑n = x ^ n

Tactic:
simpa using

Goal state after:
x : ℂ
n : ℤ
⊢ x ^ ↑n = x ^ n
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: e : ℝ
d n : ℕ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h₁ : decide (0 < ↑n / ↑d) = true
h₂ : decide (↑n / ↑d < 1) = true
⊢ 0 < ↑n / ↑d

Tactic:
simpa using

Goal state after:
e : ℝ
d n : ℕ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h₁ : decide (0 < ↑n / ↑d) = true
h₂ : decide (↑n / ↑d < 1) = true
⊢ 0 < ↑n / ↑d
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: e : ℝ
d n : ℕ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h₁ : decide (0 < ↑n / ↑d) = true
h₂ : decide (↑n / ↑d < 1) = true
h₁' : 0 < ↑n / ↑d
⊢ ↑n / ↑d < 1

Tactic:
simpa using

Goal state after:
e : ℝ
d n : ℕ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h₁ : decide (0 < ↑n / ↑d) = true
h₂ : decide (↑n / ↑d < 1) = true
h₁' : 0 < ↑n / ↑d
⊢ ↑n / ↑d < 1
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: x✝ : ℂ
⊢ x✝ ∈ (fun θ ↦ cexp (↑θ * I)) '' Ioc (-π) π ↔ x✝ ∈ sphere 0 1

Tactic:
simpa using

Goal state after:
x✝ : ℂ
⊢ (∃ x, (-π < x ∧ x ≤ π) ∧ cexp (↑x * I) = x✝) ↔ ‖x✝‖ = 1
Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex

Goal state before:
pp: a : ℝ
ha : 0 ≤ a
r : ℂ
⊢ (↑a).arg ≠ π

Tactic:
simpa using

Goal state after:
a : ℝ
ha : 0 ≤ a
r : ℂ
⊢ ¬0 = π
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case h.h
x✝¹ x✝ : ℝ
h : (↑x✝¹).toReal = (↑x✝).toReal
⊢ ↑x✝¹ = ↑x✝

Tactic:
simpa using

Goal state after:
case h.h
x✝¹ x✝ : ℝ
h : (↑x✝¹).toReal = (↑x✝).toReal
⊢ ↑x✝¹ = ↑x✝
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: z : ℂ
θ : Real.Angle
⊢ (↑z.arg).toReal = θ.toReal ↔ z.arg = θ.toReal

Tactic:
arg_coe_angle_toReal_eq_arg

Goal state after:
z : ℂ
θ : Real.Angle
⊢ z.arg = θ.toReal ↔ z.arg = θ.toReal
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: x y : ℂ
⊢ (↑x.arg).toReal = (↑y.arg).toReal ↔ x.arg = y.arg

Tactic:
arg_coe_angle_toReal_eq_arg

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

Goal state before:
pp: case convert_3
z : ℝ
hre : (↑z).re < 0
⊢ ‖↑z‖ ≠ 0

Tactic:
simpa using

Goal state after:
case convert_3
z : ℝ
hre : (↑z).re < 0
⊢ ¬z = 0
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case refine_1
z : ℝ
hre : (↑z).re < 0
this : arg =ᶠ[𝓝[{z | 0 ≤ z.im}] ↑z] fun x ↦ Real.arcsin ((-x).im / ‖x‖) + π
⊢ ‖↑z‖ ≠ 0

Tactic:
simpa using

Goal state after:
case refine_1
z : ℝ
hre : (↑z).re < 0
this : arg =ᶠ[𝓝[{z | 0 ≤ z.im}] ↑z] fun x ↦ Real.arcsin ((-x).im / ‖x‖) + π
⊢ ¬z = 0
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ Tendsto arg (𝓝[{z | 0 ≤ z.im}] z) (𝓝 π)

Tactic:
simpa using

Goal state after:
z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ Tendsto arg (𝓝[{z | 0 ≤ z.im}] z) (𝓝 π)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ ψ : Angle
h : θ.sign = ψ.sign
⊢ θ = ψ ↔ |θ.toReal| = |ψ.toReal|

Tactic:
simpa using

Goal state after:
θ ψ : Angle
h : θ.sign = ψ.sign
⊢ θ = ψ ↔ |θ.toReal| = |ψ.toReal|
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : Angle
⊢ (2 • θ).sign = -θ.sign ↔ θ = 0 ∨ π / 2 < |θ.toReal|

Tactic:
simpa using

Goal state after:
θ : Angle
⊢ (2 • θ).sign = -θ.sign ↔ θ = 0 ∨ θ.cos < 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: y : ℝ
hy : 0 < y
b : ℝ
hb : 0 ≤ b
x : ℝ
hx₀ : 0 ≤ x
hx : b ^ (1 / y) ≤ x
⊢ x ^ y ∈ Set.Ici b

Tactic:
simpa using

Goal state after:
y : ℝ
hy : 0 < y
b : ℝ
hb : 0 ≤ b
x : ℝ
hx₀ : 0 ≤ x
hx : b ^ (1 / y) ≤ x
⊢ b ≤ x ^ y
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℝ
n : ℕ
⊢ x ^ ↑n = x ^ n

Tactic:
simpa using

Goal state after:
x : ℝ
n : ℕ
⊢ x ^ ↑n = x ^ n
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

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

Tactic:
refine tendsto_exp_atBot.comp <| (tendsto_const_mul_atBot_of_neg ?_).mpr tendsto_id

Goal state after:
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
⊢ log b < 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

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

Tactic:
refine tendsto_exp_atBot.comp <| (tendsto_const_mul_atBot_of_neg ?_).mpr tendsto_id

Goal state after:
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : 0 < b
⊢ log b < 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y : ℝ
hx_nonneg : 0 ≤ x
⊢ |x ^ y| = |x| ^ y

Tactic:
by
  have h_rpow_nonneg : 0 ≤ x ^ y := Real.rpow_nonneg hx_nonneg _
  rw [abs_eq_self.mpr hx_nonneg, abs_eq_self.mpr h_rpow_nonneg]

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

Goal state before:
pp: a b c : ℝ
hb : 0 ≠ b
⊢ Tendsto ?m.40 atTop (𝓝 0)

Tactic:
simpa using

Goal state after:
a b c : ℝ
hb : 0 ≠ b
⊢ Tendsto ?m.40 atTop (𝓝 0)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

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

Tactic:
simpa using

Goal state after:
θ ψ : Angle
hθ : θ.sign = 1
hψ : ψ.sign = -1
this : (↑(θ.toReal + ψ.toReal)).toReal = θ.toReal + ψ.toReal
⊢ (θ + ψ).toReal = θ.toReal + ψ.toReal
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: case hdb
s : ℝ
n : ℕ
hn : s < ↑n
x : ℝ
hx₀ : 0 < x
hx₁ : 1 ≤ x
⊢ x ^ s ≤ x ^ n

Tactic:
simpa using

Goal state after:
case hdb
s : ℝ
n : ℕ
hn : s < ↑n
x : ℝ
hx₀ : 0 < x
hx₁ : 1 ≤ x
⊢ x ^ s ≤ x ^ n
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case cons
ι : Type u_1
a : ℝ
ha : 0 ≤ a
f : ι → ℝ
i : ι
s : Finset ι
hi : i ∉ s
ihs : (∀ x ∈ s, 0 ≤ f x) → a ^ ∑ x ∈ s, f x = ∏ x ∈ s, a ^ f x
h : ∀ x ∈ cons i s hi, 0 ≤ f x
⊢ a ^ ∑ x ∈ cons i s hi, f x = ∏ x ∈ cons i s hi, a ^ f x

Tactic:
forall_mem_cons

Goal state after:
case cons
ι : Type u_1
a : ℝ
ha : 0 ≤ a
f : ι → ℝ
i : ι
s : Finset ι
hi : i ∉ s
ihs : (∀ x ∈ s, 0 ≤ f x) → a ^ ∑ x ∈ s, f x = ∏ x ∈ s, a ^ f x
h : 0 ≤ f i ∧ ∀ x ∈ s, 0 ≤ f x
⊢ a ^ ∑ x ∈ cons i s hi, f x = ∏ x ∈ cons i s hi, a ^ f x
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y : ℝ
⊢ x ^ (-y) = x⁻¹ ^ y

Tactic:
by
  simp [rpow_def, Complex.cpow_neg, Complex.inv_cpow_eq_ite, apply_ite]

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

Goal state before:
pp: α : Type u_1
l : Filter α
f : α → ℂ
b : ℂ
hl : b.re = 0 → b ≠ 0 → ∀ᶠ (x : α) in l, f x ≠ 0
⊢ ∀ᶠ (x : α) in l, f x = 0 → b.re = 0 → b = 0

Tactic:
simpa using

Goal state after:
α : Type u_1
l : Filter α
f : α → ℂ
b : ℂ
hl : b.re = 0 → b ≠ 0 → ∀ᶠ (x : α) in l, f x ≠ 0
⊢ (∃ᶠ (x : α) in l, f x = 0) → b.re = 0 → b = 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: α : Type u_1
r c : ℝ
l : Filter α
f g : α → ℝ
h : IsBigOWith c l f g
hc : 0 ≤ c
hr : 0 ≤ r
hg : 0 ≤ᶠ[l] g
x : α
hgx : 0 x ≤ g x
hx : ‖f x‖ ≤ c * ‖g x‖
⊢ |f x| ^ r ≤ (c * |g x|) ^ r

Tactic:
by gcongr; assumption

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

Goal state before:
pp: α : Type u_1
l : Filter α
f g : α → ℝ
hfg : f =O[l] g
hg : 0 ≤ᶠ[l] g
⊢ (fun x ↦ √(f x)) =O[l] fun x ↦ √(g x)

Tactic:
simpa using

Goal state after:
α : Type u_1
l : Filter α
f g : α → ℝ
hfg : f =O[l] g
hg : 0 ≤ᶠ[l] g
⊢ (fun x ↦ f x ^ 2⁻¹) =O[l] fun x ↦ g x ^ 2⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: α : Type u_1
l : Filter α
f g : α → ℝ
hfg : f =o[l] g
hg : 0 ≤ᶠ[l] g
⊢ (fun x ↦ √(f x)) =o[l] fun x ↦ √(g x)

Tactic:
simpa using

Goal state after:
α : Type u_1
l : Filter α
f g : α → ℝ
hfg : f =o[l] g
hg : 0 ≤ᶠ[l] g
⊢ (fun x ↦ f x ^ 2⁻¹) =o[l] fun x ↦ g x ^ 2⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: a b : ℝ
h : a ≤ b
himp : b = 0 → a = 0
x : ℝ
hx : x ∈ Set.Icc 0 1
⊢ x ∈ {x | (fun x ↦ ‖x ^ b‖ ≤ ‖x ^ a‖) x}

Tactic:
simpa using

Goal state after:
a b : ℝ
h : a ≤ b
himp : b = 0 → a = 0
x : ℝ
hx : x ∈ Set.Icc 0 1
⊢ x ^ b ≤ x ^ a
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: s b : ℝ
hb : 0 < b
⊢ Tendsto (fun x ↦ x ^ s / rexp (b * x)) atTop (𝓝 0)

Tactic:
simpa using

Goal state after:
s b : ℝ
hb : 0 < b
⊢ Tendsto (fun x ↦ x ^ s * (rexp (b * x))⁻¹) atTop (𝓝 0)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: k : ℤ
b : ℝ
hb : 0 < b
⊢ (fun x ↦ x ^ k) =o[atTop] fun x ↦ rexp (b * x)

Tactic:
simpa using

Goal state after:
k : ℤ
b : ℝ
hb : 0 < b
⊢ (fun x ↦ x ^ k) =o[atTop] fun x ↦ rexp (b * x)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: k : ℕ
b : ℝ
hb : 0 < b
⊢ (fun x ↦ x ^ k) =o[atTop] fun x ↦ rexp (b * x)

Tactic:
simpa using

Goal state after:
k : ℕ
b : ℝ
hb : 0 < b
⊢ (fun x ↦ x ^ k) =o[atTop] fun x ↦ rexp (b * x)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

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

Tactic:
simpa using

Goal state after:
s : ℝ
⊢ (fun x ↦ x ^ s) =o[atTop] rexp
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℝ
hx : 0 < x
y : ℂ
⊢ ‖↑x ^ y‖ = x ^ y.re

Tactic:
rw [norm_cpow_of_ne_zero (ofReal_ne_zero.mpr hx.ne'), arg_ofReal_of_nonneg hx.le,
    zero_mul, Real.exp_zero, div_one, Complex.norm_of_nonneg hx.le]

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

Goal state before:
pp: x : ℝ
hx : x ≠ 0
y : ℝ
n : ℕ
⊢ x ^ (y + ↑n) = x ^ y * x ^ n

Tactic:
simpa using

Goal state after:
x : ℝ
hx : x ≠ 0
y : ℝ
n : ℕ
⊢ x ^ (y + ↑n) = x ^ y * x ^ n
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℝ
hx : x ≠ 0
y : ℝ
n : ℕ
⊢ x ^ (y - ↑n) = x ^ y / x ^ n

Tactic:
simpa using

Goal state after:
x : ℝ
hx : x ≠ 0
y : ℝ
n : ℕ
⊢ x ^ (y - ↑n) = x ^ y / x ^ n
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℝ
hx : x ≠ 0
y : ℝ
⊢ x ^ (y + 1) = x ^ y * x

Tactic:
simpa using

Goal state after:
x : ℝ
hx : x ≠ 0
y : ℝ
⊢ x ^ (y + 1) = x ^ y * x
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℝ
hx : x ≠ 0
y : ℝ
⊢ x ^ (y - 1) = x ^ y / x

Tactic:
simpa using

Goal state after:
x : ℝ
hx : x ≠ 0
y : ℝ
⊢ x ^ (y - 1) = x ^ y / x
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: x : ℝ≥0
n : ℕ
⊢ ↑(x ^ ↑n) = ↑(x ^ n)

Tactic:
simpa using

Goal state after:
x : ℝ≥0
n : ℕ
⊢ ↑x ^ ↑n = ↑x ^ n
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y z : ℝ
hxy : x < y
hz : 0 < z
hx : 0 = x
⊢ 0 < y

Tactic:
by rwa [← hx] at hxy

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

Goal state before:
pp: x : ℝ≥0
hx : x ≠ 0
y : ℝ
⊢ x ^ (y + 1) = x ^ y * x

Tactic:
simpa using

Goal state after:
x : ℝ≥0
hx : x ≠ 0
y : ℝ
⊢ x ^ (y + 1) = x ^ y * x
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: x : ℝ≥0
hx : x ≠ 0
y : ℝ
⊢ x ^ (y - 1) = x ^ y / x

Tactic:
simpa using

Goal state after:
x : ℝ≥0
hx : x ≠ 0
y : ℝ
⊢ x ^ (y - 1) = x ^ y / x
Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity

Goal state before:
pp: p : ℂ × ℂ
hp_fst : p.1 ∈ slitPlane
⊢ ContinuousAt (fun x ↦ cexp (Complex.log x.1 * x.2)) p

Tactic:
refine continuous_exp.continuousAt.comp ?_

Goal state after:
p : ℂ × ℂ
hp_fst : p.1 ∈ slitPlane
⊢ ContinuousAt (fun x ↦ Complex.log x.1 * x.2) p
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: ι : Type u_1
l : List ι
f : ι → ℝ
hl : ∀ i ∈ l, 0 ≤ f i
r : ℝ
⊢ ∀ x ∈ List.map f l, 0 ≤ x

Tactic:
simpa using

Goal state after:
ι : Type u_1
l : List ι
f : ι → ℝ
hl : ∀ i ∈ l, 0 ≤ f i
r : ℝ
⊢ ∀ a ∈ l, 0 ≤ f a
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case mk
ι : Type u_1
s : Multiset ι
f : ι → ℝ
r : ℝ
l : List ι
hs : ∀ i ∈ Quot.mk (⇑(List.isSetoid ι)) l, 0 ≤ f i
⊢ (Multiset.map (fun x ↦ f x ^ r) (Quot.mk (⇑(List.isSetoid ι)) l)).prod =
    (Multiset.map f (Quot.mk (⇑(List.isSetoid ι)) l)).prod ^ r

Tactic:
simpa using

Goal state after:
case mk
ι : Type u_1
s : Multiset ι
f : ι → ℝ
r : ℝ
l : List ι
hs : ∀ i ∈ Quot.mk (⇑(List.isSetoid ι)) l, 0 ≤ f i
⊢ (List.map (fun x ↦ f x ^ r) l).prod = (List.map f l).prod ^ r
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: x y : ℝ≥0
z : ℝ
hz : 0 < z
⊢ x ^ z ≤ (y ^ z⁻¹) ^ z ↔ x ^ z ≤ y

Tactic:
← one_div,

Goal state after:
x y : ℝ≥0
z : ℝ
hz : 0 < z
⊢ x ^ z ≤ (y ^ (1 / z)) ^ z ↔ x ^ z ≤ y
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: x y : ℝ≥0
z : ℝ
hz : 0 < z
⊢ (x ^ z⁻¹) ^ z ≤ y ^ z ↔ x ≤ y ^ z

Tactic:
← one_div,

Goal state after:
x y : ℝ≥0
z : ℝ
hz : 0 < z
⊢ (x ^ (1 / z)) ^ z ≤ y ^ z ↔ x ≤ y ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: x : ℝ
hx : x ≠ 0
y z : ℝ≥0
hyz : (fun y ↦ y ^ x) y = (fun y ↦ y ^ x) z
⊢ y = z

Tactic:
simpa using

Goal state after:
x : ℝ
hx : x ≠ 0
y z : ℝ≥0
hyz : (fun y ↦ y ^ x) y = (fun y ↦ y ^ x) z
⊢ y = z
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case inr.inr
x : ℝ≥0
y z : ℝ
hx₀ : x ≠ 0
hx₁ : x ≠ 1
⊢ x ^ y = x ^ z ↔ y = z ∨ x = 1 ∨ x = 0 ∧ (y = 0 ↔ z = 0)

Tactic:
simpa using

Goal state after:
case inr.inr
x : ℝ≥0
y z : ℝ
hx₀ : x ≠ 0
hx₁ : x ≠ 1
⊢ x ^ y = x ^ z ↔ y = z
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

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

Tactic:
simpa using

Goal state after:
x : ℝ≥0
y : ℝ
⊢ x ^ y = x ↔ x = 1 ∨ y = 1 ∨ x = 0 ∧ ¬y = 0