Theorem: foo (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 : ℕ
h : a % orderOf σ = 0
⊢ ∏ i ∈ range a, (σ ^ i) ↑(ηu hη) = 1
Tactic:
obtain ⟨n, hn⟩ := (Nat.dvd_iff_mod_eq_zero _ _).2 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 : ℕ
h : a % orderOf σ = 0
n : ℕ
hn : a = orderOf σ * n
⊢ ∏ i ∈ range a, (σ ^ i) ↑(ηu hη) = 1

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 : ℕ
h : a % orderOf σ = 0
n : ℕ
hn : a = orderOf σ * n
⊢ ∏ i ∈ range a, (σ ^ i) ↑(ηu hη) = 1
Tactic:
rw [hn]
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 : ℕ
h : a % orderOf σ = 0
n : ℕ
hn : a = orderOf σ * n
⊢ ∏ i ∈ range (orderOf σ * n), (σ ^ i) ↑(ηu hη) = 1

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 : ℕ
h : a % orderOf σ = 0
n : ℕ
hn : a = orderOf σ * n
⊢ ∏ i ∈ range (orderOf σ * n), (σ ^ i) ↑(ηu hη) = 1
Tactic:
revert a
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
n : ℕ
⊢ ∀ {a : ℕ}, a % orderOf σ = 0 → a = orderOf σ * n → ∏ i ∈ range (orderOf σ * n), (σ ^ i) ↑(ηu hη) = 1

State before:
case intro.zero
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 : ℕ}, a % orderOf σ = 0 → a = orderOf σ * 0 → ∏ i ∈ range (orderOf σ * 0), (σ ^ i) ↑(ηu hη) = 1
Tactic:
simp
State after:
no goals

State before:
case intro.succ
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 : ℕ}, a % orderOf σ = 0 → a = orderOf σ * (n + 1) → ∏ i ∈ range (orderOf σ * (n + 1)), (σ ^ i) ↑(ηu hη) = 1
Tactic:
intro a _ _
State after:
case intro.succ
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)
⊢ ∏ i ∈ range (orderOf σ * (n + 1)), (σ ^ i) ↑(ηu hη) = 1

State before:
case intro.succ
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)
⊢ ∏ i ∈ range (orderOf σ * (n + 1)), (σ ^ i) ↑(ηu hη) = 1
Tactic:
rw [Nat.mul_succ, prod_range_add, ih (Nat.mul_mod_right (orderOf σ) n) rfl, one_mul]
State after:
case intro.succ
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)
⊢ ∏ x ∈ range (orderOf σ), (σ ^ (orderOf σ * n + x)) ↑(ηu hη) = 1

State before:
case intro.succ
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)
⊢ ∏ x ∈ range (orderOf σ), (σ ^ (orderOf σ * n + x)) ↑(ηu hη) = 1
Tactic:
simp only [pow_add, pow_mul, pow_orderOf_eq_one, one_pow, one_mul]
State after:
case intro.succ
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)
⊢ ∏ x ∈ range (orderOf σ), (σ ^ x) ↑(ηu hη) = 1

State before:
case intro.succ
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)
⊢ ∏ x ∈ range (orderOf σ), (σ ^ x) ↑(ηu hη) = 1
Tactic:
have := Algebra.norm_eq_prod_automorphisms K η
State after:
case intro.succ
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 : (algebraMap K L) ((Algebra.norm K) η) = ∏ σ : L ≃ₐ[K] L, σ η
⊢ ∏ x ∈ range (orderOf σ), (σ ^ x) ↑(ηu hη) = 1

State before:
case intro.succ
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 : (algebraMap K L) ((Algebra.norm K) η) = ∏ σ : L ≃ₐ[K] L, σ η
⊢ ∏ x ∈ range (orderOf σ), (σ ^ x) ↑(ηu hη) = 1
Tactic:
simp only [hη, map_one] at this
State after:
case intro.succ
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 ∈ range (orderOf σ), (σ ^ x) ↑(ηu hη) = 1

State before:
case intro.succ
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 ∈ range (orderOf σ), (σ ^ x) ↑(ηu hη) = 1
Tactic:
convert this.symm
State after:
case h.e'_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, σ η
⊢ ∏ x ∈ range (orderOf σ), (σ ^ x) ↑(ηu hη) = ∏ σ : L ≃ₐ[K] L, σ η

State before:
case h.e'_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, σ η
⊢ ∏ x ∈ range (orderOf σ), (σ ^ x) ↑(ηu hη) = ∏ σ : L ≃ₐ[K] L, σ η
Tactic:
refine prod_bij (fun (n : ℕ) (_ : n ∈ range (orderOf σ)) ↦ σ ^ n) (by simp)
  (fun a ha b hb hab ↦ ?_) (fun τ _ ↦ ?_) (fun _ _ ↦ by rfl)
State after:
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

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 = τ

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

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

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, ?_⟩
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 ⟨τ, ⋯⟩) ⋯ = τ

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σ τ⟩
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 ⟨τ, ⋯⟩) ⋯ = τ

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 ⊢
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 ⟨τ, ⋯⟩) = τ

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]
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 ⟨τ, ⋯⟩))

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]
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 ⟨τ, ⋯⟩))

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