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

State before:
a b : ℕ
h : a * b = 1
⊢ a = 1
Tactic:
have h1 : a ≥ 1 := ge_one_of_prod_one h
State after:
a b : ℕ
h : a * b = 1
h1 : a ≥ 1
⊢ a = 1

State before:
a b : ℕ
h : a * b = 1
h1 : a ≥ 1
⊢ a = 1
Tactic:
have h2 : a * b ≠ 0 := by linarith
State after:
a b : ℕ
h : a * b = 1
h1 : a ≥ 1
h2 : a * b ≠ 0
⊢ a = 1

State before:
a b : ℕ
h : a * b = 1
h1 : a ≥ 1
h2 : a * b ≠ 0
⊢ a = 1
Tactic:
have h3 : a ≤ a * b := le_nonzero_prod_left h2
State after:
a b : ℕ
h : a * b = 1
h1 : a ≥ 1
h2 : a * b ≠ 0
h3 : a ≤ a * b
⊢ a = 1

State before:
a b : ℕ
h : a * b = 1
h1 : a ≥ 1
h2 : a * b ≠ 0
h3 : a ≤ a * b
⊢ a = 1
Tactic:
rewrite [h] at h3
State after:
a b : ℕ
h : a * b = 1
h1 : a ≥ 1
h2 : a * b ≠ 0
h3 : a ≤ 1
⊢ a = 1

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

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