-- Mathlib/Computability/RegularExpressions.lean
theorem mul_rmatch_iff (P Q : RegularExpression α) (x : List α) :
    (P * Q).rmatch x ↔ ∃ t u : List α, x = t ++ u ∧ P.rmatch t ∧ Q.rmatch u

Proof state:
case h.e'_2.h.e'_3.h.e'_4
α : Type u_1
inst✝ : DecidableEq α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), (P * Q).rmatch x = true ↔ ∃ t u, x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
P Q : RegularExpression α
hepsilon : P.matchEpsilon = true
u : List α
hQ : Q.rmatch u = true
b : α
t : List α
h : a = b ∧ x = t ++ u
hP : (P.deriv b).rmatch t = true
⊢ a = b

Tactic:
exact h.1

Result:
no goals

Proof state:
case nil.mp
α : Type u_1
inst✝ : DecidableEq α
P Q : RegularExpression α
h : (P.matchEpsilon && Q.matchEpsilon) = true
⊢ P.matchEpsilon = true ∧ Q.matchEpsilon = true

Tactic:
rwa [Bool.and_eq_true_iff] at h

Result:
no goals

Proof state:
case nil.mpr
α : Type u_1
inst✝ : DecidableEq α
P Q : RegularExpression α
⊢ (∃ t u, [] = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true) → (P.matchEpsilon && Q.matchEpsilon) = true

Tactic:
rintro ⟨t, u, h₁, h₂⟩

Result:
case nil.mpr.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
P Q : RegularExpression α
t u : List α
h₁ : [] = t ++ u
h₂ : P.rmatch t = true ∧ Q.rmatch u = true
⊢ (P.matchEpsilon && Q.matchEpsilon) = true

Proof state:
case nil.mpr.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
P Q : RegularExpression α
h₁ : [] = [] ++ []
h₂ : P.rmatch [] = true ∧ Q.rmatch [] = true
⊢ (P.matchEpsilon && Q.matchEpsilon) = true

Tactic:
repeat rw [rmatch] at h₂

Result:
case nil.mpr.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
P Q : RegularExpression α
h₁ : [] = [] ++ []
h₂ : P.matchEpsilon = true ∧ Q.matchEpsilon = true
⊢ (P.matchEpsilon && Q.matchEpsilon) = true

Proof state:
case pos.mpr.intro.intro.intro.intro.nil
α : Type u_1
inst✝ : DecidableEq α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), (P * Q).rmatch x = true ↔ ∃ t u, x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
P Q : RegularExpression α
hepsilon : P.matchEpsilon = true
u : List α
hQ : Q.rmatch u = true
h : a :: x = [] ++ u
hP : P.rmatch [] = true
⊢ (∃ t u, x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ Q.rmatch u = true) ∨ (Q.deriv a).rmatch x = true

Tactic:
right

Result:
case pos.mpr.intro.intro.intro.intro.nil.h
α : Type u_1
inst✝ : DecidableEq α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), (P * Q).rmatch x = true ↔ ∃ t u, x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
P Q : RegularExpression α
hepsilon : P.matchEpsilon = true
u : List α
hQ : Q.rmatch u = true
h : a :: x = [] ++ u
hP : P.rmatch [] = true
⊢ (Q.deriv a).rmatch x = true

Proof state:
case nil.mp
α : Type u_1
inst✝ : DecidableEq α
P Q : RegularExpression α
h : (P.matchEpsilon && Q.matchEpsilon) = true
⊢ ∃ t u, [] = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true

Tactic:
refine ⟨[], [], rfl, ?_⟩

Result:
case nil.mp
α : Type u_1
inst✝ : DecidableEq α
P Q : RegularExpression α
h : (P.matchEpsilon && Q.matchEpsilon) = true
⊢ P.rmatch [] = true ∧ Q.rmatch [] = true

Proof state:
case pos.mpr.intro.intro.intro.intro.cons.h
α : Type u_1
inst✝ : DecidableEq α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), (P * Q).rmatch x = true ↔ ∃ t u, x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
P Q : RegularExpression α
hepsilon : P.matchEpsilon = true
u : List α
hQ : Q.rmatch u = true
b : α
t : List α
h : a :: x = b :: t ++ u
hP : P.rmatch (b :: t) = true
⊢ ∃ t u, x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ Q.rmatch u = true

Tactic:
rw [List.cons_append, List.cons_eq_cons] at h

Result:
case pos.mpr.intro.intro.intro.intro.cons.h
α : Type u_1
inst✝ : DecidableEq α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), (P * Q).rmatch x = true ↔ ∃ t u, x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
P Q : RegularExpression α
hepsilon : P.matchEpsilon = true
u : List α
hQ : Q.rmatch u = true
b : α
t : List α
h : a = b ∧ x = t ++ u
hP : P.rmatch (b :: t) = true
⊢ ∃ t u, x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ Q.rmatch u = true

Proof state:
case pos.mp.inr
α : Type u_1
inst✝ : DecidableEq α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), (P * Q).rmatch x = true ↔ ∃ t u, x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
P Q : RegularExpression α
hepsilon : P.matchEpsilon = true
h : (Q.deriv a).rmatch x = true
⊢ ∃ t u, a :: x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true

Tactic:
exact ⟨[], a :: x, rfl, hepsilon, h⟩

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), (P * Q).rmatch x = true ↔ ∃ t u, x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
P Q : RegularExpression α
hepsilon : ¬P.matchEpsilon = true
⊢ (P.deriv a * Q).rmatch x = true ↔ ∃ t u, a :: x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true

Tactic:
rw [ih]

Result:
case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), (P * Q).rmatch x = true ↔ ∃ t u, x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
P Q : RegularExpression α
hepsilon : ¬P.matchEpsilon = true
⊢ (∃ t u, x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ Q.rmatch u = true) ↔
    ∃ t u, a :: x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true

Proof state:
case neg.mpr.intro.intro.intro.intro.cons
α : Type u_1
inst✝ : DecidableEq α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), (P * Q).rmatch x = true ↔ ∃ t u, x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
P Q : RegularExpression α
hepsilon : ¬P.matchEpsilon = true
u : List α
hQ : Q.rmatch u = true
b : α
t : List α
h : a = b ∧ x = t ++ u
hP : (P.deriv b).rmatch t = true
⊢ (P.deriv a).rmatch t = true

Tactic:
convert hP

Result:
case h.e'_2.h.e'_3.h.e'_4
α : Type u_1
inst✝ : DecidableEq α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), (P * Q).rmatch x = true ↔ ∃ t u, x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
P Q : RegularExpression α
hepsilon : ¬P.matchEpsilon = true
u : List α
hQ : Q.rmatch u = true
b : α
t : List α
h : a = b ∧ x = t ++ u
hP : (P.deriv b).rmatch t = true
⊢ a = b

Proof state:
case pos.mpr.intro.intro.intro.intro.cons.h
α : Type u_1
inst✝ : DecidableEq α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), (P * Q).rmatch x = true ↔ ∃ t u, x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
P Q : RegularExpression α
hepsilon : P.matchEpsilon = true
u : List α
hQ : Q.rmatch u = true
b : α
t : List α
h : a = b ∧ x = t ++ u
hP : (P.deriv b).rmatch t = true
⊢ (P.deriv a).rmatch t = true

Tactic:
convert hP

Result:
case h.e'_2.h.e'_3.h.e'_4
α : Type u_1
inst✝ : DecidableEq α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), (P * Q).rmatch x = true ↔ ∃ t u, x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
P Q : RegularExpression α
hepsilon : P.matchEpsilon = true
u : List α
hQ : Q.rmatch u = true
b : α
t : List α
h : a = b ∧ x = t ++ u
hP : (P.deriv b).rmatch t = true
⊢ a = b

Proof state:
case nil.mpr.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
P Q : RegularExpression α
h₁ : [] = [] ++ []
h₂ : P.matchEpsilon = true ∧ Q.rmatch [] = true
⊢ (P.matchEpsilon && Q.matchEpsilon) = true

Tactic:
rw [rmatch] at h₂

Result:
case nil.mpr.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
P Q : RegularExpression α
h₁ : [] = [] ++ []
h₂ : P.matchEpsilon = true ∧ Q.matchEpsilon = true
⊢ (P.matchEpsilon && Q.matchEpsilon) = true

Proof state:
case nil.mpr.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
P Q : RegularExpression α
h₁ : [] = [] ++ []
h₂ : P.matchEpsilon = true ∧ Q.matchEpsilon = true
⊢ (P.matchEpsilon && Q.matchEpsilon) = true

Tactic:
simp [h₂]

Result:
no goals