mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.Sections

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
I : C
inst✝² : Closed I
inst✝¹ : ChosenPullbacksAlong (curryRightUnitorHom I)
inst✝ : BraidedCategory C
A' A : C
⊢ ∀ {Y : Over I} (f : A' ⟶ A) (g : A ⟶ (sections I).obj Y),
    { toFun := sectionsCurry, invFun := sectionsUncurry, left_inv := ⋯, right_inv := ⋯ }.symm (f ≫ g) =
      (toOver I).map f ≫ { toFun := sectionsCurry, invFun := sectionsUncurry, left_inv := ⋯, right_inv := ⋯ }.symm g

Tactic:
X

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
I : C
inst✝² : Closed I
inst✝¹ : ChosenPullbacksAlong (curryRightUnitorHom I)
inst✝ : BraidedCategory C
A' A : C
X : Over I
⊢ ∀ (f : A' ⟶ A) (g : A ⟶ (sections I).obj X),
    { toFun := sectionsCurry, invFun := sectionsUncurry, left_inv := ⋯, right_inv := ⋯ }.symm (f ≫ g) =
      (toOver I).map f ≫ { toFun := sectionsCurry, invFun := sectionsUncurry, left_inv := ⋯, right_inv := ⋯ }.symm g
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.Sections

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
I : C
inst✝² : Closed I
inst✝¹ : ChosenPullbacksAlong (curryRightUnitorHom I)
inst✝ : BraidedCategory C
A : C
X' : Over I
⊢ ∀ {Y' : Over I} (f : (toOver I).obj A ⟶ X') (g : X' ⟶ Y'),
    { toFun := sectionsCurry, invFun := sectionsUncurry, left_inv := ⋯, right_inv := ⋯ } (f ≫ g) =
      { toFun := sectionsCurry, invFun := sectionsUncurry, left_inv := ⋯, right_inv := ⋯ } f ≫ (sections I).map g

Tactic:
X

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
I : C
inst✝² : Closed I
inst✝¹ : ChosenPullbacksAlong (curryRightUnitorHom I)
inst✝ : BraidedCategory C
A : C
X' X : Over I
⊢ ∀ (f : (toOver I).obj A ⟶ X') (g : X' ⟶ X),
    { toFun := sectionsCurry, invFun := sectionsUncurry, left_inv := ⋯, right_inv := ⋯ } (f ≫ g) =
      { toFun := sectionsCurry, invFun := sectionsUncurry, left_inv := ⋯, right_inv := ⋯ } f ≫ (sections I).map g
Module: Mathlib.CategoryTheory.Monad.Monadicity

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
inst✝ : ∀ (A : adj.toMonad.Algebra), HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))
A : adj.toMonad.Algebra
⊢ A.a ≫ ((comparisonAdjunction adj).unit.app A).f = G.map (coequalizer.π (F.map A.a) (adj.counit.app (F.obj A.A)))

Tactic:
comparisonAdjunction_unit_f_aux,

Goal state after:
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
inst✝ : ∀ (A : adj.toMonad.Algebra), HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))
A : adj.toMonad.Algebra
⊢ A.a ≫
      (adj.homEquiv A.A (coequalizer (F.map A.a) (adj.counit.app (F.obj A.A))))
        (coequalizer.π (F.map A.a) (adj.counit.app (F.obj A.A))) =
    G.map (coequalizer.π (F.map A.a) (adj.counit.app (F.obj A.A)))
Module: Mathlib.CategoryTheory.Monoidal.Action.Opposites

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ᵒᵖ
d✝ d'✝ : D
x✝ : d✝ ⟶ d'✝
⊢ (λₗ (op d✝)).symm.unop.hom ≫ x✝ = (op (𝟙_ C) ⊴ₗ x✝.op).unop ≫ (λₗ (op d'✝)).symm.unop.hom

Tactic:
by
    apply Quiver.Hom.op_inj
    simp

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

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'✝ x✝² : C
x✝¹ : c✝ ⟶ c'✝
x✝ : D
⊢ ((x✝¹ ▷ x✝²).op ⊵ₗ op x✝).unop =
    (αₗ (op c✝) (op x✝²) (op x✝)).symm.unop.hom ≫
      (x✝¹.op ⊵ₗ op (unop (op x✝² ⊙ₗ op x✝))).unop ≫ (αₗ (op c'✝) (op x✝²) (op x✝)).symm.unop.inv

Tactic:
by
    apply Quiver.Hom.op_inj
    simp

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

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✝ : MonoidalRightAction Cᵒᵖ Dᵒᵖ
d✝ d'✝ : D
x✝ : d✝ ⟶ d'✝
⊢ (ρᵣ (op d✝)).symm.unop.hom ≫ x✝ = (x✝.op ⊵ᵣ op (𝟙_ C)).unop ≫ (ρᵣ (op d'✝)).symm.unop.hom

Tactic:
by
    apply Quiver.Hom.op_inj
    simp

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

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✝ : MonoidalRightAction Cᵒᵖ Dᵒᵖ
x✝⁴ x✝³ x✝² : C
x✝¹ : x✝³ ⟶ x✝²
x✝ : D
⊢ (op x✝ ⊴ᵣ (x✝⁴ ◁ x✝¹).op).unop =
    (αᵣ (op x✝) (op x✝⁴) (op x✝³)).symm.unop.hom ≫
      (op (unop (op x✝ ⊙ᵣ op x✝⁴)) ⊴ᵣ x✝¹.op).unop ≫ (αᵣ (op x✝) (op x✝⁴) (op x✝²)).symm.unop.inv

Tactic:
by
    apply Quiver.Hom.op_inj
    simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Normal

Goal state before:
pp: case refine_1
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : CartesianMonoidalCategory C
G H : C
inst✝³ : GrpObj G
inst✝² : GrpObj H
φ : H ⟶ G
inst✝¹ : IsMonHom φ
inst✝ : Mono φ
ψ : G ⊗ H ⟶ H
hψ : ψ ≫ φ = G ◁ φ ≫ conj G
⊢ ∀ (X : C), (monoidHom φ X).range.Normal

Tactic:
X

Goal state after:
case refine_1
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : CartesianMonoidalCategory C
G H : C
inst✝³ : GrpObj G
inst✝² : GrpObj H
φ : H ⟶ G
inst✝¹ : IsMonHom φ
inst✝ : Mono φ
ψ : G ⊗ H ⟶ H
hψ : ψ ≫ φ = G ◁ φ ≫ conj G
X : C
⊢ (monoidHom φ X).range.Normal
Module: Mathlib.CategoryTheory.Monoidal.ExternalProduct.KanExtension

Goal state before:
pp: V : Type u₁
inst✝⁵ : Category.{v₁, u₁} V
inst✝⁴ : MonoidalCategory V
D : Type u₂
D' : Type u₃
E : Type u₄
inst✝³ : Category.{v₂, u₂} D
inst✝² : Category.{v₃, u₃} D'
inst✝¹ : Category.{v₄, u₄} E
H : D ⥤ V
L : D ⥤ D'
H' : D' ⥤ V
α : H ⟶ L ⋙ H'
K : E ⥤ V
d : D'
P : (Functor.LeftExtension.mk H' α).IsPointwiseLeftKanExtensionAt d
e : E
inst✝ : Limits.PreservesColimitsOfShape (CostructuredArrow L d) (tensorRight (K.obj e))
cone : Limits.Cocone (CostructuredArrow.proj (L.prod (𝟭 E)) (d, e) ⋙ H ⊠ K) := ⋯
equiv : CostructuredArrow L d × CostructuredArrow (𝟭 E) e ≌ CostructuredArrow (L.prod (𝟭 E)) (d, e) := ⋯
I : CostructuredArrow L d ⥤ CostructuredArrow L d × CostructuredArrow (𝟭 E) e := ⋯
this : I.Final := ⋯
diag_iso : (CostructuredArrow.proj L d ⋙ H) ⋙ tensorRight (K.obj e) ≅
  I ⋙ equiv.functor ⋙ CostructuredArrow.proj (L.prod (𝟭 E)) (d, e) ⋙ H ⊠ K := ⋯
⊢ Limits.IsColimit ((tensorRight (K.obj e)).mapCocone ((Functor.LeftExtension.mk H' α).coconeAt d))

Tactic:
exact Limits.PreservesColimit.preserves (F := tensorRight <| K.obj e) P |>.some

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

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

Tactic:
have := dcongr_arg (fun x => (normalizeIsoApp' C η' x).hom) (normalizeObj_congr n h)

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{u_2, u_1} D
P : ObjectProperty D
e : C ≌ D
inst✝ : P.IsClosedUnderIsomorphisms
X : D
x✝² : Type w
x✝¹ : SmallCategory x✝²
x✝ : IsFiltered x✝²
⊢ (∃ pres, ∀ (i : x✝²), P.inverseImage e.functor (pres.diag.obj i)) ↔ ∃ pres, ∀ (i : x✝²), P (pres.diag.obj i)

Tactic:
refine ⟨fun ⟨pres, h⟩ ↦ ?_, fun ⟨pres, h⟩ ↦ ?_⟩

Goal state after:
case refine_1
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{u_2, u_1} D
P : ObjectProperty D
e : C ≌ D
inst✝ : P.IsClosedUnderIsomorphisms
X : D
x✝³ : Type w
x✝² : SmallCategory x✝³
x✝¹ : IsFiltered x✝³
x✝ : ∃ pres, ∀ (i : x✝³), P.inverseImage e.functor (pres.diag.obj i)
pres : ColimitPresentation x✝³ (e.inverse.obj X)
h : ∀ (i : x✝³), P.inverseImage e.functor (pres.diag.obj i)
⊢ ∃ pres, ∀ (i : x✝³), P (pres.diag.obj i)

case refine_2
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{u_2, u_1} D
P : ObjectProperty D
e : C ≌ D
inst✝ : P.IsClosedUnderIsomorphisms
X : D
x✝³ : Type w
x✝² : SmallCategory x✝³
x✝¹ : IsFiltered x✝³
x✝ : ∃ pres, ∀ (i : x✝³), P (pres.diag.obj i)
pres : ColimitPresentation x✝³ X
h : ∀ (i : x✝³), P (pres.diag.obj i)
⊢ ∃ pres, ∀ (i : x✝³), P.inverseImage e.functor (pres.diag.obj i)
Module: Mathlib.CategoryTheory.MorphismProperty.Ind

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
H✝ : P ≤ isFinitelyPresentable C
X Y : C
f : X ⟶ Y
inst✝ : IsFinitelyAccessibleCategory (Under X)
H : ∀ {Z : C} (p : X ⟶ Z) (g : Z ⟶ Y), isFinitelyPresentable C p → p ≫ g = f → ∃ W u v, u ≫ v = g ∧ P (p ≫ u)
Z : Under X
g : Z ⟶ CategoryTheory.Under.mk f
hZ : IsFinitelyPresentable Z
⊢ ∃ W u v, u ≫ v = g ∧ P.underObj W

Tactic:
· obtain ⟨W, u, v, huv, hW⟩ := H Z.hom g.right hZ (CategoryTheory.Under.w g)
      exact ⟨CategoryTheory.Under.mk (Z.hom ≫ u), CategoryTheory.Under.homMk u,
          CategoryTheory.Under.homMk v, by ext; simpa, hW⟩

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

Goal state before:
pp: case H
C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
H : P ≤ isFinitelyPresentable C
X Y : C
f : X ⟶ Y
inst✝ : IsFinitelyAccessibleCategory (Under X)
⊢ P.underObj ≤ ObjectProperty.isFinitelyPresentable (Under X)

Tactic:
intro Y hY

Goal state after:
case H
C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
H : P ≤ isFinitelyPresentable C
X Y✝ : C
f : X ⟶ Y✝
inst✝ : IsFinitelyAccessibleCategory (Under X)
Y : Under X
hY : P.underObj Y
⊢ ObjectProperty.isFinitelyPresentable (Under X) Y
Module: Mathlib.CategoryTheory.Subobject.NoetherianObject

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
inst✝ : HasZeroObject C
⊢ isNoetherianObject 0

Tactic:
rw [← isNoetherianObject.is_iff]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
inst✝ : HasZeroObject C
⊢ isNoetherianObject.Is 0
Module: Mathlib.CategoryTheory.Preadditive.Projective.LiftingProperties

Goal state before:
pp: case mp
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
P Z : C
hZ : IsZero Z
a✝ : Projective P
⊢ (MorphismProperty.epimorphisms C).llp 0

Tactic:
X

Goal state after:
case mp
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
P Z : C
hZ : IsZero Z
a✝ : Projective P
X : C
⊢ ∀ ⦃Y : C⦄ (g : X ⟶ Y), MorphismProperty.epimorphisms C g → HasLiftingProperty 0 g
Module: Mathlib.CategoryTheory.Preadditive.Projective.LiftingProperties

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
P Z : C
i : Z ⟶ P
hZ : IsZero Z
⊢ Projective P ↔ (MorphismProperty.epimorphisms C).llp i

Tactic:
by
  obtain rfl := hZ.eq_of_src i 0
  constructor
  · intro _ X Y p (_ : Epi p)
    exact Projective.hasLiftingProperty_of_isZero 0 p hZ
  · intro h
    constructor
    intro X Y f p hp
    have := h _ hp
    have sq : CommSq 0 (0 : Z ⟶ P) p f := ⟨by simp⟩
    exact ⟨sq.lift, by simp⟩

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

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
inst✝² : HasKernels C
X Y : C
inst✝¹ : Simple X
inst✝ : Simple Y
f : X ⟶ Y
I : IsIso f
h : f = 0
⊢ 𝟙 X = 0

Tactic:
simp only [← IsIso.hom_inv_id f, h, zero_comp]

Goal state after:
Module: Mathlib.Order.Category.PartOrdEmb

Goal state before:
pp: J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ PartOrdEmb
c : Cocone (F ⋙ forget PartOrdEmb)
hc : IsColimit c
x : CoconePt hc
⊢ ∃ j x' y', ∃ (_ : (ConcreteCategory.hom (c.ι.app j)) x' = x) (_ : (ConcreteCategory.hom (c.ι.app j)) y' = x), x' ≤ y'

Tactic:
obtain ⟨j, x', hx⟩ := Types.jointly_surjective_of_isColimit hc x

Goal state after:
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ PartOrdEmb
c : Cocone (F ⋙ forget PartOrdEmb)
hc : IsColimit c
x : CoconePt hc
j : J
x' : (F ⋙ forget PartOrdEmb).obj j
hx : (ConcreteCategory.hom (c.ι.app j)) x' = x
⊢ ∃ j x' y', ∃ (_ : (ConcreteCategory.hom (c.ι.app j)) x' = x) (_ : (ConcreteCategory.hom (c.ι.app j)) y' = x), x' ≤ y'
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').ι
b : Fin n
⊢ b ∈ Finset.univ →
    b ≠ i →
      (∑ j_1,
          (if h : i = b then if h' : h ▸ j = j_1 then eqToHom ⋯ else 0 else 0) ≫
            if h : i' = b then if h' : h ▸ j' = j_1 then eqToHom ⋯ else 0 else 0) =
        0

Tactic:
_

Goal state after:
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').ι
b : Fin n
a✝ : b ∈ Finset.univ
⊢ b ≠ i →
    (∑ j_1,
        (if h : i = b then if h' : h ▸ j = j_1 then eqToHom ⋯ else 0 else 0) ≫
          if h : i' = b then if h' : h ▸ j' = j_1 then eqToHom ⋯ else 0 else 0) =
      0
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').ι
b : Fin n
a✝ : b ∈ Finset.univ
hb : b ≠ i
x : (f b).ι
⊢ x ∈ Finset.univ →
    ((if h : i = b then if h' : h ▸ j = x then eqToHom ⋯ else 0 else 0) ≫
        if h : i' = b then if h' : h ▸ j' = x then eqToHom ⋯ else 0 else 0) =
      0

Tactic:
_

Goal state after:
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').ι
b : Fin n
a✝¹ : b ∈ Finset.univ
hb : b ≠ i
x : (f b).ι
a✝ : x ∈ Finset.univ
⊢ ((if h : i = b then if h' : h ▸ j = x then eqToHom ⋯ else 0 else 0) ≫
      if h : i' = b then if h' : h ▸ j' = x then eqToHom ⋯ else 0 else 0) =
    0
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

Goal state after:
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').ι
hi : 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
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').ι
b : (f i).ι
⊢ b ∈ Finset.univ →
    b ≠ j →
      ((if h : i = i then if h' : h ▸ j = b then eqToHom ⋯ else 0 else 0) ≫
          if h : i' = i then if h' : h ▸ j' = b then eqToHom ⋯ else 0 else 0) =
        0

Tactic:
_

Goal state after:
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').ι
b : (f i).ι
a✝ : b ∈ Finset.univ
⊢ b ≠ j →
    ((if h : i = i then if h' : h ▸ j = b then eqToHom ⋯ else 0 else 0) ≫
        if h : i' = i then if h' : h ▸ j' = b then eqToHom ⋯ else 0 else 0) =
      0
Module: Mathlib.CategoryTheory.Preadditive.Mat

Goal state before:
pp: case h₀
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
M : Mat_ C
i j b : M.ι
⊢ b ∈ Finset.univ →
    b ≠ i → ((fun j x ↦ if h : j = b then eqToHom ⋯ else 0) ≫ fun x k ↦ if h : b = k then eqToHom ⋯ else 0) i j = 0

Tactic:
_

Goal state after:
case h₀
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
M : Mat_ C
i j b : M.ι
a✝ : b ∈ Finset.univ
⊢ b ≠ i → ((fun j x ↦ if h : j = b then eqToHom ⋯ else 0) ≫ fun x k ↦ if h : b = k then eqToHom ⋯ else 0) i j = 0
Module: Mathlib.Order.Category.PartOrdEmb

Goal state before:
pp: J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ PartOrdEmb
c : Cocone (F ⋙ forget PartOrdEmb)
hc : IsColimit c
s : Cocone F
j : J
x' y' : (F ⋙ forget PartOrdEmb).obj j
hx :
  (ConcreteCategory.hom (c.ι.app j ≫ hc.desc ((forget PartOrdEmb).mapCocone s))) x' =
    (ConcreteCategory.hom (((forget PartOrdEmb).mapCocone s).ι.app j)) x'
hy :
  (ConcreteCategory.hom (c.ι.app j ≫ hc.desc ((forget PartOrdEmb).mapCocone s))) y' =
    (ConcreteCategory.hom (((forget PartOrdEmb).mapCocone s).ι.app j)) y'
⊢ { toFun := ⇑(ConcreteCategory.hom (hc.desc ((forget PartOrdEmb).mapCocone s))), inj' := ⋯ }
        ((ConcreteCategory.hom (c.ι.app j)) x') ≤
      { toFun := ⇑(ConcreteCategory.hom (hc.desc ((forget PartOrdEmb).mapCocone s))), inj' := ⋯ }
        ((ConcreteCategory.hom (c.ι.app j)) y') ↔
    (ConcreteCategory.hom (c.ι.app j)) x' ≤ (ConcreteCategory.hom (c.ι.app j)) y'

Tactic:
simp only [Functor.mapCocone_pt, Functor.comp_obj, Functor.const_obj_obj,
      CategoryTheory.comp_apply, Functor.mapCocone_ι_app, ConcreteCategory.hom_ofHom,
      TypeCat.Fun.coe_mk, Function.Embedding.coeFn_mk] at hx hy ⊢

Goal state after:
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ PartOrdEmb
c : Cocone (F ⋙ forget PartOrdEmb)
hc : IsColimit c
s : Cocone F
j : J
x' y' : (F ⋙ forget PartOrdEmb).obj j
hx :
  (ConcreteCategory.hom (hc.desc ((forget PartOrdEmb).mapCocone s))) ((ConcreteCategory.hom (c.ι.app j)) x') =
    (ConcreteCategory.hom (s.ι.app j)) x'
hy :
  (ConcreteCategory.hom (hc.desc ((forget PartOrdEmb).mapCocone s))) ((ConcreteCategory.hom (c.ι.app j)) y') =
    (ConcreteCategory.hom (s.ι.app j)) y'
⊢ (ConcreteCategory.hom (hc.desc ((forget PartOrdEmb).mapCocone s))) ((ConcreteCategory.hom (c.ι.app j)) x') ≤
      (ConcreteCategory.hom (hc.desc ((forget PartOrdEmb).mapCocone s))) ((ConcreteCategory.hom (c.ι.app j)) y') ↔
    (ConcreteCategory.hom (c.ι.app j)) x' ≤ (ConcreteCategory.hom (c.ι.app j)) y'
Module: Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset

Goal state before:
pp: κ : Cardinal.{u}
inst✝¹ : Fact κ.IsRegular
J : CardinalDirectedPoset κ
κ' : Cardinal.{u}
inst✝ : Fact κ'.IsRegular
S : Subtype (J.PropSetWithTop κ')
x✝ : ↑↑S
⊢ x✝ ≤ ⟨⊤, ⋯⟩

Tactic:
rw [Subtype.mk_le_mk]; exact le_top

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

Goal state before:
pp: κ : Cardinal.{u}
inst✝ : Fact κ.IsRegular
X K : Type u
f : K → SetCardinalLT κ X
hK : Cardinal.mk K < κ
⊢ HasCardinalLT K κ

Tactic:
rwa [hasCardinalLT_iff_cardinal_mk_lt]

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

Goal state before:
pp: X : Type u
κ : Cardinal.{u}
inst✝ : Fact κ.IsRegular
ι : Type u
A : ι → HasCardinalLT.Set X κ
hι : Cardinal.mk ι < κ
⊢ HasCardinalLT ι κ

Tactic:
rwa [hasCardinalLT_iff_cardinal_mk_lt]

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

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
P : ProfunctorCore.{w, v₁, v₂, u₁, u₂} C D
X X' X'' : C
Y : D
f : X ⟶ X'
f' : X' ⟶ X''
⊢ P.map (f ≫ f') (𝟙 Y) = P.map f (𝟙 Y) ≫ P.map f' (𝟙 Y)

Tactic:
nth_rw 1 [← Category.id_comp (𝟙 Y)]

Goal state after:
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
P : ProfunctorCore.{w, v₁, v₂, u₁, u₂} C D
X X' X'' : C
Y : D
f : X ⟶ X'
f' : X' ⟶ X''
⊢ P.map (f ≫ f') (𝟙 Y ≫ 𝟙 Y) = P.map f (𝟙 Y) ≫ P.map f' (𝟙 Y)
Module: Mathlib.CategoryTheory.Presentable.Type

Goal state before:
pp: x✝¹ x✝ : Type u
i : x✝¹ ⟶ x✝
hi₁ : Function.Injective ⇑(hom i)
hi₂ : ∀ (G : Type u), ObjectProperty.singleton PUnit.{u + 1} G → Function.Surjective fun f ↦ f ≫ i
⊢ IsIso i

Tactic:
rw [isIso_iff_bijective]

Goal state after:
x✝¹ x✝ : Type u
i : x✝¹ ⟶ x✝
hi₁ : Function.Injective ⇑(hom i)
hi₂ : ∀ (G : Type u), ObjectProperty.singleton PUnit.{u + 1} G → Function.Surjective fun f ↦ f ≫ i
⊢ Function.Bijective ⇑(hom i)
Module: Mathlib.CategoryTheory.Sites.Coherent.CoherentSheaves

Goal state before:
pp: case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Precoherent C
P : Cᵒᵖ ⥤ Type w
hP : Presieve.IsSheaf (coherentTopology C) P
B : C
α : Type
⊢ ∀ [Finite α] (X : α → C) (π : (a : α) → X a ⟶ B),
    EffectiveEpiFamily X π → Presieve.IsSheafFor P (Presieve.ofArrows X π)

Tactic:
_

Goal state after:
case mp
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Precoherent C
P : Cᵒᵖ ⥤ Type w
hP : Presieve.IsSheaf (coherentTopology C) P
B : C
α : Type
inst✝ : Finite α
⊢ ∀ (X : α → C) (π : (a : α) → X a ⟶ B), EffectiveEpiFamily X π → Presieve.IsSheafFor P (Presieve.ofArrows X π)
Module: Mathlib.CategoryTheory.Sites.Coherent.CoherentSheaves

Goal state before:
pp: case mp
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Precoherent C
P : Cᵒᵖ ⥤ Type w
hP : Presieve.IsSheaf (coherentTopology C) P
B : C
α : Type
inst✝ : Finite α
⊢ ∀ (X : α → C) (π : (a : α) → X a ⟶ B), EffectiveEpiFamily X π → Presieve.IsSheafFor P (Presieve.ofArrows X π)

Tactic:
X

Goal state after:
case mp
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Precoherent C
P : Cᵒᵖ ⥤ Type w
hP : Presieve.IsSheaf (coherentTopology C) P
B : C
α : Type
inst✝ : Finite α
X : α → C
⊢ ∀ (π : (a : α) → X a ⟶ B), EffectiveEpiFamily X π → Presieve.IsSheafFor P (Presieve.ofArrows X π)
Module: Mathlib.CategoryTheory.Sites.Coherent.CoherentSheaves

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Precoherent C
W X : C
α : Type
⊢ ∀ [Finite α] (X_1 : α → C) (π : (a : α) → X_1 a ⟶ X),
    EffectiveEpiFamily X_1 π → Presieve.IsSheafFor (yoneda.obj W) (Presieve.ofArrows X_1 π)

Tactic:
_

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Precoherent C
W X : C
α : Type
inst✝ : Finite α
⊢ ∀ (X_1 : α → C) (π : (a : α) → X_1 a ⟶ X),
    EffectiveEpiFamily X_1 π → Presieve.IsSheafFor (yoneda.obj W) (Presieve.ofArrows X_1 π)
Module: Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology

Goal state before:
pp: case mp.top
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Precoherent C
X : C
S : Sieve X
Y : C
⊢ ∃ α, ∃ (_ : Finite α), ∃ Y_1 π, EffectiveEpiFamily Y_1 π ∧ ∀ (a : α), ⊤.arrows (π a)

Tactic:
| top Y =>

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : FinitaryPreExtensive C
X : C
w✝³ : Type
w✝² : Finite w✝³
w✝¹ : w✝³ → C
w✝ : (a : w✝³) → w✝¹ a ⟶ X
inst✝ : (ofArrows w✝¹ w✝).Extensive
hc : IsColimit (Cofan.mk X w✝)
Y✝ : C
⊢ ∀ {Z : C} {f : Y✝ ⟶ X}, ofArrows w✝¹ w✝ f → ∀ {g : Z ⟶ X}, ofArrows w✝¹ w✝ g → HasPullback f g

Tactic:
_

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : FinitaryPreExtensive C
X : C
w✝³ : Type
w✝² : Finite w✝³
w✝¹ : w✝³ → C
w✝ : (a : w✝³) → w✝¹ a ⟶ X
inst✝ : (ofArrows w✝¹ w✝).Extensive
hc : IsColimit (Cofan.mk X w✝)
Y✝ Z✝ : C
⊢ ∀ {f : Y✝ ⟶ X}, ofArrows w✝¹ w✝ f → ∀ {g : Z✝ ⟶ X}, ofArrows w✝¹ w✝ g → HasPullback f g