congr
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
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