internlm/Lean-Github huggingface dataset:
Theorem: cocycle_spec
Proof 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
hone : orderOf σ ≠ 1
nezero : NeZero (orderOf σ)
⊢ (orderOf σ).pred.pred + 2 = orderOf σ
Tactic:
rw [← Nat.succ_eq_add_one, ← Nat.succ_eq_add_one, Nat.succ_pred, Nat.succ_pred nezero.1]
Proof 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
hone : orderOf σ ≠ 1
nezero : NeZero (orderOf σ)
⊢ (orderOf σ).pred ≠ 0
Theorem: cocycle_spec
Proof 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
hone : orderOf σ ≠ 1
nezero : NeZero (orderOf σ)
⊢ (orderOf σ).pred ≠ 0
Tactic:
intro h
Proof 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
hone : orderOf σ ≠ 1
nezero : NeZero (orderOf σ)
h : (orderOf σ).pred = 0
⊢ False
Theorem: cocycle_spec
Proof 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
hone : orderOf σ ≠ 1
nezero : NeZero (orderOf σ)
h : (orderOf σ).pred = 0
⊢ False
Tactic:
rw [show 0 = Nat.pred 1 by rfl] at h
Proof 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
hone : orderOf σ ≠ 1
nezero : NeZero (orderOf σ)
h : (orderOf σ).pred = Nat.pred 1
⊢ False
Theorem: cocycle_spec
Proof 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
hone : orderOf σ ≠ 1
nezero : NeZero (orderOf σ)
h : (orderOf σ).pred = Nat.pred 1
⊢ False
Tactic:
apply hone
Proof 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
hone : orderOf σ ≠ 1
nezero : NeZero (orderOf σ)
h : (orderOf σ).pred = Nat.pred 1
⊢ orderOf σ = 1
Theorem: cocycle_spec
Proof 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
hone : orderOf σ ≠ 1
nezero : NeZero (orderOf σ)
h : (orderOf σ).pred = Nat.pred 1
⊢ orderOf σ = 1
Tactic:
exact Nat.pred_inj (Nat.pos_of_ne_zero nezero.1) zero_lt_one h
Proof state after:
no goals
Theorem: cocycle_spec
Proof 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
hone : orderOf σ ≠ 1
nezero : NeZero (orderOf σ)
this : (orderOf σ).pred.pred + 2 = orderOf σ
⊢ 1 % orderOf σ = 1
Tactic:
rw [← this]
Proof 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
hone : orderOf σ ≠ 1
nezero : NeZero (orderOf σ)
this : (orderOf σ).pred.pred + 2 = orderOf σ
⊢ 1 % ((orderOf σ).pred.pred + 2) = 1
Theorem: cocycle_spec
Proof 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
hone : orderOf σ ≠ 1
nezero : NeZero (orderOf σ)
this : (orderOf σ).pred.pred + 2 = orderOf σ
⊢ 1 % ((orderOf σ).pred.pred + 2) = 1
Tactic:
exact Nat.one_mod _
Proof state after:
no goals
Theorem: cocycle_spec
Proof 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
hone : orderOf σ ≠ 1
nezero : NeZero (orderOf σ)
h : (orderOf σ).pred = 0
⊢ 0 = Nat.pred 1
Tactic:
rfl
Proof state after:
no goals
Theorem: is_cocycle_aux
Proof 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 α β
Proof 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η α)
Theorem: is_cocycle_aux
Proof 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σ
Proof 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η α)
Theorem: is_cocycle_aux
Proof 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 α)
Proof 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η α)
Theorem: is_cocycle_aux
Proof 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 β)
Proof 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η α)
Theorem: is_cocycle_aux
Proof 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]
Proof 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))
Theorem: is_cocycle_aux
Proof 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)
Proof 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))
Theorem: is_cocycle_aux
Proof 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
Proof 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))
Theorem: is_cocycle_aux
Proof 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
Proof 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))
Theorem: is_cocycle_aux
Proof 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 ⊢
Proof 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η)
Theorem: is_cocycle_aux
Proof 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]
Proof 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η))
Theorem: is_cocycle_aux
Proof 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]
Proof 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η))
Theorem: is_cocycle_aux
Proof 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]
Proof 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η)
Theorem: is_cocycle_aux
Proof 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 σ)]
Proof 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η)
Theorem: is_cocycle_aux
Proof 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)
Proof state after:
no goals
Theorem: is_cocycle_aux
Proof 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σ
Proof state after:
no goals
Theorem: is_cocycle_aux
Proof 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]
Proof state after:
no goals
Theorem: is_cocycle_aux
Proof 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
Proof state after:
no goals