awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.InitialSeg (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r_1 : α → α → Prop
s_1 : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder α r
inst_1 : IsWellOrder β s
f : r ≺i Sum.Lex r s
g : s ≺i Sum.Lex r s
inl :
  ∀ (h : Sum.Lex r s (f.top (r := r) (s := Sum.Lex r s)) (g.top (r := s) (s := Sum.Lex r s))),
    Nonempty ((r ≼i s) ⊕ (s ≼i r))
⊢ Nonempty ((r ≼i s) ⊕ (s ≼i r))
have inr : ∀ (h : f.top (r := r) (s := Sum.Lex r s) = g.top (r := s) (s := Sum.Lex r s)), Nonempty ((r ≼i s) ⊕ (s ≼i r))
Tactic: obtain h | h | h := trichotomous_of (Sum.Lex r s) f.top g.top
-- Lean 4 proof step from Mathlib.Order.InitialSeg (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r_1 : α → α → Prop
s_1 : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder α r
inst_1 : IsWellOrder β s
f : r ≺i Sum.Lex r s
g : s ≺i Sum.Lex r s
inl :
  ∀ (h : Sum.Lex r s (f.top (r := r) (s := Sum.Lex r s)) (g.top (r := s) (s := Sum.Lex r s))),
    Nonempty ((r ≼i s) ⊕ (s ≼i r))
inr : ∀ (h : f.top (r := r) (s := Sum.Lex r s) = g.top (r := s) (s := Sum.Lex r s)), Nonempty ((r ≼i s) ⊕ (s ≼i r))
⊢ Nonempty ((r ≼i s) ⊕ (s ≼i r))
have inr₁ : ∀ (h : Sum.Lex r s (g.top (r := s) (s := Sum.Lex r s)) (f.top (r := r) (s := Sum.Lex r s))),
  Nonempty ((r ≼i s) ⊕ (s ≼i r))
Tactic: obtain h | h | h := trichotomous_of (Sum.Lex r s) f.top g.top
-- Lean 4 proof step from Mathlib.Order.InitialSeg (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r_1 : α → α → Prop
s_1 : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder α r
inst_1 : IsWellOrder β s
f_1 : r ≺i Sum.Lex r s
g : s ≺i Sum.Lex r s
h : f_1.top (r := r) (s := Sum.Lex r s) = g.top (r := s) (s := Sum.Lex r s)
f : RelIso (α := { x : α ⊕ β // Sum.Lex r s x (f_1.top (r := r) (s := Sum.Lex r s)) })
  (Subrel (Sum.Lex r s) fun (x : α ⊕ β) ↦ Sum.Lex r s x (f_1.top (r := r) (s := Sum.Lex r s))) r :=
  f_1.subrelIso (r := r) (s := Sum.Lex r s)
⊢ Nonempty ((r ≼i s) ⊕ (s ≼i r))
have inr : ∀
  (f :
    RelIso (α := { x : α ⊕ β // Sum.Lex r s x (g.top (r := s) (s := Sum.Lex r s)) })
      (Subrel (Sum.Lex r s) fun (x : α ⊕ β) ↦ Sum.Lex r s x (g.top (r := s) (s := Sum.Lex r s))) r),
  Nonempty ((r ≼i s) ⊕ (s ≼i r))
Tactic: rw [h] at f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Order.InitialSeg (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder β
a : α
b : β
inst_1 : LT α
f : (fun (x1 x2 : α) ↦ x1 < x2) ≼i fun (x1 x2 : β) ↦ x1 < x2
h : b ≤ (f : (a : α) → β) a
⊢ Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) b
have inl : ∀ (h : LE.le.{u_2} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) a : β)),
  Membership.mem.{u_2, u_2} (α := β) (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))
    ((f : (a : α) → β) a : β)
Tactic: obtain rfl | hb := h.eq_or_lt
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Order.InitialSeg (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder β
a : α
b : β
inst_1 : LT α
f : (fun (x1 x2 : α) ↦ x1 < x2) ≼i fun (x1 x2 : β) ↦ x1 < x2
h : b ≤ (f : (a : α) → β) a
inl :
  ∀ (h : LE.le.{u_2} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) a : β)),
    Membership.mem.{u_2, u_2} (α := β) (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))
      ((f : (a : α) → β) a : β)
⊢ Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) b
have inr : ∀ (hb : b < (f : (a : α) → β) a), Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) b
Tactic: obtain rfl | hb := h.eq_or_lt
-- Lean 4 proof step from Mathlib.Order.InitialSeg (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder β
a : α
inst_1 : PartialOrder α
f : (fun (x1 x2 : α) ↦ x1 < x2) ≼i fun (x1 x2 : β) ↦ x1 < x2
⊢ IsMin.{u_2} (α := β) ((f : (a : α) → β) a : β) ↔ IsMin a
have refine : ∀ (h : IsMin a) (b : β) (hb : b ≤ (f : (a : α) → β) a), (f : (a : α) → β) a ≤ b
Tactic: refine ⟨StrictMono.isMin_of_apply f.strictMono, fun h b hb ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.InitialSeg (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder β
a : α
inst_1 : PartialOrder α
f : (fun (x1 x2 : α) ↦ x1 < x2) ≼i fun (x1 x2 : β) ↦ x1 < x2
h : IsMin a
b : β
hb : b ≤ (f : (a : α) → β) a
⊢ (f : (a : α) → β) a ≤ b
have obtain : ∀ (x : α) (hb : LE.le.{u_2} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) a : β)),
  LE.le.{u_2} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) x : β)
Tactic: obtain ⟨x, rfl⟩ := f.mem_range_of_le hb
Cleared hypotheses: b, hb
-- Lean 4 proof step from Mathlib.Order.InitialSeg (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder β
a : α
inst_1 : PartialOrder α
f : (fun (x1 x2 : α) ↦ x1 < x2) ≼i fun (x1 x2 : β) ↦ x1 < x2
h : IsMin a
x : α
hb : LE.le.{u_2} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) a : β)
⊢ LE.le.{u_2} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) x : β)
have rw : ∀ (hb : x ≤ a), a ≤ x
Tactic: rw [f.le_iff_le] at hb ⊢
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Order.InitialSeg (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder β
a : α
b : β
inst_1 : PartialOrder α
f : (fun (x1 x2 : α) ↦ x1 < x2) ≼i fun (x1 x2 : β) ↦ x1 < x2
⊢ b ≤ (f : (a : α) → β) a ↔ ∃ c ≤ a, (f : (a : α) → β) c = b
have mp : b ≤ (f : (a : α) → β) a → ∃ c ≤ a, (f : (a : α) → β) c = b
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.InitialSeg (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder β
a : α
b : β
inst_1 : PartialOrder α
f : (fun (x1 x2 : α) ↦ x1 < x2) ≼i fun (x1 x2 : β) ↦ x1 < x2
mp : b ≤ (f : (a : α) → β) a → ∃ c ≤ a, (f : (a : α) → β) c = b
⊢ b ≤ (f : (a : α) → β) a ↔ ∃ c ≤ a, (f : (a : α) → β) c = b
have mpr : (∃ c ≤ a, (f : (a : α) → β) c = b) → b ≤ (f : (a : α) → β) a
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.InitialSeg (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder β
a : α
b : β
inst_1 : PartialOrder α
f : (fun (x1 x2 : α) ↦ x1 < x2) ≼i fun (x1 x2 : β) ↦ x1 < x2
h : b ≤ (f : (a : α) → β) a
⊢ ∃ c ≤ a, (f : (a : α) → β) c = b
have mp : ∀ (c : α) (hc : (f : (a : α) → β) c = b), ∃ c ≤ a, (f : (a : α) → β) c = b
Tactic: obtain ⟨c, hc⟩ := f.mem_range_of_le h
-- Lean 4 proof step from Mathlib.Order.InitialSeg (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder β
a : α
b : β
inst_1 : PartialOrder α
f : (fun (x1 x2 : α) ↦ x1 < x2) ≼i fun (x1 x2 : β) ↦ x1 < x2
h : b ≤ (f : (a : α) → β) a
c : α
hc : (f : (a : α) → β) c = b
⊢ ∃ c ≤ a, (f : (a : α) → β) c = b
have mp : c ≤ a
Tactic: refine ⟨c, ?_, hc⟩
-- Lean 4 proof step from Mathlib.Order.InitialSeg (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder β
a : α
b : β
inst_1 : PartialOrder α
f : (fun (x1 x2 : α) ↦ x1 < x2) ≼i fun (x1 x2 : β) ↦ x1 < x2
h : b ≤ (f : (a : α) → β) a
c : α
hc : (f : (a : α) → β) c = b
⊢ c ≤ a
have mp : ∀ (h : LE.le.{u_2} (α := β) ((f : (a : α) → β) c : β) ((f : (a : α) → β) a : β)) (hc : (f : (a : α) → β) c = b), c ≤ a
Tactic: rwa [← hc, f.le_iff_le] at h
Cleared hypotheses: h, hc
-- Lean 4 proof step from Mathlib.Order.InitialSeg (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder β
a : α
b : β
inst_1 : PartialOrder α
f : (fun (x1 x2 : α) ↦ x1 < x2) ≼i fun (x1 x2 : β) ↦ x1 < x2
h : b ≤ (f : (a : α) → β) a
c : α
hc : (f : (a : α) → β) c = b
mp :
  ∀ (h : LE.le.{u_2} (α := β) ((f : (a : α) → β) c : β) ((f : (a : α) → β) a : β)) (hc : (f : (a : α) → β) c = b), c ≤ a
⊢ c ≤ a
have mp₁ : ∀ (h : c ≤ a) (hc : (f : (a : α) → β) c = b), c ≤ a
Tactic: rwa [← hc, f.le_iff_le] at h
Cleared hypotheses: h, hc
-- Lean 4 proof step from Mathlib.Order.InitialSeg (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder β
a : α
b : β
inst_1 : PartialOrder α
f : (fun (x1 x2 : α) ↦ x1 < x2) ≼i fun (x1 x2 : β) ↦ x1 < x2
⊢ b < (f : (a : α) → β) a ↔ ∃ a' < a, (f : (a : α) → β) a' = b
have mp : b < (f : (a : α) → β) a → ∃ a' < a, (f : (a : α) → β) a' = b
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.InitialSeg (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder β
a : α
b : β
inst_1 : PartialOrder α
f : (fun (x1 x2 : α) ↦ x1 < x2) ≼i fun (x1 x2 : β) ↦ x1 < x2
mp : b < (f : (a : α) → β) a → ∃ a' < a, (f : (a : α) → β) a' = b
⊢ b < (f : (a : α) → β) a ↔ ∃ a' < a, (f : (a : α) → β) a' = b
have mpr : (∃ a' < a, (f : (a : α) → β) a' = b) → b < (f : (a : α) → β) a
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.InitialSeg (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder β
a : α
b : β
inst_1 : PartialOrder α
f : (fun (x1 x2 : α) ↦ x1 < x2) ≼i fun (x1 x2 : β) ↦ x1 < x2
h : b < (f : (a : α) → β) a
⊢ ∃ a' < a, (f : (a : α) → β) a' = b
have mp : ∀ (c : α) (hc : (f : (a : α) → β) c = b), ∃ a' < a, (f : (a : α) → β) a' = b
Tactic: obtain ⟨c, hc⟩ := f.mem_range_of_rel h
-- Lean 4 proof step from Mathlib.Order.InitialSeg (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder β
a : α
b : β
inst_1 : PartialOrder α
f : (fun (x1 x2 : α) ↦ x1 < x2) ≼i fun (x1 x2 : β) ↦ x1 < x2
h : b < (f : (a : α) → β) a
c : α
hc : (f : (a : α) → β) c = b
⊢ ∃ a' < a, (f : (a : α) → β) a' = b
have mp : c < a
Tactic: refine ⟨c, ?_, hc⟩
-- Lean 4 proof step from Mathlib.Order.InitialSeg (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder β
a : α
b : β
inst_1 : PartialOrder α
f : (fun (x1 x2 : α) ↦ x1 < x2) ≼i fun (x1 x2 : β) ↦ x1 < x2
h : b < (f : (a : α) → β) a
c : α
hc : (f : (a : α) → β) c = b
⊢ c < a
have mp : ∀ (h : LT.lt.{u_2} (α := β) ((f : (a : α) → β) c : β) ((f : (a : α) → β) a : β)) (hc : (f : (a : α) → β) c = b), c < a
Tactic: rwa [← hc, f.lt_iff_lt] at h
Cleared hypotheses: h, hc
-- Lean 4 proof step from Mathlib.Order.InitialSeg (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder β
a : α
b : β
inst_1 : PartialOrder α
f : (fun (x1 x2 : α) ↦ x1 < x2) ≼i fun (x1 x2 : β) ↦ x1 < x2
h : b < (f : (a : α) → β) a
c : α
hc : (f : (a : α) → β) c = b
mp :
  ∀ (h : LT.lt.{u_2} (α := β) ((f : (a : α) → β) c : β) ((f : (a : α) → β) a : β)) (hc : (f : (a : α) → β) c = b), c < a
⊢ c < a
have mp₁ : ∀ (h : c < a) (hc : (f : (a : α) → β) c = b), c < a
Tactic: rwa [← hc, f.lt_iff_lt] at h
Cleared hypotheses: h, hc
-- Lean 4 proof step from Mathlib.Order.Interval.Basic (goal)
Goal:
α : Type u_1
inst : LE α
s t : NonemptyInterval α
h : s.toProd = t.toProd
⊢ s = t
have mk : ∀ (toProd : α × α) (fst_le_snd : toProd.1 ≤ toProd.2)
  (h : { toProd := toProd, fst_le_snd := fst_le_snd : NonemptyInterval α }.toProd = t.toProd),
  { toProd := toProd, fst_le_snd := fst_le_snd : NonemptyInterval α } = t
Tactic: cases s
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Order.Interval.Basic (goal)
Goal:
α : Type u_1
inst : LE α
t : NonemptyInterval α
toProd : α × α
fst_le_snd : toProd.1 ≤ toProd.2
h : { toProd := toProd, fst_le_snd := fst_le_snd : NonemptyInterval α }.toProd = t.toProd
⊢ { toProd := toProd, fst_le_snd := fst_le_snd : NonemptyInterval α } = t
have mk : ∀ (toProd_1 : α × α) (fst_le_snd_1 : toProd_1.1 ≤ toProd_1.2)
  (h :
    { toProd := toProd, fst_le_snd := fst_le_snd : NonemptyInterval α }.toProd =
      { toProd := toProd_1, fst_le_snd := fst_le_snd_1 : NonemptyInterval α }.toProd),
  { toProd := toProd, fst_le_snd := fst_le_snd : NonemptyInterval α } =
    { toProd := toProd_1, fst_le_snd := fst_le_snd_1 }
Tactic: cases t
Cleared hypotheses: t, h
-- Lean 4 proof step from Mathlib.Order.Interval.Basic (goal)
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
⊢ Membership.mem (γ := NonemptyInterval α) (pure a) b ↔ b = a
have rw : b ∈ (↑(pure a) : Set α) ↔ b = a
Tactic: rw [← SetLike.mem_coe, coe_pure, mem_singleton_iff]
-- Lean 4 proof step from Mathlib.Order.Interval.Basic (goal)
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
rw : b ∈ (↑(pure a) : Set α) ↔ b = a
⊢ Membership.mem (γ := NonemptyInterval α) (pure a) b ↔ b = a
have rw₁ : Membership.mem (γ := Set α) {a} b ↔ b = a
Tactic: rw [← SetLike.mem_coe, coe_pure, mem_singleton_iff]
-- Lean 4 proof step from Mathlib.Order.Interval.Basic (goal)
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
rw : b ∈ (↑(pure a) : Set α) ↔ b = a
rw₁ : Membership.mem (γ := Set α) {a} b ↔ b = a
⊢ Membership.mem (γ := NonemptyInterval α) (pure a) b ↔ b = a
have rw₂ : b = a ↔ b = a
Tactic: rw [← SetLike.mem_coe, coe_pure, mem_singleton_iff]
-- Lean 4 proof step from Mathlib.Order.Interval.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α →o β
s : Interval α
⊢ Eq (α := Interval βᵒᵈ) ((dual : (a : Interval β) → Interval βᵒᵈ) (map f s) : Interval βᵒᵈ)
    (map.{u_1, u_2} (α := αᵒᵈ) ((OrderHom.dual : (a : α →o β) → αᵒᵈ →o βᵒᵈ) f)
        ((dual : (a : Interval α) → Interval αᵒᵈ) s) :
      Interval βᵒᵈ)
have bot : Eq (α := Interval βᵒᵈ) ((dual : (a : Interval β) → Interval βᵒᵈ) (map f ⊥) : Interval βᵒᵈ)
  (map.{u_1, u_2} (α := αᵒᵈ) ((OrderHom.dual : (a : α →o β) → αᵒᵈ →o βᵒᵈ) f)
      ((dual : (a : Interval α) → Interval αᵒᵈ) ⊥) :
    Interval βᵒᵈ)
Tactic: cases s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Order.Interval.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α →o β
s : Interval α
bot :
  Eq (α := Interval βᵒᵈ) ((dual : (a : Interval β) → Interval βᵒᵈ) (map f ⊥) : Interval βᵒᵈ)
    (map.{u_1, u_2} (α := αᵒᵈ) ((OrderHom.dual : (a : α →o β) → αᵒᵈ →o βᵒᵈ) f)
        ((dual : (a : Interval α) → Interval αᵒᵈ) ⊥) :
      Interval βᵒᵈ)
⊢ Eq (α := Interval βᵒᵈ) ((dual : (a : Interval β) → Interval βᵒᵈ) (map f s) : Interval βᵒᵈ)
    (map.{u_1, u_2} (α := αᵒᵈ) ((OrderHom.dual : (a : α →o β) → αᵒᵈ →o βᵒᵈ) f)
        ((dual : (a : Interval α) → Interval αᵒᵈ) s) :
      Interval βᵒᵈ)
have coe : ∀ (a : NonemptyInterval α),
  Eq (α := Interval βᵒᵈ) ((dual : (a : Interval β) → Interval βᵒᵈ) (map f (↑a : Interval α)) : Interval βᵒᵈ)
    (map.{u_1, u_2} (α := αᵒᵈ) ((OrderHom.dual : (a : α →o β) → αᵒᵈ →o βᵒᵈ) f)
        ((dual : (a : Interval α) → Interval αᵒᵈ) (↑a : Interval α)) :
      Interval βᵒᵈ)
Tactic: cases s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Order.Interval.Basic (goal)
Goal:
α : Type u_1
inst : PartialOrder α
s : Interval α
⊢ (↑((dual : (a : Interval α) → Interval αᵒᵈ) s : Interval αᵒᵈ) : Set αᵒᵈ) = (⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' (↑s : Set α)
have bot : (↑((dual : (a : Interval α) → Interval αᵒᵈ) ⊥) : Set αᵒᵈ) = (⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' (↑⊥ : Set α)
Tactic: cases s with
  | bot => rfl
  | coe s₀ => exact NonemptyInterval.coe_dual s₀
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Order.Interval.Basic (goal)
Goal:
α : Type u_1
inst : PartialOrder α
s : Interval α
bot : (↑((dual : (a : Interval α) → Interval αᵒᵈ) ⊥) : Set αᵒᵈ) = (⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' (↑⊥ : Set α)
⊢ (↑((dual : (a : Interval α) → Interval αᵒᵈ) s : Interval αᵒᵈ) : Set αᵒᵈ) = (⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' (↑s : Set α)
have coe : ∀ (s₀ : NonemptyInterval α),
  (↑((dual : (a : Interval α) → Interval αᵒᵈ) (↑s₀ : Interval α) : Interval αᵒᵈ) : Set αᵒᵈ) =
    (⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' (↑(↑s₀ : Interval α) : Set α)
Tactic: cases s with
  | bot => rfl
  | coe s₀ => exact NonemptyInterval.coe_dual s₀
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Order.Interval.Basic (goal)
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
⊢ Membership.mem (γ := Interval α) (pure a) b ↔ b = a
have rw : b ∈ (↑(pure a) : Set α) ↔ b = a
Tactic: rw [← SetLike.mem_coe, coe_pure, mem_singleton_iff]
-- Lean 4 proof step from Mathlib.Order.Interval.Basic (goal)
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
rw : b ∈ (↑(pure a) : Set α) ↔ b = a
⊢ Membership.mem (γ := Interval α) (pure a) b ↔ b = a
have rw₁ : Membership.mem (γ := Set α) {a} b ↔ b = a
Tactic: rw [← SetLike.mem_coe, coe_pure, mem_singleton_iff]
-- Lean 4 proof step from Mathlib.Order.Interval.Basic (goal)
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
rw : b ∈ (↑(pure a) : Set α) ↔ b = a
rw₁ : Membership.mem (γ := Set α) {a} b ↔ b = a
⊢ Membership.mem (γ := Interval α) (pure a) b ↔ b = a
have rw₂ : b = a ↔ b = a
Tactic: rw [← SetLike.mem_coe, coe_pure, mem_singleton_iff]
-- Lean 4 proof step from Mathlib.Order.Interval.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst : Lattice α
inst_1 : DecidableLE α
s_1 t_1 : Interval α
s t : NonemptyInterval α
⊢ (if h : s.toProd.1 ≤ t.toProd.2 ∧ t.toProd.1 ≤ s.toProd.2 then
      (↑{ fst := s.toProd.1 ⊔ t.toProd.1, snd := s.toProd.2 ⊓ t.toProd.2, fst_le_snd := ⋯ } : Interval α)
    else ⊥) ≤
    some s
have pos : ∀ (h : s.toProd.1 ≤ t.toProd.2 ∧ t.toProd.1 ≤ s.toProd.2),
  (↑{ fst := s.toProd.1 ⊔ t.toProd.1, snd := s.toProd.2 ⊓ t.toProd.2, fst_le_snd := sorry : NonemptyInterval α } :
      Interval α) ≤
    some s
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Order.Interval.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst : Lattice α
inst_1 : DecidableLE α
s_1 t_1 : Interval α
s t : NonemptyInterval α
pos :
  ∀ (h : s.toProd.1 ≤ t.toProd.2 ∧ t.toProd.1 ≤ s.toProd.2),
    (↑{ fst := s.toProd.1 ⊔ t.toProd.1, snd := s.toProd.2 ⊓ t.toProd.2, fst_le_snd := ⋯ : NonemptyInterval α } :
        Interval α) ≤
      some s
⊢ (if h : s.toProd.1 ≤ t.toProd.2 ∧ t.toProd.1 ≤ s.toProd.2 then
      (↑{ fst := s.toProd.1 ⊔ t.toProd.1, snd := s.toProd.2 ⊓ t.toProd.2, fst_le_snd := ⋯ } : Interval α)
    else ⊥) ≤
    some s
have neg : ¬(s.toProd.1 ≤ t.toProd.2 ∧ t.toProd.1 ≤ s.toProd.2) → ⊥ ≤ some s
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Order.Interval.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst : Lattice α
inst_1 : DecidableLE α
s_1 t_1 : Interval α
s t : NonemptyInterval α
⊢ (if h : s.toProd.1 ≤ t.toProd.2 ∧ t.toProd.1 ≤ s.toProd.2 then
      (↑{ fst := s.toProd.1 ⊔ t.toProd.1, snd := s.toProd.2 ⊓ t.toProd.2, fst_le_snd := ⋯ } : Interval α)
    else ⊥) ≤
    some t
have pos : ∀ (h : s.toProd.1 ≤ t.toProd.2 ∧ t.toProd.1 ≤ s.toProd.2),
  (↑{ fst := s.toProd.1 ⊔ t.toProd.1, snd := s.toProd.2 ⊓ t.toProd.2, fst_le_snd := sorry : NonemptyInterval α } :
      Interval α) ≤
    some t
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Order.Interval.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst : Lattice α
inst_1 : DecidableLE α
s_1 t_1 : Interval α
s t : NonemptyInterval α
pos :
  ∀ (h : s.toProd.1 ≤ t.toProd.2 ∧ t.toProd.1 ≤ s.toProd.2),
    (↑{ fst := s.toProd.1 ⊔ t.toProd.1, snd := s.toProd.2 ⊓ t.toProd.2, fst_le_snd := ⋯ : NonemptyInterval α } :
        Interval α) ≤
      some t
⊢ (if h : s.toProd.1 ≤ t.toProd.2 ∧ t.toProd.1 ≤ s.toProd.2 then
      (↑{ fst := s.toProd.1 ⊔ t.toProd.1, snd := s.toProd.2 ⊓ t.toProd.2, fst_le_snd := ⋯ } : Interval α)
    else ⊥) ≤
    some t
have neg : ¬(s.toProd.1 ≤ t.toProd.2 ∧ t.toProd.1 ≤ s.toProd.2) → ⊥ ≤ some t
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Order.Interval.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst : Lattice α
inst_1 : DecidableLE α
s_1 t_1 c_1 : Interval α
s : NonemptyInterval α
t c : Interval α
hb : (↑s : Interval α) ≤ t
hc : (↑s : Interval α) ≤ c
⊢ (↑s : Interval α) ≤
    match (motive := Interval α → Interval α → Interval α) t, c with
    | none, x => ⊥
    | x, none => ⊥
    | some s, some t =>
      if h : s.toProd.1 ≤ t.toProd.2 ∧ t.toProd.1 ≤ s.toProd.2 then
        (↑{ fst := s.toProd.1 ⊔ t.toProd.1, snd := s.toProd.2 ⊓ t.toProd.2, fst_le_snd := ⋯ } : Interval α)
      else ⊥
have lift : ∀ (t : NonemptyInterval α) (hb : (↑s : Interval α) ≤ (↑t : Interval α)),
  (↑s : Interval α) ≤
    match (motive := Interval α → Interval α → Interval α) (↑t : Interval α), c with
    | none, x => ⊥
    | x, none => ⊥
    | some s, some t =>
      if h : s.toProd.1 ≤ t.toProd.2 ∧ t.toProd.1 ≤ s.toProd.2 then
        (↑{ fst := s.toProd.1 ⊔ t.toProd.1, snd := s.toProd.2 ⊓ t.toProd.2, fst_le_snd := sorry } : Interval α)
      else ⊥
Tactic: lift t to NonemptyInterval α using ne_bot_of_le_ne_bot WithBot.coe_ne_bot hb
Cleared hypotheses: t, hb
-- Lean 4 proof step from Mathlib.Order.Interval.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst : Lattice α
inst_1 : DecidableLE α
s_1 t_1 c_1 : Interval α
s : NonemptyInterval α
c : Interval α
hc : (↑s : Interval α) ≤ c
t : NonemptyInterval α
hb : (↑s : Interval α) ≤ (↑t : Interval α)
⊢ (↑s : Interval α) ≤
    match (motive := Interval α → Interval α → Interval α) (↑t : Interval α), c with
    | none, x => ⊥
    | x, none => ⊥
    | some s, some t =>
      if h : s.toProd.1 ≤ t.toProd.2 ∧ t.toProd.1 ≤ s.toProd.2 then
        (↑{ fst := s.toProd.1 ⊔ t.toProd.1, snd := s.toProd.2 ⊓ t.toProd.2, fst_le_snd := ⋯ } : Interval α)
      else ⊥
have lift : ∀ (c : NonemptyInterval α) (hc : (↑s : Interval α) ≤ (↑c : Interval α)),
  (↑s : Interval α) ≤
    match (motive := Interval α → Interval α → Interval α) (↑t : Interval α), (↑c : Interval α) with
    | none, x => ⊥
    | x, none => ⊥
    | some s, some t =>
      if h : s.toProd.1 ≤ t.toProd.2 ∧ t.toProd.1 ≤ s.toProd.2 then
        (↑{ fst := s.toProd.1 ⊔ t.toProd.1, snd := s.toProd.2 ⊓ t.toProd.2, fst_le_snd := sorry } : Interval α)
      else ⊥
Tactic: lift c to NonemptyInterval α using ne_bot_of_le_ne_bot WithBot.coe_ne_bot hc
Cleared hypotheses: c, hc
-- Lean 4 proof step from Mathlib.Order.Interval.Basic (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst : Lattice α
inst_1 : DecidableLE α
s_1 t_1 c_1 : Interval α
s t : NonemptyInterval α
hb : (↑s : Interval α) ≤ (↑t : Interval α)
c : NonemptyInterval α
hc : (↑s : Interval α) ≤ (↑c : Interval α)
⊢ (↑s : Interval α) ≤
    if h : t.toProd.1 ≤ c.toProd.2 ∧ c.toProd.1 ≤ t.toProd.2 then
      (↑{ fst := t.toProd.1 ⊔ c.toProd.1, snd := t.toProd.2 ⊓ c.toProd.2, fst_le_snd := ⋯ } : Interval α)
    else ⊥
have hb₁ : s ≤ t
Tactic: simp only [Interval.coe_le_coe] at hb hc ⊢
Cleared hypotheses: hb, hc
-- Lean 4 proof step from Mathlib.Order.Interval.Basic (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst : Lattice α
inst_1 : DecidableLE α
s_1 t_1 c_1 : Interval α
s t : NonemptyInterval α
hb : (↑s : Interval α) ≤ (↑t : Interval α)
c : NonemptyInterval α
hc : (↑s : Interval α) ≤ (↑c : Interval α)
hb₁ : s ≤ t
⊢ (↑s : Interval α) ≤
    if h : t.toProd.1 ≤ c.toProd.2 ∧ c.toProd.1 ≤ t.toProd.2 then
      (↑{ fst := t.toProd.1 ⊔ c.toProd.1, snd := t.toProd.2 ⊓ c.toProd.2, fst_le_snd := ⋯ } : Interval α)
    else ⊥
have hc₁ : s ≤ c
Tactic: simp only [Interval.coe_le_coe] at hb hc ⊢
Cleared hypotheses: hb, hc
-- Lean 4 proof step from Mathlib.Order.Interval.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst : Lattice α
inst_1 : DecidableLE α
s_1 t_1 c_1 : Interval α
s t c : NonemptyInterval α
hb : s ≤ t
hc : s ≤ c
⊢ (↑s : Interval α) ≤
    if h : t.toProd.1 ≤ c.toProd.2 ∧ c.toProd.1 ≤ t.toProd.2 then
      (↑{ fst := t.toProd.1 ⊔ c.toProd.1, snd := t.toProd.2 ⊓ c.toProd.2, fst_le_snd := ⋯ } : Interval α)
    else ⊥
have rw : s ≤ { fst := t.toProd.1 ⊔ c.toProd.1, snd := t.toProd.2 ⊓ c.toProd.2, fst_le_snd := sorry }
Tactic: rw [dif_pos, Interval.coe_le_coe]
-- Lean 4 proof step from Mathlib.Order.Interval.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst : Lattice α
inst_1 : DecidableLE α
s_1 t_1 c_1 : Interval α
s t c : NonemptyInterval α
hb : s ≤ t
hc : s ≤ c
rw : s ≤ { fst := t.toProd.1 ⊔ c.toProd.1, snd := t.toProd.2 ⊓ c.toProd.2, fst_le_snd := ⋯ }
⊢ (↑s : Interval α) ≤
    if h : t.toProd.1 ≤ c.toProd.2 ∧ c.toProd.1 ≤ t.toProd.2 then
      (↑{ fst := t.toProd.1 ⊔ c.toProd.1, snd := t.toProd.2 ⊓ c.toProd.2, fst_le_snd := ⋯ } : Interval α)
    else ⊥
have hc₁ : t.toProd.1 ≤ c.toProd.2 ∧ c.toProd.1 ≤ t.toProd.2
Tactic: rw [dif_pos, Interval.coe_le_coe]
-- Lean 4 proof step from Mathlib.Order.Interval.Basic (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst : Lattice α
inst_1 : DecidableLE α
s_1 t_1 c_1 : Interval α
s t c : NonemptyInterval α
hb : s ≤ t
hc : s ≤ c
⊢ t.toProd.1 ≤ c.toProd.2 ∧ c.toProd.1 ≤ t.toProd.2
have hb₁ : t.toProd.1 ≤ s.toProd.1
Tactic: rcases hb with ⟨hb₁, hb₂⟩
Cleared hypotheses: hb