awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Computability.RegularExpressions (goal)
Goal:
α : Type u_1
inst : DecidableEq α
P : RegularExpression α
x : List α
IH :
  ∀ (t : List α) (_h : t.length < x.length),
    P.star.rmatch t = true ↔ ∃ (S : List (List α)), t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
S : List (List α)
hsum : x = S.flatten
helem : ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
⊢ P.star.rmatch x = true
have mpr : ∀
  (IH :
    ∀ (t : List α) (_h : t.length < length.{u_1} (α := α) []),
      P.star.rmatch t = true ↔ ∃ (S : List (List α)), t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true)
  (hsum : [] = S.flatten), P.star.rmatch [] = true
Tactic: rcases x with - | ⟨a, x⟩
Cleared hypotheses: x, IH, hsum
-- Lean 4 proof step from Mathlib.Computability.RegularExpressions (goal)
Goal:
α : Type u_1
inst : DecidableEq α
P : RegularExpression α
x : List α
IH :
  ∀ (t : List α) (_h : t.length < x.length),
    P.star.rmatch t = true ↔ ∃ (S : List (List α)), t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
S : List (List α)
hsum : x = S.flatten
helem : ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
mpr :
  ∀
    (IH :
      ∀ (t : List α) (_h : t.length < length.{u_1} (α := α) []),
        P.star.rmatch t = true ↔ ∃ (S : List (List α)), t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true)
    (hsum : [] = S.flatten), P.star.rmatch [] = true
⊢ P.star.rmatch x = true
have mpr₁ : ∀ (a : α) (x : List α)
  (IH :
    ∀ (t : List α) (_h : t.length < (a :: x).length),
      P.star.rmatch t = true ↔ ∃ (S : List (List α)), t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true)
  (hsum : a :: x = S.flatten), P.star.rmatch (a :: x) = true
Tactic: rcases x with - | ⟨a, x⟩
Cleared hypotheses: x, IH, hsum
-- Lean 4 proof step from Mathlib.Computability.RegularExpressions (goal)
Goal:
α : Type u_1
inst : DecidableEq α
P : RegularExpression α
S : List (List α)
helem : ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
a : α
x : List α
IH :
  ∀ (t : List α) (_h : t.length < (a :: x).length),
    P.star.rmatch t = true ↔ ∃ (S : List (List α)), t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
hsum : a :: x = S.flatten
⊢ P.star.rmatch (a :: x) = true
have mpr : ∃ (t : List α) (u : List α), x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ P.star.rmatch u = true
Tactic: rw [rmatch, deriv, mul_rmatch_iff]
-- Lean 4 proof step from Mathlib.Computability.RegularExpressions (goal)
Goal:
α : Type u_1
inst : DecidableEq α
P : RegularExpression α
S : List (List α)
helem : ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
a : α
x : List α
IH :
  ∀ (t : List α) (_h : t.length < (a :: x).length),
    P.star.rmatch t = true ↔ ∃ (S : List (List α)), t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
hsum : a :: x = S.flatten
⊢ ∃ (t : List α) (u : List α), x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ P.star.rmatch u = true
have mpr : ∀ (helem : ∀ (t : List α), Membership.mem (γ := List (List α)) [] t → t ≠ [] ∧ P.rmatch t = true)
  (hsum : a :: x = flatten []),
  ∃ (t : List α) (u : List α), x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ P.star.rmatch u = true
Tactic: rcases S with - | ⟨t', U⟩
Cleared hypotheses: S, helem, hsum
-- Lean 4 proof step from Mathlib.Computability.RegularExpressions (goal)
Goal:
α : Type u_1
inst : DecidableEq α
P : RegularExpression α
S : List (List α)
helem : ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
a : α
x : List α
IH :
  ∀ (t : List α) (_h : t.length < (a :: x).length),
    P.star.rmatch t = true ↔ ∃ (S : List (List α)), t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
hsum : a :: x = S.flatten
mpr :
  ∀ (helem : ∀ (t : List α), Membership.mem (γ := List (List α)) [] t → t ≠ [] ∧ P.rmatch t = true)
    (hsum : a :: x = flatten []),
    ∃ (t : List α) (u : List α), x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ P.star.rmatch u = true
⊢ ∃ (t : List α) (u : List α), x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ P.star.rmatch u = true
have mpr₁ : ∀ (t' : List α) (U : List (List α)) (helem : ∀ t ∈ t' :: U, t ≠ [] ∧ P.rmatch t = true)
  (hsum : a :: x = (t' :: U).flatten),
  ∃ (t : List α) (u : List α), x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ P.star.rmatch u = true
Tactic: rcases S with - | ⟨t', U⟩
Cleared hypotheses: S, helem, hsum
-- Lean 4 proof step from Mathlib.Computability.RegularExpressions (goal)
Goal:
α : Type u_1
inst : DecidableEq α
P : RegularExpression α
a : α
x : List α
IH :
  ∀ (t : List α) (_h : t.length < (a :: x).length),
    P.star.rmatch t = true ↔ ∃ (S : List (List α)), t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
t' : List α
U : List (List α)
helem : ∀ t ∈ t' :: U, t ≠ [] ∧ P.rmatch t = true
hsum : a :: x = (t' :: U).flatten
⊢ ∃ (t : List α) (u : List α), x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ P.star.rmatch u = true
have mpr : ∀ (helem : ∀ t ∈ [] :: U, t ≠ [] ∧ P.rmatch t = true) (hsum : a :: x = ([] :: U).flatten),
  ∃ (t : List α) (u : List α), x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ P.star.rmatch u = true
Tactic: obtain - | ⟨b, t⟩ := t'
Cleared hypotheses: t', helem, hsum
-- Lean 4 proof step from Mathlib.Computability.RegularExpressions (goal)
Goal:
α : Type u_1
inst : DecidableEq α
P : RegularExpression α
a : α
x : List α
IH :
  ∀ (t : List α) (_h : t.length < (a :: x).length),
    P.star.rmatch t = true ↔ ∃ (S : List (List α)), t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
t' : List α
U : List (List α)
helem : ∀ t ∈ t' :: U, t ≠ [] ∧ P.rmatch t = true
hsum : a :: x = (t' :: U).flatten
mpr :
  ∀ (helem : ∀ t ∈ [] :: U, t ≠ [] ∧ P.rmatch t = true) (hsum : a :: x = ([] :: U).flatten),
    ∃ (t : List α) (u : List α), x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ P.star.rmatch u = true
⊢ ∃ (t : List α) (u : List α), x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ P.star.rmatch u = true
have mpr₁ : ∀ (b : α) (t : List α) (helem : ∀ t_1 ∈ (b :: t) :: U, t_1 ≠ [] ∧ P.rmatch t_1 = true)
  (hsum : a :: x = ((b :: t) :: U).flatten),
  ∃ (t : List α) (u : List α), x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ P.star.rmatch u = true
Tactic: obtain - | ⟨b, t⟩ := t'
Cleared hypotheses: t', helem, hsum
-- Lean 4 proof step from Mathlib.Computability.RegularExpressions (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
P : RegularExpression α
a : α
x : List α
IH :
  ∀ (t : List α) (_h : t.length < (a :: x).length),
    P.star.rmatch t = true ↔ ∃ (S : List (List α)), t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
U : List (List α)
helem : ∀ t ∈ [] :: U, t ≠ [] ∧ P.rmatch t = true
hsum : a :: x = ([] :: U).flatten
⊢ ∃ (t : List α) (u : List α), x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ P.star.rmatch u = true
have helem₁ : (Ne.{u_1 + 1} (α := List α) [] [] ∧ P.rmatch [] = true) ∧ ∀ a ∈ U, a ≠ [] ∧ P.rmatch a = true
Tactic: simp only [forall_eq_or_imp, List.mem_cons] at helem
Cleared hypotheses: helem
-- Lean 4 proof step from Mathlib.Computability.RegularExpressions (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
P : RegularExpression α
a : α
x : List α
IH :
  ∀ (t : List α) (_h : t.length < (a :: x).length),
    P.star.rmatch t = true ↔ ∃ (S : List (List α)), 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 :: x = ((b :: t) :: U).flatten
⊢ ∃ (t : List α) (u : List α), x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ P.star.rmatch u = true
have hsum₁ : a = b ∧ x = t ++ U.flatten
Tactic: simp only [List.flatten_cons, List.cons_append, List.cons_eq_cons] at hsum
Cleared hypotheses: hsum
-- Lean 4 proof step from Mathlib.Computability.RegularExpressions (goal)
Goal:
α : Type u_1
inst : DecidableEq α
P : RegularExpression α
a : α
x : List α
IH :
  ∀ (t : List α) (_h : t.length < (a :: x).length),
    P.star.rmatch t = true ↔ ∃ (S : List (List α)), 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
⊢ ∃ (t : List α) (u : List α), x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ P.star.rmatch u = true
have mpr : (P.deriv a).rmatch t = true
Tactic: refine ⟨t, U.flatten, hsum.2, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Computability.RegularExpressions (goal)
Goal:
α : Type u_1
inst : DecidableEq α
P : RegularExpression α
a : α
x : List α
IH :
  ∀ (t : List α) (_h : t.length < (a :: x).length),
    P.star.rmatch t = true ↔ ∃ (S : List (List α)), 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
mpr : (P.deriv a).rmatch t = true
⊢ ∃ (t : List α) (u : List α), x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ P.star.rmatch u = true
have mpr₁ : P.star.rmatch U.flatten = true
Tactic: refine ⟨t, U.flatten, hsum.2, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Computability.RegularExpressions (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
P : RegularExpression α
a : α
x : List α
IH :
  ∀ (t : List α) (_h : t.length < (a :: x).length),
    P.star.rmatch t = true ↔ ∃ (S : List (List α)), 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
⊢ (P.deriv a).rmatch t = true
have helem₁ : b :: t ≠ [] ∧ P.rmatch (b :: t) = true
Tactic: specialize helem (b :: t) (by simp)
Cleared hypotheses: helem
-- Lean 4 proof step from Mathlib.Computability.RegularExpressions (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
P : RegularExpression α
a : α
x : List α
IH :
  ∀ (t : List α) (_h : t.length < (a :: x).length),
    P.star.rmatch t = true ↔ ∃ (S : List (List α)), 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
have helem₁ : b :: t ≠ [] ∧ (P.deriv b).rmatch t = true
Tactic: rw [rmatch] at helem
Cleared hypotheses: helem
-- Lean 4 proof step from Mathlib.Computability.RegularExpressions (goal)
Goal:
α : Type u_1
inst : DecidableEq α
P : RegularExpression α
a : α
x : List α
IH :
  ∀ (t : List α) (_h : t.length < (a :: x).length),
    P.star.rmatch t = true ↔ ∃ (S : List (List α)), 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
have h : a = b
Tactic: convert! helem.2
-- Lean 4 proof step from Mathlib.Computability.RegularExpressions (goal)
Goal:
α : Type u_1
inst : DecidableEq α
x : List α
⊢ rmatch zero x = true ↔ Membership.mem (γ := Language α) (matches' zero) x
have zero : false = true ↔ Membership.mem (γ := Language α) (matches' 0) x
Tactic: rw [zero_def, zero_rmatch]
-- Lean 4 proof step from Mathlib.Computability.RegularExpressions (goal)
Goal:
α : Type u_1
inst : DecidableEq α
x : List α
⊢ false = true ↔ Membership.mem (γ := Language α) (matches' 0) x
have zero : false = true → Membership.mem (γ := Language α) (matches' 0) x
Tactic: tauto
-- Lean 4 proof step from Mathlib.Computability.RegularExpressions (goal)
Goal:
α : Type u_1
inst : DecidableEq α
x : List α
zero : false = true → Membership.mem (γ := Language α) (matches' 0) x
⊢ false = true ↔ Membership.mem (γ := Language α) (matches' 0) x
have zero₁ : Membership.mem (γ := Language α) (matches' 0) x → false = true
Tactic: tauto
-- Lean 4 proof step from Mathlib.Computability.RegularExpressions (goal)
Goal:
α : Type u_1
inst : DecidableEq α
x : List α
⊢ rmatch epsilon x = true ↔ Membership.mem (γ := Language α) (matches' epsilon) x
have epsilon : rmatch 1 x = true ↔ Membership.mem (γ := Language α) (matches' 1) x
Tactic: rw [one_def, one_rmatch_iff, matches'_epsilon, Language.mem_one]
-- Lean 4 proof step from Mathlib.Computability.RegularExpressions (goal)
Goal:
α : Type u_1
inst : DecidableEq α
x : List α
epsilon : rmatch 1 x = true ↔ Membership.mem (γ := Language α) (matches' 1) x
⊢ rmatch RegularExpression.epsilon x = true ↔ Membership.mem (γ := Language α) (matches' RegularExpression.epsilon) x
have epsilon₁ : x = [] ↔ Membership.mem (γ := Language α) (matches' 1) x
Tactic: rw [one_def, one_rmatch_iff, matches'_epsilon, Language.mem_one]
-- Lean 4 proof step from Mathlib.Computability.RegularExpressions (goal)
Goal:
α : Type u_1
inst : DecidableEq α
x : List α
epsilon : rmatch 1 x = true ↔ Membership.mem (γ := Language α) (matches' 1) x
epsilon₁ : x = [] ↔ Membership.mem (γ := Language α) (matches' 1) x
⊢ rmatch RegularExpression.epsilon x = true ↔ Membership.mem (γ := Language α) (matches' RegularExpression.epsilon) x
have epsilon₂ : x = [] ↔ Membership.mem (γ := Language α) 1 x
Tactic: rw [one_def, one_rmatch_iff, matches'_epsilon, Language.mem_one]
-- Lean 4 proof step from Mathlib.Computability.RegularExpressions (goal)
Goal:
α : Type u_1
inst : DecidableEq α
x : List α
epsilon : rmatch 1 x = true ↔ Membership.mem (γ := Language α) (matches' 1) x
epsilon₁ : x = [] ↔ Membership.mem (γ := Language α) (matches' 1) x
epsilon₂ : x = [] ↔ Membership.mem (γ := Language α) 1 x
⊢ rmatch RegularExpression.epsilon x = true ↔ Membership.mem (γ := Language α) (matches' RegularExpression.epsilon) x
have epsilon₃ : x = [] ↔ x = []
Tactic: rw [one_def, one_rmatch_iff, matches'_epsilon, Language.mem_one]
-- Lean 4 proof step from Mathlib.Computability.RegularExpressions (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
x : List α
⊢ (char a).rmatch x = true ↔ x ∈ (char a).matches'
have char : x = [a] ↔ x ∈ (char a).matches'
Tactic: rw [char_rmatch_iff]
-- Lean 4 proof step from Mathlib.Computability.RegularExpressions (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a a_1 : RegularExpression α
ih₁ : ∀ (x : List α), a.rmatch x = true ↔ x ∈ a.matches'
ih₂ : ∀ (x : List α), a_1.rmatch x = true ↔ x ∈ a_1.matches'
x : List α
⊢ (a.plus a_1).rmatch x = true ↔ x ∈ (a.plus a_1).matches'
have plus : x ∈ a.matches' ∨ x ∈ a_1.matches' ↔ x ∈ (a + a_1).matches'
Tactic: rw [plus_def, add_rmatch_iff, ih₁, ih₂]
-- 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 α
⊢ (P.comp Q).rmatch x = true ↔ x ∈ (P.comp Q).matches'
have comp : (∃ (t : List α) (u : List α), x = t ++ u ∧ t ∈ P.matches' ∧ u ∈ Q.matches') ↔
  ∃ a ∈ P.matches', ∃ b ∈ Q.matches', a ++ b = x
Tactic: simp only [comp_def, mul_rmatch_iff, matches'_mul, Language.mem_mul, *]
-- 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 α
⊢ (∃ (t : List α) (u : List α), x = t ++ u ∧ t ∈ P.matches' ∧ u ∈ Q.matches') ↔
    ∃ a ∈ P.matches', ∃ b ∈ Q.matches', a ++ b = x
have comp : (∃ (t : List α) (u : List α), x = t ++ u ∧ t ∈ P.matches' ∧ u ∈ Q.matches') →
  ∃ a ∈ P.matches', ∃ b ∈ Q.matches', a ++ b = x
Tactic: tauto
-- 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
⊢ (∃ (t : List α) (u : List α), x = t ++ u ∧ t ∈ P.matches' ∧ u ∈ Q.matches') ↔
    ∃ a ∈ P.matches', ∃ b ∈ Q.matches', a ++ b = x
have comp₁ : (∃ a ∈ P.matches', ∃ b ∈ Q.matches', a ++ b = x) →
  ∃ (t : List α) (u : List α), x = t ++ u ∧ t ∈ P.matches' ∧ u ∈ Q.matches'
Tactic: tauto
-- 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'
⊢ (∃ (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 w_1 : List α), x = w ++ w_1 → w ∈ P.matches' → w_1 ∈ Q.matches' → ∃ a ∈ P.matches', ∃ b ∈ Q.matches', a ++ b = x
Tactic: tauto
-- 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
⊢ (∃ (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 → ∃ (t : List α) (u : List α), x = t ++ u ∧ t ∈ P.matches' ∧ u ∈ Q.matches'
Tactic: tauto
-- 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
⊢ (∃ (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 w_1 : List α), x = w ++ w_1 → w ∈ P.matches' → w_1 ∈ Q.matches' → w ∈ P.matches' ∧ ∃ b ∈ Q.matches', w ++ b = x
Tactic: tauto
-- 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
⊢ (∃ (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 w_1 : List α) → x = w ++ w_1 → w ∈ P.matches' → w_1 ∈ Q.matches' → List α
Tactic: tauto
-- 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 α
⊢ (∃ (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 w_1 : List α), x = w ++ w_1 → w ∈ P.matches' → w_1 ∈ Q.matches' → w ∈ P.matches'
Tactic: tauto