Theorem: ZMod.two_ne_one (FormalBook/Chapter_01.lean)

State before:
q : ℕ
inst✝ : Fact (1 < q)
⊢ 2 ≠ 1
Tactic:
intro h1
State after:
q : ℕ
inst✝ : Fact (1 < q)
h1 : 2 = 1
⊢ False

State before:
q : ℕ
inst✝ : Fact (1 < q)
h1 : 2 = 1
⊢ False
Tactic:
have h : (2 - 1 : ZMod q) = 0 := by exact Iff.mpr sub_eq_zero h1
State after:
q : ℕ
inst✝ : Fact (1 < q)
h1 : 2 = 1
h : 2 - 1 = 0
⊢ False

State before:
q : ℕ
inst✝ : Fact (1 < q)
h1 : 2 = 1
h : 2 - 1 = 0
⊢ False
Tactic:
norm_num at h
State after:
no goals

State before:
q : ℕ
inst✝ : Fact (1 < q)
h1 : 2 = 1
⊢ 2 - 1 = 0
Tactic:
exact Iff.mpr sub_eq_zero h1
State after:
no goals