awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.LocalProperties.Exactness
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_5
inst_3 : (P : Ideal R) → [inst : P.IsMaximal] → CommSemiring (Rₚ P)
inst_4 : (P : Ideal R) → [inst_11 : P.IsMaximal] → Algebra.{u_1, u_5} R (Rₚ P)
inst_5 : ∀ (P : Ideal R) [inst_11 : P.IsMaximal], IsLocalization.AtPrime.{u_1, u_5} (Rₚ P) P
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_6
inst_6 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst_7 : (P : Ideal R) → [inst_11 : P.IsMaximal] → Module.{u_1, u_6} R (Mₚ P)
inst_8 : (P : Ideal R) → [inst : P.IsMaximal] → Module.{u_5, u_6} (Rₚ P) (Mₚ P)
inst_9 : ∀ (P : Ideal R) [inst_11 : P.IsMaximal], IsScalarTower.{u_1, u_5, u_6} R (Rₚ P) (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_10 : ∀ (P : Ideal R) [inst_11 : P.IsMaximal], IsLocalizedModule.AtPrime (M' := Mₚ P) P (f P)
ι : Type u_9
v : ι → M
H :
  ∀ (P : Ideal R) [inst_11 : P.IsMaximal],
    LinearIndependent.{u_9, u_5, u_6} (Rₚ P) (M := Mₚ P) ((⇑(f P) : (a : M) → Mₚ P) ∘ v)
P : Ideal R
h : P.IsMaximal
⊢ Function.Injective (α := Finsupp.{u_9, u_5} ι (Rₚ P)) (β := Mₚ P)
    (⇑((↑R :
            {S : Type u_5} →
              {M : Type (max u_5 u_9)} →
                {M₂ : Type u_6} →
                  [inst : Semiring R] →
                    [inst_11 : Semiring S] →
                      [inst_12 : AddCommMonoid M] →
                        [inst_13 : AddCommMonoid M₂] →
                          [inst_14 : Module R M] →
                            [inst_15 : Module R M₂] →
                              [inst_16 : Module S M] →
                                [inst_17 : Module S M₂] → [CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
          (Finsupp.linearCombination (Rₚ P) ((⇑(f P) : (a : M) → Mₚ P) ∘ v))) :
      (a : ι →₀ Rₚ P) → Mₚ P)

Tactic:
exact H P
-- 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
f : M →ₗ[R] N
h :
  ∀ (J : Ideal R) [inst_5 : J.IsMaximal],
    Function.Injective (α := LocalizedModule J.primeCompl M) (β := LocalizedModule J.primeCompl N)
      (⇑((LocalizedModule.map J.primeCompl :
                (a : M →ₗ[R] N) →
                  LocalizedModule J.primeCompl M →ₗ[Localization J.primeCompl] LocalizedModule J.primeCompl N)
              f :
            LinearMap (R := Localization (M := R) J.primeCompl) (RingHom.id (Localization (M := R) J.primeCompl))
              (LocalizedModule J.primeCompl M) (LocalizedModule J.primeCompl N)) :
        (a : LocalizedModule J.primeCompl M) → LocalizedModule J.primeCompl N)
⊢ Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑f : (a : M) → N)

Tactic:
injective_of_isLocalized_maximal _ (fun _ _ ↦ mkLinearMap _ _) _ (fun _ _ ↦ mkLinearMap _ _) f h

Premises used: injective_of_isLocalized_maximal, LocalizedModule.mkLinearMap
-- 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
f : M →ₗ[R] N
h :
  ∀ (J : Ideal R) [inst_5 : J.IsMaximal],
    Function.Surjective (α := LocalizedModule J.primeCompl M) (β := LocalizedModule J.primeCompl N)
      (⇑((LocalizedModule.map J.primeCompl :
                (a : M →ₗ[R] N) →
                  LocalizedModule J.primeCompl M →ₗ[Localization J.primeCompl] LocalizedModule J.primeCompl N)
              f :
            LinearMap (R := Localization (M := R) J.primeCompl) (RingHom.id (Localization (M := R) J.primeCompl))
              (LocalizedModule J.primeCompl M) (LocalizedModule J.primeCompl N)) :
        (a : LocalizedModule J.primeCompl M) → LocalizedModule J.primeCompl N)
⊢ Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑f : (a : M) → N)

Tactic:
surjective_of_isLocalized_maximal _ (fun _ _ ↦ mkLinearMap _ _) _ (fun _ _ ↦ mkLinearMap _ _) f h

Premises used: surjective_of_isLocalized_maximal, LocalizedModule.mkLinearMap
-- 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
f : M →ₗ[R] N
h :
  ∀ (J : Ideal R) [inst_5 : J.IsMaximal],
    Function.Bijective (α := LocalizedModule J.primeCompl M) (β := LocalizedModule J.primeCompl N)
      (⇑((LocalizedModule.map J.primeCompl :
                (a : M →ₗ[R] N) →
                  LocalizedModule J.primeCompl M →ₗ[Localization J.primeCompl] LocalizedModule J.primeCompl N)
              f :
            LinearMap (R := Localization (M := R) J.primeCompl) (RingHom.id (Localization (M := R) J.primeCompl))
              (LocalizedModule J.primeCompl M) (LocalizedModule J.primeCompl N)) :
        (a : LocalizedModule J.primeCompl M) → LocalizedModule J.primeCompl N)
⊢ Function.Bijective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑f : (a : M) → N)

Tactic:
⟨injective_of_localized_maximal _ fun J _ ↦ (h J).1,
  surjective_of_localized_maximal _ fun J _ ↦ (h J).2⟩

Premises used: injective_of_localized_maximal, And.right, And.left, And.intro, surjective_of_localized_maximal, Function.Bijective
-- Module: Mathlib.RingTheory.LocalProperties.Exactness
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
f : M →ₗ[R] N
g : N →ₗ[R] L
h :
  ∀ (J : Ideal R) [inst_7 : J.IsMaximal],
    Function.Exact (M := LocalizedModule J.primeCompl M) (N := LocalizedModule J.primeCompl N) (P :=
      LocalizedModule J.primeCompl L)
      (⇑((LocalizedModule.map J.primeCompl :
                (a : M →ₗ[R] N) →
                  LocalizedModule J.primeCompl M →ₗ[Localization J.primeCompl] LocalizedModule J.primeCompl N)
              f :
            LinearMap (R := Localization (M := R) J.primeCompl) (RingHom.id (Localization (M := R) J.primeCompl))
              (LocalizedModule J.primeCompl M) (LocalizedModule J.primeCompl N)) :
        (a : LocalizedModule J.primeCompl M) → LocalizedModule J.primeCompl N)
      (⇑((LocalizedModule.map J.primeCompl :
                (a : N →ₗ[R] L) →
                  LocalizedModule J.primeCompl N →ₗ[Localization J.primeCompl] LocalizedModule J.primeCompl L)
              g :
            LinearMap (R := Localization (M := R) J.primeCompl) (RingHom.id (Localization (M := R) J.primeCompl))
              (LocalizedModule J.primeCompl N) (LocalizedModule J.primeCompl L)) :
        (a : LocalizedModule J.primeCompl N) → LocalizedModule J.primeCompl L)
⊢ Function.Exact.{u_2, u_3, u_4} (M := M) (N := N) (P := L) (⇑f : (a : M) → N) (⇑g : (a : N) → L)

Tactic:
exact_of_isLocalized_maximal _ (fun _ _ ↦ mkLinearMap _ _) _ (fun _ _ ↦ mkLinearMap _ _)
    _ (fun _ _ ↦ mkLinearMap _ _) f g h

Premises used: exact_of_isLocalized_maximal, LocalizedModule.mkLinearMap
-- 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
s : Set R
spn : Eq (α := Ideal R) (Ideal.span s) ⊤
Mₚ : (↑s : Type u_1) → Type u_5
inst_5 : (r : (↑s : Type u_1)) → AddCommMonoid (Mₚ r)
inst_6 : (r : (↑s : Type u_1)) → Module.{u_1, u_5} R (Mₚ r)
f : (r : (↑s : Type u_1)) → LinearMap.{u_1, u_1, u_2, u_5} (RingHom.id R) M (Mₚ r)
inst_7 : ∀ (r : (↑s : Type u_1)), IsLocalizedModule.Away (↑r : R) (f r)
Nₚ : (↑s : Type u_1) → Type u_6
inst_8 : (r : (↑s : Type u_1)) → AddCommMonoid (Nₚ r)
inst_9 : (r : (↑s : Type u_1)) → Module.{u_1, u_6} R (Nₚ r)
g : (r : (↑s : Type u_1)) → LinearMap.{u_1, u_1, u_3, u_6} (RingHom.id R) N (Nₚ r)
inst_10 : ∀ (r : (↑s : Type u_1)), IsLocalizedModule.Away (↑r : R) (g r)
F : M →ₗ[R] N
H :
  ∀ (r : (↑s : Type u_1)),
    Function.Injective.{u_5 + 1, u_6 + 1} (α := Mₚ r) (β := Nₚ r)
      (⇑((IsLocalizedModule.map (Submonoid.powers (↑r : R)) (f r) (g r) : (a : M →ₗ[R] N) → Mₚ r →ₗ[R] Nₚ r) F :
            LinearMap.{u_1, u_1, u_5, u_6} (RingHom.id R) (Mₚ r) (Nₚ r)) :
        (a : Mₚ r) → Nₚ r)
x y : M
eq : Eq.{u_3 + 1} (α := N) ((F : (a : M) → N) x : N) ((F : (a : M) → N) y : N)
P : (↑s : Type u_1)
⊢ Eq.{u_6 + 1} (α := Nₚ P)
    ((((IsLocalizedModule.map (Submonoid.powers (↑P : R)) (f P) (g P) : (a : M →ₗ[R] N) → Mₚ P →ₗ[R] Nₚ P) F :
            LinearMap.{u_1, u_1, u_5, u_6} (RingHom.id R) (Mₚ P) (Nₚ P)) :
          (a : Mₚ P) → Nₚ P)
        ((f P : (a : M) → Mₚ P) x) :
      Nₚ P)
    ((((IsLocalizedModule.map (Submonoid.powers (↑P : R)) (f P) (g P) : (a : M →ₗ[R] N) → Mₚ P →ₗ[R] Nₚ P) F :
            LinearMap.{u_1, u_1, u_5, u_6} (RingHom.id R) (Mₚ P) (Nₚ P)) :
          (a : Mₚ P) → Nₚ P)
        ((f P : (a : M) → Mₚ P) y) :
      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
s : Set R
spn : Eq (α := Ideal R) (Ideal.span s) ⊤
Mₚ : (↑s : Type u_1) → Type u_5
inst_5 : (r : (↑s : Type u_1)) → AddCommMonoid (Mₚ r)
inst_6 : (r : (↑s : Type u_1)) → Module.{u_1, u_5} R (Mₚ r)
f : (r : (↑s : Type u_1)) → LinearMap.{u_1, u_1, u_2, u_5} (RingHom.id R) M (Mₚ r)
inst_7 : ∀ (r : (↑s : Type u_1)), IsLocalizedModule.Away (↑r : R) (f r)
Nₚ : (↑s : Type u_1) → Type u_6
inst_8 : (r : (↑s : Type u_1)) → AddCommMonoid (Nₚ r)
inst_9 : (r : (↑s : Type u_1)) → Module.{u_1, u_6} R (Nₚ r)
g : (r : (↑s : Type u_1)) → LinearMap.{u_1, u_1, u_3, u_6} (RingHom.id R) N (Nₚ r)
inst_10 : ∀ (r : (↑s : Type u_1)), IsLocalizedModule.Away (↑r : R) (g r)
F : M →ₗ[R] N
H :
  ∀ (r : (↑s : Type u_1)),
    Function.Surjective.{u_5 + 1, u_6 + 1} (α := Mₚ r) (β := Nₚ r)
      (⇑((IsLocalizedModule.map (Submonoid.powers (↑r : R)) (f r) (g r) : (a : M →ₗ[R] N) → Mₚ r →ₗ[R] Nₚ r) F :
            LinearMap.{u_1, u_1, u_5, u_6} (RingHom.id R) (Mₚ r) (Nₚ r)) :
        (a : Mₚ r) → Nₚ r)
⊢ Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑F : (a : M) → N)

Tactic:
range_eq_top.mp <| eq_top_of_isLocalized₀_span s spn Nₚ g fun r ↦
    (range_localizedMap_eq_localized₀_range _ (f r) (g r) F).symm.trans <| range_eq_top.mpr <| H r

Premises used: Iff.mpr, Submodule.eq_top_of_isLocalized₀_span, LinearMap.range_eq_top, Submonoid.powers, Iff.mp, Eq.symm, Subtype.val, 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
s : Set R
spn : Eq (α := Ideal R) (Ideal.span s) ⊤
Mₚ : (↑s : Type u_1) → Type u_5
inst_5 : (r : (↑s : Type u_1)) → AddCommMonoid (Mₚ r)
inst_6 : (r : (↑s : Type u_1)) → Module.{u_1, u_5} R (Mₚ r)
f : (r : (↑s : Type u_1)) → LinearMap.{u_1, u_1, u_2, u_5} (RingHom.id R) M (Mₚ r)
inst_7 : ∀ (r : (↑s : Type u_1)), IsLocalizedModule.Away (↑r : R) (f r)
Nₚ : (↑s : Type u_1) → Type u_6
inst_8 : (r : (↑s : Type u_1)) → AddCommMonoid (Nₚ r)
inst_9 : (r : (↑s : Type u_1)) → Module.{u_1, u_6} R (Nₚ r)
g : (r : (↑s : Type u_1)) → LinearMap.{u_1, u_1, u_3, u_6} (RingHom.id R) N (Nₚ r)
inst_10 : ∀ (r : (↑s : Type u_1)), IsLocalizedModule.Away (↑r : R) (g r)
F : M →ₗ[R] N
H :
  ∀ (r : (↑s : Type u_1)),
    Function.Bijective.{u_5 + 1, u_6 + 1} (α := Mₚ r) (β := Nₚ r)
      (⇑((IsLocalizedModule.map (Submonoid.powers (↑r : R)) (f r) (g r) : (a : M →ₗ[R] N) → Mₚ r →ₗ[R] Nₚ r) F :
            LinearMap.{u_1, u_1, u_5, u_6} (RingHom.id R) (Mₚ r) (Nₚ r)) :
        (a : Mₚ r) → Nₚ r)
⊢ Function.Bijective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑F : (a : M) → N)

Tactic:
⟨injective_of_isLocalized_span _ spn Mₚ f Nₚ g F fun r ↦ (H r).1,
  surjective_of_isLocalized_span _ spn Mₚ f Nₚ g F fun r ↦ (H r).2⟩

Premises used: surjective_of_isLocalized_span, And.right, And.left, And.intro, Function.Bijective, injective_of_isLocalized_span
-- Module: Mathlib.RingTheory.LocalProperties.Exactness
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
s : Set R
spn : Eq (α := Ideal R) (Ideal.span s) ⊤
Mₚ : (↑s : Type u_1) → Type u_5
inst_7 : (r : (↑s : Type u_1)) → AddCommMonoid (Mₚ r)
inst_8 : (r : (↑s : Type u_1)) → Module.{u_1, u_5} R (Mₚ r)
f : (r : (↑s : Type u_1)) → LinearMap.{u_1, u_1, u_2, u_5} (RingHom.id R) M (Mₚ r)
inst_9 : ∀ (r : (↑s : Type u_1)), IsLocalizedModule.Away (↑r : R) (f r)
Nₚ : (↑s : Type u_1) → Type u_6
inst_10 : (r : (↑s : Type u_1)) → AddCommMonoid (Nₚ r)
inst_11 : (r : (↑s : Type u_1)) → Module.{u_1, u_6} R (Nₚ r)
g : (r : (↑s : Type u_1)) → LinearMap.{u_1, u_1, u_3, u_6} (RingHom.id R) N (Nₚ r)
inst_12 : ∀ (r : (↑s : Type u_1)), IsLocalizedModule.Away (↑r : R) (g r)
Lₚ : (↑s : Type u_1) → Type u_7
inst_13 : (r : (↑s : Type u_1)) → AddCommMonoid (Lₚ r)
inst_14 : (r : (↑s : Type u_1)) → Module.{u_1, u_7} R (Lₚ r)
h : (r : (↑s : Type u_1)) → LinearMap.{u_1, u_1, u_4, u_7} (RingHom.id R) L (Lₚ r)
inst_15 : ∀ (r : (↑s : Type u_1)), IsLocalizedModule.Away (↑r : R) (h r)
F : M →ₗ[R] N
G : N →ₗ[R] L
H :
  ∀ (r : (↑s : Type u_1)),
    Function.Exact.{u_5, u_6, u_7} (M := Mₚ r) (N := Nₚ r) (P := Lₚ r)
      (⇑((IsLocalizedModule.map (Submonoid.powers (↑r : R)) (f r) (g r) : (a : M →ₗ[R] N) → Mₚ r →ₗ[R] Nₚ r) F :
            LinearMap.{u_1, u_1, u_5, u_6} (RingHom.id R) (Mₚ r) (Nₚ r)) :
        (a : Mₚ r) → Nₚ r)
      (⇑((IsLocalizedModule.map (Submonoid.powers (↑r : R)) (g r) (h r) : (a : N →ₗ[R] L) → Nₚ r →ₗ[R] Lₚ r) G :
            LinearMap.{u_1, u_1, u_6, u_7} (RingHom.id R) (Nₚ r) (Lₚ r)) :
        (a : Nₚ r) → Lₚ r)
simp :
  ∀
    (H :
      ∀ (r : (↑s : Type u_1)),
        Eq.{u_6 + 1} (α := Submodule R (Nₚ r))
          (ker.{u_1, u_1, u_6, u_7} (R₂ := R) (M₂ := Lₚ r) (τ₁₂ := RingHom.id R)
            ((IsLocalizedModule.map (Submonoid.powers (↑r : R)) (g r) (h r) : (a : N →ₗ[R] L) → Nₚ r →ₗ[R] Lₚ r) G))
          (range.{u_1, u_1, u_5, u_6} (R := R) (M := Mₚ r) (τ₁₂ := RingHom.id R)
            ((IsLocalizedModule.map (Submonoid.powers (↑r : R)) (f r) (g r) : (a : M →ₗ[R] N) → Mₚ r →ₗ[R] Nₚ r) F))),
    G.ker = F.range
⊢ Function.Exact.{u_2, u_3, u_4} (M := M) (N := N) (P := L) (⇑F : (a : M) → N) (⇑G : (a : N) → L)

Tactic:
simp only [LinearMap.exact_iff] at H ⊢

Premises used: LinearMap.exact_iff
-- Module: Mathlib.RingTheory.LocalProperties.Exactness
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
s : Set R
spn : Eq (α := Ideal R) (Ideal.span s) ⊤
Mₚ : (↑s : Type u_1) → Type u_5
inst_7 : (r : (↑s : Type u_1)) → AddCommMonoid (Mₚ r)
inst_8 : (r : (↑s : Type u_1)) → Module.{u_1, u_5} R (Mₚ r)
f : (r : (↑s : Type u_1)) → LinearMap.{u_1, u_1, u_2, u_5} (RingHom.id R) M (Mₚ r)
inst_9 : ∀ (r : (↑s : Type u_1)), IsLocalizedModule.Away (↑r : R) (f r)
Nₚ : (↑s : Type u_1) → Type u_6
inst_10 : (r : (↑s : Type u_1)) → AddCommMonoid (Nₚ r)
inst_11 : (r : (↑s : Type u_1)) → Module.{u_1, u_6} R (Nₚ r)
g : (r : (↑s : Type u_1)) → LinearMap.{u_1, u_1, u_3, u_6} (RingHom.id R) N (Nₚ r)
inst_12 : ∀ (r : (↑s : Type u_1)), IsLocalizedModule.Away (↑r : R) (g r)
Lₚ : (↑s : Type u_1) → Type u_7
inst_13 : (r : (↑s : Type u_1)) → AddCommMonoid (Lₚ r)
inst_14 : (r : (↑s : Type u_1)) → Module.{u_1, u_7} R (Lₚ r)
h : (r : (↑s : Type u_1)) → LinearMap.{u_1, u_1, u_4, u_7} (RingHom.id R) L (Lₚ r)
inst_15 : ∀ (r : (↑s : Type u_1)), IsLocalizedModule.Away (↑r : R) (h r)
F : M →ₗ[R] N
G : N →ₗ[R] L
H :
  ∀ (r : (↑s : Type u_1)),
    Eq.{u_6 + 1} (α := Submodule R (Nₚ r))
      (ker.{u_1, u_1, u_6, u_7} (R₂ := R) (M₂ := Lₚ r) (τ₁₂ := RingHom.id R)
        ((IsLocalizedModule.map (Submonoid.powers (↑r : R)) (g r) (h r) : (a : N →ₗ[R] L) → Nₚ r →ₗ[R] Lₚ r) G))
      (range.{u_1, u_1, u_5, u_6} (R := R) (M := Mₚ r) (τ₁₂ := RingHom.id R)
        ((IsLocalizedModule.map (Submonoid.powers (↑r : R)) (f r) (g r) : (a : M →ₗ[R] N) → Mₚ r →ₗ[R] Nₚ r) F))
apply :
  ∀ (r : (↑s : Type u_1)),
    localized₀ (Submonoid.powers (↑r : R)) (g r) G.ker = localized₀ (Submonoid.powers (↑r : R)) (g r) F.range
⊢ G.ker = F.range

Tactic:
apply Submodule.eq_of_isLocalized₀_span s spn Nₚ g

Premises used: Submodule.eq_of_isLocalized₀_span
-- Module: Mathlib.RingTheory.LocalProperties.Exactness
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
s : Set R
spn : Eq (α := Ideal R) (Ideal.span s) ⊤
Mₚ : (↑s : Type u_1) → Type u_5
inst_7 : (r : (↑s : Type u_1)) → AddCommMonoid (Mₚ r)
inst_8 : (r : (↑s : Type u_1)) → Module.{u_1, u_5} R (Mₚ r)
f : (r : (↑s : Type u_1)) → LinearMap.{u_1, u_1, u_2, u_5} (RingHom.id R) M (Mₚ r)
inst_9 : ∀ (r : (↑s : Type u_1)), IsLocalizedModule.Away (↑r : R) (f r)
Nₚ : (↑s : Type u_1) → Type u_6
inst_10 : (r : (↑s : Type u_1)) → AddCommMonoid (Nₚ r)
inst_11 : (r : (↑s : Type u_1)) → Module.{u_1, u_6} R (Nₚ r)
g : (r : (↑s : Type u_1)) → LinearMap.{u_1, u_1, u_3, u_6} (RingHom.id R) N (Nₚ r)
inst_12 : ∀ (r : (↑s : Type u_1)), IsLocalizedModule.Away (↑r : R) (g r)
Lₚ : (↑s : Type u_1) → Type u_7
inst_13 : (r : (↑s : Type u_1)) → AddCommMonoid (Lₚ r)
inst_14 : (r : (↑s : Type u_1)) → Module.{u_1, u_7} R (Lₚ r)
h : (r : (↑s : Type u_1)) → LinearMap.{u_1, u_1, u_4, u_7} (RingHom.id R) L (Lₚ r)
inst_15 : ∀ (r : (↑s : Type u_1)), IsLocalizedModule.Away (↑r : R) (h r)
F : M →ₗ[R] N
G : N →ₗ[R] L
H :
  ∀ (r : (↑s : Type u_1)),
    Eq.{u_6 + 1} (α := Submodule R (Nₚ r))
      (ker.{u_1, u_1, u_6, u_7} (R₂ := R) (M₂ := Lₚ r) (τ₁₂ := RingHom.id R)
        ((IsLocalizedModule.map (Submonoid.powers (↑r : R)) (g r) (h r) : (a : N →ₗ[R] L) → Nₚ r →ₗ[R] Lₚ r) G))
      (range.{u_1, u_1, u_5, u_6} (R := R) (M := Mₚ r) (τ₁₂ := RingHom.id R)
        ((IsLocalizedModule.map (Submonoid.powers (↑r : R)) (f r) (g r) : (a : M →ₗ[R] N) → Mₚ r →ₗ[R] Nₚ r) F))
r : (↑s : Type u_1)
rw :
  localized₀ (Submonoid.powers (↑r : R)) (g r) G.ker =
    range.{u_1, u_1, u_5, u_6} (R := R) (M := Mₚ r) (τ₁₂ := RingHom.id R)
      ((IsLocalizedModule.map (Submonoid.powers (↑r : R)) (f r) (g r) : (a : M →ₗ[R] N) → Mₚ r →ₗ[R] Nₚ r) F)
⊢ localized₀ (Submonoid.powers (↑r : R)) (g r) G.ker = localized₀ (Submonoid.powers (↑r : R)) (g r) F.range

Tactic:
rw [← LinearMap.range_localizedMap_eq_localized₀_range _ (f r) (g r) F]

Premises used: LinearMap.range_localizedMap_eq_localized₀_range
-- Module: Mathlib.RingTheory.LocalProperties.Exactness
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
s : Set R
spn : Eq (α := Ideal R) (Ideal.span s) ⊤
Mₚ : (↑s : Type u_1) → Type u_5
inst_7 : (r : (↑s : Type u_1)) → AddCommMonoid (Mₚ r)
inst_8 : (r : (↑s : Type u_1)) → Module.{u_1, u_5} R (Mₚ r)
f : (r : (↑s : Type u_1)) → LinearMap.{u_1, u_1, u_2, u_5} (RingHom.id R) M (Mₚ r)
inst_9 : ∀ (r : (↑s : Type u_1)), IsLocalizedModule.Away (↑r : R) (f r)
Nₚ : (↑s : Type u_1) → Type u_6
inst_10 : (r : (↑s : Type u_1)) → AddCommMonoid (Nₚ r)
inst_11 : (r : (↑s : Type u_1)) → Module.{u_1, u_6} R (Nₚ r)
g : (r : (↑s : Type u_1)) → LinearMap.{u_1, u_1, u_3, u_6} (RingHom.id R) N (Nₚ r)
inst_12 : ∀ (r : (↑s : Type u_1)), IsLocalizedModule.Away (↑r : R) (g r)
Lₚ : (↑s : Type u_1) → Type u_7
inst_13 : (r : (↑s : Type u_1)) → AddCommMonoid (Lₚ r)
inst_14 : (r : (↑s : Type u_1)) → Module.{u_1, u_7} R (Lₚ r)
h : (r : (↑s : Type u_1)) → LinearMap.{u_1, u_1, u_4, u_7} (RingHom.id R) L (Lₚ r)
inst_15 : ∀ (r : (↑s : Type u_1)), IsLocalizedModule.Away (↑r : R) (h r)
F : M →ₗ[R] N
G : N →ₗ[R] L
H :
  ∀ (r : (↑s : Type u_1)),
    Eq.{u_6 + 1} (α := Submodule R (Nₚ r))
      (ker.{u_1, u_1, u_6, u_7} (R₂ := R) (M₂ := Lₚ r) (τ₁₂ := RingHom.id R)
        ((IsLocalizedModule.map (Submonoid.powers (↑r : R)) (g r) (h r) : (a : N →ₗ[R] L) → Nₚ r →ₗ[R] Lₚ r) G))
      (range.{u_1, u_1, u_5, u_6} (R := R) (M := Mₚ r) (τ₁₂ := RingHom.id R)
        ((IsLocalizedModule.map (Submonoid.powers (↑r : R)) (f r) (g r) : (a : M →ₗ[R] N) → Mₚ r →ₗ[R] Nₚ r) F))
r : (↑s : Type u_1)
rw :
  Eq.{u_6 + 1} (α := Submodule R (Nₚ r))
    (ker.{u_1, u_1, u_6, u_7} (R₂ := R) (M₂ := Lₚ r) (τ₁₂ := RingHom.id R)
      ((IsLocalizedModule.map (Submonoid.powers (↑r : R)) (g r) (h r) : (a : N →ₗ[R] L) → Nₚ r →ₗ[R] Lₚ r) G))
    (range.{u_1, u_1, u_5, u_6} (R := R) (M := Mₚ r) (τ₁₂ := RingHom.id R)
      ((IsLocalizedModule.map (Submonoid.powers (↑r : R)) (f r) (g r) : (a : M →ₗ[R] N) → Mₚ r →ₗ[R] Nₚ r) F))
⊢ localized₀ (Submonoid.powers (↑r : R)) (g r) G.ker =
    range.{u_1, u_1, u_5, u_6} (R := R) (M := Mₚ r) (τ₁₂ := RingHom.id R)
      ((IsLocalizedModule.map (Submonoid.powers (↑r : R)) (f r) (g r) : (a : M →ₗ[R] N) → Mₚ r →ₗ[R] Nₚ r) F)

Tactic:
rw [← LinearMap.ker_localizedMap_eq_localized₀_ker (.powers r.1) (g r) (h r) G]

Premises used: LinearMap.ker_localizedMap_eq_localized₀_ker, Submonoid.powers, Subtype.val
-- Module: Mathlib.RingTheory.LocalProperties.Exactness
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
s : Set R
spn : Eq (α := Ideal R) (Ideal.span s) ⊤
Mₚ : (↑s : Type u_1) → Type u_5
inst_7 : (r : (↑s : Type u_1)) → AddCommMonoid (Mₚ r)
inst_8 : (r : (↑s : Type u_1)) → Module.{u_1, u_5} R (Mₚ r)
f : (r : (↑s : Type u_1)) → LinearMap.{u_1, u_1, u_2, u_5} (RingHom.id R) M (Mₚ r)
inst_9 : ∀ (r : (↑s : Type u_1)), IsLocalizedModule.Away (↑r : R) (f r)
Nₚ : (↑s : Type u_1) → Type u_6
inst_10 : (r : (↑s : Type u_1)) → AddCommMonoid (Nₚ r)
inst_11 : (r : (↑s : Type u_1)) → Module.{u_1, u_6} R (Nₚ r)
g : (r : (↑s : Type u_1)) → LinearMap.{u_1, u_1, u_3, u_6} (RingHom.id R) N (Nₚ r)
inst_12 : ∀ (r : (↑s : Type u_1)), IsLocalizedModule.Away (↑r : R) (g r)
Lₚ : (↑s : Type u_1) → Type u_7
inst_13 : (r : (↑s : Type u_1)) → AddCommMonoid (Lₚ r)
inst_14 : (r : (↑s : Type u_1)) → Module.{u_1, u_7} R (Lₚ r)
h : (r : (↑s : Type u_1)) → LinearMap.{u_1, u_1, u_4, u_7} (RingHom.id R) L (Lₚ r)
inst_15 : ∀ (r : (↑s : Type u_1)), IsLocalizedModule.Away (↑r : R) (h r)
F : M →ₗ[R] N
G : N →ₗ[R] L
H :
  ∀ (r : (↑s : Type u_1)),
    Eq.{u_6 + 1} (α := Submodule R (Nₚ r))
      (ker.{u_1, u_1, u_6, u_7} (R₂ := R) (M₂ := Lₚ r) (τ₁₂ := RingHom.id R)
        ((IsLocalizedModule.map (Submonoid.powers (↑r : R)) (g r) (h r) : (a : N →ₗ[R] L) → Nₚ r →ₗ[R] Lₚ r) G))
      (range.{u_1, u_1, u_5, u_6} (R := R) (M := Mₚ r) (τ₁₂ := RingHom.id R)
        ((IsLocalizedModule.map (Submonoid.powers (↑r : R)) (f r) (g r) : (a : M →ₗ[R] N) → Mₚ r →ₗ[R] Nₚ r) F))
r : (↑s : Type u_1)
⊢ ∀ (x : Nₚ r),
    Membership.mem (γ := Submodule R (Nₚ r))
        (ker.{u_1, u_1, u_6, u_7} (R₂ := R) (M₂ := Lₚ r) (τ₁₂ := RingHom.id R)
          ((IsLocalizedModule.map (Submonoid.powers (↑r : R)) (g r) (h r) : (a : N →ₗ[R] L) → Nₚ r →ₗ[R] Lₚ r) G))
        x ↔
      Membership.mem (γ := Submodule R (Nₚ r))
        (range.{u_1, u_1, u_5, u_6} (R := R) (M := Mₚ r) (τ₁₂ := RingHom.id R)
          ((IsLocalizedModule.map (Submonoid.powers (↑r : R)) (f r) (g r) : (a : M →ₗ[R] N) → Mₚ r →ₗ[R] Nₚ r) F))
        x

Tactic:
have := SetLike.ext_iff.mp <| H r