awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Goal:
R₀ : Type u_1
R : Type u_2
S : Type u_3
inst : CommSemiring R₀
inst_1 : Ring R
inst_2 : Ring S
inst_3 : Algebra R₀ R
inst_4 : Algebra R₀ S
f : R →ₐ[R₀] S
M N : ModuleCat.{u_4, u_3} S
g : M ⟶ N
r₀ : R₀
m : (↑((restrictScalars f.toRingHom).obj M) : Type u_4)
⊢ Eq (α := (↑((restrictScalars f.toRingHom).obj N) : Type u_4))
    ((Hom.hom ((restrictScalars f.toRingHom).map (r₀ • g)) :
          (a : (↑((restrictScalars f.toRingHom).obj M) : Type u_4)) →
            (↑((restrictScalars f.toRingHom).obj N) : Type u_4))
        m :
      (↑((restrictScalars f.toRingHom).obj N) : Type u_4))
    ((Hom.hom (r₀ • (restrictScalars f.toRingHom).map g) :
          (a : (↑((restrictScalars f.toRingHom).obj M) : Type u_4)) →
            (↑((restrictScalars f.toRingHom).obj N) : Type u_4))
        m :
      (↑((restrictScalars f.toRingHom).obj N) : Type u_4))

Tactic:
exact congr_arg (· • g.hom m) (f.commutes r₀).symm

Premises used: congr_arg, AlgHom.commutes, HSMul.hSMul, Eq.symm, ModuleCat.Hom.hom, DFunLike.coe
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Goal:
R₀ : Type u_1
R : Type u_2
S : Type u_3
inst : CommSemiring R₀
inst_1 : Ring R
inst_2 : Ring S
inst_3 : Algebra R₀ R
inst_4 : Algebra R₀ S
e : R ≃ₐ[R₀] S
⊢ Functor.Linear R₀ (restrictScalarsEquivalenceOfRingEquiv e.toRingEquiv).functor

Tactic:
inferInstanceAs ((restrictScalars e.toAlgHom.toRingHom).Linear R₀)

Premises used: _private.0.ModuleCat.Algebra.restrictScalarsEquivalenceOfRingEquiv_linear._proof_1
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Goal:
R : Type u₁
S : Type u₂
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
M : ModuleCat.{v, u₁} R
⊢ map' f (𝟙 M) = 𝟙 (obj' f M)

Tactic:
simp [map', obj']

Premises used: ModuleCat.ExtendScalars.map', ModuleCat.ExtendScalars.obj'
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Goal:
R : Type u₁
S : Type u₂
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
M₁ M₂ M₃ : ModuleCat.{v, u₁} R
l₁₂ : M₁ ⟶ M₂
l₂₃ : M₂ ⟶ M₃
hf :
  ∀ (x : (↑(obj' f M₁) : Type (max u₂ v))),
    Eq (α := (↑(obj' f M₃) : Type (max u₂ v)))
      ((Hom.hom (map' f (l₁₂ ≫ l₂₃)) : (a : (↑(obj' f M₁) : Type (max u₂ v))) → (↑(obj' f M₃) : Type (max u₂ v))) x :
        (↑(obj' f M₃) : Type (max u₂ v)))
      ((Hom.hom (map' f l₁₂ ≫ map' f l₂₃) : (a : (↑(obj' f M₁) : Type (max u₂ v))) → (↑(obj' f M₃) : Type (max u₂ v)))
          x :
        (↑(obj' f M₃) : Type (max u₂ v)))
⊢ map' f (l₁₂ ≫ l₂₃) = map' f l₁₂ ≫ map' f l₂₃

Tactic:
ext x
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Goal:
R : Type u₁
S : Type u₂
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
M₁ M₂ M₃ : ModuleCat.{v, u₁} R
l₁₂ : M₁ ⟶ M₂
l₂₃ : M₂ ⟶ M₃
⊢ Eq (α := (↑(obj' f M₃) : Type (max u₂ v)))
    ((Hom.hom (map' f (l₁₂ ≫ l₂₃)) : (a : (↑(obj' f M₁) : Type (max u₂ v))) → (↑(obj' f M₃) : Type (max u₂ v))) 0)
    ((Hom.hom (map' f l₁₂ ≫ map' f l₂₃) : (a : (↑(obj' f M₁) : Type (max u₂ v))) → (↑(obj' f M₃) : Type (max u₂ v))) 0)

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Goal:
R : Type u₁
S : Type u₂
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
M₁ M₂ M₃ : ModuleCat.{v, u₁} R
l₁₂ : M₁ ⟶ M₂
l₂₃ : M₂ ⟶ M₃
x : (↑((restrictScalars f).obj (of S S)) : Type u₂)
y : (↑M₁ : Type v)
⊢ Eq (α := (↑(obj' f M₃) : Type (max u₂ v)))
    ((Hom.hom (map' f (l₁₂ ≫ l₂₃)) : (a : (↑(obj' f M₁) : Type (max u₂ v))) → (↑(obj' f M₃) : Type (max u₂ v)))
        (x ⊗ₜ[R] y) :
      (↑(obj' f M₃) : Type (max u₂ v)))
    ((Hom.hom (map' f l₁₂ ≫ map' f l₂₃) : (a : (↑(obj' f M₁) : Type (max u₂ v))) → (↑(obj' f M₃) : Type (max u₂ v)))
        (x ⊗ₜ[R] y) :
      (↑(obj' f M₃) : Type (max u₂ v)))

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Goal:
R : Type u₁
S : Type u₂
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
M₁ M₂ M₃ : ModuleCat.{v, u₁} R
l₁₂ : M₁ ⟶ M₂
l₂₃ : M₂ ⟶ M₃
x y : TensorProduct.{u₁, u₂, v} R (↑((restrictScalars f).obj (of S S)) : Type u₂) (↑M₁ : Type v)
ihx :
  Eq (α := (↑(obj' f M₃) : Type (max u₂ v)))
    ((Hom.hom (map' f (l₁₂ ≫ l₂₃)) : (a : (↑(obj' f M₁) : Type (max u₂ v))) → (↑(obj' f M₃) : Type (max u₂ v))) x :
      (↑(obj' f M₃) : Type (max u₂ v)))
    ((Hom.hom (map' f l₁₂ ≫ map' f l₂₃) : (a : (↑(obj' f M₁) : Type (max u₂ v))) → (↑(obj' f M₃) : Type (max u₂ v))) x :
      (↑(obj' f M₃) : Type (max u₂ v)))
ihy :
  Eq (α := (↑(obj' f M₃) : Type (max u₂ v)))
    ((Hom.hom (map' f (l₁₂ ≫ l₂₃)) : (a : (↑(obj' f M₁) : Type (max u₂ v))) → (↑(obj' f M₃) : Type (max u₂ v))) y :
      (↑(obj' f M₃) : Type (max u₂ v)))
    ((Hom.hom (map' f l₁₂ ≫ map' f l₂₃) : (a : (↑(obj' f M₁) : Type (max u₂ v))) → (↑(obj' f M₃) : Type (max u₂ v))) y :
      (↑(obj' f M₃) : Type (max u₂ v)))
hf :
  HAdd.hAdd (α := (↑(obj' f M₃) : Type (max u₂ v))) (β := (↑(obj' f M₃) : Type (max u₂ v)))
      ((Hom.hom (map' f (l₁₂ ≫ l₂₃)) : (a : (↑(obj' f M₁) : Type (max u₂ v))) → (↑(obj' f M₃) : Type (max u₂ v))) x :
        (↑(obj' f M₃) : Type (max u₂ v)))
      ((Hom.hom (map' f (l₁₂ ≫ l₂₃)) : (a : (↑(obj' f M₁) : Type (max u₂ v))) → (↑(obj' f M₃) : Type (max u₂ v))) y :
        (↑(obj' f M₃) : Type (max u₂ v))) =
    HAdd.hAdd (α := (↑(obj' f M₃) : Type (max u₂ v))) (β := (↑(obj' f M₃) : Type (max u₂ v)))
      ((Hom.hom (map' f l₁₂ ≫ map' f l₂₃) : (a : (↑(obj' f M₁) : Type (max u₂ v))) → (↑(obj' f M₃) : Type (max u₂ v)))
          x :
        (↑(obj' f M₃) : Type (max u₂ v)))
      ((Hom.hom (map' f l₁₂ ≫ map' f l₂₃) : (a : (↑(obj' f M₁) : Type (max u₂ v))) → (↑(obj' f M₃) : Type (max u₂ v)))
          y :
        (↑(obj' f M₃) : Type (max u₂ v)))
⊢ Eq (α := (↑(obj' f M₃) : Type (max u₂ v)))
    ((Hom.hom (map' f (l₁₂ ≫ l₂₃)) : (a : (↑(obj' f M₁) : Type (max u₂ v))) → (↑(obj' f M₃) : Type (max u₂ v)))
        (x + y) :
      (↑(obj' f M₃) : Type (max u₂ v)))
    ((Hom.hom (map' f l₁₂ ≫ map' f l₂₃) : (a : (↑(obj' f M₁) : Type (max u₂ v))) → (↑(obj' f M₃) : Type (max u₂ v)))
        (x + y) :
      (↑(obj' f M₃) : Type (max u₂ v)))

Tactic:
erw [LinearMap.map_add, LinearMap.map_add]

Premises used: LinearMap.map_add
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Goal:
R : Type u₁
S : Type u₂
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
M₁ M₂ M₃ : ModuleCat.{v, u₁} R
l₁₂ : M₁ ⟶ M₂
l₂₃ : M₂ ⟶ M₃
x y : TensorProduct.{u₁, u₂, v} R (↑((restrictScalars f).obj (of S S)) : Type u₂) (↑M₁ : Type v)
ihx :
  Eq (α := (↑(obj' f M₃) : Type (max u₂ v)))
    ((Hom.hom (map' f (l₁₂ ≫ l₂₃)) : (a : (↑(obj' f M₁) : Type (max u₂ v))) → (↑(obj' f M₃) : Type (max u₂ v))) x :
      (↑(obj' f M₃) : Type (max u₂ v)))
    ((Hom.hom (map' f l₁₂ ≫ map' f l₂₃) : (a : (↑(obj' f M₁) : Type (max u₂ v))) → (↑(obj' f M₃) : Type (max u₂ v))) x :
      (↑(obj' f M₃) : Type (max u₂ v)))
ihy :
  Eq (α := (↑(obj' f M₃) : Type (max u₂ v)))
    ((Hom.hom (map' f (l₁₂ ≫ l₂₃)) : (a : (↑(obj' f M₁) : Type (max u₂ v))) → (↑(obj' f M₃) : Type (max u₂ v))) y :
      (↑(obj' f M₃) : Type (max u₂ v)))
    ((Hom.hom (map' f l₁₂ ≫ map' f l₂₃) : (a : (↑(obj' f M₁) : Type (max u₂ v))) → (↑(obj' f M₃) : Type (max u₂ v))) y :
      (↑(obj' f M₃) : Type (max u₂ v)))
⊢ HAdd.hAdd (α := (↑(obj' f M₃) : Type (max u₂ v))) (β := (↑(obj' f M₃) : Type (max u₂ v)))
      ((Hom.hom (map' f (l₁₂ ≫ l₂₃)) : (a : (↑(obj' f M₁) : Type (max u₂ v))) → (↑(obj' f M₃) : Type (max u₂ v))) x :
        (↑(obj' f M₃) : Type (max u₂ v)))
      ((Hom.hom (map' f (l₁₂ ≫ l₂₃)) : (a : (↑(obj' f M₁) : Type (max u₂ v))) → (↑(obj' f M₃) : Type (max u₂ v))) y :
        (↑(obj' f M₃) : Type (max u₂ v))) =
    HAdd.hAdd (α := (↑(obj' f M₃) : Type (max u₂ v))) (β := (↑(obj' f M₃) : Type (max u₂ v)))
      ((Hom.hom (map' f l₁₂ ≫ map' f l₂₃) : (a : (↑(obj' f M₁) : Type (max u₂ v))) → (↑(obj' f M₃) : Type (max u₂ v)))
          x :
        (↑(obj' f M₃) : Type (max u₂ v)))
      ((Hom.hom (map' f l₁₂ ≫ map' f l₂₃) : (a : (↑(obj' f M₁) : Type (max u₂ v))) → (↑(obj' f M₃) : Type (max u₂ v)))
          y :
        (↑(obj' f M₃) : Type (max u₂ v)))

Tactic:
grind
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Goal:
R : Type u₁
S : Type u₂
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
M₁ M₂ M₃ : ModuleCat.{v, u₁} R
l₁₂ : M₁ ⟶ M₂
l₂₃ : M₂ ⟶ M₃
x : (↑(obj' f M₁) : Type (max u₂ v))
hf :
  Eq (α := (↑(obj' f M₃) : Type (max u₂ v)))
    ((Hom.hom (map' f (l₁₂ ≫ l₂₃)) : (a : (↑(obj' f M₁) : Type (max u₂ v))) → (↑(obj' f M₃) : Type (max u₂ v))) 0)
    ((Hom.hom (map' f l₁₂ ≫ map' f l₂₃) : (a : (↑(obj' f M₁) : Type (max u₂ v))) → (↑(obj' f M₃) : Type (max u₂ v))) 0)
hf₁ :
  ∀ (x : (↑((restrictScalars f).obj (of S S)) : Type u₂)) (y : (↑M₁ : Type v)),
    Eq (α := (↑(obj' f M₃) : Type (max u₂ v)))
      ((Hom.hom (map' f (l₁₂ ≫ l₂₃)) : (a : (↑(obj' f M₁) : Type (max u₂ v))) → (↑(obj' f M₃) : Type (max u₂ v)))
          (x ⊗ₜ[R] y) :
        (↑(obj' f M₃) : Type (max u₂ v)))
      ((Hom.hom (map' f l₁₂ ≫ map' f l₂₃) : (a : (↑(obj' f M₁) : Type (max u₂ v))) → (↑(obj' f M₃) : Type (max u₂ v)))
          (x ⊗ₜ[R] y) :
        (↑(obj' f M₃) : Type (max u₂ v)))
hf₂ :
  ∀ (x y : TensorProduct.{u₁, u₂, v} R (↑((restrictScalars f).obj (of S S)) : Type u₂) (↑M₁ : Type v))
    (ihx :
      Eq (α := (↑(obj' f M₃) : Type (max u₂ v)))
        ((Hom.hom (map' f (l₁₂ ≫ l₂₃)) : (a : (↑(obj' f M₁) : Type (max u₂ v))) → (↑(obj' f M₃) : Type (max u₂ v))) x :
          (↑(obj' f M₃) : Type (max u₂ v)))
        ((Hom.hom (map' f l₁₂ ≫ map' f l₂₃) : (a : (↑(obj' f M₁) : Type (max u₂ v))) → (↑(obj' f M₃) : Type (max u₂ v)))
            x :
          (↑(obj' f M₃) : Type (max u₂ v))))
    (ihy :
      Eq (α := (↑(obj' f M₃) : Type (max u₂ v)))
        ((Hom.hom (map' f (l₁₂ ≫ l₂₃)) : (a : (↑(obj' f M₁) : Type (max u₂ v))) → (↑(obj' f M₃) : Type (max u₂ v))) y :
          (↑(obj' f M₃) : Type (max u₂ v)))
        ((Hom.hom (map' f l₁₂ ≫ map' f l₂₃) : (a : (↑(obj' f M₁) : Type (max u₂ v))) → (↑(obj' f M₃) : Type (max u₂ v)))
            y :
          (↑(obj' f M₃) : Type (max u₂ v)))),
    Eq (α := (↑(obj' f M₃) : Type (max u₂ v)))
      ((Hom.hom (map' f (l₁₂ ≫ l₂₃)) : (a : (↑(obj' f M₁) : Type (max u₂ v))) → (↑(obj' f M₃) : Type (max u₂ v)))
          (x + y) :
        (↑(obj' f M₃) : Type (max u₂ v)))
      ((Hom.hom (map' f l₁₂ ≫ map' f l₂₃) : (a : (↑(obj' f M₁) : Type (max u₂ v))) → (↑(obj' f M₃) : Type (max u₂ v)))
          (x + y) :
        (↑(obj' f M₃) : Type (max u₂ v)))
⊢ Eq (α := (↑(obj' f M₃) : Type (max u₂ v)))
    ((Hom.hom (map' f (l₁₂ ≫ l₂₃)) : (a : (↑(obj' f M₁) : Type (max u₂ v))) → (↑(obj' f M₃) : Type (max u₂ v))) x :
      (↑(obj' f M₃) : Type (max u₂ v)))
    ((Hom.hom (map' f l₁₂ ≫ map' f l₂₃) : (a : (↑(obj' f M₁) : Type (max u₂ v))) → (↑(obj' f M₃) : Type (max u₂ v))) x :
      (↑(obj' f M₃) : Type (max u₂ v)))

Tactic:
induction x using TensorProduct.induction_on with
  | zero => rfl
  | tmul => rfl
  | add _ _ ihx ihy => erw [LinearMap.map_add, LinearMap.map_add]; grind

Premises used: LinearMap.map_add, TensorProduct.tmul
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Goal:
R : Type u₁
S : Type u₂
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
M : ModuleCat.{v, u₁} R
s s' : S
m : (↑M : Type v)
⊢ HSMul.hSMul (β := TensorProduct.{u₁, u₂, v} R (↑((restrictScalars f).obj (of S S)) : Type u₂) (↑M : Type v)) s
      (s' ⊗ₜ[R] m) =
    (s * s') ⊗ₜ[R] m

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Goal:
R : Type u₁
S : Type u₂
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
M M' : ModuleCat.{v, u₁} R
g : M ⟶ M'
s : S
m : (↑M : Type v)
⊢ Eq (α := (↑((extendScalars f).obj M') : Type (max u₂ v)))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat S) ↦ (↑x1 : Type (max u₂ v)) →ₗ[S] (↑x2 : Type (max u₂ v)))
            (CC := carrier) ((extendScalars f).map g) :
          (a : (↑((extendScalars f).obj M) : Type (max u₂ v))) → (↑((extendScalars f).obj M') : Type (max u₂ v)))
        (s ⊗ₜ[R] m) :
      (↑((extendScalars f).obj M') : Type (max u₂ v)))
    (s ⊗ₜ[R]
        (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u₁} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
              carrier) g :
            (a : (↑M : Type v)) → (↑M' : Type v))
          m :
      TensorProduct.{u₁, u₂, v} R S (↑M' : Type v))

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Goal:
R : Type u₁
S : Type u₂
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
M : ModuleCat.{u_1, u₁} R
N : ModuleCat S
α β : (extendScalars f).obj M ⟶ N
h :
  ∀ (m : (↑M : Type u_1)),
    Eq (α := (↑N : Type (max u₂ u_1)))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat S) ↦
              (↑x1 : Type (max u₂ u_1)) →ₗ[S] (↑x2 : Type (max u₂ u_1))) (CC := carrier) α :
            (a : (↑((extendScalars f).obj M) : Type (max u₂ u_1))) → (↑N : Type (max u₂ u_1)))
          (1 ⊗ₜ[R] m) :
        (↑N : Type (max u₂ u_1)))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat S) ↦
              (↑x1 : Type (max u₂ u_1)) →ₗ[S] (↑x2 : Type (max u₂ u_1))) (CC := carrier) β :
            (a : (↑((extendScalars f).obj M) : Type (max u₂ u_1))) → (↑N : Type (max u₂ u_1)))
          (1 ⊗ₜ[R] m) :
        (↑N : Type (max u₂ u_1)))
a : (restrictScalars f).map α = (restrictScalars f).map β
⊢ α = β

Tactic:
apply (restrictScalars f).map_injective

Premises used: ModuleCat.restrictScalars, CategoryTheory.Functor.map_injective
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Goal:
R : Type u₁
S : Type u₂
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
M : ModuleCat.{u_1, u₁} R
N : ModuleCat S
α β : (extendScalars f).obj M ⟶ N
h :
  ∀ (m : (↑M : Type u_1)),
    Eq (α := (↑N : Type (max u₂ u_1)))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat S) ↦
              (↑x1 : Type (max u₂ u_1)) →ₗ[S] (↑x2 : Type (max u₂ u_1))) (CC := carrier) α :
            (a : (↑((extendScalars f).obj M) : Type (max u₂ u_1))) → (↑N : Type (max u₂ u_1)))
          (1 ⊗ₜ[R] m) :
        (↑N : Type (max u₂ u_1)))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat S) ↦
              (↑x1 : Type (max u₂ u_1)) →ₗ[S] (↑x2 : Type (max u₂ u_1))) (CC := carrier) β :
            (a : (↑((extendScalars f).obj M) : Type (max u₂ u_1))) → (↑N : Type (max u₂ u_1)))
          (1 ⊗ₜ[R] m) :
        (↑N : Type (max u₂ u_1)))
this : Algebra R S := f.toAlgebra
a : Hom.hom ((restrictScalars f).map α) = Hom.hom ((restrictScalars f).map β)
⊢ (restrictScalars f).map α = (restrictScalars f).map β

Tactic:
ext : 1
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Goal:
R : Type u₁
S : Type u₂
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
M : ModuleCat.{u_1, u₁} R
N : ModuleCat S
α β : (extendScalars f).obj M ⟶ N
h :
  ∀ (m : (↑M : Type u_1)),
    Eq (α := (↑N : Type (max u₂ u_1)))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat S) ↦
              (↑x1 : Type (max u₂ u_1)) →ₗ[S] (↑x2 : Type (max u₂ u_1))) (CC := carrier) α :
            (a : (↑((extendScalars f).obj M) : Type (max u₂ u_1))) → (↑N : Type (max u₂ u_1)))
          (1 ⊗ₜ[R] m) :
        (↑N : Type (max u₂ u_1)))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat S) ↦
              (↑x1 : Type (max u₂ u_1)) →ₗ[S] (↑x2 : Type (max u₂ u_1))) (CC := carrier) β :
            (a : (↑((extendScalars f).obj M) : Type (max u₂ u_1))) → (↑N : Type (max u₂ u_1)))
          (1 ⊗ₜ[R] m) :
        (↑N : Type (max u₂ u_1)))
this : Algebra R S := f.toAlgebra
a :
  ∀ (x : (↑((restrictScalars f).obj (of S S)) : Type u₂)) (y : (↑M : Type u_1)),
    Eq (α := (↑((restrictScalars f).obj N) : Type (max u_1 u₂)))
      ((Hom.hom ((restrictScalars f).map α) :
            (a : (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑M : Type u_1)) →
              (↑((restrictScalars f).obj N) : Type (max u_1 u₂)))
          (x ⊗ₜ[R] y) :
        (↑((restrictScalars f).obj N) : Type (max u_1 u₂)))
      ((Hom.hom ((restrictScalars f).map β) :
            (a : (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑M : Type u_1)) →
              (↑((restrictScalars f).obj N) : Type (max u_1 u₂)))
          (x ⊗ₜ[R] y) :
        (↑((restrictScalars f).obj N) : Type (max u_1 u₂)))
⊢ Hom.hom ((restrictScalars f).map α) = Hom.hom ((restrictScalars f).map β)

Tactic:
apply TensorProduct.ext'

Premises used: TensorProduct.ext'
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Goal:
R : Type u₁
S : Type u₂
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
M : ModuleCat.{u_1, u₁} R
N : ModuleCat S
α β : (extendScalars f).obj M ⟶ N
h :
  ∀ (m : (↑M : Type u_1)),
    Eq (α := (↑N : Type (max u₂ u_1)))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat S) ↦
              (↑x1 : Type (max u₂ u_1)) →ₗ[S] (↑x2 : Type (max u₂ u_1))) (CC := carrier) α :
            (a : (↑((extendScalars f).obj M) : Type (max u₂ u_1))) → (↑N : Type (max u₂ u_1)))
          (1 ⊗ₜ[R] m) :
        (↑N : Type (max u₂ u_1)))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat S) ↦
              (↑x1 : Type (max u₂ u_1)) →ₗ[S] (↑x2 : Type (max u₂ u_1))) (CC := carrier) β :
            (a : (↑((extendScalars f).obj M) : Type (max u₂ u_1))) → (↑N : Type (max u₂ u_1)))
          (1 ⊗ₜ[R] m) :
        (↑N : Type (max u₂ u_1)))
this : Algebra R S := f.toAlgebra
s : S
m : (↑M : Type u_1)
a :
  Eq (α := (↑N : Type (max u_1 u₂)))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat S) ↦ (↑x1 : Type (max u_1 u₂)) →ₗ[S] (↑x2 : Type (max u_1 u₂)))
            (CC := carrier) α :
          (a : (↑((extendScalars f).obj M) : Type (max u_1 u₂))) → (↑N : Type (max u_1 u₂)))
        (s ⊗ₜ[R] m) :
      (↑N : Type (max u_1 u₂)))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat S) ↦ (↑x1 : Type (max u_1 u₂)) →ₗ[S] (↑x2 : Type (max u_1 u₂)))
            (CC := carrier) β :
          (a : (↑((extendScalars f).obj M) : Type (max u_1 u₂))) → (↑N : Type (max u_1 u₂)))
        (s ⊗ₜ[R] m) :
      (↑N : Type (max u_1 u₂)))
⊢ Eq (α := (↑((restrictScalars f).obj N) : Type (max u_1 u₂)))
    ((Hom.hom ((restrictScalars f).map α) :
          (a : (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑M : Type u_1)) →
            (↑((restrictScalars f).obj N) : Type (max u_1 u₂)))
        (s ⊗ₜ[R] m) :
      (↑((restrictScalars f).obj N) : Type (max u_1 u₂)))
    ((Hom.hom ((restrictScalars f).map β) :
          (a : (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑M : Type u_1)) →
            (↑((restrictScalars f).obj N) : Type (max u_1 u₂)))
        (s ⊗ₜ[R] m) :
      (↑((restrictScalars f).obj N) : Type (max u_1 u₂)))

Tactic:
change α (s ⊗ₜ m) = β (s ⊗ₜ m)

Premises used: CategoryTheory.ConcreteCategory.hom, TensorProduct.tmul, DFunLike.coe
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Goal:
R : Type u₁
S : Type u₂
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
M : ModuleCat.{u_1, u₁} R
N : ModuleCat S
α β : (extendScalars f).obj M ⟶ N
h :
  ∀ (m : (↑M : Type u_1)),
    Eq (α := (↑N : Type (max u₂ u_1)))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat S) ↦
              (↑x1 : Type (max u₂ u_1)) →ₗ[S] (↑x2 : Type (max u₂ u_1))) (CC := carrier) α :
            (a : (↑((extendScalars f).obj M) : Type (max u₂ u_1))) → (↑N : Type (max u₂ u_1)))
          (1 ⊗ₜ[R] m) :
        (↑N : Type (max u₂ u_1)))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat S) ↦
              (↑x1 : Type (max u₂ u_1)) →ₗ[S] (↑x2 : Type (max u₂ u_1))) (CC := carrier) β :
            (a : (↑((extendScalars f).obj M) : Type (max u₂ u_1))) → (↑N : Type (max u₂ u_1)))
          (1 ⊗ₜ[R] m) :
        (↑N : Type (max u₂ u_1)))
this : Algebra R S := f.toAlgebra
s : S
m : (↑M : Type u_1)
rw : Eq (α := TensorProduct.{u₁, u₂, u_1} R S (↑M : Type u_1)) (s ⊗ₜ[R] m) ((s * 1) ⊗ₜ[R] m)
rw₁ rw₂ : Eq (α := TensorProduct.{u₁, u₂, u_1} R S (↑M : Type u_1)) (s ⊗ₜ[R] m) (s ⊗ₜ[R] m)
⊢ s ⊗ₜ[R] m = HSMul.hSMul (β := TensorProduct.{u₁, u₂, u_1} R S (↑M : Type u_1)) s (1 ⊗ₜ[R] m)

Tactic:
rw [ExtendScalars.smul_tmul, mul_one]

Premises used: ModuleCat.ExtendScalars.smul_tmul, mul_one
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Goal:
R : Type u₁
S : Type u₂
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
M : ModuleCat.{u_1, u₁} R
N : ModuleCat S
α β : (extendScalars f).obj M ⟶ N
h :
  ∀ (m : (↑M : Type u_1)),
    Eq (α := (↑N : Type (max u₂ u_1)))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat S) ↦
              (↑x1 : Type (max u₂ u_1)) →ₗ[S] (↑x2 : Type (max u₂ u_1))) (CC := carrier) α :
            (a : (↑((extendScalars f).obj M) : Type (max u₂ u_1))) → (↑N : Type (max u₂ u_1)))
          (1 ⊗ₜ[R] m) :
        (↑N : Type (max u₂ u_1)))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat S) ↦
              (↑x1 : Type (max u₂ u_1)) →ₗ[S] (↑x2 : Type (max u₂ u_1))) (CC := carrier) β :
            (a : (↑((extendScalars f).obj M) : Type (max u₂ u_1))) → (↑N : Type (max u₂ u_1)))
          (1 ⊗ₜ[R] m) :
        (↑N : Type (max u₂ u_1)))
this : Algebra R S := f.toAlgebra
s : S
m : (↑M : Type u_1)
⊢ s ⊗ₜ[R] m = HSMul.hSMul (β := TensorProduct.{u₁, u₂, u_1} R S (↑M : Type u_1)) s (1 ⊗ₜ[R] m)

Tactic:
have : s ⊗ₜ[R] (m : M) = s • (1 : S) ⊗ₜ[R] m := by
    rw [ExtendScalars.smul_tmul, mul_one]
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Goal:
R : Type u₁
S : Type u₂
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
M : ModuleCat.{u_1, u₁} R
N : ModuleCat S
α β : (extendScalars f).obj M ⟶ N
h :
  ∀ (m : (↑M : Type u_1)),
    Eq (α := (↑N : Type (max u₂ u_1)))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat S) ↦
              (↑x1 : Type (max u₂ u_1)) →ₗ[S] (↑x2 : Type (max u₂ u_1))) (CC := carrier) α :
            (a : (↑((extendScalars f).obj M) : Type (max u₂ u_1))) → (↑N : Type (max u₂ u_1)))
          (1 ⊗ₜ[R] m) :
        (↑N : Type (max u₂ u_1)))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat S) ↦
              (↑x1 : Type (max u₂ u_1)) →ₗ[S] (↑x2 : Type (max u₂ u_1))) (CC := carrier) β :
            (a : (↑((extendScalars f).obj M) : Type (max u₂ u_1))) → (↑N : Type (max u₂ u_1)))
          (1 ⊗ₜ[R] m) :
        (↑N : Type (max u₂ u_1)))
this_1 : Algebra R S := f.toAlgebra
s : S
m : (↑M : Type u_1)
this : s ⊗ₜ[R] m = HSMul.hSMul (β := TensorProduct.{u₁, u₂, u_1} R S (↑M : Type u_1)) s (1 ⊗ₜ[R] m)
⊢ Eq (α := (↑N : Type (max u_1 u₂)))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat S) ↦ (↑x1 : Type (max u_1 u₂)) →ₗ[S] (↑x2 : Type (max u_1 u₂)))
            (CC := carrier) α :
          (a : (↑((extendScalars f).obj M) : Type (max u_1 u₂))) → (↑N : Type (max u_1 u₂)))
        (s ⊗ₜ[R] m) :
      (↑N : Type (max u_1 u₂)))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat S) ↦ (↑x1 : Type (max u_1 u₂)) →ₗ[S] (↑x2 : Type (max u_1 u₂)))
            (CC := carrier) β :
          (a : (↑((extendScalars f).obj M) : Type (max u_1 u₂))) → (↑N : Type (max u_1 u₂)))
        (s ⊗ₜ[R] m) :
      (↑N : Type (max u_1 u₂)))

Tactic:
simp only [this, map_smul, h]

Premises used: map_smul