Theorem: Ideal.NoZeroSMulDivisors_of_isLocalization (FltRegular/NumberTheory/IdealNorm.lean)

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✝
R : Type u_3
S : Type u_4
Rₚ : Type u_5
Sₚ : Type u_6
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : CommRing Rₚ
inst✝¹¹ : CommRing Sₚ
inst✝¹⁰ : Algebra R S
inst✝⁹ : Algebra R Rₚ
inst✝⁸ : Algebra R Sₚ
inst✝⁷ : Algebra S Sₚ
inst✝⁶ : Algebra Rₚ Sₚ
inst✝⁵ : IsScalarTower R S Sₚ
inst✝⁴ : IsScalarTower R Rₚ Sₚ
M : Submonoid R
hM : M ≤ R⁰
inst✝³ : IsLocalization M Rₚ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsDomain S
⊢ NoZeroSMulDivisors Rₚ Sₚ
Tactic:
have e : Algebra.algebraMapSubmonoid S M ≤ S⁰ :=
  Submonoid.map_le_of_le_comap _ <| hM.trans
    (nonZeroDivisors_le_comap_nonZeroDivisors_of_injective _
      (NoZeroSMulDivisors.algebraMap_injective _ _))
State after:
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✝
R : Type u_3
S : Type u_4
Rₚ : Type u_5
Sₚ : Type u_6
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : CommRing Rₚ
inst✝¹¹ : CommRing Sₚ
inst✝¹⁰ : Algebra R S
inst✝⁹ : Algebra R Rₚ
inst✝⁸ : Algebra R Sₚ
inst✝⁷ : Algebra S Sₚ
inst✝⁶ : Algebra Rₚ Sₚ
inst✝⁵ : IsScalarTower R S Sₚ
inst✝⁴ : IsScalarTower R Rₚ Sₚ
M : Submonoid R
hM : M ≤ R⁰
inst✝³ : IsLocalization M Rₚ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsDomain S
e : Algebra.algebraMapSubmonoid S M ≤ S⁰
⊢ NoZeroSMulDivisors Rₚ Sₚ

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✝
R : Type u_3
S : Type u_4
Rₚ : Type u_5
Sₚ : Type u_6
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : CommRing Rₚ
inst✝¹¹ : CommRing Sₚ
inst✝¹⁰ : Algebra R S
inst✝⁹ : Algebra R Rₚ
inst✝⁸ : Algebra R Sₚ
inst✝⁷ : Algebra S Sₚ
inst✝⁶ : Algebra Rₚ Sₚ
inst✝⁵ : IsScalarTower R S Sₚ
inst✝⁴ : IsScalarTower R Rₚ Sₚ
M : Submonoid R
hM : M ≤ R⁰
inst✝³ : IsLocalization M Rₚ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsDomain S
e : Algebra.algebraMapSubmonoid S M ≤ S⁰
⊢ NoZeroSMulDivisors Rₚ Sₚ
Tactic:
haveI : IsDomain Sₚ := IsLocalization.isDomain_of_le_nonZeroDivisors S e
State after:
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✝
R : Type u_3
S : Type u_4
Rₚ : Type u_5
Sₚ : Type u_6
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : CommRing Rₚ
inst✝¹¹ : CommRing Sₚ
inst✝¹⁰ : Algebra R S
inst✝⁹ : Algebra R Rₚ
inst✝⁸ : Algebra R Sₚ
inst✝⁷ : Algebra S Sₚ
inst✝⁶ : Algebra Rₚ Sₚ
inst✝⁵ : IsScalarTower R S Sₚ
inst✝⁴ : IsScalarTower R Rₚ Sₚ
M : Submonoid R
hM : M ≤ R⁰
inst✝³ : IsLocalization M Rₚ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsDomain S
e : Algebra.algebraMapSubmonoid S M ≤ S⁰
this : IsDomain Sₚ
⊢ NoZeroSMulDivisors Rₚ Sₚ

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✝
R : Type u_3
S : Type u_4
Rₚ : Type u_5
Sₚ : Type u_6
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : CommRing Rₚ
inst✝¹¹ : CommRing Sₚ
inst✝¹⁰ : Algebra R S
inst✝⁹ : Algebra R Rₚ
inst✝⁸ : Algebra R Sₚ
inst✝⁷ : Algebra S Sₚ
inst✝⁶ : Algebra Rₚ Sₚ
inst✝⁵ : IsScalarTower R S Sₚ
inst✝⁴ : IsScalarTower R Rₚ Sₚ
M : Submonoid R
hM : M ≤ R⁰
inst✝³ : IsLocalization M Rₚ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsDomain S
e : Algebra.algebraMapSubmonoid S M ≤ S⁰
this : IsDomain Sₚ
⊢ NoZeroSMulDivisors Rₚ Sₚ
Tactic:
have : algebraMap Rₚ Sₚ = IsLocalization.map (T := Algebra.algebraMapSubmonoid S M) Sₚ
  (algebraMap R S) (Submonoid.le_comap_map M) := by
  apply IsLocalization.ringHom_ext M
  simp only [IsLocalization.map_comp, ← IsScalarTower.algebraMap_eq]
State after:
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✝
R : Type u_3
S : Type u_4
Rₚ : Type u_5
Sₚ : Type u_6
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : CommRing Rₚ
inst✝¹¹ : CommRing Sₚ
inst✝¹⁰ : Algebra R S
inst✝⁹ : Algebra R Rₚ
inst✝⁸ : Algebra R Sₚ
inst✝⁷ : Algebra S Sₚ
inst✝⁶ : Algebra Rₚ Sₚ
inst✝⁵ : IsScalarTower R S Sₚ
inst✝⁴ : IsScalarTower R Rₚ Sₚ
M : Submonoid R
hM : M ≤ R⁰
inst✝³ : IsLocalization M Rₚ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsDomain S
e : Algebra.algebraMapSubmonoid S M ≤ S⁰
this✝ : IsDomain Sₚ
this : algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
⊢ NoZeroSMulDivisors Rₚ Sₚ

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✝
R : Type u_3
S : Type u_4
Rₚ : Type u_5
Sₚ : Type u_6
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : CommRing Rₚ
inst✝¹¹ : CommRing Sₚ
inst✝¹⁰ : Algebra R S
inst✝⁹ : Algebra R Rₚ
inst✝⁸ : Algebra R Sₚ
inst✝⁷ : Algebra S Sₚ
inst✝⁶ : Algebra Rₚ Sₚ
inst✝⁵ : IsScalarTower R S Sₚ
inst✝⁴ : IsScalarTower R Rₚ Sₚ
M : Submonoid R
hM : M ≤ R⁰
inst✝³ : IsLocalization M Rₚ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsDomain S
e : Algebra.algebraMapSubmonoid S M ≤ S⁰
this✝ : IsDomain Sₚ
this : algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
⊢ NoZeroSMulDivisors Rₚ Sₚ
Tactic:
rw [NoZeroSMulDivisors.iff_algebraMap_injective, RingHom.injective_iff_ker_eq_bot,
  RingHom.ker_eq_bot_iff_eq_zero]
State after:
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✝
R : Type u_3
S : Type u_4
Rₚ : Type u_5
Sₚ : Type u_6
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : CommRing Rₚ
inst✝¹¹ : CommRing Sₚ
inst✝¹⁰ : Algebra R S
inst✝⁹ : Algebra R Rₚ
inst✝⁸ : Algebra R Sₚ
inst✝⁷ : Algebra S Sₚ
inst✝⁶ : Algebra Rₚ Sₚ
inst✝⁵ : IsScalarTower R S Sₚ
inst✝⁴ : IsScalarTower R Rₚ Sₚ
M : Submonoid R
hM : M ≤ R⁰
inst✝³ : IsLocalization M Rₚ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsDomain S
e : Algebra.algebraMapSubmonoid S M ≤ S⁰
this✝ : IsDomain Sₚ
this : algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
⊢ ∀ (x : Rₚ), (algebraMap Rₚ Sₚ) x = 0 → x = 0

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✝
R : Type u_3
S : Type u_4
Rₚ : Type u_5
Sₚ : Type u_6
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : CommRing Rₚ
inst✝¹¹ : CommRing Sₚ
inst✝¹⁰ : Algebra R S
inst✝⁹ : Algebra R Rₚ
inst✝⁸ : Algebra R Sₚ
inst✝⁷ : Algebra S Sₚ
inst✝⁶ : Algebra Rₚ Sₚ
inst✝⁵ : IsScalarTower R S Sₚ
inst✝⁴ : IsScalarTower R Rₚ Sₚ
M : Submonoid R
hM : M ≤ R⁰
inst✝³ : IsLocalization M Rₚ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsDomain S
e : Algebra.algebraMapSubmonoid S M ≤ S⁰
this✝ : IsDomain Sₚ
this : algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
⊢ ∀ (x : Rₚ), (algebraMap Rₚ Sₚ) x = 0 → x = 0
Tactic:
intro x hx
State after:
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✝
R : Type u_3
S : Type u_4
Rₚ : Type u_5
Sₚ : Type u_6
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : CommRing Rₚ
inst✝¹¹ : CommRing Sₚ
inst✝¹⁰ : Algebra R S
inst✝⁹ : Algebra R Rₚ
inst✝⁸ : Algebra R Sₚ
inst✝⁷ : Algebra S Sₚ
inst✝⁶ : Algebra Rₚ Sₚ
inst✝⁵ : IsScalarTower R S Sₚ
inst✝⁴ : IsScalarTower R Rₚ Sₚ
M : Submonoid R
hM : M ≤ R⁰
inst✝³ : IsLocalization M Rₚ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsDomain S
e : Algebra.algebraMapSubmonoid S M ≤ S⁰
this✝ : IsDomain Sₚ
this : algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
x : Rₚ
hx : (algebraMap Rₚ Sₚ) x = 0
⊢ x = 0

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✝
R : Type u_3
S : Type u_4
Rₚ : Type u_5
Sₚ : Type u_6
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : CommRing Rₚ
inst✝¹¹ : CommRing Sₚ
inst✝¹⁰ : Algebra R S
inst✝⁹ : Algebra R Rₚ
inst✝⁸ : Algebra R Sₚ
inst✝⁷ : Algebra S Sₚ
inst✝⁶ : Algebra Rₚ Sₚ
inst✝⁵ : IsScalarTower R S Sₚ
inst✝⁴ : IsScalarTower R Rₚ Sₚ
M : Submonoid R
hM : M ≤ R⁰
inst✝³ : IsLocalization M Rₚ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsDomain S
e : Algebra.algebraMapSubmonoid S M ≤ S⁰
this✝ : IsDomain Sₚ
this : algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
x : Rₚ
hx : (algebraMap Rₚ Sₚ) x = 0
⊢ x = 0
Tactic:
obtain ⟨x, s, rfl⟩ := IsLocalization.mk'_surjective M x
State after:
case intro.intro
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✝
R : Type u_3
S : Type u_4
Rₚ : Type u_5
Sₚ : Type u_6
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : CommRing Rₚ
inst✝¹¹ : CommRing Sₚ
inst✝¹⁰ : Algebra R S
inst✝⁹ : Algebra R Rₚ
inst✝⁸ : Algebra R Sₚ
inst✝⁷ : Algebra S Sₚ
inst✝⁶ : Algebra Rₚ Sₚ
inst✝⁵ : IsScalarTower R S Sₚ
inst✝⁴ : IsScalarTower R Rₚ Sₚ
M : Submonoid R
hM : M ≤ R⁰
inst✝³ : IsLocalization M Rₚ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsDomain S
e : Algebra.algebraMapSubmonoid S M ≤ S⁰
this✝ : IsDomain Sₚ
this : algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
x : R
s : ↥M
hx : (algebraMap Rₚ Sₚ) (IsLocalization.mk' Rₚ x s) = 0
⊢ IsLocalization.mk' Rₚ x s = 0

State before:
case intro.intro
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✝
R : Type u_3
S : Type u_4
Rₚ : Type u_5
Sₚ : Type u_6
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : CommRing Rₚ
inst✝¹¹ : CommRing Sₚ
inst✝¹⁰ : Algebra R S
inst✝⁹ : Algebra R Rₚ
inst✝⁸ : Algebra R Sₚ
inst✝⁷ : Algebra S Sₚ
inst✝⁶ : Algebra Rₚ Sₚ
inst✝⁵ : IsScalarTower R S Sₚ
inst✝⁴ : IsScalarTower R Rₚ Sₚ
M : Submonoid R
hM : M ≤ R⁰
inst✝³ : IsLocalization M Rₚ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsDomain S
e : Algebra.algebraMapSubmonoid S M ≤ S⁰
this✝ : IsDomain Sₚ
this : algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
x : R
s : ↥M
hx : (algebraMap Rₚ Sₚ) (IsLocalization.mk' Rₚ x s) = 0
⊢ IsLocalization.mk' Rₚ x s = 0
Tactic:
simp only [RingHom.algebraMap_toAlgebra, IsLocalization.map_mk', IsLocalization.mk'_eq_zero_iff,
  Subtype.exists, exists_prop, this] at hx ⊢
State after:
case intro.intro
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✝
R : Type u_3
S : Type u_4
Rₚ : Type u_5
Sₚ : Type u_6
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : CommRing Rₚ
inst✝¹¹ : CommRing Sₚ
inst✝¹⁰ : Algebra R S
inst✝⁹ : Algebra R Rₚ
inst✝⁸ : Algebra R Sₚ
inst✝⁷ : Algebra S Sₚ
inst✝⁶ : Algebra Rₚ Sₚ
inst✝⁵ : IsScalarTower R S Sₚ
inst✝⁴ : IsScalarTower R Rₚ Sₚ
M : Submonoid R
hM : M ≤ R⁰
inst✝³ : IsLocalization M Rₚ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsDomain S
e : Algebra.algebraMapSubmonoid S M ≤ S⁰
this✝ : IsDomain Sₚ
this : algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
x : R
s : ↥M
hx : ∃ a ∈ Algebra.algebraMapSubmonoid S M, a * (algebraMap R S) x = 0
⊢ ∃ a ∈ M, a * x = 0

State before:
case intro.intro
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✝
R : Type u_3
S : Type u_4
Rₚ : Type u_5
Sₚ : Type u_6
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : CommRing Rₚ
inst✝¹¹ : CommRing Sₚ
inst✝¹⁰ : Algebra R S
inst✝⁹ : Algebra R Rₚ
inst✝⁸ : Algebra R Sₚ
inst✝⁷ : Algebra S Sₚ
inst✝⁶ : Algebra Rₚ Sₚ
inst✝⁵ : IsScalarTower R S Sₚ
inst✝⁴ : IsScalarTower R Rₚ Sₚ
M : Submonoid R
hM : M ≤ R⁰
inst✝³ : IsLocalization M Rₚ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsDomain S
e : Algebra.algebraMapSubmonoid S M ≤ S⁰
this✝ : IsDomain Sₚ
this : algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
x : R
s : ↥M
hx : ∃ a ∈ Algebra.algebraMapSubmonoid S M, a * (algebraMap R S) x = 0
⊢ ∃ a ∈ M, a * x = 0
Tactic:
obtain ⟨_, ⟨a, ha, rfl⟩, H⟩ := hx
State after:
case intro.intro.intro.intro.intro.intro
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✝
R : Type u_3
S : Type u_4
Rₚ : Type u_5
Sₚ : Type u_6
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : CommRing Rₚ
inst✝¹¹ : CommRing Sₚ
inst✝¹⁰ : Algebra R S
inst✝⁹ : Algebra R Rₚ
inst✝⁸ : Algebra R Sₚ
inst✝⁷ : Algebra S Sₚ
inst✝⁶ : Algebra Rₚ Sₚ
inst✝⁵ : IsScalarTower R S Sₚ
inst✝⁴ : IsScalarTower R Rₚ Sₚ
M : Submonoid R
hM : M ≤ R⁰
inst✝³ : IsLocalization M Rₚ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsDomain S
e : Algebra.algebraMapSubmonoid S M ≤ S⁰
this✝ : IsDomain Sₚ
this : algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
x : R
s : ↥M
a : R
ha : a ∈ ↑M
H : (algebraMap R S) a * (algebraMap R S) x = 0
⊢ ∃ a ∈ M, a * x = 0

State before:
case intro.intro.intro.intro.intro.intro
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✝
R : Type u_3
S : Type u_4
Rₚ : Type u_5
Sₚ : Type u_6
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : CommRing Rₚ
inst✝¹¹ : CommRing Sₚ
inst✝¹⁰ : Algebra R S
inst✝⁹ : Algebra R Rₚ
inst✝⁸ : Algebra R Sₚ
inst✝⁷ : Algebra S Sₚ
inst✝⁶ : Algebra Rₚ Sₚ
inst✝⁵ : IsScalarTower R S Sₚ
inst✝⁴ : IsScalarTower R Rₚ Sₚ
M : Submonoid R
hM : M ≤ R⁰
inst✝³ : IsLocalization M Rₚ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsDomain S
e : Algebra.algebraMapSubmonoid S M ≤ S⁰
this✝ : IsDomain Sₚ
this : algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
x : R
s : ↥M
a : R
ha : a ∈ ↑M
H : (algebraMap R S) a * (algebraMap R S) x = 0
⊢ ∃ a ∈ M, a * x = 0
Tactic:
simp only [← _root_.map_mul,
  (injective_iff_map_eq_zero' _).mp (NoZeroSMulDivisors.algebraMap_injective R S)] at H
State after:
case intro.intro.intro.intro.intro.intro
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✝
R : Type u_3
S : Type u_4
Rₚ : Type u_5
Sₚ : Type u_6
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : CommRing Rₚ
inst✝¹¹ : CommRing Sₚ
inst✝¹⁰ : Algebra R S
inst✝⁹ : Algebra R Rₚ
inst✝⁸ : Algebra R Sₚ
inst✝⁷ : Algebra S Sₚ
inst✝⁶ : Algebra Rₚ Sₚ
inst✝⁵ : IsScalarTower R S Sₚ
inst✝⁴ : IsScalarTower R Rₚ Sₚ
M : Submonoid R
hM : M ≤ R⁰
inst✝³ : IsLocalization M Rₚ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsDomain S
e : Algebra.algebraMapSubmonoid S M ≤ S⁰
this✝ : IsDomain Sₚ
this : algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
x : R
s : ↥M
a : R
ha : a ∈ ↑M
H : a * x = 0
⊢ ∃ a ∈ M, a * x = 0

State before:
case intro.intro.intro.intro.intro.intro
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✝
R : Type u_3
S : Type u_4
Rₚ : Type u_5
Sₚ : Type u_6
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : CommRing Rₚ
inst✝¹¹ : CommRing Sₚ
inst✝¹⁰ : Algebra R S
inst✝⁹ : Algebra R Rₚ
inst✝⁸ : Algebra R Sₚ
inst✝⁷ : Algebra S Sₚ
inst✝⁶ : Algebra Rₚ Sₚ
inst✝⁵ : IsScalarTower R S Sₚ
inst✝⁴ : IsScalarTower R Rₚ Sₚ
M : Submonoid R
hM : M ≤ R⁰
inst✝³ : IsLocalization M Rₚ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsDomain S
e : Algebra.algebraMapSubmonoid S M ≤ S⁰
this✝ : IsDomain Sₚ
this : algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
x : R
s : ↥M
a : R
ha : a ∈ ↑M
H : a * x = 0
⊢ ∃ a ∈ M, a * x = 0
Tactic:
refine ⟨a, ha, H⟩
State after:
no goals

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✝
R : Type u_3
S : Type u_4
Rₚ : Type u_5
Sₚ : Type u_6
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : CommRing Rₚ
inst✝¹¹ : CommRing Sₚ
inst✝¹⁰ : Algebra R S
inst✝⁹ : Algebra R Rₚ
inst✝⁸ : Algebra R Sₚ
inst✝⁷ : Algebra S Sₚ
inst✝⁶ : Algebra Rₚ Sₚ
inst✝⁵ : IsScalarTower R S Sₚ
inst✝⁴ : IsScalarTower R Rₚ Sₚ
M : Submonoid R
hM : M ≤ R⁰
inst✝³ : IsLocalization M Rₚ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsDomain S
e : Algebra.algebraMapSubmonoid S M ≤ S⁰
this : IsDomain Sₚ
⊢ algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
Tactic:
apply IsLocalization.ringHom_ext M
State after:
case h
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✝
R : Type u_3
S : Type u_4
Rₚ : Type u_5
Sₚ : Type u_6
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : CommRing Rₚ
inst✝¹¹ : CommRing Sₚ
inst✝¹⁰ : Algebra R S
inst✝⁹ : Algebra R Rₚ
inst✝⁸ : Algebra R Sₚ
inst✝⁷ : Algebra S Sₚ
inst✝⁶ : Algebra Rₚ Sₚ
inst✝⁵ : IsScalarTower R S Sₚ
inst✝⁴ : IsScalarTower R Rₚ Sₚ
M : Submonoid R
hM : M ≤ R⁰
inst✝³ : IsLocalization M Rₚ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsDomain S
e : Algebra.algebraMapSubmonoid S M ≤ S⁰
this : IsDomain Sₚ
⊢ (algebraMap Rₚ Sₚ).comp (algebraMap R Rₚ) = (IsLocalization.map Sₚ (algebraMap R S) ⋯).comp (algebraMap R Rₚ)

State before:
case h
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✝
R : Type u_3
S : Type u_4
Rₚ : Type u_5
Sₚ : Type u_6
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : CommRing Rₚ
inst✝¹¹ : CommRing Sₚ
inst✝¹⁰ : Algebra R S
inst✝⁹ : Algebra R Rₚ
inst✝⁸ : Algebra R Sₚ
inst✝⁷ : Algebra S Sₚ
inst✝⁶ : Algebra Rₚ Sₚ
inst✝⁵ : IsScalarTower R S Sₚ
inst✝⁴ : IsScalarTower R Rₚ Sₚ
M : Submonoid R
hM : M ≤ R⁰
inst✝³ : IsLocalization M Rₚ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsDomain S
e : Algebra.algebraMapSubmonoid S M ≤ S⁰
this : IsDomain Sₚ
⊢ (algebraMap Rₚ Sₚ).comp (algebraMap R Rₚ) = (IsLocalization.map Sₚ (algebraMap R S) ⋯).comp (algebraMap R Rₚ)
Tactic:
simp only [IsLocalization.map_comp, ← IsScalarTower.algebraMap_eq]
State after:
no goals