Theorem: Hilbert92ish_aux2 (FltRegular/NumberTheory/Hilbert92.lean)

State before:
p : ℕ+
K : Type u_1
inst✝¹³ : Field K
inst✝¹² : NumberField K
k : Type u_2
inst✝¹¹ : Field k
inst✝¹⁰ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝⁹ : AddCommGroup G
inst✝⁸ : CommGroup H
inst✝⁷ : Fintype H
hCard : Fintype.card H = ↑p
σ✝ : H
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r : ℕ
inst✝⁶ : DistribMulAction H G
inst✝⁵ : Module.Free ℤ G
inst✝⁴ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝³ : Algebra k K
inst✝² : IsGalois k K
inst✝¹ : FiniteDimensional k K
inst✝ : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
E : (𝓞 K)ˣ
ζ : k
hE : (algebraMap k K) ζ = (algebraMap (𝓞 K) K) ↑E / σ ((algebraMap (𝓞 K) K) ↑E)
hζ : ζ ^ ↑p = 1
hpodd : ↑p ≠ 2
⊢ (algebraMap k K) ((Algebra.norm k) ((algebraMap (𝓞 K) K) ↑E)) = (algebraMap (𝓞 K) K) ↑E ^ ↑p
Tactic:
have h1 : ∀ (i : ℕ), (σ ^ i) E = ((algebraMap k K ζ)⁻¹)^i * E := by
  intro i
  induction i with
  | zero =>
    simp only [pow_zero, AlgEquiv.one_apply, one_mul]
  | succ n ih =>
    rw [pow_succ', AlgEquiv.mul_apply, ih, pow_succ']
    simp only [inv_pow, map_mul, map_inv₀, map_pow, AlgEquiv.commutes]
    have h0 : (algebraMap k K) ζ ≠ 0 := fun h ↦ by simp [(map_eq_zero _).1 h] at hζ
    field_simp [h0]
    rw [← mul_assoc]
    congr
    rw [hE]
    field_simp
State after:
p : ℕ+
K : Type u_1
inst✝¹³ : Field K
inst✝¹² : NumberField K
k : Type u_2
inst✝¹¹ : Field k
inst✝¹⁰ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝⁹ : AddCommGroup G
inst✝⁸ : CommGroup H
inst✝⁷ : Fintype H
hCard : Fintype.card H = ↑p
σ✝ : H
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r : ℕ
inst✝⁶ : DistribMulAction H G
inst✝⁵ : Module.Free ℤ G
inst✝⁴ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝³ : Algebra k K
inst✝² : IsGalois k K
inst✝¹ : FiniteDimensional k K
inst✝ : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
E : (𝓞 K)ˣ
ζ : k
hE : (algebraMap k K) ζ = (algebraMap (𝓞 K) K) ↑E / σ ((algebraMap (𝓞 K) K) ↑E)
hζ : ζ ^ ↑p = 1
hpodd : ↑p ≠ 2
h1 : ∀ (i : ℕ), (σ ^ i) ((algebraMap (𝓞 K) K) ↑E) = ((algebraMap k K) ζ)⁻¹ ^ i * (algebraMap (𝓞 K) K) ↑E
⊢ (algebraMap k K) ((Algebra.norm k) ((algebraMap (𝓞 K) K) ↑E)) = (algebraMap (𝓞 K) K) ↑E ^ ↑p

State before:
p : ℕ+
K : Type u_1
inst✝¹³ : Field K
inst✝¹² : NumberField K
k : Type u_2
inst✝¹¹ : Field k
inst✝¹⁰ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝⁹ : AddCommGroup G
inst✝⁸ : CommGroup H
inst✝⁷ : Fintype H
hCard : Fintype.card H = ↑p
σ✝ : H
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r : ℕ
inst✝⁶ : DistribMulAction H G
inst✝⁵ : Module.Free ℤ G
inst✝⁴ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝³ : Algebra k K
inst✝² : IsGalois k K
inst✝¹ : FiniteDimensional k K
inst✝ : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
E : (𝓞 K)ˣ
ζ : k
hE : (algebraMap k K) ζ = (algebraMap (𝓞 K) K) ↑E / σ ((algebraMap (𝓞 K) K) ↑E)
hζ : ζ ^ ↑p = 1
hpodd : ↑p ≠ 2
h1 : ∀ (i : ℕ), (σ ^ i) ((algebraMap (𝓞 K) K) ↑E) = ((algebraMap k K) ζ)⁻¹ ^ i * (algebraMap (𝓞 K) K) ↑E
⊢ (algebraMap k K) ((Algebra.norm k) ((algebraMap (𝓞 K) K) ↑E)) = (algebraMap (𝓞 K) K) ↑E ^ ↑p
Tactic:
rw [norm_eq_prod_pow_gen σ hσ, orderOf_eq_card_of_forall_mem_zpowers hσ,
  IsGalois.card_aut_eq_finrank, hKL]
State after:
p : ℕ+
K : Type u_1
inst✝¹³ : Field K
inst✝¹² : NumberField K
k : Type u_2
inst✝¹¹ : Field k
inst✝¹⁰ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝⁹ : AddCommGroup G
inst✝⁸ : CommGroup H
inst✝⁷ : Fintype H
hCard : Fintype.card H = ↑p
σ✝ : H
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r : ℕ
inst✝⁶ : DistribMulAction H G
inst✝⁵ : Module.Free ℤ G
inst✝⁴ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝³ : Algebra k K
inst✝² : IsGalois k K
inst✝¹ : FiniteDimensional k K
inst✝ : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
E : (𝓞 K)ˣ
ζ : k
hE : (algebraMap k K) ζ = (algebraMap (𝓞 K) K) ↑E / σ ((algebraMap (𝓞 K) K) ↑E)
hζ : ζ ^ ↑p = 1
hpodd : ↑p ≠ 2
h1 : ∀ (i : ℕ), (σ ^ i) ((algebraMap (𝓞 K) K) ↑E) = ((algebraMap k K) ζ)⁻¹ ^ i * (algebraMap (𝓞 K) K) ↑E
⊢ ∏ i ∈ range ↑p, (σ ^ i) ((algebraMap (𝓞 K) K) ↑E) = (algebraMap (𝓞 K) K) ↑E ^ ↑p

State before:
p : ℕ+
K : Type u_1
inst✝¹³ : Field K
inst✝¹² : NumberField K
k : Type u_2
inst✝¹¹ : Field k
inst✝¹⁰ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝⁹ : AddCommGroup G
inst✝⁸ : CommGroup H
inst✝⁷ : Fintype H
hCard : Fintype.card H = ↑p
σ✝ : H
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r : ℕ
inst✝⁶ : DistribMulAction H G
inst✝⁵ : Module.Free ℤ G
inst✝⁴ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝³ : Algebra k K
inst✝² : IsGalois k K
inst✝¹ : FiniteDimensional k K
inst✝ : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
E : (𝓞 K)ˣ
ζ : k
hE : (algebraMap k K) ζ = (algebraMap (𝓞 K) K) ↑E / σ ((algebraMap (𝓞 K) K) ↑E)
hζ : ζ ^ ↑p = 1
hpodd : ↑p ≠ 2
h1 : ∀ (i : ℕ), (σ ^ i) ((algebraMap (𝓞 K) K) ↑E) = ((algebraMap k K) ζ)⁻¹ ^ i * (algebraMap (𝓞 K) K) ↑E
⊢ ∏ i ∈ range ↑p, (σ ^ i) ((algebraMap (𝓞 K) K) ↑E) = (algebraMap (𝓞 K) K) ↑E ^ ↑p
Tactic:
conv =>
  enter [1, 2, i]
  rw [h1 i, mul_comm]
State after:
p : ℕ+
K : Type u_1
inst✝¹³ : Field K
inst✝¹² : NumberField K
k : Type u_2
inst✝¹¹ : Field k
inst✝¹⁰ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝⁹ : AddCommGroup G
inst✝⁸ : CommGroup H
inst✝⁷ : Fintype H
hCard : Fintype.card H = ↑p
σ✝ : H
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r : ℕ
inst✝⁶ : DistribMulAction H G
inst✝⁵ : Module.Free ℤ G
inst✝⁴ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝³ : Algebra k K
inst✝² : IsGalois k K
inst✝¹ : FiniteDimensional k K
inst✝ : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
E : (𝓞 K)ˣ
ζ : k
hE : (algebraMap k K) ζ = (algebraMap (𝓞 K) K) ↑E / σ ((algebraMap (𝓞 K) K) ↑E)
hζ : ζ ^ ↑p = 1
hpodd : ↑p ≠ 2
h1 : ∀ (i : ℕ), (σ ^ i) ((algebraMap (𝓞 K) K) ↑E) = ((algebraMap k K) ζ)⁻¹ ^ i * (algebraMap (𝓞 K) K) ↑E
⊢ ∏ i ∈ range ↑p, (algebraMap (𝓞 K) K) ↑E * ((algebraMap k K) ζ)⁻¹ ^ i = (algebraMap (𝓞 K) K) ↑E ^ ↑p

State before:
p : ℕ+
K : Type u_1
inst✝¹³ : Field K
inst✝¹² : NumberField K
k : Type u_2
inst✝¹¹ : Field k
inst✝¹⁰ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝⁹ : AddCommGroup G
inst✝⁸ : CommGroup H
inst✝⁷ : Fintype H
hCard : Fintype.card H = ↑p
σ✝ : H
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r : ℕ
inst✝⁶ : DistribMulAction H G
inst✝⁵ : Module.Free ℤ G
inst✝⁴ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝³ : Algebra k K
inst✝² : IsGalois k K
inst✝¹ : FiniteDimensional k K
inst✝ : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
E : (𝓞 K)ˣ
ζ : k
hE : (algebraMap k K) ζ = (algebraMap (𝓞 K) K) ↑E / σ ((algebraMap (𝓞 K) K) ↑E)
hζ : ζ ^ ↑p = 1
hpodd : ↑p ≠ 2
h1 : ∀ (i : ℕ), (σ ^ i) ((algebraMap (𝓞 K) K) ↑E) = ((algebraMap k K) ζ)⁻¹ ^ i * (algebraMap (𝓞 K) K) ↑E
⊢ ∏ i ∈ range ↑p, (algebraMap (𝓞 K) K) ↑E * ((algebraMap k K) ζ)⁻¹ ^ i = (algebraMap (𝓞 K) K) ↑E ^ ↑p
Tactic:
rw [prod_mul_distrib, prod_const, card_range, prod_pow_eq_pow_sum, inv_pow, mul_eq_left₀,
  inv_eq_one, sum_range_id, Nat.mul_div_assoc, pow_mul, ← map_pow, hζ, map_one, one_pow]
State after:
case H
p : ℕ+
K : Type u_1
inst✝¹³ : Field K
inst✝¹² : NumberField K
k : Type u_2
inst✝¹¹ : Field k
inst✝¹⁰ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝⁹ : AddCommGroup G
inst✝⁸ : CommGroup H
inst✝⁷ : Fintype H
hCard : Fintype.card H = ↑p
σ✝ : H
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r : ℕ
inst✝⁶ : DistribMulAction H G
inst✝⁵ : Module.Free ℤ G
inst✝⁴ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝³ : Algebra k K
inst✝² : IsGalois k K
inst✝¹ : FiniteDimensional k K
inst✝ : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
E : (𝓞 K)ˣ
ζ : k
hE : (algebraMap k K) ζ = (algebraMap (𝓞 K) K) ↑E / σ ((algebraMap (𝓞 K) K) ↑E)
hζ : ζ ^ ↑p = 1
hpodd : ↑p ≠ 2
h1 : ∀ (i : ℕ), (σ ^ i) ((algebraMap (𝓞 K) K) ↑E) = ((algebraMap k K) ζ)⁻¹ ^ i * (algebraMap (𝓞 K) K) ↑E
⊢ 2 ∣ ↑p - 1

p : ℕ+
K : Type u_1
inst✝¹³ : Field K
inst✝¹² : NumberField K
k : Type u_2
inst✝¹¹ : Field k
inst✝¹⁰ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝⁹ : AddCommGroup G
inst✝⁸ : CommGroup H
inst✝⁷ : Fintype H
hCard : Fintype.card H = ↑p
σ✝ : H
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r : ℕ
inst✝⁶ : DistribMulAction H G
inst✝⁵ : Module.Free ℤ G
inst✝⁴ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝³ : Algebra k K
inst✝² : IsGalois k K
inst✝¹ : FiniteDimensional k K
inst✝ : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
E : (𝓞 K)ˣ
ζ : k
hE : (algebraMap k K) ζ = (algebraMap (𝓞 K) K) ↑E / σ ((algebraMap (𝓞 K) K) ↑E)
hζ : ζ ^ ↑p = 1
hpodd : ↑p ≠ 2
h1 : ∀ (i : ℕ), (σ ^ i) ((algebraMap (𝓞 K) K) ↑E) = ((algebraMap k K) ζ)⁻¹ ^ i * (algebraMap (𝓞 K) K) ↑E
⊢ (algebraMap (𝓞 K) K) ↑E ^ ↑p ≠ 0

State before:
p : ℕ+
K : Type u_1
inst✝¹³ : Field K
inst✝¹² : NumberField K
k : Type u_2
inst✝¹¹ : Field k
inst✝¹⁰ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝⁹ : AddCommGroup G
inst✝⁸ : CommGroup H
inst✝⁷ : Fintype H
hCard : Fintype.card H = ↑p
σ✝ : H
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r : ℕ
inst✝⁶ : DistribMulAction H G
inst✝⁵ : Module.Free ℤ G
inst✝⁴ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝³ : Algebra k K
inst✝² : IsGalois k K
inst✝¹ : FiniteDimensional k K
inst✝ : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
E : (𝓞 K)ˣ
ζ : k
hE : (algebraMap k K) ζ = (algebraMap (𝓞 K) K) ↑E / σ ((algebraMap (𝓞 K) K) ↑E)
hζ : ζ ^ ↑p = 1
hpodd : ↑p ≠ 2
⊢ ∀ (i : ℕ), (σ ^ i) ((algebraMap (𝓞 K) K) ↑E) = ((algebraMap k K) ζ)⁻¹ ^ i * (algebraMap (𝓞 K) K) ↑E
Tactic:
intro i
State after:
p : ℕ+
K : Type u_1
inst✝¹³ : Field K
inst✝¹² : NumberField K
k : Type u_2
inst✝¹¹ : Field k
inst✝¹⁰ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝⁹ : AddCommGroup G
inst✝⁸ : CommGroup H
inst✝⁷ : Fintype H
hCard : Fintype.card H = ↑p
σ✝ : H
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r : ℕ
inst✝⁶ : DistribMulAction H G
inst✝⁵ : Module.Free ℤ G
inst✝⁴ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝³ : Algebra k K
inst✝² : IsGalois k K
inst✝¹ : FiniteDimensional k K
inst✝ : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
E : (𝓞 K)ˣ
ζ : k
hE : (algebraMap k K) ζ = (algebraMap (𝓞 K) K) ↑E / σ ((algebraMap (𝓞 K) K) ↑E)
hζ : ζ ^ ↑p = 1
hpodd : ↑p ≠ 2
i : ℕ
⊢ (σ ^ i) ((algebraMap (𝓞 K) K) ↑E) = ((algebraMap k K) ζ)⁻¹ ^ i * (algebraMap (𝓞 K) K) ↑E

State before:
p : ℕ+
K : Type u_1
inst✝¹³ : Field K
inst✝¹² : NumberField K
k : Type u_2
inst✝¹¹ : Field k
inst✝¹⁰ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝⁹ : AddCommGroup G
inst✝⁸ : CommGroup H
inst✝⁷ : Fintype H
hCard : Fintype.card H = ↑p
σ✝ : H
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r : ℕ
inst✝⁶ : DistribMulAction H G
inst✝⁵ : Module.Free ℤ G
inst✝⁴ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝³ : Algebra k K
inst✝² : IsGalois k K
inst✝¹ : FiniteDimensional k K
inst✝ : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
E : (𝓞 K)ˣ
ζ : k
hE : (algebraMap k K) ζ = (algebraMap (𝓞 K) K) ↑E / σ ((algebraMap (𝓞 K) K) ↑E)
hζ : ζ ^ ↑p = 1
hpodd : ↑p ≠ 2
i : ℕ
⊢ (σ ^ i) ((algebraMap (𝓞 K) K) ↑E) = ((algebraMap k K) ζ)⁻¹ ^ i * (algebraMap (𝓞 K) K) ↑E
Tactic:
induction i with
| zero =>
  simp only [pow_zero, AlgEquiv.one_apply, one_mul]
| succ n ih =>
  rw [pow_succ', AlgEquiv.mul_apply, ih, pow_succ']
  simp only [inv_pow, map_mul, map_inv₀, map_pow, AlgEquiv.commutes]
  have h0 : (algebraMap k K) ζ ≠ 0 := fun h ↦ by simp [(map_eq_zero _).1 h] at hζ
  field_simp [h0]
  rw [← mul_assoc]
  congr
  rw [hE]
  field_simp
State after:
no goals

State before:
case zero
p : ℕ+
K : Type u_1
inst✝¹³ : Field K
inst✝¹² : NumberField K
k : Type u_2
inst✝¹¹ : Field k
inst✝¹⁰ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝⁹ : AddCommGroup G
inst✝⁸ : CommGroup H
inst✝⁷ : Fintype H
hCard : Fintype.card H = ↑p
σ✝ : H
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r : ℕ
inst✝⁶ : DistribMulAction H G
inst✝⁵ : Module.Free ℤ G
inst✝⁴ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝³ : Algebra k K
inst✝² : IsGalois k K
inst✝¹ : FiniteDimensional k K
inst✝ : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
E : (𝓞 K)ˣ
ζ : k
hE : (algebraMap k K) ζ = (algebraMap (𝓞 K) K) ↑E / σ ((algebraMap (𝓞 K) K) ↑E)
hζ : ζ ^ ↑p = 1
hpodd : ↑p ≠ 2
⊢ (σ ^ 0) ((algebraMap (𝓞 K) K) ↑E) = ((algebraMap k K) ζ)⁻¹ ^ 0 * (algebraMap (𝓞 K) K) ↑E
Tactic:
simp only [pow_zero, AlgEquiv.one_apply, one_mul]
State after:
no goals

State before:
case succ
p : ℕ+
K : Type u_1
inst✝¹³ : Field K
inst✝¹² : NumberField K
k : Type u_2
inst✝¹¹ : Field k
inst✝¹⁰ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝⁹ : AddCommGroup G
inst✝⁸ : CommGroup H
inst✝⁷ : Fintype H
hCard : Fintype.card H = ↑p
σ✝ : H
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r : ℕ
inst✝⁶ : DistribMulAction H G
inst✝⁵ : Module.Free ℤ G
inst✝⁴ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝³ : Algebra k K
inst✝² : IsGalois k K
inst✝¹ : FiniteDimensional k K
inst✝ : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
E : (𝓞 K)ˣ
ζ : k
hE : (algebraMap k K) ζ = (algebraMap (𝓞 K) K) ↑E / σ ((algebraMap (𝓞 K) K) ↑E)
hζ : ζ ^ ↑p = 1
hpodd : ↑p ≠ 2
n : ℕ
ih : (σ ^ n) ((algebraMap (𝓞 K) K) ↑E) = ((algebraMap k K) ζ)⁻¹ ^ n * (algebraMap (𝓞 K) K) ↑E
⊢ (σ ^ (n + 1)) ((algebraMap (𝓞 K) K) ↑E) = ((algebraMap k K) ζ)⁻¹ ^ (n + 1) * (algebraMap (𝓞 K) K) ↑E
Tactic:
rw [pow_succ', AlgEquiv.mul_apply, ih, pow_succ']
State after:
case succ
p : ℕ+
K : Type u_1
inst✝¹³ : Field K
inst✝¹² : NumberField K
k : Type u_2
inst✝¹¹ : Field k
inst✝¹⁰ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝⁹ : AddCommGroup G
inst✝⁸ : CommGroup H
inst✝⁷ : Fintype H
hCard : Fintype.card H = ↑p
σ✝ : H
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r : ℕ
inst✝⁶ : DistribMulAction H G
inst✝⁵ : Module.Free ℤ G
inst✝⁴ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝³ : Algebra k K
inst✝² : IsGalois k K
inst✝¹ : FiniteDimensional k K
inst✝ : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
E : (𝓞 K)ˣ
ζ : k
hE : (algebraMap k K) ζ = (algebraMap (𝓞 K) K) ↑E / σ ((algebraMap (𝓞 K) K) ↑E)
hζ : ζ ^ ↑p = 1
hpodd : ↑p ≠ 2
n : ℕ
ih : (σ ^ n) ((algebraMap (𝓞 K) K) ↑E) = ((algebraMap k K) ζ)⁻¹ ^ n * (algebraMap (𝓞 K) K) ↑E
⊢ σ (((algebraMap k K) ζ)⁻¹ ^ n * (algebraMap (𝓞 K) K) ↑E) =
    ((algebraMap k K) ζ)⁻¹ * ((algebraMap k K) ζ)⁻¹ ^ n * (algebraMap (𝓞 K) K) ↑E

State before:
case succ
p : ℕ+
K : Type u_1
inst✝¹³ : Field K
inst✝¹² : NumberField K
k : Type u_2
inst✝¹¹ : Field k
inst✝¹⁰ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝⁹ : AddCommGroup G
inst✝⁸ : CommGroup H
inst✝⁷ : Fintype H
hCard : Fintype.card H = ↑p
σ✝ : H
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r : ℕ
inst✝⁶ : DistribMulAction H G
inst✝⁵ : Module.Free ℤ G
inst✝⁴ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝³ : Algebra k K
inst✝² : IsGalois k K
inst✝¹ : FiniteDimensional k K
inst✝ : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
E : (𝓞 K)ˣ
ζ : k
hE : (algebraMap k K) ζ = (algebraMap (𝓞 K) K) ↑E / σ ((algebraMap (𝓞 K) K) ↑E)
hζ : ζ ^ ↑p = 1
hpodd : ↑p ≠ 2
n : ℕ
ih : (σ ^ n) ((algebraMap (𝓞 K) K) ↑E) = ((algebraMap k K) ζ)⁻¹ ^ n * (algebraMap (𝓞 K) K) ↑E
⊢ σ (((algebraMap k K) ζ)⁻¹ ^ n * (algebraMap (𝓞 K) K) ↑E) =
    ((algebraMap k K) ζ)⁻¹ * ((algebraMap k K) ζ)⁻¹ ^ n * (algebraMap (𝓞 K) K) ↑E
Tactic:
simp only [inv_pow, map_mul, map_inv₀, map_pow, AlgEquiv.commutes]
State after:
case succ
p : ℕ+
K : Type u_1
inst✝¹³ : Field K
inst✝¹² : NumberField K
k : Type u_2
inst✝¹¹ : Field k
inst✝¹⁰ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝⁹ : AddCommGroup G
inst✝⁸ : CommGroup H
inst✝⁷ : Fintype H
hCard : Fintype.card H = ↑p
σ✝ : H
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r : ℕ
inst✝⁶ : DistribMulAction H G
inst✝⁵ : Module.Free ℤ G
inst✝⁴ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝³ : Algebra k K
inst✝² : IsGalois k K
inst✝¹ : FiniteDimensional k K
inst✝ : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
E : (𝓞 K)ˣ
ζ : k
hE : (algebraMap k K) ζ = (algebraMap (𝓞 K) K) ↑E / σ ((algebraMap (𝓞 K) K) ↑E)
hζ : ζ ^ ↑p = 1
hpodd : ↑p ≠ 2
n : ℕ
ih : (σ ^ n) ((algebraMap (𝓞 K) K) ↑E) = ((algebraMap k K) ζ)⁻¹ ^ n * (algebraMap (𝓞 K) K) ↑E
⊢ ((algebraMap k K) ζ ^ n)⁻¹ * σ ((algebraMap (𝓞 K) K) ↑E) =
    ((algebraMap k K) ζ)⁻¹ * ((algebraMap k K) ζ ^ n)⁻¹ * (algebraMap (𝓞 K) K) ↑E

State before:
case succ
p : ℕ+
K : Type u_1
inst✝¹³ : Field K
inst✝¹² : NumberField K
k : Type u_2
inst✝¹¹ : Field k
inst✝¹⁰ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝⁹ : AddCommGroup G
inst✝⁸ : CommGroup H
inst✝⁷ : Fintype H
hCard : Fintype.card H = ↑p
σ✝ : H
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r : ℕ
inst✝⁶ : DistribMulAction H G
inst✝⁵ : Module.Free ℤ G
inst✝⁴ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝³ : Algebra k K
inst✝² : IsGalois k K
inst✝¹ : FiniteDimensional k K
inst✝ : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
E : (𝓞 K)ˣ
ζ : k
hE : (algebraMap k K) ζ = (algebraMap (𝓞 K) K) ↑E / σ ((algebraMap (𝓞 K) K) ↑E)
hζ : ζ ^ ↑p = 1
hpodd : ↑p ≠ 2
n : ℕ
ih : (σ ^ n) ((algebraMap (𝓞 K) K) ↑E) = ((algebraMap k K) ζ)⁻¹ ^ n * (algebraMap (𝓞 K) K) ↑E
⊢ ((algebraMap k K) ζ ^ n)⁻¹ * σ ((algebraMap (𝓞 K) K) ↑E) =
    ((algebraMap k K) ζ)⁻¹ * ((algebraMap k K) ζ ^ n)⁻¹ * (algebraMap (𝓞 K) K) ↑E
Tactic:
have h0 : (algebraMap k K) ζ ≠ 0 := fun h ↦ by simp [(map_eq_zero _).1 h] at hζ
State after:
case succ
p : ℕ+
K : Type u_1
inst✝¹³ : Field K
inst✝¹² : NumberField K
k : Type u_2
inst✝¹¹ : Field k
inst✝¹⁰ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝⁹ : AddCommGroup G
inst✝⁸ : CommGroup H
inst✝⁷ : Fintype H
hCard : Fintype.card H = ↑p
σ✝ : H
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r : ℕ
inst✝⁶ : DistribMulAction H G
inst✝⁵ : Module.Free ℤ G
inst✝⁴ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝³ : Algebra k K
inst✝² : IsGalois k K
inst✝¹ : FiniteDimensional k K
inst✝ : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
E : (𝓞 K)ˣ
ζ : k
hE : (algebraMap k K) ζ = (algebraMap (𝓞 K) K) ↑E / σ ((algebraMap (𝓞 K) K) ↑E)
hζ : ζ ^ ↑p = 1
hpodd : ↑p ≠ 2
n : ℕ
ih : (σ ^ n) ((algebraMap (𝓞 K) K) ↑E) = ((algebraMap k K) ζ)⁻¹ ^ n * (algebraMap (𝓞 K) K) ↑E
h0 : (algebraMap k K) ζ ≠ 0
⊢ ((algebraMap k K) ζ ^ n)⁻¹ * σ ((algebraMap (𝓞 K) K) ↑E) =
    ((algebraMap k K) ζ)⁻¹ * ((algebraMap k K) ζ ^ n)⁻¹ * (algebraMap (𝓞 K) K) ↑E

State before:
case succ
p : ℕ+
K : Type u_1
inst✝¹³ : Field K
inst✝¹² : NumberField K
k : Type u_2
inst✝¹¹ : Field k
inst✝¹⁰ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝⁹ : AddCommGroup G
inst✝⁸ : CommGroup H
inst✝⁷ : Fintype H
hCard : Fintype.card H = ↑p
σ✝ : H
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r : ℕ
inst✝⁶ : DistribMulAction H G
inst✝⁵ : Module.Free ℤ G
inst✝⁴ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝³ : Algebra k K
inst✝² : IsGalois k K
inst✝¹ : FiniteDimensional k K
inst✝ : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
E : (𝓞 K)ˣ
ζ : k
hE : (algebraMap k K) ζ = (algebraMap (𝓞 K) K) ↑E / σ ((algebraMap (𝓞 K) K) ↑E)
hζ : ζ ^ ↑p = 1
hpodd : ↑p ≠ 2
n : ℕ
ih : (σ ^ n) ((algebraMap (𝓞 K) K) ↑E) = ((algebraMap k K) ζ)⁻¹ ^ n * (algebraMap (𝓞 K) K) ↑E
h0 : (algebraMap k K) ζ ≠ 0
⊢ ((algebraMap k K) ζ ^ n)⁻¹ * σ ((algebraMap (𝓞 K) K) ↑E) =
    ((algebraMap k K) ζ)⁻¹ * ((algebraMap k K) ζ ^ n)⁻¹ * (algebraMap (𝓞 K) K) ↑E
Tactic:
field_simp [h0]
State after:
case succ
p : ℕ+
K : Type u_1
inst✝¹³ : Field K
inst✝¹² : NumberField K
k : Type u_2
inst✝¹¹ : Field k
inst✝¹⁰ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝⁹ : AddCommGroup G
inst✝⁸ : CommGroup H
inst✝⁷ : Fintype H
hCard : Fintype.card H = ↑p
σ✝ : H
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r : ℕ
inst✝⁶ : DistribMulAction H G
inst✝⁵ : Module.Free ℤ G
inst✝⁴ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝³ : Algebra k K
inst✝² : IsGalois k K
inst✝¹ : FiniteDimensional k K
inst✝ : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
E : (𝓞 K)ˣ
ζ : k
hE : (algebraMap k K) ζ = (algebraMap (𝓞 K) K) ↑E / σ ((algebraMap (𝓞 K) K) ↑E)
hζ : ζ ^ ↑p = 1
hpodd : ↑p ≠ 2
n : ℕ
ih : (σ ^ n) ((algebraMap (𝓞 K) K) ↑E) = ((algebraMap k K) ζ)⁻¹ ^ n * (algebraMap (𝓞 K) K) ↑E
h0 : (algebraMap k K) ζ ≠ 0
⊢ σ ((algebraMap (𝓞 K) K) ↑E) * ((algebraMap k K) ζ * (algebraMap k K) ζ ^ n) =
    (algebraMap (𝓞 K) K) ↑E * (algebraMap k K) ζ ^ n

State before:
case succ
p : ℕ+
K : Type u_1
inst✝¹³ : Field K
inst✝¹² : NumberField K
k : Type u_2
inst✝¹¹ : Field k
inst✝¹⁰ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝⁹ : AddCommGroup G
inst✝⁸ : CommGroup H
inst✝⁷ : Fintype H
hCard : Fintype.card H = ↑p
σ✝ : H
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r : ℕ
inst✝⁶ : DistribMulAction H G
inst✝⁵ : Module.Free ℤ G
inst✝⁴ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝³ : Algebra k K
inst✝² : IsGalois k K
inst✝¹ : FiniteDimensional k K
inst✝ : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
E : (𝓞 K)ˣ
ζ : k
hE : (algebraMap k K) ζ = (algebraMap (𝓞 K) K) ↑E / σ ((algebraMap (𝓞 K) K) ↑E)
hζ : ζ ^ ↑p = 1
hpodd : ↑p ≠ 2
n : ℕ
ih : (σ ^ n) ((algebraMap (𝓞 K) K) ↑E) = ((algebraMap k K) ζ)⁻¹ ^ n * (algebraMap (𝓞 K) K) ↑E
h0 : (algebraMap k K) ζ ≠ 0
⊢ σ ((algebraMap (𝓞 K) K) ↑E) * ((algebraMap k K) ζ * (algebraMap k K) ζ ^ n) =
    (algebraMap (𝓞 K) K) ↑E * (algebraMap k K) ζ ^ n
Tactic:
rw [← mul_assoc]
State after:
case succ
p : ℕ+
K : Type u_1
inst✝¹³ : Field K
inst✝¹² : NumberField K
k : Type u_2
inst✝¹¹ : Field k
inst✝¹⁰ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝⁹ : AddCommGroup G
inst✝⁸ : CommGroup H
inst✝⁷ : Fintype H
hCard : Fintype.card H = ↑p
σ✝ : H
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r : ℕ
inst✝⁶ : DistribMulAction H G
inst✝⁵ : Module.Free ℤ G
inst✝⁴ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝³ : Algebra k K
inst✝² : IsGalois k K
inst✝¹ : FiniteDimensional k K
inst✝ : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
E : (𝓞 K)ˣ
ζ : k
hE : (algebraMap k K) ζ = (algebraMap (𝓞 K) K) ↑E / σ ((algebraMap (𝓞 K) K) ↑E)
hζ : ζ ^ ↑p = 1
hpodd : ↑p ≠ 2
n : ℕ
ih : (σ ^ n) ((algebraMap (𝓞 K) K) ↑E) = ((algebraMap k K) ζ)⁻¹ ^ n * (algebraMap (𝓞 K) K) ↑E
h0 : (algebraMap k K) ζ ≠ 0
⊢ σ ((algebraMap (𝓞 K) K) ↑E) * (algebraMap k K) ζ * (algebraMap k K) ζ ^ n =
    (algebraMap (𝓞 K) K) ↑E * (algebraMap k K) ζ ^ n

State before:
case succ
p : ℕ+
K : Type u_1
inst✝¹³ : Field K
inst✝¹² : NumberField K
k : Type u_2
inst✝¹¹ : Field k
inst✝¹⁰ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝⁹ : AddCommGroup G
inst✝⁸ : CommGroup H
inst✝⁷ : Fintype H
hCard : Fintype.card H = ↑p
σ✝ : H
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r : ℕ
inst✝⁶ : DistribMulAction H G
inst✝⁵ : Module.Free ℤ G
inst✝⁴ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝³ : Algebra k K
inst✝² : IsGalois k K
inst✝¹ : FiniteDimensional k K
inst✝ : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
E : (𝓞 K)ˣ
ζ : k
hE : (algebraMap k K) ζ = (algebraMap (𝓞 K) K) ↑E / σ ((algebraMap (𝓞 K) K) ↑E)
hζ : ζ ^ ↑p = 1
hpodd : ↑p ≠ 2
n : ℕ
ih : (σ ^ n) ((algebraMap (𝓞 K) K) ↑E) = ((algebraMap k K) ζ)⁻¹ ^ n * (algebraMap (𝓞 K) K) ↑E
h0 : (algebraMap k K) ζ ≠ 0
⊢ σ ((algebraMap (𝓞 K) K) ↑E) * (algebraMap k K) ζ * (algebraMap k K) ζ ^ n =
    (algebraMap (𝓞 K) K) ↑E * (algebraMap k K) ζ ^ n
Tactic:
congr
State after:
case succ.e_a
p : ℕ+
K : Type u_1
inst✝¹³ : Field K
inst✝¹² : NumberField K
k : Type u_2
inst✝¹¹ : Field k
inst✝¹⁰ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝⁹ : AddCommGroup G
inst✝⁸ : CommGroup H
inst✝⁷ : Fintype H
hCard : Fintype.card H = ↑p
σ✝ : H
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r : ℕ
inst✝⁶ : DistribMulAction H G
inst✝⁵ : Module.Free ℤ G
inst✝⁴ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝³ : Algebra k K
inst✝² : IsGalois k K
inst✝¹ : FiniteDimensional k K
inst✝ : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
E : (𝓞 K)ˣ
ζ : k
hE : (algebraMap k K) ζ = (algebraMap (𝓞 K) K) ↑E / σ ((algebraMap (𝓞 K) K) ↑E)
hζ : ζ ^ ↑p = 1
hpodd : ↑p ≠ 2
n : ℕ
ih : (σ ^ n) ((algebraMap (𝓞 K) K) ↑E) = ((algebraMap k K) ζ)⁻¹ ^ n * (algebraMap (𝓞 K) K) ↑E
h0 : (algebraMap k K) ζ ≠ 0
⊢ σ ((algebraMap (𝓞 K) K) ↑E) * (algebraMap k K) ζ = (algebraMap (𝓞 K) K) ↑E

State before:
case succ.e_a
p : ℕ+
K : Type u_1
inst✝¹³ : Field K
inst✝¹² : NumberField K
k : Type u_2
inst✝¹¹ : Field k
inst✝¹⁰ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝⁹ : AddCommGroup G
inst✝⁸ : CommGroup H
inst✝⁷ : Fintype H
hCard : Fintype.card H = ↑p
σ✝ : H
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r : ℕ
inst✝⁶ : DistribMulAction H G
inst✝⁵ : Module.Free ℤ G
inst✝⁴ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝³ : Algebra k K
inst✝² : IsGalois k K
inst✝¹ : FiniteDimensional k K
inst✝ : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
E : (𝓞 K)ˣ
ζ : k
hE : (algebraMap k K) ζ = (algebraMap (𝓞 K) K) ↑E / σ ((algebraMap (𝓞 K) K) ↑E)
hζ : ζ ^ ↑p = 1
hpodd : ↑p ≠ 2
n : ℕ
ih : (σ ^ n) ((algebraMap (𝓞 K) K) ↑E) = ((algebraMap k K) ζ)⁻¹ ^ n * (algebraMap (𝓞 K) K) ↑E
h0 : (algebraMap k K) ζ ≠ 0
⊢ σ ((algebraMap (𝓞 K) K) ↑E) * (algebraMap k K) ζ = (algebraMap (𝓞 K) K) ↑E
Tactic:
rw [hE]
State after:
case succ.e_a
p : ℕ+
K : Type u_1
inst✝¹³ : Field K
inst✝¹² : NumberField K
k : Type u_2
inst✝¹¹ : Field k
inst✝¹⁰ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝⁹ : AddCommGroup G
inst✝⁸ : CommGroup H
inst✝⁷ : Fintype H
hCard : Fintype.card H = ↑p
σ✝ : H
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r : ℕ
inst✝⁶ : DistribMulAction H G
inst✝⁵ : Module.Free ℤ G
inst✝⁴ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝³ : Algebra k K
inst✝² : IsGalois k K
inst✝¹ : FiniteDimensional k K
inst✝ : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
E : (𝓞 K)ˣ
ζ : k
hE : (algebraMap k K) ζ = (algebraMap (𝓞 K) K) ↑E / σ ((algebraMap (𝓞 K) K) ↑E)
hζ : ζ ^ ↑p = 1
hpodd : ↑p ≠ 2
n : ℕ
ih : (σ ^ n) ((algebraMap (𝓞 K) K) ↑E) = ((algebraMap k K) ζ)⁻¹ ^ n * (algebraMap (𝓞 K) K) ↑E
h0 : (algebraMap k K) ζ ≠ 0
⊢ σ ((algebraMap (𝓞 K) K) ↑E) * ((algebraMap (𝓞 K) K) ↑E / σ ((algebraMap (𝓞 K) K) ↑E)) = (algebraMap (𝓞 K) K) ↑E

State before:
case succ.e_a
p : ℕ+
K : Type u_1
inst✝¹³ : Field K
inst✝¹² : NumberField K
k : Type u_2
inst✝¹¹ : Field k
inst✝¹⁰ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝⁹ : AddCommGroup G
inst✝⁸ : CommGroup H
inst✝⁷ : Fintype H
hCard : Fintype.card H = ↑p
σ✝ : H
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r : ℕ
inst✝⁶ : DistribMulAction H G
inst✝⁵ : Module.Free ℤ G
inst✝⁴ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝³ : Algebra k K
inst✝² : IsGalois k K
inst✝¹ : FiniteDimensional k K
inst✝ : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
E : (𝓞 K)ˣ
ζ : k
hE : (algebraMap k K) ζ = (algebraMap (𝓞 K) K) ↑E / σ ((algebraMap (𝓞 K) K) ↑E)
hζ : ζ ^ ↑p = 1
hpodd : ↑p ≠ 2
n : ℕ
ih : (σ ^ n) ((algebraMap (𝓞 K) K) ↑E) = ((algebraMap k K) ζ)⁻¹ ^ n * (algebraMap (𝓞 K) K) ↑E
h0 : (algebraMap k K) ζ ≠ 0
⊢ σ ((algebraMap (𝓞 K) K) ↑E) * ((algebraMap (𝓞 K) K) ↑E / σ ((algebraMap (𝓞 K) K) ↑E)) = (algebraMap (𝓞 K) K) ↑E
Tactic:
field_simp
State after:
no goals

State before:
p : ℕ+
K : Type u_1
inst✝¹³ : Field K
inst✝¹² : NumberField K
k : Type u_2
inst✝¹¹ : Field k
inst✝¹⁰ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝⁹ : AddCommGroup G
inst✝⁸ : CommGroup H
inst✝⁷ : Fintype H
hCard : Fintype.card H = ↑p
σ✝ : H
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r : ℕ
inst✝⁶ : DistribMulAction H G
inst✝⁵ : Module.Free ℤ G
inst✝⁴ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝³ : Algebra k K
inst✝² : IsGalois k K
inst✝¹ : FiniteDimensional k K
inst✝ : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
E : (𝓞 K)ˣ
ζ : k
hE : (algebraMap k K) ζ = (algebraMap (𝓞 K) K) ↑E / σ ((algebraMap (𝓞 K) K) ↑E)
hζ : ζ ^ ↑p = 1
hpodd : ↑p ≠ 2
n : ℕ
ih : (σ ^ n) ((algebraMap (𝓞 K) K) ↑E) = ((algebraMap k K) ζ)⁻¹ ^ n * (algebraMap (𝓞 K) K) ↑E
h : (algebraMap k K) ζ = 0
⊢ False
Tactic:
simp [(map_eq_zero _).1 h] at hζ
State after:
no goals

State before:
case H
p : ℕ+
K : Type u_1
inst✝¹³ : Field K
inst✝¹² : NumberField K
k : Type u_2
inst✝¹¹ : Field k
inst✝¹⁰ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝⁹ : AddCommGroup G
inst✝⁸ : CommGroup H
inst✝⁷ : Fintype H
hCard : Fintype.card H = ↑p
σ✝ : H
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r : ℕ
inst✝⁶ : DistribMulAction H G
inst✝⁵ : Module.Free ℤ G
inst✝⁴ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝³ : Algebra k K
inst✝² : IsGalois k K
inst✝¹ : FiniteDimensional k K
inst✝ : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
E : (𝓞 K)ˣ
ζ : k
hE : (algebraMap k K) ζ = (algebraMap (𝓞 K) K) ↑E / σ ((algebraMap (𝓞 K) K) ↑E)
hζ : ζ ^ ↑p = 1
hpodd : ↑p ≠ 2
h1 : ∀ (i : ℕ), (σ ^ i) ((algebraMap (𝓞 K) K) ↑E) = ((algebraMap k K) ζ)⁻¹ ^ i * (algebraMap (𝓞 K) K) ↑E
⊢ 2 ∣ ↑p - 1
Tactic:
exact even_iff_two_dvd.1 (hp.even_sub_one hpodd)
State after:
no goals

State before:
p : ℕ+
K : Type u_1
inst✝¹³ : Field K
inst✝¹² : NumberField K
k : Type u_2
inst✝¹¹ : Field k
inst✝¹⁰ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝⁹ : AddCommGroup G
inst✝⁸ : CommGroup H
inst✝⁷ : Fintype H
hCard : Fintype.card H = ↑p
σ✝ : H
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r : ℕ
inst✝⁶ : DistribMulAction H G
inst✝⁵ : Module.Free ℤ G
inst✝⁴ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝³ : Algebra k K
inst✝² : IsGalois k K
inst✝¹ : FiniteDimensional k K
inst✝ : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
E : (𝓞 K)ˣ
ζ : k
hE : (algebraMap k K) ζ = (algebraMap (𝓞 K) K) ↑E / σ ((algebraMap (𝓞 K) K) ↑E)
hζ : ζ ^ ↑p = 1
hpodd : ↑p ≠ 2
h1 : ∀ (i : ℕ), (σ ^ i) ((algebraMap (𝓞 K) K) ↑E) = ((algebraMap k K) ζ)⁻¹ ^ i * (algebraMap (𝓞 K) K) ↑E
⊢ (algebraMap (𝓞 K) K) ↑E ^ ↑p ≠ 0
Tactic:
simp
State after:
no goals