awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
s : Set ℝ
hs : ∀ x ∈ s, ∀ y ∈ s, x - y ∈ Ioo (-2 * π) (2 * π)
t₁ : ℝ
ht₁ : t₁ ∈ s
t₂ : ℝ
ht₂ : t₂ ∈ s
h1 : -(2 * π) < t₁ - t₂
h2 : t₁ - t₂ < 2 * π
heq : (cexp ((↑(t₁ - t₂) : ℂ) * I)).re = re 1 ∧ (cexp ((↑(t₁ - t₂) : ℂ) * I)).im = im 1
⊢ (cexp ((↑(t₁ - t₂) : ℂ) * I)).re = 1

Tactic:
exact heq.1

Premises used: And.left
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
a b : ℝ
h : b - a < 2 * π
x : ℝ
h_1 : x ∈ Icc a b
y : ℝ
h_2 : y ∈ Icc a b
hx1 : a ≤ x
hx2 : x ≤ b
hy1 : a ≤ y
hy2 : y ≤ b
left : -2 * π < x - y
right : x - y < 2 * π
⊢ x - y ∈ Ioo (-2 * π) (2 * π)

Tactic:
constructor
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
a b : ℝ
h : b - a < 2 * π
x : ℝ
h_1 : x ∈ Icc a b
y : ℝ
h_2 : y ∈ Icc a b
hx1 : a ≤ x
hx2 : x ≤ b
hy1 : a ≤ y
hy2 : y ≤ b
linarith : x - y ≤ -2 * π → b - a - 2 * π + (a - x) + (y - b) + (x - y - -2 * π) = 0
⊢ -2 * π < x - y

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
a b : ℝ
h : b - a < 2 * π
x : ℝ
h_1 : x ∈ Icc a b
y : ℝ
h_2 : y ∈ Icc a b
hx1 : a ≤ x
hx2 : x ≤ b
hy1 : a ≤ y
hy2 : y ≤ b
linarith : 2 * π ≤ x - y → b - a - 2 * π + (x - b) + (a - y) + (2 * π - (x - y)) = 0
⊢ x - y < 2 * π

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
a b : ℝ
h : b - a ≤ 2 * π
x : ℝ
h_1 : x ∈ Ico a b
y : ℝ
h_2 : y ∈ Ico a b
hx1 : a ≤ x
hx2 : x < b
hy1 : a ≤ y
hy2 : y < b
left : -2 * π < x - y
right : x - y < 2 * π
⊢ x - y ∈ Ioo (-2 * π) (2 * π)

Tactic:
constructor
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
a b : ℝ
h : b - a ≤ 2 * π
x : ℝ
h_1 : x ∈ Ico a b
y : ℝ
h_2 : y ∈ Ico a b
hx1 : a ≤ x
hx2 : x < b
hy1 : a ≤ y
hy2 : y < b
linarith : x - y ≤ -2 * π → b - a - 2 * π + (a - x) + (y - b) + (x - y - -2 * π) = 0
⊢ -2 * π < x - y

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
a b : ℝ
h : b - a ≤ 2 * π
x : ℝ
h_1 : x ∈ Ico a b
y : ℝ
h_2 : y ∈ Ico a b
hx1 : a ≤ x
hx2 : x < b
hy1 : a ≤ y
hy2 : y < b
linarith : 2 * π ≤ x - y → b - a - 2 * π + (x - b) + (a - y) + (2 * π - (x - y)) = 0
⊢ x - y < 2 * π

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
a b : ℝ
h : b - a ≤ 2 * π
x : ℝ
h_1 : x ∈ Ioc a b
y : ℝ
h_2 : y ∈ Ioc a b
hx1 : a < x
hx2 : x ≤ b
hy1 : a < y
hy2 : y ≤ b
left : -2 * π < x - y
right : x - y < 2 * π
⊢ x - y ∈ Ioo (-2 * π) (2 * π)

Tactic:
constructor
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
a b : ℝ
h : b - a ≤ 2 * π
x : ℝ
h_1 : x ∈ Ioc a b
y : ℝ
h_2 : y ∈ Ioc a b
hx1 : a < x
hx2 : x ≤ b
hy1 : a < y
hy2 : y ≤ b
linarith : x - y ≤ -2 * π → b - a - 2 * π + (a - x) + (y - b) + (x - y - -2 * π) = 0
⊢ -2 * π < x - y

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
a b : ℝ
h : b - a ≤ 2 * π
x : ℝ
h_1 : x ∈ Ioc a b
y : ℝ
h_2 : y ∈ Ioc a b
hx1 : a < x
hx2 : x ≤ b
hy1 : a < y
hy2 : y ≤ b
linarith : 2 * π ≤ x - y → b - a - 2 * π + (x - b) + (a - y) + (2 * π - (x - y)) = 0
⊢ x - y < 2 * π

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
⊢ Surjective (α := ℝ) (β := Circle) (⇑exp : (a : ℝ) → Circle)

Tactic:
fun z => ⟨z.val.arg, exp_arg z⟩

Premises used: Circle.exp_arg, Complex.arg, Exists.intro, Subtype.val, Function.Surjective
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
⊢ PathConnectedSpace Circle

Tactic:
exp_surjective.pathConnectedSpace exp.continuous

Premises used: ContinuousMap.continuous, Function.Surjective.pathConnectedSpace, Circle.exp, Circle.exp_surjective
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x y : Circle
⊢ 0 ≤ x.angleDiff y

Tactic:
grind [neg_pi_lt_arg y.val, arg_le_pi x.val]

Premises used: Complex.arg_le_pi, Complex.neg_pi_lt_arg, Subtype.val
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x y : Circle
h : x ≠ y
⊢ 0 < x.angleDiff y

Tactic:
grind [arg_eq_arg, neg_pi_lt_arg y.val, arg_le_pi x.val]

Premises used: Complex.arg_le_pi, Circle.arg_eq_arg, Complex.neg_pi_lt_arg, Subtype.val
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x y : Circle
⊢ x.angleDiff y < 2 * π

Tactic:
grind [neg_pi_lt_arg x.val, arg_le_pi y.val]

Premises used: Complex.arg_le_pi, Complex.neg_pi_lt_arg, Subtype.val
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x y : Circle
h : x ≠ y
⊢ x.angleDiff y + y.angleDiff x = 2 * π

Tactic:
grind [arg_eq_arg, neg_pi_lt_arg x.val, arg_le_pi y.val]

Premises used: Complex.arg_le_pi, Circle.arg_eq_arg, Complex.neg_pi_lt_arg, Subtype.val
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x y : Circle
rw :
  (exp : (a : ℝ) → Circle)
      ((if arg (↑((exp : (a : ℝ) → Circle) (↑x : ℂ).arg) : ℂ) ≤ (↑y : ℂ).arg then
          (↑y : ℂ).arg - arg (↑((exp : (a : ℝ) → Circle) (↑x : ℂ).arg) : ℂ)
        else 2 * π + (↑y : ℂ).arg - arg (↑((exp : (a : ℝ) → Circle) (↑x : ℂ).arg) : ℂ)) +
        (↑x : ℂ).arg) =
    y
⊢ HMul.hMul (α := Circle) ((exp : (a : ℝ) → Circle) (x.angleDiff y) : Circle) x = y

Tactic:
rw [← exp_arg x, ← exp_add, angleDiff]

Premises used: Circle.exp_arg, Circle.angleDiff, Circle.exp_add
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x y : Circle
pos :
  ∀ (hxy : arg (↑((exp : (a : ℝ) → Circle) (↑x : ℂ).arg) : ℂ) ≤ (↑y : ℂ).arg),
    (exp : (a : ℝ) → Circle) ((↑y : ℂ).arg - arg (↑((exp : (a : ℝ) → Circle) (↑x : ℂ).arg) : ℂ) + (↑x : ℂ).arg) = y
neg :
  ∀ (hxy : ¬arg (↑((exp : (a : ℝ) → Circle) (↑x : ℂ).arg) : ℂ) ≤ (↑y : ℂ).arg),
    (exp : (a : ℝ) → Circle)
        (2 * π + (↑y : ℂ).arg - arg (↑((exp : (a : ℝ) → Circle) (↑x : ℂ).arg) : ℂ) + (↑x : ℂ).arg) =
      y
⊢ (exp : (a : ℝ) → Circle)
      ((if arg (↑((exp : (a : ℝ) → Circle) (↑x : ℂ).arg) : ℂ) ≤ (↑y : ℂ).arg then
          (↑y : ℂ).arg - arg (↑((exp : (a : ℝ) → Circle) (↑x : ℂ).arg) : ℂ)
        else 2 * π + (↑y : ℂ).arg - arg (↑((exp : (a : ℝ) → Circle) (↑x : ℂ).arg) : ℂ)) +
        (↑x : ℂ).arg) =
    y

Tactic:
split_ifs with hxy
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x y : Circle
hxy : arg (↑((exp : (a : ℝ) → Circle) (↑x : ℂ).arg) : ℂ) ≤ (↑y : ℂ).arg
⊢ (exp : (a : ℝ) → Circle) ((↑y : ℂ).arg - arg (↑((exp : (a : ℝ) → Circle) (↑x : ℂ).arg) : ℂ) + (↑x : ℂ).arg) = y

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x y : Circle
hxy : ¬arg (↑((exp : (a : ℝ) → Circle) (↑x : ℂ).arg) : ℂ) ≤ (↑y : ℂ).arg
⊢ (exp : (a : ℝ) → Circle) (2 * π + (↑y : ℂ).arg - arg (↑((exp : (a : ℝ) → Circle) (↑x : ℂ).arg) : ℂ) + (↑x : ℂ).arg) =
    y

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x y : Circle
h : x ≠ y
⊢ Icc (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg) ∪ Icc (↑y : ℂ).arg (y.angleDiff x + (↑y : ℂ).arg) =
    Icc (min (↑x : ℂ).arg (↑y : ℂ).arg) (min (↑x : ℂ).arg (↑y : ℂ).arg + 2 * π)

Tactic:
grind [arg_eq_arg, arg_lt_arg_add_two_pi y x, arg_lt_arg_add_two_pi x y]

Premises used: Circle.arg_eq_arg, Complex.arg_lt_arg_add_two_pi, Subtype.val
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x y : Circle
h : x ≠ y
⊢ Ico (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg) ∪ Ico (↑y : ℂ).arg (y.angleDiff x + (↑y : ℂ).arg) =
    Ico (min (↑x : ℂ).arg (↑y : ℂ).arg) (min (↑x : ℂ).arg (↑y : ℂ).arg + 2 * π)

Tactic:
grind [arg_eq_arg, arg_lt_arg_add_two_pi y x, arg_lt_arg_add_two_pi x y]

Premises used: Circle.arg_eq_arg, Complex.arg_lt_arg_add_two_pi, Subtype.val
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x y : Circle
h : x ≠ y
⊢ Ioc (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg) ∪ Ioc (↑y : ℂ).arg (y.angleDiff x + (↑y : ℂ).arg) =
    Ioc (min (↑x : ℂ).arg (↑y : ℂ).arg) (min (↑x : ℂ).arg (↑y : ℂ).arg + 2 * π)

Tactic:
grind [arg_eq_arg, arg_lt_arg_add_two_pi y x, arg_lt_arg_add_two_pi x y]

Premises used: Circle.arg_eq_arg, Complex.arg_lt_arg_add_two_pi, Subtype.val
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x_1 y_1 x y : Circle
⊢ x = (exp : (a : ℝ) → Circle) (↑x : ℂ).arg

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x_1 y_1 x y : Circle
⊢ y = (exp : (a : ℝ) → Circle) (x.angleDiff y + (↑x : ℂ).arg)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x y : Circle
a : (↑unitInterval : Type)
⊢ Eq (α := Circle) ((x.path y : (a : (↑unitInterval : Type)) → Circle) a : Circle)
    ((exp : (a : ℝ) → Circle)
        ((Path.segment (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg) : (a : (↑unitInterval : Type)) → ℝ) a) :
      Circle)

Tactic:
simp [path]

Premises used: Circle.path
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x y : Circle
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) :
        ℂ)
⊢ 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)) → ℝ))

Tactic:
ext t
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
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) :
      ℂ)
h₁ 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)) :
      ℂ)
⊢ 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:
rw [path_apply, comp_apply]

Premises used: Function.comp_apply, Circle.path_apply
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x : Circle
a :
  ∀ (a : (↑unitInterval : Type)),
    Eq (α := ℂ) (↑((x.path x : (a : (↑unitInterval : Type)) → Circle) a) : ℂ)
      (↑((Path.refl x : (a : (↑unitInterval : Type)) → Circle) a) : ℂ)
⊢ x.path x = Path.refl x

Tactic:
ext a
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x : Circle
a : (↑unitInterval : Type)
⊢ Eq (α := ℂ) (↑((x.path x : (a : (↑unitInterval : Type)) → Circle) a) : ℂ)
    (↑((Path.refl x : (a : (↑unitInterval : Type)) → Circle) a) : ℂ)

Tactic:
simp [path, angleDiff]

Premises used: Circle.angleDiff, Circle.path
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x y : Circle
hne : x ≠ y
⊢ x.angleDiff y + (↑x : ℂ).arg - (↑x : ℂ).arg < 2 * π

Tactic:
simp [angleDiff_lt_two_pi]

Premises used: Circle.angleDiff_lt_two_pi
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x y : Circle
hne : x ≠ y
⊢ (↑x : ℂ).arg ≠ x.angleDiff y + (↑x : ℂ).arg

Tactic:
simp [angleDiff_pos hne |>.ne']

Premises used: LT.lt.ne', Circle.angleDiff_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x y : Circle
hne : x ≠ y
refine :
  range (ι := (↑unitInterval : Type))
      (⇑(Path.segment (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg)) : (a : (↑unitInterval : Type)) → ℝ) ⊆
    Icc (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg)
⊢ Injective (α := (↑unitInterval : Type)) (β := Circle)
    (comp (β := ℝ) (⇑exp : (a : ℝ) → Circle)
      (⇑(Path.segment (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg)) : (a : (↑unitInterval : Type)) → ℝ))

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']

Premises used: Iff.mpr, Set.InjOn.injective_iff, Circle.exp_injOn_Icc, Path.segment_injective_of_ne
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x y : Circle
hne : x ≠ y
⊢ (↑x : ℂ).arg ≤ x.angleDiff y + (↑x : ℂ).arg

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x y : Circle
hne : x ≠ y
rw : segment ℝ (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg) ⊆ Icc (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg)
rw₁ rw₂ : Icc (↑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)

Tactic:
rw [Path.range_segment, segment_eq_Icc (by simp)]

Premises used: segment_eq_Icc, Path.range_segment
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x y : Circle
⊢ (↑x : ℂ).arg ≤ x.angleDiff y + (↑x : ℂ).arg

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
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))
rw₃ 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))
⊢ Eq (α := Set Circle) (range (ι := (↑unitInterval : Type)) (⇑(x.path y) : (a : (↑unitInterval : Type)) → Circle))
    ((⇑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)]

Premises used: Set.range_comp, Circle.coe_path, segment_eq_Icc, Path.range_segment
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x y : Circle
h : x ≠ y
⊢ (↑x : ℂ).arg < x.angleDiff y + (↑x : ℂ).arg

Tactic:
simp [angleDiff_pos h]

Premises used: Circle.angleDiff_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
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))
rw₂ 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))
⊢ 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))

Tactic:
rw [coe_path, image_comp, segment_image_Ico (by simp [angleDiff_pos h])]

Premises used: Circle.coe_path, segment_image_Ico, Set.image_comp
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
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))
rw₂ 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))
⊢ 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))

Tactic:
rw [coe_path, image_comp, segment_image_Ioc (by simp [angleDiff_pos h])]

Premises used: Circle.coe_path, Set.image_comp, segment_image_Ioc
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x y : Circle
h : x ≠ y
rw : Eq (α := Set Circle) (range (ι := ℝ) (⇑exp : (a : ℝ) → Circle)) univ
⊢ Eq (α := Set Circle)
    (range (ι := (↑unitInterval : Type)) (⇑(x.path y) : (a : (↑unitInterval : Type)) → Circle) ∪
      range (ι := (↑unitInterval : Type)) (⇑(y.path x) : (a : (↑unitInterval : Type)) → Circle))
    univ

Tactic:
rw [range_path, range_path, ← image_union, Icc_union_Icc_angleDiff_add_arg h,
    periodic_exp.image_Icc two_pi_pos]

Premises used: Circle.periodic_exp, Function.Periodic.image_Icc, Circle.Icc_union_Icc_angleDiff_add_arg, Circle.range_path, Real.two_pi_pos, Set.image_union
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x y : Circle
h : x ≠ y
⊢ Eq (α := Set Circle) (range (ι := ℝ) (⇑exp : (a : ℝ) → Circle)) univ

Tactic:
exp_surjective.range_eq

Premises used: Function.Surjective.range_eq, Circle.exp_surjective
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x y : Circle
h : x ≠ y
⊢ Eq (α := Set Circle) (range (ι := ℝ) (⇑exp : (a : ℝ) → Circle)) univ

Tactic:
exact exp_surjective.range_eq

Premises used: Function.Surjective.range_eq, Circle.exp_surjective
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x y : Circle
h : x ≠ y
rw : Eq (α := Set Circle) (range (ι := ℝ) (⇑exp : (a : ℝ) → Circle)) univ
⊢ 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

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]

Premises used: Circle.periodic_exp, Circle.Ioc_union_Ioc_angleDiff_add_arg, Ne.symm, Real.two_pi_pos, Function.Periodic.image_Ioc, Circle.path_image_Ioc_of_ne, Set.image_union
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x y : Circle
h : x ≠ y
⊢ Disjoint (Ioc (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg)) (Ioc (↑y : ℂ).arg (y.angleDiff x + (↑y : ℂ).arg))

Tactic:
grind [angleDiff]

Premises used: Circle.angleDiff
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x y : Circle
h : x ≠ y
⊢ 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]
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
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))
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))
⊢ 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))

Tactic:
rw [path_image_Ioc_of_ne h, path_image_Ioc_of_ne h.symm]

Premises used: Ne.symm, Circle.path_image_Ioc_of_ne
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
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))

Tactic:
Set.disjoint_image_image fun a ha b hb ↦ ?_

Premises used: Set.disjoint_image_image
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
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))
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)
⊢ 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:
refine Set.disjoint_image_image fun a ha b hb ↦ ?_

Premises used: Set.disjoint_image_image
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
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)
⊢ min (↑x : ℂ).arg (↑y : ℂ).arg + 2 * π - min (↑x : ℂ).arg (↑y : ℂ).arg ≤ 2 * π

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
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 * π)
refine_2 : b ∈ Ioc (min (↑x : ℂ).arg (↑y : ℂ).arg) (min (↑x : ℂ).arg (↑y : ℂ).arg + 2 * π)
⊢ Ne (α := Circle) ((exp : (a : ℝ) → Circle) a : Circle) ((exp : (a : ℝ) → Circle) b : Circle)

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

Premises used: Circle.exp_injOn_Ioc, Set.InjOn.ne, Disjoint.ne_of_mem
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
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 (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg) ∪ Ioc (↑y : ℂ).arg (y.angleDiff x + (↑y : ℂ).arg)
⊢ a ∈ Ioc (min (↑x : ℂ).arg (↑y : ℂ).arg) (min (↑x : ℂ).arg (↑y : ℂ).arg + 2 * π)

Tactic:
rw [← Ioc_union_Ioc_angleDiff_add_arg h]

Premises used: Circle.Ioc_union_Ioc_angleDiff_add_arg
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
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 refine_1₁ :
  a ∉ Ioc (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg) → a ∈ 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)

Tactic:
tauto