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

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
R : Type u_1
inst✝ : AddGroupWithOne R
H : ∀ (n : ℕ), ↑n = 0 → n = 0
m n : ℕ
h : ↑m = ↑n
⊢ m = n
induction' m with m ih generalizing n
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

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
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
cases' n with n
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
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
simp only [Nat.cast_succ, add_right_cancel_iff] at h
no goals
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
rwa [ih]
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
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
rw [H n]
no goals
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
rw [← h, Nat.cast_zero]
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
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
apply H
no goals
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
rw [h, Nat.cast_zero]