awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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)
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
⊢ 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
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))
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)
⊢ G.ker = F.range

Tactic:
apply eq_of_localization₀_maximal Nₚ g

Premises used: Submodule.eq_of_localization₀_maximal
-- 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
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
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))
⊢ Eq (α := Submodule R (Nₚ J)) (localized₀ J.primeCompl (g J) G.ker) (localized₀ J.primeCompl (g J) F.range)

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]

Premises used: LinearMap.ker_localizedMap_eq_localized₀_ker, Ideal.primeCompl, 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
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
⊢ ∀ (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
-- 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
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
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
x : Nₚ J
⊢ ∀ (x : Nₚ J),
    Eq.{u_8 + 1} (α := Lₚ 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)
            x :
          Lₚ J)
        (0 : Lₚ J) ↔
      ∃ (y : Mₚ 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)
            y =
          x

Tactic:
simp only [mem_range, mem_ker] at this ⊢

Premises used: LinearMap.mem_ker, LinearMap.mem_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
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
x : Nₚ J
this :
  ∀ (x : Nₚ J),
    Eq.{u_8 + 1} (α := Lₚ 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)
            x :
          Lₚ J)
        (0 : Lₚ J) ↔
      ∃ (y : Mₚ 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)
            y =
          x
⊢ Eq.{u_8 + 1} (α := Lₚ 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)
          x :
        Lₚ J)
      (0 : Lₚ J) ↔
    ∃ (y : Mₚ 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)
          y =
        x

Tactic:
this x
-- 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
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
x : Nₚ J
this :
  ∀ (x : Nₚ J),
    Eq.{u_8 + 1} (α := Lₚ 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)
            x :
          Lₚ J)
        (0 : Lₚ J) ↔
      ∃ (y : Mₚ 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)
            y =
          x
⊢ Eq.{u_8 + 1} (α := Lₚ 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)
          x :
        Lₚ J)
      (0 : Lₚ J) ↔
    ∃ (y : Mₚ 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)
          y =
        x

Tactic:
exact this x
-- 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
rw :
  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)
⊢ Function.Injective (α := Finsupp.{u_9, u_5} ι (Rₚ P)) (β := Mₚ P)
    (⇑((IsLocalizedModule.map P.primeCompl
                ((fun (P : Ideal R) (x : P.IsMaximal) ↦
                    (Finsupp.mapRange.linearMap (Algebra.linearMap R (Rₚ P)) :
                      (ι →₀ R) →ₗ[R] Finsupp.{u_9, u_5} ι (Rₚ P)))
                  P h)
                (f P) :
              (a : (ι →₀ R) →ₗ[R] M) → (ι →₀ Rₚ P) →ₗ[R] Mₚ P)
            (Finsupp.linearCombination R v) :
          Finsupp.{u_9, u_5} ι (Rₚ P) →ₗ[R] Mₚ P) :
      (a : ι →₀ Rₚ P) → Mₚ P)

Tactic:
rw [map_linearCombination]

Premises used: IsLocalizedModule.map_linearCombination
-- 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:
H P

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, LinearIndependent, Finset.sum