Theorem: Regex.Data.SparseSet.dense_sparse_of_full (Regex/Data/SparseSet/Basic.lean)

State before:
n : Nat
s : SparseSet n
i j : Fin n
h : n ≤ s.count
⊢ s.dense[s.sparse[j]] = j
Tactic:
let f (i : Fin n) : Fin n := s.dense[i]
State after:
n : Nat
s : SparseSet n
i j : Fin n
h : n ≤ s.count
f : Fin n → Fin n := fun i => s.dense[i]
⊢ s.dense[s.sparse[j]] = j

State before:
n : Nat
s : SparseSet n
i j : Fin n
h : n ≤ s.count
f : Fin n → Fin n := fun i => s.dense[i]
⊢ s.dense[s.sparse[j]] = j
Tactic:
have inj : inj f := by
  intro x y eq
  exact dense_inj (Nat.lt_of_lt_of_le x.isLt h) (Nat.lt_of_lt_of_le y.isLt h) eq
State after:
n : Nat
s : SparseSet n
i j : Fin n
h : n ≤ s.count
f : Fin n → Fin n := fun i => s.dense[i]
inj : Regex.Data.SparseSet.Bijection.inj f
⊢ s.dense[s.sparse[j]] = j

State before:
n : Nat
s : SparseSet n
i j : Fin n
h : n ≤ s.count
f : Fin n → Fin n := fun i => s.dense[i]
inj : Regex.Data.SparseSet.Bijection.inj f
⊢ s.dense[s.sparse[j]] = j
Tactic:
have surj : surj f := surj_of_inj _ inj
State after:
n : Nat
s : SparseSet n
i j : Fin n
h : n ≤ s.count
f : Fin n → Fin n := fun i => s.dense[i]
inj : Regex.Data.SparseSet.Bijection.inj f
surj : Regex.Data.SparseSet.Bijection.surj f
⊢ s.dense[s.sparse[j]] = j

State before:
n : Nat
s : SparseSet n
i j : Fin n
h : n ≤ s.count
f : Fin n → Fin n := fun i => s.dense[i]
inj : Regex.Data.SparseSet.Bijection.inj f
surj : Regex.Data.SparseSet.Bijection.surj f
⊢ s.dense[s.sparse[j]] = j
Tactic:
have ⟨i, eq⟩ := surj j
State after:
n : Nat
s : SparseSet n
i✝ j : Fin n
h : n ≤ s.count
f : Fin n → Fin n := fun i => s.dense[i]
inj : Regex.Data.SparseSet.Bijection.inj f
surj : Regex.Data.SparseSet.Bijection.surj f
i : Fin n
eq : f i = j
⊢ s.dense[s.sparse[j]] = j

State before:
n : Nat
s : SparseSet n
i✝ j : Fin n
h : n ≤ s.count
f : Fin n → Fin n := fun i => s.dense[i]
inj : Regex.Data.SparseSet.Bijection.inj f
surj : Regex.Data.SparseSet.Bijection.surj f
i : Fin n
eq : f i = j
⊢ s.dense[s.sparse[j]] = j
Tactic:
simp [f, ←eq, s.sparse_dense i (Nat.lt_of_lt_of_le i.isLt h)]
State after:
no goals

State before:
n : Nat
s : SparseSet n
i j : Fin n
h : n ≤ s.count
f : Fin n → Fin n := fun i => s.dense[i]
⊢ inj f
Tactic:
intro x y eq
State after:
n : Nat
s : SparseSet n
i j : Fin n
h : n ≤ s.count
f : Fin n → Fin n := fun i => s.dense[i]
x y : Fin n
eq : f x = f y
⊢ x = y

State before:
n : Nat
s : SparseSet n
i j : Fin n
h : n ≤ s.count
f : Fin n → Fin n := fun i => s.dense[i]
x y : Fin n
eq : f x = f y
⊢ x = y
Tactic:
exact dense_inj (Nat.lt_of_lt_of_le x.isLt h) (Nat.lt_of_lt_of_le y.isLt h) eq
State after:
no goals