mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Ideal.Norm.RelNorm

Goal state before:
pp: case inr
R : Type u_1
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
S : Type u_3
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : IsIntegrallyClosed R
inst✝³ : IsIntegrallyClosed S
inst✝² : Algebra R S
inst✝¹ : Module.Finite R S
inst✝ : IsTorsionFree R S
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I J : Ideal S
hI : spanNorm R I = ⊤
⊢ spanNorm R (I * J) ≤ spanNorm R J

Tactic:
]

Goal state after:
case inr
R : Type u_1
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
S : Type u_3
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : IsIntegrallyClosed R
inst✝³ : IsIntegrallyClosed S
inst✝² : Algebra R S
inst✝¹ : Module.Finite R S
inst✝ : IsTorsionFree R S
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I J : Ideal S
hI : spanNorm R I = ⊤
⊢ spanNorm R (I * J) ≤ spanNorm R J
Module: Mathlib.RingTheory.Ideal.Norm.RelNorm

Goal state before:
pp: case inr.inl
R : Type u_1
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
S : Type u_3
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : IsIntegrallyClosed R
inst✝³ : IsIntegrallyClosed S
inst✝² : Algebra R S
inst✝¹ : Module.Finite R S
inst✝ : IsTorsionFree R S
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I J : Ideal S
hI : spanNorm R I = ⊤
hJ : spanNorm R J = ⊥
⊢ ⊥ ≤ ⊥

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Ideal.Norm.RelNorm

Goal state before:
pp: case inr.inr
R : Type u_1
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
S : Type u_3
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : IsIntegrallyClosed R
inst✝³ : IsIntegrallyClosed S
inst✝² : Algebra R S
inst✝¹ : Module.Finite R S
inst✝ : IsTorsionFree R S
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I J : Ideal S
hI : spanNorm R I = ⊤
hJ : spanNorm R J = ⊤
⊢ spanNorm R (I * J) ≤ ⊤

Tactic:
]

Goal state after:
case inr.inr
R : Type u_1
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
S : Type u_3
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : IsIntegrallyClosed R
inst✝³ : IsIntegrallyClosed S
inst✝² : Algebra R S
inst✝¹ : Module.Finite R S
inst✝ : IsTorsionFree R S
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I J : Ideal S
hI : spanNorm R I = ⊤
hJ : spanNorm R J = ⊤
⊢ spanNorm R (I * J) ≤ ⊤
Module: Mathlib.RingTheory.Ideal.Norm.RelNorm

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
S : Type u_3
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : IsIntegrallyClosed R
inst✝³ : IsIntegrallyClosed S
inst✝² : Algebra R S
inst✝¹ : Module.Finite R S
inst✝ : IsTorsionFree R S
I : Ideal S
⊢ Submodule.span R (⇑(Algebra.intNorm R S) '' ↑I) ≤ comap (algebraMap R S) I

Tactic:
]

Goal state after:
R : Type u_1
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
S : Type u_3
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : IsIntegrallyClosed R
inst✝³ : IsIntegrallyClosed S
inst✝² : Algebra R S
inst✝¹ : Module.Finite R S
inst✝ : IsTorsionFree R S
I : Ideal S
⊢ Submodule.span R (⇑(Algebra.intNorm R S) '' ↑I) ≤ comap (algebraMap R S) I
Module: Mathlib.NumberTheory.NumberField.Discriminant.Different

Goal state before:
pp: L : Type u_3
inst✝¹ : Field L
inst✝ : NumberField L
K₁ K₂ : IntermediateField ℚ L
h₁ : K₁.LinearDisjoint ↥K₂
h₂ : K₁ ⊔ K₂ = ⊤
h₃ :
  IsCoprime (Ideal.map (algebraMap (𝓞 ↥K₁) (𝓞 L)) (differentIdeal ℤ (𝓞 ↥K₁)))
    (Ideal.map (algebraMap (𝓞 ↥K₂) (𝓞 L)) (differentIdeal ℤ (𝓞 ↥K₂)))
x✝ : Algebra (FractionRing (𝓞 ↥K₁)) (FractionRing (𝓞 L)) := FractionRing.liftAlgebra (𝓞 ↥K₁) (FractionRing (𝓞 L))
h_main : (discr L).natAbs = Ideal.absNorm (differentIdeal (𝓞 ↥K₂) (𝓞 L)) * (discr ↥K₂).natAbs ^ finrank (↥K₂) L
⊢ K₁.LinearDisjoint ↥K₂

Tactic:
]

Goal state after:
L : Type u_3
inst✝¹ : Field L
inst✝ : NumberField L
K₁ K₂ : IntermediateField ℚ L
h₁ : K₁.LinearDisjoint ↥K₂
h₂ : K₁ ⊔ K₂ = ⊤
h₃ :
  IsCoprime (Ideal.map (algebraMap (𝓞 ↥K₁) (𝓞 L)) (differentIdeal ℤ (𝓞 ↥K₁)))
    (Ideal.map (algebraMap (𝓞 ↥K₂) (𝓞 L)) (differentIdeal ℤ (𝓞 ↥K₂)))
x✝ : Algebra (FractionRing (𝓞 ↥K₁)) (FractionRing (𝓞 L)) := FractionRing.liftAlgebra (𝓞 ↥K₁) (FractionRing (𝓞 L))
h_main : (discr L).natAbs = Ideal.absNorm (differentIdeal (𝓞 ↥K₂) (𝓞 L)) * (discr ↥K₂).natAbs ^ finrank (↥K₂) L
⊢ K₁.LinearDisjoint ↥K₂
Module: Mathlib.NumberTheory.NumberField.Discriminant.Different

Goal state before:
pp: L : Type u_3
inst✝¹ : Field L
inst✝ : NumberField L
K₁ K₂ : IntermediateField ℚ L
h₁ : K₁.LinearDisjoint ↥K₂
h₂ : K₁ ⊔ K₂ = ⊤
h₃ :
  IsCoprime (Ideal.map (algebraMap (𝓞 ↥K₁) (𝓞 L)) (differentIdeal ℤ (𝓞 ↥K₁)))
    (Ideal.map (algebraMap (𝓞 ↥K₂) (𝓞 L)) (differentIdeal ℤ (𝓞 ↥K₂)))
x✝ : Algebra (FractionRing (𝓞 ↥K₁)) (FractionRing (𝓞 L)) := FractionRing.liftAlgebra (𝓞 ↥K₁) (FractionRing (𝓞 L))
h_main : (discr L).natAbs = Ideal.absNorm (differentIdeal (𝓞 ↥K₂) (𝓞 L)) * (discr ↥K₂).natAbs ^ finrank (↥K₂) L
⊢ K₁ ⊔ K₂ = ⊤

Tactic:
]

Goal state after:
L : Type u_3
inst✝¹ : Field L
inst✝ : NumberField L
K₁ K₂ : IntermediateField ℚ L
h₁ : K₁.LinearDisjoint ↥K₂
h₂ : K₁ ⊔ K₂ = ⊤
h₃ :
  IsCoprime (Ideal.map (algebraMap (𝓞 ↥K₁) (𝓞 L)) (differentIdeal ℤ (𝓞 ↥K₁)))
    (Ideal.map (algebraMap (𝓞 ↥K₂) (𝓞 L)) (differentIdeal ℤ (𝓞 ↥K₂)))
x✝ : Algebra (FractionRing (𝓞 ↥K₁)) (FractionRing (𝓞 L)) := FractionRing.liftAlgebra (𝓞 ↥K₁) (FractionRing (𝓞 L))
h_main : (discr L).natAbs = Ideal.absNorm (differentIdeal (𝓞 ↥K₂) (𝓞 L)) * (discr ↥K₂).natAbs ^ finrank (↥K₂) L
⊢ K₁ ⊔ K₂ = ⊤
Module: Mathlib.RingTheory.Ideal.Norm.RelNorm

Goal state before:
pp: case pos
R : Type u_1
inst✝¹¹ : CommRing R
inst✝¹⁰ : IsDomain R
S : Type u_3
inst✝⁹ : CommRing S
inst✝⁸ : IsDomain S
inst✝⁷ : IsIntegrallyClosed R
inst✝⁶ : IsIntegrallyClosed S
inst✝⁵ : Algebra R S
inst✝⁴ : Module.Finite R S
inst✝³ : IsTorsionFree R S
inst✝² : IsDedekindDomain R
inst✝¹ : IsDedekindDomain S
I J : Ideal S
inst✝ : Nontrivial R
h✝ : Nontrivial S
hP : ⊥.IsMaximal
⊢ map (algebraMap R (Localization.AtPrime ⊥)) (spanNorm R I * spanNorm R J) =
    map (algebraMap R (Localization.AtPrime ⊥)) (spanNorm R I * spanNorm R J)

pp: case pos.eq_bot_or_top
R : Type u_1
inst✝¹¹ : CommRing R
inst✝¹⁰ : IsDomain R
S : Type u_3
inst✝⁹ : CommRing S
inst✝⁸ : IsDomain S
inst✝⁷ : IsIntegrallyClosed R
inst✝⁶ : IsIntegrallyClosed S
inst✝⁵ : Algebra R S
inst✝⁴ : Module.Finite R S
inst✝³ : IsTorsionFree R S
inst✝² : IsDedekindDomain R
inst✝¹ : IsDedekindDomain S
I J : Ideal S
inst✝ : Nontrivial R
h✝ : Nontrivial S
hP : ⊥.IsMaximal
⊢ ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤

Tactic:
]

Goal state after:
case pos.eq_bot_or_top
R : Type u_1
inst✝¹¹ : CommRing R
inst✝¹⁰ : IsDomain R
S : Type u_3
inst✝⁹ : CommRing S
inst✝⁸ : IsDomain S
inst✝⁷ : IsIntegrallyClosed R
inst✝⁶ : IsIntegrallyClosed S
inst✝⁵ : Algebra R S
inst✝⁴ : Module.Finite R S
inst✝³ : IsTorsionFree R S
inst✝² : IsDedekindDomain R
inst✝¹ : IsDedekindDomain S
I J : Ideal S
inst✝ : Nontrivial R
h✝ : Nontrivial S
hP : ⊥.IsMaximal
⊢ ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
Module: Mathlib.NumberTheory.NumberField.Discriminant.Different

Goal state before:
pp: L : Type u_3
inst✝¹ : Field L
inst✝ : NumberField L
K₁ K₂ : IntermediateField ℚ L
h₁ : K₁.LinearDisjoint ↥K₂
h₂ : K₁ ⊔ K₂ = ⊤
h₃ :
  IsCoprime (Ideal.map (algebraMap (𝓞 ↥K₁) (𝓞 L)) (differentIdeal ℤ (𝓞 ↥K₁)))
    (Ideal.map (algebraMap (𝓞 ↥K₂) (𝓞 L)) (differentIdeal ℤ (𝓞 ↥K₂)))
x✝ : Algebra (FractionRing (𝓞 ↥K₁)) (FractionRing (𝓞 L)) := FractionRing.liftAlgebra (𝓞 ↥K₁) (FractionRing (𝓞 L))
h_main : (discr L).natAbs = Ideal.absNorm (differentIdeal (𝓞 ↥K₂) (𝓞 L)) * (discr ↥K₂).natAbs ^ finrank (↥K₂) L
⊢ IsCoprime (Ideal.map (algebraMap (𝓞 ↥K₁) (𝓞 L)) (differentIdeal ℤ (𝓞 ↥K₁)))
    (Ideal.map (algebraMap (𝓞 ↥K₂) (𝓞 L)) (differentIdeal ℤ (𝓞 ↥K₂)))

Tactic:
]

Goal state after:
L : Type u_3
inst✝¹ : Field L
inst✝ : NumberField L
K₁ K₂ : IntermediateField ℚ L
h₁ : K₁.LinearDisjoint ↥K₂
h₂ : K₁ ⊔ K₂ = ⊤
h₃ :
  IsCoprime (Ideal.map (algebraMap (𝓞 ↥K₁) (𝓞 L)) (differentIdeal ℤ (𝓞 ↥K₁)))
    (Ideal.map (algebraMap (𝓞 ↥K₂) (𝓞 L)) (differentIdeal ℤ (𝓞 ↥K₂)))
x✝ : Algebra (FractionRing (𝓞 ↥K₁)) (FractionRing (𝓞 L)) := FractionRing.liftAlgebra (𝓞 ↥K₁) (FractionRing (𝓞 L))
h_main : (discr L).natAbs = Ideal.absNorm (differentIdeal (𝓞 ↥K₂) (𝓞 L)) * (discr ↥K₂).natAbs ^ finrank (↥K₂) L
⊢ IsCoprime (Ideal.map (algebraMap (𝓞 ↥K₁) (𝓞 L)) (differentIdeal ℤ (𝓞 ↥K₁)))
    (Ideal.map (algebraMap (𝓞 ↥K₂) (𝓞 L)) (differentIdeal ℤ (𝓞 ↥K₂)))
Module: Mathlib.RingTheory.Ideal.Norm.RelNorm

