mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Adjunction.FullyFaithful

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : L.Full
inst✝ : L.Faithful
this : R.whiskerLeft h.unit ≫ (R.associator L R).inv ≫ whiskerRight h.counit R = R.rightUnitor.hom ≫ R.leftUnitor.inv
⊢ IsIso (whiskerRight h.counit R)

Tactic:
rw [← IsIso.eq_inv_comp, Iso.inv_comp_eq] at this

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : L.Full
inst✝ : L.Faithful
this :
  whiskerRight h.counit R = (R.associator L R).hom ≫ inv (R.whiskerLeft h.unit) ≫ R.rightUnitor.hom ≫ R.leftUnitor.inv
⊢ IsIso (whiskerRight h.counit R)
Module: Mathlib.CategoryTheory.Monoidal.Linear

Goal state before:
pp: R : Type u_1
inst✝¹⁴ : Semiring R
C : Type u_2
inst✝¹³ : Category.{v_1, u_2} C
inst✝¹² : Preadditive C
inst✝¹¹ : Linear R C
inst✝¹⁰ : MonoidalCategory C
inst✝⁹ : MonoidalPreadditive C
inst✝⁸ : MonoidalLinear R C
D : Type u_3
inst✝⁷ : Category.{v_2, u_3} D
inst✝⁶ : Preadditive D
inst✝⁵ : Linear R D
inst✝⁴ : MonoidalCategory D
inst✝³ : MonoidalPreadditive D
F : D ⥤ C
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : Functor.Linear R F
X Y : D
⊢ ∀ {Z : D} (r : R) (f : Y ⟶ Z), X ◁ (r • f) = r • X ◁ f

Tactic:
Z

Goal state after:
R : Type u_1
inst✝¹⁴ : Semiring R
C : Type u_2
inst✝¹³ : Category.{v_1, u_2} C
inst✝¹² : Preadditive C
inst✝¹¹ : Linear R C
inst✝¹⁰ : MonoidalCategory C
inst✝⁹ : MonoidalPreadditive C
inst✝⁸ : MonoidalLinear R C
D : Type u_3
inst✝⁷ : Category.{v_2, u_3} D
inst✝⁶ : Preadditive D
inst✝⁵ : Linear R D
inst✝⁴ : MonoidalCategory D
inst✝³ : MonoidalPreadditive D
F : D ⥤ C
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : Functor.Linear R F
X Y Z : D
⊢ ∀ (r : R) (f : Y ⟶ Z), X ◁ (r • f) = r • X ◁ f
Module: Mathlib.CategoryTheory.Monoidal.Linear

Goal state before:
pp: R : Type u_1
inst✝¹⁴ : Semiring R
C : Type u_2
inst✝¹³ : Category.{v_1, u_2} C
inst✝¹² : Preadditive C
inst✝¹¹ : Linear R C
inst✝¹⁰ : MonoidalCategory C
inst✝⁹ : MonoidalPreadditive C
inst✝⁸ : MonoidalLinear R C
D : Type u_3
inst✝⁷ : Category.{v_2, u_3} D
inst✝⁶ : Preadditive D
inst✝⁵ : Linear R D
inst✝⁴ : MonoidalCategory D
inst✝³ : MonoidalPreadditive D
F : D ⥤ C
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : Functor.Linear R F
r : R
X Y : D
f : X ⟶ Y
⊢ ∀ (X_1 : D), (r • f) ▷ X_1 = r • f ▷ X_1

Tactic:
Z

Goal state after:
R : Type u_1
inst✝¹⁴ : Semiring R
C : Type u_2
inst✝¹³ : Category.{v_1, u_2} C
inst✝¹² : Preadditive C
inst✝¹¹ : Linear R C
inst✝¹⁰ : MonoidalCategory C
inst✝⁹ : MonoidalPreadditive C
inst✝⁸ : MonoidalLinear R C
D : Type u_3
inst✝⁷ : Category.{v_2, u_3} D
inst✝⁶ : Preadditive D
inst✝⁵ : Linear R D
inst✝⁴ : MonoidalCategory D
inst✝³ : MonoidalPreadditive D
F : D ⥤ C
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : Functor.Linear R F
r : R
X Y : D
f : X ⟶ Y
Z : D
⊢ (r • f) ▷ Z = r • f ▷ Z
Module: Mathlib.CategoryTheory.Monoidal.Discrete

Goal state before:
pp: M : Type u
inst✝ : Monoid M
X x✝¹ x✝ : Discrete M
f : x✝¹ ⟶ x✝
⊢ { as := X.as * x✝¹.as } = { as := X.as * x✝.as }

Tactic:
rw [eq_of_hom f]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Discrete

Goal state before:
pp: M : Type u
inst✝ : Monoid M
X₁✝ X₂✝ : Discrete M
f : X₁✝ ⟶ X₂✝
X : Discrete M
⊢ { as := X₁✝.as * X.as } = { as := X₂✝.as * X.as }

Tactic:
rw [eq_of_hom f]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
M : SemimoduleCat R
N : SemimoduleCat R
⊢ tensorHom (𝟙 M) (𝟙 N) = 𝟙 (of R (↑M ⊗[R] ↑N))

Tactic:
ext : 1

Goal state after:
R : Type u
inst✝ : CommSemiring R
M : SemimoduleCat R
N : SemimoduleCat R
⊢ Hom.hom (tensorHom (𝟙 M) (𝟙 N)) = Hom.hom (𝟙 (of R (↑M ⊗[R] ↑N)))
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
X₁ Y₁ Z₁ : SemimoduleCat R
X₂ Y₂ Z₂ : SemimoduleCat R
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ tensorHom f₁ f₂ ≫ tensorHom g₁ g₂ = tensorHom (f₁ ≫ g₁) (f₂ ≫ g₂)

Tactic:
ext : 1

Goal state after:
R : Type u
inst✝ : CommSemiring R
X₁ Y₁ Z₁ : SemimoduleCat R
X₂ Y₂ Z₂ : SemimoduleCat R
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ Hom.hom (tensorHom f₁ f₂ ≫ tensorHom g₁ g₂) = Hom.hom (tensorHom (f₁ ≫ g₁) (f₂ ≫ g₂))
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
X₁ : SemimoduleCat R
X₂ : SemimoduleCat R
X₃ : SemimoduleCat R
Y₁ : SemimoduleCat R
Y₂ : SemimoduleCat R
Y₃ : SemimoduleCat R
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
⊢ tensorHom (tensorHom f₁ f₂) f₃ ≫ (associator Y₁ Y₂ Y₃).hom =
    (associator X₁ X₂ X₃).hom ≫ tensorHom f₁ (tensorHom f₂ f₃)

Tactic:
ext : 1

Goal state after:
R : Type u
inst✝ : CommSemiring R
X₁ : SemimoduleCat R
X₂ : SemimoduleCat R
X₃ : SemimoduleCat R
Y₁ : SemimoduleCat R
Y₂ : SemimoduleCat R
Y₃ : SemimoduleCat R
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
⊢ Hom.hom (tensorHom (tensorHom f₁ f₂) f₃ ≫ (associator Y₁ Y₂ Y₃).hom) =
    Hom.hom ((associator X₁ X₂ X₃).hom ≫ tensorHom f₁ (tensorHom f₂ f₃))
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
W : SemimoduleCat R
X : SemimoduleCat R
Y : SemimoduleCat R
Z : SemimoduleCat R
⊢ whiskerRight (associator W X Y).hom Z ≫ (associator W (tensorObj X Y) Z).hom ≫ whiskerLeft W (associator X Y Z).hom =
    (associator (tensorObj W X) Y Z).hom ≫ (associator W X (tensorObj Y Z)).hom

Tactic:
ext : 1

Goal state after:
R : Type u
inst✝ : CommSemiring R
W : SemimoduleCat R
X : SemimoduleCat R
Y : SemimoduleCat R
Z : SemimoduleCat R
⊢ Hom.hom
      (whiskerRight (associator W X Y).hom Z ≫
        (associator W (tensorObj X Y) Z).hom ≫ whiskerLeft W (associator X Y Z).hom) =
    Hom.hom ((associator (tensorObj W X) Y Z).hom ≫ (associator W X (tensorObj Y Z)).hom)
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
M N : SemimoduleCat R
f : M ⟶ N
⊢ tensorHom (𝟙 (of R R)) f ≫ (leftUnitor N).hom = (leftUnitor M).hom ≫ f

Tactic:
ext : 1

Goal state after:
R : Type u
inst✝ : CommSemiring R
M N : SemimoduleCat R
f : M ⟶ N
⊢ Hom.hom (tensorHom (𝟙 (of R R)) f ≫ (leftUnitor N).hom) = Hom.hom ((leftUnitor M).hom ≫ f)
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
M N : SemimoduleCat R
f : M ⟶ N
⊢ tensorHom f (𝟙 (of R R)) ≫ (rightUnitor N).hom = (rightUnitor M).hom ≫ f

Tactic:
ext : 1

Goal state after:
R : Type u
inst✝ : CommSemiring R
M N : SemimoduleCat R
f : M ⟶ N
⊢ Hom.hom (tensorHom f (𝟙 (of R R)) ≫ (rightUnitor N).hom) = Hom.hom ((rightUnitor M).hom ≫ f)
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
M N : SemimoduleCat R
⊢ (associator M (of R R) N).hom ≫ tensorHom (𝟙 M) (leftUnitor N).hom = tensorHom (rightUnitor M).hom (𝟙 N)

Tactic:
ext : 1

Goal state after:
R : Type u
inst✝ : CommSemiring R
M N : SemimoduleCat R
⊢ Hom.hom ((associator M (of R R) N).hom ≫ tensorHom (𝟙 M) (leftUnitor N).hom) =
    Hom.hom (tensorHom (rightUnitor M).hom (𝟙 N))
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
M₁ M₂ M₃ : SemimoduleCat R
f g : M₁ ⊗ M₂ ⟶ M₃
h : ∀ (m : ↑M₁) (n : ↑M₂), (Hom.hom f) (m ⊗ₜ[R] n) = (Hom.hom g) (m ⊗ₜ[R] n)
x✝¹ : ↑M₁
x✝ : ↑M₂
⊢ (((TensorProduct.mk R ↑M₁ ↑M₂).compr₂ₛₗ (Hom.hom f)) x✝¹) x✝ =
    (((TensorProduct.mk R ↑M₁ ↑M₂).compr₂ₛₗ (Hom.hom g)) x✝¹) x✝

Tactic:
apply h

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
M₁ M₂ M₃ : ModuleCat R
f g : M₁ ⊗ M₂ ⟶ M₃
h : ∀ (m : ↑M₁) (n : ↑M₂), (Hom.hom f) (m ⊗ₜ[R] n) = (Hom.hom g) (m ⊗ₜ[R] n)
x✝¹ : ↑M₁
x✝ : ↑M₂
⊢ (((TensorProduct.mk R ↑M₁ ↑M₂).compr₂ₛₗ (Hom.hom f)) x✝¹) x✝ =
    (((TensorProduct.mk R ↑M₁ ↑M₂).compr₂ₛₗ (Hom.hom g)) x✝¹) x✝

Tactic:
apply h

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic

Goal state before:
pp: case refine_1
R : Type u
inst✝ : CommRing R
X✝ Y✝ Z✝ : ModuleCat R
⊢ X✝ ◁ 0 = 0

Tactic:
ext : 1

Goal state after:
case refine_1
R : Type u
inst✝ : CommRing R
X✝ Y✝ Z✝ : ModuleCat R
⊢ Hom.hom (X✝ ◁ 0) = Hom.hom 0
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic

Goal state before:
pp: case refine_2
R : Type u
inst✝ : CommRing R
X✝ Y✝ Z✝ : ModuleCat R
⊢ 0 ▷ X✝ = 0

Tactic:
ext : 1

Goal state after:
case refine_2
R : Type u
inst✝ : CommRing R
X✝ Y✝ Z✝ : ModuleCat R
⊢ Hom.hom (0 ▷ X✝) = Hom.hom 0
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic

Goal state before:
pp: case refine_3
R : Type u
inst✝ : CommRing R
X✝ Y✝ Z✝ : ModuleCat R
f✝ g✝ : Y✝ ⟶ Z✝
⊢ X✝ ◁ (f✝ + g✝) = X✝ ◁ f✝ + X✝ ◁ g✝

Tactic:
ext : 1

Goal state after:
case refine_3
R : Type u
inst✝ : CommRing R
X✝ Y✝ Z✝ : ModuleCat R
f✝ g✝ : Y✝ ⟶ Z✝
⊢ Hom.hom (X✝ ◁ (f✝ + g✝)) = Hom.hom (X✝ ◁ f✝ + X✝ ◁ g✝)
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic

Goal state before:
pp: case refine_4
R : Type u
inst✝ : CommRing R
X✝ Y✝ Z✝ : ModuleCat R
f✝ g✝ : Y✝ ⟶ Z✝
⊢ (f✝ + g✝) ▷ X✝ = f✝ ▷ X✝ + g✝ ▷ X✝

Tactic:
ext : 1

Goal state after:
case refine_4
R : Type u
inst✝ : CommRing R
X✝ Y✝ Z✝ : ModuleCat R
f✝ g✝ : Y✝ ⟶ Z✝
⊢ Hom.hom ((f✝ + g✝) ▷ X✝) = Hom.hom (f✝ ▷ X✝ + g✝ ▷ X✝)
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic

Goal state before:
pp: case refine_1
R : Type u
inst✝ : CommRing R
X✝ Y✝ Z✝ : ModuleCat R
r✝ : R
f✝ : Y✝ ⟶ Z✝
⊢ X✝ ◁ (r✝ • f✝) = r✝ • X✝ ◁ f✝

Tactic:
ext : 1

Goal state after:
case refine_1
R : Type u
inst✝ : CommRing R
X✝ Y✝ Z✝ : ModuleCat R
r✝ : R
f✝ : Y✝ ⟶ Z✝
⊢ Hom.hom (X✝ ◁ (r✝ • f✝)) = Hom.hom (r✝ • X✝ ◁ f✝)
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic

Goal state before:
pp: case refine_2
R : Type u
inst✝ : CommRing R
r✝ : R
Y✝ Z✝ : ModuleCat R
f✝ : Y✝ ⟶ Z✝
X✝ : ModuleCat R
⊢ (r✝ • f✝) ▷ X✝ = r✝ • f✝ ▷ X✝

Tactic:
ext : 1

Goal state after:
case refine_2
R : Type u
inst✝ : CommRing R
r✝ : R
Y✝ Z✝ : ModuleCat R
f✝ : Y✝ ⟶ Z✝
X✝ : ModuleCat R
⊢ Hom.hom ((r✝ • f✝) ▷ X✝) = Hom.hom (r✝ • f✝ ▷ X✝)
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
X₁ X₂ Y₁ Y₂ : SemimoduleCat R
f : X₁ ⟶ Y₁
g : X₂ ⟶ Y₂
⊢ (f ⊗ₘ g) ≫ (Y₁.braiding Y₂).hom = (X₁.braiding X₂).hom ≫ (g ⊗ₘ f)

Tactic:
ext : 1

Goal state after:
R : Type u
inst✝ : CommSemiring R
X₁ X₂ Y₁ Y₂ : SemimoduleCat R
f : X₁ ⟶ Y₁
g : X₂ ⟶ Y₂
⊢ Hom.hom ((f ⊗ₘ g) ≫ (Y₁.braiding Y₂).hom) = Hom.hom ((X₁.braiding X₂).hom ≫ (g ⊗ₘ f))
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
X Y Z : SemimoduleCat R
⊢ (α_ X Y Z).hom ≫ (X.braiding (Y ⊗ Z)).hom ≫ (α_ Y Z X).hom =
    (X.braiding Y).hom ▷ Z ≫ (α_ Y X Z).hom ≫ Y ◁ (X.braiding Z).hom

Tactic:
ext : 1

Goal state after:
R : Type u
inst✝ : CommSemiring R
X Y Z : SemimoduleCat R
⊢ Hom.hom ((α_ X Y Z).hom ≫ (X.braiding (Y ⊗ Z)).hom ≫ (α_ Y Z X).hom) =
    Hom.hom ((X.braiding Y).hom ▷ Z ≫ (α_ Y X Z).hom ≫ Y ◁ (X.braiding Z).hom)
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
X Y Z : SemimoduleCat R
⊢ (α_ X Y Z).hom ≫ (α_ X Y Z).inv ≫ ((X ⊗ Y).braiding Z).hom ≫ (α_ Z X Y).inv =
    (α_ X Y Z).hom ≫ X ◁ (Y.braiding Z).hom ≫ (α_ X Z Y).inv ≫ (X.braiding Z).hom ▷ Y

Tactic:
ext : 1

Goal state after:
R : Type u
inst✝ : CommSemiring R
X Y Z : SemimoduleCat R
⊢ Hom.hom ((α_ X Y Z).hom ≫ (α_ X Y Z).inv ≫ ((X ⊗ Y).braiding Z).hom ≫ (α_ Z X Y).inv) =
    Hom.hom ((α_ X Y Z).hom ≫ X ◁ (Y.braiding Z).hom ≫ (α_ X Z Y).inv ≫ (X.braiding Z).hom ▷ Y)
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x✝¹ x✝ : SemimoduleCat R
⊢ (x✝¹.braiding x✝).hom ≫ (x✝.braiding x✝¹).hom = 𝟙 (x✝¹ ⊗ x✝)

Tactic:
ext : 1

Goal state after:
R : Type u
inst✝ : CommSemiring R
x✝¹ x✝ : SemimoduleCat R
⊢ Hom.hom ((x✝¹.braiding x✝).hom ≫ (x✝.braiding x✝¹).hom) = Hom.hom (𝟙 (x✝¹ ⊗ x✝))
Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f f' g g' h : C
η : g ⟶ h
θ : f' ⟶ g'
ηθ : g ⊗ f' ⟶ h ⊗ g'
η₁ : f ⊗ g ⊗ f' ⟶ f ⊗ h ⊗ g'
η₂ : f ⊗ g ⊗ f' ⟶ (f ⊗ h) ⊗ g'
η₃ : (f ⊗ g) ⊗ f' ⟶ (f ⊗ h) ⊗ g'
e_ηθ : η ⊗ₘ θ = ηθ
e_η₁ : f ◁ ηθ = η₁
e_η₂ : η₁ ≫ (α_ f h g').inv = η₂
e_η₃ : (α_ f g f').hom ≫ η₂ = η₃
⊢ f ◁ η ⊗ₘ θ = η₃

Tactic:
by
  simp only [← e_ηθ, ← e_η₁, ← e_η₂, ← e_η₃]
  simp [MonoidalCategory.tensorHom_def]

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Composition

Goal state before:
pp: case of_comp
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
X✝ Y✝ Z✝ : C
f✝ : X✝ ⟶ Y✝
x✝ y✝ z✝ : C
g' : x✝ ⟶ y✝
f : y✝ ⟶ z✝
hg' : W g'
hf : W.multiplicativeClosure' f
h_rec : ∀ (g : z✝ ⟶ Z✝), W.multiplicativeClosure' g → W.multiplicativeClosure' (f ≫ g)
g : z✝ ⟶ Z✝
hg : W.multiplicativeClosure' g
⊢ W.multiplicativeClosure' ((g' ≫ f) ≫ g)

Tactic:
| of_comp g' f hg' hf h_rec =>

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Concrete

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
f : Arrow (Type u)
x₁ x₂ :
  (fun X ↦ X)
    ({ obj := fun f ↦ ↑(Set.range ⇑(TypeCat.Hom.hom f.hom)),
          map := fun {X Y} φ ↦ ↾fun y ↦ ⟨(hom (Arrow.Hom.right φ)) ↑y, ⋯⟩,
          map_id := functorialSurjectiveInjectiveFactorizationData._proof_2,
          map_comp := @functorialSurjectiveInjectiveFactorizationData._proof_3 }.obj
      f)
h :
  (hom ({ app := fun x ↦ ↾fun y ↦ ↑y, naturality := functorialSurjectiveInjectiveFactorizationData._proof_5 }.app f))
      x₁ =
    (hom ({ app := fun x ↦ ↾fun y ↦ ↑y, naturality := functorialSurjectiveInjectiveFactorizationData._proof_5 }.app f))
      x₂
⊢ ↑x₁ = ↑x₂

Tactic:
exact h

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

Goal state before:
pp: R✝ : Type w
inst✝⁴ : Ring R✝
J : Type u
inst✝³ : Category.{v, u} J
F : J ⥤ ModuleCat R✝
R : Type w
inst✝² : CommRing R
M ι : Type u
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Cocone (Discrete.functor fun x ↦ of R M)
f : (finsuppCocone R M ι).pt ⟶ s.pt
h : ∀ (j : Discrete ι), (finsuppCocone R M ι).ι.app j ≫ f = s.ι.app j
⊢ f = ↟((Finsupp.lsum R) fun i ↦ Hom.hom (s.ι.app { as := i }))

Tactic:
ext : 1

Goal state after:
R✝ : Type w
inst✝⁴ : Ring R✝
J : Type u
inst✝³ : Category.{v, u} J
F : J ⥤ ModuleCat R✝
R : Type w
inst✝² : CommRing R
M ι : Type u
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Cocone (Discrete.functor fun x ↦ of R M)
f : (finsuppCocone R M ι).pt ⟶ s.pt
h : ∀ (j : Discrete ι), (finsuppCocone R M ι).ι.app j ≫ f = s.ι.app j
⊢ Hom.hom f = Hom.hom (↟((Finsupp.lsum R) fun i ↦ Hom.hom (s.ι.app { as := i })))
Module: Mathlib.CategoryTheory.Adjunction.Mates

Goal state before:
pp: C : Type u₁
D : Type u₂
E : Type u₃
F : Type u₄
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
β : TwoSquare R₁ H G R₂
X✝ : D
⊢ G.map (adj₁.unit.app (R₁.obj X✝)) ≫ β.natTrans.app (L₁.obj (R₁.obj X✝)) ≫ (H ⋙ R₂).map (adj₁.counit.app X✝) =
    β.natTrans.app X✝

Tactic:
← β.natTrans.naturality,

Goal state after:
C : Type u₁
D : Type u₂
E : Type u₃
F : Type u₄
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
β : TwoSquare R₁ H G R₂
X✝ : D
⊢ G.map (adj₁.unit.app (R₁.obj X✝)) ≫ (R₁ ⋙ G).map (adj₁.counit.app X✝) ≫ β.natTrans.app X✝ = β.natTrans.app X✝
Module: Mathlib.Algebra.Category.AlgCat.TensorAlgebra

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x✝² x✝¹ : AlgCat R
x✝ : x✝² ⟶ x✝¹
⊢ (forget₂ (AlgCat R) (ModuleCat R) ⋙ tensorAlgebra R).map x✝ ≫ ofHom ((TensorAlgebra.lift R) LinearMap.id) =
    ofHom ((TensorAlgebra.lift R) LinearMap.id) ≫ (𝟭 (AlgCat R)).map x✝

Tactic:
ext : 1

Goal state after:
R : Type u
inst✝ : CommRing R
x✝² x✝¹ : AlgCat R
x✝ : x✝² ⟶ x✝¹
⊢ Hom.hom ((forget₂ (AlgCat R) (ModuleCat R) ⋙ tensorAlgebra R).map x✝ ≫ ofHom ((TensorAlgebra.lift R) LinearMap.id)) =
    Hom.hom (ofHom ((TensorAlgebra.lift R) LinearMap.id) ≫ (𝟭 (AlgCat R)).map x✝)
Module: Mathlib.Algebra.Category.AlgCat.TensorAlgebra

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x✝ : ModuleCat R
⊢ (tensorAlgebra R).map ({ app := fun M ↦ ModuleCat.ofHom (TensorAlgebra.ι R), naturality := ⋯ }.app x✝) ≫
      { app := fun A ↦ ofHom ((TensorAlgebra.lift R) LinearMap.id), naturality := ⋯ }.app ((tensorAlgebra R).obj x✝) =
    𝟙 ((tensorAlgebra R).obj x✝)

Tactic:
ext : 1

Goal state after:
R : Type u
inst✝ : CommRing R
x✝ : ModuleCat R
⊢ Hom.hom
      ((tensorAlgebra R).map ({ app := fun M ↦ ModuleCat.ofHom (TensorAlgebra.ι R), naturality := ⋯ }.app x✝) ≫
        { app := fun A ↦ ofHom ((TensorAlgebra.lift R) LinearMap.id), naturality := ⋯ }.app
          ((tensorAlgebra R).obj x✝)) =
    Hom.hom (𝟙 ((tensorAlgebra R).obj x✝))
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : AddCommGroup M
inst✝³ : Semiring R
inst✝² : Module Rᵐᵒᵖ M
inst✝¹ : Module R M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
m : M
⊢ IsUnit (inr m) ↔ Subsingleton R

Tactic:
simp_rw [isUnit_iff_isUnit_fst, fst_inr, isUnit_zero_iff, subsingleton_iff_zero_eq_one]

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
r : R
⊢ -(r⁻¹ •> (inl r).snd <• r⁻¹) = (inl r⁻¹).snd

Tactic:
snd_inl,

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
r : R
⊢ -(r⁻¹ •> 0 <• r⁻¹) = (inl r⁻¹).snd
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
r : R
⊢ -(r⁻¹ •> 0 <• r⁻¹) = (inl r⁻¹).snd

Tactic:
snd_inl,

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
r : R
⊢ -(r⁻¹ •> 0 <• r⁻¹) = 0
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u
A : Type v
B : Type w
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
⊢ comul ∘ₗ LinearMap.fst R A B = TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul

Tactic:
ext : 1

Goal state after:
case hl
R : Type u
A : Type v
B : Type w
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
⊢ (comul ∘ₗ LinearMap.fst R A B) ∘ₗ inl R A B =
    (TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul) ∘ₗ inl R A B

case hr
R : Type u
A : Type v
B : Type w
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
⊢ (comul ∘ₗ LinearMap.fst R A B) ∘ₗ inr R A B =
    (TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul) ∘ₗ inr R A B
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u
A : Type v
B : Type w
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
⊢ comul ∘ₗ LinearMap.snd R A B = TensorProduct.map (LinearMap.snd R A B) (LinearMap.snd R A B) ∘ₗ comul

Tactic:
ext : 1

Goal state after:
case hl
R : Type u
A : Type v
B : Type w
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
⊢ (comul ∘ₗ LinearMap.snd R A B) ∘ₗ inl R A B =
    (TensorProduct.map (LinearMap.snd R A B) (LinearMap.snd R A B) ∘ₗ comul) ∘ₗ inl R A B

case hr
R : Type u
A : Type v
B : Type w
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
⊢ (comul ∘ₗ LinearMap.snd R A B) ∘ₗ inr R A B =
    (TensorProduct.map (LinearMap.snd R A B) (LinearMap.snd R A B) ∘ₗ comul) ∘ₗ inr R A B
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: S : Type u_1
R R' : Type u
M : Type v
inst✝¹³ : CommSemiring S
inst✝¹² : Semiring R
inst✝¹¹ : CommSemiring R'
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Algebra S R
inst✝⁸ : Module S M
inst✝⁷ : Module R M
inst✝⁶ : Module Rᵐᵒᵖ M
inst✝⁵ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁴ : IsScalarTower S R M
inst✝³ : IsScalarTower S Rᵐᵒᵖ M
inst✝² : Module R' M
inst✝¹ : Module R'ᵐᵒᵖ M
inst✝ : IsCentralScalar R' M
s : S
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ s •> x.snd = (algebraMap S R) s •> x.snd + 0 <• x.fst

Tactic:
rw [smul_zero, add_zero, algebraMap_smul]

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

Goal state before:
pp: R : Type u
A : Type v
B : Type w
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
⊢ rTensor (A × B) counit ∘ₗ comul = (TensorProduct.mk R R (A × B)) 1

Tactic:
ext : 1

Goal state after:
case hl
R : Type u
A : Type v
B : Type w
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
⊢ (rTensor (A × B) counit ∘ₗ comul) ∘ₗ inl R A B = (TensorProduct.mk R R (A × B)) 1 ∘ₗ inl R A B

case hr
R : Type u
A : Type v
B : Type w
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
⊢ (rTensor (A × B) counit ∘ₗ comul) ∘ₗ inr R A B = (TensorProduct.mk R R (A × B)) 1 ∘ₗ inr R A B
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u
A : Type v
B : Type w
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
⊢ lTensor (A × B) counit ∘ₗ comul = (TensorProduct.mk R (A × B) R).flip 1

Tactic:
ext : 1

Goal state after:
case hl
R : Type u
A : Type v
B : Type w
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
⊢ (lTensor (A × B) counit ∘ₗ comul) ∘ₗ inl R A B = (TensorProduct.mk R (A × B) R).flip 1 ∘ₗ inl R A B

case hr
R : Type u
A : Type v
B : Type w
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
⊢ (lTensor (A × B) counit ∘ₗ comul) ∘ₗ inr R A B = (TensorProduct.mk R (A × B) R).flip 1 ∘ₗ inr R A B
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u
ι : Type v
A : ι → Type w
inst✝⁴ : DecidableEq ι
inst✝³ : CommSemiring R
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : (i : ι) → Module R (A i)
inst✝ : (i : ι) → Coalgebra R (A i)
⊢ rTensor (Π₀ (i : ι), A i) counit ∘ₗ comul = (TensorProduct.mk R R (Π₀ (i : ι), A i)) 1

Tactic:
ext : 1

Goal state after:
R : Type u
ι : Type v
A : ι → Type w
inst✝⁴ : DecidableEq ι
inst✝³ : CommSemiring R
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : (i : ι) → Module R (A i)
inst✝ : (i : ι) → Coalgebra R (A i)
i✝ : ι
⊢ (rTensor (Π₀ (i : ι), A i) counit ∘ₗ comul) ∘ₗ lsingle i✝ = (TensorProduct.mk R R (Π₀ (i : ι), A i)) 1 ∘ₗ lsingle i✝