internlm/Lean-Github huggingface dataset:
Theorem: foo
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
n : ℕ
ih : ∀ {a : ℕ}, a % orderOf σ = 0 → a = orderOf σ * n → ∏ i ∈ range (orderOf σ * n), (σ ^ i) ↑(ηu hη) = 1
a : ℕ
h✝ : a % orderOf σ = 0
hn✝ : a = orderOf σ * (n + 1)
this : 1 = ∏ σ : L ≃ₐ[K] L, σ η
⊢ ∀ (a : ℕ) (ha : a ∈ range (orderOf σ)), (fun n x => σ ^ n) a ha ∈ univ
Tactic:
simp
Proof state after:
no goals
Theorem: foo
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
n : ℕ
ih : ∀ {a : ℕ}, a % orderOf σ = 0 → a = orderOf σ * n → ∏ i ∈ range (orderOf σ * n), (σ ^ i) ↑(ηu hη) = 1
a : ℕ
h✝ : a % orderOf σ = 0
hn✝ : a = orderOf σ * (n + 1)
this : 1 = ∏ σ : L ≃ₐ[K] L, σ η
x✝¹ : ℕ
x✝ : x✝¹ ∈ range (orderOf σ)
⊢ (σ ^ x✝¹) ↑(ηu hη) = ((fun n x => σ ^ n) x✝¹ x✝) η
Tactic:
rfl
Proof state after:
no goals
Theorem: foo
Proof state before:
case h.e'_2.refine_1
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
n : ℕ
ih : ∀ {a : ℕ}, a % orderOf σ = 0 → a = orderOf σ * n → ∏ i ∈ range (orderOf σ * n), (σ ^ i) ↑(ηu hη) = 1
a✝ : ℕ
h✝ : a✝ % orderOf σ = 0
hn✝ : a✝ = orderOf σ * (n + 1)
this : 1 = ∏ σ : L ≃ₐ[K] L, σ η
a : ℕ
ha : a ∈ range (orderOf σ)
b : ℕ
hb : b ∈ range (orderOf σ)
hab : (fun n x => σ ^ n) a ha = (fun n x => σ ^ n) b hb
⊢ a = b
Tactic:
rwa [pow_inj_mod, Nat.mod_eq_of_lt (Finset.mem_range.1 ha),
  Nat.mod_eq_of_lt (Finset.mem_range.1 hb)] at hab
Proof state after:
no goals
Theorem: foo
Proof state before:
case h.e'_2.refine_2
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
n : ℕ
ih : ∀ {a : ℕ}, a % orderOf σ = 0 → a = orderOf σ * n → ∏ i ∈ range (orderOf σ * n), (σ ^ i) ↑(ηu hη) = 1
a : ℕ
h✝ : a % orderOf σ = 0
hn✝ : a = orderOf σ * (n + 1)
this : 1 = ∏ σ : L ≃ₐ[K] L, σ η
τ : L ≃ₐ[K] L
x✝ : τ ∈ univ
⊢ ∃ a, ∃ (ha : a ∈ range (orderOf σ)), (fun n x => σ ^ n) a ha = τ
Tactic:
refine ⟨(finEquivZPowers _ (isOfFinOrder_of_finite σ)).symm ⟨τ, hσ τ⟩, by simp, ?_⟩
Proof state after:
case h.e'_2.refine_2
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
n : ℕ
ih : ∀ {a : ℕ}, a % orderOf σ = 0 → a = orderOf σ * n → ∏ i ∈ range (orderOf σ * n), (σ ^ i) ↑(ηu hη) = 1
a : ℕ
h✝ : a % orderOf σ = 0
hn✝ : a = orderOf σ * (n + 1)
this : 1 = ∏ σ : L ≃ₐ[K] L, σ η
τ : L ≃ₐ[K] L
x✝ : τ ∈ univ
⊢ (fun n x => σ ^ n) ↑((finEquivZPowers σ ⋯).symm ⟨τ, ⋯⟩) ⋯ = τ
Theorem: foo
Proof state before:
case h.e'_2.refine_2
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
n : ℕ
ih : ∀ {a : ℕ}, a % orderOf σ = 0 → a = orderOf σ * n → ∏ i ∈ range (orderOf σ * n), (σ ^ i) ↑(ηu hη) = 1
a : ℕ
h✝ : a % orderOf σ = 0
hn✝ : a = orderOf σ * (n + 1)
this : 1 = ∏ σ : L ≃ₐ[K] L, σ η
τ : L ≃ₐ[K] L
x✝ : τ ∈ univ
⊢ (fun n x => σ ^ n) ↑((finEquivZPowers σ ⋯).symm ⟨τ, ⋯⟩) ⋯ = τ
Tactic:
have := Equiv.symm_apply_apply (finEquivZPowers _ (isOfFinOrder_of_finite σ)).symm ⟨τ, hσ τ⟩
Proof state after:
case h.e'_2.refine_2
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
n : ℕ
ih : ∀ {a : ℕ}, a % orderOf σ = 0 → a = orderOf σ * n → ∏ i ∈ range (orderOf σ * n), (σ ^ i) ↑(ηu hη) = 1
a : ℕ
h✝ : a % orderOf σ = 0
hn✝ : a = orderOf σ * (n + 1)
this✝ : 1 = ∏ σ : L ≃ₐ[K] L, σ η
τ : L ≃ₐ[K] L
x✝ : τ ∈ univ
this : (finEquivZPowers σ ⋯).symm.symm ((finEquivZPowers σ ⋯).symm ⟨τ, ⋯⟩) = ⟨τ, ⋯⟩
⊢ (fun n x => σ ^ n) ↑((finEquivZPowers σ ⋯).symm ⟨τ, ⋯⟩) ⋯ = τ
Theorem: foo
Proof state before:
case h.e'_2.refine_2
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
n : ℕ
ih : ∀ {a : ℕ}, a % orderOf σ = 0 → a = orderOf σ * n → ∏ i ∈ range (orderOf σ * n), (σ ^ i) ↑(ηu hη) = 1
a : ℕ
h✝ : a % orderOf σ = 0
hn✝ : a = orderOf σ * (n + 1)
this✝ : 1 = ∏ σ : L ≃ₐ[K] L, σ η
τ : L ≃ₐ[K] L
x✝ : τ ∈ univ
this : (finEquivZPowers σ ⋯).symm.symm ((finEquivZPowers σ ⋯).symm ⟨τ, ⋯⟩) = ⟨τ, ⋯⟩
⊢ (fun n x => σ ^ n) ↑((finEquivZPowers σ ⋯).symm ⟨τ, ⋯⟩) ⋯ = τ
Tactic:
simp only [SetLike.coe_sort_coe, Equiv.symm_symm, ← Subtype.coe_inj] at this ⊢
Proof state after:
case h.e'_2.refine_2
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
n : ℕ
ih : ∀ {a : ℕ}, a % orderOf σ = 0 → a = orderOf σ * n → ∏ i ∈ range (orderOf σ * n), (σ ^ i) ↑(ηu hη) = 1
a : ℕ
h✝ : a % orderOf σ = 0
hn✝ : a = orderOf σ * (n + 1)
this✝ : 1 = ∏ σ : L ≃ₐ[K] L, σ η
τ : L ≃ₐ[K] L
x✝ : τ ∈ univ
this : ↑((finEquivZPowers σ ⋯) ((finEquivZPowers σ ⋯).symm ⟨τ, ⋯⟩)) = τ
⊢ σ ^ ↑((finEquivZPowers σ ⋯).symm ⟨τ, ⋯⟩) = τ
Theorem: foo
Proof state before:
case h.e'_2.refine_2
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
n : ℕ
ih : ∀ {a : ℕ}, a % orderOf σ = 0 → a = orderOf σ * n → ∏ i ∈ range (orderOf σ * n), (σ ^ i) ↑(ηu hη) = 1
a : ℕ
h✝ : a % orderOf σ = 0
hn✝ : a = orderOf σ * (n + 1)
this✝ : 1 = ∏ σ : L ≃ₐ[K] L, σ η
τ : L ≃ₐ[K] L
x✝ : τ ∈ univ
this : ↑((finEquivZPowers σ ⋯) ((finEquivZPowers σ ⋯).symm ⟨τ, ⋯⟩)) = τ
⊢ σ ^ ↑((finEquivZPowers σ ⋯).symm ⟨τ, ⋯⟩) = τ
Tactic:
rw [← this]
Proof state after:
case h.e'_2.refine_2
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
n : ℕ
ih : ∀ {a : ℕ}, a % orderOf σ = 0 → a = orderOf σ * n → ∏ i ∈ range (orderOf σ * n), (σ ^ i) ↑(ηu hη) = 1
a : ℕ
h✝ : a % orderOf σ = 0
hn✝ : a = orderOf σ * (n + 1)
this✝ : 1 = ∏ σ : L ≃ₐ[K] L, σ η
τ : L ≃ₐ[K] L
x✝ : τ ∈ univ
this : ↑((finEquivZPowers σ ⋯) ((finEquivZPowers σ ⋯).symm ⟨τ, ⋯⟩)) = τ
⊢ σ ^ ↑((finEquivZPowers σ ⋯).symm ⟨↑((finEquivZPowers σ ⋯) ((finEquivZPowers σ ⋯).symm ⟨τ, ⋯⟩)), ⋯⟩) =
    ↑((finEquivZPowers σ ⋯) ((finEquivZPowers σ ⋯).symm ⟨τ, ⋯⟩))
Theorem: foo
Proof state before:
case h.e'_2.refine_2
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
n : ℕ
ih : ∀ {a : ℕ}, a % orderOf σ = 0 → a = orderOf σ * n → ∏ i ∈ range (orderOf σ * n), (σ ^ i) ↑(ηu hη) = 1
a : ℕ
h✝ : a % orderOf σ = 0
hn✝ : a = orderOf σ * (n + 1)
this✝ : 1 = ∏ σ : L ≃ₐ[K] L, σ η
τ : L ≃ₐ[K] L
x✝ : τ ∈ univ
this : ↑((finEquivZPowers σ ⋯) ((finEquivZPowers σ ⋯).symm ⟨τ, ⋯⟩)) = τ
⊢ σ ^ ↑((finEquivZPowers σ ⋯).symm ⟨↑((finEquivZPowers σ ⋯) ((finEquivZPowers σ ⋯).symm ⟨τ, ⋯⟩)), ⋯⟩) =
    ↑((finEquivZPowers σ ⋯) ((finEquivZPowers σ ⋯).symm ⟨τ, ⋯⟩))
Tactic:
simp only [SetLike.coe_sort_coe, Subtype.coe_eta, Equiv.symm_apply_apply]
Proof state after:
case h.e'_2.refine_2
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
n : ℕ
ih : ∀ {a : ℕ}, a % orderOf σ = 0 → a = orderOf σ * n → ∏ i ∈ range (orderOf σ * n), (σ ^ i) ↑(ηu hη) = 1
a : ℕ
h✝ : a % orderOf σ = 0
hn✝ : a = orderOf σ * (n + 1)
this✝ : 1 = ∏ σ : L ≃ₐ[K] L, σ η
τ : L ≃ₐ[K] L
x✝ : τ ∈ univ
this : ↑((finEquivZPowers σ ⋯) ((finEquivZPowers σ ⋯).symm ⟨τ, ⋯⟩)) = τ
⊢ σ ^ ↑((finEquivZPowers σ ⋯).symm ⟨τ, ⋯⟩) = ↑((finEquivZPowers σ ⋯) ((finEquivZPowers σ ⋯).symm ⟨τ, ⋯⟩))
Theorem: foo
Proof state before:
case h.e'_2.refine_2
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
n : ℕ
ih : ∀ {a : ℕ}, a % orderOf σ = 0 → a = orderOf σ * n → ∏ i ∈ range (orderOf σ * n), (σ ^ i) ↑(ηu hη) = 1
a : ℕ
h✝ : a % orderOf σ = 0
hn✝ : a = orderOf σ * (n + 1)
this✝ : 1 = ∏ σ : L ≃ₐ[K] L, σ η
τ : L ≃ₐ[K] L
x✝ : τ ∈ univ
this : ↑((finEquivZPowers σ ⋯) ((finEquivZPowers σ ⋯).symm ⟨τ, ⋯⟩)) = τ
⊢ σ ^ ↑((finEquivZPowers σ ⋯).symm ⟨τ, ⋯⟩) = ↑((finEquivZPowers σ ⋯) ((finEquivZPowers σ ⋯).symm ⟨τ, ⋯⟩))
Tactic:
rfl
Proof state after:
no goals
Theorem: foo
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
n : ℕ
ih : ∀ {a : ℕ}, a % orderOf σ = 0 → a = orderOf σ * n → ∏ i ∈ range (orderOf σ * n), (σ ^ i) ↑(ηu hη) = 1
a : ℕ
h✝ : a % orderOf σ = 0
hn✝ : a = orderOf σ * (n + 1)
this : 1 = ∏ σ : L ≃ₐ[K] L, σ η
τ : L ≃ₐ[K] L
x✝ : τ ∈ univ
⊢ ↑((finEquivZPowers σ ⋯).symm ⟨τ, ⋯⟩) ∈ range (orderOf σ)
Tactic:
simp
Proof state after:
no goals
Theorem: bar
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
a b : ℕ
h : a % orderOf σ = b % orderOf σ
⊢ ∏ i ∈ range a, (σ ^ i) ↑(ηu hη) = ∏ i ∈ range b, (σ ^ i) ↑(ηu hη)
Tactic:
wlog hab : b ≤ a generalizing a b
Proof state after:
case inr
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
a b : ℕ
h : a % orderOf σ = b % orderOf σ
this :
  ∀ {a b : ℕ}, a % orderOf σ = b % orderOf σ → b ≤ a → ∏ i ∈ range a, (σ ^ i) ↑(ηu hη) = ∏ i ∈ range b, (σ ^ i) ↑(ηu hη)
hab : ¬b ≤ a
⊢ ∏ i ∈ range a, (σ ^ i) ↑(ηu hη) = ∏ i ∈ range b, (σ ^ i) ↑(η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
a b : ℕ
h : a % orderOf σ = b % orderOf σ
hab : b ≤ a
⊢ ∏ i ∈ range a, (σ ^ i) ↑(ηu hη) = ∏ i ∈ range b, (σ ^ i) ↑(ηu hη)
Theorem: bar
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
a b : ℕ
h : a % orderOf σ = b % orderOf σ
hab : b ≤ a
⊢ ∏ i ∈ range a, (σ ^ i) ↑(ηu hη) = ∏ i ∈ range b, (σ ^ i) ↑(ηu hη)
Tactic:
obtain ⟨c, hc⟩ := (Nat.dvd_iff_mod_eq_zero _ _).2 (Nat.sub_mod_eq_zero_of_mod_eq h)
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
a b : ℕ
h : a % orderOf σ = b % orderOf σ
hab : b ≤ a
c : ℕ
hc : a - b = orderOf σ * c
⊢ ∏ i ∈ range a, (σ ^ i) ↑(ηu hη) = ∏ i ∈ range b, (σ ^ i) ↑(ηu hη)
Theorem: bar
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
a b : ℕ
h : a % orderOf σ = b % orderOf σ
hab : b ≤ a
c : ℕ
hc : a - b = orderOf σ * c
⊢ ∏ i ∈ range a, (σ ^ i) ↑(ηu hη) = ∏ i ∈ range b, (σ ^ i) ↑(ηu hη)
Tactic:
rw [Nat.sub_eq_iff_eq_add hab] at hc
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
a b : ℕ
h : a % orderOf σ = b % orderOf σ
hab : b ≤ a
c : ℕ
hc : a = orderOf σ * c + b
⊢ ∏ i ∈ range a, (σ ^ i) ↑(ηu hη) = ∏ i ∈ range b, (σ ^ i) ↑(ηu hη)
Theorem: bar
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
a b : ℕ
h : a % orderOf σ = b % orderOf σ
hab : b ≤ a
c : ℕ
hc : a = orderOf σ * c + b
⊢ ∏ i ∈ range a, (σ ^ i) ↑(ηu hη) = ∏ i ∈ range b, (σ ^ i) ↑(ηu hη)
Tactic:
rw [hc, prod_range_add]
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
a b : ℕ
h : a % orderOf σ = b % orderOf σ
hab : b ≤ a
c : ℕ
hc : a = orderOf σ * c + b
⊢ (∏ x ∈ range (orderOf σ * c), (σ ^ x) ↑(ηu hη)) * ∏ x ∈ range b, (σ ^ (orderOf σ * c + x)) ↑(ηu hη) =
    ∏ i ∈ range b, (σ ^ i) ↑(ηu hη)
Theorem: bar
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
a b : ℕ
h : a % orderOf σ = b % orderOf σ
hab : b ≤ a
c : ℕ
hc : a = orderOf σ * c + b
⊢ (∏ x ∈ range (orderOf σ * c), (σ ^ x) ↑(ηu hη)) * ∏ x ∈ range b, (σ ^ (orderOf σ * c + x)) ↑(ηu hη) =
    ∏ i ∈ range b, (σ ^ i) ↑(ηu hη)
Tactic:
rw [foo hσ hη (Nat.mul_mod_right (orderOf σ) c), one_mul]
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
a b : ℕ
h : a % orderOf σ = b % orderOf σ
hab : b ≤ a
c : ℕ
hc : a = orderOf σ * c + b
⊢ ∏ x ∈ range b, (σ ^ (orderOf σ * c + x)) ↑(ηu hη) = ∏ i ∈ range b, (σ ^ i) ↑(ηu hη)
Theorem: bar
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
a b : ℕ
h : a % orderOf σ = b % orderOf σ
hab : b ≤ a
c : ℕ
hc : a = orderOf σ * c + b
⊢ ∏ x ∈ range b, (σ ^ (orderOf σ * c + x)) ↑(ηu hη) = ∏ i ∈ range b, (σ ^ i) ↑(ηu hη)
Tactic:
simp [pow_add, pow_mul, pow_orderOf_eq_one]
Proof state after:
no goals
Theorem: bar
Proof state before:
case inr
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
a b : ℕ
h : a % orderOf σ = b % orderOf σ
this :
  ∀ {a b : ℕ}, a % orderOf σ = b % orderOf σ → b ≤ a → ∏ i ∈ range a, (σ ^ i) ↑(ηu hη) = ∏ i ∈ range b, (σ ^ i) ↑(ηu hη)
hab : ¬b ≤ a
⊢ ∏ i ∈ range a, (σ ^ i) ↑(ηu hη) = ∏ i ∈ range b, (σ ^ i) ↑(ηu hη)
Tactic:
exact (this h.symm (not_le.1 hab).le).symm
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
⊢ cocycle hσ hη σ = ηu hη
Tactic:
haveI nezero : NeZero (orderOf σ) :=
  ⟨fun hzero ↦ orderOf_eq_zero_iff.1 hzero (isOfFinOrder_of_finite σ)⟩
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 σ)
⊢ cocycle hσ hη σ = ηu hη
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 σ)
⊢ cocycle hσ hη σ = ηu hη
Tactic:
conv =>
  enter [1, 3]
  rw [← pow_one σ]
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 σ)
⊢ cocycle ⋯ ⋯ (σ ^ 1) = ηu hη
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 σ)
⊢ cocycle ⋯ ⋯ (σ ^ 1) = ηu hη
Tactic:
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
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 : 1 % orderOf σ = 1
⊢ cocycle ⋯ ⋯ (σ ^ 1) = ηu hη
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 : 1 % orderOf σ = 1
⊢ cocycle ⋯ ⋯ (σ ^ 1) = ηu hη
Tactic:
simp [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 : 1 % orderOf σ = 1
⊢ cocycle hσ hη σ = ηu hη
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 : 1 % orderOf σ = 1
⊢ cocycle hσ hη σ = ηu hη
Tactic:
have horder :=  hφ hσ 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 σ)
this : 1 % orderOf σ = 1
horder : ↑((φ σ) ⟨σ ^ 1, ⋯⟩) = 1 % orderOf σ
⊢ cocycle hσ hη σ = ηu hη
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 : 1 % orderOf σ = 1
horder : ↑((φ σ) ⟨σ ^ 1, ⋯⟩) = 1 % orderOf σ
⊢ cocycle hσ hη σ = ηu hη
Tactic:
simp only [SetLike.coe_sort_coe, pow_one] at horder
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 : 1 % orderOf σ = 1
horder : ↑((φ σ) ⟨σ, ⋯⟩) = 1 % orderOf σ
⊢ cocycle hσ hη σ = ηu hη
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 : 1 % orderOf σ = 1
horder : ↑((φ σ) ⟨σ, ⋯⟩) = 1 % orderOf σ
⊢ cocycle hσ hη σ = ηu hη
Tactic:
simp only [cocycle, SetLike.coe_sort_coe, horder, this, range_one, prod_singleton, pow_zero]
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 : 1 % orderOf σ = 1
horder : ↑((φ σ) ⟨σ, ⋯⟩) = 1 % orderOf σ
⊢ (Units.map ↑1) (ηu hη) = ηu hη
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 : 1 % orderOf σ = 1
horder : ↑((φ σ) ⟨σ, ⋯⟩) = 1 % orderOf σ
⊢ (Units.map ↑1) (ηu hη) = ηu hη
Tactic:
rfl
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 σ)
⊢ 1 % orderOf σ = 1
Tactic:
suffices (orderOf σ).pred.pred + 2 = orderOf σ by
  rw [← this]
  exact Nat.one_mod _
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.pred + 2 = orderOf σ