Theorem: Partition.exists_extend_partial_repFun' (Matroid/ForMathlib/SetPartition.lean)

State before:
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z a b : α
s : Set α
P✝ P : Partition s
t : Set α
h : ∀ ⦃x y : α⦄, x ∈ t → y ∈ t → P.Rel x y → x = y
⊢ ∃ f, EqOn (⇑f) id t
Tactic:
simpa using P.exists_extend_partial_repFun (fun x : t ↦ x) (by simp)
  (by simp [P.rel_self_iff_mem]) (fun x y ↦ h x.2 y.2)
State after:
no goals

State before:
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z a b : α
s : Set α
P✝ P : Partition s
t : Set α
h : ∀ ⦃x y : α⦄, x ∈ t → y ∈ t → P.Rel x y → x = y
⊢ ∀ (x : ↑t), ↑x ∉ s → (fun x => ↑x) x = ↑x
Tactic:
simp
State after:
no goals

State before:
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z a b : α
s : Set α
P✝ P : Partition s
t : Set α
h : ∀ ⦃x y : α⦄, x ∈ t → y ∈ t → P.Rel x y → x = y
⊢ ∀ (x : ↑t), ↑x ∈ s → P.Rel (↑x) ((fun x => ↑x) x)
Tactic:
simp [P.rel_self_iff_mem]
State after:
no goals