have : 1 % orderOf σ = 1 := by
  suffices (orderOf σ).pred.pred + 2 = orderOf σ by
    rw [← this]
    exact Nat.one_mod _
  rw [← Nat.succ_eq_add_one, ← Nat.succ_eq_add_one, Nat.succ_pred, Nat.succ_pred nezero.1]
  intro h
  rw [show 0 = Nat.pred 1 by rfl] at h
  apply hone
  exact Nat.pred_inj (Nat.pos_of_ne_zero nezero.1) zero_lt_one 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
hone : orderOf σ ≠ 1
nezero : NeZero (orderOf σ)
⊢ cocycle ⋯ ⋯ (σ ^ 1) = ηu 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
hone : orderOf σ ≠ 1
nezero : NeZero (orderOf σ)
this : 1 % orderOf σ = 1
⊢ cocycle ⋯ ⋯ (σ ^ 1) = ηu hη