internlm/Lean-Github huggingface dataset:
Theorem: Array.getElem_pmap
Proof state before:
case refine_2
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
as : Array α
h : ∀ (i : Nat) (hi : i < size as), p as[i]
i : Nat
hi : i < size (pmap f as h)
k : Nat
hk : k < size as
bs : Array β
IH : ∀ (j : Nat) (hjk : j < k) (hk : k ≤ size as) (hbsk : size bs = k), bs[j] = f as[j] (_ : p as[j])
j : Nat
hj : j < k + 1
hk✝ : k + 1 ≤ size as
hbsk✝ : size (push bs (f as[{ val := k, isLt := hk }.val] (_ : p as[{ val := k, isLt := hk }.val]))) = k + 1
hbsk : size bs + 1 = k + 1
⊢ (push bs (f as[k] (_ : p as[{ val := k, isLt := hk }.val])))[j] = f as[j] (_ : p as[j])
Tactic:
cases hbsk
Proof state after:
case refine_2.refl
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
as : Array α
h : ∀ (i : Nat) (hi : i < size as), p as[i]
i : Nat
hi : i < size (pmap f as h)
bs : Array β
j : Nat
hk : List.length bs.data < size as
IH :
  ∀ (j : Nat) (hjk : j < List.length bs.data) (hk : List.length bs.data ≤ size as)
    (hbsk : size bs = List.length bs.data), bs[j] = f as[j] (_ : p as[j])
hj : j < List.length bs.data + 1
hk✝ : List.length bs.data + 1 ≤ size as
hbsk :
  size
      (push bs
        (f as[{ val := List.length bs.data, isLt := hk }.val]
          (_ : p as[{ val := List.length bs.data, isLt := hk }.val]))) =
    List.length bs.data + 1
⊢ (push bs (f as[List.length bs.data] (_ : p as[{ val := List.length bs.data, isLt := hk }.val])))[j] =
    f as[j] (_ : p as[j])
Theorem: Array.getElem_pmap
Proof state before:
case refine_2.refl
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
as : Array α
h : ∀ (i : Nat) (hi : i < size as), p as[i]
i : Nat
hi : i < size (pmap f as h)
bs : Array β
j : Nat
hk : List.length bs.data < size as
IH :
  ∀ (j : Nat) (hjk : j < List.length bs.data) (hk : List.length bs.data ≤ size as)
    (hbsk : size bs = List.length bs.data), bs[j] = f as[j] (_ : p as[j])
hj : j < List.length bs.data + 1
hk✝ : List.length bs.data + 1 ≤ size as
hbsk :
  size
      (push bs
        (f as[{ val := List.length bs.data, isLt := hk }.val]
          (_ : p as[{ val := List.length bs.data, isLt := hk }.val]))) =
    List.length bs.data + 1
⊢ (push bs (f as[List.length bs.data] (_ : p as[{ val := List.length bs.data, isLt := hk }.val])))[j] =
    f as[j] (_ : p as[j])
Tactic:
cases Nat.eq_or_lt_of_le (Nat.le_of_succ_le_succ hj) with
| inl heq =>
  cases heq; exact get_push_eq ..
| inr hlt =>
  rewrite [bs.get_push_lt _ j hlt]
  exact IH j hlt (Nat.le_of_lt hk) rfl
Proof state after:
no goals
Theorem: Array.getElem_pmap
Proof state before:
case refine_2.refl.inl
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
as : Array α
h : ∀ (i : Nat) (hi : i < size as), p as[i]
i : Nat
hi : i < size (pmap f as h)
bs : Array β
j : Nat
hk : List.length bs.data < size as
IH :
  ∀ (j : Nat) (hjk : j < List.length bs.data) (hk : List.length bs.data ≤ size as)
    (hbsk : size bs = List.length bs.data), bs[j] = f as[j] (_ : p as[j])
hj : j < List.length bs.data + 1
hk✝ : List.length bs.data + 1 ≤ size as
hbsk :
  size
      (push bs
        (f as[{ val := List.length bs.data, isLt := hk }.val]
          (_ : p as[{ val := List.length bs.data, isLt := hk }.val]))) =
    List.length bs.data + 1
heq : j = List.length bs.data
⊢ (push bs (f as[List.length bs.data] (_ : p as[{ val := List.length bs.data, isLt := hk }.val])))[j] =
    f as[j] (_ : p as[j])
Tactic:
cases heq
Proof state after:
case refine_2.refl.inl.refl
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
as : Array α
h : ∀ (i : Nat) (hi : i < size as), p as[i]
i : Nat
hi : i < size (pmap f as h)
bs : Array β
hk : List.length bs.data < size as
IH :
  ∀ (j : Nat) (hjk : j < List.length bs.data) (hk : List.length bs.data ≤ size as)
    (hbsk : size bs = List.length bs.data), bs[j] = f as[j] (_ : p as[j])
hk✝ : List.length bs.data + 1 ≤ size as
hbsk :
  size
      (push bs
        (f as[{ val := List.length bs.data, isLt := hk }.val]
          (_ : p as[{ val := List.length bs.data, isLt := hk }.val]))) =
    List.length bs.data + 1
hj : List.length bs.data < List.length bs.data + 1
⊢ (push bs
        (f as[List.length bs.data] (_ : p as[{ val := List.length bs.data, isLt := hk }.val])))[List.length bs.data] =
    f as[List.length bs.data] (_ : p as[List.length bs.data])
Theorem: Array.getElem_pmap
Proof state before:
case refine_2.refl.inl.refl
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
as : Array α
h : ∀ (i : Nat) (hi : i < size as), p as[i]
i : Nat
hi : i < size (pmap f as h)
bs : Array β
hk : List.length bs.data < size as
IH :
  ∀ (j : Nat) (hjk : j < List.length bs.data) (hk : List.length bs.data ≤ size as)
    (hbsk : size bs = List.length bs.data), bs[j] = f as[j] (_ : p as[j])
hk✝ : List.length bs.data + 1 ≤ size as
hbsk :
  size
      (push bs
        (f as[{ val := List.length bs.data, isLt := hk }.val]
          (_ : p as[{ val := List.length bs.data, isLt := hk }.val]))) =
    List.length bs.data + 1
hj : List.length bs.data < List.length bs.data + 1
⊢ (push bs
        (f as[List.length bs.data] (_ : p as[{ val := List.length bs.data, isLt := hk }.val])))[List.length bs.data] =
    f as[List.length bs.data] (_ : p as[List.length bs.data])
Tactic:
exact get_push_eq ..
Proof state after:
no goals
Theorem: Array.getElem_pmap
Proof state before:
case refine_2.refl.inr
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
as : Array α
h : ∀ (i : Nat) (hi : i < size as), p as[i]
i : Nat
hi : i < size (pmap f as h)
bs : Array β
j : Nat
hk : List.length bs.data < size as
IH :
  ∀ (j : Nat) (hjk : j < List.length bs.data) (hk : List.length bs.data ≤ size as)
    (hbsk : size bs = List.length bs.data), bs[j] = f as[j] (_ : p as[j])
hj : j < List.length bs.data + 1
hk✝ : List.length bs.data + 1 ≤ size as
hbsk :
  size
      (push bs
        (f as[{ val := List.length bs.data, isLt := hk }.val]
          (_ : p as[{ val := List.length bs.data, isLt := hk }.val]))) =
    List.length bs.data + 1
hlt : j < List.length bs.data
⊢ (push bs (f as[List.length bs.data] (_ : p as[{ val := List.length bs.data, isLt := hk }.val])))[j] =
    f as[j] (_ : p as[j])
Tactic:
rewrite [bs.get_push_lt _ j hlt]
Proof state after:
case refine_2.refl.inr
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
as : Array α
h : ∀ (i : Nat) (hi : i < size as), p as[i]
i : Nat
hi : i < size (pmap f as h)
bs : Array β
j : Nat
hk : List.length bs.data < size as
IH :
  ∀ (j : Nat) (hjk : j < List.length bs.data) (hk : List.length bs.data ≤ size as)
    (hbsk : size bs = List.length bs.data), bs[j] = f as[j] (_ : p as[j])
hj : j < List.length bs.data + 1
hk✝ : List.length bs.data + 1 ≤ size as
hbsk :
  size
      (push bs
        (f as[{ val := List.length bs.data, isLt := hk }.val]
          (_ : p as[{ val := List.length bs.data, isLt := hk }.val]))) =
    List.length bs.data + 1
hlt : j < List.length bs.data
⊢ bs[j] = f as[j] (_ : p as[j])
Theorem: Array.getElem_pmap
Proof state before:
case refine_2.refl.inr
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
as : Array α
h : ∀ (i : Nat) (hi : i < size as), p as[i]
i : Nat
hi : i < size (pmap f as h)
bs : Array β
j : Nat
hk : List.length bs.data < size as
IH :
  ∀ (j : Nat) (hjk : j < List.length bs.data) (hk : List.length bs.data ≤ size as)
    (hbsk : size bs = List.length bs.data), bs[j] = f as[j] (_ : p as[j])
hj : j < List.length bs.data + 1
hk✝ : List.length bs.data + 1 ≤ size as
hbsk :
  size
      (push bs
        (f as[{ val := List.length bs.data, isLt := hk }.val]
          (_ : p as[{ val := List.length bs.data, isLt := hk }.val]))) =
    List.length bs.data + 1
hlt : j < List.length bs.data
⊢ bs[j] = f as[j] (_ : p as[j])
Tactic:
exact IH j hlt (Nat.le_of_lt hk) rfl
Proof state after:
no goals
Theorem: Array.mem_iff_mem_data
Proof state before:
α : Type u
inst✝ : DecidableEq α
a : α
as : Array α
⊢ a ∈ as ↔ a ∈ as.data
Tactic:
show as.any (fun b => a = b) = true ↔ a ∈ as.data
Proof state after:
α : Type u
inst✝ : DecidableEq α
a : α
as : Array α
⊢ any as (fun b => decide (a = b)) 0 (size as) = true ↔ a ∈ as.data
Theorem: Array.mem_iff_mem_data
Proof state before:
α : Type u
inst✝ : DecidableEq α
a : α
as : Array α
⊢ any as (fun b => decide (a = b)) 0 (size as) = true ↔ a ∈ as.data
Tactic:
rewrite [any_eq_any_data]
Proof state after:
α : Type u
inst✝ : DecidableEq α
a : α
as : Array α
⊢ (List.any as.data fun b => decide (a = b)) = true ↔ a ∈ as.data
Theorem: Array.mem_iff_mem_data
Proof state before:
α : Type u
inst✝ : DecidableEq α
a : α
as : Array α
⊢ (List.any as.data fun b => decide (a = b)) = true ↔ a ∈ as.data
Tactic:
simp only [List.any_eq_true, List.mem_iff_get]
Proof state after:
α : Type u
inst✝ : DecidableEq α
a : α
as : Array α
⊢ (∃ x, (∃ n, List.get as.data n = x) ∧ decide (a = x) = true) ↔ ∃ n, List.get as.data n = a
Theorem: Array.mem_iff_mem_data
Proof state before:
α : Type u
inst✝ : DecidableEq α
a : α
as : Array α
⊢ (∃ x, (∃ n, List.get as.data n = x) ∧ decide (a = x) = true) ↔ ∃ n, List.get as.data n = a
Tactic:
constructor
Proof state after:
case mp
α : Type u
inst✝ : DecidableEq α
a : α
as : Array α
⊢ (∃ x, (∃ n, List.get as.data n = x) ∧ decide (a = x) = true) → ∃ n, List.get as.data n = a

case mpr
α : Type u
inst✝ : DecidableEq α
a : α
as : Array α
⊢ (∃ n, List.get as.data n = a) → ∃ x, (∃ n, List.get as.data n = x) ∧ decide (a = x) = true
Theorem: Array.mem_iff_mem_data
Proof state before:
case mp
α : Type u
inst✝ : DecidableEq α
a : α
as : Array α
⊢ (∃ x, (∃ n, List.get as.data n = x) ∧ decide (a = x) = true) → ∃ n, List.get as.data n = a

case mpr
α : Type u
inst✝ : DecidableEq α
a : α
as : Array α
⊢ (∃ n, List.get as.data n = a) → ∃ x, (∃ n, List.get as.data n = x) ∧ decide (a = x) = true
Tactic:
. intro h
  let ⟨_, ⟨i,hi⟩, h⟩ := h
  cases of_decide_eq_true h
  exact ⟨i,hi⟩
Proof state after:
case mpr
α : Type u
inst✝ : DecidableEq α
a : α
as : Array α
⊢ (∃ n, List.get as.data n = a) → ∃ x, (∃ n, List.get as.data n = x) ∧ decide (a = x) = true
Theorem: Array.mem_iff_mem_data
Proof state before:
case mpr
α : Type u
inst✝ : DecidableEq α
a : α
as : Array α
⊢ (∃ n, List.get as.data n = a) → ∃ x, (∃ n, List.get as.data n = x) ∧ decide (a = x) = true
Tactic:
. intro h; exists a; simp; exact h
Proof state after:
no goals
Theorem: Array.mem_iff_mem_data
Proof state before:
case mp
α : Type u
inst✝ : DecidableEq α
a : α
as : Array α
⊢ (∃ x, (∃ n, List.get as.data n = x) ∧ decide (a = x) = true) → ∃ n, List.get as.data n = a
Tactic:
intro h
Proof state after:
case mp
α : Type u
inst✝ : DecidableEq α
a : α
as : Array α
h : ∃ x, (∃ n, List.get as.data n = x) ∧ decide (a = x) = true
⊢ ∃ n, List.get as.data n = a
Theorem: Array.mem_iff_mem_data
Proof state before:
case mp
α : Type u
inst✝ : DecidableEq α
a : α
as : Array α
h : ∃ x, (∃ n, List.get as.data n = x) ∧ decide (a = x) = true
⊢ ∃ n, List.get as.data n = a
Tactic:
let ⟨_, ⟨i,hi⟩, h⟩ := h
Proof state after:
case mp
α : Type u
inst✝ : DecidableEq α
a : α
as : Array α
h✝ : ∃ x, (∃ n, List.get as.data n = x) ∧ decide (a = x) = true
w✝ : α
i : Fin (List.length as.data)
hi : List.get as.data i = w✝
h : decide (a = w✝) = true
⊢ ∃ n, List.get as.data n = a
Theorem: Array.mem_iff_mem_data
Proof state before:
case mp
α : Type u
inst✝ : DecidableEq α
a : α
as : Array α
h✝ : ∃ x, (∃ n, List.get as.data n = x) ∧ decide (a = x) = true
w✝ : α
i : Fin (List.length as.data)
hi : List.get as.data i = w✝
h : decide (a = w✝) = true
⊢ ∃ n, List.get as.data n = a
Tactic:
cases of_decide_eq_true h
Proof state after:
case mp.refl
α : Type u
inst✝ : DecidableEq α
a : α
as : Array α
h✝ : ∃ x, (∃ n, List.get as.data n = x) ∧ decide (a = x) = true
i : Fin (List.length as.data)
hi : List.get as.data i = a
h : decide (a = a) = true
⊢ ∃ n, List.get as.data n = a
Theorem: Array.mem_iff_mem_data
Proof state before:
case mp.refl
α : Type u
inst✝ : DecidableEq α
a : α
as : Array α
h✝ : ∃ x, (∃ n, List.get as.data n = x) ∧ decide (a = x) = true
i : Fin (List.length as.data)
hi : List.get as.data i = a
h : decide (a = a) = true
⊢ ∃ n, List.get as.data n = a
Tactic:
exact ⟨i,hi⟩
Proof state after:
no goals
Theorem: Array.mem_iff_mem_data
Proof state before:
case mpr
α : Type u
inst✝ : DecidableEq α
a : α
as : Array α
⊢ (∃ n, List.get as.data n = a) → ∃ x, (∃ n, List.get as.data n = x) ∧ decide (a = x) = true
Tactic:
intro h
Proof state after:
case mpr
α : Type u
inst✝ : DecidableEq α
a : α
as : Array α
h : ∃ n, List.get as.data n = a
⊢ ∃ x, (∃ n, List.get as.data n = x) ∧ decide (a = x) = true
Theorem: Array.mem_iff_mem_data
Proof state before:
case mpr
α : Type u
inst✝ : DecidableEq α
a : α
as : Array α
h : ∃ n, List.get as.data n = a
⊢ ∃ x, (∃ n, List.get as.data n = x) ∧ decide (a = x) = true
Tactic:
exists a
Proof state after:
case mpr
α : Type u
inst✝ : DecidableEq α
a : α
as : Array α
h : ∃ n, List.get as.data n = a
⊢ (∃ n, List.get as.data n = a) ∧ decide (a = a) = true
Theorem: Array.mem_iff_mem_data
Proof state before:
case mpr
α : Type u
inst✝ : DecidableEq α
a : α
as : Array α
h : ∃ n, List.get as.data n = a
⊢ (∃ n, List.get as.data n = a) ∧ decide (a = a) = true
Tactic:
simp
Proof state after:
case mpr
α : Type u
inst✝ : DecidableEq α
a : α
as : Array α
h : ∃ n, List.get as.data n = a
⊢ ∃ n, List.get as.data n = a
Theorem: Array.mem_iff_mem_data
Proof state before:
case mpr
α : Type u
inst✝ : DecidableEq α
a : α
as : Array α
h : ∃ n, List.get as.data n = a
⊢ ∃ n, List.get as.data n = a
Tactic:
exact h
Proof state after:
no goals
Theorem: Array.mem_push
Proof state before:
α : Type u
inst✝ : DecidableEq α
a b : α
as : Array α
⊢ a ∈ push as b ↔ a ∈ as ∨ a = b
Tactic:
rw [mem_iff_mem_data, push_data, List.mem_append, mem_iff_mem_data, List.mem_singleton]
Proof state after:
no goals
Theorem: Array.nodup_ofFn
Proof state before:
α : Type u
n : Nat
f : Fin n → α
hf : ∀ (i j : Fin n), f i = f j → i = j
i j : Nat
hi : i < size (ofFn f)
hj : j < size (ofFn f)
h : (ofFn f)[i] = (ofFn f)[j]
⊢ i = j
Tactic:
simp only [Array.getElem_ofFn] at h
Proof state after:
α : Type u
n : Nat
f : Fin n → α
hf : ∀ (i j : Fin n), f i = f j → i = j
i j : Nat
hi : i < size (ofFn f)
hj : j < size (ofFn f)
h : f { val := i, isLt := (_ : i < n) } = f { val := j, isLt := (_ : j < n) }
⊢ i = j
Theorem: Array.nodup_ofFn
Proof state before:
α : Type u
n : Nat
f : Fin n → α
hf : ∀ (i j : Fin n), f i = f j → i = j
i j : Nat
hi : i < size (ofFn f)
hj : j < size (ofFn f)
h : f { val := i, isLt := (_ : i < n) } = f { val := j, isLt := (_ : j < n) }
⊢ i = j
Tactic:
cases hf _ _ h
Proof state after:
case refl
α : Type u
n : Nat
f : Fin n → α
hf : ∀ (i j : Fin n), f i = f j → i = j
i : Nat
hi hj : i < size (ofFn f)
h : f { val := i, isLt := (_ : i < n) } = f { val := i, isLt := (_ : i < n) }
⊢ i = i
Theorem: Array.nodup_ofFn
Proof state before:
case refl
α : Type u
n : Nat
f : Fin n → α
hf : ∀ (i j : Fin n), f i = f j → i = j
i : Nat
hi hj : i < size (ofFn f)
h : f { val := i, isLt := (_ : i < n) } = f { val := i, isLt := (_ : i < n) }
⊢ i = i
Tactic:
rfl
Proof state after:
no goals
Theorem: Array.nodup_push
Proof state before:
α : Type u
inst✝ : DecidableEq α
as : Array α
a : α
⊢ Nodup (push as a) ↔ Nodup as ∧ ¬a ∈ as
Tactic:
show (as.push a).data.Nodup ↔ as.Nodup ∧ a ∉ as
Proof state after:
α : Type u
inst✝ : DecidableEq α
as : Array α
a : α
⊢ List.Nodup (push as a).data ↔ Nodup as ∧ ¬a ∈ as
Theorem: Array.nodup_push
Proof state before:
α : Type u
inst✝ : DecidableEq α
as : Array α
a : α
⊢ List.Nodup (push as a).data ↔ Nodup as ∧ ¬a ∈ as
Tactic:
rewrite [Array.push_data]
Proof state after:
α : Type u
inst✝ : DecidableEq α
as : Array α
a : α
⊢ List.Nodup (as.data ++ [a]) ↔ Nodup as ∧ ¬a ∈ as
Theorem: Array.nodup_push
Proof state before:
α : Type u
inst✝ : DecidableEq α
as : Array α
a : α
⊢ List.Nodup (as.data ++ [a]) ↔ Nodup as ∧ ¬a ∈ as
Tactic:
apply Iff.trans List.pairwise_append
Proof state after:
α : Type u
inst✝ : DecidableEq α
as : Array α
a : α
⊢ (List.Pairwise (fun x x_1 => x ≠ x_1) as.data ∧
      List.Pairwise (fun x x_1 => x ≠ x_1) [a] ∧ ∀ (a_1 : α), a_1 ∈ as.data → ∀ (b : α), b ∈ [a] → a_1 ≠ b) ↔
    Nodup as ∧ ¬a ∈ as
Theorem: Array.nodup_push
Proof state before:
α : Type u
inst✝ : DecidableEq α
as : Array α
a : α
⊢ (List.Pairwise (fun x x_1 => x ≠ x_1) as.data ∧
      List.Pairwise (fun x x_1 => x ≠ x_1) [a] ∧ ∀ (a_1 : α), a_1 ∈ as.data → ∀ (b : α), b ∈ [a] → a_1 ≠ b) ↔
    Nodup as ∧ ¬a ∈ as
Tactic:
show as.Nodup ∧ [a].Nodup ∧ _ ↔ _
Proof state after:
α : Type u
inst✝ : DecidableEq α
as : Array α
a : α
⊢ (Nodup as ∧ List.Nodup [a] ∧ ∀ (a_1 : α), a_1 ∈ as.data → ∀ (b : α), b ∈ [a] → a_1 ≠ b) ↔ Nodup as ∧ ¬a ∈ as
Theorem: Array.nodup_push
Proof state before:
α : Type u
inst✝ : DecidableEq α
as : Array α
a : α
⊢ (Nodup as ∧ List.Nodup [a] ∧ ∀ (a_1 : α), a_1 ∈ as.data → ∀ (b : α), b ∈ [a] → a_1 ≠ b) ↔ Nodup as ∧ ¬a ∈ as
Tactic:
simp only [List.nodup_singleton a, true_and, ← mem_iff_mem_data, List.mem_singleton, forall_eq]
Proof state after:
α : Type u
inst✝ : DecidableEq α
as : Array α
a : α
⊢ (Nodup as ∧ ∀ (a_1 : α), a_1 ∈ as → a_1 ≠ a) ↔ Nodup as ∧ ¬a ∈ as
Theorem: Array.nodup_push
Proof state before:
α : Type u
inst✝ : DecidableEq α
as : Array α
a : α
⊢ (Nodup as ∧ ∀ (a_1 : α), a_1 ∈ as → a_1 ≠ a) ↔ Nodup as ∧ ¬a ∈ as
Tactic:
apply and_congr_right'
Proof state after:
case h
α : Type u
inst✝ : DecidableEq α
as : Array α
a : α
⊢ (∀ (a_1 : α), a_1 ∈ as → a_1 ≠ a) ↔ ¬a ∈ as
Theorem: Array.nodup_push
Proof state before:
case h
α : Type u
inst✝ : DecidableEq α
as : Array α
a : α
⊢ (∀ (a_1 : α), a_1 ∈ as → a_1 ≠ a) ↔ ¬a ∈ as
Tactic:
constructor
Proof state after:
case h.mp
α : Type u
inst✝ : DecidableEq α
as : Array α
a : α
⊢ (∀ (a_1 : α), a_1 ∈ as → a_1 ≠ a) → ¬a ∈ as

case h.mpr
α : Type u
inst✝ : DecidableEq α
as : Array α
a : α
⊢ ¬a ∈ as → ∀ (a_2 : α), a_2 ∈ as → a_2 ≠ a
Theorem: Array.nodup_push
Proof state before:
case h.mp
α : Type u
inst✝ : DecidableEq α
as : Array α
a : α
⊢ (∀ (a_1 : α), a_1 ∈ as → a_1 ≠ a) → ¬a ∈ as

case h.mpr
α : Type u
inst✝ : DecidableEq α
as : Array α
a : α
⊢ ¬a ∈ as → ∀ (a_2 : α), a_2 ∈ as → a_2 ≠ a
Tactic:
. intro h ha; exact h a ha rfl
Proof state after:
case h.mpr
α : Type u
inst✝ : DecidableEq α
as : Array α
a : α
⊢ ¬a ∈ as → ∀ (a_2 : α), a_2 ∈ as → a_2 ≠ a
Theorem: Array.nodup_push
Proof state before:
case h.mpr
α : Type u
inst✝ : DecidableEq α
as : Array α
a : α
⊢ ¬a ∈ as → ∀ (a_2 : α), a_2 ∈ as → a_2 ≠ a
Tactic:
. intro ha b hb heq; cases heq; exact ha hb
Proof state after:
no goals
Theorem: Array.nodup_push
Proof state before:
case h.mp
α : Type u
inst✝ : DecidableEq α
as : Array α
a : α
⊢ (∀ (a_1 : α), a_1 ∈ as → a_1 ≠ a) → ¬a ∈ as
Tactic:
intro h ha
Proof state after:
case h.mp
α : Type u
inst✝ : DecidableEq α
as : Array α
a : α
h : ∀ (a_1 : α), a_1 ∈ as → a_1 ≠ a
ha : a ∈ as
⊢ False
Theorem: Array.nodup_push
Proof state before:
case h.mp
α : Type u
inst✝ : DecidableEq α
as : Array α
a : α
h : ∀ (a_1 : α), a_1 ∈ as → a_1 ≠ a
ha : a ∈ as
⊢ False
Tactic:
exact h a ha rfl
Proof state after:
no goals
Theorem: Array.nodup_push
Proof state before:
case h.mpr
α : Type u
inst✝ : DecidableEq α
as : Array α
a : α
⊢ ¬a ∈ as → ∀ (a_2 : α), a_2 ∈ as → a_2 ≠ a
Tactic:
intro ha b hb heq
Proof state after:
case h.mpr
α : Type u
inst✝ : DecidableEq α
as : Array α
a : α
ha : ¬a ∈ as
b : α
hb : b ∈ as
heq : b = a
⊢ False
Theorem: Array.nodup_push
Proof state before:
case h.mpr
α : Type u
inst✝ : DecidableEq α
as : Array α
a : α
ha : ¬a ∈ as
b : α
hb : b ∈ as
heq : b = a
⊢ False
Tactic:
cases heq
Proof state after:
case h.mpr.refl
α : Type u
inst✝ : DecidableEq α
as : Array α
a : α
ha : ¬a ∈ as
hb : a ∈ as
⊢ False
Theorem: Array.nodup_push
Proof state before:
case h.mpr.refl
α : Type u
inst✝ : DecidableEq α
as : Array α
a : α
ha : ¬a ∈ as
hb : a ∈ as
⊢ False
Tactic:
exact ha hb
Proof state after:
no goals
Theorem: Array.nodup_append
Proof state before:
α : Type u
as bs : Array α
has : Nodup as
hbs : Nodup bs
hdisj : ∀ (i j : Nat) (hi : i < size as) (hj : j < size bs), as[i] ≠ bs[j]
i j : Nat
hi : i < size (as ++ bs)
hj : j < size (as ++ bs)
⊢ (as ++ bs)[i] = (as ++ bs)[j] → i = j
Tactic:
if hi' : i < as.size then
  rewrite [getElem_append_left as bs hi']
  if hj' : j < as.size then
    rewrite [getElem_append_left as bs hj']
    exact has.get_inj i j hi' hj'
  else
    rewrite [getElem_append_right as bs (Nat.le_of_not_lt hj')]
    intro hij; exfalso
    exact hdisj _ _ _ _ hij
else
  have hi'' : i ≥ as.size := Nat.le_of_not_lt hi'
  have : i - as.size < bs.size :=
    Nat.sub_lt_left_of_lt_add hi'' (size_append _ _ ▸ hi)
  rewrite [getElem_append_right as bs (Nat.le_of_not_lt hi')]
  if hj' : j < as.size then
    rewrite [getElem_append_left as bs hj']
    intro hij; exfalso
    exact hdisj _ _ _ _ hij.symm
  else
    have hj'' : j ≥ as.size := Nat.le_of_not_lt hj'
    have : j - as.size < bs.size :=
      Nat.sub_lt_left_of_lt_add hj'' (size_append _ _ ▸ hj)
    rewrite [getElem_append_right as bs (Nat.le_of_not_lt hj')]
    intro h
    have := hbs.get_inj (i-as.size) (j-as.size) ‹_› ‹_› h
    conv at this =>
      rewrite [Nat.sub_eq_iff_eq_add hi'']
      rewrite [Nat.sub_add_cancel hj'']
    exact this
Proof state after:
no goals
Theorem: Array.nodup_append
Proof state before:
α : Type u
as bs : Array α
has : Nodup as
hbs : Nodup bs
hdisj : ∀ (i j : Nat) (hi : i < size as) (hj : j < size bs), as[i] ≠ bs[j]
i j : Nat
hi : i < size (as ++ bs)
hj : j < size (as ++ bs)
hi' : i < size as
⊢ (as ++ bs)[i] = (as ++ bs)[j] → i = j
Tactic:
rewrite [getElem_append_left as bs hi']
Proof state after:
α : Type u
as bs : Array α
has : Nodup as
hbs : Nodup bs
hdisj : ∀ (i j : Nat) (hi : i < size as) (hj : j < size bs), as[i] ≠ bs[j]
i j : Nat
hi : i < size (as ++ bs)
hj : j < size (as ++ bs)
hi' : i < size as
⊢ as[i] = (as ++ bs)[j] → i = j
Theorem: Array.nodup_append
Proof state before:
α : Type u
as bs : Array α
has : Nodup as
hbs : Nodup bs
hdisj : ∀ (i j : Nat) (hi : i < size as) (hj : j < size bs), as[i] ≠ bs[j]
i j : Nat
hi : i < size (as ++ bs)
hj : j < size (as ++ bs)
hi' : i < size as
⊢ as[i] = (as ++ bs)[j] → i = j
Tactic:
if hj' : j < as.size then
  rewrite [getElem_append_left as bs hj']
  exact has.get_inj i j hi' hj'
else
  rewrite [getElem_append_right as bs (Nat.le_of_not_lt hj')]
  intro hij; exfalso
  exact hdisj _ _ _ _ hij
Proof state after:
no goals
Theorem: Array.nodup_append
Proof state before:
α : Type u
as bs : Array α
has : Nodup as
hbs : Nodup bs
hdisj : ∀ (i j : Nat) (hi : i < size as) (hj : j < size bs), as[i] ≠ bs[j]
i j : Nat
hi : i < size (as ++ bs)
hj : j < size (as ++ bs)
hi' : i < size as
hj' : j < size as
⊢ as[i] = (as ++ bs)[j] → i = j
Tactic:
rewrite [getElem_append_left as bs hj']
Proof state after:
α : Type u
as bs : Array α
has : Nodup as
hbs : Nodup bs
hdisj : ∀ (i j : Nat) (hi : i < size as) (hj : j < size bs), as[i] ≠ bs[j]
i j : Nat
hi : i < size (as ++ bs)
hj : j < size (as ++ bs)
hi' : i < size as
hj' : j < size as
⊢ as[i] = as[j] → i = j
Theorem: Array.nodup_append
Proof state before:
α : Type u
as bs : Array α
has : Nodup as
hbs : Nodup bs
hdisj : ∀ (i j : Nat) (hi : i < size as) (hj : j < size bs), as[i] ≠ bs[j]
i j : Nat
hi : i < size (as ++ bs)
hj : j < size (as ++ bs)
hi' : i < size as
hj' : j < size as
⊢ as[i] = as[j] → i = j
Tactic:
exact has.get_inj i j hi' hj'
Proof state after:
no goals
Theorem: Array.nodup_append
Proof state before:
α : Type u
as bs : Array α
has : Nodup as
hbs : Nodup bs
hdisj : ∀ (i j : Nat) (hi : i < size as) (hj : j < size bs), as[i] ≠ bs[j]
i j : Nat
hi : i < size (as ++ bs)
hj : j < size (as ++ bs)
hi' : i < size as
hj' : ¬j < size as
⊢ as[i] = (as ++ bs)[j] → i = j
Tactic:
rewrite [getElem_append_right as bs (Nat.le_of_not_lt hj')]
Proof state after:
α : Type u
as bs : Array α
has : Nodup as
hbs : Nodup bs
hdisj : ∀ (i j : Nat) (hi : i < size as) (hj : j < size bs), as[i] ≠ bs[j]
i j : Nat
hi : i < size (as ++ bs)
hj : j < size (as ++ bs)
hi' : i < size as
hj' : ¬j < size as
⊢ as[i] = bs[j - size as] → i = j
Theorem: Array.nodup_append
Proof state before:
α : Type u
as bs : Array α
has : Nodup as
hbs : Nodup bs
hdisj : ∀ (i j : Nat) (hi : i < size as) (hj : j < size bs), as[i] ≠ bs[j]
i j : Nat
hi : i < size (as ++ bs)
hj : j < size (as ++ bs)
hi' : i < size as
hj' : ¬j < size as
⊢ as[i] = bs[j - size as] → i = j
Tactic:
intro hij
Proof state after:
α : Type u
as bs : Array α
has : Nodup as
hbs : Nodup bs
hdisj : ∀ (i j : Nat) (hi : i < size as) (hj : j < size bs), as[i] ≠ bs[j]
i j : Nat
hi : i < size (as ++ bs)
hj : j < size (as ++ bs)
hi' : i < size as
hj' : ¬j < size as
hij : as[i] = bs[j - size as]
⊢ i = j