awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Localization.Module
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
m : M
i : ι
⊢ Eq (α := M →ₗ[R] ι →₀ Rₛ)
    ((↑R :
          {S : Type u_2} →
            {M : Type u_4} →
              {M₂ : Type (max u_2 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₂)
        (↑(repr (ofIsLocalizedModule Rₛ S f b)) : Mₛ →ₗ[Rₛ] ι →₀ Rₛ) ∘ₗ
      f)
    (Finsupp.mapRange.linearMap (Algebra.linearMap R Rₛ) ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R))

Tactic:
ext b fun i ↦ ?_

Premises used: Module.Basis.ext
-- Module: Mathlib.RingTheory.Localization.Module
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
m : M
i : ι
refine :
  ∀ (i : ι),
    Eq (α := ι →₀ Rₛ)
      (((↑R :
                  {S : Type u_2} →
                    {M : Type u_4} →
                      {M₂ : Type (max u_2 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₂)
                (↑(repr (ofIsLocalizedModule Rₛ S f b)) : Mₛ →ₗ[Rₛ] ι →₀ Rₛ) ∘ₗ
              f :
            (a : M) → ι →₀ Rₛ)
          ((b : (a : ι) → M) i) :
        ι →₀ Rₛ)
      ((Finsupp.mapRange.linearMap (Algebra.linearMap R Rₛ) ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R) : (a : M) → ι →₀ Rₛ)
          ((b : (a : ι) → M) i) :
        ι →₀ Rₛ)
⊢ Eq (α := M →ₗ[R] ι →₀ Rₛ)
    ((↑R :
          {S : Type u_2} →
            {M : Type u_4} →
              {M₂ : Type (max u_2 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₂)
        (↑(repr (ofIsLocalizedModule Rₛ S f b)) : Mₛ →ₗ[Rₛ] ι →₀ Rₛ) ∘ₗ
      f)
    (Finsupp.mapRange.linearMap (Algebra.linearMap R Rₛ) ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R))

Tactic:
refine ext b fun i ↦ ?_

Premises used: Module.Basis.ext
-- Module: Mathlib.RingTheory.Localization.Module
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
e_s :
  Eq.{u_4 + 1} (α := Set Mₛ) (Set.range.{u_4, u_5 + 1} (ι := ι) (⇑(ofIsLocalizedModule Rₛ S f b) : (a : ι) → Mₛ))
    (Set.image.{u_3, u_4} (α := M) (⇑f : (a : M) → Mₛ) (Set.range.{u_3, u_5 + 1} (ι := ι) (⇑b : (a : ι) → M)))
⊢ 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:
congr
-- Module: Mathlib.RingTheory.Localization.Module
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
e_s :
  ∀ (x : Mₛ),
    Membership.mem (γ := Set Mₛ) (Set.range.{u_4, u_5 + 1} (ι := ι) (⇑(ofIsLocalizedModule Rₛ S f b) : (a : ι) → Mₛ))
        x ↔
      Membership.mem (γ := Set Mₛ)
        (Set.image.{u_3, u_4} (α := M) (⇑f : (a : M) → Mₛ) (Set.range.{u_3, u_5 + 1} (ι := ι) (⇑b : (a : ι) → M))) x
⊢ Eq.{u_4 + 1} (α := Set Mₛ) (Set.range.{u_4, u_5 + 1} (ι := ι) (⇑(ofIsLocalizedModule Rₛ S f b) : (a : ι) → Mₛ))
    (Set.image.{u_3, u_4} (α := M) (⇑f : (a : M) → Mₛ) (Set.range.{u_3, u_5 + 1} (ι := ι) (⇑b : (a : ι) → M)))

Tactic:
ext
-- Module: Mathlib.RingTheory.Localization.Module
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
x : Mₛ
⊢ Membership.mem (γ := Set Mₛ) (Set.range.{u_4, u_5 + 1} (ι := ι) (⇑(ofIsLocalizedModule Rₛ S f b) : (a : ι) → Mₛ)) x ↔
    Membership.mem (γ := Set Mₛ)
      (Set.image.{u_3, u_4} (α := M) (⇑f : (a : M) → Mₛ) (Set.range.{u_3, u_5 + 1} (ι := ι) (⇑b : (a : ι) → M))) x

Tactic:
simp
-- Module: Mathlib.RingTheory.Localization.Module
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 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))))
⊢ 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:
rw [Submodule.map_span]

Premises used: Submodule.map_span
-- Module: Mathlib.RingTheory.Localization.Module
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
rw₁ rw₂ : f.range = f.range
⊢ map f (span R (Set.range.{u_3, u_5 + 1} (ι := ι) (⇑b : (a : ι) → M))) = f.range

Tactic:
rw [b.span_eq, Submodule.map_top]

Premises used: Submodule.map_top, Module.Basis.span_eq
-- Module: Mathlib.RingTheory.Localization.Module
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)))
calc₂ : map f (span R (Set.range.{u_3, u_5 + 1} (ι := ι) (⇑b : (a : ι) → M))) = f.range
⊢ span R (Set.range.{u_4, u_5 + 1} (ι := ι) (⇑(ofIsLocalizedModule Rₛ S f 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]

Premises used: LinearMap.range, Submodule.span, Set.image, Set.range, Submodule.map, Module.Basis.ofIsLocalizedModule, DFunLike.coe
-- Module: Mathlib.RingTheory.Localization.Module
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ₛ
A : Type u_3
inst_4 : CommSemiring A
inst_5 : Algebra R A
Aₛ : Type u_4
inst_6 : CommSemiring Aₛ
inst_7 : Algebra A Aₛ
inst_8 : Algebra Rₛ Aₛ
inst_9 : Algebra R Aₛ
inst_10 : IsScalarTower R Rₛ Aₛ
inst_11 : IsScalarTower R A Aₛ
inst_12 : IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ
ι : Type u_5
v : ι → A
hv : LinearIndependent R v
⊢ LinearIndependent.{u_5, u_2, u_4} Rₛ (M := Aₛ) ((⇑(algebraMap A Aₛ) : (a : A) → Aₛ) ∘ v)

Tactic:
hv.of_isLocalizedModule Rₛ S (IsScalarTower.toAlgHom R A Aₛ).toLinearMap

Premises used: AlgHom.toLinearMap, IsScalarTower.toAlgHom, LinearIndependent.of_isLocalizedModule
-- Module: Mathlib.RingTheory.Localization.Module
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ₛ
A : Type u_3
inst_4 : CommSemiring A
inst_5 : Algebra R A
Aₛ : Type u_4
inst_6 : CommSemiring Aₛ
inst_7 : Algebra A Aₛ
inst_8 : Algebra Rₛ Aₛ
inst_9 : Algebra R Aₛ
inst_10 : IsScalarTower R Rₛ Aₛ
inst_11 : IsScalarTower R A Aₛ
inst_12 : IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ
v : Set A
hv : Eq (α := Submodule R A) (span R v) ⊤
⊢ Eq.{u_4 + 1} (α := Submodule Rₛ Aₛ) (span Rₛ ((⇑(algebraMap A Aₛ) : (a : A) → Aₛ) '' v)) ⊤

Tactic:
span_eq_top_of_isLocalizedModule Rₛ S (IsScalarTower.toAlgHom R A Aₛ).toLinearMap hv

Premises used: AlgHom.toLinearMap, IsScalarTower.toAlgHom, span_eq_top_of_isLocalizedModule
-- Module: Mathlib.RingTheory.Localization.Module
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ₛ
A : Type u_3
inst_4 : CommSemiring A
inst_5 : Algebra R A
Aₛ : Type u_4
inst_6 : CommSemiring Aₛ
inst_7 : Algebra A Aₛ
inst_8 : Algebra Rₛ Aₛ
inst_9 : Algebra R Aₛ
inst_10 : IsScalarTower R Rₛ Aₛ
inst_11 : IsScalarTower R A Aₛ
inst_12 : IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ
ι : Type u_5
b : Basis ι R A
i : ι
⊢ Eq.{u_4 + 1} (α := Aₛ) ((localizationLocalization Rₛ S Aₛ b : (a : ι) → Aₛ) i : Aₛ)
    ((algebraMap A Aₛ : (a : A) → Aₛ) ((b : (a : ι) → A) i : A) : Aₛ)

Tactic:
b.ofIsLocalizedModule_apply Rₛ S _ i

Premises used: Module.Basis.ofIsLocalizedModule_apply
-- Module: Mathlib.RingTheory.Localization.Module
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ₛ
A : Type u_3
inst_4 : CommSemiring A
inst_5 : Algebra R A
Aₛ : Type u_4
inst_6 : CommSemiring Aₛ
inst_7 : Algebra A Aₛ
inst_8 : Algebra Rₛ Aₛ
inst_9 : Algebra R Aₛ
inst_10 : IsScalarTower R Rₛ Aₛ
inst_11 : IsScalarTower R A Aₛ
inst_12 : IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ
ι : Type u_5
b : Basis ι R A
x : A
i : ι
⊢ Eq.{u_2 + 1} (α := Rₛ)
    ((((repr (localizationLocalization Rₛ S Aₛ b) : (a : Aₛ) → ι →₀ Rₛ) ((algebraMap A Aₛ : (a : A) → Aₛ) x) :
            ι →₀ Rₛ) :
          (a : ι) → Rₛ)
        i :
      Rₛ)
    ((algebraMap R Rₛ : (a : R) → Rₛ) ((((b.repr : (a : A) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i : R) : Rₛ)

Tactic:
b.ofIsLocalizedModule_repr_apply Rₛ S _ _ i

Premises used: Module.Basis.ofIsLocalizedModule_repr_apply
-- Module: Mathlib.RingTheory.Localization.Module
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ₛ
A : Type u_3
inst_4 : CommSemiring A
inst_5 : Algebra R A
Aₛ : Type u_4
inst_6 : CommSemiring Aₛ
inst_7 : Algebra A Aₛ
inst_8 : Algebra Rₛ Aₛ
inst_9 : Algebra R Aₛ
inst_10 : IsScalarTower R Rₛ Aₛ
inst_11 : IsScalarTower R A Aₛ
inst_12 : IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ
ι : Type u_5
b : Basis ι R A
⊢ Eq.{u_4 + 1} (α := Submodule R Aₛ)
    (span R (Set.range.{u_4, u_5 + 1} (ι := ι) (⇑(localizationLocalization Rₛ S Aₛ b) : (a : ι) → Aₛ)))
    (LinearMap.range.{u_1, u_1, u_3, u_4} (M := A) (τ₁₂ := RingHom.id R)
      (↑(IsScalarTower.toAlgHom R A Aₛ) :
        [inst_13 : FunLike (A →ₐ[R] Aₛ) A Aₛ] → [SemilinearMapClass (A →ₐ[R] Aₛ) (RingHom.id R) A Aₛ] → A →ₗ[R] Aₛ))

Tactic:
b.ofIsLocalizedModule_span Rₛ S _

Premises used: AlgHom.toLinearMap, SemilinearMapClass.semilinearMap, Module.Basis.ofIsLocalizedModule_span
-- Module: Mathlib.RingTheory.Localization.Module
Goal:
R : Type u_3
K : Type u_4
inst : CommRing R
inst_1 : CommRing K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
V : Type u_5
inst_4 : AddCommGroup V
inst_5 : Module R V
inst_6 : Module K V
inst_7 : IsScalarTower R K V
ι : Type u_6
b : ι → V
⊢ LinearIndependent R b ↔ LinearIndependent K b

Tactic:
⟨.localization K R⁰,
    .restrict_scalars <| (faithfulSMul_iff_injective_smul_one ..).mp inferInstance⟩

Premises used: nonZeroDivisors, inferInstance, LinearIndependent.localization, Iff.intro, Iff.mp, faithfulSMul_iff_injective_smul_one, LinearIndependent.restrict_scalars
-- Module: Mathlib.RingTheory.Localization.Module
Goal:
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
⊢ (↑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 f) =
    f

Tactic:
rfl

Premises used: LinearMap.restrictScalars, rfl
-- Module: Mathlib.RingTheory.Localization.Module
Goal:
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 →ₗ[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₂)
        f) =
    f

Tactic:
rfl

Premises used: LinearMap.extendScalarsOfIsLocalization, rfl
-- Module: Mathlib.RingTheory.Localization.Module
Goal:
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.{u_6 + 1} (α := N) ((extendScalarsOfIsLocalization S A f : (a : M) → N) x : N) ((f : (a : M) → N) x : N)

Tactic:
rfl

Premises used: rfl
-- 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 y : M →ₗ[R] N
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)
⊢ extendScalarsOfIsLocalization S A (x + y) =
    HAdd.hAdd (α := M →ₗ[A] N) (extendScalarsOfIsLocalization S A x) (extendScalarsOfIsLocalization S A y)

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 y : M →ₗ[R] N
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:
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
m : A
x : M →ₗ[R] N
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)
⊢ extendScalarsOfIsLocalization S A (m • x) =
    HSMul.hSMul (α := A) (β := M →ₗ[A] N) ((RingHom.id A : (a : A) → A) m : A) (extendScalarsOfIsLocalization S A 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
m : A
x : M →ₗ[R] N
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:
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
x : M →ₗ[R] N
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)
⊢ (↑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

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 →ₗ[R] N
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:
simp