mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
h₁ : HasProjectiveDimensionLT S.X₁ n
h₃ : HasProjectiveDimensionLT S.X₃ n
this : HasExt C := HasExt.standard C
i : ℕ
hi : n ≤ i
Y : C
x₃ : Ext S.X₃ Y i
⊢ (Ext.mk₀ S.g).comp 0 ⋯ = 0

Tactic:
Ext.comp_zero

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
h₁ : HasProjectiveDimensionLT S.X₁ n
h₃ : HasProjectiveDimensionLT S.X₃ n
this : HasExt C := HasExt.standard C
i : ℕ
hi : n ≤ i
Y : C
x₃ : Ext S.X₃ Y i
⊢ 0 = 0
Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
h₁ : HasProjectiveDimensionLT S.X₁ n
h₂ : HasProjectiveDimensionLT S.X₂ (n + 1)
this : HasExt C := HasExt.standard C
⊢ ∀ (i : ℕ), n + 1 ≤ i → ∀ ⦃Y : C⦄ (e : Ext S.X₃ Y i), e = 0

Tactic:
rintro (_ | i) hi Y x₃

Goal state after:
case zero
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
h₁ : HasProjectiveDimensionLT S.X₁ n
h₂ : HasProjectiveDimensionLT S.X₂ (n + 1)
this : HasExt C := HasExt.standard C
hi : n + 1 ≤ 0
Y : C
x₃ : Ext S.X₃ Y 0
⊢ x₃ = 0

case succ
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
h₁ : HasProjectiveDimensionLT S.X₁ n
h₂ : HasProjectiveDimensionLT S.X₂ (n + 1)
this : HasExt C := HasExt.standard C
i : ℕ
hi : n + 1 ≤ i + 1
Y : C
x₃ : Ext S.X₃ Y (i + 1)
⊢ x₃ = 0
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification

Goal state before:
pp: C : Type u'
inst✝⁴ : Category.{v', u'} C
J : GrothendieckTopology C
R₀ : Cᵒᵖ ⥤ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.obj
inst✝³ : Presheaf.IsLocallyInjective J α
inst✝² : Presheaf.IsLocallySurjective J α
inst✝¹ : J.WEqualsLocallyBijective AddCommGrpCat
inst✝ : HasWeakSheafify J AddCommGrpCat
P : PresheafOfModules R₀
F : SheafOfModules R
f : (sheafification α).obj P ⟶ F
⊢ (SheafOfModules.toSheaf R).map ((sheafificationHomEquiv α).symm ((sheafificationHomEquiv α) f)) =
    ((sheafificationAdjunction J AddCommGrpCat).homEquiv P.presheaf ((SheafOfModules.toSheaf R).obj F)).symm
      ((toPresheaf R₀).map ((sheafificationHomEquiv α) f))

Tactic:
apply ((sheafificationAdjunction J AddCommGrpCat).homEquiv _ _).injective

Goal state after:
C : Type u'
inst✝⁴ : Category.{v', u'} C
J : GrothendieckTopology C
R₀ : Cᵒᵖ ⥤ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.obj
inst✝³ : Presheaf.IsLocallyInjective J α
inst✝² : Presheaf.IsLocallySurjective J α
inst✝¹ : J.WEqualsLocallyBijective AddCommGrpCat
inst✝ : HasWeakSheafify J AddCommGrpCat
P : PresheafOfModules R₀
F : SheafOfModules R
f : (sheafification α).obj P ⟶ F
⊢ ((sheafificationAdjunction J AddCommGrpCat).homEquiv P.presheaf ((SheafOfModules.toSheaf R).obj F))
      ((SheafOfModules.toSheaf R).map ((sheafificationHomEquiv α).symm ((sheafificationHomEquiv α) f))) =
    ((sheafificationAdjunction J AddCommGrpCat).homEquiv P.presheaf ((SheafOfModules.toSheaf R).obj F))
      (((sheafificationAdjunction J AddCommGrpCat).homEquiv P.presheaf ((SheafOfModules.toSheaf R).obj F)).symm
        ((toPresheaf R₀).map ((sheafificationHomEquiv α) f)))
Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension

Goal state before:
pp: case succ
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
h₁ : HasProjectiveDimensionLT S.X₁ n
h₂ : HasProjectiveDimensionLT S.X₂ (n + 1)
this : HasExt C := HasExt.standard C
i : ℕ
hi : n + 1 ≤ i + 1
Y : C
x₁ : Ext S.X₁ Y i
⊢ hS.extClass.comp 0 ⋯ = 0

Tactic:
Ext.comp_zero

Goal state after:
case succ
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
h₁ : HasProjectiveDimensionLT S.X₁ n
h₂ : HasProjectiveDimensionLT S.X₂ (n + 1)
this : HasExt C := HasExt.standard C
i : ℕ
hi : n + 1 ≤ i + 1
Y : C
x₁ : Ext S.X₁ Y i
⊢ 0 = 0
Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
h₂ : HasProjectiveDimensionLT S.X₂ n
h₃ : HasProjectiveDimensionLT S.X₃ (n + 1)
this : HasExt C := HasExt.standard C
i : ℕ
hi : n ≤ i
Y : C
x₂ : Ext S.X₂ Y i
⊢ (Ext.mk₀ S.f).comp 0 ⋯ = 0

Tactic:
Ext.comp_zero

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
h₂ : HasProjectiveDimensionLT S.X₂ n
h₃ : HasProjectiveDimensionLT S.X₃ (n + 1)
this : HasExt C := HasExt.standard C
i : ℕ
hi : n ≤ i
Y : C
x₂ : Ext S.X₂ Y i
⊢ 0 = 0
Module: Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
F : C ⥤ D
b₀✝ b₁✝ b₂✝ : LocallyDiscrete C
x✝¹ : b₀✝ ⟶ b₁✝
x✝ : b₁✝ ⟶ b₂✝
f : b₀✝.as ⟶ b₁✝.as
g : b₁✝.as ⟶ b₂✝.as
⊢ (match { as := f } ≫ { as := g } with
    | { as := f } => (F.map f).toLoc) =
    (match { as := f } with
      | { as := f } => (F.map f).toLoc) ≫
      match { as := g } with
      | { as := f } => (F.map f).toLoc

Tactic:
by simp [CategoryStruct.comp]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R₀ : Cᵒᵖ ⥤ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.obj
inst✝³ : Presheaf.IsLocallyInjective J α
inst✝² : Presheaf.IsLocallySurjective J α
M₀ : PresheafOfModules R₀
A : Sheaf J AddCommGrpCat
φ : M₀.presheaf ⟶ A.obj
inst✝¹ : Presheaf.IsLocallyInjective J φ
inst✝ : Presheaf.IsLocallySurjective J φ
X : Cᵒᵖ
r : ↑(R.obj.obj X)
m m' : ↑(A.obj.obj X)
S : Sieve (Opposite.unop X) := Presheaf.imageSieve α r ⊓ Presheaf.imageSieve φ m ⊓ Presheaf.imageSieve φ m'
hS : S ∈ J (Opposite.unop X)
Y : C
f : Y ⟶ Opposite.unop X
r₀ : ToType (R₀.obj (Opposite.op Y))
hr₀ : (ConcreteCategory.hom (α.app (Opposite.op Y))) r₀ = (ConcreteCategory.hom (R.obj.map f.op)) r
m₀ : ↑(M₀.obj (Opposite.op Y))
hm₀ : (ConcreteCategory.hom (φ.app (Opposite.op Y))) m₀ = (ConcreteCategory.hom (A.obj.map f.op)) m
m₀' : ↑(M₀.obj (Opposite.op Y))
hm₀' : (ConcreteCategory.hom (φ.app (Opposite.op Y))) m₀' = (ConcreteCategory.hom (A.obj.map f.op)) m'
⊢ (ConcreteCategory.hom (A.obj.map f.op)) (smul α φ r (m + m')) =
    (ConcreteCategory.hom (A.obj.map f.op)) (smul α φ r m + smul α φ r m')

Tactic:
(A.obj.map f.op).hom.map_add,

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R₀ : Cᵒᵖ ⥤ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.obj
inst✝³ : Presheaf.IsLocallyInjective J α
inst✝² : Presheaf.IsLocallySurjective J α
M₀ : PresheafOfModules R₀
A : Sheaf J AddCommGrpCat
φ : M₀.presheaf ⟶ A.obj
inst✝¹ : Presheaf.IsLocallyInjective J φ
inst✝ : Presheaf.IsLocallySurjective J φ
X : Cᵒᵖ
r : ↑(R.obj.obj X)
m m' : ↑(A.obj.obj X)
S : Sieve (Opposite.unop X) := Presheaf.imageSieve α r ⊓ Presheaf.imageSieve φ m ⊓ Presheaf.imageSieve φ m'
hS : S ∈ J (Opposite.unop X)
Y : C
f : Y ⟶ Opposite.unop X
r₀ : ToType (R₀.obj (Opposite.op Y))
hr₀ : (ConcreteCategory.hom (α.app (Opposite.op Y))) r₀ = (ConcreteCategory.hom (R.obj.map f.op)) r
m₀ : ↑(M₀.obj (Opposite.op Y))
hm₀ : (ConcreteCategory.hom (φ.app (Opposite.op Y))) m₀ = (ConcreteCategory.hom (A.obj.map f.op)) m
m₀' : ↑(M₀.obj (Opposite.op Y))
hm₀' : (ConcreteCategory.hom (φ.app (Opposite.op Y))) m₀' = (ConcreteCategory.hom (A.obj.map f.op)) m'
⊢ (ConcreteCategory.hom (A.obj.map f.op)) (smul α φ r (m + m')) =
    (AddCommGrpCat.Hom.hom (A.obj.map f.op)) (smul α φ r m) + (AddCommGrpCat.Hom.hom (A.obj.map f.op)) (smul α φ r m')
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R₀ : Cᵒᵖ ⥤ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.obj
inst✝³ : Presheaf.IsLocallyInjective J α
inst✝² : Presheaf.IsLocallySurjective J α
M₀ : PresheafOfModules R₀
A : Sheaf J AddCommGrpCat
φ : M₀.presheaf ⟶ A.obj
inst✝¹ : Presheaf.IsLocallyInjective J φ
inst✝ : Presheaf.IsLocallySurjective J φ
X : Cᵒᵖ
r r' : ↑(R.obj.obj X)
m : ↑(A.obj.obj X)
S : Sieve (Opposite.unop X) := Presheaf.imageSieve α r ⊓ Presheaf.imageSieve α r' ⊓ Presheaf.imageSieve φ m
hS : S ∈ J (Opposite.unop X)
Y : C
f : Y ⟶ Opposite.unop X
r₀ : ↑(R₀.obj (Opposite.op Y))
hr₀ : (ConcreteCategory.hom (α.app (Opposite.op Y))) r₀ = (ConcreteCategory.hom (R.obj.map f.op)) r
r₀' : ↑(R₀.obj (Opposite.op Y))
hr₀' : (ConcreteCategory.hom (α.app (Opposite.op Y))) r₀' = (ConcreteCategory.hom (R.obj.map f.op)) r'
m₀ : ToType (M₀.presheaf.obj (Opposite.op Y))
hm₀ : (ConcreteCategory.hom (φ.app (Opposite.op Y))) m₀ = (ConcreteCategory.hom (A.obj.map f.op)) m
⊢ (ConcreteCategory.hom (A.obj.map f.op)) (smul α φ (r + r') m) =
    (ConcreteCategory.hom (A.obj.map f.op)) (smul α φ r m + smul α φ r' m)

Tactic:
(A.obj.map f.op).hom.map_add,

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R₀ : Cᵒᵖ ⥤ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.obj
inst✝³ : Presheaf.IsLocallyInjective J α
inst✝² : Presheaf.IsLocallySurjective J α
M₀ : PresheafOfModules R₀
A : Sheaf J AddCommGrpCat
φ : M₀.presheaf ⟶ A.obj
inst✝¹ : Presheaf.IsLocallyInjective J φ
inst✝ : Presheaf.IsLocallySurjective J φ
X : Cᵒᵖ
r r' : ↑(R.obj.obj X)
m : ↑(A.obj.obj X)
S : Sieve (Opposite.unop X) := Presheaf.imageSieve α r ⊓ Presheaf.imageSieve α r' ⊓ Presheaf.imageSieve φ m
hS : S ∈ J (Opposite.unop X)
Y : C
f : Y ⟶ Opposite.unop X
r₀ : ↑(R₀.obj (Opposite.op Y))
hr₀ : (ConcreteCategory.hom (α.app (Opposite.op Y))) r₀ = (ConcreteCategory.hom (R.obj.map f.op)) r
r₀' : ↑(R₀.obj (Opposite.op Y))
hr₀' : (ConcreteCategory.hom (α.app (Opposite.op Y))) r₀' = (ConcreteCategory.hom (R.obj.map f.op)) r'
m₀ : ToType (M₀.presheaf.obj (Opposite.op Y))
hm₀ : (ConcreteCategory.hom (φ.app (Opposite.op Y))) m₀ = (ConcreteCategory.hom (A.obj.map f.op)) m
⊢ (ConcreteCategory.hom (A.obj.map f.op)) (smul α φ (r + r') m) =
    (AddCommGrpCat.Hom.hom (A.obj.map f.op)) (smul α φ r m) + (AddCommGrpCat.Hom.hom (A.obj.map f.op)) (smul α φ r' m)
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R₀ : Cᵒᵖ ⥤ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.obj
inst✝³ : Presheaf.IsLocallyInjective J α
inst✝² : Presheaf.IsLocallySurjective J α
M₀ : PresheafOfModules R₀
A : Sheaf J AddCommGrpCat
φ : M₀.presheaf ⟶ A.obj
inst✝¹ : Presheaf.IsLocallyInjective J φ
inst✝ : Presheaf.IsLocallySurjective J φ
X : Cᵒᵖ
r r' : ↑(R.obj.obj X)
m : ↑(A.obj.obj X)
S : Sieve (Opposite.unop X) := Presheaf.imageSieve α r ⊓ Presheaf.imageSieve α r' ⊓ Presheaf.imageSieve φ m
hS : S ∈ J (Opposite.unop X)
Y : C
f : Y ⟶ Opposite.unop X
r₀ : ↑(R₀.obj (Opposite.op Y))
hr₀ : (ConcreteCategory.hom (α.app (Opposite.op Y))) r₀ = (ConcreteCategory.hom (R.obj.map f.op)) r
r₀' : ↑(R₀.obj (Opposite.op Y))
hr₀' : (ConcreteCategory.hom (α.app (Opposite.op Y))) r₀' = (ConcreteCategory.hom (R.obj.map f.op)) r'
m₀ : ToType (M₀.presheaf.obj (Opposite.op Y))
hm₀ : (ConcreteCategory.hom (φ.app (Opposite.op Y))) m₀ = (ConcreteCategory.hom (A.obj.map f.op)) m
⊢ (ConcreteCategory.hom (α.app (Opposite.op Y))) (r₀ + r₀') = (ConcreteCategory.hom (R.obj.map f.op)) (r + r')

Tactic:
by rw [_root_.map_add, _root_.map_add, hr₀, hr₀']

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Flat

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : RepresentablyFlat F
inst✝ : RepresentablyFlat G
⊢ RepresentablyFlat (F ⋙ G)

Tactic:
refine ⟨fun X => IsCofiltered.of_cone_nonempty.{0} _ (fun {J} _ _ H => ?_)⟩

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : RepresentablyFlat F
inst✝ : RepresentablyFlat G
X : E
J : Type
x✝¹ : SmallCategory J
x✝ : FinCategory J
H : J ⥤ StructuredArrow X (F ⋙ G)
⊢ Nonempty (Cone H)
Module: Mathlib.CategoryTheory.Functor.Flat

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type v₁
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
F : C ⥤ D
inst✝ : RepresentablyFlat F
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
f₁ f₂ : s.pt ⟶ F.obj c.pt
h₁ : ∀ (j : J), f₁ ≫ (F.mapCone c).π.app j = s.π.app j
h₂ : ∀ (j : J), f₂ ≫ (F.mapCone c).π.app j = s.π.app j
α₁ : (F.mapCone c).toStructuredArrow ⋙ map f₁ ⟶ s.toStructuredArrow := { app := fun X ↦ eqToHom ⋯, naturality := ⋯ }
α₂ : (F.mapCone c).toStructuredArrow ⋙ map f₂ ⟶ s.toStructuredArrow := { app := fun X ↦ eqToHom ⋯, naturality := ⋯ }
c₁ : Cone (s.toStructuredArrow ⋙ pre s.pt K F) :=
  (Cone.postcompose (Functor.whiskerRight α₁ (pre s.pt K F))).obj (c.toStructuredArrowCone F f₁)
c₂ : Cone (s.toStructuredArrow ⋙ pre s.pt K F) :=
  (Cone.postcompose (Functor.whiskerRight α₂ (pre s.pt K F))).obj (c.toStructuredArrowCone F f₂)
c₀ : Cone (biconeMk J c₁ c₂) := IsCofiltered.cone (biconeMk J c₁ c₂)
g₁ : c₀.pt ⟶ c₁.pt := c₀.π.app Bicone.left
g₂ : c₀.pt ⟶ c₂.pt := c₀.π.app Bicone.right
this : ∀ (j : J), Hom.right g₁ ≫ c.π.app j = Hom.right g₂ ≫ c.π.app j
x : J
⊢ ((Functor.const J).map (Hom.right g₁) ≫ c.π).app x = ((Functor.const J).map (Hom.right g₂) ≫ c.π).app x

Tactic:
apply this

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreZeroHypercover S
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : C ⥤ D
⊢ (map F E).sieve₀ = Sieve.functorPushforward F E.sieve₀

Tactic:
by
  simp [← Sieve.generate_map_eq_functorPushforward, Presieve.map_ofArrows, map]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
R : Presieve Y
inst✝ : R.HasPullbacks f
Z : C
g : Z ⟶ X
W : C
b : W ⟶ Y
hb : R b
⊢ ∃ W_1 i e, R e ∧ i ≫ e = pullback.snd b f ≫ f

Tactic:
have := R.hasPullback f hb

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
R : Presieve Y
inst✝ : R.HasPullbacks f
Z : C
g : Z ⟶ X
W : C
b : W ⟶ Y
hb : R b
this : HasPullback b f
⊢ ∃ W_1 i e, R e ∧ i ≫ e = pullback.snd b f ≫ f
Module: Mathlib.CategoryTheory.Sites.Coverage

Goal state before:
pp: case a
C : Type u_1
inst✝ : Category.{v_1, u_1} C
K : Coverage C
X : C
S : Presieve X
hS : S ∈ K.coverings X
⊢ S ∈ K.toGrothendieck.toCoverage.coverings X

Tactic:
apply Saturate.of _ _ hS

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

Goal state before:
pp: case mpr
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
H : J.OneHypercoverFamily
P : Cᵒᵖ ⥤ A
inst✝ : H.IsGenerating
hP : ∀ ⦃X : C⦄ (E : J.OneHypercover X), H E → Nonempty (IsLimit (E.multifork P))
⊢ ∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork P))

Tactic:
rintro X ⟨S, hS⟩

Goal state after:
case mpr
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
H : J.OneHypercoverFamily
P : Cᵒᵖ ⥤ A
inst✝ : H.IsGenerating
hP : ∀ ⦃X : C⦄ (E : J.OneHypercover X), H E → Nonempty (IsLimit (E.multifork P))
X : C
S : Sieve X
hS : S ∈ J X
⊢ Nonempty (IsLimit (Cover.multifork ⟨S, hS⟩ P))
Module: Mathlib.CategoryTheory.Functor.KanExtension.Preserves

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst✝⁵ : Category.{v_1, u_1} A
inst✝⁴ : Category.{v_2, u_2} B
inst✝³ : Category.{v_3, u_3} C
inst✝² : Category.{v_4, u_4} D
G : B ⥤ D
F : A ⥤ B
L : A ⥤ C
inst✝¹ : G.PreservesPointwiseRightKanExtension F L
inst✝ : L.HasPointwiseRightKanExtension F
⊢ L.whiskerLeft (G.pointwiseRightKanExtensionCompIsoOfPreserves F L).hom ≫ L.pointwiseRightKanExtensionCounit (F ⋙ G) =
    (L.associator (L.pointwiseRightKanExtension F) G).inv ≫ whiskerRight (L.pointwiseRightKanExtensionCounit F) G

Tactic:
simp [pointwiseRightKanExtensionCompIsoOfPreserves]

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Preserves

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst✝⁵ : Category.{v_1, u_1} A
inst✝⁴ : Category.{v_2, u_2} B
inst✝³ : Category.{v_3, u_3} C
inst✝² : Category.{v_4, u_4} D
G : B ⥤ D
F : A ⥤ B
L : A ⥤ C
inst✝¹ : G.PreservesPointwiseRightKanExtension F L
inst✝ : L.HasPointwiseRightKanExtension F
a : A
⊢ (G.pointwiseRightKanExtensionCompIsoOfPreserves F L).hom.app (L.obj a) ≫
      (L.pointwiseRightKanExtensionCounit (F ⋙ G)).app a =
    G.map ((L.pointwiseRightKanExtensionCounit F).app a)

Tactic:
by
  simpa [-pointwiseRightKanExtensionCompIsoOfPreserves_hom_fac] using
    NatTrans.congr_app (pointwiseRightKanExtensionCompIsoOfPreserves_hom_fac G F L) a

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Preserves

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst✝⁵ : Category.{v_1, u_1} A
inst✝⁴ : Category.{v_2, u_2} B
inst✝³ : Category.{v_3, u_3} C
inst✝² : Category.{v_4, u_4} D
G : B ⥤ D
F : A ⥤ B
L : A ⥤ C
inst✝¹ : G.PreservesPointwiseRightKanExtension F L
inst✝ : L.HasPointwiseRightKanExtension F
⊢ L.whiskerLeft (G.pointwiseRightKanExtensionCompIsoOfPreserves F L).inv ≫
      (L.associator (L.pointwiseRightKanExtension F) G).inv ≫ whiskerRight (L.pointwiseRightKanExtensionCounit F) G =
    L.pointwiseRightKanExtensionCounit (F ⋙ G)

Tactic:
simp [pointwiseRightKanExtensionCompIsoOfPreserves]

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
K : GrothendieckTopology D
G : C ⥤ D
ℱ : Dᵒᵖ ⥤ Type v
ℱ' : Sheaf K (Type v)
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
X : D
x : ℱ.obj (op X)
this :
  ∀ {Z : D} {W₁ W₂ : C} (iWX₁ : G.obj W₁ ⟶ X) (iWX₂ : G.obj W₂ ⟶ X) (iZW₁ : Z ⟶ G.obj W₁) (iZW₂ : Z ⟶ G.obj W₂),
    iZW₁ ≫ iWX₁ = iZW₂ ≫ iWX₂ →
      (ConcreteCategory.hom (ℱ'.obj.map iZW₁.op))
          ((ConcreteCategory.hom (α.app (op W₁))) ((ConcreteCategory.hom (ℱ.map iWX₁.op)) x)) =
        (ConcreteCategory.hom (ℱ'.obj.map iZW₂.op))
          ((ConcreteCategory.hom (α.app (op W₂))) ((ConcreteCategory.hom (ℱ.map iWX₂.op)) x))
Y₁ Y₂ Z : D
iZY₁ : Z ⟶ Y₁
iZY₂ : Z ⟶ Y₂
W₁ : C
iYW₁ : Y₁ ⟶ G.obj W₁
iWX₁ : G.obj W₁ ⟶ X
h₁ : coverByImage G X (iYW₁ ≫ iWX₁)
W₂ : C
iYW₂ : Y₂ ⟶ G.obj W₂
iWX₂ : G.obj W₂ ⟶ X
h₂ : coverByImage G X (iYW₂ ≫ iWX₂)
e : iZY₁ ≫ iYW₁ ≫ iWX₁ = iZY₂ ≫ iYW₂ ≫ iWX₂
⊢ (iZY₁ ≫ { obj := W₁, lift := iYW₁, map := iWX₁, fac := ⋯ }.lift) ≫
      { obj := W₁, lift := iYW₁, map := iWX₁, fac := ⋯ }.map =
    (iZY₂ ≫ { obj := W₂, lift := iYW₂, map := iWX₂, fac := ⋯ }.lift) ≫
      { obj := W₂, lift := iYW₂, map := iWX₂, fac := ⋯ }.map

Tactic:
by simpa only [Category.assoc] using e

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

Goal state before:
pp: case e_a
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
D : Type u_2
inst✝³ : Category.{v_2, u_2} D
K : GrothendieckTopology D
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 : Cᵒᵖ
U : Aᵒᵖ
x✝ : (yoneda.obj ((G.op ⋙ ℱ).obj X)).obj U
Y : D
f : Y ⟶ G.obj (unop X)
hf : (Sieve.coverByImage G (G.obj (unop X))).arrows f
⊢ α.app X ≫ ℱ'.obj.map (Nonempty.some hf).map.op = ℱ.map (Nonempty.some hf).map.op ≫ α.app (op (Nonempty.some hf).1)

Tactic:
simpa using naturality_apply (G := G) (ℱ := ℱ ⋙ coyoneda.obj (op <| (G.op ⋙ ℱ).obj X))
    (ℱ' := ⟨_, Presheaf.isSheaf_comp_of_isSheaf K ℱ'.obj
      (coyoneda.obj (op ((G.op ⋙ ℱ).obj X))) ℱ'.property⟩)
    (whiskerRight α (coyoneda.obj _)) hf.some.map (𝟙 _)

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

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
D : Type u_2
inst✝⁵ : Category.{v_2, u_2} D
E : Type u_3
inst✝⁴ : Category.{v_3, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝³ : Category.{v_4, u_4} A
G : C ⥤ D
inst✝² : G.IsCoverDense K
inst✝¹ : G.IsLocallyFull K
ℱ✝ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
inst✝ : G.IsContinuous J K
ℱ : Sheaf K A
⊢ ∀ {Y : Sheaf K A}, Function.Injective (G.sheafPushforwardContinuous A J K).map

Tactic:
ℱ'

Goal state after:
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
inst✝ : G.IsContinuous J K
ℱ ℱ' : Sheaf K A
⊢ Function.Injective (G.sheafPushforwardContinuous A J K).map
Module: Mathlib.CategoryTheory.Sites.Canonical

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
P✝ : Cᵒᵖ ⥤ Type w
X✝ : C
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type w
X : C
S : Sieve X
hS : S ∈ {S | ∀ (Y : C) (f : Y ⟶ X), Presieve.IsSheafFor P (Sieve.pullback f S).arrows}
R : Sieve X
hR :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    S.arrows f → Sieve.pullback f R ∈ {S | ∀ (Y_1 : C) (f : Y_1 ⟶ Y), Presieve.IsSheafFor P (Sieve.pullback f S).arrows}
Z : C
g : Z ⟶ X
Y : C
f : Y ⟶ Z
hf : (Sieve.pullback g S).arrows f
this : Presieve.IsSheafFor P (Sieve.pullback f (Sieve.pullback g R)).arrows
⊢ Presieve.IsSheafFor P (Sieve.pullback f (Sieve.pullback g R)).arrows

Tactic:
apply this

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

Goal state before:
pp: C : Type u'
inst✝⁴ : Category.{v', u'} C
J : GrothendieckTopology C
R₀ : Cᵒᵖ ⥤ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.obj
inst✝³ : Presheaf.IsLocallyInjective J α
inst✝² : Presheaf.IsLocallySurjective J α
inst✝¹ : J.WEqualsLocallyBijective AddCommGrpCat
inst✝ : HasWeakSheafify J AddCommGrpCat
P Q : PresheafOfModules R₀
f : P ⟶ Q
⊢ IsIso ((presheafToSheaf J Ab).map ((toPresheaf R₀).map f)) ↔
    IsIso ((SheafOfModules.toSheaf R).map ((sheafification α).map f))

Tactic:
exact (isomorphisms _).arrow_mk_iso_iff
    (((Functor.mapArrowFunctor _ _).mapIso (sheafificationCompToSheaf.{v} α)).app (Arrow.mk f))

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
M : SheafOfModules R
⊢ Function.Bijective fun x ↦ pullbackObjUnitToUnit φ ≫ x

Tactic:
← ((pullbackPushforwardAdjunction.{u} φ).homEquiv _ _).bijective.of_comp_iff',

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 (⇑((pullbackPushforwardAdjunction φ).homEquiv (unit S) M) ∘ fun x ↦ pullbackObjUnitToUnit φ ≫ x)
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:
refine or_iff_not_imp_left.mpr fun h => ?_
    rw [IsZero.iff_isSplitMono_eq_zero (biprod.inl : Y ⟶ Y ⊞ Z)] at h
    change biprod.inl ≠ 0 at h
    have : Simple (Y ⊞ Z) := Simple.of_iso i.symm
    rw [← Simple.mono_isIso_iff_nonzero biprod.inl] at h
    rwa [Biprod.isIso_inl_iff_isZero] at h

Goal state after:
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: case mpr.inr
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 : mk f = ⊤
⊢ IsIso f

Tactic:
· exact (Subobject.isIso_iff_mk_eq_top _).mpr h

Goal state after: