mathlib-initiative/mathlib-tactics huggingface dataset:
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 : C ⥤ D
G : D ⥤ C
S : Sheaf J RingCat
R : Sheaf K RingCat
inst✝¹ : F.IsContinuous J K
inst✝ : G.IsContinuous K J
adj : F ⊣ G
φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R
ψ : R ⟶ (G.sheafPushforwardContinuous RingCat K J).obj S
H₁ : whiskerRight (NatTrans.op adj.counit) R.obj = ψ.hom ≫ G.op.whiskerLeft φ.hom
H₂ : φ.hom ≫ F.op.whiskerLeft ψ.hom ≫ whiskerRight (NatTrans.op adj.unit) S.obj = 𝟙 S.obj
this : (G ⋙ F).IsContinuous K K := ⋯
⊢ (𝟙 (((𝟭 D).sheafPushforwardContinuous RingCat K K).obj R) ≫
        (sheafPushforwardContinuousNatTrans adj.counit RingCat K K).app R).hom =
    (ψ ≫ (G.sheafPushforwardContinuous RingCat K J).map φ).hom

Tactic:
;

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✝
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
G : D ⥤ C
S : Sheaf J RingCat
R : Sheaf K RingCat
inst✝¹ : F.IsContinuous J K
inst✝ : G.IsContinuous K J
adj : F ⊣ G
φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R
ψ : R ⟶ (G.sheafPushforwardContinuous RingCat K J).obj S
H₁ : whiskerRight (NatTrans.op adj.counit) R.obj = ψ.hom ≫ G.op.whiskerLeft φ.hom
H₂ : φ.hom ≫ F.op.whiskerLeft ψ.hom ≫ whiskerRight (NatTrans.op adj.unit) S.obj = 𝟙 S.obj
this : (G ⋙ F).IsContinuous K K := ⋯
⊢ (𝟙 (((𝟭 D).sheafPushforwardContinuous RingCat K K).obj R) ≫
        (sheafPushforwardContinuousNatTrans adj.counit RingCat K K).app R).hom =
    (ψ ≫ (G.sheafPushforwardContinuous RingCat K J).map φ).hom
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 : C ⥤ D
G : D ⥤ C
S : Sheaf J RingCat
R : Sheaf K RingCat
inst✝¹ : F.IsContinuous J K
inst✝ : G.IsContinuous K J
adj : F ⊣ G
φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R
ψ : R ⟶ (G.sheafPushforwardContinuous RingCat K J).obj S
H₁ : whiskerRight (NatTrans.op adj.counit) R.obj = ψ.hom ≫ G.op.whiskerLeft φ.hom
H₂ : φ.hom ≫ F.op.whiskerLeft ψ.hom ≫ whiskerRight (NatTrans.op adj.unit) S.obj = 𝟙 S.obj
this : (F ⋙ G).IsContinuous J J := ⋯
⊢ ((φ ≫ (F.sheafPushforwardContinuous RingCat J K).map ψ) ≫
        (sheafPushforwardContinuousNatTrans adj.unit RingCat J J).app S).hom =
    (𝟙 S).hom

Tactic:
;

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✝
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
G : D ⥤ C
S : Sheaf J RingCat
R : Sheaf K RingCat
inst✝¹ : F.IsContinuous J K
inst✝ : G.IsContinuous K J
adj : F ⊣ G
φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R
ψ : R ⟶ (G.sheafPushforwardContinuous RingCat K J).obj S
H₁ : whiskerRight (NatTrans.op adj.counit) R.obj = ψ.hom ≫ G.op.whiskerLeft φ.hom
H₂ : φ.hom ≫ F.op.whiskerLeft ψ.hom ≫ whiskerRight (NatTrans.op adj.unit) S.obj = 𝟙 S.obj
this : (F ⋙ G).IsContinuous J J := ⋯
⊢ ((φ ≫ (F.sheafPushforwardContinuous RingCat J K).map ψ) ≫
        (sheafPushforwardContinuousNatTrans adj.unit RingCat J J).app S).hom =
    (𝟙 S).hom
Module: Mathlib.Topology.Sheaves.Sheaf

Goal state before:
pp: case refine_2
X : TopCat
A : Type u_1
inst✝⁵ : Category.{u, u_1} A
FC : A → A → Type u_2
CC : A → Type u
inst✝⁴ : (X Y : A) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory A FC
inst✝² : HasLimits A
inst✝¹ : PreservesLimits (forget A)
inst✝ : (forget A).ReflectsIsomorphisms
F : Presheaf A X
hF : F.IsSheaf
U : (Opens ↑X)ᵒᵖ
s t : ToType (F.obj U)
hst :
  ∀ x ∈ unop U,
    ∃ V,
      ∃ (hV : V ≤ unop U),
        x ∈ V ∧ (ConcreteCategory.hom (F.map (homOfLE hV).op)) s = (ConcreteCategory.hom (F.map (homOfLE hV).op)) t
this : Presieve.IsSheaf (Opens.grothendieckTopology ↑X) (F ⋙ forget A)
V : ↥(unop U) → Opens ↑X
hV : ∀ (x : ↥(unop U)), V x ≤ unop U
hxV : ∀ (x : ↥(unop U)), ↑x ∈ V x
H : ∀ (x : ↥(unop U)), (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) s = (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) t
Y : Opens ↑X
x : ↥(unop U)
⊢ (ConcreteCategory.hom ((F ⋙ forget A).map (homOfLE ⋯).op)) s =
    (ConcreteCategory.hom ((F ⋙ forget A).map (homOfLE ⋯).op)) t

Tactic:
;

Goal state after:
case refine_2
X : TopCat
A : Type u_1
inst✝⁵ : Category.{u, u_1} A
FC : A → A → Type u_2
CC : A → Type u
inst✝⁴ : (X Y : A) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory A FC
inst✝² : HasLimits A
inst✝¹ : PreservesLimits (forget A)
inst✝ : (forget A).ReflectsIsomorphisms
F : Presheaf A X
hF : F.IsSheaf
U : (Opens ↑X)ᵒᵖ
s t : ToType (F.obj U)
hst :
  ∀ x ∈ unop U,
    ∃ V,
      ∃ (hV : V ≤ unop U),
        x ∈ V ∧ (ConcreteCategory.hom (F.map (homOfLE hV).op)) s = (ConcreteCategory.hom (F.map (homOfLE hV).op)) t
this : Presieve.IsSheaf (Opens.grothendieckTopology ↑X) (F ⋙ forget A)
V : ↥(unop U) → Opens ↑X
hV : ∀ (x : ↥(unop U)), V x ≤ unop U
hxV : ∀ (x : ↥(unop U)), ↑x ∈ V x
H : ∀ (x : ↥(unop U)), (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) s = (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) t
Y : Opens ↑X
x : ↥(unop U)
⊢ (ConcreteCategory.hom ((F ⋙ forget A).map (homOfLE ⋯).op)) s =
    (ConcreteCategory.hom ((F ⋙ forget A).map (homOfLE ⋯).op)) t
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 : C✝ ⥤ D
G : D ⥤ C✝
S : Sheaf J✝ RingCat
R✝ : Sheaf K RingCat
inst✝³ : F.IsContinuous J✝ K
inst✝² : G.IsContinuous K J✝
adj : F ⊣ G
φ : S ⟶ (F.sheafPushforwardContinuous RingCat J✝ K).obj R✝
ψ : R✝ ⟶ (G.sheafPushforwardContinuous RingCat K J✝).obj S
H₁ : whiskerRight (NatTrans.op adj.counit) R✝.obj = ψ.hom ≫ G.op.whiskerLeft φ.hom
H₂ : φ.hom ≫ F.op.whiskerLeft ψ.hom ≫ whiskerRight (NatTrans.op adj.unit) S.obj = 𝟙 S.obj
C : Type u'
inst✝¹ : Category.{v', u'} C
inst✝ : HasBinaryProducts C
J : GrothendieckTopology C
R : Sheaf J RingCat
x : C
U V : Cᵒᵖ
f : U ⟶ V
⊢ R.obj.map (f ≫ prod.snd.op) = R.obj.map (prod.snd ≫ f.unop).op

Tactic:
;

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✝¹
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
G : D ⥤ C✝
S : Sheaf J✝ RingCat
R✝ : Sheaf K RingCat
inst✝³ : F.IsContinuous J✝ K
inst✝² : G.IsContinuous K J✝
adj : F ⊣ G
φ : S ⟶ (F.sheafPushforwardContinuous RingCat J✝ K).obj R✝
ψ : R✝ ⟶ (G.sheafPushforwardContinuous RingCat K J✝).obj S
H₁ : whiskerRight (NatTrans.op adj.counit) R✝.obj = ψ.hom ≫ G.op.whiskerLeft φ.hom
H₂ : φ.hom ≫ F.op.whiskerLeft ψ.hom ≫ whiskerRight (NatTrans.op adj.unit) S.obj = 𝟙 S.obj
C : Type u'
inst✝¹ : Category.{v', u'} C
inst✝ : HasBinaryProducts C
J : GrothendieckTopology C
R : Sheaf J RingCat
x : C
U V : Cᵒᵖ
f : U ⟶ V
⊢ R.obj.map (f ≫ prod.snd.op) = R.obj.map (prod.snd ≫ f.unop).op
Module: Mathlib.CategoryTheory.Category.Pairwise

Goal state before:
pp: case id_single
ι : Type v
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
⊢ id_single i ∈ if h : i = i then {eqToHom ⋯} else ∅

Tactic:
;

Goal state after:
case id_single
ι : Type v
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
⊢ id_single i ∈ if h : i = i then {eqToHom ⋯} else ∅
Module: Mathlib.CategoryTheory.Category.Pairwise

Goal state before:
pp: case id_pair
ι : Type v
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i j : ι
⊢ id_pair i j ∈ if h : i = i ∧ j = j then {eqToHom ⋯} else ∅

Tactic:
;

Goal state after:
case id_pair
ι : Type v
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i j : ι
⊢ id_pair i j ∈ if h : i = i ∧ j = j then {eqToHom ⋯} else ∅
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
eqv : C ≌ D
S : Sheaf J RingCat
R : Sheaf K RingCat
inst✝¹ : eqv.functor.IsContinuous J K
inst✝ : eqv.inverse.IsContinuous K J
φ : S ⟶ (eqv.functor.sheafPushforwardContinuous RingCat J K).obj R
ψ : R ⟶ (eqv.inverse.sheafPushforwardContinuous RingCat K J).obj S
H₁ : whiskerRight (NatTrans.op eqv.counit) R.obj = ψ.hom ≫ eqv.inverse.op.whiskerLeft φ.hom
H₂ : φ.hom ≫ eqv.functor.op.whiskerLeft ψ.hom ≫ whiskerRight (NatTrans.op eqv.unit) S.obj = 𝟙 S.obj
this : (eqv.inverse ⋙ eqv.functor).IsContinuous K K := ⋯
⊢ (𝟙 R ≫ (sheafPushforwardContinuousNatTrans eqv.counitIso.hom RingCat K K).app R).hom =
    (ψ ≫ (eqv.inverse.sheafPushforwardContinuous RingCat K J).map φ).hom

Tactic:
;

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✝
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : GrothendieckTopology C
K : GrothendieckTopology D
eqv : C ≌ D
S : Sheaf J RingCat
R : Sheaf K RingCat
inst✝¹ : eqv.functor.IsContinuous J K
inst✝ : eqv.inverse.IsContinuous K J
φ : S ⟶ (eqv.functor.sheafPushforwardContinuous RingCat J K).obj R
ψ : R ⟶ (eqv.inverse.sheafPushforwardContinuous RingCat K J).obj S
H₁ : whiskerRight (NatTrans.op eqv.counit) R.obj = ψ.hom ≫ eqv.inverse.op.whiskerLeft φ.hom
H₂ : φ.hom ≫ eqv.functor.op.whiskerLeft ψ.hom ≫ whiskerRight (NatTrans.op eqv.unit) S.obj = 𝟙 S.obj
this : (eqv.inverse ⋙ eqv.functor).IsContinuous K K := ⋯
⊢ (𝟙 R ≫ (sheafPushforwardContinuousNatTrans eqv.counitIso.hom RingCat K K).app R).hom =
    (ψ ≫ (eqv.inverse.sheafPushforwardContinuous RingCat K J).map φ).hom
Module: Mathlib.Topology.Sheaves.SheafCondition.Sites

