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)
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 : x₁.IsAmalgamation (R := R) (hP₁.amalgamate (R := R) x₁ hx₁)
⊢ x₂.IsAmalgamation (R := R) ((e : (a : P₁.obj (op X)) → P₂.obj (op X)) (hP₁.amalgamate (R := R) x₁ hx₁))

Tactic:
simp only [this, Equiv.symm_apply_apply]

Premises used: Equiv.symm_apply_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)
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₂)
⊢ x₁.IsAmalgamation (R := R) (hP₁.amalgamate (R := R) x₁ hx₁)

Tactic:
IsSheafFor.isAmalgamation hP₁ hx₁

Premises used: CategoryTheory.Presieve.IsSheafFor.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)
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₂)
⊢ x₁.IsAmalgamation (R := R) (hP₁.amalgamate (R := R) x₁ hx₁)

Tactic:
exact IsSheafFor.isAmalgamation hP₁ hx₁

Premises used: CategoryTheory.Presieve.IsSheafFor.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)
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)
ht₂ : x₂.IsAmalgamation (R := R) t₂
⊢ t₂ = (e : (a : P₁.obj (op X)) → P₂.obj (op X)) (hP₁.amalgamate (R := R) x₁ hx₁)

Tactic:
e.symm.injective ?_

Premises used: Equiv.injective, Equiv.symm
-- 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)
ht₂ : x₂.IsAmalgamation (R := R) t₂
refine_2 :
  Eq.{w + 1} (α := P₁.obj (op X)) ((Equiv.symm e : (a : P₂.obj (op X)) → P₁.obj (op X)) t₂ : P₁.obj (op X))
    ((Equiv.symm e : (a : P₂.obj (op X)) → P₁.obj (op X))
        ((e : (a : P₁.obj (op X)) → P₂.obj (op X)) (hP₁.amalgamate (R := R) x₁ hx₁)) :
      P₁.obj (op X))
⊢ t₂ = (e : (a : P₁.obj (op X)) → P₂.obj (op X)) (hP₁.amalgamate (R := R) x₁ hx₁)

Tactic:
refine e.symm.injective ?_

Premises used: Equiv.injective, Equiv.symm
-- 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)
ht₂ : x₂.IsAmalgamation (R := R) t₂
refine_2 : (Equiv.symm e : (a : P₂.obj (op X)) → P₁.obj (op X)) t₂ = hP₁.amalgamate (R := R) x₁ hx₁
⊢ Eq.{w + 1} (α := P₁.obj (op X)) ((Equiv.symm e : (a : P₂.obj (op X)) → P₁.obj (op X)) t₂ : P₁.obj (op X))
    ((Equiv.symm e : (a : P₂.obj (op X)) → P₁.obj (op X))
        ((e : (a : P₁.obj (op X)) → P₂.obj (op X)) (hP₁.amalgamate (R := R) x₁ hx₁)) :
      P₁.obj (op X))

Tactic:
simp only [Equiv.symm_apply_apply]

Premises used: Equiv.symm_apply_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)
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)
ht₂ : x₂.IsAmalgamation (R := R) t₂
⊢ x₁.IsAmalgamation (R := R) ((Equiv.symm e : (a : P₂.obj (op X)) → P₁.obj (op X)) t₂)

Tactic:
simpa only [this] using ht₂
-- 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)
ht₂ : x₂.IsAmalgamation (R := R) t₂
⊢ (Equiv.symm e : (a : P₂.obj (op X)) → P₁.obj (op X)) t₂ = hP₁.amalgamate (R := R) x₁ hx₁

Tactic:
exact hP₁.isSeparatedFor x₁ _ _ (by simpa only [this] using ht₂)
      (IsSheafFor.isAmalgamation hP₁ hx₁)

Premises used: CategoryTheory.Presieve.IsSheafFor.isAmalgamation, CategoryTheory.Presieve.IsSheafFor.isSeparatedFor
-- 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
⊢ IsSheafFor P₁ R ↔ IsSheafFor P₂ R

Tactic:
⟨fun h ↦ isSheafFor_of_nat_equiv _ he h,
      fun h ↦ isSheafFor_of_nat_equiv (fun _ ↦ (@e _).symm) ?_ h⟩

Premises used: CategoryTheory.Presieve.isSheafFor_of_nat_equiv, Iff.intro, Equiv.symm
-- 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
refine :
  ∀ (h : IsSheafFor P₂ R) ⦃X Y : C⦄ (f : X ⟶ Y) (x : P₂.obj (op Y)),
    Eq.{w + 1} (α := P₁.obj (op X))
      ((((fun (x : C) ↦ (Equiv.symm e : Equiv.{w' + 1, w + 1} (P₂.obj (op x)) (P₁.obj (op x)))) X :
              Equiv.{w' + 1, w + 1} (P₂.obj (op X)) (P₁.obj (op X))) :
            (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)))
          ((((fun (x : C) ↦ (Equiv.symm e : Equiv.{w' + 1, w + 1} (P₂.obj (op x)) (P₁.obj (op x)))) Y :
                  Equiv.{w' + 1, w + 1} (P₂.obj (op Y)) (P₁.obj (op Y))) :
                (a : P₂.obj (op Y)) → P₁.obj (op Y))
              x :
            P₁.obj (op Y)) :
        (fun (X : Type w) ↦ X) (P₁.obj (op X)))
⊢ IsSheafFor P₁ R ↔ IsSheafFor P₂ R

Tactic:
refine ⟨fun h ↦ isSheafFor_of_nat_equiv _ he h,
      fun h ↦ isSheafFor_of_nat_equiv (fun _ ↦ (@e _).symm) ?_ h⟩