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

State before:
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
x : SizedArray α n
y : SizedArray β n
f : α → β → γ
i : Nat
h : i < n
⊢ (zipWith x y f)[i] = f x[i] y[i]
Tactic:
induction x, y using cons_induction_on₂ generalizing i with
| empty => cases h
| cons a x b y IH =>
  simp only [zipWith_cons]
  cases i with
  | zero => simp only [get_cons_zero]
  | succ i =>
    simp only [Nat.succ_eq_add_one, get_cons_succ (hi₁:=h) (hi₂:=Nat.lt_of_succ_lt_succ h)]
    exact IH
State after:
no goals

State before:
case empty
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
f : α → β → γ
i : Nat
h : i < 0
⊢ (zipWith empty empty f)[i] = f empty[i] empty[i]
Tactic:
cases h
State after:
no goals

State before:
case cons
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
f : α → β → γ
n✝ : Nat
a : α
x : SizedArray α n✝
b : β
y : SizedArray β n✝
IH : ∀ {i : Nat} {h : i < n✝}, (zipWith x y f)[i] = f x[i] y[i]
i : Nat
h : i < n✝ + 1
⊢ (zipWith (cons a x) (cons b y) f)[i] = f (cons a x)[i] (cons b y)[i]
Tactic:
simp only [zipWith_cons]
State after:
case cons
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
f : α → β → γ
n✝ : Nat
a : α
x : SizedArray α n✝
b : β
y : SizedArray β n✝
IH : ∀ {i : Nat} {h : i < n✝}, (zipWith x y f)[i] = f x[i] y[i]
i : Nat
h : i < n✝ + 1
⊢ (cons (f a b) (zipWith x y f))[i] = f (cons a x)[i] (cons b y)[i]

State before:
case cons
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
f : α → β → γ
n✝ : Nat
a : α
x : SizedArray α n✝
b : β
y : SizedArray β n✝
IH : ∀ {i : Nat} {h : i < n✝}, (zipWith x y f)[i] = f x[i] y[i]
i : Nat
h : i < n✝ + 1
⊢ (cons (f a b) (zipWith x y f))[i] = f (cons a x)[i] (cons b y)[i]
Tactic:
cases i with
| zero => simp only [get_cons_zero]
| succ i =>
  simp only [Nat.succ_eq_add_one, get_cons_succ (hi₁:=h) (hi₂:=Nat.lt_of_succ_lt_succ h)]
  exact IH
State after:
no goals

State before:
case cons.zero
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
f : α → β → γ
n✝ : Nat
a : α
x : SizedArray α n✝
b : β
y : SizedArray β n✝
IH : ∀ {i : Nat} {h : i < n✝}, (zipWith x y f)[i] = f x[i] y[i]
h : Nat.zero < n✝ + 1
⊢ (cons (f a b) (zipWith x y f))[Nat.zero] = f (cons a x)[Nat.zero] (cons b y)[Nat.zero]
Tactic:
simp only [get_cons_zero]
State after:
no goals

State before:
case cons.succ
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
f : α → β → γ
n✝ : Nat
a : α
x : SizedArray α n✝
b : β
y : SizedArray β n✝
IH : ∀ {i : Nat} {h : i < n✝}, (zipWith x y f)[i] = f x[i] y[i]
i : Nat
h : Nat.succ i < n✝ + 1
⊢ (cons (f a b) (zipWith x y f))[Nat.succ i] = f (cons a x)[Nat.succ i] (cons b y)[Nat.succ i]
Tactic:
simp only [Nat.succ_eq_add_one, get_cons_succ (hi₁:=h) (hi₂:=Nat.lt_of_succ_lt_succ h)]
State after:
case cons.succ
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
f : α → β → γ
n✝ : Nat
a : α
x : SizedArray α n✝
b : β
y : SizedArray β n✝
IH : ∀ {i : Nat} {h : i < n✝}, (zipWith x y f)[i] = f x[i] y[i]
i : Nat
h : Nat.succ i < n✝ + 1
⊢ (zipWith x y f)[i] = f x[i] y[i]

State before:
case cons.succ
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
f : α → β → γ
n✝ : Nat
a : α
x : SizedArray α n✝
b : β
y : SizedArray β n✝
IH : ∀ {i : Nat} {h : i < n✝}, (zipWith x y f)[i] = f x[i] y[i]
i : Nat
h : Nat.succ i < n✝ + 1
⊢ (zipWith x y f)[i] = f x[i] y[i]
Tactic:
exact IH
State after:
no goals