awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
refine_1 : z ∉ Ioo x y
⊢ y ≤ z

Tactic:
suffices z ∉ Ioo x y by simp_all
-- 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
⊢ z ∉ Ioo x y

Tactic:
fun contra ↦ hxy contra <| h'.out hx hy <| mem_Icc_of_Ioo contra

Premises used: Set.OrdConnected.out, Set.mem_Icc_of_Ioo, Not
-- 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
⊢ z ∉ Ioo x y

Tactic:
exact fun contra ↦ hxy contra <| h'.out hx hy <| mem_Icc_of_Ioo contra

Premises used: Set.OrdConnected.out, Set.mem_Icc_of_Ioo
-- Module: Mathlib.Order.Interval.Set.OrdConnectedLinear
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
refine_2 : ∀ (hz' : z ∉ I), False
⊢ z ∈ I

Tactic:
by_contra hz'
-- Module: Mathlib.Order.Interval.Set.OrdConnectedLinear
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
refine_2 : ∀ (x' : α) (hx' : x ≤ x') (hx'' : Maximal (fun (x_1 : α) ↦ x_1 ∈ I ∩ Icc x z) x'), False
⊢ False

Tactic:
obtain ⟨x', hx', hx''⟩ :=
      ((finite_Icc x z).inter_of_right I).exists_le_maximal ⟨hx, le_refl _, hz.1.le⟩

Premises used: le_refl, LT.lt.le, Set.Finite.exists_le_maximal, Set.finite_Icc, Set.Finite.inter_of_right, And.left, And.intro
-- Module: Mathlib.Order.Interval.Set.OrdConnectedLinear
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'
⊢ 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')
-- Module: Mathlib.Order.Interval.Set.OrdConnectedLinear
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
refine_2 : ∀ (y' : α) (hy' : y' ≤ y) (hy'' : Minimal (fun (x : α) ↦ x ∈ I ∩ Icc z y) y'), False
⊢ False

Tactic:
obtain ⟨y', hy', hy''⟩ :=
      ((finite_Icc z y).inter_of_right I).exists_le_minimal ⟨hy, hz.2.le, le_refl _⟩

Premises used: le_refl, LT.lt.le, Set.finite_Icc, Set.Finite.inter_of_right, And.right, And.intro, Set.Finite.exists_le_minimal
-- Module: Mathlib.Order.Interval.Set.OrdConnectedLinear
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
y' : α
hy' : y' ≤ y
hy'' : Minimal (fun (x : α) ↦ x ∈ I ∩ Icc z y) y'
⊢ z < y'

Tactic:
have hzy : z < y' := lt_of_le_of_ne' hy''.1.2.1 (ne_of_mem_of_not_mem hy''.1.1 hz')
-- Module: Mathlib.Order.Interval.Set.OrdConnectedLinear
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
y' : α
hy' : y' ≤ y
hy'' : Minimal (fun (x : α) ↦ x ∈ I ∩ Icc z y) y'
hzy : z < y'
⊢ Ioc x' z ⊆ Iᶜ

Tactic:
have h₃ : Ioc x' z ⊆ Iᶜ := fun t ht ht' ↦ hx''.not_gt (⟨ht', le_trans hx' ht.1.le, ht.2⟩) ht.1
-- Module: Mathlib.Order.Interval.Set.OrdConnectedLinear
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
y' : α
hy' : y' ≤ y
hy'' : Minimal (fun (x : α) ↦ x ∈ I ∩ Icc z y) y'
hzy : z < y'
h₃ : Ioc x' z ⊆ Iᶜ
⊢ Ico z y' ⊆ Iᶜ

Tactic:
have h₄ : Ico z y' ⊆ Iᶜ := fun t ht ht' ↦ hy''.not_lt (⟨ht', ht.1, le_trans ht.2.le hy'⟩) ht.2
-- Module: Mathlib.Order.Interval.Set.OrdConnectedLinear
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
y' : α
hy' : y' ≤ y
hy'' : Minimal (fun (x : α) ↦ x ∈ I ∩ Icc z y) y'
hzy : z < y'
h₃ : Ioc x' z ⊆ Iᶜ
h₄ : Ico z y' ⊆ Iᶜ
⊢ Ioo x' y' ⊆ Iᶜ

Tactic:
simp only [← Ioc_union_Ico_eq_Ioo hxz hzy, union_subset_iff, and_true, h₃, h₄]

Premises used: and_true, Set.union_subset_iff, Set.Ioc_union_Ico_eq_Ioo
-- Module: Mathlib.Order.Interval.Set.OrdConnectedLinear
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
y' : α
hy' : y' ≤ y
hy'' : Minimal (fun (x : α) ↦ x ∈ I ∩ Icc z y) y'
hzy : z < y'
h₃ : Ioc x' z ⊆ Iᶜ
h₄ : Ico z y' ⊆ Iᶜ
⊢ Ioo x' y' ⊆ Iᶜ

Tactic:
have h₅ : Ioo x' y' ⊆ Iᶜ := by
      simp only [← Ioc_union_Ico_eq_Ioo hxz hzy, union_subset_iff, and_true, h₃, h₄]
-- Module: Mathlib.Order.Interval.Set.OrdConnectedLinear
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
y' : α
hy' : y' ≤ y
hy'' : Minimal (fun (x : α) ↦ x ∈ I ∩ Icc z y) y'
hzy : z < y'
h₃ : Ioc x' z ⊆ Iᶜ
h₄ : Ico z y' ⊆ Iᶜ
h₅ : Ioo x' y' ⊆ Iᶜ
⊢ False

Tactic:
eq_empty_iff_forall_notMem.1 (h' x' hx''.prop.1 y' hy''.prop.1 h₅) z ⟨hxz, hzy⟩

Premises used: Minimal.prop, Maximal.prop, And.left, Set.eq_empty_iff_forall_notMem, And.intro, Iff.mp
-- Module: Mathlib.Order.Interval.Set.OrdConnectedLinear
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
y' : α
hy' : y' ≤ y
hy'' : Minimal (fun (x : α) ↦ x ∈ I ∩ Icc z y) y'
hzy : z < y'
h₃ : Ioc x' z ⊆ Iᶜ
h₄ : Ico z y' ⊆ Iᶜ
h₅ : Ioo x' y' ⊆ Iᶜ
⊢ False

Tactic:
exact eq_empty_iff_forall_notMem.1 (h' x' hx''.prop.1 y' hy''.prop.1 h₅) z ⟨hxz, hzy⟩

Premises used: Minimal.prop, Maximal.prop, And.left, Set.eq_empty_iff_forall_notMem, And.intro, Iff.mp
-- Module: Mathlib.Order.Interval.Set.OrdConnectedLinear
Goal:
I : Set ℕ
h₀ : I.Nonempty
h₂ : BddAbove I
⊢ I = Icc (sInf I) (sSup I) ↔ ∀ x ∈ I, ∀ y ∈ I, Disjoint (Ioo x y) I → y ≤ x + 1

Tactic:
simp [← h₀.ordConnected_iff_of_bdd (OrderBot.bddBelow I) h₂, ordConnected_iff_disjoint_Ioo_empty]

Premises used: Set.ordConnected_iff_disjoint_Ioo_empty, Set.Nonempty.ordConnected_iff_of_bdd, OrderBot.bddBelow
-- Module: Mathlib.Order.Interval.Set.OrdConnectedLinear
Goal:
I : Set ℤ
h₀ : I.Nonempty
h₁ : BddBelow I
h₂ : BddAbove I
⊢ I = Icc (sInf I) (sSup I) ↔ ∀ x ∈ I, ∀ y ∈ I, Disjoint (Ioo x y) I → y ≤ x + 1

Tactic:
simp [← h₀.ordConnected_iff_of_bdd h₁ h₂, ordConnected_iff_disjoint_Ioo_empty]

Premises used: Set.ordConnected_iff_disjoint_Ioo_empty, Set.Nonempty.ordConnected_iff_of_bdd
-- Module: Mathlib.Order.Interval.Set.OrderEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
e : α ↪o β
x : α
⊢ preimage.{u_1, u_2} (β := β) ((⇑e : (a : α) → β) : (a : α) → β) (Ici ((e : (a : α) → β) x) : Set β) = Ici x

Tactic:
ext fun _ ↦ e.le_iff_le

Premises used: Set.ext, OrderEmbedding.le_iff_le
-- Module: Mathlib.Order.Interval.Set.OrderEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
e : α ↪o β
x : α
⊢ preimage.{u_1, u_2} (β := β) ((⇑e : (a : α) → β) : (a : α) → β) (Ioi ((e : (a : α) → β) x) : Set β) = Ioi x

Tactic:
ext fun _ ↦ e.lt_iff_lt

Premises used: Set.ext, OrderEmbedding.lt_iff_lt
-- Module: Mathlib.Order.Interval.Set.OrderEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
e : α ↪o β
x y : α
h :
  ∀ (x_1 : α),
    Membership.mem (γ := Set α)
        (preimage.{u_1, u_2} (β := β) ((⇑e : (a : α) → β) : (a : α) → β)
          (Icc ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β))
        x_1 ↔
      x_1 ∈ Icc x y
⊢ preimage.{u_1, u_2} (β := β) ((⇑e : (a : α) → β) : (a : α) → β)
      (Icc ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β) =
    Icc x y

Tactic:
ext
-- Module: Mathlib.Order.Interval.Set.OrderEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
e : α ↪o β
x y x_1 : α
⊢ Membership.mem (γ := Set α)
      (preimage.{u_1, u_2} (β := β) ((⇑e : (a : α) → β) : (a : α) → β)
        (Icc ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β))
      x_1 ↔
    x_1 ∈ Icc x y

Tactic:
simp
-- Module: Mathlib.Order.Interval.Set.OrderEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
e : α ↪o β
x y : α
h :
  ∀ (x_1 : α),
    Membership.mem (γ := Set α)
        (preimage.{u_1, u_2} (β := β) ((⇑e : (a : α) → β) : (a : α) → β)
          (Ico ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β))
        x_1 ↔
      x_1 ∈ Ico x y
⊢ preimage.{u_1, u_2} (β := β) ((⇑e : (a : α) → β) : (a : α) → β)
      (Ico ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β) =
    Ico x y

Tactic:
ext
-- Module: Mathlib.Order.Interval.Set.OrderEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
e : α ↪o β
x y x_1 : α
⊢ Membership.mem (γ := Set α)
      (preimage.{u_1, u_2} (β := β) ((⇑e : (a : α) → β) : (a : α) → β)
        (Ico ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β))
      x_1 ↔
    x_1 ∈ Ico x y

Tactic:
simp
-- Module: Mathlib.Order.Interval.Set.OrderEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
e : α ↪o β
x y : α
h :
  ∀ (x_1 : α),
    Membership.mem (γ := Set α)
        (preimage.{u_1, u_2} (β := β) ((⇑e : (a : α) → β) : (a : α) → β)
          (Ioc ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β))
        x_1 ↔
      x_1 ∈ Ioc x y
⊢ preimage.{u_1, u_2} (β := β) ((⇑e : (a : α) → β) : (a : α) → β)
      (Ioc ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β) =
    Ioc x y

Tactic:
ext
-- Module: Mathlib.Order.Interval.Set.OrderEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
e : α ↪o β
x y x_1 : α
⊢ Membership.mem (γ := Set α)
      (preimage.{u_1, u_2} (β := β) ((⇑e : (a : α) → β) : (a : α) → β)
        (Ioc ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β))
      x_1 ↔
    x_1 ∈ Ioc x y

Tactic:
simp
-- Module: Mathlib.Order.Interval.Set.OrderEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
e : α ↪o β
x y : α
h :
  ∀ (x_1 : α),
    Membership.mem (γ := Set α)
        (preimage.{u_1, u_2} (β := β) ((⇑e : (a : α) → β) : (a : α) → β)
          (Ioo ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β))
        x_1 ↔
      x_1 ∈ Ioo x y
⊢ preimage.{u_1, u_2} (β := β) ((⇑e : (a : α) → β) : (a : α) → β)
      (Ioo ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β) =
    Ioo x y

Tactic:
ext
-- Module: Mathlib.Order.Interval.Set.OrderEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
e : α ↪o β
x y x_1 : α
⊢ Membership.mem (γ := Set α)
      (preimage.{u_1, u_2} (β := β) ((⇑e : (a : α) → β) : (a : α) → β)
        (Ioo ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β))
      x_1 ↔
    x_1 ∈ Ioo x y

Tactic:
simp
-- Module: Mathlib.Order.Interval.Set.OrderEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Lattice β
e : α ↪o β
x y : α
inl :
  x ≤ y →
    preimage.{u_1, u_2} (β := β) ((⇑e : (a : α) → β) : (a : α) → β)
        (uIcc ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β) =
      uIcc x y
inr :
  y ≤ x →
    preimage.{u_1, u_2} (β := β) ((⇑e : (a : α) → β) : (a : α) → β)
        (uIcc ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β) =
      uIcc x y
⊢ preimage.{u_1, u_2} (β := β) ((⇑e : (a : α) → β) : (a : α) → β)
      (uIcc ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β) =
    uIcc x y

Tactic:
cases le_total x y

Premises used: le_total
-- Module: Mathlib.Order.Interval.Set.OrderEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Lattice β
e : α ↪o β
x y : α
h : x ≤ y
⊢ preimage.{u_1, u_2} (β := β) ((⇑e : (a : α) → β) : (a : α) → β)
      (uIcc ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β) =
    uIcc x y

Tactic:
simp [*]
-- Module: Mathlib.Order.Interval.Set.OrderEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Lattice β
e : α ↪o β
x y : α
h : y ≤ x
⊢ preimage.{u_1, u_2} (β := β) ((⇑e : (a : α) → β) : (a : α) → β)
      (uIcc ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β) =
    uIcc x y

Tactic:
simp [*]
-- Module: Mathlib.Order.Interval.Set.OrderEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
e : α ↪o β
x y : α
inl :
  x ≤ y →
    preimage.{u_1, u_2} (β := β) ((⇑e : (a : α) → β) : (a : α) → β)
        (uIoc ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β) =
      uIoc x y
inr :
  y ≤ x →
    preimage.{u_1, u_2} (β := β) ((⇑e : (a : α) → β) : (a : α) → β)
        (uIoc ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β) =
      uIoc x y
⊢ preimage.{u_1, u_2} (β := β) ((⇑e : (a : α) → β) : (a : α) → β)
      (uIoc ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β) =
    uIoc x y

Tactic:
cases le_total x y

Premises used: le_total
-- Module: Mathlib.Order.Interval.Set.OrderEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
e : α ↪o β
x y : α
h : x ≤ y
⊢ preimage.{u_1, u_2} (β := β) ((⇑e : (a : α) → β) : (a : α) → β)
      (uIoc ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β) =
    uIoc x y

Tactic:
simp [*]
-- Module: Mathlib.Order.Interval.Set.OrderEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
e : α ↪o β
x y : α
h : y ≤ x
⊢ preimage.{u_1, u_2} (β := β) ((⇑e : (a : α) → β) : (a : α) → β)
      (uIoc ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β) =
    uIoc x y

Tactic:
simp [*]
-- Module: Mathlib.Order.Interval.Set.OrderIso
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
e : α ≃o β
b : β
h :
  ∀ (x : α),
    Membership.mem (γ := Set α) ((⇑e : (a : α) → β) ⁻¹' Iic b) x ↔
      Membership.mem (γ := Set α) (Iic ((e.symm : (a : β) → α) b) : Set α) x
⊢ Eq.{u_1 + 1} (α := Set α) ((⇑e : (a : α) → β) ⁻¹' Iic b : Set α) (Iic ((e.symm : (a : β) → α) b) : Set α)

Tactic:
ext x
-- Module: Mathlib.Order.Interval.Set.OrderIso
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
e : α ≃o β
b : β
x : α
⊢ Membership.mem (γ := Set α) ((⇑e : (a : α) → β) ⁻¹' Iic b) x ↔
    Membership.mem (γ := Set α) (Iic ((e.symm : (a : β) → α) b) : Set α) x

Tactic:
simp [← e.le_iff_le]

Premises used: OrderIso.le_iff_le
-- Module: Mathlib.Order.Interval.Set.OrderIso
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
e : α ≃o β
b : β
h :
  ∀ (x : α),
    Membership.mem (γ := Set α) ((⇑e : (a : α) → β) ⁻¹' Iio b) x ↔
      Membership.mem (γ := Set α) (Iio ((e.symm : (a : β) → α) b) : Set α) x
⊢ Eq.{u_1 + 1} (α := Set α) ((⇑e : (a : α) → β) ⁻¹' Iio b : Set α) (Iio ((e.symm : (a : β) → α) b) : Set α)

Tactic:
ext x
-- Module: Mathlib.Order.Interval.Set.OrderIso
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
e : α ≃o β
b : β
x : α
⊢ Membership.mem (γ := Set α) ((⇑e : (a : α) → β) ⁻¹' Iio b) x ↔
    Membership.mem (γ := Set α) (Iio ((e.symm : (a : β) → α) b) : Set α) x

Tactic:
simp [← e.lt_iff_lt]

Premises used: OrderIso.lt_iff_lt
-- Module: Mathlib.Order.Interval.Set.OrderIso
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
e : α ≃o β
a b : β
⊢ Eq.{u_1 + 1} (α := Set α) ((⇑e : (a : α) → β) ⁻¹' Icc a b : Set α)
    (Icc ((e.symm : (a : β) → α) a) ((e.symm : (a : β) → α) b) : Set α)

Tactic:
simp [← Ici_inter_Iic]

Premises used: Set.Ici_inter_Iic
-- Module: Mathlib.Order.Interval.Set.OrderIso
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
e : α ≃o β
a b : β
⊢ Eq.{u_1 + 1} (α := Set α) ((⇑e : (a : α) → β) ⁻¹' Ico a b : Set α)
    (Ico ((e.symm : (a : β) → α) a) ((e.symm : (a : β) → α) b) : Set α)

Tactic:
simp [← Ici_inter_Iio]

Premises used: Set.Ici_inter_Iio
-- Module: Mathlib.Order.Interval.Set.OrderIso
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
e : α ≃o β
a b : β
⊢ Eq.{u_1 + 1} (α := Set α) ((⇑e : (a : α) → β) ⁻¹' Ioo a b : Set α)
    (Ioo ((e.symm : (a : β) → α) a) ((e.symm : (a : β) → α) b) : Set α)

Tactic:
simp [← Ioi_inter_Iio]

Premises used: Set.Ioi_inter_Iio
-- Module: Mathlib.Order.Interval.Set.OrderIso
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
e : α ≃o β
a : α
rw : Eq.{u_2 + 1} (α := Set β) ((⇑e.symm : (a : β) → α) ⁻¹' Iic a : Set β) (Iic ((e : (a : α) → β) a) : Set β)
rw₁ : Eq.{u_2 + 1} (α := Set β) (Iic ((e.symm.symm : (a : α) → β) a) : Set β) (Iic ((e : (a : α) → β) a) : Set β)
rw₂ rw₃ : Eq.{u_2 + 1} (α := Set β) (Iic ((e : (a : α) → β) a) : Set β) (Iic ((e : (a : α) → β) a) : Set β)
⊢ Eq.{u_2 + 1} (α := Set β) ((⇑e : (a : α) → β) '' Iic a : Set β) (Iic ((e : (a : α) → β) a) : Set β)

Tactic:
rw [e.image_eq_preimage_symm, e.symm.preimage_Iic, e.symm_symm]

Premises used: OrderIso.symm_symm, OrderIso.symm, OrderIso.image_eq_preimage_symm, OrderIso.preimage_Iic
-- Module: Mathlib.Order.Interval.Set.OrderIso
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
e : α ≃o β
a : α
rw : Eq.{u_2 + 1} (α := Set β) ((⇑e.symm : (a : β) → α) ⁻¹' Iio a : Set β) (Iio ((e : (a : α) → β) a) : Set β)
rw₁ : Eq.{u_2 + 1} (α := Set β) (Iio ((e.symm.symm : (a : α) → β) a) : Set β) (Iio ((e : (a : α) → β) a) : Set β)
rw₂ rw₃ : Eq.{u_2 + 1} (α := Set β) (Iio ((e : (a : α) → β) a) : Set β) (Iio ((e : (a : α) → β) a) : Set β)
⊢ Eq.{u_2 + 1} (α := Set β) ((⇑e : (a : α) → β) '' Iio a : Set β) (Iio ((e : (a : α) → β) a) : Set β)

Tactic:
rw [e.image_eq_preimage_symm, e.symm.preimage_Iio, e.symm_symm]

Premises used: OrderIso.symm_symm, OrderIso.preimage_Iio, OrderIso.symm, OrderIso.image_eq_preimage_symm
-- Module: Mathlib.Order.Interval.Set.OrderIso
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
e : α ≃o β
a b : α
rw :
  Eq.{u_2 + 1} (α := Set β) ((⇑e.symm : (a : β) → α) ⁻¹' Ioo a b : Set β)
    (Ioo ((e : (a : α) → β) a) ((e : (a : α) → β) b) : Set β)
rw₁ :
  Eq.{u_2 + 1} (α := Set β) (Ioo ((e.symm.symm : (a : α) → β) a) ((e.symm.symm : (a : α) → β) b) : Set β)
    (Ioo ((e : (a : α) → β) a) ((e : (a : α) → β) b) : Set β)
rw₂ rw₃ :
  Eq.{u_2 + 1} (α := Set β) (Ioo ((e : (a : α) → β) a) ((e : (a : α) → β) b) : Set β)
    (Ioo ((e : (a : α) → β) a) ((e : (a : α) → β) b) : Set β)
⊢ Eq.{u_2 + 1} (α := Set β) ((⇑e : (a : α) → β) '' Ioo a b : Set β)
    (Ioo ((e : (a : α) → β) a) ((e : (a : α) → β) b) : Set β)

Tactic:
rw [e.image_eq_preimage_symm, e.symm.preimage_Ioo, e.symm_symm]

Premises used: OrderIso.symm_symm, OrderIso.preimage_Ioo, OrderIso.symm, OrderIso.image_eq_preimage_symm
-- Module: Mathlib.Order.Interval.Set.OrderIso
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
e : α ≃o β
a b : α
rw :
  Eq.{u_2 + 1} (α := Set β) ((⇑e.symm : (a : β) → α) ⁻¹' Ioc a b : Set β)
    (Ioc ((e : (a : α) → β) a) ((e : (a : α) → β) b) : Set β)
rw₁ :
  Eq.{u_2 + 1} (α := Set β) (Ioc ((e.symm.symm : (a : α) → β) a) ((e.symm.symm : (a : α) → β) b) : Set β)
    (Ioc ((e : (a : α) → β) a) ((e : (a : α) → β) b) : Set β)
rw₂ rw₃ :
  Eq.{u_2 + 1} (α := Set β) (Ioc ((e : (a : α) → β) a) ((e : (a : α) → β) b) : Set β)
    (Ioc ((e : (a : α) → β) a) ((e : (a : α) → β) b) : Set β)
⊢ Eq.{u_2 + 1} (α := Set β) ((⇑e : (a : α) → β) '' Ioc a b : Set β)
    (Ioc ((e : (a : α) → β) a) ((e : (a : α) → β) b) : Set β)

Tactic:
rw [e.image_eq_preimage_symm, e.symm.preimage_Ioc, e.symm_symm]

Premises used: OrderIso.preimage_Ioc, OrderIso.symm_symm, OrderIso.symm, OrderIso.image_eq_preimage_symm
-- Module: Mathlib.Order.Interval.Set.OrderIso
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
e : α ≃o β
a b : α
rw :
  Eq.{u_2 + 1} (α := Set β) ((⇑e.symm : (a : β) → α) ⁻¹' Icc a b : Set β)
    (Icc ((e : (a : α) → β) a) ((e : (a : α) → β) b) : Set β)
rw₁ :
  Eq.{u_2 + 1} (α := Set β) (Icc ((e.symm.symm : (a : α) → β) a) ((e.symm.symm : (a : α) → β) b) : Set β)
    (Icc ((e : (a : α) → β) a) ((e : (a : α) → β) b) : Set β)
rw₂ rw₃ :
  Eq.{u_2 + 1} (α := Set β) (Icc ((e : (a : α) → β) a) ((e : (a : α) → β) b) : Set β)
    (Icc ((e : (a : α) → β) a) ((e : (a : α) → β) b) : Set β)
⊢ Eq.{u_2 + 1} (α := Set β) ((⇑e : (a : α) → β) '' Icc a b : Set β)
    (Icc ((e : (a : α) → β) a) ((e : (a : α) → β) b) : Set β)

Tactic:
rw [e.image_eq_preimage_symm, e.symm.preimage_Icc, e.symm_symm]

Premises used: OrderIso.symm_symm, OrderIso.symm, OrderIso.preimage_Icc, OrderIso.image_eq_preimage_symm
-- Module: Mathlib.Order.Interval.Set.OrderIso
Goal:
α : Type u_1
inst : Preorder α
inst_1 : OrderTop α
x y : (↑(Iic ⊤) : Type u_1)
⊢ LE.le (α := α)
      ((Equiv.subtypeUnivEquiv (p := fun (x : α) ↦ Membership.mem (γ := Set α) (Iic ⊤) x) ⋯ :
            (a : (↑(Iic ⊤) : Type u_1)) → α)
          x :
        α)
      ((Equiv.subtypeUnivEquiv (p := fun (x : α) ↦ Membership.mem (γ := Set α) (Iic ⊤) x) ⋯ :
            (a : (↑(Iic ⊤) : Type u_1)) → α)
          y :
        α) ↔
    x ≤ y

Tactic:
rfl
-- Module: Mathlib.Order.Interval.Set.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Preorder (α i)
x y : (i : ι) → α i
⊢ Membership.mem (γ := Set ((i : ι) → α i)) (pi (α := α) univ fun (i : ι) ↦ Ici (x i)) y ↔ y ∈ Ici x

Tactic:
simp [Pi.le_def]

Premises used: Pi.le_def
-- Module: Mathlib.Order.Interval.Set.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Preorder (α i)
x y_1 y : (i : ι) → α i
⊢ Membership.mem (γ := Set ((i : ι) → α i)) (pi (α := α) univ fun (i : ι) ↦ Icc (x i) (y_1 i)) y ↔ y ∈ Icc x y_1

Tactic:
simp [Pi.le_def, forall_and]

Premises used: Pi.le_def, forall_and
-- Module: Mathlib.Order.Interval.Set.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Preorder (α i)
s : Set ι
inst_1 : (j : ι) → Decidable (j ∈ s)
f₁ f₂ g₁ g₂ : (i : ι) → α i
h₁ : ∀ i ∈ s, f₁ i ∈ Icc (g₁ i) (g₂ i)
h₂ : ∀ i ∉ s, f₂ i ∈ Icc (g₁ i) (g₂ i)
⊢ s.piecewise (β := α) f₁ f₂ ∈ Icc g₁ g₂

Tactic:
⟨le_piecewise (fun i hi ↦ (h₁ i hi).1) fun i hi ↦ (h₂ i hi).1,
    piecewise_le (fun i hi ↦ (h₁ i hi).2) fun i hi ↦ (h₂ i hi).2⟩

Premises used: Set.Mem, setOf, Set.piecewise_le, Set.Icc, And.right, And.left, And.intro, Set.le_piecewise
-- Module: Mathlib.Order.Interval.Set.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Preorder (α i)
s : Set ι
inst_1 : (j : ι) → Decidable (j ∈ s)
f₁ f₂ g₁ g₂ : (i : ι) → α i
h₁ : f₁ ∈ Icc g₁ g₂
h₂ : f₂ ∈ Icc g₁ g₂
⊢ s.piecewise (β := α) f₁ f₂ ∈ Icc g₁ g₂

Tactic:
piecewise_mem_Icc (fun _ _ ↦ ⟨h₁.1 _, h₁.2 _⟩) fun _ _ ↦ ⟨h₂.1 _, h₂.2 _⟩

Premises used: Set.piecewise_mem_Icc, And.right, And.left, And.intro
-- Module: Mathlib.Order.Interval.Set.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Preorder (α i)
x : (i : ι) → α i
inst_1 : Nonempty ι
⊢ (pi (α := α) univ fun (i : ι) ↦ Ioi (x i)) ⊆ Ioi x

Tactic:
fun _ hz ↦
  ⟨fun i ↦ le_of_lt <| hz i trivial, fun h ↦
    (‹Nonempty ι›.elim) fun i ↦ not_lt_of_ge (h i) (hz i trivial)⟩

Premises used: Set.Ioi, trivial, Set.Mem, Nonempty.elim, setOf, le_of_lt, Set.Subset, And.intro, not_lt_of_ge