awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Computability.RegularExpressions (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
x : List α
ih :
  ∀ (P Q : RegularExpression α),
    (P * Q).rmatch x = true ↔ ∃ (t : List α) (u : List α), x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
P Q : RegularExpression α
hepsilon : ¬P.matchEpsilon = true
neg :
  (∃ (t : List α) (u : List α), x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ Q.rmatch u = true) →
    ∃ (t : List α) (u : List α), a :: x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
⊢ (∃ (t : List α) (u : List α), x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ Q.rmatch u = true) ↔
    ∃ (t : List α) (u : List α), a :: x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
have neg₁ : (∃ (t : List α) (u : List α), a :: x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true) →
  ∃ (t : List α) (u : List α), x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ Q.rmatch u = true
Tactic: constructor
-- Lean 4 proof step from Mathlib.Computability.RegularExpressions (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
x : List α
ih :
  ∀ (P Q : RegularExpression α),
    (P * Q).rmatch x = true ↔ ∃ (t : List α) (u : List α), x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
P Q : RegularExpression α
hepsilon : ¬P.matchEpsilon = true
t u : List α
h : x = t ++ u
hP : (P.deriv a).rmatch t = true
hQ : Q.rmatch u = true
⊢ a :: x = a :: t ++ u ∧ P.rmatch (a :: t) = true ∧ Q.rmatch u = true
have left : a :: x = a :: t ++ u
Tactic: tauto
-- Lean 4 proof step from Mathlib.Computability.RegularExpressions (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
x : List α
ih :
  ∀ (P Q : RegularExpression α),
    (P * Q).rmatch x = true ↔ ∃ (t : List α) (u : List α), x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
P Q : RegularExpression α
hepsilon : ¬P.matchEpsilon = true
t u : List α
h : x = t ++ u
hP : (P.deriv a).rmatch t = true
hQ : Q.rmatch u = true
left : a :: x = a :: t ++ u
⊢ a :: x = a :: t ++ u ∧ P.rmatch (a :: t) = true ∧ Q.rmatch u = true
have right : P.rmatch (a :: t) = true
Tactic: tauto
-- Lean 4 proof step from Mathlib.Computability.RegularExpressions (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
x : List α
ih :
  ∀ (P Q : RegularExpression α),
    (P * Q).rmatch x = true ↔ ∃ (t : List α) (u : List α), x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
P Q : RegularExpression α
hepsilon : ¬P.matchEpsilon = true
t u : List α
h : a :: x = t ++ u
hP : P.rmatch t = true
hQ : Q.rmatch u = true
⊢ ∃ (t : List α) (u : List α), x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ Q.rmatch u = true
have neg : ∀ (h : a :: x = [] ++ u) (hP : P.rmatch [] = true),
  ∃ (t : List α) (u : List α), x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ Q.rmatch u = true
Tactic: rcases t with - | ⟨b, t⟩
Cleared hypotheses: t, h, hP
-- Lean 4 proof step from Mathlib.Computability.RegularExpressions (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
x : List α
ih :
  ∀ (P Q : RegularExpression α),
    (P * Q).rmatch x = true ↔ ∃ (t : List α) (u : List α), x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
P Q : RegularExpression α
hepsilon : ¬P.matchEpsilon = true
t u : List α
h : a :: x = t ++ u
hP : P.rmatch t = true
hQ : Q.rmatch u = true
neg :
  ∀ (h : a :: x = [] ++ u) (hP : P.rmatch [] = true),
    ∃ (t : List α) (u : List α), x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ Q.rmatch u = true
⊢ ∃ (t : List α) (u : List α), x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ Q.rmatch u = true
have neg₁ : ∀ (b : α) (t : List α) (h : a :: x = b :: t ++ u) (hP : P.rmatch (b :: t) = true),
  ∃ (t : List α) (u : List α), x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ Q.rmatch u = true
Tactic: rcases t with - | ⟨b, t⟩
Cleared hypotheses: t, h, hP
-- Lean 4 proof step from Mathlib.Computability.RegularExpressions (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
x : List α
ih :
  ∀ (P Q : RegularExpression α),
    (P * Q).rmatch x = true ↔ ∃ (t : List α) (u : List α), 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 : List α) (u : List α), x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ Q.rmatch u = true
have h₁ : a = b ∧ x = t ++ u
Tactic: rw [List.cons_append, List.cons_eq_cons] at h
Cleared hypotheses: h, hP
-- Lean 4 proof step from Mathlib.Computability.RegularExpressions (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
x : List α
ih :
  ∀ (P Q : RegularExpression α),
    (P * Q).rmatch x = true ↔ ∃ (t : List α) (u : List α), 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 : List α) (u : List α), x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ Q.rmatch u = true
have neg : (P.deriv a).rmatch t = true
Tactic: refine ⟨t, u, h.2, ?_, hQ⟩
-- Lean 4 proof step from Mathlib.Computability.RegularExpressions (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
x : List α
ih :
  ∀ (P Q : RegularExpression α),
    (P * Q).rmatch x = true ↔ ∃ (t : List α) (u : List α), 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
⊢ (P.deriv a).rmatch t = true
have hP₁ : (P.deriv b).rmatch t = true
Tactic: rw [rmatch] at hP
Cleared hypotheses: hP
-- Lean 4 proof step from Mathlib.Computability.RegularExpressions (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
x : List α
ih :
  ∀ (P Q : RegularExpression α),
    (P * Q).rmatch x = true ↔ ∃ (t : List α) (u : List α), 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
have h₁ : a = b
Tactic: convert! hP
-- Lean 4 proof step from Mathlib.Computability.RegularExpressions (goal)
Goal:
α : Type u_1
inst : DecidableEq α
P Q : RegularExpression α
x : List α
⊢ (P * Q).rmatch x = true ↔ ∃ (t : List α) (u : List α), x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
have nil : ∀ (P Q : RegularExpression α),
  (P * Q).rmatch [] = true ↔ ∃ (t : List α) (u : List α), [] = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
Tactic: induction x generalizing P Q with
  | nil =>
    rw [rmatch]; simp only [matchEpsilon]
    constructor
    · intro h
      refine ⟨[], [], rfl, ?_⟩
      rw [rmatch, rmatch]
      rwa [Bool.and_eq_true_iff] at h
    · rintro ⟨t, u, h₁, h₂⟩
      obtain ⟨rfl, rfl⟩ := List.append_eq_nil_iff.1 h₁.symm
      repeat rw [rmatch] at h₂
      simp [h₂]
  | cons a x ih =>
    rw [rmatch]; simp only [deriv]
    split_ifs with hepsilon
    · rw [add_rmatch_iff, ih]
      constructor
      · rintro (⟨t, u, _⟩ | h)
        · exact ⟨a :: t, u, by tauto⟩
        · exact ⟨[], a :: x, rfl, hepsilon, h⟩
      · rintro ⟨t, u, h, hP, hQ⟩
        rcases t with - | ⟨b, t⟩
        · right
          rw [List.nil_append] at h
          rw [← h] at hQ
          exact hQ
        · left
          rw [List.cons_append, List.cons_eq_cons] at h
          refine ⟨t, u, h.2, ?_, hQ⟩
          rw [rmatch] at hP
          convert! hP
          exact h.1
    · rw [ih]
      constructor <;> rintro ⟨t, u, h, hP, hQ⟩
      · exact ⟨a :: t, u, by tauto⟩
      · rcases t with - | ⟨b, t⟩
        · contradiction
        · rw [List.cons_append, List.cons_eq_cons] at h
          refine ⟨t, u, h.2, ?_, hQ⟩
          rw [rmatch] at hP
          convert! hP
          exact h.1
Cleared hypotheses: P, Q, x
-- Lean 4 proof step from Mathlib.Computability.RegularExpressions (goal)
Goal:
α : Type u_1
inst : DecidableEq α
P Q : RegularExpression α
x : List α
nil :
  ∀ (P Q : RegularExpression α),
    (P * Q).rmatch [] = true ↔ ∃ (t : List α) (u : List α), [] = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
⊢ (P * Q).rmatch x = true ↔ ∃ (t : List α) (u : List α), x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
have cons : ∀ (a : α) (x : List α)
  (ih :
    ∀ (P Q : RegularExpression α),
      (P * Q).rmatch x = true ↔ ∃ (t : List α) (u : List α), x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true)
  (P Q : RegularExpression α),
  (P * Q).rmatch (a :: x) = true ↔ ∃ (t : List α) (u : List α), a :: x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
Tactic: induction x generalizing P Q with
  | nil =>
    rw [rmatch]; simp only [matchEpsilon]
    constructor
    · intro h
      refine ⟨[], [], rfl, ?_⟩
      rw [rmatch, rmatch]
      rwa [Bool.and_eq_true_iff] at h
    · rintro ⟨t, u, h₁, h₂⟩
      obtain ⟨rfl, rfl⟩ := List.append_eq_nil_iff.1 h₁.symm
      repeat rw [rmatch] at h₂
      simp [h₂]
  | cons a x ih =>
    rw [rmatch]; simp only [deriv]
    split_ifs with hepsilon
    · rw [add_rmatch_iff, ih]
      constructor
      · rintro (⟨t, u, _⟩ | h)
        · exact ⟨a :: t, u, by tauto⟩
        · exact ⟨[], a :: x, rfl, hepsilon, h⟩
      · rintro ⟨t, u, h, hP, hQ⟩
        rcases t with - | ⟨b, t⟩
        · right
          rw [List.nil_append] at h
          rw [← h] at hQ
          exact hQ
        · left
          rw [List.cons_append, List.cons_eq_cons] at h
          refine ⟨t, u, h.2, ?_, hQ⟩
          rw [rmatch] at hP
          convert! hP
          exact h.1
    · rw [ih]
      constructor <;> rintro ⟨t, u, h, hP, hQ⟩
      · exact ⟨a :: t, u, by tauto⟩
      · rcases t with - | ⟨b, t⟩
        · contradiction
        · rw [List.cons_append, List.cons_eq_cons] at h
          refine ⟨t, u, h.2, ?_, hQ⟩
          rw [rmatch] at hP
          convert! hP
          exact h.1
Cleared hypotheses: P, Q, x
-- Lean 4 proof step from Mathlib.Computability.RegularExpressions (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
P : RegularExpression α
x : List α
⊢ P.star.rmatch x = true ↔ ∃ (S : List (List α)), x = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
have 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
Tactic: have IH := fun t (_h : List.length t < List.length x) => star_rmatch_iff P t
-- 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
⊢ P.star.rmatch x = true ↔ ∃ (S : List (List α)), x = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
have mp : P.star.rmatch x = true → ∃ (S : List (List α)), x = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
Tactic: constructor
-- 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
mp : P.star.rmatch x = true → ∃ (S : List (List α)), x = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
⊢ P.star.rmatch x = true ↔ ∃ (S : List (List α)), x = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
have mpr : (∃ (S : List (List α)), x = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true) → P.star.rmatch x = true
Tactic: constructor
-- 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
⊢ P.star.rmatch x = true → ∃ (S : List (List α)), x = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
have mp : ∀
  (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),
  P.star.rmatch [] = true → ∃ (S : List (List α)), [] = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
Tactic: rcases x with - | ⟨a, x⟩
Cleared hypotheses: x, IH
-- 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
mp :
  ∀
    (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),
    P.star.rmatch [] = true → ∃ (S : List (List α)), [] = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
⊢ P.star.rmatch x = true → ∃ (S : List (List α)), x = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
have mp₁ : ∀ (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),
  P.star.rmatch (a :: x) = true → ∃ (S : List (List α)), a :: x = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
Tactic: rcases x with - | ⟨a, x⟩
Cleared hypotheses: x, IH
-- Lean 4 proof step from Mathlib.Computability.RegularExpressions (goal)
Goal:
α : Type u_1
inst : DecidableEq α
P : RegularExpression α
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
_h : P.star.rmatch [] = true
⊢ ∃ (S : List (List α)), [] = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
have h : Eq.{u_1 + 1} (α := List α) [] (flatten []) ∧
  ∀ (t : List α), Membership.mem (γ := List (List α)) [] t → t ≠ [] ∧ P.rmatch t = true
Tactic: use []
-- Lean 4 proof step from Mathlib.Computability.RegularExpressions (goal)
Goal:
α : Type u_1
inst : DecidableEq α
P : RegularExpression α
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
_h : P.star.rmatch [] = true
⊢ Eq.{u_1 + 1} (α := List α) [] [] ∧
    ∀ (t : List α), Membership.mem (γ := List (List α)) [] t → ¬t = [] ∧ P.rmatch t = true
have h : Eq.{u_1 + 1} (α := List α) [] []
Tactic: tauto
-- Lean 4 proof step from Mathlib.Computability.RegularExpressions (goal)
Goal:
α : Type u_1
inst : DecidableEq α
P : RegularExpression α
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
_h : P.star.rmatch [] = true
h : Eq.{u_1 + 1} (α := List α) [] []
⊢ Eq.{u_1 + 1} (α := List α) [] [] ∧
    ∀ (t : List α), Membership.mem (γ := List (List α)) [] t → ¬t = [] ∧ P.rmatch t = true
have h₁ : ∀ (t : List α), Membership.mem (γ := List (List α)) [] t → ¬t = [] ∧ P.rmatch t = true
Tactic: tauto
-- Lean 4 proof step from Mathlib.Computability.RegularExpressions (goal)
Goal:
α : Type u_1
inst : DecidableEq α
P : RegularExpression α
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
_h : P.star.rmatch [] = true
h : Eq.{u_1 + 1} (α := List α) [] []
h₁ : ∀ (t : List α), Membership.mem (γ := List (List α)) [] t → ¬t = [] ∧ P.rmatch t = true
h₂ h₃ h₄ : Eq.{u_1 + 1} (α := List α) [] []
h₅ h₆ : ∀ (t : List α), Membership.mem (γ := List (List α)) [] t → ¬t = [] ∧ P.rmatch t = true
⊢ Eq.{u_1 + 1} (α := List α) [] [] ∧
    ∀ (t : List α), Membership.mem (γ := List (List α)) [] t → ¬t = [] ∧ P.rmatch t = true
have h₇ : ∀ (t : List α), Membership.mem (γ := List (List α)) [] t → ¬t = []
Tactic: tauto
-- Lean 4 proof step from Mathlib.Computability.RegularExpressions (goal)
Goal:
α : Type u_1
inst : DecidableEq α
P : RegularExpression α
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
_h : P.star.rmatch [] = true
h : Eq.{u_1 + 1} (α := List α) [] []
h₁ : ∀ (t : List α), Membership.mem (γ := List (List α)) [] t → ¬t = [] ∧ P.rmatch t = true
h₂ h₃ h₄ : Eq.{u_1 + 1} (α := List α) [] []
h₅ h₆ : ∀ (t : List α), Membership.mem (γ := List (List α)) [] t → ¬t = [] ∧ P.rmatch t = true
h₇ : ∀ (t : List α), Membership.mem (γ := List (List α)) [] t → ¬t = []
⊢ Eq.{u_1 + 1} (α := List α) [] [] ∧
    ∀ (t : List α), Membership.mem (γ := List (List α)) [] t → ¬t = [] ∧ P.rmatch t = true
have h₈ : ∀ (t : List α), Membership.mem (γ := List (List α)) [] t → P.rmatch t = true
Tactic: tauto
-- 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
⊢ P.star.rmatch (a :: x) = true → ∃ (S : List (List α)), a :: x = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
have mp : (∃ (t : List α) (u : List α), x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ P.star.rmatch u = true) →
  ∃ (S : List (List α)), a :: x = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = 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 α
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 u : List α
hs : x = t ++ u
ht : (P.deriv a).rmatch t = true
hu : P.star.rmatch u = true
⊢ u.length < (a :: x).length
have rw : u.length < t.length + u.length + 1
Tactic: rw [hs, List.length_cons, List.length_append]
-- 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
t u : List α
hs : x = t ++ u
ht : (P.deriv a).rmatch t = true
hu : P.star.rmatch u = true
⊢ ∃ (S : List (List α)), a :: x = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
have hwf : u.length < (a :: x).length
Tactic: have hwf : u.length < (List.cons a x).length := by
          rw [hs, List.length_cons, List.length_append]
          lia
-- 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
t u : List α
hs : x = t ++ u
ht : (P.deriv a).rmatch t = true
hu : P.star.rmatch u = true
hwf : u.length < (a :: x).length
⊢ ∃ (S : List (List α)), a :: x = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
have hu₁ : ∃ (S : List (List α)), u = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
Tactic: rw [IH _ hwf] at hu
Cleared hypotheses: hu, hwf
-- 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 u : List α
hs : x = t ++ u
ht : (P.deriv a).rmatch t = true
hu : ∃ (S : List (List α)), u = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
hwf : u.length < (a :: x).length
⊢ ∃ (S : List (List α)), a :: x = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
have mp : ∀ (S' : List (List α)) (hsum : u = S'.flatten) (helem : ∀ t ∈ S', t ≠ [] ∧ P.rmatch t = true),
  ∃ (S : List (List α)), a :: x = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
Tactic: rcases hu with ⟨S', hsum, helem⟩
Cleared hypotheses: hu
-- 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 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
⊢ ∃ (S : List (List α)), a :: x = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
have h : a :: x = ((a :: t) :: S').flatten ∧ ∀ t_1 ∈ (a :: t) :: S', t_1 ≠ [] ∧ P.rmatch t_1 = true
Tactic: use (a :: t) :: S'
-- 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 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
⊢ a :: x = ((a :: t) :: S').flatten ∧ ∀ t_1 ∈ (a :: t) :: S', t_1 ≠ [] ∧ P.rmatch t_1 = true
have h : a :: x = ((a :: t) :: S').flatten
Tactic: constructor
-- 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 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
h : a :: x = ((a :: t) :: S').flatten
⊢ a :: x = ((a :: t) :: S').flatten ∧ ∀ t_1 ∈ (a :: t) :: S', t_1 ≠ [] ∧ P.rmatch t_1 = true
have h₁ : ∀ t_1 ∈ (a :: t) :: S', t_1 ≠ [] ∧ P.rmatch t_1 = true
Tactic: constructor
-- 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 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
have h : a :: t ≠ [] ∧ P.rmatch (a :: 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'
Cleared hypotheses: t', ht'
-- 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 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'
h : a :: t ≠ [] ∧ P.rmatch (a :: t) = true
⊢ t' ≠ [] ∧ P.rmatch t' = true
have h₁ : ∀ (ht' : Mem 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'
Cleared hypotheses: ht'