-- Mathlib/CategoryTheory/Sites/Coherent/RegularSheaves.lean
lemma isSheafFor_regular_of_projective {X : C} (S : Presieve X) [S.regular] [Projective X]
    (F : Cᵒᵖ ⥤ Type*) : S.IsSheafFor F

Proof state:
case intro.intro.intro
C : Type u_1
inst✝² : Category.{u_5, u_1} C
X : C
inst✝¹ : Projective X
F : Cᵒᵖ ⥤ Type u_4
Y : C
f : Y ⟶ X
hf : EffectiveEpi f
inst✝ : (ofArrows (fun x => Y) fun x => f).regular
⊢ ∀ (x : Unit → F.obj (op Y)), Arrows.Compatible F (fun x => f) x → ∃! t, ∀ (i : Unit), F.map f.op t = x i

Tactic:
refine fun x hx ↦ ⟨F.map (Projective.factorThru (𝟙 _) f).op <| x (), fun _ ↦ ?_, fun y h ↦ ?_⟩

Result:
case intro.intro.intro.refine_1
C : Type u_1
inst✝² : Category.{u_5, u_1} C
X : C
inst✝¹ : Projective X
F : Cᵒᵖ ⥤ Type u_4
Y : C
f : Y ⟶ X
hf : EffectiveEpi f
inst✝ : (ofArrows (fun x => Y) fun x => f).regular
x : Unit → F.obj (op Y)
hx : Arrows.Compatible F (fun x => f) x
x✝ : Unit
⊢ F.map f.op (F.map (Projective.factorThru (𝟙 X) f).op (x ())) = x x✝

case intro.intro.intro.refine_2
C : Type u_1
inst✝² : Category.{u_5, u_1} C
X : C
inst✝¹ : Projective X
F : Cᵒᵖ ⥤ Type u_4
Y : C
f : Y ⟶ X
hf : EffectiveEpi f
inst✝ : (ofArrows (fun x => Y) fun x => f).regular
x : Unit → F.obj (op Y)
hx : Arrows.Compatible F (fun x => f) x
y : F.obj (op X)
h : (fun t => ∀ (i : Unit), F.map f.op t = x i) y
⊢ y = F.map (Projective.factorThru (𝟙 X) f).op (x ())

Proof state:
case intro.intro.intro
C : Type u_1
inst✝² : Category.{u_5, u_1} C
X : C
inst✝¹ : Projective X
F : Cᵒᵖ ⥤ Type u_4
Y : C
f : Y ⟶ X
hf : EffectiveEpi f
inst✝ : (ofArrows (fun x => Y) fun x => f).regular
⊢ IsSheafFor F (ofArrows (fun x => Y) fun x => f)

Tactic:
rw [isSheafFor_arrows_iff]

Result:
case intro.intro.intro
C : Type u_1
inst✝² : Category.{u_5, u_1} C
X : C
inst✝¹ : Projective X
F : Cᵒᵖ ⥤ Type u_4
Y : C
f : Y ⟶ X
hf : EffectiveEpi f
inst✝ : (ofArrows (fun x => Y) fun x => f).regular
⊢ ∀ (x : Unit → F.obj (op Y)), Arrows.Compatible F (fun x => f) x → ∃! t, ∀ (i : Unit), F.map f.op t = x i

Proof state:
case intro.intro.intro.refine_1
C : Type u_1
inst✝² : Category.{u_5, u_1} C
X : C
inst✝¹ : Projective X
F : Cᵒᵖ ⥤ Type u_4
Y : C
f : Y ⟶ X
hf : EffectiveEpi f
inst✝ : (ofArrows (fun x => Y) fun x => f).regular
x : Unit → F.obj (op Y)
hx : Arrows.Compatible F (fun x => f) x
x✝ : Unit
⊢ F.map f.op (F.map (Projective.factorThru (𝟙 X) f).op (x ())) = x x✝

Tactic:
simpa using (hx () () Y (𝟙 Y) (f ≫ (Projective.factorThru (𝟙 _) f)) (by simp)).symm

Result:
no goals

Proof state:
case intro.intro.intro.refine_2
C : Type u_1
inst✝² : Category.{u_5, u_1} C
X : C
inst✝¹ : Projective X
F : Cᵒᵖ ⥤ Type u_4
Y : C
f : Y ⟶ X
hf : EffectiveEpi f
inst✝ : (ofArrows (fun x => Y) fun x => f).regular
x : Unit → F.obj (op Y)
hx : Arrows.Compatible F (fun x => f) x
y : F.obj (op X)
h : (fun t => ∀ (i : Unit), F.map f.op t = x i) y
⊢ y = F.map (Projective.factorThru (𝟙 X) f).op (x ())

Tactic:
simp only [← h (), ← FunctorToTypes.map_comp_apply, ← op_comp, Projective.factorThru_comp,
  op_id, FunctorToTypes.map_id_apply]

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_5, u_1} C
X : C
S : Presieve X
inst✝¹ : S.regular
inst✝ : Projective X
F : Cᵒᵖ ⥤ Type u_4
⊢ IsSheafFor F S

Tactic:
obtain ⟨Y, f, rfl, hf⟩ := Presieve.regular.single_epi (R := S)

Result:
case intro.intro.intro
C : Type u_1
inst✝² : Category.{u_5, u_1} C
X : C
inst✝¹ : Projective X
F : Cᵒᵖ ⥤ Type u_4
Y : C
f : Y ⟶ X
hf : EffectiveEpi f
inst✝ : (ofArrows (fun x => Y) fun x => f).regular
⊢ IsSheafFor F (ofArrows (fun x => Y) fun x => f)

Proof state:
C : Type u_1
inst✝² : Category.{u_5, u_1} C
X : C
inst✝¹ : Projective X
F : Cᵒᵖ ⥤ Type u_4
Y : C
f : Y ⟶ X
hf : EffectiveEpi f
inst✝ : (ofArrows (fun x => Y) fun x => f).regular
x : Unit → F.obj (op Y)
hx : Arrows.Compatible F (fun x => f) x
x✝ : Unit
⊢ 𝟙 Y ≫ (fun x => f) () = (f ≫ Projective.factorThru (𝟙 X) f) ≫ (fun x => f) ()

Tactic:
simp

Result:
no goals