awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.CoverLifting
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
h : F.IsCocontinuous J K
U : D
S : Sieve.{v_2, u_2} U
hS : S ∈ (K : (a : D) → Set (Sieve a)) U
refine_1 : Sieve.functorPullback F (Sieve.pullback (adj.counit.app U) S) ≤ Sieve.functorPushforward G S
⊢ Membership.mem (γ := Set (Sieve.{v_1, u_1} (G.obj U))) ((J : (a : C) → Set (Sieve a)) (G.obj U))
    (Sieve.functorPushforward G S)

Tactic:
refine J.superset_covering ?_ <| h.cover_lift (K.pullback_stable (adj.counit.app _) hS)

Premises used: CategoryTheory.GrothendieckTopology.superset_covering, CategoryTheory.GrothendieckTopology.pullback_stable, CategoryTheory.Adjunction.counit, CategoryTheory.NatTrans.app, CategoryTheory.Functor.IsCocontinuous.cover_lift
-- Module: Mathlib.CategoryTheory.Sites.CoverLifting
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
h : F.IsCocontinuous J K
U : D
S : Sieve.{v_2, u_2} U
hS : S ∈ (K : (a : D) → Set (Sieve a)) U
X : C
f : X ⟶ G.obj U
hf : (Sieve.functorPullback F (Sieve.pullback (adj.counit.app U) S)).arrows f
⊢ f = adj.unit.app X ≫ G.map (F.map f ≫ adj.counit.app U)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.CoverLifting
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
h : F.IsCocontinuous J K
U : D
S : Sieve.{v_2, u_2} U
hS : S ∈ (K : (a : D) → Set (Sieve a)) U
X : C
f : X ⟶ G.obj U
hf : (Sieve.functorPullback F (Sieve.pullback (adj.counit.app U) S)).arrows f
⊢ (Sieve.functorPushforward G S).arrows f

Tactic:
refine ⟨F.obj X, F.map f ≫ adj.counit.app _, adj.unit.app _, hf, by simp⟩
-- Module: Mathlib.CategoryTheory.Sites.CoverLifting
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
h : CoverPreserving K J G
U : C
S : Sieve.{v_2, u_2} (F.obj U)
hS : Membership.mem (γ := Set (Sieve.{v_2, u_2} (F.obj U))) ((K : (a : D) → Set (Sieve a)) (F.obj U)) S
⊢ Sieve.functorPullback F S ∈ (J : (a : C) → Set (Sieve a)) U

Tactic:
J.superset_covering ?_ (J.pullback_stable (adj.unit.app U) <| h.cover_preserve hS)

Premises used: CategoryTheory.GrothendieckTopology.superset_covering, CategoryTheory.Adjunction.unit, CategoryTheory.GrothendieckTopology.pullback_stable, CategoryTheory.CoverPreserving.cover_preserve, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Sites.CoverLifting
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
h : CoverPreserving K J G
U : C
S : Sieve.{v_2, u_2} (F.obj U)
hS : Membership.mem (γ := Set (Sieve.{v_2, u_2} (F.obj U))) ((K : (a : D) → Set (Sieve a)) (F.obj U)) S
refine_2 : Sieve.pullback (adj.unit.app U) (Sieve.functorPushforward G S) ≤ Sieve.functorPullback F S
⊢ Sieve.functorPullback F S ∈ (J : (a : C) → Set (Sieve a)) U

Tactic:
refine J.superset_covering ?_ (J.pullback_stable (adj.unit.app U) <| h.cover_preserve hS)

Premises used: CategoryTheory.GrothendieckTopology.superset_covering, CategoryTheory.Adjunction.unit, CategoryTheory.GrothendieckTopology.pullback_stable, CategoryTheory.CoverPreserving.cover_preserve, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Sites.CoverLifting
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
h : CoverPreserving K J G
U : C
S : Sieve.{v_2, u_2} (F.obj U)
hS : Membership.mem (γ := Set (Sieve.{v_2, u_2} (F.obj U))) ((K : (a : D) → Set (Sieve a)) (F.obj U)) S
X : C
f : X ⟶ U
refine_2 :
  ∀ (Y : D) (g : Y ⟶ F.obj U) (u : X ⟶ G.obj Y) (hg : S.arrows g) (heq : f ≫ adj.unit.app U = u ≫ G.map g),
    (Sieve.functorPullback F S).arrows f
⊢ (Sieve.pullback (adj.unit.app U) (Sieve.functorPushforward G S)).arrows f → (Sieve.functorPullback F S).arrows f

Tactic:
⟨Y, g, u, hg, heq⟩
-- Module: Mathlib.CategoryTheory.Sites.CoverLifting
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
h : CoverPreserving K J G
U : C
S : Sieve.{v_2, u_2} (F.obj U)
hS : Membership.mem (γ := Set (Sieve.{v_2, u_2} (F.obj U))) ((K : (a : D) → Set (Sieve a)) (F.obj U)) S
X : C
f : X ⟶ U
Y : D
g : Y ⟶ F.obj U
u : X ⟶ G.obj Y
hg : S.arrows g
heq : f ≫ adj.unit.app U = u ≫ G.map g
this : F.map f = ((adj.homEquiv X Y).symm : (a : X ⟶ G.obj Y) → F.obj X ⟶ Y) u ≫ g
⊢ (Sieve.functorPullback F S).arrows f

Tactic:
simp [this, S.downward_closed hg]

Premises used: CategoryTheory.Sieve.downward_closed
-- Module: Mathlib.CategoryTheory.Sites.CoverLifting
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
h : CoverPreserving K J G
U : C
S : Sieve.{v_2, u_2} (F.obj U)
hS : Membership.mem (γ := Set (Sieve.{v_2, u_2} (F.obj U))) ((K : (a : D) → Set (Sieve a)) (F.obj U)) S
X : C
f : X ⟶ U
Y : D
g : Y ⟶ F.obj U
u : X ⟶ G.obj Y
hg : S.arrows g
heq : f ≫ adj.unit.app U = u ≫ G.map g
refine_2 : F.map f = ((adj.homEquiv X Y).symm : (a : X ⟶ G.obj Y) → F.obj X ⟶ Y) u ≫ g
⊢ (Sieve.functorPullback F S).arrows f

Tactic:
suffices F.map f = (adj.homEquiv _ _).symm u ≫ g by
      simp [this, S.downward_closed hg]
-- Module: Mathlib.CategoryTheory.Sites.CoverLifting
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
h : CoverPreserving K J G
U : C
S : Sieve.{v_2, u_2} (F.obj U)
hS : Membership.mem (γ := Set (Sieve.{v_2, u_2} (F.obj U))) ((K : (a : D) → Set (Sieve a)) (F.obj U)) S
X : C
f : X ⟶ U
Y : D
g : Y ⟶ F.obj U
u : X ⟶ G.obj Y
hg : S.arrows g
heq : f ≫ adj.unit.app U = u ≫ G.map g
⊢ F.map f = ((adj.homEquiv X Y).symm : (a : X ⟶ G.obj Y) → F.obj X ⟶ Y) u ≫ g

Tactic:
simp [← Adjunction.homEquiv_naturality_right_symm, ← heq,
      Adjunction.homEquiv_naturality_left_symm]

Premises used: CategoryTheory.Adjunction.homEquiv_naturality_right_symm, CategoryTheory.Adjunction.homEquiv_naturality_left_symm
-- Module: Mathlib.CategoryTheory.Sites.CoverLifting
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
inst_2 : F.IsCocontinuous J K
⊢ G.IsRightAdjoint

Tactic:
have := adj.isRightAdjoint
-- Module: Mathlib.CategoryTheory.Sites.CoverLifting
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
inst_2 : F.IsCocontinuous J K
this : G.IsRightAdjoint
apply : CoverPreserving K J G
⊢ G.IsContinuous K J

Tactic:
apply Functor.isContinuous_of_coverPreserving (compatiblePreservingOfFlat J G)

Premises used: CategoryTheory.compatiblePreservingOfFlat, CategoryTheory.Functor.isContinuous_of_coverPreserving
-- Module: Mathlib.CategoryTheory.Sites.CoverLifting
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
inst_2 : F.IsCocontinuous J K
this : G.IsRightAdjoint
rwa rwa₁ rwa₂ rwa₃ : F.IsCocontinuous J K
⊢ CoverPreserving K J G

Tactic:
rwa [← adj.isCocontinuous_iff_coverPreserving]

Premises used: CategoryTheory.Adjunction.isCocontinuous_iff_coverPreserving
-- Module: Mathlib.CategoryTheory.Sites.CoverLifting
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
E : Type u_3
inst_2 : Category.{v_3, u_3} E
G_1 : Functor.{v_1, v_2, u_1, u_2} C D
G' : Functor.{v_2, v_3, u_2, u_3} D E
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
L : GrothendieckTopology.{v_3, u_3} E
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
inst_3 : F.IsCocontinuous J K
inst_4 : F.IsLeftAdjoint
⊢ F.rightAdjoint.IsContinuous K J

Tactic:
(Adjunction.ofIsLeftAdjoint F).isContinuous_of_isCocontinuous J K

Premises used: CategoryTheory.Adjunction.ofIsLeftAdjoint, CategoryTheory.Adjunction.isContinuous_of_isCocontinuous
-- Module: Mathlib.CategoryTheory.Sites.CoverLifting
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
A : Type w
inst_2 : Category.{w', w} A
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
inst_3 : G.IsCocontinuous J K
F : Functor.{v_1, w', u_1, w} Cᵒᵖ A
hF : Presheaf.IsSheaf J F
R : Functor.{v_2, w', u_2, w} 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
Y₁ : C
p₁ : Y₁ ⟶ Y
hp₁ :
  (↑(Subtype.mk (p := fun (S : Sieve.{v_1, u_1} Y) ↦ S ∈ (J : (a : C) → Set (Sieve a)) Y)
            (Sieve.functorPullback G (Sieve.pullback f (↑S : Sieve X))) ⋯) :
        Sieve Y).arrows
    p₁
Y₂ : C
p₂ : Y₂ ⟶ Y
hp₂ :
  (↑(Subtype.mk (p := fun (S : Sieve.{v_1, u_1} Y) ↦ S ∈ (J : (a : C) → Set (Sieve a)) Y)
            (Sieve.functorPullback G (Sieve.pullback f (↑S : Sieve X))) ⋯) :
        Sieve Y).arrows
    p₂
W : C
g₁ : W ⟶ Y₁
g₂ : W ⟶ Y₂
w : g₁ ≫ p₁ = g₂ ≫ p₂
simp :
  Eq (α := s.pt ⟶ F.obj (op W)) (s.ι { Y := G.obj Y₁, f := G.map p₁ ≫ f, hf := ⋯ } ≫ R.map (G.map g₁).op ≫ α.app (op W))
    (s.ι { Y := G.obj Y₂, f := G.map p₂ ≫ f, hf := ⋯ } ≫ R.map (G.map g₂).op ≫ α.app (op W))
⊢ CategoryStruct.comp (Y := R.obj (op (G.obj Y₁)))
        (s.ι { Y := G.obj Y₁, f := G.map p₁ ≫ f, hf := ⋯ : S.Arrow } :
          s.pt ⟶ (S.index R).left { Y := G.obj Y₁, f := G.map p₁ ≫ f, hf := ⋯ : S.Arrow })
        (α.app (op Y₁)) ≫
      F.map g₁.op =
    CategoryStruct.comp (Y := R.obj (op (G.obj Y₂)))
        (s.ι { Y := G.obj Y₂, f := G.map p₂ ≫ f, hf := ⋯ } :
          s.pt ⟶ (S.index R).left { Y := G.obj Y₂, f := G.map p₂ ≫ f, hf := ⋯ })
        (α.app (op Y₂)) ≫
      F.map g₂.op

Tactic:
simp only [Category.assoc, ← α.naturality, Functor.comp_map,
        Functor.op_map, Quiver.Hom.unop_op]

Premises used: CategoryTheory.Category.assoc, Quiver.Hom.unop_op, CategoryTheory.NatTrans.naturality, CategoryTheory.Functor.comp_map, CategoryTheory.Functor.op_map
-- Module: Mathlib.CategoryTheory.Sites.CoverLifting
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
A : Type w
inst_2 : Category.{w', w} A
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
inst_3 : G.IsCocontinuous J K
F : Functor.{v_1, w', u_1, w} Cᵒᵖ A
hF : Presheaf.IsSheaf J F
R : Functor.{v_2, w', u_2, w} 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
Y₁ : C
p₁ : Y₁ ⟶ Y
hp₁ :
  (↑(Subtype.mk (p := fun (S : Sieve.{v_1, u_1} Y) ↦ S ∈ (J : (a : C) → Set (Sieve a)) Y)
            (Sieve.functorPullback G (Sieve.pullback f (↑S : Sieve X))) ⋯) :
        Sieve Y).arrows
    p₁
Y₂ : C
p₂ : Y₂ ⟶ Y
hp₂ :
  (↑(Subtype.mk (p := fun (S : Sieve.{v_1, u_1} Y) ↦ S ∈ (J : (a : C) → Set (Sieve a)) Y)
            (Sieve.functorPullback G (Sieve.pullback f (↑S : Sieve X))) ⋯) :
        Sieve Y).arrows
    p₂
W : C
g₁ : W ⟶ Y₁
g₂ : W ⟶ Y₂
w : g₁ ≫ p₁ = g₂ ≫ p₂
⊢ G.map g₁ ≫ { Y := G.obj Y₁, f := G.map p₁ ≫ f, hf := hp₁ : S.Arrow }.f =
    G.map g₂ ≫ { Y := G.obj Y₂, f := G.map p₂ ≫ f, hf := hp₂ }.f

Tactic:
simpa using G.congr_map w =≫ f

Premises used: CategoryTheory.Functor.congr_map
-- Module: Mathlib.CategoryTheory.Sites.CoverLifting
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
A : Type w
inst_2 : Category.{w', w} A
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
inst_3 : G.IsCocontinuous J K
F : Functor.{v_1, w', u_1, w} Cᵒᵖ A
hF : Presheaf.IsSheaf J F
R : Functor.{v_2, w', u_2, w} 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
Y₁ : C
p₁ : Y₁ ⟶ Y
hp₁ :
  (↑(Subtype.mk (p := fun (S : Sieve.{v_1, u_1} Y) ↦ S ∈ (J : (a : C) → Set (Sieve a)) Y)
            (Sieve.functorPullback G (Sieve.pullback f (↑S : Sieve X))) ⋯) :
        Sieve Y).arrows
    p₁
Y₂ : C
p₂ : Y₂ ⟶ Y
hp₂ :
  (↑(Subtype.mk (p := fun (S : Sieve.{v_1, u_1} Y) ↦ S ∈ (J : (a : C) → Set (Sieve a)) Y)
            (Sieve.functorPullback G (Sieve.pullback f (↑S : Sieve X))) ⋯) :
        Sieve Y).arrows
    p₂
W : C
g₁ : W ⟶ Y₁
g₂ : W ⟶ Y₂
w : g₁ ≫ p₁ = g₂ ≫ p₂
⊢ Eq (α := s.pt ⟶ F.obj (op W)) (s.ι { Y := G.obj Y₁, f := G.map p₁ ≫ f, hf := ⋯ } ≫ R.map (G.map g₁).op ≫ α.app (op W))
    (s.ι { Y := G.obj Y₂, f := G.map p₂ ≫ f, hf := ⋯ } ≫ R.map (G.map g₂).op ≫ α.app (op W))

Tactic:
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
          .. }

Premises used: CategoryTheory.GrothendieckTopology.Cover.Arrow.Relation.mk, CategoryTheory.Functor.map, CategoryTheory.GrothendieckTopology.Cover.Relation.mk, CategoryTheory.Functor.obj, CategoryTheory.Limits.Multifork.condition_assoc
-- Module: Mathlib.CategoryTheory.Sites.CoverLifting
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
A : Type w
inst_2 : Category.{w', w} A
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
inst_3 : G.IsCocontinuous J K
F : Functor.{v_1, w', u_1, w} Cᵒᵖ A
hF : Presheaf.IsSheaf J F
R : Functor.{v_2, w', u_2, w} Dᵒᵖ A
α : G.op ⋙ R ⟶ F
X : D
S : K.Cover X
s : Multifork (S.index R)
Y : C
f : G.obj Y ⟶ X
W : C
g : W ⟶ Y
i : S.Arrow
h : G.obj W ⟶ i.Y
w : h ≫ i.f = G.map g ≫ f
⊢ (↑(Subtype.mk (p := fun (S : Sieve.{v_1, u_1} Y) ↦ S ∈ (J : (a : C) → Set (Sieve a)) Y)
            (Sieve.functorPullback G (Sieve.pullback f (↑S : Sieve X))) ⋯) :
        Sieve Y).arrows
    g

Tactic:
simpa only [Sieve.functorPullback_apply, functorPullback_mem,
        Sieve.pullback_apply, ← w] using S.1.downward_closed i.hf h

Premises used: CategoryTheory.Sieve.pullback_apply, CategoryTheory.Presieve.functorPullback_mem, CategoryTheory.Sieve.downward_closed, CategoryTheory.GrothendieckTopology.Cover.Arrow.hf, CategoryTheory.Sieve.functorPullback_apply, Subtype.val
-- Module: Mathlib.CategoryTheory.Sites.CoverLifting
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
A : Type w
inst_2 : Category.{w', w} A
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
inst_3 : G.IsCocontinuous J K
F : Functor.{v_1, w', u_1, w} Cᵒᵖ A
hF : Presheaf.IsSheaf J F
R : Functor.{v_2, w', u_2, w} Dᵒᵖ A
α : G.op ⋙ R ⟶ F
X : D
S : K.Cover X
s : Multifork (S.index R)
Y : C
f : G.obj Y ⟶ X
W : C
g : W ⟶ Y
i : S.Arrow
h : G.obj W ⟶ i.Y
w : h ≫ i.f = G.map g ≫ f
dsimp :
  CategoryStruct.comp (Y := R.obj (op (G.obj W)))
      (s.ι { Y := G.obj W, f := G.map g ≫ f, hf := ⋯ } :
        s.pt ⟶ (S.index R).left { Y := G.obj W, f := G.map g ≫ f, hf := ⋯ })
      (α.app (op W)) =
    s.ι i ≫ R.map h.op ≫ α.app (op W)
⊢ CategoryStruct.comp (Y :=
      (S.index R).left
        {
          Y :=
            G.obj
              { Y := W, f := g, hf := ⋯ :
                  GrothendieckTopology.Cover.Arrow
                    (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} Y) ↦ S ∈ (J : (a : C) → Set (Sieve a)) Y)
                      (Sieve.functorPullback G (Sieve.pullback f (↑S : Sieve X))) ⋯) }.Y,
          f :=
            G.map
                { Y := W, f := g, hf := ⋯ :
                    GrothendieckTopology.Cover.Arrow
                      (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} Y) ↦ S ∈ (J : (a : C) → Set (Sieve a)) Y)
                        (Sieve.functorPullback G (Sieve.pullback f (↑S : Sieve X))) ⋯) }.f ≫
              f,
          hf := ⋯ })
      (s.ι
        {
          Y :=
            G.obj
              { Y := W, f := g, hf := ⋯ :
                  GrothendieckTopology.Cover.Arrow
                    (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} Y) ↦ S ∈ (J : (a : C) → Set (Sieve a)) Y)
                      (Sieve.functorPullback G (Sieve.pullback f (↑S : Sieve X))) ⋯) }.Y,
          f :=
            G.map
                { Y := W, f := g, hf := ⋯ :
                    GrothendieckTopology.Cover.Arrow
                      (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} Y) ↦ S ∈ (J : (a : C) → Set (Sieve a)) Y)
                        (Sieve.functorPullback G (Sieve.pullback f (↑S : Sieve X))) ⋯) }.f ≫
              f,
          hf := ⋯ })
      (α.app
        (op
          { Y := W, f := g, hf := ⋯ :
              GrothendieckTopology.Cover.Arrow
                (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} Y) ↦ S ∈ (J : (a : C) → Set (Sieve a)) Y)
                  (Sieve.functorPullback G (Sieve.pullback f (↑S : Sieve X))) ⋯) }.Y)) =
    s.ι i ≫ R.map h.op ≫ α.app (op W)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Sites.CoverLifting
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
A : Type w
inst_2 : Category.{w', w} A
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
inst_3 : G.IsCocontinuous J K
F : Functor.{v_1, w', u_1, w} Cᵒᵖ A
hF : Presheaf.IsSheaf J F
R : Functor.{v_2, w', u_2, w} Dᵒᵖ A
α : G.op ⋙ R ⟶ F
X : D
S : K.Cover X
s : Multifork (S.index R)
Y : C
f : G.obj Y ⟶ X
W : C
g : W ⟶ Y
i : S.Arrow
h : G.obj W ⟶ i.Y
w : h ≫ i.f = G.map g ≫ f
simp :
  CategoryStruct.comp (Y := R.obj (op (G.obj W)))
      (s.ι { Y := G.obj W, f := G.map g ≫ f, hf := ⋯ } :
        s.pt ⟶ (S.index R).left { Y := G.obj W, f := G.map g ≫ f, hf := ⋯ })
      (α.app (op W)) =
    (s.ι i ≫ R.map h.op) ≫ α.app (op W)
⊢ CategoryStruct.comp (Y := R.obj (op (G.obj W)))
      (s.ι { Y := G.obj W, f := G.map g ≫ f, hf := ⋯ } :
        s.pt ⟶ (S.index R).left { Y := G.obj W, f := G.map g ≫ f, hf := ⋯ })
      (α.app (op W)) =
    s.ι i ≫ R.map h.op ≫ α.app (op W)

Tactic:
simp only [← Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Sites.CoverLifting
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
A : Type w
inst_2 : Category.{w', w} A
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
inst_3 : G.IsCocontinuous J K
F : Functor.{v_1, w', u_1, w} Cᵒᵖ A
hF : Presheaf.IsSheaf J F
R : Functor.{v_2, w', u_2, w} Dᵒᵖ A
α : G.op ⋙ R ⟶ F
X : D
S : K.Cover X
s : Multifork (S.index R)
Y : C
f : G.obj Y ⟶ X
W : C
g : W ⟶ Y
i : S.Arrow
h : G.obj W ⟶ i.Y
w : h ≫ i.f = G.map g ≫ f
e_a : s.ι { Y := G.obj W, f := G.map g ≫ f, hf := ⋯ } = s.ι i ≫ R.map h.op
⊢ CategoryStruct.comp (Y := R.obj (op (G.obj W)))
      (s.ι { Y := G.obj W, f := G.map g ≫ f, hf := ⋯ } :
        s.pt ⟶ (S.index R).left { Y := G.obj W, f := G.map g ≫ f, hf := ⋯ })
      (α.app (op W)) =
    (s.ι i ≫ R.map h.op) ≫ α.app (op W)

Tactic:
congr 1
-- Module: Mathlib.CategoryTheory.Sites.CoverLifting
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
A : Type w
inst_2 : Category.{w', w} A
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
inst_3 : G.IsCocontinuous J K
F : Functor.{v_1, w', u_1, w} Cᵒᵖ A
hF : Presheaf.IsSheaf J F
R : Functor.{v_2, w', u_2, w} Dᵒᵖ A
α : G.op ⋙ R ⟶ F
X : D
S : K.Cover X
s : Multifork (S.index R)
Y : C
f : G.obj Y ⟶ X
W : C
g : W ⟶ Y
i : S.Arrow
h : G.obj W ⟶ i.Y
w : h ≫ i.f = G.map g ≫ f
⊢ (↑S : Sieve X).arrows (G.map g ≫ f)

Tactic:
simpa only [← w] using S.1.downward_closed i.hf h

Premises used: CategoryTheory.Sieve.downward_closed, CategoryTheory.GrothendieckTopology.Cover.Arrow.hf, Subtype.val
-- Module: Mathlib.CategoryTheory.Sites.CoverLifting
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
A : Type w
inst_2 : Category.{w', w} A
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
inst_3 : G.IsCocontinuous J K
F : Functor.{v_1, w', u_1, w} Cᵒᵖ A
hF : Presheaf.IsSheaf J F
R : Functor.{v_2, w', u_2, w} Dᵒᵖ A
α : G.op ⋙ R ⟶ F
X : D
S : K.Cover X
s : Multifork (S.index R)
Y : C
f : G.obj Y ⟶ X
W : C
g : W ⟶ Y
i : S.Arrow
h : G.obj W ⟶ i.Y
w : h ≫ i.f = G.map g ≫ f
⊢ 𝟙 { Y := G.obj W, f := G.map g ≫ f, hf := ⋯ : S.Arrow }.Y ≫ { Y := G.obj W, f := G.map g ≫ f, hf := ⋯ : S.Arrow }.f =
    h ≫ i.f

Tactic:
simpa using w.symm

Premises used: Eq.symm
-- Module: Mathlib.CategoryTheory.Sites.CoverLifting
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
A : Type w
inst_2 : Category.{w', w} A
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
inst_3 : G.IsCocontinuous J K
F : Functor.{v_1, w', u_1, w} Cᵒᵖ A
hF : Presheaf.IsSheaf J F
R : Functor.{v_2, w', u_2, w} Dᵒᵖ A
α : G.op ⋙ R ⟶ F
X : D
S : K.Cover X
s : Multifork (S.index R)
Y : C
f : G.obj Y ⟶ X
W : C
g : W ⟶ Y
i : S.Arrow
h : G.obj W ⟶ i.Y
w : h ≫ i.f = G.map g ≫ f
r : S.Relation :=
  { fst := { Y := G.obj W, f := G.map g ≫ f, hf := ⋯ }, snd := i,
    r :=
      { Z := { Y := G.obj W, f := G.map g ≫ f, hf := ⋯ : S.Arrow }.Y,
        g₁ := 𝟙 { Y := G.obj W, f := G.map g ≫ f, hf := ⋯ : S.Arrow }.Y, g₂ := h, w := ⋯ :
        { Y := G.obj W, f := G.map g ≫ f, hf := ⋯ : S.Arrow }.Relation i } }
⊢ s.ι { Y := G.obj W, f := G.map g ≫ f, hf := ⋯ } = s.ι i ≫ R.map h.op

Tactic:
simpa [r] using s.condition r

Premises used: CategoryTheory.Limits.Multifork.condition