Theorem: Array.zipWith_data_eq_zipWith_data (Algdata/Data/Array/Lemmas.lean)

State before:
α : Type u
β : Type v
γ : Type w
f : α → β → γ
x : Array α
y : Array β
⊢ (zipWith x y f).data = List.zipWith f x.data y.data
Tactic:
show (zipWithAux f x y 0 #[]).data = List.zipWith f x.data y.data
State after:
α : Type u
β : Type v
γ : Type w
f : α → β → γ
x : Array α
y : Array β
⊢ (zipWithAux f x y 0 #[]).data = List.zipWith f x.data y.data

State before:
α : Type u
β : Type v
γ : Type w
f : α → β → γ
x : Array α
y : Array β
⊢ (zipWithAux f x y 0 #[]).data = List.zipWith f x.data y.data
Tactic:
rw [zipWithAux_data_eq_zipWithTR_go, List.zipWith_eq_zipWithTR]
State after:
α : Type u
β : Type v
γ : Type w
f : α → β → γ
x : Array α
y : Array β
⊢ List.zipWithTR.go f x.data y.data #[] = List.zipWithTR f x.data y.data

State before:
α : Type u
β : Type v
γ : Type w
f : α → β → γ
x : Array α
y : Array β
⊢ List.zipWithTR.go f x.data y.data #[] = List.zipWithTR f x.data y.data
Tactic:
rfl
State after:
no goals