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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : FinitaryPreExtensive C
ι : Type u_1
inst✝ : Finite ι
F : Discrete ι ⥤ C
c : Cocone F
hc : IsColimit c
i : Discrete ι
X : C
g : X ⟶ ((Functor.const (Discrete ι)).obj c.pt).obj i
⊢ HasPullback g (c.ι.app i)

Tactic:
let f : ι → C := F.obj ∘ Discrete.mk

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : FinitaryPreExtensive C
ι : Type u_1
inst✝ : Finite ι
F : Discrete ι ⥤ C
c : Cocone F
hc : IsColimit c
i : Discrete ι
X : C
g : X ⟶ ((Functor.const (Discrete ι)).obj c.pt).obj i
f : ι → C := F.obj ∘ Discrete.mk
⊢ HasPullback g (c.ι.app i)
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: J : Type v'
inst✝⁸ : Category.{u', v'} J
C : Type u
inst✝⁷ : Category.{v, u} C
D : Type u_2
inst✝⁶ : Category.{v_2, u_2} D
inst✝⁵ : HasColimitsOfShape J C
Gl : C ⥤ D
Gr : D ⥤ C
adj : Gl ⊣ Gr
inst✝⁴ : Gr.Full
inst✝³ : Gr.Faithful
F : J ⥤ D
c : Cocone (F ⋙ Gr)
H : IsVanKampenColimit c
inst✝² : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), HasPullback (Gr.map f) (adj.unit.app c.pt)
inst✝¹ : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), PreservesLimit (cospan (Gr.map f) (adj.unit.app c.pt)) Gl
inst✝ : ∀ (X : C) (i : J) (f : X ⟶ c.pt), PreservesLimit (cospan f (c.ι.app i)) Gl
this✝ : PreservesLimitsOfSize.{?u.178, ?u.177, v_2, v, u_2, u} Gr
this : PreservesColimitsOfSize.{u', v', v, v_2, u, u_2} Gl
⊢ IsVanKampenColimit (Gl.mapCocone c)

Tactic:
intro F'

Goal state after:
J : Type v'
inst✝⁸ : Category.{u', v'} J
C : Type u
inst✝⁷ : Category.{v, u} C
D : Type u_2
inst✝⁶ : Category.{v_2, u_2} D
inst✝⁵ : HasColimitsOfShape J C
Gl : C ⥤ D
Gr : D ⥤ C
adj : Gl ⊣ Gr
inst✝⁴ : Gr.Full
inst✝³ : Gr.Faithful
F : J ⥤ D
c : Cocone (F ⋙ Gr)
H : IsVanKampenColimit c
inst✝² : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), HasPullback (Gr.map f) (adj.unit.app c.pt)
inst✝¹ : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), PreservesLimit (cospan (Gr.map f) (adj.unit.app c.pt)) Gl
inst✝ : ∀ (X : C) (i : J) (f : X ⟶ c.pt), PreservesLimit (cospan f (c.ι.app i)) Gl
this✝ : PreservesLimitsOfSize.{?u.178, ?u.177, v_2, v, u_2, u} Gr
this : PreservesColimitsOfSize.{u', v', v, v_2, u, u_2} Gl
F' : J ⥤ D
⊢ ∀ (c' : Cocone F') (α : F' ⟶ (F ⋙ Gr) ⋙ Gl) (f : c'.pt ⟶ (Gl.mapCocone c).pt),
    α ≫ (Gl.mapCocone c).ι = c'.ι ≫ (const J).map f →
      NatTrans.Equifibered α →
        (Nonempty (IsColimit c') ↔ ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f ((Gl.mapCocone c).ι.app j))
Module: Mathlib.CategoryTheory.Sites.LeftExact

Goal state before:
pp: C : Type u
inst✝¹⁰ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁹ : Category.{t, w} D
inst✝⁸ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝⁷ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁶ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝⁵ : ConcreteCategory D FD
inst✝⁴ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
inst✝³ : ∀ (X : C), Small.{t, max u v} (J.Cover X)ᵒᵖ
inst✝² : HasFiniteLimits D
inst✝¹ : PreservesFiniteLimits (forget D)
inst✝ : (forget D).ReflectsIsomorphisms
⊢ PreservesFiniteLimits (J.plusFunctor D)

Tactic:
by
  apply preservesFiniteLimits_of_preservesFiniteLimitsOfSize.{t}
  intro K _ _
  have : ReflectsLimitsOfShape K (forget D) := reflectsLimitsOfShape_of_reflectsIsomorphisms
  apply preservesLimitsOfShape_plusFunctor

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

Goal state before:
pp: case fintypeObj
C : Type u
inst✝¹³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝¹² : Category.{t, w} D
inst✝¹¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝¹⁰ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁹ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝⁸ : ConcreteCategory D FD
inst✝⁷ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
inst✝⁶ : (forget D).ReflectsIsomorphisms
inst✝⁵ : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
K : Type w'
inst✝⁴ : SmallCategory K
inst✝³ : FinCategory K
inst✝² : HasLimitsOfShape K D
inst✝¹ : PreservesLimits (forget D)
inst✝ : ∀ (X : C), Small.{t, max u v} (J.Cover X)ᵒᵖ
e : K ≌ AsSmall (FinCategory.AsType K) := ⋯
this : HasLimitsOfShape (AsSmall (FinCategory.AsType K)) D
⊢ autoParam (Fintype (AsSmall (FinCategory.AsType K))) FinCategory.fintypeObj._autoParam

Tactic:
change Fintype (ULift _)
      infer_instance

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

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
X Y : C
c : BinaryCofan X Y
cofans : (X Y : C) → BinaryCofan X Y
colimits : (X Y : C) → IsColimit (cofans X Y)
cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PullbackCone f g
limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → IsLimit (cones f g)
h₁ :
  ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
    αX ≫ c.inl = (cofans X' Y').inl ≫ f →
      αY ≫ c.inr = (cofans X' Y').inr ≫ f →
        IsPullback (cofans X' Y').inl αX f c.inl ∧ IsPullback (cofans X' Y').inr αY f c.inr
h₂ : {Z : C} → (f : Z ⟶ c.pt) → IsColimit (BinaryCofan.mk (cones f c.inl).fst (cones f c.inr).fst)
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ c.inl = c'.inl ≫ f
hY : αY ≫ c.inr = c'.inr ≫ f
H₁ : IsPullback c'.inl αX f c.inl
H₂ : IsPullback c'.inr αY f c.inr
e₁ : X' ≅ (cones f c.inl).pt := H₁.isLimit.conePointUniqueUpToIso (limits f c.inl)
e₂ : Y' ≅ (cones f c.inr).pt := H₂.isLimit.conePointUniqueUpToIso (limits f c.inr)
⊢ IsColimit (BinaryCofan.mk c'.inl c'.inr)

Tactic:
have he₁ : c'.inl = e₁.hom ≫ (cones f c.inl).fst := by simp [e₁]

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
X Y : C
c : BinaryCofan X Y
cofans : (X Y : C) → BinaryCofan X Y
colimits : (X Y : C) → IsColimit (cofans X Y)
cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PullbackCone f g
limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → IsLimit (cones f g)
h₁ :
  ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
    αX ≫ c.inl = (cofans X' Y').inl ≫ f →
      αY ≫ c.inr = (cofans X' Y').inr ≫ f →
        IsPullback (cofans X' Y').inl αX f c.inl ∧ IsPullback (cofans X' Y').inr αY f c.inr
h₂ : {Z : C} → (f : Z ⟶ c.pt) → IsColimit (BinaryCofan.mk (cones f c.inl).fst (cones f c.inr).fst)
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ c.inl = c'.inl ≫ f
hY : αY ≫ c.inr = c'.inr ≫ f
H₁ : IsPullback c'.inl αX f c.inl
H₂ : IsPullback c'.inr αY f c.inr
e₁ : X' ≅ (cones f c.inl).pt := H₁.isLimit.conePointUniqueUpToIso (limits f c.inl)
e₂ : Y' ≅ (cones f c.inr).pt := H₂.isLimit.conePointUniqueUpToIso (limits f c.inr)
he₁ : c'.inl = e₁.hom ≫ (cones f c.inl).fst
⊢ IsColimit (BinaryCofan.mk c'.inl c'.inr)
Module: Mathlib.CategoryTheory.Sites.Localization

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
J : GrothendieckTopology C
D : Type u_3
inst✝¹ : Category.{v_3, u_3} D
K : GrothendieckTopology D
inst✝ : LocallySmall.{w, v_1, u_1} C
F : C ⥤ D
H : (Cᵒᵖ ⥤ Type w) ⥤ Dᵒᵖ ⥤ Type w
adj : H ⊣ (Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ (Type w)).obj F.op
h : ∀ ⦃X : C⦄ ⦃S : Sieve X⦄, S ∈ J X → K.W (H.map (Sieve.shrinkFunctor.{w, v_1, u_1} S).ι)
G : Dᵒᵖ ⥤ Type w
hG : IsSheaf K G
X : C
S : Sieve X
hS : S ∈ J X
⊢ Presheaf.IsSheaf K G

Tactic:
rwa [isSheaf_iff_isSheaf_of_type]

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

Goal state before:
pp: case mp.refine_1
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst✝¹ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝ : ConcreteCategory D FD
J : GrothendieckTopology C
F₁ F₂ : Cᵒᵖ ⥤ D
φ : F₁ ⟶ F₂
a✝ : IsLocallyInjective J φ
X : Cᵒᵖ
x y : ToType (F₁.obj X)
h : equalizerSieve ((ConcreteCategory.hom (φ.app X)) x) ((ConcreteCategory.hom (φ.app X)) y) ∈ J (unop X)
S : Sieve (unop X) := equalizerSieve ((ConcreteCategory.hom (φ.app X)) x) ((ConcreteCategory.hom (φ.app X)) y)
T : ⦃Y : C⦄ → ⦃f : Y ⟶ unop X⦄ → S.arrows f → Sieve Y :=
  fun Y f x_1 ↦ equalizerSieve ((ConcreteCategory.hom (F₁.map f.op)) x) ((ConcreteCategory.hom (F₁.map f.op)) y)
⊢ Sieve.bind S.arrows T ≤ equalizerSieve x y

pp: case mp.refine_2
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst✝¹ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝ : ConcreteCategory D FD
J : GrothendieckTopology C
F₁ F₂ : Cᵒᵖ ⥤ D
φ : F₁ ⟶ F₂
a✝ : IsLocallyInjective J φ
X : Cᵒᵖ
x y : ToType (F₁.obj X)
h : equalizerSieve ((ConcreteCategory.hom (φ.app X)) x) ((ConcreteCategory.hom (φ.app X)) y) ∈ J (unop X)
S : Sieve (unop X) := equalizerSieve ((ConcreteCategory.hom (φ.app X)) x) ((ConcreteCategory.hom (φ.app X)) y)
T : ⦃Y : C⦄ → ⦃f : Y ⟶ unop X⦄ → S.arrows f → Sieve Y :=
  fun Y f x_1 ↦ equalizerSieve ((ConcreteCategory.hom (F₁.map f.op)) x) ((ConcreteCategory.hom (F₁.map f.op)) y)
⊢ ∀ ⦃Y : C⦄ ⦃f : Y ⟶ unop X⦄,
    (equalizerSieve ((ConcreteCategory.hom (φ.app X)) x) ((ConcreteCategory.hom (φ.app X)) y)).arrows f →
      Sieve.pullback f (Sieve.bind S.arrows T) ∈ J Y

Tactic:
· rintro Y f ⟨Z, a, g, hg, ha, rfl⟩
      simpa using! ha

Goal state after:
case mp.refine_2
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst✝¹ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝ : ConcreteCategory D FD
J : GrothendieckTopology C
F₁ F₂ : Cᵒᵖ ⥤ D
φ : F₁ ⟶ F₂
a✝ : IsLocallyInjective J φ
X : Cᵒᵖ
x y : ToType (F₁.obj X)
h : equalizerSieve ((ConcreteCategory.hom (φ.app X)) x) ((ConcreteCategory.hom (φ.app X)) y) ∈ J (unop X)
S : Sieve (unop X) := equalizerSieve ((ConcreteCategory.hom (φ.app X)) x) ((ConcreteCategory.hom (φ.app X)) y)
T : ⦃Y : C⦄ → ⦃f : Y ⟶ unop X⦄ → S.arrows f → Sieve Y :=
  fun Y f x_1 ↦ equalizerSieve ((ConcreteCategory.hom (F₁.map f.op)) x) ((ConcreteCategory.hom (F₁.map f.op)) y)
⊢ ∀ ⦃Y : C⦄ ⦃f : Y ⟶ unop X⦄,
    (equalizerSieve ((ConcreteCategory.hom (φ.app X)) x) ((ConcreteCategory.hom (φ.app X)) y)).arrows f →
      Sieve.pullback f (Sieve.bind S.arrows T) ∈ J Y
Module: Mathlib.CategoryTheory.Sites.LocallyBijective

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type w)
f : F ⟶ G
h₁ : ∀ (X : Cᵒᵖ), Function.Injective ⇑(ConcreteCategory.hom (f.hom.app X))
right✝ : IsLocallySurjective f
this : ∀ (X : Cᵒᵖ), Function.Surjective ⇑(ConcreteCategory.hom (f.hom.app X))
X : Cᵒᵖ
⊢ Function.Bijective ⇑(ConcreteCategory.hom (((sheafToPresheaf J (Type w)).map f).app X))

Tactic:
exact ⟨h₁ X, this X⟩

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

Goal state before:
pp: C : Type u
inst✝¹⁰ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝⁹ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst✝⁸ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝⁷ : ConcreteCategory A FA
D : Type w
inst✝⁶ : Category.{w', w} D
FD : D → D → Type u_2
CD : D → Type (max u v)
inst✝⁵ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝⁴ : ConcreteCategory D FD
inst✝³ : HasWeakSheafify J D
inst✝² : J.HasSheafCompose (forget D)
inst✝¹ : J.PreservesSheafification (forget D)
inst✝ : (forget D).ReflectsIsomorphisms
⊢ J.WEqualsLocallyBijective D

Tactic:
by
  apply WEqualsLocallyBijective.mk'

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasInitial C
ι : Type u_3
F : Discrete ι ⥤ C
c : Cocone F
hc : IsVanKampenColimit c
i j : Discrete ι
hi : i ≠ j
⊢ IsPullback (initial.to (F.obj i)) (initial.to (F.obj j)) (c.ι.app i) (c.ι.app j)

Tactic:
let f : ι → C := F.obj ∘ Discrete.mk

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasInitial C
ι : Type u_3
F : Discrete ι ⥤ C
c : Cocone F
hc : IsVanKampenColimit c
i j : Discrete ι
hi : i ≠ j
f : ι → C := F.obj ∘ Discrete.mk
⊢ IsPullback (initial.to (F.obj i)) (initial.to (F.obj j)) (c.ι.app i) (c.ι.app j)
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasInitial C
ι : Type u_3
F : Discrete ι ⥤ C
c : Cocone F
hc : IsVanKampenColimit c
i : Discrete ι
⊢ Mono (c.ι.app i)

Tactic:
let f : ι → C := F.obj ∘ Discrete.mk

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasInitial C
ι : Type u_3
F : Discrete ι ⥤ C
c : Cocone F
hc : IsVanKampenColimit c
i : Discrete ι
f : ι → C := F.obj ∘ Discrete.mk
⊢ Mono (c.ι.app i)
Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
⊢ Projective X ↔ HasProjectiveDimensionLT X 1

Tactic:
let := HasExt.standard C
  exact ⟨fun _ ↦ inferInstance, fun _ ↦ projective_iff_subsingleton_ext_one.2
    (HasProjectiveDimensionLT.subsingleton X 1 1 (by rfl))⟩

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension

Goal state before:
pp: case succ
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
inst✝ : EnoughInjectives C
X : C
n : ℕ
hX : ∀ (Y : C), Subsingleton (Ext X Y n)
k : ℕ
hk : ∀ ⦃d : ℕ⦄ ⦃Y : C⦄ (e : Ext X Y d), d = n + k → e = 0
d : ℕ
Y : C
e : Ext X Y d
hd : d = n + (k + 1)
⊢ e = 0

Tactic:
let ⟨p⟩ := EnoughInjectives.presentation Y
    have h : (ShortComplex.mk _ _ (cokernel.condition p.f)).ShortExact :=
      { exact := ShortComplex.exact_cokernel p.f }
    have hd : n + k + 1 = d := by lia
    obtain ⟨x, rfl⟩ := Ext.covariant_sequence_exact₁ X h e
      (by subst hd; apply Ext.eq_zero_of_injective) hd
    simp [hk x rfl]

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

Goal state before:
pp: case left_id
J : Type v₁
inst✝¹ : SmallCategory J
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : J ⥤ C
c₁ c₂ : Cone F
⊢ (Bicone.casesOn Bicone.left c₁.pt c₂.pt fun j ↦ F.obj j) ⟶ Bicone.casesOn Bicone.left c₁.pt c₂.pt fun j ↦ F.obj j

pp: case right_id
J : Type v₁
inst✝¹ : SmallCategory J
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : J ⥤ C
c₁ c₂ : Cone F
⊢ (Bicone.casesOn Bicone.right c₁.pt c₂.pt fun j ↦ F.obj j) ⟶ Bicone.casesOn Bicone.right c₁.pt c₂.pt fun j ↦ F.obj j

pp: case left
J : Type v₁
inst✝¹ : SmallCategory J
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : J ⥤ C
c₁ c₂ : Cone F
j✝ : J
⊢ (Bicone.casesOn Bicone.left c₁.pt c₂.pt fun j ↦ F.obj j) ⟶
    Bicone.casesOn (Bicone.diagram j✝) c₁.pt c₂.pt fun j ↦ F.obj j

pp: case right
J : Type v₁
inst✝¹ : SmallCategory J
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : J ⥤ C
c₁ c₂ : Cone F
j✝ : J
⊢ (Bicone.casesOn Bicone.right c₁.pt c₂.pt fun j ↦ F.obj j) ⟶
    Bicone.casesOn (Bicone.diagram j✝) c₁.pt c₂.pt fun j ↦ F.obj j

pp: case diagram
J : Type v₁
inst✝¹ : SmallCategory J
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : J ⥤ C
c₁ c₂ : Cone F
j✝ k✝ : J
f : j✝ ⟶ k✝
⊢ (Bicone.casesOn (Bicone.diagram j✝) c₁.pt c₂.pt fun j ↦ F.obj j) ⟶
    Bicone.casesOn (Bicone.diagram k✝) c₁.pt c₂.pt fun j ↦ F.obj j

Tactic:
· exact 𝟙 _

Goal state after:
case right_id
J : Type v₁
inst✝¹ : SmallCategory J
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : J ⥤ C
c₁ c₂ : Cone F
⊢ (Bicone.casesOn Bicone.right c₁.pt c₂.pt fun j ↦ F.obj j) ⟶ Bicone.casesOn Bicone.right c₁.pt c₂.pt fun j ↦ F.obj j

case left
J : Type v₁
inst✝¹ : SmallCategory J
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : J ⥤ C
c₁ c₂ : Cone F
j✝ : J
⊢ (Bicone.casesOn Bicone.left c₁.pt c₂.pt fun j ↦ F.obj j) ⟶
    Bicone.casesOn (Bicone.diagram j✝) c₁.pt c₂.pt fun j ↦ F.obj j

case right
J : Type v₁
inst✝¹ : SmallCategory J
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : J ⥤ C
c₁ c₂ : Cone F
j✝ : J
⊢ (Bicone.casesOn Bicone.right c₁.pt c₂.pt fun j ↦ F.obj j) ⟶
    Bicone.casesOn (Bicone.diagram j✝) c₁.pt c₂.pt fun j ↦ F.obj j

case diagram
J : Type v₁
inst✝¹ : SmallCategory J
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : J ⥤ C
c₁ c₂ : Cone F
j✝ k✝ : J
f : j✝ ⟶ k✝
⊢ (Bicone.casesOn (Bicone.diagram j✝) c₁.pt c₂.pt fun j ↦ F.obj j) ⟶
    Bicone.casesOn (Bicone.diagram k✝) c₁.pt c₂.pt fun j ↦ F.obj j
Module: Mathlib.CategoryTheory.Limits.Bicones

Goal state before:
pp: case right_id
J : Type v₁
inst✝¹ : SmallCategory J
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : J ⥤ C
c₁ c₂ : Cone F
⊢ (Bicone.casesOn Bicone.right c₁.pt c₂.pt fun j ↦ F.obj j) ⟶ Bicone.casesOn Bicone.right c₁.pt c₂.pt fun j ↦ F.obj j

pp: case left
J : Type v₁
inst✝¹ : SmallCategory J
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : J ⥤ C
c₁ c₂ : Cone F
j✝ : J
⊢ (Bicone.casesOn Bicone.left c₁.pt c₂.pt fun j ↦ F.obj j) ⟶
    Bicone.casesOn (Bicone.diagram j✝) c₁.pt c₂.pt fun j ↦ F.obj j

pp: case right
J : Type v₁
inst✝¹ : SmallCategory J
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : J ⥤ C
c₁ c₂ : Cone F
j✝ : J
⊢ (Bicone.casesOn Bicone.right c₁.pt c₂.pt fun j ↦ F.obj j) ⟶
    Bicone.casesOn (Bicone.diagram j✝) c₁.pt c₂.pt fun j ↦ F.obj j

pp: case diagram
J : Type v₁
inst✝¹ : SmallCategory J
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : J ⥤ C
c₁ c₂ : Cone F
j✝ k✝ : J
f : j✝ ⟶ k✝
⊢ (Bicone.casesOn (Bicone.diagram j✝) c₁.pt c₂.pt fun j ↦ F.obj j) ⟶
    Bicone.casesOn (Bicone.diagram k✝) c₁.pt c₂.pt fun j ↦ F.obj j

Tactic:
· exact 𝟙 _

Goal state after:
case left
J : Type v₁
inst✝¹ : SmallCategory J
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : J ⥤ C
c₁ c₂ : Cone F
j✝ : J
⊢ (Bicone.casesOn Bicone.left c₁.pt c₂.pt fun j ↦ F.obj j) ⟶
    Bicone.casesOn (Bicone.diagram j✝) c₁.pt c₂.pt fun j ↦ F.obj j

case right
J : Type v₁
inst✝¹ : SmallCategory J
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : J ⥤ C
c₁ c₂ : Cone F
j✝ : J
⊢ (Bicone.casesOn Bicone.right c₁.pt c₂.pt fun j ↦ F.obj j) ⟶
    Bicone.casesOn (Bicone.diagram j✝) c₁.pt c₂.pt fun j ↦ F.obj j

case diagram
J : Type v₁
inst✝¹ : SmallCategory J
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : J ⥤ C
c₁ c₂ : Cone F
j✝ k✝ : J
f : j✝ ⟶ k✝
⊢ (Bicone.casesOn (Bicone.diagram j✝) c₁.pt c₂.pt fun j ↦ F.obj j) ⟶
    Bicone.casesOn (Bicone.diagram k✝) c₁.pt c₂.pt fun j ↦ F.obj j
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 (φ.app (Opposite.op Y))) (r₀ • m₀) + (ConcreteCategory.hom (φ.app (Opposite.op Y))) (r₀ • m₀')

Tactic:
map_smul_eq α φ r (m + m') f.op r₀ hr₀ (m₀ + m₀')
      (by rw [_root_.map_add, _root_.map_add, hm₀, hm₀']),

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 (φ.app (Opposite.op Y))) (r₀ • (m₀ + m₀')) =
    (ConcreteCategory.hom (φ.app (Opposite.op Y))) (r₀ • m₀) + (ConcreteCategory.hom (φ.app (Opposite.op Y))) (r₀ • m₀')
Module: Mathlib.CategoryTheory.Limits.Preserves.Opposites

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : Cᵒᵖ ⥤ D
inst✝ : ReflectsFiniteCoproducts F
x✝ : ℕ
⊢ ReflectsLimitsOfShape (Discrete (Fin x✝)) F.rightOp

Tactic:
apply +allowSynthFailures reflectsLimitsOfShape_rightOp

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : Cᵒᵖ ⥤ D
inst✝ : ReflectsFiniteCoproducts F
x✝ : ℕ
⊢ ReflectsColimitsOfShape (Discrete (Fin x✝))ᵒᵖ F
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 φ
⊢ IsLocallyInjective J (toSheafify α φ)

Tactic:
dsimp [IsLocallyInjective]; infer_instance

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

Goal state before:
pp: case mpr.a
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
h : ∀ (P : Cᵒᵖ ⥤ Type (max v u)), Presieve.IsSheaf J₁ P ↔ Presieve.IsSheaf J₂ P
⊢ J₁ ≤ J₂

pp: case a
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
h : ∀ (P : Cᵒᵖ ⥤ Type (max v u)), Presieve.IsSheaf J₁ P ↔ Presieve.IsSheaf J₂ P
⊢ J₂ ≤ J₁

Tactic:
· apply le_topology_of_closedSieves_isSheaf
      rw [h]
      apply classifier_isSheaf

Goal state after:
case a
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
h : ∀ (P : Cᵒᵖ ⥤ Type (max v u)), Presieve.IsSheaf J₁ P ↔ Presieve.IsSheaf J₂ P
⊢ J₂ ≤ J₁
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreZeroHypercover S
F : PreZeroHypercover S
f g : E.Hom F
hs : f.s₀ = g.s₀
hh : ∀ (i : E.I₀), f.h₀ i = g.h₀ i ≫ eqToHom ⋯
⊢ f = g

Tactic:
by
  cases f
  cases g
  simp only at hs
  cat_disch

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

Goal state before:
pp: case refine_1.pullback
C : Type u_2
inst✝ : Category.{u_1, u_2} C
J : Precoverage C
K : GrothendieckTopology C
hK : K ∈ {K | ∀ ⦃X : C⦄, ∀ S ∈ J.coverings X, Sieve.generate S ∈ K X}
i✝ : C
a✝¹ : Sieve i✝
X✝ : C
S✝ : Sieve X✝
a✝ : J.Saturate X✝ S✝
Y✝ : C
f✝ : Y✝ ⟶ X✝
ih : S✝ ∈ K X✝
⊢ Sieve.pullback f✝ S✝ ∈ K Y✝

Tactic:
exact K.pullback_stable _ ih

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

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_3, u_3} E
F : C ⥤ D
G : D ⥤ E
X : E
inst✝¹ : RepresentablyFlat F
inst✝ : IsCofiltered (StructuredArrow X G)
T : StructuredArrow X (F ⋙ G) ⥤ StructuredArrow X G := StructuredArrow.pre X F G
Y : StructuredArrow X G
⊢ IsCofiltered (StructuredArrow X (F ⋙ G))

Tactic:
obtain ⟨A⟩ := IsCofiltered.nonempty (C := StructuredArrow Y.right F)

Goal state after:
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_3, u_3} E
F : C ⥤ D
G : D ⥤ E
X : E
inst✝¹ : RepresentablyFlat F
inst✝ : IsCofiltered (StructuredArrow X G)
T : StructuredArrow X (F ⋙ G) ⥤ StructuredArrow X G := StructuredArrow.pre X F G
Y : StructuredArrow X G
A : StructuredArrow Y.right F
⊢ IsCofiltered (StructuredArrow X (F ⋙ G))