internlm/Lean-Github huggingface dataset:
Theorem: Ideal.spanIntNorm_mul
Proof state before:
case neg
R : Type u_1
inst✝¹⁵ : CommRing R
S : Type u_2
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
inst✝¹² : IsIntegrallyClosed R
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : NoZeroSMulDivisors R S
hRS : Module.Finite R S
inst✝⁸ : IsIntegrallyClosed S
inst✝⁷ : IsSeparable (FractionRing R) (FractionRing S)
inst✝⁶ : IsDomain R
inst✝⁵ : IsDomain S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDedekindDomain S
inst✝² : Module.Finite R S
inst✝¹ : Module.Free R S
I J : Ideal S
inst✝ : Nontrivial R
h✝ : Nontrivial S
P : Ideal R
hP : P.IsMaximal
hP0 : ¬P = ⊥
P' : Submonoid S := Algebra.algebraMapSubmonoid S P.primeCompl
Rₚ : Type u_1 := Localization.AtPrime P
⊢ map (algebraMap R (Localization.AtPrime P)) (spanIntNorm R (I * J)) =
    map (algebraMap R (Localization.AtPrime P)) (spanIntNorm R I * spanIntNorm R J)
Tactic:
let Sₚ := Localization P'
Proof state after:
case neg
R : Type u_1
inst✝¹⁵ : CommRing R
S : Type u_2
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
inst✝¹² : IsIntegrallyClosed R
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : NoZeroSMulDivisors R S
hRS : Module.Finite R S
inst✝⁸ : IsIntegrallyClosed S
inst✝⁷ : IsSeparable (FractionRing R) (FractionRing S)
inst✝⁶ : IsDomain R
inst✝⁵ : IsDomain S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDedekindDomain S
inst✝² : Module.Finite R S
inst✝¹ : Module.Free R S
I J : Ideal S
inst✝ : Nontrivial R
h✝ : Nontrivial S
P : Ideal R
hP : P.IsMaximal
hP0 : ¬P = ⊥
P' : Submonoid S := Algebra.algebraMapSubmonoid S P.primeCompl
Rₚ : Type u_1 := Localization.AtPrime P
Sₚ : Type u_2 := Localization P'
⊢ map (algebraMap R (Localization.AtPrime P)) (spanIntNorm R (I * J)) =
    map (algebraMap R (Localization.AtPrime P)) (spanIntNorm R I * spanIntNorm R J)
Theorem: Ideal.spanIntNorm_mul
Proof state before:
case neg
R : Type u_1
inst✝¹⁵ : CommRing R
S : Type u_2
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
inst✝¹² : IsIntegrallyClosed R
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : NoZeroSMulDivisors R S
hRS : Module.Finite R S
inst✝⁸ : IsIntegrallyClosed S
inst✝⁷ : IsSeparable (FractionRing R) (FractionRing S)
inst✝⁶ : IsDomain R
inst✝⁵ : IsDomain S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDedekindDomain S
inst✝² : Module.Finite R S
inst✝¹ : Module.Free R S
I J : Ideal S
inst✝ : Nontrivial R
h✝ : Nontrivial S
P : Ideal R
hP : P.IsMaximal
hP0 : ¬P = ⊥
P' : Submonoid S := Algebra.algebraMapSubmonoid S P.primeCompl
Rₚ : Type u_1 := Localization.AtPrime P
Sₚ : Type u_2 := Localization P'
⊢ map (algebraMap R (Localization.AtPrime P)) (spanIntNorm R (I * J)) =
    map (algebraMap R (Localization.AtPrime P)) (spanIntNorm R I * spanIntNorm R J)
Tactic:
letI : Algebra Rₚ Sₚ := localizationAlgebra P.primeCompl S
Proof state after:
case neg
R : Type u_1
inst✝¹⁵ : CommRing R
S : Type u_2
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
inst✝¹² : IsIntegrallyClosed R
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : NoZeroSMulDivisors R S
hRS : Module.Finite R S
inst✝⁸ : IsIntegrallyClosed S
inst✝⁷ : IsSeparable (FractionRing R) (FractionRing S)
inst✝⁶ : IsDomain R
inst✝⁵ : IsDomain S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDedekindDomain S
inst✝² : Module.Finite R S
inst✝¹ : Module.Free R S
I J : Ideal S
inst✝ : Nontrivial R
h✝ : Nontrivial S
P : Ideal R
hP : P.IsMaximal
hP0 : ¬P = ⊥
P' : Submonoid S := Algebra.algebraMapSubmonoid S P.primeCompl
Rₚ : Type u_1 := Localization.AtPrime P
Sₚ : Type u_2 := Localization P'
this : Algebra Rₚ Sₚ := localizationAlgebra P.primeCompl S
⊢ map (algebraMap R (Localization.AtPrime P)) (spanIntNorm R (I * J)) =
    map (algebraMap R (Localization.AtPrime P)) (spanIntNorm R I * spanIntNorm R J)
Theorem: Ideal.spanIntNorm_mul
Proof state before:
case neg
R : Type u_1
inst✝¹⁵ : CommRing R
S : Type u_2
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
inst✝¹² : IsIntegrallyClosed R
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : NoZeroSMulDivisors R S
hRS : Module.Finite R S
inst✝⁸ : IsIntegrallyClosed S
inst✝⁷ : IsSeparable (FractionRing R) (FractionRing S)
inst✝⁶ : IsDomain R
inst✝⁵ : IsDomain S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDedekindDomain S
inst✝² : Module.Finite R S
inst✝¹ : Module.Free R S
I J : Ideal S
inst✝ : Nontrivial R
h✝ : Nontrivial S
P : Ideal R
hP : P.IsMaximal
hP0 : ¬P = ⊥
P' : Submonoid S := Algebra.algebraMapSubmonoid S P.primeCompl
Rₚ : Type u_1 := Localization.AtPrime P
Sₚ : Type u_2 := Localization P'
this : Algebra Rₚ Sₚ := localizationAlgebra P.primeCompl S
⊢ map (algebraMap R (Localization.AtPrime P)) (spanIntNorm R (I * J)) =
    map (algebraMap R (Localization.AtPrime P)) (spanIntNorm R I * spanIntNorm R J)
Tactic:
haveI : IsScalarTower R Rₚ Sₚ :=
  IsScalarTower.of_algebraMap_eq (fun x =>
    (IsLocalization.map_eq (T := P') (Q := Localization P') P.primeCompl.le_comap_map x).symm)
Proof state after:
case neg
R : Type u_1
inst✝¹⁵ : CommRing R
S : Type u_2
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
inst✝¹² : IsIntegrallyClosed R
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : NoZeroSMulDivisors R S
hRS : Module.Finite R S
inst✝⁸ : IsIntegrallyClosed S
inst✝⁷ : IsSeparable (FractionRing R) (FractionRing S)
inst✝⁶ : IsDomain R
inst✝⁵ : IsDomain S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDedekindDomain S
inst✝² : Module.Finite R S
inst✝¹ : Module.Free R S
I J : Ideal S
inst✝ : Nontrivial R
h✝ : Nontrivial S
P : Ideal R
hP : P.IsMaximal
hP0 : ¬P = ⊥
P' : Submonoid S := Algebra.algebraMapSubmonoid S P.primeCompl
Rₚ : Type u_1 := Localization.AtPrime P
Sₚ : Type u_2 := Localization P'
this✝ : Algebra Rₚ Sₚ := localizationAlgebra P.primeCompl S
this : IsScalarTower R Rₚ Sₚ
⊢ map (algebraMap R (Localization.AtPrime P)) (spanIntNorm R (I * J)) =
    map (algebraMap R (Localization.AtPrime P)) (spanIntNorm R I * spanIntNorm R J)
Theorem: Ideal.spanIntNorm_mul
Proof state before:
case neg
R : Type u_1
inst✝¹⁵ : CommRing R
S : Type u_2
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
inst✝¹² : IsIntegrallyClosed R
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : NoZeroSMulDivisors R S
hRS : Module.Finite R S
inst✝⁸ : IsIntegrallyClosed S
inst✝⁷ : IsSeparable (FractionRing R) (FractionRing S)
inst✝⁶ : IsDomain R
inst✝⁵ : IsDomain S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDedekindDomain S
inst✝² : Module.Finite R S
inst✝¹ : Module.Free R S
I J : Ideal S
inst✝ : Nontrivial R
h✝ : Nontrivial S
P : Ideal R
hP : P.IsMaximal
hP0 : ¬P = ⊥
P' : Submonoid S := Algebra.algebraMapSubmonoid S P.primeCompl
Rₚ : Type u_1 := Localization.AtPrime P
Sₚ : Type u_2 := Localization P'
this✝ : Algebra Rₚ Sₚ := localizationAlgebra P.primeCompl S
this : IsScalarTower R Rₚ Sₚ
⊢ map (algebraMap R (Localization.AtPrime P)) (spanIntNorm R (I * J)) =
    map (algebraMap R (Localization.AtPrime P)) (spanIntNorm R I * spanIntNorm R J)
Tactic:
have h : P' ≤ S⁰ :=
  map_le_nonZeroDivisors_of_injective _ (NoZeroSMulDivisors.algebraMap_injective _ _)
    P.primeCompl_le_nonZeroDivisors
Proof state after:
case neg
R : Type u_1
inst✝¹⁵ : CommRing R
S : Type u_2
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
inst✝¹² : IsIntegrallyClosed R
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : NoZeroSMulDivisors R S
hRS : Module.Finite R S
inst✝⁸ : IsIntegrallyClosed S
inst✝⁷ : IsSeparable (FractionRing R) (FractionRing S)
inst✝⁶ : IsDomain R
inst✝⁵ : IsDomain S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDedekindDomain S
inst✝² : Module.Finite R S
inst✝¹ : Module.Free R S
I J : Ideal S
inst✝ : Nontrivial R
h✝ : Nontrivial S
P : Ideal R
hP : P.IsMaximal
hP0 : ¬P = ⊥
P' : Submonoid S := Algebra.algebraMapSubmonoid S P.primeCompl
Rₚ : Type u_1 := Localization.AtPrime P
Sₚ : Type u_2 := Localization P'
this✝ : Algebra Rₚ Sₚ := localizationAlgebra P.primeCompl S
this : IsScalarTower R Rₚ Sₚ
h : P' ≤ S⁰
⊢ map (algebraMap R (Localization.AtPrime P)) (spanIntNorm R (I * J)) =
    map (algebraMap R (Localization.AtPrime P)) (spanIntNorm R I * spanIntNorm R J)
Theorem: Ideal.spanIntNorm_mul
Proof state before:
case neg
R : Type u_1
inst✝¹⁵ : CommRing R
S : Type u_2
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
inst✝¹² : IsIntegrallyClosed R
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : NoZeroSMulDivisors R S
hRS : Module.Finite R S
inst✝⁸ : IsIntegrallyClosed S
inst✝⁷ : IsSeparable (FractionRing R) (FractionRing S)
inst✝⁶ : IsDomain R
inst✝⁵ : IsDomain S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDedekindDomain S
inst✝² : Module.Finite R S
inst✝¹ : Module.Free R S
I J : Ideal S
inst✝ : Nontrivial R
h✝ : Nontrivial S
P : Ideal R
hP : P.IsMaximal
hP0 : ¬P = ⊥
P' : Submonoid S := Algebra.algebraMapSubmonoid S P.primeCompl
Rₚ : Type u_1 := Localization.AtPrime P
Sₚ : Type u_2 := Localization P'
this✝ : Algebra Rₚ Sₚ := localizationAlgebra P.primeCompl S
this : IsScalarTower R Rₚ Sₚ
h : P' ≤ S⁰
⊢ map (algebraMap R (Localization.AtPrime P)) (spanIntNorm R (I * J)) =
    map (algebraMap R (Localization.AtPrime P)) (spanIntNorm R I * spanIntNorm R J)
Tactic:
haveI : IsDomain Sₚ := IsLocalization.isDomain_localization h
Proof state after:
case neg
R : Type u_1
inst✝¹⁵ : CommRing R
S : Type u_2
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
inst✝¹² : IsIntegrallyClosed R
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : NoZeroSMulDivisors R S
hRS : Module.Finite R S
inst✝⁸ : IsIntegrallyClosed S
inst✝⁷ : IsSeparable (FractionRing R) (FractionRing S)
inst✝⁶ : IsDomain R
inst✝⁵ : IsDomain S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDedekindDomain S
inst✝² : Module.Finite R S
inst✝¹ : Module.Free R S
I J : Ideal S
inst✝ : Nontrivial R
h✝ : Nontrivial S
P : Ideal R
hP : P.IsMaximal
hP0 : ¬P = ⊥
P' : Submonoid S := Algebra.algebraMapSubmonoid S P.primeCompl
Rₚ : Type u_1 := Localization.AtPrime P
Sₚ : Type u_2 := Localization P'
this✝¹ : Algebra Rₚ Sₚ := localizationAlgebra P.primeCompl S
this✝ : IsScalarTower R Rₚ Sₚ
h : P' ≤ S⁰
this : IsDomain Sₚ
⊢ map (algebraMap R (Localization.AtPrime P)) (spanIntNorm R (I * J)) =
    map (algebraMap R (Localization.AtPrime P)) (spanIntNorm R I * spanIntNorm R J)
Theorem: Ideal.spanIntNorm_mul
Proof state before:
case neg
R : Type u_1
inst✝¹⁵ : CommRing R
S : Type u_2
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
inst✝¹² : IsIntegrallyClosed R
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : NoZeroSMulDivisors R S
hRS : Module.Finite R S
inst✝⁸ : IsIntegrallyClosed S
inst✝⁷ : IsSeparable (FractionRing R) (FractionRing S)
inst✝⁶ : IsDomain R
inst✝⁵ : IsDomain S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDedekindDomain S
inst✝² : Module.Finite R S
inst✝¹ : Module.Free R S
I J : Ideal S
inst✝ : Nontrivial R
h✝ : Nontrivial S
P : Ideal R
hP : P.IsMaximal
hP0 : ¬P = ⊥
P' : Submonoid S := Algebra.algebraMapSubmonoid S P.primeCompl
Rₚ : Type u_1 := Localization.AtPrime P
Sₚ : Type u_2 := Localization P'
this✝¹ : Algebra Rₚ Sₚ := localizationAlgebra P.primeCompl S
this✝ : IsScalarTower R Rₚ Sₚ
h : P' ≤ S⁰
this : IsDomain Sₚ
⊢ map (algebraMap R (Localization.AtPrime P)) (spanIntNorm R (I * J)) =
    map (algebraMap R (Localization.AtPrime P)) (spanIntNorm R I * spanIntNorm R J)
Tactic:
haveI : IsDedekindDomain Sₚ := IsLocalization.isDedekindDomain S h _
Proof state after:
case neg
R : Type u_1
inst✝¹⁵ : CommRing R
S : Type u_2
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
inst✝¹² : IsIntegrallyClosed R
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : NoZeroSMulDivisors R S
hRS : Module.Finite R S
inst✝⁸ : IsIntegrallyClosed S
inst✝⁷ : IsSeparable (FractionRing R) (FractionRing S)
inst✝⁶ : IsDomain R
inst✝⁵ : IsDomain S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDedekindDomain S
inst✝² : Module.Finite R S
inst✝¹ : Module.Free R S
I J : Ideal S
inst✝ : Nontrivial R
h✝ : Nontrivial S
P : Ideal R
hP : P.IsMaximal
hP0 : ¬P = ⊥
P' : Submonoid S := Algebra.algebraMapSubmonoid S P.primeCompl
Rₚ : Type u_1 := Localization.AtPrime P
Sₚ : Type u_2 := Localization P'
this✝² : Algebra Rₚ Sₚ := localizationAlgebra P.primeCompl S
this✝¹ : IsScalarTower R Rₚ Sₚ
h : P' ≤ S⁰
this✝ : IsDomain Sₚ
this : IsDedekindDomain Sₚ
⊢ map (algebraMap R (Localization.AtPrime P)) (spanIntNorm R (I * J)) =
    map (algebraMap R (Localization.AtPrime P)) (spanIntNorm R I * spanIntNorm R J)
Theorem: Ideal.spanIntNorm_mul
Proof state before:
case neg
R : Type u_1
inst✝¹⁵ : CommRing R
S : Type u_2
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
inst✝¹² : IsIntegrallyClosed R
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : NoZeroSMulDivisors R S
hRS : Module.Finite R S
inst✝⁸ : IsIntegrallyClosed S
inst✝⁷ : IsSeparable (FractionRing R) (FractionRing S)
inst✝⁶ : IsDomain R
inst✝⁵ : IsDomain S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDedekindDomain S
inst✝² : Module.Finite R S
inst✝¹ : Module.Free R S
I J : Ideal S
inst✝ : Nontrivial R
h✝ : Nontrivial S
P : Ideal R
hP : P.IsMaximal
hP0 : ¬P = ⊥
P' : Submonoid S := Algebra.algebraMapSubmonoid S P.primeCompl
Rₚ : Type u_1 := Localization.AtPrime P
Sₚ : Type u_2 := Localization P'
this✝² : Algebra Rₚ Sₚ := localizationAlgebra P.primeCompl S
this✝¹ : IsScalarTower R Rₚ Sₚ
h : P' ≤ S⁰
this✝ : IsDomain Sₚ
this : IsDedekindDomain Sₚ
⊢ map (algebraMap R (Localization.AtPrime P)) (spanIntNorm R (I * J)) =
    map (algebraMap R (Localization.AtPrime P)) (spanIntNorm R I * spanIntNorm R J)
Tactic:
haveI : IsPrincipalIdealRing Sₚ :=
  IsDedekindDomain.isPrincipalIdealRing_localization_over_prime S P hP0
Proof state after:
case neg
R : Type u_1
inst✝¹⁵ : CommRing R
S : Type u_2
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
inst✝¹² : IsIntegrallyClosed R
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : NoZeroSMulDivisors R S
hRS : Module.Finite R S
inst✝⁸ : IsIntegrallyClosed S
inst✝⁷ : IsSeparable (FractionRing R) (FractionRing S)
inst✝⁶ : IsDomain R
inst✝⁵ : IsDomain S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDedekindDomain S
inst✝² : Module.Finite R S
inst✝¹ : Module.Free R S
I J : Ideal S
inst✝ : Nontrivial R
h✝ : Nontrivial S
P : Ideal R
hP : P.IsMaximal
hP0 : ¬P = ⊥
P' : Submonoid S := Algebra.algebraMapSubmonoid S P.primeCompl
Rₚ : Type u_1 := Localization.AtPrime P
Sₚ : Type u_2 := Localization P'
this✝³ : Algebra Rₚ Sₚ := localizationAlgebra P.primeCompl S
this✝² : IsScalarTower R Rₚ Sₚ
h : P' ≤ S⁰
this✝¹ : IsDomain Sₚ
this✝ : IsDedekindDomain Sₚ
this : IsPrincipalIdealRing Sₚ
⊢ map (algebraMap R (Localization.AtPrime P)) (spanIntNorm R (I * J)) =
    map (algebraMap R (Localization.AtPrime P)) (spanIntNorm R I * spanIntNorm R J)
Theorem: Ideal.spanIntNorm_mul
Proof state before:
case neg
R : Type u_1
inst✝¹⁵ : CommRing R
S : Type u_2
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
inst✝¹² : IsIntegrallyClosed R
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : NoZeroSMulDivisors R S
hRS : Module.Finite R S
inst✝⁸ : IsIntegrallyClosed S
inst✝⁷ : IsSeparable (FractionRing R) (FractionRing S)
inst✝⁶ : IsDomain R
inst✝⁵ : IsDomain S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDedekindDomain S
inst✝² : Module.Finite R S
inst✝¹ : Module.Free R S
I J : Ideal S
inst✝ : Nontrivial R
h✝ : Nontrivial S
P : Ideal R
hP : P.IsMaximal
hP0 : ¬P = ⊥
P' : Submonoid S := Algebra.algebraMapSubmonoid S P.primeCompl
Rₚ : Type u_1 := Localization.AtPrime P
Sₚ : Type u_2 := Localization P'
this✝³ : Algebra Rₚ Sₚ := localizationAlgebra P.primeCompl S
this✝² : IsScalarTower R Rₚ Sₚ
h : P' ≤ S⁰
this✝¹ : IsDomain Sₚ
this✝ : IsDedekindDomain Sₚ
this : IsPrincipalIdealRing Sₚ
⊢ map (algebraMap R (Localization.AtPrime P)) (spanIntNorm R (I * J)) =
    map (algebraMap R (Localization.AtPrime P)) (spanIntNorm R I * spanIntNorm R J)
Tactic:
haveI := isIntegrallyClosed_of_isLocalization P.primeCompl P.primeCompl_le_nonZeroDivisors Rₚ
Proof state after:
case neg
R : Type u_1
inst✝¹⁵ : CommRing R
S : Type u_2
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
inst✝¹² : IsIntegrallyClosed R
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : NoZeroSMulDivisors R S
hRS : Module.Finite R S
inst✝⁸ : IsIntegrallyClosed S
inst✝⁷ : IsSeparable (FractionRing R) (FractionRing S)
inst✝⁶ : IsDomain R
inst✝⁵ : IsDomain S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDedekindDomain S
inst✝² : Module.Finite R S
inst✝¹ : Module.Free R S
I J : Ideal S
inst✝ : Nontrivial R
h✝ : Nontrivial S
P : Ideal R
hP : P.IsMaximal
hP0 : ¬P = ⊥
P' : Submonoid S := Algebra.algebraMapSubmonoid S P.primeCompl
Rₚ : Type u_1 := Localization.AtPrime P
Sₚ : Type u_2 := Localization P'
this✝⁴ : Algebra Rₚ Sₚ := localizationAlgebra P.primeCompl S
this✝³ : IsScalarTower R Rₚ Sₚ
h : P' ≤ S⁰
this✝² : IsDomain Sₚ
this✝¹ : IsDedekindDomain Sₚ
this✝ : IsPrincipalIdealRing Sₚ
this : IsIntegrallyClosed Rₚ
⊢ map (algebraMap R (Localization.AtPrime P)) (spanIntNorm R (I * J)) =
    map (algebraMap R (Localization.AtPrime P)) (spanIntNorm R I * spanIntNorm R J)
Theorem: Ideal.spanIntNorm_mul
Proof state before:
case neg
R : Type u_1
inst✝¹⁵ : CommRing R
S : Type u_2
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
inst✝¹² : IsIntegrallyClosed R
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : NoZeroSMulDivisors R S
hRS : Module.Finite R S
inst✝⁸ : IsIntegrallyClosed S
inst✝⁷ : IsSeparable (FractionRing R) (FractionRing S)
inst✝⁶ : IsDomain R
inst✝⁵ : IsDomain S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDedekindDomain S
inst✝² : Module.Finite R S
inst✝¹ : Module.Free R S
I J : Ideal S
inst✝ : Nontrivial R
h✝ : Nontrivial S
P : Ideal R
hP : P.IsMaximal
hP0 : ¬P = ⊥
P' : Submonoid S := Algebra.algebraMapSubmonoid S P.primeCompl
Rₚ : Type u_1 := Localization.AtPrime P
Sₚ : Type u_2 := Localization P'
this✝⁴ : Algebra Rₚ Sₚ := localizationAlgebra P.primeCompl S
this✝³ : IsScalarTower R Rₚ Sₚ
h : P' ≤ S⁰
this✝² : IsDomain Sₚ
this✝¹ : IsDedekindDomain Sₚ
this✝ : IsPrincipalIdealRing Sₚ
this : IsIntegrallyClosed Rₚ
⊢ map (algebraMap R (Localization.AtPrime P)) (spanIntNorm R (I * J)) =
    map (algebraMap R (Localization.AtPrime P)) (spanIntNorm R I * spanIntNorm R J)
