awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.LiftingProperties.ParametrizedAdjunction
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
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
X₃ Y₃ : C₃
f₃ : X₃ ⟶ Y₃
sq₁₂ : F.PushoutObjObj f₁ f₂
sq₁₃ : G.PullbackObjObj f₁ f₃
α : Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃
⊢ sq₁₂.inl ≫
      Arrow.Hom.left
        ((fun (β : Arrow.mk f₂ ⟶ Arrow.mk sq₁₃.π) ↦
            (Arrow.homMk
                (⋯.desc
                  (((Equiv.symm adj₂.homEquiv :
                        Equiv.{v₂ + 1, v₃ + 1} (X₂ ⟶ (G.obj (op Y₁)).obj (Arrow.mk f₃).left)
                          ((F.obj Y₁).obj X₂ ⟶ (Arrow.mk f₃).left)) :
                      (a : X₂ ⟶ (G.obj (op Y₁)).obj (Arrow.mk f₃).left) → (F.obj Y₁).obj X₂ ⟶ (Arrow.mk f₃).left)
                    (Arrow.Hom.left β))
                  (((Equiv.symm adj₂.homEquiv :
                        Equiv.{v₂ + 1, v₃ + 1} (Y₂ ⟶ (G.obj (op X₁)).obj (Arrow.mk f₃).left)
                          ((F.obj X₁).obj Y₂ ⟶ (Arrow.mk f₃).left)) :
                      (a : Y₂ ⟶ (G.obj (op X₁)).obj (Arrow.mk f₃).left) → (F.obj X₁).obj Y₂ ⟶ (Arrow.mk f₃).left)
                    (Arrow.Hom.right β ≫ sq₁₃.fst))
                  ⋯)
                (((Equiv.symm adj₂.homEquiv :
                      Equiv.{v₂ + 1, v₃ + 1} (Y₂ ⟶ (G.obj (op Y₁)).obj (Arrow.mk f₃).right)
                        ((F.obj Y₁).obj Y₂ ⟶ (Arrow.mk f₃).right)) :
                    (a : Y₂ ⟶ (G.obj (op Y₁)).obj (Arrow.mk f₃).right) → (F.obj Y₁).obj Y₂ ⟶ (Arrow.mk f₃).right)
                  (Arrow.Hom.right β ≫ sq₁₃.snd))
                ⋯ :
              Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃))
          ((fun (α : Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃) ↦
              (Arrow.homMk
                  (((adj₂.homEquiv :
                        Equiv.{v₃ + 1, v₂ + 1} ((F.obj Y₁).obj (Arrow.mk f₂).left ⟶ X₃)
                          ((Arrow.mk f₂).left ⟶ (G.obj (op Y₁)).obj X₃)) :
                      (a : (F.obj Y₁).obj (Arrow.mk f₂).left ⟶ X₃) → (Arrow.mk f₂).left ⟶ (G.obj (op Y₁)).obj X₃)
                    (sq₁₂.inl ≫ Arrow.Hom.left α))
                  (⋯.lift
                    (((adj₂.homEquiv :
                          Equiv.{v₃ + 1, v₂ + 1} ((F.obj X₁).obj (Arrow.mk f₂).right ⟶ X₃)
                            ((Arrow.mk f₂).right ⟶ (G.obj (op X₁)).obj X₃)) :
                        (a : (F.obj X₁).obj (Arrow.mk f₂).right ⟶ X₃) → (Arrow.mk f₂).right ⟶ (G.obj (op X₁)).obj X₃)
                      (sq₁₂.inr ≫ Arrow.Hom.left α))
                    (((adj₂.homEquiv :
                          Equiv.{v₃ + 1, v₂ + 1} ((F.obj Y₁).obj (Arrow.mk f₂).right ⟶ Y₃)
                            ((Arrow.mk f₂).right ⟶ (G.obj (op Y₁)).obj Y₃)) :
                        (a : (F.obj Y₁).obj (Arrow.mk f₂).right ⟶ Y₃) → (Arrow.mk f₂).right ⟶ (G.obj (op Y₁)).obj Y₃)
                      (Arrow.Hom.right α))
                    ⋯)
                  ⋯ :
                Arrow.mk f₂ ⟶ Arrow.mk sq₁₃.π))
            α)) =
    sq₁₂.inl ≫ Arrow.Hom.left α

Tactic:
simp
-- Module: Mathlib.CategoryTheory.LiftingProperties.ParametrizedAdjunction
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
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
X₃ Y₃ : C₃
f₃ : X₃ ⟶ Y₃
sq₁₂ : F.PushoutObjObj f₁ f₂
sq₁₃ : G.PullbackObjObj f₁ f₃
α : Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃
⊢ sq₁₂.inr ≫
      Arrow.Hom.left
        ((fun (β : Arrow.mk f₂ ⟶ Arrow.mk sq₁₃.π) ↦
            (Arrow.homMk
                (⋯.desc
                  (((Equiv.symm adj₂.homEquiv :
                        Equiv.{v₂ + 1, v₃ + 1} (X₂ ⟶ (G.obj (op Y₁)).obj (Arrow.mk f₃).left)
                          ((F.obj Y₁).obj X₂ ⟶ (Arrow.mk f₃).left)) :
                      (a : X₂ ⟶ (G.obj (op Y₁)).obj (Arrow.mk f₃).left) → (F.obj Y₁).obj X₂ ⟶ (Arrow.mk f₃).left)
                    (Arrow.Hom.left β))
                  (((Equiv.symm adj₂.homEquiv :
                        Equiv.{v₂ + 1, v₃ + 1} (Y₂ ⟶ (G.obj (op X₁)).obj (Arrow.mk f₃).left)
                          ((F.obj X₁).obj Y₂ ⟶ (Arrow.mk f₃).left)) :
                      (a : Y₂ ⟶ (G.obj (op X₁)).obj (Arrow.mk f₃).left) → (F.obj X₁).obj Y₂ ⟶ (Arrow.mk f₃).left)
                    (Arrow.Hom.right β ≫ sq₁₃.fst))
                  ⋯)
                (((Equiv.symm adj₂.homEquiv :
                      Equiv.{v₂ + 1, v₃ + 1} (Y₂ ⟶ (G.obj (op Y₁)).obj (Arrow.mk f₃).right)
                        ((F.obj Y₁).obj Y₂ ⟶ (Arrow.mk f₃).right)) :
                    (a : Y₂ ⟶ (G.obj (op Y₁)).obj (Arrow.mk f₃).right) → (F.obj Y₁).obj Y₂ ⟶ (Arrow.mk f₃).right)
                  (Arrow.Hom.right β ≫ sq₁₃.snd))
                ⋯ :
              Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃))
          ((fun (α : Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃) ↦
              (Arrow.homMk
                  (((adj₂.homEquiv :
                        Equiv.{v₃ + 1, v₂ + 1} ((F.obj Y₁).obj (Arrow.mk f₂).left ⟶ X₃)
                          ((Arrow.mk f₂).left ⟶ (G.obj (op Y₁)).obj X₃)) :
                      (a : (F.obj Y₁).obj (Arrow.mk f₂).left ⟶ X₃) → (Arrow.mk f₂).left ⟶ (G.obj (op Y₁)).obj X₃)
                    (sq₁₂.inl ≫ Arrow.Hom.left α))
                  (⋯.lift
                    (((adj₂.homEquiv :
                          Equiv.{v₃ + 1, v₂ + 1} ((F.obj X₁).obj (Arrow.mk f₂).right ⟶ X₃)
                            ((Arrow.mk f₂).right ⟶ (G.obj (op X₁)).obj X₃)) :
                        (a : (F.obj X₁).obj (Arrow.mk f₂).right ⟶ X₃) → (Arrow.mk f₂).right ⟶ (G.obj (op X₁)).obj X₃)
                      (sq₁₂.inr ≫ Arrow.Hom.left α))
                    (((adj₂.homEquiv :
                          Equiv.{v₃ + 1, v₂ + 1} ((F.obj Y₁).obj (Arrow.mk f₂).right ⟶ Y₃)
                            ((Arrow.mk f₂).right ⟶ (G.obj (op Y₁)).obj Y₃)) :
                        (a : (F.obj Y₁).obj (Arrow.mk f₂).right ⟶ Y₃) → (Arrow.mk f₂).right ⟶ (G.obj (op Y₁)).obj Y₃)
                      (Arrow.Hom.right α))
                    ⋯)
                  ⋯ :
                Arrow.mk f₂ ⟶ Arrow.mk sq₁₃.π))
            α)) =
    sq₁₂.inr ≫ Arrow.Hom.left α

Tactic:
simp
-- Module: Mathlib.CategoryTheory.LiftingProperties.ParametrizedAdjunction
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
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
X₃ Y₃ : C₃
f₃ : X₃ ⟶ Y₃
sq₁₂ : F.PushoutObjObj f₁ f₂
sq₁₃ : G.PullbackObjObj f₁ f₃
α : Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃
⊢ Arrow.Hom.right
      ((fun (β : Arrow.mk f₂ ⟶ Arrow.mk sq₁₃.π) ↦
          (Arrow.homMk
              (⋯.desc
                (((Equiv.symm adj₂.homEquiv :
                      Equiv.{v₂ + 1, v₃ + 1} (X₂ ⟶ (G.obj (op Y₁)).obj (Arrow.mk f₃).left)
                        ((F.obj Y₁).obj X₂ ⟶ (Arrow.mk f₃).left)) :
                    (a : X₂ ⟶ (G.obj (op Y₁)).obj (Arrow.mk f₃).left) → (F.obj Y₁).obj X₂ ⟶ (Arrow.mk f₃).left)
                  (Arrow.Hom.left β))
                (((Equiv.symm adj₂.homEquiv :
                      Equiv.{v₂ + 1, v₃ + 1} (Y₂ ⟶ (G.obj (op X₁)).obj (Arrow.mk f₃).left)
                        ((F.obj X₁).obj Y₂ ⟶ (Arrow.mk f₃).left)) :
                    (a : Y₂ ⟶ (G.obj (op X₁)).obj (Arrow.mk f₃).left) → (F.obj X₁).obj Y₂ ⟶ (Arrow.mk f₃).left)
                  (Arrow.Hom.right β ≫ sq₁₃.fst))
                ⋯)
              (((Equiv.symm adj₂.homEquiv :
                    Equiv.{v₂ + 1, v₃ + 1} (Y₂ ⟶ (G.obj (op Y₁)).obj (Arrow.mk f₃).right)
                      ((F.obj Y₁).obj Y₂ ⟶ (Arrow.mk f₃).right)) :
                  (a : Y₂ ⟶ (G.obj (op Y₁)).obj (Arrow.mk f₃).right) → (F.obj Y₁).obj Y₂ ⟶ (Arrow.mk f₃).right)
                (Arrow.Hom.right β ≫ sq₁₃.snd))
              ⋯ :
            Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃))
        ((fun (α : Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃) ↦
            (Arrow.homMk
                (((adj₂.homEquiv :
                      Equiv.{v₃ + 1, v₂ + 1} ((F.obj Y₁).obj (Arrow.mk f₂).left ⟶ X₃)
                        ((Arrow.mk f₂).left ⟶ (G.obj (op Y₁)).obj X₃)) :
                    (a : (F.obj Y₁).obj (Arrow.mk f₂).left ⟶ X₃) → (Arrow.mk f₂).left ⟶ (G.obj (op Y₁)).obj X₃)
                  (sq₁₂.inl ≫ Arrow.Hom.left α))
                (⋯.lift
                  (((adj₂.homEquiv :
                        Equiv.{v₃ + 1, v₂ + 1} ((F.obj X₁).obj (Arrow.mk f₂).right ⟶ X₃)
                          ((Arrow.mk f₂).right ⟶ (G.obj (op X₁)).obj X₃)) :
                      (a : (F.obj X₁).obj (Arrow.mk f₂).right ⟶ X₃) → (Arrow.mk f₂).right ⟶ (G.obj (op X₁)).obj X₃)
                    (sq₁₂.inr ≫ Arrow.Hom.left α))
                  (((adj₂.homEquiv :
                        Equiv.{v₃ + 1, v₂ + 1} ((F.obj Y₁).obj (Arrow.mk f₂).right ⟶ Y₃)
                          ((Arrow.mk f₂).right ⟶ (G.obj (op Y₁)).obj Y₃)) :
                      (a : (F.obj Y₁).obj (Arrow.mk f₂).right ⟶ Y₃) → (Arrow.mk f₂).right ⟶ (G.obj (op Y₁)).obj Y₃)
                    (Arrow.Hom.right α))
                  ⋯)
                ⋯ :
              Arrow.mk f₂ ⟶ Arrow.mk sq₁₃.π))
          α)) =
    Arrow.Hom.right α

Tactic:
simp
-- Module: Mathlib.CategoryTheory.LiftingProperties.ParametrizedAdjunction
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
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
X₃ Y₃ : C₃
f₃ : X₃ ⟶ Y₃
sq₁₂ : F.PushoutObjObj f₁ f₂
sq₁₃ : G.PullbackObjObj f₁ f₃
β : Arrow.mk f₂ ⟶ Arrow.mk sq₁₃.π
⊢ Arrow.Hom.left
      ((fun (α : Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃) ↦
          (Arrow.homMk
              (((adj₂.homEquiv :
                    Equiv.{v₃ + 1, v₂ + 1} ((F.obj Y₁).obj (Arrow.mk f₂).left ⟶ X₃)
                      ((Arrow.mk f₂).left ⟶ (G.obj (op Y₁)).obj X₃)) :
                  (a : (F.obj Y₁).obj (Arrow.mk f₂).left ⟶ X₃) → (Arrow.mk f₂).left ⟶ (G.obj (op Y₁)).obj X₃)
                (sq₁₂.inl ≫ Arrow.Hom.left α))
              (⋯.lift
                (((adj₂.homEquiv :
                      Equiv.{v₃ + 1, v₂ + 1} ((F.obj X₁).obj (Arrow.mk f₂).right ⟶ X₃)
                        ((Arrow.mk f₂).right ⟶ (G.obj (op X₁)).obj X₃)) :
                    (a : (F.obj X₁).obj (Arrow.mk f₂).right ⟶ X₃) → (Arrow.mk f₂).right ⟶ (G.obj (op X₁)).obj X₃)
                  (sq₁₂.inr ≫ Arrow.Hom.left α))
                (((adj₂.homEquiv :
                      Equiv.{v₃ + 1, v₂ + 1} ((F.obj Y₁).obj (Arrow.mk f₂).right ⟶ Y₃)
                        ((Arrow.mk f₂).right ⟶ (G.obj (op Y₁)).obj Y₃)) :
                    (a : (F.obj Y₁).obj (Arrow.mk f₂).right ⟶ Y₃) → (Arrow.mk f₂).right ⟶ (G.obj (op Y₁)).obj Y₃)
                  (Arrow.Hom.right α))
                ⋯)
              ⋯ :
            Arrow.mk f₂ ⟶ Arrow.mk sq₁₃.π))
        ((fun (β : Arrow.mk f₂ ⟶ Arrow.mk sq₁₃.π) ↦
            (Arrow.homMk
                (⋯.desc
                  (((Equiv.symm adj₂.homEquiv :
                        Equiv.{v₂ + 1, v₃ + 1} (X₂ ⟶ (G.obj (op Y₁)).obj (Arrow.mk f₃).left)
                          ((F.obj Y₁).obj X₂ ⟶ (Arrow.mk f₃).left)) :
                      (a : X₂ ⟶ (G.obj (op Y₁)).obj (Arrow.mk f₃).left) → (F.obj Y₁).obj X₂ ⟶ (Arrow.mk f₃).left)
                    (Arrow.Hom.left β))
                  (((Equiv.symm adj₂.homEquiv :
                        Equiv.{v₂ + 1, v₃ + 1} (Y₂ ⟶ (G.obj (op X₁)).obj (Arrow.mk f₃).left)
                          ((F.obj X₁).obj Y₂ ⟶ (Arrow.mk f₃).left)) :
                      (a : Y₂ ⟶ (G.obj (op X₁)).obj (Arrow.mk f₃).left) → (F.obj X₁).obj Y₂ ⟶ (Arrow.mk f₃).left)
                    (Arrow.Hom.right β ≫ sq₁₃.fst))
                  ⋯)
                (((Equiv.symm adj₂.homEquiv :
                      Equiv.{v₂ + 1, v₃ + 1} (Y₂ ⟶ (G.obj (op Y₁)).obj (Arrow.mk f₃).right)
                        ((F.obj Y₁).obj Y₂ ⟶ (Arrow.mk f₃).right)) :
                    (a : Y₂ ⟶ (G.obj (op Y₁)).obj (Arrow.mk f₃).right) → (F.obj Y₁).obj Y₂ ⟶ (Arrow.mk f₃).right)
                  (Arrow.Hom.right β ≫ sq₁₃.snd))
                ⋯ :
              Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃))
          β)) =
    Arrow.Hom.left β

Tactic:
simp
-- Module: Mathlib.CategoryTheory.LiftingProperties.ParametrizedAdjunction
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
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
X₃ Y₃ : C₃
f₃ : X₃ ⟶ Y₃
sq₁₂ : F.PushoutObjObj f₁ f₂
sq₁₃ : G.PullbackObjObj f₁ f₃
β : Arrow.mk f₂ ⟶ Arrow.mk sq₁₃.π
⊢ Arrow.Hom.right
        ((fun (α : Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃) ↦
            (Arrow.homMk
                (((adj₂.homEquiv :
                      Equiv.{v₃ + 1, v₂ + 1} ((F.obj Y₁).obj (Arrow.mk f₂).left ⟶ X₃)
                        ((Arrow.mk f₂).left ⟶ (G.obj (op Y₁)).obj X₃)) :
                    (a : (F.obj Y₁).obj (Arrow.mk f₂).left ⟶ X₃) → (Arrow.mk f₂).left ⟶ (G.obj (op Y₁)).obj X₃)
                  (sq₁₂.inl ≫ Arrow.Hom.left α))
                (⋯.lift
                  (((adj₂.homEquiv :
                        Equiv.{v₃ + 1, v₂ + 1} ((F.obj X₁).obj (Arrow.mk f₂).right ⟶ X₃)
                          ((Arrow.mk f₂).right ⟶ (G.obj (op X₁)).obj X₃)) :
                      (a : (F.obj X₁).obj (Arrow.mk f₂).right ⟶ X₃) → (Arrow.mk f₂).right ⟶ (G.obj (op X₁)).obj X₃)
                    (sq₁₂.inr ≫ Arrow.Hom.left α))
                  (((adj₂.homEquiv :
                        Equiv.{v₃ + 1, v₂ + 1} ((F.obj Y₁).obj (Arrow.mk f₂).right ⟶ Y₃)
                          ((Arrow.mk f₂).right ⟶ (G.obj (op Y₁)).obj Y₃)) :
                      (a : (F.obj Y₁).obj (Arrow.mk f₂).right ⟶ Y₃) → (Arrow.mk f₂).right ⟶ (G.obj (op Y₁)).obj Y₃)
                    (Arrow.Hom.right α))
                  ⋯)
                ⋯ :
              Arrow.mk f₂ ⟶ Arrow.mk sq₁₃.π))
          ((fun (β : Arrow.mk f₂ ⟶ Arrow.mk sq₁₃.π) ↦
              (Arrow.homMk
                  (⋯.desc
                    (((Equiv.symm adj₂.homEquiv :
                          Equiv.{v₂ + 1, v₃ + 1} (X₂ ⟶ (G.obj (op Y₁)).obj (Arrow.mk f₃).left)
                            ((F.obj Y₁).obj X₂ ⟶ (Arrow.mk f₃).left)) :
                        (a : X₂ ⟶ (G.obj (op Y₁)).obj (Arrow.mk f₃).left) → (F.obj Y₁).obj X₂ ⟶ (Arrow.mk f₃).left)
                      (Arrow.Hom.left β))
                    (((Equiv.symm adj₂.homEquiv :
                          Equiv.{v₂ + 1, v₃ + 1} (Y₂ ⟶ (G.obj (op X₁)).obj (Arrow.mk f₃).left)
                            ((F.obj X₁).obj Y₂ ⟶ (Arrow.mk f₃).left)) :
                        (a : Y₂ ⟶ (G.obj (op X₁)).obj (Arrow.mk f₃).left) → (F.obj X₁).obj Y₂ ⟶ (Arrow.mk f₃).left)
                      (Arrow.Hom.right β ≫ sq₁₃.fst))
                    ⋯)
                  (((Equiv.symm adj₂.homEquiv :
                        Equiv.{v₂ + 1, v₃ + 1} (Y₂ ⟶ (G.obj (op Y₁)).obj (Arrow.mk f₃).right)
                          ((F.obj Y₁).obj Y₂ ⟶ (Arrow.mk f₃).right)) :
                      (a : Y₂ ⟶ (G.obj (op Y₁)).obj (Arrow.mk f₃).right) → (F.obj Y₁).obj Y₂ ⟶ (Arrow.mk f₃).right)
                    (Arrow.Hom.right β ≫ sq₁₃.snd))
                  ⋯ :
                Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃))
            β)) ≫
      sq₁₃.fst =
    Arrow.Hom.right β ≫ sq₁₃.fst

Tactic:
simp
-- Module: Mathlib.CategoryTheory.LiftingProperties.ParametrizedAdjunction
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
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
X₃ Y₃ : C₃
f₃ : X₃ ⟶ Y₃
sq₁₂ : F.PushoutObjObj f₁ f₂
sq₁₃ : G.PullbackObjObj f₁ f₃
β : Arrow.mk f₂ ⟶ Arrow.mk sq₁₃.π
⊢ Arrow.Hom.right
        ((fun (α : Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃) ↦
            (Arrow.homMk
                (((adj₂.homEquiv :
                      Equiv.{v₃ + 1, v₂ + 1} ((F.obj Y₁).obj (Arrow.mk f₂).left ⟶ X₃)
                        ((Arrow.mk f₂).left ⟶ (G.obj (op Y₁)).obj X₃)) :
                    (a : (F.obj Y₁).obj (Arrow.mk f₂).left ⟶ X₃) → (Arrow.mk f₂).left ⟶ (G.obj (op Y₁)).obj X₃)
                  (sq₁₂.inl ≫ Arrow.Hom.left α))
                (⋯.lift
                  (((adj₂.homEquiv :
                        Equiv.{v₃ + 1, v₂ + 1} ((F.obj X₁).obj (Arrow.mk f₂).right ⟶ X₃)
                          ((Arrow.mk f₂).right ⟶ (G.obj (op X₁)).obj X₃)) :
                      (a : (F.obj X₁).obj (Arrow.mk f₂).right ⟶ X₃) → (Arrow.mk f₂).right ⟶ (G.obj (op X₁)).obj X₃)
                    (sq₁₂.inr ≫ Arrow.Hom.left α))
                  (((adj₂.homEquiv :
                        Equiv.{v₃ + 1, v₂ + 1} ((F.obj Y₁).obj (Arrow.mk f₂).right ⟶ Y₃)
                          ((Arrow.mk f₂).right ⟶ (G.obj (op Y₁)).obj Y₃)) :
                      (a : (F.obj Y₁).obj (Arrow.mk f₂).right ⟶ Y₃) → (Arrow.mk f₂).right ⟶ (G.obj (op Y₁)).obj Y₃)
                    (Arrow.Hom.right α))
                  ⋯)
                ⋯ :
              Arrow.mk f₂ ⟶ Arrow.mk sq₁₃.π))
          ((fun (β : Arrow.mk f₂ ⟶ Arrow.mk sq₁₃.π) ↦
              (Arrow.homMk
                  (⋯.desc
                    (((Equiv.symm adj₂.homEquiv :
                          Equiv.{v₂ + 1, v₃ + 1} (X₂ ⟶ (G.obj (op Y₁)).obj (Arrow.mk f₃).left)
                            ((F.obj Y₁).obj X₂ ⟶ (Arrow.mk f₃).left)) :
                        (a : X₂ ⟶ (G.obj (op Y₁)).obj (Arrow.mk f₃).left) → (F.obj Y₁).obj X₂ ⟶ (Arrow.mk f₃).left)
                      (Arrow.Hom.left β))
                    (((Equiv.symm adj₂.homEquiv :
                          Equiv.{v₂ + 1, v₃ + 1} (Y₂ ⟶ (G.obj (op X₁)).obj (Arrow.mk f₃).left)
                            ((F.obj X₁).obj Y₂ ⟶ (Arrow.mk f₃).left)) :
                        (a : Y₂ ⟶ (G.obj (op X₁)).obj (Arrow.mk f₃).left) → (F.obj X₁).obj Y₂ ⟶ (Arrow.mk f₃).left)
                      (Arrow.Hom.right β ≫ sq₁₃.fst))
                    ⋯)
                  (((Equiv.symm adj₂.homEquiv :
                        Equiv.{v₂ + 1, v₃ + 1} (Y₂ ⟶ (G.obj (op Y₁)).obj (Arrow.mk f₃).right)
                          ((F.obj Y₁).obj Y₂ ⟶ (Arrow.mk f₃).right)) :
                      (a : Y₂ ⟶ (G.obj (op Y₁)).obj (Arrow.mk f₃).right) → (F.obj Y₁).obj Y₂ ⟶ (Arrow.mk f₃).right)
                    (Arrow.Hom.right β ≫ sq₁₃.snd))
                  ⋯ :
                Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃))
            β)) ≫
      sq₁₃.snd =
    Arrow.Hom.right β ≫ sq₁₃.snd

Tactic:
simp
-- Module: Mathlib.CategoryTheory.LiftingProperties.ParametrizedAdjunction
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
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
X₃ Y₃ : C₃
f₃ : X₃ ⟶ Y₃
sq₁₂ : F.PushoutObjObj f₁ f₂
sq₁₃ : G.PullbackObjObj f₁ f₃
α : Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃
⊢ Eq.{v₂ + 1} (α := (Arrow.mk f₂).right ⟶ (G.obj (op X₁)).obj X₃)
    (Arrow.Hom.right
          ((adj₂.arrowHomEquiv sq₁₂ sq₁₃ : (a : Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃) → Arrow.mk f₂ ⟶ Arrow.mk sq₁₃.π) α) ≫
        sq₁₃.fst :
      (Arrow.mk f₂).right ⟶ (G.obj (op X₁)).obj X₃)
    (((adj₂.homEquiv :
            Equiv.{v₃ + 1, v₂ + 1} ((F.obj X₁).obj Y₂ ⟶ (Arrow.mk f₃).left)
              (Y₂ ⟶ (G.obj (op X₁)).obj (Arrow.mk f₃).left)) :
          (a : (F.obj X₁).obj Y₂ ⟶ (Arrow.mk f₃).left) → Y₂ ⟶ (G.obj (op X₁)).obj (Arrow.mk f₃).left)
        (sq₁₂.inr ≫ Arrow.Hom.left α) :
      Y₂ ⟶ (G.obj (op X₁)).obj (Arrow.mk f₃).left)

Tactic:
IsPullback.lift_fst _ _ _ _

Premises used: CategoryTheory.Limits.PullbackCone.IsLimit.lift, CategoryTheory.IsPullback.lift_fst, CategoryTheory.IsPullback.lift
-- Module: Mathlib.CategoryTheory.LiftingProperties.ParametrizedAdjunction
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
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
X₃ Y₃ : C₃
f₃ : X₃ ⟶ Y₃
sq₁₂ : F.PushoutObjObj f₁ f₂
sq₁₃ : G.PullbackObjObj f₁ f₃
α : Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃
⊢ Eq.{v₂ + 1} (α := (Arrow.mk f₂).right ⟶ (G.obj (op Y₁)).obj Y₃)
    (Arrow.Hom.right
          ((adj₂.arrowHomEquiv sq₁₂ sq₁₃ : (a : Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃) → Arrow.mk f₂ ⟶ Arrow.mk sq₁₃.π) α) ≫
        sq₁₃.snd :
      (Arrow.mk f₂).right ⟶ (G.obj (op Y₁)).obj Y₃)
    (((adj₂.homEquiv :
            Equiv.{v₃ + 1, v₂ + 1} ((F.obj Y₁).obj Y₂ ⟶ (Arrow.mk f₃).right)
              (Y₂ ⟶ (G.obj (op Y₁)).obj (Arrow.mk f₃).right)) :
          (a : (F.obj Y₁).obj Y₂ ⟶ (Arrow.mk f₃).right) → Y₂ ⟶ (G.obj (op Y₁)).obj (Arrow.mk f₃).right)
        (Arrow.Hom.right α) :
      Y₂ ⟶ (G.obj (op Y₁)).obj (Arrow.mk f₃).right)

Tactic:
IsPullback.lift_snd _ _ _ _

Premises used: CategoryTheory.IsPullback.lift_snd, CategoryTheory.Limits.PullbackCone.IsLimit.lift, CategoryTheory.IsPullback.lift
-- Module: Mathlib.CategoryTheory.LiftingProperties.ParametrizedAdjunction
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
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
X₃ Y₃ : C₃
f₃ : X₃ ⟶ Y₃
sq₁₂ : F.PushoutObjObj f₁ f₂
sq₁₃ : G.PullbackObjObj f₁ f₃
β : Arrow.mk f₂ ⟶ Arrow.mk sq₁₃.π
⊢ Eq (α := (F.obj Y₁).obj X₂ ⟶ (Arrow.mk f₃).left)
    (sq₁₂.inl ≫
      Arrow.Hom.left
        (((adj₂.arrowHomEquiv sq₁₂ sq₁₃).symm : (a : Arrow.mk f₂ ⟶ Arrow.mk sq₁₃.π) → Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃) β))
    (((Equiv.symm adj₂.homEquiv :
          Equiv.{v₂ + 1, v₃ + 1} ((Arrow.mk f₂).left ⟶ (G.obj (op Y₁)).obj X₃)
            ((F.obj Y₁).obj (Arrow.mk f₂).left ⟶ X₃)) :
        (a : (Arrow.mk f₂).left ⟶ (G.obj (op Y₁)).obj X₃) → (F.obj Y₁).obj (Arrow.mk f₂).left ⟶ X₃)
      (Arrow.Hom.left β))

Tactic:
IsPushout.inl_desc _ _ _ _

Premises used: CategoryTheory.IsPushout.inl_desc, CategoryTheory.Limits.PushoutCocone.IsColimit.desc, CategoryTheory.IsPushout.desc
-- Module: Mathlib.CategoryTheory.LiftingProperties.ParametrizedAdjunction
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
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
X₃ Y₃ : C₃
f₃ : X₃ ⟶ Y₃
sq₁₂ : F.PushoutObjObj f₁ f₂
sq₁₃ : G.PullbackObjObj f₁ f₃
β : Arrow.mk f₂ ⟶ Arrow.mk sq₁₃.π
⊢ Eq (α := (F.obj X₁).obj Y₂ ⟶ (Arrow.mk f₃).left)
    (sq₁₂.inr ≫
      Arrow.Hom.left
        (((adj₂.arrowHomEquiv sq₁₂ sq₁₃).symm : (a : Arrow.mk f₂ ⟶ Arrow.mk sq₁₃.π) → Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃) β))
    (((Equiv.symm adj₂.homEquiv :
          Equiv.{v₂ + 1, v₃ + 1} ((Arrow.mk f₂).right ⟶ (G.obj (op X₁)).obj X₃)
            ((F.obj X₁).obj (Arrow.mk f₂).right ⟶ X₃)) :
        (a : (Arrow.mk f₂).right ⟶ (G.obj (op X₁)).obj X₃) → (F.obj X₁).obj (Arrow.mk f₂).right ⟶ X₃)
      (Arrow.Hom.right β ≫ sq₁₃.fst))

Tactic:
IsPushout.inr_desc _ _ _ _

Premises used: CategoryTheory.Limits.PushoutCocone.IsColimit.desc, CategoryTheory.IsPushout.inr_desc, CategoryTheory.IsPushout.desc
-- Module: Mathlib.CategoryTheory.LiftingProperties.ParametrizedAdjunction
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
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
X₃ Y₃ : C₃
f₃ : X₃ ⟶ Y₃
sq₁₂ : F.PushoutObjObj f₁ f₂
sq₁₃ : G.PullbackObjObj f₁ f₃
α : Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃
l : Arrow.LiftStruct α
⊢ (Arrow.mk sq₁₂.ι).hom ≫ l.l = Arrow.Hom.left α

Tactic:
have := l.fac_left