Theorem: List.nodup_eq_len_imp_exists_bijon (FOL/List.lean)

State before:
α : Type
inst✝ : DecidableEq α
xs ys : List α
h1 : xs.length = ys.length
h2 : xs.Nodup
h3 : ys.Nodup
⊢ ∃ f, InjOn f xs ∧ map f xs = ys
Tactic:
induction xs generalizing ys
State after:
case nil
α : Type
inst✝ : DecidableEq α
ys : List α
h1 : [].length = ys.length
h2 : [].Nodup
h3 : ys.Nodup
⊢ ∃ f, InjOn f [] ∧ map f [] = ys

case cons
α : Type
inst✝ : DecidableEq α
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (ys : List α), tail✝.length = ys.length → tail✝.Nodup → ys.Nodup → ∃ f, InjOn f tail✝ ∧ map f tail✝ = ys
ys : List α
h1 : (head✝ :: tail✝).length = ys.length
h2 : (head✝ :: tail✝).Nodup
h3 : ys.Nodup
⊢ ∃ f, InjOn f (head✝ :: tail✝) ∧ map f (head✝ :: tail✝) = ys

State before:
α : Type
inst✝ : DecidableEq α
ys : List α
h1 : [].length = ys.length
h2 : [].Nodup
h3 : ys.Nodup
⊢ ∃ f, InjOn f [] ∧ map f [] = ys
Tactic:
have s1 : ys = []
State after:
case s1
α : Type
inst✝ : DecidableEq α
ys : List α
h1 : [].length = ys.length
h2 : [].Nodup
h3 : ys.Nodup
⊢ ys = []

α : Type
inst✝ : DecidableEq α
ys : List α
h1 : [].length = ys.length
h2 : [].Nodup
h3 : ys.Nodup
s1 : ys = []
⊢ ∃ f, InjOn f [] ∧ map f [] = ys

State before:
case s1
α : Type
inst✝ : DecidableEq α
ys : List α
h1 : [].length = ys.length
h2 : [].Nodup
h3 : ys.Nodup
⊢ ys = []

α : Type
inst✝ : DecidableEq α
ys : List α
h1 : [].length = ys.length
h2 : [].Nodup
h3 : ys.Nodup
s1 : ys = []
⊢ ∃ f, InjOn f [] ∧ map f [] = ys
Tactic:
{
  apply List.eq_nil_of_length_eq_zero
  simp only [← h1]
  simp
}
State after:
α : Type
inst✝ : DecidableEq α
ys : List α
h1 : [].length = ys.length
h2 : [].Nodup
h3 : ys.Nodup
s1 : ys = []
⊢ ∃ f, InjOn f [] ∧ map f [] = ys

State before:
α : Type
inst✝ : DecidableEq α
ys : List α
h1 : [].length = ys.length
h2 : [].Nodup
h3 : ys.Nodup
s1 : ys = []
⊢ ∃ f, InjOn f [] ∧ map f [] = ys
Tactic:
simp only [s1]
State after:
α : Type
inst✝ : DecidableEq α
ys : List α
h1 : [].length = ys.length
h2 : [].Nodup
h3 : ys.Nodup
s1 : ys = []
⊢ ∃ f, InjOn f [] ∧ map f [] = []

State before:
α : Type
inst✝ : DecidableEq α
ys : List α
h1 : [].length = ys.length
h2 : [].Nodup
h3 : ys.Nodup
s1 : ys = []
⊢ ∃ f, InjOn f [] ∧ map f [] = []
Tactic:
apply Exists.intro id
State after:
α : Type
inst✝ : DecidableEq α
ys : List α
h1 : [].length = ys.length
h2 : [].Nodup
h3 : ys.Nodup
s1 : ys = []
⊢ InjOn id [] ∧ map id [] = []

State before:
α : Type
inst✝ : DecidableEq α
ys : List α
h1 : [].length = ys.length
h2 : [].Nodup
h3 : ys.Nodup
s1 : ys = []
⊢ InjOn id [] ∧ map id [] = []
Tactic:
constructor
State after:
case left
α : Type
inst✝ : DecidableEq α
ys : List α
h1 : [].length = ys.length
h2 : [].Nodup
h3 : ys.Nodup
s1 : ys = []
⊢ InjOn id []

case right
α : Type
inst✝ : DecidableEq α
ys : List α
h1 : [].length = ys.length
h2 : [].Nodup
h3 : ys.Nodup
s1 : ys = []
⊢ map id [] = []

State before:
case s1
α : Type
inst✝ : DecidableEq α
ys : List α
h1 : [].length = ys.length
h2 : [].Nodup
h3 : ys.Nodup
⊢ ys = []
Tactic:
apply List.eq_nil_of_length_eq_zero
State after:
case s1.x
α : Type
inst✝ : DecidableEq α
ys : List α
h1 : [].length = ys.length
h2 : [].Nodup
h3 : ys.Nodup
⊢ ys.length = 0

State before:
case s1.x
α : Type
inst✝ : DecidableEq α
ys : List α
h1 : [].length = ys.length
h2 : [].Nodup
h3 : ys.Nodup
⊢ ys.length = 0
Tactic:
simp only [← h1]
State after:
case s1.x
α : Type
inst✝ : DecidableEq α
ys : List α
h1 : [].length = ys.length
h2 : [].Nodup
h3 : ys.Nodup
⊢ [].length = 0

State before:
case s1.x
α : Type
inst✝ : DecidableEq α
ys : List α
h1 : [].length = ys.length
h2 : [].Nodup
h3 : ys.Nodup
⊢ [].length = 0
Tactic:
simp
State after:
no goals

State before:
case left
α : Type
inst✝ : DecidableEq α
ys : List α
h1 : [].length = ys.length
h2 : [].Nodup
h3 : ys.Nodup
s1 : ys = []
⊢ InjOn id []
Tactic:
simp only [List.InjOn]
State after:
case left
α : Type
inst✝ : DecidableEq α
ys : List α
h1 : [].length = ys.length
h2 : [].Nodup
h3 : ys.Nodup
s1 : ys = []
⊢ ∀ ⦃x₁ : α⦄, x₁ ∈ [] → ∀ ⦃x₂ : α⦄, x₂ ∈ [] → id x₁ = id x₂ → x₁ = x₂

State before:
case left
α : Type
inst✝ : DecidableEq α
ys : List α
h1 : [].length = ys.length
h2 : [].Nodup
h3 : ys.Nodup
s1 : ys = []
⊢ ∀ ⦃x₁ : α⦄, x₁ ∈ [] → ∀ ⦃x₂ : α⦄, x₂ ∈ [] → id x₁ = id x₂ → x₁ = x₂
Tactic:
simp
State after:
no goals

State before:
case right
α : Type
inst✝ : DecidableEq α
ys : List α
h1 : [].length = ys.length
h2 : [].Nodup
h3 : ys.Nodup
s1 : ys = []
⊢ map id [] = []
Tactic:
simp
State after:
no goals

State before:
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List α), xs_tl.length = ys.length → xs_tl.Nodup → ys.Nodup → ∃ f, InjOn f xs_tl ∧ map f xs_tl = ys
ys : List α
h1 : (xs_hd :: xs_tl).length = ys.length
h2 : (xs_hd :: xs_tl).Nodup
h3 : ys.Nodup
⊢ ∃ f, InjOn f (xs_hd :: xs_tl) ∧ map f (xs_hd :: xs_tl) = ys
Tactic:
cases ys
State after:
case nil
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List α), xs_tl.length = ys.length → xs_tl.Nodup → ys.Nodup → ∃ f, InjOn f xs_tl ∧ map f xs_tl = ys
h2 : (xs_hd :: xs_tl).Nodup
h1 : (xs_hd :: xs_tl).length = [].length
h3 : [].Nodup
⊢ ∃ f, InjOn f (xs_hd :: xs_tl) ∧ map f (xs_hd :: xs_tl) = []

case cons
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List α), xs_tl.length = ys.length → xs_tl.Nodup → ys.Nodup → ∃ f, InjOn f xs_tl ∧ map f xs_tl = ys
h2 : (xs_hd :: xs_tl).Nodup
head✝ : α
tail✝ : List α
h1 : (xs_hd :: xs_tl).length = (head✝ :: tail✝).length
h3 : (head✝ :: tail✝).Nodup
⊢ ∃ f, InjOn f (xs_hd :: xs_tl) ∧ map f (xs_hd :: xs_tl) = head✝ :: tail✝

State before:
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List α), xs_tl.length = ys.length → xs_tl.Nodup → ys.Nodup → ∃ f, InjOn f xs_tl ∧ map f xs_tl = ys
h2 : (xs_hd :: xs_tl).Nodup
h1 : (xs_hd :: xs_tl).length = [].length
h3 : [].Nodup
⊢ ∃ f, InjOn f (xs_hd :: xs_tl) ∧ map f (xs_hd :: xs_tl) = []
Tactic:
case nil =>
  simp at h1
State after:
no goals

State before:
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List α), xs_tl.length = ys.length → xs_tl.Nodup → ys.Nodup → ∃ f, InjOn f xs_tl ∧ map f xs_tl = ys
h2 : (xs_hd :: xs_tl).Nodup
h1 : (xs_hd :: xs_tl).length = [].length
h3 : [].Nodup
⊢ ∃ f, InjOn f (xs_hd :: xs_tl) ∧ map f (xs_hd :: xs_tl) = []
Tactic:
simp at h1
State after:
no goals

State before:
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List α), xs_tl.length = ys.length → xs_tl.Nodup → ys.Nodup → ∃ f, InjOn f xs_tl ∧ map f xs_tl = ys
h2 : (xs_hd :: xs_tl).Nodup
ys_hd : α
ys_tl : List α
h1 : (xs_hd :: xs_tl).length = (ys_hd :: ys_tl).length
h3 : (ys_hd :: ys_tl).Nodup
⊢ ∃ f, InjOn f (xs_hd :: xs_tl) ∧ map f (xs_hd :: xs_tl) = ys_hd :: ys_tl
Tactic:
simp at h1
State after:
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List α), xs_tl.length = ys.length → xs_tl.Nodup → ys.Nodup → ∃ f, InjOn f xs_tl ∧ map f xs_tl = ys
h2 : (xs_hd :: xs_tl).Nodup
ys_hd : α
ys_tl : List α
h3 : (ys_hd :: ys_tl).Nodup
h1 : xs_tl.length = ys_tl.length
⊢ ∃ f, InjOn f (xs_hd :: xs_tl) ∧ map f (xs_hd :: xs_tl) = ys_hd :: ys_tl

State before:
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List α), xs_tl.length = ys.length → xs_tl.Nodup → ys.Nodup → ∃ f, InjOn f xs_tl ∧ map f xs_tl = ys
h2 : (xs_hd :: xs_tl).Nodup
ys_hd : α
ys_tl : List α
h3 : (ys_hd :: ys_tl).Nodup
h1 : xs_tl.length = ys_tl.length
⊢ ∃ f, InjOn f (xs_hd :: xs_tl) ∧ map f (xs_hd :: xs_tl) = ys_hd :: ys_tl
Tactic:
simp at h2
State after:
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List α), xs_tl.length = ys.length → xs_tl.Nodup → ys.Nodup → ∃ f, InjOn f xs_tl ∧ map f xs_tl = ys
ys_hd : α
ys_tl : List α
h3 : (ys_hd :: ys_tl).Nodup
h1 : xs_tl.length = ys_tl.length
h2 : xs_hd ∉ xs_tl ∧ xs_tl.Nodup
⊢ ∃ f, InjOn f (xs_hd :: xs_tl) ∧ map f (xs_hd :: xs_tl) = ys_hd :: ys_tl

State before:
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List α), xs_tl.length = ys.length → xs_tl.Nodup → ys.Nodup → ∃ f, InjOn f xs_tl ∧ map f xs_tl = ys
ys_hd : α
ys_tl : List α
h3 : (ys_hd :: ys_tl).Nodup
h1 : xs_tl.length = ys_tl.length
h2 : xs_hd ∉ xs_tl ∧ xs_tl.Nodup
⊢ ∃ f, InjOn f (xs_hd :: xs_tl) ∧ map f (xs_hd :: xs_tl) = ys_hd :: ys_tl
Tactic:
simp at h3
State after:
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List α), xs_tl.length = ys.length → xs_tl.Nodup → ys.Nodup → ∃ f, InjOn f xs_tl ∧ map f xs_tl = ys
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2 : xs_hd ∉ xs_tl ∧ xs_tl.Nodup
h3 : ys_hd ∉ ys_tl ∧ ys_tl.Nodup
⊢ ∃ f, InjOn f (xs_hd :: xs_tl) ∧ map f (xs_hd :: xs_tl) = ys_hd :: ys_tl

State before:
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List α), xs_tl.length = ys.length → xs_tl.Nodup → ys.Nodup → ∃ f, InjOn f xs_tl ∧ map f xs_tl = ys
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2 : xs_hd ∉ xs_tl ∧ xs_tl.Nodup
h3 : ys_hd ∉ ys_tl ∧ ys_tl.Nodup
⊢ ∃ f, InjOn f (xs_hd :: xs_tl) ∧ map f (xs_hd :: xs_tl) = ys_hd :: ys_tl
Tactic:
cases h2
State after:
case intro
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List α), xs_tl.length = ys.length → xs_tl.Nodup → ys.Nodup → ∃ f, InjOn f xs_tl ∧ map f xs_tl = ys
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h3 : ys_hd ∉ ys_tl ∧ ys_tl.Nodup
left✝ : xs_hd ∉ xs_tl
right✝ : xs_tl.Nodup
⊢ ∃ f, InjOn f (xs_hd :: xs_tl) ∧ map f (xs_hd :: xs_tl) = ys_hd :: ys_tl

State before:
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List α), xs_tl.length = ys.length → xs_tl.Nodup → ys.Nodup → ∃ f, InjOn f xs_tl ∧ map f xs_tl = ys
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h3 : ys_hd ∉ ys_tl ∧ ys_tl.Nodup
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
⊢ ∃ f, InjOn f (xs_hd :: xs_tl) ∧ map f (xs_hd :: xs_tl) = ys_hd :: ys_tl
Tactic:
cases h3
State after:
case intro
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List α), xs_tl.length = ys.length → xs_tl.Nodup → ys.Nodup → ∃ f, InjOn f xs_tl ∧ map f xs_tl = ys
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
left✝ : ys_hd ∉ ys_tl
right✝ : ys_tl.Nodup
⊢ ∃ f, InjOn f (xs_hd :: xs_tl) ∧ map f (xs_hd :: xs_tl) = ys_hd :: ys_tl

State before:
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List α), xs_tl.length = ys.length → xs_tl.Nodup → ys.Nodup → ∃ f, InjOn f xs_tl ∧ map f xs_tl = ys
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
⊢ ∃ f, InjOn f (xs_hd :: xs_tl) ∧ map f (xs_hd :: xs_tl) = ys_hd :: ys_tl
Tactic:
simp
State after:
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List α), xs_tl.length = ys.length → xs_tl.Nodup → ys.Nodup → ∃ f, InjOn f xs_tl ∧ map f xs_tl = ys
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
⊢ ∃ f, InjOn f (xs_hd :: xs_tl) ∧ f xs_hd = ys_hd ∧ map f xs_tl = ys_tl

State before:
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List α), xs_tl.length = ys.length → xs_tl.Nodup → ys.Nodup → ∃ f, InjOn f xs_tl ∧ map f xs_tl = ys
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
⊢ ∃ f, InjOn f (xs_hd :: xs_tl) ∧ f xs_hd = ys_hd ∧ map f xs_tl = ys_tl
Tactic:
specialize xs_ih ys_tl h1 h2_right h3_right
State after:
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
xs_ih : ∃ f, InjOn f xs_tl ∧ map f xs_tl = ys_tl
⊢ ∃ f, InjOn f (xs_hd :: xs_tl) ∧ f xs_hd = ys_hd ∧ map f xs_tl = ys_tl

State before:
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
xs_ih : ∃ f, InjOn f xs_tl ∧ map f xs_tl = ys_tl
⊢ ∃ f, InjOn f (xs_hd :: xs_tl) ∧ f xs_hd = ys_hd ∧ map f xs_tl = ys_tl
Tactic:
apply Exists.elim xs_ih
State after:
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
xs_ih : ∃ f, InjOn f xs_tl ∧ map f xs_tl = ys_tl
⊢ ∀ (a : α → α),
    InjOn a xs_tl ∧ map a xs_tl = ys_tl → ∃ f, InjOn f (xs_hd :: xs_tl) ∧ f xs_hd = ys_hd ∧ map f xs_tl = ys_tl

State before:
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
xs_ih : ∃ f, InjOn f xs_tl ∧ map f xs_tl = ys_tl
⊢ ∀ (a : α → α),
    InjOn a xs_tl ∧ map a xs_tl = ys_tl → ∃ f, InjOn f (xs_hd :: xs_tl) ∧ f xs_hd = ys_hd ∧ map f xs_tl = ys_tl
Tactic:
intro f a1
State after:
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
xs_ih : ∃ f, InjOn f xs_tl ∧ map f xs_tl = ys_tl
f : α → α
a1 : InjOn f xs_tl ∧ map f xs_tl = ys_tl
⊢ ∃ f, InjOn f (xs_hd :: xs_tl) ∧ f xs_hd = ys_hd ∧ map f xs_tl = ys_tl

State before:
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
xs_ih : ∃ f, InjOn f xs_tl ∧ map f xs_tl = ys_tl
f : α → α
a1 : InjOn f xs_tl ∧ map f xs_tl = ys_tl
⊢ ∃ f, InjOn f (xs_hd :: xs_tl) ∧ f xs_hd = ys_hd ∧ map f xs_tl = ys_tl
Tactic:
clear xs_ih
State after:
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1 : InjOn f xs_tl ∧ map f xs_tl = ys_tl
⊢ ∃ f, InjOn f (xs_hd :: xs_tl) ∧ f xs_hd = ys_hd ∧ map f xs_tl = ys_tl

State before:
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1 : InjOn f xs_tl ∧ map f xs_tl = ys_tl
⊢ ∃ f, InjOn f (xs_hd :: xs_tl) ∧ f xs_hd = ys_hd ∧ map f xs_tl = ys_tl
Tactic:
simp only [List.InjOn]
State after:
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1 : InjOn f xs_tl ∧ map f xs_tl = ys_tl
⊢ ∃ f,
    (∀ ⦃x₁ : α⦄, x₁ ∈ xs_hd :: xs_tl → ∀ ⦃x₂ : α⦄, x₂ ∈ xs_hd :: xs_tl → f x₁ = f x₂ → x₁ = x₂) ∧
      f xs_hd = ys_hd ∧ map f xs_tl = ys_tl

State before:
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1 : InjOn f xs_tl ∧ map f xs_tl = ys_tl
⊢ ∃ f,
    (∀ ⦃x₁ : α⦄, x₁ ∈ xs_hd :: xs_tl → ∀ ⦃x₂ : α⦄, x₂ ∈ xs_hd :: xs_tl → f x₁ = f x₂ → x₁ = x₂) ∧
      f xs_hd = ys_hd ∧ map f xs_tl = ys_tl
Tactic:
cases a1
State after:
case intro
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
left✝ : InjOn f xs_tl
right✝ : map f xs_tl = ys_tl
⊢ ∃ f,
    (∀ ⦃x₁ : α⦄, x₁ ∈ xs_hd :: xs_tl → ∀ ⦃x₂ : α⦄, x₂ ∈ xs_hd :: xs_tl → f x₁ = f x₂ → x₁ = x₂) ∧
      f xs_hd = ys_hd ∧ map f xs_tl = ys_tl

State before:
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
⊢ ∃ f,
    (∀ ⦃x₁ : α⦄, x₁ ∈ xs_hd :: xs_tl → ∀ ⦃x₂ : α⦄, x₂ ∈ xs_hd :: xs_tl → f x₁ = f x₂ → x₁ = x₂) ∧
      f xs_hd = ys_hd ∧ map f xs_tl = ys_tl
Tactic:
apply Exists.intro (Function.updateITE f xs_hd ys_hd)
State after:
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
⊢ (∀ ⦃x₁ : α⦄,
      x₁ ∈ xs_hd :: xs_tl →
        ∀ ⦃x₂ : α⦄,
          x₂ ∈ xs_hd :: xs_tl → Function.updateITE f xs_hd ys_hd x₁ = Function.updateITE f xs_hd ys_hd x₂ → x₁ = x₂) ∧
    Function.updateITE f xs_hd ys_hd xs_hd = ys_hd ∧ map (Function.updateITE f xs_hd ys_hd) xs_tl = ys_tl

State before:
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
⊢ (∀ ⦃x₁ : α⦄,
      x₁ ∈ xs_hd :: xs_tl →
        ∀ ⦃x₂ : α⦄,
          x₂ ∈ xs_hd :: xs_tl → Function.updateITE f xs_hd ys_hd x₁ = Function.updateITE f xs_hd ys_hd x₂ → x₁ = x₂) ∧
    Function.updateITE f xs_hd ys_hd xs_hd = ys_hd ∧ map (Function.updateITE f xs_hd ys_hd) xs_tl = ys_tl
Tactic:
constructor
State after:
case left
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
⊢ ∀ ⦃x₁ : α⦄,
    x₁ ∈ xs_hd :: xs_tl →
      ∀ ⦃x₂ : α⦄,
        x₂ ∈ xs_hd :: xs_tl → Function.updateITE f xs_hd ys_hd x₁ = Function.updateITE f xs_hd ys_hd x₂ → x₁ = x₂

case right
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
⊢ Function.updateITE f xs_hd ys_hd xs_hd = ys_hd ∧ map (Function.updateITE f xs_hd ys_hd) xs_tl = ys_tl

State before:
case left
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
⊢ ∀ ⦃x₁ : α⦄,
    x₁ ∈ xs_hd :: xs_tl →
      ∀ ⦃x₂ : α⦄,
        x₂ ∈ xs_hd :: xs_tl → Function.updateITE f xs_hd ys_hd x₁ = Function.updateITE f xs_hd ys_hd x₂ → x₁ = x₂
Tactic:
intro x1 x1_mem x2 x2_mem
State after:
case left
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
x1 : α
x1_mem : x1 ∈ xs_hd :: xs_tl
x2 : α
x2_mem : x2 ∈ xs_hd :: xs_tl
⊢ Function.updateITE f xs_hd ys_hd x1 = Function.updateITE f xs_hd ys_hd x2 → x1 = x2

State before:
case left
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
x1 : α
x1_mem : x1 ∈ xs_hd :: xs_tl
x2 : α
x2_mem : x2 ∈ xs_hd :: xs_tl
⊢ Function.updateITE f xs_hd ys_hd x1 = Function.updateITE f xs_hd ys_hd x2 → x1 = x2
Tactic:
simp at x1_mem
State after:
case left
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
x1 x2 : α
x2_mem : x2 ∈ xs_hd :: xs_tl
x1_mem : x1 = xs_hd ∨ x1 ∈ xs_tl
⊢ Function.updateITE f xs_hd ys_hd x1 = Function.updateITE f xs_hd ys_hd x2 → x1 = x2

State before:
case left
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
x1 x2 : α
x2_mem : x2 ∈ xs_hd :: xs_tl
x1_mem : x1 = xs_hd ∨ x1 ∈ xs_tl
⊢ Function.updateITE f xs_hd ys_hd x1 = Function.updateITE f xs_hd ys_hd x2 → x1 = x2
Tactic:
simp at x2_mem
State after:
case left
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
x1 x2 : α
x1_mem : x1 = xs_hd ∨ x1 ∈ xs_tl
x2_mem : x2 = xs_hd ∨ x2 ∈ xs_tl
⊢ Function.updateITE f xs_hd ys_hd x1 = Function.updateITE f xs_hd ys_hd x2 → x1 = x2

State before:
case left
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
x1 x2 : α
x1_mem : x1 = xs_hd ∨ x1 ∈ xs_tl
x2_mem : x2 = xs_hd ∨ x2 ∈ xs_tl
⊢ Function.updateITE f xs_hd ys_hd x1 = Function.updateITE f xs_hd ys_hd x2 → x1 = x2
Tactic:
simp only [Function.updateITE]
State after:
case left
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
x1 x2 : α
x1_mem : x1 = xs_hd ∨ x1 ∈ xs_tl
x2_mem : x2 = xs_hd ∨ x2 ∈ xs_tl
⊢ ((if x1 = xs_hd then ys_hd else f x1) = if x2 = xs_hd then ys_hd else f x2) → x1 = x2

State before:
case left
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
x1 x2 : α
x1_mem : x1 = xs_hd ∨ x1 ∈ xs_tl
x2_mem : x2 = xs_hd ∨ x2 ∈ xs_tl
⊢ ((if x1 = xs_hd then ys_hd else f x1) = if x2 = xs_hd then ys_hd else f x2) → x1 = x2
Tactic:
split_ifs
State after:
case pos
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
x1 x2 : α
x1_mem : x1 = xs_hd ∨ x1 ∈ xs_tl
x2_mem : x2 = xs_hd ∨ x2 ∈ xs_tl
h✝¹ : x1 = xs_hd
h✝ : x2 = xs_hd
⊢ ys_hd = ys_hd → x1 = x2

case neg
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
x1 x2 : α
x1_mem : x1 = xs_hd ∨ x1 ∈ xs_tl
x2_mem : x2 = xs_hd ∨ x2 ∈ xs_tl
h✝¹ : x1 = xs_hd
h✝ : ¬x2 = xs_hd
⊢ ys_hd = f x2 → x1 = x2

case pos
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
x1 x2 : α
x1_mem : x1 = xs_hd ∨ x1 ∈ xs_tl
x2_mem : x2 = xs_hd ∨ x2 ∈ xs_tl
h✝¹ : ¬x1 = xs_hd
h✝ : x2 = xs_hd
⊢ f x1 = ys_hd → x1 = x2

case neg
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
x1 x2 : α
x1_mem : x1 = xs_hd ∨ x1 ∈ xs_tl
x2_mem : x2 = xs_hd ∨ x2 ∈ xs_tl
h✝¹ : ¬x1 = xs_hd
h✝ : ¬x2 = xs_hd
⊢ f x1 = f x2 → x1 = x2

State before:
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
x1 x2 : α
x1_mem : x1 = xs_hd ∨ x1 ∈ xs_tl
x2_mem : x2 = xs_hd ∨ x2 ∈ xs_tl
c1 : x1 = xs_hd
c2 : x2 = xs_hd
⊢ ys_hd = ys_hd → x1 = x2
Tactic:
case _ c1 c2 =>
  intro _
  simp only [c1]
  simp only [c2]
State after:
no goals

State before:
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
x1 x2 : α
x1_mem : x1 = xs_hd ∨ x1 ∈ xs_tl
x2_mem : x2 = xs_hd ∨ x2 ∈ xs_tl
c1 : x1 = xs_hd
c2 : ¬x2 = xs_hd
⊢ ys_hd = f x2 → x1 = x2
Tactic:
case _ c1 c2 =>
  intro a2
  cases x2_mem
  case inl c3 =>
    contradiction
  case inr c3 =>
    obtain s1 := List.mem_map_of_mem f c3
    simp only [a1_right] at s1
    simp only [← a2] at s1
    contradiction
State after:
no goals

State before:
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
x1 x2 : α
x1_mem : x1 = xs_hd ∨ x1 ∈ xs_tl
x2_mem : x2 = xs_hd ∨ x2 ∈ xs_tl
c1 : ¬x1 = xs_hd
c2 : x2 = xs_hd
⊢ f x1 = ys_hd → x1 = x2
Tactic:
case _ c1 c2 =>
  intro a2
  cases x1_mem
  case inl c3 =>
    contradiction
  case inr c3 =>
    obtain s1 := List.mem_map_of_mem f c3
    simp only [a1_right] at s1
    simp only [a2] at s1
    contradiction
State after:
no goals

State before:
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
x1 x2 : α
x1_mem : x1 = xs_hd ∨ x1 ∈ xs_tl
x2_mem : x2 = xs_hd ∨ x2 ∈ xs_tl
c1 : ¬x1 = xs_hd
c2 : ¬x2 = xs_hd
⊢ f x1 = f x2 → x1 = x2
Tactic:
case _ c1 c2 =>
  intro a2
  cases x1_mem
  case inl x1_mem_left =>
    contradiction
  case inr x1_mem_right =>
    cases x2_mem
    case inl x2_mem_left =>
      contradiction
    case inr x2_mem_right =>
      simp only [List.InjOn] at a1_left
      apply a1_left x1_mem_right x2_mem_right a2
State after:
no goals

State before:
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
x1 x2 : α
x1_mem : x1 = xs_hd ∨ x1 ∈ xs_tl
x2_mem : x2 = xs_hd ∨ x2 ∈ xs_tl
c1 : x1 = xs_hd
c2 : x2 = xs_hd
⊢ ys_hd = ys_hd → x1 = x2
Tactic:
intro _
State after:
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
x1 x2 : α
x1_mem : x1 = xs_hd ∨ x1 ∈ xs_tl
x2_mem : x2 = xs_hd ∨ x2 ∈ xs_tl
c1 : x1 = xs_hd
c2 : x2 = xs_hd
a✝ : ys_hd = ys_hd
⊢ x1 = x2

State before:
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
x1 x2 : α
x1_mem : x1 = xs_hd ∨ x1 ∈ xs_tl
x2_mem : x2 = xs_hd ∨ x2 ∈ xs_tl
c1 : x1 = xs_hd
c2 : x2 = xs_hd
a✝ : ys_hd = ys_hd
⊢ x1 = x2
Tactic:
simp only [c1]
State after:
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
x1 x2 : α
x1_mem : x1 = xs_hd ∨ x1 ∈ xs_tl
x2_mem : x2 = xs_hd ∨ x2 ∈ xs_tl
c1 : x1 = xs_hd
c2 : x2 = xs_hd
a✝ : ys_hd = ys_hd
⊢ xs_hd = x2

State before:
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
x1 x2 : α
x1_mem : x1 = xs_hd ∨ x1 ∈ xs_tl
x2_mem : x2 = xs_hd ∨ x2 ∈ xs_tl
c1 : x1 = xs_hd
c2 : x2 = xs_hd
a✝ : ys_hd = ys_hd
⊢ xs_hd = x2
Tactic:
simp only [c2]
State after:
no goals

State before:
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
x1 x2 : α
x1_mem : x1 = xs_hd ∨ x1 ∈ xs_tl
x2_mem : x2 = xs_hd ∨ x2 ∈ xs_tl
c1 : x1 = xs_hd
c2 : ¬x2 = xs_hd
⊢ ys_hd = f x2 → x1 = x2
Tactic:
intro a2
State after:
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
x1 x2 : α
x1_mem : x1 = xs_hd ∨ x1 ∈ xs_tl
x2_mem : x2 = xs_hd ∨ x2 ∈ xs_tl
c1 : x1 = xs_hd
c2 : ¬x2 = xs_hd
a2 : ys_hd = f x2
⊢ x1 = x2

State before:
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
x1 x2 : α
x1_mem : x1 = xs_hd ∨ x1 ∈ xs_tl
x2_mem : x2 = xs_hd ∨ x2 ∈ xs_tl
c1 : x1 = xs_hd
c2 : ¬x2 = xs_hd
a2 : ys_hd = f x2
⊢ x1 = x2
Tactic:
cases x2_mem
State after:
case inl
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
x1 x2 : α
x1_mem : x1 = xs_hd ∨ x1 ∈ xs_tl
c1 : x1 = xs_hd
c2 : ¬x2 = xs_hd
a2 : ys_hd = f x2
h✝ : x2 = xs_hd
⊢ x1 = x2

case inr
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
x1 x2 : α
x1_mem : x1 = xs_hd ∨ x1 ∈ xs_tl
c1 : x1 = xs_hd
c2 : ¬x2 = xs_hd
a2 : ys_hd = f x2
h✝ : x2 ∈ xs_tl
⊢ x1 = x2

State before:
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
x1 x2 : α
x1_mem : x1 = xs_hd ∨ x1 ∈ xs_tl
c1 : x1 = xs_hd
c2 : ¬x2 = xs_hd
a2 : ys_hd = f x2
c3 : x2 = xs_hd
⊢ x1 = x2
Tactic:
case inl c3 =>
  contradiction
State after:
no goals

State before:
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
x1 x2 : α
x1_mem : x1 = xs_hd ∨ x1 ∈ xs_tl
c1 : x1 = xs_hd
c2 : ¬x2 = xs_hd
a2 : ys_hd = f x2
c3 : x2 ∈ xs_tl
⊢ x1 = x2
Tactic:
case inr c3 =>
  obtain s1 := List.mem_map_of_mem f c3
  simp only [a1_right] at s1
  simp only [← a2] at s1
  contradiction
State after:
no goals

State before:
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
x1 x2 : α
x1_mem : x1 = xs_hd ∨ x1 ∈ xs_tl
c1 : x1 = xs_hd
c2 : ¬x2 = xs_hd
a2 : ys_hd = f x2
c3 : x2 = xs_hd
⊢ x1 = x2
Tactic:
contradiction
State after:
no goals

State before:
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
x1 x2 : α
x1_mem : x1 = xs_hd ∨ x1 ∈ xs_tl
c1 : x1 = xs_hd
c2 : ¬x2 = xs_hd
a2 : ys_hd = f x2
c3 : x2 ∈ xs_tl
⊢ x1 = x2
Tactic:
obtain s1 := List.mem_map_of_mem f c3
State after:
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
x1 x2 : α
x1_mem : x1 = xs_hd ∨ x1 ∈ xs_tl
c1 : x1 = xs_hd
c2 : ¬x2 = xs_hd
a2 : ys_hd = f x2
c3 : x2 ∈ xs_tl
s1 : f x2 ∈ map f xs_tl
⊢ x1 = x2

State before:
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
x1 x2 : α
x1_mem : x1 = xs_hd ∨ x1 ∈ xs_tl
c1 : x1 = xs_hd
c2 : ¬x2 = xs_hd
a2 : ys_hd = f x2
c3 : x2 ∈ xs_tl
s1 : f x2 ∈ map f xs_tl
⊢ x1 = x2
Tactic:
simp only [a1_right] at s1
State after:
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
x1 x2 : α
x1_mem : x1 = xs_hd ∨ x1 ∈ xs_tl
c1 : x1 = xs_hd
c2 : ¬x2 = xs_hd
a2 : ys_hd = f x2
c3 : x2 ∈ xs_tl
s1 : f x2 ∈ ys_tl
⊢ x1 = x2

State before:
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
x1 x2 : α
x1_mem : x1 = xs_hd ∨ x1 ∈ xs_tl
c1 : x1 = xs_hd
c2 : ¬x2 = xs_hd
a2 : ys_hd = f x2
c3 : x2 ∈ xs_tl
s1 : f x2 ∈ ys_tl
⊢ x1 = x2
Tactic:
simp only [← a2] at s1
State after:
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
x1 x2 : α
x1_mem : x1 = xs_hd ∨ x1 ∈ xs_tl
c1 : x1 = xs_hd
c2 : ¬x2 = xs_hd
a2 : ys_hd = f x2
c3 : x2 ∈ xs_tl
s1 : ys_hd ∈ ys_tl
⊢ x1 = x2

State before:
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
x1 x2 : α
x1_mem : x1 = xs_hd ∨ x1 ∈ xs_tl
c1 : x1 = xs_hd
c2 : ¬x2 = xs_hd
a2 : ys_hd = f x2
c3 : x2 ∈ xs_tl
s1 : ys_hd ∈ ys_tl
⊢ x1 = x2
Tactic:
contradiction
State after:
no goals

State before:
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
x1 x2 : α
x1_mem : x1 = xs_hd ∨ x1 ∈ xs_tl
x2_mem : x2 = xs_hd ∨ x2 ∈ xs_tl
c1 : ¬x1 = xs_hd
c2 : x2 = xs_hd
⊢ f x1 = ys_hd → x1 = x2
Tactic:
intro a2
State after:
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
x1 x2 : α
x1_mem : x1 = xs_hd ∨ x1 ∈ xs_tl
x2_mem : x2 = xs_hd ∨ x2 ∈ xs_tl
c1 : ¬x1 = xs_hd
c2 : x2 = xs_hd
a2 : f x1 = ys_hd
⊢ x1 = x2

State before:
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
x1 x2 : α
x1_mem : x1 = xs_hd ∨ x1 ∈ xs_tl
x2_mem : x2 = xs_hd ∨ x2 ∈ xs_tl
c1 : ¬x1 = xs_hd
c2 : x2 = xs_hd
a2 : f x1 = ys_hd
⊢ x1 = x2
Tactic:
cases x1_mem
State after:
case inl
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
x1 x2 : α
x2_mem : x2 = xs_hd ∨ x2 ∈ xs_tl
c1 : ¬x1 = xs_hd
c2 : x2 = xs_hd
a2 : f x1 = ys_hd
h✝ : x1 = xs_hd
⊢ x1 = x2

