awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
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
mp :
  (∀ (x : FamilyOfElements P R), x.Compatible (R := R) → ∃ (t : P.obj (op X)), x.IsAmalgamation (R := R) t) →
    ∀ (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), x.Compatible (R := R) → ∃ (t : P.obj (op X)), x.IsAmalgamation (R := R) t) ↔
    ∀ (x : FamilyOfElements P (generate R).arrows),
      x.Compatible (R := (generate R).arrows) → ∃ (t : P.obj (op X)), x.IsAmalgamation (R := (generate R).arrows) t
have mpr : (∀ (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), x.Compatible (R := R) → ∃ (t : P.obj (op X)), x.IsAmalgamation (R := R) t
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
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)), x.IsAmalgamation (R := (generate R).arrows) t
have apply : ∀ (a : P.obj (op X)),
  (FamilyOfElements.restrict (R₁ := R) (R₂ := (generate R).arrows) sorry x).IsAmalgamation (R := R) a →
    x.IsAmalgamation (R := (generate R).arrows) a
Tactic: apply Exists.imp _ (q _ (hx.restrict (le_generate R)))
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
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)), x.IsAmalgamation (R := R) t
have apply : ∀ (a : P.obj (op X)), x.sieveExtend (R := R).IsAmalgamation (R := (generate R).arrows) a → x.IsAmalgamation (R := R) a
Tactic: apply Exists.imp _ (q _ hx.sieveExtend)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
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
have refine_1 : (fun (t : P.obj (op X)) ↦ x.IsAmalgamation (R := singleton (𝟙 X)) t) (x (𝟙 X) sorry)
Tactic: refine ⟨x _ (Presieve.singleton_self _), ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
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) ⋯)
⊢ ∃! t : P.obj (op X), x.IsAmalgamation (R := singleton (𝟙 X)) t
have refine_2 : ∀ (y : P.obj (op X)), (fun (t : P.obj (op X)) ↦ x.IsAmalgamation (R := singleton (𝟙 X)) t) y → y = x (𝟙 X) sorry
Tactic: refine ⟨x _ (Presieve.singleton_self _), ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
⊢ IsSheafFor (X := X) P ⊤
have rw : IsSheafFor P (arrows (generate (singleton (𝟙 X))))
Tactic: rw [← arrows_top, ← generate_of_singleton_isSplitEpi (𝟙 X)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
⊢ IsSheafFor P (arrows (generate (singleton (𝟙 X))))
have rw : IsSheafFor P (singleton (𝟙 X))
Tactic: rw [← isSheafFor_iff_generate]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (hypothesis)
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)
⊢ ∃! t : P₂.obj (op X), x₂.IsAmalgamation (R := R) t
have 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)))
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])
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (hypothesis)
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)
⊢ ∃! t : P₂.obj (op X), x₂.IsAmalgamation (R := R) t
have hx₁ : 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₁])
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (hypothesis)
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
have 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₂)
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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
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
have 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₁))
Tactic: refine ⟨e (hP₁.amalgamate x₁ hx₁), ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
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₁))
⊢ ∃! t : P₂.obj (op X), x₂.IsAmalgamation (R := R) t
have 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₁)
Tactic: refine ⟨e (hP₁.amalgamate x₁ hx₁), ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
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) ((e : (a : P₁.obj (op X)) → P₂.obj (op X)) (hP₁.amalgamate (R := R) x₁ hx₁))
have refine_1 : x₁.IsAmalgamation (R := R) (hP₁.amalgamate (R := R) x₁ hx₁)
Tactic: simp only [this, Equiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
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₁)
have 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))
Tactic: refine e.symm.injective ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
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₂
⊢ 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))
have refine_2 : (Equiv.symm e : (a : P₂.obj (op X)) → P₁.obj (op X)) t₂ = hP₁.amalgamate (R := R) x₁ hx₁
Tactic: simp only [Equiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
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
have 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)))
Tactic: refine ⟨fun h ↦ isSheafFor_of_nat_equiv _ he h,
      fun h ↦ isSheafFor_of_nat_equiv (fun _ ↦ (@e _).symm) ?_ h⟩