case h
α : Type u_1
β : Type ?u.98971
γ : Type ?u.98974
l✝ m : Language α
a b x✝ : List α
l : Language α
x : List α
⊢ x ∈ l∗ ↔ x ∈ ⨆ (i : ℕ), l ^ i
α : Type u_1
β : Type ?u.98971
γ : Type ?u.98974
l✝ m : Language α
a b x : List α
l : Language α
⊢ l∗ = ⨆ (i : ℕ), l ^ i
ext x
case h
α : Type u_1
β : Type ?u.98971
γ : Type ?u.98974
l✝ m : Language α
a b x✝ : List α
l : Language α
x : List α
⊢ (∃ L, x = join L ∧ ∀ (y : List α), y ∈ L → y ∈ l) ↔ ∃ i S, x = join S ∧ length S = i ∧ ∀ (y : List α), y ∈ S → y ∈ l
case h
α : Type u_1
β : Type ?u.98971
γ : Type ?u.98974
l✝ m : Language α
a b x✝ : List α
l : Language α
x : List α
⊢ x ∈ l∗ ↔ x ∈ ⨆ (i : ℕ), l ^ i
simp only [mem_kstar, mem_iSup, mem_pow]
case h.mp
α : Type u_1
β : Type ?u.98971
γ : Type ?u.98974
l✝ m : Language α
a b x✝ : List α
l : Language α
x : List α
⊢ (∃ L, x = join L ∧ ∀ (y : List α), y ∈ L → y ∈ l) → ∃ i S, x = join S ∧ length S = i ∧ ∀ (y : List α), y ∈ S → y ∈ l

case h.mpr
α : Type u_1
β : Type ?u.98971
γ : Type ?u.98974
l✝ m : Language α
a b x✝ : List α
l : Language α
x : List α
⊢ (∃ i S, x = join S ∧ length S = i ∧ ∀ (y : List α), y ∈ S → y ∈ l) → ∃ L, x = join L ∧ ∀ (y : List α), y ∈ L → y ∈ l
case h
α : Type u_1
β : Type ?u.98971
γ : Type ?u.98974
l✝ m : Language α
a b x✝ : List α
l : Language α
x : List α
⊢ (∃ L, x = join L ∧ ∀ (y : List α), y ∈ L → y ∈ l) ↔ ∃ i S, x = join S ∧ length S = i ∧ ∀ (y : List α), y ∈ S → y ∈ l
constructor
case h.mp.intro.intro
α : Type u_1
β : Type ?u.98971
γ : Type ?u.98974
l✝ m : Language α
a b x : List α
l : Language α
S : List (List α)
hS : ∀ (y : List α), y ∈ S → y ∈ l
⊢ ∃ i S_1, join S = join S_1 ∧ length S_1 = i ∧ ∀ (y : List α), y ∈ S_1 → y ∈ l
case h.mp
α : Type u_1
β : Type ?u.98971
γ : Type ?u.98974
l✝ m : Language α
a b x✝ : List α
l : Language α
x : List α
⊢ (∃ L, x = join L ∧ ∀ (y : List α), y ∈ L → y ∈ l) → ∃ i S, x = join S ∧ length S = i ∧ ∀ (y : List α), y ∈ S → y ∈ l
rintro ⟨S, rfl, hS⟩
no goals
case h.mp.intro.intro
α : Type u_1
β : Type ?u.98971
γ : Type ?u.98974
l✝ m : Language α
a b x : List α
l : Language α
S : List (List α)
hS : ∀ (y : List α), y ∈ S → y ∈ l
⊢ ∃ i S_1, join S = join S_1 ∧ length S_1 = i ∧ ∀ (y : List α), y ∈ S_1 → y ∈ l
exact ⟨_, S, rfl, rfl, hS⟩
case h.mpr.intro.intro.intro.intro
α : Type u_1
β : Type ?u.98971
γ : Type ?u.98974
l✝ m : Language α
a b x : List α
l : Language α
S : List (List α)
hS : ∀ (y : List α), y ∈ S → y ∈ l
⊢ ∃ L, join S = join L ∧ ∀ (y : List α), y ∈ L → y ∈ l
case h.mpr
α : Type u_1
β : Type ?u.98971
γ : Type ?u.98974
l✝ m : Language α
a b x✝ : List α
l : Language α
x : List α
⊢ (∃ i S, x = join S ∧ length S = i ∧ ∀ (y : List α), y ∈ S → y ∈ l) → ∃ L, x = join L ∧ ∀ (y : List α), y ∈ L → y ∈ l
rintro ⟨_, S, rfl, rfl, hS⟩
no goals
case h.mpr.intro.intro.intro.intro
α : Type u_1
β : Type ?u.98971
γ : Type ?u.98974
l✝ m : Language α
a b x : List α
l : Language α
S : List (List α)
hS : ∀ (y : List α), y ∈ S → y ∈ l
⊢ ∃ L, join S = join L ∧ ∀ (y : List α), y ∈ L → y ∈ l
exact ⟨S, rfl, hS⟩