Theorem: SizedArray.zipWith_zipWith_right (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
z✝ : SizedArray β₂ n
f : β₁ → β₂ → α₂
g : α₁ → α₂ → γ
n✝ : Nat
b : β₁
y : SizedArray β₁ n✝
c : β₂
z : SizedArray β₂ n✝
IH : ∀ (x : SizedArray α₁ n✝), zipWith x (zipWith y z f) g = zipWith₃ x y z fun a b c => g a (f b c)
x : SizedArray α₁ (n✝ + 1)
⊢ zipWith x (zipWith (cons b y) (cons c z) f) g = zipWith₃ x (cons b y) (cons c z) fun a b c => g a (f b c)
Tactic:
rw [← x.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
z✝ : SizedArray β₂ n
f : β₁ → β₂ → α₂
g : α₁ → α₂ → γ
n✝ : Nat
b : β₁
y : SizedArray β₁ n✝
c : β₂
z : SizedArray β₂ n✝
IH : ∀ (x : SizedArray α₁ n✝), zipWith x (zipWith y z f) g = zipWith₃ x y z fun a b c => g a (f b c)
x : SizedArray α₁ (n✝ + 1)
⊢ zipWith (cons (head x) (tail x)) (zipWith (cons b y) (cons c z) f) g =
    zipWith₃ (cons (head x) (tail x)) (cons b y) (cons c z) fun a b c => g a (f b c)

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
z✝ : SizedArray β₂ n
f : β₁ → β₂ → α₂
g : α₁ → α₂ → γ
n✝ : Nat
b : β₁
y : SizedArray β₁ n✝
c : β₂
z : SizedArray β₂ n✝
IH : ∀ (x : SizedArray α₁ n✝), zipWith x (zipWith y z f) g = zipWith₃ x y z fun a b c => g a (f b c)
x : SizedArray α₁ (n✝ + 1)
⊢ zipWith (cons (head x) (tail x)) (zipWith (cons b y) (cons c z) f) g =
    zipWith₃ (cons (head x) (tail x)) (cons b y) (cons c z) fun a b c => g a (f b c)
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
z✝ : SizedArray β₂ n
f : β₁ → β₂ → α₂
g : α₁ → α₂ → γ
n✝ : Nat
b : β₁
y : SizedArray β₁ n✝
c : β₂
z : SizedArray β₂ n✝
IH : ∀ (x : SizedArray α₁ n✝), zipWith x (zipWith y z f) g = zipWith₃ x y z fun a b c => g a (f b c)
x : SizedArray α₁ (n✝ + 1)
⊢ cons (g (head x) (f b c)) (zipWith (tail x) (zipWith y z f) g) =
    cons (g (head x) (f b c)) (zipWith₃ (tail x) y z fun a b c => g a (f b c))

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
z✝ : SizedArray β₂ n
f : β₁ → β₂ → α₂
g : α₁ → α₂ → γ
n✝ : Nat
b : β₁
y : SizedArray β₁ n✝
c : β₂
z : SizedArray β₂ n✝
IH : ∀ (x : SizedArray α₁ n✝), zipWith x (zipWith y z f) g = zipWith₃ x y z fun a b c => g a (f b c)
x : SizedArray α₁ (n✝ + 1)
⊢ cons (g (head x) (f b c)) (zipWith (tail x) (zipWith y z f) g) =
    cons (g (head x) (f b c)) (zipWith₃ (tail x) y z fun a b c => g a (f b c))
Tactic:
rw [IH x.tail]
State after:
no goals