awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.ParametrizedAdjunction (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
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 α
⊢ 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₃)
have 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₃)
Tactic: dsimp at this ⊢
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.ParametrizedAdjunction (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
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 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 α
have 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 α
Tactic: apply sq₁₂.isPushout.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.ParametrizedAdjunction (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
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 α
⊢ (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 α
have 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 α
Tactic: apply sq₁₂.isPushout.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.ParametrizedAdjunction (hypothesis)
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₁₃.π) α)
⊢ 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 α
have 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₁₃.π) α)
Tactic: have := l.fac_left
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.ParametrizedAdjunction (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
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₁₃.π) α)
⊢ 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 α
have 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 α
Tactic: dsimp at this ⊢
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.ParametrizedAdjunction (hypothesis)
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₁₃.π) α)
⊢ 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 α
have 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
Tactic: have := l.fac_right =≫ sq₁₃.fst
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.ParametrizedAdjunction (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
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
⊢ 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 α
have 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 α
Tactic: dsimp at this ⊢
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.ParametrizedAdjunction (hypothesis)
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
⊢ 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 α
have 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
Tactic: simp only [Category.assoc, sq₁₃.π_fst] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.ParametrizedAdjunction (hypothesis)
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₁₃.π) α)
⊢ ((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.mk f₃).hom =
    Arrow.Hom.right α
have this : (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
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.ParametrizedAdjunction (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
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₁₃.snd =
    Arrow.Hom.right
        ((adj₂.arrowHomEquiv sq₁₂ sq₁₃ : (a : Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃) → Arrow.mk f₂ ⟶ Arrow.mk sq₁₃.π) α) ≫
      sq₁₃.snd
⊢ ((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.mk f₃).hom =
    Arrow.Hom.right α
have dsimp : ((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 ≫
    f₃ =
  Arrow.Hom.right α
Tactic: dsimp at this ⊢
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.ParametrizedAdjunction (hypothesis)
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₁₃.snd =
    Arrow.Hom.right
        ((adj₂.arrowHomEquiv sq₁₂ sq₁₃ : (a : Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃) → Arrow.mk f₂ ⟶ Arrow.mk sq₁₃.π) α) ≫
      sq₁₃.snd
⊢ ((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 ≫
      f₃ =
    Arrow.Hom.right α
have this₁ : l.l ≫ (G.obj (op Y₁)).map f₃ =
  ((adj₂.homEquiv : Equiv.{v₃ + 1, v₂ + 1} ((F.obj Y₁).obj Y₂ ⟶ Y₃) (Y₂ ⟶ (G.obj (op Y₁)).obj Y₃)) :
      (a : (F.obj Y₁).obj Y₂ ⟶ Y₃) → Y₂ ⟶ (G.obj (op Y₁)).obj Y₃)
    (Arrow.Hom.right α)
Tactic: simp only [Category.assoc, sq₁₃.π_snd, arrowHomEquiv_apply_right_snd,
          Arrow.mk_right] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.ParametrizedAdjunction (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
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.obj (op Y₁)).map f₃ =
    ((adj₂.homEquiv : Equiv.{v₃ + 1, v₂ + 1} ((F.obj Y₁).obj Y₂ ⟶ Y₃) (Y₂ ⟶ (G.obj (op Y₁)).obj Y₃)) :
        (a : (F.obj Y₁).obj Y₂ ⟶ Y₃) → Y₂ ⟶ (G.obj (op Y₁)).obj Y₃)
      (Arrow.Hom.right α)
⊢ ((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 ≫
      f₃ =
    Arrow.Hom.right α
have rw : ((Equiv.symm adj₂.homEquiv : Equiv.{v₂ + 1, v₃ + 1} (Y₂ ⟶ (G.obj (op Y₁)).obj Y₃) ((F.obj Y₁).obj Y₂ ⟶ Y₃)) :
      (a : Y₂ ⟶ (G.obj (op Y₁)).obj Y₃) → (F.obj Y₁).obj Y₂ ⟶ Y₃)
    (l.l ≫ (G.obj (op Y₁)).map f₃) =
  Arrow.Hom.right α
Tactic: rw [← adj₂.homEquiv_symm_naturality_three, this,
          Equiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.ParametrizedAdjunction (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
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.obj (op Y₁)).map f₃ =
    ((adj₂.homEquiv : Equiv.{v₃ + 1, v₂ + 1} ((F.obj Y₁).obj Y₂ ⟶ Y₃) (Y₂ ⟶ (G.obj (op Y₁)).obj Y₃)) :
        (a : (F.obj Y₁).obj Y₂ ⟶ Y₃) → Y₂ ⟶ (G.obj (op Y₁)).obj Y₃)
      (Arrow.Hom.right α)
rw :
  ((Equiv.symm adj₂.homEquiv : Equiv.{v₂ + 1, v₃ + 1} (Y₂ ⟶ (G.obj (op Y₁)).obj Y₃) ((F.obj Y₁).obj Y₂ ⟶ Y₃)) :
        (a : Y₂ ⟶ (G.obj (op Y₁)).obj Y₃) → (F.obj Y₁).obj Y₂ ⟶ Y₃)
      (l.l ≫ (G.obj (op Y₁)).map f₃) =
    Arrow.Hom.right α
⊢ ((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 ≫
      f₃ =
    Arrow.Hom.right α
have rw₁ : ((Equiv.symm adj₂.homEquiv : Equiv.{v₂ + 1, v₃ + 1} (Y₂ ⟶ (G.obj (op Y₁)).obj Y₃) ((F.obj Y₁).obj Y₂ ⟶ Y₃)) :
      (a : Y₂ ⟶ (G.obj (op Y₁)).obj Y₃) → (F.obj Y₁).obj Y₂ ⟶ Y₃)
    (((adj₂.homEquiv : Equiv.{v₃ + 1, v₂ + 1} ((F.obj Y₁).obj Y₂ ⟶ Y₃) (Y₂ ⟶ (G.obj (op Y₁)).obj Y₃)) :
        (a : (F.obj Y₁).obj Y₂ ⟶ Y₃) → Y₂ ⟶ (G.obj (op Y₁)).obj Y₃)
      (Arrow.Hom.right α)) =
  Arrow.Hom.right α
Tactic: rw [← adj₂.homEquiv_symm_naturality_three, this,
          Equiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.ParametrizedAdjunction (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
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.obj (op Y₁)).map f₃ =
    ((adj₂.homEquiv : Equiv.{v₃ + 1, v₂ + 1} ((F.obj Y₁).obj Y₂ ⟶ Y₃) (Y₂ ⟶ (G.obj (op Y₁)).obj Y₃)) :
        (a : (F.obj Y₁).obj Y₂ ⟶ Y₃) → Y₂ ⟶ (G.obj (op Y₁)).obj Y₃)
      (Arrow.Hom.right α)
rw :
  ((Equiv.symm adj₂.homEquiv : Equiv.{v₂ + 1, v₃ + 1} (Y₂ ⟶ (G.obj (op Y₁)).obj Y₃) ((F.obj Y₁).obj Y₂ ⟶ Y₃)) :
        (a : Y₂ ⟶ (G.obj (op Y₁)).obj Y₃) → (F.obj Y₁).obj Y₂ ⟶ Y₃)
      (l.l ≫ (G.obj (op Y₁)).map f₃) =
    Arrow.Hom.right α
rw₁ :
  ((Equiv.symm adj₂.homEquiv : Equiv.{v₂ + 1, v₃ + 1} (Y₂ ⟶ (G.obj (op Y₁)).obj Y₃) ((F.obj Y₁).obj Y₂ ⟶ Y₃)) :
        (a : Y₂ ⟶ (G.obj (op Y₁)).obj Y₃) → (F.obj Y₁).obj Y₂ ⟶ Y₃)
      (((adj₂.homEquiv : Equiv.{v₃ + 1, v₂ + 1} ((F.obj Y₁).obj Y₂ ⟶ Y₃) (Y₂ ⟶ (G.obj (op Y₁)).obj Y₃)) :
          (a : (F.obj Y₁).obj Y₂ ⟶ Y₃) → Y₂ ⟶ (G.obj (op Y₁)).obj Y₃)
        (Arrow.Hom.right α)) =
    Arrow.Hom.right α
⊢ ((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 ≫
      f₃ =
    Arrow.Hom.right α
have rw₂ : Arrow.Hom.right α = Arrow.Hom.right α
Tactic: rw [← adj₂.homEquiv_symm_naturality_three, this,
          Equiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.ParametrizedAdjunction (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
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₃
⊢ HasLiftingProperty sq₁₂.ι f₃ ↔ HasLiftingProperty f₂ sq₁₃.π
have simp : (∀ (φ : Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃), Nonempty.{v₃ + 1} (Arrow.LiftStruct φ)) ↔
  ∀ (φ : Arrow.mk f₂ ⟶ Arrow.mk sq₁₃.π), Nonempty.{v₂ + 1} (Arrow.LiftStruct φ)
Tactic: simp only [Arrow.hasLiftingProperty_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.ParametrizedAdjunction (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
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₃), Nonempty.{v₃ + 1} (Arrow.LiftStruct φ)) ↔
    ∀ (φ : Arrow.mk f₂ ⟶ Arrow.mk sq₁₃.π), Nonempty.{v₂ + 1} (Arrow.LiftStruct φ)
have mp : (∀ (φ : Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃), Nonempty.{v₃ + 1} (Arrow.LiftStruct φ)) →
  ∀ (φ : Arrow.mk f₂ ⟶ Arrow.mk sq₁₃.π), Nonempty.{v₂ + 1} (Arrow.LiftStruct φ)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.ParametrizedAdjunction (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
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₃
mp :
  (∀ (φ : Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃), Nonempty.{v₃ + 1} (Arrow.LiftStruct φ)) →
    ∀ (φ : Arrow.mk f₂ ⟶ Arrow.mk sq₁₃.π), Nonempty.{v₂ + 1} (Arrow.LiftStruct φ)
⊢ (∀ (φ : Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃), Nonempty.{v₃ + 1} (Arrow.LiftStruct φ)) ↔
    ∀ (φ : Arrow.mk f₂ ⟶ Arrow.mk sq₁₃.π), Nonempty.{v₂ + 1} (Arrow.LiftStruct φ)
have mpr : (∀ (φ : Arrow.mk f₂ ⟶ Arrow.mk sq₁₃.π), Nonempty.{v₂ + 1} (Arrow.LiftStruct φ)) →
  ∀ (φ : Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃), Nonempty.{v₃ + 1} (Arrow.LiftStruct φ)
Tactic: constructor