case a.h
α : Type u_1
inst✝ : SemilatticeSup α
s t : Set α
a : α
⊢ a ∈ ↑(upperClosure (s ⊻ t)) ↔ a ∈ ↑(upperClosure s ⊔ upperClosure t)
α : Type u_1
inst✝ : SemilatticeSup α
s t : Set α
⊢ upperClosure (s ⊻ t) = upperClosure s ⊔ upperClosure t
ext a
case a.h
α : Type u_1
inst✝ : SemilatticeSup α
s t : Set α
a : α
⊢ (∃ a_1, (∃ a, a ∈ s ∧ ∃ b, b ∈ t ∧ a ⊔ b = a_1) ∧ a_1 ≤ a) ↔ (∃ a_1, a_1 ∈ s ∧ a_1 ≤ a) ∧ ∃ a_1, a_1 ∈ t ∧ a_1 ≤ a
case a.h
α : Type u_1
inst✝ : SemilatticeSup α
s t : Set α
a : α
⊢ a ∈ ↑(upperClosure (s ⊻ t)) ↔ a ∈ ↑(upperClosure s ⊔ upperClosure t)
simp only [SetLike.mem_coe, mem_upperClosure, Set.mem_sups, exists_and_left, exists_prop,
  UpperSet.coe_sup, Set.mem_inter_iff]
case a.h.mp
α : Type u_1
inst✝ : SemilatticeSup α
s t : Set α
a : α
⊢ (∃ a_1, (∃ a, a ∈ s ∧ ∃ b, b ∈ t ∧ a ⊔ b = a_1) ∧ a_1 ≤ a) → (∃ a_2, a_2 ∈ s ∧ a_2 ≤ a) ∧ ∃ a_2, a_2 ∈ t ∧ a_2 ≤ a

case a.h.mpr
α : Type u_1
inst✝ : SemilatticeSup α
s t : Set α
a : α
⊢ ((∃ a_1, a_1 ∈ s ∧ a_1 ≤ a) ∧ ∃ a_1, a_1 ∈ t ∧ a_1 ≤ a) → ∃ a_2, (∃ a, a ∈ s ∧ ∃ b, b ∈ t ∧ a ⊔ b = a_2) ∧ a_2 ≤ a
case a.h
α : Type u_1
inst✝ : SemilatticeSup α
s t : Set α
a : α
⊢ (∃ a_1, (∃ a, a ∈ s ∧ ∃ b, b ∈ t ∧ a ⊔ b = a_1) ∧ a_1 ≤ a) ↔ (∃ a_1, a_1 ∈ s ∧ a_1 ≤ a) ∧ ∃ a_1, a_1 ∈ t ∧ a_1 ≤ a
constructor
case a.h.mp.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : SemilatticeSup α
s t : Set α
a b : α
hb : b ∈ s
c : α
hc : c ∈ t
ha : b ⊔ c ≤ a
⊢ (∃ a_1, a_1 ∈ s ∧ a_1 ≤ a) ∧ ∃ a_1, a_1 ∈ t ∧ a_1 ≤ a
case a.h.mp
α : Type u_1
inst✝ : SemilatticeSup α
s t : Set α
a : α
⊢ (∃ a_1, (∃ a, a ∈ s ∧ ∃ b, b ∈ t ∧ a ⊔ b = a_1) ∧ a_1 ≤ a) → (∃ a_2, a_2 ∈ s ∧ a_2 ≤ a) ∧ ∃ a_2, a_2 ∈ t ∧ a_2 ≤ a
rintro ⟨_, ⟨b, hb, c, hc, rfl⟩, ha⟩
no goals
case a.h.mp.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : SemilatticeSup α
s t : Set α
a b : α
hb : b ∈ s
c : α
hc : c ∈ t
ha : b ⊔ c ≤ a
⊢ (∃ a_1, a_1 ∈ s ∧ a_1 ≤ a) ∧ ∃ a_1, a_1 ∈ t ∧ a_1 ≤ a
exact ⟨⟨b, hb, le_sup_left.trans ha⟩, c, hc, le_sup_right.trans ha⟩
case a.h.mpr.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : SemilatticeSup α
s t : Set α
a b : α
hb : b ∈ s
hab : b ≤ a
c : α
hc : c ∈ t
hac : c ≤ a
⊢ ∃ a_1, (∃ a, a ∈ s ∧ ∃ b, b ∈ t ∧ a ⊔ b = a_1) ∧ a_1 ≤ a
case a.h.mpr
α : Type u_1
inst✝ : SemilatticeSup α
s t : Set α
a : α
⊢ ((∃ a_1, a_1 ∈ s ∧ a_1 ≤ a) ∧ ∃ a_1, a_1 ∈ t ∧ a_1 ≤ a) → ∃ a_2, (∃ a, a ∈ s ∧ ∃ b, b ∈ t ∧ a ⊔ b = a_2) ∧ a_2 ≤ a
rintro ⟨⟨b, hb, hab⟩, c, hc, hac⟩
no goals
case a.h.mpr.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : SemilatticeSup α
s t : Set α
a b : α
hb : b ∈ s
hab : b ≤ a
c : α
hc : c ∈ t
hac : c ≤ a
⊢ ∃ a_1, (∃ a, a ∈ s ∧ ∃ b, b ∈ t ∧ a ⊔ b = a_1) ∧ a_1 ≤ a
exact ⟨_, ⟨b, hb, c, hc, rfl⟩, sup_le hab hac⟩