awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck (goal)
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
t₁ t₂ : P.obj (Opposite.op Y)
h₁ : x.IsAmalgamation (R := (Sieve.pullback f S).arrows) t₁
h₂ : x.IsAmalgamation (R := (Sieve.pullback f S).arrows) t₂
Z : C
g : Z ⟶ Y
hg : (Sieve.pullback f R).arrows g
ZZ : C
gg : ZZ ⟶ Z
hgg : S.arrows (gg ≫ g ≫ f)
⊢ Eq (α := P.obj (Opposite.op ZZ))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map g.op ≫ P.map gg.op) :
          (a : P.obj (Opposite.op Y)) → P.obj (Opposite.op ZZ))
        t₁ :
      P.obj (Opposite.op ZZ))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map g.op ≫ P.map gg.op) :
          (a : P.obj (Opposite.op Y)) → P.obj (Opposite.op ZZ))
        t₂ :
      P.obj (Opposite.op ZZ))
have mpr : (Sieve.pullback f S).arrows (gg ≫ g)
Tactic: rw [← P.map_comp, ← op_comp, h₁, h₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck (goal)
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_1 : ∀ ⦃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) ⋯
Z : C
g : Z ⟶ Y
Y₁ Y₂ ZZ : C
g₁ : ZZ ⟶ Y₁
g₂ : ZZ ⟶ Y₂
f₁ : Y₁ ⟶ Z
f₂ : Y₂ ⟶ Z
h₁ : (Sieve.pullback (𝟙 Z) (Sieve.pullback (g ≫ f) S)).arrows f₁
h₂ : (Sieve.pullback (𝟙 Z) (Sieve.pullback (g ≫ f) S)).arrows f₂
h : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ Eq (α := (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op ZZ)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map g₁.op) :
          (a : (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op Y₁))) → (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op ZZ)))
        (y g f₁ h₁) :
      (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op ZZ)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map g₂.op) :
          (a : (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op Y₂))) → (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op ZZ)))
        (y g f₂ h₂) :
      (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op ZZ)))
have a : g₁ ≫ f₁ ≫ g = g₂ ≫ f₂ ≫ g
Tactic: rw [hx]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck (goal)
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_1 : ∀ ⦃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) ⋯
Z : C
g : Z ⟶ Y
Y₁ Y₂ ZZ : C
g₁ : ZZ ⟶ Y₁
g₂ : ZZ ⟶ Y₂
f₁ : Y₁ ⟶ Z
f₂ : Y₂ ⟶ Z
h₁ : (Sieve.pullback (𝟙 Z) (Sieve.pullback (g ≫ f) S)).arrows f₁
h₂ : (Sieve.pullback (𝟙 Z) (Sieve.pullback (g ≫ f) S)).arrows f₂
h : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ g₁ ≫ f₁ ≫ g = g₂ ≫ f₂ ≫ g
have a : g₂ ≫ f₂ ≫ g = g₂ ≫ f₂ ≫ g
Tactic: rw [reassoc_of% h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck (hypothesis)
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) ⋯
⊢ ∃ (t : P.obj (Opposite.op Y)), x.IsAmalgamation (R := (Sieve.pullback f S).arrows) t
have hy : ∀ ⦃Z : C⦄ (g : Z ⟶ Y), (y g).Compatible (R := (Sieve.pullback (𝟙 Z) (Sieve.pullback (g ≫ f) S)).arrows)
Tactic: have hy : ∀ ⦃Z : C⦄ (g : Z ⟶ Y), (y g).Compatible := by
        intro Z g Y₁ Y₂ ZZ g₁ g₂ f₁ f₂ h₁ h₂ h
        rw [hx]
        rw [reassoc_of% h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck (goal)
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)
⊢ ∃ (t : P.obj (Opposite.op Y)), x.IsAmalgamation (R := (Sieve.pullback f S).arrows) t
have mpr : ∀ (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)),
  ∃ (t : P.obj (Opposite.op Y)), x.IsAmalgamation (R := (Sieve.pullback f S).arrows) t
Tactic: choose z hz using fun ⦃Z : C⦄ ⦃g : Z ⟶ Y⦄ (hg : R.pullback f g) =>
        H2' hg (𝟙 _) (y g) (hy g)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck (goal)
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_1 : ∀ ⦃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
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ Y
f₂ : Y₂ ⟶ Y
h₁ : (Sieve.pullback f R).arrows f₁
h₂ : (Sieve.pullback f R).arrows f₂
h : g₁ ≫ f₁ = g₂ ≫ f₂
ZZ : C
gg : ZZ ⟶ Z
hgg : (Sieve.pullback g₁ (Sieve.pullback (f₁ ≫ f) S)).arrows gg
⊢ x ((gg ≫ g₁) ≫ f₁) ⋯ = x ((gg ≫ g₂) ≫ f₂) ⋯
have e_f : (gg ≫ g₁) ≫ f₁ = (gg ≫ g₂) ≫ f₂
Tactic: congr 1
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck (hypothesis)
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
⊢ ∃ (t : P.obj (Opposite.op Y)), x.IsAmalgamation (R := (Sieve.pullback f S).arrows) t
have hq : q.Compatible (R := (Sieve.pullback f R).arrows)
Tactic: have hq : q.Compatible := by
        intro Y₁ Y₂ Z g₁ g₂ f₁ f₂ h₁ h₂ h
        apply (H2 h₁ g₁).ext
        intro ZZ gg hgg
        simp only [← comp_apply]
        rw [← P.map_comp, ← P.map_comp, ← op_comp, ← op_comp, hz, hz]
        · dsimp [y]; congr 1; simp only [Category.assoc, h]
        · simpa [reassoc_of% h] using hgg
        · simpa using hgg
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck (goal)
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)), x.IsAmalgamation (R := (Sieve.pullback f S).arrows) t
have mpr : ∀ (t : P.obj (Opposite.op Y)) (ht : q.IsAmalgamation (R := (Sieve.pullback f R).arrows) t),
  ∃ (t : P.obj (Opposite.op Y)), x.IsAmalgamation (R := (Sieve.pullback f S).arrows) t
Tactic: obtain ⟨t, ht⟩ := H1' f q hq
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck (goal)
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
⊢ ∃ (t : P.obj (Opposite.op Y)), x.IsAmalgamation (R := (Sieve.pullback f S).arrows) t
have mpr : ∀ (Z : C) (g : Z ⟶ Y) (hg : (Sieve.pullback f S).arrows g),
  (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map g.op) :
        (a : (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op Y))) → (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op Z)))
      t =
    x g hg
Tactic: refine ⟨t, fun Z g hg => ?_⟩