awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.Precoverage (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology.{v, u} C
inst_1 : F.IsPrestack J
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
h₁ : Sieve.ofArrows X' f' ∈ (J : (a : C) → Set (Sieve a)) S
h₂ : Sieve.ofArrows X' f' ≤ Sieve.ofArrows X f
inst_2 : (F.toDescentData f').IsEquivalence
α : (i' : ι') → ι
p : (i' : ι') → X' i' ⟶ X (α i')
hp : ∀ (i' : ι'), p i' ≫ f (α i') = f' i'
⊢ (F.toDescentData f).IsEquivalence
have obtain : ∀ (H : F.DescentData f ⥤ F.DescentData f') (h : H.FullyFaithful) (e : F.toDescentData f ⋙ H ≅ F.toDescentData f'),
  (F.toDescentData f).IsEquivalence
Tactic: obtain ⟨H, h, ⟨e⟩⟩ :
      ∃ (H : _ ⥤ _) (_ : H.FullyFaithful),
        Nonempty (F.toDescentData f ⋙ H ≅ F.toDescentData f') := by
    refine ⟨pullFunctor F (p := 𝟙 _) (p' := p) (by cat_disch), ?_, ?_⟩
    · exact fullyFaithfulPullFunctor F hp h₁
    · exact ⟨toDescentDataCompPullFunctorIso _ _ ≪≫
          (Functor.isoWhiskerRight (Cat.Hom.toNatIso (F.mapId _)) _) ≪≫
            Functor.leftUnitor _⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.Precoverage (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology.{v, u} C
inst_1 : F.IsPrestack J
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
h₁ : Sieve.ofArrows X' f' ∈ (J : (a : C) → Set (Sieve a)) S
h₂ : Sieve.ofArrows X' f' ≤ Sieve.ofArrows X f
inst_2 : (F.toDescentData f').IsEquivalence
α : (i' : ι') → ι
p : (i' : ι') → X' i' ⟶ X (α i')
hp : ∀ (i' : ι'), p i' ≫ f (α i') = f' i'
H : F.DescentData f ⥤ F.DescentData f'
h : H.FullyFaithful
e : F.toDescentData f ⋙ H ≅ F.toDescentData f'
⊢ (F.toDescentData f).IsEquivalence
have this : (F.toDescentData f).Faithful
Tactic: have := (F.fullyFaithfulToDescentData _ (J.superset_covering h₂ h₁)).faithful
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.Precoverage (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology.{v, u} C
inst_1 : F.IsPrestack J
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
h₁ : Sieve.ofArrows X' f' ∈ (J : (a : C) → Set (Sieve a)) S
h₂ : Sieve.ofArrows X' f' ≤ Sieve.ofArrows X f
inst_2 : (F.toDescentData f').IsEquivalence
α : (i' : ι') → ι
p : (i' : ι') → X' i' ⟶ X (α i')
hp : ∀ (i' : ι'), p i' ≫ f (α i') = f' i'
H : F.DescentData f ⥤ F.DescentData f'
h : H.FullyFaithful
e : F.toDescentData f ⋙ H ≅ F.toDescentData f'
this : (F.toDescentData f).Faithful
⊢ (F.toDescentData f).IsEquivalence
have this₁ : (F.toDescentData f).Full
Tactic: have := (F.fullyFaithfulToDescentData _ (J.superset_covering h₂ h₁)).full
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.Precoverage (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology.{v, u} C
inst_1 : F.IsPrestack J
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
h₁ : Sieve.ofArrows X' f' ∈ (J : (a : C) → Set (Sieve a)) S
h₂ : Sieve.ofArrows X' f' ≤ Sieve.ofArrows X f
inst_2 : (F.toDescentData f').IsEquivalence
α : (i' : ι') → ι
p : (i' : ι') → X' i' ⟶ X (α i')
hp : ∀ (i' : ι'), p i' ≫ f (α i') = f' i'
H : F.DescentData f ⥤ F.DescentData f'
h : H.FullyFaithful
e : F.toDescentData f ⋙ H ≅ F.toDescentData f'
this_1 : (F.toDescentData f).Faithful
this : (F.toDescentData f).Full
⊢ (F.toDescentData f).IsEquivalence
have this₁ : (F.toDescentData f).EssSurj
Tactic: have : (F.toDescentData f).EssSurj := ⟨fun D ↦
    ⟨_, ⟨h.preimageIso (e.app _ ≪≫ (F.toDescentData f').objObjPreimageIso (H.obj D))⟩⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.Precoverage (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
S : C
R : Presieve.{v, u} S
hR₁ : F.IsStackFor R
J : GrothendieckTopology.{v, u} C
hR₂ : Sieve.generate R ∈ (J : (a : C) → Set (Sieve a)) S
inst_1 : F.IsPrestack J
R' : Presieve.{v, u} S
h : R ≤ R'
⊢ F.IsStackFor R'
have obtain : ∀ (ι : Type (max u v)) (w : ι → C) (f : (i : ι) → w i ⟶ S) (hR₁ : F.IsStackFor (Presieve.ofArrows w f))
  (hR₂ : Sieve.generate (Presieve.ofArrows w f) ∈ (J : (a : C) → Set (Sieve a)) S) (h : Presieve.ofArrows w f ≤ R'),
  F.IsStackFor R'
Tactic: obtain ⟨ι, _, f, rfl⟩ := R.exists_eq_ofArrows
Cleared hypotheses: R, hR₁, hR₂, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.Precoverage (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
S : C
J : GrothendieckTopology.{v, u} C
inst_1 : F.IsPrestack J
R' : Presieve.{v, u} S
ι : Type (max u v)
w : ι → C
f : (i : ι) → w i ⟶ S
hR₁ : F.IsStackFor (Presieve.ofArrows w f)
hR₂ : Sieve.generate (Presieve.ofArrows w f) ∈ (J : (a : C) → Set (Sieve a)) S
h : Presieve.ofArrows w f ≤ R'
⊢ F.IsStackFor R'
have obtain : ∀ (ι' : Type (max u v)) (w_1 : ι' → C) (f' : (i : ι') → w_1 i ⟶ S)
  (h : Presieve.ofArrows w f ≤ Presieve.ofArrows w_1 f'), F.IsStackFor (Presieve.ofArrows w_1 f')
Tactic: obtain ⟨ι', _, f', rfl⟩ := R'.exists_eq_ofArrows
Cleared hypotheses: R', h
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.Precoverage (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
S : C
J : GrothendieckTopology.{v, u} C
inst_1 : F.IsPrestack J
ι : Type (max u v)
w : ι → C
f : (i : ι) → w i ⟶ S
hR₁ : F.IsStackFor (Presieve.ofArrows w f)
hR₂ : Sieve.generate (Presieve.ofArrows w f) ∈ (J : (a : C) → Set (Sieve a)) S
ι' : Type (max u v)
w_1 : ι' → C
f' : (i : ι') → w_1 i ⟶ S
h : Presieve.ofArrows w f ≤ Presieve.ofArrows w_1 f'
⊢ F.IsStackFor (Presieve.ofArrows w_1 f')
have rw : ∀ (hR₁ : (F.toDescentData f).IsEquivalence)
  (hR₂ : Sieve.generate (Presieve.ofArrows w f) ∈ (J : (a : C) → Set (Sieve a)) S) (ι' : Type (max u v)) (w_2 : ι' → C)
  (f' : (i : ι') → w_2 i ⟶ S) (h : Presieve.ofArrows w f ≤ Presieve.ofArrows w_2 f'), (F.toDescentData f').IsEquivalence
Tactic: rw [isStackFor_ofArrows_iff] at hR₁ ⊢
Cleared hypotheses: hR₁, hR₂, ι', w_1, f', h
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.Precoverage (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
inst_1 : HasPullbacks.{v, u} C
J : Precoverage.{v, u} C
inst_2 : J.HasIsos
inst_3 : J.IsStableUnderBaseChange
inst_4 : J.IsStableUnderComposition
hF : ∀ (S : C), ∀ R ∈ J.coverings S, F.IsPrestackFor R
S : C
M N : (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')
⊢ Presheaf.IsSheaf (J.toGrothendieck.over S) (F.presheafHom M N)
have rw : ∀ {X : Over.{v, u} S},
  ∀
    R ∈
      (Pretopology.toPrecoverage
            (Precoverage.toPretopology (Over.{v, u} S) (Precoverage.comap (Over.forget S) J))).coverings
        X,
    Presieve.IsSheafFor (F.presheafHom M N) R
Tactic: rw [isSheaf_iff_isSheaf_of_type,
      over_toGrothendieck_eq_toGrothendieck_comap_forget,
      ← Precoverage.toGrothendieck_toPretopology_eq_toGrothendieck,
      Presieve.isSheaf_pretopology]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.Precoverage (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
inst_1 : HasPullbacks.{v, u} C
J : Precoverage.{v, u} C
inst_2 : J.HasIsos
inst_3 : J.IsStableUnderBaseChange
inst_4 : J.IsStableUnderComposition
hF : ∀ (S : C), ∀ R ∈ J.coverings S, F.IsPrestackFor R
S : C
M N : (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')
X : Over.{v, u} S
R : Presieve X
hR :
  R ∈
    (Pretopology.toPrecoverage
          (Precoverage.toPretopology (Over.{v, u} S) (Precoverage.comap (Over.forget S) J))).coverings
      X
⊢ Presieve.IsSheafFor (F.presheafHom M N) R
have hR₁ : Membership.mem (γ := Set (Presieve.{v, u} X.left)) (J.coverings X.left) (Presieve.map (Over.forget S) R)
Tactic: simp only [Precoverage.toPretopology_toPrecoverage, Precoverage.mem_comap_iff,
      Over.forget_obj] at hR
Cleared hypotheses: hR
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.Precoverage (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
inst_1 : HasPullbacks.{v, u} C
J : Precoverage.{v, u} C
inst_2 : J.HasIsos
inst_3 : J.IsStableUnderBaseChange
inst_4 : J.IsStableUnderComposition
hF : ∀ (S : C), ∀ R ∈ J.coverings S, F.IsPrestackFor R
S : C
M N : (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')
X : Over.{v, u} S
R : Presieve X
hR : Membership.mem (γ := Set (Presieve.{v, u} X.left)) (J.coverings X.left) (Presieve.map (Over.forget S) R)
⊢ Presieve.IsSheafFor (F.presheafHom M N) R
have obtain : ∀ (R' : Sieve.{v, u} X.left) (hR' : ((Sieve.overEquiv X).symm : (a : Sieve X.left) → Sieve X) R' = Sieve.generate R),
  Presieve.IsSheafFor (F.presheafHom M N) R
Tactic: obtain ⟨R', hR'⟩ := (Sieve.overEquiv _).symm.surjective (Sieve.generate R)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.Precoverage (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
inst_1 : HasPullbacks.{v, u} C
J : Precoverage.{v, u} C
inst_2 : J.HasIsos
inst_3 : J.IsStableUnderBaseChange
inst_4 : J.IsStableUnderComposition
hF : ∀ (S : C), ∀ R ∈ J.coverings S, F.IsPrestackFor R
S : C
M N : (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')
X : Over.{v, u} S
R : Presieve X
hR : Membership.mem (γ := Set (Presieve.{v, u} X.left)) (J.coverings X.left) (Presieve.map (Over.forget S) R)
R' : Sieve.{v, u} X.left
hR' : ((Sieve.overEquiv X).symm : (a : Sieve X.left) → Sieve X) R' = Sieve.generate R
⊢ Presieve.IsSheafFor (F.presheafHom M N) R
have rw : Presieve.IsSheafFor (F.presheafHom M N) (Sieve.generate R).arrows
Tactic: rw [Presieve.isSheafFor_iff_generate]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.Precoverage (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
inst_1 : HasPullbacks.{v, u} C
J : Precoverage.{v, u} C
inst_2 : J.HasIsos
inst_3 : J.IsStableUnderBaseChange
inst_4 : J.IsStableUnderComposition
hF : ∀ (S : C), ∀ R ∈ J.coverings S, F.IsPrestackFor R
S : C
M N : (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')
X : Over.{v, u} S
R : Presieve X
hR : Membership.mem (γ := Set (Presieve.{v, u} X.left)) (J.coverings X.left) (Presieve.map (Over.forget S) R)
R' : Sieve.{v, u} X.left
hR' : ((Sieve.overEquiv X).symm : (a : Sieve X.left) → Sieve X) R' = Sieve.generate R
⊢ Presieve.IsSheafFor (F.presheafHom M N) (Sieve.generate R).arrows
have hF₁ : F.IsPrestackFor (S := X.left) (Sieve.arrows ((Sieve.overEquiv X : (a : Sieve X) → Sieve X.left) (Sieve.generate R)))
Tactic: apply IsPrestackFor.isSheafFor'
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.Precoverage (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
inst_1 : HasPullbacks.{v, u} C
J : Precoverage.{v, u} C
inst_2 : J.HasIsos
inst_3 : J.IsStableUnderBaseChange
inst_4 : J.IsStableUnderComposition
hF : ∀ (S : C), ∀ R ∈ J.coverings S, F.IsStackFor R
⊢ F.IsStack J.toGrothendieck
have this : F.IsPrestack J.toGrothendieck
Tactic: have := IsPrestack.of_precoverage (fun S R hR ↦ (hF _ _ hR).isPrestackFor)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.Precoverage (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
inst_1 : HasPullbacks.{v, u} C
J : Precoverage.{v, u} C
inst_2 : J.HasIsos
inst_3 : J.IsStableUnderBaseChange
inst_4 : J.IsStableUnderComposition
hF : ∀ (S : C), ∀ R ∈ J.coverings S, F.IsStackFor R
this : F.IsPrestack J.toGrothendieck
⊢ F.IsStack J.toGrothendieck
have refine : ∀ {S : C} (R : Sieve.{v, u} S) (hR : R ∈ (J.toGrothendieck : (a : C) → Set (Sieve a)) S), F.IsStackFor R.arrows
Tactic: refine ⟨fun {S} R hR ↦ IsStackFor.essSurj ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.Precoverage (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
inst_1 : HasPullbacks.{v, u} C
J : Precoverage.{v, u} C
inst_2 : J.HasIsos
inst_3 : J.IsStableUnderBaseChange
inst_4 : J.IsStableUnderComposition
hF : ∀ (S : C), ∀ R ∈ J.coverings S, F.IsStackFor R
this : F.IsPrestack J.toGrothendieck
S : C
R : Sieve.{v, u} S
hR : R ∈ (J.toGrothendieck : (a : C) → Set (Sieve a)) S
⊢ F.IsStackFor R.arrows
have hR₁ : R ∈ (Pretopology.toGrothendieck (Precoverage.toPretopology C J) : (a : C) → Set (Sieve a)) S
Tactic: rw [← J.toGrothendieck_toPretopology_eq_toGrothendieck] at hR
Cleared hypotheses: hR
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.Precoverage (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
inst_1 : HasPullbacks.{v, u} C
J : Precoverage.{v, u} C
inst_2 : J.HasIsos
inst_3 : J.IsStableUnderBaseChange
inst_4 : J.IsStableUnderComposition
hF : ∀ (S : C), ∀ R ∈ J.coverings S, F.IsStackFor R
this : F.IsPrestack J.toGrothendieck
S : C
R : Sieve.{v, u} S
hR : R ∈ (Pretopology.toGrothendieck (Precoverage.toPretopology C J) : (a : C) → Set (Sieve a)) S
⊢ F.IsStackFor R.arrows
have obtain : ∀ (R' : Presieve.{v, u} S) (hR' : R' ∈ (Pretopology.toPrecoverage (Precoverage.toPretopology C J)).coverings S)
  (h : R' ≤ R.arrows), F.IsStackFor R.arrows
Tactic: obtain ⟨R', hR', h⟩ := hR
Cleared hypotheses: hR
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.EffectiveEpimorphic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : Y ⟶ X
⊢ generate (Presieve.singleton f) = generateSingleton f
have h : ∀ ⦃Z : C⦄ (g : Z ⟶ X), (generate (Presieve.singleton f)).arrows g ↔ (generateSingleton f).arrows g
Tactic: ext Z g
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.EffectiveEpimorphic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ X
⊢ (generate (Presieve.singleton f)).arrows g ↔ (generateSingleton f).arrows g
have h : (generate (Presieve.singleton f)).arrows g → (generateSingleton f).arrows g
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.EffectiveEpimorphic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ X
h : (generate (Presieve.singleton f)).arrows g → (generateSingleton f).arrows g
⊢ (generate (Presieve.singleton f)).arrows g ↔ (generateSingleton f).arrows g
have h₁ : (generateSingleton f).arrows g → (generate (Presieve.singleton f)).arrows g
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.EffectiveEpimorphic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : C
R : Presieve.{v, u} X
⊢ R.EffectiveEpimorphic ↔ ∀ (Y : C), IsSheafFor (Functor.obj yoneda Y) R
have simp_rw : R.EffectiveEpimorphic ↔ ∀ (Y : C), IsSheafFor (Functor.obj yoneda Y) (Sieve.generate R).arrows
Tactic: simp_rw [Presieve.isSheafFor_iff_generate R,
    Presieve.EffectiveEpimorphic, Sieve.EffectiveEpimorphic.iff_forall_isSheafFor_yoneda]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.EffectiveEpimorphic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : C
R : Presieve.{v, u} X
simp_rw : R.EffectiveEpimorphic ↔ ∀ (Y : C), IsSheafFor (Functor.obj yoneda Y) (Sieve.generate R).arrows
⊢ R.EffectiveEpimorphic ↔ ∀ (Y : C), IsSheafFor (Functor.obj yoneda Y) R
have simp_rw₁ : (Sieve.generate R).EffectiveEpimorphic ↔ ∀ (Y : C), IsSheafFor (Functor.obj yoneda Y) (Sieve.generate R).arrows
Tactic: simp_rw [Presieve.isSheafFor_iff_generate R,
    Presieve.EffectiveEpimorphic, Sieve.EffectiveEpimorphic.iff_forall_isSheafFor_yoneda]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.EffectiveEpimorphic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : C
R : Presieve.{v, u} X
hR : R.EffectiveEpimorphic
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
inst_1 : F.IsRepresentable
⊢ IsSheafFor F R
have rw : ∀ (hR : ∀ (Y : C), IsSheafFor (Functor.obj yoneda Y) R) (F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)) [F.IsRepresentable],
  IsSheafFor F R
Tactic: rw [Presieve.EffectiveEpimorphic.iff_forall_isSheafFor_yoneda] at hR
Cleared hypotheses: hR, F, inst_1
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.EffectiveEpimorphic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : C
R : Presieve.{v, u} X
hR : ∀ (Y : C), IsSheafFor (Functor.obj yoneda Y) R
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
inst_1 : F.IsRepresentable
⊢ IsSheafFor F R
have rw : IsSheafFor (F ⋙ uliftFunctor.{v, w}) R
Tactic: rw [← isSheafFor_comp_uliftFunctor_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.EffectiveEpimorphic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : C
R : Presieve.{v, u} X
hR : ∀ (Y : C), IsSheafFor (Functor.obj yoneda Y) R
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
inst_1 : F.IsRepresentable
⊢ IsSheafFor (F ⋙ uliftFunctor.{v, w}) R
have refine : IsSheafFor (Functor.obj uliftYoneda.{w, v, u} (F ⋙ uliftFunctor.{v, w}).reprX) R
Tactic: refine Presieve.isSheafFor_iso (F ⋙ uliftFunctor.{v}).uliftYonedaReprXIso ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.EffectiveEpimorphic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : C
R : Presieve.{v, u} X
hR : ∀ (Y : C), IsSheafFor (Functor.obj yoneda Y) R
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
inst_1 : F.IsRepresentable
⊢ IsSheafFor (Functor.obj yoneda (F ⋙ uliftFunctor.{v, w}).reprX ⋙ uliftFunctor.{w, v}) R
have rw : IsSheafFor (Functor.obj yoneda (F ⋙ uliftFunctor.{v, w}).reprX) R
Tactic: rw [isSheafFor_comp_uliftFunctor_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.EffectiveEpimorphic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : Y ⟶ X
Hf : IsColimit (Sieve.generateSingleton f).arrows.cocone
W : C
e : Y ⟶ W
h : ∀ {Z : C} (g₁ g₂ : Z ⟶ Y), g₁ ≫ f = g₂ ≫ f → g₁ ≫ e = g₂ ≫ e
A : Over.{v, u} X
hA : (Sieve.generateSingleton f).arrows A.hom
B : Over.{v, u} X
hB : (Sieve.generateSingleton f).arrows B.hom
q : A ⟶ B
⊢ Eq (α :=
    (Sieve.generateSingleton f).arrows.diagram.obj
        (ObjectProperty.FullSubcategory.mk (P := fun (f_1 : Over.{v, u} X) ↦ (Sieve.generateSingleton f).arrows f_1.hom)
          A hA) ⟶
      Functor.obj (C := (Sieve.generateSingleton f).arrows.category)
        (Functor.obj (Functor.const (Sieve.generateSingleton f).arrows.category) W)
        (ObjectProperty.FullSubcategory.mk (P := fun (f_1 : Over.{v, u} X) ↦ (Sieve.generateSingleton f).arrows f_1.hom)
          B hB))
    (CategoryStruct.comp (Y :=
      (Sieve.generateSingleton f).arrows.diagram.obj
        (ObjectProperty.FullSubcategory.mk (P := fun (f_1 : Over.{v, u} X) ↦ (Sieve.generateSingleton f).arrows f_1.hom)
          B hB))
      ((Sieve.generateSingleton f).arrows.diagram.map { hom := q })
      (match (motive :=
        (x : (Sieve.generateSingleton f).arrows.category) →
          (Sieve.generateSingleton f).arrows.diagram.obj x ⟶
            Functor.obj (Functor.obj (Functor.const (Sieve.generateSingleton f).arrows.category) W) x)
        ObjectProperty.FullSubcategory.mk (P := fun (f_1 : Over.{v, u} X) ↦ (Sieve.generateSingleton f).arrows f_1.hom)
          B hB with
      | { obj := obj, property := hT } => Exists.choose (p := fun (e : obj.left ⟶ Y) ↦ e ≫ f = obj.hom) hT ≫ e))
    (CategoryStruct.comp (Y :=
      Functor.obj (C := (Sieve.generateSingleton f).arrows.category)
        (Functor.obj (Functor.const (Sieve.generateSingleton f).arrows.category) W)
        (ObjectProperty.FullSubcategory.mk (P := fun (f_1 : Over.{v, u} X) ↦ (Sieve.generateSingleton f).arrows f_1.hom)
          A hA))
      (match (motive :=
        (x : (Sieve.generateSingleton f).arrows.category) →
          (Sieve.generateSingleton f).arrows.diagram.obj x ⟶
            Functor.obj (Functor.obj (Functor.const (Sieve.generateSingleton f).arrows.category) W) x)
        ObjectProperty.FullSubcategory.mk (P := fun (f_1 : Over.{v, u} X) ↦ (Sieve.generateSingleton f).arrows f_1.hom)
          A hA with
      | { obj := obj, property := hT } => Exists.choose (p := fun (e : obj.left ⟶ Y) ↦ e ≫ f = obj.hom) hT ≫ e)
      (Functor.map (Functor.obj (Functor.const (Sieve.generateSingleton f).arrows.category) W) { hom := q }))
have dsimp : Over.Hom.left q ≫ Exists.choose (p := fun (e : B.left ⟶ Y) ↦ e ≫ f = B.hom) hB ≫ e =
  (Exists.choose (p := fun (e : A.left ⟶ Y) ↦ e ≫ f = A.hom) hA ≫ e) ≫ 𝟙 W
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.EffectiveEpimorphic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : Y ⟶ X
Hf : IsColimit (Sieve.generateSingleton f).arrows.cocone
W : C
e : Y ⟶ W
h : ∀ {Z : C} (g₁ g₂ : Z ⟶ Y), g₁ ≫ f = g₂ ≫ f → g₁ ≫ e = g₂ ≫ e
A : Over.{v, u} X
hA : (Sieve.generateSingleton f).arrows A.hom
B : Over.{v, u} X
hB : (Sieve.generateSingleton f).arrows B.hom
q : A ⟶ B
⊢ Over.Hom.left q ≫ Exists.choose (p := fun (e : B.left ⟶ Y) ↦ e ≫ f = B.hom) hB ≫ e =
    (Exists.choose (p := fun (e : A.left ⟶ Y) ↦ e ≫ f = A.hom) hA ≫ e) ≫ 𝟙 W
have simp : (Over.Hom.left q ≫ Exists.choose (p := fun (e : B.left ⟶ Y) ↦ e ≫ f = B.hom) hB) ≫ e =
  Exists.choose (p := fun (e : A.left ⟶ Y) ↦ e ≫ f = A.hom) hA ≫ e
Tactic: simp only [← Category.assoc, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.EffectiveEpimorphic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : Y ⟶ X
Hf : IsColimit (Sieve.generateSingleton f).arrows.cocone
W : C
e : Y ⟶ W
h : ∀ {Z : C} (g₁ g₂ : Z ⟶ Y), g₁ ≫ f = g₂ ≫ f → g₁ ≫ e = g₂ ≫ e
A : Over.{v, u} X
hA : (Sieve.generateSingleton f).arrows A.hom
B : Over.{v, u} X
hB : (Sieve.generateSingleton f).arrows B.hom
q : A ⟶ B
⊢ (Over.Hom.left q ≫ Exists.choose (p := fun (e : B.left ⟶ Y) ↦ e ≫ f = B.hom) hB) ≫ e =
    Exists.choose (p := fun (e : A.left ⟶ Y) ↦ e ≫ f = A.hom) hA ≫ e
have a : (Over.Hom.left q ≫ Exists.choose (p := fun (e : B.left ⟶ Y) ↦ e ≫ f = B.hom) hB) ≫ f =
  Exists.choose (p := fun (e : A.left ⟶ Y) ↦ e ≫ f = A.hom) hA ≫ f
Tactic: apply h
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.EffectiveEpimorphic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : Y ⟶ X
Hf : IsColimit (Sieve.generateSingleton f).arrows.cocone
W : C
e : Y ⟶ W
h : ∀ {Z : C} (g₁ g₂ : Z ⟶ Y), g₁ ≫ f = g₂ ≫ f → g₁ ≫ e = g₂ ≫ e
A : Over.{v, u} X
hA : (Sieve.generateSingleton f).arrows A.hom
B : Over.{v, u} X
hB : (Sieve.generateSingleton f).arrows B.hom
q : A ⟶ B
⊢ (Over.Hom.left q ≫ Exists.choose (p := fun (e : B.left ⟶ Y) ↦ e ≫ f = B.hom) hB) ≫ f =
    Exists.choose (p := fun (e : A.left ⟶ Y) ↦ e ≫ f = A.hom) hA ≫ f
have a : Over.Hom.left q ≫ Exists.choose (p := fun (e : B.left ⟶ Y) ↦ e ≫ f = B.hom) hB ≫ f =
  Exists.choose (p := fun (e : A.left ⟶ Y) ↦ e ≫ f = A.hom) hA ≫ f
Tactic: rw [Category.assoc, hB.choose_spec, hA.choose_spec, Over.w]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.EffectiveEpimorphic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : Y ⟶ X
Hf : IsColimit (Sieve.generateSingleton f).arrows.cocone
W : C
e : Y ⟶ W
h : ∀ {Z : C} (g₁ g₂ : Z ⟶ Y), g₁ ≫ f = g₂ ≫ f → g₁ ≫ e = g₂ ≫ e
A : Over.{v, u} X
hA : (Sieve.generateSingleton f).arrows A.hom
B : Over.{v, u} X
hB : (Sieve.generateSingleton f).arrows B.hom
q : A ⟶ B
a :
  Over.Hom.left q ≫ Exists.choose (p := fun (e : B.left ⟶ Y) ↦ e ≫ f = B.hom) hB ≫ f =
    Exists.choose (p := fun (e : A.left ⟶ Y) ↦ e ≫ f = A.hom) hA ≫ f
⊢ (Over.Hom.left q ≫ Exists.choose (p := fun (e : B.left ⟶ Y) ↦ e ≫ f = B.hom) hB) ≫ f =
    Exists.choose (p := fun (e : A.left ⟶ Y) ↦ e ≫ f = A.hom) hA ≫ f
have a₁ : Over.Hom.left q ≫ B.hom = Exists.choose (p := fun (e : A.left ⟶ Y) ↦ e ≫ f = A.hom) hA ≫ f
Tactic: rw [Category.assoc, hB.choose_spec, hA.choose_spec, Over.w]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.EffectiveEpimorphic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : Y ⟶ X
Hf : IsColimit (Sieve.generateSingleton f).arrows.cocone
W : C
e : Y ⟶ W
h : ∀ {Z : C} (g₁ g₂ : Z ⟶ Y), g₁ ≫ f = g₂ ≫ f → g₁ ≫ e = g₂ ≫ e
A : Over.{v, u} X
hA : (Sieve.generateSingleton f).arrows A.hom
B : Over.{v, u} X
hB : (Sieve.generateSingleton f).arrows B.hom
q : A ⟶ B
a :
  Over.Hom.left q ≫ Exists.choose (p := fun (e : B.left ⟶ Y) ↦ e ≫ f = B.hom) hB ≫ f =
    Exists.choose (p := fun (e : A.left ⟶ Y) ↦ e ≫ f = A.hom) hA ≫ f
a₁ : Over.Hom.left q ≫ B.hom = Exists.choose (p := fun (e : A.left ⟶ Y) ↦ e ≫ f = A.hom) hA ≫ f
⊢ (Over.Hom.left q ≫ Exists.choose (p := fun (e : B.left ⟶ Y) ↦ e ≫ f = B.hom) hB) ≫ f =
    Exists.choose (p := fun (e : A.left ⟶ Y) ↦ e ≫ f = A.hom) hA ≫ f
have a₂ : Over.Hom.left q ≫ B.hom = A.hom
Tactic: rw [Category.assoc, hB.choose_spec, hA.choose_spec, Over.w]