have H : ∀ n, σ ^ (a + n) = σ ^ (a % orderOf σ + n) := fun n ↦ by simp [pow_inj_mod]
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 = β
Hab : ↑((φ σ) ⟨σ ^ (a + b), ⋯⟩) = (a + b) % orderOf σ
Ha : ↑((φ σ) ⟨σ ^ a, ⋯⟩) = a % orderOf σ
Hb : ↑((φ σ) ⟨σ ^ b, ⋯⟩) = b % orderOf σ
⊢ ∏ x ∈ range ((a + b) % orderOf σ), (σ ^ x) ↑(ηu hη) =
    (∏ x ∈ range (a % orderOf σ), (σ ^ x) ↑(ηu hη)) * ∏ x ∈ range (b % orderOf σ), (σ ^ a) ((σ ^ x) ↑(ηu 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 = β
Hab : ↑((φ σ) ⟨σ ^ (a + b), ⋯⟩) = (a + b) % orderOf σ
Ha : ↑((φ σ) ⟨σ ^ a, ⋯⟩) = a % orderOf σ
Hb : ↑((φ σ) ⟨σ ^ b, ⋯⟩) = b % orderOf σ
H : ∀ (n : ℕ), σ ^ (a + n) = σ ^ (a % orderOf σ + n)
⊢ ∏ x ∈ range ((a + b) % orderOf σ), (σ ^ x) ↑(ηu hη) =
    (∏ x ∈ range (a % orderOf σ), (σ ^ x) ↑(ηu hη)) * ∏ x ∈ range (b % orderOf σ), (σ ^ a) ((σ ^ x) ↑(ηu hη))