awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.CoverPreserving
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
J : GrothendieckTopology.{v₁, u₁} C
K : GrothendieckTopology.{v₂, u₂} D
inst_2 : HasPullbacks.{v₁, u₁} C
inst_3 : PreservesLimitsOfShape WalkingCospan F
H : CoverPreserving J K F
U : C
E : GrothendieckTopology.OneHypercover.{w, v₁, u₁} J U
i₁ i₂ : E.I₀
W : D
p₁ : W ⟶ F.obj (E.X i₁)
p₂ : W ⟶ F.obj (E.X i₂)
h : p₁ ≫ F.map (E.f i₁) = p₂ ≫ F.map (E.f i₂)
P : C := Limits.pullback (E.f i₁) (E.f i₂)
this_1 : HasPullback ((E.map F).f i₁) ((E.map F).f i₂)
this :
  Membership.mem (γ := Set (Sieve.{v₂, u₂} (F.obj (Limits.pullback (E.f i₁) (E.f i₂)))))
    ((K : (a : D) → Set (Sieve a)) (F.obj (Limits.pullback (E.f i₁) (E.f i₂))))
    ((E.map F).sieve₁ (F.map (pullback.fst (E.f i₁) (E.f i₂))) (F.map (pullback.snd (E.f i₁) (E.f i₂))))
⊢ Sieve.pullback (X := F.obj (Limits.pullback (E.f i₁) (E.f i₂))) (IsPullback.lift ⋯ p₁ p₂ h)
      ((E.map F).sieve₁ (F.map (pullback.fst (E.f i₁) (E.f i₂))) (F.map (pullback.snd (E.f i₁) (E.f i₂)))) ≤
    (E.map F).sieve₁ p₁ p₂

Tactic:
simp [PreOneHypercover.pullback_sieve₁]

Premises used: CategoryTheory.PreOneHypercover.pullback_sieve₁
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
R : Presieve.{v_1, u_1} Y
inst_1 : R.HasPullbacks f
Z : C
g : Z ⟶ X
this :
  ∀ (W : C) (b : W ⟶ Y) (hb : R b),
    ∃ (W_1 : C) (i : pullback b f ⟶ W_1) (e : W_1 ⟶ Y), R e ∧ i ≫ e = pullback.snd b f ≫ f
⊢ Presieve.pullbackArrows f R g → ∃ (W : C) (i : Z ⟶ W) (e : W ⟶ Y), R e ∧ i ≫ e = g ≫ f

Tactic:
⟨W, b, hb⟩
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
R : Presieve.{v_1, u_1} Y
inst_1 : R.HasPullbacks f
Z : C
g : Z ⟶ X
W : C
b : W ⟶ Y
hb : R b
⊢ HasPullback b f

Tactic:
have := R.hasPullback f hb
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
R : Presieve.{v_1, u_1} Y
inst_1 : R.HasPullbacks f
Z : C
g : Z ⟶ X
W : C
b : W ⟶ Y
hb : R b
this : HasPullback b f
⊢ ∃ (W_1 : C) (i : pullback b f ⟶ W_1) (e : W_1 ⟶ Y), R e ∧ i ≫ e = pullback.snd b f ≫ f

Tactic:
⟨_, pullback.fst _ _, b, hb, pullback.condition⟩

Premises used: And.intro, CategoryTheory.Limits.pullback.fst, Exists.intro, CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
R : Presieve.{v_1, u_1} Y
inst_1 : R.HasPullbacks f
Z : C
g : Z ⟶ X
W : C
b : W ⟶ Y
hb : R b
this : HasPullback b f
⊢ ∃ (W_1 : C) (i : pullback b f ⟶ W_1) (e : W_1 ⟶ Y), R e ∧ i ≫ e = pullback.snd b f ≫ f

Tactic:
refine ⟨_, pullback.fst _ _, b, hb, pullback.condition⟩
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : C
S T : Presieve.{v_1, u_1} X
⊢ S.FactorsThruAlong T (𝟙 X) ↔ S.FactorsThru T

Tactic:
simp [FactorsThruAlong, FactorsThru]

Premises used: CategoryTheory.Presieve.FactorsThruAlong, CategoryTheory.Presieve.FactorsThru
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : C
S T : Presieve.{v_1, u_1} X
h : S ≤ T
Y : C
g : Y ⟶ X
hg : S g
⊢ 𝟙 Y ≫ g = g

Tactic:
simp
-- 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
T : Sieve.{v_1, u_1} X
h : S.FactorsThru T.arrows
Y : C
f : Y ⟶ X
hf : S f
obtain : ∀ (W : C) (i : Y ⟶ W) (e : W ⟶ X) (h1 : T.arrows e) (hf : S (i ≫ e)), T.arrows (i ≫ e)
⊢ T.arrows f

Tactic:
obtain ⟨W, i, e, h1, rfl⟩ := h hf

Premises used: rfl
-- 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
T : Sieve.{v_1, u_1} X
h : S.FactorsThru T.arrows
Y W : C
i : Y ⟶ W
e : W ⟶ X
h1 : T.arrows e
hf : S (i ≫ e)
⊢ T.arrows (i ≫ e)

Tactic:
T.downward_closed h1 _

Premises used: CategoryTheory.Sieve.downward_closed
-- 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
T : Sieve.{v_1, u_1} X
h : S.FactorsThru T.arrows
Y W : C
i : Y ⟶ W
e : W ⟶ X
h1 : T.arrows e
hf : S (i ≫ e)
⊢ T.arrows (i ≫ e)

Tactic:
exact T.downward_closed h1 _

Premises used: CategoryTheory.Sieve.downward_closed
-- 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
⊢ S.FactorsThru ⊤

Tactic:
factorsThru_of_le _ _ le_top

Premises used: le_top, CategoryTheory.Presieve.factorsThru_of_le
-- 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 : S.FactorsThru T
hS : IsSheafFor P S
h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, T f → ∃ (R : Presieve.{v_1, u_2} Y), IsSeparatedFor P R ∧ R.FactorsThruAlong S f
simp :
  ∀
    (hS :
      IsSeparatedFor P S ∧
        ∀ (x : FamilyOfElements P S),
          x.Compatible (R := S) → ∃ (t : P.obj (Opposite.op X)), x.IsAmalgamation (R := S) t),
    IsSeparatedFor P T ∧
      ∀ (x : FamilyOfElements P T), x.Compatible (R := T) → ∃ (t : P.obj (Opposite.op X)), x.IsAmalgamation (R := T) t
⊢ IsSheafFor P T

Tactic:
simp only [← Presieve.isSeparatedFor_and_exists_isAmalgamation_iff_isSheafFor] at *

Premises used: CategoryTheory.Presieve.isSeparatedFor_and_exists_isAmalgamation_iff_isSheafFor
-- 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 : S.FactorsThru T
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
choose :
  ∀ (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),
    IsSeparatedFor P T ∧
      ∀ (x : FamilyOfElements P T), x.Compatible (R := T) → ∃ (t : P.obj (Opposite.op X)), x.IsAmalgamation (R := T) t
⊢ IsSeparatedFor P T ∧
    ∀ (x : FamilyOfElements P T), x.Compatible (R := T) → ∃ (t : P.obj (Opposite.op X)), x.IsAmalgamation (R := T) t

Tactic:
choose W i e h1 h2 using H
-- 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
⊢ IsSeparatedFor P T ∧
    ∀ (x : FamilyOfElements P T), x.Compatible (R := T) → ∃ (t : P.obj (Opposite.op X)), x.IsAmalgamation (R := T) t

Tactic:
⟨?_, fun x hx => ?_⟩

Premises used: And.intro
-- 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
refine_1 : IsSeparatedFor P T
refine_2 :
  ∀ (x : FamilyOfElements P T) (hx : x.Compatible (R := T)), ∃ (t : P.obj (Opposite.op X)), x.IsAmalgamation (R := T) t
⊢ IsSeparatedFor P T ∧
    ∀ (x : FamilyOfElements P T), x.Compatible (R := T) → ∃ (t : P.obj (Opposite.op X)), x.IsAmalgamation (R := T) t

Tactic:
refine ⟨?_, fun x 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
y₁ y₂ : P.obj (Opposite.op X)
h₁ : x.IsAmalgamation (R := T) y₁
h₂ : x.IsAmalgamation (R := T) y₂
⊢ y₁ = y₂

Tactic:
hS.1.ext (fun Y g hg => ?_)

Premises used: CategoryTheory.Presieve.IsSeparatedFor.ext, And.left
-- 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
y₁ y₂ : P.obj (Opposite.op X)
h₁ : x.IsAmalgamation (R := T) y₁
h₂ : x.IsAmalgamation (R := T) y₂
refine_1 :
  ∀ (Y : C) (g : Y ⟶ X) (hg : S g),
    Eq (α := (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op Y)))
      ((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)))
          y₁ :
        (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op Y)))
      ((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)))
          y₂ :
        (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op Y)))
⊢ y₁ = y₂

Tactic:
refine hS.1.ext (fun Y g hg => ?_)

Premises used: CategoryTheory.Presieve.IsSeparatedFor.ext, And.left
-- 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
y₁ y₂ : P.obj (Opposite.op X)
h₁ : x.IsAmalgamation (R := T) y₁
h₂ : x.IsAmalgamation (R := T) y₂
Y : C
g : Y ⟶ X
hg : S g
⊢ Eq (α := (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op Y)))
    ((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)))
        y₁ :
      (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op Y)))
    ((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)))
        y₂ :
      (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op Y)))

Tactic:
simp only [← h2 hg, op_comp, P.map_comp, types_comp_apply, h₁ _ (h1 _), h₂ _ (h1 _)]

Premises used: CategoryTheory.op_comp, CategoryTheory.Functor.map_comp, CategoryTheory.types_comp_apply
-- 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_1 : ∀ ⦃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) ⋯)
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
h₁ : S f₁
h₂ : S f₂
h : g₁ ≫ f₁ = g₂ ≫ f₂
rw :
  Eq (α := (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (g₁ ≫ i h₁).op) :
          (a : (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op (W h₁)))) →
            (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op Z)))
        (x (e h₁) ⋯) :
      (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (g₂ ≫ i h₂).op) :
          (a : (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op (W h₂)))) →
            (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op Z)))
        (x (e h₂) ⋯) :
      (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op Z)))
⊢ Eq (α := (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op Z)))
    ((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)))
        (y f₁ h₁) :
      (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op Z)))
    ((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)))
        (y f₂ h₂) :
      (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op Z)))

Tactic:
rw [← types_comp_apply (P.map (i h₁).op) (P.map g₁.op),
      ← types_comp_apply (P.map (i h₂).op) (P.map g₂.op),
      ← P.map_comp, ← op_comp, ← P.map_comp, ← op_comp]

Premises used: CategoryTheory.op_comp, Quiver.Hom.op, CategoryTheory.Functor.map, CategoryTheory.Functor.map_comp, CategoryTheory.types_comp_apply
-- 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_1 : ∀ ⦃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) ⋯)
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
h₁ : S f₁
h₂ : S f₂
h : g₁ ≫ f₁ = g₂ ≫ f₂
a : (g₁ ≫ i h₁) ≫ e h₁ = (g₂ ≫ i h₂) ≫ e h₂
⊢ Eq (α := (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (g₁ ≫ i h₁).op) :
          (a : (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op (W h₁)))) →
            (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op Z)))
        (x (e h₁) ⋯) :
      (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (g₂ ≫ i h₂).op) :
          (a : (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op (W h₂)))) →
            (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op Z)))
        (x (e h₂) ⋯) :
      (fun (X : Type u_1) ↦ X) (P.obj (Opposite.op Z)))

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_1 : ∀ ⦃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) ⋯)
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
h₁ : S f₁
h₂ : S f₂
h : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ (g₁ ≫ i h₁) ≫ e h₁ = (g₂ ≫ i h₂) ≫ e h₂

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

Premises used: CategoryTheory.Category.assoc
-- 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) ⋯)
⊢ y.Compatible (R := S)

Tactic:
have hy : y.Compatible := by
    intro Y₁ Y₂ Z g₁ g₂ f₁ f₂ h₁ h₂ h
    rw [← types_comp_apply (P.map (i h₁).op) (P.map g₁.op),
      ← types_comp_apply (P.map (i h₂).op) (P.map g₂.op),
      ← P.map_comp, ← op_comp, ← P.map_comp, ← op_comp]
    apply hx
    simp only [h2, h, Category.assoc]
-- 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)
⊢ IsSeparatedFor P S

Tactic:
let ⟨_, h2'⟩ := hS
-- 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
⊢ ∀ (x : FamilyOfElements P S), x.Compatible (R := S) → ∃ (t : P.obj (Opposite.op X)), x.IsAmalgamation (R := S) t

Tactic:
let ⟨_, h2'⟩ := hS
-- 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
refine_2 :
  ∀ (z : P.obj (Opposite.op X)) (hz : y.IsAmalgamation (R := S) z),
    ∃ (t : P.obj (Opposite.op X)), x.IsAmalgamation (R := T) t
⊢ ∃ (t : P.obj (Opposite.op X)), x.IsAmalgamation (R := T) t

Tactic:
obtain ⟨z, hz⟩ := h2' y hy
-- 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
⊢ ∃ (t : P.obj (Opposite.op X)), x.IsAmalgamation (R := T) t

Tactic:
⟨z, fun Y g hg => ?_⟩

Premises used: Exists.intro