awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.DescentData (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
J : GrothendieckTopology.{v, u} C
inst_1 : F.IsPrestack J
hf : Sieve.ofArrows X f ∈ (J : (a : C) → Set (Sieve a)) S
M N : (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')
rwa :
  Membership.mem (α := Sieve.{v, u} (Over.left.{v, u} (Over.mk (𝟙 S)))) (γ :=
    Set (Sieve.{v, u} (Over.left.{v, u} (Over.mk (𝟙 S)))))
    ((J : (a : C) → Set (Sieve a)) (Over.left.{v, u} (Over.mk (𝟙 S))))
    ((Sieve.overEquiv (Over.mk (𝟙 S)) : (a : Sieve (Over.mk (𝟙 S))) → Sieve (Over.mk (𝟙 S)).left)
        (Sieve.generate
          (Sieve.arrows
            ((Equiv.symm (Sieve.overEquiv (Over.mk (𝟙 S))) : (a : Sieve (Over.mk (𝟙 S)).left) → Sieve (Over.mk (𝟙 S)))
              (Sieve.generate (Presieve.ofArrows X f))))) :
      Sieve.{v, u} (Over.left.{v, u} (Over.mk (𝟙 S))))
⊢ Membership.mem (α := Sieve (C := Over.{v, u} S) (Over.mk (𝟙 S))) (γ :=
    Set (Sieve (C := Over.{v, u} S) (Over.mk (𝟙 S)))) ((J.over S : (a : Over S) → Set (Sieve a)) (Over.mk (𝟙 S)))
    (Sieve.generate
        (Sieve.arrows
          ((Equiv.symm (Sieve.overEquiv (Over.mk (𝟙 S))) : (a : Sieve (Over.mk (𝟙 S)).left) → Sieve (Over.mk (𝟙 S)))
            (Sieve.generate (Presieve.ofArrows X f)))) :
      Sieve (C := Over.{v, u} S) (Over.mk (𝟙 S)))
have rwa₁ : Membership.mem (α := Sieve.{v, u} (Over.left.{v, u} (Over.mk (𝟙 S)))) (γ :=
  Set (Sieve.{v, u} (Over.left.{v, u} (Over.mk (𝟙 S)))))
  ((J : (a : C) → Set (Sieve a)) (Over.left.{v, u} (Over.mk (𝟙 S))))
  ((Sieve.overEquiv (Over.mk (𝟙 S)) : (a : Sieve (Over.mk (𝟙 S))) → Sieve (Over.mk (𝟙 S)).left)
      ((Equiv.symm (Sieve.overEquiv (Over.mk (𝟙 S))) : (a : Sieve (Over.mk (𝟙 S)).left) → Sieve (Over.mk (𝟙 S)))
        (Sieve.generate (Presieve.ofArrows X f))) :
    Sieve.{v, u} (Over.left.{v, u} (Over.mk (𝟙 S))))
Tactic: rwa [GrothendieckTopology.mem_over_iff, Sieve.generate_sieve, Equiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.DescentData (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
J : GrothendieckTopology.{v, u} C
inst_1 : F.IsPrestack J
hf : Sieve.ofArrows X f ∈ (J : (a : C) → Set (Sieve a)) S
M N : (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')
rwa :
  Membership.mem (α := Sieve.{v, u} (Over.left.{v, u} (Over.mk (𝟙 S)))) (γ :=
    Set (Sieve.{v, u} (Over.left.{v, u} (Over.mk (𝟙 S)))))
    ((J : (a : C) → Set (Sieve a)) (Over.left.{v, u} (Over.mk (𝟙 S))))
    ((Sieve.overEquiv (Over.mk (𝟙 S)) : (a : Sieve (Over.mk (𝟙 S))) → Sieve (Over.mk (𝟙 S)).left)
        (Sieve.generate
          (Sieve.arrows
            ((Equiv.symm (Sieve.overEquiv (Over.mk (𝟙 S))) : (a : Sieve (Over.mk (𝟙 S)).left) → Sieve (Over.mk (𝟙 S)))
              (Sieve.generate (Presieve.ofArrows X f))))) :
      Sieve.{v, u} (Over.left.{v, u} (Over.mk (𝟙 S))))
rwa₁ :
  Membership.mem (α := Sieve.{v, u} (Over.left.{v, u} (Over.mk (𝟙 S)))) (γ :=
    Set (Sieve.{v, u} (Over.left.{v, u} (Over.mk (𝟙 S)))))
    ((J : (a : C) → Set (Sieve a)) (Over.left.{v, u} (Over.mk (𝟙 S))))
    ((Sieve.overEquiv (Over.mk (𝟙 S)) : (a : Sieve (Over.mk (𝟙 S))) → Sieve (Over.mk (𝟙 S)).left)
        ((Equiv.symm (Sieve.overEquiv (Over.mk (𝟙 S))) : (a : Sieve (Over.mk (𝟙 S)).left) → Sieve (Over.mk (𝟙 S)))
          (Sieve.generate (Presieve.ofArrows X f))) :
      Sieve.{v, u} (Over.left.{v, u} (Over.mk (𝟙 S))))
⊢ Membership.mem (α := Sieve (C := Over.{v, u} S) (Over.mk (𝟙 S))) (γ :=
    Set (Sieve (C := Over.{v, u} S) (Over.mk (𝟙 S)))) ((J.over S : (a : Over S) → Set (Sieve a)) (Over.mk (𝟙 S)))
    (Sieve.generate
        (Sieve.arrows
          ((Equiv.symm (Sieve.overEquiv (Over.mk (𝟙 S))) : (a : Sieve (Over.mk (𝟙 S)).left) → Sieve (Over.mk (𝟙 S)))
            (Sieve.generate (Presieve.ofArrows X f)))) :
      Sieve (C := Over.{v, u} S) (Over.mk (𝟙 S)))
have rwa₂ : Membership.mem (γ := Set (Sieve.{v, u} (Over.left.{v, u} (Over.mk (𝟙 S)))))
  ((J : (a : C) → Set (Sieve a)) (Over.left.{v, u} (Over.mk (𝟙 S)))) (Sieve.generate (Presieve.ofArrows X f))
Tactic: rwa [GrothendieckTopology.mem_over_iff, Sieve.generate_sieve, Equiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.DescentData (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
J : GrothendieckTopology.{v, u} C
inst_1 : F.IsPrestack J
S : C
R : Presieve.{v, u} S
hR : Sieve.generate R ∈ (J : (a : C) → Set (Sieve a)) S
⊢ F.IsPrestackFor R
have rw : Nonempty
  (Functor.FullyFaithful (C := (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')) (D :=
    F.DescentData (S := S) (X := fun (f : R.category) ↦ f.obj (P := fun (f : Over.{v, u} S) ↦ R f.hom).left)
      fun (f : R.category) ↦ f.obj (P := fun (f : Over.{v, u} S) ↦ R f.hom).hom)
    (F.toDescentData fun (f : R.category) ↦ f.obj (P := fun (f : Over.{v, u} S) ↦ R f.hom).hom))
Tactic: rw [isPrestackFor_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.DescentData (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
J : GrothendieckTopology.{v, u} C
hF : ∀ (S : C), ∀ R ∈ (J : (a : C) → Set (Sieve a)) S, F.IsPrestackFor R.arrows
S : C
M N : (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')
⊢ Presheaf.IsSheaf (J.over S) (F.presheafHom M N)
have rw : Presieve.IsSheaf (J.over S) (F.presheafHom M N)
Tactic: rw [isSheaf_iff_isSheaf_of_type]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.DescentData (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
J : GrothendieckTopology.{v, u} C
hF : ∀ (S : C), ∀ R ∈ (J : (a : C) → Set (Sieve a)) S, F.IsPrestackFor R.arrows
S_1 : C
M N : (↑(F.obj { as := op S_1 : LocallyDiscrete Cᵒᵖ }) : Type u')
U : Over.{v, u} S_1
S : Sieve U
hS : S ∈ (J.over S_1 : (a : Over S_1) → Set (Sieve a)) U
⊢ Presieve.IsSheafFor (F.presheafHom M N) S.arrows
have obtain : ∀ (U : C) (u : U ⟶ S_1) (S : Sieve (Over.mk u))
  (hS : Membership.mem (γ := Set (Sieve (Over.mk u))) ((J.over S_1 : (a : Over S_1) → Set (Sieve a)) (Over.mk u)) S),
  Presieve.IsSheafFor (F.presheafHom M N) S.arrows
Tactic: obtain ⟨U, u, rfl⟩ := Over.mk_surjective U
Cleared hypotheses: U, S, hS
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Adj Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
D₁ D₂ : F.DescentDataAsCoalgebra f
e : (i : ι) → D₁.obj i ≅ D₂.obj i
comm :
  ∀ (i₁ i₂ : ι),
    D₁.hom i₁ i₂ ≫
        Functor.map (Cat.Hom.toFunctor (Adj.Hom.l (F.map (f i₁).op.toLoc)))
          (Functor.map (Cat.Hom.toFunctor (Adj.Hom.r (F.map (f i₂).op.toLoc))) (e i₂).hom) =
      (e i₁).hom ≫ D₂.hom i₁ i₂
i₁ i₂ : ι
⊢ D₂.hom i₁ i₂ ≫
      Functor.map (Cat.Hom.toFunctor (Adj.Hom.l (F.map (f i₁).op.toLoc)))
        (Functor.map (Cat.Hom.toFunctor (Adj.Hom.r (F.map (f i₂).op.toLoc))) (e i₂).inv) =
    (e i₁).inv ≫ D₁.hom i₁ i₂
have rw : D₁.hom i₁ i₂ ≫
    Functor.map (Cat.Hom.toFunctor (Adj.Hom.l (F.map (f i₁).op.toLoc)))
      (Functor.map (Cat.Hom.toFunctor (Adj.Hom.r (F.map (f i₂).op.toLoc))) ((e i₂).hom ≫ (e i₂).inv)) =
  (e i₁).hom ≫ (e i₁).inv ≫ D₁.hom i₁ i₂
Tactic: rw [← cancel_epi (e i₁).hom, ← reassoc_of% (comm i₁ i₂), ← Functor.map_comp, ← Functor.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Adj Cat
ι : Type u_1
inst_1 : Unique ι
X S : C
f : X ⟶ S
D : F.DescentDataAsCoalgebra (S := S) (X := fun (x : ι) ↦ X) fun (x : ι) ↦ f
i₁ i₂ : ι
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have obtain : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: obtain rfl := Subsingleton.elim i₁ default
Cleared hypotheses: i₁
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Adj Cat
ι : Type u_1
inst_1 : Unique ι
X S : C
f : X ⟶ S
D : F.DescentDataAsCoalgebra (S := S) (X := fun (x : ι) ↦ X) fun (x : ι) ↦ f
i₂ : ι
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have obtain : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: obtain rfl := Subsingleton.elim i₂ default
Cleared hypotheses: i₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Adj Cat
ι : Type u_1
inst_1 : Unique ι
X S : C
f : X ⟶ S
D₁ D₂ : F.DescentDataAsCoalgebra (S := S) (X := fun (x : ι) ↦ X) fun (x : ι) ↦ f
α : D₁ ⟶ D₂
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: ext i
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Adj Cat
ι : Type u_1
inst_1 : Unique ι
X S : C
f : X ⟶ S
D₁ D₂ : F.DescentDataAsCoalgebra (S := S) (X := fun (x : ι) ↦ X) fun (x : ι) ↦ f
α : D₁ ⟶ D₂
i : ι
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: obtain rfl := Subsingleton.elim i default
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Adj Cat
ι : Type u_1
inst_1 : Unique ι
X S : C
f : X ⟶ S
⊢ Functor.IsEquivalence (C := (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }).obj : Type u')) (D :=
      F.DescentDataAsCoalgebra (S := S) (X := fun (x : ι) ↦ X) fun (x : ι) ↦ f)
      (F.toDescentDataAsCoalgebra fun (x : ι) ↦ f) ↔
    Functor.IsEquivalence (C := (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }).obj : Type u')) (D :=
      Comonad.Coalgebra (C := (↑(F.obj { as := op X : LocallyDiscrete Cᵒᵖ }).obj : Type u'))
        (Adjunction.toComonad (C := (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }).obj : Type u')) (L :=
          Cat.Hom.toFunctor (Adj.Hom.l (F.map f.op.toLoc))) (Adjunction.ofCat (Adj.Hom.adj (F.map f.op.toLoc)))))
      (Comonad.comparison (Adjunction.ofCat (Adj.Hom.adj (F.map f.op.toLoc))))
have rw : Functor.IsEquivalence (C := (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }).obj : Type u')) (D :=
    F.DescentDataAsCoalgebra (S := S) (X := fun (x : ι) ↦ X) fun (x : ι) ↦ f)
    (F.toDescentDataAsCoalgebra fun (x : ι) ↦ f) ↔
  ((F.toDescentDataAsCoalgebra fun (x : ι) ↦ f) ⋙
      (DescentDataAsCoalgebra.coalgebraEquivalence F ι f).functor).IsEquivalence
Tactic: rw [← Functor.isEquivalence_iff_of_iso
    (F.toDescentDataAsCoalgebraCompCoalgebraEquivalenceFunctorIso ι f)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
sq : (i j : ι) → ChosenPullback (f i) (f j)
obj obj' : (i : ι) → (↑(F.obj { as := op (X i) : LocallyDiscrete Cᵒᵖ }) : Type u')
hom :
  (i j : ι) →
    Quiver.Hom (V := (↑(F.obj { as := op (sq i j).pullback : LocallyDiscrete Cᵒᵖ }) : Type u'))
      (Functor.obj (Cat.Hom.toFunctor (F.map (sq i j).p₁.op.toLoc)) (obj i))
      (Functor.obj (Cat.Hom.toFunctor (F.map (sq i j).p₂.op.toLoc)) (obj' j))
Y : C
q : Y ⟶ S
i₁ i₂ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
p : Y ⟶ (sq i₁ i₂).pullback
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
hp₁ : p ≫ (sq i₁ i₂).p₁ = f₁
hp₂ : p ≫ (sq i₁ i₂).p₂ = f₂
⊢ f₁ ≫ f i₁ = f₂ ≫ f i₂
have rw : q = f₂ ≫ f i₂
Tactic: rw [hf₁, hf₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
sq : (i j : ι) → ChosenPullback (f i) (f j)
obj obj' : (i : ι) → (↑(F.obj { as := op (X i) : LocallyDiscrete Cᵒᵖ }) : Type u')
hom :
  (i j : ι) →
    Quiver.Hom (V := (↑(F.obj { as := op (sq i j).pullback : LocallyDiscrete Cᵒᵖ }) : Type u'))
      (Functor.obj (Cat.Hom.toFunctor (F.map (sq i j).p₁.op.toLoc)) (obj i))
      (Functor.obj (Cat.Hom.toFunctor (F.map (sq i j).p₂.op.toLoc)) (obj' j))
Y : C
q : Y ⟶ S
i₁ i₂ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
p : Y ⟶ (sq i₁ i₂).pullback
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
hp₁ : p ≫ (sq i₁ i₂).p₁ = f₁
hp₂ : p ≫ (sq i₁ i₂).p₂ = f₂
rw : q = f₂ ≫ f i₂
⊢ f₁ ≫ f i₁ = f₂ ≫ f i₂
have rw₁ : q = q
Tactic: rw [hf₁, hf₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
sq : (i j : ι) → ChosenPullback (f i) (f j)
obj obj' : (i : ι) → (↑(F.obj { as := op (X i) : LocallyDiscrete Cᵒᵖ }) : Type u')
hom :
  (i j : ι) →
    Quiver.Hom (V := (↑(F.obj { as := op (sq i j).pullback : LocallyDiscrete Cᵒᵖ }) : Type u'))
      (Functor.obj (Cat.Hom.toFunctor (F.map (sq i j).p₁.op.toLoc)) (obj i))
      (Functor.obj (Cat.Hom.toFunctor (F.map (sq i j).p₂.op.toLoc)) (obj' j))
Y : C
q : Y ⟶ S
i₁ i₂ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
p : Y ⟶ (sq i₁ i₂).pullback
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
hp₁ : p ≫ (sq i₁ i₂).p₁ = f₁
hp₂ : p ≫ (sq i₁ i₂).p₂ = f₂
⊢ p = ⋯.lift f₁ f₂ ⋯
have h₀ : p ≫ (sq i₁ i₂).p₁ = sorry.lift f₁ f₂ sorry ≫ (sq i₁ i₂).p₁
Tactic: apply (sq i₁ i₂).isPullback.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
sq : (i j : ι) → ChosenPullback (f i) (f j)
obj obj' : (i : ι) → (↑(F.obj { as := op (X i) : LocallyDiscrete Cᵒᵖ }) : Type u')
hom :
  (i j : ι) →
    Quiver.Hom (V := (↑(F.obj { as := op (sq i j).pullback : LocallyDiscrete Cᵒᵖ }) : Type u'))
      (Functor.obj (Cat.Hom.toFunctor (F.map (sq i j).p₁.op.toLoc)) (obj i))
      (Functor.obj (Cat.Hom.toFunctor (F.map (sq i j).p₂.op.toLoc)) (obj' j))
Y : C
q : Y ⟶ S
i₁ i₂ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
p : Y ⟶ (sq i₁ i₂).pullback
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
hp₁ : p ≫ (sq i₁ i₂).p₁ = f₁
hp₂ : p ≫ (sq i₁ i₂).p₂ = f₂
h₀ : p ≫ (sq i₁ i₂).p₁ = ⋯.lift f₁ f₂ ⋯ ≫ (sq i₁ i₂).p₁
⊢ p = ⋯.lift f₁ f₂ ⋯
have h₁ : p ≫ (sq i₁ i₂).p₂ = sorry.lift f₁ f₂ sorry ≫ (sq i₁ i₂).p₂
Tactic: apply (sq i₁ i₂).isPullback.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
sq : (i j : ι) → ChosenPullback (f i) (f j)
obj obj' : (i : ι) → (↑(F.obj { as := op (X i) : LocallyDiscrete Cᵒᵖ }) : Type u')
hom :
  (i j : ι) →
    Quiver.Hom (V := (↑(F.obj { as := op (sq i j).pullback : LocallyDiscrete Cᵒᵖ }) : Type u'))
      (Functor.obj (Cat.Hom.toFunctor (F.map (sq i j).p₁.op.toLoc)) (obj i))
      (Functor.obj (Cat.Hom.toFunctor (F.map (sq i j).p₂.op.toLoc)) (obj' j))
Y : C
q : Y ⟶ S
i₁ i₂ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
p : Y ⟶ (sq i₁ i₂).pullback
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
hp₁ : p ≫ (sq i₁ i₂).p₁ = f₁
hp₂ : p ≫ (sq i₁ i₂).p₂ = f₂
⊢ pullHom' hom q f₁ f₂ hf₁ hf₂ = pullHom (hom i₁ i₂) p f₁ f₂ ⋯ ⋯
have obtain : ∀ (hp₁ : sorry.lift f₁ f₂ sorry ≫ (sq i₁ i₂).p₁ = f₁) (hp₂ : sorry.lift f₁ f₂ sorry ≫ (sq i₁ i₂).p₂ = f₂),
  pullHom' hom q f₁ f₂ hf₁ hf₂ = pullHom (hom i₁ i₂) (sorry.lift f₁ f₂ sorry) f₁ f₂ sorry sorry
Tactic: obtain rfl : p = (sq i₁ i₂).isPullback.lift f₁ f₂ (by rw [hf₁, hf₂]) := by
    apply (sq i₁ i₂).isPullback.hom_ext <;> cat_disch
Cleared hypotheses: p, hp₁, hp₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
sq : (i j : ι) → ChosenPullback (f i) (f j)
obj obj' : (i : ι) → (↑(F.obj { as := op (X i) : LocallyDiscrete Cᵒᵖ }) : Type u')
hom :
  (i j : ι) →
    Quiver.Hom (V := (↑(F.obj { as := op (sq i j).pullback : LocallyDiscrete Cᵒᵖ }) : Type u'))
      (Functor.obj (Cat.Hom.toFunctor (F.map (sq i j).p₁.op.toLoc)) (obj i))
      (Functor.obj (Cat.Hom.toFunctor (F.map (sq i j).p₂.op.toLoc)) (obj' j))
Y Y' : C
g : Y' ⟶ Y
q : Y ⟶ S
q' : Y' ⟶ S
i₁ i₂ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
gf₁ : Y' ⟶ X i₁
gf₂ : Y' ⟶ X i₂
hq : g ≫ q = q'
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
hgf₁ : g ≫ f₁ = gf₁
hgf₂ : g ≫ f₂ = gf₂
p : Y ⟶ (sq i₁ i₂).pullback := ⋯.lift f₁ f₂ ⋯
⊢ pullHom (pullHom' hom q f₁ f₂ hf₁ hf₂) g gf₁ gf₂ ⋯ ⋯ = pullHom' hom q' gf₁ gf₂ ⋯ ⋯
have rw : pullHom (pullHom (hom i₁ i₂) p f₁ f₂ sorry sorry) g gf₁ gf₂ sorry sorry = pullHom (hom i₁ i₂) (g ≫ p) gf₁ gf₂ sorry sorry
Tactic: rw [pullHom'_eq_pullHom _ _ _ _ p, pullHom'_eq_pullHom _ _ _ _ (g ≫ p)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
sq : (i j : ι) → ChosenPullback (f i) (f j)
obj obj' : (i : ι) → (↑(F.obj { as := op (X i) : LocallyDiscrete Cᵒᵖ }) : Type u')
hom :
  (i j : ι) →
    Quiver.Hom (V := (↑(F.obj { as := op (sq i j).pullback : LocallyDiscrete Cᵒᵖ }) : Type u'))
      (Functor.obj (Cat.Hom.toFunctor (F.map (sq i j).p₁.op.toLoc)) (obj i))
      (Functor.obj (Cat.Hom.toFunctor (F.map (sq i j).p₂.op.toLoc)) (obj' j))
Y Y' : C
g : Y' ⟶ Y
q : Y ⟶ S
q' : Y' ⟶ S
i₁ i₂ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
gf₁ : Y' ⟶ X i₁
gf₂ : Y' ⟶ X i₂
hq : g ≫ q = q'
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
hgf₁ : g ≫ f₁ = gf₁
hgf₂ : g ≫ f₂ = gf₂
p : Y ⟶ (sq i₁ i₂).pullback := ⋯.lift f₁ f₂ ⋯
⊢ pullHom (pullHom (hom i₁ i₂) p f₁ f₂ ⋯ ⋯) g gf₁ gf₂ ⋯ ⋯ = pullHom (hom i₁ i₂) (g ≫ p) gf₁ gf₂ ⋯ ⋯
have dsimp : (F.mapComp' f₁.op.toLoc g.op.toLoc gf₁.op.toLoc sorry).hom.toNatTrans.app (obj i₁) ≫
    Functor.map (Cat.Hom.toFunctor (F.map g.op.toLoc))
        ((F.mapComp' (sq i₁ i₂).p₁.op.toLoc p.op.toLoc f₁.op.toLoc sorry).hom.toNatTrans.app (obj i₁) ≫
          Functor.map (Cat.Hom.toFunctor (F.map p.op.toLoc)) (hom i₁ i₂) ≫
            (F.mapComp' (sq i₁ i₂).p₂.op.toLoc p.op.toLoc f₂.op.toLoc sorry).inv.toNatTrans.app (obj' i₂)) ≫
      (F.mapComp' f₂.op.toLoc g.op.toLoc gf₂.op.toLoc sorry).inv.toNatTrans.app (obj' i₂) =
  (F.mapComp' (sq i₁ i₂).p₁.op.toLoc (CategoryStruct.comp (Y := { as := op Y }) p.op.toLoc g.op.toLoc) gf₁.op.toLoc
              sorry).hom.toNatTrans.app
      (obj i₁) ≫
    Functor.map
        (Cat.Hom.toFunctor
          (F.map (CategoryStruct.comp (Y := { as := op Y : LocallyDiscrete Cᵒᵖ }) p.op.toLoc g.op.toLoc)))
        (hom i₁ i₂) ≫
      (F.mapComp' (sq i₁ i₂).p₂.op.toLoc
                (CategoryStruct.comp (Y := { as := op Y : LocallyDiscrete Cᵒᵖ }) p.op.toLoc g.op.toLoc) gf₂.op.toLoc
                sorry).inv.toNatTrans.app
        (obj' i₂)
Tactic: dsimp [pullHom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
sq : (i j : ι) → ChosenPullback (f i) (f j)
obj obj' : (i : ι) → (↑(F.obj { as := op (X i) : LocallyDiscrete Cᵒᵖ }) : Type u')
hom :
  (i j : ι) →
    Quiver.Hom (V := (↑(F.obj { as := op (sq i j).pullback : LocallyDiscrete Cᵒᵖ }) : Type u'))
      (Functor.obj (Cat.Hom.toFunctor (F.map (sq i j).p₁.op.toLoc)) (obj i))
      (Functor.obj (Cat.Hom.toFunctor (F.map (sq i j).p₂.op.toLoc)) (obj' j))
Y Y' : C
g : Y' ⟶ Y
q : Y ⟶ S
q' : Y' ⟶ S
i₁ i₂ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
gf₁ : Y' ⟶ X i₁
gf₂ : Y' ⟶ X i₂
hq : g ≫ q = q'
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
hgf₁ : g ≫ f₁ = gf₁
hgf₂ : g ≫ f₂ = gf₂
p : Y ⟶ (sq i₁ i₂).pullback := ⋯.lift f₁ f₂ ⋯
⊢ Eq.{v + 1} (α := { as := op (X i₁) : LocallyDiscrete Cᵒᵖ } ⟶ { as := op Y })
    (CategoryStruct.comp (Y := { as := op (sq i₁ i₂).pullback }) (sq i₁ i₂).p₁.op.toLoc p.op.toLoc) f₁.op.toLoc
have rw : Eq.{v + 1} (α := { as := op (X i₁) : LocallyDiscrete Cᵒᵖ } ⟶ { as := op Y })
  (Quiver.Hom.toLoc ((sq i₁ i₂).p₁.op ≫ p.op)) f₁.op.toLoc
Tactic: rw [← Quiver.Hom.comp_toLoc, ← op_comp, IsPullback.lift_fst]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
sq : (i j : ι) → ChosenPullback (f i) (f j)
obj obj' : (i : ι) → (↑(F.obj { as := op (X i) : LocallyDiscrete Cᵒᵖ }) : Type u')
hom :
  (i j : ι) →
    Quiver.Hom (V := (↑(F.obj { as := op (sq i j).pullback : LocallyDiscrete Cᵒᵖ }) : Type u'))
      (Functor.obj (Cat.Hom.toFunctor (F.map (sq i j).p₁.op.toLoc)) (obj i))
      (Functor.obj (Cat.Hom.toFunctor (F.map (sq i j).p₂.op.toLoc)) (obj' j))
Y Y' : C
g : Y' ⟶ Y
q : Y ⟶ S
q' : Y' ⟶ S
i₁ i₂ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
gf₁ : Y' ⟶ X i₁
gf₂ : Y' ⟶ X i₂
hq : g ≫ q = q'
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
hgf₁ : g ≫ f₁ = gf₁
hgf₂ : g ≫ f₂ = gf₂
p : Y ⟶ (sq i₁ i₂).pullback := ⋯.lift f₁ f₂ ⋯
rw :
  Eq.{v + 1} (α := { as := op (X i₁) : LocallyDiscrete Cᵒᵖ } ⟶ { as := op Y })
    (Quiver.Hom.toLoc ((sq i₁ i₂).p₁.op ≫ p.op)) f₁.op.toLoc
⊢ Eq.{v + 1} (α := { as := op (X i₁) : LocallyDiscrete Cᵒᵖ } ⟶ { as := op Y })
    (CategoryStruct.comp (Y := { as := op (sq i₁ i₂).pullback }) (sq i₁ i₂).p₁.op.toLoc p.op.toLoc) f₁.op.toLoc
have rw₁ : Eq.{v + 1} (α := { as := op (X i₁) : LocallyDiscrete Cᵒᵖ } ⟶ { as := op Y }) (p ≫ (sq i₁ i₂).p₁).op.toLoc f₁.op.toLoc
Tactic: rw [← Quiver.Hom.comp_toLoc, ← op_comp, IsPullback.lift_fst]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
sq : (i j : ι) → ChosenPullback (f i) (f j)
obj obj' : (i : ι) → (↑(F.obj { as := op (X i) : LocallyDiscrete Cᵒᵖ }) : Type u')
hom :
  (i j : ι) →
    Quiver.Hom (V := (↑(F.obj { as := op (sq i j).pullback : LocallyDiscrete Cᵒᵖ }) : Type u'))
      (Functor.obj (Cat.Hom.toFunctor (F.map (sq i j).p₁.op.toLoc)) (obj i))
      (Functor.obj (Cat.Hom.toFunctor (F.map (sq i j).p₂.op.toLoc)) (obj' j))
Y Y' : C
g : Y' ⟶ Y
q : Y ⟶ S
q' : Y' ⟶ S
i₁ i₂ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
gf₁ : Y' ⟶ X i₁
gf₂ : Y' ⟶ X i₂
hq : g ≫ q = q'
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
hgf₁ : g ≫ f₁ = gf₁
hgf₂ : g ≫ f₂ = gf₂
p : Y ⟶ (sq i₁ i₂).pullback := ⋯.lift f₁ f₂ ⋯
rw :
  Eq.{v + 1} (α := { as := op (X i₁) : LocallyDiscrete Cᵒᵖ } ⟶ { as := op Y })
    (Quiver.Hom.toLoc ((sq i₁ i₂).p₁.op ≫ p.op)) f₁.op.toLoc
rw₁ :
  Eq.{v + 1} (α := { as := op (X i₁) : LocallyDiscrete Cᵒᵖ } ⟶ { as := op Y }) (p ≫ (sq i₁ i₂).p₁).op.toLoc f₁.op.toLoc
⊢ Eq.{v + 1} (α := { as := op (X i₁) : LocallyDiscrete Cᵒᵖ } ⟶ { as := op Y })
    (CategoryStruct.comp (Y := { as := op (sq i₁ i₂).pullback }) (sq i₁ i₂).p₁.op.toLoc p.op.toLoc) f₁.op.toLoc
have rw₂ : Eq.{v + 1} (α := { as := op (X i₁) : LocallyDiscrete Cᵒᵖ } ⟶ { as := op Y }) f₁.op.toLoc f₁.op.toLoc
Tactic: rw [← Quiver.Hom.comp_toLoc, ← op_comp, IsPullback.lift_fst]