-- Mathlib/Computability/Language.lean
theorem mem_pow {l : Language α} {x : List α} {n : ℕ} :
    x ∈ l ^ n ↔ ∃ S : List (List α), x = S.flatten ∧ S.length = n ∧ ∀ y ∈ S, y ∈ l

Proof state:
case succ.mpr.intro.cons.intro.intro.refl
α : 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, x = S_1.flatten ∧ S_1.length = S.length ∧ ∀ y ∈ S_1, y ∈ l
⊢ ∃ a_1 ∈ l, ∃ b, (∃ S_1, b = S_1.flatten ∧ S_1.length = S.length ∧ ∀ y ∈ S_1, y ∈ l) ∧ a_1 ++ b = (a :: S).flatten

Tactic:
rw [forall_mem_cons] at hS

Result:
case succ.mpr.intro.cons.intro.intro.refl
α : 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, x = S_1.flatten ∧ S_1.length = S.length ∧ ∀ y ∈ S_1, y ∈ l
⊢ ∃ a_1 ∈ l, ∃ b, (∃ S_1, b = S_1.flatten ∧ S_1.length = S.length ∧ ∀ y ∈ S_1, y ∈ l) ∧ a_1 ++ b = (a :: S).flatten

Proof state:
α : Type u_1
l : Language α
x✝ : List α
h : x✝ ∈ []
⊢ x✝ ∈ l

Tactic:
contradiction

Result:
no goals

Proof state:
case zero.mp
α : Type u_1
l : Language α
x : List α
⊢ x = [] → ∃ S, x = S.flatten ∧ S = [] ∧ ∀ y ∈ S, y ∈ l

Tactic:
rintro rfl

Result:
case zero.mp
α : Type u_1
l : Language α
⊢ ∃ S, [] = S.flatten ∧ S = [] ∧ ∀ y ∈ S, y ∈ l

Proof state:
case succ.mpr.intro.cons.intro.intro.refl
α : 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, x = S_1.flatten ∧ S_1.length = S.length ∧ ∀ y ∈ S_1, y ∈ l
⊢ ∃ a_1 ∈ l, ∃ b, (∃ S_1, 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⟩

Result:
no goals

Proof state:
α : Type u_1
l : Language α
x : List α
n : ℕ
⊢ x ∈ l ^ n ↔ ∃ S, x = S.flatten ∧ S.length = n ∧ ∀ y ∈ S, y ∈ l

Tactic:
induction' n with n ihn generalizing x

Result:
case zero
α : Type u_1
l : Language α
x : List α
⊢ x ∈ l ^ 0 ↔ ∃ S, x = S.flatten ∧ S.length = 0 ∧ ∀ y ∈ S, y ∈ l

case succ
α : Type u_1
l : Language α
n : ℕ
ihn : ∀ {x : List α}, x ∈ l ^ n ↔ ∃ S, x = S.flatten ∧ S.length = n ∧ ∀ y ∈ S, y ∈ l
x : List α
⊢ x ∈ l ^ (n + 1) ↔ ∃ S, x = S.flatten ∧ S.length = n + 1 ∧ ∀ y ∈ S, y ∈ l

Proof state:
case zero
α : Type u_1
l : Language α
x : List α
⊢ x ∈ l ^ 0 ↔ ∃ S, x = S.flatten ∧ S.length = 0 ∧ ∀ y ∈ S, y ∈ l

Tactic:
simp only [mem_one, pow_zero, length_eq_zero]

Result:
case zero
α : Type u_1
l : Language α
x : List α
⊢ x = [] ↔ ∃ S, x = S.flatten ∧ S = [] ∧ ∀ y ∈ S, y ∈ l

Proof state:
case zero.mpr
α : Type u_1
l : Language α
x : List α
⊢ (∃ S, x = S.flatten ∧ S = [] ∧ ∀ y ∈ S, y ∈ l) → x = []

Tactic:
rintro ⟨_, rfl, rfl, _⟩

Result:
case zero.mpr.intro.intro.intro
α : Type u_1
l : Language α
right✝ : ∀ y ∈ [], y ∈ l
⊢ [].flatten = []

Proof state:
case succ.mpr
α : Type u_1
l : Language α
n : ℕ
ihn : ∀ {x : List α}, x ∈ l ^ n ↔ ∃ S, x = S.flatten ∧ S.length = n ∧ ∀ y ∈ S, y ∈ l
x : List α
⊢ (∃ S, x = S.flatten ∧ S.length = n + 1 ∧ ∀ y ∈ S, y ∈ l) →
    ∃ a ∈ l, ∃ b, (∃ S, b = S.flatten ∧ S.length = n ∧ ∀ y ∈ S, y ∈ l) ∧ a ++ b = x

Tactic:
rintro ⟨_ | ⟨a, S⟩, rfl, hn, hS⟩ <;> cases hn

Result:
case succ.mpr.intro.cons.intro.intro.refl
α : 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, x = S_1.flatten ∧ S_1.length = S.length ∧ ∀ y ∈ S_1, y ∈ l
⊢ ∃ a_1 ∈ l, ∃ b, (∃ S_1, b = S_1.flatten ∧ S_1.length = S.length ∧ ∀ y ∈ S_1, y ∈ l) ∧ a_1 ++ b = (a :: S).flatten

Proof state:
case succ
α : Type u_1
l : Language α
n : ℕ
ihn : ∀ {x : List α}, x ∈ l ^ n ↔ ∃ S, x = S.flatten ∧ S.length = n ∧ ∀ y ∈ S, y ∈ l
x : List α
⊢ x ∈ l ^ (n + 1) ↔ ∃ S, x = S.flatten ∧ S.length = n + 1 ∧ ∀ y ∈ S, y ∈ l

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

Result:
case succ
α : Type u_1
l : Language α
n : ℕ
ihn : ∀ {x : List α}, x ∈ l ^ n ↔ ∃ S, x = S.flatten ∧ S.length = n ∧ ∀ y ∈ S, y ∈ l
x : List α
⊢ (∃ a ∈ l, ∃ b, (∃ S, b = S.flatten ∧ S.length = n ∧ ∀ y ∈ S, y ∈ l) ∧ a ++ b = x) ↔
    ∃ S, x = S.flatten ∧ S.length = n + 1 ∧ ∀ y ∈ S, y ∈ l

Proof state:
case zero.mpr.intro.intro.intro
α : Type u_1
l : Language α
right✝ : ∀ y ∈ [], y ∈ l
⊢ [].flatten = []

Tactic:
rfl

Result:
no goals

Proof state:
case zero
α : Type u_1
l : Language α
x : List α
⊢ x = [] ↔ ∃ S, x = S.flatten ∧ S = [] ∧ ∀ y ∈ S, y ∈ l

Tactic:
constructor

Result:
case zero.mp
α : Type u_1
l : Language α
x : List α
⊢ x = [] → ∃ S, x = S.flatten ∧ S = [] ∧ ∀ y ∈ S, y ∈ l

case zero.mpr
α : Type u_1
l : Language α
x : List α
⊢ (∃ S, x = S.flatten ∧ S = [] ∧ ∀ y ∈ S, y ∈ l) → x = []

Proof state:
case succ.mp.intro.intro.intro.intro.intro.intro.intro
α : 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, x = S_1.flatten ∧ S_1.length = S.length ∧ ∀ y ∈ S_1, y ∈ l
⊢ ∃ S_1, 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⟩⟩

Result:
no goals

Proof state:
case succ
α : Type u_1
l : Language α
n : ℕ
ihn : ∀ {x : List α}, x ∈ l ^ n ↔ ∃ S, x = S.flatten ∧ S.length = n ∧ ∀ y ∈ S, y ∈ l
x : List α
⊢ (∃ a ∈ l, ∃ b, (∃ S, b = S.flatten ∧ S.length = n ∧ ∀ y ∈ S, y ∈ l) ∧ a ++ b = x) ↔
    ∃ S, x = S.flatten ∧ S.length = n + 1 ∧ ∀ y ∈ S, y ∈ l

Tactic:
constructor

Result:
case succ.mp
α : Type u_1
l : Language α
n : ℕ
ihn : ∀ {x : List α}, x ∈ l ^ n ↔ ∃ S, x = S.flatten ∧ S.length = n ∧ ∀ y ∈ S, y ∈ l
x : List α
⊢ (∃ a ∈ l, ∃ b, (∃ S, b = S.flatten ∧ S.length = n ∧ ∀ y ∈ S, y ∈ l) ∧ a ++ b = x) →
    ∃ S, x = S.flatten ∧ S.length = n + 1 ∧ ∀ y ∈ S, y ∈ l

case succ.mpr
α : Type u_1
l : Language α
n : ℕ
ihn : ∀ {x : List α}, x ∈ l ^ n ↔ ∃ S, x = S.flatten ∧ S.length = n ∧ ∀ y ∈ S, y ∈ l
x : List α
⊢ (∃ S, x = S.flatten ∧ S.length = n + 1 ∧ ∀ y ∈ S, y ∈ l) →
    ∃ a ∈ l, ∃ b, (∃ S, b = S.flatten ∧ S.length = n ∧ ∀ y ∈ S, y ∈ l) ∧ a ++ b = x

Proof state:
case zero.mp
α : Type u_1
l : Language α
⊢ ∃ S, [] = S.flatten ∧ S = [] ∧ ∀ y ∈ S, y ∈ l

Tactic:
exact ⟨[], rfl, rfl, fun _ h ↦ by contradiction⟩

Result:
no goals

Proof state:
case succ.mp
α : Type u_1
l : Language α
n : ℕ
ihn : ∀ {x : List α}, x ∈ l ^ n ↔ ∃ S, x = S.flatten ∧ S.length = n ∧ ∀ y ∈ S, y ∈ l
x : List α
⊢ (∃ a ∈ l, ∃ b, (∃ S, b = S.flatten ∧ S.length = n ∧ ∀ y ∈ S, y ∈ l) ∧ a ++ b = x) →
    ∃ S, x = S.flatten ∧ S.length = n + 1 ∧ ∀ y ∈ S, y ∈ l

Tactic:
rintro ⟨a, ha, b, ⟨S, rfl, rfl, hS⟩, rfl⟩

Result:
case succ.mp.intro.intro.intro.intro.intro.intro.intro
α : 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, x = S_1.flatten ∧ S_1.length = S.length ∧ ∀ y ∈ S_1, y ∈ l
⊢ ∃ S_1, a ++ S.flatten = S_1.flatten ∧ S_1.length = S.length + 1 ∧ ∀ y ∈ S_1, y ∈ l