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

Tactic:
exact this x
-- 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) ⊤
f : M →ₗ[R] N
h :
  ∀ (r : (↑s : Type u_1)),
    Function.Injective (α := LocalizedModule (Submonoid.powers (↑r : R)) M) (β :=
      LocalizedModule (Submonoid.powers (↑r : R)) N)
      (⇑((LocalizedModule.map (Submonoid.powers (↑r : R)) :
                (a : M →ₗ[R] N) →
                  LocalizedModule (Submonoid.powers (↑r : R)) M →ₗ[Localization (Submonoid.powers (↑r : R))]
                    LocalizedModule (Submonoid.powers (↑r : R)) N)
              f :
            LinearMap (R := Localization (Submonoid.powers (↑r : R)))
              (RingHom.id (Localization (Submonoid.powers (↑r : R)))) (LocalizedModule (Submonoid.powers (↑r : R)) M)
              (LocalizedModule (Submonoid.powers (↑r : R)) N)) :
        (a : LocalizedModule (Submonoid.powers (↑r : R)) M) → LocalizedModule (Submonoid.powers (↑r : R)) N)
⊢ Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑f : (a : M) → N)

Tactic:
injective_of_isLocalized_span s spn _ (fun _ ↦ mkLinearMap _ _) _ (fun _ ↦ mkLinearMap _ _) f h

Premises used: LocalizedModule.mkLinearMap, injective_of_isLocalized_span
-- 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) ⊤
f : M →ₗ[R] N
h :
  ∀ (r : (↑s : Type u_1)),
    Function.Surjective (α := LocalizedModule (Submonoid.powers (↑r : R)) M) (β :=
      LocalizedModule (Submonoid.powers (↑r : R)) N)
      (⇑((LocalizedModule.map (Submonoid.powers (↑r : R)) :
                (a : M →ₗ[R] N) →
                  LocalizedModule (Submonoid.powers (↑r : R)) M →ₗ[Localization (Submonoid.powers (↑r : R))]
                    LocalizedModule (Submonoid.powers (↑r : R)) N)
              f :
            LinearMap (R := Localization (Submonoid.powers (↑r : R)))
              (RingHom.id (Localization (Submonoid.powers (↑r : R)))) (LocalizedModule (Submonoid.powers (↑r : R)) M)
              (LocalizedModule (Submonoid.powers (↑r : R)) N)) :
        (a : LocalizedModule (Submonoid.powers (↑r : R)) M) → LocalizedModule (Submonoid.powers (↑r : R)) N)
⊢ Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑f : (a : M) → N)

Tactic:
surjective_of_isLocalized_span s spn _ (fun _ ↦ mkLinearMap _ _) _ (fun _ ↦ mkLinearMap _ _) f h

Premises used: surjective_of_isLocalized_span, 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) ⊤
f : M →ₗ[R] N
h :
  ∀ (r : (↑s : Type u_1)),
    Function.Bijective (α := LocalizedModule (Submonoid.powers (↑r : R)) M) (β :=
      LocalizedModule (Submonoid.powers (↑r : R)) N)
      (⇑((LocalizedModule.map (Submonoid.powers (↑r : R)) :
                (a : M →ₗ[R] N) →
                  LocalizedModule (Submonoid.powers (↑r : R)) M →ₗ[Localization (Submonoid.powers (↑r : R))]
                    LocalizedModule (Submonoid.powers (↑r : R)) N)
              f :
            LinearMap (R := Localization (Submonoid.powers (↑r : R)))
              (RingHom.id (Localization (Submonoid.powers (↑r : R)))) (LocalizedModule (Submonoid.powers (↑r : R)) M)
              (LocalizedModule (Submonoid.powers (↑r : R)) N)) :
        (a : LocalizedModule (Submonoid.powers (↑r : R)) M) → LocalizedModule (Submonoid.powers (↑r : R)) N)
⊢ Function.Bijective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑f : (a : M) → N)

Tactic:
⟨injective_of_localized_span _ spn _ fun r ↦ (h r).1,
  surjective_of_localized_span _ spn _ fun r ↦ (h r).2⟩

Premises used: surjective_of_localized_span, And.right, And.left, And.intro, Function.Bijective, injective_of_localized_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) ⊤
f : M →ₗ[R] N
g : N →ₗ[R] L
h :
  ∀ (r : (↑s : Type u_1)),
    Function.Exact (M := LocalizedModule (Submonoid.powers (↑r : R)) M) (N :=
      LocalizedModule (Submonoid.powers (↑r : R)) N) (P := LocalizedModule (Submonoid.powers (↑r : R)) L)
      (⇑((LocalizedModule.map (Submonoid.powers (↑r : R)) :
                (a : M →ₗ[R] N) →
                  LocalizedModule (Submonoid.powers (↑r : R)) M →ₗ[Localization (Submonoid.powers (↑r : R))]
                    LocalizedModule (Submonoid.powers (↑r : R)) N)
              f :
            LinearMap (R := Localization (Submonoid.powers (↑r : R)))
              (RingHom.id (Localization (Submonoid.powers (↑r : R)))) (LocalizedModule (Submonoid.powers (↑r : R)) M)
              (LocalizedModule (Submonoid.powers (↑r : R)) N)) :
        (a : LocalizedModule (Submonoid.powers (↑r : R)) M) → LocalizedModule (Submonoid.powers (↑r : R)) N)
      (⇑((LocalizedModule.map (Submonoid.powers (↑r : R)) :
                (a : N →ₗ[R] L) →
                  LocalizedModule (Submonoid.powers (↑r : R)) N →ₗ[Localization (Submonoid.powers (↑r : R))]
                    LocalizedModule (Submonoid.powers (↑r : R)) L)
              g :
            LinearMap (R := Localization (Submonoid.powers (↑r : R)))
              (RingHom.id (Localization (Submonoid.powers (↑r : R)))) (LocalizedModule (Submonoid.powers (↑r : R)) N)
              (LocalizedModule (Submonoid.powers (↑r : R)) L)) :
        (a : LocalizedModule (Submonoid.powers (↑r : R)) N) → LocalizedModule (Submonoid.powers (↑r : R)) 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_span s spn _ (fun _ ↦ mkLinearMap _ _) _ (fun _ ↦ mkLinearMap _ _)
    _ (fun _ ↦ mkLinearMap _ _) f g h

Premises used: exact_of_isLocalized_span, LocalizedModule.mkLinearMap
-- Module: Mathlib.RingTheory.LocalProperties.Exactness
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ₚ)
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ₚ)
⊢ 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ₚ)

Tactic:
apply IsLocalizedModule.linearMap_ext p.primeCompl (Algebra.linearMap _ _)
    (IsScalarTower.toAlgHom R S Sₚ : S →ₗ[R] Sₚ)

Premises used: IsLocalizedModule.linearMap_ext, IsScalarTower.toAlgHom, Algebra.linearMap, SemilinearMapClass.semilinearMap, Ideal.primeCompl
-- Module: Mathlib.RingTheory.LocalProperties.Exactness
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ₚ)
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ₚ)
⊢ 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:
ext
-- Module: Mathlib.RingTheory.LocalProperties.Exactness
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ₚ)
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ₚ)
⊢ 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:
simp only [LinearMap.coe_comp, Function.comp_apply, Algebra.linearMap_apply, map_one,
    LinearMap.coe_restrictScalars]

Premises used: LinearMap.coe_restrictScalars, Algebra.linearMap_apply, LinearMap.coe_comp, map_one, Function.comp_apply
-- Module: Mathlib.RingTheory.LocalProperties.Exactness
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_5 + 1} (α := Rₚ) (1 : Rₚ) ((Algebra.linearMap R Rₚ : (a : R) → Rₚ) 1 : Rₚ)

Tactic:
simp