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

State before:
n : ℕ
h : n ∣ 1
⊢ n = 1
Tactic:
obtain (j : Nat) (h1 : 1 = n * j) from h
State after:
n : ℕ
h : n ∣ 1
j : ℕ
h1 : 1 = n * j
⊢ n = 1

State before:
n : ℕ
h : n ∣ 1
j : ℕ
h1 : 1 = n * j
⊢ n = 1
Tactic:
show n = 1 from eq_one_of_prod_one h1.symm
State after:
no goals