internlm/Lean-Github huggingface dataset:
Theorem: Array.nodup_push
Proof state before:
case cons
α : Type u
inst✝ : DecidableEq α
a b : α
x : Array α
IH : Nodup (push x a) ↔ Nodup x ∧ ¬a ∈ x
⊢ ¬(b ∈ x ∨ b = a) ∧ Nodup x ∧ ¬a ∈ x ↔ (¬b ∈ x ∧ Nodup x) ∧ ¬(a = b ∨ a ∈ x)
Tactic:
simp only [not_or, and_assoc]
Proof state after:
case cons
α : Type u
inst✝ : DecidableEq α
a b : α
x : Array α
IH : Nodup (push x a) ↔ Nodup x ∧ ¬a ∈ x
⊢ ¬b ∈ x ∧ ¬b = a ∧ Nodup x ∧ ¬a ∈ x ↔ ¬b ∈ x ∧ Nodup x ∧ ¬a = b ∧ ¬a ∈ x
Theorem: Array.nodup_push
Proof state before:
case cons
α : Type u
inst✝ : DecidableEq α
a b : α
x : Array α
IH : Nodup (push x a) ↔ Nodup x ∧ ¬a ∈ x
⊢ ¬b ∈ x ∧ ¬b = a ∧ Nodup x ∧ ¬a ∈ x ↔ ¬b ∈ x ∧ Nodup x ∧ ¬a = b ∧ ¬a ∈ x
Tactic:
apply and_congr_right'
Proof state after:
case cons.h
α : Type u
inst✝ : DecidableEq α
a b : α
x : Array α
IH : Nodup (push x a) ↔ Nodup x ∧ ¬a ∈ x
⊢ ¬b = a ∧ Nodup x ∧ ¬a ∈ x ↔ Nodup x ∧ ¬a = b ∧ ¬a ∈ x
Theorem: Array.nodup_push
Proof state before:
case cons.h
α : Type u
inst✝ : DecidableEq α
a b : α
x : Array α
IH : Nodup (push x a) ↔ Nodup x ∧ ¬a ∈ x
⊢ ¬b = a ∧ Nodup x ∧ ¬a ∈ x ↔ Nodup x ∧ ¬a = b ∧ ¬a ∈ x
Tactic:
simp only [← and_assoc]
Proof state after:
case cons.h
α : Type u
inst✝ : DecidableEq α
a b : α
x : Array α
IH : Nodup (push x a) ↔ Nodup x ∧ ¬a ∈ x
⊢ (¬b = a ∧ Nodup x) ∧ ¬a ∈ x ↔ (Nodup x ∧ ¬a = b) ∧ ¬a ∈ x
Theorem: Array.nodup_push
Proof state before:
case cons.h
α : Type u
inst✝ : DecidableEq α
a b : α
x : Array α
IH : Nodup (push x a) ↔ Nodup x ∧ ¬a ∈ x
⊢ (¬b = a ∧ Nodup x) ∧ ¬a ∈ x ↔ (Nodup x ∧ ¬a = b) ∧ ¬a ∈ x
Tactic:
rewrite[and_comm (a:=x.Nodup)]
Proof state after:
case cons.h
α : Type u
inst✝ : DecidableEq α
a b : α
x : Array α
IH : Nodup (push x a) ↔ Nodup x ∧ ¬a ∈ x
⊢ (¬b = a ∧ Nodup x) ∧ ¬a ∈ x ↔ (¬a = b ∧ Nodup x) ∧ ¬a ∈ x
Theorem: Array.nodup_push
Proof state before:
case cons.h
α : Type u
inst✝ : DecidableEq α
a b : α
x : Array α
IH : Nodup (push x a) ↔ Nodup x ∧ ¬a ∈ x
⊢ (¬b = a ∧ Nodup x) ∧ ¬a ∈ x ↔ (¬a = b ∧ Nodup x) ∧ ¬a ∈ x
Tactic:
apply and_congr_left'
Proof state after:
case cons.h.h
α : Type u
inst✝ : DecidableEq α
a b : α
x : Array α
IH : Nodup (push x a) ↔ Nodup x ∧ ¬a ∈ x
⊢ ¬b = a ∧ Nodup x ↔ ¬a = b ∧ Nodup x
Theorem: Array.nodup_push
Proof state before:
case cons.h.h
α : Type u
inst✝ : DecidableEq α
a b : α
x : Array α
IH : Nodup (push x a) ↔ Nodup x ∧ ¬a ∈ x
⊢ ¬b = a ∧ Nodup x ↔ ¬a = b ∧ Nodup x
Tactic:
apply and_congr_left'
Proof state after:
case cons.h.h.h
α : Type u
inst✝ : DecidableEq α
a b : α
x : Array α
IH : Nodup (push x a) ↔ Nodup x ∧ ¬a ∈ x
⊢ ¬b = a ↔ ¬a = b
Theorem: Array.nodup_push
Proof state before:
case cons.h.h.h
α : Type u
inst✝ : DecidableEq α
a b : α
x : Array α
IH : Nodup (push x a) ↔ Nodup x ∧ ¬a ∈ x
⊢ ¬b = a ↔ ¬a = b
Tactic:
exact ⟨Ne.symm, Ne.symm⟩
Proof state after:
no goals
Theorem: Array.nodup_iff_nodup_data
Proof state before:
α : Type u
inst✝ : DecidableEq α
x : Array α
⊢ Nodup x ↔ List.Nodup x.data
Tactic:
induction x using cons_induction with
| empty => simp only [nodup_empty, true_iff]; exact .nil
| cons a x IH =>
  simp only [nodup_cons, data_cons]
  dsimp [List.Nodup]; rewrite [List.pairwise_cons, IH]
  apply and_congr_left'
  simp only [← mem_iff_mem_data]
  constructor
  . intro h _ ha hcntr; cases hcntr
    exact h ha
  . intro h ha
    exact h a ha rfl
Proof state after:
no goals
Theorem: Array.nodup_iff_nodup_data
Proof state before:
case empty
α : Type u
inst✝ : DecidableEq α
⊢ Nodup #[] ↔ List.Nodup #[].data
Tactic:
simp only [nodup_empty, true_iff]
Proof state after:
case empty
α : Type u
inst✝ : DecidableEq α
⊢ List.Nodup #[].data
Theorem: Array.nodup_iff_nodup_data
Proof state before:
case empty
α : Type u
inst✝ : DecidableEq α
⊢ List.Nodup #[].data
Tactic:
exact .nil
Proof state after:
no goals
Theorem: Array.nodup_iff_nodup_data
Proof state before:
case cons
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
IH : Nodup x ↔ List.Nodup x.data
⊢ Nodup (cons a x) ↔ List.Nodup (cons a x).data
Tactic:
simp only [nodup_cons, data_cons]
Proof state after:
case cons
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
IH : Nodup x ↔ List.Nodup x.data
⊢ ¬a ∈ x ∧ Nodup x ↔ List.Nodup (a :: x.data)
Theorem: Array.nodup_iff_nodup_data
Proof state before:
case cons
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
IH : Nodup x ↔ List.Nodup x.data
⊢ ¬a ∈ x ∧ Nodup x ↔ List.Nodup (a :: x.data)
Tactic:
dsimp [List.Nodup]
Proof state after:
case cons
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
IH : Nodup x ↔ List.Nodup x.data
⊢ ¬a ∈ x ∧ Nodup x ↔ List.Pairwise (fun x x_1 => ¬x = x_1) (a :: x.data)
Theorem: Array.nodup_iff_nodup_data
Proof state before:
case cons
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
IH : Nodup x ↔ List.Nodup x.data
⊢ ¬a ∈ x ∧ Nodup x ↔ List.Pairwise (fun x x_1 => ¬x = x_1) (a :: x.data)
Tactic:
rewrite [List.pairwise_cons, IH]
Proof state after:
case cons
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
IH : Nodup x ↔ List.Nodup x.data
⊢ ¬a ∈ x ∧ List.Nodup x.data ↔ (∀ (a' : α), a' ∈ x.data → ¬a = a') ∧ List.Pairwise (fun x x_1 => ¬x = x_1) x.data
Theorem: Array.nodup_iff_nodup_data
Proof state before:
case cons
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
IH : Nodup x ↔ List.Nodup x.data
⊢ ¬a ∈ x ∧ List.Nodup x.data ↔ (∀ (a' : α), a' ∈ x.data → ¬a = a') ∧ List.Pairwise (fun x x_1 => ¬x = x_1) x.data
Tactic:
apply and_congr_left'
Proof state after:
case cons.h
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
IH : Nodup x ↔ List.Nodup x.data
⊢ ¬a ∈ x ↔ ∀ (a' : α), a' ∈ x.data → ¬a = a'
Theorem: Array.nodup_iff_nodup_data
Proof state before:
case cons.h
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
IH : Nodup x ↔ List.Nodup x.data
⊢ ¬a ∈ x ↔ ∀ (a' : α), a' ∈ x.data → ¬a = a'
Tactic:
simp only [← mem_iff_mem_data]
Proof state after:
case cons.h
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
IH : Nodup x ↔ List.Nodup x.data
⊢ ¬a ∈ x ↔ ∀ (a' : α), a' ∈ x → ¬a = a'
Theorem: Array.nodup_iff_nodup_data
Proof state before:
case cons.h
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
IH : Nodup x ↔ List.Nodup x.data
⊢ ¬a ∈ x ↔ ∀ (a' : α), a' ∈ x → ¬a = a'
Tactic:
constructor
Proof state after:
case cons.h.mp
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
IH : Nodup x ↔ List.Nodup x.data
⊢ ¬a ∈ x → ∀ (a' : α), a' ∈ x → ¬a = a'

case cons.h.mpr
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
IH : Nodup x ↔ List.Nodup x.data
⊢ (∀ (a' : α), a' ∈ x → ¬a = a') → ¬a ∈ x
Theorem: Array.nodup_iff_nodup_data
Proof state before:
case cons.h.mp
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
IH : Nodup x ↔ List.Nodup x.data
⊢ ¬a ∈ x → ∀ (a' : α), a' ∈ x → ¬a = a'

case cons.h.mpr
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
IH : Nodup x ↔ List.Nodup x.data
⊢ (∀ (a' : α), a' ∈ x → ¬a = a') → ¬a ∈ x
Tactic:
. intro h _ ha hcntr; cases hcntr
  exact h ha
Proof state after:
case cons.h.mpr
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
IH : Nodup x ↔ List.Nodup x.data
⊢ (∀ (a' : α), a' ∈ x → ¬a = a') → ¬a ∈ x
Theorem: Array.nodup_iff_nodup_data
Proof state before:
case cons.h.mpr
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
IH : Nodup x ↔ List.Nodup x.data
⊢ (∀ (a' : α), a' ∈ x → ¬a = a') → ¬a ∈ x
Tactic:
. intro h ha
  exact h a ha rfl
Proof state after:
no goals
Theorem: Array.nodup_iff_nodup_data
Proof state before:
case cons.h.mp
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
IH : Nodup x ↔ List.Nodup x.data
⊢ ¬a ∈ x → ∀ (a' : α), a' ∈ x → ¬a = a'
Tactic:
intro h _ ha hcntr
Proof state after:
case cons.h.mp
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
IH : Nodup x ↔ List.Nodup x.data
h : ¬a ∈ x
a'✝ : α
ha : a'✝ ∈ x
hcntr : a = a'✝
⊢ False
Theorem: Array.nodup_iff_nodup_data
Proof state before:
case cons.h.mp
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
IH : Nodup x ↔ List.Nodup x.data
h : ¬a ∈ x
a'✝ : α
ha : a'✝ ∈ x
hcntr : a = a'✝
⊢ False
Tactic:
cases hcntr
Proof state after:
case cons.h.mp.refl
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
IH : Nodup x ↔ List.Nodup x.data
h : ¬a ∈ x
ha : a ∈ x
⊢ False
Theorem: Array.nodup_iff_nodup_data
Proof state before:
case cons.h.mp.refl
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
IH : Nodup x ↔ List.Nodup x.data
h : ¬a ∈ x
ha : a ∈ x
⊢ False
Tactic:
exact h ha
Proof state after:
no goals
Theorem: Array.nodup_iff_nodup_data
Proof state before:
case cons.h.mpr
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
IH : Nodup x ↔ List.Nodup x.data
⊢ (∀ (a' : α), a' ∈ x → ¬a = a') → ¬a ∈ x
Tactic:
intro h ha
Proof state after:
case cons.h.mpr
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
IH : Nodup x ↔ List.Nodup x.data
h : ∀ (a' : α), a' ∈ x → ¬a = a'
ha : a ∈ x
⊢ False
Theorem: Array.nodup_iff_nodup_data
Proof state before:
case cons.h.mpr
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
IH : Nodup x ↔ List.Nodup x.data
h : ∀ (a' : α), a' ∈ x → ¬a = a'
ha : a ∈ x
⊢ False
Tactic:
exact h a ha rfl
Proof state after:
no goals
Theorem: Array.nodup_iff_getElem_inj
Proof state before:
α : Type u
inst✝ : DecidableEq α
x : Array α
⊢ Nodup x ↔ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
Tactic:
induction x using cons_induction with
| empty =>
  simp only [nodup_empty, true_iff]
  intro i; exact i.elim0
| cons a x IH =>
  rewrite [nodup_cons, IH]; clear IH
  constructor
  . intro h i j hxij
    rcases i with ⟨i,hi⟩; rcases j with ⟨j,hj⟩
    cases i <;> cases j <;> simp at hxij ⊢
    . exfalso; apply h.1
      rewrite [hxij]; exact getElem_mem x _
    . exfalso; apply h.1
      rewrite [← hxij]; exact getElem_mem x _
    . exact Fin.val_eq_of_eq <| h.2 ⟨_, Nat.lt_of_succ_lt_succ hi⟩ ⟨_, Nat.lt_of_succ_lt_succ hj⟩ hxij
  . intro h
    constructor
    . intro hmem
      have ⟨i,hi, hxi⟩ := mem_iff_get.mp hmem
      specialize h ⟨i+1, Nat.succ_lt_succ hi⟩ ⟨0, x.size.zero_lt_succ⟩ hxi
      cases h
    . intro i j
      specialize h i.succ j.succ
      simp only [size_cons, Fin.val_succ, getElem_cons_succ, Fin.succ_inj] at h
      exact h
Proof state after:
no goals
Theorem: Array.nodup_iff_getElem_inj
Proof state before:
case empty
α : Type u
inst✝ : DecidableEq α
⊢ Nodup #[] ↔ ∀ (i j : Fin (size #[])), #[][↑i] = #[][↑j] → i = j
Tactic:
simp only [nodup_empty, true_iff]
Proof state after:
case empty
α : Type u
inst✝ : DecidableEq α
⊢ ∀ (i j : Fin (size #[])), #[][↑i] = #[][↑j] → i = j
Theorem: Array.nodup_iff_getElem_inj
Proof state before:
case empty
α : Type u
inst✝ : DecidableEq α
⊢ ∀ (i j : Fin (size #[])), #[][↑i] = #[][↑j] → i = j
Tactic:
intro i
Proof state after:
case empty
α : Type u
inst✝ : DecidableEq α
i : Fin (size #[])
⊢ ∀ (j : Fin (size #[])), #[][↑i] = #[][↑j] → i = j
Theorem: Array.nodup_iff_getElem_inj
Proof state before:
case empty
α : Type u
inst✝ : DecidableEq α
i : Fin (size #[])
⊢ ∀ (j : Fin (size #[])), #[][↑i] = #[][↑j] → i = j
Tactic:
exact i.elim0
Proof state after:
no goals
Theorem: Array.nodup_iff_getElem_inj
Proof state before:
case cons
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
IH : Nodup x ↔ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
⊢ Nodup (cons a x) ↔ ∀ (i j : Fin (size (cons a x))), (cons a x)[↑i] = (cons a x)[↑j] → i = j
Tactic:
rewrite [nodup_cons, IH]
Proof state after:
case cons
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
IH : Nodup x ↔ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
⊢ (¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j) ↔
    ∀ (i j : Fin (size (cons a x))), (cons a x)[↑i] = (cons a x)[↑j] → i = j
Theorem: Array.nodup_iff_getElem_inj
Proof state before:
case cons
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
IH : Nodup x ↔ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
⊢ (¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j) ↔
    ∀ (i j : Fin (size (cons a x))), (cons a x)[↑i] = (cons a x)[↑j] → i = j
Tactic:
clear IH
Proof state after:
case cons
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
⊢ (¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j) ↔
    ∀ (i j : Fin (size (cons a x))), (cons a x)[↑i] = (cons a x)[↑j] → i = j
Theorem: Array.nodup_iff_getElem_inj
Proof state before:
case cons
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
⊢ (¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j) ↔
    ∀ (i j : Fin (size (cons a x))), (cons a x)[↑i] = (cons a x)[↑j] → i = j
Tactic:
constructor
Proof state after:
case cons.mp
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
⊢ (¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j) →
    ∀ (i j : Fin (size (cons a x))), (cons a x)[↑i] = (cons a x)[↑j] → i = j

case cons.mpr
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
⊢ (∀ (i j : Fin (size (cons a x))), (cons a x)[↑i] = (cons a x)[↑j] → i = j) →
    ¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
Theorem: Array.nodup_iff_getElem_inj
Proof state before:
case cons.mp
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
⊢ (¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j) →
    ∀ (i j : Fin (size (cons a x))), (cons a x)[↑i] = (cons a x)[↑j] → i = j

case cons.mpr
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
⊢ (∀ (i j : Fin (size (cons a x))), (cons a x)[↑i] = (cons a x)[↑j] → i = j) →
    ¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
Tactic:
. intro h i j hxij
  rcases i with ⟨i,hi⟩; rcases j with ⟨j,hj⟩
  cases i <;> cases j <;> simp at hxij ⊢
  . exfalso; apply h.1
    rewrite [hxij]; exact getElem_mem x _
  . exfalso; apply h.1
    rewrite [← hxij]; exact getElem_mem x _
  . exact Fin.val_eq_of_eq <| h.2 ⟨_, Nat.lt_of_succ_lt_succ hi⟩ ⟨_, Nat.lt_of_succ_lt_succ hj⟩ hxij
Proof state after:
case cons.mpr
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
⊢ (∀ (i j : Fin (size (cons a x))), (cons a x)[↑i] = (cons a x)[↑j] → i = j) →
    ¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
Theorem: Array.nodup_iff_getElem_inj
Proof state before:
case cons.mpr
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
⊢ (∀ (i j : Fin (size (cons a x))), (cons a x)[↑i] = (cons a x)[↑j] → i = j) →
    ¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
Tactic:
. intro h
  constructor
  . intro hmem
    have ⟨i,hi, hxi⟩ := mem_iff_get.mp hmem
    specialize h ⟨i+1, Nat.succ_lt_succ hi⟩ ⟨0, x.size.zero_lt_succ⟩ hxi
    cases h
  . intro i j
    specialize h i.succ j.succ
    simp only [size_cons, Fin.val_succ, getElem_cons_succ, Fin.succ_inj] at h
    exact h
Proof state after:
no goals
Theorem: Array.nodup_iff_getElem_inj
Proof state before:
case cons.mp
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
⊢ (¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j) →
    ∀ (i j : Fin (size (cons a x))), (cons a x)[↑i] = (cons a x)[↑j] → i = j
Tactic:
intro h i j hxij
Proof state after:
case cons.mp
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
i j : Fin (size (cons a x))
hxij : (cons a x)[↑i] = (cons a x)[↑j]
⊢ i = j
Theorem: Array.nodup_iff_getElem_inj
Proof state before:
case cons.mp
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
i j : Fin (size (cons a x))
hxij : (cons a x)[↑i] = (cons a x)[↑j]
⊢ i = j
Tactic:
rcases i with ⟨i,hi⟩
Proof state after:
case cons.mp.mk
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
j : Fin (size (cons a x))
i : Nat
hi : i < size (cons a x)
hxij : (cons a x)[↑{ val := i, isLt := hi }] = (cons a x)[↑j]
⊢ { val := i, isLt := hi } = j
Theorem: Array.nodup_iff_getElem_inj
Proof state before:
case cons.mp.mk
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
j : Fin (size (cons a x))
i : Nat
hi : i < size (cons a x)
hxij : (cons a x)[↑{ val := i, isLt := hi }] = (cons a x)[↑j]
⊢ { val := i, isLt := hi } = j
Tactic:
rcases j with ⟨j,hj⟩
Proof state after:
case cons.mp.mk.mk
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
i : Nat
hi : i < size (cons a x)
j : Nat
hj : j < size (cons a x)
hxij : (cons a x)[↑{ val := i, isLt := hi }] = (cons a x)[↑{ val := j, isLt := hj }]
⊢ { val := i, isLt := hi } = { val := j, isLt := hj }
Theorem: Array.nodup_iff_getElem_inj
Proof state before:
case cons.mp.mk.mk
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
i : Nat
hi : i < size (cons a x)
j : Nat
hj : j < size (cons a x)
hxij : (cons a x)[↑{ val := i, isLt := hi }] = (cons a x)[↑{ val := j, isLt := hj }]
⊢ { val := i, isLt := hi } = { val := j, isLt := hj }
Tactic:
cases i <;> cases j <;> simp at hxij ⊢
Proof state after:
case cons.mp.mk.mk.zero.succ
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
hi : Nat.zero < size (cons a x)
n✝ : Nat
hj : Nat.succ n✝ < size (cons a x)
hxij : a = x[n✝]
⊢ 0 = { val := Nat.succ n✝, isLt := hj }

case cons.mp.mk.mk.succ.zero
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
n✝ : Nat
hi : Nat.succ n✝ < size (cons a x)
hj : Nat.zero < size (cons a x)
hxij : x[n✝] = a
⊢ { val := Nat.succ n✝, isLt := hi } = 0

case cons.mp.mk.mk.succ.succ
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
n✝¹ : Nat
hi : Nat.succ n✝¹ < size (cons a x)
n✝ : Nat
hj : Nat.succ n✝ < size (cons a x)
hxij : x[n✝¹] = x[n✝]
⊢ n✝¹ = n✝
Theorem: Array.nodup_iff_getElem_inj
Proof state before:
case cons.mp.mk.mk.zero.succ
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
hi : Nat.zero < size (cons a x)
n✝ : Nat
hj : Nat.succ n✝ < size (cons a x)
hxij : a = x[n✝]
⊢ 0 = { val := Nat.succ n✝, isLt := hj }

case cons.mp.mk.mk.succ.zero
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
n✝ : Nat
hi : Nat.succ n✝ < size (cons a x)
hj : Nat.zero < size (cons a x)
hxij : x[n✝] = a
⊢ { val := Nat.succ n✝, isLt := hi } = 0

case cons.mp.mk.mk.succ.succ
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
n✝¹ : Nat
hi : Nat.succ n✝¹ < size (cons a x)
n✝ : Nat
hj : Nat.succ n✝ < size (cons a x)
hxij : x[n✝¹] = x[n✝]
⊢ n✝¹ = n✝
Tactic:
. exfalso; apply h.1
  rewrite [hxij]; exact getElem_mem x _
Proof state after:
case cons.mp.mk.mk.succ.zero
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
n✝ : Nat
hi : Nat.succ n✝ < size (cons a x)
hj : Nat.zero < size (cons a x)
hxij : x[n✝] = a
⊢ { val := Nat.succ n✝, isLt := hi } = 0

case cons.mp.mk.mk.succ.succ
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
n✝¹ : Nat
hi : Nat.succ n✝¹ < size (cons a x)
n✝ : Nat
hj : Nat.succ n✝ < size (cons a x)
hxij : x[n✝¹] = x[n✝]
⊢ n✝¹ = n✝
Theorem: Array.nodup_iff_getElem_inj
Proof state before:
case cons.mp.mk.mk.succ.zero
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
n✝ : Nat
hi : Nat.succ n✝ < size (cons a x)
hj : Nat.zero < size (cons a x)
hxij : x[n✝] = a
⊢ { val := Nat.succ n✝, isLt := hi } = 0

case cons.mp.mk.mk.succ.succ
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
n✝¹ : Nat
hi : Nat.succ n✝¹ < size (cons a x)
n✝ : Nat
hj : Nat.succ n✝ < size (cons a x)
hxij : x[n✝¹] = x[n✝]
⊢ n✝¹ = n✝
Tactic:
. exfalso; apply h.1
  rewrite [← hxij]; exact getElem_mem x _
Proof state after:
case cons.mp.mk.mk.succ.succ
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
n✝¹ : Nat
hi : Nat.succ n✝¹ < size (cons a x)
n✝ : Nat
hj : Nat.succ n✝ < size (cons a x)
hxij : x[n✝¹] = x[n✝]
⊢ n✝¹ = n✝
Theorem: Array.nodup_iff_getElem_inj
Proof state before:
case cons.mp.mk.mk.succ.succ
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
n✝¹ : Nat
hi : Nat.succ n✝¹ < size (cons a x)
n✝ : Nat
hj : Nat.succ n✝ < size (cons a x)
hxij : x[n✝¹] = x[n✝]
⊢ n✝¹ = n✝
Tactic:
. exact Fin.val_eq_of_eq <| h.2 ⟨_, Nat.lt_of_succ_lt_succ hi⟩ ⟨_, Nat.lt_of_succ_lt_succ hj⟩ hxij
Proof state after:
no goals
Theorem: Array.nodup_iff_getElem_inj
Proof state before:
case cons.mp.mk.mk.zero.succ
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
hi : Nat.zero < size (cons a x)
n✝ : Nat
hj : Nat.succ n✝ < size (cons a x)
hxij : a = x[n✝]
⊢ 0 = { val := Nat.succ n✝, isLt := hj }
Tactic:
exfalso
Proof state after:
case cons.mp.mk.mk.zero.succ.h
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
hi : Nat.zero < size (cons a x)
n✝ : Nat
hj : Nat.succ n✝ < size (cons a x)
hxij : a = x[n✝]
⊢ False
Theorem: Array.nodup_iff_getElem_inj
Proof state before:
case cons.mp.mk.mk.zero.succ.h
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
hi : Nat.zero < size (cons a x)
n✝ : Nat
hj : Nat.succ n✝ < size (cons a x)
hxij : a = x[n✝]
⊢ False
Tactic:
apply h.1
Proof state after:
case cons.mp.mk.mk.zero.succ.h
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
hi : Nat.zero < size (cons a x)
n✝ : Nat
hj : Nat.succ n✝ < size (cons a x)
hxij : a = x[n✝]
⊢ a ∈ x
Theorem: Array.nodup_iff_getElem_inj
Proof state before:
case cons.mp.mk.mk.zero.succ.h
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
hi : Nat.zero < size (cons a x)
n✝ : Nat
hj : Nat.succ n✝ < size (cons a x)
hxij : a = x[n✝]
⊢ a ∈ x
Tactic:
rewrite [hxij]
Proof state after:
case cons.mp.mk.mk.zero.succ.h
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
hi : Nat.zero < size (cons a x)
n✝ : Nat
hj : Nat.succ n✝ < size (cons a x)
hxij : a = x[n✝]
⊢ x[n✝] ∈ x
Theorem: Array.nodup_iff_getElem_inj
Proof state before:
case cons.mp.mk.mk.zero.succ.h
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
hi : Nat.zero < size (cons a x)
n✝ : Nat
hj : Nat.succ n✝ < size (cons a x)
hxij : a = x[n✝]
⊢ x[n✝] ∈ x
Tactic:
exact getElem_mem x _
Proof state after:
no goals
Theorem: Array.nodup_iff_getElem_inj
Proof state before:
case cons.mp.mk.mk.succ.zero
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
n✝ : Nat
hi : Nat.succ n✝ < size (cons a x)
hj : Nat.zero < size (cons a x)
hxij : x[n✝] = a
⊢ { val := Nat.succ n✝, isLt := hi } = 0
Tactic:
exfalso
Proof state after:
case cons.mp.mk.mk.succ.zero.h
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
n✝ : Nat
hi : Nat.succ n✝ < size (cons a x)
hj : Nat.zero < size (cons a x)
hxij : x[n✝] = a
⊢ False
Theorem: Array.nodup_iff_getElem_inj
Proof state before:
case cons.mp.mk.mk.succ.zero.h
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
n✝ : Nat
hi : Nat.succ n✝ < size (cons a x)
hj : Nat.zero < size (cons a x)
hxij : x[n✝] = a
⊢ False
Tactic:
apply h.1
Proof state after:
case cons.mp.mk.mk.succ.zero.h
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
n✝ : Nat
hi : Nat.succ n✝ < size (cons a x)
hj : Nat.zero < size (cons a x)
hxij : x[n✝] = a
⊢ a ∈ x
Theorem: Array.nodup_iff_getElem_inj
Proof state before:
case cons.mp.mk.mk.succ.zero.h
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
n✝ : Nat
hi : Nat.succ n✝ < size (cons a x)
hj : Nat.zero < size (cons a x)
hxij : x[n✝] = a
⊢ a ∈ x
Tactic:
rewrite [← hxij]
Proof state after:
case cons.mp.mk.mk.succ.zero.h
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
n✝ : Nat
hi : Nat.succ n✝ < size (cons a x)
hj : Nat.zero < size (cons a x)
hxij : x[n✝] = a
⊢ x[n✝] ∈ x
Theorem: Array.nodup_iff_getElem_inj
Proof state before:
case cons.mp.mk.mk.succ.zero.h
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
n✝ : Nat
hi : Nat.succ n✝ < size (cons a x)
hj : Nat.zero < size (cons a x)
hxij : x[n✝] = a
⊢ x[n✝] ∈ x
Tactic:
exact getElem_mem x _
Proof state after:
no goals