Theorem: ℤθ.my_natCast_succ (Mordell4/CubicRing.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, 0⟩ : ℤθ) = (⟨Int.ofNat n + 1, 0, 0⟩ : ℤθ)
State after:
a b c : ℤθ
n : ℕ
⊢ { f := Int.ofNat (n + 1), g := 0, h := 0 } = { f := Int.ofNat n + 1, g := 0, h := 0 }

State before:
a b c : ℤθ
n : ℕ
⊢ { f := Int.ofNat (n + 1), g := 0, h := 0 } = { f := Int.ofNat n + 1, g := 0, h := 0 }
Tactic:
simp
State after:
no goals