Theorem: is_cocycle_aux (FltRegular/NumberTheory/Hilbert90.lean)

State before:
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η α)
Tactic:
intro α β
State after:
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η α)

State before:
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η α)
Tactic:
have hσmon : ∀ x, x ∈ Submonoid.powers σ := by
  simpa [← mem_powers_iff_mem_zpowers] using hσ
State after:
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η α)

State before:
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η α)
Tactic:
obtain ⟨a, ha⟩ := (Submonoid.mem_powers_iff _ _).1 (hσmon α)
State after:
case 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 = α
⊢ ↑(cocycle hσ hη (α * β)) = α ↑(cocycle hσ hη β) * ↑(cocycle hσ hη α)

State before:
case 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 = α
⊢ ↑(cocycle hσ hη (α * β)) = α ↑(cocycle hσ hη β) * ↑(cocycle hσ hη α)
Tactic:
obtain ⟨b, hb⟩ := (Submonoid.mem_powers_iff _ _).1 (hσmon β)
State after:
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η α)

State before:
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η α)
Tactic:
rw [← ha, ← hb, ← pow_add]
State after:
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))

State before:
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))
Tactic:
have Hab := hφ (L := L) hσ (a + b)
State after:
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 σ
⊢ ↑(cocycle hσ hη (σ ^ (a + b))) = (σ ^ a) ↑(cocycle hσ hη (σ ^ b)) * ↑(cocycle hσ hη (σ ^ a))

State before:
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 σ
⊢ ↑(cocycle hσ hη (σ ^ (a + b))) = (σ ^ a) ↑(cocycle hσ hη (σ ^ b)) * ↑(cocycle hσ hη (σ ^ a))
Tactic:
have Ha := hφ (L := L) hσ a
State after:
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 σ
⊢ ↑(cocycle hσ hη (σ ^ (a + b))) = (σ ^ a) ↑(cocycle hσ hη (σ ^ b)) * ↑(cocycle hσ hη (σ ^ a))

State before:
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 σ
⊢ ↑(cocycle hσ hη (σ ^ (a + b))) = (σ ^ a) ↑(cocycle hσ hη (σ ^ b)) * ↑(cocycle hσ hη (σ ^ a))
Tactic:
have Hb := hφ (L := L) hσ b
State after:
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 σ
⊢ ↑(cocycle hσ hη (σ ^ (a + b))) = (σ ^ a) ↑(cocycle hσ hη (σ ^ b)) * ↑(cocycle hσ hη (σ ^ a))

State before:
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 σ
⊢ ↑(cocycle hσ hη (σ ^ (a + b))) = (σ ^ a) ↑(cocycle hσ hη (σ ^ b)) * ↑(cocycle hσ hη (σ ^ a))
Tactic:
simp only [SetLike.coe_sort_coe, Nat.cast_add, Fin.ext_iff, Fin.mod_val, Fin.coe_ofNat_eq_mod,
  Nat.mod_self, Nat.mod_zero, cocycle, Units.coe_prod, Units.coe_map, MonoidHom.coe_coe,
  map_prod] at Hab Ha Hb ⊢
State after:
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), ⋯⟩), (σ ^ x) ↑(ηu hη) =
    (∏ x ∈ range ↑((φ σ) ⟨σ ^ b, ⋯⟩), (σ ^ a) ((σ ^ x) ↑(ηu hη))) * ∏ x ∈ range ↑((φ σ) ⟨σ ^ a, ⋯⟩), (σ ^ x) ↑(ηu hη)

State before:
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), ⋯⟩), (σ ^ x) ↑(ηu hη) =
    (∏ x ∈ range ↑((φ σ) ⟨σ ^ b, ⋯⟩), (σ ^ a) ((σ ^ x) ↑(ηu hη))) * ∏ x ∈ range ↑((φ σ) ⟨σ ^ a, ⋯⟩), (σ ^ x) ↑(ηu hη)
Tactic:
rw [Hab, Ha, Hb, mul_comm]
State after:
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η))

State before:
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η))
Tactic:
have H : ∀ n, σ ^ (a + n) = σ ^ (a % orderOf σ + n) := fun n ↦ by simp [pow_inj_mod]
State after:
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η))

State before:
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η))
Tactic:
conv =>
  enter [2, 2, 2, x]
  rw [← AlgEquiv.mul_apply, ← pow_add, H]
State after:
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 % orderOf σ + x)) ↑(ηu hη)

State before:
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 % orderOf σ + x)) ↑(ηu hη)
Tactic:
rw [← prod_range_add (fun (n : ℕ) ↦ (σ ^ n) (ηu hη)) (a % orderOf σ) (b % orderOf σ)]
State after:
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 σ + b % orderOf σ), (σ ^ x) ↑(ηu hη)

State before:
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 σ + b % orderOf σ), (σ ^ x) ↑(ηu hη)
Tactic:
simpa using bar hσ hη (by simp)
State after:
no goals

State before:
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
⊢ ∀ (x : L ≃ₐ[K] L), x ∈ Submonoid.powers σ
Tactic:
simpa [← mem_powers_iff_mem_zpowers] using hσ
State after:
no goals

State before:
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 σ
n : ℕ
⊢ σ ^ (a + n) = σ ^ (a % orderOf σ + n)
Tactic:
simp [pow_inj_mod]
State after:
no goals

State before:
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)
⊢ (a + b) % orderOf σ % orderOf σ = (a % orderOf σ + b % orderOf σ) % orderOf σ
Tactic:
simp
State after:
no goals