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

State before:
α : Type u
β : Type v
γ : Type w
f : α → β → γ
x : Array α
y : Array β
z : Array γ
⊢ (zipWithAux f x y 0 z).data = List.zipWithTR.go f x.data y.data z
Tactic:
induction x using cons_induction generalizing y z with
| empty =>
  rw [zipWithAux_nil_first]; exact z.toList_eq.symm
| cons a x IH =>
  cases y using cons_cases_on with
  | empty =>
    rw [zipWithAux_nil_second]; exact z.toList_eq.symm
  | cons b y =>
    rw [zipWithAux_cons_cons_zero]; exact IH _ _
State after:
no goals

State before:
case empty
α : Type u
β : Type v
γ : Type w
f : α → β → γ
y : Array β
z : Array γ
⊢ (zipWithAux f #[] y 0 z).data = List.zipWithTR.go f #[].data y.data z
Tactic:
rw [zipWithAux_nil_first]
State after:
case empty
α : Type u
β : Type v
γ : Type w
f : α → β → γ
y : Array β
z : Array γ
⊢ z.data = List.zipWithTR.go f #[].data y.data z

State before:
case empty
α : Type u
β : Type v
γ : Type w
f : α → β → γ
y : Array β
z : Array γ
⊢ z.data = List.zipWithTR.go f #[].data y.data z
Tactic:
exact z.toList_eq.symm
State after:
no goals

State before:
case cons
α : Type u
β : Type v
γ : Type w
f : α → β → γ
a : α
x : Array α
IH : ∀ (y : Array β) (z : Array γ), (zipWithAux f x y 0 z).data = List.zipWithTR.go f x.data y.data z
y : Array β
z : Array γ
⊢ (zipWithAux f (cons a x) y 0 z).data = List.zipWithTR.go f (cons a x).data y.data z
Tactic:
cases y using cons_cases_on with
| empty =>
  rw [zipWithAux_nil_second]; exact z.toList_eq.symm
| cons b y =>
  rw [zipWithAux_cons_cons_zero]; exact IH _ _
State after:
no goals

State before:
case cons.empty
α : Type u
β : Type v
γ : Type w
f : α → β → γ
a : α
x : Array α
IH : ∀ (y : Array β) (z : Array γ), (zipWithAux f x y 0 z).data = List.zipWithTR.go f x.data y.data z
z : Array γ
⊢ (zipWithAux f (cons a x) #[] 0 z).data = List.zipWithTR.go f (cons a x).data #[].data z
Tactic:
rw [zipWithAux_nil_second]
State after:
case cons.empty
α : Type u
β : Type v
γ : Type w
f : α → β → γ
a : α
x : Array α
IH : ∀ (y : Array β) (z : Array γ), (zipWithAux f x y 0 z).data = List.zipWithTR.go f x.data y.data z
z : Array γ
⊢ z.data = List.zipWithTR.go f (cons a x).data #[].data z

State before:
case cons.empty
α : Type u
β : Type v
γ : Type w
f : α → β → γ
a : α
x : Array α
IH : ∀ (y : Array β) (z : Array γ), (zipWithAux f x y 0 z).data = List.zipWithTR.go f x.data y.data z
z : Array γ
⊢ z.data = List.zipWithTR.go f (cons a x).data #[].data z
Tactic:
exact z.toList_eq.symm
State after:
no goals

State before:
case cons.cons
α : Type u
β : Type v
γ : Type w
f : α → β → γ
a : α
x : Array α
IH : ∀ (y : Array β) (z : Array γ), (zipWithAux f x y 0 z).data = List.zipWithTR.go f x.data y.data z
z : Array γ
b : β
y : Array β
⊢ (zipWithAux f (cons a x) (cons b y) 0 z).data = List.zipWithTR.go f (cons a x).data (cons b y).data z
Tactic:
rw [zipWithAux_cons_cons_zero]
State after:
case cons.cons
α : Type u
β : Type v
γ : Type w
f : α → β → γ
a : α
x : Array α
IH : ∀ (y : Array β) (z : Array γ), (zipWithAux f x y 0 z).data = List.zipWithTR.go f x.data y.data z
z : Array γ
b : β
y : Array β
⊢ (zipWithAux f x y 0 (push z (f a b))).data = List.zipWithTR.go f (cons a x).data (cons b y).data z

State before:
case cons.cons
α : Type u
β : Type v
γ : Type w
f : α → β → γ
a : α
x : Array α
IH : ∀ (y : Array β) (z : Array γ), (zipWithAux f x y 0 z).data = List.zipWithTR.go f x.data y.data z
z : Array γ
b : β
y : Array β
⊢ (zipWithAux f x y 0 (push z (f a b))).data = List.zipWithTR.go f (cons a x).data (cons b y).data z
Tactic:
exact IH _ _
State after:
no goals