case h
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b c : α
P : Finpartition a
Q✝ Q : (i : α) → i ∈ P.parts → Finpartition i
⊢ ∀ (x : { x // x ∈ P.parts }),
    x ∈ attach P.parts →
      ∀ (y : { x // x ∈ P.parts }),
        y ∈ attach P.parts →
          x ≠ y → Disjoint ((fun i => (Q ↑i (_ : ↑i ∈ P.parts)).parts) x) ((fun i => (Q ↑i (_ : ↑i ∈ P.parts)).parts) y)
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b c : α
P : Finpartition a
Q✝ Q : (i : α) → i ∈ P.parts → Finpartition i
⊢ card (bind P Q).parts = ∑ A in attach P.parts, card (Q ↑A (_ : ↑A ∈ P.parts)).parts
apply card_biUnion
case h.mk.mk
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b✝ c✝ : α
P : Finpartition a
Q✝ Q : (i : α) → i ∈ P.parts → Finpartition i
b : α
hb : b ∈ P.parts
c : α
hc : c ∈ P.parts
hbc : { val := b, property := hb } ≠ { val := c, property := hc }
⊢ Disjoint ((fun i => (Q ↑i (_ : ↑i ∈ P.parts)).parts) { val := b, property := hb })
    ((fun i => (Q ↑i (_ : ↑i ∈ P.parts)).parts) { val := c, property := hc })
case h
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b c : α
P : Finpartition a
Q✝ Q : (i : α) → i ∈ P.parts → Finpartition i
⊢ ∀ (x : { x // x ∈ P.parts }),
    x ∈ attach P.parts →
      ∀ (y : { x // x ∈ P.parts }),
        y ∈ attach P.parts →
          x ≠ y → Disjoint ((fun i => (Q ↑i (_ : ↑i ∈ P.parts)).parts) x) ((fun i => (Q ↑i (_ : ↑i ∈ P.parts)).parts) y)
rintro ⟨b, hb⟩ - ⟨c, hc⟩ - hbc
case h.mk.mk
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b✝ c✝ : α
P : Finpartition a
Q✝ Q : (i : α) → i ∈ P.parts → Finpartition i
b : α
hb : b ∈ P.parts
c : α
hc : c ∈ P.parts
hbc : { val := b, property := hb } ≠ { val := c, property := hc }
⊢ ∀ ⦃a_1 : α⦄,
    a_1 ∈ (fun i => (Q ↑i (_ : ↑i ∈ P.parts)).parts) { val := b, property := hb } →
      ¬a_1 ∈ (fun i => (Q ↑i (_ : ↑i ∈ P.parts)).parts) { val := c, property := hc }
case h.mk.mk
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b✝ c✝ : α
P : Finpartition a
Q✝ Q : (i : α) → i ∈ P.parts → Finpartition i
b : α
hb : b ∈ P.parts
c : α
hc : c ∈ P.parts
hbc : { val := b, property := hb } ≠ { val := c, property := hc }
⊢ Disjoint ((fun i => (Q ↑i (_ : ↑i ∈ P.parts)).parts) { val := b, property := hb })
    ((fun i => (Q ↑i (_ : ↑i ∈ P.parts)).parts) { val := c, property := hc })
rw [Finset.disjoint_left]
case h.mk.mk
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b✝ c✝ : α
P : Finpartition a
Q✝ Q : (i : α) → i ∈ P.parts → Finpartition i
b : α
hb : b ∈ P.parts
c : α
hc : c ∈ P.parts
hbc : { val := b, property := hb } ≠ { val := c, property := hc }
d : α
hdb : d ∈ (fun i => (Q ↑i (_ : ↑i ∈ P.parts)).parts) { val := b, property := hb }
hdc : d ∈ (fun i => (Q ↑i (_ : ↑i ∈ P.parts)).parts) { val := c, property := hc }
⊢ False
case h.mk.mk
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b✝ c✝ : α
P : Finpartition a
Q✝ Q : (i : α) → i ∈ P.parts → Finpartition i
b : α
hb : b ∈ P.parts
c : α
hc : c ∈ P.parts
hbc : { val := b, property := hb } ≠ { val := c, property := hc }
⊢ ∀ ⦃a_1 : α⦄,
    a_1 ∈ (fun i => (Q ↑i (_ : ↑i ∈ P.parts)).parts) { val := b, property := hb } →
      ¬a_1 ∈ (fun i => (Q ↑i (_ : ↑i ∈ P.parts)).parts) { val := c, property := hc }
rintro d hdb hdc
case h.mk.mk
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b✝ c✝ : α
P : Finpartition a
Q✝ Q : (i : α) → i ∈ P.parts → Finpartition i
b : α
hb : b ∈ P.parts
c : α
hc : c ∈ P.parts
hbc : ¬b = c
d : α
hdb : d ∈ (fun i => (Q ↑i (_ : ↑i ∈ P.parts)).parts) { val := b, property := hb }
hdc : d ∈ (fun i => (Q ↑i (_ : ↑i ∈ P.parts)).parts) { val := c, property := hc }
⊢ False
case h.mk.mk
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b✝ c✝ : α
P : Finpartition a
Q✝ Q : (i : α) → i ∈ P.parts → Finpartition i
b : α
hb : b ∈ P.parts
c : α
hc : c ∈ P.parts
hbc : { val := b, property := hb } ≠ { val := c, property := hc }
d : α
hdb : d ∈ (fun i => (Q ↑i (_ : ↑i ∈ P.parts)).parts) { val := b, property := hb }
hdc : d ∈ (fun i => (Q ↑i (_ : ↑i ∈ P.parts)).parts) { val := c, property := hc }
⊢ False
rw [Ne.def, Subtype.mk_eq_mk] at hbc
no goals
case h.mk.mk
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b✝ c✝ : α
P : Finpartition a
Q✝ Q : (i : α) → i ∈ P.parts → Finpartition i
b : α
hb : b ∈ P.parts
c : α
hc : c ∈ P.parts
hbc : ¬b = c
d : α
hdb : d ∈ (fun i => (Q ↑i (_ : ↑i ∈ P.parts)).parts) { val := b, property := hb }
hdc : d ∈ (fun i => (Q ↑i (_ : ↑i ∈ P.parts)).parts) { val := c, property := hc }
⊢ False
exact
  (Q b hb).ne_bot hdb
    (eq_bot_iff.2 <|
      (le_inf ((Q b hb).le hdb) <| (Q c hc).le hdc).trans <| (P.disjoint hb hc hbc).le_bot)