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
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)
Tactic:
let g : Sₚ →+* L := IsLocalization.map _ (M := P') (T := S⁰) (RingHom.id 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ₚ
this✝² : IsPrincipalIdealRing Sₚ
this✝¹ : IsIntegrallyClosed Rₚ
this✝ : NoZeroSMulDivisors Rₚ Sₚ
this : Module.Finite Rₚ Sₚ
L : Type u_2 := FractionRing S
g : Sₚ →+* L := IsLocalization.map L (RingHom.id S) h
⊢ 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ₚ
L : Type u_2 := FractionRing S
g : Sₚ →+* L := IsLocalization.map L (RingHom.id S) h
⊢ map (algebraMap R (Localization.AtPrime P)) (spanIntNorm R (I * J)) =
    map (algebraMap R (Localization.AtPrime P)) (spanIntNorm R I * spanIntNorm R J)
Tactic:
letI := g.toAlgebra
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
g : Sₚ →+* L := IsLocalization.map L (RingHom.id S) h
this : Algebra Sₚ L := g.toAlgebra
⊢ 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ₚ
L : Type u_2 := FractionRing S
g : Sₚ →+* L := IsLocalization.map L (RingHom.id S) h
this : Algebra Sₚ L := g.toAlgebra
⊢ 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 S Sₚ (FractionRing S) := IsScalarTower.of_algebraMap_eq'
  (by rw [RingHom.algebraMap_toAlgebra, IsLocalization.map_comp, RingHom.comp_id])
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
g : Sₚ →+* L := IsLocalization.map L (RingHom.id S) h
this✝ : Algebra Sₚ L := g.toAlgebra
this : IsScalarTower S Sₚ (FractionRing 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ₚ
L : Type u_2 := FractionRing S
g : Sₚ →+* L := IsLocalization.map L (RingHom.id S) h
this✝ : Algebra Sₚ L := g.toAlgebra
this : IsScalarTower S Sₚ (FractionRing S)
⊢ map (algebraMap R (Localization.AtPrime P)) (spanIntNorm R (I * J)) =
    map (algebraMap R (Localization.AtPrime P)) (spanIntNorm R I * spanIntNorm R J)
Tactic:
letI := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization
  P' Sₚ (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
g : Sₚ →+* L := IsLocalization.map L (RingHom.id S) h
this✝¹ : Algebra Sₚ L := g.toAlgebra
this✝ : IsScalarTower S Sₚ (FractionRing S)
this : IsFractionRing Sₚ (FractionRing S) :=
  IsFractionRing.isFractionRing_of_isDomain_of_isLocalization P' Sₚ (FractionRing 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ₚ
L : Type u_2 := FractionRing S
g : Sₚ →+* L := IsLocalization.map L (RingHom.id S) h
this✝² : Algebra Sₚ L := g.toAlgebra
this✝¹ : IsScalarTower S Sₚ (FractionRing S)
this✝ : IsFractionRing Sₚ (FractionRing S) :=
  IsFractionRing.isFractionRing_of_isDomain_of_isLocalization P' Sₚ (FractionRing S)
this : IsSeparable (FractionRing Rₚ) (FractionRing Sₚ)
⊢ spanIntNorm (Localization.AtPrime P)
      (map (algebraMap S (Localization P')) I * map (algebraMap S (Localization P')) J) =
    spanIntNorm (Localization.AtPrime P) (map (algebraMap S (Localization P')) I) *
      spanIntNorm (Localization.AtPrime P) (map (algebraMap S (Localization P')) J)
Tactic:
rw [← (I.map _).span_singleton_generator, ← (J.map _).span_singleton_generator,
  span_singleton_mul_span_singleton, spanIntNorm_singleton, spanIntNorm_singleton,
    spanIntNorm_singleton, span_singleton_mul_span_singleton, _root_.map_mul]
Proof state after:
no goals
Theorem: Ideal.spanIntNorm_mul
Proof state before:
case inl
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✝ : Subsingleton S
⊢ spanIntNorm R (I * J) = spanIntNorm R I * spanIntNorm R J
Tactic:
have : ∀ I : Ideal S, I = ⊤ := fun I => Subsingleton.elim I ⊤
Proof state after:
case inl
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✝ : Subsingleton S
this : ∀ (I : Ideal S), I = ⊤
⊢ spanIntNorm R (I * J) = spanIntNorm R I * spanIntNorm R J
Theorem: Ideal.spanIntNorm_mul
Proof state before:
case inl
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✝ : Subsingleton S
this : ∀ (I : Ideal S), I = ⊤
⊢ spanIntNorm R (I * J) = spanIntNorm R I * spanIntNorm R J
Tactic:
simp [this I, this J, this (I * J)]
Proof state after:
no goals
Theorem: Ideal.spanIntNorm_mul
Proof state before:
case pos
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 = ⊥
⊢ map (algebraMap R (Localization.AtPrime P)) (spanIntNorm R (I * J)) =
    map (algebraMap R (Localization.AtPrime P)) (spanIntNorm R I * spanIntNorm R J)
Tactic:
subst hP0
Proof state after:
case pos
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
hP : ⊥.IsMaximal
⊢ map (algebraMap R (Localization.AtPrime ⊥)) (spanIntNorm R (I * J)) =
    map (algebraMap R (Localization.AtPrime ⊥)) (spanIntNorm R I * spanIntNorm R J)
Theorem: Ideal.spanIntNorm_mul
Proof state before:
case pos
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
hP : ⊥.IsMaximal
⊢ map (algebraMap R (Localization.AtPrime ⊥)) (spanIntNorm R (I * J)) =
    map (algebraMap R (Localization.AtPrime ⊥)) (spanIntNorm R I * spanIntNorm R J)
Tactic:
rw [spanIntNorm_mul_of_bot_or_top]
Proof state after:
case pos.eq_bot_or_top
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
hP : ⊥.IsMaximal
⊢ ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
Theorem: Ideal.spanIntNorm_mul
Proof state before:
case pos.eq_bot_or_top
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
hP : ⊥.IsMaximal
⊢ ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
Tactic:
intro I
Proof state after:
case pos.eq_bot_or_top
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
hP : ⊥.IsMaximal
I : Ideal R
⊢ I = ⊥ ∨ I = ⊤
Theorem: Ideal.spanIntNorm_mul
Proof state before:
case pos.eq_bot_or_top
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
hP : ⊥.IsMaximal
I : Ideal R
⊢ I = ⊥ ∨ I = ⊤
Tactic:
refine or_iff_not_imp_right.mpr fun hI => ?_
Proof state after:
case pos.eq_bot_or_top
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
hP : ⊥.IsMaximal
I : Ideal R
hI : ¬I = ⊤
⊢ I = ⊥
Theorem: Ideal.spanIntNorm_mul
Proof state before:
case pos.eq_bot_or_top
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
hP : ⊥.IsMaximal
I : Ideal R
hI : ¬I = ⊤
⊢ I = ⊥
Tactic:
exact (hP.eq_of_le hI bot_le).symm
Proof state after:
no goals
Theorem: Ideal.spanIntNorm_mul
Proof state before:
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
g : Sₚ →+* L := IsLocalization.map L (RingHom.id S) h
this : Algebra Sₚ L := g.toAlgebra
⊢ algebraMap S (FractionRing S) = (algebraMap Sₚ (FractionRing S)).comp (algebraMap S Sₚ)
Tactic:
rw [RingHom.algebraMap_toAlgebra, IsLocalization.map_comp, RingHom.comp_id]
Proof state after:
no goals