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

State before:
α : Type u_1
L : Language α
u v : Word α
⊢ u ≃( L ) v ↔ ∀ (x : Word α), u * x ≃( L ) v * x
Tactic:
constructor
State after:
case mp
α : Type u_1
L : Language α
u v : Word α
⊢ u ≃( L ) v → ∀ (x : Word α), u * x ≃( L ) v * x

case mpr
α : Type u_1
L : Language α
u v : Word α
⊢ (∀ (x : Word α), u * x ≃( L ) v * x) → u ≃( L ) v

State before:
case mp
α : Type u_1
L : Language α
u v : Word α
⊢ u ≃( L ) v → ∀ (x : Word α), u * x ≃( L ) v * x

case mpr
α : Type u_1
L : Language α
u v : Word α
⊢ (∀ (x : Word α), u * x ≃( L ) v * x) → u ≃( L ) v
Tactic:
. intro h w x
  have := h (w * x)
  rw [<- Word.monoid.mul_assoc] at this
  rw [<- Word.monoid.mul_assoc] at this
  assumption
State after:
case mpr
α : Type u_1
L : Language α
u v : Word α
⊢ (∀ (x : Word α), u * x ≃( L ) v * x) → u ≃( L ) v

State before:
case mpr
α : Type u_1
L : Language α
u v : Word α
⊢ (∀ (x : Word α), u * x ≃( L ) v * x) → u ≃( L ) v
Tactic:
. intro h w
  have := (h w) ε
  simp at this
  assumption
State after:
no goals

State before:
case mp
α : Type u_1
L : Language α
u v : Word α
⊢ u ≃( L ) v → ∀ (x : Word α), u * x ≃( L ) v * x
Tactic:
intro h w x
State after:
case mp
α : Type u_1
L : Language α
u v : Word α
h : u ≃( L ) v
w x : Word α
⊢ u * w * x ∈ L ↔ v * w * x ∈ L

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

State before:
case mp
α : Type u_1
L : Language α
u v : Word α
h : u ≃( L ) v
w x : Word α
this : u * (w * x) ∈ L ↔ v * (w * x) ∈ L
⊢ u * w * x ∈ L ↔ v * w * x ∈ L
Tactic:
rw [<- Word.monoid.mul_assoc] at this
State after:
case mp
α : Type u_1
L : Language α
u v : Word α
h : u ≃( L ) v
w x : Word α
this : u * w * x ∈ L ↔ v * (w * x) ∈ L
⊢ u * w * x ∈ L ↔ v * w * x ∈ L

State before:
case mp
α : Type u_1
L : Language α
u v : Word α
h : u ≃( L ) v
w x : Word α
this : u * w * x ∈ L ↔ v * (w * x) ∈ L
⊢ u * w * x ∈ L ↔ v * w * x ∈ L
Tactic:
rw [<- Word.monoid.mul_assoc] at this
State after:
case mp
α : Type u_1
L : Language α
u v : Word α
h : u ≃( L ) v
w x : Word α
this : u * w * x ∈ L ↔ v * w * x ∈ L
⊢ u * w * x ∈ L ↔ v * w * x ∈ L

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

State before:
case mpr
α : Type u_1
L : Language α
u v : Word α
⊢ (∀ (x : Word α), u * x ≃( L ) v * x) → u ≃( L ) v
Tactic:
intro h w
State after:
case mpr
α : Type u_1
L : Language α
u v : Word α
h : ∀ (x : Word α), u * x ≃( L ) v * x
w : Word α
⊢ u * w ∈ L ↔ v * w ∈ L

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

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

State before:
case mpr
α : Type u_1
L : Language α
u v : Word α
h : ∀ (x : Word α), u * x ≃( L ) v * x
w : Word α
this : u * w ∈ L ↔ v * w ∈ L
⊢ u * w ∈ L ↔ v * w ∈ L
Tactic:
assumption
State after:
no goals