Theorem: Partition.RepFun.image_subset_self (Matroid/ForMathlib/SetPartition.lean)

State before:
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z a b : α
s : Set α
P : Partition s
f : P.RepFun
⊢ ⇑f '' s ⊆ s
Tactic:
rintro _ ⟨a,ha,rfl⟩
State after:
case intro.intro
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z a✝ b : α
s : Set α
P : Partition s
f : P.RepFun
a : α
ha : a ∈ s
⊢ f a ∈ s

State before:
case intro.intro
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z a✝ b : α
s : Set α
P : Partition s
f : P.RepFun
a : α
ha : a ∈ s
⊢ f a ∈ s
Tactic:
exact f.apply_mem ha
State after:
no goals