awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
P Q : {R S : Type u} → [inst : CommRing R] → [inst_8 : CommRing S] → (R →+* S) → Prop
hP : LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hQ : LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
r : R
R' S' : Type u
inst_2 : CommRing R'
inst_3 : CommRing S'
inst_4 : Algebra R R'
inst_5 : Algebra S S'
inst_6 : IsLocalization.Away r R'
inst_7 : IsLocalization.Away (R := S) ((f : (a : R) → S) r : S) S'
h : P f ∧ Q f
⊢ P (IsLocalization.Away.map R' S' f r) ∧ Q (IsLocalization.Away.map R' S' f r)

Tactic:
⟨hP f r R' S' h.1, hQ f r R' S' h.2⟩

Premises used: And.right, And.left, And.intro
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
P Q : {R S : Type u} → [inst : CommRing R] → [inst_8 : CommRing S] → (R →+* S) → Prop
hP : LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hQ : LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
r : R
R' S' : Type u
inst_2 : CommRing R'
inst_3 : CommRing S'
inst_4 : Algebra R R'
inst_5 : Algebra S S'
inst_6 : IsLocalization.Away r R'
inst_7 : IsLocalization.Away (R := S) ((f : (a : R) → S) r : S) S'
h : P f ∧ Q f
⊢ P (IsLocalization.Away.map R' S' f r) ∧ Q (IsLocalization.Away.map R' S' f r)

Tactic:
exact ⟨hP f r R' S' h.1, hQ f r R' S' h.2⟩
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
P Q : {R S : Type u} → [inst : CommRing R] → [inst_4 : CommRing S] → (R →+* S) → Prop
hP : StableUnderCompositionWithLocalizationAwayTarget.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hQ : StableUnderCompositionWithLocalizationAwayTarget.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
R S T : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra S T
s : S
h : IsLocalization.Away s T
f : R →+* S
hf : P f ∧ Q f
⊢ P (comp (algebraMap S T) f) ∧ Q (comp (algebraMap S T) f)

Tactic:
⟨hP T s f hf.1, hQ T s f hf.2⟩

Premises used: And.right, And.left, And.intro
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
P Q : {R S : Type u} → [inst : CommRing R] → [inst_4 : CommRing S] → (R →+* S) → Prop
hP : StableUnderCompositionWithLocalizationAwayTarget.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hQ : StableUnderCompositionWithLocalizationAwayTarget.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
R S T : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra S T
s : S
h : IsLocalization.Away s T
f : R →+* S
hf : P f ∧ Q f
⊢ P (comp (algebraMap S T) f) ∧ Q (comp (algebraMap S T) f)

Tactic:
exact ⟨hP T s f hf.1, hQ T s f hf.2⟩
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_13 : CommRing S] → (R →+* S) → Prop
hP : IsStableUnderBaseChange @P
R S Rᵣ Sᵣ : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing Rᵣ
inst_3 : CommRing Sᵣ
inst_4 : Algebra R Rᵣ
inst_5 : Algebra S Sᵣ
inst_6 : Algebra R S
inst_7 : Algebra R Sᵣ
inst_8 : Algebra Rᵣ Sᵣ
inst_9 : IsScalarTower R S Sᵣ
inst_10 : IsScalarTower R Rᵣ Sᵣ
M : Submonoid R
inst_11 : IsLocalization M Rᵣ
inst_12 : IsLocalization (Algebra.algebraMapSubmonoid S M) Sᵣ
h : P (algebraMap R S)
⊢ P (algebraMap Rᵣ Sᵣ)

Tactic:
letI : Algebra.IsPushout R S Rᵣ Sᵣ := Algebra.isPushout_of_isLocalization M Rᵣ S Sᵣ
  hP R S Rᵣ Sᵣ h
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_8 : CommRing S] → (R →+* S) → Prop
hP : IsStableUnderBaseChange @P
R S Rᵣ Sᵣ : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing Rᵣ
inst_3 : CommRing Sᵣ
inst_4 : Algebra R Rᵣ
inst_5 : Algebra S Sᵣ
M : Submonoid R
inst_6 : IsLocalization M Rᵣ
f : R →+* S
inst_7 : IsLocalization (Submonoid.map f M) Sᵣ
hf : P f
algInst : Algebra R S := f.toAlgebra
algInst_1 : Algebra Rᵣ Sᵣ := toAlgebra (IsLocalization.map Sᵣ f ⋯)
algInst_2 : Algebra R Sᵣ :=
  toAlgebra (@comp _ _ _ _ Semiring.toNonAssocSemiring _ (IsLocalization.map Sᵣ f ⋯) (algebraMap R Rᵣ))
scalarTowerInst : IsScalarTower R Rᵣ Sᵣ := ⋯
haveI : ∀ (this : IsScalarTower R S Sᵣ), P (R := Rᵣ) (IsLocalization.map Sᵣ f ⋯)
⊢ P (R := Rᵣ) (IsLocalization.map Sᵣ f ⋯)

Tactic:
haveI : IsScalarTower R S Sᵣ := IsScalarTower.of_algebraMap_eq'
    (IsLocalization.map_comp M.le_comap_map)
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_8 : CommRing S] → (R →+* S) → Prop
hP : IsStableUnderBaseChange @P
R S Rᵣ Sᵣ : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing Rᵣ
inst_3 : CommRing Sᵣ
inst_4 : Algebra R Rᵣ
inst_5 : Algebra S Sᵣ
M : Submonoid R
inst_6 : IsLocalization M Rᵣ
f : R →+* S
inst_7 : IsLocalization (Submonoid.map f M) Sᵣ
hf : P f
algInst : Algebra R S := f.toAlgebra
algInst_1 : Algebra Rᵣ Sᵣ := toAlgebra (IsLocalization.map Sᵣ f ⋯)
algInst_2 : Algebra R Sᵣ :=
  toAlgebra (@comp _ _ _ _ Semiring.toNonAssocSemiring _ (IsLocalization.map Sᵣ f ⋯) (algebraMap R Rᵣ))
scalarTowerInst : IsScalarTower R Rᵣ Sᵣ := ⋯
this : IsScalarTower R S Sᵣ
⊢ IsLocalization (Algebra.algebraMapSubmonoid S M) Sᵣ

Tactic:
haveI : IsLocalization (Algebra.algebraMapSubmonoid S M) Sᵣ :=
    inferInstanceAs <| IsLocalization (M.map f) Sᵣ
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_8 : CommRing S] → (R →+* S) → Prop
hP : IsStableUnderBaseChange @P
R S Rᵣ Sᵣ : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing Rᵣ
inst_3 : CommRing Sᵣ
inst_4 : Algebra R Rᵣ
inst_5 : Algebra S Sᵣ
M : Submonoid R
inst_6 : IsLocalization M Rᵣ
f : R →+* S
inst_7 : IsLocalization (Submonoid.map f M) Sᵣ
hf : P f
algInst : Algebra R S := f.toAlgebra
algInst_1 : Algebra Rᵣ Sᵣ := toAlgebra (IsLocalization.map Sᵣ f ⋯)
algInst_2 : Algebra R Sᵣ :=
  toAlgebra (@comp _ _ _ _ Semiring.toNonAssocSemiring _ (IsLocalization.map Sᵣ f ⋯) (algebraMap R Rᵣ))
scalarTowerInst : IsScalarTower R Rᵣ Sᵣ := ⋯
this_1 : IsScalarTower R S Sᵣ
this : IsLocalization (Algebra.algebraMapSubmonoid S M) Sᵣ
⊢ P (R := Rᵣ) (IsLocalization.map Sᵣ f ⋯)

Tactic:
apply hP.of_isLocalization M hf

Premises used: RingHom.IsStableUnderBaseChange.of_isLocalization
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_8 : CommRing S] → (R →+* S) → Prop
hP : IsStableUnderBaseChange @P
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
M : Submonoid R
R' S' : Type u
inst_2 : CommRing R'
inst_3 : CommRing S'
inst_4 : Algebra R R'
inst_5 : Algebra S S'
inst_6 : IsLocalization M R'
inst_7 : IsLocalization (Submonoid.map f M) S'
hf : P f
⊢ P (R := R') (IsLocalization.map S' f ⋯)

Tactic:
hP.isLocalization_map _ _ hf

Premises used: RingHom.IsStableUnderBaseChange.isLocalization_map
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_8 : CommRing S] → (R →+* S) → Prop
hP : IsStableUnderBaseChange @P
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
M : Submonoid R
R' S' : Type u
inst_2 : CommRing R'
inst_3 : CommRing S'
inst_4 : Algebra R R'
inst_5 : Algebra S S'
inst_6 : IsLocalization M R'
inst_7 : IsLocalization (Submonoid.map f M) S'
hf : P f
⊢ P (R := R') (IsLocalization.map S' f ⋯)

Tactic:
exact hP.isLocalization_map _ _ hf

Premises used: RingHom.IsStableUnderBaseChange.isLocalization_map
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
p : Submonoid R
inst_3 : IsLocalization p S
I : Ideal R
rw :
  Eq (α := Submodule S S) (Submodule.localized' S p (Algebra.linearMap R S) I)
    (span ((⇑(algebraMap R S) : (a : R) → S) '' (↑I : Set R)))
rw₁ :
  Eq (α := Submodule S S) (Submodule.localized' S p (Algebra.linearMap R S) I)
    (Submodule.span S ((⇑(algebraMap R S) : (a : R) → S) '' (↑I : Set R)))
rw₂ :
  Eq (α := Submodule S S) (Submodule.span S ((⇑(Algebra.linearMap R S) : (a : R) → S) '' (↑I : Set R)))
    (Submodule.span S ((⇑(algebraMap R S) : (a : R) → S) '' (↑I : Set R)))
rw₃ rw₄ :
  Eq (α := Submodule S S) (Submodule.span S ((⇑(algebraMap R S) : (a : R) → S) '' (↑I : Set R)))
    (Submodule.span S ((⇑(algebraMap R S) : (a : R) → S) '' (↑I : Set R)))
⊢ Eq (α := Submodule S S) (Submodule.localized' S p (Algebra.linearMap R S) I) (map (F := R →+* S) (algebraMap R S) I)

Tactic:
rw [map, span, Submodule.localized'_eq_span, Algebra.coe_linearMap]

Premises used: Ideal.map, Submodule.localized'_eq_span, Ideal.span, Algebra.coe_linearMap
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
p : Submonoid R
inst_3 : IsLocalization p S
I : Ideal R
⊢ Eq (α := Submodule R S) (Submodule.localized₀ p (Algebra.linearMap R S) I)
    (Submodule.restrictScalars R (map (F := R →+* S) (algebraMap R S) I))

Tactic:
congr(Submodule.restrictScalars R $(localized'_eq_map S p I))

Premises used: congrArg, Submodule.restrictScalars, Ideal.localized'_eq_map, id
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
p : Submonoid R
inst_3 : IsLocalization p S
I : Ideal R
⊢ Eq (α := LinearMap.{u_1, u_1, u_1, u_2} (RingHom.id R) ↥I ↥(Ideal.map (F := R →+* S) (algebraMap R S) I))
    (idealMap S I)
    (((↑(LinearEquiv.ofEq (Submodule.localized₀ p (Algebra.linearMap R S) I)
              (Submodule.restrictScalars R (Ideal.map (F := R →+* S) (algebraMap R S) I)) ⋯) :
          ↥(Submodule.localized₀ p (Algebra.linearMap R S) I) →ₗ[R]
            ↥(Submodule.restrictScalars R (Ideal.map (F := R →+* S) (algebraMap R S) I))) :
        ↥(Submodule.localized₀ p (Algebra.linearMap R S) I) →ₗ[R]
          ↥(Submodule.restrictScalars R (Ideal.map (F := R →+* S) (algebraMap R S) I))) ∘ₗ
      (Submodule.toLocalized₀ p (Algebra.linearMap R S) I :
        LinearMap.{u_1, u_1, u_1, u_2} (RingHom.id R) ↥I ↥(Submodule.localized₀ p (Algebra.linearMap R S) I)))

Tactic:
rfl

Premises used: Algebra.idealMap, LinearMap.restrict, LinearMap.codRestrict, rfl
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
R : Type u_1
inst : CommSemiring R
r : R
J : Ideal R
h :
  ∀ (P : Ideal R) (x : P.IsMaximal),
    Membership.mem (α := Localization.AtPrime P) (γ := Ideal (Localization.AtPrime P))
      (map (F := R →+* Localization.AtPrime P) (algebraMap R (Localization.AtPrime P)) J)
      ((algebraMap R (Localization.AtPrime P) : (a : R) → Localization.AtPrime P) r : Localization.AtPrime P)
P : Ideal R
hP : P.IsMaximal
⊢ Membership.mem (α := Localization.AtPrime P) (γ := Submodule R (Localization.AtPrime P))
    (Submodule.localized₀ P.primeCompl (Algebra.linearMap R (Localization.AtPrime P)) J)
    ((Algebra.linearMap R (Localization.AtPrime P) : (a : R) → Localization.AtPrime P) r : Localization.AtPrime P)

Tactic:
apply (localized'_eq_map (Localization.AtPrime P) P.primeCompl J).symm ▸ h P hP
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
R : Type u_1
inst : CommSemiring R
I J : Ideal R
h :
  ∀ (P : Ideal R) (x : P.IsMaximal),
    LE.le (α := Ideal (Localization.AtPrime P))
      (map (F := R →+* Localization.AtPrime P) (algebraMap R (Localization.AtPrime P)) I)
      (map (F := R →+* Localization.AtPrime P) (algebraMap R (Localization.AtPrime P)) J)
⊢ I ≤ J

Tactic:
fun _ hm ↦ mem_of_localization_maximal fun P hP ↦ h P hP (mem_map_of_mem _ hm)

Premises used: Algebra.algebraMap, Ideal.mem_map_of_mem, Set.Mem, Localization.AtPrime, Ideal.mem_of_localization_maximal
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
x : R
hx :
  Membership.mem (γ := Submodule R R)
    (⨅ (p : Ideal R),
      ⨅ (x : p.IsPrime),
        ⨅ (_ : I ≤ p), RingHom.ker (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p)))
    x
⊢ x ∈ I

Tactic:
Ideal.mem_of_localization_maximal fun m hm ↦ ?_

Premises used: Set.Mem, Ideal.mem_of_localization_maximal
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
x : R
hx :
  Membership.mem (γ := Submodule R R)
    (⨅ (p : Ideal R),
      ⨅ (x : p.IsPrime),
        ⨅ (_ : I ≤ p), RingHom.ker (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p)))
    x
refine :
  ∀ (m : Ideal R) (hm : m.IsMaximal),
    Membership.mem (α := Localization.AtPrime m) (γ := Ideal (Localization.AtPrime m))
      (map (F := R →+* Localization.AtPrime m) (algebraMap R (Localization.AtPrime m)) I)
      ((algebraMap R (Localization.AtPrime m) : (a : R) → Localization.AtPrime m) x : Localization.AtPrime m)
⊢ x ∈ I

Tactic:
refine Ideal.mem_of_localization_maximal fun m hm ↦ ?_

Premises used: Ideal.mem_of_localization_maximal
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
x : R
hx :
  Membership.mem (γ := Submodule R R)
    (⨅ (p : Ideal R),
      ⨅ (x : p.IsPrime),
        ⨅ (_ : I ≤ p), RingHom.ker (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p)))
    x
m : Ideal R
hm : m.IsMaximal
⊢ ∀ (i : Ideal R) (i_1 : i.IsPrime) (i_2 : I ≤ i),
    Eq (α := Localization.AtPrime i)
      ((algebraMap R (Localization.AtPrime i) : (a : R) → Localization.AtPrime i) x : Localization.AtPrime i)
      (0 : Localization.AtPrime i)

Tactic:
simp only [Submodule.mem_iInf, RingHom.mem_ker] at hx

Premises used: Submodule.mem_iInf, RingHom.mem_ker
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
x : R
m : Ideal R
hm : m.IsMaximal
hx :
  ∀ (i : Ideal R) (i_1 : i.IsPrime) (i_2 : I ≤ i),
    Eq (α := Localization.AtPrime i)
      ((algebraMap R (Localization.AtPrime i) : (a : R) → Localization.AtPrime i) x : Localization.AtPrime i)
      (0 : Localization.AtPrime i)
pos :
  ∀ (hle : I ≤ m),
    Membership.mem (α := Localization.AtPrime m) (γ := Ideal (Localization.AtPrime m))
      (map (F := R →+* Localization.AtPrime m) (algebraMap R (Localization.AtPrime m)) I)
      ((algebraMap R (Localization.AtPrime m) : (a : R) → Localization.AtPrime m) x : Localization.AtPrime m)
neg :
  ∀ (hle : ¬I ≤ m),
    Membership.mem (α := Localization.AtPrime m) (γ := Ideal (Localization.AtPrime m))
      (map (F := R →+* Localization.AtPrime m) (algebraMap R (Localization.AtPrime m)) I)
      ((algebraMap R (Localization.AtPrime m) : (a : R) → Localization.AtPrime m) x : Localization.AtPrime m)
⊢ Membership.mem (α := Localization.AtPrime m) (γ := Ideal (Localization.AtPrime m))
    (map (F := R →+* Localization.AtPrime m) (algebraMap R (Localization.AtPrime m)) I)
    ((algebraMap R (Localization.AtPrime m) : (a : R) → Localization.AtPrime m) x : Localization.AtPrime m)

Tactic:
by_cases hle : I ≤ m
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
x : R
m : Ideal R
hm : m.IsMaximal
hx :
  ∀ (i : Ideal R) (i_1 : i.IsPrime) (i_2 : I ≤ i),
    Eq (α := Localization.AtPrime i)
      ((algebraMap R (Localization.AtPrime i) : (a : R) → Localization.AtPrime i) x : Localization.AtPrime i)
      (0 : Localization.AtPrime i)
hle : I ≤ m
⊢ Membership.mem (α := Localization.AtPrime m) (γ := Ideal (Localization.AtPrime m))
    (map (F := R →+* Localization.AtPrime m) (algebraMap R (Localization.AtPrime m)) I)
    ((algebraMap R (Localization.AtPrime m) : (a : R) → Localization.AtPrime m) x : Localization.AtPrime m)

Tactic:
simp [hx _ _ hle]
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
x : R
m : Ideal R
hm : m.IsMaximal
hx :
  ∀ (i : Ideal R) (i_1 : i.IsPrime) (i_2 : I ≤ i),
    Eq (α := Localization.AtPrime i)
      ((algebraMap R (Localization.AtPrime i) : (a : R) → Localization.AtPrime i) x : Localization.AtPrime i)
      (0 : Localization.AtPrime i)
hle : ¬I ≤ m
⊢ Membership.mem (α := Localization.AtPrime m) (γ := Ideal (Localization.AtPrime m))
    (map (F := R →+* Localization.AtPrime m) (algebraMap R (Localization.AtPrime m)) I)
    ((algebraMap R (Localization.AtPrime m) : (a : R) → Localization.AtPrime m) x : Localization.AtPrime m)

Tactic:
simp [IsLocalization.AtPrime.map_eq_top_of_not_le _ hle]

Premises used: IsLocalization.AtPrime.map_eq_top_of_not_le
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
R : Type u_1
inst : CommSemiring R
I J : Ideal R
h :
  ∀ (P : Ideal R) (x : P.IsMaximal),
    Eq (α := Ideal (Localization.AtPrime P))
      (map (F := R →+* Localization.AtPrime P) (algebraMap R (Localization.AtPrime P)) I)
      (map (F := R →+* Localization.AtPrime P) (algebraMap R (Localization.AtPrime P)) J)
⊢ I = J

Tactic:
le_antisymm (le_of_localization_maximal fun P hP ↦ (h P hP).le)
    (le_of_localization_maximal fun P hP ↦ (h P hP).ge)

Premises used: Eq.ge, Ideal.le_of_localization_maximal, Eq.le, le_antisymm
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
h :
  ∀ (J : Ideal R) (x : J.IsMaximal),
    Eq (α := Ideal (Localization.AtPrime J))
      (Ideal.map (F := R →+* Localization.AtPrime J) (algebraMap R (Localization.AtPrime J)) I) ⊥
P : Ideal R
hP : P.IsMaximal
⊢ Eq (α := Ideal (Localization.AtPrime P))
    (Ideal.map (F := R →+* Localization.AtPrime P) (algebraMap R (Localization.AtPrime P)) I)
    (Ideal.map (R := R) (F := R →+* Localization.AtPrime P) (algebraMap R (Localization.AtPrime P)) ⊥)

Tactic:
simpa using h P hP
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
R : Type u_1
inst : CommSemiring R
r : R
h :
  ∀ (J : Ideal R) (x : J.IsMaximal),
    Eq (α := Localization.AtPrime J)
      ((algebraMap R (Localization.AtPrime J) : (a : R) → Localization.AtPrime J) r : Localization.AtPrime J)
      (0 : Localization.AtPrime J)
⊢ r = 0

Tactic:
Module.eq_zero_of_localization_maximal _ (fun _ _ ↦ Algebra.linearMap R _) r h

Premises used: Module.eq_zero_of_localization_maximal, Algebra.linearMap
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
h :
  ∀ (J : Ideal R) (x : J.IsMaximal),
    Eq (α := Submodule R (Localization.AtPrime J)) (IsLocalization.coeSubmodule (Localization.AtPrime J) I) ⊥
⊢ I = ⊥

Tactic:
bot_unique fun r hr ↦ eq_zero_of_localization r fun J hJ ↦ (h J hJ).le ⟨r, hr, rfl⟩

Premises used: Eq.le, eq_zero_of_localization, And.intro, Exists.intro, bot_unique, rfl
-- Module: Mathlib.RingTheory.LocalProperties.Exactness
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_6
inst_5 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst_6 : (P : Ideal R) → [inst_11 : P.IsMaximal] → Module.{u_1, u_6} R (Mₚ P)
f : (P : Ideal R) → [inst_11 : P.IsMaximal] → LinearMap.{u_1, u_1, u_2, u_6} (RingHom.id R) M (Mₚ P)
inst_7 : ∀ (P : Ideal R) [inst_11 : P.IsMaximal], IsLocalizedModule.AtPrime (M' := Mₚ P) P (f P)
Nₚ : (P : Ideal R) → [P.IsMaximal] → Type u_7
inst_8 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Nₚ P)
inst_9 : (P : Ideal R) → [inst_11 : P.IsMaximal] → Module.{u_1, u_7} R (Nₚ P)
g : (P : Ideal R) → [inst_11 : P.IsMaximal] → LinearMap.{u_1, u_1, u_3, u_7} (RingHom.id R) N (Nₚ P)
inst_10 : ∀ (P : Ideal R) [inst_11 : P.IsMaximal], IsLocalizedModule.AtPrime (M' := Nₚ P) P (g P)
F : M →ₗ[R] N
H :
  ∀ (P : Ideal R) [inst_11 : P.IsMaximal],
    Function.Injective.{u_6 + 1, u_7 + 1} (α := Mₚ P) (β := Nₚ P)
      (⇑((IsLocalizedModule.map P.primeCompl (f P) (g P) : (a : M →ₗ[R] N) → Mₚ P →ₗ[R] Nₚ P) F :
            LinearMap.{u_1, u_1, u_6, u_7} (RingHom.id R) (Mₚ P) (Nₚ P)) :
        (a : Mₚ P) → Nₚ P)
x y : M
eq : Eq.{u_3 + 1} (α := N) ((F : (a : M) → N) x : N) ((F : (a : M) → N) y : N)
P : Ideal R
h : P.IsMaximal
⊢ Eq.{u_7 + 1} (α := Nₚ P)
    ((((IsLocalizedModule.map P.primeCompl (f P) (g P) : (a : M →ₗ[R] N) → Mₚ P →ₗ[R] Nₚ P) F :
            LinearMap.{u_1, u_1, u_6, u_7} (RingHom.id R) (Mₚ P) (Nₚ P)) :
          (a : Mₚ P) → Nₚ P)
        ((f P : (a : M) → Mₚ P) x : Mₚ P) :
      Nₚ P)
    ((((IsLocalizedModule.map P.primeCompl (f P) (g P) : (a : M →ₗ[R] N) → Mₚ P →ₗ[R] Nₚ P) F :
            LinearMap.{u_1, u_1, u_6, u_7} (RingHom.id R) (Mₚ P) (Nₚ P)) :
          (a : Mₚ P) → Nₚ P)
        ((f P : (a : M) → Mₚ P) y : Mₚ P) :
      Nₚ P)

Tactic:
simp [eq]
-- Module: Mathlib.RingTheory.LocalProperties.Exactness
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_6
inst_5 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst_6 : (P : Ideal R) → [inst_11 : P.IsMaximal] → Module.{u_1, u_6} R (Mₚ P)
f : (P : Ideal R) → [inst_11 : P.IsMaximal] → LinearMap.{u_1, u_1, u_2, u_6} (RingHom.id R) M (Mₚ P)
inst_7 : ∀ (P : Ideal R) [inst_11 : P.IsMaximal], IsLocalizedModule.AtPrime (M' := Mₚ P) P (f P)
Nₚ : (P : Ideal R) → [P.IsMaximal] → Type u_7
inst_8 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Nₚ P)
inst_9 : (P : Ideal R) → [inst_11 : P.IsMaximal] → Module.{u_1, u_7} R (Nₚ P)
g : (P : Ideal R) → [inst_11 : P.IsMaximal] → LinearMap.{u_1, u_1, u_3, u_7} (RingHom.id R) N (Nₚ P)
inst_10 : ∀ (P : Ideal R) [inst_11 : P.IsMaximal], IsLocalizedModule.AtPrime (M' := Nₚ P) P (g P)
F : M →ₗ[R] N
H :
  ∀ (P : Ideal R) [inst_11 : P.IsMaximal],
    Function.Surjective.{u_6 + 1, u_7 + 1} (α := Mₚ P) (β := Nₚ P)
      (⇑((IsLocalizedModule.map P.primeCompl (f P) (g P) : (a : M →ₗ[R] N) → Mₚ P →ₗ[R] Nₚ P) F :
            LinearMap.{u_1, u_1, u_6, u_7} (RingHom.id R) (Mₚ P) (Nₚ P)) :
        (a : Mₚ P) → Nₚ P)
⊢ Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑F : (a : M) → N)

Tactic:
range_eq_top.mp <| eq_top_of_localization₀_maximal Nₚ g _ <|
    fun P _ ↦ (range_localizedMap_eq_localized₀_range _ (f P) (g P) F).symm.trans <|
    range_eq_top.mpr <| H P

Premises used: Iff.mpr, LinearMap.range_eq_top, Iff.mp, Submodule.eq_top_of_localization₀_maximal, Ideal.primeCompl, Eq.symm, Eq.trans, LinearMap.range_localizedMap_eq_localized₀_range
-- Module: Mathlib.RingTheory.LocalProperties.Exactness
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_6
inst_5 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst_6 : (P : Ideal R) → [inst_11 : P.IsMaximal] → Module.{u_1, u_6} R (Mₚ P)
f : (P : Ideal R) → [inst_11 : P.IsMaximal] → LinearMap.{u_1, u_1, u_2, u_6} (RingHom.id R) M (Mₚ P)
inst_7 : ∀ (P : Ideal R) [inst_11 : P.IsMaximal], IsLocalizedModule.AtPrime (M' := Mₚ P) P (f P)
Nₚ : (P : Ideal R) → [P.IsMaximal] → Type u_7
inst_8 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Nₚ P)
inst_9 : (P : Ideal R) → [inst_11 : P.IsMaximal] → Module.{u_1, u_7} R (Nₚ P)
g : (P : Ideal R) → [inst_11 : P.IsMaximal] → LinearMap.{u_1, u_1, u_3, u_7} (RingHom.id R) N (Nₚ P)
inst_10 : ∀ (P : Ideal R) [inst_11 : P.IsMaximal], IsLocalizedModule.AtPrime (M' := Nₚ P) P (g P)
F : M →ₗ[R] N
H :
  ∀ (P : Ideal R) [inst_11 : P.IsMaximal],
    Function.Bijective.{u_6 + 1, u_7 + 1} (α := Mₚ P) (β := Nₚ P)
      (⇑((IsLocalizedModule.map P.primeCompl (f P) (g P) : (a : M →ₗ[R] N) → Mₚ P →ₗ[R] Nₚ P) F :
            LinearMap.{u_1, u_1, u_6, u_7} (RingHom.id R) (Mₚ P) (Nₚ P)) :
        (a : Mₚ P) → Nₚ P)
⊢ Function.Bijective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑F : (a : M) → N)

Tactic:
⟨injective_of_isLocalized_maximal Mₚ f Nₚ g F fun J _ ↦ (H J).1,
  surjective_of_isLocalized_maximal Mₚ f Nₚ g F fun J _ ↦ (H J).2⟩

Premises used: surjective_of_isLocalized_maximal, injective_of_isLocalized_maximal, And.right, And.left, And.intro, Function.Bijective