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

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁).toFunctor S.arrows
hx : x.SieveCompatible
M : Sieve X := Sieve.bind S.arrows fun Y f hf ↦ ↑(x f hf)
this : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (hf : S.arrows f), Sieve.pullback f M = ↑(x f hf)
⊢ ∃ t, x.IsAmalgamation t

Tactic:
refine ⟨⟨_, J₁.close_isClosed M⟩, ?_⟩

Goal state after:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁).toFunctor S.arrows
hx : x.SieveCompatible
M : Sieve X := Sieve.bind S.arrows fun Y f hf ↦ ↑(x f hf)
this : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (hf : S.arrows f), Sieve.pullback f M = ↑(x f hf)
⊢ x.IsAmalgamation ⟨J₁.close M, ⋯⟩
Module: Mathlib.CategoryTheory.Functor.Flat

Goal state before:
pp: case refine_1
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
this : Nonempty (StructuredArrow X (F ⋙ G))
A B : StructuredArrow X (F ⋙ G)
U : StructuredArrow X G := IsCofiltered.min (T.obj A) (T.obj B)
⊢ ∃ W x x, True

Tactic:
let A' : StructuredArrow U.right F := .mk (IsCofiltered.minToLeft (T.obj A) (T.obj B)).right

Goal state after:
case refine_1
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
this : Nonempty (StructuredArrow X (F ⋙ G))
A B : StructuredArrow X (F ⋙ G)
U : StructuredArrow X G := IsCofiltered.min (T.obj A) (T.obj B)
A' : StructuredArrow U.right F :=
  StructuredArrow.mk (StructuredArrow.Hom.right (IsCofiltered.minToLeft (T.obj A) (T.obj B)))
⊢ ∃ W x x, True
Module: Mathlib.CategoryTheory.Sites.Coverage

Goal state before:
pp: case refine_1.transitive
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
⊢ ∃ R ∈ J.coverings X, R ≤ S.arrows

Tactic:
refine ⟨Presieve.bind R' (fun Y f hf ↦ S' (hle _ _ hf)), ?_, fun Z u hu ↦ ?_⟩

Goal state after:
case refine_1.transitive.refine_1
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
⊢ (R'.bind fun Y f hf ↦ S' ⋯) ∈ J.coverings X

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
Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck

Goal state before:
pp: case mpr.transitive
C : Type u_3
inst✝ : Category.{u_2, u_3} C
J : Precoverage C
P : Cᵒᵖ ⥤ Type u_1
H : ∀ {X Y : C} {f : Y ⟶ X}, ∀ R ∈ J.coverings X, Presieve.IsSheafFor P (Sieve.pullback f (Sieve.generate R)).arrows
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
hS : J.Saturate X R
h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → J.Saturate Y (Sieve.pullback f S)
H1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X), Presieve.IsSheafFor P (Sieve.pullback f R).arrows
H2 :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y), Presieve.IsSheafFor P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows
⊢ ∀ ⦃Y : C⦄ (f : Y ⟶ X), Presieve.IsSheafFor P (Sieve.pullback f S).arrows

Tactic:
| transitive X R S hS h H1 H2 =>

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

Goal state before:
pp: C : Type u_4
inst✝³ : Category.{u_3, u_4} C
D : Type u_1
inst✝² : Category.{v_1, u_1} D
F : C ⥤ D
P : Dᵒᵖ ⥤ Type u_2
X : C
ι : Type (max u_4 u_3)
Y : ι → C
f : (i : ι) → Y i ⟶ X
inst✝¹ : (ofArrows Y f).HasPairwisePullbacks
inst✝ : F.PreservesPairwisePullbacks (ofArrows Y f)
this : (ofArrows (fun i ↦ F.obj (Y i)) fun i ↦ F.map (f i)).HasPairwisePullbacks
⊢ (∀ (x : (i : ι) → (F.op ⋙ P).obj (Opposite.op (Y i))),
      Arrows.PullbackCompatible (F.op ⋙ P) f x →
        ∃! t, ∀ (i : ι), (ConcreteCategory.hom ((F.op ⋙ P).map (f i).op)) t = x i) ↔
    ∀ (x : (i : ι) → P.obj (Opposite.op (F.obj (Y i)))),
      Arrows.PullbackCompatible P (fun i ↦ F.map (f i)) x →
        ∃! t, ∀ (i : ι), (ConcreteCategory.hom (P.map (F.map (f i)).op)) t = x i

