Theorem: Partition.RepFun.idem (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
a : α
⊢ f (f a) = f a
Tactic:
obtain (ha | ha) := em (a ∈ s)
State after:
case inl
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z a✝ b : α
s : Set α
P : Partition s
f : P.RepFun
a : α
ha : a ∈ s
⊢ f (f a) = f a

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

State before:
case inr
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z a✝ b : α
s : Set α
P : Partition s
f : P.RepFun
a : α
ha : a ∉ s
⊢ f (f a) = f a
Tactic:
simp_rw [f.apply_of_not_mem ha]
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 : P.RepFun
a : α
ha : a ∈ s
⊢ f (f a) = f a
Tactic:
rw [eq_comm, f.apply_eq_apply_iff_rel ha]
State after:
case inl
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z a✝ b : α
s : Set α
P : Partition s
f : P.RepFun
a : α
ha : a ∈ s
⊢ P.Rel a (f a)

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