no goals
α : Type u_1
cut : α → Ordering
t : RBNode α
path : Path α
⊢ fill' (zoom cut t path) = fill path t
induction t generalizing path with
| nil => rfl
| node _ _ _ _ iha ihb => unfold zoom; split <;> [apply iha; apply ihb; rfl]
no goals
case nil
α : Type u_1
cut : α → Ordering
path : Path α
⊢ fill' (zoom cut nil path) = fill path nil
rfl
case node
α : Type u_1
cut : α → Ordering
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
iha : ∀ (path : Path α), fill' (zoom cut l✝ path) = fill path l✝
ihb : ∀ (path : Path α), fill' (zoom cut r✝ path) = fill path r✝
path : Path α
⊢ fill'
      (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)) =
    fill path (node c✝ l✝ v✝ r✝)
case node
α : Type u_1
cut : α → Ordering
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
iha : ∀ (path : Path α), fill' (zoom cut l✝ path) = fill path l✝
ihb : ∀ (path : Path α), fill' (zoom cut r✝ path) = fill path r✝
path : Path α
⊢ fill' (zoom cut (node c✝ l✝ v✝ r✝) path) = fill path (node c✝ l✝ v✝ r✝)
unfold zoom
no goals
case node
α : Type u_1
cut : α → Ordering
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
iha : ∀ (path : Path α), fill' (zoom cut l✝ path) = fill path l✝
ihb : ∀ (path : Path α), fill' (zoom cut r✝ path) = fill path r✝
path : Path α
⊢ fill'
      (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)) =
    fill path (node c✝ l✝ v✝ r✝)
split <;> [apply iha; apply ihb; rfl]