case mk.refl
R : Type u_1
inst✝ : Ring R
m : ℕ
⊢ IsNat (↑↑m) m
R : Type u_1
inst✝ : Ring R
n : ℤ
m : ℕ
⊢ IsNat n m → IsNat (↑n) m
rintro ⟨⟨⟩⟩
no goals
case mk.refl
R : Type u_1
inst✝ : Ring R
m : ℕ
⊢ IsNat (↑↑m) m
exact ⟨by simp⟩
no goals
R : Type u_1
inst✝ : Ring R
m : ℕ
⊢ ↑↑m = ↑m
simp