awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_2 : b ∈ Ioc (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg) ∪ Ioc (↑y : ℂ).arg (y.angleDiff x + (↑y : ℂ).arg)
⊢ b ∈ 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_2 : b ∉ Ioc (↑x : ℂ).arg (x.angleDiff y + (↑x : ℂ).arg) → 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)

Tactic:
tauto
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
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))

Tactic:
(compl_subset_iff_union.mpr <| path_image_Ioc_union h).antisymm
    <| (disjoint_path_image_Ioc h.symm).subset_compl_right

Premises used: Iff.mpr, Circle.path_image_Ioc_union, Disjoint.subset_compl_right, Ne.symm, Circle.disjoint_path_image_Ioc, Set.compl_subset_iff_union, HasSubset.Subset.antisymm
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x y : Circle
h : x ≠ y
⊢ (↑x : ℂ).arg ≤ x.angleDiff y + (↑x : ℂ).arg

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x y : Circle
h : x ≠ y
⊢ LT.lt (α := (↑unitInterval : Type)) 0 1

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x y : Circle
h : x ≠ y
⊢ x ∉ {x}ᶜ

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x y : Circle
h : x ≠ y
rw :
  Subset (α := Set Circle)
    (image (α := (↑unitInterval : Type)) (⇑(y.path x) : (a : (↑unitInterval : Type)) → Circle) (Ioo 0 1)) {x}ᶜ
⊢ 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))

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]

Premises used: Set.inter_eq_left, Circle.exp_arg, Set.compl_union, Set.Ioc_insert_left, Set.Ioo_insert_right, Circle.range_path, Circle.path_image_Ioc_of_ne, Circle.compl_path_image_Ioc, Set.image_insert_eq, Path.target, Set.union_singleton, Set.insert_inter_of_notMem, Circle.path
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x y : Circle
h : x ≠ y
t : (↑unitInterval : Type)
ht : Membership.mem (γ := Set (↑unitInterval : Type)) (Ioo 0 1) t
⊢ Membership.mem (α := Circle) (γ := Set Circle) {x}ᶜ ((y.path x : (a : (↑unitInterval : Type)) → Circle) t : Circle)

Tactic:
(path_injective_of_ne h.symm).ne ht.2.ne |>.trans_eq (y.path x).target

Premises used: Set.Mem, setOf, Ne.trans_eq, Function.Injective.ne, Ne.symm, And.right, Set.singleton, Circle.path_injective_of_ne, Path.target, Circle.path, Not, LT.lt.ne
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x y : Circle
h : x ≠ y
t : (↑unitInterval : Type)
ht : Membership.mem (γ := Set (↑unitInterval : Type)) (Ioo 0 1) t
⊢ Membership.mem (α := Circle) (γ := Set Circle) {x}ᶜ ((y.path x : (a : (↑unitInterval : Type)) → Circle) t : Circle)

Tactic:
exact (path_injective_of_ne h.symm).ne ht.2.ne |>.trans_eq (y.path x).target

Premises used: Ne.trans_eq, Function.Injective.ne, Ne.symm, And.right, Circle.path_injective_of_ne, Path.target, Circle.path, LT.lt.ne
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x y : Circle
rw :
  Set.Nonempty (α := Circle)
    (range (ι := (↑unitInterval : Type)) (⇑(x.path y) : (a : (↑unitInterval : Type)) → Circle))ᶜ
⊢ SSubset (α := Set Circle) (range (ι := (↑unitInterval : Type)) (⇑(x.path y) : (a : (↑unitInterval : Type)) → Circle))
    univ

Tactic:
rw [ssubset_univ_iff_nonempty_compl]

Premises used: Set.ssubset_univ_iff_nonempty_compl
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x y : Circle
inl :
  Set.Nonempty (α := Circle)
    (range (ι := (↑unitInterval : Type)) (⇑(x.path x) : (a : (↑unitInterval : Type)) → Circle))ᶜ
inr :
  ∀ (hne : x ≠ y),
    Set.Nonempty (α := Circle)
      (range (ι := (↑unitInterval : Type)) (⇑(x.path y) : (a : (↑unitInterval : Type)) → Circle))ᶜ
⊢ Set.Nonempty (α := Circle)
    (range (ι := (↑unitInterval : Type)) (⇑(x.path y) : (a : (↑unitInterval : Type)) → Circle))ᶜ

Tactic:
obtain rfl | hne := eq_or_ne x y

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x : Circle
⊢ Membership.mem (γ := Set Circle)
    (range (ι := (↑unitInterval : Type)) (⇑(x.path x) : (a : (↑unitInterval : Type)) → Circle))ᶜ (-x)

Tactic:
simp [neg_ne_self]

Premises used: Circle.neg_ne_self
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x w : Circle
h :
  Membership.mem (γ := Set Circle)
    (range (ι := (↑unitInterval : Type)) (⇑(x.path x) : (a : (↑unitInterval : Type)) → Circle))ᶜ (-x)
⊢ Set.Nonempty (α := Circle)
    (range (ι := (↑unitInterval : Type)) (⇑(x.path x) : (a : (↑unitInterval : Type)) → Circle))ᶜ

Tactic:
use -x, by simp [neg_ne_self]
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x y : Circle
hne : x ≠ y
inr :
  Set.Nonempty (α := Circle)
    (image (α := (↑unitInterval : Type)) (⇑(y.path x) : (a : (↑unitInterval : Type)) → Circle) (Ioo 0 1))
⊢ Set.Nonempty (α := Circle)
    (range (ι := (↑unitInterval : Type)) (⇑(x.path y) : (a : (↑unitInterval : Type)) → Circle))ᶜ

Tactic:
rw [compl_range_path hne]

Premises used: Circle.compl_range_path
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x y : Circle
hne : x ≠ y
simp : LE.le (α := ℝ) 2⁻¹ 1
⊢ 2⁻¹ ∈ unitInterval

Tactic:
simp only [mem_Icc, inv_nonneg, Nat.ofNat_nonneg, true_and]

Premises used: Nat.ofNat_nonneg, inv_nonneg, Set.mem_Icc, true_and
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x y : Circle
hne : x ≠ y
linarith : LT.lt (α := ℝ) 1 2⁻¹ → 2 / 2 = 1
linarith₁ : LT.lt (α := ℝ) 1 2⁻¹ → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : LT.lt (α := ℝ) 1 2⁻¹ → GT.gt (α := ℝ) 2 0
linarith₃ : LT.lt (α := ℝ) 1 2⁻¹ → -1 + HMul.hMul (α := ℝ) 1 1 = 0
⊢ LE.le (α := ℝ) 2⁻¹ 1

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x y : Circle
hne : x ≠ y
h :
  Membership.mem (α := Circle) (γ := Set Circle)
    (image (α := (↑unitInterval : Type)) (⇑(y.path x) : (a : (↑unitInterval : Type)) → Circle) (Ioo 0 1))
    ((y.path x : (a : (↑unitInterval : Type)) → Circle) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ unitInterval) 2⁻¹ ⋯) :
      Circle)
⊢ Set.Nonempty (α := Circle)
    (image (α := (↑unitInterval : Type)) (⇑(y.path x) : (a : (↑unitInterval : Type)) → Circle) (Ioo 0 1))

Tactic:
use y.path x ⟨2⁻¹, by simp only [mem_Icc, inv_nonneg, Nat.ofNat_nonneg, true_and]; linarith⟩

Premises used: Subtype.mk, Inv.inv, OfNat.ofNat, Circle.path, DFunLike.coe
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x y : Circle
hne : x ≠ y
⊢ LT.lt (α := (↑unitInterval : Type)) 0 (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ unitInterval) 2⁻¹ ⋯)

Tactic:
simp [← unitInterval.coe_pos]

Premises used: unitInterval.coe_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x y : Circle
hne : x ≠ y
h : LT.lt (α := ℝ) (↑(Subtype.mk (p := fun (x : ℝ) ↦ x ∈ unitInterval) 2⁻¹ ⋯) : ℝ) 1
⊢ Membership.mem (α := Circle) (γ := Set Circle)
    (image (α := (↑unitInterval : Type)) (⇑(y.path x) : (a : (↑unitInterval : Type)) → Circle) (Ioo 0 1))
    ((y.path x : (a : (↑unitInterval : Type)) → Circle) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ unitInterval) 2⁻¹ ⋯) :
      Circle)

