awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑l : (a : M) → N)
⊢ Function.Surjective (α := 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_surjective S (mkLinearMap S M) (mkLinearMap S N) l hl

Premises used: LocalizedModule.liftOn, LocalizedModule.mkLinearMap, LocalizedModule.lift', IsLocalizedModule.map_surjective
-- 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_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
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
⊢ (↑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')

Tactic:
rw [LinearEquiv.eq_toLinearMap_symm_comp, ← LinearEquiv.comp_toLinearMap_symm_eq]

Premises used: LinearEquiv.comp_toLinearMap_symm_eq, LinearEquiv.eq_toLinearMap_symm_comp
-- 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_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
h :
  (((↑(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)) ∘ₗ
      g₁ =
    (IsLocalizedModule.map S g₁ g₂ : (a : M →ₗ[R] N) → M' →ₗ[R] N') l ∘ₗ g₁
⊢ ((↑(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:
apply IsLocalizedModule.linearMap_ext S g₁ g₂

Premises used: IsLocalizedModule.linearMap_ext
-- 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_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
h :
  ((↑(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)) ∘ₗ
      mkLinearMap S M =
    (IsLocalizedModule.map S g₁ g₂ : (a : M →ₗ[R] N) → M' →ₗ[R] N') l ∘ₗ g₁
⊢ (((↑(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)) ∘ₗ
      g₁ =
    (IsLocalizedModule.map S g₁ g₂ : (a : M →ₗ[R] N) → M' →ₗ[R] N') l ∘ₗ g₁

Tactic:
rw [LinearMap.comp_assoc, IsLocalizedModule.iso_symm_comp]

Premises used: LinearMap.comp_assoc, IsLocalizedModule.iso_symm_comp
-- 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_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
h :
  ∀ (x : M),
    Eq.{u_4 + 1} (α := N')
      ((((↑(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)) ∘ₗ
              mkLinearMap S M :
            (a : M) → N')
          x :
        N')
      (((IsLocalizedModule.map S g₁ g₂ : (a : M →ₗ[R] N) → M' →ₗ[R] N') l ∘ₗ g₁ : (a : M) → N') x : N')
⊢ ((↑(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)) ∘ₗ
      mkLinearMap S M =
    (IsLocalizedModule.map S g₁ g₂ : (a : M →ₗ[R] N) → M' →ₗ[R] N') l ∘ₗ g₁

Tactic:
ext
-- 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_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
x : M
⊢ Eq.{u_4 + 1} (α := N')
    ((((↑(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)) ∘ₗ
            mkLinearMap S M :
          (a : M) → N')
        x :
      N')
    (((IsLocalizedModule.map S g₁ g₂ : (a : M →ₗ[R] N) → M' →ₗ[R] N') l ∘ₗ g₁ : (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
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
rw :
  Eq (α := (a : LocalizedModule S M) → LocalizedModule S N)
    (⇑((↑(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')) :
      (a : LocalizedModule S M) → LocalizedModule S N)
    (Function.comp (β := N') (⇑(IsLocalizedModule.iso S g₂).symm : (a : N') → LocalizedModule S N)
      (Function.comp (β := M')
        (⇑((IsLocalizedModule.map S g₁ g₂ : (a : M →ₗ[R] N) → M' →ₗ[R] N') l : M' →ₗ[R] N') : (a : M') → N')
        (⇑(IsLocalizedModule.iso S g₁) : (a : LocalizedModule S M) → M')))
⊢ Eq (α := (a : 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)
    (Function.comp (β := N') (⇑(IsLocalizedModule.iso S g₂).symm : (a : N') → LocalizedModule S N)
      (Function.comp (β := M')
        (⇑((IsLocalizedModule.map S g₁ g₂ : (a : M →ₗ[R] N) → M' →ₗ[R] N') l : M' →ₗ[R] N') : (a : M') → N')
        (⇑(IsLocalizedModule.iso S g₁) : (a : LocalizedModule S M) → M')))

Tactic:
rw [← LinearMap.coe_restrictScalars R, restrictScalars_map_eq _ g₁ g₂ l]

Premises used: LocalizedModule.restrictScalars_map_eq, LinearMap.coe_restrictScalars
-- 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_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
⊢ Eq (α := (a : LocalizedModule S M) → LocalizedModule S N)
    (⇑((↑(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')) :
      (a : LocalizedModule S M) → LocalizedModule S N)
    (Function.comp (β := N') (⇑(IsLocalizedModule.iso S g₂).symm : (a : N') → LocalizedModule S N)
      (Function.comp (β := M')
        (⇑((IsLocalizedModule.map S g₁ g₂ : (a : M →ₗ[R] N) → M' →ₗ[R] N') l : M' →ₗ[R] N') : (a : M') → N')
        (⇑(IsLocalizedModule.iso S g₁) : (a : LocalizedModule S M) → M')))

Tactic:
simp
-- Module: Mathlib.RingTheory.Localization.Module
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
M' : Type u_4
N' : Type u_5
inst : CommSemiring R
S : Submonoid R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : AddCommMonoid M'
inst_6 : Module R M'
inst_7 : AddCommMonoid N'
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
⊢ Function.Injective.{u_4 + 1, u_5 + 1} (α := M') (β := N')
      (⇑((map S g₁ g₂ : (a : M →ₗ[R] N) → M' →ₗ[R] N') l : M' →ₗ[R] N') : (a : M') → N') ↔
    Function.Injective (α := LocalizedModule S M) (β := LocalizedModule S N)
      (⇑((LocalizedModule.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:
simp [LocalizedModule.coe_map_eq g₁ g₂]

Premises used: LocalizedModule.coe_map_eq
-- Module: Mathlib.RingTheory.Localization.Module
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
M' : Type u_4
N' : Type u_5
inst : CommSemiring R
S : Submonoid R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : AddCommMonoid M'
inst_6 : Module R M'
inst_7 : AddCommMonoid N'
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
⊢ Function.Surjective.{u_4 + 1, u_5 + 1} (α := M') (β := N')
      (⇑((map S g₁ g₂ : (a : M →ₗ[R] N) → M' →ₗ[R] N') l : M' →ₗ[R] N') : (a : M') → N') ↔
    Function.Surjective (α := LocalizedModule S M) (β := LocalizedModule S N)
      (⇑((LocalizedModule.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:
simp [LocalizedModule.coe_map_eq g₁ g₂]

Premises used: LocalizedModule.coe_map_eq
-- Module: Mathlib.RingTheory.Localization.Module
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
M' : Type u_4
N' : Type u_5
inst : CommSemiring R
S : Submonoid R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : AddCommMonoid M'
inst_6 : Module R M'
inst_7 : AddCommMonoid N'
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
⊢ Function.Bijective.{u_4 + 1, u_5 + 1} (α := M') (β := N')
      (⇑((map S g₁ g₂ : (a : M →ₗ[R] N) → M' →ₗ[R] N') l : M' →ₗ[R] N') : (a : M') → N') ↔
    Function.Bijective (α := LocalizedModule S M) (β := LocalizedModule S N)
      (⇑((LocalizedModule.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:
simp [LocalizedModule.coe_map_eq g₁ g₂]

Premises used: LocalizedModule.coe_map_eq
-- Module: Mathlib.RingTheory.Localization.NormTrace
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
Rₘ : Type u_3
Sₘ : Type u_4
inst_3 : CommRing Rₘ
inst_4 : Algebra R Rₘ
inst_5 : CommRing Sₘ
inst_6 : Algebra S Sₘ
M : Submonoid R
inst_7 : IsLocalization M Rₘ
inst_8 : IsLocalization (algebraMapSubmonoid S M) Sₘ
inst_9 : Algebra Rₘ Sₘ
inst_10 : Algebra R Sₘ
inst_11 : IsScalarTower R Rₘ Sₘ
inst_12 : IsScalarTower R S Sₘ
ι : Type u_5
inst_13 : Fintype ι
inst_14 : DecidableEq ι
b : Basis ι R S
a : S
a₁ :
  ∀ (i j : ι),
    Eq.{u_3 + 1} (α := Rₘ)
      ((RingHom.mapMatrix (algebraMap R Rₘ) : (a : Matrix ι ι R) → Matrix ι ι Rₘ)
          ((leftMulMatrix b : (a : S) → Matrix ι ι R) a) i j :
        Rₘ)
      ((leftMulMatrix (Basis.localizationLocalization.{u_1, u_3, u_2, u_4, u_5} Rₘ M (A := S) Sₘ b) :
            (a : Sₘ) → Matrix ι ι Rₘ)
          ((algebraMap S Sₘ : (a : S) → Sₘ) a) i j :
        Rₘ)
⊢ Eq (α := Matrix ι ι Rₘ)
    ((RingHom.mapMatrix (algebraMap R Rₘ) : (a : Matrix ι ι R) → Matrix ι ι Rₘ)
        ((leftMulMatrix b : (a : S) → Matrix ι ι R) a) :
      Matrix ι ι Rₘ)
    ((leftMulMatrix (Basis.localizationLocalization.{u_1, u_3, u_2, u_4, u_5} Rₘ M (A := S) Sₘ b) :
          (a : Sₘ) → Matrix ι ι Rₘ)
        ((algebraMap S Sₘ : (a : S) → Sₘ) a) :
      Matrix ι ι Rₘ)

Tactic:
ext i j
-- Module: Mathlib.RingTheory.Localization.NormTrace
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
Rₘ : Type u_3
Sₘ : Type u_4
inst_3 : CommRing Rₘ
inst_4 : Algebra R Rₘ
inst_5 : CommRing Sₘ
inst_6 : Algebra S Sₘ
M : Submonoid R
inst_7 : IsLocalization M Rₘ
inst_8 : IsLocalization (algebraMapSubmonoid S M) Sₘ
inst_9 : Algebra Rₘ Sₘ
inst_10 : Algebra R Sₘ
inst_11 : IsScalarTower R Rₘ Sₘ
inst_12 : IsScalarTower R S Sₘ
ι : Type u_5
inst_13 : Fintype ι
inst_14 : DecidableEq ι
b : Basis ι R S
a : S
i j : ι
⊢ Eq.{u_3 + 1} (α := Rₘ)
    ((RingHom.mapMatrix (algebraMap R Rₘ) : (a : Matrix ι ι R) → Matrix ι ι Rₘ)
        ((leftMulMatrix b : (a : S) → Matrix ι ι R) a) i j :
      Rₘ)
    ((leftMulMatrix (Basis.localizationLocalization.{u_1, u_3, u_2, u_4, u_5} Rₘ M (A := S) Sₘ b) :
          (a : Sₘ) → Matrix ι ι Rₘ)
        ((algebraMap S Sₘ : (a : S) → Sₘ) a) i j :
      Rₘ)

Tactic:
simp only [Matrix.map_apply, RingHom.mapMatrix_apply, leftMulMatrix_eq_repr_mul, ← map_mul,
    Basis.localizationLocalization_apply, Basis.localizationLocalization_repr_algebraMap]

Premises used: RingHom.mapMatrix_apply, Module.Basis.localizationLocalization_apply, Matrix.map_apply, Module.Basis.localizationLocalization_repr_algebraMap, map_mul, Algebra.leftMulMatrix_eq_repr_mul
-- Module: Mathlib.RingTheory.Localization.NormTrace
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
Rₘ : Type u_3
Sₘ : Type u_4
inst_3 : CommRing Rₘ
inst_4 : Algebra R Rₘ
inst_5 : CommRing Sₘ
inst_6 : Algebra S Sₘ
M : Submonoid R
inst_7 : IsLocalization M Rₘ
inst_8 : IsLocalization (algebraMapSubmonoid S M) Sₘ
inst_9 : Algebra Rₘ Sₘ
inst_10 : Algebra R Sₘ
inst_11 : IsScalarTower R Rₘ Sₘ
inst_12 : IsScalarTower R S Sₘ
inst_13 : Free R S
inst_14 : Module.Finite R S
a : S
inl :
  Subsingleton R →
    Eq.{u_3 + 1} (α := Rₘ) ((norm Rₘ : (a : Sₘ) → Rₘ) ((algebraMap S Sₘ : (a : S) → Sₘ) a : Sₘ) : Rₘ)
      ((algebraMap R Rₘ : (a : R) → Rₘ) ((norm R : (a : S) → R) a : R) : Rₘ)
inr :
  Nontrivial R →
    Eq.{u_3 + 1} (α := Rₘ) ((norm Rₘ : (a : Sₘ) → Rₘ) ((algebraMap S Sₘ : (a : S) → Sₘ) a : Sₘ) : Rₘ)
      ((algebraMap R Rₘ : (a : R) → Rₘ) ((norm R : (a : S) → R) a : R) : Rₘ)
⊢ Eq.{u_3 + 1} (α := Rₘ) ((norm Rₘ : (a : Sₘ) → Rₘ) ((algebraMap S Sₘ : (a : S) → Sₘ) a : Sₘ) : Rₘ)
    ((algebraMap R Rₘ : (a : R) → Rₘ) ((norm R : (a : S) → R) a : R) : Rₘ)

Tactic:
cases subsingleton_or_nontrivial R

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.RingTheory.Localization.NormTrace
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
Rₘ : Type u_3
Sₘ : Type u_4
inst_3 : CommRing Rₘ
inst_4 : Algebra R Rₘ
inst_5 : CommRing Sₘ
inst_6 : Algebra S Sₘ
M : Submonoid R
inst_7 : IsLocalization M Rₘ
inst_8 : IsLocalization (algebraMapSubmonoid S M) Sₘ
inst_9 : Algebra Rₘ Sₘ
inst_10 : Algebra R Sₘ
inst_11 : IsScalarTower R Rₘ Sₘ
inst_12 : IsScalarTower R S Sₘ
inst_13 : Free R S
inst_14 : Module.Finite R S
a : S
h : Subsingleton R
⊢ Subsingleton Rₘ

Tactic:
haveI : Subsingleton Rₘ := Module.subsingleton R Rₘ