Theorem: ℤω.normSq_coe (Mordell4/Eisenstein.lean)

State before:
a b c : ℤω
⊢ ↑normSq (OneHom.toFun (↑↑inclusion) a) = ↑(norm a)
Tactic:
cases' a with x y
State after:
case mk
b c : ℤω
x y : ℤ
⊢ ↑normSq (OneHom.toFun ↑↑inclusion { x := x, y := y }) = ↑(norm { x := x, y := y })

State before:
case mk
b c : ℤω
x y : ℤ
⊢ ↑normSq (OneHom.toFun ↑↑inclusion { x := x, y := y }) = ↑(norm { x := x, y := y })
Tactic:
simp [normSq, Norm]
State after:
case mk
b c : ℤω
x y : ℤ
⊢ (↑inclusion { x := x, y := y }).re * (↑inclusion { x := x, y := y }).re +
      (↑inclusion { x := x, y := y }).im * (↑inclusion { x := x, y := y }).im =
    ↑(norm { x := x, y := y })

State before:
case mk
b c : ℤω
x y : ℤ
⊢ (↑inclusion { x := x, y := y }).re * (↑inclusion { x := x, y := y }).re +
      (↑inclusion { x := x, y := y }).im * (↑inclusion { x := x, y := y }).im =
    ↑(norm { x := x, y := y })
Tactic:
ring_nf
State after:
case mk
b c : ℤω
x y : ℤ
⊢ (↑inclusion { x := x, y := y }).re ^ 2 + (↑inclusion { x := x, y := y }).im ^ 2 = ↑(norm { x := x, y := y })