awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.Language
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
hS₁ : a ∈ l ∧ ∀ x ∈ S, x ∈ l
⊢ ∀ {x : List α}, x ∈ l ^ S.length ↔ ∃ (S_1 : List (List α)), x = S_1.flatten ∧ S_1.length = S.length ∧ ∀ y ∈ S_1, y ∈ l

Tactic:
rw [forall_mem_cons] at hS

Premises used: List.forall_mem_cons
-- Module: Mathlib.Computability.Language
Goal:
α : Type u_1
l : Language α
a : List α
S : List (List α)
hS : a ∈ l ∧ ∀ x ∈ S, x ∈ 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

Tactic:
⟨a, hS.1, _, ⟨S, rfl, rfl, hS.2⟩, rfl⟩

Premises used: And.right, And.left, And.intro, Exists.intro, rfl
-- Module: Mathlib.Computability.Language
Goal:
α : Type u_1
l : Language α
a : List α
S : List (List α)
hS : a ∈ l ∧ ∀ x ∈ S, x ∈ 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

Tactic:
exact ⟨a, hS.1, _, ⟨S, rfl, rfl, hS.2⟩, rfl⟩
-- Module: Mathlib.Computability.Language
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
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
⊢ x ∈ l ^ n ↔ ∃ (S : List (List α)), x = S.flatten ∧ S.length = n ∧ ∀ 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⟩

Premises used: Language.mem_mul, List.forall_mem_cons, pow_succ', rfl
-- Module: Mathlib.Computability.Language
Goal:
α : Type u_1
l : Language α
h : ∀ (x : List α), x ∈ l∗ ↔ Membership.mem (γ := Language α) (⨆ (i : ℕ), l ^ i) x
⊢ l∗ = ⨆ (i : ℕ), l ^ i

Tactic:
ext x
-- Module: Mathlib.Computability.Language
Goal:
α : Type u_1
l : Language α
x : List α
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
⊢ x ∈ l∗ ↔ Membership.mem (γ := Language α) (⨆ (i : ℕ), l ^ i) x

Tactic:
simp only [mem_kstar, mem_iSup, mem_pow]

Premises used: Language.mem_iSup, Language.mem_pow, Language.mem_kstar
-- Module: Mathlib.Computability.Language
Goal:
α : Type u_1
l : Language α
x : List α
⊢ (∃ (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:
grind
-- Module: Mathlib.Computability.Language
Goal:
α : Type u_1
β : Type u_2
f : α → β
l : Language α
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)
⊢ Eq.{u_2 + 1} (α := Language β) ((map f : (a : Language α) → Language β) l∗ : Language β)
    (((map f : (a : Language α) → Language β) l)∗ : Language β)

Tactic:
rw [kstar_eq_iSup_pow, kstar_eq_iSup_pow]

Premises used: Language.kstar_eq_iSup_pow
-- Module: Mathlib.Computability.Language
Goal:
α : Type u_1
β : Type u_2
f : α → β
l : Language α
simp_rw :
  Eq.{u_2 + 1} (α := Language β) ((map f : (a : Language α) → Language β) (⨆ (i : ℕ), l ^ i))
    (⨆ (i : ℕ), (map f : (a : Language α) → Language β) (l ^ i))
⊢ 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:
simp_rw [← map_pow]

Premises used: map_pow
-- Module: Mathlib.Computability.Language
Goal:
α : Type u_1
β : Type u_2
f : α → β
l : Language α
⊢ Eq.{u_2 + 1} (α := Language β) ((map f : (a : Language α) → Language β) (⨆ (i : ℕ), l ^ i))
    (⨆ (i : ℕ), (map f : (a : Language α) → Language β) (l ^ i))

Tactic:
image_iUnion

Premises used: Set.Mem, setOf, Set.image_iUnion, Set.image, Language, Set.iUnion
-- Module: Mathlib.Computability.Language
Goal:
α : Type u_1
β : Type u_2
f : α → β
l : Language α
⊢ Eq.{u_2 + 1} (α := Language β) ((map f : (a : Language α) → Language β) (⨆ (i : ℕ), l ^ i))
    (⨆ (i : ℕ), (map f : (a : Language α) → Language β) (l ^ i))

Tactic:
exact image_iUnion

Premises used: Set.image_iUnion
-- Module: Mathlib.Computability.Language
Goal:
α : Type u_1
l : Language α
⊢ l∗ * l = l * l∗

Tactic:
simp only [kstar_eq_iSup_pow, mul_iSup, iSup_mul, ← pow_succ, ← pow_succ']

Premises used: pow_succ, Language.iSup_mul, Language.mul_iSup, Language.kstar_eq_iSup_pow, pow_succ'
-- Module: Mathlib.Computability.Language
Goal:
α : Type u_1
l : Language α
simp : HPow.hPow (β := ℕ) l 0 + ⨆ (i : ℕ), l ^ (i + 1) = ⨆ (i : ℕ), l ^ i
⊢ 1 + l * l∗ = l∗

Tactic:
simp only [kstar_eq_iSup_pow, mul_iSup, ← pow_succ', ← pow_zero l]

Premises used: pow_zero, Language.mul_iSup, Language.kstar_eq_iSup_pow, pow_succ'
-- Module: Mathlib.Computability.Language
Goal:
α : Type u_1
l : Language α
⊢ HPow.hPow (β := ℕ) l 0 + ⨆ (i : ℕ), l ^ (i + 1) = ⨆ (i : ℕ), l ^ i

Tactic:
sup_iSup_nat_succ _

Premises used: sup_iSup_nat_succ
-- Module: Mathlib.Computability.Language
Goal:
α : Type u_1
l : Language α
⊢ HPow.hPow (β := ℕ) l 0 + ⨆ (i : ℕ), l ^ (i + 1) = ⨆ (i : ℕ), l ^ i

Tactic:
exact sup_iSup_nat_succ _

Premises used: sup_iSup_nat_succ
-- Module: Mathlib.Computability.Language
Goal:
α : Type u_1
l : Language α
rw : 1 + l * l∗ = l∗
rw₁ rw₂ : l∗ = l∗
⊢ 1 + l∗ * l = l∗

Tactic:
rw [mul_self_kstar_comm, one_add_self_mul_kstar_eq_kstar]

Premises used: Language.one_add_self_mul_kstar_eq_kstar, Language.mul_self_kstar_comm
-- Module: Mathlib.Computability.Language
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
l m : Language α
a_1 b x : List α
a : Language α
x_1 : List α
hl : Membership.mem (γ := Set (List α)) 1 x_1
⊢ ∀ (y : List α), Membership.mem (γ := List (List α)) [] y → y ∈ a

Tactic:
simp
-- Module: Mathlib.Computability.Language
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
rw : ⨆ (i : ℕ), m * l ^ i ≤ m
⊢ m * l∗ ≤ m

Tactic:
rw [kstar_eq_iSup_pow, mul_iSup]

Premises used: Language.mul_iSup, Language.kstar_eq_iSup_pow
-- Module: Mathlib.Computability.Language
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

Tactic:
iSup_le fun n ↦ ?_

Premises used: iSup_le
-- Module: Mathlib.Computability.Language
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
refine : ∀ (n : ℕ), m * l ^ n ≤ m
⊢ ⨆ (i : ℕ), m * l ^ i ≤ m

Tactic:
refine iSup_le fun n ↦ ?_

Premises used: iSup_le
-- Module: Mathlib.Computability.Language
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 * HPow.hPow (β := ℕ) l 0 ≤ m

Tactic:
simp
-- Module: Mathlib.Computability.Language
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
succ₃ succ₄ : m ≤ m
⊢ m * l ^ (n + 1) ≤ m

Tactic:
grw [pow_succ, ← mul_assoc m (l ^ n) l, ih, h]

Premises used: pow_succ, mul_assoc, HPow.hPow
-- Module: Mathlib.Computability.Language
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
succ : ∀ (n : ℕ) (ih : m * l ^ n ≤ m), m * l ^ (n + 1) ≤ m
⊢ m * l ^ n ≤ m

Tactic:
induction n with
    | zero => simp
    | succ n ih => grw [pow_succ, ← mul_assoc m (l ^ n) l, ih, h]

Premises used: pow_succ, mul_assoc, HPow.hPow
-- Module: Mathlib.Computability.Language
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
rw : ⨆ (i : ℕ), l ^ i * m ≤ m
⊢ l∗ * m ≤ m

Tactic:
rw [kstar_eq_iSup_pow, iSup_mul]

Premises used: Language.iSup_mul, Language.kstar_eq_iSup_pow
-- Module: Mathlib.Computability.Language
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

Tactic:
iSup_le fun n ↦ ?_

Premises used: iSup_le
-- Module: Mathlib.Computability.Language
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
refine : ∀ (n : ℕ), l ^ n * m ≤ m
⊢ ⨆ (i : ℕ), l ^ i * m ≤ m

Tactic:
refine iSup_le fun n ↦ ?_

Premises used: iSup_le
-- Module: Mathlib.Computability.Language
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
⊢ HPow.hPow (β := ℕ) l 0 * m ≤ m

Tactic:
simp
-- Module: Mathlib.Computability.Language
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
succ₃ succ₄ : m ≤ m
⊢ l ^ (n + 1) * m ≤ m

Tactic:
grw [pow_succ, mul_assoc, h, ih]

Premises used: pow_succ, mul_assoc
-- Module: Mathlib.Computability.Language
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
succ : ∀ (n : ℕ) (ih : l ^ n * m ≤ m), l ^ (n + 1) * m ≤ m
⊢ l ^ n * m ≤ m

Tactic:
induction n with
    | zero => simp
    | succ n ih => grw [pow_succ, mul_assoc, h, ih]

Premises used: pow_succ, mul_assoc
-- Module: Mathlib.Computability.Language
Goal:
α : Type u_1
l m n : Language α
hm : [] ∉ m
h : l = m * l + n
a : l ≤ m∗ * n
a₁ : m∗ * n ≤ l
⊢ l = m∗ * n

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Computability.Language
Goal:
α : Type u_1
l m n : Language α
hm : [] ∉ m
h : l = m * l + n
x : List α
hx : x ∈ l
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
⊢ x ∈ m∗ * n

Tactic:
induction hlen : x.length using Nat.strong_induction_on generalizing x with | _ _ ih

Premises used: List.length
-- Module: Mathlib.Computability.Language
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
⊢ ∀ m_1 < x.length, ∀ ⦃x : List α⦄ (hx : x ∈ l) (hlen : x.length = m_1), x ∈ m∗ * n

Tactic:
subst hlen
-- Module: Mathlib.Computability.Language
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 * l + n

Tactic:
rw [h] at hx
-- Module: Mathlib.Computability.Language
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
hx₁ : x ∈ m * l + n
⊢ ∀ m_1 < x.length, ∀ ⦃x : List α⦄ (hx : x ∈ l) (hlen : x.length = m_1), x ∈ m∗ * n

Tactic:
rw [h] at hx
-- Module: Mathlib.Computability.Language
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
a₁ : ∀ (hx : x ∈ n), x ∈ m∗ * n
⊢ x ∈ m∗ * n

Tactic:
obtain hx | hx := hx
-- Module: Mathlib.Computability.Language
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
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
⊢ x ∈ m∗ * n

Tactic:
obtain ⟨a, ha, b, hb, rfl⟩ := mem_mul.mp hx

Premises used: Language.mem_mul, Iff.mp, rfl
-- Module: Mathlib.Computability.Language
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
⊢ ∀ 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

Premises used: List.length_append
-- Module: Mathlib.Computability.Language
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
ih₁ : ∀ m_1 < a.length + b.length, ∀ ⦃x : List α⦄ (hx : x ∈ l) (hlen : x.length = m_1), x ∈ m∗ * n
⊢ a ++ b ∈ m * l

Tactic:
rw [length_append] at ih

Premises used: List.length_append
-- Module: Mathlib.Computability.Language
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
⊢ 0 < a.length

Tactic:
have hal : 0 < a.length := length_pos_iff.mpr <| ne_of_mem_of_not_mem ha hm
-- Module: Mathlib.Computability.Language
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
⊢ b ∈ m∗ * n

Tactic:
specialize ih b.length (Nat.lt_add_left_iff_pos.mpr hal) hb rfl

Premises used: Iff.mpr, Nat.lt_add_left_iff_pos, List.length, rfl
-- Module: Mathlib.Computability.Language
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₁ : a ++ b ∈ n + m * (m∗ * n)
⊢ a ++ b ∈ m∗ * n

Tactic:
rw [← one_add_self_mul_kstar_eq_kstar, one_add_mul, mul_assoc]

Premises used: mul_assoc, Language.one_add_self_mul_kstar_eq_kstar, one_add_mul
-- Module: Mathlib.Computability.Language
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₁ : a ++ b ∈ m * (m∗ * n)
⊢ a ++ b ∈ n + m * (m∗ * n)

Tactic:
right
-- Module: Mathlib.Computability.Language
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 * (m∗ * n)

Tactic:
⟨_, ha, _, ih, rfl⟩

Premises used: Set.Mem, setOf, Set.image2, And.intro, Exists.intro, rfl
-- Module: Mathlib.Computability.Language
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 * (m∗ * n)

Tactic:
exact ⟨_, ha, _, ih, rfl⟩
-- Module: Mathlib.Computability.Language
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 ∈ n
⊢ x ∈ m∗ * n

Tactic:
⟨[], nil_mem_kstar _, _, ⟨hx, nil_append _⟩⟩

Premises used: Set.Mem, setOf, Set.image2, And.intro, List.nil_append, Exists.intro, Language.nil_mem_kstar, List.nil
-- Module: Mathlib.Computability.Language
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 ∈ n
⊢ x ∈ m∗ * n

Tactic:
exact ⟨[], nil_mem_kstar _, _, ⟨hx, nil_append _⟩⟩
-- Module: Mathlib.Computability.Language
Goal:
α : Type u_1
l m n : Language α
hm : [] ∉ m
h : l = m * l + n
a : ∀ (i : ℕ), m ^ i * n ≤ l
⊢ m∗ * n ≤ l

Tactic:
rw [kstar_eq_iSup_pow, iSup_mul, iSup_le_iff]

Premises used: Language.iSup_mul, iSup_le_iff, Language.kstar_eq_iSup_pow
-- Module: Mathlib.Computability.Language
Goal:
α : Type u_1
l m n : Language α
hm : [] ∉ m
h : l = m * l + n
a : HPow.hPow (β := ℕ) m 0 * n ≤ m * l + n
⊢ HPow.hPow (β := ℕ) m 0 * n ≤ l

Tactic:
rw [h]
-- Module: Mathlib.Computability.Language
Goal:
α : Type u_1
l m n : Language α
hm : [] ∉ m
h : l = m * l + n
a : n ≤ n + m * l
⊢ HPow.hPow (β := ℕ) m 0 * n ≤ m * l + n

Tactic:
rw [pow_zero, one_mul, add_comm]

Premises used: add_comm, pow_zero, one_mul
-- Module: Mathlib.Computability.Language
Goal:
α : Type u_1
l m n : Language α
hm : [] ∉ m
h : l = m * l + n
⊢ n ≤ n + m * l

Tactic:
le_self_add

Premises used: le_self_add
-- Module: Mathlib.Computability.Language
Goal:
α : Type u_1
l m n : Language α
hm : [] ∉ m
h : l = m * l + n
⊢ n ≤ n + m * l

Tactic:
exact le_self_add

Premises used: le_self_add
-- Module: Mathlib.Computability.Language
Goal:
α : Type u_1
l m n : Language α
hm : [] ∉ m
h : l = m * l + n
n_1 : ℕ
ih : m ^ n_1 * n ≤ l
a : m ^ (n_1 + 1) * n ≤ m * l + n
⊢ m ^ (n_1 + 1) * n ≤ l

Tactic:
rw [h]
-- Module: Mathlib.Computability.Language
Goal:
α : Type u_1
l m n : Language α
hm : [] ∉ m
h : l = m * l + n
n_1 : ℕ
ih : m ^ n_1 * n ≤ l
a : m * l ≤ m * l + n
⊢ m ^ (n_1 + 1) * n ≤ m * l + n

Tactic:
grw [add_comm, pow_add, pow_one, mul_assoc, ih]

Premises used: mul_assoc, pow_add, add_comm, pow_one
-- Module: Mathlib.Computability.Language
Goal:
α : Type u_1
l m n : Language α
hm : [] ∉ m
h : l = m * l + n
n_1 : ℕ
ih : m ^ n_1 * n ≤ l
⊢ m * l ≤ m * l + n

Tactic:
le_self_add

Premises used: le_self_add
-- Module: Mathlib.Computability.Language
Goal:
α : Type u_1
l m n : Language α
hm : [] ∉ m
h : l = m * l + n
n_1 : ℕ
ih : m ^ n_1 * n ≤ l
⊢ m * l ≤ m * l + n

Tactic:
exact le_self_add

Premises used: le_self_add
-- Module: Mathlib.Computability.Language
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
a₃ : ∀ (n_1 : ℕ) (ih : m ^ n_1 * n ≤ l), m ^ (n_1 + 1) * n ≤ m * l + n
⊢ m ^ i * 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

Premises used: mul_assoc, pow_add, add_comm, pow_zero, pow_one, le_self_add, one_mul
-- Module: Mathlib.Computability.Language
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
rw₄ rw₅ : m∗ * n = m∗ * n
⊢ l = m * l + n

Tactic:
rw [h, add_comm, ← mul_assoc, ← one_add_mul, one_add_self_mul_kstar_eq_kstar]

Premises used: mul_assoc, Language.one_add_self_mul_kstar_eq_kstar, add_comm, one_add_mul
-- Module: Mathlib.Computability.Language
Goal:
α : Type u_1
l : Language α
a : List α
⊢ a ∈ l.reverse ↔ a.reverse ∈ l

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Language.reverse
-- Module: Mathlib.Computability.Language
Goal:
α : Type u_1
l : Language α
a : List α
rw : a.reverse.reverse ∈ l ↔ a ∈ l
rw₁ rw₂ : a ∈ l ↔ a ∈ l
⊢ a.reverse ∈ l.reverse ↔ a ∈ l

Tactic:
rw [mem_reverse, List.reverse_reverse]

Premises used: Language.mem_reverse, List.reverse_reverse
-- Module: Mathlib.Computability.Language
Goal:
α : Type u_1
l : Language α
⊢ l.reverse = List.reverse '' l

Tactic:
((List.reverse_involutive.toPerm _).image_eq_preimage_symm _).symm

Premises used: Set.Mem, setOf, Language.reverse, Function.Involutive.toPerm, Equiv.image_eq_preimage_symm, List.reverse, List.reverse_involutive, Language, Eq.symm
-- Module: Mathlib.Computability.Language
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := Language α) (reverse 0) 0

Tactic:
rfl

Premises used: Set.Mem, setOf, Language.reverse, rfl
-- Module: Mathlib.Computability.Language
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := Language α) (reverse 1) 1

Tactic:
simp [reverse, ← one_def]

Premises used: Language.reverse, Language.one_def
-- Module: Mathlib.Computability.Language
Goal:
α : Type u_1
⊢ Function.Involutive.{u_1 + 1} (α := Language α) reverse

Tactic:
List.reverse_involutive.preimage

Premises used: setOf, Language.reverse, Function.Involutive.preimage, List.reverse_involutive, Language
-- Module: Mathlib.Computability.Language
Goal:
α : Type u_1
⊢ Function.Bijective.{u_1 + 1, u_1 + 1} (α := Language α) reverse

Tactic:
reverse_involutive.bijective

Premises used: Function.Involutive.bijective, Language.reverse_involutive
-- Module: Mathlib.Computability.Language
Goal:
α : Type u_1
⊢ Function.Injective.{u_1 + 1, u_1 + 1} (α := Language α) reverse

Tactic:
reverse_involutive.injective

Premises used: Function.Involutive.injective, Language.reverse_involutive
-- Module: Mathlib.Computability.Language
Goal:
α : Type u_1
⊢ Function.Surjective.{u_1 + 1, u_1 + 1} (α := Language α) reverse

Tactic:
reverse_involutive.surjective

Premises used: Function.Involutive.surjective, Language.reverse_involutive
-- Module: Mathlib.Computability.Language
Goal:
α : Type u_1
l : Language α
⊢ l.reverse.reverse = l

Tactic:
reverse_involutive l

Premises used: Language.reverse_involutive
-- Module: Mathlib.Computability.Language
Goal:
α : Type u_1
l m : Language α
⊢ (l + m).reverse = l.reverse + m.reverse

Tactic:
rfl

Premises used: Set.union, Set.Mem, setOf, Language.reverse, List.reverse, rfl
-- Module: Mathlib.Computability.Language
Goal:
α : Type u_1
l m : Language α
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)
⊢ (l * m).reverse = m.reverse * l.reverse

