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

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

State before:
q : ℕ
inst✝ : Fact (1 < q)
h : 1 = 0
⊢ False
Tactic:
have := ZMod.val_one q ▸ (ZMod.val_eq_zero (1 : ZMod q)).mpr h
State after:
q : ℕ
inst✝ : Fact (1 < q)
h : 1 = 0
this : 1 = 0
⊢ False

State before:
q : ℕ
inst✝ : Fact (1 < q)
h : 1 = 0
this : 1 = 0
⊢ False
Tactic:
linarith
State after:
no goals