awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Computability.Language (goal)
Goal:
α : Type u_1
l : Language α
n : ℕ
ihn : ∀ {x : List α}, x ∈ l ^ n ↔ ∃ (S : List (List α)), x = S.flatten ∧ S.length = n ∧ ∀ y ∈ S, y ∈ l
x : List α
⊢ (∃ a ∈ l, ∃ (b : List α), (∃ (S : List (List α)), b = S.flatten ∧ S.length = n ∧ ∀ y ∈ S, y ∈ l) ∧ a ++ b = x) ↔
    ∃ (S : List (List α)), x = S.flatten ∧ S.length = n + 1 ∧ ∀ y ∈ S, y ∈ l
have succ : (∃ a ∈ l, ∃ (b : List α), (∃ (S : List (List α)), b = S.flatten ∧ S.length = n ∧ ∀ y ∈ S, y ∈ l) ∧ a ++ b = x) →
  ∃ (S : List (List α)), x = S.flatten ∧ S.length = n + 1 ∧ ∀ y ∈ S, y ∈ l
Tactic: constructor
-- Lean 4 proof step from Mathlib.Computability.Language (goal)
Goal:
α : Type u_1
l : Language α
n : ℕ
ihn : ∀ {x : List α}, x ∈ l ^ n ↔ ∃ (S : List (List α)), x = S.flatten ∧ S.length = n ∧ ∀ y ∈ S, y ∈ l
x : List α
succ :
  (∃ a ∈ l, ∃ (b : List α), (∃ (S : List (List α)), b = S.flatten ∧ S.length = n ∧ ∀ y ∈ S, y ∈ l) ∧ a ++ b = x) →
    ∃ (S : List (List α)), x = S.flatten ∧ S.length = n + 1 ∧ ∀ y ∈ S, y ∈ l
⊢ (∃ a ∈ l, ∃ (b : List α), (∃ (S : List (List α)), b = S.flatten ∧ S.length = n ∧ ∀ y ∈ S, y ∈ l) ∧ a ++ b = x) ↔
    ∃ (S : List (List α)), x = S.flatten ∧ S.length = n + 1 ∧ ∀ y ∈ S, y ∈ l
have succ₁ : (∃ (S : List (List α)), x = S.flatten ∧ S.length = n + 1 ∧ ∀ y ∈ S, y ∈ l) →
  ∃ a ∈ l, ∃ (b : List α), (∃ (S : List (List α)), b = S.flatten ∧ S.length = n ∧ ∀ y ∈ S, y ∈ l) ∧ a ++ b = x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Computability.Language (goal)
Goal:
α : Type u_1
l : Language α
n : ℕ
ihn : ∀ {x : List α}, x ∈ l ^ n ↔ ∃ (S : List (List α)), x = S.flatten ∧ S.length = n ∧ ∀ y ∈ S, y ∈ l
a : List α
S : List (List α)
hn : (a :: S).length = n + 1
hS : ∀ y ∈ a :: S, y ∈ l
⊢ ∃ a_1 ∈ l,
    ∃ (b : List α), (∃ (S : List (List α)), b = S.flatten ∧ S.length = n ∧ ∀ y ∈ S, y ∈ l) ∧ a_1 ++ b = (a :: S).flatten
have succ : ∀
  (ihn :
    ∀ {x : List α},
      x ∈ l ^ S.length ↔ ∃ (S_1 : List (List α)), x = S_1.flatten ∧ S_1.length = S.length ∧ ∀ y ∈ S_1, y ∈ l),
  ∃ a_1 ∈ l,
    ∃ (b : List α),
      (∃ (S_1 : List (List α)), b = S_1.flatten ∧ S_1.length = S.length ∧ ∀ y ∈ S_1, y ∈ l) ∧
        a_1 ++ b = (a :: S).flatten
Tactic: cases hn
Cleared hypotheses: n, ihn, hn
-- Lean 4 proof step from Mathlib.Computability.Language (hypothesis)
Goal:
α : Type u_1
l : Language α
a : List α
S : List (List α)
hS : ∀ y ∈ a :: S, y ∈ l
ihn :
  ∀ {x : List α}, x ∈ l ^ S.length ↔ ∃ (S_1 : List (List α)), x = S_1.flatten ∧ S_1.length = S.length ∧ ∀ y ∈ S_1, y ∈ l
⊢ ∃ a_1 ∈ l,
    ∃ (b : List α),
      (∃ (S_1 : List (List α)), b = S_1.flatten ∧ S_1.length = S.length ∧ ∀ y ∈ S_1, y ∈ l) ∧
        a_1 ++ b = (a :: S).flatten
have hS₁ : a ∈ l ∧ ∀ x ∈ S, x ∈ l
Tactic: rw [forall_mem_cons] at hS
Cleared hypotheses: hS, ihn
-- Lean 4 proof step from Mathlib.Computability.Language (goal)
Goal:
α : Type u_1
l : Language α
x : List α
n : ℕ
⊢ x ∈ l ^ n ↔ ∃ (S : List (List α)), x = S.flatten ∧ S.length = n ∧ ∀ y ∈ S, y ∈ l
have zero : ∀ {x : List α}, x ∈ HPow.hPow (β := ℕ) l 0 ↔ ∃ (S : List (List α)), x = S.flatten ∧ S.length = 0 ∧ ∀ y ∈ S, y ∈ l
Tactic: induction n generalizing x with
  | zero => simp
  | succ n ihn =>
    simp only [pow_succ', mem_mul, ihn]
    constructor
    · rintro ⟨a, ha, b, ⟨S, rfl, rfl, hS⟩, rfl⟩
      exact ⟨a :: S, rfl, rfl, forall_mem_cons.2 ⟨ha, hS⟩⟩
    · rintro ⟨_ | ⟨a, S⟩, rfl, hn, hS⟩ <;> cases hn
      rw [forall_mem_cons] at hS
      exact ⟨a, hS.1, _, ⟨S, rfl, rfl, hS.2⟩, rfl⟩
Cleared hypotheses: x, n
-- Lean 4 proof step from Mathlib.Computability.Language (goal)
Goal:
α : Type u_1
l : Language α
x : List α
n : ℕ
zero : ∀ {x : List α}, x ∈ HPow.hPow (β := ℕ) l 0 ↔ ∃ (S : List (List α)), x = S.flatten ∧ S.length = 0 ∧ ∀ y ∈ S, y ∈ l
⊢ x ∈ l ^ n ↔ ∃ (S : List (List α)), x = S.flatten ∧ S.length = n ∧ ∀ y ∈ S, y ∈ l
have succ : ∀ (n : ℕ) (ihn : ∀ {x : List α}, x ∈ l ^ n ↔ ∃ (S : List (List α)), x = S.flatten ∧ S.length = n ∧ ∀ y ∈ S, y ∈ l)
  {x : List α}, x ∈ l ^ (n + 1) ↔ ∃ (S : List (List α)), x = S.flatten ∧ S.length = n + 1 ∧ ∀ y ∈ S, y ∈ l
Tactic: induction n generalizing x with
  | zero => simp
  | succ n ihn =>
    simp only [pow_succ', mem_mul, ihn]
    constructor
    · rintro ⟨a, ha, b, ⟨S, rfl, rfl, hS⟩, rfl⟩
      exact ⟨a :: S, rfl, rfl, forall_mem_cons.2 ⟨ha, hS⟩⟩
    · rintro ⟨_ | ⟨a, S⟩, rfl, hn, hS⟩ <;> cases hn
      rw [forall_mem_cons] at hS
      exact ⟨a, hS.1, _, ⟨S, rfl, rfl, hS.2⟩, rfl⟩
Cleared hypotheses: x, n
-- Lean 4 proof step from Mathlib.Computability.Language (goal)
Goal:
α : Type u_1
l : Language α
⊢ l∗ = ⨆ (i : ℕ), l ^ i
have h : ∀ (x : List α), x ∈ l∗ ↔ Membership.mem (γ := Language α) (⨆ (i : ℕ), l ^ i) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Computability.Language (goal)
Goal:
α : Type u_1
l : Language α
x : List α
⊢ x ∈ l∗ ↔ Membership.mem (γ := Language α) (⨆ (i : ℕ), l ^ i) x
have h : (∃ (L : List (List α)), x = L.flatten ∧ ∀ y ∈ L, y ∈ l) ↔
  ∃ (i : ℕ) (S : List (List α)), x = S.flatten ∧ S.length = i ∧ ∀ y ∈ S, y ∈ l
Tactic: simp only [mem_kstar, mem_iSup, mem_pow]
-- Lean 4 proof step from Mathlib.Computability.Language (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
l : Language α
⊢ Eq.{u_2 + 1} (α := Language β) ((map f : (a : Language α) → Language β) l∗ : Language β)
    (((map f : (a : Language α) → Language β) l)∗ : Language β)
have rw : Eq.{u_2 + 1} (α := Language β) ((map f : (a : Language α) → Language β) (⨆ (i : ℕ), l ^ i))
  (⨆ (i : ℕ), HPow.hPow (α := Language β) ((map f : (a : Language α) → Language β) l : Language β) i)
Tactic: rw [kstar_eq_iSup_pow, kstar_eq_iSup_pow]
-- Lean 4 proof step from Mathlib.Computability.Language (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
l : Language α
⊢ Eq.{u_2 + 1} (α := Language β) ((map f : (a : Language α) → Language β) (⨆ (i : ℕ), l ^ i))
    (⨆ (i : ℕ), HPow.hPow (α := Language β) ((map f : (a : Language α) → Language β) l : Language β) i)
have simp_rw : Eq.{u_2 + 1} (α := Language β) ((map f : (a : Language α) → Language β) (⨆ (i : ℕ), l ^ i))
  (⨆ (i : ℕ), (map f : (a : Language α) → Language β) (l ^ i))
Tactic: simp_rw [← map_pow]
-- Lean 4 proof step from Mathlib.Computability.Language (goal)
Goal:
α : Type u_1
l : Language α
⊢ 1 + l * l∗ = l∗
have simp : HPow.hPow (β := ℕ) l 0 + ⨆ (i : ℕ), l ^ (i + 1) = ⨆ (i : ℕ), l ^ i
Tactic: simp only [kstar_eq_iSup_pow, mul_iSup, ← pow_succ', ← pow_zero l]
-- Lean 4 proof step from Mathlib.Computability.Language (goal)
Goal:
α : Type u_1
l : Language α
⊢ 1 + l∗ * l = l∗
have rw : 1 + l * l∗ = l∗
Tactic: rw [mul_self_kstar_comm, one_add_self_mul_kstar_eq_kstar]
-- Lean 4 proof step from Mathlib.Computability.Language (goal)
Goal:
α : Type u_1
l : Language α
rw : 1 + l * l∗ = l∗
⊢ 1 + l∗ * l = l∗
have rw₁ : l∗ = l∗
Tactic: rw [mul_self_kstar_comm, one_add_self_mul_kstar_eq_kstar]
-- Lean 4 proof step from Mathlib.Computability.Language (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
l_1 m_1 : Language α
a b x : List α
l m : Language α
h : m * l ≤ m
⊢ m * l∗ ≤ m
have rw : ⨆ (i : ℕ), m * l ^ i ≤ m
Tactic: rw [kstar_eq_iSup_pow, mul_iSup]
-- Lean 4 proof step from Mathlib.Computability.Language (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
l_1 m_1 : Language α
a b x : List α
l m : Language α
h : m * l ≤ m
⊢ ⨆ (i : ℕ), m * l ^ i ≤ m
have refine : ∀ (n : ℕ), m * l ^ n ≤ m
Tactic: refine iSup_le fun n ↦ ?_
-- Lean 4 proof step from Mathlib.Computability.Language (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
l_1 m_1 : Language α
a b x : List α
l m : Language α
h : m * l ≤ m
n : ℕ
ih : m * l ^ n ≤ m
⊢ m * l ^ (n + 1) ≤ m
have succ : m * (l ^ n * l) ≤ m
Tactic: grw [pow_succ, ← mul_assoc m (l ^ n) l, ih, h]
-- Lean 4 proof step from Mathlib.Computability.Language (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
l_1 m_1 : Language α
a b x : List α
l m : Language α
h : m * l ≤ m
n : ℕ
ih : m * l ^ n ≤ m
succ : m * (l ^ n * l) ≤ m
⊢ m * l ^ (n + 1) ≤ m
have succ₁ : m * l ^ n * l ≤ m
Tactic: grw [pow_succ, ← mul_assoc m (l ^ n) l, ih, h]
-- Lean 4 proof step from Mathlib.Computability.Language (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
l_1 m_1 : Language α
a b x : List α
l m : Language α
h : m * l ≤ m
n : ℕ
ih : m * l ^ n ≤ m
succ : m * (l ^ n * l) ≤ m
succ₁ : m * l ^ n * l ≤ m
succ₂ : m * l ≤ m
⊢ m * l ^ (n + 1) ≤ m
have succ₃ : m ≤ m
Tactic: grw [pow_succ, ← mul_assoc m (l ^ n) l, ih, h]
-- Lean 4 proof step from Mathlib.Computability.Language (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
l_1 m_1 : Language α
a b x : List α
l m : Language α
h : m * l ≤ m
n : ℕ
⊢ m * l ^ n ≤ m
have zero : m * HPow.hPow (β := ℕ) l 0 ≤ m
Tactic: induction n with
    | zero => simp
    | succ n ih => grw [pow_succ, ← mul_assoc m (l ^ n) l, ih, h]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Computability.Language (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
l_1 m_1 : Language α
a b x : List α
l m : Language α
h : m * l ≤ m
n : ℕ
zero : m * HPow.hPow (β := ℕ) l 0 ≤ m
⊢ m * l ^ n ≤ m
have succ : ∀ (n : ℕ) (ih : m * l ^ n ≤ m), m * l ^ (n + 1) ≤ m
Tactic: induction n with
    | zero => simp
    | succ n ih => grw [pow_succ, ← mul_assoc m (l ^ n) l, ih, h]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Computability.Language (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
l_1 m_1 : Language α
a b x : List α
l m : Language α
h : l * m ≤ m
⊢ l∗ * m ≤ m
have rw : ⨆ (i : ℕ), l ^ i * m ≤ m
Tactic: rw [kstar_eq_iSup_pow, iSup_mul]
-- Lean 4 proof step from Mathlib.Computability.Language (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
l_1 m_1 : Language α
a b x : List α
l m : Language α
h : l * m ≤ m
⊢ ⨆ (i : ℕ), l ^ i * m ≤ m
have refine : ∀ (n : ℕ), l ^ n * m ≤ m
Tactic: refine iSup_le fun n ↦ ?_
-- Lean 4 proof step from Mathlib.Computability.Language (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
l_1 m_1 : Language α
a b x : List α
l m : Language α
h : l * m ≤ m
n : ℕ
ih : l ^ n * m ≤ m
⊢ l ^ (n + 1) * m ≤ m
have succ : l ^ n * l * m ≤ m
Tactic: grw [pow_succ, mul_assoc, h, ih]
-- Lean 4 proof step from Mathlib.Computability.Language (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
l_1 m_1 : Language α
a b x : List α
l m : Language α
h : l * m ≤ m
n : ℕ
ih : l ^ n * m ≤ m
succ : l ^ n * l * m ≤ m
⊢ l ^ (n + 1) * m ≤ m
have succ₁ : l ^ n * (l * m) ≤ m
Tactic: grw [pow_succ, mul_assoc, h, ih]
-- Lean 4 proof step from Mathlib.Computability.Language (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
l_1 m_1 : Language α
a b x : List α
l m : Language α
h : l * m ≤ m
n : ℕ
ih : l ^ n * m ≤ m
succ : l ^ n * l * m ≤ m
succ₁ : l ^ n * (l * m) ≤ m
succ₂ : l ^ n * m ≤ m
⊢ l ^ (n + 1) * m ≤ m
have succ₃ : m ≤ m
Tactic: grw [pow_succ, mul_assoc, h, ih]
-- Lean 4 proof step from Mathlib.Computability.Language (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
l_1 m_1 : Language α
a b x : List α
l m : Language α
h : l * m ≤ m
n : ℕ
⊢ l ^ n * m ≤ m
have zero : HPow.hPow (β := ℕ) l 0 * m ≤ m
Tactic: induction n with
    | zero => simp
    | succ n ih => grw [pow_succ, mul_assoc, h, ih]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Computability.Language (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
l_1 m_1 : Language α
a b x : List α
l m : Language α
h : l * m ≤ m
n : ℕ
zero : HPow.hPow (β := ℕ) l 0 * m ≤ m
⊢ l ^ n * m ≤ m
have succ : ∀ (n : ℕ) (ih : l ^ n * m ≤ m), l ^ (n + 1) * m ≤ m
Tactic: induction n with
    | zero => simp
    | succ n ih => grw [pow_succ, mul_assoc, h, ih]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Computability.Language (goal)
Goal:
α : Type u_1
l m n : Language α
hm : [] ∉ m
h : l = m * l + n
⊢ l = m∗ * n
have a : l ≤ m∗ * n
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Computability.Language (goal)
Goal:
α : Type u_1
l m n : Language α
hm : [] ∉ m
h : l = m * l + n
a : l ≤ m∗ * n
⊢ l = m∗ * n
have a₁ : m∗ * n ≤ l
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Computability.Language (goal)
Goal:
α : Type u_1
l m n : Language α
hm : [] ∉ m
h : l = m * l + n
x : List α
hx : x ∈ l
⊢ x ∈ m∗ * n
have a : ∀ (n_1 : ℕ) (ih : ∀ m_1 < n_1, ∀ ⦃x : List α⦄ (hx : x ∈ l) (hlen : x.length = m_1), x ∈ m∗ * n) ⦃x : List α⦄
  (hx : x ∈ l) (hlen : x.length = n_1), x ∈ m∗ * n
Tactic: induction hlen : x.length using Nat.strong_induction_on generalizing x with | _ _ ih
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Computability.Language (hypothesis)
Goal:
α : Type u_1
l m n : Language α
hm : [] ∉ m
h : l = m * l + n
n_1 : ℕ
ih : ∀ m_1 < n_1, ∀ ⦃x : List α⦄ (hx : x ∈ l) (hlen : x.length = m_1), x ∈ m∗ * n
x : List α
hx : x ∈ l
hlen : x.length = n_1
⊢ x ∈ m∗ * n
have ih₁ : ∀ m_1 < x.length, ∀ ⦃x : List α⦄ (hx : x ∈ l) (hlen : x.length = m_1), x ∈ m∗ * n
Tactic: subst hlen
Cleared hypotheses: n_1, ih, hlen
-- Lean 4 proof step from Mathlib.Computability.Language (hypothesis)
Goal:
α : Type u_1
l m n : Language α
hm : [] ∉ m
h : l = m * l + n
x : List α
hx : x ∈ l
ih : ∀ m_1 < x.length, ∀ ⦃x : List α⦄ (hx : x ∈ l) (hlen : x.length = m_1), x ∈ m∗ * n
⊢ x ∈ m∗ * n
have hx₁ : x ∈ m * l + n
Tactic: rw [h] at hx
Cleared hypotheses: hx, ih
-- Lean 4 proof step from Mathlib.Computability.Language (goal)
Goal:
α : Type u_1
l m n : Language α
hm : [] ∉ m
h : l = m * l + n
x : List α
hx : x ∈ m * l + n
ih : ∀ m_1 < x.length, ∀ ⦃x : List α⦄ (hx : x ∈ l) (hlen : x.length = m_1), x ∈ m∗ * n
⊢ x ∈ m∗ * n
have a : ∀ (hx : x ∈ m * l), x ∈ m∗ * n
Tactic: obtain hx | hx := hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Computability.Language (goal)
Goal:
α : Type u_1
l m n : Language α
hm : [] ∉ m
h : l = m * l + n
x : List α
hx : x ∈ m * l + n
ih : ∀ m_1 < x.length, ∀ ⦃x : List α⦄ (hx : x ∈ l) (hlen : x.length = m_1), x ∈ m∗ * n
a : ∀ (hx : x ∈ m * l), x ∈ m∗ * n
⊢ x ∈ m∗ * n
have a₁ : ∀ (hx : x ∈ n), x ∈ m∗ * n
Tactic: obtain hx | hx := hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Computability.Language (goal)
Goal:
α : Type u_1
l m n : Language α
hm : [] ∉ m
h : l = m * l + n
x : List α
ih : ∀ m_1 < x.length, ∀ ⦃x : List α⦄ (hx : x ∈ l) (hlen : x.length = m_1), x ∈ m∗ * n
hx : x ∈ m * l
⊢ x ∈ m∗ * n
have a : ∀ (a : List α) (ha : a ∈ m) (b : List α) (hb : b ∈ l)
  (ih : ∀ m_1 < (a ++ b).length, ∀ ⦃x : List α⦄ (hx : x ∈ l) (hlen : x.length = m_1), x ∈ m∗ * n) (hx : a ++ b ∈ m * l),
  a ++ b ∈ m∗ * n
Tactic: obtain ⟨a, ha, b, hb, rfl⟩ := mem_mul.mp hx
Cleared hypotheses: x, ih, hx
-- Lean 4 proof step from Mathlib.Computability.Language (hypothesis)
Goal:
α : Type u_1
l m n : Language α
hm : [] ∉ m
h : l = m * l + n
a : List α
ha : a ∈ m
b : List α
hb : b ∈ l
ih : ∀ m_1 < (a ++ b).length, ∀ ⦃x : List α⦄ (hx : x ∈ l) (hlen : x.length = m_1), x ∈ m∗ * n
hx : a ++ b ∈ m * l
⊢ a ++ b ∈ m∗ * n
have ih₁ : ∀ m_1 < a.length + b.length, ∀ ⦃x : List α⦄ (hx : x ∈ l) (hlen : x.length = m_1), x ∈ m∗ * n
Tactic: rw [length_append] at ih
Cleared hypotheses: ih, hx
-- Lean 4 proof step from Mathlib.Computability.Language (hypothesis)
Goal:
α : Type u_1
l m n : Language α
hm : [] ∉ m
h : l = m * l + n
a : List α
ha : a ∈ m
b : List α
hb : b ∈ l
ih : ∀ m_1 < a.length + b.length, ∀ ⦃x : List α⦄ (hx : x ∈ l) (hlen : x.length = m_1), x ∈ m∗ * n
hx : a ++ b ∈ m * l
⊢ a ++ b ∈ m∗ * n
have hal : 0 < a.length
Tactic: have hal : 0 < a.length := length_pos_iff.mpr <| ne_of_mem_of_not_mem ha hm
-- Lean 4 proof step from Mathlib.Computability.Language (hypothesis)
Goal:
α : Type u_1
l m n : Language α
hm : [] ∉ m
h : l = m * l + n
a : List α
ha : a ∈ m
b : List α
hb : b ∈ l
ih : ∀ m_1 < a.length + b.length, ∀ ⦃x : List α⦄ (hx : x ∈ l) (hlen : x.length = m_1), x ∈ m∗ * n
hx : a ++ b ∈ m * l
hal : 0 < a.length
⊢ a ++ b ∈ m∗ * n
have ih₁ : b ∈ m∗ * n
Tactic: specialize ih b.length (Nat.lt_add_left_iff_pos.mpr hal) hb rfl
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.Computability.Language (goal)
Goal:
α : Type u_1
l m n : Language α
hm : [] ∉ m
h : l = m * l + n
a : List α
ha : a ∈ m
b : List α
hb : b ∈ l
hx : a ++ b ∈ m * l
hal : 0 < a.length
ih : b ∈ m∗ * n
⊢ a ++ b ∈ m∗ * n
have a₁ : a ++ b ∈ n + m * (m∗ * n)
Tactic: rw [← one_add_self_mul_kstar_eq_kstar, one_add_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.Computability.Language (goal)
Goal:
α : Type u_1
l m n : Language α
hm : [] ∉ m
h : l = m * l + n
a : List α
ha : a ∈ m
b : List α
hb : b ∈ l
hx : a ++ b ∈ m * l
hal : 0 < a.length
ih : b ∈ m∗ * n
⊢ a ++ b ∈ n + m * (m∗ * n)
have a₁ : a ++ b ∈ m * (m∗ * n)
Tactic: right
-- Lean 4 proof step from Mathlib.Computability.Language (goal)
Goal:
α : Type u_1
l m n : Language α
hm : [] ∉ m
h : l = m * l + n
⊢ m∗ * n ≤ l
have a : ∀ (i : ℕ), m ^ i * n ≤ l
Tactic: rw [kstar_eq_iSup_pow, iSup_mul, iSup_le_iff]
-- Lean 4 proof step from Mathlib.Computability.Language (goal)
Goal:
α : Type u_1
l m n : Language α
hm : [] ∉ m
h : l = m * l + n
⊢ HPow.hPow (β := ℕ) m 0 * n ≤ l
have a : HPow.hPow (β := ℕ) m 0 * n ≤ m * l + n
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Computability.Language (goal)
Goal:
α : Type u_1
l m n : Language α
hm : [] ∉ m
h : l = m * l + n
⊢ HPow.hPow (β := ℕ) m 0 * n ≤ m * l + n
have a : n ≤ n + m * l
Tactic: rw [pow_zero, one_mul, add_comm]
-- Lean 4 proof step from Mathlib.Computability.Language (goal)
Goal:
α : Type u_1
l m n : Language α
hm : [] ∉ m
h : l = m * l + n
n_1 : ℕ
ih : m ^ n_1 * n ≤ l
⊢ m ^ (n_1 + 1) * n ≤ l
have a : m ^ (n_1 + 1) * n ≤ m * l + n
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Computability.Language (goal)
Goal:
α : Type u_1
l m n : Language α
hm : [] ∉ m
h : l = m * l + n
n_1 : ℕ
ih : m ^ n_1 * n ≤ l
⊢ m ^ (n_1 + 1) * n ≤ m * l + n
have a : m * l ≤ m * l + n
Tactic: grw [add_comm, pow_add, pow_one, mul_assoc, ih]
-- Lean 4 proof step from Mathlib.Computability.Language (goal)
Goal:
α : Type u_1
l m n : Language α
hm : [] ∉ m
h : l = m * l + n
i : ℕ
⊢ m ^ i * n ≤ l
have a : HPow.hPow (β := ℕ) m 0 * n ≤ l
Tactic: induction i with rw [h]
      | zero =>
        rw [pow_zero, one_mul, add_comm]
        exact le_self_add
      | succ _ ih =>
        grw [add_comm, pow_add, pow_one, mul_assoc, ih]
        exact le_self_add
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Computability.Language (goal)
Goal:
α : Type u_1
l m n : Language α
hm : [] ∉ m
h : l = m * l + n
i : ℕ
a : HPow.hPow (β := ℕ) m 0 * n ≤ l
⊢ m ^ i * n ≤ l
have a₁ : HPow.hPow (β := ℕ) m 0 * n ≤ m * l + n
Tactic: induction i with rw [h]
      | zero =>
        rw [pow_zero, one_mul, add_comm]
        exact le_self_add
      | succ _ ih =>
        grw [add_comm, pow_add, pow_one, mul_assoc, ih]
        exact le_self_add
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Computability.Language (goal)
Goal:
α : Type u_1
l m n : Language α
hm : [] ∉ m
h : l = m * l + n
i : ℕ
a : HPow.hPow (β := ℕ) m 0 * n ≤ l
a₁ : HPow.hPow (β := ℕ) m 0 * n ≤ m * l + n
⊢ m ^ i * n ≤ l
have a₂ : ∀ (n_1 : ℕ) (ih : m ^ n_1 * n ≤ l), m ^ (n_1 + 1) * n ≤ l
Tactic: induction i with rw [h]
      | zero =>
        rw [pow_zero, one_mul, add_comm]
        exact le_self_add
      | succ _ ih =>
        grw [add_comm, pow_add, pow_one, mul_assoc, ih]
        exact le_self_add
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Computability.Language (goal)
Goal:
α : Type u_1
l m n : Language α
hm : [] ∉ m
h : l = m * l + n
i : ℕ
a : HPow.hPow (β := ℕ) m 0 * n ≤ l
a₁ : HPow.hPow (β := ℕ) m 0 * n ≤ m * l + n
a₂ : ∀ (n_1 : ℕ) (ih : m ^ n_1 * n ≤ l), m ^ (n_1 + 1) * n ≤ l
⊢ m ^ i * n ≤ l
have a₃ : ∀ (n_1 : ℕ) (ih : m ^ n_1 * n ≤ l), m ^ (n_1 + 1) * n ≤ m * l + n
Tactic: induction i with rw [h]
      | zero =>
        rw [pow_zero, one_mul, add_comm]
        exact le_self_add
      | succ _ ih =>
        grw [add_comm, pow_add, pow_one, mul_assoc, ih]
        exact le_self_add
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Computability.Language (goal)
Goal:
α : Type u_1
l m n : Language α
hm : [] ∉ m
h : l = m∗ * n
⊢ l = m * l + n
have rw : m∗ * n = m * (m∗ * n) + n
Tactic: rw [h, add_comm, ← mul_assoc, ← one_add_mul, one_add_self_mul_kstar_eq_kstar]
-- Lean 4 proof step from Mathlib.Computability.Language (goal)
Goal:
α : Type u_1
l m n : Language α
hm : [] ∉ m
h : l = m∗ * n
rw : m∗ * n = m * (m∗ * n) + n
⊢ l = m * l + n
have rw₁ : m∗ * n = n + m * (m∗ * n)
Tactic: rw [h, add_comm, ← mul_assoc, ← one_add_mul, one_add_self_mul_kstar_eq_kstar]
-- Lean 4 proof step from Mathlib.Computability.Language (goal)
Goal:
α : Type u_1
l m n : Language α
hm : [] ∉ m
h : l = m∗ * n
rw : m∗ * n = m * (m∗ * n) + n
rw₁ : m∗ * n = n + m * (m∗ * n)
⊢ l = m * l + n
have rw₂ : m∗ * n = n + m * m∗ * n
Tactic: rw [h, add_comm, ← mul_assoc, ← one_add_mul, one_add_self_mul_kstar_eq_kstar]
-- Lean 4 proof step from Mathlib.Computability.Language (goal)
Goal:
α : Type u_1
l m n : Language α
hm : [] ∉ m
h : l = m∗ * n
rw : m∗ * n = m * (m∗ * n) + n
rw₁ : m∗ * n = n + m * (m∗ * n)
rw₂ : m∗ * n = n + m * m∗ * n
⊢ l = m * l + n
have rw₃ : m∗ * n = (1 + m * m∗) * n
Tactic: rw [h, add_comm, ← mul_assoc, ← one_add_mul, one_add_self_mul_kstar_eq_kstar]
-- Lean 4 proof step from Mathlib.Computability.Language (goal)
Goal:
α : Type u_1
l m n : Language α
hm : [] ∉ m
h : l = m∗ * n
rw : m∗ * n = m * (m∗ * n) + n
rw₁ : m∗ * n = n + m * (m∗ * n)
rw₂ : m∗ * n = n + m * m∗ * n
rw₃ : m∗ * n = (1 + m * m∗) * n
⊢ l = m * l + n
have rw₄ : m∗ * n = m∗ * n
Tactic: rw [h, add_comm, ← mul_assoc, ← one_add_mul, one_add_self_mul_kstar_eq_kstar]
-- Lean 4 proof step from Mathlib.Computability.Language (goal)
Goal:
α : Type u_1
l : Language α
a : List α
⊢ a.reverse ∈ l.reverse ↔ a ∈ l
have rw : a.reverse.reverse ∈ l ↔ a ∈ l
Tactic: rw [mem_reverse, List.reverse_reverse]
-- Lean 4 proof step from Mathlib.Computability.Language (goal)
Goal:
α : Type u_1
l : Language α
a : List α
rw : a.reverse.reverse ∈ l ↔ a ∈ l
⊢ a.reverse ∈ l.reverse ↔ a ∈ l
have rw₁ : a ∈ l ↔ a ∈ l
Tactic: rw [mem_reverse, List.reverse_reverse]
-- Lean 4 proof step from Mathlib.Computability.Language (goal)
Goal:
α : Type u_1
l m : Language α
⊢ (l * m).reverse = m.reverse * l.reverse
have simp : Eq (α := Language α) (image2 (fun (a b : List α) ↦ b.reverse ++ a.reverse) l m)
  (image2 (fun (a b : List α) ↦ a.reverse ++ b.reverse) m l)
Tactic: simp only [mul_def, reverse_eq_image, image2_image_left, image2_image_right, image_image2,
    List.reverse_append]
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
Goal:
α : Type u
σ : Type v
M : NFA α σ
S T : Set σ
a : α
⊢ M.stepSet (S ∪ T) a = M.stepSet S a ∪ M.stepSet T a
have h : ∀ (s : σ), s ∈ M.stepSet (S ∪ T) a ↔ s ∈ M.stepSet S a ∪ M.stepSet T a
Tactic: ext s
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
Goal:
α : Type u
σ : Type v
M : NFA α σ
S T : Set σ
x : List α
⊢ M.evalFrom (S ∪ T) x = M.evalFrom S x ∪ M.evalFrom T x
have nil : ∀ (S T : Set σ), M.evalFrom (S ∪ T) [] = M.evalFrom S [] ∪ M.evalFrom T []
Tactic: induction x generalizing S T with
  | nil => simp
  | cons a x ih => simp [ih]
Cleared hypotheses: S, T, x
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
Goal:
α : Type u
σ : Type v
M : NFA α σ
S T : Set σ
x : List α
nil : ∀ (S T : Set σ), M.evalFrom (S ∪ T) [] = M.evalFrom S [] ∪ M.evalFrom T []
⊢ M.evalFrom (S ∪ T) x = M.evalFrom S x ∪ M.evalFrom T x
have cons : ∀ (a : α) (x : List α) (ih : ∀ (S T : Set σ), M.evalFrom (S ∪ T) x = M.evalFrom S x ∪ M.evalFrom T x) (S T : Set σ),
  M.evalFrom (S ∪ T) (a :: x) = M.evalFrom S (a :: x) ∪ M.evalFrom T (a :: x)
Tactic: induction x generalizing S T with
  | nil => simp
  | cons a x ih => simp [ih]
Cleared hypotheses: S, T, x
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
Goal:
α : Type u
σ : Type v
M : NFA α σ
ι : Sort u_1
s : ι → Set σ
x : List α
⊢ M.evalFrom (⋃ (i : ι), s i) x = ⋃ (i : ι), M.evalFrom (s i) x
have nil : ∀ (s : ι → Set σ), M.evalFrom (⋃ (i : ι), s i) [] = ⋃ (i : ι), M.evalFrom (s i) []
Tactic: induction x generalizing s with
  | nil => simp
  | cons a x ih => simp [stepSet, Set.iUnion_comm (ι := σ) (ι' := ι), ih]
Cleared hypotheses: s, x