awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbsMax (goal)
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
inst_5 : 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
hwU : w ∈ interior U ∨ w ∈ frontier U
hle : IsMaxOn (norm ∘ f) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U) w
⊢ ∃ z ∈ frontier U, IsMaxOn (norm ∘ f) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U) z
have inl : ∀ (hwU : w ∈ interior U),
  ∃ z ∈ frontier U, IsMaxOn (norm ∘ f) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U) z
Tactic: rcases hwU with hwU | hwU
Cleared hypotheses: hwU
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbsMax (goal)
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
inst_5 : 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
hwU : w ∈ interior U ∨ w ∈ frontier U
hle : IsMaxOn (norm ∘ f) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U) w
inl :
  ∀ (hwU : w ∈ interior U),
    ∃ z ∈ frontier U, IsMaxOn (norm ∘ f) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U) z
⊢ ∃ z ∈ frontier U, IsMaxOn (norm ∘ f) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U) z
have inr : ∀ (hwU : w ∈ frontier U),
  ∃ z ∈ frontier U, IsMaxOn (norm ∘ f) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U) z
Tactic: rcases hwU with hwU | hwU
Cleared hypotheses: hwU
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbsMax (hypothesis)
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
inst_5 : 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
have this : interior U ≠ univ
Tactic: have : interior U ≠ univ := ne_top_of_le_ne_top hc.ne_univ interior_subset_closure
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbsMax (goal)
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
inst_5 : 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
this : interior U ≠ univ
⊢ ∃ z ∈ frontier U, IsMaxOn (norm ∘ f) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U) z
have inl : ∀ (z : E) (hzU : z ∈ frontier (interior U)) (hzw : infDist w (interior U)ᶜ = dist w z),
  ∃ z ∈ frontier U, IsMaxOn (norm ∘ f) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U) z
Tactic: rcases exists_mem_frontier_infDist_compl_eq_dist hwU this with ⟨z, hzU, hzw⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbsMax (goal)
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
inst_5 : 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
this : interior U ≠ univ
z : E
hzU : z ∈ frontier (interior U)
hzw : infDist w (interior U)ᶜ = dist w z
⊢ ∃ z ∈ frontier U, IsMaxOn (norm ∘ f) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U) z
have inl : ∀ (x : E) (hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U), (norm ∘ f) w = (norm ∘ f) z
Tactic: refine ⟨z, frontier_interior_subset hzU, fun x hx => (hle hx).out.trans_eq ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbsMax (goal)
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
inst_5 : 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
this : interior U ≠ univ
z : E
hzU : z ∈ frontier (interior U)
hzw : infDist w (interior U)ᶜ = dist w z
x : E
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
⊢ (norm ∘ f) w = (norm ∘ f) z
have inl : ball w (dist z w) ⊆ U
Tactic: refine (norm_eq_norm_of_isMaxOn_of_ball_subset hd (hle.on_subset subset_closure) ?_).symm
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbsMax (goal)
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
inst_5 : 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
this : interior U ≠ univ
z : E
hzU : z ∈ frontier (interior U)
hzw : infDist w (interior U)ᶜ = dist w z
x : E
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
⊢ ball w (dist z w) ⊆ U
have inl : ball w (infDist w (interior U)ᶜ) ⊆ U
Tactic: rw [dist_comm, ← hzw]
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbsMax (hypothesis)
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 : 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 ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
⊢ ‖f z‖ ≤ C
have hz₁ : z ∈ frontier U ∨ z ∈ U
Tactic: rw [closure_eq_self_union_frontier, union_comm, mem_union] at hz
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbsMax (goal)
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 : 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 ∨ z ∈ U
⊢ ‖f z‖ ≤ C
have inl : ∀ (hz : z ∈ frontier U), ‖f z‖ ≤ C
Tactic: rcases hz with hz | hz
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbsMax (goal)
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 : 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 ∨ z ∈ U
inl : ∀ (hz : z ∈ frontier U), ‖f z‖ ≤ C
⊢ ‖f z‖ ≤ C
have inr : ∀ (hz : z ∈ U), ‖f z‖ ≤ C
Tactic: rcases hz with hz | hz
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbsMax (goal)
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 : 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
have inr : ∀ (w : E) (hne : w ≠ z), ‖f z‖ ≤ C
Tactic: rcases exists_ne z with ⟨w, hne⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbsMax (hypothesis)
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 : 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
w : E
hne : w ≠ z
e : (a : ℂ) → E := (⇑(lineMap z w) : (a : ℂ) → E)
⊢ ‖f z‖ ≤ C
have hde : Differentiable ℂ e
Tactic: have hde : Differentiable ℂ e := (differentiable_id.smul_const (w - z)).add_const z
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbsMax (hypothesis)
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 : 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
w : E
hne : w ≠ z
e : (a : ℂ) → E := (⇑(lineMap z w) : (a : ℂ) → E)
hde : Differentiable ℂ e
⊢ ‖f z‖ ≤ C
have hL : AntilipschitzWith (nndist z w)⁻¹ e
Tactic: have hL : AntilipschitzWith (nndist z w)⁻¹ e := antilipschitzWith_lineMap hne.symm
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbsMax (hypothesis)
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 : 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
w : E
hne : w ≠ z
e : (a : ℂ) → E := (⇑(lineMap z w) : (a : ℂ) → E)
hde : Differentiable ℂ e
hL : AntilipschitzWith (nndist z w)⁻¹ e
⊢ ‖f z‖ ≤ C
have hd₁ : DiffContOnCl ℂ (f ∘ e) (e ⁻¹' U)
Tactic: replace hd : DiffContOnCl ℂ (f ∘ e) (e ⁻¹' U) :=
    hd.comp hde.diffContOnCl (mapsTo_preimage _ _)
Cleared hypotheses: hd
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbsMax (hypothesis)
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 : E → F
U : Set E
hU : Bornology.IsBounded U
C : ℝ
hC : ∀ z ∈ frontier U, ‖f z‖ ≤ C
z : E
hz : z ∈ U
w : E
hne : w ≠ z
e : (a : ℂ) → E := (⇑(lineMap z w) : (a : ℂ) → E)
hde : Differentiable ℂ e
hL : AntilipschitzWith (nndist z w)⁻¹ e
hd : DiffContOnCl ℂ (f ∘ e) (e ⁻¹' U)
⊢ ‖f z‖ ≤ C
have h₀ : 0 ∈ e ⁻¹' U
Tactic: have h₀ : (0 : ℂ) ∈ e ⁻¹' U := by simpa only [e, mem_preimage, lineMap_apply_zero]
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbsMax (goal)
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 : E → F
U : Set E
hU : Bornology.IsBounded U
C : ℝ
hC : ∀ z ∈ frontier U, ‖f z‖ ≤ C
z : E
hz : z ∈ U
w : E
hne : w ≠ z
e : (a : ℂ) → E := (⇑(lineMap z w) : (a : ℂ) → E)
hde : Differentiable ℂ e
hL : AntilipschitzWith (nndist z w)⁻¹ e
hd : DiffContOnCl ℂ (f ∘ e) (e ⁻¹' U)
h₀ : 0 ∈ e ⁻¹' U
⊢ ‖f z‖ ≤ C
have inr : ∀ (ζ : ℂ) (hζU : ζ ∈ frontier (e ⁻¹' U)) (hζ : IsMaxOn (norm ∘ f ∘ e) (closure (e ⁻¹' U)) ζ), ‖f z‖ ≤ C
Tactic: rcases exists_mem_frontier_isMaxOn_norm (hL.isBounded_preimage hU) ⟨0, h₀⟩ hd with ⟨ζ, hζU, hζ⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbsMax (goal)
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 : E → F
U : Set E
hU : Bornology.IsBounded U
C : ℝ
hC : ∀ z ∈ frontier U, ‖f z‖ ≤ C
z : E
hz : z ∈ U
w : E
hne : w ≠ z
e : (a : ℂ) → E := (⇑(lineMap z w) : (a : ℂ) → E)
hde : Differentiable ℂ e
hL : AntilipschitzWith (nndist z w)⁻¹ e
hd : DiffContOnCl ℂ (f ∘ e) (e ⁻¹' U)
h₀ : 0 ∈ e ⁻¹' U
ζ : ℂ
hζU : ζ ∈ frontier (e ⁻¹' U)
hζ : IsMaxOn (norm ∘ f ∘ e) (closure (e ⁻¹' U)) ζ
⊢ ‖f z‖ ≤ C
have by : ‖f z‖ = ‖f (e 0)‖
Tactic: calc
    ‖f z‖ = ‖f (e 0)‖ := by simp only [e, lineMap_apply_zero]
    _ ≤ ‖f (e ζ)‖ := hζ (subset_closure h₀)
    _ ≤ C := hC _ (hde.continuous.frontier_preimage_subset _ hζU)
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbsMax (goal)
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 (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U)
have suffices : ∀ z ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U, ‖(f - g) z‖ ≤ 0
Tactic: suffices H : ∀ z ∈ closure U, ‖(f - g) z‖ ≤ 0 by simpa [sub_eq_zero] using H
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbsMax (goal)
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
have refine : ∀ (z : E) (hz : z ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U) (w : E) (hw : w ∈ frontier U),
  ‖(f - g) w‖ ≤ 0
Tactic: refine fun z hz => norm_le_of_forall_mem_frontier_norm_le hU (hf.sub hg) (fun w hw => ?_) hz
-- Lean 4 proof step from Mathlib.Analysis.Complex.Angle (goal)
Goal:
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ angle x y = |(x / y).arg|
have refine : inner ℝ x y / (‖x‖ * ‖y‖) = Real.cos |(x / y).arg|
Tactic: refine Real.arccos_eq_of_eq_cos (abs_nonneg _) (abs_arg_le_pi _) ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.Angle (goal)
Goal:
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ inner ℝ x y / (‖x‖ * ‖y‖) = Real.cos |(x / y).arg|
have rw : inner ℝ x y / (‖x‖ * ‖y‖) = (x / y).re / ‖x / y‖
Tactic: rw [Real.cos_abs, Complex.cos_arg (div_ne_zero hx hy)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Angle (goal)
Goal:
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ inner ℝ x y / (‖x‖ * ‖y‖) = (x / y).re / ‖x / y‖
have 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‖⁻¹)
Tactic: simp [div_eq_mul_inv, Complex.normSq_eq_norm_sq]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Angle (goal)
Goal:
a : ℂ
ha : a ≠ 0
x y : ℂ
⊢ angle (a * x) (a * y) = angle x y
have inl : angle (a * 0) (a * y) = angle 0 y
Tactic: obtain rfl | hx := eq_or_ne x 0
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.Complex.Angle (goal)
Goal:
a : ℂ
ha : a ≠ 0
x y : ℂ
inl : angle (a * 0) (a * y) = angle 0 y
⊢ angle (a * x) (a * y) = angle x y
have inr : ∀ (hx : x ≠ 0), angle (a * x) (a * y) = angle x y
Tactic: obtain rfl | hx := eq_or_ne x 0
-- Lean 4 proof step from Mathlib.Analysis.Complex.Angle (goal)
Goal:
a : ℂ
ha : a ≠ 0
y : ℂ
⊢ angle (a * 0) (a * y) = angle 0 y
have inl : angle (a * 0) (a * 0) = angle (V := ℂ) 0 0
Tactic: obtain rfl | hy := eq_or_ne y 0
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Analysis.Complex.Angle (goal)
Goal:
a : ℂ
ha : a ≠ 0
y : ℂ
inl : angle (a * 0) (a * 0) = angle (V := ℂ) 0 0
⊢ angle (a * 0) (a * y) = angle 0 y
have inl₁ : ∀ (hy : y ≠ 0), angle (a * 0) (a * y) = angle 0 y
Tactic: obtain rfl | hy := eq_or_ne y 0
-- Lean 4 proof step from Mathlib.Analysis.Complex.Angle (goal)
Goal:
a : ℂ
ha : a ≠ 0
x y : ℂ
hx : x ≠ 0
⊢ angle (a * x) (a * y) = angle x y
have inr : angle (a * x) (a * 0) = angle x 0
Tactic: obtain rfl | hy := eq_or_ne y 0
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Analysis.Complex.Angle (goal)
Goal:
a : ℂ
ha : a ≠ 0
x y : ℂ
hx : x ≠ 0
inr : angle (a * x) (a * 0) = angle x 0
⊢ angle (a * x) (a * y) = angle x y
have inr₁ : ∀ (hy : y ≠ 0), angle (a * x) (a * y) = angle x y
Tactic: obtain rfl | hy := eq_or_ne y 0
-- Lean 4 proof step from Mathlib.Analysis.Complex.Angle (goal)
Goal:
a x y : ℂ
⊢ angle (x / a) y = angle x (y * a)
have inl : angle (x / 0) y = angle x (y * 0)
Tactic: obtain rfl | ha := eq_or_ne a 0
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Analysis.Complex.Angle (goal)
Goal:
a x y : ℂ
inl : angle (x / 0) y = angle x (y * 0)
⊢ angle (x / a) y = angle x (y * a)
have inr : ∀ (ha : a ≠ 0), angle (x / a) y = angle x (y * a)
Tactic: obtain rfl | ha := eq_or_ne a 0
-- Lean 4 proof step from Mathlib.Analysis.Complex.Angle (goal)
Goal:
a x y : ℂ
ha : a ≠ 0
⊢ angle (x / a) y = angle x (y * a)
have inr : angle (x / a * a) (y * a) = angle x (y * a)
Tactic: rw [← angle_mul_right ha, div_mul_cancel₀ _ ha]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Angle (goal)
Goal:
a x y : ℂ
ha : a ≠ 0
inr : angle (x / a * a) (y * a) = angle x (y * a)
⊢ angle (x / a) y = angle x (y * a)
have inr₁ : angle x (y * a) = angle x (y * a)
Tactic: rw [← angle_mul_right ha, div_mul_cancel₀ _ ha]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Angle (goal)
Goal:
a x y : ℂ
⊢ angle x (y / a) = angle (x * a) y
have rw : angle (y / a) x = angle (x * a) y
Tactic: rw [angle_comm, angle_div_left_eq_angle_mul_right, angle_comm]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Angle (goal)
Goal:
a x y : ℂ
rw : angle (y / a) x = angle (x * a) y
⊢ angle x (y / a) = angle (x * a) y
have rw₁ : angle y (x * a) = angle (x * a) y
Tactic: rw [angle_comm, angle_div_left_eq_angle_mul_right, angle_comm]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Angle (goal)
Goal:
a x y : ℂ
rw : angle (y / a) x = angle (x * a) y
rw₁ : angle y (x * a) = angle (x * a) y
⊢ angle x (y / a) = angle (x * a) y
have rw₂ : angle (x * a) y = angle (x * a) y
Tactic: rw [angle_comm, angle_div_left_eq_angle_mul_right, angle_comm]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Angle (goal)
Goal:
x y : ℝ
⊢ angle (cexp ((↑x : ℂ) * I)) (cexp ((↑y : ℂ) * I)) = |toIocMod Real.two_pi_pos (-π) (x - y)|
have simp_rw : |(cexp ((↑x : ℂ) * I) / cexp ((↑y : ℂ) * I)).arg| = |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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Angle (goal)
Goal:
x y : ℝ
simp_rw : |(cexp ((↑x : ℂ) * I) / cexp ((↑y : ℂ) * I)).arg| = |toIocMod Real.two_pi_pos (-π) (x - y)|
⊢ angle (cexp ((↑x : ℂ) * I)) (cexp ((↑y : ℂ) * I)) = |toIocMod Real.two_pi_pos (-π) (x - y)|
have simp_rw₁ : |(cexp ((↑x : ℂ) * I - (↑y : ℂ) * I)).arg| = |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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Angle (goal)
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)|
⊢ angle (cexp ((↑x : ℂ) * I)) (cexp ((↑y : ℂ) * I)) = |toIocMod Real.two_pi_pos (-π) (x - y)|
have simp_rw₂ : |(cexp (((↑x : ℂ) - (↑y : ℂ)) * I)).arg| = |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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Angle (goal)
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)|
⊢ angle (cexp ((↑x : ℂ) * I)) (cexp ((↑y : ℂ) * I)) = |toIocMod Real.two_pi_pos (-π) (x - y)|
have simp_rw₃ : |(cexp ((↑(x - y) : ℂ) * I)).arg| = |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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Angle (goal)
Goal:
x y : ℂ
hx : ‖x‖ = 1
hy : ‖y‖ = 1
⊢ ‖x - y‖ ∈ Icc (2 / π * angle x y) (angle x y)
have 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)
Tactic: wlog h : y = 1
-- Lean 4 proof step from Mathlib.Analysis.Complex.Angle (goal)
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)
⊢ ‖x - y‖ ∈ Icc (2 / π * angle x y) (angle x y)
have wlog : ∀ {x y : ℂ} (hx : ‖x‖ = 1) (hy : ‖y‖ = 1) (h : y = 1), ‖x - y‖ ∈ Icc (2 / π * angle x y) (angle x y)
Tactic: wlog h : y = 1
Cleared hypotheses: hx, hy
-- Lean 4 proof step from Mathlib.Analysis.Complex.Angle (hypothesis)
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‖ ∈ Icc (2 / π * angle x y) (angle x y)
have this₁ : ‖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
-- Lean 4 proof step from Mathlib.Analysis.Complex.Angle (goal)
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)
⊢ ‖x - y‖ ∈ Icc (2 / π * angle x y) (angle x y)
have inr : ∀ (this : ‖x / y - 1‖ ∈ Icc (2 / π * angle x (1 * y)) (angle x (1 * y))), y ≠ 0
Tactic: rwa [angle_div_left_eq_angle_mul_right, div_sub_one, norm_div, hy, div_one, one_mul]
      at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Complex.Angle (goal)
Goal:
x_1 y_1 x y : ℂ
hx : ‖x‖ = 1
hy : ‖y‖ = 1
h : y = 1
⊢ ‖x - y‖ ∈ Icc (2 / π * angle x y) (angle x y)
have subst : ∀ (hy : norm (E := ℂ) 1 = 1), ‖x - 1‖ ∈ Icc (2 / π * angle x 1) (angle x 1)
Tactic: subst y
Cleared hypotheses: y, hy, h
-- Lean 4 proof step from Mathlib.Analysis.Complex.Angle (hypothesis)
Goal:
x_1 y x : ℂ
hx : ‖x‖ = 1
hy : norm (E := ℂ) 1 = 1
⊢ ‖x - 1‖ ∈ Icc (2 / π * angle x 1) (angle x 1)
have hx₁ : ∃ θ ∈ Ioc (-π) π, cexp ((↑θ : ℂ) * I) = x
Tactic: rw [norm_eq_one_iff'] at hx
Cleared hypotheses: hx, hy
-- Lean 4 proof step from Mathlib.Analysis.Complex.Angle (goal)
Goal:
x_1 y x : ℂ
hx : ∃ θ ∈ Ioc (-π) π, cexp ((↑θ : ℂ) * I) = x
hy : norm (E := ℂ) 1 = 1
⊢ ‖x - 1‖ ∈ Icc (2 / π * angle x 1) (angle x 1)
have obtain : ∀ (θ : ℝ) (hθ : θ ∈ Ioc (-π) π),
  ‖cexp ((↑θ : ℂ) * I) - 1‖ ∈ Icc (2 / π * angle (cexp ((↑θ : ℂ) * I)) 1) (angle (cexp ((↑θ : ℂ) * I)) 1)
Tactic: obtain ⟨θ, hθ, rfl⟩ := hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Analysis.Complex.Angle (goal)
Goal:
x y : ℂ
hy : norm (E := ℂ) 1 = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ ‖cexp ((↑θ : ℂ) * I) - 1‖ ∈ Icc (2 / π * angle (cexp ((↑θ : ℂ) * I)) 1) (angle (cexp ((↑θ : ℂ) * I)) 1)
have rw : ‖cos (↑θ : ℂ) - 1 + sin (↑θ : ℂ) * I‖ ∈ Icc (2 / π * |θ|) |θ|
Tactic: rw [angle_exp_one, exp_mul_I, add_sub_right_comm, (toIocMod_eq_self _).2]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Angle (goal)
Goal:
x y : ℂ
hy : norm (E := ℂ) 1 = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
rw : ‖cos (↑θ : ℂ) - 1 + sin (↑θ : ℂ) * I‖ ∈ Icc (2 / π * |θ|) |θ|
⊢ ‖cexp ((↑θ : ℂ) * I) - 1‖ ∈ Icc (2 / π * angle (cexp ((↑θ : ℂ) * I)) 1) (angle (cexp ((↑θ : ℂ) * I)) 1)
have rw₁ : θ ∈ Ioc (-π) (-π + 2 * π)
Tactic: rw [angle_exp_one, exp_mul_I, add_sub_right_comm, (toIocMod_eq_self _).2]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Angle (goal)
Goal:
x y : ℂ
hy : norm (E := ℂ) 1 = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ ‖cos (↑θ : ℂ) - 1 + sin (↑θ : ℂ) * I‖ ∈ Icc (2 / π * |θ|) |θ|
have norm_cast : ‖(↑(Real.cos θ - 1) : ℂ) + (↑(Real.sin θ) : ℂ) * I‖ ∈ Icc (2 / π * |θ|) |θ|
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.Complex.Angle (goal)
Goal:
x y : ℂ
hy : norm (E := ℂ) 1 = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ ‖(↑(Real.cos θ - 1) : ℂ) + (↑(Real.sin θ) : ℂ) * I‖ ∈ Icc (2 / π * |θ|) |θ|
have rw : √(HPow.hPow (β := ℕ) (Real.cos θ - 1) 2 + HPow.hPow (β := ℕ) (Real.sin θ) 2) ∈ Icc (2 / π * |θ|) |θ|
Tactic: rw [norm_add_mul_I]