mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.BinaryBiproducts

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasBinaryBiproducts C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
F G : D ⥤ C
d : D
⊢ ∀ (j : Discrete WalkingPair),
    ((Cone.postcompose (pairComp F G ((evaluation D C).obj d)).symm.hom).obj
              (BinaryBiproduct.bicone (F.obj d) (G.obj d)).toCone).π.app
        j =
      (Iso.refl
            ((Cone.postcompose (pairComp F G ((evaluation D C).obj d)).symm.hom).obj
                (BinaryBiproduct.bicone (F.obj d) (G.obj d)).toCone).pt).hom ≫
        (((evaluation D C).obj d).mapCone (pointwiseBinaryBicone F G).toCone).π.app j

Tactic:
rintro (_ | _ | _)

Goal state after:
case left
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasBinaryBiproducts C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
F G : D ⥤ C
d : D
⊢ ((Cone.postcompose (pairComp F G ((evaluation D C).obj d)).symm.hom).obj
            (BinaryBiproduct.bicone (F.obj d) (G.obj d)).toCone).π.app
      { as := WalkingPair.left } =
    (Iso.refl
          ((Cone.postcompose (pairComp F G ((evaluation D C).obj d)).symm.hom).obj
              (BinaryBiproduct.bicone (F.obj d) (G.obj d)).toCone).pt).hom ≫
      (((evaluation D C).obj d).mapCone (pointwiseBinaryBicone F G).toCone).π.app { as := WalkingPair.left }

case right
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasBinaryBiproducts C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
F G : D ⥤ C
d : D
⊢ ((Cone.postcompose (pairComp F G ((evaluation D C).obj d)).symm.hom).obj
            (BinaryBiproduct.bicone (F.obj d) (G.obj d)).toCone).π.app
      { as := WalkingPair.right } =
    (Iso.refl
          ((Cone.postcompose (pairComp F G ((evaluation D C).obj d)).symm.hom).obj
              (BinaryBiproduct.bicone (F.obj d) (G.obj d)).toCone).pt).hom ≫
      (((evaluation D C).obj d).mapCone (pointwiseBinaryBicone F G).toCone).π.app { as := WalkingPair.right }
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.BinaryBiproducts

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasBinaryBiproducts C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
F G : D ⥤ C
d : D
⊢ ∀ (j : Discrete WalkingPair),
    ((Cocone.precompose (pairComp F G ((evaluation D C).obj d)).symm.inv).obj
                (BinaryBiproduct.bicone (F.obj d) (G.obj d)).toCocone).ι.app
          j ≫
        (Iso.refl
            ((Cocone.precompose (pairComp F G ((evaluation D C).obj d)).symm.inv).obj
                (BinaryBiproduct.bicone (F.obj d) (G.obj d)).toCocone).pt).hom =
      (((evaluation D C).obj d).mapCocone (pointwiseBinaryBicone F G).toCocone).ι.app j

Tactic:
rintro (_ | _ | _)

Goal state after:
case left
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasBinaryBiproducts C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
F G : D ⥤ C
d : D
⊢ ((Cocone.precompose (pairComp F G ((evaluation D C).obj d)).symm.inv).obj
              (BinaryBiproduct.bicone (F.obj d) (G.obj d)).toCocone).ι.app
        { as := WalkingPair.left } ≫
      (Iso.refl
          ((Cocone.precompose (pairComp F G ((evaluation D C).obj d)).symm.inv).obj
              (BinaryBiproduct.bicone (F.obj d) (G.obj d)).toCocone).pt).hom =
    (((evaluation D C).obj d).mapCocone (pointwiseBinaryBicone F G).toCocone).ι.app { as := WalkingPair.left }

case right
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasBinaryBiproducts C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
F G : D ⥤ C
d : D
⊢ ((Cocone.precompose (pairComp F G ((evaluation D C).obj d)).symm.inv).obj
              (BinaryBiproduct.bicone (F.obj d) (G.obj d)).toCocone).ι.app
        { as := WalkingPair.right } ≫
      (Iso.refl
          ((Cocone.precompose (pairComp F G ((evaluation D C).obj d)).symm.inv).obj
              (BinaryBiproduct.bicone (F.obj d) (G.obj d)).toCocone).pt).hom =
    (((evaluation D C).obj d).mapCocone (pointwiseBinaryBicone F G).toCocone).ι.app { as := WalkingPair.right }
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Images

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : C ⥤ Type u
f : F ⟶ G
H : MonoFactorisation f
X Y : C
g : X ⟶ Y
⊢ ((monoFactorisation f).I.map g ≫
      ↾fun x ↦
        match x with
        | ⟨x, hx⟩ => (ConcreteCategory.hom (H.e.app Y)) (Exists.choose hx)) =
    (↾fun x ↦
        match x with
        | ⟨x, hx⟩ => (ConcreteCategory.hom (H.e.app X)) (Exists.choose hx)) ≫
      H.I.map g

Tactic:
ext
      apply injective_of_mono (H.m.app Y)
      simp
      grind

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
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
E' : Type u₄
inst✝ : Category.{v₄, u₄} E'
F F' : C ⋆ D ⥤ E
αₗ : inclLeft C D ⋙ F ⟶ inclLeft C D ⋙ F'
αᵣ : inclRight C D ⋙ F ⟶ inclRight C D ⋙ F'
h :
  whiskerRight (edgeTransform C D) F ≫ (Prod.snd C D).whiskerLeft αᵣ =
    (Prod.fst C D).whiskerLeft αₗ ≫ whiskerRight (edgeTransform C D) F'
x y : D
f : x ⟶ y
⊢ (F.map ((inclRight C D).map f) ≫
      match (inclRight C D).obj y with
      | left x => αₗ.app x
      | right x => αᵣ.app x) =
    (match (inclRight C D).obj x with
      | left x => αₗ.app x
      | right x => αᵣ.app x) ≫
      F'.map ((inclRight C D).map f)

Tactic:
simpa using! αᵣ.naturality f

Goal state after:
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
𝒜 : Type w
f : 𝒜 → FormalCoproduct C
t X✝ X : FormalCoproduct C
i j : X.I
hij : i = j
⊢ X.obj i = X.obj j

Tactic:
rw [hij]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.EquifiberedLimits

Goal state before:
pp: J✝ : Type u_1
K : Type u_2
C : Type u_3
D : Type u_4
ι : Type u_5
inst✝⁵ : Category.{v_1, u_1} J✝
inst✝⁴ : Category.{v_2, u_3} C
inst✝³ : Category.{v_3, u_2} K
inst✝² : Category.{v_4, u_4} D
F : C ⥤ D
inst✝¹ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
J : Type u_1
inst✝ : Category.{v_1, u_1} J
hJ : IsConnected J
G : Over F
x✝ : limitsOfShape (fun f ↦ Equifibered f.hom) J G
i j : C
f : i ⟶ j
c : J ⥤ Over F
α : (const J).obj G ⟶ c
hc : IsLimit { pt := G, π := α }
H : ∀ (j : J), Equifibered ({ diag := c, π := α, isLimit := hc }.diag.obj j).hom
s : PullbackCone (G.hom.app j) (F.map f)
hcᵢ : IsLimit ((Over.forget F ⋙ (evaluation C D).obj i).mapCone { pt := G, π := α }) :=
  isLimitOfPreserves (Over.forget F ⋙ (evaluation C D).obj i) hc
hcⱼ : IsLimit ((Over.forget F ⋙ (evaluation C D).obj j).mapCone { pt := G, π := α }) :=
  isLimitOfPreserves (Over.forget F ⋙ (evaluation C D).obj j) hc
k₁ k₂ : J
fk₁k₂ : k₁ ⟶ k₂
⊢ (((const J).obj s.1).map fk₁k₂ ≫ ⋯.lift (s.fst ≫ (Over.Hom.left (α.app k₂)).app j) s.snd ⋯) ≫
      ({ diag := c, π := α, isLimit := hc }.diag.obj k₂).left.map f =
    (⋯.lift (s.fst ≫ (Over.Hom.left (α.app k₁)).app j) s.snd ⋯ ≫
        (c ⋙ Over.forget F ⋙ (evaluation C D).obj i).map fk₁k₂) ≫
      ({ diag := c, π := α, isLimit := hc }.diag.obj k₂).left.map f

Tactic:
by simp [← NatTrans.naturality, ← NatTrans.comp_app, ← Over.comp_left]

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits

Goal state before:
pp: J : Type u_1
J' : Type u_2
C : Type u_3
D : Type u_4
K : Type u_5
K' : Type u_6
inst✝⁷ : Category.{v_1, u_5} K
inst✝⁶ : Category.{v_2, u_6} K'
inst✝⁵ : Category.{v_3, u_1} J
inst✝⁴ : Category.{v_4, u_2} J'
inst✝³ : Category.{v_5, u_3} C
inst✝² : Category.{v_6, u_4} D
inst✝¹ : HasColimitsOfShape K' C
inst✝ : HasExactColimitsOfShape K' C
⊢ preservesFiniteLimits.colimitsOfShape K' ≤ preservesFiniteLimits

Tactic:
rintro G ⟨h⟩
    have := h.prop_diag_obj
    exact ⟨fun K _ _ ↦ (preservesLimitsOfShape K).prop_of_isColimit h.isColimit inferInstance⟩

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' : IsColimit c'
P : Cᵒᵖ ⥤ Type w
x : P.obj c.pt
⊢ coconePtToShrinkYoneda c hc' ≫ shrinkYonedaEquiv.symm x =
    (coconeCompShrinkYonedaHomEquiv hc').symm (Types.sectionOfCone (P.mapCone c) x)

Tactic:
refine hc'.hom_ext (fun _ ↦ ?_)

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' : IsColimit c'
P : Cᵒᵖ ⥤ Type w
x : P.obj c.pt
x✝ : Jᵒᵖ
⊢ c'.ι.app x✝ ≫ coconePtToShrinkYoneda c hc' ≫ shrinkYonedaEquiv.symm x =
    c'.ι.app x✝ ≫ (coconeCompShrinkYonedaHomEquiv hc').symm (Types.sectionOfCone (P.mapCone c) x)
Module: Mathlib.CategoryTheory.Limits.WeakLimits.WeakPullbacks

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasLimit (pair X Y)
inst✝ : HasWeakLimit (parallelPair (prod.fst ≫ f) (prod.snd ≫ g))
s : PullbackCone f g
⊢ prod.lift (s.π.app WalkingCospan.left) (s.π.app WalkingCospan.right) ≫ prod.fst ≫ f =
    prod.lift (s.π.app WalkingCospan.left) (s.π.app WalkingCospan.right) ≫ prod.snd ≫ g

Tactic:
simp [limit.lift_π_assoc, PullbackCone.condition]

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

Goal state before:
pp: case h_option.refine_2
J : Type w
inst✝⁴ : Fintype J
hJ :
  ∀ {C : J → Type u₁} {D : J → Type u₂} [inst : (j : J) → Category.{v₁, u₁} (C j)]
    [inst_1 : (j : J) → Category.{v₂, u₂} (D j)] (L : (j : J) → C j ⥤ D j) (W : (j : J) → MorphismProperty (C j))
    [∀ (j : J), (W j).ContainsIdentities] [∀ (j : J), (L j).IsLocalization (W j)],
    (Functor.pi L).IsLocalization (MorphismProperty.pi W)
C : Option J → Type u₁
D : Option J → Type u₂
inst✝³ : (j : Option J) → Category.{v₁, u₁} (C j)
inst✝² : (j : Option J) → Category.{v₂, u₂} (D j)
L : (j : Option J) → C j ⥤ D j
W : (j : Option J) → MorphismProperty (C j)
inst✝¹ : ∀ (j : Option J), (W j).ContainsIdentities
inst✝ : ∀ (j : Option J), (L j).IsLocalization (W j)
L₁ : C none × ((i : J) → C (some i)) ⥤ D none × ((i : J) → D (some i)) := ⋯
this : CatCommSq (Pi.optionEquivalence C).symm.functor L₁ (Functor.pi L) (Pi.optionEquivalence D).symm.functor
⊢ ∀ (j : Option J), (W j).IsInvertedBy (L j)

Tactic:
rintro (_ | i) <;> apply Localization.inverts

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

Goal state before:
pp: case symm
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✝ : 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)
a✝ : HomEquiv f✝ g✝
hfg' : projectMapAux f✝¹ f✝ = projectMapAux f✝¹ g✝
⊢ projectMapAux f✝¹ g✝ = projectMapAux f✝¹ f✝

Tactic:
| symm _ _ _ hfg' =>

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

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
inst✝² : MonoidalCategory C
inst✝¹ : MonoidalLeftAction C D
x : C
y z : D
f : y ⟶ z
inst✝ : IsIso f
⊢ x ⊴ₗ inv f ≫ x ⊴ₗ f = 𝟙 (x ⊙ₗ z)

Tactic:
rw [← actionHomRight_comp, IsIso.inv_hom_id, actionHomRight_id]

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
F : C ⥤ (D ⥤ D)ᴹᵒᵖ
inst✝ : F.Monoidal
c : C
d : D
⊢ (F.map (λ_ c).hom).unmop.app d =
    ((Functor.Monoidal.μIso F (𝟙_ C) c).unmop.app d).symm.hom ≫
      ((Functor.Monoidal.εIso F).unmop.app ((F.obj c).unmop.obj d)).symm.hom

Tactic:
by
    have e := (F.map (λ_ c).hom).unmop.app d ≫=
      (congrArg (fun t ↦ t.unmop.app d) <|
        Functor.OplaxMonoidal.left_unitality F c)
    dsimp at e
    simp only [Category.comp_id, ← NatTrans.comp_app_assoc, ← unmop_comp,
      ← F.map_comp_assoc, Iso.hom_inv_id, Functor.map_id, Category.id_comp] at e
    simp [e]

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

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
inst✝² : MonoidalCategory C
inst✝¹ : MonoidalRightAction C D
x : D
y z : C
f : y ⟶ z
inst✝ : IsIso f
⊢ x ⊴ᵣ inv f ≫ x ⊴ᵣ f = 𝟙 (x ⊙ᵣ z)

Tactic:
rw [← actionHomRight_comp, IsIso.inv_hom_id, actionHomRight_id]

Goal state after:
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
⊢ Δ ≫ A ◁ (λ_ A).inv ≫ A ◁ (β_ (𝟙_ C) A).hom ≫ ((A ◁ 𝒮 ▷ 𝟙_ C ≫ A ◁ A ◁ η) ≫ (α_ A A A).inv) ≫ μ ▷ A =
    ε ≫ (λ_ (𝟙_ C)).inv ≫ (η ⊗ₘ η)

Tactic:
slice_lhs 5 7 =>
    rw [associator_inv_naturality_right_assoc, whisker_exchange]

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ Δ ≫ A ◁ (λ_ A).inv ≫ A ◁ (β_ (𝟙_ C) A).hom ≫ A ◁ 𝒮 ▷ 𝟙_ C ≫ (α_ A A (𝟙_ C)).inv ≫ μ ▷ 𝟙_ C ≫ A ◁ η =
    ε ≫ (λ_ (𝟙_ C)).inv ≫ (η ⊗ₘ η)
Module: Mathlib.CategoryTheory.ObjectProperty.Ind

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
P : ObjectProperty C
ι : Type u_1
inst✝³ : Small.{w, u_1} ι
inst✝² : P.IsClosedUnderLimitsOfShape (Discrete ι)
inst✝¹ : HasProductsOfShape ι C
inst✝ : IsIPCOfShape.{w, u_1, v, u} ι C
⊢ P.ind.IsClosedUnderLimitsOfShape (Discrete ι)

Tactic:
by
  refine .mk' fun X ⟨Y, h⟩ ↦ ?_
  let e := equivShrink ι
  have : HasProductsOfShape (Shrink.{w} ι) C :=
    hasLimitsOfShape_of_equivalence (Discrete.equivalence e)
  have : IsIPCOfShape.{w} (Shrink.{w} ι) C := .of_equiv e
  have : P.IsClosedUnderLimitsOfShape (Discrete (Shrink.{w} ι)) :=
    .of_equivalence (Discrete.equivalence e)
  let iso : limit Y ≅ ∏ᶜ fun i ↦ Y.obj ⟨e.symm i⟩ :=
    (Pi.isoLimit _).symm ≪≫ (Pi.reindex e.symm _).symm
  rw [(ind.{w} P).prop_iff_of_iso iso]
  exact ind_pi_of_ind fun i ↦ h _

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.FreydCategory.RightFreyd

Goal state before:
pp: V : Type u_1
inst✝² : Category.{v_1, u_1} V
inst✝¹ : Preadditive V
u v : Arrow V
f : u ⟶ v
inst✝ : IsIso (Hom.right f)
Z✝ : RightFreyd V
g₁ g₂ : v ⟶ Z✝.as
eq : (quotient V).map f ≫ (quotient V).map g₁ = (quotient V).map f ≫ (quotient V).map g₂
h : RightHomotopy (f ≫ g₁) (f ≫ g₂) := homotopyOfEq (f ≫ g₁) (f ≫ g₂) eq
⊢ Hom.right g₁ - Hom.right g₂ = (inv (Hom.right f) ≫ h.hom) ≫ Z✝.as.hom

Tactic:
by simp [dsimp% h.comm]

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)
inst✝ : (i : I) → BraidedCategory (C i)
X Y Z : (i : I) → C i
i : I
⊢ ((α_ X Y Z).inv ≫ (isoMk fun i ↦ β_ ((X ⊗ Y) i) (Z i)).hom ≫ (α_ Z X Y).inv) i =
    (X ◁ (isoMk fun i ↦ β_ (Y i) (Z i)).hom ≫ (α_ X Z Y).inv ≫ (isoMk fun i ↦ β_ (X i) (Z i)).hom ▷ Y) i

Tactic:
apply hexagon_reverse

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
inst✝² : ∀ (i : ι), InvariantBasisNumber (End (s i))
o : HomOrthogonal s
α β : Type
inst✝¹ : Finite α
inst✝ : Finite β
f : α → ι
g : β → ι
i : (⨁ fun a ↦ s (f a)) ≅ ⨁ fun b ↦ s (g b)
c : ι
val✝¹ : Fintype α
val✝ : Fintype β
⊢ o.matrixDecomposition i.inv c * o.matrixDecomposition i.hom c = 1

Tactic:
by
        rw [← o.matrixDecomposition_comp]
        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
inst✝² : ∀ (i : ι), InvariantBasisNumber (End (s i))
o : HomOrthogonal s
α β : Type
inst✝¹ : Finite α
inst✝ : Finite β
f : α → ι
g : β → ι
i : (⨁ fun a ↦ s (f a)) ≅ ⨁ fun b ↦ s (g b)
c : ι
val✝¹ : Fintype α
val✝ : Fintype β
⊢ o.matrixDecomposition i.hom c * o.matrixDecomposition i.inv c = 1

Tactic:
by
        rw [← o.matrixDecomposition_comp]
        simp

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

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

Tactic:
rw [dif_pos rfl]

Goal state after:
case pos
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
i' : Fin n
j' j : (f i').ι
⊢ (if h' : ⋯ ▸ j' = j then eqToHom ⋯ else 0) = if h : i' = i' ∧ j ≍ j' then eqToHom ⋯ else 0
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 : Mat_ C ⥤ D
inst✝ : F.Additive
M N : Mat_ C
f : M ⟶ N
⊢ F.map f ≫ (additiveObjIsoBiproduct F N).hom =
    (additiveObjIsoBiproduct F M).hom ≫ biproduct.matrix fun i j ↦ F.map ((embedding C).map (f i j))

Tactic:
ext i : 1

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
inst✝¹ : HasFiniteBiproducts D
F : Mat_ C ⥤ D
inst✝ : F.Additive
M N : Mat_ C
f : M ⟶ N
i : N.ι
⊢ (F.map f ≫ (additiveObjIsoBiproduct F N).hom) ≫ biproduct.π (fun i ↦ F.obj ((embedding C).obj (N.X i))) i =
    ((additiveObjIsoBiproduct F M).hom ≫ biproduct.matrix fun i j ↦ F.map ((embedding C).map (f i j))) ≫
      biproduct.π (fun i ↦ F.obj ((embedding C).obj (N.X i))) i
Module: Mathlib.CategoryTheory.Presentable.Type

Goal state before:
pp: ⊢ (ObjectProperty.singleton PUnit.{u + 1}).IsStrongGenerator

Tactic:
rw [ObjectProperty.isStrongGenerator_iff]

Goal state after:
⊢ (ObjectProperty.singleton PUnit.{u + 1}).IsSeparating ∧
    ∀ ⦃X Y : Type u⦄ (i : X ⟶ Y) [Mono i],
      (∀ (G : Type u), ObjectProperty.singleton PUnit.{u + 1} G → Function.Surjective fun f ↦ f ≫ i) → IsIso i
Module: Mathlib.CategoryTheory.Presentable.Directed

Goal state before:
pp: J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)
this✝¹ : IsCardinalFiltered (DiagramWithUniqueTerminal J κ) κ
this✝ : IsFiltered J
this : IsFiltered (DiagramWithUniqueTerminal J κ)
j : J
D : DiagramWithUniqueTerminal J κ
f₁ f₂ : j ⟶ D.top
m₀ : J
t : D.top ⟶ m₀
hm₀ : IsEmpty (m₀ ⟶ D.top)
m₁ : J
u : m₀ ⟶ m₁
hu : f₁ ≫ t ≫ u = f₂ ≫ t ≫ u
h₁ : ¬D.P m₁
⊢ ∃ c' t, f₁ ≫ (functor J κ).map t = f₂ ≫ (functor J κ).map t

Tactic:
let φ (x : Subtype D.P) : x.1 ⟶ m₁ := D.isTerminal.lift x.2 ≫ t ≫ u

Goal state after:
J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)
this✝¹ : IsCardinalFiltered (DiagramWithUniqueTerminal J κ) κ
this✝ : IsFiltered J
this : IsFiltered (DiagramWithUniqueTerminal J κ)
j : J
D : DiagramWithUniqueTerminal J κ
f₁ f₂ : j ⟶ D.top
m₀ : J
t : D.top ⟶ m₀
hm₀ : IsEmpty (m₀ ⟶ D.top)
m₁ : J
u : m₀ ⟶ m₁
hu : f₁ ≫ t ≫ u = f₂ ≫ t ≫ u
h₁ : ¬D.P m₁
φ : (x : Subtype D.P) → ↑x ⟶ m₁ := fun x ↦ D.isTerminal.lift ⋯ ≫ t ≫ u
⊢ ∃ c' t, f₁ ≫ (functor J κ).map t = f₂ ≫ (functor J κ).map t
Module: Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology

Goal state before:
pp: case a
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : ∀ (a : α), Finite (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
⊢ (coherentCoverage C).Saturate X (Sieve.generate (Presieve.ofArrows Y π))

Tactic:
apply Coverage.Saturate.of

Goal state after:
case a
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : ∀ (a : α), Finite (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
⊢ Presieve.ofArrows Y π ∈ (coherentCoverage C).coverings X
Module: Mathlib.CategoryTheory.Sites.Coherent.RegularTopology

Goal state before:
pp: case a
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preregular C
X Y Y' : C
π : Y ⟶ X
inst✝¹ : EffectiveEpi π
π' : Y' ⟶ Y
inst✝ : EffectiveEpi π'
⊢ (regularCoverage C).Saturate X (Sieve.generate (Presieve.ofArrows (fun x ↦ Y) fun x ↦ π))

Tactic:
apply Coverage.Saturate.of

Goal state after:
case a
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preregular C
X Y Y' : C
π : Y ⟶ X
inst✝¹ : EffectiveEpi π
π' : Y' ⟶ Y
inst✝ : EffectiveEpi π'
⊢ (Presieve.ofArrows (fun x ↦ Y) fun x ↦ π) ∈ (regularCoverage C).coverings X
Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : FinitaryPreExtensive C
W : C
⊢ IsSheaf (extensiveTopology C) (yoneda.obj W)

Tactic:
extensiveTopology,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : FinitaryPreExtensive C
W : C
⊢ IsSheaf (extensiveCoverage C).toGrothendieck (yoneda.obj W)
Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves

Goal state before:
pp: case refine_1
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : FinitaryPreExtensive C
inst✝ : FinitaryExtensive C
F : Cᵒᵖ ⥤ Type w
hF : IsSheaf (extensiveTopology C) F
n : ℕ
K : Discrete (Fin n) ⥤ Cᵒᵖ
⊢ PreservesLimit K F

Tactic:
extensiveTopology,

Goal state after:
case refine_1
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : FinitaryPreExtensive C
inst✝ : FinitaryExtensive C
F : Cᵒᵖ ⥤ Type w
hF : IsSheaf (extensiveCoverage C).toGrothendieck F
n : ℕ
K : Discrete (Fin n) ⥤ Cᵒᵖ
⊢ PreservesLimit K F
Module: Mathlib.CategoryTheory.Sites.Coherent.Comparison

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : FinitaryPreExtensive C
inst✝ : Preregular C
B₁ B₂ : C
f : B₂ ⟶ B₁
α : Type
x✝ : Finite α
X₁ : α → C
π₁ : (a : α) → X₁ a ⟶ B₁
h : EffectiveEpiFamily X₁ π₁
Y : C
g : Y ⟶ B₂
w✝ : EffectiveEpi g
g' : Y ⟶ ∐ X₁
hg : g' ≫ Sigma.desc π₁ = g ≫ f
⊢ ∃ X₂ π₂, EffectiveEpiFamily X₂ π₂ ∧ ∃ i ι, ∀ (b : α), ι b ≫ π₁ (i b) = π₂ b ≫ f

Tactic:
let X₂ := fun a ↦ pullback g' (Sigma.ι X₁ a)

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : FinitaryPreExtensive C
inst✝ : Preregular C
B₁ B₂ : C
f : B₂ ⟶ B₁
α : Type
x✝ : Finite α
X₁ : α → C
π₁ : (a : α) → X₁ a ⟶ B₁
h : EffectiveEpiFamily X₁ π₁
Y : C
g : Y ⟶ B₂
w✝ : EffectiveEpi g
g' : Y ⟶ ∐ X₁
hg : g' ≫ Sigma.desc π₁ = g ≫ f
X₂ : α → C := fun a ↦ Limits.pullback g' (Sigma.ι X₁ a)
⊢ ∃ X₂ π₂, EffectiveEpiFamily X₂ π₂ ∧ ∃ i ι, ∀ (b : α), ι b ≫ π₁ (i b) = π₂ b ≫ f
Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves

Goal state before:
pp: case refine_2
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : FinitaryPreExtensive C
inst✝ : FinitaryExtensive C
F : Cᵒᵖ ⥤ Type w
hF : PreservesFiniteProducts F
⊢ IsSheaf (extensiveTopology C) F

Tactic:
extensiveTopology,

Goal state after:
case refine_2
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : FinitaryPreExtensive C
inst✝ : FinitaryExtensive C
F : Cᵒᵖ ⥤ Type w
hF : PreservesFiniteProducts F
⊢ IsSheaf (extensiveCoverage C).toGrothendieck F