awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Interval.Set.OrdConnected
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : β → α
t : Set β
s : Set α
hs : s.OrdConnected
hf : MonotoneOn f t
u : Set β := {x : β | (∃ y ∈ t, y ≤ x ∧ f y ∈ s) ∧ ∃ z ∈ t, x ≤ z ∧ f z ∈ s}
x : β
xt : x ∈ t
xs : x ∈ f ⁻¹' s
⊢ x ∈ t ∩ u

Tactic:
exact ⟨xt, ⟨x, xt, le_rfl, xs⟩, ⟨x, xt, le_rfl, xs⟩⟩
-- Module: Mathlib.Order.Interval.Set.OrdConnected
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : β → α
t : Set β
s : Set α
hs : s.OrdConnected
hf : MonotoneOn f t
u : Set β := {x : β | (∃ y ∈ t, y ≤ x ∧ f y ∈ s) ∧ ∃ z ∈ t, x ≤ z ∧ f z ∈ s}
x : β
xt : x ∈ t
y : β
yt : y ∈ t
yx : y ≤ x
ys : f y ∈ s
z : β
zt : z ∈ t
xz : x ≤ z
zs : f z ∈ s
⊢ x ∈ t ∩ f ⁻¹' s

Tactic:
⟨xt, ?_⟩

Premises used: Set.Mem, setOf, Set.inter, And.intro
-- Module: Mathlib.Order.Interval.Set.OrdConnected
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : β → α
t : Set β
s : Set α
hs : s.OrdConnected
hf : MonotoneOn f t
u : Set β := {x : β | (∃ y ∈ t, y ≤ x ∧ f y ∈ s) ∧ ∃ z ∈ t, x ≤ z ∧ f z ∈ s}
x : β
xt : x ∈ t
y : β
yt : y ∈ t
yx : y ≤ x
ys : f y ∈ s
z : β
zt : z ∈ t
xz : x ≤ z
zs : f z ∈ s
refine_3 : x ∈ f ⁻¹' s
⊢ x ∈ t ∩ f ⁻¹' s

Tactic:
refine ⟨xt, ?_⟩
-- Module: Mathlib.Order.Interval.Set.OrdConnected
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : β → α
t : Set β
s : Set α
hs : s.OrdConnected
hf : MonotoneOn f t
u : Set β := {x : β | (∃ y ∈ t, y ≤ x ∧ f y ∈ s) ∧ ∃ z ∈ t, x ≤ z ∧ f z ∈ s}
x : β
xt : x ∈ t
y : β
yt : y ∈ t
yx : y ≤ x
ys : f y ∈ s
z : β
zt : z ∈ t
xz : x ≤ z
zs : f z ∈ s
refine_3 : f x ∈ Icc (f y) (f z)
⊢ x ∈ f ⁻¹' s

Tactic:
apply hs.out ys zs

Premises used: Set.OrdConnected.out
-- Module: Mathlib.Order.Interval.Set.OrdConnected
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : β → α
t : Set β
s : Set α
hs : s.OrdConnected
hf : MonotoneOn f t
u : Set β := {x : β | (∃ y ∈ t, y ≤ x ∧ f y ∈ s) ∧ ∃ z ∈ t, x ≤ z ∧ f z ∈ s}
x : β
xt : x ∈ t
y : β
yt : y ∈ t
yx : y ≤ x
ys : f y ∈ s
z : β
zt : z ∈ t
xz : x ≤ z
zs : f z ∈ s
⊢ f x ∈ Icc (f y) (f z)

Tactic:
⟨hf yt xt yx, hf xt zt xz⟩

Premises used: Set.Mem, setOf, Set.Icc, And.intro
-- Module: Mathlib.Order.Interval.Set.OrdConnected
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : β → α
t : Set β
s : Set α
hs : s.OrdConnected
hf : MonotoneOn f t
u : Set β := {x : β | (∃ y ∈ t, y ≤ x ∧ f y ∈ s) ∧ ∃ z ∈ t, x ≤ z ∧ f z ∈ s}
x : β
xt : x ∈ t
y : β
yt : y ∈ t
yx : y ≤ x
ys : f y ∈ s
z : β
zt : z ∈ t
xz : x ≤ z
zs : f z ∈ s
⊢ f x ∈ Icc (f y) (f z)

