mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case neg
r : ℝ
hr : 0 < r
θ : ℝ
hθ : θ ∈ Ioc (-π) π
h₁ : θ < -(π / 2) ∨ π / 2 < θ
⊢ (if 0 ≤ Real.cos θ then Real.arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then Real.arcsin (-Real.sin θ) + π else Real.arcsin (-Real.sin θ) - π) =
    θ

Tactic:
]

Goal state after:
case neg
r : ℝ
hr : 0 < r
θ : ℝ
hθ : θ ∈ Ioc (-π) π
h₁ : θ < -(π / 2) ∨ π / 2 < θ
⊢ (if 0 ≤ Real.cos θ then Real.arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then Real.arcsin (-Real.sin θ) + π else Real.arcsin (-Real.sin θ) - π) =
    θ
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: x y : ℝ
hy₀ : 0 ≤ y
hy₁ : y ≤ π
hxy : x = cos y
⊢ y = y

Tactic:
]

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

Goal state before:
pp: r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
⊢ 0 < Real.cos (θ + π)

Tactic:
]

Goal state after:
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
⊢ 0 < Real.cos (θ + π)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: x : ℝ
⊢ x ≤ -1 ↔ x ≤ -1

Tactic:
]

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

Goal state before:
pp: x : ℝ
⊢ π / 2 + arcsin x = π / 2 + arcsin x

Tactic:
]

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

Goal state before:
pp: x : ℝ
hx : 1 ≤ x
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: x : ℝ
hx : x ≤ -1
⊢ π = π

Tactic:
]

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

Goal state before:
pp: case neg
x : ℝ
hx₁ : x < -1
⊢ sin (arccos x) = √(1 - x ^ 2)

Tactic:
]

Goal state after:
case neg
x : ℝ
hx₁ : x < -1
⊢ sin (arccos x) = √(1 - x ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: case neg
x : ℝ
hx₁ : -1 ≤ x
hx₂ : 1 < x
⊢ sin (arccos x) = √(1 - x ^ 2)

Tactic:
]

Goal state after:
case neg
x : ℝ
hx₁ : -1 ≤ x
hx₂ : 1 < x
⊢ sin (arccos x) = √(1 - x ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: case neg
x : ℝ
hx₁ : -1 ≤ x
hx₂ : 1 < x
⊢ sin 0 = √(1 - x ^ 2)

Tactic:
sin_zero,

Goal state after:
case neg
x : ℝ
hx₁ : -1 ≤ x
hx₂ : 1 < x
⊢ 0 = √(1 - x ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case neg.inl
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
hcos : Real.cos θ < 0
hsin : Real.sin θ < 0
⊢ θ = θ

pp: case neg.inl.hx₁
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
hcos : Real.cos θ < 0
hsin : Real.sin θ < 0
⊢ -(π / 2) ≤ θ + π

pp: case neg.inl.hx₂
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
hcos : Real.cos θ < 0
hsin : Real.sin θ < 0
⊢ θ + π ≤ π / 2

pp: case neg.inl.hnc
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
hcos : Real.cos θ < 0
hsin : Real.sin θ < 0
⊢ ¬0 ≤ Real.sin θ

pp: case neg.inl.hnc
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
hcos : Real.cos θ < 0
hsin : Real.sin θ < 0
⊢ ¬0 ≤ Real.cos θ

Tactic:
]

Goal state after:
case neg.inl.hx₁
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
hcos : Real.cos θ < 0
hsin : Real.sin θ < 0
⊢ -(π / 2) ≤ θ + π

case neg.inl.hx₂
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
hcos : Real.cos θ < 0
hsin : Real.sin θ < 0
⊢ θ + π ≤ π / 2

case neg.inl.hnc
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
hcos : Real.cos θ < 0
hsin : Real.sin θ < 0
⊢ ¬0 ≤ Real.sin θ

case neg.inl.hnc
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
hcos : Real.cos θ < 0
hsin : Real.sin θ < 0
⊢ ¬0 ≤ Real.cos θ
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: case pos
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ √(1 - x ^ 2) = √(1 - x ^ 2)

Tactic:
]

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

Goal state before:
pp: x : ℝ
⊢ π / 2 - arcsin x ≤ π / 4 ↔ π / 4 ≤ arcsin x

Tactic:
]

Goal state after:
x : ℝ
⊢ π / 2 - arcsin x ≤ π / 4 ↔ π / 4 ≤ arcsin x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

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

Tactic:
]

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

Goal state before:
pp: case neg.inr
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : π / 2 < θ
hθ : θ ≤ π
hcos : Real.cos θ < 0
hsin : 0 ≤ Real.sin θ
⊢ θ = θ

pp: case neg.inr.hx₁
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : π / 2 < θ
hθ : θ ≤ π
hcos : Real.cos θ < 0
hsin : 0 ≤ Real.sin θ
⊢ -(π / 2) ≤ θ - π

pp: case neg.inr.hx₂
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : π / 2 < θ
hθ : θ ≤ π
hcos : Real.cos θ < 0
hsin : 0 ≤ Real.sin θ
⊢ θ - π ≤ π / 2

pp: case neg.inr.hc
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : π / 2 < θ
hθ : θ ≤ π
hcos : Real.cos θ < 0
hsin : 0 ≤ Real.sin θ
⊢ 0 ≤ Real.sin θ

pp: case neg.inr.hnc
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : π / 2 < θ
hθ : θ ≤ π
hcos : Real.cos θ < 0
hsin : 0 ≤ Real.sin θ
⊢ ¬0 ≤ Real.cos θ

Tactic:
]

Goal state after:
case neg.inr.hx₁
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : π / 2 < θ
hθ : θ ≤ π
hcos : Real.cos θ < 0
hsin : 0 ≤ Real.sin θ
⊢ -(π / 2) ≤ θ - π

case neg.inr.hx₂
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : π / 2 < θ
hθ : θ ≤ π
hcos : Real.cos θ < 0
hsin : 0 ≤ Real.sin θ
⊢ θ - π ≤ π / 2

case neg.inr.hc
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : π / 2 < θ
hθ : θ ≤ π
hcos : Real.cos θ < 0
hsin : 0 ≤ Real.sin θ
⊢ 0 ≤ Real.sin θ

case neg.inr.hnc
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : π / 2 < θ
hθ : θ ≤ π
hcos : Real.cos θ < 0
hsin : 0 ≤ Real.sin θ
⊢ ¬0 ≤ Real.cos θ
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: x : ℝ
h : 0 ≤ x
⊢ arccos (cos (arcsin x)) = arcsin x

Tactic:
]

Goal state after:
x : ℝ
h : 0 ≤ x
⊢ arccos (cos (arcsin x)) = arcsin x
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: x : ℝ
A : 0 < ↑⌊‖x‖⌋₊ + 1
B : ‖x‖ / (↑⌊‖x‖⌋₊ + 1) < 1
n : ℕ
hn : n ≥ ⌊‖x‖⌋₊
⊢ ‖x‖ / (↑n + 1) * ‖x ^ n / ↑n !‖ = ‖x‖ / (↑n + 1) * ‖x ^ n / ↑n !‖

Tactic:
]

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

Goal state before:
pp: θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ θ = θ

Tactic:
]

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

Goal state before:
pp: z : ℂ
⊢ (cexp z).arg = (cexp ↑z.re * cexp (↑(z.im - toIocDiv Real.two_pi_pos (-π) z.im • (2 * π)) * I)).arg

Tactic:
]

Goal state after:
z : ℂ
⊢ (cexp z).arg = (cexp ↑z.re * cexp (↑(z.im - toIocDiv Real.two_pi_pos (-π) z.im • (2 * π)) * I)).arg
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: x : ℝ
hx : 0 < x
⊢ expOrderIso.symm ⟨|x|, ⋯⟩ = expOrderIso.symm ⟨x, hx⟩

Tactic:
]

Goal state after:
x : ℝ
hx : 0 < x
⊢ expOrderIso.symm ⟨|x|, ⋯⟩ = expOrderIso.symm ⟨x, hx⟩
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: x : ℝ
hx : x ≠ 0
⊢ |x| = |x|

Tactic:
]

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

Goal state before:
pp: x : ℝ
hx : 0 < x
⊢ |x| = x

Tactic:
]

Goal state after:
x : ℝ
hx : 0 < x
⊢ |x| = x
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: x : ℝ
hx : x < 0
⊢ |x| = -x

Tactic:
]

Goal state after:
x : ℝ
hx : x < 0
⊢ |x| = -x
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: case pos
x : ℝ
h_zero : x = 0
⊢ 0 ≤ 1

Tactic:
]

Goal state after:
case pos
x : ℝ
h_zero : x = 0
⊢ 0 ≤ 1
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: case neg
x : ℝ
h_zero : ¬x = 0
⊢ x ≤ |x|

Tactic:
]

Goal state after:
case neg
x : ℝ
h_zero : ¬x = 0
⊢ x ≤ |x|
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: z : ℂ
⊢ (cexp z).arg = (cexp z).arg

Tactic:
]

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

Goal state before:
pp: case neg
x : ℝ
hx0 : ¬x ≤ 0
h : rexp 1 * x ≤ rexp x
⊢ rexp 1 * x ≤ rexp x

Tactic:
]

Goal state after:
case neg
x : ℝ
hx0 : ¬x ≤ 0
h : rexp 1 * x ≤ rexp x
⊢ rexp 1 * x ≤ rexp x
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: x y : ℂ
h₁ : ‖x‖ = ‖y‖
h₂ : x.arg = y.arg
⊢ ↑‖y‖ * cexp (↑y.arg * I) = ↑‖y‖ * cexp (↑y.arg * I)

Tactic:
]

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

Goal state before:
pp: x : ℝ
hx0 : ¬x < 0
this : 2 ≤ rexp 1
⊢ 2 ≤ rexp 1

Tactic:
]

Goal state after:
x : ℝ
hx0 : ¬x < 0
this : 2 ≤ rexp 1
⊢ 2 ≤ rexp 1
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: ⊢ 1 = 1

Tactic:
]

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

Goal state before:
pp: case inr
z : ℂ
hπ : 0 < π
hz : z ≠ 0
N : ℤ
hN : z.arg + ↑N * (2 * π) ∈ Ioc (-π) π
⊢ z.arg ∈ Ioc (-π) π

Tactic:
]

Goal state after:
case inr
z : ℂ
hπ : 0 < π
hz : z ≠ 0
N : ℤ
hN : z.arg + ↑N * (2 * π) ∈ Ioc (-π) π
⊢ z.arg ∈ Ioc (-π) π
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: α : 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)
c : ℝ
hc : ∀ᶠ (x : α) in l, ‖f x • g x‖ ≤ c
ε : ℝ
hε0 : 0 < ε
x : α
hfgc : ‖g x‖ ≤ c / ‖f x‖
hεf : c / ε ≤ ‖f x‖
hf0 : f x ≠ 0
hc0 : 0 < c
⊢ ‖g x‖ ≤ c / ‖f x‖

Tactic:
]

Goal state after:
α : 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)
c : ℝ
hc : ∀ᶠ (x : α) in l, ‖f x • g x‖ ≤ c
ε : ℝ
hε0 : 0 < ε
x : α
hfgc : ‖g x‖ ≤ c / ‖f x‖
hεf : c / ε ≤ ‖f x‖
hf0 : f x ≠ 0
hc0 : 0 < c
⊢ ‖g x‖ ≤ c / ‖f x‖
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: case neg
x : ℝ
h : ¬x = 0
⊢ |x| = |x|

Tactic:
]

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

Goal state before:
pp: x : ℝ
⊢ log |x| = log |x|

Tactic:
]

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

Goal state before:
pp: case inr
z : ℂ
hπ : 0 < π
hz : z ≠ 0
N : ℤ
hN : z.arg + ↑N * (2 * π) ∈ Ioc (-π) π
⊢ (↑‖z‖ * (cos (↑z.arg + ↑N * (2 * ↑π)) + sin (↑z.arg + ↑N * (2 * ↑π)) * I)).arg ∈ Ioc (-π) π

Tactic:
]

Goal state after:
case inr
z : ℂ
hπ : 0 < π
hz : z ≠ 0
N : ℤ
hN : z.arg + ↑N * (2 * π) ∈ Ioc (-π) π
⊢ (↑‖z‖ * (cos (↑z.arg + ↑N * (2 * ↑π)) + sin (↑z.arg + ↑N * (2 * ↑π)) * I)).arg ∈ Ioc (-π) π
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: x : ℝ
hx : 0 < x
⊢ (x - x⁻¹) / 2 = (x - x⁻¹) / 2

Tactic:
]

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

Goal state before:
pp: case inr
z : ℂ
hπ : 0 < π
hz : z ≠ 0
N : ℤ
hN : z.arg + ↑N * (2 * π) ∈ Ioc (-π) π
this : (↑‖z‖ * (cos (↑z.arg + ↑N * (2 * ↑π)) + sin (↑z.arg + ↑N * (2 * ↑π)) * I)).arg = z.arg + ↑N * (2 * π)
⊢ z.arg + ↑N * (2 * π) ∈ Ioc (-π) π

Tactic:
]

Goal state after:
case inr
z : ℂ
hπ : 0 < π
hz : z ≠ 0
N : ℤ
hN : z.arg + ↑N * (2 * π) ∈ Ioc (-π) π
this : (↑‖z‖ * (cos (↑z.arg + ↑N * (2 * ↑π)) + sin (↑z.arg + ↑N * (2 * ↑π)) * I)).arg = z.arg + ↑N * (2 * π)
⊢ z.arg + ↑N * (2 * π) ∈ Ioc (-π) π
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: x : ℝ
hx : 0 < x
⊢ (x + x⁻¹) / 2 = (x + x⁻¹) / 2

Tactic:
]

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

Goal state before:
pp: z : ℂ
h₀ : z ≠ 0
⊢ 0 ≤ z.im ↔ 0 ≤ z.im

Tactic:
]

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

Goal state before:
pp: x : ℝ
x✝ : x ∈ univ
⊢ x = x

Tactic:
]

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

Goal state before:
pp: case inl
r : ℝ
hr : 0 < r
⊢ arg 0 = arg 0

Tactic:
]

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

Goal state before:
pp: x y : ℝ
hx : x ≠ 0
hy : y ≠ 0
⊢ |x| * |y| = |x| * |y|

Tactic:
]

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

Goal state before:
pp: x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ x.arg = y.arg ↔ x.arg = y.arg

pp: case hr
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ 0 < ‖y‖ / ‖x‖

Tactic:
]

Goal state after:
case hr
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ 0 < ‖y‖ / ‖x‖
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: x y : ℝ
hx : x ≠ 0
hy : y ≠ 0
⊢ |x| / |y| = |x| / |y|

Tactic:
]

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

Goal state before:
pp: case neg
x : ℂ
h : ¬x = 0
⊢ x.im / x.re = x.im / x.re

Tactic:
]

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

Goal state before:
pp: case refine_1
z : ℂ
h : z.arg = 0
⊢ 0 ≤ (↑‖z‖ * (cos ↑0 + sin ↑0 * I)).re ∧ (↑‖z‖ * (cos ↑0 + sin ↑0 * I)).im = 0

Tactic:
]

Goal state after:
case refine_1
z : ℂ
h : z.arg = 0
⊢ 0 ≤ (↑‖z‖ * (cos ↑0 + sin ↑0 * I)).re ∧ (↑‖z‖ * (cos ↑0 + sin ↑0 * I)).im = 0
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: case neg
x : ℝ
hx : ¬x = 0
⊢ |x|⁻¹ = |x|⁻¹

Tactic:
]

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

Goal state before:
pp: x y : ℝ
h : 0 < x
h₁ : 0 < y
⊢ x ≤ y ↔ x ≤ y

Tactic:
]

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

Goal state before:
pp: z : ℂ
⊢ 0 ≤ z.re ∧ 0 = z.im ↔ 0 ≤ z.re ∧ 0 = z.im

Tactic:
]

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

Goal state before:
pp: case hg
α : 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‖
⊢ Tendsto g l (𝓝 0)

Tactic:
]

Goal state after:
case hg
α : 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‖
⊢ Tendsto g l (𝓝 0)
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: x y : ℝ
hx : 0 < x
h : x < y
⊢ x < y

Tactic:
]

Goal state after:
x y : ℝ
hx : 0 < x
h : x < y
⊢ x < y
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case neg.mp
z : ℂ
h₀ : ¬z = 0
h : z.arg = π
⊢ (↑‖z‖ * (cos ↑π + sin ↑π * I)).re < 0 ∧ (↑‖z‖ * (cos ↑π + sin ↑π * I)).im = 0

Tactic:
]

Goal state after:
case neg.mp
z : ℂ
h₀ : ¬z = 0
h : z.arg = π
⊢ (↑‖z‖ * (cos ↑π + sin ↑π * I)).re < 0 ∧ (↑‖z‖ * (cos ↑π + sin ↑π * I)).im = 0
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: x y : ℝ
hx : 0 < x
hy : 0 < y
⊢ x < y ↔ x < y

Tactic:
]

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

Goal state before:
pp: x y : ℝ
hx : 0 < x
⊢ x ≤ rexp y ↔ x ≤ rexp y

Tactic:
]

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

Goal state before:
pp: x y : ℝ
hx : 0 < x
⊢ x < rexp y ↔ x < rexp y

Tactic:
]

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

Goal state before:
pp: case neg.mpr
x : ℝ
h : x < 0
h₀ : ¬{ re := x, im := 0 } = 0
⊢ { re := x, im := 0 }.arg = (↑(-x) * -1).arg

Tactic:
]

Goal state after:
case neg.mpr
x : ℝ
h : x < 0
h₀ : ¬{ re := x, im := 0 } = 0
⊢ { re := x, im := 0 }.arg = (↑(-x) * -1).arg
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

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

Tactic:
]

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

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

Tactic:
(arg_le_pi z).lt_iff_ne,

Goal state after:
z : ℂ
⊢ z.arg ≠ π ↔ 0 ≤ z.re ∨ z.im ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

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

Tactic:
]

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

Goal state before:
pp: z : ℂ
⊢ z.re < 0 ∧ z.im = 0 ↔ z.re < 0 ∧ z.im = 0

Tactic:
]

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

Goal state before:
pp: case inr
x : ℝ
hx✝ : 0 ≤ x
hx : 0 < x
⊢ log 1 < log x ↔ 1 < x

Tactic:
]

Goal state after:
case inr
x : ℝ
hx✝ : 0 ≤ x
hx : 0 < x
⊢ log 1 < log x ↔ 1 < x
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case neg.mp
z : ℂ
h₀ : ¬z = 0
h : z.arg = π / 2
⊢ (↑‖z‖ * (cos ↑(π / 2) + sin ↑(π / 2) * I)).re = 0 ∧ 0 < (↑‖z‖ * (cos ↑(π / 2) + sin ↑(π / 2) * I)).im

Tactic:
]

Goal state after:
case neg.mp
z : ℂ
h₀ : ¬z = 0
h : z.arg = π / 2
⊢ (↑‖z‖ * (cos ↑(π / 2) + sin ↑(π / 2) * I)).re = 0 ∧ 0 < (↑‖z‖ * (cos ↑(π / 2) + sin ↑(π / 2) * I)).im
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: x : ℝ
hx : x < -1
⊢ 0 < log (-x)

Tactic:
]

Goal state after:
x : ℝ
hx : x < -1
⊢ 0 < log (-x)
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: x : ℝ
h : 0 < x
⊢ log x < log 1 ↔ x < 1

Tactic:
]

