Theorem: bar (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
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
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η)

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)
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η)

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
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η)

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]
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η)

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]
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η)

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]
State after:
no goals

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
State after:
no goals