awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Localization.Module
Goal:
R_1 : Type u_1
Rₛ : Type u_2
R : Type u_3
inst : CommSemiring R
S : Submonoid R
A : Type u_4
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : IsLocalization S A
M : Type u_5
N : Type u_6
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : Module A M
inst_7 : IsScalarTower R A M
inst_8 : AddCommMonoid N
inst_9 : Module R N
inst_10 : Module A N
inst_11 : IsScalarTower R A N
x : M →ₗ[A] N
h :
  ∀ (x_1 : M),
    Eq.{u_6 + 1} (α := N)
      ((extendScalarsOfIsLocalization S A
              ((↑R :
                  {S : Type u_4} →
                    {M : Type u_5} →
                      {M₂ : Type u_6} →
                        [inst : Semiring R] →
                          [inst_12 : Semiring S] →
                            [inst_13 : AddCommMonoid M] →
                              [inst_14 : AddCommMonoid M₂] →
                                [inst_15 : Module R M] →
                                  [inst_16 : Module R M₂] →
                                    [inst_17 : Module S M] →
                                      [inst_18 : Module S M₂] →
                                        [CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                x) :
            (a : M) → N)
          x_1 :
        N)
      ((x : (a : M) → N) x_1 : N)
⊢ extendScalarsOfIsLocalization S A
      ((↑R :
          {S : Type u_4} →
            {M : Type u_5} →
              {M₂ : Type u_6} →
                [inst : Semiring R] →
                  [inst_12 : Semiring S] →
                    [inst_13 : AddCommMonoid M] →
                      [inst_14 : AddCommMonoid M₂] →
                        [inst_15 : Module R M] →
                          [inst_16 : Module R M₂] →
                            [inst_17 : Module S M] →
                              [inst_18 : Module S M₂] → [CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        x) =
    x

Tactic:
ext
-- Module: Mathlib.RingTheory.Localization.Module
Goal:
R_1 : Type u_1
Rₛ : Type u_2
R : Type u_3
inst : CommSemiring R
S : Submonoid R
A : Type u_4
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : IsLocalization S A
M : Type u_5
N : Type u_6
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : Module A M
inst_7 : IsScalarTower R A M
inst_8 : AddCommMonoid N
inst_9 : Module R N
inst_10 : Module A N
inst_11 : IsScalarTower R A N
x : M →ₗ[A] N
x_1 : M
⊢ Eq.{u_6 + 1} (α := N)
    ((extendScalarsOfIsLocalization S A
            ((↑R :
                {S : Type u_4} →
                  {M : Type u_5} →
                    {M₂ : Type u_6} →
                      [inst : Semiring R] →
                        [inst_12 : Semiring S] →
                          [inst_13 : AddCommMonoid M] →
                            [inst_14 : AddCommMonoid M₂] →
                              [inst_15 : Module R M] →
                                [inst_16 : Module R M₂] →
                                  [inst_17 : Module S M] →
                                    [inst_18 : Module S M₂] →
                                      [CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
              x) :
          (a : M) → N)
        x_1 :
      N)
    ((x : (a : M) → N) x_1 : N)

Tactic:
simp
-- Module: Mathlib.RingTheory.Localization.Module
Goal:
R_1 : Type u_1
Rₛ : Type u_2
R : Type u_3
inst : CommSemiring R
S : Submonoid R
A : Type u_4
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : IsLocalization S A
M : Type u_5
N : Type u_6
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : Module A M
inst_7 : IsScalarTower R A M
inst_8 : AddCommMonoid N
inst_9 : Module R N
inst_10 : Module A N
inst_11 : IsScalarTower R A N
f : M ≃ₗ[R] N
h :
  ∀ (x : N),
    Eq (α := N)
      ((LinearMap.extendScalarsOfIsLocalization S A (↑f : M →ₗ[R] N) ∘ₗ
              LinearMap.extendScalarsOfIsLocalization S A (↑f.symm : N →ₗ[R] M) :
            (a : N) → N)
          x :
        N)
      ((LinearMap.id : (a : N) → N) x : N)
⊢ Eq (α := N →ₗ[A] N)
    (LinearMap.extendScalarsOfIsLocalization S A (↑f : M →ₗ[R] N) ∘ₗ
      LinearMap.extendScalarsOfIsLocalization S A (↑f.symm : N →ₗ[R] M))
    LinearMap.id

Tactic:
ext
-- Module: Mathlib.RingTheory.Localization.Module
Goal:
R_1 : Type u_1
Rₛ : Type u_2
R : Type u_3
inst : CommSemiring R
S : Submonoid R
A : Type u_4
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : IsLocalization S A
M : Type u_5
N : Type u_6
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : Module A M
inst_7 : IsScalarTower R A M
inst_8 : AddCommMonoid N
inst_9 : Module R N
inst_10 : Module A N
inst_11 : IsScalarTower R A N
f : M ≃ₗ[R] N
x : N
⊢ Eq (α := N)
    ((LinearMap.extendScalarsOfIsLocalization S A (↑f : M →ₗ[R] N) ∘ₗ
            LinearMap.extendScalarsOfIsLocalization S A (↑f.symm : N →ₗ[R] M) :
          (a : N) → N)
        x :
      N)
    ((LinearMap.id : (a : N) → N) x : N)

Tactic:
simp
-- Module: Mathlib.RingTheory.Localization.Module
Goal:
R_1 : Type u_1
Rₛ : Type u_2
R : Type u_3
inst : CommSemiring R
S : Submonoid R
A : Type u_4
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : IsLocalization S A
M : Type u_5
N : Type u_6
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : Module A M
inst_7 : IsScalarTower R A M
inst_8 : AddCommMonoid N
inst_9 : Module R N
inst_10 : Module A N
inst_11 : IsScalarTower R A N
f : M ≃ₗ[R] N
h :
  ∀ (x : M),
    Eq (α := M)
      ((LinearMap.extendScalarsOfIsLocalization S A (↑f.symm : N →ₗ[R] M) ∘ₗ
              LinearMap.extendScalarsOfIsLocalization S A (↑f : M →ₗ[R] N) :
            (a : M) → M)
          x :
        M)
      ((LinearMap.id : (a : M) → M) x : M)
⊢ Eq (α := M →ₗ[A] M)
    (LinearMap.extendScalarsOfIsLocalization S A (↑f.symm : N →ₗ[R] M) ∘ₗ
      LinearMap.extendScalarsOfIsLocalization S A (↑f : M →ₗ[R] N))
    LinearMap.id

Tactic:
ext
-- Module: Mathlib.RingTheory.Localization.Module
Goal:
R_1 : Type u_1
Rₛ : Type u_2
R : Type u_3
inst : CommSemiring R
S : Submonoid R
A : Type u_4
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : IsLocalization S A
M : Type u_5
N : Type u_6
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : Module A M
inst_7 : IsScalarTower R A M
inst_8 : AddCommMonoid N
inst_9 : Module R N
inst_10 : Module A N
inst_11 : IsScalarTower R A N
f : M ≃ₗ[R] N
x : M
⊢ Eq (α := M)
    ((LinearMap.extendScalarsOfIsLocalization S A (↑f.symm : N →ₗ[R] M) ∘ₗ
            LinearMap.extendScalarsOfIsLocalization S A (↑f : M →ₗ[R] N) :
          (a : M) → M)
        x :
      M)
    ((LinearMap.id : (a : M) → M) x : M)

Tactic:
simp
-- Module: Mathlib.RingTheory.Localization.Module
Goal:
R_1 : Type u_1
Rₛ : Type u_2
R : Type u_3
inst : CommSemiring R
S : Submonoid R
A : Type u_4
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : IsLocalization S A
M : Type u_5
N : Type u_6
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : Module A M
inst_7 : IsScalarTower R A M
inst_8 : AddCommMonoid N
inst_9 : Module R N
inst_10 : Module A N
inst_11 : IsScalarTower R A N
e : M ≃ₗ[R] N
h :
  ∀ (x : M),
    Eq.{u_6 + 1} (α := N)
      (((fun (e : M ≃ₗ[A] N) ↦ (restrictScalars R e : M ≃ₗ[R] N))
              ((fun (e : M ≃ₗ[R] N) ↦ (extendScalarsOfIsLocalization S A e : M ≃ₗ[A] N)) e) :
            (a : M) → N)
          x :
        N)
      ((e : (a : M) → N) x : N)
⊢ (fun (e : M ≃ₗ[A] N) ↦ (restrictScalars R e : M ≃ₗ[R] N))
      ((fun (e : M ≃ₗ[R] N) ↦ (extendScalarsOfIsLocalization S A e : M ≃ₗ[A] N)) e) =
    e

Tactic:
ext
-- Module: Mathlib.RingTheory.Localization.Module
Goal:
R_1 : Type u_1
Rₛ : Type u_2
R : Type u_3
inst : CommSemiring R
S : Submonoid R
A : Type u_4
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : IsLocalization S A
M : Type u_5
N : Type u_6
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : Module A M
inst_7 : IsScalarTower R A M
inst_8 : AddCommMonoid N
inst_9 : Module R N
inst_10 : Module A N
inst_11 : IsScalarTower R A N
e : M ≃ₗ[R] N
x : M
⊢ Eq.{u_6 + 1} (α := N)
    (((fun (e : M ≃ₗ[A] N) ↦ (restrictScalars R e : M ≃ₗ[R] N))
            ((fun (e : M ≃ₗ[R] N) ↦ (extendScalarsOfIsLocalization S A e : M ≃ₗ[A] N)) e) :
          (a : M) → N)
        x :
      N)
    ((e : (a : M) → N) x : N)

Tactic:
simp
-- Module: Mathlib.RingTheory.Localization.Module
Goal:
R_1 : Type u_1
Rₛ : Type u_2
R : Type u_3
inst : CommSemiring R
S : Submonoid R
A : Type u_4
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : IsLocalization S A
M : Type u_5
N : Type u_6
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : Module A M
inst_7 : IsScalarTower R A M
inst_8 : AddCommMonoid N
inst_9 : Module R N
inst_10 : Module A N
inst_11 : IsScalarTower R A N
e : M ≃ₗ[A] N
h :
  ∀ (x : M),
    Eq.{u_6 + 1} (α := N)
      (((fun (e : M ≃ₗ[R] N) ↦ (extendScalarsOfIsLocalization S A e : M ≃ₗ[A] N))
              ((fun (e : M ≃ₗ[A] N) ↦ (restrictScalars R e : M ≃ₗ[R] N)) e) :
            (a : M) → N)
          x :
        N)
      ((e : (a : M) → N) x : N)
⊢ (fun (e : M ≃ₗ[R] N) ↦ (extendScalarsOfIsLocalization S A e : M ≃ₗ[A] N))
      ((fun (e : M ≃ₗ[A] N) ↦ (restrictScalars R e : M ≃ₗ[R] N)) e) =
    e

Tactic:
ext
-- Module: Mathlib.RingTheory.Localization.Module
Goal:
R_1 : Type u_1
Rₛ : Type u_2
R : Type u_3
inst : CommSemiring R
S : Submonoid R
A : Type u_4
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : IsLocalization S A
M : Type u_5
N : Type u_6
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : Module A M
inst_7 : IsScalarTower R A M
inst_8 : AddCommMonoid N
inst_9 : Module R N
inst_10 : Module A N
inst_11 : IsScalarTower R A N
e : M ≃ₗ[A] N
x : M
⊢ Eq.{u_6 + 1} (α := N)
    (((fun (e : M ≃ₗ[R] N) ↦ (extendScalarsOfIsLocalization S A e : M ≃ₗ[A] N))
            ((fun (e : M ≃ₗ[A] N) ↦ (restrictScalars R e : M ≃ₗ[R] N)) e) :
          (a : M) → N)
        x :
      N)
    ((e : (a : M) → N) x : N)

Tactic:
simp
-- Module: Mathlib.RingTheory.Localization.Module
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
N : Type u_4
N' : Type u_5
inst_6 : AddCommMonoid N
inst_7 : AddCommMonoid N'
inst_8 : Module R N
inst_9 : Module R N'
g : N →ₗ[R] N'
inst_10 : IsLocalizedModule S g
Rₛ : Type u_6
inst_11 : CommSemiring Rₛ
inst_12 : Algebra R Rₛ
inst_13 : Module Rₛ M'
inst_14 : Module Rₛ N'
inst_15 : IsScalarTower R Rₛ M'
inst_16 : IsScalarTower R Rₛ N'
inst_17 : IsLocalization S Rₛ
e : M ≃ₗ[R] N
a :
  Eq.{u_5 + 1} (α := N' →ₗ[R] N')
    ((↑R :
        {S : Type u_6} →
          {M M₂ : Type u_5} →
            [inst : Semiring R] →
              [inst_18 : Semiring S] →
                [inst_19 : AddCommMonoid M] →
                  [inst_20 : AddCommMonoid M₂] →
                    [inst_21 : Module R M] →
                      [inst_22 : Module R M₂] →
                        [inst_23 : Module S M] →
                          [inst_24 : Module S M₂] →
                            [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      (((mapExtendScalars S f g Rₛ : (M →ₗ[R] N) →ₗ[R] M' →ₗ[Rₛ] N') : (a : M →ₗ[R] N) → M' →ₗ[Rₛ] N')
          (↑e : M →ₗ[R] N) ∘ₗ
        ((mapExtendScalars S g f Rₛ : (N →ₗ[R] M) →ₗ[R] N' →ₗ[Rₛ] M') : (a : N →ₗ[R] M) → N' →ₗ[Rₛ] M')
          (↑e.symm : N →ₗ[R] M)))
    ((↑R :
        {S : Type u_6} →
          {M M₂ : Type u_5} →
            [inst : Semiring R] →
              [inst_18 : Semiring S] →
                [inst_19 : AddCommMonoid M] →
                  [inst_20 : AddCommMonoid M₂] →
                    [inst_21 : Module R M] →
                      [inst_22 : Module R M₂] →
                        [inst_23 : Module S M] →
                          [inst_24 : Module S M₂] →
                            [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      (S := Rₛ) LinearMap.id)
⊢ Eq.{u_5 + 1} (α := N' →ₗ[Rₛ] N')
    (((mapExtendScalars S f g Rₛ : (M →ₗ[R] N) →ₗ[R] M' →ₗ[Rₛ] N') : (a : M →ₗ[R] N) → M' →ₗ[Rₛ] N') (↑e : M →ₗ[R] N) ∘ₗ
      ((mapExtendScalars S g f Rₛ : (N →ₗ[R] M) →ₗ[R] N' →ₗ[Rₛ] M') : (a : N →ₗ[R] M) → N' →ₗ[Rₛ] M')
        (↑e.symm : N →ₗ[R] M))
    LinearMap.id

Tactic:
apply LinearMap.restrictScalars_injective R

Premises used: LinearMap.restrictScalars_injective
-- Module: Mathlib.RingTheory.Localization.Module
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
N : Type u_4
N' : Type u_5
inst_6 : AddCommMonoid N
inst_7 : AddCommMonoid N'
inst_8 : Module R N
inst_9 : Module R N'
g : N →ₗ[R] N'
inst_10 : IsLocalizedModule S g
Rₛ : Type u_6
inst_11 : CommSemiring Rₛ
inst_12 : Algebra R Rₛ
inst_13 : Module Rₛ M'
inst_14 : Module Rₛ N'
inst_15 : IsScalarTower R Rₛ M'
inst_16 : IsScalarTower R Rₛ N'
inst_17 : IsLocalization S Rₛ
e : M ≃ₗ[R] N
x : N
⊢ Eq.{u_5 + 1} (α := N')
    (((↑R :
                {S : Type u_6} →
                  {M M₂ : Type u_5} →
                    [inst : Semiring R] →
                      [inst_18 : Semiring S] →
                        [inst_19 : AddCommMonoid M] →
                          [inst_20 : AddCommMonoid M₂] →
                            [inst_21 : Module R M] →
                              [inst_22 : Module R M₂] →
                                [inst_23 : Module S M] →
                                  [inst_24 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
              (((mapExtendScalars S f g Rₛ : (M →ₗ[R] N) →ₗ[R] M' →ₗ[Rₛ] N') : (a : M →ₗ[R] N) → M' →ₗ[Rₛ] N')
                  (↑e : M →ₗ[R] N) ∘ₗ
                ((mapExtendScalars S g f Rₛ : (N →ₗ[R] M) →ₗ[R] N' →ₗ[Rₛ] M') : (a : N →ₗ[R] M) → N' →ₗ[Rₛ] M')
                  (↑e.symm : N →ₗ[R] M)) ∘ₗ
            g :
          (a : N) → N')
        x :
      N')
    (((↑R :
                {S : Type u_6} →
                  {M M₂ : Type u_5} →
                    [inst : Semiring R] →
                      [inst_18 : Semiring S] →
                        [inst_19 : AddCommMonoid M] →
                          [inst_20 : AddCommMonoid M₂] →
                            [inst_21 : Module R M] →
                              [inst_22 : Module R M₂] →
                                [inst_23 : Module S M] →
                                  [inst_24 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
              (S := Rₛ) LinearMap.id ∘ₗ
            g :
          (a : N) → N')
        x :
      N')

Tactic:
simp
-- Module: Mathlib.RingTheory.Localization.Module
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
N : Type u_4
N' : Type u_5
inst_6 : AddCommMonoid N
inst_7 : AddCommMonoid N'
inst_8 : Module R N
inst_9 : Module R N'
g : N →ₗ[R] N'
inst_10 : IsLocalizedModule S g
Rₛ : Type u_6
inst_11 : CommSemiring Rₛ
inst_12 : Algebra R Rₛ
inst_13 : Module Rₛ M'
inst_14 : Module Rₛ N'
inst_15 : IsScalarTower R Rₛ M'
inst_16 : IsScalarTower R Rₛ N'
inst_17 : IsLocalization S Rₛ
e : M ≃ₗ[R] N
a :
  Eq.{u_3 + 1} (α := M' →ₗ[R] M')
    ((↑R :
        {S : Type u_6} →
          {M M₂ : Type u_3} →
            [inst : Semiring R] →
              [inst_18 : Semiring S] →
                [inst_19 : AddCommMonoid M] →
                  [inst_20 : AddCommMonoid M₂] →
                    [inst_21 : Module R M] →
                      [inst_22 : Module R M₂] →
                        [inst_23 : Module S M] →
                          [inst_24 : Module S M₂] →
                            [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      (((mapExtendScalars S g f Rₛ : (N →ₗ[R] M) →ₗ[R] N' →ₗ[Rₛ] M') : (a : N →ₗ[R] M) → N' →ₗ[Rₛ] M')
          (↑e.symm : N →ₗ[R] M) ∘ₗ
        ((mapExtendScalars S f g Rₛ : (M →ₗ[R] N) →ₗ[R] M' →ₗ[Rₛ] N') : (a : M →ₗ[R] N) → M' →ₗ[Rₛ] N')
          (↑e : M →ₗ[R] N)))
    ((↑R :
        {S : Type u_6} →
          {M M₂ : Type u_3} →
            [inst : Semiring R] →
              [inst_18 : Semiring S] →
                [inst_19 : AddCommMonoid M] →
                  [inst_20 : AddCommMonoid M₂] →
                    [inst_21 : Module R M] →
                      [inst_22 : Module R M₂] →
                        [inst_23 : Module S M] →
                          [inst_24 : Module S M₂] →
                            [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      (S := Rₛ) LinearMap.id)
⊢ Eq.{u_3 + 1} (α := M' →ₗ[Rₛ] M')
    (((mapExtendScalars S g f Rₛ : (N →ₗ[R] M) →ₗ[R] N' →ₗ[Rₛ] M') : (a : N →ₗ[R] M) → N' →ₗ[Rₛ] M')
        (↑e.symm : N →ₗ[R] M) ∘ₗ
      ((mapExtendScalars S f g Rₛ : (M →ₗ[R] N) →ₗ[R] M' →ₗ[Rₛ] N') : (a : M →ₗ[R] N) → M' →ₗ[Rₛ] N') (↑e : M →ₗ[R] N))
    LinearMap.id

Tactic:
apply LinearMap.restrictScalars_injective R

Premises used: LinearMap.restrictScalars_injective
-- Module: Mathlib.RingTheory.Localization.Module
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
N : Type u_4
N' : Type u_5
inst_6 : AddCommMonoid N
inst_7 : AddCommMonoid N'
inst_8 : Module R N
inst_9 : Module R N'
g : N →ₗ[R] N'
inst_10 : IsLocalizedModule S g
Rₛ : Type u_6
inst_11 : CommSemiring Rₛ
inst_12 : Algebra R Rₛ
inst_13 : Module Rₛ M'
inst_14 : Module Rₛ N'
inst_15 : IsScalarTower R Rₛ M'
inst_16 : IsScalarTower R Rₛ N'
inst_17 : IsLocalization S Rₛ
e : M ≃ₗ[R] N
x : M
⊢ Eq.{u_3 + 1} (α := M')
    (((↑R :
                {S : Type u_6} →
                  {M M₂ : Type u_3} →
                    [inst : Semiring R] →
                      [inst_18 : Semiring S] →
                        [inst_19 : AddCommMonoid M] →
                          [inst_20 : AddCommMonoid M₂] →
                            [inst_21 : Module R M] →
                              [inst_22 : Module R M₂] →
                                [inst_23 : Module S M] →
                                  [inst_24 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
              (((mapExtendScalars S g f Rₛ : (N →ₗ[R] M) →ₗ[R] N' →ₗ[Rₛ] M') : (a : N →ₗ[R] M) → N' →ₗ[Rₛ] M')
                  (↑e.symm : N →ₗ[R] M) ∘ₗ
                ((mapExtendScalars S f g Rₛ : (M →ₗ[R] N) →ₗ[R] M' →ₗ[Rₛ] N') : (a : M →ₗ[R] N) → M' →ₗ[Rₛ] N')
                  (↑e : M →ₗ[R] N)) ∘ₗ
            f :
          (a : M) → M')
        x :
      M')
    (((↑R :
                {S : Type u_6} →
                  {M M₂ : Type u_3} →
                    [inst : Semiring R] →
                      [inst_18 : Semiring S] →
                        [inst_19 : AddCommMonoid M] →
                          [inst_20 : AddCommMonoid M₂] →
                            [inst_21 : Module R M] →
                              [inst_22 : Module R M₂] →
                                [inst_23 : Module S M] →
                                  [inst_24 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
              (S := Rₛ) LinearMap.id ∘ₗ
            f :
          (a : M) → M')
        x :
      M')

Tactic:
simp
-- Module: Mathlib.RingTheory.Localization.Module
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
f : M →ₗ[R] N
x : M
y : ↥S
rw :
  Eq (α := LocalizedModule S N)
    ((((map S : (a : M →ₗ[R] N) → LocalizedModule S M →ₗ[Localization S] LocalizedModule S N) f :
            LinearMap (R := Localization (M := R) S) (RingHom.id (Localization (M := R) S)) (LocalizedModule S M)
              (LocalizedModule S N)) :
          (a : LocalizedModule S M) → LocalizedModule S N)
        (IsLocalizedModule.mk' (mkLinearMap S M) x y) :
      LocalizedModule S N)
    (IsLocalizedModule.mk' (mkLinearMap S N) ((f : (a : M) → N) x) y : LocalizedModule S N)
⊢ Eq (α := LocalizedModule S N)
    ((((map S : (a : M →ₗ[R] N) → LocalizedModule S M →ₗ[Localization S] LocalizedModule S N) f :
            LinearMap (R := Localization (M := R) S) (RingHom.id (Localization (M := R) S)) (LocalizedModule S M)
              (LocalizedModule S N)) :
          (a : LocalizedModule S M) → LocalizedModule S N)
        (mk x y) :
      LocalizedModule S N)
    (mk ((f : (a : M) → N) x) y : LocalizedModule S N)

Tactic:
rw [IsLocalizedModule.mk_eq_mk', IsLocalizedModule.mk_eq_mk']

Premises used: IsLocalizedModule.mk_eq_mk'
-- Module: Mathlib.RingTheory.Localization.Module
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
f : M →ₗ[R] N
x : M
y : ↥S
⊢ Eq (α := LocalizedModule S N)
    ((((map S : (a : M →ₗ[R] N) → LocalizedModule S M →ₗ[Localization S] LocalizedModule S N) f :
            LinearMap (R := Localization (M := R) S) (RingHom.id (Localization (M := R) S)) (LocalizedModule S M)
              (LocalizedModule S N)) :
          (a : LocalizedModule S M) → LocalizedModule S N)
        (IsLocalizedModule.mk' (mkLinearMap S M) x y) :
      LocalizedModule S N)
    (IsLocalizedModule.mk' (mkLinearMap S N) ((f : (a : M) → N) x) y : LocalizedModule S N)

Tactic:
IsLocalizedModule.map_mk' _ _ _ _ _ _

Premises used: LocalizedModule.liftOn, IsLocalizedModule.map_mk', LocalizedModule.lift'
-- Module: Mathlib.RingTheory.Localization.Module
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
f : M →ₗ[R] N
x : M
y : ↥S
⊢ Eq (α := LocalizedModule S N)
    ((((map S : (a : M →ₗ[R] N) → LocalizedModule S M →ₗ[Localization S] LocalizedModule S N) f :
            LinearMap (R := Localization (M := R) S) (RingHom.id (Localization (M := R) S)) (LocalizedModule S M)
              (LocalizedModule S N)) :
          (a : LocalizedModule S M) → LocalizedModule S N)
        (IsLocalizedModule.mk' (mkLinearMap S M) x y) :
      LocalizedModule S N)
    (IsLocalizedModule.mk' (mkLinearMap S N) ((f : (a : M) → N) x) y : LocalizedModule S N)

Tactic:
exact IsLocalizedModule.map_mk' _ _ _ _ _ _

Premises used: IsLocalizedModule.map_mk'
-- Module: Mathlib.RingTheory.Localization.Module
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Eq (α :=
    LinearMap (R := Localization (M := R) S) (RingHom.id (Localization (M := R) S)) (LocalizedModule S M)
      (LocalizedModule S M))
    ((map S : (a : M →ₗ[R] M) → LocalizedModule S M →ₗ[Localization S] LocalizedModule S M) LinearMap.id :
      LinearMap (R := Localization (M := R) S) (RingHom.id (Localization (M := R) S)) (LocalizedModule S M)
        (LocalizedModule S M))
    (LinearMap.id :
      LinearMap (R := Localization (M := R) S) (RingHom.id (Localization (M := R) S)) (LocalizedModule S M)
        (LocalizedModule S M))

Tactic:
LinearMap.ext fun x ↦ LinearMap.congr_fun (IsLocalizedModule.map_id S (mkLinearMap S M)) x

Premises used: LinearMap.ext, IsLocalizedModule.map_id, LinearMap.congr_fun, LocalizedModule.mkLinearMap
-- Module: Mathlib.RingTheory.Localization.Module
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
l : M →ₗ[R] N
hl : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑l : (a : M) → N)
⊢ Function.Injective (α := LocalizedModule S M) (β := LocalizedModule S N)
    (⇑((map S : (a : M →ₗ[R] N) → LocalizedModule S M →ₗ[Localization S] LocalizedModule S N) l :
          LinearMap (R := Localization (M := R) S) (RingHom.id (Localization (M := R) S)) (LocalizedModule S M)
            (LocalizedModule S N)) :
      (a : LocalizedModule S M) → LocalizedModule S N)

Tactic:
IsLocalizedModule.map_injective S (mkLinearMap S M) (mkLinearMap S N) l hl

Premises used: LocalizedModule.liftOn, IsLocalizedModule.map_injective, LocalizedModule.mkLinearMap, LocalizedModule.lift'