-- Mathlib/CategoryTheory/Sites/IsSheafFor.lean
theorem isSheafFor_arrows_iff : (ofArrows X π).IsSheafFor P ↔
    (∀ (x : (i : I) → P.obj (op (X i))), Arrows.Compatible P π x →
    ∃! t, ∀ i, P.map (π i).op t = x i)

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
⊢ IsSheafFor P (ofArrows X π) ↔
    ∀ (x : (i : I) → P.obj (op (X i))), Arrows.Compatible P π x → ∃! t, ∀ (i : I), P.map (π i).op t = x i

Tactic:
refine ⟨fun h x hx ↦ ?_, fun h x hx ↦ ?_⟩

Result:
case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
h : IsSheafFor P (ofArrows X π)
x : (i : I) → P.obj (op (X i))
hx : Arrows.Compatible P π x
⊢ ∃! t, ∀ (i : I), P.map (π i).op t = x i

case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
h : ∀ (x : (i : I) → P.obj (op (X i))), Arrows.Compatible P π x → ∃! t, ∀ (i : I), P.map (π i).op t = x i
x : FamilyOfElements P (ofArrows X π)
hx : x.Compatible
⊢ ∃! t, x.IsAmalgamation t

Proof state:
case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
h : ∀ (x : (i : I) → P.obj (op (X i))), Arrows.Compatible P π x → ∃! t, ∀ (i : I), P.map (π i).op t = x i
x : FamilyOfElements P (ofArrows X π)
hx : x.Compatible
⊢ ∃! t, x.IsAmalgamation t

Tactic:
obtain ⟨t, hA, ht⟩ := h (fun i ↦ x (π i) (ofArrows.mk _))
  (fun i j Z gi gj ↦ hx gi gj (ofArrows.mk _) (ofArrows.mk _))

Result:
case refine_2.intro.intro
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
h : ∀ (x : (i : I) → P.obj (op (X i))), Arrows.Compatible P π x → ∃! t, ∀ (i : I), P.map (π i).op t = x i
x : FamilyOfElements P (ofArrows X π)
hx : x.Compatible
t : P.obj (op B)
hA : ∀ (i : I), P.map (π i).op t = x (π i) ⋯
ht : ∀ (y : P.obj (op B)), (fun t => ∀ (i : I), P.map (π i).op t = x (π i) ⋯) y → y = t
⊢ ∃! t, x.IsAmalgamation t

Proof state:
case refine_2.intro.intro
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
h : ∀ (x : (i : I) → P.obj (op (X i))), Arrows.Compatible P π x → ∃! t, ∀ (i : I), P.map (π i).op t = x i
x : FamilyOfElements P (ofArrows X π)
hx : x.Compatible
t : P.obj (op B)
hA : ∀ (i : I), P.map (π i).op t = x (π i) ⋯
ht : ∀ (y : P.obj (op B)), (fun t => ∀ (i : I), P.map (π i).op t = x (π i) ⋯) y → y = t
⊢ ∃! t, x.IsAmalgamation t

Tactic:
exact ⟨t, fun Y f ⟨i⟩ ↦ hA i, fun y hy ↦ ht y (fun i ↦ hy (π i) (ofArrows.mk _))⟩

Result:
no goals

Proof state:
case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
h : IsSheafFor P (ofArrows X π)
x : (i : I) → P.obj (op (X i))
hx : Arrows.Compatible P π x
⊢ ∃! t, ∀ (i : I), P.map (π i).op t = x i

Tactic:
obtain ⟨t, ht₁, ht₂⟩ := h _ hx.familyOfElements_compatible

Result:
case refine_1.intro.intro
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
h : IsSheafFor P (ofArrows X π)
x : (i : I) → P.obj (op (X i))
hx : Arrows.Compatible P π x
t : P.obj (op B)
ht₁ : hx.familyOfElements.IsAmalgamation t
ht₂ : ∀ (y : P.obj (op B)), (fun t => hx.familyOfElements.IsAmalgamation t) y → y = t
⊢ ∃! t, ∀ (i : I), P.map (π i).op t = x i

Proof state:
case refine_1.intro.intro.refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
h : IsSheafFor P (ofArrows X π)
x : (i : I) → P.obj (op (X i))
hx : Arrows.Compatible P π x
t : P.obj (op B)
ht₁ : hx.familyOfElements.IsAmalgamation t
ht₂ : ∀ (y : P.obj (op B)), (fun t => hx.familyOfElements.IsAmalgamation t) y → y = t
i : I
⊢ P.map (π i).op t = x i

Tactic:
rw [ht₁ _ (ofArrows.mk i), hx.familyOfElements_ofArrows_mk]

Result:
no goals

Proof state:
case refine_1.intro.intro.refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
h : IsSheafFor P (ofArrows X π)
x : (i : I) → P.obj (op (X i))
hx : Arrows.Compatible P π x
t : P.obj (op B)
ht₁ : hx.familyOfElements.IsAmalgamation t
ht₂ : ∀ (y : P.obj (op B)), (fun t => hx.familyOfElements.IsAmalgamation t) y → y = t
t' : P.obj (op B)
ht' : (fun t => ∀ (i : I), P.map (π i).op t = x i) t'
x✝² : C
x✝¹ : x✝² ⟶ B
x✝ : ofArrows X π x✝¹
i : I
⊢ P.map (π i).op t' = hx.familyOfElements (π i) ⋯

Tactic:
rw [ht', hx.familyOfElements_ofArrows_mk]

Result:
no goals

Proof state:
case refine_1.intro.intro
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
h : IsSheafFor P (ofArrows X π)
x : (i : I) → P.obj (op (X i))
hx : Arrows.Compatible P π x
t : P.obj (op B)
ht₁ : hx.familyOfElements.IsAmalgamation t
ht₂ : ∀ (y : P.obj (op B)), (fun t => hx.familyOfElements.IsAmalgamation t) y → y = t
⊢ ∃! t, ∀ (i : I), P.map (π i).op t = x i

Tactic:
refine ⟨t, fun i ↦ ?_, fun t' ht' ↦ ht₂ _ fun _ _ ⟨i⟩ ↦ ?_⟩

Result:
case refine_1.intro.intro.refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
h : IsSheafFor P (ofArrows X π)
x : (i : I) → P.obj (op (X i))
hx : Arrows.Compatible P π x
t : P.obj (op B)
ht₁ : hx.familyOfElements.IsAmalgamation t
ht₂ : ∀ (y : P.obj (op B)), (fun t => hx.familyOfElements.IsAmalgamation t) y → y = t
i : I
⊢ P.map (π i).op t = x i

case refine_1.intro.intro.refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
h : IsSheafFor P (ofArrows X π)
x : (i : I) → P.obj (op (X i))
hx : Arrows.Compatible P π x
t : P.obj (op B)
ht₁ : hx.familyOfElements.IsAmalgamation t
ht₂ : ∀ (y : P.obj (op B)), (fun t => hx.familyOfElements.IsAmalgamation t) y → y = t
t' : P.obj (op B)
ht' : (fun t => ∀ (i : I), P.map (π i).op t = x i) t'
x✝² : C
x✝¹ : x✝² ⟶ B
x✝ : ofArrows X π x✝¹
i : I
⊢ P.map (π i).op t' = hx.familyOfElements (π i) ⋯