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

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

Tactic:
]

Goal state after:
x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : -log x * x < 1
⊢ 0 ≤ log x⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

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

Tactic:
]

Goal state after:
x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : -log x * x < 1
⊢ x ≤ 1
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: x : ℂ
h : x.arg ≠ π
⊢ (starRingEnd ℂ) (log x) = (starRingEnd ℂ) (log x)

Tactic:
]

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

Goal state before:
pp: ψ θ : ℝ
⊢ -ψ + θ ∈ AddSubgroup.zmultiples (2 * π) ↔ ∃ k, θ - ψ = 2 * π * ↑k

Tactic:
]

Goal state after:
ψ θ : ℝ
⊢ -ψ + θ ∈ AddSubgroup.zmultiples (2 * π) ↔ ∃ k, θ - ψ = 2 * π * ↑k
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

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

Tactic:
]

Goal state after:
x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : |log x * x| < 1
aux : 0 ≤ -log x * x
⊢ |log x * x| < 1
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
⊢ rexp (2 * x / (x + 2)) ≤ 1 + x

Tactic:
]

Goal state after:
x : ℝ
hx : 0 ≤ x
⊢ rexp (2 * x / (x + 2)) ≤ 1 + x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: ⊢ 2 * π = 2 * π

Tactic:
]

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

Goal state before:
pp: ⊢ ∃ k, -π - π = 2 * π * ↑k

Tactic:
]

Goal state after:
⊢ ∃ k, -π - π = 2 * π * ↑k
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : ℝ
⊢ ↑θ = ↑θ

Tactic:
]

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

Goal state before:
pp: x : ℝ
hx : 0 < x
⊢ rexp (2 * x / (x + 2)) < 1 + x

Tactic:
]

Goal state after:
x : ℝ
hx : 0 < x
⊢ rexp (2 * x / (x + 2)) < 1 + x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: ⊢ ↑π = ↑π

Tactic:
]

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

Goal state before:
pp: case neg
x : ℂ
hx : ¬x = 0
⊢ (if x.arg = π then log x else (starRingEnd ℂ) (log x)) - ↑(Real.log (normSq x)) =
    if x.arg = π then -(starRingEnd ℂ) (log x) else -log x

pp: case neg.hr
x : ℂ
hx : ¬x = 0
⊢ 0 < (normSq x)⁻¹

pp: case neg.hx
x : ℂ
hx : ¬x = 0
⊢ (starRingEnd ℂ) x ≠ 0

Tactic:
]

Goal state after:
case neg
x : ℂ
hx : ¬x = 0
⊢ (if x.arg = π then log x else (starRingEnd ℂ) (log x)) - ↑(Real.log (normSq x)) =
    if x.arg = π then -(starRingEnd ℂ) (log x) else -log x

case neg.hr
x : ℂ
hx : ¬x = 0
⊢ 0 < (normSq x)⁻¹

case neg.hx
x : ℂ
hx : ¬x = 0
⊢ (starRingEnd ℂ) x ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : Angle
⊢ θ + ↑π = θ + ↑π

Tactic:
]

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

Goal state before:
pp: ⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: case cons
a : ℝ
l : List ℝ
ih : log l.prod = (List.map (fun x ↦ log x) l).sum
h : ¬a = 0 ∧ ∀ a ∈ l, ¬a = 0
this : l.prod ≠ 0
⊢ (List.map (fun x ↦ log x) l).sum = (List.map (fun x ↦ log x) l).sum

Tactic:
]

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

Goal state before:
pp: s : Multiset ℝ
h : ∀ x ∈ s, x ≠ 0
⊢ (Multiset.map (fun x ↦ log x) s).sum = (Multiset.map (fun x ↦ log x) s).sum

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: case neg.hr
x : ℂ
hx : ¬x = 0
⊢ x ≠ 0

Tactic:
]

Goal state after:
case neg.hr
x : ℂ
hx : ¬x = 0
⊢ x ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: case neg.hx
x : ℂ
hx : ¬x = 0
⊢ x ≠ 0

Tactic:
]

Goal state after:
case neg.hx
x : ℂ
hx : ¬x = 0
⊢ x ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: α : Type u_1
s : Finset α
f : α → ℝ
hf : ∀ x ∈ s, f x ≠ 0
⊢ (List.map (fun x ↦ log x) (List.map (fun i ↦ f i) s.toList)).sum = ∑ i ∈ s, log (f i)

Tactic:
]

Goal state after:
α : Type u_1
s : Finset α
f : α → ℝ
hf : ∀ x ∈ s, f x ≠ 0
⊢ (List.map (fun x ↦ log x) (List.map (fun i ↦ f i) s.toList)).sum = ∑ i ∈ s, log (f i)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: x : ℂ
hx : x.arg ≠ π
⊢ -log x = -log x

Tactic:
]

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

Goal state before:
pp: θ : Angle
⊢ 2 • θ ≠ 0 ↔ ¬2 • θ = 0

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: θ : Angle
⊢ θ ≠ -θ ↔ ¬θ = -θ

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: θ : Angle
⊢ -θ ≠ θ ↔ ¬-θ = θ

Tactic:
]

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

Goal state before:
pp: θ : Angle
⊢ ↑π = ↑π

Tactic:
]

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

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

Tactic:
]

Goal state after:
x : ℂ
hx : 0 ≤ x.im
⊢ (∃ n, x = ↑n * (2 * ↑π * I)) ↔ ∃ n, x = ↑n * (2 * ↑π * I)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : Angle
h : ↑π = ↑(2 • (π / 2))
⊢ 2 • θ = ↑(2 • (π / 2)) ↔ θ = ↑(π / 2) ∨ θ = ↑(-π / 2)

Tactic:
]

Goal state after:
θ : Angle
h : ↑π = ↑(2 • (π / 2))
⊢ 2 • θ = ↑(2 • (π / 2)) ↔ θ = ↑(π / 2) ∨ θ = ↑(-π / 2)
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)
⊢ ↑n * (2 * ↑π * I) = ↑↑n * (2 * ↑π * I)

Tactic:
]

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

Goal state before:
pp: case inr
n : ℕ
hn : n ≠ 0
⊢ log ↑n = log ↑n

pp: case inr.hg
n : ℕ
hn : n ≠ 0
⊢ ∀ (a : ℕ), ↑(a ^ n.factorization a) = 0 → n.factorization a = 0

Tactic:
]

Goal state after:
case inr.hg
n : ℕ
hn : n ≠ 0
⊢ ∀ (a : ℕ), ↑(a ^ n.factorization a) = 0 → n.factorization a = 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : Angle
h : ↑π = ↑(2 • (π / 2))
⊢ θ = ↑(π / 2) ∨ θ = ↑(π / 2) + ↑π ↔ θ = ↑(π / 2) ∨ θ = ↑(-π / 2)

Tactic:
]

Goal state after:
θ : Angle
h : ↑π = ↑(2 • (π / 2))
⊢ θ = ↑(π / 2) ∨ θ = ↑(π / 2) + ↑π ↔ θ = ↑(π / 2) ∨ θ = ↑(-π / 2)
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: case inr.hg
n : ℕ
hn : n ≠ 0
p : ℕ
hp : ↑(p ^ n.factorization p) = 0
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: k N : ℕ
hN : N ≠ 0
⊢ (∃ n, 2 * ↑π * I * ↑k / ↑N = ↑n * (2 * ↑π * I)) ↔ N ∣ k

Tactic:
]

Goal state after:
k N : ℕ
hN : N ≠ 0
⊢ (∃ n, 2 * ↑π * I * ↑k / ↑N = ↑n * (2 * ↑π * I)) ↔ N ∣ k
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case e_b.e_a
θ : Angle
h : ↑π = ↑(2 • (π / 2))
⊢ 0 = 0

Tactic:
]

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

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

pp: n : ℕ
⊢ ∀ᶠ (x : ℝ) in atTop, id x = 0 → log x ^ n = 0

Tactic:
]

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

n : ℕ
⊢ ∀ᶠ (x : ℝ) in atTop, id x = 0 → log x ^ n = 0
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: x y : ℂ
⊢ cexp x = cexp y ↔ cexp x = cexp y

Tactic:
]

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

Goal state before:
pp: θ : Angle
⊢ θ = ↑(π / 2) ∨ θ = ↑(-π / 2) ↔ θ = ↑(π / 2) ∨ θ = ↑(-π / 2)

Tactic:
]

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

Goal state before:
pp: z : ℂ
⊢ cexp z = cexp z

pp: z : ℂ
⊢ cexp z ≠ 0

Tactic:
]

Goal state after:
z : ℂ
⊢ cexp z ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: case refine_1
s : Set ℂ
hs : (cexp ⁻¹' s).Countable
⊢ s ⊆ s ∪ {0}

Tactic:
]

Goal state after:
case refine_1
s : Set ℂ
hs : (cexp ⁻¹' s).Countable
⊢ s ⊆ s ∪ {0}
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: case refine_2
s : Set ℂ
hs : s.Countable
⊢ (⋃ y ∈ s, cexp ⁻¹' {y}).Countable

Tactic:
]

Goal state after:
case refine_2
s : Set ℂ
hs : s.Countable
⊢ (⋃ y ∈ s, cexp ⁻¹' {y}).Countable
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case mp
θ ψ : ℝ
Hcos : (∃ n, ↑n * π = (θ + ψ) / 2) ∨ ∃ n, ↑n * π = (θ - ψ) / 2
⊢ ↑θ = ↑ψ ∨ ↑θ = -↑ψ

Tactic:
]

Goal state after:
case mp
θ ψ : ℝ
Hcos : (∃ n, ↑n * π = (θ + ψ) / 2) ∨ ∃ n, ↑n * π = (θ - ψ) / 2
⊢ ↑θ = ↑ψ ∨ ↑θ = -↑ψ
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: a : ℝ
ha : 0 < a
⊢ Iio (log a) = Iio (log a)

Tactic:
]

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

Goal state before:
pp: a : ℝ
ha : 0 < a
⊢ Iic (log a) = Iic (log a)

Tactic:
]

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

Goal state before:
pp: case mp.inl
θ ψ : ℝ
n : ℤ
hn : ↑n * π * 2 - ψ = θ
⊢ ↑θ = -↑ψ

Tactic:
]

Goal state after:
case mp.inl
θ ψ : ℝ
n : ℤ
hn : ↑n * π * 2 - ψ = θ
⊢ ↑θ = -↑ψ
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: y : ℝ
this : Tendsto (fun x ↦ 1 + y / x) atTop (𝓝 (1 + 0))
⊢ Tendsto (rexp ∘ fun x ↦ log (x + y) - log x) atTop (𝓝 (1 + 0))

Tactic:
]

Goal state after:
y : ℝ
this : Tendsto (fun x ↦ 1 + y / x) atTop (𝓝 (1 + 0))
⊢ Tendsto (rexp ∘ fun x ↦ log (x + y) - log x) atTop (𝓝 (1 + 0))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case mp.inl
θ ψ : ℝ
n : ℤ
hn : ↑n * π * 2 - ψ = θ
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: ⊢ 𝓝 0 ⊓ 𝓟 {0}ᶜ = 𝓝 0 ⊓ 𝓟 {0}ᶜ

Tactic:
]

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

Goal state before:
pp: case mp.inr
θ ψ : ℝ
n : ℤ
hn : ↑n * π * 2 + ψ = θ
⊢ ↑θ = ↑ψ

Tactic:
]

Goal state after:
case mp.inr
θ ψ : ℝ
n : ℤ
hn : ↑n * π * 2 + ψ = θ
⊢ ↑θ = ↑ψ
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: ⊢ {0}ᶜ ∈ cobounded ℂ

Tactic:
]

Goal state after:
⊢ {0}ᶜ ∈ cobounded ℂ
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: y : ℝ
this : Tendsto (fun x ↦ 1 + y / x) atTop (𝓝 (1 + 0))
x : ℝ
hx₀ : 0 < x
hxy : -y < x
⊢ (x + y) / x = (x + y) / x

pp: y : ℝ
this : Tendsto (fun x ↦ 1 + y / x) atTop (𝓝 (1 + 0))
x : ℝ
hx₀ : 0 < x
hxy : -y < x
⊢ x ≠ 0

pp: y : ℝ
this : Tendsto (fun x ↦ 1 + y / x) atTop (𝓝 (1 + 0))
x : ℝ
hx₀ : 0 < x
hxy : -y < x
⊢ 0 < x

pp: y : ℝ
this : Tendsto (fun x ↦ 1 + y / x) atTop (𝓝 (1 + 0))
x : ℝ
hx₀ : 0 < x
hxy : -y < x
⊢ 0 < x + y

Tactic:
]

Goal state after:
y : ℝ
this : Tendsto (fun x ↦ 1 + y / x) atTop (𝓝 (1 + 0))
x : ℝ
hx₀ : 0 < x
hxy : -y < x
⊢ x ≠ 0

y : ℝ
this : Tendsto (fun x ↦ 1 + y / x) atTop (𝓝 (1 + 0))
x : ℝ
hx₀ : 0 < x
hxy : -y < x
⊢ 0 < x

y : ℝ
this : Tendsto (fun x ↦ 1 + y / x) atTop (𝓝 (1 + 0))
x : ℝ
hx₀ : 0 < x
hxy : -y < x
⊢ 0 < x + y
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case mp.inr
θ ψ : ℝ
n : ℤ
hn : ↑n * π * 2 + ψ = θ
⊢ ↑ψ = ↑ψ

Tactic:
]

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

Goal state before:
pp: case mpr
θ ψ : ℝ
⊢ ((∃ k, θ - ψ = 2 * π * ↑k) ∨ ∃ k, θ - -ψ = 2 * π * ↑k) → cos θ = cos ψ

Tactic:
]

Goal state after:
case mpr
θ ψ : ℝ
⊢ ((∃ k, θ - ψ = 2 * π * ↑k) ∨ ∃ k, θ - -ψ = 2 * π * ↑k) → cos θ = cos ψ
Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex

Goal state before:
pp: x y : ℂ
⊢ ¬x = 0 ∨ y = 0 ↔ x ≠ 0 ∨ y = 0

Tactic:
]

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

Goal state before:
pp: x a : ℂ
⊢ 0 ^ x = a ↔ 0 ^ x = a

Tactic:
]

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

Goal state before:
pp: e : ℝ
n : ℕ
h : NormNum.IsNat e n
⊢ 0 ≤ Real.log ↑n

Tactic:
]

Goal state after:
e : ℝ
n : ℕ
h : NormNum.IsNat e n
⊢ 0 ≤ Real.log ↑n
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

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

Tactic:
]

Goal state after:
e : ℝ
n : ℕ
h : NormNum.IsNat e n
w : Nat.blt 1 n = true
⊢ 0 < Real.log ↑n
Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex

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

Tactic:
]

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

Goal state before:
pp: x : ℂ
⊢ (if 1 = 0 then if x = 0 then 1 else 0 else cexp (log 1 * x)) = 1

Tactic:
]

Goal state after:
x : ℂ
⊢ (if 1 = 0 then if x = 0 then 1 else 0 else cexp (log 1 * x)) = 1
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: e : ℝ
n : ℕ
h : NormNum.IsInt e (Int.negOfNat n)
⊢ 0 ≤ Real.log (-↑n)

Tactic:
]

Goal state after:
e : ℝ
n : ℕ
h : NormNum.IsInt e (Int.negOfNat n)
⊢ 0 ≤ Real.log (-↑n)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case mpr.inl
θ ψ : ℝ
k : ℤ
H : θ - ψ = 2 * π * ↑k
⊢ 0 = 0

Tactic:
]

Goal state after:
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
⊢ 0 < Real.log (-↑n)

Tactic:
]

Goal state after:
e : ℝ
n : ℕ
h : NormNum.IsInt e (Int.negOfNat n)
w : Nat.blt 1 n = true
⊢ 0 < Real.log (-↑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
⊢ 0 < Real.log ↑n

Tactic:
]

Goal state after:
e : ℝ
n : ℕ
h : NormNum.IsInt e (Int.negOfNat n)
w : Nat.blt 1 n = true
⊢ 0 < Real.log ↑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
⊢ 0 < Real.log (-↑n)

Tactic:
rw [Real.log_neg_eq_log]

Goal state after:
e : ℝ
n : ℕ
h : NormNum.IsInt e (Int.negOfNat n)
w : Nat.blt 1 n = true
⊢ 0 < Real.log ↑n
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case mpr.inr
θ ψ : ℝ
k : ℤ
H : θ - -ψ = 2 * π * ↑k
⊢ 0 = 0

Tactic:
]

Goal state after:
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
⊢ 0 < Real.log (↑n / ↑d)

Tactic:
]

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

Goal state before:
pp: case mp
θ ψ : ℝ
Hsin : cos (π / 2 - θ) = cos (π / 2 - ψ)
⊢ ↑θ = ↑ψ ∨ ↑θ + ↑ψ = ↑π

Tactic:
]

Goal state after:
case mp
θ ψ : ℝ
Hsin : cos (π / 2 - θ) = cos (π / 2 - ψ)
⊢ ↑θ = ↑ψ ∨ ↑θ + ↑ψ = ↑π
Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex

Goal state before:
pp: x y z : ℂ
hx : x ≠ 0
⊢ x ^ y * (x ^ z)⁻¹ = x ^ y * (x ^ z)⁻¹

Tactic:
]

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

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

Tactic:
]

Goal state after:
e : ℝ
d : ℕ
n : ℤ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (↑n / ↑d < -1) = true
⊢ 0 < Real.log (↑n / ↑d)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case mp.inl
θ ψ : ℝ
Hsin : cos (π / 2 - θ) = cos (π / 2 - ψ)
h : ↑(π / 2) - ↑θ = ↑(π / 2) - ↑ψ
⊢ ↑θ = ↑ψ

Tactic:
]

Goal state after:
case mp.inl
θ ψ : ℝ
Hsin : cos (π / 2 - θ) = cos (π / 2 - ψ)
h : ↑(π / 2) - ↑θ = ↑(π / 2) - ↑ψ
⊢ ↑θ = ↑ψ
Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex

Goal state before:
pp: case inr
x : ℂ
n : ℤ
y : ℂ
hx : x ≠ 0
⊢ cexp (log x * y) ^ n = cexp (log x * y) ^ n

Tactic:
]

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

Goal state before:
pp: x y : ℂ
n : ℤ
⊢ (x ^ y) ^ n = (x ^ y) ^ n

Tactic:
]

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

Goal state before:
pp: x y : ℂ
n : ℕ
⊢ (x ^ y) ^ n = (x ^ y) ^ n

Tactic:
]

Goal state after:
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
⊢ Real.log (↑n / ↑d) ≠ 0

Tactic:
]

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
⊢ Real.log (↑n / ↑d) ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex

Goal state before:
pp: x : ℂ
n : ℕ
hn : n ≠ 0
⊢ x = x

pp: x : ℂ
n : ℕ
hn : n ≠ 0
⊢ ↑n ≠ 0

Tactic:
]

Goal state after:
x : ℂ
n : ℕ
hn : n ≠ 0
⊢ ↑n ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex

Goal state before:
pp: x : ℂ
n : ℤ
hlt : -π < x.arg * ↑n
hle : x.arg * ↑n ≤ π
y : ℂ
⊢ x ^ (↑n * y) = (x ^ n) ^ y

Tactic:
]

Goal state after:
x : ℂ
n : ℤ
hlt : -π < x.arg * ↑n
hle : x.arg * ↑n ≤ π
y : ℂ
⊢ x ^ (↑n * y) = (x ^ n) ^ y
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: x : ℂ
⊢ (↑(normSq x)⁻¹ * (starRingEnd ℂ) x).arg = ((starRingEnd ℂ) x).arg

Tactic:
]

Goal state after:
x : ℂ
⊢ (↑(normSq x)⁻¹ * (starRingEnd ℂ) x).arg = ((starRingEnd ℂ) x).arg
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case mp.inr
θ ψ : ℝ
Hsin : cos (π / 2 - θ) = cos (π / 2 - ψ)
h : ↑π = ↑θ + ↑ψ
⊢ ↑θ + ↑ψ = ↑π

Tactic:
]

Goal state after:
case mp.inr
θ ψ : ℝ
Hsin : cos (π / 2 - θ) = cos (π / 2 - ψ)
h : ↑π = ↑θ + ↑ψ
⊢ ↑θ + ↑ψ = ↑π
Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex

Goal state before:
pp: x : ℂ
n : ℤ
hlt : -π < x.arg * ↑n
hle : x.arg * ↑n ≤ π
y : ℂ
⊢ (x ^ n) ^ y = (x ^ n) ^ y

pp: case h₁
x : ℂ
n : ℤ
hlt : -π < x.arg * ↑n
hle : x.arg * ↑n ≤ π
y : ℂ
⊢ -π < (log x * ↑n).im

pp: case h₂
x : ℂ
n : ℤ
hlt : -π < x.arg * ↑n
hle : x.arg * ↑n ≤ π
y : ℂ
⊢ (log x * ↑n).im ≤ π

Tactic:
]

Goal state after:
case h₁
x : ℂ
n : ℤ
hlt : -π < x.arg * ↑n
hle : x.arg * ↑n ≤ π
y : ℂ
⊢ -π < (log x * ↑n).im

case h₂
x : ℂ
n : ℤ
hlt : -π < x.arg * ↑n
hle : x.arg * ↑n ≤ π
y : ℂ
⊢ (log x * ↑n).im ≤ π
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: x : ℂ
⊢ |if x.arg = π then π else -x.arg| = |x.arg|

Tactic:
]

Goal state after:
x : ℂ
⊢ |if x.arg = π then π else -x.arg| = |x.arg|
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case mpr
θ ψ : ℝ
⊢ ((∃ k, θ - ψ = 2 * π * ↑k) ∨ ∃ k, θ - (π - ψ) = 2 * π * ↑k) → sin θ = sin ψ

Tactic:
]

Goal state after:
case mpr
θ ψ : ℝ
⊢ ((∃ k, θ - ψ = 2 * π * ↑k) ∨ ∃ k, θ - (π - ψ) = 2 * π * ↑k) → sin θ = sin ψ
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

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

Tactic:
]

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

Goal state before:
pp: x : ℂ
n : ℕ
h₀ : n ≠ 0
hlt : -(π / ↑n) < x.arg
hle : x.arg ≤ π / ↑n
⊢ x = x

pp: case hlt
x : ℂ
n : ℕ
h₀ : n ≠ 0
hlt : -(π / ↑n) < x.arg
hle : x.arg ≤ π / ↑n
⊢ -π < ↑n * x.arg

pp: case hle
x : ℂ
n : ℕ
h₀ : n ≠ 0
hlt : -(π / ↑n) < x.arg
hle : x.arg ≤ π / ↑n
⊢ ↑n * x.arg ≤ π

Tactic:
]

Goal state after:
case hlt
x : ℂ
n : ℕ
h₀ : n ≠ 0
hlt : -(π / ↑n) < x.arg
hle : x.arg ≤ π / ↑n
⊢ -π < ↑n * x.arg

case hle
x : ℂ
n : ℕ
h₀ : n ≠ 0
hlt : -(π / ↑n) < x.arg
hle : x.arg ≤ π / ↑n
⊢ ↑n * x.arg ≤ π
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: x : ℂ
⊢ (∃ θ, cexp (↑θ * I) = x) ↔ ∃ θ ∈ Ioc (-π) π, cexp (↑θ * I) = x

Tactic:
]

Goal state after:
x : ℂ
⊢ (∃ θ, cexp (↑θ * I) = x) ↔ ∃ θ ∈ Ioc (-π) π, cexp (↑θ * I) = x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ ψ : ℝ
k : ℤ
H : θ + ψ = 2 * ↑k * π + π
⊢ θ + ψ = 2 * ↑k * π + π

Tactic:
]

Goal state after:
θ ψ : ℝ
k : ℤ
H : θ + ψ = 2 * ↑k * π + π
⊢ θ + ψ = 2 * ↑k * π + π
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case mp.refine_2
θ : ℝ
⊢ cexp (↑θ * I) = cexp (↑θ * I)

Tactic:
]

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

Goal state before:
pp: case hlt
x : ℂ
n : ℕ
h₀ : n ≠ 0
hlt : -(π / ↑n) < x.arg
hle : x.arg ≤ π / ↑n
⊢ -(π / ↑n) < x.arg

Tactic:
]

Goal state after:
case hlt
x : ℂ
n : ℕ
h₀ : n ≠ 0
hlt : -(π / ↑n) < x.arg
hle : x.arg ≤ π / ↑n
⊢ -(π / ↑n) < x.arg
Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex

Goal state before:
pp: case hle
x : ℂ
n : ℕ
h₀ : n ≠ 0
hlt : -(π / ↑n) < x.arg
hle : x.arg ≤ π / ↑n
⊢ x.arg ≤ π / ↑n

Tactic:
]

Goal state after:
case hle
x : ℂ
n : ℕ
h₀ : n ≠ 0
hlt : -(π / ↑n) < x.arg
hle : x.arg ≤ π / ↑n
⊢ x.arg ≤ π / ↑n
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case inr.inl
z : ℂ
hre : z.re < 0
him : 0 ≤ z.im
⊢ z.re ≠ 0

pp: case inr.inl
z : ℂ
hre : z.re < 0
him : 0 ≤ z.im
⊢ 0 < ‖z‖

Tactic:
]

Goal state after:
case inr.inl
z : ℂ
hre : z.re < 0
him : 0 ≤ z.im
⊢ z.re ≠ 0

case inr.inl
z : ℂ
hre : z.re < 0
him : 0 ≤ z.im
⊢ 0 < ‖z‖
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case inr.inr
z : ℂ
hre : z.re < 0
him : z.im < 0
⊢ Real.arcsin ((-z).im / ‖z‖) - π ≤ π / 2

Tactic:
]

Goal state after:
case inr.inr
z : ℂ
hre : z.re < 0
him : z.im < 0
⊢ Real.arcsin ((-z).im / ‖z‖) - π ≤ π / 2
Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex

Goal state before:
pp: case inr.inl
b : ℝ
hb : 0 ≤ b
r : ℂ
hr : r ≠ 0
ha : 0 ≤ 0
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: case mpr.inr
θ ψ : ℝ
k : ℤ
H : θ - (π - ψ) = 2 * π * ↑k
H' : θ + ψ = 2 * ↑k * π + π
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: case inr.inl
z : ℂ
hre : z.re < 0
him : 0 ≤ z.im
⊢ -(π / 2) ≤ Real.arcsin ((-z).im / ‖z‖) + π

Tactic:
]

Goal state after:
case inr.inl
z : ℂ
hre : z.re < 0
him : 0 ≤ z.im
⊢ -(π / 2) ≤ Real.arcsin ((-z).im / ‖z‖) + π
Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex

Goal state before:
pp: case inr.inr.inl
a : ℝ
ha : 0 ≤ a
r : ℂ
hr : r ≠ 0
ha' : 0 < a
hb : 0 ≤ 0
⊢ 0 = 0

Tactic:
]

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

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

pp: case inr.inr
z : ℂ
hre : z.re < 0
him : z.im < 0
⊢ 0 < ‖z‖

Tactic:
]

Goal state after:
case inr.inr
z : ℂ
hre : z.re < 0
him : z.im < 0
⊢ z.re ≠ 0

case inr.inr
z : ℂ
hre : z.re < 0
him : z.im < 0
⊢ 0 < ‖z‖
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: z : ℂ
⊢ (0 ≤ z.re ∨ 0 ≤ z.im) ∧ ¬(z.re = 0 ∧ z.im < 0) ↔ 0 < z.re ∨ 0 ≤ z.im

Tactic:
]

Goal state after:
z : ℂ
⊢ (0 ≤ z.re ∨ 0 ≤ z.im) ∧ ¬(z.re = 0 ∧ z.im < 0) ↔ 0 < z.re ∨ 0 ≤ z.im
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case inr.inl
θ ψ : ℝ
Hcos : cos θ = cos ψ
Hsin : sin θ = sin ψ
hc : ↑θ = -↑ψ
hs : ↑θ = ↑ψ
⊢ ↑θ = ↑ψ

Tactic:
exact hs

Goal state after: