case mk
α : Type u
β : Type u_1
γ : Type ?u.155522
δ : Type ?u.155525
ε : Type ?u.155528
l₁ : List α
l₂ : List β
i : ℕ
fst✝ : α
snd✝ : β
⊢ get? (zip l₁ l₂) i = some (fst✝, snd✝) ↔ get? l₁ i = some (fst✝, snd✝).fst ∧ get? l₂ i = some (fst✝, snd✝).snd
α : Type u
β : Type u_1
γ : Type ?u.155522
δ : Type ?u.155525
ε : Type ?u.155528
l₁ : List α
l₂ : List β
z : α × β
i : ℕ
⊢ get? (zip l₁ l₂) i = some z ↔ get? l₁ i = some z.fst ∧ get? l₂ i = some z.snd
cases z
case mk
α : Type u
β : Type u_1
γ : Type ?u.155522
δ : Type ?u.155525
ε : Type ?u.155528
l₁ : List α
l₂ : List β
i : ℕ
fst✝ : α
snd✝ : β
⊢ (∃ x y, get? l₁ i = some x ∧ get? l₂ i = some y ∧ (x, y) = (fst✝, snd✝)) ↔
    get? l₁ i = some (fst✝, snd✝).fst ∧ get? l₂ i = some (fst✝, snd✝).snd
case mk
α : Type u
β : Type u_1
γ : Type ?u.155522
δ : Type ?u.155525
ε : Type ?u.155528
l₁ : List α
l₂ : List β
i : ℕ
fst✝ : α
snd✝ : β
⊢ get? (zip l₁ l₂) i = some (fst✝, snd✝) ↔ get? l₁ i = some (fst✝, snd✝).fst ∧ get? l₂ i = some (fst✝, snd✝).snd
rw [zip, get?_zip_with_eq_some]
case mk.mp
α : Type u
β : Type u_1
γ : Type ?u.155522
δ : Type ?u.155525
ε : Type ?u.155528
l₁ : List α
l₂ : List β
i : ℕ
fst✝ : α
snd✝ : β
⊢ (∃ x y, get? l₁ i = some x ∧ get? l₂ i = some y ∧ (x, y) = (fst✝, snd✝)) →
    get? l₁ i = some (fst✝, snd✝).fst ∧ get? l₂ i = some (fst✝, snd✝).snd

case mk.mpr
α : Type u
β : Type u_1
γ : Type ?u.155522
δ : Type ?u.155525
ε : Type ?u.155528
l₁ : List α
l₂ : List β
i : ℕ
fst✝ : α
snd✝ : β
⊢ get? l₁ i = some (fst✝, snd✝).fst ∧ get? l₂ i = some (fst✝, snd✝).snd →
    ∃ x y, get? l₁ i = some x ∧ get? l₂ i = some y ∧ (x, y) = (fst✝, snd✝)
case mk
α : Type u
β : Type u_1
γ : Type ?u.155522
δ : Type ?u.155525
ε : Type ?u.155528
l₁ : List α
l₂ : List β
i : ℕ
fst✝ : α
snd✝ : β
⊢ (∃ x y, get? l₁ i = some x ∧ get? l₂ i = some y ∧ (x, y) = (fst✝, snd✝)) ↔
    get? l₁ i = some (fst✝, snd✝).fst ∧ get? l₂ i = some (fst✝, snd✝).snd
constructor
case mk.mp.intro.intro.intro.intro
α : Type u
β : Type u_1
γ : Type ?u.155522
δ : Type ?u.155525
ε : Type ?u.155528
l₁ : List α
l₂ : List β
i : ℕ
fst✝ : α
snd✝ : β
x : α
y : β
h₀ : get? l₁ i = some x
h₁ : get? l₂ i = some y
h₂ : (x, y) = (fst✝, snd✝)
⊢ get? l₁ i = some (fst✝, snd✝).fst ∧ get? l₂ i = some (fst✝, snd✝).snd
case mk.mp
α : Type u
β : Type u_1
γ : Type ?u.155522
δ : Type ?u.155525
ε : Type ?u.155528
l₁ : List α
l₂ : List β
i : ℕ
fst✝ : α
snd✝ : β
⊢ (∃ x y, get? l₁ i = some x ∧ get? l₂ i = some y ∧ (x, y) = (fst✝, snd✝)) →
    get? l₁ i = some (fst✝, snd✝).fst ∧ get? l₂ i = some (fst✝, snd✝).snd
rintro ⟨x, y, h₀, h₁, h₂⟩
no goals
case mk.mp.intro.intro.intro.intro
α : Type u
β : Type u_1
γ : Type ?u.155522
δ : Type ?u.155525
ε : Type ?u.155528
l₁ : List α
l₂ : List β
i : ℕ
fst✝ : α
snd✝ : β
x : α
y : β
h₀ : get? l₁ i = some x
h₁ : get? l₂ i = some y
h₂ : (x, y) = (fst✝, snd✝)
⊢ get? l₁ i = some (fst✝, snd✝).fst ∧ get? l₂ i = some (fst✝, snd✝).snd
simpa [h₀, h₁] using h₂
case mk.mpr.intro
α : Type u
β : Type u_1
γ : Type ?u.155522
δ : Type ?u.155525
ε : Type ?u.155528
l₁ : List α
l₂ : List β
i : ℕ
fst✝ : α
snd✝ : β
h₀ : get? l₁ i = some (fst✝, snd✝).fst
h₁ : get? l₂ i = some (fst✝, snd✝).snd
⊢ ∃ x y, get? l₁ i = some x ∧ get? l₂ i = some y ∧ (x, y) = (fst✝, snd✝)
case mk.mpr
α : Type u
β : Type u_1
γ : Type ?u.155522
δ : Type ?u.155525
ε : Type ?u.155528
l₁ : List α
l₂ : List β
i : ℕ
fst✝ : α
snd✝ : β
⊢ get? l₁ i = some (fst✝, snd✝).fst ∧ get? l₂ i = some (fst✝, snd✝).snd →
    ∃ x y, get? l₁ i = some x ∧ get? l₂ i = some y ∧ (x, y) = (fst✝, snd✝)
rintro ⟨h₀, h₁⟩
no goals
case mk.mpr.intro
α : Type u
β : Type u_1
γ : Type ?u.155522
δ : Type ?u.155525
ε : Type ?u.155528
l₁ : List α
l₂ : List β
i : ℕ
fst✝ : α
snd✝ : β
h₀ : get? l₁ i = some (fst✝, snd✝).fst
h₁ : get? l₂ i = some (fst✝, snd✝).snd
⊢ ∃ x y, get? l₁ i = some x ∧ get? l₂ i = some y ∧ (x, y) = (fst✝, snd✝)
exact ⟨_, _, h₀, h₁, rfl⟩