mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify

Goal state before:
pp: case hm₀
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
R₀ R : Cᵒᵖ ⥤ RingCat
α : R₀ ⟶ R
inst✝¹ : Presheaf.IsLocallyInjective J α
M₀ : PresheafOfModules R₀
A : Cᵒᵖ ⥤ AddCommGrpCat
φ : M₀.presheaf ⟶ A
inst✝ : Presheaf.IsLocallyInjective J φ
hA : Presheaf.IsSeparated J A
X : C
r : ↑(R.obj (Opposite.op X))
m : ↑(A.obj (Opposite.op X))
Y Z : C
f : Y ⟶ X
g : Z ⟶ Y
r₀ : ↑(R₀.obj (Opposite.op Y))
r₀' : ↑(R₀.obj (Opposite.op Z))
m₀ : ↑(M₀.obj (Opposite.op Y))
m₀' : ↑(M₀.obj (Opposite.op Z))
hr₀ : (ConcreteCategory.hom (α.app (Opposite.op Y))) r₀ = (ConcreteCategory.hom (R.map f.op)) r
hr₀' : (ConcreteCategory.hom (α.app (Opposite.op Z))) r₀' = (ConcreteCategory.hom (R.map (f.op ≫ g.op))) r
hm₀ : (ConcreteCategory.hom (φ.app (Opposite.op Y))) m₀ = (ConcreteCategory.hom (A.map f.op)) m
hm₀' : (ConcreteCategory.hom (φ.app (Opposite.op Z))) m₀' = (ConcreteCategory.hom (A.map (f.op ≫ g.op))) m
⊢ (ConcreteCategory.hom (φ.app (Opposite.op Z))) ((ConcreteCategory.hom (M₀.map g.op)) m₀) =
    (ConcreteCategory.hom (A.map g.op)) ((ConcreteCategory.hom (A.map f.op)) m)

Tactic:
← hm₀

Goal state after:
case hm₀
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
R₀ R : Cᵒᵖ ⥤ RingCat
α : R₀ ⟶ R
inst✝¹ : Presheaf.IsLocallyInjective J α
M₀ : PresheafOfModules R₀
A : Cᵒᵖ ⥤ AddCommGrpCat
φ : M₀.presheaf ⟶ A
inst✝ : Presheaf.IsLocallyInjective J φ
hA : Presheaf.IsSeparated J A
X : C
r : ↑(R.obj (Opposite.op X))
m : ↑(A.obj (Opposite.op X))
Y Z : C
f : Y ⟶ X
g : Z ⟶ Y
r₀ : ↑(R₀.obj (Opposite.op Y))
r₀' : ↑(R₀.obj (Opposite.op Z))
m₀ : ↑(M₀.obj (Opposite.op Y))
m₀' : ↑(M₀.obj (Opposite.op Z))
hr₀ : (ConcreteCategory.hom (α.app (Opposite.op Y))) r₀ = (ConcreteCategory.hom (R.map f.op)) r
hr₀' : (ConcreteCategory.hom (α.app (Opposite.op Z))) r₀' = (ConcreteCategory.hom (R.map (f.op ≫ g.op))) r
hm₀ : (ConcreteCategory.hom (φ.app (Opposite.op Y))) m₀ = (ConcreteCategory.hom (A.map f.op)) m
hm₀' : (ConcreteCategory.hom (φ.app (Opposite.op Z))) m₀' = (ConcreteCategory.hom (A.map (f.op ≫ g.op))) m
⊢ (ConcreteCategory.hom (φ.app (Opposite.op Z))) ((ConcreteCategory.hom (M₀.map g.op)) m₀) =
    (ConcreteCategory.hom (A.map g.op)) ((ConcreteCategory.hom (φ.app (Opposite.op Y))) m₀)
Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X : C
inst✝ : HasProjectiveDimensionLT X 0
this : HasExt C := ⋯
⊢ Ext.homEquiv₀.symm (𝟙 X) = Ext.homEquiv₀.symm 0

Tactic:
simpa only [Ext.homEquiv₀_symm_apply, Ext.mk₀_zero]
    using Abelian.Ext.eq_zero_of_hasProjectiveDimensionLT _ 0 (by rfl)

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

Goal state before:
pp: I : Type u_1
B : Type u_2
inst✝² : Category.{v_1, u_1} I
inst✝¹ : Bicategory B
inst✝ : Strict B
F : I ⥤ B
b₀✝ b₁✝ b₂✝ : LocallyDiscrete I
f : b₀✝ ⟶ b₁✝
g : b₁✝ ⟶ b₂✝
⊢ (match f ≫ g with
    | { as := f } => F.map f) =
    (match f with
      | { as := f } => F.map f) ≫
      match g with
      | { as := f } => F.map f

Tactic:
obtain ⟨f⟩ := f; obtain ⟨g⟩ := g; simp [CategoryStruct.comp]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
S T : C
f : S ⟶ T
⊢ (singleton f).presieve₀ = Presieve.singleton f

Tactic:
by
  simp [singleton, presieve₀, Presieve.ofArrows_pUnit]

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

Goal state before:
pp: C : Type ?u.2
D : Type ?u.4
inst✝¹ : Category.{v_1, ?u.2} C
inst✝ : Category.{v_2, ?u.4} D
J : GrothendieckTopology C
X Y : C
f : Y ⟶ X
S : Presieve X
hS : Sieve.generate S ∈ J X
⊢ ∃ T ∈ {S | Sieve.generate S ∈ J Y}, T.FactorsThruAlong S f

Tactic:
refine ⟨(Sieve.generate S).pullback f, ?_, fun Z g h => h⟩

Goal state after:
C : Type ?u.2
D : Type ?u.4
inst✝¹ : Category.{v_1, ?u.2} C
inst✝ : Category.{v_2, ?u.4} D
J : GrothendieckTopology C
X Y : C
f : Y ⟶ X
S : Presieve X
hS : Sieve.generate S ∈ J X
⊢ (Sieve.pullback f (Sieve.generate S)).arrows ∈ {S | Sieve.generate S ∈ J Y}
Module: Mathlib.CategoryTheory.Sites.CoverPreserving

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : C ⥤ D
inst✝ : RepresentablyFlat G
⊢ ∀ (ℱ : Sheaf K (Type u_1)) {Z : C} {T : Presieve Z} {x : FamilyOfElements (G.op ⋙ ℱ.obj) T},
    x.Compatible →
      ∀ {Y₁ Y₂ : C} {X : D} (f₁ : X ⟶ G.obj Y₁) (f₂ : X ⟶ G.obj Y₂) {g₁ : Y₁ ⟶ Z} {g₂ : Y₂ ⟶ Z} (hg₁ : T g₁)
        (hg₂ : T g₂),
        f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂ →
          (ConcreteCategory.hom (ℱ.obj.map f₁.op)) (x g₁ hg₁) = (ConcreteCategory.hom (ℱ.obj.map f₂.op)) (x g₂ hg₂)

Tactic:
intro ℱ Z T x hx Y₁ Y₂ X f₁ f₂ g₁ g₂ hg₁ hg₂ e

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : C ⥤ D
inst✝ : RepresentablyFlat G
ℱ : Sheaf K (Type u_1)
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.obj) T
hx : x.Compatible
Y₁ Y₂ : C
X : D
f₁ : X ⟶ G.obj Y₁
f₂ : X ⟶ G.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
e : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂
⊢ (ConcreteCategory.hom (ℱ.obj.map f₁.op)) (x g₁ hg₁) = (ConcreteCategory.hom (ℱ.obj.map f₂.op)) (x g₂ hg₂)
Module: Mathlib.CategoryTheory.Sites.CoverLifting

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
G : C ⥤ D
A : Type w
inst✝³ : Category.{w', w} A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝² : G.IsCocontinuous J K
inst✝¹ : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F
inst✝ : G.IsContinuous J K
F : Sheaf K A
⊢ (G.op.ranAdjunction A).unit.app F.obj ≫
      G.op.ran.map ((G.sheafPushforwardContinuousCompSheafToPresheafIso A J K).inv.app F) ≫
        (G.sheafPushforwardCocontinuousCompSheafToPresheafIso A J K).inv.app
          ((G.sheafPushforwardContinuous A J K).obj F) =
    (G.op.ranAdjunction A).unit.app F.obj

Tactic:
Functor.map_id

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
G : C ⥤ D
A : Type w
inst✝³ : Category.{w', w} A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝² : G.IsCocontinuous J K
inst✝¹ : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F
inst✝ : G.IsContinuous J K
F : Sheaf K A
⊢ (G.op.ranAdjunction A).unit.app F.obj ≫
      𝟙 (G.op.ran.obj (G.op ⋙ F.obj)) ≫
        (G.sheafPushforwardCocontinuousCompSheafToPresheafIso A J K).inv.app
          ((G.sheafPushforwardContinuous A J K).obj F) =
    (G.op.ranAdjunction A).unit.app F.obj
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
D : Type u_2
inst✝⁴ : Category.{v_2, u_2} D
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝² : Category.{v_4, u_4} A
G : C ⥤ D
ℱ : Dᵒᵖ ⥤ Type v
ℱ' : Sheaf K (Type v)
α✝ : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj
X Y : Dᵒᵖ
f : X ⟶ Y
⊢ ℱ.map f ≫ appHom α (unop Y) = appHom α (unop X) ≫ ℱ'.obj.map f

Tactic:
by
    ext x
    apply Functor.IsCoverDense.ext G
    intro Y' f'
    simp only [TypeCat.Fun.toFun_apply, types_comp_apply, ← map_comp_apply]
    rw [appHom_restrict, appHom_restrict]
    simp

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

Goal state before:
pp: case refine_2.refine_3
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
inst✝ : HasPullbacks C
i j : E.I₀ × F.I₀
W : C
p₁ : W ⟶ pullback (E.f i.1) (F.f i.2)
p₂ : W ⟶ pullback (E.f j.1) (F.f j.2)
w : p₁ ≫ pullback.fst (E.f i.1) (F.f i.2) ≫ E.f i.1 = p₂ ≫ pullback.fst (E.f j.1) (F.f j.2) ≫ E.f j.1
Y : C
p : W ⟶ pullback ((E.inter F).f i) ((E.inter F).f j) := pullback.lift p₁ p₂ w
Z : C
a : Y ⟶ Z
b : Z ⟶ W
k : E.I₁ i.1 j.1
e : Z ⟶ E.Y k
h₁ : b ≫ p₁ ≫ pullback.fst (E.f i.1) (F.f i.2) = e ≫ E.p₁ k
h₂ : b ≫ p₂ ≫ pullback.fst (E.f j.1) (F.f j.2) = e ≫ E.p₂ k
l : F.I₁ i.2 j.2
u : Y ⟶ F.Y l
u₁ : (a ≫ b) ≫ p₁ ≫ pullback.snd (E.f i.1) (F.f i.2) = u ≫ F.p₁ l
u₂ : (a ≫ b) ≫ p₂ ≫ pullback.snd (E.f j.1) (F.f j.2) = u ≫ F.p₂ l
x✝ :
  (Sieve.bind (E.sieve₁ (p₁ ≫ pullback.fst (E.f i.1) (F.f i.2)) (p₂ ≫ pullback.fst (E.f j.1) (F.f j.2))).arrows
        fun x f x_1 ↦
        Sieve.pullback f
          (F.sieve₁ (p₁ ≫ pullback.snd (E.f i.1) (F.f i.2)) (p₂ ≫ pullback.snd (E.f j.1) (F.f j.2)))).arrows
    (a ≫ b)
⊢ (a ≫ b) ≫ p₂ = pullback.lift (a ≫ e) u ⋯ ≫ (E.inter F).p₂ (k, l)

Tactic:
· apply pullback.hom_ext
      · simp [h₂]
      · simpa using u₂

Goal state after:
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
D : Type u_2
inst✝³ : Category.{v_2, u_2} D
G : C ⥤ D
K : GrothendieckTopology D
inst✝² : G.LocallyCoverDense K
inst✝¹ : G.Full
inst✝ : G.Faithful
X : C
S : Sieve X
⊢ Sieve.functorPushforward G S ∈ K (G.obj X) ↔ ∃ T, Sieve.functorPullback G ↑T = S

Tactic:
constructor
  · intro hS
    exact ⟨⟨_, hS⟩, (Sieve.fullyFaithfulFunctorGaloisCoinsertion G X).u_l_eq S⟩
  · rintro ⟨T, rfl⟩
    exact LocallyCoverDense.functorPushforward_functorPullback_mem T

Goal state after:
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
X : Cᵒᵖ
r : ↑(S.obj.obj X)
⊢ (forget₂ RingCat AddCommGrpCat).map (φ.hom.app X) ≫ (((pushforward φ).obj (unit R)).val.obj X).smul r =
    ((unit S).val.obj X).smul r ≫ (forget₂ RingCat AddCommGrpCat).map (φ.hom.app X)

Tactic:
by
    ext m
    exact ((φ.hom.app X).hom.map_mul _ _).symm

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

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
inst✝² : (PresheafOfModules.pushforward φ.hom).IsRightAdjoint
inst✝¹ : HasWeakSheafify K AddCommGrpCat
inst✝ : K.WEqualsLocallyBijective AddCommGrpCat
X'✝ X✝ : SheafOfModules S
Y✝ : SheafOfModules R
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (pushforward φ).obj Y✝
⊢ ((PresheafOfModules.sheafificationAdjunction (𝟙 R.obj)).homEquiv ((PresheafOfModules.pullback φ.hom).obj X'✝.val)
          Y✝).symm
      (((PresheafOfModules.pullbackPushforwardAdjunction φ.hom).homEquiv X'✝.val Y✝.val).symm (f✝.val ≫ g✝.val)) =
    (PresheafOfModules.sheafification (𝟙 R.obj)).map ((PresheafOfModules.pullback φ.hom).map f✝.val) ≫
      ((PresheafOfModules.sheafificationAdjunction (𝟙 R.obj)).homEquiv ((PresheafOfModules.pullback φ.hom).obj X✝.val)
            Y✝).symm
        (((PresheafOfModules.pullbackPushforwardAdjunction φ.hom).homEquiv X✝.val Y✝.val).symm g✝.val)

Tactic:
erw [Adjunction.homEquiv_naturality_left_symm,
          Adjunction.homEquiv_naturality_left_symm]

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
inst✝² : (PresheafOfModules.pushforward φ.hom).IsRightAdjoint
inst✝¹ : HasWeakSheafify K AddCommGrpCat
inst✝ : K.WEqualsLocallyBijective AddCommGrpCat
X'✝ X✝ : SheafOfModules S
Y✝ : SheafOfModules R
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (pushforward φ).obj Y✝
⊢ (PresheafOfModules.sheafification (𝟙 R.obj)).map ((PresheafOfModules.pullback φ.hom).map (f✝.val ≫ g✝.val)) ≫
      ((PresheafOfModules.sheafificationAdjunction (𝟙 R.obj)).homEquiv
            ((PresheafOfModules.pullback φ.hom).obj ((PresheafOfModules.pushforward φ.hom).obj Y✝.val)) Y✝).symm
        ((PresheafOfModules.pullbackPushforwardAdjunction φ.hom).counit.app Y✝.val) =
    (PresheafOfModules.sheafification (𝟙 R.obj)).map ((PresheafOfModules.pullback φ.hom).map f✝.val) ≫
      (PresheafOfModules.sheafification (𝟙 R.obj)).map ((PresheafOfModules.pullback φ.hom).map g✝.val) ≫
        ((PresheafOfModules.sheafificationAdjunction (𝟙 R.obj)).homEquiv
              ((PresheafOfModules.pullback φ.hom).obj ((PresheafOfModules.pushforward φ.hom).obj Y✝.val)) Y✝).symm
          ((PresheafOfModules.pullbackPushforwardAdjunction φ.hom).counit.app Y✝.val)
Module: Mathlib.CategoryTheory.Limits.Lattice

Goal state before:
pp: α : Type u
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
ι : Type u
inst✝ : Fintype ι
f : ι → α
⊢ ∐ f = ?m.15

pp: α : Type u
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
ι : Type u
inst✝ : Fintype ι
f : ι → α
⊢ ?m.15 = Finset.univ.sup f

pp: α : Type u
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
ι : Type u
inst✝ : Fintype ι
f : ι → α
⊢ α

Tactic:
· exact
      (IsColimit.coconePointUniqueUpToIso (colimit.isColimit _)
          (finiteColimitCocone (Discrete.functor f)).isColimit).to_eq

Goal state after:
α : Type u
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
ι : Type u
inst✝ : Fintype ι
f : ι → α
⊢ (finiteColimitCocone (Discrete.functor f)).cocone.pt = Finset.univ.sup f
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:
rw [finite_limit_eq_finset_univ_inf (pair.{u} x y)]

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

Goal state before:
pp: case refine_1
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
inst✝² : F.IsCocontinuous J K
inst✝¹ : IsIso φ
inst✝ : F.IsLeftAdjoint
adj : F ⊣ F.rightAdjoint := Adjunction.ofIsLeftAdjoint F
shAdj : F.sheafPushforwardContinuous RingCat J K ⊣ F.rightAdjoint.sheafPushforwardContinuous RingCat K J :=
  adj.sheafPushforwardContinuous J K
ψ : R ⟶ (F.rightAdjoint.sheafPushforwardContinuous RingCat K J).obj S :=
  shAdj.unit.app R ≫ (F.rightAdjoint.sheafPushforwardContinuous RingCat K J).map (CategoryTheory.inv φ)
⊢ whiskerRight (NatTrans.op adj.counit) R.obj = ψ.hom ≫ F.rightAdjoint.op.whiskerLeft φ.hom

Tactic:
ext U : 2

Goal state after:
case refine_1
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
inst✝² : F.IsCocontinuous J K
inst✝¹ : IsIso φ
inst✝ : F.IsLeftAdjoint
adj : F ⊣ F.rightAdjoint := Adjunction.ofIsLeftAdjoint F
shAdj : F.sheafPushforwardContinuous RingCat J K ⊣ F.rightAdjoint.sheafPushforwardContinuous RingCat K J :=
  adj.sheafPushforwardContinuous J K
ψ : R ⟶ (F.rightAdjoint.sheafPushforwardContinuous RingCat K J).obj S :=
  shAdj.unit.app R ≫ (F.rightAdjoint.sheafPushforwardContinuous RingCat K J).map (CategoryTheory.inv φ)
U : Dᵒᵖ
⊢ (whiskerRight (NatTrans.op adj.counit) R.obj).app U = (ψ.hom ≫ F.rightAdjoint.op.whiskerLeft φ.hom).app U
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous

Goal state before:
pp: case refine_2
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
inst✝² : F.IsCocontinuous J K
inst✝¹ : IsIso φ
inst✝ : F.IsLeftAdjoint
adj : F ⊣ F.rightAdjoint := Adjunction.ofIsLeftAdjoint F
shAdj : F.sheafPushforwardContinuous RingCat J K ⊣ F.rightAdjoint.sheafPushforwardContinuous RingCat K J :=
  adj.sheafPushforwardContinuous J K
ψ : R ⟶ (F.rightAdjoint.sheafPushforwardContinuous RingCat K J).obj S :=
  shAdj.unit.app R ≫ (F.rightAdjoint.sheafPushforwardContinuous RingCat K J).map (CategoryTheory.inv φ)
⊢ φ.hom ≫ F.op.whiskerLeft ψ.hom ≫ whiskerRight (NatTrans.op adj.unit) S.obj = 𝟙 S.obj

Tactic:
ext U : 2

Goal state after:
case refine_2
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
inst✝² : F.IsCocontinuous J K
inst✝¹ : IsIso φ
inst✝ : F.IsLeftAdjoint
adj : F ⊣ F.rightAdjoint := Adjunction.ofIsLeftAdjoint F
shAdj : F.sheafPushforwardContinuous RingCat J K ⊣ F.rightAdjoint.sheafPushforwardContinuous RingCat K J :=
  adj.sheafPushforwardContinuous J K
ψ : R ⟶ (F.rightAdjoint.sheafPushforwardContinuous RingCat K J).obj S :=
  shAdj.unit.app R ≫ (F.rightAdjoint.sheafPushforwardContinuous RingCat K J).map (CategoryTheory.inv φ)
U : Cᵒᵖ
⊢ (φ.hom ≫ F.op.whiskerLeft ψ.hom ≫ whiskerRight (NatTrans.op adj.unit) S.obj).app U = (𝟙 S.obj).app U
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
⊢ ((pullback C f).map u ≫ (hf.pullbackObjIso 𝒢).hom).app (op U) =
    ((hf.pullbackObjIso ℱ).hom ≫ hf.functor.op.whiskerLeft u).app (op U)

Tactic:
dsimp [pullbackObjIso, pullbackObjObjOfImageOpen]

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
⊢ ((pullback C f).map u).app (op U) ≫
      (Limits.IsColimit.coconePointUniqueUpToIso
          ((Opens.map f).op.isPointwiseLeftKanExtensionLeftKanExtensionUnit 𝒢 (op U))
          (Limits.colimitOfDiagramTerminal
            { lift := fun s ↦ CostructuredArrow.homMk (homOfLE ⋯).op ⋯, fac := ⋯, uniq := ⋯ }
            (CostructuredArrow.proj (Opens.map f).op (op U) ⋙ 𝒢))).hom =
    (Limits.IsColimit.coconePointUniqueUpToIso
          ((Opens.map f).op.isPointwiseLeftKanExtensionLeftKanExtensionUnit ℱ (op U))
          (Limits.colimitOfDiagramTerminal
            { lift := fun s ↦ CostructuredArrow.homMk (homOfLE ⋯).op ⋯, fac := ⋯, uniq := ⋯ }
            (CostructuredArrow.proj (Opens.map f).op (op U) ⋙ ℱ))).hom ≫
      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
R : Presieve Y
hR : Sieve.generate R ∈ (Opens.grothendieckTopology ↑X) Y
⊢ IsLimit (Functor.mapCone F (opensLeCoverCocone (coveringOfPresieve Y R)).op) ≃
    IsLimit (Functor.mapCone F (Sieve.generate R).arrows.cocone.op)

Tactic:
convert!
    isLimitOpensLeEquivGenerate₁ F (coveringOfPresieve Y R)
      (coveringOfPresieve.iSup_eq_of_mem_grothendieck Y R hR).symm using 1

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
R : Presieve Y
hR : Sieve.generate R ∈ (Opens.grothendieckTopology ↑X) Y
⊢ IsLimit (Functor.mapCone F (Sieve.generate R).arrows.cocone.op) =
    IsLimit (Functor.mapCone F (Sieve.generate (presieveOfCoveringAux (coveringOfPresieve Y R) Y)).arrows.cocone.op)
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
⊢ F.IsSheaf ↔ F.IsSheafOpensLeCover

Tactic:
refine ⟨fun h _ ↦ h.isSheafOpensLeCover,
    fun h ↦ (Presheaf.isSheaf_iff_isLimit _ _).mpr fun Y S ↦ ?_⟩
  rw [← Sieve.generate_sieve S]
  intro hS
  rw [← (isLimitOpensLeEquivGenerate₂ F S.1 hS).nonempty_congr]
  apply h

Goal state after: