-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Alter.lean
theorem zoom_zoomed₂ (e : zoom cut t path = (t', path'))
    (hp : path.Zoomed cut) : path'.Zoomed cut :=
  match t, e with
  | nil, rfl => hp
  | node .., e => by
    revert e; unfold zoom; split
    · next h => exact fun e => zoom_zoomed₂ e ⟨h, hp⟩
    · next h => exact fun e => zoom_zoomed₂ e ⟨h, hp⟩
    · intro e; cases e; exact hp

Proof state:
α✝ : Type u_1
cut : α✝ → Ordering
t : RBNode α✝
path : Path α✝
t'✝ : RBNode α✝
path'✝ : Path α✝
e✝ : zoom cut t path = (t'✝, path'✝)
hp : Zoomed cut path
path' : Path α✝
t' : RBNode α✝
c✝ : RBColor
l✝ : RBNode α✝
v✝ : α✝
r✝ : RBNode α✝
e : zoom cut (node c✝ l✝ v✝ r✝) path = (t', path')
⊢ Zoomed cut path'

Tactic:
revert e

Result:
α✝ : Type u_1
cut : α✝ → Ordering
t : RBNode α✝
path : Path α✝
t'✝ : RBNode α✝
path'✝ : Path α✝
e : zoom cut t path = (t'✝, path'✝)
hp : Zoomed cut path
path' : Path α✝
t' : RBNode α✝
c✝ : RBColor
l✝ : RBNode α✝
v✝ : α✝
r✝ : RBNode α✝
⊢ zoom cut (node c✝ l✝ v✝ r✝) path = (t', path') → Zoomed cut path'

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'✝)
hp : Zoomed cut 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') → Zoomed cut path'

Tactic:
next h => exact fun e => zoom_zoomed₂ e ⟨h, hp⟩

Result:
no goals

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

Tactic:
exact hp

Result:
no goals

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'✝)
hp : Zoomed cut path
path' : Path α✝
t' : RBNode α✝
c✝ : RBColor
l✝ : RBNode α✝
v✝ : α✝
r✝ : RBNode α✝
x✝ : Ordering
heq✝ : cut v✝ = Ordering.eq
e : (node c✝ l✝ v✝ r✝, path) = (t', path')
⊢ Zoomed cut path'

Tactic:
cases e

Result:
case h_3.refl
α✝ : Type u_1
cut : α✝ → Ordering
t : RBNode α✝
path : Path α✝
t' : RBNode α✝
path' : Path α✝
e : zoom cut t path = (t', path')
hp : Zoomed cut path
c✝ : RBColor
l✝ : RBNode α✝
v✝ : α✝
r✝ : RBNode α✝
x✝ : Ordering
heq✝ : cut v✝ = Ordering.eq
⊢ Zoomed cut path

Proof state:
α✝ : Type u_1
cut : α✝ → Ordering
t : RBNode α✝
path : Path α✝
t'✝ : RBNode α✝
path'✝ : Path α✝
e : zoom cut t path = (t'✝, path'✝)
hp : Zoomed cut 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') →
    Zoomed cut path'

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'✝)
hp : Zoomed cut 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') → Zoomed cut path'

case h_2
α✝ : Type u_1
cut : α✝ → Ordering
t : RBNode α✝
path : Path α✝
t'✝ : RBNode α✝
path'✝ : Path α✝
e : zoom cut t path = (t'✝, path'✝)
hp : Zoomed cut 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') → Zoomed cut path'

case h_3
α✝ : Type u_1
cut : α✝ → Ordering
t : RBNode α✝
path : Path α✝
t'✝ : RBNode α✝
path'✝ : Path α✝
e : zoom cut t path = (t'✝, path'✝)
hp : Zoomed cut 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') → Zoomed cut path'

Proof state:
α✝ : Type u_1
cut : α✝ → Ordering
t : RBNode α✝
path : Path α✝
t'✝ : RBNode α✝
path'✝ : Path α✝
e : zoom cut t path = (t'✝, path'✝)
hp : Zoomed cut path
path' : Path α✝
t' : RBNode α✝
c✝ : RBColor
l✝ : RBNode α✝
v✝ : α✝
r✝ : RBNode α✝
x✝ : Ordering
h : cut v✝ = Ordering.gt
⊢ zoom cut r✝ (right c✝ l✝ v✝ path) = (t', path') → Zoomed cut path'

Tactic:
exact fun e => zoom_zoomed₂ e ⟨h, hp⟩

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'✝)
hp : Zoomed cut path
path' : Path α✝
t' : RBNode α✝
c✝ : RBColor
l✝ : RBNode α✝
v✝ : α✝
r✝ : RBNode α✝
⊢ zoom cut (node c✝ l✝ v✝ r✝) path = (t', path') → Zoomed cut path'

Tactic:
unfold zoom

Result:
α✝ : Type u_1
cut : α✝ → Ordering
t : RBNode α✝
path : Path α✝
t'✝ : RBNode α✝
path'✝ : Path α✝
e : zoom cut t path = (t'✝, path'✝)
hp : Zoomed cut 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') →
    Zoomed cut path'

Proof state:
α✝ : Type u_1
cut : α✝ → Ordering
t : RBNode α✝
path : Path α✝
t'✝ : RBNode α✝
path'✝ : Path α✝
e : zoom cut t path = (t'✝, path'✝)
hp : Zoomed cut path
path' : Path α✝
t' : RBNode α✝
c✝ : RBColor
l✝ : RBNode α✝
v✝ : α✝
r✝ : RBNode α✝
x✝ : Ordering
h : cut v✝ = Ordering.lt
⊢ zoom cut l✝ (left c✝ path v✝ r✝) = (t', path') → Zoomed cut path'

Tactic:
exact fun e => zoom_zoomed₂ e ⟨h, hp⟩

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'✝)
hp : Zoomed cut 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') → Zoomed cut path'

Tactic:
next h => exact fun e => zoom_zoomed₂ e ⟨h, hp⟩

Result:
no goals

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'✝)
hp : Zoomed cut 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') → Zoomed cut path'

Tactic:
intro e

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