awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.Halting
Goal:
C : Set (ℕ →. ℕ)
h : ComputablePred fun (c : Code) ↦ c.eval ∈ C
f g : ℕ →. ℕ
hf : Nat.Partrec f
hg : Nat.Partrec g
fC : f ∈ C
obtain :
  ∀ (w : DecidablePred fun (c : Code) ↦ c.eval ∈ C)
    (h : Computable (σ := Bool) fun (a : Code) ↦ decide ((fun (c : Code) ↦ c.eval ∈ C) a)), g ∈ C
⊢ g ∈ C

Tactic:
obtain ⟨_, h⟩ := h
-- Module: Mathlib.Computability.Halting
Goal:
C : Set (ℕ →. ℕ)
f g : ℕ →. ℕ
hf : Nat.Partrec f
hg : Nat.Partrec g
fC : f ∈ C
w : DecidablePred fun (c : Code) ↦ c.eval ∈ C
h : Computable (σ := Bool) fun (a : Code) ↦ decide ((fun (c : Code) ↦ c.eval ∈ C) a)
obtain :
  ∀ (c : Code)
    (e :
      c.eval = fun (b : ℕ) ↦
        bif decide ((fun (c : Code) ↦ c.eval ∈ C) (c, b).1) then (fun (a : Code) (b : ℕ) ↦ g (a, b).2) (c, b).1 (c, b).2
        else (fun (a : Code) (b : ℕ) ↦ f (a, b).2) (c, b).1 (c, b).2),
    g ∈ C
⊢ g ∈ C

Tactic:
obtain ⟨c, e⟩ :=
    fixed_point₂
      (Partrec.cond (h.comp fst) ((Partrec.nat_iff.2 hg).comp snd).to₂
          ((Partrec.nat_iff.2 hf).comp snd).to₂).to₂

Premises used: Iff.mpr, Nat.Partrec.Code.fixed_point₂, Computable.snd, Partrec.nat_iff, Computable.comp, Partrec.cond, Partrec.to₂, Computable.fst, Partrec.comp
-- Module: Mathlib.Computability.Halting
Goal:
C : Set (ℕ →. ℕ)
f g : ℕ →. ℕ
hf : Nat.Partrec f
hg : Nat.Partrec g
fC : f ∈ C
w : DecidablePred fun (c : Code) ↦ c.eval ∈ C
h : Computable (σ := Bool) fun (a : Code) ↦ decide ((fun (c : Code) ↦ c.eval ∈ C) a)
c : Code
e :
  c.eval = fun (b : ℕ) ↦
    bif decide ((fun (c : Code) ↦ c.eval ∈ C) (c, b).1) then (fun (a : Code) (b : ℕ) ↦ g (a, b).2) (c, b).1 (c, b).2
    else (fun (a : Code) (b : ℕ) ↦ f (a, b).2) (c, b).1 (c, b).2
⊢ c.eval = fun (b : ℕ) ↦ if c.eval ∈ C then g b else f b

Tactic:
simp only [Bool.cond_decide] at e

Premises used: Bool.cond_decide
-- Module: Mathlib.Computability.Halting
Goal:
C : Set (ℕ →. ℕ)
f g : ℕ →. ℕ
hf : Nat.Partrec f
hg : Nat.Partrec g
fC : f ∈ C
w : DecidablePred fun (c : Code) ↦ c.eval ∈ C
h : Computable (σ := Bool) fun (a : Code) ↦ decide ((fun (c : Code) ↦ c.eval ∈ C) a)
c : Code
e : c.eval = fun (b : ℕ) ↦ if c.eval ∈ C then g b else f b
pos : ∀ (H : c.eval ∈ C), g ∈ C
neg : ∀ (H : c.eval ∉ C), g ∈ C
⊢ g ∈ C

Tactic:
by_cases H : eval c ∈ C

Premises used: Nat.Partrec.Code.eval
-- Module: Mathlib.Computability.Halting
Goal:
C : Set (ℕ →. ℕ)
f g : ℕ →. ℕ
hf : Nat.Partrec f
hg : Nat.Partrec g
fC : f ∈ C
w : DecidablePred fun (c : Code) ↦ c.eval ∈ C
h : Computable (σ := Bool) fun (a : Code) ↦ decide ((fun (c : Code) ↦ c.eval ∈ C) a)
c : Code
e : c.eval = fun (b : ℕ) ↦ if c.eval ∈ C then g b else f b
H : c.eval ∈ C
⊢ g ∈ C

Tactic:
simp_all
-- Module: Mathlib.Computability.Halting
Goal:
C : Set (ℕ →. ℕ)
f g : ℕ →. ℕ
hf : Nat.Partrec f
hg : Nat.Partrec g
fC : f ∈ C
w : DecidablePred fun (c : Code) ↦ c.eval ∈ C
h : Computable (σ := Bool) fun (a : Code) ↦ decide ((fun (c : Code) ↦ c.eval ∈ C) a)
c : Code
e : c.eval = fun (b : ℕ) ↦ if c.eval ∈ C then g b else f b
H : c.eval ∉ C
⊢ g ∈ C

Tactic:
simp_all
-- Module: Mathlib.Computability.Halting
Goal:
C : Set Code
H : ∀ (cf cg : Code), cf.eval = cg.eval → (cf ∈ C ↔ cg ∈ C)
hC : ∀ (f : Code), f ∈ C ↔ f.eval ∈ eval '' C
h : C = ∅ ∨ C = Set.univ
inl :
  ∀
    (H :
      ∀ (cf cg : Code), cf.eval = cg.eval → (Membership.mem (γ := Set Code) ∅ cf ↔ Membership.mem (γ := Set Code) ∅ cg))
    (hC : ∀ (f : Code), Membership.mem (γ := Set Code) ∅ f ↔ f.eval ∈ eval '' ∅),
    ComputablePred fun (c : Code) ↦ Membership.mem (γ := Set Code) ∅ c
inr :
  ∀
    (H :
      ∀ (cf cg : Code),
        cf.eval = cg.eval → (Membership.mem (γ := Set Code) Set.univ cf ↔ Membership.mem (γ := Set Code) Set.univ cg))
    (hC : ∀ (f : Code), Membership.mem (γ := Set Code) Set.univ f ↔ f.eval ∈ eval '' Set.univ),
    ComputablePred fun (c : Code) ↦ Membership.mem (γ := Set Code) Set.univ c
⊢ ComputablePred fun (c : Code) ↦ c ∈ C

Tactic:
obtain rfl | rfl := h

Premises used: rfl
-- Module: Mathlib.Computability.Halting
Goal:
H : ∀ (cf cg : Code), cf.eval = cg.eval → (Membership.mem (γ := Set Code) ∅ cf ↔ Membership.mem (γ := Set Code) ∅ cg)
hC : ∀ (f : Code), Membership.mem (γ := Set Code) ∅ f ↔ f.eval ∈ eval '' ∅
⊢ ComputablePred fun (c : Code) ↦ Membership.mem (γ := Set Code) ∅ c

Tactic:
simpa [ComputablePred, Set.mem_empty_iff_false] using
            Computable.const _

Premises used: Set.mem_empty_iff_false, ComputablePred, Computable.const
-- Module: Mathlib.Computability.Halting
Goal:
H :
  ∀ (cf cg : Code),
    cf.eval = cg.eval → (Membership.mem (γ := Set Code) Set.univ cf ↔ Membership.mem (γ := Set Code) Set.univ cg)
hC : ∀ (f : Code), Membership.mem (γ := Set Code) Set.univ f ↔ f.eval ∈ eval '' Set.univ
⊢ ComputablePred fun (c : Code) ↦ Membership.mem (γ := Set Code) Set.univ c

Tactic:
simpa [ComputablePred, Set.mem_empty_iff_false] using
            Computable.const _

Premises used: Set.mem_empty_iff_false, ComputablePred, Computable.const
-- Module: Mathlib.Computability.Halting
Goal:
C : Set Code
H : ∀ (cf cg : Code), cf.eval = cg.eval → (cf ∈ C ↔ cg ∈ C)
hC : ∀ (f : Code), f ∈ C ↔ f.eval ∈ eval '' C
h : C = ∅ ∨ C = Set.univ
inl :
  ∀
    (H :
      ∀ (cf cg : Code), cf.eval = cg.eval → (Membership.mem (γ := Set Code) ∅ cf ↔ Membership.mem (γ := Set Code) ∅ cg))
    (hC : ∀ (f : Code), Membership.mem (γ := Set Code) ∅ f ↔ f.eval ∈ eval '' ∅),
    ComputablePred fun (c : Code) ↦ Membership.mem (γ := Set Code) ∅ c
inr :
  ∀
    (H :
      ∀ (cf cg : Code),
        cf.eval = cg.eval → (Membership.mem (γ := Set Code) Set.univ cf ↔ Membership.mem (γ := Set Code) Set.univ cg))
    (hC : ∀ (f : Code), Membership.mem (γ := Set Code) Set.univ f ↔ f.eval ∈ eval '' Set.univ),
    ComputablePred fun (c : Code) ↦ Membership.mem (γ := Set Code) Set.univ c
inl₁ :
  ∀
    (H :
      ∀ (cf cg : Code), cf.eval = cg.eval → (Membership.mem (γ := Set Code) ∅ cf ↔ Membership.mem (γ := Set Code) ∅ cg))
    (hC : ∀ (f : Code), Membership.mem (γ := Set Code) ∅ f ↔ f.eval ∈ eval '' ∅),
    ComputablePred fun (c : Code) ↦ Membership.mem (γ := Set Code) ∅ c
inr₁ :
  ∀
    (H :
      ∀ (cf cg : Code),
        cf.eval = cg.eval → (Membership.mem (γ := Set Code) Set.univ cf ↔ Membership.mem (γ := Set Code) Set.univ cg))
    (hC : ∀ (f : Code), Membership.mem (γ := Set Code) Set.univ f ↔ f.eval ∈ eval '' Set.univ),
    ComputablePred fun (c : Code) ↦ Membership.mem (γ := Set Code) Set.univ c
inl₂ :
  ∀
    (H :
      ∀ (cf cg : Code), cf.eval = cg.eval → (Membership.mem (γ := Set Code) ∅ cf ↔ Membership.mem (γ := Set Code) ∅ cg))
    (hC : ∀ (f : Code), Membership.mem (γ := Set Code) ∅ f ↔ f.eval ∈ eval '' ∅),
    ComputablePred fun (c : Code) ↦ Membership.mem (γ := Set Code) ∅ c
inr₂ :
  ∀
    (H :
      ∀ (cf cg : Code),
        cf.eval = cg.eval → (Membership.mem (γ := Set Code) Set.univ cf ↔ Membership.mem (γ := Set Code) Set.univ cg))
    (hC : ∀ (f : Code), Membership.mem (γ := Set Code) Set.univ f ↔ f.eval ∈ eval '' Set.univ),
    ComputablePred fun (c : Code) ↦ Membership.mem (γ := Set Code) Set.univ c
inl₃ :
  ∀
    (H :
      ∀ (cf cg : Code), cf.eval = cg.eval → (Membership.mem (γ := Set Code) ∅ cf ↔ Membership.mem (γ := Set Code) ∅ cg))
    (hC : ∀ (f : Code), Membership.mem (γ := Set Code) ∅ f ↔ f.eval ∈ eval '' ∅),
    ComputablePred fun (c : Code) ↦ Membership.mem (γ := Set Code) ∅ c
inr₃ :
  ∀
    (H :
      ∀ (cf cg : Code),
        cf.eval = cg.eval → (Membership.mem (γ := Set Code) Set.univ cf ↔ Membership.mem (γ := Set Code) Set.univ cg))
    (hC : ∀ (f : Code), Membership.mem (γ := Set Code) Set.univ f ↔ f.eval ∈ eval '' Set.univ),
    ComputablePred fun (c : Code) ↦ Membership.mem (γ := Set Code) Set.univ c
⊢ ComputablePred fun (c : Code) ↦ c ∈ C

Tactic:
{
          obtain rfl | rfl := h <;> simpa [ComputablePred, Set.mem_empty_iff_false] using
            Computable.const _}

Premises used: Set.mem_empty_iff_false, ComputablePred, Computable.const, rfl
-- Module: Mathlib.Computability.Halting
Goal:
C : Set Code
H : ∀ (cf cg : Code), cf.eval = cg.eval → (cf ∈ C ↔ cg ∈ C)
⊢ (ComputablePred fun (c : Code) ↦ c ∈ C) ↔ C = ∅ ∨ C = Set.univ

Tactic:
exact
      have hC : ∀ f, f ∈ C ↔ eval f ∈ eval '' C := fun f =>
        ⟨Set.mem_image_of_mem _, fun ⟨g, hg, e⟩ => (H _ _ e).1 hg⟩
      ⟨fun h =>
        or_iff_not_imp_left.2 fun C0 =>
          Set.eq_univ_of_forall fun cg =>
            let ⟨cf, fC⟩ := Set.nonempty_iff_ne_empty.2 C0
            (hC _).2 <|
              rice (eval '' C) (h.of_eq hC)
                (Partrec.nat_iff.1 <| eval_part.comp (const cf) Computable.id)
                (Partrec.nat_iff.1 <| eval_part.comp (const cg) Computable.id) ((hC _).1 fC),
        fun h => by {
          obtain rfl | rfl := h <;> simpa [ComputablePred, Set.mem_empty_iff_false] using
            Computable.const _}⟩

Premises used: Membership.mem, _private.0.ComputablePred.rice₂.match_1, Set.mem_image_of_mem, Iff.intro, Iff.mp, Nat.Partrec.Code.eval
-- Module: Mathlib.Computability.Halting
Goal:
C : Set Code
H : ∀ (cf cg : Code), cf.eval = cg.eval → (cf ∈ C ↔ cg ∈ C)
⊢ (ComputablePred fun (c : Code) ↦ c ∈ C) ↔ C = ∅ ∨ C = Set.univ

Tactic:
classical exact
      have hC : ∀ f, f ∈ C ↔ eval f ∈ eval '' C := fun f =>
        ⟨Set.mem_image_of_mem _, fun ⟨g, hg, e⟩ => (H _ _ e).1 hg⟩
      ⟨fun h =>
        or_iff_not_imp_left.2 fun C0 =>
          Set.eq_univ_of_forall fun cg =>
            let ⟨cf, fC⟩ := Set.nonempty_iff_ne_empty.2 C0
            (hC _).2 <|
              rice (eval '' C) (h.of_eq hC)
                (Partrec.nat_iff.1 <| eval_part.comp (const cf) Computable.id)
                (Partrec.nat_iff.1 <| eval_part.comp (const cg) Computable.id) ((hC _).1 fC),
        fun h => by {
          obtain rfl | rfl := h <;> simpa [ComputablePred, Set.mem_empty_iff_false] using
            Computable.const _}⟩

Premises used: Membership.mem, _private.0.ComputablePred.rice₂.match_1, Set.mem_image_of_mem, Iff.intro, Iff.mp, Nat.Partrec.Code.eval
-- Module: Mathlib.Computability.Halting
Goal:
n : ℕ
⊢ REPred fun (c : Code) ↦ (c.eval n).Dom

Tactic:
(eval_part.comp Computable.id (Computable.const _)).dom_re

Premises used: Partrec₂.comp, Nat.Partrec.Code.eval_part, Partrec.dom_re, Computable.const, Computable.id
-- Module: Mathlib.Computability.Language
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := Language α) 0 ∅

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Computability.Language
Goal:
α : Type u_1
⊢ Eq (α := Language α) 1 {[]}

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Computability.Language
Goal:
α : Type u_1
l m : Language α
⊢ l + m = l ∪ m

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Computability.Language
Goal:
α : Type u_1
l m : Language α
⊢ l - m = l \ m

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Computability.Language
Goal:
α : Type u_1
l m : Language α
⊢ l * m = image2 (fun (x1 x2 : List α) ↦ x1 ++ x2) l m

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Computability.Language
Goal:
α : Type u_1
l : Language α
⊢ l∗ = {x : List α | ∃ (L : List (List α)), x = L.flatten ∧ ∀ y ∈ L, y ∈ l}

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Computability.Language
Goal:
α : Type u_1
l m : Language α
h : ∀ (x : List α), x ∈ l ↔ x ∈ m
⊢ l = m

Tactic:
Set.ext h

Premises used: Set.ext, Language
-- Module: Mathlib.Computability.Language
Goal:
α : Type u_1
x : List α
⊢ x ∉ 0

Tactic:
id

Premises used: Set.Mem, id, Not
-- Module: Mathlib.Computability.Language
Goal:
α : Type u_1
x : List α
⊢ Membership.mem (γ := Language α) 1 x ↔ x = []

Tactic:
rfl
-- Module: Mathlib.Computability.Language
Goal:
α : Type u_1
⊢ Membership.mem (γ := Language α) 1 []

Tactic:
Set.mem_singleton _

Premises used: Set.mem_singleton, Set.Mem
-- Module: Mathlib.Computability.Language
Goal:
α : Type u_1
l m : Language α
x : List α
⊢ x ∈ l + m ↔ x ∈ l ∨ x ∈ m

Tactic:
Iff.rfl

Premises used: Set.union, Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.Computability.Language
Goal:
α : Type u_1
l m : Language α
x : List α
⊢ x ∈ l - m ↔ x ∈ l ∧ x ∉ m

Tactic:
Iff.rfl

Premises used: Set.Mem, Set.diff, Iff.rfl, setOf
-- Module: Mathlib.Computability.Language
Goal:
α : Type u_1
l m : Language α
x : List α
⊢ x ∈ l * m ↔ ∃ a ∈ l, ∃ b ∈ m, a ++ b = x

Tactic:
mem_image2

Premises used: Set.Mem, Set.mem_image2
-- Module: Mathlib.Computability.Language
Goal:
α : Type u_1
l m : Language α
a b : List α
⊢ a ∈ l → b ∈ m → a ++ b ∈ l * m

Tactic:
mem_image2_of_mem

Premises used: Set.Mem, Set.mem_image2_of_mem
-- Module: Mathlib.Computability.Language
Goal:
α : Type u_1
l : Language α
x : List α
⊢ x ∈ l∗ ↔ ∃ (L : List (List α)), x = L.flatten ∧ ∀ y ∈ L, y ∈ l

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.Computability.Language
Goal:
α : Type u_1
l : Language α
L : List (List α)
h : ∀ y ∈ L, y ∈ l
⊢ L.flatten ∈ l∗

Tactic:
⟨L, rfl, h⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, rfl
-- Module: Mathlib.Computability.Language
Goal:
α : Type u_1
l : Language α
x : List α
h : Membership.mem (γ := List (List α)) [] x
⊢ x ∈ l

Tactic:
contradiction
-- Module: Mathlib.Computability.Language
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
l_1 m : Language α
a b x : List α
l : Language α
⊢ 1 * l = l

Tactic:
simp [mul_def, one_def]

Premises used: Language.mul_def, Language.one_def
-- Module: Mathlib.Computability.Language
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
l_1 m : Language α
a b x : List α
l : Language α
⊢ l * 1 = l

Tactic:
simp [mul_def, one_def]

Premises used: Language.mul_def, Language.one_def
-- Module: Mathlib.Computability.Language
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
l m : Language α
a b x : List α
n : ℕ
zero : (if HAdd.hAdd (α := ℕ) 0 1 = 0 then 0 else 1) = HAdd.hAdd (α := Language α) (if Eq (α := ℕ) 0 0 then 0 else 1) 1
succ : ∀ (n : ℕ), (if n + 1 + 1 = 0 then 0 else 1) = HAdd.hAdd (α := Language α) (if n + 1 = 0 then 0 else 1) 1
⊢ (if n + 1 = 0 then 0 else 1) = HAdd.hAdd (α := Language α) (if n = 0 then 0 else 1) 1

Tactic:
cases n
-- Module: Mathlib.Computability.Language
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
l m : Language α
a b x : List α
⊢ (if HAdd.hAdd (α := ℕ) 0 1 = 0 then 0 else 1) = HAdd.hAdd (α := Language α) (if Eq (α := ℕ) 0 0 then 0 else 1) 1

Tactic:
simp [add_def, zero_def]

Premises used: Language.zero_def, Language.add_def
-- Module: Mathlib.Computability.Language
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
l m : Language α
a b x : List α
n : ℕ
⊢ (if n + 1 + 1 = 0 then 0 else 1) = HAdd.hAdd (α := Language α) (if n + 1 = 0 then 0 else 1) 1

Tactic:
simp [add_def, zero_def]

Premises used: Language.zero_def, Language.add_def
-- Module: Mathlib.Computability.Language
Goal:
α : Type u_1
l : Language α
⊢ l + l = l

Tactic:
sup_idem _

Premises used: sup_idem
-- Module: Mathlib.Computability.Language
Goal:
α : Type u_1
l : Language α
⊢ (map id : (a : Language α) → Language α) l = l

Tactic:
simp [map]

Premises used: Language.map
-- Module: Mathlib.Computability.Language
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
g : β → γ
f : α → β
l : Language α
⊢ Eq.{u_3 + 1} (α := Language γ)
    ((map g : (a : Language β) → Language γ) ((map f : (a : Language α) → Language β) l) : Language γ)
    ((map (g ∘ f) : (a : Language α) → Language γ) l : Language γ)

Tactic:
simp [map, image_image]

Premises used: Set.image_image, Language.map
-- Module: Mathlib.Computability.Language
Goal:
α : Type u_1
l : Language α
x : List α
mp : x ∈ l∗ → ∃ (S : List (List α)), x = S.flatten ∧ ∀ y ∈ S, y ∈ l ∧ y ≠ []
mpr : (∃ (S : List (List α)), x = S.flatten ∧ ∀ y ∈ S, y ∈ l ∧ y ≠ []) → x ∈ l∗
⊢ x ∈ l∗ ↔ ∃ (S : List (List α)), x = S.flatten ∧ ∀ y ∈ S, y ∈ l ∧ y ≠ []

Tactic:
constructor
-- Module: Mathlib.Computability.Language
Goal:
α : Type u_1
l : Language α
S : List (List α)
h : ∀ y ∈ S, y ∈ l
⊢ S.flatten = (filter (fun (l : List α) ↦ !l.isEmpty) S).flatten

Tactic:
simp [List.flatten_filter_not_isEmpty]

Premises used: List.flatten_filter_not_isEmpty
-- Module: Mathlib.Computability.Language
Goal:
α : Type u_1
l : Language α
S : List (List α)
h : ∀ y ∈ S, y ∈ l
mp : ∀ (y : List α) (hy : y ∈ filter (fun (l : List α) ↦ !l.isEmpty) S), y ∈ l ∧ y ≠ []
⊢ ∃ (S_1 : List (List α)), S.flatten = S_1.flatten ∧ ∀ y ∈ S_1, y ∈ l ∧ y ≠ []

Tactic:
refine ⟨S.filter fun l ↦ !List.isEmpty l,
      by simp [List.flatten_filter_not_isEmpty], fun y hy ↦ ?_⟩
-- Module: Mathlib.Computability.Language
Goal:
α : Type u_1
l : Language α
S : List (List α)
h : ∀ y ∈ S, y ∈ l
y : List α
hy : y ∈ filter (fun (l : List α) ↦ !l.isEmpty) S
⊢ y ∈ S ∧ ¬y = []

Tactic:
simp only [mem_filter, Bool.not_eq_eq_eq_not, Bool.not_true, isEmpty_eq_false_iff, ne_eq] at hy

Premises used: ne_eq, List.mem_filter, Bool.not_eq_eq_eq_not, List.isEmpty_eq_false_iff, Bool.not_true
-- Module: Mathlib.Computability.Language
Goal:
α : Type u_1
l : Language α
S : List (List α)
h : ∀ y ∈ S, y ∈ l
y : List α
hy : y ∈ S ∧ ¬y = []
⊢ y ∈ l ∧ y ≠ []

Tactic:
⟨h y hy.1, hy.2⟩

Premises used: And.right, And.left, And.intro
-- Module: Mathlib.Computability.Language
Goal:
α : Type u_1
l : Language α
S : List (List α)
h : ∀ y ∈ S, y ∈ l
y : List α
hy : y ∈ S ∧ ¬y = []
⊢ y ∈ l ∧ y ≠ []

Tactic:
exact ⟨h y hy.1, hy.2⟩
-- Module: Mathlib.Computability.Language
Goal:
α : Type u_1
l : Language α
x : List α
S : List (List α)
hx : x = S.flatten
h : ∀ y ∈ S, y ∈ l ∧ y ≠ []
⊢ x ∈ l∗

Tactic:
⟨S, hx, fun y hy ↦ (h y hy).1⟩

Premises used: Set.Mem, setOf, And.left, And.intro, Exists.intro
-- Module: Mathlib.Computability.Language
Goal:
α : Type u_1
l : Language α
x : List α
S : List (List α)
hx : x = S.flatten
h : ∀ y ∈ S, y ∈ l ∧ y ≠ []
⊢ x ∈ l∗

Tactic:
exact ⟨S, hx, fun y hy ↦ (h y hy).1⟩
-- Module: Mathlib.Computability.Language
Goal:
α : Type u_1
l : Language α
h :
  ∀ (x : List α),
    x ∈ l∗ ↔
      Membership.mem (γ := Language α) {x : List α | ∃ (S : List (List α)), x = S.flatten ∧ ∀ y ∈ S, y ∈ l ∧ y ≠ []} x
⊢ l∗ = {x : List α | ∃ (S : List (List α)), x = S.flatten ∧ ∀ y ∈ S, y ∈ l ∧ y ≠ []}

Tactic:
ext x
-- Module: Mathlib.Computability.Language
Goal:
α : Type u_1
l : Language α
x : List α
⊢ x ∈ l∗ ↔
    Membership.mem (γ := Language α) {x : List α | ∃ (S : List (List α)), x = S.flatten ∧ ∀ y ∈ S, y ∈ l ∧ y ≠ []} x

Tactic:
apply mem_kstar_iff_exists_nonempty

Premises used: Language.mem_kstar_iff_exists_nonempty
-- Module: Mathlib.Computability.Language
Goal:
α : Type u_1
l m : Language α
⊢ l ≤ m ↔ l + m = m

Tactic:
sup_eq_right.symm

Premises used: sup_eq_right, Iff.symm
-- Module: Mathlib.Computability.Language
Goal:
α : Type u_1
ι : Sort v
l : ι → Language α
x : List α
⊢ Membership.mem (γ := Language α) (⨆ (i : ι), l i) x ↔ ∃ (i : ι), x ∈ l i

Tactic:
mem_iUnion

Premises used: Set.Mem, Set.mem_iUnion, Language, Set.iUnion
-- Module: Mathlib.Computability.Language
Goal:
α : Type u_1
ι : Sort v
l : ι → Language α
m : Language α
⊢ (⨆ (i : ι), l i) * m = ⨆ (i : ι), l i * m

Tactic:
image2_iUnion_left _ _ _

Premises used: Set.image2_iUnion_left, Language, Set.iUnion
-- Module: Mathlib.Computability.Language
Goal:
α : Type u_1
ι : Sort v
l : ι → Language α
m : Language α
⊢ m * ⨆ (i : ι), l i = ⨆ (i : ι), m * l i

Tactic:
image2_iUnion_right _ _ _

Premises used: Set.image2_iUnion_right, Language, Set.iUnion
-- Module: Mathlib.Computability.Language
Goal:
α : Type u_1
ι : Sort v
inst : Nonempty ι
l : ι → Language α
m : Language α
⊢ (⨆ (i : ι), l i) + m = ⨆ (i : ι), l i + m

