awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.Over (goal)
Goal:
C : Type u
inst : Category.{v, u} C
S : C
X₁ X₂ X₃ X₄ : Over.{v, u} S
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
sq : CommSq t l r b
inst_1 :
  HasLift (A := X₁.left) (B := X₃.left) (X := X₂.left) (Y := X₄.left) (f := Over.Hom.left t) (i := Over.Hom.left l)
    (p := Over.Hom.left r) (g := Over.Hom.left b) ⋯
sq' : CommSq (Over.Hom.left t) (Over.Hom.left l) (Over.Hom.left r) (Over.Hom.left b) := ⋯
rw : sq'.lift ≫ X₂.hom = Over.Hom.left b ≫ X₄.hom
rw₁ : sq'.lift ≫ X₂.hom = sq'.lift ≫ Over.Hom.left r ≫ X₄.hom
⊢ sq'.lift ≫ X₂.hom = X₃.hom
have rw₂ : sq'.lift ≫ X₂.hom = sq'.lift ≫ X₂.hom
Tactic: rw [← Over.w b, ← sq'.fac_right_assoc, Over.w r]
-- 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₃
⊢ ((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 α) ≫
      (Arrow.mk sq₁₃.π).hom =
    (Arrow.mk f₂).hom ≫
      ⋯.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 α))
        ⋯
have h₀ : (((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 α) ≫
      (Arrow.mk sq₁₃.π).hom) ≫
    sq₁₃.fst =
  ((Arrow.mk f₂).hom ≫
      sorry.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 α))
        sorry) ≫
    sq₁₃.fst
Tactic: apply sq₁₃.isPullback.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 f₂ ⟶ Arrow.mk sq₁₃.π
⊢ Eq (α := (F.obj X₁).obj X₂ ⟶ (Arrow.mk f₃).left)
    ((F.map f₁).app X₂ ≫
      ((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 β))
    ((F.obj X₁).map f₂ ≫
      ((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))
have this : (Arrow.Hom.left β ≫ (Arrow.mk sq₁₃.π).hom) ≫ sq₁₃.fst = ((Arrow.mk f₂).hom ≫ Arrow.Hom.right β) ≫ sq₁₃.fst
Tactic: have := Arrow.w β =≫ sq₁₃.fst
-- 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 f₂ ⟶ Arrow.mk sq₁₃.π
this : (Arrow.Hom.left β ≫ sq₁₃.π) ≫ sq₁₃.fst = (f₂ ≫ Arrow.Hom.right β) ≫ sq₁₃.fst
⊢ Eq (α := (F.obj X₁).obj X₂ ⟶ (Arrow.mk f₃).left)
    ((F.map f₁).app X₂ ≫
      ((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 β))
    ((F.obj X₁).map f₂ ≫
      ((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))
have this₁ : Arrow.Hom.left β ≫ (G.map f₁.op).app X₃ = f₂ ≫ Arrow.Hom.right β ≫ sq₁₃.fst
Tactic: simp only [Category.assoc, sq₁₃.π_fst] 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 f₂ ⟶ Arrow.mk sq₁₃.π
⊢ ⋯.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))
        ⋯ ≫
      (Arrow.mk f₃).hom =
    (Arrow.mk sq₁₂.ι).hom ≫
      ((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)
have h₀ : sq₁₂.inl ≫
    sorry.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))
        sorry ≫
      (Arrow.mk f₃).hom =
  sq₁₂.inl ≫
    (Arrow.mk sq₁₂.ι).hom ≫
      ((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)
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 f₂ ⟶ Arrow.mk sq₁₃.π
⊢ sq₁₂.inl ≫
      ⋯.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))
          ⋯ ≫
        (Arrow.mk f₃).hom =
    sq₁₂.inl ≫
      (Arrow.mk sq₁₂.ι).hom ≫
        ((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)
have this : (Arrow.Hom.left β ≫ (Arrow.mk sq₁₃.π).hom) ≫ sq₁₃.snd = ((Arrow.mk f₂).hom ≫ Arrow.Hom.right β) ≫ sq₁₃.snd
Tactic: have := Arrow.w β =≫ sq₁₃.snd
-- 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 f₂ ⟶ Arrow.mk sq₁₃.π
this : (Arrow.Hom.left β ≫ sq₁₃.π) ≫ sq₁₃.snd = (f₂ ≫ Arrow.Hom.right β) ≫ sq₁₃.snd
⊢ sq₁₂.inl ≫
      ⋯.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))
          ⋯ ≫
        (Arrow.mk f₃).hom =
    sq₁₂.inl ≫
      (Arrow.mk sq₁₂.ι).hom ≫
        ((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)
have this₁ : Arrow.Hom.left β ≫ (G.obj (op Y₁)).map f₃ = f₂ ≫ Arrow.Hom.right β ≫ sq₁₃.snd
Tactic: simp only [Category.assoc, sq₁₃.π_snd] 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 α
⊢ 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₁₃.π) α))
have this : (Arrow.mk sq₁₂.ι).hom ≫ l.l = Arrow.Hom.left α
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 α
this : (Arrow.mk sq₁₂.ι).hom ≫ l.l = 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₁₃.π) α))
have 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 α))
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 α
⊢ 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)
have 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₃)
Tactic: apply sq₁₃.isPullback.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 α
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₃)
⊢ 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)
have 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₃)
Tactic: apply sq₁₃.isPullback.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 α
⊢ 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₃)
have this : (Arrow.mk sq₁₂.ι).hom ≫ l.l = Arrow.Hom.left α
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 α
this : (Arrow.mk sq₁₂.ι).hom ≫ l.l = Arrow.Hom.left α
⊢ 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₃)
have 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₃)
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 α
⊢ 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 this : l.l ≫ (Arrow.mk f₃).hom = Arrow.Hom.right α
Tactic: have := l.fac_right