α : Type u_1
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s s₁ s₂ t t₁ t₂ u : Finset α
a b c : α
⊢ ∀ ⦃x : α⦄, (∃ a, a ∈ s ∧ ∃ b, b ∈ t ∧ Disjoint a b ∧ a ⊔ b = x) → ∃ a, a ∈ s ∧ ∃ b, b ∈ t ∧ a ⊔ b = x
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s s₁ s₂ t t₁ t₂ u : Finset α
a b c : α
⊢ s ○ t ⊆ s ⊻ t
simp_rw [subset_iff, mem_sups, mem_disjSups]
no goals
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s s₁ s₂ t t₁ t₂ u : Finset α
a b c : α
⊢ ∀ ⦃x : α⦄, (∃ a, a ∈ s ∧ ∃ b, b ∈ t ∧ Disjoint a b ∧ a ⊔ b = x) → ∃ a, a ∈ s ∧ ∃ b, b ∈ t ∧ a ⊔ b = x
exact fun c ⟨a, b, ha, hb, _, hc⟩ => ⟨a, b, ha, hb, hc⟩