Tactic:
simp only [mul_def, reverse_eq_image, image2_image_left, image2_image_right, image_image2,
    List.reverse_append]

Premises used: Set.image2_image_right, Language.mul_def, Set.image2_image_left, Set.image_image2, Language.reverse_eq_image, List.reverse_append
-- Module: Mathlib.Computability.Language
Goal:
α : Type u_1
l m : Language α
⊢ 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:
apply image2_swap

Premises used: Set.image2_swap
-- Module: Mathlib.Computability.Language
Goal:
α : Type u_1
ι : Sort u_4
l : ι → Language α
⊢ Eq.{u_1 + 1} (α := Language α) (reverse (⨆ (i : ι), l i)) (⨆ (i : ι), (l i).reverse)

Tactic:
preimage_iUnion

Premises used: Set.Mem, setOf, Language.reverse, Set.preimage_iUnion, Language, Set.iUnion
-- Module: Mathlib.Computability.Language
Goal:
α : Type u_1
ι : Sort u_4
l : ι → Language α
⊢ Eq.{u_1 + 1} (α := Language α) (reverse (⨅ (i : ι), l i)) (⨅ (i : ι), (l i).reverse)

Tactic:
preimage_iInter

Premises used: Set.Mem, Set.iInter, setOf, Language.reverse, Set.preimage_iInter, Language
-- Module: Mathlib.Computability.Language
Goal:
α : Type u_1
l : Language α
n : ℕ
⊢ (l ^ n).reverse = l.reverse ^ n

Tactic:
MulOpposite.op_injective (map_pow (reverseIso α) l n)

Premises used: MulOpposite.op_injective, map_pow, Language.reverseIso
-- Module: Mathlib.Computability.Language
Goal:
α : Type u_1
l : Language α
⊢ l∗.reverse = l.reverse∗

Tactic:
simp only [kstar_eq_iSup_pow, reverse_iSup, reverse_pow]

Premises used: Language.reverse_iSup, Language.reverse_pow, Language.kstar_eq_iSup_pow
-- Module: Mathlib.Computability.Language
Goal:
α : Type u_1
x : List α
l m : Language α
⊢ x ∈ l ⊓ m ↔ x ∈ l ∧ x ∈ m

Tactic:
apply Set.mem_inter_iff

Premises used: Set.mem_inter_iff
-- Module: Mathlib.Computability.Language
Goal:
α : Type u_1
l : Language α
⊢ lᶜᶜ = l

Tactic:
_root_.compl_compl l

Premises used: compl_compl