mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic

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
E : Type u_3
inst✝ : Category.{v_3, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
G : C ⥤ D
U Y✝ Z✝ : D
f✝ : Y✝ ⟶ U
x✝ : Presieve.coverByImage G U f✝
g : Z✝ ⟶ Y✝
Z : C
f₁ : Y✝ ⟶ G.obj Z
f₂ : G.obj Z ⟶ U
e : f₁ ≫ f₂ = f✝
⊢ (g ≫ f₁) ≫ f₂ = g ≫ f✝

Tactic:
Category.assoc,

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
D : Type u_2
inst✝¹ : Category.{v_2, u_2} D
E : Type u_3
inst✝ : Category.{v_3, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
G : C ⥤ D
U Y✝ Z✝ : D
f✝ : Y✝ ⟶ U
x✝ : Presieve.coverByImage G U f✝
g : Z✝ ⟶ Y✝
Z : C
f₁ : Y✝ ⟶ G.obj Z
f₂ : G.obj Z ⟶ U
e : f₁ ≫ f₂ = f✝
⊢ g ≫ f₁ ≫ f₂ = g ≫ f✝
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic

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
K : GrothendieckTopology D
A : Type u_4
inst✝² : Category.{v_4, u_4} A
G : C ⥤ D
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj
X : Cᵒᵖ
U : Aᵒᵖ
x✝ : (yoneda.obj ((G.op ⋙ ℱ).obj X)).obj U
Y : D
f : Y ⟶ G.obj (unop X)
hf : (Sieve.coverByImage G (G.obj (unop X))).arrows f
| (ConcreteCategory.hom ((ℱ'.obj ⋙ coyoneda.obj (op (unop U))).map f.op))
    (have this := (ConcreteCategory.hom ((yoneda.map (α.app X)).app U)) x✝;
    this)

Tactic:
rw [← hf.some.fac]

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
D : Type u_2
inst✝³ : Category.{v_2, u_2} D
K : GrothendieckTopology D
A : Type u_4
inst✝² : Category.{v_4, u_4} A
G : C ⥤ D
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj
X : Cᵒᵖ
U : Aᵒᵖ
x✝ : (yoneda.obj ((G.op ⋙ ℱ).obj X)).obj U
Y : D
f : Y ⟶ G.obj (unop X)
hf : (Sieve.coverByImage G (G.obj (unop X))).arrows f
| (ConcreteCategory.hom
      ((ℱ'.obj ⋙ coyoneda.obj (op (unop U))).map ((Nonempty.some hf).lift ≫ (Nonempty.some hf).map).op))
    (have this := (ConcreteCategory.hom ((yoneda.map (α.app X)).app U)) x✝;
    this)
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic

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
K : GrothendieckTopology D
A : Type u_4
inst✝² : Category.{v_4, u_4} A
G : C ⥤ D
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : ℱ ⟶ ℱ'.obj
X : Dᵒᵖ
U : Aᵒᵖ
x✝ : (yoneda.obj (ℱ.obj X)).obj U
Y : D
f : Y ⟶ unop X
hf : (Sieve.coverByImage G (unop X)).arrows f
| (ConcreteCategory.hom ((ℱ'.obj ⋙ coyoneda.obj (op (unop U))).map f.op))
    (have this := (ConcreteCategory.hom ((yoneda.map (α.app X)).app U)) x✝;
    this)

Tactic:
rw [← hf.some.fac]

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
D : Type u_2
inst✝³ : Category.{v_2, u_2} D
K : GrothendieckTopology D
A : Type u_4
inst✝² : Category.{v_4, u_4} A
G : C ⥤ D
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : ℱ ⟶ ℱ'.obj
X : Dᵒᵖ
U : Aᵒᵖ
x✝ : (yoneda.obj (ℱ.obj X)).obj U
Y : D
f : Y ⟶ unop X
hf : (Sieve.coverByImage G (unop X)).arrows f
| (ConcreteCategory.hom
      ((ℱ'.obj ⋙ coyoneda.obj (op (unop U))).map ((Nonempty.some hf).lift ≫ (Nonempty.some hf).map).op))
    (have this := (ConcreteCategory.hom ((yoneda.map (α.app X)).app U)) x✝;
    this)
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic

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
E : Type u_3
inst✝⁴ : Category.{v_3, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝³ : Category.{v_4, u_4} A
G : C ⥤ D
inst✝² : G.IsCoverDense K
inst✝¹ : G.IsLocallyFull K
ℱ✝ : Dᵒᵖ ⥤ A
ℱ'✝ : Sheaf K A
inst✝ : G.IsContinuous J K
ℱ ℱ' : Sheaf K A
α β : ℱ ⟶ ℱ'
e : ((G.sheafPushforwardContinuous A J K).map α).hom = ((G.sheafPushforwardContinuous A J K).map β).hom
⊢ α.hom = β.hom

Tactic:
dsimp [sheafPushforwardContinuous] at e

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
D : Type u_2
inst✝⁵ : Category.{v_2, u_2} D
E : Type u_3
inst✝⁴ : Category.{v_3, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝³ : Category.{v_4, u_4} A
G : C ⥤ D
inst✝² : G.IsCoverDense K
inst✝¹ : G.IsLocallyFull K
ℱ✝ : Dᵒᵖ ⥤ A
ℱ'✝ : Sheaf K A
inst✝ : G.IsContinuous J K
ℱ ℱ' : Sheaf K A
α β : ℱ ⟶ ℱ'
e : G.op.whiskerLeft α.hom = G.op.whiskerLeft β.hom
⊢ α.hom = β.hom
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic

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
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
A : Type u_4
inst✝¹ : Category.{v_4, u_4} A
inst✝ : IsDenseSubsite J K G
F : Sheaf J A
X Y Z : C
f : G.obj X ⟶ G.obj Y
p : Z ⟶ X
g : Z ⟶ Y
fac : G.map p ≫ f = G.map g
W₀ : C
a : W₀ ⟶ Z
ha : (Sieve.pullback p (G.imageSieve f)).arrows a
⊢ (mapPreimage K G F f ≫ F.obj.map p.op) ≫ F.obj.map a.op = F.obj.map g.op ≫ F.obj.map a.op

Tactic:
Category.assoc,

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
A : Type u_4
inst✝¹ : Category.{v_4, u_4} A
inst✝ : IsDenseSubsite J K G
F : Sheaf J A
X Y Z : C
f : G.obj X ⟶ G.obj Y
p : Z ⟶ X
g : Z ⟶ Y
fac : G.map p ≫ f = G.map g
W₀ : C
a : W₀ ⟶ Z
ha : (Sieve.pullback p (G.imageSieve f)).arrows a
⊢ mapPreimage K G F f ≫ F.obj.map p.op ≫ F.obj.map a.op = F.obj.map g.op ≫ F.obj.map a.op
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic

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
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
A : Type u_4
inst✝¹ : Category.{v_4, u_4} A
inst✝ : IsDenseSubsite J K G
F : Sheaf J A
X : C
⊢ mapPreimage K G F (G.map (𝟙 X)) = 𝟙 (F.obj.obj (op X))

Tactic:
mapPreimage_map,

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
A : Type u_4
inst✝¹ : Category.{v_4, u_4} A
inst✝ : IsDenseSubsite J K G
F : Sheaf J A
X : C
⊢ F.obj.map (𝟙 X).op = 𝟙 (F.obj.obj (op X))
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreOneHypercover S
i i' j j' : E.I₀
hii' : i = i'
hjj' : j = j'
i'' j'' : E.I₀
hii'' : i' = i''
hjj'' : j' = j''
k : E.I₁ i j
⊢ (congrIndexOneOfEq hii'' hjj'') ((congrIndexOneOfEq hii' hjj') k) = (congrIndexOneOfEq ⋯ ⋯) k

Tactic:
subst hii' hjj'
  simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
i i' j j' : E.I₀
hii' : i = i'
hjj' : j = j'
u₀ : E.I₀ → F.I₀
u₁ : ⦃i j : E.I₀⦄ → E.I₁ i j → F.I₁ (u₀ i) (u₀ j)
k : E.I₁ i j
⊢ u₁ ((congrIndexOneOfEq hii' hjj') k) = (congrIndexOneOfEq ⋯ ⋯) (u₁ k)

Tactic:
subst hii' hjj'
  simp

Goal state after:
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.SheafEquiv

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type w
inst✝² : Category.{w', w} A
inst✝¹ : ∀ (X : Dᵒᵖ), Limits.HasLimitsOfShape (StructuredArrow X G.op) A
inst✝ : IsDenseSubsite J K G
Y : Sheaf J A
U : C
X : A
f : (yoneda.obj (((𝟭 (Cᵒᵖ ⥤ A)).obj Y.obj).obj (op U))).obj (op X)
l : (X Y Z : C) → (f : X ⟶ Y) → (g : G.obj Y ⟶ G.obj Z) → (G.imageSieve g).arrows f → (X ⟶ Z)
hl :
  ∀ (X Y Z : C) (f : X ⟶ Y) (g : G.obj Y ⟶ G.obj Z) (hf : (G.imageSieve g).arrows f),
    G.map (l X Y Z f g hf) = G.map f ≫ g
c : Limits.Cone (StructuredArrow.proj (op (G.obj U)) G.op ⋙ Y.obj) :=
  { pt := X,
    π :=
      {
        app := fun g ↦
          ⋯.amalgamate ⟨G.imageSieve g.hom.unop, ⋯⟩ (fun I ↦ f ≫ Y.obj.map (l I.Y (unop g.2) U I.f g.hom.unop ⋯).op) ⋯,
        naturality := ⋯ } }
this :
  (G.op.isPointwiseRightKanExtensionRanCounit Y.obj (op (G.obj U))).lift c ≫ (G.op.ranCounit.app Y.obj).app (op U) =
    c.π.app (StructuredArrow.mk (𝟙 (op (G.obj U))))
I : GrothendieckTopology.Cover.Arrow ⟨G.imageSieve (𝟙 (G.obj U)), ⋯⟩
V : C
iUV : V ⟶ I.Y
hiUV : iUV ≫ l I.Y U U I.f (𝟙 (G.obj U)) ⋯ = iUV ≫ I.f
⊢ (ConcreteCategory.hom ((Y.obj ⋙ coyoneda.obj (op X)).map iUV.op))
      (⋯.amalgamate ⟨G.imageSieve (StructuredArrow.mk (𝟙 (op (G.obj U)))).hom.unop, ⋯⟩
          (fun I ↦
            f ≫
              Y.obj.map
                (l I.Y (unop (StructuredArrow.mk (𝟙 (op (G.obj U)))).2) U I.f
                    (StructuredArrow.mk (𝟙 (op (G.obj U)))).hom.unop ⋯).op)
          ⋯ ≫
        Y.obj.map I.f.op) =
    (ConcreteCategory.hom ((Y.obj ⋙ coyoneda.obj (op X)).map iUV.op)) (f ≫ Y.obj.map I.f.op)

Tactic:
simp [← Functor.map_comp, ← op_comp, hiUV]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
Ps : Set (Cᵒᵖ ⥤ Type w)
J : GrothendieckTopology C
hJ : ∀ P ∈ Ps, Presieve.IsSheaf J P
X : C
S : Sieve X
⊢ S ∈ J X → S ∈ (finestTopology Ps) X

Tactic:
hS

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
Ps : Set (Cᵒᵖ ⥤ Type w)
J : GrothendieckTopology C
hJ : ∀ P ∈ Ps, Presieve.IsSheaf J P
X : C
S : Sieve X
hS : S ∈ J X
⊢ S ∈ (finestTopology Ps) X
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: case h
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
S✝ : C
E✝¹ E✝ : PreOneHypercover S✝
F✝ : PreOneHypercover S✝
G : PreOneHypercover S✝
S : C
E F : PreOneHypercover S
e : E ≅ F
i : E.I₀
⊢ 𝟙 (E.X i) = 𝟙 (E.X i) ∧ (e.inv.h₀ (e.hom.s₀ i) ≫ eqToHom ⋯) ≫ e.hom.h₀ i = 𝟙 (F.X (e.hom.s₀ i))

Tactic:
Category.assoc,

Goal state after:
case h
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
S✝ : C
E✝¹ E✝ : PreOneHypercover S✝
F✝ : PreOneHypercover S✝
G : PreOneHypercover S✝
S : C
E F : PreOneHypercover S
e : E ≅ F
i : E.I₀
⊢ 𝟙 (E.X i) = 𝟙 (E.X i) ∧ e.inv.h₀ (e.hom.s₀ i) ≫ eqToHom ⋯ ≫ e.hom.h₀ i = 𝟙 (F.X (e.hom.s₀ i))
Module: Mathlib.CategoryTheory.Sites.Equivalence

Goal state before:
pp: C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝⁹ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : D ⥤ C
A : Type u₃
inst✝⁸ : Category.{v₃, u₃} A
inst✝⁷ : G.IsCoverDense J
inst✝⁶ : G.Full
inst✝⁵ : G.IsContinuous K J
inst✝⁴ : (G.sheafPushforwardContinuous A K J).EssSurj
inst✝³ : G.IsCocontinuous K J
FA : A → A → Type u_1
CA : A → Type u_2
inst✝² : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝¹ : ConcreteCategory A FA
inst✝ : K.WEqualsLocallyBijective A
hG : CoverPreserving K J G
X✝ Y✝ : Cᵒᵖ ⥤ A
f : X✝ ⟶ Y✝
⊢ K.W (G.op.whiskerLeft f) ↔
    Presheaf.IsLocallyInjective K (G.op.whiskerLeft f) ∧ Presheaf.IsLocallySurjective K (G.op.whiskerLeft f)

Tactic:
W_iff_isLocallyBijective

Goal state after:
C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝⁹ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : D ⥤ C
A : Type u₃
inst✝⁸ : Category.{v₃, u₃} A
inst✝⁷ : G.IsCoverDense J
inst✝⁶ : G.Full
inst✝⁵ : G.IsContinuous K J
inst✝⁴ : (G.sheafPushforwardContinuous A K J).EssSurj
inst✝³ : G.IsCocontinuous K J
FA : A → A → Type u_1
CA : A → Type u_2
inst✝² : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝¹ : ConcreteCategory A FA
inst✝ : K.WEqualsLocallyBijective A
hG : CoverPreserving K J G
X✝ Y✝ : Cᵒᵖ ⥤ A
f : X✝ ⟶ Y✝
⊢ Presheaf.IsLocallyInjective K (G.op.whiskerLeft f) ∧ Presheaf.IsLocallySurjective K (G.op.whiskerLeft f) ↔
    Presheaf.IsLocallyInjective K (G.op.whiskerLeft f) ∧ Presheaf.IsLocallySurjective K (G.op.whiskerLeft f)
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
J : GrothendieckTopology C
S : C
E : J.OneHypercover S
F : Sheaf J A
c : Multifork (E.multicospanIndex F.obj)
W : C
i₁ i₂ : E.I₀
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
w : p₁ ≫ E.f i₁ = p₂ ≫ E.f i₂
⊢ c.ι i₁ ≫ F.obj.map p₁.op = c.ι i₂ ≫ F.obj.map p₂.op

Tactic:
apply F.property.hom_ext ⟨_, E.mem₁ _ _ _ _ w⟩
    rintro ⟨T, g, j, h, fac₁, fac₂⟩
    dsimp
    simp only [assoc, ← Functor.map_comp, ← op_comp, fac₁, fac₂]
    simp only [op_comp, Functor.map_comp]
    simpa using! c.condition ⟨⟨i₁, i₂⟩, j⟩ =≫ F.obj.map h.op

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators

Goal state before:
pp: C : Type u'
inst✝⁷ : Category.{v', u'} C
J : GrothendieckTopology C
R : Sheaf J RingCat
inst✝⁶ : HasWeakSheafify J AddCommGrpCat
inst✝⁵ : J.WEqualsLocallyBijective AddCommGrpCat
M✝ N P : SheafOfModules R
C' : Type u₁
inst✝⁴ : Category.{v₁, u₁} C'
J' : GrothendieckTopology C'
S : Sheaf J' RingCat
inst✝³ : HasSheafify J' AddCommGrpCat
inst✝² : J'.WEqualsLocallyBijective AddCommGrpCat
M : SheafOfModules R
G : M.GeneratingSections
F : SheafOfModules R ⥤ SheafOfModules S
inst✝¹ : PreservesColimitsOfSize.{u, u, max u u', max u u₁, max (max (u + 1) u') v', max (max (u + 1) u₁) v₁} F
η : unit S ≅ F.obj (unit R)
inst✝ : IsIso G.π
⊢ IsIso (G.map F η).π

Tactic:
by
  rw [GeneratingSections.map_π_eq]
  infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Final.Type

Goal state before:
pp: case refine_2
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
P : D ⥤ Type w
inst✝ : F.Final
x : P.ColimitType
⊢ ∃ a, F.colimitTypePrecomp P a = x

Tactic:
obtain ⟨X, x, rfl⟩ := P.ιColimitType_jointly_surjective x
    let Y : StructuredArrow X F := Classical.arbitrary _
    exact ⟨(F ⋙ P).ιColimitType Y.right (P.map Y.hom x), by simp⟩

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Final.Type

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
P : D ⥤ Type w
inst✝ : F.Final
⊢ Function.Bijective (F.colimitTypePrecomp P)

Tactic:
refine ⟨?_, fun x ↦ ?_⟩
  · have h (Y : D) : ∃ (a : P.obj Y → (F ⋙ P).ColimitType), ∀ (j : StructuredArrow Y F),
        (F ⋙ P).ιColimitType j.right ∘ P.map j.hom = a := by
      apply constant_of_preserves_morphisms'
      intro Z₁ Z₂ f
      ext x
      dsimp
      rw [← (F ⋙ P).ιColimitType_map f.right, comp_map]
      simp [← comp_apply, ← Functor.map_comp]
    choose φ hφ using h
    let c : P.CoconeTypes :=
      { pt := (F ⋙ P).ColimitType
        ι Y := φ Y
        ι_naturality {Y₁ Y₂} f := by
          ext
          have X : StructuredArrow Y₂ F := Classical.arbitrary _
          rw [← hφ Y₂ X, ← hφ Y₁ ((StructuredArrow.map f).obj X)]
          simp }
    refine Function.RightInverse.injective (g := (P.descColimitType c)) (fun x ↦ ?_)
    obtain ⟨X, x, rfl⟩ := (F ⋙ P).ιColimitType_jointly_surjective x
    simp [c, ← hφ (F.obj X) (StructuredArrow.mk (𝟙 _))]
  · obtain ⟨X, x, rfl⟩ := P.ιColimitType_jointly_surjective x
    let Y : StructuredArrow X F := Classical.arbitrary _
    exact ⟨(F ⋙ P).ιColimitType Y.right (P.map Y.hom x), by simp⟩

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Opens

Goal state before:
pp: case mpr
X Y : TopCat
f : X ⟶ Y
hf : IsInducing ⇑(ConcreteCategory.hom f)
V : Opens ↑Y
t : Set ↑Y
ht : IsOpen t
hU : IsOpen (⇑(ConcreteCategory.hom f) ⁻¹' t)
⊢ (Opens.map f).obj V ≤ { carrier := ⇑(ConcreteCategory.hom f) ⁻¹' t, is_open' := hU } →
    V ≤ hf.functorObj { carrier := ⇑(ConcreteCategory.hom f) ⁻¹' t, is_open' := hU }

Tactic:
intro h x hx

Goal state after:
case mpr
X Y : TopCat
f : X ⟶ Y
hf : IsInducing ⇑(ConcreteCategory.hom f)
V : Opens ↑Y
t : Set ↑Y
ht : IsOpen t
hU : IsOpen (⇑(ConcreteCategory.hom f) ⁻¹' t)
h : (Opens.map f).obj V ≤ { carrier := ⇑(ConcreteCategory.hom f) ⁻¹' t, is_open' := hU }
x : ↑Y
hx : x ∈ V
⊢ x ∈ hf.functorObj { carrier := ⇑(ConcreteCategory.hom f) ⁻¹' t, is_open' := hU }
Module: Mathlib.Topology.Category.TopCat.Opens

Goal state before:
pp: case refine_2
X : TopCat
⊢ ∀ (X_1 Y : Opens ↑((toTopCat X).obj ⊤)) (f : X_1 ⟶ Y),
    ⋯.functor.map f = eqToHom ⋯ ≫ (map (inclusionTopIso X).inv).map f ≫ eqToHom ⋯

Tactic:
· subsingleton

Goal state after:
Module: Mathlib.Topology.Sheaves.SheafCondition.Sites

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
F : TopCat.Presheaf C Y
U : Opens ↑X
⊢ IsCofiltered (StructuredArrow U (Opens.map f))

Tactic:
refine @IsCofiltered.mk _ _ ?_ ?_

Goal state after:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
F : TopCat.Presheaf C Y
U : Opens ↑X
⊢ IsCofilteredOrEmpty (StructuredArrow U (Opens.map f))

case refine_2
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
F : TopCat.Presheaf C Y
U : Opens ↑X
⊢ Nonempty (StructuredArrow U (Opens.map f))
Module: Mathlib.Topology.Sheaves.SheafCondition.Sites

Goal state before:
pp: X Y : TopCat
f : X ⟶ Y
U : Opens ↑Y
S : Sieve U
⊢ S ∈ (Opens.grothendieckTopology ↑Y) U →
    Sieve.functorPushforward (Opens.map f) S ∈ (Opens.grothendieckTopology ↑X) ((Opens.map f).obj U)

Tactic:
hS

Goal state after:
X Y : TopCat
f : X ⟶ Y
U : Opens ↑Y
S : Sieve U
hS : S ∈ (Opens.grothendieckTopology ↑Y) U
⊢ Sieve.functorPushforward (Opens.map f) S ∈ (Opens.grothendieckTopology ↑X) ((Opens.map f).obj U)
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent

Goal state before:
pp: C✝ : Type u₁
inst✝³ : Category.{v₁, u₁} C✝
J✝ : GrothendieckTopology C✝
R✝ : Sheaf J✝ RingCat
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
R : Sheaf J RingCat
inst✝¹ : HasSheafify J AddCommGrpCat
inst✝ : J.WEqualsLocallyBijective AddCommGrpCat
ι σ : Type u
M : SheafOfModules R
f : free ι ⟶ free σ
g : free σ ⟶ M
H : f ≫ g = 0
H' : IsColimit (CokernelCofork.ofπ g H)
h : cokernel f ≅ M := (H'.coconePointUniqueUpToIso (colimit.isColimit (parallelPair f 0))).symm
h' : Abelian.image f ≅ kernel (generatorsOfIsCokernelFree f g H H').π :=
  kernel.mapIso (cokernel.π f) (generatorsOfIsCokernelFree f g H H').π (Iso.refl (free σ)) h ⋯
comp_aux : Abelian.factorThruImage f ≫ h'.hom = kernel.lift (generatorsOfIsCokernelFree f g H H').π f ⋯
⊢ Epi
    ((kernel (generatorsOfIsCokernelFree f g H H').π).freeHomEquiv.symm
      ((kernel (generatorsOfIsCokernelFree f g H H').π).freeHomEquiv
        (kernel.lift (generatorsOfIsCokernelFree f g H H').π f ⋯)))

Tactic:
rw [← comp_aux, Equiv.symm_apply_apply]

Goal state after:
C✝ : Type u₁
inst✝³ : Category.{v₁, u₁} C✝
J✝ : GrothendieckTopology C✝
R✝ : Sheaf J✝ RingCat
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
R : Sheaf J RingCat
inst✝¹ : HasSheafify J AddCommGrpCat
inst✝ : J.WEqualsLocallyBijective AddCommGrpCat
ι σ : Type u
M : SheafOfModules R
f : free ι ⟶ free σ
g : free σ ⟶ M
H : f ≫ g = 0
H' : IsColimit (CokernelCofork.ofπ g H)
h : cokernel f ≅ M := (H'.coconePointUniqueUpToIso (colimit.isColimit (parallelPair f 0))).symm
h' : Abelian.image f ≅ kernel (generatorsOfIsCokernelFree f g H H').π :=
  kernel.mapIso (cokernel.π f) (generatorsOfIsCokernelFree f g H H').π (Iso.refl (free σ)) h ⋯
comp_aux : Abelian.factorThruImage f ≫ h'.hom = kernel.lift (generatorsOfIsCokernelFree f g H H').π f ⋯
⊢ Epi (Abelian.factorThruImage f ≫ h'.hom)
Module: Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
FC : C → C → Type u_2
CC : C → Type u_3
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
inst✝² : HasLimitsOfSize.{x, x, v_1, u_1} C
inst✝¹ : (CategoryTheory.forget C).ReflectsIsomorphisms
inst✝ : PreservesLimitsOfSize.{x, x, v_1, u_3, u_1, u_3 + 1} (CategoryTheory.forget C)
X : TopCat
F : Sheaf C X
ι : Type u_4
U : ι → Opens ↑X
V : Opens ↑X
G : Sheaf C X
f : F ⟶ G
s : ToType (F.obj.obj (op (iSup U)))
t : ToType (G.obj.obj (op V))
sf : (i : ι) → ToType (F.obj.obj (op (U i)))
h : IsGluing F.obj U sf s
hV : ∀ (i : ι), U i ≤ V
ht :
  ∀ (i : ι), (ConcreteCategory.hom (f.hom.app (op (U i)))) (sf i) = (ConcreteCategory.hom (G.obj.map (homOfLE ⋯).op)) t
⊢ (ConcreteCategory.hom (f.hom.app (op (iSup U)))) s = (ConcreteCategory.hom (G.obj.map (homOfLE ⋯).op)) t

Tactic:
by
  refine eq_of_locally_eq G U _ _ (fun _ ↦ ?_)
  rw [← NatTrans.naturality_apply, h, ht, ← ConcreteCategory.comp_apply, ← Functor.map_comp]
  rfl

Goal state after:
Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections

Goal state before:
pp: case refine_2.single.left.pair.right.right
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
s : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
ι : ULift.{w, 0} WalkingPair → Opens ↑X := fun j ↦ WalkingPair.casesOn j.down U V
hι : U ⊔ V = iSup ι
⊢ (s.snd ≫ F.obj.map (homOfLE ⋯).op) ≫ F.obj.map (eqToHom ⋯).op =
    (s.fst ≫ F.presheaf.map (homOfLE ⋯).op) ≫ F.obj.map (eqToHom ⋯).op

Tactic:
Category.assoc,

Goal state after:
case refine_2.single.left.pair.right.right
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
s : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
ι : ULift.{w, 0} WalkingPair → Opens ↑X := fun j ↦ WalkingPair.casesOn j.down U V
hι : U ⊔ V = iSup ι
⊢ s.snd ≫ F.obj.map (homOfLE ⋯).op ≫ F.obj.map (eqToHom ⋯).op =
    (s.fst ≫ F.presheaf.map (homOfLE ⋯).op) ≫ F.obj.map (eqToHom ⋯).op
Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections

Goal state before:
pp: case refine_2.single.left.pair.right.right
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
s : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
ι : ULift.{w, 0} WalkingPair → Opens ↑X := fun j ↦ WalkingPair.casesOn j.down U V
hι : U ⊔ V = iSup ι
⊢ s.snd ≫ F.obj.map (homOfLE ⋯).op ≫ F.obj.map (eqToHom ⋯).op =
    (s.fst ≫ F.presheaf.map (homOfLE ⋯).op) ≫ F.obj.map (eqToHom ⋯).op

Tactic:
Category.assoc,

Goal state after:
case refine_2.single.left.pair.right.right
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
s : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
ι : ULift.{w, 0} WalkingPair → Opens ↑X := fun j ↦ WalkingPair.casesOn j.down U V
hι : U ⊔ V = iSup ι
⊢ s.snd ≫ F.obj.map (homOfLE ⋯).op ≫ F.obj.map (eqToHom ⋯).op =
    s.fst ≫ F.presheaf.map (homOfLE ⋯).op ≫ F.obj.map (eqToHom ⋯).op
Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
s : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
⊢ (⋯.some.lift
          { pt := s.pt,
            π :=
              {
                app := fun X_1 ↦
                  Opposite.casesOn X_1 fun unop ↦
                    Pairwise.casesOn unop (fun a ↦ ULift.casesOn a fun down ↦ WalkingPair.casesOn down s.fst s.snd)
                      fun a a_1 ↦
                      ULift.casesOn a fun down ↦
                        WalkingPair.casesOn down (s.fst ≫ F.obj.map (homOfLE ⋯).op) (s.snd ≫ F.obj.map (homOfLE ⋯).op),
                naturality := ⋯ } } ≫
        F.obj.map (eqToHom ⋯).op) ≫
      F.obj.map (homOfLE ⋯).op =
    s.fst

Tactic:
Category.assoc,

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
s : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
⊢ ⋯.some.lift
        { pt := s.pt,
          π :=
            {
              app := fun X_1 ↦
                Opposite.casesOn X_1 fun unop ↦
                  Pairwise.casesOn unop (fun a ↦ ULift.casesOn a fun down ↦ WalkingPair.casesOn down s.fst s.snd)
                    fun a a_1 ↦
                    ULift.casesOn a fun down ↦
                      WalkingPair.casesOn down (s.fst ≫ F.obj.map (homOfLE ⋯).op) (s.snd ≫ F.obj.map (homOfLE ⋯).op),
              naturality := ⋯ } } ≫
      F.obj.map (eqToHom ⋯).op ≫ F.obj.map (homOfLE ⋯).op =
    s.fst