awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.DFA
Goal:
α : Type u
σ : Type v
M : DFA α σ
α' : Type u_1
f : α' → α
s : σ
x : List α'
a : α'
ih : (comap f M).evalFrom s x = M.evalFrom s (List.map f x)
⊢ (comap f M).evalFrom s (x ++ [a]) = M.evalFrom s (List.map f (x ++ [a]))

Tactic:
simp [ih]
-- Module: Mathlib.Computability.DFA
Goal:
α : Type u
σ : Type v
M : DFA α σ
α' : Type u_1
f : α' → α
s : σ
x : List α'
nil : (comap f M).evalFrom s [] = M.evalFrom s (List.map f [])
append_singleton :
  ∀ (x : List α') (a : α') (ih : (comap f M).evalFrom s x = M.evalFrom s (List.map f x)),
    (comap f M).evalFrom s (x ++ [a]) = M.evalFrom s (List.map f (x ++ [a]))
⊢ (comap f M).evalFrom s x = M.evalFrom s (List.map f x)

Tactic:
induction x using List.reverseRecOn with
  | nil => simp
  | append_singleton x a ih => simp [ih]
-- Module: Mathlib.Computability.DFA
Goal:
α : Type u
σ : Type v
M : DFA α σ
α' : Type u_1
f : α' → α
x : List α'
⊢ (comap f M).eval x = M.eval (List.map f x)

Tactic:
simp [eval]

Premises used: DFA.eval
-- Module: Mathlib.Computability.DFA
Goal:
α : Type u
σ : Type v
M : DFA α σ
α' : Type u_1
f : α' → α
h : ∀ (x : List α'), x ∈ (comap f M).accepts ↔ x ∈ List.map f ⁻¹' M.accepts
⊢ (comap f M).accepts = List.map f ⁻¹' M.accepts

Tactic:
ext x
-- Module: Mathlib.Computability.DFA
Goal:
α : Type u
σ : Type v
M : DFA α σ
α' : Type u_1
f : α' → α
x : List α'
rhs : x ∈ List.map f ⁻¹' M.accepts
| x ∈ (comap f M).accepts ↔ x ∈ List.map f ⁻¹' M.accepts

Tactic:
rhs
-- Module: Mathlib.Computability.DFA
Goal:
α : Type u
σ : Type v
M : DFA α σ
α' : Type u_1
f : α' → α
x : List α'
rw : M.eval (List.map f x) ∈ M.accept
| x ∈ List.map f ⁻¹' M.accepts

Tactic:
rw [Set.mem_preimage, mem_accepts]

Premises used: Set.mem_preimage, DFA.mem_accepts
-- Module: Mathlib.Computability.DFA
Goal:
α : Type u
σ : Type v
M : DFA α σ
α' : Type u_1
f : α' → α
x : List α'
rw : M.eval (List.map f x) ∈ M.accept
| x ∈ (comap f M).accepts ↔ x ∈ List.map f ⁻¹' M.accepts

Tactic:
rhs
    rw [Set.mem_preimage, mem_accepts]

Premises used: Set.mem_preimage, DFA.mem_accepts
-- Module: Mathlib.Computability.DFA
Goal:
α : Type u
σ : Type v
M : DFA α σ
α' : Type u_1
f : α' → α
x : List α'
h : x ∈ (comap f M).accepts ↔ M.eval (List.map f x) ∈ M.accept
⊢ x ∈ (comap f M).accepts ↔ x ∈ List.map f ⁻¹' M.accepts

Tactic:
conv =>
    rhs
    rw [Set.mem_preimage, mem_accepts]

Premises used: Set.mem_preimage, DFA.mem_accepts
-- Module: Mathlib.Computability.DFA
Goal:
α : Type u
σ : Type v
M : DFA α σ
α' : Type u_1
f : α' → α
x : List α'
⊢ x ∈ (comap f M).accepts ↔ M.eval (List.map f x) ∈ M.accept

Tactic:
simp [mem_accepts]

Premises used: DFA.mem_accepts
-- Module: Mathlib.Computability.DFA
Goal:
α : Type u
σ : Type v
M_1 : DFA α σ
α' : Type u_1
σ' : Type u_2
g : σ ≃ σ'
M : DFA α σ
⊢ (fun (M : DFA α σ') ↦
        ({ step := fun (s : σ) (a : α) ↦ (g.symm : (a : σ') → σ) (M.step ((g : (a : σ) → σ') s) a),
            start := (g.symm : (a : σ') → σ) M.start, accept := (⇑g : (a : σ) → σ') ⁻¹' M.accept } :
          DFA α σ))
      ((fun (M : DFA α σ) ↦
          ({ step := fun (s : σ') (a : α) ↦ (g : (a : σ) → σ') (M.step ((g.symm : (a : σ') → σ) s) a),
              start := (g : (a : σ) → σ') M.start, accept := (⇑g.symm : (a : σ') → σ) ⁻¹' M.accept } :
            DFA α σ'))
        M) =
    M

Tactic:
simp
-- Module: Mathlib.Computability.DFA
Goal:
α : Type u
σ : Type v
M_1 : DFA α σ
α' : Type u_1
σ' : Type u_2
g : σ ≃ σ'
M : DFA α σ'
⊢ (fun (M : DFA α σ) ↦
        ({ step := fun (s : σ') (a : α) ↦ (g : (a : σ) → σ') (M.step ((g.symm : (a : σ') → σ) s) a),
            start := (g : (a : σ) → σ') M.start, accept := (⇑g.symm : (a : σ') → σ) ⁻¹' M.accept } :
          DFA α σ'))
      ((fun (M : DFA α σ') ↦
          ({ step := fun (s : σ) (a : α) ↦ (g.symm : (a : σ') → σ) (M.step ((g : (a : σ) → σ') s) a),
              start := (g.symm : (a : σ') → σ) M.start, accept := (⇑g : (a : σ) → σ') ⁻¹' M.accept } :
            DFA α σ))
        M) =
    M

Tactic:
simp
-- Module: Mathlib.Computability.DFA
Goal:
α : Type u
σ : Type v
M : DFA α σ
⊢ (reindex (Equiv.refl σ) : (a : DFA α σ) → DFA α σ) M = M

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, rfl
-- Module: Mathlib.Computability.DFA
Goal:
α : Type u
σ : Type v
σ' : Type u_2
g : σ ≃ σ'
⊢ Eq (α := DFA α σ' ≃ DFA α σ) (Equiv.symm (reindex g)) (reindex g.symm)

Tactic:
rfl

Premises used: DFA.reindex, Equiv.symm, rfl
-- Module: Mathlib.Computability.DFA
Goal:
α : Type u
σ : Type v
M : DFA α σ
σ' : Type u_2
g : σ ≃ σ'
s : σ'
⊢ evalFrom.{u, u_2} (α := α) ((reindex g : (a : DFA α σ) → DFA α σ') M) s [] =
    (g : (a : σ) → σ') (M.evalFrom ((g.symm : (a : σ') → σ) s) [])

Tactic:
simp
-- Module: Mathlib.Computability.DFA
Goal:
α : Type u
σ : Type v
M : DFA α σ
σ' : Type u_2
g : σ ≃ σ'
s : σ'
x : List α
a : α
ih :
  evalFrom ((reindex g : (a : DFA α σ) → DFA α σ') M) s x =
    (g : (a : σ) → σ') (M.evalFrom ((g.symm : (a : σ') → σ) s) x)
⊢ evalFrom ((reindex g : (a : DFA α σ) → DFA α σ') M) s (x ++ [a]) =
    (g : (a : σ) → σ') (M.evalFrom ((g.symm : (a : σ') → σ) s) (x ++ [a]))

Tactic:
simp [ih]
-- Module: Mathlib.Computability.DFA
Goal:
α : Type u
σ : Type v
M : DFA α σ
σ' : Type u_2
g : σ ≃ σ'
s : σ'
x : List α
nil :
  evalFrom.{u, u_2} (α := α) ((reindex g : (a : DFA α σ) → DFA α σ') M) s [] =
    (g : (a : σ) → σ') (M.evalFrom ((g.symm : (a : σ') → σ) s) [])
append_singleton :
  ∀ (x : List α) (a : α)
    (ih :
      evalFrom ((reindex g : (a : DFA α σ) → DFA α σ') M) s x =
        (g : (a : σ) → σ') (M.evalFrom ((g.symm : (a : σ') → σ) s) x)),
    evalFrom ((reindex g : (a : DFA α σ) → DFA α σ') M) s (x ++ [a]) =
      (g : (a : σ) → σ') (M.evalFrom ((g.symm : (a : σ') → σ) s) (x ++ [a]))
⊢ evalFrom ((reindex g : (a : DFA α σ) → DFA α σ') M) s x =
    (g : (a : σ) → σ') (M.evalFrom ((g.symm : (a : σ') → σ) s) x)

Tactic:
induction x using List.reverseRecOn with
  | nil => simp
  | append_singleton x a ih => simp [ih]
-- Module: Mathlib.Computability.DFA
Goal:
α : Type u
σ : Type v
M : DFA α σ
σ' : Type u_2
g : σ ≃ σ'
x : List α
⊢ Eq.{u_2 + 1} (α := σ') (eval ((reindex g : (a : DFA α σ) → DFA α σ') M) x : σ') ((g : (a : σ) → σ') (M.eval x) : σ')

Tactic:
simp [eval]

Premises used: DFA.eval
-- Module: Mathlib.Computability.DFA
Goal:
α : Type u
σ : Type v
M : DFA α σ
σ' : Type u_2
g : σ ≃ σ'
h :
  ∀ (x : List α),
    Membership.mem (γ := Language α) (accepts.{u, u_2} (σ := σ') ((reindex g : (a : DFA α σ) → DFA α σ') M)) x ↔
      x ∈ M.accepts
⊢ accepts.{u, u_2} (σ := σ') ((reindex g : (a : DFA α σ) → DFA α σ') M) = M.accepts

Tactic:
ext x
-- Module: Mathlib.Computability.DFA
Goal:
α : Type u
σ : Type v
M : DFA α σ
σ' : Type u_2
g : σ ≃ σ'
x : List α
⊢ Membership.mem (γ := Language α) (accepts.{u, u_2} (σ := σ') ((reindex g : (a : DFA α σ) → DFA α σ') M)) x ↔
    x ∈ M.accepts

Tactic:
simp [mem_accepts]

Premises used: DFA.mem_accepts
-- Module: Mathlib.Computability.DFA
Goal:
α : Type u
σ : Type v
M : DFA α σ
α' : Type u_1
σ' : Type u_2
f : α' → α
g : σ ≃ σ'
⊢ Eq (α := DFA α' σ') (comap f ((reindex g : (a : DFA α σ) → DFA α σ') M))
    ((reindex g : (a : DFA α' σ) → DFA α' σ') (comap f M))

Tactic:
simp [comap, reindex]

Premises used: DFA.reindex, DFA.comap
-- Module: Mathlib.Computability.DFA
Goal:
α : Type u
σ : Type v
M : DFA α σ
⊢ Mᶜ = { step := M.step, start := M.start, accept := M.acceptᶜ }

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Computability.DFA
Goal:
α : Type u
σ : Type v
M : DFA α σ
s : σ
⊢ Mᶜ.acceptsFrom s = (M.acceptsFrom s)ᶜ

Tactic:
rfl

Premises used: Set.Mem, setOf, DFA.acceptsFrom, DFA.evalFrom, Not, rfl
-- Module: Mathlib.Computability.DFA
Goal:
α : Type u
σ : Type v
M : DFA α σ
⊢ Mᶜ.accepts = M.acceptsᶜ

Tactic:
rfl

Premises used: Set.Mem, setOf, DFA.acceptsFrom, DFA.evalFrom, DFA.accepts, Not, rfl
-- Module: Mathlib.Computability.DFA
Goal:
α : Type u
σ1 σ2 : Type v
M1 : DFA α σ1
M2 : DFA α σ2
s1 : σ1
s2 : σ2
h : ∀ (x : List α), x ∈ (M1.union M2).acceptsFrom (s1, s2) ↔ x ∈ M1.acceptsFrom s1 + M2.acceptsFrom s2
⊢ (M1.union M2).acceptsFrom (s1, s2) = M1.acceptsFrom s1 + M2.acceptsFrom s2

Tactic:
ext x
-- Module: Mathlib.Computability.DFA
Goal:
α : Type u
σ1 σ2 : Type v
M1 : DFA α σ1
M2 : DFA α σ2
s1 : σ1
s2 : σ2
x : List α
h :
  (M1.union M2).evalFrom (s1, s2) x ∈ (M1.union M2).accept ↔ M1.evalFrom s1 x ∈ M1.accept ∨ M2.evalFrom s2 x ∈ M2.accept
⊢ Membership.mem (γ := Language α) {x : List α | (M1.union M2).evalFrom (s1, s2) x ∈ (M1.union M2).accept} x ↔
    Membership.mem (γ := Set (List α)) {x : List α | M1.evalFrom s1 x ∈ M1.accept} x ∨
      Membership.mem (γ := Set (List α)) {x : List α | M2.evalFrom s2 x ∈ M2.accept} x

Tactic:
simp_rw [↑Set.mem_setOf]

Premises used: Set.mem_setOf
-- Module: Mathlib.Computability.DFA
Goal:
α : Type u
σ1 σ2 : Type v
M1 : DFA α σ1
M2 : DFA α σ2
s1 : σ1
s2 : σ2
⊢ (M1.union M2).evalFrom (s1, s2) [] ∈ (M1.union M2).accept ↔
    M1.evalFrom s1 [] ∈ M1.accept ∨ M2.evalFrom s2 [] ∈ M2.accept

Tactic:
simp
-- Module: Mathlib.Computability.DFA
Goal:
α : Type u
σ1 σ2 : Type v
M1 : DFA α σ1
M2 : DFA α σ2
a : α
x : List α
ih :
  ∀ (s1 : σ1) (s2 : σ2),
    (M1.union M2).evalFrom (s1, s2) x ∈ (M1.union M2).accept ↔
      M1.evalFrom s1 x ∈ M1.accept ∨ M2.evalFrom s2 x ∈ M2.accept
s1 : σ1
s2 : σ2
⊢ (M1.union M2).evalFrom (s1, s2) (a :: x) ∈ (M1.union M2).accept ↔
    M1.evalFrom s1 (a :: x) ∈ M1.accept ∨ M2.evalFrom s2 (a :: x) ∈ M2.accept

Tactic:
simp only [evalFrom_cons, union_step, ih]

Premises used: DFA.union_step, DFA.evalFrom_cons
-- Module: Mathlib.Computability.DFA
Goal:
α : Type u
σ1 σ2 : Type v
M1 : DFA α σ1
M2 : DFA α σ2
s1 : σ1
s2 : σ2
x : List α
h :
  ∀ (s1 : σ1) (s2 : σ2),
    (M1.union M2).evalFrom (s1, s2) [] ∈ (M1.union M2).accept ↔
      M1.evalFrom s1 [] ∈ M1.accept ∨ M2.evalFrom s2 [] ∈ M2.accept
h₁ :
  ∀ (a : α) (x : List α)
    (ih :
      ∀ (s1 : σ1) (s2 : σ2),
        (M1.union M2).evalFrom (s1, s2) x ∈ (M1.union M2).accept ↔
          M1.evalFrom s1 x ∈ M1.accept ∨ M2.evalFrom s2 x ∈ M2.accept)
    (s1 : σ1) (s2 : σ2),
    (M1.union M2).evalFrom (s1, s2) (a :: x) ∈ (M1.union M2).accept ↔
      M1.evalFrom s1 (a :: x) ∈ M1.accept ∨ M2.evalFrom s2 (a :: x) ∈ M2.accept
⊢ (M1.union M2).evalFrom (s1, s2) x ∈ (M1.union M2).accept ↔ M1.evalFrom s1 x ∈ M1.accept ∨ M2.evalFrom s2 x ∈ M2.accept

Tactic:
induction x generalizing s1 s2 with
  | nil => simp
  | cons a x ih => simp only [evalFrom_cons, union_step, ih]

Premises used: DFA.union_step, DFA.evalFrom_cons
-- Module: Mathlib.Computability.DFA
Goal:
α : Type u
σ1 σ2 : Type v
M1 : DFA α σ1
M2 : DFA α σ2
⊢ (M1.union M2).accepts = M1.accepts + M2.accepts

Tactic:
simp [accepts]

Premises used: DFA.accepts
-- Module: Mathlib.Computability.DFA
Goal:
α : Type u
σ1 σ2 : Type v
M1 : DFA α σ1
M2 : DFA α σ2
s1 : σ1
s2 : σ2
h : ∀ (x : List α), x ∈ (M1.inter M2).acceptsFrom (s1, s2) ↔ x ∈ M1.acceptsFrom s1 ⊓ M2.acceptsFrom s2
⊢ (M1.inter M2).acceptsFrom (s1, s2) = M1.acceptsFrom s1 ⊓ M2.acceptsFrom s2

Tactic:
ext x
-- Module: Mathlib.Computability.DFA
Goal:
α : Type u
σ1 σ2 : Type v
M1 : DFA α σ1
M2 : DFA α σ2
s1 : σ1
s2 : σ2
x : List α
h :
  (M1.inter M2).evalFrom (s1, s2) x ∈ (M1.inter M2).accept ↔ M1.evalFrom s1 x ∈ M1.accept ∧ M2.evalFrom s2 x ∈ M2.accept
⊢ Membership.mem (γ := Language α) {x : List α | (M1.inter M2).evalFrom (s1, s2) x ∈ (M1.inter M2).accept} x ↔
    Membership.mem (γ := Language α) {x : List α | M1.evalFrom s1 x ∈ M1.accept} x ∧
      Membership.mem (γ := Language α) {x : List α | M2.evalFrom s2 x ∈ M2.accept} x

Tactic:
simp_rw [↑Set.mem_setOf]

Premises used: Set.mem_setOf
-- Module: Mathlib.Computability.DFA
Goal:
α : Type u
σ1 σ2 : Type v
M1 : DFA α σ1
M2 : DFA α σ2
s1 : σ1
s2 : σ2
⊢ (M1.inter M2).evalFrom (s1, s2) [] ∈ (M1.inter M2).accept ↔
    M1.evalFrom s1 [] ∈ M1.accept ∧ M2.evalFrom s2 [] ∈ M2.accept

Tactic:
simp
-- Module: Mathlib.Computability.DFA
Goal:
α : Type u
σ1 σ2 : Type v
M1 : DFA α σ1
M2 : DFA α σ2
a : α
x : List α
ih :
  ∀ (s1 : σ1) (s2 : σ2),
    (M1.inter M2).evalFrom (s1, s2) x ∈ (M1.inter M2).accept ↔
      M1.evalFrom s1 x ∈ M1.accept ∧ M2.evalFrom s2 x ∈ M2.accept
s1 : σ1
s2 : σ2
⊢ (M1.inter M2).evalFrom (s1, s2) (a :: x) ∈ (M1.inter M2).accept ↔
    M1.evalFrom s1 (a :: x) ∈ M1.accept ∧ M2.evalFrom s2 (a :: x) ∈ M2.accept

Tactic:
simp only [evalFrom_cons, inter_step, ih]

Premises used: DFA.evalFrom_cons, DFA.inter_step
-- Module: Mathlib.Computability.DFA
Goal:
α : Type u
σ1 σ2 : Type v
M1 : DFA α σ1
M2 : DFA α σ2
s1 : σ1
s2 : σ2
x : List α
h :
  ∀ (s1 : σ1) (s2 : σ2),
    (M1.inter M2).evalFrom (s1, s2) [] ∈ (M1.inter M2).accept ↔
      M1.evalFrom s1 [] ∈ M1.accept ∧ M2.evalFrom s2 [] ∈ M2.accept
h₁ :
  ∀ (a : α) (x : List α)
    (ih :
      ∀ (s1 : σ1) (s2 : σ2),
        (M1.inter M2).evalFrom (s1, s2) x ∈ (M1.inter M2).accept ↔
          M1.evalFrom s1 x ∈ M1.accept ∧ M2.evalFrom s2 x ∈ M2.accept)
    (s1 : σ1) (s2 : σ2),
    (M1.inter M2).evalFrom (s1, s2) (a :: x) ∈ (M1.inter M2).accept ↔
      M1.evalFrom s1 (a :: x) ∈ M1.accept ∧ M2.evalFrom s2 (a :: x) ∈ M2.accept
⊢ (M1.inter M2).evalFrom (s1, s2) x ∈ (M1.inter M2).accept ↔ M1.evalFrom s1 x ∈ M1.accept ∧ M2.evalFrom s2 x ∈ M2.accept

Tactic:
induction x generalizing s1 s2 with
  | nil => simp
  | cons a x ih => simp only [evalFrom_cons, inter_step, ih]

Premises used: DFA.evalFrom_cons, DFA.inter_step
-- Module: Mathlib.Computability.DFA
Goal:
α : Type u
σ1 σ2 : Type v
M1 : DFA α σ1
M2 : DFA α σ2
⊢ (M1.inter M2).accepts = M1.accepts ⊓ M2.accepts

Tactic:
simp [accepts]

Premises used: DFA.accepts
-- Module: Mathlib.Computability.DFA
Goal:
T : Type u
L : Language T
hL : ∃ (σ : Type v) (x : Fintype σ) (M : DFA T σ), M.accepts = L
⊢ ∃ (σ' : Type v') (x : Fintype σ') (M : DFA T σ'), M.accepts = L

Tactic:
have ⟨σ, _, M, hM⟩ := hL
  have ⟨σ', ⟨f⟩⟩ := Small.equiv_small.{v', v} (α := σ)
  ⟨σ', Fintype.ofEquiv σ f, M.reindex f, hM ▸ DFA.accepts_reindex M f⟩

Premises used: Small.equiv_small, Exists, DFA.reindex, Eq.rec, Fintype.ofEquiv, _private.0.Language.isRegular_iff.helper.match_2, DFA.accepts, Exists.intro, DFA.accepts_reindex, _private.0.Language.isRegular_iff.helper.match_1, Eq, DFunLike.coe
-- Module: Mathlib.Computability.DFA
Goal:
T : Type u
L : Language T
⊢ L.IsRegular ↔ ∃ (σ : Type v) (x : Fintype σ) (M : DFA T σ), M.accepts = L

Tactic:
⟨Language.isRegular_iff.helper, Language.isRegular_iff.helper⟩

Premises used: _private.0.Language.isRegular_iff.helper, Iff.intro
-- Module: Mathlib.Computability.DFA
Goal:
T : Type u
L : Language T
h : L.IsRegular
σ : Type
w : Fintype σ
M : DFA T σ
hM : M.accepts = L
⊢ Mᶜ.accepts = Lᶜ

Tactic:
simp [hM]
-- Module: Mathlib.Computability.DFA
Goal:
T : Type u
L : Language T
h : Lᶜ.IsRegular
⊢ L.IsRegular

Tactic:
L.compl_compl ▸ h.compl

Premises used: Eq.rec, Language.IsRegular.compl, Language.compl_compl
-- Module: Mathlib.Computability.DFA
Goal:
T : Type u
L : Language T
⊢ Lᶜ.IsRegular ↔ L.IsRegular

Tactic:
⟨.of_compl, .compl⟩

Premises used: Language.IsRegular.of_compl, Language.IsRegular.compl, Iff.intro
-- Module: Mathlib.Computability.DFA
Goal:
T : Type u
L1 L2 : Language T
h1 : L1.IsRegular
h2 : L2.IsRegular
σ1 : Type
w : Fintype σ1
M1 : DFA T σ1
hM1 : M1.accepts = L1
σ2 : Type
w_1 : Fintype σ2
M2 : DFA T σ2
hM2 : M2.accepts = L2
⊢ (M1.union M2).accepts = L1 + L2

Tactic:
simp [hM1, hM2]
-- Module: Mathlib.Computability.DFA
Goal:
T : Type u
L1 L2 : Language T
h1 : L1.IsRegular
h2 : L2.IsRegular
σ1 : Type
w : Fintype σ1
M1 : DFA T σ1
hM1 : M1.accepts = L1
σ2 : Type
w_1 : Fintype σ2
M2 : DFA T σ2
hM2 : M2.accepts = L2
⊢ (M1.inter M2).accepts = L1 ⊓ L2

Tactic:
simp [hM1, hM2]
-- Module: Mathlib.Computability.Encoding
Goal:
α : Type u
e : Encoding.{u, u_1} α
⊢ Function.Injective e.encode

Tactic:
fun _ _ h => Option.some_injective _ ?_

Premises used: Option.some_injective, Function.Injective
-- Module: Mathlib.Computability.Encoding
Goal:
α : Type u
e : Encoding.{u, u_1} α
refine : ∀ (x x_1 : α) (h : e.encode x = e.encode x_1), some x = some x_1
⊢ Function.Injective e.encode

Tactic:
refine fun _ _ h => Option.some_injective _ ?_

Premises used: Option.some_injective
-- Module: Mathlib.Computability.Encoding
Goal:
α : Type u
e : Encoding.{u, u_1} α
x x_1 : α
h : e.encode x = e.encode x_1
rw : e.decode (e.encode x) = some x_1
rw₁ : e.decode (e.encode x) = e.decode (e.encode x_1)
rw₂ rw₃ : e.decode (e.encode x_1) = e.decode (e.encode x_1)
⊢ some x = some x_1

Tactic:
rw [← e.decode_encode, ← e.decode_encode, h]

Premises used: Computability.Encoding.decode_encode
-- Module: Mathlib.Computability.Encoding
Goal:
b : Bool
false : sectionΓ'Bool (inclusionBoolΓ' Bool.false) = Bool.false
true : sectionΓ'Bool (inclusionBoolΓ' Bool.true) = Bool.true
⊢ sectionΓ'Bool (inclusionBoolΓ' b) = b

Tactic:
cases b
-- Module: Mathlib.Computability.Encoding
Goal:
⊢ sectionΓ'Bool (inclusionBoolΓ' false) = false

Tactic:
rfl
-- Module: Mathlib.Computability.Encoding
Goal:
⊢ sectionΓ'Bool (inclusionBoolΓ' true) = true

Tactic:
rfl
-- Module: Mathlib.Computability.Encoding
Goal:
⊢ Function.Injective inclusionBoolΓ'

Tactic:
Function.HasLeftInverse.injective ⟨_, (fun _ => sectionΓ'Bool_inclusionBoolΓ')⟩

Premises used: Computability.sectionΓ'Bool_inclusionBoolΓ', Function.HasLeftInverse.injective, Exists.intro
-- Module: Mathlib.Computability.Encoding
Goal:
n : PosNum
⊢ encodePosNum n ≠ []

Tactic:
PosNum.casesOn n (List.cons_ne_nil _ _) (fun _m => List.cons_ne_nil _ _) fun _m =>
    List.cons_ne_nil _ _

Premises used: PosNum.casesOn
-- Module: Mathlib.Computability.Encoding
Goal:
⊢ (if Eq (α := List Bool) [] [] then PosNum.one else (decodePosNum []).bit1) = PosNum.one

Tactic:
rfl
-- Module: Mathlib.Computability.Encoding
Goal:
m : PosNum
hm : decodePosNum (encodePosNum m) = m
bit1 : (if encodePosNum m = [] then PosNum.one else m.bit1) = m.bit1
⊢ (if encodePosNum m = [] then PosNum.one else (decodePosNum (encodePosNum m)).bit1) = m.bit1

Tactic:
rw [hm]
-- Module: Mathlib.Computability.Encoding
Goal:
m : PosNum
hm : decodePosNum (encodePosNum m) = m
⊢ (if encodePosNum m = [] then PosNum.one else m.bit1) = m.bit1

Tactic:
if_neg (encodePosNum_nonempty m)

Premises used: Computability.encodePosNum_nonempty, if_neg
-- Module: Mathlib.Computability.Encoding
Goal:
m : PosNum
hm : decodePosNum (encodePosNum m) = m
⊢ (if encodePosNum m = [] then PosNum.one else m.bit1) = m.bit1

Tactic:
exact if_neg (encodePosNum_nonempty m)

Premises used: Computability.encodePosNum_nonempty, if_neg
-- Module: Mathlib.Computability.Encoding
Goal:
m : PosNum
hm : decodePosNum (encodePosNum m) = m
⊢ (decodePosNum (encodePosNum m)).bit0 = m.bit0

Tactic:
congr_arg PosNum.bit0 hm

Premises used: congr_arg, PosNum.bit0
-- Module: Mathlib.Computability.Encoding
Goal:
m : PosNum
hm : decodePosNum (encodePosNum m) = m
⊢ (decodePosNum (encodePosNum m)).bit0 = m.bit0

Tactic:
exact congr_arg PosNum.bit0 hm

Premises used: congr_arg, PosNum.bit0
-- Module: Mathlib.Computability.Encoding
Goal:
n : PosNum
one : decodePosNum (encodePosNum PosNum.one) = PosNum.one
one₁ : (if Eq (α := List Bool) [] [] then PosNum.one else (decodePosNum []).bit1) = PosNum.one
bit1 : ∀ (m : PosNum) (hm : decodePosNum (encodePosNum m) = m), decodePosNum (encodePosNum m.bit1) = m.bit1
bit1₁ :
  ∀ (m : PosNum) (hm : decodePosNum (encodePosNum m) = m),
    (if encodePosNum m = [] then PosNum.one else (decodePosNum (encodePosNum m)).bit1) = m.bit1
bit0 : ∀ (m : PosNum) (hm : decodePosNum (encodePosNum m) = m), decodePosNum (encodePosNum m.bit0) = m.bit0
bit0₁ : ∀ (m : PosNum) (hm : decodePosNum (encodePosNum m) = m), (decodePosNum (encodePosNum m)).bit0 = m.bit0
⊢ decodePosNum (encodePosNum n) = n

Tactic:
induction n with unfold encodePosNum decodePosNum
  | one => rfl
  | bit1 m hm =>
    rw [hm]
    exact if_neg (encodePosNum_nonempty m)
  | bit0 m hm => exact congr_arg PosNum.bit0 hm

Premises used: Computability.decodePosNum, Computability.encodePosNum
-- Module: Mathlib.Computability.Encoding
Goal:
n : Num
zero : decodeNum (encodeNum Num.zero) = Num.zero
pos : ∀ (n : PosNum), decodeNum (encodeNum (Num.pos n)) = Num.pos n
⊢ decodeNum (encodeNum n) = n

Tactic:
obtain - | n := n
-- Module: Mathlib.Computability.Encoding
Goal:
⊢ (if
        Eq (α := List Bool)
          (match (motive := Num → List Bool) Num.zero with
            | Num.zero => []
            | Num.pos n => encodePosNum n :
            List Bool)
          ([] : List Bool) then
      Num.zero
    else
      (↑(decodePosNum
            (match (motive := Num → List Bool) Num.zero with
            | Num.zero => []
            | Num.pos n => encodePosNum n)) :
        Num)) =
    Num.zero

Tactic:
rfl
-- Module: Mathlib.Computability.Encoding
Goal:
n : PosNum
pos :
  (if
        Eq (α := List Bool)
          (match (motive := Num → List Bool) Num.pos n with
            | Num.zero => []
            | Num.pos n => encodePosNum n :
            List Bool)
          ([] : List Bool) then
      Num.zero
    else (↑n : Num)) =
    Num.pos n
⊢ (if
        Eq (α := List Bool)
          (match (motive := Num → List Bool) Num.pos n with
            | Num.zero => []
            | Num.pos n => encodePosNum n :
            List Bool)
          ([] : List Bool) then
      Num.zero
    else
      (↑(decodePosNum
            (match (motive := Num → List Bool) Num.pos n with
            | Num.zero => []
            | Num.pos n => encodePosNum n)) :
        Num)) =
    Num.pos n

Tactic:
rw [decode_encodePosNum n]

Premises used: Computability.decode_encodePosNum
-- Module: Mathlib.Computability.Encoding
Goal:
n : PosNum
pos :
  (if
        Eq (α := List Bool)
          (match (motive := Num → List Bool) Num.pos n with
            | Num.zero => []
            | Num.pos n => encodePosNum n :
            List Bool)
          ([] : List Bool) then
      Num.zero
    else Num.pos n) =
    Num.pos n
⊢ (if
        Eq (α := List Bool)
          (match (motive := Num → List Bool) Num.pos n with
            | Num.zero => []
            | Num.pos n => encodePosNum n :
            List Bool)
          ([] : List Bool) then
      Num.zero
    else (↑n : Num)) =
    Num.pos n

Tactic:
rw [PosNum.cast_to_num]

Premises used: PosNum.cast_to_num
-- Module: Mathlib.Computability.Encoding
Goal:
n : PosNum
⊢ (if
        Eq (α := List Bool)
          (match (motive := Num → List Bool) Num.pos n with
            | Num.zero => []
            | Num.pos n => encodePosNum n :
            List Bool)
          ([] : List Bool) then
      Num.zero
    else Num.pos n) =
    Num.pos n

Tactic:
if_neg (encodePosNum_nonempty n)

Premises used: Computability.encodePosNum_nonempty, if_neg
-- Module: Mathlib.Computability.Encoding
Goal:
n : PosNum
⊢ (if
        Eq (α := List Bool)
          (match (motive := Num → List Bool) Num.pos n with
            | Num.zero => []
            | Num.pos n => encodePosNum n :
            List Bool)
          ([] : List Bool) then
      Num.zero
    else Num.pos n) =
    Num.pos n

Tactic:
exact if_neg (encodePosNum_nonempty n)

Premises used: Computability.encodePosNum_nonempty, if_neg
-- Module: Mathlib.Computability.Encoding
Goal:
n : ℕ
rw : (↑(↑n : Num) : ℕ)
| n

Tactic:
rw [← Num.to_of_nat n]

Premises used: Num.to_of_nat
-- Module: Mathlib.Computability.Encoding
Goal:
n : ℕ
conv_rhs : decodeNat (encodeNat n) = (↑(↑n : Num) : ℕ)
⊢ decodeNat (encodeNat n) = n

Tactic:
conv_rhs => rw [← Num.to_of_nat n]

Premises used: Num.to_of_nat
-- Module: Mathlib.Computability.Encoding
Goal:
n : ℕ
⊢ decodeNat (encodeNat n) = (↑(↑n : Num) : ℕ)

Tactic:
congr_arg ((↑) : Num → ℕ) (decode_encodeNum n)

Premises used: Computability.decodeNat, Nat.cast, congr_arg, castNum, Computability.decode_encodeNum
-- Module: Mathlib.Computability.Encoding
Goal:
n : ℕ
⊢ decodeNat (encodeNat n) = (↑(↑n : Num) : ℕ)

Tactic:
exact congr_arg ((↑) : Num → ℕ) (decode_encodeNum n)

Premises used: Nat.cast, congr_arg, castNum, Computability.decode_encodeNum
-- Module: Mathlib.Computability.Encoding
Goal:
x : ℕ
⊢ decodeNat (List.map sectionΓ'Bool (List.map inclusionBoolΓ' (encodeNat x))) = x

Tactic:
simp [Function.comp_def]

Premises used: Function.comp_def
-- Module: Mathlib.Computability.Encoding
Goal:
⊢ ∀ (n : ℕ), unaryDecodeNat (unaryEncodeNat n) = n

Tactic:
fun n =>
  Nat.rec rfl (fun (_m : ℕ) hm => (congr_arg Nat.succ hm.symm).symm) n

Premises used: Nat.rec
-- Module: Mathlib.Computability.Encoding
Goal:
b : Bool
⊢ decodeBool (encodeBool b) = b

Tactic:
rfl

Premises used: Computability.decodeBool, rfl