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

Goal state before:
pp: case fintypeHom
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 ((j j' : AsSmall (FinCategory.AsType K)) → Fintype (j ⟶ j')) FinCategory.fintypeHom._autoParam

Tactic:
· intro j j'
      change Fintype (ULift _)
      infer_instance

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

Goal state before:
pp: case e'_2.e'_6
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)
P : Cᵒᵖ ⥤ D
e_1✝ : (P ⟶ sheafify J P) = ((𝟭 (Cᵒᵖ ⥤ D)).obj P ⟶ (sheafToPresheaf J D).obj ((presheafToSheaf J D).obj P))
e_3✝ : P = (𝟭 (Cᵒᵖ ⥤ D)).obj P
e_4✝ : J.sheafify P = (plusPlusSheaf J D ⋙ sheafToPresheaf J D).obj P
⊢ J.toSheafify = (plusPlusAdjunction J D).unit.app

Tactic:
ext1 P

Goal state after:
case e'_2.e'_6
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)
P✝ : Cᵒᵖ ⥤ D
e_1✝ : (P✝ ⟶ sheafify J P✝) = ((𝟭 (Cᵒᵖ ⥤ D)).obj P✝ ⟶ (sheafToPresheaf J D).obj ((presheafToSheaf J D).obj P✝))
e_3✝ : P✝ = (𝟭 (Cᵒᵖ ⥤ D)).obj P✝
e_4✝ : J.sheafify P✝ = (plusPlusSheaf J D ⋙ sheafToPresheaf J D).obj P✝
P : Cᵒᵖ ⥤ D
⊢ J.toSheafify P = (plusPlusAdjunction J D).unit.app P
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasInitial C
H : IsUniversalColimit (BinaryCofan.mk (𝟙 (⊥_ C)) (𝟙 (⊥_ C)))
A : C
f : A ⟶ ⊥_ C
this : IsColimit (BinaryCofan.mk (𝟙 A) (𝟙 A))
h₁ : (BinaryCofan.mk (𝟙 A) (𝟙 A)).inl ≫ 𝟙 A = f ≫ initial.to A
h₂ : (BinaryCofan.mk (𝟙 A) (𝟙 A)).inr ≫ 𝟙 A = 𝟙 A
⊢ IsIso f

Tactic:
exact ⟨⟨_, ((Category.id_comp _).symm.trans h₁).symm, initialIsInitial.hom_ext _ _⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Adjunction

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} D₁
inst✝⁴ : Category.{v_4, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝³ : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : L₂.IsLocalization W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
inst✝¹ : CatCommSq G L₁ L₂ G'
inst✝ : CatCommSq F L₂ L₁ F'
X₁ : C₁
eq : G.map (adj.unit.app X₁) ≫ adj.counit.app (G.obj X₁) = 𝟙 (G.obj X₁)
⊢ (CatCommSq.iso G L₁ L₂ G').inv.app ((𝟭 C₁).obj X₁) ≫
      (G ⋙ L₂).map (adj.unit.app X₁) ≫
        L₂.map (adj.counit.app (G.obj X₁)) ≫ (𝟭 D₂).map ((CatCommSq.iso G L₁ L₂ G').hom.app X₁) =
    (NatTrans.id (𝟭 D₁ ⋙ G')).app (L₁.obj X₁)

Tactic:
← L₂.map_comp_assoc,

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} D₁
inst✝⁴ : Category.{v_4, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝³ : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : L₂.IsLocalization W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
inst✝¹ : CatCommSq G L₁ L₂ G'
inst✝ : CatCommSq F L₂ L₁ F'
X₁ : C₁
eq : G.map (adj.unit.app X₁) ≫ adj.counit.app (G.obj X₁) = 𝟙 (G.obj X₁)
⊢ (CatCommSq.iso G L₁ L₂ G').inv.app ((𝟭 C₁).obj X₁) ≫
      L₂.map (G.map (adj.unit.app X₁) ≫ adj.counit.app (G.obj X₁)) ≫
        (𝟭 D₂).map ((CatCommSq.iso G L₁ L₂ G').hom.app X₁) =
    (NatTrans.id (𝟭 D₁ ⋙ G')).app (L₁.obj X₁)
Module: Mathlib.CategoryTheory.Localization.Bousfield

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
G : D ⥤ C
adj : G ⊣ F
inst✝¹ : F.Full
inst✝ : F.Faithful
P₁ P₂ : D
f : P₁ ⟶ P₂
⊢ isLocal (fun x ↦ x ∈ Set.range F.obj) f ↔ (MorphismProperty.isomorphisms C).inverseImage G f

Tactic:
isLocal_iff_isIso_map adj

Goal state after:
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
G : D ⥤ C
adj : G ⊣ F
inst✝¹ : F.Full
inst✝ : F.Faithful
P₁ P₂ : D
f : P₁ ⟶ P₂
⊢ IsIso (G.map f) ↔ (MorphismProperty.isomorphisms C).inverseImage G f
Module: Mathlib.CategoryTheory.Localization.Bousfield

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
G : D ⥤ C
adj : G ⊣ F
inst✝¹ : F.Full
inst✝ : F.Faithful
⊢ G.IsLocalization (isLocal fun x ↦ x ∈ Set.range F.obj)

Tactic:
by
  rw [isLocal_eq_inverseImage_isomorphisms adj]
  exact adj.isLocalization

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

Goal state before:
pp: 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₂ : Sheaf J D
φ : F₁ ⟶ F₂
inst✝ : J.HasSheafCompose (forget D)
F G : Sheaf J (Type w)
f : F ⟶ G
⊢ IsLocallyInjective (imageι f)

Tactic:
by
  dsimp [Sheaf.imageι]
  infer_instance

Goal state after:
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
X : Cᵒᵖ
s : G.obj.obj X
H : Presieve.IsSheafFor F.obj (Presheaf.imageSieve f.hom s).arrows
t : Presieve.FamilyOfElements F.obj (Presheaf.imageSieve f.hom s).arrows :=
  fun Y g hg ↦ Presheaf.localPreimage f.hom s g hg
Y₁ Y₂ W : C
g₁ : W ⟶ Y₁
g₂ : W ⟶ Y₂
f₁ : Y₁ ⟶ Opposite.unop X
f₂ : Y₂ ⟶ Opposite.unop X
hf₁ : (Presheaf.imageSieve f.hom s).arrows f₁
hf₂ : (Presheaf.imageSieve f.hom s).arrows f₂
w : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ (ConcreteCategory.hom (F.obj.map g₁.op)) (t f₁ hf₁) = (ConcreteCategory.hom (F.obj.map g₂.op)) (t f₂ hf₂)

Tactic:
apply h₁

Goal state after:
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
X : Cᵒᵖ
s : G.obj.obj X
H : Presieve.IsSheafFor F.obj (Presheaf.imageSieve f.hom s).arrows
t : Presieve.FamilyOfElements F.obj (Presheaf.imageSieve f.hom s).arrows := ⋯
Y₁ Y₂ W : C
g₁ : W ⟶ Y₁
g₂ : W ⟶ Y₂
f₁ : Y₁ ⟶ Opposite.unop X
f₂ : Y₂ ⟶ Opposite.unop X
hf₁ : (Presheaf.imageSieve f.hom s).arrows f₁
hf₂ : (Presheaf.imageSieve f.hom s).arrows f₂
w : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ (ConcreteCategory.hom (f.hom.app (Opposite.op W))) ((ConcreteCategory.hom (F.obj.map g₁.op)) (t f₁ hf₁)) =
    (ConcreteCategory.hom (f.hom.app (Opposite.op W))) ((ConcreteCategory.hom (F.obj.map g₂.op)) (t f₂ hf₂))
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
inst✝⁴ : HasWeakSheafify J A
inst✝³ : (forget A).ReflectsIsomorphisms
inst✝² : J.HasSheafCompose (forget A)
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ A), Presheaf.IsLocallyInjective J (CategoryTheory.toSheafify J P)
inst✝ : ∀ (P : Cᵒᵖ ⥤ A), Presheaf.IsLocallySurjective J (CategoryTheory.toSheafify J P)
P Q : Cᵒᵖ ⥤ A
f : P ⟶ Q
⊢ Sheaf.IsLocallyInjective ((presheafToSheaf J A).map f) ∧ Sheaf.IsLocallySurjective ((presheafToSheaf J A).map f) ↔
    Presheaf.IsLocallyInjective J (f ≫ CategoryTheory.toSheafify J Q) ∧
      Presheaf.IsLocallySurjective J (f ≫ CategoryTheory.toSheafify J Q)

Tactic:
CategoryTheory.toSheafify_naturality,

Goal state after:
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
inst✝⁴ : HasWeakSheafify J A
inst✝³ : (forget A).ReflectsIsomorphisms
inst✝² : J.HasSheafCompose (forget A)
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ A), Presheaf.IsLocallyInjective J (CategoryTheory.toSheafify J P)
inst✝ : ∀ (P : Cᵒᵖ ⥤ A), Presheaf.IsLocallySurjective J (CategoryTheory.toSheafify J P)
P Q : Cᵒᵖ ⥤ A
f : P ⟶ Q
⊢ Sheaf.IsLocallyInjective ((presheafToSheaf J A).map f) ∧ Sheaf.IsLocallySurjective ((presheafToSheaf J A).map f) ↔
    Presheaf.IsLocallyInjective J (CategoryTheory.toSheafify J P ≫ CategoryTheory.sheafifyMap J f) ∧
      Presheaf.IsLocallySurjective J (CategoryTheory.toSheafify J P ≫ CategoryTheory.sheafifyMap J f)
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Submodule

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M : PresheafOfModules R
N₁ N₂ : M.Submodule
h : ∀ (X : Cᵒᵖ), N₁.obj X = N₂.obj X
⊢ N₁ = N₂

Tactic:
cases N₁; cases N₂; congr 1; ext X : 1; exact h X

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
hX : IsZero X
this : HasExt C := HasExt.standard C
i : ℕ
hi : 0 ≤ i
Y : C
e : Ext X Y i
⊢ e = 0

Tactic:
← e.mk₀_id_comp,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
hX : IsZero X
this : HasExt C := HasExt.standard C
i : ℕ
hi : 0 ≤ i
Y : C
e : Ext X Y i
⊢ (Ext.mk₀ (𝟙 X)).comp e ⋯ = 0
Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X : C
inst✝ : HasProjectiveDimensionLT X 0
⊢ IsZero X

Tactic:
let := HasExt.standard C
  rw [IsZero.iff_id_eq_zero]
  apply Ext.homEquiv₀.symm.injective
  simpa only [Ext.homEquiv₀_symm_apply, Ext.mk₀_zero]
    using Abelian.Ext.eq_zero_of_hasProjectiveDimensionLT _ 0 (by rfl)

Goal state after:
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✝ : PreservesFiniteProducts F
x✝ : ℕ
⊢ PreservesColimitsOfShape (Discrete (Fin x✝)) F.op

Tactic:
apply +allowSynthFailures preservesColimitsOfShape_op

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

Tactic:
apply +allowSynthFailures reflectsColimitsOfShape_unop

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : Cᵒᵖ ⥤ Dᵒᵖ
inst✝ : ReflectsFiniteProducts F
x✝ : ℕ
⊢ ReflectsLimitsOfShape (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 φ
X : Cᵒᵖ
r r' : ↑(R.obj.obj X)
m : ↑(A.obj.obj X)
⊢ smul α φ (r + r') m = smul α φ r m + smul α φ r' m

Tactic:
by
  let S := Presheaf.imageSieve α r ⊓ Presheaf.imageSieve α r' ⊓ Presheaf.imageSieve φ m
  have hS : S ∈ J X.unop := by
    refine J.intersection_covering (J.intersection_covering ?_ ?_) ?_
    all_goals apply Presheaf.imageSieve_mem
  apply A.isSeparated _ _ hS
  rintro Y f ⟨⟨⟨r₀ : R₀.obj _, (hr₀ : (α.app (Opposite.op Y)) r₀ = (R.obj.map f.op) r)⟩,
    ⟨r₀' : R₀.obj _, (hr₀' : (α.app (Opposite.op Y)) r₀' = (R.obj.map f.op) r')⟩⟩, ⟨m₀, hm₀⟩⟩
  rw [(A.obj.map f.op).hom.map_add, map_smul_eq α φ r m f.op r₀ hr₀ m₀ hm₀,
    map_smul_eq α φ r' m f.op r₀' hr₀' m₀ hm₀,
    map_smul_eq α φ (r + r') m f.op (r₀ + r₀') (by rw [_root_.map_add, _root_.map_add, hr₀, hr₀'])
      m₀ hm₀, add_smul, _root_.map_add]

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
F : C ⥤ D
inst✝ : RepresentablyFlat F
J : Type ?u.26
𝒥✝ : SmallCategory J
x✝ : FinCategory J
K : J ⥤ C
c : Cone K
⊢ ∀ (hc : IsLimit c), Nonempty (IsLimit (F.mapCone c))

Tactic:
hc

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : RepresentablyFlat F
J : Type ?u.26
𝒥✝ : SmallCategory J
x✝ : FinCategory J
K : J ⥤ C
c : Cone K
hc : IsLimit c
⊢ Nonempty (IsLimit (F.mapCone c))
Module: Mathlib.CategoryTheory.Sites.Closed

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X : C
S : Sieve X
H : Presieve.IsSheafFor (Functor.closedSieves J).toFunctor S.arrows
this✝ : J.IsClosed ⊤
this : ⟨J.close S, ⋯⟩ = ⟨⊤, this✝⟩
⊢ J.close S = ⊤

Tactic:
by
    rw [Subtype.ext_iff] at this
    exact this

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

Goal state before:
pp: case refine_1.transitive.refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
J : Pretopology C
T : C
S✝ : Sieve T
X : C
R S : Sieve X
hR : J.toCoverage.Saturate X R
hRS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → J.toCoverage.Saturate Y (Sieve.pullback f S)
R' : Presieve X
hR' : R' ∈ J.coverings X
hle : R' ≤ R.arrows
S' : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → R.arrows f → Presieve Y
hS' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (a : R.arrows f), S' a ∈ J.coverings Y
hS'le : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (a : R.arrows f), S' a ≤ (Sieve.pullback f S).arrows
Z : C
u : Z ⟶ X
hu : R'.bind (fun Y f hf ↦ S' ⋯) u
⊢ S.arrows u

Tactic:
obtain ⟨W, g, w, hw, hg, rfl⟩ := hu

Goal state after:
case refine_1.transitive.refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
J : Pretopology C
T : C
S✝ : Sieve T
X : C
R S : Sieve X
hR : J.toCoverage.Saturate X R
hRS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → J.toCoverage.Saturate Y (Sieve.pullback f S)
R' : Presieve X
hR' : R' ∈ J.coverings X
hle : R' ≤ R.arrows
S' : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → R.arrows f → Presieve Y
hS' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (a : R.arrows f), S' a ∈ J.coverings Y
hS'le : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (a : R.arrows f), S' a ≤ (Sieve.pullback f S).arrows
Z W : C
g : Z ⟶ W
w : W ⟶ X
hw : R' w
hg : S' ⋯ g
⊢ S.arrows (g ≫ w)
Module: Mathlib.CategoryTheory.Sites.Continuous

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
F₂ : D ⥤ E
F₁₂ : C ⥤ E
e : F₁ ⋙ F₂ ≅ F₁₂
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
inst✝¹ : F₁.IsContinuous J K
inst✝ : F₂.IsContinuous K L
⊢ F₁₂.IsContinuous J L

Tactic:
have := Functor.isContinuous_comp F₁ F₂ J K L
  apply Functor.isContinuous_of_iso e

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

Goal state before:
pp: case refine_1
C : Type u
inst✝³ : Category.{v, u} C
A : Type u_1
inst✝² : Category.{v_1, u_1} A
S : C
E : PreOneHypercover S
c : Cofan E.X
hc : IsColimit c
d : Cofan E.Y'
hd : IsColimit d
F : Cᵒᵖ ⥤ A
inst✝¹ : PreservesLimit (Discrete.functor fun i ↦ op (E.X i)) F
inst✝ : PreservesLimit (Discrete.functor fun i ↦ op (E.Y' i)) F
c' : Fan (E.multicospanIndex F).left := Fan.mk (F.obj (op c.pt)) fun i ↦ F.map (c.inj i).op
hc' : IsLimit c' := isLimitFanMkObjOfIsLimit F (fun i ↦ op (E.X i)) (fun i ↦ (c.inj i).op) (Cofan.IsColimit.op hc)
d' : Fan (E.multicospanIndex F).right := Fan.mk (F.obj (op d.pt)) fun i ↦ F.map (d.inj i).op
hd' : IsLimit d' := isLimitFanMkObjOfIsLimit F (fun i ↦ op (E.Y' i)) (fun i ↦ (d.inj i).op) (Cofan.IsColimit.op hd)
⊢ (Iso.refl c'.pt).hom ≫ F.map (Cofan.IsColimit.desc hd fun x ↦ E.p₁ x.snd ≫ c.inj x.fst.1).op =
    (E.multicospanIndex F).fstPiMapOfIsLimit c' hd' ≫ (Iso.refl d'.pt).hom

Tactic:
refine Fan.IsLimit.hom_ext hd' _ _ fun i ↦ ?_

Goal state after:
case refine_1
C : Type u
inst✝³ : Category.{v, u} C
A : Type u_1
inst✝² : Category.{v_1, u_1} A
S : C
E : PreOneHypercover S
c : Cofan E.X
hc : IsColimit c
d : Cofan E.Y'
hd : IsColimit d
F : Cᵒᵖ ⥤ A
inst✝¹ : PreservesLimit (Discrete.functor fun i ↦ op (E.X i)) F
inst✝ : PreservesLimit (Discrete.functor fun i ↦ op (E.Y' i)) F
c' : Fan (E.multicospanIndex F).left := Fan.mk (F.obj (op c.pt)) fun i ↦ F.map (c.inj i).op
hc' : IsLimit c' := isLimitFanMkObjOfIsLimit F (fun i ↦ op (E.X i)) (fun i ↦ (c.inj i).op) (Cofan.IsColimit.op hc)
d' : Fan (E.multicospanIndex F).right := Fan.mk (F.obj (op d.pt)) fun i ↦ F.map (d.inj i).op
hd' : IsLimit d' := isLimitFanMkObjOfIsLimit F (fun i ↦ op (E.Y' i)) (fun i ↦ (d.inj i).op) (Cofan.IsColimit.op hd)
i : E.multicospanShape.R
⊢ ((Iso.refl c'.pt).hom ≫ F.map (Cofan.IsColimit.desc hd fun x ↦ E.p₁ x.snd ≫ c.inj x.fst.1).op) ≫ d'.proj i =
    ((E.multicospanIndex F).fstPiMapOfIsLimit c' hd' ≫ (Iso.refl d'.pt).hom) ≫ d'.proj i
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: case refine_2
C : Type u
inst✝³ : Category.{v, u} C
A : Type u_1
inst✝² : Category.{v_1, u_1} A
S : C
E : PreOneHypercover S
c : Cofan E.X
hc : IsColimit c
d : Cofan E.Y'
hd : IsColimit d
F : Cᵒᵖ ⥤ A
inst✝¹ : PreservesLimit (Discrete.functor fun i ↦ op (E.X i)) F
inst✝ : PreservesLimit (Discrete.functor fun i ↦ op (E.Y' i)) F
c' : Fan (E.multicospanIndex F).left := Fan.mk (F.obj (op c.pt)) fun i ↦ F.map (c.inj i).op
hc' : IsLimit c' := isLimitFanMkObjOfIsLimit F (fun i ↦ op (E.X i)) (fun i ↦ (c.inj i).op) (Cofan.IsColimit.op hc)
d' : Fan (E.multicospanIndex F).right := Fan.mk (F.obj (op d.pt)) fun i ↦ F.map (d.inj i).op
hd' : IsLimit d' := isLimitFanMkObjOfIsLimit F (fun i ↦ op (E.Y' i)) (fun i ↦ (d.inj i).op) (Cofan.IsColimit.op hd)
⊢ (Iso.refl c'.pt).hom ≫ F.map (Cofan.IsColimit.desc hd fun x ↦ E.p₂ x.snd ≫ c.inj x.fst.2).op =
    (E.multicospanIndex F).sndPiMapOfIsLimit c' hd' ≫ (Iso.refl d'.pt).hom

Tactic:
refine Fan.IsLimit.hom_ext hd' _ _ fun i ↦ ?_

Goal state after:
case refine_2
C : Type u
inst✝³ : Category.{v, u} C
A : Type u_1
inst✝² : Category.{v_1, u_1} A
S : C
E : PreOneHypercover S
c : Cofan E.X
hc : IsColimit c
d : Cofan E.Y'
hd : IsColimit d
F : Cᵒᵖ ⥤ A
inst✝¹ : PreservesLimit (Discrete.functor fun i ↦ op (E.X i)) F
inst✝ : PreservesLimit (Discrete.functor fun i ↦ op (E.Y' i)) F
c' : Fan (E.multicospanIndex F).left := Fan.mk (F.obj (op c.pt)) fun i ↦ F.map (c.inj i).op
hc' : IsLimit c' := isLimitFanMkObjOfIsLimit F (fun i ↦ op (E.X i)) (fun i ↦ (c.inj i).op) (Cofan.IsColimit.op hc)
d' : Fan (E.multicospanIndex F).right := Fan.mk (F.obj (op d.pt)) fun i ↦ F.map (d.inj i).op
hd' : IsLimit d' := isLimitFanMkObjOfIsLimit F (fun i ↦ op (E.Y' i)) (fun i ↦ (d.inj i).op) (Cofan.IsColimit.op hd)
i : E.multicospanShape.R
⊢ ((Iso.refl c'.pt).hom ≫ F.map (Cofan.IsColimit.desc hd fun x ↦ E.p₂ x.snd ≫ c.inj x.fst.2).op) ≫ d'.proj i =
    ((E.multicospanIndex F).sndPiMapOfIsLimit c' hd' ≫ (Iso.refl d'.pt).hom) ≫ d'.proj i
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreOneHypercover S
i i' j j' : E.I₀
hii' : i = i'
hjj' : j = j'
i'' j'' : E.I₀
hii'' : i' = i''
hjj'' : j' = j''
k : E.I₁ i j
⊢ (congrIndexOneOfEq hii'' hjj'') ((congrIndexOneOfEq hii' hjj') k) = (congrIndexOneOfEq ⋯ ⋯) k

Tactic:
by
  subst hii' hjj'
  simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
i i' j j' : E.I₀
hii' : i = i'
hjj' : j = j'
u₀ : E.I₀ → F.I₀
u₁ : ⦃i j : E.I₀⦄ → E.I₁ i j → F.I₁ (u₀ i) (u₀ j)
k : E.I₁ i j
⊢ u₁ ((congrIndexOneOfEq hii' hjj') k) = (congrIndexOneOfEq ⋯ ⋯) (u₁ k)

Tactic:
by
  subst hii' hjj'
  simp

Goal state after: