Theorem: ℤα.my_intCast_of_nat (Mordell4/Rt7Ring.lean)

State before:
a b c : ℤα
⊢ ∀ (n : ℕ), intCast ↑n = natCast n
Tactic:
intro n
State after:
a b c : ℤα
n : ℕ
⊢ intCast ↑n = natCast n

State before:
a b c : ℤα
n : ℕ
⊢ intCast ↑n = natCast n
Tactic:
rfl
State after:
no goals