-- Mathlib/CategoryTheory/Sites/IsSheafFor.lean
theorem isSheafFor_iff_yonedaSheafCondition {P : Cᵒᵖ ⥤ Type v₁} :
    IsSheafFor P (S : Presieve X) ↔ YonedaSheafCondition P S

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
S : Sieve X
P : Cᵒᵖ ⥤ Type v₁
⊢ (∀ (x : FamilyOfElements P S.arrows), x.Compatible → ∃! t, x.IsAmalgamation t) ↔
    ∀ (b : { x // x.Compatible }),
      ∃! g, (↑(natTransEquivCompatibleFamily (natTransEquivCompatibleFamily.symm b))).IsAmalgamation (yonedaEquiv g)

Tactic:
rw [Subtype.forall]

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
S : Sieve X
P : Cᵒᵖ ⥤ Type v₁
⊢ (∀ (x : FamilyOfElements P S.arrows), x.Compatible → ∃! t, x.IsAmalgamation t) ↔
    ∀ (a : FamilyOfElements P S.arrows) (b : a.Compatible),
      ∃! g,
        (↑(natTransEquivCompatibleFamily (natTransEquivCompatibleFamily.symm ⟨a, b⟩))).IsAmalgamation (yonedaEquiv g)

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
S : Sieve X
P : Cᵒᵖ ⥤ Type v₁
x : FamilyOfElements P S.arrows
hx : x.Compatible
⊢ (∃! t, x.IsAmalgamation t) ↔
    ∃! g, (↑(natTransEquivCompatibleFamily (natTransEquivCompatibleFamily.symm ⟨x, hx⟩))).IsAmalgamation (yonedaEquiv g)

Tactic:
simp [Equiv.existsUnique_congr_right]

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
S : Sieve X
P : Cᵒᵖ ⥤ Type v₁
⊢ IsSheafFor P S.arrows ↔ YonedaSheafCondition P S

Tactic:
rw [IsSheafFor, YonedaSheafCondition]

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
S : Sieve X
P : Cᵒᵖ ⥤ Type v₁
⊢ (∀ (x : FamilyOfElements P S.arrows), x.Compatible → ∃! t, x.IsAmalgamation t) ↔
    ∀ (f : S.functor ⟶ P), ∃! g, S.functorInclusion ≫ g = f

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
S : Sieve X
P : Cᵒᵖ ⥤ Type v₁
⊢ (∀ (x : FamilyOfElements P S.arrows), x.Compatible → ∃! t, x.IsAmalgamation t) ↔
    ∀ (f : S.functor ⟶ P), ∃! g, S.functorInclusion ≫ g = f

Tactic:
simp_rw [extension_iff_amalgamation]

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
S : Sieve X
P : Cᵒᵖ ⥤ Type v₁
⊢ (∀ (x : FamilyOfElements P S.arrows), x.Compatible → ∃! t, x.IsAmalgamation t) ↔
    ∀ (f : S.functor ⟶ P), ∃! g, (↑(natTransEquivCompatibleFamily f)).IsAmalgamation (yonedaEquiv g)

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
S : Sieve X
P : Cᵒᵖ ⥤ Type v₁
⊢ (∀ (x : FamilyOfElements P S.arrows), x.Compatible → ∃! t, x.IsAmalgamation t) ↔
    ∀ (f : S.functor ⟶ P), ∃! g, (↑(natTransEquivCompatibleFamily f)).IsAmalgamation (yonedaEquiv g)

Tactic:
rw [Equiv.forall_congr_left natTransEquivCompatibleFamily]

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
S : Sieve X
P : Cᵒᵖ ⥤ Type v₁
⊢ (∀ (x : FamilyOfElements P S.arrows), x.Compatible → ∃! t, x.IsAmalgamation t) ↔
    ∀ (b : { x // x.Compatible }),
      ∃! g, (↑(natTransEquivCompatibleFamily (natTransEquivCompatibleFamily.symm b))).IsAmalgamation (yonedaEquiv g)

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
S : Sieve X
P : Cᵒᵖ ⥤ Type v₁
⊢ (∀ (x : FamilyOfElements P S.arrows), x.Compatible → ∃! t, x.IsAmalgamation t) ↔
    ∀ (a : FamilyOfElements P S.arrows) (b : a.Compatible),
      ∃! g,
        (↑(natTransEquivCompatibleFamily (natTransEquivCompatibleFamily.symm ⟨a, b⟩))).IsAmalgamation (yonedaEquiv g)

Tactic:
exact forall₂_congr fun x hx ↦ by simp [Equiv.existsUnique_congr_right]

Result:
no goals