awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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ₚ)
    (((↑(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ₚ)
⊢ 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:
rw [show 1 = Algebra.linearMap R Rₚ 1 by simp, IsLocalizedModule.map_apply]

Premises used: IsLocalizedModule.map_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_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:
simp
-- 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ₚ : (p : Ideal R) → [p.IsMaximal] → Type u_3
inst_3 : (p : Ideal R) → [inst : p.IsMaximal] → CommSemiring (Rₚ p)
inst_4 : (p : Ideal R) → [inst_13 : p.IsMaximal] → Algebra.{u_1, u_3} R (Rₚ p)
Sₚ : (p : Ideal R) → [p.IsMaximal] → Type u_4
inst_5 : (p : Ideal R) → [inst : p.IsMaximal] → CommSemiring (Sₚ p)
inst_6 : (p : Ideal R) → [inst : p.IsMaximal] → Algebra.{u_2, u_4} S (Sₚ p)
inst_7 : (p : Ideal R) → [inst : p.IsMaximal] → Algebra.{u_3, u_4} (Rₚ p) (Sₚ p)
inst_8 : (p : Ideal R) → [inst_13 : p.IsMaximal] → Algebra.{u_1, u_4} R (Sₚ p)
inst_9 : ∀ (p : Ideal R) [inst_13 : p.IsMaximal], IsScalarTower.{u_1, u_3, u_4} R (Rₚ p) (Sₚ p)
inst_10 : ∀ (p : Ideal R) [inst_13 : p.IsMaximal], IsScalarTower.{u_1, u_2, u_4} R S (Sₚ p)
inst_11 : ∀ (p : Ideal R) [inst_13 : p.IsMaximal], IsLocalization.AtPrime.{u_1, u_3} (Rₚ p) p
inst_12 :
  ∀ (p : Ideal R) [inst_13 : p.IsMaximal],
    IsLocalizedModule.AtPrime.{u_1, u_2, u_4} (M := S) (M' := Sₚ p) p
      (↑(IsScalarTower.toAlgHom R S (Sₚ p)) :
        [inst_14 : FunLike (S →ₐ[R] Sₚ p) S (Sₚ p)] →
          [SemilinearMapClass (S →ₐ[R] Sₚ p) (RingHom.id R) S (Sₚ p)] → S →ₗ[R] Sₚ p)
H :
  ∀ (p : Ideal R) [inst : p.IsMaximal],
    Function.Injective.{u_3 + 1, u_4 + 1} (α := Rₚ p) (β := Sₚ p) (⇑(algebraMap (Rₚ p) (Sₚ p)) : (a : Rₚ p) → Sₚ p)
p : Ideal R
hp : p.IsMaximal
⊢ Function.Injective.{u_3 + 1, u_4 + 1} (α := Rₚ p) (β := Sₚ p)
    (⇑((↑R :
            {S M : Type u_3} →
              {M₂ : Type u_4} →
                [inst : Semiring R] →
                  [inst_13 : Semiring S] →
                    [inst_14 : AddCommMonoid M] →
                      [inst_15 : AddCommMonoid M₂] →
                        [inst_16 : Module R M] →
                          [inst_17 : Module R M₂] →
                            [inst_18 : Module S M] →
                              [inst_19 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
          (Algebra.linearMap (Rₚ p) (Sₚ p))) :
      (a : Rₚ p) → Sₚ p)

Tactic:
H p
-- 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ₚ : (p : Ideal R) → [p.IsMaximal] → Type u_3
inst_3 : (p : Ideal R) → [inst : p.IsMaximal] → CommSemiring (Rₚ p)
inst_4 : (p : Ideal R) → [inst_13 : p.IsMaximal] → Algebra.{u_1, u_3} R (Rₚ p)
Sₚ : (p : Ideal R) → [p.IsMaximal] → Type u_4
inst_5 : (p : Ideal R) → [inst : p.IsMaximal] → CommSemiring (Sₚ p)
inst_6 : (p : Ideal R) → [inst : p.IsMaximal] → Algebra.{u_2, u_4} S (Sₚ p)
inst_7 : (p : Ideal R) → [inst : p.IsMaximal] → Algebra.{u_3, u_4} (Rₚ p) (Sₚ p)
inst_8 : (p : Ideal R) → [inst_13 : p.IsMaximal] → Algebra.{u_1, u_4} R (Sₚ p)
inst_9 : ∀ (p : Ideal R) [inst_13 : p.IsMaximal], IsScalarTower.{u_1, u_3, u_4} R (Rₚ p) (Sₚ p)
inst_10 : ∀ (p : Ideal R) [inst_13 : p.IsMaximal], IsScalarTower.{u_1, u_2, u_4} R S (Sₚ p)
inst_11 : ∀ (p : Ideal R) [inst_13 : p.IsMaximal], IsLocalization.AtPrime.{u_1, u_3} (Rₚ p) p
inst_12 :
  ∀ (p : Ideal R) [inst_13 : p.IsMaximal],
    IsLocalizedModule.AtPrime.{u_1, u_2, u_4} (M := S) (M' := Sₚ p) p
      (↑(IsScalarTower.toAlgHom R S (Sₚ p)) :
        [inst_14 : FunLike (S →ₐ[R] Sₚ p) S (Sₚ p)] →
          [SemilinearMapClass (S →ₐ[R] Sₚ p) (RingHom.id R) S (Sₚ p)] → S →ₗ[R] Sₚ p)
H :
  ∀ (p : Ideal R) [inst : p.IsMaximal],
    Function.Injective.{u_3 + 1, u_4 + 1} (α := Rₚ p) (β := Sₚ p) (⇑(algebraMap (Rₚ p) (Sₚ p)) : (a : Rₚ p) → Sₚ p)
p : Ideal R
hp : p.IsMaximal
⊢ Function.Injective.{u_3 + 1, u_4 + 1} (α := Rₚ p) (β := Sₚ p)
    (⇑((↑R :
            {S M : Type u_3} →
              {M₂ : Type u_4} →
                [inst : Semiring R] →
                  [inst_13 : Semiring S] →
                    [inst_14 : AddCommMonoid M] →
                      [inst_15 : AddCommMonoid M₂] →
                        [inst_16 : Module R M] →
                          [inst_17 : Module R M₂] →
                            [inst_18 : Module S M] →
                              [inst_19 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
          (Algebra.linearMap (Rₚ p) (Sₚ p))) :
      (a : Rₚ p) → Sₚ p)

Tactic:
exact H p
-- 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ₚ : (p : Ideal R) → [p.IsMaximal] → Type u_3
inst_3 : (p : Ideal R) → [inst : p.IsMaximal] → CommSemiring (Rₚ p)
inst_4 : (p : Ideal R) → [inst_13 : p.IsMaximal] → Algebra.{u_1, u_3} R (Rₚ p)
Sₚ : (p : Ideal R) → [p.IsMaximal] → Type u_4
inst_5 : (p : Ideal R) → [inst : p.IsMaximal] → CommSemiring (Sₚ p)
inst_6 : (p : Ideal R) → [inst : p.IsMaximal] → Algebra.{u_2, u_4} S (Sₚ p)
inst_7 : (p : Ideal R) → [inst : p.IsMaximal] → Algebra.{u_3, u_4} (Rₚ p) (Sₚ p)
inst_8 : (p : Ideal R) → [inst_13 : p.IsMaximal] → Algebra.{u_1, u_4} R (Sₚ p)
inst_9 : ∀ (p : Ideal R) [inst_13 : p.IsMaximal], IsScalarTower.{u_1, u_3, u_4} R (Rₚ p) (Sₚ p)
inst_10 : ∀ (p : Ideal R) [inst_13 : p.IsMaximal], IsScalarTower.{u_1, u_2, u_4} R S (Sₚ p)
inst_11 : ∀ (p : Ideal R) [inst_13 : p.IsMaximal], IsLocalization.AtPrime.{u_1, u_3} (Rₚ p) p
inst_12 :
  ∀ (p : Ideal R) [inst_13 : p.IsMaximal],
    IsLocalizedModule.AtPrime.{u_1, u_2, u_4} (M := S) (M' := Sₚ p) p
      (↑(IsScalarTower.toAlgHom R S (Sₚ p)) :
        [inst_14 : FunLike (S →ₐ[R] Sₚ p) S (Sₚ p)] →
          [SemilinearMapClass (S →ₐ[R] Sₚ p) (RingHom.id R) S (Sₚ p)] → S →ₗ[R] Sₚ p)
H :
  ∀ (p : Ideal R) [inst : p.IsMaximal],
    Function.Surjective.{u_3 + 1, u_4 + 1} (α := Rₚ p) (β := Sₚ p) (⇑(algebraMap (Rₚ p) (Sₚ p)) : (a : Rₚ p) → Sₚ p)
p : Ideal R
hp : p.IsMaximal
⊢ Function.Surjective.{u_3 + 1, u_4 + 1} (α := Rₚ p) (β := Sₚ p)
    (⇑((↑R :
            {S M : Type u_3} →
              {M₂ : Type u_4} →
                [inst : Semiring R] →
                  [inst_13 : Semiring S] →
                    [inst_14 : AddCommMonoid M] →
                      [inst_15 : AddCommMonoid M₂] →
                        [inst_16 : Module R M] →
                          [inst_17 : Module R M₂] →
                            [inst_18 : Module S M] →
                              [inst_19 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
          (Algebra.linearMap (Rₚ p) (Sₚ p))) :
      (a : Rₚ p) → Sₚ p)

Tactic:
H p
-- 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ₚ : (p : Ideal R) → [p.IsMaximal] → Type u_3
inst_3 : (p : Ideal R) → [inst : p.IsMaximal] → CommSemiring (Rₚ p)
inst_4 : (p : Ideal R) → [inst_13 : p.IsMaximal] → Algebra.{u_1, u_3} R (Rₚ p)
Sₚ : (p : Ideal R) → [p.IsMaximal] → Type u_4
inst_5 : (p : Ideal R) → [inst : p.IsMaximal] → CommSemiring (Sₚ p)
inst_6 : (p : Ideal R) → [inst : p.IsMaximal] → Algebra.{u_2, u_4} S (Sₚ p)
inst_7 : (p : Ideal R) → [inst : p.IsMaximal] → Algebra.{u_3, u_4} (Rₚ p) (Sₚ p)
inst_8 : (p : Ideal R) → [inst_13 : p.IsMaximal] → Algebra.{u_1, u_4} R (Sₚ p)
inst_9 : ∀ (p : Ideal R) [inst_13 : p.IsMaximal], IsScalarTower.{u_1, u_3, u_4} R (Rₚ p) (Sₚ p)
inst_10 : ∀ (p : Ideal R) [inst_13 : p.IsMaximal], IsScalarTower.{u_1, u_2, u_4} R S (Sₚ p)
inst_11 : ∀ (p : Ideal R) [inst_13 : p.IsMaximal], IsLocalization.AtPrime.{u_1, u_3} (Rₚ p) p
inst_12 :
  ∀ (p : Ideal R) [inst_13 : p.IsMaximal],
    IsLocalizedModule.AtPrime.{u_1, u_2, u_4} (M := S) (M' := Sₚ p) p
      (↑(IsScalarTower.toAlgHom R S (Sₚ p)) :
        [inst_14 : FunLike (S →ₐ[R] Sₚ p) S (Sₚ p)] →
          [SemilinearMapClass (S →ₐ[R] Sₚ p) (RingHom.id R) S (Sₚ p)] → S →ₗ[R] Sₚ p)
H :
  ∀ (p : Ideal R) [inst : p.IsMaximal],
    Function.Surjective.{u_3 + 1, u_4 + 1} (α := Rₚ p) (β := Sₚ p) (⇑(algebraMap (Rₚ p) (Sₚ p)) : (a : Rₚ p) → Sₚ p)
p : Ideal R
hp : p.IsMaximal
⊢ Function.Surjective.{u_3 + 1, u_4 + 1} (α := Rₚ p) (β := Sₚ p)
    (⇑((↑R :
            {S M : Type u_3} →
              {M₂ : Type u_4} →
                [inst : Semiring R] →
                  [inst_13 : Semiring S] →
                    [inst_14 : AddCommMonoid M] →
                      [inst_15 : AddCommMonoid M₂] →
                        [inst_16 : Module R M] →
                          [inst_17 : Module R M₂] →
                            [inst_18 : Module S M] →
                              [inst_19 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
          (Algebra.linearMap (Rₚ p) (Sₚ p))) :
      (a : Rₚ p) → Sₚ p)

Tactic:
exact H p
-- 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ₚ : (p : Ideal R) → [p.IsMaximal] → Type u_3
inst_3 : (p : Ideal R) → [inst : p.IsMaximal] → CommSemiring (Rₚ p)
inst_4 : (p : Ideal R) → [inst_13 : p.IsMaximal] → Algebra.{u_1, u_3} R (Rₚ p)
Sₚ : (p : Ideal R) → [p.IsMaximal] → Type u_4
inst_5 : (p : Ideal R) → [inst : p.IsMaximal] → CommSemiring (Sₚ p)
inst_6 : (p : Ideal R) → [inst : p.IsMaximal] → Algebra.{u_2, u_4} S (Sₚ p)
inst_7 : (p : Ideal R) → [inst : p.IsMaximal] → Algebra.{u_3, u_4} (Rₚ p) (Sₚ p)
inst_8 : (p : Ideal R) → [inst_13 : p.IsMaximal] → Algebra.{u_1, u_4} R (Sₚ p)
inst_9 : ∀ (p : Ideal R) [inst_13 : p.IsMaximal], IsScalarTower.{u_1, u_3, u_4} R (Rₚ p) (Sₚ p)
inst_10 : ∀ (p : Ideal R) [inst_13 : p.IsMaximal], IsScalarTower.{u_1, u_2, u_4} R S (Sₚ p)
inst_11 : ∀ (p : Ideal R) [inst_13 : p.IsMaximal], IsLocalization.AtPrime.{u_1, u_3} (Rₚ p) p
inst_12 :
  ∀ (p : Ideal R) [inst_13 : p.IsMaximal],
    IsLocalizedModule.AtPrime.{u_1, u_2, u_4} (M := S) (M' := Sₚ p) p
      (↑(IsScalarTower.toAlgHom R S (Sₚ p)) :
        [inst_14 : FunLike (S →ₐ[R] Sₚ p) S (Sₚ p)] →
          [SemilinearMapClass (S →ₐ[R] Sₚ p) (RingHom.id R) S (Sₚ p)] → S →ₗ[R] Sₚ p)
H :
  ∀ (p : Ideal R) [inst : p.IsMaximal],
    Function.Bijective.{u_3 + 1, u_4 + 1} (α := Rₚ p) (β := Sₚ p) (⇑(algebraMap (Rₚ p) (Sₚ p)) : (a : Rₚ p) → Sₚ p)
⊢ Function.Bijective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)

Tactic:
⟨injective_of_isLocalization_isMaximal _ _ (fun p _ ↦ (H p).1),
    surjective_of_isLocalization_isMaximal _ _ (fun p _ ↦ (H p).2)⟩

Premises used: injective_of_isLocalization_isMaximal, surjective_of_isLocalization_isMaximal, And.right, And.left, And.intro, Function.Bijective
-- Module: Mathlib.RingTheory.LocalProperties.Exactness
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
s : Set R
hs : Eq (α := Ideal R) (Ideal.span s) ⊤
Rᵣ : (↑s : Type u_1) → Type u_3
inst_2 : (r : (↑s : Type u_1)) → CommSemiring (Rᵣ r)
inst_3 : (r : (↑s : Type u_1)) → Algebra.{u_1, u_3} R (Rᵣ r)
Sᵣ : (↑s : Type u_1) → Type u_4
inst_4 : (r : (↑s : Type u_1)) → CommSemiring (Sᵣ r)
inst_5 : (r : (↑s : Type u_1)) → Algebra.{u_2, u_4} S (Sᵣ r)
f : R →+* S
inst_6 : ∀ (r : (↑s : Type u_1)), IsLocalization.Away.{u_1, u_3} (↑r : R) (Rᵣ r)
inst_7 : ∀ (r : (↑s : Type u_1)), IsLocalization.Away.{u_2, u_4} (R := S) ((f : (a : R) → S) (↑r : R) : S) (Sᵣ r)
h :
  ∀ (r : (↑s : Type u_1)),
    Function.Injective.{u_3 + 1, u_4 + 1} (α := Rᵣ r) (β := Sᵣ r)
      (⇑(IsLocalization.Away.map (Rᵣ r) (Sᵣ r) f (↑r : R)) : (a : Rᵣ r) → Sᵣ r)
algInst : Algebra R S := f.toAlgebra
this : (r : (↑s : Type u_1)) → Algebra.{u_1, u_4} R (Sᵣ r) :=
  fun (r : (↑s : Type u_1)) ↦ RingHom.toAlgebra (RingHom.comp (algebraMap S (Sᵣ r)) f)
⊢ ∀ (r : (↑s : Type u_1)), IsScalarTower.{u_1, u_2, u_4} R S (Sᵣ r)

Tactic:
have (r : s) : IsScalarTower R S (Sᵣ r) := IsScalarTower.of_algebraMap_eq' rfl
-- Module: Mathlib.RingTheory.LocalProperties.Exactness
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
s : Set R
hs : Eq (α := Ideal R) (Ideal.span s) ⊤
Rᵣ : (↑s : Type u_1) → Type u_3
inst_2 : (r : (↑s : Type u_1)) → CommSemiring (Rᵣ r)
inst_3 : (r : (↑s : Type u_1)) → Algebra.{u_1, u_3} R (Rᵣ r)
Sᵣ : (↑s : Type u_1) → Type u_4
inst_4 : (r : (↑s : Type u_1)) → CommSemiring (Sᵣ r)
inst_5 : (r : (↑s : Type u_1)) → Algebra.{u_2, u_4} S (Sᵣ r)
f : R →+* S
inst_6 : ∀ (r : (↑s : Type u_1)), IsLocalization.Away.{u_1, u_3} (↑r : R) (Rᵣ r)
inst_7 : ∀ (r : (↑s : Type u_1)), IsLocalization.Away.{u_2, u_4} (R := S) ((f : (a : R) → S) (↑r : R) : S) (Sᵣ r)
h :
  ∀ (r : (↑s : Type u_1)),
    Function.Injective.{u_3 + 1, u_4 + 1} (α := Rᵣ r) (β := Sᵣ r)
      (⇑(IsLocalization.Away.map (Rᵣ r) (Sᵣ r) f (↑r : R)) : (a : Rᵣ r) → Sᵣ r)
algInst : Algebra R S := f.toAlgebra
this_1 : (r : (↑s : Type u_1)) → Algebra.{u_1, u_4} R (Sᵣ r) :=
  fun (r : (↑s : Type u_1)) ↦ RingHom.toAlgebra (RingHom.comp (algebraMap S (Sᵣ r)) f)
this : ∀ (r : (↑s : Type u_1)), IsScalarTower.{u_1, u_2, u_4} R S (Sᵣ r)
⊢ ∀ (r : (↑s : Type u_1)), IsLocalization.Away.{u_2, u_4} (R := S) ((algebraMap R S : (a : R) → S) (↑r : R) : S) (Sᵣ r)

Tactic:
have : ∀ r, IsLocalization.Away (algebraMap R S r.val) (Sᵣ r) := ‹_›
-- Module: Mathlib.RingTheory.LocalProperties.Exactness
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
s : Set R
hs : Eq (α := Ideal R) (Ideal.span s) ⊤
Rᵣ : (↑s : Type u_1) → Type u_3
inst_2 : (r : (↑s : Type u_1)) → CommSemiring (Rᵣ r)
inst_3 : (r : (↑s : Type u_1)) → Algebra.{u_1, u_3} R (Rᵣ r)
Sᵣ : (↑s : Type u_1) → Type u_4
inst_4 : (r : (↑s : Type u_1)) → CommSemiring (Sᵣ r)
inst_5 : (r : (↑s : Type u_1)) → Algebra.{u_2, u_4} S (Sᵣ r)
f : R →+* S
inst_6 : ∀ (r : (↑s : Type u_1)), IsLocalization.Away.{u_1, u_3} (↑r : R) (Rᵣ r)
inst_7 : ∀ (r : (↑s : Type u_1)), IsLocalization.Away.{u_2, u_4} (R := S) ((f : (a : R) → S) (↑r : R) : S) (Sᵣ r)
h :
  ∀ (r : (↑s : Type u_1)),
    Function.Injective.{u_3 + 1, u_4 + 1} (α := Rᵣ r) (β := Sᵣ r)
      (⇑(IsLocalization.Away.map (Rᵣ r) (Sᵣ r) f (↑r : R)) : (a : Rᵣ r) → Sᵣ r)
algInst : Algebra R S := f.toAlgebra
this_1 : (r : (↑s : Type u_1)) → Algebra.{u_1, u_4} R (Sᵣ r) :=
  fun (r : (↑s : Type u_1)) ↦ RingHom.toAlgebra (RingHom.comp (algebraMap S (Sᵣ r)) f)
this_2 : ∀ (r : (↑s : Type u_1)), IsScalarTower.{u_1, u_2, u_4} R S (Sᵣ r)
this_3 :
  ∀ (r : (↑s : Type u_1)), IsLocalization.Away.{u_2, u_4} (R := S) ((algebraMap R S : (a : R) → S) (↑r : R) : S) (Sᵣ r)
this : (r : (↑s : Type u_1)) → Algebra.{u_3, u_4} (Rᵣ r) (Sᵣ r) :=
  fun (r : (↑s : Type u_1)) ↦ localizationAlgebra (Submonoid.powers (↑r : R)) S
r : (↑s : Type u_1)
⊢ ∀ (x : R),
    Eq.{u_4 + 1} (α := Sᵣ r) ((algebraMap R (Sᵣ r) : (a : R) → Sᵣ r) x : Sᵣ r)
      ((algebraMap (Rᵣ r) (Sᵣ r) : (a : Rᵣ r) → Sᵣ r) ((algebraMap R (Rᵣ r) : (a : R) → Rᵣ r) x) : Sᵣ r)

Tactic:
simp [RingHom.algebraMap_toAlgebra]

Premises used: RingHom.algebraMap_toAlgebra
-- Module: Mathlib.RingTheory.LocalProperties.Exactness
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
s : Set R
hs : Eq (α := Ideal R) (Ideal.span s) ⊤
Rᵣ : (↑s : Type u_1) → Type u_3
inst_2 : (r : (↑s : Type u_1)) → CommSemiring (Rᵣ r)
inst_3 : (r : (↑s : Type u_1)) → Algebra.{u_1, u_3} R (Rᵣ r)
Sᵣ : (↑s : Type u_1) → Type u_4
inst_4 : (r : (↑s : Type u_1)) → CommSemiring (Sᵣ r)
inst_5 : (r : (↑s : Type u_1)) → Algebra.{u_2, u_4} S (Sᵣ r)
f : R →+* S
inst_6 : ∀ (r : (↑s : Type u_1)), IsLocalization.Away.{u_1, u_3} (↑r : R) (Rᵣ r)
inst_7 : ∀ (r : (↑s : Type u_1)), IsLocalization.Away.{u_2, u_4} (R := S) ((f : (a : R) → S) (↑r : R) : S) (Sᵣ r)
h :
  ∀ (r : (↑s : Type u_1)),
    Function.Injective.{u_3 + 1, u_4 + 1} (α := Rᵣ r) (β := Sᵣ r)
      (⇑(IsLocalization.Away.map (Rᵣ r) (Sᵣ r) f (↑r : R)) : (a : Rᵣ r) → Sᵣ r)
algInst : Algebra R S := f.toAlgebra
this_1 : (r : (↑s : Type u_1)) → Algebra.{u_1, u_4} R (Sᵣ r) :=
  fun (r : (↑s : Type u_1)) ↦ RingHom.toAlgebra (RingHom.comp (algebraMap S (Sᵣ r)) f)
this_2 : ∀ (r : (↑s : Type u_1)), IsScalarTower.{u_1, u_2, u_4} R S (Sᵣ r)
this_3 :
  ∀ (r : (↑s : Type u_1)), IsLocalization.Away.{u_2, u_4} (R := S) ((algebraMap R S : (a : R) → S) (↑r : R) : S) (Sᵣ r)
this : (r : (↑s : Type u_1)) → Algebra.{u_3, u_4} (Rᵣ r) (Sᵣ r) :=
  fun (r : (↑s : Type u_1)) ↦ localizationAlgebra (Submonoid.powers (↑r : R)) S
⊢ ∀ (r : (↑s : Type u_1)), IsScalarTower.{u_1, u_3, u_4} R (Rᵣ r) (Sᵣ r)

Tactic:
have (r : s) : IsScalarTower R (Rᵣ r) (Sᵣ r) :=
    .of_algebraMap_eq <| by simp [RingHom.algebraMap_toAlgebra]
-- Module: Mathlib.RingTheory.LocalProperties.Exactness
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
s : Set R
hs : Eq (α := Ideal R) (Ideal.span s) ⊤
Rᵣ : (↑s : Type u_1) → Type u_3
inst_2 : (r : (↑s : Type u_1)) → CommSemiring (Rᵣ r)
inst_3 : (r : (↑s : Type u_1)) → Algebra.{u_1, u_3} R (Rᵣ r)
Sᵣ : (↑s : Type u_1) → Type u_4
inst_4 : (r : (↑s : Type u_1)) → CommSemiring (Sᵣ r)
inst_5 : (r : (↑s : Type u_1)) → Algebra.{u_2, u_4} S (Sᵣ r)
f : R →+* S
inst_6 : ∀ (r : (↑s : Type u_1)), IsLocalization.Away.{u_1, u_3} (↑r : R) (Rᵣ r)
inst_7 : ∀ (r : (↑s : Type u_1)), IsLocalization.Away.{u_2, u_4} (R := S) ((f : (a : R) → S) (↑r : R) : S) (Sᵣ r)
h :
  ∀ (r : (↑s : Type u_1)),
    Function.Injective.{u_3 + 1, u_4 + 1} (α := Rᵣ r) (β := Sᵣ r)
      (⇑(IsLocalization.Away.map (Rᵣ r) (Sᵣ r) f (↑r : R)) : (a : Rᵣ r) → Sᵣ r)
algInst : Algebra R S := f.toAlgebra
this_1 : (r : (↑s : Type u_1)) → Algebra.{u_1, u_4} R (Sᵣ r) :=
  fun (r : (↑s : Type u_1)) ↦ RingHom.toAlgebra (RingHom.comp (algebraMap S (Sᵣ r)) f)
this_2 : ∀ (r : (↑s : Type u_1)), IsScalarTower.{u_1, u_2, u_4} R S (Sᵣ r)
this_3 :
  ∀ (r : (↑s : Type u_1)), IsLocalization.Away.{u_2, u_4} (R := S) ((algebraMap R S : (a : R) → S) (↑r : R) : S) (Sᵣ r)
this_4 : (r : (↑s : Type u_1)) → Algebra.{u_3, u_4} (Rᵣ r) (Sᵣ r) :=
  fun (r : (↑s : Type u_1)) ↦ localizationAlgebra (Submonoid.powers (↑r : R)) S
this : ∀ (r : (↑s : Type u_1)), IsScalarTower.{u_1, u_3, u_4} R (Rᵣ r) (Sᵣ r)
apply :
  ∀ (r : (↑s : Type u_1)),
    Function.Injective.{u_3 + 1, u_4 + 1} (α := Rᵣ r) (β := Sᵣ r)
      (⇑((IsLocalizedModule.map (Submonoid.powers (↑r : R)) (Algebra.linearMap R (Rᵣ r))
                  (AlgHom.toLinearMap (IsScalarTower.toAlgHom R S (Sᵣ r))) :
                (a : R →ₗ[R] S) → Rᵣ r →ₗ[R] Sᵣ r)
              (Algebra.linearMap R S) :
            LinearMap.{u_1, u_1, u_3, u_4} (RingHom.id R) (Rᵣ r) (Sᵣ r)) :
        (a : Rᵣ r) → Sᵣ r)
⊢ Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)

Tactic:
apply injective_of_isLocalized_span s hs Rᵣ (fun r : s ↦ Algebra.linearMap _ _) _
    (fun r : s ↦ ((IsScalarTower.toAlgHom R S (Sᵣ r)).toLinearMap)) (Algebra.linearMap R S)

Premises used: AlgHom.toLinearMap, IsScalarTower.toAlgHom, Algebra.linearMap, injective_of_isLocalized_span
-- Module: Mathlib.RingTheory.LocalProperties.Exactness
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
s : Set R
hs : Eq (α := Ideal R) (Ideal.span s) ⊤
Rᵣ : (↑s : Type u_1) → Type u_3
inst_2 : (r : (↑s : Type u_1)) → CommSemiring (Rᵣ r)
inst_3 : (r : (↑s : Type u_1)) → Algebra.{u_1, u_3} R (Rᵣ r)
Sᵣ : (↑s : Type u_1) → Type u_4
inst_4 : (r : (↑s : Type u_1)) → CommSemiring (Sᵣ r)
inst_5 : (r : (↑s : Type u_1)) → Algebra.{u_2, u_4} S (Sᵣ r)
f : R →+* S
inst_6 : ∀ (r : (↑s : Type u_1)), IsLocalization.Away.{u_1, u_3} (↑r : R) (Rᵣ r)
inst_7 : ∀ (r : (↑s : Type u_1)), IsLocalization.Away.{u_2, u_4} (R := S) ((f : (a : R) → S) (↑r : R) : S) (Sᵣ r)
h :
  ∀ (r : (↑s : Type u_1)),
    Function.Injective.{u_3 + 1, u_4 + 1} (α := Rᵣ r) (β := Sᵣ r)
      (⇑(IsLocalization.Away.map (Rᵣ r) (Sᵣ r) f (↑r : R)) : (a : Rᵣ r) → Sᵣ r)
algInst : Algebra R S := f.toAlgebra
this_1 : (r : (↑s : Type u_1)) → Algebra.{u_1, u_4} R (Sᵣ r) :=
  fun (r : (↑s : Type u_1)) ↦ RingHom.toAlgebra (RingHom.comp (algebraMap S (Sᵣ r)) f)
this_2 : ∀ (r : (↑s : Type u_1)), IsScalarTower.{u_1, u_2, u_4} R S (Sᵣ r)
this_3 :
  ∀ (r : (↑s : Type u_1)), IsLocalization.Away.{u_2, u_4} (R := S) ((algebraMap R S : (a : R) → S) (↑r : R) : S) (Sᵣ r)
this_4 : (r : (↑s : Type u_1)) → Algebra.{u_3, u_4} (Rᵣ r) (Sᵣ r) :=
  fun (r : (↑s : Type u_1)) ↦ localizationAlgebra (Submonoid.powers (↑r : R)) S
this : ∀ (r : (↑s : Type u_1)), IsScalarTower.{u_1, u_3, u_4} R (Rᵣ r) (Sᵣ r)
⊢ ∀ (r : (↑s : Type u_1)),
    Function.Injective.{u_3 + 1, u_4 + 1} (α := Rᵣ r) (β := Sᵣ r)
      (⇑((IsLocalizedModule.map (Submonoid.powers (↑r : R)) (Algebra.linearMap R (Rᵣ r))
                  (AlgHom.toLinearMap (IsScalarTower.toAlgHom R S (Sᵣ r))) :
                (a : R →ₗ[R] S) → Rᵣ r →ₗ[R] Sᵣ r)
              (Algebra.linearMap R S) :
            LinearMap.{u_1, u_1, u_3, u_4} (RingHom.id R) (Rᵣ r) (Sᵣ r)) :
        (a : Rᵣ r) → Sᵣ r)

Tactic:
simpa [IsLocalization.map_linearMap_eq_toLinearMap_mapₐ] using h

Premises used: IsLocalization.map_linearMap_eq_toLinearMap_mapₐ