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

State before:
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z a b : α
s : Set α
P✝ P : Partition s
⊢ Nonempty P.RepFun
Tactic:
obtain ⟨f, -⟩ := P.exists_extend_partial_repFun' (t := ∅) (by simp)
State after:
case intro
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z a b : α
s : Set α
P✝ P : Partition s
f : P.RepFun
⊢ Nonempty P.RepFun

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

State before:
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z a b : α
s : Set α
P✝ P : Partition s
⊢ ∀ ⦃x y : α⦄, x ∈ ∅ → y ∈ ∅ → P.Rel x y → x = y
Tactic:
simp
State after:
no goals