Tactic:
iSup_sup

Premises used: iSup_sup
-- Module: Mathlib.Computability.Language
Goal:
α : Type u_1
ι : Sort v
inst : Nonempty ι
l : ι → Language α
m : Language α
⊢ m + ⨆ (i : ι), l i = ⨆ (i : ι), m + l i

Tactic:
sup_iSup

Premises used: sup_iSup
-- Module: Mathlib.Computability.Language
Goal:
α : Type u_1
ι : Sort v
l : ι → Language α
m : Language α
⊢ (⨆ (i : ι), l i) - m = ⨆ (i : ι), l i - m

Tactic:
iUnion_diff _ _

Premises used: Set.iUnion_diff, Language, Set.iUnion
-- Module: Mathlib.Computability.Language
Goal:
α : Type u_1
ι : Sort v
inst : Nonempty ι
l : ι → Language α
m : Language α
⊢ m - ⨆ (i : ι), l i = ⨅ (i : ι), m - l i

Tactic:
diff_iUnion _ _

Premises used: Set.iInter, Set.diff_iUnion, Language, Set.iUnion
-- Module: Mathlib.Computability.Language
Goal:
α : Type u_1
l : Language α
x : List α
⊢ x ∈ HPow.hPow (β := ℕ) l 0 ↔ ∃ (S : List (List α)), x = S.flatten ∧ S.length = 0 ∧ ∀ y ∈ S, y ∈ l

Tactic:
simp
-- Module: Mathlib.Computability.Language
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
⊢ x ∈ l ^ (n + 1) ↔ ∃ (S : List (List α)), x = S.flatten ∧ S.length = n + 1 ∧ ∀ y ∈ S, y ∈ l

Tactic:
simp only [pow_succ', mem_mul, ihn]

Premises used: Language.mem_mul, pow_succ'
-- Module: Mathlib.Computability.Language
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
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
⊢ (∃ 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
-- Module: Mathlib.Computability.Language
Goal:
α : Type u_1
l : Language α
a : List α
ha : a ∈ l
S : List (List α)
hS : ∀ y ∈ 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
⊢ ∃ (S_1 : List (List α)), a ++ S.flatten = S_1.flatten ∧ S_1.length = S.length + 1 ∧ ∀ y ∈ S_1, y ∈ l

Tactic:
⟨a :: S, rfl, rfl, forall_mem_cons.2 ⟨ha, hS⟩⟩

Premises used: Iff.mpr, List.cons, List.forall_mem_cons, And.intro, Exists.intro, rfl
-- Module: Mathlib.Computability.Language
Goal:
α : Type u_1
l : Language α
a : List α
ha : a ∈ l
S : List (List α)
hS : ∀ y ∈ 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
⊢ ∃ (S_1 : List (List α)), a ++ S.flatten = S_1.flatten ∧ S_1.length = S.length + 1 ∧ ∀ y ∈ S_1, y ∈ l

Tactic:
exact ⟨a :: S, rfl, rfl, forall_mem_cons.2 ⟨ha, hS⟩⟩
-- Module: Mathlib.Computability.Language
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
hn : length.{u_1} (α := List α) [] = n + 1
hS : ∀ (y : List α), Membership.mem (γ := List (List α)) [] y → y ∈ l
⊢ ∃ a ∈ l, ∃ (b : List α), (∃ (S : List (List α)), b = S.flatten ∧ S.length = n ∧ ∀ y ∈ S, y ∈ l) ∧ a ++ b = flatten []

Tactic:
cases hn
-- Module: Mathlib.Computability.Language
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
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
⊢ ∃ a_1 ∈ l,
    ∃ (b : List α), (∃ (S : List (List α)), b = S.flatten ∧ S.length = n ∧ ∀ y ∈ S, y ∈ l) ∧ a_1 ++ b = (a :: S).flatten

Tactic:
cases hn
-- 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
⊢ a ∈ l ∧ ∀ x ∈ S, x ∈ l

Tactic:
rw [forall_mem_cons] at hS

Premises used: List.forall_mem_cons