-- Mathlib/Testing/Plausible/Functions.lean
theorem applyId_injective [DecidableEq α] {xs ys : List α} (h₀ : List.Nodup xs) (h₁ : xs ~ ys) :
    Injective.{u + 1, u + 1} (List.applyId (xs.zip ys))

Proof state:
case pos
α : 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

Tactic:
rw [h] at hx

Result:
case pos
α : 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) y ∉ ys
hy : applyId (xs.zip ys) y ∈ ys
⊢ x = y

Proof state:
case pos.intro.intro.e_a
α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
i : ℕ
h : ys[i]? = some (applyId (xs.zip ys) y)
hx : xs[i]? = some x
j : ℕ
hy : xs[j]? = some y
h₂ : xs.length = ys.length
⊢ ys[j]? = ys[i]?

Tactic:
rw [h]

Result:
case pos.intro.intro.e_a
α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
i : ℕ
h : ys[i]? = some (applyId (xs.zip ys) y)
hx : xs[i]? = some x
j : ℕ
hy : xs[j]? = some y
h₂ : xs.length = ys.length
⊢ ys[j]? = some (applyId (xs.zip ys) y)

Proof state:
case pos
α : 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

Tactic:
rw [← applyId_mem_iff h₀ h₁] at hx hy

Result:
case pos
α : 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

Proof state:
case pos.intro
α : 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, xs[i]? = some y
i : ℕ
hx : xs[i]? = some x
⊢ x = y

Tactic:
obtain ⟨j, hy⟩ := hy

Result:
case pos.intro.intro
α : 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 : xs[i]? = some x
j : ℕ
hy : xs[j]? = some y
⊢ x = y

Proof state:
case pos.intro.intro
α : 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 : xs[i]? = some x
j : ℕ
hy : xs[j]? = some y
⊢ some x = some y

Tactic:
have h₂ := h₁.length_eq

Result:
case pos.intro.intro
α : 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 : xs[i]? = some x
j : ℕ
hy : xs[j]? = some y
h₂ : xs.length = ys.length
⊢ some x = some y

Proof state:
case neg
α : 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) y ∈ ys
hy : applyId (xs.zip ys) y ∉ ys
⊢ x = y

Tactic:
contradiction

Result:
no goals

Proof state:
case neg
α : 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

Tactic:
rwa [List.applyId_eq_self, List.applyId_eq_self] at h <;> assumption

Result:
no goals

Proof state:
case pos.intro.intro
α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
i : ℕ
h : ys[i]? = some (applyId (xs.zip ys) y)
hx : xs[i]? = some x
j : ℕ
hy : xs[j]? = some y
h₂ : xs.length = ys.length
⊢ xs[i]? = xs[j]?

Tactic:
congr

Result:
case pos.intro.intro.e_a
α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
i : ℕ
h : ys[i]? = some (applyId (xs.zip ys) y)
hx : xs[i]? = some x
j : ℕ
hy : xs[j]? = some y
h₂ : xs.length = ys.length
⊢ i = j

Proof state:
case pos
α : 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, xs[i]? = some x
hy : ∃ i, xs[i]? = some y
⊢ x = y

Tactic:
obtain ⟨i, hx⟩ := hx

Result:
case pos.intro
α : 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, xs[i]? = some y
i : ℕ
hx : xs[i]? = some x
⊢ x = y

Proof state:
case pos.intro.intro.e_a
α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
i : ℕ
h : ys[i]? = some (applyId (xs.zip ys) y)
hx : xs[i]? = some x
j : ℕ
hy : xs[j]? = some y
h₂ : xs.length = ys.length
⊢ ys[i]? = ys[j]?

Tactic:
symm

Result:
case pos.intro.intro.e_a
α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
i : ℕ
h : ys[i]? = some (applyId (xs.zip ys) y)
hx : xs[i]? = some x
j : ℕ
hy : xs[j]? = some y
h₂ : xs.length = ys.length
⊢ ys[j]? = ys[i]?

Proof state:
case pos.intro.intro.e_a
α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
i : ℕ
h : ys[i]? = some (applyId (xs.zip ys) y)
hx : xs[i]? = some x
j : ℕ
hy : xs[j]? = some y
h₂ : xs.length = ys.length
⊢ ys[j]? = some (applyId (xs.zip ys) y)

Tactic:
rw [← List.applyId_zip_eq] <;> assumption

Result:
no goals

Proof state:
case pos
α : 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

Tactic:
rw [List.mem_iff_getElem?] at hx hy

Result:
case pos
α : 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, xs[i]? = some x
hy : ∃ i, xs[i]? = some y
⊢ x = y

Proof state:
case pos
α : 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) y ∉ ys
hy : applyId (xs.zip ys) y ∈ ys
⊢ x = y

Tactic:
contradiction

Result:
no goals

Proof state:
α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
⊢ Injective (applyId (xs.zip ys))

Tactic:
intro x y h

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

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

Tactic:
by_cases hx : x ∈ xs <;> by_cases hy : y ∈ xs

Result:
case pos
α : 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

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

case pos
α : 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

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

Proof state:
case intro
α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
i : ℕ
h : ys[i]? = some (applyId (xs.zip ys) y)
j : ℕ
hy : xs[j]? = some y
h₂ : xs.length = ys.length
hx : i < xs.length
hx' : xs[i] = x
⊢ i < xs.length

Tactic:
exact hx

Result:
no goals

Proof state:
case pos.intro.intro
α : 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 : xs[i]? = some x
j : ℕ
hy : xs[j]? = some y
h₂ : xs.length = ys.length
⊢ some x = some y

Tactic:
rw [List.applyId_zip_eq h₀ h₂ _ _ _ hx] at h

Result:
case pos.intro.intro
α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
i : ℕ
h : ys[i]? = some (applyId (xs.zip ys) y)
hx : xs[i]? = some x
j : ℕ
hy : xs[j]? = some y
h₂ : xs.length = ys.length
⊢ some x = some y