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

State before:
α : Type u_1
L : Language α
u v : Word α
⊢ (∃ w, u * w ∈ L ∧ v * w ∉ L) → ¬u ≃( L ) v
Tactic:
intro ⟨ w, uw_in_l, vw_nin_l ⟩ contra
State after:
α : Type u_1
L : Language α
u v w : Word α
uw_in_l : u * w ∈ L
vw_nin_l : v * w ∉ L
contra : u ≃( L ) v
⊢ False

State before:
α : Type u_1
L : Language α
u v w : Word α
uw_in_l : u * w ∈ L
vw_nin_l : v * w ∉ L
contra : u ≃( L ) v
⊢ False
Tactic:
apply vw_nin_l
State after:
α : Type u_1
L : Language α
u v w : Word α
uw_in_l : u * w ∈ L
vw_nin_l : v * w ∉ L
contra : u ≃( L ) v
⊢ v * w ∈ L

State before:
α : Type u_1
L : Language α
u v w : Word α
uw_in_l : u * w ∈ L
vw_nin_l : v * w ∉ L
contra : u ≃( L ) v
⊢ v * w ∈ L
Tactic:
apply (contra w).mp
State after:
α : Type u_1
L : Language α
u v w : Word α
uw_in_l : u * w ∈ L
vw_nin_l : v * w ∉ L
contra : u ≃( L ) v
⊢ u * w ∈ L

State before:
α : Type u_1
L : Language α
u v w : Word α
uw_in_l : u * w ∈ L
vw_nin_l : v * w ∉ L
contra : u ≃( L ) v
⊢ u * w ∈ L
Tactic:
exact uw_in_l
State after:
no goals