case nil
α✝ : Type u
β✝ : Type ?u.112193
γ✝ : Type ?u.112196
δ : Type ?u.112199
ε : Type ?u.112202
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
z : γ
l₂ : List β
i : ℕ
⊢ get? (zipWith f [] l₂) i = some z ↔ ∃ x y, get? [] i = some x ∧ get? l₂ i = some y ∧ f x y = z

case cons
α✝ : Type u
β✝ : Type ?u.112193
γ✝ : Type ?u.112196
δ : Type ?u.112199
ε : Type ?u.112202
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
z : γ
head✝ : α
tail✝ : List α
tail_ih✝ :
  ∀ (l₂ : List β) (i : ℕ),
    get? (zipWith f tail✝ l₂) i = some z ↔ ∃ x y, get? tail✝ i = some x ∧ get? l₂ i = some y ∧ f x y = z
l₂ : List β
i : ℕ
⊢ get? (zipWith f (head✝ :: tail✝) l₂) i = some z ↔
    ∃ x y, get? (head✝ :: tail✝) i = some x ∧ get? l₂ i = some y ∧ f x y = z
α✝ : Type u
β✝ : Type ?u.112193
γ✝ : Type ?u.112196
δ : Type ?u.112199
ε : Type ?u.112202
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
l₁ : List α
l₂ : List β
z : γ
i : ℕ
⊢ get? (zipWith f l₁ l₂) i = some z ↔ ∃ x y, get? l₁ i = some x ∧ get? l₂ i = some y ∧ f x y = z
induction l₁ generalizing l₂ i
no goals
case nil
α✝ : Type u
β✝ : Type ?u.112193
γ✝ : Type ?u.112196
δ : Type ?u.112199
ε : Type ?u.112202
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
z : γ
l₂ : List β
i : ℕ
⊢ get? (zipWith f [] l₂) i = some z ↔ ∃ x y, get? [] i = some x ∧ get? l₂ i = some y ∧ f x y = z
simp [zipWith]
case cons.cons
α✝ : Type u
β✝ : Type ?u.112193
γ✝ : Type ?u.112196
δ : Type ?u.112199
ε : Type ?u.112202
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
z : γ
head✝¹ : α
tail✝¹ : List α
tail_ih✝ :
  ∀ (l₂ : List β) (i : ℕ),
    get? (zipWith f tail✝¹ l₂) i = some z ↔ ∃ x y, get? tail✝¹ i = some x ∧ get? l₂ i = some y ∧ f x y = z
i : ℕ
head✝ : β
tail✝ : List β
⊢ get? (f head✝¹ head✝ :: zipWith f tail✝¹ tail✝) i = some z ↔
    ∃ x y, get? (head✝¹ :: tail✝¹) i = some x ∧ get? (head✝ :: tail✝) i = some y ∧ f x y = z
case cons
α✝ : Type u
β✝ : Type ?u.112193
γ✝ : Type ?u.112196
δ : Type ?u.112199
ε : Type ?u.112202
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
z : γ
head✝ : α
tail✝ : List α
tail_ih✝ :
  ∀ (l₂ : List β) (i : ℕ),
    get? (zipWith f tail✝ l₂) i = some z ↔ ∃ x y, get? tail✝ i = some x ∧ get? l₂ i = some y ∧ f x y = z
l₂ : List β
i : ℕ
⊢ get? (zipWith f (head✝ :: tail✝) l₂) i = some z ↔
    ∃ x y, get? (head✝ :: tail✝) i = some x ∧ get? l₂ i = some y ∧ f x y = z
cases l₂ <;> simp only [zipWith, get?, exists_false, and_false_iff, false_and_iff]
no goals
case cons.cons
α✝ : Type u
β✝ : Type ?u.112193
γ✝ : Type ?u.112196
δ : Type ?u.112199
ε : Type ?u.112202
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
z : γ
head✝¹ : α
tail✝¹ : List α
tail_ih✝ :
  ∀ (l₂ : List β) (i : ℕ),
    get? (zipWith f tail✝¹ l₂) i = some z ↔ ∃ x y, get? tail✝¹ i = some x ∧ get? l₂ i = some y ∧ f x y = z
i : ℕ
head✝ : β
tail✝ : List β
⊢ get? (f head✝¹ head✝ :: zipWith f tail✝¹ tail✝) i = some z ↔
    ∃ x y, get? (head✝¹ :: tail✝¹) i = some x ∧ get? (head✝ :: tail✝) i = some y ∧ f x y = z
cases i <;> simp [*]