case inr
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
x1 x2 : α
x2_mem : x2 = xs_hd ∨ x2 ∈ xs_tl
c1 : ¬x1 = xs_hd
c2 : x2 = xs_hd
a2 : f x1 = ys_hd
h✝ : x1 ∈ xs_tl
⊢ x1 = x2

State before:
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
x1 x2 : α
x2_mem : x2 = xs_hd ∨ x2 ∈ xs_tl
c1 : ¬x1 = xs_hd
c2 : x2 = xs_hd
a2 : f x1 = ys_hd
c3 : x1 = xs_hd
⊢ x1 = x2
Tactic:
case inl c3 =>
  contradiction
State after:
no goals

State before:
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
x1 x2 : α
x2_mem : x2 = xs_hd ∨ x2 ∈ xs_tl
c1 : ¬x1 = xs_hd
c2 : x2 = xs_hd
a2 : f x1 = ys_hd
c3 : x1 ∈ xs_tl
⊢ x1 = x2
Tactic:
case inr c3 =>
  obtain s1 := List.mem_map_of_mem f c3
  simp only [a1_right] at s1
  simp only [a2] at s1
  contradiction
State after:
no goals

State before:
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
x1 x2 : α
x2_mem : x2 = xs_hd ∨ x2 ∈ xs_tl
c1 : ¬x1 = xs_hd
c2 : x2 = xs_hd
a2 : f x1 = ys_hd
c3 : x1 = xs_hd
⊢ x1 = x2
Tactic:
contradiction
State after:
no goals

State before:
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
x1 x2 : α
x2_mem : x2 = xs_hd ∨ x2 ∈ xs_tl
c1 : ¬x1 = xs_hd
c2 : x2 = xs_hd
a2 : f x1 = ys_hd
c3 : x1 ∈ xs_tl
⊢ x1 = x2
Tactic:
obtain s1 := List.mem_map_of_mem f c3
State after:
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
x1 x2 : α
x2_mem : x2 = xs_hd ∨ x2 ∈ xs_tl
c1 : ¬x1 = xs_hd
c2 : x2 = xs_hd
a2 : f x1 = ys_hd
c3 : x1 ∈ xs_tl
s1 : f x1 ∈ map f xs_tl
⊢ x1 = x2

State before:
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
x1 x2 : α
x2_mem : x2 = xs_hd ∨ x2 ∈ xs_tl
c1 : ¬x1 = xs_hd
c2 : x2 = xs_hd
a2 : f x1 = ys_hd
c3 : x1 ∈ xs_tl
s1 : f x1 ∈ map f xs_tl
⊢ x1 = x2
Tactic:
simp only [a1_right] at s1
State after:
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
x1 x2 : α
x2_mem : x2 = xs_hd ∨ x2 ∈ xs_tl
c1 : ¬x1 = xs_hd
c2 : x2 = xs_hd
a2 : f x1 = ys_hd
c3 : x1 ∈ xs_tl
s1 : f x1 ∈ ys_tl
⊢ x1 = x2

State before:
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
x1 x2 : α
x2_mem : x2 = xs_hd ∨ x2 ∈ xs_tl
c1 : ¬x1 = xs_hd
c2 : x2 = xs_hd
a2 : f x1 = ys_hd
c3 : x1 ∈ xs_tl
s1 : f x1 ∈ ys_tl
⊢ x1 = x2
Tactic:
simp only [a2] at s1
State after:
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
x1 x2 : α
x2_mem : x2 = xs_hd ∨ x2 ∈ xs_tl
c1 : ¬x1 = xs_hd
c2 : x2 = xs_hd
a2 : f x1 = ys_hd
c3 : x1 ∈ xs_tl
s1 : ys_hd ∈ ys_tl
⊢ x1 = x2

State before:
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
x1 x2 : α
x2_mem : x2 = xs_hd ∨ x2 ∈ xs_tl
c1 : ¬x1 = xs_hd
c2 : x2 = xs_hd
a2 : f x1 = ys_hd
c3 : x1 ∈ xs_tl
s1 : ys_hd ∈ ys_tl
⊢ x1 = x2
Tactic:
contradiction
State after:
no goals

State before:
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
x1 x2 : α
x1_mem : x1 = xs_hd ∨ x1 ∈ xs_tl
x2_mem : x2 = xs_hd ∨ x2 ∈ xs_tl
c1 : ¬x1 = xs_hd
c2 : ¬x2 = xs_hd
⊢ f x1 = f x2 → x1 = x2
Tactic:
intro a2
State after:
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
x1 x2 : α
x1_mem : x1 = xs_hd ∨ x1 ∈ xs_tl
x2_mem : x2 = xs_hd ∨ x2 ∈ xs_tl
c1 : ¬x1 = xs_hd
c2 : ¬x2 = xs_hd
a2 : f x1 = f x2
⊢ x1 = x2

State before:
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
x1 x2 : α
x1_mem : x1 = xs_hd ∨ x1 ∈ xs_tl
x2_mem : x2 = xs_hd ∨ x2 ∈ xs_tl
c1 : ¬x1 = xs_hd
c2 : ¬x2 = xs_hd
a2 : f x1 = f x2
⊢ x1 = x2
Tactic:
cases x1_mem
State after:
case inl
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
x1 x2 : α
x2_mem : x2 = xs_hd ∨ x2 ∈ xs_tl
c1 : ¬x1 = xs_hd
c2 : ¬x2 = xs_hd
a2 : f x1 = f x2
h✝ : x1 = xs_hd
⊢ x1 = x2

case inr
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
x1 x2 : α
x2_mem : x2 = xs_hd ∨ x2 ∈ xs_tl
c1 : ¬x1 = xs_hd
c2 : ¬x2 = xs_hd
a2 : f x1 = f x2
h✝ : x1 ∈ xs_tl
⊢ x1 = x2

State before:
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
x1 x2 : α
x2_mem : x2 = xs_hd ∨ x2 ∈ xs_tl
c1 : ¬x1 = xs_hd
c2 : ¬x2 = xs_hd
a2 : f x1 = f x2
x1_mem_left : x1 = xs_hd
⊢ x1 = x2
Tactic:
case inl x1_mem_left =>
  contradiction
State after:
no goals

State before:
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
x1 x2 : α
x2_mem : x2 = xs_hd ∨ x2 ∈ xs_tl
c1 : ¬x1 = xs_hd
c2 : ¬x2 = xs_hd
a2 : f x1 = f x2
x1_mem_right : x1 ∈ xs_tl
⊢ x1 = x2
Tactic:
case inr x1_mem_right =>
  cases x2_mem
  case inl x2_mem_left =>
    contradiction
  case inr x2_mem_right =>
    simp only [List.InjOn] at a1_left
    apply a1_left x1_mem_right x2_mem_right a2
State after:
no goals

State before:
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
x1 x2 : α
x2_mem : x2 = xs_hd ∨ x2 ∈ xs_tl
c1 : ¬x1 = xs_hd
c2 : ¬x2 = xs_hd
a2 : f x1 = f x2
x1_mem_left : x1 = xs_hd
⊢ x1 = x2
Tactic:
contradiction
State after:
no goals

State before:
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
x1 x2 : α
x2_mem : x2 = xs_hd ∨ x2 ∈ xs_tl
c1 : ¬x1 = xs_hd
c2 : ¬x2 = xs_hd
a2 : f x1 = f x2
x1_mem_right : x1 ∈ xs_tl
⊢ x1 = x2
Tactic:
cases x2_mem
State after:
case inl
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
x1 x2 : α
c1 : ¬x1 = xs_hd
c2 : ¬x2 = xs_hd
a2 : f x1 = f x2
x1_mem_right : x1 ∈ xs_tl
h✝ : x2 = xs_hd
⊢ x1 = x2

case inr
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
x1 x2 : α
c1 : ¬x1 = xs_hd
c2 : ¬x2 = xs_hd
a2 : f x1 = f x2
x1_mem_right : x1 ∈ xs_tl
h✝ : x2 ∈ xs_tl
⊢ x1 = x2

State before:
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
x1 x2 : α
c1 : ¬x1 = xs_hd
c2 : ¬x2 = xs_hd
a2 : f x1 = f x2
x1_mem_right : x1 ∈ xs_tl
x2_mem_left : x2 = xs_hd
⊢ x1 = x2
Tactic:
case inl x2_mem_left =>
  contradiction
State after:
no goals

State before:
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
x1 x2 : α
c1 : ¬x1 = xs_hd
c2 : ¬x2 = xs_hd
a2 : f x1 = f x2
x1_mem_right : x1 ∈ xs_tl
x2_mem_right : x2 ∈ xs_tl
⊢ x1 = x2
Tactic:
case inr x2_mem_right =>
  simp only [List.InjOn] at a1_left
  apply a1_left x1_mem_right x2_mem_right a2
State after:
no goals

State before:
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
x1 x2 : α
c1 : ¬x1 = xs_hd
c2 : ¬x2 = xs_hd
a2 : f x1 = f x2
x1_mem_right : x1 ∈ xs_tl
x2_mem_left : x2 = xs_hd
⊢ x1 = x2
Tactic:
contradiction
State after:
no goals

State before:
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
x1 x2 : α
c1 : ¬x1 = xs_hd
c2 : ¬x2 = xs_hd
a2 : f x1 = f x2
x1_mem_right : x1 ∈ xs_tl
x2_mem_right : x2 ∈ xs_tl
⊢ x1 = x2
Tactic:
simp only [List.InjOn] at a1_left
State after:
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : ∀ ⦃x₁ : α⦄, x₁ ∈ xs_tl → ∀ ⦃x₂ : α⦄, x₂ ∈ xs_tl → f x₁ = f x₂ → x₁ = x₂
a1_right : map f xs_tl = ys_tl
x1 x2 : α
c1 : ¬x1 = xs_hd
c2 : ¬x2 = xs_hd
a2 : f x1 = f x2
x1_mem_right : x1 ∈ xs_tl
x2_mem_right : x2 ∈ xs_tl
⊢ x1 = x2

State before:
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : ∀ ⦃x₁ : α⦄, x₁ ∈ xs_tl → ∀ ⦃x₂ : α⦄, x₂ ∈ xs_tl → f x₁ = f x₂ → x₁ = x₂
a1_right : map f xs_tl = ys_tl
x1 x2 : α
c1 : ¬x1 = xs_hd
c2 : ¬x2 = xs_hd
a2 : f x1 = f x2
x1_mem_right : x1 ∈ xs_tl
x2_mem_right : x2 ∈ xs_tl
⊢ x1 = x2
Tactic:
apply a1_left x1_mem_right x2_mem_right a2
State after:
no goals

State before:
case right
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
⊢ Function.updateITE f xs_hd ys_hd xs_hd = ys_hd ∧ map (Function.updateITE f xs_hd ys_hd) xs_tl = ys_tl
Tactic:
constructor
State after:
case right.left
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
⊢ Function.updateITE f xs_hd ys_hd xs_hd = ys_hd

case right.right
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
⊢ map (Function.updateITE f xs_hd ys_hd) xs_tl = ys_tl

State before:
case right.left
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
⊢ Function.updateITE f xs_hd ys_hd xs_hd = ys_hd
Tactic:
simp only [Function.updateITE]
State after:
case right.left
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
⊢ (if True then ys_hd else f xs_hd) = ys_hd

State before:
case right.left
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
⊢ (if True then ys_hd else f xs_hd) = ys_hd
Tactic:
simp
State after:
no goals

State before:
case right.right
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
⊢ map (Function.updateITE f xs_hd ys_hd) xs_tl = ys_tl
Tactic:
simp only [← a1_right]
State after:
case right.right
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
⊢ map (Function.updateITE f xs_hd ys_hd) xs_tl = map f xs_tl

State before:
case right.right
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
⊢ map (Function.updateITE f xs_hd ys_hd) xs_tl = map f xs_tl
Tactic:
apply Function.updateITE_not_mem_list
State after:
case right.right.h1
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
⊢ xs_hd ∉ xs_tl

State before:
case right.right.h1
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
⊢ xs_hd ∉ xs_tl
Tactic:
exact h2_left
State after:
no goals