-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem zoom_zoomed₁ (e : zoom cut t path = (t', path')) : t'.OnRoot (cut · = .eq) :=
  match t, e with
  | nil, rfl => trivial
  | node .., e => by
    revert e; unfold zoom; split
    · exact zoom_zoomed₁
    · exact zoom_zoomed₁
    · next H => intro e; cases e; exact H

Proof state:
case h_1
α✝ : Type u_1
cut : α✝ → Ordering
t : RBNode α✝
path : Path α✝
t'✝ : RBNode α✝
path'✝ : Path α✝
e : zoom cut t path = (t'✝, path'✝)
path' : Path α✝
t' : RBNode α✝
c✝ : RBColor
l✝ : RBNode α✝
v✝ : α✝
r✝ : RBNode α✝
x✝ : Ordering
heq✝ : cut v✝ = Ordering.lt
⊢ zoom cut l✝ (left c✝ path v✝ r✝) = (t', path') → OnRoot (fun x => cut x = Ordering.eq) t'

Tactic:
exact zoom_zoomed₁

Result:
no goals

Proof state:
α✝ : Type u_1
cut : α✝ → Ordering
t : RBNode α✝
path : Path α✝
t'✝ : RBNode α✝
path'✝ : Path α✝
e : zoom cut t path = (t'✝, path'✝)
path' : Path α✝
t' : RBNode α✝
c✝ : RBColor
l✝ : RBNode α✝
v✝ : α✝
r✝ : RBNode α✝
x✝ : Ordering
H : cut v✝ = Ordering.eq
⊢ (node c✝ l✝ v✝ r✝, path) = (t', path') → OnRoot (fun x => cut x = Ordering.eq) t'

Tactic:
intro e

Result:
α✝ : Type u_1
cut : α✝ → Ordering
t : RBNode α✝
path : Path α✝
t'✝ : RBNode α✝
path'✝ : Path α✝
e✝ : zoom cut t path = (t'✝, path'✝)
path' : Path α✝
t' : RBNode α✝
c✝ : RBColor
l✝ : RBNode α✝
v✝ : α✝
r✝ : RBNode α✝
x✝ : Ordering
H : cut v✝ = Ordering.eq
e : (node c✝ l✝ v✝ r✝, path) = (t', path')
⊢ OnRoot (fun x => cut x = Ordering.eq) t'

Proof state:
α✝ : Type u_1
cut : α✝ → Ordering
t : RBNode α✝
path : Path α✝
t'✝ : RBNode α✝
path'✝ : Path α✝
e✝ : zoom cut t path = (t'✝, path'✝)
path' : Path α✝
t' : RBNode α✝
c✝ : RBColor
l✝ : RBNode α✝
v✝ : α✝
r✝ : RBNode α✝
e : zoom cut (node c✝ l✝ v✝ r✝) path = (t', path')
⊢ OnRoot (fun x => cut x = Ordering.eq) t'

Tactic:
revert e

Result:
α✝ : Type u_1
cut : α✝ → Ordering
t : RBNode α✝
path : Path α✝
t'✝ : RBNode α✝
path'✝ : Path α✝
e : zoom cut t path = (t'✝, path'✝)
path' : Path α✝
t' : RBNode α✝
c✝ : RBColor
l✝ : RBNode α✝
v✝ : α✝
r✝ : RBNode α✝
⊢ zoom cut (node c✝ l✝ v✝ r✝) path = (t', path') → OnRoot (fun x => cut x = Ordering.eq) t'

Proof state:
case h_3
α✝ : Type u_1
cut : α✝ → Ordering
t : RBNode α✝
path : Path α✝
t'✝ : RBNode α✝
path'✝ : Path α✝
e : zoom cut t path = (t'✝, path'✝)
path' : Path α✝
t' : RBNode α✝
c✝ : RBColor
l✝ : RBNode α✝
v✝ : α✝
r✝ : RBNode α✝
x✝ : Ordering
heq✝ : cut v✝ = Ordering.eq
⊢ (node c✝ l✝ v✝ r✝, path) = (t', path') → OnRoot (fun x => cut x = Ordering.eq) t'

Tactic:
next H => intro e; cases e; exact H

Result:
no goals

Proof state:
α✝ : Type u_1
cut : α✝ → Ordering
t : RBNode α✝
path : Path α✝
t'✝ : RBNode α✝
path'✝ : Path α✝
e✝ : zoom cut t path = (t'✝, path'✝)
path' : Path α✝
t' : RBNode α✝
c✝ : RBColor
l✝ : RBNode α✝
v✝ : α✝
r✝ : RBNode α✝
x✝ : Ordering
H : cut v✝ = Ordering.eq
e : (node c✝ l✝ v✝ r✝, path) = (t', path')
⊢ OnRoot (fun x => cut x = Ordering.eq) t'

Tactic:
cases e

Result:
case refl
α✝ : Type u_1
cut : α✝ → Ordering
t : RBNode α✝
path : Path α✝
t' : RBNode α✝
path' : Path α✝
e : zoom cut t path = (t', path')
c✝ : RBColor
l✝ : RBNode α✝
v✝ : α✝
r✝ : RBNode α✝
x✝ : Ordering
H : cut v✝ = Ordering.eq
⊢ OnRoot (fun x => cut x = Ordering.eq) (node c✝ l✝ v✝ r✝)

Proof state:
α✝ : Type u_1
cut : α✝ → Ordering
t : RBNode α✝
path : Path α✝
t'✝ : RBNode α✝
path'✝ : Path α✝
e : zoom cut t path = (t'✝, path'✝)
path' : Path α✝
t' : RBNode α✝
c✝ : RBColor
l✝ : RBNode α✝
v✝ : α✝
r✝ : RBNode α✝
⊢ zoom cut (node c✝ l✝ v✝ r✝) path = (t', path') → OnRoot (fun x => cut x = Ordering.eq) t'

Tactic:
unfold zoom

Result:
α✝ : Type u_1
cut : α✝ → Ordering
t : RBNode α✝
path : Path α✝
t'✝ : RBNode α✝
path'✝ : Path α✝
e : zoom cut t path = (t'✝, path'✝)
path' : Path α✝
t' : RBNode α✝
c✝ : RBColor
l✝ : RBNode α✝
v✝ : α✝
r✝ : RBNode α✝
⊢ (match cut v✝ with
      | Ordering.lt => zoom cut l✝ (left c✝ path v✝ r✝)
      | Ordering.gt => zoom cut r✝ (right c✝ l✝ v✝ path)
      | Ordering.eq => (node c✝ l✝ v✝ r✝, path)) =
      (t', path') →
    OnRoot (fun x => cut x = Ordering.eq) t'

Proof state:
case refl
α✝ : Type u_1
cut : α✝ → Ordering
t : RBNode α✝
path : Path α✝
t' : RBNode α✝
path' : Path α✝
e : zoom cut t path = (t', path')
c✝ : RBColor
l✝ : RBNode α✝
v✝ : α✝
r✝ : RBNode α✝
x✝ : Ordering
H : cut v✝ = Ordering.eq
⊢ OnRoot (fun x => cut x = Ordering.eq) (node c✝ l✝ v✝ r✝)

Tactic:
exact H

Result:
no goals

Proof state:
case h_2
α✝ : Type u_1
cut : α✝ → Ordering
t : RBNode α✝
path : Path α✝
t'✝ : RBNode α✝
path'✝ : Path α✝
e : zoom cut t path = (t'✝, path'✝)
path' : Path α✝
t' : RBNode α✝
c✝ : RBColor
l✝ : RBNode α✝
v✝ : α✝
r✝ : RBNode α✝
x✝ : Ordering
heq✝ : cut v✝ = Ordering.gt
⊢ zoom cut r✝ (right c✝ l✝ v✝ path) = (t', path') → OnRoot (fun x => cut x = Ordering.eq) t'

Tactic:
exact zoom_zoomed₁

Result:
no goals

Proof state:
α✝ : Type u_1
cut : α✝ → Ordering
t : RBNode α✝
path : Path α✝
t'✝ : RBNode α✝
path'✝ : Path α✝
e : zoom cut t path = (t'✝, path'✝)
path' : Path α✝
t' : RBNode α✝
c✝ : RBColor
l✝ : RBNode α✝
v✝ : α✝
r✝ : RBNode α✝
⊢ (match cut v✝ with
      | Ordering.lt => zoom cut l✝ (left c✝ path v✝ r✝)
      | Ordering.gt => zoom cut r✝ (right c✝ l✝ v✝ path)
      | Ordering.eq => (node c✝ l✝ v✝ r✝, path)) =
      (t', path') →
    OnRoot (fun x => cut x = Ordering.eq) t'

Tactic:
split

Result:
case h_1
α✝ : Type u_1
cut : α✝ → Ordering
t : RBNode α✝
path : Path α✝
t'✝ : RBNode α✝
path'✝ : Path α✝
e : zoom cut t path = (t'✝, path'✝)
path' : Path α✝
t' : RBNode α✝
c✝ : RBColor
l✝ : RBNode α✝
v✝ : α✝
r✝ : RBNode α✝
x✝ : Ordering
heq✝ : cut v✝ = Ordering.lt
⊢ zoom cut l✝ (left c✝ path v✝ r✝) = (t', path') → OnRoot (fun x => cut x = Ordering.eq) t'

case h_2
α✝ : Type u_1
cut : α✝ → Ordering
t : RBNode α✝
path : Path α✝
t'✝ : RBNode α✝
path'✝ : Path α✝
e : zoom cut t path = (t'✝, path'✝)
path' : Path α✝
t' : RBNode α✝
c✝ : RBColor
l✝ : RBNode α✝
v✝ : α✝
r✝ : RBNode α✝
x✝ : Ordering
heq✝ : cut v✝ = Ordering.gt
⊢ zoom cut r✝ (right c✝ l✝ v✝ path) = (t', path') → OnRoot (fun x => cut x = Ordering.eq) t'

case h_3
α✝ : Type u_1
cut : α✝ → Ordering
t : RBNode α✝
path : Path α✝
t'✝ : RBNode α✝
path'✝ : Path α✝
e : zoom cut t path = (t'✝, path'✝)
path' : Path α✝
t' : RBNode α✝
c✝ : RBColor
l✝ : RBNode α✝
v✝ : α✝
r✝ : RBNode α✝
x✝ : Ordering
heq✝ : cut v✝ = Ordering.eq
⊢ (node c✝ l✝ v✝ r✝, path) = (t', path') → OnRoot (fun x => cut x = Ordering.eq) t'