case mk
α : Type u_1
β : Type ?u.463
γ : Type ?u.466
δ : Type ?u.469
ι : Sort ?u.472
κ : ι → Sort ?u.477
inst✝ : LE α
s t✝ t : NonemptyInterval α
toProd✝ : α × α
fst_le_snd✝ : toProd✝.fst ≤ toProd✝.snd
h : { toProd := toProd✝, fst_le_snd := fst_le_snd✝ }.toProd = t.toProd
⊢ { toProd := toProd✝, fst_le_snd := fst_le_snd✝ } = t
α : Type u_1
β : Type ?u.463
γ : Type ?u.466
δ : Type ?u.469
ι : Sort ?u.472
κ : ι → Sort ?u.477
inst✝ : LE α
s✝ t✝ s t : NonemptyInterval α
h : s.toProd = t.toProd
⊢ s = t
cases s
case mk.mk
α : Type u_1
β : Type ?u.463
γ : Type ?u.466
δ : Type ?u.469
ι : Sort ?u.472
κ : ι → Sort ?u.477
inst✝ : LE α
s t : NonemptyInterval α
toProd✝¹ : α × α
fst_le_snd✝¹ : toProd✝¹.fst ≤ toProd✝¹.snd
toProd✝ : α × α
fst_le_snd✝ : toProd✝.fst ≤ toProd✝.snd
h : { toProd := toProd✝¹, fst_le_snd := fst_le_snd✝¹ }.toProd = { toProd := toProd✝, fst_le_snd := fst_le_snd✝ }.toProd
⊢ { toProd := toProd✝¹, fst_le_snd := fst_le_snd✝¹ } = { toProd := toProd✝, fst_le_snd := fst_le_snd✝ }
case mk
α : Type u_1
β : Type ?u.463
γ : Type ?u.466
δ : Type ?u.469
ι : Sort ?u.472
κ : ι → Sort ?u.477
inst✝ : LE α
s t✝ t : NonemptyInterval α
toProd✝ : α × α
fst_le_snd✝ : toProd✝.fst ≤ toProd✝.snd
h : { toProd := toProd✝, fst_le_snd := fst_le_snd✝ }.toProd = t.toProd
⊢ { toProd := toProd✝, fst_le_snd := fst_le_snd✝ } = t
cases t
no goals
case mk.mk
α : Type u_1
β : Type ?u.463
γ : Type ?u.466
δ : Type ?u.469
ι : Sort ?u.472
κ : ι → Sort ?u.477
inst✝ : LE α
s t : NonemptyInterval α
toProd✝¹ : α × α
fst_le_snd✝¹ : toProd✝¹.fst ≤ toProd✝¹.snd
toProd✝ : α × α
fst_le_snd✝ : toProd✝.fst ≤ toProd✝.snd
h : { toProd := toProd✝¹, fst_le_snd := fst_le_snd✝¹ }.toProd = { toProd := toProd✝, fst_le_snd := fst_le_snd✝ }.toProd
⊢ { toProd := toProd✝¹, fst_le_snd := fst_le_snd✝¹ } = { toProd := toProd✝, fst_le_snd := fst_le_snd✝ }
congr