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

Goal state before:
pp: case refine_1
z : ℂ
hz : ‖z‖ = 1
⊢ cexp (↑z.arg * I) = z

Tactic:
calc
      exp (arg z * I) = ‖z‖ * exp (arg z * I) := by rw [hz, ofReal_one, one_mul]
      _ = z := norm_mul_exp_arg_mul_I z

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

Goal state before:
pp: case refine_2
z : ℂ
⊢ (∃ θ, cexp (↑θ * I) = z) → ‖z‖ = 1

Tactic:
·

Goal state after:
case refine_2
z : ℂ
⊢ (∃ θ, cexp (↑θ * I) = z) → ‖z‖ = 1
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

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

pp: case pos
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ sin (arcsin x) / √(1 - x ^ 2) = x / √(1 - x ^ 2)

Tactic:
·

Goal state after:
case neg
x : ℝ
hx₁ : -1 ≤ x
hx₂ : ¬x ≤ 1
⊢ sin (arcsin x) / √(1 - x ^ 2) = x / √(1 - x ^ 2)
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: case inr.left
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 : ℕ), (-1) ^ i * f i - ∑ i ∈ Finset.range (2 * n + 1), (-1) ^ i * f i ≤ f (2 * n + 1)

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:
·

Goal state after:
case inr.left
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 : ℕ), (-1) ^ i * f i - ∑ i ∈ Finset.range (2 * n + 1), (-1) ^ i * f i ≤ f (2 * n + 1)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case pos
r : ℝ
hr : 0 < r
θ : ℝ
hθ : θ ∈ Ioc (-π) π
h₁ : θ ∈ Icc (-(π / 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 θ) - π) =
    θ

pp: case neg
r : ℝ
hr : 0 < r
θ : ℝ
hθ : θ ∈ Ioc (-π) π
h₁ : θ ∉ Icc (-(π / 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 pos
r : ℝ
hr : 0 < r
θ : ℝ
hθ : θ ∈ Ioc (-π) π
h₁ : θ ∈ Icc (-(π / 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.Complex.Arg

Goal state before:
pp: case neg
r : ℝ
hr : 0 < r
θ : ℝ
hθ : θ ∈ Ioc (-π) π
h₁ : θ ∉ Icc (-(π / 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₁ : θ ∉ Icc (-(π / 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.Complex.Arg

Goal state before:
pp: case neg.inl
r : ℝ
hr : 0 < r
θ : ℝ
hθ : θ ∈ Ioc (-π) π
h₁ : θ < -(π / 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 θ) - π) =
    θ

pp: case neg.inr
r : ℝ
hr : 0 < r
θ : ℝ
hθ : θ ∈ Ioc (-π) π
h₁ : π / 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.inl
r : ℝ
hr : 0 < r
θ : ℝ
hθ : θ ∈ Ioc (-π) π
h₁ : θ < -(π / 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.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:
·

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)
⊢ ∑ i ∈ Finset.range (2 * n + 1), (-1) ^ i * f i - ∑' (i : ℕ), (-1) ^ i * f i ≤ f (2 * n + 1)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

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

pp: case pos
x : ℝ
hx₁ : -1 ≤ x
⊢ sin (arccos x) = √(1 - x ^ 2)

Tactic:
·

Goal state after:
case neg
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₂ : ¬x ≤ 1
⊢ sin (arccos x) = √(1 - x ^ 2)

pp: case pos
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ sin (arccos x) = √(1 - x ^ 2)

Tactic:
·

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

Goal state before:
pp: case neg.inr
r : ℝ
hr : 0 < r
θ : ℝ
hθ : θ ∈ Ioc (-π) π
h₁ : π / 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.inr
r : ℝ
hr : 0 < r
θ : ℝ
hθ : θ ∈ Ioc (-π) π
h₁ : π / 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: case mp
x : ℝ
⊢ π / 2 - arcsin x ≤ π / 4 → π / 4 ≤ arcsin x

Tactic:
·

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

Goal state before:
pp: case mpr
x : ℝ
⊢ π / 4 ≤ arcsin x → π / 2 - arcsin x ≤ π / 4

Tactic:
·

Goal state after:
case mpr
x : ℝ
⊢ π / 4 ≤ arcsin x → π / 2 - arcsin x ≤ π / 4
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: z : ℂ
⊢ (cexp z).arg =
    (↑(rexp z.re) * (cos ↑(toIocMod Real.two_pi_pos (-π) z.im) + sin ↑(toIocMod Real.two_pi_pos (-π) z.im) * I)).arg

pp: z : ℂ
⊢ toIocMod Real.two_pi_pos (-π) z.im ∈ Ioc (-π) π

Tactic:
·

Goal state after:
z : ℂ
⊢ (cexp z).arg =
    (↑(rexp z.re) * (cos ↑(toIocMod Real.two_pi_pos (-π) z.im) + sin ↑(toIocMod Real.two_pi_pos (-π) z.im) * I)).arg
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: case pos
x : ℝ
h_zero : x = 0
⊢ x ≤ rexp (log x)

pp: case neg
x : ℝ
h_zero : ¬x = 0
⊢ x ≤ rexp (log x)

Tactic:
·

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

Goal state before:
pp: case neg
x : ℝ
h_zero : ¬x = 0
⊢ x ≤ rexp (log x)

Tactic:
·

Goal state after:
case neg
x : ℝ
h_zero : ¬x = 0
⊢ x ≤ rexp (log x)
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: case pos
x : ℝ
hx0 : x ≤ 0
⊢ rexp 1 * x ≤ rexp x

pp: case neg
x : ℝ
hx0 : ¬x ≤ 0
⊢ rexp 1 * x ≤ rexp x

Tactic:
·

Goal state after:
case pos
x : ℝ
hx0 : x ≤ 0
⊢ rexp 1 * x ≤ rexp x
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

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

Tactic:
·

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

Goal state before:
pp: z : ℂ
⊢ toIocMod Real.two_pi_pos (-π) z.im ∈ Ioc (-π) π

Tactic:
·

Goal state after:
z : ℂ
⊢ toIocMod Real.two_pi_pos (-π) z.im ∈ Ioc (-π) π
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 ε

pp: case inr
α : 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 : ‖f x • g x‖ ≤ c
hεf : c / ε ≤ ‖f x‖
hf0 : f x ≠ 0
hc0 : 0 < c
⊢ g x ∈ closedBall 0 ε

Tactic:
·

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‖
⊢ g x ∈ closedBall 0 ε
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case inl
hπ : 0 < π
⊢ arg 0 ∈ Ioc (-π) π

pp: case inr
z : ℂ
hπ : 0 < π
hz : z ≠ 0
⊢ z.arg ∈ Ioc (-π) π

Tactic:
·

Goal state after:
case inl
hπ : 0 < π
⊢ arg 0 ∈ Ioc (-π) π
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: case pos
x : ℝ
hx0 : x < 0
⊢ 2 * x ≤ rexp x

pp: case neg
x : ℝ
hx0 : ¬x < 0
⊢ 2 * x ≤ rexp x

Tactic:
·

Goal state after:
case pos
x : ℝ
hx0 : x < 0
⊢ 2 * x ≤ rexp x
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

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

Tactic:
·

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

Goal state before:
pp: x : ℝ
⊢ 2 * x ≤ rexp x

Tactic:
by
  by_cases hx0 : x < 0
  · exact le_trans (mul_nonpos_of_nonneg_of_nonpos (by simp only [Nat.ofNat_nonneg]) hx0.le)
      (exp_nonneg x)
  · apply le_trans (mul_le_mul_of_nonneg_right _ (le_of_not_gt hx0)) exp_one_mul_le_exp
    have := Real.add_one_le_exp 1
    rwa [one_add_one_eq_two] at this

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

Goal state before:
pp: case pos
x : ℝ
h : x = 0
⊢ log |x| = log x

pp: case neg
x : ℝ
h : ¬x = 0
⊢ log |x| = log x

Tactic:
·

Goal state after:
case pos
x : ℝ
h : x = 0
⊢ log |x| = log x
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

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

Tactic:
·

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

Goal state before:
pp: case inl
⊢ 0 ≤ arg 0 ↔ 0 ≤ im 0

pp: case inr
z : ℂ
h₀ : z ≠ 0
⊢ 0 ≤ z.arg ↔ 0 ≤ z.im

Tactic:
·

Goal state after:
case inl
⊢ 0 ≤ arg 0 ↔ 0 ≤ im 0
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: z : ℂ
h₀ : z ≠ 0
⊢ 0 ≤ Real.sin z.arg → 0 ≤ z.arg

Tactic:
by
        contrapose!
        intro h
        exact Real.sin_neg_of_neg_of_neg_pi_lt h (neg_pi_lt_arg _)

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

Goal state before:
pp: case inl
r : ℝ
hr : 0 < r
⊢ (↑r * 0).arg = arg 0

pp: case inr
x : ℂ
r : ℝ
hr : 0 < r
hx : x ≠ 0
⊢ (↑r * x).arg = x.arg

Tactic:
·

Goal state after:
case inl
r : ℝ
hr : 0 < r
⊢ (↑r * 0).arg = arg 0
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case pos
x : ℂ
h : x = 0
⊢ Real.tan x.arg = x.im / x.re

pp: case neg
x : ℂ
h : ¬x = 0
⊢ Real.tan x.arg = x.im / x.re

Tactic:
·

Goal state after:
case pos
x : ℂ
h : x = 0
⊢ Real.tan x.arg = x.im / x.re
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case refine_1
z : ℂ
h : z.arg = 0
⊢ 0 ≤ z.re ∧ z.im = 0

pp: case refine_2
z : ℂ
⊢ 0 ≤ z.re ∧ z.im = 0 → z.arg = 0

Tactic:
·

Goal state after:
case refine_1
z : ℂ
h : z.arg = 0
⊢ 0 ≤ z.re ∧ z.im = 0
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: case pos
x : ℝ
hx : x = 0
⊢ log x⁻¹ = -log x

pp: case neg
x : ℝ
hx : ¬x = 0
⊢ log x⁻¹ = -log x

Tactic:
·

Goal state after:
case pos
x : ℝ
hx : x = 0
⊢ log x⁻¹ = -log x
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 (norm ∘ fun x ↦ ‖f₁ x - f₂ x‖)

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 (fun x ↦ ‖g x‖) l (𝓝 0)

Tactic:
·

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 (norm ∘ fun x ↦ ‖f₁ x - f₂ x‖)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case refine_1
z : ℂ
h : z.arg = 0
⊢ 0 ≤ z.re ∧ z.im = 0

Tactic:
rw [← norm_mul_cos_add_sin_mul_I z, h]
    simp [norm_nonneg]

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

Goal state before:
pp: case refine_2
z : ℂ
⊢ 0 ≤ z.re ∧ z.im = 0 → z.arg = 0

Tactic:
·

Goal state after:
case refine_2
z : ℂ
⊢ 0 ≤ z.re ∧ z.im = 0 → z.arg = 0
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 (fun x ↦ ‖g x‖) 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 (fun x ↦ ‖g x‖) l (𝓝 0)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case pos
z : ℂ
h₀ : z = 0
⊢ z.arg = π ↔ z.re < 0 ∧ z.im = 0

pp: case neg
z : ℂ
h₀ : ¬z = 0
⊢ z.arg = π ↔ z.re < 0 ∧ z.im = 0

Tactic:
·

Goal state after:
case pos
z : ℂ
h₀ : z = 0
⊢ z.arg = π ↔ z.re < 0 ∧ z.im = 0
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case neg.mp
z : ℂ
h₀ : ¬z = 0
⊢ z.arg = π → z.re < 0 ∧ z.im = 0

pp: case neg.mpr
z : ℂ
h₀ : ¬z = 0
⊢ z.re < 0 ∧ z.im = 0 → z.arg = π

Tactic:
·

Goal state after:
case neg.mp
z : ℂ
h₀ : ¬z = 0
⊢ z.arg = π → z.re < 0 ∧ z.im = 0
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: case hf₁
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)
⊢ Tendsto (fun x ↦ ↑⌊x⌋₊) atTop (cobounded K)

pp: case hbdd
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)
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) atTop fun x ↦ ‖↑⌊x⌋₊ - x‖

Tactic:
·

Goal state after:
case hf₁
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)
⊢ Tendsto (fun x ↦ ↑⌊x⌋₊) atTop (cobounded K)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case neg.mpr
z : ℂ
h₀ : ¬z = 0
⊢ z.re < 0 ∧ z.im = 0 → z.arg = π

Tactic:
·

Goal state after:
case neg.mpr
z : ℂ
h₀ : ¬z = 0
⊢ z.re < 0 ∧ z.im = 0 → z.arg = π
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: case hbdd
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)
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) atTop fun x ↦ ‖↑⌊x⌋₊ - x‖

Tactic:
·

Goal state after:
case hbdd
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)
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) atTop fun x ↦ ‖↑⌊x⌋₊ - x‖
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: case inl
x y : ℝ
h : log x ≤ y
hx : x ≤ 0
⊢ x ≤ rexp y

pp: case inr
x y : ℝ
h : log x ≤ y
hx : 0 < x
⊢ x ≤ rexp y

Tactic:
·

Goal state after:
case inl
x y : ℝ
h : log x ≤ y
hx : x ≤ 0
⊢ x ≤ rexp y
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: case inr
x y : ℝ
h : log x ≤ y
hx : 0 < x
⊢ x ≤ rexp y

Tactic:
·

Goal state after:
case inr
x y : ℝ
h : log x ≤ y
hx : 0 < x
⊢ x ≤ rexp y
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: case inl
x y : ℝ
h : log x < y
hx : x ≤ 0
⊢ x < rexp y

pp: case inr
x y : ℝ
h : log x < y
hx : 0 < x
⊢ x < rexp y

Tactic:
·

Goal state after:
case inl
x y : ℝ
h : log x < y
hx : x ≤ 0
⊢ x < rexp y
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case pos
z : ℂ
h₀ : z = 0
⊢ z.arg = π / 2 ↔ z.re = 0 ∧ 0 < z.im

pp: case neg
z : ℂ
h₀ : ¬z = 0
⊢ z.arg = π / 2 ↔ z.re = 0 ∧ 0 < z.im

Tactic:
·

Goal state after:
case pos
z : ℂ
h₀ : z = 0
⊢ z.arg = π / 2 ↔ z.re = 0 ∧ 0 < z.im
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: case inr
x y : ℝ
h : log x < y
hx : 0 < x
⊢ x < rexp y

Tactic:
·

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

Goal state before:
pp: case neg.mp
z : ℂ
h₀ : ¬z = 0
⊢ z.arg = π / 2 → z.re = 0 ∧ 0 < z.im

pp: case neg.mpr
z : ℂ
h₀ : ¬z = 0
⊢ z.re = 0 ∧ 0 < z.im → z.arg = π / 2

Tactic:
·

Goal state after:
case neg.mp
z : ℂ
h₀ : ¬z = 0
⊢ z.arg = π / 2 → z.re = 0 ∧ 0 < z.im
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: case inl
hx : 0 ≤ 0
⊢ 0 < log 0 ↔ 1 < 0

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

Tactic:
·

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

Goal state before:
pp: case neg.mpr
z : ℂ
h₀ : ¬z = 0
⊢ z.re = 0 ∧ 0 < z.im → z.arg = π / 2

Tactic:
·

Goal state after:
case neg.mpr
z : ℂ
h₀ : ¬z = 0
⊢ z.re = 0 ∧ 0 < z.im → z.arg = π / 2
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case pos
z : ℂ
h₀ : z = 0
⊢ z.arg = -(π / 2) ↔ z.re = 0 ∧ z.im < 0

pp: case neg
z : ℂ
h₀ : ¬z = 0
⊢ z.arg = -(π / 2) ↔ z.re = 0 ∧ z.im < 0

Tactic:
·

Goal state after:
case pos
z : ℂ
h₀ : z = 0
⊢ z.arg = -(π / 2) ↔ z.re = 0 ∧ z.im < 0
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: case inl
hx : 0 ≤ 0
⊢ log 0 ≤ 0 ↔ 0 ≤ 1

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

Tactic:
·

Goal state after:
case inl
hx : 0 ≤ 0
⊢ log 0 ≤ 0 ↔ 0 ≤ 1
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case neg.mp
z : ℂ
h₀ : ¬z = 0
⊢ z.arg = -(π / 2) → z.re = 0 ∧ z.im < 0

pp: case neg.mpr
z : ℂ
h₀ : ¬z = 0
⊢ z.re = 0 ∧ z.im < 0 → z.arg = -(π / 2)

Tactic:
·

Goal state after:
case neg.mp
z : ℂ
h₀ : ¬z = 0
⊢ z.arg = -(π / 2) → z.re = 0 ∧ z.im < 0
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case neg.mpr
z : ℂ
h₀ : ¬z = 0
⊢ z.re = 0 ∧ z.im < 0 → z.arg = -(π / 2)

Tactic:
·

Goal state after:
case neg.mpr
z : ℂ
h₀ : ¬z = 0
⊢ z.re = 0 ∧ z.im < 0 → z.arg = -(π / 2)
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: case mp
x : ℝ
⊢ log x = 0 → x = 0 ∨ x = 1 ∨ x = -1

pp: case mpr
x : ℝ
⊢ x = 0 ∨ x = 1 ∨ x = -1 → log x = 0

Tactic:
·

Goal state after:
case mp
x : ℝ
⊢ log x = 0 → x = 0 ∨ x = 1 ∨ x = -1