awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.LiftingProperties.Limits
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y Z W : C
f : X ⟶ Y
s : X ⟶ Z
g : Z ⟶ W
t : Y ⟶ W
inst_1 : HasPushout s f
T₁ T₂ : C
p : T₁ ⟶ T₂
inst_2 : HasLiftingProperty f p
⊢ HasLiftingProperty (B := pushout s f) (pushout.inl s f) p

Tactic:
(IsPushout.of_hasPushout s f).hasLiftingProperty p

Premises used: CategoryTheory.IsPushout.of_hasPushout, CategoryTheory.IsPushout.hasLiftingProperty
-- Module: Mathlib.CategoryTheory.LiftingProperties.Limits
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y Z W : C
f : X ⟶ Y
s : X ⟶ Z
g : Z ⟶ W
t : Y ⟶ W
inst_1 : HasPushout s f
T₁ T₂ : C
p : T₁ ⟶ T₂
inst_2 : HasLiftingProperty s p
⊢ HasLiftingProperty (B := pushout s f) (pushout.inr s f) p

Tactic:
(IsPushout.of_hasPushout s f).flip.hasLiftingProperty p

Premises used: CategoryTheory.IsPushout.of_hasPushout, CategoryTheory.IsPushout.flip, CategoryTheory.IsPushout.hasLiftingProperty
-- Module: Mathlib.CategoryTheory.LiftingProperties.Limits
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y Z W : C
f : X ⟶ Y
s : X ⟶ Z
g : Z ⟶ W
t : Y ⟶ W
inst_1 : HasPullback g t
T₁ T₂ : C
p : T₁ ⟶ T₂
inst_2 : HasLiftingProperty p g
⊢ HasLiftingProperty (X := pullback g t) p (pullback.snd g t)

Tactic:
(IsPullback.of_hasPullback g t).hasLiftingProperty p

Premises used: CategoryTheory.IsPullback.hasLiftingProperty, CategoryTheory.IsPullback.of_hasPullback
-- Module: Mathlib.CategoryTheory.LiftingProperties.Limits
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y Z W : C
f : X ⟶ Y
s : X ⟶ Z
g : Z ⟶ W
t : Y ⟶ W
inst_1 : HasPullback g t
T₁ T₂ : C
p : T₁ ⟶ T₂
inst_2 : HasLiftingProperty p t
⊢ HasLiftingProperty (X := pullback g t) p (pullback.fst g t)

Tactic:
(IsPullback.of_hasPullback g t).flip.hasLiftingProperty p

Premises used: CategoryTheory.IsPullback.flip, CategoryTheory.IsPullback.hasLiftingProperty, CategoryTheory.IsPullback.of_hasPullback
-- Module: Mathlib.CategoryTheory.LiftingProperties.Limits
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X_1 Y_1 Z W : C
f_1 : X_1 ⟶ Y_1
s : X_1 ⟶ Z
g : Z ⟶ W
t_1 : Y_1 ⟶ W
J : Type u_2
A B : J → C
inst_1 : HasProduct.{u_2, v_1, u_1} A
inst_2 : HasProduct.{u_2, v_1, u_1} B
f : (j : J) → A j ⟶ B j
X Y : C
p : X ⟶ Y
inst_3 : ∀ (j : J), HasLiftingProperty p (f j)
t : X ⟶ piObj.{u_2, v_1, u_1} A
b : Y ⟶ piObj.{u_2, v_1, u_1} B
sq : CommSq t p (Limits.Pi.map f) b
j : J
rw : (t ≫ Pi.π A j) ≫ f j = CategoryStruct.comp (Y := piObj.{u_2, v_1, u_1} B) (t ≫ Limits.Pi.map f) (Pi.π B j)
⊢ (t ≫ Pi.π A j) ≫ f j = p ≫ b ≫ Pi.π B j

Tactic:
rw [← Category.assoc, ← sq.w]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.CommSq.w
-- Module: Mathlib.CategoryTheory.LiftingProperties.Limits
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X_1 Y_1 Z W : C
f_1 : X_1 ⟶ Y_1
s : X_1 ⟶ Z
g : Z ⟶ W
t_1 : Y_1 ⟶ W
J : Type u_2
A B : J → C
inst_1 : HasProduct.{u_2, v_1, u_1} A
inst_2 : HasProduct.{u_2, v_1, u_1} B
f : (j : J) → A j ⟶ B j
X Y : C
p : X ⟶ Y
inst_3 : ∀ (j : J), HasLiftingProperty p (f j)
t : X ⟶ piObj.{u_2, v_1, u_1} A
b : Y ⟶ piObj.{u_2, v_1, u_1} B
sq : CommSq t p (Limits.Pi.map f) b
j : J
⊢ (t ≫ Pi.π A j) ≫ f j = CategoryStruct.comp (Y := piObj.{u_2, v_1, u_1} B) (t ≫ Limits.Pi.map f) (Pi.π B j)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.LiftingProperties.Limits
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X_1 Y_1 Z W : C
f_1 : X_1 ⟶ Y_1
s : X_1 ⟶ Z
g : Z ⟶ W
t_1 : Y_1 ⟶ W
J : Type u_2
A B : J → C
inst_1 : HasProduct.{u_2, v_1, u_1} A
inst_2 : HasProduct.{u_2, v_1, u_1} B
f : (j : J) → A j ⟶ B j
X Y : C
p : X ⟶ Y
inst_3 : ∀ (j : J), HasLiftingProperty p (f j)
t : X ⟶ piObj.{u_2, v_1, u_1} A
b : Y ⟶ piObj.{u_2, v_1, u_1} B
sq : CommSq t p (Limits.Pi.map f) b
⊢ ∀ (j : J), CommSq (t ≫ Pi.π A j) p (f j) (b ≫ Pi.π B j)

Tactic:
have sq' (j : J) :
        CommSq (t ≫ Pi.π _ j) p (f j) (b ≫ Pi.π _ j) :=
      ⟨by rw [← Category.assoc, ← sq.w]; simp⟩
-- Module: Mathlib.CategoryTheory.LiftingProperties.Limits
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X_1 Y_1 Z W : C
f_1 : X_1 ⟶ Y_1
s : X_1 ⟶ Z
g : Z ⟶ W
t_1 : Y_1 ⟶ W
J : Type u_2
A B : J → C
inst_1 : HasProduct.{u_2, v_1, u_1} A
inst_2 : HasProduct.{u_2, v_1, u_1} B
f : (j : J) → A j ⟶ B j
X Y : C
p : X ⟶ Y
inst_3 : ∀ (j : J), HasLiftingProperty p (f j)
t : X ⟶ piObj.{u_2, v_1, u_1} A
b : Y ⟶ piObj.{u_2, v_1, u_1} B
sq : CommSq t p (Limits.Pi.map f) b
sq' : ∀ (j : J), CommSq (t ≫ Pi.π A j) p (f j) (b ≫ Pi.π B j)
⊢ sq.HasLift

Tactic:
⟨⟨{ l := Pi.lift (fun j ↦ (sq' j).lift) }⟩⟩

Premises used: CategoryTheory.CommSq.lift, Nonempty.intro, CategoryTheory.CommSq.LiftStruct.mk, CategoryTheory.CommSq.HasLift.mk, CategoryTheory.Limits.Pi.lift
-- Module: Mathlib.CategoryTheory.LiftingProperties.Limits
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X_1 Y_1 Z W : C
f_1 : X_1 ⟶ Y_1
s : X_1 ⟶ Z
g : Z ⟶ W
t_1 : Y_1 ⟶ W
J : Type u_2
A B : J → C
inst_1 : HasProduct.{u_2, v_1, u_1} A
inst_2 : HasProduct.{u_2, v_1, u_1} B
f : (j : J) → A j ⟶ B j
X Y : C
p : X ⟶ Y
inst_3 : ∀ (j : J), HasLiftingProperty p (f j)
t : X ⟶ piObj.{u_2, v_1, u_1} A
b : Y ⟶ piObj.{u_2, v_1, u_1} B
sq : CommSq t p (Limits.Pi.map f) b
sq' : ∀ (j : J), CommSq (t ≫ Pi.π A j) p (f j) (b ≫ Pi.π B j)
⊢ sq.HasLift

Tactic:
exact ⟨⟨{ l := Pi.lift (fun j ↦ (sq' j).lift) }⟩⟩
-- Module: Mathlib.CategoryTheory.LiftingProperties.Limits
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X_1 Y_1 Z W : C
f_1 : X_1 ⟶ Y_1
s : X_1 ⟶ Z
g : Z ⟶ W
t_1 : Y_1 ⟶ W
J : Type u_2
A B : J → C
inst_1 : HasCoproduct.{u_2, v_1, u_1} A
inst_2 : HasCoproduct.{u_2, v_1, u_1} B
f : (j : J) → A j ⟶ B j
X Y : C
p : X ⟶ Y
inst_3 : ∀ (j : J), HasLiftingProperty (f j) p
t : sigmaObj.{u_2, v_1, u_1} A ⟶ X
b : sigmaObj.{u_2, v_1, u_1} B ⟶ Y
sq : CommSq t (Limits.Sigma.map f) p b
j : J
⊢ (Sigma.ι A j ≫ t) ≫ p = f j ≫ Sigma.ι B j ≫ b

Tactic:
simp [sq.w]

Premises used: CategoryTheory.CommSq.w
-- Module: Mathlib.CategoryTheory.LiftingProperties.Limits
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X_1 Y_1 Z W : C
f_1 : X_1 ⟶ Y_1
s : X_1 ⟶ Z
g : Z ⟶ W
t_1 : Y_1 ⟶ W
J : Type u_2
A B : J → C
inst_1 : HasCoproduct.{u_2, v_1, u_1} A
inst_2 : HasCoproduct.{u_2, v_1, u_1} B
f : (j : J) → A j ⟶ B j
X Y : C
p : X ⟶ Y
inst_3 : ∀ (j : J), HasLiftingProperty (f j) p
t : sigmaObj.{u_2, v_1, u_1} A ⟶ X
b : sigmaObj.{u_2, v_1, u_1} B ⟶ Y
sq : CommSq t (Limits.Sigma.map f) p b
⊢ ∀ (j : J), CommSq (Sigma.ι A j ≫ t) (f j) p (Sigma.ι B j ≫ b)

Tactic:
have sq' (j : J) :
        CommSq (Sigma.ι _ j ≫ t) (f j) p (Sigma.ι _ j ≫ b) :=
      ⟨by simp [sq.w]⟩
-- Module: Mathlib.CategoryTheory.LiftingProperties.Limits
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X_1 Y_1 Z W : C
f_1 : X_1 ⟶ Y_1
s : X_1 ⟶ Z
g : Z ⟶ W
t_1 : Y_1 ⟶ W
J : Type u_2
A B : J → C
inst_1 : HasCoproduct.{u_2, v_1, u_1} A
inst_2 : HasCoproduct.{u_2, v_1, u_1} B
f : (j : J) → A j ⟶ B j
X Y : C
p : X ⟶ Y
inst_3 : ∀ (j : J), HasLiftingProperty (f j) p
t : sigmaObj.{u_2, v_1, u_1} A ⟶ X
b : sigmaObj.{u_2, v_1, u_1} B ⟶ Y
sq : CommSq t (Limits.Sigma.map f) p b
sq' : ∀ (j : J), CommSq (Sigma.ι A j ≫ t) (f j) p (Sigma.ι B j ≫ b)
⊢ sq.HasLift

Tactic:
⟨⟨{ l := Sigma.desc (fun j ↦ (sq' j).lift) }⟩⟩

Premises used: CategoryTheory.CommSq.lift, Nonempty.intro, CategoryTheory.CommSq.LiftStruct.mk, CategoryTheory.CommSq.HasLift.mk, CategoryTheory.Limits.Sigma.desc
-- Module: Mathlib.CategoryTheory.LiftingProperties.Limits
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X_1 Y_1 Z W : C
f_1 : X_1 ⟶ Y_1
s : X_1 ⟶ Z
g : Z ⟶ W
t_1 : Y_1 ⟶ W
J : Type u_2
A B : J → C
inst_1 : HasCoproduct.{u_2, v_1, u_1} A
inst_2 : HasCoproduct.{u_2, v_1, u_1} B
f : (j : J) → A j ⟶ B j
X Y : C
p : X ⟶ Y
inst_3 : ∀ (j : J), HasLiftingProperty (f j) p
t : sigmaObj.{u_2, v_1, u_1} A ⟶ X
b : sigmaObj.{u_2, v_1, u_1} B ⟶ Y
sq : CommSq t (Limits.Sigma.map f) p b
sq' : ∀ (j : J), CommSq (Sigma.ι A j ≫ t) (f j) p (Sigma.ι B j ≫ b)
⊢ sq.HasLift

Tactic:
exact ⟨⟨{ l := Sigma.desc (fun j ↦ (sq' j).lift) }⟩⟩
-- Module: Mathlib.CategoryTheory.LiftingProperties.Over
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
rw₂ rw₃ : sq'.lift ≫ X₂.hom = sq'.lift ≫ X₂.hom
⊢ sq'.lift ≫ X₂.hom = X₃.hom

Tactic:
rw [← Over.w b, ← sq'.fac_right_assoc, Over.w r]

Premises used: CategoryTheory.CommSq.fac_right_assoc, CategoryTheory.Over.w
-- Module: Mathlib.CategoryTheory.LiftingProperties.Over
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) := ⋯
⊢ sq.HasLift

Tactic:
exact ⟨⟨{
    l := Over.homMk sq'.lift
      (by rw [← Over.w b, ← sq'.fac_right_assoc, Over.w r])
  }⟩⟩
-- Module: Mathlib.CategoryTheory.LiftingProperties.Over
Goal:
C : Type u
inst : Category.{v, u} C
S : C
A B X Y : Over.{v, u} S
i : A ⟶ B
p : X ⟶ Y
inst_1 : HasLiftingProperty (Over.Hom.left i) (Over.Hom.left p)
⊢ HasLiftingProperty i p

Tactic:
⟨fun _ ↦ .over⟩

Premises used: CategoryTheory.CommSq.HasLift.over, CategoryTheory.HasLiftingProperty.mk
-- Module: Mathlib.CategoryTheory.LiftingProperties.ParametrizedAdjunction
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
F : C₁ ⥤ Functor.{v₂, v₃, u₂, u₃} C₂ C₃
G : C₁ᵒᵖ ⥤ Functor.{v₃, v₂, u₃, u₂} C₃ C₂
adj₂ : F ⊣₂ G
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
X₃ Y₃ : C₃
f₃ : X₃ ⟶ Y₃
sq₁₂ : F.PushoutObjObj f₁ f₂
sq₁₃ : G.PullbackObjObj f₁ f₃
α : Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃
⊢ Eq.{v₂ + 1} (α := (Arrow.mk f₂).right ⟶ (G.obj (op X₁)).obj Y₃)
    (((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 α) ≫
        (G.obj (op X₁)).map f₃ :
      (Arrow.mk f₂).right ⟶ (G.obj (op X₁)).obj Y₃)
    (((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 α) ≫
        (G.map f₁.op).app Y₃ :
      (Arrow.mk f₂).right ⟶ (G.obj (op X₁)).obj Y₃)

Tactic:
simp [← adj₂.homEquiv_naturality_one,
              ← adj₂.homEquiv_naturality_three]

Premises used: CategoryTheory.ParametrizedAdjunction.homEquiv_naturality_three, 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₃
⊢ (((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 ≫
        ⋯.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 α))
          ⋯) ≫
      sq₁₃.fst

Tactic:
simp [← adj₂.homEquiv_naturality_two,
                ← adj₂.homEquiv_naturality_one,
                sq₁₂.isPushout.w_assoc]

Premises used: CategoryTheory.ParametrizedAdjunction.homEquiv_naturality_two, CategoryTheory.Functor.PushoutObjObj.isPushout, CategoryTheory.IsPushout.toCommSq, CategoryTheory.CommSq.w_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₃
⊢ (((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₁₃.snd =
    ((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 α))
          ⋯) ≫
      sq₁₃.snd

Tactic:
simp [← adj₂.homEquiv_naturality_two,
                ← adj₂.homEquiv_naturality_three]

Premises used: CategoryTheory.ParametrizedAdjunction.homEquiv_naturality_two, CategoryTheory.ParametrizedAdjunction.homEquiv_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 f₂ ⟶ Arrow.mk sq₁₃.π
⊢ (Arrow.Hom.left β ≫ (Arrow.mk sq₁₃.π).hom) ≫ sq₁₃.fst = ((Arrow.mk f₂).hom ≫ Arrow.Hom.right β) ≫ sq₁₃.fst

Tactic:
have := Arrow.w β =≫ 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 f₂ ⟶ Arrow.mk sq₁₃.π
this : (Arrow.Hom.left β ≫ sq₁₃.π) ≫ sq₁₃.fst = (f₂ ≫ Arrow.Hom.right β) ≫ sq₁₃.fst
⊢ Arrow.Hom.left β ≫ (G.map f₁.op).app X₃ = f₂ ≫ Arrow.Hom.right β ≫ 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 f₂ ⟶ Arrow.mk sq₁₃.π
this : Arrow.Hom.left β ≫ (G.map f₁.op).app X₃ = 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))

Tactic:
simp only [← adj₂.homEquiv_symm_naturality_one,
            ← adj₂.homEquiv_symm_naturality_two,
            Arrow.mk_left, Arrow.mk_right, this]

Premises used: CategoryTheory.ParametrizedAdjunction.homEquiv_symm_naturality_one, CategoryTheory.Arrow.mk_right, CategoryTheory.ParametrizedAdjunction.homEquiv_symm_naturality_two, CategoryTheory.Arrow.mk_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 f₂ ⟶ Arrow.mk sq₁₃.π
⊢ (Arrow.Hom.left β ≫ (Arrow.mk sq₁₃.π).hom) ≫ sq₁₃.snd = ((Arrow.mk f₂).hom ≫ Arrow.Hom.right β) ≫ sq₁₃.snd

Tactic:
have := Arrow.w β =≫ sq₁₃.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 f₂ ⟶ Arrow.mk sq₁₃.π
this : (Arrow.Hom.left β ≫ sq₁₃.π) ≫ sq₁₃.snd = (f₂ ≫ Arrow.Hom.right β) ≫ sq₁₃.snd
⊢ Arrow.Hom.left β ≫ (G.obj (op Y₁)).map f₃ = f₂ ≫ Arrow.Hom.right β ≫ sq₁₃.snd

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

Premises used: CategoryTheory.Category.assoc, 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 f₂ ⟶ Arrow.mk sq₁₃.π
this : Arrow.Hom.left β ≫ (G.obj (op Y₁)).map f₃ = 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)

Tactic:
simp [← adj₂.homEquiv_symm_naturality_two,
            ← adj₂.homEquiv_symm_naturality_three, this]

Premises used: CategoryTheory.ParametrizedAdjunction.homEquiv_symm_naturality_three, CategoryTheory.ParametrizedAdjunction.homEquiv_symm_naturality_two
-- Module: Mathlib.CategoryTheory.LiftingProperties.ParametrizedAdjunction
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
F : C₁ ⥤ Functor.{v₂, v₃, u₂, u₃} C₂ C₃
G : C₁ᵒᵖ ⥤ Functor.{v₃, v₂, u₃, u₂} C₃ C₂
adj₂ : F ⊣₂ G
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
X₃ Y₃ : C₃
f₃ : X₃ ⟶ Y₃
sq₁₂ : F.PushoutObjObj f₁ f₂
sq₁₃ : G.PullbackObjObj f₁ f₃
β : Arrow.mk f₂ ⟶ Arrow.mk sq₁₃.π
⊢ sq₁₂.inr ≫
      ⋯.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₁₂.inr ≫
      (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:
simp [← adj₂.homEquiv_symm_naturality_one,
            ← adj₂.homEquiv_symm_naturality_three, sq₁₃.isPullback.w]

Premises used: CategoryTheory.ParametrizedAdjunction.homEquiv_symm_naturality_one, CategoryTheory.ParametrizedAdjunction.homEquiv_symm_naturality_three, CategoryTheory.IsPullback.toCommSq, CategoryTheory.CommSq.w, CategoryTheory.Functor.PullbackObjObj.isPullback