Theorem: HTPI.ge_one_of_prod_one (HTPILib/Chap7.lean)

State before:
a b : ℕ
h : a * b = 1
⊢ a ≥ 1
Tactic:
have h1 : a ≠ 0 := by
  by_contra h1
  rewrite [h1] at h
  contradict h
  linarith
  done
State after:
a b : ℕ
h : a * b = 1
h1 : a ≠ 0
⊢ a ≥ 1

State before:
a b : ℕ
h : a * b = 1
h1 : a ≠ 0
⊢ a ≥ 1
Tactic:
show a ≥ 1 from Nat.pos_of_ne_zero h1
State after:
no goals

State before:
a b : ℕ
h : a * b = 1
⊢ a ≠ 0
Tactic:
by_contra h1
State after:
a b : ℕ
h : a * b = 1
h1 : a = 0
⊢ False

State before:
a b : ℕ
h : a * b = 1
h1 : a = 0
⊢ False
Tactic:
rewrite [h1] at h
State after:
a b : ℕ
h : 0 * b = 1
h1 : a = 0
⊢ False

State before:
a b : ℕ
h : 0 * b = 1
h1 : a = 0
⊢ False
Tactic:
contradict h
State after:
a b : ℕ
h : 0 * b = 1
h1 : a = 0
⊢ ¬0 * b = 1

State before:
a b : ℕ
h : 0 * b = 1
h1 : a = 0
⊢ ¬0 * b = 1
Tactic:
linarith
State after:
no goals