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)
i₁ i₂ : (data X).I₀
j : (data X).I₁ i₁ i₂
W₀ : C₀
a : W₀ ⟶ (data X).Y j
ha :
  (↑(Subtype.mk (p := fun (S : Sieve.{v₀, u₀} ((data X).Y j)) ↦
            Membership.mem (γ := Set (Sieve.{v₀, u₀} ((data X).Y j))) ((J₀ : (a : C₀) → Set (Sieve a)) ((data X).Y j))
              S)
            (Sieve.functorPullback F (Sieve.pullback (F.map ((data X).p₁ j) ≫ (data X).f i₁) (↑S : Sieve X))) ⋯) :
        Sieve ((data X).Y j)).arrows
    a
⊢ (liftAux hG₀ s i₁ ≫ G.map (F.map ((data X).p₁ j)).op) ≫
      (F.op ⋙ G).map
        { Y := W₀, f := a, hf := ha :
              GrothendieckTopology.Cover.Arrow
                (Subtype.mk (p := fun (S : Sieve.{v₀, u₀} ((data X).Y j)) ↦
                  Membership.mem (γ := Set (Sieve.{v₀, u₀} ((data X).Y j)))
                    ((J₀ : (a : C₀) → Set (Sieve a)) ((data X).Y j)) S)
                  (Sieve.functorPullback F (Sieve.pullback (F.map ((data X).p₁ j) ≫ (data X).f i₁) (↑S : Sieve X)))
                  ⋯) }.f.op =
    (liftAux hG₀ s i₂ ≫ G.map (F.map ((data X).p₂ j)).op) ≫ (F.op ⋙ G).map { Y := W₀, f := a, hf := ha }.f.op
have dsimp : (liftAux hG₀ s i₁ ≫ G.map (F.map ((data X).p₁ j)).op) ≫ G.map (F.map a).op =
  (liftAux hG₀ s i₂ ≫ G.map (F.map ((data X).p₂ j)).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)
i₁ i₂ : (data X).I₀
j : (data X).I₁ i₁ i₂
W₀ : C₀
a : W₀ ⟶ (data X).Y j
ha :
  (↑(Subtype.mk (p := fun (S : Sieve.{v₀, u₀} ((data X).Y j)) ↦
            Membership.mem (γ := Set (Sieve.{v₀, u₀} ((data X).Y j))) ((J₀ : (a : C₀) → Set (Sieve a)) ((data X).Y j))
              S)
            (Sieve.functorPullback F (Sieve.pullback (F.map ((data X).p₁ j) ≫ (data X).f i₁) (↑S : Sieve X))) ⋯) :
        Sieve ((data X).Y j)).arrows
    a
⊢ (liftAux hG₀ s i₁ ≫ G.map (F.map ((data X).p₁ j)).op) ≫ G.map (F.map a).op =
    (liftAux hG₀ s i₂ ≫ G.map (F.map ((data X).p₂ j)).op) ≫ G.map (F.map a).op
have simp : liftAux hG₀ s i₁ ≫ G.map (F.map (a ≫ (data X).p₁ j)).op = liftAux hG₀ s i₂ ≫ G.map (F.map (a ≫ (data X).p₂ j)).op
Tactic: simp only [assoc, ← Functor.map_comp, ← op_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense (hypothesis)
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)
i₁ i₂ : (data X).I₀
j : (data X).I₁ i₁ i₂
W₀ : C₀
a : W₀ ⟶ (data X).Y j
ha :
  (↑(Subtype.mk (p := fun (S : Sieve.{v₀, u₀} ((data X).Y j)) ↦
            Membership.mem (γ := Set (Sieve.{v₀, u₀} ((data X).Y j))) ((J₀ : (a : C₀) → Set (Sieve a)) ((data X).Y j))
              S)
            (Sieve.functorPullback F (Sieve.pullback (F.map ((data X).p₁ j) ≫ (data X).f i₁) (↑S : Sieve X))) ⋯) :
        Sieve ((data X).Y j)).arrows
    a
⊢ liftAux hG₀ s i₁ ≫ G.map (F.map (a ≫ (data X).p₁ j)).op = liftAux hG₀ s i₂ ≫ G.map (F.map (a ≫ (data X).p₂ j)).op
have ha₁ : (↑S : Sieve X).arrows (F.map (a ≫ (data X).p₁ j) ≫ (data X).f i₁)
Tactic: have ha₁ : S (F.map (a ≫ (data X).p₁ j) ≫ (data X).f i₁) := by simpa using ha
-- 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)
i₁ i₂ : (data X).I₀
j : (data X).I₁ i₁ i₂
W₀ : C₀
a : W₀ ⟶ (data X).Y j
ha :
  (↑(Subtype.mk (p := fun (S : Sieve.{v₀, u₀} ((data X).Y j)) ↦
            Membership.mem (γ := Set (Sieve.{v₀, u₀} ((data X).Y j))) ((J₀ : (a : C₀) → Set (Sieve a)) ((data X).Y j))
              S)
            (Sieve.functorPullback F (Sieve.pullback (F.map ((data X).p₁ j) ≫ (data X).f i₁) (↑S : Sieve X))) ⋯) :
        Sieve ((data X).Y j)).arrows
    a
ha₁ : (↑S : Sieve X).arrows (F.map (a ≫ (data X).p₁ j) ≫ (data X).f i₁)
⊢ (↑S : Sieve X).arrows (F.map (a ≫ (data X).p₂ j) ≫ (data X).f i₂)
have rwa : (↑S : Sieve X).arrows (F.map a ≫ F.map ((data X).p₂ j) ≫ (data X).f i₂)
Tactic: rwa [Functor.map_comp_assoc, ← (data X).w j]
-- 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)
i₁ i₂ : (data X).I₀
j : (data X).I₁ i₁ i₂
W₀ : C₀
a : W₀ ⟶ (data X).Y j
ha :
  (↑(Subtype.mk (p := fun (S : Sieve.{v₀, u₀} ((data X).Y j)) ↦
            Membership.mem (γ := Set (Sieve.{v₀, u₀} ((data X).Y j))) ((J₀ : (a : C₀) → Set (Sieve a)) ((data X).Y j))
              S)
            (Sieve.functorPullback F (Sieve.pullback (F.map ((data X).p₁ j) ≫ (data X).f i₁) (↑S : Sieve X))) ⋯) :
        Sieve ((data X).Y j)).arrows
    a
ha₁ : (↑S : Sieve X).arrows (F.map (a ≫ (data X).p₁ j) ≫ (data X).f i₁)
rwa : (↑S : Sieve X).arrows (F.map a ≫ F.map ((data X).p₂ j) ≫ (data X).f i₂)
⊢ (↑S : Sieve X).arrows (F.map (a ≫ (data X).p₂ j) ≫ (data X).f i₂)
have rwa₁ : (↑S : Sieve X).arrows (F.map a ≫ F.map ((data X).p₁ j) ≫ (data X).f i₁)
Tactic: rwa [Functor.map_comp_assoc, ← (data X).w j]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense (hypothesis)
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)
i₁ i₂ : (data X).I₀
j : (data X).I₁ i₁ i₂
W₀ : C₀
a : W₀ ⟶ (data X).Y j
ha :
  (↑(Subtype.mk (p := fun (S : Sieve.{v₀, u₀} ((data X).Y j)) ↦
            Membership.mem (γ := Set (Sieve.{v₀, u₀} ((data X).Y j))) ((J₀ : (a : C₀) → Set (Sieve a)) ((data X).Y j))
              S)
            (Sieve.functorPullback F (Sieve.pullback (F.map ((data X).p₁ j) ≫ (data X).f i₁) (↑S : Sieve X))) ⋯) :
        Sieve ((data X).Y j)).arrows
    a
ha₁ : (↑S : Sieve X).arrows (F.map (a ≫ (data X).p₁ j) ≫ (data X).f i₁)
⊢ liftAux hG₀ s i₁ ≫ G.map (F.map (a ≫ (data X).p₁ j)).op = liftAux hG₀ s i₂ ≫ G.map (F.map (a ≫ (data X).p₂ j)).op
have ha₂ : (↑S : Sieve X).arrows (F.map (a ≫ (data X).p₂ j) ≫ (data X).f i₂)
Tactic: have ha₂ : S (F.map (a ≫ (data X).p₂ j) ≫ (data X).f i₂) := by
      rwa [Functor.map_comp_assoc, ← (data X).w j]
-- 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)
i₁ i₂ : (data X).I₀
j : (data X).I₁ i₁ i₂
W₀ : C₀
a : W₀ ⟶ (data X).Y j
ha :
  (↑(Subtype.mk (p := fun (S : Sieve.{v₀, u₀} ((data X).Y j)) ↦
            Membership.mem (γ := Set (Sieve.{v₀, u₀} ((data X).Y j))) ((J₀ : (a : C₀) → Set (Sieve a)) ((data X).Y j))
              S)
            (Sieve.functorPullback F (Sieve.pullback (F.map ((data X).p₁ j) ≫ (data X).f i₁) (↑S : Sieve X))) ⋯) :
        Sieve ((data X).Y j)).arrows
    a
ha₁ : (↑S : Sieve X).arrows (F.map (a ≫ (data X).p₁ j) ≫ (data X).f i₁)
ha₂ : (↑S : Sieve X).arrows (F.map (a ≫ (data X).p₂ j) ≫ (data X).f i₂)
⊢ liftAux hG₀ s i₁ ≫ G.map (F.map (a ≫ (data X).p₁ j)).op = liftAux hG₀ s i₂ ≫ G.map (F.map (a ≫ (data X).p₂ j)).op
have rw : Eq (α := s.pt ⟶ G.obj (op (F.obj W₀)))
  (s.ι { Y := F.obj W₀, f := F.map (a ≫ (data X).p₁ j) ≫ (data X).f i₁, hf := ha₁ } :
    s.pt ⟶ (S.index G).left { Y := F.obj W₀, f := F.map (a ≫ (data X).p₁ j) ≫ (data X).f i₁, hf := ha₁ })
  (s.ι { Y := F.obj W₀, f := F.map (a ≫ (data X).p₂ j) ≫ (data X).f i₂, hf := ha₂ })
Tactic: rw [liftAux_fac _ _ _ ha₁, liftAux_fac _ _ _ ha₂]
-- 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)
i₁ i₂ : (data X).I₀
j : (data X).I₁ i₁ i₂
W₀ : C₀
a : W₀ ⟶ (data X).Y j
ha :
  (↑(Subtype.mk (p := fun (S : Sieve.{v₀, u₀} ((data X).Y j)) ↦
            Membership.mem (γ := Set (Sieve.{v₀, u₀} ((data X).Y j))) ((J₀ : (a : C₀) → Set (Sieve a)) ((data X).Y j))
              S)
            (Sieve.functorPullback F (Sieve.pullback (F.map ((data X).p₁ j) ≫ (data X).f i₁) (↑S : Sieve X))) ⋯) :
        Sieve ((data X).Y j)).arrows
    a
ha₁ : (↑S : Sieve X).arrows (F.map (a ≫ (data X).p₁ j) ≫ (data X).f i₁)
ha₂ : (↑S : Sieve X).arrows (F.map (a ≫ (data X).p₂ j) ≫ (data X).f i₂)
⊢ Eq (α := s.pt ⟶ G.obj (op (F.obj W₀)))
    (s.ι { Y := F.obj W₀, f := F.map (a ≫ (data X).p₁ j) ≫ (data X).f i₁, hf := ha₁ } :
      s.pt ⟶ (S.index G).left { Y := F.obj W₀, f := F.map (a ≫ (data X).p₁ j) ≫ (data X).f i₁, hf := ha₁ })
    (s.ι { Y := F.obj W₀, f := F.map (a ≫ (data X).p₂ j) ≫ (data X).f i₂, hf := ha₂ })
have h : F.map (a ≫ (data X).p₁ j) ≫ (data X).f i₁ = F.map (a ≫ (data X).p₂ j) ≫ (data X).f i₂
Tactic: congr 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)
i₁ i₂ : (data X).I₀
j : (data X).I₁ i₁ i₂
W₀ : C₀
a : W₀ ⟶ (data X).Y j
ha :
  (↑(Subtype.mk (p := fun (S : Sieve.{v₀, u₀} ((data X).Y j)) ↦
            Membership.mem (γ := Set (Sieve.{v₀, u₀} ((data X).Y j))) ((J₀ : (a : C₀) → Set (Sieve a)) ((data X).Y j))
              S)
            (Sieve.functorPullback F (Sieve.pullback (F.map ((data X).p₁ j) ≫ (data X).f i₁) (↑S : Sieve X))) ⋯) :
        Sieve ((data X).Y j)).arrows
    a
ha₁ : (↑S : Sieve X).arrows (F.map (a ≫ (data X).p₁ j) ≫ (data X).f i₁)
ha₂ : (↑S : Sieve X).arrows (F.map (a ≫ (data X).p₂ j) ≫ (data X).f i₂)
⊢ F.map (a ≫ (data X).p₁ j) ≫ (data X).f i₁ = F.map (a ≫ (data X).p₂ j) ≫ (data X).f i₂
have h : F.map a ≫ F.map ((data X).p₁ j) ≫ (data X).f i₁ = F.map (a ≫ (data X).p₂ j) ≫ (data X).f i₂
Tactic: rw [map_comp_assoc, map_comp_assoc, (data X).w j]
-- 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)
i₁ i₂ : (data X).I₀
j : (data X).I₁ i₁ i₂
W₀ : C₀
a : W₀ ⟶ (data X).Y j
ha :
  (↑(Subtype.mk (p := fun (S : Sieve.{v₀, u₀} ((data X).Y j)) ↦
            Membership.mem (γ := Set (Sieve.{v₀, u₀} ((data X).Y j))) ((J₀ : (a : C₀) → Set (Sieve a)) ((data X).Y j))
              S)
            (Sieve.functorPullback F (Sieve.pullback (F.map ((data X).p₁ j) ≫ (data X).f i₁) (↑S : Sieve X))) ⋯) :
        Sieve ((data X).Y j)).arrows
    a
ha₁ : (↑S : Sieve X).arrows (F.map (a ≫ (data X).p₁ j) ≫ (data X).f i₁)
ha₂ : (↑S : Sieve X).arrows (F.map (a ≫ (data X).p₂ j) ≫ (data X).f i₂)
h : F.map a ≫ F.map ((data X).p₁ j) ≫ (data X).f i₁ = F.map (a ≫ (data X).p₂ j) ≫ (data X).f i₂
⊢ F.map (a ≫ (data X).p₁ j) ≫ (data X).f i₁ = F.map (a ≫ (data X).p₂ j) ≫ (data X).f i₂
have h₁ : F.map a ≫ F.map ((data X).p₁ j) ≫ (data X).f i₁ = F.map a ≫ F.map ((data X).p₂ j) ≫ (data X).f i₂
Tactic: rw [map_comp_assoc, map_comp_assoc, (data X).w j]
-- 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)
i₁ i₂ : (data X).I₀
j : (data X).I₁ i₁ i₂
W₀ : C₀
a : W₀ ⟶ (data X).Y j
ha :
  (↑(Subtype.mk (p := fun (S : Sieve.{v₀, u₀} ((data X).Y j)) ↦
            Membership.mem (γ := Set (Sieve.{v₀, u₀} ((data X).Y j))) ((J₀ : (a : C₀) → Set (Sieve a)) ((data X).Y j))
              S)
            (Sieve.functorPullback F (Sieve.pullback (F.map ((data X).p₁ j) ≫ (data X).f i₁) (↑S : Sieve X))) ⋯) :
        Sieve ((data X).Y j)).arrows
    a
ha₁ : (↑S : Sieve X).arrows (F.map (a ≫ (data X).p₁ j) ≫ (data X).f i₁)
ha₂ : (↑S : Sieve X).arrows (F.map (a ≫ (data X).p₂ j) ≫ (data X).f i₂)
h : F.map a ≫ F.map ((data X).p₁ j) ≫ (data X).f i₁ = F.map (a ≫ (data X).p₂ j) ≫ (data X).f i₂
h₁ : F.map a ≫ F.map ((data X).p₁ j) ≫ (data X).f i₁ = F.map a ≫ F.map ((data X).p₂ j) ≫ (data X).f i₂
⊢ F.map (a ≫ (data X).p₁ j) ≫ (data X).f i₁ = F.map (a ≫ (data X).p₂ j) ≫ (data X).f i₂
have h₂ : F.map a ≫ F.map ((data X).p₂ j) ≫ (data X).f i₂ = F.map a ≫ F.map ((data X).p₂ j) ≫ (data X).f i₂
Tactic: rw [map_comp_assoc, map_comp_assoc, (data X).w j]
-- 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
⊢ (↑S : Sieve X).arrows (F.map e ≫ (data X).f j)
have rw : (↑S : Sieve X).arrows (F.map d ≫ F.map b ≫ PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data a.Y)) i ≫ a.f)
Tactic: rw [fac₂, assoc, fac₁]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense (hypothesis)
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
⊢ (((lift hG₀ hG s ≫ G.map a.f.op) ≫
          G.map (PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data a.Y)) i).op) ≫
        G.map (F.map b).op) ≫
      G.map (F.map d).op =
    ((s.ι a ≫ G.map (PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data a.Y)) i).op) ≫ G.map (F.map b).op) ≫
      G.map (F.map d).op
have he : (↑S : Sieve X).arrows (F.map e ≫ (data X).f j)
Tactic: have he : S (F.map e ≫ (data X).f j) := by
          rw [fac₂, assoc, fac₁]
          simpa only [assoc] using S.1.downward_closed a.hf (F.map d ≫ F.map b ≫ (data a.Y).f i)
-- 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)
⊢ (((lift hG₀ hG s ≫ G.map a.f.op) ≫
          G.map (PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data a.Y)) i).op) ≫
        G.map (F.map b).op) ≫
      G.map (F.map d).op =
    ((s.ι a ≫ G.map (PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data a.Y)) i).op) ≫ G.map (F.map b).op) ≫
      G.map (F.map d).op
have simp : lift hG₀ hG s ≫ G.map (F.map d ≫ c ≫ (data X).f j).op =
  s.ι a ≫ G.map (F.map d ≫ F.map b ≫ PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data a.Y)) i).op
Tactic: simp only [assoc, ← Functor.map_comp, ← op_comp, ← 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.{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)
| lift hG₀ hG s ≫ G.map (F.map d ≫ c ≫ (data X).f j).op
have simp : liftAux hG₀ s j ≫ G.map c.op ≫ G.map (F.map d).op
Tactic: simp only [op_comp, Functor.map_comp, assoc, lift_map_assoc]
-- 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)
⊢ lift hG₀ hG s ≫ G.map (F.map d ≫ c ≫ (data X).f j).op =
    s.ι a ≫ G.map (F.map d ≫ F.map b ≫ PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data a.Y)) i).op
have conv_lhs : 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
Tactic: conv_lhs => simp only [op_comp, Functor.map_comp, assoc, lift_map_assoc]