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

Goal state before:
pp: C : Type u
inst✝¹³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝¹² : Category.{t, w} D
inst✝¹¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝¹⁰ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁹ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝⁸ : ConcreteCategory D FD
inst✝⁷ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
inst✝⁶ : (forget D).ReflectsIsomorphisms
inst✝⁵ : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
K : Type w'
inst✝⁴ : SmallCategory K
inst✝³ : FinCategory K
inst✝² : HasLimitsOfShape K D
inst✝¹ : PreservesLimits (forget D)
inst✝ : ∀ (X : C), Small.{t, max u v} (J.Cover X)ᵒᵖ
e : K ≌ AsSmall (FinCategory.AsType K) := ⋯
this✝ : HasLimitsOfShape (AsSmall (FinCategory.AsType K)) D
this : FinCategory (AsSmall (FinCategory.AsType K))
F : AsSmall (FinCategory.AsType K) ⥤ Cᵒᵖ ⥤ D
⊢ ∀ {c : Cone F} (hc : IsLimit c), Nonempty (IsLimit ((plusPlusSheaf J D).mapCone c))

Tactic:
intro S

Goal state after:
C : Type u
inst✝¹³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝¹² : Category.{t, w} D
inst✝¹¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝¹⁰ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁹ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝⁸ : ConcreteCategory D FD
inst✝⁷ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
inst✝⁶ : (forget D).ReflectsIsomorphisms
inst✝⁵ : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
K : Type w'
inst✝⁴ : SmallCategory K
inst✝³ : FinCategory K
inst✝² : HasLimitsOfShape K D
inst✝¹ : PreservesLimits (forget D)
inst✝ : ∀ (X : C), Small.{t, max u v} (J.Cover X)ᵒᵖ
e : K ≌ AsSmall (FinCategory.AsType K) := (FinCategory.equivAsType K).symm.trans AsSmall.equiv
this✝ : HasLimitsOfShape (AsSmall (FinCategory.AsType K)) D
this : FinCategory (AsSmall (FinCategory.AsType K))
F : AsSmall (FinCategory.AsType K) ⥤ Cᵒᵖ ⥤ D
S : Cone F
⊢ ∀ (hc : IsLimit S), Nonempty (IsLimit ((plusPlusSheaf J D).mapCone S))
Module: Mathlib.CategoryTheory.Sites.LeftExact

Goal state before:
pp: C : Type u
inst✝¹⁴ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝¹³ : Category.{t, w} D
inst✝¹² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝¹¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
FD : D → D → Type u_1
CD : D → Type t
inst✝¹⁰ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝⁹ : ConcreteCategory D FD
inst✝⁸ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
inst✝⁷ : (forget D).ReflectsIsomorphisms
inst✝⁶ : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
K : Type w'
inst✝⁵ : SmallCategory K
inst✝⁴ : FinCategory K
inst✝³ : HasLimitsOfShape K D
inst✝² : PreservesLimits (forget D)
inst✝¹ : ∀ (X : C), Small.{t, max u v} (J.Cover X)ᵒᵖ
inst✝ : HasFiniteLimits D
⊢ ∀ (J_1 : Type t) {𝒥 : SmallCategory J_1} (x : FinCategory J_1), PreservesLimitsOfShape J_1 (plusPlusSheaf J D)

Tactic:
intros

Goal state after:
C : Type u
inst✝¹⁴ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝¹³ : Category.{t, w} D
inst✝¹² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝¹¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
FD : D → D → Type u_1
CD : D → Type t
inst✝¹⁰ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝⁹ : ConcreteCategory D FD
inst✝⁸ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
inst✝⁷ : (forget D).ReflectsIsomorphisms
inst✝⁶ : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
K : Type w'
inst✝⁵ : SmallCategory K
inst✝⁴ : FinCategory K
inst✝³ : HasLimitsOfShape K D
inst✝² : PreservesLimits (forget D)
inst✝¹ : ∀ (X : C), Small.{t, max u v} (J.Cover X)ᵒᵖ
inst✝ : HasFiniteLimits D
J✝ : Type t
𝒥✝ : SmallCategory J✝
x✝ : FinCategory J✝
⊢ PreservesLimitsOfShape J✝ (plusPlusSheaf J D)
Module: Mathlib.CategoryTheory.Adhesive.Basic

Goal state before:
pp: 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✝
D : Type u''
inst✝³ : Category.{v'', u''} D
inst✝² : Adhesive C
inst✝¹ : HasPullbacks C
inst✝ : HasPushouts C
W X Y Z : D ⥤ C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
hf : Mono f
H : IsPushout f g h i
x : D
⊢ IsVanKampenColimit
    ((Cocone.precompose (diagramIsoSpan (span f g ⋙ (evaluation D C).obj x)).inv).obj
      (((evaluation D C).obj x).mapCocone (PushoutCocone.mk h i ⋯)))

Tactic:
refine IsVanKampenColimit.of_iso ?_ (PushoutCocone.isoMk _).symm

Goal state after:
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✝
D : Type u''
inst✝³ : Category.{v'', u''} D
inst✝² : Adhesive C
inst✝¹ : HasPullbacks C
inst✝ : HasPushouts C
W X Y Z : D ⥤ C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
hf : Mono f
H : IsPushout f g h i
x : D
⊢ IsVanKampenColimit
    (PushoutCocone.mk ((((evaluation D C).obj x).mapCocone (PushoutCocone.mk h i ⋯)).ι.app WalkingSpan.left)
      ((((evaluation D C).obj x).mapCocone (PushoutCocone.mk h i ⋯)).ι.app WalkingSpan.right) ⋯)
Module: Mathlib.CategoryTheory.Adhesive.Basic

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u''
inst✝⁵ : Category.{v'', u''} D
F : C ⥤ D
inst✝⁴ : Adhesive D
H₁ : ∀ {X Y S : C} (f : X ⟶ S) (g : Y ⟶ S) [Mono f], HasPullback f g
H₂ : ∀ {X Y S : C} (f : S ⟶ X) (g : S ⟶ Y) [Mono f], HasPushout f g
inst✝³ : PreservesLimitsOfShape WalkingCospan F
inst✝² : ReflectsLimitsOfShape WalkingCospan F
inst✝¹ : PreservesColimitsOfShape WalkingSpan F
inst✝ : ReflectsColimitsOfShape WalkingSpan F
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
hf : Mono f
H : IsPushout f g h i
⊢ IsVanKampenColimit
    ((Cocone.precompose (diagramIsoSpan (span f g ⋙ F)).inv).obj (F.mapCocone (PushoutCocone.mk h i ⋯)))

Tactic:
refine IsVanKampenColimit.of_iso ?_ (PushoutCocone.isoMk _).symm

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u''
inst✝⁵ : Category.{v'', u''} D
F : C ⥤ D
inst✝⁴ : Adhesive D
H₁ : ∀ {X Y S : C} (f : X ⟶ S) (g : Y ⟶ S) [Mono f], HasPullback f g
H₂ : ∀ {X Y S : C} (f : S ⟶ X) (g : S ⟶ Y) [Mono f], HasPushout f g
inst✝³ : PreservesLimitsOfShape WalkingCospan F
inst✝² : ReflectsLimitsOfShape WalkingCospan F
inst✝¹ : PreservesColimitsOfShape WalkingSpan F
inst✝ : ReflectsColimitsOfShape WalkingSpan F
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
hf : Mono f
H : IsPushout f g h i
⊢ IsVanKampenColimit
    (PushoutCocone.mk ((F.mapCocone (PushoutCocone.mk h i ⋯)).ι.app WalkingSpan.left)
      ((F.mapCocone (PushoutCocone.mk h i ⋯)).ι.app WalkingSpan.right) ⋯)
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
X Y : C
c : BinaryCofan X Y
cofans : (X Y : C) → BinaryCofan X Y
colimits : (X Y : C) → IsColimit (cofans X Y)
cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PullbackCone f g
limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → IsLimit (cones f g)
h₁ :
  ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
    αX ≫ c.inl = (cofans X' Y').inl ≫ f →
      αY ≫ c.inr = (cofans X' Y').inr ≫ f →
        IsPullback (cofans X' Y').inl αX f c.inl ∧ IsPullback (cofans X' Y').inr αY f c.inr
h₂ : {Z : C} → (f : Z ⟶ c.pt) → IsColimit (BinaryCofan.mk (cones f c.inl).fst (cones f c.inr).fst)
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ c.inl = c'.inl ≫ f
hY : αY ≫ c.inr = c'.inr ≫ f
H₁ : IsPullback c'.inl αX f c.inl
H₂ : IsPullback c'.inr αY f c.inr
e₁ : X' ≅ (cones f c.inl).pt := H₁.isLimit.conePointUniqueUpToIso (limits f c.inl)
e₂ : Y' ≅ (cones f c.inr).pt := H₂.isLimit.conePointUniqueUpToIso (limits f c.inr)
he₁ : c'.inl = e₁.hom ≫ (cones f c.inl).fst
he₂ : c'.inr = e₂.hom ≫ (cones f c.inr).fst
⊢ IsColimit (BinaryCofan.mk (e₁.hom ≫ (cones f c.inl).fst) c'.inr)

Tactic:
he₂

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
X Y : C
c : BinaryCofan X Y
cofans : (X Y : C) → BinaryCofan X Y
colimits : (X Y : C) → IsColimit (cofans X Y)
cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PullbackCone f g
limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → IsLimit (cones f g)
h₁ :
  ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
    αX ≫ c.inl = (cofans X' Y').inl ≫ f →
      αY ≫ c.inr = (cofans X' Y').inr ≫ f →
        IsPullback (cofans X' Y').inl αX f c.inl ∧ IsPullback (cofans X' Y').inr αY f c.inr
h₂ : {Z : C} → (f : Z ⟶ c.pt) → IsColimit (BinaryCofan.mk (cones f c.inl).fst (cones f c.inr).fst)
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ c.inl = c'.inl ≫ f
hY : αY ≫ c.inr = c'.inr ≫ f
H₁ : IsPullback c'.inl αX f c.inl
H₂ : IsPullback c'.inr αY f c.inr
e₁ : X' ≅ (cones f c.inl).pt := H₁.isLimit.conePointUniqueUpToIso (limits f c.inl)
e₂ : Y' ≅ (cones f c.inr).pt := H₂.isLimit.conePointUniqueUpToIso (limits f c.inr)
he₁ : c'.inl = e₁.hom ≫ (cones f c.inl).fst
he₂ : c'.inr = e₂.hom ≫ (cones f c.inr).fst
⊢ IsColimit (BinaryCofan.mk (e₁.hom ≫ (cones f c.inl).fst) (e₂.hom ≫ (cones f c.inr).fst))
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
inst✝ : HasInitial C
c : BinaryCofan X Y
h : IsVanKampenColimit c
⊢ IsPullback (initial.to ((pair X Y).obj { as := WalkingPair.left }))
    (initial.to ((pair X Y).obj { as := WalkingPair.right })) c.inl c.inr

Tactic:
refine ((h (BinaryCofan.mk (initial.to Y) (𝟙 Y)) (mapPair (initial.to X) (𝟙 Y)) c.inr ?_
      (.of_discrete _)).mp ⟨?_⟩ ⟨WalkingPair.left⟩).flip
  · ext ⟨⟨⟩⟩ <;> simp
  · exact ((BinaryCofan.isColimit_iff_isIso_inr initialIsInitial _).mpr (by
      dsimp
      infer_instance)).some

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst✝² : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝¹ : ConcreteCategory D FD
J : GrothendieckTopology C
F₁ F₂ F₃ : Cᵒᵖ ⥤ D
φ : F₁ ⟶ F₂
ψ : F₂ ⟶ F₃
φψ : F₁ ⟶ F₃
fac : φ ≫ ψ = φψ
inst✝ : IsLocallyInjective J φψ
⊢ IsLocallyInjective J φ

Tactic:
subst fac

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst✝² : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝¹ : ConcreteCategory D FD
J : GrothendieckTopology C
F₁ F₂ F₃ : Cᵒᵖ ⥤ D
φ : F₁ ⟶ F₂
ψ : F₂ ⟶ F₃
inst✝ : IsLocallyInjective J (φ ≫ ψ)
⊢ IsLocallyInjective J φ
Module: Mathlib.CategoryTheory.Sites.PreservesSheafification

Goal state before:
pp: C : Type u
inst✝¹⁸ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u_1
B : Type u_2
inst✝¹⁷ : Category.{v_1, u_1} A
inst✝¹⁶ : Category.{v_2, u_2} B
F✝ : A ⥤ B
D : Type u_3
E : Type u_4
inst✝¹⁵ : Category.{v_3, u_3} D
inst✝¹⁴ : Category.{v_4, u_4} E
F : D ⥤ E
inst✝¹³ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst✝¹² : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst✝¹¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹⁰ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst✝⁹ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
inst✝⁸ : ∀ (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
FD : D → D → Type u_5
CD : D → Type u_6
FE : E → E → Type u_7
CE : E → Type u_8
inst✝⁷ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝⁶ : (X Y : E) → FunLike (FE X Y) (CE X) (CE Y)
instCCD : ConcreteCategory D FD
instCCE : ConcreteCategory E FE
inst✝⁵ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
inst✝⁴ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget E)
inst✝³ : PreservesLimitsOfSize.{max v u, max v u, v_3, u_6, u_3, u_6 + 1} (forget D)
inst✝² : PreservesLimitsOfSize.{max v u, max v u, v_4, u_8, u_4, u_8 + 1} (forget E)
inst✝¹ : (forget D).ReflectsIsomorphisms
inst✝ : (forget E).ReflectsIsomorphisms
P : Cᵒᵖ ⥤ D
⊢ IsIso ((sheafComposeNatTrans J F (plusPlusAdjunction J D) (plusPlusAdjunction J E)).app P)

Tactic:
rw [← isIso_iff_of_reflects_iso _ (sheafToPresheaf J E),
    sheafToPresheaf_map_sheafComposeNatTrans_eq_sheafifyCompIso_inv]
  infer_instance

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type w)
f : F ⟶ G
h₁ : ∀ (X : Cᵒᵖ), Function.Injective ⇑(ConcreteCategory.hom (f.hom.app X))
right✝ : IsLocallySurjective f
X : Cᵒᵖ
s : G.obj.obj X
H : Presieve.IsSheafFor F.obj (Presheaf.imageSieve f.hom s).arrows
t : Presieve.FamilyOfElements F.obj (Presheaf.imageSieve f.hom s).arrows :=
  fun Y g hg ↦ Presheaf.localPreimage f.hom s g hg
Y₁ Y₂ W : C
g₁ : W ⟶ Y₁
g₂ : W ⟶ Y₂
⊢ ∀ ⦃f₁ : Y₁ ⟶ Opposite.unop X⦄ ⦃f₂ : Y₂ ⟶ Opposite.unop X⦄ (h₁ : (Presheaf.imageSieve f.hom s).arrows f₁)
    (h₂ : (Presheaf.imageSieve f.hom s).arrows f₂),
    g₁ ≫ f₁ = g₂ ≫ f₂ →
      (ConcreteCategory.hom (F.obj.map g₁.op)) (t f₁ h₁) = (ConcreteCategory.hom (F.obj.map g₂.op)) (t f₂ h₂)

Tactic:
f₁

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type w)
f : F ⟶ G
h₁ : ∀ (X : Cᵒᵖ), Function.Injective ⇑(ConcreteCategory.hom (f.hom.app X))
right✝ : IsLocallySurjective f
X : Cᵒᵖ
s : G.obj.obj X
H : Presieve.IsSheafFor F.obj (Presheaf.imageSieve f.hom s).arrows
t : Presieve.FamilyOfElements F.obj (Presheaf.imageSieve f.hom s).arrows :=
  fun Y g hg ↦ Presheaf.localPreimage f.hom s g hg
Y₁ Y₂ W : C
g₁ : W ⟶ Y₁
g₂ : W ⟶ Y₂
f₁ : Y₁ ⟶ Opposite.unop X
⊢ ∀ ⦃f₂ : Y₂ ⟶ Opposite.unop X⦄ (h₁ : (Presheaf.imageSieve f.hom s).arrows f₁)
    (h₂ : (Presheaf.imageSieve f.hom s).arrows f₂),
    g₁ ≫ f₁ = g₂ ≫ f₂ →
      (ConcreteCategory.hom (F.obj.map g₁.op)) (t f₁ h₁) = (ConcreteCategory.hom (F.obj.map g₂.op)) (t f₂ h₂)
Module: Mathlib.CategoryTheory.Sites.LocallySurjective

Goal state before:
pp: case hR
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₁
inst✝ : IsLocallySurjective J f₂
U✝ : C
s : ToType (F₃.obj (op U✝))
this : (Sieve.bind (imageSieve f₂ s).arrows fun x x_1 h ↦ imageSieve f₁ (Exists.choose h)) ≤ imageSieve (f₁ ≫ f₂) s
⊢ ∀ ⦃Y : C⦄ ⦃f : Y ⟶ U✝⦄ (H : (imageSieve f₂ s).arrows f), imageSieve f₁ (Exists.choose H) ∈ J Y

Tactic:
intros

Goal state after:
case hR
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₁
inst✝ : IsLocallySurjective J f₂
U✝ : C
s : ToType (F₃.obj (op U✝))
this : (Sieve.bind (imageSieve f₂ s).arrows fun x x_1 h ↦ imageSieve f₁ (Exists.choose h)) ≤ imageSieve (f₁ ≫ f₂) s
Y✝ : C
f✝ : Y✝ ⟶ U✝
H✝ : (imageSieve f₂ s).arrows f✝
⊢ imageSieve f₁ (Exists.choose H✝) ∈ J Y✝
Module: Mathlib.CategoryTheory.Sites.LocallySurjective

Goal state before:
pp: 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₃
f₃ : F₁ ⟶ F₃
fac : f₁ ≫ f₂ = f₃
inst✝ : IsLocallySurjective J f₃
⊢ IsLocallySurjective J f₂

Tactic:
subst fac

Goal state after:
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₂)
⊢ IsLocallySurjective J f₂
Module: Mathlib.CategoryTheory.Sites.LocallySurjective

Goal state before:
pp: 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₃
f₃ : F₁ ⟶ F₃
fac : f₁ ≫ f₂ = f₃
inst✝¹ : IsLocallyInjective J f₃
inst✝ : IsLocallySurjective J f₁
⊢ IsLocallyInjective J f₂

Tactic:
subst fac

Goal state after:
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₁
inst✝ : IsLocallyInjective J (f₁ ≫ f₂)
⊢ IsLocallyInjective J f₂
Module: Mathlib.CategoryTheory.Sites.LocallyBijective

Goal state before:
pp: case mp
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 G : Sheaf J A
f : F ⟶ G
inst✝¹ : (forget A).ReflectsIsomorphisms
inst✝ : J.HasSheafCompose (forget A)
⊢ IsLocallyInjective f ∧ IsLocallySurjective f → IsIso f

Tactic:
rintro ⟨_, _⟩

Goal state after:
case mp
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 G : Sheaf J A
f : F ⟶ G
inst✝¹ : (forget A).ReflectsIsomorphisms
inst✝ : J.HasSheafCompose (forget A)
left✝ : IsLocallyInjective f
right✝ : IsLocallySurjective f
⊢ IsIso f
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf

Goal state before:
pp: case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R : Sheaf J RingCat
X Y : Cᵒᵖ
hX : Limits.IsInitial X
hY : Limits.IsInitial Y
φ : X ≅ Y
M : SheafOfModules R
⊢ ((forgetToSheafModuleCat R X hX).obj M).obj ≅
    ((forgetToSheafModuleCat R Y hY ⋙
            sheafCompose J (ModuleCat.restrictScalars (RingCat.Hom.hom (R.obj.map φ.hom)))).obj
        M).obj

pp: case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R : Sheaf J RingCat
X Y : Cᵒᵖ
hX : Limits.IsInitial X
hY : Limits.IsInitial Y
φ : X ≅ Y
⊢ ∀ {X_1 Y_1 : SheafOfModules R} (f : X_1 ⟶ Y_1),
    (forgetToSheafModuleCat R X hX).map f ≫ (ObjectProperty.isoMk (Presheaf.IsSheaf J) ?refine_1).hom =
      (ObjectProperty.isoMk (Presheaf.IsSheaf J) ?refine_1).hom ≫
        (forgetToSheafModuleCat R Y hY ⋙
              sheafCompose J (ModuleCat.restrictScalars (RingCat.Hom.hom (R.obj.map φ.hom)))).map
          f

Tactic:
· refine NatIso.ofComponents (fun U ↦ ?_) ?_
    · dsimp [PresheafOfModules.forgetToPresheafModuleCatObjObj]
      refine ModuleCat.restrictScalarsComp'App _ _ _ ?_ _
      simpa using congr((R.obj.map $(hX.hom_ext (hX.to U) (φ.hom ≫ hY.to U))).hom)
    cat_disch

Goal state after:
case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R : Sheaf J RingCat
X Y : Cᵒᵖ
hX : Limits.IsInitial X
hY : Limits.IsInitial Y
φ : X ≅ Y
⊢ ∀ {X_1 Y_1 : SheafOfModules R} (f : X_1 ⟶ Y_1),
    (forgetToSheafModuleCat R X hX).map f ≫
        (ObjectProperty.isoMk (Presheaf.IsSheaf J)
            (NatIso.ofComponents
              (fun U ↦
                id
                  (ModuleCat.restrictScalarsComp'App (RingCat.Hom.hom (R.obj.map φ.hom))
                    (RingCat.Hom.hom (R.obj.map (hY.to U))) (RingCat.Hom.hom (R.obj.map (hX.to U))) ⋯ (Y_1.val.obj U)))
              ⋯)).hom =
      (ObjectProperty.isoMk (Presheaf.IsSheaf J)
            (NatIso.ofComponents
              (fun U ↦
                id
                  (ModuleCat.restrictScalarsComp'App (RingCat.Hom.hom (R.obj.map φ.hom))
                    (RingCat.Hom.hom (R.obj.map (hY.to U))) (RingCat.Hom.hom (R.obj.map (hX.to U))) ⋯ (X_1.val.obj U)))
              ⋯)).hom ≫
        (forgetToSheafModuleCat R Y hY ⋙
              sheafCompose J (ModuleCat.restrictScalars (RingCat.Hom.hom (R.obj.map φ.hom)))).map
          f
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R : Sheaf J RingCat
⊢ ∀ (P Q R_1 : SheafOfModules R) (f f' : P ⟶ Q) (g : Q ⟶ R_1), (f + f') ≫ g = f ≫ g + f' ≫ g

Tactic:
intros

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R : Sheaf J RingCat
P✝ Q✝ R✝ : SheafOfModules R
f✝ f'✝ : P✝ ⟶ Q✝
g✝ : Q✝ ⟶ R✝
⊢ (f✝ + f'✝) ≫ g✝ = f✝ ≫ g✝ + f'✝ ≫ g✝
Module: Mathlib.CategoryTheory.Sites.LocallySurjective

Goal state before:
pp: 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₃
f₃ : F₁ ⟶ F₃
fac : f₁ ≫ f₂ = f₃
inst✝¹ : IsLocallySurjective J f₃
inst✝ : IsLocallyInjective J f₂
⊢ IsLocallySurjective J f₁

Tactic:
subst fac

Goal state after:
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✝¹ : IsLocallyInjective J f₂
inst✝ : IsLocallySurjective J (f₁ ≫ f₂)
⊢ IsLocallySurjective J f₁
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: case refine_2.hd₁
C : Type u
inst✝² : Category.{v, u} C
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan fun i ↦ f i.succ
c₂ : BinaryCofan (f 0) c₁.pt
t₁ : IsVanKampenColimit c₁
t₂ : IsVanKampenColimit c₂
inst✝¹ : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i
inst✝ : HasFiniteCoproducts C
j : Fin (n + 1)
F' : Fin (n + 1) → C
c : Cocone (Discrete.functor F')
α : Discrete.functor F' ⟶ Discrete.functor f
i : c.pt ⟶ (extendCofan c₁ c₂).pt
e : α ≫ (extendCofan c₁ c₂).ι = c.ι ≫ (const (Discrete (Fin (n + 1)))).map i
hα : NatTrans.Equifibered α
Hc : IsColimit c
T : C
⊢ ∀ (f : F' 0 ⟶ T) (g : (∐ fun j ↦ (Discrete.functor F').obj { as := j.succ }) ⟶ T),
    (BinaryCofan.mk (c.ι.app { as := 0 }) (Sigma.desc fun b ↦ c.ι.app { as := b.succ })).inl ≫
        Hc.desc
          (Cofan.mk T fun i ↦
            Fin.cases f (fun i ↦ Sigma.ι (fun j ↦ (Discrete.functor F').obj { as := j.succ }) i ≫ g) i) =
      f

Tactic:
f₁

Goal state after:
case refine_2.hd₁
C : Type u
inst✝² : Category.{v, u} C
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan fun i ↦ f i.succ
c₂ : BinaryCofan (f 0) c₁.pt
t₁ : IsVanKampenColimit c₁
t₂ : IsVanKampenColimit c₂
inst✝¹ : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i
inst✝ : HasFiniteCoproducts C
j : Fin (n + 1)
F' : Fin (n + 1) → C
c : Cocone (Discrete.functor F')
α : Discrete.functor F' ⟶ Discrete.functor f
i : c.pt ⟶ (extendCofan c₁ c₂).pt
e : α ≫ (extendCofan c₁ c₂).ι = c.ι ≫ (const (Discrete (Fin (n + 1)))).map i
hα : NatTrans.Equifibered α
Hc : IsColimit c
T : C
f₁ : F' 0 ⟶ T
⊢ ∀ (g : (∐ fun j ↦ (Discrete.functor F').obj { as := j.succ }) ⟶ T),
    (BinaryCofan.mk (c.ι.app { as := 0 }) (Sigma.desc fun b ↦ c.ι.app { as := b.succ })).inl ≫
        Hc.desc
          (Cofan.mk T fun i ↦
            Fin.cases f₁ (fun i ↦ Sigma.ι (fun j ↦ (Discrete.functor F').obj { as := j.succ }) i ≫ g) i) =
      f₁