-- Mathlib/CategoryTheory/Sites/IsSheafFor.lean
theorem extension_iff_amalgamation {P : Cᵒᵖ ⥤ Type v₁} (x : S.functor ⟶ P) (g : yoneda.obj X ⟶ P) :
    S.functorInclusion ≫ g = x ↔
      (natTransEquivCompatibleFamily x).1.IsAmalgamation (yonedaEquiv g)

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
S : Sieve X
P : Cᵒᵖ ⥤ Type v₁
x : S.functor ⟶ P
g : yoneda.obj X ⟶ P
⊢ S.functorInclusion ≫ g = x ↔ ∀ ⦃Y : C⦄ (f : Y ⟶ X) (h : S.arrows f), P.map f.op (yonedaEquiv g) = x.app (op Y) ⟨f, h⟩

Tactic:
constructor

Result:
case mp
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
S : Sieve X
P : Cᵒᵖ ⥤ Type v₁
x : S.functor ⟶ P
g : yoneda.obj X ⟶ P
⊢ S.functorInclusion ≫ g = x → ∀ ⦃Y : C⦄ (f : Y ⟶ X) (h : S.arrows f), P.map f.op (yonedaEquiv g) = x.app (op Y) ⟨f, h⟩

case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
S : Sieve X
P : Cᵒᵖ ⥤ Type v₁
x : S.functor ⟶ P
g : yoneda.obj X ⟶ P
⊢ (∀ ⦃Y : C⦄ (f : Y ⟶ X) (h : S.arrows f), P.map f.op (yonedaEquiv g) = x.app (op Y) ⟨f, h⟩) →
    S.functorInclusion ≫ g = x

Proof state:
case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
S : Sieve X
P : Cᵒᵖ ⥤ Type v₁
x : S.functor ⟶ P
g : yoneda.obj X ⟶ P
⊢ (∀ ⦃Y : C⦄ (f : Y ⟶ X) (h : S.arrows f), P.map f.op (yonedaEquiv g) = x.app (op Y) ⟨f, h⟩) →
    S.functorInclusion ≫ g = x

Tactic:
intro h

Result:
case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
S : Sieve X
P : Cᵒᵖ ⥤ Type v₁
x : S.functor ⟶ P
g : yoneda.obj X ⟶ P
h : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (h : S.arrows f), P.map f.op (yonedaEquiv g) = x.app (op Y) ⟨f, h⟩
⊢ S.functorInclusion ≫ g = x

Proof state:
case mp
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
S : Sieve X
P : Cᵒᵖ ⥤ Type v₁
g : yoneda.obj X ⟶ P
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ yonedaEquiv (yoneda.map f ≫ g) = (S.functorInclusion ≫ g).app (op Y) ⟨f, hf⟩

Tactic:
dsimp

Result:
case mp
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
S : Sieve X
P : Cᵒᵖ ⥤ Type v₁
g : yoneda.obj X ⟶ P
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ yonedaEquiv (yoneda.map f ≫ g) = g.app (op Y) f

Proof state:
case h.e'_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
S : Sieve X
P : Cᵒᵖ ⥤ Type v₁
x : S.functor ⟶ P
g : yoneda.obj X ⟶ P
h : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (h : S.arrows f), P.map f.op (yonedaEquiv g) = x.app (op Y) ⟨f, h⟩
Y : Cᵒᵖ
f : unop Y ⟶ X
hf : S.arrows f
⊢ g.app Y f = g.app Y (𝟙 (unop Y) ≫ f)

Tactic:
simp

Result:
no goals

Proof state:
case h.e'_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
S : Sieve X
P : Cᵒᵖ ⥤ Type v₁
x : S.functor ⟶ P
g : yoneda.obj X ⟶ P
h : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (h : S.arrows f), P.map f.op (yonedaEquiv g) = x.app (op Y) ⟨f, h⟩
Y : Cᵒᵖ
f : unop Y ⟶ X
hf : S.arrows f
⊢ (S.functorInclusion ≫ g).app Y ⟨f, hf⟩ = P.map f.op (yonedaEquiv g)

Tactic:
rw [yonedaEquiv_naturality]

Result:
case h.e'_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
S : Sieve X
P : Cᵒᵖ ⥤ Type v₁
x : S.functor ⟶ P
g : yoneda.obj X ⟶ P
h : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (h : S.arrows f), P.map f.op (yonedaEquiv g) = x.app (op Y) ⟨f, h⟩
Y : Cᵒᵖ
f : unop Y ⟶ X
hf : S.arrows f
⊢ (S.functorInclusion ≫ g).app Y ⟨f, hf⟩ = yonedaEquiv (yoneda.map f ≫ g)

Proof state:
case mpr.w.h.h.mk
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
S : Sieve X
P : Cᵒᵖ ⥤ Type v₁
x : S.functor ⟶ P
g : yoneda.obj X ⟶ P
h : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (h : S.arrows f), P.map f.op (yonedaEquiv g) = x.app (op Y) ⟨f, h⟩
Y : Cᵒᵖ
f : unop Y ⟶ X
hf : S.arrows f
⊢ (S.functorInclusion ≫ g).app Y ⟨f, hf⟩ = x.app Y ⟨f, hf⟩

Tactic:
convert h f hf

Result:
case h.e'_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
S : Sieve X
P : Cᵒᵖ ⥤ Type v₁
x : S.functor ⟶ P
g : yoneda.obj X ⟶ P
h : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (h : S.arrows f), P.map f.op (yonedaEquiv g) = x.app (op Y) ⟨f, h⟩
Y : Cᵒᵖ
f : unop Y ⟶ X
hf : S.arrows f
⊢ (S.functorInclusion ≫ g).app Y ⟨f, hf⟩ = P.map f.op (yonedaEquiv g)

Proof state:
case mp
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
S : Sieve X
P : Cᵒᵖ ⥤ Type v₁
g : yoneda.obj X ⟶ P
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ P.map f.op (yonedaEquiv g) = (S.functorInclusion ≫ g).app (op Y) ⟨f, hf⟩

Tactic:
rw [yonedaEquiv_naturality]

Result:
case mp
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
S : Sieve X
P : Cᵒᵖ ⥤ Type v₁
g : yoneda.obj X ⟶ P
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ yonedaEquiv (yoneda.map f ≫ g) = (S.functorInclusion ≫ g).app (op Y) ⟨f, hf⟩

Proof state:
case mp
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
S : Sieve X
P : Cᵒᵖ ⥤ Type v₁
g : yoneda.obj X ⟶ P
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ yonedaEquiv (yoneda.map f ≫ g) = g.app (op Y) f

Tactic:
simp [yonedaEquiv_apply]

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
S : Sieve X
P : Cᵒᵖ ⥤ Type v₁
x : S.functor ⟶ P
g : yoneda.obj X ⟶ P
⊢ S.functorInclusion ≫ g = x ↔ (↑(natTransEquivCompatibleFamily x)).IsAmalgamation (yonedaEquiv g)

Tactic:
change _ ↔ ∀ ⦃Y : C⦄ (f : Y ⟶ X) (h : S f), P.map f.op (yonedaEquiv g) = x.app (op Y) ⟨f, h⟩

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
S : Sieve X
P : Cᵒᵖ ⥤ Type v₁
x : S.functor ⟶ P
g : yoneda.obj X ⟶ P
⊢ S.functorInclusion ≫ g = x ↔ ∀ ⦃Y : C⦄ (f : Y ⟶ X) (h : S.arrows f), P.map f.op (yonedaEquiv g) = x.app (op Y) ⟨f, h⟩

Proof state:
case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
S : Sieve X
P : Cᵒᵖ ⥤ Type v₁
x : S.functor ⟶ P
g : yoneda.obj X ⟶ P
h : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (h : S.arrows f), P.map f.op (yonedaEquiv g) = x.app (op Y) ⟨f, h⟩
⊢ S.functorInclusion ≫ g = x

Tactic:
ext Y ⟨f, hf⟩

Result:
case mpr.w.h.h.mk
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
S : Sieve X
P : Cᵒᵖ ⥤ Type v₁
x : S.functor ⟶ P
g : yoneda.obj X ⟶ P
h : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (h : S.arrows f), P.map f.op (yonedaEquiv g) = x.app (op Y) ⟨f, h⟩
Y : Cᵒᵖ
f : unop Y ⟶ X
hf : S.arrows f
⊢ (S.functorInclusion ≫ g).app Y ⟨f, hf⟩ = x.app Y ⟨f, hf⟩

Proof state:
case h.e'_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
S : Sieve X
P : Cᵒᵖ ⥤ Type v₁
x : S.functor ⟶ P
g : yoneda.obj X ⟶ P
h : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (h : S.arrows f), P.map f.op (yonedaEquiv g) = x.app (op Y) ⟨f, h⟩
Y : Cᵒᵖ
f : unop Y ⟶ X
hf : S.arrows f
⊢ (S.functorInclusion ≫ g).app Y ⟨f, hf⟩ = yonedaEquiv (yoneda.map f ≫ g)

Tactic:
dsimp [yonedaEquiv]

Result:
case h.e'_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
S : Sieve X
P : Cᵒᵖ ⥤ Type v₁
x : S.functor ⟶ P
g : yoneda.obj X ⟶ P
h : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (h : S.arrows f), P.map f.op (yonedaEquiv g) = x.app (op Y) ⟨f, h⟩
Y : Cᵒᵖ
f : unop Y ⟶ X
hf : S.arrows f
⊢ g.app Y f = g.app Y (𝟙 (unop Y) ≫ f)

Proof state:
case mp
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
S : Sieve X
P : Cᵒᵖ ⥤ Type v₁
x : S.functor ⟶ P
g : yoneda.obj X ⟶ P
⊢ S.functorInclusion ≫ g = x → ∀ ⦃Y : C⦄ (f : Y ⟶ X) (h : S.arrows f), P.map f.op (yonedaEquiv g) = x.app (op Y) ⟨f, h⟩

Tactic:
rintro rfl Y f hf

Result:
case mp
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
S : Sieve X
P : Cᵒᵖ ⥤ Type v₁
g : yoneda.obj X ⟶ P
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ P.map f.op (yonedaEquiv g) = (S.functorInclusion ≫ g).app (op Y) ⟨f, hf⟩