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

State before:
a b c : ℤω
⊢ natNorm (a * b) = natNorm a * natNorm b
Tactic:
have := normSq_mul a b
State after:
a b c : ℤω
this :
  ↑normSq (OneHom.toFun (↑↑inclusion) a * OneHom.toFun (↑↑inclusion) b) =
    ↑normSq (OneHom.toFun (↑↑inclusion) a) * ↑normSq (OneHom.toFun (↑↑inclusion) b)
⊢ natNorm (a * b) = natNorm a * natNorm b

State before:
a b c : ℤω
this :
  ↑normSq (OneHom.toFun (↑↑inclusion) a * OneHom.toFun (↑↑inclusion) b) =
    ↑normSq (OneHom.toFun (↑↑inclusion) a) * ↑normSq (OneHom.toFun (↑↑inclusion) b)
⊢ natNorm (a * b) = natNorm a * natNorm b
Tactic:
rw [← coe_hMul] at this
State after:
a b c : ℤω
this :
  ↑normSq (OneHom.toFun (↑↑inclusion) (a * b)) =
    ↑normSq (OneHom.toFun (↑↑inclusion) a) * ↑normSq (OneHom.toFun (↑↑inclusion) b)
⊢ natNorm (a * b) = natNorm a * natNorm b

State before:
a b c : ℤω
this :
  ↑normSq (OneHom.toFun (↑↑inclusion) (a * b)) =
    ↑normSq (OneHom.toFun (↑↑inclusion) a) * ↑normSq (OneHom.toFun (↑↑inclusion) b)
⊢ natNorm (a * b) = natNorm a * natNorm b
Tactic:
simp only [natNorm_coe] at this
State after:
a b c : ℤω
this : ↑(natNorm (a * b)) = ↑(natNorm a) * ↑(natNorm b)
⊢ natNorm (a * b) = natNorm a * natNorm b

State before:
a b c : ℤω
this : ↑(natNorm (a * b)) = ↑(natNorm a) * ↑(natNorm b)
⊢ natNorm (a * b) = natNorm a * natNorm b
Tactic:
exact_mod_cast this
State after:
no goals