awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Localization.BaseChange (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : IsLocalization S A
M₁ : Type u_5
M₂ : Type u_6
inst_4 : AddCommMonoid M₁
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₁
inst_7 : Module R M₂
inst_8 : Module A M₁
inst_9 : Module A M₂
inst_10 : IsScalarTower R A M₁
inst_11 : IsScalarTower R A M₂
x : M₁
x_1 : M₂
r : R
s : ↥S
simp_rw :
  HSMul.hSMul (β := M₁ ⊗[R] M₂) (↑s : R) ((mk' A r s • x) ⊗ₜ[R] x_1) =
    HSMul.hSMul (β := M₁ ⊗[R] M₂) (↑s : R) (x ⊗ₜ[R] (mk' A r s • x_1))
simp_rw₁ : Eq (α := M₁ ⊗[R] M₂) (((↑s : R) • mk' A r s • x) ⊗ₜ[R] x_1) (((↑s : R) • x) ⊗ₜ[R] (mk' A r s • x_1))
simp_rw₂ : Eq (α := M₁ ⊗[R] M₂) ((((↑s : R) • mk' A r s) • x) ⊗ₜ[R] x_1) (((↑s : R) • x) ⊗ₜ[R] (mk' A r s • x_1))
simp_rw₃ : Eq (α := M₁ ⊗[R] M₂) ((((↑s : R) • mk' A r s) • x) ⊗ₜ[R] x_1) (x ⊗ₜ[R] ((↑s : R) • mk' A r s • x_1))
⊢ HSMul.hSMul (α := A) (β := M₁ ⊗[R] M₂) ((algebraMap R A : (a : R) → A) (↑s : R) : A) ((mk' A r s • x) ⊗ₜ[R] x_1) =
    HSMul.hSMul (α := A) (β := M₁ ⊗[R] M₂) ((algebraMap R A : (a : R) → A) (↑s : R) : A) (x ⊗ₜ[R] (mk' A r s • x_1))
have simp_rw₄ : Eq (α := M₁ ⊗[R] M₂) ((((↑s : R) • mk' A r s) • x) ⊗ₜ[R] x_1) (x ⊗ₜ[R] (((↑s : R) • mk' A r s) • x_1))
Tactic: simp_rw [algebraMap_smul, smul_tmul', ← smul_assoc, smul_tmul, ← smul_assoc, smul_mk'_self,
      algebraMap_smul, smul_tmul]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.BaseChange (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : IsLocalization S A
M₁ : Type u_5
M₂ : Type u_6
inst_4 : AddCommMonoid M₁
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₁
inst_7 : Module R M₂
inst_8 : Module A M₁
inst_9 : Module A M₂
inst_10 : IsScalarTower R A M₁
inst_11 : IsScalarTower R A M₂
x : M₁
x_1 : M₂
r : R
s : ↥S
simp_rw :
  HSMul.hSMul (β := M₁ ⊗[R] M₂) (↑s : R) ((mk' A r s • x) ⊗ₜ[R] x_1) =
    HSMul.hSMul (β := M₁ ⊗[R] M₂) (↑s : R) (x ⊗ₜ[R] (mk' A r s • x_1))
simp_rw₁ : Eq (α := M₁ ⊗[R] M₂) (((↑s : R) • mk' A r s • x) ⊗ₜ[R] x_1) (((↑s : R) • x) ⊗ₜ[R] (mk' A r s • x_1))
simp_rw₂ : Eq (α := M₁ ⊗[R] M₂) ((((↑s : R) • mk' A r s) • x) ⊗ₜ[R] x_1) (((↑s : R) • x) ⊗ₜ[R] (mk' A r s • x_1))
simp_rw₃ : Eq (α := M₁ ⊗[R] M₂) ((((↑s : R) • mk' A r s) • x) ⊗ₜ[R] x_1) (x ⊗ₜ[R] ((↑s : R) • mk' A r s • x_1))
simp_rw₄ : Eq (α := M₁ ⊗[R] M₂) ((((↑s : R) • mk' A r s) • x) ⊗ₜ[R] x_1) (x ⊗ₜ[R] (((↑s : R) • mk' A r s) • x_1))
⊢ HSMul.hSMul (α := A) (β := M₁ ⊗[R] M₂) ((algebraMap R A : (a : R) → A) (↑s : R) : A) ((mk' A r s • x) ⊗ₜ[R] x_1) =
    HSMul.hSMul (α := A) (β := M₁ ⊗[R] M₂) ((algebraMap R A : (a : R) → A) (↑s : R) : A) (x ⊗ₜ[R] (mk' A r s • x_1))
have simp_rw₅ : Eq (α := M₁ ⊗[R] M₂) (HSMul.hSMul.{u_2, u_5, u_5} (α := A) ((algebraMap R A : (a : R) → A) r : A) x ⊗ₜ[R] x_1)
  (x ⊗ₜ[R] HSMul.hSMul.{u_2, u_6, u_6} (α := A) ((algebraMap R A : (a : R) → A) r : A) x_1)
Tactic: simp_rw [algebraMap_smul, smul_tmul', ← smul_assoc, smul_tmul, ← smul_assoc, smul_mk'_self,
      algebraMap_smul, smul_tmul]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.BaseChange (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : IsLocalization S A
M₁ : Type u_5
M₂ : Type u_6
inst_4 : AddCommMonoid M₁
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₁
inst_7 : Module R M₂
inst_8 : Module A M₁
inst_9 : Module A M₂
inst_10 : IsScalarTower R A M₁
inst_11 : IsScalarTower R A M₂
x : M₁
x_1 : M₂
r : R
s : ↥S
simp_rw :
  HSMul.hSMul (β := M₁ ⊗[R] M₂) (↑s : R) ((mk' A r s • x) ⊗ₜ[R] x_1) =
    HSMul.hSMul (β := M₁ ⊗[R] M₂) (↑s : R) (x ⊗ₜ[R] (mk' A r s • x_1))
simp_rw₁ : Eq (α := M₁ ⊗[R] M₂) (((↑s : R) • mk' A r s • x) ⊗ₜ[R] x_1) (((↑s : R) • x) ⊗ₜ[R] (mk' A r s • x_1))
simp_rw₂ : Eq (α := M₁ ⊗[R] M₂) ((((↑s : R) • mk' A r s) • x) ⊗ₜ[R] x_1) (((↑s : R) • x) ⊗ₜ[R] (mk' A r s • x_1))
simp_rw₃ : Eq (α := M₁ ⊗[R] M₂) ((((↑s : R) • mk' A r s) • x) ⊗ₜ[R] x_1) (x ⊗ₜ[R] ((↑s : R) • mk' A r s • x_1))
simp_rw₄ : Eq (α := M₁ ⊗[R] M₂) ((((↑s : R) • mk' A r s) • x) ⊗ₜ[R] x_1) (x ⊗ₜ[R] (((↑s : R) • mk' A r s) • x_1))
simp_rw₅ :
  Eq (α := M₁ ⊗[R] M₂) (HSMul.hSMul.{u_2, u_5, u_5} (α := A) ((algebraMap R A : (a : R) → A) r : A) x ⊗ₜ[R] x_1)
    (x ⊗ₜ[R] HSMul.hSMul.{u_2, u_6, u_6} (α := A) ((algebraMap R A : (a : R) → A) r : A) x_1)
⊢ HSMul.hSMul (α := A) (β := M₁ ⊗[R] M₂) ((algebraMap R A : (a : R) → A) (↑s : R) : A) ((mk' A r s • x) ⊗ₜ[R] x_1) =
    HSMul.hSMul (α := A) (β := M₁ ⊗[R] M₂) ((algebraMap R A : (a : R) → A) (↑s : R) : A) (x ⊗ₜ[R] (mk' A r s • x_1))
have simp_rw₆ : Eq (α := M₁ ⊗[R] M₂) ((r • x) ⊗ₜ[R] x_1) (x ⊗ₜ[R] (r • x_1))
Tactic: simp_rw [algebraMap_smul, smul_tmul', ← smul_assoc, smul_tmul, ← smul_assoc, smul_mk'_self,
      algebraMap_smul, smul_tmul]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.BaseChange (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : IsLocalization S A
M : Type u_3
inst_4 : AddCommMonoid M
inst_5 : Module R M
M' : Type u_4
inst_6 : AddCommMonoid M'
inst_7 : Module R M'
inst_8 : Module A M'
inst_9 : IsScalarTower R A M'
f : M →ₗ[R] M'
M₁ : Type ?u.68522
M₂ : Type ?u.68525
B : Type ?u.70458
C : Type ?u.70581
inst_10 : AddCommMonoid M₁
inst_11 : AddCommMonoid M₂
inst_12 : Module R M₁
inst_13 : Module R M₂
inst_14 : Module A M₁
inst_15 : Module A M₂
inst_16 : IsScalarTower R A M₁
inst_17 : IsScalarTower R A M₂
inst_18 : Semiring B
inst_19 : Algebra R B
inst_20 : Algebra A B
inst_21 : IsScalarTower R A B
inst_22 : Semiring C
inst_23 : Algebra R C
inst_24 : Algebra A C
inst_25 : IsScalarTower R A C
N : Type u_5
N' : Type u_6
inst_26 : AddCommMonoid N
inst_27 : Module R N
inst_28 : AddCommMonoid N'
inst_29 : Module R N'
g : N →ₗ[R] N'
inst_30 : IsLocalizedModule S f
inst_31 : IsLocalizedModule S g
eM : M' ≃ₗ[R] Localization (M := R) S ⊗[R] M :=
  IsLocalizedModule.linearEquiv S f
    ((mk R (Localization (M := R) S) M : (a : Localization S) → M →ₗ[R] Localization S ⊗[R] M) 1)
eN : N' ≃ₗ[R] Localization (M := R) S ⊗[R] N :=
  IsLocalizedModule.linearEquiv S g
    ((mk R (Localization (M := R) S) N : (a : Localization S) → N →ₗ[R] Localization S ⊗[R] N) 1)
⊢ IsLocalizedModule S (TensorProduct.map f g)
have h : TensorProduct.map f g =
  (↑(LinearEquiv.restrictScalars R (AlgebraTensorModule.distribBaseChange R (Localization (M := R) S) M N) ≪≫ₗ
          LinearEquiv.symm
            (TensorProduct.congr eM eN ≪≫ₗ
              TensorProduct.equivOfCompatibleSMul (Localization (M := R) S) R R (Localization (M := R) S ⊗[R] M)
                (Localization (M := R) S ⊗[R] N))) :
      Localization S ⊗[R] (M ⊗[R] N) →ₗ[R] M' ⊗[R] N') ∘ₗ
    (mk R (Localization (M := R) S) (M ⊗[R] N) : (a : Localization S) → M ⊗[R] N →ₗ[R] Localization S ⊗[R] (M ⊗[R] N)) 1
Tactic: convert!
    IsLocalizedModule.of_linearEquiv S (TensorProduct.mk R (Localization S) (M ⊗[R] N) 1) <|
      (AlgebraTensorModule.distribBaseChange R (Localization S) ..).restrictScalars R ≪≫ₗ
        (congr eM eN ≪≫ₗ TensorProduct.equivOfCompatibleSMul ..).symm
-- Lean 4 proof step from Mathlib.RingTheory.Localization.BaseChange (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : IsLocalization S A
T : Type u_5
B : Type u_6
inst_4 : CommSemiring T
inst_5 : CommSemiring B
inst_6 : Algebra R T
inst_7 : Algebra T B
inst_8 : Algebra R B
inst_9 : Algebra A B
inst_10 : IsScalarTower R T B
inst_11 : IsScalarTower R A B
⊢ IsLocalization (algebraMapSubmonoid T S) B ↔ IsPushout R T A B
have rw : IsLocalizedModule S (AlgHom.toLinearMap (IsScalarTower.toAlgHom R T B)) ↔
  IsBaseChange A (AlgHom.toLinearMap (IsScalarTower.toAlgHom R T B))
Tactic: rw [Algebra.IsPushout.comm, Algebra.isPushout_iff, ← isLocalizedModule_iff_isLocalization]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.BaseChange (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : IsLocalization S A
T : Type u_5
B : Type u_6
inst_4 : CommSemiring T
inst_5 : CommSemiring B
inst_6 : Algebra R T
inst_7 : Algebra T B
inst_8 : Algebra R B
inst_9 : Algebra A B
inst_10 : IsScalarTower R T B
inst_11 : IsScalarTower R A B
⊢ IsLocalizedModule S (AlgHom.toLinearMap (IsScalarTower.toAlgHom R T B)) ↔
    IsBaseChange A (AlgHom.toLinearMap (IsScalarTower.toAlgHom R T B))
have rw : IsLocalizedModule S (AlgHom.toLinearMap (IsScalarTower.toAlgHom R T B)) ↔
  IsLocalizedModule S (AlgHom.toLinearMap (IsScalarTower.toAlgHom R T B))
Tactic: rw [← isLocalizedModule_iff_isBaseChange (S := S)]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.BaseChange (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
T : Type u_5
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : Algebra A T
inst_6 : IsScalarTower R A T
H : Function.Bijective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
⊢ IsPushout R T A T
have this : IsLocalization (IsUnit.submonoid R) A
Tactic: have : IsLocalization (IsUnit.submonoid R) A :=
    IsLocalization.of_le_isUnit_of_bijective Algebra.algebraMapSubmonoid_isUnit_le_isUnit H
-- Lean 4 proof step from Mathlib.RingTheory.Localization.BaseChange (goal)
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
T : Type u_5
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : Algebra A T
inst_6 : IsScalarTower R A T
H : Function.Bijective.{u_2 + 1, u_5 + 1} (α := A) (β := T) (⇑(algebraMap A T) : (a : A) → T)
⊢ IsLocalization (algebraMapSubmonoid A (IsUnit.submonoid R)) T
have apply : LE.le (α := Submonoid T) (algebraMapSubmonoid T (algebraMapSubmonoid A (IsUnit.submonoid R))) (IsUnit.submonoid T)
Tactic: apply IsLocalization.of_le_isUnit_of_bijective _ H
-- Lean 4 proof step from Mathlib.RingTheory.Localization.BaseChange (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
T : Type u_5
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : Algebra A T
inst_6 : IsScalarTower R A T
H : Function.Bijective.{u_2 + 1, u_5 + 1} (α := A) (β := T) (⇑(algebraMap A T) : (a : A) → T)
⊢ IsPushout R A R T
have this : IsLocalization (algebraMapSubmonoid A (IsUnit.submonoid R)) T
Tactic: have : IsLocalization (algebraMapSubmonoid A (IsUnit.submonoid R)) T := by
    apply IsLocalization.of_le_isUnit_of_bijective _ H
    simpa using Algebra.algebraMapSubmonoid_isUnit_le
-- Lean 4 proof step from Mathlib.RingTheory.Localization.BaseChange (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : IsLocalization S A
M : Type u_3
inst_4 : AddCommMonoid M
inst_5 : Module R M
M' : Type u_4
inst_6 : AddCommMonoid M'
inst_7 : Module R M'
inst_8 : Module A M'
inst_9 : IsScalarTower R A M'
f : M →ₗ[R] M'
T : Type u_5
B : Type u_6
inst_10 : CommSemiring T
inst_11 : CommSemiring B
inst_12 : Algebra R T
inst_13 : Algebra T B
inst_14 : Algebra R B
inst_15 : Algebra A B
inst_16 : IsScalarTower R T B
inst_17 : IsScalarTower R A B
α : Type u_7
inst_18 : IsLocalizedModule S f
e : Localization (M := R) S ⊗[R] M ≃ₗ[R] M' :=
  LinearEquiv.restrictScalars R (LinearEquiv.symm (LocalizedModule.equivTensorProduct S M)) ≪≫ₗ
    IsLocalizedModule.iso S f
e' : Localization (M := R) S ⊗[R] (α →₀ M) ≃ₗ[R] α →₀ M' :=
  (finsuppRight R R (Localization (M := R) S) M α :
      Localization (M := R) S ⊗[R] (α →₀ M) ≃ₗ[R] α →₀ Localization (M := R) S ⊗[R] M) ≪≫ₗ
    (Finsupp.mapRange.linearEquiv e : (α →₀ Localization (M := R) S ⊗[R] M) ≃ₗ[R] α →₀ M')
this : IsLocalizedModule S ((↑e'.symm : (α →₀ M') →ₗ[R] Localization S ⊗[R] (α →₀ M)) ∘ₗ Finsupp.mapRange.linearMap f)
⊢ IsLocalizedModule (M := α →₀ M) S (Finsupp.mapRange.linearMap f)
have h : Finsupp.mapRange.linearMap f =
  (↑e' : Localization S ⊗[R] (α →₀ M) →ₗ[R] α →₀ M') ∘ₗ
    (↑e'.symm : (α →₀ M') →ₗ[R] Localization S ⊗[R] (α →₀ M)) ∘ₗ Finsupp.mapRange.linearMap f
Tactic: convert! this.of_linearEquiv (e := e')
-- Lean 4 proof step from Mathlib.RingTheory.Localization.BaseChange (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : IsLocalization S A
M : Type u_3
inst_4 : AddCommMonoid M
inst_5 : Module R M
M' : Type u_4
inst_6 : AddCommMonoid M'
inst_7 : Module R M'
inst_8 : Module A M'
inst_9 : IsScalarTower R A M'
f : M →ₗ[R] M'
T : Type u_5
B : Type u_6
inst_10 : CommSemiring T
inst_11 : CommSemiring B
inst_12 : Algebra R T
inst_13 : Algebra T B
inst_14 : Algebra R B
inst_15 : Algebra A B
inst_16 : IsScalarTower R T B
inst_17 : IsScalarTower R A B
α : Type u_7
inst_18 : IsLocalizedModule S f
e : Localization (M := R) S ⊗[R] M ≃ₗ[R] M' :=
  LinearEquiv.restrictScalars R (LinearEquiv.symm (LocalizedModule.equivTensorProduct S M)) ≪≫ₗ
    IsLocalizedModule.iso S f
e' : Localization (M := R) S ⊗[R] (α →₀ M) ≃ₗ[R] α →₀ M' :=
  (finsuppRight R R (Localization (M := R) S) M α :
      Localization (M := R) S ⊗[R] (α →₀ M) ≃ₗ[R] α →₀ Localization (M := R) S ⊗[R] M) ≪≫ₗ
    (Finsupp.mapRange.linearEquiv e : (α →₀ Localization (M := R) S ⊗[R] M) ≃ₗ[R] α →₀ M')
this : IsLocalizedModule S ((↑e'.symm : (α →₀ M') →ₗ[R] Localization S ⊗[R] (α →₀ M)) ∘ₗ Finsupp.mapRange.linearMap f)
⊢ Finsupp.mapRange.linearMap f =
    (↑e' : Localization S ⊗[R] (α →₀ M) →ₗ[R] α →₀ M') ∘ₗ
      (↑e'.symm : (α →₀ M') →ₗ[R] Localization S ⊗[R] (α →₀ M)) ∘ₗ Finsupp.mapRange.linearMap f
have h : ∀ (a : α) (x : M) (a_1 : α),
  Eq.{u_4 + 1} (α := M')
    ((((Finsupp.mapRange.linearMap f ∘ₗ Finsupp.lsingle a : (a : M) → α →₀ M') x : α →₀ M') : (a : α) → M') a_1 : M')
    ((((((↑e' : Localization S ⊗[R] (α →₀ M) →ₗ[R] α →₀ M') ∘ₗ
                    (↑e'.symm : (α →₀ M') →ₗ[R] Localization S ⊗[R] (α →₀ M)) ∘ₗ Finsupp.mapRange.linearMap f) ∘ₗ
                  Finsupp.lsingle a :
                (a : M) → α →₀ M')
              x :
            α →₀ M') :
          (a : α) → M')
        a_1 :
      M')
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Localization.BaseChange (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : IsLocalization S A
M : Type u_3
inst_4 : AddCommMonoid M
inst_5 : Module R M
M' : Type u_4
inst_6 : AddCommMonoid M'
inst_7 : Module R M'
inst_8 : Module A M'
inst_9 : IsScalarTower R A M'
f : M →ₗ[R] M'
T : Type u_5
B : Type u_6
inst_10 : CommSemiring T
inst_11 : CommSemiring B
inst_12 : Algebra R T
inst_13 : Algebra T B
inst_14 : Algebra R B
inst_15 : Algebra A B
inst_16 : IsScalarTower R T B
inst_17 : IsScalarTower R A B
α : Type u_7
inst_18 : IsLocalizedModule S f
e : Localization (M := R) S ⊗[R] M ≃ₗ[R] M' :=
  LinearEquiv.restrictScalars R (LinearEquiv.symm (LocalizedModule.equivTensorProduct S M)) ≪≫ₗ
    IsLocalizedModule.iso S f
e' : Localization (M := R) S ⊗[R] (α →₀ M) ≃ₗ[R] α →₀ M' :=
  (finsuppRight R R (Localization (M := R) S) M α :
      Localization (M := R) S ⊗[R] (α →₀ M) ≃ₗ[R] α →₀ Localization (M := R) S ⊗[R] M) ≪≫ₗ
    (Finsupp.mapRange.linearEquiv e : (α →₀ Localization (M := R) S ⊗[R] M) ≃ₗ[R] α →₀ M')
⊢ IsLocalizedModule (M := α →₀ M) S (Finsupp.mapRange.linearMap f)
have suffices : IsLocalizedModule S ((↑e'.symm : (α →₀ M') →ₗ[R] Localization S ⊗[R] (α →₀ M)) ∘ₗ Finsupp.mapRange.linearMap f)
Tactic: suffices IsLocalizedModule S (e'.symm.toLinearMap ∘ₗ Finsupp.mapRange.linearMap f) by
    convert! this.of_linearEquiv (e := e')
    ext
    simp
-- Lean 4 proof step from Mathlib.RingTheory.Localization.BaseChange (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : IsLocalization S A
M : Type u_3
inst_4 : AddCommMonoid M
inst_5 : Module R M
M' : Type u_4
inst_6 : AddCommMonoid M'
inst_7 : Module R M'
inst_8 : Module A M'
inst_9 : IsScalarTower R A M'
f : M →ₗ[R] M'
T : Type u_5
B : Type u_6
inst_10 : CommSemiring T
inst_11 : CommSemiring B
inst_12 : Algebra R T
inst_13 : Algebra T B
inst_14 : Algebra R B
inst_15 : Algebra A B
inst_16 : IsScalarTower R T B
inst_17 : IsScalarTower R A B
α : Type u_7
inst_18 : IsLocalizedModule S f
e : Localization (M := R) S ⊗[R] M ≃ₗ[R] M' :=
  LinearEquiv.restrictScalars R (LinearEquiv.symm (LocalizedModule.equivTensorProduct S M)) ≪≫ₗ
    IsLocalizedModule.iso S f
e' : Localization (M := R) S ⊗[R] (α →₀ M) ≃ₗ[R] α →₀ M' :=
  (finsuppRight R R (Localization (M := R) S) M α :
      Localization (M := R) S ⊗[R] (α →₀ M) ≃ₗ[R] α →₀ Localization (M := R) S ⊗[R] M) ≪≫ₗ
    (Finsupp.mapRange.linearEquiv e : (α →₀ Localization (M := R) S ⊗[R] M) ≃ₗ[R] α →₀ M')
⊢ IsLocalizedModule S ((↑e'.symm : (α →₀ M') →ₗ[R] Localization S ⊗[R] (α →₀ M)) ∘ₗ Finsupp.mapRange.linearMap f)
have rw : IsBaseChange (Localization (M := R) S)
  ((↑e'.symm : (α →₀ M') →ₗ[R] Localization S ⊗[R] (α →₀ M)) ∘ₗ Finsupp.mapRange.linearMap f)
Tactic: rw [isLocalizedModule_iff_isBaseChange S (Localization S)]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.BaseChange (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : IsLocalization S A
M : Type u_3
inst_4 : AddCommMonoid M
inst_5 : Module R M
M' : Type u_4
inst_6 : AddCommMonoid M'
inst_7 : Module R M'
inst_8 : Module A M'
inst_9 : IsScalarTower R A M'
f : M →ₗ[R] M'
T : Type u_5
B : Type u_6
inst_10 : CommSemiring T
inst_11 : CommSemiring B
inst_12 : Algebra R T
inst_13 : Algebra T B
inst_14 : Algebra R B
inst_15 : Algebra A B
inst_16 : IsScalarTower R T B
inst_17 : IsScalarTower R A B
α : Type u_7
inst_18 : IsLocalizedModule S f
e : Localization (M := R) S ⊗[R] M ≃ₗ[R] M' :=
  LinearEquiv.restrictScalars R (LinearEquiv.symm (LocalizedModule.equivTensorProduct S M)) ≪≫ₗ
    IsLocalizedModule.iso S f
e' : Localization (M := R) S ⊗[R] (α →₀ M) ≃ₗ[R] α →₀ M' :=
  (finsuppRight R R (Localization (M := R) S) M α :
      Localization (M := R) S ⊗[R] (α →₀ M) ≃ₗ[R] α →₀ Localization (M := R) S ⊗[R] M) ≪≫ₗ
    (Finsupp.mapRange.linearEquiv e : (α →₀ Localization (M := R) S ⊗[R] M) ≃ₗ[R] α →₀ M')
⊢ IsBaseChange (Localization (M := R) S)
    ((↑e'.symm : (α →₀ M') →ₗ[R] Localization S ⊗[R] (α →₀ M)) ∘ₗ Finsupp.mapRange.linearMap f)
have h : (↑e'.symm : (α →₀ M') →ₗ[R] Localization S ⊗[R] (α →₀ M)) ∘ₗ Finsupp.mapRange.linearMap f =
  (mk R (Localization (M := R) S) (α →₀ M) : (a : Localization S) → (α →₀ M) →ₗ[R] Localization S ⊗[R] (α →₀ M)) 1
Tactic: convert! TensorProduct.isBaseChange R (α →₀ M) (Localization S) using 1
-- Lean 4 proof step from Mathlib.RingTheory.Localization.BaseChange (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : IsLocalization S A
M : Type u_3
inst_4 : AddCommMonoid M
inst_5 : Module R M
M' : Type u_4
inst_6 : AddCommMonoid M'
inst_7 : Module R M'
inst_8 : Module A M'
inst_9 : IsScalarTower R A M'
f : M →ₗ[R] M'
T : Type u_5
B : Type u_6
inst_10 : CommSemiring T
inst_11 : CommSemiring B
inst_12 : Algebra R T
inst_13 : Algebra T B
inst_14 : Algebra R B
inst_15 : Algebra A B
inst_16 : IsScalarTower R T B
inst_17 : IsScalarTower R A B
α : Type u_7
inst_18 : IsLocalizedModule S f
e : Localization (M := R) S ⊗[R] M ≃ₗ[R] M' :=
  LinearEquiv.restrictScalars R (LinearEquiv.symm (LocalizedModule.equivTensorProduct S M)) ≪≫ₗ
    IsLocalizedModule.iso S f
e' : Localization (M := R) S ⊗[R] (α →₀ M) ≃ₗ[R] α →₀ M' :=
  (finsuppRight R R (Localization (M := R) S) M α :
      Localization (M := R) S ⊗[R] (α →₀ M) ≃ₗ[R] α →₀ Localization (M := R) S ⊗[R] M) ≪≫ₗ
    (Finsupp.mapRange.linearEquiv e : (α →₀ Localization (M := R) S ⊗[R] M) ≃ₗ[R] α →₀ M')
⊢ (↑e'.symm : (α →₀ M') →ₗ[R] Localization S ⊗[R] (α →₀ M)) ∘ₗ Finsupp.mapRange.linearMap f =
    (mk R (Localization (M := R) S) (α →₀ M) : (a : Localization S) → (α →₀ M) →ₗ[R] Localization S ⊗[R] (α →₀ M)) 1
have h : ∀ (a : α) (m : M),
  Eq (α := Localization (M := R) S ⊗[R] (α →₀ M))
    ((((↑e'.symm : (α →₀ M') →ₗ[R] Localization S ⊗[R] (α →₀ M)) ∘ₗ Finsupp.mapRange.linearMap f) ∘ₗ Finsupp.lsingle a :
          (a : M) → Localization S ⊗[R] (α →₀ M))
        m :
      Localization (M := R) S ⊗[R] (α →₀ M))
    (((mk R (Localization (M := R) S) (α →₀ M) : (a : Localization S) → (α →₀ M) →ₗ[R] Localization S ⊗[R] (α →₀ M))
              1 ∘ₗ
            Finsupp.lsingle a :
          (a : M) → Localization S ⊗[R] (α →₀ M))
        m :
      Localization (M := R) S ⊗[R] (α →₀ M))
Tactic: ext a m
-- Lean 4 proof step from Mathlib.RingTheory.Localization.BaseChange (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : IsLocalization S A
M : Type u_3
inst_4 : AddCommMonoid M
inst_5 : Module R M
M' : Type u_4
inst_6 : AddCommMonoid M'
inst_7 : Module R M'
inst_8 : Module A M'
inst_9 : IsScalarTower R A M'
f : M →ₗ[R] M'
T : Type u_5
B : Type u_6
inst_10 : CommSemiring T
inst_11 : CommSemiring B
inst_12 : Algebra R T
inst_13 : Algebra T B
inst_14 : Algebra R B
inst_15 : Algebra A B
inst_16 : IsScalarTower R T B
inst_17 : IsScalarTower R A B
α : Type u_7
inst_18 : IsLocalizedModule S f
e : Localization (M := R) S ⊗[R] M ≃ₗ[R] M' :=
  LinearEquiv.restrictScalars R (LinearEquiv.symm (LocalizedModule.equivTensorProduct S M)) ≪≫ₗ
    IsLocalizedModule.iso S f
e' : Localization (M := R) S ⊗[R] (α →₀ M) ≃ₗ[R] α →₀ M' :=
  (finsuppRight R R (Localization (M := R) S) M α :
      Localization (M := R) S ⊗[R] (α →₀ M) ≃ₗ[R] α →₀ Localization (M := R) S ⊗[R] M) ≪≫ₗ
    (Finsupp.mapRange.linearEquiv e : (α →₀ Localization (M := R) S ⊗[R] M) ≃ₗ[R] α →₀ M')
a : α
m : M
⊢ Eq (α := Localization (M := R) S ⊗[R] (α →₀ M))
    ((((↑e'.symm : (α →₀ M') →ₗ[R] Localization S ⊗[R] (α →₀ M)) ∘ₗ Finsupp.mapRange.linearMap f) ∘ₗ Finsupp.lsingle a :
          (a : M) → Localization S ⊗[R] (α →₀ M))
        m :
      Localization (M := R) S ⊗[R] (α →₀ M))
    (((mk R (Localization (M := R) S) (α →₀ M) : (a : Localization S) → (α →₀ M) →ₗ[R] Localization S ⊗[R] (α →₀ M))
              1 ∘ₗ
            Finsupp.lsingle a :
          (a : M) → Localization S ⊗[R] (α →₀ M))
        m :
      Localization (M := R) S ⊗[R] (α →₀ M))
have h : Eq (α := α →₀ Localization (M := R) S ⊗[R] M)
  (((finsuppRight R R (Localization (M := R) S) M α :
          Localization (M := R) S ⊗[R] (α →₀ M) ≃ₗ[R] α →₀ Localization (M := R) S ⊗[R] M) :
        (a : Localization S ⊗[R] (α →₀ M)) → α →₀ Localization S ⊗[R] M)
      ((((↑e'.symm : (α →₀ M') →ₗ[R] Localization S ⊗[R] (α →₀ M)) ∘ₗ Finsupp.mapRange.linearMap f) ∘ₗ
            Finsupp.lsingle a :
          (a : M) → Localization S ⊗[R] (α →₀ M))
        m) :
    α →₀ Localization (M := R) S ⊗[R] M)
  (((finsuppRight R R (Localization (M := R) S) M α :
          Localization (M := R) S ⊗[R] (α →₀ M) ≃ₗ[R] α →₀ Localization (M := R) S ⊗[R] M) :
        (a : Localization S ⊗[R] (α →₀ M)) → α →₀ Localization S ⊗[R] M)
      (((mk R (Localization (M := R) S) (α →₀ M) : (a : Localization S) → (α →₀ M) →ₗ[R] Localization S ⊗[R] (α →₀ M))
              1 ∘ₗ
            Finsupp.lsingle a :
          (a : M) → Localization S ⊗[R] (α →₀ M))
        m) :
    α →₀ Localization (M := R) S ⊗[R] M)
Tactic: apply (finsuppRight R R (Localization S) M α).injective