α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a b : α
P : RegularExpression α
x : List α
A : ∀ (m n : ℕ), n < m + n + 1
⊢ rmatch (star P) x = true ↔ ∃ S, x = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a b : α
P : RegularExpression α
x : List α
⊢ rmatch (star P) x = true ↔ ∃ S, x = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true
have A : ∀ m n : ℕ, n < m + n + 1 := by
  intro m n
  convert add_lt_add_of_le_of_lt (add_le_add (zero_le m) (le_refl n)) zero_lt_one
  simp
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a b : α
P : RegularExpression α
x : List α
A : ∀ (m n : ℕ), n < m + n + 1
IH :
  ∀ (t : List α),
    length t < length x →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
⊢ rmatch (star P) x = true ↔ ∃ S, x = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a b : α
P : RegularExpression α
x : List α
A : ∀ (m n : ℕ), n < m + n + 1
⊢ rmatch (star P) x = true ↔ ∃ S, x = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true
have IH := fun t (_h : List.length t < List.length x) => star_rmatch_iff P t
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a b : α
P : RegularExpression α
x : List α
A : ∀ (m n : ℕ), n < m + n + 1
IH :
  ∀ (t : List α),
    length t < length x →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
⊢ rmatch (star P) x = true ↔ ∃ S, x = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a b : α
P : RegularExpression α
x : List α
A : ∀ (m n : ℕ), n < m + n + 1
IH :
  ∀ (t : List α),
    length t < length x →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
⊢ rmatch (star P) x = true ↔ ∃ S, x = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true
clear star_rmatch_iff
case mp
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a b : α
P : RegularExpression α
x : List α
A : ∀ (m n : ℕ), n < m + n + 1
IH :
  ∀ (t : List α),
    length t < length x →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
⊢ rmatch (star P) x = true → ∃ S, x = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true

case mpr
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a b : α
P : RegularExpression α
x : List α
A : ∀ (m n : ℕ), n < m + n + 1
IH :
  ∀ (t : List α),
    length t < length x →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
⊢ (∃ S, x = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true) → rmatch (star P) x = true
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a b : α
P : RegularExpression α
x : List α
A : ∀ (m n : ℕ), n < m + n + 1
IH :
  ∀ (t : List α),
    length t < length x →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
⊢ rmatch (star P) x = true ↔ ∃ S, x = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true
constructor
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a b : α
P : RegularExpression α
x : List α
m n : ℕ
⊢ n < m + n + 1
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a b : α
P : RegularExpression α
x : List α
⊢ ∀ (m n : ℕ), n < m + n + 1
intro m n
case h.e'_3
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a b : α
P : RegularExpression α
x : List α
m n : ℕ
⊢ n = 0 + n + 0
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a b : α
P : RegularExpression α
x : List α
m n : ℕ
⊢ n < m + n + 1
convert add_lt_add_of_le_of_lt (add_le_add (zero_le m) (le_refl n)) zero_lt_one
no goals
case h.e'_3
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a b : α
P : RegularExpression α
x : List α
m n : ℕ
⊢ n = 0 + n + 0
simp
case mp.nil
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a b : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
IH :
  ∀ (t : List α),
    length t < length [] →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
⊢ rmatch (star P) [] = true → ∃ S, [] = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true

case mp.cons
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a✝ b : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
⊢ rmatch (star P) (a :: x) = true → ∃ S, a :: x = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true
case mp
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a b : α
P : RegularExpression α
x : List α
A : ∀ (m n : ℕ), n < m + n + 1
IH :
  ∀ (t : List α),
    length t < length x →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
⊢ rmatch (star P) x = true → ∃ S, x = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true
cases' x with a x
case mp.nil
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a b : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
IH :
  ∀ (t : List α),
    length t < length [] →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
_h : rmatch (star P) [] = true
⊢ ∃ S, [] = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true
case mp.nil
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a b : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
IH :
  ∀ (t : List α),
    length t < length [] →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
⊢ rmatch (star P) [] = true → ∃ S, [] = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true
intro _h
case mp.nil
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a b : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
IH :
  ∀ (t : List α),
    length t < length [] →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
_h : rmatch (star P) [] = true
⊢ [] = join [] ∧ ∀ (t : List α), t ∈ [] → t ≠ [] ∧ rmatch P t = true
case mp.nil
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a b : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
IH :
  ∀ (t : List α),
    length t < length [] →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
_h : rmatch (star P) [] = true
⊢ ∃ S, [] = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true
use []
case mp.nil
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a b : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
IH :
  ∀ (t : List α),
    length t < length [] →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
_h : rmatch (star P) [] = true
⊢ [] = [] ∧ ∀ (t : List α), t ∈ [] → ¬t = [] ∧ rmatch P t = true
case mp.nil
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a b : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
IH :
  ∀ (t : List α),
    length t < length [] →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
_h : rmatch (star P) [] = true
⊢ [] = join [] ∧ ∀ (t : List α), t ∈ [] → t ≠ [] ∧ rmatch P t = true
dsimp
no goals
case mp.nil
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a b : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
IH :
  ∀ (t : List α),
    length t < length [] →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
_h : rmatch (star P) [] = true
⊢ [] = [] ∧ ∀ (t : List α), t ∈ [] → ¬t = [] ∧ rmatch P t = true
tauto
case mp.cons
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a✝ b : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
⊢ (∃ t u, x = t ++ u ∧ rmatch (deriv P a) t = true ∧ rmatch (star P) u = true) →
    ∃ S, a :: x = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true
case mp.cons
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a✝ b : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
⊢ rmatch (star P) (a :: x) = true → ∃ S, a :: x = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true
rw [rmatch, deriv, mul_rmatch_iff]
case mp.cons.intro.intro.intro.intro
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a✝ b : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
t u : List α
hs : x = t ++ u
ht : rmatch (deriv P a) t = true
hu : rmatch (star P) u = true
⊢ ∃ S, a :: x = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true
case mp.cons
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a✝ b : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
⊢ (∃ t u, x = t ++ u ∧ rmatch (deriv P a) t = true ∧ rmatch (star P) u = true) →
    ∃ S, a :: x = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true
rintro ⟨t, u, hs, ht, hu⟩
case mp.cons.intro.intro.intro.intro
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a✝ b : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
t u : List α
hs : x = t ++ u
ht : rmatch (deriv P a) t = true
hu : rmatch (star P) u = true
hwf : length u < length (a :: x)
⊢ ∃ S, a :: x = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true
case mp.cons.intro.intro.intro.intro
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a✝ b : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
t u : List α
hs : x = t ++ u
ht : rmatch (deriv P a) t = true
hu : rmatch (star P) u = true
⊢ ∃ S, a :: x = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true
have hwf : u.length < (List.cons a x).length := by
  rw [hs, List.length_cons, List.length_append]
  apply A
case mp.cons.intro.intro.intro.intro
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a✝ b : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
t u : List α
hs : x = t ++ u
ht : rmatch (deriv P a) t = true
hu : ∃ S, u = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true
hwf : length u < length (a :: x)
⊢ ∃ S, a :: x = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true
case mp.cons.intro.intro.intro.intro
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a✝ b : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
t u : List α
hs : x = t ++ u
ht : rmatch (deriv P a) t = true
hu : rmatch (star P) u = true
hwf : length u < length (a :: x)
⊢ ∃ S, a :: x = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true
rw [IH _ hwf] at hu
case mp.cons.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a✝ b : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
t u : List α
hs : x = t ++ u
ht : rmatch (deriv P a) t = true
hwf : length u < length (a :: x)
S' : List (List α)
hsum : u = join S'
helem : ∀ (t : List α), t ∈ S' → t ≠ [] ∧ rmatch P t = true
⊢ ∃ S, a :: x = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true
case mp.cons.intro.intro.intro.intro
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a✝ b : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
t u : List α
hs : x = t ++ u
ht : rmatch (deriv P a) t = true
hu : ∃ S, u = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true
hwf : length u < length (a :: x)
⊢ ∃ S, a :: x = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true
rcases hu with ⟨S', hsum, helem⟩
case mp.cons.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a✝ b : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
t u : List α
hs : x = t ++ u
ht : rmatch (deriv P a) t = true
hwf : length u < length (a :: x)
S' : List (List α)
hsum : u = join S'
helem : ∀ (t : List α), t ∈ S' → t ≠ [] ∧ rmatch P t = true
⊢ a :: x = join ((a :: t) :: S') ∧ ∀ (t_1 : List α), t_1 ∈ (a :: t) :: S' → t_1 ≠ [] ∧ rmatch P t_1 = true
case mp.cons.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a✝ b : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
t u : List α
hs : x = t ++ u
ht : rmatch (deriv P a) t = true
hwf : length u < length (a :: x)
S' : List (List α)
hsum : u = join S'
helem : ∀ (t : List α), t ∈ S' → t ≠ [] ∧ rmatch P t = true
⊢ ∃ S, a :: x = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true
use (a :: t) :: S'
case mp.cons.intro.intro.intro.intro.intro.intro.left
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a✝ b : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
t u : List α
hs : x = t ++ u
ht : rmatch (deriv P a) t = true
hwf : length u < length (a :: x)
S' : List (List α)
hsum : u = join S'
helem : ∀ (t : List α), t ∈ S' → t ≠ [] ∧ rmatch P t = true
⊢ a :: x = join ((a :: t) :: S')

case mp.cons.intro.intro.intro.intro.intro.intro.right
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a✝ b : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
t u : List α
hs : x = t ++ u
ht : rmatch (deriv P a) t = true
hwf : length u < length (a :: x)
S' : List (List α)
hsum : u = join S'
helem : ∀ (t : List α), t ∈ S' → t ≠ [] ∧ rmatch P t = true
⊢ ∀ (t_1 : List α), t_1 ∈ (a :: t) :: S' → t_1 ≠ [] ∧ rmatch P t_1 = true
case mp.cons.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a✝ b : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
t u : List α
hs : x = t ++ u
ht : rmatch (deriv P a) t = true
hwf : length u < length (a :: x)
S' : List (List α)
hsum : u = join S'
helem : ∀ (t : List α), t ∈ S' → t ≠ [] ∧ rmatch P t = true
⊢ a :: x = join ((a :: t) :: S') ∧ ∀ (t_1 : List α), t_1 ∈ (a :: t) :: S' → t_1 ≠ [] ∧ rmatch P t_1 = true
constructor
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a✝ b : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
t u : List α
hs : x = t ++ u
ht : rmatch (deriv P a) t = true
hu : rmatch (star P) u = true
⊢ length u < Nat.succ (length t + length u)
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a✝ b : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
t u : List α
hs : x = t ++ u
ht : rmatch (deriv P a) t = true
hu : rmatch (star P) u = true
⊢ length u < length (a :: x)
rw [hs, List.length_cons, List.length_append]
no goals
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a✝ b : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
t u : List α
hs : x = t ++ u
ht : rmatch (deriv P a) t = true
hu : rmatch (star P) u = true
⊢ length u < Nat.succ (length t + length u)
apply A
no goals
case mp.cons.intro.intro.intro.intro.intro.intro.left
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a✝ b : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
t u : List α
hs : x = t ++ u
ht : rmatch (deriv P a) t = true
hwf : length u < length (a :: x)
S' : List (List α)
hsum : u = join S'
helem : ∀ (t : List α), t ∈ S' → t ≠ [] ∧ rmatch P t = true
⊢ a :: x = join ((a :: t) :: S')
simp [hs, hsum]
case mp.cons.intro.intro.intro.intro.intro.intro.right
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a✝ b : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
t u : List α
hs : x = t ++ u
ht : rmatch (deriv P a) t = true
hwf : length u < length (a :: x)
S' : List (List α)
hsum : u = join S'
helem : ∀ (t : List α), t ∈ S' → t ≠ [] ∧ rmatch P t = true
t' : List α
ht' : t' ∈ (a :: t) :: S'
⊢ t' ≠ [] ∧ rmatch P t' = true
case mp.cons.intro.intro.intro.intro.intro.intro.right
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a✝ b : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
t u : List α
hs : x = t ++ u
ht : rmatch (deriv P a) t = true
hwf : length u < length (a :: x)
S' : List (List α)
hsum : u = join S'
helem : ∀ (t : List α), t ∈ S' → t ≠ [] ∧ rmatch P t = true
⊢ ∀ (t_1 : List α), t_1 ∈ (a :: t) :: S' → t_1 ≠ [] ∧ rmatch P t_1 = true
intro t' ht'
case mp.cons.intro.intro.intro.intro.intro.intro.right.head
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a✝ b : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
t u : List α
hs : x = t ++ u
ht : rmatch (deriv P a) t = true
hwf : length u < length (a :: x)
S' : List (List α)
hsum : u = join S'
helem : ∀ (t : List α), t ∈ S' → t ≠ [] ∧ rmatch P t = true
⊢ a :: t ≠ [] ∧ rmatch P (a :: t) = true

case mp.cons.intro.intro.intro.intro.intro.intro.right.tail
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a✝¹ b : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
t u : List α
hs : x = t ++ u
ht : rmatch (deriv P a) t = true
hwf : length u < length (a :: x)
S' : List (List α)
hsum : u = join S'
helem : ∀ (t : List α), t ∈ S' → t ≠ [] ∧ rmatch P t = true
t' : List α
a✝ : Mem t' S'
⊢ t' ≠ [] ∧ rmatch P t' = true
case mp.cons.intro.intro.intro.intro.intro.intro.right
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a✝ b : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
t u : List α
hs : x = t ++ u
ht : rmatch (deriv P a) t = true
hwf : length u < length (a :: x)
S' : List (List α)
hsum : u = join S'
helem : ∀ (t : List α), t ∈ S' → t ≠ [] ∧ rmatch P t = true
t' : List α
ht' : t' ∈ (a :: t) :: S'
⊢ t' ≠ [] ∧ rmatch P t' = true
cases ht'
case mp.cons.intro.intro.intro.intro.intro.intro.right.tail
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a✝¹ b : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
t u : List α
hs : x = t ++ u
ht : rmatch (deriv P a) t = true
hwf : length u < length (a :: x)
S' : List (List α)
hsum : u = join S'
helem : ∀ (t : List α), t ∈ S' → t ≠ [] ∧ rmatch P t = true
t' : List α
a✝ : Mem t' S'
⊢ t' ≠ [] ∧ rmatch P t' = true
case mp.cons.intro.intro.intro.intro.intro.intro.right.head
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a✝ b : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
t u : List α
hs : x = t ++ u
ht : rmatch (deriv P a) t = true
hwf : length u < length (a :: x)
S' : List (List α)
hsum : u = join S'
helem : ∀ (t : List α), t ∈ S' → t ≠ [] ∧ rmatch P t = true
⊢ a :: t ≠ [] ∧ rmatch P (a :: t) = true

case mp.cons.intro.intro.intro.intro.intro.intro.right.tail
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a✝¹ b : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
t u : List α
hs : x = t ++ u
ht : rmatch (deriv P a) t = true
hwf : length u < length (a :: x)
S' : List (List α)
hsum : u = join S'
helem : ∀ (t : List α), t ∈ S' → t ≠ [] ∧ rmatch P t = true
t' : List α
a✝ : Mem t' S'
⊢ t' ≠ [] ∧ rmatch P t' = true
case head ht' =>
  simp only [ne_eq, not_false_iff, true_and, rmatch]
  exact ht
no goals
case mp.cons.intro.intro.intro.intro.intro.intro.right.tail
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a✝¹ b : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
t u : List α
hs : x = t ++ u
ht : rmatch (deriv P a) t = true
hwf : length u < length (a :: x)
S' : List (List α)
hsum : u = join S'
helem : ∀ (t : List α), t ∈ S' → t ≠ [] ∧ rmatch P t = true
t' : List α
a✝ : Mem t' S'
⊢ t' ≠ [] ∧ rmatch P t' = true
case tail ht' => exact helem t' ht'
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
ht' b : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
t u : List α
hs : x = t ++ u
ht : rmatch (deriv P a) t = true
hwf : length u < length (a :: x)
S' : List (List α)
hsum : u = join S'
helem : ∀ (t : List α), t ∈ S' → t ≠ [] ∧ rmatch P t = true
⊢ rmatch (deriv P a) t = true
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
ht' b : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
t u : List α
hs : x = t ++ u
ht : rmatch (deriv P a) t = true
hwf : length u < length (a :: x)
S' : List (List α)
hsum : u = join S'
helem : ∀ (t : List α), t ∈ S' → t ≠ [] ∧ rmatch P t = true
⊢ a :: t ≠ [] ∧ rmatch P (a :: t) = true
simp only [ne_eq, not_false_iff, true_and, rmatch]
no goals
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
ht' b : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
t u : List α
hs : x = t ++ u
ht : rmatch (deriv P a) t = true
hwf : length u < length (a :: x)
S' : List (List α)
hsum : u = join S'
helem : ∀ (t : List α), t ∈ S' → t ≠ [] ∧ rmatch P t = true
⊢ rmatch (deriv P a) t = true
exact ht
no goals
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a✝ b : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
t u : List α
hs : x = t ++ u
ht : rmatch (deriv P a) t = true
hwf : length u < length (a :: x)
S' : List (List α)
hsum : u = join S'
helem : ∀ (t : List α), t ∈ S' → t ≠ [] ∧ rmatch P t = true
t' : List α
ht' : Mem t' S'
⊢ t' ≠ [] ∧ rmatch P t' = true
exact helem t' ht'
case mpr.intro.intro
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a b : α
P : RegularExpression α
x : List α
A : ∀ (m n : ℕ), n < m + n + 1
IH :
  ∀ (t : List α),
    length t < length x →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
S : List (List α)
hsum : x = join S
helem : ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true
⊢ rmatch (star P) x = true
case mpr
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a b : α
P : RegularExpression α
x : List α
A : ∀ (m n : ℕ), n < m + n + 1
IH :
  ∀ (t : List α),
    length t < length x →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
⊢ (∃ S, x = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true) → rmatch (star P) x = true
rintro ⟨S, hsum, helem⟩
case mpr.intro.intro
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a b : α
P : RegularExpression α
x : List α
A : ∀ (m n : ℕ), n < m + n + 1
IH :
  ∀ (t : List α),
    length t < length x →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
S : List (List α)
hsum : x = join S
helem : ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true
⊢ rmatch (star P) x = true
case mpr.intro.intro
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a b : α
P : RegularExpression α
x : List α
A : ∀ (m n : ℕ), n < m + n + 1
IH :
  ∀ (t : List α),
    length t < length x →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
S : List (List α)
hsum : x = join S
helem : ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true
⊢ rmatch (star P) x = true
dsimp
case mpr.intro.intro.nil
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a b : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
S : List (List α)
helem : ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true
IH :
  ∀ (t : List α),
    length t < length [] →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
hsum : [] = join S
⊢ rmatch (star P) [] = true

case mpr.intro.intro.cons
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a✝ b : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
S : List (List α)
helem : ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
hsum : a :: x = join S
⊢ rmatch (star P) (a :: x) = true
case mpr.intro.intro
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a b : α
P : RegularExpression α
x : List α
A : ∀ (m n : ℕ), n < m + n + 1
IH :
  ∀ (t : List α),
    length t < length x →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
S : List (List α)
hsum : x = join S
helem : ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true
⊢ rmatch (star P) x = true
cases' x with a x
no goals
case mpr.intro.intro.nil
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a b : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
S : List (List α)
helem : ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true
IH :
  ∀ (t : List α),
    length t < length [] →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
hsum : [] = join S
⊢ rmatch (star P) [] = true
rfl
case mpr.intro.intro.cons
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a✝ b : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
S : List (List α)
helem : ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
hsum : a :: x = join S
⊢ ∃ t u, x = t ++ u ∧ rmatch (deriv P a) t = true ∧ rmatch (star P) u = true
case mpr.intro.intro.cons
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a✝ b : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
S : List (List α)
helem : ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
hsum : a :: x = join S
⊢ rmatch (star P) (a :: x) = true
rw [rmatch, deriv, mul_rmatch_iff]
case mpr.intro.intro.cons.nil
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a✝ b : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
helem : ∀ (t : List α), t ∈ [] → t ≠ [] ∧ rmatch P t = true
hsum : a :: x = join []
⊢ ∃ t u, x = t ++ u ∧ rmatch (deriv P a) t = true ∧ rmatch (star P) u = true

case mpr.intro.intro.cons.cons
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a✝ b : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
t' : List α
U : List (List α)
helem : ∀ (t : List α), t ∈ t' :: U → t ≠ [] ∧ rmatch P t = true
hsum : a :: x = join (t' :: U)
⊢ ∃ t u, x = t ++ u ∧ rmatch (deriv P a) t = true ∧ rmatch (star P) u = true
case mpr.intro.intro.cons
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a✝ b : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
S : List (List α)
helem : ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
hsum : a :: x = join S
⊢ ∃ t u, x = t ++ u ∧ rmatch (deriv P a) t = true ∧ rmatch (star P) u = true
cases' S with t' U
no goals
case mpr.intro.intro.cons.nil
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a✝ b : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
helem : ∀ (t : List α), t ∈ [] → t ≠ [] ∧ rmatch P t = true
hsum : a :: x = join []
⊢ ∃ t u, x = t ++ u ∧ rmatch (deriv P a) t = true ∧ rmatch (star P) u = true
exact ⟨[], [], by tauto⟩
no goals
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a✝ b : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
helem : ∀ (t : List α), t ∈ [] → t ≠ [] ∧ rmatch P t = true
hsum : a :: x = join []
⊢ x = [] ++ [] ∧ rmatch (deriv P a) [] = true ∧ rmatch (star P) [] = true
tauto
case mpr.intro.intro.cons.cons.nil
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a✝ b : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
U : List (List α)
helem : ∀ (t : List α), t ∈ [] :: U → t ≠ [] ∧ rmatch P t = true
hsum : a :: x = join ([] :: U)
⊢ ∃ t u, x = t ++ u ∧ rmatch (deriv P a) t = true ∧ rmatch (star P) u = true

case mpr.intro.intro.cons.cons.cons
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a✝ b✝ : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
U : List (List α)
b : α
t : List α
helem : ∀ (t_1 : List α), t_1 ∈ (b :: t) :: U → t_1 ≠ [] ∧ rmatch P t_1 = true
hsum : a :: x = join ((b :: t) :: U)
⊢ ∃ t u, x = t ++ u ∧ rmatch (deriv P a) t = true ∧ rmatch (star P) u = true
case mpr.intro.intro.cons.cons
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a✝ b : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
t' : List α
U : List (List α)
helem : ∀ (t : List α), t ∈ t' :: U → t ≠ [] ∧ rmatch P t = true
hsum : a :: x = join (t' :: U)
⊢ ∃ t u, x = t ++ u ∧ rmatch (deriv P a) t = true ∧ rmatch (star P) u = true
cases' t' with b t
case mpr.intro.intro.cons.cons.cons
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a✝ b✝ : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
U : List (List α)
b : α
t : List α
helem : ∀ (t_1 : List α), t_1 ∈ (b :: t) :: U → t_1 ≠ [] ∧ rmatch P t_1 = true
hsum : a = b ∧ x = t ++ join U
⊢ ∃ t u, x = t ++ u ∧ rmatch (deriv P a) t = true ∧ rmatch (star P) u = true
case mpr.intro.intro.cons.cons.cons
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a✝ b✝ : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
U : List (List α)
b : α
t : List α
helem : ∀ (t_1 : List α), t_1 ∈ (b :: t) :: U → t_1 ≠ [] ∧ rmatch P t_1 = true
hsum : a :: x = join ((b :: t) :: U)
⊢ ∃ t u, x = t ++ u ∧ rmatch (deriv P a) t = true ∧ rmatch (star P) u = true
simp only [List.join, List.cons_append, List.cons_eq_cons] at hsum
case mpr.intro.intro.cons.cons.cons.refine'_1
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a✝ b✝ : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
U : List (List α)
b : α
t : List α
helem : ∀ (t_1 : List α), t_1 ∈ (b :: t) :: U → t_1 ≠ [] ∧ rmatch P t_1 = true
hsum : a = b ∧ x = t ++ join U
⊢ rmatch (deriv P a) t = true

case mpr.intro.intro.cons.cons.cons.refine'_2
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a✝ b✝ : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
U : List (List α)
b : α
t : List α
helem : ∀ (t_1 : List α), t_1 ∈ (b :: t) :: U → t_1 ≠ [] ∧ rmatch P t_1 = true
hsum : a = b ∧ x = t ++ join U
⊢ rmatch (star P) (join U) = true
case mpr.intro.intro.cons.cons.cons
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a✝ b✝ : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
U : List (List α)
b : α
t : List α
helem : ∀ (t_1 : List α), t_1 ∈ (b :: t) :: U → t_1 ≠ [] ∧ rmatch P t_1 = true
hsum : a = b ∧ x = t ++ join U
⊢ ∃ t u, x = t ++ u ∧ rmatch (deriv P a) t = true ∧ rmatch (star P) u = true
refine' ⟨t, U.join, hsum.2, _, _⟩
case mpr.intro.intro.cons.cons.nil
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a✝ b : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
U : List (List α)
hsum : a :: x = join ([] :: U)
helem : ([] ≠ [] ∧ rmatch P [] = true) ∧ ∀ (a : List α), a ∈ U → a ≠ [] ∧ rmatch P a = true
⊢ ∃ t u, x = t ++ u ∧ rmatch (deriv P a) t = true ∧ rmatch (star P) u = true
case mpr.intro.intro.cons.cons.nil
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a✝ b : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
U : List (List α)
helem : ∀ (t : List α), t ∈ [] :: U → t ≠ [] ∧ rmatch P t = true
hsum : a :: x = join ([] :: U)
⊢ ∃ t u, x = t ++ u ∧ rmatch (deriv P a) t = true ∧ rmatch (star P) u = true
simp only [forall_eq_or_imp, List.mem_cons] at helem
no goals
case mpr.intro.intro.cons.cons.nil
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a✝ b : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
U : List (List α)
hsum : a :: x = join ([] :: U)
helem : ([] ≠ [] ∧ rmatch P [] = true) ∧ ∀ (a : List α), a ∈ U → a ≠ [] ∧ rmatch P a = true
⊢ ∃ t u, x = t ++ u ∧ rmatch (deriv P a) t = true ∧ rmatch (star P) u = true
simp only [eq_self_iff_true, not_true, Ne.def, false_and_iff] at helem
case mpr.intro.intro.cons.cons.cons.refine'_1
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a✝ b✝ : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
U : List (List α)
b : α
t : List α
hsum : a = b ∧ x = t ++ join U
helem : b :: t ≠ [] ∧ rmatch P (b :: t) = true
⊢ rmatch (deriv P a) t = true
case mpr.intro.intro.cons.cons.cons.refine'_1
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a✝ b✝ : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
U : List (List α)
b : α
t : List α
helem : ∀ (t_1 : List α), t_1 ∈ (b :: t) :: U → t_1 ≠ [] ∧ rmatch P t_1 = true
hsum : a = b ∧ x = t ++ join U
⊢ rmatch (deriv P a) t = true
specialize helem (b :: t) (by simp)
case mpr.intro.intro.cons.cons.cons.refine'_1
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a✝ b✝ : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
U : List (List α)
b : α
t : List α
hsum : a = b ∧ x = t ++ join U
helem : b :: t ≠ [] ∧ rmatch (deriv P b) t = true
⊢ rmatch (deriv P a) t = true
case mpr.intro.intro.cons.cons.cons.refine'_1
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a✝ b✝ : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
U : List (List α)
b : α
t : List α
hsum : a = b ∧ x = t ++ join U
helem : b :: t ≠ [] ∧ rmatch P (b :: t) = true
⊢ rmatch (deriv P a) t = true
rw [rmatch] at helem
case h.e'_2.h.e'_3.h.e'_4
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a✝ b✝ : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
U : List (List α)
b : α
t : List α
hsum : a = b ∧ x = t ++ join U
helem : b :: t ≠ [] ∧ rmatch (deriv P b) t = true
⊢ a = b
case mpr.intro.intro.cons.cons.cons.refine'_1
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a✝ b✝ : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
U : List (List α)
b : α
t : List α
hsum : a = b ∧ x = t ++ join U
helem : b :: t ≠ [] ∧ rmatch (deriv P b) t = true
⊢ rmatch (deriv P a) t = true
convert helem.2
no goals
case h.e'_2.h.e'_3.h.e'_4
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a✝ b✝ : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
U : List (List α)
b : α
t : List α
hsum : a = b ∧ x = t ++ join U
helem : b :: t ≠ [] ∧ rmatch (deriv P b) t = true
⊢ a = b
exact hsum.1
no goals
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a✝ b✝ : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
U : List (List α)
b : α
t : List α
helem : ∀ (t_1 : List α), t_1 ∈ (b :: t) :: U → t_1 ≠ [] ∧ rmatch P t_1 = true
hsum : a = b ∧ x = t ++ join U
⊢ b :: t ∈ (b :: t) :: U
simp
case mpr.intro.intro.cons.cons.cons.refine'_2
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a✝ b✝ : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
U : List (List α)
b : α
t : List α
helem : ∀ (t_1 : List α), t_1 ∈ (b :: t) :: U → t_1 ≠ [] ∧ rmatch P t_1 = true
hsum : a = b ∧ x = t ++ join U
hwf : length (join U) < length (a :: x)
⊢ rmatch (star P) (join U) = true
case mpr.intro.intro.cons.cons.cons.refine'_2
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a✝ b✝ : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
U : List (List α)
b : α
t : List α
helem : ∀ (t_1 : List α), t_1 ∈ (b :: t) :: U → t_1 ≠ [] ∧ rmatch P t_1 = true
hsum : a = b ∧ x = t ++ join U
⊢ rmatch (star P) (join U) = true
have hwf : U.join.length < (List.cons a x).length := by
  rw [hsum.1, hsum.2]
  simp only [List.length_append, List.length_join, List.length]
  apply A
case mpr.intro.intro.cons.cons.cons.refine'_2
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a✝ b✝ : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
U : List (List α)
b : α
t : List α
helem : ∀ (t_1 : List α), t_1 ∈ (b :: t) :: U → t_1 ≠ [] ∧ rmatch P t_1 = true
hsum : a = b ∧ x = t ++ join U
hwf : length (join U) < length (a :: x)
⊢ ∃ S, join U = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true
case mpr.intro.intro.cons.cons.cons.refine'_2
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a✝ b✝ : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
U : List (List α)
b : α
t : List α
helem : ∀ (t_1 : List α), t_1 ∈ (b :: t) :: U → t_1 ≠ [] ∧ rmatch P t_1 = true
hsum : a = b ∧ x = t ++ join U
hwf : length (join U) < length (a :: x)
⊢ rmatch (star P) (join U) = true
rw [IH _ hwf]
case mpr.intro.intro.cons.cons.cons.refine'_2
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a✝ b✝ : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
U : List (List α)
b : α
t✝ : List α
helem : ∀ (t : List α), t ∈ (b :: t✝) :: U → t ≠ [] ∧ rmatch P t = true
hsum : a = b ∧ x = t✝ ++ join U
hwf : length (join U) < length (a :: x)
t : List α
h : t ∈ U
⊢ t ∈ (b :: t✝) :: U
case mpr.intro.intro.cons.cons.cons.refine'_2
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a✝ b✝ : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
U : List (List α)
b : α
t : List α
helem : ∀ (t_1 : List α), t_1 ∈ (b :: t) :: U → t_1 ≠ [] ∧ rmatch P t_1 = true
hsum : a = b ∧ x = t ++ join U
hwf : length (join U) < length (a :: x)
⊢ ∃ S, join U = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true
refine' ⟨U, rfl, fun t h => helem t _⟩
case mpr.intro.intro.cons.cons.cons.refine'_2.a
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a✝ b✝ : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
U : List (List α)
b : α
t✝ : List α
helem : ∀ (t : List α), t ∈ (b :: t✝) :: U → t ≠ [] ∧ rmatch P t = true
hsum : a = b ∧ x = t✝ ++ join U
hwf : length (join U) < length (a :: x)
t : List α
h : t ∈ U
⊢ Mem t U
case mpr.intro.intro.cons.cons.cons.refine'_2
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a✝ b✝ : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
U : List (List α)
b : α
t✝ : List α
helem : ∀ (t : List α), t ∈ (b :: t✝) :: U → t ≠ [] ∧ rmatch P t = true
hsum : a = b ∧ x = t✝ ++ join U
hwf : length (join U) < length (a :: x)
t : List α
h : t ∈ U
⊢ t ∈ (b :: t✝) :: U
right
no goals
case mpr.intro.intro.cons.cons.cons.refine'_2.a
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a✝ b✝ : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
U : List (List α)
b : α
t✝ : List α
helem : ∀ (t : List α), t ∈ (b :: t✝) :: U → t ≠ [] ∧ rmatch P t = true
hsum : a = b ∧ x = t✝ ++ join U
hwf : length (join U) < length (a :: x)
t : List α
h : t ∈ U
⊢ Mem t U
assumption
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a✝ b✝ : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
U : List (List α)
b : α
t : List α
helem : ∀ (t_1 : List α), t_1 ∈ (b :: t) :: U → t_1 ≠ [] ∧ rmatch P t_1 = true
hsum : a = b ∧ x = t ++ join U
⊢ length (join U) < length (b :: (t ++ join U))
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a✝ b✝ : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
U : List (List α)
b : α
t : List α
helem : ∀ (t_1 : List α), t_1 ∈ (b :: t) :: U → t_1 ≠ [] ∧ rmatch P t_1 = true
hsum : a = b ∧ x = t ++ join U
⊢ length (join U) < length (a :: x)
rw [hsum.1, hsum.2]
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a✝ b✝ : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
U : List (List α)
b : α
t : List α
helem : ∀ (t_1 : List α), t_1 ∈ (b :: t) :: U → t_1 ≠ [] ∧ rmatch P t_1 = true
hsum : a = b ∧ x = t ++ join U
⊢ sum (map length U) < length t + sum (map length U) + 1
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a✝ b✝ : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
U : List (List α)
b : α
t : List α
helem : ∀ (t_1 : List α), t_1 ∈ (b :: t) :: U → t_1 ≠ [] ∧ rmatch P t_1 = true
hsum : a = b ∧ x = t ++ join U
⊢ length (join U) < length (b :: (t ++ join U))
simp only [List.length_append, List.length_join, List.length]
no goals
α : Type u_1
β : Type ?u.53385
γ : Type ?u.53388
dec : DecidableEq α
a✝ b✝ : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
U : List (List α)
b : α
t : List α
helem : ∀ (t_1 : List α), t_1 ∈ (b :: t) :: U → t_1 ≠ [] ∧ rmatch P t_1 = true
hsum : a = b ∧ x = t ++ join U
⊢ sum (map length U) < length t + sum (map length U) + 1
apply A