-- 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 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

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

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₃ : 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 (fun x => x.1) (xs.zip ys)).Nodup

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

Tactic:
dsimp [Option.getD]

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

Proof state:
case pos
α : 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₃ : some (h ▸ y) = some val
⊢ val ∈ y :: ys ↔ x ∈ x' :: xs

Tactic:
rw [Option.some_inj] at h₃

Result:
case pos
α : 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₃ : h ▸ y = val
⊢ val ∈ y :: ys ↔ x ∈ 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₅ : 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

Tactic:
rcases h₃ with ⟨a, b, h₃, h₄, h₅⟩

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

Proof state:
case some.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)
ys : List α
h₀ : (x' :: xs).Nodup
h₃ : dlookup x (map Prod.toSigma ((x' :: xs).zip ys)) = some val
h₂ : ys.Nodup
h₁ : (x' :: xs).length = ys.length
⊢ val ∈ ys ↔ x ∈ x' :: xs

Tactic:
rcases ys with - | ⟨y, ys⟩

Result:
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

case some.cons.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)
h₀ : (x' :: xs).Nodup
y : α
ys : List α
h₃ : dlookup x (map Prod.toSigma ((x' :: xs).zip (y :: ys))) = some val
h₂ : (y :: ys).Nodup
h₁ : (x' :: xs).length = (y :: ys).length
⊢ val ∈ y :: ys ↔ x ∈ 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 = y ∨ x ∈ xs ↔ False ∨ x ∈ xs

Tactic:
suffices val ∈ ys by tauto

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 ∈ ys

Proof state:
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

Tactic:
obtain - | ⟨h₂, h₄⟩ := h₂

Result:
case neg.cons.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₁ : (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'
⊢ val ∈ y :: ys ↔ x ∈ x' :: xs

Proof state:
case pos
α : Type u
inst✝ : DecidableEq α
x val : α
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).Nodup
h₁ : (x :: xs).length = (y :: ys).length
h₃ : ⋯ ▸ y = val
⊢ val ∈ y :: ys ↔ x ∈ x :: xs

Tactic:
subst val

Result:
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