Tactic:
exact ⟨hf yt xt yx, hf xt zt xz⟩
-- Module: Mathlib.Order.Interval.Set.OrdConnected
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : β → α
t : Set β
s : Set α
hs : s.OrdConnected
hf : AntitoneOn f t
⊢ ∃ (u : Set β), u.OrdConnected ∧ t ∩ f ⁻¹' s = t ∩ u

Tactic:
(OrdConnected.preimage_monotoneOn hs.dual hf.dual_right :)

Premises used: Set.Mem, setOf, AntitoneOn.dual_right, Set.preimage, Set.OrdConnected.dual, OrderDual, Set.OrdConnected.preimage_monotoneOn
-- Module: Mathlib.Order.Interval.Set.OrdConnected
Goal:
α : Type u_1
inst : PartialOrder α
s : Set α
hs : IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
z : α
hz : z ∈ Icc x y
⊢ x ∈ s

Tactic:
obtain rfl := hs.eq hx hy (hz.1.trans hz.2)

Premises used: And.right, And.left, IsAntichain.eq, LE.le.trans, rfl
-- Module: Mathlib.Order.Interval.Set.OrdConnected
Goal:
α : Type u_1
inst : PartialOrder α
s : Set α
hs : IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
z : α
hz : z ∈ Icc x y
hy₁ : x ∈ s
⊢ z ∈ Icc x x

Tactic:
obtain rfl := hs.eq hx hy (hz.1.trans hz.2)

Premises used: And.right, And.left, IsAntichain.eq, LE.le.trans, rfl
-- Module: Mathlib.Order.Interval.Set.OrdConnected
Goal:
α : Type u_1
inst : PartialOrder α
s : Set α
hs : IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) s
x : α
hx : x ∈ s
z : α
hy : x ∈ s
hz : z ∈ Icc x x
⊢ z = x

Tactic:
rw [Icc_self, mem_singleton_iff] at hz

Premises used: Set.Icc_self, Set.mem_singleton_iff
-- Module: Mathlib.Order.Interval.Set.OrdConnected
Goal:
α : Type u_1
inst : PartialOrder α
s : Set α
hs : IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) s
x : α
hx : x ∈ s
z : α
hy : x ∈ s
hz : z = x
rwa rwa₁ rwa₂ rwa₃ : x ∈ s
⊢ z ∈ s

Tactic:
rwa [hz]
-- Module: Mathlib.Order.Interval.Set.OrdConnected
Goal:
α : Type u_1
inst : PartialOrder α
s : Set α
x y : α
h : Ioo x y ⊆ s
⊢ (s ∩ Icc x y).OrdConnected

Tactic:
ordConnected_of_Ioo fun _u ⟨_, hu, _⟩ _v ⟨_, _, hv⟩ _ ↦
    Ioo_subset_Ioo hu hv |>.trans <| subset_inter h Ioo_subset_Icc_self

Premises used: Set.Ioo_subset_Icc_self, _private.0.Set.ordConnected_inter_Icc_of_subset.match_1, HasSubset.Subset.trans, HasSubset.Subset, Inter.inter, Set.subset_inter, Set.Icc, Set.Ioo_subset_Ioo, Set.Ioo, Set.ordConnected_of_Ioo
-- Module: Mathlib.Order.Interval.Set.OrdConnected
Goal:
α : Type u_1
inst : PartialOrder α
s : Set α
x y : α
hx : x ∈ s
hy : y ∈ s
⊢ (s ∩ Icc x y).OrdConnected ↔ Ioo x y ⊆ s

Tactic:
⟨fun h ↦ Ioo_subset_Icc_self.trans fun z hz ↦ ?_, ordConnected_inter_Icc_of_subset⟩

Premises used: Set.Ioo_subset_Icc_self, HasSubset.Subset.trans, Set.ordConnected_inter_Icc_of_subset, Iff.intro
-- Module: Mathlib.Order.Interval.Set.OrdConnected
Goal:
α : Type u_1
inst : PartialOrder α
s : Set α
x y : α
hx : x ∈ s
hy : y ∈ s
refine : ∀ (h : (s ∩ Icc x y).OrdConnected) (z : α) (hz : z ∈ Icc x y), z ∈ s
⊢ (s ∩ Icc x y).OrdConnected ↔ Ioo x y ⊆ s

Tactic:
refine ⟨fun h ↦ Ioo_subset_Icc_self.trans fun z hz ↦ ?_, ordConnected_inter_Icc_of_subset⟩
-- Module: Mathlib.Order.Interval.Set.OrdConnected
Goal:
α : Type u_1
inst : PartialOrder α
s : Set α
x y : α
hx : x ∈ s
hy : y ∈ s
h : (s ∩ Icc x y).OrdConnected
z : α
hz : z ∈ Icc x y
⊢ x ≤ y

Tactic:
have hxy : x ≤ y := hz.1.trans hz.2
-- Module: Mathlib.Order.Interval.Set.OrdConnected
Goal:
α : Type u_1
inst : PartialOrder α
s : Set α
x y : α
hx : x ∈ s
hy : y ∈ s
h : (s ∩ Icc x y).OrdConnected
z : α
hz : z ∈ Icc x y
hxy : x ≤ y
⊢ z ∈ s

Tactic:
h.out ⟨hx, left_mem_Icc.2 hxy⟩ ⟨hy, right_mem_Icc.2 hxy⟩ hz |>.1

Premises used: Iff.mpr, Set.right_mem_Icc, Set.OrdConnected.out, And.left, Set.left_mem_Icc, And.intro
-- Module: Mathlib.Order.Interval.Set.OrdConnected
Goal:
α : Type u_1
inst : PartialOrder α
s : Set α
x y : α
hx : x ∈ s
hy : y ∈ s
h : (s ∩ Icc x y).OrdConnected
z : α
hz : z ∈ Icc x y
hxy : x ≤ y
⊢ z ∈ s

Tactic:
exact h.out ⟨hx, left_mem_Icc.2 hxy⟩ ⟨hy, right_mem_Icc.2 hxy⟩ hz |>.1

Premises used: Iff.mpr, Set.right_mem_Icc, Set.OrdConnected.out, And.left, Set.left_mem_Icc, And.intro
-- Module: Mathlib.Order.Interval.Set.OrdConnected
Goal:
α : Type u_1
inst : PartialOrder α
s : Set α
x y : α
hx : x ∈ s
hy : y ∈ s
simp_rw : ¬Ioo x y ⊆ s ↔ ∃ z ∉ s, z ∈ Ioo x y
simp_rw₁ : (¬∀ x_1 ∈ Ioo x y, x_1 ∈ s) ↔ ∃ z ∉ s, z ∈ Ioo x y
simp_rw₂ : (∃ (x_1 : α) (_ : x_1 ∈ Ioo x y), x_1 ∉ s) ↔ ∃ z ∉ s, z ∈ Ioo x y
simp_rw₃ : (∃ x_1 ∈ Ioo x y, x_1 ∉ s) ↔ ∃ z ∉ s, z ∈ Ioo x y
⊢ ¬(s ∩ Icc x y).OrdConnected ↔ ∃ z ∉ s, z ∈ Ioo x y

Tactic:
simp_rw [ordConnected_inter_Icc_iff hx hy, subset_def, not_forall, exists_prop, and_comm]

Premises used: Set.subset_def, and_comm, exists_prop, Set.ordConnected_inter_Icc_iff, Classical.not_forall
-- Module: Mathlib.Order.Interval.Set.OrdConnected
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
⊢ [[a, b]].OrdConnected

Tactic:
ordConnected_Icc

Premises used: Set.ordConnected_Icc, Set.uIcc
-- Module: Mathlib.Order.Interval.Set.OrdConnected
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
⊢ (Ι a b).OrdConnected

Tactic:
ordConnected_Ioc

Premises used: Set.uIoc, Set.ordConnected_Ioc
-- Module: Mathlib.Order.Interval.Set.OrdConnected
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
hs : s.OrdConnected
x : α
hx : x ∈ s
y : α
hy : y ∈ s
⊢ [[x, y]] ⊆ s

Tactic:
hs.out (min_rec' (· ∈ s) hx hy) (max_rec' (· ∈ s) hx hy)

Premises used: Membership.mem, Set.OrdConnected.out, max_rec', min_rec', Set.uIcc
-- Module: Mathlib.Order.Interval.Set.OrdConnected
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
hs : s.OrdConnected
x : α
hx : x ∈ s
y : α
hy : y ∈ s
⊢ Ι x y ⊆ s

