awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ ((↑(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
have 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₁
Tactic: apply IsLocalizedModule.linearMap_ext S g₁ g₂
-- 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
⊢ (((↑(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₁
have 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₁
Tactic: rw [LinearMap.comp_assoc, IsLocalizedModule.iso_symm_comp]
-- 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
⊢ ((↑(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₁
have 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')
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
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)
    (⇑((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')))
have 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')))
Tactic: rw [← LinearMap.coe_restrictScalars R, restrictScalars_map_eq _ g₁ g₂ l]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.NormTrace (goal)
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
⊢ 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ₘ)
have 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ₘ)
Tactic: ext i j
-- Lean 4 proof step from Mathlib.RingTheory.Localization.NormTrace (goal)
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
⊢ 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ₘ)
have 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ₘ)
Tactic: cases subsingleton_or_nontrivial R
-- Lean 4 proof step from Mathlib.RingTheory.Localization.NormTrace (goal)
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ₘ)
⊢ 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ₘ)
have 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ₘ)
Tactic: cases subsingleton_or_nontrivial R
-- Lean 4 proof step from Mathlib.RingTheory.Localization.NormTrace (hypothesis)
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
⊢ 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ₘ)
have this : Subsingleton Rₘ
Tactic: haveI : Subsingleton Rₘ := Module.subsingleton R Rₘ
-- Lean 4 proof step from Mathlib.RingTheory.Localization.NormTrace (goal)
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 : Nontrivial R
b : Basis (Free.ChooseBasisIndex R S) R S := Free.chooseBasis R S
this : DecidableEq (Free.ChooseBasisIndex R S) := Classical.decEq (Free.ChooseBasisIndex R S)
⊢ 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ₘ)
have inr : Eq.{u_3 + 1} (α := Rₘ)
  (Matrix.det.{u_3, u_2} (n := Free.ChooseBasisIndex R S)
      ((leftMulMatrix (Basis.localizationLocalization Rₘ M (A := S) Sₘ b) :
          (a : Sₘ) → Matrix (Free.ChooseBasisIndex R S) (Free.ChooseBasisIndex R S) Rₘ)
        ((algebraMap S Sₘ : (a : S) → Sₘ) a)) :
    Rₘ)
  ((algebraMap R Rₘ : (a : R) → Rₘ) ((norm R : (a : S) → R) a : R) : Rₘ)
Tactic: rw [Algebra.norm_eq_matrix_det (b.localizationLocalization Rₘ M Sₘ),
    Algebra.norm_eq_matrix_det b, RingHom.map_det, ← Algebra.map_leftMulMatrix_localization]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.NormTrace (goal)
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 : Nontrivial R
b : Basis (Free.ChooseBasisIndex R S) R S := Free.chooseBasis R S
this : DecidableEq (Free.ChooseBasisIndex R S) := Classical.decEq (Free.ChooseBasisIndex R S)
inr :
  Eq.{u_3 + 1} (α := Rₘ)
    (Matrix.det.{u_3, u_2} (n := Free.ChooseBasisIndex R S)
        ((leftMulMatrix (Basis.localizationLocalization Rₘ M (A := S) Sₘ b) :
            (a : Sₘ) → Matrix (Free.ChooseBasisIndex R S) (Free.ChooseBasisIndex R S) Rₘ)
          ((algebraMap S Sₘ : (a : S) → Sₘ) a)) :
      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ₘ)
have inr₁ : Eq.{u_3 + 1} (α := Rₘ)
  (Matrix.det.{u_3, u_2} (n := Free.ChooseBasisIndex R S)
      ((leftMulMatrix (Basis.localizationLocalization Rₘ M (A := S) Sₘ b) :
          (a : Sₘ) → Matrix (Free.ChooseBasisIndex R S) (Free.ChooseBasisIndex R S) Rₘ)
        ((algebraMap S Sₘ : (a : S) → Sₘ) a)) :
    Rₘ)
  ((algebraMap R Rₘ : (a : R) → Rₘ)
      (Matrix.det.{u_1, u_2} (n := Free.ChooseBasisIndex R S)
        ((leftMulMatrix b : (a : S) → Matrix (Free.ChooseBasisIndex R S) (Free.ChooseBasisIndex R S) R) a)) :
    Rₘ)
Tactic: rw [Algebra.norm_eq_matrix_det (b.localizationLocalization Rₘ M Sₘ),
    Algebra.norm_eq_matrix_det b, RingHom.map_det, ← Algebra.map_leftMulMatrix_localization]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.NormTrace (goal)
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 : Nontrivial R
b : Basis (Free.ChooseBasisIndex R S) R S := Free.chooseBasis R S
this : DecidableEq (Free.ChooseBasisIndex R S) := Classical.decEq (Free.ChooseBasisIndex R S)
inr :
  Eq.{u_3 + 1} (α := Rₘ)
    (Matrix.det.{u_3, u_2} (n := Free.ChooseBasisIndex R S)
        ((leftMulMatrix (Basis.localizationLocalization Rₘ M (A := S) Sₘ b) :
            (a : Sₘ) → Matrix (Free.ChooseBasisIndex R S) (Free.ChooseBasisIndex R S) Rₘ)
          ((algebraMap S Sₘ : (a : S) → Sₘ) a)) :
      Rₘ)
    ((algebraMap R Rₘ : (a : R) → Rₘ) ((norm R : (a : S) → R) a : R) : Rₘ)
inr₁ :
  Eq.{u_3 + 1} (α := Rₘ)
    (Matrix.det.{u_3, u_2} (n := Free.ChooseBasisIndex R S)
        ((leftMulMatrix (Basis.localizationLocalization Rₘ M (A := S) Sₘ b) :
            (a : Sₘ) → Matrix (Free.ChooseBasisIndex R S) (Free.ChooseBasisIndex R S) Rₘ)
          ((algebraMap S Sₘ : (a : S) → Sₘ) a)) :
      Rₘ)
    ((algebraMap R Rₘ : (a : R) → Rₘ)
        (Matrix.det.{u_1, u_2} (n := Free.ChooseBasisIndex R S)
          ((leftMulMatrix b : (a : S) → Matrix (Free.ChooseBasisIndex R S) (Free.ChooseBasisIndex R S) R) a)) :
      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ₘ)
have inr₂ : Eq.{u_3 + 1} (α := Rₘ)
  (Matrix.det.{u_3, u_2} (n := Free.ChooseBasisIndex R S)
    ((leftMulMatrix (Basis.localizationLocalization Rₘ M (A := S) Sₘ b) :
        (a : Sₘ) → Matrix (Free.ChooseBasisIndex R S) (Free.ChooseBasisIndex R S) Rₘ)
      ((algebraMap S Sₘ : (a : S) → Sₘ) a)))
  (Matrix.det.{u_3, u_2} (n := Free.ChooseBasisIndex R S)
    ((RingHom.mapMatrix (algebraMap R Rₘ) :
        (a : Matrix (Free.ChooseBasisIndex R S) (Free.ChooseBasisIndex R S) R) →
          Matrix (Free.ChooseBasisIndex R S) (Free.ChooseBasisIndex R S) Rₘ)
      ((leftMulMatrix b : (a : S) → Matrix (Free.ChooseBasisIndex R S) (Free.ChooseBasisIndex R S) R) a)))
Tactic: rw [Algebra.norm_eq_matrix_det (b.localizationLocalization Rₘ M Sₘ),
    Algebra.norm_eq_matrix_det b, RingHom.map_det, ← Algebra.map_leftMulMatrix_localization]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.NormTrace (goal)
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
⊢ Eq.{u_3 + 1} (α := Rₘ) ((trace Rₘ Sₘ : (a : Sₘ) → Rₘ) ((algebraMap S Sₘ : (a : S) → Sₘ) a : Sₘ) : Rₘ)
    ((algebraMap R Rₘ : (a : R) → Rₘ) ((trace R S : (a : S) → R) a : R) : Rₘ)
have inl : Subsingleton R →
  Eq.{u_3 + 1} (α := Rₘ) ((trace Rₘ Sₘ : (a : Sₘ) → Rₘ) ((algebraMap S Sₘ : (a : S) → Sₘ) a : Sₘ) : Rₘ)
    ((algebraMap R Rₘ : (a : R) → Rₘ) ((trace R S : (a : S) → R) a : R) : Rₘ)
Tactic: cases subsingleton_or_nontrivial R
-- Lean 4 proof step from Mathlib.RingTheory.Localization.NormTrace (goal)
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ₘ) ((trace Rₘ Sₘ : (a : Sₘ) → Rₘ) ((algebraMap S Sₘ : (a : S) → Sₘ) a : Sₘ) : Rₘ)
      ((algebraMap R Rₘ : (a : R) → Rₘ) ((trace R S : (a : S) → R) a : R) : Rₘ)
⊢ Eq.{u_3 + 1} (α := Rₘ) ((trace Rₘ Sₘ : (a : Sₘ) → Rₘ) ((algebraMap S Sₘ : (a : S) → Sₘ) a : Sₘ) : Rₘ)
    ((algebraMap R Rₘ : (a : R) → Rₘ) ((trace R S : (a : S) → R) a : R) : Rₘ)
have inr : Nontrivial R →
  Eq.{u_3 + 1} (α := Rₘ) ((trace Rₘ Sₘ : (a : Sₘ) → Rₘ) ((algebraMap S Sₘ : (a : S) → Sₘ) a : Sₘ) : Rₘ)
    ((algebraMap R Rₘ : (a : R) → Rₘ) ((trace R S : (a : S) → R) a : R) : Rₘ)
Tactic: cases subsingleton_or_nontrivial R
-- Lean 4 proof step from Mathlib.RingTheory.Localization.NormTrace (hypothesis)
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
⊢ Eq.{u_3 + 1} (α := Rₘ) ((trace Rₘ Sₘ : (a : Sₘ) → Rₘ) ((algebraMap S Sₘ : (a : S) → Sₘ) a : Sₘ) : Rₘ)
    ((algebraMap R Rₘ : (a : R) → Rₘ) ((trace R S : (a : S) → R) a : R) : Rₘ)
have this : Subsingleton Rₘ
Tactic: haveI : Subsingleton Rₘ := Module.subsingleton R Rₘ