-- Mathlib/Order/Partition/Finpartition.lean
theorem mem_bind : b ∈ (P.bind Q).parts ↔ ∃ A hA, b ∈ (Q A hA).parts

Proof state:
case mpr
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b : α
P : Finpartition a
Q : (i : α) → i ∈ P.parts → Finpartition i
⊢ (∃ A, ∃ (hA : A ∈ P.parts), b ∈ (Q A hA).parts) → ∃ a_2 ∈ P.parts.attach, b ∈ (Q ↑a_2 ⋯).parts

Tactic:
rintro ⟨A, hA, h⟩

Result:
case mpr.intro.intro
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b : α
P : Finpartition a
Q : (i : α) → i ∈ P.parts → Finpartition i
A : α
hA : A ∈ P.parts
h : b ∈ (Q A hA).parts
⊢ ∃ a_1 ∈ P.parts.attach, b ∈ (Q ↑a_1 ⋯).parts

Proof state:
case mp
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b : α
P : Finpartition a
Q : (i : α) → i ∈ P.parts → Finpartition i
⊢ (∃ a_1 ∈ P.parts.attach, b ∈ (Q ↑a_1 ⋯).parts) → ∃ A, ∃ (hA : A ∈ P.parts), b ∈ (Q A hA).parts

Tactic:
rintro ⟨⟨A, hA⟩, -, h⟩

Result:
case mp.intro.mk.intro
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b : α
P : Finpartition a
Q : (i : α) → i ∈ P.parts → Finpartition i
A : α
hA : A ∈ P.parts
h : b ∈ (Q ↑⟨A, hA⟩ ⋯).parts
⊢ ∃ A, ∃ (hA : A ∈ P.parts), b ∈ (Q A hA).parts

Proof state:
case mp.intro.mk.intro
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b : α
P : Finpartition a
Q : (i : α) → i ∈ P.parts → Finpartition i
A : α
hA : A ∈ P.parts
h : b ∈ (Q ↑⟨A, hA⟩ ⋯).parts
⊢ ∃ A, ∃ (hA : A ∈ P.parts), b ∈ (Q A hA).parts

Tactic:
exact ⟨A, hA, h⟩

Result:
no goals

Proof state:
case mpr.intro.intro
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b : α
P : Finpartition a
Q : (i : α) → i ∈ P.parts → Finpartition i
A : α
hA : A ∈ P.parts
h : b ∈ (Q A hA).parts
⊢ ∃ a_1 ∈ P.parts.attach, b ∈ (Q ↑a_1 ⋯).parts

Tactic:
exact ⟨⟨A, hA⟩, mem_attach _ ⟨A, hA⟩, h⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b : α
P : Finpartition a
Q : (i : α) → i ∈ P.parts → Finpartition i
⊢ b ∈ (P.bind Q).parts ↔ ∃ A, ∃ (hA : A ∈ P.parts), b ∈ (Q A hA).parts

Tactic:
rw [bind, mem_biUnion]

Result:
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b : α
P : Finpartition a
Q : (i : α) → i ∈ P.parts → Finpartition i
⊢ (∃ a_1 ∈ P.parts.attach, b ∈ (Q ↑a_1 ⋯).parts) ↔ ∃ A, ∃ (hA : A ∈ P.parts), b ∈ (Q A hA).parts

Proof state:
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b : α
P : Finpartition a
Q : (i : α) → i ∈ P.parts → Finpartition i
⊢ (∃ a_1 ∈ P.parts.attach, b ∈ (Q ↑a_1 ⋯).parts) ↔ ∃ A, ∃ (hA : A ∈ P.parts), b ∈ (Q A hA).parts

Tactic:
constructor

Result:
case mp
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b : α
P : Finpartition a
Q : (i : α) → i ∈ P.parts → Finpartition i
⊢ (∃ a_1 ∈ P.parts.attach, b ∈ (Q ↑a_1 ⋯).parts) → ∃ A, ∃ (hA : A ∈ P.parts), b ∈ (Q A hA).parts

case mpr
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b : α
P : Finpartition a
Q : (i : α) → i ∈ P.parts → Finpartition i
⊢ (∃ A, ∃ (hA : A ∈ P.parts), b ∈ (Q A hA).parts) → ∃ a_2 ∈ P.parts.attach, b ∈ (Q ↑a_2 ⋯).parts