-- Mathlib/Computability/PostTuringMachine.lean
theorem exists_enc_dec [Inhabited Γ] [Finite Γ] :
    ∃ (n : ℕ) (enc : Γ → List.Vector Bool n) (dec : List.Vector Bool n → Γ),
      enc default = Vector.replicate n false ∧ ∀ a, dec (enc a) = a

Proof state:
case intro.intro
Γ : Type u_1
inst✝¹ : Inhabited Γ
inst✝ : Finite Γ
n : ℕ
e : Γ ≃ Fin n
this : DecidableEq Γ := e.decidableEq
G : Fin n ↪ Fin n → Bool := { toFun := fun a b => decide (a = b), inj' := ⋯ }
H : Γ ↪ List.Vector Bool n := (e.toEmbedding.trans G).trans (Equiv.vectorEquivFin Bool n).symm.toEmbedding
⊢ ∃ n enc dec, enc default = Vector.replicate n false ∧ ∀ (a : Γ), dec (enc a) = a

Tactic:
let enc := H.setValue default (Vector.replicate n false)

Result:
case intro.intro
Γ : Type u_1
inst✝¹ : Inhabited Γ
inst✝ : Finite Γ
n : ℕ
e : Γ ≃ Fin n
this : DecidableEq Γ := e.decidableEq
G : Fin n ↪ Fin n → Bool := { toFun := fun a b => decide (a = b), inj' := ⋯ }
H : Γ ↪ List.Vector Bool n := (e.toEmbedding.trans G).trans (Equiv.vectorEquivFin Bool n).symm.toEmbedding
enc : Γ ↪ List.Vector Bool n := H.setValue default (Vector.replicate n false)
⊢ ∃ n enc dec, enc default = Vector.replicate n false ∧ ∀ (a : Γ), dec (enc a) = a

Proof state:
Γ : Type u_1
inst✝¹ : Inhabited Γ
inst✝ : Finite Γ
⊢ ∃ n enc dec, enc default = Vector.replicate n false ∧ ∀ (a : Γ), dec (enc a) = a

Tactic:
rcases Finite.exists_equiv_fin Γ with ⟨n, ⟨e⟩⟩

Result:
case intro.intro
Γ : Type u_1
inst✝¹ : Inhabited Γ
inst✝ : Finite Γ
n : ℕ
e : Γ ≃ Fin n
⊢ ∃ n enc dec, enc default = Vector.replicate n false ∧ ∀ (a : Γ), dec (enc a) = a

Proof state:
case intro.intro
Γ : Type u_1
inst✝¹ : Inhabited Γ
inst✝ : Finite Γ
n : ℕ
e : Γ ≃ Fin n
this : DecidableEq Γ := e.decidableEq
G : Fin n ↪ Fin n → Bool := { toFun := fun a b => decide (a = b), inj' := ⋯ }
⊢ ∃ n enc dec, enc default = Vector.replicate n false ∧ ∀ (a : Γ), dec (enc a) = a

Tactic:
let H := (e.toEmbedding.trans G).trans (Equiv.vectorEquivFin _ _).symm.toEmbedding

Result:
case intro.intro
Γ : Type u_1
inst✝¹ : Inhabited Γ
inst✝ : Finite Γ
n : ℕ
e : Γ ≃ Fin n
this : DecidableEq Γ := e.decidableEq
G : Fin n ↪ Fin n → Bool := { toFun := fun a b => decide (a = b), inj' := ⋯ }
H : Γ ↪ List.Vector Bool n := (e.toEmbedding.trans G).trans (Equiv.vectorEquivFin Bool n).symm.toEmbedding
⊢ ∃ n enc dec, enc default = Vector.replicate n false ∧ ∀ (a : Γ), dec (enc a) = a

Proof state:
case intro.intro
Γ : Type u_1
inst✝¹ : Inhabited Γ
inst✝ : Finite Γ
n : ℕ
e : Γ ≃ Fin n
⊢ ∃ n enc dec, enc default = Vector.replicate n false ∧ ∀ (a : Γ), dec (enc a) = a

Tactic:
letI : DecidableEq Γ := e.decidableEq

Result:
case intro.intro
Γ : Type u_1
inst✝¹ : Inhabited Γ
inst✝ : Finite Γ
n : ℕ
e : Γ ≃ Fin n
this : DecidableEq Γ := e.decidableEq
⊢ ∃ n enc dec, enc default = Vector.replicate n false ∧ ∀ (a : Γ), dec (enc a) = a

Proof state:
case intro.intro
Γ : Type u_1
inst✝¹ : Inhabited Γ
inst✝ : Finite Γ
n : ℕ
e : Γ ≃ Fin n
this : DecidableEq Γ := e.decidableEq
G : Fin n ↪ Fin n → Bool := { toFun := fun a b => decide (a = b), inj' := ⋯ }
H : Γ ↪ List.Vector Bool n := (e.toEmbedding.trans G).trans (Equiv.vectorEquivFin Bool n).symm.toEmbedding
enc : Γ ↪ List.Vector Bool n := H.setValue default (Vector.replicate n false)
⊢ ∃ n enc dec, enc default = Vector.replicate n false ∧ ∀ (a : Γ), dec (enc a) = a

Tactic:
exact ⟨_, enc, Function.invFun enc, H.setValue_eq _ _, Function.leftInverse_invFun enc.2⟩

Result:
no goals

Proof state:
case intro.intro
Γ : Type u_1
inst✝¹ : Inhabited Γ
inst✝ : Finite Γ
n : ℕ
e : Γ ≃ Fin n
this : DecidableEq Γ := e.decidableEq
⊢ ∃ n enc dec, enc default = Vector.replicate n false ∧ ∀ (a : Γ), dec (enc a) = a

Tactic:
let G : Fin n ↪ Fin n → Bool :=
  ⟨fun a b ↦ a = b, fun a b h ↦
    Bool.of_decide_true <| (congr_fun h b).trans <| Bool.decide_true rfl⟩

Result:
case intro.intro
Γ : Type u_1
inst✝¹ : Inhabited Γ
inst✝ : Finite Γ
n : ℕ
e : Γ ≃ Fin n
this : DecidableEq Γ := e.decidableEq
G : Fin n ↪ Fin n → Bool := { toFun := fun a b => decide (a = b), inj' := ⋯ }
⊢ ∃ n enc dec, enc default = Vector.replicate n false ∧ ∀ (a : Γ), dec (enc a) = a