-- Mathlib/Order/Partition/Finpartition.lean
theorem card_bind (Q : ∀ i ∈ P.parts, Finpartition i) :
    #(P.bind Q).parts = ∑ A ∈ P.parts.attach, #(Q _ A.2).parts

Proof state:
case h.mk.mk
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a : α
P : Finpartition a
Q : (i : α) → i ∈ P.parts → Finpartition i
b : α
hb : b ∈ P.parts
c : α
hc : c ∈ P.parts
hbc : ⟨b, hb⟩ ≠ ⟨c, hc⟩
⊢ ∀ ⦃a_1 : α⦄, a_1 ∈ (Q ↑⟨b, hb⟩ ⋯).parts → a_1 ∉ (Q ↑⟨c, hc⟩ ⋯).parts

Tactic:
rintro d hdb hdc

Result:
case h.mk.mk
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a : α
P : Finpartition a
Q : (i : α) → i ∈ P.parts → Finpartition i
b : α
hb : b ∈ P.parts
c : α
hc : c ∈ P.parts
hbc : ⟨b, hb⟩ ≠ ⟨c, hc⟩
d : α
hdb : d ∈ (Q ↑⟨b, hb⟩ ⋯).parts
hdc : d ∈ (Q ↑⟨c, hc⟩ ⋯).parts
⊢ False

Proof state:
case h.mk.mk
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a : α
P : Finpartition a
Q : (i : α) → i ∈ P.parts → Finpartition i
b : α
hb : b ∈ P.parts
c : α
hc : c ∈ P.parts
hbc : ¬b = c
d : α
hdb : d ∈ (Q ↑⟨b, hb⟩ ⋯).parts
hdc : d ∈ (Q ↑⟨c, hc⟩ ⋯).parts
⊢ False

Tactic:
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)

Result:
no goals

Proof state:
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a : α
P : Finpartition a
Q : (i : α) → i ∈ P.parts → Finpartition i
⊢ #(P.bind Q).parts = ∑ A ∈ P.parts.attach, #(Q ↑A ⋯).parts

Tactic:
apply card_biUnion

Result:
case h
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a : α
P : Finpartition a
Q : (i : α) → i ∈ P.parts → Finpartition i
⊢ ∀ x ∈ P.parts.attach, ∀ y ∈ P.parts.attach, x ≠ y → Disjoint (Q ↑x ⋯).parts (Q ↑y ⋯).parts

Proof state:
case h.mk.mk
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a : α
P : Finpartition a
Q : (i : α) → i ∈ P.parts → Finpartition i
b : α
hb : b ∈ P.parts
c : α
hc : c ∈ P.parts
hbc : ⟨b, hb⟩ ≠ ⟨c, hc⟩
d : α
hdb : d ∈ (Q ↑⟨b, hb⟩ ⋯).parts
hdc : d ∈ (Q ↑⟨c, hc⟩ ⋯).parts
⊢ False

Tactic:
rw [Ne, Subtype.mk_eq_mk] at hbc

Result:
case h.mk.mk
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a : α
P : Finpartition a
Q : (i : α) → i ∈ P.parts → Finpartition i
b : α
hb : b ∈ P.parts
c : α
hc : c ∈ P.parts
hbc : ¬b = c
d : α
hdb : d ∈ (Q ↑⟨b, hb⟩ ⋯).parts
hdc : d ∈ (Q ↑⟨c, hc⟩ ⋯).parts
⊢ False

Proof state:
case h.mk.mk
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a : α
P : Finpartition a
Q : (i : α) → i ∈ P.parts → Finpartition i
b : α
hb : b ∈ P.parts
c : α
hc : c ∈ P.parts
hbc : ⟨b, hb⟩ ≠ ⟨c, hc⟩
⊢ Disjoint (Q ↑⟨b, hb⟩ ⋯).parts (Q ↑⟨c, hc⟩ ⋯).parts

Tactic:
rw [Finset.disjoint_left]

Result:
case h.mk.mk
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a : α
P : Finpartition a
Q : (i : α) → i ∈ P.parts → Finpartition i
b : α
hb : b ∈ P.parts
c : α
hc : c ∈ P.parts
hbc : ⟨b, hb⟩ ≠ ⟨c, hc⟩
⊢ ∀ ⦃a_1 : α⦄, a_1 ∈ (Q ↑⟨b, hb⟩ ⋯).parts → a_1 ∉ (Q ↑⟨c, hc⟩ ⋯).parts

Proof state:
case h
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a : α
P : Finpartition a
Q : (i : α) → i ∈ P.parts → Finpartition i
⊢ ∀ x ∈ P.parts.attach, ∀ y ∈ P.parts.attach, x ≠ y → Disjoint (Q ↑x ⋯).parts (Q ↑y ⋯).parts

Tactic:
rintro ⟨b, hb⟩ - ⟨c, hc⟩ - hbc

Result:
case h.mk.mk
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a : α
P : Finpartition a
Q : (i : α) → i ∈ P.parts → Finpartition i
b : α
hb : b ∈ P.parts
c : α
hc : c ∈ P.parts
hbc : ⟨b, hb⟩ ≠ ⟨c, hc⟩
⊢ Disjoint (Q ↑⟨b, hb⟩ ⋯).parts (Q ↑⟨c, hc⟩ ⋯).parts