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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
S✝ T✝ : C
E✝ : PreZeroHypercover S✝
F : PreZeroHypercover S✝
S T : C
f : S ⟶ T
E : PreZeroHypercover T
inst✝¹ : ∀ (i : E.I₀), HasPullback f (E.f i)
inst✝ : ∀ (i : E.I₀), HasPullback (E.f i) f
⊢ { s₀ := id, h₀ := fun i ↦ (pullbackSymmetry f (E.f i)).inv, w₀ := ⋯ } ≫
      { s₀ := id, h₀ := fun i ↦ (pullbackSymmetry f (E.f i)).hom, w₀ := ⋯ } =
    𝟙 (pullback₂ f E)

Tactic:
apply Hom.ext (by rfl)

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
S✝ T✝ : C
E✝ : PreZeroHypercover S✝
F : PreZeroHypercover S✝
S T : C
f : S ⟶ T
E : PreZeroHypercover T
inst✝¹ : ∀ (i : E.I₀), HasPullback f (E.f i)
inst✝ : ∀ (i : E.I₀), HasPullback (E.f i) f
⊢ ({ s₀ := id, h₀ := fun i ↦ (pullbackSymmetry f (E.f i)).inv, w₀ := ⋯ } ≫
        { s₀ := id, h₀ := fun i ↦ (pullbackSymmetry f (E.f i)).hom, w₀ := ⋯ }).h₀ ≍
    (𝟙 (pullback₂ f E)).h₀
Module: Mathlib.CategoryTheory.Functor.Flat

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Category.{v_3, u_3} E
F : C ⥤ D
G : D ⥤ E
X : E
inst✝ : RepresentablyCoflat F
h : IsFiltered (CostructuredArrow G X)
⊢ IsFiltered (CostructuredArrow (F ⋙ G) X)

Tactic:
rw [← isCofiltered_op_iff_isFiltered, IsCofiltered.iff_of_equivalence
    (costructuredArrowOpEquivalence _ _)] at h ⊢

Goal state after:
C : Type u_1
D : Type u_2
E : Type u_3
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Category.{v_3, u_3} E
F : C ⥤ D
G : D ⥤ E
X : E
inst✝ : RepresentablyCoflat F
h : IsCofiltered (StructuredArrow (op X) G.op)
⊢ IsCofiltered (StructuredArrow (op X) (F ⋙ G).op)
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J K : Precoverage C
h : ∀ ⦃X : C⦄ ⦃E : J.ZeroHypercover X⦄, E.presieve₀ ∈ K.coverings X
X : C
⊢ J.coverings X ⊆ K.coverings X

Tactic:
R

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J K : Precoverage C
h : ∀ ⦃X : C⦄ ⦃E : J.ZeroHypercover X⦄, E.presieve₀ ∈ K.coverings X
X : C
R : Presieve X
⊢ R ∈ J.coverings X → R ∈ K.coverings X
Module: Mathlib.CategoryTheory.Sites.Coverage

Goal state before:
pp: C : Type u_2
inst✝ : Category.{v_1, u_2} C
K L : Coverage C
P : Cᵒᵖ ⥤ Type u_1
h : (∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R) ∧ ∀ {X : C}, ∀ R ∈ L.coverings X, IsSheafFor P R
X : C
⊢ ∀ R ∈ (K ⊔ L).coverings X, IsSheafFor P R

Tactic:
R

Goal state after:
C : Type u_2
inst✝ : Category.{v_1, u_2} C
K L : Coverage C
P : Cᵒᵖ ⥤ Type u_1
h : (∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R) ∧ ∀ {X : C}, ∀ R ∈ L.coverings X, IsSheafFor P R
X : C
R : Presieve X
⊢ R ∈ (K ⊔ L).coverings X → IsSheafFor P R
Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck

Goal state before:
pp: C : Type u_3
inst✝ : Category.{u_2, u_3} C
J : Precoverage C
P : Cᵒᵖ ⥤ Type u_1
h : IsSheaf J.toGrothendieck P
S : C
R : Presieve S
hR : R ∈ J.coverings S
⊢ IsSheafFor P R

Tactic:
rw [J.isSheaf_toGrothendieck_iff] at h
  simpa [Presieve.isSheafFor_iff_generate] using h (f := 𝟙 S) R hR

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

Goal state before:
pp: case refine_2
C : Type u_2
inst✝ : Category.{u_3, u_2} C
K : Precoverage C
J : GrothendieckTopology C
h : K ≤ J.toPrecoverage
X : C
⊢ K.toGrothendieck X ⊆ J X

Tactic:
R

Goal state after:
case refine_2
C : Type u_2
inst✝ : Category.{u_3, u_2} C
K : Precoverage C
J : GrothendieckTopology C
h : K ≤ J.toPrecoverage
X : C
R : Sieve X
⊢ R ∈ K.toGrothendieck X → R ∈ J X
Module: Mathlib.CategoryTheory.Sites.Continuous

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
F : C ⥤ D
J : Precoverage C
K : Precoverage D
inst✝⁴ : J.IsStableUnderBaseChange
inst✝³ : J.HasPullbacks
inst✝² : K.IsStableUnderBaseChange
inst✝¹ : K.HasPullbacks
inst✝ : J.PullbacksPreservedBy F
h : J ≤ Precoverage.comap F K
x✝ : Sheaf K.toGrothendieck (Type (max u₁ v₁ u₂ v₂))
G : Dᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)
H✝ : Presheaf.IsSheaf K.toGrothendieck G
H : ∀ {X : D}, ∀ R ∈ K.toCoverage.coverings X, Presieve.IsSheafFor G R
X : C
⊢ ∀ R ∈ J.toCoverage.coverings X, Presieve.IsSheafFor (F.op ⋙ { obj := G, property := H✝ }.obj) R

Tactic:
R

Goal state after:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
F : C ⥤ D
J : Precoverage C
K : Precoverage D
inst✝⁴ : J.IsStableUnderBaseChange
inst✝³ : J.HasPullbacks
inst✝² : K.IsStableUnderBaseChange
inst✝¹ : K.HasPullbacks
inst✝ : J.PullbacksPreservedBy F
h : J ≤ Precoverage.comap F K
x✝ : Sheaf K.toGrothendieck (Type (max u₁ v₁ u₂ v₂))
G : Dᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)
H✝ : Presheaf.IsSheaf K.toGrothendieck G
H : ∀ {X : D}, ∀ R ∈ K.toCoverage.coverings X, Presieve.IsSheafFor G R
X : C
R : Presieve X
⊢ R ∈ J.toCoverage.coverings X → Presieve.IsSheafFor (F.op ⋙ { obj := G, property := H✝ }.obj) R
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
i₁ i₂ : E.I₀
inst✝ : HasPullback (E.f i₁) (E.f i₂)
k : E.I₁ i₁ i₂
⊢ E.toPullback k ≫ pullback.fst (E.f i₁) (E.f i₂) = E.p₁ k

Tactic:
pullback.lift_fst

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
i₁ i₂ : E.I₀
inst✝ : HasPullback (E.f i₁) (E.f i₂)
k : E.I₁ i₁ i₂
⊢ E.p₁ k = E.p₁ k
Module: Mathlib.CategoryTheory.Sites.CoverPreserving

Goal state before:
pp: case hunique
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
hF₁ : CompatiblePreserving K F
hF₂ : CoverPreserving J K F
G : Sheaf K (Type (max u₁ v₁ u₂ v₂))
X : C
S : Sieve X
hS : S ∈ J X
x : FamilyOfElements (F.op ⋙ G.obj) S.arrows
hx : x.Compatible
y₁ y₂ : (F.op ⋙ G.obj).obj (op X)
hy₁ : x.IsAmalgamation y₁
hy₂ : x.IsAmalgamation y₂
Y : D
Z : C
g : Z ⟶ X
h : Y ⟶ F.obj Z
hg : S.arrows g
⊢ (ConcreteCategory.hom (G.obj.map (h ≫ F.map g).op)) y₁ = (ConcreteCategory.hom (G.obj.map (h ≫ F.map g).op)) y₂

Tactic:
simpa using! congrArg _ ((hy₁ g hg).trans (hy₂ g hg).symm)

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

Goal state before:
pp: case hx
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
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj
X Y : Aᵒᵖ
f : X ⟶ Y
U : Dᵒᵖ
x : ((coyoneda ⋙ (whiskeringLeft Dᵒᵖ A (Type v_4)).obj ℱ).obj X).obj U
⊢ (pushforwardFamily (homOver α (unop Y)) (f.unop ≫ x)).Compatible

pp: case h
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
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj
X Y : Aᵒᵖ
f : X ⟶ Y
U : Dᵒᵖ
x : ((coyoneda ⋙ (whiskeringLeft Dᵒᵖ A (Type v_4)).obj ℱ).obj X).obj U
⊢ (pushforwardFamily (homOver α (unop Y)) (f.unop ≫ x)).IsAmalgamation
    (f.unop ≫ (ConcreteCategory.hom (appHom (homOver α (unop X)) (unop U))) x)

Tactic:
· exact pushforwardFamily_compatible (homOver α Y.unop) (f.unop ≫ x)

Goal state after:
case h
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
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj
X Y : Aᵒᵖ
f : X ⟶ Y
U : Dᵒᵖ
x : ((coyoneda ⋙ (whiskeringLeft Dᵒᵖ A (Type v_4)).obj ℱ).obj X).obj U
⊢ (pushforwardFamily (homOver α (unop Y)) (f.unop ≫ x)).IsAmalgamation
    (f.unop ≫ (ConcreteCategory.hom (appHom (homOver α (unop X)) (unop U))) x)
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: case h₁
C : Type u
inst✝³ : Category.{v, u} C
A : Type u_1
inst✝² : Category.{v_1, u_1} A
S : C
E : PreOneHypercover S
F : PreOneHypercover S
G✝ : PreOneHypercover S
inst✝¹ : ∀ (i : E.I₀) (j : F.I₀), HasPullback (E.f i) (F.f j)
inst✝ : ∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b), HasPullback (E.p₁ k ≫ E.f i) (F.p₁ l ≫ F.f a)
G : PreOneHypercover S
f : G.Hom E
g : G.Hom F
i✝ j✝ : G.I₀
k : G.I₁ i✝ j✝
⊢ (pullback.lift (f.h₁ k) (g.h₁ k) ⋯ ≫ (E.inter F).p₂ (f.s₁ k, g.s₁ k)) ≫
      pullback.snd
        (E.f
          ((Equiv.sigmaEquivProd E.I₀ F.toPreZeroHypercover.1).symm
              ((PreZeroHypercover.interLift f.toHom g.toHom).s₀ j✝)).fst)
        (F.f
          ((Equiv.sigmaEquivProd E.I₀ F.toPreZeroHypercover.1).symm
              ((PreZeroHypercover.interLift f.toHom g.toHom).s₀ j✝)).snd) =
    (G.p₂ k ≫ (PreZeroHypercover.interLift f.toHom g.toHom).h₀ j✝) ≫
      pullback.snd
        (E.f
          ((Equiv.sigmaEquivProd E.I₀ F.toPreZeroHypercover.1).symm
              ((PreZeroHypercover.interLift f.toHom g.toHom).s₀ j✝)).fst)
        (F.f
          ((Equiv.sigmaEquivProd E.I₀ F.toPreZeroHypercover.1).symm
              ((PreZeroHypercover.interLift f.toHom g.toHom).s₀ j✝)).snd)

Tactic:
· simpa using g.w₁₂ k

Goal state after:
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
U : Over X
S : Sieve U
hS : S ∈ (J.over X) U
⊢ Sieve.functorPushforward (Over.map f) S ∈ (J.over Y) ((Over.map f).obj U)

Tactic:
obtain ⟨S, rfl⟩ := (Sieve.overEquiv U).symm.surjective S

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X Y : C
f : X ⟶ Y
U : Over X
S : Sieve U.left
hS : (Sieve.overEquiv U).symm S ∈ (J.over X) U
⊢ Sieve.functorPushforward (Over.map f) ((Sieve.overEquiv U).symm S) ∈ (J.over Y) ((Over.map f).obj U)
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
K : Precoverage C
inst✝¹ : K.HasPullbacks
inst✝ : K.IsStableUnderBaseChange
X Y : C
right : Discrete PUnit.{1}
s : Y ⟶ X
⊢ (K.toGrothendieck.over X) { left := Y, right := right, hom := s } ⊆
    (Precoverage.comap (Over.forget X) K).toGrothendieck { left := Y, right := right, hom := s }

Tactic:
R

Goal state after:
case refine_1
C : Type u
inst✝² : Category.{v, u} C
K : Precoverage C
inst✝¹ : K.HasPullbacks
inst✝ : K.IsStableUnderBaseChange
X Y : C
right : Discrete PUnit.{1}
s : Y ⟶ X
R : Sieve { left := Y, right := right, hom := s }
⊢ R ∈ (K.toGrothendieck.over X) { left := Y, right := right, hom := s } →
    R ∈ (Precoverage.comap (Over.forget X) K).toGrothendieck { left := Y, right := right, hom := s }
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
K : Precoverage C
inst✝¹ : K.HasPullbacks
inst✝ : K.IsStableUnderBaseChange
X : C
Y : Over X
⊢ (Precoverage.comap (Over.forget X) K).coverings Y ⊆ (K.toGrothendieck.over X).toPrecoverage.coverings Y

Tactic:
R

Goal state after:
case refine_2
C : Type u
inst✝² : Category.{v, u} C
K : Precoverage C
inst✝¹ : K.HasPullbacks
inst✝ : K.IsStableUnderBaseChange
X : C
Y : Over X
R : Presieve Y
⊢ R ∈ (Precoverage.comap (Over.forget X) K).coverings Y → R ∈ (K.toGrothendieck.over X).toPrecoverage.coverings Y
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X : C
inst✝ : Simple X
⊢ ¬IsZero X

Tactic:
simpa [Limits.IsZero.iff_id_eq_zero] using id_nonzero X

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

Goal state before:
pp: case a
T : Type u
inst✝ : TopologicalSpace T
X : Opens T
⊢ (grothendieckTopology T).toPretopology.coverings X ⊆ (pretopology T).coverings X

Tactic:
R

Goal state after:
case a
T : Type u
inst✝ : TopologicalSpace T
X : Opens T
R : Presieve X
⊢ R ∈ (grothendieckTopology T).toPretopology.coverings X → R ∈ (pretopology T).coverings X
Module: Mathlib.CategoryTheory.Sites.Spaces

Goal state before:
pp: case a
T : Type u
inst✝ : TopologicalSpace T
X : Opens T
⊢ (pretopology T).coverings X ⊆ (grothendieckTopology T).toPretopology.coverings X

Tactic:
R

Goal state after:
case a
T : Type u
inst✝ : TopologicalSpace T
X : Opens T
R : Presieve X
⊢ R ∈ (pretopology T).coverings X → R ∈ (grothendieckTopology T).toPretopology.coverings 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✝
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
G : D ⥤ C
S : Sheaf J RingCat
R : Sheaf K RingCat
inst✝¹ : F.IsContinuous J K
inst✝ : G.IsContinuous K J
adj : F ⊣ G
φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R
ψ : R ⟶ (G.sheafPushforwardContinuous RingCat K J).obj S
H₁ : whiskerRight (NatTrans.op adj.counit) R.obj = ψ.hom ≫ G.op.whiskerLeft φ.hom
H₂ : φ.hom ≫ F.op.whiskerLeft ψ.hom ≫ whiskerRight (NatTrans.op adj.unit) S.obj = 𝟙 S.obj
this : (G ⋙ F).IsContinuous K K := isContinuous_comp G F K J K
⊢ 𝟙 (((𝟭 D).sheafPushforwardContinuous RingCat K K).obj R) ≫
      (sheafPushforwardContinuousNatTrans adj.counit RingCat K K).app R =
    ψ ≫ (G.sheafPushforwardContinuous RingCat K J).map φ

Tactic:
by ext1; simpa

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

Tactic:
by ext1; simpa

Goal state after:
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
C : Type u'
inst✝¹ : Category.{v', u'} C
inst✝ : HasBinaryProducts C
J : GrothendieckTopology C
R : Sheaf J RingCat
x : C
⊢ (𝟙 (R.over x)).hom ≫
      (Over.forget x).op.whiskerLeft (pushforwardOver x).hom ≫
        whiskerRight (NatTrans.op (Over.forgetAdjStar x).unit) (R.over x).obj =
    𝟙 (R.over x).obj

Tactic:
ext y : 2
    simp [pushforwardOver, ← Functor.map_comp, ← op_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Category.Pairwise

Goal state before:
pp: ι : Type v
α : Type u
U : ι → α
inst✝ : CompleteLattice α
s : Cocone (diagram U)
⊢ (cocone U).pt ≤ s.pt

Tactic:
by
      apply sSup_le
      rintro _ ⟨j, rfl⟩
      exact (s.ι.app (single j)).le

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
eqv : C ≌ D
S : Sheaf J RingCat
R : Sheaf K RingCat
inst✝¹ : eqv.functor.IsContinuous J K
inst✝ : eqv.inverse.IsContinuous K J
φ : S ⟶ (eqv.functor.sheafPushforwardContinuous RingCat J K).obj R
ψ : R ⟶ (eqv.inverse.sheafPushforwardContinuous RingCat K J).obj S
H₁ : whiskerRight (NatTrans.op eqv.counit) R.obj = ψ.hom ≫ eqv.inverse.op.whiskerLeft φ.hom
H₂ : φ.hom ≫ eqv.functor.op.whiskerLeft ψ.hom ≫ whiskerRight (NatTrans.op eqv.unit) S.obj = 𝟙 S.obj
this : (eqv.inverse ⋙ eqv.functor).IsContinuous K K := isContinuous_comp eqv.inverse eqv.functor K J K
⊢ 𝟙 R ≫ (sheafPushforwardContinuousNatTrans eqv.counitIso.hom RingCat K K).app R =
    ψ ≫ (eqv.inverse.sheafPushforwardContinuous RingCat K J).map φ

Tactic:
by ext1; simpa

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
eqv : C ≌ D
S : Sheaf J RingCat
R : Sheaf K RingCat
inst✝¹ : eqv.functor.IsContinuous J K
inst✝ : eqv.inverse.IsContinuous K J
φ : S ⟶ (eqv.functor.sheafPushforwardContinuous RingCat J K).obj R
ψ : R ⟶ (eqv.inverse.sheafPushforwardContinuous RingCat K J).obj S
H₁ : whiskerRight (NatTrans.op eqv.counit) R.obj = ψ.hom ≫ eqv.inverse.op.whiskerLeft φ.hom
H₂ : φ.hom ≫ eqv.functor.op.whiskerLeft ψ.hom ≫ whiskerRight (NatTrans.op eqv.unit) S.obj = 𝟙 S.obj
this : (eqv.functor ⋙ eqv.inverse).IsContinuous J J := isContinuous_comp eqv.functor eqv.inverse J K J
⊢ (φ ≫ (eqv.functor.sheafPushforwardContinuous RingCat J K).map ψ) ≫
      (sheafPushforwardContinuousNatTrans eqv.unitIso.hom RingCat J J).app S =
    𝟙 S

Tactic:
by ext1; simpa

Goal state after:
Module: Mathlib.Topology.Sheaves.SheafCondition.Sites

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
F : TopCat.Presheaf C Y
⊢ RepresentablyFlat (Opens.map f)

Tactic:
by
  constructor
  intro U
  refine @IsCofiltered.mk _ _ ?_ ?_
  · constructor
    · intro V W
      exact ⟨⟨⟨PUnit.unit⟩, V.right ⊓ W.right, homOfLE <| le_inf V.hom.le W.hom.le⟩,
        StructuredArrow.homMk (homOfLE inf_le_left),
        StructuredArrow.homMk (homOfLE inf_le_right), trivial⟩
    · exact fun _ _ _ _ ↦ ⟨_, 𝟙 _, by simp [eq_iff_true_of_subsingleton]⟩
  · exact ⟨StructuredArrow.mk <| show U ⟶ (Opens.map f).obj ⊤ from homOfLE le_top⟩

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Ulift

Goal state before:
pp: R : Type u
inst✝ : Ring R
⊢ Limits.PreservesFiniteColimits (uliftFunctor.{v', v, u} R)

Tactic:
have := ((CategoryTheory.Functor.exact_tfae (uliftFunctor.{v', v} R)).out 1 3).mp
    (uliftFunctor_map_exact R)

Goal state after:
R : Type u
inst✝ : Ring R
this :
  Limits.PreservesFiniteLimits (uliftFunctor.{v', v, u} R) ∧ Limits.PreservesFiniteColimits (uliftFunctor.{v', v, u} R)
⊢ Limits.PreservesFiniteColimits (uliftFunctor.{v', v, u} R)
Module: Mathlib.Algebra.Category.MonCat.Colimits

Goal state before:
pp: case h.mul
J : Type v
inst✝ : Category.{u, v} J
F : J ⥤ MonCat
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), (colimitCocone F).ι.app j ≫ m = s.ι.app j
x y : Prequotient F
hx : (Hom.hom m) (Quot.mk (⇑(colimitSetoid F)) x) = (Hom.hom (descMorphism F s)) (Quot.mk (⇑(colimitSetoid F)) x)
hy : (Hom.hom m) (Quot.mk (⇑(colimitSetoid F)) y) = (Hom.hom (descMorphism F s)) (Quot.mk (⇑(colimitSetoid F)) y)
⊢ (Hom.hom m) (Quot.mk (⇑(colimitSetoid F)) (x.mul y)) =
    (Hom.hom (descMorphism F s)) (Quot.mk (⇑(colimitSetoid F)) (x.mul y))

Tactic:
rw [quot_mul, map_mul, hx, hy]

Goal state after:
case h.mul
J : Type v
inst✝ : Category.{u, v} J
F : J ⥤ MonCat
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), (colimitCocone F).ι.app j ≫ m = s.ι.app j
x y : Prequotient F
hx : (Hom.hom m) (Quot.mk (⇑(colimitSetoid F)) x) = (Hom.hom (descMorphism F s)) (Quot.mk (⇑(colimitSetoid F)) x)
hy : (Hom.hom m) (Quot.mk (⇑(colimitSetoid F)) y) = (Hom.hom (descMorphism F s)) (Quot.mk (⇑(colimitSetoid F)) y)
⊢ (Hom.hom (descMorphism F s)) (Quot.mk (⇑(colimitSetoid F)) x) *
      (Hom.hom (descMorphism F s)) (Quot.mk (⇑(colimitSetoid F)) y) =
    (Hom.hom (descMorphism F s)) (Quot.mk (⇑(colimitSetoid F)) x * Quot.mk (⇑(colimitSetoid F)) y)
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: R₁ : Type u_1
R₂ : Type u_2
inst✝⁹ : Semiring R₁
inst✝⁸ : Semiring R₂
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst✝⁷ : RingHomInvPair σ₁₂ σ₂₁
inst✝⁶ : RingHomInvPair σ₂₁ σ₁₂
M₁ : Type u_4
inst✝⁵ : TopologicalSpace M₁
inst✝⁴ : AddCommMonoid M₁
M₂ : Type u_5
inst✝³ : TopologicalSpace M₂
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R₁ M₁
inst✝ : Module R₂ M₂
e : M₁ ≃SL[σ₁₂] M₂
s : Set M₂
⊢ ⇑e.symm '' s = ⇑e ⁻¹' s

Tactic:
rw [e.symm.image_eq_preimage_symm, e.symm_symm]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer

Goal state before:
pp: J : MulticospanShape
inst✝³ : Fintype J.L
inst✝² : Fintype J.R
inst✝¹ : DecidableEq J.L
inst✝ : DecidableEq J.R
a : J.L
b : J.R
h₁ : J.fst b = a
h₂ : J.snd b = a
f : (left a ⟶ right b) → Prop :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ f (eqToHom ⋯ ≫ Hom.fst b) = ?m.537

Tactic:
subst h₁

Goal state after:
J : MulticospanShape
inst✝³ : Fintype J.L
inst✝² : Fintype J.R
inst✝¹ : DecidableEq J.L
inst✝ : DecidableEq J.R
b : J.R
h₂ : J.snd b = J.fst b
f : (left (J.fst b) ⟶ right b) → Prop :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ f (eqToHom ⋯ ≫ Hom.fst b) = ?m.540 (J.fst b) ⋯ h₂
Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer

Goal state before:
pp: J : MultispanShape
inst✝³ : Fintype J.L
inst✝² : Fintype J.R
inst✝¹ : DecidableEq J.L
inst✝ : DecidableEq J.R
a : J.L
b : J.R
h₁ : J.fst a = b
h₂ : J.snd a = b
f : (left a ⟶ right b) → Prop :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ f (Hom.fst a ≫ eqToHom ⋯) = ?m.529

Tactic:
subst h₁

Goal state after:
J : MultispanShape
inst✝³ : Fintype J.L
inst✝² : Fintype J.R
inst✝¹ : DecidableEq J.L
inst✝ : DecidableEq J.R
a : J.L
h₂ : J.snd a = J.fst a
f : (left a ⟶ right (J.fst a)) → Prop :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ f (Hom.fst a ≫ eqToHom ⋯) = ?m.532 (J.fst a) ⋯ h₂