mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.Grp.Colimits

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
inst✝ : DecidableEq J
j : J
x : ↑(F.obj j)
⊢ (((QuotientAddGroup.mk' (Relations (F ⋙ uliftFunctor))).comp
            (DFinsupp.singleAddHom (fun j ↦ ↑(uliftFunctor.obj (F.obj j))) j)).comp
        AddEquiv.ulift.symm.toAddMonoidHom)
      x =
    ((QuotientAddGroup.mk' (Relations (F ⋙ uliftFunctor))).comp
        (DFinsupp.singleAddHom (fun j ↦ ↑(uliftFunctor.obj (F.obj j))) j))
      { down := x }

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Colimits

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
inst✝ : DecidableEq J
j : J
x : ↑((F ⋙ uliftFunctor).obj j)
⊢ (quotUliftToQuot F) ((Quot.ι (F ⋙ uliftFunctor) j) x) = (Quot.ι F j) x.down

Tactic:
dsimp [quotUliftToQuot, Quot.ι]

Goal state after:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
inst✝ : DecidableEq J
j : J
x : ↑((F ⋙ uliftFunctor).obj j)
⊢ (QuotientAddGroup.lift (Relations (F ⋙ uliftFunctor))
        (DFinsupp.sumAddHom fun j ↦
          ((QuotientAddGroup.mk' (Relations F)).comp (DFinsupp.singleAddHom (fun j ↦ ↑(F.obj j)) j)).comp
            ↑AddEquiv.ulift)
        ⋯)
      (((QuotientAddGroup.mk' (Relations (F ⋙ uliftFunctor))).comp
          (DFinsupp.singleAddHom (fun j ↦ ↑(uliftFunctor.obj (F.obj j))) j))
        x) =
    ((QuotientAddGroup.mk' (Relations F)).comp (DFinsupp.singleAddHom (fun j ↦ ↑(F.obj j)) j)) x.down
Module: Mathlib.Algebra.Category.Grp.Colimits

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
inst✝ : DecidableEq J
j : J
x : ↑((F ⋙ uliftFunctor).obj j)
⊢ ((QuotientAddGroup.mk' (Relations F)).comp (DFinsupp.singleAddHom (fun j ↦ ↑(F.obj j)) j)) (↑AddEquiv.ulift x) =
    ((QuotientAddGroup.mk' (Relations F)).comp (DFinsupp.singleAddHom (fun j ↦ ↑(F.obj j)) j)) x.down

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Colimits

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
x : Quot (F ⋙ uliftFunctor)
j : J
a : ↑((F ⋙ uliftFunctor).obj j)
⊢ (Quot.ι (F ⋙ uliftFunctor) j) { down := a.down } = (Quot.ι (F ⋙ uliftFunctor) j) a

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Colimits

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
inst✝ : DecidableEq J
c : Cocone F
j : J
a : ↑(F.obj j)
⊢ (ConcreteCategory.hom ((uliftFunctor.mapCocone c).ι.app j)) { down := a } =
    AddEquiv.ulift.symm ((ConcreteCategory.hom (c.ι.app j)) a)

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Colimits

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
h : Function.Bijective ⇑(Quot.desc F c)
s : Cocone F
m : c.pt ⟶ s.pt
hm : ∀ (j : J), c.ι.app j ≫ m = s.ι.app j
x : Quot F
eq : (Hom.hom m).comp ↑(AddEquiv.ofBijective (Quot.desc F c) h) = Quot.desc F s
⊢ (Hom.hom m) ((AddEquiv.ofBijective (Quot.desc F c) h) x) =
    ((Hom.hom m).comp ↑(AddEquiv.ofBijective (Quot.desc F c) h)) x

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Colimits

Goal state before:
pp: G H : AddCommGrpCat
f : G ⟶ H
⊢ ofHom (mk' (Hom.hom f).range) ≫ ofHom (lift (Hom.hom f).range (Hom.hom (cokernel.π f)) ⋯) = cokernel.π f

Tactic:
rfl

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : NonAssocSemiring M
inst✝ : NonAssocSemiring N
c : RingCon M
f : M →+* N
h : ker f ≤ c
hf : Surjective ⇑f
x y : M
⊢ c x y → ∃ a b, c a b ∧ f a = f x ∧ f b = f y

Tactic:
grind

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

Goal state before:
pp: case mk
M : Type u_1
P : Type u_3
inst✝¹ : NonAssocSemiring M
inst✝ : NonAssocSemiring P
c : RingCon M
f : c.Quotient →+* P
x : c.Quotient
a✝ : M
⊢ (c.lift (f.comp c.mk') ⋯) (Quot.mk (⇑c.toSetoid) a✝) = f (Quot.mk (⇑c.toSetoid) a✝)

Tactic:
rfl

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

Goal state before:
pp: case e'_2.e'_6
M : Type u_1
N : Type u_2
inst✝¹ : NonAssocSemiring M
inst✝ : NonAssocSemiring N
c : RingCon M
f : N ≃+* M
d : RingCon N
hcd : d = c.comap f
x : N
⊢ ⟦f x⟧ = ↑(f x)

Tactic:
rfl

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

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : NonAssocSemiring M
inst✝¹ : NonAssocSemiring N
inst✝ : NonAssocSemiring P
c✝ : RingCon M
f : M →+* P
c d : RingCon M
h : c ≤ d
x y : (ker (c.map d h)).Quotient
w z : c.Quotient
a b : M
⊢ (c.quotientQuotientEquivQuotient d.toSetoid h).toFun (↑↑a * ↑↑b) = d.mk' (a * b)

Tactic:
rfl

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

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : NonAssocSemiring M
inst✝¹ : NonAssocSemiring N
inst✝ : NonAssocSemiring P
c✝ : RingCon M
f : M →+* P
c d : RingCon M
h : c ≤ d
x y : (ker (c.map d h)).Quotient
w z : c.Quotient
a b : M
⊢ (c.quotientQuotientEquivQuotient d.toSetoid h).toFun (↑↑a + ↑↑b) = d.mk' (a + b)

Tactic:
rfl

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

Goal state before:
pp: M : Type u_1
P : Type u_3
R : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring M
inst✝² : Algebra R M
inst✝¹ : Semiring P
inst✝ : Algebra R P
f : M →ₐ[R] P
x : M
⊢ (kerLiftₐ f) ↑x = f x

Tactic:
rfl

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

Goal state before:
pp: M : Type u_1
P : Type u_3
R : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring M
inst✝² : Algebra R M
inst✝¹ : Semiring P
inst✝ : Algebra R P
f : M →ₐ[R] P
x : M
⊢ ↑((quotientKerEquivRangeₐ f) ↑x) = f x

Tactic:
rfl

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

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
R : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring M
inst✝⁴ : Algebra R M
inst✝³ : Semiring N
inst✝² : Algebra R N
inst✝¹ : Semiring P
inst✝ : Algebra R P
c✝ d✝ : RingCon M
f : M →ₐ[R] P
c d : RingCon M
h : c ≤ d
x✝ : R
⊢ (c.quotientQuotientEquivQuotient d h).toFun ((algebraMap R (ker ↑(factorₐ R h)).Quotient) x✝) =
    (algebraMap R d.Quotient) x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : M
⊢ (RingCon.mkₐ R (ringCon R M)) (FreeAlgebra.ι R m) =
    { toFun := fun m ↦ ↑(FreeAlgebra.ι R m), map_add' := ⋯, map_smul' := ⋯ } m

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
F : TensorAlgebra R M →ₐ[R] A
x : M
⊢ F ↑(FreeAlgebra.ι R x) = F ↑(FreeAlgebra.ι R x)

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : M →ₗ[R] A
x : M
⊢ ((lift R) f) ((ι R) x) = (((lift R) f).toLinearMap ∘ₗ ι R) x

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
C : TensorAlgebra R M → Prop
algebraMap : ∀ (r : R), C ((Algebra.algebraMap R (TensorAlgebra R M)) r)
ι : ∀ (x : M), C ((TensorAlgebra.ι R) x)
mul : ∀ (a b : TensorAlgebra R M), C a → C b → C (a * b)
add : ∀ (a b : TensorAlgebra R M), C a → C b → C (a + b)
a : TensorAlgebra R M
s : Subalgebra R (TensorAlgebra R M) :=
  { carrier := {a | C a}, mul_mem' := mul, one_mem' := ⋯, add_mem' := add, zero_mem' := ⋯,
    algebraMap_mem' := algebraMap }
of : M →ₗ[R] ↥s := LinearMap.codRestrict (Subalgebra.toSubmodule s) (TensorAlgebra.ι R) ι
x : M
⊢ ↑(of x) = (TensorAlgebra.ι R) x

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
n✝ : ℕ
h : x.snd <• x.fst = x.fst •> x.snd
n : ℕ
⊢ ∀ x_1 ∈ List.map (fun i ↦ x.fst ^ (n - i + i) •> x.snd) (List.range n.succ), x_1 = x.fst ^ n •> x.snd

Tactic:
grind

Goal state after:
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: case succ
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
n✝ : ℕ
⊢ (x.fst ^ n✝ * x.fst) •> x.snd +
      (List.map (fun i ↦ x.fst ^ (n✝ - i) •> (x.snd <• (x.fst ^ i * x.fst))) (List.range (n✝ + 1))).sum =
    (x.fst ^ n✝ * x.fst) •> x.snd +
      (List.map (fun x_1 ↦ x.fst ^ (n✝ - x_1) •> (op x.fst * op (x.fst ^ x_1)) •> x.snd) (List.range (n✝ + 1))).sum

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Mates

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ : C ⥤ D
R₁ R₂ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : R₁ ⟶ R₂
c : C
⊢ adj₁.unit.app c ≫ α.app (L₁.obj c) = adj₂.unit.app c ≫ R₂.map (((conjugateEquiv adj₁ adj₂).symm α).app c)

Tactic:
conv_lhs => rw [← (conjugateEquiv adj₁ adj₂).right_inv α]
    exact (unit_conjugateEquiv adj₁ adj₂ ((conjugateEquiv adj₁ adj₂).symm α) c)

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
⊢ (LinearMap.rTensor R LinearMap.id ∘ₗ (TensorProduct.mk R R R) 1) 1 = ((TensorProduct.mk R R R) 1) 1

Tactic:
rfl

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
⊢ (LinearMap.lTensor R LinearMap.id ∘ₗ (TensorProduct.mk R R R) 1) 1 = ((TensorProduct.mk R R R).flip 1) 1

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: case h2
R : Type u
M : Type v
inst✝³ : DivisionSemiring R
inst✝² : AddCommGroup M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
m : M
⊢ -(0⁻¹ •> m <• 0⁻¹) = snd 0

Tactic:
inv_zero,

Goal state after:
case h2
R : Type u
M : Type v
inst✝³ : DivisionSemiring R
inst✝² : AddCommGroup M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
m : M
⊢ -(0 •> m <• 0) = snd 0
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : DivisionSemiring R
inst✝² : AddCommGroup M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
x : tsze R M
hx : x.fst ≠ 0
⊢ x⁻¹ * x = 1

Tactic:
convert mul_left_eq_one _ _ (_root_.inv_mul_cancel₀ hx)

Goal state after:
R : Type u
M : Type v
inst✝³ : DivisionSemiring R
inst✝² : AddCommGroup M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
x : tsze R M
hx : x.fst ≠ 0
⊢ x⁻¹ = inl x.fst⁻¹ + inr (-(x.fst⁻¹ •> x.snd <• x.fst⁻¹))
Module: Mathlib.RingTheory.Coalgebra.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✝¹¹ : AddCommMonoid A
inst✝¹⁰ : Module R A
inst✝⁹ : AddCommMonoid B
inst✝⁸ : Module R B
inst✝⁷ : AddCommMonoid C
inst✝⁶ : Module R C
inst✝⁵ : AddCommMonoid D
inst✝⁴ : Module R D
inst✝³ : CoalgebraStruct R A
inst✝² : CoalgebraStruct R B
inst✝¹ : CoalgebraStruct R C
inst✝ : CoalgebraStruct R D
x✝ : A
⊢ (counit ∘ₗ LinearMap.id) x✝ = counit x✝

Tactic:
rfl

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

Goal state before:
pp: R : Type u
A : Type v
B : Type w
ι : Type u_1
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid A
inst✝⁶ : AddCommMonoid B
inst✝⁵ : Module R A
inst✝⁴ : Module R B
inst✝³ : Coalgebra R A
inst✝² : Coalgebra R B
a : A
repr : Repr R a ι
F : Type u_2
inst✝¹ : FunLike F A B
inst✝ : CoalgHomClass F R A B
φ : F
⊢ ∑ x ∈ repr.index, (map ↑φ ↑φ) (repr.left x ⊗ₜ[R] repr.right x) =
    ∑ i ∈ repr.index, (⇑φ ∘ repr.left) i ⊗ₜ[R] (⇑φ ∘ repr.right) i

Tactic:
rfl

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : CoalgebraStruct R M
x : n →₀ M
⊢ (counit ∘ₗ Finsupp.lcoeFun) x = counit x

Tactic:
← Finsupp.univ_sum_single x

Goal state after:
R : Type u_1
n : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : CoalgebraStruct R M
x : n →₀ M
⊢ (counit ∘ₗ Finsupp.lcoeFun) (∑ a, Finsupp.single a (x a)) = counit (∑ a, Finsupp.single a (x a))
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : CoalgebraStruct R M
x : n →₀ M
⊢ (comul ∘ₗ lcoeFun) x = (map lcoeFun lcoeFun ∘ₗ comul) x

Tactic:
← Finsupp.univ_sum_single x

Goal state after:
R : Type u_1
n : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : CoalgebraStruct R M
x : n →₀ M
⊢ (comul ∘ₗ lcoeFun) (∑ a, Finsupp.single a (x a)) = (map lcoeFun lcoeFun ∘ₗ comul) (∑ a, Finsupp.single a (x a))
Module: Mathlib.RingTheory.Bialgebra.Hom

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : CoalgebraStruct R A
inst✝ : CoalgebraStruct R B
f : A →ₗc[R] B
h : f.toFun 1 = 1
h₁ : ∀ (x y : A), f.toFun (x * y) = f.toFun x * f.toFun y
⊢ ↑{ toCoalgHom := f, map_one' := h, map_mul' := h₁ } = f

Tactic:
rfl

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : CoalgebraStruct R A
inst✝ : CoalgebraStruct R B
f : A →ₐc[R] B
⊢ ↑↑f = ↑f

Tactic:
rfl

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 : R →+* S
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:
rfl

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 : R →+* S
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 f).map x✝

Tactic:
rfl

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:
rfl

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

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

Tactic:
rfl

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:
rfl

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₃
M : ModuleCat R₃
r : R₁
x : ↑((restrictScalars (g.comp f)).obj M)
⊢ (AddEquiv.refl ↑((restrictScalars (g.comp f)).obj M)) (r • x) =
    r • (AddEquiv.refl ↑((restrictScalars (g.comp f)).obj M)) x

Tactic:
rfl

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

Goal state before:
pp: case zero
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₃
⊢ (Hom.hom (map' f (l₁₂ ≫ l₂₃))) 0 = (Hom.hom (map' f l₁₂ ≫ map' f l₂₃)) 0

Tactic:
rfl

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

Goal state before:
pp: case tmul
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₃
x✝ : ↑((restrictScalars f).obj (of S S))
y✝ : ↑M₁
⊢ (Hom.hom (map' f (l₁₂ ≫ l₂₃))) (x✝ ⊗ₜ[R] y✝) = (Hom.hom (map' f l₁₂ ≫ map' f l₂₃)) (x✝ ⊗ₜ[R] y✝)

Tactic:
rfl

Goal state after:
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
M₁ M₂ M₃ : ModuleCat R
l₁₂ : M₁ ⟶ M₂
l₂₃ : M₂ ⟶ M₃
x✝ y✝ : ↑((restrictScalars f).obj (of S S)) ⊗[R] ↑M₁
ihx : (Hom.hom (map' f (l₁₂ ≫ l₂₃))) x✝ = (Hom.hom (map' f l₁₂ ≫ map' f l₂₃)) x✝
ihy : (Hom.hom (map' f (l₁₂ ≫ l₂₃))) y✝ = (Hom.hom (map' f l₁₂ ≫ map' f l₂₃)) y✝
⊢ (Hom.hom (map' f (l₁₂ ≫ l₂₃))) x✝ + (Hom.hom (map' f (l₁₂ ≫ l₂₃))) y✝ =
    (Hom.hom (map' f l₁₂ ≫ map' f l₂₃)) x✝ + (Hom.hom (map' f l₁₂ ≫ map' f l₂₃)) y✝

Tactic:
grind

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
x✝ : ↑((forget₂ (CoalgCat R) (ModuleCat R)).obj (X ⊗ Y))
⊢ (ModuleCat.Hom.hom ((forget₂ (CoalgCat R) (ModuleCat R)).map (X ◁ f))) x✝ =
    (ModuleCat.Hom.hom
        ((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))
      x✝

Tactic:
rfl

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
x✝ : ↑((forget₂ (CoalgCat R) (ModuleCat R)).obj (X₁✝ ⊗ f))
⊢ (ModuleCat.Hom.hom ((forget₂ (CoalgCat R) (ModuleCat R)).map (X ▷ f))) x✝ =
    (ModuleCat.Hom.hom
        ((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))
      x✝

Tactic:
rfl

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₂✝
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:
rfl

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
X Y Z : CoalgCat R
x✝² : ↑X.toModuleCat
x✝¹ : ↑Y.toModuleCat
x✝ : ↑Z.toModuleCat
⊢ ((((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))))
          x✝²)
        x✝¹)
      x✝ =
    ((((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)))
          x✝²)
        x✝¹)
      x✝

Tactic:
rfl

Goal state after:
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:
rfl

Goal state after:
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:
rfl

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
x✝ : ↑(CoextendScalars.obj' f x✝¹)
⊢ (Hom.hom (CoextendScalars.map' f (𝟙 x✝¹))) x✝ = (Hom.hom (𝟙 (CoextendScalars.obj' f x✝¹))) x✝

Tactic:
rfl

Goal state after: