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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y Z : C
f : Y ≅ Z
⊢ X ◁ 𝟙 Y = 𝟙 (X ⊗ Y)

Tactic:
whiskerLeft_id

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y Z : C
f : Y ≅ Z
⊢ 𝟙 (X ⊗ Y) = 𝟙 (X ⊗ Y)
Module: Mathlib.CategoryTheory.Monoidal.Category

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y Z : C
f : Y ≅ Z
⊢ X ◁ 𝟙 Z = 𝟙 (X ⊗ Z)

Tactic:
whiskerLeft_id

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y Z : C
f : Y ≅ Z
⊢ 𝟙 (X ⊗ Z) = 𝟙 (X ⊗ Z)
Module: Mathlib.CategoryTheory.Monoidal.Category

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
X Y Z : C
f : Y ⟶ Z
inst✝ : IsIso f
⊢ X ◁ 𝟙 Y = 𝟙 (X ⊗ Y)

Tactic:
whiskerLeft_id

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
X Y Z : C
f : Y ⟶ Z
inst✝ : IsIso f
⊢ 𝟙 (X ⊗ Y) = 𝟙 (X ⊗ Y)
Module: Mathlib.CategoryTheory.Monoidal.Category

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
X Y Z : C
f : Y ⟶ Z
inst✝ : IsIso f
⊢ X ◁ 𝟙 Z = 𝟙 (X ⊗ Z)

Tactic:
whiskerLeft_id

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
X Y Z : C
f : Y ⟶ Z
inst✝ : IsIso f
⊢ 𝟙 (X ⊗ Z) = 𝟙 (X ⊗ Z)
Module: Mathlib.CategoryTheory.Monoidal.NaturalTransformation

Goal state before:
pp: C : Type u₁
inst✝¹⁴ : Category.{v₁, u₁} C
inst✝¹³ : MonoidalCategory C
D : Type u₂
inst✝¹² : Category.{v₂, u₂} D
inst✝¹¹ : MonoidalCategory D
E : Type u₃
inst✝¹⁰ : Category.{v₃, u₃} E
inst✝⁹ : MonoidalCategory E
E' : Type u₄
inst✝⁸ : Category.{v₄, u₄} E'
inst✝⁷ : MonoidalCategory E'
F₁ F₂ F₃ : C ⥤ D
τ : F₁ ⟶ F₂
inst✝⁶ : F₁.LaxMonoidal
inst✝⁵ : F₂.LaxMonoidal
inst✝⁴ : F₃.LaxMonoidal
G₁ G₂ : D ⥤ E
inst✝³ : G₁.LaxMonoidal
inst✝² : G₂.LaxMonoidal
τ' : G₁ ⟶ G₂
inst✝¹ : IsMonoidal τ
inst✝ : IsMonoidal τ'
⊢ ε (F₁ ⋙ G₁) ≫ (τ ◫ τ').app (𝟙_ C) = ε (F₂ ⋙ G₂)

Tactic:
simp only [comp_obj, comp_ε, hcomp_app, assoc, naturality_assoc, unit_assoc, ← map_comp, unit]

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

Goal state before:
pp: C : Type u₁
inst✝¹³ : Category.{v₁, u₁} C
inst✝¹² : MonoidalCategory C
D : Type u₂
inst✝¹¹ : Category.{v₂, u₂} D
inst✝¹⁰ : MonoidalCategory D
E : Type u₃
inst✝⁹ : Category.{v₃, u₃} E
inst✝⁸ : MonoidalCategory E
E' : Type u₄
inst✝⁷ : Category.{v₄, u₄} E'
inst✝⁶ : MonoidalCategory E'
F₁ F₂ F₃ : C ⥤ D
τ : F₁ ⟶ F₂
inst✝⁵ : F₁.LaxMonoidal
inst✝⁴ : F₂.LaxMonoidal
inst✝³ : F₃.LaxMonoidal
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : F.Monoidal
inst✝¹ : G.LaxMonoidal
inst✝ : adj.IsMonoidal
X Y : D
⊢ μ (G ⋙ F) X Y ≫ adj.counit.app (X ⊗ Y) = (adj.counit.app X ⊗ₘ adj.counit.app Y) ≫ μ (𝟭 D) X Y

Tactic:
dsimp
    rw [assoc, map_μ_comp_counit_app_tensor, μ_δ_assoc, comp_id]

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : C ⥤ D
inst✝ : F.Monoidal
⊢ CategoryTheory.inv (η F) ≫ η F = 𝟙 (𝟙_ D)

Tactic:
IsIso.inv_hom_id

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : C ⥤ D
inst✝ : F.Monoidal
⊢ 𝟙 (𝟙_ D) = 𝟙 (𝟙_ D)
Module: Mathlib.CategoryTheory.Limits.Opposites

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
F : Jᵒᵖ ⥤ C
c : Cone F
hc : IsLimit c
s : Cocone F.rightOp
m : (coconeRightOpOfCone c).pt ⟶ s.pt
w : ∀ (j : J), (coconeRightOpOfCone c).ι.app j ≫ m = s.ι.app j
j : Jᵒᵖ
⊢ (m.unop ≫ c.π.app j).op = ((hc.lift (coneOfCoconeRightOp s)).op.unop ≫ c.π.app j).op

Tactic:
simpa only [Quiver.Hom.unop_op, IsLimit.fac] using! w (unop j)

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

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : F.OplaxMonoidal
X Y Z : D
⊢ (adj.homEquiv ((G.obj X ⊗ G.obj Y) ⊗ G.obj Z) (X ⊗ Y ⊗ Z)).symm
      ((adj.homEquiv (G.obj X ⊗ G.obj Y) (X ⊗ Y)) (δ F (G.obj X) (G.obj Y) ≫ (adj.counit.app X ⊗ₘ adj.counit.app Y)) ▷
          G.obj Z ≫
        (adj.homEquiv (G.obj (X ⊗ Y) ⊗ G.obj Z) ((X ⊗ Y) ⊗ Z))
            (δ F (G.obj (X ⊗ Y)) (G.obj Z) ≫ (adj.counit.app (X ⊗ Y) ⊗ₘ adj.counit.app Z)) ≫
          G.map (α_ X Y Z).hom) =
    (adj.homEquiv ((G.obj X ⊗ G.obj Y) ⊗ G.obj Z) (X ⊗ Y ⊗ Z)).symm
      ((α_ (G.obj X) (G.obj Y) (G.obj Z)).hom ≫
        G.obj X ◁
            (adj.homEquiv (G.obj Y ⊗ G.obj Z) (Y ⊗ Z))
              (δ F (G.obj Y) (G.obj Z) ≫ (adj.counit.app Y ⊗ₘ adj.counit.app Z)) ≫
          (adj.homEquiv (G.obj X ⊗ G.obj (Y ⊗ Z)) (X ⊗ Y ⊗ Z))
            (δ F (G.obj X) (G.obj (Y ⊗ Z)) ≫ (adj.counit.app X ⊗ₘ adj.counit.app (Y ⊗ Z))))

Tactic:
by
    simp only [homEquiv_unit, comp_obj, map_comp, comp_whiskerRight, assoc, homEquiv_counit,
      counit_naturality, counit_naturality_assoc, left_triangle_components_assoc,
      MonoidalCategory.whiskerLeft_comp]
    rw [← δ_natural_left_assoc, ← δ_natural_left_assoc, ← δ_natural_left_assoc]
    have := @NatTrans.whiskerRight_app_tensor_app_assoc _ _ _ _ _ _ _ _ _ adj.counit adj.counit
    dsimp only [id_obj, comp_obj, Functor.comp_map, Functor.id_map] at this
    rw [this, this, tensorHom_def, assoc, ← comp_whiskerRight_assoc,
      left_triangle_components, id_whiskerRight, id_comp,
      whisker_exchange_assoc, whisker_exchange_assoc, ← tensorHom_def_assoc,
      associator_naturality, OplaxMonoidal.associativity_assoc]
    rw [← δ_natural_right_assoc, ← δ_natural_right_assoc, ← δ_natural_right_assoc]
    nth_rw 4 [tensorHom_def]
    rw [← whisker_exchange, ← MonoidalCategory.whiskerLeft_comp_assoc,
      ← MonoidalCategory.whiskerLeft_comp_assoc,
      ← MonoidalCategory.whiskerLeft_comp_assoc, assoc, assoc,
      counit_naturality, counit_naturality_assoc, left_triangle_components_assoc,
      MonoidalCategory.whiskerLeft_comp, assoc, tensorHom_def, whisker_exchange]

Goal state after:
Module: Mathlib.CategoryTheory.ConcreteCategory.EpiMono

Goal state before:
pp: case mp
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
h : MorphismProperty.injective C = monomorphisms C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : monomorphisms C f
⊢ Mono ((forget C).map f)

Tactic:
rw [mono_iff_injective]

Goal state after:
case mp
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
h : MorphismProperty.injective C = monomorphisms C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : monomorphisms C f
⊢ Function.Injective ⇑(hom ((forget C).map f))
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ HasColimit (cospan f g).op ↔ HasPullback f g

Tactic:
hasColimit_op_iff_hasLimit

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ HasLimit (cospan f g) ↔ HasPullback f g
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F G : C ⥤ D
inst✝ : F.Monoidal
i : F ≅ G
X Y Z : C
⊢ ((((((i.inv.app X ⊗ₘ i.inv.app Y) ▷ G.obj Z ≫ LaxMonoidal.μ F X Y ▷ G.obj Z) ≫ i.hom.app (X ⊗ Y) ▷ G.obj Z) ≫
            (i.inv.app (X ⊗ Y) ⊗ₘ i.inv.app Z)) ≫
          LaxMonoidal.μ F (X ⊗ Y) Z) ≫
        F.map (α_ X Y Z).hom) ≫
      i.hom.app (X ⊗ Y ⊗ Z) =
    ((((((α_ (G.obj X) (G.obj Y) (G.obj Z)).hom ≫ G.obj X ◁ (i.inv.app Y ⊗ₘ i.inv.app Z)) ≫
              G.obj X ◁ LaxMonoidal.μ F Y Z) ≫
            G.obj X ◁ i.hom.app (Y ⊗ Z)) ≫
          (i.inv.app X ⊗ₘ i.inv.app (Y ⊗ Z))) ≫
        LaxMonoidal.μ F X (Y ⊗ Z)) ≫
      i.hom.app (X ⊗ Y ⊗ Z)

Tactic:
congr 1

Goal state after:
case e_a
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F G : C ⥤ D
inst✝ : F.Monoidal
i : F ≅ G
X Y Z : C
⊢ (((((i.inv.app X ⊗ₘ i.inv.app Y) ▷ G.obj Z ≫ LaxMonoidal.μ F X Y ▷ G.obj Z) ≫ i.hom.app (X ⊗ Y) ▷ G.obj Z) ≫
          (i.inv.app (X ⊗ Y) ⊗ₘ i.inv.app Z)) ≫
        LaxMonoidal.μ F (X ⊗ Y) Z) ≫
      F.map (α_ X Y Z).hom =
    (((((α_ (G.obj X) (G.obj Y) (G.obj Z)).hom ≫ G.obj X ◁ (i.inv.app Y ⊗ₘ i.inv.app Z)) ≫
            G.obj X ◁ LaxMonoidal.μ F Y Z) ≫
          G.obj X ◁ i.hom.app (Y ⊗ Z)) ≫
        (i.inv.app X ⊗ₘ i.inv.app (Y ⊗ Z))) ≫
      LaxMonoidal.μ F X (Y ⊗ Z)
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
this : Equivalence (Relation.Map ⇑c.toSetoid ⇑f ⇑f)
⊢ ⇑(mapGen ⇑f) ≤ Relation.Map ⇑c ⇑f ⇑f

Tactic:
intro _ _ hg

Goal state after:
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
this : Equivalence (Relation.Map ⇑c.toSetoid ⇑f ⇑f)
i✝¹ i✝ : N
hg : (mapGen ⇑f) i✝¹ i✝
⊢ Relation.Map (⇑c) (⇑f) (⇑f) i✝¹ i✝
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✝ d✝ c : RingCon M
d : ↑(Set.Ici c)
⊢ (fun d ↦ ⟨d.comap c.mk', ⋯⟩) ((fun d ↦ mapGen ⇑c.mk') d) = d

Tactic:
ext
    simp only [comap_rel]
    rw [mapGen_apply_apply_of_surjective c.mk' (c.ker_mk'_eq.trans_le d.2) c.mk'_surjective]

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
r : R
x : M
⊢ ↑(FreeAlgebra.ι R (r • x)) = (RingHom.id R) r • ↑(FreeAlgebra.ι R x)

Tactic:
rw [← RingCon.coe_smul]

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
x : M
⊢ ↑(FreeAlgebra.ι R (r • x)) = ↑((RingHom.id R) r • FreeAlgebra.ι R x)
Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic

Goal state before:
pp: case add
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : TensorAlgebra R M
hx : x ∈ Algebra.adjoin R (Set.range ⇑(ι R))
hy : y ∈ Algebra.adjoin R (Set.range ⇑(ι R))
⊢ x + y ∈ Algebra.adjoin R (Set.range ⇑(ι R))

Tactic:
| add x y hx hy =>

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

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : MonoidWithZero R
inst✝² : AddMonoid M
inst✝¹ : DistribMulAction R M
inst✝ : DistribMulAction Rᵐᵒᵖ M
r : R
m : M
⊢ r •> m + 0 = r •> m

Tactic:
add_zero

Goal state after:
R : Type u
M : Type v
inst✝³ : MonoidWithZero R
inst✝² : AddMonoid M
inst✝¹ : DistribMulAction R M
inst✝ : DistribMulAction Rᵐᵒᵖ M
r : R
m : M
⊢ r •> m = r •> m
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
r : R
x : tsze R M
⊢ r •> x.snd + 0 = r •> x.snd

Tactic:
add_zero

Goal state after:
R : Type u
M : Type v
inst✝³ : Monoid R
inst✝² : AddMonoid M
inst✝¹ : DistribMulAction R M
inst✝ : DistribMulAction Rᵐᵒᵖ M
r : R
x : tsze R M
⊢ r •> x.snd = r •> x.snd
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
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ x.2 + 0 = x.2

Tactic:
add_zero

Goal state after:
R : Type u
M : Type v
inst✝³ : Monoid R
inst✝² : AddMonoid M
inst✝¹ : DistribMulAction R M
inst✝ : DistribMulAction Rᵐᵒᵖ M
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ x.2 = x.2
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
A : Type u_2
inst✝² : Semiring A
inst✝¹ : Algebra S A
inst✝ : Algebra R' A
f : R →ₐ[S] A
g : M →ₗ[S] A
hg : ∀ (x y : M), g x * g y = 0
hfg : ∀ (r : R) (x : M), g (r •> x) = f r * g x
hgf : ∀ (r : R) (x : M), g (x <• r) = g x * f r
⊢ 1 + 0 = 1

Tactic:
add_zero

Goal state after:
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
A : Type u_2
inst✝² : Semiring A
inst✝¹ : Algebra S A
inst✝ : Algebra R' A
f : R →ₐ[S] A
g : M →ₗ[S] A
hg : ∀ (x y : M), g x * g y = 0
hfg : ∀ (r : R) (x : M), g (r •> x) = f r * g x
hgf : ∀ (r : R) (x : M), g (x <• r) = g x * f r
⊢ 1 = 1
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: S : Type u_1
R : Type u
M : Type v
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Semiring 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
A : Type u_2
inst✝¹ : Semiring A
inst✝ : Algebra S A
f : R →ₐ[S] A
g : M →ₗ[S] A
hg : ∀ (x y : M), g x * g y = 0
hfg : ∀ (r : R) (x : M), g (r •> x) = f r * g x
hgf : ∀ (r : R) (x : M), g (x <• r) = g x * f r
r : R
⊢ f r + 0 = f r

Tactic:
add_zero

Goal state after:
S : Type u_1
R : Type u
M : Type v
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Semiring 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
A : Type u_2
inst✝¹ : Semiring A
inst✝ : Algebra S A
f : R →ₐ[S] A
g : M →ₗ[S] A
hg : ∀ (x y : M), g x * g y = 0
hfg : ∀ (r : R) (x : M), g (r •> x) = f r * g x
hgf : ∀ (r : R) (x : M), g (x <• r) = g x * f r
r : R
⊢ f r = f r
Module: Mathlib.RingTheory.Coalgebra.Equiv

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : Module R A
inst✝³ : Coalgebra R A
inst✝² : AddCommMonoid B
inst✝¹ : Module R B
inst✝ : CoalgebraStruct R B
f : A ≃ₗc[R] B
⊢ (((↑(TensorProduct.assoc R B B B) ∘ₗ
            LinearMap.rTensor B ((TensorProduct.map f.toLinearMap f.toLinearMap ∘ₗ comul) ∘ₗ ↑f.toLinearEquiv.symm)) ∘ₗ
          TensorProduct.map f.toLinearMap f.toLinearMap) ∘ₗ
        comul) ∘ₗ
      ↑f.toLinearEquiv.symm =
    ((LinearMap.lTensor B ((TensorProduct.map f.toLinearMap f.toLinearMap ∘ₗ comul) ∘ₗ ↑f.toLinearEquiv.symm) ∘ₗ
          TensorProduct.map f.toLinearMap f.toLinearMap) ∘ₗ
        comul) ∘ₗ
      ↑f.toLinearEquiv.symm

Tactic:
congr 1

Goal state after:
case e_f
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : Module R A
inst✝³ : Coalgebra R A
inst✝² : AddCommMonoid B
inst✝¹ : Module R B
inst✝ : CoalgebraStruct R B
f : A ≃ₗc[R] B
⊢ ((↑(TensorProduct.assoc R B B B) ∘ₗ
          LinearMap.rTensor B ((TensorProduct.map f.toLinearMap f.toLinearMap ∘ₗ comul) ∘ₗ ↑f.toLinearEquiv.symm)) ∘ₗ
        TensorProduct.map f.toLinearMap f.toLinearMap) ∘ₗ
      comul =
    (LinearMap.lTensor B ((TensorProduct.map f.toLinearMap f.toLinearMap ∘ₗ comul) ∘ₗ ↑f.toLinearEquiv.symm) ∘ₗ
        TensorProduct.map f.toLinearMap f.toLinearMap) ∘ₗ
      comul
Module: Mathlib.RingTheory.Bialgebra.Basic

Goal state before:
pp: R✝ : Type u
A✝ : Type v
inst✝⁵ : CommSemiring R✝
inst✝⁴ : Semiring A✝
inst✝³ : Bialgebra R✝ A✝
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
C : Coalgebra R A
counit_one : counit 1 = 1
counit_mul : ∀ {a b : A}, counit (a * b) = counit a * counit b
comul_one : comul 1 = 1
comul_mul : ∀ {a b : A}, comul (a * b) = comul a * comul b
⊢ (LinearMap.mul R A).compr₂ comul = (LinearMap.mul R (A ⊗[R] A)).compl₁₂ comul comul

Tactic:
ext; exact comul_mul

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
A : n → Type u_3
inst✝² : (i : n) → AddCommMonoid (A i)
inst✝¹ : (i : n) → Module R (A i)
inst✝ : (i : n) → CoalgebraStruct R (A i)
i : n
⊢ comul ∘ₗ proj i = map (proj i) (proj i) ∘ₗ comul

Tactic:
ext j; have := eq_or_ne i j
  aesop (add simp [map_map, proj_comp_single, diag])

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
A : n → Type u_3
inst✝² : (i : n) → AddCommMonoid (A i)
inst✝¹ : (i : n) → Module R (A i)
inst✝ : (i : n) → Coalgebra R (A i)
⊢ ↑(TensorProduct.assoc R ((i : n) → A i) ((i : n) → A i) ((i : n) → A i)) ∘ₗ rTensor ((i : n) → A i) comul ∘ₗ comul =
    lTensor ((i : n) → A i) comul ∘ₗ comul

Tactic:
ext : 1
    simp_rw [comp_assoc, comul_comp_single, ← comp_assoc, lTensor_comp_map, comul_comp_single,
      comp_assoc, ← comp_assoc comul, rTensor_comp_map, comul_comp_single, ← map_comp_rTensor,
      ← map_comp_lTensor, comp_assoc, ← coassoc, ← comp_assoc comul, ← comp_assoc,
      map_map_comp_assoc_eq]

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✝
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:
congr 1

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✝
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:
congr 1

Goal state after:
Module: Mathlib.Algebra.Ring.BooleanRing

Goal state before:
pp: α : Type u_1
inst✝ : BooleanRing α
a : α
⊢ -a = -a + 0

Tactic:
add_zero

Goal state after:
α : Type u_1
inst✝ : BooleanRing α
a : α
⊢ -a = -a
Module: Mathlib.Algebra.Ring.BooleanRing

Goal state before:
pp: α : Type u_1
inst✝ : BooleanRing α
a b : α
⊢ a * b + b * a = 0

Tactic:
have : a + b = a + b + (a * b + b * a) :=
    calc
      a + b = (a + b) * (a + b) := by rw [mul_self]
      _ = a * a + a * b + (b * a + b * b) := by rw [add_mul, mul_add, mul_add]
      _ = a + a * b + (b * a + b) := by simp only [mul_self]
      _ = a + b + (a * b + b * a) := by abel
  rwa [left_eq_add] at this

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
F F' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
⊢ adj1.unit ≫ whiskerRight (adj1.leftAdjointUniq adj2).hom G = adj2.unit

Tactic:
ext x
  rw [NatTrans.comp_app, ← homEquiv_leftAdjointUniq_hom_app adj1 adj2]
  simp

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
F F' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
x : C
⊢ adj1.unit.app x ≫ G.map ((adj1.leftAdjointUniq adj2).hom.app x) = adj2.unit.app x

Tactic:
rw [← unit_leftAdjointUniq_hom adj1 adj2]; rfl

Goal state after:
Module: Mathlib.Algebra.Ring.BooleanRing

Goal state before:
pp: α : Type u_1
inst✝ : BooleanRing α
a b : α
⊢ a + 0 = a

Tactic:
add_zero

Goal state after:
α : Type u_1
inst✝ : BooleanRing α
a b : α
⊢ a = a
Module: Mathlib.Algebra.Ring.BooleanRing

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : BooleanRing α
inst✝¹ : BooleanRing β
inst✝ : BooleanRing γ
a : α
⊢ 1 + 0 = 1

Tactic:
add_zero

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : BooleanRing α
inst✝¹ : BooleanRing β
inst✝ : BooleanRing γ
a : α
⊢ 1 = 1
Module: Mathlib.Algebra.Ring.BooleanRing

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : BooleanRing α
inst✝¹ : BooleanRing β
inst✝ : BooleanRing γ
a : α
⊢ a + 0 = a

Tactic:
add_zero

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : BooleanRing α
inst✝¹ : BooleanRing β
inst✝ : BooleanRing γ
a : α
⊢ a = a
Module: Mathlib.RingTheory.Bialgebra.TensorProduct

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
ι : Type u_4
κ : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Bialgebra R A
inst✝¹ : Semiring B
inst✝ : Bialgebra R B
a : A
b : B
⊢ counit ∘ₗ LinearMap.mul' R A = counit

Tactic:
ext; simp [mul_comm]

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
M N O : C
inst✝² : ComonObj M
inst✝¹ : ComonObj N
inst✝ : ComonObj O
A : Comon C
f : A ⟶ trivial C
⊢ f = { hom := ε, isComonHom_hom := ⋯ }

Tactic:
by
    ext
    rw [← Category.comp_id f.hom]
    dsimp only [trivial_X]
    rw [← trivial_comon_counit, IsComonHom.hom_counit]

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

Goal state before:
pp: R : Type u_1
M : Type u_3
N : Type u_4
M' : Type u_6
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
inst✝ : Coalgebra R M
f : M →ₗ[R] M'
g : N →ₗ[R] M
⊢ ((α ∘ₗ δ ⊗ₘ f) ∘ₗ δ) ∘ₗ g = ((LinearMap.id ⊗ₘ (LinearMap.id ⊗ₘ f) ∘ₗ LinearMap.id ⊗ₘ δ) ∘ₗ δ) ∘ₗ g

Tactic:
congr 1

Goal state after:
case e_f
R : Type u_1
M : Type u_3
N : Type u_4
M' : Type u_6
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
inst✝ : Coalgebra R M
f : M →ₗ[R] M'
g : N →ₗ[R] M
⊢ (α ∘ₗ δ ⊗ₘ f) ∘ₗ δ = (LinearMap.id ⊗ₘ (LinearMap.id ⊗ₘ f) ∘ₗ LinearMap.id ⊗ₘ δ) ∘ₗ δ