case mk.refl
R : Type u_1
inst✝ : AddMonoidWithOne R
m : ℕ
⊢ IsNat (↑↑m) m
R : Type u_1
inst✝ : AddMonoidWithOne R
n m : ℕ
⊢ IsNat n m → IsNat (↑n) m
rintro ⟨⟨⟩⟩
no goals
case mk.refl
R : Type u_1
inst✝ : AddMonoidWithOne R
m : ℕ
⊢ IsNat (↑↑m) m
exact ⟨rfl⟩