mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R : Type u₁
S : Type u₂
inst✝¹ : Ring R
inst✝ : Ring S
f g : R →+* S
e : f = g
X : ModuleCat S
x✝¹ : R
x✝ : ↑((restrictScalars f).obj X)
⊢ (AddEquiv.refl ↑((restrictScalars f).obj X)).toFun (x✝¹ • x✝) =
    (RingHom.id R) x✝¹ • (AddEquiv.refl ↑((restrictScalars f).obj X)).toFun x✝

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Bialgebra.Hom

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A
inst✝¹⁰ : Semiring B
inst✝⁹ : Semiring C
inst✝⁸ : Semiring D
inst✝⁷ : Algebra R A
inst✝⁶ : Algebra R B
inst✝⁵ : Algebra R C
inst✝⁴ : Algebra R D
inst✝³ : CoalgebraStruct R A
inst✝² : CoalgebraStruct R B
inst✝¹ : CoalgebraStruct R C
inst✝ : CoalgebraStruct R D
φ f : A →ₐc[R] B
f' : A → B
h : f' = ⇑f
⊢ ((↑f).copy f' h).toFun 1 = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R : Type u₁
S : Type u₂
inst✝¹ : Ring R
inst✝ : Ring S
f g : R →+* S
e : f = g
X✝ Y✝ : ModuleCat S
x✝ : X✝ ⟶ Y✝
⊢ (restrictScalars f).map x✝ ≫
      (let __spread.0 := AddEquiv.refl ↑((restrictScalars f).obj Y✝);
          { toFun := __spread.0.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __spread.0.invFun, left_inv := ⋯,
            right_inv := ⋯ }).toModuleIso.hom =
    (let __spread.0 := AddEquiv.refl ↑((restrictScalars f).obj X✝);
          { toFun := __spread.0.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __spread.0.invFun, left_inv := ⋯,
            right_inv := ⋯ }).toModuleIso.hom ≫
      (restrictScalars g).map x✝

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Bialgebra.Hom

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A
inst✝¹⁰ : Semiring B
inst✝⁹ : Semiring C
inst✝⁸ : Semiring D
inst✝⁷ : Algebra R A
inst✝⁶ : Algebra R B
inst✝⁵ : Algebra R C
inst✝⁴ : Algebra R D
inst✝³ : CoalgebraStruct R A
inst✝² : CoalgebraStruct R B
inst✝¹ : CoalgebraStruct R C
inst✝ : CoalgebraStruct R D
φ f : A →ₐc[R] B
f' : A → B
h : f' = ⇑f
⊢ ∀ (x y : A), ((↑f).copy f' h).toFun (x * y) = ((↑f).copy f' h).toFun x * ((↑f).copy f' h).toFun y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R : Type u₁
inst✝ : Ring R
f : R →+* R
hf : f = RingHom.id R
M : ModuleCat R
⊢ ↑((restrictScalars f).obj M) ≃+ ↑M

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R : Type u₁
inst✝ : Ring R
f : R →+* R
hf : f = RingHom.id R
M : ModuleCat R
r : R
x : ↑((restrictScalars f).obj M)
⊢ (AddEquiv.refl ↑((restrictScalars f).obj M)) (r • x) = r • (AddEquiv.refl ↑((restrictScalars f).obj M)) x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R₁ : Type u₁
R₂ : Type u₂
R₃ : Type u₃
inst✝² : Ring R₁
inst✝¹ : Ring R₂
inst✝ : Ring R₃
f : R₁ →+* R₂
g : R₂ →+* R₃
gf : R₁ →+* R₃
hgf : gf = g.comp f
M : ModuleCat R₃
⊢ ↑((restrictScalars gf).obj M) ≃+ ↑((restrictScalars f).obj ((restrictScalars g).obj M))

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Bialgebra.Hom

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Bialgebra R A
⊢ (counitAlgHom R A).comp (Algebra.ofId R A) = counitAlgHom R R

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Bialgebra.Hom

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Bialgebra R A
⊢ (Algebra.TensorProduct.map (Algebra.ofId R A) (Algebra.ofId R A)).comp (comulAlgHom R R) =
    (comulAlgHom R A).comp (Algebra.ofId R A)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R₁ : Type u₁
R₂ : Type u₂
R₃ : Type u₃
inst✝² : Ring R₁
inst✝¹ : Ring R₂
inst✝ : Ring R₃
f : R₁ →+* R₂
g : R₂ →+* R₃
gf : R₁ →+* R₃
hgf : gf = g.comp f
M : ModuleCat R₃
r : R₁
x : ↑((restrictScalars gf).obj M)
⊢ (AddEquiv.refl ↑((restrictScalars gf).obj M)) (r • x) = r • (AddEquiv.refl ↑((restrictScalars gf).obj M)) x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
e : R ≃+* S
this : Module R ↑(of S S) := e.toRingHom.toModule
x : R
y : ↑(of S S)
⊢ e.symm.toFun (x • y) = (RingHom.id R) x • e.symm.toFun y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R₀ : Type u_1
R : Type u_2
S : Type u_3
inst✝⁴ : CommSemiring R₀
inst✝³ : Ring R
inst✝² : Ring S
inst✝¹ : Algebra R₀ R
inst✝ : Algebra R₀ S
f : R →ₐ[R₀] S
M N : ModuleCat S
g : M ⟶ N
r₀ : R₀
⊢ (restrictScalars f.toRingHom).map (r₀ • g) = r₀ • (restrictScalars f.toRingHom).map g

Tactic:
by

Goal state after:
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
M : ModuleCat R
⊢ map' f (𝟙 M) = 𝟙 (obj' f M)

Tactic:
by

Goal state after:
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
M₁ M₂ M₃ : ModuleCat R
l₁₂ : M₁ ⟶ M₂
l₂₃ : M₂ ⟶ M₃
⊢ map' f (l₁₂ ≫ l₂₃) = map' f l₁₂ ≫ map' f l₂₃

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Bialgebra.Equiv

Goal state before:
pp: R : Type u
A : Type v
B : Type w
C : Type u₁
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Bialgebra R A
inst✝ : Bialgebra R B
f : A →ₐc[R] B
hf : Bijective ⇑f
⊢ (counitAlgHom R B).comp ↑(AlgEquiv.ofBijective (↑f) hf) = counitAlgHom R A

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Bialgebra.Equiv

Goal state before:
pp: R : Type u
A : Type v
B : Type w
C : Type u₁
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Bialgebra R A
inst✝ : Bialgebra R B
f : A →ₐc[R] B
hf : Bijective ⇑f
⊢ (Algebra.TensorProduct.map ↑(AlgEquiv.ofBijective (↑f) hf) ↑(AlgEquiv.ofBijective (↑f) hf)).comp (comulAlgHom R A) =
    (comulAlgHom R B).comp ↑(AlgEquiv.ofBijective (↑f) hf)

Tactic:
by

Goal state after:
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
M : ModuleCat R
N : ModuleCat S
α β : (extendScalars f).obj M ⟶ N
h : ∀ (m : ↑M), (ConcreteCategory.hom α) (1 ⊗ₜ[R] m) = (ConcreteCategory.hom β) (1 ⊗ₜ[R] m)
this : Algebra R S := f.toAlgebra
s : S
m : ↑M
⊢ s ⊗ₜ[R] m = s • 1 ⊗ₜ[R] m

Tactic:
by

Goal state after:
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
M : ModuleCat R
N : ModuleCat S
α β : (extendScalars f).obj M ⟶ N
h : ∀ (m : ↑M), (ConcreteCategory.hom α) (1 ⊗ₜ[R] m) = (ConcreteCategory.hom β) (1 ⊗ₜ[R] m)
⊢ α = β

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.CoalgCat.Monoidal

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

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.CoalgCat.Monoidal

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

Tactic:
by

Goal state after:
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₂✝
⊢ (forget₂ (CoalgCat R) (ModuleCat R)).map (f ⊗ₘ g) =
    (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

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.CoalgCat.Monoidal

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

Tactic:
by

Goal state after:
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 : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : S
g : ↑((restrictScalars f).obj (of S S)) →ₗ[R] M
x y : S
⊢ g ((x + y) * s) = g (x * s) + g (y * s)

Tactic:
by

Goal state after:
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 : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : S
g : ↑((restrictScalars f).obj (of S S)) →ₗ[R] M
r : R
t : S
⊢ g (r • t * s) = (RingHom.id R) r • g (t * s)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.CoalgCat.Monoidal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
X : CoalgCat R
⊢ (TensorProduct.mk R ↑(𝟙_ (CoalgCat R)).toModuleCat ↑X.toModuleCat).compr₂ₛₗ
      (ModuleCat.Hom.hom ((forget₂ (CoalgCat R) (ModuleCat R)).map (λ_ X).hom)) =
    (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)

Tactic:
by

Goal state after:
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 : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s t : S
g : ↑((restrictScalars f).obj (of S S)) →ₗ[R] M
x : S
⊢ ((s * t) • g) x = (s • t • g) x

Tactic:
by

Goal state after:
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 : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
g : ↑((restrictScalars f).obj (of S S)) →ₗ[R] M
s : S
⊢ (1 • g) s = g s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.CoalgCat.Monoidal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
X : CoalgCat R
⊢ (TensorProduct.mk R ↑X.toModuleCat ↑(𝟙_ (CoalgCat R)).toModuleCat).compr₂ₛₗ
      (ModuleCat.Hom.hom ((forget₂ (CoalgCat R) (ModuleCat R)).map (ρ_ X).hom)) =
    (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)

Tactic:
by

Goal state after:
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 : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x✝¹ x✝ : S
⊢ (x✝¹ • 0) x✝ = 0 x✝

Tactic:
by

Goal state after:
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 : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : S
g h : ↑((restrictScalars f).obj (of S S)) →ₗ[R] M
x✝ : S
⊢ (s • (g + h)) x✝ = (s • g + s • h) x✝

Tactic:
by

Goal state after:
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 : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s1 s2 : S
g : ↑((restrictScalars f).obj (of S S)) →ₗ[R] M
x : S
⊢ ((s1 + s2) • g) x = (s1 • g + s2 • g) x

Tactic:
by

Goal state after:
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 : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
g : ↑((restrictScalars f).obj (of S S)) →ₗ[R] M
x : S
⊢ (0 • g) x = 0 x

Tactic:
by

Goal state after:
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
⊢ Hom.hom g ∘ₗ (s • h) = (RingHom.id S) s • Hom.hom g ∘ₗ h

Tactic:
by

Goal state after:
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
⊢ CoextendScalars.map' f (𝟙 x✝) = 𝟙 (CoextendScalars.obj' f x✝)

Tactic:
by

Goal state after:
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✝
⊢ CoextendScalars.map' f (x✝¹ ≫ x✝) = CoextendScalars.map' f x✝¹ ≫ CoextendScalars.map' f x✝

Tactic:
by

Goal state after:
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
Y : ModuleCat S
g : (restrictScalars f).obj Y ⟶ X
y : ↑Y
s1 s2 : S
⊢ (ConcreteCategory.hom g) ((s1 + s2) • y) = (ConcreteCategory.hom g) (s1 • y) + (ConcreteCategory.hom g) (s2 • y)

Tactic:
by

Goal state after:
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
Y : ModuleCat S
g : (restrictScalars f).obj Y ⟶ X
y : ↑Y
r : R
s : S
⊢ (ConcreteCategory.hom g) ((r • s) • y) = (RingHom.id R) r • (ConcreteCategory.hom g) (s • y)

Tactic:
by

Goal state after:
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
Y : ModuleCat S
g : (restrictScalars f).obj Y ⟶ X
y1 y2 : ↑Y
s : S
⊢ ((CoextendScalars.equiv f X)
        ((CoextendScalars.equiv f X).symm
          { toFun := fun s ↦ (ConcreteCategory.hom g) (s • (y1 + y2)), map_add' := ⋯, map_smul' := ⋯ }))
      s =
    ((CoextendScalars.equiv f X)
        ((CoextendScalars.equiv f X).symm
            { toFun := fun s ↦ (ConcreteCategory.hom g) (s • y1), map_add' := ⋯, map_smul' := ⋯ } +
          (CoextendScalars.equiv f X).symm
            { toFun := fun s ↦ (ConcreteCategory.hom g) (s • y2), map_add' := ⋯, map_smul' := ⋯ }))
      s

Tactic:
by

Goal state after:
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
Y : ModuleCat S
g : (restrictScalars f).obj Y ⟶ X
s : S
y : ↑Y
t : S
⊢ ((CoextendScalars.equiv f X)
        ((CoextendScalars.equiv f X).symm
          { toFun := fun s_1 ↦ (ConcreteCategory.hom g) (s_1 • s • y), map_add' := ⋯, map_smul' := ⋯ }))
      t =
    ((CoextendScalars.equiv f X)
        ((RingHom.id S) s •
          (CoextendScalars.equiv f X).symm
            { toFun := fun s ↦ (ConcreteCategory.hom g) (s • y), map_add' := ⋯, map_smul' := ⋯ }))
      t

Tactic:
by

Goal state after:
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
Y : ModuleCat S
g : Y ⟶ (coextendScalars f).obj X
x y : ↑((restrictScalars f).obj Y)
⊢ ((CoextendScalars.equiv f X) ((ConcreteCategory.hom g) (x + y))) 1 =
    ((CoextendScalars.equiv f X) ((ConcreteCategory.hom g) x)) 1 +
      ((CoextendScalars.equiv f X) ((ConcreteCategory.hom g) y)) 1

Tactic:
by

Goal state after:
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
Y : ModuleCat S
g : Y ⟶ (coextendScalars f).obj X
r : R
y : ↑Y
⊢ ((CoextendScalars.equiv f X) ((ConcreteCategory.hom g) (r • y))) 1 =
    (RingHom.id R) r • ((CoextendScalars.equiv f X) ((ConcreteCategory.hom g) y)) 1

Tactic:
by

Goal state after:
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
Y : ModuleCat S
y : ↑Y
r : R
s : S
⊢ (r • s) • y = (RingHom.id R) r • s • y

Tactic:
by

Goal state after:
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
Y : ModuleCat S
y1 y2 : ↑Y
s : S
⊢ ((CoextendScalars.equiv f ((restrictScalars f).obj Y))
        ((CoextendScalars.equiv f ((restrictScalars f).obj Y)).symm
          { toFun := fun s ↦ s • (y1 + y2), map_add' := ⋯, map_smul' := ⋯ }))
      s =
    ((CoextendScalars.equiv f ((restrictScalars f).obj Y))
        ((CoextendScalars.equiv f ((restrictScalars f).obj Y)).symm
            { toFun := fun s ↦ s • y1, map_add' := ⋯, map_smul' := ⋯ } +
          (CoextendScalars.equiv f ((restrictScalars f).obj Y)).symm
            { toFun := fun s ↦ s • y2, map_add' := ⋯, map_smul' := ⋯ }))
      s

Tactic:
by

Goal state after:
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
Y : ModuleCat S
s : S
y : ↑Y
t : S
⊢ ((CoextendScalars.equiv f ((restrictScalars f).obj Y))
        ((CoextendScalars.equiv f ((restrictScalars f).obj Y)).symm
          { toFun := fun s_1 ↦ s_1 • s • y, map_add' := ⋯, map_smul' := ⋯ }))
      t =
    ((CoextendScalars.equiv f ((restrictScalars f).obj Y))
        ((RingHom.id S) s •
          (CoextendScalars.equiv f ((restrictScalars f).obj Y)).symm
            { toFun := fun s ↦ s • y, map_add' := ⋯, map_smul' := ⋯ }))
      t

Tactic:
by

Goal state after:
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
Y Y' : ModuleCat S
g : Y ⟶ Y'
y : ↑Y
s : S
⊢ ((CoextendScalars.equiv f ((restrictScalars f).obj Y')) ((Hom.hom ((𝟭 (ModuleCat S)).map g ≫ ↟(app' f Y'))) y)) s =
    ((CoextendScalars.equiv f ((restrictScalars f).obj Y'))
        ((Hom.hom (↟(app' f Y) ≫ (restrictScalars f ⋙ coextendScalars f).map g)) y))
      s

Tactic:
by

Goal state after:
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
x1 x2 : ↑((restrictScalars f).obj ((coextendScalars f).obj X))
⊢ ((CoextendScalars.equiv f X) (x1 + x2)) 1 = ((CoextendScalars.equiv f X) x1) 1 + ((CoextendScalars.equiv f X) x2) 1

Tactic:
by

Goal state after:
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
r : R
g : ↑((restrictScalars f).obj ((coextendScalars f).obj X))
⊢ ((CoextendScalars.equiv f X) (r • g)) 1 = (RingHom.id R) r • ((CoextendScalars.equiv f X) g) 1

Tactic:
by

Goal state after:
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
⊢ RestrictionCoextensionAdj.HomEquiv.toRestriction f (RestrictionCoextensionAdj.HomEquiv.fromRestriction f g) = g

Tactic:
by

Goal state after:
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
⊢ RestrictionCoextensionAdj.HomEquiv.fromRestriction f (RestrictionCoextensionAdj.HomEquiv.toRestriction f g) = g

Tactic:
by

Goal state after: