case nil
α : Type u
β : Type u_1
γ : Type u_2
δ : Type ?u.94446
ε : Type ?u.94449
f : α → β → γ
l₂✝ : List β
i✝ : ℕ
l₂ : List β
i : ℕ
⊢ get? (zipWith f [] l₂) i = Option.bind (Option.map f (get? [] i)) fun g => Option.map g (get? l₂ i)

case cons
α : Type u
β : Type u_1
γ : Type u_2
δ : Type ?u.94446
ε : Type ?u.94449
f : α → β → γ
l₂✝ : List β
i✝ : ℕ
head : α
tail : List α
tail_ih✝ :
  ∀ (l₂ : List β) (i : ℕ),
    get? (zipWith f tail l₂) i = Option.bind (Option.map f (get? tail i)) fun g => Option.map g (get? l₂ i)
l₂ : List β
i : ℕ
⊢ get? (zipWith f (head :: tail) l₂) i =
    Option.bind (Option.map f (get? (head :: tail) i)) fun g => Option.map g (get? l₂ i)
α : Type u
β : Type u_1
γ : Type u_2
δ : Type ?u.94446
ε : Type ?u.94449
f : α → β → γ
l₁ : List α
l₂ : List β
i : ℕ
⊢ get? (zipWith f l₁ l₂) i = Option.bind (Option.map f (get? l₁ i)) fun g => Option.map g (get? l₂ i)
induction' l₁ with head tail generalizing l₂ i
no goals
case nil
α : Type u
β : Type u_1
γ : Type u_2
δ : Type ?u.94446
ε : Type ?u.94449
f : α → β → γ
l₂✝ : List β
i✝ : ℕ
l₂ : List β
i : ℕ
⊢ get? (zipWith f [] l₂) i = Option.bind (Option.map f (get? [] i)) fun g => Option.map g (get? l₂ i)
rw [zipWith] <;> simp
case cons.nil
α : Type u
β : Type u_1
γ : Type u_2
δ : Type ?u.94446
ε : Type ?u.94449
f : α → β → γ
l₂ : List β
i✝ : ℕ
head : α
tail : List α
tail_ih✝ :
  ∀ (l₂ : List β) (i : ℕ),
    get? (zipWith f tail l₂) i = Option.bind (Option.map f (get? tail i)) fun g => Option.map g (get? l₂ i)
i : ℕ
⊢ get? (zipWith f (head :: tail) []) i =
    Option.bind (Option.map f (get? (head :: tail) i)) fun g => Option.map g (get? [] i)

case cons.cons
α : Type u
β : Type u_1
γ : Type u_2
δ : Type ?u.94446
ε : Type ?u.94449
f : α → β → γ
l₂ : List β
i✝ : ℕ
head : α
tail : List α
tail_ih✝ :
  ∀ (l₂ : List β) (i : ℕ),
    get? (zipWith f tail l₂) i = Option.bind (Option.map f (get? tail i)) fun g => Option.map g (get? l₂ i)
i : ℕ
head✝ : β
tail✝ : List β
⊢ get? (zipWith f (head :: tail) (head✝ :: tail✝)) i =
    Option.bind (Option.map f (get? (head :: tail) i)) fun g => Option.map g (get? (head✝ :: tail✝) i)
case cons
α : Type u
β : Type u_1
γ : Type u_2
δ : Type ?u.94446
ε : Type ?u.94449
f : α → β → γ
l₂✝ : List β
i✝ : ℕ
head : α
tail : List α
tail_ih✝ :
  ∀ (l₂ : List β) (i : ℕ),
    get? (zipWith f tail l₂) i = Option.bind (Option.map f (get? tail i)) fun g => Option.map g (get? l₂ i)
l₂ : List β
i : ℕ
⊢ get? (zipWith f (head :: tail) l₂) i =
    Option.bind (Option.map f (get? (head :: tail) i)) fun g => Option.map g (get? l₂ i)
cases l₂
case cons.nil
α : Type u
β : Type u_1
γ : Type u_2
δ : Type ?u.94446
ε : Type ?u.94449
f : α → β → γ
l₂ : List β
i✝ : ℕ
head : α
tail : List α
tail_ih✝ :
  ∀ (l₂ : List β) (i : ℕ),
    get? (zipWith f tail l₂) i = Option.bind (Option.map f (get? tail i)) fun g => Option.map g (get? l₂ i)
i : ℕ
⊢ none = Option.bind (Option.map f (get? (head :: tail) i)) fun g => none

case cons.cons
α : Type u
β : Type u_1
γ : Type u_2
δ : Type ?u.94446
ε : Type ?u.94449
f : α → β → γ
l₂ : List β
i✝ : ℕ
head : α
tail : List α
tail_ih✝ :
  ∀ (l₂ : List β) (i : ℕ),
    get? (zipWith f tail l₂) i = Option.bind (Option.map f (get? tail i)) fun g => Option.map g (get? l₂ i)
i : ℕ
head✝ : β
tail✝ : List β
⊢ get? (zipWith f (head :: tail) (head✝ :: tail✝)) i =
    Option.bind (Option.map f (get? (head :: tail) i)) fun g => Option.map g (get? (head✝ :: tail✝) i)
case cons.nil
α : Type u
β : Type u_1
γ : Type u_2
δ : Type ?u.94446
ε : Type ?u.94449
f : α → β → γ
l₂ : List β
i✝ : ℕ
head : α
tail : List α
tail_ih✝ :
  ∀ (l₂ : List β) (i : ℕ),
    get? (zipWith f tail l₂) i = Option.bind (Option.map f (get? tail i)) fun g => Option.map g (get? l₂ i)
i : ℕ
⊢ get? (zipWith f (head :: tail) []) i =
    Option.bind (Option.map f (get? (head :: tail) i)) fun g => Option.map g (get? [] i)

case cons.cons
α : Type u
β : Type u_1
γ : Type u_2
δ : Type ?u.94446
ε : Type ?u.94449
f : α → β → γ
l₂ : List β
i✝ : ℕ
head : α
tail : List α
tail_ih✝ :
  ∀ (l₂ : List β) (i : ℕ),
    get? (zipWith f tail l₂) i = Option.bind (Option.map f (get? tail i)) fun g => Option.map g (get? l₂ i)
i : ℕ
head✝ : β
tail✝ : List β
⊢ get? (zipWith f (head :: tail) (head✝ :: tail✝)) i =
    Option.bind (Option.map f (get? (head :: tail) i)) fun g => Option.map g (get? (head✝ :: tail✝) i)
simp only [zipWith, Seq.seq, Functor.map, get?, Option.map_none']
no goals
case cons.nil
α : Type u
β : Type u_1
γ : Type u_2
δ : Type ?u.94446
ε : Type ?u.94449
f : α → β → γ
l₂ : List β
i✝ : ℕ
head : α
tail : List α
tail_ih✝ :
  ∀ (l₂ : List β) (i : ℕ),
    get? (zipWith f tail l₂) i = Option.bind (Option.map f (get? tail i)) fun g => Option.map g (get? l₂ i)
i : ℕ
⊢ none = Option.bind (Option.map f (get? (head :: tail) i)) fun g => none
cases (head :: tail).get? i <;> rfl
no goals
case cons.cons
α : Type u
β : Type u_1
γ : Type u_2
δ : Type ?u.94446
ε : Type ?u.94449
f : α → β → γ
l₂ : List β
i✝ : ℕ
head : α
tail : List α
tail_ih✝ :
  ∀ (l₂ : List β) (i : ℕ),
    get? (zipWith f tail l₂) i = Option.bind (Option.map f (get? tail i)) fun g => Option.map g (get? l₂ i)
i : ℕ
head✝ : β
tail✝ : List β
⊢ get? (zipWith f (head :: tail) (head✝ :: tail✝)) i =
    Option.bind (Option.map f (get? (head :: tail) i)) fun g => Option.map g (get? (head✝ :: tail✝) i)
cases i <;> simp only [Option.map_some', get?, Option.some_bind', *]