Tactic:
refine mem_image_of_mem _ ⟨by simp [← unitInterval.coe_pos], unitInterval.coe_lt_one.mp ?_⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x y : Circle
hne : x ≠ y
linarith : LE.le (α := ℝ) 1 (↑(Subtype.mk (p := fun (x : ℝ) ↦ x ∈ unitInterval) 2⁻¹ ⋯) : ℝ) → 2 / 2 = 1
linarith₁ :
  LE.le (α := ℝ) 1 (↑(Subtype.mk (p := fun (x : ℝ) ↦ x ∈ unitInterval) 2⁻¹ ⋯) : ℝ) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : LE.le (α := ℝ) 1 (↑(Subtype.mk (p := fun (x : ℝ) ↦ x ∈ unitInterval) 2⁻¹ ⋯) : ℝ) → GT.gt (α := ℝ) 2 0
linarith₃ :
  LE.le (α := ℝ) 1 (↑(Subtype.mk (p := fun (x : ℝ) ↦ x ∈ unitInterval) 2⁻¹ ⋯) : ℝ) → -1 + HMul.hMul (α := ℝ) 1 1 = 0
⊢ LT.lt (α := ℝ) (↑(Subtype.mk (p := fun (x : ℝ) ↦ x ∈ unitInterval) 2⁻¹ ⋯) : ℝ) 1

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x y : Circle
h : x ≠ y
⊢ LE.le (α := (↑unitInterval : Type)) 0 1

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x y : Circle
h : x ≠ y
rw :
  Eq (α := Set Circle)
    (image (α := (↑unitInterval : Type)) (⇑(x.path y) : (a : (↑unitInterval : Type)) → Circle)
        (insert 0 (insert 1 (Ioo 0 1))) ∩
      image (α := (↑unitInterval : Type)) (⇑(y.path x) : (a : (↑unitInterval : Type)) → Circle)
        (insert 0 (insert 1 (Ioo 0 1))))
    {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))
    {x, y}

Tactic:
rw [← image_univ, ← image_univ, unitInterval.univ_eq_Icc, ← Ioc_insert_left (by simp),
    ← Ioo_insert_right (by simp)]

Premises used: Set.image_univ, Set.Ioc_insert_left, Set.Ioo_insert_right, unitInterval.univ_eq_Icc
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x y : Circle
h : x ≠ y
simp_rw :
  Eq (α := Set Circle)
    (insert ((x.path y : (a : (↑unitInterval : Type)) → Circle) 0)
        (insert ((x.path y : (a : (↑unitInterval : Type)) → Circle) 1)
          (image (α := (↑unitInterval : Type)) (⇑(x.path y) : (a : (↑unitInterval : Type)) → Circle) (Ioo 0 1))) ∩
      insert ((y.path x : (a : (↑unitInterval : Type)) → Circle) 0)
        (insert ((y.path x : (a : (↑unitInterval : Type)) → Circle) 1)
          (image (α := (↑unitInterval : Type)) (⇑(y.path x) : (a : (↑unitInterval : Type)) → Circle) (Ioo 0 1))))
    {x, y}
⊢ Eq (α := Set Circle)
    (image (α := (↑unitInterval : Type)) (⇑(x.path y) : (a : (↑unitInterval : Type)) → Circle)
        (insert 0 (insert 1 (Ioo 0 1))) ∩
      image (α := (↑unitInterval : Type)) (⇑(y.path x) : (a : (↑unitInterval : Type)) → Circle)
        (insert 0 (insert 1 (Ioo 0 1))))
    {x, y}

Tactic:
simp_rw [image_insert_eq]

Premises used: Set.image_insert_eq
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x y : Circle
h : x ≠ y
⊢ Disjoint (α := Set Circle)
    (image (α := (↑unitInterval : Type)) (⇑(x.path y) : (a : (↑unitInterval : Type)) → Circle) (Ioo 0 1))
    (image (α := (↑unitInterval : Type)) (⇑(y.path x) : (a : (↑unitInterval : Type)) → Circle) (Ioo 0 1))

Tactic:
(disjoint_path_image_Ioc h).mono ?_ ?_

Premises used: Circle.disjoint_path_image_Ioc, Disjoint.mono
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x y : Circle
h : x ≠ y
refine_1 :
  LE.le (α := Set Circle)
    (image (α := (↑unitInterval : Type)) (⇑(x.path y) : (a : (↑unitInterval : Type)) → Circle) (Ioo 0 1))
    (image (α := (↑unitInterval : Type)) (⇑(x.path y) : (a : (↑unitInterval : Type)) → Circle) (Ioc 0 1))
refine_2 :
  LE.le (α := Set Circle)
    (image (α := (↑unitInterval : Type)) (⇑(y.path x) : (a : (↑unitInterval : Type)) → Circle) (Ioo 0 1))
    (image (α := (↑unitInterval : Type)) (⇑(y.path x) : (a : (↑unitInterval : Type)) → Circle) (Ioc 0 1))
⊢ Disjoint (α := Set Circle)
    (image (α := (↑unitInterval : Type)) (⇑(x.path y) : (a : (↑unitInterval : Type)) → Circle) (Ioo 0 1))
    (image (α := (↑unitInterval : Type)) (⇑(y.path x) : (a : (↑unitInterval : Type)) → Circle) (Ioo 0 1))

Tactic:
refine (disjoint_path_image_Ioc h).mono ?_ ?_

Premises used: Circle.disjoint_path_image_Ioc, Disjoint.mono
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x y : Circle
h : x ≠ y
⊢ LE.le (α := Set Circle)
    (image (α := (↑unitInterval : Type)) (⇑(x.path y) : (a : (↑unitInterval : Type)) → Circle) (Ioo 0 1))
    (image (α := (↑unitInterval : Type)) (⇑(x.path y) : (a : (↑unitInterval : Type)) → Circle) (Ioc 0 1))

Tactic:
image_mono Ioo_subset_Ioc_self

Premises used: Set.image_mono, Set.Ioo_subset_Ioc_self
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x y : Circle
h : x ≠ y
⊢ LE.le (α := Set Circle)
    (image (α := (↑unitInterval : Type)) (⇑(x.path y) : (a : (↑unitInterval : Type)) → Circle) (Ioo 0 1))
    (image (α := (↑unitInterval : Type)) (⇑(x.path y) : (a : (↑unitInterval : Type)) → Circle) (Ioc 0 1))

Tactic:
exact image_mono Ioo_subset_Ioc_self

Premises used: Set.image_mono, Set.Ioo_subset_Ioc_self
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x y : Circle
h : x ≠ y
⊢ LE.le (α := Set Circle)
    (image (α := (↑unitInterval : Type)) (⇑(y.path x) : (a : (↑unitInterval : Type)) → Circle) (Ioo 0 1))
    (image (α := (↑unitInterval : Type)) (⇑(y.path x) : (a : (↑unitInterval : Type)) → Circle) (Ioc 0 1))

Tactic:
image_mono Ioo_subset_Ioc_self

Premises used: Set.image_mono, Set.Ioo_subset_Ioc_self
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x y : Circle
h : x ≠ y
⊢ LE.le (α := Set Circle)
    (image (α := (↑unitInterval : Type)) (⇑(y.path x) : (a : (↑unitInterval : Type)) → Circle) (Ioo 0 1))
    (image (α := (↑unitInterval : Type)) (⇑(y.path x) : (a : (↑unitInterval : Type)) → Circle) (Ioc 0 1))

Tactic:
exact image_mono Ioo_subset_Ioc_self

Premises used: Set.image_mono, Set.Ioo_subset_Ioc_self
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x y : Circle
h : x ≠ y
⊢ Disjoint (α := Set Circle)
    (image (α := (↑unitInterval : Type)) (⇑(x.path y) : (a : (↑unitInterval : Type)) → Circle) (Ioo 0 1))
    (image (α := (↑unitInterval : Type)) (⇑(y.path x) : (a : (↑unitInterval : Type)) → Circle) (Ioo 0 1))

Tactic:
have h : Disjoint ((x.path y) '' Ioo 0 1) ((y.path x) '' Ioo 0 1) := by
    refine (disjoint_path_image_Ioc h).mono ?_ ?_ <;> exact image_mono Ioo_subset_Ioc_self
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x y : Circle
h_1 : x ≠ y
h :
  Disjoint (α := Set Circle)
    (image (α := (↑unitInterval : Type)) (⇑(x.path y) : (a : (↑unitInterval : Type)) → Circle) (Ioo 0 1))
    (image (α := (↑unitInterval : Type)) (⇑(y.path x) : (a : (↑unitInterval : Type)) → Circle) (Ioo 0 1))
⊢ Eq (α := Set Circle)
    (insert ((x.path y : (a : (↑unitInterval : Type)) → Circle) 0)
        (insert ((x.path y : (a : (↑unitInterval : Type)) → Circle) 1)
          (image (α := (↑unitInterval : Type)) (⇑(x.path y) : (a : (↑unitInterval : Type)) → Circle) (Ioo 0 1))) ∩
      insert ((y.path x : (a : (↑unitInterval : Type)) → Circle) 0)
        (insert ((y.path x : (a : (↑unitInterval : Type)) → Circle) 1)
          (image (α := (↑unitInterval : Type)) (⇑(y.path x) : (a : (↑unitInterval : Type)) → Circle) (Ioo 0 1))))
    {x, y}

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x : Circle
⊢ IsPathConnected (X := Circle) {x}ᶜ

Tactic:
⟨-x, neg_ne_self x, fun y (hyx : y ≠ x) ↦ ?_⟩

Premises used: IsPathConnected, And.intro, Exists.intro, Circle.neg_ne_self, Neg.neg
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x : Circle
refine : ∀ (y : Circle) (hyx : y ≠ x), JoinedIn {x}ᶜ (-x) y
⊢ IsPathConnected (X := Circle) {x}ᶜ

Tactic:
refine ⟨-x, neg_ne_self x, fun y (hyx : y ≠ x) ↦ ?_⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x y : Circle
hyx : y ≠ x
inl :
  ∀ (hxP : x ∉ range (ι := (↑unitInterval : Type)) (⇑((-x).path y) : (a : (↑unitInterval : Type)) → Circle)),
    JoinedIn {x}ᶜ (-x) y
inr :
  ∀
    (hxP :
      Membership.mem (γ := Set Circle)
        (range (ι := (↑unitInterval : Type)) (⇑((-x).path y) : (a : (↑unitInterval : Type)) → Circle)) x),
    JoinedIn {x}ᶜ (-x) y
⊢ JoinedIn {x}ᶜ (-x) y

Tactic:
obtain hxP | hxP := (em (x ∈ range (path (-x) y))).symm

Premises used: Membership.mem, em, Or.symm, Set.range, Circle.path, DFunLike.coe, Neg.neg
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x y : Circle
hyx : y ≠ x
hxP : x ∉ range (ι := (↑unitInterval : Type)) (⇑((-x).path y) : (a : (↑unitInterval : Type)) → Circle)
t : (↑unitInterval : Type)
⊢ Membership.mem (α := Circle) (γ := Set Circle) {x}ᶜ (((-x).path y : (a : (↑unitInterval : Type)) → Circle) t : Circle)

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x y : Circle
hyx : y ≠ x
hxP : x ∉ range (ι := (↑unitInterval : Type)) (⇑((-x).path y) : (a : (↑unitInterval : Type)) → Circle)
⊢ JoinedIn {x}ᶜ (-x) y

Tactic:
exact ⟨(path (-x) y), fun t ↦ by grind⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x y : Circle
hyx : y ≠ x
hxP :
  Membership.mem (γ := Set Circle)
    (range (ι := (↑unitInterval : Type)) (⇑((-x).path y) : (a : (↑unitInterval : Type)) → Circle)) x
⊢ JoinedIn {x}ᶜ (-x) y

Tactic:
⟨(path y (-x)).symm, ?_⟩

Premises used: JoinedIn, Path.symm, Exists.intro, Circle.path, Neg.neg
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x y : Circle
hyx : y ≠ x
hxP :
  Membership.mem (γ := Set Circle)
    (range (ι := (↑unitInterval : Type)) (⇑((-x).path y) : (a : (↑unitInterval : Type)) → Circle)) x
inr :
  ∀ (t : (↑unitInterval : Type)),
    Membership.mem (α := Circle) (γ := Set Circle) {x}ᶜ
      ((Path.symm (y.path (-x)) : (a : (↑unitInterval : Type)) → Circle) t : Circle)
⊢ JoinedIn {x}ᶜ (-x) y

