case h
α : Type u_1
β : Type ?u.86402
γ : Type ?u.86405
l✝ m : Language α
a b x✝ : List α
l : Language α
x : List α
⊢ x ∈ l∗ ↔ x ∈ {x | ∃ S, x = join S ∧ ∀ (y : List α), y ∈ S → y ∈ l ∧ y ≠ []}
α : Type u_1
β : Type ?u.86402
γ : Type ?u.86405
l✝ m : Language α
a b x : List α
l : Language α
⊢ l∗ = {x | ∃ S, x = join S ∧ ∀ (y : List α), y ∈ S → y ∈ l ∧ y ≠ []}
ext x
case h.mp
α : Type u_1
β : Type ?u.86402
γ : Type ?u.86405
l✝ m : Language α
a b x✝ : List α
l : Language α
x : List α
⊢ x ∈ l∗ → x ∈ {x | ∃ S, x = join S ∧ ∀ (y : List α), y ∈ S → y ∈ l ∧ y ≠ []}

case h.mpr
α : Type u_1
β : Type ?u.86402
γ : Type ?u.86405
l✝ m : Language α
a b x✝ : List α
l : Language α
x : List α
⊢ x ∈ {x | ∃ S, x = join S ∧ ∀ (y : List α), y ∈ S → y ∈ l ∧ y ≠ []} → x ∈ l∗
case h
α : Type u_1
β : Type ?u.86402
γ : Type ?u.86405
l✝ m : Language α
a b x✝ : List α
l : Language α
x : List α
⊢ x ∈ l∗ ↔ x ∈ {x | ∃ S, x = join S ∧ ∀ (y : List α), y ∈ S → y ∈ l ∧ y ≠ []}
constructor
case h.mp.intro.intro
α : Type u_1
β : Type ?u.86402
γ : Type ?u.86405
l✝ m : Language α
a b x : List α
l : Language α
S : List (List α)
h : ∀ (y : List α), y ∈ S → y ∈ l
⊢ join S ∈ {x | ∃ S, x = join S ∧ ∀ (y : List α), y ∈ S → y ∈ l ∧ y ≠ []}
case h.mp
α : Type u_1
β : Type ?u.86402
γ : Type ?u.86405
l✝ m : Language α
a b x✝ : List α
l : Language α
x : List α
⊢ x ∈ l∗ → x ∈ {x | ∃ S, x = join S ∧ ∀ (y : List α), y ∈ S → y ∈ l ∧ y ≠ []}
rintro ⟨S, rfl, h⟩
case h.mp.intro.intro
α : Type u_1
β : Type ?u.86402
γ : Type ?u.86405
l✝ m : Language α
a b x : List α
l : Language α
S : List (List α)
h : ∀ (y : List α), y ∈ S → y ∈ l
y : List α
hy : y ∈ filter (fun l => decide ¬isEmpty l = true) S
⊢ y ∈ l ∧ y ≠ []
case h.mp.intro.intro
α : Type u_1
β : Type ?u.86402
γ : Type ?u.86405
l✝ m : Language α
a b x : List α
l : Language α
S : List (List α)
h : ∀ (y : List α), y ∈ S → y ∈ l
⊢ join S ∈ {x | ∃ S, x = join S ∧ ∀ (y : List α), y ∈ S → y ∈ l ∧ y ≠ []}
refine' ⟨S.filter fun l ↦ ¬List.isEmpty l, by simp, fun y hy ↦ _⟩
case h.mp.intro.intro
α : Type u_1
β : Type ?u.86402
γ : Type ?u.86405
l✝ m : Language α
a b x : List α
l : Language α
S : List (List α)
h : ∀ (y : List α), y ∈ S → y ∈ l
y : List α
hy : y ∈ S ∧ isEmpty y = false
⊢ y ∈ l ∧ y ≠ []
case h.mp.intro.intro
α : Type u_1
β : Type ?u.86402
γ : Type ?u.86405
l✝ m : Language α
a b x : List α
l : Language α
S : List (List α)
h : ∀ (y : List α), y ∈ S → y ∈ l
y : List α
hy : y ∈ filter (fun l => decide ¬isEmpty l = true) S
⊢ y ∈ l ∧ y ≠ []
simp [mem_filter, List.isEmpty_iff_eq_nil] at hy
case h.mp.intro.intro
α : Type u_1
β : Type ?u.86402
γ : Type ?u.86405
l✝ m : Language α
a b x : List α
l : Language α
S : List (List α)
h : ∀ (y : List α), y ∈ S → y ∈ l
y : List α
hy : y ∈ S ∧ isEmpty y = false
hyl : y ∈ S
hyr : isEmpty y = false
⊢ y ∈ l ∧ y ≠ []
case h.mp.intro.intro
α : Type u_1
β : Type ?u.86402
γ : Type ?u.86405
l✝ m : Language α
a b x : List α
l : Language α
S : List (List α)
h : ∀ (y : List α), y ∈ S → y ∈ l
y : List α
hy : y ∈ S ∧ isEmpty y = false
⊢ y ∈ l ∧ y ≠ []
let ⟨hyl, hyr⟩ := hy
case h.mp.intro.intro
α : Type u_1
β : Type ?u.86402
γ : Type ?u.86405
l✝ m : Language α
a b x : List α
l : Language α
S : List (List α)
h : ∀ (y : List α), y ∈ S → y ∈ l
y : List α
hy : y ∈ S ∧ isEmpty y = false
hyl : y ∈ S
hyr : isEmpty y = false
⊢ y ≠ []
case h.mp.intro.intro
α : Type u_1
β : Type ?u.86402
γ : Type ?u.86405
l✝ m : Language α
a b x : List α
l : Language α
S : List (List α)
h : ∀ (y : List α), y ∈ S → y ∈ l
y : List α
hy : y ∈ S ∧ isEmpty y = false
hyl : y ∈ S
hyr : isEmpty y = false
⊢ y ∈ l ∧ y ≠ []
apply And.intro (h y hyl)
case h.mp.intro.intro.nil
α : Type u_1
β : Type ?u.86402
γ : Type ?u.86405
l✝ m : Language α
a b x : List α
l : Language α
S : List (List α)
h : ∀ (y : List α), y ∈ S → y ∈ l
hy : [] ∈ S ∧ isEmpty [] = false
hyl : [] ∈ S
hyr : isEmpty [] = false
⊢ False
case h.mp.intro.intro
α : Type u_1
β : Type ?u.86402
γ : Type ?u.86405
l✝ m : Language α
a b x : List α
l : Language α
S : List (List α)
h : ∀ (y : List α), y ∈ S → y ∈ l
y : List α
hy : y ∈ S ∧ isEmpty y = false
hyl : y ∈ S
hyr : isEmpty y = false
⊢ y ≠ []
cases y <;> simp only [ne_eq, not_true, not_false_iff]
no goals
case h.mp.intro.intro.nil
α : Type u_1
β : Type ?u.86402
γ : Type ?u.86405
l✝ m : Language α
a b x : List α
l : Language α
S : List (List α)
h : ∀ (y : List α), y ∈ S → y ∈ l
hy : [] ∈ S ∧ isEmpty [] = false
hyl : [] ∈ S
hyr : isEmpty [] = false
⊢ False
contradiction
no goals
α : Type u_1
β : Type ?u.86402
γ : Type ?u.86405
l✝ m : Language α
a b x : List α
l : Language α
S : List (List α)
h : ∀ (y : List α), y ∈ S → y ∈ l
⊢ join S = join (filter (fun l => decide ¬isEmpty l = true) S)
simp
case h.mpr.intro.intro
α : Type u_1
β : Type ?u.86402
γ : Type ?u.86405
l✝ m : Language α
a b x✝ : List α
l : Language α
x : List α
S : List (List α)
hx : x = join S
h : ∀ (y : List α), y ∈ S → y ∈ l ∧ y ≠ []
⊢ x ∈ l∗
case h.mpr
α : Type u_1
β : Type ?u.86402
γ : Type ?u.86405
l✝ m : Language α
a b x✝ : List α
l : Language α
x : List α
⊢ x ∈ {x | ∃ S, x = join S ∧ ∀ (y : List α), y ∈ S → y ∈ l ∧ y ≠ []} → x ∈ l∗
rintro ⟨S, hx, h⟩
no goals
case h.mpr.intro.intro
α : Type u_1
β : Type ?u.86402
γ : Type ?u.86405
l✝ m : Language α
a b x✝ : List α
l : Language α
x : List α
S : List (List α)
hx : x = join S
h : ∀ (y : List α), y ∈ S → y ∈ l ∧ y ≠ []
⊢ x ∈ l∗
exact ⟨S, hx, fun y hy ↦ (h y hy).1⟩