Tactic:
haveI := NoZeroSMulDivisors_of_isLocalization R S Rₚ Sₚ _ P.primeCompl_le_nonZeroDivisors
Proof state after:
case neg
R : Type u_1
inst✝¹⁵ : CommRing R
S : Type u_2
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
inst✝¹² : IsIntegrallyClosed R
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : NoZeroSMulDivisors R S
hRS : Module.Finite R S
inst✝⁸ : IsIntegrallyClosed S
inst✝⁷ : IsSeparable (FractionRing R) (FractionRing S)
inst✝⁶ : IsDomain R
inst✝⁵ : IsDomain S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDedekindDomain S
inst✝² : Module.Finite R S
inst✝¹ : Module.Free R S
I J : Ideal S
inst✝ : Nontrivial R
h✝ : Nontrivial S
P : Ideal R
hP : P.IsMaximal
hP0 : ¬P = ⊥
P' : Submonoid S := Algebra.algebraMapSubmonoid S P.primeCompl
Rₚ : Type u_1 := Localization.AtPrime P
Sₚ : Type u_2 := Localization P'
this✝⁵ : Algebra Rₚ Sₚ := localizationAlgebra P.primeCompl S
this✝⁴ : IsScalarTower R Rₚ Sₚ
h : P' ≤ S⁰
this✝³ : IsDomain Sₚ
this✝² : IsDedekindDomain Sₚ
this✝¹ : IsPrincipalIdealRing Sₚ
this✝ : IsIntegrallyClosed Rₚ
this : NoZeroSMulDivisors Rₚ Sₚ
⊢ map (algebraMap R (Localization.AtPrime P)) (spanIntNorm R (I * J)) =
    map (algebraMap R (Localization.AtPrime P)) (spanIntNorm R I * spanIntNorm R J)
Theorem: Ideal.spanIntNorm_mul
Proof state before:
case neg
R : Type u_1
inst✝¹⁵ : CommRing R
S : Type u_2
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
inst✝¹² : IsIntegrallyClosed R
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : NoZeroSMulDivisors R S
hRS : Module.Finite R S
inst✝⁸ : IsIntegrallyClosed S
inst✝⁷ : IsSeparable (FractionRing R) (FractionRing S)
inst✝⁶ : IsDomain R
inst✝⁵ : IsDomain S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDedekindDomain S
inst✝² : Module.Finite R S
inst✝¹ : Module.Free R S
I J : Ideal S
inst✝ : Nontrivial R
h✝ : Nontrivial S
P : Ideal R
hP : P.IsMaximal
hP0 : ¬P = ⊥
P' : Submonoid S := Algebra.algebraMapSubmonoid S P.primeCompl
Rₚ : Type u_1 := Localization.AtPrime P
Sₚ : Type u_2 := Localization P'
this✝⁵ : Algebra Rₚ Sₚ := localizationAlgebra P.primeCompl S
this✝⁴ : IsScalarTower R Rₚ Sₚ
h : P' ≤ S⁰
this✝³ : IsDomain Sₚ
this✝² : IsDedekindDomain Sₚ
this✝¹ : IsPrincipalIdealRing Sₚ
this✝ : IsIntegrallyClosed Rₚ
this : NoZeroSMulDivisors Rₚ Sₚ
⊢ map (algebraMap R (Localization.AtPrime P)) (spanIntNorm R (I * J)) =
    map (algebraMap R (Localization.AtPrime P)) (spanIntNorm R I * spanIntNorm R J)
Tactic:
haveI := Module.Finite_of_isLocalization R S Rₚ Sₚ P.primeCompl
Proof state after:
case neg
R : Type u_1
inst✝¹⁵ : CommRing R
S : Type u_2
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
inst✝¹² : IsIntegrallyClosed R
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : NoZeroSMulDivisors R S
hRS : Module.Finite R S
inst✝⁸ : IsIntegrallyClosed S
inst✝⁷ : IsSeparable (FractionRing R) (FractionRing S)
inst✝⁶ : IsDomain R
inst✝⁵ : IsDomain S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDedekindDomain S
inst✝² : Module.Finite R S
inst✝¹ : Module.Free R S
I J : Ideal S
inst✝ : Nontrivial R
h✝ : Nontrivial S
P : Ideal R
hP : P.IsMaximal
hP0 : ¬P = ⊥
P' : Submonoid S := Algebra.algebraMapSubmonoid S P.primeCompl
Rₚ : Type u_1 := Localization.AtPrime P
Sₚ : Type u_2 := Localization P'
this✝⁶ : Algebra Rₚ Sₚ := localizationAlgebra P.primeCompl S
this✝⁵ : IsScalarTower R Rₚ Sₚ
h : P' ≤ S⁰
this✝⁴ : IsDomain Sₚ
this✝³ : IsDedekindDomain Sₚ
this✝² : IsPrincipalIdealRing Sₚ
this✝¹ : IsIntegrallyClosed Rₚ
this✝ : NoZeroSMulDivisors Rₚ Sₚ
this : Module.Finite Rₚ Sₚ
⊢ map (algebraMap R (Localization.AtPrime P)) (spanIntNorm R (I * J)) =
    map (algebraMap R (Localization.AtPrime P)) (spanIntNorm R I * spanIntNorm R J)
Theorem: Ideal.spanIntNorm_mul
Proof state before:
case neg
R : Type u_1
inst✝¹⁵ : CommRing R
S : Type u_2
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
inst✝¹² : IsIntegrallyClosed R
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : NoZeroSMulDivisors R S
hRS : Module.Finite R S
inst✝⁸ : IsIntegrallyClosed S
inst✝⁷ : IsSeparable (FractionRing R) (FractionRing S)
inst✝⁶ : IsDomain R
inst✝⁵ : IsDomain S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDedekindDomain S
inst✝² : Module.Finite R S
inst✝¹ : Module.Free R S
I J : Ideal S
inst✝ : Nontrivial R
h✝ : Nontrivial S
P : Ideal R
hP : P.IsMaximal
hP0 : ¬P = ⊥
P' : Submonoid S := Algebra.algebraMapSubmonoid S P.primeCompl
Rₚ : Type u_1 := Localization.AtPrime P
Sₚ : Type u_2 := Localization P'
this✝⁶ : Algebra Rₚ Sₚ := localizationAlgebra P.primeCompl S
this✝⁵ : IsScalarTower R Rₚ Sₚ
h : P' ≤ S⁰
this✝⁴ : IsDomain Sₚ
this✝³ : IsDedekindDomain Sₚ
this✝² : IsPrincipalIdealRing Sₚ
this✝¹ : IsIntegrallyClosed Rₚ
this✝ : NoZeroSMulDivisors Rₚ Sₚ
this : Module.Finite Rₚ Sₚ
⊢ map (algebraMap R (Localization.AtPrime P)) (spanIntNorm R (I * J)) =
    map (algebraMap R (Localization.AtPrime P)) (spanIntNorm R I * spanIntNorm R J)
Tactic:
let L := FractionRing S
Proof state after:
case neg
R : Type u_1
inst✝¹⁵ : CommRing R
S : Type u_2
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
inst✝¹² : IsIntegrallyClosed R
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : NoZeroSMulDivisors R S
hRS : Module.Finite R S
inst✝⁸ : IsIntegrallyClosed S
inst✝⁷ : IsSeparable (FractionRing R) (FractionRing S)
inst✝⁶ : IsDomain R
inst✝⁵ : IsDomain S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDedekindDomain S
inst✝² : Module.Finite R S
inst✝¹ : Module.Free R S
I J : Ideal S
inst✝ : Nontrivial R
h✝ : Nontrivial S
P : Ideal R
hP : P.IsMaximal
hP0 : ¬P = ⊥
P' : Submonoid S := Algebra.algebraMapSubmonoid S P.primeCompl
Rₚ : Type u_1 := Localization.AtPrime P
Sₚ : Type u_2 := Localization P'
this✝⁶ : Algebra Rₚ Sₚ := localizationAlgebra P.primeCompl S
this✝⁵ : IsScalarTower R Rₚ Sₚ
h : P' ≤ S⁰
this✝⁴ : IsDomain Sₚ
this✝³ : IsDedekindDomain Sₚ
this✝² : IsPrincipalIdealRing Sₚ
this✝¹ : IsIntegrallyClosed Rₚ
this✝ : NoZeroSMulDivisors Rₚ Sₚ
this : Module.Finite Rₚ Sₚ
L : Type u_2 := FractionRing S
⊢ map (algebraMap R (Localization.AtPrime P)) (spanIntNorm R (I * J)) =
    map (algebraMap R (Localization.AtPrime P)) (spanIntNorm R I * spanIntNorm R J)