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

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
M N P : SheafOfModules R
σ : M.GeneratingSections
p : M ⟶ N
inst✝ : Epi p
⊢ Epi (N.freeHomEquiv.symm fun i ↦ sectionsMap p (σ.s i))

Tactic:
by
    rw [← freeHomEquiv_symm_comp]
    apply epi_comp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
A : Type u_1
inst✝¹ : Category.{v_1, u_1} A
J : Precoverage C
S : C
E : J.ZeroHypercover S
inst✝ : E.HasPullbacks
⊢ ∀ (i₁ i₂ : E.toPreOneHypercover.I₀),
    E.toPreOneHypercover.sieve₁' i₁ i₂ ∈
      J.toGrothendieck (pullback (E.toPreOneHypercover.f i₁) (E.toPreOneHypercover.f i₂))

Tactic:
simp

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

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
M✝¹ N P : SheafOfModules R
C' : Type u₁
inst✝⁶ : Category.{v₁, u₁} C'
J' : GrothendieckTopology C'
S : Sheaf J' RingCat
inst✝⁵ : HasSheafify J' AddCommGrpCat
inst✝⁴ : J'.WEqualsLocallyBijective AddCommGrpCat
M✝ : SheafOfModules R
G✝ : M✝.GeneratingSections
F : SheafOfModules R ⥤ SheafOfModules S
inst✝³ : PreservesColimitsOfSize.{u, u, max u u', max u u₁, max (max (u + 1) u') v', max (max (u + 1) u₁) v₁} F
η : unit S ≅ F.obj (unit R)
inst✝² : ∀ (X : C), HasSheafify (J.over X) AddCommGrpCat
inst✝¹ : HasBinaryProducts C
inst✝ : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat
M : SheafOfModules R
G : M.GeneratingSections
x✝ : C
⊢ Sieve.ofObjects id x✝ = ⊤

Tactic:
simp

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

Goal state before:
pp: case e'_5
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : C ⥤ D
X : C
U : Over X
S : Sieve ((Over.post F).obj U)
Z : C
g : Z ⟶ U.left
hg : (functorPullback F ((overEquiv ((Over.post F).obj U)) S)).arrows g
⊢ F.map (g ≫ U.hom) = F.map g ≫ ((Over.post F).obj U).hom

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X : C
Y : Over X
⊢ ⊤ ∈ ⇑(Sieve.overEquiv Y) ⁻¹' J Y.left

Tactic:
simp

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

Goal state before:
pp: case e'_2
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 f₁ =
    Over.Hom.left ((Over.isoMk (Iso.refl W.left) ⋯).inv ≫ (Over.map f).map (Over.homMk (Over.Hom.left f₁) ⋯))

Tactic:
simp

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

Goal state before:
pp: case e'_3
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 f₂ =
    Over.Hom.left ((Over.isoMk (Iso.refl W.left) ⋯).inv ≫ (Over.map f).map (Over.homMk (Over.Hom.left f₂) ⋯))

Tactic:
simp

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

Goal state before:
pp: C : Type u'
inst✝¹ : Category.{v_1, u'} C
inst✝ : HasBinaryProducts C
J : GrothendieckTopology C
X U : C
S : Sieve U
hs : S ∈ J U
y : C
f : y ⟶ ((Over.star X).obj U).left
⊢ (Sieve.pullback prod.snd S).arrows f →
    ((Sieve.overEquiv ((Over.star X).obj U)) (Sieve.functorPushforward (Over.star X) S)).arrows f

Tactic:
hf

Goal state after:
C : Type u'
inst✝¹ : Category.{v_1, u'} C
inst✝ : HasBinaryProducts C
J : GrothendieckTopology C
X U : C
S : Sieve U
hs : S ∈ J U
y : C
f : y ⟶ ((Over.star X).obj U).left
hf : (Sieve.pullback prod.snd S).arrows f
⊢ ((Sieve.overEquiv ((Over.star X).obj U)) (Sieve.functorPushforward (Over.star X) S)).arrows f
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: case refine_1
C : Type u'
inst✝¹ : Category.{v_1, u'} C
inst✝ : HasBinaryProducts C
J : GrothendieckTopology C
X U : C
S : Sieve U
hs : S ∈ J U
y : C
f : y ⟶ ((Over.star X).obj U).left
hf : (Sieve.pullback prod.snd S).arrows f
⊢ f ≫ prod.fst = (prod.lift (f ≫ prod.fst) (𝟙 y) ≫ (Over.star X ⋙ Over.forget X).map (f ≫ prod.snd)) ≫ prod.fst

Tactic:
simp

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

Goal state before:
pp: case refine_2
C : Type u'
inst✝¹ : Category.{v_1, u'} C
inst✝ : HasBinaryProducts C
J : GrothendieckTopology C
X U : C
S : Sieve U
hs : S ∈ J U
y : C
f : y ⟶ ((Over.star X).obj U).left
hf : (Sieve.pullback prod.snd S).arrows f
⊢ f ≫ prod.snd = (prod.lift (f ≫ prod.fst) (𝟙 y) ≫ (Over.star X ⋙ Over.forget X).map (f ≫ prod.snd)) ≫ prod.snd

Tactic:
simp

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
⊢ f ≫ 𝟙 Y = f

Tactic:
simp

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
⊢ 𝟙 X ≫ f = f

Tactic:
simp

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 Z T : C
f : X ⟶ Y
g : Y ⟶ Z
h : Z ⟶ T
⊢ f ≫ g ≫ h = (f ≫ g) ≫ h

Tactic:
simp

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
F : Sheaf J A
X Y : C
f : X ⟶ Y
⊢ ∀ {X_1 Y_1 : (Over X)ᵒᵖ} (f_1 : X_1 ⟶ Y_1),
    (((Over.map f).sheafPushforwardContinuous A (J.over X) (J.over Y)).obj (F.over Y)).obj.map f_1 ≫
        (Iso.refl
            ((((Over.map f).sheafPushforwardContinuous A (J.over X) (J.over Y)).obj (F.over Y)).obj.obj Y_1)).hom =
      (Iso.refl ((((Over.map f).sheafPushforwardContinuous A (J.over X) (J.over Y)).obj (F.over Y)).obj.obj X_1)).hom ≫
        (F.over X).obj.map f_1

Tactic:
simp

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

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

Tactic:
simp

Goal state after:
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) → P.obj Y → (F ⋙ P).ColimitType
hφ : ∀ (Y : D) (j : StructuredArrow Y F), (F ⋙ P).ιColimitType j.right ∘ ⇑(ConcreteCategory.hom (P.map j.hom)) = φ Y
Y₁ Y₂ : D
f : Y₁ ⟶ Y₂
x✝ : (fun X ↦ X) (P.obj Y₁)
X : StructuredArrow Y₂ F
⊢ (((F ⋙ P).ιColimitType X.right ∘ ⇑(ConcreteCategory.hom (P.map X.hom))) ∘ ⇑(ConcreteCategory.hom (P.map f))) x✝ =
    ((F ⋙ P).ιColimitType ((StructuredArrow.map f).obj X).right ∘
        ⇑(ConcreteCategory.hom (P.map ((StructuredArrow.map f).obj X).hom)))
      x✝

Tactic:
simp

Goal state after:
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
X : D
x : P.obj X
Y : StructuredArrow X F := Classical.arbitrary (StructuredArrow X F)
⊢ F.colimitTypePrecomp P ((F ⋙ P).ιColimitType Y.right ((ConcreteCategory.hom (P.map Y.hom)) x)) = P.ιColimitType X x

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
inst✝ : Simple 0
⊢ 0 ≫ 0 = 𝟙 0 ∧ 0 ≫ 0 = 𝟙 0

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : IsSimpleOrder (Subobject X)
Y : C
f : Y ⟶ X
⊢ ∀ [Mono f], IsIso f ↔ f ≠ 0

Tactic:
hf

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.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:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
cases x
    simp [le_def]

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
conv_rhs => rw [← hf.map_functorObj U]

Goal state after:
X Y : TopCat
f : X ⟶ Y
hf : IsInducing ⇑(ConcreteCategory.hom f)
U : Opens ↑X
x : ↑X
⊢ (ConcreteCategory.hom f) x ∈ hf.functorObj U ↔ x ∈ (Opens.map f).obj (hf.functorObj U)
Module: Mathlib.Topology.Category.TopCat.Opens

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

Tactic:
simp

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

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

Tactic:
trans
  · exact
      (IsLimit.conePointUniqueUpToIso (limit.isLimit _)
          (finiteLimitCone (Discrete.functor f)).isLimit).to_eq
  change Finset.univ.inf (f ∘ discreteEquiv.toEmbedding) = Fintype.elems.inf f
  simp only [← Finset.inf_map, Finset.univ_map_equiv_to_embedding]
  rfl

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
X : SheafOfModules R
U : Cᵒᵖ
x : ↑(((pushforward φ).obj X).val.obj U)
⊢ (ConcreteCategory.hom (X.val.presheaf.map (𝟙 (F.obj (Opposite.unop U))).op)) x =
    (ModuleCat.Hom.hom ((𝟙 ((pushforward φ).obj X)).val.app U)) x

Tactic:
simp

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
X : SheafOfModules S
U : Dᵒᵖ
x : ↑(((pushforward ψ).obj X).val.obj U)
⊢ (ConcreteCategory.hom (X.val.presheaf.map (𝟙 (G.obj (Opposite.unop U))).op)) x =
    (ModuleCat.Hom.hom ((𝟙 ((pushforward ψ).obj X)).val.app U)) x

Tactic:
simp

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
inst✝ : HasColimits C
X Y : TopCat
f : X ⟶ Y
ℱ : Presheaf C Y
U : Opens ↑X
H : IsOpen (⇑(ConcreteCategory.hom f) '' ↑U)
⊢ ((pullback C f).obj ℱ).obj (op U) ≅ ℱ.obj (op { carrier := ⇑(ConcreteCategory.hom f) '' ↑U, is_open' := H })

Tactic:
let x : CostructuredArrow (Opens.map f).op (op U) := CostructuredArrow.mk
    (@homOfLE _ _ _ ((Opens.map f).obj ⟨_, H⟩) (Set.image_preimage.le_u_l _)).op
  have hx : IsTerminal x :=
    { lift := fun s ↦ by
        fapply CostructuredArrow.homMk
        · change op (unop _) ⟶ op (⟨_, H⟩ : Opens _)
          refine (homOfLE ?_).op
          apply (Set.image_mono s.pt.hom.unop.le).trans
          exact Set.image_preimage.l_u_le (SetLike.coe s.pt.left.unop)
        · simp [eq_iff_true_of_subsingleton] }
  exact IsColimit.coconePointUniqueUpToIso
    ((Opens.map f).op.isPointwiseLeftKanExtensionLeftKanExtensionUnit ℱ (op U))
    (colimitOfDiagramTerminal hx _)

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
X : Cᵒᵖ
hX : IsInitial X
hX' : IsInitial (F.op.obj X)
⊢ pushforward φ ⋙ forgetToSheafModuleCat S X hX ≅
    forgetToSheafModuleCat R (F.op.obj X) hX' ⋙
      sheafCompose K (ModuleCat.restrictScalars (RingCat.Hom.hom (φ.hom.app X))) ⋙
        F.sheafPushforwardContinuous (ModuleCat ↑(S.obj.obj X)) J K

Tactic:
refine NatIso.ofComponents (fun M ↦ ObjectProperty.isoMk _ ?_) ?_

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
X : Cᵒᵖ
hX : IsInitial X
hX' : IsInitial (F.op.obj X)
M : SheafOfModules R
⊢ ((pushforward φ ⋙ forgetToSheafModuleCat S X hX).obj M).obj ≅
    ((forgetToSheafModuleCat R (F.op.obj X) hX' ⋙
            sheafCompose K (ModuleCat.restrictScalars (RingCat.Hom.hom (φ.hom.app X))) ⋙
              F.sheafPushforwardContinuous (ModuleCat ↑(S.obj.obj X)) J K).obj
        M).obj

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
X : Cᵒᵖ
hX : IsInitial X
hX' : IsInitial (F.op.obj X)
⊢ ∀ {X_1 Y : SheafOfModules R} (f : X_1 ⟶ Y),
    (pushforward φ ⋙ forgetToSheafModuleCat S X hX).map f ≫ (ObjectProperty.isoMk (Presheaf.IsSheaf J) ?refine_1).hom =
      (ObjectProperty.isoMk (Presheaf.IsSheaf J) ?refine_1).hom ≫
        (forgetToSheafModuleCat R (F.op.obj X) hX' ⋙
              sheafCompose K (ModuleCat.restrictScalars (RingCat.Hom.hom (φ.hom.app X))) ⋙
                F.sheafPushforwardContinuous (ModuleCat ↑(S.obj.obj X)) J K).map
          f
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent

Goal state before:
pp: C✝ : Type u₁
inst✝³ : Category.{v₁, u₁} C✝
J✝ : GrothendieckTopology C✝
R✝ : Sheaf J✝ RingCat
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
R : Sheaf J RingCat
inst✝¹ : HasSheafify J AddCommGrpCat
inst✝ : J.WEqualsLocallyBijective AddCommGrpCat
ι σ : Type u
M : SheafOfModules R
P : M.Presentation
⊢ ((kernel P.generators.π).freeHomEquiv.symm P.relations.s ≫ kernel.ι P.generators.π) ≫ P.generators.π = 0

Tactic:
simp

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

Goal state before:
pp: C✝ : Type u₁
inst✝⁴ : Category.{v₁, u₁} C✝
J✝ : GrothendieckTopology C✝
R✝ : Sheaf J✝ RingCat
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R : Sheaf J RingCat
inst✝² : HasSheafify J AddCommGrpCat
inst✝¹ : J.WEqualsLocallyBijective AddCommGrpCat
ι σ✝ : Type u
M N : SheafOfModules R
f : M ⟶ N
inst✝ : IsIso f
σ : M.Presentation
⊢ kernel (σ.generators.π ≫ f) = kernel (σ.generators.ofEpi f).π

Tactic:
simp

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

Goal state before:
pp: C✝ : Type u₁
inst✝⁷ : Category.{v₁, u₁} C✝
J✝ : GrothendieckTopology C✝
R✝ : Sheaf J✝ RingCat
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R : Sheaf J RingCat
inst✝⁵ : HasSheafify J AddCommGrpCat
inst✝⁴ : J.WEqualsLocallyBijective AddCommGrpCat
ι σ : Type u
C' : Type u₂
inst✝³ : Category.{v₂, u₂} C'
J' : GrothendieckTopology C'
S : Sheaf J' RingCat
inst✝² : HasSheafify J' AddCommGrpCat
inst✝¹ : J'.WEqualsLocallyBijective AddCommGrpCat
M : SheafOfModules R
P : M.Presentation
F : SheafOfModules R ⥤ SheafOfModules S
inst✝ : PreservesColimitsOfSize.{u, u, max u u₁, max u u₂, max (max (u + 1) u₁) v₁, max (max (u + 1) u₂) v₂} F
η : unit S ≅ F.obj (unit R)
⊢ (parallelPair ((kernel P.generators.π).freeHomEquiv.symm P.relations.s ≫ kernel.ι P.generators.π) 0 ⋙ F).map
        WalkingParallelPairHom.right ≫
      (mapFreeIso F P.generators.I η).symm.hom =
    (mapFreeIso F P.relations.I η).symm.hom ≫ (parallelPair (P.mapRelations F η) 0).map WalkingParallelPairHom.right

Tactic:
simp

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

Goal state before:
pp: case e'_2
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
FC : C → C → Type u_2
CC : C → Type u_3
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
inst✝² : HasLimitsOfSize.{x, x, v_1, u_1} C
inst✝¹ : (CategoryTheory.forget C).ReflectsIsomorphisms
inst✝ : PreservesLimitsOfSize.{x, x, v_1, u_3, u_1, u_3 + 1} (CategoryTheory.forget C)
X : TopCat
F : Sheaf C X
ι : Type u_4
U : ι → Opens ↑X
V : Opens ↑X
iUV : (i : ι) → U i ⟶ V
hcover : V ≤ iSup U
sf : (i : ι) → ToType (F.obj.obj (op (U i)))
h : IsCompatible F.obj U sf
V_eq_supr_U : V = iSup U
gl : ToType (F.obj.obj (op (iSup U)))
gl_spec : IsGluing F.obj U sf gl
gl_uniq : ∀ (y : ToType (F.obj.obj (op (iSup U)))), (fun s ↦ IsGluing F.obj U sf s) y → y = gl
gl' : ToType (F.obj.obj (op V))
gl'_spec : ∀ (i : ι), (ConcreteCategory.hom (F.obj.map (iUV i).op)) gl' = sf i
⊢ gl' = (ConcreteCategory.hom (F.obj.map ((eqToHom ⋯).op ≫ (eqToHom V_eq_supr_U).op))) gl'

Tactic:
simp

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
ι : Type u_2
U : ι → Opens ↑X
V : OpensLeCover U
i : ι
a : (Functor.fromPUnit V).obj { as := PUnit.unit } ⟶ (pairwiseToOpensLeCover U).obj (single i)
i' j' : ι
b : (Functor.fromPUnit V).obj { as := PUnit.unit } ⟶ (pairwiseToOpensLeCover U).obj (Pairwise.pair i' j')
⊢ ((pairwiseToOpensLeCover U).obj (Pairwise.pair i' j')).obj ≤ U i'

Tactic:
simp

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
ι : Type u_2
U : ι → Opens ↑X
V : OpensLeCover U
i : ι
a : (Functor.fromPUnit V).obj { as := PUnit.unit } ⟶ (pairwiseToOpensLeCover U).obj (single i)
i' j' : ι
b : (Functor.fromPUnit V).obj { as := PUnit.unit } ⟶ (pairwiseToOpensLeCover U).obj (Pairwise.pair i' j')
⊢ ((pairwiseToOpensLeCover U).obj (Pairwise.pair i' j')).obj ≤ ((pairwiseToOpensLeCover U).obj (single i')).obj

Tactic:
simp

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
ι : Type u_2
U : ι → Opens ↑X
V : OpensLeCover U
i j : ι
a : (Functor.fromPUnit V).obj { as := PUnit.unit } ⟶ (pairwiseToOpensLeCover U).obj (Pairwise.pair i j)
i' : ι
b : (Functor.fromPUnit V).obj { as := PUnit.unit } ⟶ (pairwiseToOpensLeCover U).obj (single i')
⊢ ((pairwiseToOpensLeCover U).obj (Pairwise.pair i j)).obj ≤ ((pairwiseToOpensLeCover U).obj (single i)).obj

Tactic:
simp

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
ι : Type u_2
U : ι → Opens ↑X
V : OpensLeCover U
i j : ι
a : (Functor.fromPUnit V).obj { as := PUnit.unit } ⟶ (pairwiseToOpensLeCover U).obj (Pairwise.pair i j)
i' : ι
b : (Functor.fromPUnit V).obj { as := PUnit.unit } ⟶ (pairwiseToOpensLeCover U).obj (single i')
⊢ ((pairwiseToOpensLeCover U).obj (Pairwise.pair i j)).obj ≤ U i

Tactic:
simp

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
ι : Type u_2
U : ι → Opens ↑X
V : OpensLeCover U
i j : ι
a : (Functor.fromPUnit V).obj { as := PUnit.unit } ⟶ (pairwiseToOpensLeCover U).obj (Pairwise.pair i j)
i' j' : ι
b : (Functor.fromPUnit V).obj { as := PUnit.unit } ⟶ (pairwiseToOpensLeCover U).obj (Pairwise.pair i' j')
⊢ ((pairwiseToOpensLeCover U).obj (Pairwise.pair i j)).obj ≤ ((pairwiseToOpensLeCover U).obj (single i)).obj

Tactic:
simp

Goal state after: