awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
J : GrothendieckTopology.{v₁, u₁} C
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
X : C
S : Sieve.{v₁, u₁} X
R : Presieve.{v₁, u₁} X
E : Aᵒᵖ
x : { x : FamilyOfElements (P ⋙ Functor.obj coyoneda E) S.arrows // x.SieveCompatible }
f f' : S.arrows.categoryᵒᵖ
g : f ⟶ f'
this :
  (↑x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows)
      (Over.Hom.left g.unop.hom ≫ (unop f).obj (P := fun (f : Over.{v₁, u₁} X) ↦ S.arrows f.hom).hom) ⋯ =
    (↑x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows)
        (unop f).obj (P := fun (f : Over.{v₁, u₁} X) ↦ S.arrows f.hom).hom ⋯ ≫
      P.map (Over.Hom.left g.unop.hom).op
h :
  Over.Hom.left g.unop.hom ≫ (unop f).obj (P := fun (f : Over.{v₁, u₁} X) ↦ S.arrows f.hom).hom =
    (unop f').obj (P := fun (f : Over.{v₁, u₁} X) ↦ S.arrows f.hom).hom
⊢ (↑x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows)
      (unop f').obj (P := fun (f : Over.{v₁, u₁} X) ↦ S.arrows f.hom).hom ⋯ =
    (↑x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows)
      (Over.Hom.left g.unop.hom ≫ (unop f).obj (P := fun (f : Over.{v₁, u₁} X) ↦ S.arrows f.hom).hom) ⋯

Tactic:
convert! rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
J : GrothendieckTopology.{v₁, u₁} C
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
X : C
S : Sieve.{v₁, u₁} X
R : Presieve.{v₁, u₁} X
E : Aᵒᵖ
x : { x : FamilyOfElements (P ⋙ Functor.obj coyoneda E) S.arrows // x.SieveCompatible }
f f' : S.arrows.categoryᵒᵖ
g : f ⟶ f'
this :
  (↑x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows)
      (Over.Hom.left g.unop.hom ≫ (unop f).obj (P := fun (f : Over.{v₁, u₁} X) ↦ S.arrows f.hom).hom) ⋯ =
    (↑x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows)
        (unop f).obj (P := fun (f : Over.{v₁, u₁} X) ↦ S.arrows f.hom).hom ⋯ ≫
      P.map (Over.Hom.left g.unop.hom).op
⊢ Over.Hom.left g.unop.hom ≫ (unop f).obj (P := fun (f : Over.{v₁, u₁} X) ↦ S.arrows f.hom).hom =
    (unop f').obj (P := fun (f : Over.{v₁, u₁} X) ↦ S.arrows f.hom).hom

Tactic:
simp only [Over.w]

Premises used: CategoryTheory.Over.w
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
X : C
S : Sieve.{v₁, u₁} X
dsimp :
  Nonempty (IsLimit (P.mapCone S.arrows.cocone.op)) ↔
    ∀ (E : Aᵒᵖ) (x : FamilyOfElements (P ⋙ Functor.obj coyoneda E) S.arrows),
      x.Compatible (R := S.arrows) → ∃! t : unop E ⟶ P.obj (op X), x.IsAmalgamation (R := S.arrows) t
⊢ Nonempty (IsLimit (P.mapCone S.arrows.cocone.op)) ↔ ∀ (E : Aᵒᵖ), IsSheafFor (P ⋙ Functor.obj coyoneda E) S.arrows

Tactic:
dsimp [IsSheafFor]

Premises used: CategoryTheory.Presieve.IsSheafFor
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
X : C
S : Sieve.{v₁, u₁} X
simp_rw :
  Nonempty (IsLimit (P.mapCone S.arrows.cocone.op)) ↔
    ∀ (E : Aᵒᵖ) (x : FamilyOfElements (P ⋙ Functor.obj coyoneda E) S.arrows),
      x.SieveCompatible → ∃! t : unop E ⟶ P.obj (op X), x.IsAmalgamation (R := S.arrows) t
⊢ Nonempty (IsLimit (P.mapCone S.arrows.cocone.op)) ↔
    ∀ (E : Aᵒᵖ) (x : FamilyOfElements (P ⋙ Functor.obj coyoneda E) S.arrows),
      x.Compatible (R := S.arrows) → ∃! t : unop E ⟶ P.obj (op X), x.IsAmalgamation (R := S.arrows) t

Tactic:
simp_rw [compatible_iff_sieveCompatible]

Premises used: CategoryTheory.Presieve.compatible_iff_sieveCompatible
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
X : C
S : Sieve.{v₁, u₁} X
rw :
  Nonempty ((X_1 : Cone (S.arrows.diagram.op ⋙ P)) → Unique (X_1 ⟶ P.mapCone S.arrows.cocone.op)) ↔
    ∀ (E : Aᵒᵖ) (x : FamilyOfElements (P ⋙ Functor.obj coyoneda E) S.arrows),
      x.SieveCompatible → ∃! t : unop E ⟶ P.obj (op X), x.IsAmalgamation (R := S.arrows) t
⊢ Nonempty (IsLimit (P.mapCone S.arrows.cocone.op)) ↔
    ∀ (E : Aᵒᵖ) (x : FamilyOfElements (P ⋙ Functor.obj coyoneda E) S.arrows),
      x.SieveCompatible → ∃! t : unop E ⟶ P.obj (op X), x.IsAmalgamation (R := S.arrows) t

Tactic:
rw [((Cone.isLimitEquivIsTerminal _).trans (isTerminalEquivUnique _ _)).nonempty_congr]

Premises used: Equiv.trans, CategoryTheory.Limits.Cone.isLimitEquivIsTerminal, Equiv.nonempty_congr, CategoryTheory.Limits.isTerminalEquivUnique
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
X : C
S : Sieve.{v₁, u₁} X
rw :
  (∀ (i : Cone (S.arrows.diagram.op ⋙ P)), Nonempty.{v₂ + 1} (Unique (i ⟶ P.mapCone S.arrows.cocone.op))) ↔
    ∀ (E : Aᵒᵖ) (x : FamilyOfElements (P ⋙ Functor.obj coyoneda E) S.arrows),
      x.SieveCompatible → ∃! t : unop E ⟶ P.obj (op X), x.IsAmalgamation (R := S.arrows) t
⊢ Nonempty ((X_1 : Cone (S.arrows.diagram.op ⋙ P)) → Unique (X_1 ⟶ P.mapCone S.arrows.cocone.op)) ↔
    ∀ (E : Aᵒᵖ) (x : FamilyOfElements (P ⋙ Functor.obj coyoneda E) S.arrows),
      x.SieveCompatible → ∃! t : unop E ⟶ P.obj (op X), x.IsAmalgamation (R := S.arrows) t

Tactic:
rw [Classical.nonempty_pi]

Premises used: Classical.nonempty_pi
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
X : C
S : Sieve.{v₁, u₁} X
mp :
  (∀ (i : Cone (S.arrows.diagram.op ⋙ P)), Nonempty.{v₂ + 1} (Unique (i ⟶ P.mapCone S.arrows.cocone.op))) →
    ∀ (E : Aᵒᵖ) (x : FamilyOfElements (P ⋙ Functor.obj coyoneda E) S.arrows),
      x.SieveCompatible → ∃! t : unop E ⟶ P.obj (op X), x.IsAmalgamation (R := S.arrows) t
mpr :
  (∀ (E : Aᵒᵖ) (x : FamilyOfElements (P ⋙ Functor.obj coyoneda E) S.arrows),
      x.SieveCompatible → ∃! t : unop E ⟶ P.obj (op X), x.IsAmalgamation (R := S.arrows) t) →
    ∀ (i : Cone (S.arrows.diagram.op ⋙ P)), Nonempty.{v₂ + 1} (Unique (i ⟶ P.mapCone S.arrows.cocone.op))
⊢ (∀ (i : Cone (S.arrows.diagram.op ⋙ P)), Nonempty.{v₂ + 1} (Unique (i ⟶ P.mapCone S.arrows.cocone.op))) ↔
    ∀ (E : Aᵒᵖ) (x : FamilyOfElements (P ⋙ Functor.obj coyoneda E) S.arrows),
      x.SieveCompatible → ∃! t : unop E ⟶ P.obj (op X), x.IsAmalgamation (R := S.arrows) t

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
X : C
S : Sieve.{v₁, u₁} X
hu : ∀ (i : Cone (S.arrows.diagram.op ⋙ P)), Nonempty.{v₂ + 1} (Unique (i ⟶ P.mapCone S.arrows.cocone.op))
E : Aᵒᵖ
x : FamilyOfElements (P ⋙ Functor.obj coyoneda E) S.arrows
hx : x.SieveCompatible
⊢ Nonempty.{v₂ + 1} (Unique (hx.cone ⟶ P.mapCone S.arrows.cocone.op))

Tactic:
specialize hu hx.cone

Premises used: CategoryTheory.Presieve.FamilyOfElements.SieveCompatible.cone
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
X : C
S : Sieve.{v₁, u₁} X
E : Aᵒᵖ
x : FamilyOfElements (P ⋙ Functor.obj coyoneda E) S.arrows
hx : x.SieveCompatible
hu : Nonempty.{v₂ + 1} (Unique (hx.cone ⟶ P.mapCone S.arrows.cocone.op))
⊢ Nonempty.{v₂ + 1} (Unique { t : (P ⋙ Functor.obj coyoneda E).obj (op X) // x.IsAmalgamation (R := S.arrows) t })

Tactic:
rw [(homEquivAmalgamation hx).uniqueCongr.nonempty_congr] at hu

Premises used: Equiv.uniqueCongr, CategoryTheory.Presheaf.homEquivAmalgamation, Equiv.nonempty_congr
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
X : C
S : Sieve.{v₁, u₁} X
E : Aᵒᵖ
x : FamilyOfElements (P ⋙ Functor.obj coyoneda E) S.arrows
hx : x.SieveCompatible
hu : Nonempty.{v₂ + 1} (Unique { t : (P ⋙ Functor.obj coyoneda E).obj (op X) // x.IsAmalgamation (R := S.arrows) t })
⊢ ∃! t : unop E ⟶ P.obj (op X), x.IsAmalgamation (R := S.arrows) t

Tactic:
(unique_subtype_iff_existsUnique _).1 hu

Premises used: unique_subtype_iff_existsUnique, Iff.mp
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
X : C
S : Sieve.{v₁, u₁} X
E : Aᵒᵖ
x : FamilyOfElements (P ⋙ Functor.obj coyoneda E) S.arrows
hx : x.SieveCompatible
hu : Nonempty.{v₂ + 1} (Unique { t : (P ⋙ Functor.obj coyoneda E).obj (op X) // x.IsAmalgamation (R := S.arrows) t })
⊢ ∃! t : unop E ⟶ P.obj (op X), x.IsAmalgamation (R := S.arrows) t

Tactic:
exact (unique_subtype_iff_existsUnique _).1 hu

Premises used: unique_subtype_iff_existsUnique, Iff.mp
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
X : C
S : Sieve.{v₁, u₁} X
h :
  ∀ (E : Aᵒᵖ) (x : FamilyOfElements (P ⋙ Functor.obj coyoneda E) S.arrows),
    x.SieveCompatible → ∃! t : unop E ⟶ P.obj (op X), x.IsAmalgamation (R := S.arrows) t
E : A
π : Functor.obj (Functor.const S.arrows.categoryᵒᵖ) E ⟶ S.arrows.diagram.op ⋙ P
eqv : (S.arrows.diagram.op ⋙ P).cones.obj (op E) ≃
  { x : FamilyOfElements (P ⋙ Functor.obj coyoneda (op E)) S.arrows // x.SieveCompatible } :=
  conesEquivSieveCompatibleFamily P S (op E)
mpr :
  Nonempty.{v₂ + 1}
    (Unique
      ({ pt := E, π := eqv.invFun (eqv.toFun π) : Cone (S.arrows.diagram.op ⋙ P) } ⟶ P.mapCone S.arrows.cocone.op))
⊢ Nonempty.{v₂ + 1} (Unique ({ pt := E, π := π : Cone (S.arrows.diagram.op ⋙ P) } ⟶ P.mapCone S.arrows.cocone.op))

Tactic:
rw [← eqv.left_inv π]

Premises used: Equiv.left_inv
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
X : C
S : Sieve.{v₁, u₁} X
h :
  ∀ (E : Aᵒᵖ) (x : FamilyOfElements (P ⋙ Functor.obj coyoneda E) S.arrows),
    x.SieveCompatible → ∃! t : unop E ⟶ P.obj (op X), x.IsAmalgamation (R := S.arrows) t
E : A
π : Functor.obj (Functor.const S.arrows.categoryᵒᵖ) E ⟶ S.arrows.diagram.op ⋙ P
eqv : (S.arrows.diagram.op ⋙ P).cones.obj (op E) ≃
  { x : FamilyOfElements (P ⋙ Functor.obj coyoneda (op E)) S.arrows // x.SieveCompatible } :=
  conesEquivSieveCompatibleFamily P S (op E)
mpr :
  Nonempty.{v₂ + 1}
    (Unique
      { t : (P ⋙ Functor.obj coyoneda (op E)).obj (op X) //
        IsAmalgamation (R := S.arrows)
          (↑((eqv :
                  (a : (S.arrows.diagram.op ⋙ P).cones.obj (op E)) →
                    { x : FamilyOfElements (P ⋙ coyoneda.obj (op E)) S.arrows // x.SieveCompatible })
                π) :
            FamilyOfElements (P ⋙ coyoneda.obj (op E)) S.arrows)
          t })
⊢ Nonempty.{v₂ + 1}
    (Unique
      ({ pt := E, π := eqv.invFun (eqv.toFun π) : Cone (S.arrows.diagram.op ⋙ P) } ⟶ P.mapCone S.arrows.cocone.op))

Tactic:
erw [(homEquivAmalgamation (eqv π).2).uniqueCongr.nonempty_congr]

Premises used: Equiv.uniqueCongr, CategoryTheory.Presheaf.homEquivAmalgamation, Equiv.nonempty_congr, DFunLike.coe, Subtype.property
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
X : C
S : Sieve.{v₁, u₁} X
h :
  ∀ (E : Aᵒᵖ) (x : FamilyOfElements (P ⋙ Functor.obj coyoneda E) S.arrows),
    x.SieveCompatible → ∃! t : unop E ⟶ P.obj (op X), x.IsAmalgamation (R := S.arrows) t
E : A
π : Functor.obj (Functor.const S.arrows.categoryᵒᵖ) E ⟶ S.arrows.diagram.op ⋙ P
eqv : (S.arrows.diagram.op ⋙ P).cones.obj (op E) ≃
  { x : FamilyOfElements (P ⋙ Functor.obj coyoneda (op E)) S.arrows // x.SieveCompatible } :=
  conesEquivSieveCompatibleFamily P S (op E)
mpr :
  ∃! a : (P ⋙ Functor.obj coyoneda (op E)).obj (op X),
    IsAmalgamation (R := S.arrows)
      (↑((eqv :
              (a : (S.arrows.diagram.op ⋙ P).cones.obj (op E)) →
                { x : FamilyOfElements (P ⋙ coyoneda.obj (op E)) S.arrows // x.SieveCompatible })
            π) :
        FamilyOfElements (P ⋙ coyoneda.obj (op E)) S.arrows)
      a
⊢ Nonempty.{v₂ + 1}
    (Unique
      { t : (P ⋙ Functor.obj coyoneda (op E)).obj (op X) //
        IsAmalgamation (R := S.arrows)
          (↑((eqv :
                  (a : (S.arrows.diagram.op ⋙ P).cones.obj (op E)) →
                    { x : FamilyOfElements (P ⋙ coyoneda.obj (op E)) S.arrows // x.SieveCompatible })
                π) :
            FamilyOfElements (P ⋙ coyoneda.obj (op E)) S.arrows)
          t })

Tactic:
rw [unique_subtype_iff_existsUnique]

Premises used: unique_subtype_iff_existsUnique
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
X : C
S : Sieve.{v₁, u₁} X
h :
  ∀ (E : Aᵒᵖ) (x : FamilyOfElements (P ⋙ Functor.obj coyoneda E) S.arrows),
    x.SieveCompatible → ∃! t : unop E ⟶ P.obj (op X), x.IsAmalgamation (R := S.arrows) t
E : A
π : Functor.obj (Functor.const S.arrows.categoryᵒᵖ) E ⟶ S.arrows.diagram.op ⋙ P
eqv : (S.arrows.diagram.op ⋙ P).cones.obj (op E) ≃
  { x : FamilyOfElements (P ⋙ Functor.obj coyoneda (op E)) S.arrows // x.SieveCompatible } :=
  conesEquivSieveCompatibleFamily P S (op E)
⊢ ∃! a : (P ⋙ Functor.obj coyoneda (op E)).obj (op X),
    IsAmalgamation (R := S.arrows)
      (↑((eqv :
              (a : (S.arrows.diagram.op ⋙ P).cones.obj (op E)) →
                { x : FamilyOfElements (P ⋙ coyoneda.obj (op E)) S.arrows // x.SieveCompatible })
            π) :
        FamilyOfElements (P ⋙ coyoneda.obj (op E)) S.arrows)
      a

Tactic:
h _ _ (eqv π).2

Premises used: DFunLike.coe, Subtype.property
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
X : C
S : Sieve.{v₁, u₁} X
h :
  ∀ (E : Aᵒᵖ) (x : FamilyOfElements (P ⋙ Functor.obj coyoneda E) S.arrows),
    x.SieveCompatible → ∃! t : unop E ⟶ P.obj (op X), x.IsAmalgamation (R := S.arrows) t
E : A
π : Functor.obj (Functor.const S.arrows.categoryᵒᵖ) E ⟶ S.arrows.diagram.op ⋙ P
eqv : (S.arrows.diagram.op ⋙ P).cones.obj (op E) ≃
  { x : FamilyOfElements (P ⋙ Functor.obj coyoneda (op E)) S.arrows // x.SieveCompatible } :=
  conesEquivSieveCompatibleFamily P S (op E)
⊢ ∃! a : (P ⋙ Functor.obj coyoneda (op E)).obj (op X),
    IsAmalgamation (R := S.arrows)
      (↑((eqv :
              (a : (S.arrows.diagram.op ⋙ P).cones.obj (op E)) →
                { x : FamilyOfElements (P ⋙ coyoneda.obj (op E)) S.arrows // x.SieveCompatible })
            π) :
        FamilyOfElements (P ⋙ coyoneda.obj (op E)) S.arrows)
      a

Tactic:
exact h _ _ (eqv π).2

Premises used: DFunLike.coe, Subtype.property
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
X : C
S : Sieve.{v₁, u₁} X
mp :
  (∀ (c : Cone (S.arrows.diagram.op ⋙ P)), Subsingleton.{v₂ + 1} (c ⟶ P.mapCone S.arrows.cocone.op)) →
    ∀ (E : Aᵒᵖ), IsSeparatedFor (P ⋙ Functor.obj coyoneda E) S.arrows
mpr :
  (∀ (E : Aᵒᵖ), IsSeparatedFor (P ⋙ Functor.obj coyoneda E) S.arrows) →
    ∀ (c : Cone (S.arrows.diagram.op ⋙ P)), Subsingleton.{v₂ + 1} (c ⟶ P.mapCone S.arrows.cocone.op)
⊢ (∀ (c : Cone (S.arrows.diagram.op ⋙ P)), Subsingleton.{v₂ + 1} (c ⟶ P.mapCone S.arrows.cocone.op)) ↔
    ∀ (E : Aᵒᵖ), IsSeparatedFor (P ⋙ Functor.obj coyoneda E) S.arrows

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
X : C
S : Sieve.{v₁, u₁} X
hs : ∀ (c : Cone (S.arrows.diagram.op ⋙ P)), Subsingleton.{v₂ + 1} (c ⟶ P.mapCone S.arrows.cocone.op)
E : Aᵒᵖ
x : FamilyOfElements (P ⋙ Functor.obj coyoneda E) S.arrows
t₁ t₂ : (P ⋙ Functor.obj coyoneda E).obj (op X)
h₁ : x.IsAmalgamation (R := S.arrows) t₁
h₂ : x.IsAmalgamation (R := S.arrows) t₂
⊢ x.Compatible (R := S.arrows)

Tactic:
have hx := is_compatible_of_exists_amalgamation x ⟨t₁, h₁⟩
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
X : C
S : Sieve.{v₁, u₁} X
hs : ∀ (c : Cone (S.arrows.diagram.op ⋙ P)), Subsingleton.{v₂ + 1} (c ⟶ P.mapCone S.arrows.cocone.op)
E : Aᵒᵖ
x : FamilyOfElements (P ⋙ Functor.obj coyoneda E) S.arrows
t₁ t₂ : (P ⋙ Functor.obj coyoneda E).obj (op X)
h₁ : x.IsAmalgamation (R := S.arrows) t₁
h₂ : x.IsAmalgamation (R := S.arrows) t₂
hx : x.Compatible (R := S.arrows)
⊢ x.SieveCompatible

Tactic:
rw [compatible_iff_sieveCompatible] at hx

Premises used: CategoryTheory.Presieve.compatible_iff_sieveCompatible
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
X : C
S : Sieve.{v₁, u₁} X
hs : ∀ (c : Cone (S.arrows.diagram.op ⋙ P)), Subsingleton.{v₂ + 1} (c ⟶ P.mapCone S.arrows.cocone.op)
E : Aᵒᵖ
x : FamilyOfElements (P ⋙ Functor.obj coyoneda E) S.arrows
t₁ t₂ : (P ⋙ Functor.obj coyoneda E).obj (op X)
h₁ : x.IsAmalgamation (R := S.arrows) t₁
h₂ : x.IsAmalgamation (R := S.arrows) t₂
hx : x.SieveCompatible
⊢ Subsingleton.{v₂ + 1} (hx.cone ⟶ P.mapCone S.arrows.cocone.op)

Tactic:
specialize hs hx.cone

Premises used: CategoryTheory.Presieve.FamilyOfElements.SieveCompatible.cone
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
X : C
S : Sieve.{v₁, u₁} X
E : Aᵒᵖ
x : FamilyOfElements (P ⋙ Functor.obj coyoneda E) S.arrows
t₁ t₂ : (P ⋙ Functor.obj coyoneda E).obj (op X)
h₁ : x.IsAmalgamation (R := S.arrows) t₁
h₂ : x.IsAmalgamation (R := S.arrows) t₂
hx : x.SieveCompatible
hs : Subsingleton.{v₂ + 1} (hx.cone ⟶ P.mapCone S.arrows.cocone.op)
⊢ ∀ (a b : hx.cone ⟶ P.mapCone S.arrows.cocone.op), a = b

Tactic:
rcases hs with ⟨hs⟩
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
X : C
S : Sieve.{v₁, u₁} X
E : Aᵒᵖ
x : FamilyOfElements (P ⋙ Functor.obj coyoneda E) S.arrows
t₁ t₂ : (P ⋙ Functor.obj coyoneda E).obj (op X)
h₁ : x.IsAmalgamation (R := S.arrows) t₁
h₂ : x.IsAmalgamation (R := S.arrows) t₂
hx : x.SieveCompatible
hs : ∀ (a b : hx.cone ⟶ P.mapCone S.arrows.cocone.op), a = b
⊢ t₁ = t₂

Tactic:
simpa only [Subtype.mk.injEq] using (show Subtype.mk t₁ h₁ = ⟨t₂, h₂⟩ from
      (homEquivAmalgamation hx).symm.injective (hs _ _))

Premises used: CategoryTheory.Presheaf.homEquivAmalgamation, Subtype.mk, Subtype.mk.injEq, Equiv.injective, Equiv.symm, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
X : C
S : Sieve.{v₁, u₁} X
h : ∀ (E : Aᵒᵖ), IsSeparatedFor (P ⋙ Functor.obj coyoneda E) S.arrows
E : A
π : Functor.obj (Functor.const S.arrows.categoryᵒᵖ) E ⟶ S.arrows.diagram.op ⋙ P
eqv : (S.arrows.diagram.op ⋙ P).cones.obj (op E) ≃
  { x : FamilyOfElements (P ⋙ Functor.obj coyoneda (op E)) S.arrows // x.SieveCompatible } :=
  conesEquivSieveCompatibleFamily P S (op E)
mpr : ∀ (a b : { pt := E, π := π : Cone (S.arrows.diagram.op ⋙ P) } ⟶ P.mapCone S.arrows.cocone.op), a = b
⊢ Subsingleton.{v₂ + 1} ({ pt := E, π := π : Cone (S.arrows.diagram.op ⋙ P) } ⟶ P.mapCone S.arrows.cocone.op)

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
X : C
S : Sieve.{v₁, u₁} X
h : ∀ (E : Aᵒᵖ), IsSeparatedFor (P ⋙ Functor.obj coyoneda E) S.arrows
E : A
π : Functor.obj (Functor.const S.arrows.categoryᵒᵖ) E ⟶ S.arrows.diagram.op ⋙ P
eqv : (S.arrows.diagram.op ⋙ P).cones.obj (op E) ≃
  { x : FamilyOfElements (P ⋙ Functor.obj coyoneda (op E)) S.arrows // x.SieveCompatible } :=
  conesEquivSieveCompatibleFamily P S (op E)
mpr :
  ∀ (a b : { pt := E, π := eqv.invFun (eqv.toFun π) : Cone (S.arrows.diagram.op ⋙ P) } ⟶ P.mapCone S.arrows.cocone.op),
    a = b
⊢ ∀ (a b : { pt := E, π := π : Cone (S.arrows.diagram.op ⋙ P) } ⟶ P.mapCone S.arrows.cocone.op), a = b

Tactic:
rw [← eqv.left_inv π]

Premises used: Equiv.left_inv
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
X : C
S : Sieve.{v₁, u₁} X
h : ∀ (E : Aᵒᵖ), IsSeparatedFor (P ⋙ Functor.obj coyoneda E) S.arrows
E : A
π : Functor.obj (Functor.const S.arrows.categoryᵒᵖ) E ⟶ S.arrows.diagram.op ⋙ P
eqv : (S.arrows.diagram.op ⋙ P).cones.obj (op E) ≃
  { x : FamilyOfElements (P ⋙ Functor.obj coyoneda (op E)) S.arrows // x.SieveCompatible } :=
  conesEquivSieveCompatibleFamily P S (op E)
f₁ f₂ : { pt := E, π := eqv.invFun (eqv.toFun π) : Cone (S.arrows.diagram.op ⋙ P) } ⟶ P.mapCone S.arrows.cocone.op
eqv' : (SieveCompatible.cone (E := op E) (x :=
      (↑((eqv :
              (a : (S.arrows.diagram.op ⋙ P).cones.obj (op E)) →
                { x : FamilyOfElements (P ⋙ coyoneda.obj (op E)) S.arrows // x.SieveCompatible })
            π) :
        FamilyOfElements (P ⋙ coyoneda.obj (op E)) S.arrows))
      ⋯ ⟶
    P.mapCone S.arrows.cocone.op) ≃
  { t : (P ⋙ Functor.obj coyoneda (op E)).obj (op X) //
    IsAmalgamation (R := S.arrows)
      (↑((eqv :
              (a : (S.arrows.diagram.op ⋙ P).cones.obj (op E)) →
                { x : FamilyOfElements (P ⋙ coyoneda.obj (op E)) S.arrows // x.SieveCompatible })
            π) :
        FamilyOfElements (P ⋙ coyoneda.obj (op E)) S.arrows)
      t } :=
  homEquivAmalgamation ⋯
⊢ IsAmalgamation.{v₂, v₁, u₁} (P := P ⋙ Functor.obj coyoneda (op E)) (R := S.arrows)
    (↑((eqv :
            (a : (S.arrows.diagram.op ⋙ P).cones.obj (op E)) →
              { x : FamilyOfElements (P ⋙ coyoneda.obj (op E)) S.arrows // x.SieveCompatible })
          π) :
      FamilyOfElements (P ⋙ coyoneda.obj (op E)) S.arrows)
    (↑((eqv' :
            (a : ⋯.cone ⟶ P.mapCone S.arrows.cocone.op) →
              { t : (P ⋙ coyoneda.obj (op E)).obj (op X) //
                (↑((eqv :
                            (a : (S.arrows.diagram.op ⋙ P).cones.obj (op E)) →
                              { x : FamilyOfElements (P ⋙ coyoneda.obj (op E)) S.arrows // x.SieveCompatible })
                          π) :
                      FamilyOfElements (P ⋙ coyoneda.obj (op E)) S.arrows).IsAmalgamation
                  t })
          f₁) :
      (P ⋙ coyoneda.obj (op E)).obj (op X))

Tactic:
(eqv' _).2

Premises used: DFunLike.coe, Subtype.property