awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Computability.DFA (goal)
Goal:
α : Type u
σ : Type v
M : DFA α σ
inst : Fintype σ
x : List α
hx_1 : x ∈ M.accepts
hlen_1 : Fintype.card σ ≤ x.length
a b c : List α
hx : x = a ++ b ++ c
hlen : a.length + b.length ≤ Fintype.card σ
hnil : b ≠ []
hb : M.evalFrom (M.evalFrom M.start a) b = M.evalFrom M.start a
hc : M.evalFrom (M.evalFrom M.start a) c = M.evalFrom M.start x
⊢ ∃ (a : List α) (b : List α) (c : List α),
    x = a ++ b ++ c ∧
      a.length + b.length ≤ Fintype.card σ ∧ b ≠ [] ∧ HMul.hMul (α := Language α) {a} {b}∗ * {c} ≤ M.accepts
have right : HMul.hMul (α := Language α) {a} {b}∗ * {c} ≤ M.accepts
Tactic: use a, b, c, hx, hlen, hnil
-- Lean 4 proof step from Mathlib.Computability.DFA (hypothesis)
Goal:
α : Type u
σ : Type v
M : DFA α σ
inst : Fintype σ
x : List α
hx_1 : x ∈ M.accepts
hlen_1 : Fintype.card σ ≤ x.length
a b c : List α
hx : x = a ++ b ++ c
hlen : a.length + b.length ≤ Fintype.card σ
hnil : b ≠ []
hb : M.evalFrom (M.evalFrom M.start a) b = M.evalFrom M.start a
hc : M.evalFrom (M.evalFrom M.start a) c = M.evalFrom M.start x
y : List α
hy : y ∈ HMul.hMul (α := Language α) {a} {b}∗ * {c}
⊢ y ∈ M.accepts
have hy₁ : ∃ a_1 ∈ HMul.hMul (α := Language α) {a} {b}∗, ∃ (b : List α), Membership.mem (γ := Language α) {c} b ∧ a_1 ++ b = y
Tactic: rw [Language.mem_mul] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Computability.DFA (goal)
Goal:
α : Type u
σ : Type v
M : DFA α σ
inst : Fintype σ
x : List α
hx_1 : x ∈ M.accepts
hlen_1 : Fintype.card σ ≤ x.length
a b c : List α
hx : x = a ++ b ++ c
hlen : a.length + b.length ≤ Fintype.card σ
hnil : b ≠ []
hb : M.evalFrom (M.evalFrom M.start a) b = M.evalFrom M.start a
hc : M.evalFrom (M.evalFrom M.start a) c = M.evalFrom M.start x
y : List α
hy : ∃ a_1 ∈ HMul.hMul (α := Language α) {a} {b}∗, ∃ (b : List α), Membership.mem (γ := Language α) {c} b ∧ a_1 ++ b = y
⊢ y ∈ M.accepts
have right : ∀ (ab : List α) (hab : ab ∈ HMul.hMul (α := Language α) {a} {b}∗) (c' : List α)
  (hc' : Membership.mem (γ := Language α) {c} c'), ab ++ c' ∈ M.accepts
Tactic: rcases hy with ⟨ab, hab, c', hc', rfl⟩
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.Computability.DFA (goal)
Goal:
α : Type u
σ : Type v
M : DFA α σ
inst : Fintype σ
x : List α
hx_1 : x ∈ M.accepts
hlen_1 : Fintype.card σ ≤ x.length
a b c : List α
hx : x = a ++ b ++ c
hlen : a.length + b.length ≤ Fintype.card σ
hnil : b ≠ []
hb : M.evalFrom (M.evalFrom M.start a) b = M.evalFrom M.start a
hc : M.evalFrom (M.evalFrom M.start a) c = M.evalFrom M.start x
ab : List α
hab : ab ∈ HMul.hMul (α := Language α) {a} {b}∗
c' : List α
hc' : Membership.mem (γ := Language α) {c} c'
⊢ ab ++ c' ∈ M.accepts
have right : ∀
  (hab :
    ∃ (a_1 : List α),
      Membership.mem (γ := Language α) {a} a_1 ∧
        ∃ (b_1 : List α), Membership.mem (γ := Language α) {b}∗ b_1 ∧ a_1 ++ b_1 = ab)
  (c' : List α) (hc' : Membership.mem (γ := Language α) {c} c'), ab ++ c' ∈ M.accepts
Tactic: rw [Language.mem_mul] at hab
Cleared hypotheses: hab, c', hc'
-- Lean 4 proof step from Mathlib.Computability.DFA (goal)
Goal:
α : Type u
σ : Type v
M : DFA α σ
inst : Fintype σ
x : List α
hx_1 : x ∈ M.accepts
hlen_1 : Fintype.card σ ≤ x.length
a b c : List α
hx : x = a ++ b ++ c
hlen : a.length + b.length ≤ Fintype.card σ
hnil : b ≠ []
hb : M.evalFrom (M.evalFrom M.start a) b = M.evalFrom M.start a
hc : M.evalFrom (M.evalFrom M.start a) c = M.evalFrom M.start x
ab : List α
hab :
  ∃ (a_1 : List α),
    Membership.mem (γ := Language α) {a} a_1 ∧
      ∃ (b_1 : List α), Membership.mem (γ := Language α) {b}∗ b_1 ∧ a_1 ++ b_1 = ab
c' : List α
hc' : Membership.mem (γ := Language α) {c} c'
⊢ ab ++ c' ∈ M.accepts
have right : ∀ (a' : List α) (ha' : Membership.mem (γ := Language α) {a} a') (b' : List α)
  (hb' : Membership.mem (γ := Language α) {b}∗ b'), a' ++ b' ++ c' ∈ M.accepts
Tactic: rcases hab with ⟨a', ha', b', hb', rfl⟩
Cleared hypotheses: ab, hab
-- Lean 4 proof step from Mathlib.Computability.DFA (goal)
Goal:
α : Type u
σ : Type v
M : DFA α σ
inst : Fintype σ
x : List α
hx_1 : x ∈ M.accepts
hlen_1 : Fintype.card σ ≤ x.length
a b c : List α
hx : x = a ++ b ++ c
hlen : a.length + b.length ≤ Fintype.card σ
hnil : b ≠ []
hb : M.evalFrom (M.evalFrom M.start a) b = M.evalFrom M.start a
hc : M.evalFrom (M.evalFrom M.start a) c = M.evalFrom M.start x
c' : List α
hc' : Membership.mem (γ := Language α) {c} c'
a' : List α
ha' : Membership.mem (γ := Language α) {a} a'
b' : List α
hb' : Membership.mem (γ := Language α) {b}∗ b'
⊢ a' ++ b' ++ c' ∈ M.accepts
have right : ∀ (hc' : c' = c) (a' : List α) (ha' : a' = a) (b' : List α) (hb' : Membership.mem (γ := Language α) {b}∗ b'),
  a' ++ b' ++ c' ∈ M.accepts
Tactic: rw [Set.mem_singleton_iff] at ha' hc'
Cleared hypotheses: hc', a', ha', b', hb'
-- Lean 4 proof step from Mathlib.Computability.DFA (hypothesis)
Goal:
α : Type u
σ : Type v
M : DFA α σ
inst : Fintype σ
x : List α
hx_1 : x ∈ M.accepts
hlen_1 : Fintype.card σ ≤ x.length
a b c : List α
hx : x = a ++ b ++ c
hlen : a.length + b.length ≤ Fintype.card σ
hnil : b ≠ []
hb : M.evalFrom (M.evalFrom M.start a) b = M.evalFrom M.start a
hc : M.evalFrom (M.evalFrom M.start a) c = M.evalFrom M.start x
c' : List α
hc' : c' = c
a' : List α
ha' : a' = a
b' : List α
hb' : Membership.mem (γ := Language α) {b}∗ b'
⊢ a' ++ b' ++ c' ∈ M.accepts
have hlen₁ : a'.length + b.length ≤ Fintype.card σ
Tactic: substs ha' hc'
Cleared hypotheses: a, c, hx, hlen, hb, hc, hc', ha'
-- Lean 4 proof step from Mathlib.Computability.DFA (hypothesis)
Goal:
α : Type u
σ : Type v
M : DFA α σ
inst : Fintype σ
x : List α
hx_1 : x ∈ M.accepts
hlen_1 : Fintype.card σ ≤ x.length
a b c : List α
hx : x = a ++ b ++ c
hlen : a.length + b.length ≤ Fintype.card σ
hnil : b ≠ []
hb : M.evalFrom (M.evalFrom M.start a) b = M.evalFrom M.start a
hc : M.evalFrom (M.evalFrom M.start a) c = M.evalFrom M.start x
c' : List α
hc' : c' = c
a' : List α
ha' : a' = a
b' : List α
hb' : Membership.mem (γ := Language α) {b}∗ b'
hlen₁ : a'.length + b.length ≤ Fintype.card σ
⊢ a' ++ b' ++ c' ∈ M.accepts
have hb₁ : M.evalFrom (M.evalFrom M.start a') b = M.evalFrom M.start a'
Tactic: substs ha' hc'
Cleared hypotheses: a, c, hx, hlen, hb, hc, hc', ha'
-- Lean 4 proof step from Mathlib.Computability.DFA (hypothesis)
Goal:
α : Type u
σ : Type v
M : DFA α σ
inst : Fintype σ
x : List α
hx_1 : x ∈ M.accepts
hlen_1 : Fintype.card σ ≤ x.length
a b c : List α
hx : x = a ++ b ++ c
hlen : a.length + b.length ≤ Fintype.card σ
hnil : b ≠ []
hb : M.evalFrom (M.evalFrom M.start a) b = M.evalFrom M.start a
hc : M.evalFrom (M.evalFrom M.start a) c = M.evalFrom M.start x
c' : List α
hc' : c' = c
a' : List α
ha' : a' = a
b' : List α
hb' : Membership.mem (γ := Language α) {b}∗ b'
hlen₁ : a'.length + b.length ≤ Fintype.card σ
hb₁ : M.evalFrom (M.evalFrom M.start a') b = M.evalFrom M.start a'
⊢ a' ++ b' ++ c' ∈ M.accepts
have hx₁ : x = a' ++ b ++ c'
Tactic: substs ha' hc'
Cleared hypotheses: a, c, hx, hlen, hb, hc, hc', ha'
-- Lean 4 proof step from Mathlib.Computability.DFA (hypothesis)
Goal:
α : Type u
σ : Type v
M : DFA α σ
inst : Fintype σ
x : List α
hx_1 : x ∈ M.accepts
hlen_1 : Fintype.card σ ≤ x.length
a b c : List α
hx : x = a ++ b ++ c
hlen : a.length + b.length ≤ Fintype.card σ
hnil : b ≠ []
hb : M.evalFrom (M.evalFrom M.start a) b = M.evalFrom M.start a
hc : M.evalFrom (M.evalFrom M.start a) c = M.evalFrom M.start x
c' : List α
hc' : c' = c
a' : List α
ha' : a' = a
b' : List α
hb' : Membership.mem (γ := Language α) {b}∗ b'
hlen₁ : a'.length + b.length ≤ Fintype.card σ
hb₁ : M.evalFrom (M.evalFrom M.start a') b = M.evalFrom M.start a'
hx₁ : x = a' ++ b ++ c'
⊢ a' ++ b' ++ c' ∈ M.accepts
have hc₁ : M.evalFrom (M.evalFrom M.start a') c' = M.evalFrom M.start x
Tactic: substs ha' hc'
Cleared hypotheses: a, c, hx, hlen, hb, hc, hc', ha'
-- Lean 4 proof step from Mathlib.Computability.DFA (hypothesis)
Goal:
α : Type u
σ : Type v
M : DFA α σ
inst : Fintype σ
x : List α
hx_1 : x ∈ M.accepts
hlen_1 : Fintype.card σ ≤ x.length
b : List α
hnil : b ≠ []
c' a' b' : List α
hb' : Membership.mem (γ := Language α) {b}∗ b'
hlen : a'.length + b.length ≤ Fintype.card σ
hb : M.evalFrom (M.evalFrom M.start a') b = M.evalFrom M.start a'
hx : x = a' ++ b ++ c'
hc : M.evalFrom (M.evalFrom M.start a') c' = M.evalFrom M.start x
⊢ a' ++ b' ++ c' ∈ M.accepts
have h : M.evalFrom (M.evalFrom M.start a') b' = M.evalFrom M.start a'
Tactic: have h := M.evalFrom_of_pow hb hb'
-- Lean 4 proof step from Mathlib.Computability.DFA (goal)
Goal:
α : Type u
σ : Type v
M : DFA α σ
inst : Fintype σ
x : List α
hx_1 : x ∈ M.accepts
hlen_1 : Fintype.card σ ≤ x.length
b : List α
hnil : b ≠ []
c' a' b' : List α
hb' : Membership.mem (γ := Language α) {b}∗ b'
hlen : a'.length + b.length ≤ Fintype.card σ
hb : M.evalFrom (M.evalFrom M.start a') b = M.evalFrom M.start a'
hx : x = a' ++ b ++ c'
hc : M.evalFrom (M.evalFrom M.start a') c' = M.evalFrom M.start x
h : M.evalFrom (M.evalFrom M.start a') b' = M.evalFrom M.start a'
⊢ a' ++ b' ++ c' ∈ M.accepts
have right : M.eval (a' ++ b' ++ c') ∈ M.accept
Tactic: rwa [mem_accepts, eval, evalFrom_of_append, evalFrom_of_append, h, hc]
-- Lean 4 proof step from Mathlib.Computability.DFA (goal)
Goal:
α : Type u
σ : Type v
M : DFA α σ
inst : Fintype σ
x : List α
hx_1 : x ∈ M.accepts
hlen_1 : Fintype.card σ ≤ x.length
b : List α
hnil : b ≠ []
c' a' b' : List α
hb' : Membership.mem (γ := Language α) {b}∗ b'
hlen : a'.length + b.length ≤ Fintype.card σ
hb : M.evalFrom (M.evalFrom M.start a') b = M.evalFrom M.start a'
hx : x = a' ++ b ++ c'
hc : M.evalFrom (M.evalFrom M.start a') c' = M.evalFrom M.start x
h : M.evalFrom (M.evalFrom M.start a') b' = M.evalFrom M.start a'
right : M.eval (a' ++ b' ++ c') ∈ M.accept
⊢ a' ++ b' ++ c' ∈ M.accepts
have right₁ : M.evalFrom M.start (a' ++ b' ++ c') ∈ M.accept
Tactic: rwa [mem_accepts, eval, evalFrom_of_append, evalFrom_of_append, h, hc]
-- Lean 4 proof step from Mathlib.Computability.DFA (goal)
Goal:
α : Type u
σ : Type v
M : DFA α σ
inst : Fintype σ
x : List α
hx_1 : x ∈ M.accepts
hlen_1 : Fintype.card σ ≤ x.length
b : List α
hnil : b ≠ []
c' a' b' : List α
hb' : Membership.mem (γ := Language α) {b}∗ b'
hlen : a'.length + b.length ≤ Fintype.card σ
hb : M.evalFrom (M.evalFrom M.start a') b = M.evalFrom M.start a'
hx : x = a' ++ b ++ c'
hc : M.evalFrom (M.evalFrom M.start a') c' = M.evalFrom M.start x
h : M.evalFrom (M.evalFrom M.start a') b' = M.evalFrom M.start a'
right : M.eval (a' ++ b' ++ c') ∈ M.accept
right₁ : M.evalFrom M.start (a' ++ b' ++ c') ∈ M.accept
⊢ a' ++ b' ++ c' ∈ M.accepts
have right₂ : M.evalFrom (M.evalFrom M.start (a' ++ b')) c' ∈ M.accept
Tactic: rwa [mem_accepts, eval, evalFrom_of_append, evalFrom_of_append, h, hc]
-- Lean 4 proof step from Mathlib.Computability.DFA (goal)
Goal:
α : Type u
σ : Type v
M : DFA α σ
inst : Fintype σ
x : List α
hx_1 : x ∈ M.accepts
hlen_1 : Fintype.card σ ≤ x.length
b : List α
hnil : b ≠ []
c' a' b' : List α
hb' : Membership.mem (γ := Language α) {b}∗ b'
hlen : a'.length + b.length ≤ Fintype.card σ
hb : M.evalFrom (M.evalFrom M.start a') b = M.evalFrom M.start a'
hx : x = a' ++ b ++ c'
hc : M.evalFrom (M.evalFrom M.start a') c' = M.evalFrom M.start x
h : M.evalFrom (M.evalFrom M.start a') b' = M.evalFrom M.start a'
right : M.eval (a' ++ b' ++ c') ∈ M.accept
right₁ : M.evalFrom M.start (a' ++ b' ++ c') ∈ M.accept
right₂ : M.evalFrom (M.evalFrom M.start (a' ++ b')) c' ∈ M.accept
⊢ a' ++ b' ++ c' ∈ M.accepts
have right₃ : M.evalFrom (M.evalFrom (M.evalFrom M.start a') b') c' ∈ M.accept
Tactic: rwa [mem_accepts, eval, evalFrom_of_append, evalFrom_of_append, h, hc]
-- Lean 4 proof step from Mathlib.Computability.DFA (goal)
Goal:
α : Type u
σ : Type v
M : DFA α σ
inst : Fintype σ
x : List α
hx_1 : x ∈ M.accepts
hlen_1 : Fintype.card σ ≤ x.length
b : List α
hnil : b ≠ []
c' a' b' : List α
hb' : Membership.mem (γ := Language α) {b}∗ b'
hlen : a'.length + b.length ≤ Fintype.card σ
hb : M.evalFrom (M.evalFrom M.start a') b = M.evalFrom M.start a'
hx : x = a' ++ b ++ c'
hc : M.evalFrom (M.evalFrom M.start a') c' = M.evalFrom M.start x
h : M.evalFrom (M.evalFrom M.start a') b' = M.evalFrom M.start a'
right : M.eval (a' ++ b' ++ c') ∈ M.accept
right₁ : M.evalFrom M.start (a' ++ b' ++ c') ∈ M.accept
right₂ : M.evalFrom (M.evalFrom M.start (a' ++ b')) c' ∈ M.accept
right₃ : M.evalFrom (M.evalFrom (M.evalFrom M.start a') b') c' ∈ M.accept
⊢ a' ++ b' ++ c' ∈ M.accepts
have right₄ : M.evalFrom (M.evalFrom M.start a') c' ∈ M.accept
Tactic: rwa [mem_accepts, eval, evalFrom_of_append, evalFrom_of_append, h, hc]
-- Lean 4 proof step from Mathlib.Computability.DFA (goal)
Goal:
α : Type u
σ : Type v
M : DFA α σ
inst : Fintype σ
x : List α
hx_1 : x ∈ M.accepts
hlen_1 : Fintype.card σ ≤ x.length
b : List α
hnil : b ≠ []
c' a' b' : List α
hb' : Membership.mem (γ := Language α) {b}∗ b'
hlen : a'.length + b.length ≤ Fintype.card σ
hb : M.evalFrom (M.evalFrom M.start a') b = M.evalFrom M.start a'
hx : x = a' ++ b ++ c'
hc : M.evalFrom (M.evalFrom M.start a') c' = M.evalFrom M.start x
h : M.evalFrom (M.evalFrom M.start a') b' = M.evalFrom M.start a'
right : M.eval (a' ++ b' ++ c') ∈ M.accept
right₁ : M.evalFrom M.start (a' ++ b' ++ c') ∈ M.accept
right₂ : M.evalFrom (M.evalFrom M.start (a' ++ b')) c' ∈ M.accept
right₃ : M.evalFrom (M.evalFrom (M.evalFrom M.start a') b') c' ∈ M.accept
right₄ : M.evalFrom (M.evalFrom M.start a') c' ∈ M.accept
⊢ a' ++ b' ++ c' ∈ M.accepts
have right₅ : M.evalFrom M.start x ∈ M.accept
Tactic: rwa [mem_accepts, eval, evalFrom_of_append, evalFrom_of_append, h, hc]
-- Lean 4 proof step from Mathlib.Computability.DFA (goal)
Goal:
α : Type u
σ : Type v
M : DFA α σ
α' : Type u_1
f : α' → α
s : σ
x : List α'
⊢ (comap f M).evalFrom s x = M.evalFrom s (List.map f x)
have nil : (comap f M).evalFrom s [] = M.evalFrom s (List.map f [])
Tactic: induction x using List.reverseRecOn with
  | nil => simp
  | append_singleton x a ih => simp [ih]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Computability.DFA (goal)
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 [])
⊢ (comap f M).evalFrom s x = M.evalFrom s (List.map f x)
have 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]))
Tactic: induction x using List.reverseRecOn with
  | nil => simp
  | append_singleton x a ih => simp [ih]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Computability.DFA (goal)
Goal:
α : Type u
σ : Type v
M : DFA α σ
α' : Type u_1
f : α' → α
⊢ (comap f M).accepts = List.map f ⁻¹' M.accepts
have h : ∀ (x : List α'), x ∈ (comap f M).accepts ↔ x ∈ List.map f ⁻¹' M.accepts
Tactic: ext x
-- Lean 4 proof step from Mathlib.Computability.DFA (goal)
Goal:
α : Type u
σ : Type v
M : DFA α σ
α' : Type u_1
f : α' → α
x : List α'
| x ∈ (comap f M).accepts ↔ x ∈ List.map f ⁻¹' M.accepts
have rhs : x ∈ List.map f ⁻¹' M.accepts
Tactic: rhs
-- Lean 4 proof step from Mathlib.Computability.DFA (goal)
Goal:
α : Type u
σ : Type v
M : DFA α σ
α' : Type u_1
f : α' → α
x : List α'
| x ∈ List.map f ⁻¹' M.accepts
have rw : M.eval (List.map f x) ∈ M.accept
Tactic: rw [Set.mem_preimage, mem_accepts]
-- Lean 4 proof step from Mathlib.Computability.DFA (goal)
Goal:
α : Type u
σ : Type v
M : DFA α σ
α' : Type u_1
f : α' → α
x : List α'
| x ∈ (comap f M).accepts ↔ x ∈ List.map f ⁻¹' M.accepts
have rw : M.eval (List.map f x) ∈ M.accept
Tactic: rhs
    rw [Set.mem_preimage, mem_accepts]
-- Lean 4 proof step from Mathlib.Computability.DFA (goal)
Goal:
α : Type u
σ : Type v
M : DFA α σ
α' : Type u_1
f : α' → α
x : List α'
⊢ x ∈ (comap f M).accepts ↔ x ∈ List.map f ⁻¹' M.accepts
have h : x ∈ (comap f M).accepts ↔ M.eval (List.map f x) ∈ M.accept
Tactic: conv =>
    rhs
    rw [Set.mem_preimage, mem_accepts]
-- Lean 4 proof step from Mathlib.Computability.DFA (goal)
Goal:
α : Type u
σ : Type v
M : DFA α σ
σ' : Type u_2
g : σ ≃ σ'
s : σ'
x : List α
⊢ evalFrom ((reindex g : (a : DFA α σ) → DFA α σ') M) s x =
    (g : (a : σ) → σ') (M.evalFrom ((g.symm : (a : σ') → σ) s) x)
have nil : evalFrom.{u, u_2} (α := α) ((reindex g : (a : DFA α σ) → DFA α σ') M) s [] =
  (g : (a : σ) → σ') (M.evalFrom ((g.symm : (a : σ') → σ) s) [])
Tactic: induction x using List.reverseRecOn with
  | nil => simp
  | append_singleton x a ih => simp [ih]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Computability.DFA (goal)
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) [])
⊢ evalFrom ((reindex g : (a : DFA α σ) → DFA α σ') M) s x =
    (g : (a : σ) → σ') (M.evalFrom ((g.symm : (a : σ') → σ) s) x)
have 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]))
Tactic: induction x using List.reverseRecOn with
  | nil => simp
  | append_singleton x a ih => simp [ih]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Computability.DFA (goal)
Goal:
α : Type u
σ : Type v
M : DFA α σ
σ' : Type u_2
g : σ ≃ σ'
⊢ accepts.{u, u_2} (σ := σ') ((reindex g : (a : DFA α σ) → DFA α σ') M) = M.accepts
have h : ∀ (x : List α),
  Membership.mem (γ := Language α) (accepts.{u, u_2} (σ := σ') ((reindex g : (a : DFA α σ) → DFA α σ') M)) x ↔
    x ∈ M.accepts
Tactic: ext x
-- Lean 4 proof step from Mathlib.Computability.DFA (goal)
Goal:
α : Type u
σ1 σ2 : Type v
M1 : DFA α σ1
M2 : DFA α σ2
s1 : σ1
s2 : σ2
⊢ (M1.union M2).acceptsFrom (s1, s2) = M1.acceptsFrom s1 + M2.acceptsFrom s2
have h : ∀ (x : List α), x ∈ (M1.union M2).acceptsFrom (s1, s2) ↔ x ∈ M1.acceptsFrom s1 + M2.acceptsFrom s2
Tactic: ext x
-- Lean 4 proof step from Mathlib.Computability.DFA (goal)
Goal:
α : Type u
σ1 σ2 : Type v
M1 : DFA α σ1
M2 : DFA α σ2
s1 : σ1
s2 : σ2
x : List α
⊢ 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
have h : (M1.union M2).evalFrom (s1, s2) x ∈ (M1.union M2).accept ↔ M1.evalFrom s1 x ∈ M1.accept ∨ M2.evalFrom s2 x ∈ M2.accept
Tactic: simp_rw [↑Set.mem_setOf]
-- Lean 4 proof step from Mathlib.Computability.DFA (goal)
Goal:
α : Type u
σ1 σ2 : Type v
M1 : DFA α σ1
M2 : DFA α σ2
s1 : σ1
s2 : σ2
x : List α
⊢ (M1.union M2).evalFrom (s1, s2) x ∈ (M1.union M2).accept ↔ M1.evalFrom s1 x ∈ M1.accept ∨ M2.evalFrom s2 x ∈ M2.accept
have 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
Tactic: induction x generalizing s1 s2 with
  | nil => simp
  | cons a x ih => simp only [evalFrom_cons, union_step, ih]
Cleared hypotheses: s1, s2, x
-- Lean 4 proof step from Mathlib.Computability.DFA (goal)
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
⊢ (M1.union M2).evalFrom (s1, s2) x ∈ (M1.union M2).accept ↔ M1.evalFrom s1 x ∈ M1.accept ∨ M2.evalFrom s2 x ∈ M2.accept
have 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
Tactic: induction x generalizing s1 s2 with
  | nil => simp
  | cons a x ih => simp only [evalFrom_cons, union_step, ih]
Cleared hypotheses: s1, s2, x
-- Lean 4 proof step from Mathlib.Computability.DFA (goal)
Goal:
α : Type u
σ1 σ2 : Type v
M1 : DFA α σ1
M2 : DFA α σ2
s1 : σ1
s2 : σ2
⊢ (M1.inter M2).acceptsFrom (s1, s2) = M1.acceptsFrom s1 ⊓ M2.acceptsFrom s2
have h : ∀ (x : List α), x ∈ (M1.inter M2).acceptsFrom (s1, s2) ↔ x ∈ M1.acceptsFrom s1 ⊓ M2.acceptsFrom s2
Tactic: ext x
-- Lean 4 proof step from Mathlib.Computability.DFA (goal)
Goal:
α : Type u
σ1 σ2 : Type v
M1 : DFA α σ1
M2 : DFA α σ2
s1 : σ1
s2 : σ2
x : List α
⊢ 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
have h : (M1.inter M2).evalFrom (s1, s2) x ∈ (M1.inter M2).accept ↔ M1.evalFrom s1 x ∈ M1.accept ∧ M2.evalFrom s2 x ∈ M2.accept
Tactic: simp_rw [↑Set.mem_setOf]
-- Lean 4 proof step from Mathlib.Computability.DFA (goal)
Goal:
α : Type u
σ1 σ2 : Type v
M1 : DFA α σ1
M2 : DFA α σ2
s1 : σ1
s2 : σ2
x : List α
⊢ (M1.inter M2).evalFrom (s1, s2) x ∈ (M1.inter M2).accept ↔ M1.evalFrom s1 x ∈ M1.accept ∧ M2.evalFrom s2 x ∈ M2.accept
have 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
Tactic: induction x generalizing s1 s2 with
  | nil => simp
  | cons a x ih => simp only [evalFrom_cons, inter_step, ih]
Cleared hypotheses: s1, s2, x
-- Lean 4 proof step from Mathlib.Computability.DFA (goal)
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
⊢ (M1.inter M2).evalFrom (s1, s2) x ∈ (M1.inter M2).accept ↔ M1.evalFrom s1 x ∈ M1.accept ∧ M2.evalFrom s2 x ∈ M2.accept
have 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
Tactic: induction x generalizing s1 s2 with
  | nil => simp
  | cons a x ih => simp only [evalFrom_cons, inter_step, ih]
Cleared hypotheses: s1, s2, x
-- Lean 4 proof step from Mathlib.Computability.Encoding (goal)
Goal:
α : Type u
e : Encoding.{u, u_1} α
⊢ Function.Injective e.encode
have refine : ∀ (x x_1 : α) (h : e.encode x = e.encode x_1), some x = some x_1
Tactic: refine fun _ _ h => Option.some_injective _ ?_
-- Lean 4 proof step from Mathlib.Computability.Encoding (goal)
Goal:
α : Type u
e : Encoding.{u, u_1} α
x x_1 : α
h : e.encode x = e.encode x_1
⊢ some x = some x_1
have rw : e.decode (e.encode x) = some x_1
Tactic: rw [← e.decode_encode, ← e.decode_encode, h]
-- Lean 4 proof step from Mathlib.Computability.Encoding (goal)
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
⊢ some x = some x_1
have rw₁ : e.decode (e.encode x) = e.decode (e.encode x_1)
Tactic: rw [← e.decode_encode, ← e.decode_encode, h]
-- Lean 4 proof step from Mathlib.Computability.Encoding (goal)
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)
⊢ some x = some x_1
have rw₂ : e.decode (e.encode x_1) = e.decode (e.encode x_1)
Tactic: rw [← e.decode_encode, ← e.decode_encode, h]
-- Lean 4 proof step from Mathlib.Computability.Encoding (goal)
Goal:
b : Bool
⊢ sectionΓ'Bool (inclusionBoolΓ' b) = b
have false : sectionΓ'Bool (inclusionBoolΓ' false) = false
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Computability.Encoding (goal)
Goal:
b : Bool
false : sectionΓ'Bool (inclusionBoolΓ' Bool.false) = Bool.false
⊢ sectionΓ'Bool (inclusionBoolΓ' b) = b
have true : sectionΓ'Bool (inclusionBoolΓ' true) = true
Tactic: cases b
Cleared hypotheses: b