awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (hypothesis)
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
⊢ val ∈ y :: ys ↔ x ∈ x' :: xs
have h₄ : Eq.rec (motive := fun (x : α) (x_1 : x' = x) ↦ α) y h = val
Tactic: rw [Option.some_inj] at 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₂ : (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
⊢ val ∈ y :: ys ↔ x ∈ x' :: xs
have pos : ∀ (h₀ : (x :: xs).Nodup) (h₁ : (x :: xs).length = (y :: ys).length)
  (h₃ : Eq.rec (motive := fun (x_1 : α) (x : x = x_1) ↦ α) y sorry = val), val ∈ y :: ys ↔ x ∈ x :: xs
Tactic: subst x'
Cleared hypotheses: x', h₀, h₁, h, h₃
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (goal)
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
⊢ val ∈ y :: ys ↔ x ∈ x :: xs
have 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 sorry))
      (h₂ : ys.Nodup) (h₁ : xs.length = ys.length),
      Membership.mem (α := α) ys (Eq.rec (motive := fun (x_1 : α) (x : x = x_1) ↦ α) y sorry : α) ↔ x ∈ xs),
  Membership.mem (α := α) (y :: ys) (Eq.rec (motive := fun (x_1 : α) (x : x = x_1) ↦ α) y sorry : α) ↔ x ∈ x :: xs
Tactic: subst val
Cleared hypotheses: val, xs_ih, h₃
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (hypothesis)
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
⊢ val ∈ y :: ys ↔ x ∈ x' :: xs
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 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
⊢ val ∈ y :: ys ↔ x ∈ x' :: xs
have h₄ : ∀ a' ∈ xs, x' ≠ a'
Tactic: obtain - | ⟨h₀, h₅⟩ := h₀
Cleared hypotheses: h₀
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (hypothesis)
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'
⊢ val ∈ y :: ys ↔ x ∈ x' :: xs
have h₄ : List.Pairwise (fun (x1 x2 : α) ↦ x1 ≠ x2) ys
Tactic: obtain - | ⟨h₂, h₄⟩ := h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (hypothesis)
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
⊢ val ∈ y :: ys ↔ x ∈ x' :: xs
have h₆ : ∀ a' ∈ ys, y ≠ a'
Tactic: obtain - | ⟨h₂, h₄⟩ := h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (hypothesis)
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'
⊢ val ∈ y :: ys ↔ x ∈ x' :: xs
have h₆ : xs.length = ys.length
Tactic: have h₆ := Nat.succ.inj h₁
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (hypothesis)
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 ∈ y :: ys ↔ x ∈ x' :: xs
have xs_ih₁ : val ∈ ys ↔ x ∈ xs
Tactic: specialize xs_ih h₅ h₃ h₄ h₆
Cleared hypotheses: xs_ih
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (goal)
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
⊢ val ∈ y :: ys ↔ x ∈ x' :: xs
have neg : val = y ∨ x ∈ xs ↔ False ∨ x ∈ xs
Tactic: simp only [Ne.symm h, xs_ih, List.mem_cons]
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (goal)
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
⊢ val = y ∨ x ∈ xs ↔ False ∨ x ∈ xs
have inl : ∀ (this : val ∈ ys), val ∈ ys → x ∈ xs → (val = y ∨ x ∈ xs ↔ False ∨ x ∈ xs)
Tactic: tauto
Cleared hypotheses: xs_ih, this
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (goal)
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)
⊢ val = y ∨ x ∈ xs ↔ False ∨ x ∈ xs
have inr : ∀ (this : val ∈ ys), val ∉ ys → x ∉ xs → (val = y ∨ x ∈ xs ↔ False ∨ x ∈ xs)
Tactic: tauto
Cleared hypotheses: xs_ih, this
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (goal)
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)
⊢ val = y ∨ x ∈ xs ↔ False ∨ x ∈ xs
have inl₂ : ∀ (this : val ∈ ys), val ∈ ys → x ∈ xs → val = y ∨ x ∈ xs → False ∨ x ∈ xs
Tactic: tauto
Cleared hypotheses: xs_ih, this
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (goal)
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
⊢ val = y ∨ x ∈ xs ↔ False ∨ x ∈ xs
have inl₃ : ∀ (this : val ∈ ys), val ∈ ys → x ∈ xs → False ∨ x ∈ xs → val = y ∨ x ∈ xs
Tactic: tauto
Cleared hypotheses: xs_ih, this
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (goal)
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
⊢ val = y ∨ x ∈ xs ↔ False ∨ x ∈ xs
have inl₄ : ∀ (this : val ∈ ys), val ∈ ys → x ∈ xs → val = y → False ∨ x ∈ xs
Tactic: tauto
Cleared hypotheses: xs_ih, this
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (goal)
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
⊢ val = y ∨ x ∈ xs ↔ False ∨ x ∈ xs
have inl₅ : ∀ (this : val ∈ ys), val ∈ ys → x ∈ xs → x ∈ xs → False ∨ x ∈ xs
Tactic: tauto
Cleared hypotheses: xs_ih, this
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (goal)
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
⊢ val = y ∨ x ∈ xs ↔ False ∨ x ∈ xs
have inl₈ : ∀ (this : val ∈ ys), val ∈ ys → x ∈ xs → val = y → ¬False → x ∈ xs
Tactic: tauto
Cleared hypotheses: xs_ih, this
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (goal)
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
⊢ val = y ∨ x ∈ xs ↔ False ∨ x ∈ xs
have inl₉ : ∀ (this : val ∈ ys), val ∈ ys → x ∈ xs → x ∈ xs → ¬False → x ∈ xs
Tactic: tauto
Cleared hypotheses: xs_ih, this
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (goal)
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
⊢ val = y ∨ x ∈ xs ↔ False ∨ x ∈ xs
have inl₁₀ : ∀ (this : val ∈ ys), val ∈ ys → x ∈ xs → x ∈ xs → val = y ∨ x ∈ xs
Tactic: tauto
Cleared hypotheses: xs_ih, this
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (goal)
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
⊢ val = y ∨ x ∈ xs ↔ False ∨ x ∈ xs
have inl₁₂ : ∀ (this : val ∈ ys), val ∈ ys → x ∈ xs → x ∈ xs → ¬val = y → x ∈ xs
Tactic: tauto
Cleared hypotheses: xs_ih, this
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (goal)
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
⊢ val = y ∨ x ∈ xs ↔ False ∨ x ∈ xs
have neg : val ∈ ys
Tactic: suffices val ∈ ys by tauto
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (goal)
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
⊢ val ∈ ys
have 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
Tactic: rw [← Option.mem_def, List.mem_dlookup_iff] at h₃
Cleared hypotheses: h₃, h₅, h₀, h₄, h₂, h₆, xs_ih
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (goal)
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
⊢ val ∈ ys
have 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 : α) ↦ α)
Tactic: rw [← Option.mem_def, List.mem_dlookup_iff] at h₃
Cleared hypotheses: h₃, h₅, h₀, h₄, h₂, h₆, xs_ih
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (hypothesis)
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
⊢ val ∈ ys
have h₇ : ∃ (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₃
Cleared hypotheses: h₃
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (hypothesis)
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)
⊢ val ∈ ys
have h₇ : (x, val) ∈ xs.zip ys
Tactic: rcases h₃ with ⟨a, b, h₃, h₄, h₅⟩
Cleared hypotheses: h₃
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (goal)
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
⊢ (map Prod.toSigma (xs.zip ys)).NodupKeys (β := fun (x : α) ↦ α)
have neg : Nodup (α := α) (map (fun (x : α × α) ↦ x.1) (xs.zip ys))
Tactic: simp only [List.NodupKeys, List.keys, comp_def, Prod.fst_toSigma, List.map_map]
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (goal)
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
⊢ Nodup (α := α) (map (fun (x : α × α) ↦ x.1) (xs.zip ys))
have neg : xs.Nodup
Tactic: rwa [List.map_fst_zip (le_of_eq h₆)]