Theorem: Ideal.spanIntNorm_localization
Proof state before:
case refine_1
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)
I : Ideal S
M : Submonoid R
hM : M ≤ R⁰
Rₘ : Type u_3
Sₘ : Type u_4
inst✝¹⁶ : CommRing Rₘ
inst✝¹⁵ : Algebra R Rₘ
inst✝¹⁴ : CommRing Sₘ
inst✝¹³ : Algebra S Sₘ
inst✝¹² : Algebra Rₘ Sₘ
inst✝¹¹ : Algebra R Sₘ
inst✝¹⁰ : IsScalarTower R Rₘ Sₘ
inst✝⁹ : IsScalarTower R S Sₘ
inst✝⁸ : IsLocalization M Rₘ
inst✝⁷ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝⁶ : IsIntegrallyClosed Rₘ
inst✝⁵ : IsDomain Rₘ
inst✝⁴ : IsDomain Sₘ
inst✝³ : NoZeroSMulDivisors Rₘ Sₘ
inst✝² : Module.Finite Rₘ Sₘ
inst✝¹ : IsIntegrallyClosed Sₘ
inst✝ : IsSeparable (FractionRing Rₘ) (FractionRing Sₘ)
K : Type u_1 := FractionRing R
f : Rₘ →+* K := IsLocalization.map K (RingHom.id R) hM
this✝⁸ : Algebra Rₘ K := f.toAlgebra
this✝⁷ : IsScalarTower R Rₘ K
this✝⁶ : IsFractionRing Rₘ K := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M Rₘ K
L : Type u_2 := FractionRing S
g : Sₘ →+* L := IsLocalization.map L (RingHom.id S) ⋯
this✝⁵ : Algebra Sₘ L := g.toAlgebra
this✝⁴ : IsScalarTower S Sₘ L
this✝³ : Algebra Rₘ L := ((algebraMap K L).comp f).toAlgebra
this✝² : IsScalarTower Rₘ K L
this✝¹ : IsScalarTower Rₘ Sₘ L
this✝ : IsFractionRing Sₘ L :=
  IsFractionRing.isFractionRing_of_isDomain_of_isLocalization (Algebra.algebraMapSubmonoid S M) Sₘ L
this : IsIntegralClosure Sₘ Rₘ L
a' : Sₘ
ha' : a' ∈ ↑(map (algebraMap S Sₘ) I)
⊢ a' ∈ ⇑(Algebra.intNorm Rₘ Sₘ) ⁻¹' ↑(Submodule.span Rₘ (⇑(algebraMap R Rₘ) ∘ ⇑(Algebra.intNorm R S) '' ↑I))
Tactic:
simp only [Set.mem_preimage, submodule_span_eq, ← map_spanIntNorm, SetLike.mem_coe,
  IsLocalization.mem_map_algebraMap_iff (Algebra.algebraMapSubmonoid S M) Sₘ,
  IsLocalization.mem_map_algebraMap_iff M Rₘ, Prod.exists] at ha' ⊢
Proof state after:
case refine_1
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)
I : Ideal S
M : Submonoid R
hM : M ≤ R⁰
Rₘ : Type u_3
Sₘ : Type u_4
inst✝¹⁶ : CommRing Rₘ
inst✝¹⁵ : Algebra R Rₘ
inst✝¹⁴ : CommRing Sₘ
inst✝¹³ : Algebra S Sₘ
inst✝¹² : Algebra Rₘ Sₘ
inst✝¹¹ : Algebra R Sₘ
inst✝¹⁰ : IsScalarTower R Rₘ Sₘ
inst✝⁹ : IsScalarTower R S Sₘ
inst✝⁸ : IsLocalization M Rₘ
inst✝⁷ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝⁶ : IsIntegrallyClosed Rₘ
inst✝⁵ : IsDomain Rₘ
inst✝⁴ : IsDomain Sₘ
inst✝³ : NoZeroSMulDivisors Rₘ Sₘ
inst✝² : Module.Finite Rₘ Sₘ
inst✝¹ : IsIntegrallyClosed Sₘ
inst✝ : IsSeparable (FractionRing Rₘ) (FractionRing Sₘ)
K : Type u_1 := FractionRing R
f : Rₘ →+* K := IsLocalization.map K (RingHom.id R) hM
this✝⁸ : Algebra Rₘ K := f.toAlgebra
this✝⁷ : IsScalarTower R Rₘ K
this✝⁶ : IsFractionRing Rₘ K := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M Rₘ K
L : Type u_2 := FractionRing S
g : Sₘ →+* L := IsLocalization.map L (RingHom.id S) ⋯
this✝⁵ : Algebra Sₘ L := g.toAlgebra
this✝⁴ : IsScalarTower S Sₘ L
this✝³ : Algebra Rₘ L := ((algebraMap K L).comp f).toAlgebra
this✝² : IsScalarTower Rₘ K L
this✝¹ : IsScalarTower Rₘ Sₘ L
this✝ : IsFractionRing Sₘ L :=
  IsFractionRing.isFractionRing_of_isDomain_of_isLocalization (Algebra.algebraMapSubmonoid S M) Sₘ L
this : IsIntegralClosure Sₘ Rₘ L
a' : Sₘ
ha' : ∃ a b, a' * (algebraMap S Sₘ) ↑b = (algebraMap S Sₘ) ↑a
⊢ ∃ a b, (Algebra.intNorm Rₘ Sₘ) a' * (algebraMap R Rₘ) ↑b = (algebraMap R Rₘ) ↑a