[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
l m : Language α
a b x✝ x : List α
⊢ x ∈ 1 ↔ x = []
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m : Language α
a b x : List α
l : Language α
x✝ : List α
h : x✝ ∈ []
⊢ x✝ ∈ l
[PROOFSTEP]
contradiction
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m : Language α
a b x : List α
l : Language α
⊢ 1 * l = l
[PROOFSTEP]
simp [mul_def, one_def]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m : Language α
a b x : List α
l : Language α
⊢ l * 1 = l
[PROOFSTEP]
simp [mul_def, one_def]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
l m : Language α
a b x : List α
n : ℕ
⊢ NatCast.natCast (n + 1) = NatCast.natCast n + 1
[PROOFSTEP]
cases n
[GOAL]
case zero
α : Type u_1
β : Type u_2
γ : Type u_3
l m : Language α
a b x : List α
⊢ NatCast.natCast (Nat.zero + 1) = NatCast.natCast Nat.zero + 1
[PROOFSTEP]
simp [Nat.cast, add_def, zero_def]
[GOAL]
case succ
α : Type u_1
β : Type u_2
γ : Type u_3
l m : Language α
a b x : List α
n✝ : ℕ
⊢ NatCast.natCast (Nat.succ n✝ + 1) = NatCast.natCast (Nat.succ n✝) + 1
[PROOFSTEP]
simp [Nat.cast, add_def, zero_def]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m : Language α
a b x : List α
l : Language α
⊢ ↑(map id) l = l
[PROOFSTEP]
simp [map]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m : Language α
a b x : List α
g : β → γ
f : α → β
l : Language α
⊢ ↑(map g) (↑(map f) l) = ↑(map (g ∘ f)) l
[PROOFSTEP]
simp [map, image_image]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m : Language α
a b x : List α
l : Language α
⊢ l∗ = {x | ∃ S, x = join S ∧ ∀ (y : List α), y ∈ S → y ∈ l ∧ y ≠ []}
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
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 ≠ []}
[PROOFSTEP]
constructor
[GOAL]
case h.mp
α : Type u_1
β : Type u_2
γ : Type u_3
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 ≠ []}
[PROOFSTEP]
rintro ⟨S, rfl, h⟩
[GOAL]
case h.mp.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
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 ≠ []}
[PROOFSTEP]
refine'
  ⟨S.filter fun l ↦ ¬List.isEmpty l, by simp, fun y hy ↦ _⟩
    -- Porting note: The previous code was:
        -- rw [mem_filter, empty_iff_eq_nil] at hy
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
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)
[PROOFSTEP]
simp
[GOAL]
case h.mp.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
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 ≠ []
[PROOFSTEP]
rw [mem_filter, decide_not, Bool.decide_coe, Bool.not_eq_true', ← Bool.bool_iff_false, isEmpty_iff_eq_nil] at hy 
[GOAL]
case h.mp.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m : Language α
a b x : List α
l : Language α
S : List (List α)
h : ∀ (y : List α), y ∈ S → y ∈ l
y : List α
hy : y ∈ S ∧ ¬y = []
⊢ y ∈ l ∧ y ≠ []
[PROOFSTEP]
exact ⟨h y hy.1, hy.2⟩
[GOAL]
case h.mpr
α : Type u_1
β : Type u_2
γ : Type u_3
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∗
[PROOFSTEP]
rintro ⟨S, hx, h⟩
[GOAL]
case h.mpr.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
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∗
[PROOFSTEP]
exact ⟨S, hx, fun y hy ↦ (h y hy).1⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
l m : Language α
a b x : List α
l₁ l₂ m₁ m₂ : Language α
⊢ l₁ ≤ m₁ → l₂ ≤ m₂ → l₁ * l₂ ≤ m₁ * m₂
[PROOFSTEP]
intro h₁ h₂ x hx
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
l m : Language α
a b x✝ : List α
l₁ l₂ m₁ m₂ : Language α
h₁ : l₁ ≤ m₁
h₂ : l₂ ≤ m₂
x : List α
hx : x ∈ l₁ * l₂
⊢ x ∈ m₁ * m₂
[PROOFSTEP]
simp only [mul_def, exists_and_left, mem_image2, image_prod] at hx ⊢
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
l m : Language α
a b x✝ : List α
l₁ l₂ m₁ m₂ : Language α
h₁ : l₁ ≤ m₁
h₂ : l₂ ≤ m₂
x : List α
hx : ∃ a, a ∈ l₁ ∧ ∃ x_1, x_1 ∈ l₂ ∧ a ++ x_1 = x
⊢ ∃ a, a ∈ m₁ ∧ ∃ x_1, x_1 ∈ m₂ ∧ a ++ x_1 = x
[PROOFSTEP]
tauto
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m : Language α
a b x✝ : List α
l : Language α
x : List α
n : ℕ
⊢ x ∈ l ^ n ↔ ∃ S, x = join S ∧ length S = n ∧ ∀ (y : List α), y ∈ S → y ∈ l
[PROOFSTEP]
induction' n with n ihn generalizing x
[GOAL]
case zero
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m : Language α
a b x✝¹ : List α
l : Language α
x✝ x : List α
⊢ x ∈ l ^ Nat.zero ↔ ∃ S, x = join S ∧ length S = Nat.zero ∧ ∀ (y : List α), y ∈ S → y ∈ l
[PROOFSTEP]
simp only [mem_one, pow_zero, length_eq_zero]
[GOAL]
case zero
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m : Language α
a b x✝¹ : List α
l : Language α
x✝ x : List α
⊢ x = [] ↔ ∃ S, x = join S ∧ S = [] ∧ ∀ (y : List α), y ∈ S → y ∈ l
[PROOFSTEP]
constructor
[GOAL]
case zero.mp
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m : Language α
a b x✝¹ : List α
l : Language α
x✝ x : List α
⊢ x = [] → ∃ S, x = join S ∧ S = [] ∧ ∀ (y : List α), y ∈ S → y ∈ l
[PROOFSTEP]
rintro rfl
[GOAL]
case zero.mp
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m : Language α
a b x✝ : List α
l : Language α
x : List α
⊢ ∃ S, [] = join S ∧ S = [] ∧ ∀ (y : List α), y ∈ S → y ∈ l
[PROOFSTEP]
exact ⟨[], rfl, rfl, fun _ h ↦ by contradiction⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m : Language α
a b x✝¹ : List α
l : Language α
x x✝ : List α
h : x✝ ∈ []
⊢ x✝ ∈ l
[PROOFSTEP]
contradiction
[GOAL]
case zero.mpr
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m : Language α
a b x✝¹ : List α
l : Language α
x✝ x : List α
⊢ (∃ S, x = join S ∧ S = [] ∧ ∀ (y : List α), y ∈ S → y ∈ l) → x = []
[PROOFSTEP]
rintro ⟨_, rfl, rfl, _⟩
[GOAL]
case zero.mpr.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m : Language α
a b x✝ : List α
l : Language α
x : List α
right✝ : ∀ (y : List α), y ∈ [] → y ∈ l
⊢ join [] = []
[PROOFSTEP]
rfl
[GOAL]
case succ
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m : Language α
a b x✝¹ : List α
l : Language α
x✝ : List α
n : ℕ
ihn : ∀ {x : List α}, x ∈ l ^ n ↔ ∃ S, x = join S ∧ length S = n ∧ ∀ (y : List α), y ∈ S → y ∈ l
x : List α
⊢ x ∈ l ^ Nat.succ n ↔ ∃ S, x = join S ∧ length S = Nat.succ n ∧ ∀ (y : List α), y ∈ S → y ∈ l
[PROOFSTEP]
simp only [pow_succ, mem_mul, ihn]
[GOAL]
case succ
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m : Language α
a b x✝¹ : List α
l : Language α
x✝ : List α
n : ℕ
ihn : ∀ {x : List α}, x ∈ l ^ n ↔ ∃ S, x = join S ∧ length S = n ∧ ∀ (y : List α), y ∈ S → y ∈ l
x : List α
⊢ (∃ a b, a ∈ l ∧ (∃ S, b = join S ∧ length S = n ∧ ∀ (y : List α), y ∈ S → y ∈ l) ∧ a ++ b = x) ↔
    ∃ S, x = join S ∧ length S = Nat.succ n ∧ ∀ (y : List α), y ∈ S → y ∈ l
[PROOFSTEP]
constructor
[GOAL]
case succ.mp
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m : Language α
a b x✝¹ : List α
l : Language α
x✝ : List α
n : ℕ
ihn : ∀ {x : List α}, x ∈ l ^ n ↔ ∃ S, x = join S ∧ length S = n ∧ ∀ (y : List α), y ∈ S → y ∈ l
x : List α
⊢ (∃ a b, a ∈ l ∧ (∃ S, b = join S ∧ length S = n ∧ ∀ (y : List α), y ∈ S → y ∈ l) ∧ a ++ b = x) →
    ∃ S, x = join S ∧ length S = Nat.succ n ∧ ∀ (y : List α), y ∈ S → y ∈ l
[PROOFSTEP]
rintro ⟨a, b, ha, ⟨S, rfl, rfl, hS⟩, rfl⟩
[GOAL]
case succ.mp.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m : Language α
a✝ b x✝ : List α
l : Language α
x a : List α
ha : a ∈ l
S : List (List α)
hS : ∀ (y : List α), y ∈ S → y ∈ l
ihn : ∀ {x : List α}, x ∈ l ^ length S ↔ ∃ S_1, x = join S_1 ∧ length S_1 = length S ∧ ∀ (y : List α), y ∈ S_1 → y ∈ l
⊢ ∃ S_1, a ++ join S = join S_1 ∧ length S_1 = Nat.succ (length S) ∧ ∀ (y : List α), y ∈ S_1 → y ∈ l
[PROOFSTEP]
exact ⟨a :: S, rfl, rfl, forall_mem_cons.2 ⟨ha, hS⟩⟩
[GOAL]
case succ.mpr
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m : Language α
a b x✝¹ : List α
l : Language α
x✝ : List α
n : ℕ
ihn : ∀ {x : List α}, x ∈ l ^ n ↔ ∃ S, x = join S ∧ length S = n ∧ ∀ (y : List α), y ∈ S → y ∈ l
x : List α
⊢ (∃ S, x = join S ∧ length S = Nat.succ n ∧ ∀ (y : List α), y ∈ S → y ∈ l) →
    ∃ a b, a ∈ l ∧ (∃ S, b = join S ∧ length S = n ∧ ∀ (y : List α), y ∈ S → y ∈ l) ∧ a ++ b = x
[PROOFSTEP]
rintro ⟨_ | ⟨a, S⟩, rfl, hn, hS⟩
[GOAL]
case succ.mpr.intro.nil.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m : Language α
a b x✝ : List α
l : Language α
x : List α
n : ℕ
ihn : ∀ {x : List α}, x ∈ l ^ n ↔ ∃ S, x = join S ∧ length S = n ∧ ∀ (y : List α), y ∈ S → y ∈ l
hn : length [] = Nat.succ n
hS : ∀ (y : List α), y ∈ [] → y ∈ l
⊢ ∃ a b, a ∈ l ∧ (∃ S, b = join S ∧ length S = n ∧ ∀ (y : List α), y ∈ S → y ∈ l) ∧ a ++ b = join []
[PROOFSTEP]
cases hn
[GOAL]
case succ.mpr.intro.cons.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m : Language α
a✝ b x✝ : List α
l : Language α
x : List α
n : ℕ
ihn : ∀ {x : List α}, x ∈ l ^ n ↔ ∃ S, x = join S ∧ length S = n ∧ ∀ (y : List α), y ∈ S → y ∈ l
a : List α
S : List (List α)
hn : length (a :: S) = Nat.succ n
hS : ∀ (y : List α), y ∈ a :: S → y ∈ l
⊢ ∃ a_1 b, a_1 ∈ l ∧ (∃ S, b = join S ∧ length S = n ∧ ∀ (y : List α), y ∈ S → y ∈ l) ∧ a_1 ++ b = join (a :: S)
[PROOFSTEP]
cases hn
[GOAL]
case succ.mpr.intro.cons.intro.intro.refl
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m : Language α
a✝ b x✝ : List α
l : Language α
x a : List α
S : List (List α)
hS : ∀ (y : List α), y ∈ a :: S → y ∈ l
ihn :
  ∀ {x : List α},
    x ∈ l ^ Nat.add (length S) 0 ↔
      ∃ S_1, x = join S_1 ∧ length S_1 = Nat.add (length S) 0 ∧ ∀ (y : List α), y ∈ S_1 → y ∈ l
⊢ ∃ a_1 b,
    a_1 ∈ l ∧
      (∃ S_1, b = join S_1 ∧ length S_1 = Nat.add (length S) 0 ∧ ∀ (y : List α), y ∈ S_1 → y ∈ l) ∧
        a_1 ++ b = join (a :: S)
[PROOFSTEP]
rw [forall_mem_cons] at hS 
[GOAL]
case succ.mpr.intro.cons.intro.intro.refl
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m : Language α
a✝ b x✝ : List α
l : Language α
x a : List α
S : List (List α)
hS : a ∈ l ∧ ∀ (x : List α), x ∈ S → x ∈ l
ihn :
  ∀ {x : List α},
    x ∈ l ^ Nat.add (length S) 0 ↔
      ∃ S_1, x = join S_1 ∧ length S_1 = Nat.add (length S) 0 ∧ ∀ (y : List α), y ∈ S_1 → y ∈ l
⊢ ∃ a_1 b,
    a_1 ∈ l ∧
      (∃ S_1, b = join S_1 ∧ length S_1 = Nat.add (length S) 0 ∧ ∀ (y : List α), y ∈ S_1 → y ∈ l) ∧
        a_1 ++ b = join (a :: S)
[PROOFSTEP]
exact ⟨a, _, hS.1, ⟨S, rfl, rfl, hS.2⟩, rfl⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m : Language α
a b x : List α
l : Language α
⊢ l∗ = ⨆ (i : ℕ), l ^ i
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m : Language α
a b x✝ : List α
l : Language α
x : List α
⊢ x ∈ l∗ ↔ x ∈ ⨆ (i : ℕ), l ^ i
[PROOFSTEP]
simp only [mem_kstar, mem_iSup, mem_pow]
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
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
[PROOFSTEP]
constructor
[GOAL]
case h.mp
α : Type u_1
β : Type u_2
γ : Type u_3
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
[PROOFSTEP]
rintro ⟨S, rfl, hS⟩
[GOAL]
case h.mp.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
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
[PROOFSTEP]
exact ⟨_, S, rfl, rfl, hS⟩
[GOAL]
case h.mpr
α : Type u_1
β : Type u_2
γ : Type u_3
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
[PROOFSTEP]
rintro ⟨_, S, rfl, rfl, hS⟩
[GOAL]
case h.mpr.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
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
[PROOFSTEP]
exact ⟨S, rfl, hS⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m : Language α
a b x : List α
f : α → β
l : Language α
⊢ ↑(map f) l∗ = (↑(map f) l)∗
[PROOFSTEP]
rw [kstar_eq_iSup_pow, kstar_eq_iSup_pow]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m : Language α
a b x : List α
f : α → β
l : Language α
⊢ ↑(map f) (⨆ (i : ℕ), l ^ i) = ⨆ (i : ℕ), ↑(map f) l ^ i
[PROOFSTEP]
simp_rw [← map_pow]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m : Language α
a b x : List α
f : α → β
l : Language α
⊢ ↑(map f) (⨆ (i : ℕ), l ^ i) = ⨆ (i : ℕ), ↑(map f) (l ^ i)
[PROOFSTEP]
exact image_iUnion
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m : Language α
a b x : List α
l : Language α
⊢ l∗ * l = l * l∗
[PROOFSTEP]
simp only [kstar_eq_iSup_pow, mul_iSup, iSup_mul, ← pow_succ, ← pow_succ']
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m : Language α
a b x : List α
l : Language α
⊢ 1 + l * l∗ = l∗
[PROOFSTEP]
simp only [kstar_eq_iSup_pow, mul_iSup, ← pow_succ, ← pow_zero l]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m : Language α
a b x : List α
l : Language α
⊢ l ^ 0 + ⨆ (i : ℕ), l ^ (i + 1) = ⨆ (i : ℕ), l ^ i
[PROOFSTEP]
exact sup_iSup_nat_succ _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m : Language α
a b x : List α
l : Language α
⊢ 1 + l∗ * l = l∗
[PROOFSTEP]
rw [mul_self_kstar_comm, one_add_self_mul_kstar_eq_kstar]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m : Language α
a✝ b x : List α
src✝¹ : Semiring (Language α) := instSemiring
src✝ : CompleteAtomicBooleanAlgebra (Set (List α)) := Set.completeAtomicBooleanAlgebra
a : Language α
l : List α
hl : l ∈ 1
⊢ ∀ (y : List α), y ∈ [] → y ∈ a
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m✝ : Language α
a b x : List α
src✝¹ : Semiring (Language α) := instSemiring
src✝ : CompleteAtomicBooleanAlgebra (Set (List α)) := Set.completeAtomicBooleanAlgebra
l m : Language α
h : m * l ≤ m
⊢ m * l∗ ≤ m
[PROOFSTEP]
rw [kstar_eq_iSup_pow, mul_iSup]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m✝ : Language α
a b x : List α
src✝¹ : Semiring (Language α) := instSemiring
src✝ : CompleteAtomicBooleanAlgebra (Set (List α)) := Set.completeAtomicBooleanAlgebra
l m : Language α
h : m * l ≤ m
⊢ ⨆ (i : ℕ), m * l ^ i ≤ m
[PROOFSTEP]
refine' iSup_le (fun n ↦ _)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m✝ : Language α
a b x : List α
src✝¹ : Semiring (Language α) := instSemiring
src✝ : CompleteAtomicBooleanAlgebra (Set (List α)) := Set.completeAtomicBooleanAlgebra
l m : Language α
h : m * l ≤ m
n : ℕ
⊢ m * l ^ n ≤ m
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m✝ : Language α
a b x : List α
src✝¹ : Semiring (Language α) := instSemiring
src✝ : CompleteAtomicBooleanAlgebra (Set (List α)) := Set.completeAtomicBooleanAlgebra
l m : Language α
h : m * l ≤ m
⊢ m * l ^ Nat.zero ≤ m
[PROOFSTEP]
simp
[GOAL]
case succ
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m✝ : Language α
a b x : List α
src✝¹ : Semiring (Language α) := instSemiring
src✝ : CompleteAtomicBooleanAlgebra (Set (List α)) := Set.completeAtomicBooleanAlgebra
l m : Language α
h : m * l ≤ m
n : ℕ
ih : m * l ^ n ≤ m
⊢ m * l ^ Nat.succ n ≤ m
[PROOFSTEP]
rw [pow_succ, ← mul_assoc m l (l ^ n)]
[GOAL]
case succ
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m✝ : Language α
a b x : List α
src✝¹ : Semiring (Language α) := instSemiring
src✝ : CompleteAtomicBooleanAlgebra (Set (List α)) := Set.completeAtomicBooleanAlgebra
l m : Language α
h : m * l ≤ m
n : ℕ
ih : m * l ^ n ≤ m
⊢ m * l * l ^ n ≤ m
[PROOFSTEP]
exact le_trans (le_mul_congr h le_rfl) ih
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m✝ : Language α
a b x : List α
src✝¹ : Semiring (Language α) := instSemiring
src✝ : CompleteAtomicBooleanAlgebra (Set (List α)) := Set.completeAtomicBooleanAlgebra
l m : Language α
h : l * m ≤ m
⊢ l∗ * m ≤ m
[PROOFSTEP]
rw [kstar_eq_iSup_pow, iSup_mul]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m✝ : Language α
a b x : List α
src✝¹ : Semiring (Language α) := instSemiring
src✝ : CompleteAtomicBooleanAlgebra (Set (List α)) := Set.completeAtomicBooleanAlgebra
l m : Language α
h : l * m ≤ m
⊢ ⨆ (i : ℕ), l ^ i * m ≤ m
[PROOFSTEP]
refine' iSup_le (fun n ↦ _)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m✝ : Language α
a b x : List α
src✝¹ : Semiring (Language α) := instSemiring
src✝ : CompleteAtomicBooleanAlgebra (Set (List α)) := Set.completeAtomicBooleanAlgebra
l m : Language α
h : l * m ≤ m
n : ℕ
⊢ l ^ n * m ≤ m
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m✝ : Language α
a b x : List α
src✝¹ : Semiring (Language α) := instSemiring
src✝ : CompleteAtomicBooleanAlgebra (Set (List α)) := Set.completeAtomicBooleanAlgebra
l m : Language α
h : l * m ≤ m
⊢ l ^ Nat.zero * m ≤ m
[PROOFSTEP]
simp
[GOAL]
case succ
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m✝ : Language α
a b x : List α
src✝¹ : Semiring (Language α) := instSemiring
src✝ : CompleteAtomicBooleanAlgebra (Set (List α)) := Set.completeAtomicBooleanAlgebra
l m : Language α
h : l * m ≤ m
n : ℕ
ih : l ^ n * m ≤ m
⊢ l ^ Nat.succ n * m ≤ m
[PROOFSTEP]
rw [pow_succ', mul_assoc (l ^ n) l m]
[GOAL]
case succ
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m✝ : Language α
a b x : List α
src✝¹ : Semiring (Language α) := instSemiring
src✝ : CompleteAtomicBooleanAlgebra (Set (List α)) := Set.completeAtomicBooleanAlgebra
l m : Language α
h : l * m ≤ m
n : ℕ
ih : l ^ n * m ≤ m
⊢ l ^ n * (l * m) ≤ m
[PROOFSTEP]
exact le_trans (le_mul_congr le_rfl h) ih
