Theorem: Partition.RepFun.rel_of_ne_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
hne : a ≠ b
hab : f a = f b
⊢ P.Rel a b
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
hne : a ≠ b
hab : f a = f b
ha : a ∈ s
⊢ P.Rel a b

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

State before:
case inl
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z a b : α
s : Set α
P : Partition s
f : P.RepFun
hne : a ≠ b
hab : f a = f b
ha : a ∈ s
⊢ P.Rel a b

case inr
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z a b : α
s : Set α
P : Partition s
f : P.RepFun
hne : a ≠ b
hab : f a = f b
ha : a ∉ s
⊢ P.Rel a b
Tactic:
exact f.rel_of_apply_eq_apply ha hab
State after:
case inr
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z a b : α
s : Set α
P : Partition s
f : P.RepFun
hne : a ≠ b
hab : f a = f b
ha : a ∉ s
⊢ P.Rel a b

State before:
case inr
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z a b : α
s : Set α
P : Partition s
f : P.RepFun
hne : a ≠ b
hab : f a = f b
ha : a ∉ s
⊢ P.Rel a b
Tactic:
obtain (hb | hb) := em (b ∈ s)
State after:
case inr.inl
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z a b : α
s : Set α
P : Partition s
f : P.RepFun
hne : a ≠ b
hab : f a = f b
ha : a ∉ s
hb : b ∈ s
⊢ P.Rel a b

case inr.inr
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z a b : α
s : Set α
P : Partition s
f : P.RepFun
hne : a ≠ b
hab : f a = f b
ha : a ∉ s
hb : b ∉ s
⊢ P.Rel a b

State before:
case inr.inl
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z a b : α
s : Set α
P : Partition s
f : P.RepFun
hne : a ≠ b
hab : f a = f b
ha : a ∉ s
hb : b ∈ s
⊢ P.Rel a b

case inr.inr
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z a b : α
s : Set α
P : Partition s
f : P.RepFun
hne : a ≠ b
hab : f a = f b
ha : a ∉ s
hb : b ∉ s
⊢ P.Rel a b
Tactic:
exact (f.rel_of_apply_eq_apply hb hab.symm).symm
State after:
case inr.inr
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z a b : α
s : Set α
P : Partition s
f : P.RepFun
hne : a ≠ b
hab : f a = f b
ha : a ∉ s
hb : b ∉ s
⊢ P.Rel a b

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

State before:
case inr.inr
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z a b : α
s : Set α
P : Partition s
f : P.RepFun
hne : a ≠ b
hab : a = b
ha : a ∉ s
hb : b ∉ s
⊢ P.Rel a b
Tactic:
contradiction
State after:
no goals