awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.LocalProperties.Semilocal
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Finite.{u_1 + 1} (MaximalSpectrum R)
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_2
inst_2 : (P : Ideal R) → [inst : P.IsMaximal] → CommRing (Rₚ P)
inst_3 : (P : Ideal R) → [inst_6 : P.IsMaximal] → Algebra.{u_1, u_2} R (Rₚ P)
inst_4 : ∀ (P : Ideal R) [inst_6 : P.IsMaximal], IsLocalization.AtPrime.{u_1, u_2} (Rₚ P) P
inst_5 : IsDomain R
hpid : ∀ (P : Ideal R) [inst : P.IsMaximal], IsPrincipalIdealRing.{u_2} (Rₚ P)
⊢ IsNoetherianRing R

Tactic:
have : IsNoetherianRing R :=
    IsNoetherianRing.of_isLocalization_maximal Rₚ fun P _ => inferInstance
-- Module: Mathlib.RingTheory.LocalProperties.Semilocal
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Finite.{u_1 + 1} (MaximalSpectrum R)
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_2
inst_2 : (P : Ideal R) → [inst : P.IsMaximal] → CommRing (Rₚ P)
inst_3 : (P : Ideal R) → [inst_6 : P.IsMaximal] → Algebra.{u_1, u_2} R (Rₚ P)
inst_4 : ∀ (P : Ideal R) [inst_6 : P.IsMaximal], IsLocalization.AtPrime.{u_1, u_2} (Rₚ P) P
inst_5 : IsDomain R
hpid : ∀ (P : Ideal R) [inst : P.IsMaximal], IsPrincipalIdealRing.{u_2} (Rₚ P)
this : IsNoetherianRing R
⊢ IsIntegrallyClosed R

Tactic:
IsIntegrallyClosed.of_isLocalization_maximal Rₚ fun P hP => ?_

Premises used: IsIntegrallyClosed.of_isLocalization_maximal
-- Module: Mathlib.RingTheory.LocalProperties.Semilocal
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Finite.{u_1 + 1} (MaximalSpectrum R)
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_2
inst_2 : (P : Ideal R) → [inst : P.IsMaximal] → CommRing (Rₚ P)
inst_3 : (P : Ideal R) → [inst_6 : P.IsMaximal] → Algebra.{u_1, u_2} R (Rₚ P)
inst_4 : ∀ (P : Ideal R) [inst_6 : P.IsMaximal], IsLocalization.AtPrime.{u_1, u_2} (Rₚ P) P
inst_5 : IsDomain R
hpid : ∀ (P : Ideal R) [inst : P.IsMaximal], IsPrincipalIdealRing.{u_2} (Rₚ P)
this : IsNoetherianRing R
refine : ∀ (P : Ideal R) (hP : P.IsMaximal), IsIntegrallyClosed.{u_2} (Rₚ P)
⊢ IsIntegrallyClosed R

Tactic:
refine IsIntegrallyClosed.of_isLocalization_maximal Rₚ fun P hP => ?_

Premises used: IsIntegrallyClosed.of_isLocalization_maximal
-- Module: Mathlib.RingTheory.LocalProperties.Semilocal
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Finite.{u_1 + 1} (MaximalSpectrum R)
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_2
inst_2 : (P : Ideal R) → [inst : P.IsMaximal] → CommRing (Rₚ P)
inst_3 : (P : Ideal R) → [inst_6 : P.IsMaximal] → Algebra.{u_1, u_2} R (Rₚ P)
inst_4 : ∀ (P : Ideal R) [inst_6 : P.IsMaximal], IsLocalization.AtPrime.{u_1, u_2} (Rₚ P) P
inst_5 : IsDomain R
hpid : ∀ (P : Ideal R) [inst : P.IsMaximal], IsPrincipalIdealRing.{u_2} (Rₚ P)
this : IsNoetherianRing R
P : Ideal R
hP : P.IsMaximal
⊢ IsDomain.{u_2} (Rₚ P)

Tactic:
have : IsDomain (Rₚ P) := IsLocalization.isDomain_of_atPrime (Rₚ P) P
-- Module: Mathlib.RingTheory.LocalProperties.Semilocal
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Finite.{u_1 + 1} (MaximalSpectrum R)
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_2
inst_2 : (P : Ideal R) → [inst : P.IsMaximal] → CommRing (Rₚ P)
inst_3 : (P : Ideal R) → [inst_6 : P.IsMaximal] → Algebra.{u_1, u_2} R (Rₚ P)
inst_4 : ∀ (P : Ideal R) [inst_6 : P.IsMaximal], IsLocalization.AtPrime.{u_1, u_2} (Rₚ P) P
inst_5 : IsDomain R
hpid : ∀ (P : Ideal R) [inst : P.IsMaximal], IsPrincipalIdealRing.{u_2} (Rₚ P)
this_1 : IsNoetherianRing R
P : Ideal R
hP : P.IsMaximal
this : IsDomain.{u_2} (Rₚ P)
⊢ IsIntegrallyClosed.{u_2} (Rₚ P)

Tactic:
infer_instance
-- Module: Mathlib.RingTheory.LocalProperties.Semilocal
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Finite.{u_1 + 1} (MaximalSpectrum R)
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_2
inst_2 : (P : Ideal R) → [inst : P.IsMaximal] → CommRing (Rₚ P)
inst_3 : (P : Ideal R) → [inst_6 : P.IsMaximal] → Algebra.{u_1, u_2} R (Rₚ P)
inst_4 : ∀ (P : Ideal R) [inst_6 : P.IsMaximal], IsLocalization.AtPrime.{u_1, u_2} (Rₚ P) P
inst_5 : IsDomain R
hpid : ∀ (P : Ideal R) [inst : P.IsMaximal], IsPrincipalIdealRing.{u_2} (Rₚ P)
this : IsNoetherianRing R
⊢ IsIntegrallyClosed R

Tactic:
have : IsIntegrallyClosed R := by
    refine IsIntegrallyClosed.of_isLocalization_maximal Rₚ fun P hP => ?_
    have : IsDomain (Rₚ P) := IsLocalization.isDomain_of_atPrime (Rₚ P) P
    infer_instance
-- Module: Mathlib.RingTheory.LocalProperties.Semilocal
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Finite.{u_1 + 1} (MaximalSpectrum R)
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_2
inst_2 : (P : Ideal R) → [inst : P.IsMaximal] → CommRing (Rₚ P)
inst_3 : (P : Ideal R) → [inst_6 : P.IsMaximal] → Algebra.{u_1, u_2} R (Rₚ P)
inst_4 : ∀ (P : Ideal R) [inst_6 : P.IsMaximal], IsLocalization.AtPrime.{u_1, u_2} (Rₚ P) P
inst_5 : IsDomain R
hpid : ∀ (P : Ideal R) [inst : P.IsMaximal], IsPrincipalIdealRing.{u_2} (Rₚ P)
this_1 : IsNoetherianRing R
this : IsIntegrallyClosed R
⊢ Ring.KrullDimLE 1 R

Tactic:
have : Ring.KrullDimLE 1 R :=
    Ring.krullDimLE_of_isLocalization_maximal Rₚ fun P _ => inferInstance
-- Module: Mathlib.RingTheory.LocalProperties.Semilocal
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Finite.{u_1 + 1} (MaximalSpectrum R)
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_2
inst_2 : (P : Ideal R) → [inst : P.IsMaximal] → CommRing (Rₚ P)
inst_3 : (P : Ideal R) → [inst_6 : P.IsMaximal] → Algebra.{u_1, u_2} R (Rₚ P)
inst_4 : ∀ (P : Ideal R) [inst_6 : P.IsMaximal], IsLocalization.AtPrime.{u_1, u_2} (Rₚ P) P
inst_5 : IsDomain R
hpid : ∀ (P : Ideal R) [inst : P.IsMaximal], IsPrincipalIdealRing.{u_2} (Rₚ P)
this_1 : IsNoetherianRing R
this_2 : IsIntegrallyClosed R
this : Ring.KrullDimLE 1 R
⊢ ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → I.IsMaximal

Tactic:
rw [Ring.krullDimLE_one_iff_of_noZeroDivisors] at this

Premises used: Ring.krullDimLE_one_iff_of_noZeroDivisors
-- Module: Mathlib.RingTheory.LocalProperties.Semilocal
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Finite.{u_1 + 1} (MaximalSpectrum R)
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_2
inst_2 : (P : Ideal R) → [inst : P.IsMaximal] → CommRing (Rₚ P)
inst_3 : (P : Ideal R) → [inst_6 : P.IsMaximal] → Algebra.{u_1, u_2} R (Rₚ P)
inst_4 : ∀ (P : Ideal R) [inst_6 : P.IsMaximal], IsLocalization.AtPrime.{u_1, u_2} (Rₚ P) P
inst_5 : IsDomain R
hpid : ∀ (P : Ideal R) [inst : P.IsMaximal], IsPrincipalIdealRing.{u_2} (Rₚ P)
this_1 : IsNoetherianRing R
this_2 : IsIntegrallyClosed R
this : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → I.IsMaximal
⊢ IsDedekindDomain R

Tactic:
have dedekind : IsDedekindDomain R := { maximalOfPrime := this _ }
-- Module: Mathlib.RingTheory.LocalProperties.Semilocal
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Finite.{u_1 + 1} (MaximalSpectrum R)
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_2
inst_2 : (P : Ideal R) → [inst : P.IsMaximal] → CommRing (Rₚ P)
inst_3 : (P : Ideal R) → [inst_6 : P.IsMaximal] → Algebra.{u_1, u_2} R (Rₚ P)
inst_4 : ∀ (P : Ideal R) [inst_6 : P.IsMaximal], IsLocalization.AtPrime.{u_1, u_2} (Rₚ P) P
inst_5 : IsDomain R
hpid : ∀ (P : Ideal R) [inst : P.IsMaximal], IsPrincipalIdealRing.{u_2} (Rₚ P)
this_1 : IsNoetherianRing R
this_2 : IsIntegrallyClosed R
this : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → I.IsMaximal
dedekind : IsDedekindDomain R
rw : Set.Finite.{u_1} (α := Ideal R) (Set.range MaximalSpectrum.asIdeal)
⊢ Set.Finite.{u_1} (α := Ideal R) {P : Ideal R | P.IsMaximal}

Tactic:
rw [← MaximalSpectrum.range_asIdeal]

Premises used: MaximalSpectrum.range_asIdeal
-- Module: Mathlib.RingTheory.LocalProperties.Semilocal
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Finite.{u_1 + 1} (MaximalSpectrum R)
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_2
inst_2 : (P : Ideal R) → [inst : P.IsMaximal] → CommRing (Rₚ P)
inst_3 : (P : Ideal R) → [inst_6 : P.IsMaximal] → Algebra.{u_1, u_2} R (Rₚ P)
inst_4 : ∀ (P : Ideal R) [inst_6 : P.IsMaximal], IsLocalization.AtPrime.{u_1, u_2} (Rₚ P) P
inst_5 : IsDomain R
hpid : ∀ (P : Ideal R) [inst : P.IsMaximal], IsPrincipalIdealRing.{u_2} (Rₚ P)
this_1 : IsNoetherianRing R
this_2 : IsIntegrallyClosed R
this : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → I.IsMaximal
dedekind : IsDedekindDomain R
⊢ Set.Finite.{u_1} (α := Ideal R) (Set.range MaximalSpectrum.asIdeal)

Tactic:
Set.finite_range MaximalSpectrum.asIdeal

Premises used: MaximalSpectrum.asIdeal, Set.finite_range
-- Module: Mathlib.RingTheory.LocalProperties.Semilocal
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Finite.{u_1 + 1} (MaximalSpectrum R)
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_2
inst_2 : (P : Ideal R) → [inst : P.IsMaximal] → CommRing (Rₚ P)
inst_3 : (P : Ideal R) → [inst_6 : P.IsMaximal] → Algebra.{u_1, u_2} R (Rₚ P)
inst_4 : ∀ (P : Ideal R) [inst_6 : P.IsMaximal], IsLocalization.AtPrime.{u_1, u_2} (Rₚ P) P
inst_5 : IsDomain R
hpid : ∀ (P : Ideal R) [inst : P.IsMaximal], IsPrincipalIdealRing.{u_2} (Rₚ P)
this_1 : IsNoetherianRing R
this_2 : IsIntegrallyClosed R
this : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → I.IsMaximal
dedekind : IsDedekindDomain R
⊢ Set.Finite.{u_1} (α := Ideal R) (Set.range MaximalSpectrum.asIdeal)

Tactic:
exact Set.finite_range MaximalSpectrum.asIdeal

Premises used: MaximalSpectrum.asIdeal, Set.finite_range
-- Module: Mathlib.RingTheory.LocalProperties.Semilocal
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Finite.{u_1 + 1} (MaximalSpectrum R)
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_2
inst_2 : (P : Ideal R) → [inst : P.IsMaximal] → CommRing (Rₚ P)
inst_3 : (P : Ideal R) → [inst_6 : P.IsMaximal] → Algebra.{u_1, u_2} R (Rₚ P)
inst_4 : ∀ (P : Ideal R) [inst_6 : P.IsMaximal], IsLocalization.AtPrime.{u_1, u_2} (Rₚ P) P
inst_5 : IsDomain R
hpid : ∀ (P : Ideal R) [inst : P.IsMaximal], IsPrincipalIdealRing.{u_2} (Rₚ P)
this_1 : IsNoetherianRing R
this_2 : IsIntegrallyClosed R
this : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → I.IsMaximal
dedekind : IsDedekindDomain R
⊢ Set.Finite.{u_1} (α := Ideal R) {P : Ideal R | P.IsMaximal}

Tactic:
have hp_finite : {P : Ideal R | P.IsMaximal}.Finite := by
    rw [← MaximalSpectrum.range_asIdeal]
    exact Set.finite_range MaximalSpectrum.asIdeal
-- Module: Mathlib.RingTheory.LocalProperties.Semilocal
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Finite.{u_1 + 1} (MaximalSpectrum R)
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_2
inst_2 : (P : Ideal R) → [inst : P.IsMaximal] → CommRing (Rₚ P)
inst_3 : (P : Ideal R) → [inst_6 : P.IsMaximal] → Algebra.{u_1, u_2} R (Rₚ P)
inst_4 : ∀ (P : Ideal R) [inst_6 : P.IsMaximal], IsLocalization.AtPrime.{u_1, u_2} (Rₚ P) P
inst_5 : IsDomain R
hpid : ∀ (P : Ideal R) [inst : P.IsMaximal], IsPrincipalIdealRing.{u_2} (Rₚ P)
this_1 : IsNoetherianRing R
this_2 : IsIntegrallyClosed R
this : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → I.IsMaximal
dedekind : IsDedekindDomain R
hp_finite : Set.Finite.{u_1} (α := Ideal R) {P : Ideal R | P.IsMaximal}
⊢ IsPrincipalIdealRing R

Tactic:
IsPrincipalIdealRing.of_finite_maximals hp_finite

Premises used: IsPrincipalIdealRing.of_finite_maximals
-- Module: Mathlib.RingTheory.LocalProperties.Semilocal
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Finite.{u_1 + 1} (MaximalSpectrum R)
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_2
inst_2 : (P : Ideal R) → [inst : P.IsMaximal] → CommRing (Rₚ P)
inst_3 : (P : Ideal R) → [inst_6 : P.IsMaximal] → Algebra.{u_1, u_2} R (Rₚ P)
inst_4 : ∀ (P : Ideal R) [inst_6 : P.IsMaximal], IsLocalization.AtPrime.{u_1, u_2} (Rₚ P) P
inst_5 : IsDomain R
hpid : ∀ (P : Ideal R) [inst : P.IsMaximal], IsPrincipalIdealRing.{u_2} (Rₚ P)
this_1 : IsNoetherianRing R
this_2 : IsIntegrallyClosed R
this : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → I.IsMaximal
dedekind : IsDedekindDomain R
hp_finite : Set.Finite.{u_1} (α := Ideal R) {P : Ideal R | P.IsMaximal}
⊢ IsPrincipalIdealRing R

Tactic:
exact IsPrincipalIdealRing.of_finite_maximals hp_finite

Premises used: IsPrincipalIdealRing.of_finite_maximals
-- Module: Mathlib.RingTheory.LocalProperties.Submodule
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_5
inst_3 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst_4 : (P : Ideal R) → [inst_6 : P.IsMaximal] → Module.{u_1, u_5} R (Mₚ P)
f : (P : Ideal R) → [inst_6 : P.IsMaximal] → LinearMap.{u_1, u_1, u_2, u_5} (RingHom.id R) M (Mₚ P)
inst_5 : ∀ (P : Ideal R) [inst_6 : P.IsMaximal], IsLocalizedModule (M' := Mₚ P) P.primeCompl (f P)
m : M
N : Submodule R M
h :
  ∀ (P : Ideal R) [inst_6 : P.IsMaximal],
    Membership.mem (α := Mₚ P) (γ := Submodule R (Mₚ P)) (localized₀ P.primeCompl (f P) N)
      ((f P : (a : M) → Mₚ P) m : Mₚ P)
I : Ideal R := comap (LinearMap.toSpanSingleton R M m) N
this : I = ⊤
⊢ m ∈ N

Tactic:
simpa [I] using I.eq_top_iff_one.mp this

Premises used: Ideal.eq_top_iff_one, Iff.mp
-- Module: Mathlib.RingTheory.LocalProperties.Submodule
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_5
inst_3 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst_4 : (P : Ideal R) → [inst_6 : P.IsMaximal] → Module.{u_1, u_5} R (Mₚ P)
f : (P : Ideal R) → [inst_6 : P.IsMaximal] → LinearMap.{u_1, u_1, u_2, u_5} (RingHom.id R) M (Mₚ P)
inst_5 : ∀ (P : Ideal R) [inst_6 : P.IsMaximal], IsLocalizedModule (M' := Mₚ P) P.primeCompl (f P)
m : M
N : Submodule R M
h :
  ∀ (P : Ideal R) [inst_6 : P.IsMaximal],
    Membership.mem (α := Mₚ P) (γ := Submodule R (Mₚ P)) (localized₀ P.primeCompl (f P) N)
      ((f P : (a : M) → Mₚ P) m : Mₚ P)
I : Ideal R := comap (LinearMap.toSpanSingleton R M m) N
suffices : I = ⊤
⊢ m ∈ N

Tactic:
suffices I = ⊤ by simpa [I] using I.eq_top_iff_one.mp this
-- Module: Mathlib.RingTheory.LocalProperties.Submodule
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_5
inst_3 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst_4 : (P : Ideal R) → [inst_6 : P.IsMaximal] → Module.{u_1, u_5} R (Mₚ P)
f : (P : Ideal R) → [inst_6 : P.IsMaximal] → LinearMap.{u_1, u_1, u_2, u_5} (RingHom.id R) M (Mₚ P)
inst_5 : ∀ (P : Ideal R) [inst_6 : P.IsMaximal], IsLocalizedModule (M' := Mₚ P) P.primeCompl (f P)
m : M
N : Submodule R M
h :
  ∀ (P : Ideal R) [inst_6 : P.IsMaximal],
    Membership.mem (α := Mₚ P) (γ := Submodule R (Mₚ P)) (localized₀ P.primeCompl (f P) N)
      ((f P : (a : M) → Mₚ P) m : Mₚ P)
I : Ideal R := comap (LinearMap.toSpanSingleton R M m) N
⊢ I = ⊤

Tactic:
Not.imp_symm I.exists_le_maximal fun ⟨P, hP, le⟩ ↦ ?_

Premises used: False, Not.imp_symm, Ideal.exists_le_maximal, _private.0.Submodule.mem_of_localization_maximal.match_1
-- Module: Mathlib.RingTheory.LocalProperties.Submodule
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_5
inst_3 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst_4 : (P : Ideal R) → [inst_6 : P.IsMaximal] → Module.{u_1, u_5} R (Mₚ P)
f : (P : Ideal R) → [inst_6 : P.IsMaximal] → LinearMap.{u_1, u_1, u_2, u_5} (RingHom.id R) M (Mₚ P)
inst_5 : ∀ (P : Ideal R) [inst_6 : P.IsMaximal], IsLocalizedModule (M' := Mₚ P) P.primeCompl (f P)
m : M
N : Submodule R M
h :
  ∀ (P : Ideal R) [inst_6 : P.IsMaximal],
    Membership.mem (α := Mₚ P) (γ := Submodule R (Mₚ P)) (localized₀ P.primeCompl (f P) N)
      ((f P : (a : M) → Mₚ P) m : Mₚ P)
I : Ideal R := comap (LinearMap.toSpanSingleton R M m) N
refine : (∃ (M : Ideal R), M.IsMaximal ∧ I ≤ M) → ∀ (P : Ideal R) (hP : P.IsMaximal) (le : I ≤ P), False
⊢ I = ⊤

Tactic:
refine Not.imp_symm I.exists_le_maximal fun ⟨P, hP, le⟩ ↦ ?_

Premises used: False, Not.imp_symm, Ideal.exists_le_maximal, _private.0.Submodule.mem_of_localization_maximal.match_1
-- Module: Mathlib.RingTheory.LocalProperties.Submodule
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_5
inst_3 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst_4 : (P : Ideal R) → [inst_6 : P.IsMaximal] → Module.{u_1, u_5} R (Mₚ P)
f : (P : Ideal R) → [inst_6 : P.IsMaximal] → LinearMap.{u_1, u_1, u_2, u_5} (RingHom.id R) M (Mₚ P)
inst_5 : ∀ (P : Ideal R) [inst_6 : P.IsMaximal], IsLocalizedModule (M' := Mₚ P) P.primeCompl (f P)
m : M
N : Submodule R M
h :
  ∀ (P : Ideal R) [inst_6 : P.IsMaximal],
    Membership.mem (α := Mₚ P) (γ := Submodule R (Mₚ P)) (localized₀ P.primeCompl (f P) N)
      ((f P : (a : M) → Mₚ P) m : Mₚ P)
I : Ideal R := comap (LinearMap.toSpanSingleton R M m) N
h_1 : ∃ (M : Ideal R), M.IsMaximal ∧ I ≤ M
P : Ideal R
hP : P.IsMaximal
le : I ≤ P
obtain :
  ∀ (a : M) (ha : a ∈ N) (s : ↥P.primeCompl)
    (e : Eq (α := Mₚ P) (IsLocalizedModule.mk' (f P) a s) ((f P : (a : M) → Mₚ P) m)), False
⊢ False

Tactic:
obtain ⟨a, ha, s, e⟩ := h P
-- Module: Mathlib.RingTheory.LocalProperties.Submodule
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_5
inst_3 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst_4 : (P : Ideal R) → [inst_6 : P.IsMaximal] → Module.{u_1, u_5} R (Mₚ P)
f : (P : Ideal R) → [inst_6 : P.IsMaximal] → LinearMap.{u_1, u_1, u_2, u_5} (RingHom.id R) M (Mₚ P)
inst_5 : ∀ (P : Ideal R) [inst_6 : P.IsMaximal], IsLocalizedModule (M' := Mₚ P) P.primeCompl (f P)
m : M
N : Submodule R M
h :
  ∀ (P : Ideal R) [inst_6 : P.IsMaximal],
    Membership.mem (α := Mₚ P) (γ := Submodule R (Mₚ P)) (localized₀ P.primeCompl (f P) N)
      ((f P : (a : M) → Mₚ P) m : Mₚ P)
I : Ideal R := comap (LinearMap.toSpanSingleton R M m) N
h_1 : ∃ (M : Ideal R), M.IsMaximal ∧ I ≤ M
P : Ideal R
hP : P.IsMaximal
le : I ≤ P
a : M
ha : a ∈ N
s : ↥P.primeCompl
e : Eq (α := Mₚ P) (IsLocalizedModule.mk' (f P) a s) ((f P : (a : M) → Mₚ P) m)
⊢ ∃ (s_1 : ↥P.primeCompl), s_1 • s • m = s_1 • HSMul.hSMul.{u_1, u_2, u_2} (α := ↥P.primeCompl) 1 a

Tactic:
rw [← IsLocalizedModule.mk'_one P.primeCompl, IsLocalizedModule.mk'_eq_mk'_iff] at e

Premises used: IsLocalizedModule.mk'_eq_mk'_iff, IsLocalizedModule.mk'_one, Ideal.primeCompl
-- Module: Mathlib.RingTheory.LocalProperties.Submodule
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_5
inst_3 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst_4 : (P : Ideal R) → [inst_6 : P.IsMaximal] → Module.{u_1, u_5} R (Mₚ P)
f : (P : Ideal R) → [inst_6 : P.IsMaximal] → LinearMap.{u_1, u_1, u_2, u_5} (RingHom.id R) M (Mₚ P)
inst_5 : ∀ (P : Ideal R) [inst_6 : P.IsMaximal], IsLocalizedModule (M' := Mₚ P) P.primeCompl (f P)
m : M
N : Submodule R M
h :
  ∀ (P : Ideal R) [inst_6 : P.IsMaximal],
    Membership.mem (α := Mₚ P) (γ := Submodule R (Mₚ P)) (localized₀ P.primeCompl (f P) N)
      ((f P : (a : M) → Mₚ P) m : Mₚ P)
I : Ideal R := comap (LinearMap.toSpanSingleton R M m) N
h_1 : ∃ (M : Ideal R), M.IsMaximal ∧ I ≤ M
P : Ideal R
hP : P.IsMaximal
le : I ≤ P
a : M
ha : a ∈ N
s : ↥P.primeCompl
e : ∃ (s_1 : ↥P.primeCompl), s_1 • s • m = s_1 • HSMul.hSMul.{u_1, u_2, u_2} (α := ↥P.primeCompl) 1 a
obtain : ∀ (t : ↥P.primeCompl) (ht : t • s • m = t • HSMul.hSMul.{u_1, u_2, u_2} (α := ↥P.primeCompl) 1 a), False
⊢ False

Tactic:
obtain ⟨t, ht⟩ := e
-- Module: Mathlib.RingTheory.LocalProperties.Submodule
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_5
inst_3 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst_4 : (P : Ideal R) → [inst_6 : P.IsMaximal] → Module.{u_1, u_5} R (Mₚ P)
f : (P : Ideal R) → [inst_6 : P.IsMaximal] → LinearMap.{u_1, u_1, u_2, u_5} (RingHom.id R) M (Mₚ P)
inst_5 : ∀ (P : Ideal R) [inst_6 : P.IsMaximal], IsLocalizedModule (M' := Mₚ P) P.primeCompl (f P)
m : M
N : Submodule R M
h :
  ∀ (P : Ideal R) [inst_6 : P.IsMaximal],
    Membership.mem (α := Mₚ P) (γ := Submodule R (Mₚ P)) (localized₀ P.primeCompl (f P) N)
      ((f P : (a : M) → Mₚ P) m : Mₚ P)
I : Ideal R := comap (LinearMap.toSpanSingleton R M m) N
h_1 : ∃ (M : Ideal R), M.IsMaximal ∧ I ≤ M
P : Ideal R
hP : P.IsMaximal
le : I ≤ P
a : M
ha : a ∈ N
s t : ↥P.primeCompl
ht : t • s • m = t • HSMul.hSMul.{u_1, u_2, u_2} (α := ↥P.primeCompl) 1 a
⊢ (t * s) • m = (t * 1) • a

Tactic:
simp_rw [smul_smul] at ht

Premises used: smul_smul
-- Module: Mathlib.RingTheory.LocalProperties.Submodule
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_5
inst_3 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst_4 : (P : Ideal R) → [inst_6 : P.IsMaximal] → Module.{u_1, u_5} R (Mₚ P)
f : (P : Ideal R) → [inst_6 : P.IsMaximal] → LinearMap.{u_1, u_1, u_2, u_5} (RingHom.id R) M (Mₚ P)
inst_5 : ∀ (P : Ideal R) [inst_6 : P.IsMaximal], IsLocalizedModule (M' := Mₚ P) P.primeCompl (f P)
m : M
N : Submodule R M
h :
  ∀ (P : Ideal R) [inst_6 : P.IsMaximal],
    Membership.mem (α := Mₚ P) (γ := Submodule R (Mₚ P)) (localized₀ P.primeCompl (f P) N)
      ((f P : (a : M) → Mₚ P) m : Mₚ P)
I : Ideal R := comap (LinearMap.toSpanSingleton R M m) N
h_1 : ∃ (M : Ideal R), M.IsMaximal ∧ I ≤ M
P : Ideal R
hP : P.IsMaximal
le : I ≤ P
a : M
ha : a ∈ N
s t : ↥P.primeCompl
ht : (t * s) • m = (t * 1) • a
⊢ (↑(t * s) : R) ∈ I

Tactic:
apply ht ▸ smul_mem _ _ ha
-- Module: Mathlib.RingTheory.LocalProperties.Submodule
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_5
inst_3 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst_4 : (P : Ideal R) → [inst_6 : P.IsMaximal] → Module.{u_1, u_5} R (Mₚ P)
f : (P : Ideal R) → [inst_6 : P.IsMaximal] → LinearMap.{u_1, u_1, u_2, u_5} (RingHom.id R) M (Mₚ P)
inst_5 : ∀ (P : Ideal R) [inst_6 : P.IsMaximal], IsLocalizedModule (M' := Mₚ P) P.primeCompl (f P)
m : M
N : Submodule R M
h :
  ∀ (P : Ideal R) [inst_6 : P.IsMaximal],
    Membership.mem (α := Mₚ P) (γ := Submodule R (Mₚ P)) (localized₀ P.primeCompl (f P) N)
      ((f P : (a : M) → Mₚ P) m : Mₚ P)
I : Ideal R := comap (LinearMap.toSpanSingleton R M m) N
h_1 : ∃ (M : Ideal R), M.IsMaximal ∧ I ≤ M
P : Ideal R
hP : P.IsMaximal
le : I ≤ P
a : M
ha : a ∈ N
s t : ↥P.primeCompl
ht : (t * s) • m = (t * 1) • a
⊢ False

Tactic:
exact (t * s).2 (le <| by apply ht ▸ smul_mem _ _ ha)

Premises used: HMul.hMul, Subtype.property
-- Module: Mathlib.RingTheory.LocalProperties.Submodule
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_5
inst_3 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst_4 : (P : Ideal R) → [inst_6 : P.IsMaximal] → Module.{u_1, u_5} R (Mₚ P)
f : (P : Ideal R) → [inst_6 : P.IsMaximal] → LinearMap.{u_1, u_1, u_2, u_5} (RingHom.id R) M (Mₚ P)
inst_5 : ∀ (P : Ideal R) [inst_6 : P.IsMaximal], IsLocalizedModule (M' := Mₚ P) P.primeCompl (f P)
N₁ N₂ : Submodule R M
h :
  ∀ (P : Ideal R) [inst_6 : P.IsMaximal],
    LE.le (α := Submodule R (Mₚ P)) (localized₀ P.primeCompl (f P) N₁) (localized₀ P.primeCompl (f P) N₂)
m : M
hm : m ∈ N₁
P : Ideal R
hP : P.IsMaximal
⊢ Eq (α := Mₚ P) (IsLocalizedModule.mk' (S := P.primeCompl) (f P) m 1) ((f P : (a : M) → Mₚ P) m)

Tactic:
simp
-- Module: Mathlib.RingTheory.LocalProperties.Submodule
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_5
inst_3 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst_4 : (P : Ideal R) → [inst_6 : P.IsMaximal] → Module.{u_1, u_5} R (Mₚ P)
f : (P : Ideal R) → [inst_6 : P.IsMaximal] → LinearMap.{u_1, u_1, u_2, u_5} (RingHom.id R) M (Mₚ P)
inst_5 : ∀ (P : Ideal R) [inst_6 : P.IsMaximal], IsLocalizedModule (M' := Mₚ P) P.primeCompl (f P)
N₁ N₂ : Submodule R M
h :
  ∀ (P : Ideal R) [inst_6 : P.IsMaximal],
    Eq (α := Submodule R (Mₚ P)) (localized₀ P.primeCompl (f P) N₁) (localized₀ P.primeCompl (f P) N₂)
⊢ N₁ = N₂

Tactic:
le_antisymm (Submodule.le_of_localization_maximal Mₚ f fun P _ ↦ (h P).le)
    (Submodule.le_of_localization_maximal Mₚ f fun P _ ↦ (h P).ge)

Premises used: Eq.ge, Submodule.le_of_localization_maximal, Eq.le, le_antisymm