-- Mathlib/Testing/Plausible/Functions.lean
theorem applyId_mem_iff [DecidableEq α] {xs ys : List α} (h₀ : List.Nodup xs) (h₁ : xs ~ ys)
    (x : α) : List.applyId.{u} (xs.zip ys) x ∈ ys ↔ x ∈ xs

Proof state:
case some.cons.nil
α : Type u
inst✝ : DecidableEq α
x val x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    xs.Nodup →
      dlookup x (map Prod.toSigma (xs.zip ys)) = some val → ys.Nodup → xs.length = ys.length → (val ∈ ys ↔ x ∈ xs)
h₀ : (x' :: xs).Nodup
h₃ : dlookup x (map Prod.toSigma ((x' :: xs).zip [])) = some val
h₂ : [].Nodup
h₁ : (x' :: xs).length = [].length
⊢ val ∈ [] ↔ x ∈ x' :: xs

Tactic:
cases h₃

Result:
no goals

Proof state:
case some
α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x val : α
h₃ : dlookup x (map Prod.toSigma (xs.zip ys)) = some val
⊢ (some val).getD x ∈ ys ↔ x ∈ xs

Tactic:
have h₂ : ys.Nodup := h₁.nodup_iff.1 h₀

Result:
case some
α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x val : α
h₃ : dlookup x (map Prod.toSigma (xs.zip ys)) = some val
h₂ : ys.Nodup
⊢ (some val).getD x ∈ ys ↔ x ∈ xs

Proof state:
case neg.cons.cons
α : Type u
inst✝ : DecidableEq α
x val x' : α
xs : List α
y : α
ys : List α
h₁ : (x' :: xs).length = (y :: ys).length
h : ¬x' = x
h₃ : dlookup 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

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

Result:
case neg.cons.cons
α : Type u
inst✝ : DecidableEq α
x val x' : α
xs : List α
y : α
ys : List α
h₁ : (x' :: xs).length = (y :: ys).length
h : ¬x' = x
h₃ : ⟨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

case neg.cons.cons
α : 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 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

Proof state:
case neg.cons.cons
α : Type u
inst✝ : DecidableEq α
x val x' : α
xs : List α
y : α
ys : List α
h₁ : (x' :: xs).length = (y :: ys).length
h : ¬x' = x
h₃ : dlookup 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

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

Result:
case neg.cons.cons
α : Type u
inst✝ : DecidableEq α
x val x' : α
xs : List α
y : α
ys : List α
h₁ : (x' :: xs).length = (y :: ys).length
h : ¬x' = x
h₃ : dlookup 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

Proof state:
case pos
α : Type u
inst✝ : DecidableEq α
x : α
xs : List α
y : α
ys : List α
h₂ : (y :: ys).Nodup
h₀ : (x :: xs).Nodup
h₁ : (x :: xs).length = (y :: ys).length
xs_ih :
  ∀ {ys : List α},
    xs.Nodup →
      dlookup x (map Prod.toSigma (xs.zip ys)) = some (⋯ ▸ y) → ys.Nodup → xs.length = ys.length → (⋯ ▸ y ∈ ys ↔ x ∈ xs)
⊢ ⋯ ▸ y ∈ y :: ys ↔ x ∈ x :: xs

Tactic:
simp only [List.mem_cons, true_or, eq_self_iff_true]

Result:
no goals

Proof state:
case neg
α : Type u
inst✝ : DecidableEq α
x val x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    xs.Nodup →
      dlookup x (map Prod.toSigma (xs.zip ys)) = some val → ys.Nodup → 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 x (map Prod.toSigma (xs.zip ys)) = some val
⊢ val ∈ y :: ys ↔ x ∈ x' :: xs

Tactic:
obtain - | ⟨h₀, h₅⟩ := h₀

Result:
case neg.cons
α : Type u
inst✝ : DecidableEq α
x val x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    xs.Nodup →
      dlookup x (map Prod.toSigma (xs.zip ys)) = some val → ys.Nodup → 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 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

Proof state:
case some
α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
x val : α
h₃ : dlookup x (map Prod.toSigma (xs.zip ys)) = some val
h₂ : ys.Nodup
h₁ : xs.length = ys.length
⊢ (some val).getD x ∈ ys ↔ x ∈ xs

Tactic:
dsimp

Result:
case some
α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
x val : α
h₃ : dlookup x (map Prod.toSigma (xs.zip ys)) = some val
h₂ : ys.Nodup
h₁ : xs.length = ys.length
⊢ val ∈ ys ↔ x ∈ xs

Proof state:
case neg.cons.cons
α : Type u
inst✝ : DecidableEq α
x val x' : α
xs : List α
y : α
ys : List α
h₁ : (x' :: xs).length = (y :: ys).length
h : ¬x' = x
h₃ : ⟨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:
simp only [Prod.toSigma, List.mem_map, heq_iff_eq, Prod.exists] at h₃

Result:
case neg.cons.cons
α : 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 ∧ ⟨a, b⟩ = ⟨x, val⟩
⊢ val ∈ ys

Proof state:
case some
α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x val : α
h₃ : dlookup x (map Prod.toSigma (xs.zip ys)) = some val
h₂ : ys.Nodup
⊢ (some val).getD x ∈ ys ↔ x ∈ xs

Tactic:
replace h₁ : xs.length = ys.length := h₁.length_eq

Result:
case some
α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
x val : α
h₃ : dlookup x (map Prod.toSigma (xs.zip ys)) = some val
h₂ : ys.Nodup
h₁ : xs.length = ys.length
⊢ (some val).getD x ∈ ys ↔ x ∈ xs