α : Type u_2
β : Type u_1
β₂ : Type ?u.98007
γ : Type ?u.98010
ι : Sort ?u.98013
ι' : Sort ?u.98016
κ : ι → Sort ?u.98021
κ' : ι' → Sort ?u.98026
inst✝ : CompleteLattice α
f✝ g s t : ι → α
a b✝ : α
b : β
f : (x : β) → b = x → α
⊢ f b (_ : b = b) ≤ f b (_ : b = b)
α : Type u_2
β : Type u_1
β₂ : Type ?u.98007
γ : Type ?u.98010
ι : Sort ?u.98013
ι' : Sort ?u.98016
κ : ι → Sort ?u.98021
κ' : ι' → Sort ?u.98026
inst✝ : CompleteLattice α
f✝ g s t : ι → α
a b✝ : α
b : β
f : (x : β) → b = x → α
c : β
⊢ ∀ (j : b = c), f c j ≤ f b (_ : b = b)
rintro rfl
no goals
α : Type u_2
β : Type u_1
β₂ : Type ?u.98007
γ : Type ?u.98010
ι : Sort ?u.98013
ι' : Sort ?u.98016
κ : ι → Sort ?u.98021
κ' : ι' → Sort ?u.98026
inst✝ : CompleteLattice α
f✝ g s t : ι → α
a b✝ : α
b : β
f : (x : β) → b = x → α
⊢ f b (_ : b = b) ≤ f b (_ : b = b)
rfl