internlm/Lean-Github huggingface dataset:
Theorem: List.Nodup.erase
Proof state before:
case cons
α : Type u
β : Type v
inst✝ : DecidableEq α
a b : α
l : List α
IH : Nodup l → Nodup (List.erase l a)
hnodup : Nodup (b :: l)
hhead : ∀ (a' : α), a' ∈ l → b ≠ a'
htail : Nodup l
⊢ Nodup
    (match b == a with
    | true => l
    | false => b :: List.erase l a)
Tactic:
match b == a with
| true => dsimp; exact htail
| false =>
  dsimp; refine pairwise_cons.mpr <| And.intro ?_ ?_
  . intro _ hb h; cases h
    exact hhead b (List.mem_of_mem_erase hb) rfl
  . exact IH htail
Proof state after:
no goals
Theorem: List.Nodup.erase
Proof state before:
α : Type u
β : Type v
inst✝ : DecidableEq α
a b : α
l : List α
IH : Nodup l → Nodup (List.erase l a)
hnodup : Nodup (b :: l)
hhead : ∀ (a' : α), a' ∈ l → b ≠ a'
htail : Nodup l
⊢ Nodup
    (match true with
    | true => l
    | false => b :: List.erase l a)
Tactic:
dsimp
Proof state after:
α : Type u
β : Type v
inst✝ : DecidableEq α
a b : α
l : List α
IH : Nodup l → Nodup (List.erase l a)
hnodup : Nodup (b :: l)
hhead : ∀ (a' : α), a' ∈ l → b ≠ a'
htail : Nodup l
⊢ Nodup l
Theorem: List.Nodup.erase
Proof state before:
α : Type u
β : Type v
inst✝ : DecidableEq α
a b : α
l : List α
IH : Nodup l → Nodup (List.erase l a)
hnodup : Nodup (b :: l)
hhead : ∀ (a' : α), a' ∈ l → b ≠ a'
htail : Nodup l
⊢ Nodup l
Tactic:
exact htail
Proof state after:
no goals
Theorem: List.Nodup.erase
Proof state before:
α : Type u
β : Type v
inst✝ : DecidableEq α
a b : α
l : List α
IH : Nodup l → Nodup (List.erase l a)
hnodup : Nodup (b :: l)
hhead : ∀ (a' : α), a' ∈ l → b ≠ a'
htail : Nodup l
⊢ Nodup
    (match false with
    | true => l
    | false => b :: List.erase l a)
Tactic:
dsimp
Proof state after:
α : Type u
β : Type v
inst✝ : DecidableEq α
a b : α
l : List α
IH : Nodup l → Nodup (List.erase l a)
hnodup : Nodup (b :: l)
hhead : ∀ (a' : α), a' ∈ l → b ≠ a'
htail : Nodup l
⊢ Nodup (b :: List.erase l a)
Theorem: List.Nodup.erase
Proof state before:
α : Type u
β : Type v
inst✝ : DecidableEq α
a b : α
l : List α
IH : Nodup l → Nodup (List.erase l a)
hnodup : Nodup (b :: l)
hhead : ∀ (a' : α), a' ∈ l → b ≠ a'
htail : Nodup l
⊢ Nodup (b :: List.erase l a)
Tactic:
refine pairwise_cons.mpr <| And.intro ?_ ?_
Proof state after:
case refine_1
α : Type u
β : Type v
inst✝ : DecidableEq α
a b : α
l : List α
IH : Nodup l → Nodup (List.erase l a)
hnodup : Nodup (b :: l)
hhead : ∀ (a' : α), a' ∈ l → b ≠ a'
htail : Nodup l
⊢ ∀ (a' : α), a' ∈ List.erase l a → b ≠ a'

case refine_2
α : Type u
β : Type v
inst✝ : DecidableEq α
a b : α
l : List α
IH : Nodup l → Nodup (List.erase l a)
hnodup : Nodup (b :: l)
hhead : ∀ (a' : α), a' ∈ l → b ≠ a'
htail : Nodup l
⊢ Pairwise (fun x x_1 => x ≠ x_1) (List.erase l a)
Theorem: List.Nodup.erase
Proof state before:
case refine_1
α : Type u
β : Type v
inst✝ : DecidableEq α
a b : α
l : List α
IH : Nodup l → Nodup (List.erase l a)
hnodup : Nodup (b :: l)
hhead : ∀ (a' : α), a' ∈ l → b ≠ a'
htail : Nodup l
⊢ ∀ (a' : α), a' ∈ List.erase l a → b ≠ a'

case refine_2
α : Type u
β : Type v
inst✝ : DecidableEq α
a b : α
l : List α
IH : Nodup l → Nodup (List.erase l a)
hnodup : Nodup (b :: l)
hhead : ∀ (a' : α), a' ∈ l → b ≠ a'
htail : Nodup l
⊢ Pairwise (fun x x_1 => x ≠ x_1) (List.erase l a)
Tactic:
. intro _ hb h; cases h
  exact hhead b (List.mem_of_mem_erase hb) rfl
Proof state after:
case refine_2
α : Type u
β : Type v
inst✝ : DecidableEq α
a b : α
l : List α
IH : Nodup l → Nodup (List.erase l a)
hnodup : Nodup (b :: l)
hhead : ∀ (a' : α), a' ∈ l → b ≠ a'
htail : Nodup l
⊢ Pairwise (fun x x_1 => x ≠ x_1) (List.erase l a)
Theorem: List.Nodup.erase
Proof state before:
case refine_2
α : Type u
β : Type v
inst✝ : DecidableEq α
a b : α
l : List α
IH : Nodup l → Nodup (List.erase l a)
hnodup : Nodup (b :: l)
hhead : ∀ (a' : α), a' ∈ l → b ≠ a'
htail : Nodup l
⊢ Pairwise (fun x x_1 => x ≠ x_1) (List.erase l a)
Tactic:
. exact IH htail
Proof state after:
no goals
Theorem: List.Nodup.erase
Proof state before:
case refine_1
α : Type u
β : Type v
inst✝ : DecidableEq α
a b : α
l : List α
IH : Nodup l → Nodup (List.erase l a)
hnodup : Nodup (b :: l)
hhead : ∀ (a' : α), a' ∈ l → b ≠ a'
htail : Nodup l
⊢ ∀ (a' : α), a' ∈ List.erase l a → b ≠ a'
Tactic:
intro _ hb h
Proof state after:
case refine_1
α : Type u
β : Type v
inst✝ : DecidableEq α
a b : α
l : List α
IH : Nodup l → Nodup (List.erase l a)
hnodup : Nodup (b :: l)
hhead : ∀ (a' : α), a' ∈ l → b ≠ a'
htail : Nodup l
a'✝ : α
hb : a'✝ ∈ List.erase l a
h : b = a'✝
⊢ False
Theorem: List.Nodup.erase
Proof state before:
case refine_1
α : Type u
β : Type v
inst✝ : DecidableEq α
a b : α
l : List α
IH : Nodup l → Nodup (List.erase l a)
hnodup : Nodup (b :: l)
hhead : ∀ (a' : α), a' ∈ l → b ≠ a'
htail : Nodup l
a'✝ : α
hb : a'✝ ∈ List.erase l a
h : b = a'✝
⊢ False
Tactic:
cases h
Proof state after:
case refine_1.refl
α : Type u
β : Type v
inst✝ : DecidableEq α
a b : α
l : List α
IH : Nodup l → Nodup (List.erase l a)
hnodup : Nodup (b :: l)
hhead : ∀ (a' : α), a' ∈ l → b ≠ a'
htail : Nodup l
hb : b ∈ List.erase l a
⊢ False
Theorem: List.Nodup.erase
Proof state before:
case refine_1.refl
α : Type u
β : Type v
inst✝ : DecidableEq α
a b : α
l : List α
IH : Nodup l → Nodup (List.erase l a)
hnodup : Nodup (b :: l)
hhead : ∀ (a' : α), a' ∈ l → b ≠ a'
htail : Nodup l
hb : b ∈ List.erase l a
⊢ False
Tactic:
exact hhead b (List.mem_of_mem_erase hb) rfl
Proof state after:
no goals
Theorem: List.Nodup.erase
Proof state before:
case refine_2
α : Type u
β : Type v
inst✝ : DecidableEq α
a b : α
l : List α
IH : Nodup l → Nodup (List.erase l a)
hnodup : Nodup (b :: l)
hhead : ∀ (a' : α), a' ∈ l → b ≠ a'
htail : Nodup l
⊢ Pairwise (fun x x_1 => x ≠ x_1) (List.erase l a)
Tactic:
exact IH htail
Proof state after:
no goals
Theorem: List.nodup_cons_of_notmem_nodup
Proof state before:
α : Type u
β : Type v
a : α
l : List α
ha : ¬a ∈ l
hnodup : Nodup l
⊢ Nodup (a :: l)
Tactic:
refine .cons ?_ hnodup
Proof state after:
α : Type u
β : Type v
a : α
l : List α
ha : ¬a ∈ l
hnodup : Nodup l
⊢ ∀ (a' : α), a' ∈ l → a ≠ a'
Theorem: List.nodup_cons_of_notmem_nodup
Proof state before:
α : Type u
β : Type v
a : α
l : List α
ha : ¬a ∈ l
hnodup : Nodup l
⊢ ∀ (a' : α), a' ∈ l → a ≠ a'
Tactic:
intros _ hal h
Proof state after:
α : Type u
β : Type v
a : α
l : List α
ha : ¬a ∈ l
hnodup : Nodup l
a'✝ : α
hal : a'✝ ∈ l
h : a = a'✝
⊢ False
Theorem: List.nodup_cons_of_notmem_nodup
Proof state before:
α : Type u
β : Type v
a : α
l : List α
ha : ¬a ∈ l
hnodup : Nodup l
a'✝ : α
hal : a'✝ ∈ l
h : a = a'✝
⊢ False
Tactic:
cases h
Proof state after:
case refl
α : Type u
β : Type v
a : α
l : List α
ha : ¬a ∈ l
hnodup : Nodup l
hal : a ∈ l
⊢ False
Theorem: List.nodup_cons_of_notmem_nodup
Proof state before:
case refl
α : Type u
β : Type v
a : α
l : List α
ha : ¬a ∈ l
hnodup : Nodup l
hal : a ∈ l
⊢ False
Tactic:
exact ha hal
Proof state after:
no goals
Theorem: List.nodup_range'
Proof state before:
α : Type u
β : Type v
start len step : Nat
hstep : step > 0
⊢ Nodup (range' start len step)
Tactic:
induction len generalizing start with
| zero => exact .nil
| succ len IH =>
  refine Pairwise.cons ?_ (IH _)
  intro n hn; let ⟨k,hk⟩ := mem_range'.mp hn
  suffices start < n from Nat.ne_of_lt this
  calc start
    _ < start + step := Nat.lt_add_of_pos_right hstep
    _ ≤ start + step + step * k := Nat.le_add_right ..
    _ = n := hk.2.symm
Proof state after:
no goals
Theorem: List.nodup_range'
Proof state before:
case zero
α : Type u
β : Type v
step : Nat
hstep : step > 0
start : Nat
⊢ Nodup (range' start Nat.zero step)
Tactic:
exact .nil
Proof state after:
no goals
Theorem: List.nodup_range'
Proof state before:
case succ
α : Type u
β : Type v
step : Nat
hstep : step > 0
len : Nat
IH : ∀ (start : Nat), Nodup (range' start len step)
start : Nat
⊢ Nodup (range' start (Nat.succ len) step)
Tactic:
refine Pairwise.cons ?_ (IH _)
Proof state after:
case succ
α : Type u
β : Type v
step : Nat
hstep : step > 0
len : Nat
IH : ∀ (start : Nat), Nodup (range' start len step)
start : Nat
⊢ ∀ (a' : Nat), a' ∈ range' (start + step) len step → start ≠ a'
Theorem: List.nodup_range'
Proof state before:
case succ
α : Type u
β : Type v
step : Nat
hstep : step > 0
len : Nat
IH : ∀ (start : Nat), Nodup (range' start len step)
start : Nat
⊢ ∀ (a' : Nat), a' ∈ range' (start + step) len step → start ≠ a'
Tactic:
intro n hn
Proof state after:
case succ
α : Type u
β : Type v
step : Nat
hstep : step > 0
len : Nat
IH : ∀ (start : Nat), Nodup (range' start len step)
start n : Nat
hn : n ∈ range' (start + step) len step
⊢ start ≠ n
Theorem: List.nodup_range'
Proof state before:
case succ
α : Type u
β : Type v
step : Nat
hstep : step > 0
len : Nat
IH : ∀ (start : Nat), Nodup (range' start len step)
start n : Nat
hn : n ∈ range' (start + step) len step
⊢ start ≠ n
Tactic:
let ⟨k,hk⟩ := mem_range'.mp hn
Proof state after:
case succ
α : Type u
β : Type v
step : Nat
hstep : step > 0
len : Nat
IH : ∀ (start : Nat), Nodup (range' start len step)
start n : Nat
hn : n ∈ range' (start + step) len step
k : Nat
hk : k < len ∧ n = start + step + step * k
⊢ start ≠ n
Theorem: List.nodup_range'
Proof state before:
case succ
α : Type u
β : Type v
step : Nat
hstep : step > 0
len : Nat
IH : ∀ (start : Nat), Nodup (range' start len step)
start n : Nat
hn : n ∈ range' (start + step) len step
k : Nat
hk : k < len ∧ n = start + step + step * k
⊢ start ≠ n
Tactic:
suffices start < n from Nat.ne_of_lt this
Proof state after:
case succ
α : Type u
β : Type v
step : Nat
hstep : step > 0
len : Nat
IH : ∀ (start : Nat), Nodup (range' start len step)
start n : Nat
hn : n ∈ range' (start + step) len step
k : Nat
hk : k < len ∧ n = start + step + step * k
⊢ start < n
Theorem: List.nodup_range'
Proof state before:
case succ
α : Type u
β : Type v
step : Nat
hstep : step > 0
len : Nat
IH : ∀ (start : Nat), Nodup (range' start len step)
start n : Nat
hn : n ∈ range' (start + step) len step
k : Nat
hk : k < len ∧ n = start + step + step * k
⊢ start < n
Tactic:
calc start
  _ < start + step := Nat.lt_add_of_pos_right hstep
  _ ≤ start + step + step * k := Nat.le_add_right ..
  _ = n := hk.2.symm
Proof state after:
no goals
Theorem: List.nodup_range
Proof state before:
α : Type u
β : Type v
n : Nat
⊢ Nodup (range n)
Tactic:
rewrite [range_eq_range']
Proof state after:
α : Type u
β : Type v
n : Nat
⊢ Nodup (range' 0 n)
Theorem: List.nodup_range
Proof state before:
α : Type u
β : Type v
n : Nat
⊢ Nodup (range' 0 n)
Tactic:
apply nodup_range'
Proof state after:
case hstep
α : Type u
β : Type v
n : Nat
⊢ 1 > 0
Theorem: List.nodup_range
Proof state before:
case hstep
α : Type u
β : Type v
n : Nat
⊢ 1 > 0
Tactic:
decide
Proof state after:
no goals
Theorem: List.nodup_of_nodup_map
Proof state before:
α : Type u
β : Type v
f : α → β
l : List α
h : Nodup (map f l)
⊢ Nodup l
Tactic:
induction l with
| nil => exact .nil
| cons a l IH =>
  dsimp at h
  apply nodup_cons_of_notmem_nodup
  . intro ha; exact h.head <| List.mem_map_of_mem f ha
  . exact IH h.tail
Proof state after:
no goals
Theorem: List.nodup_of_nodup_map
Proof state before:
case nil
α : Type u
β : Type v
f : α → β
h : Nodup (map f [])
⊢ Nodup []
Tactic:
exact .nil
Proof state after:
no goals
Theorem: List.nodup_of_nodup_map
Proof state before:
case cons
α : Type u
β : Type v
f : α → β
a : α
l : List α
IH : Nodup (map f l) → Nodup l
h : Nodup (map f (a :: l))
⊢ Nodup (a :: l)
Tactic:
dsimp at h
Proof state after:
case cons
α : Type u
β : Type v
f : α → β
a : α
l : List α
IH : Nodup (map f l) → Nodup l
h : Nodup (f a :: map f l)
⊢ Nodup (a :: l)
Theorem: List.nodup_of_nodup_map
Proof state before:
case cons
α : Type u
β : Type v
f : α → β
a : α
l : List α
IH : Nodup (map f l) → Nodup l
h : Nodup (f a :: map f l)
⊢ Nodup (a :: l)
Tactic:
apply nodup_cons_of_notmem_nodup
Proof state after:
case cons.ha
α : Type u
β : Type v
f : α → β
a : α
l : List α
IH : Nodup (map f l) → Nodup l
h : Nodup (f a :: map f l)
⊢ ¬a ∈ l

case cons.hnodup
α : Type u
β : Type v
f : α → β
a : α
l : List α
IH : Nodup (map f l) → Nodup l
h : Nodup (f a :: map f l)
⊢ Nodup l
Theorem: List.nodup_of_nodup_map
Proof state before:
case cons.ha
α : Type u
β : Type v
f : α → β
a : α
l : List α
IH : Nodup (map f l) → Nodup l
h : Nodup (f a :: map f l)
⊢ ¬a ∈ l

case cons.hnodup
α : Type u
β : Type v
f : α → β
a : α
l : List α
IH : Nodup (map f l) → Nodup l
h : Nodup (f a :: map f l)
⊢ Nodup l
Tactic:
. intro ha; exact h.head <| List.mem_map_of_mem f ha
Proof state after:
case cons.hnodup
α : Type u
β : Type v
f : α → β
a : α
l : List α
IH : Nodup (map f l) → Nodup l
h : Nodup (f a :: map f l)
⊢ Nodup l
Theorem: List.nodup_of_nodup_map
Proof state before:
case cons.hnodup
α : Type u
β : Type v
f : α → β
a : α
l : List α
IH : Nodup (map f l) → Nodup l
h : Nodup (f a :: map f l)
⊢ Nodup l
Tactic:
. exact IH h.tail
Proof state after:
no goals
Theorem: List.nodup_of_nodup_map
Proof state before:
case cons.ha
α : Type u
β : Type v
f : α → β
a : α
l : List α
IH : Nodup (map f l) → Nodup l
h : Nodup (f a :: map f l)
⊢ ¬a ∈ l
Tactic:
intro ha
Proof state after:
case cons.ha
α : Type u
β : Type v
f : α → β
a : α
l : List α
IH : Nodup (map f l) → Nodup l
h : Nodup (f a :: map f l)
ha : a ∈ l
⊢ False
Theorem: List.nodup_of_nodup_map
Proof state before:
case cons.ha
α : Type u
β : Type v
f : α → β
a : α
l : List α
IH : Nodup (map f l) → Nodup l
h : Nodup (f a :: map f l)
ha : a ∈ l
⊢ False
Tactic:
exact h.head <| List.mem_map_of_mem f ha
Proof state after:
no goals
Theorem: List.nodup_of_nodup_map
Proof state before:
case cons.hnodup
α : Type u
β : Type v
f : α → β
a : α
l : List α
IH : Nodup (map f l) → Nodup l
h : Nodup (f a :: map f l)
⊢ Nodup l
Tactic:
exact IH h.tail
Proof state after:
no goals
Theorem: List.nodup_of_get_inj
Proof state before:
α : Type u
β : Type v
l : List α
h : ∀ (i j : Nat) (x : i < length l) (x_1 : j < length l), l[i] = l[j] → i = j
⊢ Nodup l
Tactic:
induction l with
| nil => exact .nil
| cons a l IH =>
  refine .cons ?_ (IH fun i j hi hj hl => ?_)
  . intro _ hmem heq; cases heq
    have ⟨⟨i,hi⟩,hl⟩ := List.mem_iff_get.mp hmem
    have : i+1 = 0 :=
      h (i+1) 0 (Nat.succ_lt_succ hi) l.length.zero_lt_succ hl
    cases this
  . apply Nat.succ.inj
    exact h (i+1) (j+1) (Nat.succ_lt_succ hi) (Nat.succ_lt_succ hj) hl
Proof state after:
no goals
Theorem: List.nodup_of_get_inj
Proof state before:
case nil
α : Type u
β : Type v
h : ∀ (i j : Nat) (x : i < length []) (x_1 : j < length []), [][i] = [][j] → i = j
⊢ Nodup []
Tactic:
exact .nil
Proof state after:
no goals
Theorem: List.nodup_of_get_inj
Proof state before:
case cons
α : Type u
β : Type v
a : α
l : List α
IH : (∀ (i j : Nat) (x : i < length l) (x_1 : j < length l), l[i] = l[j] → i = j) → Nodup l
h : ∀ (i j : Nat) (x : i < length (a :: l)) (x_1 : j < length (a :: l)), (a :: l)[i] = (a :: l)[j] → i = j
⊢ Nodup (a :: l)
Tactic:
refine .cons ?_ (IH fun i j hi hj hl => ?_)
Proof state after:
case cons.refine_1
α : Type u
β : Type v
a : α
l : List α
IH : (∀ (i j : Nat) (x : i < length l) (x_1 : j < length l), l[i] = l[j] → i = j) → Nodup l
h : ∀ (i j : Nat) (x : i < length (a :: l)) (x_1 : j < length (a :: l)), (a :: l)[i] = (a :: l)[j] → i = j
⊢ ∀ (a' : α), a' ∈ l → a ≠ a'

case cons.refine_2
α : Type u
β : Type v
a : α
l : List α
IH : (∀ (i j : Nat) (x : i < length l) (x_1 : j < length l), l[i] = l[j] → i = j) → Nodup l
h : ∀ (i j : Nat) (x : i < length (a :: l)) (x_1 : j < length (a :: l)), (a :: l)[i] = (a :: l)[j] → i = j
i j : Nat
hi : i < length l
hj : j < length l
hl : l[i] = l[j]
⊢ i = j
Theorem: List.nodup_of_get_inj
Proof state before:
case cons.refine_1
α : Type u
β : Type v
a : α
l : List α
IH : (∀ (i j : Nat) (x : i < length l) (x_1 : j < length l), l[i] = l[j] → i = j) → Nodup l
h : ∀ (i j : Nat) (x : i < length (a :: l)) (x_1 : j < length (a :: l)), (a :: l)[i] = (a :: l)[j] → i = j
⊢ ∀ (a' : α), a' ∈ l → a ≠ a'

case cons.refine_2
α : Type u
β : Type v
a : α
l : List α
IH : (∀ (i j : Nat) (x : i < length l) (x_1 : j < length l), l[i] = l[j] → i = j) → Nodup l
h : ∀ (i j : Nat) (x : i < length (a :: l)) (x_1 : j < length (a :: l)), (a :: l)[i] = (a :: l)[j] → i = j
i j : Nat
hi : i < length l
hj : j < length l
hl : l[i] = l[j]
⊢ i = j
Tactic:
. intro _ hmem heq; cases heq
  have ⟨⟨i,hi⟩,hl⟩ := List.mem_iff_get.mp hmem
  have : i+1 = 0 :=
    h (i+1) 0 (Nat.succ_lt_succ hi) l.length.zero_lt_succ hl
  cases this
Proof state after:
case cons.refine_2
α : Type u
β : Type v
a : α
l : List α
IH : (∀ (i j : Nat) (x : i < length l) (x_1 : j < length l), l[i] = l[j] → i = j) → Nodup l
h : ∀ (i j : Nat) (x : i < length (a :: l)) (x_1 : j < length (a :: l)), (a :: l)[i] = (a :: l)[j] → i = j
i j : Nat
hi : i < length l
hj : j < length l
hl : l[i] = l[j]
⊢ i = j
Theorem: List.nodup_of_get_inj
Proof state before:
case cons.refine_2
α : Type u
β : Type v
a : α
l : List α
IH : (∀ (i j : Nat) (x : i < length l) (x_1 : j < length l), l[i] = l[j] → i = j) → Nodup l
h : ∀ (i j : Nat) (x : i < length (a :: l)) (x_1 : j < length (a :: l)), (a :: l)[i] = (a :: l)[j] → i = j
i j : Nat
hi : i < length l
hj : j < length l
hl : l[i] = l[j]
⊢ i = j
Tactic:
. apply Nat.succ.inj
  exact h (i+1) (j+1) (Nat.succ_lt_succ hi) (Nat.succ_lt_succ hj) hl
Proof state after:
no goals
Theorem: List.nodup_of_get_inj
Proof state before:
case cons.refine_1
α : Type u
β : Type v
a : α
l : List α
IH : (∀ (i j : Nat) (x : i < length l) (x_1 : j < length l), l[i] = l[j] → i = j) → Nodup l
h : ∀ (i j : Nat) (x : i < length (a :: l)) (x_1 : j < length (a :: l)), (a :: l)[i] = (a :: l)[j] → i = j
⊢ ∀ (a' : α), a' ∈ l → a ≠ a'
Tactic:
intro _ hmem heq
Proof state after:
case cons.refine_1
α : Type u
β : Type v
a : α
l : List α
IH : (∀ (i j : Nat) (x : i < length l) (x_1 : j < length l), l[i] = l[j] → i = j) → Nodup l
h : ∀ (i j : Nat) (x : i < length (a :: l)) (x_1 : j < length (a :: l)), (a :: l)[i] = (a :: l)[j] → i = j
a'✝ : α
hmem : a'✝ ∈ l
heq : a = a'✝
⊢ False
Theorem: List.nodup_of_get_inj
Proof state before:
case cons.refine_1
α : Type u
β : Type v
a : α
l : List α
IH : (∀ (i j : Nat) (x : i < length l) (x_1 : j < length l), l[i] = l[j] → i = j) → Nodup l
h : ∀ (i j : Nat) (x : i < length (a :: l)) (x_1 : j < length (a :: l)), (a :: l)[i] = (a :: l)[j] → i = j
a'✝ : α
hmem : a'✝ ∈ l
heq : a = a'✝
⊢ False
Tactic:
cases heq
Proof state after:
case cons.refine_1.refl
α : Type u
β : Type v
a : α
l : List α
IH : (∀ (i j : Nat) (x : i < length l) (x_1 : j < length l), l[i] = l[j] → i = j) → Nodup l
h : ∀ (i j : Nat) (x : i < length (a :: l)) (x_1 : j < length (a :: l)), (a :: l)[i] = (a :: l)[j] → i = j
hmem : a ∈ l
⊢ False
Theorem: List.nodup_of_get_inj
Proof state before:
case cons.refine_1.refl
α : Type u
β : Type v
a : α
l : List α
IH : (∀ (i j : Nat) (x : i < length l) (x_1 : j < length l), l[i] = l[j] → i = j) → Nodup l
h : ∀ (i j : Nat) (x : i < length (a :: l)) (x_1 : j < length (a :: l)), (a :: l)[i] = (a :: l)[j] → i = j
hmem : a ∈ l
⊢ False
Tactic:
have ⟨⟨i,hi⟩,hl⟩ := List.mem_iff_get.mp hmem
Proof state after:
case cons.refine_1.refl
α : Type u
β : Type v
a : α
l : List α
IH : (∀ (i j : Nat) (x : i < length l) (x_1 : j < length l), l[i] = l[j] → i = j) → Nodup l
h : ∀ (i j : Nat) (x : i < length (a :: l)) (x_1 : j < length (a :: l)), (a :: l)[i] = (a :: l)[j] → i = j
hmem : a ∈ l
i : Nat
hi : i < length l
hl : get l { val := i, isLt := hi } = a
⊢ False
Theorem: List.nodup_of_get_inj
Proof state before:
case cons.refine_1.refl
α : Type u
β : Type v
a : α
l : List α
IH : (∀ (i j : Nat) (x : i < length l) (x_1 : j < length l), l[i] = l[j] → i = j) → Nodup l
h : ∀ (i j : Nat) (x : i < length (a :: l)) (x_1 : j < length (a :: l)), (a :: l)[i] = (a :: l)[j] → i = j
hmem : a ∈ l
i : Nat
hi : i < length l
hl : get l { val := i, isLt := hi } = a
⊢ False
Tactic:
have : i+1 = 0 :=
  h (i+1) 0 (Nat.succ_lt_succ hi) l.length.zero_lt_succ hl
Proof state after:
case cons.refine_1.refl
α : Type u
β : Type v
a : α
l : List α
IH : (∀ (i j : Nat) (x : i < length l) (x_1 : j < length l), l[i] = l[j] → i = j) → Nodup l
h : ∀ (i j : Nat) (x : i < length (a :: l)) (x_1 : j < length (a :: l)), (a :: l)[i] = (a :: l)[j] → i = j
hmem : a ∈ l
i : Nat
hi : i < length l
hl : get l { val := i, isLt := hi } = a
this : i + 1 = 0
⊢ False
Theorem: List.nodup_of_get_inj
Proof state before:
case cons.refine_1.refl
α : Type u
β : Type v
a : α
l : List α
IH : (∀ (i j : Nat) (x : i < length l) (x_1 : j < length l), l[i] = l[j] → i = j) → Nodup l
h : ∀ (i j : Nat) (x : i < length (a :: l)) (x_1 : j < length (a :: l)), (a :: l)[i] = (a :: l)[j] → i = j
hmem : a ∈ l
i : Nat
hi : i < length l
hl : get l { val := i, isLt := hi } = a
this : i + 1 = 0
⊢ False
Tactic:
cases this
Proof state after:
no goals
Theorem: List.nodup_of_get_inj
Proof state before:
case cons.refine_2
α : Type u
β : Type v
a : α
l : List α
IH : (∀ (i j : Nat) (x : i < length l) (x_1 : j < length l), l[i] = l[j] → i = j) → Nodup l
h : ∀ (i j : Nat) (x : i < length (a :: l)) (x_1 : j < length (a :: l)), (a :: l)[i] = (a :: l)[j] → i = j
i j : Nat
hi : i < length l
hj : j < length l
hl : l[i] = l[j]
⊢ i = j
Tactic:
apply Nat.succ.inj
Proof state after:
case cons.refine_2.x
α : Type u
β : Type v
a : α
l : List α
IH : (∀ (i j : Nat) (x : i < length l) (x_1 : j < length l), l[i] = l[j] → i = j) → Nodup l
h : ∀ (i j : Nat) (x : i < length (a :: l)) (x_1 : j < length (a :: l)), (a :: l)[i] = (a :: l)[j] → i = j
i j : Nat
hi : i < length l
hj : j < length l
hl : l[i] = l[j]
⊢ Nat.succ i = Nat.succ j
Theorem: List.nodup_of_get_inj
Proof state before:
case cons.refine_2.x
α : Type u
β : Type v
a : α
l : List α
IH : (∀ (i j : Nat) (x : i < length l) (x_1 : j < length l), l[i] = l[j] → i = j) → Nodup l
h : ∀ (i j : Nat) (x : i < length (a :: l)) (x_1 : j < length (a :: l)), (a :: l)[i] = (a :: l)[j] → i = j
i j : Nat
hi : i < length l
hj : j < length l
hl : l[i] = l[j]
⊢ Nat.succ i = Nat.succ j
Tactic:
exact h (i+1) (j+1) (Nat.succ_lt_succ hi) (Nat.succ_lt_succ hj) hl
Proof state after:
no goals
Theorem: List.Nodup.get_inj
Proof state before:
α : Type u
β : Type v
l : List α
nodup : Nodup l
i j : Nat
hi : i < length l
hj : j < length l
h : l[i] = l[j]
⊢ i = j
Tactic:
induction l generalizing i j with
| nil => cases hi
| cons a l IH =>
  cases nodup with | cons ha nodup =>
  specialize IH nodup
  cases i <;> cases j <;> dsimp at h
  . rfl
  . exfalso
    suffices a ∈ l from ha a this rfl
    exact List.mem_iff_get.mpr ⟨_, h.symm⟩
  . exfalso
    suffices a ∈ l from ha a this rfl
    exact List.mem_iff_get.mpr ⟨_, h⟩
  . exact congrArg Nat.succ <| IH _ _ h
Proof state after:
no goals
Theorem: List.Nodup.get_inj
Proof state before:
case nil
α : Type u
β : Type v
nodup : Nodup []
i j : Nat
hi : i < length []
hj : j < length []
h : [][i] = [][j]
⊢ i = j
Tactic:
cases hi
Proof state after:
no goals
Theorem: List.Nodup.get_inj
Proof state before:
case cons
α : Type u
β : Type v
a : α
l : List α
IH : Nodup l → ∀ (i j : Nat) {hi : i < length l} {hj : j < length l}, l[i] = l[j] → i = j
nodup : Nodup (a :: l)
i j : Nat
hi : i < length (a :: l)
hj : j < length (a :: l)
h : (a :: l)[i] = (a :: l)[j]
⊢ i = j
Tactic:
cases nodup with | cons ha nodup =>
specialize IH nodup
cases i <;> cases j <;> dsimp at h
. rfl
. exfalso
  suffices a ∈ l from ha a this rfl
  exact List.mem_iff_get.mpr ⟨_, h.symm⟩
. exfalso
  suffices a ∈ l from ha a this rfl
  exact List.mem_iff_get.mpr ⟨_, h⟩
. exact congrArg Nat.succ <| IH _ _ h
Proof state after:
no goals
Theorem: List.Nodup.get_inj
Proof state before:
case cons.cons
α : Type u
β : Type v
a : α
l : List α
IH : Nodup l → ∀ (i j : Nat) {hi : i < length l} {hj : j < length l}, l[i] = l[j] → i = j
i j : Nat
hi : i < length (a :: l)
hj : j < length (a :: l)
h : (a :: l)[i] = (a :: l)[j]
nodup : Pairwise (fun x x_1 => x ≠ x_1) l
ha : ∀ (a' : α), a' ∈ l → a ≠ a'
⊢ i = j
Tactic:
specialize IH nodup
Proof state after:
case cons.cons
α : Type u
β : Type v
a : α
l : List α
i j : Nat
hi : i < length (a :: l)
hj : j < length (a :: l)
h : (a :: l)[i] = (a :: l)[j]
nodup : Pairwise (fun x x_1 => x ≠ x_1) l
ha : ∀ (a' : α), a' ∈ l → a ≠ a'
IH : ∀ (i j : Nat) {hi : i < length l} {hj : j < length l}, l[i] = l[j] → i = j
⊢ i = j