Theorem: Partition.RepFun.rel_of_apply_eq_apply (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
ha : a ∈ s
hab : f a = f b
⊢ P.Rel a b
Tactic:
refine (f.rel_apply ha).trans ?_
State after:
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z a b : α
s : Set α
P : Partition s
f : P.RepFun
ha : a ∈ s
hab : f a = f b
⊢ P.Rel (f a) b

State before:
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z a b : α
s : Set α
P : Partition s
f : P.RepFun
ha : a ∈ s
hab : f a = f b
⊢ P.Rel (f a) b
Tactic:
rw [hab, P.rel_comm]
State after:
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z a b : α
s : Set α
P : Partition s
f : P.RepFun
ha : a ∈ s
hab : f a = f b
⊢ P.Rel b (f b)

State before:
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z a b : α
s : Set α
P : Partition s
f : P.RepFun
ha : a ∈ s
hab : f a = f b
⊢ P.Rel b (f b)
Tactic:
refine f.rel_apply <| by_contra fun hb ↦ ?_
State after:
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z a b : α
s : Set α
P : Partition s
f : P.RepFun
ha : a ∈ s
hab : f a = f b
hb : b ∉ s
⊢ False

State before:
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z a b : α
s : Set α
P : Partition s
f : P.RepFun
ha : a ∈ s
hab : f a = f b
hb : b ∉ s
⊢ False
Tactic:
rw [f.apply_of_not_mem hb] at hab
State after:
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z a b : α
s : Set α
P : Partition s
f : P.RepFun
ha : a ∈ s
hab : f a = b
hb : b ∉ s
⊢ False

State before:
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z a b : α
s : Set α
P : Partition s
f : P.RepFun
ha : a ∈ s
hab : f a = b
hb : b ∉ s
⊢ False
Tactic:
rw [← hab] at hb
State after:
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z a b : α
s : Set α
P : Partition s
f : P.RepFun
ha : a ∈ s
hab : f a = b
hb : f a ∉ s
⊢ False

State before:
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z a b : α
s : Set α
P : Partition s
f : P.RepFun
ha : a ∈ s
hab : f a = b
hb : f a ∉ s
⊢ False
Tactic:
exact hb <| f.apply_mem ha
State after:
no goals