Theorem: Misc.Nat.mul_eq_one (LeanSAT/Util/Misc.lean)

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

case mpr
a b : Nat
⊢ a = 1 ∧ b = 1 → a * b = 1

State before:
case mp
a b : Nat
⊢ a * b = 1 → a = 1 ∧ b = 1

case mpr
a b : Nat
⊢ a = 1 ∧ b = 1 → a * b = 1
Tactic:
. intro h
  exact ⟨Nat.eq_one_of_mul_eq_one_right h, Nat.eq_one_of_mul_eq_one_left h⟩
State after:
case mpr
a b : Nat
⊢ a = 1 ∧ b = 1 → a * b = 1

State before:
case mpr
a b : Nat
⊢ a = 1 ∧ b = 1 → a * b = 1
Tactic:
. intro h
  rw [h.1, h.2]
State after:
no goals

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

State before:
case mp
a b : Nat
h : a * b = 1
⊢ a = 1 ∧ b = 1
Tactic:
exact ⟨Nat.eq_one_of_mul_eq_one_right h, Nat.eq_one_of_mul_eq_one_left h⟩
State after:
no goals

State before:
case mpr
a b : Nat
⊢ a = 1 ∧ b = 1 → a * b = 1
Tactic:
intro h
State after:
case mpr
a b : Nat
h : a = 1 ∧ b = 1
⊢ a * b = 1

State before:
case mpr
a b : Nat
h : a = 1 ∧ b = 1
⊢ a * b = 1
Tactic:
rw [h.1, h.2]
State after:
no goals