awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_3
inst : Category.{u_2, u_3} C
J : Precoverage.{u_2, u_3} C
P : Functor.{u_2, u_1, u_3, u_1 + 1} Cᵒᵖ (Type u_1)
X_1 : C
S_1 : Sieve.{u_2, u_3} X_1
X : C
R S : Sieve.{u_2, u_3} X
hS : J.Saturate X R
h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → J.Saturate Y (Sieve.pullback f S)
Y : C
f : Y ⟶ X
H :
  ∀ {X Y : C} {f : Y ⟶ X},
    ∀ R ∈ J.coverings X,
      Presieve.IsSeparatedFor P (Sieve.pullback f (Sieve.generate R)).arrows ∧
        ∀ (x : Presieve.FamilyOfElements P (Sieve.pullback f (Sieve.generate R)).arrows),
          x.Compatible (R := (Sieve.pullback f (Sieve.generate R)).arrows) →
            ∃ (t : P.obj (Opposite.op Y)), x.IsAmalgamation (R := (Sieve.pullback f (Sieve.generate R)).arrows) t
H1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X), Presieve.IsSeparatedFor P (Sieve.pullback f R).arrows
H1' :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (x : Presieve.FamilyOfElements P (Sieve.pullback f R).arrows),
    x.Compatible (R := (Sieve.pullback f R).arrows) →
      ∃ (t : P.obj (Opposite.op Y)), x.IsAmalgamation (R := (Sieve.pullback f R).arrows) t
H2 :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y), Presieve.IsSeparatedFor P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows
H2' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f →
      ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y) (x : Presieve.FamilyOfElements P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows),
        x.Compatible (R := (Sieve.pullback f_1 (Sieve.pullback f S)).arrows) →
          ∃ (t : P.obj (Opposite.op Y_1)), x.IsAmalgamation (R := (Sieve.pullback f_1 (Sieve.pullback f S)).arrows) t
x : Presieve.FamilyOfElements P (Sieve.pullback f S).arrows
hx : x.Compatible (R := (Sieve.pullback f S).arrows)
y : ⦃Z : C⦄ → (g : Z ⟶ Y) → Presieve.FamilyOfElements P (Sieve.pullback (𝟙 Z) (Sieve.pullback (g ≫ f) S)).arrows :=
  fun (Z : C) (g : Z ⟶ Y) (ZZ : C) (gg : ZZ ⟶ Z) (hgg : (Sieve.pullback (𝟙 Z) (Sieve.pullback (g ≫ f) S)).arrows gg) ↦
    x (gg ≫ g) ⋯
hy : ∀ ⦃Z : C⦄ (g : Z ⟶ Y), (y g).Compatible (R := (Sieve.pullback (𝟙 Z) (Sieve.pullback (g ≫ f) S)).arrows)
z : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → (hg : (Sieve.pullback f R).arrows g) → P.obj (Opposite.op Z)
hz :
  ∀ ⦃Z : C⦄ ⦃g : Z ⟶ Y⦄ (hg : (Sieve.pullback f R).arrows g),
    (y g).IsAmalgamation (R := (Sieve.pullback (𝟙 Z) (Sieve.pullback (g ≫ f) S)).arrows) (z hg)
q : Presieve.FamilyOfElements P (Sieve.pullback f R).arrows :=
  fun (Z : C) (g : Z ⟶ Y) (hg : (Sieve.pullback f R).arrows g) ↦ z hg
hq : q.Compatible (R := (Sieve.pullback f R).arrows)
t : P.obj (Opposite.op Y)
ht : q.IsAmalgamation (R := (Sieve.pullback f R).arrows) t
Z : C
g : Z ⟶ Y
hg : (Sieve.pullback f S).arrows g
ZZ : C
gg : ZZ ⟶ Z
hgg : (Sieve.pullback (g ≫ f) R).arrows gg
⊢ (Sieve.pullback f R).arrows (gg ≫ g)

Tactic:
simpa using hgg
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_3
inst : Category.{u_2, u_3} C
J : Precoverage.{u_2, u_3} C
P : Functor.{u_2, u_1, u_3, u_1 + 1} Cᵒᵖ (Type u_1)
X_1 : C
S_1 : Sieve.{u_2, u_3} X_1
X : C
R S : Sieve.{u_2, u_3} X
hS : J.Saturate X R
h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → J.Saturate Y (Sieve.pullback f S)
Y : C
f : Y ⟶ X
H :
  ∀ {X Y : C} {f : Y ⟶ X},
    ∀ R ∈ J.coverings X,
      Presieve.IsSeparatedFor P (Sieve.pullback f (Sieve.generate R)).arrows ∧
        ∀ (x : Presieve.FamilyOfElements P (Sieve.pullback f (Sieve.generate R)).arrows),
          x.Compatible (R := (Sieve.pullback f (Sieve.generate R)).arrows) →
            ∃ (t : P.obj (Opposite.op Y)), x.IsAmalgamation (R := (Sieve.pullback f (Sieve.generate R)).arrows) t
H1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X), Presieve.IsSeparatedFor P (Sieve.pullback f R).arrows
H1' :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (x : Presieve.FamilyOfElements P (Sieve.pullback f R).arrows),
    x.Compatible (R := (Sieve.pullback f R).arrows) →
      ∃ (t : P.obj (Opposite.op Y)), x.IsAmalgamation (R := (Sieve.pullback f R).arrows) t
H2 :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y), Presieve.IsSeparatedFor P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows
H2' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f →
      ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y) (x : Presieve.FamilyOfElements P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows),
        x.Compatible (R := (Sieve.pullback f_1 (Sieve.pullback f S)).arrows) →
          ∃ (t : P.obj (Opposite.op Y_1)), x.IsAmalgamation (R := (Sieve.pullback f_1 (Sieve.pullback f S)).arrows) t
x : Presieve.FamilyOfElements P (Sieve.pullback f S).arrows
hx : x.Compatible (R := (Sieve.pullback f S).arrows)
y : ⦃Z : C⦄ → (g : Z ⟶ Y) → Presieve.FamilyOfElements P (Sieve.pullback (𝟙 Z) (Sieve.pullback (g ≫ f) S)).arrows :=
  fun (Z : C) (g : Z ⟶ Y) (ZZ : C) (gg : ZZ ⟶ Z) (hgg : (Sieve.pullback (𝟙 Z) (Sieve.pullback (g ≫ f) S)).arrows gg) ↦
    x (gg ≫ g) ⋯
hy : ∀ ⦃Z : C⦄ (g : Z ⟶ Y), (y g).Compatible (R := (Sieve.pullback (𝟙 Z) (Sieve.pullback (g ≫ f) S)).arrows)
z : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → (hg : (Sieve.pullback f R).arrows g) → P.obj (Opposite.op Z)
hz :
  ∀ ⦃Z : C⦄ ⦃g : Z ⟶ Y⦄ (hg : (Sieve.pullback f R).arrows g),
    (y g).IsAmalgamation (R := (Sieve.pullback (𝟙 Z) (Sieve.pullback (g ≫ f) S)).arrows) (z hg)
q : Presieve.FamilyOfElements P (Sieve.pullback f R).arrows :=
  fun (Z : C) (g : Z ⟶ Y) (hg : (Sieve.pullback f R).arrows g) ↦ z hg
hq : q.Compatible (R := (Sieve.pullback f R).arrows)
t : P.obj (Opposite.op Y)
ht : q.IsAmalgamation (R := (Sieve.pullback f R).arrows) t
Z : C
g : Z ⟶ Y
hg : (Sieve.pullback f S).arrows g
ZZ : C
gg : ZZ ⟶ Z
hgg : (Sieve.pullback (g ≫ f) R).arrows gg
⊢ (Sieve.pullback f R).arrows (gg ≫ g)

Tactic:
on_goal 2 => simpa using hgg
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_3
inst : Category.{u_2, u_3} C
J : Precoverage.{u_2, u_3} C
P : Functor.{u_2, u_1, u_3, u_1 + 1} Cᵒᵖ (Type u_1)
X_1 : C
S_1 : Sieve.{u_2, u_3} X_1
X : C
R S : Sieve.{u_2, u_3} X
hS : J.Saturate X R
h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → J.Saturate Y (Sieve.pullback f S)
Y : C
f : Y ⟶ X
H :
  ∀ {X Y : C} {f : Y ⟶ X},
    ∀ R ∈ J.coverings X,
      Presieve.IsSeparatedFor P (Sieve.pullback f (Sieve.generate R)).arrows ∧
        ∀ (x : Presieve.FamilyOfElements P (Sieve.pullback f (Sieve.generate R)).arrows),
          x.Compatible (R := (Sieve.pullback f (Sieve.generate R)).arrows) →
            ∃ (t : P.obj (Opposite.op Y)), x.IsAmalgamation (R := (Sieve.pullback f (Sieve.generate R)).arrows) t
H1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X), Presieve.IsSeparatedFor P (Sieve.pullback f R).arrows
H1' :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (x : Presieve.FamilyOfElements P (Sieve.pullback f R).arrows),
    x.Compatible (R := (Sieve.pullback f R).arrows) →
      ∃ (t : P.obj (Opposite.op Y)), x.IsAmalgamation (R := (Sieve.pullback f R).arrows) t
H2 :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y), Presieve.IsSeparatedFor P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows
H2' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f →
      ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y) (x : Presieve.FamilyOfElements P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows),
        x.Compatible (R := (Sieve.pullback f_1 (Sieve.pullback f S)).arrows) →
          ∃ (t : P.obj (Opposite.op Y_1)), x.IsAmalgamation (R := (Sieve.pullback f_1 (Sieve.pullback f S)).arrows) t
x : Presieve.FamilyOfElements P (Sieve.pullback f S).arrows
hx : x.Compatible (R := (Sieve.pullback f S).arrows)
y : ⦃Z : C⦄ → (g : Z ⟶ Y) → Presieve.FamilyOfElements P (Sieve.pullback (𝟙 Z) (Sieve.pullback (g ≫ f) S)).arrows :=
  fun (Z : C) (g : Z ⟶ Y) (ZZ : C) (gg : ZZ ⟶ Z) (hgg : (Sieve.pullback (𝟙 Z) (Sieve.pullback (g ≫ f) S)).arrows gg) ↦
    x (gg ≫ g) ⋯
hy : ∀ ⦃Z : C⦄ (g : Z ⟶ Y), (y g).Compatible (R := (Sieve.pullback (𝟙 Z) (Sieve.pullback (g ≫ f) S)).arrows)
z : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → (hg : (Sieve.pullback f R).arrows g) → P.obj (Opposite.op Z)
hz :
  ∀ ⦃Z : C⦄ ⦃g : Z ⟶ Y⦄ (hg : (Sieve.pullback f R).arrows g),
    (y g).IsAmalgamation (R := (Sieve.pullback (𝟙 Z) (Sieve.pullback (g ≫ f) S)).arrows) (z hg)
q : Presieve.FamilyOfElements P (Sieve.pullback f R).arrows :=
  fun (Z : C) (g : Z ⟶ Y) (hg : (Sieve.pullback f R).arrows g) ↦ z hg
hq : q.Compatible (R := (Sieve.pullback f R).arrows)
t : P.obj (Opposite.op Y)
ht : q.IsAmalgamation (R := (Sieve.pullback f R).arrows) t
Z : C
g : Z ⟶ Y
hg : (Sieve.pullback f S).arrows g
ZZ : C
gg : ZZ ⟶ Z
hgg : (Sieve.pullback (g ≫ f) R).arrows gg
⊢ q (gg ≫ g) ⋯ =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map gg.op) :
        (a : (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op Z))) → (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op ZZ)))
      (x g hg)

Tactic:
(H2 hgg (𝟙 _)).ext (fun ZZZ ggg hggg => ?_)

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Presieve.IsSeparatedFor.ext
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_3
inst : Category.{u_2, u_3} C
J : Precoverage.{u_2, u_3} C
P : Functor.{u_2, u_1, u_3, u_1 + 1} Cᵒᵖ (Type u_1)
X_1 : C
S_1 : Sieve.{u_2, u_3} X_1
X : C
R S : Sieve.{u_2, u_3} X
hS : J.Saturate X R
h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → J.Saturate Y (Sieve.pullback f S)
Y : C
f : Y ⟶ X
H :
  ∀ {X Y : C} {f : Y ⟶ X},
    ∀ R ∈ J.coverings X,
      Presieve.IsSeparatedFor P (Sieve.pullback f (Sieve.generate R)).arrows ∧
        ∀ (x : Presieve.FamilyOfElements P (Sieve.pullback f (Sieve.generate R)).arrows),
          x.Compatible (R := (Sieve.pullback f (Sieve.generate R)).arrows) →
            ∃ (t : P.obj (Opposite.op Y)), x.IsAmalgamation (R := (Sieve.pullback f (Sieve.generate R)).arrows) t
H1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X), Presieve.IsSeparatedFor P (Sieve.pullback f R).arrows
H1' :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (x : Presieve.FamilyOfElements P (Sieve.pullback f R).arrows),
    x.Compatible (R := (Sieve.pullback f R).arrows) →
      ∃ (t : P.obj (Opposite.op Y)), x.IsAmalgamation (R := (Sieve.pullback f R).arrows) t
H2 :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y), Presieve.IsSeparatedFor P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows
H2' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f →
      ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y) (x : Presieve.FamilyOfElements P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows),
        x.Compatible (R := (Sieve.pullback f_1 (Sieve.pullback f S)).arrows) →
          ∃ (t : P.obj (Opposite.op Y_1)), x.IsAmalgamation (R := (Sieve.pullback f_1 (Sieve.pullback f S)).arrows) t
x : Presieve.FamilyOfElements P (Sieve.pullback f S).arrows
hx : x.Compatible (R := (Sieve.pullback f S).arrows)
y : ⦃Z : C⦄ → (g : Z ⟶ Y) → Presieve.FamilyOfElements P (Sieve.pullback (𝟙 Z) (Sieve.pullback (g ≫ f) S)).arrows :=
  fun (Z : C) (g : Z ⟶ Y) (ZZ : C) (gg : ZZ ⟶ Z) (hgg : (Sieve.pullback (𝟙 Z) (Sieve.pullback (g ≫ f) S)).arrows gg) ↦
    x (gg ≫ g) ⋯
hy : ∀ ⦃Z : C⦄ (g : Z ⟶ Y), (y g).Compatible (R := (Sieve.pullback (𝟙 Z) (Sieve.pullback (g ≫ f) S)).arrows)
z : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → (hg : (Sieve.pullback f R).arrows g) → P.obj (Opposite.op Z)
hz :
  ∀ ⦃Z : C⦄ ⦃g : Z ⟶ Y⦄ (hg : (Sieve.pullback f R).arrows g),
    (y g).IsAmalgamation (R := (Sieve.pullback (𝟙 Z) (Sieve.pullback (g ≫ f) S)).arrows) (z hg)
q : Presieve.FamilyOfElements P (Sieve.pullback f R).arrows :=
  fun (Z : C) (g : Z ⟶ Y) (hg : (Sieve.pullback f R).arrows g) ↦ z hg
hq : q.Compatible (R := (Sieve.pullback f R).arrows)
t : P.obj (Opposite.op Y)
ht : q.IsAmalgamation (R := (Sieve.pullback f R).arrows) t
Z : C
g : Z ⟶ Y
hg : (Sieve.pullback f S).arrows g
ZZ : C
gg : ZZ ⟶ Z
hgg : (Sieve.pullback (g ≫ f) R).arrows gg
ZZZ : C
ggg : ZZZ ⟶ ZZ
hggg : (Sieve.pullback (𝟙 ZZ) (Sieve.pullback (gg ≫ g ≫ f) S)).arrows ggg
⊢ (Sieve.pullback (𝟙 ZZ) (Sieve.pullback ((gg ≫ g) ≫ f) S)).arrows ggg

Tactic:
simpa using hggg
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_3
inst : Category.{u_2, u_3} C
J : Precoverage.{u_2, u_3} C
P : Functor.{u_2, u_1, u_3, u_1 + 1} Cᵒᵖ (Type u_1)
X_1 : C
S_1 : Sieve.{u_2, u_3} X_1
X : C
R S : Sieve.{u_2, u_3} X
hS : J.Saturate X R
h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → J.Saturate Y (Sieve.pullback f S)
Y : C
f : Y ⟶ X
H :
  ∀ {X Y : C} {f : Y ⟶ X},
    ∀ R ∈ J.coverings X,
      Presieve.IsSeparatedFor P (Sieve.pullback f (Sieve.generate R)).arrows ∧
        ∀ (x : Presieve.FamilyOfElements P (Sieve.pullback f (Sieve.generate R)).arrows),
          x.Compatible (R := (Sieve.pullback f (Sieve.generate R)).arrows) →
            ∃ (t : P.obj (Opposite.op Y)), x.IsAmalgamation (R := (Sieve.pullback f (Sieve.generate R)).arrows) t
H1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X), Presieve.IsSeparatedFor P (Sieve.pullback f R).arrows
H1' :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (x : Presieve.FamilyOfElements P (Sieve.pullback f R).arrows),
    x.Compatible (R := (Sieve.pullback f R).arrows) →
      ∃ (t : P.obj (Opposite.op Y)), x.IsAmalgamation (R := (Sieve.pullback f R).arrows) t
H2 :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y), Presieve.IsSeparatedFor P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows
H2' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f →
      ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y) (x : Presieve.FamilyOfElements P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows),
        x.Compatible (R := (Sieve.pullback f_1 (Sieve.pullback f S)).arrows) →
          ∃ (t : P.obj (Opposite.op Y_1)), x.IsAmalgamation (R := (Sieve.pullback f_1 (Sieve.pullback f S)).arrows) t
x : Presieve.FamilyOfElements P (Sieve.pullback f S).arrows
hx : x.Compatible (R := (Sieve.pullback f S).arrows)
y : ⦃Z : C⦄ → (g : Z ⟶ Y) → Presieve.FamilyOfElements P (Sieve.pullback (𝟙 Z) (Sieve.pullback (g ≫ f) S)).arrows :=
  fun (Z : C) (g : Z ⟶ Y) (ZZ : C) (gg : ZZ ⟶ Z) (hgg : (Sieve.pullback (𝟙 Z) (Sieve.pullback (g ≫ f) S)).arrows gg) ↦
    x (gg ≫ g) ⋯
hy : ∀ ⦃Z : C⦄ (g : Z ⟶ Y), (y g).Compatible (R := (Sieve.pullback (𝟙 Z) (Sieve.pullback (g ≫ f) S)).arrows)
z : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → (hg : (Sieve.pullback f R).arrows g) → P.obj (Opposite.op Z)
hz :
  ∀ ⦃Z : C⦄ ⦃g : Z ⟶ Y⦄ (hg : (Sieve.pullback f R).arrows g),
    (y g).IsAmalgamation (R := (Sieve.pullback (𝟙 Z) (Sieve.pullback (g ≫ f) S)).arrows) (z hg)
q : Presieve.FamilyOfElements P (Sieve.pullback f R).arrows :=
  fun (Z : C) (g : Z ⟶ Y) (hg : (Sieve.pullback f R).arrows g) ↦ z hg
hq : q.Compatible (R := (Sieve.pullback f R).arrows)
t : P.obj (Opposite.op Y)
ht : q.IsAmalgamation (R := (Sieve.pullback f R).arrows) t
Z : C
g : Z ⟶ Y
hg : (Sieve.pullback f S).arrows g
ZZ : C
gg : ZZ ⟶ Z
hgg : (Sieve.pullback (g ≫ f) R).arrows gg
ZZZ : C
ggg : ZZZ ⟶ ZZ
hggg : (Sieve.pullback (𝟙 ZZ) (Sieve.pullback (gg ≫ g ≫ f) S)).arrows ggg
⊢ (Sieve.pullback (𝟙 ZZ) (Sieve.pullback ((gg ≫ g) ≫ f) S)).arrows ggg

Tactic:
on_goal 2 => simpa using hggg
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_3
inst : Category.{u_2, u_3} C
J : Precoverage.{u_2, u_3} C
P : Functor.{u_2, u_1, u_3, u_1 + 1} Cᵒᵖ (Type u_1)
X_1 : C
S_1 : Sieve.{u_2, u_3} X_1
X : C
R S : Sieve.{u_2, u_3} X
hS : J.Saturate X R
h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → J.Saturate Y (Sieve.pullback f S)
Y : C
f : Y ⟶ X
H :
  ∀ {X Y : C} {f : Y ⟶ X},
    ∀ R ∈ J.coverings X,
      Presieve.IsSeparatedFor P (Sieve.pullback f (Sieve.generate R)).arrows ∧
        ∀ (x : Presieve.FamilyOfElements P (Sieve.pullback f (Sieve.generate R)).arrows),
          x.Compatible (R := (Sieve.pullback f (Sieve.generate R)).arrows) →
            ∃ (t : P.obj (Opposite.op Y)), x.IsAmalgamation (R := (Sieve.pullback f (Sieve.generate R)).arrows) t
H1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X), Presieve.IsSeparatedFor P (Sieve.pullback f R).arrows
H1' :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (x : Presieve.FamilyOfElements P (Sieve.pullback f R).arrows),
    x.Compatible (R := (Sieve.pullback f R).arrows) →
      ∃ (t : P.obj (Opposite.op Y)), x.IsAmalgamation (R := (Sieve.pullback f R).arrows) t
H2 :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y), Presieve.IsSeparatedFor P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows
H2' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f →
      ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y) (x : Presieve.FamilyOfElements P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows),
        x.Compatible (R := (Sieve.pullback f_1 (Sieve.pullback f S)).arrows) →
          ∃ (t : P.obj (Opposite.op Y_1)), x.IsAmalgamation (R := (Sieve.pullback f_1 (Sieve.pullback f S)).arrows) t
x : Presieve.FamilyOfElements P (Sieve.pullback f S).arrows
hx : x.Compatible (R := (Sieve.pullback f S).arrows)
y : ⦃Z : C⦄ → (g : Z ⟶ Y) → Presieve.FamilyOfElements P (Sieve.pullback (𝟙 Z) (Sieve.pullback (g ≫ f) S)).arrows :=
  fun (Z : C) (g : Z ⟶ Y) (ZZ : C) (gg : ZZ ⟶ Z) (hgg : (Sieve.pullback (𝟙 Z) (Sieve.pullback (g ≫ f) S)).arrows gg) ↦
    x (gg ≫ g) ⋯
hy : ∀ ⦃Z : C⦄ (g : Z ⟶ Y), (y g).Compatible (R := (Sieve.pullback (𝟙 Z) (Sieve.pullback (g ≫ f) S)).arrows)
z : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → (hg : (Sieve.pullback f R).arrows g) → P.obj (Opposite.op Z)
hz :
  ∀ ⦃Z : C⦄ ⦃g : Z ⟶ Y⦄ (hg : (Sieve.pullback f R).arrows g),
    (y g).IsAmalgamation (R := (Sieve.pullback (𝟙 Z) (Sieve.pullback (g ≫ f) S)).arrows) (z hg)
q : Presieve.FamilyOfElements P (Sieve.pullback f R).arrows :=
  fun (Z : C) (g : Z ⟶ Y) (hg : (Sieve.pullback f R).arrows g) ↦ z hg
hq : q.Compatible (R := (Sieve.pullback f R).arrows)
t : P.obj (Opposite.op Y)
ht : q.IsAmalgamation (R := (Sieve.pullback f R).arrows) t
Z : C
g : Z ⟶ Y
hg : (Sieve.pullback f S).arrows g
ZZ : C
gg : ZZ ⟶ Z
hgg : (Sieve.pullback (g ≫ f) R).arrows gg
ZZZ : C
ggg : ZZZ ⟶ ZZ
hggg : (Sieve.pullback (𝟙 ZZ) (Sieve.pullback (gg ≫ g ≫ f) S)).arrows ggg
⊢ y (gg ≫ g) ggg ⋯ =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (ggg ≫ gg).op) :
        (a : (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op Z))) → P.obj (Opposite.op ZZZ))
      (x g hg)

Tactic:
(H2 hgg ggg).ext (fun ZZZZ gggg _ => ?_)

Premises used: CategoryTheory.Presieve.IsSeparatedFor.ext
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_3
inst : Category.{u_2, u_3} C
J : Precoverage.{u_2, u_3} C
P : Functor.{u_2, u_1, u_3, u_1 + 1} Cᵒᵖ (Type u_1)
X_1 : C
S_1 : Sieve.{u_2, u_3} X_1
X : C
R S : Sieve.{u_2, u_3} X
hS : J.Saturate X R
h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → J.Saturate Y (Sieve.pullback f S)
Y : C
f : Y ⟶ X
H :
  ∀ {X Y : C} {f : Y ⟶ X},
    ∀ R ∈ J.coverings X,
      Presieve.IsSeparatedFor P (Sieve.pullback f (Sieve.generate R)).arrows ∧
        ∀ (x : Presieve.FamilyOfElements P (Sieve.pullback f (Sieve.generate R)).arrows),
          x.Compatible (R := (Sieve.pullback f (Sieve.generate R)).arrows) →
            ∃ (t : P.obj (Opposite.op Y)), x.IsAmalgamation (R := (Sieve.pullback f (Sieve.generate R)).arrows) t
H1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X), Presieve.IsSeparatedFor P (Sieve.pullback f R).arrows
H1' :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (x : Presieve.FamilyOfElements P (Sieve.pullback f R).arrows),
    x.Compatible (R := (Sieve.pullback f R).arrows) →
      ∃ (t : P.obj (Opposite.op Y)), x.IsAmalgamation (R := (Sieve.pullback f R).arrows) t
H2 :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y), Presieve.IsSeparatedFor P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows
H2' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f →
      ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y) (x : Presieve.FamilyOfElements P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows),
        x.Compatible (R := (Sieve.pullback f_1 (Sieve.pullback f S)).arrows) →
          ∃ (t : P.obj (Opposite.op Y_1)), x.IsAmalgamation (R := (Sieve.pullback f_1 (Sieve.pullback f S)).arrows) t
x : Presieve.FamilyOfElements P (Sieve.pullback f S).arrows
hx : x.Compatible (R := (Sieve.pullback f S).arrows)
y : ⦃Z : C⦄ → (g : Z ⟶ Y) → Presieve.FamilyOfElements P (Sieve.pullback (𝟙 Z) (Sieve.pullback (g ≫ f) S)).arrows :=
  fun (Z : C) (g : Z ⟶ Y) (ZZ : C) (gg : ZZ ⟶ Z) (hgg : (Sieve.pullback (𝟙 Z) (Sieve.pullback (g ≫ f) S)).arrows gg) ↦
    x (gg ≫ g) ⋯
hy : ∀ ⦃Z : C⦄ (g : Z ⟶ Y), (y g).Compatible (R := (Sieve.pullback (𝟙 Z) (Sieve.pullback (g ≫ f) S)).arrows)
z : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → (hg : (Sieve.pullback f R).arrows g) → P.obj (Opposite.op Z)
hz :
  ∀ ⦃Z : C⦄ ⦃g : Z ⟶ Y⦄ (hg : (Sieve.pullback f R).arrows g),
    (y g).IsAmalgamation (R := (Sieve.pullback (𝟙 Z) (Sieve.pullback (g ≫ f) S)).arrows) (z hg)
q : Presieve.FamilyOfElements P (Sieve.pullback f R).arrows :=
  fun (Z : C) (g : Z ⟶ Y) (hg : (Sieve.pullback f R).arrows g) ↦ z hg
hq : q.Compatible (R := (Sieve.pullback f R).arrows)
t : P.obj (Opposite.op Y)
ht : q.IsAmalgamation (R := (Sieve.pullback f R).arrows) t
Z : C
g : Z ⟶ Y
hg : (Sieve.pullback f S).arrows g
ZZ : C
gg : ZZ ⟶ Z
hgg : (Sieve.pullback (g ≫ f) R).arrows gg
ZZZ : C
ggg : ZZZ ⟶ ZZ
hggg : (Sieve.pullback (𝟙 ZZ) (Sieve.pullback (gg ≫ g ≫ f) S)).arrows ggg
ZZZZ : C
gggg : ZZZZ ⟶ ZZZ
h_1 : (Sieve.pullback ggg (Sieve.pullback (gg ≫ g ≫ f) S)).arrows gggg
⊢ gggg ≫ ggg ≫ gg ≫ g = (gggg ≫ ggg ≫ gg) ≫ g

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_2
inst : Category.{u_1, u_2} C
J : Precoverage.{u_1, u_2} C
inst_1 : J.IsStableUnderComposition
inst_2 : J.IsStableUnderBaseChange
inst_3 : J.HasPullbacks
inst_4 : J.HasIsos
X : C
S : Sieve.{u_1, u_2} X
⊢ S ∈ (J.toGrothendieck : (a : C) → Set (Sieve a)) X ↔ ∃ R ∈ J.coverings X, R ≤ S.arrows

Tactic:
⟨fun hS ↦ ?_, fun ⟨R, hR, hle⟩ ↦ ?_⟩

Premises used: _private.0.CategoryTheory.Precoverage.mem_toGrothendieck_iff_of_isStableUnderComposition.match_1, Membership.mem, Iff.intro, CategoryTheory.Precoverage.toGrothendieck, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_2
inst : Category.{u_1, u_2} C
J : Precoverage.{u_1, u_2} C
inst_1 : J.IsStableUnderComposition
inst_2 : J.IsStableUnderBaseChange
inst_3 : J.HasPullbacks
inst_4 : J.HasIsos
X : C
S : Sieve.{u_1, u_2} X
refine_1 : ∀ (hS : S ∈ (J.toGrothendieck : (a : C) → Set (Sieve a)) X), ∃ R ∈ J.coverings X, R ≤ S.arrows
refine_2 :
  (∃ R ∈ J.coverings X, R ≤ S.arrows) →
    ∀ (R : Presieve.{u_1, u_2} X) (hR : R ∈ J.coverings X) (hle : R ≤ S.arrows),
      S ∈ (J.toGrothendieck : (a : C) → Set (Sieve a)) X
⊢ S ∈ (J.toGrothendieck : (a : C) → Set (Sieve a)) X ↔ ∃ R ∈ J.coverings X, R ≤ S.arrows

Tactic:
refine ⟨fun hS ↦ ?_, fun ⟨R, hR, hle⟩ ↦ ?_⟩
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_2
inst : Category.{u_1, u_2} C
J : Precoverage.{u_1, u_2} C
inst_1 : J.IsStableUnderComposition
inst_2 : J.IsStableUnderBaseChange
inst_3 : J.HasPullbacks
inst_4 : J.HasIsos
X_1 : C
S : Sieve.{u_1, u_2} X_1
X : C
R : Presieve.{u_1, u_2} X
hR : R ∈ J.coverings X
right : R ≤ (Sieve.generate R).arrows
⊢ ∃ R_1 ∈ J.coverings X, R_1 ≤ (Sieve.generate R).arrows

Tactic:
use R, hR
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_2
inst : Category.{u_1, u_2} C
J : Precoverage.{u_1, u_2} C
inst_1 : J.IsStableUnderComposition
inst_2 : J.IsStableUnderBaseChange
inst_3 : J.HasPullbacks
inst_4 : J.HasIsos
X_1 : C
S : Sieve.{u_1, u_2} X_1
X : C
R : Presieve.{u_1, u_2} X
hR : R ∈ J.coverings X
⊢ R ≤ (Sieve.generate R).arrows

Tactic:
Sieve.le_generate R

Premises used: CategoryTheory.Sieve.le_generate
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_2
inst : Category.{u_1, u_2} C
J : Precoverage.{u_1, u_2} C
inst_1 : J.IsStableUnderComposition
inst_2 : J.IsStableUnderBaseChange
inst_3 : J.HasPullbacks
inst_4 : J.HasIsos
X_1 : C
S : Sieve.{u_1, u_2} X_1
X : C
R : Presieve.{u_1, u_2} X
hR : R ∈ J.coverings X
⊢ R ≤ (Sieve.generate R).arrows

Tactic:
exact Sieve.le_generate R

Premises used: CategoryTheory.Sieve.le_generate
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_2
inst : Category.{u_1, u_2} C
J : Precoverage.{u_1, u_2} C
inst_1 : J.IsStableUnderComposition
inst_2 : J.IsStableUnderBaseChange
inst_3 : J.HasPullbacks
inst_4 : J.HasIsos
X_1 : C
S : Sieve.{u_1, u_2} X_1
X : C
⊢ LE.le (α := Presieve.{u_1, u_2} X) (Presieve.singleton (𝟙 X)) (Sieve.arrows ⊤)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_2
inst : Category.{u_1, u_2} C
J : Precoverage.{u_1, u_2} C
inst_1 : J.IsStableUnderComposition
inst_2 : J.IsStableUnderBaseChange
inst_3 : J.HasPullbacks
inst_4 : J.HasIsos
X_1 : C
S : Sieve.{u_1, u_2} X_1
X : C
⊢ ∃ R ∈ J.coverings X, R ≤ Sieve.arrows ⊤

Tactic:
exact ⟨Presieve.singleton (𝟙 X), mem_coverings_of_isIso (𝟙 X), by simp⟩