awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Basic (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
hP : OfLocalizationSpanTarget.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hP' : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set S
hs : Eq (α := Ideal S) (Ideal.span s) ⊤
hT_1 :
  ∀ (r : (↑s : Type u)),
    ∃ (T : Type u) (x : CommRing T) (x_1 : Algebra S T) (_ : IsLocalization.Away (↑r : S) T),
      P (comp (algebraMap S T) f)
r : (↑s : Type u)
T : Type u
w : CommRing T
w_1 : Algebra S T
w_2 : IsLocalization.Away (↑r : S) T
hT : P (comp (algebraMap S T) f)
h :
  Eq (α := R →+* Localization.Away (↑r : S))
    (comp (algebraMap S (Localization.Away (↑r : S))) f : R →+* Localization.Away (↑r : S))
    (comp
        (@comp _ _ _ _ Semiring.toNonAssocSemiring _
          (RingEquiv.toRingHom
            (AlgEquiv.toRingEquiv (AlgEquiv.symm (Localization.algEquiv (Submonoid.powers (↑r : S)) T))))
          (algebraMap S T))
        f :
      R →+* Localization (Submonoid.powers (↑r : S)))
h₁ :
  Eq (α := R →+* Localization.Away (↑r : S)) (comp (algebraMap S (Localization.Away (↑r : S))) f)
    (comp
      (@comp _ _ _ _ Semiring.toNonAssocSemiring _
        (↑(AlgEquiv.toRingEquiv (AlgEquiv.symm (Localization.algEquiv (Submonoid.powers (↑r : S)) T))) :
          T →+* Localization (Submonoid.powers (↑r : S)))
        (algebraMap S T))
      f)
h₂ :
  Eq (α := R →+* Localization.Away (↑r : S)) (comp (algebraMap S (Localization.Away (↑r : S))) f)
    (comp
      (@comp _ _ _ _ Semiring.toNonAssocSemiring _
        (↑(AlgEquiv.symm (Localization.algEquiv (Submonoid.powers (↑r : S)) T)) :
          T →+* Localization (Submonoid.powers (↑r : S)))
        (algebraMap S T))
      f)
h₃ :
  Eq (α := R →+* Localization.Away (↑r : S)) (comp (algebraMap S (Localization.Away (↑r : S))) f)
    (comp
      (@comp _ _ _ _ Semiring.toNonAssocSemiring _
        (IsLocalization.map (M := Submonoid.powers (↑r : S)) (T := Submonoid.powers (↑r : S))
          (Localization (Submonoid.powers (↑r : S))) (id S) ⋯)
        (algebraMap S T))
      f)
h₄ :
  Eq (α := R →+* Localization.Away (↑r : S)) (comp (algebraMap S (Localization.Away (↑r : S))) f)
    (comp (comp (algebraMap S (Localization (Submonoid.powers (↑r : S)))) (id S)) f)
⊢ Eq (α := R →+* Localization.Away (↑r : S))
    (comp (algebraMap S (Localization.Away (↑r : S))) f : R →+* Localization.Away (↑r : S))
    (@comp _ _ _ _ Semiring.toNonAssocSemiring _
        (RingEquiv.toRingHom
          (AlgEquiv.toRingEquiv (AlgEquiv.symm (Localization.algEquiv (Submonoid.powers (↑r : S)) T))))
        (comp (algebraMap S T) f) :
      R →+* Localization (Submonoid.powers (↑r : S)))
have h₅ : Eq (α := R →+* Localization.Away (↑r : S)) (comp (algebraMap S (Localization.Away (↑r : S))) f)
  (comp (algebraMap S (Localization (Submonoid.powers (↑r : S)))) f)
Tactic: rw [← RingHom.comp_assoc, RingEquiv.toRingHom_eq_coe,
    AlgEquiv.toRingEquiv_toRingHom, Localization.coe_algEquiv_symm, IsLocalization.map_comp,
    RingHom.comp_id]
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Basic (goal)
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ᵣ := ⋯
⊢ P (R := Rᵣ) (IsLocalization.map Sᵣ f ⋯)
have haveI : ∀ (this : IsScalarTower R S Sᵣ), P (R := Rᵣ) (IsLocalization.map Sᵣ f sorry)
Tactic: haveI : IsScalarTower R S Sᵣ := IsScalarTower.of_algebraMap_eq'
    (IsLocalization.map_comp M.le_comap_map)
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Basic (hypothesis)
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ᵣ
⊢ P (R := Rᵣ) (IsLocalization.map Sᵣ f ⋯)
have this₁ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sᵣ
Tactic: haveI : IsLocalization (Algebra.algebraMapSubmonoid S M) Sᵣ :=
    inferInstanceAs <| IsLocalization (M.map f) Sᵣ
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Basic (goal)
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 S S) (Submodule.localized' S p (Algebra.linearMap R S) I) (map (F := R →+* S) (algebraMap R S) I)
have rw : Eq (α := Submodule S S) (Submodule.localized' S p (Algebra.linearMap R S) I)
  (span ((⇑(algebraMap R S) : (a : R) → S) '' (↑I : Set R)))
Tactic: rw [map, span, Submodule.localized'_eq_span, Algebra.coe_linearMap]
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Basic (goal)
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)))
⊢ Eq (α := Submodule S S) (Submodule.localized' S p (Algebra.linearMap R S) I) (map (F := R →+* S) (algebraMap R S) I)
have 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)))
Tactic: rw [map, span, Submodule.localized'_eq_span, Algebra.coe_linearMap]
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Basic (goal)
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)))
⊢ Eq (α := Submodule S S) (Submodule.localized' S p (Algebra.linearMap R S) I) (map (F := R →+* S) (algebraMap R S) I)
have 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)))
Tactic: rw [map, span, Submodule.localized'_eq_span, Algebra.coe_linearMap]
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Basic (goal)
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)))
⊢ Eq (α := Submodule S S) (Submodule.localized' S p (Algebra.linearMap R S) I) (map (F := R →+* S) (algebraMap R S) I)
have 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)))
Tactic: rw [map, span, Submodule.localized'_eq_span, Algebra.coe_linearMap]
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Basic (goal)
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
have 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)
Tactic: refine Ideal.mem_of_localization_maximal fun m hm ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Basic (hypothesis)
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
⊢ 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)
have 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)
Tactic: simp only [Submodule.mem_iInf, RingHom.mem_ker] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Basic (goal)
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)
⊢ 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)
have 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)
Tactic: by_cases hle : I ≤ m
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Basic (goal)
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)
⊢ 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)
have 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)
Tactic: by_cases hle : I ≤ m
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Exactness (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
L : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : AddCommMonoid L
inst_6 : Module R L
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_6
inst_7 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst_8 : (P : Ideal R) → [inst_16 : P.IsMaximal] → Module.{u_1, u_6} R (Mₚ P)
f : (P : Ideal R) → [inst_16 : P.IsMaximal] → LinearMap.{u_1, u_1, u_2, u_6} (RingHom.id R) M (Mₚ P)
inst_9 : ∀ (P : Ideal R) [inst_16 : P.IsMaximal], IsLocalizedModule.AtPrime (M' := Mₚ P) P (f P)
Nₚ : (P : Ideal R) → [P.IsMaximal] → Type u_7
inst_10 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Nₚ P)
inst_11 : (P : Ideal R) → [inst_16 : P.IsMaximal] → Module.{u_1, u_7} R (Nₚ P)
g : (P : Ideal R) → [inst_16 : P.IsMaximal] → LinearMap.{u_1, u_1, u_3, u_7} (RingHom.id R) N (Nₚ P)
inst_12 : ∀ (P : Ideal R) [inst_16 : P.IsMaximal], IsLocalizedModule.AtPrime (M' := Nₚ P) P (g P)
Lₚ : (P : Ideal R) → [P.IsMaximal] → Type u_8
inst_13 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Lₚ P)
inst_14 : (P : Ideal R) → [inst_16 : P.IsMaximal] → Module.{u_1, u_8} R (Lₚ P)
h : (P : Ideal R) → [inst_16 : P.IsMaximal] → LinearMap.{u_1, u_1, u_4, u_8} (RingHom.id R) L (Lₚ P)
inst_15 : ∀ (P : Ideal R) [inst_16 : P.IsMaximal], IsLocalizedModule.AtPrime (M' := Lₚ P) P (h P)
F : M →ₗ[R] N
G : N →ₗ[R] L
H :
  ∀ (J : Ideal R) [inst_16 : J.IsMaximal],
    Function.Exact.{u_6, u_7, u_8} (M := Mₚ J) (N := Nₚ J) (P := Lₚ J)
      (⇑((IsLocalizedModule.map J.primeCompl (f J) (g J) : (a : M →ₗ[R] N) → Mₚ J →ₗ[R] Nₚ J) F :
            LinearMap.{u_1, u_1, u_6, u_7} (RingHom.id R) (Mₚ J) (Nₚ J)) :
        (a : Mₚ J) → Nₚ J)
      (⇑((IsLocalizedModule.map J.primeCompl (g J) (h J) : (a : N →ₗ[R] L) → Nₚ J →ₗ[R] Lₚ J) G :
            LinearMap.{u_1, u_1, u_7, u_8} (RingHom.id R) (Nₚ J) (Lₚ J)) :
        (a : Nₚ J) → Lₚ J)
⊢ Function.Exact.{u_2, u_3, u_4} (M := M) (N := N) (P := L) (⇑F : (a : M) → N) (⇑G : (a : N) → L)
have simp : ∀
  (H :
    ∀ (J : Ideal R) [inst_16 : J.IsMaximal],
      Eq.{u_7 + 1} (α := Submodule R (Nₚ J))
        (ker.{u_1, u_1, u_7, u_8} (R₂ := R) (M₂ := Lₚ J) (τ₁₂ := RingHom.id R)
          ((IsLocalizedModule.map J.primeCompl (g J) (h J) : (a : N →ₗ[R] L) → Nₚ J →ₗ[R] Lₚ J) G))
        (range.{u_1, u_1, u_6, u_7} (R := R) (M := Mₚ J) (τ₁₂ := RingHom.id R)
          ((IsLocalizedModule.map J.primeCompl (f J) (g J) : (a : M →ₗ[R] N) → Mₚ J →ₗ[R] Nₚ J) F))),
  G.ker = F.range
Tactic: simp only [LinearMap.exact_iff] at H ⊢
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Exactness (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
L : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : AddCommMonoid L
inst_6 : Module R L
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_6
inst_7 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst_8 : (P : Ideal R) → [inst_16 : P.IsMaximal] → Module.{u_1, u_6} R (Mₚ P)
f : (P : Ideal R) → [inst_16 : P.IsMaximal] → LinearMap.{u_1, u_1, u_2, u_6} (RingHom.id R) M (Mₚ P)
inst_9 : ∀ (P : Ideal R) [inst_16 : P.IsMaximal], IsLocalizedModule.AtPrime (M' := Mₚ P) P (f P)
Nₚ : (P : Ideal R) → [P.IsMaximal] → Type u_7
inst_10 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Nₚ P)
inst_11 : (P : Ideal R) → [inst_16 : P.IsMaximal] → Module.{u_1, u_7} R (Nₚ P)
g : (P : Ideal R) → [inst_16 : P.IsMaximal] → LinearMap.{u_1, u_1, u_3, u_7} (RingHom.id R) N (Nₚ P)
inst_12 : ∀ (P : Ideal R) [inst_16 : P.IsMaximal], IsLocalizedModule.AtPrime (M' := Nₚ P) P (g P)
Lₚ : (P : Ideal R) → [P.IsMaximal] → Type u_8
inst_13 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Lₚ P)
inst_14 : (P : Ideal R) → [inst_16 : P.IsMaximal] → Module.{u_1, u_8} R (Lₚ P)
h : (P : Ideal R) → [inst_16 : P.IsMaximal] → LinearMap.{u_1, u_1, u_4, u_8} (RingHom.id R) L (Lₚ P)
inst_15 : ∀ (P : Ideal R) [inst_16 : P.IsMaximal], IsLocalizedModule.AtPrime (M' := Lₚ P) P (h P)
F : M →ₗ[R] N
G : N →ₗ[R] L
H :
  ∀ (J : Ideal R) [inst_16 : J.IsMaximal],
    Eq.{u_7 + 1} (α := Submodule R (Nₚ J))
      (ker.{u_1, u_1, u_7, u_8} (R₂ := R) (M₂ := Lₚ J) (τ₁₂ := RingHom.id R)
        ((IsLocalizedModule.map J.primeCompl (g J) (h J) : (a : N →ₗ[R] L) → Nₚ J →ₗ[R] Lₚ J) G))
      (range.{u_1, u_1, u_6, u_7} (R := R) (M := Mₚ J) (τ₁₂ := RingHom.id R)
        ((IsLocalizedModule.map J.primeCompl (f J) (g J) : (a : M →ₗ[R] N) → Mₚ J →ₗ[R] Nₚ J) F))
⊢ G.ker = F.range
have apply : ∀ (P : Ideal R) [inst_16 : P.IsMaximal],
  Eq (α := Submodule R (Nₚ P)) (localized₀ P.primeCompl (g P) G.ker) (localized₀ P.primeCompl (g P) F.range)
Tactic: apply eq_of_localization₀_maximal Nₚ g
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Exactness (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
L : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : AddCommMonoid L
inst_6 : Module R L
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_6
inst_7 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst_8 : (P : Ideal R) → [inst_16 : P.IsMaximal] → Module.{u_1, u_6} R (Mₚ P)
f : (P : Ideal R) → [inst_16 : P.IsMaximal] → LinearMap.{u_1, u_1, u_2, u_6} (RingHom.id R) M (Mₚ P)
inst_9 : ∀ (P : Ideal R) [inst_16 : P.IsMaximal], IsLocalizedModule.AtPrime (M' := Mₚ P) P (f P)
Nₚ : (P : Ideal R) → [P.IsMaximal] → Type u_7
inst_10 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Nₚ P)
inst_11 : (P : Ideal R) → [inst_16 : P.IsMaximal] → Module.{u_1, u_7} R (Nₚ P)
g : (P : Ideal R) → [inst_16 : P.IsMaximal] → LinearMap.{u_1, u_1, u_3, u_7} (RingHom.id R) N (Nₚ P)
inst_12 : ∀ (P : Ideal R) [inst_16 : P.IsMaximal], IsLocalizedModule.AtPrime (M' := Nₚ P) P (g P)
Lₚ : (P : Ideal R) → [P.IsMaximal] → Type u_8
inst_13 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Lₚ P)
inst_14 : (P : Ideal R) → [inst_16 : P.IsMaximal] → Module.{u_1, u_8} R (Lₚ P)
h : (P : Ideal R) → [inst_16 : P.IsMaximal] → LinearMap.{u_1, u_1, u_4, u_8} (RingHom.id R) L (Lₚ P)
inst_15 : ∀ (P : Ideal R) [inst_16 : P.IsMaximal], IsLocalizedModule.AtPrime (M' := Lₚ P) P (h P)
F : M →ₗ[R] N
G : N →ₗ[R] L
H :
  ∀ (J : Ideal R) [inst_16 : J.IsMaximal],
    Eq.{u_7 + 1} (α := Submodule R (Nₚ J))
      (ker.{u_1, u_1, u_7, u_8} (R₂ := R) (M₂ := Lₚ J) (τ₁₂ := RingHom.id R)
        ((IsLocalizedModule.map J.primeCompl (g J) (h J) : (a : N →ₗ[R] L) → Nₚ J →ₗ[R] Lₚ J) G))
      (range.{u_1, u_1, u_6, u_7} (R := R) (M := Mₚ J) (τ₁₂ := RingHom.id R)
        ((IsLocalizedModule.map J.primeCompl (f J) (g J) : (a : M →ₗ[R] N) → Mₚ J →ₗ[R] Nₚ J) F))
J : Ideal R
hJ : J.IsMaximal
⊢ Eq (α := Submodule R (Nₚ J)) (localized₀ J.primeCompl (g J) G.ker) (localized₀ J.primeCompl (g J) F.range)
have rw : Eq.{u_7 + 1} (α := Submodule R (Nₚ J))
  (ker.{u_1, u_1, u_7, u_8} (R₂ := R) (M₂ := Lₚ J) (τ₁₂ := RingHom.id R)
    ((IsLocalizedModule.map J.primeCompl (g J) (h J) : (a : N →ₗ[R] L) → Nₚ J →ₗ[R] Lₚ J) G))
  (range.{u_1, u_1, u_6, u_7} (R := R) (M := Mₚ J) (τ₁₂ := RingHom.id R)
    ((IsLocalizedModule.map J.primeCompl (f J) (g J) : (a : M →ₗ[R] N) → Mₚ J →ₗ[R] Nₚ J) F))
Tactic: rw [← LinearMap.range_localizedMap_eq_localized₀_range _ (f J) (g J) F,
    ← LinearMap.ker_localizedMap_eq_localized₀_ker J.primeCompl (g J) (h J) G]
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Exactness (hypothesis)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
L : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : AddCommMonoid L
inst_6 : Module R L
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_6
inst_7 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst_8 : (P : Ideal R) → [inst_16 : P.IsMaximal] → Module.{u_1, u_6} R (Mₚ P)
f : (P : Ideal R) → [inst_16 : P.IsMaximal] → LinearMap.{u_1, u_1, u_2, u_6} (RingHom.id R) M (Mₚ P)
inst_9 : ∀ (P : Ideal R) [inst_16 : P.IsMaximal], IsLocalizedModule.AtPrime (M' := Mₚ P) P (f P)
Nₚ : (P : Ideal R) → [P.IsMaximal] → Type u_7
inst_10 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Nₚ P)
inst_11 : (P : Ideal R) → [inst_16 : P.IsMaximal] → Module.{u_1, u_7} R (Nₚ P)
g : (P : Ideal R) → [inst_16 : P.IsMaximal] → LinearMap.{u_1, u_1, u_3, u_7} (RingHom.id R) N (Nₚ P)
inst_12 : ∀ (P : Ideal R) [inst_16 : P.IsMaximal], IsLocalizedModule.AtPrime (M' := Nₚ P) P (g P)
Lₚ : (P : Ideal R) → [P.IsMaximal] → Type u_8
inst_13 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Lₚ P)
inst_14 : (P : Ideal R) → [inst_16 : P.IsMaximal] → Module.{u_1, u_8} R (Lₚ P)
h : (P : Ideal R) → [inst_16 : P.IsMaximal] → LinearMap.{u_1, u_1, u_4, u_8} (RingHom.id R) L (Lₚ P)
inst_15 : ∀ (P : Ideal R) [inst_16 : P.IsMaximal], IsLocalizedModule.AtPrime (M' := Lₚ P) P (h P)
F : M →ₗ[R] N
G : N →ₗ[R] L
H :
  ∀ (J : Ideal R) [inst_16 : J.IsMaximal],
    Eq.{u_7 + 1} (α := Submodule R (Nₚ J))
      (ker.{u_1, u_1, u_7, u_8} (R₂ := R) (M₂ := Lₚ J) (τ₁₂ := RingHom.id R)
        ((IsLocalizedModule.map J.primeCompl (g J) (h J) : (a : N →ₗ[R] L) → Nₚ J →ₗ[R] Lₚ J) G))
      (range.{u_1, u_1, u_6, u_7} (R := R) (M := Mₚ J) (τ₁₂ := RingHom.id R)
        ((IsLocalizedModule.map J.primeCompl (f J) (g J) : (a : M →ₗ[R] N) → Mₚ J →ₗ[R] Nₚ J) F))
J : Ideal R
hJ : J.IsMaximal
⊢ Eq.{u_7 + 1} (α := Submodule R (Nₚ J))
    (ker.{u_1, u_1, u_7, u_8} (R₂ := R) (M₂ := Lₚ J) (τ₁₂ := RingHom.id R)
      ((IsLocalizedModule.map J.primeCompl (g J) (h J) : (a : N →ₗ[R] L) → Nₚ J →ₗ[R] Lₚ J) G))
    (range.{u_1, u_1, u_6, u_7} (R := R) (M := Mₚ J) (τ₁₂ := RingHom.id R)
      ((IsLocalizedModule.map J.primeCompl (f J) (g J) : (a : M →ₗ[R] N) → Mₚ J →ₗ[R] Nₚ J) F))
have this : ∀ (x : Nₚ J),
  Membership.mem (γ := Submodule R (Nₚ J))
      (ker.{u_1, u_1, u_7, u_8} (R₂ := R) (M₂ := Lₚ J) (τ₁₂ := RingHom.id R)
        ((IsLocalizedModule.map J.primeCompl (g J) (h J) : (a : N →ₗ[R] L) → Nₚ J →ₗ[R] Lₚ J) G))
      x ↔
    Membership.mem (γ := Submodule R (Nₚ J))
      (range.{u_1, u_1, u_6, u_7} (R := R) (M := Mₚ J) (τ₁₂ := RingHom.id R)
        ((IsLocalizedModule.map J.primeCompl (f J) (g J) : (a : M →ₗ[R] N) → Mₚ J →ₗ[R] Nₚ J) F))
      x
Tactic: have := SetLike.ext_iff.mp <| H J