awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Testing.Plausible.Functions
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
cons₁ : ¬x' = x
⊢ (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:
rw [if_neg]

Premises used: if_neg
-- Module: Mathlib.Testing.Plausible.Functions
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
cons₁ : xs.length = tail.length
cons₂ : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs n = some x
⊢ applyId (xs.zip tail) x = y ↔ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) tail n = some y

Tactic:
apply xs_ih
-- Module: Mathlib.Testing.Plausible.Functions
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'
⊢ xs.Nodup

Tactic:
solve_by_elim [Nat.succ.inj]

Premises used: Nat.succ.inj
-- Module: Mathlib.Testing.Plausible.Functions
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'
⊢ xs.length = tail.length

Tactic:
solve_by_elim [Nat.succ.inj]

Premises used: Nat.succ.inj
-- Module: Mathlib.Testing.Plausible.Functions
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'
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs n = some x

Tactic:
solve_by_elim [Nat.succ.inj]

Premises used: Nat.succ.inj
-- Module: Mathlib.Testing.Plausible.Functions
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 : x ∈ xs
⊢ ¬x' = x

Tactic:
apply h₀
-- Module: Mathlib.Testing.Plausible.Functions
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 ∈ xs

Tactic:
apply List.mem_of_getElem? h₂

Premises used: List.mem_of_getElem?
-- Module: Mathlib.Testing.Plausible.Functions
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
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
⊢ applyId (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₂

Premises used: List.getElem?_cons_succ, List.mem_of_getElem?, List.length_cons, Option.some.injEq, Nat.lt_add_one, Plausible.InjectiveFunction.List.applyId_cons, List.cons, Nat.succ.inj, List.getElem_cons_zero, List.getElem?_eq_getElem, add_pos_iff, or_true, if_neg, lt_add_iff_pos_left, List.nil, List.zip_cons_cons
-- Module: Mathlib.Testing.Plausible.Functions
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)) = Option.none
none : x ∈ ys ↔ x ∈ xs
⊢ Option.getD Option.none x ∈ ys ↔ x ∈ xs

Tactic:
dsimp [Option.getD]

Premises used: Option.getD
-- Module: Mathlib.Testing.Plausible.Functions
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)) = Option.none
none none₁ : x ∈ ys ↔ x ∈ ys
⊢ x ∈ ys ↔ x ∈ xs

Tactic:
rw [h₁.mem_iff]

Premises used: List.Perm.mem_iff
-- Module: Mathlib.Testing.Plausible.Functions
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
⊢ ys.Nodup

Tactic:
have h₂ : ys.Nodup := h₁.nodup_iff.1 h₀
-- Module: Mathlib.Testing.Plausible.Functions
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
⊢ xs.length = ys.length

Tactic:
replace h₁ : xs.length = ys.length := h₁.length_eq
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
inst : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
x val : α
h₃ : dlookup (β := fun (x : α) ↦ α) x (map Prod.toSigma (xs.zip ys)) = Option.some val
h₂ : ys.Nodup
h₁ : xs.length = ys.length
some : val ∈ ys ↔ x ∈ xs
⊢ (Option.some val).getD x ∈ ys ↔ x ∈ xs

Tactic:
dsimp
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
inst : DecidableEq α
x val : α
ys : List α
h₀ : Nodup.{u} (α := α) []
h₃ : dlookup (β := fun (x : α) ↦ α) x (map Prod.toSigma (zip [] ys)) = some val
h₂ : ys.Nodup
h₁ : length.{u} (α := α) [] = ys.length
⊢ val ∈ ys ↔ Membership.mem (γ := List α) [] x

Tactic:
contradiction
-- Module: Mathlib.Testing.Plausible.Functions
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
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
⊢ val ∈ ys ↔ x ∈ x' :: xs

Tactic:
rcases ys with - | ⟨y, ys⟩
-- Module: Mathlib.Testing.Plausible.Functions
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
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:
cases h₃
-- Module: Mathlib.Testing.Plausible.Functions
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
neg :
  ∀ (h : ¬x' = x) (h₃ : dlookup (β := fun (x : α) ↦ α) x (map Prod.toSigma (xs.zip ys)) = some val),
    val ∈ y :: ys ↔ x ∈ x' :: xs
⊢ val ∈ y :: ys ↔ x ∈ x' :: xs

Tactic:
split_ifs at h₃ with h
-- Module: Mathlib.Testing.Plausible.Functions
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₂ : (y :: ys).Nodup
h₁ : (x' :: xs).length = (y :: ys).length
h : x' = x
h₃ : some (Eq.rec (motive := fun (x : α) (x_1 : x' = x) ↦ α) y h) = some val
⊢ Eq.rec (motive := fun (x : α) (x_1 : x' = x) ↦ α) y h = val

Tactic:
rw [Option.some_inj] at h₃

Premises used: Option.some_inj
-- Module: Mathlib.Testing.Plausible.Functions
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₂ : (y :: ys).Nodup
h₁ : (x' :: xs).length = (y :: ys).length
h : x' = x
h₃ : Eq.rec (motive := fun (x : α) (x_1 : x' = x) ↦ α) y h = val
pos :
  ∀ (h₀ : (x :: xs).Nodup) (h₁ : (x :: xs).length = (y :: ys).length)
    (h₃ : Eq.rec (motive := fun (x_1 : α) (x : x = x_1) ↦ α) y ⋯ = val), val ∈ y :: ys ↔ x ∈ x :: xs
⊢ val ∈ y :: ys ↔ x ∈ x' :: xs

Tactic:
subst x'
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
inst : DecidableEq α
x val : α
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
y : α
ys : List α
h₂ : (y :: ys).Nodup
h₀ : (x :: xs).Nodup
h₁ : (x :: xs).length = (y :: ys).length
h₃ : Eq.rec (motive := fun (x_1 : α) (x : x = x_1) ↦ α) y ⋯ = val
pos :
  ∀
    (xs_ih :
      ∀ {ys : List α} (h₀ : xs.Nodup)
        (h₃ :
          dlookup (β := fun (x : α) ↦ α) x (map Prod.toSigma (xs.zip ys)) =
            some (Eq.rec (motive := fun (x_1 : α) (x : x = x_1) ↦ α) y ⋯))
        (h₂ : ys.Nodup) (h₁ : xs.length = ys.length),
        Membership.mem (α := α) ys (Eq.rec (motive := fun (x_1 : α) (x : x = x_1) ↦ α) y ⋯ : α) ↔ x ∈ xs),
    Membership.mem (α := α) (y :: ys) (Eq.rec (motive := fun (x_1 : α) (x : x = x_1) ↦ α) y ⋯ : α) ↔ x ∈ x :: xs
⊢ val ∈ y :: ys ↔ x ∈ x :: xs

Tactic:
subst val
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
inst : DecidableEq α
x : α
xs : List α
y : α
ys : List α
h₂ : (y :: ys).Nodup
h₀ : (x :: xs).Nodup
h₁ : (x :: xs).length = (y :: ys).length
xs_ih :
  ∀ {ys : List α} (h₀ : xs.Nodup)
    (h₃ :
      dlookup (β := fun (x : α) ↦ α) x (map Prod.toSigma (xs.zip ys)) =
        some (Eq.rec (motive := fun (x_1 : α) (x : x = x_1) ↦ α) y ⋯))
    (h₂ : ys.Nodup) (h₁ : xs.length = ys.length),
    Membership.mem (α := α) ys (Eq.rec (motive := fun (x_1 : α) (x : x = x_1) ↦ α) y ⋯ : α) ↔ x ∈ xs
⊢ Membership.mem (α := α) (y :: ys) (Eq.rec (motive := fun (x_1 : α) (x : x = x_1) ↦ α) y ⋯ : α) ↔ x ∈ x :: xs

Tactic:
simp only [List.mem_cons, true_or]

Premises used: true_or, List.mem_cons
-- Module: Mathlib.Testing.Plausible.Functions
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₂ : (y :: ys).Nodup
h₁ : (x' :: xs).length = (y :: ys).length
h : ¬x' = x
h₃ : dlookup (β := fun (x : α) ↦ α) x (map Prod.toSigma (xs.zip ys)) = some val
⊢ List.Pairwise (fun (x1 x2 : α) ↦ x1 ≠ x2) xs

Tactic:
obtain - | ⟨h₀, h₅⟩ := h₀
-- Module: Mathlib.Testing.Plausible.Functions
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₂ : (y :: ys).Nodup
h₁ : (x' :: xs).length = (y :: ys).length
h : ¬x' = x
h₃ : dlookup (β := fun (x : α) ↦ α) x (map Prod.toSigma (xs.zip ys)) = some val
h₅ : List.Pairwise (fun (x1 x2 : α) ↦ x1 ≠ x2) xs
⊢ ∀ a' ∈ xs, x' ≠ a'

Tactic:
obtain - | ⟨h₀, h₅⟩ := h₀
-- Module: Mathlib.Testing.Plausible.Functions
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
y : α
ys : List α
h₂ : (y :: ys).Nodup
h₁ : (x' :: xs).length = (y :: ys).length
h : ¬x' = x
h₃ : dlookup (β := fun (x : α) ↦ α) x (map Prod.toSigma (xs.zip ys)) = some val
h₅ : List.Pairwise (fun (x1 x2 : α) ↦ x1 ≠ x2) xs
h₀ : ∀ a' ∈ xs, x' ≠ a'
⊢ List.Pairwise (fun (x1 x2 : α) ↦ x1 ≠ x2) ys

Tactic:
obtain - | ⟨h₂, h₄⟩ := h₂
-- Module: Mathlib.Testing.Plausible.Functions
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
y : α
ys : List α
h₂ : (y :: ys).Nodup
h₁ : (x' :: xs).length = (y :: ys).length
h : ¬x' = x
h₃ : dlookup (β := fun (x : α) ↦ α) x (map Prod.toSigma (xs.zip ys)) = some val
h₅ : List.Pairwise (fun (x1 x2 : α) ↦ x1 ≠ x2) xs
h₀ : ∀ a' ∈ xs, x' ≠ a'
h₄ : List.Pairwise (fun (x1 x2 : α) ↦ x1 ≠ x2) ys
⊢ ∀ a' ∈ ys, y ≠ a'

Tactic:
obtain - | ⟨h₂, h₄⟩ := h₂
-- Module: Mathlib.Testing.Plausible.Functions
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
y : α
ys : List α
h₁ : (x' :: xs).length = (y :: ys).length
h : ¬x' = x
h₃ : dlookup (β := fun (x : α) ↦ α) x (map Prod.toSigma (xs.zip ys)) = some val
h₅ : List.Pairwise (fun (x1 x2 : α) ↦ x1 ≠ x2) xs
h₀ : ∀ a' ∈ xs, x' ≠ a'
h₄ : List.Pairwise (fun (x1 x2 : α) ↦ x1 ≠ x2) ys
h₂ : ∀ a' ∈ ys, y ≠ a'
⊢ xs.length = ys.length

Tactic:
have h₆ := Nat.succ.inj h₁
-- Module: Mathlib.Testing.Plausible.Functions
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
y : α
ys : List α
h₁ : (x' :: xs).length = (y :: ys).length
h : ¬x' = x
h₃ : dlookup (β := fun (x : α) ↦ α) x (map Prod.toSigma (xs.zip ys)) = some val
h₅ : List.Pairwise (fun (x1 x2 : α) ↦ x1 ≠ x2) xs
h₀ : ∀ a' ∈ xs, x' ≠ a'
h₄ : List.Pairwise (fun (x1 x2 : α) ↦ x1 ≠ x2) ys
h₂ : ∀ a' ∈ ys, y ≠ a'
h₆ : xs.length = ys.length
⊢ val ∈ ys ↔ x ∈ xs

Tactic:
specialize xs_ih h₅ h₃ h₄ h₆
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
inst : DecidableEq α
x val x' : α
xs : List α
y : α
ys : List α
h₁ : (x' :: xs).length = (y :: ys).length
h : ¬x' = x
h₃ : dlookup (β := fun (x : α) ↦ α) x (map Prod.toSigma (xs.zip ys)) = some val
h₅ : List.Pairwise (fun (x1 x2 : α) ↦ x1 ≠ x2) xs
h₀ : ∀ a' ∈ xs, x' ≠ a'
h₄ : List.Pairwise (fun (x1 x2 : α) ↦ x1 ≠ x2) ys
h₂ : ∀ a' ∈ ys, y ≠ a'
h₆ : xs.length = ys.length
xs_ih : val ∈ ys ↔ x ∈ xs
neg : val = y ∨ x ∈ xs ↔ False ∨ x ∈ xs
⊢ val ∈ y :: ys ↔ x ∈ x' :: xs

Tactic:
simp only [Ne.symm h, xs_ih, List.mem_cons]

Premises used: Ne.symm, List.mem_cons
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
inst : DecidableEq α
x val x' : α
xs : List α
y : α
ys : List α
h₁ : (x' :: xs).length = (y :: ys).length
h : ¬x' = x
h₃ : dlookup (β := fun (x : α) ↦ α) x (map Prod.toSigma (xs.zip ys)) = some val
h₅ : List.Pairwise (fun (x1 x2 : α) ↦ x1 ≠ x2) xs
h₀ : ∀ a' ∈ xs, x' ≠ a'
h₄ : List.Pairwise (fun (x1 x2 : α) ↦ x1 ≠ x2) ys
h₂ : ∀ a' ∈ ys, y ≠ a'
h₆ : xs.length = ys.length
xs_ih : val ∈ ys ↔ x ∈ xs
this : val ∈ ys
inl : ∀ (this : val ∈ ys), val ∈ ys → x ∈ xs → (val = y ∨ x ∈ xs ↔ False ∨ x ∈ xs)
inr : ∀ (this : val ∈ ys), val ∉ ys → x ∉ xs → (val = y ∨ x ∈ xs ↔ False ∨ x ∈ xs)
inl₁ : ∀ (this : val ∈ ys), val ∈ ys → x ∈ xs → (val = y ∨ x ∈ xs ↔ False ∨ x ∈ xs)
inl₂ : ∀ (this : val ∈ ys), val ∈ ys → x ∈ xs → val = y ∨ x ∈ xs → False ∨ x ∈ xs
inl₃ : ∀ (this : val ∈ ys), val ∈ ys → x ∈ xs → False ∨ x ∈ xs → val = y ∨ x ∈ xs
inl₄ : ∀ (this : val ∈ ys), val ∈ ys → x ∈ xs → val = y → False ∨ x ∈ xs
inl₅ : ∀ (this : val ∈ ys), val ∈ ys → x ∈ xs → x ∈ xs → False ∨ x ∈ xs
inl₆ : ∀ (this : val ∈ ys), val ∈ ys → x ∈ xs → val = y → False ∨ x ∈ xs
inl₇ : ∀ (this : val ∈ ys), val ∈ ys → x ∈ xs → x ∈ xs → False ∨ x ∈ xs
inl₈ : ∀ (this : val ∈ ys), val ∈ ys → x ∈ xs → val = y → ¬False → x ∈ xs
inl₉ : ∀ (this : val ∈ ys), val ∈ ys → x ∈ xs → x ∈ xs → ¬False → x ∈ xs
inl₁₀ inl₁₁ : ∀ (this : val ∈ ys), val ∈ ys → x ∈ xs → x ∈ xs → val = y ∨ x ∈ xs
inl₁₂ : ∀ (this : val ∈ ys), val ∈ ys → x ∈ xs → x ∈ xs → ¬val = y → x ∈ xs
⊢ val = y ∨ x ∈ xs ↔ False ∨ x ∈ xs

Tactic:
tauto
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
inst : DecidableEq α
x val x' : α
xs : List α
y : α
ys : List α
h₁ : (x' :: xs).length = (y :: ys).length
h : ¬x' = x
h₃ : dlookup (β := fun (x : α) ↦ α) x (map Prod.toSigma (xs.zip ys)) = some val
h₅ : List.Pairwise (fun (x1 x2 : α) ↦ x1 ≠ x2) xs
h₀ : ∀ a' ∈ xs, x' ≠ a'
h₄ : List.Pairwise (fun (x1 x2 : α) ↦ x1 ≠ x2) ys
h₂ : ∀ a' ∈ ys, y ≠ a'
h₆ : xs.length = ys.length
xs_ih : val ∈ ys ↔ x ∈ xs
neg : val ∈ ys
⊢ val = y ∨ x ∈ xs ↔ False ∨ x ∈ xs

Tactic:
suffices val ∈ ys by tauto
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
inst : DecidableEq α
x val x' : α
xs : List α
y : α
ys : List α
h₁ : (x' :: xs).length = (y :: ys).length
h : ¬x' = x
h₃ : dlookup (β := fun (x : α) ↦ α) x (map Prod.toSigma (xs.zip ys)) = some val
h₅ : List.Pairwise (fun (x1 x2 : α) ↦ x1 ≠ x2) xs
h₀ : ∀ a' ∈ xs, x' ≠ a'
h₄ : List.Pairwise (fun (x1 x2 : α) ↦ x1 ≠ x2) ys
h₂ : ∀ a' ∈ ys, y ≠ a'
h₆ : xs.length = ys.length
xs_ih : val ∈ ys ↔ x ∈ xs
neg :
  ∀ (h₃ : Sigma.mk (β := fun (x : α) ↦ α) x val ∈ map Prod.toSigma (xs.zip ys))
    (h₅ : List.Pairwise (fun (x1 x2 : α) ↦ x1 ≠ x2) xs) (h₀ : ∀ a' ∈ xs, x' ≠ a')
    (h₄ : List.Pairwise (fun (x1 x2 : α) ↦ x1 ≠ x2) ys) (h₂ : ∀ a' ∈ ys, y ≠ a') (h₆ : xs.length = ys.length)
    (xs_ih : val ∈ ys ↔ x ∈ xs), val ∈ ys
neg₁ :
  ∀ (h₃ : val ∈ dlookup (β := fun (x : α) ↦ α) x (map Prod.toSigma (xs.zip ys)))
    (h₅ : List.Pairwise (fun (x1 x2 : α) ↦ x1 ≠ x2) xs) (h₀ : ∀ a' ∈ xs, x' ≠ a')
    (h₄ : List.Pairwise (fun (x1 x2 : α) ↦ x1 ≠ x2) ys) (h₂ : ∀ a' ∈ ys, y ≠ a') (h₆ : xs.length = ys.length)
    (xs_ih : val ∈ ys ↔ x ∈ xs), (map Prod.toSigma (xs.zip ys)).NodupKeys (β := fun (x : α) ↦ α)
⊢ val ∈ ys

Tactic:
rw [← Option.mem_def, List.mem_dlookup_iff] at h₃

Premises used: List.mem_dlookup_iff, Option.mem_def
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
inst : DecidableEq α
x val x' : α
xs : List α
y : α
ys : List α
h₁ : (x' :: xs).length = (y :: ys).length
h : ¬x' = x
h₃ : Sigma.mk (β := fun (x : α) ↦ α) x val ∈ map Prod.toSigma (xs.zip ys)
h₅ : List.Pairwise (fun (x1 x2 : α) ↦ x1 ≠ x2) xs
h₀ : ∀ a' ∈ xs, x' ≠ a'
h₄ : List.Pairwise (fun (x1 x2 : α) ↦ x1 ≠ x2) ys
h₂ : ∀ a' ∈ ys, y ≠ a'
h₆ : xs.length = ys.length
xs_ih : val ∈ ys ↔ x ∈ xs
⊢ ∃ (a : α) (b : α),
    (a, b) ∈ xs.zip ys ∧
      Eq (α := (_ : α) × α) (Sigma.mk (β := fun (x : α) ↦ α) a b) (Sigma.mk (β := fun (x : α) ↦ α) x val)

Tactic:
simp only [Prod.toSigma, List.mem_map, Prod.exists] at h₃

Premises used: Prod.toSigma, List.mem_map, Prod.exists
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
inst : DecidableEq α
x val x' : α
xs : List α
y : α
ys : List α
h₁ : (x' :: xs).length = (y :: ys).length
h : ¬x' = x
h₅ : List.Pairwise (fun (x1 x2 : α) ↦ x1 ≠ x2) xs
h₀ : ∀ a' ∈ xs, x' ≠ a'
h₄ : List.Pairwise (fun (x1 x2 : α) ↦ x1 ≠ x2) ys
h₂ : ∀ a' ∈ ys, y ≠ a'
h₆ : xs.length = ys.length
xs_ih : val ∈ ys ↔ x ∈ xs
h₃ :
  ∃ (a : α) (b : α),
    (a, b) ∈ xs.zip ys ∧
      Eq (α := (_ : α) × α) (Sigma.mk (β := fun (x : α) ↦ α) a b) (Sigma.mk (β := fun (x : α) ↦ α) x val)
⊢ (x, val) ∈ xs.zip ys

Tactic:
rcases h₃ with ⟨a, b, h₃, h₄, h₅⟩