-- Mathlib/CategoryTheory/Sites/Sheaf.lean
theorem subsingleton_iff_isSeparatedFor :
    (∀ c, Subsingleton (c ⟶ P.mapCone S.arrows.cocone.op)) ↔
      ∀ E : Aᵒᵖ, IsSeparatedFor (P ⋙ coyoneda.obj E) S.arrows

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
⊢ (∀ (c : Cone (S.arrows.diagram.op ⋙ P)), Subsingleton (c ⟶ P.mapCone S.arrows.cocone.op)) ↔
    ∀ (E : Aᵒᵖ), IsSeparatedFor (P ⋙ coyoneda.obj E) S.arrows

Tactic:
constructor

Result:
case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
⊢ (∀ (c : Cone (S.arrows.diagram.op ⋙ P)), Subsingleton (c ⟶ P.mapCone S.arrows.cocone.op)) →
    ∀ (E : Aᵒᵖ), IsSeparatedFor (P ⋙ coyoneda.obj E) S.arrows

case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
⊢ (∀ (E : Aᵒᵖ), IsSeparatedFor (P ⋙ coyoneda.obj E) S.arrows) →
    ∀ (c : Cone (S.arrows.diagram.op ⋙ P)), Subsingleton (c ⟶ P.mapCone S.arrows.cocone.op)

Proof state:
case mp.intro
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
E : Aᵒᵖ
x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows
t₁ t₂ : (P ⋙ coyoneda.obj E).obj (op X)
h₁ : x.IsAmalgamation t₁
h₂ : x.IsAmalgamation 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 _ _))

Result:
no goals

Proof state:
case mpr.mk.allEq
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
h : ∀ (E : Aᵒᵖ), IsSeparatedFor (P ⋙ coyoneda.obj E) S.arrows
E : A
π : (Functor.const S.arrows.categoryᵒᵖ).obj E ⟶ S.arrows.diagram.op ⋙ P
eqv : (S.arrows.diagram.op ⋙ P).cones.obj (op E) ≃ { x // x.SieveCompatible } :=
  conesEquivSieveCompatibleFamily P S (op E)
f₁ f₂ : { pt := E, π := eqv.invFun (eqv.toFun π) } ⟶ P.mapCone S.arrows.cocone.op
eqv' : (⋯.cone ⟶ P.mapCone S.arrows.cocone.op) ≃ { t // (↑(eqv π)).IsAmalgamation t } := homEquivAmalgamation ⋯
⊢ f₁ = f₂

Tactic:
apply eqv'.injective

Result:
case mpr.mk.allEq.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
h : ∀ (E : Aᵒᵖ), IsSeparatedFor (P ⋙ coyoneda.obj E) S.arrows
E : A
π : (Functor.const S.arrows.categoryᵒᵖ).obj E ⟶ S.arrows.diagram.op ⋙ P
eqv : (S.arrows.diagram.op ⋙ P).cones.obj (op E) ≃ { x // x.SieveCompatible } :=
  conesEquivSieveCompatibleFamily P S (op E)
f₁ f₂ : { pt := E, π := eqv.invFun (eqv.toFun π) } ⟶ P.mapCone S.arrows.cocone.op
eqv' : (⋯.cone ⟶ P.mapCone S.arrows.cocone.op) ≃ { t // (↑(eqv π)).IsAmalgamation t } := homEquivAmalgamation ⋯
⊢ eqv' f₁ = eqv' f₂

Proof state:
case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
hs : ∀ (c : Cone (S.arrows.diagram.op ⋙ P)), Subsingleton (c ⟶ P.mapCone S.arrows.cocone.op)
E : Aᵒᵖ
x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows
t₁ t₂ : (P ⋙ coyoneda.obj E).obj (op X)
h₁ : x.IsAmalgamation t₁
h₂ : x.IsAmalgamation t₂
hx : x.SieveCompatible
⊢ t₁ = t₂

Tactic:
specialize hs hx.cone

Result:
case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
E : Aᵒᵖ
x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows
t₁ t₂ : (P ⋙ coyoneda.obj E).obj (op X)
h₁ : x.IsAmalgamation t₁
h₂ : x.IsAmalgamation t₂
hx : x.SieveCompatible
hs : Subsingleton (hx.cone ⟶ P.mapCone S.arrows.cocone.op)
⊢ t₁ = t₂

Proof state:
case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
⊢ (∀ (E : Aᵒᵖ), IsSeparatedFor (P ⋙ coyoneda.obj E) S.arrows) →
    ∀ (c : Cone (S.arrows.diagram.op ⋙ P)), Subsingleton (c ⟶ P.mapCone S.arrows.cocone.op)

Tactic:
rintro h ⟨E, π⟩

Result:
case mpr.mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
h : ∀ (E : Aᵒᵖ), IsSeparatedFor (P ⋙ coyoneda.obj E) S.arrows
E : A
π : (Functor.const S.arrows.categoryᵒᵖ).obj E ⟶ S.arrows.diagram.op ⋙ P
⊢ Subsingleton ({ pt := E, π := π } ⟶ P.mapCone S.arrows.cocone.op)

Proof state:
case mpr.mk.allEq.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
h : ∀ (E : Aᵒᵖ), IsSeparatedFor (P ⋙ coyoneda.obj E) S.arrows
E : A
π : (Functor.const S.arrows.categoryᵒᵖ).obj E ⟶ S.arrows.diagram.op ⋙ P
eqv : (S.arrows.diagram.op ⋙ P).cones.obj (op E) ≃ { x // x.SieveCompatible } :=
  conesEquivSieveCompatibleFamily P S (op E)
f₁ f₂ : { pt := E, π := eqv.invFun (eqv.toFun π) } ⟶ P.mapCone S.arrows.cocone.op
eqv' : (⋯.cone ⟶ P.mapCone S.arrows.cocone.op) ≃ { t // (↑(eqv π)).IsAmalgamation t } := homEquivAmalgamation ⋯
⊢ ↑(eqv' f₁) = ↑(eqv' f₂)

Tactic:
apply h _ (eqv π).1 <;> exact (eqv' _).2

Result:
no goals

Proof state:
case mpr.mk.allEq
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
h : ∀ (E : Aᵒᵖ), IsSeparatedFor (P ⋙ coyoneda.obj E) S.arrows
E : A
π : (Functor.const S.arrows.categoryᵒᵖ).obj E ⟶ S.arrows.diagram.op ⋙ P
eqv : (S.arrows.diagram.op ⋙ P).cones.obj (op E) ≃ { x // x.SieveCompatible } :=
  conesEquivSieveCompatibleFamily P S (op E)
⊢ ∀ (a b : { pt := E, π := eqv.invFun (eqv.toFun π) } ⟶ P.mapCone S.arrows.cocone.op), a = b

Tactic:
intro f₁ f₂

Result:
case mpr.mk.allEq
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
h : ∀ (E : Aᵒᵖ), IsSeparatedFor (P ⋙ coyoneda.obj E) S.arrows
E : A
π : (Functor.const S.arrows.categoryᵒᵖ).obj E ⟶ S.arrows.diagram.op ⋙ P
eqv : (S.arrows.diagram.op ⋙ P).cones.obj (op E) ≃ { x // x.SieveCompatible } :=
  conesEquivSieveCompatibleFamily P S (op E)
f₁ f₂ : { pt := E, π := eqv.invFun (eqv.toFun π) } ⟶ P.mapCone S.arrows.cocone.op
⊢ f₁ = f₂

Proof state:
case mpr.mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
h : ∀ (E : Aᵒᵖ), IsSeparatedFor (P ⋙ coyoneda.obj E) S.arrows
E : A
π : (Functor.const S.arrows.categoryᵒᵖ).obj E ⟶ S.arrows.diagram.op ⋙ P
⊢ Subsingleton ({ pt := E, π := π } ⟶ P.mapCone S.arrows.cocone.op)

Tactic:
let eqv := conesEquivSieveCompatibleFamily P S (op E)

Result:
case mpr.mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
h : ∀ (E : Aᵒᵖ), IsSeparatedFor (P ⋙ coyoneda.obj E) S.arrows
E : A
π : (Functor.const S.arrows.categoryᵒᵖ).obj E ⟶ S.arrows.diagram.op ⋙ P
eqv : (S.arrows.diagram.op ⋙ P).cones.obj (op E) ≃ { x // x.SieveCompatible } :=
  conesEquivSieveCompatibleFamily P S (op E)
⊢ Subsingleton ({ pt := E, π := π } ⟶ P.mapCone S.arrows.cocone.op)

Proof state:
case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
hs : ∀ (c : Cone (S.arrows.diagram.op ⋙ P)), Subsingleton (c ⟶ P.mapCone S.arrows.cocone.op)
E : Aᵒᵖ
x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows
t₁ t₂ : (P ⋙ coyoneda.obj E).obj (op X)
h₁ : x.IsAmalgamation t₁
h₂ : x.IsAmalgamation t₂
hx : x.Compatible
⊢ t₁ = t₂

Tactic:
rw [compatible_iff_sieveCompatible] at hx

Result:
case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
hs : ∀ (c : Cone (S.arrows.diagram.op ⋙ P)), Subsingleton (c ⟶ P.mapCone S.arrows.cocone.op)
E : Aᵒᵖ
x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows
t₁ t₂ : (P ⋙ coyoneda.obj E).obj (op X)
h₁ : x.IsAmalgamation t₁
h₂ : x.IsAmalgamation t₂
hx : x.SieveCompatible
⊢ t₁ = t₂