awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Interval.Set.OrdConnectedComponent
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
x y : (↑s : Type u_1)
h : [[s.ordConnectedProj x, s.ordConnectedProj y]] ⊆ s
⊢ s.ordConnectedProj x = s.ordConnectedProj y

Tactic:
ordConnectedProj_eq.2
      (mem_ordConnectedComponent_trans
        (mem_ordConnectedComponent_trans (ordConnectedProj_mem_ordConnectedComponent _ _) h)
        (mem_ordConnectedComponent_ordConnectedProj _ _))

Premises used: Iff.mpr, Set.mem_ordConnectedComponent_trans, Set.mem_ordConnectedComponent_ordConnectedProj, Set.ordConnectedProj_eq, Set.ordConnectedProj_mem_ordConnectedComponent
-- Module: Mathlib.Order.Interval.Set.OrdConnectedComponent
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
x y : (↑s : Type u_1)
h : [[s.ordConnectedProj x, s.ordConnectedProj y]] ⊆ s
⊢ s.ordConnectedProj x = s.ordConnectedProj y

Tactic:
exact
    ordConnectedProj_eq.2
      (mem_ordConnectedComponent_trans
        (mem_ordConnectedComponent_trans (ordConnectedProj_mem_ordConnectedComponent _ _) h)
        (mem_ordConnectedComponent_ordConnectedProj _ _))

Premises used: Iff.mpr, Set.mem_ordConnectedComponent_trans, Set.mem_ordConnectedComponent_ordConnectedProj, Set.ordConnectedProj_eq, Set.ordConnectedProj_mem_ordConnectedComponent
-- Module: Mathlib.Order.Interval.Set.OrdConnectedComponent
Goal:
α : Type u_1
inst : LinearOrder α
s t : Set α
⊢ s.ordSeparatingSet t = t.ordSeparatingSet s

Tactic:
inter_comm _ _

Premises used: Set.ordSeparatingSet, Set.inter_comm
-- Module: Mathlib.Order.Interval.Set.OrdConnectedComponent
Goal:
α : Type u_1
inst : LinearOrder α
s t : Set α
⊢ Disjoint s (s.ordSeparatingSet t)

Tactic:
Disjoint.inter_right' _ <|
    disjoint_iUnion₂_right.2 fun _ _ =>
      disjoint_compl_right.mono_right <| ordConnectedComponent_subset

Premises used: Iff.mpr, Set.ordSeparatingSet, Set.disjoint_iUnion₂_right, Set.ordConnectedComponent_subset, disjoint_compl_right, Disjoint.inter_right', Disjoint.mono_right
-- Module: Mathlib.Order.Interval.Set.OrdConnectedComponent
Goal:
α : Type u_1
inst : LinearOrder α
s t : Set α
⊢ Disjoint t (s.ordSeparatingSet t)

Tactic:
ordSeparatingSet_comm t s ▸ disjoint_left_ordSeparatingSet

Premises used: Set.ordSeparatingSet_comm, Eq.rec, Set.disjoint_left_ordSeparatingSet
-- Module: Mathlib.Order.Interval.Set.OrdConnectedComponent
Goal:
α : Type u_1
inst : LinearOrder α
s t : Set α
⊢ Eq (α := Set αᵒᵈ) (ordSeparatingSet ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s) ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' t))
    ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s.ordSeparatingSet t)

Tactic:
simp only [ordSeparatingSet, mem_preimage, ← toDual.surjective.iUnion_comp, ofDual_toDual,
    dual_ordConnectedComponent, ← preimage_compl, preimage_inter, preimage_iUnion]

Premises used: OrderDual.toDual, Set.preimage_inter, Set.dual_ordConnectedComponent, Set.ordSeparatingSet, Function.Surjective.iUnion_comp, Set.preimage_iUnion, OrderDual.ofDual_toDual, Equiv.surjective, Set.preimage_compl, Set.mem_preimage
-- Module: Mathlib.Order.Interval.Set.OrdConnectedComponent
Goal:
α : Type u_1
inst : LinearOrder α
s t : Set α
rw : s.ordT5Nhd t ⊓ t.ordT5Nhd s ≤ ⊥
⊢ Disjoint (s.ordT5Nhd t) (t.ordT5Nhd s)

Tactic:
rw [disjoint_iff_inf_le]

Premises used: disjoint_iff_inf_le
-- Module: Mathlib.Order.Interval.Set.OrdConnectedComponent
Goal:
α : Type u_1
inst : LinearOrder α
s t : Set α
x : α
hx₁ : x ∈ s.ordT5Nhd t
hx₂ : x ∈ t.ordT5Nhd s
rcases :
  ∀ (a : α) (has : a ∈ s) (ha : x ∈ (tᶜ ∩ (s.ordSeparatingSet t).ordConnectedSectionᶜ).ordConnectedComponent a),
    Membership.mem (γ := Set α) ⊥ x
⊢ Membership.mem (γ := Set α) ⊥ x

Tactic:
rcases mem_iUnion₂.1 hx₁ with ⟨a, has, ha⟩

Premises used: Set.mem_iUnion₂, Iff.mp
-- Module: Mathlib.Order.Interval.Set.OrdConnectedComponent
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
rcases :
  ∀ (b : α) (hbt : b ∈ t) (hb : x ∈ (sᶜ ∩ (t.ordSeparatingSet s).ordConnectedSectionᶜ).ordConnectedComponent b),
    Membership.mem (γ := Set α) ⊥ x
⊢ Membership.mem (γ := Set α) ⊥ x

Tactic:
rcases mem_iUnion₂.1 hx₂ with ⟨b, hbt, hb⟩

Premises used: Set.mem_iUnion₂, Iff.mp
-- Module: Mathlib.Order.Interval.Set.OrdConnectedComponent
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
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
⊢ Membership.mem (γ := Set α) ⊥ x

Tactic:
rw [mem_ordConnectedComponent, subset_inter_iff] at ha hb

Premises used: Set.subset_inter_iff, Set.mem_ordConnectedComponent
-- Module: Mathlib.Order.Interval.Set.OrdConnectedComponent
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
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
⊢ Membership.mem (γ := Set α) ⊥ x

Tactic:
wlog hab : a ≤ b with H
-- Module: Mathlib.Order.Interval.Set.OrdConnectedComponent
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ᶜ
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:
H b hbt hb a has ha (le_of_not_ge hab)

Premises used: le_of_not_ge
-- Module: Mathlib.Order.Interval.Set.OrdConnectedComponent
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ᶜ
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:
exact H b hbt hb a has ha (le_of_not_ge hab)

Premises used: le_of_not_ge
-- Module: Mathlib.Order.Interval.Set.OrdConnectedComponent
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
⊢ [[a, x]] ⊆ tᶜ

Tactic:
obtain ⟨ha, ha'⟩ := ha
-- Module: Mathlib.Order.Interval.Set.OrdConnectedComponent
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ᶜ
⊢ [[a, x]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ

Tactic:
obtain ⟨ha, ha'⟩ := ha
-- Module: Mathlib.Order.Interval.Set.OrdConnectedComponent
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ᶜ
⊢ [[b, x]] ⊆ sᶜ

Tactic:
obtain ⟨hb, hb'⟩ := hb
-- Module: Mathlib.Order.Interval.Set.OrdConnectedComponent
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ᶜ
⊢ [[b, x]] ⊆ (t.ordSeparatingSet s).ordConnectedSectionᶜ

Tactic:
obtain ⟨hb, hb'⟩ := hb
-- Module: Mathlib.Order.Interval.Set.OrdConnectedComponent
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ᶜ
⊢ [[x, b]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ

Tactic:
rw [ordSeparatingSet_comm, uIcc_comm] at hb'

Premises used: Set.uIcc_comm, Set.ordSeparatingSet_comm
-- Module: Mathlib.Order.Interval.Set.OrdConnectedComponent
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' : [[x, b]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ
⊢ [[a, b]] ⊆ [[a, x]] ∪ [[x, b]]

Tactic:
uIcc_subset_uIcc_union_uIcc

Premises used: Set.uIcc_subset_uIcc_union_uIcc
-- Module: Mathlib.Order.Interval.Set.OrdConnectedComponent
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' : [[x, b]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ
⊢ [[a, x]] ∪ [[x, b]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ

Tactic:
union_subset ha' hb'

Premises used: Set.union_subset
-- Module: Mathlib.Order.Interval.Set.OrdConnectedComponent
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' : [[x, b]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ
⊢ [[a, b]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ

Tactic:
calc
      [[a, b]] ⊆ [[a, x]] ∪ [[x, b]] := uIcc_subset_uIcc_union_uIcc
      _ ⊆ (ordSeparatingSet s t).ordConnectedSectionᶜ := union_subset ha' hb'

Premises used: Set.ordSeparatingSet, Set.uIcc_subset_uIcc_union_uIcc, Set.union_subset, Set.ordConnectedSection
-- Module: Mathlib.Order.Interval.Set.OrdConnectedComponent
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ᶜ

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'
-- Module: Mathlib.Order.Interval.Set.OrdConnectedComponent
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
inr : ∀ (hax : a ≤ x), Membership.mem (γ := Set α) ⊥ x
⊢ Membership.mem (γ := Set α) ⊥ x

Tactic:
rcases le_total x a with hxa | hax

Premises used: le_total
-- Module: Mathlib.Order.Interval.Set.OrdConnectedComponent
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ᶜ
hxa : x ≤ a
⊢ Membership.mem (γ := Set α) ⊥ x

Tactic:
hb (Icc_subset_uIcc' ⟨hxa, hab⟩) has

Premises used: Set.Mem, And.intro, Set.Icc_subset_uIcc'
-- Module: Mathlib.Order.Interval.Set.OrdConnectedComponent
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ᶜ
hxa : x ≤ a
⊢ Membership.mem (γ := Set α) ⊥ x

Tactic:
exact hb (Icc_subset_uIcc' ⟨hxa, hab⟩) has

Premises used: And.intro, Set.Icc_subset_uIcc'
-- Module: Mathlib.Order.Interval.Set.OrdConnectedComponent
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
inr₁ : ∀ (hxb : x ≤ b), Membership.mem (γ := Set α) ⊥ x
⊢ Membership.mem (γ := Set α) ⊥ x

Tactic:
rcases le_total b x with hbx | hxb

Premises used: le_total
-- Module: Mathlib.Order.Interval.Set.OrdConnectedComponent
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
hbx : b ≤ x
⊢ Membership.mem (γ := Set α) ⊥ x

Tactic:
ha (Icc_subset_uIcc ⟨hab, hbx⟩) hbt

Premises used: Set.Mem, Set.Icc_subset_uIcc, And.intro
-- Module: Mathlib.Order.Interval.Set.OrdConnectedComponent
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
hbx : b ≤ x
⊢ Membership.mem (γ := Set α) ⊥ x

Tactic:
exact ha (Icc_subset_uIcc ⟨hab, hbx⟩) hbt

Premises used: Set.Icc_subset_uIcc, And.intro
-- Module: Mathlib.Order.Interval.Set.OrdConnectedComponent
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
⊢ x ∈ s.ordSeparatingSet t

Tactic:
have h' : x ∈ ordSeparatingSet s t := ⟨mem_iUnion₂.2 ⟨a, has, ha⟩, mem_iUnion₂.2 ⟨b, hbt, hb⟩⟩
-- Module: Mathlib.Order.Interval.Set.OrdConnectedComponent
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
⊢ x ∈ s.ordSeparatingSet t

Tactic:
h'
-- Module: Mathlib.Order.Interval.Set.OrdConnectedComponent
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
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 : α)
⊢ Membership.mem (γ := Set α) ⊥ x

Tactic:
lift x to ordSeparatingSet s t using h'

Premises used: Set.ordSeparatingSet
-- Module: Mathlib.Order.Interval.Set.OrdConnectedComponent
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
inr : (s.ordSeparatingSet t).ordConnectedComponent (↑x : α) ⊆ [[a, b]]
⊢ Membership.mem (γ := Set α) ⊥ (↑x : α)

Tactic:
suffices ordConnectedComponent (ordSeparatingSet s t) x ⊆ [[a, b]] from
    hsub (this <| ordConnectedProj_mem_ordConnectedComponent _ x) (mem_range_self _)
-- Module: Mathlib.Order.Interval.Set.OrdConnectedComponent
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 : α)
inr : ¬y < a ∧ ¬b < y
⊢ y ∈ [[a, b]]

Tactic:
rw [uIcc_of_le hab, mem_Icc, ← not_lt, ← not_lt]

Premises used: Set.uIcc_of_le, not_lt, Set.mem_Icc
-- Module: Mathlib.Order.Interval.Set.OrdConnectedComponent
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 : α)
⊢ ∀ (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⟩)
-- Module: Mathlib.Order.Interval.Set.OrdConnectedComponent
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
⊢ ∀ (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⟩)
-- Module: Mathlib.Order.Interval.Set.OrdConnectedComponent
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
sol2 : ∀ (hby : b < y), False
⊢ ¬y < a ∧ ¬b < y

Tactic:
⟨sol1, sol2⟩

Premises used: And.intro
-- Module: Mathlib.Order.Interval.Set.OrdConnectedComponent
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
sol2 : ∀ (hby : b < y), False
⊢ ¬y < a ∧ ¬b < y

Tactic:
exact ⟨sol1, sol2⟩
-- Module: Mathlib.Order.Interval.Set.OrdConnectedLinear
Goal:
α : Type u_1
I : Set α
inst : ConditionallyCompleteLinearOrder α
inst_1 : LocallyFiniteOrder α
h₀ : I.Nonempty
h₁ : BddBelow I
h₂ : BddAbove I
⊢ I.OrdConnected ↔ I = Icc (sInf I) (sSup I)

Tactic:
have h₄ : I.Finite := h₁.finite_of_bddAbove h₂
  ⟨fun _ ↦ le_antisymm (subset_Icc_csInf_csSup h₁ h₂)
    (I.Icc_subset (h₀.csInf_mem h₄) (h₀.csSup_mem h₄)), fun h₃ ↦ h₃ ▸ ordConnected_Icc⟩

Premises used: Eq.rec, Set.Nonempty.csSup_mem, Set.ordConnected_Icc, le_antisymm, Iff.intro, Set.Icc_subset, subset_Icc_csInf_csSup, Eq.symm, BddBelow.finite_of_bddAbove, Set.Nonempty.csInf_mem
-- Module: Mathlib.Order.Interval.Set.OrdConnectedLinear
Goal:
α : Type u_1
I : Set α
inst : ConditionallyCompleteLinearOrder α
inst_1 : OrderTop α
inst_2 : OrderBot α
inst_3 : LocallyFiniteOrder α
h₀ : I.Nonempty
⊢ I.OrdConnected ↔ I = Icc (sInf I) (sSup I)

Tactic:
h₀.ordConnected_iff_of_bdd (OrderBot.bddBelow I) (OrderTop.bddAbove I)

Premises used: OrderTop.bddAbove, Set.Nonempty.ordConnected_iff_of_bdd, OrderBot.bddBelow
-- Module: Mathlib.Order.Interval.Set.OrdConnectedLinear
Goal:
α : Type u_1
I : Set α
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
simp_rw : I.OrdConnected ↔ ∀ x ∈ I, ∀ y ∈ I, Ioo x y ⊆ Iᶜ → Ioo x y = ∅
⊢ I.OrdConnected ↔ ∀ x ∈ I, ∀ y ∈ I, Disjoint (Ioo x y) I → Ioo x y = ∅

Tactic:
simp_rw [← Set.subset_compl_iff_disjoint_right]

Premises used: Set.subset_compl_iff_disjoint_right
-- Module: Mathlib.Order.Interval.Set.OrdConnectedLinear
Goal:
α : Type u_1
I : Set α
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
⊢ I.OrdConnected ↔ ∀ x ∈ I, ∀ y ∈ I, Ioo x y ⊆ Iᶜ → Ioo x y = ∅

Tactic:
⟨fun h' x hx y hy hxy ↦ ?_, fun h' ↦ ordConnected_of_Ioo fun x hx y hy hxy z hz ↦ ?_⟩

Premises used: Iff.intro, Set.ordConnected_of_Ioo
-- Module: Mathlib.Order.Interval.Set.OrdConnectedLinear
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 = ∅
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
⊢ I.OrdConnected ↔ ∀ x ∈ I, ∀ y ∈ I, 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 ↦ ?_⟩
-- Module: Mathlib.Order.Interval.Set.OrdConnectedLinear
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
h : ∀ (z : α), z ∈ Ioo x y ↔ Membership.mem (γ := Set α) ∅ z
⊢ Ioo x y = ∅

Tactic:
ext z
-- Module: Mathlib.Order.Interval.Set.OrdConnectedLinear
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
z : α
⊢ z ∈ Ioo x y ↔ Membership.mem (γ := Set α) ∅ z

Tactic:
simpa using this z
-- Module: Mathlib.Order.Interval.Set.OrdConnectedLinear
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ᶜ
refine_1 : ∀ (z : α), x < z → y ≤ z
⊢ Ioo x y = ∅

Tactic:
suffices ∀ z, x < z → y ≤ z by ext z; simpa using this z
-- Module: Mathlib.Order.Interval.Set.OrdConnectedLinear
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
this : z ∉ Ioo x y
⊢ y ≤ z

Tactic:
simp_all