Goal state before:
pp: case mp
X : TopCat
ι : Type u_1
inst✝ : Category.{v_1, u_1} ι
B : ι ⥤ Opens ↑X
hd : B.IsCoverDense (Opens.grothendieckTopology ↑X)
U : Opens ↑X
x : ↑X
hx : x ∈ U
⊢ ∃ U' ∈ Set.range B.obj, x ∈ U' ∧ U' ≤ U

Tactic:
;

Goal state after:
case mp
X : TopCat
ι : Type u_1
inst✝ : Category.{v_1, u_1} ι
B : ι ⥤ Opens ↑X
hd : B.IsCoverDense (Opens.grothendieckTopology ↑X)
U : Opens ↑X
x : ↑X
hx : x ∈ U
⊢ ∃ U' ∈ Set.range B.obj, x ∈ U' ∧ U' ≤ U
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
eqv : C ≌ D
S : Sheaf J RingCat
R : Sheaf K RingCat
inst✝¹ : eqv.functor.IsContinuous J K
inst✝ : eqv.inverse.IsContinuous K J
φ : S ⟶ (eqv.functor.sheafPushforwardContinuous RingCat J K).obj R
ψ : R ⟶ (eqv.inverse.sheafPushforwardContinuous RingCat K J).obj S
H₁ : whiskerRight (NatTrans.op eqv.counit) R.obj = ψ.hom ≫ eqv.inverse.op.whiskerLeft φ.hom
H₂ : φ.hom ≫ eqv.functor.op.whiskerLeft ψ.hom ≫ whiskerRight (NatTrans.op eqv.unit) S.obj = 𝟙 S.obj
this : (eqv.functor ⋙ eqv.inverse).IsContinuous J J := ⋯
⊢ ((φ ≫ (eqv.functor.sheafPushforwardContinuous RingCat J K).map ψ) ≫
        (sheafPushforwardContinuousNatTrans eqv.unitIso.hom RingCat J J).app S).hom =
    (𝟙 S).hom

Tactic:
;

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✝
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : GrothendieckTopology C
K : GrothendieckTopology D
eqv : C ≌ D
S : Sheaf J RingCat
R : Sheaf K RingCat
inst✝¹ : eqv.functor.IsContinuous J K
inst✝ : eqv.inverse.IsContinuous K J
φ : S ⟶ (eqv.functor.sheafPushforwardContinuous RingCat J K).obj R
ψ : R ⟶ (eqv.inverse.sheafPushforwardContinuous RingCat K J).obj S
H₁ : whiskerRight (NatTrans.op eqv.counit) R.obj = ψ.hom ≫ eqv.inverse.op.whiskerLeft φ.hom
H₂ : φ.hom ≫ eqv.functor.op.whiskerLeft ψ.hom ≫ whiskerRight (NatTrans.op eqv.unit) S.obj = 𝟙 S.obj
this : (eqv.functor ⋙ eqv.inverse).IsContinuous J J := ⋯
⊢ ((φ ≫ (eqv.functor.sheafPushforwardContinuous RingCat J K).map ψ) ≫
        (sheafPushforwardContinuousNatTrans eqv.unitIso.hom RingCat J J).app S).hom =
    (𝟙 S).hom
Module: Mathlib.Topology.Sheaves.SheafCondition.Sites

Goal state before:
pp: case mpr
X : TopCat
ι : Type u_1
inst✝ : Category.{v_1, u_1} ι
B : ι ⥤ Opens ↑X
hb : ∀ {U : Opens ↑X} {x : ↑X}, x ∈ U → ∃ U' ∈ Set.range B.obj, x ∈ U' ∧ U' ≤ U
⊢ B.IsCoverDense (Opens.grothendieckTopology ↑X)

Tactic:
;

Goal state after:
case mpr
X : TopCat
ι : Type u_1
inst✝ : Category.{v_1, u_1} ι
B : ι ⥤ Opens ↑X
hb : ∀ {U : Opens ↑X} {x : ↑X}, x ∈ U → ∃ U' ∈ Set.range B.obj, x ∈ U' ∧ U' ≤ U
⊢ B.IsCoverDense (Opens.grothendieckTopology ↑X)
Module: Mathlib.Topology.Sheaves.SheafCondition.Sites

Goal state before:
pp: case mpr
X : TopCat
ι : Type u_1
inst✝ : Category.{v_1, u_1} ι
B : ι ⥤ Opens ↑X
hb : ∀ {U : Opens ↑X} {x : ↑X}, x ∈ U → ∃ U' ∈ Set.range B.obj, x ∈ U' ∧ U' ≤ U
⊢ ∀ (U : Opens ↑X), Sieve.coverByImage B U ∈ (Opens.grothendieckTopology ↑X) U

Tactic:
;

Goal state after:
case mpr
X : TopCat
ι : Type u_1
inst✝ : Category.{v_1, u_1} ι
B : ι ⥤ Opens ↑X
hb : ∀ {U : Opens ↑X} {x : ↑X}, x ∈ U → ∃ U' ∈ Set.range B.obj, x ∈ U' ∧ U' ≤ U
⊢ ∀ (U : Opens ↑X), Sieve.coverByImage B U ∈ (Opens.grothendieckTopology ↑X) U
Module: Mathlib.Topology.Sheaves.SheafCondition.Sites

Goal state before:
pp: case mpr
X : TopCat
ι : Type u_1
inst✝ : Category.{v_1, u_1} ι
B : ι ⥤ Opens ↑X
hb : ∀ {U : Opens ↑X} {x : ↑X}, x ∈ U → ∃ U' ∈ Set.range B.obj, x ∈ U' ∧ U' ≤ U
U : Opens ↑X
x : ↑X
hx : x ∈ U
⊢ ∃ U_1 f, (Sieve.coverByImage B U).arrows f ∧ x ∈ U_1

Tactic:
;

Goal state after:
case mpr
X : TopCat
ι : Type u_1
inst✝ : Category.{v_1, u_1} ι
B : ι ⥤ Opens ↑X
hb : ∀ {U : Opens ↑X} {x : ↑X}, x ∈ U → ∃ U' ∈ Set.range B.obj, x ∈ U' ∧ U' ≤ U
U : Opens ↑X
x : ↑X
hx : x ∈ U
⊢ ∃ U_1 f, (Sieve.coverByImage B U).arrows f ∧ x ∈ U_1
Module: Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing

Goal state before:
pp: case e'_2
X : TopCat
F : Presheaf (Type u_4) X
ι : Type x
U : ι → Opens ↑X
s : (j : (CategoryTheory.Pairwise ι)ᵒᵖ) → ((Pairwise.diagram U).op ⋙ F).obj j
h :
  ∃! s_1,
    ∀ (i : (CategoryTheory.Pairwise ι)ᵒᵖ),
      (ConcreteCategory.hom ((Functor.mapCone F (Pairwise.cocone U).op).π.app i)) s_1 =
        objPairwiseOfFamily (fun i ↦ s (op (Pairwise.single i))) i
hs : s ∈ ((Pairwise.diagram U).op ⋙ F).sections
e_1✝ : (Functor.mapCone F (Pairwise.cocone U).op).pt = ToType (F.obj (op (iSup U)))
x✝ : (Functor.mapCone F (Pairwise.cocone U).op).pt
a✝ : (CategoryTheory.Pairwise ι)ᵒᵖ
⊢ s = objPairwiseOfFamily fun i ↦ s (op (Pairwise.single i))

Tactic:
;

Goal state after:
case e'_2
X : TopCat
F : Presheaf (Type u_4) X
ι : Type x
U : ι → Opens ↑X
s : (j : (CategoryTheory.Pairwise ι)ᵒᵖ) → ((Pairwise.diagram U).op ⋙ F).obj j
h :
  ∃! s_1,
    ∀ (i : (CategoryTheory.Pairwise ι)ᵒᵖ),
      (ConcreteCategory.hom ((Functor.mapCone F (Pairwise.cocone U).op).π.app i)) s_1 =
        objPairwiseOfFamily (fun i ↦ s (op (Pairwise.single i))) i
hs : s ∈ ((Pairwise.diagram U).op ⋙ F).sections
e_1✝ : (Functor.mapCone F (Pairwise.cocone U).op).pt = ToType (F.obj (op (iSup U)))
x✝ : (Functor.mapCone F (Pairwise.cocone U).op).pt
a✝ : (CategoryTheory.Pairwise ι)ᵒᵖ
⊢ s = objPairwiseOfFamily fun i ↦ s (op (Pairwise.single i))
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
inst✝² : ∀ (X : C), HasWeakSheafify (J.over X) AddCommGrpCat
inst✝¹ : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat
M : SheafOfModules R
q : M.QuasicoherentData
inst✝ : q.IsFinitePresentation
⊢ ∀ (i : q.I), (q.presentation i).generators.IsFiniteType

Tactic:
;

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R : Sheaf J RingCat
inst✝² : ∀ (X : C), HasWeakSheafify (J.over X) AddCommGrpCat
inst✝¹ : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat
M : SheafOfModules R
q : M.QuasicoherentData
inst✝ : q.IsFinitePresentation
⊢ ∀ (i : q.I), (q.presentation i).generators.IsFiniteType
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
inst✝⁴ : HasBinaryProducts C
J : GrothendieckTopology C
R : Sheaf J RingCat
inst✝³ : HasSheafify J AddCommGrpCat
inst✝² : J.WEqualsLocallyBijective AddCommGrpCat
inst✝¹ : ∀ (X : C), HasSheafify (J.over X) AddCommGrpCat
inst✝ : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat
M : SheafOfModules R
P : M.Presentation
x : C
⊢ ∀ ⦃Y : C⦄ (f : Y ⟶ x), (Sieve.ofObjects id x).arrows f ↔ ⊤.arrows f

Tactic:
intro _ f

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
inst✝⁴ : HasBinaryProducts C
J : GrothendieckTopology C
R : Sheaf J RingCat
inst✝³ : HasSheafify J AddCommGrpCat
inst✝² : J.WEqualsLocallyBijective AddCommGrpCat
inst✝¹ : ∀ (X : C), HasSheafify (J.over X) AddCommGrpCat
inst✝ : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat
M : SheafOfModules R
P : M.Presentation
x Y✝ : C
f : Y✝ ⟶ x
⊢ (Sieve.ofObjects id x).arrows f ↔ ⊤.arrows f
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
inst✝³ : ∀ (X : C), HasSheafify (J.over X) AddCommGrpCat
inst✝² : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat
inst✝¹ : ∀ (X : C) (Y : Over X), HasSheafify ((J.over X).over Y) AddCommGrpCat
inst✝ : ∀ (X : C) (Y : Over X), ((J.over X).over Y).WEqualsLocallyBijective AddCommGrpCat
R : Sheaf J RingCat
M : SheafOfModules R
I : Type u
X : I → C
hX : J.CoversTop X
D : (i : I) → (M.over (X i)).QuasicoherentData
i : (i : I) × (D i).I
x✝ : (Over ((D i.fst).X i.snd).left)ᵒᵖ
⊢ (Functor.whiskerRight (NatTrans.op ((D i.fst).X i.snd).iteratedSliceEquiv.counit)
          (R.over ((D i.fst).X i.snd).left).obj).app
      x✝ =
    ((𝟙 (R.over ((D i.fst).X i.snd).left)).hom ≫
          ((D i.fst).X i.snd).iteratedSliceEquiv.inverse.op.whiskerLeft
            (𝟙 ((R.over (X i.fst)).over ((D i.fst).X i.snd))).hom).app
      x✝

Tactic:
;

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R✝ : Sheaf J RingCat
inst✝³ : ∀ (X : C), HasSheafify (J.over X) AddCommGrpCat
inst✝² : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat
inst✝¹ : ∀ (X : C) (Y : Over X), HasSheafify ((J.over X).over Y) AddCommGrpCat
inst✝ : ∀ (X : C) (Y : Over X), ((J.over X).over Y).WEqualsLocallyBijective AddCommGrpCat
R : Sheaf J RingCat
M : SheafOfModules R
I : Type u
X : I → C
hX : J.CoversTop X
D : (i : I) → (M.over (X i)).QuasicoherentData
i : (i : I) × (D i).I
x✝ : (Over ((D i.fst).X i.snd).left)ᵒᵖ
⊢ (Functor.whiskerRight (NatTrans.op ((D i.fst).X i.snd).iteratedSliceEquiv.counit)
          (R.over ((D i.fst).X i.snd).left).obj).app
      x✝ =
    ((𝟙 (R.over ((D i.fst).X i.snd).left)).hom ≫
          ((D i.fst).X i.snd).iteratedSliceEquiv.inverse.op.whiskerLeft
            (𝟙 ((R.over (X i.fst)).over ((D i.fst).X i.snd))).hom).app
      x✝