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_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'
h : IsBaseChange A f
this_1 : Module A (LocalizedModule S M) := LocalizedModule.moduleOfIsLocalization
this : IsBaseChange (N := LocalizedModule S M) A (LocalizedModule.mkLinearMap S M)
e : LocalizedModule S M ≃ₗ[R] M' := LinearEquiv.restrictScalars R (this.equiv.symm ≪≫ₗ h.equiv)
x : M
h₁ :
  Eq.{u_4 + 1} (α := M') ((f : (a : M) → M') x : M')
    (Function.comp (β := LocalizedModule S M) (⇑(↑e : LocalizedModule S M →ₗ[R] M') : (a : LocalizedModule S M) → M')
        (⇑(LocalizedModule.mkLinearMap S M) : (a : M) → LocalizedModule S M) x :
      M')
⊢ Eq.{u_4 + 1} (α := M') ((f : (a : M) → M') x : M')
    (((↑e : LocalizedModule S M →ₗ[R] M') ∘ₗ LocalizedModule.mkLinearMap S M : (a : M) → M') x : M')
have h₂ : Eq.{u_4 + 1} (α := M') ((f : (a : M) → M') x : M')
  (Function.comp (β := LocalizedModule S M) (⇑e : (a : LocalizedModule S M) → M')
      (⇑(LocalizedModule.mkLinearMap S M) : (a : M) → LocalizedModule S M) x :
    M')
Tactic: rw [LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply,
    LinearEquiv.restrictScalars_apply, LinearEquiv.trans_apply, IsBaseChange.equiv_symm_apply,
    IsBaseChange.equiv_tmul, one_smul]
-- 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'
h : IsBaseChange A f
this_1 : Module A (LocalizedModule S M) := LocalizedModule.moduleOfIsLocalization
this : IsBaseChange (N := LocalizedModule S M) A (LocalizedModule.mkLinearMap S M)
e : LocalizedModule S M ≃ₗ[R] M' := LinearEquiv.restrictScalars R (this.equiv.symm ≪≫ₗ h.equiv)
x : M
h₁ :
  Eq.{u_4 + 1} (α := M') ((f : (a : M) → M') x : M')
    (Function.comp (β := LocalizedModule S M) (⇑(↑e : LocalizedModule S M →ₗ[R] M') : (a : LocalizedModule S M) → M')
        (⇑(LocalizedModule.mkLinearMap S M) : (a : M) → LocalizedModule S M) x :
      M')
h₂ :
  Eq.{u_4 + 1} (α := M') ((f : (a : M) → M') x : M')
    (Function.comp (β := LocalizedModule S M) (⇑e : (a : LocalizedModule S M) → M')
        (⇑(LocalizedModule.mkLinearMap S M) : (a : M) → LocalizedModule S M) x :
      M')
⊢ Eq.{u_4 + 1} (α := M') ((f : (a : M) → M') x : M')
    (((↑e : LocalizedModule S M →ₗ[R] M') ∘ₗ LocalizedModule.mkLinearMap S M : (a : M) → M') x : M')
have h₃ : Eq.{u_4 + 1} (α := M') ((f : (a : M) → M') x : M')
  ((e : (a : LocalizedModule S M) → M')
      ((LocalizedModule.mkLinearMap S M : (a : M) → LocalizedModule S M) x : LocalizedModule S M) :
    M')
Tactic: rw [LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply,
    LinearEquiv.restrictScalars_apply, LinearEquiv.trans_apply, IsBaseChange.equiv_symm_apply,
    IsBaseChange.equiv_tmul, one_smul]
-- 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'
h : IsBaseChange A f
this_1 : Module A (LocalizedModule S M) := LocalizedModule.moduleOfIsLocalization
this : IsBaseChange (N := LocalizedModule S M) A (LocalizedModule.mkLinearMap S M)
e : LocalizedModule S M ≃ₗ[R] M' := LinearEquiv.restrictScalars R (this.equiv.symm ≪≫ₗ h.equiv)
x : M
h₁ :
  Eq.{u_4 + 1} (α := M') ((f : (a : M) → M') x : M')
    (Function.comp (β := LocalizedModule S M) (⇑(↑e : LocalizedModule S M →ₗ[R] M') : (a : LocalizedModule S M) → M')
        (⇑(LocalizedModule.mkLinearMap S M) : (a : M) → LocalizedModule S M) x :
      M')
h₂ :
  Eq.{u_4 + 1} (α := M') ((f : (a : M) → M') x : M')
    (Function.comp (β := LocalizedModule S M) (⇑e : (a : LocalizedModule S M) → M')
        (⇑(LocalizedModule.mkLinearMap S M) : (a : M) → LocalizedModule S M) x :
      M')
h₃ :
  Eq.{u_4 + 1} (α := M') ((f : (a : M) → M') x : M')
    ((e : (a : LocalizedModule S M) → M')
        ((LocalizedModule.mkLinearMap S M : (a : M) → LocalizedModule S M) x : LocalizedModule S M) :
      M')
⊢ Eq.{u_4 + 1} (α := M') ((f : (a : M) → M') x : M')
    (((↑e : LocalizedModule S M →ₗ[R] M') ∘ₗ LocalizedModule.mkLinearMap S M : (a : M) → M') x : M')
have h₄ : Eq.{u_4 + 1} (α := M') ((f : (a : M) → M') x : M')
  ((this.equiv.symm ≪≫ₗ h.equiv : (a : LocalizedModule S M) → M')
      ((LocalizedModule.mkLinearMap S M : (a : M) → LocalizedModule S M) x : LocalizedModule S M) :
    M')
Tactic: rw [LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply,
    LinearEquiv.restrictScalars_apply, LinearEquiv.trans_apply, IsBaseChange.equiv_symm_apply,
    IsBaseChange.equiv_tmul, one_smul]
-- 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'
h : IsBaseChange A f
this_1 : Module A (LocalizedModule S M) := LocalizedModule.moduleOfIsLocalization
this : IsBaseChange (N := LocalizedModule S M) A (LocalizedModule.mkLinearMap S M)
e : LocalizedModule S M ≃ₗ[R] M' := LinearEquiv.restrictScalars R (this.equiv.symm ≪≫ₗ h.equiv)
x : M
h₁ :
  Eq.{u_4 + 1} (α := M') ((f : (a : M) → M') x : M')
    (Function.comp (β := LocalizedModule S M) (⇑(↑e : LocalizedModule S M →ₗ[R] M') : (a : LocalizedModule S M) → M')
        (⇑(LocalizedModule.mkLinearMap S M) : (a : M) → LocalizedModule S M) x :
      M')
h₂ :
  Eq.{u_4 + 1} (α := M') ((f : (a : M) → M') x : M')
    (Function.comp (β := LocalizedModule S M) (⇑e : (a : LocalizedModule S M) → M')
        (⇑(LocalizedModule.mkLinearMap S M) : (a : M) → LocalizedModule S M) x :
      M')
h₃ :
  Eq.{u_4 + 1} (α := M') ((f : (a : M) → M') x : M')
    ((e : (a : LocalizedModule S M) → M')
        ((LocalizedModule.mkLinearMap S M : (a : M) → LocalizedModule S M) x : LocalizedModule S M) :
      M')
h₄ :
  Eq.{u_4 + 1} (α := M') ((f : (a : M) → M') x : M')
    ((this.equiv.symm ≪≫ₗ h.equiv : (a : LocalizedModule S M) → M')
        ((LocalizedModule.mkLinearMap S M : (a : M) → LocalizedModule S M) x : LocalizedModule S M) :
      M')
⊢ Eq.{u_4 + 1} (α := M') ((f : (a : M) → M') x : M')
    (((↑e : LocalizedModule S M →ₗ[R] M') ∘ₗ LocalizedModule.mkLinearMap S M : (a : M) → M') x : M')
have h₅ : Eq.{u_4 + 1} (α := M') ((f : (a : M) → M') x : M')
  ((h.equiv : (a : TensorProduct R A M) → M')
      ((this.equiv.symm : (a : LocalizedModule S M) → TensorProduct R A M)
          ((LocalizedModule.mkLinearMap S M : (a : M) → LocalizedModule S M) x) :
        TensorProduct R A M) :
    M')
Tactic: rw [LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply,
    LinearEquiv.restrictScalars_apply, LinearEquiv.trans_apply, IsBaseChange.equiv_symm_apply,
    IsBaseChange.equiv_tmul, one_smul]
-- 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'
h : IsBaseChange A f
this_1 : Module A (LocalizedModule S M) := LocalizedModule.moduleOfIsLocalization
this : IsBaseChange (N := LocalizedModule S M) A (LocalizedModule.mkLinearMap S M)
e : LocalizedModule S M ≃ₗ[R] M' := LinearEquiv.restrictScalars R (this.equiv.symm ≪≫ₗ h.equiv)
x : M
h₁ :
  Eq.{u_4 + 1} (α := M') ((f : (a : M) → M') x : M')
    (Function.comp (β := LocalizedModule S M) (⇑(↑e : LocalizedModule S M →ₗ[R] M') : (a : LocalizedModule S M) → M')
        (⇑(LocalizedModule.mkLinearMap S M) : (a : M) → LocalizedModule S M) x :
      M')
h₂ :
  Eq.{u_4 + 1} (α := M') ((f : (a : M) → M') x : M')
    (Function.comp (β := LocalizedModule S M) (⇑e : (a : LocalizedModule S M) → M')
        (⇑(LocalizedModule.mkLinearMap S M) : (a : M) → LocalizedModule S M) x :
      M')
h₃ :
  Eq.{u_4 + 1} (α := M') ((f : (a : M) → M') x : M')
    ((e : (a : LocalizedModule S M) → M')
        ((LocalizedModule.mkLinearMap S M : (a : M) → LocalizedModule S M) x : LocalizedModule S M) :
      M')
h₄ :
  Eq.{u_4 + 1} (α := M') ((f : (a : M) → M') x : M')
    ((this.equiv.symm ≪≫ₗ h.equiv : (a : LocalizedModule S M) → M')
        ((LocalizedModule.mkLinearMap S M : (a : M) → LocalizedModule S M) x : LocalizedModule S M) :
      M')
h₅ :
  Eq.{u_4 + 1} (α := M') ((f : (a : M) → M') x : M')
    ((h.equiv : (a : TensorProduct R A M) → M')
        ((this.equiv.symm : (a : LocalizedModule S M) → TensorProduct R A M)
            ((LocalizedModule.mkLinearMap S M : (a : M) → LocalizedModule S M) x) :
          TensorProduct R A M) :
      M')
⊢ Eq.{u_4 + 1} (α := M') ((f : (a : M) → M') x : M')
    (((↑e : LocalizedModule S M →ₗ[R] M') ∘ₗ LocalizedModule.mkLinearMap S M : (a : M) → M') x : M')
have h₆ : Eq.{u_4 + 1} (α := M') ((f : (a : M) → M') x : M') ((h.equiv : (a : TensorProduct R A M) → M') (1 ⊗ₜ[R] x) : M')
Tactic: rw [LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply,
    LinearEquiv.restrictScalars_apply, LinearEquiv.trans_apply, IsBaseChange.equiv_symm_apply,
    IsBaseChange.equiv_tmul, one_smul]
-- 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'
h : IsBaseChange A f
this_1 : Module A (LocalizedModule S M) := LocalizedModule.moduleOfIsLocalization
this : IsBaseChange (N := LocalizedModule S M) A (LocalizedModule.mkLinearMap S M)
e : LocalizedModule S M ≃ₗ[R] M' := LinearEquiv.restrictScalars R (this.equiv.symm ≪≫ₗ h.equiv)
x : M
h₁ :
  Eq.{u_4 + 1} (α := M') ((f : (a : M) → M') x : M')
    (Function.comp (β := LocalizedModule S M) (⇑(↑e : LocalizedModule S M →ₗ[R] M') : (a : LocalizedModule S M) → M')
        (⇑(LocalizedModule.mkLinearMap S M) : (a : M) → LocalizedModule S M) x :
      M')
h₂ :
  Eq.{u_4 + 1} (α := M') ((f : (a : M) → M') x : M')
    (Function.comp (β := LocalizedModule S M) (⇑e : (a : LocalizedModule S M) → M')
        (⇑(LocalizedModule.mkLinearMap S M) : (a : M) → LocalizedModule S M) x :
      M')
h₃ :
  Eq.{u_4 + 1} (α := M') ((f : (a : M) → M') x : M')
    ((e : (a : LocalizedModule S M) → M')
        ((LocalizedModule.mkLinearMap S M : (a : M) → LocalizedModule S M) x : LocalizedModule S M) :
      M')
h₄ :
  Eq.{u_4 + 1} (α := M') ((f : (a : M) → M') x : M')
    ((this.equiv.symm ≪≫ₗ h.equiv : (a : LocalizedModule S M) → M')
        ((LocalizedModule.mkLinearMap S M : (a : M) → LocalizedModule S M) x : LocalizedModule S M) :
      M')
h₅ :
  Eq.{u_4 + 1} (α := M') ((f : (a : M) → M') x : M')
    ((h.equiv : (a : TensorProduct R A M) → M')
        ((this.equiv.symm : (a : LocalizedModule S M) → TensorProduct R A M)
            ((LocalizedModule.mkLinearMap S M : (a : M) → LocalizedModule S M) x) :
          TensorProduct R A M) :
      M')
h₆ : Eq.{u_4 + 1} (α := M') ((f : (a : M) → M') x : M') ((h.equiv : (a : TensorProduct R A M) → M') (1 ⊗ₜ[R] x) : M')
⊢ Eq.{u_4 + 1} (α := M') ((f : (a : M) → M') x : M')
    (((↑e : LocalizedModule S M →ₗ[R] M') ∘ₗ LocalizedModule.mkLinearMap S M : (a : M) → M') x : M')
have h₇ : (f : (a : M) → M') x = HSMul.hSMul.{u_2, u_4, u_4} (α := A) (β := M') 1 ((f : (a : M) → M') x : M')
Tactic: rw [LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply,
    LinearEquiv.restrictScalars_apply, LinearEquiv.trans_apply, IsBaseChange.equiv_symm_apply,
    IsBaseChange.equiv_tmul, one_smul]
-- 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'
h : IsBaseChange A f
this_1 : Module A (LocalizedModule S M) := LocalizedModule.moduleOfIsLocalization
this : IsBaseChange (N := LocalizedModule S M) A (LocalizedModule.mkLinearMap S M)
e : LocalizedModule S M ≃ₗ[R] M' := LinearEquiv.restrictScalars R (this.equiv.symm ≪≫ₗ h.equiv)
x : M
h₁ :
  Eq.{u_4 + 1} (α := M') ((f : (a : M) → M') x : M')
    (Function.comp (β := LocalizedModule S M) (⇑(↑e : LocalizedModule S M →ₗ[R] M') : (a : LocalizedModule S M) → M')
        (⇑(LocalizedModule.mkLinearMap S M) : (a : M) → LocalizedModule S M) x :
      M')
h₂ :
  Eq.{u_4 + 1} (α := M') ((f : (a : M) → M') x : M')
    (Function.comp (β := LocalizedModule S M) (⇑e : (a : LocalizedModule S M) → M')
        (⇑(LocalizedModule.mkLinearMap S M) : (a : M) → LocalizedModule S M) x :
      M')
h₃ :
  Eq.{u_4 + 1} (α := M') ((f : (a : M) → M') x : M')
    ((e : (a : LocalizedModule S M) → M')
        ((LocalizedModule.mkLinearMap S M : (a : M) → LocalizedModule S M) x : LocalizedModule S M) :
      M')
h₄ :
  Eq.{u_4 + 1} (α := M') ((f : (a : M) → M') x : M')
    ((this.equiv.symm ≪≫ₗ h.equiv : (a : LocalizedModule S M) → M')
        ((LocalizedModule.mkLinearMap S M : (a : M) → LocalizedModule S M) x : LocalizedModule S M) :
      M')
h₅ :
  Eq.{u_4 + 1} (α := M') ((f : (a : M) → M') x : M')
    ((h.equiv : (a : TensorProduct R A M) → M')
        ((this.equiv.symm : (a : LocalizedModule S M) → TensorProduct R A M)
            ((LocalizedModule.mkLinearMap S M : (a : M) → LocalizedModule S M) x) :
          TensorProduct R A M) :
      M')
h₆ : Eq.{u_4 + 1} (α := M') ((f : (a : M) → M') x : M') ((h.equiv : (a : TensorProduct R A M) → M') (1 ⊗ₜ[R] x) : M')
h₇ : (f : (a : M) → M') x = HSMul.hSMul.{u_2, u_4, u_4} (α := A) (β := M') 1 ((f : (a : M) → M') x : M')
⊢ Eq.{u_4 + 1} (α := M') ((f : (a : M) → M') x : M')
    (((↑e : LocalizedModule S M →ₗ[R] M') ∘ₗ LocalizedModule.mkLinearMap S M : (a : M) → M') x : M')
have h₈ : Eq.{u_4 + 1} (α := M') ((f : (a : M) → M') x : M') ((f : (a : M) → M') x : M')
Tactic: rw [LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply,
    LinearEquiv.restrictScalars_apply, LinearEquiv.trans_apply, IsBaseChange.equiv_symm_apply,
    IsBaseChange.equiv_tmul, one_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.BaseChange (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_3
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : M
s : ↥S
⊢ Eq (α := Localization (M := R) S ⊗[R] M)
    ((equivTensorProduct S M : (a : LocalizedModule S M) → Localization S ⊗[R] M) (mk x s) :
      Localization (M := R) S ⊗[R] M)
    (Localization.mk 1 s ⊗ₜ[R] x : Localization (M := R) S ⊗[R] M)
have a : Eq (α := LocalizedModule S M)
  ((LinearEquiv.symm (equivTensorProduct S M) : (a : Localization S ⊗[R] M) → LocalizedModule S M)
      ((equivTensorProduct S M : (a : LocalizedModule S M) → Localization S ⊗[R] M) (mk x s)) :
    LocalizedModule S M)
  ((LinearEquiv.symm (equivTensorProduct S M) : (a : Localization S ⊗[R] M) → LocalizedModule S M)
      (Localization.mk 1 s ⊗ₜ[R] x) :
    LocalizedModule S M)
Tactic: apply (equivTensorProduct S M).symm.injective
-- 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
inst_10 : CommSemiring T
inst_11 : Algebra R T
⊢ IsLocalizedModule (M := T) (M' := A ⊗[R] T) S
    (↑(IsScalarTower.toAlgHom R T (A ⊗[R] T)) :
      [inst_12 : FunLike (T →ₐ[R] A ⊗[R] T) T (A ⊗[R] T)] →
        [SemilinearMapClass (T →ₐ[R] A ⊗[R] T) (RingHom.id R) T (A ⊗[R] T)] → T →ₗ[R] A ⊗[R] T)
have rw : IsBaseChange (M := T) (N := A ⊗[R] T) A
  (↑(IsScalarTower.toAlgHom R T (A ⊗[R] T)) :
    [inst_12 : FunLike (T →ₐ[R] A ⊗[R] T) T (A ⊗[R] T)] →
      [SemilinearMapClass (T →ₐ[R] A ⊗[R] T) (RingHom.id R) T (A ⊗[R] T)] → T →ₗ[R] A ⊗[R] T)
Tactic: rw [isLocalizedModule_iff_isBaseChange (S := S) (A := A)]
-- 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₂
a : A
x : M₁
x_1 : M₂
⊢ Eq (α := M₁ ⊗[R] M₂) ((a • x) ⊗ₜ[R] x_1) (x ⊗ₜ[R] (a • x_1))
have obtain : ∀ (r : R) (s : ↥S), Eq (α := M₁ ⊗[R] M₂) ((mk' A r s • x) ⊗ₜ[R] x_1) (x ⊗ₜ[R] (mk' A r s • x_1))
Tactic: obtain ⟨r, s, rfl⟩ := exists_mk'_eq S a
Cleared hypotheses: a
-- 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
⊢ Eq (α := M₁ ⊗[R] M₂) ((mk' A r s • x) ⊗ₜ[R] x_1) (x ⊗ₜ[R] (mk' A r s • x_1))
have rw : 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))
Tactic: rw [← (map_units A s).smul_left_cancel]
-- 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
⊢ 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 : 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))
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))
⊢ 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) (((↑s : R) • x) ⊗ₜ[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))
⊢ 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) (((↑s : R) • x) ⊗ₜ[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))
⊢ 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]