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

State before:
α : Type u_1
inst✝ : CompleteLattice α
s✝ x✝ y z a b : α
s : Set α
P : Partition s
f f' : P.RepFun
x : α
⊢ f (f' x) = f x
Tactic:
obtain (hx | hx) := em (x ∈ s)
State after:
case inl
α : Type u_1
inst✝ : CompleteLattice α
s✝ x✝ y z a b : α
s : Set α
P : Partition s
f f' : P.RepFun
x : α
hx : x ∈ s
⊢ f (f' x) = f x

case inr
α : Type u_1
inst✝ : CompleteLattice α
s✝ x✝ y z a b : α
s : Set α
P : Partition s
f f' : P.RepFun
x : α
hx : x ∉ s
⊢ f (f' x) = f x

State before:
case inr
α : Type u_1
inst✝ : CompleteLattice α
s✝ x✝ y z a b : α
s : Set α
P : Partition s
f f' : P.RepFun
x : α
hx : x ∉ s
⊢ f (f' x) = f x
Tactic:
rw [f'.apply_of_not_mem hx, f.apply_of_not_mem hx]
State after:
no goals

State before:
case inl
α : Type u_1
inst✝ : CompleteLattice α
s✝ x✝ y z a b : α
s : Set α
P : Partition s
f f' : P.RepFun
x : α
hx : x ∈ s
⊢ f (f' x) = f x
Tactic:
exact f.apply_eq_apply (f'.rel_apply hx).symm
State after:
no goals