have := KummersLemma.isUnramified hp hζ u hcong hu L
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁷ : Field K
inst✝⁶ : NumberField K
inst✝⁵ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝⁴ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u✝ : (𝓞 K)ˣ
hcong✝ : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u✝ - 1
hu✝ : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u✝
L✝ : Type ?u.27748
inst✝³ : Field L✝
inst✝² : Algebra K L✝
inst✝¹ : FiniteDimensional K L✝
inst✝ : IsSplittingField K L✝ (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u✝))
σ : L✝ ≃ₐ[K] L✝
hσ : ∀ (x : L✝ ≃ₐ[K] L✝), x ∈ Subgroup.zpowers σ
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
this✝⁶ : Fact (Irreducible (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))) :=
  { out := X_pow_sub_C_irreducible_of_prime Fact.out hu }
L : Type u_1 := AdjoinRoot (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
this✝⁵ : IsSplittingField K (AdjoinRoot (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))) (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
this✝⁴ : IsGalois K L
this✝³ : FiniteDimensional K L
this✝² : IsCyclic (L ≃ₐ[K] L)
this✝¹ : CharZero L
this✝ : FiniteDimensional ℚ L
this : NumberField L
hKL : FiniteDimensional.finrank K L = ↑p
⊢ False
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁷ : Field K
inst✝⁶ : NumberField K
inst✝⁵ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝⁴ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u✝ : (𝓞 K)ˣ
hcong✝ : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u✝ - 1
hu✝ : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u✝
L✝ : Type ?u.27748
inst✝³ : Field L✝
inst✝² : Algebra K L✝
inst✝¹ : FiniteDimensional K L✝
inst✝ : IsSplittingField K L✝ (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u✝))
σ : L✝ ≃ₐ[K] L✝
hσ : ∀ (x : L✝ ≃ₐ[K] L✝), x ∈ Subgroup.zpowers σ
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
this✝⁷ : Fact (Irreducible (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))) :=
  { out := X_pow_sub_C_irreducible_of_prime Fact.out hu }
L : Type u_1 := AdjoinRoot (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
this✝⁶ : IsSplittingField K (AdjoinRoot (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))) (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
this✝⁵ : IsGalois K L
this✝⁴ : FiniteDimensional K L
this✝³ : IsCyclic (L ≃ₐ[K] L)
this✝² : CharZero L
this✝¹ : FiniteDimensional ℚ L
this✝ : NumberField L
hKL : FiniteDimensional.finrank K L = ↑p
this : IsUnramified (𝓞 K) (𝓞 L)
⊢ False