[GOAL]
α : Type u_1
inst✝ : SemilatticeSup α
s s₁ s₂ t t₁ t₂ u v : Set α
a b c : α
⊢ c ∈ s ⊻ t ↔ ∃ a, a ∈ s ∧ ∃ b, b ∈ t ∧ a ⊔ b = c
[PROOFSTEP]
simp [(· ⊻ ·)]
[GOAL]
α : Type u_1
inst✝ : SemilatticeSup α
s✝ s₁ s₂ t✝ t₁ t₂ u v : Set α
a b c : α
s t : Set α
⊢ image2 (fun x x_1 => x ⊔ x_1) s t = s ⊻ t
[PROOFSTEP]
have : (s ×ˢ t).image (uncurry (· ⊔ ·)) = Set.image2 (fun x x_1 => x ⊔ x_1) s t := by
  simp only [ge_iff_le, image_uncurry_prod]
[GOAL]
α : Type u_1
inst✝ : SemilatticeSup α
s✝ s₁ s₂ t✝ t₁ t₂ u v : Set α
a b c : α
s t : Set α
⊢ (uncurry fun x x_1 => x ⊔ x_1) '' s ×ˢ t = image2 (fun x x_1 => x ⊔ x_1) s t
[PROOFSTEP]
simp only [ge_iff_le, image_uncurry_prod]
[GOAL]
α : Type u_1
inst✝ : SemilatticeSup α
s✝ s₁ s₂ t✝ t₁ t₂ u v : Set α
a b c : α
s t : Set α
this : (uncurry fun x x_1 => x ⊔ x_1) '' s ×ˢ t = image2 (fun x x_1 => x ⊔ x_1) s t
⊢ image2 (fun x x_1 => x ⊔ x_1) s t = s ⊻ t
[PROOFSTEP]
rw [← this]
[GOAL]
α : Type u_1
inst✝ : SemilatticeSup α
s✝ s₁ s₂ t✝ t₁ t₂ u v : Set α
a b c : α
s t : Set α
this : (uncurry fun x x_1 => x ⊔ x_1) '' s ×ˢ t = image2 (fun x x_1 => x ⊔ x_1) s t
⊢ (uncurry fun x x_1 => x ⊔ x_1) '' s ×ˢ t = s ⊻ t
[PROOFSTEP]
exact image_uncurry_prod _ _ _
[GOAL]
α : Type u_1
inst✝ : SemilatticeInf α
s s₁ s₂ t t₁ t₂ u v : Set α
a b c : α
⊢ c ∈ s ⊼ t ↔ ∃ a, a ∈ s ∧ ∃ b, b ∈ t ∧ a ⊓ b = c
[PROOFSTEP]
simp [(· ⊼ ·)]
[GOAL]
α : Type u_1
inst✝ : SemilatticeInf α
s✝ s₁ s₂ t✝ t₁ t₂ u v : Set α
a b c : α
s t : Set α
⊢ image2 (fun x x_1 => x ⊓ x_1) s t = s ⊼ t
[PROOFSTEP]
have : (s ×ˢ t).image (uncurry (· ⊓ ·)) = Set.image2 (fun x x_1 => x ⊓ x_1) s t := by
  simp only [@ge_iff_le, @Set.image_uncurry_prod]
[GOAL]
α : Type u_1
inst✝ : SemilatticeInf α
s✝ s₁ s₂ t✝ t₁ t₂ u v : Set α
a b c : α
s t : Set α
⊢ (uncurry fun x x_1 => x ⊓ x_1) '' s ×ˢ t = image2 (fun x x_1 => x ⊓ x_1) s t
[PROOFSTEP]
simp only [@ge_iff_le, @Set.image_uncurry_prod]
[GOAL]
α : Type u_1
inst✝ : SemilatticeInf α
s✝ s₁ s₂ t✝ t₁ t₂ u v : Set α
a b c : α
s t : Set α
this : (uncurry fun x x_1 => x ⊓ x_1) '' s ×ˢ t = image2 (fun x x_1 => x ⊓ x_1) s t
⊢ image2 (fun x x_1 => x ⊓ x_1) s t = s ⊼ t
[PROOFSTEP]
rw [← this]
[GOAL]
α : Type u_1
inst✝ : SemilatticeInf α
s✝ s₁ s₂ t✝ t₁ t₂ u v : Set α
a b c : α
s t : Set α
this : (uncurry fun x x_1 => x ⊓ x_1) '' s ×ˢ t = image2 (fun x x_1 => x ⊓ x_1) s t
⊢ (uncurry fun x x_1 => x ⊓ x_1) '' s ×ˢ t = s ⊼ t
[PROOFSTEP]
exact image_uncurry_prod _ _ _
[GOAL]
α : Type u_1
inst✝ : SemilatticeSup α
s t : Set α
⊢ upperClosure (s ⊻ t) = upperClosure s ⊔ upperClosure t
[PROOFSTEP]
ext a
[GOAL]
case a.h
α : Type u_1
inst✝ : SemilatticeSup α
s t : Set α
a : α
⊢ a ∈ ↑(upperClosure (s ⊻ t)) ↔ a ∈ ↑(upperClosure s ⊔ upperClosure t)
[PROOFSTEP]
simp only [SetLike.mem_coe, mem_upperClosure, Set.mem_sups, exists_and_left, exists_prop, UpperSet.coe_sup,
  Set.mem_inter_iff]
[GOAL]
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
[PROOFSTEP]
constructor
[GOAL]
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
[PROOFSTEP]
rintro ⟨_, ⟨b, hb, c, hc, rfl⟩, ha⟩
[GOAL]
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
[PROOFSTEP]
exact ⟨⟨b, hb, le_sup_left.trans ha⟩, c, hc, le_sup_right.trans ha⟩
[GOAL]
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
[PROOFSTEP]
rintro ⟨⟨b, hb, hab⟩, c, hc, hac⟩
[GOAL]
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
[PROOFSTEP]
exact ⟨_, ⟨b, hb, c, hc, rfl⟩, sup_le hab hac⟩
[GOAL]
α : Type u_1
inst✝ : SemilatticeInf α
s t : Set α
⊢ lowerClosure (s ⊼ t) = lowerClosure s ⊓ lowerClosure t
[PROOFSTEP]
ext a
[GOAL]
case a.h
α : Type u_1
inst✝ : SemilatticeInf α
s t : Set α
a : α
⊢ a ∈ ↑(lowerClosure (s ⊼ t)) ↔ a ∈ ↑(lowerClosure s ⊓ lowerClosure t)
[PROOFSTEP]
simp only [SetLike.mem_coe, mem_lowerClosure, Set.mem_infs, exists_and_left, exists_prop, LowerSet.coe_sup,
  Set.mem_inter_iff]
[GOAL]
case a.h
α : Type u_1
inst✝ : SemilatticeInf α
s t : Set α
a : α
⊢ (∃ a_1, (∃ a, a ∈ s ∧ ∃ b, b ∈ t ∧ a ⊓ b = a_1) ∧ a ≤ a_1) ↔ a ∈ lowerClosure s ⊓ lowerClosure t
[PROOFSTEP]
constructor
[GOAL]
case a.h.mp
α : Type u_1
inst✝ : SemilatticeInf α
s t : Set α
a : α
⊢ (∃ a_1, (∃ a, a ∈ s ∧ ∃ b, b ∈ t ∧ a ⊓ b = a_1) ∧ a ≤ a_1) → a ∈ lowerClosure s ⊓ lowerClosure t
[PROOFSTEP]
rintro ⟨_, ⟨b, hb, c, hc, rfl⟩, ha⟩
[GOAL]
case a.h.mp.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : SemilatticeInf α
s t : Set α
a b : α
hb : b ∈ s
c : α
hc : c ∈ t
ha : a ≤ b ⊓ c
⊢ a ∈ lowerClosure s ⊓ lowerClosure t
[PROOFSTEP]
exact ⟨⟨b, hb, ha.trans inf_le_left⟩, c, hc, ha.trans inf_le_right⟩
[GOAL]
case a.h.mpr
α : Type u_1
inst✝ : SemilatticeInf α
s t : Set α
a : α
⊢ a ∈ lowerClosure s ⊓ lowerClosure t → ∃ a_2, (∃ a, a ∈ s ∧ ∃ b, b ∈ t ∧ a ⊓ b = a_2) ∧ a ≤ a_2
[PROOFSTEP]
rintro ⟨⟨b, hb, hab⟩, c, hc, hac⟩
[GOAL]
case a.h.mpr.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : SemilatticeInf α
s t : Set α
a b : α
hb : b ∈ s
hab : a ≤ b
c : α
hc : c ∈ t
hac : a ≤ c
⊢ ∃ a_1, (∃ a, a ∈ s ∧ ∃ b, b ∈ t ∧ a ⊓ b = a_1) ∧ a ≤ a_1
[PROOFSTEP]
exact ⟨_, ⟨b, hb, c, hc, rfl⟩, le_inf hab hac⟩
