-- Mathlib/Computability/RegularExpressions.lean
theorem star_rmatch_iff (P : RegularExpression α) :
    ∀ x : List α, (star P).rmatch x ↔ ∃ S : List (List α), x
          = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t :=
  fun x => by
    have IH := fun t (_h : List.length t < List.length x) => star_rmatch_iff P t
    clear star_rmatch_iff
    constructor
    · rcases x with - | ⟨a, x⟩
      · intro _h
        use []; dsimp; tauto
      · rw [rmatch, deriv, mul_rmatch_iff]
        rintro ⟨t, u, hs, ht, hu⟩
        have hwf : u.length < (List.cons a x).length

Proof state:
case mpr.intro.intro.cons
α : Type u_1
inst✝ : DecidableEq α
P : RegularExpression α
S : List (List α)
helem : ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
a : α
x : List α
IH :
  ∀ (t : List α),
    t.length < (a :: x).length → (P.star.rmatch t = true ↔ ∃ S, t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true)
hsum : a :: x = S.flatten
⊢ P.star.rmatch (a :: x) = true

Tactic:
rw [rmatch, deriv, mul_rmatch_iff]

Result:
case mpr.intro.intro.cons
α : Type u_1
inst✝ : DecidableEq α
P : RegularExpression α
S : List (List α)
helem : ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
a : α
x : List α
IH :
  ∀ (t : List α),
    t.length < (a :: x).length → (P.star.rmatch t = true ↔ ∃ S, t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true)
hsum : a :: x = S.flatten
⊢ ∃ t u, x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ P.star.rmatch u = true

Proof state:
case mpr.intro.intro.cons.cons.cons.refine_2
α : Type u_1
inst✝ : DecidableEq α
P : RegularExpression α
a : α
x : List α
IH :
  ∀ (t : List α),
    t.length < (a :: x).length → (P.star.rmatch t = true ↔ ∃ S, t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true)
U : List (List α)
b : α
t : List α
helem : ∀ t_1 ∈ (b :: t) :: U, t_1 ≠ [] ∧ P.rmatch t_1 = true
hsum : a = b ∧ x = t ++ U.flatten
hwf : U.flatten.length < (a :: x).length
⊢ ∃ S, U.flatten = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true

Tactic:
refine ⟨U, rfl, fun t h => helem t ?_⟩

Result:
case mpr.intro.intro.cons.cons.cons.refine_2
α : Type u_1
inst✝ : DecidableEq α
P : RegularExpression α
a : α
x : List α
IH :
  ∀ (t : List α),
    t.length < (a :: x).length → (P.star.rmatch t = true ↔ ∃ S, t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true)
U : List (List α)
b : α
t✝ : List α
helem : ∀ t ∈ (b :: t✝) :: U, t ≠ [] ∧ P.rmatch t = true
hsum : a = b ∧ x = t✝ ++ U.flatten
hwf : U.flatten.length < (a :: x).length
t : List α
h : t ∈ U
⊢ t ∈ (b :: t✝) :: U

Proof state:
case mpr.intro.intro.cons.cons.cons.refine_1
α : Type u_1
inst✝ : DecidableEq α
P : RegularExpression α
a : α
x : List α
IH :
  ∀ (t : List α),
    t.length < (a :: x).length → (P.star.rmatch t = true ↔ ∃ S, t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true)
U : List (List α)
b : α
t : List α
hsum : a = b ∧ x = t ++ U.flatten
helem : b :: t ≠ [] ∧ P.rmatch (b :: t) = true
⊢ (P.deriv a).rmatch t = true

Tactic:
rw [rmatch] at helem

Result:
case mpr.intro.intro.cons.cons.cons.refine_1
α : Type u_1
inst✝ : DecidableEq α
P : RegularExpression α
a : α
x : List α
IH :
  ∀ (t : List α),
    t.length < (a :: x).length → (P.star.rmatch t = true ↔ ∃ S, t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true)
U : List (List α)
b : α
t : List α
hsum : a = b ∧ x = t ++ U.flatten
helem : b :: t ≠ [] ∧ (P.deriv b).rmatch t = true
⊢ (P.deriv a).rmatch t = true

Proof state:
case mpr.intro.intro.cons.cons.cons.refine_1
α : Type u_1
inst✝ : DecidableEq α
P : RegularExpression α
a : α
x : List α
IH :
  ∀ (t : List α),
    t.length < (a :: x).length → (P.star.rmatch t = true ↔ ∃ S, t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true)
U : List (List α)
b : α
t : List α
hsum : a = b ∧ x = t ++ U.flatten
helem : b :: t ≠ [] ∧ (P.deriv b).rmatch t = true
⊢ (P.deriv a).rmatch t = true

Tactic:
convert helem.2

Result:
case h.e'_2.h.e'_3.h.e'_4
α : Type u_1
inst✝ : DecidableEq α
P : RegularExpression α
a : α
x : List α
IH :
  ∀ (t : List α),
    t.length < (a :: x).length → (P.star.rmatch t = true ↔ ∃ S, t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true)
U : List (List α)
b : α
t : List α
hsum : a = b ∧ x = t ++ U.flatten
helem : b :: t ≠ [] ∧ (P.deriv b).rmatch t = true
⊢ a = b

Proof state:
case h
α : Type u_1
inst✝ : DecidableEq α
P : RegularExpression α
IH :
  ∀ (t : List α),
    t.length < [].length → (P.star.rmatch t = true ↔ ∃ S, t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true)
_h : P.star.rmatch [] = true
⊢ [] = [] ∧ ∀ t ∈ [], ¬t = [] ∧ P.rmatch t = true

Tactic:
tauto

Result:
no goals

Proof state:
case mpr.intro.intro.cons.cons.cons.refine_2.a
α : Type u_1
inst✝ : DecidableEq α
P : RegularExpression α
a : α
x : List α
IH :
  ∀ (t : List α),
    t.length < (a :: x).length → (P.star.rmatch t = true ↔ ∃ S, t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true)
U : List (List α)
b : α
t✝ : List α
helem : ∀ t ∈ (b :: t✝) :: U, t ≠ [] ∧ P.rmatch t = true
hsum : a = b ∧ x = t✝ ++ U.flatten
hwf : U.flatten.length < (a :: x).length
t : List α
h : t ∈ U
⊢ Mem t U

Tactic:
assumption

Result:
no goals

Proof state:
case h
α : Type u_1
inst✝ : DecidableEq α
P : RegularExpression α
IH :
  ∀ (t : List α),
    t.length < [].length → (P.star.rmatch t = true ↔ ∃ S, t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true)
_h : P.star.rmatch [] = true
⊢ [] = [].flatten ∧ ∀ t ∈ [], t ≠ [] ∧ P.rmatch t = true

Tactic:
dsimp

Result:
case h
α : Type u_1
inst✝ : DecidableEq α
P : RegularExpression α
IH :
  ∀ (t : List α),
    t.length < [].length → (P.star.rmatch t = true ↔ ∃ S, t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true)
_h : P.star.rmatch [] = true
⊢ [] = [] ∧ ∀ t ∈ [], ¬t = [] ∧ P.rmatch t = true

Proof state:
case mpr.intro.intro.cons.cons.nil
α : Type u_1
inst✝ : DecidableEq α
P : RegularExpression α
a : α
x : List α
IH :
  ∀ (t : List α),
    t.length < (a :: x).length → (P.star.rmatch t = true ↔ ∃ S, t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true)
U : List (List α)
hsum : a :: x = ([] :: U).flatten
helem : ([] ≠ [] ∧ P.rmatch [] = true) ∧ ∀ a ∈ U, a ≠ [] ∧ P.rmatch a = true
⊢ ∃ t u, x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ P.star.rmatch u = true

Tactic:
simp only [eq_self_iff_true, not_true, Ne, false_and] at helem

Result:
no goals

Proof state:
case h.right
α : Type u_1
inst✝ : DecidableEq α
P : RegularExpression α
a : α
x : List α
IH :
  ∀ (t : List α),
    t.length < (a :: x).length → (P.star.rmatch t = true ↔ ∃ S, t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true)
t u : List α
hs : x = t ++ u
ht : (P.deriv a).rmatch t = true
hwf : u.length < (a :: x).length
S' : List (List α)
hsum : u = S'.flatten
helem : ∀ t ∈ S', t ≠ [] ∧ P.rmatch t = true
t' : List α
ht' : t' ∈ (a :: t) :: S'
⊢ t' ≠ [] ∧ P.rmatch t' = true

Tactic:
cases ht' with
| head ht' =>
  simp only [ne_eq, not_false_iff, true_and, rmatch, reduceCtorEq]
  exact ht
| tail _ ht' => exact helem t' ht'

Result:
no goals

Proof state:
case mp.cons
α : Type u_1
inst✝ : DecidableEq α
P : RegularExpression α
a : α
x : List α
IH :
  ∀ (t : List α),
    t.length < (a :: x).length → (P.star.rmatch t = true ↔ ∃ S, t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true)
⊢ P.star.rmatch (a :: x) = true → ∃ S, a :: x = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true

Tactic:
rw [rmatch, deriv, mul_rmatch_iff]

Result:
case mp.cons
α : Type u_1
inst✝ : DecidableEq α
P : RegularExpression α
a : α
x : List α
IH :
  ∀ (t : List α),
    t.length < (a :: x).length → (P.star.rmatch t = true ↔ ∃ S, t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true)
⊢ (∃ t u, x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ P.star.rmatch u = true) →
    ∃ S, a :: x = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true

Proof state:
α : Type u_1
inst✝ : DecidableEq α
P : RegularExpression α
a : α
x : List α
IH :
  ∀ (t : List α),
    t.length < (a :: x).length → (P.star.rmatch t = true ↔ ∃ S, t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true)
helem : ∀ t ∈ [], t ≠ [] ∧ P.rmatch t = true
hsum : a :: x = [].flatten
⊢ x = [] ++ [] ∧ (P.deriv a).rmatch [] = true ∧ P.star.rmatch [] = true

Tactic:
tauto

Result:
no goals