awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrdConnected (goal)
Goal:
α : Type u_3
inst : PartialOrder α
s : Set α
hs : ∀ x ∈ s, ∀ y ∈ s, x < y → Ioo x y ⊆ s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≤ y
inl : ∀ (hy : x ∈ s) (hxy : x ≤ x), Icc x x ⊆ s
⊢ Icc x y ⊆ s
have inr : ∀ (hxy' : x < y), Icc x y ⊆ s
Tactic: rcases eq_or_lt_of_le hxy with (rfl | hxy')
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrdConnected (goal)
Goal:
α : Type u_3
inst : PartialOrder α
s : Set α
hs : ∀ x ∈ s, ∀ y ∈ s, x < y → Ioo x y ⊆ s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≤ y
hxy' : x < y
⊢ Icc x y ⊆ s
have inr : insert x (insert y (Ioo x y)) ⊆ s
Tactic: rw [← Ioc_insert_left hxy, ← Ioo_insert_right hxy']
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrdConnected (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
e : α ↪o β
he : OrdConnected.{u_2} (α := β) (range.{u_2, u_1 + 1} (ι := α) (⇑e : (a : α) → β))
x y : α
⊢ Eq.{u_2 + 1} (α := Set β) ((⇑e : (a : α) → β) '' Icc x y : Set β)
    (Icc ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β)
have rw : Eq.{u_2 + 1} (α := Set β)
  (image.{u_1, u_2} (α := α) (⇑e : (a : α) → β)
      (preimage.{u_1, u_2} (β := β) ((⇑e : (a : α) → β) : (a : α) → β)
        (Icc ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β)) :
    Set β)
  (Icc ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β)
Tactic: rw [← e.preimage_Icc, image_preimage_eq_inter_range, inter_eq_left.2 (he.out ⟨_, rfl⟩ ⟨_, rfl⟩)]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrdConnected (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
e : α ↪o β
he : OrdConnected.{u_2} (α := β) (range.{u_2, u_1 + 1} (ι := α) (⇑e : (a : α) → β))
x y : α
rw :
  Eq.{u_2 + 1} (α := Set β)
    (image.{u_1, u_2} (α := α) (⇑e : (a : α) → β)
        (preimage.{u_1, u_2} (β := β) ((⇑e : (a : α) → β) : (a : α) → β)
          (Icc ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β)) :
      Set β)
    (Icc ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β)
⊢ Eq.{u_2 + 1} (α := Set β) ((⇑e : (a : α) → β) '' Icc x y : Set β)
    (Icc ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β)
have rw₁ : Eq.{u_2 + 1} (α := Set β)
  (Icc ((e : (a : α) → β) x) ((e : (a : α) → β) y) ∩ range.{u_2, u_1 + 1} (ι := α) (⇑e : (a : α) → β) : Set β)
  (Icc ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β)
Tactic: rw [← e.preimage_Icc, image_preimage_eq_inter_range, inter_eq_left.2 (he.out ⟨_, rfl⟩ ⟨_, rfl⟩)]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrdConnected (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
e : α ↪o β
he : OrdConnected.{u_2} (α := β) (range.{u_2, u_1 + 1} (ι := α) (⇑e : (a : α) → β))
x y : α
rw :
  Eq.{u_2 + 1} (α := Set β)
    (image.{u_1, u_2} (α := α) (⇑e : (a : α) → β)
        (preimage.{u_1, u_2} (β := β) ((⇑e : (a : α) → β) : (a : α) → β)
          (Icc ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β)) :
      Set β)
    (Icc ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β)
rw₁ :
  Eq.{u_2 + 1} (α := Set β)
    (Icc ((e : (a : α) → β) x) ((e : (a : α) → β) y) ∩ range.{u_2, u_1 + 1} (ι := α) (⇑e : (a : α) → β) : Set β)
    (Icc ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β)
⊢ Eq.{u_2 + 1} (α := Set β) ((⇑e : (a : α) → β) '' Icc x y : Set β)
    (Icc ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β)
have rw₂ : Eq.{u_2 + 1} (α := Set β) (Icc ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β)
  (Icc ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β)
Tactic: rw [← e.preimage_Icc, image_preimage_eq_inter_range, inter_eq_left.2 (he.out ⟨_, rfl⟩ ⟨_, rfl⟩)]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrdConnected (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
e : α ↪o β
he : OrdConnected.{u_2} (α := β) (range.{u_2, u_1 + 1} (ι := α) (⇑e : (a : α) → β))
x y : α
⊢ Eq.{u_2 + 1} (α := Set β) ((⇑e : (a : α) → β) '' Ico x y : Set β)
    (Ico ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β)
have rw : Eq.{u_2 + 1} (α := Set β)
  (image.{u_1, u_2} (α := α) (⇑e : (a : α) → β)
      (preimage.{u_1, u_2} (β := β) ((⇑e : (a : α) → β) : (a : α) → β)
        (Ico ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β)) :
    Set β)
  (Ico ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β)
Tactic: rw [← e.preimage_Ico, image_preimage_eq_inter_range,
    inter_eq_left.2 <| Ico_subset_Icc_self.trans <| he.out ⟨_, rfl⟩ ⟨_, rfl⟩]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrdConnected (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
e : α ↪o β
he : OrdConnected.{u_2} (α := β) (range.{u_2, u_1 + 1} (ι := α) (⇑e : (a : α) → β))
x y : α
rw :
  Eq.{u_2 + 1} (α := Set β)
    (image.{u_1, u_2} (α := α) (⇑e : (a : α) → β)
        (preimage.{u_1, u_2} (β := β) ((⇑e : (a : α) → β) : (a : α) → β)
          (Ico ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β)) :
      Set β)
    (Ico ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β)
⊢ Eq.{u_2 + 1} (α := Set β) ((⇑e : (a : α) → β) '' Ico x y : Set β)
    (Ico ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β)
have rw₁ : Eq.{u_2 + 1} (α := Set β)
  (Ico ((e : (a : α) → β) x) ((e : (a : α) → β) y) ∩ range.{u_2, u_1 + 1} (ι := α) (⇑e : (a : α) → β) : Set β)
  (Ico ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β)
Tactic: rw [← e.preimage_Ico, image_preimage_eq_inter_range,
    inter_eq_left.2 <| Ico_subset_Icc_self.trans <| he.out ⟨_, rfl⟩ ⟨_, rfl⟩]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrdConnected (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
e : α ↪o β
he : OrdConnected.{u_2} (α := β) (range.{u_2, u_1 + 1} (ι := α) (⇑e : (a : α) → β))
x y : α
rw :
  Eq.{u_2 + 1} (α := Set β)
    (image.{u_1, u_2} (α := α) (⇑e : (a : α) → β)
        (preimage.{u_1, u_2} (β := β) ((⇑e : (a : α) → β) : (a : α) → β)
          (Ico ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β)) :
      Set β)
    (Ico ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β)
rw₁ :
  Eq.{u_2 + 1} (α := Set β)
    (Ico ((e : (a : α) → β) x) ((e : (a : α) → β) y) ∩ range.{u_2, u_1 + 1} (ι := α) (⇑e : (a : α) → β) : Set β)
    (Ico ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β)
⊢ Eq.{u_2 + 1} (α := Set β) ((⇑e : (a : α) → β) '' Ico x y : Set β)
    (Ico ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β)
have rw₂ : Eq.{u_2 + 1} (α := Set β) (Ico ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β)
  (Ico ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β)
Tactic: rw [← e.preimage_Ico, image_preimage_eq_inter_range,
    inter_eq_left.2 <| Ico_subset_Icc_self.trans <| he.out ⟨_, rfl⟩ ⟨_, rfl⟩]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrdConnected (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
e : α ↪o β
he : OrdConnected.{u_2} (α := β) (range.{u_2, u_1 + 1} (ι := α) (⇑e : (a : α) → β))
x y : α
⊢ Eq.{u_2 + 1} (α := Set β) ((⇑e : (a : α) → β) '' Ioc x y : Set β)
    (Ioc ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β)
have rw : Eq.{u_2 + 1} (α := Set β)
  (image.{u_1, u_2} (α := α) (⇑e : (a : α) → β)
      (preimage.{u_1, u_2} (β := β) ((⇑e : (a : α) → β) : (a : α) → β)
        (Ioc ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β)) :
    Set β)
  (Ioc ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β)
Tactic: rw [← e.preimage_Ioc, image_preimage_eq_inter_range,
    inter_eq_left.2 <| Ioc_subset_Icc_self.trans <| he.out ⟨_, rfl⟩ ⟨_, rfl⟩]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrdConnected (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
e : α ↪o β
he : OrdConnected.{u_2} (α := β) (range.{u_2, u_1 + 1} (ι := α) (⇑e : (a : α) → β))
x y : α
rw :
  Eq.{u_2 + 1} (α := Set β)
    (image.{u_1, u_2} (α := α) (⇑e : (a : α) → β)
        (preimage.{u_1, u_2} (β := β) ((⇑e : (a : α) → β) : (a : α) → β)
          (Ioc ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β)) :
      Set β)
    (Ioc ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β)
⊢ Eq.{u_2 + 1} (α := Set β) ((⇑e : (a : α) → β) '' Ioc x y : Set β)
    (Ioc ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β)
have rw₁ : Eq.{u_2 + 1} (α := Set β)
  (Ioc ((e : (a : α) → β) x) ((e : (a : α) → β) y) ∩ range.{u_2, u_1 + 1} (ι := α) (⇑e : (a : α) → β) : Set β)
  (Ioc ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β)
Tactic: rw [← e.preimage_Ioc, image_preimage_eq_inter_range,
    inter_eq_left.2 <| Ioc_subset_Icc_self.trans <| he.out ⟨_, rfl⟩ ⟨_, rfl⟩]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrdConnected (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
e : α ↪o β
he : OrdConnected.{u_2} (α := β) (range.{u_2, u_1 + 1} (ι := α) (⇑e : (a : α) → β))
x y : α
rw :
  Eq.{u_2 + 1} (α := Set β)
    (image.{u_1, u_2} (α := α) (⇑e : (a : α) → β)
        (preimage.{u_1, u_2} (β := β) ((⇑e : (a : α) → β) : (a : α) → β)
          (Ioc ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β)) :
      Set β)
    (Ioc ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β)
rw₁ :
  Eq.{u_2 + 1} (α := Set β)
    (Ioc ((e : (a : α) → β) x) ((e : (a : α) → β) y) ∩ range.{u_2, u_1 + 1} (ι := α) (⇑e : (a : α) → β) : Set β)
    (Ioc ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β)
⊢ Eq.{u_2 + 1} (α := Set β) ((⇑e : (a : α) → β) '' Ioc x y : Set β)
    (Ioc ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β)
have rw₂ : Eq.{u_2 + 1} (α := Set β) (Ioc ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β)
  (Ioc ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β)
Tactic: rw [← e.preimage_Ioc, image_preimage_eq_inter_range,
    inter_eq_left.2 <| Ioc_subset_Icc_self.trans <| he.out ⟨_, rfl⟩ ⟨_, rfl⟩]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrdConnected (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
e : α ↪o β
he : OrdConnected.{u_2} (α := β) (range.{u_2, u_1 + 1} (ι := α) (⇑e : (a : α) → β))
x y : α
⊢ Eq.{u_2 + 1} (α := Set β) ((⇑e : (a : α) → β) '' Ioo x y : Set β)
    (Ioo ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β)
have rw : Eq.{u_2 + 1} (α := Set β)
  (image.{u_1, u_2} (α := α) (⇑e : (a : α) → β)
      (preimage.{u_1, u_2} (β := β) ((⇑e : (a : α) → β) : (a : α) → β)
        (Ioo ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β)) :
    Set β)
  (Ioo ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β)
Tactic: rw [← e.preimage_Ioo, image_preimage_eq_inter_range,
    inter_eq_left.2 <| Ioo_subset_Icc_self.trans <| he.out ⟨_, rfl⟩ ⟨_, rfl⟩]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrdConnected (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
e : α ↪o β
he : OrdConnected.{u_2} (α := β) (range.{u_2, u_1 + 1} (ι := α) (⇑e : (a : α) → β))
x y : α
rw :
  Eq.{u_2 + 1} (α := Set β)
    (image.{u_1, u_2} (α := α) (⇑e : (a : α) → β)
        (preimage.{u_1, u_2} (β := β) ((⇑e : (a : α) → β) : (a : α) → β)
          (Ioo ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β)) :
      Set β)
    (Ioo ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β)
⊢ Eq.{u_2 + 1} (α := Set β) ((⇑e : (a : α) → β) '' Ioo x y : Set β)
    (Ioo ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β)
have rw₁ : Eq.{u_2 + 1} (α := Set β)
  (Ioo ((e : (a : α) → β) x) ((e : (a : α) → β) y) ∩ range.{u_2, u_1 + 1} (ι := α) (⇑e : (a : α) → β) : Set β)
  (Ioo ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β)
Tactic: rw [← e.preimage_Ioo, image_preimage_eq_inter_range,
    inter_eq_left.2 <| Ioo_subset_Icc_self.trans <| he.out ⟨_, rfl⟩ ⟨_, rfl⟩]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrdConnected (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
e : α ↪o β
he : OrdConnected.{u_2} (α := β) (range.{u_2, u_1 + 1} (ι := α) (⇑e : (a : α) → β))
x y : α
rw :
  Eq.{u_2 + 1} (α := Set β)
    (image.{u_1, u_2} (α := α) (⇑e : (a : α) → β)
        (preimage.{u_1, u_2} (β := β) ((⇑e : (a : α) → β) : (a : α) → β)
          (Ioo ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β)) :
      Set β)
    (Ioo ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β)
rw₁ :
  Eq.{u_2 + 1} (α := Set β)
    (Ioo ((e : (a : α) → β) x) ((e : (a : α) → β) y) ∩ range.{u_2, u_1 + 1} (ι := α) (⇑e : (a : α) → β) : Set β)
    (Ioo ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β)
⊢ Eq.{u_2 + 1} (α := Set β) ((⇑e : (a : α) → β) '' Ioo x y : Set β)
    (Ioo ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β)
have rw₂ : Eq.{u_2 + 1} (α := Set β) (Ioo ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β)
  (Ioo ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β)
Tactic: rw [← e.preimage_Ioo, image_preimage_eq_inter_range,
    inter_eq_left.2 <| Ioo_subset_Icc_self.trans <| he.out ⟨_, rfl⟩ ⟨_, rfl⟩]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrdConnected (goal)
Goal:
α : Type u_3
inst : PartialOrder α
a : α
⊢ OrdConnected (α := α) {a}
have rw : (Icc a a).OrdConnected
Tactic: rw [← Icc_self]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrdConnected (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
E : Type u_3
inst_2 : EquivLike E α β
inst_3 : OrderIsoClass E α β
e : E
s : Set α
hs : s.OrdConnected
⊢ OrdConnected.{u_2} (α := β) ((⇑e : (a : α) → β) '' s)
have erw : OrdConnected.{u_2} (α := β) ((⇑(OrderIso.symm (↑e : α ≃o β)) : (a : β) → α) ⁻¹' s)
Tactic: erw [(e : α ≃o β).image_eq_preimage_symm]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrdConnected (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
E : Type u_3
inst_2 : EquivLike E α β
inst_3 : OrderIsoClass E α β
e : E
⊢ OrdConnected.{u_2} (α := β) (range.{u_2, u_1 + 1} (ι := α) (⇑e : (a : α) → β))
have simp_rw : OrdConnected.{u_2} (α := β) (image.{u_1, u_2} (α := α) (⇑e : (a : α) → β) univ)
Tactic: simp_rw [← image_univ]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrdConnected (goal)
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}
⊢ ∃ (u : Set β), u.OrdConnected ∧ t ∩ f ⁻¹' s = t ∩ u
have refine_1 : ∀ ⦃x : β⦄ (hx : x ∈ u) ⦃y : β⦄ (hy : y ∈ u), Icc x y ⊆ u
Tactic: refine ⟨u, ⟨?_⟩, Subset.antisymm ?_ ?_⟩
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrdConnected (goal)
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}
refine_1 : ∀ ⦃x : β⦄ (hx : x ∈ u) ⦃y : β⦄ (hy : y ∈ u), Icc x y ⊆ u
⊢ ∃ (u : Set β), u.OrdConnected ∧ t ∩ f ⁻¹' s = t ∩ u
have refine_2 : t ∩ f ⁻¹' s ⊆ t ∩ u
Tactic: refine ⟨u, ⟨?_⟩, Subset.antisymm ?_ ?_⟩
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrdConnected (goal)
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}
refine_1 : ∀ ⦃x : β⦄ (hx : x ∈ u) ⦃y : β⦄ (hy : y ∈ u), Icc x y ⊆ u
refine_2 : t ∩ f ⁻¹' s ⊆ t ∩ u
⊢ ∃ (u : Set β), u.OrdConnected ∧ t ∩ f ⁻¹' s = t ∩ u
have refine_3 : t ∩ u ⊆ t ∩ f ⁻¹' s
Tactic: refine ⟨u, ⟨?_⟩, Subset.antisymm ?_ ?_⟩
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrdConnected (goal)
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
have refine_3 : x ∈ f ⁻¹' s
Tactic: refine ⟨xt, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrdConnected (goal)
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 ∈ f ⁻¹' s
have refine_3 : f x ∈ Icc (f y) (f z)
Tactic: apply hs.out ys zs
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrdConnected (hypothesis)
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 ∈ s
have hz₁ : z ∈ Icc x x
Tactic: obtain rfl := hs.eq hx hy (hz.1.trans hz.2)
Cleared hypotheses: y, hy, hz
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrdConnected (hypothesis)
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 ∈ s
have hz₁ : z = x
Tactic: rw [Icc_self, mem_singleton_iff] at hz
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrdConnected (goal)
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
have refine : ∀ (h : (s ∩ Icc x y).OrdConnected) (z : α) (hz : z ∈ Icc x y), z ∈ s
Tactic: refine ⟨fun h ↦ Ioo_subset_Icc_self.trans fun z hz ↦ ?_, ordConnected_inter_Icc_of_subset⟩
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrdConnected (hypothesis)
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
⊢ z ∈ s
have hxy : x ≤ y
Tactic: have hxy : x ≤ y := hz.1.trans hz.2
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrdConnected (goal)
Goal:
α : Type u_1
inst : PartialOrder α
s : Set α
x y : α
hx : x ∈ s
hy : y ∈ s
⊢ ¬(s ∩ Icc x y).OrdConnected ↔ ∃ z ∉ s, z ∈ Ioo x y
have simp_rw : ¬Ioo x y ⊆ s ↔ ∃ z ∉ s, z ∈ Ioo x y
Tactic: simp_rw [ordConnected_inter_Icc_iff hx hy, subset_def, not_forall, exists_prop, and_comm]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrdConnected (goal)
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
⊢ ¬(s ∩ Icc x y).OrdConnected ↔ ∃ z ∉ s, z ∈ Ioo x y
have simp_rw₁ : (¬∀ x_1 ∈ Ioo x y, x_1 ∈ s) ↔ ∃ z ∉ s, z ∈ Ioo x y
Tactic: simp_rw [ordConnected_inter_Icc_iff hx hy, subset_def, not_forall, exists_prop, and_comm]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrdConnected (goal)
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
⊢ ¬(s ∩ Icc x y).OrdConnected ↔ ∃ z ∉ s, z ∈ Ioo x y
have simp_rw₂ : (∃ (x_1 : α) (_ : x_1 ∈ Ioo x y), x_1 ∉ s) ↔ ∃ z ∉ s, z ∈ Ioo x y
Tactic: simp_rw [ordConnected_inter_Icc_iff hx hy, subset_def, not_forall, exists_prop, and_comm]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrdConnected (goal)
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
⊢ ¬(s ∩ Icc x y).OrdConnected ↔ ∃ z ∉ s, z ∈ Ioo x y
have simp_rw₃ : (∃ x_1 ∈ Ioo x y, x_1 ∉ s) ↔ ∃ z ∉ s, z ∈ Ioo x y
Tactic: simp_rw [ordConnected_inter_Icc_iff hx hy, subset_def, not_forall, exists_prop, and_comm]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrdConnected (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
x : α
h : ∀ y ∈ s, [[x, y]] ⊆ s
y : α
hy : y ∈ s
z : α
hz : z ∈ s
⊢ [[y, x]] ∪ [[x, z]] = [[x, y]] ∪ [[x, z]]
have rw : [[x, y]] ∪ [[x, z]] = [[x, y]] ∪ [[x, z]]
Tactic: rw [uIcc_comm]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrdConnected (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
x : α
hx : x ∈ s
⊢ s.OrdConnected ↔ ∀ ⦃y : α⦄, y ∈ s → [[y, x]] ⊆ s
have simp_rw : (∀ ⦃y : α⦄, y ∈ s → [[x, y]] ⊆ s) ↔ ∀ ⦃y : α⦄, y ∈ s → [[y, x]] ⊆ s
Tactic: simp_rw [ordConnected_iff_uIcc_subset_left hx, uIcc_comm]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrdConnectedComponent (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
x : α
⊢ x ∈ s.ordConnectedComponent x ↔ x ∈ s
have rw : [[x, x]] ⊆ s ↔ x ∈ s
Tactic: rw [mem_ordConnectedComponent, uIcc_self, singleton_subset_iff]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrdConnectedComponent (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
x : α
rw : [[x, x]] ⊆ s ↔ x ∈ s
⊢ x ∈ s.ordConnectedComponent x ↔ x ∈ s
have rw₁ : {x} ⊆ s ↔ x ∈ s
Tactic: rw [mem_ordConnectedComponent, uIcc_self, singleton_subset_iff]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrdConnectedComponent (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
x : α
rw : [[x, x]] ⊆ s ↔ x ∈ s
rw₁ : {x} ⊆ s ↔ x ∈ s
⊢ x ∈ s.ordConnectedComponent x ↔ x ∈ s
have rw₂ : x ∈ s ↔ x ∈ s
Tactic: rw [mem_ordConnectedComponent, uIcc_self, singleton_subset_iff]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrdConnectedComponent (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
x : α
⊢ s.ordConnectedComponent x = ∅ ↔ x ∉ s
have rw : ¬(s.ordConnectedComponent x).Nonempty ↔ x ∉ s
Tactic: rw [← not_nonempty_iff_eq_empty, nonempty_ordConnectedComponent]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrdConnectedComponent (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
x : α
rw : ¬(s.ordConnectedComponent x).Nonempty ↔ x ∉ s
⊢ s.ordConnectedComponent x = ∅ ↔ x ∉ s
have rw₁ : x ∉ s ↔ x ∉ s
Tactic: rw [← not_nonempty_iff_eq_empty, nonempty_ordConnectedComponent]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrdConnectedComponent (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
x y : α
⊢ y ∈ s.ordConnectedComponent x ↔ x ∈ s.ordConnectedComponent y
have rw : [[x, y]] ⊆ s ↔ x ∈ s.ordConnectedComponent y
Tactic: rw [mem_ordConnectedComponent, mem_ordConnectedComponent, uIcc_comm]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrdConnectedComponent (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
x y : α
rw : [[x, y]] ⊆ s ↔ x ∈ s.ordConnectedComponent y
⊢ y ∈ s.ordConnectedComponent x ↔ x ∈ s.ordConnectedComponent y
have rw₁ : [[x, y]] ⊆ s ↔ [[y, x]] ⊆ s
Tactic: rw [mem_ordConnectedComponent, mem_ordConnectedComponent, uIcc_comm]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrdConnectedComponent (goal)
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
⊢ y ∈ s.ordConnectedComponent x ↔ x ∈ s.ordConnectedComponent y
have rw₂ : [[y, x]] ⊆ s ↔ [[y, x]] ⊆ s
Tactic: rw [mem_ordConnectedComponent, mem_ordConnectedComponent, uIcc_comm]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrdConnectedComponent (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
x y : (↑s : Type u_1)
⊢ s.ordConnectedProj x = s.ordConnectedProj y ↔ [[(↑x : α), (↑y : α)]] ⊆ s
have mp : s.ordConnectedProj x = s.ordConnectedProj y → [[(↑x : α), (↑y : α)]] ⊆ s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrdConnectedComponent (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
x y : (↑s : Type u_1)
mp : s.ordConnectedProj x = s.ordConnectedProj y → [[(↑x : α), (↑y : α)]] ⊆ s
⊢ s.ordConnectedProj x = s.ordConnectedProj y ↔ [[(↑x : α), (↑y : α)]] ⊆ s
have mpr : [[(↑x : α), (↑y : α)]] ⊆ s → s.ordConnectedProj x = s.ordConnectedProj y
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrdConnectedComponent (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
x y : (↑s : Type u_1)
h : s.ordConnectedProj x = s.ordConnectedProj y
⊢ [[(↑x : α), (↑y : α)]] ⊆ s
have mp : (↑y : α) ∈ s
Tactic: rw [← mem_ordConnectedComponent, ← ordConnectedComponent_ordConnectedProj, h,
      ordConnectedComponent_ordConnectedProj, self_mem_ordConnectedComponent]