-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Zip.lean
theorem getElem?_zip_eq_some {l₁ : List α} {l₂ : List β} {z : α × β} {i : Nat} :
    (zip l₁ l₂)[i]? = some z ↔ l₁[i]? = some z.1 ∧ l₂[i]? = some z.2

Proof state:
case mk
α : Type u_1
β : Type u_2
l₁ : List α
l₂ : List β
i : Nat
fst✝ : α
snd✝ : β
⊢ (l₁.zip l₂)[i]? = some (fst✝, snd✝) ↔ l₁[i]? = some (fst✝, snd✝).fst ∧ l₂[i]? = some (fst✝, snd✝).snd

Tactic:
rw [zip, getElem?_zipWith_eq_some]

Result:
case mk
α : Type u_1
β : Type u_2
l₁ : List α
l₂ : List β
i : Nat
fst✝ : α
snd✝ : β
⊢ (∃ x y, l₁[i]? = some x ∧ l₂[i]? = some y ∧ (x, y) = (fst✝, snd✝)) ↔
    l₁[i]? = some (fst✝, snd✝).fst ∧ l₂[i]? = some (fst✝, snd✝).snd

Proof state:
case mk.mp
α : Type u_1
β : Type u_2
l₁ : List α
l₂ : List β
i : Nat
fst✝ : α
snd✝ : β
⊢ (∃ x y, l₁[i]? = some x ∧ l₂[i]? = some y ∧ (x, y) = (fst✝, snd✝)) →
    l₁[i]? = some (fst✝, snd✝).fst ∧ l₂[i]? = some (fst✝, snd✝).snd

Tactic:
rintro ⟨x, y, h₀, h₁, h₂⟩

Result:
case mk.mp.intro.intro.intro.intro
α : Type u_1
β : Type u_2
l₁ : List α
l₂ : List β
i : Nat
fst✝ : α
snd✝ : β
x : α
y : β
h₀ : l₁[i]? = some x
h₁ : l₂[i]? = some y
h₂ : (x, y) = (fst✝, snd✝)
⊢ l₁[i]? = some (fst✝, snd✝).fst ∧ l₂[i]? = some (fst✝, snd✝).snd

Proof state:
case mk.mpr.intro
α : Type u_1
β : Type u_2
l₁ : List α
l₂ : List β
i : Nat
fst✝ : α
snd✝ : β
h₀ : l₁[i]? = some (fst✝, snd✝).fst
h₁ : l₂[i]? = some (fst✝, snd✝).snd
⊢ ∃ x y, l₁[i]? = some x ∧ l₂[i]? = some y ∧ (x, y) = (fst✝, snd✝)

Tactic:
exact ⟨_, _, h₀, h₁, rfl⟩

Result:
no goals

Proof state:
case mk
α : Type u_1
β : Type u_2
l₁ : List α
l₂ : List β
i : Nat
fst✝ : α
snd✝ : β
⊢ (∃ x y, l₁[i]? = some x ∧ l₂[i]? = some y ∧ (x, y) = (fst✝, snd✝)) ↔
    l₁[i]? = some (fst✝, snd✝).fst ∧ l₂[i]? = some (fst✝, snd✝).snd

Tactic:
constructor

Result:
case mk.mp
α : Type u_1
β : Type u_2
l₁ : List α
l₂ : List β
i : Nat
fst✝ : α
snd✝ : β
⊢ (∃ x y, l₁[i]? = some x ∧ l₂[i]? = some y ∧ (x, y) = (fst✝, snd✝)) →
    l₁[i]? = some (fst✝, snd✝).fst ∧ l₂[i]? = some (fst✝, snd✝).snd

case mk.mpr
α : Type u_1
β : Type u_2
l₁ : List α
l₂ : List β
i : Nat
fst✝ : α
snd✝ : β
⊢ l₁[i]? = some (fst✝, snd✝).fst ∧ l₂[i]? = some (fst✝, snd✝).snd →
    ∃ x y, l₁[i]? = some x ∧ l₂[i]? = some y ∧ (x, y) = (fst✝, snd✝)

Proof state:
α : Type u_1
β : Type u_2
l₁ : List α
l₂ : List β
z : α × β
i : Nat
⊢ (l₁.zip l₂)[i]? = some z ↔ l₁[i]? = some z.fst ∧ l₂[i]? = some z.snd

Tactic:
cases z

Result:
case mk
α : Type u_1
β : Type u_2
l₁ : List α
l₂ : List β
i : Nat
fst✝ : α
snd✝ : β
⊢ (l₁.zip l₂)[i]? = some (fst✝, snd✝) ↔ l₁[i]? = some (fst✝, snd✝).fst ∧ l₂[i]? = some (fst✝, snd✝).snd

Proof state:
case mk.mpr
α : Type u_1
β : Type u_2
l₁ : List α
l₂ : List β
i : Nat
fst✝ : α
snd✝ : β
⊢ l₁[i]? = some (fst✝, snd✝).fst ∧ l₂[i]? = some (fst✝, snd✝).snd →
    ∃ x y, l₁[i]? = some x ∧ l₂[i]? = some y ∧ (x, y) = (fst✝, snd✝)

Tactic:
rintro ⟨h₀, h₁⟩

Result:
case mk.mpr.intro
α : Type u_1
β : Type u_2
l₁ : List α
l₂ : List β
i : Nat
fst✝ : α
snd✝ : β
h₀ : l₁[i]? = some (fst✝, snd✝).fst
h₁ : l₂[i]? = some (fst✝, snd✝).snd
⊢ ∃ x y, l₁[i]? = some x ∧ l₂[i]? = some y ∧ (x, y) = (fst✝, snd✝)

Proof state:
case mk.mp.intro.intro.intro.intro
α : Type u_1
β : Type u_2
l₁ : List α
l₂ : List β
i : Nat
fst✝ : α
snd✝ : β
x : α
y : β
h₀ : l₁[i]? = some x
h₁ : l₂[i]? = some y
h₂ : (x, y) = (fst✝, snd✝)
⊢ l₁[i]? = some (fst✝, snd✝).fst ∧ l₂[i]? = some (fst✝, snd✝).snd

Tactic:
simpa [h₀, h₁] using h₂

Result:
no goals