Theorem: Partition.RepFun.coeFun_eq_id_of_eq_discrete (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
hP : P = Partition.discrete s
⊢ ⇑f = id
Tactic:
subst hP
State after:
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z a b : α
s : Set α
f : (Partition.discrete s).RepFun
⊢ ⇑f = id

State before:
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z a b : α
s : Set α
f : (Partition.discrete s).RepFun
⊢ ⇑f = id
Tactic:
exact repFun_discrete_coeFun s f
State after:
no goals