case refine'_1
α : Type u_1
β : Type ?u.31757
inst✝ : PartialOrder α
a b c : α
h : Icc a b = {c}
⊢ a = c ∧ b = c

case refine'_2
α : Type u_1
β : Type ?u.31757
inst✝ : PartialOrder α
a b c : α
⊢ a = c ∧ b = c → Icc a b = {c}
α : Type u_1
β : Type ?u.31757
inst✝ : PartialOrder α
a b c : α
⊢ Icc a b = {c} ↔ a = c ∧ b = c
refine' ⟨fun h => _, _⟩
case refine'_1
α : Type u_1
β : Type ?u.31757
inst✝ : PartialOrder α
a b c : α
h : Icc a b = {c}
hab : a ≤ b
⊢ a = c ∧ b = c
case refine'_1
α : Type u_1
β : Type ?u.31757
inst✝ : PartialOrder α
a b c : α
h : Icc a b = {c}
⊢ a = c ∧ b = c
have hab : a ≤ b := nonempty_Icc.1 (h.symm.subst <| singleton_nonempty c)
no goals
case refine'_1
α : Type u_1
β : Type ?u.31757
inst✝ : PartialOrder α
a b c : α
h : Icc a b = {c}
hab : a ≤ b
⊢ a = c ∧ b = c
exact
  ⟨eq_of_mem_singleton <| h.subst <| left_mem_Icc.2 hab,
    eq_of_mem_singleton <| h.subst <| right_mem_Icc.2 hab⟩
case refine'_2.intro
α : Type u_1
β : Type ?u.31757
inst✝ : PartialOrder α
b : α
⊢ Icc b b = {b}
case refine'_2
α : Type u_1
β : Type ?u.31757
inst✝ : PartialOrder α
a b c : α
⊢ a = c ∧ b = c → Icc a b = {c}
rintro ⟨rfl, rfl⟩
no goals
case refine'_2.intro
α : Type u_1
β : Type ?u.31757
inst✝ : PartialOrder α
b : α
⊢ Icc b b = {b}
exact Icc_self _