awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
x y : Circle
hne : x ≠ y
⊢ Set.Nonempty (α := Circle)
    (range (ι := (↑unitInterval : Type)) (⇑(x.path y) : (a : (↑unitInterval : Type)) → Circle))ᶜ
have inr : Set.Nonempty (α := Circle)
  (image (α := (↑unitInterval : Type)) (⇑(y.path x) : (a : (↑unitInterval : Type)) → Circle) (Ioo 0 1))
Tactic: rw [compl_range_path hne]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
x y : Circle
hne : x ≠ y
⊢ 2⁻¹ ∈ unitInterval
have simp : LE.le (α := ℝ) 2⁻¹ 1
Tactic: simp only [mem_Icc, inv_nonneg, Nat.ofNat_nonneg, true_and]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
x y : Circle
hne : x ≠ y
⊢ LE.le (α := ℝ) 2⁻¹ 1
have linarith : LT.lt (α := ℝ) 1 2⁻¹ → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
x y : Circle
hne : x ≠ y
linarith : LT.lt (α := ℝ) 1 2⁻¹ → 2 / 2 = 1
⊢ LE.le (α := ℝ) 2⁻¹ 1
have linarith₁ : LT.lt (α := ℝ) 1 2⁻¹ → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
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
⊢ LE.le (α := ℝ) 2⁻¹ 1
have linarith₂ : LT.lt (α := ℝ) 1 2⁻¹ → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
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
⊢ LE.le (α := ℝ) 2⁻¹ 1
have linarith₃ : LT.lt (α := ℝ) 1 2⁻¹ → -1 + HMul.hMul (α := ℝ) 1 1 = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
x y : Circle
hne : x ≠ y
⊢ Set.Nonempty (α := Circle)
    (image (α := (↑unitInterval : Type)) (⇑(y.path x) : (a : (↑unitInterval : Type)) → Circle) (Ioo 0 1))
have 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⁻¹ sorry) : Circle)
Tactic: use y.path x ⟨2⁻¹, by simp only [mem_Icc, inv_nonneg, Nat.ofNat_nonneg, true_and]; linarith⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
x y : Circle
hne : x ≠ y
⊢ 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)
have h : LT.lt (α := ℝ) (↑(Subtype.mk (p := fun (x : ℝ) ↦ x ∈ unitInterval) 2⁻¹ sorry) : ℝ) 1
Tactic: refine mem_image_of_mem _ ⟨by simp [← unitInterval.coe_pos], unitInterval.coe_lt_one.mp ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
x y : Circle
hne : x ≠ y
⊢ LT.lt (α := ℝ) (↑(Subtype.mk (p := fun (x : ℝ) ↦ x ∈ unitInterval) 2⁻¹ ⋯) : ℝ) 1
have linarith : LE.le (α := ℝ) 1 (↑(Subtype.mk (p := fun (x : ℝ) ↦ x ∈ unitInterval) 2⁻¹ sorry) : ℝ) → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
x y : Circle
hne : x ≠ y
linarith : LE.le (α := ℝ) 1 (↑(Subtype.mk (p := fun (x : ℝ) ↦ x ∈ unitInterval) 2⁻¹ ⋯) : ℝ) → 2 / 2 = 1
⊢ LT.lt (α := ℝ) (↑(Subtype.mk (p := fun (x : ℝ) ↦ x ∈ unitInterval) 2⁻¹ ⋯) : ℝ) 1
have linarith₁ : LE.le (α := ℝ) 1 (↑(Subtype.mk (p := fun (x : ℝ) ↦ x ∈ unitInterval) 2⁻¹ sorry) : ℝ) → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
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
⊢ LT.lt (α := ℝ) (↑(Subtype.mk (p := fun (x : ℝ) ↦ x ∈ unitInterval) 2⁻¹ ⋯) : ℝ) 1
have linarith₂ : LE.le (α := ℝ) 1 (↑(Subtype.mk (p := fun (x : ℝ) ↦ x ∈ unitInterval) 2⁻¹ sorry) : ℝ) → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
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
⊢ LT.lt (α := ℝ) (↑(Subtype.mk (p := fun (x : ℝ) ↦ x ∈ unitInterval) 2⁻¹ ⋯) : ℝ) 1
have linarith₃ : LE.le (α := ℝ) 1 (↑(Subtype.mk (p := fun (x : ℝ) ↦ x ∈ unitInterval) 2⁻¹ sorry) : ℝ) → -1 + HMul.hMul (α := ℝ) 1 1 = 0
Tactic: linarith
-- 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))
    {x, y}
