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₃
l : Arrow.LiftStruct α
this : (Arrow.mk sq₁₂.ι).hom ≫ l.l = Arrow.Hom.left α
dsimp :
  Eq (α := X₂ ⟶ (G.obj (op Y₁)).obj X₃)
    (f₂ ≫
      ((adj₂.homEquiv : Equiv.{v₃ + 1, v₂ + 1} ((F.obj Y₁).obj Y₂ ⟶ X₃) (Y₂ ⟶ (G.obj (op Y₁)).obj X₃)) :
          (a : (F.obj Y₁).obj Y₂ ⟶ X₃) → Y₂ ⟶ (G.obj (op Y₁)).obj X₃)
        l.l)
    (((adj₂.homEquiv : Equiv.{v₃ + 1, v₂ + 1} ((F.obj Y₁).obj X₂ ⟶ X₃) (X₂ ⟶ (G.obj (op Y₁)).obj X₃)) :
        (a : (F.obj Y₁).obj X₂ ⟶ X₃) → X₂ ⟶ (G.obj (op Y₁)).obj X₃)
      (sq₁₂.inl ≫ Arrow.Hom.left α))
⊢ Eq (α := (Arrow.mk f₂).left ⟶ (Arrow.mk sq₁₃.π).left)
    ((Arrow.mk f₂).hom ≫
      ((adj₂.homEquiv :
            Equiv.{v₃ + 1, v₂ + 1} ((F.obj Y₁).obj (Arrow.mk f₂).right ⟶ X₃)
              ((Arrow.mk f₂).right ⟶ (G.obj (op Y₁)).obj X₃)) :
          (a : (F.obj Y₁).obj (Arrow.mk f₂).right ⟶ X₃) → (Arrow.mk f₂).right ⟶ (G.obj (op Y₁)).obj X₃)
        l.l)
    (Arrow.Hom.left
      ((adj₂.arrowHomEquiv sq₁₂ sq₁₃ : (a : Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃) → Arrow.mk f₂ ⟶ Arrow.mk sq₁₃.π) α))

Tactic:
dsimp at this ⊢
-- 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 α
this : sq₁₂.ι ≫ l.l = Arrow.Hom.left α
⊢ Eq (α := X₂ ⟶ (G.obj (op Y₁)).obj X₃)
    (f₂ ≫
      ((adj₂.homEquiv : Equiv.{v₃ + 1, v₂ + 1} ((F.obj Y₁).obj Y₂ ⟶ X₃) (Y₂ ⟶ (G.obj (op Y₁)).obj X₃)) :
          (a : (F.obj Y₁).obj Y₂ ⟶ X₃) → Y₂ ⟶ (G.obj (op Y₁)).obj X₃)
        l.l)
    (((adj₂.homEquiv : Equiv.{v₃ + 1, v₂ + 1} ((F.obj Y₁).obj X₂ ⟶ X₃) (X₂ ⟶ (G.obj (op Y₁)).obj X₃)) :
        (a : (F.obj Y₁).obj X₂ ⟶ X₃) → X₂ ⟶ (G.obj (op Y₁)).obj X₃)
      (sq₁₂.inl ≫ Arrow.Hom.left α))

Tactic:
simp only [← adj₂.homEquiv_naturality_two, ← this,
          sq₁₂.inl_ι_assoc]

