awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
x y : Circle
⊢ Eq (α := (a : (↑unitInterval : Type)) → Circle) (⇑(x.path y) : (a : (↑unitInterval : Type)) → Circle)
    (comp (β := ℝ) (⇑exp : (a : ℝ) → Circle)
      (⇑(Path.segment (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg)) : (a : (↑unitInterval : Type)) → ℝ))
have h : ∀ (t : (↑unitInterval : Type)),
  Eq (α := ℂ) (↑((x.path y : (a : (↑unitInterval : Type)) → Circle) t) : ℂ)
    (↑(comp (β := ℝ) (⇑exp : (a : ℝ) → Circle)
          (⇑(Path.segment (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg)) : (a : (↑unitInterval : Type)) → ℝ) t) :
      ℂ)
Tactic: ext t
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
x y : Circle
t : (↑unitInterval : Type)
⊢ Eq (α := ℂ) (↑((x.path y : (a : (↑unitInterval : Type)) → Circle) t) : ℂ)
    (↑(comp (β := ℝ) (⇑exp : (a : ℝ) → Circle)
          (⇑(Path.segment (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg)) : (a : (↑unitInterval : Type)) → ℝ) t) :
      ℂ)
have h : Eq (α := ℂ)
  (↑((exp : (a : ℝ) → Circle)
        ((Path.segment (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg) : (a : (↑unitInterval : Type)) → ℝ) t)) :
    ℂ)
  (↑(comp (β := ℝ) (⇑exp : (a : ℝ) → Circle)
        (⇑(Path.segment (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg)) : (a : (↑unitInterval : Type)) → ℝ) t) :
    ℂ)
Tactic: rw [path_apply, comp_apply]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
x y : Circle
t : (↑unitInterval : Type)
h :
  Eq (α := ℂ)
    (↑((exp : (a : ℝ) → Circle)
          ((Path.segment (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg) : (a : (↑unitInterval : Type)) → ℝ) t)) :
      ℂ)
    (↑(comp (β := ℝ) (⇑exp : (a : ℝ) → Circle)
          (⇑(Path.segment (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg)) : (a : (↑unitInterval : Type)) → ℝ) t) :
      ℂ)
⊢ Eq (α := ℂ) (↑((x.path y : (a : (↑unitInterval : Type)) → Circle) t) : ℂ)
    (↑(comp (β := ℝ) (⇑exp : (a : ℝ) → Circle)
          (⇑(Path.segment (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg)) : (a : (↑unitInterval : Type)) → ℝ) t) :
      ℂ)
have h₁ : Eq (α := ℂ)
  (↑((exp : (a : ℝ) → Circle)
        ((Path.segment (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg) : (a : (↑unitInterval : Type)) → ℝ) t)) :
    ℂ)
  (↑((exp : (a : ℝ) → Circle)
        ((Path.segment (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg) : (a : (↑unitInterval : Type)) → ℝ) t)) :
    ℂ)
Tactic: rw [path_apply, comp_apply]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
x : Circle
⊢ x.path x = Path.refl x
have a : ∀ (a : (↑unitInterval : Type)),
  Eq (α := ℂ) (↑((x.path x : (a : (↑unitInterval : Type)) → Circle) a) : ℂ)
    (↑((Path.refl x : (a : (↑unitInterval : Type)) → Circle) a) : ℂ)
Tactic: ext a
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
x y : Circle
hne : x ≠ y
⊢ Injective (α := (↑unitInterval : Type)) (β := Circle)
    (comp (β := ℝ) (⇑exp : (a : ℝ) → Circle)
      (⇑(Path.segment (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg)) : (a : (↑unitInterval : Type)) → ℝ))
have refine : range (ι := (↑unitInterval : Type))
    (⇑(Path.segment (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg)) : (a : (↑unitInterval : Type)) → ℝ) ⊆
  Icc (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg)
Tactic: refine (exp_injOn_Icc (a := x.val.arg) (b := angleDiff x y + x.val.arg)
    <| by simp [angleDiff_lt_two_pi]).injective_iff _ ?_ |>.mpr
    <| Path.segment_injective_of_ne <| by simp [angleDiff_pos hne |>.ne']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
x y : Circle
hne : x ≠ y
⊢ range (ι := (↑unitInterval : Type))
      (⇑(Path.segment (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg)) : (a : (↑unitInterval : Type)) → ℝ) ⊆
    Icc (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg)
have rw : segment ℝ (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg) ⊆ Icc (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg)
Tactic: rw [Path.range_segment, segment_eq_Icc (by simp)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
x y : Circle
hne : x ≠ y
rw : segment ℝ (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg) ⊆ Icc (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg)
⊢ range (ι := (↑unitInterval : Type))
      (⇑(Path.segment (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg)) : (a : (↑unitInterval : Type)) → ℝ) ⊆
    Icc (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg)
have rw₁ : Icc (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg) ⊆ Icc (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg)
Tactic: rw [Path.range_segment, segment_eq_Icc (by simp)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
x y : Circle
⊢ Eq (α := Set Circle) (range (ι := (↑unitInterval : Type)) (⇑(x.path y) : (a : (↑unitInterval : Type)) → Circle))
    ((⇑exp : (a : ℝ) → Circle) '' Icc (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg))
have rw : Eq (α := Set Circle)
  (range (ι := (↑unitInterval : Type))
    (comp (β := ℝ) (⇑exp : (a : ℝ) → Circle)
      (⇑(Path.segment (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg)) : (a : (↑unitInterval : Type)) → ℝ)))
  ((⇑exp : (a : ℝ) → Circle) '' Icc (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg))
Tactic: rw [coe_path, range_comp, Path.range_segment, segment_eq_Icc (by simp)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
x y : Circle
rw :
  Eq (α := Set Circle)
    (range (ι := (↑unitInterval : Type))
      (comp (β := ℝ) (⇑exp : (a : ℝ) → Circle)
        (⇑(Path.segment (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg)) : (a : (↑unitInterval : Type)) → ℝ)))
    ((⇑exp : (a : ℝ) → Circle) '' Icc (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg))
⊢ Eq (α := Set Circle) (range (ι := (↑unitInterval : Type)) (⇑(x.path y) : (a : (↑unitInterval : Type)) → Circle))
    ((⇑exp : (a : ℝ) → Circle) '' Icc (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg))
have rw₁ : Eq (α := Set Circle)
  (image (α := ℝ) (⇑exp : (a : ℝ) → Circle)
    (range (ι := (↑unitInterval : Type))
      (⇑(Path.segment (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg)) : (a : (↑unitInterval : Type)) → ℝ)))
  ((⇑exp : (a : ℝ) → Circle) '' Icc (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg))
Tactic: rw [coe_path, range_comp, Path.range_segment, segment_eq_Icc (by simp)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
x y : Circle
rw :
  Eq (α := Set Circle)
    (range (ι := (↑unitInterval : Type))
      (comp (β := ℝ) (⇑exp : (a : ℝ) → Circle)
        (⇑(Path.segment (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg)) : (a : (↑unitInterval : Type)) → ℝ)))
    ((⇑exp : (a : ℝ) → Circle) '' Icc (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg))
rw₁ :
  Eq (α := Set Circle)
    (image (α := ℝ) (⇑exp : (a : ℝ) → Circle)
      (range (ι := (↑unitInterval : Type))
        (⇑(Path.segment (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg)) : (a : (↑unitInterval : Type)) → ℝ)))
    ((⇑exp : (a : ℝ) → Circle) '' Icc (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg))
⊢ Eq (α := Set Circle) (range (ι := (↑unitInterval : Type)) (⇑(x.path y) : (a : (↑unitInterval : Type)) → Circle))
    ((⇑exp : (a : ℝ) → Circle) '' Icc (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg))
have rw₂ : Eq (α := Set Circle) ((⇑exp : (a : ℝ) → Circle) '' segment ℝ (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg))
  ((⇑exp : (a : ℝ) → Circle) '' Icc (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg))
Tactic: rw [coe_path, range_comp, Path.range_segment, segment_eq_Icc (by simp)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
x y : Circle
rw :
  Eq (α := Set Circle)
    (range (ι := (↑unitInterval : Type))
      (comp (β := ℝ) (⇑exp : (a : ℝ) → Circle)
        (⇑(Path.segment (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg)) : (a : (↑unitInterval : Type)) → ℝ)))
    ((⇑exp : (a : ℝ) → Circle) '' Icc (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg))
rw₁ :
  Eq (α := Set Circle)
    (image (α := ℝ) (⇑exp : (a : ℝ) → Circle)
      (range (ι := (↑unitInterval : Type))
        (⇑(Path.segment (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg)) : (a : (↑unitInterval : Type)) → ℝ)))
    ((⇑exp : (a : ℝ) → Circle) '' Icc (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg))
rw₂ :
  Eq (α := Set Circle) ((⇑exp : (a : ℝ) → Circle) '' segment ℝ (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg))
    ((⇑exp : (a : ℝ) → Circle) '' Icc (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg))
⊢ Eq (α := Set Circle) (range (ι := (↑unitInterval : Type)) (⇑(x.path y) : (a : (↑unitInterval : Type)) → Circle))
    ((⇑exp : (a : ℝ) → Circle) '' Icc (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg))
have rw₃ : Eq (α := Set Circle) ((⇑exp : (a : ℝ) → Circle) '' Icc (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg))
  ((⇑exp : (a : ℝ) → Circle) '' Icc (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg))
Tactic: rw [coe_path, range_comp, Path.range_segment, segment_eq_Icc (by simp)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
x y : Circle
h : x ≠ y
⊢ Eq (α := Set Circle)
    (image (α := (↑unitInterval : Type)) (⇑(x.path y) : (a : (↑unitInterval : Type)) → Circle) (Ico 0 1))
    ((⇑exp : (a : ℝ) → Circle) '' Ico (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg))
have rw : Eq (α := Set Circle)
  (image (α := (↑unitInterval : Type))
    (comp (β := ℝ) (⇑exp : (a : ℝ) → Circle)
      (⇑(Path.segment (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg)) : (a : (↑unitInterval : Type)) → ℝ))
    (Ico 0 1))
  ((⇑exp : (a : ℝ) → Circle) '' Ico (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg))
Tactic: rw [coe_path, image_comp, segment_image_Ico (by simp [angleDiff_pos h])]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
x y : Circle
h : x ≠ y
rw :
  Eq (α := Set Circle)
    (image (α := (↑unitInterval : Type))
      (comp (β := ℝ) (⇑exp : (a : ℝ) → Circle)
        (⇑(Path.segment (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg)) : (a : (↑unitInterval : Type)) → ℝ))
      (Ico 0 1))
    ((⇑exp : (a : ℝ) → Circle) '' Ico (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg))
⊢ Eq (α := Set Circle)
    (image (α := (↑unitInterval : Type)) (⇑(x.path y) : (a : (↑unitInterval : Type)) → Circle) (Ico 0 1))
    ((⇑exp : (a : ℝ) → Circle) '' Ico (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg))
have rw₁ : Eq (α := Set Circle)
  (image (α := ℝ) (⇑exp : (a : ℝ) → Circle)
    (image (α := (↑unitInterval : Type))
      (⇑(Path.segment (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg)) : (a : (↑unitInterval : Type)) → ℝ) (Ico 0 1)))
  ((⇑exp : (a : ℝ) → Circle) '' Ico (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg))
Tactic: rw [coe_path, image_comp, segment_image_Ico (by simp [angleDiff_pos h])]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
x y : Circle
h : x ≠ y
rw :
  Eq (α := Set Circle)
    (image (α := (↑unitInterval : Type))
      (comp (β := ℝ) (⇑exp : (a : ℝ) → Circle)
        (⇑(Path.segment (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg)) : (a : (↑unitInterval : Type)) → ℝ))
      (Ico 0 1))
    ((⇑exp : (a : ℝ) → Circle) '' Ico (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg))
rw₁ :
  Eq (α := Set Circle)
    (image (α := ℝ) (⇑exp : (a : ℝ) → Circle)
      (image (α := (↑unitInterval : Type))
        (⇑(Path.segment (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg)) : (a : (↑unitInterval : Type)) → ℝ) (Ico 0 1)))
    ((⇑exp : (a : ℝ) → Circle) '' Ico (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg))
⊢ Eq (α := Set Circle)
    (image (α := (↑unitInterval : Type)) (⇑(x.path y) : (a : (↑unitInterval : Type)) → Circle) (Ico 0 1))
    ((⇑exp : (a : ℝ) → Circle) '' Ico (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg))
have rw₂ : Eq (α := Set Circle) ((⇑exp : (a : ℝ) → Circle) '' Ico (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg))
  ((⇑exp : (a : ℝ) → Circle) '' Ico (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg))
Tactic: rw [coe_path, image_comp, segment_image_Ico (by simp [angleDiff_pos h])]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
x y : Circle
h : x ≠ y
⊢ Eq (α := Set Circle)
    (image (α := (↑unitInterval : Type)) (⇑(x.path y) : (a : (↑unitInterval : Type)) → Circle) (Ioc 0 1))
    ((⇑exp : (a : ℝ) → Circle) '' Ioc (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg))
have rw : Eq (α := Set Circle)
  (image (α := (↑unitInterval : Type))
    (comp (β := ℝ) (⇑exp : (a : ℝ) → Circle)
      (⇑(Path.segment (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg)) : (a : (↑unitInterval : Type)) → ℝ))
    (Ioc 0 1))
  ((⇑exp : (a : ℝ) → Circle) '' Ioc (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg))
Tactic: rw [coe_path, image_comp, segment_image_Ioc (by simp [angleDiff_pos h])]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
x y : Circle
h : x ≠ y
rw :
  Eq (α := Set Circle)
    (image (α := (↑unitInterval : Type))
      (comp (β := ℝ) (⇑exp : (a : ℝ) → Circle)
        (⇑(Path.segment (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg)) : (a : (↑unitInterval : Type)) → ℝ))
      (Ioc 0 1))
    ((⇑exp : (a : ℝ) → Circle) '' Ioc (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg))
⊢ Eq (α := Set Circle)
    (image (α := (↑unitInterval : Type)) (⇑(x.path y) : (a : (↑unitInterval : Type)) → Circle) (Ioc 0 1))
    ((⇑exp : (a : ℝ) → Circle) '' Ioc (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg))
have rw₁ : Eq (α := Set Circle)
  (image (α := ℝ) (⇑exp : (a : ℝ) → Circle)
    (image (α := (↑unitInterval : Type))
      (⇑(Path.segment (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg)) : (a : (↑unitInterval : Type)) → ℝ) (Ioc 0 1)))
  ((⇑exp : (a : ℝ) → Circle) '' Ioc (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg))
Tactic: rw [coe_path, image_comp, segment_image_Ioc (by simp [angleDiff_pos h])]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
x y : Circle
h : x ≠ y
rw :
  Eq (α := Set Circle)
    (image (α := (↑unitInterval : Type))
      (comp (β := ℝ) (⇑exp : (a : ℝ) → Circle)
        (⇑(Path.segment (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg)) : (a : (↑unitInterval : Type)) → ℝ))
      (Ioc 0 1))
    ((⇑exp : (a : ℝ) → Circle) '' Ioc (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg))
rw₁ :
  Eq (α := Set Circle)
    (image (α := ℝ) (⇑exp : (a : ℝ) → Circle)
      (image (α := (↑unitInterval : Type))
        (⇑(Path.segment (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg)) : (a : (↑unitInterval : Type)) → ℝ) (Ioc 0 1)))
    ((⇑exp : (a : ℝ) → Circle) '' Ioc (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg))
⊢ Eq (α := Set Circle)
    (image (α := (↑unitInterval : Type)) (⇑(x.path y) : (a : (↑unitInterval : Type)) → Circle) (Ioc 0 1))
    ((⇑exp : (a : ℝ) → Circle) '' Ioc (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg))
have rw₂ : Eq (α := Set Circle) ((⇑exp : (a : ℝ) → Circle) '' Ioc (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg))
  ((⇑exp : (a : ℝ) → Circle) '' Ioc (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg))
Tactic: rw [coe_path, image_comp, segment_image_Ioc (by simp [angleDiff_pos h])]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
x y : Circle
h : x ≠ y
⊢ Eq (α := Set Circle)
    (range (ι := (↑unitInterval : Type)) (⇑(x.path y) : (a : (↑unitInterval : Type)) → Circle) ∪
      range (ι := (↑unitInterval : Type)) (⇑(y.path x) : (a : (↑unitInterval : Type)) → Circle))
    univ
have rw : Eq (α := Set Circle) (range (ι := ℝ) (⇑exp : (a : ℝ) → Circle)) univ
Tactic: rw [range_path, range_path, ← image_union, Icc_union_Icc_angleDiff_add_arg h,
    periodic_exp.image_Icc two_pi_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
x y : Circle
h : x ≠ y
⊢ Eq (α := Set Circle)
    (image (α := (↑unitInterval : Type)) (⇑(x.path y) : (a : (↑unitInterval : Type)) → Circle) (Ioc 0 1) ∪
      image (α := (↑unitInterval : Type)) (⇑(y.path x) : (a : (↑unitInterval : Type)) → Circle) (Ioc 0 1))
    univ
have rw : Eq (α := Set Circle) (range (ι := ℝ) (⇑exp : (a : ℝ) → Circle)) univ
Tactic: rw [path_image_Ioc_of_ne h, path_image_Ioc_of_ne h.symm, ← image_union,
    Ioc_union_Ioc_angleDiff_add_arg h, periodic_exp.image_Ioc two_pi_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (hypothesis)
Goal:
x y : Circle
h : x ≠ y
⊢ Disjoint (α := Set Circle)
    (image (α := (↑unitInterval : Type)) (⇑(x.path y) : (a : (↑unitInterval : Type)) → Circle) (Ioc 0 1))
    (image (α := (↑unitInterval : Type)) (⇑(y.path x) : (a : (↑unitInterval : Type)) → Circle) (Ioc 0 1))
have hdisj : Disjoint (Ioc (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg)) (Ioc (↑y : ℂ).arg (y.angleDiff x + (↑y : ℂ).arg))
Tactic: have hdisj : Disjoint (Ioc x.val.arg (angleDiff x y + x.val.arg))
      (Ioc y.val.arg (angleDiff y x + y.val.arg)) := by grind [angleDiff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
x y : Circle
h : x ≠ y
hdisj : Disjoint (Ioc (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg)) (Ioc (↑y : ℂ).arg (y.angleDiff x + (↑y : ℂ).arg))
⊢ Disjoint (α := Set Circle)
    (image (α := (↑unitInterval : Type)) (⇑(x.path y) : (a : (↑unitInterval : Type)) → Circle) (Ioc 0 1))
    (image (α := (↑unitInterval : Type)) (⇑(y.path x) : (a : (↑unitInterval : Type)) → Circle) (Ioc 0 1))
have rw : Disjoint (α := Set Circle) ((⇑exp : (a : ℝ) → Circle) '' Ioc (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg))
  ((⇑exp : (a : ℝ) → Circle) '' Ioc (↑y : ℂ).arg (y.angleDiff x + (↑y : ℂ).arg))
Tactic: rw [path_image_Ioc_of_ne h, path_image_Ioc_of_ne h.symm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
x y : Circle
h : x ≠ y
hdisj : Disjoint (Ioc (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg)) (Ioc (↑y : ℂ).arg (y.angleDiff x + (↑y : ℂ).arg))
⊢ Disjoint (α := Set Circle) ((⇑exp : (a : ℝ) → Circle) '' Ioc (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg))
    ((⇑exp : (a : ℝ) → Circle) '' Ioc (↑y : ℂ).arg (y.angleDiff x + (↑y : ℂ).arg))
have refine : ∀ (a : ℝ) (ha : a ∈ Ioc (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg)) (b : ℝ)
  (hb : b ∈ Ioc (↑y : ℂ).arg (y.angleDiff x + (↑y : ℂ).arg)),
  Ne (α := Circle) ((exp : (a : ℝ) → Circle) a : Circle) ((exp : (a : ℝ) → Circle) b : Circle)
Tactic: refine Set.disjoint_image_image fun a ha b hb ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
x y : Circle
h : x ≠ y
hdisj : Disjoint (Ioc (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg)) (Ioc (↑y : ℂ).arg (y.angleDiff x + (↑y : ℂ).arg))
a : ℝ
ha : a ∈ Ioc (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg)
b : ℝ
hb : b ∈ Ioc (↑y : ℂ).arg (y.angleDiff x + (↑y : ℂ).arg)
⊢ Ne (α := Circle) ((exp : (a : ℝ) → Circle) a : Circle) ((exp : (a : ℝ) → Circle) b : Circle)
have refine_1 : a ∈ Ioc (min (↑x : ℂ).arg (↑y : ℂ).arg) (min (↑x : ℂ).arg (↑y : ℂ).arg + 2 * π)
Tactic: refine exp_injOn_Ioc (a := min x.val.arg y.val.arg) (b := min x.val.arg y.val.arg + 2 * π)
    (by simp) |>.ne ?_ ?_ <| hdisj.ne_of_mem ha hb
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
x y : Circle
h : x ≠ y
hdisj : Disjoint (Ioc (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg)) (Ioc (↑y : ℂ).arg (y.angleDiff x + (↑y : ℂ).arg))
a : ℝ
ha : a ∈ Ioc (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg)
b : ℝ
hb : b ∈ Ioc (↑y : ℂ).arg (y.angleDiff x + (↑y : ℂ).arg)
refine_1 : a ∈ Ioc (min (↑x : ℂ).arg (↑y : ℂ).arg) (min (↑x : ℂ).arg (↑y : ℂ).arg + 2 * π)
⊢ Ne (α := Circle) ((exp : (a : ℝ) → Circle) a : Circle) ((exp : (a : ℝ) → Circle) b : Circle)
have refine_2 : b ∈ Ioc (min (↑x : ℂ).arg (↑y : ℂ).arg) (min (↑x : ℂ).arg (↑y : ℂ).arg + 2 * π)
Tactic: refine exp_injOn_Ioc (a := min x.val.arg y.val.arg) (b := min x.val.arg y.val.arg + 2 * π)
    (by simp) |>.ne ?_ ?_ <| hdisj.ne_of_mem ha hb
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
x y : Circle
h : x ≠ y
hdisj : Disjoint (Ioc (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg)) (Ioc (↑y : ℂ).arg (y.angleDiff x + (↑y : ℂ).arg))
a : ℝ
ha : a ∈ Ioc (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg)
b : ℝ
hb : b ∈ Ioc (↑y : ℂ).arg (y.angleDiff x + (↑y : ℂ).arg)
⊢ a ∈ Ioc (min (↑x : ℂ).arg (↑y : ℂ).arg) (min (↑x : ℂ).arg (↑y : ℂ).arg + 2 * π)
have refine_1 : a ∈ Ioc (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg) ∪ Ioc (↑y : ℂ).arg (y.angleDiff x + (↑y : ℂ).arg)
Tactic: rw [← Ioc_union_Ioc_angleDiff_add_arg h]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
x y : Circle
h : x ≠ y
hdisj : Disjoint (Ioc (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg)) (Ioc (↑y : ℂ).arg (y.angleDiff x + (↑y : ℂ).arg))
a : ℝ
ha : a ∈ Ioc (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg)
b : ℝ
hb : b ∈ Ioc (↑y : ℂ).arg (y.angleDiff x + (↑y : ℂ).arg)
⊢ a ∈ Ioc (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg) ∪ Ioc (↑y : ℂ).arg (y.angleDiff x + (↑y : ℂ).arg)
have refine_1 : a ∉ Ioc (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg) → a ∈ Ioc (↑y : ℂ).arg (y.angleDiff x + (↑y : ℂ).arg)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
x y : Circle
h : x ≠ y
hdisj : Disjoint (Ioc (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg)) (Ioc (↑y : ℂ).arg (y.angleDiff x + (↑y : ℂ).arg))
a : ℝ
ha : a ∈ Ioc (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg)
b : ℝ
hb : b ∈ Ioc (↑y : ℂ).arg (y.angleDiff x + (↑y : ℂ).arg)
⊢ b ∈ Ioc (min (↑x : ℂ).arg (↑y : ℂ).arg) (min (↑x : ℂ).arg (↑y : ℂ).arg + 2 * π)
have refine_2 : b ∈ Ioc (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg) ∪ Ioc (↑y : ℂ).arg (y.angleDiff x + (↑y : ℂ).arg)
Tactic: rw [← Ioc_union_Ioc_angleDiff_add_arg h]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
x y : Circle
h : x ≠ y
hdisj : Disjoint (Ioc (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg)) (Ioc (↑y : ℂ).arg (y.angleDiff x + (↑y : ℂ).arg))
a : ℝ
ha : a ∈ Ioc (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg)
b : ℝ
hb : b ∈ Ioc (↑y : ℂ).arg (y.angleDiff x + (↑y : ℂ).arg)
⊢ b ∈ Ioc (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg) ∪ Ioc (↑y : ℂ).arg (y.angleDiff x + (↑y : ℂ).arg)
have refine_2 : b ∉ Ioc (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg) → b ∈ Ioc (↑y : ℂ).arg (y.angleDiff x + (↑y : ℂ).arg)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
x y : Circle
h : x ≠ y
⊢ Eq (α := Set Circle) (range (ι := (↑unitInterval : Type)) (⇑(x.path y) : (a : (↑unitInterval : Type)) → Circle))ᶜ
    (image (α := (↑unitInterval : Type)) (⇑(y.path x) : (a : (↑unitInterval : Type)) → Circle) (Ioo 0 1))
have rw : Subset (α := Set Circle)
  (image (α := (↑unitInterval : Type)) (⇑(y.path x) : (a : (↑unitInterval : Type)) → Circle) (Ioo 0 1)) {x}ᶜ
Tactic: rw [range_path, ← Ioc_insert_left (by simp), image_insert_eq,
    ← path_image_Ioc_of_ne h, ← union_singleton, compl_union, compl_path_image_Ioc h,
    ← Ioo_insert_right (by simp), image_insert_eq, (y.path x).target, exp_arg,
    insert_inter_of_notMem (by simp), inter_eq_left]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
x y : Circle
⊢ SSubset (α := Set Circle) (range (ι := (↑unitInterval : Type)) (⇑(x.path y) : (a : (↑unitInterval : Type)) → Circle))
    univ
have rw : Set.Nonempty (α := Circle) (range (ι := (↑unitInterval : Type)) (⇑(x.path y) : (a : (↑unitInterval : Type)) → Circle))ᶜ
Tactic: rw [ssubset_univ_iff_nonempty_compl]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
x y : Circle
⊢ Set.Nonempty (α := Circle)
    (range (ι := (↑unitInterval : Type)) (⇑(x.path y) : (a : (↑unitInterval : Type)) → Circle))ᶜ
have inl : Set.Nonempty (α := Circle) (range (ι := (↑unitInterval : Type)) (⇑(x.path x) : (a : (↑unitInterval : Type)) → Circle))ᶜ
Tactic: obtain rfl | hne := eq_or_ne x y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
x y : Circle
inl :
  Set.Nonempty (α := Circle)
    (range (ι := (↑unitInterval : Type)) (⇑(x.path x) : (a : (↑unitInterval : Type)) → Circle))ᶜ
⊢ Set.Nonempty (α := Circle)
    (range (ι := (↑unitInterval : Type)) (⇑(x.path y) : (a : (↑unitInterval : Type)) → Circle))ᶜ
have inr : ∀ (hne : x ≠ y),
  Set.Nonempty (α := Circle)
    (range (ι := (↑unitInterval : Type)) (⇑(x.path y) : (a : (↑unitInterval : Type)) → Circle))ᶜ
Tactic: obtain rfl | hne := eq_or_ne x y
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
x w : Circle
⊢ Set.Nonempty (α := Circle)
    (range (ι := (↑unitInterval : Type)) (⇑(x.path x) : (a : (↑unitInterval : Type)) → Circle))ᶜ
have h : Membership.mem (γ := Set Circle)
  (range (ι := (↑unitInterval : Type)) (⇑(x.path x) : (a : (↑unitInterval : Type)) → Circle))ᶜ (-x)
Tactic: use -x, by simp [neg_ne_self]