Theorem: nequiv_if_diff_parity' (meetings/ex4.lean)

State before:
x y : ℤ
⊢ Even x → Odd y → ¬equiv_rel x y
Tactic:
intros ex ey equiv
State after:
x y : ℤ
ex : Even x
ey : Odd y
equiv : equiv_rel x y
⊢ False

State before:
x y : ℤ
ex : Even x
ey : Odd y
equiv : equiv_rel x y
⊢ False
Tactic:
have nequiv := nequiv_if_diff_parity ey ex
State after:
x y : ℤ
ex : Even x
ey : Odd y
equiv : equiv_rel x y
nequiv : ¬equiv_rel y x
⊢ False

State before:
x y : ℤ
ex : Even x
ey : Odd y
equiv : equiv_rel x y
nequiv : ¬equiv_rel y x
⊢ False
Tactic:
exact nequiv (equiv_inst.symm equiv)
State after:
no goals