case mp
α : Type u
β : Type v
inst✝ : SemilatticeSup α
a b c d : α
⊢ a ≤ b → ∃ c, b = a ⊔ c

case mpr
α : Type u
β : Type v
inst✝ : SemilatticeSup α
a b c d : α
⊢ (∃ c, b = a ⊔ c) → a ≤ b
α : Type u
β : Type v
inst✝ : SemilatticeSup α
a b c d : α
⊢ a ≤ b ↔ ∃ c, b = a ⊔ c
constructor
case mp
α : Type u
β : Type v
inst✝ : SemilatticeSup α
a b c d : α
h : a ≤ b
⊢ ∃ c, b = a ⊔ c
case mp
α : Type u
β : Type v
inst✝ : SemilatticeSup α
a b c d : α
⊢ a ≤ b → ∃ c, b = a ⊔ c
intro h
no goals
case mp
α : Type u
β : Type v
inst✝ : SemilatticeSup α
a b c d : α
h : a ≤ b
⊢ ∃ c, b = a ⊔ c
exact ⟨b, (sup_eq_right.mpr h).symm⟩
case mpr.intro
α : Type u
β : Type v
inst✝ : SemilatticeSup α
a c✝ d c : α
⊢ a ≤ a ⊔ c
case mpr
α : Type u
β : Type v
inst✝ : SemilatticeSup α
a b c d : α
⊢ (∃ c, b = a ⊔ c) → a ≤ b
rintro ⟨c, rfl : _ = _ ⊔ _⟩
no goals
case mpr.intro
α : Type u
β : Type v
inst✝ : SemilatticeSup α
a c✝ d c : α
⊢ a ≤ a ⊔ c
exact le_sup_left