awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrdConnectedLinear (hypothesis)
Goal:
α : Type u_1
I : Set α
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
h' : ∀ x ∈ I, ∀ y ∈ I, Ioo x y ⊆ Iᶜ → Ioo x y = ∅
x : α
hx : x ∈ I
y : α
hy : y ∈ I
hxy : x < y
z : α
hz : z ∈ Ioo x y
hz' : z ∉ I
x' : α
hx' : x ≤ x'
hx'' : Maximal (fun (x_1 : α) ↦ x_1 ∈ I ∩ Icc x z) x'
hxz : x' < z
y' : α
hy' : y' ≤ y
hy'' : Minimal (fun (x : α) ↦ x ∈ I ∩ Icc z y) y'
⊢ False
have hzy : 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')
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrdConnectedLinear (hypothesis)
Goal:
α : Type u_1
I : Set α
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
h' : ∀ x ∈ I, ∀ y ∈ I, Ioo x y ⊆ Iᶜ → Ioo x y = ∅
x : α
hx : x ∈ I
y : α
hy : y ∈ I
hxy : x < y
z : α
hz : z ∈ Ioo x y
hz' : z ∉ I
x' : α
hx' : x ≤ x'
hx'' : Maximal (fun (x_1 : α) ↦ x_1 ∈ I ∩ Icc x z) x'
hxz : x' < z
y' : α
hy' : y' ≤ y
hy'' : Minimal (fun (x : α) ↦ x ∈ I ∩ Icc z y) y'
hzy : z < y'
⊢ False
have h₃ : 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
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrdConnectedLinear (hypothesis)
Goal:
α : Type u_1
I : Set α
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
h' : ∀ x ∈ I, ∀ y ∈ I, Ioo x y ⊆ Iᶜ → Ioo x y = ∅
x : α
hx : x ∈ I
y : α
hy : y ∈ I
hxy : x < y
z : α
hz : z ∈ Ioo x y
hz' : z ∉ I
x' : α
hx' : x ≤ x'
hx'' : Maximal (fun (x_1 : α) ↦ x_1 ∈ I ∩ Icc x z) x'
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ᶜ
⊢ False
have h₄ : 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
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrdConnectedLinear (hypothesis)
Goal:
α : Type u_1
I : Set α
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
h' : ∀ x ∈ I, ∀ y ∈ I, Ioo x y ⊆ Iᶜ → Ioo x y = ∅
x : α
hx : x ∈ I
y : α
hy : y ∈ I
hxy : x < y
z : α
hz : z ∈ Ioo x y
hz' : z ∉ I
x' : α
hx' : x ≤ x'
hx'' : Maximal (fun (x_1 : α) ↦ x_1 ∈ I ∩ Icc x z) x'
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ᶜ
⊢ False
have h₅ : 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₄]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrderEmbedding (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
e : α ↪o β
x y : α
⊢ preimage.{u_1, u_2} (β := β) ((⇑e : (a : α) → β) : (a : α) → β)
      (Icc ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β) =
    Icc x y
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrderEmbedding (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
e : α ↪o β
x y : α
⊢ preimage.{u_1, u_2} (β := β) ((⇑e : (a : α) → β) : (a : α) → β)
      (Ico ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β) =
    Ico x y
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrderEmbedding (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
e : α ↪o β
x y : α
⊢ preimage.{u_1, u_2} (β := β) ((⇑e : (a : α) → β) : (a : α) → β)
      (Ioc ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β) =
    Ioc x y
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrderEmbedding (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
e : α ↪o β
x y : α
⊢ preimage.{u_1, u_2} (β := β) ((⇑e : (a : α) → β) : (a : α) → β)
      (Ioo ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β) =
    Ioo x y
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrderEmbedding (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Lattice β
e : α ↪o β
x y : α
⊢ preimage.{u_1, u_2} (β := β) ((⇑e : (a : α) → β) : (a : α) → β)
      (uIcc ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β) =
    uIcc x y
have inl : 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
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrderEmbedding (goal)
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
⊢ preimage.{u_1, u_2} (β := β) ((⇑e : (a : α) → β) : (a : α) → β)
      (uIcc ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β) =
    uIcc x y
have inr : y ≤ x →
  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
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrderEmbedding (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
e : α ↪o β
x y : α
⊢ preimage.{u_1, u_2} (β := β) ((⇑e : (a : α) → β) : (a : α) → β)
      (uIoc ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β) =
    uIoc x y
have inl : 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
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrderEmbedding (goal)
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
⊢ preimage.{u_1, u_2} (β := β) ((⇑e : (a : α) → β) : (a : α) → β)
      (uIoc ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β) =
    uIoc x y
have inr : y ≤ x →
  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
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrderIso (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
e : α ≃o β
b : β
⊢ Eq.{u_1 + 1} (α := Set α) ((⇑e : (a : α) → β) ⁻¹' Iic b : Set α) (Iic ((e.symm : (a : β) → α) b) : Set α)
have h : ∀ (x : α),
  Membership.mem (γ := Set α) ((⇑e : (a : α) → β) ⁻¹' Iic b) x ↔
    Membership.mem (γ := Set α) (Iic ((e.symm : (a : β) → α) b) : Set α) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrderIso (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
e : α ≃o β
b : β
⊢ Eq.{u_1 + 1} (α := Set α) ((⇑e : (a : α) → β) ⁻¹' Iio b : Set α) (Iio ((e.symm : (a : β) → α) b) : Set α)
have h : ∀ (x : α),
  Membership.mem (γ := Set α) ((⇑e : (a : α) → β) ⁻¹' Iio b) x ↔
    Membership.mem (γ := Set α) (Iio ((e.symm : (a : β) → α) b) : Set α) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrderIso (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
e : α ≃o β
a : α
⊢ Eq.{u_2 + 1} (α := Set β) ((⇑e : (a : α) → β) '' Iic a : Set β) (Iic ((e : (a : α) → β) a) : Set β)
have rw : Eq.{u_2 + 1} (α := Set β) ((⇑e.symm : (a : β) → α) ⁻¹' Iic a : Set β) (Iic ((e : (a : α) → β) a) : Set β)
Tactic: rw [e.image_eq_preimage_symm, e.symm.preimage_Iic, e.symm_symm]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrderIso (goal)
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 β)
⊢ Eq.{u_2 + 1} (α := Set β) ((⇑e : (a : α) → β) '' Iic a : Set β) (Iic ((e : (a : α) → β) a) : Set β)
have rw₁ : Eq.{u_2 + 1} (α := Set β) (Iic ((e.symm.symm : (a : α) → β) a) : Set β) (Iic ((e : (a : α) → β) a) : Set β)
Tactic: rw [e.image_eq_preimage_symm, e.symm.preimage_Iic, e.symm_symm]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrderIso (goal)
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 β)
⊢ Eq.{u_2 + 1} (α := Set β) ((⇑e : (a : α) → β) '' Iic a : Set β) (Iic ((e : (a : α) → β) a) : Set β)
have rw₂ : Eq.{u_2 + 1} (α := Set β) (Iic ((e : (a : α) → β) a) : Set β) (Iic ((e : (a : α) → β) a) : Set β)
Tactic: rw [e.image_eq_preimage_symm, e.symm.preimage_Iic, e.symm_symm]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrderIso (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
e : α ≃o β
a : α
⊢ Eq.{u_2 + 1} (α := Set β) ((⇑e : (a : α) → β) '' Iio a : Set β) (Iio ((e : (a : α) → β) a) : Set β)
have rw : Eq.{u_2 + 1} (α := Set β) ((⇑e.symm : (a : β) → α) ⁻¹' Iio a : Set β) (Iio ((e : (a : α) → β) a) : Set β)
Tactic: rw [e.image_eq_preimage_symm, e.symm.preimage_Iio, e.symm_symm]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrderIso (goal)
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 β)
⊢ Eq.{u_2 + 1} (α := Set β) ((⇑e : (a : α) → β) '' Iio a : Set β) (Iio ((e : (a : α) → β) a) : Set β)
have rw₁ : Eq.{u_2 + 1} (α := Set β) (Iio ((e.symm.symm : (a : α) → β) a) : Set β) (Iio ((e : (a : α) → β) a) : Set β)
Tactic: rw [e.image_eq_preimage_symm, e.symm.preimage_Iio, e.symm_symm]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrderIso (goal)
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 β)
⊢ Eq.{u_2 + 1} (α := Set β) ((⇑e : (a : α) → β) '' Iio a : Set β) (Iio ((e : (a : α) → β) a) : Set β)
have rw₂ : Eq.{u_2 + 1} (α := Set β) (Iio ((e : (a : α) → β) a) : Set β) (Iio ((e : (a : α) → β) a) : Set β)
Tactic: rw [e.image_eq_preimage_symm, e.symm.preimage_Iio, e.symm_symm]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrderIso (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
e : α ≃o β
a b : α
⊢ Eq.{u_2 + 1} (α := Set β) ((⇑e : (a : α) → β) '' Ioo a b : Set β)
    (Ioo ((e : (a : α) → β) a) ((e : (a : α) → β) b) : Set β)
have rw : Eq.{u_2 + 1} (α := Set β) ((⇑e.symm : (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]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrderIso (goal)
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 β)
⊢ Eq.{u_2 + 1} (α := Set β) ((⇑e : (a : α) → β) '' Ioo a b : Set β)
    (Ioo ((e : (a : α) → β) a) ((e : (a : α) → β) b) : Set β)
have 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 β)
Tactic: rw [e.image_eq_preimage_symm, e.symm.preimage_Ioo, e.symm_symm]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrderIso (goal)
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 β)
⊢ Eq.{u_2 + 1} (α := Set β) ((⇑e : (a : α) → β) '' Ioo a b : Set β)
    (Ioo ((e : (a : α) → β) a) ((e : (a : α) → β) b) : Set β)
have rw₂ : Eq.{u_2 + 1} (α := Set β) (Ioo ((e : (a : α) → β) a) ((e : (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]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrderIso (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
e : α ≃o β
a b : α
⊢ Eq.{u_2 + 1} (α := Set β) ((⇑e : (a : α) → β) '' Ioc a b : Set β)
    (Ioc ((e : (a : α) → β) a) ((e : (a : α) → β) b) : Set β)
have rw : Eq.{u_2 + 1} (α := Set β) ((⇑e.symm : (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]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrderIso (goal)
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 β)
⊢ Eq.{u_2 + 1} (α := Set β) ((⇑e : (a : α) → β) '' Ioc a b : Set β)
    (Ioc ((e : (a : α) → β) a) ((e : (a : α) → β) b) : Set β)
have 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 β)
Tactic: rw [e.image_eq_preimage_symm, e.symm.preimage_Ioc, e.symm_symm]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrderIso (goal)
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 β)
⊢ Eq.{u_2 + 1} (α := Set β) ((⇑e : (a : α) → β) '' Ioc a b : Set β)
    (Ioc ((e : (a : α) → β) a) ((e : (a : α) → β) b) : Set β)
have rw₂ : Eq.{u_2 + 1} (α := Set β) (Ioc ((e : (a : α) → β) a) ((e : (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]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrderIso (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
e : α ≃o β
a b : α
⊢ Eq.{u_2 + 1} (α := Set β) ((⇑e : (a : α) → β) '' Icc a b : Set β)
    (Icc ((e : (a : α) → β) a) ((e : (a : α) → β) b) : Set β)
have rw : Eq.{u_2 + 1} (α := Set β) ((⇑e.symm : (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]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrderIso (goal)
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 β)
⊢ Eq.{u_2 + 1} (α := Set β) ((⇑e : (a : α) → β) '' Icc a b : Set β)
    (Icc ((e : (a : α) → β) a) ((e : (a : α) → β) b) : Set β)
have 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 β)
Tactic: rw [e.image_eq_preimage_symm, e.symm.preimage_Icc, e.symm_symm]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrderIso (goal)
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 β)
⊢ Eq.{u_2 + 1} (α := Set β) ((⇑e : (a : α) → β) '' Icc a b : Set β)
    (Icc ((e : (a : α) → β) a) ((e : (a : α) → β) b) : Set β)
have rw₂ : Eq.{u_2 + 1} (α := Set β) (Icc ((e : (a : α) → β) a) ((e : (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]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Preorder (α i)
inst_1 : DecidableEq ι
x y : (i : ι) → α i
i₀ : ι
m : α i₀
hm : x i₀ ≤ m
⊢ Ioc m (y i₀) = Ioi m ∩ Ioc (x i₀) (y i₀)
have rw : Ioi m ∩ Iic (y i₀) = Ioi m ∩ Ioc (x i₀) (y i₀)
Tactic: rw [← Ioi_inter_Iic, ← Ioi_inter_Iic, ← inter_assoc,
      inter_eq_self_of_subset_left (Ioi_subset_Ioi hm)]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Preorder (α i)
inst_1 : DecidableEq ι
x y : (i : ι) → α i
i₀ : ι
m : α i₀
hm : x i₀ ≤ m
rw : Ioi m ∩ Iic (y i₀) = Ioi m ∩ Ioc (x i₀) (y i₀)
⊢ Ioc m (y i₀) = Ioi m ∩ Ioc (x i₀) (y i₀)
have rw₁ : Ioi m ∩ Iic (y i₀) = Ioi m ∩ (Ioi (x i₀) ∩ Iic (y i₀))
Tactic: rw [← Ioi_inter_Iic, ← Ioi_inter_Iic, ← inter_assoc,
      inter_eq_self_of_subset_left (Ioi_subset_Ioi hm)]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Preorder (α i)
inst_1 : DecidableEq ι
x y : (i : ι) → α i
i₀ : ι
m : α i₀
hm : x i₀ ≤ m
rw : Ioi m ∩ Iic (y i₀) = Ioi m ∩ Ioc (x i₀) (y i₀)
rw₁ : Ioi m ∩ Iic (y i₀) = Ioi m ∩ (Ioi (x i₀) ∩ Iic (y i₀))
⊢ Ioc m (y i₀) = Ioi m ∩ Ioc (x i₀) (y i₀)
have rw₂ : Ioi m ∩ Iic (y i₀) = Ioi m ∩ Ioi (x i₀) ∩ Iic (y i₀)
Tactic: rw [← Ioi_inter_Iic, ← Ioi_inter_Iic, ← inter_assoc,
      inter_eq_self_of_subset_left (Ioi_subset_Ioi hm)]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Preorder (α i)
inst_1 : DecidableEq ι
x y : (i : ι) → α i
i₀ : ι
m : α i₀
hm : x i₀ ≤ m
rw : Ioi m ∩ Iic (y i₀) = Ioi m ∩ Ioc (x i₀) (y i₀)
rw₁ : Ioi m ∩ Iic (y i₀) = Ioi m ∩ (Ioi (x i₀) ∩ Iic (y i₀))
rw₂ : Ioi m ∩ Iic (y i₀) = Ioi m ∩ Ioi (x i₀) ∩ Iic (y i₀)
⊢ Ioc m (y i₀) = Ioi m ∩ Ioc (x i₀) (y i₀)
have rw₃ : Ioi m ∩ Iic (y i₀) = Ioi m ∩ Iic (y i₀)
Tactic: rw [← Ioi_inter_Iic, ← Ioi_inter_Iic, ← inter_assoc,
      inter_eq_self_of_subset_left (Ioi_subset_Ioi hm)]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Pi (hypothesis)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Preorder (α i)
inst_1 : DecidableEq ι
x y : (i : ι) → α i
i₀ : ι
m : α i₀
hm : x i₀ ≤ m
⊢ Eq (α := Set ((i : ι) → α i)) (pi (α := α) univ fun (i : ι) ↦ Ioc (update (β := α) x i₀ m i) (y i))
    ({z : (i : ι) → α i | m < z i₀} ∩ pi (α := α) univ fun (i : ι) ↦ Ioc (x i) (y i))
have this : Ioc m (y i₀) = Ioi m ∩ Ioc (x i₀) (y i₀)
Tactic: have : Ioc m (y i₀) = Ioi m ∩ Ioc (x i₀) (y i₀) := by
    rw [← Ioi_inter_Iic, ← Ioi_inter_Iic, ← inter_assoc,
      inter_eq_self_of_subset_left (Ioi_subset_Ioi hm)]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Preorder (α i)
inst_1 : DecidableEq ι
x y : (i : ι) → α i
i₀ : ι
m : α i₀
hm : x i₀ ≤ m
this : Ioc m (y i₀) = Ioi m ∩ Ioc (x i₀) (y i₀)
⊢ Eq (α := Set ((i : ι) → α i)) (pi (α := α) univ fun (i : ι) ↦ Ioc (update (β := α) x i₀ m i) (y i))
    ({z : (i : ι) → α i | m < z i₀} ∩ pi (α := α) univ fun (i : ι) ↦ Ioc (x i) (y i))
have simp_rw : Eq (α := Set ((i : ι) → α i))
  ({x_1 : (i : ι) → α i | x_1 i₀ ∈ Ioi m ∩ Ioc (x i₀) (y i₀)} ∩ pi (α := α) {i₀}ᶜ fun (j : ι) ↦ Ioc (x j) (y j))
  ({z : (i : ι) → α i | m < z i₀} ∩ {x_1 : (i : ι) → α i | x_1 i₀ ∈ Ioc (x i₀) (y i₀)} ∩
    pi (α := α) {i₀}ᶜ fun (j : ι) ↦ Ioc (x j) (y j))
Tactic: simp_rw [univ_pi_update i₀ _ _ fun i z ↦ Ioc z (y i), ← pi_inter_compl ({i₀} : Set ι),
    singleton_pi', ← inter_assoc, this]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Preorder (α i)
inst_1 : DecidableEq ι
x y : (i : ι) → α i
i₀ : ι
m : α i₀
hm : m ≤ y i₀
⊢ Ioc (x i₀) m = Iic m ∩ Ioc (x i₀) (y i₀)
have rw : Ioi (x i₀) ∩ Iic m = Iic m ∩ Ioc (x i₀) (y i₀)
Tactic: rw [← Ioi_inter_Iic, ← Ioi_inter_Iic, inter_left_comm,
      inter_eq_self_of_subset_left (Iic_subset_Iic.2 hm)]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Preorder (α i)
inst_1 : DecidableEq ι
x y : (i : ι) → α i
i₀ : ι
m : α i₀
hm : m ≤ y i₀
rw : Ioi (x i₀) ∩ Iic m = Iic m ∩ Ioc (x i₀) (y i₀)
⊢ Ioc (x i₀) m = Iic m ∩ Ioc (x i₀) (y i₀)
have rw₁ : Ioi (x i₀) ∩ Iic m = Iic m ∩ (Ioi (x i₀) ∩ Iic (y i₀))
Tactic: rw [← Ioi_inter_Iic, ← Ioi_inter_Iic, inter_left_comm,
      inter_eq_self_of_subset_left (Iic_subset_Iic.2 hm)]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Preorder (α i)
inst_1 : DecidableEq ι
x y : (i : ι) → α i
i₀ : ι
m : α i₀
hm : m ≤ y i₀
rw : Ioi (x i₀) ∩ Iic m = Iic m ∩ Ioc (x i₀) (y i₀)
rw₁ : Ioi (x i₀) ∩ Iic m = Iic m ∩ (Ioi (x i₀) ∩ Iic (y i₀))
⊢ Ioc (x i₀) m = Iic m ∩ Ioc (x i₀) (y i₀)
have rw₂ : Ioi (x i₀) ∩ Iic m = Ioi (x i₀) ∩ (Iic m ∩ Iic (y i₀))
Tactic: rw [← Ioi_inter_Iic, ← Ioi_inter_Iic, inter_left_comm,
      inter_eq_self_of_subset_left (Iic_subset_Iic.2 hm)]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Preorder (α i)
inst_1 : DecidableEq ι
x y : (i : ι) → α i
i₀ : ι
m : α i₀
hm : m ≤ y i₀
rw : Ioi (x i₀) ∩ Iic m = Iic m ∩ Ioc (x i₀) (y i₀)
rw₁ : Ioi (x i₀) ∩ Iic m = Iic m ∩ (Ioi (x i₀) ∩ Iic (y i₀))
rw₂ : Ioi (x i₀) ∩ Iic m = Ioi (x i₀) ∩ (Iic m ∩ Iic (y i₀))
⊢ Ioc (x i₀) m = Iic m ∩ Ioc (x i₀) (y i₀)
have rw₃ : Ioi (x i₀) ∩ Iic m = Ioi (x i₀) ∩ Iic m
Tactic: rw [← Ioi_inter_Iic, ← Ioi_inter_Iic, inter_left_comm,
      inter_eq_self_of_subset_left (Iic_subset_Iic.2 hm)]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Pi (hypothesis)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Preorder (α i)
inst_1 : DecidableEq ι
x y : (i : ι) → α i
i₀ : ι
m : α i₀
hm : m ≤ y i₀
⊢ Eq (α := Set ((i : ι) → α i)) (pi (α := α) univ fun (i : ι) ↦ Ioc (x i) (update (β := α) y i₀ m i))
    ({z : (i : ι) → α i | z i₀ ≤ m} ∩ pi (α := α) univ fun (i : ι) ↦ Ioc (x i) (y i))
have this : Ioc (x i₀) m = Iic m ∩ Ioc (x i₀) (y i₀)
Tactic: have : Ioc (x i₀) m = Iic m ∩ Ioc (x i₀) (y i₀) := by
    rw [← Ioi_inter_Iic, ← Ioi_inter_Iic, inter_left_comm,
      inter_eq_self_of_subset_left (Iic_subset_Iic.2 hm)]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Preorder (α i)
inst_1 : DecidableEq ι
x y : (i : ι) → α i
i₀ : ι
m : α i₀
hm : m ≤ y i₀
this : Ioc (x i₀) m = Iic m ∩ Ioc (x i₀) (y i₀)
⊢ Eq (α := Set ((i : ι) → α i)) (pi (α := α) univ fun (i : ι) ↦ Ioc (x i) (update (β := α) y i₀ m i))
    ({z : (i : ι) → α i | z i₀ ≤ m} ∩ pi (α := α) univ fun (i : ι) ↦ Ioc (x i) (y i))
have simp_rw : Eq (α := Set ((i : ι) → α i))
  ({x_1 : (i : ι) → α i | x_1 i₀ ∈ Iic m ∩ Ioc (x i₀) (y i₀)} ∩ pi (α := α) {i₀}ᶜ fun (j : ι) ↦ Ioc (x j) (y j))
  ({z : (i : ι) → α i | z i₀ ≤ m} ∩ {x_1 : (i : ι) → α i | x_1 i₀ ∈ Ioc (x i₀) (y i₀)} ∩
    pi (α := α) {i₀}ᶜ fun (j : ι) ↦ Ioc (x j) (y j))
Tactic: simp_rw [univ_pi_update i₀ y m fun i z ↦ Ioc (x i) z, ← pi_inter_compl ({i₀} : Set ι),
    singleton_pi', ← inter_assoc, this]