Theorem: Hilbert92ish
Proof state before:
case intro.intro.intro
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 σ
hpodd : ↑p ≠ 2
h : ℕ
ζ : (𝓞 k)ˣ
hζ : IsPrimitiveRoot ((algebraMap (𝓞 k) k) ↑ζ) (↑p ^ h)
hζ' : ∀ (ε : (𝓞 k)ˣ) (n : ℕ), ε ^ ↑p ^ n = 1 → ∃ i, ζ ^ i = ε
⊢ ∃ η,
    (Algebra.norm k) ((algebraMap (𝓞 K) K) ↑η) = 1 ∧
      ∀ (ε : (𝓞 K)ˣ), (algebraMap (𝓞 K) K) ↑η ≠ (algebraMap (𝓞 K) K) ↑ε / σ ((algebraMap (𝓞 K) K) ↑ε)
Tactic:
by_cases H : ∀ ε : (𝓞 K)ˣ, algebraMap k K ζ ^ ((p : ℕ)^(h - 1)) ≠ ε / (σ ε : K)
Proof state after:
case pos
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 σ
hpodd : ↑p ≠ 2
h : ℕ
ζ : (𝓞 k)ˣ
hζ : IsPrimitiveRoot ((algebraMap (𝓞 k) k) ↑ζ) (↑p ^ h)
hζ' : ∀ (ε : (𝓞 k)ˣ) (n : ℕ), ε ^ ↑p ^ n = 1 → ∃ i, ζ ^ i = ε
H :
  ∀ (ε : (𝓞 K)ˣ),
    (algebraMap k K) ((algebraMap (𝓞 k) k) ↑ζ) ^ ↑p ^ (h - 1) ≠ (algebraMap (𝓞 K) K) ↑ε / σ ((algebraMap (𝓞 K) K) ↑ε)
⊢ ∃ η,
    (Algebra.norm k) ((algebraMap (𝓞 K) K) ↑η) = 1 ∧
      ∀ (ε : (𝓞 K)ˣ), (algebraMap (𝓞 K) K) ↑η ≠ (algebraMap (𝓞 K) K) ↑ε / σ ((algebraMap (𝓞 K) K) ↑ε)

case neg
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 σ
hpodd : ↑p ≠ 2
h : ℕ
ζ : (𝓞 k)ˣ
hζ : IsPrimitiveRoot ((algebraMap (𝓞 k) k) ↑ζ) (↑p ^ h)
hζ' : ∀ (ε : (𝓞 k)ˣ) (n : ℕ), ε ^ ↑p ^ n = 1 → ∃ i, ζ ^ i = ε
H :
  ¬∀ (ε : (𝓞 K)ˣ),
      (algebraMap k K) ((algebraMap (𝓞 k) k) ↑ζ) ^ ↑p ^ (h - 1) ≠ (algebraMap (𝓞 K) K) ↑ε / σ ((algebraMap (𝓞 K) K) ↑ε)
⊢ ∃ η,
    (Algebra.norm k) ((algebraMap (𝓞 K) K) ↑η) = 1 ∧
      ∀ (ε : (𝓞 K)ˣ), (algebraMap (𝓞 K) K) ↑η ≠ (algebraMap (𝓞 K) K) ↑ε / σ ((algebraMap (𝓞 K) K) ↑ε)