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

State before:
m n : Nat
h : m * 0 = 1
⊢ 0 = 1
Tactic:
contradiction
State after:
no goals

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

State before:
m n n✝ : Nat
h : m * (n✝ + 2) = 1
⊢ n✝ + 2 = 1
Tactic:
cases m
State after:
case zero
n n✝ : Nat
h : 0 * (n✝ + 2) = 1
⊢ n✝ + 2 = 1

case succ
n n✝¹ n✝ : Nat
h : (n✝ + 1) * (n✝¹ + 2) = 1
⊢ n✝¹ + 2 = 1

State before:
case zero
n n✝ : Nat
h : 0 * (n✝ + 2) = 1
⊢ n✝ + 2 = 1
Tactic:
rw [Nat.zero_mul] at h
State after:
case zero
n n✝ : Nat
h : 0 = 1
⊢ n✝ + 2 = 1

State before:
case zero
n n✝ : Nat
h : 0 = 1
⊢ n✝ + 2 = 1
Tactic:
contradiction
State after:
no goals

State before:
case succ
n n✝¹ n✝ : Nat
h : (n✝ + 1) * (n✝¹ + 2) = 1
⊢ n✝¹ + 2 = 1
Tactic:
rw [Nat.succ_mul] at h
State after:
case succ
n n✝¹ n✝ : Nat
h : n✝ * (n✝¹ + 2) + (n✝¹ + 2) = 1
⊢ n✝¹ + 2 = 1

State before:
case succ
n n✝¹ n✝ : Nat
h : n✝ * (n✝¹ + 2) + (n✝¹ + 2) = 1
⊢ n✝¹ + 2 = 1
Tactic:
injection h
State after:
case succ
n n✝¹ n✝ : Nat
n_eq✝ : (n✝ * (n✝¹ + 2)).add (n✝¹ + 1) = 0
⊢ n✝¹ + 2 = 1

State before:
case succ
n n✝¹ n✝ : Nat
n_eq✝ : (n✝ * (n✝¹ + 2)).add (n✝¹ + 1) = 0
⊢ n✝¹ + 2 = 1
Tactic:
contradiction
State after:
no goals