mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Basic

Goal state before:
pp: case e_a
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
inst✝³ : MonoidalClosed C
J : Type u₂
inst✝² : Category.{v₂, u₂} J
inst✝¹ : ∀ (F₁ F₂ : J ⥤ C), HasFunctorEnrichedHom C F₁ F₂
F₁ F₂ F₃ F₃' : J ⥤ C
inst✝ : ∀ (F₁ F₂ : J ⥤ C), HasEnrichedHom C F₁ F₂
f : F₁ ⊗ F₂ ⟶ F₃
f₃ : F₃ ⟶ F₃'
j : J
k : Under j
⊢ (ρ_ ((ihom (F₁.obj k.right)).obj (F₃.obj k.right))).inv ≫
      (ihom (F₁.obj k.right)).obj (F₃.obj k.right) ◁ (eHomEquiv C) (f₃.app k.right) ≫
        eComp C (F₁.obj k.right) (F₃.obj k.right) (F₃'.obj k.right) =
    (ihom (F₁.obj k.right)).map (f₃.app k.right)

Tactic:
apply enrichedOrdinaryCategorySelf_eHomWhiskerLeft

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Closed.Ideal

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Reflective i
inst✝³ : MonoidalClosed C
inst✝² : CartesianMonoidalCategory D
inst✝¹ : ExponentialIdeal i
inst✝ : BraidedCategory C
A B : C
⊢ prodComparison (reflector i) A B ≫ (bijection i A B ((reflector i).obj (A ⊗ B))) (𝟙 ((reflector i).obj (A ⊗ B))) =
    𝟙 ((reflector i).obj (A ⊗ B))

Tactic:
by
      rw [← (bijection i _ _ _).injective.eq_iff, bijection_natural, ← bijection_symm_apply_id,
        Equiv.apply_symm_apply, Category.id_comp]

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 G : C ⥤ V
inst✝ : DayConvolution F G
ℌ : DayConvolutionInternalHom F (F ⊛ G) H
c c' c'' : C
f : c' ⟶ c''
⊢ MonoidalClosed.curry ((DayConvolution.unit F G).app (c', c)) ≫
      ((((dayConvolutionInternalHomDiagramFunctor F).obj (F ⊛ G)).obj c).obj (op c')).map f =
    MonoidalClosed.curry ((DayConvolution.unit F G).app (c'', c)) ≫
      ((((dayConvolutionInternalHomDiagramFunctor F).obj (F ⊛ G)).obj c).map f.op).app c''

Tactic:
have := DayConvolution.unit_naturality F G f (𝟙 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 G : C ⥤ V
inst✝ : DayConvolution F G
ℌ : DayConvolutionInternalHom F (F ⊛ G) H
c c' c'' : C
f : c' ⟶ c''
this :
  (F.map f ⊗ₘ G.map (𝟙 c)) ≫ (DayConvolution.unit F G).app (c'', c) =
    (DayConvolution.unit F G).app (c', c) ≫ (F ⊛ G).map (f ⊗ₘ 𝟙 c)
⊢ MonoidalClosed.curry ((DayConvolution.unit F G).app (c', c)) ≫
      ((((dayConvolutionInternalHomDiagramFunctor F).obj (F ⊛ G)).obj c).obj (op c')).map f =
    MonoidalClosed.curry ((DayConvolution.unit F G).app (c'', c)) ≫
      ((((dayConvolutionInternalHomDiagramFunctor F).obj (F ⊛ G)).obj c).map f.op).app c''
Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence

Goal state before:
pp: C : Type u
X Y : F C
n : (Discrete ∘ NormalMonoidalObject) C
⊢ (α_ (inclusion.obj { as := n.as }) X Y).symm ≪≫
      normalizeIsoApp' C X n.as ▷ᵢ Y ≪≫ normalizeIsoApp C Y { as := X.normalizeObj n.as } =
    (α_ (inclusionObj n.as) X Y).symm ≪≫ normalizeIsoApp' C X n.as ▷ᵢ Y ≪≫ normalizeIsoApp' C Y (X.normalizeObj n.as)

Tactic:
normalizeIsoApp_eq Y ⟨normalizeObj X n.as⟩

Goal state after:
C : Type u
X Y : F C
n : (Discrete ∘ NormalMonoidalObject) C
⊢ (α_ (inclusion.obj { as := n.as }) X Y).symm ≪≫
      normalizeIsoApp' C X n.as ▷ᵢ Y ≪≫ normalizeIsoApp' C Y { as := X.normalizeObj n.as }.as =
    (α_ (inclusionObj n.as) X Y).symm ≪≫ normalizeIsoApp' C X n.as ▷ᵢ Y ≪≫ normalizeIsoApp' C Y (X.normalizeObj n.as)
Module: Mathlib.CategoryTheory.Monoidal.Limits.Cokernels

Goal state before:
pp: C : Type u_1
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Preadditive C
inst✝⁵ : MonoidalCategory C
inst✝⁴ : MonoidalPreadditive C
X₁ Y₁ : C
f₁ : X₁ ⟶ Y₁
c₁ : CokernelCofork f₁
hc₁ : IsColimit c₁
X₂ Y₂ : C
f₂ : X₂ ⟶ Y₂
c₂ : CokernelCofork f₂
hc₂ : IsColimit c₂
inst✝³ : HasBinaryCoproduct (X₁ ⊗ Y₂) (Y₁ ⊗ X₂)
inst✝² : PreservesColimit (parallelPair f₂ 0) (tensorLeft c₁.pt)
inst✝¹ : PreservesColimit (parallelPair f₁ 0) (tensorRight Y₂)
inst✝ : PreservesColimit (parallelPair f₁ 0) (tensorRight X₂)
⊢ HasBinaryCoproduct (((curriedTensor C).obj X₁).obj Y₂) (((curriedTensor C).obj Y₁).obj X₂)

Tactic:
by assumption

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 (𝟙_ C)).hom ≫ η_ X Y ▷ X) ⊗≫ ((β_ (Y ⊗ X) X).inv ≫ ε_ X Y ▷ X) ⊗≫ 𝟙 X = 𝟙 X

Tactic:
← 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.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.of_iso
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✝ X'✝ Y'✝ : C
f : X✝ ⟶ Y✝
g : X'✝ ⟶ Y'✝
e : Arrow.mk f ≅ Arrow.mk g
hf : sourceLocalClosure K P f
h : ∃ R ∈ K.coverings X✝, ∀ (U : C) (g : U ⟶ X✝), R g → P (g ≫ f)
⊢ ∃ R ∈ K.coverings X'✝, ∀ (U : C) (g_1 : U ⟶ X'✝), R g_1 → P (g_1 ≫ g)

Tactic:
| of_iso f g e hf h =>

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
D : Type u₃
inst✝⁵ : Category.{v₃, u₃} D
inst✝⁴ : InducedLawfulDayConvolutionMonoidalCategoryStructCore C V D
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) (tensorRight v)
inst✝ :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorLeft v)
d₁ d₁' d₂ d₂' : D
f : d₁ ⟶ d₂
f' : d₁' ⟶ d₂'
⊢ (tensorObjIsoConvolution C V d₁ d₁').hom ≫
      DayConvolution.map ((ι C V D).map f) ((ι C V D).map f') ≫ (tensorObjIsoConvolution C V d₂ d₂').inv =
    DayConvolution.map ((ι C V D).map f) ((ι C V D).map f')

Tactic:
apply (convolutions C V d₁ d₁').corepresentableBy.homEquiv.injective

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
D : Type u₃
inst✝⁵ : Category.{v₃, u₃} D
inst✝⁴ : InducedLawfulDayConvolutionMonoidalCategoryStructCore C V D
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) (tensorRight v)
inst✝ :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorLeft v)
d₁ d₁' d₂ d₂' : D
f : d₁ ⟶ d₂
f' : d₁' ⟶ d₂'
⊢ (DayConvolution.corepresentableBy ((ι C V D).obj d₁) ((ι C V D).obj d₁')).homEquiv
      ((tensorObjIsoConvolution C V d₁ d₁').hom ≫
        DayConvolution.map ((ι C V D).map f) ((ι C V D).map f') ≫ (tensorObjIsoConvolution C V d₂ d₂').inv) =
    (DayConvolution.corepresentableBy ((ι C V D).obj d₁) ((ι C V D).obj d₁')).homEquiv
      (DayConvolution.map ((ι C V D).map f) ((ι C V D).map f'))
Module: Mathlib.CategoryTheory.MorphismProperty.LocalEpi

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝¹ : G.Faithful
inst✝ : G.Full
⊢ G.essImage.localEpi = (MorphismProperty.epimorphisms D).inverseImage F

Tactic:
by
  rw [← Functor.isoClosure_eq_essImage, localEpi_isoClosure,
    localEpi_mem_range_eq_inverseImage_epimorphisms adj]

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:
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.Order.Category.PartOrdEmb

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

Tactic:
have hx := ConcreteCategory.congr_hom (hc.fac ((forget _).mapCocone s) j) x'

Goal state after:
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ PartOrdEmb
c : Cocone (F ⋙ forget PartOrdEmb)
hc : IsColimit c
s : Cocone F
j : J
x' y' : (F ⋙ forget PartOrdEmb).obj j
hx :
  (ConcreteCategory.hom (c.ι.app j ≫ hc.desc ((forget PartOrdEmb).mapCocone s))) x' =
    (ConcreteCategory.hom (((forget PartOrdEmb).mapCocone s).ι.app j)) x'
⊢ { 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.OrthogonalReflection

Goal state before:
pp: case refine_1
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₁ g₂ : Y ⟶ Z
h : (fun g ↦ f ≫ g) g₁ = (fun g ↦ f ≫ g) g₂
⊢ g₁ = g₂

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 ⟨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)]

Goal state after:
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
Module: Mathlib.CategoryTheory.Presentable.Type

Goal state before:
pp: case refine_2
X : Type u
κ : Cardinal.{u}
hκ : Cardinal.aleph0 ≤ κ
this : IsFiltered (HasCardinalLT.Set X κ)
⊢ ∀ (i : HasCardinalLT.Set X κ) (x y : (fun X ↦ X) ((functor X κ).obj i)),
    (hom ((cocone X κ).ι.app i)) x = (hom ((cocone X κ).ι.app i)) y →
      ∃ k f, (hom ((functor X κ).map f)) x = (hom ((functor X κ).map f)) y

Tactic:
· rintro A ⟨x, hx⟩ ⟨y, hy⟩ rfl
    exact ⟨A, 𝟙 _, rfl⟩

Goal state after:
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
⊢ (Function.Bijective fun f ↦ (ConcreteCategory.hom (F.map f.op)) x) ↔
    Function.Bijective ⇑(ConcreteCategory.hom ((uliftYonedaEquiv.symm { down := x }).app (op Y)))

Tactic:
← Function.Bijective.of_comp_iff _ Equiv.ulift.{w}.symm.bijective,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
X : C
x : F.obj (op X)
Y : C
⊢ (Function.Bijective fun f ↦ (ConcreteCategory.hom (F.map f.op)) x) ↔
    Function.Bijective (⇑(ConcreteCategory.hom ((uliftYonedaEquiv.symm { down := x }).app (op Y))) ∘ ⇑Equiv.ulift.symm)
Module: Mathlib.CategoryTheory.Sites.Coherent.CoherentSheaves

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Precoherent C
W X : C
α : Type
inst✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
H : EffectiveEpiFamily Y π
h_colim : Limits.IsColimit (Sieve.generate (Presieve.ofArrows Y π)).arrows.cocone
x : Presieve.FamilyOfElements (yoneda.obj W) (Presieve.ofArrows Y π)
hx : x.Compatible
x_ext : Presieve.FamilyOfElements (yoneda.obj W) (Sieve.generate (Presieve.ofArrows Y π)).arrows := x.sieveExtend
hx_ext : x.sieveExtend.Compatible
S : Sieve X := Sieve.generate (Presieve.ofArrows Y π)
t : (yoneda.obj W).obj (Opposite.op X)
t_amalg : x_ext.IsAmalgamation t
t_uniq : ∀ (y : (yoneda.obj W).obj (Opposite.op X)), (fun t ↦ x_ext.IsAmalgamation t) y → y = t
⊢ ∃! t, x.IsAmalgamation t

Tactic:
refine ⟨t, ?_, ?_⟩

Goal state after:
case refine_1
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Precoherent C
W X : C
α : Type
inst✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
H : EffectiveEpiFamily Y π
h_colim : Limits.IsColimit (Sieve.generate (Presieve.ofArrows Y π)).arrows.cocone
x : Presieve.FamilyOfElements (yoneda.obj W) (Presieve.ofArrows Y π)
hx : x.Compatible
x_ext : Presieve.FamilyOfElements (yoneda.obj W) (Sieve.generate (Presieve.ofArrows Y π)).arrows := x.sieveExtend
hx_ext : x.sieveExtend.Compatible
S : Sieve X := Sieve.generate (Presieve.ofArrows Y π)
t : (yoneda.obj W).obj (Opposite.op X)
t_amalg : x_ext.IsAmalgamation t
t_uniq : ∀ (y : (yoneda.obj W).obj (Opposite.op X)), (fun t ↦ x_ext.IsAmalgamation t) y → y = t
⊢ (fun t ↦ x.IsAmalgamation t) t

case refine_2
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Precoherent C
W X : C
α : Type
inst✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
H : EffectiveEpiFamily Y π
h_colim : Limits.IsColimit (Sieve.generate (Presieve.ofArrows Y π)).arrows.cocone
x : Presieve.FamilyOfElements (yoneda.obj W) (Presieve.ofArrows Y π)
hx : x.Compatible
x_ext : Presieve.FamilyOfElements (yoneda.obj W) (Sieve.generate (Presieve.ofArrows Y π)).arrows := x.sieveExtend
hx_ext : x.sieveExtend.Compatible
S : Sieve X := Sieve.generate (Presieve.ofArrows Y π)
t : (yoneda.obj W).obj (Opposite.op X)
t_amalg : x_ext.IsAmalgamation t
t_uniq : ∀ (y : (yoneda.obj W).obj (Opposite.op X)), (fun t ↦ x_ext.IsAmalgamation t) y → y = t
⊢ ∀ (y : (yoneda.obj W).obj (Opposite.op X)), (fun t ↦ x.IsAmalgamation t) y → y = t
Module: Mathlib.CategoryTheory.Sites.Coherent.RegularTopology

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preregular C
X : C
S : Sieve X
Y : C
π : Y ⟶ X
h : EffectiveEpi π ∧ S.arrows π
⊢ Sieve.generate (Presieve.ofArrows (fun x ↦ Y) fun x ↦ π) ≤ S

Tactic:
Sieve.generate_le_iff (Presieve.ofArrows _ _) S

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preregular C
X : C
S : Sieve X
Y : C
π : Y ⟶ X
h : EffectiveEpi π ∧ S.arrows π
⊢ (Presieve.ofArrows (fun x ↦ Y) fun x ↦ π) ≤ S.arrows
Module: Mathlib.CategoryTheory.Sites.Coherent.RegularTopology

Goal state before:
pp: 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 π'
⊢ EffectiveEpi (π' ≫ π)

Tactic:
by
  rw [effectiveEpi_iff_effectiveEpiFamily, ← Sieve.effectiveEpimorphic_family]
  suffices h₂ : (Sieve.generate (Presieve.ofArrows _ _)) ∈ (regularTopology C) X by
    change Nonempty _
    rw [← Sieve.forallYonedaIsSheaf_iff_colimit]
    exact fun W => regularTopology.isSheaf_yoneda_obj W _ h₂
  apply Coverage.Saturate.transitive X (Sieve.generate (Presieve.ofArrows (fun () ↦ Y)
      (fun () ↦ π)))
  · apply Coverage.Saturate.of
    use Y, π
  · intro V f ⟨Y₁, h, g, ⟨hY, hf⟩⟩
    rw [← hf, Sieve.pullback_comp]
    apply (regularTopology C).pullback_stable'
    apply regularTopology.mem_sieves_of_hasEffectiveEpi
    cases hY
    exact ⟨Y', π', inferInstance, Y', (𝟙 _), π' ≫ π, Presieve.ofArrows.mk (), (by simp)⟩

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

Goal state before:
pp: case refine_1.of
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preregular C
inst✝ : FinitaryPreExtensive C
B : C
S : Sieve B
Y : C
T : Presieve Y
hT : T ∈ (extensiveCoverage C ⊔ regularCoverage C).coverings Y
⊢ T ∈ (coherentCoverage C).coverings Y

Tactic:
simp only [Coverage.sup_covering, Set.mem_union] at hT

Goal state after:
case refine_1.of
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preregular C
inst✝ : FinitaryPreExtensive C
B : C
S : Sieve B
Y : C
T : Presieve Y
hT : T ∈ (extensiveCoverage C).coverings Y ∨ T ∈ (regularCoverage C).coverings Y
⊢ T ∈ (coherentCoverage C).coverings Y
Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison

Goal state before:
pp: case refine_2.refine_2
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
X : C
S : Sieve X
hS : Sieve.functorPushforward F S ∈ (regularTopology D) (F.obj X)
Y : D
π : Y ⟶ F.obj X
H₁ : EffectiveEpi π
H₂ : (Sieve.functorPushforward F S).arrows π
g₀ : F.effectiveEpiOverObj Y ⟶ Y := F.effectiveEpiOver Y
⊢ S.arrows (F.preimage (g₀ ≫ π))

Tactic:
· obtain ⟨W, g₁, g₂, h₁, h₂⟩ := H₂
      rw [h₂]
      convert! S.downward_closed h₁ (F.preimage (g₀ ≫ g₂))
      exact F.map_injective (by simp)

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preregular C
W X w✝ Y : C
f : Y ⟶ X
hf : EffectiveEpi f
hS : ∃ f_1, ((ofArrows (fun x ↦ Y) fun x ↦ f) = ofArrows (fun x ↦ w✝) fun x ↦ f_1) ∧ EffectiveEpi f_1
this : (ofArrows (fun x ↦ Y) fun x ↦ f).regular
h_colim : IsColimit (Sieve.generate (ofArrows (fun x ↦ Y) fun x ↦ f)).arrows.cocone
x : FamilyOfElements (yoneda.obj W) (ofArrows (fun x ↦ Y) fun x ↦ f)
hx : x.Compatible
x_ext : FamilyOfElements (yoneda.obj W) (Sieve.generate (ofArrows (fun x ↦ Y) fun x ↦ f)).arrows := x.sieveExtend
hx_ext : x.sieveExtend.Compatible
S : Sieve X := Sieve.generate (ofArrows (fun x ↦ Y) fun x ↦ f)
t : (yoneda.obj W).obj (op X)
t_amalg : x_ext.IsAmalgamation t
t_uniq : ∀ (y : (yoneda.obj W).obj (op X)), (fun t ↦ x_ext.IsAmalgamation t) y → y = t
⊢ ∃! t, x.IsAmalgamation t

Tactic:
refine ⟨t, ?_, ?_⟩

Goal state after:
case refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preregular C
W X w✝ Y : C
f : Y ⟶ X
hf : EffectiveEpi f
hS : ∃ f_1, ((ofArrows (fun x ↦ Y) fun x ↦ f) = ofArrows (fun x ↦ w✝) fun x ↦ f_1) ∧ EffectiveEpi f_1
this : (ofArrows (fun x ↦ Y) fun x ↦ f).regular
h_colim : IsColimit (Sieve.generate (ofArrows (fun x ↦ Y) fun x ↦ f)).arrows.cocone
x : FamilyOfElements (yoneda.obj W) (ofArrows (fun x ↦ Y) fun x ↦ f)
hx : x.Compatible
x_ext : FamilyOfElements (yoneda.obj W) (Sieve.generate (ofArrows (fun x ↦ Y) fun x ↦ f)).arrows := x.sieveExtend
hx_ext : x.sieveExtend.Compatible
S : Sieve X := Sieve.generate (ofArrows (fun x ↦ Y) fun x ↦ f)
t : (yoneda.obj W).obj (op X)
t_amalg : x_ext.IsAmalgamation t
t_uniq : ∀ (y : (yoneda.obj W).obj (op X)), (fun t ↦ x_ext.IsAmalgamation t) y → y = t
⊢ (fun t ↦ x.IsAmalgamation t) t

case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preregular C
W X w✝ Y : C
f : Y ⟶ X
hf : EffectiveEpi f
hS : ∃ f_1, ((ofArrows (fun x ↦ Y) fun x ↦ f) = ofArrows (fun x ↦ w✝) fun x ↦ f_1) ∧ EffectiveEpi f_1
this : (ofArrows (fun x ↦ Y) fun x ↦ f).regular
h_colim : IsColimit (Sieve.generate (ofArrows (fun x ↦ Y) fun x ↦ f)).arrows.cocone
x : FamilyOfElements (yoneda.obj W) (ofArrows (fun x ↦ Y) fun x ↦ f)
hx : x.Compatible
x_ext : FamilyOfElements (yoneda.obj W) (Sieve.generate (ofArrows (fun x ↦ Y) fun x ↦ f)).arrows := x.sieveExtend
hx_ext : x.sieveExtend.Compatible
S : Sieve X := Sieve.generate (ofArrows (fun x ↦ Y) fun x ↦ f)
t : (yoneda.obj W).obj (op X)
t_amalg : x_ext.IsAmalgamation t
t_uniq : ∀ (y : (yoneda.obj W).obj (op X)), (fun t ↦ x_ext.IsAmalgamation t) y → y = t
⊢ ∀ (y : (yoneda.obj W).obj (op X)), (fun t ↦ x.IsAmalgamation t) y → y = t