Theorem: SizedArray.zipWith_push (Algdata/Data/Array/Sized.lean)

State before:
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
x : SizedArray α n
a : α
y : SizedArray β n
b : β
f : α → β → γ
⊢ zipWith (push x a) (push y b) f = push (zipWith x y f) (f a b)
Tactic:
unfold zipWith
State after:
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
x : SizedArray α n
a : α
y : SizedArray β n
b : β
f : α → β → γ
⊢ mapIdx (fun i => f (push x a)[i]) (push y b) = push (mapIdx (fun i => f x[i]) y) (f a b)

State before:
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
x : SizedArray α n
a : α
y : SizedArray β n
b : β
f : α → β → γ
⊢ mapIdx (fun i => f (push x a)[i]) (push y b) = push (mapIdx (fun i => f x[i]) y) (f a b)
Tactic:
rw [mapIdx_push]
State after:
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
x : SizedArray α n
a : α
y : SizedArray β n
b : β
f : α → β → γ
⊢ push (mapIdx (fun i => f (push x a)[{ val := ↑i, isLt := (_ : ↑i < Nat.succ n) }]) y)
      (f (push x a)[{ val := n, isLt := (_ : n < Nat.succ n) }] b) =
    push (mapIdx (fun i => f x[i]) y) (f a b)

State before:
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
x : SizedArray α n
a : α
y : SizedArray β n
b : β
f : α → β → γ
⊢ push (mapIdx (fun i => f (push x a)[{ val := ↑i, isLt := (_ : ↑i < Nat.succ n) }]) y)
      (f (push x a)[{ val := n, isLt := (_ : n < Nat.succ n) }] b) =
    push (mapIdx (fun i => f x[i]) y) (f a b)
Tactic:
conv =>
  lhs; arg 2
  change f ((push x a)[n]'n.lt_succ_self) b
  rw [get_push, dif_neg n.lt_irrefl]
State after:
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
x : SizedArray α n
a : α
y : SizedArray β n
b : β
f : α → β → γ
⊢ push (mapIdx (fun i => f (push x a)[{ val := ↑i, isLt := (_ : ↑i < Nat.succ n) }]) y) (f a b) =
    push (mapIdx (fun i => f x[i]) y) (f a b)

State before:
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
x : SizedArray α n
a : α
y : SizedArray β n
b : β
f : α → β → γ
⊢ push (mapIdx (fun i => f (push x a)[{ val := ↑i, isLt := (_ : ↑i < Nat.succ n) }]) y) (f a b) =
    push (mapIdx (fun i => f x[i]) y) (f a b)
Tactic:
apply congrFun
State after:
case h
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
x : SizedArray α n
a : α
y : SizedArray β n
b : β
f : α → β → γ
⊢ push (mapIdx (fun i => f (push x a)[{ val := ↑i, isLt := (_ : ↑i < Nat.succ n) }]) y) =
    push (mapIdx (fun i => f x[i]) y)

State before:
case h
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
x : SizedArray α n
a : α
y : SizedArray β n
b : β
f : α → β → γ
⊢ push (mapIdx (fun i => f (push x a)[{ val := ↑i, isLt := (_ : ↑i < Nat.succ n) }]) y) =
    push (mapIdx (fun i => f x[i]) y)
Tactic:
apply congrArg
State after:
case h.h
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
x : SizedArray α n
a : α
y : SizedArray β n
b : β
f : α → β → γ
⊢ mapIdx (fun i => f (push x a)[{ val := ↑i, isLt := (_ : ↑i < Nat.succ n) }]) y = mapIdx (fun i => f x[i]) y

State before:
case h.h
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
x : SizedArray α n
a : α
y : SizedArray β n
b : β
f : α → β → γ
⊢ mapIdx (fun i => f (push x a)[{ val := ↑i, isLt := (_ : ↑i < Nat.succ n) }]) y = mapIdx (fun i => f x[i]) y
Tactic:
apply congrFun
State after:
case h.h.h
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
x : SizedArray α n
a : α
y : SizedArray β n
b : β
f : α → β → γ
⊢ (mapIdx fun i => f (push x a)[{ val := ↑i, isLt := (_ : ↑i < Nat.succ n) }]) = fun y => mapIdx (fun i => f x[i]) y

State before:
case h.h.h
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
x : SizedArray α n
a : α
y : SizedArray β n
b : β
f : α → β → γ
⊢ (mapIdx fun i => f (push x a)[{ val := ↑i, isLt := (_ : ↑i < Nat.succ n) }]) = fun y => mapIdx (fun i => f x[i]) y
Tactic:
apply congrArg
State after:
case h.h.h.h
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
x : SizedArray α n
a : α
y : SizedArray β n
b : β
f : α → β → γ
⊢ (fun i => f (push x a)[{ val := ↑i, isLt := (_ : ↑i < Nat.succ n) }]) = fun i => f x[i]

State before:
case h.h.h.h
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
x : SizedArray α n
a : α
y : SizedArray β n
b : β
f : α → β → γ
⊢ (fun i => f (push x a)[{ val := ↑i, isLt := (_ : ↑i < Nat.succ n) }]) = fun i => f x[i]
Tactic:
funext i
State after:
case h.h.h.h.h
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
x : SizedArray α n
a : α
y : SizedArray β n
b : β
f : α → β → γ
i : Fin n
⊢ f (push x a)[{ val := ↑i, isLt := (_ : ↑i < Nat.succ n) }] = f x[i]

State before:
case h.h.h.h.h
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
x : SizedArray α n
a : α
y : SizedArray β n
b : β
f : α → β → γ
i : Fin n
⊢ f (push x a)[{ val := ↑i, isLt := (_ : ↑i < Nat.succ n) }] = f x[i]
Tactic:
cases i with | mk i h =>
apply congrArg
show (push x a)[i]'(.step h) = x[i]'h
rw [get_push, dif_pos h]
State after:
no goals

State before:
case h.h.h.h.h.mk
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
x : SizedArray α n
a : α
y : SizedArray β n
b : β
f : α → β → γ
i : Nat
h : i < n
⊢ f (push x a)[{ val := ↑{ val := i, isLt := h }, isLt := (_ : ↑{ val := i, isLt := h } < Nat.succ n) }] =
    f x[{ val := i, isLt := h }]
Tactic:
apply congrArg
State after:
case h.h.h.h.h.mk.h
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
x : SizedArray α n
a : α
y : SizedArray β n
b : β
f : α → β → γ
i : Nat
h : i < n
⊢ (push x a)[{ val := ↑{ val := i, isLt := h }, isLt := (_ : ↑{ val := i, isLt := h } < Nat.succ n) }] =
    x[{ val := i, isLt := h }]

State before:
case h.h.h.h.h.mk.h
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
x : SizedArray α n
a : α
y : SizedArray β n
b : β
f : α → β → γ
i : Nat
h : i < n
⊢ (push x a)[{ val := ↑{ val := i, isLt := h }, isLt := (_ : ↑{ val := i, isLt := h } < Nat.succ n) }] =
    x[{ val := i, isLt := h }]
Tactic:
show (push x a)[i]'(.step h) = x[i]'h
State after:
case h.h.h.h.h.mk.h
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
x : SizedArray α n
a : α
y : SizedArray β n
b : β
f : α → β → γ
i : Nat
h : i < n
⊢ (push x a)[i] = x[i]

State before:
case h.h.h.h.h.mk.h
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
x : SizedArray α n
a : α
y : SizedArray β n
b : β
f : α → β → γ
i : Nat
h : i < n
⊢ (push x a)[i] = x[i]
Tactic:
rw [get_push, dif_pos h]
State after:
no goals