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

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

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

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

State before:
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
a : α
x : SizedArray α n
b : β
y : SizedArray β n
f : α → β → γ
⊢ mapIdx ((fun i => f (cons a x)[i]) ∘ Fin.succ) y = mapIdx (fun i => f x[i]) y
Tactic:
apply congrFun
State after:
case h
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
a : α
x : SizedArray α n
b : β
y : SizedArray β n
f : α → β → γ
⊢ mapIdx ((fun i => f (cons a x)[i]) ∘ Fin.succ) = fun y => mapIdx (fun i => f x[i]) y

State before:
case h
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
a : α
x : SizedArray α n
b : β
y : SizedArray β n
f : α → β → γ
⊢ mapIdx ((fun i => f (cons a x)[i]) ∘ Fin.succ) = fun y => 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
a : α
x : SizedArray α n
b : β
y : SizedArray β n
f : α → β → γ
⊢ (fun i => f (cons a x)[i]) ∘ Fin.succ = fun i => f x[i]

State before:
case h.h
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
a : α
x : SizedArray α n
b : β
y : SizedArray β n
f : α → β → γ
⊢ (fun i => f (cons a x)[i]) ∘ Fin.succ = fun i => f x[i]
Tactic:
funext i
State after:
case h.h.h
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
a : α
x : SizedArray α n
b : β
y : SizedArray β n
f : α → β → γ
i : Fin n
⊢ ((fun i => f (cons a x)[i]) ∘ Fin.succ) i = f x[i]

State before:
case h.h.h
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
a : α
x : SizedArray α n
b : β
y : SizedArray β n
f : α → β → γ
i : Fin n
⊢ ((fun i => f (cons a x)[i]) ∘ Fin.succ) i = f x[i]
Tactic:
cases i with | mk i h => rfl
State after:
no goals

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