α : 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
α : 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
rw [← this]
no goals
α : 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
exact image_uncurry_prod _ _ _
no goals
α : 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
simp only [ge_iff_le, image_uncurry_prod]