Goal state before:
pp: case neg
R : Type u_1
inst✝¹¹ : CommRing R
inst✝¹⁰ : IsDomain R
S : Type u_3
inst✝⁹ : CommRing S
inst✝⁸ : IsDomain S
inst✝⁷ : IsIntegrallyClosed R
inst✝⁶ : IsIntegrallyClosed S
inst✝⁵ : Algebra R S
inst✝⁴ : Module.Finite R S
inst✝³ : IsTorsionFree R S
inst✝² : IsDedekindDomain R
inst✝¹ : IsDedekindDomain S
I J : Ideal S
inst✝ : Nontrivial R
h✝ : Nontrivial S
P : Ideal R
hP : P.IsMaximal
hP0 : ¬P = ⊥
this : NeZero P
P' : Submonoid S := Algebra.algebraMapSubmonoid S P.primeCompl
⊢ span
      {(Algebra.intNorm (Localization.AtPrime P) (Localization P'))
            (IsPrincipal.generator (map (algebraMap S (Localization P')) I)) *
          (Algebra.intNorm (Localization.AtPrime P) (Localization P'))
            (IsPrincipal.generator (map (algebraMap S (Localization P')) J))} =
    span
      {(Algebra.intNorm (Localization.AtPrime P) (Localization P'))
            (IsPrincipal.generator (map (algebraMap S (Localization P')) I)) *
          (Algebra.intNorm (Localization.AtPrime P) (Localization P'))
            (IsPrincipal.generator (map (algebraMap S (Localization P')) J))}

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Ideal.Norm.RelNorm

Goal state before:
pp: R : Type u_1
inst✝¹⁸ : CommRing R
inst✝¹⁷ : IsDomain R
S : Type u_3
inst✝¹⁶ : CommRing S
inst✝¹⁵ : IsDomain S
inst✝¹⁴ : IsIntegrallyClosed R
inst✝¹³ : IsIntegrallyClosed S
inst✝¹² : Algebra R S
inst✝¹¹ : Module.Finite R S
inst✝¹⁰ : IsTorsionFree R S
T : Type u_4
inst✝⁹ : CommRing T
inst✝⁸ : IsDomain T
inst✝⁷ : IsIntegrallyClosed T
inst✝⁶ : Algebra R T
inst✝⁵ : Algebra T S
inst✝⁴ : Module.Finite R T
inst✝³ : Module.Finite T S
inst✝² : IsTorsionFree R T
inst✝¹ : IsTorsionFree T S
inst✝ : IsScalarTower R T S
I : Ideal S
x : S
hx : x ∈ ↑I
⊢ (intNorm R S) x = (intNorm R S) x

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Discriminant.Different

Goal state before:
pp: L : Type u_3
inst✝¹ : Field L
inst✝ : NumberField L
K₁ K₂ : IntermediateField ℚ L
h₁ : K₁.LinearDisjoint ↥K₂
h₂ : K₁ ⊔ K₂ = ⊤
h₃ :
  IsCoprime (Ideal.map (algebraMap (𝓞 ↥K₁) (𝓞 L)) (differentIdeal ℤ (𝓞 ↥K₁)))
    (Ideal.map (algebraMap (𝓞 ↥K₂) (𝓞 L)) (differentIdeal ℤ (𝓞 ↥K₂)))
x✝ : Algebra (FractionRing (𝓞 ↥K₁)) (FractionRing (𝓞 L)) := FractionRing.liftAlgebra (𝓞 ↥K₁) (FractionRing (𝓞 L))
h_main : (discr L).natAbs = (discr ↥K₁).natAbs ^ finrank ℚ ↥K₂ * (discr ↥K₂).natAbs ^ finrank ℚ ↥K₁
⊢ (discr L).natAbs = (discr ↥K₁).natAbs ^ finrank ℚ ↥K₂ * (discr ↥K₂).natAbs ^ finrank ℚ ↥K₁

Tactic:
]

Goal state after:
L : Type u_3
inst✝¹ : Field L
inst✝ : NumberField L
K₁ K₂ : IntermediateField ℚ L
h₁ : K₁.LinearDisjoint ↥K₂
h₂ : K₁ ⊔ K₂ = ⊤
h₃ :
  IsCoprime (Ideal.map (algebraMap (𝓞 ↥K₁) (𝓞 L)) (differentIdeal ℤ (𝓞 ↥K₁)))
    (Ideal.map (algebraMap (𝓞 ↥K₂) (𝓞 L)) (differentIdeal ℤ (𝓞 ↥K₂)))
x✝ : Algebra (FractionRing (𝓞 ↥K₁)) (FractionRing (𝓞 L)) := FractionRing.liftAlgebra (𝓞 ↥K₁) (FractionRing (𝓞 L))
h_main : (discr L).natAbs = (discr ↥K₁).natAbs ^ finrank ℚ ↥K₂ * (discr ↥K₂).natAbs ^ finrank ℚ ↥K₁
⊢ (discr L).natAbs = (discr ↥K₁).natAbs ^ finrank ℚ ↥K₂ * (discr ↥K₂).natAbs ^ finrank ℚ ↥K₁
Module: Mathlib.RingTheory.Ideal.Norm.RelNorm

Goal state before:
pp: case inl
R : Type u_1
inst✝¹⁸ : CommRing R
inst✝¹⁷ : IsDomain R
S : Type u_3
inst✝¹⁶ : CommRing S
inst✝¹⁵ : IsDomain S
inst✝¹⁴ : IsIntegrallyClosed R
inst✝¹³ : IsIntegrallyClosed S
inst✝¹² : Algebra R S
inst✝¹¹ : Module.Finite R S
inst✝¹⁰ : IsTorsionFree R S
T : Type u_4
inst✝⁹ : CommRing T
inst✝⁸ : IsDomain T
inst✝⁷ : IsIntegrallyClosed T
inst✝⁶ : Algebra R T
inst✝⁵ : Algebra T S
inst✝⁴ : Module.Finite R T
inst✝³ : Module.Finite T S
inst✝² : IsTorsionFree R T
inst✝¹ : IsTorsionFree T S
inst✝ : IsScalarTower R T S
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I : Ideal S
h : spanNorm R I = ⊥
⊢ ⊥ = ⊥

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Discriminant.Different

Goal state before:
pp: case mp
K : Type u_1
𝒪 : Type u_2
inst✝⁴ : Field K
inst✝³ : NumberField K
inst✝² : CommRing 𝒪
inst✝¹ : Algebra 𝒪 K
inst✝ : IsIntegralClosure 𝒪 ℤ K
p : ℤ
hp : Prime p
this✝³ : IsDomain 𝒪
this✝² : IsDedekindDomain 𝒪
this✝¹ : IsFractionRing 𝒪 K
this✝ : Module.Finite ℤ 𝒪
this : CharZero 𝒪
h : p ∣ ↑(Ideal.absNorm (differentIdeal ℤ 𝒪))
⊢ ∃ P, P.IsMaximal ∧ P.LiesOver (Ideal.span {p}) ∧ P ∣ differentIdeal ℤ 𝒪

Tactic:
]

Goal state after:
case mp
K : Type u_1
𝒪 : Type u_2
inst✝⁴ : Field K
inst✝³ : NumberField K
inst✝² : CommRing 𝒪
inst✝¹ : Algebra 𝒪 K
inst✝ : IsIntegralClosure 𝒪 ℤ K
p : ℤ
hp : Prime p
this✝³ : IsDomain 𝒪
this✝² : IsDedekindDomain 𝒪
this✝¹ : IsFractionRing 𝒪 K
this✝ : Module.Finite ℤ 𝒪
this : CharZero 𝒪
h : p ∣ ↑(Ideal.absNorm (differentIdeal ℤ 𝒪))
⊢ ∃ P, P.IsMaximal ∧ P.LiesOver (Ideal.span {p}) ∧ P ∣ differentIdeal ℤ 𝒪
Module: Mathlib.RingTheory.Ideal.Norm.RelNorm

Goal state before:
pp: case pos
R : Type u_1
inst✝²¹ : CommRing R
inst✝²⁰ : IsDomain R
S : Type u_3
inst✝¹⁹ : CommRing S
inst✝¹⁸ : IsDomain S
inst✝¹⁷ : IsIntegrallyClosed R
inst✝¹⁶ : IsIntegrallyClosed S
inst✝¹⁵ : Algebra R S
inst✝¹⁴ : Module.Finite R S
inst✝¹³ : IsTorsionFree R S
T : Type u_4
inst✝¹² : CommRing T
inst✝¹¹ : IsDomain T
inst✝¹⁰ : IsIntegrallyClosed T
inst✝⁹ : Algebra R T
inst✝⁸ : Algebra T S
inst✝⁷ : Module.Finite R T
inst✝⁶ : Module.Finite T S
inst✝⁵ : IsTorsionFree R T
inst✝⁴ : IsTorsionFree T S
inst✝³ : IsScalarTower R T S
inst✝² : IsDedekindDomain R
inst✝¹ : IsDedekindDomain T
inst✝ : IsDedekindDomain S
I : Ideal S
hP : ⊥.IsMaximal
⊢ map (algebraMap R (Localization.AtPrime ⊥)) (spanNorm R I) =
    map (algebraMap R (Localization.AtPrime ⊥)) (spanNorm R I)

pp: case pos.eq_bot_or_top
R : Type u_1
inst✝²¹ : CommRing R
inst✝²⁰ : IsDomain R
S : Type u_3
inst✝¹⁹ : CommRing S
inst✝¹⁸ : IsDomain S
inst✝¹⁷ : IsIntegrallyClosed R
inst✝¹⁶ : IsIntegrallyClosed S
inst✝¹⁵ : Algebra R S
inst✝¹⁴ : Module.Finite R S
inst✝¹³ : IsTorsionFree R S
T : Type u_4
inst✝¹² : CommRing T
inst✝¹¹ : IsDomain T
inst✝¹⁰ : IsIntegrallyClosed T
inst✝⁹ : Algebra R T
inst✝⁸ : Algebra T S
inst✝⁷ : Module.Finite R T
inst✝⁶ : Module.Finite T S
inst✝⁵ : IsTorsionFree R T
inst✝⁴ : IsTorsionFree T S
inst✝³ : IsScalarTower R T S
inst✝² : IsDedekindDomain R
inst✝¹ : IsDedekindDomain T
inst✝ : IsDedekindDomain S
I : Ideal S
hP : ⊥.IsMaximal
⊢ ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤

Tactic:
]

Goal state after:
case pos.eq_bot_or_top
R : Type u_1
inst✝²¹ : CommRing R
inst✝²⁰ : IsDomain R
S : Type u_3
inst✝¹⁹ : CommRing S
inst✝¹⁸ : IsDomain S
inst✝¹⁷ : IsIntegrallyClosed R
inst✝¹⁶ : IsIntegrallyClosed S
inst✝¹⁵ : Algebra R S
inst✝¹⁴ : Module.Finite R S
inst✝¹³ : IsTorsionFree R S
T : Type u_4
inst✝¹² : CommRing T
inst✝¹¹ : IsDomain T
inst✝¹⁰ : IsIntegrallyClosed T
inst✝⁹ : Algebra R T
inst✝⁸ : Algebra T S
inst✝⁷ : Module.Finite R T
inst✝⁶ : Module.Finite T S
inst✝⁵ : IsTorsionFree R T
inst✝⁴ : IsTorsionFree T S
inst✝³ : IsScalarTower R T S
inst✝² : IsDedekindDomain R
inst✝¹ : IsDedekindDomain T
inst✝ : IsDedekindDomain S
I : Ideal S
hP : ⊥.IsMaximal
⊢ ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
Module: Mathlib.NumberTheory.NumberField.Discriminant.Different

Goal state before:
pp: case mpr
K : Type u_1
𝒪 : Type u_2
inst✝⁴ : Field K
inst✝³ : NumberField K
inst✝² : CommRing 𝒪
inst✝¹ : Algebra 𝒪 K
inst✝ : IsIntegralClosure 𝒪 ℤ K
p : ℤ
hp : Prime p
this✝⁴ : IsDomain 𝒪
this✝³ : IsDedekindDomain 𝒪
this✝² : IsFractionRing 𝒪 K
this✝¹ : Module.Finite ℤ 𝒪
this✝ : CharZero 𝒪
P : Ideal 𝒪
hP : P.IsMaximal
hP' : P.LiesOver (Ideal.span {p})
hP'' : P ∣ differentIdeal ℤ 𝒪
this : p ^ P.inertiaDeg ℤ ∣ discr K
⊢ p ∣ discr K

Tactic:
]

Goal state after:
case mpr
K : Type u_1
𝒪 : Type u_2
inst✝⁴ : Field K
inst✝³ : NumberField K
inst✝² : CommRing 𝒪
inst✝¹ : Algebra 𝒪 K
inst✝ : IsIntegralClosure 𝒪 ℤ K
p : ℤ
hp : Prime p
this✝⁴ : IsDomain 𝒪
this✝³ : IsDedekindDomain 𝒪
this✝² : IsFractionRing 𝒪 K
this✝¹ : Module.Finite ℤ 𝒪
this✝ : CharZero 𝒪
P : Ideal 𝒪
hP : P.IsMaximal
hP' : P.LiesOver (Ideal.span {p})
hP'' : P ∣ differentIdeal ℤ 𝒪
this : p ^ P.inertiaDeg ℤ ∣ discr K
⊢ p ∣ discr K
Module: Mathlib.RingTheory.Ideal.Norm.RelNorm

Goal state before:
pp: case neg
R : Type u_1
inst✝²¹ : CommRing R
inst✝²⁰ : IsDomain R
S : Type u_3
inst✝¹⁹ : CommRing S
inst✝¹⁸ : IsDomain S
inst✝¹⁷ : IsIntegrallyClosed R
inst✝¹⁶ : IsIntegrallyClosed S
inst✝¹⁵ : Algebra R S
inst✝¹⁴ : Module.Finite R S
inst✝¹³ : IsTorsionFree R S
T : Type u_4
inst✝¹² : CommRing T
inst✝¹¹ : IsDomain T
inst✝¹⁰ : IsIntegrallyClosed T
inst✝⁹ : Algebra R T
inst✝⁸ : Algebra T S
inst✝⁷ : Module.Finite R T
inst✝⁶ : Module.Finite T S
inst✝⁵ : IsTorsionFree R T
inst✝⁴ : IsTorsionFree T S
inst✝³ : IsScalarTower R T S
inst✝² : IsDedekindDomain R
inst✝¹ : IsDedekindDomain T
inst✝ : IsDedekindDomain S
I : Ideal S
P : Ideal R
hP✝ : P.IsMaximal
hP : ¬P = ⊥
Rₚ : Type u_1 := Localization.AtPrime P
Tₚ : Type u_4 := Localization (algebraMapSubmonoid T P.primeCompl)
Sₚ : Type u_3 := Localization (algebraMapSubmonoid S P.primeCompl)
this : NeZero P
h : algebraMapSubmonoid T P.primeCompl ≤ T⁰
⊢ span {(intNorm (Localization.AtPrime P) Sₚ) (IsPrincipal.generator (map (algebraMap S Sₚ) I))} =
    span {(intNorm Rₚ Sₚ) (IsPrincipal.generator (map (algebraMap S Sₚ) I))}

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Ideal.Norm.RelNorm

Goal state before:
pp: R : Type u_1
S✝ : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
S : Type u_3
inst✝⁸ : CommRing S
inst✝⁷ : IsDomain S
inst✝⁶ : IsIntegrallyClosed R
inst✝⁵ : IsIntegrallyClosed S
inst✝⁴ : Algebra R S
inst✝³ : Module.Finite R S
inst✝² : IsTorsionFree R S
inst✝¹ : IsDedekindDomain R
inst✝ : IsDedekindDomain S
⊢ ⊤ = ⊤

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Ideal.Norm.RelNorm

Goal state before:
pp: R : Type u_1
inst✝¹⁶ : CommRing R
inst✝¹⁵ : IsDomain R
S : Type u_3
inst✝¹⁴ : CommRing S
inst✝¹³ : IsDomain S
inst✝¹² : IsIntegrallyClosed R
inst✝¹¹ : IsIntegrallyClosed S
inst✝¹⁰ : Algebra R S
inst✝⁹ : Module.Finite R S
inst✝⁸ : IsTorsionFree R S
inst✝⁷ : IsDedekindDomain R
inst✝⁶ : IsDedekindDomain S
T : Type u_4
inst✝⁵ : CommRing T
inst✝⁴ : IsDedekindDomain T
inst✝³ : IsIntegrallyClosed T
inst✝² : Algebra R T
inst✝¹ : Module.Finite R T
inst✝ : IsTorsionFree R T
σ : S ≃ₐ[R] T
I : Ideal S
x✝¹ : R
x✝ : x✝¹ ∈ ⇑(Algebra.intNorm R T) '' ↑(map σ I)
x : T
hx₁ : x ∈ ↑(map σ I)
hx₂ : (Algebra.intNorm R T) x = x✝¹
⊢ x ∈ map σ.toRingEquiv I

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹⁶ : CommRing R
inst✝¹⁵ : IsDomain R
S : Type u_3
inst✝¹⁴ : CommRing S
inst✝¹³ : IsDomain S
inst✝¹² : IsIntegrallyClosed R
inst✝¹¹ : IsIntegrallyClosed S
inst✝¹⁰ : Algebra R S
inst✝⁹ : Module.Finite R S
inst✝⁸ : IsTorsionFree R S
inst✝⁷ : IsDedekindDomain R
inst✝⁶ : IsDedekindDomain S
T : Type u_4
inst✝⁵ : CommRing T
inst✝⁴ : IsDedekindDomain T
inst✝³ : IsIntegrallyClosed T
inst✝² : Algebra R T
inst✝¹ : Module.Finite R T
inst✝ : IsTorsionFree R T
σ : S ≃ₐ[R] T
I : Ideal S
x✝¹ : R
x✝ : x✝¹ ∈ ⇑(Algebra.intNorm R T) '' ↑(map σ I)
x : T
hx₁ : x ∈ ↑(map σ I)
hx₂ : (Algebra.intNorm R T) x = x✝¹
⊢ x ∈ map σ.toRingEquiv I
Module: Mathlib.NumberTheory.NumberField.Discriminant.Different

Goal state before:
pp: K : Type u_1
𝒪 : Type u_2
inst✝⁴ : Field K
inst✝³ : NumberField K
inst✝² : CommRing 𝒪
inst✝¹ : Algebra 𝒪 K
inst✝ : IsIntegralClosure 𝒪 ℤ K
p : ℤ
hp : Prime p
this✝¹ : IsDomain 𝒪
this✝ : IsDedekindDomain 𝒪
this : CharZero 𝒪
⊢ (∀ (P : Ideal 𝒪) (x : P.IsMaximal), P.LiesOver (Ideal.span {p}) → Algebra.IsUnramifiedAt ℤ P) ↔
    Algebra.IsUnramifiedIn 𝒪 (Ideal.span {p})

Tactic:
]

Goal state after:
K : Type u_1
𝒪 : Type u_2
inst✝⁴ : Field K
inst✝³ : NumberField K
inst✝² : CommRing 𝒪
inst✝¹ : Algebra 𝒪 K
inst✝ : IsIntegralClosure 𝒪 ℤ K
p : ℤ
hp : Prime p
this✝¹ : IsDomain 𝒪
this✝ : IsDedekindDomain 𝒪
this : CharZero 𝒪
⊢ (∀ (P : Ideal 𝒪) (x : P.IsMaximal), P.LiesOver (Ideal.span {p}) → Algebra.IsUnramifiedAt ℤ P) ↔
    Algebra.IsUnramifiedIn 𝒪 (Ideal.span {p})
Module: Mathlib.NumberTheory.NumberField.Discriminant.Different

Goal state before:
pp: K : Type u_1
𝒪 : Type u_2
inst✝⁴ : Field K
inst✝³ : NumberField K
inst✝² : CommRing 𝒪
inst✝¹ : Algebra 𝒪 K
inst✝ : IsIntegralClosure 𝒪 ℤ K
p : ℤ
hp : Prime p
this✝¹ : IsDomain 𝒪
this✝ : IsDedekindDomain 𝒪
this : CharZero 𝒪
⊢ (∀ (P : Ideal 𝒪) (x : P.IsMaximal), P.LiesOver (Ideal.span {p}) → Algebra.IsUnramifiedAt ℤ P) ↔
    ∀ (P : Ideal 𝒪) (x : P.IsPrime), ↑p ∈ P → Algebra.IsUnramifiedAt ℤ P

Tactic:
]

Goal state after:
K : Type u_1
𝒪 : Type u_2
inst✝⁴ : Field K
inst✝³ : NumberField K
inst✝² : CommRing 𝒪
inst✝¹ : Algebra 𝒪 K
inst✝ : IsIntegralClosure 𝒪 ℤ K
p : ℤ
hp : Prime p
this✝¹ : IsDomain 𝒪
this✝ : IsDedekindDomain 𝒪
this : CharZero 𝒪
⊢ (∀ (P : Ideal 𝒪) (x : P.IsMaximal), P.LiesOver (Ideal.span {p}) → Algebra.IsUnramifiedAt ℤ P) ↔
    ∀ (P : Ideal 𝒪) (x : P.IsPrime), ↑p ∈ P → Algebra.IsUnramifiedAt ℤ P
Module: Mathlib.RingTheory.Ideal.Norm.RelNorm

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
S : Type u_3
inst✝⁸ : CommRing S
inst✝⁷ : IsDomain S
inst✝⁶ : IsIntegrallyClosed R
inst✝⁵ : IsIntegrallyClosed S
inst✝⁴ : Algebra R S
inst✝³ : Module.Finite R S
inst✝² : IsTorsionFree R S
inst✝¹ : IsDedekindDomain R
inst✝ : IsDedekindDomain S
I : Ideal R
⊢ spanNorm R (map (algebraMap R S) I) = I ^ finrank R S

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
S : Type u_3
inst✝⁸ : CommRing S
inst✝⁷ : IsDomain S
inst✝⁶ : IsIntegrallyClosed R
inst✝⁵ : IsIntegrallyClosed S
inst✝⁴ : Algebra R S
inst✝³ : Module.Finite R S
inst✝² : IsTorsionFree R S
inst✝¹ : IsDedekindDomain R
inst✝ : IsDedekindDomain S
I : Ideal R
⊢ spanNorm R (map (algebraMap R S) I) = I ^ finrank R S
Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral

Goal state before:
pp: case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
⊢ ((cyclotomic p ℤ).comp (X + C 1)).Monic

Tactic:
]

Goal state after:
case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
⊢ ((cyclotomic p ℤ).comp (X + C 1)).Monic
Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral

Goal state before:
pp: case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
h : 1 = 0
⊢ False

Tactic:
]

Goal state after:
case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
h : 1 = 0
⊢ False
Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral

Goal state before:
pp: case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
i : ℕ
hi : i < ((cyclotomic p ℤ).comp (X + 1)).natDegree
⊢ ∑ x ∈ range p, (lcoeff ℤ i) (↑(p.choose (x + 1)) * X ^ x) ∈ ℤ ∙ ↑p

Tactic:
]

Goal state after:
case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
i : ℕ
hi : i < ((cyclotomic p ℤ).comp (X + 1)).natDegree
⊢ ∑ x ∈ range p, (lcoeff ℤ i) (↑(p.choose (x + 1)) * X ^ x) ∈ ℤ ∙ ↑p
Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral

Goal state before:
pp: case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
i : ℕ
hi : i < p - 1
⊢ (∑ x ∈ range p, if x = i then ↑(p.choose (x + 1)) else 0) ∈ ℤ ∙ ↑p

Tactic:
]

Goal state after:
case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
i : ℕ
hi : i < p - 1
⊢ (∑ x ∈ range p, if x = i then ↑(p.choose (x + 1)) else 0) ∈ ℤ ∙ ↑p
Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral

Goal state before:
pp: case refine_3
p : ℕ
hp : Fact (Nat.Prime p)
⊢ eval (0 + eval 0 1) (∑ i ∈ range p, X ^ i) ∉ (ℤ ∙ ↑p) ^ 2

Tactic:
eval_one,

Goal state after:
case refine_3
p : ℕ
hp : Fact (Nat.Prime p)
⊢ eval (0 + 1) (∑ i ∈ range p, X ^ i) ∉ (ℤ ∙ ↑p) ^ 2
Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral

Goal state before:
pp: case refine_3
p : ℕ
hp : Fact (Nat.Prime p)
⊢ ¬↑p ^ 2 ∣ ↑p

Tactic:
]

Goal state after:
case refine_3
p : ℕ
hp : Fact (Nat.Prime p)
⊢ ¬↑p ^ 2 ∣ ↑p
Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral

Goal state before:
pp: case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ((cyclotomic (p ^ (n + 1)) ℤ).comp (X + C 1)).Monic

Tactic:
]

Goal state after:
case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ((cyclotomic (p ^ (n + 1)) ℤ).comp (X + C 1)).Monic
Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral

Goal state before:
pp: case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
h : 1 = 0
⊢ False

Tactic:
]

Goal state after:
case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
h : 1 = 0
⊢ False