awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrdConnectedComponent (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
⊢ Eq.{u_1 + 1} (α := Set αᵒᵈ)
    (range fun (x : (↑((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s) : Type u_1)) ↦
      Nonempty.some (s := ordConnectedComponent ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s) (↑x : αᵒᵈ)) ⋯)
    (preimage (β := α) (⇑ofDual : (a : αᵒᵈ) → α)
      (range fun (x : (↑s : Type u_1)) ↦ Nonempty.some (s := s.ordConnectedComponent (↑x : α)) ⋯))
have h : ∀ (x : αᵒᵈ),
  Membership.mem (γ := Set αᵒᵈ)
      (range fun (x : (↑((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s) : Type u_1)) ↦
        Nonempty.some (s := ordConnectedComponent ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s) (↑x : αᵒᵈ)) sorry)
      x ↔
    Membership.mem (γ := Set αᵒᵈ)
      (preimage (β := α) (⇑ofDual : (a : αᵒᵈ) → α)
        (range fun (x : (↑s : Type u_1)) ↦ Nonempty.some (s := s.ordConnectedComponent (↑x : α)) sorry))
      x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrdConnectedComponent (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
x : αᵒᵈ
⊢ Membership.mem (γ := Set αᵒᵈ)
      (range fun (x : (↑((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s) : Type u_1)) ↦
        Nonempty.some (s := ordConnectedComponent ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s) (↑x : αᵒᵈ)) ⋯)
      x ↔
    Membership.mem (γ := Set αᵒᵈ)
      (preimage (β := α) (⇑ofDual : (a : αᵒᵈ) → α)
        (range fun (x : (↑s : Type u_1)) ↦ Nonempty.some (s := s.ordConnectedComponent (↑x : α)) ⋯))
      x
have h : (∃ (a : α) (h : a ∈ s), Nonempty.some (s := (⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s.ordConnectedComponent a) sorry = x) ↔
  ∃ (a : α) (h : a ∈ s), Nonempty.some (s := s.ordConnectedComponent a) sorry = (ofDual : (a : αᵒᵈ) → α) x
Tactic: simp only [mem_range, Subtype.exists, mem_preimage, OrderDual.exists, dual_ordConnectedComponent,
    ofDual_toDual]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrdConnectedComponent (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
x : αᵒᵈ
⊢ (∃ (a : α) (h : a ∈ s), Nonempty.some (s := (⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s.ordConnectedComponent a) ⋯ = x) ↔
    ∃ (a : α) (h : a ∈ s), Nonempty.some (s := s.ordConnectedComponent a) ⋯ = (ofDual : (a : αᵒᵈ) → α) x
have h : (∃ (a : α) (h : a ∈ s), Nonempty.some (s := (⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s.ordConnectedComponent a) sorry = x) →
  ∃ (a : α) (h : a ∈ s), Nonempty.some (s := s.ordConnectedComponent a) sorry = (ofDual : (a : αᵒᵈ) → α) x
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrdConnectedComponent (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
x : αᵒᵈ
h :
  (∃ (a : α) (h : a ∈ s), Nonempty.some (s := (⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s.ordConnectedComponent a) ⋯ = x) →
    ∃ (a : α) (h : a ∈ s), Nonempty.some (s := s.ordConnectedComponent a) ⋯ = (ofDual : (a : αᵒᵈ) → α) x
⊢ (∃ (a : α) (h : a ∈ s), Nonempty.some (s := (⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s.ordConnectedComponent a) ⋯ = x) ↔
    ∃ (a : α) (h : a ∈ s), Nonempty.some (s := s.ordConnectedComponent a) ⋯ = (ofDual : (a : αᵒᵈ) → α) x
have h₁ : (∃ (a : α) (h : a ∈ s), Nonempty.some (s := s.ordConnectedComponent a) sorry = (ofDual : (a : αᵒᵈ) → α) x) →
  ∃ (a : α) (h : a ∈ s), Nonempty.some (s := (⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s.ordConnectedComponent a) sorry = x
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrdConnectedComponent (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
x : αᵒᵈ
h :
  (∃ (a : α) (h : a ∈ s), Nonempty.some (s := (⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s.ordConnectedComponent a) ⋯ = x) →
    ∃ (a : α) (h : a ∈ s), Nonempty.some (s := s.ordConnectedComponent a) ⋯ = (ofDual : (a : αᵒᵈ) → α) x
h₁ :
  (∃ (a : α) (h : a ∈ s), Nonempty.some (s := s.ordConnectedComponent a) ⋯ = (ofDual : (a : αᵒᵈ) → α) x) →
    ∃ (a : α) (h : a ∈ s), Nonempty.some (s := (⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s.ordConnectedComponent a) ⋯ = x
⊢ (∃ (a : α) (h : a ∈ s), Nonempty.some (s := (⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s.ordConnectedComponent a) ⋯ = x) ↔
    ∃ (a : α) (h : a ∈ s), Nonempty.some (s := s.ordConnectedComponent a) ⋯ = (ofDual : (a : αᵒᵈ) → α) x
have h₂ : ∀ (w : α) (w_1 : w ∈ s),
  Nonempty.some (s := (⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s.ordConnectedComponent w) sorry = x →
    ∃ (a : α) (h : a ∈ s), Nonempty.some (s := s.ordConnectedComponent a) sorry = (ofDual : (a : αᵒᵈ) → α) x
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrdConnectedComponent (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
x : αᵒᵈ
h :
  (∃ (a : α) (h : a ∈ s), Nonempty.some (s := (⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s.ordConnectedComponent a) ⋯ = x) →
    ∃ (a : α) (h : a ∈ s), Nonempty.some (s := s.ordConnectedComponent a) ⋯ = (ofDual : (a : αᵒᵈ) → α) x
h₁ :
  (∃ (a : α) (h : a ∈ s), Nonempty.some (s := s.ordConnectedComponent a) ⋯ = (ofDual : (a : αᵒᵈ) → α) x) →
    ∃ (a : α) (h : a ∈ s), Nonempty.some (s := (⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s.ordConnectedComponent a) ⋯ = x
h₂ h₃ h₄ :
  ∀ (w : α) (w_1 : w ∈ s),
    Nonempty.some (s := (⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s.ordConnectedComponent w) ⋯ = x →
      ∃ (a : α) (h : a ∈ s), Nonempty.some (s := s.ordConnectedComponent a) ⋯ = (ofDual : (a : αᵒᵈ) → α) x
⊢ (∃ (a : α) (h : a ∈ s), Nonempty.some (s := (⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s.ordConnectedComponent a) ⋯ = x) ↔
    ∃ (a : α) (h : a ∈ s), Nonempty.some (s := s.ordConnectedComponent a) ⋯ = (ofDual : (a : αᵒᵈ) → α) x
have h₅ : ∀ (w : α) (w_1 : w ∈ s),
  Nonempty.some (s := s.ordConnectedComponent w) sorry = (ofDual : (a : αᵒᵈ) → α) x →
    ∃ (a : α) (h : a ∈ s), Nonempty.some (s := (⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s.ordConnectedComponent a) sorry = x
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrdConnectedComponent (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
x y : α
hx : x ∈ s.ordConnectedSection
hy : y ∈ s.ordConnectedSection
h : [[x, y]] ⊆ s
⊢ x = y
have rcases : ∀ (x : (↑s : Type u_1)) (h : [[s.ordConnectedProj x, y]] ⊆ s), s.ordConnectedProj x = y
Tactic: rcases hx with ⟨x, rfl⟩
Cleared hypotheses: x, hx, h
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrdConnectedComponent (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
y : α
hy : y ∈ s.ordConnectedSection
x : (↑s : Type u_1)
h : [[s.ordConnectedProj x, y]] ⊆ s
⊢ s.ordConnectedProj x = y
have rcases : ∀ (y : (↑s : Type u_1)) (h : [[s.ordConnectedProj x, s.ordConnectedProj y]] ⊆ s),
  s.ordConnectedProj x = s.ordConnectedProj y
Tactic: rcases hy with ⟨y, rfl⟩
Cleared hypotheses: y, hy, h
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrdConnectedComponent (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s t : Set α
⊢ Disjoint (s.ordT5Nhd t) (t.ordT5Nhd s)
have rw : s.ordT5Nhd t ⊓ t.ordT5Nhd s ≤ ⊥
Tactic: rw [disjoint_iff_inf_le]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrdConnectedComponent (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s t : Set α
x : α
hx₁ : x ∈ s.ordT5Nhd t
hx₂ : x ∈ t.ordT5Nhd s
⊢ Membership.mem (γ := Set α) ⊥ x
have rcases : ∀ (a : α) (has : a ∈ s) (ha : x ∈ (tᶜ ∩ (s.ordSeparatingSet t).ordConnectedSectionᶜ).ordConnectedComponent a),
  Membership.mem (γ := Set α) ⊥ x
Tactic: rcases mem_iUnion₂.1 hx₁ with ⟨a, has, ha⟩
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrdConnectedComponent (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s t : Set α
x : α
hx₂ : x ∈ t.ordT5Nhd s
a : α
has : a ∈ s
ha : x ∈ (tᶜ ∩ (s.ordSeparatingSet t).ordConnectedSectionᶜ).ordConnectedComponent a
⊢ Membership.mem (γ := Set α) ⊥ x
have rcases : ∀ (b : α) (hbt : b ∈ t) (hb : x ∈ (sᶜ ∩ (t.ordSeparatingSet s).ordConnectedSectionᶜ).ordConnectedComponent b),
  Membership.mem (γ := Set α) ⊥ x
Tactic: rcases mem_iUnion₂.1 hx₂ with ⟨b, hbt, hb⟩
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrdConnectedComponent (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s t : Set α
x a : α
has : a ∈ s
ha : x ∈ (tᶜ ∩ (s.ordSeparatingSet t).ordConnectedSectionᶜ).ordConnectedComponent a
b : α
hbt : b ∈ t
hb : x ∈ (sᶜ ∩ (t.ordSeparatingSet s).ordConnectedSectionᶜ).ordConnectedComponent b
⊢ Membership.mem (γ := Set α) ⊥ x
have rw : ∀ (ha : [[a, x]] ⊆ tᶜ ∧ [[a, x]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ) (b : α) (hbt : b ∈ t)
  (hb : [[b, x]] ⊆ sᶜ ∧ [[b, x]] ⊆ (t.ordSeparatingSet s).ordConnectedSectionᶜ), Membership.mem (γ := Set α) ⊥ x
Tactic: rw [mem_ordConnectedComponent, subset_inter_iff] at ha hb
Cleared hypotheses: ha, b, hbt, hb
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrdConnectedComponent (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s t : Set α
x a : α
has : a ∈ s
ha : [[a, x]] ⊆ tᶜ ∧ [[a, x]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ
b : α
hbt : b ∈ t
hb : [[b, x]] ⊆ sᶜ ∧ [[b, x]] ⊆ (t.ordSeparatingSet s).ordConnectedSectionᶜ
⊢ Membership.mem (γ := Set α) ⊥ x
have inr : ∀
  (H :
    ∀ {α : Type u_1} [inst : LinearOrder α] {s t : Set α} ⦃x : α⦄ (a : α) (has : a ∈ s)
      (ha : [[a, x]] ⊆ tᶜ ∧ [[a, x]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ) (b : α) (hbt : b ∈ t)
      (hb : [[b, x]] ⊆ sᶜ ∧ [[b, x]] ⊆ (t.ordSeparatingSet s).ordConnectedSectionᶜ) (hab : a ≤ b),
      Membership.mem (γ := Set α) ⊥ x)
  (hab : ¬a ≤ b), Membership.mem (γ := Set α) ⊥ x
Tactic: wlog hab : a ≤ b with H
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrdConnectedComponent (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s t : Set α
x a : α
has : a ∈ s
ha : [[a, x]] ⊆ tᶜ ∧ [[a, x]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ
b : α
hbt : b ∈ t
hb : [[b, x]] ⊆ sᶜ ∧ [[b, x]] ⊆ (t.ordSeparatingSet s).ordConnectedSectionᶜ
inr :
  ∀
    (H :
      ∀ {α : Type u_1} [inst : LinearOrder α] {s t : Set α} ⦃x : α⦄ (a : α) (has : a ∈ s)
        (ha : [[a, x]] ⊆ tᶜ ∧ [[a, x]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ) (b : α) (hbt : b ∈ t)
        (hb : [[b, x]] ⊆ sᶜ ∧ [[b, x]] ⊆ (t.ordSeparatingSet s).ordConnectedSectionᶜ) (hab : a ≤ b),
        Membership.mem (γ := Set α) ⊥ x)
    (hab : ¬a ≤ b), Membership.mem (γ := Set α) ⊥ x
⊢ Membership.mem (γ := Set α) ⊥ x
have wlog : ∀ {α : Type u_1} [inst : LinearOrder α] {s t : Set α} ⦃x : α⦄ (a : α) (has : a ∈ s)
  (ha : [[a, x]] ⊆ tᶜ ∧ [[a, x]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ) (b : α) (hbt : b ∈ t)
  (hb : [[b, x]] ⊆ sᶜ ∧ [[b, x]] ⊆ (t.ordSeparatingSet s).ordConnectedSectionᶜ) (hab : a ≤ b),
  Membership.mem (γ := Set α) ⊥ x
Tactic: wlog hab : a ≤ b with H
Cleared hypotheses: x, a, has, ha, b, hbt, hb
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrdConnectedComponent (hypothesis)
Goal:
α_1 : Type u_1
inst : LinearOrder α_1
s_1 t_1 : Set α_1
α : Type u_1
inst_1 : LinearOrder α
s t : Set α
x a : α
has : a ∈ s
ha : [[a, x]] ⊆ tᶜ ∧ [[a, x]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ
b : α
hbt : b ∈ t
hb : [[b, x]] ⊆ sᶜ ∧ [[b, x]] ⊆ (t.ordSeparatingSet s).ordConnectedSectionᶜ
hab : a ≤ b
⊢ Membership.mem (γ := Set α) ⊥ x
have ha₁ : [[a, x]] ⊆ tᶜ
Tactic: obtain ⟨ha, ha'⟩ := ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrdConnectedComponent (hypothesis)
Goal:
α_1 : Type u_1
inst : LinearOrder α_1
s_1 t_1 : Set α_1
α : Type u_1
inst_1 : LinearOrder α
s t : Set α
x a : α
has : a ∈ s
ha : [[a, x]] ⊆ tᶜ ∧ [[a, x]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ
b : α
hbt : b ∈ t
hb : [[b, x]] ⊆ sᶜ ∧ [[b, x]] ⊆ (t.ordSeparatingSet s).ordConnectedSectionᶜ
hab : a ≤ b
ha₁ : [[a, x]] ⊆ tᶜ
⊢ Membership.mem (γ := Set α) ⊥ x
have ha' : [[a, x]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ
Tactic: obtain ⟨ha, ha'⟩ := ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrdConnectedComponent (hypothesis)
Goal:
α_1 : Type u_1
inst : LinearOrder α_1
s_1 t_1 : Set α_1
α : Type u_1
inst_1 : LinearOrder α
s t : Set α
x a : α
has : a ∈ s
b : α
hbt : b ∈ t
hb : [[b, x]] ⊆ sᶜ ∧ [[b, x]] ⊆ (t.ordSeparatingSet s).ordConnectedSectionᶜ
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
ha' : [[a, x]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ
⊢ Membership.mem (γ := Set α) ⊥ x
have hb₁ : [[b, x]] ⊆ sᶜ
Tactic: obtain ⟨hb, hb'⟩ := hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrdConnectedComponent (hypothesis)
Goal:
α_1 : Type u_1
inst : LinearOrder α_1
s_1 t_1 : Set α_1
α : Type u_1
inst_1 : LinearOrder α
s t : Set α
x a : α
has : a ∈ s
b : α
hbt : b ∈ t
hb : [[b, x]] ⊆ sᶜ ∧ [[b, x]] ⊆ (t.ordSeparatingSet s).ordConnectedSectionᶜ
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
ha' : [[a, x]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ
hb₁ : [[b, x]] ⊆ sᶜ
⊢ Membership.mem (γ := Set α) ⊥ x
have hb' : [[b, x]] ⊆ (t.ordSeparatingSet s).ordConnectedSectionᶜ
Tactic: obtain ⟨hb, hb'⟩ := hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrdConnectedComponent (hypothesis)
Goal:
α_1 : Type u_1
inst : LinearOrder α_1
s_1 t_1 : Set α_1
α : Type u_1
inst_1 : LinearOrder α
s t : Set α
x a : α
has : a ∈ s
b : α
hbt : b ∈ t
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
ha' : [[a, x]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ
hb : [[b, x]] ⊆ sᶜ
hb' : [[b, x]] ⊆ (t.ordSeparatingSet s).ordConnectedSectionᶜ
⊢ [[a, b]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ
have hb'₁ : [[x, b]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ
Tactic: rw [ordSeparatingSet_comm, uIcc_comm] at hb'
Cleared hypotheses: hb'
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrdConnectedComponent (hypothesis)
Goal:
α_1 : Type u_1
inst : LinearOrder α_1
s_1 t_1 : Set α_1
α : Type u_1
inst_1 : LinearOrder α
s t : Set α
x a : α
has : a ∈ s
b : α
hbt : b ∈ t
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
ha' : [[a, x]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ
hb : [[b, x]] ⊆ sᶜ
hb' : [[b, x]] ⊆ (t.ordSeparatingSet s).ordConnectedSectionᶜ
⊢ Membership.mem (γ := Set α) ⊥ x
have hsub : [[a, b]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ
Tactic: have hsub : [[a, b]] ⊆ (ordSeparatingSet s t).ordConnectedSectionᶜ := by
    rw [ordSeparatingSet_comm, uIcc_comm] at hb'
    calc
      [[a, b]] ⊆ [[a, x]] ∪ [[x, b]] := uIcc_subset_uIcc_union_uIcc
      _ ⊆ (ordSeparatingSet s t).ordConnectedSectionᶜ := union_subset ha' hb'
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrdConnectedComponent (goal)
Goal:
α_1 : Type u_1
inst : LinearOrder α_1
s_1 t_1 : Set α_1
α : Type u_1
inst_1 : LinearOrder α
s t : Set α
x a : α
has : a ∈ s
b : α
hbt : b ∈ t
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
hb : [[b, x]] ⊆ sᶜ
hsub : [[a, b]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ
⊢ Membership.mem (γ := Set α) ⊥ x
have inl : ∀ (hxa : x ≤ a), Membership.mem (γ := Set α) ⊥ x
Tactic: rcases le_total x a with hxa | hax
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrdConnectedComponent (goal)
Goal:
α_1 : Type u_1
inst : LinearOrder α_1
s_1 t_1 : Set α_1
α : Type u_1
inst_1 : LinearOrder α
s t : Set α
x a : α
has : a ∈ s
b : α
hbt : b ∈ t
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
hb : [[b, x]] ⊆ sᶜ
hsub : [[a, b]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ
inl : ∀ (hxa : x ≤ a), Membership.mem (γ := Set α) ⊥ x
⊢ Membership.mem (γ := Set α) ⊥ x
have inr : ∀ (hax : a ≤ x), Membership.mem (γ := Set α) ⊥ x
Tactic: rcases le_total x a with hxa | hax
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrdConnectedComponent (goal)
Goal:
α_1 : Type u_1
inst : LinearOrder α_1
s_1 t_1 : Set α_1
α : Type u_1
inst_1 : LinearOrder α
s t : Set α
x a : α
has : a ∈ s
b : α
hbt : b ∈ t
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
hb : [[b, x]] ⊆ sᶜ
hsub : [[a, b]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ
hax : a ≤ x
⊢ Membership.mem (γ := Set α) ⊥ x
have inr : ∀ (hbx : b ≤ x), Membership.mem (γ := Set α) ⊥ x
Tactic: rcases le_total b x with hbx | hxb
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrdConnectedComponent (goal)
Goal:
α_1 : Type u_1
inst : LinearOrder α_1
s_1 t_1 : Set α_1
α : Type u_1
inst_1 : LinearOrder α
s t : Set α
x a : α
has : a ∈ s
b : α
hbt : b ∈ t
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
hb : [[b, x]] ⊆ sᶜ
hsub : [[a, b]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ
hax : a ≤ x
inr : ∀ (hbx : b ≤ x), Membership.mem (γ := Set α) ⊥ x
⊢ Membership.mem (γ := Set α) ⊥ x
have inr₁ : ∀ (hxb : x ≤ b), Membership.mem (γ := Set α) ⊥ x
Tactic: rcases le_total b x with hbx | hxb
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrdConnectedComponent (hypothesis)
Goal:
α_1 : Type u_1
inst : LinearOrder α_1
s_1 t_1 : Set α_1
α : Type u_1
inst_1 : LinearOrder α
s t : Set α
x a : α
has : a ∈ s
b : α
hbt : b ∈ t
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
hb : [[b, x]] ⊆ sᶜ
hsub : [[a, b]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ
hax : a ≤ x
hxb : x ≤ b
⊢ Membership.mem (γ := Set α) ⊥ x
have h' : x ∈ s.ordSeparatingSet t
Tactic: have h' : x ∈ ordSeparatingSet s t := ⟨mem_iUnion₂.2 ⟨a, has, ha⟩, mem_iUnion₂.2 ⟨b, hbt, hb⟩⟩
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrdConnectedComponent (goal)
Goal:
α_1 : Type u_1
inst : LinearOrder α_1
s_1 t_1 : Set α_1
α : Type u_1
inst_1 : LinearOrder α
s t : Set α
x a : α
has : a ∈ s
b : α
hbt : b ∈ t
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
hb : [[b, x]] ⊆ sᶜ
hsub : [[a, b]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ
hax : a ≤ x
hxb : x ≤ b
h' : x ∈ s.ordSeparatingSet t
⊢ Membership.mem (γ := Set α) ⊥ x
have inr : ∀ (x : { x : α // x ∈ s.ordSeparatingSet t }) (ha : [[a, (↑x : α)]] ⊆ tᶜ) (hb : [[b, (↑x : α)]] ⊆ sᶜ)
  (hax : a ≤ (↑x : α)) (hxb : (↑x : α) ≤ b), Membership.mem (γ := Set α) ⊥ (↑x : α)
Tactic: lift x to ordSeparatingSet s t using h'
Cleared hypotheses: x, ha, hb, hax, hxb, h'
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrdConnectedComponent (goal)
Goal:
α_1 : Type u_1
inst : LinearOrder α_1
s_1 t_1 : Set α_1
α : Type u_1
inst_1 : LinearOrder α
s t : Set α
a : α
has : a ∈ s
b : α
hbt : b ∈ t
hab : a ≤ b
hsub : [[a, b]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ
x : { x : α // x ∈ s.ordSeparatingSet t }
ha : [[a, (↑x : α)]] ⊆ tᶜ
hb : [[b, (↑x : α)]] ⊆ sᶜ
hax : a ≤ (↑x : α)
hxb : (↑x : α) ≤ b
⊢ Membership.mem (γ := Set α) ⊥ (↑x : α)
have inr : (s.ordSeparatingSet t).ordConnectedComponent (↑x : α) ⊆ [[a, b]]
Tactic: suffices ordConnectedComponent (ordSeparatingSet s t) x ⊆ [[a, b]] from
    hsub (this <| ordConnectedProj_mem_ordConnectedComponent _ x) (mem_range_self _)
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrdConnectedComponent (goal)
Goal:
α_1 : Type u_1
inst : LinearOrder α_1
s_1 t_1 : Set α_1
α : Type u_1
inst_1 : LinearOrder α
s t : Set α
a : α
has : a ∈ s
b : α
hbt : b ∈ t
hab : a ≤ b
hsub : [[a, b]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ
x : { x : α // x ∈ s.ordSeparatingSet t }
ha : [[a, (↑x : α)]] ⊆ tᶜ
hb : [[b, (↑x : α)]] ⊆ sᶜ
hax : a ≤ (↑x : α)
hxb : (↑x : α) ≤ b
y : α
hy : y ∈ (s.ordSeparatingSet t).ordConnectedComponent (↑x : α)
⊢ y ∈ [[a, b]]
have inr : ¬y < a ∧ ¬b < y
Tactic: rw [uIcc_of_le hab, mem_Icc, ← not_lt, ← not_lt]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrdConnectedComponent (hypothesis)
Goal:
α_1 : Type u_1
inst : LinearOrder α_1
s_1 t_1 : Set α_1
α : Type u_1
inst_1 : LinearOrder α
s t : Set α
a : α
has : a ∈ s
b : α
hbt : b ∈ t
hab : a ≤ b
hsub : [[a, b]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ
x : { x : α // x ∈ s.ordSeparatingSet t }
ha : [[a, (↑x : α)]] ⊆ tᶜ
hb : [[b, (↑x : α)]] ⊆ sᶜ
hax : a ≤ (↑x : α)
hxb : (↑x : α) ≤ b
y : α
hy : y ∈ (s.ordSeparatingSet t).ordConnectedComponent (↑x : α)
⊢ ¬y < a ∧ ¬b < y
have sol1 : ∀ (hya : y < a), False
Tactic: have sol1 := fun (hya : y < a) =>
      (disjoint_left (t := ordSeparatingSet s t)).1 disjoint_left_ordSeparatingSet has
        (hy <| Icc_subset_uIcc' ⟨hya.le, hax⟩)
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrdConnectedComponent (hypothesis)
Goal:
α_1 : Type u_1
inst : LinearOrder α_1
s_1 t_1 : Set α_1
α : Type u_1
inst_1 : LinearOrder α
s t : Set α
a : α
has : a ∈ s
b : α
hbt : b ∈ t
hab : a ≤ b
hsub : [[a, b]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ
x : { x : α // x ∈ s.ordSeparatingSet t }
ha : [[a, (↑x : α)]] ⊆ tᶜ
hb : [[b, (↑x : α)]] ⊆ sᶜ
hax : a ≤ (↑x : α)
hxb : (↑x : α) ≤ b
y : α
hy : y ∈ (s.ordSeparatingSet t).ordConnectedComponent (↑x : α)
sol1 : ∀ (hya : y < a), False
⊢ ¬y < a ∧ ¬b < y
have sol2 : ∀ (hby : b < y), False
Tactic: have sol2 := fun (hby : b < y) =>
      (disjoint_left (t := ordSeparatingSet s t)).1 disjoint_right_ordSeparatingSet hbt
        (hy <| Icc_subset_uIcc ⟨hxb, hby.le⟩)
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrdConnectedLinear (goal)
Goal:
α : Type u_1
I : Set α
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
⊢ I.OrdConnected ↔ ∀ x ∈ I, ∀ y ∈ I, Disjoint (Ioo x y) I → Ioo x y = ∅
have simp_rw : I.OrdConnected ↔ ∀ x ∈ I, ∀ y ∈ I, Ioo x y ⊆ Iᶜ → Ioo x y = ∅
Tactic: simp_rw [← Set.subset_compl_iff_disjoint_right]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrdConnectedLinear (goal)
Goal:
α : Type u_1
I : Set α
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
⊢ I.OrdConnected ↔ ∀ x ∈ I, ∀ y ∈ I, Ioo x y ⊆ Iᶜ → Ioo x y = ∅
have refine_1 : ∀ (h' : I.OrdConnected) (x : α) (hx : x ∈ I) (y : α) (hy : y ∈ I) (hxy : Ioo x y ⊆ Iᶜ), Ioo x y = ∅
Tactic: refine ⟨fun h' x hx y hy hxy ↦ ?_, fun h' ↦ ordConnected_of_Ioo fun x hx y hy hxy z hz ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrdConnectedLinear (goal)
Goal:
α : Type u_1
I : Set α
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
refine_1 : ∀ (h' : I.OrdConnected) (x : α) (hx : x ∈ I) (y : α) (hy : y ∈ I) (hxy : Ioo x y ⊆ Iᶜ), Ioo x y = ∅
⊢ I.OrdConnected ↔ ∀ x ∈ I, ∀ y ∈ I, Ioo x y ⊆ Iᶜ → Ioo x y = ∅
have refine_2 : ∀ (h' : ∀ x ∈ I, ∀ y ∈ I, Ioo x y ⊆ Iᶜ → Ioo x y = ∅) (x : α) (hx : x ∈ I) (y : α) (hy : y ∈ I) (hxy : x < y) (z : α)
  (hz : z ∈ Ioo x y), z ∈ I
Tactic: refine ⟨fun h' x hx y hy hxy ↦ ?_, fun h' ↦ ordConnected_of_Ioo fun x hx y hy hxy z hz ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrdConnectedLinear (goal)
Goal:
α : Type u_1
I : Set α
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
h' : I.OrdConnected
x : α
hx : x ∈ I
y : α
hy : y ∈ I
hxy : Ioo x y ⊆ Iᶜ
this : ∀ (z : α), x < z → y ≤ z
⊢ Ioo x y = ∅
have h : ∀ (z : α), z ∈ Ioo x y ↔ Membership.mem (γ := Set α) ∅ z
Tactic: ext z
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrdConnectedLinear (goal)
Goal:
α : Type u_1
I : Set α
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
h' : I.OrdConnected
x : α
hx : x ∈ I
y : α
hy : y ∈ I
hxy : Ioo x y ⊆ Iᶜ
⊢ Ioo x y = ∅
have refine_1 : ∀ (z : α), x < z → y ≤ z
Tactic: suffices ∀ z, x < z → y ≤ z by ext z; simpa using this z
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrdConnectedLinear (goal)
Goal:
α : Type u_1
I : Set α
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
h' : I.OrdConnected
x : α
hx : x ∈ I
y : α
hy : y ∈ I
hxy : Ioo x y ⊆ Iᶜ
z : α
hz : x < z
⊢ y ≤ z
have refine_1 : z ∉ Ioo x y
Tactic: suffices z ∉ Ioo x y by simp_all
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrdConnectedLinear (goal)
Goal:
α : Type u_1
I : Set α
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
h' : ∀ x ∈ I, ∀ y ∈ I, Ioo x y ⊆ Iᶜ → Ioo x y = ∅
x : α
hx : x ∈ I
y : α
hy : y ∈ I
hxy : x < y
z : α
hz : z ∈ Ioo x y
⊢ z ∈ I
have refine_2 : ∀ (hz' : z ∉ I), False
Tactic: by_contra hz'
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrdConnectedLinear (goal)
Goal:
α : Type u_1
I : Set α
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
h' : ∀ x ∈ I, ∀ y ∈ I, Ioo x y ⊆ Iᶜ → Ioo x y = ∅
x : α
hx : x ∈ I
y : α
hy : y ∈ I
hxy : x < y
z : α
hz : z ∈ Ioo x y
hz' : z ∉ I
⊢ False
have refine_2 : ∀ (x' : α) (hx' : x ≤ x') (hx'' : Maximal (fun (x_1 : α) ↦ x_1 ∈ I ∩ Icc x z) x'), False
Tactic: obtain ⟨x', hx', hx''⟩ :=
      ((finite_Icc x z).inter_of_right I).exists_le_maximal ⟨hx, le_refl _, hz.1.le⟩
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrdConnectedLinear (hypothesis)
Goal:
α : Type u_1
I : Set α
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
h' : ∀ x ∈ I, ∀ y ∈ I, Ioo x y ⊆ Iᶜ → Ioo x y = ∅
x : α
hx : x ∈ I
y : α
hy : y ∈ I
hxy : x < y
z : α
hz : z ∈ Ioo x y
hz' : z ∉ I
x' : α
hx' : x ≤ x'
hx'' : Maximal (fun (x_1 : α) ↦ x_1 ∈ I ∩ Icc x z) x'
⊢ False
have hxz : x' < z
Tactic: have hxz : x' < z := lt_of_le_of_ne hx''.1.2.2 (ne_of_mem_of_not_mem hx''.1.1 hz')
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrdConnectedLinear (goal)
Goal:
α : Type u_1
I : Set α
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
h' : ∀ x ∈ I, ∀ y ∈ I, Ioo x y ⊆ Iᶜ → Ioo x y = ∅
x : α
hx : x ∈ I
y : α
hy : y ∈ I
hxy : x < y
z : α
hz : z ∈ Ioo x y
hz' : z ∉ I
x' : α
hx' : x ≤ x'
hx'' : Maximal (fun (x_1 : α) ↦ x_1 ∈ I ∩ Icc x z) x'
hxz : x' < z
⊢ False
have refine_2 : ∀ (y' : α) (hy' : y' ≤ y) (hy'' : Minimal (fun (x : α) ↦ x ∈ I ∩ Icc z y) y'), False
Tactic: obtain ⟨y', hy', hy''⟩ :=
      ((finite_Icc z y).inter_of_right I).exists_le_minimal ⟨hy, hz.2.le, le_refl _⟩