mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Monoidal.Limits.HasLimits

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : MonoidalCategory C
J : Type u₁
inst✝² : Category.{v₁, u₁} J
F G : J ⥤ C
inst✝¹ : HasColimit F
inst✝ : HasColimit G
w : F ≅ G
j : J
Q : C
⊢ colimit.ι F j ▷ Q ≫ (HasColimit.isoOfNatIso w).hom ▷ Q = w.hom.app j ▷ Q ≫ colimit.ι G j ▷ Q

Tactic:
by
  simp [← MonoidalCategory.comp_whiskerRight]

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 y : D
f : x ⟶ y
⊢ 𝟙_ C ⊴ₗ f = (λₗ x).hom ≫ f ≫ (λₗ y).inv

Tactic:
rw [← Category.assoc, actionUnitIso_hom_naturality]

Goal state after:
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 y : D
f : x ⟶ y
⊢ 𝟙_ C ⊴ₗ f = (𝟙_ C ⊴ₗ f ≫ (λₗ y).hom) ≫ (λₗ y).inv
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 y : D
f : x ⟶ y
⊢ f ⊵ᵣ 𝟙_ C = (ρᵣ x).hom ≫ f ≫ (ρᵣ y).inv

Tactic:
rw [← Category.assoc, actionUnitIso_hom_naturality]

Goal state after:
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 y : D
f : x ⟶ y
⊢ f ⊵ᵣ 𝟙_ C = (f ⊵ᵣ 𝟙_ C ≫ (ρᵣ y).hom) ≫ (ρᵣ y).inv
Module: Mathlib.CategoryTheory.Monoidal.Braided.Reflection

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 D
inst✝⁴ : SymmetricCategory D
inst✝³ : MonoidalClosed D
R : C ⥤ D
inst✝² : R.Faithful
inst✝¹ : R.Full
L : D ⥤ C
adj : L ⊣ R
c : C
d : D
inst✝ : IsIso (L.map (adj.unit.app ((ihom d).obj (R.obj c)) ⊗ₘ adj.unit.app d))
this : d ◁ adj.unit.app ((ihom d).obj (R.obj c)) ≫ adjRetractionAux adj c d = (ihom.ev d).app (R.obj c)
⊢ adj.unit.app ((ihom d).obj (R.obj c)) ≫ adjRetraction adj c d = 𝟙 ((𝟭 D).obj ((ihom d).obj (R.obj c)))

Tactic:
simp only [id_obj, adjRetraction, ← curry_natural_left, this]
    simp [curry_eq]

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 ◁ φ ≫ conj G) → ∀ (X : C), (monoidHom φ X).range.Normal

Tactic:
intro ⟨ψ, hψ⟩ X
    constructor
    rintro - ⟨x, rfl⟩ z
    exact ⟨lift z x ≫ ψ, by simp [hψ]⟩

Goal state after:
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:
have := congrArg (fun t ↦ F.obj x.1 ◁ t) <| ℌ.hπ x.2 f.1

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
inst✝ : DayConvolution F H
ℌ : DayConvolutionInternalHom F G H
x y : C × C
f : x ⟶ y
this :
  F.obj x.1 ◁ (ℌ.π x.2 x.1 ≫ (ihom (F.obj x.1)).map (G.map (f.1 ▷ x.2))) =
    F.obj x.1 ◁ (ℌ.π x.2 y.1 ≫ (MonoidalClosed.pre (F.map f.1)).app (G.obj (y.1 ⊗ x.2)))
⊢ (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
Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.DayFunctor

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
hasDayConvolution : ∀ (F G : C ⥤ V), (tensor C).HasPointwiseLeftKanExtension (F ⊠ G)
hasDayConvolutionUnit : (Functor.fromPUnit (𝟙_ C)).HasPointwiseLeftKanExtension (Functor.fromPUnit (𝟙_ 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)
inst✝³ :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorLeft v)
inst✝² :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorRight v)
inst✝¹ :
  ∀ (v : V) (d : C × C),
    Limits.PreservesColimitsOfShape (CostructuredArrow ((𝟭 C).prod (Functor.fromPUnit (𝟙_ C))) d) (tensorRight v)
inst✝ :
  ∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((tensor C).prod (𝟭 C)) d) (tensorRight v)
F G H : C ⊛⥤ V
α β : F ⊗ G ⟶ H
h : ∀ (x y : C), (F.η G).app (x, y) ≫ α.natTrans.app (x ⊗ y) = (F.η G).app (x, y) ≫ β.natTrans.app (x ⊗ y)
⊢ α = β

Tactic:
ext : 1
  apply Functor.hom_ext_of_isLeftKanExtension
    (F ⊗ G).functor (η F G) _
  ext ⟨x, y⟩
  exact h x y

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
V : Type u₂
inst✝³ : Category.{v₂, u₂} V
inst✝² : MonoidalCategory C
inst✝¹ : MonoidalCategory V
F G : C ⥤ V
inst✝ : DayConvolution F G
x x' y y' : C
f : x ⟶ x'
g : y ⟶ y'
⊢ (F.map f ⊗ₘ G.map g) ≫ (unit F G).app (x', y') = (unit F G).app (x, y) ≫ (F ⊛ G).map (f ⊗ₘ g)

Tactic:
simpa [tensorHom_def] using (unit F G).naturality (f ×ₘ g)

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ 𝟙 X ⊗≫ (X ◁ η_ X Y ≫ (β_ X (X ⊗ Y)).hom) ⊗≫ ((β_ (Y ⊗ X) X).inv ≫ ε_ X Y ▷ X) ⊗≫ 𝟙 X = 𝟙 X

Tactic:
rw [braiding_naturality_right, ← braiding_inv_naturality_right]

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ 𝟙 X ⊗≫ ((β_ X (𝟙_ C)).hom ≫ η_ X Y ▷ X) ⊗≫ (X ◁ ε_ X Y ≫ (β_ (𝟙_ C) X).inv) ⊗≫ 𝟙 X = 𝟙 X
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: case a.a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
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 : Mon C
M N : Bimod X Y
f : M ⟶ N
| M.actLeft ≫ f.hom

pp: case a.a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
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 : Mon C
M N : Bimod X Y
f : M ⟶ N
| (λ_ N.X).inv

pp: case a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
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 : Mon C
M N : Bimod X Y
f : M ⟶ N
| η ▷ N.X

pp: case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
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 : Mon C
M N : Bimod X Y
f : M ⟶ N
| coequalizer.π (μ ▷ N.X) ((α_ X.X X.X N.X).hom ≫ X.X ◁ N.actLeft)

Tactic:
rw [Hom.left_act_hom]

Goal state after:
case a.a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
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 : Mon C
M N : Bimod X Y
f : M ⟶ N
| X.X ◁ f.hom ≫ N.actLeft

case a.a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
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 : Mon C
M N : Bimod X Y
f : M ⟶ N
| (λ_ N.X).inv

case a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
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 : Mon C
M N : Bimod X Y
f : M ⟶ N
| η ▷ N.X

case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
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 : Mon C
M N : Bimod X Y
f : M ⟶ N
| coequalizer.π (μ ▷ N.X) ((α_ X.X X.X N.X).hom ≫ X.X ◁ N.actLeft)
Module: Mathlib.CategoryTheory.Monoidal.DayConvolution

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
V : Type u₂
inst✝⁵ : Category.{v₂, u₂} V
inst✝⁴ : MonoidalCategory C
inst✝³ : MonoidalCategory V
U : C ⥤ V
inst✝² : DayConvolutionUnit U
F : C ⥤ V
inst✝¹ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (fromPUnit (𝟙_ C)) d) (tensorRight v)
inst✝ : DayConvolution U F
x : C
⊢ (λ_ (F.obj x)).inv ≫
      ((ConcreteCategory.hom
                (𝟙
                  (prod.leftInverseUnitor C ⋙ fromPUnit (𝟙_ V) ⊠ F ⟶
                    prod.leftInverseUnitor C ⋙ (fromPUnit (𝟙_ C)).prod (𝟭 C) ⋙ tensor C ⋙ U ⊛ F)))
              ((prod.leftUnitorEquivalence C).congrLeft.fullyFaithfulFunctor.homEquiv
                (((U ⊠ F).homEquivOfIsLeftKanExtension (extensionUnitLeft U (φ U) F) (tensor C ⋙ U ⊛ F))
                  (((U ⊛ F).homEquivOfIsLeftKanExtension (DayConvolution.unit U F) (U ⊛ F)) (𝟙 (U ⊛ F)))))).app
          x ≫
        (U ⊛ F).map (λ_ x).hom =
    (λ_ (F.obj x)).inv ≫ can ▷ F.obj x ≫ (DayConvolution.unit U F).app (𝟙_ C, x) ≫ (U ⊛ F).map (λ_ x).hom

Tactic:
dsimp [prod.leftUnitorEquivalence, Equivalence.congrLeft, Equivalence.fullyFaithfulFunctor,
    Functor.FullyFaithful.homEquiv]

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
U : C ⥤ V
inst✝² : DayConvolutionUnit U
F : C ⥤ V
inst✝¹ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (fromPUnit (𝟙_ C)) d) (tensorRight v)
inst✝ : DayConvolution U F
x : C
⊢ (λ_ (F.obj x)).inv ≫
      ((ConcreteCategory.hom
                (𝟙
                  (prod.leftInverseUnitor C ⋙ fromPUnit (𝟙_ V) ⊠ F ⟶
                    prod.leftInverseUnitor C ⋙ (fromPUnit (𝟙_ C)).prod (𝟭 C) ⋙ tensor C ⋙ U ⊛ F)))
              ((prod.leftInverseUnitor C).whiskerLeft
                (((U ⊠ F).homEquivOfIsLeftKanExtension (extensionUnitLeft U (φ U) F) (tensor C ⋙ U ⊛ F))
                  (((U ⊛ F).homEquivOfIsLeftKanExtension (DayConvolution.unit U F) (U ⊛ F)) (𝟙 (U ⊛ F)))))).app
          x ≫
        (U ⊛ F).map (λ_ x).hom =
    (λ_ (F.obj x)).inv ≫ can ▷ F.obj x ≫ (DayConvolution.unit U F).app (𝟙_ C, x) ≫ (U ⊛ F).map (λ_ x).hom
Module: Mathlib.CategoryTheory.ObjectProperty.Ind

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
X : C
hX : P X
⊢ P.ind X

Tactic:
exact ⟨PUnit, inferInstance, inferInstance, .self X, by simpa⟩

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

Goal state before:
pp: case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
H : P ≤ isFinitelyPresentable C
inst✝ : IsFinitelyAccessibleCategory C
X : C
x✝ : P.ind X
Z : C
g : Z ⟶ X
hZ : IsFinitelyPresentable Z
J : Type w
w✝¹ : SmallCategory J
w✝ : IsFiltered J
pres : ColimitPresentation J X
h : ∀ (i : J), P (pres.diag.obj i)
⊢ ∃ W u v, u ≫ v = g ∧ P W

pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
H : P ≤ isFinitelyPresentable C
inst✝ : IsFinitelyAccessibleCategory C
X : C
hfac : ∀ {Z : C} (g : Z ⟶ X) [IsFinitelyPresentable Z], ∃ W u v, u ≫ v = g ∧ P W
⊢ P.ind X

Tactic:
· have : IsFinitelyPresentable Z := hZ
    obtain ⟨j, u, hcomp⟩ := IsFinitelyPresentable.exists_hom_of_isColimit pres.isColimit g
    exact ⟨_, u, pres.ι.app j, hcomp, h j⟩

Goal state after:
case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
H : P ≤ isFinitelyPresentable C
inst✝ : IsFinitelyAccessibleCategory C
X : C
hfac : ∀ {Z : C} (g : Z ⟶ X) [IsFinitelyPresentable Z], ∃ W u v, u ≫ v = g ∧ P W
⊢ P.ind X
Module: Mathlib.CategoryTheory.MorphismProperty.LocalClosure

Goal state before:
pp: case comp
C : Type u
inst✝¹ : Category.{v, u} C
K : Precoverage C
P Q : MorphismProperty C
h : P ≤ Q
inst✝ : Q.IsLocalAtSource K
X Y : C
f✝ : X ⟶ Y
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : sourceLocalClosure K P f
R : Presieve X✝
hR : R ∈ K.coverings X✝
U✝ : C
g : U✝ ⟶ X✝
hg : R g
ih : Q f
⊢ Q (g ≫ f)

Tactic:
apply IsLocalAtSource.comp hR _ hg ih

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

Goal state before:
pp: α : PartOrdEmb
P : Set ↑α → Prop
inst✝¹ : IsDirectedOrder (Subtype P)
inst✝ : Nonempty (Subtype P)
hP : ∀ (a : ↑α), ∃ J, P J ∧ a ∈ J
a : ((forget PartOrdEmb).mapCocone (coconeOfPredicateSet P)).pt
⊢ ∃ i xi, a = (ConcreteCategory.hom (((forget PartOrdEmb).mapCocone (coconeOfPredicateSet P)).ι.app i)) xi

Tactic:
obtain ⟨J, hJ, ha⟩ := hP a

Goal state after:
α : PartOrdEmb
P : Set ↑α → Prop
inst✝¹ : IsDirectedOrder (Subtype P)
inst✝ : Nonempty (Subtype P)
hP : ∀ (a : ↑α), ∃ J, P J ∧ a ∈ J
a : ((forget PartOrdEmb).mapCocone (coconeOfPredicateSet P)).pt
J : Set ↑α
hJ : P J
ha : a ∈ J
⊢ ∃ i xi, a = (ConcreteCategory.hom (((forget PartOrdEmb).mapCocone (coconeOfPredicateSet P)).ι.app i)) xi
Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection

Goal state before:
pp: case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
W : MorphismProperty C
J : Type u'
inst✝³ : Category.{v', u'} J
inst✝² : EssentiallySmall.{w, v', u'} J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hW : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → IsCardinalPresentable X κ ∧ IsCardinalPresentable Y κ
Z : C
x✝ : W.isLocal.colimitsOfShape J Z
X Y : C
f : X ⟶ Y
hf : W f
p : W.isLocal.ColimitOfShape J Z
left✝ : IsCardinalPresentable X κ
right✝ : IsCardinalPresentable Y κ
g : X ⟶ Z
⊢ ∃ a, (fun g ↦ f ≫ g) a = g

Tactic:
· obtain ⟨j, g, rfl⟩ := IsCardinalPresentable.exists_hom_of_isColimit κ p.isColimit g
      obtain ⟨g, rfl⟩ := (p.prop_diag_obj j _ hf).2 g
      exact ⟨g ≫ p.ι.app j, by simp⟩

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✝⁴ : HasCoproduct D₁.obj₁
inst✝³ : HasCoproduct D₁.obj₂
inst✝² : HasPushouts C
inst✝¹ : MorphismProperty.IsSmall.{w, v, u} W
inst✝ : LocallySmall.{w, v, u} C
⊢ Small.{w, max u v} (D₂ W Z)

Tactic:
dsimp [D₂]
  infer_instance

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✝³ : HasCoproduct D₁.obj₁
inst✝² : HasCoproduct D₁.obj₂
inst✝¹ : HasPushouts C
inst✝ : HasMulticoequalizer (D₂.multispanIndex W Z)
x✝ : IsIso (toSucc W Z)
X Y : C
f : X ⟶ Y
hf : W f
g : X ⟶ Z
hZ : toStep W Z ≫ fromStep W Z ≫ inv (toSucc W Z) = 𝟙 Z
⊢ (fun g ↦ f ≫ g) (D₁.ιRight f hf g ≫ pushout.inl (D₁.t W Z) (D₁.l W Z) ≫ fromStep W Z ≫ inv (toSucc W Z)) = g

Tactic:
simp [← D₁.ιLeft_comp_t_assoc, pushout.condition_assoc, hZ]

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.SharplyLT.Basic

Goal state before:
pp: case succ.refine_1
κ₁ κ₂ : Cardinal.{w}
inst✝¹ : Fact κ₁.IsRegular
inst✝ : Fact κ₂.IsRegular
h₀ : κ₁ < κ₂
X : Type w
Y : (B : Set X) → HasCardinalLT (↑B) κ₂ → Set (SetCardinalLT κ₁ ↑B)
hY : ∀ (B : Set X) (hB : HasCardinalLT (↑B) κ₂), HasCardinalLT (↑(Y B hB)) κ₂
m : (B : Set X) → (hB : HasCardinalLT (↑B) κ₂) → (C : SetCardinalLT κ₁ ↑B) → C ∈ Y B hB → X
A : Set X
hA : HasCardinalLT (↑A) κ₂
j : κ₁.ord.ToType
hj : ¬IsMax j
hj' : HasCardinalLT (↑(transfiniteIterate (φ Y m) j A)) κ₂
hκ₂ : κ₂.IsRegular
x✝¹ : ↑(Y (transfiniteIterate (φ Y m) j A) hj')
C : SetCardinalLT κ₁ ↑(transfiniteIterate (φ Y m) j A)
hC : C ∈ Y (transfiniteIterate (φ Y m) j A) hj'
x✝ : ↑(Subtype.val '' ↑↑⟨C, hC⟩)
c : X
hc : c ∈ Subtype.val '' ↑↑⟨C, hC⟩
⊢ ↑↑C

Tactic:
simp only [Set.mem_image, Subtype.exists, exists_and_right, exists_eq_right] at hc
      exact ⟨⟨c, hc.choose⟩, hc.choose_spec⟩

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Regular C
X Y : C
f✝ : X ⟶ Y
A B : C
f : A ⟶ B
A' : Subobject A
B' : Subobject B
⊢ (⋯.lift ((A' ⊓ (Subobject.pullback f).obj B').ofLE ((Subobject.pullback f).obj B') ⋯ ≫ pullbackπ f B')
          ((A' ⊓ (Subobject.pullback f).obj B').ofLE A' ⋯ ≫ (imageFactorisation f A').F.e) ⋯ ≫
        ((«exists» f).obj A' ⊓ B').ofLE ((«exists» f).obj A') ⋯) ≫
      ((«exists» f).obj A').arrow =
    (A' ⊓ (Subobject.pullback f).obj B').arrow ≫ f

Tactic:
(inf_isPullback ((«exists» f).obj A') B').flip.lift_snd

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Regular C
X Y : C
f✝ : X ⟶ Y
A B : C
f : A ⟶ B
A' : Subobject A
B' : Subobject B
⊢ ((A' ⊓ (Subobject.pullback f).obj B').ofLE A' ⋯ ≫ (imageFactorisation f A').F.e) ≫ ((«exists» f).obj A').arrow =
    (A' ⊓ (Subobject.pullback f).obj B').arrow ≫ f
Module: Mathlib.CategoryTheory.Presentable.Directed

Goal state before:
pp: case inr
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
h₂ : ∀ {j : J} (hj : D.P j) {f : j ⟶ m₁}, (D₄ D φ).W f → f = φ ⟨j, hj⟩
h₃ : ∀ {f : m₁ ⟶ m₁}, (D₄ D φ).W f → f = 𝟙 m₁
X Y j : J
hj : D.P j
⊢ ∃ li lj, (D₄ D φ).W li ∧ (D₄ D φ).W lj ∧ φ ⟨j, hj⟩ ≫ lj = li

Tactic:
· exact ⟨φ ⟨_, hj⟩, 𝟙 _, Or.inr ⟨_⟩, Or.inl (Or.inr ⟨⟨⟩⟩), by simp⟩

Goal state after:
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 π'
⊢ (Presieve.ofArrows (fun x ↦ Y) fun x ↦ π) ∈ (regularCoverage C).coverings X

Tactic:
use Y, π

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

Goal state before:
pp: case mpr
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
FD : D → D → Type u_3
CD : D → Type w
inst✝² : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝¹ : ConcreteCategory D FD
inst✝ : Preregular C
F G : Cᵒᵖ ⥤ D
f : F ⟶ G
⊢ (∀ (X : C) (y : ToType (G.obj (op X))),
      ∃ X' φ,
        ∃ (_ : EffectiveEpi φ),
          ∃ x, (ConcreteCategory.hom (f.app (op X'))) x = (ConcreteCategory.hom (G.map (op φ))) y) →
    Presheaf.IsLocallySurjective (regularTopology C) f

Tactic:
· intro h
    refine ⟨fun y ↦ ?_⟩
    obtain ⟨X', π, h, h'⟩ := h _ y
    rw [regularTopology.mem_sieves_iff_hasEffectiveEpi]
    exact ⟨X', π, h, h'⟩

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

Goal state before:
pp: case refine_1
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
A : Type u₃
inst✝⁴ : Category.{v₃, u₃} A
F : Cᵒᵖ ⥤ A
B : Type u₄
inst✝³ : Category.{v₄, u₄} B
s : A ⥤ B
inst✝² : Preregular C
inst✝¹ : FinitaryExtensive C
h : ∀ {Y X : C} (f : Y ⟶ X) [EffectiveEpi f], HasPullback f f
inst✝ : ReflectsFiniteLimits s
left✝ : PreservesFiniteProducts (F ⋙ s)
hF₂ : EqualizerCondition (F ⋙ s)
n : ℕ
K : Discrete (Fin n) ⥤ Cᵒᵖ
c : Cone K
hc : IsLimit c
⊢ Nonempty (IsLimit (F.mapCone c))

Tactic:
exact ⟨isLimitOfReflects s (isLimitOfPreserves (F ⋙ s) hc)⟩

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u₂
inst✝² : Category.{v₂, u₂} A
inst✝¹ : HasWeakSheafify J A
inst✝ : HasGlobalSectionsFunctor J A
F G : Sheaf J A
f : F ⟶ G
U : Cᵒᵖ
⊢ (Γ J A).map f ≫ G.ΓRes U = F.ΓRes U ≫ f.hom.app U

Tactic:
refine .trans ?_ <| congr_app (ΓHomEquiv_naturality_right_symm _ _) U
  exact (congr_app (ΓHomEquiv_naturality_left_symm ((Γ J A).map f) (𝟙 _)) U).symm.trans (by simp)

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.Saturate

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
A : Type u_2
inst✝³ : Category.{v_2, u_2} A
S✝¹ : C
E✝¹ : PreZeroHypercover S✝¹
inst✝² : E✝¹.HasPullbacks
S✝ : C
E✝ : PreZeroHypercover S✝
inst✝¹ : E✝.HasPullbacks
S : C
E : PreZeroHypercover S
inst✝ : E.HasPullbacks
F : Cᵒᵖ ⥤ A
⊢ PreOneHypercover.Homotopy (PreOneHypercover.Hom.comp E.toSaturateOfHasPullbacks E.fromSaturateOfHasPullbacks)
    (PreOneHypercover.Hom.id E.toPreOneHypercover)

Tactic:
by
      rw [toSaturateOfHasPullbacks_fromSaturateOfHasPullbacks]
      exact E.toPreOneHypercoverHomotopy

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

Goal state before:
pp: case refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
K : GrothendieckTopology C
A : Type u_2
inst✝ : Category.{v_2, u_2} A
ι : Type u_3
X : ι → C
hX : K.CoversTop X
F G : Sheaf K A
f : F ⟶ G
h : ∀ (i : ι), IsIso ((K.overPullback A (X i)).map f)
hiso : ∀ (Z : C) (i : ι) (g : Z ⟶ X i), IsIso (f.hom.app (op Z))
W : Cᵒᵖ
S : K.Cover (unop W) := hX.cover (unop W)
harrow : ∀ (I : S.Arrow), IsIso (f.hom.app (op I.Y))
invMap : G.obj.obj (op (unop W)) ⟶ F.obj.obj (op (unop W)) :=
  ⋯.amalgamate S (fun I ↦ G.obj.map I.f.op ≫ inv (f.hom.app (op I.Y))) ⋯
I : S.Arrow
⊢ f.hom.app W ≫ G.obj.map I.f.op ≫ inv (f.hom.app (op I.Y)) = F.obj.map I.f.op

Tactic:
← f.hom.naturality_assoc

Goal state after:
case refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
K : GrothendieckTopology C
A : Type u_2
inst✝ : Category.{v_2, u_2} A
ι : Type u_3
X : ι → C
hX : K.CoversTop X
F G : Sheaf K A
f : F ⟶ G
h : ∀ (i : ι), IsIso ((K.overPullback A (X i)).map f)
hiso : ∀ (Z : C) (i : ι) (g : Z ⟶ X i), IsIso (f.hom.app (op Z))
W : Cᵒᵖ
S : K.Cover (unop W) := hX.cover (unop W)
harrow : ∀ (I : S.Arrow), IsIso (f.hom.app (op I.Y))
invMap : G.obj.obj (op (unop W)) ⟶ F.obj.obj (op (unop W)) :=
  ⋯.amalgamate S (fun I ↦ G.obj.map I.f.op ≫ inv (f.hom.app (op I.Y))) ⋯
I : S.Arrow
⊢ F.obj.map I.f.op ≫ f.hom.app (op I.Y) ≫ inv (f.hom.app (op I.Y)) = F.obj.map I.f.op
Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology C
inst✝ : F.IsPrestack J
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
hf' : Sieve.ofArrows X' f' ∈ J S
D₁ D₂ : F.DescentData f
φ : (pullFunctor F ⋯).obj D₁ ⟶ (pullFunctor F ⋯).obj D₂
i : ι'
⊢ D₁.hom (f' i) (p' i) (p' i) ⋯ ⋯ ≫ φ.hom i ≫ D₂.hom (f' i) (p' i) (p' i) ⋯ ⋯ = φ.hom i

Tactic:
D₁.hom_self _ _ (by cat_disch),

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology C
inst✝ : F.IsPrestack J
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
hf' : Sieve.ofArrows X' f' ∈ J S
D₁ D₂ : F.DescentData f
φ : (pullFunctor F ⋯).obj D₁ ⟶ (pullFunctor F ⋯).obj D₂
i : ι'
⊢ 𝟙 ((F.map (p' i).op.toLoc).toFunctor.obj (D₁.obj (α i))) ≫ φ.hom i ≫ D₂.hom (f' i) (p' i) (p' i) ⋯ ⋯ = φ.hom i