awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Exactness (goal)
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)
    (⇑((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)
have 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)
Tactic: rw [map_linearCombination]
-- 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
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)
⊢ 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 :
    ∀ (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
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
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))
⊢ G.ker = F.range
have apply : ∀ (r : (↑s : Type u_1)),
  localized₀ (Submonoid.powers (↑r : R)) (g r) G.ker = localized₀ (Submonoid.powers (↑r : R)) (g r) F.range
Tactic: apply Submodule.eq_of_isLocalized₀_span s spn 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
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)
⊢ localized₀ (Submonoid.powers (↑r : R)) (g r) G.ker = localized₀ (Submonoid.powers (↑r : R)) (g r) F.range
have 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)
Tactic: rw [← LinearMap.range_localizedMap_eq_localized₀_range _ (f r) (g r) F]
-- 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
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)
⊢ 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)
have 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))
Tactic: rw [← LinearMap.ker_localizedMap_eq_localized₀_ker (.powers r.1) (g r) (h r) 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
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)
⊢ 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))
have this : ∀ (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
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Exactness (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
Rₚ : Type u_5
Sₚ : Type u_6
inst_3 : CommSemiring Rₚ
inst_4 : Algebra R Rₚ
inst_5 : CommSemiring Sₚ
inst_6 : Algebra S Sₚ
inst_7 : Algebra R Sₚ
inst_8 : IsScalarTower R S Sₚ
inst_9 : Algebra Rₚ Sₚ
inst_10 : IsScalarTower R Rₚ Sₚ
p : Ideal R
inst_11 : p.IsPrime
inst_12 : IsLocalization.AtPrime Rₚ p
inst_13 :
  IsLocalizedModule.AtPrime.{u_1, u_2, u_6} (M := S) (M' := Sₚ) p
    (↑(IsScalarTower.toAlgHom R S Sₚ) :
      [inst_14 : FunLike (S →ₐ[R] Sₚ) S Sₚ] → [SemilinearMapClass (S →ₐ[R] Sₚ) (RingHom.id R) S Sₚ] → S →ₗ[R] Sₚ)
⊢ Eq (α := Rₚ →ₗ[R] Sₚ)
    ((map p.primeCompl (Algebra.linearMap R Rₚ)
            (↑(IsScalarTower.toAlgHom R S Sₚ) :
              [inst_14 : FunLike (S →ₐ[R] Sₚ) S Sₚ] →
                [SemilinearMapClass (S →ₐ[R] Sₚ) (RingHom.id R) S Sₚ] → S →ₗ[R] Sₚ) :
          (a : R →ₗ[R] S) → Rₚ →ₗ[R] Sₚ)
        (Algebra.linearMap R S) :
      Rₚ →ₗ[R] Sₚ)
    ((↑R :
          {S M : Type u_5} →
            {M₂ : Type u_6} →
              [inst : Semiring R] →
                [inst_14 : Semiring S] →
                  [inst_15 : AddCommMonoid M] →
                    [inst_16 : AddCommMonoid M₂] →
                      [inst_17 : Module R M] →
                        [inst_18 : Module R M₂] →
                          [inst_19 : Module S M] →
                            [inst_20 : Module S M₂] →
                              [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        (Algebra.linearMap Rₚ Sₚ) :
      Rₚ →ₗ[R] Sₚ)
have h : Eq (α := R →ₗ[R] Sₚ)
  ((map p.primeCompl (Algebra.linearMap R Rₚ)
          (↑(IsScalarTower.toAlgHom R S Sₚ) :
            [inst_14 : FunLike (S →ₐ[R] Sₚ) S Sₚ] →
              [SemilinearMapClass (S →ₐ[R] Sₚ) (RingHom.id R) S Sₚ] → S →ₗ[R] Sₚ) :
        (a : R →ₗ[R] S) → Rₚ →ₗ[R] Sₚ)
      (Algebra.linearMap R S) ∘ₗ
    Algebra.linearMap R Rₚ)
  ((↑R :
        {S M : Type u_5} →
          {M₂ : Type u_6} →
            [inst : Semiring R] →
              [inst_14 : Semiring S] →
                [inst_15 : AddCommMonoid M] →
                  [inst_16 : AddCommMonoid M₂] →
                    [inst_17 : Module R M] →
                      [inst_18 : Module R M₂] →
                        [inst_19 : Module S M] →
                          [inst_20 : Module S M₂] →
                            [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      (Algebra.linearMap Rₚ Sₚ) ∘ₗ
    Algebra.linearMap R Rₚ)
Tactic: apply IsLocalizedModule.linearMap_ext p.primeCompl (Algebra.linearMap _ _)
    (IsScalarTower.toAlgHom R S Sₚ : S →ₗ[R] Sₚ)
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Exactness (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
Rₚ : Type u_5
Sₚ : Type u_6
inst_3 : CommSemiring Rₚ
inst_4 : Algebra R Rₚ
inst_5 : CommSemiring Sₚ
inst_6 : Algebra S Sₚ
inst_7 : Algebra R Sₚ
inst_8 : IsScalarTower R S Sₚ
inst_9 : Algebra Rₚ Sₚ
inst_10 : IsScalarTower R Rₚ Sₚ
p : Ideal R
inst_11 : p.IsPrime
inst_12 : IsLocalization.AtPrime Rₚ p
inst_13 :
  IsLocalizedModule.AtPrime.{u_1, u_2, u_6} (M := S) (M' := Sₚ) p
    (↑(IsScalarTower.toAlgHom R S Sₚ) :
      [inst_14 : FunLike (S →ₐ[R] Sₚ) S Sₚ] → [SemilinearMapClass (S →ₐ[R] Sₚ) (RingHom.id R) S Sₚ] → S →ₗ[R] Sₚ)
⊢ Eq (α := R →ₗ[R] Sₚ)
    ((map p.primeCompl (Algebra.linearMap R Rₚ)
            (↑(IsScalarTower.toAlgHom R S Sₚ) :
              [inst_14 : FunLike (S →ₐ[R] Sₚ) S Sₚ] →
                [SemilinearMapClass (S →ₐ[R] Sₚ) (RingHom.id R) S Sₚ] → S →ₗ[R] Sₚ) :
          (a : R →ₗ[R] S) → Rₚ →ₗ[R] Sₚ)
        (Algebra.linearMap R S) ∘ₗ
      Algebra.linearMap R Rₚ)
    ((↑R :
          {S M : Type u_5} →
            {M₂ : Type u_6} →
              [inst : Semiring R] →
                [inst_14 : Semiring S] →
                  [inst_15 : AddCommMonoid M] →
                    [inst_16 : AddCommMonoid M₂] →
                      [inst_17 : Module R M] →
                        [inst_18 : Module R M₂] →
                          [inst_19 : Module S M] →
                            [inst_20 : Module S M₂] →
                              [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        (Algebra.linearMap Rₚ Sₚ) ∘ₗ
      Algebra.linearMap R Rₚ)
have h : Eq.{u_6 + 1} (α := Sₚ)
  (((map p.primeCompl (Algebra.linearMap R Rₚ)
                (↑(IsScalarTower.toAlgHom R S Sₚ) :
                  [inst_14 : FunLike (S →ₐ[R] Sₚ) S Sₚ] →
                    [SemilinearMapClass (S →ₐ[R] Sₚ) (RingHom.id R) S Sₚ] → S →ₗ[R] Sₚ) :
              (a : R →ₗ[R] S) → Rₚ →ₗ[R] Sₚ)
            (Algebra.linearMap R S) ∘ₗ
          Algebra.linearMap R Rₚ :
        (a : R) → Sₚ)
      1 :
    Sₚ)
  (((↑R :
              {S M : Type u_5} →
                {M₂ : Type u_6} →
                  [inst : Semiring R] →
                    [inst_14 : Semiring S] →
                      [inst_15 : AddCommMonoid M] →
                        [inst_16 : AddCommMonoid M₂] →
                          [inst_17 : Module R M] →
                            [inst_18 : Module R M₂] →
                              [inst_19 : Module S M] →
                                [inst_20 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            (Algebra.linearMap Rₚ Sₚ) ∘ₗ
          Algebra.linearMap R Rₚ :
        (a : R) → Sₚ)
      1 :
    Sₚ)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Exactness (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
Rₚ : Type u_5
Sₚ : Type u_6
inst_3 : CommSemiring Rₚ
inst_4 : Algebra R Rₚ
inst_5 : CommSemiring Sₚ
inst_6 : Algebra S Sₚ
inst_7 : Algebra R Sₚ
inst_8 : IsScalarTower R S Sₚ
inst_9 : Algebra Rₚ Sₚ
inst_10 : IsScalarTower R Rₚ Sₚ
p : Ideal R
inst_11 : p.IsPrime
inst_12 : IsLocalization.AtPrime Rₚ p
inst_13 :
  IsLocalizedModule.AtPrime.{u_1, u_2, u_6} (M := S) (M' := Sₚ) p
    (↑(IsScalarTower.toAlgHom R S Sₚ) :
      [inst_14 : FunLike (S →ₐ[R] Sₚ) S Sₚ] → [SemilinearMapClass (S →ₐ[R] Sₚ) (RingHom.id R) S Sₚ] → S →ₗ[R] Sₚ)
⊢ Eq.{u_6 + 1} (α := Sₚ)
    (((map p.primeCompl (Algebra.linearMap R Rₚ)
                  (↑(IsScalarTower.toAlgHom R S Sₚ) :
                    [inst_14 : FunLike (S →ₐ[R] Sₚ) S Sₚ] →
                      [SemilinearMapClass (S →ₐ[R] Sₚ) (RingHom.id R) S Sₚ] → S →ₗ[R] Sₚ) :
                (a : R →ₗ[R] S) → Rₚ →ₗ[R] Sₚ)
              (Algebra.linearMap R S) ∘ₗ
            Algebra.linearMap R Rₚ :
          (a : R) → Sₚ)
        1 :
      Sₚ)
    (((↑R :
                {S M : Type u_5} →
                  {M₂ : Type u_6} →
                    [inst : Semiring R] →
                      [inst_14 : Semiring S] →
                        [inst_15 : AddCommMonoid M] →
                          [inst_16 : AddCommMonoid M₂] →
                            [inst_17 : Module R M] →
                              [inst_18 : Module R M₂] →
                                [inst_19 : Module S M] →
                                  [inst_20 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
              (Algebra.linearMap Rₚ Sₚ) ∘ₗ
            Algebra.linearMap R Rₚ :
          (a : R) → Sₚ)
        1 :
      Sₚ)
have h : Eq.{u_6 + 1} (α := Sₚ)
  ((((map p.primeCompl (Algebra.linearMap R Rₚ)
                (↑(IsScalarTower.toAlgHom R S Sₚ) :
                  [inst_14 : FunLike (S →ₐ[R] Sₚ) S Sₚ] →
                    [SemilinearMapClass (S →ₐ[R] Sₚ) (RingHom.id R) S Sₚ] → S →ₗ[R] Sₚ) :
              (a : R →ₗ[R] S) → Rₚ →ₗ[R] Sₚ)
            (Algebra.linearMap R S) :
          Rₚ →ₗ[R] Sₚ) :
        (a : Rₚ) → Sₚ)
      1 :
    Sₚ)
  (1 : Sₚ)
Tactic: simp only [LinearMap.coe_comp, Function.comp_apply, Algebra.linearMap_apply, map_one,
    LinearMap.coe_restrictScalars]
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Exactness (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
Rₚ : Type u_5
Sₚ : Type u_6
inst_3 : CommSemiring Rₚ
inst_4 : Algebra R Rₚ
inst_5 : CommSemiring Sₚ
inst_6 : Algebra S Sₚ
inst_7 : Algebra R Sₚ
inst_8 : IsScalarTower R S Sₚ
inst_9 : Algebra Rₚ Sₚ
inst_10 : IsScalarTower R Rₚ Sₚ
p : Ideal R
inst_11 : p.IsPrime
inst_12 : IsLocalization.AtPrime Rₚ p
inst_13 :
  IsLocalizedModule.AtPrime.{u_1, u_2, u_6} (M := S) (M' := Sₚ) p
    (↑(IsScalarTower.toAlgHom R S Sₚ) :
      [inst_14 : FunLike (S →ₐ[R] Sₚ) S Sₚ] → [SemilinearMapClass (S →ₐ[R] Sₚ) (RingHom.id R) S Sₚ] → S →ₗ[R] Sₚ)
⊢ Eq.{u_6 + 1} (α := Sₚ)
    ((((map p.primeCompl (Algebra.linearMap R Rₚ)
                  (↑(IsScalarTower.toAlgHom R S Sₚ) :
                    [inst_14 : FunLike (S →ₐ[R] Sₚ) S Sₚ] →
                      [SemilinearMapClass (S →ₐ[R] Sₚ) (RingHom.id R) S Sₚ] → S →ₗ[R] Sₚ) :
                (a : R →ₗ[R] S) → Rₚ →ₗ[R] Sₚ)
              (Algebra.linearMap R S) :
            Rₚ →ₗ[R] Sₚ) :
          (a : Rₚ) → Sₚ)
        1 :
      Sₚ)
    (1 : Sₚ)
have h : Eq.{u_6 + 1} (α := Sₚ)
  (((↑(IsScalarTower.toAlgHom R S Sₚ) :
          [inst_14 : FunLike (S →ₐ[R] Sₚ) S Sₚ] → [SemilinearMapClass (S →ₐ[R] Sₚ) (RingHom.id R) S Sₚ] → S →ₗ[R] Sₚ) :
        (a : S) → Sₚ)
      ((Algebra.linearMap R S : (a : R) → S) 1 : S) :
    Sₚ)
  (1 : Sₚ)
Tactic: rw [show 1 = Algebra.linearMap R Rₚ 1 by simp, IsLocalizedModule.map_apply]