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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : HasPullbacks C
X Y : C
f : X ⟶ Y
⊢ (Over.map f).IsCocontinuous (J.over X) (J.over Y)

Tactic:
]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : HasPullbacks C
X Y : C
f : X ⟶ Y
⊢ (Over.map f).IsCocontinuous (J.over X) (J.over Y)
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
hf : (Sieve.pullback prod.snd S).arrows f
⊢ ((Sieve.overEquiv ((Over.star X).obj U)) (Sieve.functorPushforward (Over.star X) S)).arrows f

Tactic:
dsimp [Sieve.overEquiv]

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
⊢ Presieve.functorPushforward (Over.forget X) (Presieve.functorPushforward (Over.star X) S.arrows) f
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
hf : (Sieve.pullback prod.snd S).arrows f
⊢ Presieve.functorPushforward (Over.star X ⋙ Over.forget X) S.arrows f

Tactic:
]

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
⊢ Presieve.functorPushforward (Over.star X ⋙ Over.forget X) S.arrows f
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: case refine_1.of
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
Z : C
S : Presieve Z
hS : S ∈ K.toCoverage.coverings Z
s : Z ⟶ X
⊢ Sieve.generate (Presieve.functorPullback (Over.forget X) S) ∈
    (Precoverage.comap (Over.forget X) K).toGrothendieck { left := Z, right := right, hom := s }

Tactic:
]

Goal state after:
case refine_1.of
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
Z : C
S : Presieve Z
hS : S ∈ K.toCoverage.coverings Z
s : Z ⟶ X
⊢ Sieve.generate (Presieve.functorPullback (Over.forget X) S) ∈
    (Precoverage.comap (Over.forget X) K).toGrothendieck { left := Z, right := right, hom := s }
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.overEquiv Z).symm (Sieve.pullback (Over.Hom.left g) S) ∈ (Precoverage.comap (Over.forget X) K).toGrothendieck Z

Tactic:
]

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.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
⊢ Precoverage.comap (Over.forget X) K ≤ (K.toGrothendieck.over X).toPrecoverage

Tactic:
]

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
⊢ Precoverage.comap (Over.forget X) K ≤ (K.toGrothendieck.over X).toPrecoverage
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
R : Presieve Y
hR : Presieve.map (Over.forget X) R ∈ K.coverings ((Over.forget X).obj Y)
⊢ R ∈ (K.toGrothendieck.over X).toPrecoverage.coverings Y

Tactic:
]

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
hR : Presieve.map (Over.forget X) R ∈ K.coverings ((Over.forget X).obj Y)
⊢ R ∈ (K.toGrothendieck.over X).toPrecoverage.coverings Y
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
R : Presieve Y
hR : Presieve.map (Over.forget X) R ∈ K.coverings ((Over.forget X).obj Y)
⊢ Sieve.generate (Presieve.map (Over.forget X) R) ∈ K.toGrothendieck Y.left

Tactic:
]

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
hR : Presieve.map (Over.forget X) R ∈ K.coverings ((Over.forget X).obj Y)
⊢ Sieve.generate (Presieve.map (Over.forget X) R) ∈ K.toGrothendieck Y.left
Module: Mathlib.CategoryTheory.Limits.Final.Type

Goal state before:
pp: case refine_1
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
s₁ s₂ : ↑P.sections
h : F.sectionsPrecomp s₁ = F.sectionsPrecomp s₂
Y : D
X : CostructuredArrow F Y := Classical.arbitrary (CostructuredArrow F Y)
this : ↑s₁ (F.obj X.left) = ↑s₂ (F.obj X.left)
h₁ : (ConcreteCategory.hom (P.map X.hom)) (↑s₁ (F.obj X.left)) = ↑s₁ Y
h₂ : (ConcreteCategory.hom (P.map X.hom)) (↑s₂ (F.obj X.left)) = ↑s₂ Y
⊢ ↑s₂ Y = ↑s₂ Y

Tactic:
]

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

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 ((F ⋙ P).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.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:
]

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
Z₁ Z₂ : StructuredArrow Y F
f : Z₁ ⟶ Z₂
x : (fun X ↦ X) (P.obj Y)
⊢ (F ⋙ P).ιColimitType Z₂.right
      ((ConcreteCategory.hom (P.map (F.map (StructuredArrow.Hom.right f)))) ((ConcreteCategory.hom (P.map Z₁.hom)) x)) =
    (F ⋙ P).ιColimitType Z₂.right ((ConcreteCategory.hom (P.map Z₂.hom)) x)

Tactic:
]

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 (F.map (StructuredArrow.Hom.right f)))) ((ConcreteCategory.hom (P.map Z₁.hom)) x)) =
    (F ⋙ P).ιColimitType Z₂.right ((ConcreteCategory.hom (P.map Z₂.hom)) x)
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:
]

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) → 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✝
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.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)

Tactic:
]

Goal state after:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
D' : Type u₃
inst✝⁵ : Category.{v₃, u₃} D'
D'' : Type u₄
inst✝⁴ : Category.{v₄, u₄} D''
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
S : Sheaf J RingCat
R : Sheaf K RingCat
inst✝³ : F.IsContinuous J K
φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R
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.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
⊢ ∀ (T : SheafOfModules R), Function.Bijective fun x ↦ pullbackObjUnitToUnit φ ≫ x

Tactic:
]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
S : Sheaf J RingCat
R : Sheaf K RingCat
inst✝² : F.IsContinuous J K
φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R
inst✝¹ : (pushforward φ).IsRightAdjoint
inst✝ : F.Final
⊢ ∀ (T : SheafOfModules R), Function.Bijective fun x ↦ pullbackObjUnitToUnit φ ≫ 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
⊢ Function.Bijective
    (⇑((pushforward φ).obj M).unitHomEquiv ∘
      ⇑((pullbackPushforwardAdjunction φ).homEquiv (unit S) M) ∘ fun x ↦ pullbackObjUnitToUnit φ ≫ x)

Tactic:
]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
S : Sheaf J RingCat
R : Sheaf K RingCat
inst✝² : F.IsContinuous J K
φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R
inst✝¹ : (pushforward φ).IsRightAdjoint
inst✝ : F.Final
M : SheafOfModules R
⊢ Function.Bijective
    (⇑((pushforward φ).obj M).unitHomEquiv ∘
      ⇑((pullbackPushforwardAdjunction φ).homEquiv (unit S) M) ∘ fun x ↦ pullbackObjUnitToUnit φ ≫ 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
⊢ unitToPushforwardObjUnit φ ≫ (pushforward φ).map f = unitToPushforwardObjUnit φ ≫ (pushforward φ).map f

Tactic:
]

Goal state after:
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.PreservesMonomorphisms
inst✝³ : F.PreservesZeroMorphisms
inst✝² : F.ReflectsIsomorphisms
inst✝¹ : F.Faithful
X : C
inst✝ : Simple (F.obj X)
Y : C
g : Y ⟶ X
x✝ : Mono g
⊢ g = 0 ↔ g = 0

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: case mp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Simple Y
i : X ≅ Y
Y✝ : C
f : Y✝ ⟶ X
m : Mono f
h : IsIso f
w : f = 0
j : f ≫ i.hom ≠ 0
⊢ False

Tactic:
]

Goal state after:
case mp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Simple Y
i : X ≅ Y
Y✝ : C
f : Y✝ ⟶ X
m : Mono f
h : IsIso f
w : f = 0
j : f ≫ i.hom ≠ 0
⊢ False
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Simple Y
i : X ≅ Y
Y✝ : C
f : Y✝ ⟶ X
m : Mono f
h : f ≠ 0
j : IsIso (f ≫ i.hom)
⊢ IsIso ((f ≫ i.hom) ≫ i.inv)

Tactic:
]

Goal state after:
case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Simple Y
i : X ≅ Y
Y✝ : C
f : Y✝ ⟶ X
m : Mono f
h : f ≠ 0
j : IsIso (f ≫ i.hom)
⊢ IsIso ((f ≫ i.hom) ≫ i.inv)
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
⊢ Simple (F.asEquivalence.functor.obj X)

Tactic:
]

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
⊢ Simple (F.asEquivalence.functor.obj X)
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:
]

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
⊢ Simple (F.asEquivalence.functor.obj X)
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasEqualizers C
X Y : C
inst✝¹ : Simple Y
f : X ⟶ Y
inst✝ : HasImage f
w : f ≠ 0
⊢ Epi (factorThruImage f ≫ image.ι f)

Tactic:
]

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasEqualizers C
X Y : C
inst✝¹ : Simple Y
f : X ⟶ Y
inst✝ : HasImage f
w : f ≠ 0
⊢ Epi (factorThruImage f ≫ image.ι f)
Module: Mathlib.Algebra.Category.ModuleCat.Simple

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ IsSimpleOrder (Submodule R ↑(of R M)) ↔ IsSimpleOrder (Submodule R M)

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X Y : C
⊢ biprod.snd ≫ biprod.inr = 0 ↔ IsZero Y

Tactic:
]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X Y : C
⊢ biprod.snd ≫ biprod.inr = 0 ↔ IsZero Y
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X Y : C
h : biprod.snd = 0
⊢ biprod.snd ≫ biprod.inr = 0

Tactic:
]

Goal state after:
case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X Y : C
h : biprod.snd = 0
⊢ biprod.snd ≫ biprod.inr = 0
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X Y : C
h : biprod.snd = 0
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
X : C
inst✝ : Simple X
Y Z : C
i : X ≅ Y ⊞ Z
h : ¬biprod.inl = 0
⊢ IsZero Z

Tactic:
]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
X : C
inst✝ : Simple X
Y Z : C
i : X ≅ Y ⊞ Z
h : ¬biprod.inl = 0
⊢ IsZero Z
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
X : C
inst✝ : Simple X
Y Z : C
i : X ≅ Y ⊞ Z
h : IsIso biprod.inl
this : Simple (Y ⊞ Z)
⊢ IsZero Z

Tactic:
]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
X : C
inst✝ : Simple X
Y Z : C
i : X ≅ Y ⊞ Z
h : IsIso biprod.inl
this : Simple (Y ⊞ Z)
⊢ IsZero Z
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
X : C
inst✝ : Simple X
Y Z : C
i : X ≅ Y ⊞ Z
h : IsZero Z
this : Simple (Y ⊞ Z)
⊢ IsZero Z

Tactic:
]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
X : C
inst✝ : Simple X
Y Z : C
i : X ≅ Y ⊞ Z
h : IsZero Z
this : Simple (Y ⊞ Z)
⊢ IsZero Z
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: case mp
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
i : mk f = ⊤
⊢ f ≠ 0

Tactic:
]

Goal state after:
case mp
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
i : mk f = ⊤
⊢ f ≠ 0
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: case mp
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
i : mk f = ⊤
w : mk f = ⊥
⊢ False

Tactic:
]

Goal state after:
case mp
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
i : mk f = ⊤
w : mk f = ⊥
⊢ False
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: case mpr.inl
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
i : f ≠ 0
h : f = 0
⊢ IsIso f

Tactic:
]

Goal state after:
case mpr.inl
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
i : f ≠ 0
h : f = 0
⊢ IsIso f
Module: Mathlib.CategoryTheory.Limits.Preorder

Goal state before:
pp: C : Type u
inst✝¹ : Preorder C
J : Type u'
inst✝ : Category.{v, u'} J
F : J ⥤ C
c : Cone F
x : C
i : J
p : F.obj i = x
⊢ c.pt ≤ F.obj i

Tactic:
]

Goal state after:
C : Type u
inst✝¹ : Preorder C
J : Type u'
inst✝ : Category.{v, u'} J
F : J ⥤ C
c : Cone F
x : C
i : J
p : F.obj i = x
⊢ c.pt ≤ F.obj i