-- Mathlib/Algebra/Category/ModuleCat/Presheaf/Pullback.lean
lemma pullbackObjIsDefined_eq_top :
    PullbackObjIsDefined.{u} φ = ⊤

Proof state:
C D : Type u
inst✝¹ : SmallCategory C
inst✝ : SmallCategory D
F : C ⥤ D
R : Dᵒᵖ ⥤ RingCat
S : Cᵒᵖ ⥤ RingCat
φ : S ⟶ F.op ⋙ R
⊢ PullbackObjIsDefined φ = ⊤

Tactic:
ext M

Result:
case h.a
C D : Type u
inst✝¹ : SmallCategory C
inst✝ : SmallCategory D
F : C ⥤ D
R : Dᵒᵖ ⥤ RingCat
S : Cᵒᵖ ⥤ RingCat
φ : S ⟶ F.op ⋙ R
M : PresheafOfModules S
⊢ PullbackObjIsDefined φ M ↔ ⊤ M

Proof state:
case h.a
C D : Type u
inst✝¹ : SmallCategory C
inst✝ : SmallCategory D
F : C ⥤ D
R : Dᵒᵖ ⥤ RingCat
S : Cᵒᵖ ⥤ RingCat
φ : S ⟶ F.op ⋙ R
M : PresheafOfModules S
⊢ PullbackObjIsDefined φ M ↔ ⊤ M

Tactic:
simp only [Pi.top_apply, Prop.top_eq_true, iff_true]

Result:
case h.a
C D : Type u
inst✝¹ : SmallCategory C
inst✝ : SmallCategory D
F : C ⥤ D
R : Dᵒᵖ ⥤ RingCat
S : Cᵒᵖ ⥤ RingCat
φ : S ⟶ F.op ⋙ R
M : PresheafOfModules S
⊢ PullbackObjIsDefined φ M

Proof state:
case h.a.one
C D : Type u
inst✝¹ : SmallCategory C
inst✝ : SmallCategory D
F : C ⥤ D
R : Dᵒᵖ ⥤ RingCat
S : Cᵒᵖ ⥤ RingCat
φ : S ⟶ F.op ⋙ R
M : PresheafOfModules S
⊢ (pushforward φ).LeftAdjointObjIsDefined ((parallelPair M.toFreeYonedaCoproduct 0).obj WalkingParallelPair.one)

Tactic:
apply Functor.leftAdjointObjIsDefined_colimit _
  (fun _ ↦ pullbackObjIsDefined_free_yoneda _ _)

Result:
no goals

Proof state:
case h.a
C D : Type u
inst✝¹ : SmallCategory C
inst✝ : SmallCategory D
F : C ⥤ D
R : Dᵒᵖ ⥤ RingCat
S : Cᵒᵖ ⥤ RingCat
φ : S ⟶ F.op ⋙ R
M : PresheafOfModules S
⊢ PullbackObjIsDefined φ M

Tactic:
apply Functor.leftAdjointObjIsDefined_of_isColimit
  M.isColimitFreeYonedaCoproductsCokernelCofork

Result:
case h.a
C D : Type u
inst✝¹ : SmallCategory C
inst✝ : SmallCategory D
F : C ⥤ D
R : Dᵒᵖ ⥤ RingCat
S : Cᵒᵖ ⥤ RingCat
φ : S ⟶ F.op ⋙ R
M : PresheafOfModules S
⊢ ∀ (j : WalkingParallelPair), (pushforward φ).LeftAdjointObjIsDefined ((parallelPair M.toFreeYonedaCoproduct 0).obj j)

Proof state:
case h.a.zero
C D : Type u
inst✝¹ : SmallCategory C
inst✝ : SmallCategory D
F : C ⥤ D
R : Dᵒᵖ ⥤ RingCat
S : Cᵒᵖ ⥤ RingCat
φ : S ⟶ F.op ⋙ R
M : PresheafOfModules S
⊢ (pushforward φ).LeftAdjointObjIsDefined ((parallelPair M.toFreeYonedaCoproduct 0).obj WalkingParallelPair.zero)

case h.a.one
C D : Type u
inst✝¹ : SmallCategory C
inst✝ : SmallCategory D
F : C ⥤ D
R : Dᵒᵖ ⥤ RingCat
S : Cᵒᵖ ⥤ RingCat
φ : S ⟶ F.op ⋙ R
M : PresheafOfModules S
⊢ (pushforward φ).LeftAdjointObjIsDefined ((parallelPair M.toFreeYonedaCoproduct 0).obj WalkingParallelPair.one)

Tactic:
all_goals
  apply Functor.leftAdjointObjIsDefined_colimit _
    (fun _ ↦ pullbackObjIsDefined_free_yoneda _ _)

Result:
no goals

Proof state:
case h.a
C D : Type u
inst✝¹ : SmallCategory C
inst✝ : SmallCategory D
F : C ⥤ D
R : Dᵒᵖ ⥤ RingCat
S : Cᵒᵖ ⥤ RingCat
φ : S ⟶ F.op ⋙ R
M : PresheafOfModules S
⊢ ∀ (j : WalkingParallelPair), (pushforward φ).LeftAdjointObjIsDefined ((parallelPair M.toFreeYonedaCoproduct 0).obj j)

Tactic:
rintro (_ | _)

Result:
case h.a.zero
C D : Type u
inst✝¹ : SmallCategory C
inst✝ : SmallCategory D
F : C ⥤ D
R : Dᵒᵖ ⥤ RingCat
S : Cᵒᵖ ⥤ RingCat
φ : S ⟶ F.op ⋙ R
M : PresheafOfModules S
⊢ (pushforward φ).LeftAdjointObjIsDefined ((parallelPair M.toFreeYonedaCoproduct 0).obj WalkingParallelPair.zero)

case h.a.one
C D : Type u
inst✝¹ : SmallCategory C
inst✝ : SmallCategory D
F : C ⥤ D
R : Dᵒᵖ ⥤ RingCat
S : Cᵒᵖ ⥤ RingCat
φ : S ⟶ F.op ⋙ R
M : PresheafOfModules S
⊢ (pushforward φ).LeftAdjointObjIsDefined ((parallelPair M.toFreeYonedaCoproduct 0).obj WalkingParallelPair.one)