Tactic:
refine ⟨(path y (-x)).symm, ?_⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x : Circle
hyx : -x ≠ x
hxP :
  Membership.mem (γ := Set Circle)
    (range (ι := (↑unitInterval : Type)) (⇑((-x).path (-x)) : (a : (↑unitInterval : Type)) → Circle)) x
⊢ False

Tactic:
simp [(neg_ne_self x).symm] at hxP

Premises used: Ne.symm, Circle.neg_ne_self
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x y : Circle
hyx : y ≠ x
hxP :
  Membership.mem (γ := Set Circle)
    (range (ι := (↑unitInterval : Type)) (⇑((-x).path y) : (a : (↑unitInterval : Type)) → Circle)) x
⊢ -x ≠ y

Tactic:
have hne : -x ≠ y := by
    rintro rfl
    simp [(neg_ne_self x).symm] at hxP
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x y : Circle
hyx : y ≠ x
hxP :
  Membership.mem (γ := Set Circle)
    (range (ι := (↑unitInterval : Type)) (⇑((-x).path y) : (a : (↑unitInterval : Type)) → Circle)) x
hne : -x ≠ y
hP₂ :
  Membership.mem (γ := Set Circle)
    (range (ι := (↑unitInterval : Type)) (⇑(y.path (-x)) : (a : (↑unitInterval : Type)) → Circle)) x
⊢ Membership.mem (γ := Set Circle)
    (range (ι := (↑unitInterval : Type)) (⇑((-x).path y) : (a : (↑unitInterval : Type)) → Circle) ∩
      range (ι := (↑unitInterval : Type)) (⇑(y.path (-x)) : (a : (↑unitInterval : Type)) → Circle))
    x

Tactic:
have h : x ∈ range _ ∩ _ := ⟨hxP, hP₂⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x y : Circle
hyx : y ≠ x
hxP :
  Membership.mem (γ := Set Circle)
    (range (ι := (↑unitInterval : Type)) (⇑((-x).path y) : (a : (↑unitInterval : Type)) → Circle)) x
hne : -x ≠ y
hP₂ :
  Membership.mem (γ := Set Circle)
    (range (ι := (↑unitInterval : Type)) (⇑(y.path (-x)) : (a : (↑unitInterval : Type)) → Circle)) x
h :
  Membership.mem (γ := Set Circle)
    (range (ι := (↑unitInterval : Type)) (⇑((-x).path y) : (a : (↑unitInterval : Type)) → Circle) ∩
      range (ι := (↑unitInterval : Type)) (⇑(y.path (-x)) : (a : (↑unitInterval : Type)) → Circle))
    x
⊢ Membership.mem (γ := Set Circle) {-x, y} x

Tactic:
rw [range_path_inter_range_path hne] at h

Premises used: Circle.range_path_inter_range_path
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x y : Circle
hyx : y ≠ x
hxP :
  Membership.mem (γ := Set Circle)
    (range (ι := (↑unitInterval : Type)) (⇑((-x).path y) : (a : (↑unitInterval : Type)) → Circle)) x
hne : -x ≠ y
hP₂ :
  Membership.mem (γ := Set Circle)
    (range (ι := (↑unitInterval : Type)) (⇑(y.path (-x)) : (a : (↑unitInterval : Type)) → Circle)) x
h : Membership.mem (γ := Set Circle) {-x, y} x
⊢ False

Tactic:
simp [(neg_ne_self x).symm, hyx.symm] at h

Premises used: Ne.symm, Circle.neg_ne_self
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x y : Circle
hyx : y ≠ x
hxP :
  Membership.mem (γ := Set Circle)
    (range (ι := (↑unitInterval : Type)) (⇑((-x).path y) : (a : (↑unitInterval : Type)) → Circle)) x
hne : -x ≠ y
⊢ x ∉ range (ι := (↑unitInterval : Type)) (⇑(y.path (-x)) : (a : (↑unitInterval : Type)) → Circle)

Tactic:
have hP₂ : x ∉ range (path y (-x)) := by
    rintro hP₂
    have h : x ∈ range _ ∩ _ := ⟨hxP, hP₂⟩
    rw [range_path_inter_range_path hne] at h
    simp [(neg_ne_self x).symm, hyx.symm] at h
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x y : Circle
hyx : y ≠ x
hxP :
  Membership.mem (γ := Set Circle)
    (range (ι := (↑unitInterval : Type)) (⇑((-x).path y) : (a : (↑unitInterval : Type)) → Circle)) x
hne : -x ≠ y
hP₂ : x ∉ range (ι := (↑unitInterval : Type)) (⇑(y.path (-x)) : (a : (↑unitInterval : Type)) → Circle)
⊢ ∀ (t : (↑unitInterval : Type)),
    Membership.mem (α := Circle) (γ := Set Circle) {x}ᶜ
      ((Path.symm (y.path (-x)) : (a : (↑unitInterval : Type)) → Circle) t : Circle)

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x y : Circle
hxy : x ≠ y
simp :
  ∃ (x_1 : Set Circle),
    ¬{x, y}ᶜ ⊆ x_1 ∧
      ∃ (x_2 : Set Circle) (_ : IsClosed x_1) (_ : IsClosed x_2) (_ : {x, y}ᶜ ⊆ x_1 ∪ x_2) (_ :
        {x, y}ᶜ ∩ (x_1 ∩ x_2) = ∅), ¬{x, y}ᶜ ⊆ x_2
⊢ ¬IsPreconnected (α := Circle) {x, y}ᶜ

Tactic:
simp only [isPreconnected_iff_subset_of_disjoint_closed, not_forall, not_or, exists_and_left]

Premises used: isPreconnected_iff_subset_of_disjoint_closed, exists_and_left, not_or, Classical.not_forall
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x y : Circle
hxy : x ≠ y
⊢ ∃ (x_1 : Set Circle),
    ¬{x, y}ᶜ ⊆ x_1 ∧
      ∃ (x_2 : Set Circle) (_ : IsClosed x_1) (_ : IsClosed x_2) (_ : {x, y}ᶜ ⊆ x_1 ∪ x_2) (_ :
        {x, y}ᶜ ∩ (x_1 ∩ x_2) = ∅), ¬{x, y}ᶜ ⊆ x_2

Tactic:
⟨range (path x y), ?_, range (path y x), (isCompact_range (path x y).continuous).isClosed,
    (isCompact_range (path y x).continuous).isClosed, ?_, ?_, ?_⟩

Premises used: isCompact_range, Path.continuous, And.intro, Exists.intro, Set.range, Circle.path, DFunLike.coe, IsCompact.isClosed
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x y : Circle
hxy : x ≠ y
refine_1 :
  ¬Subset (α := Set Circle) {x, y}ᶜ
      (range (ι := (↑unitInterval : Type)) (⇑(x.path y) : (a : (↑unitInterval : Type)) → Circle))
refine_2 :
  Subset (α := Set Circle) {x, y}ᶜ
    (range (ι := (↑unitInterval : Type)) (⇑(x.path y) : (a : (↑unitInterval : Type)) → Circle) ∪
      range (ι := (↑unitInterval : Type)) (⇑(y.path x) : (a : (↑unitInterval : Type)) → Circle))
refine_3 :
  Eq (α := Set Circle)
    ({x, y}ᶜ ∩
      (range (ι := (↑unitInterval : Type)) (⇑(x.path y) : (a : (↑unitInterval : Type)) → Circle) ∩
        range (ι := (↑unitInterval : Type)) (⇑(y.path x) : (a : (↑unitInterval : Type)) → Circle)))
    ∅
refine_4 :
  ¬Subset (α := Set Circle) {x, y}ᶜ
      (range (ι := (↑unitInterval : Type)) (⇑(y.path x) : (a : (↑unitInterval : Type)) → Circle))
⊢ ∃ (x_1 : Set Circle),
    ¬{x, y}ᶜ ⊆ x_1 ∧
      ∃ (x_2 : Set Circle) (_ : IsClosed x_1) (_ : IsClosed x_2) (_ : {x, y}ᶜ ⊆ x_1 ∪ x_2) (_ :
        {x, y}ᶜ ∩ (x_1 ∩ x_2) = ∅), ¬{x, y}ᶜ ⊆ x_2

Tactic:
refine ⟨range (path x y), ?_, range (path y x), (isCompact_range (path x y).continuous).isClosed,
    (isCompact_range (path y x).continuous).isClosed, ?_, ?_, ?_⟩