-- Mathlib/Computability/RegularExpressions.lean
theorem rmatch_iff_matches' (P : RegularExpression α) (x : List α) :
    P.rmatch x ↔ x ∈ P.matches'

Proof state:
case comp
α : Type u_1
inst✝ : DecidableEq α
P Q : RegularExpression α
ih₁ : ∀ (x : List α), P.rmatch x = true ↔ x ∈ P.matches'
ih₂ : ∀ (x : List α), Q.rmatch x = true ↔ x ∈ Q.matches'
x : List α
⊢ (∃ t u, x = t ++ u ∧ t ∈ P.matches' ∧ u ∈ Q.matches') ↔ ∃ a ∈ P.matches', ∃ b ∈ Q.matches', a ++ b = x

Tactic:
tauto

Result:
no goals

Proof state:
case char
α : Type u_1
inst✝ : DecidableEq α
a✝ : α
x : List α
⊢ x = [a✝] ↔ x ∈ (char a✝).matches'

Tactic:
rfl

Result:
no goals

Proof state:
case zero
α : Type u_1
inst✝ : DecidableEq α
x : List α
⊢ false = true ↔ x ∈ matches' 0

Tactic:
tauto

Result:
no goals

Proof state:
case zero
α : Type u_1
inst✝ : DecidableEq α
x : List α
⊢ zero.rmatch x = true ↔ x ∈ zero.matches'

Tactic:
rw [zero_def, zero_rmatch]

Result:
case zero
α : Type u_1
inst✝ : DecidableEq α
x : List α
⊢ false = true ↔ x ∈ matches' 0

Proof state:
case epsilon
α : Type u_1
inst✝ : DecidableEq α
x : List α
⊢ epsilon.rmatch x = true ↔ x ∈ epsilon.matches'

Tactic:
rw [one_def, one_rmatch_iff, matches'_epsilon, Language.mem_one]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
P : RegularExpression α
x : List α
⊢ P.rmatch x = true ↔ x ∈ P.matches'

Tactic:
induction P generalizing x with
| zero =>
  rw [zero_def, zero_rmatch]
  tauto
| epsilon =>
  rw [one_def, one_rmatch_iff, matches'_epsilon, Language.mem_one]
| char =>
  rw [char_rmatch_iff]
  rfl
| plus _ _ ih₁ ih₂ =>
  rw [plus_def, add_rmatch_iff, ih₁, ih₂]
  rfl
| comp P Q ih₁ ih₂ =>
  simp only [comp_def, mul_rmatch_iff, matches'_mul, Language.mem_mul, *]
  tauto
| star _ ih =>
  simp only [star_rmatch_iff, matches'_star, ih, Language.mem_kstar_iff_exists_nonempty, and_comm]

Result:
no goals

Proof state:
case star
α : Type u_1
inst✝ : DecidableEq α
a✝ : RegularExpression α
ih : ∀ (x : List α), a✝.rmatch x = true ↔ x ∈ a✝.matches'
x : List α
⊢ a✝.star.rmatch x = true ↔ x ∈ a✝.star.matches'

Tactic:
simp only [star_rmatch_iff, matches'_star, ih, Language.mem_kstar_iff_exists_nonempty, and_comm]

Result:
no goals

Proof state:
case plus
α : Type u_1
inst✝ : DecidableEq α
a✝¹ a✝ : RegularExpression α
ih₁ : ∀ (x : List α), a✝¹.rmatch x = true ↔ x ∈ a✝¹.matches'
ih₂ : ∀ (x : List α), a✝.rmatch x = true ↔ x ∈ a✝.matches'
x : List α
⊢ x ∈ a✝¹.matches' ∨ x ∈ a✝.matches' ↔ x ∈ (a✝¹ + a✝).matches'

Tactic:
rfl

Result:
no goals

Proof state:
case comp
α : Type u_1
inst✝ : DecidableEq α
P Q : RegularExpression α
ih₁ : ∀ (x : List α), P.rmatch x = true ↔ x ∈ P.matches'
ih₂ : ∀ (x : List α), Q.rmatch x = true ↔ x ∈ Q.matches'
x : List α
⊢ (P.comp Q).rmatch x = true ↔ x ∈ (P.comp Q).matches'

Tactic:
simp only [comp_def, mul_rmatch_iff, matches'_mul, Language.mem_mul, *]

Result:
case comp
α : Type u_1
inst✝ : DecidableEq α
P Q : RegularExpression α
ih₁ : ∀ (x : List α), P.rmatch x = true ↔ x ∈ P.matches'
ih₂ : ∀ (x : List α), Q.rmatch x = true ↔ x ∈ Q.matches'
x : List α
⊢ (∃ t u, x = t ++ u ∧ t ∈ P.matches' ∧ u ∈ Q.matches') ↔ ∃ a ∈ P.matches', ∃ b ∈ Q.matches', a ++ b = x

Proof state:
case char
α : Type u_1
inst✝ : DecidableEq α
a✝ : α
x : List α
⊢ (char a✝).rmatch x = true ↔ x ∈ (char a✝).matches'

Tactic:
rw [char_rmatch_iff]

Result:
case char
α : Type u_1
inst✝ : DecidableEq α
a✝ : α
x : List α
⊢ x = [a✝] ↔ x ∈ (char a✝).matches'

Proof state:
case plus
α : Type u_1
inst✝ : DecidableEq α
a✝¹ a✝ : RegularExpression α
ih₁ : ∀ (x : List α), a✝¹.rmatch x = true ↔ x ∈ a✝¹.matches'
ih₂ : ∀ (x : List α), a✝.rmatch x = true ↔ x ∈ a✝.matches'
x : List α
⊢ (a✝¹.plus a✝).rmatch x = true ↔ x ∈ (a✝¹.plus a✝).matches'

Tactic:
rw [plus_def, add_rmatch_iff, ih₁, ih₂]

Result:
case plus
α : Type u_1
inst✝ : DecidableEq α
a✝¹ a✝ : RegularExpression α
ih₁ : ∀ (x : List α), a✝¹.rmatch x = true ↔ x ∈ a✝¹.matches'
ih₂ : ∀ (x : List α), a✝.rmatch x = true ↔ x ∈ a✝.matches'
x : List α
⊢ x ∈ a✝¹.matches' ∨ x ∈ a✝.matches' ↔ x ∈ (a✝¹ + a✝).matches'