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

State before:
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
x✝ : SizedArray α n
y✝ : SizedArray β n
f : α → β → γ
n✝ : Nat
a : α
x : SizedArray α n✝
b : β
y : SizedArray β n✝
IH : zipWith y x (flip f) = zipWith x y f
⊢ zipWith (cons b y) (cons a x) (flip f) = zipWith (cons a x) (cons b y) f
Tactic:
simp only [zipWith_cons]
State after:
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
x✝ : SizedArray α n
y✝ : SizedArray β n
f : α → β → γ
n✝ : Nat
a : α
x : SizedArray α n✝
b : β
y : SizedArray β n✝
IH : zipWith y x (flip f) = zipWith x y f
⊢ cons (flip f b a) (zipWith y x (flip f)) = cons (f a b) (zipWith x y f)

State before:
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
x✝ : SizedArray α n
y✝ : SizedArray β n
f : α → β → γ
n✝ : Nat
a : α
x : SizedArray α n✝
b : β
y : SizedArray β n✝
IH : zipWith y x (flip f) = zipWith x y f
⊢ cons (flip f b a) (zipWith y x (flip f)) = cons (f a b) (zipWith x y f)
Tactic:
exact congrArg (cons (f a b)) IH
State after:
no goals