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

State before:
α✝¹ : Type u_1
inst✝² : CompleteLattice α✝¹
s✝¹ x y z : α✝¹
α✝ : Type u_2
inst✝¹ : CompleteDistribLattice α✝
s✝ : α✝
α : Type u_3
inst✝ : CompleteDistribLattice α
s : α
P : Partition s
Qs : (a : α) → a ∈ P → Partition a
⊢ P.bind Qs ≤ P
Tactic:
intro t ht
State after:
α✝¹ : Type u_1
inst✝² : CompleteLattice α✝¹
s✝¹ x y z : α✝¹
α✝ : Type u_2
inst✝¹ : CompleteDistribLattice α✝
s✝ : α✝
α : Type u_3
inst✝ : CompleteDistribLattice α
s : α
P : Partition s
Qs : (a : α) → a ∈ P → Partition a
t : α
ht : t ∈ P.bind Qs
⊢ ∃ y ∈ P, t ≤ y

State before:
α✝¹ : Type u_1
inst✝² : CompleteLattice α✝¹
s✝¹ x y z : α✝¹
α✝ : Type u_2
inst✝¹ : CompleteDistribLattice α✝
s✝ : α✝
α : Type u_3
inst✝ : CompleteDistribLattice α
s : α
P : Partition s
Qs : (a : α) → a ∈ P → Partition a
t : α
ht : t ∈ P.bind Qs
⊢ ∃ y ∈ P, t ≤ y
Tactic:
obtain ⟨b, hbp, h⟩ := mem_bind_iff.1 ht
State after:
case intro.intro
α✝¹ : Type u_1
inst✝² : CompleteLattice α✝¹
s✝¹ x y z : α✝¹
α✝ : Type u_2
inst✝¹ : CompleteDistribLattice α✝
s✝ : α✝
α : Type u_3
inst✝ : CompleteDistribLattice α
s : α
P : Partition s
Qs : (a : α) → a ∈ P → Partition a
t : α
ht : t ∈ P.bind Qs
b : α
hbp : b ∈ P
h : t ∈ Qs b hbp
⊢ ∃ y ∈ P, t ≤ y

State before:
case intro.intro
α✝¹ : Type u_1
inst✝² : CompleteLattice α✝¹
s✝¹ x y z : α✝¹
α✝ : Type u_2
inst✝¹ : CompleteDistribLattice α✝
s✝ : α✝
α : Type u_3
inst✝ : CompleteDistribLattice α
s : α
P : Partition s
Qs : (a : α) → a ∈ P → Partition a
t : α
ht : t ∈ P.bind Qs
b : α
hbp : b ∈ P
h : t ∈ Qs b hbp
⊢ ∃ y ∈ P, t ≤ y
Tactic:
exact ⟨b, hbp, Partition.le_of_mem _ h⟩
State after:
no goals