case zero
α : Type u_1
β : Type ?u.95661
γ : Type ?u.95664
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

case succ
α : Type u_1
β : Type ?u.95661
γ : Type ?u.95664
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
α : Type u_1
β : Type ?u.95661
γ : Type ?u.95664
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
induction' n with n ihn generalizing x
case zero
α : Type u_1
β : Type ?u.95661
γ : Type ?u.95664
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
case zero
α : Type u_1
β : Type ?u.95661
γ : Type ?u.95664
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
simp only [mem_one, pow_zero, length_eq_zero]
case zero.mp
α : Type u_1
β : Type ?u.95661
γ : Type ?u.95664
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

case zero.mpr
α : Type u_1
β : Type ?u.95661
γ : Type ?u.95664
l✝ m : Language α
a b x✝¹ : List α
l : Language α
x✝ x : List α
⊢ (∃ S, x = join S ∧ length S = Nat.zero ∧ ∀ (y : List α), y ∈ S → y ∈ l) → x ∈ l ^ Nat.zero
case zero
α : Type u_1
β : Type ?u.95661
γ : Type ?u.95664
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
constructor
case zero.mp
α : Type u_1
β : Type ?u.95661
γ : Type ?u.95664
l✝ m : Language α
a b x✝ : List α
l : Language α
x : List α
⊢ ∃ S, [] = join S ∧ length S = Nat.zero ∧ ∀ (y : List α), y ∈ S → y ∈ l
case zero.mp
α : Type u_1
β : Type ?u.95661
γ : Type ?u.95664
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
rintro rfl
no goals
case zero.mp
α : Type u_1
β : Type ?u.95661
γ : Type ?u.95664
l✝ m : Language α
a b x✝ : List α
l : Language α
x : List α
⊢ ∃ S, [] = join S ∧ length S = Nat.zero ∧ ∀ (y : List α), y ∈ S → y ∈ l
exact ⟨[], rfl, rfl, fun _ h ↦ by contradiction⟩
no goals
α : Type u_1
β : Type ?u.95661
γ : Type ?u.95664
l✝ m : Language α
a b x✝¹ : List α
l : Language α
x x✝ : List α
h : x✝ ∈ []
⊢ x✝ ∈ l
contradiction
case zero.mpr.intro.intro.intro
α : Type u_1
β : Type ?u.95661
γ : Type ?u.95664
l✝ m : Language α
a b x✝ : List α
l : Language α
x : List α
w✝ : List (List α)
h₀ : length w✝ = Nat.zero
right✝ : ∀ (y : List α), y ∈ w✝ → y ∈ l
⊢ join w✝ ∈ l ^ Nat.zero
case zero.mpr
α : Type u_1
β : Type ?u.95661
γ : Type ?u.95664
l✝ m : Language α
a b x✝¹ : List α
l : Language α
x✝ x : List α
⊢ (∃ S, x = join S ∧ length S = Nat.zero ∧ ∀ (y : List α), y ∈ S → y ∈ l) → x ∈ l ^ Nat.zero
rintro ⟨_, rfl, h₀, _⟩
case zero.mpr.intro.intro.intro
α : Type u_1
β : Type ?u.95661
γ : Type ?u.95664
l✝ m : Language α
a b x✝ : List α
l : Language α
x : List α
w✝ : List (List α)
h₀ : length w✝ = Nat.zero
right✝ : ∀ (y : List α), y ∈ w✝ → y ∈ l
⊢ ∀ (l : List α), l ∈ w✝ → l = []
case zero.mpr.intro.intro.intro
α : Type u_1
β : Type ?u.95661
γ : Type ?u.95664
l✝ m : Language α
a b x✝ : List α
l : Language α
x : List α
w✝ : List (List α)
h₀ : length w✝ = Nat.zero
right✝ : ∀ (y : List α), y ∈ w✝ → y ∈ l
⊢ join w✝ ∈ l ^ Nat.zero
simp
case zero.mpr.intro.intro.intro
α : Type u_1
β : Type ?u.95661
γ : Type ?u.95664
l✝¹ m : Language α
a b x✝ : List α
l : Language α
x : List α
w✝ : List (List α)
h₀ : length w✝ = Nat.zero
right✝ : ∀ (y : List α), y ∈ w✝ → y ∈ l
l✝ : List α
h₁ : l✝ ∈ w✝
⊢ l✝ = []
case zero.mpr.intro.intro.intro
α : Type u_1
β : Type ?u.95661
γ : Type ?u.95664
l✝ m : Language α
a b x✝ : List α
l : Language α
x : List α
w✝ : List (List α)
h₀ : length w✝ = Nat.zero
right✝ : ∀ (y : List α), y ∈ w✝ → y ∈ l
⊢ ∀ (l : List α), l ∈ w✝ → l = []
intros _ h₁
case zero.mpr.intro.intro.intro
α : Type u_1
β : Type ?u.95661
γ : Type ?u.95664
l✝¹ m : Language α
a b x✝ : List α
l : Language α
x : List α
w✝ : List (List α)
h₀ : w✝ = []
right✝ : ∀ (y : List α), y ∈ w✝ → y ∈ l
l✝ : List α
h₁ : l✝ ∈ w✝
⊢ l✝ = []
case zero.mpr.intro.intro.intro
α : Type u_1
β : Type ?u.95661
γ : Type ?u.95664
l✝¹ m : Language α
a b x✝ : List α
l : Language α
x : List α
w✝ : List (List α)
h₀ : length w✝ = Nat.zero
right✝ : ∀ (y : List α), y ∈ w✝ → y ∈ l
l✝ : List α
h₁ : l✝ ∈ w✝
⊢ l✝ = []
rw [length_eq_zero] at h₀
case zero.mpr.intro.intro.intro
α : Type u_1
β : Type ?u.95661
γ : Type ?u.95664
l✝¹ m : Language α
a b x✝ : List α
l : Language α
x : List α
w✝ : List (List α)
h₀ : w✝ = []
right✝ : ∀ (y : List α), y ∈ w✝ → y ∈ l
l✝ : List α
h₁ : l✝ ∈ []
⊢ l✝ = []
case zero.mpr.intro.intro.intro
α : Type u_1
β : Type ?u.95661
γ : Type ?u.95664
l✝¹ m : Language α
a b x✝ : List α
l : Language α
x : List α
w✝ : List (List α)
h₀ : w✝ = []
right✝ : ∀ (y : List α), y ∈ w✝ → y ∈ l
l✝ : List α
h₁ : l✝ ∈ w✝
⊢ l✝ = []
rw [h₀] at h₁
no goals
case zero.mpr.intro.intro.intro
α : Type u_1
β : Type ?u.95661
γ : Type ?u.95664
l✝¹ m : Language α
a b x✝ : List α
l : Language α
x : List α
w✝ : List (List α)
h₀ : w✝ = []
right✝ : ∀ (y : List α), y ∈ w✝ → y ∈ l
l✝ : List α
h₁ : l✝ ∈ []
⊢ l✝ = []
contradiction
case succ
α : Type u_1
β : Type ?u.95661
γ : Type ?u.95664
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
case succ
α : Type u_1
β : Type ?u.95661
γ : Type ?u.95664
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
simp only [pow_succ, mem_mul, ihn]
case succ.mp
α : Type u_1
β : Type ?u.95661
γ : Type ?u.95664
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

case succ.mpr
α : Type u_1
β : Type ?u.95661
γ : Type ?u.95664
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
case succ
α : Type u_1
β : Type ?u.95661
γ : Type ?u.95664
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
constructor
case succ.mp.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.95661
γ : Type ?u.95664
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
case succ.mp
α : Type u_1
β : Type ?u.95661
γ : Type ?u.95664
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
rintro ⟨a, b, ha, ⟨S, rfl, rfl, hS⟩, rfl⟩
no goals
case succ.mp.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.95661
γ : Type ?u.95664
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
exact ⟨a :: S, rfl, rfl, forall_mem_cons.2 ⟨ha, hS⟩⟩
case succ.mpr.intro.cons.intro.intro.refl
α : Type u_1
β : Type ?u.95661
γ : Type ?u.95664
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)
case succ.mpr
α : Type u_1
β : Type ?u.95661
γ : Type ?u.95664
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
rintro ⟨_ | ⟨a, S⟩, rfl, hn, hS⟩ <;> cases hn
case succ.mpr.intro.cons.intro.intro.refl
α : Type u_1
β : Type ?u.95661
γ : Type ?u.95664
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)
case succ.mpr.intro.cons.intro.intro.refl
α : Type u_1
β : Type ?u.95661
γ : Type ?u.95664
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)
rw [forall_mem_cons] at hS
no goals
case succ.mpr.intro.cons.intro.intro.refl
α : Type u_1
β : Type ?u.95661
γ : Type ?u.95664
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)
exact ⟨a, _, hS.1, ⟨S, rfl, rfl, hS.2⟩, rfl⟩