awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.AbsMax
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
inst_4 : Nontrivial E
f g : E → F
U : Set E
hU : Bornology.IsBounded U
hf : DiffContOnCl ℂ f U
hg : DiffContOnCl ℂ g U
hfg : EqOn f g (frontier U)
suffices : ∀ z ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U, ‖(f - g) z‖ ≤ 0
⊢ EqOn f g (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U)

Tactic:
suffices H : ∀ z ∈ closure U, ‖(f - g) z‖ ≤ 0 by simpa [sub_eq_zero] using H
-- Module: Mathlib.Analysis.Complex.AbsMax
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
inst_4 : Nontrivial E
f g : E → F
U : Set E
hU : Bornology.IsBounded U
hf : DiffContOnCl ℂ f U
hg : DiffContOnCl ℂ g U
hfg : EqOn f g (frontier U)
⊢ ∀ z ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U, ‖(f - g) z‖ ≤ 0

Tactic:
fun z hz => norm_le_of_forall_mem_frontier_norm_le hU (hf.sub hg) (fun w hw => ?_) hz

Premises used: Complex.norm_le_of_forall_mem_frontier_norm_le, DiffContOnCl.sub
-- Module: Mathlib.Analysis.Complex.AbsMax
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
inst_4 : Nontrivial E
f g : E → F
U : Set E
hU : Bornology.IsBounded U
hf : DiffContOnCl ℂ f U
hg : DiffContOnCl ℂ g U
hfg : EqOn f g (frontier U)
refine :
  ∀ (z : E) (hz : z ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U) (w : E) (hw : w ∈ frontier U),
    ‖(f - g) w‖ ≤ 0
⊢ ∀ z ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U, ‖(f - g) z‖ ≤ 0

Tactic:
refine fun z hz => norm_le_of_forall_mem_frontier_norm_le hU (hf.sub hg) (fun w hw => ?_) hz

Premises used: Complex.norm_le_of_forall_mem_frontier_norm_le, DiffContOnCl.sub
-- Module: Mathlib.Analysis.Complex.AbsMax
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
inst_4 : Nontrivial E
f g : E → F
U : Set E
hU : Bornology.IsBounded U
hf : DiffContOnCl ℂ f U
hg : DiffContOnCl ℂ g U
hfg : EqOn f g (frontier U)
z : E
hz : z ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
w : E
hw : w ∈ frontier U
⊢ ‖(f - g) w‖ ≤ 0

Tactic:
simp [hfg hw]
-- Module: Mathlib.Analysis.Complex.AbsMax
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
inst_4 : Nontrivial E
f g : E → F
U : Set E
hU : Bornology.IsBounded U
hf : DiffContOnCl ℂ f U
hg : DiffContOnCl ℂ g U
hfg : EqOn f g (frontier U)
⊢ EqOn f g U

Tactic:
(eqOn_closure_of_eqOn_frontier hU hf hg hfg).mono subset_closure

Premises used: subset_closure, Complex.eqOn_closure_of_eqOn_frontier, Set.EqOn.mono
-- Module: Mathlib.Analysis.Complex.Angle
Goal:
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ angle x y = |(x / y).arg|

Tactic:
Real.arccos_eq_of_eq_cos (abs_nonneg _) (abs_arg_le_pi _) ?_

Premises used: InnerProductGeometry.angle, Complex.abs_arg_le_pi, Real.arccos_eq_of_eq_cos, abs_nonneg
-- Module: Mathlib.Analysis.Complex.Angle
Goal:
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
refine : inner ℝ x y / (‖x‖ * ‖y‖) = Real.cos |(x / y).arg|
⊢ angle x y = |(x / y).arg|

Tactic:
refine Real.arccos_eq_of_eq_cos (abs_nonneg _) (abs_arg_le_pi _) ?_

Premises used: Complex.abs_arg_le_pi, Real.arccos_eq_of_eq_cos, abs_nonneg
-- Module: Mathlib.Analysis.Complex.Angle
Goal:
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
rw : inner ℝ x y / (‖x‖ * ‖y‖) = (x / y).re / ‖x / y‖
⊢ inner ℝ x y / (‖x‖ * ‖y‖) = Real.cos |(x / y).arg|

Tactic:
rw [Real.cos_abs, Complex.cos_arg (div_ne_zero hx hy)]

Premises used: div_ne_zero, Complex.cos_arg, Real.cos_abs
-- Module: Mathlib.Analysis.Complex.Angle
Goal:
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
simp :
  (y.re * x.re + y.im * x.im) * (‖y‖⁻¹ * ‖x‖⁻¹) =
    (x.re * (y.re * (HPow.hPow (β := ℕ) ‖y‖ 2)⁻¹) + x.im * (y.im * (HPow.hPow (β := ℕ) ‖y‖ 2)⁻¹)) * (‖y‖ * ‖x‖⁻¹)