have 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}
Tactic: rw [← image_univ, ← image_univ, unitInterval.univ_eq_Icc, ← Ioc_insert_left (by simp),
    ← Ioo_insert_right (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)
        (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}
have 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}
Tactic: simp_rw [image_insert_eq]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
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))
have 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))
Tactic: refine (disjoint_path_image_Ioc h).mono ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
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))
⊢ 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))
have 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))
Tactic: refine (disjoint_path_image_Ioc h).mono ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (hypothesis)
Goal:
x y : Circle
h : x ≠ y
⊢ 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}
have 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))
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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
x : Circle
⊢ IsPathConnected (X := Circle) {x}ᶜ
have refine : ∀ (y : Circle) (hyx : y ≠ x), JoinedIn {x}ᶜ (-x) y
Tactic: refine ⟨-x, neg_ne_self x, fun y (hyx : y ≠ x) ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
x y : Circle
hyx : y ≠ x
⊢ JoinedIn {x}ᶜ (-x) y
have inl : ∀ (hxP : x ∉ range (ι := (↑unitInterval : Type)) (⇑((-x).path y) : (a : (↑unitInterval : Type)) → Circle)),
  JoinedIn {x}ᶜ (-x) y
Tactic: obtain hxP | hxP := (em (x ∈ range (path (-x) y))).symm
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
x y : Circle
hyx : y ≠ x
inl :
  ∀ (hxP : x ∉ range (ι := (↑unitInterval : Type)) (⇑((-x).path y) : (a : (↑unitInterval : Type)) → Circle)),
    JoinedIn {x}ᶜ (-x) y
⊢ JoinedIn {x}ᶜ (-x) y
have inr : ∀
  (hxP :
    Membership.mem (γ := Set Circle)
      (range (ι := (↑unitInterval : Type)) (⇑((-x).path y) : (a : (↑unitInterval : Type)) → Circle)) x),
  JoinedIn {x}ᶜ (-x) y
Tactic: obtain hxP | hxP := (em (x ∈ range (path (-x) y))).symm
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
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
have inr : ∀ (t : (↑unitInterval : Type)),
  Membership.mem (α := Circle) (γ := Set Circle) {x}ᶜ
    ((Path.symm (y.path (-x)) : (a : (↑unitInterval : Type)) → Circle) t : Circle)
Tactic: refine ⟨(path y (-x)).symm, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (hypothesis)
Goal:
x y : Circle
hyx : y ≠ x
hxP :
  Membership.mem (γ := Set Circle)
    (range (ι := (↑unitInterval : Type)) (⇑((-x).path y) : (a : (↑unitInterval : Type)) → Circle)) x
⊢ ∀ (t : (↑unitInterval : Type)),
    Membership.mem (α := Circle) (γ := Set Circle) {x}ᶜ
      ((Path.symm (y.path (-x)) : (a : (↑unitInterval : Type)) → Circle) t : Circle)
have hne : -x ≠ y
Tactic: have hne : -x ≠ y := by
    rintro rfl
    simp [(neg_ne_self x).symm] at hxP
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (hypothesis)
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
⊢ False
have 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
Tactic: have h : x ∈ range _ ∩ _ := ⟨hxP, hP₂⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (hypothesis)
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
⊢ False
have h₁ : Membership.mem (γ := Set Circle) {-x, y} x
Tactic: rw [range_path_inter_range_path hne] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (hypothesis)
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
⊢ ∀ (t : (↑unitInterval : Type)),
    Membership.mem (α := Circle) (γ := Set Circle) {x}ᶜ
      ((Path.symm (y.path (-x)) : (a : (↑unitInterval : Type)) → Circle) t : Circle)
have hP₂ : 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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
x y : Circle
hxy : x ≠ y
⊢ ¬IsPreconnected (α := Circle) {x, y}ᶜ
have 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
Tactic: simp only [isPreconnected_iff_subset_of_disjoint_closed, not_forall, not_or, exists_and_left]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
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
have refine_1 : ¬Subset (α := Set Circle) {x, y}ᶜ
    (range (ι := (↑unitInterval : Type)) (⇑(x.path y) : (a : (↑unitInterval : Type)) → Circle))
Tactic: refine ⟨range (path x y), ?_, range (path y x), (isCompact_range (path x y).continuous).isClosed,
    (isCompact_range (path y x).continuous).isClosed, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
x y : Circle
hxy : x ≠ y
refine_1 :
  ¬Subset (α := Set Circle) {x, y}ᶜ
      (range (ι := (↑unitInterval : Type)) (⇑(x.path y) : (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
have 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))
Tactic: refine ⟨range (path x y), ?_, range (path y x), (isCompact_range (path x y).continuous).isClosed,
    (isCompact_range (path y x).continuous).isClosed, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
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))
⊢ ∃ (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
have 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)))
  ∅
Tactic: refine ⟨range (path x y), ?_, range (path y x), (isCompact_range (path x y).continuous).isClosed,
    (isCompact_range (path y x).continuous).isClosed, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
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)))
    ∅
⊢ ∃ (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
have refine_4 : ¬Subset (α := Set Circle) {x, y}ᶜ
    (range (ι := (↑unitInterval : Type)) (⇑(y.path x) : (a : (↑unitInterval : Type)) → Circle))
Tactic: refine ⟨range (path x y), ?_, range (path y x), (isCompact_range (path x y).continuous).isClosed,
    (isCompact_range (path y x).continuous).isClosed, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
x y : Circle
hxy : x ≠ y
⊢ ¬Subset (α := Set Circle) {x, y}ᶜ
      (range (ι := (↑unitInterval : Type)) (⇑(x.path y) : (a : (↑unitInterval : Type)) → Circle))
have refine_1 : ¬Eq (α := Set Circle) (range (ι := (↑unitInterval : Type)) (⇑(x.path y) : (a : (↑unitInterval : Type)) → Circle)) univ
Tactic: rw [compl_subset_iff_union, union_eq_right.mpr (by simp only [pair_subset_iff,
      (path x y).source_mem_range, (path x y).target_mem_range, and_self])]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
x y : Circle
hxy : x ≠ y
⊢ 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))
have refine_2 : Subset (α := Set Circle) {x, y}ᶜ univ
Tactic: rw [range_path_union_range_path hxy]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
x y : Circle
hxy : x ≠ y
⊢ 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)))
    ∅
have refine_3 : Eq (α := Set Circle) ({x, y}ᶜ ∩ {x, y}) ∅
Tactic: rw [range_path_inter_range_path hxy]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
x y : Circle
hxy : x ≠ y
⊢ ¬Subset (α := Set Circle) {x, y}ᶜ
      (range (ι := (↑unitInterval : Type)) (⇑(y.path x) : (a : (↑unitInterval : Type)) → Circle))
have refine_4 : ¬Eq (α := Set Circle) (range (ι := (↑unitInterval : Type)) (⇑(y.path x) : (a : (↑unitInterval : Type)) → Circle)) univ
Tactic: rw [compl_subset_iff_union, union_eq_right.mpr (by simp only [pair_subset_iff,
      (path y x).source_mem_range, (path y x).target_mem_range, and_self])]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
