-- Mathlib/Testing/Plausible/Functions.lean
theorem List.applyId_zip_eq [DecidableEq α] {xs ys : List α} (h₀ : List.Nodup xs)
    (h₁ : xs.length = ys.length) (x y : α) (i : ℕ) (h₂ : xs[i]? = some x) :
    List.applyId.{u} (xs.zip ys) x = y ↔ ys[i]? = some y

Proof state:
case cons.zero.cons
α : Type u
inst✝ : DecidableEq α
y x' : α
xs : List α
h₀ : (x' :: xs).Nodup
xs_ih :
  ∀ {ys : List α},
    xs.Nodup → xs.length = ys.length → ∀ (i : ℕ), xs[i]? = some x' → (applyId (xs.zip ys) x' = y ↔ ys[i]? = some y)
head✝ : α
tail✝ : List α
h₁ : (x' :: xs).length = (head✝ :: tail✝).length
⊢ applyId ((x' :: xs).zip (head✝ :: tail✝)) x' = y ↔ (head✝ :: tail✝)[0]? = some y

Tactic:
simp

Result:
no goals

Proof state:
case cons.succ.cons.cons
α : Type u
inst✝ : DecidableEq α
x y x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    xs.Nodup → xs.length = ys.length → ∀ (i : ℕ), xs[i]? = some x → (applyId (xs.zip ys) x = y ↔ ys[i]? = some y)
n✝ : ℕ
h₂ : (x' :: xs)[n✝ + 1]? = some x
head✝ : α
tail✝ : List α
h₁✝ : (x' :: xs).length = (head✝ :: tail✝).length
h₁ : List.Pairwise (fun x1 x2 => x1 ≠ x2) xs
h₀ : ∀ a' ∈ xs, x' ≠ a'
⊢ applyId ((x' :: xs).zip (head✝ :: tail✝)) x = y ↔ (head✝ :: tail✝)[n✝ + 1]? = some y

Tactic:
simp only [getElem?_cons_succ, zip_cons_cons, applyId_cons] at h₂ ⊢

Result:
case cons.succ.cons.cons
α : Type u
inst✝ : DecidableEq α
x y x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    xs.Nodup → xs.length = ys.length → ∀ (i : ℕ), xs[i]? = some x → (applyId (xs.zip ys) x = y ↔ ys[i]? = some y)
n✝ : ℕ
head✝ : α
tail✝ : List α
h₁✝ : (x' :: xs).length = (head✝ :: tail✝).length
h₁ : List.Pairwise (fun x1 x2 => x1 ≠ x2) xs
h₀ : ∀ a' ∈ xs, x' ≠ a'
h₂ : xs[n✝]? = some x
⊢ (if x' = x then head✝ else applyId (xs.zip tail✝) x) = y ↔ tail✝[n✝]? = some y

Proof state:
case cons.zero
α : Type u
inst✝ : DecidableEq α
x y x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    xs.Nodup → xs.length = ys.length → ∀ (i : ℕ), xs[i]? = some x → (applyId (xs.zip ys) x = y ↔ ys[i]? = some y)
ys : List α
h₀ : (x' :: xs).Nodup
h₁ : (x' :: xs).length = ys.length
h₂ : x' = x
⊢ applyId ((x' :: xs).zip ys) x = y ↔ ys[0]? = some y

Tactic:
subst h₂

Result:
case cons.zero
α : Type u
inst✝ : DecidableEq α
y x' : α
xs ys : List α
h₀ : (x' :: xs).Nodup
h₁ : (x' :: xs).length = ys.length
xs_ih :
  ∀ {ys : List α},
    xs.Nodup → xs.length = ys.length → ∀ (i : ℕ), xs[i]? = some x' → (applyId (xs.zip ys) x' = y ↔ ys[i]? = some y)
⊢ applyId ((x' :: xs).zip ys) x' = y ↔ ys[0]? = some y

Proof state:
case cons.succ.cons.cons.hnc
α : Type u
inst✝ : DecidableEq α
x y x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    xs.Nodup → xs.length = ys.length → ∀ (i : ℕ), xs[i]? = some x → (applyId (xs.zip ys) x = y ↔ ys[i]? = some y)
n✝ : ℕ
head✝ : α
tail✝ : List α
h₁✝ : (x' :: xs).length = (head✝ :: tail✝).length
h₁ : List.Pairwise (fun x1 x2 => x1 ≠ x2) xs
h₀ : ∀ a' ∈ xs, x' ≠ a'
h₂ : xs[n✝]? = some x
⊢ ¬x' = x

Tactic:
apply h₀

Result:
case cons.succ.cons.cons.hnc.a
α : Type u
inst✝ : DecidableEq α
x y x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    xs.Nodup → xs.length = ys.length → ∀ (i : ℕ), xs[i]? = some x → (applyId (xs.zip ys) x = y ↔ ys[i]? = some y)
n✝ : ℕ
head✝ : α
tail✝ : List α
h₁✝ : (x' :: xs).length = (head✝ :: tail✝).length
h₁ : List.Pairwise (fun x1 x2 => x1 ≠ x2) xs
h₀ : ∀ a' ∈ xs, x' ≠ a'
h₂ : xs[n✝]? = some x
⊢ x ∈ xs

Proof state:
case cons.zero
α : Type u
inst✝ : DecidableEq α
x y x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    xs.Nodup → xs.length = ys.length → ∀ (i : ℕ), xs[i]? = some x → (applyId (xs.zip ys) x = y ↔ ys[i]? = some y)
ys : List α
h₀ : (x' :: xs).Nodup
h₁ : (x' :: xs).length = ys.length
h₂ : (x' :: xs)[0]? = some x
⊢ applyId ((x' :: xs).zip ys) x = y ↔ ys[0]? = some y

Tactic:
simp only [length_cons, lt_add_iff_pos_left, add_pos_iff, Nat.lt_add_one, or_true,
  getElem?_eq_getElem, getElem_cons_zero, Option.some.injEq] at h₂

Result:
case cons.zero
α : Type u
inst✝ : DecidableEq α
x y x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    xs.Nodup → xs.length = ys.length → ∀ (i : ℕ), xs[i]? = some x → (applyId (xs.zip ys) x = y ↔ ys[i]? = some y)
ys : List α
h₀ : (x' :: xs).Nodup
h₁ : (x' :: xs).length = ys.length
h₂ : x' = x
⊢ applyId ((x' :: xs).zip ys) x = y ↔ ys[0]? = some y

Proof state:
case cons.succ.cons
α : Type u
inst✝ : DecidableEq α
x y x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    xs.Nodup → xs.length = ys.length → ∀ (i : ℕ), xs[i]? = some x → (applyId (xs.zip ys) x = y ↔ ys[i]? = some y)
h₀ : (x' :: xs).Nodup
n✝ : ℕ
h₂ : (x' :: xs)[n✝ + 1]? = some x
head✝ : α
tail✝ : List α
h₁ : (x' :: xs).length = (head✝ :: tail✝).length
⊢ applyId ((x' :: xs).zip (head✝ :: tail✝)) x = y ↔ (head✝ :: tail✝)[n✝ + 1]? = some y

Tactic:
obtain - | ⟨h₀, h₁⟩ := h₀

Result:
case cons.succ.cons.cons
α : Type u
inst✝ : DecidableEq α
x y x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    xs.Nodup → xs.length = ys.length → ∀ (i : ℕ), xs[i]? = some x → (applyId (xs.zip ys) x = y ↔ ys[i]? = some y)
n✝ : ℕ
h₂ : (x' :: xs)[n✝ + 1]? = some x
head✝ : α
tail✝ : List α
h₁✝ : (x' :: xs).length = (head✝ :: tail✝).length
h₁ : List.Pairwise (fun x1 x2 => x1 ≠ x2) xs
h₀ : ∀ a' ∈ xs, x' ≠ a'
⊢ applyId ((x' :: xs).zip (head✝ :: tail✝)) x = y ↔ (head✝ :: tail✝)[n✝ + 1]? = some y

Proof state:
case cons.succ.cons.cons
α : Type u
inst✝ : DecidableEq α
x y x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    xs.Nodup → xs.length = ys.length → ∀ (i : ℕ), xs[i]? = some x → (applyId (xs.zip ys) x = y ↔ ys[i]? = some y)
n✝ : ℕ
head✝ : α
tail✝ : List α
h₁✝ : (x' :: xs).length = (head✝ :: tail✝).length
h₁ : List.Pairwise (fun x1 x2 => x1 ≠ x2) xs
h₀ : ∀ a' ∈ xs, x' ≠ a'
h₂ : xs[n✝]? = some x
⊢ applyId (xs.zip tail✝) x = y ↔ tail✝[n✝]? = some y

Tactic:
apply xs_ih <;> solve_by_elim [Nat.succ.inj]

Result:
no goals

Proof state:
case nil
α : Type u
inst✝ : DecidableEq α
x y : α
ys : List α
h₀ : [].Nodup
h₁ : [].length = ys.length
i : ℕ
h₂ : [][i]? = some x
⊢ applyId ([].zip ys) x = y ↔ ys[i]? = some y

Tactic:
cases h₂

Result:
no goals

Proof state:
case cons.succ.cons.cons.hnc.a
α : Type u
inst✝ : DecidableEq α
x y x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    xs.Nodup → xs.length = ys.length → ∀ (i : ℕ), xs[i]? = some x → (applyId (xs.zip ys) x = y ↔ ys[i]? = some y)
n✝ : ℕ
head✝ : α
tail✝ : List α
h₁✝ : (x' :: xs).length = (head✝ :: tail✝).length
h₁ : List.Pairwise (fun x1 x2 => x1 ≠ x2) xs
h₀ : ∀ a' ∈ xs, x' ≠ a'
h₂ : xs[n✝]? = some x
⊢ x ∈ xs

Tactic:
apply List.mem_of_getElem? h₂

Result:
no goals

Proof state:
case cons.succ.cons.cons
α : Type u
inst✝ : DecidableEq α
x y x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    xs.Nodup → xs.length = ys.length → ∀ (i : ℕ), xs[i]? = some x → (applyId (xs.zip ys) x = y ↔ ys[i]? = some y)
n✝ : ℕ
head✝ : α
tail✝ : List α
h₁✝ : (x' :: xs).length = (head✝ :: tail✝).length
h₁ : List.Pairwise (fun x1 x2 => x1 ≠ x2) xs
h₀ : ∀ a' ∈ xs, x' ≠ a'
h₂ : xs[n✝]? = some x
⊢ (if x' = x then head✝ else applyId (xs.zip tail✝) x) = y ↔ tail✝[n✝]? = some y

Tactic:
rw [if_neg]

Result:
case cons.succ.cons.cons
α : Type u
inst✝ : DecidableEq α
x y x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    xs.Nodup → xs.length = ys.length → ∀ (i : ℕ), xs[i]? = some x → (applyId (xs.zip ys) x = y ↔ ys[i]? = some y)
n✝ : ℕ
head✝ : α
tail✝ : List α
h₁✝ : (x' :: xs).length = (head✝ :: tail✝).length
h₁ : List.Pairwise (fun x1 x2 => x1 ≠ x2) xs
h₀ : ∀ a' ∈ xs, x' ≠ a'
h₂ : xs[n✝]? = some x
⊢ applyId (xs.zip tail✝) x = y ↔ tail✝[n✝]? = some y

case cons.succ.cons.cons.hnc
α : Type u
inst✝ : DecidableEq α
x y x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    xs.Nodup → xs.length = ys.length → ∀ (i : ℕ), xs[i]? = some x → (applyId (xs.zip ys) x = y ↔ ys[i]? = some y)
n✝ : ℕ
head✝ : α
tail✝ : List α
h₁✝ : (x' :: xs).length = (head✝ :: tail✝).length
h₁ : List.Pairwise (fun x1 x2 => x1 ≠ x2) xs
h₀ : ∀ a' ∈ xs, x' ≠ a'
h₂ : xs[n✝]? = some x
⊢ ¬x' = x