awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
β : Type v
inst : DecidableEq α
y : β
x : α
m : List ((_ : α) × β)
ih :
  Option.map (Sigma.snd (β := fun (x : α) ↦ β))
      (List.find? (fun (x_1 : (_ : α) × β) ↦ decide (x_1.fst (β := fun (x : α) ↦ β) = x)) m) =
    List.dlookup (β := fun (x : α) ↦ β) x m
fst : α
snd : β
heq : ¬fst = x
neg :
  Option.map (Sigma.snd (β := fun (x : α) ↦ β))
      (List.find? (fun (x_1 : (_ : α) × β) ↦ decide (x_1.fst (β := fun (x : α) ↦ β) = x))
        (Sigma.mk (β := fun (x : α) ↦ β) fst snd :: m)) =
    List.dlookup (β := fun (x : α) ↦ β) x m
neg₁ : x ≠ Sigma.fst (β := fun (x : α) ↦ β) (Sigma.mk (β := fun (x : α) ↦ β) fst snd)
⊢ Option.map (Sigma.snd (β := fun (x : α) ↦ β))
      (List.find? (fun (x_1 : (_ : α) × β) ↦ decide (x_1.fst (β := fun (x : α) ↦ β) = x))
        (Sigma.mk (β := fun (x : α) ↦ β) fst snd :: m)) =
    List.dlookup (β := fun (x : α) ↦ β) x (Sigma.mk (β := fun (x : α) ↦ β) fst snd :: m)

Tactic:
rw [List.dlookup_cons_ne]

Premises used: List.dlookup_cons_ne
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
β : Type v
inst : DecidableEq α
y : β
x : α
m : List ((_ : α) × β)
ih :
  Option.map (Sigma.snd (β := fun (x : α) ↦ β))
      (List.find? (fun (x_1 : (_ : α) × β) ↦ decide (x_1.fst (β := fun (x : α) ↦ β) = x)) m) =
    List.dlookup (β := fun (x : α) ↦ β) x m
fst : α
snd : β
heq : ¬fst = x
⊢ Option.map (Sigma.snd (β := fun (x : α) ↦ β))
      (List.find? (fun (x_1 : (_ : α) × β) ↦ decide (x_1.fst (β := fun (x : α) ↦ β) = x))
        (Sigma.mk (β := fun (x : α) ↦ β) fst snd :: m)) =
    List.dlookup (β := fun (x : α) ↦ β) x m

Tactic:
simp [heq, ih]
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
β : Type v
inst : DecidableEq α
y : β
x : α
m : List ((_ : α) × β)
ih :
  Option.map (Sigma.snd (β := fun (x : α) ↦ β))
      (List.find? (fun (x_1 : (_ : α) × β) ↦ decide (x_1.fst (β := fun (x : α) ↦ β) = x)) m) =
    List.dlookup (β := fun (x : α) ↦ β) x m
fst : α
snd : β
heq : ¬fst = x
neg : Sigma.fst (β := fun (x : α) ↦ β) (Sigma.mk (β := fun (x : α) ↦ β) fst snd) ≠ x
⊢ x ≠ Sigma.fst (β := fun (x : α) ↦ β) (Sigma.mk (β := fun (x : α) ↦ β) fst snd)

Tactic:
symm
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
β : Type v
inst : DecidableEq α
y : β
x : α
m : List ((_ : α) × β)
ih :
  Option.map (Sigma.snd (β := fun (x : α) ↦ β))
      (List.find? (fun (x_1 : (_ : α) × β) ↦ decide (x_1.fst (β := fun (x : α) ↦ β) = x)) m) =
    List.dlookup (β := fun (x : α) ↦ β) x m
fst : α
snd : β
heq : ¬fst = x
⊢ Sigma.fst (β := fun (x : α) ↦ β) (Sigma.mk (β := fun (x : α) ↦ β) fst snd) ≠ x

Tactic:
simp [heq]
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
β : Type v
inst : DecidableEq α
m : List ((_ : α) × β)
y : β
x : α
e_opt :
  Eq.{v + 1} (α := Option β)
    (Option.map (α := (_ : α) × β) (Sigma.snd (β := fun (x : α) ↦ β))
        (List.find? (fun (x_1 : (_ : α) × β) ↦ decide (x_1.fst (β := fun (x : α) ↦ β) = x)) []) :
      Option β)
    (List.dlookup (β := fun (x : α) ↦ β) x [] : Option β)
e_opt₁ :
  ∀ (p : (_ : α) × β) (m : List ((_ : α) × β))
    (ih :
      Option.map (Sigma.snd (β := fun (x : α) ↦ β))
          (List.find? (fun (x_1 : (_ : α) × β) ↦ decide (x_1.fst (β := fun (x : α) ↦ β) = x)) m) =
        List.dlookup (β := fun (x : α) ↦ β) x m),
    Option.map (Sigma.snd (β := fun (x : α) ↦ β))
        (List.find? (fun (x_1 : (_ : α) × β) ↦ decide (x_1.fst (β := fun (x : α) ↦ β) = x)) (p :: m)) =
      List.dlookup (β := fun (x : α) ↦ β) x (p :: m)
⊢ Option.map (Sigma.snd (β := fun (x : α) ↦ β))
      (List.find? (fun (x_1 : (_ : α) × β) ↦ decide (x_1.fst (β := fun (x : α) ↦ β) = x)) m) =
    List.dlookup (β := fun (x : α) ↦ β) x m

Tactic:
induction m with
  | nil => simp
  | cons p m ih =>
    rcases p with ⟨fst, snd⟩
    by_cases heq : fst = x
    · simp [heq]
    · rw [List.dlookup_cons_ne]
      · simp [heq, ih]
      · symm
        simp [heq]

Premises used: List.dlookup_cons_ne
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
β : Type v
inst : DecidableEq α
inst_1 : Zero β
inst_2 : DecidableEq β
tf : TotalFunction α β
a : α
rcases :
  ∀ (A : List ((_ : α) × β)) (y : β), a ∈ (withDefault A y).zeroDefaultSupp ↔ (withDefault A y).zeroDefault.apply a ≠ 0
⊢ a ∈ tf.zeroDefaultSupp ↔ tf.zeroDefault.apply a ≠ 0

Tactic:
rcases tf with ⟨A, y⟩
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
β : Type v
inst : DecidableEq α
inst_1 : Zero β
inst_2 : DecidableEq β
a : α
A : List ((_ : α) × β)
y : β
simp :
  (∃ (x : β), Sigma.mk (β := fun (a : α) ↦ β) a x ∈ A.dedupKeys (β := fun (x : α) ↦ β) ∧ (decide ¬x = 0) = true) ↔
    ¬(withDefault A 0).apply a = 0
⊢ a ∈ (withDefault A y).zeroDefaultSupp ↔ (withDefault A y).zeroDefault.apply a ≠ 0

Tactic:
simp only [zeroDefaultSupp, List.mem_map, List.mem_filter, exists_and_right,
      List.mem_toFinset, exists_eq_right, Sigma.exists, Ne, zeroDefault]

Premises used: List.mem_toFinset, Sigma.exists, Plausible.TotalFunction.zeroDefault, exists_eq_right, Ne, exists_and_right, List.mem_filter, Plausible.TotalFunction.zeroDefaultSupp, List.mem_map
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
β : Type v
inst : DecidableEq α
inst_1 : Zero β
inst_2 : DecidableEq β
a : α
A : List ((_ : α) × β)
y : β
rw :
  (∃ (x : β), Sigma.mk (β := fun (a : α) ↦ β) a x ∈ A.dedupKeys (β := fun (x : α) ↦ β) ∧ (decide ¬x = 0) = true) ↔
    ¬(List.dlookup (β := fun (x : α) ↦ β) a A).getD 0 = 0
⊢ (∃ (x : β), Sigma.mk (β := fun (a : α) ↦ β) a x ∈ A.dedupKeys (β := fun (x : α) ↦ β) ∧ (decide ¬x = 0) = true) ↔
    ¬(withDefault A 0).apply a = 0

Tactic:
rw [apply_eq_dlookup]

Premises used: _private.0.Plausible.TotalFunction.apply_eq_dlookup
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
β : Type v
inst : DecidableEq α
inst_1 : Zero β
inst_2 : DecidableEq β
a : α
A : List ((_ : α) × β)
y : β
mp :
  (∃ (x : β), Sigma.mk (β := fun (a : α) ↦ β) a x ∈ A.dedupKeys (β := fun (x : α) ↦ β) ∧ (decide ¬x = 0) = true) →
    ¬(List.dlookup (β := fun (x : α) ↦ β) a A).getD 0 = 0
mpr :
  ¬(List.dlookup (β := fun (x : α) ↦ β) a A).getD 0 = 0 →
    ∃ (x : β), Sigma.mk (β := fun (a : α) ↦ β) a x ∈ A.dedupKeys (β := fun (x : α) ↦ β) ∧ (decide ¬x = 0) = true
⊢ (∃ (x : β), Sigma.mk (β := fun (a : α) ↦ β) a x ∈ A.dedupKeys (β := fun (x : α) ↦ β) ∧ (decide ¬x = 0) = true) ↔
    ¬(List.dlookup (β := fun (x : α) ↦ β) a A).getD 0 = 0

Tactic:
constructor
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
β : Type v
inst : DecidableEq α
inst_1 : Zero β
inst_2 : DecidableEq β
a : α
A : List ((_ : α) × β)
y od : β
hval : Sigma.mk (β := fun (a : α) ↦ β) a od ∈ A.dedupKeys (β := fun (x : α) ↦ β)
hod : (decide ¬od = 0) = true
⊢ od ∈ List.dlookup (β := fun (x : α) ↦ β) a (A.dedupKeys (β := fun (x : α) ↦ β))

Tactic:
have := List.mem_dlookup (List.nodupKeys_dedupKeys A) hval
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
β : Type v
inst : DecidableEq α
inst_1 : Zero β
inst_2 : DecidableEq β
a : α
A : List ((_ : α) × β)
y od : β
hval : Sigma.mk (β := fun (a : α) ↦ β) a od ∈ A.dedupKeys (β := fun (x : α) ↦ β)
hod : (decide ¬od = 0) = true
this : od ∈ List.dlookup (β := fun (x : α) ↦ β) a (A.dedupKeys (β := fun (x : α) ↦ β))
mp : ¬(some od).getD 0 = 0
rw : List.dlookup (β := fun (x : α) ↦ β) a A = some od
⊢ ¬(List.dlookup (β := fun (x : α) ↦ β) a A).getD 0 = 0

Tactic:
rw [(_ : List.dlookup a A = od)]
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
β : Type v
inst : DecidableEq α
inst_1 : Zero β
inst_2 : DecidableEq β
a : α
A : List ((_ : α) × β)
y od : β
hval : Sigma.mk (β := fun (a : α) ↦ β) a od ∈ A.dedupKeys (β := fun (x : α) ↦ β)
hod : (decide ¬od = 0) = true
this : od ∈ List.dlookup (β := fun (x : α) ↦ β) a (A.dedupKeys (β := fun (x : α) ↦ β))
⊢ ¬(some od).getD 0 = 0

Tactic:
simpa using hod
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
β : Type v
inst : DecidableEq α
inst_1 : Zero β
inst_2 : DecidableEq β
a : α
A : List ((_ : α) × β)
y od : β
hval : Sigma.mk (β := fun (a : α) ↦ β) a od ∈ A.dedupKeys (β := fun (x : α) ↦ β)
hod : (decide ¬od = 0) = true
this : od ∈ List.dlookup (β := fun (x : α) ↦ β) a (A.dedupKeys (β := fun (x : α) ↦ β))
⊢ List.dlookup (β := fun (x : α) ↦ β) a A = some od

Tactic:
simpa [List.dlookup_dedupKeys]

Premises used: List.dlookup_dedupKeys
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
β : Type v
inst : DecidableEq α
inst_1 : Zero β
inst_2 : DecidableEq β
a : α
A : List ((_ : α) × β)
y : β
h : ¬(List.dlookup (β := fun (x : α) ↦ β) a A).getD 0 = 0
h₁ :
  Sigma.mk (β := fun (a : α) ↦ β) a ((List.dlookup (β := fun (x : α) ↦ β) a A).getD 0) ∈
      A.dedupKeys (β := fun (x : α) ↦ β) ∧
    (decide ¬(List.dlookup (β := fun (x : α) ↦ β) a A).getD 0 = 0) = true
⊢ ∃ (x : β), Sigma.mk (β := fun (a : α) ↦ β) a x ∈ A.dedupKeys (β := fun (x : α) ↦ β) ∧ (decide ¬x = 0) = true

Tactic:
use (A.dlookup a).getD (0 : β)

Premises used: Option.getD, OfNat.ofNat, List.dlookup
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
β : Type v
inst : DecidableEq α
inst_1 : Zero β
inst_2 : DecidableEq β
a : α
A : List ((_ : α) × β)
y : β
h : ¬(List.dlookup (β := fun (x : α) ↦ β) a A).getD 0 = 0
h₁ :
  ∀ (h : ¬(List.dlookup (β := fun (x : α) ↦ β) a (A.dedupKeys (β := fun (x : α) ↦ β))).getD 0 = 0),
    Sigma.mk (β := fun (a : α) ↦ β) a
          ((List.dlookup (β := fun (x : α) ↦ β) a (A.dedupKeys (β := fun (x : α) ↦ β))).getD 0) ∈
        A.dedupKeys (β := fun (x : α) ↦ β) ∧
      (decide ¬(List.dlookup (β := fun (x : α) ↦ β) a (A.dedupKeys (β := fun (x : α) ↦ β))).getD 0 = 0) = true
⊢ Sigma.mk (β := fun (a : α) ↦ β) a ((List.dlookup (β := fun (x : α) ↦ β) a A).getD 0) ∈
      A.dedupKeys (β := fun (x : α) ↦ β) ∧
    (decide ¬(List.dlookup (β := fun (x : α) ↦ β) a A).getD 0 = 0) = true

Tactic:
rw [← List.dlookup_dedupKeys] at h ⊢

Premises used: List.dlookup_dedupKeys
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
β : Type v
inst : DecidableEq α
inst_1 : Zero β
inst_2 : DecidableEq β
a : α
A : List ((_ : α) × β)
y : β
h : ¬(List.dlookup (β := fun (x : α) ↦ β) a (A.dedupKeys (β := fun (x : α) ↦ β))).getD 0 = 0
h₁ :
  List.dlookup (β := fun (x : α) ↦ β) a (A.dedupKeys (β := fun (x : α) ↦ β)) =
      some ((List.dlookup (β := fun (x : α) ↦ β) a (A.dedupKeys (β := fun (x : α) ↦ β))).getD 0) ∧
    decide True = true
⊢ Sigma.mk (β := fun (a : α) ↦ β) a
        ((List.dlookup (β := fun (x : α) ↦ β) a (A.dedupKeys (β := fun (x : α) ↦ β))).getD 0) ∈
      A.dedupKeys (β := fun (x : α) ↦ β) ∧
    (decide ¬(List.dlookup (β := fun (x : α) ↦ β) a (A.dedupKeys (β := fun (x : α) ↦ β))).getD 0 = 0) = true

Tactic:
simp only [h, ← List.mem_dlookup_iff A.nodupKeys_dedupKeys, not_false_iff, Option.mem_def]

Premises used: List.nodupKeys_dedupKeys, List.mem_dlookup_iff, not_false_iff, Option.mem_def
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
β : Type v
inst : DecidableEq α
inst_1 : Zero β
inst_2 : DecidableEq β
a : α
A : List ((_ : α) × β)
y : β
h : ¬(List.dlookup (β := fun (x : α) ↦ β) a (A.dedupKeys (β := fun (x : α) ↦ β))).getD 0 = 0
h₁ :
  ∀ (haA : List.dlookup (β := fun (x : α) ↦ β) a (A.dedupKeys (β := fun (x : α) ↦ β)) = none),
    Eq.{v + 1} (α := Option β) none (some (Option.getD none 0)) ∧ decide True = true
h₂ :
  ∀ (val : β) (haA : List.dlookup (β := fun (x : α) ↦ β) a (A.dedupKeys (β := fun (x : α) ↦ β)) = some val),
    some val = some ((some val).getD 0) ∧ decide True = true
⊢ List.dlookup (β := fun (x : α) ↦ β) a (A.dedupKeys (β := fun (x : α) ↦ β)) =
      some ((List.dlookup (β := fun (x : α) ↦ β) a (A.dedupKeys (β := fun (x : α) ↦ β))).getD 0) ∧
    decide True = true

Tactic:
cases haA : List.dlookup a A.dedupKeys

Premises used: List.dedupKeys, List.dlookup
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
β : Type v
inst : DecidableEq α
inst_1 : Zero β
inst_2 : DecidableEq β
a : α
A : List ((_ : α) × β)
y : β
h : ¬(List.dlookup (β := fun (x : α) ↦ β) a (A.dedupKeys (β := fun (x : α) ↦ β))).getD 0 = 0
haA : List.dlookup (β := fun (x : α) ↦ β) a (A.dedupKeys (β := fun (x : α) ↦ β)) = none
⊢ Eq.{v + 1} (α := Option β) none (some (Option.getD none 0)) ∧ decide True = true

Tactic:
simp [haA] at h
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
β : Type v
inst : DecidableEq α
inst_1 : Zero β
inst_2 : DecidableEq β
a : α
A : List ((_ : α) × β)
y : β
h : ¬(List.dlookup (β := fun (x : α) ↦ β) a (A.dedupKeys (β := fun (x : α) ↦ β))).getD 0 = 0
val : β
haA : List.dlookup (β := fun (x : α) ↦ β) a (A.dedupKeys (β := fun (x : α) ↦ β)) = some val
⊢ some val = some ((some val).getD 0) ∧ decide True = true

Tactic:
simp
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
inst : DecidableEq α
xs : List (α × α)
x y z : α
simp :
  Option.getD (if h : y = x then some z else dlookup (β := fun (x : α) ↦ α) x (map Prod.toSigma xs)) x =
    if y = x then z else (dlookup (β := fun (x : α) ↦ α) x (map Prod.toSigma xs)).getD x
⊢ applyId ((y, z) :: xs) x = if y = x then z else applyId xs x

Tactic:
simp only [List.applyId, List.dlookup, eq_rec_constant, Prod.toSigma, List.map]

Premises used: Prod.toSigma, List.map, Plausible.InjectiveFunction.List.applyId, eq_rec_constant, List.dlookup
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
inst : DecidableEq α
xs : List (α × α)
x y z : α
pos : y = x → (some z).getD x = z
neg :
  ¬y = x →
    (dlookup (β := fun (x : α) ↦ α) x (map Prod.toSigma xs)).getD x =
      (dlookup (β := fun (x : α) ↦ α) x (map Prod.toSigma xs)).getD x
⊢ Option.getD (if h : y = x then some z else dlookup (β := fun (x : α) ↦ α) x (map Prod.toSigma xs)) x =
    if y = x then z else (dlookup (β := fun (x : α) ↦ α) x (map Prod.toSigma xs)).getD x

Tactic:
split_ifs
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
inst : DecidableEq α
xs : List (α × α)
x y z : α
h : y = x
⊢ (some z).getD x = z

Tactic:
rfl
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
inst : DecidableEq α
xs : List (α × α)
x y z : α
h : ¬y = x
⊢ (dlookup (β := fun (x : α) ↦ α) x (map Prod.toSigma xs)).getD x =
    (dlookup (β := fun (x : α) ↦ α) x (map Prod.toSigma xs)).getD x

Tactic:
rfl
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
inst : DecidableEq α
x y : α
ys : List α
h₀ : Nodup.{u} (α := α) []
h₁ : length.{u} (α := α) [] = ys.length
i : ℕ
h₂ : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [] i = some x
⊢ applyId (zip [] ys) x = y ↔ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) ys i = some y

Tactic:
cases 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
ys : List α
h₀ : (x' :: xs).Nodup
h₁ : (x' :: xs).length = ys.length
i : ℕ
h₂ : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x' :: xs) i = some x
cons :
  ∀ (h₂ : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x' :: xs) 0 = some x),
    applyId ((x' :: xs).zip ys) x = y ↔ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) ys 0 = some y
cons₁ :
  ∀ (n : ℕ) (h₂ : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x' :: xs) (n + 1) = some x),
    applyId ((x' :: xs).zip ys) x = y ↔
      getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) ys (n + 1) = some y
⊢ applyId ((x' :: xs).zip ys) x = y ↔ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) ys i = some y

Tactic:
cases i
-- 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
ys : List α
h₀ : (x' :: xs).Nodup
h₁ : (x' :: xs).length = ys.length
h₂ : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x' :: xs) 0 = some x
⊢ x' = x

Tactic:
simp only [length_cons, lt_add_iff_pos_left, add_pos_iff, Nat.lt_add_one, or_true,
        getElem?_eq_getElem, getElem_cons_zero, Option.some.injEq] at h₂

Premises used: List.length_cons, Option.some.injEq, Nat.lt_add_one, List.getElem_cons_zero, List.getElem?_eq_getElem, add_pos_iff, or_true, lt_add_iff_pos_left
-- 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
ys : List α
h₀ : (x' :: xs).Nodup
h₁ : (x' :: xs).length = ys.length
h₂ : x' = x
cons :
  ∀
    (xs_ih :
      ∀ {ys : List α} (h₀ : xs.Nodup) (h₁ : xs.length = ys.length) (i : ℕ)
        (h₂ : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs i = some x'),
        applyId (xs.zip ys) x' = y ↔ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) ys i = some y),
    applyId ((x' :: xs).zip ys) x' = y ↔ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) ys 0 = some y
⊢ applyId ((x' :: xs).zip ys) x = y ↔ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) ys 0 = some y

Tactic:
subst h₂
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
inst : DecidableEq α
y x' : α
xs ys : List α
h₀ : (x' :: xs).Nodup
h₁ : (x' :: xs).length = ys.length
xs_ih :
  ∀ {ys : List α} (h₀ : xs.Nodup) (h₁ : xs.length = ys.length) (i : ℕ)
    (h₂ : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs i = some x'),
    applyId (xs.zip ys) x' = y ↔ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) ys i = some y
cons :
  ∀ (h₁ : (x' :: xs).length = length.{u} (α := α) []),
    applyId ((x' :: xs).zip []) x' = y ↔ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [] 0 = some y
cons₁ :
  ∀ (head : α) (tail : List α) (h₁ : (x' :: xs).length = (head :: tail).length),
    applyId ((x' :: xs).zip (head :: tail)) x' = y ↔
      getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (head :: tail) 0 = some y
⊢ applyId ((x' :: xs).zip ys) x' = y ↔ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) ys 0 = some y

Tactic:
cases ys
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
inst : DecidableEq α
y x' : α
xs : List α
h₀ : (x' :: xs).Nodup
xs_ih :
  ∀ {ys : List α} (h₀ : xs.Nodup) (h₁ : xs.length = ys.length) (i : ℕ)
    (h₂ : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs i = some x'),
    applyId (xs.zip ys) x' = y ↔ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) ys i = some y
h₁ : (x' :: xs).length = length.{u} (α := α) []
⊢ applyId ((x' :: xs).zip []) x' = y ↔ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [] 0 = some y

Tactic:
cases h₁
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
inst : DecidableEq α
y x' : α
xs : List α
h₀ : (x' :: xs).Nodup
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
head : α
tail : List α
h₁ : (x' :: xs).length = (head :: tail).length
⊢ applyId ((x' :: xs).zip (head :: tail)) x' = y ↔
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (head :: tail) 0 = some y

Tactic:
simp
-- 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
ys : List α
h₀ : (x' :: xs).Nodup
h₁ : (x' :: xs).length = ys.length
n : ℕ
h₂ : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x' :: xs) (n + 1) = some x
cons :
  ∀ (h₁ : (x' :: xs).length = length.{u} (α := α) []),
    applyId ((x' :: xs).zip []) x = y ↔
      getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [] (n + 1) = some y
cons₁ :
  ∀ (head : α) (tail : List α) (h₁ : (x' :: xs).length = (head :: tail).length),
    applyId ((x' :: xs).zip (head :: tail)) x = y ↔
      getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (head :: tail) (n + 1) = some y
⊢ applyId ((x' :: xs).zip ys) x = y ↔ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) ys (n + 1) = some y

Tactic:
cases ys
-- 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
h₀ : (x' :: xs).Nodup
n : ℕ
h₂ : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x' :: xs) (n + 1) = some x
h₁ : (x' :: xs).length = length.{u} (α := α) []
⊢ applyId ((x' :: xs).zip []) x = y ↔ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [] (n + 1) = some y

Tactic:
cases 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
h₀ : (x' :: xs).Nodup
n : ℕ
h₂ : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x' :: xs) (n + 1) = some x
head : α
tail : List α
h₁ : (x' :: xs).length = (head :: tail).length
⊢ List.Pairwise (fun (x1 x2 : α) ↦ x1 ≠ x2) xs

Tactic:
obtain - | ⟨h₀, h₁⟩ := 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
h₀ : (x' :: xs).Nodup
n : ℕ
h₂ : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x' :: xs) (n + 1) = some x
head : α
tail : List α
h₁ : (x' :: xs).length = (head :: tail).length
h₃ : List.Pairwise (fun (x1 x2 : α) ↦ x1 ≠ x2) xs
⊢ ∀ a' ∈ xs, x' ≠ a'

Tactic:
obtain - | ⟨h₀, h₁⟩ := 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) (x' :: xs) (n + 1) = some x
head : α
tail : List α
h₁_1 : (x' :: xs).length = (head :: tail).length
h₁ : List.Pairwise (fun (x1 x2 : α) ↦ x1 ≠ x2) xs
h₀ : ∀ a' ∈ xs, x' ≠ a'
cons :
  (if x' = x then head else applyId (xs.zip tail) x) = y ↔
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) tail n = some y
⊢ applyId ((x' :: xs).zip (head :: tail)) x = y ↔
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (head :: tail) (n + 1) = some y

Tactic:
simp only [getElem?_cons_succ, zip_cons_cons, applyId_cons] at h₂ ⊢

Premises used: List.getElem?_cons_succ, Plausible.InjectiveFunction.List.applyId_cons, List.zip_cons_cons