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 α
s t : σ
hlen : Fintype.card σ ≤ x.length
hx : M.evalFrom s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : M.evalFrom s (List.take (↑n : ℕ) x) = M.evalFrom s (List.take (↑m : ℕ) x)
hle : (↑n : ℕ) ≤ (↑m : ℕ)
⊢ M.evalFrom (M.evalFrom s (List.take (↑n : ℕ) (List.take (↑m : ℕ) x))) (List.drop (↑n : ℕ) (List.take (↑m : ℕ) x)) =
    M.evalFrom s (List.take (↑n : ℕ) (List.take (↑m : ℕ) x))
have rw : M.evalFrom (M.evalFrom s (List.take (min (↑n : ℕ) (↑m : ℕ)) x)) (List.drop (↑n : ℕ) (List.take (↑m : ℕ) x)) =
  M.evalFrom s (List.take (min (↑n : ℕ) (↑m : ℕ)) x)
Tactic: rw [List.take_take, min_eq_left hle, ← evalFrom_of_append, heq, ← min_eq_left hle, ←
      List.take_take, min_eq_left hle, List.take_append_drop]
-- Lean 4 proof step from Mathlib.Computability.DFA (goal)
Goal:
α : Type u
σ : Type v
M : DFA α σ
inst : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ x.length
hx : M.evalFrom s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : M.evalFrom s (List.take (↑n : ℕ) x) = M.evalFrom s (List.take (↑m : ℕ) x)
hle : (↑n : ℕ) ≤ (↑m : ℕ)
rw :
  M.evalFrom (M.evalFrom s (List.take (min (↑n : ℕ) (↑m : ℕ)) x)) (List.drop (↑n : ℕ) (List.take (↑m : ℕ) x)) =
    M.evalFrom s (List.take (min (↑n : ℕ) (↑m : ℕ)) x)
⊢ M.evalFrom (M.evalFrom s (List.take (↑n : ℕ) (List.take (↑m : ℕ) x))) (List.drop (↑n : ℕ) (List.take (↑m : ℕ) x)) =
    M.evalFrom s (List.take (↑n : ℕ) (List.take (↑m : ℕ) x))
have rw₁ : M.evalFrom (M.evalFrom s (List.take (↑n : ℕ) x)) (List.drop (↑n : ℕ) (List.take (↑m : ℕ) x)) =
  M.evalFrom s (List.take (↑n : ℕ) x)
Tactic: rw [List.take_take, min_eq_left hle, ← evalFrom_of_append, heq, ← min_eq_left hle, ←
      List.take_take, min_eq_left hle, List.take_append_drop]
-- Lean 4 proof step from Mathlib.Computability.DFA (goal)
Goal:
α : Type u
σ : Type v
M : DFA α σ
inst : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ x.length
hx : M.evalFrom s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : M.evalFrom s (List.take (↑n : ℕ) x) = M.evalFrom s (List.take (↑m : ℕ) x)
hle : (↑n : ℕ) ≤ (↑m : ℕ)
rw :
  M.evalFrom (M.evalFrom s (List.take (min (↑n : ℕ) (↑m : ℕ)) x)) (List.drop (↑n : ℕ) (List.take (↑m : ℕ) x)) =
    M.evalFrom s (List.take (min (↑n : ℕ) (↑m : ℕ)) x)
rw₁ :
  M.evalFrom (M.evalFrom s (List.take (↑n : ℕ) x)) (List.drop (↑n : ℕ) (List.take (↑m : ℕ) x)) =
    M.evalFrom s (List.take (↑n : ℕ) x)
⊢ M.evalFrom (M.evalFrom s (List.take (↑n : ℕ) (List.take (↑m : ℕ) x))) (List.drop (↑n : ℕ) (List.take (↑m : ℕ) x)) =
    M.evalFrom s (List.take (↑n : ℕ) (List.take (↑m : ℕ) x))
have rw₂ : M.evalFrom s (List.take (↑n : ℕ) x ++ List.drop (↑n : ℕ) (List.take (↑m : ℕ) x)) = M.evalFrom s (List.take (↑n : ℕ) x)
Tactic: rw [List.take_take, min_eq_left hle, ← evalFrom_of_append, heq, ← min_eq_left hle, ←
      List.take_take, min_eq_left hle, List.take_append_drop]
-- Lean 4 proof step from Mathlib.Computability.DFA (goal)
Goal:
α : Type u
σ : Type v
M : DFA α σ
inst : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ x.length
hx : M.evalFrom s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : M.evalFrom s (List.take (↑n : ℕ) x) = M.evalFrom s (List.take (↑m : ℕ) x)
hle : (↑n : ℕ) ≤ (↑m : ℕ)
rw :
  M.evalFrom (M.evalFrom s (List.take (min (↑n : ℕ) (↑m : ℕ)) x)) (List.drop (↑n : ℕ) (List.take (↑m : ℕ) x)) =
    M.evalFrom s (List.take (min (↑n : ℕ) (↑m : ℕ)) x)
rw₁ :
  M.evalFrom (M.evalFrom s (List.take (↑n : ℕ) x)) (List.drop (↑n : ℕ) (List.take (↑m : ℕ) x)) =
    M.evalFrom s (List.take (↑n : ℕ) x)
rw₂ :
  M.evalFrom s (List.take (↑n : ℕ) x ++ List.drop (↑n : ℕ) (List.take (↑m : ℕ) x)) = M.evalFrom s (List.take (↑n : ℕ) x)
⊢ M.evalFrom (M.evalFrom s (List.take (↑n : ℕ) (List.take (↑m : ℕ) x))) (List.drop (↑n : ℕ) (List.take (↑m : ℕ) x)) =
    M.evalFrom s (List.take (↑n : ℕ) (List.take (↑m : ℕ) x))
have rw₃ : M.evalFrom s (List.take (↑n : ℕ) x ++ List.drop (↑n : ℕ) (List.take (↑m : ℕ) x)) = M.evalFrom s (List.take (↑m : ℕ) x)
Tactic: rw [List.take_take, min_eq_left hle, ← evalFrom_of_append, heq, ← min_eq_left hle, ←
      List.take_take, min_eq_left hle, List.take_append_drop]
-- Lean 4 proof step from Mathlib.Computability.DFA (goal)
Goal:
α : Type u
σ : Type v
M : DFA α σ
inst : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ x.length
hx : M.evalFrom s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : M.evalFrom s (List.take (↑n : ℕ) x) = M.evalFrom s (List.take (↑m : ℕ) x)
hle : (↑n : ℕ) ≤ (↑m : ℕ)
rw :
  M.evalFrom (M.evalFrom s (List.take (min (↑n : ℕ) (↑m : ℕ)) x)) (List.drop (↑n : ℕ) (List.take (↑m : ℕ) x)) =
    M.evalFrom s (List.take (min (↑n : ℕ) (↑m : ℕ)) x)
rw₁ :
  M.evalFrom (M.evalFrom s (List.take (↑n : ℕ) x)) (List.drop (↑n : ℕ) (List.take (↑m : ℕ) x)) =
    M.evalFrom s (List.take (↑n : ℕ) x)
rw₂ :
  M.evalFrom s (List.take (↑n : ℕ) x ++ List.drop (↑n : ℕ) (List.take (↑m : ℕ) x)) = M.evalFrom s (List.take (↑n : ℕ) x)
rw₃ :
  M.evalFrom s (List.take (↑n : ℕ) x ++ List.drop (↑n : ℕ) (List.take (↑m : ℕ) x)) = M.evalFrom s (List.take (↑m : ℕ) x)
⊢ M.evalFrom (M.evalFrom s (List.take (↑n : ℕ) (List.take (↑m : ℕ) x))) (List.drop (↑n : ℕ) (List.take (↑m : ℕ) x)) =
    M.evalFrom s (List.take (↑n : ℕ) (List.take (↑m : ℕ) x))
have rw₄ : M.evalFrom s (List.take (min (↑n : ℕ) (↑m : ℕ)) x ++ List.drop (min (↑n : ℕ) (↑m : ℕ)) (List.take (↑m : ℕ) x)) =
  M.evalFrom s (List.take (↑m : ℕ) x)
Tactic: rw [List.take_take, min_eq_left hle, ← evalFrom_of_append, heq, ← min_eq_left hle, ←
      List.take_take, min_eq_left hle, List.take_append_drop]
-- Lean 4 proof step from Mathlib.Computability.DFA (goal)
Goal:
α : Type u
σ : Type v
M : DFA α σ
inst : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ x.length
hx : M.evalFrom s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : M.evalFrom s (List.take (↑n : ℕ) x) = M.evalFrom s (List.take (↑m : ℕ) x)
hle : (↑n : ℕ) ≤ (↑m : ℕ)
rw :
  M.evalFrom (M.evalFrom s (List.take (min (↑n : ℕ) (↑m : ℕ)) x)) (List.drop (↑n : ℕ) (List.take (↑m : ℕ) x)) =
    M.evalFrom s (List.take (min (↑n : ℕ) (↑m : ℕ)) x)
rw₁ :
  M.evalFrom (M.evalFrom s (List.take (↑n : ℕ) x)) (List.drop (↑n : ℕ) (List.take (↑m : ℕ) x)) =
    M.evalFrom s (List.take (↑n : ℕ) x)
rw₂ :
  M.evalFrom s (List.take (↑n : ℕ) x ++ List.drop (↑n : ℕ) (List.take (↑m : ℕ) x)) = M.evalFrom s (List.take (↑n : ℕ) x)
rw₃ :
  M.evalFrom s (List.take (↑n : ℕ) x ++ List.drop (↑n : ℕ) (List.take (↑m : ℕ) x)) = M.evalFrom s (List.take (↑m : ℕ) x)
rw₄ :
  M.evalFrom s (List.take (min (↑n : ℕ) (↑m : ℕ)) x ++ List.drop (min (↑n : ℕ) (↑m : ℕ)) (List.take (↑m : ℕ) x)) =
    M.evalFrom s (List.take (↑m : ℕ) x)
⊢ M.evalFrom (M.evalFrom s (List.take (↑n : ℕ) (List.take (↑m : ℕ) x))) (List.drop (↑n : ℕ) (List.take (↑m : ℕ) x)) =
    M.evalFrom s (List.take (↑n : ℕ) (List.take (↑m : ℕ) x))
have rw₅ : M.evalFrom s (List.take (↑n : ℕ) (List.take (↑m : ℕ) x) ++ List.drop (min (↑n : ℕ) (↑m : ℕ)) (List.take (↑m : ℕ) x)) =
  M.evalFrom s (List.take (↑m : ℕ) x)
Tactic: rw [List.take_take, min_eq_left hle, ← evalFrom_of_append, heq, ← min_eq_left hle, ←
      List.take_take, min_eq_left hle, List.take_append_drop]
-- Lean 4 proof step from Mathlib.Computability.DFA (goal)
Goal:
α : Type u
σ : Type v
M : DFA α σ
inst : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ x.length
hx : M.evalFrom s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : M.evalFrom s (List.take (↑n : ℕ) x) = M.evalFrom s (List.take (↑m : ℕ) x)
hle : (↑n : ℕ) ≤ (↑m : ℕ)
rw :
  M.evalFrom (M.evalFrom s (List.take (min (↑n : ℕ) (↑m : ℕ)) x)) (List.drop (↑n : ℕ) (List.take (↑m : ℕ) x)) =
    M.evalFrom s (List.take (min (↑n : ℕ) (↑m : ℕ)) x)
rw₁ :
  M.evalFrom (M.evalFrom s (List.take (↑n : ℕ) x)) (List.drop (↑n : ℕ) (List.take (↑m : ℕ) x)) =
    M.evalFrom s (List.take (↑n : ℕ) x)
rw₂ :
  M.evalFrom s (List.take (↑n : ℕ) x ++ List.drop (↑n : ℕ) (List.take (↑m : ℕ) x)) = M.evalFrom s (List.take (↑n : ℕ) x)
rw₃ :
  M.evalFrom s (List.take (↑n : ℕ) x ++ List.drop (↑n : ℕ) (List.take (↑m : ℕ) x)) = M.evalFrom s (List.take (↑m : ℕ) x)
rw₄ :
  M.evalFrom s (List.take (min (↑n : ℕ) (↑m : ℕ)) x ++ List.drop (min (↑n : ℕ) (↑m : ℕ)) (List.take (↑m : ℕ) x)) =
    M.evalFrom s (List.take (↑m : ℕ) x)
rw₅ :
  M.evalFrom s (List.take (↑n : ℕ) (List.take (↑m : ℕ) x) ++ List.drop (min (↑n : ℕ) (↑m : ℕ)) (List.take (↑m : ℕ) x)) =
    M.evalFrom s (List.take (↑m : ℕ) x)
⊢ M.evalFrom (M.evalFrom s (List.take (↑n : ℕ) (List.take (↑m : ℕ) x))) (List.drop (↑n : ℕ) (List.take (↑m : ℕ) x)) =
    M.evalFrom s (List.take (↑n : ℕ) (List.take (↑m : ℕ) x))
have rw₆ : M.evalFrom s (List.take (↑n : ℕ) (List.take (↑m : ℕ) x) ++ List.drop (↑n : ℕ) (List.take (↑m : ℕ) x)) =
  M.evalFrom s (List.take (↑m : ℕ) x)
Tactic: rw [List.take_take, min_eq_left hle, ← evalFrom_of_append, heq, ← min_eq_left hle, ←
      List.take_take, min_eq_left hle, List.take_append_drop]
-- Lean 4 proof step from Mathlib.Computability.DFA (goal)
Goal:
α : Type u
σ : Type v
M : DFA α σ
inst : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ x.length
hx : M.evalFrom s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : M.evalFrom s (List.take (↑n : ℕ) x) = M.evalFrom s (List.take (↑m : ℕ) x)
hle : (↑n : ℕ) ≤ (↑m : ℕ)
rw :
  M.evalFrom (M.evalFrom s (List.take (min (↑n : ℕ) (↑m : ℕ)) x)) (List.drop (↑n : ℕ) (List.take (↑m : ℕ) x)) =
    M.evalFrom s (List.take (min (↑n : ℕ) (↑m : ℕ)) x)
rw₁ :
  M.evalFrom (M.evalFrom s (List.take (↑n : ℕ) x)) (List.drop (↑n : ℕ) (List.take (↑m : ℕ) x)) =
    M.evalFrom s (List.take (↑n : ℕ) x)
rw₂ :
  M.evalFrom s (List.take (↑n : ℕ) x ++ List.drop (↑n : ℕ) (List.take (↑m : ℕ) x)) = M.evalFrom s (List.take (↑n : ℕ) x)
rw₃ :
  M.evalFrom s (List.take (↑n : ℕ) x ++ List.drop (↑n : ℕ) (List.take (↑m : ℕ) x)) = M.evalFrom s (List.take (↑m : ℕ) x)
rw₄ :
  M.evalFrom s (List.take (min (↑n : ℕ) (↑m : ℕ)) x ++ List.drop (min (↑n : ℕ) (↑m : ℕ)) (List.take (↑m : ℕ) x)) =
    M.evalFrom s (List.take (↑m : ℕ) x)
rw₅ :
  M.evalFrom s (List.take (↑n : ℕ) (List.take (↑m : ℕ) x) ++ List.drop (min (↑n : ℕ) (↑m : ℕ)) (List.take (↑m : ℕ) x)) =
    M.evalFrom s (List.take (↑m : ℕ) x)
rw₆ :
  M.evalFrom s (List.take (↑n : ℕ) (List.take (↑m : ℕ) x) ++ List.drop (↑n : ℕ) (List.take (↑m : ℕ) x)) =
    M.evalFrom s (List.take (↑m : ℕ) x)
⊢ M.evalFrom (M.evalFrom s (List.take (↑n : ℕ) (List.take (↑m : ℕ) x))) (List.drop (↑n : ℕ) (List.take (↑m : ℕ) x)) =
    M.evalFrom s (List.take (↑n : ℕ) (List.take (↑m : ℕ) x))
have rw₇ : M.evalFrom s (List.take (↑m : ℕ) x) = M.evalFrom s (List.take (↑m : ℕ) x)
Tactic: rw [List.take_take, min_eq_left hle, ← evalFrom_of_append, heq, ← min_eq_left hle, ←
      List.take_take, min_eq_left hle, List.take_append_drop]
-- Lean 4 proof step from Mathlib.Computability.DFA (hypothesis)
Goal:
α : Type u
σ : Type v
M : DFA α σ
inst : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ x.length
hx : M.evalFrom s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : M.evalFrom s (List.take (↑n : ℕ) x) = M.evalFrom s (List.take (↑m : ℕ) x)
hle : (↑n : ℕ) ≤ (↑m : ℕ)
⊢ M.evalFrom (M.evalFrom s (List.take (↑n : ℕ) (List.take (↑m : ℕ) x))) (List.drop (↑n : ℕ) (List.take (↑m : ℕ) x)) =
      M.evalFrom s (List.take (↑n : ℕ) (List.take (↑m : ℕ) x)) ∧
    M.evalFrom (M.evalFrom s (List.take (↑n : ℕ) (List.take (↑m : ℕ) x))) (List.drop (↑m : ℕ) x) = t
have hq : M.evalFrom (M.evalFrom s (List.take (↑n : ℕ) (List.take (↑m : ℕ) x))) (List.drop (↑n : ℕ) (List.take (↑m : ℕ) x)) =
  M.evalFrom s (List.take (↑n : ℕ) (List.take (↑m : ℕ) x))
Tactic: have hq : M.evalFrom (M.evalFrom s ((x.take m).take n)) ((x.take m).drop n) =
      M.evalFrom s ((x.take m).take n) := by
    rw [List.take_take, min_eq_left hle, ← evalFrom_of_append, heq, ← min_eq_left hle, ←
      List.take_take, min_eq_left hle, List.take_append_drop]
-- Lean 4 proof step from Mathlib.Computability.DFA (goal)
Goal:
α : Type u
σ : Type v
M : DFA α σ
inst : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ x.length
hx : M.evalFrom s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : M.evalFrom s (List.take (↑n : ℕ) x) = M.evalFrom s (List.take (↑m : ℕ) x)
hle : (↑n : ℕ) ≤ (↑m : ℕ)
hq :
  M.evalFrom (M.evalFrom s (List.take (↑n : ℕ) (List.take (↑m : ℕ) x))) (List.drop (↑n : ℕ) (List.take (↑m : ℕ) x)) =
    M.evalFrom s (List.take (↑n : ℕ) (List.take (↑m : ℕ) x))
⊢ M.evalFrom (M.evalFrom s (List.take (↑n : ℕ) (List.take (↑m : ℕ) x))) (List.drop (↑n : ℕ) (List.take (↑m : ℕ) x)) =
      M.evalFrom s (List.take (↑n : ℕ) (List.take (↑m : ℕ) x)) ∧
    M.evalFrom (M.evalFrom s (List.take (↑n : ℕ) (List.take (↑m : ℕ) x))) (List.drop (↑m : ℕ) x) = t
have right : M.evalFrom (M.evalFrom s (List.take (↑n : ℕ) (List.take (↑m : ℕ) x))) (List.drop (↑m : ℕ) x) = t
Tactic: use hq
-- Lean 4 proof step from Mathlib.Computability.DFA (goal)
Goal:
α : Type u
σ : Type v
M : DFA α σ
inst : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ x.length
hx : M.evalFrom s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : M.evalFrom s (List.take (↑n : ℕ) x) = M.evalFrom s (List.take (↑m : ℕ) x)
hle : (↑n : ℕ) ≤ (↑m : ℕ)
hq :
  M.evalFrom (M.evalFrom s (List.take (↑n : ℕ) (List.take (↑m : ℕ) x))) (List.drop (↑n : ℕ) (List.take (↑m : ℕ) x)) =
    M.evalFrom s (List.take (↑n : ℕ) (List.take (↑m : ℕ) x))
⊢ M.evalFrom (M.evalFrom s (List.take (↑n : ℕ) (List.take (↑m : ℕ) x))) (List.drop (↑m : ℕ) x) = t
have right : M.evalFrom
    (M.evalFrom (M.evalFrom s (List.take (↑n : ℕ) (List.take (↑m : ℕ) x))) (List.drop (↑n : ℕ) (List.take (↑m : ℕ) x)))
    (List.drop (↑m : ℕ) x) =
  t
Tactic: rwa [← hq, ← evalFrom_of_append, ← evalFrom_of_append, ← List.append_assoc,
    List.take_append_drop, List.take_append_drop]
-- Lean 4 proof step from Mathlib.Computability.DFA (goal)
Goal:
α : Type u
σ : Type v
M : DFA α σ
inst : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ x.length
hx : M.evalFrom s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : M.evalFrom s (List.take (↑n : ℕ) x) = M.evalFrom s (List.take (↑m : ℕ) x)
hle : (↑n : ℕ) ≤ (↑m : ℕ)
hq :
  M.evalFrom (M.evalFrom s (List.take (↑n : ℕ) (List.take (↑m : ℕ) x))) (List.drop (↑n : ℕ) (List.take (↑m : ℕ) x)) =
    M.evalFrom s (List.take (↑n : ℕ) (List.take (↑m : ℕ) x))
right :
  M.evalFrom
      (M.evalFrom (M.evalFrom s (List.take (↑n : ℕ) (List.take (↑m : ℕ) x)))
        (List.drop (↑n : ℕ) (List.take (↑m : ℕ) x)))
      (List.drop (↑m : ℕ) x) =
    t
⊢ M.evalFrom (M.evalFrom s (List.take (↑n : ℕ) (List.take (↑m : ℕ) x))) (List.drop (↑m : ℕ) x) = t
have right₁ : M.evalFrom (M.evalFrom s (List.take (↑n : ℕ) (List.take (↑m : ℕ) x)))
    (List.drop (↑n : ℕ) (List.take (↑m : ℕ) x) ++ List.drop (↑m : ℕ) x) =
  t
Tactic: rwa [← hq, ← evalFrom_of_append, ← evalFrom_of_append, ← List.append_assoc,
    List.take_append_drop, List.take_append_drop]
-- Lean 4 proof step from Mathlib.Computability.DFA (goal)
Goal:
α : Type u
σ : Type v
M : DFA α σ
inst : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ x.length
hx : M.evalFrom s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : M.evalFrom s (List.take (↑n : ℕ) x) = M.evalFrom s (List.take (↑m : ℕ) x)
hle : (↑n : ℕ) ≤ (↑m : ℕ)
hq :
  M.evalFrom (M.evalFrom s (List.take (↑n : ℕ) (List.take (↑m : ℕ) x))) (List.drop (↑n : ℕ) (List.take (↑m : ℕ) x)) =
    M.evalFrom s (List.take (↑n : ℕ) (List.take (↑m : ℕ) x))
right :
  M.evalFrom
      (M.evalFrom (M.evalFrom s (List.take (↑n : ℕ) (List.take (↑m : ℕ) x)))
        (List.drop (↑n : ℕ) (List.take (↑m : ℕ) x)))
      (List.drop (↑m : ℕ) x) =
    t
right₁ :
  M.evalFrom (M.evalFrom s (List.take (↑n : ℕ) (List.take (↑m : ℕ) x)))
      (List.drop (↑n : ℕ) (List.take (↑m : ℕ) x) ++ List.drop (↑m : ℕ) x) =
    t
⊢ M.evalFrom (M.evalFrom s (List.take (↑n : ℕ) (List.take (↑m : ℕ) x))) (List.drop (↑m : ℕ) x) = t
have right₂ : M.evalFrom s
    (List.take (↑n : ℕ) (List.take (↑m : ℕ) x) ++ (List.drop (↑n : ℕ) (List.take (↑m : ℕ) x) ++ List.drop (↑m : ℕ) x)) =
  t
Tactic: rwa [← hq, ← evalFrom_of_append, ← evalFrom_of_append, ← List.append_assoc,
    List.take_append_drop, List.take_append_drop]
-- Lean 4 proof step from Mathlib.Computability.DFA (goal)
Goal:
α : Type u
σ : Type v
M : DFA α σ
inst : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ x.length
hx : M.evalFrom s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : M.evalFrom s (List.take (↑n : ℕ) x) = M.evalFrom s (List.take (↑m : ℕ) x)
hle : (↑n : ℕ) ≤ (↑m : ℕ)
hq :
  M.evalFrom (M.evalFrom s (List.take (↑n : ℕ) (List.take (↑m : ℕ) x))) (List.drop (↑n : ℕ) (List.take (↑m : ℕ) x)) =
    M.evalFrom s (List.take (↑n : ℕ) (List.take (↑m : ℕ) x))
right :
  M.evalFrom
      (M.evalFrom (M.evalFrom s (List.take (↑n : ℕ) (List.take (↑m : ℕ) x)))
        (List.drop (↑n : ℕ) (List.take (↑m : ℕ) x)))
      (List.drop (↑m : ℕ) x) =
    t
right₁ :
  M.evalFrom (M.evalFrom s (List.take (↑n : ℕ) (List.take (↑m : ℕ) x)))
      (List.drop (↑n : ℕ) (List.take (↑m : ℕ) x) ++ List.drop (↑m : ℕ) x) =
    t
right₂ :
  M.evalFrom s
      (List.take (↑n : ℕ) (List.take (↑m : ℕ) x) ++
        (List.drop (↑n : ℕ) (List.take (↑m : ℕ) x) ++ List.drop (↑m : ℕ) x)) =
    t
⊢ M.evalFrom (M.evalFrom s (List.take (↑n : ℕ) (List.take (↑m : ℕ) x))) (List.drop (↑m : ℕ) x) = t
have right₃ : M.evalFrom s
    (List.take (↑n : ℕ) (List.take (↑m : ℕ) x) ++ List.drop (↑n : ℕ) (List.take (↑m : ℕ) x) ++ List.drop (↑m : ℕ) x) =
  t
Tactic: rwa [← hq, ← evalFrom_of_append, ← evalFrom_of_append, ← List.append_assoc,
    List.take_append_drop, List.take_append_drop]
-- Lean 4 proof step from Mathlib.Computability.DFA (goal)
Goal:
α : Type u
σ : Type v
M : DFA α σ
inst : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ x.length
hx : M.evalFrom s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : M.evalFrom s (List.take (↑n : ℕ) x) = M.evalFrom s (List.take (↑m : ℕ) x)
hle : (↑n : ℕ) ≤ (↑m : ℕ)
hq :
  M.evalFrom (M.evalFrom s (List.take (↑n : ℕ) (List.take (↑m : ℕ) x))) (List.drop (↑n : ℕ) (List.take (↑m : ℕ) x)) =
    M.evalFrom s (List.take (↑n : ℕ) (List.take (↑m : ℕ) x))
right :
  M.evalFrom
      (M.evalFrom (M.evalFrom s (List.take (↑n : ℕ) (List.take (↑m : ℕ) x)))
        (List.drop (↑n : ℕ) (List.take (↑m : ℕ) x)))
      (List.drop (↑m : ℕ) x) =
    t
right₁ :
  M.evalFrom (M.evalFrom s (List.take (↑n : ℕ) (List.take (↑m : ℕ) x)))
      (List.drop (↑n : ℕ) (List.take (↑m : ℕ) x) ++ List.drop (↑m : ℕ) x) =
    t
right₂ :
  M.evalFrom s
      (List.take (↑n : ℕ) (List.take (↑m : ℕ) x) ++
        (List.drop (↑n : ℕ) (List.take (↑m : ℕ) x) ++ List.drop (↑m : ℕ) x)) =
    t
right₃ :
  M.evalFrom s
      (List.take (↑n : ℕ) (List.take (↑m : ℕ) x) ++ List.drop (↑n : ℕ) (List.take (↑m : ℕ) x) ++ List.drop (↑m : ℕ) x) =
    t
⊢ M.evalFrom (M.evalFrom s (List.take (↑n : ℕ) (List.take (↑m : ℕ) x))) (List.drop (↑m : ℕ) x) = t
have right₄ : M.evalFrom s (List.take (↑m : ℕ) x ++ List.drop (↑m : ℕ) x) = t
Tactic: rwa [← hq, ← evalFrom_of_append, ← evalFrom_of_append, ← List.append_assoc,
    List.take_append_drop, List.take_append_drop]
-- Lean 4 proof step from Mathlib.Computability.DFA (hypothesis)
Goal:
α : Type u
σ : Type v
M : DFA α σ
x y : List α
s : σ
hx : M.evalFrom s x = s
hy : Membership.mem (γ := Language α) {x}∗ y
⊢ M.evalFrom s y = s
have hy₁ : ∃ (L : List (List α)), y = L.flatten ∧ ∀ y ∈ L, Membership.mem (γ := Language α) {x} y
Tactic: rw [Language.mem_kstar] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Computability.DFA (goal)
Goal:
α : Type u
σ : Type v
M : DFA α σ
x y : List α
s : σ
hx : M.evalFrom s x = s
hy : ∃ (L : List (List α)), y = L.flatten ∧ ∀ y ∈ L, Membership.mem (γ := Language α) {x} y
⊢ M.evalFrom s y = s
have rcases : ∀ (S : List (List α)) (hS : ∀ y ∈ S, Membership.mem (γ := Language α) {x} y), M.evalFrom s S.flatten = s
Tactic: rcases hy with ⟨S, rfl, hS⟩
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.Computability.DFA (hypothesis)
Goal:
α : Type u
σ : Type v
M : DFA α σ
x : List α
s : σ
hx : M.evalFrom s x = s
a : List α
S : List (List α)
ih : ∀ (hS : ∀ y ∈ S, Membership.mem (γ := Language α) {x} y), M.evalFrom s S.flatten = s
hS : ∀ y ∈ a :: S, Membership.mem (γ := Language α) {x} y
⊢ M.evalFrom s (a :: S).flatten = s
have ha : Membership.mem (γ := Language α) {x} a
Tactic: have ha := hS a List.mem_cons_self
-- Lean 4 proof step from Mathlib.Computability.DFA (hypothesis)
Goal:
α : Type u
σ : Type v
M : DFA α σ
x : List α
s : σ
hx : M.evalFrom s x = s
a : List α
S : List (List α)
ih : ∀ (hS : ∀ y ∈ S, Membership.mem (γ := Language α) {x} y), M.evalFrom s S.flatten = s
hS : ∀ y ∈ a :: S, Membership.mem (γ := Language α) {x} y
ha : Membership.mem (γ := Language α) {x} a
⊢ M.evalFrom s (a :: S).flatten = s
have ha₁ : a = x
Tactic: rw [Set.mem_singleton_iff] at ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Computability.DFA (goal)
Goal:
α : Type u
σ : Type v
M : DFA α σ
x : List α
s : σ
hx : M.evalFrom s x = s
a : List α
S : List (List α)
ih : ∀ (hS : ∀ y ∈ S, Membership.mem (γ := Language α) {x} y), M.evalFrom s S.flatten = s
hS : ∀ y ∈ a :: S, Membership.mem (γ := Language α) {x} y
ha : a = x
⊢ M.evalFrom s (a :: S).flatten = s
have cons : M.evalFrom s S.flatten = s
Tactic: rw [List.flatten_cons, evalFrom_of_append, ha, hx]
-- Lean 4 proof step from Mathlib.Computability.DFA (goal)
Goal:
α : Type u
σ : Type v
M : DFA α σ
x : List α
s : σ
hx : M.evalFrom s x = s
a : List α
S : List (List α)
ih : ∀ (hS : ∀ y ∈ S, Membership.mem (γ := Language α) {x} y), M.evalFrom s S.flatten = s
hS : ∀ y ∈ a :: S, Membership.mem (γ := Language α) {x} y
ha : a = x
⊢ M.evalFrom s S.flatten = s
have cons : ∀ y ∈ S, Membership.mem (γ := Language α) {x} y
Tactic: apply ih
-- Lean 4 proof step from Mathlib.Computability.DFA (goal)
Goal:
α : Type u
σ : Type v
M : DFA α σ
x : List α
s : σ
hx : M.evalFrom s x = s
S : List (List α)
hS : ∀ y ∈ S, Membership.mem (γ := Language α) {x} y
⊢ M.evalFrom s S.flatten = s
have nil : ∀ (hS : ∀ (y : List α), Membership.mem (γ := List (List α)) [] y → Membership.mem (γ := Language α) {x} y),
  M.evalFrom s (List.flatten []) = s
Tactic: induction S with
  | nil => rfl
  | cons a S ih =>
    have ha := hS a List.mem_cons_self
    rw [Set.mem_singleton_iff] at ha
    rw [List.flatten_cons, evalFrom_of_append, ha, hx]
    apply ih
    intro z hz
    exact hS z (List.mem_cons_of_mem a hz)
Cleared hypotheses: S, hS
-- Lean 4 proof step from Mathlib.Computability.DFA (goal)
Goal:
α : Type u
σ : Type v
M : DFA α σ
x : List α
s : σ
hx : M.evalFrom s x = s
S : List (List α)
hS : ∀ y ∈ S, Membership.mem (γ := Language α) {x} y
nil :
  ∀ (hS : ∀ (y : List α), Membership.mem (γ := List (List α)) [] y → Membership.mem (γ := Language α) {x} y),
    M.evalFrom s (List.flatten []) = s
⊢ M.evalFrom s S.flatten = s
have cons : ∀ (a : List α) (S : List (List α))
  (ih : ∀ (hS : ∀ y ∈ S, Membership.mem (γ := Language α) {x} y), M.evalFrom s S.flatten = s)
  (hS : ∀ y ∈ a :: S, Membership.mem (γ := Language α) {x} y), M.evalFrom s (a :: S).flatten = s
Tactic: induction S with
  | nil => rfl
  | cons a S ih =>
    have ha := hS a List.mem_cons_self
    rw [Set.mem_singleton_iff] at ha
    rw [List.flatten_cons, evalFrom_of_append, ha, hx]
    apply ih
    intro z hz
    exact hS z (List.mem_cons_of_mem a hz)
Cleared hypotheses: S, hS
-- Lean 4 proof step from Mathlib.Computability.DFA (goal)
Goal:
α : Type u
σ : Type v
M : DFA α σ
inst : Fintype σ
x : List α
hx : x ∈ M.accepts
hlen : Fintype.card σ ≤ x.length
⊢ ∃ (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 obtain : ∀ (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
Tactic: obtain ⟨_, a, b, c, hx, hlen, hnil, rfl, hb, hc⟩ := M.evalFrom_split (s := M.start) hlen rfl