mathlib-initiative/mathlib-tactics huggingface dataset:
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ᵒᵖ
inst✝ : HasLimit F
j : J
⊢ colimit.ι F.unop j ≫ (colimitUnopIsoOpLimit F).hom = (limit.π F (op j)).unop

Tactic:
by
  simp [colimitUnopIsoOpLimit]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C ⥤ D
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : PreservesLimit (cospan f g) G
c : Cone (cospan g f)
hc : IsLimit c
⊢ IsLimit (G.mapCone c)

Tactic:
apply (IsLimit.postcomposeHomEquiv (diagramIsoCospan.{v₂} _) _).toFun

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C ⥤ D
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : PreservesLimit (cospan f g) G
c : Cone (cospan g f)
hc : IsLimit c
⊢ IsLimit ((Cone.postcompose (diagramIsoCospan (cospan g f ⋙ G)).hom).obj (G.mapCone c))
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
⊢ ∀ (j : WalkingSpan),
    ((Cocone.precompose (diagramIsoSpan (span f g ⋙ G)).symm.hom).obj (G.mapCocone (PushoutCocone.mk h k comm))).ι.app
          j ≫
        (Iso.refl
            ((Cocone.precompose (diagramIsoSpan (span f g ⋙ G)).symm.hom).obj
                (G.mapCocone (PushoutCocone.mk h k comm))).pt).hom =
      (PushoutCocone.mk (G.map h) (G.map k) ⋯).ι.app j

Tactic:
rintro (_ | _ | _)

Goal state after:
case none
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
⊢ ((Cocone.precompose (diagramIsoSpan (span f g ⋙ G)).symm.hom).obj (G.mapCocone (PushoutCocone.mk h k comm))).ι.app
        none ≫
      (Iso.refl
          ((Cocone.precompose (diagramIsoSpan (span f g ⋙ G)).symm.hom).obj
              (G.mapCocone (PushoutCocone.mk h k comm))).pt).hom =
    (PushoutCocone.mk (G.map h) (G.map k) ⋯).ι.app none

case some.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
⊢ ((Cocone.precompose (diagramIsoSpan (span f g ⋙ G)).symm.hom).obj (G.mapCocone (PushoutCocone.mk h k comm))).ι.app
        (some WalkingPair.left) ≫
      (Iso.refl
          ((Cocone.precompose (diagramIsoSpan (span f g ⋙ G)).symm.hom).obj
              (G.mapCocone (PushoutCocone.mk h k comm))).pt).hom =
    (PushoutCocone.mk (G.map h) (G.map k) ⋯).ι.app (some WalkingPair.left)

case some.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
⊢ ((Cocone.precompose (diagramIsoSpan (span f g ⋙ G)).symm.hom).obj (G.mapCocone (PushoutCocone.mk h k comm))).ι.app
        (some WalkingPair.right) ≫
      (Iso.refl
          ((Cocone.precompose (diagramIsoSpan (span f g ⋙ G)).symm.hom).obj
              (G.mapCocone (PushoutCocone.mk h k comm))).pt).hom =
    (PushoutCocone.mk (G.map h) (G.map k) ⋯).ι.app (some WalkingPair.right)
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
X✝ Y Z : C
f : X✝ ⟶ Y
g : X✝ ⟶ Z
inst✝² : HasPushout f g
inst✝¹ : HasPushout (G.map f) (G.map g)
inst✝ : PreservesColimit (span f g) G
c : PushoutCocone f g
X : C
⊢ ∀ (j : WalkingCospan),
    ((Cone.postcompose (isoWhiskerRight (cospanOp f g).symm (yoneda.obj X)).hom).obj
              (Cone.whisker walkingSpanOpEquiv.symm.functor ((yoneda.obj X).mapCone (Cocone.op c)))).π.app
        j =
      (Iso.refl
            ((Cone.postcompose (isoWhiskerRight (cospanOp f g).symm (yoneda.obj X)).hom).obj
                (Cone.whisker walkingSpanOpEquiv.symm.functor ((yoneda.obj X).mapCone (Cocone.op c)))).pt).hom ≫
        ((yoneda.obj X).mapCone c.op).π.app j

Tactic:
rintro (_ | _ | _)

Goal state after:
case none
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
X✝ Y Z : C
f : X✝ ⟶ Y
g : X✝ ⟶ Z
inst✝² : HasPushout f g
inst✝¹ : HasPushout (G.map f) (G.map g)
inst✝ : PreservesColimit (span f g) G
c : PushoutCocone f g
X : C
⊢ ((Cone.postcompose (isoWhiskerRight (cospanOp f g).symm (yoneda.obj X)).hom).obj
            (Cone.whisker walkingSpanOpEquiv.symm.functor ((yoneda.obj X).mapCone (Cocone.op c)))).π.app
      none =
    (Iso.refl
          ((Cone.postcompose (isoWhiskerRight (cospanOp f g).symm (yoneda.obj X)).hom).obj
              (Cone.whisker walkingSpanOpEquiv.symm.functor ((yoneda.obj X).mapCone (Cocone.op c)))).pt).hom ≫
      ((yoneda.obj X).mapCone c.op).π.app none

case some.left
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
X✝ Y Z : C
f : X✝ ⟶ Y
g : X✝ ⟶ Z
inst✝² : HasPushout f g
inst✝¹ : HasPushout (G.map f) (G.map g)
inst✝ : PreservesColimit (span f g) G
c : PushoutCocone f g
X : C
⊢ ((Cone.postcompose (isoWhiskerRight (cospanOp f g).symm (yoneda.obj X)).hom).obj
            (Cone.whisker walkingSpanOpEquiv.symm.functor ((yoneda.obj X).mapCone (Cocone.op c)))).π.app
      (some WalkingPair.left) =
    (Iso.refl
          ((Cone.postcompose (isoWhiskerRight (cospanOp f g).symm (yoneda.obj X)).hom).obj
              (Cone.whisker walkingSpanOpEquiv.symm.functor ((yoneda.obj X).mapCone (Cocone.op c)))).pt).hom ≫
      ((yoneda.obj X).mapCone c.op).π.app (some WalkingPair.left)

case some.right
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
X✝ Y Z : C
f : X✝ ⟶ Y
g : X✝ ⟶ Z
inst✝² : HasPushout f g
inst✝¹ : HasPushout (G.map f) (G.map g)
inst✝ : PreservesColimit (span f g) G
c : PushoutCocone f g
X : C
⊢ ((Cone.postcompose (isoWhiskerRight (cospanOp f g).symm (yoneda.obj X)).hom).obj
            (Cone.whisker walkingSpanOpEquiv.symm.functor ((yoneda.obj X).mapCone (Cocone.op c)))).π.app
      (some WalkingPair.right) =
    (Iso.refl
          ((Cone.postcompose (isoWhiskerRight (cospanOp f g).symm (yoneda.obj X)).hom).obj
              (Cone.whisker walkingSpanOpEquiv.symm.functor ((yoneda.obj X).mapCone (Cocone.op c)))).pt).hom ≫
      ((yoneda.obj X).mapCone c.op).π.app (some WalkingPair.right)
Module: Mathlib.CategoryTheory.MorphismProperty.Composition

Goal state before:
pp: 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✝
g : Y✝ ⟶ Z✝
hf : W.multiplicativeClosure f
hg : W.multiplicativeClosure g
⊢ W.multiplicativeClosure (f ≫ g)

Tactic:
induction hg with
    | of _ hf₀ => exact .comp_of f _ hf hf₀
    | id _ => rwa [Category.comp_id]
    | comp_of f' g hf' hg h_rec =>
      rw [← Category.assoc]
      exact .comp_of (f ≫ f') g (h_rec f hf) hg

Goal state after:
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
⊢ HasPushout f.unop g.unop ↔ HasPullback f g

Tactic:
by
  rw [HasPushout, hasColimit_iff_of_iso (spanUnop f g), hasColimit_inverse_equivalence_comp_iff,
    hasColimit_leftOp_iff_hasLimit]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ (α_ X (𝟙_ C) (𝟙_ C)).hom ≫ (β_ X (𝟙_ C ⊗ 𝟙_ C)).hom ≫ (λ_ (𝟙_ C)).hom ▷ X ≫ (β_ X (𝟙_ C)).inv =
    (α_ X (𝟙_ C) (𝟙_ C)).hom ≫ X ◁ (λ_ (𝟙_ C)).hom ≫ (β_ X (𝟙_ C)).hom ≫ (β_ X (𝟙_ C)).inv

Tactic:
(slice_lhs 2 3 => rw [← braiding_naturality_right])

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ (α_ X (𝟙_ C) (𝟙_ C)).hom ≫ (X ◁ (λ_ (𝟙_ C)).hom ≫ (β_ X (𝟙_ C)).hom) ≫ (β_ X (𝟙_ C)).inv =
    (α_ X (𝟙_ C) (𝟙_ C)).hom ≫ X ◁ (λ_ (𝟙_ C)).hom ≫ (β_ X (𝟙_ C)).hom ≫ (β_ X (𝟙_ C)).inv
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'
e : C ≌ D
inst✝² : e.functor.Monoidal
inst✝¹ : e.inverse.Monoidal
inst✝ : e.IsMonoidal
⊢ ε e.symm.inverse = e.symm.toAdjunction.unit.app (𝟙_ D) ≫ e.symm.inverse.map (η e.symm.functor)

Tactic:
by
    simp only [toAdjunction]
    dsimp [symm]
    rw [counitIso_inv_app_comp_functor_map_η_inverse]

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

Goal state before:
pp: case add
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✝ y✝ z✝ : N
a✝¹ : RingConGen.Rel (Relation.Map ⇑c ⇑f ⇑f) y✝ z✝
h₂ : Relation.Map (⇑c) (⇑f) (⇑f) y✝ z✝
a b : M
h1 : c a b
a✝ : RingConGen.Rel (Relation.Map ⇑c ⇑f ⇑f) (f a) (f b)
⊢ Relation.Map (⇑c) (⇑f) (⇑f) (f a + y✝) (f b + z✝)

Tactic:
rcases h₂ with ⟨p, q, h2, rfl, rfl⟩

Goal state after:
case add
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
a b : M
h1 : c a b
a✝¹ : RingConGen.Rel (Relation.Map ⇑c ⇑f ⇑f) (f a) (f b)
p q : M
h2 : c p q
a✝ : RingConGen.Rel (Relation.Map ⇑c ⇑f ⇑f) (f p) (f q)
⊢ Relation.Map (⇑c) (⇑f) (⇑f) (f a + f p) (f b + f q)
Module: Mathlib.RingTheory.Congruence.Hom

Goal state before:
pp: case add
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✝ w✝ x✝ y✝ z✝ : N
a✝¹ : RingConGen.Rel (Relation.Map ⇑c ⇑f ⇑f) w✝ x✝
a✝ : RingConGen.Rel (Relation.Map ⇑c ⇑f ⇑f) y✝ z✝
h₁ : Relation.Map (⇑c) (⇑f) (⇑f) w✝ x✝
h₂ : Relation.Map (⇑c) (⇑f) (⇑f) y✝ z✝
⊢ Relation.Map (⇑c) (⇑f) (⇑f) (w✝ + y✝) (x✝ + z✝)

Tactic:
| add _ _ h₁ h₂ =>

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

Goal state before:
pp: case mul
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✝ y✝ z✝ : N
a✝¹ : RingConGen.Rel (Relation.Map ⇑c ⇑f ⇑f) y✝ z✝
h₂ : Relation.Map (⇑c) (⇑f) (⇑f) y✝ z✝
a b : M
h1 : c a b
a✝ : RingConGen.Rel (Relation.Map ⇑c ⇑f ⇑f) (f a) (f b)
⊢ Relation.Map (⇑c) (⇑f) (⇑f) (f a * y✝) (f b * z✝)

Tactic:
rcases h₂ with ⟨p, q, h2, rfl, rfl⟩

Goal state after:
case mul
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
a b : M
h1 : c a b
a✝¹ : RingConGen.Rel (Relation.Map ⇑c ⇑f ⇑f) (f a) (f b)
p q : M
h2 : c p q
a✝ : RingConGen.Rel (Relation.Map ⇑c ⇑f ⇑f) (f p) (f q)
⊢ Relation.Map (⇑c) (⇑f) (⇑f) (f a * f p) (f b * f q)
Module: Mathlib.CategoryTheory.Adjunction.Mates

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

Tactic:
simp only [comp_obj, Functor.comp_map, map_comp, assoc]

Goal state after:
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
x : tsze R M
r : R
h : x.fst * r = 1
⊢ x * (inl r + inr (-(r •> (x.snd <• r)))) = 1

Tactic:
ext <;> dsimp
  · rw [add_zero, h]
  · rw [add_zero, zero_add, smul_neg, smul_smul, h, one_smul, neg_add_cancel]

Goal state after:
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
⊢ f 1 + g 0 = 1

Tactic:
rw [map_zero, map_one, add_zero]

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:
by
    ext : 1
    · rw [comp_assoc, comul_comp_inl, ← comp_assoc, rTensor_comp_map, counit_comp_inl,
        ← lTensor_comp_rTensor, comp_assoc, rTensor_counit_comp_comul, lTensor_comp_mk]
    · rw [comp_assoc, comul_comp_inr, ← comp_assoc, rTensor_comp_map, counit_comp_inr,
        ← lTensor_comp_rTensor, comp_assoc, rTensor_counit_comp_comul, lTensor_comp_mk]

Goal state after:
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)
⊢ ↑(TensorProduct.assoc R (Π₀ (i : ι), A i) (Π₀ (i : ι), A i) (Π₀ (i : ι), A i)) ∘ₗ
      rTensor (Π₀ (i : ι), A i) comul ∘ₗ comul =
    lTensor (Π₀ (i : ι), A i) comul ∘ₗ comul

Tactic:
ext i : 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 : ι
⊢ (↑(TensorProduct.assoc R (Π₀ (i : ι), A i) (Π₀ (i : ι), A i) (Π₀ (i : ι), A i)) ∘ₗ
        rTensor (Π₀ (i : ι), A i) comul ∘ₗ comul) ∘ₗ
      lsingle i =
    (lTensor (Π₀ (i : ι), A i) comul ∘ₗ comul) ∘ₗ lsingle i
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u
ι : Type v
A : Type w
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Coalgebra R A
⊢ ↑(TensorProduct.assoc R (ι →₀ A) (ι →₀ A) (ι →₀ A)) ∘ₗ rTensor (ι →₀ A) comul ∘ₗ comul =
    lTensor (ι →₀ A) comul ∘ₗ comul

Tactic:
ext i : 1

Goal state after:
R : Type u
ι : Type v
A : Type w
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Coalgebra R A
i : ι
⊢ (↑(TensorProduct.assoc R (ι →₀ A) (ι →₀ A) (ι →₀ A)) ∘ₗ rTensor (ι →₀ A) comul ∘ₗ comul) ∘ₗ lsingle i =
    (lTensor (ι →₀ A) comul ∘ₗ comul) ∘ₗ lsingle i
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:
simp [RingHom.toModule_smul]

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 (g ≫ ↟(app' f Y'))) y)) s =
    ((CoextendScalars.equiv f ((restrictScalars f).obj Y'))
        ((Hom.hom (↟(app' f Y) ≫ (coextendScalars f).map ((restrictScalars f).map g))) y))
      s

Tactic:
change s • (g y) = g (s • y)

Goal state after:
R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
Y Y' : ModuleCat S
g : Y ⟶ Y'
y : ↑Y
s : S
⊢ s • (ConcreteCategory.hom g) y = (ConcreteCategory.hom g) (s • y)
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: case refine_3.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
m1 : Module R S := Module.compHom S f
m2 : Module R ↑Y := Module.compHom (↑Y) f
s : S
x✝ y✝ : ↑((restrictScalars f).obj (of S S)) ⊗[R] ↑X
ih1 :
  (lift { toFun := fun s ↦ evalAt f s g, map_add' := ⋯, map_smul' := ⋯ }) (s • x✝) =
    s • (lift { toFun := fun s ↦ evalAt f s g, map_add' := ⋯, map_smul' := ⋯ }) x✝
ih2 :
  (lift { toFun := fun s ↦ evalAt f s g, map_add' := ⋯, map_smul' := ⋯ }) (s • y✝) =
    s • (lift { toFun := fun s ↦ evalAt f s g, map_add' := ⋯, map_smul' := ⋯ }) y✝
⊢ s • (lift { toFun := fun s ↦ evalAt f s g, map_add' := ⋯, map_smul' := ⋯ }) x✝ +
      (lift { toFun := fun s ↦ evalAt f s g, map_add' := ⋯, map_smul' := ⋯ }) (s • y✝) =
    s • (lift { toFun := fun s ↦ evalAt f s g, map_add' := ⋯, map_smul' := ⋯ }) (x✝ + y✝)

Tactic:
ih2,

Goal state after:
case refine_3.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
m1 : Module R S := Module.compHom S f
m2 : Module R ↑Y := Module.compHom (↑Y) f
s : S
x✝ y✝ : ↑((restrictScalars f).obj (of S S)) ⊗[R] ↑X
ih1 :
  (lift { toFun := fun s ↦ evalAt f s g, map_add' := ⋯, map_smul' := ⋯ }) (s • x✝) =
    s • (lift { toFun := fun s ↦ evalAt f s g, map_add' := ⋯, map_smul' := ⋯ }) x✝
ih2 :
  (lift { toFun := fun s ↦ evalAt f s g, map_add' := ⋯, map_smul' := ⋯ }) (s • y✝) =
    s • (lift { toFun := fun s ↦ evalAt f s g, map_add' := ⋯, map_smul' := ⋯ }) y✝
⊢ s • (lift { toFun := fun s ↦ evalAt f s g, map_add' := ⋯, map_smul' := ⋯ }) x✝ +
      s • (lift { toFun := fun s ↦ evalAt f s g, map_add' := ⋯, map_smul' := ⋯ }) y✝ =
    s • (lift { toFun := fun s ↦ evalAt f s g, map_add' := ⋯, map_smul' := ⋯ }) (x✝ + y✝)
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

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

Tactic:
by
    let m1 : Module R S := Module.compHom S f; let m2 : Module R Y := Module.compHom Y f
    apply hom_ext
    apply LinearMap.ext; intro z
    induction z using TensorProduct.induction_on with
    | zero => rw [map_zero, map_zero]
    | tmul x s =>
      erw [TensorProduct.lift.tmul]
      simp only [LinearMap.coe_mk]
      change S at x
      dsimp
      erw [← map_smul, ExtendScalars.smul_tmul, mul_one x]
      rfl
    | add _ _ ih1 ih2 => rw [map_add, map_add, ih1, ih2]

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 : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
⊢ (adj1.rightAdjointUniq adj1).hom = 𝟙 G

Tactic:
by
  delta rightAdjointUniq
  simp

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'
f : M →ₗ[R] M'
⊢ α⁻¹ ∘ₗ f ⊗ₘ λ⁻¹ = (f ⊗ₘ LinearMap.id ∘ₗ ρ⁻¹) ⊗ₘ LinearMap.id

Tactic:
by
  ext; rfl

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'
f : M →ₗ[R] M'
⊢ α⁻¹ ∘ₗ f ⊗ₘ ρ⁻¹ = (f ⊗ₘ LinearMap.id) ⊗ₘ LinearMap.id ∘ₗ ρ⁻¹

Tactic:
by
  ext; rfl

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

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

Tactic:
by
  ext; rfl

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

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

Tactic:
by
  ext; rfl

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

Goal state before:
pp: R : Type u_1
M : Type u_3
M' : Type u_6
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
⊢ λ⁻¹ ∘ₗ f = LinearMap.id ⊗ₘ f ∘ₗ λ⁻¹

Tactic:
by
  ext; rfl

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

Goal state before:
pp: R : Type u_1
M : Type u_3
M' : Type u_6
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
⊢ ρ⁻¹ ∘ₗ f = f ⊗ₘ LinearMap.id ∘ₗ ρ⁻¹

Tactic:
by
  ext; rfl

Goal state after: