-- Lean 4 proof step from Mathlib.Computability.RegularExpressions (goal)
Goal:
α : 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 α
comp :
  (∃ (t : List α) (u : List α), x = t ++ u ∧ t ∈ P.matches' ∧ u ∈ Q.matches') →
    ∃ a ∈ P.matches', ∃ b ∈ Q.matches', a ++ b = x
comp₁ :
  (∃ a ∈ P.matches', ∃ b ∈ Q.matches', a ++ b = x) →
    ∃ (t : List α) (u : List α), x = t ++ u ∧ t ∈ P.matches' ∧ u ∈ Q.matches'
comp₂ comp₃ comp₄ :
  ∀ (w w_1 : List α), x = w ++ w_1 → w ∈ P.matches' → w_1 ∈ Q.matches' → ∃ a ∈ P.matches', ∃ b ∈ Q.matches', a ++ b = x
comp₅ comp₆ comp₇ :
  ∀ w ∈ P.matches',
    ∀ w_1 ∈ Q.matches', w ++ w_1 = x → ∃ (t : List α) (u : List α), x = t ++ u ∧ t ∈ P.matches' ∧ u ∈ Q.matches'
comp₈ comp₉ comp₁₀ :
  ∀ (w w_1 : List α), x = w ++ w_1 → w ∈ P.matches' → w_1 ∈ Q.matches' → ∃ a ∈ P.matches', ∃ b ∈ Q.matches', a ++ b = x
comp₁₁ comp₁₂ comp₁₃ :
  ∀ w ∈ P.matches',
    ∀ w_1 ∈ Q.matches', w ++ w_1 = x → ∃ (t : List α) (u : List α), x = t ++ u ∧ t ∈ P.matches' ∧ u ∈ Q.matches'
comp₁₄ comp₁₅ :
  ∀ (w w_1 : List α), x = w ++ w_1 → w ∈ P.matches' → w_1 ∈ Q.matches' → ∃ a ∈ P.matches', ∃ b ∈ Q.matches', a ++ b = x
comp₁₆ :
  ∀ (w w_1 : List α), x = w ++ w_1 → w ∈ P.matches' → w_1 ∈ Q.matches' → w ∈ P.matches' ∧ ∃ b ∈ Q.matches', w ++ b = x
comp₁₇ : (w w_1 : List α) → x = w ++ w_1 → w ∈ P.matches' → w_1 ∈ Q.matches' → List α
comp₁₈ :
  ∀ (w w_1 : List α), x = w ++ w_1 → w ∈ P.matches' → w_1 ∈ Q.matches' → w ∈ P.matches' ∧ ∃ b ∈ Q.matches', w ++ b = x
comp₁₉ : (w w_1 : List α) → x = w ++ w_1 → w ∈ P.matches' → w_1 ∈ Q.matches' → List α
comp₂₀ : ∀ (w w_1 : List α), x = w ++ w_1 → w ∈ P.matches' → w_1 ∈ Q.matches' → w ∈ P.matches'
comp₂₁ : ∀ (w w_1 : List α), x = w ++ w_1 → w ∈ P.matches' → w_1 ∈ Q.matches' → ∃ b ∈ Q.matches', w ++ b = x
comp₂₂ : (w w_1 : List α) → x = w ++ w_1 → w ∈ P.matches' → w_1 ∈ Q.matches' → List α
comp₂₃ : ∀ (w w_1 : List α), x = w ++ w_1 → w ∈ P.matches' → w_1 ∈ Q.matches' → w ∈ P.matches'
comp₂₄ : ∀ (w w_1 : List α), x = w ++ w_1 → w ∈ P.matches' → w_1 ∈ Q.matches' → ∃ b ∈ Q.matches', w ++ b = x
comp₂₅ : (w w_1 : List α) → x = w ++ w_1 → w ∈ P.matches' → w_1 ∈ Q.matches' → List α
comp₂₆ comp₂₇ : ∀ (w w_1 : List α), x = w ++ w_1 → w ∈ P.matches' → w_1 ∈ Q.matches' → ∃ b ∈ Q.matches', w ++ b = x
comp₂₈ comp₂₉ :
  ∀ w ∈ P.matches',
    ∀ w_1 ∈ Q.matches', w ++ w_1 = x → ∃ (t : List α) (u : List α), x = t ++ u ∧ t ∈ P.matches' ∧ u ∈ Q.matches'
comp₃₀ :
  ∀ w ∈ P.matches', ∀ w_1 ∈ Q.matches', w ++ w_1 = x → ∃ (u : List α), x = w ++ u ∧ w ∈ P.matches' ∧ u ∈ Q.matches'
comp₃₁ : (w : List α) → w ∈ P.matches' → (w_1 : List α) → w_1 ∈ Q.matches' → w ++ w_1 = x → List α
comp₃₂ :
  ∀ w ∈ P.matches', ∀ w_1 ∈ Q.matches', w ++ w_1 = x → ∃ (u : List α), x = w ++ u ∧ w ∈ P.matches' ∧ u ∈ Q.matches'
comp₃₃ : (w : List α) → w ∈ P.matches' → (w_1 : List α) → w_1 ∈ Q.matches' → w ++ w_1 = x → List α
⊢ (∃ (t : List α) (u : List α), x = t ++ u ∧ t ∈ P.matches' ∧ u ∈ Q.matches') ↔
    ∃ a ∈ P.matches', ∃ b ∈ Q.matches', a ++ b = x
have comp₃₄ : ∀ w ∈ P.matches', ∀ w_1 ∈ Q.matches', w ++ w_1 = x → x = w ++ w_1 ∧ w ∈ P.matches' ∧ w_1 ∈ Q.matches'
Tactic: tauto