awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense (goal)
Goal:
C₀ : Type u₀
C : Type u
inst : Category.{v₀, u₀} C₀
inst_1 : Category.{v, u} C
F : Functor.{v₀, v, u₀, u} C₀ C
J₀ : GrothendieckTopology.{v₀, u₀} C₀
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_2 : Category.{v', u'} A
inst_3 : IsDenseSubsite J₀ J F
data : (X : C) → OneHypercoverDenseData.{u_1, v₀, v, u₀, u} F J₀ J X
G : Functor.{v, v', u, u'} Cᵒᵖ A
hG₀ : Presheaf.IsSheaf J₀ (F.op ⋙ G)
hG : (X : C) → IsLimit ((data X).toOneHypercover.multifork G)
X : C
S : J.Cover X
s : Multifork (S.index G)
a : S.Arrow
i : PreOneHypercoverDenseData.I₀ (S := a.Y) (toPreOneHypercoverDenseData (data a.Y))
X₀ : C₀
b : X₀ ⟶ PreOneHypercoverDenseData.X (toPreOneHypercoverDenseData (data a.Y)) i
Y : C
j : (data X).I₀
c : F.obj X₀ ⟶ F.obj ((data X).X j)
fac₁ : c ≫ (data X).f j = F.map b ≫ PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data a.Y)) i ≫ a.f
Y₀ : C₀
d : Y₀ ⟶ X₀
e : Y₀ ⟶ (data X).X j
fac₂ : F.map e = F.map d ≫ c
he : (↑S : Sieve X).arrows (F.map e ≫ (data X).f j)
⊢ liftAux hG₀ s j ≫ G.map c.op ≫ G.map (F.map d).op =
    s.ι a ≫ G.map (F.map d ≫ F.map b ≫ PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data a.Y)) i).op
have rw : s.ι { Y := F.obj Y₀, f := F.map e ≫ (data X).f j, hf := he } =
  s.ι a ≫ G.map (F.map d ≫ F.map b ≫ PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data a.Y)) i).op
Tactic: rw [← Functor.map_comp, ← op_comp, ← fac₂, liftAux_fac _ _ _ he]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense (goal)
Goal:
C₀ : Type u₀
C : Type u
inst : Category.{v₀, u₀} C₀
inst_1 : Category.{v, u} C
F : Functor.{v₀, v, u₀, u} C₀ C
J₀ : GrothendieckTopology.{v₀, u₀} C₀
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_2 : Category.{v', u'} A
inst_3 : IsDenseSubsite J₀ J F
data : (X : C) → OneHypercoverDenseData.{u_1, v₀, v, u₀, u} F J₀ J X
G : Functor.{v, v', u, u'} Cᵒᵖ A
hG₀ : Presheaf.IsSheaf J₀ (F.op ⋙ G)
hG : (X : C) → IsLimit ((data X).toOneHypercover.multifork G)
X : C
S : J.Cover X
s : Multifork (S.index G)
f₁ f₂ : s.pt ⟶ G.obj (op X)
h : ∀ (a : S.Arrow), f₁ ≫ G.map a.f.op = f₂ ≫ G.map a.f.op
i : (data X).toOneHypercover.multicospanShape.L
⊢ f₁ ≫ ((data X).toOneHypercover.multifork G).ι i = f₂ ≫ ((data X).toOneHypercover.multifork G).ι i
have refine : ∀
  (I :
    GrothendieckTopology.Cover.Arrow
      (Subtype.mk (p := fun (S : Sieve.{v₀, u₀} ((data X).X i)) ↦
        Membership.mem (γ := Set (Sieve.{v₀, u₀} ((data X).X i))) ((J₀ : (a : C₀) → Set (Sieve a)) ((data X).X i)) S)
        (Sieve.functorPullback F (Sieve.pullback ((data X).f i) (↑S : Sieve X))) sorry)),
  (f₁ ≫ ((data X).toOneHypercover.multifork G).ι i) ≫ (F.op ⋙ G).map I.f.op =
    (f₂ ≫ ((data X).toOneHypercover.multifork G).ι i) ≫ (F.op ⋙ G).map I.f.op
Tactic: refine Presheaf.IsSheaf.hom_ext hG₀
      ⟨_, cover_lift F J₀ _ (J.pullback_stable ((data X).f i) S.2)⟩ _ _ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense (goal)
Goal:
C₀ : Type u₀
C : Type u
inst : Category.{v₀, u₀} C₀
inst_1 : Category.{v, u} C
F : Functor.{v₀, v, u₀, u} C₀ C
J₀ : GrothendieckTopology.{v₀, u₀} C₀
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_2 : Category.{v', u'} A
inst_3 : IsDenseSubsite J₀ J F
data : (X : C) → OneHypercoverDenseData.{u_1, v₀, v, u₀, u} F J₀ J X
G : Functor.{v, v', u, u'} Cᵒᵖ A
hG₀ : Presheaf.IsSheaf J₀ (F.op ⋙ G)
hG : (X : C) → IsLimit ((data X).toOneHypercover.multifork G)
X : C
S : J.Cover X
s : Multifork (S.index G)
f₁ f₂ : s.pt ⟶ G.obj (op X)
h : ∀ (a : S.Arrow), f₁ ≫ G.map a.f.op = f₂ ≫ G.map a.f.op
i : (data X).toOneHypercover.multicospanShape.L
X₀ : C₀
a : X₀ ⟶ (data X).X i
ha :
  (↑(Subtype.mk (p := fun (S : Sieve.{v₀, u₀} ((data X).X i)) ↦
            Membership.mem (γ := Set (Sieve.{v₀, u₀} ((data X).X i))) ((J₀ : (a : C₀) → Set (Sieve a)) ((data X).X i))
              S)
            (Sieve.functorPullback F (Sieve.pullback ((data X).f i) (↑S : Sieve X))) ⋯) :
        Sieve ((data X).X i)).arrows
    a
⊢ (f₁ ≫ ((data X).toOneHypercover.multifork G).ι i) ≫
      (F.op ⋙ G).map
        { Y := X₀, f := a, hf := ha :
              GrothendieckTopology.Cover.Arrow
                (Subtype.mk (p := fun (S : Sieve.{v₀, u₀} ((data X).X i)) ↦
                  Membership.mem (γ := Set (Sieve.{v₀, u₀} ((data X).X i)))
                    ((J₀ : (a : C₀) → Set (Sieve a)) ((data X).X i)) S)
                  (Sieve.functorPullback F (Sieve.pullback ((data X).f i) (↑S : Sieve X))) ⋯) }.f.op =
    (f₂ ≫ ((data X).toOneHypercover.multifork G).ι i) ≫ (F.op ⋙ G).map { Y := X₀, f := a, hf := ha }.f.op
have dsimp : (f₁ ≫ G.map ((data X).f i).op) ≫ G.map (F.map a).op = (f₂ ≫ G.map ((data X).f i).op) ≫ G.map (F.map a).op
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense (goal)
Goal:
C₀ : Type u₀
C : Type u
inst : Category.{v₀, u₀} C₀
inst_1 : Category.{v, u} C
F : Functor.{v₀, v, u₀, u} C₀ C
J₀ : GrothendieckTopology.{v₀, u₀} C₀
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_2 : Category.{v', u'} A
inst_3 : IsDenseSubsite J₀ J F
data : (X : C) → OneHypercoverDenseData.{u_1, v₀, v, u₀, u} F J₀ J X
G : Functor.{v, v', u, u'} Cᵒᵖ A
hG₀ : Presheaf.IsSheaf J₀ (F.op ⋙ G)
hG : (X : C) → IsLimit ((data X).toOneHypercover.multifork G)
X : C
S : J.Cover X
s : Multifork (S.index G)
f₁ f₂ : s.pt ⟶ G.obj (op X)
h : ∀ (a : S.Arrow), f₁ ≫ G.map a.f.op = f₂ ≫ G.map a.f.op
i : (data X).toOneHypercover.multicospanShape.L
X₀ : C₀
a : X₀ ⟶ (data X).X i
ha :
  (↑(Subtype.mk (p := fun (S : Sieve.{v₀, u₀} ((data X).X i)) ↦
            Membership.mem (γ := Set (Sieve.{v₀, u₀} ((data X).X i))) ((J₀ : (a : C₀) → Set (Sieve a)) ((data X).X i))
              S)
            (Sieve.functorPullback F (Sieve.pullback ((data X).f i) (↑S : Sieve X))) ⋯) :
        Sieve ((data X).X i)).arrows
    a
⊢ (f₁ ≫ G.map ((data X).f i).op) ≫ G.map (F.map a).op = (f₂ ≫ G.map ((data X).f i).op) ≫ G.map (F.map a).op
have simp : f₁ ≫ G.map (F.map a ≫ (data X).f i).op = f₂ ≫ G.map (F.map a ≫ (data X).f i).op
Tactic: simp only [assoc, ← Functor.map_comp, ← op_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense (goal)
Goal:
C₀ : Type u₀
C : Type u
inst : Category.{v₀, u₀} C₀
inst_1 : Category.{v, u} C
F : Functor.{v₀, v, u₀, u} C₀ C
J₀ : GrothendieckTopology.{v₀, u₀} C₀
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_2 : Category.{v', u'} A
inst_3 : IsDenseSubsite J₀ J F
data : (X : C) → OneHypercoverDenseData.{u_1, v₀, v, u₀, u} F J₀ J X
G : Functor.{v, v', u, u'} Cᵒᵖ A
⊢ Presheaf.IsSheaf J G ↔
    Presheaf.IsSheaf J₀ (F.op ⋙ G) ∧ ∀ (X : C), Nonempty (IsLimit ((data X).toOneHypercover.multifork G))
have refine : (Presheaf.IsSheaf J₀ (F.op ⋙ G) ∧ ∀ (X : C), Nonempty (IsLimit ((data X).toOneHypercover.multifork G))) →
  ∀ (hG₀ : Presheaf.IsSheaf J₀ (F.op ⋙ G)) (hG : ∀ (X : C), Nonempty (IsLimit ((data X).toOneHypercover.multifork G))),
    Presheaf.IsSheaf J G
Tactic: refine ⟨fun hG ↦ ⟨op_comp_isSheaf F J₀ J ⟨_, hG⟩,
    fun X ↦ ⟨(data X).toOneHypercover.isLimitMultifork ⟨G, hG⟩⟩⟩, fun ⟨hG₀, hG⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense (goal)
Goal:
C₀ : Type u₀
C : Type u
inst : Category.{v₀, u₀} C₀
inst_1 : Category.{v, u} C
F : Functor.{v₀, v, u₀, u} C₀ C
J₀ : GrothendieckTopology.{v₀, u₀} C₀
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_2 : Category.{v', u'} A
inst_3 : IsDenseSubsite J₀ J F
data : (X : C) → OneHypercoverDenseData.{u_1, v₀, v, u₀, u} F J₀ J X
G : Functor.{v, v', u, u'} Cᵒᵖ A
h : Presheaf.IsSheaf J₀ (F.op ⋙ G) ∧ ∀ (X : C), Nonempty (IsLimit ((data X).toOneHypercover.multifork G))
hG₀ : Presheaf.IsSheaf J₀ (F.op ⋙ G)
hG : ∀ (X : C), Nonempty (IsLimit ((data X).toOneHypercover.multifork G))
⊢ Presheaf.IsSheaf J G
have rw : ∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork G))
Tactic: rw [Presheaf.isSheaf_iff_multifork]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense (goal)
Goal:
C₀ : Type u₀
C : Type u
inst : Category.{v₀, u₀} C₀
inst_1 : Category.{v, u} C
F : Functor.{v₀, v, u₀, u} C₀ C
J₀ : GrothendieckTopology.{v₀, u₀} C₀
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_2 : Category.{v', u'} A
inst_3 : IsDenseSubsite J₀ J F
data : (X : C) → OneHypercoverDenseData.{u_1, v₀, v, u₀, u} F J₀ J X
G : Functor.{v, v', u, u'} Cᵒᵖ A
h : Presheaf.IsSheaf J₀ (F.op ⋙ G) ∧ ∀ (X : C), Nonempty (IsLimit ((data X).toOneHypercover.multifork G))
hG₀ : Presheaf.IsSheaf J₀ (F.op ⋙ G)
hG : ∀ (X : C), Nonempty (IsLimit ((data X).toOneHypercover.multifork G))
⊢ ∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork G))
have replace : ∀ (hG : (X : C) → IsLimit ((data X).toOneHypercover.multifork G)) (X : C) (S : J.Cover X),
  Nonempty (IsLimit (S.multifork G))
Tactic: replace hG := fun X ↦ (hG X).some
Cleared hypotheses: hG
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense (goal)
Goal:
C₀ : Type u₀
C : Type u
inst : Category.{v₀, u₀} C₀
inst_1 : Category.{v, u} C
F : Functor.{v₀, v, u₀, u} C₀ C
J₀ : GrothendieckTopology.{v₀, u₀} C₀
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_2 : Category.{v', u'} A
inst_3 : IsDenseSubsite J₀ J F
data : (X : C) → OneHypercoverDenseData.{w, v₀, v, u₀, u} F J₀ J X
inst_4 : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf.{v₀, v', u₀, u'} J₀ A
X : C
i₁ i₂ : (data X).I₀
Y₀ : C₀
p₁ : F.obj Y₀ ⟶ F.obj ((data X).X i₁)
p₂ : F.obj Y₀ ⟶ F.obj ((data X).X i₂)
fac : p₁ ≫ (data X).f i₁ = p₂ ≫ (data X).f i₂
⊢ Eq (α := presheafObj data G₀ X ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op Y₀))
    (presheafObjπ data G₀ X i₁ ≫ IsDenseSubsite.mapPreimage J F G₀ p₁)
    (presheafObjπ data G₀ X i₂ ≫ IsDenseSubsite.mapPreimage J F G₀ p₂)
have refine : ∀
  (I :
    GrothendieckTopology.Cover.Arrow
      (Subtype.mk (p := fun (S : Sieve.{v₀, u₀} Y₀) ↦ S ∈ (J₀ : (a : C₀) → Set (Sieve a)) Y₀)
        (F.imageSieve p₁ ⊓ F.imageSieve p₂) sorry)),
  Eq (α := presheafObj data G₀ X ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op I.Y))
    ((presheafObjπ data G₀ X i₁ ≫ IsDenseSubsite.mapPreimage J F G₀ p₁) ≫ G₀.obj (P := Presheaf.IsSheaf J₀).map I.f.op)
    ((presheafObjπ data G₀ X i₂ ≫ IsDenseSubsite.mapPreimage J F G₀ p₂) ≫ G₀.obj (P := Presheaf.IsSheaf J₀).map I.f.op)
Tactic: refine Presheaf.IsSheaf.hom_ext G₀.property ⟨_,
    J₀.intersection_covering (IsDenseSubsite.imageSieve_mem J₀ J F p₁)
      (IsDenseSubsite.imageSieve_mem J₀ J F p₂)⟩ _ _ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense (goal)
Goal:
C₀ : Type u₀
C : Type u
inst : Category.{v₀, u₀} C₀
inst_1 : Category.{v, u} C
F : Functor.{v₀, v, u₀, u} C₀ C
J₀ : GrothendieckTopology.{v₀, u₀} C₀
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_2 : Category.{v', u'} A
inst_3 : IsDenseSubsite J₀ J F
data : (X : C) → OneHypercoverDenseData.{w, v₀, v, u₀, u} F J₀ J X
inst_4 : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf.{v₀, v', u₀, u'} J₀ A
X : C
X₀ Y₀ : C₀
f : F.obj X₀ ⟶ X
g : Y₀ ⟶ X₀
h₁ h₂ : (data X).SieveStruct f g
⊢ Eq (α := presheafObj data G₀ X ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op Y₀)) (res data G₀ h₁) (res data G₀ h₂)
have refine : ∀
  (I :
    GrothendieckTopology.Cover.Arrow
      (Subtype.mk (p := fun (S : Sieve.{v₀, u₀} Y₀) ↦ S ∈ (J₀ : (a : C₀) → Set (Sieve a)) Y₀)
        (F.imageSieve h₁.q ⊓ F.imageSieve h₂.q) sorry)),
  Eq (α := presheafObj data G₀ X ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op I.Y))
    (res data G₀ h₁ ≫ G₀.obj (P := Presheaf.IsSheaf J₀).map I.f.op)
    (res data G₀ h₂ ≫ G₀.obj (P := Presheaf.IsSheaf J₀).map I.f.op)
Tactic: refine Presheaf.IsSheaf.hom_ext G₀.property
    ⟨_, J₀.intersection_covering (IsDenseSubsite.imageSieve_mem J₀ J F h₁.q)
      (IsDenseSubsite.imageSieve_mem J₀ J F h₂.q)⟩ _ _ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense (goal)
Goal:
C₀ : Type u₀
C : Type u
inst : Category.{v₀, u₀} C₀
inst_1 : Category.{v, u} C
F : Functor.{v₀, v, u₀, u} C₀ C
J₀ : GrothendieckTopology.{v₀, u₀} C₀
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_2 : Category.{v', u'} A
inst_3 : IsDenseSubsite J₀ J F
data : (X : C) → OneHypercoverDenseData.{w, v₀, v, u₀, u} F J₀ J X
inst_4 : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf.{v₀, v', u₀, u'} J₀ A
X : C
X₀ Y₀ : C₀
f : F.obj X₀ ⟶ X
g : Y₀ ⟶ X₀
h₁ h₂ : (data X).SieveStruct f g
Z₀ : C₀
a : Z₀ ⟶ Y₀
b₁ : Z₀ ⟶ (data X).X h₁.i₀
w₁ : F.map b₁ = F.map a ≫ h₁.q
b₂ : Z₀ ⟶ (data X).X h₂.i₀
w₂ : F.map b₂ = F.map a ≫ h₂.q
⊢ F.map b₁ ≫ (data X).f h₁.i₀ = F.map b₂ ≫ (data X).f h₂.i₀
have rw : (F.map a ≫ h₁.q) ≫ (data X).f h₁.i₀ = F.map b₂ ≫ (data X).f h₂.i₀
Tactic: rw [w₁, w₂, assoc, assoc, h₁.fac, h₂.fac]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense (goal)
Goal:
C₀ : Type u₀
C : Type u
inst : Category.{v₀, u₀} C₀
inst_1 : Category.{v, u} C
F : Functor.{v₀, v, u₀, u} C₀ C
J₀ : GrothendieckTopology.{v₀, u₀} C₀
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_2 : Category.{v', u'} A
inst_3 : IsDenseSubsite J₀ J F
data : (X : C) → OneHypercoverDenseData.{w, v₀, v, u₀, u} F J₀ J X
inst_4 : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf.{v₀, v', u₀, u'} J₀ A
X : C
X₀ Y₀ : C₀
f : F.obj X₀ ⟶ X
g : Y₀ ⟶ X₀
h₁ h₂ : (data X).SieveStruct f g
Z₀ : C₀
a : Z₀ ⟶ Y₀
b₁ : Z₀ ⟶ (data X).X h₁.i₀
w₁ : F.map b₁ = F.map a ≫ h₁.q
b₂ : Z₀ ⟶ (data X).X h₂.i₀
w₂ : F.map b₂ = F.map a ≫ h₂.q
rw : (F.map a ≫ h₁.q) ≫ (data X).f h₁.i₀ = F.map b₂ ≫ (data X).f h₂.i₀
⊢ F.map b₁ ≫ (data X).f h₁.i₀ = F.map b₂ ≫ (data X).f h₂.i₀
have rw₁ : (F.map a ≫ h₁.q) ≫ (data X).f h₁.i₀ = (F.map a ≫ h₂.q) ≫ (data X).f h₂.i₀
Tactic: rw [w₁, w₂, assoc, assoc, h₁.fac, h₂.fac]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense (goal)
Goal:
C₀ : Type u₀
C : Type u
inst : Category.{v₀, u₀} C₀
inst_1 : Category.{v, u} C
F : Functor.{v₀, v, u₀, u} C₀ C
J₀ : GrothendieckTopology.{v₀, u₀} C₀
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_2 : Category.{v', u'} A
inst_3 : IsDenseSubsite J₀ J F
data : (X : C) → OneHypercoverDenseData.{w, v₀, v, u₀, u} F J₀ J X
inst_4 : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf.{v₀, v', u₀, u'} J₀ A
X : C
X₀ Y₀ : C₀
f : F.obj X₀ ⟶ X
g : Y₀ ⟶ X₀
h₁ h₂ : (data X).SieveStruct f g
Z₀ : C₀
a : Z₀ ⟶ Y₀
b₁ : Z₀ ⟶ (data X).X h₁.i₀
w₁ : F.map b₁ = F.map a ≫ h₁.q
b₂ : Z₀ ⟶ (data X).X h₂.i₀
w₂ : F.map b₂ = F.map a ≫ h₂.q
rw : (F.map a ≫ h₁.q) ≫ (data X).f h₁.i₀ = F.map b₂ ≫ (data X).f h₂.i₀
rw₁ : (F.map a ≫ h₁.q) ≫ (data X).f h₁.i₀ = (F.map a ≫ h₂.q) ≫ (data X).f h₂.i₀
⊢ F.map b₁ ≫ (data X).f h₁.i₀ = F.map b₂ ≫ (data X).f h₂.i₀
have rw₂ : F.map a ≫ h₁.q ≫ (data X).f h₁.i₀ = (F.map a ≫ h₂.q) ≫ (data X).f h₂.i₀
Tactic: rw [w₁, w₂, assoc, assoc, h₁.fac, h₂.fac]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense (goal)
Goal:
C₀ : Type u₀
C : Type u
inst : Category.{v₀, u₀} C₀
inst_1 : Category.{v, u} C
F : Functor.{v₀, v, u₀, u} C₀ C
J₀ : GrothendieckTopology.{v₀, u₀} C₀
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_2 : Category.{v', u'} A
inst_3 : IsDenseSubsite J₀ J F
data : (X : C) → OneHypercoverDenseData.{w, v₀, v, u₀, u} F J₀ J X
inst_4 : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf.{v₀, v', u₀, u'} J₀ A
X : C
X₀ Y₀ : C₀
f : F.obj X₀ ⟶ X
g : Y₀ ⟶ X₀
h₁ h₂ : (data X).SieveStruct f g
Z₀ : C₀
a : Z₀ ⟶ Y₀
b₁ : Z₀ ⟶ (data X).X h₁.i₀
w₁ : F.map b₁ = F.map a ≫ h₁.q
b₂ : Z₀ ⟶ (data X).X h₂.i₀
w₂ : F.map b₂ = F.map a ≫ h₂.q
rw : (F.map a ≫ h₁.q) ≫ (data X).f h₁.i₀ = F.map b₂ ≫ (data X).f h₂.i₀
rw₁ : (F.map a ≫ h₁.q) ≫ (data X).f h₁.i₀ = (F.map a ≫ h₂.q) ≫ (data X).f h₂.i₀
rw₂ : F.map a ≫ h₁.q ≫ (data X).f h₁.i₀ = (F.map a ≫ h₂.q) ≫ (data X).f h₂.i₀
⊢ F.map b₁ ≫ (data X).f h₁.i₀ = F.map b₂ ≫ (data X).f h₂.i₀
have rw₃ : F.map a ≫ h₁.q ≫ (data X).f h₁.i₀ = F.map a ≫ h₂.q ≫ (data X).f h₂.i₀
Tactic: rw [w₁, w₂, assoc, assoc, h₁.fac, h₂.fac]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense (goal)
Goal:
C₀ : Type u₀
C : Type u
inst : Category.{v₀, u₀} C₀
inst_1 : Category.{v, u} C
F : Functor.{v₀, v, u₀, u} C₀ C
J₀ : GrothendieckTopology.{v₀, u₀} C₀
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_2 : Category.{v', u'} A
inst_3 : IsDenseSubsite J₀ J F
data : (X : C) → OneHypercoverDenseData.{w, v₀, v, u₀, u} F J₀ J X
inst_4 : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf.{v₀, v', u₀, u'} J₀ A
X : C
X₀ Y₀ : C₀
f : F.obj X₀ ⟶ X
g : Y₀ ⟶ X₀
h₁ h₂ : (data X).SieveStruct f g
Z₀ : C₀
a : Z₀ ⟶ Y₀
b₁ : Z₀ ⟶ (data X).X h₁.i₀
w₁ : F.map b₁ = F.map a ≫ h₁.q
b₂ : Z₀ ⟶ (data X).X h₂.i₀
w₂ : F.map b₂ = F.map a ≫ h₂.q
rw : (F.map a ≫ h₁.q) ≫ (data X).f h₁.i₀ = F.map b₂ ≫ (data X).f h₂.i₀
rw₁ : (F.map a ≫ h₁.q) ≫ (data X).f h₁.i₀ = (F.map a ≫ h₂.q) ≫ (data X).f h₂.i₀
rw₂ : F.map a ≫ h₁.q ≫ (data X).f h₁.i₀ = (F.map a ≫ h₂.q) ≫ (data X).f h₂.i₀
rw₃ : F.map a ≫ h₁.q ≫ (data X).f h₁.i₀ = F.map a ≫ h₂.q ≫ (data X).f h₂.i₀
⊢ F.map b₁ ≫ (data X).f h₁.i₀ = F.map b₂ ≫ (data X).f h₂.i₀
have rw₄ : F.map a ≫ F.map g ≫ f = F.map a ≫ h₂.q ≫ (data X).f h₂.i₀
Tactic: rw [w₁, w₂, assoc, assoc, h₁.fac, h₂.fac]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense (goal)
Goal:
C₀ : Type u₀
C : Type u
inst : Category.{v₀, u₀} C₀
inst_1 : Category.{v, u} C
F : Functor.{v₀, v, u₀, u} C₀ C
J₀ : GrothendieckTopology.{v₀, u₀} C₀
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_2 : Category.{v', u'} A
inst_3 : IsDenseSubsite J₀ J F
data : (X : C) → OneHypercoverDenseData.{w, v₀, v, u₀, u} F J₀ J X
inst_4 : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf.{v₀, v', u₀, u'} J₀ A
X : C
X₀ Y₀ : C₀
f : F.obj X₀ ⟶ X
g : Y₀ ⟶ X₀
h₁ h₂ : (data X).SieveStruct f g
Z₀ : C₀
a : Z₀ ⟶ Y₀
b₁ : Z₀ ⟶ (data X).X h₁.i₀
w₁ : F.map b₁ = F.map a ≫ h₁.q
b₂ : Z₀ ⟶ (data X).X h₂.i₀
w₂ : F.map b₂ = F.map a ≫ h₂.q
rw : (F.map a ≫ h₁.q) ≫ (data X).f h₁.i₀ = F.map b₂ ≫ (data X).f h₂.i₀
rw₁ : (F.map a ≫ h₁.q) ≫ (data X).f h₁.i₀ = (F.map a ≫ h₂.q) ≫ (data X).f h₂.i₀
rw₂ : F.map a ≫ h₁.q ≫ (data X).f h₁.i₀ = (F.map a ≫ h₂.q) ≫ (data X).f h₂.i₀
rw₃ : F.map a ≫ h₁.q ≫ (data X).f h₁.i₀ = F.map a ≫ h₂.q ≫ (data X).f h₂.i₀
rw₄ : F.map a ≫ F.map g ≫ f = F.map a ≫ h₂.q ≫ (data X).f h₂.i₀
⊢ F.map b₁ ≫ (data X).f h₁.i₀ = F.map b₂ ≫ (data X).f h₂.i₀
have rw₅ : F.map a ≫ F.map g ≫ f = F.map a ≫ F.map g ≫ f
Tactic: rw [w₁, w₂, assoc, assoc, h₁.fac, h₂.fac]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense (goal)
Goal:
C₀ : Type u₀
C : Type u
inst : Category.{v₀, u₀} C₀
inst_1 : Category.{v, u} C
F : Functor.{v₀, v, u₀, u} C₀ C
J₀ : GrothendieckTopology.{v₀, u₀} C₀
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_2 : Category.{v', u'} A
inst_3 : IsDenseSubsite J₀ J F
data : (X : C) → OneHypercoverDenseData.{w, v₀, v, u₀, u} F J₀ J X
inst_4 : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf.{v₀, v', u₀, u'} J₀ A
X : C
X₀ Y₀ : C₀
f : F.obj X₀ ⟶ X
g : Y₀ ⟶ X₀
h₁ h₂ : (data X).SieveStruct f g
Z₀ : C₀
a : Z₀ ⟶ Y₀
b₁ : Z₀ ⟶ (data X).X h₁.i₀
w₁ : F.map b₁ = F.map a ≫ h₁.q
b₂ : Z₀ ⟶ (data X).X h₂.i₀
w₂ : F.map b₂ = F.map a ≫ h₂.q
⊢ Eq (α :=
    presheafObj data G₀ X ⟶
      G₀.obj (P := Presheaf.IsSheaf J₀).obj
        (op
          (GrothendieckTopology.Cover.Arrow.Y (J := J₀) (S :=
            Subtype.mk (p := fun (S : Sieve.{v₀, u₀} Y₀) ↦ S ∈ (J₀ : (a : C₀) → Set (Sieve a)) Y₀)
              (F.imageSieve h₁.q ⊓ F.imageSieve h₂.q) ⋯)
            { Y := Z₀, f := a, hf := ⋯ })))
    (res data G₀ h₁ ≫
      G₀.obj (P := Presheaf.IsSheaf J₀).map
        (Quiver.Hom.op (GrothendieckTopology.Cover.Arrow.f { Y := Z₀, f := a, hf := ⋯ })))
    (res data G₀ h₂ ≫
      G₀.obj (P := Presheaf.IsSheaf J₀).map
        (Quiver.Hom.op (GrothendieckTopology.Cover.Arrow.f { Y := Z₀, f := a, hf := ⋯ })))
