mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Category.TopCat.Limits.Products

Goal state before:
pp: case e'_5
X Y : TopCat
c : BinaryCofan X Y
h₁ : IsOpenEmbedding ⇑(ConcreteCategory.hom c.inl)
h₂ : IsOpenEmbedding ⇑(ConcreteCategory.hom c.inr)
h₃ : IsCompl (range ⇑(ConcreteCategory.hom c.inl)) (range ⇑(ConcreteCategory.hom c.inr))
this✝ :
  ∀ (x : ↑(((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ range ⇑(ConcreteCategory.hom c.inl) ∨ x ∈ range ⇑(ConcreteCategory.hom c.inr)
T : TopCat
f : X ⟶ T
g : Y ⟶ T
this : ∀ a ∉ range ⇑(ConcreteCategory.hom c.inl), a ∈ range ⇑(ConcreteCategory.hom c.inr)
e_1✝ : ↑(range ⇑(ConcreteCategory.hom c.inl))ᶜ = { a // a ∉ range ⇑(ConcreteCategory.hom c.inl) }
⊢ ((range ⇑(ConcreteCategory.hom c.inl))ᶜ.domRestrict fun x ↦
      if h : x ∈ range ⇑(ConcreteCategory.hom c.inl) then
        (ConcreteCategory.hom f) ((Equiv.ofInjective ⇑(ConcreteCategory.hom c.inl) ⋯).symm ⟨x, ⋯⟩)
      else (ConcreteCategory.hom g) ((Equiv.ofInjective ⇑(ConcreteCategory.hom c.inr) ⋯).symm ⟨x, ⋯⟩)) =
    ⇑(ConcreteCategory.hom g) ∘ ⇑⋯.toHomeomorph.symm ∘ Subtype.map (fun a ↦ a) this

Tactic:
ext ⟨x, hx⟩

Goal state after:
case e'_5
X Y : TopCat
c : BinaryCofan X Y
h₁ : IsOpenEmbedding ⇑(ConcreteCategory.hom c.inl)
h₂ : IsOpenEmbedding ⇑(ConcreteCategory.hom c.inr)
h₃ : IsCompl (range ⇑(ConcreteCategory.hom c.inl)) (range ⇑(ConcreteCategory.hom c.inr))
this✝ :
  ∀ (x : ↑(((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ range ⇑(ConcreteCategory.hom c.inl) ∨ x ∈ range ⇑(ConcreteCategory.hom c.inr)
T : TopCat
f : X ⟶ T
g : Y ⟶ T
this : ∀ a ∉ range ⇑(ConcreteCategory.hom c.inl), a ∈ range ⇑(ConcreteCategory.hom c.inr)
e_1✝ : ↑(range ⇑(ConcreteCategory.hom c.inl))ᶜ = { a // a ∉ range ⇑(ConcreteCategory.hom c.inl) }
x : ↑c.1
hx : x ∈ (range ⇑(ConcreteCategory.hom c.inl))ᶜ
⊢ (range ⇑(ConcreteCategory.hom c.inl))ᶜ.domRestrict
      (fun x ↦
        if h : x ∈ range ⇑(ConcreteCategory.hom c.inl) then
          (ConcreteCategory.hom f) ((Equiv.ofInjective ⇑(ConcreteCategory.hom c.inl) ⋯).symm ⟨x, ⋯⟩)
        else (ConcreteCategory.hom g) ((Equiv.ofInjective ⇑(ConcreteCategory.hom c.inr) ⋯).symm ⟨x, ⋯⟩))
      ⟨x, hx⟩ =
    (⇑(ConcreteCategory.hom g) ∘ ⇑⋯.toHomeomorph.symm ∘ Subtype.map (fun a ↦ a) this) ⟨x, hx⟩
Module: Mathlib.CategoryTheory.Limits.MonoCoprod

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
I₁ : Type u_2
I₂ : Type u_3
X : I₁ ⊕ I₂ → C
c : Cofan X
c₁ : Cofan (X ∘ Sum.inl)
c₂ : Cofan (X ∘ Sum.inr)
hc : IsColimit c
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
inst✝ : MonoCoprod C
inr : c₂.pt ⟶ c.pt
hinr : ∀ (i₂ : I₂), c₂.inj i₂ ≫ inr = c.inj (Sum.inr i₂)
this : inr = (binaryCofanSum c c₁ c₂ hc₁ hc₂).inr
⊢ Mono (binaryCofanSum c c₁ c₂ hc₁ hc₂).inr

Tactic:
exact MonoCoprod.binaryCofan_inr _ (isColimitBinaryCofanSum c c₁ c₂ hc hc₁ hc₂)

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

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H : IsPushout f g h i
H' : H.IsVanKampen
X' Y' : C
⊢ ∀ ⦃Z' : C⦄ (h' : X' ⟶ Z') (i' : Y' ⟶ Z') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (αZ : Z' ⟶ Z),
    CommSq h' αX αZ h →
      CommSq i' αY αZ i →
        ∀ [HasPullback αX f],
          IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i ↔
            ∃ W' f' g' αW, IsPullback f' αW αX f ∧ IsPullback g' αW αY g ∧ IsPushout f' g' h' i'

Tactic:
Z'

Goal state after:
case mp
C : Type u
inst✝ : Category.{v, u} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H : IsPushout f g h i
H' : H.IsVanKampen
X' Y' Z' : C
⊢ ∀ (h' : X' ⟶ Z') (i' : Y' ⟶ Z') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (αZ : Z' ⟶ Z),
    CommSq h' αX αZ h →
      CommSq i' αY αZ i →
        ∀ [HasPullback αX f],
          IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i ↔
            ∃ W' f' g' αW, IsPullback f' αW αX f ∧ IsPullback g' αW αY g ∧ IsPushout f' g' h' i'
Module: Mathlib.CategoryTheory.Adhesive.Basic

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H : IsPushout f g h i
H' :
  ∀ ⦃X' Y' Z' : C⦄ (h' : X' ⟶ Z') (i' : Y' ⟶ Z') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (αZ : Z' ⟶ Z),
    CommSq h' αX αZ h →
      CommSq i' αY αZ i →
        ∀ [HasPullback αX f],
          IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i ↔
            ∃ W' f' g' αW, IsPullback f' αW αX f ∧ IsPullback g' αW αY g ∧ IsPushout f' g' h' i'
W' X' Y' : C
⊢ ∀ ⦃Z' : C⦄ (f' : W' ⟶ X') (g' : W' ⟶ Y') (h' : X' ⟶ Z') (i' : Y' ⟶ Z') (αW : W' ⟶ W) (αX : X' ⟶ X) (αY : Y' ⟶ Y)
    (αZ : Z' ⟶ Z),
    IsPullback f' αW αX f →
      IsPullback g' αW αY g →
        CommSq h' αX αZ h →
          CommSq i' αY αZ i →
            CommSq f' g' h' i' → (IsPushout f' g' h' i' ↔ IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i)

Tactic:
Z'

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H : IsPushout f g h i
H' :
  ∀ ⦃X' Y' Z' : C⦄ (h' : X' ⟶ Z') (i' : Y' ⟶ Z') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (αZ : Z' ⟶ Z),
    CommSq h' αX αZ h →
      CommSq i' αY αZ i →
        ∀ [HasPullback αX f],
          IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i ↔
            ∃ W' f' g' αW, IsPullback f' αW αX f ∧ IsPullback g' αW αY g ∧ IsPushout f' g' h' i'
W' X' Y' Z' : C
⊢ ∀ (f' : W' ⟶ X') (g' : W' ⟶ Y') (h' : X' ⟶ Z') (i' : Y' ⟶ Z') (αW : W' ⟶ W) (αX : X' ⟶ X) (αY : Y' ⟶ Y) (αZ : Z' ⟶ Z),
    IsPullback f' αW αX f →
      IsPullback g' αW αY g →
        CommSq h' αX αZ h →
          CommSq i' αY αZ i →
            CommSq f' g' h' i' → (IsPushout f' g' h' i' ↔ IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i)
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: case h₁
J : Type v'
inst✝⁶ : Category.{u', v'} J
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_2
inst✝⁴ : Category.{v_2, u_2} D
Gl : C ⥤ D
Gr : D ⥤ C
adj : Gl ⊣ Gr
inst✝³ : Gr.Full
inst✝² : Gr.Faithful
F : J ⥤ D
c : Cocone (F ⋙ Gr)
H : IsUniversalColimit c
inst✝¹ : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), HasPullback (Gr.map f) (adj.unit.app c.pt)
inst✝ : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), PreservesLimit (cospan (Gr.map f) (adj.unit.app c.pt)) Gl
this✝² : PreservesLimitsOfSize.{?u.146, ?u.145, v_2, v, u_2, u} Gr
this✝¹ : PreservesColimitsOfSize.{u', v', v, v_2, u, u_2} Gl
F' : J ⥤ D
c' : Cocone F'
α : F' ⟶ (F ⋙ Gr) ⋙ Gl
f : c'.pt ⟶ (Gl.mapCocone c).pt
h : α ≫ (Gl.mapCocone c).ι = c'.ι ≫ (const J).map f
hα : NatTrans.Equifibered α
hc' : ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f ((Gl.mapCocone c).ι.app j)
this✝ : HasPullback (Gl.map (Gr.map f)) (Gl.map (adj.unit.app c.pt))
α' : F' ⟶ F := α ≫ (F.associator Gr Gl).hom ≫ F.whiskerLeft adj.counit ≫ F.rightUnitor.hom
hα' : NatTrans.Equifibered α'
hadj : ∀ (X : C), Gl.map (adj.unit.app X) = inv (adj.counit.app (Gl.1 ((𝟭 C).obj X)))
this : ∀ (X : C), IsIso (Gl.map (adj.unit.app X))
hα'' : ∀ (j : J), Gl.map (Gr.map (α'.app j)) = adj.counit.app (F'.1 j) ≫ α.app j
hc'' : ∀ (j : J), α.app j ≫ Gl.map (c.ι.app j) = c'.ι.app j ≫ f
β : F' ⋙ Gr ⋙ Gl ≅ F' := F'.isoWhiskerLeft (asIso adj.counit) ≪≫ F'.rightUnitor
c'' : Cocone (F' ⋙ Gr) :=
  { pt := pullback (Gr.map f) (adj.unit.app c.pt),
    ι := { app := fun j ↦ pullback.lift (Gr.map (c'.ι.app j)) (Gr.map (α'.app j) ≫ c.ι.app j) ⋯, naturality := ⋯ } }
j : J
⊢ ((Cocone.precompose β.hom).obj c').ι.app j ≫ f = Gl.map (Gr.map (α'.app j) ≫ c.ι.app j)

Tactic:
· rw [Gl.map_comp, hα'', Category.assoc, hc'']
        dsimp [β]
        rw [Category.comp_id, Category.assoc]

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

Goal state before:
pp: case h'_w.h'_w
J : Type v'
inst✝⁴ : Category.{u', v'} J
C : Type u
inst✝³ : Category.{v, u} C
W X Y Z✝ : C
f✝ : W ⟶ X
g✝ : W ⟶ Y
h : X ⟶ Z✝
i : Y ⟶ Z✝
inst✝² : Adhesive C
Z A B : C
a : A ⟶ Z
b : B ⟶ Z
inst✝¹ : Mono a
inst✝ : Mono b
K : C
f g : K ⟶ pushout (fst a b) (snd a b)
w : f ≫ pushout.desc a b ⋯ = g ≫ pushout.desc a b ⋯
u : A ⟶ pushout (fst a b) (snd a b) := ⋯
v : B ⟶ pushout (fst a b) (snd a b) := ⋯
this✝¹ : Mono u := ⋯
this✝ : Mono v := ⋯
sq_f_u : IsPullback (fst f u) (snd f u) f u := ⋯
sq_f_v : IsPullback (fst f v) (snd f v) f v := ⋯
sq_g_u : IsPullback (fst g u) (snd g u) g u := ⋯
sq_g_v : IsPullback (fst g v) (snd g v) g v := ⋯
l₁ : pullback f u ⟶ K := ⋯
f₁ : pullback f u ⟶ A := ⋯
l₂ : pullback f v ⟶ K := ⋯
f₂ : pullback f v ⟶ B := ⋯
m₁ : pullback g u ⟶ K := ⋯
g₁ : pullback g u ⟶ A := ⋯
m₂ : pullback g v ⟶ K := ⋯
g₂ : pullback g v ⟶ B := ⋯
w✝² : C
f' : w✝² ⟶ pullback f u
w✝¹ : w✝² ⟶ pullback f v
w✝ : w✝² ⟶ pullback a b
p₁ : IsPullback f' w✝ (snd f u) (fst a b)
left✝ : IsPullback w✝¹ w✝ (snd f v) (snd a b)
h₁ : IsPushout f' w✝¹ (fst f u) (fst f v)
this : Mono f' := ⋯
sq₁₁ : IsPullback (fst m₁ l₁) (snd m₁ l₁) m₁ l₁ := ⋯
sq₁₂ : IsPullback (fst m₁ l₂) (snd m₁ l₂) m₁ l₂ := ⋯
⊢ fst m₁ l₁ ≫ fst g u ≫ f = fst m₁ l₁ ≫ fst g u ≫ g

Tactic:
pullback.condition_assoc,

Goal state after:
case h'_w.h'_w
J : Type v'
inst✝⁴ : Category.{u', v'} J
C : Type u
inst✝³ : Category.{v, u} C
W X Y Z✝ : C
f✝ : W ⟶ X
g✝ : W ⟶ Y
h : X ⟶ Z✝
i : Y ⟶ Z✝
inst✝² : Adhesive C
Z A B : C
a : A ⟶ Z
b : B ⟶ Z
inst✝¹ : Mono a
inst✝ : Mono b
K : C
f g : K ⟶ pushout (fst a b) (snd a b)
w : f ≫ pushout.desc a b ⋯ = g ≫ pushout.desc a b ⋯
u : A ⟶ pushout (fst a b) (snd a b) := inl (fst a b) (snd a b)
v : B ⟶ pushout (fst a b) (snd a b) := inr (fst a b) (snd a b)
this✝¹ : Mono u := mono_of_isPushout_of_mono_right (of_hasPushout (fst a b) (snd a b))
this✝ : Mono v := mono_of_isPushout_of_mono_left (of_hasPushout (fst a b) (snd a b))
sq_f_u : IsPullback (fst f u) (snd f u) f u := of_hasPullback f u
sq_f_v : IsPullback (fst f v) (snd f v) f v := of_hasPullback f v
sq_g_u : IsPullback (fst g u) (snd g u) g u := of_hasPullback g u
sq_g_v : IsPullback (fst g v) (snd g v) g v := of_hasPullback g v
l₁ : pullback f u ⟶ K := fst f u
f₁ : pullback f u ⟶ A := snd f u
l₂ : pullback f v ⟶ K := fst f v
f₂ : pullback f v ⟶ B := snd f v
m₁ : pullback g u ⟶ K := fst g u
g₁ : pullback g u ⟶ A := snd g u
m₂ : pullback g v ⟶ K := fst g v
g₂ : pullback g v ⟶ B := snd g v
w✝² : C
f' : w✝² ⟶ pullback f u
w✝¹ : w✝² ⟶ pullback f v
w✝ : w✝² ⟶ pullback a b
p₁ : IsPullback f' w✝ (snd f u) (fst a b)
left✝ : IsPullback w✝¹ w✝ (snd f v) (snd a b)
h₁ : IsPushout f' w✝¹ (fst f u) (fst f v)
this : Mono f' := Eq.mpr (id (congrArg (fun _a ↦ Mono _a) (Eq.symm (isoPullback_hom_fst p₁)))) inferInstance
sq₁₁ : IsPullback (fst m₁ l₁) (snd m₁ l₁) m₁ l₁ := of_hasPullback m₁ l₁
sq₁₂ : IsPullback (fst m₁ l₂) (snd m₁ l₂) m₁ l₂ := of_hasPullback m₁ l₂
⊢ snd m₁ l₁ ≫ l₁ ≫ f = fst m₁ l₁ ≫ fst g u ≫ g
Module: Mathlib.CategoryTheory.Localization.Bousfield

Goal state before:
pp: case mp
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
hX : P X
hY : P Y
⊢ P.isLocal f → IsIso f

Tactic:
intro hf
    obtain ⟨g, hg⟩ := (hf _ hX).2 (𝟙 X)
    exact ⟨g, hg, (hf _ hY).1 (by simp only [reassoc_of% hg, comp_id])⟩

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
J : GrothendieckTopology C
A : Type u_2
inst✝¹ : Category.{v_2, u_2} A
inst✝ : HasWeakSheafify J A
⊢ (presheafToSheaf J A).IsLocalization ((MorphismProperty.isomorphisms (Sheaf J A)).inverseImage (presheafToSheaf J A))

Tactic:
exact (sheafificationAdjunction J A).isLocalization

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

Goal state before:
pp: case refine_2
C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝⁴ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst✝³ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝² : ConcreteCategory A FA
F₁ F₂ F₃ : Cᵒᵖ ⥤ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
inst✝¹ : IsLocallySurjective J (f₁ ≫ f₂)
inst✝ : IsLocallyInjective J f₂
X : C
x : ToType (F₂.obj (op X))
S : Sieve X := imageSieve (f₁ ≫ f₂) ((ConcreteCategory.hom (f₂.app (op X))) x)
T : ⦃Y : C⦄ → (f : Y ⟶ X) → S.arrows f → Sieve Y :=
  fun Y f hf ↦
    equalizerSieve
      ((ConcreteCategory.hom (f₁.app (op Y))) (localPreimage (f₁ ≫ f₂) ((ConcreteCategory.hom (f₂.app (op X))) x) f hf))
      ((ConcreteCategory.hom (F₂.map f.op)) x)
⊢ ∀ ⦃Y : C⦄ ⦃f : Y ⟶ unop (op X)⦄,
    (imageSieve (f₁ ≫ f₂) ((ConcreteCategory.hom (f₂.app (op X))) x)).arrows f →
      Sieve.pullback f (Sieve.bind S.arrows T) ∈ J Y

Tactic:
intro Y f hf
      apply J.superset_covering (Sieve.le_pullback_bind _ _ _ hf)
      apply equalizerSieve_mem J f₂
      rw [NatTrans.naturality_apply, ← app_localPreimage (f₁ ≫ f₂) _ _ hf,
        NatTrans.comp_app, ConcreteCategory.comp_apply]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify

Goal state before:
pp: case hr₀
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
R₀ R : Cᵒᵖ ⥤ RingCat
α : R₀ ⟶ R
inst✝¹ : Presheaf.IsLocallyInjective J α
M₀ : PresheafOfModules R₀
A : Cᵒᵖ ⥤ AddCommGrpCat
φ : M₀.presheaf ⟶ A
inst✝ : Presheaf.IsLocallyInjective J φ
hA : Presheaf.IsSeparated J A
X : C
r : ↑(R.obj (Opposite.op X))
m : ↑(A.obj (Opposite.op X))
Y Z : C
f : Y ⟶ X
g : Z ⟶ Y
r₀ : ↑(R₀.obj (Opposite.op Y))
r₀' : ↑(R₀.obj (Opposite.op Z))
m₀ : ↑(M₀.obj (Opposite.op Y))
m₀' : ↑(M₀.obj (Opposite.op Z))
hr₀ : (ConcreteCategory.hom (α.app (Opposite.op Y))) r₀ = (ConcreteCategory.hom (R.map f.op)) r
hr₀' : (ConcreteCategory.hom (α.app (Opposite.op Z))) r₀' = (ConcreteCategory.hom (R.map (f.op ≫ g.op))) r
hm₀ : (ConcreteCategory.hom (φ.app (Opposite.op Y))) m₀ = (ConcreteCategory.hom (A.map f.op)) m
hm₀' : (ConcreteCategory.hom (φ.app (Opposite.op Z))) m₀' = (ConcreteCategory.hom (A.map (f.op ≫ g.op))) m
⊢ (ConcreteCategory.hom (α.app (Opposite.op Z))) ((ConcreteCategory.hom (R₀.map g.op)) r₀) =
    (ConcreteCategory.hom (R.map (f.op ≫ g.op))) r

Tactic:
R.map_comp,

Goal state after:
case hr₀
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
R₀ R : Cᵒᵖ ⥤ RingCat
α : R₀ ⟶ R
inst✝¹ : Presheaf.IsLocallyInjective J α
M₀ : PresheafOfModules R₀
A : Cᵒᵖ ⥤ AddCommGrpCat
φ : M₀.presheaf ⟶ A
inst✝ : Presheaf.IsLocallyInjective J φ
hA : Presheaf.IsSeparated J A
X : C
r : ↑(R.obj (Opposite.op X))
m : ↑(A.obj (Opposite.op X))
Y Z : C
f : Y ⟶ X
g : Z ⟶ Y
r₀ : ↑(R₀.obj (Opposite.op Y))
r₀' : ↑(R₀.obj (Opposite.op Z))
m₀ : ↑(M₀.obj (Opposite.op Y))
m₀' : ↑(M₀.obj (Opposite.op Z))
hr₀ : (ConcreteCategory.hom (α.app (Opposite.op Y))) r₀ = (ConcreteCategory.hom (R.map f.op)) r
hr₀' : (ConcreteCategory.hom (α.app (Opposite.op Z))) r₀' = (ConcreteCategory.hom (R.map (f.op ≫ g.op))) r
hm₀ : (ConcreteCategory.hom (φ.app (Opposite.op Y))) m₀ = (ConcreteCategory.hom (A.map f.op)) m
hm₀' : (ConcreteCategory.hom (φ.app (Opposite.op Z))) m₀' = (ConcreteCategory.hom (A.map (f.op ≫ g.op))) m
⊢ (ConcreteCategory.hom (α.app (Opposite.op Z))) ((ConcreteCategory.hom (R₀.map g.op)) r₀) =
    (ConcreteCategory.hom (R.map f.op ≫ R.map g.op)) r
Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X : C
inst✝ : HasExt C
⊢ Projective X ↔ ∀ ⦃Y : C⦄, Subsingleton (Ext X Y 1)

Tactic:
refine ⟨fun h ↦ HasProjectiveDimensionLT.subsingleton X 1 1 (by rfl),
    fun h ↦ ⟨fun f g _ ↦ ?_⟩⟩

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X : C
inst✝ : HasExt C
h : ∀ ⦃Y : C⦄, Subsingleton (Ext X Y 1)
E✝ X✝ : C
f : X ⟶ X✝
g : E✝ ⟶ X✝
x✝ : Epi g
⊢ ∃ f', f' ≫ g = f
Module: Mathlib.CategoryTheory.Limits.Preserves.Opposites

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : PreservesFiniteCoproducts F
n : ℕ
⊢ PreservesLimitsOfShape (Discrete (Fin n)) F.op

Tactic:
apply +allowSynthFailures preservesLimitsOfShape_op
    exact preservesColimitsOfShape_of_equiv (Discrete.opposite _).symm _

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Flat

Goal state before:
pp: case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
x✝ : RepresentablyCoflat F.op
X : D
⊢ IsCofiltered (StructuredArrow X F)

Tactic:
suffices IsFiltered (StructuredArrow X F)ᵒᵖ from isCofiltered_of_isFiltered_op _
    apply IsFiltered.of_equivalence (structuredArrowOpEquivalence _ _).symm

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

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
S : C
R : Presieve S
Y : C
f : Y ⟶ S
h : R f
i : ↑R.uncurry := ⟨⟨Y, f⟩, h⟩
⊢ R.preZeroHypercover.presieve₀ f

Tactic:
exact .mk i

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

Goal state before:
pp: case mpr.transitive.refine_1
C : Type u_3
inst✝ : Category.{u_2, u_3} C
J : Precoverage C
P : Cᵒᵖ ⥤ Type u_1
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
hS : J.Saturate X R
h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → J.Saturate Y (Sieve.pullback f S)
Y : C
f : Y ⟶ X
H :
  ∀ {X Y : C} {f : Y ⟶ X},
    ∀ R ∈ J.coverings X,
      Presieve.IsSeparatedFor P (Sieve.pullback f (Sieve.generate R)).arrows ∧
        ∀ (x : Presieve.FamilyOfElements P (Sieve.pullback f (Sieve.generate R)).arrows),
          x.Compatible → ∃ t, x.IsAmalgamation t
H1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X), Presieve.IsSeparatedFor P (Sieve.pullback f R).arrows
H1' :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (x : Presieve.FamilyOfElements P (Sieve.pullback f R).arrows),
    x.Compatible → ∃ t, x.IsAmalgamation t
H2 :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y), Presieve.IsSeparatedFor P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows
H2' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f →
      ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y) (x : Presieve.FamilyOfElements P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows),
        x.Compatible → ∃ t, x.IsAmalgamation t
x : Presieve.FamilyOfElements P (Sieve.pullback f S).arrows
t₁ : P.obj (Opposite.op Y)
⊢ ∀ (t₂ : P.obj (Opposite.op Y)), x.IsAmalgamation t₁ → x.IsAmalgamation t₂ → t₁ = t₂

Tactic:
t₂

Goal state after:
case mpr.transitive.refine_1
C : Type u_3
inst✝ : Category.{u_2, u_3} C
J : Precoverage C
P : Cᵒᵖ ⥤ Type u_1
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
hS : J.Saturate X R
h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → J.Saturate Y (Sieve.pullback f S)
Y : C
f : Y ⟶ X
H :
  ∀ {X Y : C} {f : Y ⟶ X},
    ∀ R ∈ J.coverings X,
      Presieve.IsSeparatedFor P (Sieve.pullback f (Sieve.generate R)).arrows ∧
        ∀ (x : Presieve.FamilyOfElements P (Sieve.pullback f (Sieve.generate R)).arrows),
          x.Compatible → ∃ t, x.IsAmalgamation t
H1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X), Presieve.IsSeparatedFor P (Sieve.pullback f R).arrows
H1' :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (x : Presieve.FamilyOfElements P (Sieve.pullback f R).arrows),
    x.Compatible → ∃ t, x.IsAmalgamation t
H2 :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y), Presieve.IsSeparatedFor P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows
H2' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f →
      ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y) (x : Presieve.FamilyOfElements P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows),
        x.Compatible → ∃ t, x.IsAmalgamation t
x : Presieve.FamilyOfElements P (Sieve.pullback f S).arrows
t₁ t₂ : P.obj (Opposite.op Y)
⊢ x.IsAmalgamation t₁ → x.IsAmalgamation t₂ → t₁ = t₂
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : Precoverage C
S T : C
f : S ⟶ T
hf : Presieve.singleton f ∈ J.coverings T
⊢ (PreZeroHypercover.singleton f).presieve₀ ∈ J.coverings T

Tactic:
simpa [PreZeroHypercover.presieve₀, PreZeroHypercover.singleton, Presieve.ofArrows_pUnit]

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

Goal state before:
pp: case inr
C : Type ?u.2
D : Type ?u.4
inst✝¹ : Category.{v_1, ?u.2} C
inst✝ : Category.{v_2, ?u.4} D
x y : Coverage C
X Y : C
f : Y ⟶ X
S : Presieve X
hy : S ∈ y.coverings X
⊢ ∃ T ∈ x.coverings Y ∪ y.coverings Y, T.FactorsThruAlong S f

Tactic:
· obtain ⟨T, hT⟩ := y.pullback f S hy
        exact ⟨T, Or.inr hT.1, hT.2⟩

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

Goal state before:
pp: C : Type ?u.2
D : Type ?u.4
inst✝¹ : Category.{v_1, ?u.2} C
inst✝ : Category.{v_2, ?u.4} D
x y : Coverage C
⊢ ∀ ⦃X Y : C⦄ (f : Y ⟶ X),
    ∀ S ∈ x.coverings X ∪ y.coverings X, ∃ T ∈ x.coverings Y ∪ y.coverings Y, T.FactorsThruAlong S f

Tactic:
rintro X Y f S (hx | hy)
      · obtain ⟨T, hT⟩ := x.pullback f S hx
        exact ⟨T, Or.inl hT.1, hT.2⟩
      · obtain ⟨T, hT⟩ := y.pullback f S hy
        exact ⟨T, Or.inr hT.1, hT.2⟩

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

Goal state before:
pp: case refine_3
C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
inst✝ : J.IsStableUnderBaseChange
S : C
E F : PreZeroHypercover S
e : E ≅ F
h : E.presieve₀ ∈ J.coverings S
⊢ ∀ (i : F.I₀), IsPullback (F.f i) (e.inv.h₀ i) (𝟙 S) (E.f (e.inv.s₀ i))

Tactic:
· intro i
      exact CategoryTheory.IsPullback.of_vert_isIso (by simp)

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

Goal state before:
pp: C : Type u_2
inst✝⁴ : Category.{u_1, u_2} C
J : Precoverage C
inst✝³ : J.IsStableUnderComposition
inst✝² : J.IsStableUnderBaseChange
inst✝¹ : Limits.HasPullbacks C
inst✝ : J.HasIsos
⊢ (toPretopology C J).toGrothendieck = J.toGrothendieck

Tactic:
ext
  exact J.mem_toGrothendieck_iff_of_isStableUnderComposition.symm

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
K : GrothendieckTopology D
F : C ⥤ D
inst✝¹ : F.Full
inst✝ : F.Faithful
hF : {c : C} → {d : D} → (d ⟶ F.obj c) → (c' : C) × (F.obj c' ≅ d)
⊢ ∀ (ℱ : Sheaf K (Type u_1)) {Z : C} {T : Presieve Z} {x : FamilyOfElements (F.op ⋙ ℱ.obj) T},
    x.Compatible →
      ∀ {Y₁ Y₂ : C} {X : D} (f₁ : X ⟶ F.obj Y₁) (f₂ : X ⟶ F.obj Y₂) {g₁ : Y₁ ⟶ Z} {g₂ : Y₂ ⟶ Z} (hg₁ : T g₁)
        (hg₂ : T g₂),
        f₁ ≫ F.map g₁ = f₂ ≫ F.map g₂ →
          (ConcreteCategory.hom (ℱ.obj.map f₁.op)) (x g₁ hg₁) = (ConcreteCategory.hom (ℱ.obj.map f₂.op)) (x g₂ hg₂)

Tactic:
introv hx he

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
K : GrothendieckTopology D
F : C ⥤ D
inst✝¹ : F.Full
inst✝ : F.Faithful
hF : {c : C} → {d : D} → (d ⟶ F.obj c) → (c' : C) × (F.obj c' ≅ d)
ℱ : Sheaf K (Type u_1)
Z : C
T : Presieve Z
x : FamilyOfElements (F.op ⋙ ℱ.obj) T
hx : x.Compatible
Y₁ Y₂ : C
X : D
f₁ : X ⟶ F.obj Y₁
f₂ : X ⟶ F.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
he : f₁ ≫ F.map g₁ = f₂ ≫ F.map g₂
⊢ (ConcreteCategory.hom (ℱ.obj.map f₁.op)) (x g₁ hg₁) = (ConcreteCategory.hom (ℱ.obj.map f₂.op)) (x g₂ hg₂)
Module: Mathlib.CategoryTheory.Sites.CoverPreserving

Goal state before:
pp: case hex
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
hF₁ : CompatiblePreserving K F
hF₂ : CoverPreserving J K F
G : Sheaf K (Type (max u₁ v₁ u₂ v₂))
X : C
S : Sieve X
hS : S ∈ J X
x : FamilyOfElements (F.op ⋙ G.obj) S.arrows
hx : x.Compatible
H : IsSheafFor G.obj (Sieve.functorPushforward F S).arrows
⊢ ∃ x_1, x.IsAmalgamation x_1

Tactic:
exact ⟨H.amalgamate (x.functorPushforward F) (hx.functorPushforward hF₁),
        fun V f hf => (H.isAmalgamation (hx.functorPushforward hF₁) (F.map f) _).trans
          (hF₁.apply_map _ hx hf)⟩

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
A : Type u_1
inst✝² : Category.{v_1, u_1} A
S : C
E✝ : PreOneHypercover S
E : PreOneHypercover S
F : PreOneHypercover S
inst✝¹ : ∀ (i : E.I₀) (j : F.I₀), HasPullback (E.f i) (F.f j)
inst✝ : ∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b), HasPullback (E.p₁ k ≫ E.f i) (F.p₁ l ≫ F.f a)
i j : __spread✝⁻⁰.I₀
k : E.I₁ i.1 j.1 × F.I₁ i.2 j.2
⊢ (F.p₁ k.2 ≫ F.f i.2) ≫ 𝟙 S = F.p₂ k.2 ≫ F.f ((Equiv.sigmaEquivProd E.I₀ F.toPreZeroHypercover.1).symm j).snd

Tactic:
simp [F.w]

Goal state after: