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₃
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.obj (op X₁))
inst_4 : PreservesLimitsOfShape (Discrete PEmpty.{1}) (G.obj (op Y₁))
h : IsTerminal.{v₃, u₃} Y₃
hX₁ : IsTerminal.{v₂, u₂} ((G.obj (op X₁)).obj Y₃) := IsTerminal.isTerminalObj (G.obj (op X₁)) Y₃ h
hY₁ : IsTerminal.{v₂, u₂} ((G.obj (op Y₁)).obj Y₃) := IsTerminal.isTerminalObj (G.obj (op Y₁)) Y₃ h
⊢ IsPullback (𝟙 ((G.obj (op X₁)).obj X₃))
    ((IsTerminal.isTerminalObj (G.obj (op Y₁)) Y₃ h).from ((G.obj (op X₁)).obj X₃)) ((G.obj (op X₁)).map f₃)
    ((G.map f₁.op).app Y₃)
have inst : IsIso ((G.map f₁.op).app Y₃)
Tactic: apply +allowSynthFailures IsPullback.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 : G.PullbackObjObj f₁ f₃
inst_4 : PreservesLimitsOfShape (Discrete PEmpty.{1}) (G.obj (op X₁))
inst_5 : PreservesLimitsOfShape (Discrete PEmpty.{1}) (G.obj (op Y₁))
h : IsTerminal.{v₃, u₃} Y₃
hX₁ : IsTerminal.{v₂, u₂} ((G.obj (op X₁)).obj Y₃) := IsTerminal.isTerminalObj (G.obj (op X₁)) Y₃ h
hY₁ : IsTerminal.{v₂, u₂} ((G.obj (op Y₁)).obj Y₃) := IsTerminal.isTerminalObj (G.obj (op Y₁)) Y₃ h
inst : IsIso ((G.map f₁.op).app Y₃)
⊢ IsPullback (𝟙 ((G.obj (op X₁)).obj X₃))
    ((IsTerminal.isTerminalObj (G.obj (op Y₁)) Y₃ h).from ((G.obj (op X₁)).obj X₃)) ((G.obj (op X₁)).map f₃)
    ((G.map f₁.op).app Y₃)
have sq₁ : CommSq (𝟙 ((G.obj (op X₁)).obj X₃)) ((IsTerminal.isTerminalObj (G.obj (op Y₁)) Y₃ h).from ((G.obj (op X₁)).obj X₃))
  ((G.obj (op X₁)).map f₃) ((G.map f₁.op).app Y₃)
Tactic: apply +allowSynthFailures IsPullback.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 : G.PullbackObjObj f₁_1 f₃_1
f₁ f₁' : Arrow.{v₁, u₁} C₁
f₃ : Arrow.{v₃, u₃} C₃
sq₁₃ : G.PullbackObjObj f₁.hom f₃.hom
sq₁₃' : G.PullbackObjObj f₁'.hom f₃.hom
sq : f₁' ⟶ f₁
⊢ (sq₁₃.fst ≫ (G.map (Arrow.Hom.left sq).op).app f₃.left) ≫ (G.obj (op f₁'.left)).map f₃.hom =
    (sq₁₃.snd ≫ (G.map (Arrow.Hom.right sq).op).app f₃.right) ≫ (G.map f₁'.hom.op).app f₃.right
have simp : sq₁₃.fst ≫ (G.map (Arrow.Hom.left sq).op).app f₃.left ≫ (G.obj (op f₁'.left)).map f₃.hom =
  sq₁₃.snd ≫ (G.map (Arrow.Hom.right sq).op).app f₃.right ≫ (G.map f₁'.hom.op).app f₃.right
Tactic: simp [Arrow.mk_right]
-- 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 : G.PullbackObjObj f₁_1 f₃_1
f₁ f₁' : Arrow.{v₁, u₁} C₁
f₃ : Arrow.{v₃, u₃} C₃
sq₁₃ : G.PullbackObjObj f₁.hom f₃.hom
sq₁₃' : G.PullbackObjObj f₁'.hom f₃.hom
sq : f₁' ⟶ f₁
⊢ map (𝟭 C₂) ((G.map (Arrow.Hom.right sq).op).app f₃.left) ≫ (Arrow.mk sq₁₃'.π).hom =
    (Arrow.mk sq₁₃.π).hom ≫
      map (𝟭 C₂)
        (⋯.lift (sq₁₃.fst ≫ (G.map (Arrow.Hom.left sq).op).app f₃.left)
          (sq₁₃.snd ≫ (G.map (Arrow.Hom.right sq).op).app f₃.right) ⋯)
have h₁ : (map (𝟭 C₂) ((G.map (Arrow.Hom.right sq).op).app f₃.left) ≫ (Arrow.mk sq₁₃'.π).hom) ≫ sq₁₃'.fst =
  ((Arrow.mk sq₁₃.π).hom ≫
      map (𝟭 C₂)
        (sorry.lift (sq₁₃.fst ≫ (G.map (Arrow.Hom.left sq).op).app f₃.left)
          (sq₁₃.snd ≫ (G.map (Arrow.Hom.right sq).op).app f₃.right) sorry)) ≫
    sq₁₃'.fst
Tactic: apply PullbackObjObj.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 : G.PullbackObjObj f₁_1 f₃_1
f₁ f₁' : Arrow.{v₁, u₁} C₁
f₃ : Arrow.{v₃, u₃} C₃
sq₁₃ : G.PullbackObjObj f₁.hom f₃.hom
sq₁₃' : G.PullbackObjObj f₁'.hom f₃.hom
sq : f₁' ⟶ f₁
h₁ :
  (map (𝟭 C₂) ((G.map (Arrow.Hom.right sq).op).app f₃.left) ≫ (Arrow.mk sq₁₃'.π).hom) ≫ sq₁₃'.fst =
    ((Arrow.mk sq₁₃.π).hom ≫
        map (𝟭 C₂)
          (⋯.lift (sq₁₃.fst ≫ (G.map (Arrow.Hom.left sq).op).app f₃.left)
            (sq₁₃.snd ≫ (G.map (Arrow.Hom.right sq).op).app f₃.right) ⋯)) ≫
      sq₁₃'.fst
⊢ map (𝟭 C₂) ((G.map (Arrow.Hom.right sq).op).app f₃.left) ≫ (Arrow.mk sq₁₃'.π).hom =
    (Arrow.mk sq₁₃.π).hom ≫
      map (𝟭 C₂)
        (⋯.lift (sq₁₃.fst ≫ (G.map (Arrow.Hom.left sq).op).app f₃.left)
          (sq₁₃.snd ≫ (G.map (Arrow.Hom.right sq).op).app f₃.right) ⋯)
have h₂ : (map (𝟭 C₂) ((G.map (Arrow.Hom.right sq).op).app f₃.left) ≫ (Arrow.mk sq₁₃'.π).hom) ≫ sq₁₃'.snd =
  ((Arrow.mk sq₁₃.π).hom ≫
      map (𝟭 C₂)
        (sorry.lift (sq₁₃.fst ≫ (G.map (Arrow.Hom.left sq).op).app f₃.left)
          (sq₁₃.snd ≫ (G.map (Arrow.Hom.right sq).op).app f₃.right) sorry)) ≫
    sq₁₃'.snd
Tactic: apply PullbackObjObj.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 : G.PullbackObjObj f₁_1 f₃_1
f₁_2 f₁' : Arrow.{v₁, u₁} C₁
f₃_2 : Arrow.{v₃, u₃} C₃
sq₁₃_1 : G.PullbackObjObj f₁_2.hom f₃_2.hom
sq₁₃'_1 : G.PullbackObjObj f₁'.hom f₃_2.hom
f₁ : Arrow.{v₁, u₁} C₁
f₃ f₃' : Arrow.{v₃, u₃} C₃
sq₁₃ : G.PullbackObjObj f₁.hom f₃.hom
sq₁₃' : G.PullbackObjObj f₁.hom f₃'.hom
sq : f₃ ⟶ f₃'
⊢ (sq₁₃.fst ≫ (G.obj (op f₁.left)).map (Arrow.Hom.left sq)) ≫ (G.obj (op f₁.left)).map f₃'.hom =
    (sq₁₃.snd ≫ (G.obj (op f₁.right)).map (Arrow.Hom.right sq)) ≫ (G.map f₁.hom.op).app f₃'.right
have simp : sq₁₃.fst ≫ (G.obj (op f₁.left)).map (Arrow.Hom.left sq) ≫ (G.obj (op f₁.left)).map f₃'.hom =
  sq₁₃.snd ≫ (G.map f₁.hom.op).app f₃.right ≫ (G.obj (op f₁.left)).map (Arrow.Hom.right sq)
Tactic: simp [Arrow.mk_right]
-- 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 : G.PullbackObjObj f₁_1 f₃_1
f₁_2 f₁' : Arrow.{v₁, u₁} C₁
f₃_2 : Arrow.{v₃, u₃} C₃
sq₁₃_1 : G.PullbackObjObj f₁_2.hom f₃_2.hom
sq₁₃'_1 : G.PullbackObjObj f₁'.hom f₃_2.hom
f₁ : Arrow.{v₁, u₁} C₁
f₃ f₃' : Arrow.{v₃, u₃} C₃
sq₁₃ : G.PullbackObjObj f₁.hom f₃.hom
sq₁₃' : G.PullbackObjObj f₁.hom f₃'.hom
sq : f₃ ⟶ f₃'
⊢ map (𝟭 C₂) ((G.obj (op f₁.right)).map (Arrow.Hom.left sq)) ≫ (Arrow.mk sq₁₃'.π).hom =
    (Arrow.mk sq₁₃.π).hom ≫
      map (𝟭 C₂)
        (⋯.lift (sq₁₃.fst ≫ (G.obj (op f₁.left)).map (Arrow.Hom.left sq))
          (sq₁₃.snd ≫ (G.obj (op f₁.right)).map (Arrow.Hom.right sq)) ⋯)
have h₁ : (map (𝟭 C₂) ((G.obj (op f₁.right)).map (Arrow.Hom.left sq)) ≫ (Arrow.mk sq₁₃'.π).hom) ≫ sq₁₃'.fst =
  ((Arrow.mk sq₁₃.π).hom ≫
      map (𝟭 C₂)
        (sorry.lift (sq₁₃.fst ≫ (G.obj (op f₁.left)).map (Arrow.Hom.left sq))
          (sq₁₃.snd ≫ (G.obj (op f₁.right)).map (Arrow.Hom.right sq)) sorry)) ≫
    sq₁₃'.fst
Tactic: apply PullbackObjObj.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 : G.PullbackObjObj f₁_1 f₃_1
f₁_2 f₁' : Arrow.{v₁, u₁} C₁
f₃_2 : Arrow.{v₃, u₃} C₃
sq₁₃_1 : G.PullbackObjObj f₁_2.hom f₃_2.hom
sq₁₃'_1 : G.PullbackObjObj f₁'.hom f₃_2.hom
f₁ : Arrow.{v₁, u₁} C₁
f₃ f₃' : Arrow.{v₃, u₃} C₃
sq₁₃ : G.PullbackObjObj f₁.hom f₃.hom
sq₁₃' : G.PullbackObjObj f₁.hom f₃'.hom
sq : f₃ ⟶ f₃'
h₁ :
  (map (𝟭 C₂) ((G.obj (op f₁.right)).map (Arrow.Hom.left sq)) ≫ (Arrow.mk sq₁₃'.π).hom) ≫ sq₁₃'.fst =
    ((Arrow.mk sq₁₃.π).hom ≫
        map (𝟭 C₂)
          (⋯.lift (sq₁₃.fst ≫ (G.obj (op f₁.left)).map (Arrow.Hom.left sq))
            (sq₁₃.snd ≫ (G.obj (op f₁.right)).map (Arrow.Hom.right sq)) ⋯)) ≫
      sq₁₃'.fst
⊢ map (𝟭 C₂) ((G.obj (op f₁.right)).map (Arrow.Hom.left sq)) ≫ (Arrow.mk sq₁₃'.π).hom =
    (Arrow.mk sq₁₃.π).hom ≫
      map (𝟭 C₂)
        (⋯.lift (sq₁₃.fst ≫ (G.obj (op f₁.left)).map (Arrow.Hom.left sq))
          (sq₁₃.snd ≫ (G.obj (op f₁.right)).map (Arrow.Hom.right sq)) ⋯)
have h₂ : (map (𝟭 C₂) ((G.obj (op f₁.right)).map (Arrow.Hom.left sq)) ≫ (Arrow.mk sq₁₃'.π).hom) ≫ sq₁₃'.snd =
  ((Arrow.mk sq₁₃.π).hom ≫
      map (𝟭 C₂)
        (sorry.lift (sq₁₃.fst ≫ (G.obj (op f₁.left)).map (Arrow.Hom.left sq))
          (sq₁₃.snd ≫ (G.obj (op f₁.right)).map (Arrow.Hom.right sq)) sorry)) ≫
    sq₁₃'.snd
Tactic: apply PullbackObjObj.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₂
adj₂ : F ⊣₂ G
inst_3 : HasPullbacks.{v₂, u₂} C₂
inst_4 : HasPushouts.{v₃, u₃} C₃
X₁ Y₁ : Arrow.{v₁, u₁} C₁
x : X₁ ⟶ Y₁
⊢ Adjunction.unit (LeibnizAdjunction.adj F G adj₂ X₁) ≫
      whiskerRight (F.leibnizPushout.map x) (G.leibnizPullback.obj (op X₁)) =
    Adjunction.unit (LeibnizAdjunction.adj F G adj₂ Y₁) ≫
      (F.leibnizPushout.obj Y₁).whiskerLeft (G.leibnizPullback.map x.op)
have w : ∀ (x_1 : Arrow.{v₂, u₂} C₂),
  Arrow.Hom.left
      ((Adjunction.unit (LeibnizAdjunction.adj F G adj₂ X₁) ≫
            whiskerRight (F.leibnizPushout.map x) (G.leibnizPullback.obj (op X₁))).app
        x_1) =
    Arrow.Hom.left
      ((Adjunction.unit (LeibnizAdjunction.adj F G adj₂ Y₁) ≫
            (F.leibnizPushout.obj Y₁).whiskerLeft (G.leibnizPullback.map x.op)).app
        x_1)
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₂
adj₂ : F ⊣₂ G
inst_3 : HasPullbacks.{v₂, u₂} C₂
inst_4 : HasPushouts.{v₃, u₃} C₃
X₁ Y₁ : Arrow.{v₁, u₁} C₁
x : X₁ ⟶ Y₁
w :
  ∀ (x_1 : Arrow.{v₂, u₂} C₂),
    Arrow.Hom.left
        ((Adjunction.unit (LeibnizAdjunction.adj F G adj₂ X₁) ≫
              whiskerRight (F.leibnizPushout.map x) (G.leibnizPullback.obj (op X₁))).app
          x_1) =
      Arrow.Hom.left
        ((Adjunction.unit (LeibnizAdjunction.adj F G adj₂ Y₁) ≫
              (F.leibnizPushout.obj Y₁).whiskerLeft (G.leibnizPullback.map x.op)).app
          x_1)
⊢ Adjunction.unit (LeibnizAdjunction.adj F G adj₂ X₁) ≫
      whiskerRight (F.leibnizPushout.map x) (G.leibnizPullback.obj (op X₁)) =
    Adjunction.unit (LeibnizAdjunction.adj F G adj₂ Y₁) ≫
      (F.leibnizPushout.obj Y₁).whiskerLeft (G.leibnizPullback.map x.op)
have w₁ : ∀ (x_1 : Arrow.{v₂, u₂} C₂),
  Arrow.Hom.right
      ((Adjunction.unit (LeibnizAdjunction.adj F G adj₂ X₁) ≫
            whiskerRight (F.leibnizPushout.map x) (G.leibnizPullback.obj (op X₁))).app
        x_1) =
    Arrow.Hom.right
      ((Adjunction.unit (LeibnizAdjunction.adj F G adj₂ Y₁) ≫
            (F.leibnizPushout.obj Y₁).whiskerLeft (G.leibnizPullback.map x.op)).app
        x_1)
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₂
adj₂ : F ⊣₂ G
inst_3 : HasPullbacks.{v₂, u₂} C₂
inst_4 : HasPushouts.{v₃, u₃} C₃
X₁ Y₁ : Arrow.{v₁, u₁} C₁
x : X₁ ⟶ Y₁
x_1 : Arrow.{v₂, u₂} C₂
⊢ Arrow.Hom.right
      ((Adjunction.unit (LeibnizAdjunction.adj F G adj₂ X₁) ≫
            whiskerRight (F.leibnizPushout.map x) (G.leibnizPullback.obj (op X₁))).app
        x_1) =
    Arrow.Hom.right
      ((Adjunction.unit (LeibnizAdjunction.adj F G adj₂ Y₁) ≫
            (F.leibnizPushout.obj Y₁).whiskerLeft (G.leibnizPullback.map x.op)).app
        x_1)
have w : Arrow.Hom.right
      ((Adjunction.unit (LeibnizAdjunction.adj F G adj₂ X₁) ≫
            whiskerRight (F.leibnizPushout.map x) (G.leibnizPullback.obj (op X₁))).app
        x_1) ≫
    pullback.fst ((G.obj (op (unop (op X₁)).left)).map ((F.leibnizPushout.obj Y₁).obj x_1).hom)
      ((G.map (unop (op X₁)).hom.op).app ((F.leibnizPushout.obj Y₁).obj x_1).right) =
  Arrow.Hom.right
      ((Adjunction.unit (LeibnizAdjunction.adj F G adj₂ Y₁) ≫
            (F.leibnizPushout.obj Y₁).whiskerLeft (G.leibnizPullback.map x.op)).app
        x_1) ≫
    pullback.fst ((G.obj (op (unop (op X₁)).left)).map ((F.leibnizPushout.obj Y₁).obj x_1).hom)
      ((G.map (unop (op X₁)).hom.op).app ((F.leibnizPushout.obj Y₁).obj x_1).right)
Tactic: apply pullback.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₂
adj₂ : F ⊣₂ G
inst_3 : HasPullbacks.{v₂, u₂} C₂
inst_4 : HasPushouts.{v₃, u₃} C₃
X₁ Y₁ : Arrow.{v₁, u₁} C₁
x : X₁ ⟶ Y₁
x_1 : Arrow.{v₂, u₂} C₂
w :
  Arrow.Hom.right
        ((Adjunction.unit (LeibnizAdjunction.adj F G adj₂ X₁) ≫
              whiskerRight (F.leibnizPushout.map x) (G.leibnizPullback.obj (op X₁))).app
          x_1) ≫
      pullback.fst ((G.obj (op (unop (op X₁)).left)).map ((F.leibnizPushout.obj Y₁).obj x_1).hom)
        ((G.map (unop (op X₁)).hom.op).app ((F.leibnizPushout.obj Y₁).obj x_1).right) =
    Arrow.Hom.right
        ((Adjunction.unit (LeibnizAdjunction.adj F G adj₂ Y₁) ≫
              (F.leibnizPushout.obj Y₁).whiskerLeft (G.leibnizPullback.map x.op)).app
          x_1) ≫
      pullback.fst ((G.obj (op (unop (op X₁)).left)).map ((F.leibnizPushout.obj Y₁).obj x_1).hom)
        ((G.map (unop (op X₁)).hom.op).app ((F.leibnizPushout.obj Y₁).obj x_1).right)
⊢ Arrow.Hom.right
      ((Adjunction.unit (LeibnizAdjunction.adj F G adj₂ X₁) ≫
            whiskerRight (F.leibnizPushout.map x) (G.leibnizPullback.obj (op X₁))).app
        x_1) =
    Arrow.Hom.right
      ((Adjunction.unit (LeibnizAdjunction.adj F G adj₂ Y₁) ≫
            (F.leibnizPushout.obj Y₁).whiskerLeft (G.leibnizPullback.map x.op)).app
        x_1)
have w₁ : Arrow.Hom.right
      ((Adjunction.unit (LeibnizAdjunction.adj F G adj₂ X₁) ≫
            whiskerRight (F.leibnizPushout.map x) (G.leibnizPullback.obj (op X₁))).app
        x_1) ≫
    pullback.snd ((G.obj (op (unop (op X₁)).left)).map ((F.leibnizPushout.obj Y₁).obj x_1).hom)
      ((G.map (unop (op X₁)).hom.op).app ((F.leibnizPushout.obj Y₁).obj x_1).right) =
  Arrow.Hom.right
      ((Adjunction.unit (LeibnizAdjunction.adj F G adj₂ Y₁) ≫
            (F.leibnizPushout.obj Y₁).whiskerLeft (G.leibnizPullback.map x.op)).app
        x_1) ≫
    pullback.snd ((G.obj (op (unop (op X₁)).left)).map ((F.leibnizPushout.obj Y₁).obj x_1).hom)
      ((G.map (unop (op X₁)).hom.op).app ((F.leibnizPushout.obj Y₁).obj x_1).right)
Tactic: apply pullback.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square (goal)
Goal:
C : Type u
inst : Category.{v, u} C
sq₁ sq₂ : Square.{v, u} C
h : sq₁.IsPullback
e : sq₁ ≅ sq₂
⊢ sq₂.IsPullback
have refine_1 : Eq (α := sq₁.X₁ ⟶ sq₂.X₂) (sq₁.f₁₂ ≫ Iso.hom (Functor.mapIso evaluation₂ e))
  (Iso.hom (Functor.mapIso evaluation₁ e) ≫ sq₂.f₁₂)
Tactic: refine CategoryTheory.IsPullback.of_iso h
    (evaluation₁.mapIso e) (evaluation₂.mapIso e)
    (evaluation₃.mapIso e) (evaluation₄.mapIso e) ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square (goal)
Goal:
C : Type u
inst : Category.{v, u} C
sq₁ sq₂ : Square.{v, u} C
h : sq₁.IsPullback
e : sq₁ ≅ sq₂
refine_1 :
  Eq (α := sq₁.X₁ ⟶ sq₂.X₂) (sq₁.f₁₂ ≫ Iso.hom (Functor.mapIso evaluation₂ e))
    (Iso.hom (Functor.mapIso evaluation₁ e) ≫ sq₂.f₁₂)
⊢ sq₂.IsPullback
have refine_2 : Eq (α := sq₁.X₁ ⟶ sq₂.X₃) (sq₁.f₁₃ ≫ Iso.hom (Functor.mapIso evaluation₃ e))
  (Iso.hom (Functor.mapIso evaluation₁ e) ≫ sq₂.f₁₃)
Tactic: refine CategoryTheory.IsPullback.of_iso h
    (evaluation₁.mapIso e) (evaluation₂.mapIso e)
    (evaluation₃.mapIso e) (evaluation₄.mapIso e) ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square (goal)
Goal:
C : Type u
inst : Category.{v, u} C
sq₁ sq₂ : Square.{v, u} C
h : sq₁.IsPullback
e : sq₁ ≅ sq₂
refine_1 :
  Eq (α := sq₁.X₁ ⟶ sq₂.X₂) (sq₁.f₁₂ ≫ Iso.hom (Functor.mapIso evaluation₂ e))
    (Iso.hom (Functor.mapIso evaluation₁ e) ≫ sq₂.f₁₂)
refine_2 :
  Eq (α := sq₁.X₁ ⟶ sq₂.X₃) (sq₁.f₁₃ ≫ Iso.hom (Functor.mapIso evaluation₃ e))
    (Iso.hom (Functor.mapIso evaluation₁ e) ≫ sq₂.f₁₃)
⊢ sq₂.IsPullback
have refine_3 : Eq (α := sq₁.X₂ ⟶ sq₂.X₄) (sq₁.f₂₄ ≫ Iso.hom (Functor.mapIso evaluation₄ e))
  (Iso.hom (Functor.mapIso evaluation₂ e) ≫ sq₂.f₂₄)
Tactic: refine CategoryTheory.IsPullback.of_iso h
    (evaluation₁.mapIso e) (evaluation₂.mapIso e)
    (evaluation₃.mapIso e) (evaluation₄.mapIso e) ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square (goal)
Goal:
C : Type u
inst : Category.{v, u} C
sq₁ sq₂ : Square.{v, u} C
h : sq₁.IsPullback
e : sq₁ ≅ sq₂
refine_1 :
  Eq (α := sq₁.X₁ ⟶ sq₂.X₂) (sq₁.f₁₂ ≫ Iso.hom (Functor.mapIso evaluation₂ e))
    (Iso.hom (Functor.mapIso evaluation₁ e) ≫ sq₂.f₁₂)
refine_2 :
  Eq (α := sq₁.X₁ ⟶ sq₂.X₃) (sq₁.f₁₃ ≫ Iso.hom (Functor.mapIso evaluation₃ e))
    (Iso.hom (Functor.mapIso evaluation₁ e) ≫ sq₂.f₁₃)
refine_3 :
  Eq (α := sq₁.X₂ ⟶ sq₂.X₄) (sq₁.f₂₄ ≫ Iso.hom (Functor.mapIso evaluation₄ e))
    (Iso.hom (Functor.mapIso evaluation₂ e) ≫ sq₂.f₂₄)
⊢ sq₂.IsPullback
have refine_4 : Eq (α := sq₁.X₃ ⟶ sq₂.X₄) (sq₁.f₃₄ ≫ Iso.hom (Functor.mapIso evaluation₄ e))
  (Iso.hom (Functor.mapIso evaluation₃ e) ≫ sq₂.f₃₄)
Tactic: refine CategoryTheory.IsPullback.of_iso h
    (evaluation₁.mapIso e) (evaluation₂.mapIso e)
    (evaluation₃.mapIso e) (evaluation₄.mapIso e) ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square (goal)
Goal:
C : Type u
inst : Category.{v, u} C
sq₁ sq₂ : Square.{v, u} C
h : sq₁.IsPushout
e : sq₁ ≅ sq₂
⊢ sq₂.IsPushout
have refine_1 : Eq (α := sq₁.X₁ ⟶ sq₂.X₂) (sq₁.f₁₂ ≫ Iso.hom (Functor.mapIso evaluation₂ e))
  (Iso.hom (Functor.mapIso evaluation₁ e) ≫ sq₂.f₁₂)
Tactic: refine CategoryTheory.IsPushout.of_iso h
    (evaluation₁.mapIso e) (evaluation₂.mapIso e)
    (evaluation₃.mapIso e) (evaluation₄.mapIso e) ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square (goal)
Goal:
C : Type u
inst : Category.{v, u} C
sq₁ sq₂ : Square.{v, u} C
h : sq₁.IsPushout
e : sq₁ ≅ sq₂
refine_1 :
  Eq (α := sq₁.X₁ ⟶ sq₂.X₂) (sq₁.f₁₂ ≫ Iso.hom (Functor.mapIso evaluation₂ e))
    (Iso.hom (Functor.mapIso evaluation₁ e) ≫ sq₂.f₁₂)
⊢ sq₂.IsPushout
have refine_2 : Eq (α := sq₁.X₁ ⟶ sq₂.X₃) (sq₁.f₁₃ ≫ Iso.hom (Functor.mapIso evaluation₃ e))
  (Iso.hom (Functor.mapIso evaluation₁ e) ≫ sq₂.f₁₃)
Tactic: refine CategoryTheory.IsPushout.of_iso h
    (evaluation₁.mapIso e) (evaluation₂.mapIso e)
    (evaluation₃.mapIso e) (evaluation₄.mapIso e) ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square (goal)
Goal:
C : Type u
inst : Category.{v, u} C
sq₁ sq₂ : Square.{v, u} C
h : sq₁.IsPushout
e : sq₁ ≅ sq₂
refine_1 :
  Eq (α := sq₁.X₁ ⟶ sq₂.X₂) (sq₁.f₁₂ ≫ Iso.hom (Functor.mapIso evaluation₂ e))
    (Iso.hom (Functor.mapIso evaluation₁ e) ≫ sq₂.f₁₂)
refine_2 :
  Eq (α := sq₁.X₁ ⟶ sq₂.X₃) (sq₁.f₁₃ ≫ Iso.hom (Functor.mapIso evaluation₃ e))
    (Iso.hom (Functor.mapIso evaluation₁ e) ≫ sq₂.f₁₃)
⊢ sq₂.IsPushout
have refine_3 : Eq (α := sq₁.X₂ ⟶ sq₂.X₄) (sq₁.f₂₄ ≫ Iso.hom (Functor.mapIso evaluation₄ e))
  (Iso.hom (Functor.mapIso evaluation₂ e) ≫ sq₂.f₂₄)
Tactic: refine CategoryTheory.IsPushout.of_iso h
    (evaluation₁.mapIso e) (evaluation₂.mapIso e)
    (evaluation₃.mapIso e) (evaluation₄.mapIso e) ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square (goal)
Goal:
C : Type u
inst : Category.{v, u} C
sq₁ sq₂ : Square.{v, u} C
h : sq₁.IsPushout
e : sq₁ ≅ sq₂
refine_1 :
  Eq (α := sq₁.X₁ ⟶ sq₂.X₂) (sq₁.f₁₂ ≫ Iso.hom (Functor.mapIso evaluation₂ e))
    (Iso.hom (Functor.mapIso evaluation₁ e) ≫ sq₂.f₁₂)
refine_2 :
  Eq (α := sq₁.X₁ ⟶ sq₂.X₃) (sq₁.f₁₃ ≫ Iso.hom (Functor.mapIso evaluation₃ e))
    (Iso.hom (Functor.mapIso evaluation₁ e) ≫ sq₂.f₁₃)
refine_3 :
  Eq (α := sq₁.X₂ ⟶ sq₂.X₄) (sq₁.f₂₄ ≫ Iso.hom (Functor.mapIso evaluation₄ e))
    (Iso.hom (Functor.mapIso evaluation₂ e) ≫ sq₂.f₂₄)
⊢ sq₂.IsPushout
have refine_4 : Eq (α := sq₁.X₃ ⟶ sq₂.X₄) (sq₁.f₃₄ ≫ Iso.hom (Functor.mapIso evaluation₄ e))
  (Iso.hom (Functor.mapIso evaluation₃ e) ≫ sq₂.f₃₄)
Tactic: refine CategoryTheory.IsPushout.of_iso h
    (evaluation₁.mapIso e) (evaluation₂.mapIso e)
    (evaluation₃.mapIso e) (evaluation₄.mapIso e) ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
sq : Square.{v, u} C
h : sq.IsPullback
inst_1 : Mono sq.f₃₄
⊢ Mono sq.f₁₂
have this : Mono sq.flip.f₂₄
Tactic: have : Mono sq.flip.f₂₄ := by dsimp; infer_instance
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
sq : Square.{v, u} C
h : sq.IsPushout
inst_1 : Epi sq.f₁₂
⊢ Epi sq.f₃₄
have this : Epi sq.flip.f₁₃
Tactic: have : Epi sq.flip.f₁₃ := by dsimp; infer_instance
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
A B_1 : C
f g : A ⟶ B_1
F : Functor.{v, v₂, u, u₂} C D
G : Functor.{v₂, v, u₂, u} D C
adj : F ⊣ G
B : D
⊢ F.map (adj.unit.app (G.obj B)) ≫ F.map (G.map (adj.counit.app B)) =
    𝟙 (F.obj (G.obj (Functor.obj.{v₂, v₂, u₂, u₂} (𝟭 D) B)))
have rw : F.map (𝟙 (G.obj B)) = 𝟙 (F.obj (G.obj (Functor.obj.{v₂, v₂, u₂, u₂} (𝟭 D) B)))
Tactic: rw [← F.map_comp, adj.right_triangle_components]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
Goal:
X Y : WalkingReflexivePair
f : X.Hom Y
⊢ (Hom.id X).comp f = f
have left : (Hom.id one).comp Hom.left = Hom.left
Tactic: cases f
Cleared hypotheses: X, Y, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
Goal:
X Y : WalkingReflexivePair
f : X.Hom Y
left : (Hom.id one).comp Hom.left = Hom.left
⊢ (Hom.id X).comp f = f
have right : (Hom.id one).comp Hom.right = Hom.right
Tactic: cases f
Cleared hypotheses: X, Y, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
Goal:
X Y : WalkingReflexivePair
f : X.Hom Y
left : (Hom.id one).comp Hom.left = Hom.left
right : (Hom.id one).comp Hom.right = Hom.right
⊢ (Hom.id X).comp f = f
have reflexion : (Hom.id zero).comp Hom.reflexion = Hom.reflexion
Tactic: cases f
Cleared hypotheses: X, Y, f