have refine : ∀
  (I :
    GrothendieckTopology.Cover.Arrow
      (Subtype.mk (p := fun (S : Sieve.{v₀, u₀} Z₀) ↦ S ∈ (J₀ : (a : C₀) → Set (Sieve a)) Z₀) ((data X).sieve₁₀ b₁ b₂)
        sorry)),
  Eq (α := presheafObj data G₀ X ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op I.Y))
    ((res data G₀ h₁ ≫
        G₀.obj (P := Presheaf.IsSheaf J₀).map
          (Quiver.Hom.op (GrothendieckTopology.Cover.Arrow.f { Y := Z₀, f := a, hf := sorry }))) ≫
      G₀.obj (P := Presheaf.IsSheaf J₀).map I.f.op)
    ((res data G₀ h₂ ≫
        G₀.obj (P := Presheaf.IsSheaf J₀).map
          (Quiver.Hom.op (GrothendieckTopology.Cover.Arrow.f { Y := Z₀, f := a, hf := sorry }))) ≫
      G₀.obj (P := Presheaf.IsSheaf J₀).map I.f.op)
Tactic: refine Presheaf.IsSheaf.hom_ext G₀.property
    ⟨_, (data X).mem₁₀ h₁.i₀ h₂.i₀ b₁ b₂ (by rw [w₁, w₂, assoc, assoc, h₁.fac, h₂.fac])⟩ _ _ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense (goal)
