mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.Braided

Goal state before:
pp: C : Type u₁
inst✝¹⁸ : Category.{v₁, u₁} C
V : Type u₂
inst✝¹⁷ : Category.{v₂, u₂} V
inst✝¹⁶ : MonoidalCategory C
inst✝¹⁵ : BraidedCategory C
inst✝¹⁴ : MonoidalCategory V
inst✝¹³ : BraidedCategory V
F G : C ⥤ 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)
H : C ⥤ V
inst✝¹⁰ : DayConvolution F G
inst✝⁹ : DayConvolution G H
inst✝⁸ : DayConvolution F (G ⊛ H)
inst✝⁷ : DayConvolution (F ⊛ G) H
inst✝⁶ : DayConvolution H (F ⊛ G)
inst✝⁵ : DayConvolution H F
inst✝⁴ : DayConvolution (H ⊛ F) G
inst✝³ : DayConvolution H G
inst✝² : DayConvolution F (H ⊛ G)
inst✝¹ : DayConvolution F H
inst✝ : DayConvolution (F ⊛ H) G
x y z : C
⊢ F.obj x ◁ (β_ (G.obj y) (H.obj z)).hom ≫
      (α_ (F.obj x) (H.obj z) (G.obj y)).inv ≫
        (β_ (F.obj x) (H.obj z)).hom ▷ G.obj y ≫
          (unit H F).app (z, x) ▷ G.obj y ≫
            (unit (H ⊛ F) G).app (z ⊗ x, y) ≫ ((H ⊛ F) ⊛ G).map ((β_ z x).hom ▷ y ≫ (α_ x z y).hom ≫ x ◁ (β_ z y).hom) =
    F.obj x ◁ (β_ (G.obj y) (H.obj z)).hom ≫
      (α_ (F.obj x) (H.obj z) (G.obj y)).inv ≫
        (unit F H).app (x, z) ▷ G.obj y ≫
          (braiding F H).hom.app (x ⊗ z) ▷ G.obj y ≫
            (unit (H ⊛ F) G).app (x ⊗ z, y) ≫ ((H ⊛ F) ⊛ G).map ((α_ x z y).hom ≫ x ◁ (β_ z y).hom)

Tactic:
congr 2

Goal state after:
case e_a
C : Type u₁
inst✝¹⁸ : Category.{v₁, u₁} C
V : Type u₂
inst✝¹⁷ : Category.{v₂, u₂} V
inst✝¹⁶ : MonoidalCategory C
inst✝¹⁵ : BraidedCategory C
inst✝¹⁴ : MonoidalCategory V
inst✝¹³ : BraidedCategory V
F G : C ⥤ 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)
H : C ⥤ V
inst✝¹⁰ : DayConvolution F G
inst✝⁹ : DayConvolution G H
inst✝⁸ : DayConvolution F (G ⊛ H)
inst✝⁷ : DayConvolution (F ⊛ G) H
inst✝⁶ : DayConvolution H (F ⊛ G)
inst✝⁵ : DayConvolution H F
inst✝⁴ : DayConvolution (H ⊛ F) G
inst✝³ : DayConvolution H G
inst✝² : DayConvolution F (H ⊛ G)
inst✝¹ : DayConvolution F H
inst✝ : DayConvolution (F ⊛ H) G
x y z : C
⊢ (β_ (F.obj x) (H.obj z)).hom ▷ G.obj y ≫
      (unit H F).app (z, x) ▷ G.obj y ≫
        (unit (H ⊛ F) G).app (z ⊗ x, y) ≫ ((H ⊛ F) ⊛ G).map ((β_ z x).hom ▷ y ≫ (α_ x z y).hom ≫ x ◁ (β_ z y).hom) =
    (unit F H).app (x, z) ▷ G.obj y ≫
      (braiding F H).hom.app (x ⊗ z) ▷ G.obj y ≫
        (unit (H ⊛ F) G).app (x ⊗ z, y) ≫ ((H ⊛ F) ⊛ G).map ((α_ x z y).hom ≫ x ◁ (β_ z y).hom)
Module: Mathlib.CategoryTheory.Monoidal.Hopf_

Goal state before:
pp: case hba
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 ≫ 𝒮) ▷ A ≫ B ◁ f ≫ μ = 1

Tactic:
Conv.one_eq

Goal state after:
case hba
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 ≫ 𝒮) ▷ A ≫ B ◁ 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 ▷ A ≫ B ◁ (𝒮 ≫ f) ≫ μ = 1

Tactic:
Conv.one_eq

Goal state after:
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 ▷ A ≫ B ◁ (𝒮 ≫ f) ≫ μ = ε ≫ η
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
this : η ≫ Δ ≫ 𝒮 ▷ A ≫ μ = η ≫ Δ ≫ 𝒮 ▷ A ≫ μ
| η ≫ Δ ≫ 𝒮 ▷ A ≫ μ = η ≫ Δ ≫ 𝒮 ▷ A ≫ μ

Tactic:
rhs
    rw [antipode_left]

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
this : η ≫ Δ ≫ 𝒮 ▷ A ≫ μ = η ≫ Δ ≫ 𝒮 ▷ A ≫ μ
| η ≫ ε ≫ η
Module: Mathlib.CategoryTheory.Monoidal.Hopf_

Goal state before:
pp: case hba
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ Δ ≫ (𝒮 ≫ Δ) ▷ A ≫ (A ⊗ A) ◁ Δ ≫ μ = 1

Tactic:
Conv.one_eq

Goal state after:
case hba
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ Δ ≫ (𝒮 ≫ Δ) ▷ A ≫ (A ⊗ A) ◁ Δ ≫ μ = ε ≫ η
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 : C
inst✝ : HopfObj A
⊢ Δ ≫ Δ ▷ A ≫ (A ⊗ A) ◁ (Δ ≫ (β_ A A).hom ≫ (𝒮 ⊗ₘ 𝒮)) ≫ μ = 1

Tactic:
Conv.one_eq

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

Goal state before:
pp: case hba
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ Δ ≫ (μ ≫ 𝒮) ▷ (A ⊗ A) ≫ A ◁ μ ≫ μ = 1

Tactic:
Conv.one_eq

Goal state after:
case hba
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ Δ ≫ (μ ≫ 𝒮) ▷ (A ⊗ A) ≫ A ◁ μ ≫ μ = ε ≫ η
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 : C
inst✝ : HopfObj A
⊢ Δ ≫ μ ▷ (A ⊗ A) ≫ A ◁ ((𝒮 ⊗ₘ 𝒮) ≫ (β_ A A).hom ≫ μ) ≫ μ = 1

Tactic:
Conv.one_eq

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

Goal state before:
pp: case hba
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
comm : (β_ A A).hom ≫ μ = μ
⊢ Δ ≫ (𝒮 ≫ 𝒮) ▷ A ≫ A ◁ 𝒮 ≫ μ = 1

Tactic:
Conv.one_eq

Goal state after:
case hba
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
comm : (β_ A A).hom ≫ μ = μ
⊢ Δ ≫ (𝒮 ≫ 𝒮) ▷ A ≫ A ◁ 𝒮 ≫ μ = ε ≫ η
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 : C
inst✝ : HopfObj A
comm : (β_ A A).hom ≫ μ = μ
⊢ Δ ≫ 𝒮 ▷ A ≫ A ◁ 𝟙 A ≫ μ = 1

Tactic:
Conv.one_eq

Goal state after:
case hac
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
comm : (β_ A A).hom ≫ μ = μ
⊢ Δ ≫ 𝒮 ▷ A ≫ A ◁ 𝟙 A ≫ μ = ε ≫ η
Module: Mathlib.CategoryTheory.Monoidal.Internal.Module

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
A : ModuleCat R
inst✝ : MonObj A
x y : R
⊢ (Hom.hom η).toFun (x * y) = (Hom.hom η).toFun x * (Hom.hom η).toFun y

Tactic:
by
      have h := LinearMap.congr_fun (ModuleCat.hom_ext_iff.mp (one_mul A).symm) (x ⊗ₜ η[A] y)
      rwa [MonoidalCategory.leftUnitor_hom_apply, ← η[A].hom.map_smul] at h

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

Goal state before:
pp: J : Type w
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimitsOfShape J C
inst✝ : MonoidalCategory C
F G H : J ⥤ C
j : J
| limit.lift (F ⊗ G) { pt := limit F ⊗ limit G, π := { app := fun j ↦ limit.π F j ⊗ₘ limit.π G j, naturality := ⋯ } } ▷
      limit H ≫
    (limit.π (F ⊗ G) j ⊗ₘ limit.π H j) ≫ (α_ (F.obj j) (G.obj j) (H.obj j)).hom

Tactic:
rw [tensorHom_def, Category.assoc, ← comp_whiskerRight_assoc,
        limit.lift_π, tensor_whiskerLeft, Category.assoc, Category.assoc,
        Iso.inv_hom_id, Category.comp_id,
        ← associator_naturality_right, ← tensorHom_def_assoc]

Goal state after:
J : Type w
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimitsOfShape J C
inst✝ : MonoidalCategory C
F G H : J ⥤ C
j : J
| ({ pt := limit F ⊗ limit G, π := { app := fun j ↦ limit.π F j ⊗ₘ limit.π G j, naturality := ⋯ } }.π.app j ⊗ₘ
      limit.π H j) ≫
    (α_ (F.obj j) (G.obj j) (H.obj j)).hom
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
F' G' : C ⥤ V
inst✝ : DayConvolution F' G'
f : F ⟶ F'
g : G ⟶ G'
x y : C
⊢ (unit F G).app (x, y) ≫ (map f g).app (x ⊗ y) = (f.app x ⊗ₘ g.app y) ≫ (unit F' G').app (x, y)

Tactic:
simpa [tensorHom_def] using!
    (Functor.descOfIsLeftKanExtension_fac_app (F ⊛ G) (unit F G) (F' ⊛ G') <|
      (externalProductBifunctor C C V).map (f ×ₘ g) ≫ unit F' G') (x, y)

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

Goal state before:
pp: 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 ≫ colimit.ι (parallelPair (μ ▷ N.X) ((α_ X.X X.X N.X).hom ≫ X.X ◁ N.actLeft)) WalkingParallelPair.one =
    X.X ◁ f.hom ≫
      (λ_ (X.X ⊗ N.X)).inv ≫
        η ▷ (X.X ⊗ N.X) ≫
          (α_ X.X X.X N.X).inv ≫ μ ▷ N.X ≫ coequalizer.π (μ ▷ N.X) ((α_ X.X X.X N.X).hom ≫ X.X ◁ N.actLeft)

Tactic:
slice_rhs 3 4 => rw [associator_inv_naturality_left]

Goal state after:
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 ≫ colimit.ι (parallelPair (μ ▷ N.X) ((α_ X.X X.X N.X).hom ≫ X.X ◁ N.actLeft)) WalkingParallelPair.one =
    X.X ◁ f.hom ≫
      (λ_ (X.X ⊗ N.X)).inv ≫
        (((α_ (𝟙_ C) X.X N.X).inv ≫ η ▷ X.X ▷ N.X) ≫ μ ▷ N.X) ≫
          coequalizer.π (μ ▷ N.X) ((α_ X.X X.X N.X).hom ≫ X.X ◁ N.actLeft)
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
F : C ⥤ D
inst✝¹ : P.IsClosedUnderIsomorphisms
inst✝ : F.IsEquivalence
⊢ (P.inverseImage F).ind = P.ind.inverseImage F

Tactic:
refine le_antisymm (ind_inverseImage_le _ _) fun X ⟨J, _, _, pres, h⟩ ↦ ?_

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
D : Type u_1
inst✝² : Category.{u_2, u_1} D
P : ObjectProperty D
F : C ⥤ D
inst✝¹ : P.IsClosedUnderIsomorphisms
inst✝ : F.IsEquivalence
X : C
x✝ : P.ind.inverseImage F X
J : Type w
w✝¹ : SmallCategory J
w✝ : IsFiltered J
pres : ColimitPresentation J (F.obj X)
h : ∀ (i : J), P (pres.diag.obj i)
⊢ (P.inverseImage F).ind X
Module: Mathlib.CategoryTheory.Presentable.ColimitPresentation

Goal state before:
pp: case hom
C : Type u
inst✝⁷ : Category.{v, u} C
J✝ : Type u_1
I✝ : J✝ → Type u_2
inst✝⁶ : Category.{v_1, u_1} J✝
inst✝⁵ : (j : J✝) → Category.{?u.14, u_2} (I✝ j)
D✝ : J✝ ⥤ C
P✝ : (j : J✝) → ColimitPresentation (I✝ j) (D✝.obj j)
J : Type w
I : J → Type w
inst✝⁴ : SmallCategory J
inst✝³ : (j : J) → SmallCategory (I j)
D : J ⥤ C
P : (j : J) → ColimitPresentation (I j) (D.obj j)
inst✝² : IsFiltered J
inst✝¹ : ∀ (j : J), IsFiltered (I j)
inst✝ : ∀ (j : J) (i : I j), IsFinitelyPresentable ((P j).diag.obj i)
k l : Total P
f g : k ⟶ l
a : J := ⋯
a' : I (IsFiltered.coeq f.base g.base)
u : Total.mk P l.fst l.snd ⟶ Total.mk P (IsFiltered.coeq f.base g.base) a'
hu : u.base = IsFiltered.coeqHom f.base g.base
this :
  (f.hom ≫ u.hom) ≫
      (P (Total.mk P (IsFiltered.coeq f.base g.base) a').fst).ι.app
        (Total.mk P (IsFiltered.coeq f.base g.base) a').snd =
    (g.hom ≫ u.hom) ≫
      (P (Total.mk P (IsFiltered.coeq f.base g.base) a').fst).ι.app (Total.mk P (IsFiltered.coeq f.base g.base) a').snd
j : I (Total.mk P (IsFiltered.coeq f.base g.base) a').fst
p q : a' ⟶ j
hpq :
  (f.hom ≫ u.hom) ≫ (P (Total.mk P (IsFiltered.coeq f.base g.base) a').fst).diag.map p =
    (g.hom ≫ u.hom) ≫ (P (Total.mk P (IsFiltered.coeq f.base g.base) a').fst).diag.map q
⊢ (f ≫
        u ≫
          { base := 𝟙 (Total.mk P (IsFiltered.coeq f.base g.base) a').fst,
            hom := (P (Total.mk P (IsFiltered.coeq f.base g.base) a').fst).diag.map (p ≫ IsFiltered.coeqHom p q),
            w := ⋯ }).hom =
    (g ≫
        u ≫
          { base := 𝟙 (Total.mk P (IsFiltered.coeq f.base g.base) a').fst,
            hom := (P (Total.mk P (IsFiltered.coeq f.base g.base) a').fst).diag.map (p ≫ IsFiltered.coeqHom p q),
            w := ⋯ }).hom

Tactic:
· rw [Category.assoc] at hpq
      simp only [Functor.map_comp, comp_hom, reassoc_of% hpq]
      simp [← Functor.map_comp, ← IsFiltered.coeq_condition]

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

Goal state before:
pp: case refine_1.comp.refine_1
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✝
hf : sourceLocalClosure K P f
U✝ : C
g : U✝ ⟶ X✝
E : K.ZeroHypercover X✝
h : ∀ (U : C) (g : U ⟶ X✝), Presieve.ofArrows E.X E.f g → P (g ≫ f)
F : K.ZeroHypercover X✝
hg : Presieve.ofArrows F.X F.f g
U : C
v : U ⟶ U✝
i : (Precoverage.ZeroHypercover.pullback₁ g E).I₀
⊢ K.morphismProperty (pullback.snd g (E.f i))

pp: case refine_1.comp.refine_2
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✝
hf : sourceLocalClosure K P f
U✝ : C
g : U✝ ⟶ X✝
E : K.ZeroHypercover X✝
h : ∀ (U : C) (g : U ⟶ X✝), Presieve.ofArrows E.X E.f g → P (g ≫ f)
F : K.ZeroHypercover X✝
hg : Presieve.ofArrows F.X F.f g
U : C
v : U ⟶ U✝
i : (Precoverage.ZeroHypercover.pullback₁ g E).I₀
⊢ P (E.f i ≫ f)

Tactic:
· obtain ⟨j⟩ := hg
        exact (F.pullback₂ (E.f i)).morphismProperty j

Goal state after:
case refine_1.comp.refine_2
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✝
hf : sourceLocalClosure K P f
U✝ : C
g : U✝ ⟶ X✝
E : K.ZeroHypercover X✝
h : ∀ (U : C) (g : U ⟶ X✝), Presieve.ofArrows E.X E.f g → P (g ≫ f)
F : K.ZeroHypercover X✝
hg : Presieve.ofArrows F.X F.f g
U : C
v : U ⟶ U✝
i : (Precoverage.ZeroHypercover.pullback₁ g E).I₀
⊢ P (E.f i ≫ f)
Module: Mathlib.CategoryTheory.Preadditive.EndoFunctor

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : F.Additive
A₁ A₂ : Coalgebra F
α : A₁ ⟶ A₂
⊢ A₁.str ≫ F.map (-α.f) = (-α.f) ≫ A₂.str

Tactic:
by simp only [Functor.map_neg, comp_neg, Endofunctor.Coalgebra.Hom.h, neg_comp]

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

Goal state before:
pp: case intro
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 α
⊢ Cardinal.mk ↑(f ⁻¹' {c}) = Cardinal.mk ↑(g ⁻¹' {c})

Tactic:
cases nonempty_fintype β

Goal state after:
case intro.intro
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 β
⊢ Cardinal.mk ↑(f ⁻¹' {c}) = Cardinal.mk ↑(g ⁻¹' {c})
Module: Mathlib.CategoryTheory.Preadditive.Projective.LiftingProperties

Goal state before:
pp: case mpr
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
P Z : C
hZ : IsZero Z
h : (MorphismProperty.epimorphisms C).llp 0
X Y : C
f : P ⟶ Y
p : X ⟶ Y
hp : Epi p
this : HasLiftingProperty 0 p
sq : CommSq 0 0 p f
⊢ ∃ f', f' ≫ p = f

Tactic:
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
𝕜 : Type u_2
inst✝⁷ : Field 𝕜
inst✝⁶ : IsAlgClosed 𝕜
inst✝⁵ : Linear 𝕜 C
inst✝⁴ : HasKernels C
X Y : C
inst✝³ : FiniteDimensional 𝕜 (X ⟶ X)
inst✝² : FiniteDimensional 𝕜 (X ⟶ Y)
inst✝¹ : Simple X
inst✝ : Simple Y
⊢ finrank 𝕜 (X ⟶ Y) = 1 ↔ Nonempty (X ≅ Y)

Tactic:
by
  fconstructor
  · intro h
    rw [finrank_eq_one_iff'] at h
    obtain ⟨f, nz, -⟩ := h
    rw [← isIso_iff_nonzero] at nz
    exact ⟨asIso f⟩
  · rintro ⟨f⟩
    have le_one := finrank_hom_simple_simple_le_one 𝕜 X Y
    have zero_lt : 0 < finrank 𝕜 (X ⟶ Y) :=
      finrank_pos_iff_exists_ne_zero.mpr ⟨f.hom, (isIso_iff_nonzero f.hom).mp inferInstance⟩
    lia

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : HasCardinalFilteredGenerator C κ
⊢ ∃ J x, Nonempty (C ≌ J)

Tactic:
exists_equivalence_iff_of_locallySmall

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : HasCardinalFilteredGenerator C κ
⊢ ObjectProperty.EssentiallySmall.{w + 1, v, u} ⊤
Module: Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset

Goal state before:
pp: κ : Cardinal.{u}
inst✝ : Fact κ.IsRegular
J : CardinalDirectedPoset κ
K : Type u
α : K → Subtype J.PropSet
hK : HasCardinalLT K κ
t : (k : K) → ↑↑(α k) := fun k ↦ ⊤_ ↑↑(α k)
m : ↑J.obj := IsCardinalFiltered.max (fun k ↦ ↑(t k)) hK
S : Set ↑J.obj := (⋃ k, ↑(α k)) ∪ {m}
⊢ ∀ (a : ↑S), a ≤ ⟨m, ⋯⟩

Tactic:
by
          rintro ⟨s, hs⟩
          simp only [Set.union_singleton, Set.mem_insert_iff, Set.mem_iUnion, S] at hs
          obtain rfl | ⟨k, hs⟩ := hs
          · simp
          · simp only [Subtype.mk_le_mk]
            exact leOfHom ((by exact terminal.from (C := (α k).val) ⟨_, hs⟩) ≫
              IsCardinalFiltered.toMax _ hK k)

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

Goal state before:
pp: case inl.inl
J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
i✝ j✝ : J
f✝ : i✝ ⟶ j✝
i : ι
hf : (D i).W f✝
⊢ (∃ a, (D a).P j✝) ∨ m = j✝

Tactic:
exact Or.inl ⟨i, (D i).tgt hf⟩

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Finite α
Y Z : α → C
π : (a : α) → Y a ⟶ X
inst✝ : EffectiveEpiFamily Y π
f : (a : α) → Z a ⟶ Y a
h : ∀ (a : α), EffectiveEpi (f a)
⊢ EffectiveEpiFamily Z fun a ↦ f a ≫ π a

Tactic:
simp_rw [effectiveEpi_iff_effectiveEpiFamily] at h

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Finite α
Y Z : α → C
π : (a : α) → Y a ⟶ X
inst✝ : EffectiveEpiFamily Y π
f : (a : α) → Z a ⟶ Y a
h : ∀ (a : α), EffectiveEpiFamily (fun x ↦ Z a) fun x ↦ f a
⊢ EffectiveEpiFamily Z fun a ↦ f a ≫ π a
Module: Mathlib.CategoryTheory.Sites.Coherent.RegularTopology

Goal state before:
pp: case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preregular C
X : C
S : Sieve X
⊢ S ∈ (regularTopology C) X → ∃ Y π, EffectiveEpi π ∧ S.arrows π

pp: case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preregular C
X : C
S : Sieve X
⊢ (∃ Y π, EffectiveEpi π ∧ S.arrows π) → S ∈ (regularTopology C) X

Tactic:
· intro h
    induction h with
    | of Y T hS =>
      rcases hS with ⟨Y', π, h'⟩
      refine ⟨Y', π, h'.2, ?_⟩
      rcases h' with ⟨rfl, _⟩
      exact ⟨Y', 𝟙 Y', π, Presieve.ofArrows.mk (), (by simp)⟩
    | top Y => exact ⟨Y, (𝟙 Y), inferInstance, by simp only [Sieve.top_apply]⟩
    | transitive Y R S _ _ a b =>
      rcases a with ⟨Y₁, π, ⟨h₁, h₂⟩⟩
      choose Y' π' _ H using b h₂
      exact ⟨Y', π' ≫ π, inferInstance, (by simpa using H)⟩

Goal state after:
case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preregular C
X : C
S : Sieve X
⊢ (∃ Y π, EffectiveEpi π ∧ S.arrows π) → S ∈ (regularTopology C) X
Module: Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
sq : (i j : ι) → ChosenPullback (f i) (f j)
obj obj' : (i : ι) → ↑(F.obj { as := op (X i) })
hom :
  (i j : ι) → (F.map (sq i j).p₁.op.toLoc).toFunctor.obj (obj i) ⟶ (F.map (sq i j).p₂.op.toLoc).toFunctor.obj (obj' j)
Y : C
q : Y ⟶ S
i₁ i₂ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
p : Y ⟶ (sq i₁ i₂).pullback
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
hp₁ : p ≫ (sq i₁ i₂).p₁ = f₁
hp₂ : p ≫ (sq i₁ i₂).p₂ = f₂
⊢ pullHom' hom q f₁ f₂ hf₁ hf₂ = pullHom (hom i₁ i₂) p f₁ f₂ ⋯ ⋯

Tactic:
obtain rfl : p = (sq i₁ i₂).isPullback.lift f₁ f₂ (by rw [hf₁, hf₂]) := by
    apply (sq i₁ i₂).isPullback.hom_ext <;> cat_disch
  rfl

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Descent.DescentData

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
D : F.DescentData f
M : ↑(F.obj { as := op S })
Y' Y : C
g : Y' ⟶ Y
q : Y ⟶ S
q' : Y' ⟶ S
hq : g ≫ q = q'
i₁ i₂ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
gf₁ : Y' ⟶ X i₁
gf₂ : Y' ⟶ X i₂
hgf₁ : g ≫ f₁ = gf₁
hgf₂ : g ≫ f₂ = gf₂
⊢ pullHom
      ((F.mapComp' (f i₁).op.toLoc f₁.op.toLoc q.op.toLoc ⋯).inv.toNatTrans.app M ≫
        (F.mapComp' (f i₂).op.toLoc f₂.op.toLoc q.op.toLoc ⋯).hom.toNatTrans.app M)
      g gf₁ gf₂ ⋯ ⋯ =
    (F.mapComp' (f i₁).op.toLoc gf₁.op.toLoc q'.op.toLoc ⋯).inv.toNatTrans.app M ≫
      (F.mapComp' (f i₂).op.toLoc gf₂.op.toLoc q'.op.toLoc ⋯).hom.toNatTrans.app M

Tactic:
simp only [pullHom, Functor.map_comp, Category.assoc,
      F.mapComp'₀₁₃_inv_app (f i₁).op.toLoc f₁.op.toLoc g.op.toLoc q.op.toLoc
        gf₁.op.toLoc q'.op.toLoc (by grind) (by grind) (by grind),
      F.mapComp'₀₂₃_inv_comp_mapComp'₀₁₃_hom_app (f i₂).op.toLoc f₂.op.toLoc g.op.toLoc
      q.op.toLoc gf₂.op.toLoc q'.op.toLoc (by grind) (by grind) (by grind)]

Goal state after: