-- 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' = v ∨ v' ∈ w✝¹ ∨ v' ∈ w✝
⊢ (v' = v✝ ∨ v' ∈ w✝¹ ∨ v' ∈ w✝) ∧ ¬find? (cmp v) t = some v' ∨ v' = v

Tactic:
rcases h with _|h <;> simp [*]

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✝
⊢ ¬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✝
this : List.Pairwise (cmpLT cmp) t.toList
⊢ cmpLT cmp v' v'

Tactic:
simp [h₁, List.pairwise_append] at this

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✝
this :
  List.Pairwise (cmpLT cmp) w✝¹ ∧
    ((∀ (a' : α), a' ∈ w✝ → cmpLT cmp v' a') ∧ List.Pairwise (cmpLT cmp) w✝) ∧
      ∀ (a : α), a ∈ w✝¹ → cmpLT cmp a v' ∧ ∀ (a_2 : α), a_2 ∈ w✝ → cmpLT cmp a a_2
⊢ cmpLT cmp 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
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
p : Path α
e : zoom (cmp v) t = (node c✝ l✝ v✝ r✝, p)
⊢ v' ∈ t ∧ find? (cmp v) t ≠ some v' ∨ v' = v

Tactic:
let ⟨_, _, h₁, h₂⟩ := exists_insert_toList_zoom_node 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
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✝
⊢ 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✝ 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✝
this : cmpLT cmp v' v'
⊢ False

Tactic:
cases OrientedCmp.cmp_refl.symm.trans this.1

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
⊢ v' ∈ insert cmp t v ↔ v' ∈ t ∧ find? (cmp v) t ≠ some v' ∨ v' = v

Tactic:
refine ⟨fun h => ?_, fun | .inl ⟨h₁, h₂⟩ => ?_ | .inr h => ?_⟩

Result:
case refine_1
α : 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
⊢ v' ∈ t ∧ find? (cmp v) t ≠ some v' ∨ v' = v

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

case refine_3
α : 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' = v
⊢ v' ∈ insert cmp t 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✝
⊢ ¬find? (cmp v) t = some v'

Tactic:
rw [find?_eq_zoom, 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
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'

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 : (node c✝ l✝ v✝ r✝, p).fst.root? = some v'
⊢ False

Tactic:
cases h

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✝
⊢ False

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
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✝
⊢ 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
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

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✝
⊢ ¬find? (cmp v) t = some v' ∨ v' = v

Tactic:
refine .inl fun 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 : find? (cmp v) t = some v'
⊢ False