R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))
n : ℕ+
⊢ ↑(IsUnit.unit (_ : IsUnit ↑↑n)) = ↑↑n
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))
n : ℕ+
⊢ ↑↑n = ↑↑n
change ((PNat.isUnit_natCast (R := R) n).unit : R) = ↑n
no goals
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))
n : ℕ+
⊢ ↑(IsUnit.unit (_ : IsUnit ↑↑n)) = ↑↑n
simp only [IsUnit.unit_spec]