Goal state after:
x : ℝ
h : 0 < x
⊢ log x < log 1 ↔ x < 1
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case neg.mpr
y : ℝ
h₀ : ¬{ re := 0, im := y } = 0
hy : 0 < y
⊢ { re := 0, im := y }.arg = { re := 0, im := y }.arg

Tactic:
]

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

Goal state before:
pp: x : ℝ
h0 : x < 0
h1 : -1 < x
⊢ log (-x) < 0

Tactic:
]

Goal state after:
x : ℝ
h0 : x < 0
h1 : -1 < x
⊢ log (-x) < 0
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: x : ℝ
hx : 0 < x
⊢ 1 ≤ x ↔ 1 ≤ x

Tactic:
]

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

Goal state before:
pp: x : ℂ
hx : x ≠ 0
⊢ x = x

Tactic:
]

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

Goal state before:
pp: case inr
x : ℝ
hx✝ : 0 ≤ x
hx : 0 < x
⊢ x ≤ 1 ↔ x ≤ 1

Tactic:
]

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

Goal state before:
pp: n : ℕ
⊢ 0 ≤ log ↑n

Tactic:
]

Goal state after:
n : ℕ
⊢ 0 ≤ log ↑n
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case neg.mp
z : ℂ
h₀ : ¬z = 0
h : z.arg = -(π / 2)
⊢ (↑‖z‖ * (cos ↑(-(π / 2)) + sin ↑(-(π / 2)) * I)).re = 0 ∧ (↑‖z‖ * (cos ↑(-(π / 2)) + sin ↑(-(π / 2)) * I)).im < 0

Tactic:
]

Goal state after:
case neg.mp
z : ℂ
h₀ : ¬z = 0
h : z.arg = -(π / 2)
⊢ (↑‖z‖ * (cos ↑(-(π / 2)) + sin ↑(-(π / 2)) * I)).re = 0 ∧ (↑‖z‖ * (cos ↑(-(π / 2)) + sin ↑(-(π / 2)) * I)).im < 0
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: x : ℂ
hx₁ : -π < x.im
hx₂ : x.im ≤ π
⊢ x = x

Tactic:
]

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

Goal state before:
pp: case inl
n : ℤ
hn : 0 < n
⊢ 0 ≤ log ↑n

Tactic:
| inl hn =>

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

Goal state before:
pp: case inr.inl
n : ℤ
hn : 0 = n
⊢ 0 ≤ log ↑n

Tactic:
| inl hn =>

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

Goal state before:
pp: n : ℤ
hn : 0 < -n
⊢ 1 ≤ -↑n

Tactic:
]

Goal state after:
n : ℤ
hn : 0 < -n
⊢ 1 ≤ -↑n
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: x : ℂ
⊢ ↑x.re + ↑(toIocMod Real.two_pi_pos (-π) x.im) * I = ↑x.re + ↑(toIocMod Real.two_pi_pos (-π) x.im) * I

Tactic:
]

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

Goal state before:
pp: case inr.inr
n : ℤ
hn : n < 0
this : 1 ≤ -↑n
⊢ 0 ≤ log (-↑n)

Tactic:
]

Goal state after:
case inr.inr
n : ℤ
hn : n < 0
this : 1 ≤ -↑n
⊢ 0 ≤ log (-↑n)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case neg.mpr
y : ℝ
h₀ : ¬{ re := 0, im := y } = 0
hy : y < 0
⊢ (↑0 + ↑y * I).arg = (↑(-y) * -I).arg

Tactic:
]

Goal state after:
case neg.mpr
y : ℝ
h₀ : ¬{ re := 0, im := y } = 0
hy : y < 0
⊢ (↑0 + ↑y * I).arg = (↑(-y) * -I).arg
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x < y
⊢ log |y| < log |x|

Tactic:
]

Goal state after:
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x < y
⊢ log |y| < log |x|
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: z : ℂ
h₁ : 0 ≤ z.im
h₂ : z ≠ 0
⊢ z.arg = z.arg

Tactic:
]

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

Goal state before:
pp: x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x < y
⊢ x < y

Tactic:
]

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

Goal state before:
pp: x : ℂ
⊢ ↑x.re + ↑x.im * I - ↑(toIocDiv Real.two_pi_pos (-π) x.im • (2 * π)) * I =
    x - ↑(toIocDiv Real.two_pi_pos (-π) x.im) * (2 * ↑π * I)

Tactic:
]

Goal state after:
x : ℂ
⊢ ↑x.re + ↑x.im * I - ↑(toIocDiv Real.two_pi_pos (-π) x.im • (2 * π)) * I =
    x - ↑(toIocDiv Real.two_pi_pos (-π) x.im) * (2 * ↑π * I)
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: x : ℝ
hx1 : 0 < x
hx2 : x ≠ 1
⊢ x ≠ 1

pp: x : ℝ
hx1 : 0 < x
hx2 : x ≠ 1
⊢ 1 ∈ Ioi 0

Tactic:
]

Goal state after:
x : ℝ
hx1 : 0 < x
hx2 : x ≠ 1
⊢ x ≠ 1

x : ℝ
hx1 : 0 < x
hx2 : x ≠ 1
⊢ 1 ∈ Ioi 0
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: z : ℂ
hz : z.im < 0
h₀ : z ≠ 0
⊢ z.arg = z.arg

pp: case hx₁
z : ℂ
hz : z.im < 0
h₀ : z ≠ 0
⊢ 0 ≤ -z.arg

pp: case hx₂
z : ℂ
hz : z.im < 0
h₀ : z ≠ 0
⊢ -z.arg ≤ π

Tactic:
]

Goal state after:
case hx₁
z : ℂ
hz : z.im < 0
h₀ : z ≠ 0
⊢ 0 ≤ -z.arg

case hx₂
z : ℂ
hz : z.im < 0
h₀ : z ≠ 0
⊢ -z.arg ≤ π
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:
]

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: x y : ℂ
hx₁ : -π < x.im
hx₂ : x.im ≤ π
hy₁ : -π < y.im
hy₂ : y.im ≤ π
hxy : cexp x = cexp y
⊢ log (cexp y) = log (cexp y)

Tactic:
]

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

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
⊢ Real.log x = Real.log x

Tactic:
]

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

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: case succ.inr
x : ℝ
n : ℕ
ih : log (x ^ n) = ↑n * log x
hx : x ≠ 0
⊢ ↑n * log x + log x = ↑n * log x + log x

Tactic:
]

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

Goal state before:
pp: r : ℝ
hr : 0 < r
x : ℂ
hx : x ≠ 0
⊢ ↑(Real.log r) + log x = ↑(Real.log r) + log x

Tactic:
]

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

Goal state before:
pp: case ofNat
x : ℝ
a✝ : ℕ
⊢ ↑a✝ * log x = ↑a✝ * log x

Tactic:
]

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

Goal state before:
pp: case negSucc
x : ℝ
a✝ : ℕ
⊢ -(↑a✝ + 1) * log x = -(↑a✝ + 1) * log x

Tactic:
]

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

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
⊢ log x = log x

pp: x : ℝ
hx : 0 ≤ x
⊢ 2 ≠ 0

Tactic:
]

Goal state after:
x : ℝ
hx : 0 ≤ x
⊢ 2 ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: x : ℝ
hx : 0 < x
⊢ log x + 1 ≤ x

Tactic:
]

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

Goal state before:
pp: x : ℝ
hx : 0 < x
⊢ x = x

Tactic:
]

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

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

Tactic:
]

Goal state after:
x : ℝ
hx : 0 ≤ x
⊢ log x⁻¹ ≤ x⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: case pos
x : ℂ
hx : x.arg = π
⊢ ↑(Real.log ‖x‖) + ↑π * I = ↑(Real.log ‖x‖) + ↑π * I

Tactic:
]

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

Goal state before:
pp: x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : -log x * x < 1
⊢ |log x * x| < 1

Tactic:
]

Goal state after:
x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : -log x * x < 1
⊢ |log x * x| < 1