mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.LocallyFree

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
inst✝³ : ∀ (X : C), HasSheafify (J.over X) AddCommGrpCat
inst✝² : HasBinaryProducts C
inst✝¹ : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat
inst✝ : HasSheafify J AddCommGrpCat
I : Type u
i : (free.generatingSections I).localGeneratorsData.I
⊢ IsIso ((free.generatingSections I).localGeneratorsData.generators i).π

Tactic:
dsimp

Goal state after:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R : Sheaf J RingCat
inst✝⁵ : HasWeakSheafify J AddCommGrpCat
inst✝⁴ : J.WEqualsLocallyBijective AddCommGrpCat
inst✝³ : ∀ (X : C), HasSheafify (J.over X) AddCommGrpCat
inst✝² : HasBinaryProducts C
inst✝¹ : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat
inst✝ : HasSheafify J AddCommGrpCat
I : Type u
i : (free.generatingSections I).localGeneratorsData.I
⊢ IsIso ((free.generatingSections I).map (pushforward (𝟙 (R.over i))) (Iso.refl (unit (R.over i)))).π
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
x✝¹ : Sheaf (J.over Y) A
x✝ : (Over X)ᵒᵖ
⊢ (((J.overMapPullbackComp A f (𝟙 Y)).inv ≫
                Functor.whiskerRight (J.overMapPullbackId A Y).hom (J.overMapPullback A f) ≫
                  (J.overMapPullback A f).leftUnitor.hom).app
            x✝¹).hom.app
      x✝ =
    ((J.overMapPullbackCongr A ⋯).hom.app x✝¹).hom.app x✝

Tactic:
dsimp

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
x✝¹ : Sheaf (J.over Y) A
x✝ : (Over X)ᵒᵖ
⊢ ((J.overMapPullbackComp A f (𝟙 Y)).inv.app x✝¹).hom.app x✝ ≫
      ((J.overMapPullbackId A Y).hom.app x✝¹).hom.app (Opposite.op ((Over.map f).obj (Opposite.unop x✝))) ≫
        𝟙 (x✝¹.obj.obj (Opposite.op ((Over.map f).obj (Opposite.unop x✝)))) =
    x✝¹.obj.map ((Over.mapCongr (f ≫ 𝟙 Y) f ⋯).inv.app (Opposite.unop x✝)).op
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
x✝¹ : Sheaf (J.over Y) A
x✝ : (Over X)ᵒᵖ
⊢ (((J.overMapPullbackComp A (𝟙 X) f).inv ≫
                (J.overMapPullback A f).whiskerLeft (J.overMapPullbackId A X).hom ≫
                  (J.overMapPullback A f).rightUnitor.hom).app
            x✝¹).hom.app
      x✝ =
    ((J.overMapPullbackCongr A ⋯).hom.app x✝¹).hom.app x✝

Tactic:
dsimp

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
x✝¹ : Sheaf (J.over Y) A
x✝ : (Over X)ᵒᵖ
⊢ ((J.overMapPullbackComp A (𝟙 X) f).inv.app x✝¹).hom.app x✝ ≫
      ((J.overMapPullbackId A X).hom.app ((J.overMapPullback A f).obj x✝¹)).hom.app x✝ ≫
        𝟙 (x✝¹.obj.obj (Opposite.op ((Over.map f).obj (Opposite.unop x✝)))) =
    x✝¹.obj.map ((Over.mapCongr (𝟙 X ≫ f) f ⋯).inv.app (Opposite.unop x✝)).op
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 Z T : C
f : X ⟶ Y
g : Y ⟶ Z
h : Z ⟶ T
x✝¹ : Sheaf (J.over T) A
x✝ : (Over X)ᵒᵖ
⊢ (((J.overMapPullbackComp A f (g ≫ h)).inv ≫
                Functor.whiskerRight (J.overMapPullbackComp A g h).inv (J.overMapPullback A f) ≫
                  ((J.overMapPullback A h).associator (J.overMapPullback A g) (J.overMapPullback A f)).hom ≫
                    (J.overMapPullback A h).whiskerLeft (J.overMapPullbackComp A f g).hom ≫
                      (J.overMapPullbackComp A (f ≫ g) h).hom).app
            x✝¹).hom.app
      x✝ =
    ((J.overMapPullbackCongr A ⋯).hom.app x✝¹).hom.app x✝

Tactic:
dsimp

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝ : Category.{v', u'} A
X Y Z T : C
f : X ⟶ Y
g : Y ⟶ Z
h : Z ⟶ T
x✝¹ : Sheaf (J.over T) A
x✝ : (Over X)ᵒᵖ
⊢ ((J.overMapPullbackComp A f (g ≫ h)).inv.app x✝¹).hom.app x✝ ≫
      ((J.overMapPullbackComp A g h).inv.app x✝¹).hom.app (Opposite.op ((Over.map f).obj (Opposite.unop x✝))) ≫
        𝟙 (x✝¹.obj.obj (Opposite.op ((Over.map h).obj ((Over.map g).obj ((Over.map f).obj (Opposite.unop x✝)))))) ≫
          ((J.overMapPullbackComp A f g).hom.app ((J.overMapPullback A h).obj x✝¹)).hom.app x✝ ≫
            ((J.overMapPullbackComp A (f ≫ g) h).hom.app x✝¹).hom.app x✝ =
    x✝¹.obj.map ((Over.mapCongr (f ≫ g ≫ h) ((f ≫ g) ≫ h) ⋯).inv.app (Opposite.unop x✝)).op
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: case refine_1.transitive
C : Type u
inst✝² : Category.{v, u} C
K : Precoverage C
inst✝¹ : K.HasPullbacks
inst✝ : K.IsStableUnderBaseChange
X Y✝ : C
R✝ : Sieve Y✝
Y : C
R S : Sieve Y
hR : K.toCoverage.Saturate Y R
H : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → K.toCoverage.Saturate Y_1 (Sieve.pullback f S)
s : Y ⟶ X
Z : Over X
ih :
  ∀ (s : Y ⟶ X),
    (Sieve.overEquiv { left := Y, right := Z.right, hom := s }).symm R ∈
      (Precoverage.comap (Over.forget X) K).toGrothendieck { left := Y, right := Z.right, hom := s }
ih' :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
    R.arrows f →
      ∀ (s : Y_1 ⟶ X),
        (Sieve.overEquiv { left := Y_1, right := Z.right, hom := s }).symm (Sieve.pullback f S) ∈
          (Precoverage.comap (Over.forget X) K).toGrothendieck { left := Y_1, right := Z.right, hom := s }
g : Z ⟶ { left := Y, right := Z.right, hom := s }
hg : ((Sieve.overEquiv { left := Y, right := Z.right, hom := s }).symm R).arrows g
⊢ Sieve.pullback g ((Sieve.overEquiv { left := Y, right := Z.right, hom := s }).symm S) ∈
    (Precoverage.comap (Over.forget X) K).toGrothendieck Z

Tactic:
← Sieve.overEquiv_symm_pullback

Goal state after:
case refine_1.transitive
C : Type u
inst✝² : Category.{v, u} C
K : Precoverage C
inst✝¹ : K.HasPullbacks
inst✝ : K.IsStableUnderBaseChange
X Y✝ : C
R✝ : Sieve Y✝
Y : C
R S : Sieve Y
hR : K.toCoverage.Saturate Y R
H : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → K.toCoverage.Saturate Y_1 (Sieve.pullback f S)
s : Y ⟶ X
Z : Over X
ih :
  ∀ (s : Y ⟶ X),
    (Sieve.overEquiv { left := Y, right := Z.right, hom := s }).symm R ∈
      (Precoverage.comap (Over.forget X) K).toGrothendieck { left := Y, right := Z.right, hom := s }
ih' :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
    R.arrows f →
      ∀ (s : Y_1 ⟶ X),
        (Sieve.overEquiv { left := Y_1, right := Z.right, hom := s }).symm (Sieve.pullback f S) ∈
          (Precoverage.comap (Over.forget X) K).toGrothendieck { left := Y_1, right := Z.right, hom := s }
g : Z ⟶ { left := Y, right := Z.right, hom := s }
hg : ((Sieve.overEquiv { left := Y, right := Z.right, hom := s }).symm R).arrows g
⊢ (Sieve.overEquiv Z).symm (Sieve.pullback (Over.Hom.left g) S) ∈ (Precoverage.comap (Over.forget X) K).toGrothendieck Z
Module: Mathlib.CategoryTheory.Limits.Final.Type

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
P : D ⥤ Type w
inst✝ : F.Initial
t : ↑(F ⋙ P).sections
Y : D
Z₁ Z₂ : CostructuredArrow F Y
φ : Z₁ ⟶ Z₂
⊢ (ConcreteCategory.hom (P.map Z₁.hom)) (↑t Z₁.left) = (ConcreteCategory.hom (P.map Z₂.hom)) (↑t Z₂.left)

Tactic:
dsimp

Goal state after:
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
P : D ⥤ Type w
inst✝ : F.Initial
t : ↑(F ⋙ P).sections
Y : D
Z₁ Z₂ : CostructuredArrow F Y
φ : Z₁ ⟶ Z₂
⊢ (ConcreteCategory.hom (P.map Z₁.hom)) (↑t Z₁.left) = (ConcreteCategory.hom (P.map Z₂.hom)) (↑t Z₂.left)
Module: Mathlib.CategoryTheory.Limits.Final.Type

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
P : D ⥤ Type w
inst✝ : F.Initial
t : ↑(F ⋙ P).sections
Y : D
Z₁ Z₂ : CostructuredArrow F Y
φ : Z₁ ⟶ Z₂
⊢ (ConcreteCategory.hom (P.map Z₁.hom)) (↑t Z₁.left) =
    (ConcreteCategory.hom (P.map Z₂.hom)) ((ConcreteCategory.hom ((F ⋙ P).map φ.left)) (↑t Z₁.left))

Tactic:
dsimp

Goal state after:
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
P : D ⥤ Type w
inst✝ : F.Initial
t : ↑(F ⋙ P).sections
Y : D
Z₁ Z₂ : CostructuredArrow F Y
φ : Z₁ ⟶ Z₂
⊢ (ConcreteCategory.hom (P.map Z₁.hom)) (↑t Z₁.left) =
    (ConcreteCategory.hom (P.map Z₂.hom)) ((ConcreteCategory.hom (P.map (F.map φ.left))) (↑t Z₁.left))
Module: Mathlib.CategoryTheory.Limits.Final.Type

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
P : D ⥤ Type w
inst✝ : F.Final
Y : D
Z₁ Z₂ : StructuredArrow Y F
f : Z₁ ⟶ Z₂
x : (fun X ↦ X) (P.obj Y)
⊢ ((F ⋙ P).ιColimitType Z₁.right ∘ ⇑(ConcreteCategory.hom (P.map Z₁.hom))) x =
    ((F ⋙ P).ιColimitType Z₂.right ∘ ⇑(ConcreteCategory.hom (P.map Z₂.hom))) x

Tactic:
dsimp

Goal state after:
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
P : D ⥤ Type w
inst✝ : F.Final
Y : D
Z₁ Z₂ : StructuredArrow Y F
f : Z₁ ⟶ Z₂
x : (fun X ↦ X) (P.obj Y)
⊢ (F ⋙ P).ιColimitType Z₁.right ((ConcreteCategory.hom (P.map Z₁.hom)) x) =
    (F ⋙ P).ιColimitType Z₂.right ((ConcreteCategory.hom (P.map Z₂.hom)) x)
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackFree

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
inst✝¹ : (pushforward φ).IsRightAdjoint
inst✝ : F.Final
M : SheafOfModules R
f : unit R ⟶ M
⊢ (⇑((pushforward φ).obj M).unitHomEquiv ∘
        ⇑((pullbackPushforwardAdjunction φ).homEquiv (unit S) M) ∘ fun x ↦ pullbackObjUnitToUnit φ ≫ x)
      f =
    (pushforwardSections φ ∘ ⇑M.unitHomEquiv) f

Tactic:
dsimp

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
inst✝¹ : (pushforward φ).IsRightAdjoint
inst✝ : F.Final
M : SheafOfModules R
f : unit R ⟶ M
⊢ ((pushforward φ).obj M).unitHomEquiv
      (((pullbackPushforwardAdjunction φ).homEquiv (unit S) M) (pullbackObjUnitToUnit φ ≫ f)) =
    pushforwardSections φ (M.unitHomEquiv f)
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
D : Type u_1
inst✝³ : Category.{v_1, u_1} D
inst✝² : HasZeroMorphisms D
F : C ⥤ D
inst✝¹ : F.IsEquivalence
X : C
inst✝ : Simple X
this :
  F.asEquivalence.functor.obj (F.asEquivalence.inverse.obj (F.asEquivalence.functor.obj X)) ≅
    F.asEquivalence.functor.obj X
⊢ Simple (F.asEquivalence.functor.obj X)

Tactic:
have := Simple.of_iso <| Functor.preimageIso _ this

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
D : Type u_1
inst✝³ : Category.{v_1, u_1} D
inst✝² : HasZeroMorphisms D
F : C ⥤ D
inst✝¹ : F.IsEquivalence
X : C
inst✝ : Simple X
this✝ :
  F.asEquivalence.functor.obj (F.asEquivalence.inverse.obj (F.asEquivalence.functor.obj X)) ≅
    F.asEquivalence.functor.obj X
this : Simple (F.asEquivalence.inverse.obj (F.asEquivalence.functor.obj X))
⊢ Simple (F.asEquivalence.functor.obj X)
Module: Mathlib.Topology.Category.TopCat.Opens

Goal state before:
pp: case mpr
X Y : TopCat
f : X ⟶ Y
hf : IsInducing ⇑(ConcreteCategory.hom f)
V : Opens ↑Y
t : Set ↑Y
ht : IsOpen t
hU : IsOpen (⇑(ConcreteCategory.hom f) ⁻¹' t)
h : (Opens.map f).obj V ≤ { carrier := ⇑(ConcreteCategory.hom f) ⁻¹' t, is_open' := hU }
x : ↑Y
hx : x ∈ V
⊢ ↑((Opens.map f).obj { carrier := V.carrier ∪ t, is_open' := ⋯ }) =
    ↑{ carrier := ⇑(ConcreteCategory.hom f) ⁻¹' t, is_open' := hU }

Tactic:
dsimp

Goal state after:
case mpr
X Y : TopCat
f : X ⟶ Y
hf : IsInducing ⇑(ConcreteCategory.hom f)
V : Opens ↑Y
t : Set ↑Y
ht : IsOpen t
hU : IsOpen (⇑(ConcreteCategory.hom f) ⁻¹' t)
h : (Opens.map f).obj V ≤ { carrier := ⇑(ConcreteCategory.hom f) ⁻¹' t, is_open' := hU }
x : ↑Y
hx : x ∈ V
⊢ ⇑(ConcreteCategory.hom f) ⁻¹' ↑V ∪ ⇑(ConcreteCategory.hom f) ⁻¹' t = ⇑(ConcreteCategory.hom f) ⁻¹' t
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:
dsimp

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.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:
rw [map_functor_eq V]

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
x : ↑(((pushforward φ).obj X).val.obj U)
⊢ (ModuleCat.Hom.hom
        (((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))))
      x =
    (ModuleCat.Hom.hom
        ((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))
      x

Tactic:
dsimp

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 : SheafOfModules S
U V : Cᵒᵖ
i : U ⟶ V
x : ↑(((pushforward φ).obj X).val.obj U)
⊢ (ModuleCat.Hom.hom
        ((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.Hom.hom (((pushforward φ).obj X).val.map i)) x) =
    (ModuleCat.Hom.hom
        ((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))
      x
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
⊢ IsGLB (Set.range (Discrete.functor fun i ↦ hf.functor.obj (g i)).obj)
    (Fan.mk (hf.functor.obj (Fan.mk (⨅ i, g i) fun i ↦ homOfLE ⋯).pt) fun i ↦
        hf.functor.map ((Fan.mk (⨅ i, g i) fun i ↦ homOfLE ⋯).proj i)).pt

Tactic:
simp only [Discrete.range_functor, homOfLE_leOfHom, Fan.mk_pt, hf.functor_obj_iInf]

Goal state after:
X Y : TopCat
f : X ⟶ Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
ι : Type u_1
inst✝¹ : Nonempty ι
inst✝ : Finite ι
g : ι → Opens ↑X
⊢ IsGLB (Set.range fun i ↦ hf.functor.obj (g i)) (⨅ i, hf.functor.obj (g i))
Module: Mathlib.Topology.Sheaves.Presheaf

Goal state before:
pp: C✝ : Type u
inst✝³ : Category.{v, u} C✝
X✝ : TopCat
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
X Y : TopCat
H₁ : X ≅ Y
ℱ : Presheaf C X
𝒢 : Presheaf C Y
H₂ : (pushforward C H₁.hom).obj ℱ ⟶ 𝒢
U : (Opens ↑X)ᵒᵖ
⊢ U = (Opens.map H₁.hom).op.obj (op ((Opens.map H₁.inv).obj (unop U)))

Tactic:
by simp [Opens.map_def, Set.preimage_preimage]

Goal state after:
Module: Mathlib.Topology.Sheaves.Presheaf

Goal state before:
pp: C✝ : Type u
inst✝³ : Category.{v, u} C✝
X✝ : TopCat
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
X Y : TopCat
H₁ : X ≅ Y
ℱ : Presheaf C Y
𝒢 : Presheaf C X
H₂ : ℱ ⟶ (pushforward C H₁.hom).obj 𝒢
U : (Opens ↑X)ᵒᵖ
⊢ (Opens.map H₁.hom).op.obj (op ((Opens.map H₁.inv).obj (unop U))) = U

Tactic:
by simp [Opens.map_def, Set.preimage_preimage]

Goal state after:
Module: Mathlib.Topology.Sheaves.Presheaf

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
f : X ⟶ Y
ℱ : Presheaf C Y
U V : Opens ↑X
HU : IsOpen (⇑(ConcreteCategory.hom f) '' ↑U)
HV : IsOpen (⇑(ConcreteCategory.hom f) '' ↑V)
le : U ≤ V
j : CostructuredArrow (Opens.map f).op (op V)
eq :
  ((LeftExtension.mk ((Opens.map f).op.leftKanExtension ℱ) ((Opens.map f).op.leftKanExtensionUnit ℱ)).coconeAt
              (op V)).ι.app
        j ≫
      ((pullback C f).obj ℱ).map (homOfLE le).op =
    ((LeftExtension.mk ((Opens.map f).op.leftKanExtension ℱ) ((Opens.map f).op.leftKanExtensionUnit ℱ)).coconeAt
            (op U)).ι.app
      ((CostructuredArrow.map (homOfLE le).op).obj j)
⊢ (CostructuredArrow.proj (Opens.map f).op (op U) ⋙ ℱ).map
      (IsTerminal.from { lift := fun s ↦ CostructuredArrow.homMk (homOfLE ⋯).op ⋯, fac := ⋯, uniq := ⋯ }
        ((CostructuredArrow.map (homOfLE le).op).obj j)) =
    (CostructuredArrow.proj (Opens.map f).op (op V) ⋙ ℱ).map
        (IsTerminal.from { lift := fun s ↦ CostructuredArrow.homMk (homOfLE ⋯).op ⋯, fac := ⋯, uniq := ⋯ } j) ≫
      ℱ.map (IsOpenMap.functorMap HU HV le).op

Tactic:
dsimp

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
f : X ⟶ Y
ℱ : Presheaf C Y
U V : Opens ↑X
HU : IsOpen (⇑(ConcreteCategory.hom f) '' ↑U)
HV : IsOpen (⇑(ConcreteCategory.hom f) '' ↑V)
le : U ≤ V
j : CostructuredArrow (Opens.map f).op (op V)
eq :
  ((LeftExtension.mk ((Opens.map f).op.leftKanExtension ℱ) ((Opens.map f).op.leftKanExtensionUnit ℱ)).coconeAt
              (op V)).ι.app
        j ≫
      ((pullback C f).obj ℱ).map (homOfLE le).op =
    ((LeftExtension.mk ((Opens.map f).op.leftKanExtension ℱ) ((Opens.map f).op.leftKanExtensionUnit ℱ)).coconeAt
            (op U)).ι.app
      ((CostructuredArrow.map (homOfLE le).op).obj j)
⊢ ℱ.map
      ((CostructuredArrow.proj (Opens.map f).op (op U)).map
        (IsTerminal.from { lift := fun s ↦ CostructuredArrow.homMk (homOfLE ⋯).op ⋯, fac := ⋯, uniq := ⋯ }
          ((CostructuredArrow.map (homOfLE le).op).obj j))) =
    ℱ.map
        ((CostructuredArrow.proj (Opens.map f).op (op V)).map
          (IsTerminal.from { lift := fun s ↦ CostructuredArrow.homMk (homOfLE ⋯).op ⋯, fac := ⋯, uniq := ⋯ } j)) ≫
      ℱ.map (IsOpenMap.functorMap HU HV le).op
Module: Mathlib.Topology.Sheaves.Presheaf

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Limits.HasColimits C
X Y : TopCat
f : X ⟶ Y
hf : IsOpenMap ⇑(ConcreteCategory.hom f)
ℱ 𝒢 : TopCat.Presheaf C Y
u : ℱ ⟶ 𝒢
U : Opens ↑X
j : CostructuredArrow (Opens.map f).op (op U)
eq :
  ((LeftExtension.mk ((Opens.map f).op.leftKanExtension ℱ) ((Opens.map f).op.leftKanExtensionUnit ℱ)).coconeAt
              (op U)).ι.app
        j ≫
      ((pullback C f).map u).app (op U) =
    ((CostructuredArrow.proj (Opens.map f).op (op U)).whiskerLeft u).app j ≫
      ((LeftExtension.mk ((Opens.map f).op.leftKanExtension 𝒢) ((Opens.map f).op.leftKanExtensionUnit 𝒢)).coconeAt
              (op U)).ι.app
        j
⊢ ((CostructuredArrow.proj (Opens.map f).op (op U)).whiskerLeft u).app j ≫
      (Limits.coconeOfDiagramTerminal { lift := fun s ↦ CostructuredArrow.homMk (homOfLE ⋯).op ⋯, fac := ⋯, uniq := ⋯ }
              (CostructuredArrow.proj (Opens.map f).op (op U) ⋙ 𝒢)).ι.app
        j =
    (Limits.coconeOfDiagramTerminal { lift := fun s ↦ CostructuredArrow.homMk (homOfLE ⋯).op ⋯, fac := ⋯, uniq := ⋯ }
              (CostructuredArrow.proj (Opens.map f).op (op U) ⋙ ℱ)).ι.app
        j ≫
      u.app (op (hf.functor.obj U))

Tactic:
dsimp

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Limits.HasColimits C
X Y : TopCat
f : X ⟶ Y
hf : IsOpenMap ⇑(ConcreteCategory.hom f)
ℱ 𝒢 : TopCat.Presheaf C Y
u : ℱ ⟶ 𝒢
U : Opens ↑X
j : CostructuredArrow (Opens.map f).op (op U)
eq :
  ((LeftExtension.mk ((Opens.map f).op.leftKanExtension ℱ) ((Opens.map f).op.leftKanExtensionUnit ℱ)).coconeAt
              (op U)).ι.app
        j ≫
      ((pullback C f).map u).app (op U) =
    ((CostructuredArrow.proj (Opens.map f).op (op U)).whiskerLeft u).app j ≫
      ((LeftExtension.mk ((Opens.map f).op.leftKanExtension 𝒢) ((Opens.map f).op.leftKanExtensionUnit 𝒢)).coconeAt
              (op U)).ι.app
        j
⊢ u.app j.left ≫
      𝒢.map
        (Limits.IsTerminal.from { lift := fun s ↦ CostructuredArrow.homMk (homOfLE ⋯).op ⋯, fac := ⋯, uniq := ⋯ }
            j).left =
    ℱ.map
        (Limits.IsTerminal.from { lift := fun s ↦ CostructuredArrow.homMk (homOfLE ⋯).op ⋯, fac := ⋯, uniq := ⋯ }
            j).left ≫
      u.app (op (hf.functor.obj U))
Module: Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Presheaf C X
ι : Type u_2
U : ι → Opens ↑X
Y : Opens ↑X
hY : Y = iSup U
j : (ObjectProperty.FullSubcategory fun f ↦ (Sieve.generate (presieveOfCoveringAux U Y)).arrows f.hom)ᵒᵖ
⊢ F.map (eqToHom ⋯) ≫ (Functor.mapCone F (Sieve.generate (presieveOfCoveringAux U Y)).arrows.cocone.op).π.app j =
    (Cone.whisker (generateEquivalenceOpensLe U hY).op.functor (Functor.mapCone F (opensLeCoverCocone U).op)).π.app j

Tactic:
dsimp

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Presheaf C X
ι : Type u_2
U : ι → Opens ↑X
Y : Opens ↑X
hY : Y = iSup U
j : (ObjectProperty.FullSubcategory fun f ↦ (Sieve.generate (presieveOfCoveringAux U Y)).arrows f.hom)ᵒᵖ
⊢ F.map (eqToHom ⋯) ≫ F.map (unop j).obj.hom.op =
    F.map ((opensLeCoverCocone U).ι.app ((generateEquivalenceOpensLe_functor' U).obj (unop j))).op