awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Module (goal)
Goal:
R : Type u_1
Rₛ : Type u_2
inst : CommSemiring R
S : Submonoid R
inst_1 : CommSemiring Rₛ
inst_2 : Algebra R Rₛ
inst_3 : IsLocalization S Rₛ
M : Type u_3
Mₛ : Type u_4
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid Mₛ
inst_7 : Module R Mₛ
inst_8 : Module Rₛ Mₛ
inst_9 : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst_10 : IsLocalizedModule S f
ι : Type u_5
b : Basis ι R M
⊢ span R (Set.image.{u_3, u_4} (α := M) (⇑f : (a : M) → Mₛ) (Set.range.{u_3, u_5 + 1} (ι := ι) (⇑b : (a : ι) → M))) =
    map f (span R (Set.range.{u_3, u_5 + 1} (ι := ι) (⇑b : (a : ι) → M)))
have rw : Eq.{u_4 + 1} (α := Submodule R Mₛ)
  (span R (Set.image.{u_3, u_4} (α := M) (⇑f : (a : M) → Mₛ) (Set.range.{u_3, u_5 + 1} (ι := ι) (⇑b : (a : ι) → M))))
  (span R (Set.image.{u_3, u_4} (α := M) (⇑f : (a : M) → Mₛ) (Set.range.{u_3, u_5 + 1} (ι := ι) (⇑b : (a : ι) → M))))
Tactic: rw [Submodule.map_span]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Module (goal)
Goal:
R : Type u_1
Rₛ : Type u_2
inst : CommSemiring R
S : Submonoid R
inst_1 : CommSemiring Rₛ
inst_2 : Algebra R Rₛ
inst_3 : IsLocalization S Rₛ
M : Type u_3
Mₛ : Type u_4
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid Mₛ
inst_7 : Module R Mₛ
inst_8 : Module Rₛ Mₛ
inst_9 : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst_10 : IsLocalizedModule S f
ι : Type u_5
b : Basis ι R M
⊢ map f (span R (Set.range.{u_3, u_5 + 1} (ι := ι) (⇑b : (a : ι) → M))) = f.range
have rw : map f ⊤ = f.range
Tactic: rw [b.span_eq, Submodule.map_top]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Module (goal)
Goal:
R : Type u_1
Rₛ : Type u_2
inst : CommSemiring R
S : Submonoid R
inst_1 : CommSemiring Rₛ
inst_2 : Algebra R Rₛ
inst_3 : IsLocalization S Rₛ
M : Type u_3
Mₛ : Type u_4
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid Mₛ
inst_7 : Module R Mₛ
inst_8 : Module Rₛ Mₛ
inst_9 : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst_10 : IsLocalizedModule S f
ι : Type u_5
b : Basis ι R M
rw : map f ⊤ = f.range
⊢ map f (span R (Set.range.{u_3, u_5 + 1} (ι := ι) (⇑b : (a : ι) → M))) = f.range
have rw₁ : f.range = f.range
Tactic: rw [b.span_eq, Submodule.map_top]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Module (goal)
Goal:
R : Type u_1
Rₛ : Type u_2
inst : CommSemiring R
S : Submonoid R
inst_1 : CommSemiring Rₛ
inst_2 : Algebra R Rₛ
inst_3 : IsLocalization S Rₛ
M : Type u_3
Mₛ : Type u_4
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid Mₛ
inst_7 : Module R Mₛ
inst_8 : Module Rₛ Mₛ
inst_9 : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst_10 : IsLocalizedModule S f
ι : Type u_5
b : Basis ι R M
⊢ span R (Set.range.{u_4, u_5 + 1} (ι := ι) (⇑(ofIsLocalizedModule Rₛ S f b) : (a : ι) → Mₛ)) = f.range
have calc : Eq.{u_4 + 1} (α := Submodule R Mₛ)
  (span R (Set.range.{u_4, u_5 + 1} (ι := ι) (⇑(ofIsLocalizedModule Rₛ S f b) : (a : ι) → Mₛ)))
  (span R (Set.image.{u_3, u_4} (α := M) (⇑f : (a : M) → Mₛ) (Set.range.{u_3, u_5 + 1} (ι := ι) (⇑b : (a : ι) → M))))
Tactic: calc span R (Set.range (b.ofIsLocalizedModule Rₛ S f))
    _ = span R (f '' (Set.range b)) := by congr; ext; simp
    _ = map f (span R (Set.range b)) := by rw [Submodule.map_span]
    _ = LinearMap.range f := by rw [b.span_eq, Submodule.map_top]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Module (goal)
Goal:
R : Type u_1
Rₛ : Type u_2
inst : CommSemiring R
S : Submonoid R
inst_1 : CommSemiring Rₛ
inst_2 : Algebra R Rₛ
inst_3 : IsLocalization S Rₛ
M : Type u_3
Mₛ : Type u_4
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid Mₛ
inst_7 : Module R Mₛ
inst_8 : Module Rₛ Mₛ
inst_9 : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst_10 : IsLocalizedModule S f
ι : Type u_5
b : Basis ι R M
calc :
  Eq.{u_4 + 1} (α := Submodule R Mₛ)
    (span R (Set.range.{u_4, u_5 + 1} (ι := ι) (⇑(ofIsLocalizedModule Rₛ S f b) : (a : ι) → Mₛ)))
    (span R (Set.image.{u_3, u_4} (α := M) (⇑f : (a : M) → Mₛ) (Set.range.{u_3, u_5 + 1} (ι := ι) (⇑b : (a : ι) → M))))
⊢ span R (Set.range.{u_4, u_5 + 1} (ι := ι) (⇑(ofIsLocalizedModule Rₛ S f b) : (a : ι) → Mₛ)) = f.range
have calc₁ : span R (Set.image.{u_3, u_4} (α := M) (⇑f : (a : M) → Mₛ) (Set.range.{u_3, u_5 + 1} (ι := ι) (⇑b : (a : ι) → M))) =
  map f (span R (Set.range.{u_3, u_5 + 1} (ι := ι) (⇑b : (a : ι) → M)))
Tactic: calc span R (Set.range (b.ofIsLocalizedModule Rₛ S f))
    _ = span R (f '' (Set.range b)) := by congr; ext; simp
    _ = map f (span R (Set.range b)) := by rw [Submodule.map_span]
    _ = LinearMap.range f := by rw [b.span_eq, Submodule.map_top]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Module (goal)
Goal:
R : Type u_1
Rₛ : Type u_2
inst : CommSemiring R
S : Submonoid R
inst_1 : CommSemiring Rₛ
inst_2 : Algebra R Rₛ
inst_3 : IsLocalization S Rₛ
M : Type u_3
Mₛ : Type u_4
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid Mₛ
inst_7 : Module R Mₛ
inst_8 : Module Rₛ Mₛ
inst_9 : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst_10 : IsLocalizedModule S f
ι : Type u_5
b : Basis ι R M
calc :
  Eq.{u_4 + 1} (α := Submodule R Mₛ)
    (span R (Set.range.{u_4, u_5 + 1} (ι := ι) (⇑(ofIsLocalizedModule Rₛ S f b) : (a : ι) → Mₛ)))
    (span R (Set.image.{u_3, u_4} (α := M) (⇑f : (a : M) → Mₛ) (Set.range.{u_3, u_5 + 1} (ι := ι) (⇑b : (a : ι) → M))))
calc₁ :
  span R (Set.image.{u_3, u_4} (α := M) (⇑f : (a : M) → Mₛ) (Set.range.{u_3, u_5 + 1} (ι := ι) (⇑b : (a : ι) → M))) =
    map f (span R (Set.range.{u_3, u_5 + 1} (ι := ι) (⇑b : (a : ι) → M)))
⊢ span R (Set.range.{u_4, u_5 + 1} (ι := ι) (⇑(ofIsLocalizedModule Rₛ S f b) : (a : ι) → Mₛ)) = f.range
have calc₂ : map f (span R (Set.range.{u_3, u_5 + 1} (ι := ι) (⇑b : (a : ι) → M))) = f.range
Tactic: calc span R (Set.range (b.ofIsLocalizedModule Rₛ S f))
    _ = span R (f '' (Set.range b)) := by congr; ext; simp
    _ = map f (span R (Set.range b)) := by rw [Submodule.map_span]
    _ = LinearMap.range f := by rw [b.span_eq, Submodule.map_top]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Module (goal)
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 y : M →ₗ[R] N
⊢ extendScalarsOfIsLocalization S A (x + y) =
    HAdd.hAdd (α := M →ₗ[A] N) (extendScalarsOfIsLocalization S A x) (extendScalarsOfIsLocalization S A y)
have h : ∀ (x_1 : M),
  Eq.{u_6 + 1} (α := N) ((extendScalarsOfIsLocalization S A (x + y) : (a : M) → N) x_1 : N)
    ((HAdd.hAdd (α := M →ₗ[A] N) (extendScalarsOfIsLocalization S A x) (extendScalarsOfIsLocalization S A y) :
          (a : M) → N)
        x_1 :
      N)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Module (goal)
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
m : A
x : M →ₗ[R] N
⊢ extendScalarsOfIsLocalization S A (m • x) =
    HSMul.hSMul (α := A) (β := M →ₗ[A] N) ((RingHom.id A : (a : A) → A) m : A) (extendScalarsOfIsLocalization S A x)
have h : ∀ (x_1 : M),
  Eq.{u_6 + 1} (α := N) ((extendScalarsOfIsLocalization S A (m • x) : (a : M) → N) x_1 : N)
    ((HSMul.hSMul (α := A) (β := M →ₗ[A] N) ((RingHom.id A : (a : A) → A) m : A) (extendScalarsOfIsLocalization S A x) :
          (a : M) → N)
        x_1 :
      N)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Module (goal)
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 →ₗ[R] N
⊢ (↑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₂)
      (extendScalarsOfIsLocalization S A x) =
    x
have h : ∀ (x_1 : M),
  Eq.{u_6 + 1} (α := N)
    (((↑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₂)
            (extendScalarsOfIsLocalization S A x) :
          (a : M) → N)
        x_1 :
      N)
    ((x : (a : M) → N) x_1 : N)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Module (goal)
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
⊢ 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
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Module (goal)
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
⊢ Eq (α := N →ₗ[A] N)
    (LinearMap.extendScalarsOfIsLocalization S A (↑f : M →ₗ[R] N) ∘ₗ
      LinearMap.extendScalarsOfIsLocalization S A (↑f.symm : N →ₗ[R] M))
    LinearMap.id
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Module (goal)
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
⊢ Eq (α := M →ₗ[A] M)
    (LinearMap.extendScalarsOfIsLocalization S A (↑f.symm : N →ₗ[R] M) ∘ₗ
      LinearMap.extendScalarsOfIsLocalization S A (↑f : M →ₗ[R] N))
    LinearMap.id
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Module (goal)
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
⊢ (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
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Module (goal)
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
⊢ (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
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Module (goal)
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
⊢ 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
have 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)
Tactic: apply LinearMap.restrictScalars_injective R
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Module (goal)
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
⊢ 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
have 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)
Tactic: apply LinearMap.restrictScalars_injective R
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Module (goal)
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)
        (mk x y) :
      LocalizedModule S N)
    (mk ((f : (a : M) → N) x) y : LocalizedModule S N)
have 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)
Tactic: rw [IsLocalizedModule.mk_eq_mk', IsLocalizedModule.mk_eq_mk']
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Module (goal)
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_5
inst_3 : AddCommMonoid N
inst_4 : Module R N
M' : Type u_3
N' : Type u_4
inst_5 : AddCommMonoid M'
inst_6 : AddCommMonoid N'
inst_7 : Module R M'
inst_8 : Module R N'
g₁ : M →ₗ[R] M'
g₂ : N →ₗ[R] N'
inst_9 : IsLocalizedModule S g₁
inst_10 : IsLocalizedModule S g₂
l : M →ₗ[R] N
⊢ (↑R :
        {S : Type u_1} →
          {M : Type (max u_1 u_2)} →
            {M₂ : Type (max u_1 u_5)} →
              [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₂] →
                              [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      (S := Localization (M := R) S)
      ((map S : (a : M →ₗ[R] N) → LocalizedModule S M →ₗ[Localization S] LocalizedModule S N) l) =
    (↑(IsLocalizedModule.iso S g₂).symm : N' →ₗ[R] LocalizedModule S N) ∘ₗ
      (IsLocalizedModule.map S g₁ g₂ : (a : M →ₗ[R] N) → M' →ₗ[R] N') l ∘ₗ
        (↑(IsLocalizedModule.iso S g₁) : LocalizedModule S M →ₗ[R] M')
have rw : ((↑(IsLocalizedModule.iso S g₂) : LocalizedModule S N →ₗ[R] N') ∘ₗ
      (↑R :
          {S : Type u_1} →
            {M : Type (max u_1 u_2)} →
              {M₂ : Type (max u_1 u_5)} →
                [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₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        (S := Localization (M := R) S)
        ((map S : (a : M →ₗ[R] N) → LocalizedModule S M →ₗ[Localization S] LocalizedModule S N) l)) ∘ₗ
    (↑(IsLocalizedModule.iso S g₁).symm : M' →ₗ[R] LocalizedModule S M) =
  (IsLocalizedModule.map S g₁ g₂ : (a : M →ₗ[R] N) → M' →ₗ[R] N') l
Tactic: rw [LinearEquiv.eq_toLinearMap_symm_comp, ← LinearEquiv.comp_toLinearMap_symm_eq]