Theorem: MyhillNerodeRelation.not_congruent_if (FormalSystems/Chomsky/Regular/Nerode.lean)

State before:
α : Type u_1
L : Language α
u v : Word α
pre : u ≠ v
⊢ (∃ w, Language.isSingleton ({u * w, v * w} ∩ L)) → ¬u ≃( L ) v
Tactic:
intro ⟨ w, singl, singl_inter, h ⟩
State after:
α : Type u_1
L : Language α
u v : Word α
pre : u ≠ v
w singl : Word α
singl_inter : singl ∈ {u * w, v * w} ∩ L
h : ∀ v_1 ∈ {u * w, v * w} ∩ L, v_1 = singl
⊢ ¬u ≃( L ) v

State before:
α : Type u_1
L : Language α
u v : Word α
pre : u ≠ v
w singl : Word α
singl_inter : singl ∈ {u * w, v * w} ∩ L
h : ∀ v_1 ∈ {u * w, v * w} ∩ L, v_1 = singl
⊢ ¬u ≃( L ) v
Tactic:
intro contra
State after:
α : Type u_1
L : Language α
u v : Word α
pre : u ≠ v
w singl : Word α
singl_inter : singl ∈ {u * w, v * w} ∩ L
h : ∀ v_1 ∈ {u * w, v * w} ∩ L, v_1 = singl
contra : u ≃( L ) v
⊢ False

State before:
α : Type u_1
L : Language α
u v : Word α
pre : u ≠ v
w singl : Word α
singl_inter : singl ∈ {u * w, v * w} ∩ L
h : ∀ v_1 ∈ {u * w, v * w} ∩ L, v_1 = singl
contra : u ≃( L ) v
⊢ False
Tactic:
have h2 := contra w
State after:
α : Type u_1
L : Language α
u v : Word α
pre : u ≠ v
w singl : Word α
singl_inter : singl ∈ {u * w, v * w} ∩ L
h : ∀ v_1 ∈ {u * w, v * w} ∩ L, v_1 = singl
contra : u ≃( L ) v
h2 : u * w ∈ L ↔ v * w ∈ L
⊢ False

State before:
α : Type u_1
L : Language α
u v : Word α
pre : u ≠ v
w singl : Word α
singl_inter : singl ∈ {u * w, v * w} ∩ L
h : ∀ v_1 ∈ {u * w, v * w} ∩ L, v_1 = singl
contra : u ≃( L ) v
h2 : u * w ∈ L ↔ v * w ∈ L
⊢ False
Tactic:
cases singl_inter.left
State after:
case inl
α : Type u_1
L : Language α
u v : Word α
pre : u ≠ v
w singl : Word α
singl_inter : singl ∈ {u * w, v * w} ∩ L
h : ∀ v_1 ∈ {u * w, v * w} ∩ L, v_1 = singl
contra : u ≃( L ) v
h2 : u * w ∈ L ↔ v * w ∈ L
h✝ : singl = u * w
⊢ False

case inr
α : Type u_1
L : Language α
u v : Word α
pre : u ≠ v
w singl : Word α
singl_inter : singl ∈ {u * w, v * w} ∩ L
h : ∀ v_1 ∈ {u * w, v * w} ∩ L, v_1 = singl
contra : u ≃( L ) v
h2 : u * w ∈ L ↔ v * w ∈ L
h✝ : singl ∈ {v * w}
⊢ False

State before:
α : Type u_1
L : Language α
u v : Word α
pre : u ≠ v
w singl : Word α
singl_inter : singl ∈ {u * w, v * w} ∩ L
h : ∀ v_1 ∈ {u * w, v * w} ∩ L, v_1 = singl
contra : u ≃( L ) v
h2 : u * w ∈ L ↔ v * w ∈ L
e : singl = u * w
⊢ False
Tactic:
case inl e =>
  have vw_in_l := h2.mp $ e ▸ singl_inter.right
  have vw_eq_uw := e ▸ h (v*w) ⟨ Or.inr rfl, vw_in_l ⟩
  exact pre <| Eq.symm <| Word.mul_right_cancel vw_eq_uw
State after:
no goals

State before:
α : Type u_1
L : Language α
u v : Word α
pre : u ≠ v
w singl : Word α
singl_inter : singl ∈ {u * w, v * w} ∩ L
h : ∀ v_1 ∈ {u * w, v * w} ∩ L, v_1 = singl
contra : u ≃( L ) v
h2 : u * w ∈ L ↔ v * w ∈ L
e : singl ∈ {v * w}
⊢ False
Tactic:
case inr e =>
  have uw_in_l := h2.mpr $ e ▸ singl_inter.right
  have uw_eq_vw := e ▸ h (u*w) ⟨ Or.inl rfl, uw_in_l ⟩
  exact pre <| Word.mul_right_cancel uw_eq_vw
State after:
no goals

State before:
α : Type u_1
L : Language α
u v : Word α
pre : u ≠ v
w singl : Word α
singl_inter : singl ∈ {u * w, v * w} ∩ L
h : ∀ v_1 ∈ {u * w, v * w} ∩ L, v_1 = singl
contra : u ≃( L ) v
h2 : u * w ∈ L ↔ v * w ∈ L
e : singl = u * w
⊢ False
Tactic:
have vw_in_l := h2.mp $ e ▸ singl_inter.right
State after:
α : Type u_1
L : Language α
u v : Word α
pre : u ≠ v
w singl : Word α
singl_inter : singl ∈ {u * w, v * w} ∩ L
h : ∀ v_1 ∈ {u * w, v * w} ∩ L, v_1 = singl
contra : u ≃( L ) v
h2 : u * w ∈ L ↔ v * w ∈ L
e : singl = u * w
vw_in_l : v * w ∈ L
⊢ False

State before:
α : Type u_1
L : Language α
u v : Word α
pre : u ≠ v
w singl : Word α
singl_inter : singl ∈ {u * w, v * w} ∩ L
h : ∀ v_1 ∈ {u * w, v * w} ∩ L, v_1 = singl
contra : u ≃( L ) v
h2 : u * w ∈ L ↔ v * w ∈ L
e : singl = u * w
vw_in_l : v * w ∈ L
⊢ False
Tactic:
have vw_eq_uw := e ▸ h (v*w) ⟨ Or.inr rfl, vw_in_l ⟩
State after:
α : Type u_1
L : Language α
u v : Word α
pre : u ≠ v
w singl : Word α
singl_inter : singl ∈ {u * w, v * w} ∩ L
h : ∀ v_1 ∈ {u * w, v * w} ∩ L, v_1 = singl
contra : u ≃( L ) v
h2 : u * w ∈ L ↔ v * w ∈ L
e : singl = u * w
vw_in_l : v * w ∈ L
vw_eq_uw : v * w = u * w
⊢ False

State before:
α : Type u_1
L : Language α
u v : Word α
pre : u ≠ v
w singl : Word α
singl_inter : singl ∈ {u * w, v * w} ∩ L
h : ∀ v_1 ∈ {u * w, v * w} ∩ L, v_1 = singl
contra : u ≃( L ) v
h2 : u * w ∈ L ↔ v * w ∈ L
e : singl = u * w
vw_in_l : v * w ∈ L
vw_eq_uw : v * w = u * w
⊢ False
Tactic:
exact pre <| Eq.symm <| Word.mul_right_cancel vw_eq_uw
State after:
no goals

State before:
α : Type u_1
L : Language α
u v : Word α
pre : u ≠ v
w singl : Word α
singl_inter : singl ∈ {u * w, v * w} ∩ L
h : ∀ v_1 ∈ {u * w, v * w} ∩ L, v_1 = singl
contra : u ≃( L ) v
h2 : u * w ∈ L ↔ v * w ∈ L
e : singl ∈ {v * w}
⊢ False
Tactic:
have uw_in_l := h2.mpr $ e ▸ singl_inter.right
State after:
α : Type u_1
L : Language α
u v : Word α
pre : u ≠ v
w singl : Word α
singl_inter : singl ∈ {u * w, v * w} ∩ L
h : ∀ v_1 ∈ {u * w, v * w} ∩ L, v_1 = singl
contra : u ≃( L ) v
h2 : u * w ∈ L ↔ v * w ∈ L
e : singl ∈ {v * w}
uw_in_l : u * w ∈ L
⊢ False

State before:
α : Type u_1
L : Language α
u v : Word α
pre : u ≠ v
w singl : Word α
singl_inter : singl ∈ {u * w, v * w} ∩ L
h : ∀ v_1 ∈ {u * w, v * w} ∩ L, v_1 = singl
contra : u ≃( L ) v
h2 : u * w ∈ L ↔ v * w ∈ L
e : singl ∈ {v * w}
uw_in_l : u * w ∈ L
⊢ False
Tactic:
have uw_eq_vw := e ▸ h (u*w) ⟨ Or.inl rfl, uw_in_l ⟩
State after:
α : Type u_1
L : Language α
u v : Word α
pre : u ≠ v
w singl : Word α
singl_inter : singl ∈ {u * w, v * w} ∩ L
h : ∀ v_1 ∈ {u * w, v * w} ∩ L, v_1 = singl
contra : u ≃( L ) v
h2 : u * w ∈ L ↔ v * w ∈ L
e : singl ∈ {v * w}
uw_in_l : u * w ∈ L
uw_eq_vw : u * w = v * w
⊢ False

State before:
α : Type u_1
L : Language α
u v : Word α
pre : u ≠ v
w singl : Word α
singl_inter : singl ∈ {u * w, v * w} ∩ L
h : ∀ v_1 ∈ {u * w, v * w} ∩ L, v_1 = singl
contra : u ≃( L ) v
h2 : u * w ∈ L ↔ v * w ∈ L
e : singl ∈ {v * w}
uw_in_l : u * w ∈ L
uw_eq_vw : u * w = v * w
⊢ False
Tactic:
exact pre <| Word.mul_right_cancel uw_eq_vw
State after:
no goals