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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X Y : C
f : X ⟶ Y
F : Sheaf (J.over Y) (Type u_1)
Z : Over X
x✝ : Presieve Z
x : Presieve.FamilyOfElements ((Over.map f).op ⋙ F.obj) x✝
hx : x.Compatible
Y₁ Y₂ : Over X
W : Over Y
f₁ : W ⟶ (Over.map f).obj Y₁
f₂ : W ⟶ (Over.map f).obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : x✝ g₁
hg₂ : x✝ g₂
h : f₁ ≫ (Over.map f).map g₁ = f₂ ≫ (Over.map f).map g₂
W' : Over X := ⋯
g₁' : W' ⟶ Y₁ := ⋯
g₂' : W' ⟶ Y₂ := ⋯
e : (Over.map f).obj W' ≅ W := ⋯
⊢ Over.Hom.left (g₁' ≫ g₁) = Over.Hom.left (g₂' ≫ g₂)

Tactic:
;

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X Y : C
f : X ⟶ Y
F : Sheaf (J.over Y) (Type u_1)
Z : Over X
x✝ : Presieve Z
x : Presieve.FamilyOfElements ((Over.map f).op ⋙ F.obj) x✝
hx : x.Compatible
Y₁ Y₂ : Over X
W : Over Y
f₁ : W ⟶ (Over.map f).obj Y₁
f₂ : W ⟶ (Over.map f).obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : x✝ g₁
hg₂ : x✝ g₂
h : f₁ ≫ (Over.map f).map g₁ = f₂ ≫ (Over.map f).map g₂
W' : Over X := ⋯
g₁' : W' ⟶ Y₁ := ⋯
g₂' : W' ⟶ Y₂ := ⋯
e : (Over.map f).obj W' ≅ W := ⋯
⊢ Over.Hom.left (g₁' ≫ g₁) = Over.Hom.left (g₂' ≫ g₂)
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J✝ J : GrothendieckTopology C
X : C
Y : Over X
E : (J.over X).OneHypercover Y
i₁ i₂ : E.I₀
W : C
p₁ : W ⟶ (Over.forget X).obj (E.X i₁)
p₂ : W ⟶ (Over.forget X).obj (E.X i₂)
w : p₁ ≫ (Over.forget X).map (E.f i₁) = p₂ ≫ (Over.forget X).map (E.f i₂)
this : p₁ ≫ (E.X i₁).hom = p₂ ≫ (E.X i₂).hom
⊢ Over.Hom.left (Over.homMk p₁ ⋯ ≫ E.f i₁) = Over.Hom.left (Over.homMk p₂ ⋯ ≫ E.f i₂)

Tactic:
;

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J✝ J : GrothendieckTopology C
X : C
Y : Over X
E : (J.over X).OneHypercover Y
i₁ i₂ : E.I₀
W : C
p₁ : W ⟶ (Over.forget X).obj (E.X i₁)
p₂ : W ⟶ (Over.forget X).obj (E.X i₂)
w : p₁ ≫ (Over.forget X).map (E.f i₁) = p₂ ≫ (Over.forget X).map (E.f i₂)
this : p₁ ≫ (E.X i₁).hom = p₂ ≫ (E.X i₂).hom
⊢ Over.Hom.left (Over.homMk p₁ ⋯ ≫ E.f i₁) = Over.Hom.left (Over.homMk p₂ ⋯ ≫ E.f i₂)
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
J✝ : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
X : C
inst✝ : F.PreservesOneHypercovers J K
Y : Over X
E : (J.over X).OneHypercover Y
E' : K.OneHypercover (F.obj ((Over.forget X).obj Y)) := (E.map (Over.forget X) J).map F K
⊢ ∀ (i₁ i₂ : E.I₀) ⦃W : Over (F.obj X)⦄ (p₁ : W ⟶ (Over.post F).obj (E.X i₁)) (p₂ : W ⟶ (Over.post F).obj (E.X i₂)),
    p₁ ≫ (Over.post F).map (E.f i₁) = p₂ ≫ (Over.post F).map (E.f i₂) →
      (E.map (Over.post F)).sieve₁ p₁ p₂ ∈ (K.over (F.obj X)) W

Tactic:
intro i₁ i₂ W p₁ p₂ w
    simp_rw [GrothendieckTopology.mem_over_iff, Sieve.overEquiv_preOneHypercover_sieve₁,
      ← PreOneHypercover.map_comp, Over.post_forget_eq_forget_comp, PreOneHypercover.map_comp]
    exact E'.mem₁ _ _ _ _ congr($(w).left)

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝ : Category.{v', u'} A
X Y : C
f : X ⟶ Y
⊢ J.overMapPullback A f = J.overMapPullback A f

Tactic:
;

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝ : Category.{v', u'} A
X Y : C
f : X ⟶ Y
⊢ J.overMapPullback A f = J.overMapPullback A f
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)
⊢ ∀ {Y : C} (f : Y ⟶ X) [Mono f], IsIso f ↔ f ≠ 0

Tactic:
;

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : IsSimpleOrder (Subobject X)
⊢ ∀ {Y : C} (f : Y ⟶ X) [Mono f], IsIso f ↔ f ≠ 0
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)
Y : C
f : Y ⟶ X
hf : Mono f
⊢ IsIso f ↔ f ≠ 0

Tactic:
;

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : IsSimpleOrder (Subobject X)
Y : C
f : Y ⟶ X
hf : Mono f
⊢ IsIso f ↔ f ≠ 0
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
x : C
i : J
p : F.obj i = x
⊢ c.pt ≤ x

Tactic:
;

Goal state after:
C : Type u
inst✝¹ : Preorder C
J : Type u'
inst✝ : Category.{v, u'} J
F : J ⥤ C
c : Cone F
x : C
i : J
p : F.obj i = x
⊢ c.pt ≤ x
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
x : C
i : J
p : F.obj i = x
⊢ c.pt ≤ F.obj i

Tactic:
;

Goal state after:
C : Type u
inst✝¹ : Preorder C
J : Type u'
inst✝ : Category.{v, u'} J
F : J ⥤ C
c : Cone F
x : C
i : J
p : F.obj i = x
⊢ c.pt ≤ F.obj i
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
x : C
i : J
p : F.obj i = x
⊢ x ≤ c.pt

Tactic:
;

Goal state after:
C : Type u
inst✝¹ : Preorder C
J : Type u'
inst✝ : Category.{v, u'} J
F : J ⥤ C
c : Cocone F
x : C
i : J
p : F.obj i = x
⊢ x ≤ c.pt
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
x : C
i : J
p : F.obj i = x
⊢ F.obj i ≤ c.pt

Tactic:
;

Goal state after:
C : Type u
inst✝¹ : Preorder C
J : Type u'
inst✝ : Category.{v, u'} J
F : J ⥤ C
c : Cocone F
x : C
i : J
p : F.obj i = x
⊢ F.obj i ≤ c.pt
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:
;

Goal state after:
C : Type u
inst✝ : SemilatticeInf C
X Y : C
s✝ : BinaryFan X Y
⊢ homOfLE ⋯ ≫ homOfLE ⋯ = s✝.fst
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:
;

Goal state after:
C : Type u
inst✝ : SemilatticeInf C
X Y : C
s✝ : BinaryFan X Y
⊢ homOfLE ⋯ ≫ homOfLE ⋯ = s✝.snd
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
x✝¹ : m✝ ≫ homOfLE ⋯ = s✝.fst
x✝ : m✝ ≫ homOfLE ⋯ = s✝.snd
⊢ m✝ = homOfLE ⋯

Tactic:
;

Goal state after:
C : Type u
inst✝ : SemilatticeInf C
X Y : C
s✝ : BinaryFan X Y
m✝ : s✝.pt ⟶ X ⊓ Y
x✝¹ : m✝ ≫ homOfLE ⋯ = s✝.fst
x✝ : m✝ ≫ homOfLE ⋯ = s✝.snd
⊢ m✝ = homOfLE ⋯
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:
;

Goal state after:
C : Type u
inst✝ : SemilatticeSup C
X Y : C
s✝ : BinaryCofan X Y
⊢ homOfLE ⋯ ≫ homOfLE ⋯ = s✝.inl
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:
;

Goal state after:
C : Type u
inst✝ : SemilatticeSup C
X Y : C
s✝ : BinaryCofan X Y
⊢ homOfLE ⋯ ≫ homOfLE ⋯ = s✝.inr
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
x✝¹ : homOfLE ⋯ ≫ m✝ = s✝.inl
x✝ : homOfLE ⋯ ≫ m✝ = s✝.inr
⊢ m✝ = homOfLE ⋯

Tactic:
;

Goal state after:
C : Type u
inst✝ : SemilatticeSup C
X Y : C
s✝ : BinaryCofan X Y
m✝ : X ⊔ Y ⟶ s✝.pt
x✝¹ : homOfLE ⋯ ≫ m✝ = s✝.inl
x✝ : homOfLE ⋯ ≫ m✝ = s✝.inr
⊢ m✝ = homOfLE ⋯
Module: Mathlib.Topology.Category.TopCat.Opens

Goal state before:
pp: X Y Z : TopCat
U V W : Opens ↑X
down✝ : U ≤ V
a₂✝ : U ⟶ V
a✝ : (fun f ↦ Set.inclusion ⋯) { down := { down := down✝ } } = (fun f ↦ Set.inclusion ⋯) a₂✝
⊢ { down := { down := down✝ } } = a₂✝

Tactic:
;

Goal state after:
X Y Z : TopCat
U V W : Opens ↑X
down✝ : U ≤ V
a₂✝ : U ⟶ V
a✝ : (fun f ↦ Set.inclusion ⋯) { down := { down := down✝ } } = (fun f ↦ Set.inclusion ⋯) a₂✝
⊢ { down := { down := down✝ } } = a₂✝
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)
x✝ : ↑X
⊢ x✝ ∈ ↑{ carrier := ⇑(ConcreteCategory.hom f) ⁻¹' ↑(sSup x✝¹), is_open' := ⋯ } ↔
    x✝ ∈ ↑(sSup ((fun U ↦ { carrier := ⇑(ConcreteCategory.hom f) ⁻¹' ↑U, is_open' := ⋯ }) '' x✝¹))

Tactic:
;

Goal state after:
X Y Z : TopCat
U V W : Opens ↑X
f : X ⟶ Y
x✝¹ : Set (Opens ↑Y)
x✝ : ↑X
⊢ x✝ ∈ ↑{ carrier := ⇑(ConcreteCategory.hom f) ⁻¹' ↑(sSup x✝¹), is_open' := ⋯ } ↔
    x✝ ∈ ↑(sSup ((fun U ↦ { carrier := ⇑(ConcreteCategory.hom f) ⁻¹' ↑U, is_open' := ⋯ }) '' x✝¹))
Module: Mathlib.Topology.Category.TopCat.OpenNhds

Goal state before:
pp: X Y : TopCat
f : X ⟶ Y
x : ↑X
U V W : OpenNhds x
down✝ : U ≤ V
a₂✝ : U ⟶ V
a✝ : (fun f ↦ Set.inclusion ⋯) { down := { down := down✝ } } = (fun f ↦ Set.inclusion ⋯) a₂✝
⊢ { down := { down := down✝ } } = a₂✝

Tactic:
;

Goal state after:
X Y : TopCat
f : X ⟶ Y
x : ↑X
U V W : OpenNhds x
down✝ : U ≤ V
a₂✝ : U ⟶ V
a✝ : (fun f ↦ Set.inclusion ⋯) { down := { down := down✝ } } = (fun f ↦ Set.inclusion ⋯) a₂✝
⊢ { down := { down := down✝ } } = a₂✝
Module: Mathlib.Topology.Category.TopCat.Opens

Goal state before:
pp: case a
X Y : TopCat
f : X ⟶ Y
hf : IsInducing ⇑(ConcreteCategory.hom f)
x : ↑X
s : Opens ↑Y
hx : (ConcreteCategory.hom f) x ∈ s
⊢ x ∈ (Opens.map f).obj s

Tactic:
;

Goal state after:
case a
X Y : TopCat
f : X ⟶ Y
hf : IsInducing ⇑(ConcreteCategory.hom f)
x : ↑X
s : Opens ↑Y
hx : (ConcreteCategory.hom f) x ∈ s
⊢ x ∈ (Opens.map f).obj s
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
X : SheafOfModules R
U : Cᵒᵖ
⊢ RingCat.Hom.hom (φ.hom.app U) = RingCat.Hom.hom (φ.hom.app U)

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

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
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✝
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
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:
;

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
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✝
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''
x✝¹ : SheafOfModules R''
X✝ : Cᵒᵖ
x✝ : ↑(((pushforward ψ' ⋙ pushforward ψ ⋙ pushforward φ).obj x✝¹).val.obj X✝)
⊢ (ModuleCat.Hom.hom
        ((((pushforward ψ').isoWhiskerLeft (pushforwardComp φ ψ) ≪≫
                      pushforwardComp (φ ≫ (F.sheafPushforwardContinuous RingCat J K).map ψ) ψ').hom.app
                x✝¹).val.app
          X✝))
      x✝ =
    (ModuleCat.Hom.hom
        (((((pushforward ψ').associator (pushforward ψ) (pushforward φ)).symm ≪≫
                      isoWhiskerRight (pushforwardComp ψ ψ') (pushforward φ) ≪≫
                        pushforwardComp φ (ψ ≫ (G.sheafPushforwardContinuous RingCat K K').map ψ')).hom.app
                x✝¹).val.app
          X✝))
      x✝

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
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''
x✝¹ : SheafOfModules R''
X✝ : Cᵒᵖ
x✝ : ↑(((pushforward ψ' ⋙ pushforward ψ ⋙ pushforward φ).obj x✝¹).val.obj X✝)
⊢ (ModuleCat.Hom.hom
        ((((pushforward ψ').isoWhiskerLeft (pushforwardComp φ ψ) ≪≫
                      pushforwardComp (φ ≫ (F.sheafPushforwardContinuous RingCat J K).map ψ) ψ').hom.app
                x✝¹).val.app
          X✝))
      x✝ =
    (ModuleCat.Hom.hom
        (((((pushforward ψ').associator (pushforward ψ) (pushforward φ)).symm ≪≫
                      isoWhiskerRight (pushforwardComp ψ ψ') (pushforward φ) ≪≫
                        pushforwardComp φ (ψ ≫ (G.sheafPushforwardContinuous RingCat K K').map ψ')).hom.app
                x✝¹).val.app
          X✝))
      x✝
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
x✝¹ : SheafOfModules R
X✝ : Cᵒᵖ
x✝ : ↑(((pushforward φ ⋙ pushforward (𝟙 S)).obj x✝¹).val.obj X✝)
⊢ (ModuleCat.Hom.hom (((pushforwardComp (𝟙 S) φ).hom.app x✝¹).val.app X✝)) x✝ =
    (ModuleCat.Hom.hom
        ((((pushforward φ).isoWhiskerLeft (pushforwardId S) ≪≫ (pushforward φ).rightUnitor).hom.app x✝¹).val.app X✝))
      x✝

Tactic:
;

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
S : Sheaf J RingCat
R : Sheaf K RingCat
inst✝ : F.IsContinuous J K
φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R
x✝¹ : SheafOfModules R
X✝ : Cᵒᵖ
x✝ : ↑(((pushforward φ ⋙ pushforward (𝟙 S)).obj x✝¹).val.obj X✝)
⊢ (ModuleCat.Hom.hom (((pushforwardComp (𝟙 S) φ).hom.app x✝¹).val.app X✝)) x✝ =
    (ModuleCat.Hom.hom
        ((((pushforward φ).isoWhiskerLeft (pushforwardId S) ≪≫ (pushforward φ).rightUnitor).hom.app x✝¹).val.app X✝))
      x✝
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
x✝¹ : SheafOfModules R
X✝ : Cᵒᵖ
x✝ : ↑(((pushforward (𝟙 R) ⋙ pushforward φ).obj x✝¹).val.obj X✝)
⊢ (ModuleCat.Hom.hom (((pushforwardComp φ (𝟙 R)).hom.app x✝¹).val.app X✝)) x✝ =
    (ModuleCat.Hom.hom
        (((isoWhiskerRight (pushforwardId R) (pushforward φ) ≪≫ (pushforward φ).leftUnitor).hom.app x✝¹).val.app X✝))
      x✝

Tactic:
;

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
S : Sheaf J RingCat
R : Sheaf K RingCat
inst✝ : F.IsContinuous J K
φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R
x✝¹ : SheafOfModules R
X✝ : Cᵒᵖ
x✝ : ↑(((pushforward (𝟙 R) ⋙ pushforward φ).obj x✝¹).val.obj X✝)
⊢ (ModuleCat.Hom.hom (((pushforwardComp φ (𝟙 R)).hom.app x✝¹).val.app X✝)) x✝ =
    (ModuleCat.Hom.hom
        (((isoWhiskerRight (pushforwardId R) (pushforward φ) ≪≫ (pushforward φ).leftUnitor).hom.app x✝¹).val.app X✝))
      x✝
Module: Mathlib.Topology.Category.TopCat.Opens

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

Tactic:
;

Goal state after:
X : TopCat
U : Opens ↑X
V : Opens ↥U
⊢ ⋯.functor.obj ((map U.inclusion').obj (⋯.functor.obj V)) = ⋯.functor.obj V
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
j : J
⊢ s.pt ≤ F.obj j

Tactic:
;

Goal state after:
α : Type u
inst✝¹ : CompleteLattice α
J : Type w
inst✝ : Category.{w', w} J
F : J ⥤ α
s : Cone F
j : J
⊢ s.pt ≤ F.obj j
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
j : J
⊢ F.obj j ≤ s.pt

Tactic:
;

Goal state after:
α : Type u
inst✝¹ : CompleteLattice α
J : Type w
inst✝ : Category.{w', w} J
F : J ⥤ α
s : Cocone F
j : J
⊢ F.obj j ≤ s.pt
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✝ : Cᵒᵖ
⊢ ((φ ≫ (sheafPushforwardContinuousNatTrans α.hom RingCat J K).app S) ≫
            (sheafPushforwardContinuousNatTrans α.inv RingCat J K).app S).hom.app
      x✝ =
    φ.hom.app x✝

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 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✝ : Cᵒᵖ
⊢ ((φ ≫ (sheafPushforwardContinuousNatTrans α.hom RingCat J K).app S) ≫
            (sheafPushforwardContinuousNatTrans α.inv RingCat J K).app S).hom.app
      x✝ =
    φ.hom.app x✝