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

State before:
a b c : ℤα
⊢ natCast 0 = zero
Tactic:
unfold natCast
State after:
a b c : ℤα
⊢ { z := ↑0, w := 0 } = zero

State before:
a b c : ℤα
⊢ { z := ↑0, w := 0 } = zero
Tactic:
rw [Int.ofNat_zero]
State after:
a b c : ℤα
⊢ { z := 0, w := 0 } = zero

State before:
a b c : ℤα
⊢ { z := 0, w := 0 } = zero
Tactic:
rfl
State after:
no goals