Theorem: Nat.eq_one_of_mul_eq_one_right (Extra/Nat/Lemmas.lean)

State before:
m n : Nat
h : m * n = 1
⊢ m = 1
Tactic:
rw [Nat.mul_comm] at h
State after:
m n : Nat
h : n * m = 1
⊢ m = 1

State before:
m n : Nat
h : n * m = 1
⊢ m = 1
Tactic:
exact eq_one_of_mul_eq_one_left h
State after:
no goals