rw [← ha, ← hb, ← pow_add]
case intro.intro
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 σ
a : ℕ
ha : σ ^ a = α
b : ℕ
hb : σ ^ b = β
⊢ ↑(cocycle hσ hη (α * β)) = α ↑(cocycle hσ hη β) * ↑(cocycle hσ hη α)
case intro.intro
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 σ
a : ℕ
ha : σ ^ a = α
b : ℕ
hb : σ ^ b = β
⊢ ↑(cocycle hσ hη (σ ^ (a + b))) = (σ ^ a) ↑(cocycle hσ hη (σ ^ b)) * ↑(cocycle hσ hη (σ ^ a))