[GOAL]
R : Type u_1
inst✝ : AddGroupWithOne R
H : ∀ (n : ℕ), ↑n = 0 → n = 0
m n : ℕ
h : ↑m = ↑n
⊢ m = n
[PROOFSTEP]
induction' m with m ih generalizing n
[GOAL]
case zero
R : Type u_1
inst✝ : AddGroupWithOne R
H : ∀ (n : ℕ), ↑n = 0 → n = 0
m n✝ : ℕ
h✝ : ↑m = ↑n✝
n : ℕ
h : ↑Nat.zero = ↑n
⊢ Nat.zero = n
[PROOFSTEP]
rw [H n]
[GOAL]
case zero
R : Type u_1
inst✝ : AddGroupWithOne R
H : ∀ (n : ℕ), ↑n = 0 → n = 0
m n✝ : ℕ
h✝ : ↑m = ↑n✝
n : ℕ
h : ↑Nat.zero = ↑n
⊢ ↑n = 0
[PROOFSTEP]
rw [← h, Nat.cast_zero]
[GOAL]
case succ
R : Type u_1
inst✝ : AddGroupWithOne R
H : ∀ (n : ℕ), ↑n = 0 → n = 0
m✝ n✝ : ℕ
h✝ : ↑m✝ = ↑n✝
m : ℕ
ih : ∀ (n : ℕ), ↑m = ↑n → m = n
n : ℕ
h : ↑(Nat.succ m) = ↑n
⊢ Nat.succ m = n
[PROOFSTEP]
cases' n with n
[GOAL]
case succ.zero
R : Type u_1
inst✝ : AddGroupWithOne R
H : ∀ (n : ℕ), ↑n = 0 → n = 0
m✝ n : ℕ
h✝ : ↑m✝ = ↑n
m : ℕ
ih : ∀ (n : ℕ), ↑m = ↑n → m = n
h : ↑(Nat.succ m) = ↑Nat.zero
⊢ Nat.succ m = Nat.zero
[PROOFSTEP]
apply H
[GOAL]
case succ.zero.a
R : Type u_1
inst✝ : AddGroupWithOne R
H : ∀ (n : ℕ), ↑n = 0 → n = 0
m✝ n : ℕ
h✝ : ↑m✝ = ↑n
m : ℕ
ih : ∀ (n : ℕ), ↑m = ↑n → m = n
h : ↑(Nat.succ m) = ↑Nat.zero
⊢ ↑(Nat.succ m) = 0
[PROOFSTEP]
rw [h, Nat.cast_zero]
[GOAL]
case succ.succ
R : Type u_1
inst✝ : AddGroupWithOne R
H : ∀ (n : ℕ), ↑n = 0 → n = 0
m✝ n✝ : ℕ
h✝ : ↑m✝ = ↑n✝
m : ℕ
ih : ∀ (n : ℕ), ↑m = ↑n → m = n
n : ℕ
h : ↑(Nat.succ m) = ↑(Nat.succ n)
⊢ Nat.succ m = Nat.succ n
[PROOFSTEP]
simp only [Nat.cast_succ, add_right_cancel_iff] at h 
[GOAL]
case succ.succ
R : Type u_1
inst✝ : AddGroupWithOne R
H : ∀ (n : ℕ), ↑n = 0 → n = 0
m✝ n✝ : ℕ
h✝ : ↑m✝ = ↑n✝
m : ℕ
ih : ∀ (n : ℕ), ↑m = ↑n → m = n
n : ℕ
h : ↑m = ↑n
⊢ Nat.succ m = Nat.succ n
[PROOFSTEP]
rwa [ih]
[GOAL]
R : Type u_1
inst✝¹ : AddMonoidWithOne R
inst✝ : CharZero R
n : ℕ
⊢ ↑n = 0 ↔ n = 0
[PROOFSTEP]
rw [← cast_zero, cast_inj]
[GOAL]
R : Type u_1
inst✝¹ : AddMonoidWithOne R
inst✝ : CharZero R
n : ℕ
⊢ ↑n + 1 ≠ 0
[PROOFSTEP]
norm_cast
[GOAL]
R : Type u_1
inst✝¹ : AddMonoidWithOne R
inst✝ : CharZero R
n : ℕ
⊢ ¬n + 1 = 0
[PROOFSTEP]
exact n.succ_ne_zero
[GOAL]
R : Type u_1
inst✝¹ : AddMonoidWithOne R
inst✝ : CharZero R
n : ℕ
⊢ ↑n = 1 ↔ n = 1
[PROOFSTEP]
rw [← cast_one, cast_inj]
[GOAL]
R : Type u_1
inst✝¹ : AddMonoidWithOne R
inst✝ : CharZero R
n : ℕ
h : Nat.AtLeastTwo n
⊢ ofNat n ≠ 1
[PROOFSTEP]
rw [← Nat.cast_eq_ofNat, ← @Nat.cast_one R, Ne.def, Nat.cast_inj]
[GOAL]
R : Type u_1
inst✝¹ : AddMonoidWithOne R
inst✝ : CharZero R
n : ℕ
h : Nat.AtLeastTwo n
⊢ ¬n = 1
[PROOFSTEP]
exact ne_of_gt h.prop
