case h.h
α : Type u
β : Type v
inst✝² : SemilatticeSup α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : IsTotal α fun x x_1 => x ≤ x_1
x y : α
⊢ x ⊔ y = maxDefault x y
α : Type u
β : Type v
inst✝² : SemilatticeSup α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : IsTotal α fun x x_1 => x ≤ x_1
⊢ (fun x x_1 => x ⊔ x_1) = maxDefault
ext (x y)
case h.h
α : Type u
β : Type v
inst✝² : SemilatticeSup α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : IsTotal α fun x x_1 => x ≤ x_1
x y : α
⊢ x ⊔ y = if x ≤ y then y else x
case h.h
α : Type u
β : Type v
inst✝² : SemilatticeSup α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : IsTotal α fun x x_1 => x ≤ x_1
x y : α
⊢ x ⊔ y = maxDefault x y
unfold maxDefault
case h.h.inl
α : Type u
β : Type v
inst✝² : SemilatticeSup α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : IsTotal α fun x x_1 => x ≤ x_1
x y : α
h' : x ≤ y
⊢ x ⊔ y = y

case h.h.inr
α : Type u
β : Type v
inst✝² : SemilatticeSup α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : IsTotal α fun x x_1 => x ≤ x_1
x y : α
h' : ¬x ≤ y
⊢ x ⊔ y = x
case h.h
α : Type u
β : Type v
inst✝² : SemilatticeSup α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : IsTotal α fun x x_1 => x ≤ x_1
x y : α
⊢ x ⊔ y = if x ≤ y then y else x
split_ifs with h'