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

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
A : Type w
inst✝¹ : Category.{w', w} A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝ : G.IsCocontinuous J K
F : Cᵒᵖ ⥤ A
hF : Presheaf.IsSheaf J F
R : Dᵒᵖ ⥤ A
α : G.op ⋙ R ⟶ F
hR : (Functor.RightExtension.mk R α).IsPointwiseRightKanExtension
X : D
S : K.Cover X
s : Multifork (S.index R)
i : S.Arrow
j : StructuredArrow (op i.Y) G.op
⊢ (lift hF hR s ≫ R.map i.f.op) ≫ ((Functor.RightExtension.mk R α).coneAt (op i.Y)).π.app j =
    s.ι i ≫ ((Functor.RightExtension.mk R α).coneAt (op i.Y)).π.app j

Tactic:
have eq := fac' hF hR s (StructuredArrow.mk (i.f.op ≫ j.hom))

Goal state after:
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
A : Type w
inst✝¹ : Category.{w', w} A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝ : G.IsCocontinuous J K
F : Cᵒᵖ ⥤ A
hF : Presheaf.IsSheaf J F
R : Dᵒᵖ ⥤ A
α : G.op ⋙ R ⟶ F
hR : (Functor.RightExtension.mk R α).IsPointwiseRightKanExtension
X : D
S : K.Cover X
s : Multifork (S.index R)
i : S.Arrow
j : StructuredArrow (op i.Y) G.op
eq :
  lift hF hR s ≫ R.map (StructuredArrow.mk (i.f.op ≫ j.hom)).hom ≫ α.app (StructuredArrow.mk (i.f.op ≫ j.hom)).right =
    liftAux hF α s (StructuredArrow.mk (i.f.op ≫ j.hom)).hom.unop
⊢ (lift hF hR s ≫ R.map i.f.op) ≫ ((Functor.RightExtension.mk R α).coneAt (op i.Y)).π.app j =
    s.ι i ≫ ((Functor.RightExtension.mk R α).coneAt (op i.Y)).π.app j
Module: Mathlib.CategoryTheory.Sites.CoverLifting

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
A : Type w
inst✝³ : Category.{w', w} A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝² : G.IsCocontinuous J K
inst✝¹ : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F
inst✝ : G.IsContinuous J K
F : Sheaf J A
⊢ (G.sheafPushforwardContinuousCompSheafToPresheafIso A J K).symm.inv.app
        ((G.sheafPushforwardCocontinuous A J K).obj F) ≫
      ((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).map
          ((G.sheafPushforwardCocontinuousCompSheafToPresheafIso A J K).symm.inv.app F) ≫
        (G.op.ranAdjunction A).counit.app ((sheafToPresheaf J A).obj F) =
    (G.op.ranAdjunction A).counit.app F.obj

Tactic:
by cat_disch

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
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
⊢ ∃! t, x.IsAmalgamation t

Tactic:
apply existsUnique_of_exists_of_unique

Goal state after:
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
⊢ ∃ x_1, x.IsAmalgamation x_1

case hunique
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
⊢ ∀ (y₁ y₂ : (F.op ⋙ G.obj).obj (op X)), x.IsAmalgamation y₁ → x.IsAmalgamation y₂ → y₁ = y₂
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.SheafEquiv

Goal state before:
pp: case refine_2
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
W₁ : C
g₁ : G.obj W₁ ⟶ G.obj U
W₂ : C
g₂ : G.obj W₂ ⟶ G.obj U
i : W₂ ⟶ W₁
hi✝ : (StructuredArrow.mk (op g₁)).hom ≫ G.op.map (op i) = (StructuredArrow.mk (op g₂)).hom
hi : G.map i ≫ g₁ = g₂
⊢ 𝟙 X ≫ ⋯.amalgamate ⟨G.imageSieve g₂, ⋯⟩ (fun I ↦ f ≫ Y.obj.map (l I.Y W₂ U I.f g₂ ⋯).op) ⋯ =
    ⋯.amalgamate ⟨G.imageSieve g₁, ⋯⟩ (fun I ↦ f ≫ Y.obj.map (l I.Y W₁ U I.f g₁ ⋯).op) ⋯ ≫ Y.obj.map (op i)

Tactic:
subst hi

Goal state after:
case refine_2
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
W₁ : C
g₁ : G.obj W₁ ⟶ G.obj U
W₂ : C
i : W₂ ⟶ W₁
hi : (StructuredArrow.mk (op g₁)).hom ≫ G.op.map (op i) = (StructuredArrow.mk (op (G.map i ≫ g₁))).hom
⊢ 𝟙 X ≫ ⋯.amalgamate ⟨G.imageSieve (G.map i ≫ g₁), ⋯⟩ (fun I ↦ f ≫ Y.obj.map (l I.Y W₂ U I.f (G.map i ≫ g₁) ⋯).op) ⋯ =
    ⋯.amalgamate ⟨G.imageSieve g₁, ⋯⟩ (fun I ↦ f ≫ Y.obj.map (l I.Y W₁ U I.f g₁ ⋯).op) ⋯ ≫ Y.obj.map (op i)
Module: Mathlib.CategoryTheory.Sites.InducedTopology

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
K : GrothendieckTopology D
inst✝ : LocallySmall.{max u₁ v₁ u₂ v₂, v₁, u₁} C
X : C
S : Sieve X
G : (Cᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)) ⥤ Dᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)
adj : G ⊣ (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max u₁ v₁ u₂ v₂))).obj F.op
⊢ (∀ ⦃Y : C⦄ (f : Y ⟶ X), K.W (G.map (Sieve.shrinkFunctor.{max u₁ v₁ u₂ v₂, v₁, u₁} (Sieve.pullback f S)).ι)) →
    S ∈ (F.inducedTopology K) X

Tactic:
· intro H
    apply Sheaf.mem_finestTopology_of_forall_isSheafFor
    rintro - ⟨P, rfl⟩ Y f
    dsimp
    rw [Presieve.isSheafFor_iff_bijective_shrinkFunctor_ι_comp]
    exact (adj.map_comp_bijective_iff _ _).mp (H f _ P.property)

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

Goal state before:
pp: case mp
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
K : GrothendieckTopology D
e : C ≌ D
inst✝¹ : e.functor.IsCocontinuous J K
inst✝ : e.inverse.IsCocontinuous K J
X : C
S : Sieve X
⊢ Sieve.functorPushforward e.functor S ∈ K (e.functor.obj X) → S ∈ J X

Tactic:
intro H
      refine J.superset_covering ?_ (e.functor.cover_lift J K H)
      rw [(Sieve.fullyFaithfulFunctorGaloisCoinsertion e.functor X).u_l_eq S]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
S : C
E F : PreOneHypercover S
e : E ≅ F
i j : F.I₀
k : F.I₁ i j
⊢ e.hom.s₁ (e.inv.s₁ k) = (congrIndexOneOfEq ⋯ ⋯) k

Tactic:
by
  obtain ⟨hs₀, hh₀, hs₁, hh₁⟩ := PreOneHypercover.Hom.ext'_iff.mp e.inv_hom_id
  simpa using! hs₁ i j k

Goal state after:
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
e : C ≌ D
inst✝³ : IsDenseSubsite K J e.inverse
A : Type u_1
inst✝² : Category.{v_1, u_1} A
B : Type u_2
inst✝¹ : Category.{v_2, u_2} B
F : A ⥤ B
inst✝ : K.HasSheafCompose F
P : Cᵒᵖ ⥤ A
hP : Presheaf.IsSheaf J P
⊢ Presheaf.IsSheaf J (P ⋙ F)

Tactic:
have hP' : Presheaf.IsSheaf K (e.inverse.op ⋙ P ⋙ F) := by
      change Presheaf.IsSheaf K ((_ ⋙ _) ⋙ _)
      apply HasSheafCompose.isSheaf
      exact e.inverse.op_comp_isSheaf K J ⟨P, hP⟩
    replace hP' : Presheaf.IsSheaf J (e.functor.op ⋙ e.inverse.op ⋙ P ⋙ F) :=
      e.functor.op_comp_isSheaf _ _ ⟨_, hP'⟩
    exact (Presheaf.isSheaf_of_iso_iff ((isoWhiskerRight e.op.unitIso.symm (P ⋙ F)))).mp hP'

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Connected

Goal state before:
pp: J : Type u'
inst✝³ : Category.{v', u'} J
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
K : C ⥤ D
inst✝ : IsConnected J
B : D
F : J ⥤ CostructuredArrow K B
c : Cone (F ⋙ proj K B)
⊢ (proj K B).mapCone (raiseCone c) = c

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Sites.CoversTop.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
I : Type u_1
Y : I → C
x : FamilyOfElementsOnObjects F Y
hx : x.IsCompatible
hY : J.CoversTop Y
hF : IsSheaf J F
H : Presieve.IsSheaf J F
⊢ ∃! s, ∀ (i : I), ↑s (Opposite.op (Y i)) = x i

Tactic:
apply existsUnique_of_exists_of_unique

Goal state after:
case hex
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
I : Type u_1
Y : I → C
x : FamilyOfElementsOnObjects F Y
hx : x.IsCompatible
hY : J.CoversTop Y
hF : IsSheaf J F
H : Presieve.IsSheaf J F
⊢ ∃ x_1, ∀ (i : I), ↑x_1 (Opposite.op (Y i)) = x i

case hunique
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
I : Type u_1
Y : I → C
x : FamilyOfElementsOnObjects F Y
hx : x.IsCompatible
hY : J.CoversTop Y
hF : IsSheaf J F
H : Presieve.IsSheaf J F
⊢ ∀ (y₁ y₂ : ↑F.sections),
    (∀ (i : I), ↑y₁ (Opposite.op (Y i)) = x i) → (∀ (i : I), ↑y₂ (Opposite.op (Y i)) = x i) → y₁ = y₂
Module: Mathlib.CategoryTheory.Sites.CoversTop.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
I : Type u_1
Y : I → C
x : FamilyOfElementsOnObjects F Y
hx : x.IsCompatible
hY : J.CoversTop Y
hF : IsSheaf J F
H : Presieve.IsSheaf J F
s : (X : C) → F.obj (Opposite.op X) := fun X ↦ ⋯.amalgamate (x.familyOfElements X) ⋯
hs : ∀ {X : C} (i : I) (f : X ⟶ Y i), s X = (ConcreteCategory.hom (F.map f.op)) (x i)
W X : C
a : W ⟶ X
i : I
⊢ ∀ (x : W ⟶ Y i), (ConcreteCategory.hom (F.map a.op)) (s X) = s W

Tactic:
b

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
I : Type u_1
Y : I → C
x : FamilyOfElementsOnObjects F Y
hx : x.IsCompatible
hY : J.CoversTop Y
hF : IsSheaf J F
H : Presieve.IsSheaf J F
s : (X : C) → F.obj (Opposite.op X) := fun X ↦ ⋯.amalgamate (x.familyOfElements X) ⋯
hs : ∀ {X : C} (i : I) (f : X ⟶ Y i), s X = (ConcreteCategory.hom (F.map f.op)) (x i)
W X : C
a : W ⟶ X
i : I
b : W ⟶ Y i
⊢ (ConcreteCategory.hom (F.map a.op)) (s X) = s W
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
E : PreOneHypercover Y
i₁ i₂ : E.I₀
W : Over X
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
Y✝ : C
f✝ : Y✝ ⟶ W.left
k : (E.map (Over.forget X)).I₁ i₁ i₂
b : Y✝ ⟶ (E.map (Over.forget X)).Y k
hb₁ : f✝ ≫ Over.Hom.left p₁ = b ≫ (E.map (Over.forget X)).p₁ k
hb₂ : f✝ ≫ Over.Hom.left p₂ = b ≫ (E.map (Over.forget X)).p₂ k
⊢ Over.homMk f✝ ⋯ ≫ p₁ = Over.homMk b ⋯ ≫ E.p₁ k

Tactic:
by cat_disch

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
E : PreOneHypercover Y
i₁ i₂ : E.I₀
W : Over X
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
Y✝ : C
f✝ : Y✝ ⟶ W.left
k : (E.map (Over.forget X)).I₁ i₁ i₂
b : Y✝ ⟶ (E.map (Over.forget X)).Y k
hb₁ : f✝ ≫ Over.Hom.left p₁ = b ≫ (E.map (Over.forget X)).p₁ k
hb₂ : f✝ ≫ Over.Hom.left p₂ = b ≫ (E.map (Over.forget X)).p₂ k
⊢ Over.homMk f✝ ⋯ ≫ p₂ = Over.homMk b ⋯ ≫ E.p₂ k

Tactic:
by cat_disch

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : Over X
S : Sieve Z.left
W : Over Y
g : W ⟶ (Over.map f).obj Z
hg : ((overEquiv ((Over.map f).obj Z)).symm S).arrows g
⊢ g = Over.homMk (𝟙 W.left) ⋯ ≫ (Over.map f).map (Over.homMk (Over.Hom.left g) ⋯)

Tactic:
by cat_disch

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

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
D' : Type u₃
inst✝⁵ : Category.{v₃, u₃} D'
D'' : Type u₄
inst✝⁴ : Category.{v₄, u₄} D''
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
S : Sheaf J RingCat
R : Sheaf K RingCat
inst✝³ : F.IsContinuous J K
φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R
inst✝² : (PresheafOfModules.pushforward φ.hom).IsRightAdjoint
inst✝¹ : HasWeakSheafify K AddCommGrpCat
inst✝ : K.WEqualsLocallyBijective AddCommGrpCat
X'✝ X✝ : SheafOfModules S
Y✝ : SheafOfModules R
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (pushforward φ).obj Y✝
⊢ (((PresheafOfModules.sheafificationAdjunction (𝟙 R.obj)).homEquiv
              ((PresheafOfModules.pullback φ.hom).obj ((forget S).obj X'✝)) Y✝).trans
          (((PresheafOfModules.pullbackPushforwardAdjunction φ.hom).homEquiv X'✝.val Y✝.val).trans
            (fullyFaithfulForget S).homEquiv.symm)).symm
      (f✝ ≫ g✝) =
    (forget S ⋙ PresheafOfModules.pullback φ.hom ⋙ PresheafOfModules.sheafification (𝟙 R.obj)).map f✝ ≫
      (((PresheafOfModules.sheafificationAdjunction (𝟙 R.obj)).homEquiv
                ((PresheafOfModules.pullback φ.hom).obj ((forget S).obj X✝)) Y✝).trans
            (((PresheafOfModules.pullbackPushforwardAdjunction φ.hom).homEquiv X✝.val Y✝.val).trans
              (fullyFaithfulForget S).homEquiv.symm)).symm
        g✝

Tactic:
dsimp [Functor.FullyFaithful.homEquiv]

Goal state after:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
D' : Type u₃
inst✝⁵ : Category.{v₃, u₃} D'
D'' : Type u₄
inst✝⁴ : Category.{v₄, u₄} D''
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
S : Sheaf J RingCat
R : Sheaf K RingCat
inst✝³ : F.IsContinuous J K
φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R
inst✝² : (PresheafOfModules.pushforward φ.hom).IsRightAdjoint
inst✝¹ : HasWeakSheafify K AddCommGrpCat
inst✝ : K.WEqualsLocallyBijective AddCommGrpCat
X'✝ X✝ : SheafOfModules S
Y✝ : SheafOfModules R
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (pushforward φ).obj Y✝
⊢ ((PresheafOfModules.sheafificationAdjunction (𝟙 R.obj)).homEquiv ((PresheafOfModules.pullback φ.hom).obj X'✝.val)
          Y✝).symm
      (((PresheafOfModules.pullbackPushforwardAdjunction φ.hom).homEquiv X'✝.val Y✝.val).symm (f✝.val ≫ g✝.val)) =
    (PresheafOfModules.sheafification (𝟙 R.obj)).map ((PresheafOfModules.pullback φ.hom).map f✝.val) ≫
      ((PresheafOfModules.sheafificationAdjunction (𝟙 R.obj)).homEquiv ((PresheafOfModules.pullback φ.hom).obj X✝.val)
            Y✝).symm
        (((PresheafOfModules.pullbackPushforwardAdjunction φ.hom).homEquiv X✝.val Y✝.val).symm g✝.val)
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.Algebra.Category.ModuleCat.Sheaf.PullbackFree

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
S : Sheaf J RingCat
R : Sheaf K RingCat
inst✝ : F.IsContinuous J K
φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R
X✝ Y✝ : Cᵒᵖ
f : X✝ ⟶ Y✝
⊢ (unit S).val.map f ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom (S.obj.map f))).map
        (ModuleCat.homMk ((forget₂ RingCat AddCommGrpCat).map (φ.hom.app Y✝)) ⋯) =
    ModuleCat.homMk ((forget₂ RingCat AddCommGrpCat).map (φ.hom.app X✝)) ⋯ ≫ ((pushforward φ).obj (unit R)).val.map f

Tactic:
by
    ext
    exact ConcreteCategory.congr_hom (φ.hom.naturality f) _

Goal state after:
Module: Mathlib.CategoryTheory.Category.GaloisConnection

Goal state before:
pp: X✝ : Type u
Y✝ : Type v
inst✝¹ : Preorder X✝
inst✝ : Preorder Y✝
l : X✝ → Y✝
u : Y✝ → X✝
gc : GaloisConnection l u
X : X✝
Y : Y✝
⊢ Function.LeftInverse (fun f ↦ CategoryTheory.homOfLE ⋯) fun f ↦ CategoryTheory.homOfLE ⋯

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Category.GaloisConnection

Goal state before:
pp: X✝ : Type u
Y✝ : Type v
inst✝¹ : Preorder X✝
inst✝ : Preorder Y✝
l : X✝ → Y✝
u : Y✝ → X✝
gc : GaloisConnection l u
X : X✝
Y : Y✝
⊢ Function.RightInverse (fun f ↦ CategoryTheory.homOfLE ⋯) fun f ↦ CategoryTheory.homOfLE ⋯

Tactic:
by cat_disch

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

Goal state before:
pp: X✝ Y✝ Z : TopCat
U✝ V W : Opens ↑X✝
X Y : TopCat
H : X ≅ Y
U : Opens ↑Y
⊢ (𝟭 (Opens ↑Y)).obj U = ((mapMapIso H).functor ⋙ (mapMapIso H).inverse).obj U

Tactic:
by cat_disch

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

Goal state before:
pp: X✝ Y✝ Z : TopCat
U V W : Opens ↑X✝
X Y : TopCat
H : X ≅ Y
⊢ ∀ {X_1 Y_1 : Opens ↑Y} (f : X_1 ⟶ Y_1),
    (𝟭 (Opens ↑Y)).map f ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ ((mapMapIso H).functor ⋙ (mapMapIso H).inverse).map f

Tactic:
by cat_disch

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

Goal state before:
pp: X✝ Y✝ Z : TopCat
U✝ V W : Opens ↑X✝
X Y : TopCat
H : X ≅ Y
U : Opens ↑X
⊢ ((mapMapIso H).inverse ⋙ (mapMapIso H).functor).obj U = (𝟭 (Opens ↑X)).obj U

Tactic:
by cat_disch

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

Goal state before:
pp: X✝ Y✝ Z : TopCat
U V W : Opens ↑X✝
X Y : TopCat
H : X ≅ Y
⊢ ∀ {X_1 Y_1 : Opens ↑X} (f : X_1 ⟶ Y_1),
    ((mapMapIso H).inverse ⋙ (mapMapIso H).functor).map f ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ (𝟭 (Opens ↑X)).map f

Tactic:
by cat_disch

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

Goal state before:
pp: C✝ : Type u₁
inst✝⁹ : Category.{v₁, u₁} C✝
D✝ : Type u₂
inst✝⁸ : Category.{v₂, u₂} D✝
D' : Type u₃
inst✝⁷ : Category.{v₃, u₃} D'
D'' : Type u₄
inst✝⁶ : Category.{v₄, u₄} D''
J✝ : GrothendieckTopology C✝
K✝ : GrothendieckTopology D✝
F✝ : C✝ ⥤ D✝
S✝ : Sheaf J✝ RingCat
R : Sheaf K✝ RingCat
inst✝⁵ : F✝.IsContinuous J✝ K✝
φ✝ : S✝ ⟶ (F✝.sheafPushforwardContinuous RingCat J✝ K✝).obj R
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : GrothendieckTopology C
K : GrothendieckTopology D
F G H : C ⥤ D
T : Sheaf J RingCat
S : Sheaf K RingCat
inst✝² : F.IsContinuous J K
inst✝¹ : G.IsContinuous J K
inst✝ : H.IsContinuous J K
φ : T ⟶ (G.sheafPushforwardContinuous RingCat J K).obj S
⊢ φ = φ ≫ (sheafPushforwardContinuousNatTrans (𝟙 G) RingCat J K).app S

Tactic:
by cat_disch

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
T : Sheaf J RingCat
S : Sheaf K RingCat
inst✝ : G.IsContinuous J K
φ : T ⟶ (G.sheafPushforwardContinuous RingCat J K).obj S
⊢ pushforwardNatTrans φ (𝟙 G) = (pushforwardCongr ⋯).hom

Tactic:
by cat_disch

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

Goal state before:
pp: T : Type u
inst✝ : TopologicalSpace T
X : Opens T
S : Presieve X
Ti : ⦃Y : Opens T⦄ → (f : Y ⟶ X) → S f → Presieve Y
hS : S ∈ {R | ∀ x ∈ X, ∃ U f, R f ∧ x ∈ U}
hTi : ∀ ⦃Y : Opens T⦄ (f : Y ⟶ X) (H : S f), Ti f H ∈ {R | ∀ x ∈ Y, ∃ U f, R f ∧ x ∈ U}
x : T
hx : x ∈ X
⊢ ∃ U f, S.bind Ti f ∧ x ∈ U

Tactic:
rcases hS x hx with ⟨U, f, hf, hU⟩
    rcases hTi f hf x hU with ⟨V, g, hg, hV⟩
    exact ⟨_, _, ⟨_, g, f, hf, hg, rfl⟩, hV⟩

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

Goal state before:
pp: C✝ : Type u₁
inst✝⁹ : Category.{v₁, u₁} C✝
D✝ : Type u₂
inst✝⁸ : Category.{v₂, u₂} D✝
D' : Type u₃
inst✝⁷ : Category.{v₃, u₃} D'
D'' : Type u₄
inst✝⁶ : Category.{v₄, u₄} D''
J✝ : GrothendieckTopology C✝
K✝ : GrothendieckTopology D✝
F✝ : C✝ ⥤ D✝
S✝ : Sheaf J✝ RingCat
R : Sheaf K✝ RingCat
inst✝⁵ : F✝.IsContinuous J✝ K✝
φ✝¹ : S✝ ⟶ (F✝.sheafPushforwardContinuous RingCat J✝ K✝).obj R
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : GrothendieckTopology C
K : GrothendieckTopology D
F G H : C ⥤ D
T : Sheaf J RingCat
S : Sheaf K RingCat
inst✝² : F.IsContinuous J K
inst✝¹ : G.IsContinuous J K
inst✝ : H.IsContinuous J K
φ✝ : T ⟶ (G.sheafPushforwardContinuous RingCat J K).obj S
α : F ⟶ G
β : G ⟶ H
φ : T ⟶ (H.sheafPushforwardContinuous RingCat J K).obj S
⊢ (φ ≫ (sheafPushforwardContinuousNatTrans β RingCat J K).app S) ≫
      (sheafPushforwardContinuousNatTrans α RingCat J K).app S =
    φ ≫ (sheafPushforwardContinuousNatTrans (α ≫ β) RingCat J K).app S

Tactic:
by cat_disch

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : GrothendieckTopology C
K : GrothendieckTopology D
F G H : C ⥤ D
T : Sheaf J RingCat
S : Sheaf K RingCat
inst✝² : F.IsContinuous J K
inst✝¹ : G.IsContinuous J K
inst✝ : H.IsContinuous J K
α : F ⟶ G
β : G ⟶ H
φ : T ⟶ (H.sheafPushforwardContinuous RingCat J K).obj S
⊢ pushforwardNatTrans φ (α ≫ β) =
    pushforwardNatTrans φ β ≫
      pushforwardNatTrans (φ ≫ (sheafPushforwardContinuousNatTrans β RingCat J K).app S) α ≫ (pushforwardCongr ⋯).hom

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.Topology.Sheaves.Sheaf

Goal state before:
pp: X : TopCat
F : Presheaf (Discrete Unit) X
x✝² : Discrete Unit
U : Opens ↑X
S : Sieve U
x✝¹ : S ∈ (Opens.grothendieckTopology ↑X) U
x : Presieve.FamilyOfElements (F ⋙ coyoneda.obj (op x✝²)) S.arrows
x✝ : x.Compatible
⊢ (fun t ↦ x.IsAmalgamation t) (eqToHom ⋯)

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.Topology.Sheaves.Sheaf

Goal state before:
pp: X : TopCat
F : Presheaf (Discrete Unit) X
x✝³ : Discrete Unit
U : Opens ↑X
S : Sieve U
x✝² : S ∈ (Opens.grothendieckTopology ↑X) U
x : Presieve.FamilyOfElements (F ⋙ coyoneda.obj (op x✝³)) S.arrows
x✝¹ : x.Compatible
x✝ : (F ⋙ coyoneda.obj (op x✝³)).obj (op U)
⊢ (fun t ↦ x.IsAmalgamation t) x✝ → x✝ = eqToHom ⋯

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.Topology.Sheaves.Presheaf

Goal state before:
pp: C✝ : Type u
inst✝³ : Category.{v, u} C✝
X✝ : TopCat
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
X Y : TopCat
f g : X ⟶ Y
h : f = g
ℱ : Presheaf C X
U : (Opens ↑Y)ᵒᵖ
⊢ (Opens.map f).op.obj U = (Opens.map g).op.obj U

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.Topology.Sheaves.Presheaf

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
H₁ : X ≅ Y
ℱ : Presheaf C Y
𝒢 : Presheaf C X
H₂ : ℱ ⟶ (pushforward C H₁.hom).obj 𝒢
U : (Opens ↑X)ᵒᵖ
⊢ (pushforwardToOfIso H₁ H₂).app U = H₂.app (op ((Opens.map H₁.inv).obj (unop U))) ≫ 𝒢.map (eqToHom ⋯)

Tactic:
simp [pushforwardToOfIso, Equivalence.toAdjunction, Adjunction.homEquiv_counit]

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

Goal state before:
pp: X Y : TopCat
f : X ⟶ Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
this : Mono f
U : Opens ↑X
⊢ {d : Opens ↑Y} → (d ⟶ hf.functor.obj U) → (c' : Opens ↑X) × (hf.functor.obj c' ≅ d)

Tactic:
V

Goal state after:
X Y : TopCat
f : X ⟶ Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
this : Mono f
U : Opens ↑X
V : Opens ↑Y
⊢ (V ⟶ hf.functor.obj U) → (c' : Opens ↑X) × (hf.functor.obj c' ≅ V)