Theorem: KummersLemma.separable_poly
Proof state before:
case hI
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
I : Ideal (𝓞 K)
inst✝ : I.IsMaximal
L : Type u_1 := K[↑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 }
J : Ideal (𝓞 L) := Ideal.map (algebraMap (𝓞 K) (𝓞 L)) I
this✝¹ : AddCommGroup (𝓞 L) := AddCommGroupWithOne.toAddCommGroup
this✝ : Module (𝓞 K) (𝓞 L) := Algebra.toModule
this : CommRing (𝓞 L ⧸ J) := Ideal.Quotient.commRing J
i : 𝓞 K ⧸ I →+* 𝓞 L ⧸ J := Ideal.quotientMap J (algebraMap (𝓞 K) (𝓞 L)) ⋯
⊢ ¬I = ⊤

case hI.hf₁
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
I : Ideal (𝓞 K)
inst✝ : I.IsMaximal
L : Type u_1 := K[↑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 }
J : Ideal (𝓞 L) := Ideal.map (algebraMap (𝓞 K) (𝓞 L)) I
this✝¹ : AddCommGroup (𝓞 L) := AddCommGroupWithOne.toAddCommGroup
this✝ : Module (𝓞 K) (𝓞 L) := Algebra.toModule
this : CommRing (𝓞 L ⧸ J) := Ideal.Quotient.commRing J
i : 𝓞 K ⧸ I →+* 𝓞 L ⧸ J := Ideal.quotientMap J (algebraMap (𝓞 K) (𝓞 L)) ⋯
⊢ Function.Injective ⇑(algebraMap (𝓞 K) (𝓞 L))

case hI.hf₂
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
I : Ideal (𝓞 K)
inst✝ : I.IsMaximal
L : Type u_1 := K[↑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 }
J : Ideal (𝓞 L) := Ideal.map (algebraMap (𝓞 K) (𝓞 L)) I
this✝¹ : AddCommGroup (𝓞 L) := AddCommGroupWithOne.toAddCommGroup
this✝ : Module (𝓞 K) (𝓞 L) := Algebra.toModule
this : CommRing (𝓞 L ⧸ J) := Ideal.Quotient.commRing J
i : 𝓞 K ⧸ I →+* 𝓞 L ⧸ J := Ideal.quotientMap J (algebraMap (𝓞 K) (𝓞 L)) ⋯
⊢ (algebraMap (𝓞 K) (𝓞 L)).IsIntegral
Tactic:
exact Ideal.IsMaximal.ne_top ‹_›
Proof state after:
case hI.hf₁
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
I : Ideal (𝓞 K)
inst✝ : I.IsMaximal
L : Type u_1 := K[↑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 }
J : Ideal (𝓞 L) := Ideal.map (algebraMap (𝓞 K) (𝓞 L)) I
this✝¹ : AddCommGroup (𝓞 L) := AddCommGroupWithOne.toAddCommGroup
this✝ : Module (𝓞 K) (𝓞 L) := Algebra.toModule
this : CommRing (𝓞 L ⧸ J) := Ideal.Quotient.commRing J
i : 𝓞 K ⧸ I →+* 𝓞 L ⧸ J := Ideal.quotientMap J (algebraMap (𝓞 K) (𝓞 L)) ⋯
⊢ Function.Injective ⇑(algebraMap (𝓞 K) (𝓞 L))

case hI.hf₂
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
I : Ideal (𝓞 K)
inst✝ : I.IsMaximal
L : Type u_1 := K[↑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 }
J : Ideal (𝓞 L) := Ideal.map (algebraMap (𝓞 K) (𝓞 L)) I
this✝¹ : AddCommGroup (𝓞 L) := AddCommGroupWithOne.toAddCommGroup
this✝ : Module (𝓞 K) (𝓞 L) := Algebra.toModule
this : CommRing (𝓞 L ⧸ J) := Ideal.Quotient.commRing J
i : 𝓞 K ⧸ I →+* 𝓞 L ⧸ J := Ideal.quotientMap J (algebraMap (𝓞 K) (𝓞 L)) ⋯
⊢ (algebraMap (𝓞 K) (𝓞 L)).IsIntegral