⊢ inner ℝ x y / (‖x‖ * ‖y‖) = (x / y).re / ‖x / y‖

Tactic:
simp [div_eq_mul_inv, Complex.normSq_eq_norm_sq]

Premises used: Complex.normSq_eq_norm_sq, div_eq_mul_inv
-- Module: Mathlib.Analysis.Complex.Angle
Goal:
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ (y.re * x.re + y.im * x.im) * (‖y‖⁻¹ * ‖x‖⁻¹) =
    (x.re * (y.re * (HPow.hPow (β := ℕ) ‖y‖ 2)⁻¹) + x.im * (y.im * (HPow.hPow (β := ℕ) ‖y‖ 2)⁻¹)) * (‖y‖ * ‖x‖⁻¹)

Tactic:
field
-- Module: Mathlib.Analysis.Complex.Angle
Goal:
y : ℂ
hy : y ≠ 0
⊢ angle 1 y = |y.arg|

Tactic:
simp [angle_eq_abs_arg, hy]

Premises used: Complex.angle_eq_abs_arg
-- Module: Mathlib.Analysis.Complex.Angle
Goal:
x : ℂ
hx : x ≠ 0
⊢ angle x 1 = |x.arg|

Tactic:
simp [angle_eq_abs_arg, hx]

Premises used: Complex.angle_eq_abs_arg
-- Module: Mathlib.Analysis.Complex.Angle
Goal:
a : ℂ
ha : a ≠ 0
x y : ℂ
inl : angle (a * 0) (a * y) = angle 0 y
inr : ∀ (hx : x ≠ 0), angle (a * x) (a * y) = angle x y
⊢ angle (a * x) (a * y) = angle x y

Tactic:
obtain rfl | hx := eq_or_ne x 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.Complex.Angle
Goal:
a : ℂ
ha : a ≠ 0
y : ℂ
inl : angle (a * 0) (a * 0) = angle (V := ℂ) 0 0
inl₁ : ∀ (hy : y ≠ 0), angle (a * 0) (a * y) = angle 0 y
⊢ angle (a * 0) (a * y) = angle 0 y

Tactic:
obtain rfl | hy := eq_or_ne y 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.Complex.Angle
Goal:
a : ℂ
ha : a ≠ 0
x y : ℂ
hx : x ≠ 0
inr : angle (a * x) (a * 0) = angle x 0
inr₁ : ∀ (hy : y ≠ 0), angle (a * x) (a * y) = angle x y
⊢ angle (a * x) (a * y) = angle x y

Tactic:
obtain rfl | hy := eq_or_ne y 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.Complex.Angle
Goal:
a : ℂ
ha : a ≠ 0
⊢ angle (a * 0) (a * 0) = angle (V := ℂ) 0 0

Tactic:
simp [angle_eq_abs_arg, mul_div_mul_left, *]

Premises used: Complex.angle_eq_abs_arg, mul_div_mul_left
-- Module: Mathlib.Analysis.Complex.Angle
Goal:
a : ℂ
ha : a ≠ 0
y : ℂ
hy : y ≠ 0
⊢ angle (a * 0) (a * y) = angle 0 y

Tactic:
simp [angle_eq_abs_arg, mul_div_mul_left, *]

Premises used: Complex.angle_eq_abs_arg, mul_div_mul_left
-- Module: Mathlib.Analysis.Complex.Angle
Goal:
a : ℂ
ha : a ≠ 0
x : ℂ
hx : x ≠ 0
⊢ angle (a * x) (a * 0) = angle x 0

Tactic:
simp [angle_eq_abs_arg, mul_div_mul_left, *]

Premises used: Complex.angle_eq_abs_arg, mul_div_mul_left
-- Module: Mathlib.Analysis.Complex.Angle
Goal:
a : ℂ
ha : a ≠ 0
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ angle (a * x) (a * y) = angle x y

Tactic:
simp [angle_eq_abs_arg, mul_div_mul_left, *]

Premises used: Complex.angle_eq_abs_arg, mul_div_mul_left
-- Module: Mathlib.Analysis.Complex.Angle
Goal:
a : ℂ
ha : a ≠ 0
x y : ℂ
⊢ angle (x * a) (y * a) = angle x y

Tactic:
simp [mul_comm, angle_mul_left ha]

Premises used: Complex.angle_mul_left, mul_comm
-- Module: Mathlib.Analysis.Complex.Angle
Goal:
a x y : ℂ
inl : angle (x / 0) y = angle x (y * 0)
inr : ∀ (ha : a ≠ 0), angle (x / a) y = angle x (y * a)
⊢ angle (x / a) y = angle x (y * a)

Tactic:
obtain rfl | ha := eq_or_ne a 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.Complex.Angle
Goal:
x y : ℂ
⊢ angle (x / 0) y = angle x (y * 0)

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.Angle
Goal:
a x y : ℂ
ha : a ≠ 0
inr : angle (x / a * a) (y * a) = angle x (y * a)
inr₁ inr₂ : angle x (y * a) = angle x (y * a)
⊢ angle (x / a) y = angle x (y * a)

Tactic:
rw [← angle_mul_right ha, div_mul_cancel₀ _ ha]

Premises used: div_mul_cancel₀, Complex.angle_mul_right
-- Module: Mathlib.Analysis.Complex.Angle
Goal:
a x y : ℂ
rw : angle (y / a) x = angle (x * a) y
rw₁ : angle y (x * a) = angle (x * a) y
rw₂ rw₃ : angle (x * a) y = angle (x * a) y
⊢ angle x (y / a) = angle (x * a) y

Tactic:
rw [angle_comm, angle_div_left_eq_angle_mul_right, angle_comm]

Premises used: Complex.angle_div_left_eq_angle_mul_right, InnerProductGeometry.angle_comm
-- Module: Mathlib.Analysis.Complex.Angle
Goal:
x y : ℝ
simp_rw : |(cexp ((↑x : ℂ) * I) / cexp ((↑y : ℂ) * I)).arg| = |toIocMod Real.two_pi_pos (-π) (x - y)|
simp_rw₁ : |(cexp ((↑x : ℂ) * I - (↑y : ℂ) * I)).arg| = |toIocMod Real.two_pi_pos (-π) (x - y)|
simp_rw₂ : |(cexp (((↑x : ℂ) - (↑y : ℂ)) * I)).arg| = |toIocMod Real.two_pi_pos (-π) (x - y)|
simp_rw₃ : |(cexp ((↑(x - y) : ℂ) * I)).arg| = |toIocMod Real.two_pi_pos (-π) (x - y)|
⊢ angle (cexp ((↑x : ℂ) * I)) (cexp ((↑y : ℂ) * I)) = |toIocMod Real.two_pi_pos (-π) (x - y)|

Tactic:
simp_rw [angle_eq_abs_arg (exp_ne_zero _) (exp_ne_zero _), ← exp_sub, ← sub_mul, ← ofReal_sub,
    arg_exp_mul_I]

Premises used: Complex.exp_ne_zero, Complex.arg_exp_mul_I, Complex.angle_eq_abs_arg, sub_mul, Complex.ofReal_sub, Complex.exp_sub
-- Module: Mathlib.Analysis.Complex.Angle
Goal:
x : ℝ
⊢ angle (cexp ((↑x : ℂ) * I)) 1 = |toIocMod Real.two_pi_pos (-π) x|

Tactic:
simpa using angle_exp_exp x 0

Premises used: OfNat.ofNat, Complex.angle_exp_exp
-- Module: Mathlib.Analysis.Complex.Angle
Goal:
x y : ℂ
hx : ‖x‖ = 1
hy : ‖y‖ = 1
inr :
  ∀ (this : ∀ {x y : ℂ} (hx : ‖x‖ = 1) (hy : ‖y‖ = 1) (h : y = 1), ‖x - y‖ ∈ Icc (2 / π * angle x y) (angle x y))
    (h : ¬y = 1), ‖x - y‖ ∈ Icc (2 / π * angle x y) (angle x y)
wlog : ∀ {x y : ℂ} (hx : ‖x‖ = 1) (hy : ‖y‖ = 1) (h : y = 1), ‖x - y‖ ∈ Icc (2 / π * angle x y) (angle x y)
⊢ ‖x - y‖ ∈ Icc (2 / π * angle x y) (angle x y)

Tactic:
wlog h : y = 1
-- Module: Mathlib.Analysis.Complex.Angle
Goal:
x y : ℂ
hx : ‖x‖ = 1
hy : ‖y‖ = 1
this : ∀ {x y : ℂ} (hx : ‖x‖ = 1) (hy : ‖y‖ = 1) (h : y = 1), ‖x - y‖ ∈ Icc (2 / π * angle x y) (angle x y)
h : ¬y = 1
⊢ ‖x / y‖ = 1

Tactic:
simp only [norm_div, hx, hy, div_one]

Premises used: norm_div, div_one
-- Module: Mathlib.Analysis.Complex.Angle
Goal:
x y : ℂ
hx : ‖x‖ = 1
hy : ‖y‖ = 1
this : ∀ {x y : ℂ} (hx : ‖x‖ = 1) (hy : ‖y‖ = 1) (h : y = 1), ‖x - y‖ ∈ Icc (2 / π * angle x y) (angle x y)
h : ¬y = 1
⊢ ‖x / y - 1‖ ∈ Icc (2 / π * angle (x / y) 1) (angle (x / y) 1)

Tactic:
have := @this (x / y) 1 (by simp only [norm_div, hx, hy, div_one]) norm_one rfl
-- Module: Mathlib.Analysis.Complex.Angle
Goal:
x y : ℂ
hx : ‖x‖ = 1
hy : ‖y‖ = 1
this_1 : ∀ {x y : ℂ} (hx : ‖x‖ = 1) (hy : ‖y‖ = 1) (h : y = 1), ‖x - y‖ ∈ Icc (2 / π * angle x y) (angle x y)
h : ¬y = 1
this : ‖x / y - 1‖ ∈ Icc (2 / π * angle (x / y) 1) (angle (x / y) 1)
inr : ∀ (this : ‖x / y - 1‖ ∈ Icc (2 / π * angle x (1 * y)) (angle x (1 * y))), y ≠ 0
⊢ ‖x - y‖ ∈ Icc (2 / π * angle x y) (angle x y)

Tactic:
rwa [angle_div_left_eq_angle_mul_right, div_sub_one, norm_div, hy, div_one, one_mul]
      at this

Premises used: Complex.angle_div_left_eq_angle_mul_right, norm_div, div_sub_one, div_one, one_mul
-- Module: Mathlib.Analysis.Complex.Angle
Goal:
x : ℂ
hx : ‖x‖ = 1
this_1 : ∀ {x y : ℂ} (hx : ‖x‖ = 1) (hy : ‖y‖ = 1) (h : y = 1), ‖x - y‖ ∈ Icc (2 / π * angle x y) (angle x y)
hy : norm (E := ℂ) 0 = 1
h : ¬Eq (α := ℂ) 0 1
this : ‖x / 0 - 1‖ ∈ Icc (2 / π * angle x (HMul.hMul (α := ℂ) 1 0)) (angle x (HMul.hMul (α := ℂ) 1 0))
⊢ False

Tactic:
simp at hy
-- Module: Mathlib.Analysis.Complex.Angle
Goal:
x_1 y_1 x y : ℂ
hx : ‖x‖ = 1
hy : ‖y‖ = 1
h : y = 1
subst : ∀ (hy : norm (E := ℂ) 1 = 1), ‖x - 1‖ ∈ Icc (2 / π * angle x 1) (angle x 1)
⊢ ‖x - y‖ ∈ Icc (2 / π * angle x y) (angle x y)

Tactic:
subst y
-- Module: Mathlib.Analysis.Complex.Angle
Goal:
x_1 y x : ℂ
hx : ‖x‖ = 1
hy : norm (E := ℂ) 1 = 1
⊢ ∃ θ ∈ Ioc (-π) π, cexp ((↑θ : ℂ) * I) = x

Tactic:
rw [norm_eq_one_iff'] at hx

Premises used: Complex.norm_eq_one_iff'
-- Module: Mathlib.Analysis.Complex.Angle
Goal:
x_1 y x : ℂ
hx : ‖x‖ = 1
hy : norm (E := ℂ) 1 = 1
hx₁ : ∃ θ ∈ Ioc (-π) π, cexp ((↑θ : ℂ) * I) = x
⊢ norm (E := ℂ) 1 = 1

Tactic:
rw [norm_eq_one_iff'] at hx

Premises used: Complex.norm_eq_one_iff'
-- Module: Mathlib.Analysis.Complex.Angle
Goal:
x_1 y x : ℂ
hx : ∃ θ ∈ Ioc (-π) π, cexp ((↑θ : ℂ) * I) = x
hy : norm (E := ℂ) 1 = 1
obtain :
  ∀ (θ : ℝ) (hθ : θ ∈ Ioc (-π) π),
    ‖cexp ((↑θ : ℂ) * I) - 1‖ ∈ Icc (2 / π * angle (cexp ((↑θ : ℂ) * I)) 1) (angle (cexp ((↑θ : ℂ) * I)) 1)
⊢ ‖x - 1‖ ∈ Icc (2 / π * angle x 1) (angle x 1)

Tactic:
obtain ⟨θ, hθ, rfl⟩ := hx

Premises used: rfl
-- Module: Mathlib.Analysis.Complex.Angle
Goal:
x y : ℂ
hy : norm (E := ℂ) 1 = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
rw : ‖cos (↑θ : ℂ) - 1 + sin (↑θ : ℂ) * I‖ ∈ Icc (2 / π * |θ|) |θ|
rw₁ : θ ∈ Ioc (-π) (-π + 2 * π)
⊢ ‖cexp ((↑θ : ℂ) * I) - 1‖ ∈ Icc (2 / π * angle (cexp ((↑θ : ℂ) * I)) 1) (angle (cexp ((↑θ : ℂ) * I)) 1)

Tactic:
rw [angle_exp_one, exp_mul_I, add_sub_right_comm, (toIocMod_eq_self _).2]

Premises used: Iff.mpr, toIocMod_eq_self, Complex.angle_exp_one, add_sub_right_comm, Complex.exp_mul_I
-- Module: Mathlib.Analysis.Complex.Angle
Goal:
x y : ℂ
hy : norm (E := ℂ) 1 = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
norm_cast : ‖(↑(Real.cos θ - 1) : ℂ) + (↑(Real.sin θ) : ℂ) * I‖ ∈ Icc (2 / π * |θ|) |θ|
⊢ ‖cos (↑θ : ℂ) - 1 + sin (↑θ : ℂ) * I‖ ∈ Icc (2 / π * |θ|) |θ|

Tactic:
norm_cast
-- Module: Mathlib.Analysis.Complex.Angle
Goal:
x y : ℂ
hy : norm (E := ℂ) 1 = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
rw : √(HPow.hPow (β := ℕ) (Real.cos θ - 1) 2 + HPow.hPow (β := ℕ) (Real.sin θ) 2) ∈ Icc (2 / π * |θ|) |θ|
⊢ ‖(↑(Real.cos θ - 1) : ℂ) + (↑(Real.sin θ) : ℂ) * I‖ ∈ Icc (2 / π * |θ|) |θ|

Tactic:
rw [norm_add_mul_I]

Premises used: Complex.norm_add_mul_I
-- Module: Mathlib.Analysis.Complex.Angle
Goal:
x y : ℂ
hy : norm (E := ℂ) 1 = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ √(HPow.hPow (β := ℕ) (Real.cos θ - 1) 2 + HPow.hPow (β := ℕ) (Real.sin θ) 2) ∈ Icc (2 / π * |θ|) |θ|

Tactic:
⟨Real.le_sqrt_of_sq_le ?_, ?_⟩

Premises used: Set.Mem, setOf, Real.le_sqrt_of_sq_le, Set.Icc, And.intro
-- Module: Mathlib.Analysis.Complex.Angle
Goal:
x y : ℂ
hy : norm (E := ℂ) 1 = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
refine_1 :
  HPow.hPow (β := ℕ) (2 / π * |θ|) 2 ≤ HPow.hPow (β := ℕ) (Real.cos θ - 1) 2 + HPow.hPow (β := ℕ) (Real.sin θ) 2
refine_2 : √(HPow.hPow (β := ℕ) (Real.cos θ - 1) 2 + HPow.hPow (β := ℕ) (Real.sin θ) 2) ≤ |θ|
⊢ √(HPow.hPow (β := ℕ) (Real.cos θ - 1) 2 + HPow.hPow (β := ℕ) (Real.sin θ) 2) ∈ Icc (2 / π * |θ|) |θ|

Tactic:
refine ⟨Real.le_sqrt_of_sq_le ?_, ?_⟩
-- Module: Mathlib.Analysis.Complex.Angle
Goal:
x y : ℂ
hy : norm (E := ℂ) 1 = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
refine_1 :
  HPow.hPow (β := ℕ) (2 / π) 2 * HPow.hPow (β := ℕ) θ 2 ≤
    HPow.hPow (β := ℕ) (Real.cos θ - 1) 2 + HPow.hPow (β := ℕ) (Real.sin θ) 2
⊢ HPow.hPow (β := ℕ) (2 / π * |θ|) 2 ≤ HPow.hPow (β := ℕ) (Real.cos θ - 1) 2 + HPow.hPow (β := ℕ) (Real.sin θ) 2

Tactic:
rw [mul_pow, ← abs_pow, abs_sq]

Premises used: abs_sq, mul_pow, abs_pow
-- Module: Mathlib.Analysis.Complex.Angle
Goal:
x y : ℂ
hy : norm (E := ℂ) 1 = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ HPow.hPow (β := ℕ) (2 / π) 2 * HPow.hPow (β := ℕ) θ 2 =
    2 * (1 - (1 - 2 / HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) θ 2))

Tactic:
ring
-- Module: Mathlib.Analysis.Complex.Angle
Goal:
x y : ℂ
hy : norm (E := ℂ) 1 = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
hbc : Real.cos θ ≤ 1 - 2 / HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) θ 2
⊢ 2 * (1 - (1 - 2 / HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) θ 2)) ≤ 2 * (1 - Real.cos θ)

Tactic:
gcongr
-- Module: Mathlib.Analysis.Complex.Angle
Goal:
x y : ℂ
hy : norm (E := ℂ) 1 = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ Real.cos θ ≤ 1 - 2 / HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) θ 2

Tactic:
Real.cos_le_one_sub_mul_cos_sq <| abs_le.2 <| Ioc_subset_Icc_self hθ

Premises used: Iff.mpr, abs_le, Real.cos_le_one_sub_mul_cos_sq, Set.Ioc_subset_Icc_self
-- Module: Mathlib.Analysis.Complex.Angle
Goal:
x y : ℂ
hy : norm (E := ℂ) 1 = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ Real.cos θ ≤ 1 - 2 / HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) θ 2

Tactic:
exact Real.cos_le_one_sub_mul_cos_sq <| abs_le.2 <| Ioc_subset_Icc_self hθ

Premises used: Iff.mpr, abs_le, Real.cos_le_one_sub_mul_cos_sq, Set.Ioc_subset_Icc_self
-- Module: Mathlib.Analysis.Complex.Angle
Goal:
x y : ℂ
hy : norm (E := ℂ) 1 = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ 2 * (1 - Real.cos θ) = HPow.hPow (β := ℕ) (Real.cos θ - 1) 2 + HPow.hPow (β := ℕ) (Real.sin θ) 2

Tactic:
linear_combination -θ.cos_sq_add_sin_sq

Premises used: Real.cos_sq_add_sin_sq
-- Module: Mathlib.Analysis.Complex.Angle
Goal:
x y : ℂ
hy : norm (E := ℂ) 1 = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
_ :
  HPow.hPow (β := ℕ) (2 / π) 2 * HPow.hPow (β := ℕ) θ 2 =
    2 * (1 - (1 - 2 / HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) θ 2))
_₁ : 2 * (1 - (1 - 2 / HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) θ 2)) ≤ 2 * (1 - Real.cos θ)
_₂ : 2 * (1 - Real.cos θ) = HPow.hPow (β := ℕ) (Real.cos θ - 1) 2 + HPow.hPow (β := ℕ) (Real.sin θ) 2
⊢ HPow.hPow (β := ℕ) (2 / π) 2 * HPow.hPow (β := ℕ) θ 2 ≤
    HPow.hPow (β := ℕ) (Real.cos θ - 1) 2 + HPow.hPow (β := ℕ) (Real.sin θ) 2

Tactic:
calc
        _ = 2 * (1 - (1 - 2 / π ^ 2 * θ ^ 2)) := by ring
        _ ≤ 2 * (1 - θ.cos) := by
            gcongr; exact Real.cos_le_one_sub_mul_cos_sq <| abs_le.2 <| Ioc_subset_Icc_self hθ
        _ = _ := by linear_combination -θ.cos_sq_add_sin_sq

Premises used: Real.pi, HMul.hMul, Real.cos, HSub.hSub, HDiv.hDiv, HPow.hPow, OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.Angle
Goal:
x y : ℂ
hy : norm (E := ℂ) 1 = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ 0 ≤ |θ|

Tactic:
positivity
-- Module: Mathlib.Analysis.Complex.Angle
Goal:
x y : ℂ
hy : norm (E := ℂ) 1 = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
refine_2 : HPow.hPow (β := ℕ) (Real.cos θ - 1) 2 + HPow.hPow (β := ℕ) (Real.sin θ) 2 ≤ HPow.hPow (β := ℕ) θ 2
⊢ √(HPow.hPow (β := ℕ) (Real.cos θ - 1) 2 + HPow.hPow (β := ℕ) (Real.sin θ) 2) ≤ |θ|

Tactic:
rw [Real.sqrt_le_left (by positivity), ← abs_pow, abs_sq]

Premises used: abs_sq, Real.sqrt_le_left, abs_pow
-- Module: Mathlib.Analysis.Complex.Angle
Goal:
x y : ℂ
hy : norm (E := ℂ) 1 = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ HPow.hPow (β := ℕ) (Real.cos θ - 1) 2 + HPow.hPow (β := ℕ) (Real.sin θ) 2 = 2 * (1 - Real.cos θ)

Tactic:
linear_combination θ.cos_sq_add_sin_sq

Premises used: Real.cos_sq_add_sin_sq
-- Module: Mathlib.Analysis.Complex.Angle
Goal:
x y : ℂ
hy : norm (E := ℂ) 1 = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
hbc : 1 - HPow.hPow (β := ℕ) θ 2 / 2 ≤ Real.cos θ
⊢ 2 * (1 - Real.cos θ) ≤ 2 * (1 - (1 - HPow.hPow (β := ℕ) θ 2 / 2))

Tactic:
gcongr
-- Module: Mathlib.Analysis.Complex.Angle
Goal:
x y : ℂ
hy : norm (E := ℂ) 1 = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ 1 - HPow.hPow (β := ℕ) θ 2 / 2 ≤ Real.cos θ

Tactic:
Real.one_sub_sq_div_two_le_cos

Premises used: Real.one_sub_sq_div_two_le_cos
-- Module: Mathlib.Analysis.Complex.Angle
Goal:
x y : ℂ
hy : norm (E := ℂ) 1 = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ 1 - HPow.hPow (β := ℕ) θ 2 / 2 ≤ Real.cos θ

Tactic:
exact Real.one_sub_sq_div_two_le_cos

Premises used: Real.one_sub_sq_div_two_le_cos
-- Module: Mathlib.Analysis.Complex.Angle
Goal:
x y : ℂ
hy : norm (E := ℂ) 1 = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ 2 * (1 - (1 - HPow.hPow (β := ℕ) θ 2 / 2)) = HPow.hPow (β := ℕ) θ 2

Tactic:
ring
-- Module: Mathlib.Analysis.Complex.Angle
Goal:
x y : ℂ
hy : norm (E := ℂ) 1 = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
_ : HPow.hPow (β := ℕ) (Real.cos θ - 1) 2 + HPow.hPow (β := ℕ) (Real.sin θ) 2 = 2 * (1 - Real.cos θ)
_₁ : 2 * (1 - Real.cos θ) ≤ 2 * (1 - (1 - HPow.hPow (β := ℕ) θ 2 / 2))
_₂ : 2 * (1 - (1 - HPow.hPow (β := ℕ) θ 2 / 2)) = HPow.hPow (β := ℕ) θ 2
⊢ HPow.hPow (β := ℕ) (Real.cos θ - 1) 2 + HPow.hPow (β := ℕ) (Real.sin θ) 2 ≤ HPow.hPow (β := ℕ) θ 2

Tactic:
calc
        _ = 2 * (1 - θ.cos) := by linear_combination θ.cos_sq_add_sin_sq
        _ ≤ 2 * (1 - (1 - θ ^ 2 / 2)) := by gcongr; exact Real.one_sub_sq_div_two_le_cos
        _ = _ := by ring

Premises used: Real.cos, HSub.hSub, HDiv.hDiv, HPow.hPow, OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.Angle
Goal:
x y : ℂ
hy : norm (E := ℂ) 1 = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ θ ∈ Ioc (-π) π

Tactic:
hθ
-- Module: Mathlib.Analysis.Complex.Angle
Goal:
x y : ℂ
hy : norm (E := ℂ) 1 = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
h : -π + 2 * π = π
⊢ θ ∈ Ioc (-π) (-π + 2 * π)

Tactic:
convert! hθ
-- Module: Mathlib.Analysis.Complex.Angle
Goal:
x y : ℂ
hy : norm (E := ℂ) 1 = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ -π + 2 * π = π

Tactic:
ring
-- Module: Mathlib.Analysis.Complex.Angle
Goal:
x y : ℂ
hx : ‖x‖ = 1
hy : ‖y‖ = 1
⊢ ‖x - y‖ ≤ angle x y

Tactic:
(norm_sub_mem_Icc_angle hx hy).2

Premises used: Complex.norm_sub_mem_Icc_angle, And.right
-- Module: Mathlib.Analysis.Complex.Angle
Goal:
x y : ℂ
hx : ‖x‖ = 1
hy : ‖y‖ = 1
⊢ 2 / π * angle x y ≤ ‖x - y‖

Tactic:
(norm_sub_mem_Icc_angle hx hy).1

Premises used: Complex.norm_sub_mem_Icc_angle, And.left
-- Module: Mathlib.Analysis.Complex.Angle
Goal:
x y : ℂ
hx : ‖x‖ = 1
hy : ‖y‖ = 1
⊢ 0 < π / 2

Tactic:
positivity
-- Module: Mathlib.Analysis.Complex.Angle
Goal:
x y : ℂ
hx : ‖x‖ = 1
hy : ‖y‖ = 1
rw : 2 / π * angle x y ≤ ‖x - y‖
⊢ angle x y ≤ π / 2 * ‖x - y‖

Tactic:
rw [← div_le_iff₀' <| by positivity, div_eq_inv_mul, inv_div]

Premises used: inv_div, div_eq_inv_mul, div_le_iff₀'
-- Module: Mathlib.Analysis.Complex.Angle
Goal:
x y : ℂ
hx : ‖x‖ = 1
hy : ‖y‖ = 1
⊢ 2 / π * angle x y ≤ ‖x - y‖

Tactic:
mul_angle_le_norm_sub hx hy

Premises used: Complex.mul_angle_le_norm_sub
-- Module: Mathlib.Analysis.Complex.Angle
Goal:
x y : ℂ
hx : ‖x‖ = 1
hy : ‖y‖ = 1
⊢ 2 / π * angle x y ≤ ‖x - y‖

Tactic:
exact mul_angle_le_norm_sub hx hy

Premises used: Complex.mul_angle_le_norm_sub
-- Module: Mathlib.Analysis.Complex.Arg
Goal:
x y : ℂ
inl : SameRay ℝ 0 y ↔ Eq (α := ℂ) 0 0 ∨ y = 0 ∨ arg 0 = y.arg
inr : ∀ (hx : x ≠ 0), SameRay ℝ x y ↔ x = 0 ∨ y = 0 ∨ x.arg = y.arg
⊢ SameRay ℝ x y ↔ x = 0 ∨ y = 0 ∨ x.arg = y.arg

Tactic:
rcases eq_or_ne x 0 with (rfl | hx)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.Complex.Arg
Goal:
y : ℂ
⊢ SameRay ℝ 0 y ↔ Eq (α := ℂ) 0 0 ∨ y = 0 ∨ arg 0 = y.arg

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.Arg
Goal:
x y : ℂ
hx : x ≠ 0
inr : SameRay ℝ x 0 ↔ x = 0 ∨ Eq (α := ℂ) 0 0 ∨ x.arg = arg 0
inr₁ : ∀ (hy : y ≠ 0), SameRay ℝ x y ↔ x = 0 ∨ y = 0 ∨ x.arg = y.arg
⊢ SameRay ℝ x y ↔ x = 0 ∨ y = 0 ∨ x.arg = y.arg

Tactic:
rcases eq_or_ne y 0 with (rfl | hy)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.Complex.Arg
Goal:
x : ℂ
hx : x ≠ 0
⊢ SameRay ℝ x 0 ↔ x = 0 ∨ Eq (α := ℂ) 0 0 ∨ x.arg = arg 0

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.Arg
Goal:
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
inr : ‖x‖ • y = ‖y‖ • x ↔ False ∨ False ∨ (↑‖y‖ : ℂ) / (↑‖x‖ : ℂ) * x = y
⊢ SameRay ℝ x y ↔ x = 0 ∨ y = 0 ∨ x.arg = y.arg

Tactic:
simp only [hx, hy, sameRay_iff_norm_smul_eq, arg_eq_arg_iff hx hy]

Premises used: Complex.arg_eq_arg_iff, sameRay_iff_norm_smul_eq
-- Module: Mathlib.Analysis.Complex.Arg
Goal:
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ ‖x‖ • y = ‖y‖ • x ↔ False ∨ False ∨ (↑‖y‖ : ℂ) / (↑‖x‖ : ℂ) * x = y

Tactic:
simp [field, hx, mul_comm, eq_comm]

Premises used: eq_comm, mul_comm
-- Module: Mathlib.Analysis.Complex.Arg
Goal:
x y : ℂ
rw : x = 0 ∨ y = 0 ∨ x.arg = y.arg ↔ (↑(x / y).arg : Real.Angle) = 0
⊢ SameRay ℝ x y ↔ (x / y).arg = 0

Tactic:
rw [← Real.Angle.toReal_zero, ← arg_coe_angle_eq_iff_eq_toReal, sameRay_iff]

Premises used: Complex.arg_coe_angle_eq_iff_eq_toReal, Complex.sameRay_iff, Real.Angle.toReal_zero
-- Module: Mathlib.Analysis.Complex.Arg
Goal:
x y : ℂ
pos : ∀ (hx : x = 0), x = 0 ∨ y = 0 ∨ x.arg = y.arg ↔ (↑(x / y).arg : Real.Angle) = 0
neg : ∀ (hx : ¬x = 0), x = 0 ∨ y = 0 ∨ x.arg = y.arg ↔ (↑(x / y).arg : Real.Angle) = 0
⊢ x = 0 ∨ y = 0 ∨ x.arg = y.arg ↔ (↑(x / y).arg : Real.Angle) = 0

Tactic:
by_cases hx : x = 0
-- Module: Mathlib.Analysis.Complex.Arg
Goal:
x y : ℂ
hx : x = 0
⊢ x = 0 ∨ y = 0 ∨ x.arg = y.arg ↔ (↑(x / y).arg : Real.Angle) = 0

Tactic:
simp [hx]
-- Module: Mathlib.Analysis.Complex.Arg
Goal:
x y : ℂ
hx : ¬x = 0
pos : ∀ (hy : y = 0), x = 0 ∨ y = 0 ∨ x.arg = y.arg ↔ (↑(x / y).arg : Real.Angle) = 0
neg : ∀ (hy : ¬y = 0), x = 0 ∨ y = 0 ∨ x.arg = y.arg ↔ (↑(x / y).arg : Real.Angle) = 0
⊢ x = 0 ∨ y = 0 ∨ x.arg = y.arg ↔ (↑(x / y).arg : Real.Angle) = 0

Tactic:
by_cases hy : y = 0
-- Module: Mathlib.Analysis.Complex.Arg
Goal:
x y : ℂ
hx : ¬x = 0
hy : y = 0
⊢ x = 0 ∨ y = 0 ∨ x.arg = y.arg ↔ (↑(x / y).arg : Real.Angle) = 0

Tactic:
simp [hy]
-- Module: Mathlib.Analysis.Complex.Arg
Goal:
x y : ℂ
hx : ¬x = 0
hy : ¬y = 0
⊢ x = 0 ∨ y = 0 ∨ x.arg = y.arg ↔ (↑(x / y).arg : Real.Angle) = 0

Tactic:
simp [hx, hy, arg_div_coe_angle, sub_eq_zero]

Premises used: sub_eq_zero, Complex.arg_div_coe_angle
-- Module: Mathlib.Analysis.Complex.Arg
Goal:
x y : ℂ
⊢ ‖x + y‖ = ‖x‖ + ‖y‖ ↔ x = 0 ∨ y = 0 ∨ x.arg = y.arg

Tactic:
sameRay_iff_norm_add.symm.trans sameRay_iff

Premises used: sameRay_iff_norm_add, Iff.trans, Complex.sameRay_iff, Iff.symm