Tactic:
Ioc_subset_Icc_self.trans <| hs.uIcc_subset hx hy

Premises used: Set.OrdConnected.uIcc_subset, Set.uIoc, Set.Ioc_subset_Icc_self, HasSubset.Subset.trans
-- Module: Mathlib.Order.Interval.Set.OrdConnected
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
⊢ s.OrdConnected ↔ ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → [[x, y]] ⊆ s

Tactic:
⟨fun h => h.uIcc_subset, fun H => ⟨fun _ hx _ hy => Icc_subset_uIcc.trans <| H hx hy⟩⟩

Premises used: Set.OrdConnected.uIcc_subset, Set.Icc_subset_uIcc, HasSubset.Subset.trans, Set.OrdConnected.mk, Iff.intro
-- Module: Mathlib.Order.Interval.Set.OrdConnected
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
x : α
h : ∀ y ∈ s, [[x, y]] ⊆ s
y : α
hy : y ∈ s
z : α
hz : z ∈ s
rw rw₁ : [[x, y]] ∪ [[x, z]] = [[x, y]] ∪ [[x, z]]
⊢ [[y, x]] ∪ [[x, z]] = [[x, y]] ∪ [[x, z]]

Tactic:
rw [uIcc_comm]

Premises used: Set.uIcc_comm
-- Module: Mathlib.Order.Interval.Set.OrdConnected
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
x : α
hx : x ∈ s
⊢ s.OrdConnected ↔ ∀ ⦃y : α⦄, y ∈ s → [[x, y]] ⊆ s

Tactic:
⟨fun hs => hs.uIcc_subset hx, ordConnected_of_uIcc_subset_left⟩

Premises used: Set.OrdConnected.uIcc_subset, Set.ordConnected_of_uIcc_subset_left, Iff.intro
-- Module: Mathlib.Order.Interval.Set.OrdConnected
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
x : α
hx : x ∈ s
simp_rw : (∀ ⦃y : α⦄, y ∈ s → [[x, y]] ⊆ s) ↔ ∀ ⦃y : α⦄, y ∈ s → [[y, x]] ⊆ s
⊢ s.OrdConnected ↔ ∀ ⦃y : α⦄, y ∈ s → [[y, x]] ⊆ s

Tactic:
simp_rw [ordConnected_iff_uIcc_subset_left hx, uIcc_comm]

Premises used: Set.ordConnected_iff_uIcc_subset_left, Set.uIcc_comm
-- Module: Mathlib.Order.Interval.Set.OrdConnected
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
inst_1 : s.OrdConnected
a b : (↑s : Type u_1)
⊢ Subtype.val (p := fun (x : α) ↦ x ∈ s) '' [[a, b]] = [[(↑a : α), (↑b : α)]]

Tactic:
simp [uIcc, (Subtype.mono_coe (· ∈ s)).map_inf, (Subtype.mono_coe (· ∈ s)).map_sup]

Premises used: Monotone.map_sup, Membership.mem, Subtype.mono_coe, Set.uIcc, Monotone.map_inf
-- Module: Mathlib.Order.Interval.Set.OrdConnected
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
inst_1 : s.OrdConnected
a b : (↑s : Type u_1)
⊢ Subtype.val (p := fun (x : α) ↦ x ∈ s) '' Ι a b = Ι (↑a : α) (↑b : α)

Tactic:
simp [uIoc, (Subtype.mono_coe (· ∈ s)).map_inf, (Subtype.mono_coe (· ∈ s)).map_sup]

Premises used: Set.uIoc, Monotone.map_sup, Membership.mem, Subtype.mono_coe, Monotone.map_inf
-- Module: Mathlib.Order.Interval.Set.OrdConnected
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
inst_1 : s.OrdConnected
a b : (↑s : Type u_1)
⊢ Subtype.val (p := fun (x : α) ↦ x ∈ s) '' uIoo a b = uIoo (↑a : α) (↑b : α)

Tactic:
simp [uIoo, (Subtype.mono_coe (· ∈ s)).map_inf, (Subtype.mono_coe (· ∈ s)).map_sup]

Premises used: Monotone.map_sup, Membership.mem, Subtype.mono_coe, Set.uIoo, Monotone.map_inf
-- Module: Mathlib.Order.Interval.Set.OrdConnectedComponent
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
x y : α
⊢ y ∈ s.ordConnectedComponent x ↔ [[x, y]] ⊆ s

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.ordConnectedComponent
-- Module: Mathlib.Order.Interval.Set.OrdConnectedComponent
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
x_1 x : α
⊢ Membership.mem (α := αᵒᵈ) (γ := Set αᵒᵈ)
      (ordConnectedComponent ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s) ((toDual : (a : α) → αᵒᵈ) x_1) : Set αᵒᵈ)
      ((toDual : (a : α) → αᵒᵈ) x : αᵒᵈ) ↔
    Membership.mem (α := αᵒᵈ) (γ := Set αᵒᵈ) ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s.ordConnectedComponent x_1)
      ((toDual : (a : α) → αᵒᵈ) x : αᵒᵈ)

Tactic:
simp [mem_ordConnectedComponent]

Premises used: Set.mem_ordConnectedComponent
-- Module: Mathlib.Order.Interval.Set.OrdConnectedComponent
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
x : α
⊢ s.ordConnectedComponent x ⊆ s

Tactic:
fun _ hy =>
  hy right_mem_uIcc

Premises used: Set.right_mem_uIcc, Set.Subset
-- Module: Mathlib.Order.Interval.Set.OrdConnectedComponent
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
x : α
t : Set α
h : s.OrdConnected
hs : x ∈ s
ht : s ⊆ t
⊢ s ⊆ t.ordConnectedComponent x

Tactic:
fun _ hy => (h.uIcc_subset hs hy).trans ht

Premises used: Set.OrdConnected.uIcc_subset, Set.Mem, setOf, HasSubset.Subset.trans, Set.Subset, Set.ordConnectedComponent
-- Module: Mathlib.Order.Interval.Set.OrdConnectedComponent
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
x : α
rw : [[x, x]] ⊆ s ↔ x ∈ s
rw₁ : {x} ⊆ s ↔ x ∈ s
rw₂ rw₃ : x ∈ s ↔ x ∈ s
⊢ x ∈ s.ordConnectedComponent x ↔ x ∈ s

Tactic:
rw [mem_ordConnectedComponent, uIcc_self, singleton_subset_iff]

Premises used: Set.singleton_subset_iff, Set.uIcc_self, Set.mem_ordConnectedComponent
-- Module: Mathlib.Order.Interval.Set.OrdConnectedComponent
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
x : α
⊢ (s.ordConnectedComponent x).Nonempty ↔ x ∈ s

Tactic:
⟨fun ⟨_, hy⟩ => hy <| left_mem_uIcc, fun h => ⟨x, self_mem_ordConnectedComponent.2 h⟩⟩

Premises used: Iff.mpr, Set.self_mem_ordConnectedComponent, Membership.mem, Set.left_mem_uIcc, _private.0.Set.nonempty_ordConnectedComponent.match_1, Iff.intro, Exists.intro
-- Module: Mathlib.Order.Interval.Set.OrdConnectedComponent
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
x : α
rw : ¬(s.ordConnectedComponent x).Nonempty ↔ x ∉ s
rw₁ rw₂ : x ∉ s ↔ x ∉ s
⊢ s.ordConnectedComponent x = ∅ ↔ x ∉ s

Tactic:
rw [← not_nonempty_iff_eq_empty, nonempty_ordConnectedComponent]

Premises used: Set.not_nonempty_iff_eq_empty, Set.nonempty_ordConnectedComponent
-- Module: Mathlib.Order.Interval.Set.OrdConnectedComponent
Goal:
α : Type u_1
inst : LinearOrder α
x : α
⊢ ordConnectedComponent ∅ x = ∅

Tactic:
ordConnectedComponent_eq_empty.2 (notMem_empty x)

Premises used: Iff.mpr, Set.ordConnectedComponent_eq_empty, Set.notMem_empty
-- Module: Mathlib.Order.Interval.Set.OrdConnectedComponent
Goal:
α : Type u_1
inst : LinearOrder α
x : α
⊢ ordConnectedComponent univ x = univ

Tactic:
simp [ordConnectedComponent]

Premises used: Set.ordConnectedComponent
-- Module: Mathlib.Order.Interval.Set.OrdConnectedComponent
Goal:
α : Type u_1
inst : LinearOrder α
s t : Set α
x : α
⊢ (s ∩ t).ordConnectedComponent x = s.ordConnectedComponent x ∩ t.ordConnectedComponent x

Tactic:
simp [ordConnectedComponent, setOf_and]

Premises used: Set.setOf_and, Set.ordConnectedComponent
-- Module: Mathlib.Order.Interval.Set.OrdConnectedComponent
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
x y : α
rw : [[x, y]] ⊆ s ↔ x ∈ s.ordConnectedComponent y
rw₁ : [[x, y]] ⊆ s ↔ [[y, x]] ⊆ s
rw₂ rw₃ : [[y, x]] ⊆ s ↔ [[y, x]] ⊆ s
⊢ y ∈ s.ordConnectedComponent x ↔ x ∈ s.ordConnectedComponent y

Tactic:
rw [mem_ordConnectedComponent, mem_ordConnectedComponent, uIcc_comm]

Premises used: Set.uIcc_comm, Set.mem_ordConnectedComponent
-- Module: Mathlib.Order.Interval.Set.OrdConnectedComponent
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
x y z : α
hxy : y ∈ s.ordConnectedComponent x
hyz : z ∈ s.ordConnectedComponent y
⊢ z ∈ s.ordConnectedComponent x

Tactic:
calc
    [[x, z]] ⊆ [[x, y]] ∪ [[y, z]] := uIcc_subset_uIcc_union_uIcc
    _ ⊆ s := union_subset hxy hyz

Premises used: Trans.trans, Set.Mem, setOf, Set.uIcc_subset_uIcc_union_uIcc, Set.union_subset, Set.ordConnectedComponent
-- Module: Mathlib.Order.Interval.Set.OrdConnectedComponent
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
x y : α
h : [[x, y]] ⊆ s
⊢ s.ordConnectedComponent x = s.ordConnectedComponent y

Tactic:
ext fun _ =>
    ⟨mem_ordConnectedComponent_trans (mem_ordConnectedComponent_comm.2 h),
      mem_ordConnectedComponent_trans h⟩

Premises used: Iff.mpr, Set.ext, Set.mem_ordConnectedComponent_trans, Set.mem_ordConnectedComponent_comm, Iff.intro
-- Module: Mathlib.Order.Interval.Set.OrdConnectedComponent
Goal:
α : Type u_1
inst : LinearOrder α
s t : Set α
x y z : α
⊢ (s.ordConnectedComponent x).OrdConnected

Tactic:
ordConnected_of_uIcc_subset_left fun _ hy _ hz => (uIcc_subset_uIcc_left hz).trans hy

Premises used: Set.uIcc_subset_uIcc_left, HasSubset.Subset.trans, Set.ordConnected_of_uIcc_subset_left
-- Module: Mathlib.Order.Interval.Set.OrdConnectedComponent
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
x : (↑s : Type u_1)
⊢ s.ordConnectedProj x ∈ s.ordConnectedComponent (↑x : α)

Tactic:
Nonempty.some_mem _

Premises used: Set.Mem, Set.ordConnectedProj, Set.Nonempty.some_mem
-- Module: Mathlib.Order.Interval.Set.OrdConnectedComponent
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
x : (↑s : Type u_1)
⊢ (↑x : α) ∈ s.ordConnectedComponent (s.ordConnectedProj x)

Tactic:
mem_ordConnectedComponent_comm.2 <| ordConnectedProj_mem_ordConnectedComponent s x

Premises used: Iff.mpr, Set.mem_ordConnectedComponent_comm, Set.ordConnectedProj_mem_ordConnectedComponent
-- Module: Mathlib.Order.Interval.Set.OrdConnectedComponent
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
x : (↑s : Type u_1)
⊢ s.ordConnectedComponent (s.ordConnectedProj x) = s.ordConnectedComponent (↑x : α)

Tactic:
ordConnectedComponent_eq <| mem_ordConnectedComponent_ordConnectedProj _ _

Premises used: Set.mem_ordConnectedComponent_ordConnectedProj, Set.ordConnectedComponent_eq
-- Module: Mathlib.Order.Interval.Set.OrdConnectedComponent
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
x y : (↑s : Type u_1)
mp : s.ordConnectedProj x = s.ordConnectedProj y → [[(↑x : α), (↑y : α)]] ⊆ s
mpr : [[(↑x : α), (↑y : α)]] ⊆ s → s.ordConnectedProj x = s.ordConnectedProj y
⊢ s.ordConnectedProj x = s.ordConnectedProj y ↔ [[(↑x : α), (↑y : α)]] ⊆ s

Tactic:
constructor
-- 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
mp : (↑y : α) ∈ s
⊢ [[(↑x : α), (↑y : α)]] ⊆ s

Tactic:
rw [← mem_ordConnectedComponent, ← ordConnectedComponent_ordConnectedProj, h,
      ordConnectedComponent_ordConnectedProj, self_mem_ordConnectedComponent]

Premises used: Set.self_mem_ordConnectedComponent, Set.ordConnectedComponent_ordConnectedProj, Set.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
⊢ (↑y : α) ∈ s

Tactic:
y.2

Premises used: Subtype.property
-- 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
⊢ (↑y : α) ∈ s

Tactic:
exact y.2

Premises used: Subtype.property
-- Module: Mathlib.Order.Interval.Set.OrdConnectedComponent
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
x y : (↑s : Type u_1)
h : [[(↑x : α), (↑y : α)]] ⊆ s
⊢ s.ordConnectedProj x = s.ordConnectedProj y

Tactic:
simp only [ordConnectedProj, ordConnectedComponent_eq h]

Premises used: Set.ordConnectedProj, Set.ordConnectedComponent_eq
-- Module: Mathlib.Order.Interval.Set.OrdConnectedComponent
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
h :
  ∀ (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
⊢ 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 : α)) ⋯))

Tactic:
ext x
-- Module: Mathlib.Order.Interval.Set.OrdConnectedComponent
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
⊢ 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

Tactic:
simp only [mem_range, Subtype.exists, mem_preimage, OrderDual.exists, dual_ordConnectedComponent,
    ofDual_toDual]

Premises used: Set.dual_ordConnectedComponent, Set.mem_range, Subtype.exists, OrderDual.exists, OrderDual.ofDual_toDual, Set.mem_preimage
-- Module: Mathlib.Order.Interval.Set.OrdConnectedComponent
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
h₅ h₆ h₇ :
  ∀ (w : α) (w_1 : w ∈ s),
    Nonempty.some (s := s.ordConnectedComponent w) ⋯ = (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
h₁₁ h₁₂ h₁₃ :
  ∀ (w : α) (w_1 : w ∈ s),
    Nonempty.some (s := s.ordConnectedComponent w) ⋯ = (ofDual : (a : αᵒᵈ) → α) x →
      ∃ (a : α) (h : a ∈ s), Nonempty.some (s := (⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s.ordConnectedComponent a) ⋯ = x
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
h₁₆ h₁₇ :
  ∀ (w : α) (w_1 : w ∈ s),
    Nonempty.some (s := s.ordConnectedComponent w) ⋯ = (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

Tactic:
tauto
-- Module: Mathlib.Order.Interval.Set.OrdConnectedComponent
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
⊢ s.ordConnectedSection ⊆ s

Tactic:
range_subset_iff.2 fun _ => ordConnectedComponent_subset <| Nonempty.some_mem _

Premises used: Iff.mpr, Set.ordConnectedProj._proof_1, Set.Nonempty.some_mem, Set.ordConnectedSection, Set.ordConnectedComponent_subset, Set.range_subset_iff
-- Module: Mathlib.Order.Interval.Set.OrdConnectedComponent
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
x y : α
hx : x ∈ s.ordConnectedSection
hy : y ∈ s.ordConnectedSection
h : [[x, y]] ⊆ s
rcases : ∀ (x : (↑s : Type u_1)) (h : [[s.ordConnectedProj x, y]] ⊆ s), s.ordConnectedProj x = y
⊢ x = y

Tactic:
rcases hx with ⟨x, rfl⟩

Premises used: rfl
-- Module: Mathlib.Order.Interval.Set.OrdConnectedComponent
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
y : α
hy : y ∈ s.ordConnectedSection
x : (↑s : Type u_1)
h : [[s.ordConnectedProj x, y]] ⊆ s
rcases :
  ∀ (y : (↑s : Type u_1)) (h : [[s.ordConnectedProj x, s.ordConnectedProj y]] ⊆ s),
    s.ordConnectedProj x = s.ordConnectedProj y
⊢ s.ordConnectedProj x = y

Tactic:
rcases hy with ⟨y, rfl⟩

Premises used: rfl