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

State before:
m n : Nat
⊢ m * n = 1 ↔ m = 1 ∧ n = 1
Tactic:
constructor
State after:
case mp
m n : Nat
⊢ m * n = 1 → m = 1 ∧ n = 1

case mpr
m n : Nat
⊢ m = 1 ∧ n = 1 → m * n = 1

State before:
case mp
m n : Nat
⊢ m * n = 1 → m = 1 ∧ n = 1
Tactic:
intro h
State after:
case mp
m n : Nat
h : m * n = 1
⊢ m = 1 ∧ n = 1

State before:
case mp
m n : Nat
h : m * n = 1
⊢ m = 1 ∧ n = 1
Tactic:
rw [eq_one_of_mul_eq_one_right h, eq_one_of_mul_eq_one_left h]
State after:
case mp
m n : Nat
h : m * n = 1
⊢ 1 = 1 ∧ 1 = 1

State before:
case mp
m n : Nat
h : m * n = 1
⊢ 1 = 1 ∧ 1 = 1
Tactic:
trivial
State after:
no goals

State before:
case mpr
m n : Nat
⊢ m = 1 ∧ n = 1 → m * n = 1
Tactic:
intro ⟨hm, hn⟩
State after:
case mpr
m n : Nat
hm : m = 1
hn : n = 1
⊢ m * n = 1

State before:
case mpr
m n : Nat
hm : m = 1
hn : n = 1
⊢ m * n = 1
Tactic:
rw [hm, hn]
State after:
no goals