Tactic:
dsimp [Arrows.PullbackCompatible]

Goal state after:
C : Type u_4
inst✝³ : Category.{u_3, u_4} C
D : Type u_1
inst✝² : Category.{v_1, u_1} D
F : C ⥤ D
P : Dᵒᵖ ⥤ Type u_2
X : C
ι : Type (max u_4 u_3)
Y : ι → C
f : (i : ι) → Y i ⟶ X
inst✝¹ : (ofArrows Y f).HasPairwisePullbacks
inst✝ : F.PreservesPairwisePullbacks (ofArrows Y f)
this : (ofArrows (fun i ↦ F.obj (Y i)) fun i ↦ F.map (f i)).HasPairwisePullbacks
⊢ (∀ (x : (i : ι) → P.obj (Opposite.op (F.obj (Y i)))),
      (∀ (i j : ι),
          (ConcreteCategory.hom (P.map (F.map (pullback.fst (f i) (f j))).op)) (x i) =
            (ConcreteCategory.hom (P.map (F.map (pullback.snd (f i) (f j))).op)) (x j)) →
        ∃! t, ∀ (i : ι), (ConcreteCategory.hom (P.map (F.map (f i)).op)) t = x i) ↔
    ∀ (x : (i : ι) → P.obj (Opposite.op (F.obj (Y i)))),
      (∀ (i j : ι),
          (ConcreteCategory.hom (P.map (pullback.fst (F.map (f i)) (F.map (f j))).op)) (x i) =
            (ConcreteCategory.hom (P.map (pullback.snd (F.map (f i)) (F.map (f j))).op)) (x j)) →
        ∃! t, ∀ (i : ι), (ConcreteCategory.hom (P.map (F.map (f i)).op)) t = x i
Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck

Goal state before:
pp: C : Type u_3
inst✝¹ : Category.{u_2, u_3} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
J : GrothendieckTopology C
ι : Type (max u_3 u_2)
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : Presieve.ofArrows X f ∈ J.toPrecoverage.coverings S
Y : C
g : Y ⟶ S
P : ι → C
p₁ : (i : ι) → P i ⟶ Y
p₂ : (i : ι) → P i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
⊢ Presieve.ofArrows P p₁ ∈ J.toPrecoverage.coverings Y

Tactic:
rw [mem_toPrecoverage_iff, ← Sieve.ofArrows, Sieve.ofArrows_eq_pullback_of_isPullback _ h]

Goal state after:
C : Type u_3
inst✝¹ : Category.{u_2, u_3} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
J : GrothendieckTopology C
ι : Type (max u_3 u_2)
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : Presieve.ofArrows X f ∈ J.toPrecoverage.coverings S
Y : C
g : Y ⟶ S
P : ι → C
p₁ : (i : ι) → P i ⟶ Y
p₂ : (i : ι) → P i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
⊢ Sieve.pullback g (Sieve.ofArrows X f) ∈ J Y
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
i₁ i₂ : E.I₀
W : C
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
Z Z' : C
g : Z ⟶ W
j : E.I₁ i₁ i₂
h : Z ⟶ E.Y j
fac₁ : g ≫ p₁ = h ≫ E.p₁ j
fac₂ : g ≫ p₂ = h ≫ E.p₂ j
φ : Z' ⟶ Z
⊢ (φ ≫ g) ≫ p₁ = (φ ≫ h) ≫ E.p₁ j

Tactic:
by simpa using φ ≫= fac₁

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

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
G : C ⥤ D
A : Type w
inst✝¹ : Category.{w', w} A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝ : G.IsCocontinuous J K
F : Cᵒᵖ ⥤ A
hF : Presheaf.IsSheaf J F
R : Dᵒᵖ ⥤ A
α : G.op ⋙ R ⟶ F
hR : (Functor.RightExtension.mk R α).IsPointwiseRightKanExtension
X : D
S : K.Cover X
s : Multifork (S.index R)
Y : C
f : G.obj Y ⟶ X
⊢ ∀ (b : (GrothendieckTopology.Cover.shape ⟨Sieve.functorPullback G (Sieve.pullback f ↑S), ⋯⟩).R),
    (s.ι
            {
              Y :=
                G.obj ((GrothendieckTopology.Cover.shape ⟨Sieve.functorPullback G (Sieve.pullback f ↑S), ⋯⟩).fst b).Y,
              f :=
                G.map ((GrothendieckTopology.Cover.shape ⟨Sieve.functorPullback G (Sieve.pullback f ↑S), ⋯⟩).fst b).f ≫
                  f,
              hf := ⋯ } ≫
          α.app (op ((GrothendieckTopology.Cover.shape ⟨Sieve.functorPullback G (Sieve.pullback f ↑S), ⋯⟩).fst b).Y)) ≫
        (GrothendieckTopology.Cover.index ⟨Sieve.functorPullback G (Sieve.pullback f ↑S), ⋯⟩ F).fst b =
      (s.ι
            {
              Y :=
                G.obj ((GrothendieckTopology.Cover.shape ⟨Sieve.functorPullback G (Sieve.pullback f ↑S), ⋯⟩).snd b).Y,
              f :=
                G.map ((GrothendieckTopology.Cover.shape ⟨Sieve.functorPullback G (Sieve.pullback f ↑S), ⋯⟩).snd b).f ≫
                  f,
              hf := ⋯ } ≫
          α.app (op ((GrothendieckTopology.Cover.shape ⟨Sieve.functorPullback G (Sieve.pullback f ↑S), ⋯⟩).snd b).Y)) ≫
        (GrothendieckTopology.Cover.index ⟨Sieve.functorPullback G (Sieve.pullback f ↑S), ⋯⟩ F).snd b

Tactic:
by
      intro { fst := ⟨Y₁, p₁, hp₁⟩, snd := ⟨Y₂, p₂, hp₂⟩, r := ⟨W, g₁, g₂, w⟩ }
      dsimp at g₁ g₂ w ⊢
      simp only [Category.assoc, ← α.naturality, Functor.comp_map,
        Functor.op_map, Quiver.Hom.unop_op]
      apply s.condition_assoc
        { fst.hf := hp₁
          snd.hf := hp₂
          r.g₁ := G.map g₁
          r.g₂ := G.map g₂
          r.w := by simpa using G.congr_map w =≫ f
          .. }

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

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
G : C ⥤ D
A : Type w
inst✝³ : Category.{w', w} A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝² : G.IsCocontinuous J K
inst✝¹ : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F
inst✝ : G.IsContinuous J K
F : Sheaf K A
⊢ (G.op.ranAdjunction A).unit.app F.obj ≫
      G.op.ran.map ((G.sheafPushforwardContinuousCompSheafToPresheafIso A J K).inv.app F) ≫
        (G.sheafPushforwardCocontinuousCompSheafToPresheafIso A J K).inv.app
          ((G.sheafPushforwardContinuous A J K).obj F) =
    (G.op.ranAdjunction A).unit.app F.obj

Tactic:
erw [Functor.map_id]

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
G : C ⥤ D
A : Type w
inst✝³ : Category.{w', w} A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝² : G.IsCocontinuous J K
inst✝¹ : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F
inst✝ : G.IsContinuous J K
F : Sheaf K A
⊢ (G.op.ranAdjunction A).unit.app F.obj ≫
      𝟙 (G.op.ran.obj (G.op ⋙ F.obj)) ≫
        (G.sheafPushforwardCocontinuousCompSheafToPresheafIso A J K).inv.app
          ((G.sheafPushforwardContinuous A J K).obj F) =
    (G.op.ranAdjunction A).unit.app F.obj
Module: Mathlib.CategoryTheory.Sites.LocallyFullyFaithful

Goal state before:
pp: C : Type uC
inst✝³ : Category.{vC, uC} C
D : Type uD
inst✝² : Category.{vD, uD} D
G✝ : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type u_1
inst✝¹ : Category.{v_1, u_1} A
G : C ⥤ D
inst✝ : G.Faithful
U✝ V✝ : C
f₁ f₂ : U✝ ⟶ V✝
e : G.map f₁ = G.map f₂
⊢ Sieve.functorPushforward G (Sieve.equalizer f₁ f₂) ∈ K (G.obj U✝)

Tactic:
by obtain rfl := G.map_injective e; simp

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

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
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type w
inst✝² : Category.{w', w} A
inst✝¹ : ∀ (X : Dᵒᵖ), Limits.HasLimitsOfShape (StructuredArrow X G.op) A
inst✝ : IsDenseSubsite J K G
Y : Sheaf J A
U : C
X : A
f : (yoneda.obj (((𝟭 (Cᵒᵖ ⥤ A)).obj Y.obj).obj (op U))).obj (op X)
l : (X Y Z : C) → (f : X ⟶ Y) → (g : G.obj Y ⟶ G.obj Z) → (G.imageSieve g).arrows f → (X ⟶ Z)
hl :
  ∀ (X Y Z : C) (f : X ⟶ Y) (g : G.obj Y ⟶ G.obj Z) (hf : (G.imageSieve g).arrows f),
    G.map (l X Y Z f g hf) = G.map f ≫ g
g : StructuredArrow (op (G.obj U)) G.op
I₁ I₂ : GrothendieckTopology.Cover.Arrow ⟨G.imageSieve g.hom.unop, ⋯⟩
r : I₁.Relation I₂
⊢ G.map (r.g₁ ≫ l I₁.Y (unop g.2) U I₁.f g.hom.unop ⋯) = G.map (r.g₂ ≫ l I₂.Y (unop g.2) U I₂.f g.hom.unop ⋯)

Tactic:
map_comp,

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
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type w
inst✝² : Category.{w', w} A
inst✝¹ : ∀ (X : Dᵒᵖ), Limits.HasLimitsOfShape (StructuredArrow X G.op) A
inst✝ : IsDenseSubsite J K G
Y : Sheaf J A
U : C
X : A
f : (yoneda.obj (((𝟭 (Cᵒᵖ ⥤ A)).obj Y.obj).obj (op U))).obj (op X)
l : (X Y Z : C) → (f : X ⟶ Y) → (g : G.obj Y ⟶ G.obj Z) → (G.imageSieve g).arrows f → (X ⟶ Z)
hl :
  ∀ (X Y Z : C) (f : X ⟶ Y) (g : G.obj Y ⟶ G.obj Z) (hf : (G.imageSieve g).arrows f),
    G.map (l X Y Z f g hf) = G.map f ≫ g
g : StructuredArrow (op (G.obj U)) G.op
I₁ I₂ : GrothendieckTopology.Cover.Arrow ⟨G.imageSieve g.hom.unop, ⋯⟩
r : I₁.Relation I₂
⊢ G.map r.g₁ ≫ G.map (l I₁.Y (unop g.2) U I₁.f g.hom.unop ⋯) = G.map (r.g₂ ≫ l I₂.Y (unop g.2) U I₂.f g.hom.unop ⋯)
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.SheafEquiv

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
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type w
inst✝² : Category.{w', w} A
inst✝¹ : ∀ (X : Dᵒᵖ), Limits.HasLimitsOfShape (StructuredArrow X G.op) A
inst✝ : IsDenseSubsite J K G
Y : Sheaf J A
U : C
X : A
f : (yoneda.obj (((𝟭 (Cᵒᵖ ⥤ A)).obj Y.obj).obj (op U))).obj (op X)
l : (X Y Z : C) → (f : X ⟶ Y) → (g : G.obj Y ⟶ G.obj Z) → (G.imageSieve g).arrows f → (X ⟶ Z)
hl :
  ∀ (X Y Z : C) (f : X ⟶ Y) (g : G.obj Y ⟶ G.obj Z) (hf : (G.imageSieve g).arrows f),
    G.map (l X Y Z f g hf) = G.map f ≫ g
g : StructuredArrow (op (G.obj U)) G.op
I₁ I₂ : GrothendieckTopology.Cover.Arrow ⟨G.imageSieve g.hom.unop, ⋯⟩
r : I₁.Relation I₂
⊢ G.map r.g₁ ≫ G.map I₁.f ≫ g.hom.unop = G.map (r.g₂ ≫ l I₂.Y (unop g.2) U I₂.f g.hom.unop ⋯)

Tactic:
map_comp,

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
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type w
inst✝² : Category.{w', w} A
inst✝¹ : ∀ (X : Dᵒᵖ), Limits.HasLimitsOfShape (StructuredArrow X G.op) A
inst✝ : IsDenseSubsite J K G
Y : Sheaf J A
U : C
X : A
f : (yoneda.obj (((𝟭 (Cᵒᵖ ⥤ A)).obj Y.obj).obj (op U))).obj (op X)
l : (X Y Z : C) → (f : X ⟶ Y) → (g : G.obj Y ⟶ G.obj Z) → (G.imageSieve g).arrows f → (X ⟶ Z)
hl :
  ∀ (X Y Z : C) (f : X ⟶ Y) (g : G.obj Y ⟶ G.obj Z) (hf : (G.imageSieve g).arrows f),
    G.map (l X Y Z f g hf) = G.map f ≫ g
g : StructuredArrow (op (G.obj U)) G.op
I₁ I₂ : GrothendieckTopology.Cover.Arrow ⟨G.imageSieve g.hom.unop, ⋯⟩
r : I₁.Relation I₂
⊢ G.map r.g₁ ≫ G.map I₁.f ≫ g.hom.unop = G.map r.g₂ ≫ G.map (l I₂.Y (unop g.2) U I₂.f g.hom.unop ⋯)
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.SheafEquiv

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
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type w
inst✝² : Category.{w', w} A
inst✝¹ : ∀ (X : Dᵒᵖ), Limits.HasLimitsOfShape (StructuredArrow X G.op) A
inst✝ : IsDenseSubsite J K G
Y : Sheaf J A
U : C
X : A
f : (yoneda.obj (((𝟭 (Cᵒᵖ ⥤ A)).obj Y.obj).obj (op U))).obj (op X)
l : (X Y Z : C) → (f : X ⟶ Y) → (g : G.obj Y ⟶ G.obj Z) → (G.imageSieve g).arrows f → (X ⟶ Z)
hl :
  ∀ (X Y Z : C) (f : X ⟶ Y) (g : G.obj Y ⟶ G.obj Z) (hf : (G.imageSieve g).arrows f),
    G.map (l X Y Z f g hf) = G.map f ≫ g
⊢ Limits.Cone (StructuredArrow.proj (op (G.obj U)) G.op ⋙ Y.obj)

Tactic:
by
      refine ⟨X, ⟨fun g ↦ ?_, fun g₁ g₂ i ↦ ?_⟩⟩
      · refine Y.2.amalgamate ⟨_, IsDenseSubsite.imageSieve_mem J K G g.hom.unop⟩
          (fun I ↦ f ≫ Y.1.map (l _ _ _ _ _ I.hf).op) fun I₁ I₂ r ↦ ?_
        apply (Y.2 X _ (IsDenseSubsite.equalizer_mem J K G (r.g₁ ≫ l _ _ _ _ _ I₁.hf)
          (r.g₂ ≫ l _ _ _ _ _ I₂.hf) ?_)).isSeparatedFor.ext fun V iUV (hiUV : _ = _) ↦ ?_
        · rw [map_comp, hl, map_comp, hl, ← map_comp_assoc, r.w, map_comp_assoc]
        · simp [← map_comp, ← op_comp, hiUV]
      · obtain ⟨⟨W₁⟩, ⟨g₁⟩, rfl⟩ := g₁.mk_surjective
        obtain ⟨⟨W₂⟩, ⟨g₂⟩, rfl⟩ := g₂.mk_surjective
        obtain ⟨⟨i⟩, hi, rfl⟩ := StructuredArrow.homMk_surjective i
        replace hi := Quiver.Hom.op_inj hi
        dsimp at g₁ g₂ i hi ⊢
        subst hi
        rw [Category.id_comp]
        apply Y.2.hom_ext ⟨_, IsDenseSubsite.imageSieve_mem J K G (G.map i ≫ g₁)⟩
        intro I
        simp only [Presheaf.IsSheaf.amalgamate_map, Category.assoc, ← Functor.map_comp]
        let I' : GrothendieckTopology.Cover.Arrow ⟨_, IsDenseSubsite.imageSieve_mem J K G g₁⟩ :=
          ⟨_, I.f ≫ i, ⟨l _ _ _ _ _ I.hf, by simp [hl]⟩⟩
        refine Eq.trans ?_ (Y.2.amalgamate_map _ _ _ I').symm
        apply (Y.2 X _ (IsDenseSubsite.equalizer_mem J K G (l _ _ _ _ _ I.hf)
          (l _ _ _ _ _ I'.hf) (by simp [I', hl]))).isSeparatedFor.ext
            fun V iUV (hiUV : _ = _) ↦ ?_
        simp [I', ← Functor.map_comp, ← op_comp, hiUV]

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
s₀ : E.I₀ ≃ F.I₀
s₁ : ⦃i j : E.I₀⦄ → E.I₁ i j ≃ F.I₁ (s₀ i) (s₀ j)
i j : E.I₀
k : E.I₁ i j
⊢ s₁ ((congrIndexOneOfEq ⋯ ⋯) k) = s₁ (s₁.symm ((congrIndexOneOfEq ⋯ ⋯) (s₁ k)))

Tactic:
simp [PreOneHypercover.congrIndexOneOfEq_naturality (u₁ := fun i j k ↦ s₁ k)]

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

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
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type w
inst✝² : Category.{w', w} A
inst✝¹ : ∀ (X : Dᵒᵖ), Limits.HasLimitsOfShape (StructuredArrow X G.op) A
inst✝ : IsDenseSubsite J K G
Y : Sheaf J A
⊢ IsIso ((G.sheafAdjunctionCocontinuous A J K).counit.app Y)

Tactic:
apply +allowSynthFailures ReflectsIsomorphisms.reflects (sheafToPresheaf J A)
  rw [NatTrans.isIso_iff_isIso_app]
  intro ⟨U⟩
  apply +allowSynthFailures ReflectsIsomorphisms.reflects yoneda
  rw [NatTrans.isIso_iff_isIso_app]
  intro ⟨X⟩
  simpa [sheafAdjunctionCocontinuous_counit_app_hom]
    using! isIso_ranCounit_app_of_isDenseSubsite G J K Y U X

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
S✝ : C
E✝¹ E✝ : PreOneHypercover S✝
F✝ : PreOneHypercover S✝
G : PreOneHypercover S✝
S : C
E F : PreOneHypercover S
s₀ : E.I₀ ≃ F.I₀
h₀ : (i : E.I₀) → E.X i ≅ F.X (s₀ i)
s₁ : ⦃i j : E.I₀⦄ → E.I₁ i j ≃ F.I₁ (s₀ i) (s₀ j)
h₁ : ⦃i j : E.I₀⦄ → (k : E.I₁ i j) → E.Y k ≅ F.Y (s₁ k)
w₀ : ∀ (i : E.I₀), (h₀ i).hom ≫ F.f (s₀ i) = E.f i
w₁₁ : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), (h₁ k).hom ≫ F.p₁ (s₁ k) = E.p₁ k ≫ (h₀ i).hom
w₁₂ : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), (h₁ k).hom ≫ F.p₂ (s₁ k) = E.p₂ k ≫ (h₀ j).hom
i j : F.I₀
k : F.I₁ i j
⊢ (congrIndexOneOfEqIso ⋯ ⋯ k).inv ≫ eqToHom ⋯ = 𝟙 (F.Y k) ≫ (congrIndexOneOfEqIso ⋯ ⋯ k).inv ≫ eqToHom ⋯

Tactic:
exact (Category.id_comp _).symm

Goal state after:
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✝ : CreatesFiniteCoproducts F
x✝¹ : Type
x✝ : Fintype x✝¹
⊢ CreatesLimitsOfShape (Discrete x✝¹) F.unop

Tactic:
apply +allowSynthFailures createsLimitsOfShapeUnop

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✝ : CreatesFiniteCoproducts F
x✝¹ : Type
x✝ : Fintype x✝¹
⊢ CreatesColimitsOfShape (Discrete x✝¹)ᵒᵖ F
Module: Mathlib.CategoryTheory.Sites.Equivalence

Goal state before:
pp: case mp
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : D ⥤ C
A : Type u₃
inst✝⁴ : Category.{v₃, u₃} A
inst✝³ : G.IsCoverDense J
inst✝² : G.Full
inst✝¹ : G.IsContinuous K J
inst✝ : (G.sheafPushforwardContinuous A K J).EssSurj
P✝ Q : Cᵒᵖ ⥤ A
f : P✝ ⟶ Q
P : Dᵒᵖ ⥤ A
⊢ ObjectProperty.isoClosure (fun x ↦ x ∈ Set.range (sheafToPresheaf K A).obj) P →
    ObjectProperty.isoClosure (fun x ↦ x ∈ Set.range (sheafToPresheaf J A ⋙ (whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op).obj) P

Tactic:
rintro ⟨_, ⟨R, rfl⟩, ⟨e⟩⟩

Goal state after:
case mp
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : D ⥤ C
A : Type u₃
inst✝⁴ : Category.{v₃, u₃} A
inst✝³ : G.IsCoverDense J
inst✝² : G.Full
inst✝¹ : G.IsContinuous K J
inst✝ : (G.sheafPushforwardContinuous A K J).EssSurj
P✝ Q : Cᵒᵖ ⥤ A
f : P✝ ⟶ Q
P : Dᵒᵖ ⥤ A
R : Sheaf K A
e : P ≅ (sheafToPresheaf K A).obj R
⊢ ObjectProperty.isoClosure (fun x ↦ x ∈ Set.range (sheafToPresheaf J A ⋙ (whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op).obj) P
Module: Mathlib.CategoryTheory.Sites.Equivalence

Goal state before:
pp: case mpr
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : D ⥤ C
A : Type u₃
inst✝⁴ : Category.{v₃, u₃} A
inst✝³ : G.IsCoverDense J
inst✝² : G.Full
inst✝¹ : G.IsContinuous K J
inst✝ : (G.sheafPushforwardContinuous A K J).EssSurj
P✝ Q : Cᵒᵖ ⥤ A
f : P✝ ⟶ Q
P : Dᵒᵖ ⥤ A
⊢ ObjectProperty.isoClosure (fun x ↦ x ∈ Set.range (sheafToPresheaf J A ⋙ (whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op).obj) P →
    ObjectProperty.isoClosure (fun x ↦ x ∈ Set.range (sheafToPresheaf K A).obj) P

Tactic:
rintro ⟨_, ⟨R, rfl⟩, ⟨e⟩⟩

Goal state after:
case mpr
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : D ⥤ C
A : Type u₃
inst✝⁴ : Category.{v₃, u₃} A
inst✝³ : G.IsCoverDense J
inst✝² : G.Full
inst✝¹ : G.IsContinuous K J
inst✝ : (G.sheafPushforwardContinuous A K J).EssSurj
P✝ Q : Cᵒᵖ ⥤ A
f : P✝ ⟶ Q
P : Dᵒᵖ ⥤ A
R : Sheaf J A
e : P ≅ (sheafToPresheaf J A ⋙ (whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op).obj R
⊢ ObjectProperty.isoClosure (fun x ↦ x ∈ Set.range (sheafToPresheaf K A).obj) P