awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Computability.RegularExpressions (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a head_1 head : α
tail : List α
h : a = head_1
cons : rmatch 0 tail = true ↔ head_1 = a ∧ head :: tail = []
⊢ (deriv 1 head).rmatch tail = true ↔ head_1 = a ∧ head :: tail = []
have cons₁ : false = true ↔ head_1 = a ∧ head :: tail = []
Tactic: simp_rw [deriv_one, zero_rmatch, reduceCtorEq, and_false]
-- Lean 4 proof step from Mathlib.Computability.RegularExpressions (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a head_1 head : α
tail : List α
h : a = head_1
cons : rmatch 0 tail = true ↔ head_1 = a ∧ head :: tail = []
cons₁ : false = true ↔ head_1 = a ∧ head :: tail = []
⊢ (deriv 1 head).rmatch tail = true ↔ head_1 = a ∧ head :: tail = []
have cons₂ : False ↔ head_1 = a ∧ False
Tactic: simp_rw [deriv_one, zero_rmatch, reduceCtorEq, and_false]
-- Lean 4 proof step from Mathlib.Computability.RegularExpressions (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a head_1 head : α
tail : List α
h : ¬a = head_1
⊢ (deriv 0 head).rmatch tail = true ↔ head_1 = a ∧ head :: tail = []
have cons : rmatch 0 tail = true ↔ head_1 = a ∧ head :: tail = []
Tactic: simp_rw [deriv_zero, zero_rmatch, reduceCtorEq, and_false]
-- Lean 4 proof step from Mathlib.Computability.RegularExpressions (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a head_1 head : α
tail : List α
h : ¬a = head_1
cons : rmatch 0 tail = true ↔ head_1 = a ∧ head :: tail = []
⊢ (deriv 0 head).rmatch tail = true ↔ head_1 = a ∧ head :: tail = []
have cons₁ : false = true ↔ head_1 = a ∧ head :: tail = []
Tactic: simp_rw [deriv_zero, zero_rmatch, reduceCtorEq, and_false]
-- Lean 4 proof step from Mathlib.Computability.RegularExpressions (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a head_1 head : α
tail : List α
h : ¬a = head_1
cons : rmatch 0 tail = true ↔ head_1 = a ∧ head :: tail = []
cons₁ : false = true ↔ head_1 = a ∧ head :: tail = []
⊢ (deriv 0 head).rmatch tail = true ↔ head_1 = a ∧ head :: tail = []
have cons₂ : False ↔ head_1 = a ∧ False
Tactic: simp_rw [deriv_zero, zero_rmatch, reduceCtorEq, and_false]
-- Lean 4 proof step from Mathlib.Computability.RegularExpressions (goal)
Goal:
α : Type u_1
inst : DecidableEq α
head : α
tail : List α
ih : ∀ (P Q : RegularExpression α), (P + Q).rmatch tail = true ↔ P.rmatch tail = true ∨ Q.rmatch tail = true
P Q : RegularExpression α
⊢ (P + Q).rmatch (head :: tail) = true ↔ P.rmatch (head :: tail) = true ∨ Q.rmatch (head :: tail) = true
have cons : (P.deriv head + Q.deriv head).rmatch tail = true ↔ P.rmatch (head :: tail) = true ∨ Q.rmatch (head :: tail) = true
Tactic: rw [rmatch, deriv_add]
-- 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 ↔ P.rmatch x = true ∨ Q.rmatch x = true
have nil : ∀ (P Q : RegularExpression α), (P + Q).rmatch [] = true ↔ P.rmatch [] = true ∨ Q.rmatch [] = true
Tactic: induction x generalizing P Q with
  | nil => simp only [rmatch, matchEpsilon, Bool.or_eq_true_iff]
  | cons _ _ ih =>
    rw [rmatch, deriv_add]
    exact ih _ _
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 ↔ P.rmatch [] = true ∨ Q.rmatch [] = true
⊢ (P + Q).rmatch x = true ↔ P.rmatch x = true ∨ Q.rmatch x = true
have cons : ∀ (head : α) (tail : List α)
  (ih : ∀ (P Q : RegularExpression α), (P + Q).rmatch tail = true ↔ P.rmatch tail = true ∨ Q.rmatch tail = true)
  (P Q : RegularExpression α),
  (P + Q).rmatch (head :: tail) = true ↔ P.rmatch (head :: tail) = true ∨ Q.rmatch (head :: tail) = true
Tactic: induction x generalizing P Q with
  | nil => simp only [rmatch, matchEpsilon, Bool.or_eq_true_iff]
  | cons _ _ ih =>
    rw [rmatch, deriv_add]
    exact ih _ _
Cleared hypotheses: P, Q, x
-- Lean 4 proof step from Mathlib.Computability.RegularExpressions (goal)
Goal:
α : Type u_1
inst : DecidableEq α
P Q : RegularExpression α
⊢ (P.matchEpsilon && Q.matchEpsilon) = true ↔
    ∃ (t : List α) (u : List α), [] = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
have nil : (P.matchEpsilon && Q.matchEpsilon) = true →
  ∃ (t : List α) (u : List α), [] = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
Tactic: constructor
-- Lean 4 proof step from Mathlib.Computability.RegularExpressions (goal)
Goal:
α : Type u_1
inst : DecidableEq α
P Q : RegularExpression α
nil :
  (P.matchEpsilon && Q.matchEpsilon) = true →
    ∃ (t : List α) (u : List α), [] = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
⊢ (P.matchEpsilon && Q.matchEpsilon) = true ↔
    ∃ (t : List α) (u : List α), [] = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
have nil₁ : (∃ (t : List α) (u : List α), [] = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true) →
  (P.matchEpsilon && Q.matchEpsilon) = true
Tactic: constructor
-- Lean 4 proof step from Mathlib.Computability.RegularExpressions (goal)
Goal:
α : Type u_1
inst : DecidableEq α
P Q : RegularExpression α
h : (P.matchEpsilon && Q.matchEpsilon) = true
⊢ ∃ (t : List α) (u : List α), [] = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
have nil : P.rmatch [] = true ∧ Q.rmatch [] = true
Tactic: refine ⟨[], [], rfl, ?_⟩
-- Lean 4 proof step from Mathlib.Computability.RegularExpressions (goal)
Goal:
α : Type u_1
inst : DecidableEq α
P Q : RegularExpression α
h : (P.matchEpsilon && Q.matchEpsilon) = true
⊢ P.matchEpsilon = true ∧ Q.matchEpsilon = true
have nil : ∀ (h : P.matchEpsilon = true ∧ Q.matchEpsilon = true), P.matchEpsilon = true ∧ Q.matchEpsilon = true
Tactic: rwa [Bool.and_eq_true_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Computability.RegularExpressions (hypothesis)
Goal:
α : 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
have h₃ : [] = HAppend.hAppend (α := List α) [] []
Tactic: obtain ⟨rfl, rfl⟩ := List.append_eq_nil_iff.1 h₁.symm
Cleared hypotheses: t, u, h₁, h₂
-- Lean 4 proof step from Mathlib.Computability.RegularExpressions (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
P Q : RegularExpression α
t u : List α
h₁ : [] = t ++ u
h₂ : P.rmatch t = true ∧ Q.rmatch u = true
h₃ : [] = HAppend.hAppend (α := List α) [] []
⊢ (P.matchEpsilon && Q.matchEpsilon) = true
have h₄ : P.rmatch [] = true ∧ Q.rmatch [] = true
Tactic: obtain ⟨rfl, rfl⟩ := List.append_eq_nil_iff.1 h₁.symm
Cleared hypotheses: t, u, h₁, h₂
-- Lean 4 proof step from Mathlib.Computability.RegularExpressions (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
P Q : RegularExpression α
h₁ : [] = HAppend.hAppend (α := List α) [] []
h₂ : P.rmatch [] = true ∧ Q.rmatch [] = true
⊢ (P.matchEpsilon && Q.matchEpsilon) = true
have h₃ : P.matchEpsilon = true ∧ Q.rmatch [] = true
Tactic: rw [rmatch] at h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Computability.RegularExpressions (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
P Q : RegularExpression α
h₁ : [] = HAppend.hAppend (α := List α) [] []
h₂ : P.matchEpsilon = true ∧ Q.rmatch [] = true
⊢ (P.matchEpsilon && Q.matchEpsilon) = true
have h₃ : P.matchEpsilon = true ∧ Q.matchEpsilon = true
Tactic: rw [rmatch] at h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Computability.RegularExpressions (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
P Q : RegularExpression α
h₁ : [] = HAppend.hAppend (α := List α) [] []
h₂ : P.rmatch [] = true ∧ Q.rmatch [] = true
⊢ (P.matchEpsilon && Q.matchEpsilon) = true
have h₃ : P.matchEpsilon = true ∧ Q.matchEpsilon = true
Tactic: repeat rw [rmatch] at h₂
Cleared hypotheses: h₂
-- 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 α
⊢ (P * Q).rmatch (a :: x) = true ↔ ∃ (t : List α) (u : List α), a :: x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
have cons : ((P * Q).deriv a).rmatch x = true ↔ ∃ (t : List α) (u : List α), a :: x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
Tactic: rw [rmatch]
-- 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 α
⊢ (if P.matchEpsilon = true then P.deriv a * Q + Q.deriv a else P.deriv a * Q).rmatch x = true ↔
    ∃ (t : List α) (u : List α), a :: x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
have pos : ∀ (hepsilon : P.matchEpsilon = true),
  (P.deriv a * Q + Q.deriv a).rmatch x = true ↔
    ∃ (t : List α) (u : List α), a :: x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
Tactic: split_ifs with hepsilon
-- 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 α
pos :
  ∀ (hepsilon : P.matchEpsilon = true),
    (P.deriv a * Q + Q.deriv a).rmatch x = true ↔
      ∃ (t : List α) (u : List α), a :: x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
⊢ (if P.matchEpsilon = true then P.deriv a * Q + Q.deriv a else P.deriv a * Q).rmatch x = true ↔
    ∃ (t : List α) (u : List α), a :: x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
have neg : ∀ (hepsilon : ¬P.matchEpsilon = true),
  (P.deriv a * Q).rmatch x = true ↔ ∃ (t : List α) (u : List α), a :: x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
Tactic: split_ifs with hepsilon
-- 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
⊢ (P.deriv a * Q + Q.deriv a).rmatch x = true ↔
    ∃ (t : List α) (u : List α), a :: x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
have pos : (∃ (t : List α) (u : List α), x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ Q.rmatch u = true) ∨
    (Q.deriv a).rmatch x = true ↔
  ∃ (t : List α) (u : List α), a :: x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
Tactic: rw [add_rmatch_iff, ih]
-- 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 : List α) (u : List α), x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ Q.rmatch u = true) ∨
      (Q.deriv a).rmatch x = true ↔
    ∃ (t : List α) (u : List α), a :: x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
have pos : (∃ (t : List α) (u : List α), x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ Q.rmatch u = true) ∨
    (Q.deriv a).rmatch x = true →
  ∃ (t : List α) (u : List α), a :: x = t ++ u ∧ P.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
pos :
  (∃ (t : List α) (u : List α), x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ Q.rmatch u = true) ∨
      (Q.deriv a).rmatch x = 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) ∨
      (Q.deriv a).rmatch x = true ↔
    ∃ (t : List α) (u : List α), a :: x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
have pos₁ : (∃ (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) ∨
    (Q.deriv a).rmatch x = 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 ∧ (P.deriv a).rmatch t = true ∧ Q.rmatch u = true
⊢ a :: x = a :: t ++ u ∧ P.rmatch (a :: t) = true ∧ Q.rmatch u = true
have tauto : x = t ++ u →
  (P.deriv a).rmatch t = true → Q.rmatch u = true → a :: x = a :: t ++ u ∧ P.rmatch (a :: t) = true ∧ Q.rmatch u = true
Tactic: tauto
Cleared hypotheses: h
-- 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 ∧ (P.deriv a).rmatch t = true ∧ Q.rmatch u = true
tauto tauto₁ :
  x = t ++ u →
    (P.deriv a).rmatch t = true →
      Q.rmatch u = true → a :: x = a :: t ++ u ∧ P.rmatch (a :: t) = true ∧ Q.rmatch u = true
⊢ a :: x = a :: t ++ u ∧ P.rmatch (a :: t) = true ∧ Q.rmatch u = true
have left : x = t ++ u → (P.deriv a).rmatch t = true → Q.rmatch u = true → a :: x = a :: t ++ u
Tactic: tauto
Cleared hypotheses: h
-- 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 ∧ (P.deriv a).rmatch t = true ∧ Q.rmatch u = true
tauto tauto₁ :
  x = t ++ u →
    (P.deriv a).rmatch t = true →
      Q.rmatch u = true → a :: x = a :: t ++ u ∧ P.rmatch (a :: t) = true ∧ Q.rmatch u = true
left : x = t ++ u → (P.deriv a).rmatch t = true → Q.rmatch u = true → a :: x = a :: t ++ u
⊢ a :: x = a :: t ++ u ∧ P.rmatch (a :: t) = true ∧ Q.rmatch u = true
have right : x = t ++ u → (P.deriv a).rmatch t = true → Q.rmatch u = true → P.rmatch (a :: t) = true
Tactic: tauto
Cleared hypotheses: h
-- 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 ∧ (P.deriv a).rmatch t = true ∧ Q.rmatch u = true
tauto tauto₁ :
  x = t ++ u →
    (P.deriv a).rmatch t = true →
      Q.rmatch u = true → a :: x = a :: t ++ u ∧ P.rmatch (a :: t) = true ∧ Q.rmatch u = true
left : x = t ++ u → (P.deriv a).rmatch t = true → Q.rmatch u = true → a :: x = a :: t ++ u
right : x = t ++ u → (P.deriv a).rmatch t = true → Q.rmatch u = true → P.rmatch (a :: t) = true
⊢ a :: x = a :: t ++ u ∧ P.rmatch (a :: t) = true ∧ Q.rmatch u = true
have right₁ : x = t ++ u → (P.deriv a).rmatch t = true → Q.rmatch u = true → Q.rmatch u = true
Tactic: tauto
Cleared hypotheses: h
-- 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) ∨
    (Q.deriv a).rmatch x = true
have pos : ∀ (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) ∨
    (Q.deriv a).rmatch x = 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
pos :
  ∀ (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) ∨
      (Q.deriv a).rmatch x = true
⊢ (∃ (t : List α) (u : List α), x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ Q.rmatch u = true) ∨
    (Q.deriv a).rmatch x = true
have pos₁ : ∀ (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) ∨
    (Q.deriv a).rmatch x = 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
u : List α
hQ : Q.rmatch u = true
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) ∨
    (Q.deriv a).rmatch x = true
have pos : (Q.deriv a).rmatch x = true
Tactic: right
-- 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
h : a :: x = [] ++ u
hP : P.rmatch [] = true
⊢ (Q.deriv a).rmatch x = true
have h₁ : a :: x = u
Tactic: rw [List.nil_append] at h
Cleared hypotheses: 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
h : a :: x = u
hP : P.rmatch [] = true
⊢ (Q.deriv a).rmatch x = true
have hQ₁ : Q.rmatch (a :: x) = true
Tactic: rw [← h] at hQ
Cleared hypotheses: hQ, 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 :: 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) ∨
    (Q.deriv a).rmatch x = true
have pos : ∃ (t : List α) (u : List α), x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ Q.rmatch u = true
Tactic: left
-- 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 pos : (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 α
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
⊢ (P.deriv a * Q).rmatch x = true ↔ ∃ (t : List α) (u : List α), a :: x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
have 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
Tactic: rw [ih]
-- 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 : 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 α), 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
Tactic: constructor