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

Goal state before:
pp: case inr
E : Type u
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℂ F
inst✝¹ : Nontrivial E
inst✝ : FiniteDimensional ℂ E
f : E → F
U : Set E
hb : Bornology.IsBounded U
hne : U.Nonempty
hd : DiffContOnCl ℂ f U
hc : IsCompact (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U)
w : E
hle : IsMaxOn (norm ∘ f) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U) w
hwU : w ∈ frontier U
⊢ ∃ z ∈ frontier U, IsMaxOn (norm ∘ f) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U) z

pp: case inl
E : Type u
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℂ F
inst✝¹ : Nontrivial E
inst✝ : FiniteDimensional ℂ E
f : E → F
U : Set E
hb : Bornology.IsBounded U
hne : U.Nonempty
hd : DiffContOnCl ℂ f U
hc : IsCompact (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U)
w : E
hle : IsMaxOn (norm ∘ f) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U) w
hwU : w ∈ interior U
⊢ ∃ z ∈ frontier U, IsMaxOn (norm ∘ f) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U) z

Tactic:
;

Goal state after:
case inr
E : Type u
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℂ F
inst✝¹ : Nontrivial E
inst✝ : FiniteDimensional ℂ E
f : E → F
U : Set E
hb : Bornology.IsBounded U
hne : U.Nonempty
hd : DiffContOnCl ℂ f U
hc : IsCompact (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U)
w : E
hle : IsMaxOn (norm ∘ f) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U) w
hwU : w ∈ frontier U
⊢ ∃ z ∈ frontier U, IsMaxOn (norm ∘ f) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U) z

case inl
E : Type u
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℂ F
inst✝¹ : Nontrivial E
inst✝ : FiniteDimensional ℂ E
f : E → F
U : Set E
hb : Bornology.IsBounded U
hne : U.Nonempty
hd : DiffContOnCl ℂ f U
hc : IsCompact (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U)
w : E
hle : IsMaxOn (norm ∘ f) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U) w
hwU : w ∈ interior U
⊢ ∃ z ∈ frontier U, IsMaxOn (norm ∘ f) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U) z
Module: Mathlib.Analysis.Complex.AbsMax

Goal state before:
pp: case inl
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f : E → F
U : Set E
hU : Bornology.IsBounded U
hd : DiffContOnCl ℂ f U
C : ℝ
hC : ∀ z ∈ frontier U, ‖f z‖ ≤ C
z : E
hz : z ∈ frontier U
⊢ ‖f z‖ ≤ C

pp: case inr
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f : E → F
U : Set E
hU : Bornology.IsBounded U
hd : DiffContOnCl ℂ f U
C : ℝ
hC : ∀ z ∈ frontier U, ‖f z‖ ≤ C
z : E
hz : z ∈ U
⊢ ‖f z‖ ≤ C

Tactic:
;

Goal state after:
case inl
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f : E → F
U : Set E
hU : Bornology.IsBounded U
hd : DiffContOnCl ℂ f U
C : ℝ
hC : ∀ z ∈ frontier U, ‖f z‖ ≤ C
z : E
hz : z ∈ frontier U
⊢ ‖f z‖ ≤ C

case inr
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f : E → F
U : Set E
hU : Bornology.IsBounded U
hd : DiffContOnCl ℂ f U
C : ℝ
hC : ∀ z ∈ frontier U, ‖f z‖ ≤ C
z : E
hz : z ∈ U
⊢ ‖f z‖ ≤ C
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.ComplexDeriv

Goal state before:
pp: x : ℂ
hx : cos x = 0
h : sin x = 0
⊢ False

Tactic:
simpa [*, sq] using sin_sq_add_cos_sq x

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

Goal state before:
pp: this : ContinuousOn (fun x ↦ sin x / cos x) {x | cos x ≠ 0}
x : ℝ
⊢ sin x / cos x = tan x

Tactic:
;

Goal state after:
this : ContinuousOn (fun x ↦ sin x / cos x) {x | cos x ≠ 0}
x : ℝ
⊢ sin x / cos x = tan x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: this : -(π / 2) < π / 2
⊢ Tendsto tan (𝓝[>] (-(π / 2))) atBot

Tactic:
;

Goal state after:
this : -(π / 2) < π / 2
⊢ Tendsto tan (𝓝[>] (-(π / 2))) atBot
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: this : -(π / 2) < π / 2
⊢ Tendsto tan (𝓝[<] (π / 2)) atTop

Tactic:
;

Goal state after:
this : -(π / 2) < π / 2
⊢ Tendsto tan (𝓝[<] (π / 2)) atTop
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: x : ℝ
h : x ∈ Ioo (↑(Int.negSucc 0)) 1
⊢ arcsin x = arcsin (x / √(1 - x ^ 2) / √(1 + x ^ 2 / (1 - x ^ 2)))

pp: x : ℝ
h : x ∈ Ioo (↑(Int.negSucc 0)) 1
⊢ 0 ≤ 1 - x ^ 2

Tactic:
one_add_div

Goal state after:
x : ℝ
h : x ∈ Ioo (↑(Int.negSucc 0)) 1
⊢ arcsin x = arcsin (x / √(1 - x ^ 2) / √((1 - x ^ 2 + x ^ 2) / (1 - x ^ 2)))

x : ℝ
h : x ∈ Ioo (↑(Int.negSucc 0)) 1
⊢ 1 - x ^ 2 ≠ 0

x : ℝ
h : x ∈ Ioo (↑(Int.negSucc 0)) 1
⊢ 0 ≤ 1 - x ^ 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: x : ℝ
h : 0 ≤ x
⊢ arcsin (x / √(1 + x ^ 2)) = arcsin √(1 - (√(1 + x ^ 2))⁻¹ ^ 2)

pp: x : ℝ
h : 0 ≤ x
⊢ 0 ≤ (√(1 + x ^ 2))⁻¹

Tactic:
;

Goal state after:
x : ℝ
h : 0 ≤ x
⊢ arcsin (x / √(1 + x ^ 2)) = arcsin √(1 - (√(1 + x ^ 2))⁻¹ ^ 2)

x : ℝ
h : 0 ≤ x
⊢ 0 ≤ (√(1 + x ^ 2))⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: x : ℝ
h : 0 ≤ x
⊢ 0 ≤ (√(1 + x ^ 2))⁻¹

pp: x : ℝ
h : 0 ≤ x
⊢ arcsin (x / √(1 + x ^ 2)) = arcsin √(1 - (√(1 + x ^ 2))⁻¹ ^ 2)

Tactic:
;

Goal state after:
x : ℝ
h : 0 ≤ x
⊢ 0 ≤ (√(1 + x ^ 2))⁻¹

x : ℝ
h : 0 ≤ x
⊢ arcsin (x / √(1 + x ^ 2)) = arcsin √(1 - (√(1 + x ^ 2))⁻¹ ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: x : ℝ
k : ℤ
h : arctan x = (2 * ↑k + 1) * π / 2
lb : Int.negSucc 0 < 2 * k + 1
ub : 2 * k + 1 < 1
⊢ False

Tactic:
;

Goal state after:
x : ℝ
k : ℤ
h : arctan x = (2 * ↑k + 1) * π / 2
lb : Int.negSucc 0 < 2 * k + 1
ub : 2 * k + 1 < 1
⊢ False
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: x : ℝ
k : ℤ
h : arctan x = (2 * ↑k + 1) * π / 2
ub : 2 * k + 1 < 1
lb : -1 < 2 * k + 1
⊢ False

Tactic:
;

Goal state after:
x : ℝ
k : ℤ
h : arctan x = (2 * ↑k + 1) * π / 2
ub : 2 * k + 1 < 1
lb : -1 < 2 * k + 1
⊢ False
Module: Mathlib.Analysis.Convex.Deriv

Goal state before:
pp: case inl
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
x : ℝ
hxs hys : x ∈ interior S
hxy : x ≤ x
⊢ (fun x ↦ derivWithin f (Ioi x) x) x ≤ (fun x ↦ derivWithin f (Ioi x) x) x

pp: case inr
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
x : ℝ
hxs : x ∈ interior S
y : ℝ
hys : y ∈ interior S
hxy✝ : x ≤ y
hxy : x < y
⊢ (fun x ↦ derivWithin f (Ioi x) x) x ≤ (fun x ↦ derivWithin f (Ioi x) x) y

Tactic:
;

Goal state after:
case inl
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
x : ℝ
hxs hys : x ∈ interior S
hxy : x ≤ x
⊢ (fun x ↦ derivWithin f (Ioi x) x) x ≤ (fun x ↦ derivWithin f (Ioi x) x) x

case inr
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
x : ℝ
hxs : x ∈ interior S
y : ℝ
hys : y ∈ interior S
hxy✝ : x ≤ y
hxy : x < y
⊢ (fun x ↦ derivWithin f (Ioi x) x) x ≤ (fun x ↦ derivWithin f (Ioi x) x) y
Module: Mathlib.Analysis.Convex.Deriv

Goal state before:
pp: S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
x : ℝ
hxs : x ∈ interior S
y : ℝ
hys : y ∈ interior S
hxy✝ : x ≤ y
hxy : x < y
⊢ y ∈ S

Tactic:
;

Goal state after:
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
x : ℝ
hxs : x ∈ interior S
y : ℝ
hys : y ∈ interior S
hxy✝ : x ≤ y
hxy : x < y
⊢ y ∈ S
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: x : ℝ
h₁ : -1 < x
h₂ : x < 1
⊢ arctan ((x + x) / (1 - x * x)) = arctan (2 * x / (1 - x ^ 2))

Tactic:
;

Goal state after:
x : ℝ
h₁ : -1 < x
h₂ : x < 1
⊢ arctan ((x + x) / (1 - x * x)) = arctan (2 * x / (1 - x ^ 2))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: x : ℝ
h₁ : -1 < x
h₂ : x < 1
⊢ (x + x) / (1 - x * x) = 2 * x / (1 - x ^ 2)

Tactic:
;

Goal state after:
x : ℝ
h₁ : -1 < x
h₂ : x < 1
⊢ (x + x) / (1 - x * x) = 2 * x / (1 - x ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: x : ℝ
h : 1 < x
⊢ arctan ((x + x) / (1 - x * x)) + π = arctan (2 * x / (1 - x ^ 2)) + π

Tactic:
;

Goal state after:
x : ℝ
h : 1 < x
⊢ arctan ((x + x) / (1 - x * x)) + π = arctan (2 * x / (1 - x ^ 2)) + π
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: case e_a
x : ℝ
h : 1 < x
⊢ (x + x) / (1 - x * x) = 2 * x / (1 - x ^ 2)

Tactic:
;

Goal state after:
case e_a
x : ℝ
h : 1 < x
⊢ (x + x) / (1 - x * x) = 2 * x / (1 - x ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: x : ℝ
h : x < -1
⊢ arctan ((x + x) / (1 - x * x)) - π = arctan (2 * x / (1 - x ^ 2)) - π

Tactic:
;

Goal state after:
x : ℝ
h : x < -1
⊢ arctan ((x + x) / (1 - x * x)) - π = arctan (2 * x / (1 - x ^ 2)) - π
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: case e_a
x : ℝ
h : x < -1
⊢ (x + x) / (1 - x * x) = 2 * x / (1 - x ^ 2)

Tactic:
;

Goal state after:
case e_a
x : ℝ
h : x < -1
⊢ (x + x) / (1 - x * x) = 2 * x / (1 - x ^ 2)
Module: Mathlib.Analysis.Convex.Deriv

Goal state before:
pp: case inl
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
x : ℝ
hxs hys : x ∈ interior S
hxy : x ≤ x
⊢ (fun x ↦ derivWithin f (Iio x) x) x ≤ (fun x ↦ derivWithin f (Iio x) x) x

pp: case inr
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
x : ℝ
hxs : x ∈ interior S
y : ℝ
hys : y ∈ interior S
hxy✝ : x ≤ y
hxy : x < y
⊢ (fun x ↦ derivWithin f (Iio x) x) x ≤ (fun x ↦ derivWithin f (Iio x) x) y

Tactic:
;

Goal state after:
case inl
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
x : ℝ
hxs hys : x ∈ interior S
hxy : x ≤ x
⊢ (fun x ↦ derivWithin f (Iio x) x) x ≤ (fun x ↦ derivWithin f (Iio x) x) x

case inr
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
x : ℝ
hxs : x ∈ interior S
y : ℝ
hys : y ∈ interior S
hxy✝ : x ≤ y
hxy : x < y
⊢ (fun x ↦ derivWithin f (Iio x) x) x ≤ (fun x ↦ derivWithin f (Iio x) x) y
Module: Mathlib.Analysis.Convex.Deriv

Goal state before:
pp: S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
x : ℝ
hxs : x ∈ interior S
y : ℝ
hys : y ∈ interior S
hxy✝ : x ≤ y
hxy : x < y
⊢ x ∈ S

Tactic:
;

Goal state after:
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
x : ℝ
hxs : x ∈ interior S
y : ℝ
hys : y ∈ interior S
hxy✝ : x ≤ y
hxy : x < y
⊢ x ∈ S
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds

Goal state before:
pp: x : ℝ
⊢ 2 * (|x| / 2) = |x|

Tactic:
;

Goal state after:
x : ℝ
⊢ 2 * (|x| / 2) = |x|
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds

Goal state before:

Tactic:
_ = 2 * |Real.sin (x / 2)| := by simp
    _ ≤ 2 * |x / 2| := (mul_le_mul_iff_of_pos_left zero_lt_two).mpr Real.abs_sin_le_abs
    _ = _ := by rw [abs_div, Nat.abs_ofNat, Real.norm_eq_abs]; ring

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

Goal state before:
pp: x : ℝ
⊢ ↑‖Complex.exp (Complex.I * ↑x) - 1‖₊ ≤ ↑‖x‖₊

Tactic:
;

Goal state after:
x : ℝ
⊢ ↑‖Complex.exp (Complex.I * ↑x) - 1‖₊ ≤ ↑‖x‖₊
Module: Mathlib.Analysis.Complex.Arg

Goal state before:
pp: case pos
x y : ℂ
hx : x = 0
⊢ x = 0 ∨ y = 0 ∨ x.arg = y.arg ↔ ↑(x / y).arg = 0

pp: case neg
x y : ℂ
hx : ¬x = 0
⊢ x = 0 ∨ y = 0 ∨ x.arg = y.arg ↔ ↑(x / y).arg = 0

Tactic:
;

Goal state after:
case pos
x y : ℂ
hx : x = 0
⊢ x = 0 ∨ y = 0 ∨ x.arg = y.arg ↔ ↑(x / y).arg = 0

case neg
x y : ℂ
hx : ¬x = 0
⊢ x = 0 ∨ y = 0 ∨ x.arg = y.arg ↔ ↑(x / y).arg = 0
Module: Mathlib.Analysis.Complex.Arg

Goal state before:
pp: case pos
x y : ℂ
hx : ¬x = 0
hy : y = 0
⊢ x = 0 ∨ y = 0 ∨ x.arg = y.arg ↔ ↑(x / y).arg = 0

pp: case neg
x y : ℂ
hx : ¬x = 0
hy : ¬y = 0
⊢ x = 0 ∨ y = 0 ∨ x.arg = y.arg ↔ ↑(x / y).arg = 0

Tactic:
;

Goal state after:
case pos
x y : ℂ
hx : ¬x = 0
hy : y = 0
⊢ x = 0 ∨ y = 0 ∨ x.arg = y.arg ↔ ↑(x / y).arg = 0

case neg
x y : ℂ
hx : ¬x = 0
hy : ¬y = 0
⊢ x = 0 ∨ y = 0 ∨ x.arg = y.arg ↔ ↑(x / y).arg = 0
Module: Mathlib.Analysis.Complex.Angle

Goal state before:
pp: case h
x y : ℂ
hy : ‖1‖ = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ Real.cos θ ≤ 1 - 2 / π ^ 2 * θ ^ 2

Tactic:
;

Goal state after:
case h
x y : ℂ
hy : ‖1‖ = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ Real.cos θ ≤ 1 - 2 / π ^ 2 * θ ^ 2
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

Goal state before:
pp: case inl
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
y : V
⊢ √((1 - ⟪0, y⟫ / (‖0‖ * ‖y‖) * (⟪0, y⟫ / (‖0‖ * ‖y‖))) * (‖0‖ * ‖y‖) ^ 2) = √(⟪0, 0⟫ * ⟪y, y⟫ - ⟪0, y⟫ * ⟪0, y⟫)

pp: case inr
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
⊢ √((1 - ⟪x, y⟫ / (‖x‖ * ‖y‖) * (⟪x, y⟫ / (‖x‖ * ‖y‖))) * (‖x‖ * ‖y‖) ^ 2) = √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫)

Tactic:
;

Goal state after:
case inl
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
y : V
⊢ √((1 - ⟪0, y⟫ / (‖0‖ * ‖y‖) * (⟪0, y⟫ / (‖0‖ * ‖y‖))) * (‖0‖ * ‖y‖) ^ 2) = √(⟪0, 0⟫ * ⟪y, y⟫ - ⟪0, y⟫ * ⟪0, y⟫)

case inr
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
⊢ √((1 - ⟪x, y⟫ / (‖x‖ * ‖y‖) * (⟪x, y⟫ / (‖x‖ * ‖y‖))) * (‖x‖ * ‖y‖) ^ 2) = √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫)
Module: Mathlib.Analysis.Complex.Angle

Goal state before:
pp: case h
x y : ℂ
hy : ‖1‖ = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ 1 - θ ^ 2 / 2 ≤ Real.cos θ

Tactic:
;

Goal state after:
case h
x y : ℂ
hy : ‖1‖ = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ 1 - θ ^ 2 / 2 ≤ Real.cos θ
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

Goal state before:
pp: case inr.inl
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x : V
hx : x ≠ 0
⊢ √((1 - ⟪x, 0⟫ / (‖x‖ * ‖0‖) * (⟪x, 0⟫ / (‖x‖ * ‖0‖))) * (‖x‖ * ‖0‖) ^ 2) = √(⟪x, x⟫ * ⟪0, 0⟫ - ⟪x, 0⟫ * ⟪x, 0⟫)

pp: case inr.inr
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
⊢ √((1 - ⟪x, y⟫ / (‖x‖ * ‖y‖) * (⟪x, y⟫ / (‖x‖ * ‖y‖))) * (‖x‖ * ‖y‖) ^ 2) = √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫)

Tactic:
;

Goal state after:
case inr.inl
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x : V
hx : x ≠ 0
⊢ √((1 - ⟪x, 0⟫ / (‖x‖ * ‖0‖) * (⟪x, 0⟫ / (‖x‖ * ‖0‖))) * (‖x‖ * ‖0‖) ^ 2) = √(⟪x, x⟫ * ⟪0, 0⟫ - ⟪x, 0⟫ * ⟪x, 0⟫)

case inr.inr
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
⊢ √((1 - ⟪x, y⟫ / (‖x‖ * ‖y‖) * (⟪x, y⟫ / (‖x‖ * ‖y‖))) * (‖x‖ * ‖y‖) ^ 2) = √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫)
Module: Mathlib.Analysis.Complex.Angle

Goal state before:
pp: x y : ℂ
hx : ‖x‖ = 1
hy : ‖y‖ = 1
⊢ 2 / π * angle x y ≤ ‖x - y‖

Tactic:
;

Goal state after:
x y : ℂ
hx : ‖x‖ = 1
hy : ‖y‖ = 1
⊢ 2 / π * angle x y ≤ ‖x - y‖
Module: Mathlib.Analysis.Complex.BorelCaratheodory

Goal state before:
pp: M : ℝ
z w : ℂ
x✝¹ : M ≠ 0
x✝ : 2 * ↑M - z ≠ 0
h : w = z / (2 * ↑M - z)
⊢ z = 2 * ↑M * (z / (2 * ↑M - z)) / (1 + z / (2 * ↑M - z))

Tactic:
;

Goal state after:
M : ℝ
z w : ℂ
x✝¹ : M ≠ 0
x✝ : 2 * ↑M - z ≠ 0
h : w = z / (2 * ↑M - z)
⊢ z = 2 * ↑M * (z / (2 * ↑M - z)) / (1 + z / (2 * ↑M - z))
Module: Mathlib.Analysis.Complex.BorelCaratheodory

Goal state before:
pp: M : ℝ
z w : ℂ
x✝¹ : M ≠ 0
x✝ : 2 * ↑M - z ≠ 0
h : w = z / (2 * ↑M - z)
⊢ z = z * 2 * ↑M / (2 * ↑M - z + z)

Tactic:
;

Goal state after:
M : ℝ
z w : ℂ
x✝¹ : M ≠ 0
x✝ : 2 * ↑M - z ≠ 0
h : w = z / (2 * ↑M - z)
⊢ z = z * 2 * ↑M / (2 * ↑M - z + z)
Module: Mathlib.Analysis.Complex.BorelCaratheodory

Goal state before:
pp: M : ℝ
z w : ℂ
x✝¹ : M ≠ 0
x✝ : 2 * ↑M - z ≠ 0
h : w = z / (2 * ↑M - z)
⊢ z = z * ↑M * (↑M)⁻¹

Tactic:
;

Goal state after:
M : ℝ
z w : ℂ
x✝¹ : M ≠ 0
x✝ : 2 * ↑M - z ≠ 0
h : w = z / (2 * ↑M - z)
⊢ z = z * ↑M * (↑M)⁻¹
Module: Mathlib.Analysis.Complex.BorelCaratheodory

Goal state before:
pp: case h
M : ℝ
z w : ℂ
x✝¹ : M ≠ 0
x✝ : 2 * ↑M - z ≠ 0
h : w = z / (2 * ↑M - z)
⊢ ↑M ≠ 0

Tactic:
;

Goal state after:
case h
M : ℝ
z w : ℂ
x✝¹ : M ≠ 0
x✝ : 2 * ↑M - z ≠ 0
h : w = z / (2 * ↑M - z)
⊢ ↑M ≠ 0
Module: Mathlib.Analysis.Complex.BorelCaratheodory

Goal state before:
pp: case hdb
M : ℝ
w : ℂ
hM : 0 < M
hw : ‖w‖ < 1
⊢ ‖1‖ - ‖w‖ ≤ ‖1 + w‖

Tactic:
;

Goal state after:
case hdb
M : ℝ
w : ℂ
hM : 0 < M
hw : ‖w‖ < 1
⊢ ‖1‖ - ‖w‖ ≤ ‖1 + w‖
Module: Mathlib.Analysis.Complex.BorelCaratheodory

Goal state before:
pp: case hd
f : ℂ → ℂ
M R : ℝ
z : ℂ
hM : 0 < M
hf : DifferentiableOn ℂ f (ball 0 R)
hf₁ : Set.MapsTo f (ball 0 R) {z | z.re ≤ M}
hR : 0 < R
hz : z ∈ ball 0 R
hf₂ : f 0 = 0
w : ℂ := ⋯
hzR : ‖z‖ < R
hwR : ‖f z / (2 * ↑M - f z)‖ ≤ ‖z‖ / R
h_denom : 2 * ↑M - f z ≠ 0
⊢ 0 < 1 - ‖z‖ / R

Tactic:
;

Goal state after:
case hd
f : ℂ → ℂ
M R : ℝ
z : ℂ
hM : 0 < M
hf : DifferentiableOn ℂ f (ball 0 R)
hf₁ : Set.MapsTo f (ball 0 R) {z | z.re ≤ M}
hR : 0 < R
hz : z ∈ ball 0 R
hf₂ : f 0 = 0
w : ℂ := ⋯
hzR : ‖z‖ < R
hwR : ‖f z / (2 * ↑M - f z)‖ ≤ ‖z‖ / R
h_denom : 2 * ↑M - f z ≠ 0
⊢ 0 < 1 - ‖z‖ / R
Module: Mathlib.Analysis.Complex.BorelCaratheodory

Goal state before:
pp: case h
f : ℂ → ℂ
M R : ℝ
z : ℂ
hM : 0 < M
hf : DifferentiableOn ℂ f (ball 0 R)
hf₁ : Set.MapsTo f (ball 0 R) {z | z.re ≤ M}
hR : 0 < R
hz : z ∈ ball 0 R
x : ℂ
hx : x ∈ ball 0 R
⊢ (f x).re ≤ M

Tactic:
;

Goal state after:
case h
f : ℂ → ℂ
M R : ℝ
z : ℂ
hM : 0 < M
hf : DifferentiableOn ℂ f (ball 0 R)
hf₁ : Set.MapsTo f (ball 0 R) {z | z.re ≤ M}
hR : 0 < R
hz : z ∈ ball 0 R
x : ℂ
hx : x ∈ ball 0 R
⊢ (f x).re ≤ M
Module: Mathlib.Analysis.Complex.BorelCaratheodory

Goal state before:
pp: f : ℂ → ℂ
M R : ℝ
z : ℂ
hM : 0 < M
hf : DifferentiableOn ℂ f (ball 0 R)
hf₁ : Set.MapsTo f (ball 0 R) {z | z.re ≤ M}
hR : 0 < R
hz : z ∈ ball 0 R
hfz : ‖f z - f 0‖ ≤ 2 * (M + ‖f 0‖) * ‖z‖ / (R - ‖z‖)
h_denom_ne : R - ‖z‖ ≠ 0
⊢ 2 * (M + ‖f 0‖) * ‖z‖ + ‖f 0‖ * (R - ‖z‖) = 2 * M * ‖z‖ + ‖f 0‖ * (R + ‖z‖)

Tactic:
;

Goal state after:
f : ℂ → ℂ
M R : ℝ
z : ℂ
hM : 0 < M
hf : DifferentiableOn ℂ f (ball 0 R)
hf₁ : Set.MapsTo f (ball 0 R) {z | z.re ≤ M}
hR : 0 < R
hz : z ∈ ball 0 R
hfz : ‖f z - f 0‖ ≤ 2 * (M + ‖f 0‖) * ‖z‖ / (R - ‖z‖)
h_denom_ne : R - ‖z‖ ≠ 0
⊢ 2 * (M + ‖f 0‖) * ‖z‖ + ‖f 0‖ * (R - ‖z‖) = 2 * M * ‖z‖ + ‖f 0‖ * (R + ‖z‖)
Module: Mathlib.Analysis.Complex.CoveringMap

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
n : ℕ
hn : ↑n ≠ 0
x✝ : 𝕜
⊢ x✝ ∈ {x | x ≠ 0} ↔ x✝ ∈ (fun x ↦ x ^ n) ⁻¹' {0}ᶜ

Tactic:
;

Goal state after:
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
n : ℕ
hn : ↑n ≠ 0
x✝ : 𝕜
⊢ x✝ ∈ {x | x ≠ 0} ↔ x✝ ∈ (fun x ↦ x ^ n) ⁻¹' {0}ᶜ
Module: Mathlib.Analysis.Complex.CoveringMap

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
n : ℤ
hn : ↑n ≠ 0
this : ∀ (x : 𝕜), x ^ n = 0 ↔ x = 0
x✝ : 𝕜
⊢ x✝ ∈ (fun x ↦ x ^ n) ⁻¹' {0}ᶜ ↔ x✝ ∈ {0}ᶜ

Tactic:
;

Goal state after:
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
n : ℤ
hn : ↑n ≠ 0
this : ∀ (x : 𝕜), x ^ n = 0 ↔ x = 0
x✝ : 𝕜
⊢ x✝ ∈ (fun x ↦ x ^ n) ⁻¹' {0}ᶜ ↔ x✝ ∈ {0}ᶜ
Module: Mathlib.Analysis.Complex.CoveringMap

Goal state before:
pp: case refine_2.convert_2
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
n : ℤ
hn : ↑n ≠ 0
this : ∀ (x : 𝕜), x ^ n = 0 ↔ x = 0
x✝ : 𝕜
⊢ x✝ ∈ (fun x ↦ x ^ n) ⁻¹' {0}ᶜ ↔ x✝ ∈ fun x ↦ x = 0 → False

Tactic:
;

Goal state after:
case refine_2.convert_2
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
n : ℤ
hn : ↑n ≠ 0
this : ∀ (x : 𝕜), x ^ n = 0 ↔ x = 0
x✝ : 𝕜
⊢ x✝ ∈ (fun x ↦ x ^ n) ⁻¹' {0}ᶜ ↔ x✝ ∈ fun x ↦ x = 0 → False
Module: Mathlib.Analysis.Complex.CoveringMap

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
n : ℕ
hn : ↑n ≠ 0
surj : Function.Surjective fun x ↦ x ^ n
this✝ : NeZero n
this : IsQuotientMap ({0}ᶜ.restrictPreimage fun x ↦ x ^ n)
e : 𝕜ˣ ≃ₜ { g // g ≠ 0 } := unitsHomeomorphNeZero
x✝ : 𝕜ˣ
⊢ x✝ ^ n = ((⇑e.symm ∘ {0}ᶜ.restrictPreimage fun x ↦ x ^ n) ∘ ⇑(e.trans (Homeomorph.ofEqSubtypes ?m.141))) x✝

pp: 𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
n : ℕ
hn : ↑n ≠ 0
surj : Function.Surjective fun x ↦ x ^ n
this✝ : NeZero n
this : IsQuotientMap ({0}ᶜ.restrictPreimage fun x ↦ x ^ n)
e : 𝕜ˣ ≃ₜ { g // g ≠ 0 } := unitsHomeomorphNeZero
⊢ (fun g ↦ g ≠ 0) = fun x ↦ x ∈ (fun x ↦ x ^ n) ⁻¹' {0}ᶜ

Tactic:
· exact (e.left_inv _).symm

Goal state after:
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
n : ℕ
hn : ↑n ≠ 0
surj : Function.Surjective fun x ↦ x ^ n
this✝ : NeZero n
this : IsQuotientMap ({0}ᶜ.restrictPreimage fun x ↦ x ^ n)
e : 𝕜ˣ ≃ₜ { g // g ≠ 0 } := unitsHomeomorphNeZero
⊢ (fun g ↦ g ≠ 0) = fun x ↦ x ∈ (fun x ↦ x ^ n) ⁻¹' {0}ᶜ
Module: Mathlib.Analysis.Complex.CoveringMap

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
n : ℕ
hn : ↑n ≠ 0
surj : Function.Surjective fun x ↦ x ^ n
this✝ : NeZero n
this : IsQuotientMap ({0}ᶜ.restrictPreimage fun x ↦ x ^ n)
e : 𝕜ˣ ≃ₜ { g // g ≠ 0 } := ⋯
x✝ : 𝕜
⊢ x✝ ≠ 0 ↔ x✝ ∈ (fun x ↦ x ^ n) ⁻¹' {0}ᶜ

Tactic:
;

Goal state after:
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
n : ℕ
hn : ↑n ≠ 0
surj : Function.Surjective fun x ↦ x ^ n
this✝ : NeZero n
this : IsQuotientMap ({0}ᶜ.restrictPreimage fun x ↦ x ^ n)
e : 𝕜ˣ ≃ₜ { g // g ≠ 0 } := ⋯
x✝ : 𝕜
⊢ x✝ ≠ 0 ↔ x✝ ∈ (fun x ↦ x ^ n) ⁻¹' {0}ᶜ
Module: Mathlib.Analysis.Complex.CoveringMap

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
n : ℕ
hn : ↑(-↑n) ≠ 0
surj : Function.Surjective fun x ↦ x ^ (-↑n)
x✝ : 𝕜ˣ
⊢ x✝ ∈ (zpowGroupHom (-↑n)).ker ↔ x✝ ∈ (powMonoidHom n).ker

Tactic:
;

Goal state after:
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
n : ℕ
hn : ↑(-↑n) ≠ 0
surj : Function.Surjective fun x ↦ x ^ (-↑n)
x✝ : 𝕜ˣ
⊢ x✝ ∈ (zpowGroupHom (-↑n)).ker ↔ x✝ ∈ (powMonoidHom n).ker
Module: Mathlib.Analysis.Normed.Module.Ball.Action

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CharZero 𝕜
r : ℝ
hr : r ≠ 0
x : ↑(sphere 0 r)
this : IsAddTorsionFree E
h : x = -x
⊢ ↑(-x) = -↑x

Tactic:
;

Goal state after:
𝕜 : Type u_1
E : Type u_3
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CharZero 𝕜
r : ℝ
hr : r ≠ 0
x : ↑(sphere 0 r)
this : IsAddTorsionFree E
h : x = -x
⊢ ↑(-x) = -↑x
Module: Mathlib.Analysis.Complex.CoveringMap

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
n : ℕ
hn : ↑(-↑n) ≠ 0
surj : Function.Surjective fun x ↦ x ^ (-↑n)
x✝ : 𝕜ˣ
⊢ ↑(x✝ ^ (-↑n)) = ↑((⇑(Homeomorph.inv 𝕜ˣ) ∘ fun x ↦ x ^ n) x✝)

Tactic:
;

Goal state after:
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
n : ℕ
hn : ↑(-↑n) ≠ 0
surj : Function.Surjective fun x ↦ x ^ (-↑n)
x✝ : 𝕜ˣ
⊢ ↑(x✝ ^ (-↑n)) = ↑((⇑(Homeomorph.inv 𝕜ˣ) ∘ fun x ↦ x ^ n) x✝)
Module: Mathlib.Analysis.Complex.CoveringMap

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
n : ℕ
hn : ↑(-↑n) ≠ 0
surj : Function.Surjective fun x ↦ x ^ (-↑n)
x✝ : 𝕜
⊢ x✝ ^ n = (Inv.inv ∘ fun x ↦ x ^ (-↑n)) x✝

Tactic:
;

Goal state after:
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
n : ℕ
hn : ↑(-↑n) ≠ 0
surj : Function.Surjective fun x ↦ x ^ (-↑n)
x✝ : 𝕜
⊢ x✝ ^ n = (Inv.inv ∘ fun x ↦ x ^ (-↑n)) x✝
Module: Mathlib.Analysis.Complex.UnitDisc.Basic

Goal state before:
pp: z : 𝔻
⊢ ↑(star (star z)) = ↑z

Tactic:
;

Goal state after:
z : 𝔻
⊢ ↑(star (star z)) = ↑z
Module: Mathlib.Analysis.Complex.UnitDisc.Basic

Goal state before:
pp: z : 𝕔𝔻
⊢ ↑(star (star z)) = ↑z

Tactic:
;

Goal state after:
z : 𝕔𝔻
⊢ ↑(star (star z)) = ↑z