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

Goal state before:
pp: case mp
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
hX : P X
hY : P Y
⊢ P.isColocal f → IsIso f

pp: case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
hX : P X
hY : P Y
⊢ IsIso f → P.isColocal f

Tactic:
· intro hf
    obtain ⟨g, hg⟩ := (hf _ hY).2 (𝟙 Y)
    exact ⟨g, (hf _ hX).1 (by cat_disch), hg⟩

Goal state after:
case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
hX : P X
hY : P Y
⊢ IsIso f → P.isColocal 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 ((MorphismProperty.isomorphisms C).inverseImage G)

Tactic:
exact adj.isLocalization

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u_1
B : Type u_2
inst✝² : Category.{v_1, u_1} A
inst✝¹ : Category.{v_2, u_2} B
F : A ⥤ B
G₁ : (Cᵒᵖ ⥤ A) ⥤ Sheaf J A
adj₁ : G₁ ⊣ sheafToPresheaf J A
G₂ : (Cᵒᵖ ⥤ B) ⥤ Sheaf J B
adj₂ : G₂ ⊣ sheafToPresheaf J B
inst✝ : J.HasSheafCompose F
P Q : Cᵒᵖ ⥤ A
f : P ⟶ Q
⊢ G₂.map (whiskerRight f F) ≫
      (adj₂.homEquiv (Q ⋙ F) ((sheafCompose J F).obj (G₁.obj Q))).symm (whiskerRight (adj₁.unit.app Q) F) =
    (adj₂.homEquiv (P ⋙ F) ((sheafCompose J F).obj (G₁.obj P))).symm (whiskerRight (adj₁.unit.app P) F) ≫
      (sheafCompose J F).map (G₁.map f)

Tactic:
erw [← adj₂.homEquiv_naturality_left_symm,
      ← adj₂.homEquiv_naturality_right_symm]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u_1
B : Type u_2
inst✝² : Category.{v_1, u_1} A
inst✝¹ : Category.{v_2, u_2} B
F : A ⥤ B
G₁ : (Cᵒᵖ ⥤ A) ⥤ Sheaf J A
adj₁ : G₁ ⊣ sheafToPresheaf J A
G₂ : (Cᵒᵖ ⥤ B) ⥤ Sheaf J B
adj₂ : G₂ ⊣ sheafToPresheaf J B
inst✝ : J.HasSheafCompose F
P Q : Cᵒᵖ ⥤ A
f : P ⟶ Q
⊢ (adj₂.homEquiv (P ⋙ F) ((sheafCompose J F).obj (G₁.obj Q))).symm
      (whiskerRight f F ≫ whiskerRight (adj₁.unit.app Q) F) =
    (adj₂.homEquiv (P ⋙ F) ((sheafCompose J F).obj (G₁.obj Q))).symm
      (whiskerRight (adj₁.unit.app P) F ≫ (sheafToPresheaf J B).map ((sheafCompose J F).map (G₁.map f)))
Module: Mathlib.CategoryTheory.Sites.PreservesSheafification

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u_1
B : Type u_2
inst✝² : Category.{v_1, u_1} A
inst✝¹ : Category.{v_2, u_2} B
F : A ⥤ B
G₁ : (Cᵒᵖ ⥤ A) ⥤ Sheaf J A
adj₁ : G₁ ⊣ sheafToPresheaf J A
G₂ : (Cᵒᵖ ⥤ B) ⥤ Sheaf J B
adj₂ : G₂ ⊣ sheafToPresheaf J B
inst✝ : J.HasSheafCompose F
P : Cᵒᵖ ⥤ A
⊢ adj₂.unit.app (P ⋙ F) ≫ (sheafToPresheaf J B).map ((sheafComposeNatTrans J F adj₁ adj₂).app P) =
    whiskerRight (adj₁.unit.app P) F

Tactic:
by
  simp [sheafComposeNatTrans, -ObjectProperty.ι_obj, -ObjectProperty.ι_map,
    Adjunction.homEquiv_counit]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u_1
B : Type u_2
inst✝² : Category.{v_1, u_1} A
inst✝¹ : Category.{v_2, u_2} B
F : A ⥤ B
G₁ : (Cᵒᵖ ⥤ A) ⥤ Sheaf J A
adj₁ : G₁ ⊣ sheafToPresheaf J A
G₂ : (Cᵒᵖ ⥤ B) ⥤ Sheaf J B
adj₂ : G₂ ⊣ sheafToPresheaf J B
inst✝ : J.HasSheafCompose F
⊢ (∀ (P : Cᵒᵖ ⥤ A), IsIso (G₂.map (whiskerRight (adj₁.unit.app P) F))) ↔
    ∀ (X : Cᵒᵖ ⥤ A), IsIso ((sheafComposeNatTrans J F adj₁ adj₂).app X)

Tactic:
apply forall_congr'

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u_1
B : Type u_2
inst✝² : Category.{v_1, u_1} A
inst✝¹ : Category.{v_2, u_2} B
F : A ⥤ B
G₁ : (Cᵒᵖ ⥤ A) ⥤ Sheaf J A
adj₁ : G₁ ⊣ sheafToPresheaf J A
G₂ : (Cᵒᵖ ⥤ B) ⥤ Sheaf J B
adj₂ : G₂ ⊣ sheafToPresheaf J B
inst✝ : J.HasSheafCompose F
⊢ ∀ (a : Cᵒᵖ ⥤ A),
    IsIso (G₂.map (whiskerRight (adj₁.unit.app a) F)) ↔ IsIso ((sheafComposeNatTrans J F adj₁ adj₂).app a)
Module: Mathlib.CategoryTheory.Sites.PreservesSheafification

Goal state before:
pp: C : Type u
inst✝¹⁶ : Category.{v, u} C
J : GrothendieckTopology C
D : Type u_3
E : Type u_4
inst✝¹⁵ : Category.{v_3, u_3} D
inst✝¹⁴ : Category.{v_4, u_4} E
F : D ⥤ E
inst✝¹³ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst✝¹² : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst✝¹¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹⁰ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst✝⁹ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
inst✝⁸ : ∀ (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
FD : D → D → Type u_5
CD : D → Type u_6
FE : E → E → Type u_7
CE : E → Type u_8
inst✝⁷ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝⁶ : (X Y : E) → FunLike (FE X Y) (CE X) (CE Y)
instCCD : ConcreteCategory D FD
instCCE : ConcreteCategory E FE
inst✝⁵ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
inst✝⁴ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget E)
inst✝³ : PreservesLimitsOfSize.{max v u, max v u, v_3, u_6, u_3, u_6 + 1} (forget D)
inst✝² : PreservesLimitsOfSize.{max v u, max v u, v_4, u_8, u_4, u_8 + 1} (forget E)
inst✝¹ : (forget D).ReflectsIsomorphisms
inst✝ : (forget E).ReflectsIsomorphisms
P : Cᵒᵖ ⥤ D
⊢ (sheafToPresheaf J E).map ((sheafComposeNatTrans J F (plusPlusAdjunction J D) (plusPlusAdjunction J E)).app P) =
    (J.sheafifyCompIso F P).inv

Tactic:
suffices (sheafComposeNatTrans J F (plusPlusAdjunction J D) (plusPlusAdjunction J E)).app P =
    ⟨(sheafifyCompIso J F P).inv⟩ by
    rw [this]
    rfl
  apply ((plusPlusAdjunction J E).homEquiv _ _).injective
  convert! sheafComposeNatTrans_fac J F (plusPlusAdjunction J D) (plusPlusAdjunction J E) P
  dsimp [plusPlusAdjunction]
  simp

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

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
F G : Cᵒᵖ ⥤ A
f : F ⟶ G
⊢ IsLocallySurjective J f ↔ Subfunctor.sheafify J (Subfunctor.range (whiskerRight f (forget A))) = ⊤

Tactic:
simp only [Subfunctor.ext_iff, funext_iff, Set.ext_iff, Subfunctor.top_obj,
    Set.top_eq_univ, Set.mem_univ, iff_true]

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
F G : Cᵒᵖ ⥤ A
f : F ⟶ G
⊢ IsLocallySurjective J f ↔
    ∀ (x : Cᵒᵖ) (x_1 : (G ⋙ forget A).obj x),
      x_1 ∈ (Subfunctor.sheafify J (Subfunctor.range (whiskerRight f (forget A)))).obj x
Module: Mathlib.CategoryTheory.Sites.LocallySurjective

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
F₁ F₂ F₃ : Cᵒᵖ ⥤ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
inst✝¹ : IsLocallySurjective J f₁
inst✝ : IsLocallySurjective J f₂
U✝ : C
s : ToType (F₃.obj (op U✝))
V W : C
i : V ⟶ W
j : W ⟶ U✝
H : (imageSieve f₂ s).arrows j
t' : ToType (F₁.obj (op V))
ht' : (ConcreteCategory.hom (f₁.app (op V))) t' = (ConcreteCategory.hom (F₂.map i.op)) (Exists.choose H)
⊢ (ConcreteCategory.hom ((f₁ ≫ f₂).app (op V))) t' = (ConcreteCategory.hom (F₃.map j.op ≫ F₃.map i.op)) s

Tactic:
NatTrans.comp_app,

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
F₁ F₂ F₃ : Cᵒᵖ ⥤ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
inst✝¹ : IsLocallySurjective J f₁
inst✝ : IsLocallySurjective J f₂
U✝ : C
s : ToType (F₃.obj (op U✝))
V W : C
i : V ⟶ W
j : W ⟶ U✝
H : (imageSieve f₂ s).arrows j
t' : ToType (F₁.obj (op V))
ht' : (ConcreteCategory.hom (f₁.app (op V))) t' = (ConcreteCategory.hom (F₂.map i.op)) (Exists.choose H)
⊢ (ConcreteCategory.hom (f₁.app (op V) ≫ f₂.app (op V))) t' = (ConcreteCategory.hom (F₃.map j.op ≫ F₃.map i.op)) s
Module: Mathlib.CategoryTheory.Sites.LocallyBijective

Goal state before:
pp: case mp
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
F G : Sheaf J A
f : F ⟶ G
inst✝¹ : (forget A).ReflectsIsomorphisms
inst✝ : J.HasSheafCompose (forget A)
left✝ : IsLocallyInjective f
right✝ : IsLocallySurjective f
⊢ IsIso f

Tactic:
← isIso_iff_of_reflects_iso f (sheafCompose J (forget A)),

Goal state after:
case mp
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
F G : Sheaf J A
f : F ⟶ G
inst✝¹ : (forget A).ReflectsIsomorphisms
inst✝ : J.HasSheafCompose (forget A)
left✝ : IsLocallyInjective f
right✝ : IsLocallySurjective f
⊢ IsIso ((sheafCompose J (forget A)).map f)
Module: Mathlib.CategoryTheory.Sites.LocallySurjective

Goal state before:
pp: case refine_2
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
F₁ F₂ F₃ : Cᵒᵖ ⥤ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
inst✝¹ : IsLocallySurjective J (f₁ ≫ f₂)
inst✝ : IsLocallyInjective J f₂
X : C
x : ToType (F₂.obj (op X))
S : Sieve X := imageSieve (f₁ ≫ f₂) ((ConcreteCategory.hom (f₂.app (op X))) x)
T : ⦃Y : C⦄ → (f : Y ⟶ X) → S.arrows f → Sieve Y :=
  fun Y f hf ↦
    equalizerSieve
      ((ConcreteCategory.hom (f₁.app (op Y))) (localPreimage (f₁ ≫ f₂) ((ConcreteCategory.hom (f₂.app (op X))) x) f hf))
      ((ConcreteCategory.hom (F₂.map f.op)) x)
Y : C
f : Y ⟶ unop (op X)
hf : (imageSieve (f₁ ≫ f₂) ((ConcreteCategory.hom (f₂.app (op X))) x)).arrows f
⊢ (ConcreteCategory.hom (f₂.app (op Y)))
      ((ConcreteCategory.hom (f₁.app (op Y)))
        (localPreimage (f₁ ≫ f₂) ((ConcreteCategory.hom (f₂.app (op X))) x) f hf)) =
    (ConcreteCategory.hom ((f₁ ≫ f₂).app (op Y)))
      (localPreimage (f₁ ≫ f₂) ((ConcreteCategory.hom (f₂.app (op X))) x) f hf)

Tactic:
NatTrans.comp_app,

