awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_2
inst : Category.{v_1, u_2} C
X : C
S T : Presieve.{v_1, u_2} X
P : Functor.{v_1, u_1, u_2, u_1 + 1} Cᵒᵖ (Type u_1)
h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, T f → ∃ (R : Presieve.{v_1, u_2} Y), IsSeparatedFor P R ∧ R.FactorsThruAlong S f
hS :
  IsSeparatedFor P S ∧
    ∀ (x : FamilyOfElements P S), x.Compatible (R := S) → ∃ (t : P.obj (Opposite.op X)), x.IsAmalgamation (R := S) t
W : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → S g → C
i : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → (a : S g) → Z ⟶ W a
e : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → (a : S g) → W a ⟶ X
h1 : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ X⦄ (a : S g), T (e a)
h2 : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ X⦄ (a : S g), i a ≫ e a = g
x : FamilyOfElements P T
hx : x.Compatible (R := T)
y : FamilyOfElements P S :=
  fun (Y : C) (g : Y ⟶ X) (hg : S g) ↦
    (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (i hg).op) :
        (a : (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op (W hg)))) → (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op Y)))
      (x (e hg) ⋯)
hy : y.Compatible (R := S)
left : IsSeparatedFor P S
h2' : ∀ (x : FamilyOfElements P S), x.Compatible (R := S) → ∃ (t : P.obj (Opposite.op X)), x.IsAmalgamation (R := S) t
z : P.obj (Opposite.op X)
hz : y.IsAmalgamation (R := S) z
refine_2 :
  ∀ (Y : C) (g : Y ⟶ X) (hg : T g),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map g.op) :
          (a : (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op X))) → (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op Y)))
        z =
      x g hg
⊢ ∃ (t : P.obj (Opposite.op X)), x.IsAmalgamation (R := T) t

Tactic:
refine ⟨z, fun Y g hg => ?_⟩
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_2
inst : Category.{v_1, u_2} C
X : C
S T : Presieve.{v_1, u_2} X
P : Functor.{v_1, u_1, u_2, u_1 + 1} Cᵒᵖ (Type u_1)
h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, T f → ∃ (R : Presieve.{v_1, u_2} Y), IsSeparatedFor P R ∧ R.FactorsThruAlong S f
hS :
  IsSeparatedFor P S ∧
    ∀ (x : FamilyOfElements P S), x.Compatible (R := S) → ∃ (t : P.obj (Opposite.op X)), x.IsAmalgamation (R := S) t
W : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → S g → C
i : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → (a : S g) → Z ⟶ W a
e : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → (a : S g) → W a ⟶ X
h1 : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ X⦄ (a : S g), T (e a)
h2 : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ X⦄ (a : S g), i a ≫ e a = g
x : FamilyOfElements P T
hx : x.Compatible (R := T)
y : FamilyOfElements P S :=
  fun (Y : C) (g : Y ⟶ X) (hg : S g) ↦
    (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (i hg).op) :
        (a : (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op (W hg)))) → (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op Y)))
      (x (e hg) ⋯)
hy : y.Compatible (R := S)
left : IsSeparatedFor P S
h2' : ∀ (x : FamilyOfElements P S), x.Compatible (R := S) → ∃ (t : P.obj (Opposite.op X)), x.IsAmalgamation (R := S) t
z : P.obj (Opposite.op X)
hz : y.IsAmalgamation (R := S) z
Y : C
g : Y ⟶ X
hg : T g
refine_2 :
  ∀ (R : Presieve.{v_1, u_2} Y) (hR1 : IsSeparatedFor P R) (hR2 : R.FactorsThruAlong S g),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map g.op) :
          (a : (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op X))) → (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op Y)))
        z =
      x g hg
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map g.op) :
        (a : (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op X))) → (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op Y)))
      z =
    x g hg

Tactic:
obtain ⟨R, hR1, hR2⟩ := h hg
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_2
inst : Category.{v_1, u_2} C
X : C
S T : Presieve.{v_1, u_2} X
P : Functor.{v_1, u_1, u_2, u_1 + 1} Cᵒᵖ (Type u_1)
h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, T f → ∃ (R : Presieve.{v_1, u_2} Y), IsSeparatedFor P R ∧ R.FactorsThruAlong S f
hS :
  IsSeparatedFor P S ∧
    ∀ (x : FamilyOfElements P S), x.Compatible (R := S) → ∃ (t : P.obj (Opposite.op X)), x.IsAmalgamation (R := S) t
W : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → S g → C
i : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → (a : S g) → Z ⟶ W a
e : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → (a : S g) → W a ⟶ X
h1 : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ X⦄ (a : S g), T (e a)
h2 : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ X⦄ (a : S g), i a ≫ e a = g
x : FamilyOfElements P T
hx : x.Compatible (R := T)
y : FamilyOfElements P S :=
  fun (Y : C) (g : Y ⟶ X) (hg : S g) ↦
    (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (i hg).op) :
        (a : (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op (W hg)))) → (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op Y)))
      (x (e hg) ⋯)
hy : y.Compatible (R := S)
left : IsSeparatedFor P S
h2' : ∀ (x : FamilyOfElements P S), x.Compatible (R := S) → ∃ (t : P.obj (Opposite.op X)), x.IsAmalgamation (R := S) t
z : P.obj (Opposite.op X)
hz : y.IsAmalgamation (R := S) z
Y : C
g : Y ⟶ X
hg : T g
R : Presieve.{v_1, u_2} Y
hR1 : IsSeparatedFor P R
hR2 : R.FactorsThruAlong S g
refine_2 :
  ∀ (WW : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → R g → C) (ii : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → (a : R g) → Z ⟶ WW a)
    (ee : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → (a : R g) → WW a ⟶ X) (hh1 : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ Y⦄ (a : R g), S (ee a))
    (hh2 : ∀ ⦃Z : C⦄ ⦃g_1 : Z ⟶ Y⦄ (a : R g_1), ii a ≫ ee a = g_1 ≫ g),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map g.op) :
          (a : (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op X))) → (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op Y)))
        z =
      x g hg
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map g.op) :
        (a : (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op X))) → (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op Y)))
      z =
    x g hg

Tactic:
choose WW ii ee hh1 hh2 using hR2
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_2
inst : Category.{v_1, u_2} C
X : C
S T : Presieve.{v_1, u_2} X
P : Functor.{v_1, u_1, u_2, u_1 + 1} Cᵒᵖ (Type u_1)
h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, T f → ∃ (R : Presieve.{v_1, u_2} Y), IsSeparatedFor P R ∧ R.FactorsThruAlong S f
hS :
  IsSeparatedFor P S ∧
    ∀ (x : FamilyOfElements P S), x.Compatible (R := S) → ∃ (t : P.obj (Opposite.op X)), x.IsAmalgamation (R := S) t
W : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → S g → C
i : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → (a : S g) → Z ⟶ W a
e : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → (a : S g) → W a ⟶ X
h1 : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ X⦄ (a : S g), T (e a)
h2 : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ X⦄ (a : S g), i a ≫ e a = g
x : FamilyOfElements P T
hx : x.Compatible (R := T)
y : FamilyOfElements P S :=
  fun (Y : C) (g : Y ⟶ X) (hg : S g) ↦
    (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (i hg).op) :
        (a : (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op (W hg)))) → (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op Y)))
      (x (e hg) ⋯)
hy : y.Compatible (R := S)
left : IsSeparatedFor P S
h2' : ∀ (x : FamilyOfElements P S), x.Compatible (R := S) → ∃ (t : P.obj (Opposite.op X)), x.IsAmalgamation (R := S) t
z : P.obj (Opposite.op X)
hz : y.IsAmalgamation (R := S) z
Y : C
g : Y ⟶ X
hg : T g
R : Presieve.{v_1, u_2} Y
hR1 : IsSeparatedFor P R
WW : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → R g → C
ii : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → (a : R g) → Z ⟶ WW a
ee : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → (a : R g) → WW a ⟶ X
hh1 : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ Y⦄ (a : R g), S (ee a)
hh2 : ∀ ⦃Z : C⦄ ⦃g_1 : Z ⟶ Y⦄ (a : R g_1), ii a ≫ ee a = g_1 ≫ g
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map g.op) :
        (a : (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op X))) → (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op Y)))
      z =
    x g hg

Tactic:
hR1.ext (fun Q t ht => ?_)

Premises used: CategoryTheory.Presieve.IsSeparatedFor.ext
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_2
inst : Category.{v_1, u_2} C
X : C
S T : Presieve.{v_1, u_2} X
P : Functor.{v_1, u_1, u_2, u_1 + 1} Cᵒᵖ (Type u_1)
h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, T f → ∃ (R : Presieve.{v_1, u_2} Y), IsSeparatedFor P R ∧ R.FactorsThruAlong S f
hS :
  IsSeparatedFor P S ∧
    ∀ (x : FamilyOfElements P S), x.Compatible (R := S) → ∃ (t : P.obj (Opposite.op X)), x.IsAmalgamation (R := S) t
W : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → S g → C
i : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → (a : S g) → Z ⟶ W a
e : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → (a : S g) → W a ⟶ X
h1 : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ X⦄ (a : S g), T (e a)
h2 : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ X⦄ (a : S g), i a ≫ e a = g
x : FamilyOfElements P T
hx : x.Compatible (R := T)
y : FamilyOfElements P S :=
  fun (Y : C) (g : Y ⟶ X) (hg : S g) ↦
    (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (i hg).op) :
        (a : (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op (W hg)))) → (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op Y)))
      (x (e hg) ⋯)
hy : y.Compatible (R := S)
left : IsSeparatedFor P S
h2' : ∀ (x : FamilyOfElements P S), x.Compatible (R := S) → ∃ (t : P.obj (Opposite.op X)), x.IsAmalgamation (R := S) t
z : P.obj (Opposite.op X)
hz : y.IsAmalgamation (R := S) z
Y : C
g : Y ⟶ X
hg : T g
R : Presieve.{v_1, u_2} Y
hR1 : IsSeparatedFor P R
WW : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → R g → C
ii : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → (a : R g) → Z ⟶ WW a
ee : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → (a : R g) → WW a ⟶ X
hh1 : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ Y⦄ (a : R g), S (ee a)
hh2 : ∀ ⦃Z : C⦄ ⦃g_1 : Z ⟶ Y⦄ (a : R g_1), ii a ≫ ee a = g_1 ≫ g
refine_2 :
  ∀ (Q : C) (t : Q ⟶ Y) (ht : R t),
    Eq (α := (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op Q)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map t.op) :
            (a : (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op Y))) → (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op Q)))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map g.op) :
                (a : (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op X))) →
                  (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op Y)))
              z :
            (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op Y))) :
        (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op Q)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map t.op) :
            (a : (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op Y))) → (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op Q)))
          (x g hg) :
        (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op Q)))
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map g.op) :
        (a : (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op X))) → (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op Y)))
      z =
    x g hg

Tactic:
refine hR1.ext (fun Q t ht => ?_)

Premises used: CategoryTheory.Presieve.IsSeparatedFor.ext
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_2
inst : Category.{v_1, u_2} C
X : C
S T : Presieve.{v_1, u_2} X
P : Functor.{v_1, u_1, u_2, u_1 + 1} Cᵒᵖ (Type u_1)
h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, T f → ∃ (R : Presieve.{v_1, u_2} Y), IsSeparatedFor P R ∧ R.FactorsThruAlong S f
hS :
  IsSeparatedFor P S ∧
    ∀ (x : FamilyOfElements P S), x.Compatible (R := S) → ∃ (t : P.obj (Opposite.op X)), x.IsAmalgamation (R := S) t
W : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → S g → C
i : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → (a : S g) → Z ⟶ W a
e : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → (a : S g) → W a ⟶ X
h1 : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ X⦄ (a : S g), T (e a)
h2 : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ X⦄ (a : S g), i a ≫ e a = g
x : FamilyOfElements P T
hx : x.Compatible (R := T)
y : FamilyOfElements P S :=
  fun (Y : C) (g : Y ⟶ X) (hg : S g) ↦
    (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (i hg).op) :
        (a : (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op (W hg)))) → (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op Y)))
      (x (e hg) ⋯)
hy : y.Compatible (R := S)
left : IsSeparatedFor P S
h2' : ∀ (x : FamilyOfElements P S), x.Compatible (R := S) → ∃ (t : P.obj (Opposite.op X)), x.IsAmalgamation (R := S) t
z : P.obj (Opposite.op X)
hz : y.IsAmalgamation (R := S) z
Y : C
g : Y ⟶ X
hg : T g
R : Presieve.{v_1, u_2} Y
hR1 : IsSeparatedFor P R
WW : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → R g → C
ii : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → (a : R g) → Z ⟶ WW a
ee : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → (a : R g) → WW a ⟶ X
hh1 : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ Y⦄ (a : R g), S (ee a)
hh2 : ∀ ⦃Z : C⦄ ⦃g_1 : Z ⟶ Y⦄ (a : R g_1), ii a ≫ ee a = g_1 ≫ g
Q : C
t : Q ⟶ Y
ht : R t
refine_2 : (ii ht ≫ i ⋯) ≫ e ⋯ = t ≫ g
⊢ Eq (α := (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op Q)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (ii ht ≫ i ⋯).op) :
          (a : (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op (W ⋯)))) → (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op Q)))
        (x (e ⋯) ⋯) :
      (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op Q)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map t.op) :
          (a : (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op Y))) → (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op Q)))
        (x g hg) :
      (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op Q)))

Tactic:
apply hx
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_2
inst : Category.{v_1, u_2} C
X : C
S T : Presieve.{v_1, u_2} X
P : Functor.{v_1, u_1, u_2, u_1 + 1} Cᵒᵖ (Type u_1)
h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, T f → ∃ (R : Presieve.{v_1, u_2} Y), IsSeparatedFor P R ∧ R.FactorsThruAlong S f
hS :
  IsSeparatedFor P S ∧
    ∀ (x : FamilyOfElements P S), x.Compatible (R := S) → ∃ (t : P.obj (Opposite.op X)), x.IsAmalgamation (R := S) t
W : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → S g → C
i : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → (a : S g) → Z ⟶ W a
e : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → (a : S g) → W a ⟶ X
h1 : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ X⦄ (a : S g), T (e a)
h2 : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ X⦄ (a : S g), i a ≫ e a = g
x : FamilyOfElements P T
hx : x.Compatible (R := T)
y : FamilyOfElements P S :=
  fun (Y : C) (g : Y ⟶ X) (hg : S g) ↦
    (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (i hg).op) :
        (a : (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op (W hg)))) → (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op Y)))
      (x (e hg) ⋯)
hy : y.Compatible (R := S)
left : IsSeparatedFor P S
h2' : ∀ (x : FamilyOfElements P S), x.Compatible (R := S) → ∃ (t : P.obj (Opposite.op X)), x.IsAmalgamation (R := S) t
z : P.obj (Opposite.op X)
hz : y.IsAmalgamation (R := S) z
Y : C
g : Y ⟶ X
hg : T g
R : Presieve.{v_1, u_2} Y
hR1 : IsSeparatedFor P R
WW : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → R g → C
ii : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → (a : R g) → Z ⟶ WW a
ee : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → (a : R g) → WW a ⟶ X
hh1 : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ Y⦄ (a : R g), S (ee a)
hh2 : ∀ ⦃Z : C⦄ ⦃g_1 : Z ⟶ Y⦄ (a : R g_1), ii a ≫ ee a = g_1 ≫ g
Q : C
t : Q ⟶ Y
ht : R t
⊢ (ii ht ≫ i ⋯) ≫ e ⋯ = t ≫ g

Tactic:
simp only [Category.assoc, h2, hh2]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_1
D : Type ?u.31285
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, ?u.31285} D
J : GrothendieckTopology.{v_1, u_1} C
X Y : C
f : Y ⟶ X
S : Presieve.{v_1, u_1} X
S₁ :
  ∀ (hS : Sieve.generate S ∈ (J : (a : C) → Set (Sieve a)) X),
    ∃ (T : Presieve.{v_1, u_1} Y),
      Membership.mem (γ := Set (Presieve.{v_1, u_1} Y))
          {S : Presieve.{v_1, u_1} Y | Sieve.generate S ∈ (J : (a : C) → Set (Sieve a)) Y} T ∧
        T.FactorsThruAlong S f
⊢ Membership.mem (γ := Set (Presieve.{v_1, u_1} X))
      {S : Presieve.{v_1, u_1} X | Sieve.generate S ∈ (J : (a : C) → Set (Sieve a)) X} S →
    ∃ (T : Presieve.{v_1, u_1} Y),
      Membership.mem (γ := Set (Presieve.{v_1, u_1} Y))
          {S : Presieve.{v_1, u_1} Y | Sieve.generate S ∈ (J : (a : C) → Set (Sieve a)) Y} T ∧
        T.FactorsThruAlong S f

Tactic:
(hS : Sieve.generate S ∈ J X)
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_1
D : Type ?u.31285
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, ?u.31285} D
J : GrothendieckTopology.{v_1, u_1} C
X Y : C
f : Y ⟶ X
S : Presieve.{v_1, u_1} X
hS : Sieve.generate S ∈ (J : (a : C) → Set (Sieve a)) X
⊢ ∃ (T : Presieve.{v_1, u_1} Y),
    Membership.mem (γ := Set (Presieve.{v_1, u_1} Y))
        {S : Presieve.{v_1, u_1} Y | Sieve.generate S ∈ (J : (a : C) → Set (Sieve a)) Y} T ∧
      T.FactorsThruAlong S f

Tactic:
⟨(Sieve.generate S).pullback f, ?_, fun Z g h => h⟩

Premises used: CategoryTheory.Sieve.arrows, And.intro, Exists.intro, CategoryTheory.Sieve.generate, CategoryTheory.Sieve.pullback
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_1
D : Type ?u.31285
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, ?u.31285} D
J : GrothendieckTopology.{v_1, u_1} C
X Y : C
f : Y ⟶ X
S : Presieve.{v_1, u_1} X
hS : Sieve.generate S ∈ (J : (a : C) → Set (Sieve a)) X
refine :
  Membership.mem (γ := Set (Presieve.{v_1, u_1} Y))
    {S : Presieve.{v_1, u_1} Y | Sieve.generate S ∈ (J : (a : C) → Set (Sieve a)) Y}
    (Sieve.pullback f (Sieve.generate S)).arrows
⊢ ∃ (T : Presieve.{v_1, u_1} Y),
    Membership.mem (γ := Set (Presieve.{v_1, u_1} Y))
        {S : Presieve.{v_1, u_1} Y | Sieve.generate S ∈ (J : (a : C) → Set (Sieve a)) Y} T ∧
      T.FactorsThruAlong S f

Tactic:
refine ⟨(Sieve.generate S).pullback f, ?_, fun Z g h => h⟩
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_1
D : Type ?u.31285
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, ?u.31285} D
J : GrothendieckTopology.{v_1, u_1} C
X Y : C
f : Y ⟶ X
S : Presieve.{v_1, u_1} X
hS : Sieve.generate S ∈ (J : (a : C) → Set (Sieve a)) X
rw : Sieve.pullback f (Sieve.generate S) ∈ (J : (a : C) → Set (Sieve a)) Y
⊢ Sieve.generate (Sieve.pullback f (Sieve.generate S)).arrows ∈ (J : (a : C) → Set (Sieve a)) Y

Tactic:
rw [Sieve.generate_sieve]

Premises used: CategoryTheory.Sieve.generate_sieve
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_1
D : Type ?u.31285
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, ?u.31285} D
J : GrothendieckTopology.{v_1, u_1} C
X Y : C
f : Y ⟶ X
S : Presieve.{v_1, u_1} X
hS : Sieve.generate S ∈ (J : (a : C) → Set (Sieve a)) X
⊢ Sieve.pullback f (Sieve.generate S) ∈ (J : (a : C) → Set (Sieve a)) Y

Tactic:
J.pullback_stable _ hS

Premises used: Set.Mem, CategoryTheory.GrothendieckTopology.pullback_stable
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_1
D : Type ?u.31285
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, ?u.31285} D
J : GrothendieckTopology.{v_1, u_1} C
X Y : C
f : Y ⟶ X
S : Presieve.{v_1, u_1} X
hS : Sieve.generate S ∈ (J : (a : C) → Set (Sieve a)) X
⊢ Sieve.pullback f (Sieve.generate S) ∈ (J : (a : C) → Set (Sieve a)) Y

Tactic:
exact J.pullback_stable _ hS

Premises used: CategoryTheory.GrothendieckTopology.pullback_stable
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : C
S : Presieve.{v_1, u_1} X
J : GrothendieckTopology.{v_1, u_1} C
⊢ S ∈ J.toCoverage.coverings X ↔ Sieve.generate S ∈ (J : (a : C) → Set (Sieve a)) X

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
S T : Sieve.{v_1, u_1} X
h : S ≤ T
f : Y ⟶ X
hf : S.arrows f
h₁ : ∀ ⦃Z : C⦄ (g : Z ⟶ Y), (Sieve.pullback f T).arrows g ↔ Sieve.arrows ⊤ g
⊢ Sieve.pullback f T = ⊤

Tactic:
ext Z g
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
S T : Sieve.{v_1, u_1} X
h : S ≤ T
f : Y ⟶ X
hf : S.arrows f
Z : C
g : Z ⟶ Y
h₁ : T.arrows (g ≫ f)
⊢ (Sieve.pullback f T).arrows g ↔ Sieve.arrows ⊤ g

Tactic:
simp only [Sieve.pullback_apply, Sieve.top_apply, iff_true]

Premises used: CategoryTheory.Sieve.pullback_apply, CategoryTheory.Sieve.top_apply, iff_true
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
S T : Sieve.{v_1, u_1} X
h : S ≤ T
f : Y ⟶ X
hf : S.arrows f
Z : C
g : Z ⟶ Y
h₁ : S.arrows (g ≫ f)
⊢ T.arrows (g ≫ f)

Tactic:
apply h
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
S T : Sieve.{v_1, u_1} X
h : S ≤ T
f : Y ⟶ X
hf : S.arrows f
Z : C
g : Z ⟶ Y
h₁ : S.arrows f
⊢ S.arrows (g ≫ f)

Tactic:
apply S.downward_closed

Premises used: CategoryTheory.Sieve.downward_closed
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
S T : Sieve.{v_1, u_1} X
h : S ≤ T
f : Y ⟶ X
hf : S.arrows f
Z : C
g : Z ⟶ Y
⊢ S.arrows f

Tactic:
hf
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
S T : Sieve.{v_1, u_1} X
h : S ≤ T
f : Y ⟶ X
hf : S.arrows f
Z : C
g : Z ⟶ Y
⊢ S.arrows f

Tactic:
exact hf
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
K : Coverage.{v_1, u_1} C
X : C
S T : Sieve.{v_1, u_1} X
h : S ≤ T
hS : K.Saturate X S
apply : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → K.Saturate Y (Sieve.pullback f T)
⊢ K.Saturate X T

Tactic:
apply Saturate.transitive _ _ _ hS

Premises used: CategoryTheory.Coverage.Saturate.transitive
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
K : Coverage.{v_1, u_1} C
X : C
S T : Sieve.{v_1, u_1} X
h : S ≤ T
hS : K.Saturate X S
Y : C
g : Y ⟶ X
hg : S.arrows g
rw : K.Saturate Y ⊤
hf : S.arrows g
⊢ K.Saturate Y (Sieve.pullback g T)

Tactic:
rw [eq_top_pullback (h := h)]

Premises used: CategoryTheory.Coverage.eq_top_pullback
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
K : Coverage.{v_1, u_1} C
X : C
S T : Sieve.{v_1, u_1} X
h : S ≤ T
hS : K.Saturate X S
Y : C
g : Y ⟶ X
hg : S.arrows g
⊢ K.Saturate Y ⊤

Tactic:
apply Saturate.top

Premises used: CategoryTheory.Coverage.Saturate.top
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
K : Coverage.{v_1, u_1} C
X : C
S T : Sieve.{v_1, u_1} X
h : S ≤ T
hS : K.Saturate X S
Y : C
g : Y ⟶ X
hg : S.arrows g
⊢ S.arrows g

Tactic:
assumption
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
K : Coverage.{v_1, u_1} C
X_1 Y : C
S_1 : Sieve.{v_1, u_1} X_1
X : C
S : Presieve.{v_1, u_1} X
hS : S ∈ K.coverings X
f : Y ⟶ X
of :
  ∀ (R : Presieve.{v_1, u_1} Y) (hR1 : R ∈ K.coverings Y) (hR2 : R.FactorsThruAlong S f),
    K.Saturate Y (Sieve.pullback f (Sieve.generate S))
⊢ K.Saturate Y (Sieve.pullback f (Sieve.generate S))

Tactic:
obtain ⟨R, hR1, hR2⟩ := K.pullback f S hS

Premises used: CategoryTheory.Coverage.pullback
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
K : Coverage.{v_1, u_1} C
X_1 Y : C
S_1 : Sieve.{v_1, u_1} X_1
X : C
S : Presieve.{v_1, u_1} X
hS : S ∈ K.coverings X
f : Y ⟶ X
R : Presieve.{v_1, u_1} Y
hR1 : R ∈ K.coverings Y
hR2 : R.FactorsThruAlong S f
of : Sieve.generate R ≤ Sieve.pullback f (Sieve.generate S)
⊢ K.Saturate Y (Sieve.pullback f (Sieve.generate S))

Tactic:
suffices Sieve.generate R ≤ (Sieve.generate S).pullback f from
      saturate_of_superset _ this (Saturate.of _ _ hR1)
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
K : Coverage.{v_1, u_1} C
X_1 Y : C
S_1 : Sieve.{v_1, u_1} X_1
X : C
S : Presieve.{v_1, u_1} X
hS : S ∈ K.coverings X
f : Y ⟶ X
R : Presieve.{v_1, u_1} Y
hR1 : R ∈ K.coverings Y
hR2 : R.FactorsThruAlong S f
Z : C
g : Z ⟶ Y
of : ∀ (W : C) (i : Z ⟶ W) (e : W ⟶ Y) (h1 : R e) (h2 : i ≫ e = g), (Sieve.pullback f (Sieve.generate S)).arrows g
⊢ (Sieve.generate R).arrows g → (Sieve.pullback f (Sieve.generate S)).arrows g

Tactic:
⟨W, i, e, h1, h2⟩
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
K : Coverage.{v_1, u_1} C
X_1 Y : C
S_1 : Sieve.{v_1, u_1} X_1
X : C
S : Presieve.{v_1, u_1} X
hS : S ∈ K.coverings X
f : Y ⟶ X
R : Presieve.{v_1, u_1} Y
hR1 : R ∈ K.coverings Y
hR2 : R.FactorsThruAlong S f
Z : C
g : Z ⟶ Y
W : C
i : Z ⟶ W
e : W ⟶ Y
h1 : R e
h2 : i ≫ e = g
of :
  ∀ (WW : C) (ii : W ⟶ WW) (ee : WW ⟶ X) (hh1 : S ee) (hh2 : ii ≫ ee = e ≫ f),
    (Sieve.pullback f (Sieve.generate S)).arrows g
⊢ (Sieve.pullback f (Sieve.generate S)).arrows g

Tactic:
obtain ⟨WW, ii, ee, hh1, hh2⟩ := hR2 h1
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
K : Coverage.{v_1, u_1} C
X_1 Y : C
S_1 : Sieve.{v_1, u_1} X_1
X : C
S : Presieve.{v_1, u_1} X
hS : S ∈ K.coverings X
f : Y ⟶ X
R : Presieve.{v_1, u_1} Y
hR1 : R ∈ K.coverings Y
hR2 : R.FactorsThruAlong S f
Z : C
g : Z ⟶ Y
W : C
i : Z ⟶ W
e : W ⟶ Y
h1 : R e
h2 : i ≫ e = g
WW : C
ii : W ⟶ WW
ee : WW ⟶ X
hh1 : S ee
hh2 : ii ≫ ee = e ≫ f
⊢ (Sieve.pullback f (Sieve.generate S)).arrows g

Tactic:
⟨WW, i ≫ ii, ee, hh1, ?_⟩

Premises used: And.intro, Exists.intro, CategoryTheory.CategoryStruct.comp
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
K : Coverage.{v_1, u_1} C
X_1 Y : C
S_1 : Sieve.{v_1, u_1} X_1
X : C
S : Presieve.{v_1, u_1} X
hS : S ∈ K.coverings X
f : Y ⟶ X
R : Presieve.{v_1, u_1} Y
hR1 : R ∈ K.coverings Y
hR2 : R.FactorsThruAlong S f
Z : C
g : Z ⟶ Y
W : C
i : Z ⟶ W
e : W ⟶ Y
h1 : R e
h2 : i ≫ e = g
WW : C
ii : W ⟶ WW
ee : WW ⟶ X
hh1 : S ee
hh2 : ii ≫ ee = e ≫ f
of : (i ≫ ii) ≫ ee = g ≫ f
⊢ (Sieve.pullback f (Sieve.generate S)).arrows g

Tactic:
refine ⟨WW, i ≫ ii, ee, hh1, ?_⟩