awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.CoproductSheafCondition (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A : Type u_2
inst_1 : Category.{v_2, u_2} A
S : C
E : PreZeroHypercover.{w, v_1, u_1} S
inst_2 : E.HasPullbacks
c : Cofan.{w, v_1, u_1} E.X
hc : IsColimit c
huniv : IsUniversalColimit c
inst_3 : (E.sigmaOfIsColimit hc).HasPullbacks
inst_4 : ∀ (i : E.I₀), HasPullback (E.f i) ((E.sigmaOfIsColimit hc).f PUnit.unit)
F : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ A
inst_5 :
  PreservesLimit.{w, w, v_1, v_2, u_1, u_2} (J := Discrete E.toPreOneHypercover.I₀)
    (Discrete.functor fun (i : E.toPreOneHypercover.I₀) ↦ op (E.toPreOneHypercover.X i)) F
inst_6 :
  PreservesLimit.{w, w, v_1, v_2, u_1, u_2} (J := Discrete E.toPreOneHypercover.I₁')
    (Discrete.functor fun (i : E.toPreOneHypercover.I₁') ↦ op (E.toPreOneHypercover.Y' i)) F
this : HasPullback (Cofan.IsColimit.desc hc E.f) (Cofan.IsColimit.desc hc E.f)
c' : Cofan.{w, v_1, u_1} E.toPreOneHypercover.Y' :=
  Cofan.mk ((E.sigmaOfIsColimit hc).toPreOneHypercover.Y (i₁ := PUnit.unit) (i₂ := PUnit.unit) PUnit.unit)
    fun (b : E.toPreOneHypercover.I₁') ↦
    pullback.map
      (E.f b.fst (β := fun (i : E.toPreOneHypercover.I₀ × E.toPreOneHypercover.I₀) ↦ E.toPreOneHypercover.I₁ i.1 i.2).1)
      (E.f b.fst (β := fun (i : E.toPreOneHypercover.I₀ × E.toPreOneHypercover.I₀) ↦ E.toPreOneHypercover.I₁ i.1 i.2).2)
      ((E.sigmaOfIsColimit hc).f PUnit.unit) ((E.sigmaOfIsColimit hc).f PUnit.unit)
      (c.inj
        b.fst (β := fun (i : E.toPreOneHypercover.I₀ × E.toPreOneHypercover.I₀) ↦ E.toPreOneHypercover.I₁ i.1 i.2).1)
      (c.inj
        b.fst (β := fun (i : E.toPreOneHypercover.I₀ × E.toPreOneHypercover.I₀) ↦ E.toPreOneHypercover.I₁ i.1 i.2).2)
      (𝟙 S) ⋯ ⋯
equiv : E.toPreOneHypercover.I₁' ≃ E.I₀ × E.I₀ := Equiv.sigmaPUnit (E.toPreOneHypercover.I₀ × E.toPreOneHypercover.I₀)
hc' : IsColimit c'
⊢ IsLimit ((E.sigmaOfIsColimit hc).toPreOneHypercover.multifork F) ≃ IsLimit (E.toPreOneHypercover.multifork F)
have refine : IsLimit ((E.sigmaOfIsColimit hc).toPreOneHypercover.multifork F) ≃
  IsLimit ((E.toPreOneHypercover.sigmaOfIsColimit hc hc').multifork F)
Tactic: refine .trans ?_ (E.toPreOneHypercover.isLimitSigmaOfIsColimitEquiv hc hc' F)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.CoproductSheafCondition (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A : Type u_2
inst_1 : Category.{v_2, u_2} A
S : C
E : PreZeroHypercover.{w, v_1, u_1} S
inst_2 : E.HasPullbacks
c : Cofan.{w, v_1, u_1} E.X
hc : IsColimit c
huniv : IsUniversalColimit c
inst_3 : (E.sigmaOfIsColimit hc).HasPullbacks
inst_4 : ∀ (i : E.I₀), HasPullback (E.f i) ((E.sigmaOfIsColimit hc).f PUnit.unit)
F : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ A
inst_5 :
  PreservesLimit.{w, w, v_1, v_2, u_1, u_2} (J := Discrete E.toPreOneHypercover.I₀)
    (Discrete.functor fun (i : E.toPreOneHypercover.I₀) ↦ op (E.toPreOneHypercover.X i)) F
inst_6 :
  PreservesLimit.{w, w, v_1, v_2, u_1, u_2} (J := Discrete E.toPreOneHypercover.I₁')
    (Discrete.functor fun (i : E.toPreOneHypercover.I₁') ↦ op (E.toPreOneHypercover.Y' i)) F
this : HasPullback (Cofan.IsColimit.desc hc E.f) (Cofan.IsColimit.desc hc E.f)
c' : Cofan.{w, v_1, u_1} E.toPreOneHypercover.Y' :=
  Cofan.mk ((E.sigmaOfIsColimit hc).toPreOneHypercover.Y (i₁ := PUnit.unit) (i₂ := PUnit.unit) PUnit.unit)
    fun (b : E.toPreOneHypercover.I₁') ↦
    pullback.map
      (E.f b.fst (β := fun (i : E.toPreOneHypercover.I₀ × E.toPreOneHypercover.I₀) ↦ E.toPreOneHypercover.I₁ i.1 i.2).1)
      (E.f b.fst (β := fun (i : E.toPreOneHypercover.I₀ × E.toPreOneHypercover.I₀) ↦ E.toPreOneHypercover.I₁ i.1 i.2).2)
      ((E.sigmaOfIsColimit hc).f PUnit.unit) ((E.sigmaOfIsColimit hc).f PUnit.unit)
      (c.inj
        b.fst (β := fun (i : E.toPreOneHypercover.I₀ × E.toPreOneHypercover.I₀) ↦ E.toPreOneHypercover.I₁ i.1 i.2).1)
      (c.inj
        b.fst (β := fun (i : E.toPreOneHypercover.I₀ × E.toPreOneHypercover.I₀) ↦ E.toPreOneHypercover.I₁ i.1 i.2).2)
      (𝟙 S) ⋯ ⋯
equiv : E.toPreOneHypercover.I₁' ≃ E.I₀ × E.I₀ := Equiv.sigmaPUnit (E.toPreOneHypercover.I₀ × E.toPreOneHypercover.I₀)
hc' : IsColimit c'
⊢ IsLimit ((E.sigmaOfIsColimit hc).toPreOneHypercover.multifork F) ≃
    IsLimit ((E.toPreOneHypercover.sigmaOfIsColimit hc hc').multifork F)
have f : (E.sigmaOfIsColimit hc).toPreOneHypercover ≅ E.toPreOneHypercover.sigmaOfIsColimit hc hc'
Tactic: apply PreOneHypercover.isLimitEquivOfIso
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.CoverLifting (goal)
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
⊢ F.IsCocontinuous J K ↔ CoverPreserving K J G
have refine_1 : ∀ (h : F.IsCocontinuous J K) {U : D} {S : Sieve.{v_2, u_2} U},
  S ∈ (K : (a : D) → Set (Sieve a)) U →
    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 ⟨fun h ↦ ⟨?_⟩, fun h ↦ ⟨?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.CoverLifting (goal)
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
refine_1 :
  ∀ (h : F.IsCocontinuous J K) {U : D} {S : Sieve.{v_2, u_2} U},
    S ∈ (K : (a : D) → Set (Sieve a)) U →
      Membership.mem (γ := Set (Sieve.{v_1, u_1} (G.obj U))) ((J : (a : C) → Set (Sieve a)) (G.obj U))
        (Sieve.functorPushforward G S)
⊢ F.IsCocontinuous J K ↔ CoverPreserving K J G
have refine_2 : ∀ (h : CoverPreserving K J G) {U : C} {S : Sieve.{v_2, u_2} (F.obj U)},
  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: refine ⟨fun h ↦ ⟨?_⟩, fun h ↦ ⟨?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.CoverLifting (goal)
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
⊢ Membership.mem (γ := Set (Sieve.{v_1, u_1} (G.obj U))) ((J : (a : C) → Set (Sieve a)) (G.obj U))
    (Sieve.functorPushforward G S)
have refine_1 : Sieve.functorPullback F (Sieve.pullback (adj.counit.app U) S) ≤ Sieve.functorPushforward G S
Tactic: refine J.superset_covering ?_ <| h.cover_lift (K.pullback_stable (adj.counit.app _) hS)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.CoverLifting (goal)
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
have refine_2 : Sieve.pullback (adj.unit.app U) (Sieve.functorPushforward G S) ≤ Sieve.functorPullback F S
Tactic: refine J.superset_covering ?_ (J.pullback_stable (adj.unit.app U) <| h.cover_preserve hS)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.CoverLifting (goal)
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
⊢ (Sieve.pullback (adj.unit.app U) (Sieve.functorPushforward G S)).arrows f → (Sieve.functorPullback F S).arrows f
have 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
Tactic: ⟨Y, g, u, hg, heq⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.CoverLifting (goal)
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
⊢ (Sieve.functorPullback F S).arrows f
have refine_2 : F.map f = ((adj.homEquiv X Y).symm : (a : X ⟶ G.obj Y) → F.obj X ⟶ Y) u ≫ g
Tactic: suffices F.map f = (adj.homEquiv _ _).symm u ≫ g by
      simp [this, S.downward_closed hg]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.CoverLifting (hypothesis)
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.IsContinuous K J
have this : G.IsRightAdjoint
Tactic: have := adj.isRightAdjoint
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.CoverLifting (goal)
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
⊢ G.IsContinuous K J
have apply : CoverPreserving K J G
Tactic: apply Functor.isContinuous_of_coverPreserving (compatiblePreservingOfFlat J G)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.CoverLifting (goal)
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₂
⊢ 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
have simp : Eq (α := s.pt ⟶ F.obj (op W)) (s.ι { Y := G.obj Y₁, f := G.map p₁ ≫ f, hf := sorry } ≫ R.map (G.map g₁).op ≫ α.app (op W))
  (s.ι { Y := G.obj Y₂, f := G.map p₂ ≫ f, hf := sorry } ≫ R.map (G.map g₂).op ≫ α.app (op W))
Tactic: simp only [Category.assoc, ← α.naturality, Functor.comp_map,
        Functor.op_map, Quiver.Hom.unop_op]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.CoverLifting (goal)
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
⊢ 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)
have dsimp : CategoryStruct.comp (Y := R.obj (op (G.obj W)))
    (s.ι { Y := G.obj W, f := G.map g ≫ f, hf := sorry } :
      s.pt ⟶ (S.index R).left { Y := G.obj W, f := G.map g ≫ f, hf := sorry })
    (α.app (op W)) =
  s.ι i ≫ R.map h.op ≫ α.app (op W)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.CoverLifting (goal)
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
⊢ 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)
have simp : CategoryStruct.comp (Y := R.obj (op (G.obj W)))
    (s.ι { Y := G.obj W, f := G.map g ≫ f, hf := sorry } :
      s.pt ⟶ (S.index R).left { Y := G.obj W, f := G.map g ≫ f, hf := sorry })
    (α.app (op W)) =
  (s.ι i ≫ R.map h.op) ≫ α.app (op W)
Tactic: simp only [← Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.CoverLifting (goal)
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
⊢ 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)
have e_a : s.ι { Y := G.obj W, f := G.map g ≫ f, hf := sorry } = s.ι i ≫ R.map h.op
Tactic: congr 1
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.CoverLifting (goal)
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 Y' : C
f : G.obj Y ⟶ X
f' : G.obj Y' ⟶ X
W : C
a : W ⟶ Y
b : W ⟶ Y'
w : G.map a ≫ f = G.map b ≫ f'
⊢ liftAux hF α s f ≫ F.map a.op = liftAux hF α s f' ≫ F.map b.op
have h : ∀
  (I :
    GrothendieckTopology.Cover.Arrow
      (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} W) ↦ S ∈ (J : (a : C) → Set (Sieve a)) W)
        (Sieve.functorPullback G (Sieve.pullback (G.map a ≫ f) (↑S : Sieve X))) sorry)),
  (liftAux hF α s f ≫ F.map a.op) ≫ F.map I.f.op = (liftAux hF α s f' ≫ F.map b.op) ≫ F.map I.f.op
Tactic: apply hF.hom_ext ⟨_, G.cover_lift J K (K.pullback_stable (G.map a ≫ f) S.2)⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.CoverLifting (goal)
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 Y' : C
f : G.obj Y ⟶ X
f' : G.obj Y' ⟶ X
W : C
a : W ⟶ Y
b : W ⟶ Y'
w : G.map a ≫ f = G.map b ≫ f'
T : C
g : T ⟶ W
hg :
  (↑(Subtype.mk (p := fun (S : Sieve.{v_1, u_1} W) ↦ S ∈ (J : (a : C) → Set (Sieve a)) W)
            (Sieve.functorPullback G (Sieve.pullback (G.map a ≫ f) (↑S : Sieve X))) ⋯) :
        Sieve W).arrows
    g
⊢ (liftAux hF α s f ≫ F.map a.op) ≫
      F.map
        { Y := T, f := g, hf := hg :
              GrothendieckTopology.Cover.Arrow
                (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} W) ↦ S ∈ (J : (a : C) → Set (Sieve a)) W)
                  (Sieve.functorPullback G (Sieve.pullback (G.map a ≫ f) (↑S : Sieve X))) ⋯) }.f.op =
    (liftAux hF α s f' ≫ F.map b.op) ≫ F.map { Y := T, f := g, hf := hg }.f.op
have h : (liftAux hF α s f ≫ F.map a.op) ≫ F.map g.op = (liftAux hF α s f' ≫ F.map b.op) ≫ F.map g.op
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.CoverLifting (hypothesis)
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 Y' : C
f : G.obj Y ⟶ X
f' : G.obj Y' ⟶ X
W : C
a : W ⟶ Y
b : W ⟶ Y'
w : G.map a ≫ f = G.map b ≫ f'
T : C
g : T ⟶ W
hg :
  (↑(Subtype.mk (p := fun (S : Sieve.{v_1, u_1} W) ↦ S ∈ (J : (a : C) → Set (Sieve a)) W)
            (Sieve.functorPullback G (Sieve.pullback (G.map a ≫ f) (↑S : Sieve X))) ⋯) :
        Sieve W).arrows
    g
⊢ (liftAux hF α s f ≫ F.map a.op) ≫ F.map g.op = (liftAux hF α s f' ≫ F.map b.op) ≫ F.map g.op
have eq₁ : liftAux hF α s f ≫ F.map (g ≫ a).op =
  s.ι { Y := G.obj T, f := G.map g ≫ G.map a ≫ f, hf := hg } ≫ R.map (Quiver.Hom.op (𝟙 (G.obj T))) ≫ α.app (op T)
Tactic: have eq₁ := liftAux_map hF α s f (g ≫ a) ⟨_, _, hg⟩ (𝟙 _) (by simp)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.CoverLifting (hypothesis)
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 Y' : C
f : G.obj Y ⟶ X
f' : G.obj Y' ⟶ X
W : C
a : W ⟶ Y
b : W ⟶ Y'
w : G.map a ≫ f = G.map b ≫ f'
T : C
g : T ⟶ W
hg :
  (↑(Subtype.mk (p := fun (S : Sieve.{v_1, u_1} W) ↦ S ∈ (J : (a : C) → Set (Sieve a)) W)
            (Sieve.functorPullback G (Sieve.pullback (G.map a ≫ f) (↑S : Sieve X))) ⋯) :
        Sieve W).arrows
    g
eq₁ :
  liftAux hF α s f ≫ F.map (g ≫ a).op =
    s.ι { Y := G.obj T, f := G.map g ≫ G.map a ≫ f, hf := hg } ≫ R.map (Quiver.Hom.op (𝟙 (G.obj T))) ≫ α.app (op T)
⊢ (liftAux hF α s f ≫ F.map a.op) ≫ F.map g.op = (liftAux hF α s f' ≫ F.map b.op) ≫ F.map g.op
have eq₂ : liftAux hF α s f' ≫ F.map (g ≫ b).op =
  s.ι { Y := G.obj T, f := G.map g ≫ G.map a ≫ f, hf := hg } ≫ R.map (Quiver.Hom.op (𝟙 (G.obj T))) ≫ α.app (op T)
Tactic: have eq₂ := liftAux_map hF α s f' (g ≫ b) ⟨_, _, hg⟩ (𝟙 _) (by simp [w])
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.CoverLifting (hypothesis)
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 Y' : C
f : G.obj Y ⟶ X
f' : G.obj Y' ⟶ X
W : C
a : W ⟶ Y
b : W ⟶ Y'
w : G.map a ≫ f = G.map b ≫ f'
T : C
g : T ⟶ W
hg :
  (↑(Subtype.mk (p := fun (S : Sieve.{v_1, u_1} W) ↦ S ∈ (J : (a : C) → Set (Sieve a)) W)
            (Sieve.functorPullback G (Sieve.pullback (G.map a ≫ f) (↑S : Sieve X))) ⋯) :
        Sieve W).arrows
    g
eq₁ :
  Eq (α := s.pt ⟶ F.obj (op T)) (liftAux hF α s f ≫ F.map (a.op ≫ g.op))
    (s.ι { Y := G.obj T, f := G.map g ≫ G.map a ≫ f, hf := hg } ≫ R.map (𝟙 (op (G.obj T))) ≫ α.app (op T))
eq₂ :
  Eq (α := s.pt ⟶ F.obj (op T)) (liftAux hF α s f' ≫ F.map (b.op ≫ g.op))
    (s.ι { Y := G.obj T, f := G.map g ≫ G.map a ≫ f, hf := hg } ≫ R.map (𝟙 (op (G.obj T))) ≫ α.app (op T))
⊢ (liftAux hF α s f ≫ F.map a.op) ≫ F.map g.op = (liftAux hF α s f' ≫ F.map b.op) ≫ F.map g.op
have eq₃ : liftAux hF α s f ≫ F.map a.op ≫ F.map g.op =
  CategoryStruct.comp (Y := R.obj (op (G.obj T)))
    (s.ι { Y := G.obj T, f := G.map g ≫ G.map a ≫ f, hf := hg } :
      s.pt ⟶ (S.index R).left { Y := G.obj T, f := G.map g ≫ G.map a ≫ f, hf := hg })
    (α.app (op T))
Tactic: simp only [Functor.map_comp, Functor.map_id, Category.id_comp] at eq₁ eq₂
Cleared hypotheses: eq₁, eq₂