internlm/Lean-Github huggingface dataset:
Theorem: List.nodup_eq_len_imp_exists_bijon
Proof 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
Proof 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
Theorem: List.nodup_eq_len_imp_exists_bijon
Proof 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]
Proof 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
Theorem: List.nodup_eq_len_imp_exists_bijon
Proof 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
Proof 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
Theorem: List.nodup_eq_len_imp_exists_bijon
Proof 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]
Proof state after:
no goals
Theorem: List.nodup_eq_len_imp_exists_bijon
Proof 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
Proof state after:
no goals
Theorem: List.nodup_eq_len_imp_exists_bijon
Proof 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
Proof state after:
no goals
Theorem: List.nodup_eq_len_imp_exists_bijon
Proof 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
Proof state after:
no goals
Theorem: List.nodup_eq_len_imp_exists_bijon
Proof 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 _
Proof 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
Theorem: List.nodup_eq_len_imp_exists_bijon
Proof 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]
Proof 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
Theorem: List.nodup_eq_len_imp_exists_bijon
Proof 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]
Proof state after:
no goals
Theorem: List.nodup_eq_len_imp_exists_bijon
Proof 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
Proof 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
Theorem: List.nodup_eq_len_imp_exists_bijon
Proof 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
Proof 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
Theorem: List.nodup_eq_len_imp_exists_bijon
Proof 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
Proof state after:
no goals
Theorem: List.nodup_eq_len_imp_exists_bijon
Proof 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
Proof state after:
no goals
Theorem: List.nodup_eq_len_imp_exists_bijon
Proof 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
Proof state after:
no goals
Theorem: List.nodup_eq_len_imp_exists_bijon
Proof 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
Proof 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
Theorem: List.nodup_eq_len_imp_exists_bijon
Proof 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
Proof 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
Theorem: List.nodup_eq_len_imp_exists_bijon
Proof 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
Proof 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
Theorem: List.nodup_eq_len_imp_exists_bijon
Proof 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
Proof state after:
no goals
Theorem: List.nodup_eq_len_imp_exists_bijon
Proof 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
Proof 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
Theorem: List.nodup_eq_len_imp_exists_bijon
Proof 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
Proof 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
Theorem: List.nodup_eq_len_imp_exists_bijon
Proof 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
Proof state after:
no goals
Theorem: List.nodup_eq_len_imp_exists_bijon
Proof 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
Proof state after:
no goals
Theorem: List.nodup_eq_len_imp_exists_bijon
Proof 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
Proof state after:
no goals
Theorem: List.nodup_eq_len_imp_exists_bijon
Proof 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
Proof 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
Theorem: List.nodup_eq_len_imp_exists_bijon
Proof 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
Proof 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
Theorem: List.nodup_eq_len_imp_exists_bijon
Proof 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
Proof 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
Theorem: List.nodup_eq_len_imp_exists_bijon
Proof 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
Proof state after:
no goals