θ : Angle
⊢ (↑θ.toCircle : ℂ) = (↑θ.cos : ℂ) + (↑θ.sin : ℂ) * I
have h : ∀ (x : ℝ), (↑(↑x : Angle).toCircle : ℂ) = (↑(↑x : Angle).cos : ℂ) + (↑(↑x : Angle).sin : ℂ) * I
Tactic: induction θ using Angle.induction_on
Cleared hypotheses: θ
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
⊢ toCircle 0 = 1
have rw : (↑0 : Angle).toCircle = 1
Tactic: rw [← coe_zero, toCircle_coe, Circle.exp_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
rw : (↑0 : Angle).toCircle = 1
⊢ toCircle 0 = 1
have rw₁ : Eq (α := Circle) ((Circle.exp : (a : ℝ) → Circle) 0) 1
Tactic: rw [← coe_zero, toCircle_coe, Circle.exp_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
rw : (↑0 : Angle).toCircle = 1
rw₁ : Eq (α := Circle) ((Circle.exp : (a : ℝ) → Circle) 0) 1
⊢ toCircle 0 = 1
have rw₂ : Eq (α := Circle) 1 1
Tactic: rw [← coe_zero, toCircle_coe, Circle.exp_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
θ : Angle
⊢ (-θ).toCircle = θ.toCircle⁻¹
have h : ∀ (x : ℝ), (-(↑x : Angle)).toCircle = (↑x : Angle).toCircle⁻¹
Tactic: induction θ using Angle.induction_on
Cleared hypotheses: θ
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
x : ℝ
⊢ (-(↑x : Angle)).toCircle = (↑x : Angle).toCircle⁻¹
have h : (↑(-x) : Angle).toCircle = (↑x : Angle).toCircle⁻¹
Tactic: simp_rw [← coe_neg, toCircle_coe, Circle.exp_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
x : ℝ
h : (↑(-x) : Angle).toCircle = (↑x : Angle).toCircle⁻¹
⊢ (-(↑x : Angle)).toCircle = (↑x : Angle).toCircle⁻¹
have h₁ : Eq (α := Circle) ((Circle.exp : (a : ℝ) → Circle) (-x) : Circle) (((Circle.exp : (a : ℝ) → Circle) x)⁻¹ : Circle)
Tactic: simp_rw [← coe_neg, toCircle_coe, Circle.exp_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
θ₁ θ₂ : Angle
⊢ (θ₁ + θ₂).toCircle = θ₁.toCircle * θ₂.toCircle
have h : ∀ (x : ℝ), ((↑x : Angle) + θ₂).toCircle = (↑x : Angle).toCircle * θ₂.toCircle
Tactic: induction θ₁ using Angle.induction_on
Cleared hypotheses: θ₁
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
θ₂ : Angle
x : ℝ
⊢ ((↑x : Angle) + θ₂).toCircle = (↑x : Angle).toCircle * θ₂.toCircle
have h : ∀ (x_1 : ℝ), ((↑x : Angle) + (↑x_1 : Angle)).toCircle = (↑x : Angle).toCircle * (↑x_1 : Angle).toCircle
Tactic: induction θ₂ using Angle.induction_on
Cleared hypotheses: θ₂
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
θ : Angle
⊢ (↑(↑θ.toCircle : ℂ).arg : Angle) = θ
have h : ∀ (x : ℝ), (↑(↑(↑x : Angle).toCircle : ℂ).arg : Angle) = (↑x : Angle)
Tactic: induction θ using Angle.induction_on
Cleared hypotheses: θ
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
x : ℝ
⊢ (↑(↑(↑x : Angle).toCircle : ℂ).arg : Angle) = (↑x : Angle)
have h : (↑(arg (↑((Circle.exp : (a : ℝ) → Circle) x) : ℂ)) : Angle) = (↑x : Angle)
Tactic: rw [toCircle_coe, Circle.coe_exp, exp_mul_I, ← ofReal_cos, ← ofReal_sin, ←
    Angle.cos_coe, ← Angle.sin_coe, arg_cos_add_sin_mul_I_coe_angle]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Circle (goal)
Goal:
x : ℝ
h : (↑(arg (↑((Circle.exp : (a : ℝ) → Circle) x) : ℂ)) : Angle) = (↑x : Angle)
⊢ (↑(↑(↑x : Angle).toCircle : ℂ).arg : Angle) = (↑x : Angle)
have h₁ : (↑(cexp ((↑x : ℂ) * I)).arg : Angle) = (↑x : Angle)
Tactic: rw [toCircle_coe, Circle.coe_exp, exp_mul_I, ← ofReal_cos, ← ofReal_sin, ←
    Angle.cos_coe, ← Angle.sin_coe, arg_cos_add_sin_mul_I_coe_angle]