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

State before:
α : Type u_1
L : Language α
u v : Word α
h : u ≃( L ) v
⊢ u ∈ L ↔ v ∈ L
Tactic:
have := h ε
State after:
α : Type u_1
L : Language α
u v : Word α
h : u ≃( L ) v
this : u * ε ∈ L ↔ v * ε ∈ L
⊢ u ∈ L ↔ v ∈ L

State before:
α : Type u_1
L : Language α
u v : Word α
h : u ≃( L ) v
this : u * ε ∈ L ↔ v * ε ∈ L
⊢ u ∈ L ↔ v ∈ L
Tactic:
simp at this
State after:
α : Type u_1
L : Language α
u v : Word α
h : u ≃( L ) v
this : u ∈ L ↔ v ∈ L
⊢ u ∈ L ↔ v ∈ L

State before:
α : Type u_1
L : Language α
u v : Word α
h : u ≃( L ) v
this : u ∈ L ↔ v ∈ L
⊢ u ∈ L ↔ v ∈ L
Tactic:
assumption
State after:
no goals