internlm/Lean-Github huggingface dataset:
Theorem: Language.concat_assoc
Proof state before:
case h.mp
α : Type u_1
X Y Z : Language α
x : Word α
⊢ x ∈ X ∘ₗ Y ∘ₗ Z → x ∈ X ∘ₗ (Y ∘ₗ Z)

case h.mpr
α : Type u_1
X Y Z : Language α
x : Word α
⊢ x ∈ X ∘ₗ (Y ∘ₗ Z) → x ∈ X ∘ₗ Y ∘ₗ Z
Tactic:
. intro
  | ⟨u, v, ⟨u1, u2, pu1, pu2, pu⟩, pv, px⟩ =>
    rw [pu, Word.monoid.mul_assoc u1 u2 v] at px
    exact ⟨ u1, u2 * v, pu1, ⟨u2, v, pu2, pv, rfl⟩, px ⟩
Proof state after:
case h.mpr
α : Type u_1
X Y Z : Language α
x : Word α
⊢ x ∈ X ∘ₗ (Y ∘ₗ Z) → x ∈ X ∘ₗ Y ∘ₗ Z
Theorem: Language.concat_assoc
Proof state before:
case h.mpr
α : Type u_1
X Y Z : Language α
x : Word α
⊢ x ∈ X ∘ₗ (Y ∘ₗ Z) → x ∈ X ∘ₗ Y ∘ₗ Z
Tactic:
. intro
  | ⟨u, v, pu, ⟨v1, v2, pv1, pv2, pv⟩, px⟩ =>
    rw [pv, <- Word.monoid.mul_assoc u v1 v2] at px
    exact ⟨ u * v1, v2, ⟨u, v1, pu, pv1, rfl⟩, pv2, px ⟩
Proof state after:
no goals
Theorem: Language.concat_assoc
Proof state before:
case h.mp
α : Type u_1
X Y Z : Language α
x : Word α
⊢ x ∈ X ∘ₗ Y ∘ₗ Z → x ∈ X ∘ₗ (Y ∘ₗ Z)
Tactic:
intro
| ⟨u, v, ⟨u1, u2, pu1, pu2, pu⟩, pv, px⟩ =>
  rw [pu, Word.monoid.mul_assoc u1 u2 v] at px
  exact ⟨ u1, u2 * v, pu1, ⟨u2, v, pu2, pv, rfl⟩, px ⟩
Proof state after:
no goals
Theorem: Language.concat_assoc
Proof state before:
α : Type u_1
X Y Z : Language α
x : Word α
x✝ : x ∈ X ∘ₗ Y ∘ₗ Z
u v u1 u2 : Word α
pu1 : u1 ∈ X
pu2 : u2 ∈ Y
pu : u = u1 * u2
pv : v ∈ Z
px : x = u * v
⊢ x ∈ X ∘ₗ (Y ∘ₗ Z)
Tactic:
rw [pu, Word.monoid.mul_assoc u1 u2 v] at px
Proof state after:
α : Type u_1
X Y Z : Language α
x : Word α
x✝ : x ∈ X ∘ₗ Y ∘ₗ Z
u v u1 u2 : Word α
pu1 : u1 ∈ X
pu2 : u2 ∈ Y
pu : u = u1 * u2
pv : v ∈ Z
px : x = u1 * (u2 * v)
⊢ x ∈ X ∘ₗ (Y ∘ₗ Z)
Theorem: Language.concat_assoc
Proof state before:
α : Type u_1
X Y Z : Language α
x : Word α
x✝ : x ∈ X ∘ₗ Y ∘ₗ Z
u v u1 u2 : Word α
pu1 : u1 ∈ X
pu2 : u2 ∈ Y
pu : u = u1 * u2
pv : v ∈ Z
px : x = u1 * (u2 * v)
⊢ x ∈ X ∘ₗ (Y ∘ₗ Z)
Tactic:
exact ⟨ u1, u2 * v, pu1, ⟨u2, v, pu2, pv, rfl⟩, px ⟩
Proof state after:
no goals
Theorem: Language.concat_assoc
Proof state before:
case h.mpr
α : Type u_1
X Y Z : Language α
x : Word α
⊢ x ∈ X ∘ₗ (Y ∘ₗ Z) → x ∈ X ∘ₗ Y ∘ₗ Z
Tactic:
intro
| ⟨u, v, pu, ⟨v1, v2, pv1, pv2, pv⟩, px⟩ =>
  rw [pv, <- Word.monoid.mul_assoc u v1 v2] at px
  exact ⟨ u * v1, v2, ⟨u, v1, pu, pv1, rfl⟩, pv2, px ⟩
Proof state after:
no goals
Theorem: Language.concat_assoc
Proof state before:
α : Type u_1
X Y Z : Language α
x : Word α
x✝ : x ∈ X ∘ₗ (Y ∘ₗ Z)
u v : Word α
pu : u ∈ X
v1 v2 : Word α
pv1 : v1 ∈ Y
pv2 : v2 ∈ Z
pv : v = v1 * v2
px : x = u * v
⊢ x ∈ X ∘ₗ Y ∘ₗ Z
Tactic:
rw [pv, <- Word.monoid.mul_assoc u v1 v2] at px
Proof state after:
α : Type u_1
X Y Z : Language α
x : Word α
x✝ : x ∈ X ∘ₗ (Y ∘ₗ Z)
u v : Word α
pu : u ∈ X
v1 v2 : Word α
pv1 : v1 ∈ Y
pv2 : v2 ∈ Z
pv : v = v1 * v2
px : x = u * v1 * v2
⊢ x ∈ X ∘ₗ Y ∘ₗ Z
Theorem: Language.concat_assoc
Proof state before:
α : Type u_1
X Y Z : Language α
x : Word α
x✝ : x ∈ X ∘ₗ (Y ∘ₗ Z)
u v : Word α
pu : u ∈ X
v1 v2 : Word α
pv1 : v1 ∈ Y
pv2 : v2 ∈ Z
pv : v = v1 * v2
px : x = u * v1 * v2
⊢ x ∈ X ∘ₗ Y ∘ₗ Z
Tactic:
exact ⟨ u * v1, v2, ⟨u, v1, pu, pv1, rfl⟩, pv2, px ⟩
Proof state after:
no goals
Theorem: Language.mul_eps
Proof state before:
α : Type u_1
L : Language α
⊢ L ∘ₗ epsilon = L
Tactic:
apply funext
Proof state after:
case h
α : Type u_1
L : Language α
⊢ ∀ (x : Word α), (L ∘ₗ epsilon) x = L x
Theorem: Language.mul_eps
Proof state before:
case h
α : Type u_1
L : Language α
⊢ ∀ (x : Word α), (L ∘ₗ epsilon) x = L x
Tactic:
intro w
Proof state after:
case h
α : Type u_1
L : Language α
w : Word α
⊢ (L ∘ₗ epsilon) w = L w
Theorem: Language.mul_eps
Proof state before:
case h
α : Type u_1
L : Language α
w : Word α
⊢ (L ∘ₗ epsilon) w = L w
Tactic:
apply propext
Proof state after:
case h.a
α : Type u_1
L : Language α
w : Word α
⊢ (L ∘ₗ epsilon) w ↔ L w
Theorem: Language.mul_eps
Proof state before:
case h.a
α : Type u_1
L : Language α
w : Word α
⊢ (L ∘ₗ epsilon) w ↔ L w
Tactic:
constructor
Proof state after:
case h.a.mp
α : Type u_1
L : Language α
w : Word α
⊢ (L ∘ₗ epsilon) w → L w

case h.a.mpr
α : Type u_1
L : Language α
w : Word α
⊢ L w → (L ∘ₗ epsilon) w
Theorem: Language.mul_eps
Proof state before:
case h.a.mp
α : Type u_1
L : Language α
w : Word α
⊢ (L ∘ₗ epsilon) w → L w

case h.a.mpr
α : Type u_1
L : Language α
w : Word α
⊢ L w → (L ∘ₗ epsilon) w
Tactic:
. rw [Language.concat]
  intro ⟨u,v, h1, h2, h3⟩
  simp [Language.epsilon, Membership.mem] at h2
  simp [h3, h2, Word.epsilon]
  exact h1
Proof state after:
case h.a.mpr
α : Type u_1
L : Language α
w : Word α
⊢ L w → (L ∘ₗ epsilon) w
Theorem: Language.mul_eps
Proof state before:
case h.a.mpr
α : Type u_1
L : Language α
w : Word α
⊢ L w → (L ∘ₗ epsilon) w
Tactic:
. intro h ; simp [Language.concat]
  exists w ; simp [Membership.mem, h]
  simp [Language.epsilon] ; rfl
Proof state after:
no goals
Theorem: Language.mul_eps
Proof state before:
case h.a.mp
α : Type u_1
L : Language α
w : Word α
⊢ (L ∘ₗ epsilon) w → L w
Tactic:
rw [Language.concat]
Proof state after:
case h.a.mp
α : Type u_1
L : Language α
w : Word α
⊢ (∃ u v, u ∈ L ∧ v ∈ epsilon ∧ w = u * v) → L w
Theorem: Language.mul_eps
Proof state before:
case h.a.mp
α : Type u_1
L : Language α
w : Word α
⊢ (∃ u v, u ∈ L ∧ v ∈ epsilon ∧ w = u * v) → L w
Tactic:
intro ⟨u,v, h1, h2, h3⟩
Proof state after:
case h.a.mp
α : Type u_1
L : Language α
w u v : Word α
h1 : u ∈ L
h2 : v ∈ epsilon
h3 : w = u * v
⊢ L w
Theorem: Language.mul_eps
Proof state before:
case h.a.mp
α : Type u_1
L : Language α
w u v : Word α
h1 : u ∈ L
h2 : v ∈ epsilon
h3 : w = u * v
⊢ L w
Tactic:
simp [Language.epsilon, Membership.mem] at h2
Proof state after:
case h.a.mp
α : Type u_1
L : Language α
w u v : Word α
h1 : u ∈ L
h2 : v = ε
h3 : w = u * v
⊢ L w
Theorem: Language.mul_eps
Proof state before:
case h.a.mp
α : Type u_1
L : Language α
w u v : Word α
h1 : u ∈ L
h2 : v = ε
h3 : w = u * v
⊢ L w
Tactic:
simp [h3, h2, Word.epsilon]
Proof state after:
case h.a.mp
α : Type u_1
L : Language α
w u v : Word α
h1 : u ∈ L
h2 : v = ε
h3 : w = u * v
⊢ L u
Theorem: Language.mul_eps
Proof state before:
case h.a.mp
α : Type u_1
L : Language α
w u v : Word α
h1 : u ∈ L
h2 : v = ε
h3 : w = u * v
⊢ L u
Tactic:
exact h1
Proof state after:
no goals
Theorem: Language.mul_eps
Proof state before:
case h.a.mpr
α : Type u_1
L : Language α
w : Word α
⊢ L w → (L ∘ₗ epsilon) w
Tactic:
intro h
Proof state after:
case h.a.mpr
α : Type u_1
L : Language α
w : Word α
h : L w
⊢ (L ∘ₗ epsilon) w
Theorem: Language.mul_eps
Proof state before:
case h.a.mpr
α : Type u_1
L : Language α
w : Word α
h : L w
⊢ (L ∘ₗ epsilon) w
Tactic:
simp [Language.concat]
Proof state after:
case h.a.mpr
α : Type u_1
L : Language α
w : Word α
h : L w
⊢ ∃ u ∈ L, ∃ x ∈ epsilon, w = u * x
Theorem: Language.mul_eps
Proof state before:
case h.a.mpr
α : Type u_1
L : Language α
w : Word α
h : L w
⊢ ∃ u ∈ L, ∃ x ∈ epsilon, w = u * x
Tactic:
exists w
Proof state after:
case h.a.mpr
α : Type u_1
L : Language α
w : Word α
h : L w
⊢ w ∈ L ∧ ∃ x ∈ epsilon, w = w * x
Theorem: Language.mul_eps
Proof state before:
case h.a.mpr
α : Type u_1
L : Language α
w : Word α
h : L w
⊢ w ∈ L ∧ ∃ x ∈ epsilon, w = w * x
Tactic:
simp [Membership.mem, h]
Proof state after:
case h.a.mpr
α : Type u_1
L : Language α
w : Word α
h : L w
⊢ epsilon 1
Theorem: Language.mul_eps
Proof state before:
case h.a.mpr
α : Type u_1
L : Language α
w : Word α
h : L w
⊢ epsilon 1
Tactic:
simp [Language.epsilon]
Proof state after:
case h.a.mpr
α : Type u_1
L : Language α
w : Word α
h : L w
⊢ 1 = ε
Theorem: Language.mul_eps
Proof state before:
case h.a.mpr
α : Type u_1
L : Language α
w : Word α
h : L w
⊢ 1 = ε
Tactic:
rfl
Proof state after:
no goals
Theorem: Language.eps_mul
Proof state before:
α : Type u_1
L : Language α
⊢ epsilon ∘ₗ L = L
Tactic:
apply funext
Proof state after:
case h
α : Type u_1
L : Language α
⊢ ∀ (x : Word α), (epsilon ∘ₗ L) x = L x
Theorem: Language.eps_mul
Proof state before:
case h
α : Type u_1
L : Language α
⊢ ∀ (x : Word α), (epsilon ∘ₗ L) x = L x
Tactic:
intro w
Proof state after:
case h
α : Type u_1
L : Language α
w : Word α
⊢ (epsilon ∘ₗ L) w = L w
Theorem: Language.eps_mul
Proof state before:
case h
α : Type u_1
L : Language α
w : Word α
⊢ (epsilon ∘ₗ L) w = L w
Tactic:
apply propext
Proof state after:
case h.a
α : Type u_1
L : Language α
w : Word α
⊢ (epsilon ∘ₗ L) w ↔ L w
Theorem: Language.eps_mul
Proof state before:
case h.a
α : Type u_1
L : Language α
w : Word α
⊢ (epsilon ∘ₗ L) w ↔ L w
Tactic:
constructor
Proof state after:
case h.a.mp
α : Type u_1
L : Language α
w : Word α
⊢ (epsilon ∘ₗ L) w → L w

case h.a.mpr
α : Type u_1
L : Language α
w : Word α
⊢ L w → (epsilon ∘ₗ L) w
Theorem: Language.eps_mul
Proof state before:
case h.a.mp
α : Type u_1
L : Language α
w : Word α
⊢ (epsilon ∘ₗ L) w → L w

case h.a.mpr
α : Type u_1
L : Language α
w : Word α
⊢ L w → (epsilon ∘ₗ L) w
Tactic:
. rw [Language.concat]
  intro ⟨u,v, h1, h2, h3⟩
  simp [Language.epsilon, Membership.mem] at h1
  simp [h3, h1, Word.epsilon]
  exact h2
Proof state after:
case h.a.mpr
α : Type u_1
L : Language α
w : Word α
⊢ L w → (epsilon ∘ₗ L) w
Theorem: Language.eps_mul
Proof state before:
case h.a.mpr
α : Type u_1
L : Language α
w : Word α
⊢ L w → (epsilon ∘ₗ L) w
Tactic:
. intro h
  simp [Language.concat]
  exists ε ; simp [Language.epsilon, Membership.mem]
  assumption
Proof state after:
no goals
Theorem: Language.eps_mul
Proof state before:
case h.a.mp
α : Type u_1
L : Language α
w : Word α
⊢ (epsilon ∘ₗ L) w → L w
Tactic:
rw [Language.concat]
Proof state after:
case h.a.mp
α : Type u_1
L : Language α
w : Word α
⊢ (∃ u v, u ∈ epsilon ∧ v ∈ L ∧ w = u * v) → L w
Theorem: Language.eps_mul
Proof state before:
case h.a.mp
α : Type u_1
L : Language α
w : Word α
⊢ (∃ u v, u ∈ epsilon ∧ v ∈ L ∧ w = u * v) → L w
Tactic:
intro ⟨u,v, h1, h2, h3⟩
Proof state after:
case h.a.mp
α : Type u_1
L : Language α
w u v : Word α
h1 : u ∈ epsilon
h2 : v ∈ L
h3 : w = u * v
⊢ L w
Theorem: Language.eps_mul
Proof state before:
case h.a.mp
α : Type u_1
L : Language α
w u v : Word α
h1 : u ∈ epsilon
h2 : v ∈ L
h3 : w = u * v
⊢ L w
Tactic:
simp [Language.epsilon, Membership.mem] at h1
Proof state after:
case h.a.mp
α : Type u_1
L : Language α
w u v : Word α
h1 : u = ε
h2 : v ∈ L
h3 : w = u * v
⊢ L w
Theorem: Language.eps_mul
Proof state before:
case h.a.mp
α : Type u_1
L : Language α
w u v : Word α
h1 : u = ε
h2 : v ∈ L
h3 : w = u * v
⊢ L w
Tactic:
simp [h3, h1, Word.epsilon]
Proof state after:
case h.a.mp
α : Type u_1
L : Language α
w u v : Word α
h1 : u = ε
h2 : v ∈ L
h3 : w = u * v
⊢ L v
Theorem: Language.eps_mul
Proof state before:
case h.a.mp
α : Type u_1
L : Language α
w u v : Word α
h1 : u = ε
h2 : v ∈ L
h3 : w = u * v
⊢ L v
Tactic:
exact h2
Proof state after:
no goals
Theorem: Language.eps_mul
Proof state before:
case h.a.mpr
α : Type u_1
L : Language α
w : Word α
⊢ L w → (epsilon ∘ₗ L) w
Tactic:
intro h
Proof state after:
case h.a.mpr
α : Type u_1
L : Language α
w : Word α
h : L w
⊢ (epsilon ∘ₗ L) w
Theorem: Language.eps_mul
Proof state before:
case h.a.mpr
α : Type u_1
L : Language α
w : Word α
h : L w
⊢ (epsilon ∘ₗ L) w
Tactic:
simp [Language.concat]
Proof state after:
case h.a.mpr
α : Type u_1
L : Language α
w : Word α
h : L w
⊢ ∃ u ∈ epsilon, ∃ x ∈ L, w = u * x
Theorem: Language.eps_mul
Proof state before:
case h.a.mpr
α : Type u_1
L : Language α
w : Word α
h : L w
⊢ ∃ u ∈ epsilon, ∃ x ∈ L, w = u * x
Tactic:
exists ε
Proof state after:
case h.a.mpr
α : Type u_1
L : Language α
w : Word α
h : L w
⊢ ε ∈ epsilon ∧ ∃ x ∈ L, w = ε * x
Theorem: Language.eps_mul
Proof state before:
case h.a.mpr
α : Type u_1
L : Language α
w : Word α
h : L w
⊢ ε ∈ epsilon ∧ ∃ x ∈ L, w = ε * x
Tactic:
simp [Language.epsilon, Membership.mem]
Proof state after:
case h.a.mpr
α : Type u_1
L : Language α
w : Word α
h : L w
⊢ L w
Theorem: Language.eps_mul
Proof state before:
case h.a.mpr
α : Type u_1
L : Language α
w : Word α
h : L w
⊢ L w
Tactic:
assumption
Proof state after:
no goals
Theorem: Language.mul_empty
Proof state before:
α : Type u_1
L : Language α
⊢ L ∘ₗ ∅ = ∅
Tactic:
apply Set.ext
Proof state after:
case h
α : Type u_1
L : Language α
⊢ ∀ (x : Word α), x ∈ L ∘ₗ ∅ ↔ x ∈ ∅
Theorem: Language.mul_empty
Proof state before:
case h
α : Type u_1
L : Language α
⊢ ∀ (x : Word α), x ∈ L ∘ₗ ∅ ↔ x ∈ ∅
Tactic:
intro w
Proof state after:
case h
α : Type u_1
L : Language α
w : Word α
⊢ w ∈ L ∘ₗ ∅ ↔ w ∈ ∅
Theorem: Language.mul_empty
Proof state before:
case h
α : Type u_1
L : Language α
w : Word α
⊢ w ∈ L ∘ₗ ∅ ↔ w ∈ ∅
Tactic:
constructor
Proof state after:
case h.mp
α : Type u_1
L : Language α
w : Word α
⊢ w ∈ L ∘ₗ ∅ → w ∈ ∅

case h.mpr
α : Type u_1
L : Language α
w : Word α
⊢ w ∈ ∅ → w ∈ L ∘ₗ ∅
Theorem: Language.mul_empty
Proof state before:
case h.mp
α : Type u_1
L : Language α
w : Word α
⊢ w ∈ L ∘ₗ ∅ → w ∈ ∅

case h.mpr
α : Type u_1
L : Language α
w : Word α
⊢ w ∈ ∅ → w ∈ L ∘ₗ ∅
Tactic:
. intro n
  match n with
  | ⟨_,_,_,h,_⟩ =>
    apply False.elim h
Proof state after:
case h.mpr
α : Type u_1
L : Language α
w : Word α
⊢ w ∈ ∅ → w ∈ L ∘ₗ ∅
Theorem: Language.mul_empty
Proof state before:
case h.mpr
α : Type u_1
L : Language α
w : Word α
⊢ w ∈ ∅ → w ∈ L ∘ₗ ∅
Tactic:
. intro n
  apply False.elim n
Proof state after:
no goals
Theorem: Language.mul_empty
Proof state before:
case h.mp
α : Type u_1
L : Language α
w : Word α
⊢ w ∈ L ∘ₗ ∅ → w ∈ ∅
Tactic:
intro n
Proof state after:
case h.mp
α : Type u_1
L : Language α
w : Word α
n : w ∈ L ∘ₗ ∅
⊢ w ∈ ∅
Theorem: Language.mul_empty
Proof state before:
case h.mp
α : Type u_1
L : Language α
w : Word α
n : w ∈ L ∘ₗ ∅
⊢ w ∈ ∅
Tactic:
match n with
| ⟨_,_,_,h,_⟩ =>
  apply False.elim h
Proof state after:
no goals
Theorem: Language.mul_empty
Proof state before:
α : Type u_1
L : Language α
w : Word α
n : w ∈ L ∘ₗ ∅
w✝¹ w✝ : Word α
left✝ : w✝¹ ∈ L
h : w✝ ∈ ∅
right✝ : w = w✝¹ * w✝
⊢ w ∈ ∅
Tactic:
apply False.elim h
Proof state after:
no goals
Theorem: Language.mul_empty
Proof state before:
case h.mpr
α : Type u_1
L : Language α
w : Word α
⊢ w ∈ ∅ → w ∈ L ∘ₗ ∅
Tactic:
intro n
Proof state after:
case h.mpr
α : Type u_1
L : Language α
w : Word α
n : w ∈ ∅
⊢ w ∈ L ∘ₗ ∅
Theorem: Language.mul_empty
Proof state before:
case h.mpr
α : Type u_1
L : Language α
w : Word α
n : w ∈ ∅
⊢ w ∈ L ∘ₗ ∅
Tactic:
apply False.elim n
Proof state after:
no goals
Theorem: Language.empty_mul
Proof state before:
α : Type u_1
L : Language α
⊢ ∅ ∘ₗ L = ∅
Tactic:
apply Set.ext
Proof state after:
case h
α : Type u_1
L : Language α
⊢ ∀ (x : Word α), x ∈ ∅ ∘ₗ L ↔ x ∈ ∅
Theorem: Language.empty_mul
Proof state before:
case h
α : Type u_1
L : Language α
⊢ ∀ (x : Word α), x ∈ ∅ ∘ₗ L ↔ x ∈ ∅
Tactic:
intro w
Proof state after:
case h
α : Type u_1
L : Language α
w : Word α
⊢ w ∈ ∅ ∘ₗ L ↔ w ∈ ∅
Theorem: Language.empty_mul
Proof state before:
case h
α : Type u_1
L : Language α
w : Word α
⊢ w ∈ ∅ ∘ₗ L ↔ w ∈ ∅
Tactic:
constructor
Proof state after:
case h.mp
α : Type u_1
L : Language α
w : Word α
⊢ w ∈ ∅ ∘ₗ L → w ∈ ∅

case h.mpr
α : Type u_1
L : Language α
w : Word α
⊢ w ∈ ∅ → w ∈ ∅ ∘ₗ L
Theorem: Language.empty_mul
Proof state before:
case h.mp
α : Type u_1
L : Language α
w : Word α
⊢ w ∈ ∅ ∘ₗ L → w ∈ ∅

case h.mpr
α : Type u_1
L : Language α
w : Word α
⊢ w ∈ ∅ → w ∈ ∅ ∘ₗ L
Tactic:
. intro n
  match n with
  | ⟨_,_,h,_,_⟩ =>
    apply False.elim h
Proof state after:
case h.mpr
α : Type u_1
L : Language α
w : Word α
⊢ w ∈ ∅ → w ∈ ∅ ∘ₗ L
Theorem: Language.empty_mul
Proof state before:
case h.mpr
α : Type u_1
L : Language α
w : Word α
⊢ w ∈ ∅ → w ∈ ∅ ∘ₗ L
Tactic:
. intro n
  apply False.elim n
Proof state after:
no goals
Theorem: Language.empty_mul
Proof state before:
case h.mp
α : Type u_1
L : Language α
w : Word α
⊢ w ∈ ∅ ∘ₗ L → w ∈ ∅
Tactic:
intro n
Proof state after:
case h.mp
α : Type u_1
L : Language α
w : Word α
n : w ∈ ∅ ∘ₗ L
⊢ w ∈ ∅
Theorem: Language.empty_mul
Proof state before:
case h.mp
α : Type u_1
L : Language α
w : Word α
n : w ∈ ∅ ∘ₗ L
⊢ w ∈ ∅
Tactic:
match n with
| ⟨_,_,h,_,_⟩ =>
  apply False.elim h
Proof state after:
no goals
Theorem: Language.empty_mul
Proof state before:
α : Type u_1
L : Language α
w : Word α
n : w ∈ ∅ ∘ₗ L
w✝¹ w✝ : Word α
h : w✝¹ ∈ ∅
left✝ : w✝ ∈ L
right✝ : w = w✝¹ * w✝
⊢ w ∈ ∅
Tactic:
apply False.elim h
Proof state after:
no goals
Theorem: Language.empty_mul
Proof state before:
case h.mpr
α : Type u_1
L : Language α
w : Word α
⊢ w ∈ ∅ → w ∈ ∅ ∘ₗ L
Tactic:
intro n
Proof state after:
case h.mpr
α : Type u_1
L : Language α
w : Word α
n : w ∈ ∅
⊢ w ∈ ∅ ∘ₗ L
Theorem: Language.empty_mul
Proof state before:
case h.mpr
α : Type u_1
L : Language α
w : Word α
n : w ∈ ∅
⊢ w ∈ ∅ ∘ₗ L
Tactic:
apply False.elim n
Proof state after:
no goals
Theorem: Language.concat_dist_union_r
Proof state before:
α : Type u_1
L1 L2 L3 : Language α
⊢ (L1 ∪ L2) ∘ₗ L3 = L1 ∘ₗ L3 ∪ L2 ∘ₗ L3
Tactic:
apply Set.ext
Proof state after:
case h
α : Type u_1
L1 L2 L3 : Language α
⊢ ∀ (x : Word α), x ∈ (L1 ∪ L2) ∘ₗ L3 ↔ x ∈ L1 ∘ₗ L3 ∪ L2 ∘ₗ L3
Theorem: Language.concat_dist_union_r
Proof state before:
case h
α : Type u_1
L1 L2 L3 : Language α
⊢ ∀ (x : Word α), x ∈ (L1 ∪ L2) ∘ₗ L3 ↔ x ∈ L1 ∘ₗ L3 ∪ L2 ∘ₗ L3
Tactic:
intro w
Proof state after:
case h
α : Type u_1
L1 L2 L3 : Language α
w : Word α
⊢ w ∈ (L1 ∪ L2) ∘ₗ L3 ↔ w ∈ L1 ∘ₗ L3 ∪ L2 ∘ₗ L3
Theorem: Language.concat_dist_union_r
Proof state before:
case h
α : Type u_1
L1 L2 L3 : Language α
w : Word α
⊢ w ∈ (L1 ∪ L2) ∘ₗ L3 ↔ w ∈ L1 ∘ₗ L3 ∪ L2 ∘ₗ L3
Tactic:
constructor
Proof state after:
case h.mp
α : Type u_1
L1 L2 L3 : Language α
w : Word α
⊢ w ∈ (L1 ∪ L2) ∘ₗ L3 → w ∈ L1 ∘ₗ L3 ∪ L2 ∘ₗ L3

case h.mpr
α : Type u_1
L1 L2 L3 : Language α
w : Word α
⊢ w ∈ L1 ∘ₗ L3 ∪ L2 ∘ₗ L3 → w ∈ (L1 ∪ L2) ∘ₗ L3
Theorem: Language.concat_dist_union_r
Proof state before:
case h.mp
α : Type u_1
L1 L2 L3 : Language α
w : Word α
⊢ w ∈ (L1 ∪ L2) ∘ₗ L3 → w ∈ L1 ∘ₗ L3 ∪ L2 ∘ₗ L3

case h.mpr
α : Type u_1
L1 L2 L3 : Language α
w : Word α
⊢ w ∈ L1 ∘ₗ L3 ∪ L2 ∘ₗ L3 → w ∈ (L1 ∪ L2) ∘ₗ L3
Tactic:
. intro
  | ⟨u,v,h1,h2,h3⟩ =>
    cases h1 with
    | inl hl => apply Or.inl; exists u; exists v
    | inr hr => apply Or.inr; exists u; exists v
Proof state after:
case h.mpr
α : Type u_1
L1 L2 L3 : Language α
w : Word α
⊢ w ∈ L1 ∘ₗ L3 ∪ L2 ∘ₗ L3 → w ∈ (L1 ∪ L2) ∘ₗ L3
Theorem: Language.concat_dist_union_r
Proof state before:
case h.mpr
α : Type u_1
L1 L2 L3 : Language α
w : Word α
⊢ w ∈ L1 ∘ₗ L3 ∪ L2 ∘ₗ L3 → w ∈ (L1 ∪ L2) ∘ₗ L3
Tactic:
. intro
  | Or.inl hl => cases hl with | intro u pu => cases pu with | intro v pv =>
      match pv with
      | ⟨h1, h2, h3⟩ => exists u, v; exact ⟨Or.inl h1, h2, h3⟩
  | Or.inr hr => cases hr with | intro u pu => cases pu with | intro v pv =>
      match pv with
      | ⟨h1, h2, h3⟩ => exists u, v; exact ⟨Or.inr h1, h2, h3⟩
Proof state after:
no goals
Theorem: Language.concat_dist_union_r
Proof state before:
case h.mp
α : Type u_1
L1 L2 L3 : Language α
w : Word α
⊢ w ∈ (L1 ∪ L2) ∘ₗ L3 → w ∈ L1 ∘ₗ L3 ∪ L2 ∘ₗ L3
Tactic:
intro
| ⟨u,v,h1,h2,h3⟩ =>
  cases h1 with
  | inl hl => apply Or.inl; exists u; exists v
  | inr hr => apply Or.inr; exists u; exists v
Proof state after:
no goals
Theorem: Language.concat_dist_union_r
Proof state before:
α : Type u_1
L1 L2 L3 : Language α
w : Word α
x✝ : w ∈ (L1 ∪ L2) ∘ₗ L3
u v : Word α
h1 : u ∈ L1 ∪ L2
h2 : v ∈ L3
h3 : w = u * v
⊢ w ∈ L1 ∘ₗ L3 ∪ L2 ∘ₗ L3
Tactic:
cases h1 with
| inl hl => apply Or.inl; exists u; exists v
| inr hr => apply Or.inr; exists u; exists v
Proof state after:
no goals
Theorem: Language.concat_dist_union_r
Proof state before:
case inl
α : Type u_1
L1 L2 L3 : Language α
w : Word α
x✝ : w ∈ (L1 ∪ L2) ∘ₗ L3
u v : Word α
h2 : v ∈ L3
h3 : w = u * v
hl : u ∈ L1
⊢ w ∈ L1 ∘ₗ L3 ∪ L2 ∘ₗ L3
Tactic:
apply Or.inl
Proof state after:
case inl.h
α : Type u_1
L1 L2 L3 : Language α
w : Word α
x✝ : w ∈ (L1 ∪ L2) ∘ₗ L3
u v : Word α
h2 : v ∈ L3
h3 : w = u * v
hl : u ∈ L1
⊢ w ∈ L1 ∘ₗ L3
Theorem: Language.concat_dist_union_r
Proof state before:
case inl.h
α : Type u_1
L1 L2 L3 : Language α
w : Word α
x✝ : w ∈ (L1 ∪ L2) ∘ₗ L3
u v : Word α
h2 : v ∈ L3
h3 : w = u * v
hl : u ∈ L1
⊢ w ∈ L1 ∘ₗ L3
Tactic:
exists u
Proof state after:
case inl.h
α : Type u_1
L1 L2 L3 : Language α
w : Word α
x✝ : w ∈ (L1 ∪ L2) ∘ₗ L3
u v : Word α
h2 : v ∈ L3
h3 : w = u * v
hl : u ∈ L1
⊢ ∃ v, u ∈ L1 ∧ v ∈ L3 ∧ w = u * v
Theorem: Language.concat_dist_union_r
Proof state before:
case inl.h
α : Type u_1
L1 L2 L3 : Language α
w : Word α
x✝ : w ∈ (L1 ∪ L2) ∘ₗ L3
u v : Word α
h2 : v ∈ L3
h3 : w = u * v
hl : u ∈ L1
⊢ ∃ v, u ∈ L1 ∧ v ∈ L3 ∧ w = u * v
Tactic:
exists v
Proof state after:
no goals
Theorem: Language.concat_dist_union_r
Proof state before:
case inr
α : Type u_1
L1 L2 L3 : Language α
w : Word α
x✝ : w ∈ (L1 ∪ L2) ∘ₗ L3
u v : Word α
h2 : v ∈ L3
h3 : w = u * v
hr : u ∈ L2
⊢ w ∈ L1 ∘ₗ L3 ∪ L2 ∘ₗ L3
Tactic:
apply Or.inr
Proof state after:
case inr.h
α : Type u_1
L1 L2 L3 : Language α
w : Word α
x✝ : w ∈ (L1 ∪ L2) ∘ₗ L3
u v : Word α
h2 : v ∈ L3
h3 : w = u * v
hr : u ∈ L2
⊢ w ∈ L2 ∘ₗ L3
Theorem: Language.concat_dist_union_r
Proof state before:
case inr.h
α : Type u_1
L1 L2 L3 : Language α
w : Word α
x✝ : w ∈ (L1 ∪ L2) ∘ₗ L3
u v : Word α
h2 : v ∈ L3
h3 : w = u * v
hr : u ∈ L2
⊢ w ∈ L2 ∘ₗ L3
Tactic:
exists u
Proof state after:
case inr.h
α : Type u_1
L1 L2 L3 : Language α
w : Word α
x✝ : w ∈ (L1 ∪ L2) ∘ₗ L3
u v : Word α
h2 : v ∈ L3
h3 : w = u * v
hr : u ∈ L2
⊢ ∃ v, u ∈ L2 ∧ v ∈ L3 ∧ w = u * v
Theorem: Language.concat_dist_union_r
Proof state before:
case inr.h
α : Type u_1
L1 L2 L3 : Language α
w : Word α
x✝ : w ∈ (L1 ∪ L2) ∘ₗ L3
u v : Word α
h2 : v ∈ L3
h3 : w = u * v
hr : u ∈ L2
⊢ ∃ v, u ∈ L2 ∧ v ∈ L3 ∧ w = u * v
Tactic:
exists v
Proof state after:
no goals
Theorem: Language.concat_dist_union_r
Proof state before:
case h.mpr
α : Type u_1
L1 L2 L3 : Language α
w : Word α
⊢ w ∈ L1 ∘ₗ L3 ∪ L2 ∘ₗ L3 → w ∈ (L1 ∪ L2) ∘ₗ L3
Tactic:
intro
| Or.inl hl => cases hl with | intro u pu => cases pu with | intro v pv =>
    match pv with
    | ⟨h1, h2, h3⟩ => exists u, v; exact ⟨Or.inl h1, h2, h3⟩
| Or.inr hr => cases hr with | intro u pu => cases pu with | intro v pv =>
    match pv with
    | ⟨h1, h2, h3⟩ => exists u, v; exact ⟨Or.inr h1, h2, h3⟩
Proof state after:
no goals
Theorem: Language.concat_dist_union_r
Proof state before:
α : Type u_1
L1 L2 L3 : Language α
w : Word α
x✝ : w ∈ L1 ∘ₗ L3 ∪ L2 ∘ₗ L3
hl : w ∈ L1 ∘ₗ L3
⊢ w ∈ (L1 ∪ L2) ∘ₗ L3
Tactic:
cases hl with | intro u pu => cases pu with | intro v pv =>
match pv with
| ⟨h1, h2, h3⟩ => exists u, v; exact ⟨Or.inl h1, h2, h3⟩
Proof state after:
no goals
Theorem: Language.concat_dist_union_r
Proof state before:
case intro
α : Type u_1
L1 L2 L3 : Language α
w : Word α
x✝ : w ∈ L1 ∘ₗ L3 ∪ L2 ∘ₗ L3
u : Word α
pu : ∃ v, u ∈ L1 ∧ v ∈ L3 ∧ w = u * v
⊢ w ∈ (L1 ∪ L2) ∘ₗ L3
Tactic:
cases pu with | intro v pv =>
match pv with
| ⟨h1, h2, h3⟩ => exists u, v; exact ⟨Or.inl h1, h2, h3⟩
Proof state after:
no goals
Theorem: Language.concat_dist_union_r
Proof state before:
case intro.intro
α : Type u_1
L1 L2 L3 : Language α
w : Word α
x✝ : w ∈ L1 ∘ₗ L3 ∪ L2 ∘ₗ L3
u v : Word α
pv : u ∈ L1 ∧ v ∈ L3 ∧ w = u * v
⊢ w ∈ (L1 ∪ L2) ∘ₗ L3
Tactic:
match pv with
| ⟨h1, h2, h3⟩ => exists u, v; exact ⟨Or.inl h1, h2, h3⟩
Proof state after:
no goals
Theorem: Language.concat_dist_union_r
Proof state before:
α : Type u_1
L1 L2 L3 : Language α
w : Word α
x✝ : w ∈ L1 ∘ₗ L3 ∪ L2 ∘ₗ L3
u v : Word α
pv : u ∈ L1 ∧ v ∈ L3 ∧ w = u * v
h1 : u ∈ L1
h2 : v ∈ L3
h3 : w = u * v
⊢ w ∈ (L1 ∪ L2) ∘ₗ L3
Tactic:
exists u, v
Proof state after:
α : Type u_1
L1 L2 L3 : Language α
w : Word α
x✝ : w ∈ L1 ∘ₗ L3 ∪ L2 ∘ₗ L3
u v : Word α
pv : u ∈ L1 ∧ v ∈ L3 ∧ w = u * v
h1 : u ∈ L1
h2 : v ∈ L3
h3 : w = u * v
⊢ u ∈ L1 ∪ L2 ∧ v ∈ L3 ∧ w = u * v
Theorem: Language.concat_dist_union_r
Proof state before:
α : Type u_1
L1 L2 L3 : Language α
w : Word α
x✝ : w ∈ L1 ∘ₗ L3 ∪ L2 ∘ₗ L3
u v : Word α
pv : u ∈ L1 ∧ v ∈ L3 ∧ w = u * v
h1 : u ∈ L1
h2 : v ∈ L3
h3 : w = u * v
⊢ u ∈ L1 ∪ L2 ∧ v ∈ L3 ∧ w = u * v
Tactic:
exact ⟨Or.inl h1, h2, h3⟩
Proof state after:
no goals
Theorem: Language.concat_dist_union_r
Proof state before:
α : Type u_1
L1 L2 L3 : Language α
w : Word α
x✝ : w ∈ L1 ∘ₗ L3 ∪ L2 ∘ₗ L3
hr : w ∈ L2 ∘ₗ L3
⊢ w ∈ (L1 ∪ L2) ∘ₗ L3
Tactic:
cases hr with | intro u pu => cases pu with | intro v pv =>
match pv with
| ⟨h1, h2, h3⟩ => exists u, v; exact ⟨Or.inr h1, h2, h3⟩
Proof state after:
no goals