Goal state after:
case refine_2
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
F₁ F₂ F₃ : Cᵒᵖ ⥤ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
inst✝¹ : IsLocallySurjective J (f₁ ≫ f₂)
inst✝ : IsLocallyInjective J f₂
X : C
x : ToType (F₂.obj (op X))
S : Sieve X := imageSieve (f₁ ≫ f₂) ((ConcreteCategory.hom (f₂.app (op X))) x)
T : ⦃Y : C⦄ → (f : Y ⟶ X) → S.arrows f → Sieve Y :=
  fun Y f hf ↦
    equalizerSieve
      ((ConcreteCategory.hom (f₁.app (op Y))) (localPreimage (f₁ ≫ f₂) ((ConcreteCategory.hom (f₂.app (op X))) x) f hf))
      ((ConcreteCategory.hom (F₂.map f.op)) x)
Y : C
f : Y ⟶ unop (op X)
hf : (imageSieve (f₁ ≫ f₂) ((ConcreteCategory.hom (f₂.app (op X))) x)).arrows f
⊢ (ConcreteCategory.hom (f₂.app (op Y)))
      ((ConcreteCategory.hom (f₁.app (op Y)))
        (localPreimage (f₁ ≫ f₂) ((ConcreteCategory.hom (f₂.app (op X))) x) f hf)) =
    (ConcreteCategory.hom (f₁.app (op Y) ≫ f₂.app (op Y)))
      (localPreimage (f₁ ≫ f₂) ((ConcreteCategory.hom (f₂.app (op X))) x) f hf)
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: case refine_2.refine_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasInitial C
ι : Type u_3
X : ι → C
c : Cofan X
hc : IsVanKampenColimit c
i j : ι
inst✝ : DecidableEq ι
t : Cofan fun k ↦ if k = i then X i else ⊥_ C
m : (Cofan.mk (X i) fun k ↦ if h : k = i then eqToHom ⋯ else eqToHom ⋯ ≫ initial.to (X i)).pt ⟶ t.pt
⊢ (∀ (j : ι),
      (Cofan.mk (X i) fun k ↦ if h : k = i then eqToHom ⋯ else eqToHom ⋯ ≫ initial.to (X i)).inj j ≫ m = t.inj j) →
    m = eqToHom ⋯ ≫ t.inj i

Tactic:
hm

Goal state after:
case refine_2.refine_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasInitial C
ι : Type u_3
X : ι → C
c : Cofan X
hc : IsVanKampenColimit c
i j : ι
inst✝ : DecidableEq ι
t : Cofan fun k ↦ if k = i then X i else ⊥_ C
m : (Cofan.mk (X i) fun k ↦ if h : k = i then eqToHom ⋯ else eqToHom ⋯ ≫ initial.to (X i)).pt ⟶ t.pt
hm :
  ∀ (j : ι), (Cofan.mk (X i) fun k ↦ if h : k = i then eqToHom ⋯ else eqToHom ⋯ ≫ initial.to (X i)).inj j ≫ m = t.inj j
⊢ m = eqToHom ⋯ ≫ t.inj i
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
ι : Type u_3
S B : C
X : ι → C
a : Cofan X
hau : IsUniversalColimit a
f : (i : ι) → X i ⟶ S
u : a.pt ⟶ S
v : B ⟶ S
P : ι → C
q₁ : (i : ι) → P i ⟶ B
q₂ : (i : ι) → P i ⟶ X i
hP : ∀ (i : ι), IsPullback (q₁ i) (q₂ i) v (f i)
d : Cofan P
hd : IsColimit d
hu : ∀ (i : ι), a.inj i ≫ u = f i
inst✝ : HasPullback v u
i : ι
⊢ q₁ i ≫ v = (q₂ i ≫ a.inj i) ≫ u

Tactic:
by simp [(hP i).w, hu]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
ι : Type u_3
S B : C
X : ι → C
a : Cofan X
hau : IsUniversalColimit a
f : (i : ι) → X i ⟶ S
u : a.pt ⟶ S
v : B ⟶ S
P : ι → C
q₁ : (i : ι) → P i ⟶ X i
q₂ : (i : ι) → P i ⟶ B
hP : ∀ (i : ι), IsPullback (q₁ i) (q₂ i) (f i) v
d : Cofan P
hd : IsColimit d
hu : ∀ (i : ι), a.inj i ≫ u = f i
inst✝ : HasPullback u v
i : ι
⊢ (q₁ i ≫ a.inj i) ≫ u = q₂ i ≫ v

Tactic:
by simp [(hP i).w, hu]

Goal state after:
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
⊢ S ∈ J X ↔ Presieve.IsSheafFor (Functor.closedSieves J).toFunctor S.arrows

Tactic:
by
  refine ⟨fun hS ↦ classifier_isSheaf _ _ hS, fun H ↦ ?_⟩
  rw [← J.close_eq_top_iff_mem]
  have : J.IsClosed (⊤ : Sieve X) := by
    intro Y f _
    trivial
  suffices (⟨J.close S, J.close_isClosed S⟩ : Subtype _) = ⟨⊤, this⟩ by
    rw [Subtype.ext_iff] at this
    exact this
  refine H.isSeparatedFor.ext fun Y f hf ↦ ?_
  simp only [Subfunctor.toFunctor_obj, Functor.sieves_obj, Functor.closedSieves_obj, Set.coe_ofPred]
  ext1
  dsimp
  rw [Sieve.pullback_top, ← J.pullback_close, S.pullback_eq_top_of_mem hf,
    J.close_eq_top_iff_mem]
  apply J.top_mem

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

Goal state before:
pp: case transitive
C : Type u_1
inst✝ : Category.{v_1, u_1} C
K : Coverage C
X✝ Y : C
S✝ : Sieve X✝
X : C
R S : Sieve X
a✝ : K.Saturate X R
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → K.Saturate Y (Sieve.pullback f S)
H1 : ∀ (f : Y ⟶ X), K.Saturate Y (Sieve.pullback f R)
a_ih✝ :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ X⦄, R.arrows f → ∀ (f_1 : Y ⟶ Y_1), K.Saturate Y (Sieve.pullback f_1 (Sieve.pullback f S))
f : Y ⟶ X
⊢ K.Saturate Y (Sieve.pullback f S)

Tactic:
refine (H1 f).transitive _ _ _ fun Z g hg ↦ ?_

Goal state after:
case transitive
C : Type u_1
inst✝ : Category.{v_1, u_1} C
K : Coverage C
X✝ Y : C
S✝ : Sieve X✝
X : C
R S : Sieve X
a✝ : K.Saturate X R
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → K.Saturate Y (Sieve.pullback f S)
H1 : ∀ (f : Y ⟶ X), K.Saturate Y (Sieve.pullback f R)
a_ih✝ :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ X⦄, R.arrows f → ∀ (f_1 : Y ⟶ Y_1), K.Saturate Y (Sieve.pullback f_1 (Sieve.pullback f S))
f : Y ⟶ X
Z : C
g : Z ⟶ Y
hg : (Sieve.pullback f R).arrows g
⊢ K.Saturate Z (Sieve.pullback g (Sieve.pullback f S))
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
F : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝ : F.IsContinuous J K
G : Sheaf K (Type t)
⊢ Presieve.IsSheaf J (F.op ⋙ G.obj ⋙ uliftFunctor.{max u₁ v₁ u₂ v₂, t})

Tactic:
apply isSheaf_of_isContinuous_aux.{t} J K

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝ : F.IsContinuous J K
G : Sheaf K (Type t)
⊢ Presieve.IsSheaf K (G.obj ⋙ uliftFunctor.{max u₁ v₁ u₂ v₂, t})
Module: Mathlib.CategoryTheory.Sites.CoverPreserving

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : C ⥤ D
inst✝ : RepresentablyFlat G
⊢ CompatiblePreserving K G

Tactic:
constructor
  intro ℱ Z T x hx Y₁ Y₂ X f₁ f₂ g₁ g₂ hg₁ hg₂ e
  -- First, `f₁` and `f₂` form a cone over `cospan g₁ g₂ ⋙ u`.
  let c : Cone (cospan g₁ g₂ ⋙ G) :=
    (Cone.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj (PullbackCone.mk f₁ f₂ e)
  /-
    This can then be viewed as a cospan of structured arrows, and we may obtain an arbitrary cone
    over it since `StructuredArrow W u` is cofiltered.
    Then, it suffices to prove that it is compatible when restricted onto `u(c'.X.right)`.
    -/
  let c' := IsCofiltered.cone (c.toStructuredArrow ⋙ StructuredArrow.pre _ _ _)
  have eq₁ : f₁ = (c'.pt.hom ≫ G.map (c'.π.app left).right) ≫ eqToHom (by simp) := by simp [c]
  have eq₂ : f₂ = (c'.pt.hom ≫ G.map (c'.π.app right).right) ≫ eqToHom (by simp) := by simp [c]
  conv_lhs => rw [eq₁]
  conv_rhs => rw [eq₂]
  simp only [c, op_comp, Functor.map_comp, types_comp_apply, eqToHom_op, eqToHom_map]
  apply congr_arg -- Porting note: was `congr 1` which for some reason doesn't do anything here
  -- despite goal being of the form f a = f b, with f=`ℱ.val.map (Quiver.Hom.op c'.pt.hom)`
  /-
    Since everything now falls in the image of `u`,
    the result follows from the compatibility of `x` in the image of `u`.
    -/
  injection c'.π.naturality WalkingCospan.Hom.inl with _ e₁
  injection c'.π.naturality WalkingCospan.Hom.inr with _ e₂
  exact hx (c'.π.app left).right (c'.π.app right).right hg₁ hg₂ (e₁.symm.trans e₂)

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

Goal state before:
pp: case refine_2
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝¹ : HasPullbacks C
inst✝ : PreservesLimitsOfShape WalkingCospan F
H : CoverPreserving J K F
U : C
E : J.OneHypercover U
i₁ i₂ : E.I₀
W : D
p₁ : W ⟶ F.obj (E.X i₁)
p₂ : W ⟶ F.obj (E.X i₂)
h : p₁ ≫ F.map (E.f i₁) = p₂ ≫ F.map (E.f i₂)
P : C := Limits.pullback (E.f i₁) (E.f i₂)
this✝ : HasPullback ((E.map F).f i₁) ((E.map F).f i₂)
this :
  (E.map F).sieve₁ (F.map (pullback.fst (E.f i₁) (E.f i₂))) (F.map (pullback.snd (E.f i₁) (E.f i₂))) ∈
    K (F.obj (Limits.pullback (E.f i₁) (E.f i₂)))
⊢ (E.map F).sieve₁ p₁ p₂ ∈ K W

Tactic:
refine K.superset_covering ?_
      (K.pullback_stable (IsPullback.lift (.map _ (.of_hasPullback _ _)) p₁ p₂ h) this)

Goal state after:
case refine_2
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝¹ : HasPullbacks C
inst✝ : PreservesLimitsOfShape WalkingCospan F
H : CoverPreserving J K F
U : C
E : J.OneHypercover U
i₁ i₂ : E.I₀
W : D
p₁ : W ⟶ F.obj (E.X i₁)
p₂ : W ⟶ F.obj (E.X i₂)
h : p₁ ≫ F.map (E.f i₁) = p₂ ≫ F.map (E.f i₂)
P : C := Limits.pullback (E.f i₁) (E.f i₂)
this✝ : HasPullback ((E.map F).f i₁) ((E.map F).f i₂)
this :
  (E.map F).sieve₁ (F.map (pullback.fst (E.f i₁) (E.f i₂))) (F.map (pullback.snd (E.f i₁) (E.f i₂))) ∈
    K (F.obj (Limits.pullback (E.f i₁) (E.f i₂)))
⊢ Sieve.pullback (⋯.lift p₁ p₂ h)
      ((E.map F).sieve₁ (F.map (pullback.fst (E.f i₁) (E.f i₂))) (F.map (pullback.snd (E.f i₁) (E.f i₂)))) ≤
    (E.map F).sieve₁ p₁ p₂
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
A : Type u_4
inst✝² : Category.{v_4, u_4} A
G : C ⥤ D
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
ℱ ℱ' : Sheaf K A
α : ℱ ⟶ ℱ'
i : IsIso (G.op.whiskerLeft α.hom)
⊢ α.hom = (sheafIso (asIso (G.op.whiskerLeft α.hom))).hom.hom

Tactic:
apply (sheafHom_eq _ _).symm

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
f g : E.Hom F
⊢ f = g ↔
    ∃ (hs₀ : f.s₀ = g.s₀) (_ : ∀ (i : E.I₀), f.h₀ i = g.h₀ i ≫ eqToHom ⋯) (hs₁ :
      ∀ (i j : E.I₀) (k : E.I₁ i j), f.s₁ k = (congrIndexOneOfEq ⋯ ⋯) (g.s₁ k)),
      ∀ (i j : E.I₀) (k : E.I₁ i j), f.h₁ k = g.h₁ k ≫ (congrIndexOneOfEqIso ⋯ ⋯ (g.s₁ k)).inv ≫ eqToHom ⋯

Tactic:
by
  refine ⟨fun h ↦ ?_, fun ⟨hs₀, hh₀, hs₁, hh₁⟩ ↦ Hom.ext' hs₀ hh₀ hs₁ hh₁⟩
  subst h
  simp [congrIndexOneOfEq]

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
K : GrothendieckTopology D
e : C ≌ D
inst✝ : IsDenseSubsite K J e.inverse
x✝¹ : D
x✝ : Sieve x✝¹
⊢ x✝ ∈ K x✝¹ ↔ x✝ ∈ (e.inverse.inducedTopology J) x✝¹

Tactic:
mem_inducedTopology_iff_of_isCoverDense

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
K : GrothendieckTopology D
e : C ≌ D
inst✝ : IsDenseSubsite K J e.inverse
x✝¹ : D
x✝ : Sieve x✝¹
⊢ x✝ ∈ K x✝¹ ↔ Sieve.functorPushforward e.inverse x✝ ∈ J (e.inverse.obj x✝¹)
Module: Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
F : C ⥤ D
inst✝ : CreatesFiniteProducts F
x✝¹ : Type
x✝ : Fintype x✝¹
⊢ CreatesColimitsOfShape (Discrete x✝¹) F.op

Tactic:
apply +allowSynthFailures createsColimitsOfShapeOp

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
F : C ⥤ D
inst✝ : CreatesFiniteProducts F
x✝¹ : Type
x✝ : Fintype x✝¹
⊢ CreatesLimitsOfShape (Discrete x✝¹)ᵒᵖ F
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
A : Type u_1
inst✝² : Category.{v_1, u_1} A
S : C
E : PreOneHypercover S
F : PreOneHypercover S
G✝ : PreOneHypercover S
inst✝¹ : ∀ (i : E.I₀) (j : F.I₀), HasPullback (E.f i) (F.f j)
inst✝ : ∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b), HasPullback (E.p₁ k ≫ E.f i) (F.p₁ l ≫ F.f a)
G : PreOneHypercover S
f : G.Hom E
g : G.Hom F
i✝ j✝ : G.I₀
k : G.I₁ i✝ j✝
⊢ pullback.lift (f.h₁ k) (g.h₁ k) ⋯ ≫ (E.inter F).p₂ (f.s₁ k, g.s₁ k) =
    G.p₂ k ≫ (PreZeroHypercover.interLift f.toHom g.toHom).h₀ j✝

Tactic:
by
    apply pullback.hom_ext
    · simpa using f.w₁₂ k
    · simpa using g.w₁₂ k

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
J : GrothendieckTopology C
S : C
E : J.OneHypercover S
F : Sheaf J A
c : Multifork (E.multicospanIndex F.obj)
m : c.pt ⟶ (E.multifork F.obj).pt
⊢ (∀ (i : E.multicospanShape.L), m ≫ (E.multifork F.obj).ι i = c.ι i) → m = multiforkLift c

Tactic:
hm

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
J : GrothendieckTopology C
S : C
E : J.OneHypercover S
F : Sheaf J A
c : Multifork (E.multicospanIndex F.obj)
m : c.pt ⟶ (E.multifork F.obj).pt
hm : ∀ (i : E.multicospanShape.L), m ≫ (E.multifork F.obj).ι i = c.ι i
⊢ m = multiforkLift c
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreZeroHypercover S
inst✝ : E.HasPullbacks
i j : E.I₀
⊢ E.toPreOneHypercover.sieve₁' i j = ⊤

Tactic:
rw [eq_top_iff]
  intro Y f _
  refine ⟨pullback (E.f i) (E.f j), f, 𝟙 _, ?_, by simp⟩
  refine Presieve.ofArrows.mk' ⟨⟩ rfl ?_
  apply pullback.hom_ext <;> simp [PreOneHypercover.toPullback]

Goal state after: