internlm/Lean-Github huggingface dataset:
Theorem: Array.push_pop_eq
Proof state before:
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
this✝ : 0 < a.size
i : Nat
h hi₂✝ : i < a.size
h' : a.size - 1 ≤ i
this : i ≤ a.size - 1
⊢ a.back' hemp = a[i]
Tactic:
have : i = a.size - 1 := Nat.le_antisymm this h'
Proof state after:
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
this✝¹ : 0 < a.size
i : Nat
h hi₂✝ : i < a.size
h' : a.size - 1 ≤ i
this✝ : i ≤ a.size - 1
this : i = a.size - 1
⊢ a.back' hemp = a[i]
Theorem: Array.push_pop_eq
Proof state before:
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
this✝¹ : 0 < a.size
i : Nat
h hi₂✝ : i < a.size
h' : a.size - 1 ≤ i
this✝ : i ≤ a.size - 1
this : i = a.size - 1
⊢ a.back' hemp = a[i]
Tactic:
simp [back', this]
Proof state after:
no goals
Theorem: Array.mem_pop
Proof state before:
α : Type u_1
a : Array α
x : α
hemp : ¬a.isEmpty = true
mem : x ∈ a
neq : x ≠ a.back' hemp
⊢ x ∈ a.pop
Tactic:
rw [←Array.push_pop_eq a hemp] at mem
Proof state after:
α : Type u_1
a : Array α
x : α
hemp : ¬a.isEmpty = true
mem : x ∈ a.pop.push (a.back' hemp)
neq : x ≠ a.back' hemp
⊢ x ∈ a.pop
Theorem: Array.mem_pop
Proof state before:
α : Type u_1
a : Array α
x : α
hemp : ¬a.isEmpty = true
mem : x ∈ a.pop.push (a.back' hemp)
neq : x ≠ a.back' hemp
⊢ x ∈ a.pop
Tactic:
cases (Array.mem_push _ _ _).mp mem with
| inl mem => exact mem
| inr eq => exact absurd eq neq
Proof state after:
no goals
Theorem: Array.mem_pop
Proof state before:
case inl
α : Type u_1
a : Array α
x : α
hemp : ¬a.isEmpty = true
mem✝ : x ∈ a.pop.push (a.back' hemp)
neq : x ≠ a.back' hemp
mem : x ∈ a.pop
⊢ x ∈ a.pop
Tactic:
exact mem
Proof state after:
no goals
Theorem: Array.mem_pop
Proof state before:
case inr
α : Type u_1
a : Array α
x : α
hemp : ¬a.isEmpty = true
mem : x ∈ a.pop.push (a.back' hemp)
neq : x ≠ a.back' hemp
eq : x = a.back' hemp
⊢ x ∈ a.pop
Tactic:
exact absurd eq neq
Proof state after:
no goals
Theorem: Array.mem_pop_or_eq_of_mem
Proof state before:
α : Type u_1
a : Array α
x : α
hemp : ¬a.isEmpty = true
mem : x ∈ a
⊢ x ∈ a.pop ∨ x = a.back' hemp
Tactic:
rw [←Array.push_pop_eq a hemp] at mem
Proof state after:
α : Type u_1
a : Array α
x : α
hemp : ¬a.isEmpty = true
mem : x ∈ a.pop.push (a.back' hemp)
⊢ x ∈ a.pop ∨ x = a.back' hemp
Theorem: Array.mem_pop_or_eq_of_mem
Proof state before:
α : Type u_1
a : Array α
x : α
hemp : ¬a.isEmpty = true
mem : x ∈ a.pop.push (a.back' hemp)
⊢ x ∈ a.pop ∨ x = a.back' hemp
Tactic:
exact (Array.mem_push _ _ _).mp mem
Proof state after:
no goals
Theorem: Array.mem_of_mem_pop
Proof state before:
α : Type u_1
a : Array α
x : α
mem : x ∈ a.pop
⊢ x ∈ a
Tactic:
cases decEq a.isEmpty true with
| isTrue hemp =>
  have := (Array.isEmpty_iff).mp hemp
  subst this
  simp at mem
| isFalse hemp =>
  rw [←Array.push_pop_eq a hemp]
  apply (Array.mem_push _ _ _).mpr
  exact Or.inl mem
Proof state after:
no goals
Theorem: Array.mem_of_mem_pop
Proof state before:
case isTrue
α : Type u_1
a : Array α
x : α
mem : x ∈ a.pop
hemp : a.isEmpty = true
⊢ x ∈ a
Tactic:
have := (Array.isEmpty_iff).mp hemp
Proof state after:
case isTrue
α : Type u_1
a : Array α
x : α
mem : x ∈ a.pop
hemp : a.isEmpty = true
this : a = #[]
⊢ x ∈ a
Theorem: Array.mem_of_mem_pop
Proof state before:
case isTrue
α : Type u_1
a : Array α
x : α
mem : x ∈ a.pop
hemp : a.isEmpty = true
this : a = #[]
⊢ x ∈ a
Tactic:
subst this
Proof state after:
case isTrue
α : Type u_1
x : α
mem : x ∈ #[].pop
hemp : #[].isEmpty = true
⊢ x ∈ #[]
Theorem: Array.mem_of_mem_pop
Proof state before:
case isTrue
α : Type u_1
x : α
mem : x ∈ #[].pop
hemp : #[].isEmpty = true
⊢ x ∈ #[]
Tactic:
simp at mem
Proof state after:
no goals
Theorem: Array.mem_of_mem_pop
Proof state before:
case isFalse
α : Type u_1
a : Array α
x : α
mem : x ∈ a.pop
hemp : ¬a.isEmpty = true
⊢ x ∈ a
Tactic:
rw [←Array.push_pop_eq a hemp]
Proof state after:
case isFalse
α : Type u_1
a : Array α
x : α
mem : x ∈ a.pop
hemp : ¬a.isEmpty = true
⊢ x ∈ a.pop.push (a.back' hemp)
Theorem: Array.mem_of_mem_pop
Proof state before:
case isFalse
α : Type u_1
a : Array α
x : α
mem : x ∈ a.pop
hemp : ¬a.isEmpty = true
⊢ x ∈ a.pop.push (a.back' hemp)
Tactic:
apply (Array.mem_push _ _ _).mpr
Proof state after:
case isFalse
α : Type u_1
a : Array α
x : α
mem : x ∈ a.pop
hemp : ¬a.isEmpty = true
⊢ x ∈ a.pop ∨ x = a.back' hemp
Theorem: Array.mem_of_mem_pop
Proof state before:
case isFalse
α : Type u_1
a : Array α
x : α
mem : x ∈ a.pop
hemp : ¬a.isEmpty = true
⊢ x ∈ a.pop ∨ x = a.back' hemp
Tactic:
exact Or.inl mem
Proof state after:
no goals
Theorem: Regex.Data.SparseSet.mem_insert_of_mem
Proof state before:
n : Nat
s : SparseSet n
i j : Fin n
⊢ i ∈ s → i ∈ s.insert j
Tactic:
intro h
Proof state after:
n : Nat
s : SparseSet n
i j : Fin n
h : i ∈ s
⊢ i ∈ s.insert j
Theorem: Regex.Data.SparseSet.mem_insert_of_mem
Proof state before:
n : Nat
s : SparseSet n
i j : Fin n
h : i ∈ s
⊢ i ∈ s.insert j
Tactic:
unfold SparseSet.insert
Proof state after:
n : Nat
s : SparseSet n
i j : Fin n
h : i ∈ s
⊢ i ∈
    if mem : j ∈ s then s
    else
      match s, mem with
      | { count := count, dense := dense, sparse := sparse, sparse_dense := sparse_dense, le_count := le_count }, mem =>
        let_fun isLt := ⋯;
        let dense' := dense.set count isLt j;
        let sparse' := sparse.set ↑j ⋯ ⟨count, isLt⟩;
        let_fun sparse_dense' := ⋯;
        { count := count + 1, dense := dense', sparse := sparse', sparse_dense := sparse_dense', le_count := isLt }
Theorem: Regex.Data.SparseSet.mem_insert_of_mem
Proof state before:
n : Nat
s : SparseSet n
i j : Fin n
h : i ∈ s
⊢ i ∈
    if mem : j ∈ s then s
    else
      match s, mem with
      | { count := count, dense := dense, sparse := sparse, sparse_dense := sparse_dense, le_count := le_count }, mem =>
        let_fun isLt := ⋯;
        let dense' := dense.set count isLt j;
        let sparse' := sparse.set ↑j ⋯ ⟨count, isLt⟩;
        let_fun sparse_dense' := ⋯;
        { count := count + 1, dense := dense', sparse := sparse', sparse_dense := sparse_dense', le_count := isLt }
Tactic:
split
Proof state after:
case inl
n : Nat
s : SparseSet n
i j : Fin n
h : i ∈ s
h✝ : j ∈ s
⊢ i ∈ s

case inr
n : Nat
s : SparseSet n
i j : Fin n
h : i ∈ s
h✝ : ¬j ∈ s
⊢ i ∈
    match s, h✝ with
    | { count := count, dense := dense, sparse := sparse, sparse_dense := sparse_dense, le_count := le_count }, mem =>
      let_fun isLt := ⋯;
      let dense' := dense.set count isLt j;
      let sparse' := sparse.set ↑j ⋯ ⟨count, isLt⟩;
      let_fun sparse_dense' := ⋯;
      { count := count + 1, dense := dense', sparse := sparse', sparse_dense := sparse_dense', le_count := isLt }
Theorem: Regex.Data.SparseSet.mem_insert_of_mem
Proof state before:
case inl
n : Nat
s : SparseSet n
i j : Fin n
h : i ∈ s
h✝ : j ∈ s
⊢ i ∈ s

case inr
n : Nat
s : SparseSet n
i j : Fin n
h : i ∈ s
h✝ : ¬j ∈ s
⊢ i ∈
    match s, h✝ with
    | { count := count, dense := dense, sparse := sparse, sparse_dense := sparse_dense, le_count := le_count }, mem =>
      let_fun isLt := ⋯;
      let dense' := dense.set count isLt j;
      let sparse' := sparse.set ↑j ⋯ ⟨count, isLt⟩;
      let_fun sparse_dense' := ⋯;
      { count := count + 1, dense := dense', sparse := sparse', sparse_dense := sparse_dense', le_count := isLt }
Tactic:
next => exact h
Proof state after:
case inr
n : Nat
s : SparseSet n
i j : Fin n
h : i ∈ s
h✝ : ¬j ∈ s
⊢ i ∈
    match s, h✝ with
    | { count := count, dense := dense, sparse := sparse, sparse_dense := sparse_dense, le_count := le_count }, mem =>
      let_fun isLt := ⋯;
      let dense' := dense.set count isLt j;
      let sparse' := sparse.set ↑j ⋯ ⟨count, isLt⟩;
      let_fun sparse_dense' := ⋯;
      { count := count + 1, dense := dense', sparse := sparse', sparse_dense := sparse_dense', le_count := isLt }
Theorem: Regex.Data.SparseSet.mem_insert_of_mem
Proof state before:
case inr
n : Nat
s : SparseSet n
i j : Fin n
h : i ∈ s
h✝ : ¬j ∈ s
⊢ i ∈
    match s, h✝ with
    | { count := count, dense := dense, sparse := sparse, sparse_dense := sparse_dense, le_count := le_count }, mem =>
      let_fun isLt := ⋯;
      let dense' := dense.set count isLt j;
      let sparse' := sparse.set ↑j ⋯ ⟨count, isLt⟩;
      let_fun sparse_dense' := ⋯;
      { count := count + 1, dense := dense', sparse := sparse', sparse_dense := sparse_dense', le_count := isLt }
Tactic:
next hmem =>
  simp [mem, Vec.get_set]
  if heq : j.val = i.val then
    simp [heq]
    exact Fin.eq_of_val_eq heq
  else
    simp [mem] at h
    simp [heq]
    have : s.count ≠ s.sparse[i.val].val := Nat.ne_of_gt h.left
    simp [this, h]
    exact Nat.lt_trans h.left (Nat.lt_succ_self _)
Proof state after:
no goals
Theorem: Regex.Data.SparseSet.mem_insert_of_mem
Proof state before:
n : Nat
s : SparseSet n
i j : Fin n
h : i ∈ s
h✝ : j ∈ s
⊢ i ∈ s
Tactic:
exact h
Proof state after:
no goals
Theorem: Regex.Data.SparseSet.mem_insert_of_mem
Proof state before:
n : Nat
s : SparseSet n
i j : Fin n
h : i ∈ s
hmem : ¬j ∈ s
⊢ i ∈
    match s, hmem with
    | { count := count, dense := dense, sparse := sparse, sparse_dense := sparse_dense, le_count := le_count }, mem =>
      let_fun isLt := ⋯;
      let dense' := dense.set count isLt j;
      let sparse' := sparse.set ↑j ⋯ ⟨count, isLt⟩;
      let_fun sparse_dense' := ⋯;
      { count := count + 1, dense := dense', sparse := sparse', sparse_dense := sparse_dense', le_count := isLt }
Tactic:
simp [mem, Vec.get_set]
Proof state after:
n : Nat
s : SparseSet n
i j : Fin n
h : i ∈ s
hmem : ¬j ∈ s
⊢ ↑(if ↑j = ↑i then ⟨s.count, ⋯⟩ else s.sparse[↑i]) < s.count + 1 ∧
    (if s.count = ↑(if ↑j = ↑i then ⟨s.count, ⋯⟩ else s.sparse[↑i]) then j
      else s.dense[↑(if ↑j = ↑i then ⟨s.count, ⋯⟩ else s.sparse[↑i])]) =
      i
Theorem: Regex.Data.SparseSet.mem_insert_of_mem
Proof state before:
n : Nat
s : SparseSet n
i j : Fin n
h : i ∈ s
hmem : ¬j ∈ s
⊢ ↑(if ↑j = ↑i then ⟨s.count, ⋯⟩ else s.sparse[↑i]) < s.count + 1 ∧
    (if s.count = ↑(if ↑j = ↑i then ⟨s.count, ⋯⟩ else s.sparse[↑i]) then j
      else s.dense[↑(if ↑j = ↑i then ⟨s.count, ⋯⟩ else s.sparse[↑i])]) =
      i
Tactic:
if heq : j.val = i.val then
  simp [heq]
  exact Fin.eq_of_val_eq heq
else
  simp [mem] at h
  simp [heq]
  have : s.count ≠ s.sparse[i.val].val := Nat.ne_of_gt h.left
  simp [this, h]
  exact Nat.lt_trans h.left (Nat.lt_succ_self _)
Proof state after:
no goals
Theorem: Regex.Data.SparseSet.mem_insert_of_mem
Proof state before:
n : Nat
s : SparseSet n
i j : Fin n
h : i ∈ s
hmem : ¬j ∈ s
heq : ↑j = ↑i
⊢ ↑(if ↑j = ↑i then ⟨s.count, ⋯⟩ else s.sparse[↑i]) < s.count + 1 ∧
    (if s.count = ↑(if ↑j = ↑i then ⟨s.count, ⋯⟩ else s.sparse[↑i]) then j
      else s.dense[↑(if ↑j = ↑i then ⟨s.count, ⋯⟩ else s.sparse[↑i])]) =
      i
Tactic:
simp [heq]
Proof state after:
n : Nat
s : SparseSet n
i j : Fin n
h : i ∈ s
hmem : ¬j ∈ s
heq : ↑j = ↑i
⊢ j = i
Theorem: Regex.Data.SparseSet.mem_insert_of_mem
Proof state before:
n : Nat
s : SparseSet n
i j : Fin n
h : i ∈ s
hmem : ¬j ∈ s
heq : ↑j = ↑i
⊢ j = i
Tactic:
exact Fin.eq_of_val_eq heq
Proof state after:
no goals
Theorem: Regex.Data.SparseSet.mem_insert_of_mem
Proof state before:
n : Nat
s : SparseSet n
i j : Fin n
h : i ∈ s
hmem : ¬j ∈ s
heq : ¬↑j = ↑i
⊢ ↑(if ↑j = ↑i then ⟨s.count, ⋯⟩ else s.sparse[↑i]) < s.count + 1 ∧
    (if s.count = ↑(if ↑j = ↑i then ⟨s.count, ⋯⟩ else s.sparse[↑i]) then j
      else s.dense[↑(if ↑j = ↑i then ⟨s.count, ⋯⟩ else s.sparse[↑i])]) =
      i
Tactic:
simp [mem] at h
Proof state after:
n : Nat
s : SparseSet n
i j : Fin n
hmem : ¬j ∈ s
heq : ¬↑j = ↑i
h : ↑s.sparse[↑i] < s.count ∧ s.dense[↑s.sparse[↑i]] = i
⊢ ↑(if ↑j = ↑i then ⟨s.count, ⋯⟩ else s.sparse[↑i]) < s.count + 1 ∧
    (if s.count = ↑(if ↑j = ↑i then ⟨s.count, ⋯⟩ else s.sparse[↑i]) then j
      else s.dense[↑(if ↑j = ↑i then ⟨s.count, ⋯⟩ else s.sparse[↑i])]) =
      i
Theorem: Regex.Data.SparseSet.mem_insert_of_mem
Proof state before:
n : Nat
s : SparseSet n
i j : Fin n
hmem : ¬j ∈ s
heq : ¬↑j = ↑i
h : ↑s.sparse[↑i] < s.count ∧ s.dense[↑s.sparse[↑i]] = i
⊢ ↑(if ↑j = ↑i then ⟨s.count, ⋯⟩ else s.sparse[↑i]) < s.count + 1 ∧
    (if s.count = ↑(if ↑j = ↑i then ⟨s.count, ⋯⟩ else s.sparse[↑i]) then j
      else s.dense[↑(if ↑j = ↑i then ⟨s.count, ⋯⟩ else s.sparse[↑i])]) =
      i
Tactic:
simp [heq]
Proof state after:
n : Nat
s : SparseSet n
i j : Fin n
hmem : ¬j ∈ s
heq : ¬↑j = ↑i
h : ↑s.sparse[↑i] < s.count ∧ s.dense[↑s.sparse[↑i]] = i
⊢ ↑s.sparse[↑i] < s.count + 1 ∧ (if s.count = ↑s.sparse[↑i] then j else s.dense[↑s.sparse[↑i]]) = i
Theorem: Regex.Data.SparseSet.mem_insert_of_mem
Proof state before:
n : Nat
s : SparseSet n
i j : Fin n
hmem : ¬j ∈ s
heq : ¬↑j = ↑i
h : ↑s.sparse[↑i] < s.count ∧ s.dense[↑s.sparse[↑i]] = i
⊢ ↑s.sparse[↑i] < s.count + 1 ∧ (if s.count = ↑s.sparse[↑i] then j else s.dense[↑s.sparse[↑i]]) = i
Tactic:
have : s.count ≠ s.sparse[i.val].val := Nat.ne_of_gt h.left
Proof state after:
n : Nat
s : SparseSet n
i j : Fin n
hmem : ¬j ∈ s
heq : ¬↑j = ↑i
h : ↑s.sparse[↑i] < s.count ∧ s.dense[↑s.sparse[↑i]] = i
this : s.count ≠ ↑s.sparse[↑i]
⊢ ↑s.sparse[↑i] < s.count + 1 ∧ (if s.count = ↑s.sparse[↑i] then j else s.dense[↑s.sparse[↑i]]) = i
Theorem: Regex.Data.SparseSet.mem_insert_of_mem
Proof state before:
n : Nat
s : SparseSet n
i j : Fin n
hmem : ¬j ∈ s
heq : ¬↑j = ↑i
h : ↑s.sparse[↑i] < s.count ∧ s.dense[↑s.sparse[↑i]] = i
this : s.count ≠ ↑s.sparse[↑i]
⊢ ↑s.sparse[↑i] < s.count + 1 ∧ (if s.count = ↑s.sparse[↑i] then j else s.dense[↑s.sparse[↑i]]) = i
Tactic:
simp [this, h]
Proof state after:
n : Nat
s : SparseSet n
i j : Fin n
hmem : ¬j ∈ s
heq : ¬↑j = ↑i
h : ↑s.sparse[↑i] < s.count ∧ s.dense[↑s.sparse[↑i]] = i
this : s.count ≠ ↑s.sparse[↑i]
⊢ ↑s.sparse[↑i] < s.count + 1
Theorem: Regex.Data.SparseSet.mem_insert_of_mem
Proof state before:
n : Nat
s : SparseSet n
i j : Fin n
hmem : ¬j ∈ s
heq : ¬↑j = ↑i
h : ↑s.sparse[↑i] < s.count ∧ s.dense[↑s.sparse[↑i]] = i
this : s.count ≠ ↑s.sparse[↑i]
⊢ ↑s.sparse[↑i] < s.count + 1
Tactic:
exact Nat.lt_trans h.left (Nat.lt_succ_self _)
Proof state after:
no goals
Theorem: Regex.Data.SparseSet.eq_or_mem_of_mem_insert
Proof state before:
n : Nat
s : SparseSet n
i j : Fin n
⊢ i ∈ s.insert j → i = j ∨ i ∈ s
Tactic:
intro h
Proof state after:
n : Nat
s : SparseSet n
i j : Fin n
h : i ∈ s.insert j
⊢ i = j ∨ i ∈ s
Theorem: Regex.Data.SparseSet.eq_or_mem_of_mem_insert
Proof state before:
n : Nat
s : SparseSet n
i j : Fin n
h : i ∈ s.insert j
⊢ i = j ∨ i ∈ s
Tactic:
if heq : i = j then
  exact Or.inl heq
else
  suffices i ∈ s from Or.inr this
  unfold SparseSet.insert at h
  split at h
  next => exact h
  next hmem =>
    have ne : j.val ≠ i.val := Ne.symm (Fin.val_ne_of_ne heq)
    simp [mem, Vec.get_set, ne] at h
    split at h
    case inl heq' => simp [h] at heq
    case inr heq' =>
      have : s.sparse[i.val] < s.count := by
        have : s.sparse[i.val] ≤ s.count := Nat.le_of_lt_succ h.left
        exact Nat.lt_of_le_of_ne this (Ne.symm heq')
      simp [mem, this, h]
Proof state after:
no goals
Theorem: Regex.Data.SparseSet.eq_or_mem_of_mem_insert
Proof state before:
n : Nat
s : SparseSet n
i j : Fin n
h : i ∈ s.insert j
heq : i = j
⊢ i = j ∨ i ∈ s
Tactic:
exact Or.inl heq
Proof state after:
no goals
Theorem: Regex.Data.SparseSet.eq_or_mem_of_mem_insert
Proof state before:
n : Nat
s : SparseSet n
i j : Fin n
h : i ∈ s.insert j
heq : ¬i = j
⊢ i = j ∨ i ∈ s
Tactic:
suffices i ∈ s from Or.inr this
Proof state after:
n : Nat
s : SparseSet n
i j : Fin n
h : i ∈ s.insert j
heq : ¬i = j
⊢ i ∈ s
Theorem: Regex.Data.SparseSet.eq_or_mem_of_mem_insert
Proof state before:
n : Nat
s : SparseSet n
i j : Fin n
h : i ∈ s.insert j
heq : ¬i = j
⊢ i ∈ s
Tactic:
unfold SparseSet.insert at h
Proof state after:
n : Nat
s : SparseSet n
i j : Fin n
h :
  i ∈
    if mem : j ∈ s then s
    else
      match s, mem with
      | { count := count, dense := dense, sparse := sparse, sparse_dense := sparse_dense, le_count := le_count }, mem =>
        let_fun isLt := ⋯;
        let dense' := dense.set count isLt j;
        let sparse' := sparse.set ↑j ⋯ ⟨count, isLt⟩;
        let_fun sparse_dense' := ⋯;
        { count := count + 1, dense := dense', sparse := sparse', sparse_dense := sparse_dense', le_count := isLt }
heq : ¬i = j
⊢ i ∈ s
Theorem: Regex.Data.SparseSet.eq_or_mem_of_mem_insert
Proof state before:
n : Nat
s : SparseSet n
i j : Fin n
h :
  i ∈
    if mem : j ∈ s then s
    else
      match s, mem with
      | { count := count, dense := dense, sparse := sparse, sparse_dense := sparse_dense, le_count := le_count }, mem =>
        let_fun isLt := ⋯;
        let dense' := dense.set count isLt j;
        let sparse' := sparse.set ↑j ⋯ ⟨count, isLt⟩;
        let_fun sparse_dense' := ⋯;
        { count := count + 1, dense := dense', sparse := sparse', sparse_dense := sparse_dense', le_count := isLt }
heq : ¬i = j
⊢ i ∈ s
Tactic:
split at h
Proof state after:
case inl
n : Nat
s : SparseSet n
i j : Fin n
heq : ¬i = j
h✝ : j ∈ s
h : i ∈ s
⊢ i ∈ s

case inr
n : Nat
s : SparseSet n
i j : Fin n
heq : ¬i = j
h✝ : ¬j ∈ s
h :
  i ∈
    match s, h✝ with
    | { count := count, dense := dense, sparse := sparse, sparse_dense := sparse_dense, le_count := le_count }, mem =>
      let_fun isLt := ⋯;
      let dense' := dense.set count isLt j;
      let sparse' := sparse.set ↑j ⋯ ⟨count, isLt⟩;
      let_fun sparse_dense' := ⋯;
      { count := count + 1, dense := dense', sparse := sparse', sparse_dense := sparse_dense', le_count := isLt }
⊢ i ∈ s
Theorem: Regex.Data.SparseSet.eq_or_mem_of_mem_insert
Proof state before:
case inl
n : Nat
s : SparseSet n
i j : Fin n
heq : ¬i = j
h✝ : j ∈ s
h : i ∈ s
⊢ i ∈ s

case inr
n : Nat
s : SparseSet n
i j : Fin n
heq : ¬i = j
h✝ : ¬j ∈ s
h :
  i ∈
    match s, h✝ with
    | { count := count, dense := dense, sparse := sparse, sparse_dense := sparse_dense, le_count := le_count }, mem =>
      let_fun isLt := ⋯;
      let dense' := dense.set count isLt j;
      let sparse' := sparse.set ↑j ⋯ ⟨count, isLt⟩;
      let_fun sparse_dense' := ⋯;
      { count := count + 1, dense := dense', sparse := sparse', sparse_dense := sparse_dense', le_count := isLt }
⊢ i ∈ s
Tactic:
next => exact h
Proof state after:
case inr
n : Nat
s : SparseSet n
i j : Fin n
heq : ¬i = j
h✝ : ¬j ∈ s
h :
  i ∈
    match s, h✝ with
    | { count := count, dense := dense, sparse := sparse, sparse_dense := sparse_dense, le_count := le_count }, mem =>
      let_fun isLt := ⋯;
      let dense' := dense.set count isLt j;
      let sparse' := sparse.set ↑j ⋯ ⟨count, isLt⟩;
      let_fun sparse_dense' := ⋯;
      { count := count + 1, dense := dense', sparse := sparse', sparse_dense := sparse_dense', le_count := isLt }
⊢ i ∈ s
Theorem: Regex.Data.SparseSet.eq_or_mem_of_mem_insert
Proof state before:
case inr
n : Nat
s : SparseSet n
i j : Fin n
heq : ¬i = j
h✝ : ¬j ∈ s
h :
  i ∈
    match s, h✝ with
    | { count := count, dense := dense, sparse := sparse, sparse_dense := sparse_dense, le_count := le_count }, mem =>
      let_fun isLt := ⋯;
      let dense' := dense.set count isLt j;
      let sparse' := sparse.set ↑j ⋯ ⟨count, isLt⟩;
      let_fun sparse_dense' := ⋯;
      { count := count + 1, dense := dense', sparse := sparse', sparse_dense := sparse_dense', le_count := isLt }
⊢ i ∈ s
Tactic:
next hmem =>
  have ne : j.val ≠ i.val := Ne.symm (Fin.val_ne_of_ne heq)
  simp [mem, Vec.get_set, ne] at h
  split at h
  case inl heq' => simp [h] at heq
  case inr heq' =>
    have : s.sparse[i.val] < s.count := by
      have : s.sparse[i.val] ≤ s.count := Nat.le_of_lt_succ h.left
      exact Nat.lt_of_le_of_ne this (Ne.symm heq')
    simp [mem, this, h]
Proof state after:
no goals
Theorem: Regex.Data.SparseSet.eq_or_mem_of_mem_insert
Proof state before:
n : Nat
s : SparseSet n
i j : Fin n
heq : ¬i = j
h✝ : j ∈ s
h : i ∈ s
⊢ i ∈ s
Tactic:
exact h
Proof state after:
no goals
Theorem: Regex.Data.SparseSet.eq_or_mem_of_mem_insert
Proof state before:
n : Nat
s : SparseSet n
i j : Fin n
heq : ¬i = j
hmem : ¬j ∈ s
h :
  i ∈
    match s, hmem with
    | { count := count, dense := dense, sparse := sparse, sparse_dense := sparse_dense, le_count := le_count }, mem =>
      let_fun isLt := ⋯;
      let dense' := dense.set count isLt j;
      let sparse' := sparse.set ↑j ⋯ ⟨count, isLt⟩;
      let_fun sparse_dense' := ⋯;
      { count := count + 1, dense := dense', sparse := sparse', sparse_dense := sparse_dense', le_count := isLt }
⊢ i ∈ s
Tactic:
have ne : j.val ≠ i.val := Ne.symm (Fin.val_ne_of_ne heq)
Proof state after:
n : Nat
s : SparseSet n
i j : Fin n
heq : ¬i = j
hmem : ¬j ∈ s
h :
  i ∈
    match s, hmem with
    | { count := count, dense := dense, sparse := sparse, sparse_dense := sparse_dense, le_count := le_count }, mem =>
      let_fun isLt := ⋯;
      let dense' := dense.set count isLt j;
      let sparse' := sparse.set ↑j ⋯ ⟨count, isLt⟩;
      let_fun sparse_dense' := ⋯;
      { count := count + 1, dense := dense', sparse := sparse', sparse_dense := sparse_dense', le_count := isLt }
ne : ↑j ≠ ↑i
⊢ i ∈ s
Theorem: Regex.Data.SparseSet.eq_or_mem_of_mem_insert
Proof state before:
n : Nat
s : SparseSet n
i j : Fin n
heq : ¬i = j
hmem : ¬j ∈ s
h :
  i ∈
    match s, hmem with
    | { count := count, dense := dense, sparse := sparse, sparse_dense := sparse_dense, le_count := le_count }, mem =>
      let_fun isLt := ⋯;
      let dense' := dense.set count isLt j;
      let sparse' := sparse.set ↑j ⋯ ⟨count, isLt⟩;
      let_fun sparse_dense' := ⋯;
      { count := count + 1, dense := dense', sparse := sparse', sparse_dense := sparse_dense', le_count := isLt }
ne : ↑j ≠ ↑i
⊢ i ∈ s
Tactic:
simp [mem, Vec.get_set, ne] at h
Proof state after:
n : Nat
s : SparseSet n
i j : Fin n
heq : ¬i = j
hmem : ¬j ∈ s
ne : ↑j ≠ ↑i
h : ↑s.sparse[↑i] < s.count + 1 ∧ (if s.count = ↑s.sparse[↑i] then j else s.dense[↑s.sparse[↑i]]) = i
⊢ i ∈ s
Theorem: Regex.Data.SparseSet.eq_or_mem_of_mem_insert
Proof state before:
n : Nat
s : SparseSet n
i j : Fin n
heq : ¬i = j
hmem : ¬j ∈ s
ne : ↑j ≠ ↑i
h : ↑s.sparse[↑i] < s.count + 1 ∧ (if s.count = ↑s.sparse[↑i] then j else s.dense[↑s.sparse[↑i]]) = i
⊢ i ∈ s
Tactic:
split at h
Proof state after:
case inl
n : Nat
s : SparseSet n
i j : Fin n
heq : ¬i = j
hmem : ¬j ∈ s
ne : ↑j ≠ ↑i
h✝ : s.count = ↑s.sparse[↑i]
h : ↑s.sparse[↑i] < s.count + 1 ∧ j = i
⊢ i ∈ s

case inr
n : Nat
s : SparseSet n
i j : Fin n
heq : ¬i = j
hmem : ¬j ∈ s
ne : ↑j ≠ ↑i
h✝ : ¬s.count = ↑s.sparse[↑i]
h : ↑s.sparse[↑i] < s.count + 1 ∧ s.dense[↑s.sparse[↑i]] = i
⊢ i ∈ s
Theorem: Regex.Data.SparseSet.eq_or_mem_of_mem_insert
Proof state before:
n : Nat
s : SparseSet n
i j : Fin n
heq : ¬i = j
hmem : ¬j ∈ s
ne : ↑j ≠ ↑i
heq' : s.count = ↑s.sparse[↑i]
h : ↑s.sparse[↑i] < s.count + 1 ∧ j = i
⊢ i ∈ s
Tactic:
case inl heq' => simp [h] at heq
Proof state after:
no goals
Theorem: Regex.Data.SparseSet.eq_or_mem_of_mem_insert
Proof state before:
n : Nat
s : SparseSet n
i j : Fin n
heq : ¬i = j
hmem : ¬j ∈ s
ne : ↑j ≠ ↑i
heq' : ¬s.count = ↑s.sparse[↑i]
h : ↑s.sparse[↑i] < s.count + 1 ∧ s.dense[↑s.sparse[↑i]] = i
⊢ i ∈ s
Tactic:
case inr heq' =>
  have : s.sparse[i.val] < s.count := by
    have : s.sparse[i.val] ≤ s.count := Nat.le_of_lt_succ h.left
    exact Nat.lt_of_le_of_ne this (Ne.symm heq')
  simp [mem, this, h]
Proof state after:
no goals
Theorem: Regex.Data.SparseSet.eq_or_mem_of_mem_insert
Proof state before:
n : Nat
s : SparseSet n
i j : Fin n
heq : ¬i = j
hmem : ¬j ∈ s
ne : ↑j ≠ ↑i
heq' : s.count = ↑s.sparse[↑i]
h : ↑s.sparse[↑i] < s.count + 1 ∧ j = i
⊢ i ∈ s
Tactic:
simp [h] at heq
Proof state after:
no goals
Theorem: Regex.Data.SparseSet.eq_or_mem_of_mem_insert
Proof state before:
n : Nat
s : SparseSet n
i j : Fin n
heq : ¬i = j
hmem : ¬j ∈ s
ne : ↑j ≠ ↑i
heq' : ¬s.count = ↑s.sparse[↑i]
h : ↑s.sparse[↑i] < s.count + 1 ∧ s.dense[↑s.sparse[↑i]] = i
⊢ i ∈ s
Tactic:
have : s.sparse[i.val] < s.count := by
  have : s.sparse[i.val] ≤ s.count := Nat.le_of_lt_succ h.left
  exact Nat.lt_of_le_of_ne this (Ne.symm heq')
Proof state after:
n : Nat
s : SparseSet n
i j : Fin n
heq : ¬i = j
hmem : ¬j ∈ s
ne : ↑j ≠ ↑i
heq' : ¬s.count = ↑s.sparse[↑i]
h : ↑s.sparse[↑i] < s.count + 1 ∧ s.dense[↑s.sparse[↑i]] = i
this : ↑s.sparse[↑i] < s.count
⊢ i ∈ s
Theorem: Regex.Data.SparseSet.eq_or_mem_of_mem_insert
Proof state before:
n : Nat
s : SparseSet n
i j : Fin n
heq : ¬i = j
hmem : ¬j ∈ s
ne : ↑j ≠ ↑i
heq' : ¬s.count = ↑s.sparse[↑i]
h : ↑s.sparse[↑i] < s.count + 1 ∧ s.dense[↑s.sparse[↑i]] = i
this : ↑s.sparse[↑i] < s.count
⊢ i ∈ s
Tactic:
simp [mem, this, h]
Proof state after:
no goals