Theorem: Std.RBSet.findP?_insert_of_ne (Etch/Verification/RBMap.lean)

State before:
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
v : α
inst✝¹ : TransCmp cmp
inst✝ : IsStrictCut cmp cut
t : RBSet α cmp
h : cut v ≠ Ordering.eq
⊢ findP? (insert t v) cut = findP? t cut
Tactic:
refine Option.ext fun u =>
  findP?_some.trans <| .trans (and_congr_left fun h' => ?_) findP?_some.symm
State after:
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
v : α
inst✝¹ : TransCmp cmp
inst✝ : IsStrictCut cmp cut
t : RBSet α cmp
h : cut v ≠ Ordering.eq
u : α
h' : cut u = Ordering.eq
⊢ u ∈ toList (insert t v) ↔ u ∈ toList t

State before:
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
v : α
inst✝¹ : TransCmp cmp
inst✝ : IsStrictCut cmp cut
t : RBSet α cmp
h : cut v ≠ Ordering.eq
u : α
h' : cut u = Ordering.eq
⊢ u ∈ toList (insert t v) ↔ u ∈ toList t
Tactic:
rw [mem_toList_insert, or_iff_left, and_iff_left]
State after:
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
v : α
inst✝¹ : TransCmp cmp
inst✝ : IsStrictCut cmp cut
t : RBSet α cmp
h : cut v ≠ Ordering.eq
u : α
h' : cut u = Ordering.eq
⊢ find? t v ≠ some u

α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
v : α
inst✝¹ : TransCmp cmp
inst✝ : IsStrictCut cmp cut
t : RBSet α cmp
h : cut v ≠ Ordering.eq
u : α
h' : cut u = Ordering.eq
⊢ ¬u = v

State before:
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
v : α
inst✝¹ : TransCmp cmp
inst✝ : IsStrictCut cmp cut
t : RBSet α cmp
h : cut v ≠ Ordering.eq
u : α
h' : cut u = Ordering.eq
⊢ find? t v ≠ some u
Tactic:
exact mt (fun h => by rwa [IsCut.congr (cut := cut) (find?_some_eq_eq h)]) h
State after:
no goals

State before:
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
v : α
inst✝¹ : TransCmp cmp
inst✝ : IsStrictCut cmp cut
t : RBSet α cmp
h✝ : cut v ≠ Ordering.eq
u : α
h' : cut u = Ordering.eq
h : find? t v = some u
⊢ cut v = Ordering.eq
Tactic:
rwa [IsCut.congr (cut := cut) (find?_some_eq_eq h)]
State after:
no goals

State before:
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
v : α
inst✝¹ : TransCmp cmp
inst✝ : IsStrictCut cmp cut
t : RBSet α cmp
h : cut v ≠ Ordering.eq
u : α
h' : cut u = Ordering.eq
⊢ ¬u = v
Tactic:
rintro rfl
State after:
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
inst✝¹ : TransCmp cmp
inst✝ : IsStrictCut cmp cut
t : RBSet α cmp
u : α
h' : cut u = Ordering.eq
h : cut u ≠ Ordering.eq
⊢ False

State before:
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
inst✝¹ : TransCmp cmp
inst✝ : IsStrictCut cmp cut
t : RBSet α cmp
u : α
h' : cut u = Ordering.eq
h : cut u ≠ Ordering.eq
⊢ False
Tactic:
contradiction
State after:
no goals