Theorem: Word.encodek (FormalSystems/Preliminaries/Word.lean)

State before:
α : Type u_1
inst : Alphabet α
⊢ decode (encode []) = []
Tactic:
simp [encode, decode]
State after:
no goals

State before:
α : Type u_1
inst : Alphabet α
x : α
xs : List α
⊢ decode (encode (x :: xs)) = x :: xs
Tactic:
have ih := encodek xs
State after:
α : Type u_1
inst : Alphabet α
x : α
xs : List α
ih : decode (encode xs) = xs
⊢ decode (encode (x :: xs)) = x :: xs

State before:
α : Type u_1
inst : Alphabet α
x : α
xs : List α
ih : decode (encode xs) = xs
⊢ decode (encode (x :: xs)) = x :: xs
Tactic:
simp [encode, decode, Nat.fin_mod, FinDenumerable.decode_fin]
State after:
α : Type u_1
inst : Alphabet α
x : α
xs : List α
ih : decode (encode xs) = xs
⊢ Option.get (Encodable.decode ((encode xs * Fintype.card α + Encodable.encode x) % Fintype.card α)) ⋯ ::
      decode ((encode xs * Fintype.card α + Encodable.encode x) / Fintype.card α) =
    x :: xs

State before:
α : Type u_1
inst : Alphabet α
x : α
xs : List α
ih : decode (encode xs) = xs
⊢ Option.get (Encodable.decode ((encode xs * Fintype.card α + Encodable.encode x) % Fintype.card α)) ⋯ ::
      decode ((encode xs * Fintype.card α + Encodable.encode x) / Fintype.card α) =
    x :: xs
Tactic:
simp [<- Nat.mod_add_mod, Nat.mod_eq_of_lt $ inst.encode_lt_card x]
State after:
α : Type u_1
inst : Alphabet α
x : α
xs : List α
ih : decode (encode xs) = xs
⊢ x :: decode ((encode xs * Fintype.card α + Encodable.encode x) / Fintype.card α) = x :: xs

State before:
α : Type u_1
inst : Alphabet α
x : α
xs : List α
ih : decode (encode xs) = xs
⊢ x :: decode ((encode xs * Fintype.card α + Encodable.encode x) / Fintype.card α) = x :: xs
Tactic:
simp [Nat.add_div inst.card_pos, Nat.div_eq_of_lt $ inst.encode_lt_card x]
State after:
α : Type u_1
inst : Alphabet α
x : α
xs : List α
ih : decode (encode xs) = xs
⊢ x ::
      decode
        (encode xs * Fintype.card α / Fintype.card α +
          if Fintype.card α ≤ Encodable.encode x % Fintype.card α then 1 else 0) =
    x :: xs

State before:
α : Type u_1
inst : Alphabet α
x : α
xs : List α
ih : decode (encode xs) = xs
⊢ x ::
      decode
        (encode xs * Fintype.card α / Fintype.card α +
          if Fintype.card α ≤ Encodable.encode x % Fintype.card α then 1 else 0) =
    x :: xs
Tactic:
simp [Nat.mul_div_cancel (encode xs) inst.card_pos]
State after:
α : Type u_1
inst : Alphabet α
x : α
xs : List α
ih : decode (encode xs) = xs
⊢ x :: decode (encode xs + if Fintype.card α ≤ Encodable.encode x % Fintype.card α then 1 else 0) = x :: xs

State before:
α : Type u_1
inst : Alphabet α
x : α
xs : List α
ih : decode (encode xs) = xs
⊢ x :: decode (encode xs + if Fintype.card α ≤ Encodable.encode x % Fintype.card α then 1 else 0) = x :: xs
Tactic:
rw [<- ite_not _]
State after:
α : Type u_1
inst : Alphabet α
x : α
xs : List α
ih : decode (encode xs) = xs
⊢ x :: decode (encode xs + if ¬Fintype.card α ≤ Encodable.encode x % Fintype.card α then 0 else 1) = x :: xs

State before:
α : Type u_1
inst : Alphabet α
x : α
xs : List α
ih : decode (encode xs) = xs
⊢ x :: decode (encode xs + if ¬Fintype.card α ≤ Encodable.encode x % Fintype.card α then 0 else 1) = x :: xs
Tactic:
simp [Nat.not_le_of_lt _, Nat.mod_lt _ inst.card_pos, ih]
State after:
no goals