[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : SemilatticeSup α
s s₁ s₂ t t₁ t₂ u v : Finset α
a b c : α
⊢ c ∈ s ⊻ t ↔ ∃ a, a ∈ s ∧ ∃ b, b ∈ t ∧ a ⊔ b = c
[PROOFSTEP]
simp [(· ⊻ ·)]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : SemilatticeInf α
s s₁ s₂ t t₁ t₂ u v : Finset α
a b c : α
⊢ c ∈ s ⊼ t ↔ ∃ a, a ∈ s ∧ ∃ b, b ∈ t ∧ a ⊓ b = c
[PROOFSTEP]
simp [(· ⊼ ·)]
[GOAL]
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s s₁ s₂ t t₁ t₂ u : Finset α
a b c : α
⊢ c ∈ s ○ t ↔ ∃ a, a ∈ s ∧ ∃ b, b ∈ t ∧ Disjoint a b ∧ a ⊔ b = c
[PROOFSTEP]
simp [disjSups, and_assoc]
[GOAL]
α : 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
[PROOFSTEP]
simp_rw [subset_iff, mem_sups, mem_disjSups]
[GOAL]
α : 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
[PROOFSTEP]
exact fun c ⟨a, b, ha, hb, _, hc⟩ => ⟨a, b, ha, hb, hc⟩
[GOAL]
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s s₁ s₂ t t₁ t₂ u : Finset α
a b c : α
p : α → Prop
⊢ (∀ (c : α), c ∈ s ○ t → p c) ↔ ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → Disjoint a b → p (a ⊔ b)
[PROOFSTEP]
simp_rw [mem_disjSups]
[GOAL]
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s s₁ s₂ t t₁ t₂ u : Finset α
a b c : α
p : α → Prop
⊢ (∀ (c : α), (∃ a, a ∈ s ∧ ∃ b, b ∈ t ∧ Disjoint a b ∧ a ⊔ b = c) → p c) ↔
    ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → Disjoint a b → p (a ⊔ b)
[PROOFSTEP]
refine' ⟨fun h a ha b hb hab => h _ ⟨_, ha, _, hb, hab, rfl⟩, _⟩
[GOAL]
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s s₁ s₂ t t₁ t₂ u : Finset α
a b c : α
p : α → Prop
⊢ (∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → Disjoint a b → p (a ⊔ b)) →
    ∀ (c : α), (∃ a, a ∈ s ∧ ∃ b, b ∈ t ∧ Disjoint a b ∧ a ⊔ b = c) → p c
[PROOFSTEP]
rintro h _ ⟨a, ha, b, hb, hab, rfl⟩
[GOAL]
case intro.intro.intro.intro.intro
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s s₁ s₂ t t₁ t₂ u : Finset α
a✝ b✝ c : α
p : α → Prop
h : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → Disjoint a b → p (a ⊔ b)
a : α
ha : a ∈ s
b : α
hb : b ∈ t
hab : Disjoint a b
⊢ p (a ⊔ b)
[PROOFSTEP]
exact h _ ha _ hb hab
[GOAL]
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s s₁ s₂ t t₁ t₂ u : Finset α
a b c : α
⊢ Finset.Nonempty (s ○ t) → Finset.Nonempty s
[PROOFSTEP]
simp_rw [Finset.Nonempty, mem_disjSups]
[GOAL]
α : 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) → ∃ x, x ∈ s
[PROOFSTEP]
exact fun ⟨_, a, ha, _⟩ => ⟨a, ha⟩
[GOAL]
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s s₁ s₂ t t₁ t₂ u : Finset α
a b c : α
⊢ Finset.Nonempty (s ○ t) → Finset.Nonempty t
[PROOFSTEP]
simp_rw [Finset.Nonempty, mem_disjSups]
[GOAL]
α : 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) → ∃ x, x ∈ t
[PROOFSTEP]
exact fun ⟨_, _, _, b, hb, _⟩ => ⟨b, hb⟩
[GOAL]
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s s₁ s₂ t t₁ t₂ u : Finset α
a b c : α
⊢ ∅ ○ t = ∅
[PROOFSTEP]
simp [disjSups]
[GOAL]
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s s₁ s₂ t t₁ t₂ u : Finset α
a b c : α
⊢ s ○ ∅ = ∅
[PROOFSTEP]
simp [disjSups]
[GOAL]
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s s₁ s₂ t t₁ t₂ u : Finset α
a b c : α
⊢ {a} ○ {b} = if Disjoint a b then {a ⊔ b} else ∅
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s s₁ s₂ t t₁ t₂ u : Finset α
a b c : α
h : Disjoint a b
⊢ {a} ○ {b} = {a ⊔ b}
[PROOFSTEP]
simp [disjSups, filter_singleton, h]
[GOAL]
case neg
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s s₁ s₂ t t₁ t₂ u : Finset α
a b c : α
h : ¬Disjoint a b
⊢ {a} ○ {b} = ∅
[PROOFSTEP]
simp [disjSups, filter_singleton, h]
[GOAL]
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s s₁ s₂ t t₁ t₂ u : Finset α
a b c : α
⊢ (s₁ ∪ s₂) ○ t = s₁ ○ t ∪ s₂ ○ t
[PROOFSTEP]
simp [disjSups, filter_union, image_union]
[GOAL]
α : 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₁ ∪ t₂) = s ○ t₁ ∪ s ○ t₂
[PROOFSTEP]
simp [disjSups, filter_union, image_union]
[GOAL]
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s s₁ s₂ t t₁ t₂ u : Finset α
a b c : α
⊢ (s₁ ∩ s₂) ○ t ⊆ s₁ ○ t ∩ s₂ ○ t
[PROOFSTEP]
simpa only [disjSups, inter_product, filter_inter_distrib] using image_inter_subset _ _ _
[GOAL]
α : 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₁ ∩ t₂) ⊆ s ○ t₁ ∩ s ○ t₂
[PROOFSTEP]
simpa only [disjSups, product_inter, filter_inter_distrib] using image_inter_subset _ _ _
[GOAL]
α : 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 = t ○ s
[PROOFSTEP]
ext
[GOAL]
case a
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s s₁ s₂ t t₁ t₂ u : Finset α
a b c a✝ : α
⊢ a✝ ∈ s ○ t ↔ a✝ ∈ t ○ s
[PROOFSTEP]
rw [mem_disjSups, mem_disjSups]
  -- Porting note: `exists₂_comm` no longer works with `∃ _ ∈ _, ∃ _ ∈ _, _`
[GOAL]
case a
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s s₁ s₂ t t₁ t₂ u : Finset α
a b c a✝ : α
⊢ (∃ a, a ∈ s ∧ ∃ b, b ∈ t ∧ Disjoint a b ∧ a ⊔ b = a✝) ↔ ∃ a, a ∈ t ∧ ∃ b, b ∈ s ∧ Disjoint a b ∧ a ⊔ b = a✝
[PROOFSTEP]
constructor
[GOAL]
case a.mp
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s s₁ s₂ t t₁ t₂ u : Finset α
a b c a✝ : α
⊢ (∃ a, a ∈ s ∧ ∃ b, b ∈ t ∧ Disjoint a b ∧ a ⊔ b = a✝) → ∃ a, a ∈ t ∧ ∃ b, b ∈ s ∧ Disjoint a b ∧ a ⊔ b = a✝
[PROOFSTEP]
rintro ⟨a, ha, b, hb, hd, hs⟩
[GOAL]
case a.mp.intro.intro.intro.intro.intro
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s s₁ s₂ t t₁ t₂ u : Finset α
a✝¹ b✝ c a✝ a : α
ha : a ∈ s
b : α
hb : b ∈ t
hd : Disjoint a b
hs : a ⊔ b = a✝
⊢ ∃ a, a ∈ t ∧ ∃ b, b ∈ s ∧ Disjoint a b ∧ a ⊔ b = a✝
[PROOFSTEP]
rw [disjoint_comm] at hd 
[GOAL]
case a.mp.intro.intro.intro.intro.intro
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s s₁ s₂ t t₁ t₂ u : Finset α
a✝¹ b✝ c a✝ a : α
ha : a ∈ s
b : α
hb : b ∈ t
hd : Disjoint b a
hs : a ⊔ b = a✝
⊢ ∃ a, a ∈ t ∧ ∃ b, b ∈ s ∧ Disjoint a b ∧ a ⊔ b = a✝
[PROOFSTEP]
rw [sup_comm] at hs 
[GOAL]
case a.mp.intro.intro.intro.intro.intro
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s s₁ s₂ t t₁ t₂ u : Finset α
a✝¹ b✝ c a✝ a : α
ha : a ∈ s
b : α
hb : b ∈ t
hd : Disjoint b a
hs : b ⊔ a = a✝
⊢ ∃ a, a ∈ t ∧ ∃ b, b ∈ s ∧ Disjoint a b ∧ a ⊔ b = a✝
[PROOFSTEP]
exact ⟨b, hb, a, ha, hd, hs⟩
[GOAL]
case a.mpr
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s s₁ s₂ t t₁ t₂ u : Finset α
a b c a✝ : α
⊢ (∃ a, a ∈ t ∧ ∃ b, b ∈ s ∧ Disjoint a b ∧ a ⊔ b = a✝) → ∃ a, a ∈ s ∧ ∃ b, b ∈ t ∧ Disjoint a b ∧ a ⊔ b = a✝
[PROOFSTEP]
rintro ⟨a, ha, b, hb, hd, hs⟩
[GOAL]
case a.mpr.intro.intro.intro.intro.intro
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s s₁ s₂ t t₁ t₂ u : Finset α
a✝¹ b✝ c a✝ a : α
ha : a ∈ t
b : α
hb : b ∈ s
hd : Disjoint a b
hs : a ⊔ b = a✝
⊢ ∃ a, a ∈ s ∧ ∃ b, b ∈ t ∧ Disjoint a b ∧ a ⊔ b = a✝
[PROOFSTEP]
rw [disjoint_comm] at hd 
[GOAL]
case a.mpr.intro.intro.intro.intro.intro
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s s₁ s₂ t t₁ t₂ u : Finset α
a✝¹ b✝ c a✝ a : α
ha : a ∈ t
b : α
hb : b ∈ s
hd : Disjoint b a
hs : a ⊔ b = a✝
⊢ ∃ a, a ∈ s ∧ ∃ b, b ∈ t ∧ Disjoint a b ∧ a ⊔ b = a✝
[PROOFSTEP]
rw [sup_comm] at hs 
[GOAL]
case a.mpr.intro.intro.intro.intro.intro
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s s₁ s₂ t t₁ t₂ u : Finset α
a✝¹ b✝ c a✝ a : α
ha : a ∈ t
b : α
hb : b ∈ s
hd : Disjoint b a
hs : b ⊔ a = a✝
⊢ ∃ a, a ∈ s ∧ ∃ b, b ∈ t ∧ Disjoint a b ∧ a ⊔ b = a✝
[PROOFSTEP]
exact ⟨b, hb, a, ha, hd, hs⟩
[GOAL]
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s t u v : Finset α
⊢ ∀ (s t u : Finset α), s ○ t ○ u = s ○ (t ○ u)
[PROOFSTEP]
refine' associative_of_commutative_of_le disjSups_comm _
[GOAL]
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s t u v : Finset α
⊢ ∀ (a b c : Finset α), a ○ b ○ c ≤ a ○ (b ○ c)
[PROOFSTEP]
simp only [le_eq_subset, disjSups_subset_iff, mem_disjSups]
[GOAL]
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s t u v : Finset α
⊢ ∀ (a b c : Finset α) (a_1 : α),
    (∃ a_2, a_2 ∈ a ∧ ∃ b_1, b_1 ∈ b ∧ Disjoint a_2 b_1 ∧ a_2 ⊔ b_1 = a_1) →
      ∀ (b_1 : α),
        b_1 ∈ c →
          Disjoint a_1 b_1 →
            ∃ a_5,
              a_5 ∈ a ∧
                ∃ b_2, (∃ a, a ∈ b ∧ ∃ b, b ∈ c ∧ Disjoint a b ∧ a ⊔ b = b_2) ∧ Disjoint a_5 b_2 ∧ a_5 ⊔ b_2 = a_1 ⊔ b_1
[PROOFSTEP]
rintro s t u _ ⟨a, ha, b, hb, hab, rfl⟩ c hc habc
[GOAL]
case intro.intro.intro.intro.intro
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s✝ t✝ u✝ v s t u : Finset α
a : α
ha : a ∈ s
b : α
hb : b ∈ t
hab : Disjoint a b
c : α
hc : c ∈ u
habc : Disjoint (a ⊔ b) c
⊢ ∃ a_1,
    a_1 ∈ s ∧ ∃ b_1, (∃ a, a ∈ t ∧ ∃ b, b ∈ u ∧ Disjoint a b ∧ a ⊔ b = b_1) ∧ Disjoint a_1 b_1 ∧ a_1 ⊔ b_1 = a ⊔ b ⊔ c
[PROOFSTEP]
rw [disjoint_sup_left] at habc 
[GOAL]
case intro.intro.intro.intro.intro
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s✝ t✝ u✝ v s t u : Finset α
a : α
ha : a ∈ s
b : α
hb : b ∈ t
hab : Disjoint a b
c : α
hc : c ∈ u
habc : Disjoint a c ∧ Disjoint b c
⊢ ∃ a_1,
    a_1 ∈ s ∧ ∃ b_1, (∃ a, a ∈ t ∧ ∃ b, b ∈ u ∧ Disjoint a b ∧ a ⊔ b = b_1) ∧ Disjoint a_1 b_1 ∧ a_1 ⊔ b_1 = a ⊔ b ⊔ c
[PROOFSTEP]
exact ⟨a, ha, _, ⟨b, hb, c, hc, habc.2, rfl⟩, hab.sup_right habc.1, sup_assoc.symm⟩
[GOAL]
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s t u v : Finset α
⊢ s ○ (t ○ u) = t ○ (s ○ u)
[PROOFSTEP]
simp_rw [← disjSups_assoc, disjSups_comm s]
[GOAL]
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s t u v : Finset α
⊢ s ○ t ○ u = s ○ u ○ t
[PROOFSTEP]
simp_rw [disjSups_assoc, disjSups_comm]
[GOAL]
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s t u v : Finset α
⊢ s ○ t ○ (u ○ v) = s ○ u ○ (t ○ v)
[PROOFSTEP]
simp_rw [← disjSups_assoc, disjSups_right_comm]
