-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem mem_insert [@TransCmp α cmp] {t : RBNode α} (ht : Balanced t c n) (ht₂ : Ordered cmp t) :
    v' ∈ t.insert cmp v ↔ (v' ∈ t ∧ t.find? (cmp v) ≠ some v') ∨ v' = v

Proof state:
α : Type u_1
cmp : α → α → Ordering
c : RBColor
n : Nat
v v' : α
inst✝ : TransCmp cmp
t : RBNode α
ht : t.Balanced c n
ht₂ : Ordered cmp t
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
p : Path α
e : zoom (cmp v) t = (node c✝ l✝ v✝ r✝, p)
w✝¹ w✝ : List α
h₁ : t.toList = w✝¹ ++ v✝ :: w✝
h₂ : (insert cmp t v).toList = w✝¹ ++ v :: w✝
h : v' ∈ w✝¹ ∨ v' = v ∨ v' ∈ w✝
⊢ v' ∈ t ∧ find? (cmp v) t ≠ some v' ∨ v' = v

Tactic:
simp [← mem_toList, h₁]

Result:
α : Type u_1
cmp : α → α → Ordering
c : RBColor
n : Nat
v v' : α
inst✝ : TransCmp cmp
t : RBNode α
ht : t.Balanced c n
ht₂ : Ordered cmp t
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
p : Path α
e : zoom (cmp v) t = (node c✝ l✝ v✝ r✝, p)
w✝¹ w✝ : List α
h₁ : t.toList = w✝¹ ++ v✝ :: w✝
h₂ : (insert cmp t v).toList = w✝¹ ++ v :: w✝
h : v' ∈ w✝¹ ∨ v' = v ∨ v' ∈ w✝
⊢ (v' ∈ w✝¹ ∨ v' = v✝ ∨ v' ∈ w✝) ∧ ¬find? (cmp v) t = some v' ∨ v' = v

Proof state:
α : Type u_1
cmp : α → α → Ordering
c : RBColor
n : Nat
v v' : α
inst✝ : TransCmp cmp
t : RBNode α
ht : t.Balanced c n
ht₂ : Ordered cmp t
p : Path α
e : zoom (cmp v) t = (nil, p)
w✝¹ w✝ : List α
h₁ : t.toList = w✝¹ ++ w✝
h₂ : (insert cmp t v).toList = w✝¹ ++ v :: w✝
h : (v' ∈ w✝¹ ∨ v' ∈ w✝) ∨ v' = v
⊢ v' ∈ t ∧ find? (cmp v) t ≠ some v' ∨ v' = v

Tactic:
refine h.imp_left fun h => ?_

Result:
α : Type u_1
cmp : α → α → Ordering
c : RBColor
n : Nat
v v' : α
inst✝ : TransCmp cmp
t : RBNode α
ht : t.Balanced c n
ht₂ : Ordered cmp t
p : Path α
e : zoom (cmp v) t = (nil, p)
w✝¹ w✝ : List α
h₁ : t.toList = w✝¹ ++ w✝
h₂ : (insert cmp t v).toList = w✝¹ ++ v :: w✝
h✝ : (v' ∈ w✝¹ ∨ v' ∈ w✝) ∨ v' = v
h : v' ∈ w✝¹ ∨ v' ∈ w✝
⊢ v' ∈ t ∧ find? (cmp v) t ≠ some v'

Proof state:
α : Type u_1
cmp : α → α → Ordering
c : RBColor
n : Nat
v v' : α
inst✝ : TransCmp cmp
t : RBNode α
ht : t.Balanced c n
ht₂ : Ordered cmp t
p : Path α
e : zoom (cmp v) t = (nil, p)
w✝¹ w✝ : List α
h₁ : t.toList = w✝¹ ++ w✝
h₂ : (insert cmp t v).toList = w✝¹ ++ v :: w✝
h✝ : (v' ∈ w✝¹ ∨ v' ∈ w✝) ∨ v' = v
h : v' ∈ w✝¹ ∨ v' ∈ w✝
⊢ ¬(nil, p).fst.root? = some v'

Tactic:
nofun

Result:
no goals

Proof state:
α : Type u_1
cmp : α → α → Ordering
c : RBColor
n : Nat
v v' : α
inst✝ : TransCmp cmp
t : RBNode α
ht : t.Balanced c n
ht₂ : Ordered cmp t
h : v' ∈ insert cmp t v
p : Path α
e : zoom (cmp v) t = (nil, p)
⊢ v' ∈ t ∧ find? (cmp v) t ≠ some v' ∨ v' = v

Tactic:
let ⟨_, _, h₁, h₂⟩ := exists_insert_toList_zoom_nil ht e

Result:
α : Type u_1
cmp : α → α → Ordering
c : RBColor
n : Nat
v v' : α
inst✝ : TransCmp cmp
t : RBNode α
ht : t.Balanced c n
ht₂ : Ordered cmp t
h : v' ∈ insert cmp t v
p : Path α
e : zoom (cmp v) t = (nil, p)
w✝¹ w✝ : List α
h₁ : t.toList = w✝¹ ++ w✝
h₂ : (insert cmp t v).toList = w✝¹ ++ v :: w✝
⊢ v' ∈ t ∧ find? (cmp v) t ≠ some v' ∨ v' = v

Proof state:
α : Type u_1
cmp : α → α → Ordering
c : RBColor
n : Nat
v v' : α
inst✝ : TransCmp cmp
t : RBNode α
ht : t.Balanced c n
ht₂ : Ordered cmp t
h : v' ∈ insert cmp t v
p : Path α
e : zoom (cmp v) t = (nil, p)
w✝¹ w✝ : List α
h₁ : t.toList = w✝¹ ++ w✝
h₂ : (insert cmp t v).toList = w✝¹ ++ v :: w✝
⊢ v' ∈ t ∧ find? (cmp v) t ≠ some v' ∨ v' = v

Tactic:
simp [← mem_toList, h₂] at h

Result:
α : Type u_1
cmp : α → α → Ordering
c : RBColor
n : Nat
v v' : α
inst✝ : TransCmp cmp
t : RBNode α
ht : t.Balanced c n
ht₂ : Ordered cmp t
p : Path α
e : zoom (cmp v) t = (nil, p)
w✝¹ w✝ : List α
h₁ : t.toList = w✝¹ ++ w✝
h₂ : (insert cmp t v).toList = w✝¹ ++ v :: w✝
h : v' ∈ w✝¹ ∨ v' = v ∨ v' ∈ w✝
⊢ v' ∈ t ∧ find? (cmp v) t ≠ some v' ∨ v' = v

Proof state:
α : Type u_1
cmp : α → α → Ordering
c : RBColor
n : Nat
v v' : α
inst✝ : TransCmp cmp
t : RBNode α
ht : t.Balanced c n
ht₂ : Ordered cmp t
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
p : Path α
e : zoom (cmp v) t = (node c✝ l✝ v✝ r✝, p)
w✝¹ w✝ : List α
h₁ : t.toList = w✝¹ ++ v✝ :: w✝
h₂ : (insert cmp t v).toList = w✝¹ ++ v :: w✝
h : v' ∈ w✝¹ ∨ v' = v ∨ v' ∈ w✝
⊢ (v' ∈ w✝¹ ∨ v' = v✝ ∨ v' ∈ w✝) ∧ ¬find? (cmp v) t = some v' ∨ v' = v

Tactic:
rw [or_left_comm] at h ⊢

Result:
α : Type u_1
cmp : α → α → Ordering
c : RBColor
n : Nat
v v' : α
inst✝ : TransCmp cmp
t : RBNode α
ht : t.Balanced c n
ht₂ : Ordered cmp t
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
p : Path α
e : zoom (cmp v) t = (node c✝ l✝ v✝ r✝, p)
w✝¹ w✝ : List α
h₁ : t.toList = w✝¹ ++ v✝ :: w✝
h₂ : (insert cmp t v).toList = w✝¹ ++ v :: w✝
h : v' = v ∨ v' ∈ w✝¹ ∨ v' ∈ w✝
⊢ (v' = v✝ ∨ v' ∈ w✝¹ ∨ v' ∈ w✝) ∧ ¬find? (cmp v) t = some v' ∨ v' = v

Proof state:
case inr.refl
α : Type u_1
cmp : α → α → Ordering
c : RBColor
n : Nat
v v' : α
inst✝ : TransCmp cmp
t : RBNode α
ht : t.Balanced c n
ht₂ : Ordered cmp t
c✝ : RBColor
l✝ r✝ : RBNode α
p : Path α
w✝¹ w✝ : List α
h₂ : (insert cmp t v).toList = w✝¹ ++ v :: w✝
h : v' ∈ w✝¹ ∨ v' ∈ w✝
e : zoom (cmp v) t = (node c✝ l✝ v' r✝, p)
h₁ : t.toList = w✝¹ ++ v' :: w✝
⊢ False

Tactic:
suffices cmpLT cmp v' v' by cases OrientedCmp.cmp_refl.symm.trans this.1

Result:
case inr.refl
α : Type u_1
cmp : α → α → Ordering
c : RBColor
n : Nat
v v' : α
inst✝ : TransCmp cmp
t : RBNode α
ht : t.Balanced c n
ht₂ : Ordered cmp t
c✝ : RBColor
l✝ r✝ : RBNode α
p : Path α
w✝¹ w✝ : List α
h₂ : (insert cmp t v).toList = w✝¹ ++ v :: w✝
h : v' ∈ w✝¹ ∨ v' ∈ w✝
e : zoom (cmp v) t = (node c✝ l✝ v' r✝, p)
h₁ : t.toList = w✝¹ ++ v' :: w✝
⊢ cmpLT cmp v' v'

Proof state:
case refine_2
α : Type u_1
cmp : α → α → Ordering
c : RBColor
n : Nat
v v' : α
inst✝ : TransCmp cmp
t : RBNode α
ht : t.Balanced c n
ht₂ : Ordered cmp t
h₁ : v' ∈ t
h₂ : find? (cmp v) t ≠ some v'
⊢ v' ∈ insert cmp t v

Tactic:
exact (mem_insert_of_mem ht h₁).resolve_right fun h' => h₂ <| ht₂.find?_some.2 ⟨h₁, h'⟩

Result:
no goals

Proof state:
α : Type u_1
cmp : α → α → Ordering
c : RBColor
n : Nat
v v' : α
inst✝ : TransCmp cmp
t : RBNode α
ht : t.Balanced c n
ht₂ : Ordered cmp t
p : Path α
e : zoom (cmp v) t = (nil, p)
w✝¹ w✝ : List α
h₁ : t.toList = w✝¹ ++ w✝
h₂ : (insert cmp t v).toList = w✝¹ ++ v :: w✝
h : v' ∈ w✝¹ ∨ v' = v ∨ v' ∈ w✝
⊢ v' ∈ t ∧ find? (cmp v) t ≠ some v' ∨ v' = v

Tactic:
rw [← or_assoc, or_right_comm] at h

Result:
α : Type u_1
cmp : α → α → Ordering
c : RBColor
n : Nat
v v' : α
inst✝ : TransCmp cmp
t : RBNode α
ht : t.Balanced c n
ht₂ : Ordered cmp t
p : Path α
e : zoom (cmp v) t = (nil, p)
w✝¹ w✝ : List α
h₁ : t.toList = w✝¹ ++ w✝
h₂ : (insert cmp t v).toList = w✝¹ ++ v :: w✝
h : (v' ∈ w✝¹ ∨ v' ∈ w✝) ∨ v' = v
⊢ v' ∈ t ∧ find? (cmp v) t ≠ some v' ∨ v' = v

Proof state:
case inr
α : Type u_1
cmp : α → α → Ordering
c : RBColor
n : Nat
v v' : α
inst✝ : TransCmp cmp
t : RBNode α
ht : t.Balanced c n
ht₂ : Ordered cmp t
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
p : Path α
e : zoom (cmp v) t = (node c✝ l✝ v✝ r✝, p)
w✝¹ w✝ : List α
h₁ : t.toList = w✝¹ ++ v✝ :: w✝
h₂ : (insert cmp t v).toList = w✝¹ ++ v :: w✝
h✝ : v' ∈ w✝¹ ∨ v' ∈ w✝
h : find? (cmp v) t = some v'
⊢ False

Tactic:
rw [find?_eq_zoom, e] at h

Result:
case inr
α : Type u_1
cmp : α → α → Ordering
c : RBColor
n : Nat
v v' : α
inst✝ : TransCmp cmp
t : RBNode α
ht : t.Balanced c n
ht₂ : Ordered cmp t
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
p : Path α
e : zoom (cmp v) t = (node c✝ l✝ v✝ r✝, p)
w✝¹ w✝ : List α
h₁ : t.toList = w✝¹ ++ v✝ :: w✝
h₂ : (insert cmp t v).toList = w✝¹ ++ v :: w✝
h✝ : v' ∈ w✝¹ ∨ v' ∈ w✝
h : (node c✝ l✝ v✝ r✝, p).fst.root? = some v'
⊢ False