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

State before:
a b c : ℤα
⊢ ∀ (n : ℕ), natCast (n + 1) = add (natCast n) one
Tactic:
intro n
State after:
a b c : ℤα
n : ℕ
⊢ natCast (n + 1) = add (natCast n) one

State before:
a b c : ℤα
n : ℕ
⊢ natCast (n + 1) = add (natCast n) one
Tactic:
change (⟨Int.ofNat (n + 1), 0⟩ : ℤα) = (⟨Int.ofNat n + 1, 0⟩ : ℤα)
State after:
a b c : ℤα
n : ℕ
⊢ { z := Int.ofNat (n + 1), w := 0 } = { z := Int.ofNat n + 1, w := 0 }

State before:
a b c : ℤα
n : ℕ
⊢ { z := Int.ofNat (n + 1), w := 0 } = { z := Int.ofNat n + 1, w := 0 }
Tactic:
simp
State after:
no goals