awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₃ : (x, val) ∈ xs.zip ys
⊢ val ∈ ys

Tactic:
apply (List.of_mem_zip h₃).2

Premises used: And.right, List.of_mem_zip
-- 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₃ : 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
neg : Nodup (α := α) (map (fun (x : α × α) ↦ x.1) (xs.zip ys))
⊢ (map Prod.toSigma (xs.zip ys)).NodupKeys (β := fun (x : α) ↦ α)

Tactic:
simp only [List.NodupKeys, List.keys, comp_def, Prod.fst_toSigma, List.map_map]

Premises used: List.keys, List.map_map, Prod.fst_toSigma, Function.comp_def, List.NodupKeys
-- 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₃ : 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
neg neg₁ neg₂ neg₃ : xs.Nodup
⊢ Nodup (α := α) (map (fun (x : α × α) ↦ x.1) (xs.zip ys))

Tactic:
rwa [List.map_fst_zip (le_of_eq h₆)]

Premises used: List.map_fst_zip, le_of_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 :
  ∀ {ys : List α} (h₀ : Nodup.{u} (α := α) [])
    (h₃ : dlookup (β := fun (x : α) ↦ α) x (map Prod.toSigma (zip [] ys)) = Option.some val) (h₂ : ys.Nodup)
    (h₁ : length.{u} (α := α) [] = ys.length), val ∈ ys ↔ Membership.mem (γ := List α) [] x
some₁ :
  ∀ (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), val ∈ ys ↔ x ∈ x' :: xs
⊢ val ∈ ys ↔ x ∈ xs

Tactic:
induction xs generalizing ys with
    | nil => contradiction
    | cons x' xs xs_ih =>
      rcases ys with - | ⟨y, ys⟩
      · cases h₃
      dsimp [List.dlookup] at h₃; split_ifs at h₃ with h
      · rw [Option.some_inj] at h₃
        subst x'; subst val
        simp only [List.mem_cons, true_or]
      · obtain - | ⟨h₀, h₅⟩ := h₀
        obtain - | ⟨h₂, h₄⟩ := h₂
        have h₆ := Nat.succ.inj h₁
        specialize xs_ih h₅ h₃ h₄ h₆
        simp only [Ne.symm h, xs_ih, List.mem_cons]
        suffices val ∈ ys by tauto
        rw [← Option.mem_def, List.mem_dlookup_iff] at h₃
        · simp only [Prod.toSigma, List.mem_map, Prod.exists] at h₃
          rcases h₃ with ⟨a, b, h₃, h₄, h₅⟩
          apply (List.of_mem_zip h₃).2
        simp only [List.NodupKeys, List.keys, comp_def, Prod.fst_toSigma, List.map_map]
        rwa [List.map_fst_zip (le_of_eq h₆)]

Premises used: Prod.toSigma, true_or, List.keys, List.map_map, List.cons, Prod.fst_toSigma, Function.comp_def, List.mem_dlookup_iff, List.NodupKeys, List.mem_cons, List.mem_map, Prod.exists, List.dlookup, Option.some_inj, Option.mem_def, List.nil
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
inst : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x : α
cases :
  ∀ (x_1 : Option α) (h₃ : dlookup (β := fun (x : α) ↦ α) x (map Prod.toSigma (xs.zip ys)) = x_1),
    x_1.getD x ∈ ys ↔ x ∈ xs
⊢ (dlookup (β := fun (x : α) ↦ α) x (map Prod.toSigma (xs.zip ys))).getD x ∈ ys ↔ x ∈ xs

Tactic:
cases h₃ : List.dlookup x (List.map Prod.toSigma (xs.zip ys)) with
  | none =>
    dsimp [Option.getD]
    rw [h₁.mem_iff]
  | some val =>
    have h₂ : ys.Nodup := h₁.nodup_iff.1 h₀
    replace h₁ : xs.length = ys.length := h₁.length_eq
    dsimp
    induction xs generalizing ys with
    | nil => contradiction
    | cons x' xs xs_ih =>
      rcases ys with - | ⟨y, ys⟩
      · cases h₃
      dsimp [List.dlookup] at h₃; split_ifs at h₃ with h
      · rw [Option.some_inj] at h₃
        subst x'; subst val
        simp only [List.mem_cons, true_or]
      · obtain - | ⟨h₀, h₅⟩ := h₀
        obtain - | ⟨h₂, h₄⟩ := h₂
        have h₆ := Nat.succ.inj h₁
        specialize xs_ih h₅ h₃ h₄ h₆
        simp only [Ne.symm h, xs_ih, List.mem_cons]
        suffices val ∈ ys by tauto
        rw [← Option.mem_def, List.mem_dlookup_iff] at h₃
        · simp only [Prod.toSigma, List.mem_map, Prod.exists] at h₃
          rcases h₃ with ⟨a, b, h₃, h₄, h₅⟩
          apply (List.of_mem_zip h₃).2
        simp only [List.NodupKeys, List.keys, comp_def, Prod.fst_toSigma, List.map_map]
        rwa [List.map_fst_zip (le_of_eq h₆)]

Premises used: Prod.toSigma, true_or, List.map, List.keys, Option.getD, Option.some, List.map_map, List.zip, List.cons, Option.none, Prod.fst_toSigma, Function.comp_def, List.mem_dlookup_iff, List.NodupKeys, List.mem_cons, List.mem_map, Prod.exists, List.Perm.mem_iff, List.dlookup, Option.some_inj, Option.mem_def, List.nil
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
inst : DecidableEq α
xs ys : List α
x : α
h : x ∉ xs
rw : Option.getD none x = x
rw₁ : x ∉ (map Prod.toSigma (xs.zip ys)).keys (β := fun (x : α) ↦ α)
⊢ (dlookup (β := fun (x : α) ↦ α) x (map Prod.toSigma (xs.zip ys))).getD x = x

Tactic:
rw [List.dlookup_eq_none.2]

Premises used: Iff.mpr, List.dlookup_eq_none
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
inst : DecidableEq α
xs ys : List α
x : α
h : x ∉ xs
⊢ Option.getD none x = x

Tactic:
rfl
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
inst : DecidableEq α
xs ys : List α
x : α
h : x ∉ xs
simp : ∀ (x_1 : α), (x, x_1) ∉ xs.zip ys
⊢ x ∉ (map Prod.toSigma (xs.zip ys)).keys (β := fun (x : α) ↦ α)

Tactic:
simp only [List.keys, not_exists, Prod.toSigma, exists_and_right, exists_eq_right, List.mem_map,
    Function.comp_apply, List.map_map, Prod.exists]

Premises used: Prod.toSigma, List.keys, not_exists, exists_eq_right, List.map_map, exists_and_right, Function.comp_apply, List.mem_map, Prod.exists
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
inst : DecidableEq α
xs ys : List α
x : α
h : x ∉ xs
y : α
hy : (x, y) ∈ xs.zip ys
⊢ False

Tactic:
h (List.of_mem_zip hy).1

Premises used: And.left, List.of_mem_zip
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
inst : DecidableEq α
xs ys : List α
x : α
h : x ∉ xs
y : α
hy : (x, y) ∈ xs.zip ys
⊢ False

Tactic:
exact h (List.of_mem_zip hy).1

Premises used: And.left, List.of_mem_zip
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
inst : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
h : applyId (xs.zip ys) x = applyId (xs.zip ys) y
pos : ∀ (hx : x ∈ xs), x = y
neg : ∀ (hx : x ∉ xs), x = y
⊢ x = y

Tactic:
by_cases hx : x ∈ xs
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
inst : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
h : applyId (xs.zip ys) x = applyId (xs.zip ys) y
hx : x ∈ xs
pos : ∀ (hy : y ∈ xs), x = y
neg : ∀ (hy : y ∉ xs), x = y
⊢ x = y

Tactic:
by_cases hy : y ∈ xs
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
inst : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
h : applyId (xs.zip ys) x = applyId (xs.zip ys) y
hx : x ∉ xs
pos : ∀ (hy : y ∈ xs), x = y
neg : ∀ (hy : y ∉ xs), x = y
⊢ x = y

Tactic:
by_cases hy : y ∈ xs
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
inst : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
h : applyId (xs.zip ys) x = applyId (xs.zip ys) y
hx : x ∈ xs
hy : y ∈ xs
⊢ ∃ (i : ℕ), getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs i = some x

Tactic:
rw [List.mem_iff_getElem?] at hx hy

Premises used: List.mem_iff_getElem?
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
inst : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
h : applyId (xs.zip ys) x = applyId (xs.zip ys) y
hx : x ∈ xs
hy : y ∈ xs
hx₁ : ∃ (i : ℕ), getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs i = some x
⊢ ∃ (i : ℕ), getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs i = some y

Tactic:
rw [List.mem_iff_getElem?] at hx hy

Premises used: List.mem_iff_getElem?
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
inst : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
h : applyId (xs.zip ys) x = applyId (xs.zip ys) y
hx : ∃ (i : ℕ), getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs i = some x
hy : ∃ (i : ℕ), getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs i = some y
pos : ∀ (i : ℕ) (hx : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs i = some x), x = y
⊢ x = y

Tactic:
obtain ⟨i, hx⟩ := hx
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
inst : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
h : applyId (xs.zip ys) x = applyId (xs.zip ys) y
hy : ∃ (i : ℕ), getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs i = some y
i : ℕ
hx : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs i = some x
pos : ∀ (j : ℕ) (hy : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs j = some y), x = y
⊢ x = y

Tactic:
obtain ⟨j, hy⟩ := hy
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
inst : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
h : applyId (xs.zip ys) x = applyId (xs.zip ys) y
i : ℕ
hx : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs i = some x
j : ℕ
hy : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs j = some y
this : some x = some y
⊢ x = y

Tactic:
injection this
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
inst : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
h : applyId (xs.zip ys) x = applyId (xs.zip ys) y
i : ℕ
hx : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs i = some x
j : ℕ
hy : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs j = some y
pos : some x = some y
⊢ x = y

Tactic:
suffices some x = some y by injection this
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
inst : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
h : applyId (xs.zip ys) x = applyId (xs.zip ys) y
i : ℕ
hx : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs i = some x
j : ℕ
hy : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs j = some y
⊢ xs.length = ys.length

Tactic:
have h₂ := h₁.length_eq
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
inst : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
h : applyId (xs.zip ys) x = applyId (xs.zip ys) y
i : ℕ
hx : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs i = some x
j : ℕ
hy : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs j = some y
h₂ : xs.length = ys.length
pos :
  ∀ (h : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) ys i = some (applyId (xs.zip ys) y))
    (hx : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs i = some x) (j : ℕ)
    (hy : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs j = some y) (h₂ : xs.length = ys.length),
    some x = some y
⊢ some x = some y

Tactic:
rw [List.applyId_zip_eq h₀ h₂ _ _ _ hx] at h

Premises used: Plausible.InjectiveFunction.List.applyId_zip_eq
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
inst : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
i : ℕ
h : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) ys i = some (applyId (xs.zip ys) y)
hx : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs i = some x
j : ℕ
hy : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs j = some y
h₂ : xs.length = ys.length
pos :
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs i =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs j
⊢ some x = some y

Tactic:
rw [← hx, ← hy]
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
inst : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
i : ℕ
h : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) ys i = some (applyId (xs.zip ys) y)
hx : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs i = some x
j : ℕ
hy : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs j = some y
h₂ : xs.length = ys.length
pos : i = j
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs i =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs j

Tactic:
congr
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
inst : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
i : ℕ
h : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) ys i = some (applyId (xs.zip ys) y)
hx : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs i = some x
j : ℕ
hy : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs j = some y
h₂ : xs.length = ys.length
pos :
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) ys i =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) ys j
apply : i < ys.length
⊢ i = j

Tactic:
apply (List.getElem?_inj _ (h₁.nodup_iff.1 h₀)).mp

Premises used: List.Perm.nodup_iff, List.getElem?_inj, Iff.mp
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
inst : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
i : ℕ
h : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) ys i = some (applyId (xs.zip ys) y)
hx : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs i = some x
j : ℕ
hy : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs j = some y
h₂ : xs.length = ys.length
pos :
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) ys j =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) ys i
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) ys i =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) ys j

Tactic:
symm
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
inst : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
i : ℕ
h : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) ys i = some (applyId (xs.zip ys) y)
hx : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs i = some x
j : ℕ
hy : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs j = some y
h₂ : xs.length = ys.length
pos : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) ys j = some (applyId (xs.zip ys) y)
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) ys j =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) ys i

Tactic:
rw [h]
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
inst : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
i : ℕ
h : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) ys i = some (applyId (xs.zip ys) y)
hx : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs i = some x
j : ℕ
hy : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs j = some y
h₂ : xs.length = ys.length
pos : xs.Nodup
pos₁ : xs.length = ys.length
pos₂ : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs j = some y
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) ys j = some (applyId (xs.zip ys) y)

Tactic:
rw [← List.applyId_zip_eq]

Premises used: Plausible.InjectiveFunction.List.applyId_zip_eq
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
inst : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
i : ℕ
h : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) ys i = some (applyId (xs.zip ys) y)
hx : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs i = some x
j : ℕ
hy : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs j = some y
h₂ : xs.length = ys.length
⊢ xs.Nodup

Tactic:
assumption
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
inst : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
i : ℕ
h : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) ys i = some (applyId (xs.zip ys) y)
hx : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs i = some x
j : ℕ
hy : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs j = some y
h₂ : xs.length = ys.length
⊢ xs.length = ys.length

Tactic:
assumption
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
inst : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
i : ℕ
h : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) ys i = some (applyId (xs.zip ys) y)
hx : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs i = some x
j : ℕ
hy : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs j = some y
h₂ : xs.length = ys.length
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs j = some y

Tactic:
assumption
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
inst : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
i : ℕ
h : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) ys i = some (applyId (xs.zip ys) y)
hx : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs i = some x
j : ℕ
hy : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs j = some y
h₂ : xs.length = ys.length
rw : i < xs.length
⊢ i < ys.length

Tactic:
rw [← h₁.length_eq]

Premises used: List.Perm.length_eq
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
inst : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
i : ℕ
h : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) ys i = some (applyId (xs.zip ys) y)
hx : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs i = some x
j : ℕ
hy : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs j = some y
h₂ : xs.length = ys.length
rw :
  ∀ (hx : ∃ (h : i < xs.length), getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs i h = x) (j : ℕ)
    (hy : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs j = some y) (h₂ : xs.length = ys.length),
    i < xs.length
⊢ i < xs.length

Tactic:
rw [List.getElem?_eq_some_iff] at hx

Premises used: List.getElem?_eq_some_iff
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
inst : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
i : ℕ
h : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) ys i = some (applyId (xs.zip ys) y)
hx : ∃ (h : i < xs.length), getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs i h = x
j : ℕ
hy : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs j = some y
h₂ : xs.length = ys.length
⊢ i < xs.length

Tactic:
obtain ⟨hx, hx'⟩ := hx
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
inst : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
i : ℕ
h : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) ys i = some (applyId (xs.zip ys) y)
hx : ∃ (h : i < xs.length), getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs i h = x
j : ℕ
hy : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs j = some y
h₂ : xs.length = ys.length
hx₁ : i < xs.length
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs i hx₁ = x

Tactic:
obtain ⟨hx, hx'⟩ := hx
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
inst : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
i : ℕ
h : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) ys i = some (applyId (xs.zip ys) y)
j : ℕ
hy : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs j = some y
h₂ : xs.length = ys.length
hx : i < xs.length
hx' : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs i hx = x
⊢ i < xs.length

Tactic:
hx
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
inst : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
i : ℕ
h : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) ys i = some (applyId (xs.zip ys) y)
j : ℕ
hy : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs j = some y
h₂ : xs.length = ys.length
hx : i < xs.length
hx' : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs i hx = x
⊢ i < xs.length

Tactic:
exact hx
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
inst : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
h : applyId (xs.zip ys) x = applyId (xs.zip ys) y
hx : x ∈ xs
hy : y ∉ xs
⊢ applyId (xs.zip ys) x ∈ ys

Tactic:
rw [← applyId_mem_iff h₀ h₁] at hx hy

Premises used: Plausible.InjectiveFunction.applyId_mem_iff
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
inst : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
h : applyId (xs.zip ys) x = applyId (xs.zip ys) y
hx : x ∈ xs
hy : y ∉ xs
hx₁ : applyId (xs.zip ys) x ∈ ys
⊢ applyId (xs.zip ys) y ∉ ys

Tactic:
rw [← applyId_mem_iff h₀ h₁] at hx hy

Premises used: Plausible.InjectiveFunction.applyId_mem_iff
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
inst : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
h : applyId (xs.zip ys) x = applyId (xs.zip ys) y
hx : applyId (xs.zip ys) x ∈ ys
hy : applyId (xs.zip ys) y ∉ ys
⊢ applyId (xs.zip ys) y ∈ ys

Tactic:
rw [h] at hx
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
inst : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
h : applyId (xs.zip ys) x = applyId (xs.zip ys) y
hx : applyId (xs.zip ys) x ∈ ys
hy : applyId (xs.zip ys) y ∉ ys
hx₁ : applyId (xs.zip ys) y ∈ ys
⊢ applyId (xs.zip ys) y ∉ ys

Tactic:
rw [h] at hx
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
inst : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
h : applyId (xs.zip ys) x = applyId (xs.zip ys) y
hx : applyId (xs.zip ys) y ∈ ys
hy : applyId (xs.zip ys) y ∉ ys
⊢ x = y

Tactic:
contradiction
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
inst : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
h : applyId (xs.zip ys) x = applyId (xs.zip ys) y
hx : x ∉ xs
hy : y ∈ xs
⊢ applyId (xs.zip ys) x ∉ ys

Tactic:
rw [← applyId_mem_iff h₀ h₁] at hx hy

Premises used: Plausible.InjectiveFunction.applyId_mem_iff
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
inst : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
h : applyId (xs.zip ys) x = applyId (xs.zip ys) y
hx : x ∉ xs
hy : y ∈ xs
hx₁ : applyId (xs.zip ys) x ∉ ys
⊢ applyId (xs.zip ys) y ∈ ys

Tactic:
rw [← applyId_mem_iff h₀ h₁] at hx hy

Premises used: Plausible.InjectiveFunction.applyId_mem_iff
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
inst : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
h : applyId (xs.zip ys) x = applyId (xs.zip ys) y
hx : applyId (xs.zip ys) x ∉ ys
hy : applyId (xs.zip ys) y ∈ ys
⊢ applyId (xs.zip ys) y ∉ ys

Tactic:
rw [h] at hx
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
inst : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
h : applyId (xs.zip ys) x = applyId (xs.zip ys) y
hx : applyId (xs.zip ys) x ∉ ys
hy : applyId (xs.zip ys) y ∈ ys
hx₁ : applyId (xs.zip ys) y ∉ ys
⊢ applyId (xs.zip ys) y ∈ ys

Tactic:
rw [h] at hx