awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ val ∈ ys ↔ x ∈ xs
have some : ∀ {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: 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₆)]
Cleared hypotheses: xs, ys, h₀, h₃, h₂, 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)) = 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
⊢ val ∈ ys ↔ x ∈ xs
have 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
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₆)]
Cleared hypotheses: xs, ys, h₀, h₃, h₂, 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 : α
⊢ (dlookup (β := fun (x : α) ↦ α) x (map Prod.toSigma (xs.zip ys))).getD x ∈ ys ↔ x ∈ xs
have cases : ∀ (x_1 : Option α) (h₃ : dlookup (β := fun (x : α) ↦ α) x (map Prod.toSigma (xs.zip ys)) = x_1),
  x_1.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₆)]
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (goal)
Goal:
α : Type u
inst : DecidableEq α
xs ys : List α
x : α
h : x ∉ xs
⊢ (dlookup (β := fun (x : α) ↦ α) x (map Prod.toSigma (xs.zip ys))).getD x = x
have rw : Option.getD none x = x
Tactic: rw [List.dlookup_eq_none.2]
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (goal)
Goal:
α : Type u
inst : DecidableEq α
xs ys : List α
x : α
h : x ∉ xs
rw : Option.getD none x = x
⊢ (dlookup (β := fun (x : α) ↦ α) x (map Prod.toSigma (xs.zip ys))).getD x = x
have rw₁ : x ∉ (map Prod.toSigma (xs.zip ys)).keys (β := fun (x : α) ↦ α)
Tactic: rw [List.dlookup_eq_none.2]
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (goal)
Goal:
α : Type u
inst : DecidableEq α
xs ys : List α
x : α
h : x ∉ xs
⊢ x ∉ (map Prod.toSigma (xs.zip ys)).keys (β := fun (x : α) ↦ α)
have simp : ∀ (x_1 : α), (x, x_1) ∉ xs.zip ys
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]
-- 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 y : α
h : applyId (xs.zip ys) x = applyId (xs.zip ys) y
⊢ x = y
have pos : ∀ (hx : x ∈ xs), x = y
Tactic: by_cases hx : x ∈ xs
-- 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 y : α
h : applyId (xs.zip ys) x = applyId (xs.zip ys) y
pos : ∀ (hx : x ∈ xs), x = y
⊢ x = y
have neg : ∀ (hx : x ∉ xs), x = y
Tactic: by_cases hx : x ∈ xs
-- 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 y : α
h : applyId (xs.zip ys) x = applyId (xs.zip ys) y
hx : x ∈ xs
⊢ x = y
have pos : ∀ (hy : y ∈ xs), x = y
Tactic: by_cases hy : y ∈ xs
-- 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 y : α
h : applyId (xs.zip ys) x = applyId (xs.zip ys) y
hx : x ∈ xs
pos : ∀ (hy : y ∈ xs), x = y
⊢ x = y
have neg : ∀ (hy : y ∉ xs), x = y
Tactic: by_cases hy : y ∈ xs
-- 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 y : α
h : applyId (xs.zip ys) x = applyId (xs.zip ys) y
hx : x ∉ xs
⊢ x = y
have pos : ∀ (hy : y ∈ xs), x = y
Tactic: by_cases hy : y ∈ xs
-- 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 y : α
h : applyId (xs.zip ys) x = applyId (xs.zip ys) y
hx : x ∉ xs
pos : ∀ (hy : y ∈ xs), x = y
⊢ x = y
have neg : ∀ (hy : y ∉ xs), x = y
Tactic: by_cases hy : y ∈ xs
-- 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 y : α
h : applyId (xs.zip ys) x = applyId (xs.zip ys) y
hx : x ∈ xs
hy : y ∈ xs
⊢ x = y
have hx₁ : ∃ (i : ℕ), getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs i = some x
Tactic: rw [List.mem_iff_getElem?] at hx hy
Cleared hypotheses: hx, hy
-- 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 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
⊢ x = y
have hy₁ : ∃ (i : ℕ), getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs i = some y
Tactic: rw [List.mem_iff_getElem?] at hx hy
Cleared hypotheses: hx, hy
-- 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 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
⊢ x = y
have pos : ∀ (i : ℕ) (hx : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs i = some x), x = y
Tactic: obtain ⟨i, hx⟩ := hx
Cleared hypotheses: hx
-- 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 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
⊢ x = y
have pos : ∀ (j : ℕ) (hy : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs j = some y), x = y
Tactic: obtain ⟨j, hy⟩ := hy
Cleared hypotheses: hy
-- 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 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
⊢ x = y
have pos : some x = some y
Tactic: suffices some x = some y by injection this
-- 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 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
⊢ some x = some y
have h₂ : xs.length = ys.length
Tactic: have h₂ := h₁.length_eq
-- 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 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
⊢ some x = some y
have 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
Tactic: rw [List.applyId_zip_eq h₀ h₂ _ _ _ hx] at h
Cleared hypotheses: h, hx, j, hy, 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 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
⊢ some x = some y
have pos : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs i =
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs j
Tactic: rw [← hx, ← hy]
-- 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 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 i =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs j
have pos : i = j
Tactic: congr
-- 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 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
⊢ i = j
have pos : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) ys i =
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) ys j
Tactic: apply (List.getElem?_inj _ (h₁.nodup_iff.1 h₀)).mp
-- 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 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
⊢ i = j
have apply : i < ys.length
Tactic: apply (List.getElem?_inj _ (h₁.nodup_iff.1 h₀)).mp
-- 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 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) ys i =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) ys j
have pos : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) ys j =
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) ys i
Tactic: symm
-- 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 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) ys j =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) ys i
have pos : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) ys j = some (applyId (xs.zip ys) y)
Tactic: rw [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 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
⊢ i < ys.length
have rw : i < xs.length
Tactic: rw [← h₁.length_eq]
-- 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 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
⊢ i < xs.length
have 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
Tactic: rw [List.getElem?_eq_some_iff] at hx
Cleared hypotheses: hx, j, hy, 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 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
⊢ i < xs.length
have hx' : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs i hx₁ = x
Tactic: obtain ⟨hx, hx'⟩ := hx
Cleared hypotheses: hx
-- 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 y : α
h : applyId (xs.zip ys) x = applyId (xs.zip ys) y
hx : x ∈ xs
hy : y ∉ xs
⊢ x = y
have hx₁ : applyId (xs.zip ys) x ∈ ys
Tactic: rw [← applyId_mem_iff h₀ h₁] at hx hy
Cleared hypotheses: hx, hy
-- 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 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
⊢ x = y
have hy₁ : applyId (xs.zip ys) y ∉ ys
Tactic: rw [← applyId_mem_iff h₀ h₁] at hx hy
Cleared hypotheses: hx, hy
-- 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 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
⊢ x = y
have hx₁ : applyId (xs.zip ys) y ∈ ys
Tactic: rw [h] at hx
Cleared hypotheses: hx, hy
-- 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 y : α
h : applyId (xs.zip ys) x = applyId (xs.zip ys) y
hx : x ∉ xs
hy : y ∈ xs
⊢ x = y
have hx₁ : applyId (xs.zip ys) x ∉ ys
Tactic: rw [← applyId_mem_iff h₀ h₁] at hx hy
Cleared hypotheses: hx, hy
-- 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 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
⊢ x = y
have hy₁ : applyId (xs.zip ys) y ∈ ys
Tactic: rw [← applyId_mem_iff h₀ h₁] at hx hy
Cleared hypotheses: hx, hy
-- 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 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
⊢ x = y
have hx₁ : applyId (xs.zip ys) y ∉ ys
Tactic: rw [h] at hx
Cleared hypotheses: hx, hy
-- 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 y : α
h : applyId (xs.zip ys) x = applyId (xs.zip ys) y
hx : x ∉ xs
hy : y ∉ xs
⊢ x = y
have neg : ∀ (h : x = applyId (xs.zip ys) y) (hx : x ∉ xs) (hy : y ∉ xs), y ∉ xs
Tactic: rwa [List.applyId_eq_self, List.applyId_eq_self] at h
Cleared hypotheses: h, hx, hy
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (goal)
Goal:
α : Type u
inst : DecidableEq α
f : InjectiveFunction α
⊢ Injective f.apply
have obtain : ∀ (xs : List ((_ : α) × α))
  (hperm : map (Sigma.fst (β := fun (x : α) ↦ α)) xs ~ map (Sigma.snd (β := fun (x : α) ↦ α)) xs)
  (hnodup : Nodup (α := α) (map (Sigma.snd (β := fun (x : α) ↦ α)) xs)), Injective (mapToSelf xs hperm hnodup).apply
Tactic: obtain ⟨xs, hperm, hnodup⟩ := f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (goal)
Goal:
α : Type u
inst : DecidableEq α
xs : List ((_ : α) × α)
hperm : map (Sigma.fst (β := fun (x : α) ↦ α)) xs ~ map (Sigma.snd (β := fun (x : α) ↦ α)) xs
hnodup : Nodup (α := α) (map (Sigma.snd (β := fun (x : α) ↦ α)) xs)
⊢ Injective (mapToSelf xs hperm hnodup).apply
have generalize : ∀ (xs₀ : List α) (h₀ : map (Sigma.fst (β := fun (x : α) ↦ α)) xs = xs₀), Injective (mapToSelf xs hperm hnodup).apply
Tactic: generalize h₀ : List.map Sigma.fst xs = xs₀
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (goal)
Goal:
α : Type u
inst : DecidableEq α
xs : List ((_ : α) × α)
hperm : map (Sigma.fst (β := fun (x : α) ↦ α)) xs ~ map (Sigma.snd (β := fun (x : α) ↦ α)) xs
hnodup : Nodup (α := α) (map (Sigma.snd (β := fun (x : α) ↦ α)) xs)
xs₀ : List α
h₀ : map (Sigma.fst (β := fun (x : α) ↦ α)) xs = xs₀
⊢ Injective (mapToSelf xs hperm hnodup).apply
have generalize : ∀ (xs₁ : List α) (h₁ : map (id (Sigma.snd (β := fun (x : α) ↦ α))) xs = xs₁),
  Injective (mapToSelf xs hperm hnodup).apply
Tactic: generalize h₁ : xs.map (@id ((Σ _ : α, α) → α) <| @Sigma.snd α fun _ : α => α) = xs₁
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (goal)
Goal:
α : Type u
inst : DecidableEq α
xs : List ((_ : α) × α)
hperm : map (Sigma.fst (β := fun (x : α) ↦ α)) xs ~ map (Sigma.snd (β := fun (x : α) ↦ α)) xs
hnodup : Nodup (α := α) (map (Sigma.snd (β := fun (x : α) ↦ α)) xs)
xs₀ : List α
h₀ : map (Sigma.fst (β := fun (x : α) ↦ α)) xs = xs₀
xs₁ : List α
h₁ : map (Sigma.snd (β := fun (x : α) ↦ α)) xs = xs₁
⊢ xs = List.toFinmap' (xs₀.zip xs₁)
have rw : xs =
  map
    (fun (x : α × α) ↦
      match (motive := α × α → (_ : α) × α) x with
      | (a, b) => Sigma.mk (β := fun (x : α) ↦ α) a b)
    ((map (Sigma.fst (β := fun (x : α) ↦ α)) xs).zip (map (Sigma.snd (β := fun (x : α) ↦ α)) xs))
Tactic: rw [← h₀, ← h₁, List.toFinmap']
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (goal)
Goal:
α : Type u
inst : DecidableEq α
xs : List ((_ : α) × α)
⊢ xs =
    map
      (fun (x : α × α) ↦
        match (motive := α × α → (_ : α) × α) x with
        | (a, b) => Sigma.mk (β := fun (x : α) ↦ α) a b)
      ((map (Sigma.fst (β := fun (x : α) ↦ α)) xs).zip (map (Sigma.snd (β := fun (x : α) ↦ α)) xs))
have nil : Eq.{u + 1} (α := List ((_ : α) × α)) []
  (map
    (fun (x : α × α) ↦
      match (motive := α × α → (_ : α) × α) x with
      | (a, b) => Sigma.mk (β := fun (x : α) ↦ α) a b)
    (zip (map (α := (_ : α) × α) (Sigma.fst (β := fun (x : α) ↦ α)) [])
      (map (α := (_ : α) × α) (Sigma.snd (β := fun (x : α) ↦ α)) [])))
Tactic: induction xs with
    | nil => simp only [List.zip_nil_right, List.map_nil]
    | cons xs_hd xs_tl xs_ih =>
      simp only [Sigma.eta, List.zip_cons_cons,
        List.map, List.cons_inj_right]
      exact xs_ih
Cleared hypotheses: xs