mathlib-initiative/mathlib-tactics huggingface dataset:
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

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
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)
⊢ α.natTrans = β.natTrans
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 : C ⊛⥤ V
α β : 𝟙_ (C ⊛⥤ V) ⟶ F
h : ν C V ≫ α.natTrans.app (𝟙_ C) = ν C V ≫ β.natTrans.app (𝟙_ C)
x✝ : Discrete PUnit.{1}
⊢ (νNatTrans C V ≫ (Functor.fromPUnit (𝟙_ C)).whiskerLeft α.natTrans).app x✝ =
    (νNatTrans C V ≫ (Functor.fromPUnit (𝟙_ C)).whiskerLeft β.natTrans).app x✝

Tactic:
exact h

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

Goal state before:
pp: case a
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
inst✝³ : BraidedCategory C
A B : C
inst✝² : HopfObj A
inst✝¹ : HopfObj B
f : A ⟶ B
inst✝ : IsBimonHom f
| f ≫ ε

pp: case a
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
inst✝³ : BraidedCategory C
A B : C
inst✝² : HopfObj A
inst✝¹ : HopfObj B
f : A ⟶ B
inst✝ : IsBimonHom f
| η

Tactic:
rw [IsComonHom.hom_counit]

Goal state after:
case a
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
inst✝³ : BraidedCategory C
A B : C
inst✝² : HopfObj A
inst✝¹ : HopfObj B
f : A ⟶ B
inst✝ : IsBimonHom f
| ε

case a
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
inst✝³ : BraidedCategory C
A B : C
inst✝² : HopfObj A
inst✝¹ : HopfObj B
f : A ⟶ B
inst✝ : IsBimonHom f
| η
Module: Mathlib.CategoryTheory.Monoidal.Hopf_

Goal state before:
pp: case hac
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
inst✝³ : BraidedCategory C
A B : C
inst✝² : HopfObj A
inst✝¹ : HopfObj B
f : A ⟶ B
inst✝ : IsBimonHom f
⊢ f * 𝒮 ≫ f = 1

Tactic:
· rw [Conv.mul_eq, Conv.one_eq]
    simp only [whiskerLeft_comp, Category.assoc]
    slice_lhs 2 3 =>
      rw [← whisker_exchange]
    slice_lhs 3 4 =>
      rw [← tensorHom_def]
    slice_lhs 3 4 =>
      rw [← IsMonHom.mul_hom]
    slice_lhs 1 3 =>
      rw [antipode_right]
    slice_lhs 2 3 =>
      rw [IsMonHom.one_hom]

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 ◁ A ◁ η) ≫ A ◁ 𝒮 ▷ A) ≫ (α_ A A A).inv) ≫ μ ▷ A =
    ε ≫ (λ_ (𝟙_ C)).inv ≫ (η ⊗ₘ η)

Tactic:
slice_lhs 4 5 =>
    simp only [← whiskerLeft_comp]
    rw [whisker_exchange]
    simp only [whiskerLeft_comp]

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 ◁ η) ≫ (α_ A A A).inv) ≫ μ ▷ A =
    ε ≫ (λ_ (𝟙_ C)).inv ≫ (η ⊗ₘ η)
Module: Mathlib.CategoryTheory.Monoidal.Internal.Module

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A : AlgCat R
⊢ MonoidalCategoryStruct.whiskerRight (↟(Algebra.linearMap R ↑A)) (of R ↑A) ≫ ↟(mul' R ↑A) =
    (MonoidalCategoryStruct.leftUnitor (of R ↑A)).hom

Tactic:
ext : 1

Goal state after:
R : Type u
inst✝ : CommRing R
A : AlgCat R
⊢ Hom.hom (MonoidalCategoryStruct.whiskerRight (↟(Algebra.linearMap R ↑A)) (of R ↑A) ≫ ↟(mul' R ↑A)) =
    Hom.hom (MonoidalCategoryStruct.leftUnitor (of R ↑A)).hom
Module: Mathlib.CategoryTheory.Monoidal.Internal.Module

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A : AlgCat R
⊢ MonoidalCategoryStruct.whiskerLeft (of R ↑A) (↟(Algebra.linearMap R ↑A)) ≫ ↟(mul' R ↑A) =
    (MonoidalCategoryStruct.rightUnitor (of R ↑A)).hom

Tactic:
ext : 1

Goal state after:
R : Type u
inst✝ : CommRing R
A : AlgCat R
⊢ Hom.hom (MonoidalCategoryStruct.whiskerLeft (of R ↑A) (↟(Algebra.linearMap R ↑A)) ≫ ↟(mul' R ↑A)) =
    Hom.hom (MonoidalCategoryStruct.rightUnitor (of R ↑A)).hom
Module: Mathlib.CategoryTheory.Monoidal.Internal.Module

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A : AlgCat R
⊢ MonoidalCategoryStruct.whiskerRight (↟(mul' R ↑A)) (of R ↑A) ≫ ↟(mul' R ↑A) =
    (MonoidalCategoryStruct.associator (of R ↑A) (of R ↑A) (of R ↑A)).hom ≫
      MonoidalCategoryStruct.whiskerLeft (of R ↑A) (↟(mul' R ↑A)) ≫ ↟(mul' R ↑A)

Tactic:
ext : 1

Goal state after:
R : Type u
inst✝ : CommRing R
A : AlgCat R
⊢ Hom.hom (MonoidalCategoryStruct.whiskerRight (↟(mul' R ↑A)) (of R ↑A) ≫ ↟(mul' R ↑A)) =
    Hom.hom
      ((MonoidalCategoryStruct.associator (of R ↑A) (of R ↑A) (of R ↑A)).hom ≫
        MonoidalCategoryStruct.whiskerLeft (of R ↑A) (↟(mul' R ↑A)) ≫ ↟(mul' R ↑A))
Module: Mathlib.CategoryTheory.Monoidal.Internal.Module

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A : Mon (ModuleCat R)
⊢ μ ≫ ↟{ toFun := _root_.id, map_add' := ⋯, map_smul' := ⋯ } =
    MonoidalCategoryStruct.tensorHom (↟{ toFun := _root_.id, map_add' := ⋯, map_smul' := ⋯ })
        (↟{ toFun := _root_.id, map_add' := ⋯, map_smul' := ⋯ }) ≫
      μ

Tactic:
ext : 1

Goal state after:
R : Type u
inst✝ : CommRing R
A : Mon (ModuleCat R)
⊢ Hom.hom (μ ≫ ↟{ toFun := _root_.id, map_add' := ⋯, map_smul' := ⋯ }) =
    Hom.hom
      (MonoidalCategoryStruct.tensorHom (↟{ toFun := _root_.id, map_add' := ⋯, map_smul' := ⋯ })
          (↟{ toFun := _root_.id, map_add' := ⋯, map_smul' := ⋯ }) ≫
        μ)
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
H : C ⥤ V
inst✝⁸ : DayConvolution G H
inst✝⁷ : DayConvolution F (G ⊛ H)
inst✝⁶ : DayConvolution (F ⊛ G) H
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)
F' G' H' : C ⥤ V
inst✝³ : DayConvolution F' G'
inst✝² : DayConvolution G' H'
inst✝¹ : DayConvolution F' (G' ⊛ H')
inst✝ : DayConvolution (F' ⊛ G') H'
f : F ⟶ F'
g : G ⟶ G'
h : H ⟶ H'
x✝ : (C × C) × C
⊢ (unit F G).app x✝.1 ▷ H.obj x✝.2 ≫
      ((map f g).app (x✝.1.1 ⊗ x✝.1.2) ⊗ₘ h.app x✝.2) ≫
        (unit (F' ⊛ G') H').app (x✝.1.1 ⊗ x✝.1.2, x✝.2) ≫ (associator F' G' H').hom.app ((x✝.1.1 ⊗ x✝.1.2) ⊗ x✝.2) =
    (unit F G).app x✝.1 ▷ H.obj x✝.2 ≫
      (unit (F ⊛ G) H).app (x✝.1.1 ⊗ x✝.1.2, x✝.2) ≫
        (associator F G H).hom.app ((x✝.1.1 ⊗ x✝.1.2) ⊗ x✝.2) ≫ (map f (map g h)).app ((x✝.1.1 ⊗ x✝.1.2) ⊗ x✝.2)

Tactic:
associator_hom_unit_unit_assoc

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
F G : C ⥤ V
inst✝⁹ : DayConvolution F G
H : C ⥤ V
inst✝⁸ : DayConvolution G H
inst✝⁷ : DayConvolution F (G ⊛ H)
inst✝⁶ : DayConvolution (F ⊛ G) H
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)
F' G' H' : C ⥤ V
inst✝³ : DayConvolution F' G'
inst✝² : DayConvolution G' H'
inst✝¹ : DayConvolution F' (G' ⊛ H')
inst✝ : DayConvolution (F' ⊛ G') H'
f : F ⟶ F'
g : G ⟶ G'
h : H ⟶ H'
x✝ : (C × C) × C
⊢ (unit F G).app x✝.1 ▷ H.obj x✝.2 ≫
      ((map f g).app (x✝.1.1 ⊗ x✝.1.2) ⊗ₘ h.app x✝.2) ≫
        (unit (F' ⊛ G') H').app (x✝.1.1 ⊗ x✝.1.2, x✝.2) ≫ (associator F' G' H').hom.app ((x✝.1.1 ⊗ x✝.1.2) ⊗ x✝.2) =
    (α_ (F.obj x✝.1.1) (G.obj x✝.1.2) (H.obj x✝.2)).hom ≫
      F.obj x✝.1.1 ◁ (unit G H).app (x✝.1.2, x✝.2) ≫
        (unit F (G ⊛ H)).app (x✝.1.1, x✝.1.2 ⊗ x✝.2) ≫
          (F ⊛ G ⊛ H).map (α_ x✝.1.1 x✝.1.2 x✝.2).inv ≫ (map f (map g h)).app ((x✝.1.1 ⊗ x✝.1.2) ⊗ x✝.2)
Module: Mathlib.CategoryTheory.Presentable.Dense

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
κ : Cardinal.{w}
inst✝³ : Fact κ.IsRegular
J : Type u'
inst✝² : Category.{v', u'} J
inst✝¹ : EssentiallySmall.{w, v', u'} J
inst✝ : IsCardinalFiltered J κ
X : C
p : (isCardinalPresentable C κ).ColimitOfShape J X
this : IsFiltered J
⊢ p.toCostructuredArrow.Final

Tactic:
rw [Functor.final_iff_of_isFiltered]

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
κ : Cardinal.{w}
inst✝³ : Fact κ.IsRegular
J : Type u'
inst✝² : Category.{v', u'} J
inst✝¹ : EssentiallySmall.{w, v', u'} J
inst✝ : IsCardinalFiltered J κ
X : C
p : (isCardinalPresentable C κ).ColimitOfShape J X
this : IsFiltered J
⊢ (∀ (d : CostructuredArrow (isCardinalPresentable C κ).ι X), ∃ c, Nonempty (d ⟶ p.toCostructuredArrow.obj c)) ∧
    ∀ {d : CostructuredArrow (isCardinalPresentable C κ).ι X} {c : J} (s s' : d ⟶ p.toCostructuredArrow.obj c),
      ∃ c' t, s ≫ p.toCostructuredArrow.map t = s' ≫ p.toCostructuredArrow.map t
Module: Mathlib.CategoryTheory.MorphismProperty.LocalClosure

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
K : Precoverage C
P : MorphismProperty C
inst✝⁵ : P.RespectsIso
inst✝⁴ : P.RespectsLeft K.morphismProperty
inst✝³ : K.HasIsos
inst✝² : K.IsStableUnderBaseChange
inst✝¹ : K.IsStableUnderComposition
inst✝ : K.HasPullbacks
X Y : C
f✝ : X ⟶ Y
X✝ Y✝ : C
f : X✝ ⟶ Y✝
E : K.ZeroHypercover X✝
h : ∀ (U : C) (g : U ⟶ X✝), Presieve.ofArrows E.X E.f g → sourceLocalClosure K P (g ≫ f)
ih :
  ∀ (U : C) (g : U ⟶ X✝),
    Presieve.ofArrows E.X E.f g → ∃ R ∈ K.coverings U, ∀ (U_1 : C) (g_1 : U_1 ⟶ U), R g_1 → P (g_1 ≫ g ≫ f)
S : (i : E.I₀) → Presieve (E.X i)
h' : ∀ (i : E.I₀) (U : C) (g : U ⟶ E.X i), S i g → P (g ≫ E.f i ≫ f)
F : (i : E.I₀) → K.ZeroHypercover (E.X i)
hF : ∀ (i : E.I₀), S i = Presieve.ofArrows (F i).X (F i).f
U : C
g : U ⟶ X✝
x✝ : (E.bind F).presieve₀ g
j : (E.bind F).I₀
⊢ S j.fst ((F j.fst).f j.snd)

Tactic:
simp [hF]

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
hf : P.localEpi f
⊢ P.isoClosure.localEpi f

Tactic:
Z

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
hf : P.localEpi f
Z : C
⊢ P.isoClosure Z → Function.Injective fun g ↦ f ≫ g
Module: Mathlib.CategoryTheory.Preadditive.Comma

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

Tactic:
simp [add_zsmul]

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

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

Tactic:
simp [add_zsmul]

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

Goal state before:
pp: case w'
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
⊢ ∀ x ∉ g ⁻¹' {h c},
    eqToHom ⋯ ≫
        biproduct.ι (fun a ↦ s (f a)) a ≫
          z ≫
            ((biproduct.π (fun b ↦ s (g b)) x ≫ biproduct.ι (fun b ↦ s (g b)) x) ≫ w) ≫
              biproduct.π (fun b ↦ s (h b)) c =
      0

Tactic:
intro b nm
    simp only [Set.mem_preimage, Set.mem_singleton_iff] at nm
    simp only [Category.assoc]
    convert! comp_zero
    convert! comp_zero
    convert! comp_zero
    convert! comp_zero
    simp only [o.eq_zero nm]

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

Goal state before:
pp: case inl
C : Type u_1
inst✝⁸ : Category.{v_1, u_1} C
inst✝⁷ : Preadditive C
𝕜 : Type u_2
inst✝⁶ : Field 𝕜
inst✝⁵ : IsAlgClosed 𝕜
inst✝⁴ : Linear 𝕜 C
inst✝³ : HasKernels C
X Y : C
inst✝² : FiniteDimensional 𝕜 (X ⟶ X)
inst✝¹ : Simple X
inst✝ : Simple Y
h : Subsingleton (X ⟶ Y)
⊢ finrank 𝕜 (X ⟶ Y) ≤ 1

Tactic:
rw [finrank_zero_of_subsingleton]
    exact zero_le_one

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
s : Cocone F
x y : CoconePt hc
h :
  (ConcreteCategory.hom (hc.desc ((forget PartOrdEmb).mapCocone s))) x =
    (ConcreteCategory.hom (hc.desc ((forget PartOrdEmb).mapCocone s))) y
⊢ x = y

Tactic:
obtain ⟨j, x', y', rfl, rfl⟩ :=
      Types.FilteredColimit.jointly_surjective_of_isColimit₂ hc x y

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
h :
  (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.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
x y : CoconePt hc
⊢ { toFun := ⇑(ConcreteCategory.hom (hc.desc ((forget PartOrdEmb).mapCocone s))), inj' := ⋯ } x ≤
      { toFun := ⇑(ConcreteCategory.hom (hc.desc ((forget PartOrdEmb).mapCocone s))), inj' := ⋯ } y ↔
    x ≤ y

Tactic:
obtain ⟨j, x', y', rfl, rfl⟩ :=
      Types.FilteredColimit.jointly_surjective_of_isColimit₂ hc x y

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
⊢ { 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'
Module: Mathlib.CategoryTheory.Presentable.Directed

Goal state before:
pp: J : Type w
inst✝ : SmallCategory J
κ : Cardinal.{w}
x✝¹ x✝ : DiagramWithUniqueTerminal J κ
h₁ : x✝¹.W ≤ x✝.W ∧ x✝¹.P ≤ x✝.P
h₂ : x✝.W ≤ x✝¹.W ∧ x✝.P ≤ x✝¹.P
⊢ x✝¹ = x✝

Tactic:
ext : 1

Goal state after:
case hW
J : Type w
inst✝ : SmallCategory J
κ : Cardinal.{w}
x✝¹ x✝ : DiagramWithUniqueTerminal J κ
h₁ : x✝¹.W ≤ x✝.W ∧ x✝¹.P ≤ x✝.P
h₂ : x✝.W ≤ x✝¹.W ∧ x✝.P ≤ x✝¹.P
⊢ x✝¹.W = x✝.W

case hP
J : Type w
inst✝ : SmallCategory J
κ : Cardinal.{w}
x✝¹ x✝ : DiagramWithUniqueTerminal J κ
h₁ : x✝¹.W ≤ x✝.W ∧ x✝¹.P ≤ x✝.P
h₂ : x✝.W ≤ x✝¹.W ∧ x✝.P ≤ x✝¹.P
⊢ x✝¹.P = x✝.P
Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection

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

Tactic:
exact h

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

Goal state before:
pp: case refine_2.mk.refl
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preregular C
X Y : C
f : Y ⟶ X
Z : C
π : Z ⟶ X
h_epi : EffectiveEpi π
W : C
h : W ⟶ Y
w✝ : EffectiveEpi h
i : W ⟶ Z
this : i ≫ π = h ≫ f
⊢ Presieve.ofArrows (fun x ↦ Z) (fun x ↦ π) π

Tactic:
rw [Presieve.ofArrows_pUnit]

Goal state after:
case refine_2.mk.refl
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preregular C
X Y : C
f : Y ⟶ X
Z : C
π : Z ⟶ X
h_epi : EffectiveEpi π
W : C
h : W ⟶ Y
w✝ : EffectiveEpi h
i : W ⟶ Z
this : i ≫ π = h ≫ f
⊢ Presieve.singleton π π
Module: Mathlib.CategoryTheory.RepresentedBy

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
X : C
x : F.obj (op X)
Y : C
e : Y ≅ X
h : F.IsRepresentedBy ((ConcreteCategory.hom (F.map e.hom.op)) x)
⊢ x = (ConcreteCategory.hom (F.map e.inv.op)) ((ConcreteCategory.hom (F.map e.hom.op)) x)

Tactic:
simp [← comp_apply, ← map_comp, ← op_comp]

Goal state after:
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 κ)
⊢ (functor J κ).Final

Tactic:
rw [Functor.final_iff_of_isFiltered]

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 κ)
⊢ (∀ (d : J), ∃ c, Nonempty (d ⟶ (functor J κ).obj c)) ∧
    ∀ {d : J} {c : DiagramWithUniqueTerminal J κ} (s s' : d ⟶ (functor J κ).obj c),
      ∃ c' t, s ≫ (functor J κ).map t = s' ≫ (functor J κ).map t
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⟩
f : m₁ ⟶ m₁
hf : MorphismProperty.ofHoms φ f
⊢ f = 𝟙 m₁

Tactic:
rw [MorphismProperty.ofHoms_iff] at hf
      obtain ⟨⟨j, hj⟩, hf⟩ := hf
      obtain rfl : m₁ = j := congr_arg Arrow.leftFunc.obj hf
      exact (h₁ hj).elim

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

Goal state before:
pp: case mpr.hR
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : FinitaryPreExtensive C
X : C
S : Sieve X
α : Type
w✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : Nonempty (IsColimit (Cofan.mk X π))
h' : ∀ (a : α), S.arrows (π a)
⊢ Nonempty (IsColimit (Cofan.mk X π))

Tactic:
exact h

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

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
F : C ⥤ D
inst✝⁵ : F.PreservesEffectiveEpis
inst✝⁴ : F.ReflectsEffectiveEpis
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.EffectivelyEnough
inst✝ : Preregular D
B : D
⊢ Presieve.singleton (F.effectiveEpiOver B) ∈ (regularCoverage D).coverings B

Tactic:
refine ⟨F.effectiveEpiOverObj B, F.effectiveEpiOver B, ?_, inferInstance⟩

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
F : C ⥤ D
inst✝⁵ : F.PreservesEffectiveEpis
inst✝⁴ : F.ReflectsEffectiveEpis
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.EffectivelyEnough
inst✝ : Preregular D
B : D
⊢ Presieve.singleton (F.effectiveEpiOver B) =
    Presieve.ofArrows (fun x ↦ F.effectiveEpiOverObj B) fun x ↦ F.effectiveEpiOver B
Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison

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
F : C ⥤ D
inst✝⁵ : F.PreservesEffectiveEpis
inst✝⁴ : F.ReflectsEffectiveEpis
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.EffectivelyEnough
inst✝ : Preregular D
⊢ regularTopology C = F.inducedTopology (regularTopology D)

Tactic:
by
  ext X S
  have := F.reflects_preregular
  rw [← exists_effectiveEpi_iff_mem_induced F X]
  rw [← mem_sieves_iff_hasEffectiveEpi S]

Goal state after: