awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
X : C
R : Presieve.{v₁, u₁} X
q : ∀ (x : FamilyOfElements P R), x.Compatible (R := R) → ∃ (t : P.obj (op X)), x.IsAmalgamation (R := R) t
x : FamilyOfElements P (generate R).arrows
hx : x.Compatible (R := (generate R).arrows)
apply :
  ∀ (a : P.obj (op X)),
    (FamilyOfElements.restrict (R₁ := R) (R₂ := (generate R).arrows) ⋯ x).IsAmalgamation (R := R) a →
      x.IsAmalgamation (R := (generate R).arrows) a
⊢ ∃ (t : P.obj (op X)), x.IsAmalgamation (R := (generate R).arrows) t

Tactic:
apply Exists.imp _ (q _ (hx.restrict (le_generate R)))

Premises used: CategoryTheory.Sieve.le_generate, Exists.imp, CategoryTheory.Presieve.FamilyOfElements.Compatible.restrict
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
X : C
R : Presieve.{v₁, u₁} X
q : ∀ (x : FamilyOfElements P R), x.Compatible (R := R) → ∃ (t : P.obj (op X)), x.IsAmalgamation (R := R) t
x : FamilyOfElements P (generate R).arrows
hx : x.Compatible (R := (generate R).arrows)
t : P.obj (op X)
ht : (FamilyOfElements.restrict (R₁ := R) (R₂ := (generate R).arrows) ⋯ x).IsAmalgamation (R := R) t
⊢ x.IsAmalgamation (R := (generate R).arrows) t

Tactic:
simpa [hx] using isAmalgamation_sieveExtend _ _ ht

Premises used: CategoryTheory.Presieve.isAmalgamation_sieveExtend
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
X : C
R : Presieve.{v₁, u₁} X
q :
  ∀ (x : FamilyOfElements P (generate R).arrows),
    x.Compatible (R := (generate R).arrows) → ∃ (t : P.obj (op X)), x.IsAmalgamation (R := (generate R).arrows) t
x : FamilyOfElements P R
hx : x.Compatible (R := R)
apply :
  ∀ (a : P.obj (op X)), x.sieveExtend (R := R).IsAmalgamation (R := (generate R).arrows) a → x.IsAmalgamation (R := R) a
⊢ ∃ (t : P.obj (op X)), x.IsAmalgamation (R := R) t

Tactic:
apply Exists.imp _ (q _ hx.sieveExtend)

Premises used: Exists.imp, CategoryTheory.Presieve.FamilyOfElements.Compatible.sieveExtend
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
X : C
R : Presieve.{v₁, u₁} X
q :
  ∀ (x : FamilyOfElements P (generate R).arrows),
    x.Compatible (R := (generate R).arrows) → ∃ (t : P.obj (op X)), x.IsAmalgamation (R := (generate R).arrows) t
x : FamilyOfElements P R
hx : x.Compatible (R := R)
t : P.obj (op X)
ht : x.sieveExtend (R := R).IsAmalgamation (R := (generate R).arrows) t
⊢ x.IsAmalgamation (R := R) t

Tactic:
simpa [hx] using isAmalgamation_restrict (le_generate R) _ _ ht

Premises used: CategoryTheory.Sieve.le_generate, CategoryTheory.Presieve.isAmalgamation_restrict
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
x : FamilyOfElements P (singleton (𝟙 X))
_ : x.Compatible (R := singleton (𝟙 X)) → ∃! t : P.obj (op X), x.IsAmalgamation (R := singleton (𝟙 X)) t
⊢ x.Compatible (R := singleton (𝟙 X)) → ∃! t : P.obj (op X), x.IsAmalgamation (R := singleton (𝟙 X)) t

Tactic:
_
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
x : FamilyOfElements P (singleton (𝟙 X))
h : x.Compatible (R := singleton (𝟙 X))
⊢ ∃! t : P.obj (op X), x.IsAmalgamation (R := singleton (𝟙 X)) t

Tactic:
⟨x _ (Presieve.singleton_self _), ?_, ?_⟩

Premises used: CategoryTheory.Presieve.singleton_self, ExistsUnique, And.intro, Exists.intro
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
x : FamilyOfElements P (singleton (𝟙 X))
h : x.Compatible (R := singleton (𝟙 X))
refine_1 : (fun (t : P.obj (op X)) ↦ x.IsAmalgamation (R := singleton (𝟙 X)) t) (x (𝟙 X) ⋯)
refine_2 : ∀ (y : P.obj (op X)), (fun (t : P.obj (op X)) ↦ x.IsAmalgamation (R := singleton (𝟙 X)) t) y → y = x (𝟙 X) ⋯
⊢ ∃! t : P.obj (op X), x.IsAmalgamation (R := singleton (𝟙 X)) t

Tactic:
refine ⟨x _ (Presieve.singleton_self _), ?_, ?_⟩
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
x : FamilyOfElements P (singleton (𝟙 X))
h : x.Compatible (R := singleton (𝟙 X))
Y : C
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (Quiver.Hom.op (𝟙 X))) :
        (a : (fun (X : Type w) ↦ X) (P.obj (op X))) → (fun (X : Type w) ↦ X) (P.obj (op X)))
      (x (𝟙 X) ⋯) =
    x (𝟙 X) ⋯

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
x : FamilyOfElements P (singleton (𝟙 X))
h : x.Compatible (R := singleton (𝟙 X))
t : P.obj (op X)
ht : x.IsAmalgamation (R := singleton (𝟙 X)) t
⊢ t = x (𝟙 X) ⋯

Tactic:
simpa using ht _ (Presieve.singleton_self _)

Premises used: CategoryTheory.Presieve.singleton_self
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
rw : IsSheafFor P (arrows (generate (singleton (𝟙 X))))
⊢ IsSheafFor (X := X) P ⊤

Tactic:
rw [← arrows_top, ← generate_of_singleton_isSplitEpi (𝟙 X)]

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Sieve.arrows_top, CategoryTheory.Sieve.generate_of_singleton_isSplitEpi
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
rw : IsSheafFor P (singleton (𝟙 X))
⊢ IsSheafFor P (arrows (generate (singleton (𝟙 X))))

Tactic:
rw [← isSheafFor_iff_generate]

Premises used: CategoryTheory.Presieve.isSheafFor_iff_generate
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
⊢ IsSheafFor P (singleton (𝟙 X))

Tactic:
apply isSheafFor_singleton_iso

Premises used: CategoryTheory.Presieve.isSheafFor_singleton_iso
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P₁ : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
P₂ : Functor.{v₁, w', u₁, w' + 1} Cᵒᵖ (Type w')
e : ⦃X : C⦄ → Equiv.{w + 1, w' + 1} (P₁.obj (op X)) (P₂.obj (op X))
he :
  ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : P₁.obj (op Y)),
    Eq.{w' + 1} (α := P₂.obj (op X))
      ((e : (a : P₁.obj (op X)) → P₂.obj (op X))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (P₁.map f.op) :
              (a : (fun (X : Type w) ↦ X) (P₁.obj (op Y))) → (fun (X : Type w) ↦ X) (P₁.obj (op X)))
            x) :
        P₂.obj (op X))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (P₂.map f.op) :
            (a : (fun (X : Type w') ↦ X) (P₂.obj (op Y))) → (fun (X : Type w') ↦ X) (P₂.obj (op X)))
          ((e : (a : P₁.obj (op Y)) → P₂.obj (op Y)) x : P₂.obj (op Y)) :
        (fun (X : Type w') ↦ X) (P₂.obj (op X)))
X_1 : C
R : Presieve.{v₁, u₁} X_1
hP₁ : IsSheafFor P₁ R
x₂ : FamilyOfElements P₂ R
hx₂ : x₂.Compatible (R := R)
X Y : C
f : X ⟶ Y
x : P₂.obj (op Y)
⊢ Eq.{w' + 1} (α := P₂.obj (op X))
    ((e : (a : P₁.obj (op X)) → P₂.obj (op X))
        ((Equiv.symm e : (a : P₂.obj (op X)) → P₁.obj (op X))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (P₂.map f.op) :
              (a : (fun (X : Type w') ↦ X) (P₂.obj (op Y))) → (fun (X : Type w') ↦ X) (P₂.obj (op X)))
            x)) :
      P₂.obj (op X))
    ((e : (a : P₁.obj (op X)) → P₂.obj (op X))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (P₁.map f.op) :
            (a : (fun (X : Type w) ↦ X) (P₁.obj (op Y))) → (fun (X : Type w) ↦ X) (P₁.obj (op X)))
          ((Equiv.symm e : (a : P₂.obj (op Y)) → P₁.obj (op Y)) x : P₁.obj (op Y))) :
      P₂.obj (op X))

Tactic:
simp only [Equiv.apply_symm_apply, he]

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P₁ : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
P₂ : Functor.{v₁, w', u₁, w' + 1} Cᵒᵖ (Type w')
e : ⦃X : C⦄ → Equiv.{w + 1, w' + 1} (P₁.obj (op X)) (P₂.obj (op X))
he :
  ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : P₁.obj (op Y)),
    Eq.{w' + 1} (α := P₂.obj (op X))
      ((e : (a : P₁.obj (op X)) → P₂.obj (op X))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (P₁.map f.op) :
              (a : (fun (X : Type w) ↦ X) (P₁.obj (op Y))) → (fun (X : Type w) ↦ X) (P₁.obj (op X)))
            x) :
        P₂.obj (op X))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (P₂.map f.op) :
            (a : (fun (X : Type w') ↦ X) (P₂.obj (op Y))) → (fun (X : Type w') ↦ X) (P₂.obj (op X)))
          ((e : (a : P₁.obj (op Y)) → P₂.obj (op Y)) x : P₂.obj (op Y)) :
        (fun (X : Type w') ↦ X) (P₂.obj (op X)))
X : C
R : Presieve.{v₁, u₁} X
hP₁ : IsSheafFor P₁ R
x₂ : FamilyOfElements P₂ R
hx₂ : x₂.Compatible (R := R)
⊢ ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : P₂.obj (op Y)),
    Eq.{w + 1} (α := P₁.obj (op X))
      ((Equiv.symm e : (a : P₂.obj (op X)) → P₁.obj (op X))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (P₂.map f.op) :
              (a : (fun (X : Type w') ↦ X) (P₂.obj (op Y))) → (fun (X : Type w') ↦ X) (P₂.obj (op X)))
            x) :
        P₁.obj (op X))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (P₁.map f.op) :
            (a : (fun (X : Type w) ↦ X) (P₁.obj (op Y))) → (fun (X : Type w) ↦ X) (P₁.obj (op X)))
          ((Equiv.symm e : (a : P₂.obj (op Y)) → P₁.obj (op Y)) x : P₁.obj (op Y)) :
        (fun (X : Type w) ↦ X) (P₁.obj (op X)))

Tactic:
have he' : ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : P₂.obj (op Y)),
    e.symm (P₂.map f.op x) = P₁.map f.op (e.symm x) := fun X Y f x ↦
      e.injective (by simp only [Equiv.apply_symm_apply, he])
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P₁ : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
P₂ : Functor.{v₁, w', u₁, w' + 1} Cᵒᵖ (Type w')
e : ⦃X : C⦄ → Equiv.{w + 1, w' + 1} (P₁.obj (op X)) (P₂.obj (op X))
he :
  ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : P₁.obj (op Y)),
    Eq.{w' + 1} (α := P₂.obj (op X))
      ((e : (a : P₁.obj (op X)) → P₂.obj (op X))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (P₁.map f.op) :
              (a : (fun (X : Type w) ↦ X) (P₁.obj (op Y))) → (fun (X : Type w) ↦ X) (P₁.obj (op X)))
            x) :
        P₂.obj (op X))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (P₂.map f.op) :
            (a : (fun (X : Type w') ↦ X) (P₂.obj (op Y))) → (fun (X : Type w') ↦ X) (P₂.obj (op X)))
          ((e : (a : P₁.obj (op Y)) → P₂.obj (op Y)) x : P₂.obj (op Y)) :
        (fun (X : Type w') ↦ X) (P₂.obj (op X)))
X : C
R : Presieve.{v₁, u₁} X
hP₁ : IsSheafFor P₁ R
x₂ : FamilyOfElements P₂ R
hx₂ : x₂.Compatible (R := R)
he' :
  ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : P₂.obj (op Y)),
    Eq.{w + 1} (α := P₁.obj (op X))
      ((Equiv.symm e : (a : P₂.obj (op X)) → P₁.obj (op X))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (P₂.map f.op) :
              (a : (fun (X : Type w') ↦ X) (P₂.obj (op Y))) → (fun (X : Type w') ↦ X) (P₂.obj (op X)))
            x) :
        P₁.obj (op X))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (P₁.map f.op) :
            (a : (fun (X : Type w) ↦ X) (P₁.obj (op Y))) → (fun (X : Type w) ↦ X) (P₁.obj (op X)))
          ((Equiv.symm e : (a : P₂.obj (op Y)) → P₁.obj (op Y)) x : P₁.obj (op Y)) :
        (fun (X : Type w) ↦ X) (P₁.obj (op X)))
x₁ : FamilyOfElements P₁ R :=
  fun (Y : C) (f : Y ⟶ X) (hf : R f) ↦ (Equiv.symm e : (a : P₂.obj (op Y)) → P₁.obj (op Y)) (x₂ f hf)
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
h₁ : R f₁
h₂ : R f₂
fac : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ Eq.{w' + 1} (α := P₂.obj (op Z))
    ((e : (a : P₁.obj (op Z)) → P₂.obj (op Z))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (P₁.map g₁.op) :
            (a : (fun (X : Type w) ↦ X) (P₁.obj (op Y₁))) → (fun (X : Type w) ↦ X) (P₁.obj (op Z)))
          (x₁ f₁ h₁)) :
      P₂.obj (op Z))
    ((e : (a : P₁.obj (op Z)) → P₂.obj (op Z))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (P₁.map g₂.op) :
            (a : (fun (X : Type w) ↦ X) (P₁.obj (op Y₂))) → (fun (X : Type w) ↦ X) (P₁.obj (op Z)))
          (x₁ f₂ h₂)) :
      P₂.obj (op Z))

Tactic:
simp only [he, Equiv.apply_symm_apply, hx₂ g₁ g₂ h₁ h₂ fac, x₁]

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P₁ : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
P₂ : Functor.{v₁, w', u₁, w' + 1} Cᵒᵖ (Type w')
e : ⦃X : C⦄ → Equiv.{w + 1, w' + 1} (P₁.obj (op X)) (P₂.obj (op X))
he :
  ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : P₁.obj (op Y)),
    Eq.{w' + 1} (α := P₂.obj (op X))
      ((e : (a : P₁.obj (op X)) → P₂.obj (op X))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (P₁.map f.op) :
              (a : (fun (X : Type w) ↦ X) (P₁.obj (op Y))) → (fun (X : Type w) ↦ X) (P₁.obj (op X)))
            x) :
        P₂.obj (op X))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (P₂.map f.op) :
            (a : (fun (X : Type w') ↦ X) (P₂.obj (op Y))) → (fun (X : Type w') ↦ X) (P₂.obj (op X)))
          ((e : (a : P₁.obj (op Y)) → P₂.obj (op Y)) x : P₂.obj (op Y)) :
        (fun (X : Type w') ↦ X) (P₂.obj (op X)))
X : C
R : Presieve.{v₁, u₁} X
hP₁ : IsSheafFor P₁ R
x₂ : FamilyOfElements P₂ R
hx₂ : x₂.Compatible (R := R)
he' :
  ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : P₂.obj (op Y)),
    Eq.{w + 1} (α := P₁.obj (op X))
      ((Equiv.symm e : (a : P₂.obj (op X)) → P₁.obj (op X))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (P₂.map f.op) :
              (a : (fun (X : Type w') ↦ X) (P₂.obj (op Y))) → (fun (X : Type w') ↦ X) (P₂.obj (op X)))
            x) :
        P₁.obj (op X))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (P₁.map f.op) :
            (a : (fun (X : Type w) ↦ X) (P₁.obj (op Y))) → (fun (X : Type w) ↦ X) (P₁.obj (op X)))
          ((Equiv.symm e : (a : P₂.obj (op Y)) → P₁.obj (op Y)) x : P₁.obj (op Y)) :
        (fun (X : Type w) ↦ X) (P₁.obj (op X)))
x₁ : FamilyOfElements P₁ R :=
  fun (Y : C) (f : Y ⟶ X) (hf : R f) ↦ (Equiv.symm e : (a : P₂.obj (op Y)) → P₁.obj (op Y)) (x₂ f hf)
⊢ x₁.Compatible (R := R)

Tactic:
have hx₁ : x₁.Compatible := fun Y₁ Y₂ Z g₁ g₂ f₁ f₂ h₁ h₂ fac ↦ e.injective
    (by simp only [he, Equiv.apply_symm_apply, hx₂ g₁ g₂ h₁ h₂ fac, x₁])
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P₁ : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
P₂ : Functor.{v₁, w', u₁, w' + 1} Cᵒᵖ (Type w')
e : ⦃X : C⦄ → Equiv.{w + 1, w' + 1} (P₁.obj (op X)) (P₂.obj (op X))
he :
  ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : P₁.obj (op Y)),
    Eq.{w' + 1} (α := P₂.obj (op X))
      ((e : (a : P₁.obj (op X)) → P₂.obj (op X))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (P₁.map f.op) :
              (a : (fun (X : Type w) ↦ X) (P₁.obj (op Y))) → (fun (X : Type w) ↦ X) (P₁.obj (op X)))
            x) :
        P₂.obj (op X))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (P₂.map f.op) :
            (a : (fun (X : Type w') ↦ X) (P₂.obj (op Y))) → (fun (X : Type w') ↦ X) (P₂.obj (op X)))
          ((e : (a : P₁.obj (op Y)) → P₂.obj (op Y)) x : P₂.obj (op Y)) :
        (fun (X : Type w') ↦ X) (P₂.obj (op X)))
X : C
R : Presieve.{v₁, u₁} X
hP₁ : IsSheafFor P₁ R
x₂ : FamilyOfElements P₂ R
hx₂ : x₂.Compatible (R := R)
he' :
  ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : P₂.obj (op Y)),
    Eq.{w + 1} (α := P₁.obj (op X))
      ((Equiv.symm e : (a : P₂.obj (op X)) → P₁.obj (op X))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (P₂.map f.op) :
              (a : (fun (X : Type w') ↦ X) (P₂.obj (op Y))) → (fun (X : Type w') ↦ X) (P₂.obj (op X)))
            x) :
        P₁.obj (op X))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (P₁.map f.op) :
            (a : (fun (X : Type w) ↦ X) (P₁.obj (op Y))) → (fun (X : Type w) ↦ X) (P₁.obj (op X)))
          ((Equiv.symm e : (a : P₂.obj (op Y)) → P₁.obj (op Y)) x : P₁.obj (op Y)) :
        (fun (X : Type w) ↦ X) (P₁.obj (op X)))
x₁ : FamilyOfElements P₁ R :=
  fun (Y : C) (f : Y ⟶ X) (hf : R f) ↦ (Equiv.symm e : (a : P₂.obj (op Y)) → P₁.obj (op Y)) (x₂ f hf)
hx₁ : x₁.Compatible (R := R)
t₂ : P₂.obj (op X)
⊢ x₂.IsAmalgamation (R := R) t₂ ↔ x₁.IsAmalgamation (R := R) ((Equiv.symm e : (a : P₂.obj (op X)) → P₁.obj (op X)) t₂)

Tactic:
simp only [FamilyOfElements.IsAmalgamation, x₁,
      ← he', EmbeddingLike.apply_eq_iff_eq]

Premises used: EmbeddingLike.apply_eq_iff_eq, CategoryTheory.Presieve.FamilyOfElements.IsAmalgamation
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P₁ : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
P₂ : Functor.{v₁, w', u₁, w' + 1} Cᵒᵖ (Type w')
e : ⦃X : C⦄ → Equiv.{w + 1, w' + 1} (P₁.obj (op X)) (P₂.obj (op X))
he :
  ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : P₁.obj (op Y)),
    Eq.{w' + 1} (α := P₂.obj (op X))
      ((e : (a : P₁.obj (op X)) → P₂.obj (op X))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (P₁.map f.op) :
              (a : (fun (X : Type w) ↦ X) (P₁.obj (op Y))) → (fun (X : Type w) ↦ X) (P₁.obj (op X)))
            x) :
        P₂.obj (op X))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (P₂.map f.op) :
            (a : (fun (X : Type w') ↦ X) (P₂.obj (op Y))) → (fun (X : Type w') ↦ X) (P₂.obj (op X)))
          ((e : (a : P₁.obj (op Y)) → P₂.obj (op Y)) x : P₂.obj (op Y)) :
        (fun (X : Type w') ↦ X) (P₂.obj (op X)))
X : C
R : Presieve.{v₁, u₁} X
hP₁ : IsSheafFor P₁ R
x₂ : FamilyOfElements P₂ R
hx₂ : x₂.Compatible (R := R)
he' :
  ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : P₂.obj (op Y)),
    Eq.{w + 1} (α := P₁.obj (op X))
      ((Equiv.symm e : (a : P₂.obj (op X)) → P₁.obj (op X))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (P₂.map f.op) :
              (a : (fun (X : Type w') ↦ X) (P₂.obj (op Y))) → (fun (X : Type w') ↦ X) (P₂.obj (op X)))
            x) :
        P₁.obj (op X))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (P₁.map f.op) :
            (a : (fun (X : Type w) ↦ X) (P₁.obj (op Y))) → (fun (X : Type w) ↦ X) (P₁.obj (op X)))
          ((Equiv.symm e : (a : P₂.obj (op Y)) → P₁.obj (op Y)) x : P₁.obj (op Y)) :
        (fun (X : Type w) ↦ X) (P₁.obj (op X)))
x₁ : FamilyOfElements P₁ R :=
  fun (Y : C) (f : Y ⟶ X) (hf : R f) ↦ (Equiv.symm e : (a : P₂.obj (op Y)) → P₁.obj (op Y)) (x₂ f hf)
hx₁ : x₁.Compatible (R := R)
⊢ ∀ (t₂ : P₂.obj (op X)),
    x₂.IsAmalgamation (R := R) t₂ ↔ x₁.IsAmalgamation (R := R) ((Equiv.symm e : (a : P₂.obj (op X)) → P₁.obj (op X)) t₂)

Tactic:
have : ∀ (t₂ : P₂.obj (op X)),
      x₂.IsAmalgamation t₂ ↔ x₁.IsAmalgamation (e.symm t₂) := fun t₂ ↦ by
    simp only [FamilyOfElements.IsAmalgamation, x₁,
      ← he', EmbeddingLike.apply_eq_iff_eq]
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P₁ : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
P₂ : Functor.{v₁, w', u₁, w' + 1} Cᵒᵖ (Type w')
e : ⦃X : C⦄ → Equiv.{w + 1, w' + 1} (P₁.obj (op X)) (P₂.obj (op X))
he :
  ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : P₁.obj (op Y)),
    Eq.{w' + 1} (α := P₂.obj (op X))
      ((e : (a : P₁.obj (op X)) → P₂.obj (op X))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (P₁.map f.op) :
              (a : (fun (X : Type w) ↦ X) (P₁.obj (op Y))) → (fun (X : Type w) ↦ X) (P₁.obj (op X)))
            x) :
        P₂.obj (op X))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (P₂.map f.op) :
            (a : (fun (X : Type w') ↦ X) (P₂.obj (op Y))) → (fun (X : Type w') ↦ X) (P₂.obj (op X)))
          ((e : (a : P₁.obj (op Y)) → P₂.obj (op Y)) x : P₂.obj (op Y)) :
        (fun (X : Type w') ↦ X) (P₂.obj (op X)))
X : C
R : Presieve.{v₁, u₁} X
hP₁ : IsSheafFor P₁ R
x₂ : FamilyOfElements P₂ R
hx₂ : x₂.Compatible (R := R)
he' :
  ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : P₂.obj (op Y)),
    Eq.{w + 1} (α := P₁.obj (op X))
      ((Equiv.symm e : (a : P₂.obj (op X)) → P₁.obj (op X))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (P₂.map f.op) :
              (a : (fun (X : Type w') ↦ X) (P₂.obj (op Y))) → (fun (X : Type w') ↦ X) (P₂.obj (op X)))
            x) :
        P₁.obj (op X))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (P₁.map f.op) :
            (a : (fun (X : Type w) ↦ X) (P₁.obj (op Y))) → (fun (X : Type w) ↦ X) (P₁.obj (op X)))
          ((Equiv.symm e : (a : P₂.obj (op Y)) → P₁.obj (op Y)) x : P₁.obj (op Y)) :
        (fun (X : Type w) ↦ X) (P₁.obj (op X)))
x₁ : FamilyOfElements P₁ R :=
  fun (Y : C) (f : Y ⟶ X) (hf : R f) ↦ (Equiv.symm e : (a : P₂.obj (op Y)) → P₁.obj (op Y)) (x₂ f hf)
hx₁ : x₁.Compatible (R := R)
this :
  ∀ (t₂ : P₂.obj (op X)),
    x₂.IsAmalgamation (R := R) t₂ ↔ x₁.IsAmalgamation (R := R) ((Equiv.symm e : (a : P₂.obj (op X)) → P₁.obj (op X)) t₂)
⊢ ∃! t : P₂.obj (op X), x₂.IsAmalgamation (R := R) t

Tactic:
⟨e (hP₁.amalgamate x₁ hx₁), ?_, ?_⟩

Premises used: CategoryTheory.Presieve.IsSheafFor.amalgamate, ExistsUnique, And.intro, Exists.intro, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P₁ : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
P₂ : Functor.{v₁, w', u₁, w' + 1} Cᵒᵖ (Type w')
e : ⦃X : C⦄ → Equiv.{w + 1, w' + 1} (P₁.obj (op X)) (P₂.obj (op X))
he :
  ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : P₁.obj (op Y)),
    Eq.{w' + 1} (α := P₂.obj (op X))
      ((e : (a : P₁.obj (op X)) → P₂.obj (op X))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (P₁.map f.op) :
              (a : (fun (X : Type w) ↦ X) (P₁.obj (op Y))) → (fun (X : Type w) ↦ X) (P₁.obj (op X)))
            x) :
        P₂.obj (op X))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (P₂.map f.op) :
            (a : (fun (X : Type w') ↦ X) (P₂.obj (op Y))) → (fun (X : Type w') ↦ X) (P₂.obj (op X)))
          ((e : (a : P₁.obj (op Y)) → P₂.obj (op Y)) x : P₂.obj (op Y)) :
        (fun (X : Type w') ↦ X) (P₂.obj (op X)))
X : C
R : Presieve.{v₁, u₁} X
hP₁ : IsSheafFor P₁ R
x₂ : FamilyOfElements P₂ R
hx₂ : x₂.Compatible (R := R)
he' :
  ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : P₂.obj (op Y)),
    Eq.{w + 1} (α := P₁.obj (op X))
      ((Equiv.symm e : (a : P₂.obj (op X)) → P₁.obj (op X))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (P₂.map f.op) :
              (a : (fun (X : Type w') ↦ X) (P₂.obj (op Y))) → (fun (X : Type w') ↦ X) (P₂.obj (op X)))
            x) :
        P₁.obj (op X))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (P₁.map f.op) :
            (a : (fun (X : Type w) ↦ X) (P₁.obj (op Y))) → (fun (X : Type w) ↦ X) (P₁.obj (op X)))
          ((Equiv.symm e : (a : P₂.obj (op Y)) → P₁.obj (op Y)) x : P₁.obj (op Y)) :
        (fun (X : Type w) ↦ X) (P₁.obj (op X)))
x₁ : FamilyOfElements P₁ R :=
  fun (Y : C) (f : Y ⟶ X) (hf : R f) ↦ (Equiv.symm e : (a : P₂.obj (op Y)) → P₁.obj (op Y)) (x₂ f hf)
hx₁ : x₁.Compatible (R := R)
this :
  ∀ (t₂ : P₂.obj (op X)),
    x₂.IsAmalgamation (R := R) t₂ ↔ x₁.IsAmalgamation (R := R) ((Equiv.symm e : (a : P₂.obj (op X)) → P₁.obj (op X)) t₂)
refine_1 :
  (fun (t : P₂.obj (op X)) ↦ x₂.IsAmalgamation (R := R) t)
    ((e : (a : P₁.obj (op X)) → P₂.obj (op X)) (hP₁.amalgamate (R := R) x₁ hx₁))
refine_2 :
  ∀ (y : P₂.obj (op X)),
    (fun (t : P₂.obj (op X)) ↦ x₂.IsAmalgamation (R := R) t) y →
      y = (e : (a : P₁.obj (op X)) → P₂.obj (op X)) (hP₁.amalgamate (R := R) x₁ hx₁)
⊢ ∃! t : P₂.obj (op X), x₂.IsAmalgamation (R := R) t

Tactic:
refine ⟨e (hP₁.amalgamate x₁ hx₁), ?_, ?_⟩