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

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 : D ⥤ E
G : E ⥤ D
adj : F ⊣ G
X✝ Y✝ : C ⥤ D
f✝ : X✝ ⟶ Y✝
⊢ (𝟭 (C ⥤ D)).map f✝ ≫ ((𝟭 (C ⥤ D)).obj Y✝).rightUnitor.inv ≫ Y✝.whiskerLeft adj.unit ≫ (Y✝.associator F G).inv =
    (((𝟭 (C ⥤ D)).obj X✝).rightUnitor.inv ≫ X✝.whiskerLeft adj.unit ≫ (X✝.associator F G).inv) ≫
      ((whiskeringRight C D E).obj F ⋙ (whiskeringRight C E D).obj G).map f✝

Tactic:
ext

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 : D ⥤ E
G : E ⥤ D
adj : F ⊣ G
X✝ Y✝ : C ⥤ D
f✝ : X✝ ⟶ Y✝
x✝ : C
⊢ ((𝟭 (C ⥤ D)).map f✝ ≫ ((𝟭 (C ⥤ D)).obj Y✝).rightUnitor.inv ≫ Y✝.whiskerLeft adj.unit ≫ (Y✝.associator F G).inv).app
      x✝ =
    ((((𝟭 (C ⥤ D)).obj X✝).rightUnitor.inv ≫ X✝.whiskerLeft adj.unit ≫ (X✝.associator F G).inv) ≫
          ((whiskeringRight C D E).obj F ⋙ (whiskeringRight C E D).obj G).map f✝).app
      x✝
Module: Mathlib.CategoryTheory.Adjunction.Whiskering

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 : D ⥤ E
G : E ⥤ D
adj : F ⊣ G
X✝ Y✝ : C ⥤ E
f✝ : X✝ ⟶ Y✝
⊢ ((whiskeringRight C E D).obj G ⋙ (whiskeringRight C D E).obj F).map f✝ ≫
      (Y✝.associator G F).hom ≫ Y✝.whiskerLeft adj.counit ≫ Y✝.rightUnitor.hom =
    ((X✝.associator G F).hom ≫ X✝.whiskerLeft adj.counit ≫ X✝.rightUnitor.hom) ≫ (𝟭 (C ⥤ E)).map f✝

Tactic:
ext

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 : D ⥤ E
G : E ⥤ D
adj : F ⊣ G
X✝ Y✝ : C ⥤ E
f✝ : X✝ ⟶ Y✝
x✝ : C
⊢ (((whiskeringRight C E D).obj G ⋙ (whiskeringRight C D E).obj F).map f✝ ≫
          (Y✝.associator G F).hom ≫ Y✝.whiskerLeft adj.counit ≫ Y✝.rightUnitor.hom).app
      x✝ =
    (((X✝.associator G F).hom ≫ X✝.whiskerLeft adj.counit ≫ X✝.rightUnitor.hom) ≫ (𝟭 (C ⥤ E)).map f✝).app x✝
Module: Mathlib.CategoryTheory.Adjunction.Whiskering

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 : D ⥤ E
G : E ⥤ D
adj : F ⊣ G
X : D ⥤ C
⊢ ((whiskeringLeft E D C).obj G).map
        ({ app := fun X ↦ ((𝟭 (D ⥤ C)).obj X).leftUnitor.inv ≫ whiskerRight adj.unit X ≫ (F.associator G X).hom,
              naturality := ⋯ }.app
          X) ≫
      { app := fun X ↦ (G.associator F X).inv ≫ whiskerRight adj.counit X ≫ X.leftUnitor.hom, naturality := ⋯ }.app
        (((whiskeringLeft E D C).obj G).obj X) =
    𝟙 (((whiskeringLeft E D C).obj G).obj X)

Tactic:
ext

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 : D ⥤ E
G : E ⥤ D
adj : F ⊣ G
X : D ⥤ C
x✝ : E
⊢ (((whiskeringLeft E D C).obj G).map
            ({ app := fun X ↦ ((𝟭 (D ⥤ C)).obj X).leftUnitor.inv ≫ whiskerRight adj.unit X ≫ (F.associator G X).hom,
                  naturality := ⋯ }.app
              X) ≫
          { app := fun X ↦ (G.associator F X).inv ≫ whiskerRight adj.counit X ≫ X.leftUnitor.hom, naturality := ⋯ }.app
            (((whiskeringLeft E D C).obj G).obj X)).app
      x✝ =
    (𝟙 (((whiskeringLeft E D C).obj G).obj X)).app x✝
Module: Mathlib.CategoryTheory.Adjunction.Whiskering

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 : D ⥤ E
G : E ⥤ D
adj : F ⊣ G
X : E ⥤ C
⊢ { app := fun X ↦ ((𝟭 (D ⥤ C)).obj X).leftUnitor.inv ≫ whiskerRight adj.unit X ≫ (F.associator G X).hom,
            naturality := ⋯ }.app
        (((whiskeringLeft D E C).obj F).obj X) ≫
      ((whiskeringLeft D E C).obj F).map
        ({ app := fun X ↦ (G.associator F X).inv ≫ whiskerRight adj.counit X ≫ X.leftUnitor.hom, naturality := ⋯ }.app
          X) =
    𝟙 (((whiskeringLeft D E C).obj F).obj X)

Tactic:
ext

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 : D ⥤ E
G : E ⥤ D
adj : F ⊣ G
X : E ⥤ C
x✝ : D
⊢ ({ app := fun X ↦ ((𝟭 (D ⥤ C)).obj X).leftUnitor.inv ≫ whiskerRight adj.unit X ≫ (F.associator G X).hom,
                naturality := ⋯ }.app
            (((whiskeringLeft D E C).obj F).obj X) ≫
          ((whiskeringLeft D E C).obj F).map
            ({ app := fun X ↦ (G.associator F X).inv ≫ whiskerRight adj.counit X ≫ X.leftUnitor.hom,
                  naturality := ⋯ }.app
              X)).app
      x✝ =
    (𝟙 (((whiskeringLeft D E C).obj F).obj X)).app x✝
Module: Mathlib.CategoryTheory.Functor.KanExtension.Preserves

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst✝⁶ : Category.{v_1, u_1} A
inst✝⁵ : Category.{v_2, u_2} B
inst✝⁴ : Category.{v_3, u_3} C
inst✝³ : Category.{v_4, u_4} D
G : B ⥤ D
F✝ : A ⥤ B
L : A ⥤ C
inst✝² : G.PreservesLeftKanExtensions L
inst✝¹ : ∀ (F : A ⥤ B), L.HasLeftKanExtension F
inst✝ : ∀ (F : A ⥤ D), L.HasLeftKanExtension F
F F' : A ⥤ B
η : F ⟶ F'
⊢ (whiskerRight (L.leftKanExtensionUnit F) G ≫ (L.associator (L.leftKanExtension F) G).hom) ≫
      L.whiskerLeft
          (whiskerRight
            ((L.leftKanExtension F).descOfIsLeftKanExtension (L.leftKanExtensionUnit F) (L.leftKanExtension F')
              (η ≫ L.leftKanExtensionUnit F'))
            G) ≫
        L.whiskerLeft (G.leftKanExtensionCompIsoOfPreserves F' L).hom =
    (whiskerRight (L.leftKanExtensionUnit F) G ≫ (L.associator (L.leftKanExtension F) G).hom) ≫
      L.whiskerLeft (G.leftKanExtensionCompIsoOfPreserves F L).hom ≫
        L.whiskerLeft
          ((L.leftKanExtension (F ⋙ G)).descOfIsLeftKanExtension (L.leftKanExtensionUnit (F ⋙ G))
            (L.leftKanExtension (F' ⋙ G)) (whiskerRight η G ≫ L.leftKanExtensionUnit (F' ⋙ G)))

Tactic:
ext

Goal state after:
A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst✝⁶ : Category.{v_1, u_1} A
inst✝⁵ : Category.{v_2, u_2} B
inst✝⁴ : Category.{v_3, u_3} C
inst✝³ : Category.{v_4, u_4} D
G : B ⥤ D
F✝ : A ⥤ B
L : A ⥤ C
inst✝² : G.PreservesLeftKanExtensions L
inst✝¹ : ∀ (F : A ⥤ B), L.HasLeftKanExtension F
inst✝ : ∀ (F : A ⥤ D), L.HasLeftKanExtension F
F F' : A ⥤ B
η : F ⟶ F'
x✝ : A
⊢ ((whiskerRight (L.leftKanExtensionUnit F) G ≫ (L.associator (L.leftKanExtension F) G).hom) ≫
          L.whiskerLeft
              (whiskerRight
                ((L.leftKanExtension F).descOfIsLeftKanExtension (L.leftKanExtensionUnit F) (L.leftKanExtension F')
                  (η ≫ L.leftKanExtensionUnit F'))
                G) ≫
            L.whiskerLeft (G.leftKanExtensionCompIsoOfPreserves F' L).hom).app
      x✝ =
    ((whiskerRight (L.leftKanExtensionUnit F) G ≫ (L.associator (L.leftKanExtension F) G).hom) ≫
          L.whiskerLeft (G.leftKanExtensionCompIsoOfPreserves F L).hom ≫
            L.whiskerLeft
              ((L.leftKanExtension (F ⋙ G)).descOfIsLeftKanExtension (L.leftKanExtensionUnit (F ⋙ G))
                (L.leftKanExtension (F' ⋙ G)) (whiskerRight η G ≫ L.leftKanExtensionUnit (F' ⋙ G)))).app
      x✝
Module: Mathlib.CategoryTheory.Functor.KanExtension.Preserves

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst✝⁶ : Category.{v_1, u_1} A
inst✝⁵ : Category.{v_2, u_2} B
inst✝⁴ : Category.{v_3, u_3} C
inst✝³ : Category.{v_4, u_4} D
G : B ⥤ D
F✝ : A ⥤ B
L : A ⥤ C
inst✝² : G.PreservesRightKanExtensions L
inst✝¹ : ∀ (F : A ⥤ B), L.HasRightKanExtension F
inst✝ : ∀ (F : A ⥤ D), L.HasRightKanExtension F
F F' : A ⥤ B
η : F ⟶ F'
⊢ (L.whiskerLeft
          (whiskerRight
            ((L.rightKanExtension F').liftOfIsRightKanExtension (L.rightKanExtensionCounit F') (L.rightKanExtension F)
              (L.rightKanExtensionCounit F ≫ η))
            G) ≫
        L.whiskerLeft (G.rightKanExtensionCompIsoOfPreserves F' L).hom) ≫
      L.rightKanExtensionCounit (F' ⋙ G) =
    (L.whiskerLeft (G.rightKanExtensionCompIsoOfPreserves F L).hom ≫
        L.whiskerLeft
          ((L.rightKanExtension (F' ⋙ G)).liftOfIsRightKanExtension (L.rightKanExtensionCounit (F' ⋙ G))
            (L.rightKanExtension (F ⋙ G)) (L.rightKanExtensionCounit (F ⋙ G) ≫ whiskerRight η G))) ≫
      L.rightKanExtensionCounit (F' ⋙ G)

Tactic:
ext

Goal state after:
A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst✝⁶ : Category.{v_1, u_1} A
inst✝⁵ : Category.{v_2, u_2} B
inst✝⁴ : Category.{v_3, u_3} C
inst✝³ : Category.{v_4, u_4} D
G : B ⥤ D
F✝ : A ⥤ B
L : A ⥤ C
inst✝² : G.PreservesRightKanExtensions L
inst✝¹ : ∀ (F : A ⥤ B), L.HasRightKanExtension F
inst✝ : ∀ (F : A ⥤ D), L.HasRightKanExtension F
F F' : A ⥤ B
η : F ⟶ F'
x✝ : A
⊢ ((L.whiskerLeft
              (whiskerRight
                ((L.rightKanExtension F').liftOfIsRightKanExtension (L.rightKanExtensionCounit F')
                  (L.rightKanExtension F) (L.rightKanExtensionCounit F ≫ η))
                G) ≫
            L.whiskerLeft (G.rightKanExtensionCompIsoOfPreserves F' L).hom) ≫
          L.rightKanExtensionCounit (F' ⋙ G)).app
      x✝ =
    ((L.whiskerLeft (G.rightKanExtensionCompIsoOfPreserves F L).hom ≫
            L.whiskerLeft
              ((L.rightKanExtension (F' ⋙ G)).liftOfIsRightKanExtension (L.rightKanExtensionCounit (F' ⋙ G))
                (L.rightKanExtension (F ⋙ G)) (L.rightKanExtensionCounit (F ⋙ G) ≫ whiskerRight η G))) ≫
          L.rightKanExtensionCounit (F' ⋙ G)).app
      x✝
Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck

Goal state before:
pp: C : Type u_2
inst✝⁴ : Category.{u_1, u_2} C
J : Precoverage C
inst✝³ : J.IsStableUnderComposition
inst✝² : J.IsStableUnderBaseChange
inst✝¹ : Limits.HasPullbacks C
inst✝ : J.HasIsos
⊢ (toPretopology C J).toGrothendieck = J.toGrothendieck

Tactic:
ext

Goal state after:
C : Type u_2
inst✝⁴ : Category.{u_1, u_2} C
J : Precoverage C
inst✝³ : J.IsStableUnderComposition
inst✝² : J.IsStableUnderBaseChange
inst✝¹ : Limits.HasPullbacks C
inst✝ : J.HasIsos
x✝¹ : C
x✝ : Sieve x✝¹
⊢ x✝ ∈ (toPretopology C J).toGrothendieck x✝¹ ↔ x✝ ∈ J.toGrothendieck x✝¹
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

Goal state after:
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
⊢ ∀ (ℱ : Sheaf K (Type u_1)) {Z : C} {T : Presieve Z} {x : FamilyOfElements (G.op ⋙ ℱ.obj) T},
    x.Compatible →
      ∀ {Y₁ Y₂ : C} {X : D} (f₁ : X ⟶ G.obj Y₁) (f₂ : X ⟶ G.obj Y₂) {g₁ : Y₁ ⟶ Z} {g₂ : Y₂ ⟶ Z} (hg₁ : T g₁)
        (hg₂ : T g₂),
        f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂ →
          (ConcreteCategory.hom (ℱ.obj.map f₁.op)) (x g₁ hg₁) = (ConcreteCategory.hom (ℱ.obj.map f₂.op)) (x g₂ hg₂)
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 F' : C ⥤ D
τ : F ⟶ F'
e : F ≅ F'
G : D ⥤ E
F'' : C ⥤ C
eF'' : F'' ≅ 𝟭 C
FG : C ⥤ E
eFG : F ⋙ G ≅ FG
A : Type u
inst✝² : Category.{t, u} A
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
inst✝¹ : F.IsContinuous J K
inst✝ : F'.IsContinuous J K
⊢ sheafPushforwardContinuousNatTrans e.inv A J K ≫ sheafPushforwardContinuousNatTrans e.hom A J K =
    𝟙 (F.sheafPushforwardContinuous A J K)

Tactic:
ext

Goal state after:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
F F' : C ⥤ D
τ : F ⟶ F'
e : F ≅ F'
G : D ⥤ E
F'' : C ⥤ C
eF'' : F'' ≅ 𝟭 C
FG : C ⥤ E
eFG : F ⋙ G ≅ FG
A : Type u
inst✝² : Category.{t, u} A
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
inst✝¹ : F.IsContinuous J K
inst✝ : F'.IsContinuous J K
x✝¹ : Sheaf K A
x✝ : Cᵒᵖ
⊢ ((sheafPushforwardContinuousNatTrans e.inv A J K ≫ sheafPushforwardContinuousNatTrans e.hom A J K).app x✝¹).hom.app
      x✝ =
    ((𝟙 (F.sheafPushforwardContinuous A J K)).app x✝¹).hom.app x✝
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 F' : C ⥤ D
τ : F ⟶ F'
e : F ≅ F'
G : D ⥤ E
F'' : C ⥤ C
eF'' : F'' ≅ 𝟭 C
FG : C ⥤ E
eFG : F ⋙ G ≅ FG
A : Type u
inst✝² : Category.{t, u} A
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
inst✝¹ : F.IsContinuous J K
inst✝ : F'.IsContinuous J K
⊢ sheafPushforwardContinuousNatTrans e.hom A J K ≫ sheafPushforwardContinuousNatTrans e.inv A J K =
    𝟙 (F'.sheafPushforwardContinuous A J K)

Tactic:
ext

Goal state after:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
F F' : C ⥤ D
τ : F ⟶ F'
e : F ≅ F'
G : D ⥤ E
F'' : C ⥤ C
eF'' : F'' ≅ 𝟭 C
FG : C ⥤ E
eFG : F ⋙ G ≅ FG
A : Type u
inst✝² : Category.{t, u} A
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
inst✝¹ : F.IsContinuous J K
inst✝ : F'.IsContinuous J K
x✝¹ : Sheaf K A
x✝ : Cᵒᵖ
⊢ ((sheafPushforwardContinuousNatTrans e.hom A J K ≫ sheafPushforwardContinuousNatTrans e.inv A J K).app x✝¹).hom.app
      x✝ =
    ((𝟙 (F'.sheafPushforwardContinuous A J K)).app x✝¹).hom.app x✝
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₂ : E.I₀
inst✝ : HasPullback (E.f i₁) (E.f i₂)
W : C
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
w : p₁ ≫ E.f i₁ = p₂ ≫ E.f i₂
Z : C
g : Z ⟶ W
⊢ (E.sieve₁ p₁ p₂).arrows g ↔ (Sieve.pullback (pullback.lift p₁ p₂ w) (E.sieve₁' i₁ i₂)).arrows g

Tactic:
constructor

Goal state after:
case mp
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
i₁ i₂ : E.I₀
inst✝ : HasPullback (E.f i₁) (E.f i₂)
W : C
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
w : p₁ ≫ E.f i₁ = p₂ ≫ E.f i₂
Z : C
g : Z ⟶ W
⊢ (E.sieve₁ p₁ p₂).arrows g → (Sieve.pullback (pullback.lift p₁ p₂ w) (E.sieve₁' i₁ i₂)).arrows g

case mpr
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
i₁ i₂ : E.I₀
inst✝ : HasPullback (E.f i₁) (E.f i₂)
W : C
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
w : p₁ ≫ E.f i₁ = p₂ ≫ E.f i₂
Z : C
g : Z ⟶ W
⊢ (Sieve.pullback (pullback.lift p₁ p₂ w) (E.sieve₁' i₁ i₂)).arrows g → (E.sieve₁ p₁ p₂).arrows g
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
F : C ⥤ D
inst✝¹ : F.Full
inst✝ : F.Faithful
hF : {c : C} → {d : D} → (d ⟶ F.obj c) → (c' : C) × (F.obj c' ≅ d)
⊢ CompatiblePreserving K F

Tactic:
constructor

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
K : GrothendieckTopology D
F : C ⥤ D
inst✝¹ : F.Full
inst✝ : F.Faithful
hF : {c : C} → {d : D} → (d ⟶ F.obj c) → (c' : C) × (F.obj c' ≅ d)
⊢ ∀ (ℱ : Sheaf K (Type u_1)) {Z : C} {T : Presieve Z} {x : FamilyOfElements (F.op ⋙ ℱ.obj) T},
    x.Compatible →
      ∀ {Y₁ Y₂ : C} {X : D} (f₁ : X ⟶ F.obj Y₁) (f₂ : X ⟶ F.obj Y₂) {g₁ : Y₁ ⟶ Z} {g₂ : Y₂ ⟶ Z} (hg₁ : T g₁)
        (hg₂ : T g₂),
        f₁ ≫ F.map g₁ = f₂ ≫ F.map g₂ →
          (ConcreteCategory.hom (ℱ.obj.map f₁.op)) (x g₁ hg₁) = (ConcreteCategory.hom (ℱ.obj.map f₂.op)) (x g₂ hg₂)
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
U V : C
f : U ⟶ V
⊢ G.imageSieve (G.map f) = ⊤

Tactic:
ext W g; simpa using ⟨g ≫ f, by simp⟩

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

Goal state before:
pp: C : Type uC
inst✝ : Category.{vC, uC} C
U V : C
f : U ⟶ V
⊢ equalizer f f = ⊤

Tactic:
ext

Goal state after:
C : Type uC
inst✝ : Category.{vC, uC} C
U V : C
f : U ⟶ V
Y✝ : C
f✝ : Y✝ ⟶ U
⊢ (equalizer f f).arrows f✝ ↔ ⊤.arrows f✝
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
K : GrothendieckTopology D
G : C ⥤ D
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
X : C
T : ↑(K (G.obj X))
Y : D
iYX : Y ⟶ G.obj X
hiYX : (↑T).arrows iYX
Z : C
iZY : G.obj Z ⟶ Y
⊢ Sieve.functorPushforward G (G.imageSieve (iZY ≫ iYX)) ≤
    Sieve.pullback iZY (Sieve.pullback iYX (Sieve.functorPushforward G (Sieve.functorPullback G ↑T)))

Tactic:
rintro W _ ⟨V, iVZ, iWV, ⟨iVX, e⟩, rfl⟩

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
K : GrothendieckTopology D
G : C ⥤ D
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
X : C
T : ↑(K (G.obj X))
Y : D
iYX : Y ⟶ G.obj X
hiYX : (↑T).arrows iYX
Z : C
iZY : G.obj Z ⟶ Y
W : D
V : C
iVZ : V ⟶ Z
iWV : W ⟶ G.obj V
iVX : V ⟶ X
e : G.map iVX = G.map iVZ ≫ iZY ≫ iYX
⊢ (Sieve.pullback iZY (Sieve.pullback iYX (Sieve.functorPushforward G (Sieve.functorPullback G ↑T)))).arrows
    (iWV ≫ G.map iVZ)
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
D : Type u_2
inst✝¹ : Category.{v_2, u_2} D
K : GrothendieckTopology D
G : C ⥤ D
ℱ : Dᵒᵖ ⥤ Type v
ℱ' : Sheaf K (Type v)
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj
inst✝ : G.IsLocallyFull K
X Y : C
i : G.obj X ⟶ G.obj Y
⊢ α.app (op Y) ≫ ℱ'.obj.map i.op = ℱ.map i.op ≫ α.app (op X)

Tactic:
ext

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
D : Type u_2
inst✝¹ : Category.{v_2, u_2} D
K : GrothendieckTopology D
G : C ⥤ D
ℱ : Dᵒᵖ ⥤ Type v
ℱ' : Sheaf K (Type v)
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj
inst✝ : G.IsLocallyFull K
X Y : C
i : G.obj X ⟶ G.obj Y
x✝ : (G.op ⋙ ℱ).obj (op Y)
⊢ (ConcreteCategory.hom (α.app (op Y) ≫ ℱ'.obj.map i.op)).toFun x✝ =
    (ConcreteCategory.hom (ℱ.map i.op ≫ α.app (op X))).toFun x✝
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
S W : C
p : W ⟶ S
⊢ (trivial S).sieve₁ p p = ⊤

Tactic:
ext

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
S W : C
p : W ⟶ S
Y✝ : C
f✝ : Y✝ ⟶ W
⊢ ((trivial S).sieve₁ p p).arrows f✝ ↔ ⊤.arrows f✝
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
K : GrothendieckTopology D
G : C ⥤ D
ℱ : Dᵒᵖ ⥤ Type v
ℱ' : Sheaf K (Type v)
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
X : D
Y : C
f : op X ⟶ op (G.obj Y)
⊢ appHom α X ≫ ℱ'.obj.map f = ℱ.map f ≫ α.app (op Y)

Tactic:
ext

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
K : GrothendieckTopology D
G : C ⥤ D
ℱ : Dᵒᵖ ⥤ Type v
ℱ' : Sheaf K (Type v)
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
X : D
Y : C
f : op X ⟶ op (G.obj Y)
x✝ : ℱ.obj (op X)
⊢ (ConcreteCategory.hom (appHom α X ≫ ℱ'.obj.map f)).toFun x✝ = (ConcreteCategory.hom (ℱ.map f ≫ α.app (op Y))).toFun x✝
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic

Goal state before:
pp: case h
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
D : Type u_2
inst✝⁴ : Category.{v_2, u_2} D
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝² : Category.{v_4, u_4} A
G : C ⥤ D
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
ℱ✝ : Dᵒᵖ ⥤ A
ℱ'✝ ℱ ℱ' : Sheaf K A
i : G.op ⋙ ℱ.obj ≅ G.op ⋙ ℱ'.obj
X : Dᵒᵖ
⊢ yoneda.map ((sheafHom i.hom).app X) ≫ (sheafYonedaHom i.inv).app X = 𝟙 (yoneda.obj (ℱ.obj.obj X)) ∧
    (sheafYonedaHom i.inv).app X ≫ yoneda.map ((sheafHom i.hom).app X) = 𝟙 (yoneda.obj (ℱ'.obj.obj X))

Tactic:
constructor

Goal state after:
case h.left
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
D : Type u_2
inst✝⁴ : Category.{v_2, u_2} D
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝² : Category.{v_4, u_4} A
G : C ⥤ D
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
ℱ✝ : Dᵒᵖ ⥤ A
ℱ'✝ ℱ ℱ' : Sheaf K A
i : G.op ⋙ ℱ.obj ≅ G.op ⋙ ℱ'.obj
X : Dᵒᵖ
⊢ yoneda.map ((sheafHom i.hom).app X) ≫ (sheafYonedaHom i.inv).app X = 𝟙 (yoneda.obj (ℱ.obj.obj X))

case h.right
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
D : Type u_2
inst✝⁴ : Category.{v_2, u_2} D
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝² : Category.{v_4, u_4} A
G : C ⥤ D
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
ℱ✝ : Dᵒᵖ ⥤ A
ℱ'✝ ℱ ℱ' : Sheaf K A
i : G.op ⋙ ℱ.obj ≅ G.op ⋙ ℱ'.obj
X : Dᵒᵖ
⊢ (sheafYonedaHom i.inv).app X ≫ yoneda.map ((sheafHom i.hom).app X) = 𝟙 (yoneda.obj (ℱ'.obj.obj X))
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
⊢ Function.Bijective ⇑(ConcreteCategory.hom ((yoneda.map ((G.op.ranCounit.app Y.obj).app (op U))).app (op X)))

Tactic:
constructor

Goal state after:
case left
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
⊢ Function.Injective ⇑(ConcreteCategory.hom ((yoneda.map ((G.op.ranCounit.app Y.obj).app (op U))).app (op X)))

case right
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
⊢ Function.Surjective ⇑(ConcreteCategory.hom ((yoneda.map ((G.op.ranCounit.app Y.obj).app (op U))).app (op X)))
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.SheafEquiv

Goal state before:
pp: case refine_1
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
⊢ ((const (StructuredArrow (op (G.obj U)) G.op)).obj X).obj g ⟶ (StructuredArrow.proj (op (G.obj U)) G.op ⋙ Y.obj).obj g

Tactic:
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 ↦ ?_

Goal state after:
case refine_1
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₂
⊢ (f ≫ Y.obj.map (l I₁.Y (unop g.2) U I₁.f g.hom.unop ⋯).op) ≫ Y.obj.map r.g₁.op =
    (f ≫ Y.obj.map (l I₂.Y (unop g.2) U I₂.f g.hom.unop ⋯).op) ≫ Y.obj.map r.g₂.op