-- Mathlib/CategoryTheory/Sites/Coherent/RegularSheaves.lean
theorem equalizerCondition_precomp_of_preservesPullback (P : Cᵒᵖ ⥤ D) (F : E ⥤ C)
    [∀ {X B} (π : X ⟶ B) [EffectiveEpi π], PreservesLimit (cospan π π) F]
    [F.PreservesEffectiveEpis] (hP : EqualizerCondition P) : EqualizerCondition (F.op ⋙ P)

Proof state:
case refine_2
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁵ : Category.{u_4, u_1} C
inst✝⁴ : Category.{u_5, u_2} D
inst✝³ : Category.{u_6, u_3} E
P : Cᵒᵖ ⥤ D
F : E ⥤ C
inst✝² : ∀ {X B : E} (π : X ⟶ B) [inst : EffectiveEpi π], PreservesLimit (cospan π π) F
inst✝¹ : F.PreservesEffectiveEpis
hP : EqualizerCondition P
X B : E
π : X ⟶ B
inst✝ : EffectiveEpi π
c : PullbackCone π π
hc : IsLimit c
h : P.map (F.map π).op = (F.op ⋙ P).map π.op
⊢ IsLimit (Fork.ofι (P.map (F.map π).op) ⋯)

Tactic:
refine (hP (F.map π) (PullbackCone.mk (F.map c.fst) (F.map c.snd) ?_) ?_).some

Result:
case refine_2.refine_1
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁵ : Category.{u_4, u_1} C
inst✝⁴ : Category.{u_5, u_2} D
inst✝³ : Category.{u_6, u_3} E
P : Cᵒᵖ ⥤ D
F : E ⥤ C
inst✝² : ∀ {X B : E} (π : X ⟶ B) [inst : EffectiveEpi π], PreservesLimit (cospan π π) F
inst✝¹ : F.PreservesEffectiveEpis
hP : EqualizerCondition P
X B : E
π : X ⟶ B
inst✝ : EffectiveEpi π
c : PullbackCone π π
hc : IsLimit c
h : P.map (F.map π).op = (F.op ⋙ P).map π.op
⊢ F.map c.fst ≫ F.map π = F.map c.snd ≫ F.map π

case refine_2.refine_2
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁵ : Category.{u_4, u_1} C
inst✝⁴ : Category.{u_5, u_2} D
inst✝³ : Category.{u_6, u_3} E
P : Cᵒᵖ ⥤ D
F : E ⥤ C
inst✝² : ∀ {X B : E} (π : X ⟶ B) [inst : EffectiveEpi π], PreservesLimit (cospan π π) F
inst✝¹ : F.PreservesEffectiveEpis
hP : EqualizerCondition P
X B : E
π : X ⟶ B
inst✝ : EffectiveEpi π
c : PullbackCone π π
hc : IsLimit c
h : P.map (F.map π).op = (F.op ⋙ P).map π.op
⊢ IsLimit (PullbackCone.mk (F.map c.fst) (F.map c.snd) ?refine_2.refine_1)

Proof state:
case refine_2.refine_1
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁵ : Category.{u_4, u_1} C
inst✝⁴ : Category.{u_5, u_2} D
inst✝³ : Category.{u_6, u_3} E
P : Cᵒᵖ ⥤ D
F : E ⥤ C
inst✝² : ∀ {X B : E} (π : X ⟶ B) [inst : EffectiveEpi π], PreservesLimit (cospan π π) F
inst✝¹ : F.PreservesEffectiveEpis
hP : EqualizerCondition P
X B : E
π : X ⟶ B
inst✝ : EffectiveEpi π
c : PullbackCone π π
hc : IsLimit c
h : P.map (F.map π).op = (F.op ⋙ P).map π.op
⊢ F.map c.fst ≫ F.map π = F.map c.snd ≫ F.map π

Tactic:
simp only [← map_comp, c.condition]

Result:
no goals

Proof state:
case refine_2.refine_2
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁵ : Category.{u_4, u_1} C
inst✝⁴ : Category.{u_5, u_2} D
inst✝³ : Category.{u_6, u_3} E
P : Cᵒᵖ ⥤ D
F : E ⥤ C
inst✝² : ∀ {X B : E} (π : X ⟶ B) [inst : EffectiveEpi π], PreservesLimit (cospan π π) F
inst✝¹ : F.PreservesEffectiveEpis
hP : EqualizerCondition P
X B : E
π : X ⟶ B
inst✝ : EffectiveEpi π
c : PullbackCone π π
hc : IsLimit c
h : P.map (F.map π).op = (F.op ⋙ P).map π.op
⊢ IsLimit (PullbackCone.mk (F.map c.fst) (F.map c.snd) ⋯)

Tactic:
exact (isLimitMapConePullbackConeEquiv F c.condition)
  (isLimitOfPreserves F (hc.ofIsoLimit (PullbackCone.ext (Iso.refl _) (by simp) (by simp))))

Result:
no goals

Proof state:
case refine_1
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁵ : Category.{u_4, u_1} C
inst✝⁴ : Category.{u_5, u_2} D
inst✝³ : Category.{u_6, u_3} E
P : Cᵒᵖ ⥤ D
F : E ⥤ C
inst✝² : ∀ {X B : E} (π : X ⟶ B) [inst : EffectiveEpi π], PreservesLimit (cospan π π) F
inst✝¹ : F.PreservesEffectiveEpis
hP : EqualizerCondition P
X B : E
π : X ⟶ B
inst✝ : EffectiveEpi π
c : PullbackCone π π
hc : IsLimit c
h : P.map (F.map π).op = (F.op ⋙ P).map π.op
⊢ P.map (F.map π).op ≫ (F.op ⋙ P).map c.fst.op = P.map (F.map π).op ≫ (F.op ⋙ P).map c.snd.op

Tactic:
simp only [Functor.comp_map, op_map, Quiver.Hom.unop_op, ← map_comp, ← op_comp, c.condition]

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁵ : Category.{u_4, u_1} C
inst✝⁴ : Category.{u_5, u_2} D
inst✝³ : Category.{u_6, u_3} E
P : Cᵒᵖ ⥤ D
F : E ⥤ C
inst✝² : ∀ {X B : E} (π : X ⟶ B) [inst : EffectiveEpi π], PreservesLimit (cospan π π) F
inst✝¹ : F.PreservesEffectiveEpis
hP : EqualizerCondition P
X B : E
π : X ⟶ B
inst✝ : EffectiveEpi π
c : PullbackCone π π
hc : IsLimit c
h : P.map (F.map π).op = (F.op ⋙ P).map π.op
⊢ Nonempty (IsLimit (Fork.ofι ((F.op ⋙ P).map π.op) ⋯))

Tactic:
refine ⟨(IsLimit.equivIsoLimit (ForkOfι.ext ?_ _ h)) ?_⟩

Result:
case refine_1
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁵ : Category.{u_4, u_1} C
inst✝⁴ : Category.{u_5, u_2} D
inst✝³ : Category.{u_6, u_3} E
P : Cᵒᵖ ⥤ D
F : E ⥤ C
inst✝² : ∀ {X B : E} (π : X ⟶ B) [inst : EffectiveEpi π], PreservesLimit (cospan π π) F
inst✝¹ : F.PreservesEffectiveEpis
hP : EqualizerCondition P
X B : E
π : X ⟶ B
inst✝ : EffectiveEpi π
c : PullbackCone π π
hc : IsLimit c
h : P.map (F.map π).op = (F.op ⋙ P).map π.op
⊢ P.map (F.map π).op ≫ (F.op ⋙ P).map c.fst.op = P.map (F.map π).op ≫ (F.op ⋙ P).map c.snd.op

case refine_2
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁵ : Category.{u_4, u_1} C
inst✝⁴ : Category.{u_5, u_2} D
inst✝³ : Category.{u_6, u_3} E
P : Cᵒᵖ ⥤ D
F : E ⥤ C
inst✝² : ∀ {X B : E} (π : X ⟶ B) [inst : EffectiveEpi π], PreservesLimit (cospan π π) F
inst✝¹ : F.PreservesEffectiveEpis
hP : EqualizerCondition P
X B : E
π : X ⟶ B
inst✝ : EffectiveEpi π
c : PullbackCone π π
hc : IsLimit c
h : P.map (F.map π).op = (F.op ⋙ P).map π.op
⊢ IsLimit (Fork.ofι (P.map (F.map π).op) ?refine_1)

Proof state:
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁵ : Category.{u_4, u_1} C
inst✝⁴ : Category.{u_5, u_2} D
inst✝³ : Category.{u_6, u_3} E
P : Cᵒᵖ ⥤ D
F : E ⥤ C
inst✝² : ∀ {X B : E} (π : X ⟶ B) [inst : EffectiveEpi π], PreservesLimit (cospan π π) F
inst✝¹ : F.PreservesEffectiveEpis
hP : EqualizerCondition P
X B : E
π : X ⟶ B
inst✝ : EffectiveEpi π
c : PullbackCone π π
hc : IsLimit c
⊢ P.map (F.map π).op = (F.op ⋙ P).map π.op

Tactic:
simp

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_5, u_2} D
inst✝² : Category.{u_6, u_3} E
P : Cᵒᵖ ⥤ D
F : E ⥤ C
inst✝¹ : ∀ {X B : E} (π : X ⟶ B) [inst : EffectiveEpi π], PreservesLimit (cospan π π) F
inst✝ : F.PreservesEffectiveEpis
hP : EqualizerCondition P
⊢ EqualizerCondition (F.op ⋙ P)

Tactic:
intro X B π _ c hc

Result:
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁵ : Category.{u_4, u_1} C
inst✝⁴ : Category.{u_5, u_2} D
inst✝³ : Category.{u_6, u_3} E
P : Cᵒᵖ ⥤ D
F : E ⥤ C
inst✝² : ∀ {X B : E} (π : X ⟶ B) [inst : EffectiveEpi π], PreservesLimit (cospan π π) F
inst✝¹ : F.PreservesEffectiveEpis
hP : EqualizerCondition P
X B : E
π : X ⟶ B
inst✝ : EffectiveEpi π
c : PullbackCone π π
hc : IsLimit c
⊢ Nonempty (IsLimit (Fork.ofι ((F.op ⋙ P).map π.op) ⋯))

Proof state:
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁵ : Category.{u_4, u_1} C
inst✝⁴ : Category.{u_5, u_2} D
inst✝³ : Category.{u_6, u_3} E
P : Cᵒᵖ ⥤ D
F : E ⥤ C
inst✝² : ∀ {X B : E} (π : X ⟶ B) [inst : EffectiveEpi π], PreservesLimit (cospan π π) F
inst✝¹ : F.PreservesEffectiveEpis
hP : EqualizerCondition P
X B : E
π : X ⟶ B
inst✝ : EffectiveEpi π
c : PullbackCone π π
hc : IsLimit c
⊢ Nonempty (IsLimit (Fork.ofι ((F.op ⋙ P).map π.op) ⋯))

Tactic:
have h : P.map (F.map π).op = (F.op ⋙ P).map π.op := by simp

Result:
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁵ : Category.{u_4, u_1} C
inst✝⁴ : Category.{u_5, u_2} D
inst✝³ : Category.{u_6, u_3} E
P : Cᵒᵖ ⥤ D
F : E ⥤ C
inst✝² : ∀ {X B : E} (π : X ⟶ B) [inst : EffectiveEpi π], PreservesLimit (cospan π π) F
inst✝¹ : F.PreservesEffectiveEpis
hP : EqualizerCondition P
X B : E
π : X ⟶ B
inst✝ : EffectiveEpi π
c : PullbackCone π π
hc : IsLimit c
h : P.map (F.map π).op = (F.op ⋙ P).map π.op
⊢ Nonempty (IsLimit (Fork.ofι ((F.op ⋙ P).map π.op) ⋯))