Premises used: CategoryTheory.ParametrizedAdjunction.homEquiv_naturality_two, CategoryTheory.Functor.PushoutObjObj.inl_ι_assoc
-- 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 α
h₀ :
  Eq.{v₂ + 1} (α := (Arrow.mk f₂).right ⟶ (G.obj (op X₁)).obj X₃)
    ((((adj₂.homEquiv :
                Equiv.{v₃ + 1, v₂ + 1} ((F.obj Y₁).obj (Arrow.mk f₂).right ⟶ X₃)
                  ((Arrow.mk f₂).right ⟶ (G.obj (op Y₁)).obj X₃)) :
              (a : (F.obj Y₁).obj (Arrow.mk f₂).right ⟶ X₃) → (Arrow.mk f₂).right ⟶ (G.obj (op Y₁)).obj X₃)
            l.l ≫
          (Arrow.mk sq₁₃.π).hom) ≫
        sq₁₃.fst :
      (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₃)
h₁ :
  Eq.{v₂ + 1} (α := (Arrow.mk f₂).right ⟶ (G.obj (op Y₁)).obj Y₃)
    ((((adj₂.homEquiv :
                Equiv.{v₃ + 1, v₂ + 1} ((F.obj Y₁).obj (Arrow.mk f₂).right ⟶ X₃)
                  ((Arrow.mk f₂).right ⟶ (G.obj (op Y₁)).obj X₃)) :
              (a : (F.obj Y₁).obj (Arrow.mk f₂).right ⟶ X₃) → (Arrow.mk f₂).right ⟶ (G.obj (op Y₁)).obj X₃)
            l.l ≫
          (Arrow.mk sq₁₃.π).hom) ≫
        sq₁₃.snd :
      (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₃)
⊢ Eq.{v₂ + 1} (α := (Arrow.mk f₂).right ⟶ (Arrow.mk sq₁₃.π).right)
    (((adj₂.homEquiv :
              Equiv.{v₃ + 1, v₂ + 1} ((F.obj Y₁).obj (Arrow.mk f₂).right ⟶ X₃)
                ((Arrow.mk f₂).right ⟶ (G.obj (op Y₁)).obj X₃)) :
            (a : (F.obj Y₁).obj (Arrow.mk f₂).right ⟶ X₃) → (Arrow.mk f₂).right ⟶ (G.obj (op Y₁)).obj X₃)
          l.l ≫
        (Arrow.mk sq₁₃.π).hom :
      (Arrow.mk f₂).right ⟶ (Arrow.mk sq₁₃.π).right)
    (Arrow.Hom.right
        ((adj₂.arrowHomEquiv sq₁₂ sq₁₃ : (a : Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃) → Arrow.mk f₂ ⟶ Arrow.mk sq₁₃.π) α) :
      (Arrow.mk f₂).right ⟶ (Arrow.mk sq₁₃.π).right)

Tactic:
apply sq₁₃.isPullback.hom_ext

Premises used: CategoryTheory.IsPullback.hom_ext, CategoryTheory.Functor.PullbackObjObj.isPullback
-- 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 α
this : (Arrow.mk sq₁₂.ι).hom ≫ l.l = Arrow.Hom.left α
h₀ :
  Eq.{v₂ + 1} (α := Y₂ ⟶ (G.obj (op X₁)).obj X₃)
    ((((adj₂.homEquiv : Equiv.{v₃ + 1, v₂ + 1} ((F.obj Y₁).obj Y₂ ⟶ X₃) (Y₂ ⟶ (G.obj (op Y₁)).obj X₃)) :
              (a : (F.obj Y₁).obj Y₂ ⟶ X₃) → Y₂ ⟶ (G.obj (op Y₁)).obj X₃)
            l.l ≫
          sq₁₃.π) ≫
        sq₁₃.fst :
      Y₂ ⟶ (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 :
      Y₂ ⟶ (G.obj (op X₁)).obj X₃)
⊢ Eq.{v₂ + 1} (α := (Arrow.mk f₂).right ⟶ (G.obj (op X₁)).obj X₃)
    ((((adj₂.homEquiv :
                Equiv.{v₃ + 1, v₂ + 1} ((F.obj Y₁).obj (Arrow.mk f₂).right ⟶ X₃)
                  ((Arrow.mk f₂).right ⟶ (G.obj (op Y₁)).obj X₃)) :
              (a : (F.obj Y₁).obj (Arrow.mk f₂).right ⟶ X₃) → (Arrow.mk f₂).right ⟶ (G.obj (op Y₁)).obj X₃)
            l.l ≫
          (Arrow.mk sq₁₃.π).hom) ≫
        sq₁₃.fst :
      (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₃)

Tactic:
dsimp at this ⊢
-- 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 α
this : sq₁₂.ι ≫ l.l = Arrow.Hom.left α
⊢ Eq.{v₂ + 1} (α := Y₂ ⟶ (G.obj (op X₁)).obj X₃)
    ((((adj₂.homEquiv : Equiv.{v₃ + 1, v₂ + 1} ((F.obj Y₁).obj Y₂ ⟶ X₃) (Y₂ ⟶ (G.obj (op Y₁)).obj X₃)) :
              (a : (F.obj Y₁).obj Y₂ ⟶ X₃) → Y₂ ⟶ (G.obj (op Y₁)).obj X₃)
            l.l ≫
          sq₁₃.π) ≫
        sq₁₃.fst :
      Y₂ ⟶ (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 :
      Y₂ ⟶ (G.obj (op X₁)).obj X₃)

Tactic:
simp only [Category.assoc, sq₁₃.π_fst, ← adj₂.homEquiv_naturality_one,
            arrowHomEquiv_apply_right_fst, Arrow.mk_left, ← this, sq₁₂.inr_ι_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.PullbackObjObj.π_fst, CategoryTheory.ParametrizedAdjunction.arrowHomEquiv_apply_right_fst, CategoryTheory.Arrow.mk_left, CategoryTheory.Functor.PushoutObjObj.inr_ι_assoc, CategoryTheory.ParametrizedAdjunction.homEquiv_naturality_one
-- 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 α
⊢ l.l ≫ (Arrow.mk f₃).hom = Arrow.Hom.right α

Tactic:
have := l.fac_right
-- 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 α
this : l.l ≫ (Arrow.mk f₃).hom = Arrow.Hom.right α
h₁ :
  Eq.{v₂ + 1} (α := Y₂ ⟶ (G.obj (op Y₁)).obj Y₃)
    ((((adj₂.homEquiv : Equiv.{v₃ + 1, v₂ + 1} ((F.obj Y₁).obj Y₂ ⟶ X₃) (Y₂ ⟶ (G.obj (op Y₁)).obj X₃)) :
              (a : (F.obj Y₁).obj Y₂ ⟶ X₃) → Y₂ ⟶ (G.obj (op Y₁)).obj X₃)
            l.l ≫
          sq₁₃.π) ≫
        sq₁₃.snd :
      Y₂ ⟶ (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 :
      Y₂ ⟶ (G.obj (op Y₁)).obj Y₃)
⊢ Eq.{v₂ + 1} (α := (Arrow.mk f₂).right ⟶ (G.obj (op Y₁)).obj Y₃)
    ((((adj₂.homEquiv :
                Equiv.{v₃ + 1, v₂ + 1} ((F.obj Y₁).obj (Arrow.mk f₂).right ⟶ X₃)
                  ((Arrow.mk f₂).right ⟶ (G.obj (op Y₁)).obj X₃)) :
              (a : (F.obj Y₁).obj (Arrow.mk f₂).right ⟶ X₃) → (Arrow.mk f₂).right ⟶ (G.obj (op Y₁)).obj X₃)
            l.l ≫
          (Arrow.mk sq₁₃.π).hom) ≫
        sq₁₃.snd :
      (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₃)

Tactic:
dsimp at this ⊢
-- 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 α
this : l.l ≫ f₃ = Arrow.Hom.right α
⊢ Eq.{v₂ + 1} (α := Y₂ ⟶ (G.obj (op Y₁)).obj Y₃)
    ((((adj₂.homEquiv : Equiv.{v₃ + 1, v₂ + 1} ((F.obj Y₁).obj Y₂ ⟶ X₃) (Y₂ ⟶ (G.obj (op Y₁)).obj X₃)) :
              (a : (F.obj Y₁).obj Y₂ ⟶ X₃) → Y₂ ⟶ (G.obj (op Y₁)).obj X₃)
            l.l ≫
          sq₁₃.π) ≫
        sq₁₃.snd :
      Y₂ ⟶ (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 :
      Y₂ ⟶ (G.obj (op Y₁)).obj Y₃)

Tactic:
simp only [Category.assoc, sq₁₃.π_snd, ← this, adj₂.homEquiv_naturality_three,
            arrowHomEquiv_apply_right_snd, Arrow.mk_right]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.ParametrizedAdjunction.arrowHomEquiv_apply_right_snd, CategoryTheory.Arrow.mk_right, CategoryTheory.ParametrizedAdjunction.homEquiv_naturality_three, CategoryTheory.Functor.PullbackObjObj.π_snd
-- 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.{v₂, u₂} (C := C₂) (f := Arrow.mk f₂) (g := Arrow.mk sq₁₃.π)
    ((adj₂.arrowHomEquiv sq₁₂ sq₁₃ : (a : Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃) → Arrow.mk f₂ ⟶ Arrow.mk sq₁₃.π) α)
h₀ :
  sq₁₂.inl ≫
      (Arrow.mk sq₁₂.ι).hom ≫
        ((Equiv.symm adj₂.homEquiv :
              Equiv.{v₂ + 1, v₃ + 1} (Y₂ ⟶ (G.obj (op Y₁)).obj (Arrow.mk f₃).left)
                ((F.obj Y₁).obj Y₂ ⟶ (Arrow.mk f₃).left)) :
            (a : Y₂ ⟶ (G.obj (op Y₁)).obj (Arrow.mk f₃).left) → (F.obj Y₁).obj Y₂ ⟶ (Arrow.mk f₃).left)
          l.l =
    sq₁₂.inl ≫ Arrow.Hom.left α
h₁ :
  sq₁₂.inr ≫
      (Arrow.mk sq₁₂.ι).hom ≫
        ((Equiv.symm adj₂.homEquiv :
              Equiv.{v₂ + 1, v₃ + 1} (Y₂ ⟶ (G.obj (op Y₁)).obj (Arrow.mk f₃).left)
                ((F.obj Y₁).obj Y₂ ⟶ (Arrow.mk f₃).left)) :
            (a : Y₂ ⟶ (G.obj (op Y₁)).obj (Arrow.mk f₃).left) → (F.obj Y₁).obj Y₂ ⟶ (Arrow.mk f₃).left)
          l.l =
    sq₁₂.inr ≫ Arrow.Hom.left α
⊢ (Arrow.mk sq₁₂.ι).hom ≫
      ((Equiv.symm adj₂.homEquiv :
            Equiv.{v₂ + 1, v₃ + 1} (Y₂ ⟶ (G.obj (op Y₁)).obj (Arrow.mk f₃).left)
              ((F.obj Y₁).obj Y₂ ⟶ (Arrow.mk f₃).left)) :
          (a : Y₂ ⟶ (G.obj (op Y₁)).obj (Arrow.mk f₃).left) → (F.obj Y₁).obj Y₂ ⟶ (Arrow.mk f₃).left)
        l.l =
    Arrow.Hom.left α

Tactic:
apply sq₁₂.isPushout.hom_ext

Premises used: CategoryTheory.Functor.PushoutObjObj.isPushout, CategoryTheory.IsPushout.hom_ext
-- 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.{v₂, u₂} (C := C₂) (f := Arrow.mk f₂) (g := Arrow.mk sq₁₃.π)
    ((adj₂.arrowHomEquiv sq₁₂ sq₁₃ : (a : Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃) → Arrow.mk f₂ ⟶ Arrow.mk sq₁₃.π) α)
⊢ (Arrow.mk f₂).hom ≫ l.l =
    Arrow.Hom.left
      ((adj₂.arrowHomEquiv sq₁₂ sq₁₃ : (a : Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃) → Arrow.mk f₂ ⟶ Arrow.mk sq₁₃.π) α)

Tactic:
have := l.fac_left
-- 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.{v₂, u₂} (C := C₂) (f := Arrow.mk f₂) (g := Arrow.mk sq₁₃.π)
    ((adj₂.arrowHomEquiv sq₁₂ sq₁₃ : (a : Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃) → Arrow.mk f₂ ⟶ Arrow.mk sq₁₃.π) α)
this :
  (Arrow.mk f₂).hom ≫ l.l =
    Arrow.Hom.left
      ((adj₂.arrowHomEquiv sq₁₂ sq₁₃ : (a : Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃) → Arrow.mk f₂ ⟶ Arrow.mk sq₁₃.π) α)
h₀ :
  sq₁₂.inl ≫
      sq₁₂.ι ≫
        ((Equiv.symm adj₂.homEquiv : Equiv.{v₂ + 1, v₃ + 1} (Y₂ ⟶ (G.obj (op Y₁)).obj X₃) ((F.obj Y₁).obj Y₂ ⟶ X₃)) :
            (a : Y₂ ⟶ (G.obj (op Y₁)).obj X₃) → (F.obj Y₁).obj Y₂ ⟶ X₃)
          l.l =
    sq₁₂.inl ≫ Arrow.Hom.left α
⊢ sq₁₂.inl ≫
      (Arrow.mk sq₁₂.ι).hom ≫
        ((Equiv.symm adj₂.homEquiv :
              Equiv.{v₂ + 1, v₃ + 1} (Y₂ ⟶ (G.obj (op Y₁)).obj (Arrow.mk f₃).left)
                ((F.obj Y₁).obj Y₂ ⟶ (Arrow.mk f₃).left)) :
            (a : Y₂ ⟶ (G.obj (op Y₁)).obj (Arrow.mk f₃).left) → (F.obj Y₁).obj Y₂ ⟶ (Arrow.mk f₃).left)
          l.l =
    sq₁₂.inl ≫ Arrow.Hom.left α

Tactic:
dsimp at this ⊢
-- 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.{v₂, u₂} (C := C₂) (f := Arrow.mk f₂) (g := Arrow.mk sq₁₃.π)
    ((adj₂.arrowHomEquiv sq₁₂ sq₁₃ : (a : Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃) → Arrow.mk f₂ ⟶ Arrow.mk sq₁₃.π) α)
this :
  f₂ ≫ l.l =
    ((adj₂.homEquiv : Equiv.{v₃ + 1, v₂ + 1} ((F.obj Y₁).obj X₂ ⟶ X₃) (X₂ ⟶ (G.obj (op Y₁)).obj X₃)) :
        (a : (F.obj Y₁).obj X₂ ⟶ X₃) → X₂ ⟶ (G.obj (op Y₁)).obj X₃)
      (sq₁₂.inl ≫ Arrow.Hom.left α)
⊢ sq₁₂.inl ≫
      sq₁₂.ι ≫
        ((Equiv.symm adj₂.homEquiv : Equiv.{v₂ + 1, v₃ + 1} (Y₂ ⟶ (G.obj (op Y₁)).obj X₃) ((F.obj Y₁).obj Y₂ ⟶ X₃)) :
            (a : Y₂ ⟶ (G.obj (op Y₁)).obj X₃) → (F.obj Y₁).obj Y₂ ⟶ X₃)
          l.l =
    sq₁₂.inl ≫ Arrow.Hom.left α

Tactic:
simp only [sq₁₂.inl_ι_assoc, ← adj₂.homEquiv_symm_naturality_two,
            this, Equiv.symm_apply_apply]

Premises used: Equiv.symm_apply_apply, CategoryTheory.ParametrizedAdjunction.homEquiv_symm_naturality_two, CategoryTheory.Functor.PushoutObjObj.inl_ι_assoc
-- 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.{v₂, u₂} (C := C₂) (f := Arrow.mk f₂) (g := Arrow.mk sq₁₃.π)
    ((adj₂.arrowHomEquiv sq₁₂ sq₁₃ : (a : Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃) → Arrow.mk f₂ ⟶ Arrow.mk sq₁₃.π) α)
⊢ (l.l ≫ (Arrow.mk sq₁₃.π).hom) ≫ sq₁₃.fst =
    Arrow.Hom.right
        ((adj₂.arrowHomEquiv sq₁₂ sq₁₃ : (a : Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃) → Arrow.mk f₂ ⟶ Arrow.mk sq₁₃.π) α) ≫
      sq₁₃.fst

Tactic:
have := l.fac_right =≫ sq₁₃.fst
-- 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.{v₂, u₂} (C := C₂) (f := Arrow.mk f₂) (g := Arrow.mk sq₁₃.π)
    ((adj₂.arrowHomEquiv sq₁₂ sq₁₃ : (a : Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃) → Arrow.mk f₂ ⟶ Arrow.mk sq₁₃.π) α)
this :
  (l.l ≫ (Arrow.mk sq₁₃.π).hom) ≫ sq₁₃.fst =
    Arrow.Hom.right
        ((adj₂.arrowHomEquiv sq₁₂ sq₁₃ : (a : Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃) → Arrow.mk f₂ ⟶ Arrow.mk sq₁₃.π) α) ≫
      sq₁₃.fst
h₁ :
  sq₁₂.inr ≫
      sq₁₂.ι ≫
        ((Equiv.symm adj₂.homEquiv : Equiv.{v₂ + 1, v₃ + 1} (Y₂ ⟶ (G.obj (op Y₁)).obj X₃) ((F.obj Y₁).obj Y₂ ⟶ X₃)) :
            (a : Y₂ ⟶ (G.obj (op Y₁)).obj X₃) → (F.obj Y₁).obj Y₂ ⟶ X₃)
          l.l =
    sq₁₂.inr ≫ Arrow.Hom.left α
⊢ sq₁₂.inr ≫
      (Arrow.mk sq₁₂.ι).hom ≫
        ((Equiv.symm adj₂.homEquiv :
              Equiv.{v₂ + 1, v₃ + 1} (Y₂ ⟶ (G.obj (op Y₁)).obj (Arrow.mk f₃).left)
                ((F.obj Y₁).obj Y₂ ⟶ (Arrow.mk f₃).left)) :
            (a : Y₂ ⟶ (G.obj (op Y₁)).obj (Arrow.mk f₃).left) → (F.obj Y₁).obj Y₂ ⟶ (Arrow.mk f₃).left)
          l.l =
    sq₁₂.inr ≫ Arrow.Hom.left α

Tactic:
dsimp at this ⊢
-- 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.{v₂, u₂} (C := C₂) (f := Arrow.mk f₂) (g := Arrow.mk sq₁₃.π)
    ((adj₂.arrowHomEquiv sq₁₂ sq₁₃ : (a : Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃) → Arrow.mk f₂ ⟶ Arrow.mk sq₁₃.π) α)
this :
  (l.l ≫ sq₁₃.π) ≫ sq₁₃.fst =
    Arrow.Hom.right
        ((adj₂.arrowHomEquiv sq₁₂ sq₁₃ : (a : Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃) → Arrow.mk f₂ ⟶ Arrow.mk sq₁₃.π) α) ≫
      sq₁₃.fst
⊢ l.l ≫ (G.map f₁.op).app X₃ =
    Arrow.Hom.right
        ((adj₂.arrowHomEquiv sq₁₂ sq₁₃ : (a : Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃) → Arrow.mk f₂ ⟶ Arrow.mk sq₁₃.π) α) ≫
      sq₁₃.fst

Tactic:
simp only [Category.assoc, sq₁₃.π_fst] at this

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.PullbackObjObj.π_fst
-- 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.{v₂, u₂} (C := C₂) (f := Arrow.mk f₂) (g := Arrow.mk sq₁₃.π)
    ((adj₂.arrowHomEquiv sq₁₂ sq₁₃ : (a : Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃) → Arrow.mk f₂ ⟶ Arrow.mk sq₁₃.π) α)
this :
  l.l ≫ (G.map f₁.op).app X₃ =
    Arrow.Hom.right
        ((adj₂.arrowHomEquiv sq₁₂ sq₁₃ : (a : Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃) → Arrow.mk f₂ ⟶ Arrow.mk sq₁₃.π) α) ≫
      sq₁₃.fst
⊢ sq₁₂.inr ≫
      sq₁₂.ι ≫
        ((Equiv.symm adj₂.homEquiv : Equiv.{v₂ + 1, v₃ + 1} (Y₂ ⟶ (G.obj (op Y₁)).obj X₃) ((F.obj Y₁).obj Y₂ ⟶ X₃)) :
            (a : Y₂ ⟶ (G.obj (op Y₁)).obj X₃) → (F.obj Y₁).obj Y₂ ⟶ X₃)
          l.l =
    sq₁₂.inr ≫ Arrow.Hom.left α

Tactic:
simp only [sq₁₂.inr_ι_assoc, ← adj₂.homEquiv_symm_naturality_one,
            this, Equiv.symm_apply_apply, arrowHomEquiv_apply_right_fst, Arrow.mk_left]

Premises used: CategoryTheory.ParametrizedAdjunction.homEquiv_symm_naturality_one, Equiv.symm_apply_apply, CategoryTheory.ParametrizedAdjunction.arrowHomEquiv_apply_right_fst, CategoryTheory.Arrow.mk_left, CategoryTheory.Functor.PushoutObjObj.inr_ι_assoc
-- 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.{v₂, u₂} (C := C₂) (f := Arrow.mk f₂) (g := Arrow.mk sq₁₃.π)
    ((adj₂.arrowHomEquiv sq₁₂ sq₁₃ : (a : Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃) → Arrow.mk f₂ ⟶ Arrow.mk sq₁₃.π) α)
⊢ (l.l ≫ (Arrow.mk sq₁₃.π).hom) ≫ sq₁₃.snd =
    Arrow.Hom.right
        ((adj₂.arrowHomEquiv sq₁₂ sq₁₃ : (a : Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃) → Arrow.mk f₂ ⟶ Arrow.mk sq₁₃.π) α) ≫
      sq₁₃.snd

Tactic:
have := l.fac_right =≫ sq₁₃.snd