mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Galois.IsFundamentalgroup

Goal state before:
pp: C : Type u₁
inst✝⁹ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : (X : C) → MulAction G (F.obj X).obj
inst✝⁶ : IsNaturalSMul F G
inst✝⁵ : GaloisCategory C
inst✝⁴ : FiberFunctor F
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : CompactSpace G
inst✝ : ∀ (X : C), ContinuousSMul G (F.obj X).obj
h : ∀ (X : C) [IsGalois X], MulAction.IsPretransitive G (F.obj X).obj
t : Aut F
gi : PointedGaloisObject F → G
hgi : ∀ (X : PointedGaloisObject F) (x : (F.obj X.obj).obj), gi X • x = (ConcreteCategory.hom (t.hom.app X.obj)) x
cl : PointedGaloisObject F → Set G := fun X ↦ gi X • ↑(MulAction.stabilizer G X.pt)
c : Set G := ⋂ i, cl i
⊢ ∃ a, (toAut F G) a = t

Tactic:
have hne : c.Nonempty := by
    rw [← Set.univ_inter c]
    apply CompactSpace.isCompact_univ.inter_iInter_nonempty
    · intro X
      apply IsClosed.leftCoset
      exact Subgroup.isClosed_of_isOpen _ (stabilizer_isOpen G X.pt)
    · intro s
      rw [Set.univ_inter]
      obtain ⟨gs, hgs⟩ :=
        toAut_surjective_isGalois_finite_family F G t (fun X : s ↦ X.val.obj) h
      use gs
      simp only [Set.mem_iInter]
      intro X hXmem
      rw [mem_leftCoset_iff, SetLike.mem_coe, MulAction.mem_stabilizer_iff, mul_smul,
        hgs ⟨X, hXmem⟩, ← hgi X, inv_smul_smul]

Goal state after:
C : Type u₁
inst✝⁹ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : (X : C) → MulAction G (F.obj X).obj
inst✝⁶ : IsNaturalSMul F G
inst✝⁵ : GaloisCategory C
inst✝⁴ : FiberFunctor F
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : CompactSpace G
inst✝ : ∀ (X : C), ContinuousSMul G (F.obj X).obj
h : ∀ (X : C) [IsGalois X], MulAction.IsPretransitive G (F.obj X).obj
t : Aut F
gi : PointedGaloisObject F → G
hgi : ∀ (X : PointedGaloisObject F) (x : (F.obj X.obj).obj), gi X • x = (ConcreteCategory.hom (t.hom.app X.obj)) x
cl : PointedGaloisObject F → Set G := fun X ↦ gi X • ↑(MulAction.stabilizer G X.pt)
c : Set G := ⋂ i, cl i
hne : c.Nonempty
⊢ ∃ a, (toAut F G) a = t
Module: Mathlib.CategoryTheory.Join.Basic

Goal state before:
pp: case left
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
D' : Type u₄
inst✝ : Category.{v₄, u₄} D'
e : C ≌ C'
e' : D ≌ D'
a✝ : C
⊢ (mapPair e.functor e'.functor).map
        ((mapPairId.symm ≪≫
                mapIsoWhiskerRight e.unitIso (𝟭 D) ≪≫
                  mapIsoWhiskerLeft (e.functor ⋙ e.inverse) e'.unitIso ≪≫
                    mapPairComp e.functor e'.functor e.inverse e'.inverse).hom.app
          (left a✝)) ≫
      ((mapPairComp e.inverse e'.inverse e.functor e'.functor).symm ≪≫
              mapIsoWhiskerRight e.counitIso (e'.inverse ⋙ e'.functor) ≪≫
                mapIsoWhiskerLeft (𝟭 C') e'.counitIso ≪≫ mapPairId).hom.app
        ((mapPair e.functor e'.functor).obj (left a✝)) =
    𝟙 ((mapPair e.functor e'.functor).obj (left a✝))

Tactic:
simp [← (inclLeft C' D').map_comp, ← (inclRight C' D').map_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Join.Basic

Goal state before:
pp: case right
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
D' : Type u₄
inst✝ : Category.{v₄, u₄} D'
e : C ≌ C'
e' : D ≌ D'
a✝ : D
⊢ (mapPair e.functor e'.functor).map
        ((mapPairId.symm ≪≫
                mapIsoWhiskerRight e.unitIso (𝟭 D) ≪≫
                  mapIsoWhiskerLeft (e.functor ⋙ e.inverse) e'.unitIso ≪≫
                    mapPairComp e.functor e'.functor e.inverse e'.inverse).hom.app
          (right a✝)) ≫
      ((mapPairComp e.inverse e'.inverse e.functor e'.functor).symm ≪≫
              mapIsoWhiskerRight e.counitIso (e'.inverse ⋙ e'.functor) ≪≫
                mapIsoWhiskerLeft (𝟭 C') e'.counitIso ≪≫ mapPairId).hom.app
        ((mapPair e.functor e'.functor).obj (right a✝)) =
    𝟙 ((mapPair e.functor e'.functor).obj (right a✝))

Tactic:
simp [← (inclLeft C' D').map_comp, ← (inclRight C' D').map_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.PiProd

Goal state before:
pp: case pos
C : Type u_1
I : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
X Y : I → C
f : (i : I) → X i ⟶ Y i
P : I → Prop
inst✝⁶ : HasProduct X
inst✝⁵ : HasProduct Y
inst✝⁴ : HasProduct fun i ↦ X ↑i
inst✝³ : HasProduct fun i ↦ X ↑i
inst✝² : HasProduct fun i ↦ Y ↑i
inst✝¹ : HasProduct fun i ↦ Y ↑i
inst✝ : (i : I) → Decidable (P i)
x✝¹ : BinaryFan (∏ᶜ fun i ↦ X ↑i) (∏ᶜ fun i ↦ X ↑i)
x✝ : x✝¹.pt ⟶ ∏ᶜ X
h₁ : (x✝ ≫ map' Subtype.val fun x ↦ 𝟙 (X ↑x)) = x✝¹.fst
h₂ : (x✝ ≫ map' Subtype.val fun x ↦ 𝟙 (X ↑x)) = x✝¹.snd
b : I
h : P b
⊢ x✝ ≫ π X b =
    (lift fun b ↦
        if h : P b then x✝¹.π.app { as := WalkingPair.left } ≫ π (fun i ↦ X ↑i) ⟨b, h⟩
        else x✝¹.π.app { as := WalkingPair.right } ≫ π (fun i ↦ X ↑i) ⟨b, h⟩) ≫
      π X b

Tactic:
simp [← h₁, dif_pos h]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.PreservesLimit

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : Type u'
inst✝¹ : Category.{v', u'} J
inst✝ : LocallySmall.{w, v, u} C
F : J ⥤ Cᵒᵖ
c : Cone F
c' : Cocone (F.leftOp ⋙ shrinkYoneda.{w, v, u})
hc : IsLimit c
hc' : IsColimit c'
P : Cᵒᵖ ⥤ Type w
f : c'.pt ⟶ P
X X' : J
g : X ⟶ X'
⊢ (ConcreteCategory.hom (P.map (F.map g))) (shrinkYonedaEquiv (c'.ι.app (op X) ≫ f)) =
    (ConcreteCategory.hom ((c'.ι.app (op X) ≫ f).app (op (unop (F.1 X')))))
      (shrinkYonedaEquiv (shrinkYoneda.{w, v, u}.map (F.map g).unop))

Tactic:
rw [shrinkYonedaEquiv_shrinkYoneda_map]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
J : Type u'
inst✝¹ : Category.{v', u'} J
inst✝ : LocallySmall.{w, v, u} C
F : J ⥤ Cᵒᵖ
c : Cone F
c' : Cocone (F.leftOp ⋙ shrinkYoneda.{w, v, u})
hc : IsLimit c
hc' : IsColimit c'
P : Cᵒᵖ ⥤ Type w
f : c'.pt ⟶ P
X X' : J
g : X ⟶ X'
⊢ (ConcreteCategory.hom (P.map (F.map g))) (shrinkYonedaEquiv (c'.ι.app (op X) ≫ f)) =
    (ConcreteCategory.hom ((c'.ι.app (op X) ≫ f).app (op (unop (F.1 X')))))
      (shrinkYonedaObjObjEquiv.symm (F.map g).unop)
Module: Mathlib.CategoryTheory.Localization.BousfieldTransfiniteComposition

Goal state before:
pp: case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
P : ObjectProperty C
J : Type w
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
inst✝¹ : OrderBot J
inst✝ : WellFoundedLT J
X Y : C
f : X ⟶ Y
x✝ : P.isLocal.transfiniteCompositionsOfShape J f
Z : C
hZ : P Z
hf : P.isLocal.TransfiniteCompositionOfShape J f
g : X ⟶ Z
d : (hf.F.op ⋙ yoneda.obj Z).WellOrderInductionData := Functor.WellOrderInductionData.ofExists ⋯ ⋯
σ : ↑(hf.F.op ⋙ yoneda.obj Z).sections := d.sectionsMk (hf.isoBot.hom ≫ g)
c : Cocone hf.F := { pt := Z, ι := { app := fun j ↦ ↑σ (op j), naturality := ⋯ } }
⊢ ∃ a, (fun g ↦ f ≫ g) a = g

Tactic:
exact ⟨hf.isColimit.desc c, by
        simp only [← hf.fac, Category.assoc, hf.isColimit.fac c ⊥, c, σ,
          d.sectionsMk_val_op_bot, Iso.inv_hom_id_assoc]⟩

Goal state after:
Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfFunctorialResolutions

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
ρ : C₂ ⥤ C₁
i : 𝟭 C₂ ⟶ ρ ⋙ Φ.functor
hi : ∀ (X₂ : C₂), W₂ (i.app X₂)
hW₁ : W₁ = W₂.inverseImage Φ.functor
inst✝³ : Φ.functor.Full
inst✝² : Φ.functor.Faithful
inst✝¹ : W₂.HasTwoOutOfThreeProperty
inst✝ : W₂.IsMultiplicative
this✝ : W₁.IsMultiplicative
this : Φ.IsLocalizedEquivalence
⊢ Φ.IsRightDerivabilityStructure

Tactic:
have := Φ.hasRightResolutions_arrow_of_functorial_resolutions i hi

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
ρ : C₂ ⥤ C₁
i : 𝟭 C₂ ⟶ ρ ⋙ Φ.functor
hi : ∀ (X₂ : C₂), W₂ (i.app X₂)
hW₁ : W₁ = W₂.inverseImage Φ.functor
inst✝³ : Φ.functor.Full
inst✝² : Φ.functor.Faithful
inst✝¹ : W₂.HasTwoOutOfThreeProperty
inst✝ : W₂.IsMultiplicative
this✝¹ : W₁.IsMultiplicative
this✝ : Φ.IsLocalizedEquivalence
this : Φ.arrow.HasRightResolutions
⊢ Φ.IsRightDerivabilityStructure
Module: Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Groupoid

Goal state before:
pp: D : Type u
C : Type u_1
inst✝³ : Groupoid D
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalClosed C
F G : D ⥤ C
⊢ ∀ ⦃X Y : D⦄ (f : X ⟶ Y),
    ((𝟭 (D ⥤ C)).obj G).map f ≫ (ihom.coev (F.obj Y)).app (G.obj Y) =
      (ihom.coev (F.obj X)).app (G.obj X) ≫ ((tensorLeft F ⋙ F.closedIhom).obj G).map f

Tactic:
by
      intro X Y f
      dsimp
      simp only [ihom.coev_naturality, closedIhom_obj_map, Monoidal.tensorObj_map]
      dsimp
      rw [coev_app_comp_pre_app_assoc, ← Functor.map_comp, tensorHom_def]
      simp

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

Goal state before:
pp: 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)
X Y Z : Mon C
M : Bimod X Y
N₁ N₂ : Bimod Y Z
f : N₁ ⟶ N₂
⊢ ((α_ M.X Y.X N₁.X).hom ≫ M.X ◁ N₁.actLeft) ≫ M.X ◁ f.hom =
    (M.X ⊗ Y.X) ◁ f.hom ≫ (α_ M.X Y.X N₂.X).hom ≫ M.X ◁ N₂.actLeft

Tactic:
simp only [Category.assoc, tensor_whiskerLeft, Iso.inv_hom_id_assoc,
            Iso.cancel_iso_hom_left]

Goal state after:
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)
X Y Z : Mon C
M : Bimod X Y
N₁ N₂ : Bimod Y Z
f : N₁ ⟶ N₂
⊢ M.X ◁ N₁.actLeft ≫ M.X ◁ f.hom = M.X ◁ Y.X ◁ f.hom ≫ M.X ◁ N₂.actLeft
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
X X' : D
f : (reflector i).obj (A ⊗ B) ⟶ X
g : X ⟶ X'
⊢ i.map
      (i.fullyFaithfulOfReflective.preimage
        (prodComparison i ((reflector i).obj A) ((reflector i).obj B) ≫
          uncurry
              ((unitCompPartialBijective B ⋯)
                (curry
                  ((β_ B (i.obj ((reflector i).obj A))).inv ≫
                    uncurry
                        ((unitCompPartialBijective A ⋯)
                          (curry
                            ((β_ A B).inv ≫ ((reflectorAdjunction i).homEquiv (A ⊗ B) X') (f ≫ g) ≫ 𝟙 (i.obj X')))) ≫
                      𝟙 (i.obj X')))) ≫
            𝟙 (i.obj X'))) =
    i.map
      (i.fullyFaithfulOfReflective.preimage
          (prodComparison i ((reflector i).obj A) ((reflector i).obj B) ≫
            uncurry
                ((unitCompPartialBijective B ⋯)
                  (curry
                    ((β_ B (i.obj ((reflector i).obj A))).inv ≫
                      uncurry
                          ((unitCompPartialBijective A ⋯)
                            (curry ((β_ A B).inv ≫ ((reflectorAdjunction i).homEquiv (A ⊗ B) X) f ≫ 𝟙 (i.obj X)))) ≫
                        𝟙 (i.obj X)))) ≫
              𝟙 (i.obj X)) ≫
        g)

Tactic:
Functor.FullyFaithful.map_preimage,

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
X X' : D
f : (reflector i).obj (A ⊗ B) ⟶ X
g : X ⟶ X'
⊢ prodComparison i ((reflector i).obj A) ((reflector i).obj B) ≫
      uncurry
          ((unitCompPartialBijective B ⋯)
            (curry
              ((β_ B (i.obj ((reflector i).obj A))).inv ≫
                uncurry
                    ((unitCompPartialBijective A ⋯)
                      (curry ((β_ A B).inv ≫ ((reflectorAdjunction i).homEquiv (A ⊗ B) X') (f ≫ g) ≫ 𝟙 (i.obj X')))) ≫
                  𝟙 (i.obj X')))) ≫
        𝟙 (i.obj X') =
    i.map
      (i.fullyFaithfulOfReflective.preimage
          (prodComparison i ((reflector i).obj A) ((reflector i).obj B) ≫
            uncurry
                ((unitCompPartialBijective B ⋯)
                  (curry
                    ((β_ B (i.obj ((reflector i).obj A))).inv ≫
                      uncurry
                          ((unitCompPartialBijective A ⋯)
                            (curry ((β_ A B).inv ≫ ((reflectorAdjunction i).homEquiv (A ⊗ B) X) f ≫ 𝟙 (i.obj X)))) ≫
                        𝟙 (i.obj X)))) ≫
              𝟙 (i.obj X)) ≫
        g)
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
η : F ⟶ G
H : C ⥤ V
inst✝³ : DayConvolution F H
inst✝² : DayConvolution H F
inst✝¹ : DayConvolution G H
inst✝ : DayConvolution H G
⊢ map η (𝟙 H) ≫ (braiding G H).hom = (braiding F H).hom ≫ map (𝟙 H) η

Tactic:
by
  apply Functor.hom_ext_of_isLeftKanExtension (F ⊛ H) (unit F H)
  ext ⟨_, _⟩
  simp

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✝¹² : ∀ (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)
H : C ⥤ V
inst✝¹⁰ : DayConvolution F G
inst✝⁹ : DayConvolution G H
inst✝⁸ : DayConvolution F (G ⊛ H)
inst✝⁷ : DayConvolution (F ⊛ G) H
inst✝⁶ : DayConvolution H F
inst✝⁵ : DayConvolution G (H ⊛ F)
inst✝⁴ : DayConvolution (G ⊛ H) F
inst✝³ : DayConvolution G F
inst✝² : DayConvolution (G ⊛ F) H
inst✝¹ : DayConvolution F H
inst✝ : DayConvolution G (F ⊛ H)
z x y : C
⊢ (β_ (F.obj x) (G.obj y)).hom ▷ H.obj z ≫
      (α_ (G.obj y) (F.obj x) (H.obj z)).hom ≫
        G.obj y ◁ ((β_ (F.obj x) (H.obj z)).hom ≫ (unit H F).app (z, x)) ≫
          (unit G (H ⊛ F)).app (y, z ⊗ x) ≫
            (G ⊛ H ⊛ F).map (y ◁ (β_ z x).hom) ≫ (G ⊛ H ⊛ F).map (α_ y x z).inv ≫ (G ⊛ H ⊛ F).map ((β_ y x).hom ▷ z) =
    ((β_ (F.obj x) (G.obj y)).hom ≫ (unit G F).app (y, x) ≫ (G ⊛ F).map (β_ y x).hom) ▷ H.obj z ≫
      (unit (G ⊛ F) H).app (x ⊗ y, z) ≫
        (associator G F H).hom.app ((x ⊗ y) ⊗ z) ≫ (map (𝟙 G) (braiding F H).hom).app ((x ⊗ y) ⊗ z)

Tactic:
simp only [whiskerLeft_comp, ← Functor.map_comp, Category.assoc,
    Functor.comp_obj, tensor_obj, comp_whiskerRight,
    whiskerRight_comp_unit_app_assoc, NatTrans.naturality_assoc,
    NatTrans.naturality, associator_hom_unit_unit_assoc,
    externalProductBifunctor_obj_obj, unit_app_map_app_assoc, NatTrans.id_app,
    id_tensorHom]

Goal state after:
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✝¹² : ∀ (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)
H : C ⥤ V
inst✝¹⁰ : DayConvolution F G
inst✝⁹ : DayConvolution G H
inst✝⁸ : DayConvolution F (G ⊛ H)
inst✝⁷ : DayConvolution (F ⊛ G) H
inst✝⁶ : DayConvolution H F
inst✝⁵ : DayConvolution G (H ⊛ F)
inst✝⁴ : DayConvolution (G ⊛ H) F
inst✝³ : DayConvolution G F
inst✝² : DayConvolution (G ⊛ F) H
inst✝¹ : DayConvolution F H
inst✝ : DayConvolution G (F ⊛ H)
z x y : C
⊢ (β_ (F.obj x) (G.obj y)).hom ▷ H.obj z ≫
      (α_ (G.obj y) (F.obj x) (H.obj z)).hom ≫
        G.obj y ◁ (β_ (F.obj x) (H.obj z)).hom ≫
          G.obj y ◁ (unit H F).app (z, x) ≫
            (unit G (H ⊛ F)).app (y, z ⊗ x) ≫ (G ⊛ H ⊛ F).map (y ◁ (β_ z x).hom ≫ (α_ y x z).inv ≫ (β_ y x).hom ▷ z) =
    (β_ (F.obj x) (G.obj y)).hom ▷ H.obj z ≫
      (α_ (G.obj y) (F.obj x) (H.obj z)).hom ≫
        G.obj y ◁ (unit F H).app (x, z) ≫
          G.obj y ◁ (braiding F H).hom.app (x ⊗ z) ≫
            (unit G (H ⊛ F)).app (y, x ⊗ z) ≫ (G ⊛ H ⊛ F).map ((α_ y x z).inv ≫ (β_ y x).hom ▷ z)
Module: Mathlib.CategoryTheory.Subobject.ArtinianObject

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

Tactic:
ObjectProperty.is_iff,

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
h : ∀ (f : ℕ → Subobject X), ¬StrictAnti f
⊢ isArtinianObject.Is X

Tactic:
ObjectProperty.is_iff,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X : C
h : ∀ (f : ℕ → Subobject X), ¬StrictAnti f
⊢ isArtinianObject X
Module: Mathlib.CategoryTheory.Subobject.ArtinianObject

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
X : C
h : ∀ (F : ℕ ⥤ (MonoOver X)ᵒᵖ), IsFiltered.IsEventuallyConstant F
F : ℕ →o (Subobject X)ᵒᵈ
n : ℕ
hn : (⋯.functor ⋙ (orderDualEquivalence (Subobject X)).functor ⋙ Subobject.representative.op).IsEventuallyConstantFrom n
⊢ ∃ n, ∀ (m : ℕ), n ≤ m → F n = F m

Tactic:
refine ⟨n, fun m hm ↦ Eq.symm ?_⟩

Goal state after:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
X : C
h : ∀ (F : ℕ ⥤ (MonoOver X)ᵒᵖ), IsFiltered.IsEventuallyConstant F
F : ℕ →o (Subobject X)ᵒᵈ
n : ℕ
hn : (⋯.functor ⋙ (orderDualEquivalence (Subobject X)).functor ⋙ Subobject.representative.op).IsEventuallyConstantFrom n
m : ℕ
hm : n ≤ m
⊢ F m = F n
Module: Mathlib.CategoryTheory.MorphismProperty.LocalEpi

Goal state before:
pp: case refine_1
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝¹ : G.Faithful
inst✝ : G.Full
X Y : C
f : X ⟶ Y
h : localEpi (fun x ↦ x ∈ Set.range G.obj) (G.map (F.map f))
Z : D
u v : F.obj Y ⟶ Z
huv : F.map f ≫ u = F.map f ≫ v
⊢ u = v

Tactic:
refine G.map_injective ?_
    apply h ⟨Z, rfl⟩
    simp [← Functor.map_comp, huv]

Goal state after:
Module: Mathlib.CategoryTheory.Subobject.NoetherianObject

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

Tactic:
ObjectProperty.is_iff,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X : C
⊢ isNoetherianObject X ↔ ∀ (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
h : ∀ (f : ℕ → Subobject X), ¬StrictMono f
⊢ isNoetherianObject.Is X

Tactic:
ObjectProperty.is_iff,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X : C
h : ∀ (f : ℕ → Subobject X), ¬StrictMono f
⊢ isNoetherianObject X
Module: Mathlib.CategoryTheory.Preadditive.Comma

Goal state before:
pp: A : Type u₁
inst✝⁷ : Category.{v₁, u₁} A
inst✝⁶ : Preadditive A
B : Type u₂
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Preadditive B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
inst✝² : Preadditive T
L : A ⥤ T
inst✝¹ : L.Additive
R : B ⥤ T
inst✝ : R.Additive
u v : Comma L R
⊢ ∀ (x : u ⟶ v), 0 • x = 0

Tactic:
by simp_rw [HSMul.hSMul, SMul.smul]; cat_disch

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

Goal state before:
pp: I : Type w₁
C : I → Type u₁
inst✝⁶ : (i : I) → Category.{v₁, u₁} (C i)
inst✝⁵ : (i : I) → MonoidalCategory (C i)
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
inst✝³ : MonoidalCategory D
F G : D ⥤ ((i : I) → C i)
inst✝² : F.LaxMonoidal
inst✝¹ : G.LaxMonoidal
τ : (i : I) → F ⋙ eval C i ⟶ G ⋙ eval C i
inst✝ : ∀ (i : I), NatTrans.IsMonoidal (τ i)
X Y : D
i : I
⊢ (Functor.LaxMonoidal.μ F X Y ≫ (NatTrans.pi' τ).app (X ⊗ Y)) i =
    (((NatTrans.pi' τ).app X ⊗ₘ (NatTrans.pi' τ).app Y) ≫ Functor.LaxMonoidal.μ G X Y) i

Tactic:
simpa using NatTrans.IsMonoidal.tensor _ _ (τ := τ i)

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

Goal state before:
pp: A : Type u₁
inst✝⁷ : Category.{v₁, u₁} A
inst✝⁶ : Preadditive A
B : Type u₂
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Preadditive B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
inst✝² : Preadditive T
L : A ⥤ T
inst✝¹ : L.Additive
R : B ⥤ T
inst✝ : R.Additive
u v : Comma L R
⊢ ∀ (a : u ⟶ v), 0 • a = 0

Tactic:
by simp_rw [HSMul.hSMul, SMul.smul]; cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset

Goal state before:
pp: κ : Cardinal.{u}
inst✝² : Fact κ.IsRegular
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCardinalFiltered J κ
F : J ⥤ PartOrdEmb
c : Cocone (F ⋙ forget PartOrdEmb)
hc : IsColimit c
hF : ∀ (j : J), IsCardinalFiltered (↑(F.obj j)) κ
this : IsFiltered J
⊢ IsCardinalFiltered (CoconePt hc) κ

Tactic:
refine isCardinalFiltered_preorder _ _ (fun K f hK ↦ ?_)

Goal state after:
κ : Cardinal.{u}
inst✝² : Fact κ.IsRegular
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCardinalFiltered J κ
F : J ⥤ PartOrdEmb
c : Cocone (F ⋙ forget PartOrdEmb)
hc : IsColimit c
hF : ∀ (j : J), IsCardinalFiltered (↑(F.obj j)) κ
this : IsFiltered J
K : Type u
f : K → CoconePt hc
hK : Cardinal.mk K < κ
⊢ ∃ j, ∀ (k : K), f k ≤ j
Module: Mathlib.CategoryTheory.Preadditive.Mat

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Preadditive C
D : Type u₁
inst✝² : Category.{v₁, u₁} D
inst✝¹ : Preadditive D
F : Mat_ C ⥤ D
inst✝ : F.Additive
M : Mat_ C
i : M.ι
⊢ (F.map (biproduct.lift fun i j x ↦ if h : j = i then eqToHom ⋯ else 0) ≫
        biproduct.lift (F.mapBicone (biproduct.bicone fun i ↦ (embedding C).obj (M.X i))).π) ≫
      biproduct.π (fun i ↦ F.obj ((embedding C).obj (M.X i))) i =
    F.map
      ((biproduct.lift fun i j x ↦ if h : j = i then eqToHom ⋯ else 0) ≫
        biproduct.π (fun i ↦ (embedding C).obj (M.X i)) i)

Tactic:
rw [biproduct.lift_π, Category.assoc]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Preadditive C
D : Type u₁
inst✝² : Category.{v₁, u₁} D
inst✝¹ : Preadditive D
F : Mat_ C ⥤ D
inst✝ : F.Additive
M : Mat_ C
i : M.ι
⊢ F.map (biproduct.lift fun i j x ↦ if h : j = i then eqToHom ⋯ else 0) ≫
      biproduct.lift (F.mapBicone (biproduct.bicone fun i ↦ (embedding C).obj (M.X i))).π ≫
        biproduct.π (fun i ↦ F.obj ((embedding C).obj (M.X i))) i =
    F.map fun j x ↦ if h : j = i then eqToHom ⋯ else 0
Module: Mathlib.CategoryTheory.Preadditive.Mat

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
R : Type u
inst✝ : Semiring R
W✝ X✝ Y✝ Z✝ : Mat R
f✝ : Matrix W✝.obj X✝.obj R
g✝ : Matrix X✝.obj Y✝.obj R
h✝ : Matrix Y✝.obj Z✝.obj R
⊢ ((have this :=
        (have this := f✝;
          this) *
          have this := g✝;
          this;
      this) *
      have this := h✝;
      this) =
    (have this := f✝;
      this) *
      have this :=
        (have this := g✝;
          this) *
          have this := h✝;
          this;
      this

Tactic:
simp [Matrix.mul_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection

Goal state before:
pp: case refine_1.h₀
C : Type u
inst✝⁴ : Category.{v, u} C
W : MorphismProperty C
Z : C
inst✝³ : HasCoproduct D₁.obj₁
inst✝² : HasCoproduct D₁.obj₂
inst✝¹ : HasPushouts C
inst✝ : HasMulticoequalizer (D₂.multispanIndex W Z)
T : C
hT : W.isLocal T
φ₁ φ₂ : succ W Z ⟶ T
h : toStep W Z ≫ fromStep W Z ≫ φ₁ = toStep W Z ≫ fromStep W Z ≫ φ₂
d : D₁ W Z
⊢ Sigma.ι D₁.obj₂ d ≫ pushout.inl (D₁.t W Z) (D₁.l W Z) ≫ Multicoequalizer.π (D₂.multispanIndex W Z) PUnit.unit ≫ φ₁ =
    Sigma.ι D₁.obj₂ d ≫ pushout.inl (D₁.t W Z) (D₁.l W Z) ≫ Multicoequalizer.π (D₂.multispanIndex W Z) PUnit.unit ≫ φ₂

Tactic:
apply (hT d.1.1.hom d.1.2).1
      simp only [← D₁.ι_comp_t_assoc, pushout.condition_assoc, h]

Goal state after: