mathlib-initiative/mathlib-tactics huggingface dataset:
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
ℌ : DayConvolutionInternalHom F G H
G' H' : C ⥤ V
f✝ : G ⟶ G'
ℌ' : DayConvolutionInternalHom F G' H'
c c' : C
f : c ⟶ c'
j : (multicospanShapeEnd C).L
⊢ H.map f ≫
      Wedge.IsLimit.lift (ℌ'.isLimitWedge c') (fun j ↦ ℌ.π c' j ≫ (ihom (F.obj j)).map (f✝.app (j ⊗ c'))) ⋯ ≫
        ℌ'.π c' j =
    Wedge.IsLimit.lift (ℌ'.isLimitWedge c) (fun j ↦ ℌ.π c j ≫ (ihom (F.obj j)).map (f✝.app (j ⊗ c))) ⋯ ≫
      ℌ'.π c j ≫ (ihom (F.obj j)).map (G'.map (j ◁ f))

Tactic:
rw [← Wedge.mk_ι
        (F := dayConvolutionInternalHomDiagramFunctor F |>.obj _ |>.obj c')
        (H'.obj c') (ℌ'.π c') (ℌ'.hπ c'),
      ← Wedge.mk_ι
        (F := dayConvolutionInternalHomDiagramFunctor F |>.obj _ |>.obj c)
        (H'.obj c) (ℌ'.π c) (ℌ'.hπ c),
      Wedge.IsLimit.lift_ι (ℌ'.isLimitWedge c'),
      Wedge.IsLimit.lift_ι_assoc (ℌ'.isLimitWedge c)]

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
ℌ : DayConvolutionInternalHom F G H
G' H' : C ⥤ V
f✝ : G ⟶ G'
ℌ' : DayConvolutionInternalHom F G' H'
c c' : C
f : c ⟶ c'
j : (multicospanShapeEnd C).L
⊢ H.map f ≫ ℌ.π c' j ≫ (ihom (F.obj j)).map (f✝.app (j ⊗ c')) =
    (ℌ.π c j ≫ (ihom (F.obj j)).map (f✝.app (j ⊗ c))) ≫ (ihom (F.obj j)).map (G'.map (j ◁ 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)
⊢ α.natTrans = β.natTrans

Tactic:
apply Functor.hom_ext_of_isLeftKanExtension
    (F ⊗ G).functor (η F G) _

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)
⊢ F.η G ≫ (tensor C).whiskerLeft α.natTrans = F.η G ≫ (tensor C).whiskerLeft β.natTrans
Module: Mathlib.CategoryTheory.Monoidal.Hopf_

Goal state before:
pp: case a.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 ⊗ₘ 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
| Δ

pp: case a.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
| A ◁ 𝒮

Tactic:
← IsMonHom.mul_hom

Goal state after:
case a.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

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.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
| A ◁ 𝒮
Module: Mathlib.CategoryTheory.MorphismProperty.LocalClosure

Goal state before:
pp: case 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
h : sourceLocalClosure K P f
⊢ ∃ R ∈ K.coverings X, ∀ (U : C) (g : U ⟶ X), R g → P (g ≫ f)

Tactic:
induction h with

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝³ : HasZeroMorphisms C
inst✝² : HasFiniteBiproducts C
o : HomOrthogonal s
α β : Type
inst✝¹ : Finite α
inst✝ : Finite β
f : α → ι
g : β → ι
z : (i : ι) → Matrix (↑(g ⁻¹' {i})) (↑(f ⁻¹' {i})) (End (s i))
⊢ (fun z i j k ↦ eqToHom ⋯ ≫ biproduct.components z ↑k ↑j ≫ eqToHom ⋯)
      ((fun z ↦ biproduct.matrix fun j k ↦ if h : f j = g k then z (f j) ⟨k, ⋯⟩ ⟨j, ⋯⟩ ≫ eqToHom ⋯ else 0) z) =
    z

Tactic:
by
    ext i ⟨j, w⟩ ⟨k, ⟨⟩⟩
    simp only [eqToHom_refl, biproduct.matrix_components, Category.id_comp]
    split_ifs with h
    · simp
    · exfalso
      exact h w.symm

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

Goal state before:
pp: case refine_1
κ : Cardinal.{u}
inst✝¹ : Fact κ.IsRegular
J : CardinalDirectedPoset κ
κ' : Cardinal.{u}
inst✝ : Fact κ'.IsRegular
hJ : HasCardinalLT (↑J.obj) κ'
h : κ ≤ κ'
A : Type u
x✝¹ : SmallCategory A
x✝ : IsCardinalFiltered A κ'
F : A ⥤ CardinalDirectedPoset κ
c : Cocone F
this✝ : IsFiltered A
this : IsCardinalFiltered A κ
hc : IsColimit ((forget (CardinalDirectedPoset κ)).mapCocone c)
f : ((coyoneda.obj (Opposite.op J)).mapCocone c).pt
⊢ ∃ i xi, f = (ConcreteCategory.hom (((coyoneda.obj (Opposite.op J)).mapCocone c).ι.app i)) xi

pp: case refine_2
κ : Cardinal.{u}
inst✝¹ : Fact κ.IsRegular
J : CardinalDirectedPoset κ
κ' : Cardinal.{u}
inst✝ : Fact κ'.IsRegular
hJ : HasCardinalLT (↑J.obj) κ'
h✝ : κ ≤ κ'
A : Type u
x✝¹ : SmallCategory A
x✝ : IsCardinalFiltered A κ'
F : A ⥤ CardinalDirectedPoset κ
c : Cocone F
this✝ : IsFiltered A
this : IsCardinalFiltered A κ
hc : IsColimit ((forget (CardinalDirectedPoset κ)).mapCocone c)
j : A
f g : (fun X ↦ X) ((F ⋙ coyoneda.obj (Opposite.op J)).obj j)
h :
  (ConcreteCategory.hom (((coyoneda.obj (Opposite.op J)).mapCocone c).ι.app j)) f =
    (ConcreteCategory.hom (((coyoneda.obj (Opposite.op J)).mapCocone c).ι.app j)) g
⊢ ∃ k f_1,
    (ConcreteCategory.hom ((F ⋙ coyoneda.obj (Opposite.op J)).map f_1)) f =
      (ConcreteCategory.hom ((F ⋙ coyoneda.obj (Opposite.op J)).map f_1)) g

Tactic:
· dsimp at f
      choose j g hg using fun (x : J.obj) ↦ Types.jointly_surjective_of_isColimit hc (f x)
      let m := IsCardinalFiltered.max j hJ
      let φ (x : J.obj) : (F.obj m).obj := F.map (IsCardinalFiltered.toMax j hJ x) (g x)
      have hφ (x : J.obj) : f x = c.ι.app _ (φ x) := by
        dsimp [φ]
        rw [← hg, ← ConcreteCategory.comp_apply, c.w]
        rfl
      refine ⟨m,
        ObjectProperty.homMk (PartOrdEmb.ofHom
          { toFun := φ
            inj' x y h := Hom.injective f (by simpa [hφ])
            map_rel_iff' {x y} := ?_ }), ?_⟩
      · simp [← Hom.le_iff_le f, hφ]
      · dsimp
        ext x
        trans c.ι.app (j x) (g x)
        · exact (hg x).symm
        · exact (ConcreteCategory.congr_hom (c.w (IsCardinalFiltered.toMax j hJ x)).symm (g x))

Goal state after:
case refine_2
κ : Cardinal.{u}
inst✝¹ : Fact κ.IsRegular
J : CardinalDirectedPoset κ
κ' : Cardinal.{u}
inst✝ : Fact κ'.IsRegular
hJ : HasCardinalLT (↑J.obj) κ'
h✝ : κ ≤ κ'
A : Type u
x✝¹ : SmallCategory A
x✝ : IsCardinalFiltered A κ'
F : A ⥤ CardinalDirectedPoset κ
c : Cocone F
this✝ : IsFiltered A
this : IsCardinalFiltered A κ
hc : IsColimit ((forget (CardinalDirectedPoset κ)).mapCocone c)
j : A
f g : (fun X ↦ X) ((F ⋙ coyoneda.obj (Opposite.op J)).obj j)
h :
  (ConcreteCategory.hom (((coyoneda.obj (Opposite.op J)).mapCocone c).ι.app j)) f =
    (ConcreteCategory.hom (((coyoneda.obj (Opposite.op J)).mapCocone c).ι.app j)) g
⊢ ∃ k f_1,
    (ConcreteCategory.hom ((F ⋙ coyoneda.obj (Opposite.op J)).map f_1)) f =
      (ConcreteCategory.hom ((F ⋙ coyoneda.obj (Opposite.op J)).map f_1)) g
Module: Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset

Goal state before:
pp: case none
κ : Cardinal.{u}
inst✝¹ : Fact κ.IsRegular
J : CardinalDirectedPoset κ
κ' : Cardinal.{u}
inst✝ : Fact κ'.IsRegular
⊢ ∃ S, J.PropSetWithTop κ' S ∧ none ∈ S

Tactic:
exact ⟨_, propSetWithTop_pair _ (Classical.arbitrary _), by aesop⟩

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

Goal state before:
pp: case refine_2
J : Type w
inst✝¹ : SmallCategory J
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
j x✝² : J
h₁ : __Diagram✝.P x✝²
x✝¹ x✝ : x✝² ⟶ j
h₂ : __Diagram✝.W x✝¹
h₃ : __Diagram✝.W x✝
⊢ x✝¹ = x✝

Tactic:
simp only [Diagram.single_P, ObjectProperty.singleton_iff] at h₁
      subst h₁
      obtain ⟨⟨⟩⟩ := h₂
      obtain ⟨⟨⟩⟩ := h₃
      simp

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

Goal state before:
pp: 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
⊢ Function.Bijective fun g ↦ f ≫ g

Tactic:
obtain ⟨_, _⟩ := hW f hf
    refine ⟨fun g₁ g₂ h ↦ ?_, fun g ↦ ?_⟩
    · obtain ⟨j₁, g₁, rfl⟩ := IsCardinalPresentable.exists_hom_of_isColimit κ p.isColimit g₁
      obtain ⟨j₂, g₂, rfl⟩ := IsCardinalPresentable.exists_hom_of_isColimit κ p.isColimit g₂
      dsimp at h ⊢
      obtain ⟨j₃, u, v, huv⟩ :=
        IsCardinalPresentable.exists_eq_of_isColimit κ p.isColimit (f ≫ g₁) (f ≫ g₂)
          (by simpa)
      simp only [Category.assoc] at huv
      rw [← p.w u, ← p.w v, reassoc_of% ((p.prop_diag_obj j₃ _ hf).1 huv)]
    · 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.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)
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m₀ : ι → J
t₀ : (i : ι) → (D i).top ⟶ m₀ i
hm₀ : ∀ (i : ι), IsEmpty (m₀ i ⟶ (D i).top)
m₁ : J := max m₀ hι
t₁ : (i : ι) → m₀ i ⟶ m₁ := fun i ↦ toMax m₀ hι i
u : (i : ι) → (D i).top ⟶ m₁ := fun i ↦ t₀ i ≫ t₁ i
S : Type (max 0 w) := { x // (D x.1).P x.2.2 ∧ (D x.2.1).P x.2.2 }
shape : MultispanShape :=
  { L := { x // (D x.1).P x.2.2 ∧ (D x.2.1).P x.2.2 }, R := PUnit.{w + 1}, fst := fun x ↦ PUnit.unit,
    snd := fun x ↦ PUnit.unit }
index : MultispanIndex shape J :=
  { left := fun x ↦ (↑x).2.2, right := fun x ↦ m₁, fst := fun x ↦ (D (↑x).1).isTerminal.lift ⋯ ≫ u (↑x).1,
    snd := fun x ↦ (D (↑x).2.1).isTerminal.lift ⋯ ≫ u (↑x).2.1 }
hκ : Cardinal.aleph0 ≤ κ
hL : HasCardinalLT shape.L κ
hR : HasCardinalLT shape.R κ
hshape : HasCardinalLT (Arrow (WalkingMultispan shape)) κ
c : Multicofork index := cocone index.multispan hshape
i₁ i₂ : ι
j : J
h₁ : (D i₁).P j
h₂ : (D i₂).P j
⊢ (D i₁).isTerminal.lift h₁ ≫ (fun i ↦ u i ≫ c.π PUnit.unit) i₁ =
    (D i₂).isTerminal.lift h₂ ≫ (fun i ↦ u i ≫ c.π PUnit.unit) i₂

Tactic:
by simpa [index, shape] using c.condition ⟨⟨i₁, i₂, j⟩, h₁, h₂⟩

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

Goal state before:
pp: case inl.inr
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
X Y : J
i✝ : Unit
⊢ (∃ a, (D a).P m) ∨ m = m

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)
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
X Y : J
i : ι
j : J
hj : (D i).P j
⊢ (∃ a, (D a).P ↑⟨i, ⟨j, hj⟩⟩.snd) ∨ m = ↑⟨i, ⟨j, hj⟩⟩.snd

Tactic:
· exact Or.inr rfl

Goal state after:
case inr
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
X Y : J
i : ι
j : J
hj : (D i).P j
⊢ (∃ a, (D a).P ↑⟨i, ⟨j, hj⟩⟩.snd) ∨ m = ↑⟨i, ⟨j, hj⟩⟩.snd
Module: Mathlib.CategoryTheory.Presentable.Directed

Goal state before:
pp: case inl.inr
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
X Y : J
i✝ : Unit
⊢ (∃ a, (D a).P m) ∨ m = m

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)
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
X Y : J
i : ι
j : J
hj : (D i).P j
⊢ (∃ a, (D a).P m) ∨ m = m

Tactic:
· exact Or.inr rfl

Goal state after:
case inr
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
X Y : J
i : ι
j : J
hj : (D i).P j
⊢ (∃ a, (D a).P m) ∨ m = m
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)
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
X Y : J
i : ι
j : J
hj : (D i).P j
⊢ (∃ a, (D a).P m) ∨ m = m

Tactic:
· exact Or.inr rfl

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
⊢ frobeniusMorphism f A' B' ≫ ((«exists» f).obj A' ⊓ B').arrow = (A' ⊓ (Subobject.pullback f).obj B').arrow ≫ f

Tactic:
rw [frobeniusMorphism, ← inf_comp_left, ← Category.assoc,
      (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.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:
h

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
h : EffectiveEpiFamily X π
⊢ Presieve.IsSheafFor P (Presieve.ofArrows X π)
Module: Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology

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

Tactic:
induction h with

Goal state after:
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
h : S ∈ (regularTopology C) X
⊢ ∃ Y π, EffectiveEpi π ∧ S.arrows π

Tactic:
induction h with

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

Goal state before:
pp: case refine_2
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : FinitaryPreExtensive C
inst✝ : FinitaryExtensive C
F : Cᵒᵖ ⥤ Type w
hF : PreservesFiniteProducts F
X : C
R : Presieve X
Y : Type
α : Finite Y
Z : Y → C
π : (a : Y) → Z a ⟶ X
hR : R = ofArrows Z π
hi : IsIso (Sigma.desc π)
this✝ : IsIso (Sigma.desc (Cofan.mk X π).inj)
this : R.Extensive
⊢ IsSheafFor F R

Tactic:
exact isSheafFor_extensive_of_preservesFiniteProducts R F

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

Goal state before:
pp: case refine_1
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preregular C
inst✝ : FinitaryPreExtensive C
B : C
S : Sieve B
h : S ∈ (extensiveCoverage C ⊔ regularCoverage C).toGrothendieck B
⊢ S ∈ (coherentTopology C) B

Tactic:
induction h with

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

Goal state before:
pp: case refine_2
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preregular C
inst✝ : FinitaryPreExtensive C
B : C
S : Sieve B
h : S ∈ (coherentTopology C) B
⊢ S ∈ (extensiveCoverage C ⊔ regularCoverage C).toGrothendieck B

Tactic:
induction h with

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : Cᵒᵖ ⥤ Type u_4
X B : C
π : X ⟶ B
inst✝ : EffectiveEpi π
c : PullbackCone π π
hP :
  ∀ (y : P.obj (op X)),
    (ConcreteCategory.hom (P.map c.fst.op)) y = (ConcreteCategory.hom (P.map c.snd.op)) y →
      ∃! x, (ConcreteCategory.hom (P.map π.op)) x = y
hc : IsLimit c
⊢ Function.Bijective ⇑(ConcreteCategory.hom (mapToEqualizer P π c.fst c.snd ⋯))

Tactic:
rw [Function.bijective_iff_existsUnique]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : Cᵒᵖ ⥤ Type u_4
X B : C
π : X ⟶ B
inst✝ : EffectiveEpi π
c : PullbackCone π π
hP :
  ∀ (y : P.obj (op X)),
    (ConcreteCategory.hom (P.map c.fst.op)) y = (ConcreteCategory.hom (P.map c.snd.op)) y →
      ∃! x, (ConcreteCategory.hom (P.map π.op)) x = y
hc : IsLimit c
⊢ ∀ (b : (fun X ↦ X) ↑{x | (ConcreteCategory.hom (P.map c.fst.op)) x = (ConcreteCategory.hom (P.map c.snd.op)) x}),
    ∃! a, (ConcreteCategory.hom (mapToEqualizer P π c.fst c.snd ⋯)) a = b
Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves

Goal state before:
pp: case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : Cᵒᵖ ⥤ Type u_4
X B : C
π : X ⟶ B
inst✝ : EffectiveEpi π
c : PullbackCone π π
hP :
  ∀ (y : P.obj (op X)),
    (ConcreteCategory.hom (P.map c.fst.op)) y = (ConcreteCategory.hom (P.map c.snd.op)) y →
      ∃! x, (ConcreteCategory.hom (P.map π.op)) x = y
hc : IsLimit c
b : P.obj (op X)
hb : b ∈ {x | (ConcreteCategory.hom (P.map c.fst.op)) x = (ConcreteCategory.hom (P.map c.snd.op)) x}
a : P.obj (op B)
ha₁ : (ConcreteCategory.hom (P.map π.op)) a = b
ha₂ : ∀ (y : P.obj (op B)), (fun x ↦ (ConcreteCategory.hom (P.map π.op)) x = b) y → y = a
y : P.obj (op B)
⊢ (fun a ↦ (ConcreteCategory.hom (mapToEqualizer P π c.fst c.snd ⋯)) a = ⟨b, hb⟩) y → y = a

Tactic:
h

Goal state after:
case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : Cᵒᵖ ⥤ Type u_4
X B : C
π : X ⟶ B
inst✝ : EffectiveEpi π
c : PullbackCone π π
hP :
  ∀ (y : P.obj (op X)),
    (ConcreteCategory.hom (P.map c.fst.op)) y = (ConcreteCategory.hom (P.map c.snd.op)) y →
      ∃! x, (ConcreteCategory.hom (P.map π.op)) x = y
hc : IsLimit c
b : P.obj (op X)
hb : b ∈ {x | (ConcreteCategory.hom (P.map c.fst.op)) x = (ConcreteCategory.hom (P.map c.snd.op)) x}
a : P.obj (op B)
ha₁ : (ConcreteCategory.hom (P.map π.op)) a = b
ha₂ : ∀ (y : P.obj (op B)), (fun x ↦ (ConcreteCategory.hom (P.map π.op)) x = b) y → y = a
y : P.obj (op B)
h : (ConcreteCategory.hom (mapToEqualizer P π c.fst c.snd ⋯)) y = ⟨b, hb⟩
⊢ y = a
Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveTopology

Goal state before:
pp: case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : FinitaryPreExtensive C
X : C
S : Sieve X
h : S ∈ (extensiveTopology C) X
⊢ ∃ α, ∃ (_ : Finite α), ∃ Y π, Nonempty (IsColimit (Cofan.mk X π)) ∧ ∀ (a : α), S.arrows (π a)

Tactic:
induction h with

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

Goal state before:
pp: case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : Cᵒᵖ ⥤ Type u_4
X B : C
π : X ⟶ B
inst✝ : EffectiveEpi π
c : PullbackCone π π
hP :
  ∀ (b : (fun X ↦ X) ↑{x | (ConcreteCategory.hom (P.map c.fst.op)) x = (ConcreteCategory.hom (P.map c.snd.op)) x}),
    ∃! a, (ConcreteCategory.hom (mapToEqualizer P π c.fst c.snd ⋯)) a = b
hc : IsLimit c
b : P.obj (op X)
hb : (ConcreteCategory.hom (P.map c.fst.op)) b = (ConcreteCategory.hom (P.map c.snd.op)) b
a : P.obj (op B)
ha₁ : (ConcreteCategory.hom (mapToEqualizer P π c.fst c.snd ⋯)) a = ⟨b, hb⟩
ha₂ :
  ∀ (y : (fun X ↦ X) (P.obj (op B))),
    (fun a ↦ (ConcreteCategory.hom (mapToEqualizer P π c.fst c.snd ⋯)) a = ⟨b, hb⟩) y → y = a
y : P.obj (op B)
⊢ (fun x ↦ (ConcreteCategory.hom (P.map π.op)) x = b) y → y = a

Tactic:
h

Goal state after:
case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : Cᵒᵖ ⥤ Type u_4
X B : C
π : X ⟶ B
inst✝ : EffectiveEpi π
c : PullbackCone π π
hP :
  ∀ (b : (fun X ↦ X) ↑{x | (ConcreteCategory.hom (P.map c.fst.op)) x = (ConcreteCategory.hom (P.map c.snd.op)) x}),
    ∃! a, (ConcreteCategory.hom (mapToEqualizer P π c.fst c.snd ⋯)) a = b
hc : IsLimit c
b : P.obj (op X)
hb : (ConcreteCategory.hom (P.map c.fst.op)) b = (ConcreteCategory.hom (P.map c.snd.op)) b
a : P.obj (op B)
ha₁ : (ConcreteCategory.hom (mapToEqualizer P π c.fst c.snd ⋯)) a = ⟨b, hb⟩
ha₂ :
  ∀ (y : (fun X ↦ X) (P.obj (op B))),
    (fun a ↦ (ConcreteCategory.hom (mapToEqualizer P π c.fst c.snd ⋯)) a = ⟨b, hb⟩) y → y = a
y : P.obj (op B)
h : (ConcreteCategory.hom (P.map π.op)) y = b
⊢ y = a
Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
X : C
S : Presieve X
inst✝¹ : S.regular
inst✝ : Projective X
F : Cᵒᵖ ⥤ Type u_4
⊢ IsSheafFor F S

Tactic:
obtain ⟨Y, f, rfl, hf⟩ := Presieve.regular.single_epi (R := S)

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
X : C
inst✝¹ : Projective X
F : Cᵒᵖ ⥤ Type u_4
Y : C
f : Y ⟶ X
hf : EffectiveEpi f
inst✝ : (ofArrows (fun x ↦ Y) fun x ↦ f).regular
⊢ IsSheafFor F (ofArrows (fun x ↦ Y) fun x ↦ f)