mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: case snoc.snoc
X : Type u_1
inst✝ : TopologicalSpace X
n✝ : ℕ
s : Set X
h : IsPathConnected s
n : ℕ
p : Fin n → X
y : X
hp₂ : ∀ (x : X), (∀ (i : Fin n), p i ∈ s) → x ∈ s → ∃ γ, range ⇑γ ⊆ s ∧ ∀ (i : Fin n), p i ∈ range ⇑γ
x : X
hx : x ∈ s
hp : ∀ (i : Fin n), p i ∈ s
hy : y ∈ s
⊢ ∃ γ, range ⇑γ ⊆ s ∧ (∀ (i : Fin n), p i ∈ range ⇑γ) ∧ y ∈ range ⇑γ

Tactic:
specialize hp₂ y hp hy

Goal state after:
case snoc.snoc
X : Type u_1
inst✝ : TopologicalSpace X
n✝ : ℕ
s : Set X
h : IsPathConnected s
n : ℕ
p : Fin n → X
y : X
hp₂ : ∃ γ, range ⇑γ ⊆ s ∧ ∀ (i : Fin n), p i ∈ range ⇑γ
x : X
hx : x ∈ s
hp : ∀ (i : Fin n), p i ∈ s
hy : y ∈ s
⊢ ∃ γ, range ⇑γ ⊆ s ∧ (∀ (i : Fin n), p i ∈ range ⇑γ) ∧ y ∈ range ⇑γ
Module: Mathlib.Topology.Path

Goal state before:
pp: case pos
X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
γ : Path x y
γ' : Path y z
t : ↑I
h✝ : ↑t ≤ 1 / 2
⊢ γ.extend (2 * ↑t) = γ ⟨2 * ↑t, ⋯⟩

pp: case neg
X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
γ : Path x y
γ' : Path y z
t : ↑I
h✝ : ¬↑t ≤ 1 / 2
⊢ γ'.extend (2 * ↑t - 1) = γ' ⟨2 * ↑t - 1, ⋯⟩

Tactic:
<;>

Goal state after:
case pos
X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
γ : Path x y
γ' : Path y z
t : ↑I
h✝ : ↑t ≤ 1 / 2
⊢ γ.extend (2 * ↑t) = γ ⟨2 * ↑t, ⋯⟩

case neg
X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
γ : Path x y
γ' : Path y z
t : ↑I
h✝ : ¬↑t ≤ 1 / 2
⊢ γ'.extend (2 * ↑t - 1) = γ' ⟨2 * ↑t - 1, ⋯⟩
Module: Mathlib.Topology.Path

Goal state before:
pp: case pos
X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
γ : Path x y
γ' : Path y z
t : ↑I
h : ↑(σ t) ≤ 1 / 2
h₁ : ↑t ≤ 1 / 2
⊢ γ ⟨2 * ↑(σ t), ⋯⟩ = γ' (σ ⟨2 * ↑t, ⋯⟩)

pp: case neg
X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
γ : Path x y
γ' : Path y z
t : ↑I
h : ↑(σ t) ≤ 1 / 2
h₁ : ¬↑t ≤ 1 / 2
⊢ γ ⟨2 * ↑(σ t), ⋯⟩ = γ (σ ⟨2 * ↑t - 1, ⋯⟩)

pp: case pos
X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
γ : Path x y
γ' : Path y z
t : ↑I
h : ¬↑(σ t) ≤ 1 / 2
h₂ : ↑t ≤ 1 / 2
⊢ γ' ⟨2 * ↑(σ t) - 1, ⋯⟩ = γ' (σ ⟨2 * ↑t, ⋯⟩)

pp: case neg
X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
γ : Path x y
γ' : Path y z
t : ↑I
h : ¬↑(σ t) ≤ 1 / 2
h₂ : ¬↑t ≤ 1 / 2
⊢ γ' ⟨2 * ↑(σ t) - 1, ⋯⟩ = γ (σ ⟨2 * ↑t - 1, ⋯⟩)

Tactic:
<;>

Goal state after:
case pos
X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
γ : Path x y
γ' : Path y z
t : ↑I
h : ↑(σ t) ≤ 1 / 2
h₁ : ↑t ≤ 1 / 2
⊢ γ ⟨2 * ↑(σ t), ⋯⟩ = γ' (σ ⟨2 * ↑t, ⋯⟩)

case neg
X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
γ : Path x y
γ' : Path y z
t : ↑I
h : ↑(σ t) ≤ 1 / 2
h₁ : ¬↑t ≤ 1 / 2
⊢ γ ⟨2 * ↑(σ t), ⋯⟩ = γ (σ ⟨2 * ↑t - 1, ⋯⟩)

case pos
X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
γ : Path x y
γ' : Path y z
t : ↑I
h : ¬↑(σ t) ≤ 1 / 2
h₂ : ↑t ≤ 1 / 2
⊢ γ' ⟨2 * ↑(σ t) - 1, ⋯⟩ = γ' (σ ⟨2 * ↑t, ⋯⟩)

case neg
X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
γ : Path x y
γ' : Path y z
t : ↑I
h : ¬↑(σ t) ≤ 1 / 2
h₂ : ¬↑t ≤ 1 / 2
⊢ γ' ⟨2 * ↑(σ t) - 1, ⋯⟩ = γ (σ ⟨2 * ↑t - 1, ⋯⟩)
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: case h
X : Type u_1
inst✝ : TopologicalSpace X
n✝ : ℕ
s : Set X
h : IsPathConnected s
n : ℕ
p : Fin n → X
y x : X
hx : x ∈ s
hp : ∀ (i : Fin n), p i ∈ s
hy : y ∈ s
γ₀ : Path (snoc p y 0) y
hγ₀s : range ⇑γ₀ ⊆ s
hγ₀p : ∀ (i : Fin n), p i ∈ range ⇑γ₀
γ₁ : Path y x
hγ₁ : range ⇑γ₁ ⊆ s
⊢ range ⇑(γ₀.trans γ₁) ⊆ s ∧ (∀ (i : Fin n), p i ∈ range ⇑(γ₀.trans γ₁)) ∧ y ∈ range ⇑(γ₀.trans γ₁)

Tactic:
simp only [Path.trans_range, mem_union, Path.source_mem_range, or_true, and_true,
      union_subset_iff]

Goal state after:
case h
X : Type u_1
inst✝ : TopologicalSpace X
n✝ : ℕ
s : Set X
h : IsPathConnected s
n : ℕ
p : Fin n → X
y x : X
hx : x ∈ s
hp : ∀ (i : Fin n), p i ∈ s
hy : y ∈ s
γ₀ : Path (snoc p y 0) y
hγ₀s : range ⇑γ₀ ⊆ s
hγ₀p : ∀ (i : Fin n), p i ∈ range ⇑γ₀
γ₁ : Path y x
hγ₁ : range ⇑γ₁ ⊆ s
⊢ (range ⇑γ₀ ⊆ s ∧ range ⇑γ₁ ⊆ s) ∧ ∀ (i : Fin n), p i ∈ range ⇑γ₀ ∨ p i ∈ range ⇑γ₁
Module: Mathlib.Topology.Instances.ZMultiples

Goal state before:
pp: a : ℝ
⊢ Tendsto (⇑(zmultiples a).subtype) Filter.cofinite (cocompact ℝ)

Tactic:
refine (zmultiples a).tendsto_coe_cofinite_of_discrete ?_

Goal state after:
a : ℝ
⊢ IsDiscrete ↑(zmultiples a)
Module: Mathlib.Topology.Instances.AddCircle.Real

Goal state before:
pp: case hx
N : ℕ
inst✝ : NeZero N
x y : ZMod N
hxy : ↑(↑x.val / ↑N) = ↑(↑y.val / ↑N)
this : 0 < ↑N
⊢ ↑x.val / ↑N ∈ Ico ?m.62 (?m.62 + 1)

pp: case hy
N : ℕ
inst✝ : NeZero N
x y : ZMod N
hxy : ↑(↑x.val / ↑N) = ↑(↑y.val / ↑N)
this : 0 < ↑N
⊢ ↑y.val / ↑N ∈ Ico ?m.62 (?m.62 + 1)

pp: N : ℕ
inst✝ : NeZero N
x y : ZMod N
hxy : ↑(↑x.val / ↑N) = ↑(↑y.val / ↑N)
this : 0 < ↑N
⊢ ℝ

Tactic:
<;>

Goal state after:
case hx
N : ℕ
inst✝ : NeZero N
x y : ZMod N
hxy : ↑(↑x.val / ↑N) = ↑(↑y.val / ↑N)
this : 0 < ↑N
⊢ ↑x.val / ↑N ∈ Ico ?m.62 (?m.62 + 1)

case hy
N : ℕ
inst✝ : NeZero N
x y : ZMod N
hxy : ↑(↑x.val / ↑N) = ↑(↑y.val / ↑N)
this : 0 < ↑N
⊢ ↑y.val / ↑N ∈ Ico ?m.62 (?m.62 + 1)

N : ℕ
inst✝ : NeZero N
x y : ZMod N
hxy : ↑(↑x.val / ↑N) = ↑(↑y.val / ↑N)
this : 0 < ↑N
⊢ ℝ
Module: Mathlib.Analysis.Normed.Group.AddCircle

Goal state before:
pp: p : ℝ
hp : 0 < p
x : ℝ
⊢ ‖↑x‖ = p * |p⁻¹ * x - ↑(round (p⁻¹ * x))|

Tactic:
conv_rhs =>
    congr
    rw [← abs_eq_self.mpr hp.le]

Goal state after:
p : ℝ
hp : 0 < p
x : ℝ
⊢ ‖↑x‖ = |p| * |p⁻¹ * x - ↑(round (p⁻¹ * x))|
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: case pos
n : ℕ
h✝ : Even n
⊢ ‖0‖ ≤ 1

pp: case neg
n : ℕ
h✝ : ¬Even n
⊢ ‖1‖ ≤ 1

Tactic:
<;>

Goal state after:
case pos
n : ℕ
h✝ : Even n
⊢ ‖0‖ ≤ 1

case neg
n : ℕ
h✝ : ¬Even n
⊢ ‖1‖ ≤ 1
Module: Mathlib.Topology.Path

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

Tactic:
have h₄ : 1 ≤ t₀ := le_of_lt (by simpa using h₁)

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

Goal state before:
pp: case pos
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t : ℝ
x : ↑I
hx : ↑x ≤ t
⊢ (γ.truncate t t) x = ((refl (γ.extend t)).cast ⋯ ⋯) x

pp: case neg
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t : ℝ
x : ↑I
hx : ¬↑x ≤ t
⊢ (γ.truncate t t) x = ((refl (γ.extend t)).cast ⋯ ⋯) x

Tactic:
<;>

Goal state after:
case pos
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t : ℝ
x : ↑I
hx : ↑x ≤ t
⊢ (γ.truncate t t) x = ((refl (γ.extend t)).cast ⋯ ⋯) x

case neg
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t : ℝ
x : ↑I
hx : ¬↑x ≤ t
⊢ (γ.truncate t t) x = ((refl (γ.extend t)).cast ⋯ ⋯) x
Module: Mathlib.Topology.Path

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type u_3
γ✝ : Path x y
a b : X
γ : Path a b
⊢ γ.extend (min 1 1) = b

Tactic:
by rw [min_self, γ.extend_one]

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

Goal state before:
pp: case pos
x : ℂ
h✝ : 0 ≤ x.re
⊢ Real.sin (Real.arcsin (x.im / ‖x‖)) = x.im / ‖x‖

pp: case pos
x : ℂ
h✝¹ : ¬0 ≤ x.re
h✝ : 0 ≤ x.im
⊢ Real.sin (Real.arcsin ((-x).im / ‖x‖) + π) = x.im / ‖x‖

pp: case neg
x : ℂ
h✝¹ : ¬0 ≤ x.re
h✝ : ¬0 ≤ x.im
⊢ Real.sin (Real.arcsin ((-x).im / ‖x‖) - π) = x.im / ‖x‖

Tactic:
<;>

Goal state after:
case pos
x : ℂ
h✝ : 0 ≤ x.re
⊢ Real.sin (Real.arcsin (x.im / ‖x‖)) = x.im / ‖x‖

case pos
x : ℂ
h✝¹ : ¬0 ≤ x.re
h✝ : 0 ≤ x.im
⊢ Real.sin (Real.arcsin ((-x).im / ‖x‖) + π) = x.im / ‖x‖

case neg
x : ℂ
h✝¹ : ¬0 ≤ x.re
h✝ : ¬0 ≤ x.im
⊢ Real.sin (Real.arcsin ((-x).im / ‖x‖) - π) = x.im / ‖x‖
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: case left
x : ℝ
this : 0 < π
⊢ -(π / 2) < π / 4

pp: case right
x : ℝ
this : 0 < π
⊢ π / 4 ≤ π / 2

Tactic:
<;>

Goal state after:
case left
x : ℝ
this : 0 < π
⊢ -(π / 2) < π / 4

case right
x : ℝ
this : 0 < π
⊢ π / 4 ≤ π / 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

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

Tactic:
cos_arcsin

Goal state after:
x : ℝ
⊢ sin (arcsin x) / √(1 - x ^ 2) = x / √(1 - x ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case inr.a
x : ℂ
hx : x ≠ 0
this : ‖x‖ ≠ 0
⊢ (↑‖x‖ * cexp (↑x.arg * I)).re = x.re

pp: case inr.a
x : ℂ
hx : x ≠ 0
this : ‖x‖ ≠ 0
⊢ (↑‖x‖ * cexp (↑x.arg * I)).im = x.im

Tactic:
<;>

Goal state after:
case inr.a
x : ℂ
hx : x ≠ 0
this : ‖x‖ ≠ 0
⊢ (↑‖x‖ * cexp (↑x.arg * I)).re = x.re

case inr.a
x : ℂ
hx : x ≠ 0
this : ‖x‖ ≠ 0
⊢ (↑‖x‖ * cexp (↑x.arg * I)).im = x.im
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: x : ℝ
hx₁ : 0 ≤ x
hx₂ : x ≤ π
⊢ π / 2 - (π / 2 - x) = x

pp: case hx₁
x : ℝ
hx₁ : 0 ≤ x
hx₂ : x ≤ π
⊢ -(π / 2) ≤ π / 2 - x

pp: case hx₂
x : ℝ
hx₁ : 0 ≤ x
hx₂ : x ≤ π
⊢ π / 2 - x ≤ π / 2

Tactic:
<;>

Goal state after:
x : ℝ
hx₁ : 0 ≤ x
hx₂ : x ≤ π
⊢ π / 2 - (π / 2 - x) = x

case hx₁
x : ℝ
hx₁ : 0 ≤ x
hx₂ : x ≤ π
⊢ -(π / 2) ≤ π / 2 - x

case hx₂
x : ℝ
hx₁ : 0 ≤ x
hx₂ : x ≤ π
⊢ π / 2 - x ≤ π / 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: case hx₁
x : ℝ
hx₁ : 0 ≤ x
hx₂ : x ≤ π
⊢ x ≤ π

pp: case hx₂
x : ℝ
hx₁ : 0 ≤ x
hx₂ : x ≤ π
⊢ 0 ≤ x

Tactic:
<;>

Goal state after:
case hx₁
x : ℝ
hx₁ : 0 ≤ x
hx₂ : x ≤ π
⊢ x ≤ π

case hx₂
x : ℝ
hx₁ : 0 ≤ x
hx₂ : x ≤ π
⊢ 0 ≤ x
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

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

pp: case refine_2
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
⊢ θ + π < π / 2

Tactic:
<;>

Goal state after:
case refine_1
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
⊢ -(π / 2) < θ + π

case refine_2
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
⊢ θ + π < π / 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

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

Tactic:
cos_arcsin

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

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

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

Tactic:
<;>

Goal state after:
case mp
x : ℝ
⊢ π / 2 - arcsin x ≤ π / 4 → π / 4 ≤ arcsin x

case mpr
x : ℝ
⊢ π / 4 ≤ arcsin x → π / 2 - arcsin x ≤ π / 4
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: case inl
⊢ log (0 / 0) = 0

pp: case inr
x : ℝ
hx : x ≠ 0
⊢ log (x / x) = 0

Tactic:
<;>

Goal state after:
case inl
⊢ log (0 / 0) = 0

case inr
x : ℝ
hx : x ≠ 0
⊢ log (x / x) = 0
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case inl
⊢ (0 / 0).arg = 0

pp: case inr
x : ℂ
hx : x ≠ 0
⊢ (x / x).arg = 0

Tactic:
<;>

Goal state after:
case inl
⊢ (0 / 0).arg = 0

case inr
x : ℂ
hx : x ≠ 0
⊢ (x / x).arg = 0
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: case mpr.inl
⊢ log 0 = 0

pp: case mpr.inr.inl
⊢ log 1 = 0

pp: case mpr.inr.inr
⊢ log (-1) = 0

Tactic:
<;>

Goal state after:
case mpr.inl
⊢ log 0 = 0

case mpr.inr.inl
⊢ log 1 = 0

case mpr.inr.inr
⊢ log (-1) = 0
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case inl
x : ℂ
hr : x.re < 0
⊢ (if 0 ≤ x.re then -Real.arcsin (x.im / ‖x‖)
    else if 0 ≤ -x.im then Real.arcsin (x.im / ‖x‖) + π else Real.arcsin (x.im / ‖x‖) - π) =
    if x.re < 0 ∧ x.im = 0 then π
    else
      -if 0 ≤ x.re then Real.arcsin (x.im / ‖x‖)
        else if 0 ≤ x.im then -Real.arcsin (x.im / ‖x‖) + π else -Real.arcsin (x.im / ‖x‖) - π

pp: case inr.inl
x : ℂ
hr : x.re = 0
⊢ (if 0 ≤ x.re then -Real.arcsin (x.im / ‖x‖)
    else if 0 ≤ -x.im then Real.arcsin (x.im / ‖x‖) + π else Real.arcsin (x.im / ‖x‖) - π) =
    if x.re < 0 ∧ x.im = 0 then π
    else
      -if 0 ≤ x.re then Real.arcsin (x.im / ‖x‖)
        else if 0 ≤ x.im then -Real.arcsin (x.im / ‖x‖) + π else -Real.arcsin (x.im / ‖x‖) - π

pp: case inr.inr
x : ℂ
hr : 0 < x.re
⊢ (if 0 ≤ x.re then -Real.arcsin (x.im / ‖x‖)
    else if 0 ≤ -x.im then Real.arcsin (x.im / ‖x‖) + π else Real.arcsin (x.im / ‖x‖) - π) =
    if x.re < 0 ∧ x.im = 0 then π
    else
      -if 0 ≤ x.re then Real.arcsin (x.im / ‖x‖)
        else if 0 ≤ x.im then -Real.arcsin (x.im / ‖x‖) + π else -Real.arcsin (x.im / ‖x‖) - π

Tactic:
<;>

Goal state after:
case inl
x : ℂ
hr : x.re < 0
⊢ (if 0 ≤ x.re then -Real.arcsin (x.im / ‖x‖)
    else if 0 ≤ -x.im then Real.arcsin (x.im / ‖x‖) + π else Real.arcsin (x.im / ‖x‖) - π) =
    if x.re < 0 ∧ x.im = 0 then π
    else
      -if 0 ≤ x.re then Real.arcsin (x.im / ‖x‖)
        else if 0 ≤ x.im then -Real.arcsin (x.im / ‖x‖) + π else -Real.arcsin (x.im / ‖x‖) - π

case inr.inl
x : ℂ
hr : x.re = 0
⊢ (if 0 ≤ x.re then -Real.arcsin (x.im / ‖x‖)
    else if 0 ≤ -x.im then Real.arcsin (x.im / ‖x‖) + π else Real.arcsin (x.im / ‖x‖) - π) =
    if x.re < 0 ∧ x.im = 0 then π
    else
      -if 0 ≤ x.re then Real.arcsin (x.im / ‖x‖)
        else if 0 ≤ x.im then -Real.arcsin (x.im / ‖x‖) + π else -Real.arcsin (x.im / ‖x‖) - π

case inr.inr
x : ℂ
hr : 0 < x.re
⊢ (if 0 ≤ x.re then -Real.arcsin (x.im / ‖x‖)
    else if 0 ≤ -x.im then Real.arcsin (x.im / ‖x‖) + π else Real.arcsin (x.im / ‖x‖) - π) =
    if x.re < 0 ∧ x.im = 0 then π
    else
      -if 0 ≤ x.re then Real.arcsin (x.im / ‖x‖)
        else if 0 ≤ x.im then -Real.arcsin (x.im / ‖x‖) + π else -Real.arcsin (x.im / ‖x‖) - π
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: x : ℝ
⊢ ContinuousAt log x ↔ x ≠ 0

Tactic:
refine ⟨?_, continuousAt_log⟩
  rintro h rfl
  exact not_tendsto_nhds_of_tendsto_atBot tendsto_log_nhdsNE_zero _ <|
    h.tendsto.mono_left nhdsWithin_le_nhds

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

Goal state before:
pp: case e'_1.e'_3
θ : Angle
⊢ 0 = 2 • 0

pp: case e'_2.e'_2
θ : Angle
⊢ ↑π = 0 + ↑π

Tactic:
<;>

Goal state after:
case e'_1.e'_3
θ : Angle
⊢ 0 = 2 • 0

case e'_2.e'_2
θ : Angle
⊢ ↑π = 0 + ↑π
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: x : ℂ
h : x ∈ slitPlane
⊢ ContinuousAt log x

Tactic:
refine ContinuousAt.add ?_ ?_
  · refine continuous_ofReal.continuousAt.comp ?_
    refine (Real.continuousAt_log ?_).comp continuous_norm.continuousAt
    exact norm_ne_zero_iff.mpr <| slitPlane_ne_zero h
  · have h_cont_mul : Continuous fun x : ℂ => x * I := by fun_prop
    refine h_cont_mul.continuousAt.comp (continuous_ofReal.continuousAt.comp ?_)
    exact continuousAt_arg h

Goal state after:
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 ≠ 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.Pow.Complex

Goal state before:
pp: case pos
x y : ℂ
h✝¹ : x = 0
h✝ : y = 0
⊢ 1 = 0 ↔ x = 0 ∧ y ≠ 0

pp: case neg
x y : ℂ
h✝¹ : x = 0
h✝ : ¬y = 0
⊢ 0 = 0 ↔ x = 0 ∧ y ≠ 0

pp: case neg
x y : ℂ
h✝ : ¬x = 0
⊢ cexp (log x * y) = 0 ↔ x = 0 ∧ y ≠ 0

Tactic:
<;>

Goal state after:
case pos
x y : ℂ
h✝¹ : x = 0
h✝ : y = 0
⊢ 1 = 0 ↔ x = 0 ∧ y ≠ 0

case neg
x y : ℂ
h✝¹ : x = 0
h✝ : ¬y = 0
⊢ 0 = 0 ↔ x = 0 ∧ y ≠ 0

case neg
x y : ℂ
h✝ : ¬x = 0
⊢ cexp (log x * y) = 0 ↔ x = 0 ∧ y ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex

Goal state before:
pp: case pos
x : ℂ
h✝¹ : 1 = 0
h✝ : x = 0
⊢ 1 = 1

pp: case neg
x : ℂ
h✝¹ : 1 = 0
h✝ : ¬x = 0
⊢ 0 = 1

pp: case neg
x : ℂ
h✝ : ¬1 = 0
⊢ cexp (log 1 * x) = 1

Tactic:
<;>

Goal state after:
case pos
x : ℂ
h✝¹ : 1 = 0
h✝ : x = 0
⊢ 1 = 1

case neg
x : ℂ
h✝¹ : 1 = 0
h✝ : ¬x = 0
⊢ 0 = 1

case neg
x : ℂ
h✝ : ¬1 = 0
⊢ cexp (log 1 * x) = 1
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

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

Tactic:
rw [← sub_eq_zero, cos_sub_cos, H, mul_assoc 2 π k, mul_div_cancel_left₀ _ (two_ne_zero' ℝ),
        mul_comm π _, sin_int_mul_pi, mul_zero]

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

Goal state before:
pp: case pos
x y : ℂ
h✝¹ : x = 0
h✝ : y = 0
⊢ 1 = 1⁻¹

pp: case neg
x y : ℂ
h✝¹ : x = 0
h✝ : ¬y = 0
⊢ 0 = 0⁻¹

pp: case neg
x y : ℂ
h✝ : ¬x = 0
⊢ cexp (-(log x * y)) = (cexp (log x * y))⁻¹

Tactic:
<;>

Goal state after:
case pos
x y : ℂ
h✝¹ : x = 0
h✝ : y = 0
⊢ 1 = 1⁻¹

case neg
x y : ℂ
h✝¹ : x = 0
h✝ : ¬y = 0
⊢ 0 = 0⁻¹

case neg
x y : ℂ
h✝ : ¬x = 0
⊢ cexp (-(log x * y)) = (cexp (log x * y))⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex

Goal state before:
pp: case inl.inr.inl
n : ℤ
hn : n ≠ 0
⊢ 0 ^ (↑n * 0) = (0 ^ 0) ^ n

pp: case inl.inr.inr
n : ℤ
y : ℂ
hn : n ≠ 0
hy : y ≠ 0
⊢ 0 ^ (↑n * y) = (0 ^ y) ^ n

Tactic:
<;>

Goal state after:
case inl.inr.inl
n : ℤ
hn : n ≠ 0
⊢ 0 ^ (↑n * 0) = (0 ^ 0) ^ n

case inl.inr.inr
n : ℤ
y : ℂ
hn : n ≠ 0
hy : y ≠ 0
⊢ 0 ^ (↑n * y) = (0 ^ y) ^ n
Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex

Goal state before:
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.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 e ≠ 0

Tactic:
by
    rw [eq, invOf_eq_inv, ← div_eq_mul_inv]
    have h₁' : 0 < (n : ℝ) / d := by
      simpa using (Rat.cast_pos (K := ℝ)).2 (of_decide_eq_true h₁)
    have h₂' : (n : ℝ) / d < 1 := by
      simpa using (Rat.cast_lt (K := ℝ)).2 (of_decide_eq_true h₂)
    exact ne_of_lt <| Real.log_neg h₁' h₂'

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

Goal state before:
pp: case pos
x : ℂ
h✝ : x.arg = π
⊢ |π| = |x.arg|

pp: case neg
x : ℂ
h✝ : ¬x.arg = π
⊢ |(-x.arg)| = |x.arg|

Tactic:
<;>

Goal state after:
case pos
x : ℂ
h✝ : x.arg = π
⊢ |π| = |x.arg|

case neg
x : ℂ
h✝ : ¬x.arg = π
⊢ |(-x.arg)| = |x.arg|
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

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

Tactic:
rw [lt_iff_le_and_ne, arg_le_pi_div_two_iff, Ne, arg_eq_pi_div_two_iff]
  rcases lt_trichotomy z.re 0 with hre | hre | hre
  · have : z ≠ 0 := by simp [Complex.ext_iff, hre.ne]
    simp [hre.ne, hre.not_ge, hre.not_gt, this]
  · have : z = 0 ↔ z.im = 0 := by simp [Complex.ext_iff, hre]
    simp [hre, this, or_comm, le_iff_eq_or_lt]
  · simp [hre, hre.le, hre.ne']

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

Goal state before:
pp: case pos
x : ℂ
h : x.arg = π
⊢ ↑((starRingEnd ℂ) x).arg = -↑x.arg

pp: case neg
x : ℂ
h : ¬x.arg = π
⊢ ↑((starRingEnd ℂ) x).arg = -↑x.arg

Tactic:
<;>

Goal state after:
case pos
x : ℂ
h : x.arg = π
⊢ ↑((starRingEnd ℂ) x).arg = -↑x.arg

case neg
x : ℂ
h : ¬x.arg = π
⊢ ↑((starRingEnd ℂ) x).arg = -↑x.arg
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case pos
x : ℂ
h : x.arg = π
⊢ ↑x⁻¹.arg = -↑x.arg

pp: case neg
x : ℂ
h : ¬x.arg = π
⊢ ↑x⁻¹.arg = -↑x.arg

Tactic:
<;>

Goal state after:
case pos
x : ℂ
h : x.arg = π
⊢ ↑x⁻¹.arg = -↑x.arg

case neg
x : ℂ
h : ¬x.arg = π
⊢ ↑x⁻¹.arg = -↑x.arg
Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex

Goal state before:
pp: case pos
x n : ℂ
hx : x = 0
hn : n = 0
ha : x.arg = π
⊢ 1 = 1

pp: case neg
x n : ℂ
hx : x = 0
hn : n = 0
ha : ¬x.arg = π
⊢ 1 = 1

pp: case pos
x n : ℂ
hx : x = 0
hn : ¬n = 0
ha : x.arg = π
⊢ 0 = 0

pp: case neg
x n : ℂ
hx : x = 0
hn : ¬n = 0
ha : ¬x.arg = π
⊢ 0 = 0

pp: case pos
x n : ℂ
hx : ¬x = 0
h✝ : x.arg = π
⊢ (cexp ((starRingEnd ℂ) (log x) * n))⁻¹ = (cexp ((starRingEnd ℂ) (log x) * n))⁻¹

pp: case neg
x n : ℂ
hx : ¬x = 0
h✝ : ¬x.arg = π
⊢ (cexp (log x * n))⁻¹ = (cexp (log x * n))⁻¹

Tactic:
<;>

Goal state after:
case pos
x n : ℂ
hx : x = 0
hn : n = 0
ha : x.arg = π
⊢ 1 = 1

case neg
x n : ℂ
hx : x = 0
hn : n = 0
ha : ¬x.arg = π
⊢ 1 = 1

case pos
x n : ℂ
hx : x = 0
hn : ¬n = 0
ha : x.arg = π
⊢ 0 = 0

case neg
x n : ℂ
hx : x = 0
hn : ¬n = 0
ha : ¬x.arg = π
⊢ 0 = 0

case pos
x n : ℂ
hx : ¬x = 0
h✝ : x.arg = π
⊢ (cexp ((starRingEnd ℂ) (log x) * n))⁻¹ = (cexp ((starRingEnd ℂ) (log x) * n))⁻¹

case neg
x n : ℂ
hx : ¬x = 0
h✝ : ¬x.arg = π
⊢ (cexp (log x * n))⁻¹ = (cexp (log x * n))⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case left
⊢ -π < π / 2

pp: case right
⊢ π / 2 ≤ π

Tactic:
<;>

Goal state after:
case left
⊢ -π < π / 2

case right
⊢ π / 2 ≤ π
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case left
⊢ -π < -π / 2

pp: case right
⊢ -π / 2 ≤ π

Tactic:
<;>

Goal state after:
case left
⊢ -π < -π / 2

case right
⊢ -π / 2 ≤ π
Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex

Goal state before:
pp: case pos
x n : ℂ
hcx : x = 0
hn : n = 0
hx : x.arg = π
⊢ 1 = 1

pp: case neg
x n : ℂ
hcx : x = 0
hn : n = 0
hx : ¬x.arg = π
⊢ 1 = 1

pp: case pos
x n : ℂ
hcx : x = 0
hn : ¬n = 0
h✝ : x.arg = π
⊢ 0 = 0

pp: case neg
x n : ℂ
hcx : x = 0
hn : ¬n = 0
h✝ : ¬x.arg = π
⊢ 0 = 0

pp: case pos
x n : ℂ
hcx : ¬x = 0
h✝ : x.arg = π
⊢ cexp (log x * n) = cexp (log x * n)

pp: case neg
x n : ℂ
hcx : ¬x = 0
h✝ : ¬x.arg = π
⊢ cexp ((starRingEnd ℂ) (log x) * n) = cexp ((starRingEnd ℂ) (log x) * n)

Tactic:
<;>

Goal state after:
case pos
x n : ℂ
hcx : x = 0
hn : n = 0
hx : x.arg = π
⊢ 1 = 1

case neg
x n : ℂ
hcx : x = 0
hn : n = 0
hx : ¬x.arg = π
⊢ 1 = 1

case pos
x n : ℂ
hcx : x = 0
hn : ¬n = 0
h✝ : x.arg = π
⊢ 0 = 0

case neg
x n : ℂ
hcx : x = 0
hn : ¬n = 0
h✝ : ¬x.arg = π
⊢ 0 = 0

case pos
x n : ℂ
hcx : ¬x = 0
h✝ : x.arg = π
⊢ cexp (log x * n) = cexp (log x * n)

case neg
x n : ℂ
hcx : ¬x = 0
h✝ : ¬x.arg = π
⊢ cexp ((starRingEnd ℂ) (log x) * n) = cexp ((starRingEnd ℂ) (log x) * n)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case e'_1
θ : ℝ
⊢ 2 = 2 * ↑1

pp: case e'_2.e'_3
θ : ℝ
⊢ π = (2 * ↑1 - 1) * π

pp: case e'_2.e'_4
θ : ℝ
⊢ 3 = 2 * ↑1 + 1

Tactic:
<;>

Goal state after:
case e'_1
θ : ℝ
⊢ 2 = 2 * ↑1

case e'_2.e'_3
θ : ℝ
⊢ π = (2 * ↑1 - 1) * π

case e'_2.e'_4
θ : ℝ
⊢ 3 = 2 * ↑1 + 1
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case e'_1
θ : ℝ
⊢ θ + 2 * π = θ - 2 * ↑(-1) * π

pp: case e'_2
θ : ℝ
⊢ Set.Ioc (-3 * π) (-π) = Set.Ioc ((2 * ↑(-1) - 1) * π) ((2 * ↑(-1) + 1) * π)

Tactic:
<;>

Goal state after:
case e'_1
θ : ℝ
⊢ θ + 2 * π = θ - 2 * ↑(-1) * π

case e'_2
θ : ℝ
⊢ Set.Ioc (-3 * π) (-π) = Set.Ioc ((2 * ↑(-1) - 1) * π) ((2 * ↑(-1) + 1) * π)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case pos
n : ℕ
n0 : n = 0
⊢ ↑(0 ^ n).arg = n • ↑(arg 0)

pp: case neg
n : ℕ
n0 : ¬n = 0
⊢ ↑(0 ^ n).arg = n • ↑(arg 0)

Tactic:
<;>

Goal state after:
case pos
n : ℕ
n0 : n = 0
⊢ ↑(0 ^ n).arg = n • ↑(arg 0)

case neg
n : ℕ
n0 : ¬n = 0
⊢ ↑(0 ^ n).arg = n • ↑(arg 0)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case inl
ψ : Angle
⊢ |(↑(π / 2) - ψ).cos| = |ψ.sin|

pp: case inr
ψ : Angle
⊢ |(↑(π / 2) - ψ + ↑π).cos| = |ψ.sin|

Tactic:
<;>

Goal state after:
case inl
ψ : Angle
⊢ |(↑(π / 2) - ψ).cos| = |ψ.sin|

case inr
ψ : Angle
⊢ |(↑(π / 2) - ψ + ↑π).cos| = |ψ.sin|