-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem mem_insert_of_mem {t : RBNode α} (ht : Balanced t c n) (h : v' ∈ t) :
    v' ∈ t.insert cmp v ∨ cmp v v' = .eq

Proof state:
α : Type u_1
c : RBColor
n : Nat
v' : α
cmp : α → α → Ordering
v : α
t : RBNode α
ht : t.Balanced c n
h : v' ∈ t
⊢ v' ∈ insert cmp t v ∨ cmp v v' = Ordering.eq

Tactic:
match e : zoom (cmp v) t with
| (nil, p) =>
  let ⟨_, _, h₁, h₂⟩ := exists_insert_toList_zoom_nil ht e
  simp [← mem_toList, h₁] at h
  simp [← mem_toList, h₂]; cases h <;> simp [*]
| (node .., p) =>
  let ⟨_, _, h₁, h₂⟩ := exists_insert_toList_zoom_node ht e
  simp [← mem_toList, h₁] at h
  simp [← mem_toList, h₂]; rcases h with h|h|h <;> simp [*]
  exact .inr (Path.zoom_zoomed₁ e)

Result:
no goals

Proof state:
α : Type u_1
c : RBColor
n : Nat
v' : α
cmp : α → α → Ordering
v : α
t : RBNode α
ht : t.Balanced c n
h : v' ∈ 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✝
⊢ v' ∈ insert cmp t v ∨ cmp v v' = Ordering.eq

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

Result:
α : Type u_1
c : RBColor
n : Nat
v' : α
cmp : α → α → Ordering
v : α
t : RBNode α
ht : t.Balanced c n
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' ∈ insert cmp t v ∨ cmp v v' = Ordering.eq

Proof state:
α : Type u_1
c : RBColor
n : Nat
v' : α
cmp : α → α → Ordering
v : α
t : RBNode α
ht : t.Balanced c n
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✝) ∨ cmp v v' = Ordering.eq

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

Result:
case inr.inl
α : Type u_1
c : RBColor
n : Nat
v' : α
cmp : α → α → Ordering
v : α
t : RBNode α
ht : t.Balanced c n
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✝ = v ∨ v✝ ∈ w✝) ∨ cmp v v✝ = Ordering.eq

Proof state:
α : Type u_1
c : RBColor
n : Nat
v' : α
cmp : α → α → Ordering
v : α
t : RBNode α
ht : t.Balanced c n
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' ∈ insert cmp t v ∨ cmp v v' = Ordering.eq

Tactic:
simp [← mem_toList, h₂]

Result:
α : Type u_1
c : RBColor
n : Nat
v' : α
cmp : α → α → Ordering
v : α
t : RBNode α
ht : t.Balanced c n
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' ∈ w✝¹ ∨ v' = v ∨ v' ∈ w✝) ∨ cmp v v' = Ordering.eq

Proof state:
α : Type u_1
c : RBColor
n : Nat
v' : α
cmp : α → α → Ordering
v : α
t : RBNode α
ht : t.Balanced c n
h : v' ∈ t
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
p : Path α
e : zoom (cmp v) t = (node c✝ l✝ v✝ r✝, p)
⊢ v' ∈ insert cmp t v ∨ cmp v v' = Ordering.eq

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

Result:
α : Type u_1
c : RBColor
n : Nat
v' : α
cmp : α → α → Ordering
v : α
t : RBNode α
ht : t.Balanced c n
h : v' ∈ 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✝
⊢ v' ∈ insert cmp t v ∨ cmp v v' = Ordering.eq

Proof state:
α : Type u_1
c : RBColor
n : Nat
v' : α
cmp : α → α → Ordering
v : α
t : RBNode α
ht : t.Balanced c n
h : v' ∈ 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✝
⊢ v' ∈ insert cmp t v ∨ cmp v v' = Ordering.eq

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

Result:
α : Type u_1
c : RBColor
n : Nat
v' : α
cmp : α → α → Ordering
v : α
t : RBNode α
ht : t.Balanced c n
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' ∈ insert cmp t v ∨ cmp v v' = Ordering.eq

Proof state:
α : Type u_1
c : RBColor
n : Nat
v' : α
cmp : α → α → Ordering
v : α
t : RBNode α
ht : t.Balanced c n
h : v' ∈ t
p : Path α
e : zoom (cmp v) t = (nil, p)
⊢ v' ∈ insert cmp t v ∨ cmp v v' = Ordering.eq

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

Result:
α : Type u_1
c : RBColor
n : Nat
v' : α
cmp : α → α → Ordering
v : α
t : RBNode α
ht : t.Balanced c n
h : v' ∈ 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✝
⊢ v' ∈ insert cmp t v ∨ cmp v v' = Ordering.eq

Proof state:
α : Type u_1
c : RBColor
n : Nat
v' : α
cmp : α → α → Ordering
v : α
t : RBNode α
ht : t.Balanced c n
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' ∈ insert cmp t v ∨ cmp v v' = Ordering.eq

Tactic:
simp [← mem_toList, h₂]

Result:
α : Type u_1
c : RBColor
n : Nat
v' : α
cmp : α → α → Ordering
v : α
t : RBNode α
ht : t.Balanced c n
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✝) ∨ cmp v v' = Ordering.eq

Proof state:
α : Type u_1
c : RBColor
n : Nat
v' : α
cmp : α → α → Ordering
v : α
t : RBNode α
ht : t.Balanced c n
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' ∈ w✝¹ ∨ v' = v ∨ v' ∈ w✝) ∨ cmp v v' = Ordering.eq

Tactic:
cases h <;> simp [*]

Result:
no goals

Proof state:
case inr.inl
α : Type u_1
c : RBColor
n : Nat
v' : α
cmp : α → α → Ordering
v : α
t : RBNode α
ht : t.Balanced c n
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✝ = v ∨ v✝ ∈ w✝) ∨ cmp v v✝ = Ordering.eq

Tactic:
exact .inr (Path.zoom_zoomed₁ e)

Result:
no goals