awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
F : C₁ ⥤ Functor.{v₂, v₃, u₂, u₃} C₂ C₃
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
sq : F.PushoutObjObj f₁ f₂
⊢ sq.flip.ι = sq.ι
have h₀ : sq.flip.inl ≫ sq.flip.ι = sq.flip.inl ≫ sq.ι
Tactic: apply sq.flip.isPushout.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
F : C₁ ⥤ Functor.{v₂, v₃, u₂, u₃} C₂ C₃
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
sq : F.PushoutObjObj f₁ f₂
h₀ : sq.flip.inl ≫ sq.flip.ι = sq.flip.inl ≫ sq.ι
⊢ sq.flip.ι = sq.ι
have h₁ : sq.flip.inr ≫ sq.flip.ι = sq.flip.inr ≫ sq.ι
Tactic: apply sq.flip.isPushout.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
F : C₁ ⥤ Functor.{v₂, v₃, u₂, u₃} C₂ C₃
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
sq : F.PushoutObjObj f₁ f₂
⊢ sq.flip.inl ≫ sq.flip.ι = sq.flip.inl ≫ sq.ι
have h₀ : (F.flip.obj Y₂).map f₁ = sq.flip.inl ≫ sq.ι
Tactic: rw [inl_ι, flip_inl, inr_ι, flip_obj_map]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
F : C₁ ⥤ Functor.{v₂, v₃, u₂, u₃} C₂ C₃
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
sq : F.PushoutObjObj f₁ f₂
h₀ : (F.flip.obj Y₂).map f₁ = sq.flip.inl ≫ sq.ι
⊢ sq.flip.inl ≫ sq.flip.ι = sq.flip.inl ≫ sq.ι
have h₁ : (F.flip.obj Y₂).map f₁ = sq.inr ≫ sq.ι
Tactic: rw [inl_ι, flip_inl, inr_ι, flip_obj_map]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
F : C₁ ⥤ Functor.{v₂, v₃, u₂, u₃} C₂ C₃
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
sq : F.PushoutObjObj f₁ f₂
h₀ : (F.flip.obj Y₂).map f₁ = sq.flip.inl ≫ sq.ι
h₁ : (F.flip.obj Y₂).map f₁ = sq.inr ≫ sq.ι
⊢ sq.flip.inl ≫ sq.flip.ι = sq.flip.inl ≫ sq.ι
have h₂ : (F.flip.obj Y₂).map f₁ = (F.map f₁).app Y₂
Tactic: rw [inl_ι, flip_inl, inr_ι, flip_obj_map]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
F : C₁ ⥤ Functor.{v₂, v₃, u₂, u₃} C₂ C₃
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
sq : F.PushoutObjObj f₁ f₂
h₀ : (F.flip.obj Y₂).map f₁ = sq.flip.inl ≫ sq.ι
h₁ : (F.flip.obj Y₂).map f₁ = sq.inr ≫ sq.ι
h₂ : (F.flip.obj Y₂).map f₁ = (F.map f₁).app Y₂
⊢ sq.flip.inl ≫ sq.flip.ι = sq.flip.inl ≫ sq.ι
have h₃ : (F.map f₁).app Y₂ = (F.map f₁).app Y₂
Tactic: rw [inl_ι, flip_inl, inr_ι, flip_obj_map]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
F : C₁ ⥤ Functor.{v₂, v₃, u₂, u₃} C₂ C₃
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
sq : F.PushoutObjObj f₁ f₂
⊢ sq.flip.inr ≫ sq.flip.ι = sq.flip.inr ≫ sq.ι
have h₁ : (F.flip.map f₂).app Y₁ = sq.flip.inr ≫ sq.ι
Tactic: rw [inr_ι, flip_inr, inl_ι, flip_map_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
F : C₁ ⥤ Functor.{v₂, v₃, u₂, u₃} C₂ C₃
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
sq : F.PushoutObjObj f₁ f₂
h₁ : (F.flip.map f₂).app Y₁ = sq.flip.inr ≫ sq.ι
⊢ sq.flip.inr ≫ sq.flip.ι = sq.flip.inr ≫ sq.ι
have h₂ : (F.flip.map f₂).app Y₁ = sq.inl ≫ sq.ι
Tactic: rw [inr_ι, flip_inr, inl_ι, flip_map_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
F : C₁ ⥤ Functor.{v₂, v₃, u₂, u₃} C₂ C₃
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
sq : F.PushoutObjObj f₁ f₂
h₁ : (F.flip.map f₂).app Y₁ = sq.flip.inr ≫ sq.ι
h₂ : (F.flip.map f₂).app Y₁ = sq.inl ≫ sq.ι
⊢ sq.flip.inr ≫ sq.flip.ι = sq.flip.inr ≫ sq.ι
have h₃ : (F.flip.map f₂).app Y₁ = (F.obj Y₁).map f₂
Tactic: rw [inr_ι, flip_inr, inl_ι, flip_map_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
F : C₁ ⥤ Functor.{v₂, v₃, u₂, u₃} C₂ C₃
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
sq : F.PushoutObjObj f₁ f₂
h₁ : (F.flip.map f₂).app Y₁ = sq.flip.inr ≫ sq.ι
h₂ : (F.flip.map f₂).app Y₁ = sq.inl ≫ sq.ι
h₃ : (F.flip.map f₂).app Y₁ = (F.obj Y₁).map f₂
⊢ sq.flip.inr ≫ sq.flip.ι = sq.flip.inr ≫ sq.ι
have h₄ : (F.obj Y₁).map f₂ = (F.obj Y₁).map f₂
Tactic: rw [inr_ι, flip_inr, inl_ι, flip_map_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
F : C₁ ⥤ Functor.{v₂, v₃, u₂, u₃} C₂ C₃
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
sq : F.PushoutObjObj f₁ f₂
F' : C₁ ⥤ Functor.{v₂, v₃, u₂, u₃} C₂ C₃
e : F ≅ F'
⊢ (sq.ofNatIso e).ι = sq.ι ≫ (e.hom.app Y₁).app Y₂
have hₗ : sq.inl ≫ (sq.ofNatIso e).ι = sq.inl ≫ sq.ι ≫ (e.hom.app Y₁).app Y₂
Tactic: apply sq.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
F : C₁ ⥤ Functor.{v₂, v₃, u₂, u₃} C₂ C₃
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
sq : F.PushoutObjObj f₁ f₂
F' : C₁ ⥤ Functor.{v₂, v₃, u₂, u₃} C₂ C₃
e : F ≅ F'
hₗ : sq.inl ≫ (sq.ofNatIso e).ι = sq.inl ≫ sq.ι ≫ (e.hom.app Y₁).app Y₂
⊢ (sq.ofNatIso e).ι = sq.ι ≫ (e.hom.app Y₁).app Y₂
have hᵣ : sq.inr ≫ (sq.ofNatIso e).ι = sq.inr ≫ sq.ι ≫ (e.hom.app Y₁).app Y₂
Tactic: apply sq.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
F : C₁ ⥤ Functor.{v₂, v₃, u₂, u₃} C₂ C₃
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
inst_3 : HasPushout ((F.map f₁).app X₂) ((F.obj X₁).map f₂)
⊢ (ofHasPushout F f₁ f₂).ι = pushout.desc ((F.obj Y₁).map f₂) ((F.map f₁).app Y₂) ⋯
have hₗ : (ofHasPushout F f₁ f₂).inl ≫ (ofHasPushout F f₁ f₂).ι =
  (ofHasPushout F f₁ f₂).inl ≫ pushout.desc ((F.obj Y₁).map f₂) ((F.map f₁).app Y₂) sorry
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
F : C₁ ⥤ Functor.{v₂, v₃, u₂, u₃} C₂ C₃
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
inst_3 : HasPushout ((F.map f₁).app X₂) ((F.obj X₁).map f₂)
hₗ :
  (ofHasPushout F f₁ f₂).inl ≫ (ofHasPushout F f₁ f₂).ι =
    (ofHasPushout F f₁ f₂).inl ≫ pushout.desc ((F.obj Y₁).map f₂) ((F.map f₁).app Y₂) ⋯
⊢ (ofHasPushout F f₁ f₂).ι = pushout.desc ((F.obj Y₁).map f₂) ((F.map f₁).app Y₂) ⋯
have hᵣ : (ofHasPushout F f₁ f₂).inr ≫ (ofHasPushout F f₁ f₂).ι =
  (ofHasPushout F f₁ f₂).inr ≫ pushout.desc ((F.obj Y₁).map f₂) ((F.map f₁).app Y₂) sorry
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
F : C₁ ⥤ Functor.{v₂, v₃, u₂, u₃} C₂ C₃
G : C₁ᵒᵖ ⥤ Functor.{v₃, v₂, u₃, u₂} C₃ C₂
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
sq : F.PushoutObjObj f₁ f₂
inst_3 : PreservesColimitsOfShape (Discrete PEmpty.{1}) (F.flip.obj X₂)
inst_4 : PreservesColimitsOfShape (Discrete PEmpty.{1}) (F.flip.obj Y₂)
h : IsInitial.{v₁, u₁} X₁
hX₂ : IsInitial.{v₃, u₃} ((F.flip.obj X₂).obj X₁) := IsInitial.isInitialObj (F.flip.obj X₂) X₁ h
hY₂ : IsInitial.{v₃, u₃} ((F.flip.obj Y₂).obj X₁) := IsInitial.isInitialObj (F.flip.obj Y₂) X₁ h
⊢ IsPushout ((F.map f₁).app X₂) ((F.obj X₁).map f₂) (𝟙 ((F.obj Y₁).obj X₂))
    ((IsInitial.isInitialObj (F.flip.obj Y₂) X₁ h).to ((F.obj Y₁).obj X₂))
have inst : IsIso ((F.obj X₁).map f₂)
Tactic: apply +allowSynthFailures IsPushout.of_vert_isIso
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst_1 : Category.{v₁, u₁} C₁
inst_2 : Category.{v₂, u₂} C₂
inst_3 : Category.{v₃, u₃} C₃
F : C₁ ⥤ Functor.{v₂, v₃, u₂, u₃} C₂ C₃
G : C₁ᵒᵖ ⥤ Functor.{v₃, v₂, u₃, u₂} C₃ C₂
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
sq : F.PushoutObjObj f₁ f₂
inst_4 : PreservesColimitsOfShape (Discrete PEmpty.{1}) (F.flip.obj X₂)
inst_5 : PreservesColimitsOfShape (Discrete PEmpty.{1}) (F.flip.obj Y₂)
h : IsInitial.{v₁, u₁} X₁
hX₂ : IsInitial.{v₃, u₃} ((F.flip.obj X₂).obj X₁) := IsInitial.isInitialObj (F.flip.obj X₂) X₁ h
hY₂ : IsInitial.{v₃, u₃} ((F.flip.obj Y₂).obj X₁) := IsInitial.isInitialObj (F.flip.obj Y₂) X₁ h
inst : IsIso ((F.obj X₁).map f₂)
⊢ IsPushout ((F.map f₁).app X₂) ((F.obj X₁).map f₂) (𝟙 ((F.obj Y₁).obj X₂))
    ((IsInitial.isInitialObj (F.flip.obj Y₂) X₁ h).to ((F.obj Y₁).obj X₂))
have sq₁ : CommSq ((F.map f₁).app X₂) ((F.obj X₁).map f₂) (𝟙 ((F.obj Y₁).obj X₂))
  ((IsInitial.isInitialObj (F.flip.obj Y₂) X₁ h).to ((F.obj Y₁).obj X₂))
Tactic: apply +allowSynthFailures IsPushout.of_vert_isIso
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
F : C₁ ⥤ Functor.{v₂, v₃, u₂, u₃} C₂ C₃
G : C₁ᵒᵖ ⥤ Functor.{v₃, v₂, u₃, u₂} C₃ C₂
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
sq : F.PushoutObjObj f₁ f₂
inst_3 : PreservesColimitsOfShape (Discrete PEmpty.{1}) (F.obj X₁)
inst_4 : PreservesColimitsOfShape (Discrete PEmpty.{1}) (F.obj Y₁)
h : IsInitial.{v₂, u₂} X₂
hX₁ : IsInitial.{v₃, u₃} ((F.obj X₁).obj X₂) := IsInitial.isInitialObj (F.obj X₁) X₂ h
hY₁ : IsInitial.{v₃, u₃} ((F.obj Y₁).obj X₂) := IsInitial.isInitialObj (F.obj Y₁) X₂ h
⊢ IsPushout ((F.map f₁).app X₂) ((F.obj X₁).map f₂) ((IsInitial.isInitialObj (F.obj Y₁) X₂ h).to ((F.obj X₁).obj Y₂))
    (𝟙 ((F.obj X₁).obj Y₂))
have inst : IsIso ((F.map f₁).app X₂)
Tactic: apply +allowSynthFailures IsPushout.of_horiz_isIso
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst_1 : Category.{v₁, u₁} C₁
inst_2 : Category.{v₂, u₂} C₂
inst_3 : Category.{v₃, u₃} C₃
F : C₁ ⥤ Functor.{v₂, v₃, u₂, u₃} C₂ C₃
G : C₁ᵒᵖ ⥤ Functor.{v₃, v₂, u₃, u₂} C₃ C₂
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
sq : F.PushoutObjObj f₁ f₂
inst_4 : PreservesColimitsOfShape (Discrete PEmpty.{1}) (F.obj X₁)
inst_5 : PreservesColimitsOfShape (Discrete PEmpty.{1}) (F.obj Y₁)
h : IsInitial.{v₂, u₂} X₂
hX₁ : IsInitial.{v₃, u₃} ((F.obj X₁).obj X₂) := IsInitial.isInitialObj (F.obj X₁) X₂ h
hY₁ : IsInitial.{v₃, u₃} ((F.obj Y₁).obj X₂) := IsInitial.isInitialObj (F.obj Y₁) X₂ h
inst : IsIso ((F.map f₁).app X₂)
⊢ IsPushout ((F.map f₁).app X₂) ((F.obj X₁).map f₂) ((IsInitial.isInitialObj (F.obj Y₁) X₂ h).to ((F.obj X₁).obj Y₂))
    (𝟙 ((F.obj X₁).obj Y₂))
have sq₁ : CommSq ((F.map f₁).app X₂) ((F.obj X₁).map f₂) ((IsInitial.isInitialObj (F.obj Y₁) X₂ h).to ((F.obj X₁).obj Y₂))
  (𝟙 ((F.obj X₁).obj Y₂))
Tactic: apply +allowSynthFailures IsPushout.of_horiz_isIso
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
F : C₁ ⥤ Functor.{v₂, v₃, u₂, u₃} C₂ C₃
G : C₁ᵒᵖ ⥤ Functor.{v₃, v₂, u₃, u₂} C₃ C₂
X₁ Y₁ : C₁
f₁_1 : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂_1 : X₂ ⟶ Y₂
sq_1 : F.PushoutObjObj f₁_1 f₂_1
f₁ f₁' : Arrow.{v₁, u₁} C₁
f₂ : Arrow.{v₂, u₂} C₂
sq₁₂ : F.PushoutObjObj f₁.hom f₂.hom
sq₁₂' : F.PushoutObjObj f₁'.hom f₂.hom
sq : f₁ ⟶ f₁'
⊢ (F.map f₁.hom).app f₂.left ≫ (F.map (Arrow.Hom.right sq)).app f₂.left ≫ sq₁₂'.inl =
    (F.obj f₁.left).map f₂.hom ≫ (F.map (Arrow.Hom.left sq)).app f₂.right ≫ sq₁₂'.inr
have simp : (F.map f₁.hom).app f₂.left ≫ (F.map (Arrow.Hom.right sq)).app f₂.left ≫ sq₁₂'.inl =
  (F.obj f₁.left).map f₂.hom ≫ (F.map (Arrow.Hom.left sq)).app f₂.right ≫ sq₁₂'.inr
Tactic: simp only [Arrow.mk_left]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
F : C₁ ⥤ Functor.{v₂, v₃, u₂, u₃} C₂ C₃
G : C₁ᵒᵖ ⥤ Functor.{v₃, v₂, u₃, u₂} C₃ C₂
X₁ Y₁ : C₁
f₁_1 : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂_1 : X₂ ⟶ Y₂
sq_1 : F.PushoutObjObj f₁_1 f₂_1
f₁ f₁' : Arrow.{v₁, u₁} C₁
f₂ : Arrow.{v₂, u₂} C₂
sq₁₂ : F.PushoutObjObj f₁.hom f₂.hom
sq₁₂' : F.PushoutObjObj f₁'.hom f₂.hom
sq : f₁ ⟶ f₁'
⊢ map (𝟭 C₃)
        (⋯.desc ((F.map (Arrow.Hom.right sq)).app f₂.left ≫ sq₁₂'.inl)
          ((F.map (Arrow.Hom.left sq)).app f₂.right ≫ sq₁₂'.inr) ⋯) ≫
      (Arrow.mk sq₁₂'.ι).hom =
    (Arrow.mk sq₁₂.ι).hom ≫ map (𝟭 C₃) ((F.map (Arrow.Hom.right sq)).app f₂.right)
have hₗ : sq₁₂.inl ≫
    map (𝟭 C₃)
        (sorry.desc ((F.map (Arrow.Hom.right sq)).app f₂.left ≫ sq₁₂'.inl)
          ((F.map (Arrow.Hom.left sq)).app f₂.right ≫ sq₁₂'.inr) sorry) ≫
      (Arrow.mk sq₁₂'.ι).hom =
  sq₁₂.inl ≫ (Arrow.mk sq₁₂.ι).hom ≫ map (𝟭 C₃) ((F.map (Arrow.Hom.right sq)).app f₂.right)
Tactic: apply PushoutObjObj.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
F : C₁ ⥤ Functor.{v₂, v₃, u₂, u₃} C₂ C₃
G : C₁ᵒᵖ ⥤ Functor.{v₃, v₂, u₃, u₂} C₃ C₂
X₁ Y₁ : C₁
f₁_1 : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂_1 : X₂ ⟶ Y₂
sq_1 : F.PushoutObjObj f₁_1 f₂_1
f₁ f₁' : Arrow.{v₁, u₁} C₁
f₂ : Arrow.{v₂, u₂} C₂
sq₁₂ : F.PushoutObjObj f₁.hom f₂.hom
sq₁₂' : F.PushoutObjObj f₁'.hom f₂.hom
sq : f₁ ⟶ f₁'
hₗ :
  sq₁₂.inl ≫
      map (𝟭 C₃)
          (⋯.desc ((F.map (Arrow.Hom.right sq)).app f₂.left ≫ sq₁₂'.inl)
            ((F.map (Arrow.Hom.left sq)).app f₂.right ≫ sq₁₂'.inr) ⋯) ≫
        (Arrow.mk sq₁₂'.ι).hom =
    sq₁₂.inl ≫ (Arrow.mk sq₁₂.ι).hom ≫ map (𝟭 C₃) ((F.map (Arrow.Hom.right sq)).app f₂.right)
⊢ map (𝟭 C₃)
        (⋯.desc ((F.map (Arrow.Hom.right sq)).app f₂.left ≫ sq₁₂'.inl)
          ((F.map (Arrow.Hom.left sq)).app f₂.right ≫ sq₁₂'.inr) ⋯) ≫
      (Arrow.mk sq₁₂'.ι).hom =
    (Arrow.mk sq₁₂.ι).hom ≫ map (𝟭 C₃) ((F.map (Arrow.Hom.right sq)).app f₂.right)
have hᵣ : sq₁₂.inr ≫
    map (𝟭 C₃)
        (sorry.desc ((F.map (Arrow.Hom.right sq)).app f₂.left ≫ sq₁₂'.inl)
          ((F.map (Arrow.Hom.left sq)).app f₂.right ≫ sq₁₂'.inr) sorry) ≫
      (Arrow.mk sq₁₂'.ι).hom =
  sq₁₂.inr ≫ (Arrow.mk sq₁₂.ι).hom ≫ map (𝟭 C₃) ((F.map (Arrow.Hom.right sq)).app f₂.right)
Tactic: apply PushoutObjObj.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
F : C₁ ⥤ Functor.{v₂, v₃, u₂, u₃} C₂ C₃
G : C₁ᵒᵖ ⥤ Functor.{v₃, v₂, u₃, u₂} C₃ C₂
X₁ Y₁ : C₁
f₁_1 : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂_1 : X₂ ⟶ Y₂
sq_1 : F.PushoutObjObj f₁_1 f₂_1
f₁_2 f₁' : Arrow.{v₁, u₁} C₁
f₂_2 : Arrow.{v₂, u₂} C₂
sq₁₂_1 : F.PushoutObjObj f₁_2.hom f₂_2.hom
sq₁₂'_1 : F.PushoutObjObj f₁'.hom f₂_2.hom
f₁ : Arrow.{v₁, u₁} C₁
f₂ f₂' : Arrow.{v₂, u₂} C₂
sq₁₂ : F.PushoutObjObj f₁.hom f₂.hom
sq₁₂' : F.PushoutObjObj f₁.hom f₂'.hom
sq : f₂ ⟶ f₂'
⊢ (F.map f₁.hom).app f₂.left ≫ (F.obj f₁.right).map (Arrow.Hom.left sq) ≫ sq₁₂'.inl =
    (F.obj f₁.left).map f₂.hom ≫ (F.obj f₁.left).map (Arrow.Hom.right sq) ≫ sq₁₂'.inr
have simp : (F.map f₁.hom).app f₂.left ≫ (F.obj f₁.right).map (Arrow.Hom.left sq) ≫ sq₁₂'.inl =
  (F.obj f₁.left).map f₂.hom ≫ (F.obj f₁.left).map (Arrow.Hom.right sq) ≫ sq₁₂'.inr
Tactic: simp only [Arrow.mk_left]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
F : C₁ ⥤ Functor.{v₂, v₃, u₂, u₃} C₂ C₃
G : C₁ᵒᵖ ⥤ Functor.{v₃, v₂, u₃, u₂} C₃ C₂
X₁ Y₁ : C₁
f₁_1 : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂_1 : X₂ ⟶ Y₂
sq_1 : F.PushoutObjObj f₁_1 f₂_1
f₁_2 f₁' : Arrow.{v₁, u₁} C₁
f₂_2 : Arrow.{v₂, u₂} C₂
sq₁₂_1 : F.PushoutObjObj f₁_2.hom f₂_2.hom
sq₁₂'_1 : F.PushoutObjObj f₁'.hom f₂_2.hom
f₁ : Arrow.{v₁, u₁} C₁
f₂ f₂' : Arrow.{v₂, u₂} C₂
sq₁₂ : F.PushoutObjObj f₁.hom f₂.hom
sq₁₂' : F.PushoutObjObj f₁.hom f₂'.hom
sq : f₂ ⟶ f₂'
⊢ map (𝟭 C₃)
        (⋯.desc ((F.obj f₁.right).map (Arrow.Hom.left sq) ≫ sq₁₂'.inl)
          ((F.obj f₁.left).map (Arrow.Hom.right sq) ≫ sq₁₂'.inr) ⋯) ≫
      (Arrow.mk sq₁₂'.ι).hom =
    (Arrow.mk sq₁₂.ι).hom ≫ map (𝟭 C₃) ((F.obj f₁.right).map (Arrow.Hom.right sq))
have hₗ : sq₁₂.inl ≫
    map (𝟭 C₃)
        (sorry.desc ((F.obj f₁.right).map (Arrow.Hom.left sq) ≫ sq₁₂'.inl)
          ((F.obj f₁.left).map (Arrow.Hom.right sq) ≫ sq₁₂'.inr) sorry) ≫
      (Arrow.mk sq₁₂'.ι).hom =
  sq₁₂.inl ≫ (Arrow.mk sq₁₂.ι).hom ≫ map (𝟭 C₃) ((F.obj f₁.right).map (Arrow.Hom.right sq))
Tactic: apply PushoutObjObj.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
F : C₁ ⥤ Functor.{v₂, v₃, u₂, u₃} C₂ C₃
G : C₁ᵒᵖ ⥤ Functor.{v₃, v₂, u₃, u₂} C₃ C₂
X₁ Y₁ : C₁
f₁_1 : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂_1 : X₂ ⟶ Y₂
sq_1 : F.PushoutObjObj f₁_1 f₂_1
f₁_2 f₁' : Arrow.{v₁, u₁} C₁
f₂_2 : Arrow.{v₂, u₂} C₂
sq₁₂_1 : F.PushoutObjObj f₁_2.hom f₂_2.hom
sq₁₂'_1 : F.PushoutObjObj f₁'.hom f₂_2.hom
f₁ : Arrow.{v₁, u₁} C₁
f₂ f₂' : Arrow.{v₂, u₂} C₂
sq₁₂ : F.PushoutObjObj f₁.hom f₂.hom
sq₁₂' : F.PushoutObjObj f₁.hom f₂'.hom
sq : f₂ ⟶ f₂'
hₗ :
  sq₁₂.inl ≫
      map (𝟭 C₃)
          (⋯.desc ((F.obj f₁.right).map (Arrow.Hom.left sq) ≫ sq₁₂'.inl)
            ((F.obj f₁.left).map (Arrow.Hom.right sq) ≫ sq₁₂'.inr) ⋯) ≫
        (Arrow.mk sq₁₂'.ι).hom =
    sq₁₂.inl ≫ (Arrow.mk sq₁₂.ι).hom ≫ map (𝟭 C₃) ((F.obj f₁.right).map (Arrow.Hom.right sq))
⊢ map (𝟭 C₃)
        (⋯.desc ((F.obj f₁.right).map (Arrow.Hom.left sq) ≫ sq₁₂'.inl)
          ((F.obj f₁.left).map (Arrow.Hom.right sq) ≫ sq₁₂'.inr) ⋯) ≫
      (Arrow.mk sq₁₂'.ι).hom =
    (Arrow.mk sq₁₂.ι).hom ≫ map (𝟭 C₃) ((F.obj f₁.right).map (Arrow.Hom.right sq))
have hᵣ : sq₁₂.inr ≫
    map (𝟭 C₃)
        (sorry.desc ((F.obj f₁.right).map (Arrow.Hom.left sq) ≫ sq₁₂'.inl)
          ((F.obj f₁.left).map (Arrow.Hom.right sq) ≫ sq₁₂'.inr) sorry) ≫
      (Arrow.mk sq₁₂'.ι).hom =
  sq₁₂.inr ≫ (Arrow.mk sq₁₂.ι).hom ≫ map (𝟭 C₃) ((F.obj f₁.right).map (Arrow.Hom.right sq))
Tactic: apply PushoutObjObj.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
G : C₁ᵒᵖ ⥤ Functor.{v₃, v₂, u₃, u₂} C₃ C₂
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₃ Y₃ : C₃
f₃ : X₃ ⟶ Y₃
inst_3 : HasPullback ((G.obj (op X₁)).map f₃) ((G.map f₁.op).app Y₃)
⊢ (ofHasPullback G f₁ f₃).π = pullback.lift ((G.map f₁.op).app X₃) ((G.obj (op Y₁)).map f₃) ⋯
have h₁ : (ofHasPullback G f₁ f₃).π ≫ (ofHasPullback G f₁ f₃).fst =
  pullback.lift ((G.map f₁.op).app X₃) ((G.obj (op Y₁)).map f₃) sorry ≫ (ofHasPullback G f₁ f₃).fst
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
G : C₁ᵒᵖ ⥤ Functor.{v₃, v₂, u₃, u₂} C₃ C₂
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₃ Y₃ : C₃
f₃ : X₃ ⟶ Y₃
inst_3 : HasPullback ((G.obj (op X₁)).map f₃) ((G.map f₁.op).app Y₃)
h₁ :
  (ofHasPullback G f₁ f₃).π ≫ (ofHasPullback G f₁ f₃).fst =
    pullback.lift ((G.map f₁.op).app X₃) ((G.obj (op Y₁)).map f₃) ⋯ ≫ (ofHasPullback G f₁ f₃).fst
⊢ (ofHasPullback G f₁ f₃).π = pullback.lift ((G.map f₁.op).app X₃) ((G.obj (op Y₁)).map f₃) ⋯
have h₂ : (ofHasPullback G f₁ f₃).π ≫ (ofHasPullback G f₁ f₃).snd =
  pullback.lift ((G.map f₁.op).app X₃) ((G.obj (op Y₁)).map f₃) sorry ≫ (ofHasPullback G f₁ f₃).snd
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
F : C₁ ⥤ Functor.{v₂, v₃, u₂, u₃} C₂ C₃
G : C₁ᵒᵖ ⥤ Functor.{v₃, v₂, u₃, u₂} C₃ C₂
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₃ Y₃ : C₃
f₃ : X₃ ⟶ Y₃
sq : G.PullbackObjObj f₁ f₃
inst_3 : PreservesLimitsOfShape (Discrete PEmpty.{1}) (G.flip.obj X₃)
inst_4 : PreservesLimitsOfShape (Discrete PEmpty.{1}) (G.flip.obj Y₃)
h : IsInitial.{v₁, u₁} X₁
hX₃ : IsTerminal.{v₂, u₂} ((G.flip.obj X₃).obj (op X₁)) :=
  IsTerminal.isTerminalObj (G.flip.obj X₃) (op X₁) (IsInitial.op C₁ h)
hY₃ : IsTerminal.{v₂, u₂} ((G.flip.obj Y₃).obj (op X₁)) :=
  IsTerminal.isTerminalObj (G.flip.obj Y₃) (op X₁) (IsInitial.op C₁ h)
⊢ IsPullback ((IsTerminal.isTerminalObj (G.flip.obj X₃) (op X₁) (IsInitial.op C₁ h)).from ((G.obj (op Y₁)).obj Y₃))
    (𝟙 ((G.obj (op Y₁)).obj Y₃)) ((G.obj (op X₁)).map f₃) ((G.map f₁.op).app Y₃)
have inst : IsIso ((G.obj (op X₁)).map f₃)
Tactic: apply +allowSynthFailures IsPullback.of_vert_isIso
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst_1 : Category.{v₁, u₁} C₁
inst_2 : Category.{v₂, u₂} C₂
inst_3 : Category.{v₃, u₃} C₃
F : C₁ ⥤ Functor.{v₂, v₃, u₂, u₃} C₂ C₃
G : C₁ᵒᵖ ⥤ Functor.{v₃, v₂, u₃, u₂} C₃ C₂
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₃ Y₃ : C₃
f₃ : X₃ ⟶ Y₃
sq : G.PullbackObjObj f₁ f₃
inst_4 : PreservesLimitsOfShape (Discrete PEmpty.{1}) (G.flip.obj X₃)
inst_5 : PreservesLimitsOfShape (Discrete PEmpty.{1}) (G.flip.obj Y₃)
h : IsInitial.{v₁, u₁} X₁
hX₃ : IsTerminal.{v₂, u₂} ((G.flip.obj X₃).obj (op X₁)) :=
  IsTerminal.isTerminalObj (G.flip.obj X₃) (op X₁) (IsInitial.op C₁ h)
hY₃ : IsTerminal.{v₂, u₂} ((G.flip.obj Y₃).obj (op X₁)) :=
  IsTerminal.isTerminalObj (G.flip.obj Y₃) (op X₁) (IsInitial.op C₁ h)
inst : IsIso ((G.obj (op X₁)).map f₃)
⊢ IsPullback ((IsTerminal.isTerminalObj (G.flip.obj X₃) (op X₁) (IsInitial.op C₁ h)).from ((G.obj (op Y₁)).obj Y₃))
    (𝟙 ((G.obj (op Y₁)).obj Y₃)) ((G.obj (op X₁)).map f₃) ((G.map f₁.op).app Y₃)
have sq₁ : CommSq ((IsTerminal.isTerminalObj (G.flip.obj X₃) (op X₁) (IsInitial.op C₁ h)).from ((G.obj (op Y₁)).obj Y₃))
  (𝟙 ((G.obj (op Y₁)).obj Y₃)) ((G.obj (op X₁)).map f₃) ((G.map f₁.op).app Y₃)
Tactic: apply +allowSynthFailures IsPullback.of_vert_isIso