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

State before:
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
α₁ : Type u₁
α₂ : Type u₂
β₁ : Type v₁
β₂ : Type v₂
x✝ : SizedArray α₁ n
y✝ : SizedArray α₂ n
f : α₁ → α₂ → β₁
z✝ : SizedArray β₂ n
g : β₁ → β₂ → γ
n✝ : Nat
a : α₁
x : SizedArray α₁ n✝
b : α₂
y : SizedArray α₂ n✝
IH : ∀ (x_1 : SizedArray β₂ n✝), zipWith (zipWith x y f) x_1 g = zipWith₃ x y x_1 fun a₁ a₂ b₂ => g (f a₁ a₂) b₂
z : SizedArray β₂ (n✝ + 1)
⊢ zipWith (zipWith (cons a x) (cons b y) f) z g = zipWith₃ (cons a x) (cons b y) z fun a₁ a₂ b₂ => g (f a₁ a₂) b₂
Tactic:
rw [← z.cons_head_tail]
State after:
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
α₁ : Type u₁
α₂ : Type u₂
β₁ : Type v₁
β₂ : Type v₂
x✝ : SizedArray α₁ n
y✝ : SizedArray α₂ n
f : α₁ → α₂ → β₁
z✝ : SizedArray β₂ n
g : β₁ → β₂ → γ
n✝ : Nat
a : α₁
x : SizedArray α₁ n✝
b : α₂
y : SizedArray α₂ n✝
IH : ∀ (x_1 : SizedArray β₂ n✝), zipWith (zipWith x y f) x_1 g = zipWith₃ x y x_1 fun a₁ a₂ b₂ => g (f a₁ a₂) b₂
z : SizedArray β₂ (n✝ + 1)
⊢ zipWith (zipWith (cons a x) (cons b y) f) (cons (head z) (tail z)) g =
    zipWith₃ (cons a x) (cons b y) (cons (head z) (tail z)) fun a₁ a₂ b₂ => g (f a₁ a₂) b₂

State before:
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
α₁ : Type u₁
α₂ : Type u₂
β₁ : Type v₁
β₂ : Type v₂
x✝ : SizedArray α₁ n
y✝ : SizedArray α₂ n
f : α₁ → α₂ → β₁
z✝ : SizedArray β₂ n
g : β₁ → β₂ → γ
n✝ : Nat
a : α₁
x : SizedArray α₁ n✝
b : α₂
y : SizedArray α₂ n✝
IH : ∀ (x_1 : SizedArray β₂ n✝), zipWith (zipWith x y f) x_1 g = zipWith₃ x y x_1 fun a₁ a₂ b₂ => g (f a₁ a₂) b₂
z : SizedArray β₂ (n✝ + 1)
⊢ zipWith (zipWith (cons a x) (cons b y) f) (cons (head z) (tail z)) g =
    zipWith₃ (cons a x) (cons b y) (cons (head z) (tail z)) fun a₁ a₂ b₂ => g (f a₁ a₂) b₂
Tactic:
simp only [zipWith_cons, zipWith₃_cons]
State after:
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
α₁ : Type u₁
α₂ : Type u₂
β₁ : Type v₁
β₂ : Type v₂
x✝ : SizedArray α₁ n
y✝ : SizedArray α₂ n
f : α₁ → α₂ → β₁
z✝ : SizedArray β₂ n
g : β₁ → β₂ → γ
n✝ : Nat
a : α₁
x : SizedArray α₁ n✝
b : α₂
y : SizedArray α₂ n✝
IH : ∀ (x_1 : SizedArray β₂ n✝), zipWith (zipWith x y f) x_1 g = zipWith₃ x y x_1 fun a₁ a₂ b₂ => g (f a₁ a₂) b₂
z : SizedArray β₂ (n✝ + 1)
⊢ cons (g (f a b) (head z)) (zipWith (zipWith x y f) (tail z) g) =
    cons (g (f a b) (head z)) (zipWith₃ x y (tail z) fun a₁ a₂ b₂ => g (f a₁ a₂) b₂)

State before:
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
α₁ : Type u₁
α₂ : Type u₂
β₁ : Type v₁
β₂ : Type v₂
x✝ : SizedArray α₁ n
y✝ : SizedArray α₂ n
f : α₁ → α₂ → β₁
z✝ : SizedArray β₂ n
g : β₁ → β₂ → γ
n✝ : Nat
a : α₁
x : SizedArray α₁ n✝
b : α₂
y : SizedArray α₂ n✝
IH : ∀ (x_1 : SizedArray β₂ n✝), zipWith (zipWith x y f) x_1 g = zipWith₃ x y x_1 fun a₁ a₂ b₂ => g (f a₁ a₂) b₂
z : SizedArray β₂ (n✝ + 1)
⊢ cons (g (f a b) (head z)) (zipWith (zipWith x y f) (tail z) g) =
    cons (g (f a b) (head z)) (zipWith₃ x y (tail z) fun a₁ a₂ b₂ => g (f a₁ a₂) b₂)
Tactic:
rw [IH z.tail]
State after:
no goals