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.{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
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 α
⊢ ((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 α

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₁₃.snd =
    Arrow.Hom.right
        ((adj₂.arrowHomEquiv sq₁₂ sq₁₃ : (a : Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃) → Arrow.mk f₂ ⟶ Arrow.mk sq₁₃.π) α) ≫
      sq₁₃.snd
⊢ 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

Premises used: CategoryTheory.Category.assoc, CategoryTheory.ParametrizedAdjunction.arrowHomEquiv_apply_right_snd, CategoryTheory.Arrow.mk_right, 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₁₃.π) α)
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 α
rw₂ rw₃ : 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 α

Tactic:
rw [← adj₂.homEquiv_symm_naturality_three, this,
          Equiv.symm_apply_apply]

Premises used: Equiv.symm_apply_apply, CategoryTheory.ParametrizedAdjunction.homEquiv_symm_naturality_three
-- 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₃
x : Arrow.LiftStruct α
⊢ (fun
          (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 :=
              ((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,
            fac_left := ⋯, fac_right := ⋯ } :
          ⋯.LiftStruct))
      ((fun (l : Arrow.LiftStruct α) ↦
          ({
              l :=
                ((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,
              fac_left := ⋯, fac_right := ⋯ } :
            CommSq.LiftStruct.{v₂, u₂} (C := C₂) (A := (Arrow.mk f₂).left) (X := (Arrow.mk sq₁₃.π).left) (f :=
              Arrow.Hom.left
                ((adj₂.arrowHomEquiv sq₁₂ sq₁₃ : (a : Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃) → Arrow.mk f₂ ⟶ Arrow.mk sq₁₃.π)
                  α))
              ⋯))
        x) =
    x

Tactic:
aesop
-- 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₃
x :
  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₁₃.π) α)
⊢ (fun (l : Arrow.LiftStruct α) ↦
        ({
            l :=
              ((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,
            fac_left := ⋯, fac_right := ⋯ } :
          CommSq.LiftStruct.{v₂, u₂} (C := C₂) (A := (Arrow.mk f₂).left) (X := (Arrow.mk sq₁₃.π).left) (f :=
            Arrow.Hom.left
              ((adj₂.arrowHomEquiv sq₁₂ sq₁₃ : (a : Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃) → Arrow.mk f₂ ⟶ Arrow.mk sq₁₃.π) α))
            ⋯))
      ((fun
            (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 :=
                ((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,
              fac_left := ⋯, fac_right := ⋯ } :
            ⋯.LiftStruct))
        x) =
    x

Tactic:
aesop
-- 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₃
simp :
  (∀ (φ : Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃), Nonempty.{v₃ + 1} (Arrow.LiftStruct φ)) ↔
    ∀ (φ : Arrow.mk f₂ ⟶ Arrow.mk sq₁₃.π), Nonempty.{v₂ + 1} (Arrow.LiftStruct φ)
⊢ HasLiftingProperty sq₁₂.ι f₃ ↔ HasLiftingProperty f₂ sq₁₃.π

Tactic:
simp only [Arrow.hasLiftingProperty_iff]

Premises used: CategoryTheory.Arrow.hasLiftingProperty_iff
-- 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₃
mp :
  (∀ (φ : Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃), Nonempty.{v₃ + 1} (Arrow.LiftStruct φ)) →
    ∀ (φ : Arrow.mk f₂ ⟶ Arrow.mk sq₁₃.π), Nonempty.{v₂ + 1} (Arrow.LiftStruct φ)
mpr :
  (∀ (φ : Arrow.mk f₂ ⟶ Arrow.mk sq₁₃.π), Nonempty.{v₂ + 1} (Arrow.LiftStruct φ)) →
    ∀ (φ : Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃), 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 φ)

Tactic:
constructor
-- 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₃
h : ∀ (φ : Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃), Nonempty.{v₃ + 1} (Arrow.LiftStruct φ)
β : Arrow.mk f₂ ⟶ Arrow.mk sq₁₃.π
mp :
  ∀ (α : Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃),
    Nonempty.{v₂ + 1}
      (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₁₃.π) α))
⊢ Nonempty.{v₂ + 1} (Arrow.LiftStruct β)

Tactic:
obtain ⟨α, rfl⟩ := (adj₂.arrowHomEquiv sq₁₂ sq₁₃).surjective β

Premises used: CategoryTheory.ParametrizedAdjunction.arrowHomEquiv, Equiv.surjective, rfl
-- 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₃
h : ∀ (φ : Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃), Nonempty.{v₃ + 1} (Arrow.LiftStruct φ)
α : Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃
⊢ Nonempty.{v₂ + 1}
    (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₁₃.π) α))

Tactic:
⟨adj₂.liftStructEquiv sq₁₂ sq₁₃ α (h α).some⟩

Premises used: Nonempty.some, Nonempty.intro, CategoryTheory.ParametrizedAdjunction.liftStructEquiv, DFunLike.coe
-- 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₃
h : ∀ (φ : Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃), Nonempty.{v₃ + 1} (Arrow.LiftStruct φ)
α : Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃
⊢ Nonempty.{v₂ + 1}
    (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₁₃.π) α))

Tactic:
exact ⟨adj₂.liftStructEquiv sq₁₂ sq₁₃ α (h α).some⟩
-- 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₃
h : ∀ (φ : Arrow.mk f₂ ⟶ Arrow.mk sq₁₃.π), Nonempty.{v₂ + 1} (Arrow.LiftStruct φ)
α : Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃
⊢ Nonempty.{v₃ + 1} (Arrow.LiftStruct α)

Tactic:
⟨(adj₂.liftStructEquiv sq₁₂ sq₁₃ α).symm (h _).some⟩

Premises used: Nonempty.some, Nonempty.intro, Equiv.symm, CategoryTheory.ParametrizedAdjunction.liftStructEquiv, DFunLike.coe
-- 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₃
h : ∀ (φ : Arrow.mk f₂ ⟶ Arrow.mk sq₁₃.π), Nonempty.{v₂ + 1} (Arrow.LiftStruct φ)
α : Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃
⊢ Nonempty.{v₃ + 1} (Arrow.LiftStruct α)

Tactic:
exact ⟨(adj₂.liftStructEquiv sq₁₂ sq₁₃ α).symm (h _).some⟩
-- Module: Mathlib.CategoryTheory.LiftingProperties.PushoutProduct
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPushouts.{v, u} C
inst_2 : HasPullbacks.{v, u} C
inst_3 : MonoidalCategory.{v, u} C
inst_4 : MonoidalClosed.{v, u} C
X Y Z : Arrow.{v, u} C
⊢ HasLiftingProperty (X □ Y).hom Z.hom ↔ HasLiftingProperty Y.hom (Opposite.op X ⋔ Z).hom

Tactic:
ParametrizedAdjunction.hasLiftingProperty_iff MonoidalClosed.internalHomAdjunction₂
    (PushoutObjObj.ofHasPushout ..) (PullbackObjObj.ofHasPullback ..)

Premises used: CategoryTheory.Functor.PullbackObjObj.π, CategoryTheory.ParametrizedAdjunction.hasLiftingProperty_iff, CategoryTheory.Functor.PushoutObjObj.ofHasPushout, CategoryTheory.Limits.PushoutCocone.IsColimit.desc, CategoryTheory.Functor.PushoutObjObj.ι, CategoryTheory.Limits.colimit, CategoryTheory.Limits.PullbackCone.IsLimit.lift, CategoryTheory.Limits.limit, CategoryTheory.Functor.PullbackObjObj.ofHasPullback, CategoryTheory.IsPushout.desc, CategoryTheory.IsPullback.lift, CategoryTheory.MonoidalClosed.internalHomAdjunction₂
-- Module: Mathlib.CategoryTheory.LiftingProperties.PushoutProduct
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPushouts.{v, u} C
inst_2 : HasPullbacks.{v, u} C
inst_3 : MonoidalCategory.{v, u} C
inst_4 : MonoidalClosed.{v, u} C
inst_5 : BraidedCategory.{v, u} C
X Y Z : Arrow.{v, u} C
rw : HasLiftingProperty (X □ Y).hom Z.hom ↔ HasLiftingProperty (Y □ X).hom Z.hom
⊢ HasLiftingProperty (X □ Y).hom Z.hom ↔ HasLiftingProperty X.hom (Opposite.op Y ⋔ Z).hom

Tactic:
rw [← hasLiftingProperty_iff]

Premises used: CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.hasLiftingProperty_iff
-- Module: Mathlib.CategoryTheory.LiftingProperties.PushoutProduct
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPushouts.{v, u} C
inst_2 : HasPullbacks.{v, u} C
inst_3 : MonoidalCategory.{v, u} C
inst_4 : MonoidalClosed.{v, u} C
inst_5 : BraidedCategory.{v, u} C
X Y Z : Arrow.{v, u} C
⊢ HasLiftingProperty (X □ Y).hom Z.hom ↔ HasLiftingProperty (Y □ X).hom Z.hom

Tactic:
HasLiftingProperty.iff_of_arrow_iso_left (braiding _ _) _

Premises used: CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.braiding, CategoryTheory.Limits.PushoutCocone.IsColimit.desc, CategoryTheory.Functor.PushoutObjObj.ι, CategoryTheory.Limits.colimit, CategoryTheory.HasLiftingProperty.iff_of_arrow_iso_left, CategoryTheory.IsPushout.desc
-- Module: Mathlib.CategoryTheory.LiftingProperties.PushoutProduct
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPushouts.{v, u} C
inst_2 : HasPullbacks.{v, u} C
inst_3 : MonoidalCategory.{v, u} C
inst_4 : MonoidalClosed.{v, u} C
inst_5 : BraidedCategory.{v, u} C
X Y Z : Arrow.{v, u} C
⊢ HasLiftingProperty (X □ Y).hom Z.hom ↔ HasLiftingProperty (Y □ X).hom Z.hom

Tactic:
exact HasLiftingProperty.iff_of_arrow_iso_left (braiding _ _) _

Premises used: CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.braiding, CategoryTheory.HasLiftingProperty.iff_of_arrow_iso_left
-- Module: Mathlib.CategoryTheory.LiftingProperties.PushoutProduct
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPushouts.{v, u} C
inst_2 : HasPullbacks.{v, u} C
inst_3 : MonoidalCategory.{v, u} C
inst_4 : MonoidalClosed.{v, u} C
A B K L X Y : C
f : A ⟶ B
g : K ⟶ L
h : X ⟶ Y
⊢ HasLiftingProperty (Arrow.mk f □ Arrow.mk g).hom h ↔ HasLiftingProperty g (Opposite.op (Arrow.mk f) ⋔ Arrow.mk h).hom

Tactic:
ParametrizedAdjunction.hasLiftingProperty_iff MonoidalClosed.internalHomAdjunction₂
    (PushoutObjObj.ofHasPushout ..) (PullbackObjObj.ofHasPullback ..)

Premises used: CategoryTheory.Functor.PullbackObjObj.π, CategoryTheory.ParametrizedAdjunction.hasLiftingProperty_iff, CategoryTheory.Functor.PushoutObjObj.ofHasPushout, CategoryTheory.Limits.PushoutCocone.IsColimit.desc, CategoryTheory.Functor.PushoutObjObj.ι, CategoryTheory.Limits.colimit, CategoryTheory.Limits.PullbackCone.IsLimit.lift, CategoryTheory.Limits.limit, CategoryTheory.Functor.PullbackObjObj.ofHasPullback, CategoryTheory.IsPushout.desc, CategoryTheory.IsPullback.lift, CategoryTheory.MonoidalClosed.internalHomAdjunction₂
-- Module: Mathlib.CategoryTheory.LiftingProperties.PushoutProduct
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPushouts.{v, u} C
inst_2 : HasPullbacks.{v, u} C
inst_3 : MonoidalCategory.{v, u} C
inst_4 : MonoidalClosed.{v, u} C
inst_5 : BraidedCategory.{v, u} C
A B K L X Y : C
f : A ⟶ B
g : K ⟶ L
h : X ⟶ Y
rw : HasLiftingProperty (Arrow.mk f □ Arrow.mk g).hom h ↔ HasLiftingProperty (Arrow.mk g □ Arrow.mk f).hom h
⊢ HasLiftingProperty (Arrow.mk f □ Arrow.mk g).hom h ↔ HasLiftingProperty f (Opposite.op (Arrow.mk g) ⋔ Arrow.mk h).hom

Tactic:
rw [← hasLiftingProperty_mk_iff]

Premises used: CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.hasLiftingProperty_mk_iff
-- Module: Mathlib.CategoryTheory.LiftingProperties.PushoutProduct
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPushouts.{v, u} C
inst_2 : HasPullbacks.{v, u} C
inst_3 : MonoidalCategory.{v, u} C
inst_4 : MonoidalClosed.{v, u} C
inst_5 : BraidedCategory.{v, u} C
A B K L X Y : C
f : A ⟶ B
g : K ⟶ L
h : X ⟶ Y
⊢ HasLiftingProperty (Arrow.mk f □ Arrow.mk g).hom h ↔ HasLiftingProperty (Arrow.mk g □ Arrow.mk f).hom h

Tactic:
HasLiftingProperty.iff_of_arrow_iso_left (braiding _ _) h

Premises used: CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.braiding, CategoryTheory.Limits.PushoutCocone.IsColimit.desc, CategoryTheory.Functor.PushoutObjObj.ι, CategoryTheory.Limits.colimit, CategoryTheory.HasLiftingProperty.iff_of_arrow_iso_left, CategoryTheory.IsPushout.desc
-- Module: Mathlib.CategoryTheory.LiftingProperties.PushoutProduct
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPushouts.{v, u} C
inst_2 : HasPullbacks.{v, u} C
inst_3 : MonoidalCategory.{v, u} C
inst_4 : MonoidalClosed.{v, u} C
inst_5 : BraidedCategory.{v, u} C
A B K L X Y : C
f : A ⟶ B
g : K ⟶ L
h : X ⟶ Y
⊢ HasLiftingProperty (Arrow.mk f □ Arrow.mk g).hom h ↔ HasLiftingProperty (Arrow.mk g □ Arrow.mk f).hom h

Tactic:
exact HasLiftingProperty.iff_of_arrow_iso_left (braiding _ _) h

Premises used: CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.braiding, CategoryTheory.HasLiftingProperty.iff_of_arrow_iso_left
-- Module: Mathlib.CategoryTheory.LiftingProperties.PushoutProduct
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPushouts.{v, u} C
inst_2 : HasPullbacks.{v, u} C
inst_3 : CartesianMonoidalCategory.{v, u} C
inst_4 : MonoidalClosed.{v, u} C
inst_5 : BraidedCategory.{v, u} C
A B K L X Y : C
g : K ⟶ L
h : X ⟶ Y
i : IsInitial.{v, u} A
dsimp :
  HasLiftingProperty (A := pt (F := curriedTensor C) (ofHasPushout (curriedTensor C) (i.to B) g))
      (ι (ofHasPushout (curriedTensor C) (i.to B) g)) h ↔
    HasLiftingProperty (X := B ⟹ X) g (map (ihom B) h)
⊢ HasLiftingProperty (Arrow.mk (i.to B) □ Arrow.mk g).hom h ↔ HasLiftingProperty (X := B ⟹ X) g (map (ihom B) h)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.LiftingProperties.PushoutProduct
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPushouts.{v, u} C
inst_2 : HasPullbacks.{v, u} C
inst_3 : CartesianMonoidalCategory.{v, u} C
inst_4 : MonoidalClosed.{v, u} C
inst_5 : BraidedCategory.{v, u} C
A B K L X Y : C
g : K ⟶ L
h : X ⟶ Y
i : IsInitial.{v, u} A
⊢ HasLiftingProperty (A :=
      pt (F := curriedTensor C) (ofHasPushout (curriedTensor C) (Arrow.mk (i.to B)).hom (Arrow.mk g).hom))
      (ι (ofHasPushout (curriedTensor C) (Arrow.mk (i.to B)).hom (Arrow.mk g).hom)) h ↔
    HasLiftingProperty (A := tensorObj.{v, u} (𝒞 := inst) B (Arrow.mk g).left) (B ◁ (Arrow.mk g).hom) h

Tactic:
have := HasLiftingProperty.iff_of_arrow_iso_left (isInitialIso' g i (W := B)) h
-- Module: Mathlib.CategoryTheory.LiftingProperties.PushoutProduct
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPushouts.{v, u} C
inst_2 : HasPullbacks.{v, u} C
inst_3 : CartesianMonoidalCategory.{v, u} C
inst_4 : MonoidalClosed.{v, u} C
inst_5 : BraidedCategory.{v, u} C
A B K L X Y : C
g : K ⟶ L
h : X ⟶ Y
i : IsInitial.{v, u} A
this :
  HasLiftingProperty (A :=
      pt (F := curriedTensor C) (ofHasPushout (curriedTensor C) (Arrow.mk (i.to B)).hom (Arrow.mk g).hom))
      (ι (ofHasPushout (curriedTensor C) (Arrow.mk (i.to B)).hom (Arrow.mk g).hom)) h ↔
    HasLiftingProperty (A := tensorObj.{v, u} (𝒞 := inst) B (Arrow.mk g).left) (B ◁ (Arrow.mk g).hom) h
rw :
  HasLiftingProperty (A := tensorObj.{v, u} (𝒞 := inst) B K) (B ◁ g) h ↔
    HasLiftingProperty (X := B ⟹ X) g (map (ihom B) h)
⊢ HasLiftingProperty (A := pt (F := curriedTensor C) (ofHasPushout (curriedTensor C) (i.to B) g))
      (ι (ofHasPushout (curriedTensor C) (i.to B) g)) h ↔
    HasLiftingProperty (X := B ⟹ X) g (map (ihom B) h)

Tactic:
rw [dsimp% this]