mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: case mp
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c d : C
f : c ⟶ d
⊢ Groupoid.inv f ∈ S.arrows d c → f ∈ S.arrows c d

Tactic:
intro h
    simpa only [inv_eq_inv, IsIso.inv_inv] using S.inv h

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Chosen.End

Goal state before:
pp: J✝ : Type u_1
C✝ : Type u_2
inst✝⁵ : Category.{v_1, u_2} C✝
inst✝⁴ : Category.{v_2, u_1} J✝
F✝ : J✝ᵒᵖ ⥤ J✝ ⥤ C✝
inst✝³ : ChosenCoendsOfShape J✝ C✝
X✝ : C✝
f✝¹ : (j : J✝) → (F✝.obj (op j)).obj j ⟶ X✝
hf✝ : ∀ ⦃i j : J✝⦄ (g : i ⟶ j), (F✝.map g.op).app i ≫ f✝¹ i = (F✝.obj (op j)).map g ≫ f✝¹ j
J : Type u_3
C : Type u_4
inst✝² : Category.{v_3, u_4} C
inst✝¹ : Category.{v_4, u_3} J
F : Jᵒᵖ ⥤ J ⥤ C
inst✝ : ChosenEndsOfShape J C
X : C
f✝ : (j : J) → X ⟶ (F.obj (op j)).obj j
hf : ∀ ⦃i j : J⦄ (g : i ⟶ j), f✝ i ≫ (F.obj (op i)).map g = f✝ j ≫ (F.map g.op).app j
G : Jᵒᵖ ⥤ J ⥤ C
f : F ⟶ G
j j' : J
φ : j ⟶ j'
e : (F.obj (op j)).map φ ≫ (f.app (op j)).app j' = (f.app (op j)).app j ≫ (G.obj (op j)).map φ
⊢ π F j ≫ (f.app (op j)).app j ≫ (G.obj (op j)).map φ = π F j' ≫ (f.app (op j')).app j' ≫ (G.map φ.op).app j'

Tactic:
rw [← e, reassoc_of% chosenEnd.condition F φ]

Goal state after:
J✝ : Type u_1
C✝ : Type u_2
inst✝⁵ : Category.{v_1, u_2} C✝
inst✝⁴ : Category.{v_2, u_1} J✝
F✝ : J✝ᵒᵖ ⥤ J✝ ⥤ C✝
inst✝³ : ChosenCoendsOfShape J✝ C✝
X✝ : C✝
f✝¹ : (j : J✝) → (F✝.obj (op j)).obj j ⟶ X✝
hf✝ : ∀ ⦃i j : J✝⦄ (g : i ⟶ j), (F✝.map g.op).app i ≫ f✝¹ i = (F✝.obj (op j)).map g ≫ f✝¹ j
J : Type u_3
C : Type u_4
inst✝² : Category.{v_3, u_4} C
inst✝¹ : Category.{v_4, u_3} J
F : Jᵒᵖ ⥤ J ⥤ C
inst✝ : ChosenEndsOfShape J C
X : C
f✝ : (j : J) → X ⟶ (F.obj (op j)).obj j
hf : ∀ ⦃i j : J⦄ (g : i ⟶ j), f✝ i ≫ (F.obj (op i)).map g = f✝ j ≫ (F.map g.op).app j
G : Jᵒᵖ ⥤ J ⥤ C
f : F ⟶ G
j j' : J
φ : j ⟶ j'
e : (F.obj (op j)).map φ ≫ (f.app (op j)).app j' = (f.app (op j)).app j ≫ (G.obj (op j)).map φ
⊢ π F j' ≫ (F.map φ.op).app j' ≫ (f.app (op j)).app j' = π F j' ≫ (f.app (op j')).app j' ≫ (G.map φ.op).app j'
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u₁
inst✝ : Category.{v₁, u₁} A
X Y Z : FormalCoproduct C
f : X ⟶ Z
g : Y ⟶ Z
i : Function.Pullback f.f g.f
⊢ Z.obj (f.f (↑i).1) = Z.obj (g.f (↑i).2)

Tactic:
i.2

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u₁
inst✝ : Category.{v₁, u₁} A
X Y Z : FormalCoproduct C
f : X ⟶ Z
g : Y ⟶ Z
i : Function.Pullback f.f g.f
⊢ Z.obj (g.f (↑i).2) = Z.obj (g.f (↑i).2)
Module: Mathlib.CategoryTheory.Monoidal.Braided.Multifunctor

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : MonoidalCategory C
⊢ (bifunctorComp₁₂ (curriedTensor C) (curriedTensor C)).flip = bifunctorComp₁₂ (curriedTensor C).flip (curriedTensor C)

Tactic:
by
  rfl

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : MonoidalCategory C
⊢ (bifunctorComp₂₃ (curriedTensor C) (curriedTensor C)).flip =
    (bifunctorComp₂₃ (curriedTensor C) (curriedTensor C).flip).flip.flip₁₃

Tactic:
by
  rfl

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : MonoidalCategory C
⊢ bifunctorComp₁₂ (curriedTensor C) (curriedTensor C) =
    (bifunctorComp₂₃ (curriedTensor C).flip (curriedTensor C)).flip.flip₂₃

Tactic:
by
  rfl

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

Goal state before:
pp: case α_inv_hom
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝ : C → D
X Y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f g : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
X✝ Y✝ Z✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ projectMapAux f✝ ((α_inv X✝ Y✝ Z✝).comp (α_hom X✝ Y✝ Z✝)) = projectMapAux f✝ (Hom.id (X✝.tensor (Y✝.tensor Z✝)))

Tactic:
dsimp only [projectMapAux]; rw [Iso.inv_hom_id]

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

Goal state before:
pp: case ρ_inv_hom
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝ : C → D
X Y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f g : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
X✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ projectMapAux f✝ ((ρ_inv X✝).comp (ρ_hom X✝)) = projectMapAux f✝ (Hom.id X✝)

Tactic:
dsimp only [projectMapAux]; rw [Iso.inv_hom_id]

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

Goal state before:
pp: case l_inv_hom
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝ : C → D
X Y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f g : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
X✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ projectMapAux f✝ ((l_inv X✝).comp (l_hom X✝)) = projectMapAux f✝ (Hom.id X✝)

Tactic:
dsimp only [projectMapAux]; rw [Iso.inv_hom_id]

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

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Category.{v_3, u_3} E
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalCategory D
inst✝⁵ : MonoidalCategory E
L : C ⥤ D
W : MorphismProperty C
inst✝⁴ : L.IsLocalization W
inst✝³ : L.Monoidal
F : D ⥤ E
G : C ⥤ E
inst✝² : G.Monoidal
inst✝¹ : W.ContainsIdentities
inst✝ : Lifting L W G F
X Y : C
⊢ μ F (L.obj X) (L.obj Y) =
    ((Lifting.iso L W G F).hom.app X ⊗ₘ (Lifting.iso L W G F).hom.app Y) ≫
      μ G X Y ≫ (Lifting.iso L W G F).inv.app (X ⊗ Y) ≫ F.map (δ L X Y)

Tactic:
by
  simp [Functor.CoreMonoidal.toLaxMonoidal_μ, curriedTensorPreIsoPost_hom_app_app]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Action.End

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : MonoidalLeftAction C D
c₁ c₂ c₃ : C
⊢ Quiver.Hom.mop { app := fun x ↦ (αₗ c₁ c₂ x).inv, naturality := ⋯ } ▷ (curriedActionMop C D).obj c₃ ≫
      Quiver.Hom.mop { app := fun x ↦ (αₗ (c₁ ⊗ c₂) c₃ x).inv, naturality := ⋯ } ≫
        (curriedActionMop C D).map (α_ c₁ c₂ c₃).hom =
    (α_ ((curriedActionMop C D).obj c₁) ((curriedActionMop C D).obj c₂) ((curriedActionMop C D).obj c₃)).hom ≫
      (curriedActionMop C D).obj c₁ ◁ Quiver.Hom.mop { app := fun x ↦ (αₗ c₂ c₃ x).inv, naturality := ⋯ } ≫
        Quiver.Hom.mop { app := fun x ↦ (αₗ c₁ (c₂ ⊗ c₃) x).inv, naturality := ⋯ }

Tactic:
apply (mopEquiv (D ⥤ D)).fullyFaithfulInverse.map_injective

Goal state after:
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : MonoidalLeftAction C D
c₁ c₂ c₃ : C
⊢ (mopEquiv (D ⥤ D)).inverse.map
      (Quiver.Hom.mop { app := fun x ↦ (αₗ c₁ c₂ x).inv, naturality := ⋯ } ▷ (curriedActionMop C D).obj c₃ ≫
        Quiver.Hom.mop { app := fun x ↦ (αₗ (c₁ ⊗ c₂) c₃ x).inv, naturality := ⋯ } ≫
          (curriedActionMop C D).map (α_ c₁ c₂ c₃).hom) =
    (mopEquiv (D ⥤ D)).inverse.map
      ((α_ ((curriedActionMop C D).obj c₁) ((curriedActionMop C D).obj c₂) ((curriedActionMop C D).obj c₃)).hom ≫
        (curriedActionMop C D).obj c₁ ◁ Quiver.Hom.mop { app := fun x ↦ (αₗ c₂ c₃ x).inv, naturality := ⋯ } ≫
          Quiver.Hom.mop { app := fun x ↦ (αₗ c₁ (c₂ ⊗ c₃) x).inv, naturality := ⋯ })
Module: Mathlib.CategoryTheory.Monoidal.Mod

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalLeftAction C D
A : C
inst✝ : MonObj A
M : Mod D A
⊢ (𝟙 M).hom = 𝟙 M.X

Tactic:
by
  rfl

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : CartesianMonoidalCategory C
inst✝³ : CartesianMonoidalCategory D
F : C ⥤ D
inst✝² : MonoidalClosed C
inst✝¹ : MonoidalClosed D
inst✝ : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
A B : C
⊢ F.map ((ihom.coev A).app B) ≫ (expComparison F A).natTrans.app (A ⊗ B) =
    (ihom.coev (F.obj A)).app (F.obj B) ≫ (ihom (F.obj A)).map (inv (prodComparison F A B))

Tactic:
by
  convert! unit_mateEquiv _ _ (prodComparisonNatIso F A).inv B using 3
  apply IsIso.inv_eq_of_hom_inv_id -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11041): was `ext`
  simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Closed.InternalCurrying

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : MonoidalCategory C
x y z : C
inst✝² : Closed x
inst✝¹ : Closed y
inst✝ : Closed (x ⊗ y)
⊢ uncurry (ihomCurry x y z ≫ ihomUncurry x y z) = uncurry (𝟙 ((ihom (x ⊗ y)).obj z))

Tactic:
uncurry_natural_left,

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : MonoidalCategory C
x y z : C
inst✝² : Closed x
inst✝¹ : Closed y
inst✝ : Closed (x ⊗ y)
⊢ (x ⊗ y) ◁ ihomCurry x y z ≫ uncurry (ihomUncurry x y z) = uncurry (𝟙 ((ihom (x ⊗ y)).obj z))
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
⊢ ((reflectorAdjunction i).homEquiv (A ⊗ B) ((reflector i).obj A ⊗ (reflector i).obj B)).symm
      ((β_ A B).hom ≫
        uncurry
          ((reflectorAdjunction i).unit.app A ≫
            curry
              ((β_ B (i.obj ((reflector i).obj A))).hom ≫
                uncurry
                  ((reflectorAdjunction i).unit.app B ≫
                    curry (prodComparisonIso i ((reflector i).obj A) ((reflector i).obj B)).inv)))) =
    prodComparison (reflector i) A B

Tactic:
uncurry_natural_left,

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 ≫
        B ◁ (reflectorAdjunction i).unit.app A ≫
          uncurry
            (curry
              ((β_ B (i.obj ((reflector i).obj A))).hom ≫
                uncurry
                  ((reflectorAdjunction i).unit.app B ≫
                    curry (prodComparisonIso i ((reflector i).obj A) ((reflector i).obj B)).inv)))) =
    prodComparison (reflector i) A B
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
⊢ ((reflectorAdjunction i).homEquiv (A ⊗ B) ((reflector i).obj A ⊗ (reflector i).obj B)).symm
      ((β_ A B).hom ≫
        B ◁ (reflectorAdjunction i).unit.app A ≫
          (β_ B (i.obj ((reflector i).obj A))).hom ≫
            uncurry
              ((reflectorAdjunction i).unit.app B ≫
                curry (prodComparisonIso i ((reflector i).obj A) ((reflector i).obj B)).inv)) =
    prodComparison (reflector i) A B

Tactic:
uncurry_natural_left,

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 ≫
        B ◁ (reflectorAdjunction i).unit.app A ≫
          (β_ B (i.obj ((reflector i).obj A))).hom ≫
            i.obj ((reflector i).obj A) ◁ (reflectorAdjunction i).unit.app B ≫
              uncurry (curry (prodComparisonIso i ((reflector i).obj A) ((reflector i).obj B)).inv)) =
    prodComparison (reflector i) A B
Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed

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
inst✝ : MonoidalClosed V
F G H : C ⥤ V
ℌ : DayConvolutionInternalHom F G H
G' H' : C ⥤ V
f✝ : G ⟶ G'
ℌ' : DayConvolutionInternalHom F G' H'
c c' : C
f : c ⟶ c'
j : (multicospanShapeEnd C).L
⊢ H.map f ≫
      Wedge.IsLimit.lift (ℌ'.isLimitWedge c') (fun j ↦ ℌ.π c' j ≫ (ihom (F.obj j)).map (f✝.app (j ⊗ c'))) ⋯ ≫
        ℌ'.π c' j =
    Wedge.IsLimit.lift (ℌ'.isLimitWedge c) (fun j ↦ ℌ.π c j ≫ (ihom (F.obj j)).map (f✝.app (j ⊗ c))) ⋯ ≫
      ℌ'.π c j ≫ (ihom (F.obj j)).map (G'.map (j ◁ f))

Tactic:
← Wedge.mk_ι
        (F := dayConvolutionInternalHomDiagramFunctor F |>.obj _ |>.obj c')
        (H'.obj c') (ℌ'.π c') (ℌ'.hπ c'),

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
inst✝ : MonoidalClosed V
F G H : C ⥤ V
ℌ : DayConvolutionInternalHom F G H
G' H' : C ⥤ V
f✝ : G ⟶ G'
ℌ' : DayConvolutionInternalHom F G' H'
c c' : C
f : c ⟶ c'
j : (multicospanShapeEnd C).L
⊢ H.map f ≫
      Wedge.IsLimit.lift (ℌ'.isLimitWedge c') (fun j ↦ ℌ.π c' j ≫ (ihom (F.obj j)).map (f✝.app (j ⊗ c'))) ⋯ ≫
        Multifork.ι (Wedge.mk (H'.obj c') (ℌ'.π c') ⋯) j =
    Wedge.IsLimit.lift (ℌ'.isLimitWedge c) (fun j ↦ ℌ.π c j ≫ (ihom (F.obj j)).map (f✝.app (j ⊗ c))) ⋯ ≫
      ℌ'.π c j ≫ (ihom (F.obj j)).map (G'.map (j ◁ f))
Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed

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
inst✝¹ : MonoidalClosed V
F G H : C ⥤ V
inst✝ : DayConvolution F H
ℌ : DayConvolutionInternalHom F G H
x y : C × C
f : x ⟶ y
⊢ (unop (op (F ⊠ H))).map f ≫ MonoidalClosed.uncurry (ℌ.π y.2 y.1) =
    MonoidalClosed.uncurry (ℌ.π x.2 x.1) ≫ (((Functor.whiskeringLeft (C × C) C V).obj (tensor C)).obj G).map f

Tactic:
by
        have := congrArg (fun t ↦ F.obj x.1 ◁ t) <| ℌ.hπ x.2 f.1
        dsimp at this ⊢
        simp only [whiskerLeft_comp] at this
        simp only [Category.assoc, MonoidalClosed.uncurry_eq, Functor.id_obj,
          ← whiskerLeft_comp_assoc, map_comp_π]
        simp only [whiskerLeft_comp, Category.assoc, ihom.ev_naturality,
          Functor.comp_obj, curriedTensor_obj_obj, Functor.id_obj,
          ← whisker_exchange_assoc, tensorHom_def, Functor.map_comp,
          ← ihom.ev_naturality_assoc]
        rw [reassoc_of% this]
        simp

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
o : HomOrthogonal s
α β γ : Type
inst✝² : Finite α
inst✝¹ : Fintype β
inst✝ : Finite γ
f : α → ι
g : β → ι
h : γ → ι
z : (⨁ fun a ↦ s (f a)) ⟶ ⨁ fun b ↦ s (g b)
w : (⨁ fun b ↦ s (g b)) ⟶ ⨁ fun c ↦ s (h c)
c : γ
a : α
j_property✝ : a ∈ f ⁻¹' {h c}
j_property : f a = h c
| eqToHom ⋯ ≫ biproduct.ι (fun a ↦ s (f a)) a ≫ z ≫ (𝟙 (⨁ fun b ↦ s (g b)) ≫ w) ≫ biproduct.π (fun b ↦ s (h b)) c

Tactic:
← biproduct.total

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
o : HomOrthogonal s
α β γ : Type
inst✝² : Finite α
inst✝¹ : Fintype β
inst✝ : Finite γ
f : α → ι
g : β → ι
h : γ → ι
z : (⨁ fun a ↦ s (f a)) ⟶ ⨁ fun b ↦ s (g b)
w : (⨁ fun b ↦ s (g b)) ⟶ ⨁ fun c ↦ s (h c)
c : γ
a : α
j_property✝ : a ∈ f ⁻¹' {h c}
j_property : f a = h c
| eqToHom ⋯ ≫
    biproduct.ι (fun a ↦ s (f a)) a ≫
      z ≫
        ((∑ j, biproduct.π (fun b ↦ s (g b)) j ≫ biproduct.ι (fun b ↦ s (g b)) j) ≫ w) ≫ biproduct.π (fun b ↦ s (h b)) c
Module: Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset

Goal state before:
pp: κ : Cardinal.{u}
inst✝ : Fact κ.IsRegular
X : Type u
hX : Cardinal.mk X = κ
⊢ ∃ Q, ∃ (_ : ObjectProperty.Small.{u, u, u + 1} Q), hasCardinalLTWithTerminal κ ≤ Q.isoClosure

Tactic:
let α : Type u := Σ (S : Set X) (_ : PartialOrder S),
      ULift.{u} (PLift (IsCardinalFiltered S κ))

Goal state after:
κ : Cardinal.{u}
inst✝ : Fact κ.IsRegular
X : Type u
hX : Cardinal.mk X = κ
α : Type u := (S : Set X) × (x : PartialOrder ↑S) × ULift.{u, 0} (PLift (IsCardinalFiltered (↑S) κ))
⊢ ∃ Q, ∃ (_ : ObjectProperty.Small.{u, u, u + 1} Q), hasCardinalLTWithTerminal κ ≤ Q.isoClosure
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
inst✝² : HasFiniteBiproducts D
F : C ⥤ D
inst✝¹ : F.Additive
L : Mat_ C ⥤ D
inst✝ : L.Additive
α : embedding C ⋙ L ≅ F
X✝ Y✝ : Mat_ C
f : X✝ ⟶ Y✝
⊢ L.map f ≫
      (additiveObjIsoBiproduct L Y✝ ≪≫
          (biproduct.mapIso fun i ↦ α.app (Y✝.X i)) ≪≫
            (biproduct.mapIso fun i ↦ (embeddingLiftIso F).symm.app (Y✝.X i)) ≪≫
              (additiveObjIsoBiproduct (lift F) Y✝).symm).hom =
    (additiveObjIsoBiproduct L X✝ ≪≫
          (biproduct.mapIso fun i ↦ α.app (X✝.X i)) ≪≫
            (biproduct.mapIso fun i ↦ (embeddingLiftIso F).symm.app (X✝.X i)) ≪≫
              (additiveObjIsoBiproduct (lift F) X✝).symm).hom ≫
      (lift F).map f

Tactic:
dsimp only [Iso.trans_hom, Iso.symm_hom, biproduct.mapIso_hom]
      simp only [additiveObjIsoBiproduct_naturality_assoc]
      simp only [biproduct.matrix_map_assoc, Category.assoc]
      simp only [additiveObjIsoBiproduct_naturality']
      simp only [biproduct.map_matrix_assoc]
      congr 3
      ext j k
      apply biproduct.hom_ext
      rintro ⟨⟩
      dsimp
      simpa using α.hom.naturality (f j k)

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

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
W : MorphismProperty C
Z : C
inst✝⁶ : HasPushouts C
inst✝⁵ : ∀ (Z : C), HasCoproduct D₁.obj₁
inst✝⁴ : ∀ (Z : C), HasCoproduct D₁.obj₂
inst✝³ : ∀ (Z : C), HasMulticoequalizer (D₂.multispanIndex W Z)
κ : Cardinal.{w}
inst✝² : OrderBot κ.ord.ToType
inst✝¹ : HasIterationOfShape κ.ord.ToType C
inst✝ : Fact κ.IsRegular
X Y : C
f : X ⟶ Y
hf : W f
j : κ.ord.ToType
g₁ g₂ : Y ⟶ (iteration W Z κ).obj j
hg : f ≫ g₁ = f ≫ g₂
⊢ g₁ ≫ (iteration W Z κ).map (homOfLE ⋯) = g₂ ≫ (iteration W Z κ).map (homOfLE ⋯)

Tactic:
by
  simp [iteration_map_succ, reassoc_of% (toSucc_injectivity f hf _ _ hg)]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Coherent.Basic

Goal state before:
pp: case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : FinitaryPreExtensive C
X Y : C
f : Y ⟶ X
S : Presieve X
α : Type
hα : Finite α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
h_iso : IsIso (Sigma.desc π)
Z' : α → C := fun a ↦ pullback f (π a)
π' : (a : α) → Z' a ⟶ Y := fun a ↦ pullback.fst f (π a)
⊢ (Presieve.ofArrows Z' π').FactorsThruAlong S f

Tactic:
intro W g hg
      rcases hg with ⟨a⟩
      refine ⟨Z a, pullback.snd _ _, π a, ?_, by rw [CategoryTheory.Limits.pullback.condition]⟩
      rw [hS]
      exact Presieve.ofArrows.mk a

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveTopology

Goal state before:
pp: case mp.of.refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : FinitaryPreExtensive C
X✝ : C
S✝ : Sieve X✝
X : C
S : Presieve X
α : Type
w✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : S = Presieve.ofArrows Y π
h' : IsIso (Sigma.desc π)
a : α
⊢ (Sieve.generate S).arrows (π a)

Tactic:
· obtain ⟨rfl, _⟩ := h
        exact ⟨Y a, 𝟙 Y a, π a, Presieve.ofArrows.mk a, by simp⟩

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

Goal state before:
pp: case mpr
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝⁷ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w
inst✝⁶ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝⁵ : ConcreteCategory A FA
inst✝⁴ : HasFunctorialSurjectiveInjectiveFactorization A
inst✝³ : J.WEqualsLocallyBijective A
inst✝² : HasSheafify J A
inst✝¹ : J.HasSheafCompose (forget A)
inst✝ : Balanced (Sheaf J A)
F G : Sheaf J A
φ : F ⟶ G
a✝ : Epi φ
data : (locallySurjective J A).MapFactorizationData (locallyInjective J A) φ :=
  (locallySurjective J A).factorizationData (locallyInjective J A) φ
this✝¹ : IsLocallySurjective data.i
this✝ : IsLocallyInjective data.p
this : Epi data.p
⊢ IsLocallySurjective φ

Tactic:
have := mono_of_isLocallyInjective data.p

Goal state after:
case mpr
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝⁷ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w
inst✝⁶ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝⁵ : ConcreteCategory A FA
inst✝⁴ : HasFunctorialSurjectiveInjectiveFactorization A
inst✝³ : J.WEqualsLocallyBijective A
inst✝² : HasSheafify J A
inst✝¹ : J.HasSheafCompose (forget A)
inst✝ : Balanced (Sheaf J A)
F G : Sheaf J A
φ : F ⟶ G
a✝ : Epi φ
data : (locallySurjective J A).MapFactorizationData (locallyInjective J A) φ :=
  (locallySurjective J A).factorizationData (locallyInjective J A) φ
this✝² : IsLocallySurjective data.i
this✝¹ : IsLocallyInjective data.p
this✝ : Epi data.p
this : Mono data.p
⊢ IsLocallySurjective φ
Module: Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Adj Cat
ι : Type u_1
inst✝ : Unique ι
X S : C
f : X ⟶ S
⊢ (F.toDescentDataAsCoalgebra fun x ↦ f).IsEquivalence ↔
    ((F.toDescentDataAsCoalgebra fun x ↦ f) ⋙ (DescentDataAsCoalgebra.coalgebraEquivalence F ι f).functor).IsEquivalence

Tactic:
exact ⟨fun _ ↦ inferInstance, fun _ ↦
    Functor.isEquivalence_of_comp_right _
      ((DescentDataAsCoalgebra.coalgebraEquivalence F ι f).functor)⟩

Goal state after:
Module: Mathlib.CategoryTheory.Sites.SheafHom

Goal state before:
pp: case mpr
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u'
inst✝ : Category.{v', u'} A
F G : Cᵒᵖ ⥤ A
X : C
S : Sieve X
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
hx : x.Compatible
y : (presheafHom F G).obj (op X)
h : ∀ (Y : C) (g : Y ⟶ X) (hg : S.arrows g), y.app (op (Over.mk g)) = (x g hg).app (op (Over.mk (𝟙 Y)))
Y : C
g : Y ⟶ X
hg : S.arrows g
W : Over Y
⊢ (x (W.hom ≫ g) ⋯).app (op (Over.mk (𝟙 W.left))) = (x g hg).app (op W)

Tactic:
have H := hx (𝟙 _) W.hom (S.downward_closed hg W.hom) hg (by simp)

Goal state after:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u'
inst✝ : Category.{v', u'} A
F G : Cᵒᵖ ⥤ A
X : C
S : Sieve X
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
hx : x.Compatible
y : (presheafHom F G).obj (op X)
h : ∀ (Y : C) (g : Y ⟶ X) (hg : S.arrows g), y.app (op (Over.mk g)) = (x g hg).app (op (Over.mk (𝟙 Y)))
Y : C
g : Y ⟶ X
hg : S.arrows g
W : Over Y
H :
  (ConcreteCategory.hom ((presheafHom F G).map (𝟙 W.left).op)) (x (W.hom ≫ g) ⋯) =
    (ConcreteCategory.hom ((presheafHom F G).map W.hom.op)) (x g hg)
⊢ (x (W.hom ≫ g) ⋯).app (op (Over.mk (𝟙 W.left))) = (x g hg).app (op W)
Module: Mathlib.CategoryTheory.Sites.Point.OfIsCofiltered

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : LocallySmall.{w, v, u} C
N : Type u'
inst✝¹ : Category.{v', u'} N
p : N ⥤ C
inst✝ : InitiallySmall N
U : N
X : C
f : p.obj U ⟶ X
Y : C
g : X ⟶ Y
⊢ (hom
        ((p.op.whiskerLeft (shrinkYoneda.{w, v, u}.map g)).app (op U) ≫
          colimit.ι (p.op ⋙ shrinkYoneda.{w, v, u}.obj Y) (op U)))
      (shrinkYonedaObjObjEquiv.symm f) =
    fiberMk (f ≫ g)

Tactic:
by
      simp [fiberMk, shrinkYoneda_map_app_shrinkYonedaObjObjEquiv_symm.{w}]

Goal state after: