Theorem: Partition.mem_bind_iff (Matroid/ForMathlib/SetPartition.lean)

State before:
α✝ : Type u_1
inst✝¹ : CompleteLattice α✝
s✝ x y z : α✝
α : Type u_2
inst✝ : CompleteDistribLattice α
s : α
P : Partition s
Qs : (a : α) → a ∈ P → Partition a
a : α
⊢ a ∈ P.bind Qs ↔ ∃ b, ∃ (hb : b ∈ P), a ∈ Qs b hb
Tactic:
change _ ∈ ⋃ _, _ ↔ _
State after:
α✝ : Type u_1
inst✝¹ : CompleteLattice α✝
s✝ x y z : α✝
α : Type u_2
inst✝ : CompleteDistribLattice α
s : α
P : Partition s
Qs : (a : α) → a ∈ P → Partition a
a : α
⊢ a ∈ ⋃ x, ↑(Qs ↑x ⋯) ↔ ∃ b, ∃ (hb : b ∈ P), a ∈ Qs b hb

State before:
α✝ : Type u_1
inst✝¹ : CompleteLattice α✝
s✝ x y z : α✝
α : Type u_2
inst✝ : CompleteDistribLattice α
s : α
P : Partition s
Qs : (a : α) → a ∈ P → Partition a
a : α
⊢ a ∈ ⋃ x, ↑(Qs ↑x ⋯) ↔ ∃ b, ∃ (hb : b ∈ P), a ∈ Qs b hb
Tactic:
simp
State after:
no goals