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
X Y : C
f : X ⟶ Y
U : Over X
S : Sieve ((Over.map f).obj U)
hS : S ∈ (J.over Y) ((Over.map f).obj U)
⊢ Sieve.functorPullback (Over.map f) S ∈ (J.over X) U

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
K : GrothendieckTopology D
F : C ⥤ D
X : C
inst✝ : F.IsCocontinuous J K
U : Over X
S : Sieve ((Over.post F).obj U)
hS : S ∈ (K.over (F.obj X)) ((Over.post F).obj U)
⊢ Sieve.functorPullback (Over.post F) S ∈ (J.over X) U

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
K : GrothendieckTopology D
F : C ⥤ D
X : C
h : CoverPreserving J K F
U : Over X
S : Sieve U
hS : S ∈ (J.over X) U
⊢ Sieve.functorPushforward (Over.post F) S ∈ (K.over (F.obj X)) ((Over.post F).obj U)

Tactic:
by

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

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
J✝ J : GrothendieckTopology C
X : C
Y : Over X
E : (J.over X).OneHypercover Y
⊢ Sieve.functorPushforward (Over.forget X) E.sieve₀ ∈ J Y.left

Tactic:
exact E.mem₀

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J✝ J : GrothendieckTopology C
X : C
Y : Over X
E : (J.over X).OneHypercover Y
i₁ i₂ : E.I₀
W : C
p₁ : W ⟶ (Over.forget X).obj (E.X i₁)
p₂ : W ⟶ (Over.forget X).obj (E.X i₂)
w : p₁ ≫ (Over.forget X).map (E.f i₁) = p₂ ≫ (Over.forget X).map (E.f i₂)
this : p₁ ≫ (E.X i₁).hom = p₂ ≫ (E.X i₂).hom
⊢ Over.homMk p₁ ⋯ ≫ E.f i₁ = Over.homMk p₂ ⋯ ≫ E.f i₂

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
R : Sheaf J RingCat
inst✝¹ : HasWeakSheafify J AddCommGrpCat
inst✝ : J.WEqualsLocallyBijective AddCommGrpCat
I : Type u
⊢ Epi ((free I).freeHomEquiv.symm fun i ↦ freeSection i)

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
R : Sheaf J RingCat
inst✝¹ : HasWeakSheafify J AddCommGrpCat
inst✝ : J.WEqualsLocallyBijective AddCommGrpCat
I : Type u
⊢ IsIso (free.generatingSections I).π

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J✝ J : GrothendieckTopology C
X : C
⊢ (Over.forget X).PreservesOneHypercovers (J.over X) J

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R : Sheaf J RingCat
inst✝⁵ : HasWeakSheafify J AddCommGrpCat
inst✝⁴ : J.WEqualsLocallyBijective AddCommGrpCat
inst✝³ : ∀ (X : C), HasSheafify (J.over X) AddCommGrpCat
inst✝² : HasBinaryProducts C
inst✝¹ : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat
inst✝ : HasSheafify J AddCommGrpCat
I : Type u
i : (free.generatingSections I).localGeneratorsData.I
⊢ IsIso ((free.generatingSections I).localGeneratorsData.generators i).π

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J✝ : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
X : C
inst✝ : F.PreservesOneHypercovers J K
⊢ (Over.post F).PreservesOneHypercovers (J.over X) (K.over (F.obj X))

Tactic:
by

Goal state after:
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
⊢ CoverPreserving (J.over Y) (J.over X) (Over.pullback f)

Tactic:
by

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
⊢ Sieve.functorPushforward (Over.star X) S ∈ (J.over X) ((Over.star X).obj U)

Tactic:
by

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 g : X ⟶ Y
h : f = g
⊢ J.overMapPullback A f = J.overMapPullback A g

Tactic:
by

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 g : X ⟶ Y
h : f = g
⊢ J.overMapPullbackCongr A h = eqToIso ⋯

Tactic:
by

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:
by

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
⊢ (J.overMapPullbackComp A f (𝟙 Y)).inv ≫
      Functor.whiskerRight (J.overMapPullbackId A Y).hom (J.overMapPullback A f) ≫
        (J.overMapPullback A f).leftUnitor.hom =
    (J.overMapPullbackCongr A ⋯).hom

Tactic:
by

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:
by

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
⊢ (J.overMapPullbackComp A (𝟙 X) f).inv ≫
      (J.overMapPullback A f).whiskerLeft (J.overMapPullbackId A X).hom ≫ (J.overMapPullback A f).rightUnitor.hom =
    (J.overMapPullbackCongr A ⋯).hom

Tactic:
by

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:
by

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
⊢ (J.overMapPullbackComp A f (g ≫ h)).inv ≫
      Functor.whiskerRight (J.overMapPullbackComp A g h).inv (J.overMapPullback A f) ≫
        ((J.overMapPullback A h).associator (J.overMapPullback A g) (J.overMapPullback A f)).hom ≫
          (J.overMapPullback A h).whiskerLeft (J.overMapPullbackComp A f g).hom ≫
            (J.overMapPullbackComp A (f ≫ g) h).hom =
    (J.overMapPullbackCongr A ⋯).hom

Tactic:
by

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:
by

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
inst✝ : Limits.HasPullbacks C
F : Sheaf J A
X Y : C
f : X ⟶ Y
⊢ ∀ ⦃X_1 Y_1 : (Over Y)ᵒᵖ⦄ (f_1 : X_1 ⟶ Y_1),
    (F.over Y).obj.map f_1 ≫ F.obj.map (Limits.pullback.fst (Opposite.unop Y_1).hom f).op =
      F.obj.map (Limits.pullback.fst (Opposite.unop X_1).hom f).op ≫
        (((Over.pullback f).sheafPushforwardContinuous A (J.over Y) (J.over X)).obj (F.over X)).obj.map f_1

Tactic:
by

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

Goal state before:
pp: 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
⊢ Presieve.functorPullback (Over.forget X) S ∈
    (Precoverage.comap (Over.forget X) K).coverings { left := Z, right := right, hom := s }

Tactic:
by

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

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

Tactic:
by

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 : C
f : Over X
⊢ ∀ {X_1 : Over f.left} {S : Sieve X_1},
    Sieve.functorPushforward f.iteratedSliceEquiv.inverse S ∈
        ((J.over X).over f) (f.iteratedSliceEquiv.inverse.obj X_1) ↔
      S ∈ (J.over f.left) X_1

Tactic:
by

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
⊢ ∃ a, ∀ (j : CostructuredArrow F Y), (ConcreteCategory.hom (P.map j.hom)) (↑t j.left) = a

Tactic:
by

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
⊢ Function.Bijective F.sectionsPrecomp

Tactic:
by

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
⊢ ∃ a, ∀ (j : StructuredArrow Y F), (F ⋙ P).ιColimitType j.right ∘ ⇑(ConcreteCategory.hom (P.map j.hom)) = a

Tactic:
by

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₂
⊢ φ Y₂ ∘ ⇑(ConcreteCategory.hom (P.map f)) = φ Y₁

Tactic:
by

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:
by

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
⊢ Function.Bijective (F.colimitTypePrecomp P)

Tactic:
by

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

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✝ Y✝ : Cᵒᵖ
f : X✝ ⟶ Y✝
⊢ (unit S).val.map f ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom (S.obj.map f))).map
        (ModuleCat.homMk ((forget₂ RingCat AddCommGrpCat).map (φ.hom.app Y✝)) ⋯) =
    ModuleCat.homMk ((forget₂ RingCat AddCommGrpCat).map (φ.hom.app X✝)) ⋯ ≫ ((pushforward φ).obj (unit R)).val.map f

Tactic:
by

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
M : SheafOfModules R
f : unit R ⟶ M
⊢ pushforwardSections φ (M.unitHomEquiv f) =
    ((pushforward φ).obj M).unitHomEquiv (unitToPushforwardObjUnit φ ≫ (pushforward φ).map f)

Tactic:
by

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 ((forget S).obj X')) Y).trans
            (((PresheafOfModules.pullbackPushforwardAdjunction φ.hom).homEquiv X'.val Y.val).trans
              (fullyFaithfulForget S).homEquiv.symm)).symm
        (f ≫ g) =
      (forget S ⋙ PresheafOfModules.pullback φ.hom ⋙ PresheafOfModules.sheafification (𝟙 R.obj)).map f ≫
        (((PresheafOfModules.sheafificationAdjunction (𝟙 R.obj)).homEquiv
                  ((PresheafOfModules.pullback φ.hom).obj ((forget S).obj X)) Y).trans
              (((PresheafOfModules.pullbackPushforwardAdjunction φ.hom).homEquiv X.val Y.val).trans
                (fullyFaithfulForget S).homEquiv.symm)).symm
          g

Tactic:
by

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 : SheafOfModules S} {Y Y' : SheafOfModules R}
    (f : (forget S ⋙ PresheafOfModules.pullback φ.hom ⋙ PresheafOfModules.sheafification (𝟙 R.obj)).obj X ⟶ Y)
    (g : Y ⟶ Y'),
    (((PresheafOfModules.sheafificationAdjunction (𝟙 R.obj)).homEquiv
              ((PresheafOfModules.pullback φ.hom).obj ((forget S).obj X)) Y').trans
          (((PresheafOfModules.pullbackPushforwardAdjunction φ.hom).homEquiv X.val Y'.val).trans
            (fullyFaithfulForget S).homEquiv.symm))
        (f ≫ g) =
      (((PresheafOfModules.sheafificationAdjunction (𝟙 R.obj)).homEquiv
                ((PresheafOfModules.pullback φ.hom).obj ((forget S).obj X)) Y).trans
            (((PresheafOfModules.pullbackPushforwardAdjunction φ.hom).homEquiv X.val Y.val).trans
              (fullyFaithfulForget S).homEquiv.symm))
          f ≫
        (pushforward φ).map g

Tactic:
by

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
⊢ IsIso g ↔ g ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: 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
⊢ IsIso (f ≫ i.hom)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: 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
⊢ IsIso (f ≫ i.hom)

Tactic:
by

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
inst✝¹ : (pushforward φ).IsRightAdjoint
inst✝ : F.Final
⊢ IsIso (pullbackObjUnitToUnit φ)

Tactic:
by

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
inst✝⁵ : (pushforward φ).IsRightAdjoint
inst✝⁴ : HasWeakSheafify J AddCommGrpCat
inst✝³ : HasWeakSheafify K AddCommGrpCat
inst✝² : J.WEqualsLocallyBijective AddCommGrpCat
inst✝¹ : K.WEqualsLocallyBijective AddCommGrpCat
inst✝ : F.Final
I : Type u
i : I
⊢ (pullback φ).map (ιFree i) ≫ (pullbackObjFreeIso φ I).hom = pullbackObjUnitToUnit φ ≫ ιFree i

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: 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
⊢ IsIso f ↔ f ≠ 0

Tactic:
by

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
inst✝⁵ : (pushforward φ).IsRightAdjoint
inst✝⁴ : HasWeakSheafify J✝ AddCommGrpCat
inst✝³ : HasWeakSheafify K AddCommGrpCat
inst✝² : J✝.WEqualsLocallyBijective AddCommGrpCat
inst✝¹ : K.WEqualsLocallyBijective AddCommGrpCat
inst✝ : F.Final
I J : Type u
f : I → J
i : I
⊢ (Cofan.mk ((pullback φ).obj (free I)) fun j ↦ (pullback φ).map (ιFree j)).inj i ≫
      (pullback φ).map (freeMap f) ≫ (pullbackObjFreeIso φ J).hom =
    (Cofan.mk ((pullback φ).obj (free I)) fun j ↦ (pullback φ).map (ιFree j)).inj i ≫
      (pullbackObjFreeIso φ I).hom ≫ freeMap f

Tactic:
by

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.IsEquivalence
X : C
inst✝ : Simple X
⊢ Simple (F.obj X)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
X Y : C
inst✝¹ : Simple X
f : X ⟶ Y
inst✝ : HasKernel f
w : f ≠ 0
⊢ kernel.ι f = 0

Tactic:
by

Goal state after:
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
⊢ Simple (of R M) ↔ IsSimpleModule R M

Tactic:
by

Goal state after:
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 f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
X Y : C
inst✝¹ : Simple Y
f : X ⟶ Y
inst✝ : Mono f
w : IsIso f → False
⊢ f = 0

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X : C
inst✝ : Simple X
⊢ IsIso (𝟙 X)

Tactic:
by

Goal state after:
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:
by

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:
by

Goal state after:
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
h : ∀ {Z : C} (f : X ⟶ Z) [Epi f], IsIso f ↔ f ≠ 0
Y : C
f : Y ⟶ X
I : Mono f
hf : f ≠ 0
this : Epi f
⊢ IsIso f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: case mpr
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
h : ∀ {Z : C} (f : X ⟶ Z) [Epi f], IsIso f ↔ f ≠ 0
Y : C
f : Y ⟶ X
I : Mono f
hf : f ≠ 0
⊢ IsIso f

Tactic:
suffices Epi f by exact isIso_of_mono_of_epi _

Goal state after:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
h : ∀ {Z : C} (f : X ⟶ Z) [Epi f], IsIso f ↔ f ≠ 0
Y : C
f : Y ⟶ X
I : Mono f
hf : f ≠ 0
⊢ Epi f
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
h : ∀ {Z : C} (f : X ⟶ Z) [Epi f], IsIso f ↔ f ≠ 0
Y : C
f : Y ⟶ X
I : Mono f
⊢ IsIso f ↔ f ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X Y : C
inst✝ : Simple Y
f : X ⟶ Y
w : f ≠ 0
⊢ cokernel.π f = 0

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
X Y : C
inst✝¹ : Simple X
f : X ⟶ Y
inst✝ : Epi f
w : IsIso f → False
⊢ f = 0

Tactic:
by

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

Goal state before:
pp: X✝ : Type u
Y✝ : Type v
inst✝¹ : Preorder X✝
inst✝ : Preorder Y✝
l : X✝ → Y✝
u : Y✝ → X✝
gc : GaloisConnection l u
X : X✝
Y : Y✝
⊢ Function.LeftInverse (fun f ↦ CategoryTheory.homOfLE ⋯) fun f ↦ CategoryTheory.homOfLE ⋯

Tactic:
by

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
⊢ IsIso biprod.inl ↔ IsZero Y

Tactic:
by

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

Goal state before:
pp: X✝ : Type u
Y✝ : Type v
inst✝¹ : Preorder X✝
inst✝ : Preorder Y✝
l : X✝ → Y✝
u : Y✝ → X✝
gc : GaloisConnection l u
X : X✝
Y : Y✝
⊢ Function.RightInverse (fun f ↦ CategoryTheory.homOfLE ⋯) fun f ↦ CategoryTheory.homOfLE ⋯

Tactic:
by

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
⊢ IsZero Y ∨ IsZero Z

Tactic:
by

Goal state after: