have hσmon : ∀ x, x ∈ Submonoid.powers σ := by
  simpa [← mem_powers_iff_mem_zpowers] using hσ
K : Type u_1
L : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : NumberField K
inst✝² : Algebra K L
inst✝¹ : IsGalois K L
inst✝ : FiniteDimensional K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
η : L
hη : (Algebra.norm K) η = 1
α β : L ≃ₐ[K] L
⊢ ↑(cocycle hσ hη (α * β)) = α ↑(cocycle hσ hη β) * ↑(cocycle hσ hη α)
K : Type u_1
L : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : NumberField K
inst✝² : Algebra K L
inst✝¹ : IsGalois K L
inst✝ : FiniteDimensional K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
η : L
hη : (Algebra.norm K) η = 1
α β : L ≃ₐ[K] L
hσmon : ∀ (x : L ≃ₐ[K] L), x ∈ Submonoid.powers σ
⊢ ↑(cocycle hσ hη (α * β)) = α ↑(cocycle hσ hη β) * ↑(cocycle hσ hη α)