-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Alter.lean
theorem _root_.Batteries.RBNode.Balanced.zoom : t.Balanced c n → path.Balanced c₀ n₀ c n →
    zoom cut t path = (t', path') → ∃ c n, t'.Balanced c n ∧ path'.Balanced c₀ n₀ c n
  | .nil, hp => fun e => by cases e; exact ⟨_, _, .nil, hp⟩
  | .red ha hb, hp => by
    unfold zoom; split
    · exact ha.zoom (.redL hb hp)
    · exact hb.zoom (.redR ha hp)
    · intro e; cases e; exact ⟨_, _, .red ha hb, hp⟩
  | .black ha hb, hp => by
    unfold zoom; split
    · exact ha.zoom (.blackL hb hp)
    · exact hb.zoom (.blackR ha hp)
    · intro e; cases e; exact ⟨_, _, .black ha hb, hp⟩

Proof state:
case h_3.refl
α✝ : Type u_1
cut : α✝ → Ordering
t : RBNode α✝
path : Path α✝
c₀ : RBColor
n₀ : Nat
c : RBColor
n✝ n : Nat
x✝¹ y✝ : RBNode α✝
v✝ : α✝
ha : x✝¹.Balanced black n
hb : y✝.Balanced black n
hp : Path.Balanced c₀ n₀ path red n
x✝ : Ordering
heq✝ : cut v✝ = Ordering.eq
⊢ ∃ c n, (node red x✝¹ v✝ y✝).Balanced c n ∧ Path.Balanced c₀ n₀ path c n

Tactic:
exact ⟨_, _, .red ha hb, hp⟩

Result:
no goals

Proof state:
α✝ : Type u_1
cut : α✝ → Ordering
t : RBNode α✝
path : Path α✝
t' : RBNode α✝
path' : Path α✝
c₀ : RBColor
n₀ : Nat
c : RBColor
n✝ n : Nat
x✝ y✝ : RBNode α✝
v✝ : α✝
ha : x✝.Balanced black n
hb : y✝.Balanced black n
hp : Path.Balanced c₀ n₀ path red n
⊢ zoom cut (node red x✝ v✝ y✝) path = (t', path') → ∃ c n, t'.Balanced c n ∧ Path.Balanced c₀ n₀ path' c n

Tactic:
unfold zoom

Result:
α✝ : Type u_1
cut : α✝ → Ordering
t : RBNode α✝
path : Path α✝
t' : RBNode α✝
path' : Path α✝
c₀ : RBColor
n₀ : Nat
c : RBColor
n✝ n : Nat
x✝ y✝ : RBNode α✝
v✝ : α✝
ha : x✝.Balanced black n
hb : y✝.Balanced black n
hp : Path.Balanced c₀ n₀ path red n
⊢ (match cut v✝ with
      | Ordering.lt => zoom cut x✝ (left red path v✝ y✝)
      | Ordering.gt => zoom cut y✝ (right red x✝ v✝ path)
      | Ordering.eq => (node red x✝ v✝ y✝, path)) =
      (t', path') →
    ∃ c n, t'.Balanced c n ∧ Path.Balanced c₀ n₀ path' c n

Proof state:
α✝ : Type u_1
cut : α✝ → Ordering
t : RBNode α✝
path : Path α✝
t' : RBNode α✝
path' : Path α✝
c₀ : RBColor
n₀ : Nat
c : RBColor
n : Nat
x✝ : RBNode α✝
c₁✝ : RBColor
n✝ : Nat
y✝ : RBNode α✝
c₂✝ : RBColor
v✝ : α✝
ha : x✝.Balanced c₁✝ n✝
hb : y✝.Balanced c₂✝ n✝
hp : Path.Balanced c₀ n₀ path black (n✝ + 1)
⊢ zoom cut (node black x✝ v✝ y✝) path = (t', path') → ∃ c n, t'.Balanced c n ∧ Path.Balanced c₀ n₀ path' c n

Tactic:
unfold zoom

Result:
α✝ : Type u_1
cut : α✝ → Ordering
t : RBNode α✝
path : Path α✝
t' : RBNode α✝
path' : Path α✝
c₀ : RBColor
n₀ : Nat
c : RBColor
n : Nat
x✝ : RBNode α✝
c₁✝ : RBColor
n✝ : Nat
y✝ : RBNode α✝
c₂✝ : RBColor
v✝ : α✝
ha : x✝.Balanced c₁✝ n✝
hb : y✝.Balanced c₂✝ n✝
hp : Path.Balanced c₀ n₀ path black (n✝ + 1)
⊢ (match cut v✝ with
      | Ordering.lt => zoom cut x✝ (left black path v✝ y✝)
      | Ordering.gt => zoom cut y✝ (right black x✝ v✝ path)
      | Ordering.eq => (node black x✝ v✝ y✝, path)) =
      (t', path') →
    ∃ c n, t'.Balanced c n ∧ Path.Balanced c₀ n₀ path' c n

Proof state:
case refl
α✝ : Type u_1
cut : α✝ → Ordering
t : RBNode α✝
path : Path α✝
c₀ : RBColor
n₀ : Nat
c : RBColor
n : Nat
hp : Path.Balanced c₀ n₀ path black 0
⊢ ∃ c n, nil.Balanced c n ∧ Path.Balanced c₀ n₀ path c n

Tactic:
exact ⟨_, _, .nil, hp⟩

Result:
no goals