Goal:
C₀ : Type u₀
C : Type u
inst : Category.{v₀, u₀} C₀
inst_1 : Category.{v, u} C
F : Functor.{v₀, v, u₀, u} C₀ C
J₀ : GrothendieckTopology.{v₀, u₀} C₀
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_2 : Category.{v', u'} A
inst_3 : IsDenseSubsite J₀ J F
data : (X : C) → OneHypercoverDenseData.{w, v₀, v, u₀, u} F J₀ J X
inst_4 : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf.{v₀, v', u₀, u'} J₀ A
X : C
X₀ Y₀ : C₀
f : F.obj X₀ ⟶ X
g : Y₀ ⟶ X₀
h₁ h₂ : (data X).SieveStruct f g
Z₀ : C₀
a : Z₀ ⟶ Y₀
b₁ : Z₀ ⟶ (data X).X h₁.i₀
w₁ : F.map b₁ = F.map a ≫ h₁.q
b₂ : Z₀ ⟶ (data X).X h₂.i₀
w₂ : F.map b₂ = F.map a ≫ h₂.q
W₀ : C₀
c : W₀ ⟶ Z₀
hc :
  (↑(Subtype.mk (p := fun (S : Sieve.{v₀, u₀} Z₀) ↦ S ∈ (J₀ : (a : C₀) → Set (Sieve a)) Z₀) ((data X).sieve₁₀ b₁ b₂)
            ⋯) :
        Sieve Z₀).arrows
    c
⊢ Eq (α :=
    presheafObj data G₀ X ⟶
      G₀.obj (P := Presheaf.IsSheaf J₀).obj
        (op
          { Y := W₀, f := c, hf := hc :
              GrothendieckTopology.Cover.Arrow
                (Subtype.mk (p := fun (S : Sieve.{v₀, u₀} Z₀) ↦ S ∈ (J₀ : (a : C₀) → Set (Sieve a)) Z₀)
                  ((data X).sieve₁₀ b₁ b₂) ⋯) }.Y))
    ((res data G₀ h₁ ≫
        G₀.obj (P := Presheaf.IsSheaf J₀).map
          (Quiver.Hom.op (GrothendieckTopology.Cover.Arrow.f { Y := Z₀, f := a, hf := ⋯ }))) ≫
      G₀.obj (P := Presheaf.IsSheaf J₀).map
        { Y := W₀, f := c, hf := hc :
              GrothendieckTopology.Cover.Arrow
                (Subtype.mk (p := fun (S : Sieve.{v₀, u₀} Z₀) ↦ S ∈ (J₀ : (a : C₀) → Set (Sieve a)) Z₀)
                  ((data X).sieve₁₀ b₁ b₂) ⋯) }.f.op)
    ((res data G₀ h₂ ≫
        G₀.obj (P := Presheaf.IsSheaf J₀).map
          (Quiver.Hom.op (GrothendieckTopology.Cover.Arrow.f { Y := Z₀, f := a, hf := ⋯ }))) ≫
      G₀.obj (P := Presheaf.IsSheaf J₀).map
        { Y := W₀, f := c, hf := hc :
              GrothendieckTopology.Cover.Arrow
                (Subtype.mk (p := fun (S : Sieve.{v₀, u₀} Z₀) ↦ S ∈ (J₀ : (a : C₀) → Set (Sieve a)) Z₀)
                  ((data X).sieve₁₀ b₁ b₂) ⋯) }.f.op)
have dsimp : Eq (α := presheafObj data G₀ X ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op W₀))
  (((presheafObjπ data G₀ X h₁.i₀ ≫ IsDenseSubsite.mapPreimage J F G₀ h₁.q) ≫
      G₀.obj (P := Presheaf.IsSheaf J₀).map a.op) ≫
    G₀.obj (P := Presheaf.IsSheaf J₀).map c.op)
  (((presheafObjπ data G₀ X h₂.i₀ ≫ IsDenseSubsite.mapPreimage J F G₀ h₂.q) ≫
      G₀.obj (P := Presheaf.IsSheaf J₀).map a.op) ≫
    G₀.obj (P := Presheaf.IsSheaf J₀).map c.op)
Tactic: dsimp [res]