mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.CoalgCat.Monoidal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
X₁✝ Y₁✝ X₂✝ Y₂✝ : CoalgCat R
f : X₁✝ ⟶ Y₁✝
g : X₂✝ ⟶ Y₂✝
x✝ : ↑((forget₂ (CoalgCat R) (ModuleCat R)).obj (X₁✝ ⊗ X₂✝))
⊢ (ModuleCat.Hom.hom ((forget₂ (CoalgCat R) (ModuleCat R)).map (f ⊗ₘ g))) x✝ =
    (ModuleCat.Hom.hom
        ((Iso.refl ((forget₂ (CoalgCat R) (ModuleCat R)).obj X₁✝ ⊗ (forget₂ (CoalgCat R) (ModuleCat R)).obj X₂✝)).inv ≫
          ((forget₂ (CoalgCat R) (ModuleCat R)).map f ⊗ₘ (forget₂ (CoalgCat R) (ModuleCat R)).map g) ≫
            (Iso.refl
                ((forget₂ (CoalgCat R) (ModuleCat R)).obj Y₁✝ ⊗ (forget₂ (CoalgCat R) (ModuleCat R)).obj Y₂✝)).hom))
      x✝

Tactic:
;

Goal state after:
R : Type u
inst✝ : CommRing R
X₁✝ Y₁✝ X₂✝ Y₂✝ : CoalgCat R
f : X₁✝ ⟶ Y₁✝
g : X₂✝ ⟶ Y₂✝
x✝ : ↑((forget₂ (CoalgCat R) (ModuleCat R)).obj (X₁✝ ⊗ X₂✝))
⊢ (ModuleCat.Hom.hom ((forget₂ (CoalgCat R) (ModuleCat R)).map (f ⊗ₘ g))) x✝ =
    (ModuleCat.Hom.hom
        ((Iso.refl ((forget₂ (CoalgCat R) (ModuleCat R)).obj X₁✝ ⊗ (forget₂ (CoalgCat R) (ModuleCat R)).obj X₂✝)).inv ≫
          ((forget₂ (CoalgCat R) (ModuleCat R)).map f ⊗ₘ (forget₂ (CoalgCat R) (ModuleCat R)).map g) ≫
            (Iso.refl
                ((forget₂ (CoalgCat R) (ModuleCat R)).obj Y₁✝ ⊗ (forget₂ (CoalgCat R) (ModuleCat R)).obj Y₂✝)).hom))
      x✝
Module: Mathlib.Algebra.Category.CoalgCat.Monoidal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
X : CoalgCat R
x✝ : ↑X.toModuleCat
⊢ (((TensorProduct.mk R ↑(𝟙_ (CoalgCat R)).toModuleCat ↑X.toModuleCat).compr₂ₛₗ
          (ModuleCat.Hom.hom ((forget₂ (CoalgCat R) (ModuleCat R)).map (λ_ X).hom)))
        1)
      x✝ =
    (((TensorProduct.mk R ↑(𝟙_ (CoalgCat R)).toModuleCat ↑X.toModuleCat).compr₂ₛₗ
          (ModuleCat.Hom.hom
            (((Iso.refl
                      ((forget₂ (CoalgCat R) (ModuleCat R)).obj (𝟙_ (CoalgCat R)) ⊗
                        (forget₂ (CoalgCat R) (ModuleCat R)).obj X)).symm ≪≫
                  ((Iso.refl (𝟙_ (ModuleCat R))).symm ⊗ᵢ Iso.refl ((forget₂ (CoalgCat R) (ModuleCat R)).obj X))) ≪≫
                λ_ ((forget₂ (CoalgCat R) (ModuleCat R)).obj X)).hom))
        1)
      x✝

Tactic:
;

Goal state after:
R : Type u
inst✝ : CommRing R
X : CoalgCat R
x✝ : ↑X.toModuleCat
⊢ (((TensorProduct.mk R ↑(𝟙_ (CoalgCat R)).toModuleCat ↑X.toModuleCat).compr₂ₛₗ
          (ModuleCat.Hom.hom ((forget₂ (CoalgCat R) (ModuleCat R)).map (λ_ X).hom)))
        1)
      x✝ =
    (((TensorProduct.mk R ↑(𝟙_ (CoalgCat R)).toModuleCat ↑X.toModuleCat).compr₂ₛₗ
          (ModuleCat.Hom.hom
            (((Iso.refl
                      ((forget₂ (CoalgCat R) (ModuleCat R)).obj (𝟙_ (CoalgCat R)) ⊗
                        (forget₂ (CoalgCat R) (ModuleCat R)).obj X)).symm ≪≫
                  ((Iso.refl (𝟙_ (ModuleCat R))).symm ⊗ᵢ Iso.refl ((forget₂ (CoalgCat R) (ModuleCat R)).obj X))) ≪≫
                λ_ ((forget₂ (CoalgCat R) (ModuleCat R)).obj X)).hom))
        1)
      x✝
Module: Mathlib.Algebra.Category.CoalgCat.Monoidal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
X : CoalgCat R
x✝ : ↑X.toModuleCat
⊢ (((TensorProduct.mk R ↑X.toModuleCat ↑(𝟙_ (CoalgCat R)).toModuleCat).compr₂ₛₗ
          (ModuleCat.Hom.hom ((forget₂ (CoalgCat R) (ModuleCat R)).map (ρ_ X).hom)))
        x✝)
      1 =
    (((TensorProduct.mk R ↑X.toModuleCat ↑(𝟙_ (CoalgCat R)).toModuleCat).compr₂ₛₗ
          (ModuleCat.Hom.hom
            (((Iso.refl
                      ((forget₂ (CoalgCat R) (ModuleCat R)).obj X ⊗
                        (forget₂ (CoalgCat R) (ModuleCat R)).obj (𝟙_ (CoalgCat R)))).symm ≪≫
                  (Iso.refl ((forget₂ (CoalgCat R) (ModuleCat R)).obj X) ⊗ᵢ (Iso.refl (𝟙_ (ModuleCat R))).symm)) ≪≫
                ρ_ ((forget₂ (CoalgCat R) (ModuleCat R)).obj X)).hom))
        x✝)
      1

Tactic:
;

Goal state after:
R : Type u
inst✝ : CommRing R
X : CoalgCat R
x✝ : ↑X.toModuleCat
⊢ (((TensorProduct.mk R ↑X.toModuleCat ↑(𝟙_ (CoalgCat R)).toModuleCat).compr₂ₛₗ
          (ModuleCat.Hom.hom ((forget₂ (CoalgCat R) (ModuleCat R)).map (ρ_ X).hom)))
        x✝)
      1 =
    (((TensorProduct.mk R ↑X.toModuleCat ↑(𝟙_ (CoalgCat R)).toModuleCat).compr₂ₛₗ
          (ModuleCat.Hom.hom
            (((Iso.refl
                      ((forget₂ (CoalgCat R) (ModuleCat R)).obj X ⊗
                        (forget₂ (CoalgCat R) (ModuleCat R)).obj (𝟙_ (CoalgCat R)))).symm ≪≫
                  (Iso.refl ((forget₂ (CoalgCat R) (ModuleCat R)).obj X) ⊗ᵢ (Iso.refl (𝟙_ (ModuleCat R))).symm)) ≪≫
                ρ_ ((forget₂ (CoalgCat R) (ModuleCat R)).obj X)).hom))
        x✝)
      1
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
M✝ : ModuleCat R
M M' : ModuleCat R
g : M ⟶ M'
s : S
h : ↑((restrictScalars f).obj (of S S)) →ₗ[R] ↑M
x✝ : ↑((restrictScalars f).obj (of S S))
⊢ (Hom.hom g ∘ₗ (s • h)) x✝ = ((RingHom.id S) s • Hom.hom g ∘ₗ h) x✝

Tactic:
;

Goal state after:
R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
M✝ : ModuleCat R
M M' : ModuleCat R
g : M ⟶ M'
s : S
h : ↑((restrictScalars f).obj (of S S)) →ₗ[R] ↑M
x✝ : ↑((restrictScalars f).obj (of S S))
⊢ (Hom.hom g ∘ₗ (s • h)) x✝ = ((RingHom.id S) s • Hom.hom g ∘ₗ h) x✝
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
x✝¹ : ModuleCat R
x✝ : ↑(CoextendScalars.obj' f x✝¹)
⊢ (Hom.hom (CoextendScalars.map' f (𝟙 x✝¹))) x✝ = (Hom.hom (𝟙 (CoextendScalars.obj' f x✝¹))) x✝

Tactic:
;

Goal state after:
R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
x✝¹ : ModuleCat R
x✝ : ↑(CoextendScalars.obj' f x✝¹)
⊢ (Hom.hom (CoextendScalars.map' f (𝟙 x✝¹))) x✝ = (Hom.hom (𝟙 (CoextendScalars.obj' f x✝¹))) x✝
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
X✝ Y✝ Z✝ : ModuleCat R
x✝² : X✝ ⟶ Y✝
x✝¹ : Y✝ ⟶ Z✝
x✝ : ↑(CoextendScalars.obj' f X✝)
⊢ (Hom.hom (CoextendScalars.map' f (x✝² ≫ x✝¹))) x✝ =
    (Hom.hom (CoextendScalars.map' f x✝² ≫ CoextendScalars.map' f x✝¹)) x✝

Tactic:
;

Goal state after:
R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
X✝ Y✝ Z✝ : ModuleCat R
x✝² : X✝ ⟶ Y✝
x✝¹ : Y✝ ⟶ Z✝
x✝ : ↑(CoextendScalars.obj' f X✝)
⊢ (Hom.hom (CoextendScalars.map' f (x✝² ≫ x✝¹))) x✝ =
    (Hom.hom (CoextendScalars.map' f x✝² ≫ CoextendScalars.map' f x✝¹)) x✝
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
X : ModuleCat S
Y : ModuleCat R
g : (restrictScalars f).obj X ⟶ Y
x✝ : ↑((restrictScalars f).obj X)
⊢ (Hom.hom
        (RestrictionCoextensionAdj.HomEquiv.toRestriction f (RestrictionCoextensionAdj.HomEquiv.fromRestriction f g)))
      x✝ =
    (Hom.hom g) x✝

Tactic:
;

Goal state after:
R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
X : ModuleCat S
Y : ModuleCat R
g : (restrictScalars f).obj X ⟶ Y
x✝ : ↑((restrictScalars f).obj X)
⊢ (Hom.hom
        (RestrictionCoextensionAdj.HomEquiv.toRestriction f (RestrictionCoextensionAdj.HomEquiv.fromRestriction f g)))
      x✝ =
    (Hom.hom g) x✝
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
X : ModuleCat S
Y : ModuleCat R
g : X ⟶ (coextendScalars f).obj Y
x✝¹ : ↑X
x✝ : ↑((restrictScalars f).obj (of S S))
⊢ ((CoextendScalars.equiv f Y)
        ((Hom.hom
            (RestrictionCoextensionAdj.HomEquiv.fromRestriction f
              (RestrictionCoextensionAdj.HomEquiv.toRestriction f g)))
          x✝¹))
      x✝ =
    ((CoextendScalars.equiv f Y) ((Hom.hom g) x✝¹)) x✝

Tactic:
;

Goal state after:
R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
X : ModuleCat S
Y : ModuleCat R
g : X ⟶ (coextendScalars f).obj Y
x✝¹ : ↑X
x✝ : ↑((restrictScalars f).obj (of S S))
⊢ ((CoextendScalars.equiv f Y)
        ((Hom.hom
            (RestrictionCoextensionAdj.HomEquiv.fromRestriction f
              (RestrictionCoextensionAdj.HomEquiv.toRestriction f g)))
          x✝¹))
      x✝ =
    ((CoextendScalars.equiv f Y) ((Hom.hom g) x✝¹)) x✝
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
g : (extendScalars f).obj X ⟶ Y
x✝¹ x✝ : ↑X
⊢ (ConcreteCategory.hom g) (1 ⊗ₜ[R] (x✝¹ + x✝)) =
    (ConcreteCategory.hom g) (1 ⊗ₜ[R] x✝¹) + (ConcreteCategory.hom g) (1 ⊗ₜ[R] x✝)

Tactic:
;

Goal state after:
R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
g : (extendScalars f).obj X ⟶ Y
x✝¹ x✝ : ↑X
⊢ (ConcreteCategory.hom g) (1 ⊗ₜ[R] (x✝¹ + x✝)) =
    (ConcreteCategory.hom g) (1 ⊗ₜ[R] x✝¹) + (ConcreteCategory.hom g) (1 ⊗ₜ[R] x✝)
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
s : S
g : X ⟶ (restrictScalars f).obj Y
⊢ ∀ (m : R) (x : ↑X),
    { toFun := fun x ↦ s • (ConcreteCategory.hom g) x, map_add' := ⋯ }.toFun (m • x) =
      (RingHom.id R) m • { toFun := fun x ↦ s • (ConcreteCategory.hom g) x, map_add' := ⋯ }.toFun x

Tactic:
intro r

Goal state after:
R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
s : S
g : X ⟶ (restrictScalars f).obj Y
r : R
⊢ ∀ (x : ↑X),
    { toFun := fun x ↦ s • (ConcreteCategory.hom g) x, map_add' := ⋯ }.toFun (r • x) =
      (RingHom.id R) r • { toFun := fun x ↦ s • (ConcreteCategory.hom g) x, map_add' := ⋯ }.toFun x
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
g : X ⟶ (restrictScalars f).obj Y
m1 : Module R S := Module.compHom S f
⊢ (extendScalars f).obj X ⟶ Y

Tactic:
;

Goal state after:
R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
g : X ⟶ (restrictScalars f).obj Y
m1 : Module R S := Module.compHom S f
⊢ (extendScalars f).obj X ⟶ Y
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
g : (extendScalars f).obj X ⟶ Y
m1 : Module R S := Module.compHom S f
⊢ HomEquiv.fromExtendScalars f (HomEquiv.toRestrictScalars f g) = g

Tactic:
;

Goal state after:
R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
g : (extendScalars f).obj X ⟶ Y
m1 : Module R S := Module.compHom S f
⊢ HomEquiv.fromExtendScalars f (HomEquiv.toRestrictScalars f g) = g
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
g : (extendScalars f).obj X ⟶ Y
m1 : Module R S := ⋯
m2 : Module R ↑Y := ⋯
⊢ ∀ (x : ↑((extendScalars f).obj X)),
    (Hom.hom (HomEquiv.fromExtendScalars f (HomEquiv.toRestrictScalars f g))) x = (Hom.hom g) x

Tactic:
;

Goal state after:
R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
g : (extendScalars f).obj X ⟶ Y
m1 : Module R S := ⋯
m2 : Module R ↑Y := ⋯
⊢ ∀ (x : ↑((extendScalars f).obj X)),
    (Hom.hom (HomEquiv.fromExtendScalars f (HomEquiv.toRestrictScalars f g))) x = (Hom.hom g) x
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
g : X ⟶ (restrictScalars f).obj Y
m1 : Module R S := Module.compHom S f
⊢ HomEquiv.toRestrictScalars f (HomEquiv.fromExtendScalars f g) = g

Tactic:
;

Goal state after:
R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
g : X ⟶ (restrictScalars f).obj Y
m1 : Module R S := Module.compHom S f
⊢ HomEquiv.toRestrictScalars f (HomEquiv.fromExtendScalars f g) = g
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
X : ModuleCat R
x x' : ↑X
⊢ 1 ⊗ₜ[R] (x + x') = 1 ⊗ₜ[R] x + 1 ⊗ₜ[R] x'

Tactic:
;

Goal state after:
R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
X : ModuleCat R
x x' : ↑X
⊢ 1 ⊗ₜ[R] (x + x') = 1 ⊗ₜ[R] x + 1 ⊗ₜ[R] x'
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
X : ModuleCat R
r : R
x : ↑X
m1 : Module R S := Module.compHom S f
⊢ 1 ⊗ₜ[R] (r • x) = r • 1 ⊗ₜ[R] x

Tactic:
;

Goal state after:
R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
X : ModuleCat R
r : R
x : ↑X
m1 : Module R S := Module.compHom S f
⊢ 1 ⊗ₜ[R] (r • x) = r • 1 ⊗ₜ[R] x
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
Y : ModuleCat S
m1 : Module R S := Module.compHom S f
m2 : Module R ↑Y := Module.compHom (↑Y) f
s : S
r : R
y : ↑Y
⊢ s • f r • y = f r • s • y

Tactic:
← mul_smul,

Goal state after:
R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
Y : ModuleCat S
m1 : Module R S := Module.compHom S f
m2 : Module R ↑Y := Module.compHom (↑Y) f
s : S
r : R
y : ↑Y
⊢ (s * f r) • y = f r • s • y
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: case add
R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
Y Y' : ModuleCat S
g : Y ⟶ Y'
m1 : Module R S := Module.compHom S f
m2✝ : Module R ↑Y := Module.compHom (↑Y) f
m2 : Module R ↑Y' := Module.compHom (↑Y') f
x✝ y✝ : ↑((restrictScalars f).obj (of S S)) ⊗[R] ↑((restrictScalars f).obj Y)
ih₁ :
  (Hom.hom ((restrictScalars f ⋙ extendScalars f).map g ≫ Counit.map f)) x✝ =
    (Hom.hom (Counit.map f ≫ (𝟭 (ModuleCat S)).map g)) x✝
ih₂ :
  (Hom.hom ((restrictScalars f ⋙ extendScalars f).map g ≫ Counit.map f)) y✝ =
    (Hom.hom (Counit.map f ≫ (𝟭 (ModuleCat S)).map g)) y✝
⊢ (Hom.hom ((restrictScalars f ⋙ extendScalars f).map g ≫ Counit.map f)) x✝ +
      (Hom.hom ((restrictScalars f ⋙ extendScalars f).map g ≫ Counit.map f)) y✝ =
    (Hom.hom (Counit.map f ≫ (𝟭 (ModuleCat S)).map g)) x✝ + (Hom.hom (Counit.map f ≫ (𝟭 (ModuleCat S)).map g)) y✝

Tactic:
;

Goal state after:
case add
R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
Y Y' : ModuleCat S
g : Y ⟶ Y'
m1 : Module R S := Module.compHom S f
m2✝ : Module R ↑Y := Module.compHom (↑Y) f
m2 : Module R ↑Y' := Module.compHom (↑Y') f
x✝ y✝ : ↑((restrictScalars f).obj (of S S)) ⊗[R] ↑((restrictScalars f).obj Y)
ih₁ :
  (Hom.hom ((restrictScalars f ⋙ extendScalars f).map g ≫ Counit.map f)) x✝ =
    (Hom.hom (Counit.map f ≫ (𝟭 (ModuleCat S)).map g)) x✝
ih₂ :
  (Hom.hom ((restrictScalars f ⋙ extendScalars f).map g ≫ Counit.map f)) y✝ =
    (Hom.hom (Counit.map f ≫ (𝟭 (ModuleCat S)).map g)) y✝
⊢ (Hom.hom ((restrictScalars f ⋙ extendScalars f).map g ≫ Counit.map f)) x✝ +
      (Hom.hom ((restrictScalars f ⋙ extendScalars f).map g ≫ Counit.map f)) y✝ =
    (Hom.hom (Counit.map f ≫ (𝟭 (ModuleCat S)).map g)) x✝ + (Hom.hom (Counit.map f ≫ (𝟭 (ModuleCat S)).map g)) y✝
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: case add
R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
g : X ⟶ (restrictScalars f).obj Y
x✝ y✝ : ↑((restrictScalars f).obj (of S S)) ⊗[R] ↑X
a✝¹ :
  (Hom.hom ((ExtendRestrictScalarsAdj.homEquiv f).symm g)) x✝ =
    (Hom.hom ((extendScalars f).map g ≫ (ExtendRestrictScalarsAdj.counit f).app Y)) x✝
a✝ :
  (Hom.hom ((ExtendRestrictScalarsAdj.homEquiv f).symm g)) y✝ =
    (Hom.hom ((extendScalars f).map g ≫ (ExtendRestrictScalarsAdj.counit f).app Y)) y✝
⊢ (Hom.hom ((ExtendRestrictScalarsAdj.homEquiv f).symm g)) x✝ +
      (Hom.hom ((ExtendRestrictScalarsAdj.homEquiv f).symm g)) y✝ =
    (Hom.hom ((extendScalars f).map g ≫ (ExtendRestrictScalarsAdj.counit f).app Y)) x✝ +
      (Hom.hom ((extendScalars f).map g ≫ (ExtendRestrictScalarsAdj.counit f).app Y)) y✝

Tactic:
;

Goal state after:
case add
R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
g : X ⟶ (restrictScalars f).obj Y
x✝ y✝ : ↑((restrictScalars f).obj (of S S)) ⊗[R] ↑X
a✝¹ :
  (Hom.hom ((ExtendRestrictScalarsAdj.homEquiv f).symm g)) x✝ =
    (Hom.hom ((extendScalars f).map g ≫ (ExtendRestrictScalarsAdj.counit f).app Y)) x✝
a✝ :
  (Hom.hom ((ExtendRestrictScalarsAdj.homEquiv f).symm g)) y✝ =
    (Hom.hom ((extendScalars f).map g ≫ (ExtendRestrictScalarsAdj.counit f).app Y)) y✝
⊢ (Hom.hom ((ExtendRestrictScalarsAdj.homEquiv f).symm g)) x✝ +
      (Hom.hom ((ExtendRestrictScalarsAdj.homEquiv f).symm g)) y✝ =
    (Hom.hom ((extendScalars f).map g ≫ (ExtendRestrictScalarsAdj.counit f).app Y)) x✝ +
      (Hom.hom ((extendScalars f).map g ≫ (ExtendRestrictScalarsAdj.counit f).app Y)) y✝
Module: Mathlib.RingTheory.Coalgebra.TensorProduct

Goal state before:
pp: case e'_2.tmul.tmul
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid A
inst✝⁷ : AddCommMonoid B
inst✝⁶ : Algebra R S
inst✝⁵ : Module R A
inst✝⁴ : Module S A
inst✝³ : Module R B
inst✝² : IsScalarTower R S A
inst✝¹ : Coalgebra R B
inst✝ : Coalgebra S A
x : A
y : B
x₁ x₂ : A
y₁ y₂ : B
⊢ (LinearMap.lTensor (A ⊗[R] B) counit)
      ((AlgebraTensorModule.tensorTensorTensorComm R S R S A A B B) (x₁ ⊗ₜ[S] x₂ ⊗ₜ[R] (y₁ ⊗ₜ[R] y₂))) =
    (TensorProduct.rid S A) ((LinearMap.lTensor A counit) (x₁ ⊗ₜ[S] x₂)) ⊗ₜ[R]
        (TensorProduct.rid R B) ((LinearMap.lTensor B counit) (y₁ ⊗ₜ[R] y₂)) ⊗ₜ[S]
      1

Tactic:
apply (TensorProduct.rid S _).injective

Goal state after:
case e'_2.tmul.tmul
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid A
inst✝⁷ : AddCommMonoid B
inst✝⁶ : Algebra R S
inst✝⁵ : Module R A
inst✝⁴ : Module S A
inst✝³ : Module R B
inst✝² : IsScalarTower R S A
inst✝¹ : Coalgebra R B
inst✝ : Coalgebra S A
x : A
y : B
x₁ x₂ : A
y₁ y₂ : B
⊢ (TensorProduct.rid S (A ⊗[R] B))
      ((LinearMap.lTensor (A ⊗[R] B) counit)
        ((AlgebraTensorModule.tensorTensorTensorComm R S R S A A B B) (x₁ ⊗ₜ[S] x₂ ⊗ₜ[R] (y₁ ⊗ₜ[R] y₂)))) =
    (TensorProduct.rid S (A ⊗[R] B))
      ((TensorProduct.rid S A) ((LinearMap.lTensor A counit) (x₁ ⊗ₜ[S] x₂)) ⊗ₜ[R]
          (TensorProduct.rid R B) ((LinearMap.lTensor B counit) (y₁ ⊗ₜ[R] y₂)) ⊗ₜ[S]
        1)
Module: Mathlib.RingTheory.Coalgebra.TensorProduct

Goal state before:
pp: R✝ : Type u_1
S✝ : Type u_2
A : Type u_3
B : Type u_4
inst✝²⁷ : CommSemiring R✝
inst✝²⁶ : CommSemiring S✝
inst✝²⁵ : AddCommMonoid A
inst✝²⁴ : AddCommMonoid B
inst✝²³ : Algebra R✝ S✝
inst✝²² : Module R✝ A
inst✝²¹ : Module S✝ A
inst✝²⁰ : Module R✝ B
inst✝¹⁹ : IsScalarTower R✝ S✝ A
R : Type u_5
S : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
inst✝¹⁸ : CommSemiring R
inst✝¹⁷ : CommSemiring S
inst✝¹⁶ : Algebra R S
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : AddCommMonoid N
inst✝¹³ : AddCommMonoid P
inst✝¹² : AddCommMonoid Q
inst✝¹¹ : Module R M
inst✝¹⁰ : Module R N
inst✝⁹ : Module R P
inst✝⁸ : Module R Q
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower R S M
inst✝⁵ : Coalgebra S M
inst✝⁴ : Module S N
inst✝³ : IsScalarTower R S N
inst✝² : Coalgebra S N
inst✝¹ : Coalgebra R P
inst✝ : Coalgebra R Q
f : M →ₗc[S] N
g : P →ₗc[R] Q
x✝¹ : M
x✝ : P
⊢ ((AlgebraTensorModule.curry (counit ∘ₗ AlgebraTensorModule.map f.toLinearMap g.toLinearMap)) x✝¹) x✝ =
    ((AlgebraTensorModule.curry counit) x✝¹) x✝

Tactic:
;

Goal state after:
R✝ : Type u_1
S✝ : Type u_2
A : Type u_3
B : Type u_4
inst✝²⁷ : CommSemiring R✝
inst✝²⁶ : CommSemiring S✝
inst✝²⁵ : AddCommMonoid A
inst✝²⁴ : AddCommMonoid B
inst✝²³ : Algebra R✝ S✝
inst✝²² : Module R✝ A
inst✝²¹ : Module S✝ A
inst✝²⁰ : Module R✝ B
inst✝¹⁹ : IsScalarTower R✝ S✝ A
R : Type u_5
S : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
inst✝¹⁸ : CommSemiring R
inst✝¹⁷ : CommSemiring S
inst✝¹⁶ : Algebra R S
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : AddCommMonoid N
inst✝¹³ : AddCommMonoid P
inst✝¹² : AddCommMonoid Q
inst✝¹¹ : Module R M
inst✝¹⁰ : Module R N
inst✝⁹ : Module R P
inst✝⁸ : Module R Q
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower R S M
inst✝⁵ : Coalgebra S M
inst✝⁴ : Module S N
inst✝³ : IsScalarTower R S N
inst✝² : Coalgebra S N
inst✝¹ : Coalgebra R P
inst✝ : Coalgebra R Q
f : M →ₗc[S] N
g : P →ₗc[R] Q
x✝¹ : M
x✝ : P
⊢ ((AlgebraTensorModule.curry (counit ∘ₗ AlgebraTensorModule.map f.toLinearMap g.toLinearMap)) x✝¹) x✝ =
    ((AlgebraTensorModule.curry counit) x✝¹) x✝