case h.h
α : Type u
β : Type v
inst✝² : SemilatticeInf α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : IsTotal α fun x x_1 => x ≤ x_1
x y : α
⊢ x ⊓ y = minDefault x y
α : Type u
β : Type v
inst✝² : SemilatticeInf α
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) = minDefault
ext (x y)
case h.h
α : Type u
β : Type v
inst✝² : SemilatticeInf α
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 x else y
case h.h
α : Type u
β : Type v
inst✝² : SemilatticeInf α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : IsTotal α fun x x_1 => x ≤ x_1
x y : α
⊢ x ⊓ y = minDefault x y
unfold minDefault
case h.h.inl
α : Type u
β : Type v
inst✝² : SemilatticeInf α
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.inr
α : Type u
β : Type v
inst✝² : SemilatticeInf α
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
α : Type u
β : Type v
inst✝² : SemilatticeInf α
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 x else y
split_ifs with h'