α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b c : α
P : Finpartition a
Q : (i : α) → i ∈ P.parts → Finpartition i
⊢ (∃ a_1, a_1 ∈ attach P.parts ∧ b ∈ (Q ↑a_1 (_ : ↑a_1 ∈ P.parts)).parts) ↔ ∃ A hA, b ∈ (Q A hA).parts
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b c : α
P : Finpartition a
Q : (i : α) → i ∈ P.parts → Finpartition i
⊢ b ∈ (bind P Q).parts ↔ ∃ A hA, b ∈ (Q A hA).parts
rw [bind, mem_biUnion]
case mp
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b c : α
P : Finpartition a
Q : (i : α) → i ∈ P.parts → Finpartition i
⊢ (∃ a_1, a_1 ∈ attach P.parts ∧ b ∈ (Q ↑a_1 (_ : ↑a_1 ∈ P.parts)).parts) → ∃ A hA, b ∈ (Q A hA).parts

case mpr
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b c : α
P : Finpartition a
Q : (i : α) → i ∈ P.parts → Finpartition i
⊢ (∃ A hA, b ∈ (Q A hA).parts) → ∃ a_2, a_2 ∈ attach P.parts ∧ b ∈ (Q ↑a_2 (_ : ↑a_2 ∈ P.parts)).parts
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b c : α
P : Finpartition a
Q : (i : α) → i ∈ P.parts → Finpartition i
⊢ (∃ a_1, a_1 ∈ attach P.parts ∧ b ∈ (Q ↑a_1 (_ : ↑a_1 ∈ P.parts)).parts) ↔ ∃ A hA, b ∈ (Q A hA).parts
constructor
case mp.intro.mk.intro
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b c : α
P : Finpartition a
Q : (i : α) → i ∈ P.parts → Finpartition i
A : α
hA : A ∈ P.parts
h : b ∈ (Q ↑{ val := A, property := hA } (_ : ↑{ val := A, property := hA } ∈ P.parts)).parts
⊢ ∃ A hA, b ∈ (Q A hA).parts
case mp
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b c : α
P : Finpartition a
Q : (i : α) → i ∈ P.parts → Finpartition i
⊢ (∃ a_1, a_1 ∈ attach P.parts ∧ b ∈ (Q ↑a_1 (_ : ↑a_1 ∈ P.parts)).parts) → ∃ A hA, b ∈ (Q A hA).parts
rintro ⟨⟨A, hA⟩, -, h⟩
no goals
case mp.intro.mk.intro
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b c : α
P : Finpartition a
Q : (i : α) → i ∈ P.parts → Finpartition i
A : α
hA : A ∈ P.parts
h : b ∈ (Q ↑{ val := A, property := hA } (_ : ↑{ val := A, property := hA } ∈ P.parts)).parts
⊢ ∃ A hA, b ∈ (Q A hA).parts
exact ⟨A, hA, h⟩
case mpr.intro.intro
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b c : α
P : Finpartition a
Q : (i : α) → i ∈ P.parts → Finpartition i
A : α
hA : A ∈ P.parts
h : b ∈ (Q A hA).parts
⊢ ∃ a_1, a_1 ∈ attach P.parts ∧ b ∈ (Q ↑a_1 (_ : ↑a_1 ∈ P.parts)).parts
case mpr
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b c : α
P : Finpartition a
Q : (i : α) → i ∈ P.parts → Finpartition i
⊢ (∃ A hA, b ∈ (Q A hA).parts) → ∃ a_2, a_2 ∈ attach P.parts ∧ b ∈ (Q ↑a_2 (_ : ↑a_2 ∈ P.parts)).parts
rintro ⟨A, hA, h⟩
no goals
case mpr.intro.intro
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b c : α
P : Finpartition a
Q : (i : α) → i ∈ P.parts → Finpartition i
A : α
hA : A ∈ P.parts
h : b ∈ (Q A hA).parts
⊢ ∃ a_1, a_1 ∈ attach P.parts ∧ b ∈ (Q ↑a_1 (_ : ↑a_1 ∈ P.parts)).parts
exact ⟨⟨A, hA⟩, mem_attach _ ⟨A, hA⟩, h⟩