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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : Simple X
a : Subobject X
⊢ a = ⊥ ∨ a = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : IsSimpleOrder (Subobject X)
⊢ Simple X

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X : C
⊢ Simple X → IsSimpleOrder (Subobject X)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X : C
⊢ IsSimpleOrder (Subobject X) → Simple X

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Preorder C
J : Type u'
inst✝ : Category.{v, u'} J
F : J ⥤ C
c : Cone F
⊢ c.pt ∈ lowerBounds (Set.range F.obj)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Preorder C
J : Type u'
inst✝ : Category.{v, u'} J
F : J ⥤ C
c : Cocone F
⊢ c.pt ∈ upperBounds (Set.range F.obj)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : SemilatticeInf C
X Y : C
⊢ ∀ (s : BinaryFan X Y), homOfLE ⋯ ≫ homOfLE ⋯ = s.fst

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : SemilatticeInf C
X Y : C
⊢ ∀ (s : BinaryFan X Y), homOfLE ⋯ ≫ homOfLE ⋯ = s.snd

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : SemilatticeInf C
X Y : C
⊢ ∀ (s : BinaryFan X Y) (m : s.pt ⟶ X ⊓ Y), m ≫ homOfLE ⋯ = s.fst → m ≫ homOfLE ⋯ = s.snd → m = homOfLE ⋯

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : SemilatticeInf C
F : Discrete WalkingPair ⥤ C
⊢ HasLimit F

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : SemilatticeSup C
X Y : C
⊢ ∀ (s : BinaryCofan X Y), homOfLE ⋯ ≫ homOfLE ⋯ = s.inl

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : SemilatticeSup C
X Y : C
⊢ ∀ (s : BinaryCofan X Y), homOfLE ⋯ ≫ homOfLE ⋯ = s.inr

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : SemilatticeSup C
X Y : C
⊢ ∀ (s : BinaryCofan X Y) (m : X ⊔ Y ⟶ s.pt), homOfLE ⋯ ≫ m = s.inl → homOfLE ⋯ ≫ m = s.inr → m = homOfLE ⋯

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : SemilatticeSup C
F : Discrete WalkingPair ⥤ C
⊢ HasColimit F

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : CompleteLattice C
ι : Type u_1
X : ι → C
⊢ IsGLB (Set.range (Discrete.functor X).obj) (Fan.mk (⨅ i, X i) fun i ↦ homOfLE ⋯).pt

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : CompleteLattice C
ι : Type u_1
X : ι → C
⊢ IsLUB (Set.range (Discrete.functor X).obj) (Cofan.mk (⨆ i, X i) fun i ↦ homOfLE ⋯).pt

Tactic:
by

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

Goal state before:
pp: X Y Z : TopCat
U V W : Opens ↑X
⊢ Function.Injective fun f ↦ Set.inclusion ⋯

Tactic:
by

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

Goal state before:
pp: X Y Z : TopCat
U V W : Opens ↑X
f : X ⟶ Y
x✝ : Set (Opens ↑Y)
⊢ { carrier := ⇑(ConcreteCategory.hom f) ⁻¹' ↑(sSup x✝), is_open' := ⋯ } =
    sSup ((fun U ↦ { carrier := ⇑(ConcreteCategory.hom f) ⁻¹' ↑U, is_open' := ⋯ }) '' x✝)

Tactic:
by

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

Goal state before:
pp: X : TopCat
U : (Opens ↑X)ᵒᵖ
⊢ (map (𝟙 X)).obj (unop U) = unop U

Tactic:
by

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

Goal state before:
pp: X : TopCat
U : (Opens ↑X)ᵒᵖ
⊢ (map (𝟙 X)).op.obj U = U

Tactic:
by

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

Goal state before:
pp: X Y : TopCat
f : X ⟶ Y
x✝¹ : ↑X
U V W : OpenNhds x✝¹
x✝ : ↑X
x : OpenNhds x✝
⊢ x ≤ ⟨⊤, trivial⟩

Tactic:
by

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

Goal state before:
pp: X Y : TopCat
f : X ⟶ Y
x : ↑X
U V W : OpenNhds x
⊢ Function.Injective fun f ↦ Set.inclusion ⋯

Tactic:
by

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

Goal state before:
pp: X Y : TopCat
f : X ⟶ Y
ι : Type u_1
U : ι → Opens ↑Y
⊢ (map f).obj (iSup U) = iSup ((map f).obj ∘ U)

Tactic:
by

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

Goal state before:
pp: X : TopCat
x : ↑X
U : (OpenNhds x)ᵒᵖ
⊢ (map (𝟙 X) x).obj (unop U) = unop U

Tactic:
by

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

Goal state before:
pp: X : TopCat
x : ↑X
U : (OpenNhds x)ᵒᵖ
⊢ (map (𝟙 X) x).op.obj U = U

Tactic:
by

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

Goal state before:
pp: X : TopCat
⊢ map (𝟙 X) = 𝟭 (Opens ↑X)

Tactic:
by

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

Goal state before:
pp: X Y Z : TopCat
U✝ V W : Opens ↑X
f g : X ⟶ Y
h : f = g
U : Opens ↑Y
⊢ (map f).obj U = (map g).obj U

Tactic:
by

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

Goal state before:
pp: X Y : TopCat
f g : X ⟶ Y
h : f = g
⊢ map f = map g

Tactic:
by

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

Goal state before:
pp: X Y Z : TopCat
U✝ V W : Opens ↑X
f g : X ⟶ Y
h : f = g
U : Opens ↑Y
⊢ (map g).obj U = (map f).obj U

Tactic:
by

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

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

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

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

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

Goal state before:
pp: X Y : TopCat
f : X ⟶ Y
hf : IsOpenMap ⇑(ConcreteCategory.hom f)
H : Mono f
X✝ Y✝ : Opens ↑X
i : hf.functor.obj X✝ ⟶ hf.functor.obj Y✝
x : ↑X
hx : x ∈ X✝
⊢ x ∈ Y✝

Tactic:
by

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

Goal state before:
pp: X Y : TopCat
f : X ⟶ Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
ι : Type u_1
inst✝¹ : Nonempty ι
inst✝ : Finite ι
g : ι → Opens ↑X
⊢ hf.functor.obj (⨅ i, g i) = ⨅ i, hf.functor.obj (g i)

Tactic:
by

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

Goal state before:
pp: X Y : TopCat
f : X ⟶ Y
hf : IsInducing ⇑(ConcreteCategory.hom f)
U : Opens ↑X
⊢ (Opens.map f).obj (hf.functorObj U) = U

Tactic:
by

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

Goal state before:
pp: X Y : TopCat
f : X ⟶ Y
hf : IsInducing ⇑(ConcreteCategory.hom f)
U : Opens ↑X
x : ↑X
⊢ (ConcreteCategory.hom f) x ∈ hf.functorObj U ↔ x ∈ U

Tactic:
by

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
e : φ = ψ
X : SheafOfModules R
U : Cᵒᵖ
⊢ RingCat.Hom.hom (φ.hom.app U) = RingCat.Hom.hom (ψ.hom.app U)

Tactic:
by

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
e : φ = ψ
X : SheafOfModules R
x✝² x✝¹ : Cᵒᵖ
x✝ : x✝² ⟶ x✝¹
⊢ ((forget S).obj ((pushforward φ).obj X)).map x✝ ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom (S.obj.map x✝))).map
        ((ModuleCat.restrictScalarsCongr ⋯).app
            (((PresheafOfModules.pushforward₀ F ((sheafToPresheaf K RingCat).obj R)).obj X.val).obj x✝¹)).hom =
    ((ModuleCat.restrictScalarsCongr ⋯).app
          (((PresheafOfModules.pushforward₀ F ((sheafToPresheaf K RingCat).obj R)).obj X.val).obj x✝²)).hom ≫
      ((forget S).obj ((pushforward ψ).obj X)).map x✝

Tactic:
by

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
e : φ = ψ
X✝ Y✝ : SheafOfModules R
x✝ : X✝ ⟶ Y✝
⊢ (pushforward φ).map x✝ ≫
      ((fullyFaithfulForget S).preimageIso
          (PresheafOfModules.isoMk
            (fun U ↦
              (ModuleCat.restrictScalarsCongr ⋯).app
                (((PresheafOfModules.pushforward₀ F ((sheafToPresheaf K RingCat).obj R)).obj Y✝.val).obj U))
            ⋯)).hom =
    ((fullyFaithfulForget S).preimageIso
          (PresheafOfModules.isoMk
            (fun U ↦
              (ModuleCat.restrictScalarsCongr ⋯).app
                (((PresheafOfModules.pushforward₀ F ((sheafToPresheaf K RingCat).obj R)).obj X✝.val).obj U))
            ⋯)).hom ≫
      (pushforward ψ).map x✝

Tactic:
by

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

Goal state before:
pp: X Y : TopCat
f : X ⟶ Y
hf : IsInducing ⇑(ConcreteCategory.hom f)
U : Opens ↑X
V : Opens ↑Y
⊢ V ≤ hf.functorObj U ↔ (Opens.map f).obj V ≤ U

Tactic:
by

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

Goal state before:
pp: X : TopCat
U : Opens ↑X
⊢ ⋯.functor.obj ⊤ = U

Tactic:
by

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

Goal state before:
pp: X : TopCat
U : Opens ↑X
⊢ (map U.inclusion').obj U = ⊤

Tactic:
by

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

Goal state before:
pp: X : TopCat
U : Opens ↑X
⊢ (map U.inclusion' ⋙ ⋯.functor).obj U = (𝟭 (Opens ↑X)).obj U

Tactic:
by

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
K' : GrothendieckTopology D'
K'' : GrothendieckTopology D''
G : D ⥤ D'
R' : Sheaf K' RingCat
inst✝³ : G.IsContinuous K K'
ψ : R ⟶ (G.sheafPushforwardContinuous RingCat K K').obj R'
G' : D' ⥤ D''
R'' : Sheaf K'' RingCat
inst✝² : G'.IsContinuous K' K''
inst✝¹ : (G ⋙ G').IsContinuous K K''
inst✝ : (F ⋙ G).IsContinuous J K'
ψ' : R' ⟶ (G'.sheafPushforwardContinuous RingCat K' K'').obj R''
⊢ (pushforward ψ').isoWhiskerLeft (pushforwardComp φ ψ) ≪≫
      pushforwardComp (φ ≫ (F.sheafPushforwardContinuous RingCat J K).map ψ) ψ' =
    ((pushforward ψ').associator (pushforward ψ) (pushforward φ)).symm ≪≫
      isoWhiskerRight (pushforwardComp ψ ψ') (pushforward φ) ≪≫
        pushforwardComp φ (ψ ≫ (G.sheafPushforwardContinuous RingCat K K').map ψ')

Tactic:
by

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

Goal state before:
pp: X : TopCat
⊢ ⋯.functor = map (inclusionTopIso X).inv

Tactic:
by

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 : C ⥤ D
S : Sheaf J RingCat
R : Sheaf K RingCat
inst✝ : F.IsContinuous J K
φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R
⊢ pushforwardComp (𝟙 S) φ = (pushforward φ).isoWhiskerLeft (pushforwardId S) ≪≫ (pushforward φ).rightUnitor

Tactic:
by

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 : C ⥤ D
S : Sheaf J RingCat
R : Sheaf K RingCat
inst✝ : F.IsContinuous J K
φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R
⊢ pushforwardComp φ (𝟙 R) = isoWhiskerRight (pushforwardId R) (pushforward φ) ≪≫ (pushforward φ).leftUnitor

Tactic:
by

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

Goal state before:
pp: X Y : TopCat
f : X ⟶ Y
hf : IsOpenMap ⇑(ConcreteCategory.hom f)
U : Opens ↑Y
⊢ hf.functor.obj ((map f).obj U) = hf.functor.obj ⊤ ⊓ U

Tactic:
by

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

Goal state before:
pp: X : TopCat
U : Opens ↑X
⊢ Set.range ⇑(ConcreteCategory.hom U.inclusion') = ↑U

Tactic:
by

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

Goal state before:
pp: X : TopCat
U V : Opens ↑X
⊢ ⋯.functor.obj ((map U.inclusion').obj V) = V ⊓ U

Tactic:
by

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

Goal state before:
pp: X : TopCat
U : Opens ↑X
V : Opens ↥U
⊢ (map U.inclusion' ⋙ ⋯.functor).obj (⋯.functor.obj V) = (𝟭 (Opens ↑X)).obj (⋯.functor.obj V)

Tactic:
by

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

Goal state before:
pp: X : TopCat
U : Opens ↑X
V : Opens ↥U
⊢ ⋯.adjunction.counit.app (⋯.functor.obj V) = eqToHom ⋯

Tactic:
by

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

Goal state before:
pp: X Y : TopCat
f : X ⟶ Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
ι : Type u_1
inst✝¹ : Nonempty ι
inst✝ : Finite ι
⊢ PreservesLimitsOfShape (Discrete ι) hf.functor

Tactic:
by

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
X : SheafOfModules S
U V : Cᵒᵖ
i : U ⟶ V
⊢ ((pushforward φ).obj X).val.map i ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom (T.obj.map i))).map
        ((ModuleCat.restrictScalars (RingCat.Hom.hom (φ.hom.app V))).map (X.val.map (α.app (Opposite.unop V)).op)) =
    (ModuleCat.restrictScalars (RingCat.Hom.hom (φ.hom.app U))).map (X.val.map (α.app (Opposite.unop U)).op) ≫
      ((pushforward (φ ≫ (sheafPushforwardContinuousNatTrans α RingCat J K).app S)).obj X).val.map i

Tactic:
by

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

Goal state before:
pp: α : Type u
J : Type w
inst✝³ : SmallCategory J
inst✝² : FinCategory J
inst✝¹ : SemilatticeInf α
inst✝ : OrderTop α
⊢ ∀ (J : Type) [𝒥 : SmallCategory J] [FinCategory J], HasLimitsOfShape J α

Tactic:
by

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

Goal state before:
pp: α : Type u
J : Type w
inst✝³ : SmallCategory J
inst✝² : FinCategory J
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
⊢ ∀ (J : Type) [𝒥 : SmallCategory J] [FinCategory J], HasColimitsOfShape J α

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝² : SemilatticeInf α
inst✝¹ : OrderTop α
ι : Type u
inst✝ : Fintype ι
f : ι → α
⊢ ∏ᶜ f = Finset.univ.inf f

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
ι : Type u
inst✝ : Fintype ι
f : ι → α
⊢ ∐ f = Finset.univ.sup f

Tactic:
by

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

Goal state before:
pp: α : Type u
J : Type w
inst✝³ : SmallCategory J
inst✝² : FinCategory J
inst✝¹ : SemilatticeInf α
inst✝ : OrderTop α
⊢ ∀ (x y : α), HasLimit (pair x y)

Tactic:
by

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

Goal state before:
pp: α : Type u
J : Type w
inst✝³ : SmallCategory J
inst✝² : FinCategory J
inst✝¹ : SemilatticeInf α
inst✝ : OrderTop α
⊢ HasBinaryProducts α

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝¹ : SemilatticeInf α
inst✝ : OrderTop α
x y : α
⊢ limit (pair x y) = Finset.univ.inf (pair x y).obj

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝¹ : SemilatticeInf α
inst✝ : OrderTop α
x y : α
⊢ x ⊓ (y ⊓ ⊤) = x ⊓ y

Tactic:
by

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

Goal state before:
pp: α : Type u
J : Type w
inst✝³ : SmallCategory J
inst✝² : FinCategory J
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
⊢ ∀ (x y : α), HasColimit (pair x y)

Tactic:
by

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

Goal state before:
pp: α : Type u
J : Type w
inst✝³ : SmallCategory J
inst✝² : FinCategory J
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
⊢ HasBinaryCoproducts α

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
x y : α
⊢ colimit (pair x y) = Finset.univ.sup (pair x y).obj

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
x y : α
⊢ x ⊔ (y ⊔ ⊥) = x ⊔ y

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝¹ : SemilatticeInf α
inst✝ : OrderTop α
x y z : α
f : x ⟶ z
g : y ⟶ z
⊢ limit (cospan f g) = Finset.univ.inf (cospan f g).obj

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝¹ : SemilatticeInf α
inst✝ : OrderTop α
x y z : α
f : x ⟶ z
g : y ⟶ z
⊢ z ⊓ (x ⊓ (y ⊓ ⊤)) = z ⊓ (x ⊓ y)

Tactic:
by

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
X Y : SheafOfModules S
f : X ⟶ Y
⊢ (pushforward φ).map f ≫
      {
        val :=
          {
            app := fun U ↦
              (ModuleCat.restrictScalars (RingCat.Hom.hom (φ.hom.app U))).map (Y.val.map (α.app (Opposite.unop U)).op),
            naturality := ⋯ } } =
    {
        val :=
          {
            app := fun U ↦
              (ModuleCat.restrictScalars (RingCat.Hom.hom (φ.hom.app U))).map (X.val.map (α.app (Opposite.unop U)).op),
            naturality := ⋯ } } ≫
      (pushforward (φ ≫ (sheafPushforwardContinuousNatTrans α RingCat J K).app S)).map f

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
x y z : α
f : z ⟶ x
g : z ⟶ y
⊢ colimit (span f g) = Finset.univ.sup (span f g).obj

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
x y z : α
f : z ⟶ x
g : z ⟶ y
⊢ z ⊔ (x ⊔ (y ⊔ ⊥)) = z ⊔ (x ⊔ y)

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝¹ : CompleteLattice α
J : Type w
inst✝ : Category.{w', w} J
F : J ⥤ α
s : Cone F
⊢ ∀ b ∈ Set.range F.obj, s.pt ≤ b

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝¹ : CompleteLattice α
J : Type w
inst✝ : Category.{w', w} J
F : J ⥤ α
s : Cocone F
⊢ ∀ b ∈ Set.range F.obj, b ≤ s.pt

Tactic:
by

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

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

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

Goal state before:
pp: T : Type u
inst✝ : TopologicalSpace T
X Y : Opens T
S : Sieve X
f : Y ⟶ X
hf : S ∈ {S | ∀ x ∈ X, ∃ U f, S.arrows f ∧ x ∈ U}
y : T
hy : y ∈ Y
⊢ ∃ U f_1, (Sieve.pullback f S).arrows f_1 ∧ y ∈ U

Tactic:
by

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

Goal state before:
pp: T : Type u
inst✝ : TopologicalSpace T
X : Opens T
S : Sieve X
hS : S ∈ {S | ∀ x ∈ X, ∃ U f, S.arrows f ∧ x ∈ U}
R : Sieve X
hR : ∀ ⦃Y : Opens T⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ {S | ∀ x ∈ Y, ∃ U f, S.arrows f ∧ x ∈ U}
x : T
hx : x ∈ X
⊢ ∃ U f, R.arrows f ∧ x ∈ U

Tactic:
by

Goal state after: