α : 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)
α : 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)
refine' associative_of_commutative_of_le disjSups_comm _
α : 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
α : 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)
simp only [le_eq_subset, disjSups_subset_iff, mem_disjSups]
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
α : 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
rintro s t u _ ⟨a, ha, b, hb, hab, rfl⟩ c hc habc
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
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
rw [disjoint_sup_left] at habc
no goals
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
exact ⟨a, ha, _, ⟨b, hb, c, hc, habc.2, rfl⟩, hab.sup_right habc.1, sup_assoc.symm⟩