Proof state:
case h_1
α✝ : Type u_1
cut : α✝ → Ordering
t : RBNode α✝
path : Path α✝
t' : RBNode α✝
path' : Path α✝
c₀ : RBColor
n₀ : Nat
c : RBColor
n✝ n : Nat
x✝¹ y✝ : RBNode α✝
v✝ : α✝
ha : x✝¹.Balanced black n
hb : y✝.Balanced black n
hp : Path.Balanced c₀ n₀ path red n
x✝ : Ordering
heq✝ : cut v✝ = Ordering.lt
⊢ zoom cut x✝¹ (left red path v✝ y✝) = (t', path') → ∃ c n, t'.Balanced c n ∧ Path.Balanced c₀ n₀ path' c n

Tactic:
exact ha.zoom (.redL hb hp)

Result:
no goals

Proof state:
α✝ : Type u_1
cut : α✝ → Ordering
t : RBNode α✝
path : Path α✝
t' : RBNode α✝
path' : Path α✝
c₀ : RBColor
n₀ : Nat
c : RBColor
n✝ n : Nat
x✝ y✝ : RBNode α✝
v✝ : α✝
ha : x✝.Balanced black n
hb : y✝.Balanced black n
hp : Path.Balanced c₀ n₀ path red n
⊢ (match cut v✝ with
      | Ordering.lt => zoom cut x✝ (left red path v✝ y✝)
      | Ordering.gt => zoom cut y✝ (right red x✝ v✝ path)
      | Ordering.eq => (node red x✝ v✝ y✝, path)) =
      (t', path') →
    ∃ c n, t'.Balanced c n ∧ Path.Balanced c₀ n₀ path' c n

Tactic:
split

Result:
case h_1
α✝ : Type u_1
cut : α✝ → Ordering
t : RBNode α✝
path : Path α✝
t' : RBNode α✝
path' : Path α✝
c₀ : RBColor
n₀ : Nat
c : RBColor
n✝ n : Nat
x✝¹ y✝ : RBNode α✝
v✝ : α✝
ha : x✝¹.Balanced black n
hb : y✝.Balanced black n
hp : Path.Balanced c₀ n₀ path red n
x✝ : Ordering
heq✝ : cut v✝ = Ordering.lt
⊢ zoom cut x✝¹ (left red path v✝ y✝) = (t', path') → ∃ c n, t'.Balanced c n ∧ Path.Balanced c₀ n₀ path' c n

case h_2
α✝ : Type u_1
cut : α✝ → Ordering
t : RBNode α✝
path : Path α✝
t' : RBNode α✝
path' : Path α✝
c₀ : RBColor
n₀ : Nat
c : RBColor
n✝ n : Nat
x✝¹ y✝ : RBNode α✝
v✝ : α✝
ha : x✝¹.Balanced black n
hb : y✝.Balanced black n
hp : Path.Balanced c₀ n₀ path red n
x✝ : Ordering
heq✝ : cut v✝ = Ordering.gt
⊢ zoom cut y✝ (right red x✝¹ v✝ path) = (t', path') → ∃ c n, t'.Balanced c n ∧ Path.Balanced c₀ n₀ path' c n

case h_3
α✝ : Type u_1
cut : α✝ → Ordering
t : RBNode α✝
path : Path α✝
t' : RBNode α✝
path' : Path α✝
c₀ : RBColor
n₀ : Nat
c : RBColor
n✝ n : Nat
x✝¹ y✝ : RBNode α✝
v✝ : α✝
ha : x✝¹.Balanced black n
hb : y✝.Balanced black n
hp : Path.Balanced c₀ n₀ path red n
x✝ : Ordering
heq✝ : cut v✝ = Ordering.eq
⊢ (node red x✝¹ v✝ y✝, path) = (t', path') → ∃ c n, t'.Balanced c n ∧ Path.Balanced c₀ n₀ path' c n

Proof state:
case h_3.refl
α✝ : Type u_1
cut : α✝ → Ordering
t : RBNode α✝
path : Path α✝
c₀ : RBColor
n₀ : Nat
c : RBColor
n : Nat
x✝¹ : RBNode α✝
c₁✝ : RBColor
n✝ : Nat
y✝ : RBNode α✝
c₂✝ : RBColor
v✝ : α✝
ha : x✝¹.Balanced c₁✝ n✝
hb : y✝.Balanced c₂✝ n✝
hp : Path.Balanced c₀ n₀ path black (n✝ + 1)
x✝ : Ordering
heq✝ : cut v✝ = Ordering.eq
⊢ ∃ c n, (node black x✝¹ v✝ y✝).Balanced c n ∧ Path.Balanced c₀ n₀ path c n

Tactic:
exact ⟨_, _, .black ha hb, hp⟩

Result:
no goals

Proof state:
α✝ : Type u_1
cut : α✝ → Ordering
t : RBNode α✝
path : Path α✝
t' : RBNode α✝
path' : Path α✝
c₀ : RBColor
n₀ : Nat
c : RBColor
n : Nat
hp : Path.Balanced c₀ n₀ path black 0
e : zoom cut nil path = (t', path')
⊢ ∃ c n, t'.Balanced c n ∧ Path.Balanced c₀ n₀ path' c n

Tactic:
cases e

Result:
case refl
α✝ : Type u_1
cut : α✝ → Ordering
t : RBNode α✝
path : Path α✝
c₀ : RBColor
n₀ : Nat
c : RBColor
n : Nat
hp : Path.Balanced c₀ n₀ path black 0
⊢ ∃ c n, nil.Balanced c n ∧ Path.Balanced c₀ n₀ path c n