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

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

State before:
α : Type u_1
inst : Alphabet α
n : ℕ
⊢ encode (decode (Nat.succ n)) = Nat.succ n
Tactic:
have ih := @decodenk α _ (n / inst.card)
State after:
α : Type u_1
inst : Alphabet α
n : ℕ
ih : encode (decode (n / Fintype.card α)) = n / Fintype.card α
⊢ encode (decode (Nat.succ n)) = Nat.succ n

State before:
α : Type u_1
inst : Alphabet α
n : ℕ
ih : encode (decode (n / Fintype.card α)) = n / Fintype.card α
⊢ encode (decode (Nat.succ n)) = Nat.succ n
Tactic:
simp [decode, FinDenumerable.decode_fin]
State after:
α : Type u_1
inst : Alphabet α
n : ℕ
ih : encode (decode (n / Fintype.card α)) = n / Fintype.card α
⊢ encode (Option.get (Encodable.decode ↑(Nat.fin_mod n ⋯)) ⋯ :: decode (n / Fintype.card α)) = Nat.succ n

State before:
α : Type u_1
inst : Alphabet α
n : ℕ
ih : encode (decode (n / Fintype.card α)) = n / Fintype.card α
⊢ encode (Option.get (Encodable.decode ↑(Nat.fin_mod n ⋯)) ⋯ :: decode (n / Fintype.card α)) = Nat.succ n
Tactic:
simp [encode, inst.decode_fin_is_some (Nat.fin_mod _ _)]
State after:
α : Type u_1
inst : Alphabet α
n : ℕ
ih : encode (decode (n / Fintype.card α)) = n / Fintype.card α
⊢ encode (decode (n / Fintype.card α)) * Fintype.card α +
      Encodable.encode (Option.get (Encodable.decode ↑(Nat.fin_mod n ⋯)) ⋯) =
    n

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

State before:
α : Type u_1
inst : Alphabet α
n : ℕ
ih : encode (decode (n / Fintype.card α)) = n / Fintype.card α
⊢ n / Fintype.card α * Fintype.card α + Encodable.encode (FinDenumerable.decode_fin (Nat.fin_mod n ⋯)) = n
Tactic:
rw [<- inst.encode_fin_eq_encode _, inst.decodenk]
State after:
α : Type u_1
inst : Alphabet α
n : ℕ
ih : encode (decode (n / Fintype.card α)) = n / Fintype.card α
⊢ n / Fintype.card α * Fintype.card α + ↑(Nat.fin_mod n ⋯) = n

State before:
α : Type u_1
inst : Alphabet α
n : ℕ
ih : encode (decode (n / Fintype.card α)) = n / Fintype.card α
⊢ n / Fintype.card α * Fintype.card α + ↑(Nat.fin_mod n ⋯) = n
Tactic:
simp [Nat.fin_mod, Nat.mul_comm, Nat.div_add_mod n inst.card]
State after:
no goals

State before:
α : Type u_1
inst : Alphabet α
n✝ : ℕ
a✝ : ∀ (y : ℕ), (invImage (fun a => a) instWellFoundedRelation).1 y n✝ → encode (decode y) = y
n : ℕ
x✝ : ∀ (y : ℕ), (invImage (fun a => a) instWellFoundedRelation).1 y (Nat.succ n) → encode (decode y) = y
⊢ (invImage (fun a => a) instWellFoundedRelation).1 (n / Fintype.card α) (Nat.succ n)
Tactic:
simp [InvImage]
State after:
α : Type u_1
inst : Alphabet α
n✝ : ℕ
a✝ : ∀ (y : ℕ), (invImage (fun a => a) instWellFoundedRelation).1 y n✝ → encode (decode y) = y
n : ℕ
x✝ : ∀ (y : ℕ), (invImage (fun a => a) instWellFoundedRelation).1 y (Nat.succ n) → encode (decode y) = y
⊢ WellFoundedRelation.rel (n / Fintype.card α) (Nat.succ n)

State before:
α : Type u_1
inst : Alphabet α
n✝ : ℕ
a✝ : ∀ (y : ℕ), (invImage (fun a => a) instWellFoundedRelation).1 y n✝ → encode (decode y) = y
n : ℕ
x✝ : ∀ (y : ℕ), (invImage (fun a => a) instWellFoundedRelation).1 y (Nat.succ n) → encode (decode y) = y
⊢ WellFoundedRelation.rel (n / Fintype.card α) (Nat.succ n)
Tactic:
apply Nat.lt_of_le_of_lt
State after:
case h₁
α : Type u_1
inst : Alphabet α
n✝ : ℕ
a✝ : ∀ (y : ℕ), (invImage (fun a => a) instWellFoundedRelation).1 y n✝ → encode (decode y) = y
n : ℕ
x✝ : ∀ (y : ℕ), (invImage (fun a => a) instWellFoundedRelation).1 y (Nat.succ n) → encode (decode y) = y
⊢ sizeOf (n / Fintype.card α) ≤ ?m

case h₂
α : Type u_1
inst : Alphabet α
n✝ : ℕ
a✝ : ∀ (y : ℕ), (invImage (fun a => a) instWellFoundedRelation).1 y n✝ → encode (decode y) = y
n : ℕ
x✝ : ∀ (y : ℕ), (invImage (fun a => a) instWellFoundedRelation).1 y (Nat.succ n) → encode (decode y) = y
⊢ ?m < sizeOf (Nat.succ n)

case m
α : Type u_1
inst : Alphabet α
n✝ : ℕ
a✝ : ∀ (y : ℕ), (invImage (fun a => a) instWellFoundedRelation).1 y n✝ → encode (decode y) = y
n : ℕ
x✝ : ∀ (y : ℕ), (invImage (fun a => a) instWellFoundedRelation).1 y (Nat.succ n) → encode (decode y) = y
⊢ ℕ

State before:
case h₁
α : Type u_1
inst : Alphabet α
n✝ : ℕ
a✝ : ∀ (y : ℕ), (invImage (fun a => a) instWellFoundedRelation).1 y n✝ → encode (decode y) = y
n : ℕ
x✝ : ∀ (y : ℕ), (invImage (fun a => a) instWellFoundedRelation).1 y (Nat.succ n) → encode (decode y) = y
⊢ sizeOf (n / Fintype.card α) ≤ ?m

case h₂
α : Type u_1
inst : Alphabet α
n✝ : ℕ
a✝ : ∀ (y : ℕ), (invImage (fun a => a) instWellFoundedRelation).1 y n✝ → encode (decode y) = y
n : ℕ
x✝ : ∀ (y : ℕ), (invImage (fun a => a) instWellFoundedRelation).1 y (Nat.succ n) → encode (decode y) = y
⊢ ?m < sizeOf (Nat.succ n)

case m
α : Type u_1
inst : Alphabet α
n✝ : ℕ
a✝ : ∀ (y : ℕ), (invImage (fun a => a) instWellFoundedRelation).1 y n✝ → encode (decode y) = y
n : ℕ
x✝ : ∀ (y : ℕ), (invImage (fun a => a) instWellFoundedRelation).1 y (Nat.succ n) → encode (decode y) = y
⊢ ℕ
Tactic:
exact Nat.div_le_self n inst.card
State after:
case h₂
α : Type u_1
inst : Alphabet α
n✝ : ℕ
a✝ : ∀ (y : ℕ), (invImage (fun a => a) instWellFoundedRelation).1 y n✝ → encode (decode y) = y
n : ℕ
x✝ : ∀ (y : ℕ), (invImage (fun a => a) instWellFoundedRelation).1 y (Nat.succ n) → encode (decode y) = y
⊢ n < sizeOf (Nat.succ n)

State before:
case h₂
α : Type u_1
inst : Alphabet α
n✝ : ℕ
a✝ : ∀ (y : ℕ), (invImage (fun a => a) instWellFoundedRelation).1 y n✝ → encode (decode y) = y
n : ℕ
x✝ : ∀ (y : ℕ), (invImage (fun a => a) instWellFoundedRelation).1 y (Nat.succ n) → encode (decode y) = y
⊢ n < sizeOf (Nat.succ n)
Tactic:
simp
State after:
no goals