awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (goal)
Goal:
α : Type u
inst : DecidableEq α
xs : List (α × α)
x y z : α
pos : y = x → (some z).getD x = z
⊢ Option.getD (if h : y = x then some z else dlookup (β := fun (x : α) ↦ α) x (map Prod.toSigma xs)) x =
    if y = x then z else (dlookup (β := fun (x : α) ↦ α) x (map Prod.toSigma xs)).getD x
have neg : ¬y = x →
  (dlookup (β := fun (x : α) ↦ α) x (map Prod.toSigma xs)).getD x =
    (dlookup (β := fun (x : α) ↦ α) x (map Prod.toSigma xs)).getD x
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (goal)
Goal:
α : Type u
inst : DecidableEq α
x y x' : α
xs : List α
xs_ih :
  ∀ {ys : List α} (h₀ : xs.Nodup) (h₁ : xs.length = ys.length) (i : ℕ)
    (h₂ : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs i = some x),
    applyId (xs.zip ys) x = y ↔ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) ys i = some y
ys : List α
h₀ : (x' :: xs).Nodup
h₁ : (x' :: xs).length = ys.length
i : ℕ
h₂ : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x' :: xs) i = some x
⊢ applyId ((x' :: xs).zip ys) x = y ↔ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) ys i = some y
have cons : ∀ (h₂ : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x' :: xs) 0 = some x),
  applyId ((x' :: xs).zip ys) x = y ↔ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) ys 0 = some y
Tactic: cases i
Cleared hypotheses: i, h₂
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (goal)
Goal:
α : Type u
inst : DecidableEq α
x y x' : α
xs : List α
xs_ih :
  ∀ {ys : List α} (h₀ : xs.Nodup) (h₁ : xs.length = ys.length) (i : ℕ)
    (h₂ : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs i = some x),
    applyId (xs.zip ys) x = y ↔ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) ys i = some y
ys : List α
h₀ : (x' :: xs).Nodup
h₁ : (x' :: xs).length = ys.length
i : ℕ
h₂ : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x' :: xs) i = some x
cons :
  ∀ (h₂ : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x' :: xs) 0 = some x),
    applyId ((x' :: xs).zip ys) x = y ↔ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) ys 0 = some y
⊢ applyId ((x' :: xs).zip ys) x = y ↔ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) ys i = some y
have cons₁ : ∀ (n : ℕ) (h₂ : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x' :: xs) (n + 1) = some x),
  applyId ((x' :: xs).zip ys) x = y ↔ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) ys (n + 1) = some y
Tactic: cases i
Cleared hypotheses: i, h₂
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (hypothesis)
Goal:
α : Type u
inst : DecidableEq α
x y x' : α
xs : List α
xs_ih :
  ∀ {ys : List α} (h₀ : xs.Nodup) (h₁ : xs.length = ys.length) (i : ℕ)
    (h₂ : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs i = some x),
    applyId (xs.zip ys) x = y ↔ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) ys i = some y
ys : List α
h₀ : (x' :: xs).Nodup
h₁ : (x' :: xs).length = ys.length
h₂ : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x' :: xs) 0 = some x
⊢ applyId ((x' :: xs).zip ys) x = y ↔ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) ys 0 = some y
have h₃ : x' = x
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₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (goal)
Goal:
α : Type u
inst : DecidableEq α
x y x' : α
xs : List α
xs_ih :
  ∀ {ys : List α} (h₀ : xs.Nodup) (h₁ : xs.length = ys.length) (i : ℕ)
    (h₂ : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs i = some x),
    applyId (xs.zip ys) x = y ↔ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) 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 ↔ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) ys 0 = some y
have cons : ∀
  (xs_ih :
    ∀ {ys : List α} (h₀ : xs.Nodup) (h₁ : xs.length = ys.length) (i : ℕ)
      (h₂ : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs i = some x'),
      applyId (xs.zip ys) x' = y ↔ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) ys i = some y),
  applyId ((x' :: xs).zip ys) x' = y ↔ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) ys 0 = some y
Tactic: subst h₂
Cleared hypotheses: x, xs_ih, h₂
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (goal)
Goal:
α : Type u
inst : DecidableEq α
y x' : α
xs ys : List α
h₀ : (x' :: xs).Nodup
h₁ : (x' :: xs).length = ys.length
xs_ih :
  ∀ {ys : List α} (h₀ : xs.Nodup) (h₁ : xs.length = ys.length) (i : ℕ)
    (h₂ : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs i = some x'),
    applyId (xs.zip ys) x' = y ↔ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) ys i = some y
⊢ applyId ((x' :: xs).zip ys) x' = y ↔ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) ys 0 = some y
have cons : ∀ (h₁ : (x' :: xs).length = length.{u} (α := α) []),
  applyId ((x' :: xs).zip []) x' = y ↔ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [] 0 = some y
Tactic: cases ys
Cleared hypotheses: ys, h₁
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (goal)
Goal:
α : Type u
inst : DecidableEq α
y x' : α
xs ys : List α
h₀ : (x' :: xs).Nodup
h₁ : (x' :: xs).length = ys.length
xs_ih :
  ∀ {ys : List α} (h₀ : xs.Nodup) (h₁ : xs.length = ys.length) (i : ℕ)
    (h₂ : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs i = some x'),
    applyId (xs.zip ys) x' = y ↔ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) ys i = some y
cons :
  ∀ (h₁ : (x' :: xs).length = length.{u} (α := α) []),
    applyId ((x' :: xs).zip []) x' = y ↔ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [] 0 = some y
⊢ applyId ((x' :: xs).zip ys) x' = y ↔ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) ys 0 = some y
have cons₁ : ∀ (head : α) (tail : List α) (h₁ : (x' :: xs).length = (head :: tail).length),
  applyId ((x' :: xs).zip (head :: tail)) x' = y ↔
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (head :: tail) 0 = some y
Tactic: cases ys
Cleared hypotheses: ys, h₁
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (goal)
Goal:
α : Type u
inst : DecidableEq α
x y x' : α
xs : List α
xs_ih :
  ∀ {ys : List α} (h₀ : xs.Nodup) (h₁ : xs.length = ys.length) (i : ℕ)
    (h₂ : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs i = some x),
    applyId (xs.zip ys) x = y ↔ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) ys i = some y
ys : List α
h₀ : (x' :: xs).Nodup
h₁ : (x' :: xs).length = ys.length
n : ℕ
h₂ : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x' :: xs) (n + 1) = some x
⊢ applyId ((x' :: xs).zip ys) x = y ↔ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) ys (n + 1) = some y
have cons : ∀ (h₁ : (x' :: xs).length = length.{u} (α := α) []),
  applyId ((x' :: xs).zip []) x = y ↔ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [] (n + 1) = some y
Tactic: cases ys
Cleared hypotheses: ys, h₁
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (goal)
Goal:
α : Type u
inst : DecidableEq α
x y x' : α
xs : List α
xs_ih :
  ∀ {ys : List α} (h₀ : xs.Nodup) (h₁ : xs.length = ys.length) (i : ℕ)
    (h₂ : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs i = some x),
    applyId (xs.zip ys) x = y ↔ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) ys i = some y
ys : List α
h₀ : (x' :: xs).Nodup
h₁ : (x' :: xs).length = ys.length
n : ℕ
h₂ : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x' :: xs) (n + 1) = some x
cons :
  ∀ (h₁ : (x' :: xs).length = length.{u} (α := α) []),
    applyId ((x' :: xs).zip []) x = y ↔
      getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [] (n + 1) = some y
⊢ applyId ((x' :: xs).zip ys) x = y ↔ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) ys (n + 1) = some y
have cons₁ : ∀ (head : α) (tail : List α) (h₁ : (x' :: xs).length = (head :: tail).length),
  applyId ((x' :: xs).zip (head :: tail)) x = y ↔
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (head :: tail) (n + 1) = some y
Tactic: cases ys
Cleared hypotheses: ys, h₁
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (hypothesis)
Goal:
α : Type u
inst : DecidableEq α
x y x' : α
xs : List α
xs_ih :
  ∀ {ys : List α} (h₀ : xs.Nodup) (h₁ : xs.length = ys.length) (i : ℕ)
    (h₂ : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs i = some x),
    applyId (xs.zip ys) x = y ↔ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) ys i = some y
h₀ : (x' :: xs).Nodup
n : ℕ
h₂ : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x' :: xs) (n + 1) = some x
head : α
tail : List α
h₁ : (x' :: xs).length = (head :: tail).length
⊢ applyId ((x' :: xs).zip (head :: tail)) x = y ↔
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (head :: tail) (n + 1) = some y
have h₃ : List.Pairwise (fun (x1 x2 : α) ↦ x1 ≠ x2) xs
Tactic: obtain - | ⟨h₀, h₁⟩ := h₀
Cleared hypotheses: h₀
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (hypothesis)
Goal:
α : Type u
inst : DecidableEq α
x y x' : α
xs : List α
xs_ih :
  ∀ {ys : List α} (h₀ : xs.Nodup) (h₁ : xs.length = ys.length) (i : ℕ)
    (h₂ : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs i = some x),
    applyId (xs.zip ys) x = y ↔ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) ys i = some y
h₀ : (x' :: xs).Nodup
n : ℕ
h₂ : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (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
⊢ applyId ((x' :: xs).zip (head :: tail)) x = y ↔
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (head :: tail) (n + 1) = some y
have h₄ : ∀ a' ∈ xs, x' ≠ a'
Tactic: obtain - | ⟨h₀, h₁⟩ := h₀
Cleared hypotheses: h₀
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (goal)
Goal:
α : Type u
inst : DecidableEq α
x y x' : α
xs : List α
xs_ih :
  ∀ {ys : List α} (h₀ : xs.Nodup) (h₁ : xs.length = ys.length) (i : ℕ)
    (h₂ : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs i = some x),
    applyId (xs.zip ys) x = y ↔ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) ys i = some y
n : ℕ
h₂ : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x' :: xs) (n + 1) = some x
head : α
tail : List α
h₁_1 : (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 ↔
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (head :: tail) (n + 1) = some y
have cons : (if x' = x then head else applyId (xs.zip tail) x) = y ↔
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) tail n = some y
Tactic: simp only [getElem?_cons_succ, zip_cons_cons, applyId_cons] at h₂ ⊢
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (goal)
Goal:
α : Type u
inst : DecidableEq α
x y x' : α
xs : List α
xs_ih :
  ∀ {ys : List α} (h₀ : xs.Nodup) (h₁ : xs.length = ys.length) (i : ℕ)
    (h₂ : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs i = some x),
    applyId (xs.zip ys) x = y ↔ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) ys i = some y
n : ℕ
h₂ : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs n = some x
head : α
tail : List α
h₁_1 : (x' :: xs).length = (head :: tail).length
h₁ : List.Pairwise (fun (x1 x2 : α) ↦ x1 ≠ x2) xs
h₀ : ∀ a' ∈ xs, x' ≠ a'
⊢ (if x' = x then head else applyId (xs.zip tail) x) = y ↔
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) tail n = some y
have cons : applyId (xs.zip tail) x = y ↔ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) tail n = some y
Tactic: rw [if_neg]
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (goal)
Goal:
α : Type u
inst : DecidableEq α
x y x' : α
xs : List α
xs_ih :
  ∀ {ys : List α} (h₀ : xs.Nodup) (h₁ : xs.length = ys.length) (i : ℕ)
    (h₂ : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs i = some x),
    applyId (xs.zip ys) x = y ↔ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) ys i = some y
n : ℕ
h₂ : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs n = some x
head : α
tail : List α
h₁_1 : (x' :: xs).length = (head :: tail).length
h₁ : List.Pairwise (fun (x1 x2 : α) ↦ x1 ≠ x2) xs
h₀ : ∀ a' ∈ xs, x' ≠ a'
cons : applyId (xs.zip tail) x = y ↔ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) tail n = some y
⊢ (if x' = x then head else applyId (xs.zip tail) x) = y ↔
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) tail n = some y
have cons₁ : ¬x' = x
Tactic: rw [if_neg]
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (goal)
Goal:
α : Type u
inst : DecidableEq α
x y x' : α
xs : List α
xs_ih :
  ∀ {ys : List α} (h₀ : xs.Nodup) (h₁ : xs.length = ys.length) (i : ℕ)
    (h₂ : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs i = some x),
    applyId (xs.zip ys) x = y ↔ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) ys i = some y
n : ℕ
h₂ : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs n = some x
head : α
tail : List α
h₁_1 : (x' :: xs).length = (head :: tail).length
h₁ : List.Pairwise (fun (x1 x2 : α) ↦ x1 ≠ x2) xs
h₀ : ∀ a' ∈ xs, x' ≠ a'
⊢ applyId (xs.zip tail) x = y ↔ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) tail n = some y
have cons : xs.Nodup
Tactic: apply xs_ih
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (goal)
Goal:
α : Type u
inst : DecidableEq α
x y x' : α
xs : List α
xs_ih :
  ∀ {ys : List α} (h₀ : xs.Nodup) (h₁ : xs.length = ys.length) (i : ℕ)
    (h₂ : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs i = some x),
    applyId (xs.zip ys) x = y ↔ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) ys i = some y
n : ℕ
h₂ : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs n = some x
head : α
tail : List α
h₁_1 : (x' :: xs).length = (head :: tail).length
h₁ : List.Pairwise (fun (x1 x2 : α) ↦ x1 ≠ x2) xs
h₀ : ∀ a' ∈ xs, x' ≠ a'
cons : xs.Nodup
⊢ applyId (xs.zip tail) x = y ↔ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) tail n = some y
have cons₁ : xs.length = tail.length
Tactic: apply xs_ih
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (goal)
Goal:
α : Type u
inst : DecidableEq α
x y x' : α
xs : List α
xs_ih :
  ∀ {ys : List α} (h₀ : xs.Nodup) (h₁ : xs.length = ys.length) (i : ℕ)
    (h₂ : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs i = some x),
    applyId (xs.zip ys) x = y ↔ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) ys i = some y
n : ℕ
h₂ : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs n = some x
head : α
tail : List α
h₁_1 : (x' :: xs).length = (head :: tail).length
h₁ : List.Pairwise (fun (x1 x2 : α) ↦ x1 ≠ x2) xs
h₀ : ∀ a' ∈ xs, x' ≠ a'
⊢ ¬x' = x
have cons : x ∈ xs
Tactic: apply h₀
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (goal)
Goal:
α : Type u
inst : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs.length = ys.length
x y : α
i : ℕ
h₂ : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs i = some x
⊢ applyId (xs.zip ys) x = y ↔ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) ys i = some y
have nil : ∀ {ys : List α} (h₀ : Nodup.{u} (α := α) []) (h₁ : length.{u} (α := α) [] = ys.length) (i : ℕ)
  (h₂ : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [] i = some x),
  applyId (zip [] ys) x = y ↔ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) ys i = some y
Tactic: induction xs generalizing ys i with
  | nil => cases h₂
  | cons x' xs xs_ih =>
    cases i
    · 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₂
      subst h₂
      cases ys
      · cases h₁
      · simp
    · cases ys
      · cases h₁
      · obtain - | ⟨h₀, h₁⟩ := h₀
        simp only [getElem?_cons_succ, zip_cons_cons, applyId_cons] at h₂ ⊢
        rw [if_neg]
        · apply xs_ih <;> solve_by_elim [Nat.succ.inj]
        · apply h₀; apply List.mem_of_getElem? h₂
Cleared hypotheses: xs, ys, h₀, h₁, i, h₂
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (goal)
Goal:
α : Type u
inst : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs.length = ys.length
x y : α
i : ℕ
h₂ : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs i = some x
nil :
  ∀ {ys : List α} (h₀ : Nodup.{u} (α := α) []) (h₁ : length.{u} (α := α) [] = ys.length) (i : ℕ)
    (h₂ : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [] i = some x),
    applyId (zip [] ys) x = y ↔ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) ys i = some y
⊢ applyId (xs.zip ys) x = y ↔ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) ys i = some y
have cons : ∀ (x' : α) (xs : List α)
  (xs_ih :
    ∀ {ys : List α} (h₀ : xs.Nodup) (h₁ : xs.length = ys.length) (i : ℕ)
      (h₂ : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs i = some x),
      applyId (xs.zip ys) x = y ↔ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) ys i = some y)
  {ys : List α} (h₀ : (x' :: xs).Nodup) (h₁ : (x' :: xs).length = ys.length) (i : ℕ)
  (h₂ : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x' :: xs) i = some x),
  applyId ((x' :: xs).zip ys) x = y ↔ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) ys i = some y
Tactic: induction xs generalizing ys i with
  | nil => cases h₂
  | cons x' xs xs_ih =>
    cases i
    · 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₂
      subst h₂
      cases ys
      · cases h₁
      · simp
    · cases ys
      · cases h₁
      · obtain - | ⟨h₀, h₁⟩ := h₀
        simp only [getElem?_cons_succ, zip_cons_cons, applyId_cons] at h₂ ⊢
        rw [if_neg]
        · apply xs_ih <;> solve_by_elim [Nat.succ.inj]
        · apply h₀; apply List.mem_of_getElem? h₂
Cleared hypotheses: xs, ys, h₀, h₁, i, h₂
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (goal)
Goal:
α : Type u
inst : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x : α
h₃ : dlookup (β := fun (x : α) ↦ α) x (map Prod.toSigma (xs.zip ys)) = none
⊢ Option.getD none x ∈ ys ↔ x ∈ xs
have none : x ∈ ys ↔ x ∈ xs
Tactic: dsimp [Option.getD]
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (goal)
Goal:
α : Type u
inst : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x : α
h₃ : dlookup (β := fun (x : α) ↦ α) x (map Prod.toSigma (xs.zip ys)) = none
⊢ x ∈ ys ↔ x ∈ xs
have none : x ∈ ys ↔ x ∈ ys
Tactic: rw [h₁.mem_iff]
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (hypothesis)
Goal:
α : Type u
inst : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x val : α
h₃ : dlookup (β := fun (x : α) ↦ α) x (map Prod.toSigma (xs.zip ys)) = some val
⊢ (some val).getD x ∈ ys ↔ x ∈ xs
have h₂ : ys.Nodup
Tactic: have h₂ : ys.Nodup := h₁.nodup_iff.1 h₀
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (hypothesis)
Goal:
α : Type u
inst : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x val : α
h₃ : dlookup (β := fun (x : α) ↦ α) x (map Prod.toSigma (xs.zip ys)) = some val
h₂ : ys.Nodup
⊢ (some val).getD x ∈ ys ↔ x ∈ xs
have h₄ : xs.length = ys.length
Tactic: replace h₁ : xs.length = ys.length := h₁.length_eq
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (goal)
Goal:
α : Type u
inst : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
x val : α
h₃ : dlookup (β := fun (x : α) ↦ α) x (map Prod.toSigma (xs.zip ys)) = some val
h₂ : ys.Nodup
h₁ : xs.length = ys.length
⊢ (some val).getD x ∈ ys ↔ x ∈ xs
have some : val ∈ ys ↔ x ∈ xs
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (goal)
Goal:
α : Type u
inst : DecidableEq α
x val x' : α
xs : List α
xs_ih :
  ∀ {ys : List α} (h₀ : xs.Nodup) (h₃ : dlookup (β := fun (x : α) ↦ α) x (map Prod.toSigma (xs.zip ys)) = some val)
    (h₂ : ys.Nodup) (h₁ : xs.length = ys.length), val ∈ ys ↔ x ∈ xs
ys : List α
h₀ : (x' :: xs).Nodup
h₃ : dlookup (β := fun (x : α) ↦ α) x (map Prod.toSigma ((x' :: xs).zip ys)) = some val
h₂ : ys.Nodup
h₁ : (x' :: xs).length = ys.length
⊢ val ∈ ys ↔ x ∈ x' :: xs
have some : ∀ (h₃ : dlookup (β := fun (x : α) ↦ α) x (map Prod.toSigma ((x' :: xs).zip [])) = some val) (h₂ : Nodup.{u} (α := α) [])
  (h₁ : (x' :: xs).length = length.{u} (α := α) []), Membership.mem (γ := List α) [] val ↔ x ∈ x' :: xs
Tactic: rcases ys with - | ⟨y, ys⟩
Cleared hypotheses: ys, h₃, h₂, h₁
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (goal)
Goal:
α : Type u
inst : DecidableEq α
x val x' : α
xs : List α
xs_ih :
  ∀ {ys : List α} (h₀ : xs.Nodup)
    (h₃ : dlookup (β := fun (x : α) ↦ α) x (map Prod.toSigma (xs.zip ys)) = Option.some val) (h₂ : ys.Nodup)
    (h₁ : xs.length = ys.length), val ∈ ys ↔ x ∈ xs
ys : List α
h₀ : (x' :: xs).Nodup
h₃ : dlookup (β := fun (x : α) ↦ α) x (map Prod.toSigma ((x' :: xs).zip ys)) = Option.some val
h₂ : ys.Nodup
h₁ : (x' :: xs).length = ys.length
some :
  ∀ (h₃ : dlookup (β := fun (x : α) ↦ α) x (map Prod.toSigma ((x' :: xs).zip [])) = Option.some val)
    (h₂ : Nodup.{u} (α := α) []) (h₁ : (x' :: xs).length = length.{u} (α := α) []),
    Membership.mem (γ := List α) [] val ↔ x ∈ x' :: xs
⊢ val ∈ ys ↔ x ∈ x' :: xs
have some₁ : ∀ (y : α) (ys : List α)
  (h₃ : dlookup (β := fun (x : α) ↦ α) x (map Prod.toSigma ((x' :: xs).zip (y :: ys))) = Option.some val)
  (h₂ : (y :: ys).Nodup) (h₁ : (x' :: xs).length = (y :: ys).length), val ∈ y :: ys ↔ x ∈ x' :: xs
Tactic: rcases ys with - | ⟨y, ys⟩
Cleared hypotheses: ys, h₃, h₂, h₁
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (goal)
Goal:
α : Type u
inst : DecidableEq α
x val x' : α
xs : List α
xs_ih :
  ∀ {ys : List α} (h₀ : xs.Nodup) (h₃ : dlookup (β := fun (x : α) ↦ α) x (map Prod.toSigma (xs.zip ys)) = some val)
    (h₂ : ys.Nodup) (h₁ : xs.length = ys.length), val ∈ ys ↔ x ∈ xs
h₀ : (x' :: xs).Nodup
y : α
ys : List α
h₃ :
  (if h : x' = x then some (Eq.rec (motive := fun (x : α) (x_1 : x' = x) ↦ α) y h)
    else dlookup (β := fun (x : α) ↦ α) x (map Prod.toSigma (xs.zip ys))) =
    some val
h₂ : (y :: ys).Nodup
h₁ : (x' :: xs).length = (y :: ys).length
⊢ val ∈ y :: ys ↔ x ∈ x' :: xs
have pos : ∀ (h : x' = x) (h₃ : some (Eq.rec (motive := fun (x : α) (x_1 : x' = x) ↦ α) y h) = some val),
  val ∈ y :: ys ↔ x ∈ x' :: xs
Tactic: split_ifs at h₃ with h
Cleared hypotheses: h₃
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (goal)
Goal:
α : Type u
inst : DecidableEq α
x val x' : α
xs : List α
xs_ih :
  ∀ {ys : List α} (h₀ : xs.Nodup) (h₃ : dlookup (β := fun (x : α) ↦ α) x (map Prod.toSigma (xs.zip ys)) = some val)
    (h₂ : ys.Nodup) (h₁ : xs.length = ys.length), val ∈ ys ↔ x ∈ xs
h₀ : (x' :: xs).Nodup
y : α
ys : List α
h₃ :
  (if h : x' = x then some (Eq.rec (motive := fun (x : α) (x_1 : x' = x) ↦ α) y h)
    else dlookup (β := fun (x : α) ↦ α) x (map Prod.toSigma (xs.zip ys))) =
    some val
h₂ : (y :: ys).Nodup
h₁ : (x' :: xs).length = (y :: ys).length
pos :
  ∀ (h : x' = x) (h₃ : some (Eq.rec (motive := fun (x : α) (x_1 : x' = x) ↦ α) y h) = some val),
    val ∈ y :: ys ↔ x ∈ x' :: xs
⊢ val ∈ y :: ys ↔ x ∈ x' :: xs
have neg : ∀ (h : ¬x' = x) (h₃ : dlookup (β := fun (x : α) ↦ α) x (map Prod.toSigma (xs.zip ys)) = some val),
  val ∈ y :: ys ↔ x ∈ x' :: xs
Tactic: split_ifs at h₃ with h
Cleared hypotheses: h₃