awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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'
⊢ (∃ (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' → ∃ 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
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'
⊢ (∃ (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 → ∃ (u : List α), x = w ++ u ∧ w ∈ 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
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'
⊢ (∃ (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 : List α) → w ∈ P.matches' → (w_1 : List α) → w_1 ∈ Q.matches' → w ++ w_1 = x → List α
Tactic: tauto
-- Lean 4 proof step from Mathlib.Computability.RegularExpressions (goal)
Goal:
α : Type u_1
inst : DecidableEq α
P : RegularExpression α
x : List α
⊢ P.rmatch x = true ↔ x ∈ P.matches'
have zero : ∀ (x : List α), rmatch zero x = true ↔ Membership.mem (γ := Language α) (matches' zero) x
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]
Cleared hypotheses: P, x
-- Lean 4 proof step from Mathlib.Computability.RegularExpressions (goal)
Goal:
α : Type u_1
inst : DecidableEq α
P : RegularExpression α
x : List α
zero :
  ∀ (x : List α),
    rmatch RegularExpression.zero x = true ↔ Membership.mem (γ := Language α) (matches' RegularExpression.zero) x
⊢ P.rmatch x = true ↔ x ∈ P.matches'
have epsilon : ∀ (x : List α), rmatch epsilon x = true ↔ Membership.mem (γ := Language α) (matches' epsilon) x
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]
Cleared hypotheses: P, x
-- Lean 4 proof step from Mathlib.Computability.RegularExpressions (goal)
Goal:
α : Type u_1
inst : DecidableEq α
P : RegularExpression α
x : List α
zero :
  ∀ (x : List α),
    rmatch RegularExpression.zero x = true ↔ Membership.mem (γ := Language α) (matches' RegularExpression.zero) x
epsilon :
  ∀ (x : List α),
    rmatch RegularExpression.epsilon x = true ↔ Membership.mem (γ := Language α) (matches' RegularExpression.epsilon) x
⊢ P.rmatch x = true ↔ x ∈ P.matches'
have char : ∀ (a : α) (x : List α), (char a).rmatch x = true ↔ x ∈ (char a).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]
Cleared hypotheses: P, x
-- Lean 4 proof step from Mathlib.Computability.RegularExpressions (goal)
Goal:
α : Type u_1
inst : DecidableEq α
P : RegularExpression α
x : List α
zero :
  ∀ (x : List α),
    rmatch RegularExpression.zero x = true ↔ Membership.mem (γ := Language α) (matches' RegularExpression.zero) x
epsilon :
  ∀ (x : List α),
    rmatch RegularExpression.epsilon x = true ↔ Membership.mem (γ := Language α) (matches' RegularExpression.epsilon) x
char : ∀ (a : α) (x : List α), (RegularExpression.char a).rmatch x = true ↔ x ∈ (RegularExpression.char a).matches'
⊢ P.rmatch x = true ↔ x ∈ P.matches'
have plus : ∀ (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'
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]
Cleared hypotheses: P, x
-- Lean 4 proof step from Mathlib.Computability.RegularExpressions (goal)
Goal:
α : Type u_1
inst : DecidableEq α
P : RegularExpression α
x : List α
zero :
  ∀ (x : List α),
    rmatch RegularExpression.zero x = true ↔ Membership.mem (γ := Language α) (matches' RegularExpression.zero) x
epsilon :
  ∀ (x : List α),
    rmatch RegularExpression.epsilon x = true ↔ Membership.mem (γ := Language α) (matches' RegularExpression.epsilon) x
char : ∀ (a : α) (x : List α), (RegularExpression.char a).rmatch x = true ↔ x ∈ (RegularExpression.char a).matches'
plus :
  ∀ (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'
⊢ P.rmatch x = true ↔ x ∈ P.matches'
have comp : ∀ (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: 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]
Cleared hypotheses: P, x
-- Lean 4 proof step from Mathlib.Computability.RegularExpressions (goal)
Goal:
α : Type u_1
inst : DecidableEq α
P : RegularExpression α
x : List α
zero :
  ∀ (x : List α),
    rmatch RegularExpression.zero x = true ↔ Membership.mem (γ := Language α) (matches' RegularExpression.zero) x
epsilon :
  ∀ (x : List α),
    rmatch RegularExpression.epsilon x = true ↔ Membership.mem (γ := Language α) (matches' RegularExpression.epsilon) x
char : ∀ (a : α) (x : List α), (RegularExpression.char a).rmatch x = true ↔ x ∈ (RegularExpression.char a).matches'
plus :
  ∀ (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'
comp :
  ∀ (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'
⊢ P.rmatch x = true ↔ x ∈ P.matches'
have star : ∀ (a : RegularExpression α) (ih : ∀ (x : List α), a.rmatch x = true ↔ x ∈ a.matches') (x : List α),
  a.star.rmatch x = true ↔ x ∈ a.star.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]
Cleared hypotheses: P, x
-- Lean 4 proof step from Mathlib.Computability.RegularExpressions (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
P : RegularExpression α
⊢ map f (HPow.hPow (β := ℕ) P 0) = HPow.hPow (β := ℕ) (map f P) 0
have unfold : (match (motive := RegularExpression α → RegularExpression β) HPow.hPow (β := ℕ) P 0 with
  | zero => 0
  | epsilon => 1
  | char a => char (f a)
  | R.plus S => map f R + map f S
  | R.comp S => map f R * map f S
  | R.star => (map f R).star) =
  HPow.hPow (α := RegularExpression β) (β := ℕ)
    (match (motive := RegularExpression α → RegularExpression β) P with
      | zero => 0
      | epsilon => 1
      | char a => char (f a)
      | R.plus S => map f R + map f S
      | R.comp S => map f R * map f S
      | R.star => (map f R).star :
      RegularExpression β)
    0
Tactic: unfold map
-- Lean 4 proof step from Mathlib.Computability.RegularExpressions (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
a : α
⊢ (map f (char a)).matches' = (Language.map f : (a : Language α) → Language β) (char a).matches'
have rw : (Language.map f : (a : Language α) → Language β) (char a).matches' = (map f (char a)).matches'
Tactic: rw [eq_comm]
-- Lean 4 proof step from Mathlib.Computability.StateTransition (goal)
Goal:
σ : Type u_1
f : σ → Option σ
a b c : σ
h : f a = f b
⊢ (∃ b_1 ∈ f b, ReflTransGen (fun (a b : σ) ↦ b ∈ f a) b_1 c) ↔ ∃ b ∈ f a, ReflTransGen (fun (a b : σ) ↦ b ∈ f a) b c
have rw : (∃ b_1 ∈ f b, ReflTransGen (fun (a b : σ) ↦ b ∈ f a) b_1 c) ↔ ∃ b_1 ∈ f b, ReflTransGen (fun (a b : σ) ↦ b ∈ f a) b_1 c
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Computability.StateTransition (goal)
Goal:
σ : Type u_1
f : σ → Option σ
a b c : σ
h₁ : Reaches₁ f a c
h₂ : b ∈ f a
⊢ Reaches f b c
have rcases : ∀ (b' : σ) (hab : b' ∈ f a) (hbc : ReflTransGen (fun (a b : σ) ↦ b ∈ f a) b' c), Reaches f b c
Tactic: rcases TransGen.head'_iff.1 h₁ with ⟨b', hab, hbc⟩
-- Lean 4 proof step from Mathlib.Computability.StateTransition (hypothesis)
Goal:
σ : Type u_1
f : σ → Option σ
a b c : σ
h₁ : Reaches₁ f a c
h₂ : b ∈ f a
b' : σ
hab : b' ∈ f a
hbc : ReflTransGen (fun (a b : σ) ↦ b ∈ f a) b' c
hab₁ : b ∈ f a
⊢ Reaches f b c
have hbc₁ : ReflTransGen (fun (a b : σ) ↦ b ∈ f a) b c
Tactic: cases Option.mem_unique hab h₂
Cleared hypotheses: b', hab, hbc
-- Lean 4 proof step from Mathlib.Computability.StateTransition (goal)
Goal:
σ : Type u_2
f : σ → Option σ
b : σ
C : σ → Sort u_1
a : σ
h : b ∈ eval f a
H : (a : σ) → b ∈ eval f a → ((a' : σ) → f a = some a' → C a') → C a
a' : σ
ha' : Membership.mem (γ := Part σ) (PFun.fix (fun (s : σ) ↦ Part.some ((f s).elim (Sum.inl s) Sum.inr)) a') b
h' : (a'' : σ) → Sum.inr a'' ∈ Part.some ((f a').elim (Sum.inl a') Sum.inr) → C a''
b' : σ
e : f a' = some b'
⊢ Sum.inr b' = (f a').elim (Sum.inl a') Sum.inr
have rw : Sum.inr b' = (some b').elim (Sum.inl a') Sum.inr
Tactic: rw [e]
-- Lean 4 proof step from Mathlib.Computability.StateTransition (goal)
Goal:
σ : Type u_1
f : σ → Option σ
a b : σ
⊢ b ∈ eval f a ↔ Reaches f a b ∧ f b = none
have refine_1 : ∀ (h : b ∈ eval f a), Reaches f a b ∧ f b = none
Tactic: refine ⟨fun h ↦ ?_, fun ⟨h₁, h₂⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Computability.StateTransition (goal)
Goal:
σ : Type u_1
f : σ → Option σ
a b : σ
refine_1 : ∀ (h : b ∈ eval f a), Reaches f a b ∧ f b = none
⊢ b ∈ eval f a ↔ Reaches f a b ∧ f b = none
have refine_2 : Reaches f a b ∧ f b = none → ∀ (h₁ : Reaches f a b) (h₂ : f b = none), b ∈ eval f a
Tactic: refine ⟨fun h ↦ ?_, fun ⟨h₁, h₂⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Computability.StateTransition (goal)
Goal:
σ : Type u_1
f : σ → Option σ
a b : σ
h : b ∈ eval f a
⊢ Reaches f a b ∧ f b = none
have refine_1 : ∀ (a : σ) (h : b ∈ eval f a) (IH : ∀ (a' : σ), f a = some a' → Reaches f a' b ∧ f b = none), Reaches f a b ∧ f b = none
Tactic: refine evalInduction h fun a h IH ↦ ?_
-- Lean 4 proof step from Mathlib.Computability.StateTransition (goal)
Goal:
σ : Type u_1
f : σ → Option σ
a_1 b : σ
h_1 : b ∈ eval f a_1
a : σ
h : b ∈ eval f a
IH : ∀ (a' : σ), f a = some a' → Reaches f a' b ∧ f b = none
⊢ Reaches f a b ∧ f b = none
have refine_1 : ∀ (e : f a = none), Reaches f a b ∧ f b = none
Tactic: rcases e : f a with - | a'
-- Lean 4 proof step from Mathlib.Computability.StateTransition (goal)
Goal:
σ : Type u_1
f : σ → Option σ
a_1 b : σ
h_1 : b ∈ eval f a_1
a : σ
h : b ∈ eval f a
IH : ∀ (a' : σ), f a = some a' → Reaches f a' b ∧ f b = none
refine_1 : ∀ (e : f a = none), Reaches f a b ∧ f b = none
⊢ Reaches f a b ∧ f b = none
have refine_1₁ : ∀ (a' : σ) (e : f a = some a'), Reaches f a b ∧ f b = none
Tactic: rcases e : f a with - | a'
-- Lean 4 proof step from Mathlib.Computability.StateTransition (goal)
Goal:
σ : Type u_1
f : σ → Option σ
a_1 b : σ
h_1 : b ∈ eval f a_1
a : σ
h : b ∈ eval f a
IH : ∀ (a' : σ), f a = some a' → Reaches f a' b ∧ f b = none
e : f a = none
⊢ Sum.inl a = (f a).elim (Sum.inl a) Sum.inr
have rw : Eq (α := σ ⊕ σ) (Sum.inl a) (Option.elim none (Sum.inl a) Sum.inr)
Tactic: rw [e]
-- Lean 4 proof step from Mathlib.Computability.StateTransition (goal)
Goal:
σ : Type u_1
f : σ → Option σ
a_1 b : σ
h_1 : b ∈ eval f a_1
a : σ
h : b ∈ eval f a
IH : ∀ (a' : σ), f a = some a' → Reaches f a' b ∧ f b = none
e : f a = none
⊢ Reaches f a b ∧ f b = none
have refine_1 : Reaches f a a ∧ f a = none
Tactic: rw [Part.mem_unique h
          (PFun.mem_fix_iff.2 <| Or.inl <| Part.mem_some_iff.2 <| by rw [e]; rfl)]
-- Lean 4 proof step from Mathlib.Computability.StateTransition (goal)
Goal:
σ : Type u_1
f : σ → Option σ
a_1 b : σ
h_1 : b ∈ eval f a_1
a : σ
h : b ∈ eval f a
IH : ∀ (a' : σ), f a = some a' → Reaches f a' b ∧ f b = none
a' : σ
e : f a = some a'
⊢ Reaches f a b ∧ f b = none
have refine_1 : ∀ (h : Sum.inl b ∈ Part.some ((f a).elim (Sum.inl a) Sum.inr)), Reaches f a b ∧ f b = none
Tactic: rcases PFun.mem_fix_iff.1 h with (h | ⟨_, h, _⟩)
-- Lean 4 proof step from Mathlib.Computability.StateTransition (goal)
Goal:
σ : Type u_1
f : σ → Option σ
a_1 b : σ
h_1 : b ∈ eval f a_1
a : σ
h : b ∈ eval f a
IH : ∀ (a' : σ), f a = some a' → Reaches f a' b ∧ f b = none
a' : σ
e : f a = some a'
refine_1 : ∀ (h : Sum.inl b ∈ Part.some ((f a).elim (Sum.inl a) Sum.inr)), Reaches f a b ∧ f b = none
⊢ Reaches f a b ∧ f b = none
have refine_1₁ : ∀ (w : σ) (h : Sum.inr w ∈ Part.some ((f a).elim (Sum.inl a) Sum.inr)),
  Membership.mem (γ := Part σ) (PFun.fix (fun (s : σ) ↦ Part.some ((f s).elim (Sum.inl s) Sum.inr)) w) b →
    Reaches f a b ∧ f b = none
Tactic: rcases PFun.mem_fix_iff.1 h with (h | ⟨_, h, _⟩)
-- Lean 4 proof step from Mathlib.Computability.StateTransition (hypothesis)
Goal:
σ : Type u_1
f : σ → Option σ
a_1 b : σ
h_1 : b ∈ eval f a_1
a : σ
h_2 : b ∈ eval f a
IH : ∀ (a' : σ), f a = some a' → Reaches f a' b ∧ f b = none
a' : σ
e : f a = some a'
h : Sum.inl b ∈ Part.some ((f a).elim (Sum.inl a) Sum.inr)
⊢ Reaches f a b ∧ f b = none
have h₁ : Sum.inl b ∈ Part.some ((some a').elim (Sum.inl a) Sum.inr)
Tactic: rw [e] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Computability.StateTransition (hypothesis)
Goal:
σ : Type u_1
f : σ → Option σ
a_1 b : σ
h_1 : b ∈ eval f a_1
a : σ
h_2 : b ∈ eval f a
IH : ∀ (a' : σ), f a = some a' → Reaches f a' b ∧ f b = none
a' : σ
e : f a = some a'
w : σ
h : Sum.inr w ∈ Part.some ((f a).elim (Sum.inl a) Sum.inr)
right : Membership.mem (γ := Part σ) (PFun.fix (fun (s : σ) ↦ Part.some ((f s).elim (Sum.inl s) Sum.inr)) w) b
⊢ Reaches f a b ∧ f b = none
have h₁ : Sum.inr w ∈ Part.some ((some a').elim (Sum.inl a) Sum.inr)
Tactic: rw [e] at h
Cleared hypotheses: h, right
-- Lean 4 proof step from Mathlib.Computability.StateTransition (hypothesis)
Goal:
σ : Type u_1
f : σ → Option σ
a_1 b : σ
h_1 : b ∈ eval f a_1
a : σ
h_2 : b ∈ eval f a
IH : ∀ (a' : σ), f a = some a' → Reaches f a' b ∧ f b = none
a' : σ
e : f a = some a'
w : σ
h : Sum.inr w ∈ Part.some ((some a').elim (Sum.inl a) Sum.inr)
right : Membership.mem (γ := Part σ) (PFun.fix (fun (s : σ) ↦ Part.some ((f s).elim (Sum.inl s) Sum.inr)) w) b
⊢ Reaches f a b ∧ f b = none
have h₁ : Sum.inr a' ∈ Part.some ((some a').elim (Sum.inl a) Sum.inr)
Tactic: cases Part.mem_some_iff.1 h
Cleared hypotheses: w, h, right
-- Lean 4 proof step from Mathlib.Computability.StateTransition (hypothesis)
Goal:
σ : Type u_1
f : σ → Option σ
a_1 b : σ
h_1 : b ∈ eval f a_1
a : σ
h_2 : b ∈ eval f a
IH : ∀ (a' : σ), f a = some a' → Reaches f a' b ∧ f b = none
a' : σ
e : f a = some a'
w : σ
h : Sum.inr w ∈ Part.some ((some a').elim (Sum.inl a) Sum.inr)
right : Membership.mem (γ := Part σ) (PFun.fix (fun (s : σ) ↦ Part.some ((f s).elim (Sum.inl s) Sum.inr)) w) b
h₁ : Sum.inr a' ∈ Part.some ((some a').elim (Sum.inl a) Sum.inr)
⊢ Reaches f a b ∧ f b = none
have right : Membership.mem (γ := Part σ) (PFun.fix (fun (s : σ) ↦ Part.some ((f s).elim (Sum.inl s) Sum.inr)) a') b
Tactic: cases Part.mem_some_iff.1 h
Cleared hypotheses: w, h, right