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

State before:
α : Type u_1
inst✝ : CompleteLattice α
s✝¹ x y z a b : α
s✝ : Set α
P : Partition s✝
s : Set α
f : (Partition.discrete s).RepFun
⊢ ⇑f = id
Tactic:
ext x
State after:
case h
α : Type u_1
inst✝ : CompleteLattice α
s✝¹ x✝ y z a b : α
s✝ : Set α
P : Partition s✝
s : Set α
f : (Partition.discrete s).RepFun
x : α
⊢ f x = id x

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

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

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

State before:
case h.inl
α : Type u_1
inst✝ : CompleteLattice α
s✝¹ x✝ y z a b : α
s✝ : Set α
P : Partition s✝
s : Set α
f : (Partition.discrete s).RepFun
x : α
hx : x ∈ s
⊢ f x = id x
Tactic:
have hx' := f.rel_apply hx
State after:
case h.inl
α : Type u_1
inst✝ : CompleteLattice α
s✝¹ x✝ y z a b : α
s✝ : Set α
P : Partition s✝
s : Set α
f : (Partition.discrete s).RepFun
x : α
hx : x ∈ s
hx' : (Partition.discrete s).Rel x (f x)
⊢ f x = id x

State before:
case h.inl
α : Type u_1
inst✝ : CompleteLattice α
s✝¹ x✝ y z a b : α
s✝ : Set α
P : Partition s✝
s : Set α
f : (Partition.discrete s).RepFun
x : α
hx : x ∈ s
hx' : (Partition.discrete s).Rel x (f x)
⊢ f x = id x
Tactic:
simp only [discrete.rel_iff_eq] at hx'
State after:
case h.inl
α : Type u_1
inst✝ : CompleteLattice α
s✝¹ x✝ y z a b : α
s✝ : Set α
P : Partition s✝
s : Set α
f : (Partition.discrete s).RepFun
x : α
hx : x ∈ s
hx' : x = f x ∧ x ∈ s
⊢ f x = id x

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