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

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Reflective i
inst✝³ : MonoidalClosed C
inst✝² : CartesianMonoidalCategory D
inst✝¹ : ExponentialIdeal i
inst✝ : BraidedCategory C
A B : C
⊢ (bijection i A B ((reflector i).obj A ⊗ (reflector i).obj B)).symm (𝟙 ((reflector i).obj A ⊗ (reflector i).obj B)) =
    prodComparison (reflector i) A B

Tactic:
simp only [bijection, Equiv.trans_def, curriedTensor_obj_obj, Equiv.symm_trans_apply,
    Equiv.symm_symm, Functor.FullyFaithful.homEquiv_apply, Functor.map_id, Iso.homCongr_symm,
    Iso.symm_symm_eq, Iso.refl_symm, Iso.homCongr_apply, Iso.refl_hom, Category.comp_id,
    unitCompPartialBijective_symm_apply, Functor.id_obj, Functor.comp_obj, Iso.symm_inv]

Goal state after:
C : Type u₁
D : Type u₂
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Reflective i
inst✝³ : MonoidalClosed C
inst✝² : CartesianMonoidalCategory D
inst✝¹ : ExponentialIdeal i
inst✝ : BraidedCategory C
A B : C
⊢ ((reflectorAdjunction i).homEquiv (A ⊗ B) ((reflector i).obj A ⊗ (reflector i).obj B)).symm
      ((β_ A B).hom ≫
        ((ihom.adjunction B).homEquiv A (i.obj ((reflector i).obj A ⊗ (reflector i).obj B))).symm
          ((reflectorAdjunction i).unit.app A ≫
            ((ihom.adjunction B).homEquiv (i.obj ((reflector i).obj A))
                (i.obj ((reflector i).obj A ⊗ (reflector i).obj B)))
              ((β_ B (i.obj ((reflector i).obj A))).hom ≫
                ((ihom.adjunction (i.obj ((reflector i).obj A))).homEquiv B
                      (i.obj ((reflector i).obj A ⊗ (reflector i).obj B))).symm
                  ((reflectorAdjunction i).unit.app B ≫
                    ((ihom.adjunction (i.obj ((reflector i).obj A))).homEquiv (i.obj ((reflector i).obj B))
                        (i.obj ((reflector i).obj A ⊗ (reflector i).obj B)))
                      (prodComparisonIso i ((reflector i).obj A) ((reflector i).obj B)).inv)))) =
    prodComparison (reflector i) A B
Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.Braided

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
V : Type u₂
inst✝⁶ : Category.{v₂, u₂} V
inst✝⁵ : MonoidalCategory C
inst✝⁴ : BraidedCategory C
inst✝³ : MonoidalCategory V
inst✝² : BraidedCategory V
F G : C ⥤ V
inst✝¹ : DayConvolution F G
inst✝ : DayConvolution G F
⊢ (corepresentableBy F G).homEquiv.symm (braidingHomCorepresenting F G) ≫
      (corepresentableBy G F).homEquiv.symm (braidingInvCorepresenting F G) =
    𝟙 (F ⊛ G)

Tactic:
apply Functor.hom_ext_of_isLeftKanExtension (F ⊛ G) (unit F G)
    ext
    simp [-tensor_obj]

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

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
V : Type u₂
inst✝⁶ : Category.{v₂, u₂} V
inst✝⁵ : MonoidalCategory C
inst✝⁴ : BraidedCategory C
inst✝³ : MonoidalCategory V
inst✝² : BraidedCategory V
F G : C ⥤ V
inst✝¹ : DayConvolution F G
inst✝ : DayConvolution G F
x y : C
⊢ (unit F G).app (x, y) ≫ (braiding F G).hom.app ((tensor C).obj (x, y)) =
    (β_ ((G, F).2.obj (y, x).2) ((G, F).1.obj (y, x).1)).hom ≫
      (unit G F).app (y, x) ≫ (G ⊛ F).map (β_ (y, x).1 (y, x).2).hom

Tactic:
simp [braiding, braidingHomCorepresenting, -tensor_obj]

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

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
V : Type u₂
inst✝⁶ : Category.{v₂, u₂} V
inst✝⁵ : MonoidalCategory C
inst✝⁴ : BraidedCategory C
inst✝³ : MonoidalCategory V
inst✝² : BraidedCategory V
F G : C ⥤ V
inst✝¹ : DayConvolution F G
inst✝ : DayConvolution G F
x y : C
⊢ (unit G F).app (x, y) ≫ (braiding F G).inv.app ((tensor C).obj (x, y)) =
    (β_ ((F, G).1.obj (y, x).1) ((F, G).2.obj (y, x).2)).inv ≫
      (unit F G).app (y, x) ≫ (F ⊛ G).map (β_ (y, x).2 (y, x).1).inv

Tactic:
simp [braiding, braidingHomCorepresenting, -tensor_obj]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence

Goal state before:
pp: C : Type u
X✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
X Y : NormalMonoidalObject C
f : X = Y
⊢ ((tensorFunc C).obj X✝).map { down := { down := f } } ≫ (normalizeIsoApp C X✝ { as := Y }).hom =
    (normalizeIsoApp C X✝ { as := X }).hom ≫ ((normalize' C).obj X✝).map { down := { down := f } }

Tactic:
subst f

Goal state after:
C : Type u
X✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
X : NormalMonoidalObject C
⊢ ((tensorFunc C).obj X✝).map { down := { down := ⋯ } } ≫ (normalizeIsoApp C X✝ { as := X }).hom =
    (normalizeIsoApp C X✝ { as := X }).hom ≫ ((normalize' C).obj X✝).map { down := { down := ⋯ } }
Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence

Goal state before:
pp: C : Type u
X✝ Y✝ X' X Y : F C
f : X ⟶ Y
ih :
  ∀ (n : NormalMonoidalObject C),
    inclusionObj n ◁ f ≫ (normalizeIsoApp' C Y n).hom = (normalizeIsoApp' C X n).hom ≫ inclusion.map (eqToHom ⋯)
n : NormalMonoidalObject C
⊢ (α_ (inclusionObj n) X' X).inv ≫
      (inclusionObj n ⊗ X') ◁ f ≫ (normalizeIsoApp' C X' n).hom ▷ Y ≫ (normalizeIsoApp' C Y (X'.normalizeObj n)).hom =
    ((α_ (inclusionObj n) X' X).inv ≫
        (normalizeIsoApp' C X' n).hom ▷ X ≫ (normalizeIsoApp' C X (X'.normalizeObj n)).hom) ≫
      inclusion.map (eqToHom ⋯)

Tactic:
whisker_exchange_assoc,

Goal state after:
C : Type u
X✝ Y✝ X' X Y : F C
f : X ⟶ Y
ih :
  ∀ (n : NormalMonoidalObject C),
    inclusionObj n ◁ f ≫ (normalizeIsoApp' C Y n).hom = (normalizeIsoApp' C X n).hom ≫ inclusion.map (eqToHom ⋯)
n : NormalMonoidalObject C
⊢ (α_ (inclusionObj n) X' X).inv ≫
      (normalizeIsoApp' C X' n).hom ▷ X ≫
        inclusionObj (X'.normalizeObj n) ◁ f ≫ (normalizeIsoApp' C Y (X'.normalizeObj n)).hom =
    ((α_ (inclusionObj n) X' X).inv ≫
        (normalizeIsoApp' C X' n).hom ▷ X ≫ (normalizeIsoApp' C X (X'.normalizeObj n)).hom) ≫
      inclusion.map (eqToHom ⋯)
Module: Mathlib.CategoryTheory.Monoidal.Hopf_

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
this : η ≫ Δ ≫ 𝒮 ▷ A ≫ μ = η ≫ Δ ≫ 𝒮 ▷ A ≫ μ
| η ≫ Δ ≫ 𝒮 ▷ A ≫ μ = η ≫ Δ ≫ 𝒮 ▷ A ≫ μ

Tactic:
rhs

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
this : η ≫ Δ ≫ 𝒮 ▷ A ≫ μ = η ≫ Δ ≫ 𝒮 ▷ A ≫ μ
| η ≫ Δ ≫ 𝒮 ▷ A ≫ μ
Module: Mathlib.CategoryTheory.Monoidal.Hopf_

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
this : η ≫ (ρ_ A).inv ≫ A ◁ η ≫ 𝒮 ▷ A ≫ μ = η ≫ ε ≫ η
⊢ η ≫ 𝒮 = η

Tactic:
whisker_exchange_assoc,

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
this : η ≫ (ρ_ A).inv ≫ 𝒮 ▷ 𝟙_ C ≫ A ◁ η ≫ μ = η ≫ ε ≫ η
⊢ η ≫ 𝒮 = η
Module: Mathlib.CategoryTheory.Monoidal.Hopf_

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
this : Δ ≫ 𝒮 ▷ A ≫ μ ≫ ε = Δ ≫ 𝒮 ▷ A ≫ μ ≫ ε
| Δ ≫ 𝒮 ▷ A ≫ μ ≫ ε = Δ ≫ 𝒮 ▷ A ≫ μ ≫ ε

Tactic:
rhs

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
this : Δ ≫ 𝒮 ▷ A ≫ μ ≫ ε = Δ ≫ 𝒮 ▷ A ≫ μ ≫ ε
| Δ ≫ 𝒮 ▷ A ≫ μ ≫ ε
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: case a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
A B : Mon C
M : Bimod A B
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
R S T U : Mon C
P : Bimod R S
Q : Bimod S T
L : Bimod T U
| P.X ◁ Q.actRight ▷ L.X ≫ (α_ P.X Q.X L.X).inv

pp: case a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
A B : Mon C
M : Bimod A B
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
R S T U : Mon C
P : Bimod R S
Q : Bimod S T
L : Bimod T U
| coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ▷ L.X

pp: case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
A B : Mon C
M : Bimod A B
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
R S T U : Mon C
P : Bimod R S
Q : Bimod S T
L : Bimod T U
| coequalizer.π (TensorBimod.actRight P Q ▷ L.X)
    ((α_ (coequalizer (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)) T.X L.X).hom ≫
      coequalizer (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ◁ L.actLeft)

Tactic:
associator_inv_naturality_middle

Goal state after:
case a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
A B : Mon C
M : Bimod A B
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
R S T U : Mon C
P : Bimod R S
Q : Bimod S T
L : Bimod T U
| (α_ P.X (Q.X ⊗ T.X) L.X).inv ≫ (P.X ◁ Q.actRight) ▷ L.X

case a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
A B : Mon C
M : Bimod A B
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
R S T U : Mon C
P : Bimod R S
Q : Bimod S T
L : Bimod T U
| coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ▷ L.X

case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
A B : Mon C
M : Bimod A B
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
R S T U : Mon C
P : Bimod R S
Q : Bimod S T
L : Bimod T U
| coequalizer.π (TensorBimod.actRight P Q ▷ L.X)
    ((α_ (coequalizer (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)) T.X L.X).hom ≫
      coequalizer (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ◁ L.actLeft)
Module: Mathlib.CategoryTheory.Monoidal.Hopf_

Goal state before:
pp: case hba
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ μ ≫ 𝒮 * μ = 1

pp: case hac
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ μ * (𝒮 ⊗ₘ 𝒮) ≫ (β_ A A).hom ≫ μ = 1

Tactic:
· -- Unfold the algebra structure in the convolution monoid,
    -- then `simp?, simp only [tensor_μ], simp?`.
    rw [Conv.mul_eq, Conv.one_eq]
    simp only [Comon.tensorObj_comul, whiskerRight_tensor, comp_whiskerRight, Category.assoc,
      Comon.tensorObj_counit]
    simp only [tensorμ]
    simp only [Category.assoc, pentagon_hom_inv_inv_inv_inv_assoc]
    exact mul_antipode₁ A

Goal state after:
case hac
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ μ * (𝒮 ⊗ₘ 𝒮) ≫ (β_ A A).hom ≫ μ = 1
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon C
P : Bimod R S
⊢ (λ_ P.X).inv ≫ η ▷ P.X ≫ P.actLeft = 𝟙 P.X

Tactic:
one_actLeft,

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon C
P : Bimod R S
⊢ (λ_ P.X).inv ≫ (λ_ P.X).hom = 𝟙 P.X
Module: Mathlib.CategoryTheory.Monoidal.DayConvolution

Goal state before:
pp: C : Type u₁
inst✝¹³ : Category.{v₁, u₁} C
V : Type u₂
inst✝¹² : Category.{v₂, u₂} V
inst✝¹¹ : MonoidalCategory C
inst✝¹⁰ : MonoidalCategory V
F G : C ⥤ V
inst✝⁹ : DayConvolution F G
H : C ⥤ V
inst✝⁸ : DayConvolution G H
inst✝⁷ : DayConvolution F (G ⊛ H)
inst✝⁶ : DayConvolution (F ⊛ G) H
inst✝⁵ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)
inst✝⁴ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)
F' G' H' : C ⥤ V
inst✝³ : DayConvolution F' G'
inst✝² : DayConvolution G' H'
inst✝¹ : DayConvolution F' (G' ⊛ H')
inst✝ : DayConvolution (F' ⊛ G') H'
f : F ⟶ F'
g : G ⟶ G'
h : H ⟶ H'
x✝ : (C × C) × C
⊢ (f.app x✝.1.1 ⊗ₘ g.app x✝.1.2) ▷ H.obj x✝.2 ≫
      (F'.obj x✝.1.1 ⊗ G'.obj x✝.1.2) ◁ h.app x✝.2 ≫
        (α_ (F'.obj x✝.1.1) ((G', H').1.obj (x✝.1.2, x✝.2).1) ((G', H').2.obj (x✝.1.2, x✝.2).2)).hom ≫
          F'.obj x✝.1.1 ◁ (unit G' H').app (x✝.1.2, x✝.2) ≫
            (unit F' (G' ⊛ H')).app (x✝.1.1, x✝.1.2 ⊗ x✝.2) ≫
              (F' ⊛ G' ⊛ H').map (α_ (x✝.1.1, x✝.1.2 ⊗ x✝.2).1 x✝.1.2 x✝.2).inv =
    (α_ (F.obj x✝.1.1) (G.obj x✝.1.2) (H.obj x✝.2)).hom ≫
      F.obj x✝.1.1 ◁ (unit G H).app (x✝.1.2, x✝.2) ≫
        f.app x✝.1.1 ▷ (G ⊛ H).obj (x✝.1.2 ⊗ x✝.2) ≫
          F'.obj x✝.1.1 ◁ (map g h).app (x✝.1.2 ⊗ x✝.2) ≫
            (unit F' (G' ⊛ H')).app (x✝.1.1, x✝.1.2 ⊗ x✝.2) ≫ (F' ⊛ G' ⊛ H').map (α_ x✝.1.1 x✝.1.2 x✝.2).inv

Tactic:
whisker_exchange_assoc,

Goal state after:
C : Type u₁
inst✝¹³ : Category.{v₁, u₁} C
V : Type u₂
inst✝¹² : Category.{v₂, u₂} V
inst✝¹¹ : MonoidalCategory C
inst✝¹⁰ : MonoidalCategory V
F G : C ⥤ V
inst✝⁹ : DayConvolution F G
H : C ⥤ V
inst✝⁸ : DayConvolution G H
inst✝⁷ : DayConvolution F (G ⊛ H)
inst✝⁶ : DayConvolution (F ⊛ G) H
inst✝⁵ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)
inst✝⁴ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)
F' G' H' : C ⥤ V
inst✝³ : DayConvolution F' G'
inst✝² : DayConvolution G' H'
inst✝¹ : DayConvolution F' (G' ⊛ H')
inst✝ : DayConvolution (F' ⊛ G') H'
f : F ⟶ F'
g : G ⟶ G'
h : H ⟶ H'
x✝ : (C × C) × C
⊢ (f.app x✝.1.1 ⊗ₘ g.app x✝.1.2) ▷ H.obj x✝.2 ≫
      (F'.obj x✝.1.1 ⊗ G'.obj x✝.1.2) ◁ h.app x✝.2 ≫
        (α_ (F'.obj x✝.1.1) ((G', H').1.obj (x✝.1.2, x✝.2).1) ((G', H').2.obj (x✝.1.2, x✝.2).2)).hom ≫
          F'.obj x✝.1.1 ◁ (unit G' H').app (x✝.1.2, x✝.2) ≫
            (unit F' (G' ⊛ H')).app (x✝.1.1, x✝.1.2 ⊗ x✝.2) ≫
              (F' ⊛ G' ⊛ H').map (α_ (x✝.1.1, x✝.1.2 ⊗ x✝.2).1 x✝.1.2 x✝.2).inv =
    (α_ (F.obj x✝.1.1) (G.obj x✝.1.2) (H.obj x✝.2)).hom ≫
      f.app x✝.1.1 ▷ (G.obj x✝.1.2 ⊗ H.obj x✝.2) ≫
        F'.obj x✝.1.1 ◁ (unit G H).app (x✝.1.2, x✝.2) ≫
          F'.obj x✝.1.1 ◁ (map g h).app (x✝.1.2 ⊗ x✝.2) ≫
            (unit F' (G' ⊛ H')).app (x✝.1.1, x✝.1.2 ⊗ x✝.2) ≫ (F' ⊛ G' ⊛ H').map (α_ x✝.1.1 x✝.1.2 x✝.2).inv
Module: Mathlib.CategoryTheory.MorphismProperty.LocalClosure

Goal state before:
pp: case refine_1.of_iso
C : Type u
inst✝⁶ : Category.{v, u} C
K : Precoverage C
P : MorphismProperty C
inst✝⁵ : P.RespectsIso
inst✝⁴ : P.RespectsLeft K.morphismProperty
inst✝³ : K.HasIsos
inst✝² : K.IsStableUnderBaseChange
inst✝¹ : K.IsStableUnderComposition
inst✝ : K.HasPullbacks
X Y : C
f✝ : X ⟶ Y
X✝ Y✝ X'✝ Y'✝ : C
f : X✝ ⟶ Y✝
g : X'✝ ⟶ Y'✝
e : Arrow.mk f ≅ Arrow.mk g
hf : sourceLocalClosure K P f
h : ∃ R ∈ K.coverings X✝, ∀ (U : C) (g : U ⟶ X✝), R g → P (g ≫ f)
⊢ ∃ R ∈ K.coverings X'✝, ∀ (U : C) (g_1 : U ⟶ X'✝), R g_1 → P (g_1 ≫ g)

Tactic:
obtain ⟨R, hR, h⟩ := h
      rw [K.mem_iff_exists_zeroHypercover] at hR
      obtain ⟨E, rfl⟩ := hR
      refine ⟨_, (E.pushforward e.hom.left (K.mem_coverings_of_isIso _)).mem₀, ?_⟩
      intro U v ⟨i⟩
      dsimp
      simp only [Category.assoc, Arrow.w_mk_right, Arrow.mk_left, Arrow.mk_right, Arrow.mk_hom]
      rw [← Category.assoc, P.cancel_right_of_respectsIso]
      exact h _ _ ⟨i⟩

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
P : MorphismProperty C
inst✝⁴ : ∀ (X : C), IsFinitelyAccessibleCategory (Under X)
inst✝³ : HasPushouts C
inst✝² : P.IsStableUnderComposition
inst✝¹ : P.IsStableUnderCobaseChange
inst✝ : P.PreIndSpreads
H : P ≤ isFinitelyPresentable C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
T : C
p : X ⟶ T
u : T ⟶ Z
hp : isFinitelyPresentable C p
hpu : p ≫ u = f ≫ g
J₁ : Type w
w✝³ : SmallCategory J₁
w✝² : IsFiltered J₁
D₁ : J₁ ⥤ C
s₁ : (Functor.const J₁).obj X ⟶ D₁
t₁ : D₁ ⟶ (Functor.const J₁).obj Y
ht₁ : IsColimit { pt := Y, ι := t₁ }
h₁ : ∀ (j : J₁), P (s₁.app j) ∧ s₁.app j ≫ t₁.app j = f
J₂ : Type w
w✝¹ : SmallCategory J₂
w✝ : IsFiltered J₂
D₂ : J₂ ⥤ C
s₂ : (Functor.const J₂).obj Y ⟶ D₂
t₂ : D₂ ⟶ (Functor.const J₂).obj Z
ht₂ : IsColimit { pt := Z, ι := t₂ }
h₂ : ∀ (j : J₂), P (s₂.app j) ∧ s₂.app j ≫ t₂.app j = g
this : IsFinitelyPresentable (CategoryTheory.Under.mk p)
j₂ : J₂
q : T ⟶ D₂.obj j₂
hcomp : p ≫ q = ((Functor.const J₂).map f ≫ s₂).app j₂
hu : q ≫ { pt := Z, ι := t₂ }.ι.app j₂ = u
j₁ : J₁
W : C
f' : D₁.obj j₁ ⟶ W
g' : W ⟶ D₂.obj j₂
h : IsPushout ({ pt := Y, ι := t₁ }.ι.app j₁) f' (s₂.app j₂) g'
hf' : P f'
D' : Under j₁ ⥤ C := (Under.post D₁ ⋙ Under.pushout f') ⋙ CategoryTheory.Under.forget W
⊢ ∃ W u_1 v, u_1 ≫ v = u ∧ P (p ≫ u_1)

Tactic:
let c' : Cocone D' :=
      (Under.pushout f' ⋙ CategoryTheory.Under.forget _).mapCocone
        ((Cocone.mk _ t₁).underPost j₁) |>.extend h.isoPushout.inv

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
P : MorphismProperty C
inst✝⁴ : ∀ (X : C), IsFinitelyAccessibleCategory (Under X)
inst✝³ : HasPushouts C
inst✝² : P.IsStableUnderComposition
inst✝¹ : P.IsStableUnderCobaseChange
inst✝ : P.PreIndSpreads
H : P ≤ isFinitelyPresentable C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
T : C
p : X ⟶ T
u : T ⟶ Z
hp : isFinitelyPresentable C p
hpu : p ≫ u = f ≫ g
J₁ : Type w
w✝³ : SmallCategory J₁
w✝² : IsFiltered J₁
D₁ : J₁ ⥤ C
s₁ : (Functor.const J₁).obj X ⟶ D₁
t₁ : D₁ ⟶ (Functor.const J₁).obj Y
ht₁ : IsColimit { pt := Y, ι := t₁ }
h₁ : ∀ (j : J₁), P (s₁.app j) ∧ s₁.app j ≫ t₁.app j = f
J₂ : Type w
w✝¹ : SmallCategory J₂
w✝ : IsFiltered J₂
D₂ : J₂ ⥤ C
s₂ : (Functor.const J₂).obj Y ⟶ D₂
t₂ : D₂ ⟶ (Functor.const J₂).obj Z
ht₂ : IsColimit { pt := Z, ι := t₂ }
h₂ : ∀ (j : J₂), P (s₂.app j) ∧ s₂.app j ≫ t₂.app j = g
this : IsFinitelyPresentable (CategoryTheory.Under.mk p)
j₂ : J₂
q : T ⟶ D₂.obj j₂
hcomp : p ≫ q = ((Functor.const J₂).map f ≫ s₂).app j₂
hu : q ≫ { pt := Z, ι := t₂ }.ι.app j₂ = u
j₁ : J₁
W : C
f' : D₁.obj j₁ ⟶ W
g' : W ⟶ D₂.obj j₂
h : IsPushout ({ pt := Y, ι := t₁ }.ι.app j₁) f' (s₂.app j₂) g'
hf' : P f'
D' : Under j₁ ⥤ C := (Under.post D₁ ⋙ Under.pushout f') ⋙ CategoryTheory.Under.forget W
c' : Cocone D' :=
  ((Under.pushout f' ⋙ CategoryTheory.Under.forget W).mapCocone ({ pt := Y, ι := t₁ }.underPost j₁)).extend
    h.isoPushout.inv
⊢ ∃ W u_1 v, u_1 ≫ v = u ∧ P (p ≫ u_1)
Module: Mathlib.CategoryTheory.Subobject.ArtinianObject

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
⊢ WellFoundedGT (Subobject X)ᵒᵈ ↔ ∀ (f : ℕ →o (Subobject X)ᵒᵈ), ∃ n, ∀ (m : ℕ), n ≤ m → f n = f m

Tactic:
wellFoundedGT_iff_monotone_chain_condition

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X : C
⊢ (∀ (a : ℕ →o (Subobject X)ᵒᵈ), ∃ n, ∀ (m : ℕ), n ≤ m → a n = a m) ↔
    ∀ (f : ℕ →o (Subobject X)ᵒᵈ), ∃ n, ∀ (m : ℕ), n ≤ m → f n = f m
Module: Mathlib.CategoryTheory.Subobject.NoetherianObject

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
⊢ WellFoundedGT (Subobject X) ↔ ∀ (f : ℕ →o Subobject X), ∃ n, ∀ (m : ℕ), n ≤ m → f n = f m

Tactic:
wellFoundedGT_iff_monotone_chain_condition

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X : C
⊢ (∀ (a : ℕ →o Subobject X), ∃ n, ∀ (m : ℕ), n ≤ m → a n = a m) ↔
    ∀ (f : ℕ →o Subobject X), ∃ n, ∀ (m : ℕ), n ≤ m → f n = f m
Module: Mathlib.CategoryTheory.MorphismProperty.Ind

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
P : MorphismProperty C
inst✝⁴ : ∀ (X : C), IsFinitelyAccessibleCategory (Under X)
inst✝³ : HasPushouts C
inst✝² : P.IsStableUnderComposition
inst✝¹ : P.IsStableUnderCobaseChange
inst✝ : P.PreIndSpreads
H : P ≤ isFinitelyPresentable C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : P.ind f
hg : P.ind g
⊢ P.ind (f ≫ g)

Tactic:
rw [ind_iff_exists H]
    intro T p u hp hpu
    obtain ⟨J₁, _, _, D₁, s₁, t₁, ht₁, h₁⟩ := hf
    obtain ⟨J₂, _, _, D₂, s₂, t₂, ht₂, h₂⟩ := hg
    have : IsFinitelyPresentable (CategoryTheory.Under.mk p) := hp
    obtain ⟨j₂, q, hcomp, hu⟩ := IsFinitelyPresentable.exists_hom_of_isColimit_under
        ht₂ p ((Functor.const _).map f ≫ s₂) u <| by simp [h₂, hpu]
    obtain ⟨j₁, W, f', g', h, hf'⟩ :=
      P.exists_isPushout_of_isFiltered ht₁ (s₂.app j₂) (h₂ j₂).left
    let D' : Under j₁ ⥤ C :=
      (Under.post D₁ ⋙ Under.pushout f') ⋙ CategoryTheory.Under.forget _
    let c' : Cocone D' :=
      (Under.pushout f' ⋙ CategoryTheory.Under.forget _).mapCocone
        ((Cocone.mk _ t₁).underPost j₁) |>.extend h.isoPushout.inv
    let hc' : IsColimit c' :=
      IsColimit.extendIso _ <| isColimitOfPreserves _ (ht₁.underPost j₁)
    let s' : (Functor.const (Under j₁)).obj X ⟶ D' :=
      { app k := s₁.app k.right ≫ pushout.inl _ _
        naturality k l a := by
          have h2 := s₁.naturality a.right
          simp only [Functor.const_obj_obj, Functor.const_obj_map, Category.id_comp] at h2
          simp [h2, D'] }
    obtain ⟨j₃, v, hcomp', hq⟩ := IsFinitelyPresentable.exists_hom_of_isColimit_under
        hc' p s' q <| fun k ↦ by
      simp [c', s', hcomp, reassoc_of% (h₁ k.right).right]
    refine ⟨D'.obj j₃, v, c'.ι.app j₃ ≫ t₂.app j₂, ?_, ?_⟩
    · rwa [reassoc_of% hq]
    · rw [hcomp']
      exact P.comp_mem _ _ (h₁ _).left (P.pushout_inl _ _ hf')

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.EilenbergMoore

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : Preadditive C
T : Monad C
inst✝¹ : T.Additive
U : Comonad C
inst✝ : U.Additive
F G : U.Coalgebra
⊢ F.a ≫ U.map 0 = 0 ≫ G.a

Tactic:
simp only [Functor.map_zero, comp_zero, zero_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.EndoFunctor

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : F.Additive
A₁ A₂ : Algebra F
r : ℤ
α : A₁ ⟶ A₂
⊢ F.map (r • α.f) ≫ A₂.str = A₁.str ≫ (r • α.f)

Tactic:
by rw [comp_zsmul, Functor.map_zsmul, zsmul_comp, Endofunctor.Algebra.Hom.h]

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Mat

Goal state before:
pp: case h₁
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
i : Fin n
j : (f i).ι
i' : Fin n
j' : (f i').ι
⊢ i ∉ Finset.univ →
    (∑ j_1,
        (if h : i = i then if h' : h ▸ j = j_1 then eqToHom ⋯ else 0 else 0) ≫
          if h : i' = i then if h' : h ▸ j' = j_1 then eqToHom ⋯ else 0 else 0) =
      0

Tactic:
intro hi
              simp at hi

Goal state after: