mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Localization.Adjunction

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} D₁
inst✝⁴ : Category.{v_4, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝³ : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : L₂.IsLocalization W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
inst✝¹ : CatCommSq G L₁ L₂ G'
inst✝ : CatCommSq F L₂ L₁ F'
X₂ : C₂
eq : adj.unit.app (F.obj X₂) ≫ F.map (adj.counit.app X₂) = 𝟙 (F.obj X₂)
⊢ (Localization.ε adj L₁ W₁ L₂ G' F').app (F'.obj (L₂.obj X₂)) ≫
      F'.map
        (G'.map ((CatCommSq.iso F L₂ L₁ F').inv.app X₂) ≫
          (CatCommSq.iso G L₁ L₂ G').inv.app (F.obj X₂) ≫ L₂.map (adj.counit.app X₂)) =
    (NatTrans.id (F' ⋙ 𝟭 D₁)).app (L₂.obj X₂)

Tactic:
F'.map_comp,

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} D₁
inst✝⁴ : Category.{v_4, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝³ : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : L₂.IsLocalization W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
inst✝¹ : CatCommSq G L₁ L₂ G'
inst✝ : CatCommSq F L₂ L₁ F'
X₂ : C₂
eq : adj.unit.app (F.obj X₂) ≫ F.map (adj.counit.app X₂) = 𝟙 (F.obj X₂)
⊢ (Localization.ε adj L₁ W₁ L₂ G' F').app (F'.obj (L₂.obj X₂)) ≫
      F'.map (G'.map ((CatCommSq.iso F L₂ L₁ F').inv.app X₂)) ≫
        F'.map ((CatCommSq.iso G L₁ L₂ G').inv.app (F.obj X₂) ≫ L₂.map (adj.counit.app X₂)) =
    (NatTrans.id (F' ⋙ 𝟭 D₁)).app (L₂.obj X₂)
Module: Mathlib.CategoryTheory.Localization.Bousfield

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
P : ObjectProperty C
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
hf : P.isLocal f
hfg : P.isLocal (f ≫ g)
Z : C
hZ : P Z
⊢ Function.Bijective fun g_1 ↦ g ≫ g_1

Tactic:
by
    rw [← Function.Bijective.of_comp_iff' (hf Z hZ)]
    simpa using! hfg Z hZ

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

Goal state before:
pp: case mpr.right
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : ObjectProperty C
Y Z : C
g : Y ⟶ Z
hg : P.isColocal g
X X' : C
hX' : P X'
e : X ≅ X'
⊢ Function.Surjective fun f ↦ f ≫ g

Tactic:
intro f
      obtain ⟨a, h⟩ := (hg _ hX').2 (e.inv ≫ f)
      exact ⟨e.hom ≫ a, by simp [h]⟩

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

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
P : ObjectProperty C
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
hf : P.isColocal f
hg : P.isColocal g
X : C
hX : P X
x✝ : X ⟶ X✝
⊢ x✝ ≫ f ≫ g = ((fun f ↦ f ≫ g) ∘ fun f_1 ↦ f_1 ≫ f) x✝

Tactic:
cat_disch

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

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
P : ObjectProperty C
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
hg : P.isColocal g
hfg : P.isColocal (f ≫ g)
X : C
hX : P X
x✝ : X ⟶ X✝
⊢ ((fun f ↦ f ≫ g) ∘ fun f_1 ↦ f_1 ≫ f) x✝ = x✝ ≫ f ≫ g

Tactic:
cat_disch

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

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
P : ObjectProperty C
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
hf : P.isColocal f
hfg : P.isColocal (f ≫ g)
X : C
hX : P X
x✝ : X ⟶ X✝
⊢ ((fun f ↦ f ≫ g) ∘ fun f_1 ↦ f_1 ≫ f) x✝ = x✝ ≫ f ≫ g

Tactic:
cat_disch

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

Goal state before:
pp: 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
hf : P.isColocal f
g : Y ⟶ X
hg : (fun f_1 ↦ f_1 ≫ f) g = 𝟙 Y
⊢ (fun f_1 ↦ f_1 ≫ f) (f ≫ g) = (fun f_1 ↦ f_1 ≫ f) (𝟙 X)

Tactic:
cat_disch

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

Goal state before:
pp: case e'_3
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : G ⊣ F
inst✝¹ : G.Full
inst✝ : G.Faithful
X : C
Y : D
e_1✝ : (G.obj Y ⟶ (F ⋙ G).obj X) = (G.obj Y ⟶ G.obj (F.obj X))
e_2✝ : (G.obj Y ⟶ (𝟭 C).obj X) = (G.obj Y ⟶ X)
⊢ (fun f ↦ f ≫ adj.counit.app X) =
    (fun g ↦ G.map g ≫ adj.counit.app X) ∘ ⇑(Functor.FullyFaithful.ofFullyFaithful G).homEquiv.symm

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasInitial C
X Y : C
c : BinaryCofan X Y
h : IsVanKampenColimit c
⊢ Mono c.inr

Tactic:
refine PullbackCone.mono_of_isLimitMkIdId _ (IsPullback.isLimit ?_)

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasInitial C
X Y : C
c : BinaryCofan X Y
h : IsVanKampenColimit c
⊢ IsPullback (𝟙 ((pair X Y).obj { as := WalkingPair.right })) (𝟙 ((pair X Y).obj { as := WalkingPair.right })) c.inr
    c.inr
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
this : ∀ (X : Cᵒᵖ), Function.Surjective ⇑(ConcreteCategory.hom (f.hom.app X))
⊢ IsIso f

Tactic:
by
      rw [← isIso_iff_of_reflects_iso _ (sheafToPresheaf _ _), NatTrans.isIso_iff_isIso_app]
      intro X
      rw [isIso_iff_bijective]
      exact ⟨h₁ X, this X⟩

Goal state after:
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₃
inst✝ : IsLocallySurjective J (f₁ ≫ f₂)
⊢ IsLocallySurjective J f₂

Tactic:
exact isLocallySurjective_of_isLocallySurjective J f₁ f₂

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

Goal state before:
pp: case refine_1.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
M : SheafOfModules R
⊢ ∀ {X_1 Y_1 : Cᵒᵖ} (f : X_1 ⟶ Y_1),
    ((forgetToSheafModuleCat R X hX).obj M).obj.map f ≫
        (id
            (ModuleCat.restrictScalarsComp'App (RingCat.Hom.hom (R.obj.map φ.hom))
              (RingCat.Hom.hom (R.obj.map (hY.to Y_1))) (RingCat.Hom.hom (R.obj.map (hX.to Y_1))) ⋯
              (M.val.obj Y_1))).hom =
      (id
            (ModuleCat.restrictScalarsComp'App (RingCat.Hom.hom (R.obj.map φ.hom))
              (RingCat.Hom.hom (R.obj.map (hY.to X_1))) (RingCat.Hom.hom (R.obj.map (hX.to X_1))) ⋯
              (M.val.obj X_1))).hom ≫
        ((forgetToSheafModuleCat R Y hY ⋙
                    sheafCompose J (ModuleCat.restrictScalars (RingCat.Hom.hom (R.obj.map φ.hom)))).obj
                M).obj.map
          f

Tactic:
cat_disch

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

Goal state before:
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)
            (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

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasInitial C
ι : Type u_3
X : ι → C
c : Cofan X
hc : IsVanKampenColimit c
i j : ι
inst✝ : DecidableEq ι
⊢ IsPullback (if h : j = i then eqToHom ⋯ else eqToHom ⋯ ≫ initial.to (X i))
    (if h : j = i then eqToHom ⋯ else eqToHom ⋯ ≫ initial.to (X j)) (c.inj i) (c.inj j)

Tactic:
refine (hc (Cofan.mk (X i) (f := fun k ↦ if k = i then X i else ⊥_ C)
    (fun k ↦ if h : k = i then (eqToHom <| if_pos h) else (eqToHom <| if_neg h) ≫ initial.to _))
    (Discrete.natTrans (fun k ↦ if h : k.1 = i then (eqToHom <| (if_pos h).trans
      (congr_arg X h.symm)) else (eqToHom <| if_neg h) ≫ initial.to _))
    (c.inj i) ?_ (.of_discrete _)).mp ⟨?_⟩ ⟨j⟩

Goal state after:
case refine_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasInitial C
ι : Type u_3
X : ι → C
c : Cofan X
hc : IsVanKampenColimit c
i j : ι
inst✝ : DecidableEq ι
⊢ (Discrete.natTrans fun k ↦ if h : k.as = i then eqToHom ⋯ else eqToHom ⋯ ≫ initial.to ((Discrete.functor X).obj k)) ≫
      c.ι =
    (Cofan.mk (X i) fun k ↦ if h : k = i then eqToHom ⋯ else eqToHom ⋯ ≫ initial.to (X i)).ι ≫
      (const (Discrete ι)).map (c.inj i)

case refine_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasInitial C
ι : Type u_3
X : ι → C
c : Cofan X
hc : IsVanKampenColimit c
i j : ι
inst✝ : DecidableEq ι
⊢ IsColimit (Cofan.mk (X i) fun k ↦ if h : k = i then eqToHom ⋯ else eqToHom ⋯ ≫ initial.to (X i))
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasInitial C
ι : Type u_3
i : Discrete ι
f : ι → C
c : Cocone (Discrete.functor f)
hc : IsVanKampenColimit c
⊢ Mono (c.ι.app i)

Tactic:
refine PullbackCone.mono_of_isLimitMkIdId _ (IsPullback.isLimit ?_)

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasInitial C
ι : Type u_3
i : Discrete ι
f : ι → C
c : Cocone (Discrete.functor f)
hc : IsVanKampenColimit c
⊢ IsPullback (𝟙 ((Discrete.functor f).obj i)) (𝟙 ((Discrete.functor f).obj i)) (c.ι.app i) (c.ι.app i)
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Submodule

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M : PresheafOfModules R
N : M.Submodule
⊢ ∀ (X : Cᵒᵖ) (r : ↑(R.obj X)) (m : ↑(N.toPresheafOfModules.obj X)),
    (ConcreteCategory.hom
          ({ app := fun X ↦ AddCommGrpCat.ofHom (N.obj X).subtype.toAddMonoidHom, naturality := ⋯ }.app X))
        (r • m) =
      r •
        (ConcreteCategory.hom
            ({ app := fun X ↦ AddCommGrpCat.ofHom (N.obj X).subtype.toAddMonoidHom, naturality := ⋯ }.app X))
          m

Tactic:
cat_disch

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M : PresheafOfModules R
N N₁ N₂ : M.Submodule
hle : N₁ ≤ N₂
⊢ ∀ (X : Cᵒᵖ) (r : ↑(R.obj X)) (m : ↑(N₁.toPresheafOfModules.obj X)),
    (ConcreteCategory.hom
          ({ app := fun X ↦ AddCommGrpCat.ofHom (Submodule.inclusion ⋯).toAddMonoidHom, naturality := ⋯ }.app X))
        (r • m) =
      r •
        (ConcreteCategory.hom
            ({ app := fun X ↦ AddCommGrpCat.ofHom (Submodule.inclusion ⋯).toAddMonoidHom, naturality := ⋯ }.app X))
          m

Tactic:
cat_disch

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

Goal state before:
pp: C : Type u'
inst✝⁴ : Category.{v', u'} C
J : GrothendieckTopology C
R₀ : Cᵒᵖ ⥤ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.obj
inst✝³ : Presheaf.IsLocallyInjective J α
inst✝² : Presheaf.IsLocallySurjective J α
inst✝¹ : J.WEqualsLocallyBijective AddCommGrpCat
inst✝ : HasWeakSheafify J AddCommGrpCat
P : PresheafOfModules R₀
F : SheafOfModules R
⊢ ((sheafification α).obj P ⟶ F) ≃ (P ⟶ (restrictScalars α).obj ((SheafOfModules.forget R).obj F))

Tactic:
by
  apply sheafifyHomEquiv

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.LocallyDiscrete

Goal state before:
pp: C : Type u
⊢ Function.LeftInverse mk as

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.LocallyDiscrete

Goal state before:
pp: C : Type u
⊢ Function.RightInverse mk as

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.SigmaConst

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasCoproducts C
R : C
J : Type u'
x✝ : Category.{v', u'} J
K : J ⥤ Type w
c : Cocone K
hc : (K.coconeTypesEquiv.symm c).IsColimit
coconeTypes : Cocone (K ⋙ sigmaConst.obj R) → K.CoconeTypes :=
  fun s ↦ { pt := R ⟶ s.pt, ι := fun j k ↦ Sigma.ι (fun x ↦ R) k ≫ s.ι.app j, ι_naturality := ⋯ }
s : Cocone (K ⋙ sigmaConst.obj R)
j : J
⊢ ((sigmaConst.obj R).mapCocone c).ι.app j ≫ Sigma.desc (hc.desc (coconeTypes s)) = s.ι.app j

Tactic:
dsimp
        ext k
        simp [dsimp% hc.fac_apply, dsimp% Sigma.ι_desc (hc.desc (coconeTypes s)), coconeTypes]

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

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
I : Type u
M : SheafOfModules R
i : I
f : free I ⟶ M
⊢ sectionsMap (M.freeHomEquiv.symm (M.freeHomEquiv f)) (freeSection i) = M.freeHomEquiv f i

Tactic:
cat_disch

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : RepresentablyFlat F
J : Type v₁
𝒥✝ : SmallCategory J
x✝ : FinCategory J
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
m : s.pt ⟶ (F.mapCone c).pt
h : ∀ (j : J), m ≫ (F.mapCone c).π.app j = s.π.app j
⊢ m = PreservesFiniteLimitsOfFlat.lift F hc s

Tactic:
by
        apply PreservesFiniteLimitsOfFlat.uniq F hc
        · exact h
        · exact PreservesFiniteLimitsOfFlat.fac F hc s

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

Goal state before:
pp: case mk.mk
C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreZeroHypercover S
F : PreZeroHypercover S
s₀✝¹ : E.I₀ → F.I₀
h₀✝¹ : (i : E.I₀) → E.X i ⟶ F.X (s₀✝¹ i)
w₀✝¹ : ∀ (i : E.I₀), h₀✝¹ i ≫ F.f (s₀✝¹ i) = E.f i
s₀✝ : E.I₀ → F.I₀
h₀✝ : (i : E.I₀) → E.X i ⟶ F.X (s₀✝ i)
w₀✝ : ∀ (i : E.I₀), h₀✝ i ≫ F.f (s₀✝ i) = E.f i
hs : s₀✝¹ = s₀✝
hh : ∀ (i : E.I₀), { s₀ := s₀✝¹, h₀ := h₀✝¹, w₀ := w₀✝¹ }.h₀ i = { s₀ := s₀✝, h₀ := h₀✝, w₀ := w₀✝ }.h₀ i ≫ eqToHom ⋯
⊢ { s₀ := s₀✝¹, h₀ := h₀✝¹, w₀ := w₀✝¹ } = { s₀ := s₀✝, h₀ := h₀✝, w₀ := w₀✝ }

Tactic:
cat_disch

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

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_3, u_3} E
F : C ⥤ D
G : D ⥤ E
X : E
inst✝¹ : RepresentablyFlat F
inst✝ : IsCofiltered (StructuredArrow X G)
T : StructuredArrow X (F ⋙ G) ⥤ StructuredArrow X G := StructuredArrow.pre X F G
Y : StructuredArrow X G
A : StructuredArrow Y.right F
⊢ IsCofiltered (StructuredArrow X (F ⋙ G))

Tactic:
have : Nonempty (StructuredArrow X (F ⋙ G)) := ⟨.mk (Y.hom ≫ G.map A.hom)⟩

Goal state after:
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_3, u_3} E
F : C ⥤ D
G : D ⥤ E
X : E
inst✝¹ : RepresentablyFlat F
inst✝ : IsCofiltered (StructuredArrow X G)
T : StructuredArrow X (F ⋙ G) ⥤ StructuredArrow X G := StructuredArrow.pre X F G
Y : StructuredArrow X G
A : StructuredArrow Y.right F
this : Nonempty (StructuredArrow X (F ⋙ G))
⊢ IsCofiltered (StructuredArrow X (F ⋙ G))
Module: Mathlib.CategoryTheory.Sites.Continuous

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : C
E : PreOneHypercover X
F : C ⥤ D
W : C
i₁ i₂ : E.I₀
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
⊢ Sieve.functorPushforward F (E.sieve₁ p₁ p₂) ≤ (E.map F).sieve₁ (F.map p₁) (F.map p₂)

Tactic:
rw [Sieve.functorPushforward_le_iff_le_functorPullback]
  intro Y f ⟨k, u, hf₁, hf₂⟩
  exact ⟨k, F.map u, by simp [← Functor.map_comp, hf₁], by simp [← Functor.map_comp, hf₂]⟩

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

Goal state before:
pp: case refine_1
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
X : C
E : PreOneHypercover X
F : C ⥤ D
i₁ i₂ : E.I₀
inst✝¹ : HasPullback (E.f i₁) (E.f i₂)
inst✝ : PreservesLimit (cospan (E.f i₁) (E.f i₂)) F
this : HasPullback ((E.map F).f i₁) ((E.map F).f i₂)
⊢ Sieve.functorPushforward F (E.sieve₁' i₁ i₂) ≤
    (E.map F).sieve₁ (F.map (pullback.fst (E.f i₁) (E.f i₂))) (F.map (pullback.snd (E.f i₁) (E.f i₂)))

Tactic:
rw [PreOneHypercover.sieve₁'_eq_sieve₁]
    apply PreOneHypercover.functorPushforward_sieve₁_map_le

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

Goal state before:
pp: C : Type u_2
inst✝ : Category.{u_3, u_2} C
K : Precoverage C
J : GrothendieckTopology C
⊢ K.toGrothendieck ≤ J ↔ K ≤ J.toPrecoverage

Tactic:
by
  refine ⟨fun h X R hR ↦ ?_, fun h ↦ ?_⟩
  · rw [GrothendieckTopology.mem_toPrecoverage_iff]
    exact h _ (generate_mem_toGrothendieck hR)
  · intro X R hR
    induction hR with
    | of X S hS => exact h _ hS
    | top X => grind
    | pullback X S _ Y f _ => grind
    | transitive X S R _ _ _ _ => grind

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

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreOneHypercover S
i₁ i₂ : E.I₀
W : C
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
T : C
f : T ⟶ W
Z : C
g : Z ⟶ T
k : E.I₁ i₁ i₂
u : Z ⟶ E.Y k
hu₁ : (g ≫ f) ≫ p₁ = u ≫ E.p₁ k
hu₂ : (g ≫ f) ≫ p₂ = u ≫ E.p₂ k
⊢ (E.sieve₁ (f ≫ p₁) (f ≫ p₂)).arrows g

Tactic:
cat_disch

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

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreOneHypercover S
i₁ i₂ : E.I₀
W : C
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
T : C
f : T ⟶ W
Z : C
g : Z ⟶ T
k : E.I₁ i₁ i₂
u : Z ⟶ E.Y k
hu₁ : g ≫ f ≫ p₁ = u ≫ E.p₁ k
hu₂ : g ≫ f ≫ p₂ = u ≫ E.p₂ k
⊢ (Sieve.pullback f (E.sieve₁ p₁ p₂)).arrows g

Tactic:
cat_disch

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
i₁ i₂ : E.I₀
inst✝ : HasPullback (E.f i₁) (E.f i₂)
W : C
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
w : p₁ ≫ E.f i₁ = p₂ ≫ E.f i₂
Z : C
g : Z ⟶ W
j : E.I₁ i₁ i₂
h : Z ⟶ E.Y j
fac₁ : g ≫ p₁ = h ≫ E.p₁ j
fac₂ : g ≫ p₂ = h ≫ E.p₂ j
⊢ h ≫ E.toPullback j = g ≫ pullback.lift p₁ p₂ w

Tactic:
cat_disch

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

Goal state before:
pp: case e_h
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
i₁ i₂ : E.I₀
inst✝ : HasPullback (E.f i₁) (E.f i₂)
⊢ 𝟙 (pullback (E.f i₁) (E.f i₂)) = pullback.lift (pullback.fst (E.f i₁) (E.f i₂)) (pullback.snd (E.f i₁) (E.f i₂)) ⋯

Tactic:
cat_disch

Goal state after:
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:
cat_disch

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

Goal state before:
pp: case refine_4
C : Type u
inst✝³ : Category.{v, u} C
A : Type u_1
inst✝² : Category.{v_1, u_1} A
S : C
E : PreOneHypercover S
c : Cofan E.X
hc : IsColimit c
d : Cofan E.Y'
hd : IsColimit d
F : Cᵒᵖ ⥤ A
inst✝¹ : PreservesLimit (Discrete.functor fun i ↦ op (E.X i)) F
inst✝ : PreservesLimit (Discrete.functor fun i ↦ op (E.Y' i)) F
⊢ ∀ (i : (E.sigmaOfIsColimit hc hd).multicospanShape.R),
    ((E.sigmaOfIsColimit hc hd).multicospanIndex F).fst i ≫
        (Iso.refl (((E.sigmaOfIsColimit hc hd).multicospanIndex F).right i)).hom =
      (Iso.refl
            (((E.sigmaOfIsColimit hc hd).multicospanIndex F).left
              ((E.sigmaOfIsColimit hc hd).multicospanShape.fst i))).hom ≫
        (MulticospanIndex.ofParallelHoms (E.sigmaOfIsColimit hc hd).multicospanShape
              (F.map (Cofan.IsColimit.desc hd fun x ↦ E.p₁ x.snd ≫ c.inj x.fst.1).op)
              (F.map (Cofan.IsColimit.desc hd fun x ↦ E.p₂ x.snd ≫ c.inj x.fst.2).op)).fst
          i

Tactic:
cat_disch

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

Goal state before:
pp: case refine_5
C : Type u
inst✝³ : Category.{v, u} C
A : Type u_1
inst✝² : Category.{v_1, u_1} A
S : C
E : PreOneHypercover S
c : Cofan E.X
hc : IsColimit c
d : Cofan E.Y'
hd : IsColimit d
F : Cᵒᵖ ⥤ A
inst✝¹ : PreservesLimit (Discrete.functor fun i ↦ op (E.X i)) F
inst✝ : PreservesLimit (Discrete.functor fun i ↦ op (E.Y' i)) F
⊢ ∀ (i : (E.sigmaOfIsColimit hc hd).multicospanShape.R),
    ((E.sigmaOfIsColimit hc hd).multicospanIndex F).snd i ≫
        (Iso.refl (((E.sigmaOfIsColimit hc hd).multicospanIndex F).right i)).hom =
      (Iso.refl
            (((E.sigmaOfIsColimit hc hd).multicospanIndex F).left
              ((E.sigmaOfIsColimit hc hd).multicospanShape.snd i))).hom ≫
        (MulticospanIndex.ofParallelHoms (E.sigmaOfIsColimit hc hd).multicospanShape
              (F.map (Cofan.IsColimit.desc hd fun x ↦ E.p₁ x.snd ≫ c.inj x.fst.1).op)
              (F.map (Cofan.IsColimit.desc hd fun x ↦ E.p₂ x.snd ≫ c.inj x.fst.2).op)).snd
          i

Tactic:
cat_disch

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

Goal state before:
pp: case refine_6
C : Type u
inst✝³ : Category.{v, u} C
A : Type u_1
inst✝² : Category.{v_1, u_1} A
S : C
E : PreOneHypercover S
c : Cofan E.X
hc : IsColimit c
d : Cofan E.Y'
hd : IsColimit d
F : Cᵒᵖ ⥤ A
inst✝¹ : PreservesLimit (Discrete.functor fun i ↦ op (E.X i)) F
inst✝ : PreservesLimit (Discrete.functor fun i ↦ op (E.Y' i)) F
⊢ ∀ (i : (E.sigmaOfIsColimit hc hd).multicospanShape.L),
    (Iso.refl ((E.sigmaOfIsColimit hc hd).multifork F).pt).hom ≫
        Multifork.ι
          ((MulticospanIndex.multiforkOfParallelHomsEquivFork (E.sigmaOfIsColimit hc hd).multicospanShape
                    (F.map (Cofan.IsColimit.desc hd fun x ↦ E.p₁ x.snd ≫ c.inj x.fst.1).op)
                    (F.map (Cofan.IsColimit.desc hd fun x ↦ E.p₂ x.snd ≫ c.inj x.fst.2).op)).symm.functor.obj
            (E.forkOfIsColimit hc hd F))
          i =
      ((E.sigmaOfIsColimit hc hd).multifork F).ι i ≫
        (Iso.refl (((E.sigmaOfIsColimit hc hd).multicospanIndex F).left i)).hom

Tactic:
cat_disch

Goal state after: