awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.LiftingProperties.Adjunction
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
F : Functor.{v_2, v_1, u_2, u_1} D C
adj : G ⊣ F
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
h : HasLiftingProperty (G.map i) p
f : A ⟶ F.obj X
g : B ⟶ F.obj Y
sq : CommSq f i (F.map p) g
mp : ⋯.HasLift
⊢ sq.HasLift

Tactic:
rw [← sq.left_adjoint_hasLift_iff adj]

Premises used: CategoryTheory.CommSq.left_adjoint_hasLift_iff
-- Module: Mathlib.CategoryTheory.LiftingProperties.Adjunction
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
F : Functor.{v_2, v_1, u_2, u_1} D C
adj : G ⊣ F
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
h : HasLiftingProperty (G.map i) p
f : A ⟶ F.obj X
g : B ⟶ F.obj Y
sq : CommSq f i (F.map p) g
⊢ ⋯.HasLift

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.LiftingProperties.Adjunction
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
F : Functor.{v_2, v_1, u_2, u_1} D C
adj : G ⊣ F
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
h : HasLiftingProperty i (F.map p)
f : G.obj A ⟶ X
g : G.obj B ⟶ Y
sq : CommSq f (G.map i) p g
mpr : ⋯.HasLift
⊢ sq.HasLift

Tactic:
rw [← sq.right_adjoint_hasLift_iff adj]

Premises used: CategoryTheory.CommSq.right_adjoint_hasLift_iff
-- Module: Mathlib.CategoryTheory.LiftingProperties.Adjunction
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
F : Functor.{v_2, v_1, u_2, u_1} D C
adj : G ⊣ F
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
h : HasLiftingProperty i (F.map p)
f : G.obj A ⟶ X
g : G.obj B ⟶ Y
sq : CommSq f (G.map i) p g
⊢ ⋯.HasLift

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.LiftingProperties.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B B' X Y Y' : C
i : A ⟶ B
i' : B ⟶ B'
p : X ⟶ Y
p' : Y ⟶ Y'
f : A ⟶ X
g : B ⟶ Y
sq : CommSq f i p g
hip : HasLiftingProperty i p
⊢ sq.HasLift

Tactic:
hip.sq_hasLift _

Premises used: CategoryTheory.HasLiftingProperty.sq_hasLift
-- Module: Mathlib.CategoryTheory.LiftingProperties.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
h : HasLiftingProperty i p
f : Opposite.op Y ⟶ Opposite.op B
g : Opposite.op X ⟶ Opposite.op A
sq : CommSq f p.op i.op g
simp : CommSq.HasLift (g := f.unop) ⋯
⊢ sq.HasLift

Tactic:
simp only [CommSq.HasLift.iff_unop, Quiver.Hom.unop_op]

Premises used: Quiver.Hom.unop_op, CategoryTheory.CommSq.HasLift.iff_unop
-- Module: Mathlib.CategoryTheory.LiftingProperties.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
h : HasLiftingProperty i p
f : Opposite.op Y ⟶ Opposite.op B
g : Opposite.op X ⟶ Opposite.op A
sq : CommSq f p.op i.op g
⊢ CommSq.HasLift (g := f.unop) ⋯

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.LiftingProperties.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B X Y : Cᵒᵖ
i : A ⟶ B
p : X ⟶ Y
h : HasLiftingProperty.{v_1, u_1} (C := Cᵒᵖ) (A := A) (B := B) (X := X) (Y := Y) i p
f : Opposite.unop Y ⟶ Opposite.unop B
g : Opposite.unop X ⟶ Opposite.unop A
sq : CommSq f p.unop i.unop g
rw : ⋯.HasLift
⊢ sq.HasLift

Tactic:
rw [CommSq.HasLift.iff_op]

Premises used: CategoryTheory.CommSq.HasLift.iff_op
-- Module: Mathlib.CategoryTheory.LiftingProperties.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B X Y : Cᵒᵖ
i : A ⟶ B
p : X ⟶ Y
h : HasLiftingProperty.{v_1, u_1} (C := Cᵒᵖ) (A := A) (B := B) (X := X) (Y := Y) i p
f : Opposite.unop Y ⟶ Opposite.unop B
g : Opposite.unop X ⟶ Opposite.unop A
sq : CommSq f p.unop i.unop g
simp : CommSq.HasLift (g := f.op) ⋯
⊢ ⋯.HasLift

Tactic:
simp only [Quiver.Hom.op_unop]

Premises used: Quiver.Hom.op_unop
-- Module: Mathlib.CategoryTheory.LiftingProperties.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B X Y : Cᵒᵖ
i : A ⟶ B
p : X ⟶ Y
h : HasLiftingProperty.{v_1, u_1} (C := Cᵒᵖ) (A := A) (B := B) (X := X) (Y := Y) i p
f : Opposite.unop Y ⟶ Opposite.unop B
g : Opposite.unop X ⟶ Opposite.unop A
sq : CommSq f p.unop i.unop g
⊢ CommSq.HasLift (g := f.op) ⋯

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.LiftingProperties.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
⊢ HasLiftingProperty i p ↔
    HasLiftingProperty.{v_1, u_1} (C := Cᵒᵖ) (A := Opposite.op Y) (B := Opposite.op X) (X := Opposite.op B) (Y :=
      Opposite.op A) p.op i.op

Tactic:
⟨op, unop⟩

Premises used: CategoryTheory.HasLiftingProperty.unop, CategoryTheory.HasLiftingProperty.op, Iff.intro
-- Module: Mathlib.CategoryTheory.LiftingProperties.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B X Y : Cᵒᵖ
i : A ⟶ B
p : X ⟶ Y
⊢ HasLiftingProperty.{v_1, u_1} (C := Cᵒᵖ) (A := A) (B := B) (X := X) (Y := Y) i p ↔ HasLiftingProperty p.unop i.unop

Tactic:
⟨unop, op⟩

Premises used: CategoryTheory.HasLiftingProperty.unop, CategoryTheory.HasLiftingProperty.op, Iff.intro
-- Module: Mathlib.CategoryTheory.LiftingProperties.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B B' X Y Y' : C
i : A ⟶ B
i' : B ⟶ B'
p : X ⟶ Y
p' : Y ⟶ Y'
inst_1 : IsIso i
f : A ⟶ X
g : B ⟶ Y
sq : CommSq f i p g
⊢ i ≫ inv i ≫ f = f

Tactic:
simp only [IsIso.hom_inv_id_assoc]

Premises used: CategoryTheory.IsIso.hom_inv_id_assoc
-- Module: Mathlib.CategoryTheory.LiftingProperties.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B B' X Y Y' : C
i : A ⟶ B
i' : B ⟶ B'
p : X ⟶ Y
p' : Y ⟶ Y'
inst_1 : IsIso i
f : A ⟶ X
g : B ⟶ Y
sq : CommSq f i p g
⊢ (inv i ≫ f) ≫ p = g

Tactic:
simp only [sq.w, assoc, IsIso.inv_hom_id_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.CommSq.w, CategoryTheory.IsIso.inv_hom_id_assoc
-- Module: Mathlib.CategoryTheory.LiftingProperties.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B B' X Y Y' : C
i : A ⟶ B
i' : B ⟶ B'
p : X ⟶ Y
p' : Y ⟶ Y'
inst_1 : HasLiftingProperty i p
inst_2 : HasLiftingProperty i' p
f : A ⟶ X
g : B' ⟶ Y
sq : CommSq f (i ≫ i') p g
⊢ f ≫ p = (i ≫ i') ≫ g

Tactic:
have fac := sq.w
-- Module: Mathlib.CategoryTheory.LiftingProperties.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B B' X Y Y' : C
i : A ⟶ B
i' : B ⟶ B'
p : X ⟶ Y
p' : Y ⟶ Y'
inst_1 : HasLiftingProperty i p
inst_2 : HasLiftingProperty i' p
f : A ⟶ X
g : B' ⟶ Y
sq : CommSq f (i ≫ i') p g
fac : f ≫ p = (i ≫ i') ≫ g
⊢ f ≫ p = i ≫ i' ≫ g

Tactic:
rw [assoc] at fac

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.LiftingProperties.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B B' X Y Y' : C
i : A ⟶ B
i' : B ⟶ B'
p : X ⟶ Y
p' : Y ⟶ Y'
inst_1 : HasLiftingProperty i p
inst_2 : HasLiftingProperty i' p
f : A ⟶ X
g : B' ⟶ Y
sq : CommSq f (i ≫ i') p g
fac : f ≫ p = i ≫ i' ≫ g
⊢ (i ≫ i') ≫ CommSq.lift (f := ⋯.lift) ⋯ = f

Tactic:
simp only [assoc, CommSq.fac_left]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.CommSq.fac_left
-- Module: Mathlib.CategoryTheory.LiftingProperties.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B B' X Y Y' : C
i : A ⟶ B
i' : B ⟶ B'
p : X ⟶ Y
p' : Y ⟶ Y'
inst_1 : HasLiftingProperty i p
inst_2 : HasLiftingProperty i' p
f : A ⟶ X
g : B' ⟶ Y
sq : CommSq f (i ≫ i') p g
fac : f ≫ p = i ≫ i' ≫ g
⊢ CommSq.lift (f := ⋯.lift) ⋯ ≫ p = g

Tactic:
simp only [CommSq.fac_right]

Premises used: CategoryTheory.CommSq.fac_right
-- Module: Mathlib.CategoryTheory.LiftingProperties.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B B' X Y Y' : C
i : A ⟶ B
i' : B ⟶ B'
p : X ⟶ Y
p' : Y ⟶ Y'
inst_1 : HasLiftingProperty i p
inst_2 : HasLiftingProperty i' p
f : A ⟶ X
g : B' ⟶ Y
sq : CommSq f (i ≫ i') p g
fac : f ≫ p = i ≫ i' ≫ g
⊢ sq.HasLift

Tactic:
exact
      CommSq.HasLift.mk'
        { l := (CommSq.mk (CommSq.mk fac).fac_right).lift
          fac_left := by simp only [assoc, CommSq.fac_left]
          fac_right := by simp only [CommSq.fac_right] }

Premises used: CategoryTheory.CommSq.HasLift.mk', CategoryTheory.CommSq.lift, CategoryTheory.CommSq.fac_right, CategoryTheory.CommSq.mk, CategoryTheory.CommSq.LiftStruct.mk
-- Module: Mathlib.CategoryTheory.LiftingProperties.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B A' B' X Y : C
i : A ⟶ B
i' : A' ⟶ B'
e : Arrow.mk i ≅ Arrow.mk i'
p : X ⟶ Y
hip : HasLiftingProperty i p
rw : HasLiftingProperty (Arrow.Hom.left e.inv ≫ i ≫ Arrow.Hom.right e.hom) p
⊢ HasLiftingProperty i' p

Tactic:
rw [Arrow.iso_w' e]

Premises used: CategoryTheory.Arrow.iso_w'
-- Module: Mathlib.CategoryTheory.LiftingProperties.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B A' B' X Y : C
i : A ⟶ B
i' : A' ⟶ B'
e : Arrow.mk i ≅ Arrow.mk i'
p : X ⟶ Y
hip : HasLiftingProperty i p
⊢ HasLiftingProperty (Arrow.Hom.left e.inv ≫ i ≫ Arrow.Hom.right e.hom) p

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.LiftingProperties.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B X Y X' Y' : C
i : A ⟶ B
p : X ⟶ Y
p' : X' ⟶ Y'
e : Arrow.mk p ≅ Arrow.mk p'
hip : HasLiftingProperty i p
rw : HasLiftingProperty i (Arrow.Hom.left e.inv ≫ p ≫ Arrow.Hom.right e.hom)
⊢ HasLiftingProperty i p'

Tactic:
rw [Arrow.iso_w' e]

Premises used: CategoryTheory.Arrow.iso_w'
-- Module: Mathlib.CategoryTheory.LiftingProperties.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B X Y X' Y' : C
i : A ⟶ B
p : X ⟶ Y
p' : X' ⟶ Y'
e : Arrow.mk p ≅ Arrow.mk p'
hip : HasLiftingProperty i p
⊢ HasLiftingProperty i (Arrow.Hom.left e.inv ≫ p ≫ Arrow.Hom.right e.hom)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.LiftingProperties.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B A' B' X Y : C
i : A ⟶ B
i' : A' ⟶ B'
e : Arrow.mk i ≅ Arrow.mk i'
p : X ⟶ Y
mp : HasLiftingProperty i p → HasLiftingProperty i' p
mpr : HasLiftingProperty i' p → HasLiftingProperty i p
⊢ HasLiftingProperty i p ↔ HasLiftingProperty i' p

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.LiftingProperties.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B A' B' X Y : C
i : A ⟶ B
i' : A' ⟶ B'
e : Arrow.mk i ≅ Arrow.mk i'
p : X ⟶ Y
h : HasLiftingProperty i p
⊢ HasLiftingProperty i' p

Tactic:
of_arrow_iso_left e p

Premises used: CategoryTheory.HasLiftingProperty.of_arrow_iso_left
-- Module: Mathlib.CategoryTheory.LiftingProperties.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B A' B' X Y : C
i : A ⟶ B
i' : A' ⟶ B'
e : Arrow.mk i ≅ Arrow.mk i'
p : X ⟶ Y
h : HasLiftingProperty i' p
⊢ HasLiftingProperty i p

Tactic:
of_arrow_iso_left e.symm p

Premises used: CategoryTheory.Iso.symm, CategoryTheory.HasLiftingProperty.of_arrow_iso_left
-- Module: Mathlib.CategoryTheory.LiftingProperties.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B A' B' X Y : C
i : A ⟶ B
i' : A' ⟶ B'
e : Arrow.mk i ≅ Arrow.mk i'
p : X ⟶ Y
h : HasLiftingProperty i p
⊢ HasLiftingProperty i' p

Tactic:
exacts [of_arrow_iso_left e p, of_arrow_iso_left e.symm p]

Premises used: CategoryTheory.HasLiftingProperty.of_arrow_iso_left
-- Module: Mathlib.CategoryTheory.LiftingProperties.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B X Y X' Y' : C
i : A ⟶ B
p : X ⟶ Y
p' : X' ⟶ Y'
e : Arrow.mk p ≅ Arrow.mk p'
mp : HasLiftingProperty i p → HasLiftingProperty i p'
mpr : HasLiftingProperty i p' → HasLiftingProperty i p
⊢ HasLiftingProperty i p ↔ HasLiftingProperty i p'

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.LiftingProperties.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B X Y X' Y' : C
i : A ⟶ B
p : X ⟶ Y
p' : X' ⟶ Y'
e : Arrow.mk p ≅ Arrow.mk p'
h : HasLiftingProperty i p
⊢ HasLiftingProperty i p'

Tactic:
of_arrow_iso_right i e

Premises used: CategoryTheory.HasLiftingProperty.of_arrow_iso_right
-- Module: Mathlib.CategoryTheory.LiftingProperties.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B X Y X' Y' : C
i : A ⟶ B
p : X ⟶ Y
p' : X' ⟶ Y'
e : Arrow.mk p ≅ Arrow.mk p'
h : HasLiftingProperty i p'
⊢ HasLiftingProperty i p

Tactic:
of_arrow_iso_right i e.symm

Premises used: CategoryTheory.Iso.symm, CategoryTheory.HasLiftingProperty.of_arrow_iso_right
-- Module: Mathlib.CategoryTheory.LiftingProperties.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B X Y X' Y' : C
i : A ⟶ B
p : X ⟶ Y
p' : X' ⟶ Y'
e : Arrow.mk p ≅ Arrow.mk p'
h : HasLiftingProperty i p
⊢ HasLiftingProperty i p'

Tactic:
exacts [of_arrow_iso_right i e, of_arrow_iso_right i e.symm]

Premises used: CategoryTheory.HasLiftingProperty.of_arrow_iso_right
-- Module: Mathlib.CategoryTheory.LiftingProperties.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y Z W Z' W' : C
g : Z ⟶ W
g' : Z' ⟶ W'
h : RetractArrow g' g
f : X ⟶ Y
inst_1 : HasLiftingProperty g f
u : Z' ⟶ X
v : W' ⟶ Y
sq : CommSq u g' f v
⊢ CommSq (Arrow.Hom.left h.r ≫ u) g f (Arrow.Hom.right h.r ≫ v)

Tactic:
simp only [Arrow.mk_left,
      Arrow.mk_right, Category.assoc, sq.w, Arrow.w_mk_right_assoc, Arrow.mk_hom, CommSq.mk]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Arrow.w_mk_right_assoc, CategoryTheory.Arrow.mk_right, CategoryTheory.CommSq.mk, CategoryTheory.Arrow.mk_hom, CategoryTheory.CommSq.w, CategoryTheory.Arrow.mk_left
-- Module: Mathlib.CategoryTheory.LiftingProperties.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y Z W Z' W' : C
g : Z ⟶ W
g' : Z' ⟶ W'
h : RetractArrow g' g
f : X ⟶ Y
inst_1 : HasLiftingProperty g f
u : Z' ⟶ X
v : W' ⟶ Y
sq : CommSq u g' f v
⊢ CommSq (Arrow.Hom.left h.r ≫ u) g f (Arrow.Hom.right h.r ≫ v)

Tactic:
have sq' : CommSq (h.r.left ≫ u) g f (h.r.right ≫ v) := by simp only [Arrow.mk_left,
      Arrow.mk_right, Category.assoc, sq.w, Arrow.w_mk_right_assoc, Arrow.mk_hom, CommSq.mk]
-- Module: Mathlib.CategoryTheory.LiftingProperties.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y Z W Z' W' : C
g : Z ⟶ W
g' : Z' ⟶ W'
h : RetractArrow g' g
f : X ⟶ Y
inst_1 : HasLiftingProperty g f
u : Z' ⟶ X
v : W' ⟶ Y
sq : CommSq u g' f v
sq' : CommSq (Arrow.Hom.left h.r ≫ u) g f (Arrow.Hom.right h.r ≫ v)
⊢ g' ≫ Arrow.Hom.right h.i ≫ sq'.lift = u

Tactic:
simp only [← h.i_w_assoc, sq'.fac_left, h.retract_left_assoc,
              Arrow.mk_left, Category.id_comp]

Premises used: CategoryTheory.RetractArrow.retract_left_assoc, CategoryTheory.Arrow.mk_left, CategoryTheory.RetractArrow.i_w_assoc, CategoryTheory.CommSq.fac_left, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.LiftingProperties.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y Z W Z' W' : C
g : Z ⟶ W
g' : Z' ⟶ W'
h : RetractArrow g' g
f : X ⟶ Y
inst_1 : HasLiftingProperty g f
u : Z' ⟶ X
v : W' ⟶ Y
sq : CommSq u g' f v
sq' : CommSq (Arrow.Hom.left h.r ≫ u) g f (Arrow.Hom.right h.r ≫ v)
⊢ sq.HasLift

Tactic:
exact
      ⟨⟨{ l := h.i.right ≫ sq'.lift
          fac_left := by
            simp only [← h.i_w_assoc, sq'.fac_left, h.retract_left_assoc,
              Arrow.mk_left, Category.id_comp]}⟩⟩
-- Module: Mathlib.CategoryTheory.LiftingProperties.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y Z W X' Y' : C
f : X ⟶ Y
f' : X' ⟶ Y'
h : RetractArrow f' f
g : Z ⟶ W
inst_1 : HasLiftingProperty g f
u : Z ⟶ X'
v : W ⟶ Y'
sq : CommSq u g f' v
rw : (u ≫ Arrow.Hom.left h.i) ≫ f = (g ≫ v) ≫ Arrow.Hom.right h.i
rw₁ : (u ≫ Arrow.Hom.left h.i) ≫ f = (u ≫ f') ≫ Arrow.Hom.right h.i
rw₂ : u ≫ Arrow.Hom.left h.i ≫ f = (u ≫ f') ≫ Arrow.Hom.right h.i
rw₃ : u ≫ f' ≫ Arrow.Hom.right h.i = (u ≫ f') ≫ Arrow.Hom.right h.i
rw₄ rw₅ : u ≫ f' ≫ Arrow.Hom.right h.i = u ≫ f' ≫ Arrow.Hom.right h.i
⊢ (u ≫ Arrow.Hom.left h.i) ≫ f = g ≫ v ≫ Arrow.Hom.right h.i

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

Premises used: CategoryTheory.Category.assoc, CategoryTheory.RetractArrow.i_w, CategoryTheory.CommSq.w
-- Module: Mathlib.CategoryTheory.LiftingProperties.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
mp : HasLiftingProperty i p → ∀ (φ : mk i ⟶ mk p), Nonempty.{v_1 + 1} (LiftStruct φ)
mpr : (∀ (φ : mk i ⟶ mk p), Nonempty.{v_1 + 1} (LiftStruct φ)) → HasLiftingProperty i p
⊢ HasLiftingProperty i p ↔ ∀ (φ : mk i ⟶ mk p), Nonempty.{v_1 + 1} (LiftStruct φ)

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.LiftingProperties.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
h : HasLiftingProperty i p
φ : mk i ⟶ mk p
⊢ CommSq (Hom.left φ) i p (Hom.right φ)

Tactic:
have sq : CommSq φ.left i p φ.right := CommSq.mk φ.w
-- Module: Mathlib.CategoryTheory.LiftingProperties.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
h : HasLiftingProperty i p
φ : mk i ⟶ mk p
sq : CommSq (Hom.left φ) i p (Hom.right φ)
⊢ Nonempty.{v_1 + 1} (LiftStruct φ)

Tactic:
⟨{ l := sq.lift }⟩

Premises used: CategoryTheory.CommSq.lift, Nonempty.intro, CategoryTheory.CommSq.LiftStruct.mk
-- Module: Mathlib.CategoryTheory.LiftingProperties.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
h : HasLiftingProperty i p
φ : mk i ⟶ mk p
sq : CommSq (Hom.left φ) i p (Hom.right φ)
⊢ Nonempty.{v_1 + 1} (LiftStruct φ)

Tactic:
exact ⟨{ l := sq.lift }⟩
-- Module: Mathlib.CategoryTheory.LiftingProperties.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
h : ∀ (φ : mk i ⟶ mk p), Nonempty.{v_1 + 1} (LiftStruct φ)
⊢ HasLiftingProperty i p

Tactic:
⟨fun {f g} sq ↦ ⟨h (Arrow.homMk f g sq.w)⟩⟩

Premises used: CategoryTheory.HasLiftingProperty.mk, CategoryTheory.CommSq.HasLift.mk, CategoryTheory.CommSq.w, CategoryTheory.Arrow.homMk
-- Module: Mathlib.CategoryTheory.LiftingProperties.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
h : ∀ (φ : mk i ⟶ mk p), Nonempty.{v_1 + 1} (LiftStruct φ)
⊢ HasLiftingProperty i p

Tactic:
exact ⟨fun {f g} sq ↦ ⟨h (Arrow.homMk f g sq.w)⟩⟩
-- 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
h : IsPushout s f g t
Z' W' : C
g' : Z' ⟶ W'
inst_1 : HasLiftingProperty f g'
u : Z ⟶ Z'
v : W ⟶ W'
sq : CommSq u g g' v
rw : (s ≫ u) ≫ g' = (f ≫ t) ≫ v
rw₁ : (s ≫ u) ≫ g' = (s ≫ g) ≫ v
rw₂ : s ≫ u ≫ g' = (s ≫ g) ≫ v
rw₃ : s ≫ u ≫ g' = s ≫ g ≫ v
rw₄ rw₅ : s ≫ g ≫ v = s ≫ g ≫ v
⊢ (s ≫ u) ≫ g' = f ≫ t ≫ v

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

Premises used: CategoryTheory.Category.assoc, CategoryTheory.IsPushout.toCommSq, CategoryTheory.CommSq.w
-- 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
h : IsPushout s f g t
Z' W' : C
g' : Z' ⟶ W'
inst_1 : HasLiftingProperty f g'
u : Z ⟶ Z'
v : W ⟶ W'
sq : CommSq u g g' v
⊢ (s ≫ u) ≫ g' = f ≫ t ≫ v

Tactic:
have w : (s ≫ u) ≫ g' = f ≫ (t ≫ v) := by
      rw [← Category.assoc, ← h.w, Category.assoc, Category.assoc, sq.w]
-- 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
h : IsPushout s f g t
Z' W' : C
g' : Z' ⟶ W'
inst_1 : HasLiftingProperty f g'
u : Z ⟶ Z'
v : W ⟶ W'
sq : CommSq u g g' v
w : (s ≫ u) ≫ g' = f ≫ t ≫ v
rw rw₁ : s ≫ u = s ≫ u
⊢ s ≫ u = f ≫ ⋯.lift

Tactic:
rw [CommSq.fac_left]

Premises used: CategoryTheory.CommSq.fac_left
-- 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
h : IsPushout s f g t
Z' W' : C
g' : Z' ⟶ W'
inst_1 : HasLiftingProperty f g'
u : Z ⟶ Z'
v : W ⟶ W'
sq : CommSq u g g' v
w : (s ≫ u) ≫ g' = f ≫ t ≫ v
rw : u ≫ g' = g ≫ v
rw₁ rw₂ : g ≫ v = g ≫ v
⊢ g ≫ h.desc u ⋯.lift ⋯ ≫ g' = g ≫ v

Tactic:
rw [h.inl_desc_assoc, sq.w]

Premises used: CategoryTheory.IsPushout.inl_desc_assoc, CategoryTheory.CommSq.w
-- 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
h : IsPushout s f g t
Z' W' : C
g' : Z' ⟶ W'
inst_1 : HasLiftingProperty f g'
u : Z ⟶ Z'
v : W ⟶ W'
sq : CommSq u g g' v
w : (s ≫ u) ≫ g' = f ≫ t ≫ v
rw : ⋯.lift ≫ g' = t ≫ v
rw₁ rw₂ : t ≫ v = t ≫ v
⊢ t ≫ h.desc u ⋯.lift ⋯ ≫ g' = t ≫ v

Tactic:
rw [h.inr_desc_assoc, CommSq.fac_right]

Premises used: CategoryTheory.CommSq.fac_right, CategoryTheory.IsPushout.inr_desc_assoc
-- 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
h : IsPushout s f g t
Z' W' : C
g' : Z' ⟶ W'
inst_1 : HasLiftingProperty f g'
u : Z ⟶ Z'
v : W ⟶ W'
sq : CommSq u g g' v
w : (s ≫ u) ≫ g' = f ≫ t ≫ v
⊢ sq.HasLift

Tactic:
exact ⟨h.desc u (CommSq.mk w).lift (by rw [CommSq.fac_left]), h.inl_desc ..,
      h.hom_ext (by rw [h.inl_desc_assoc, sq.w]) (by rw [h.inr_desc_assoc, CommSq.fac_right])⟩
-- 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
h : IsPullback s f g t
X' Y' : C
f' : X' ⟶ Y'
inst_1 : HasLiftingProperty f' g
u : X' ⟶ X
v : Y' ⟶ Y
sq : CommSq u f' f v
rw : u ≫ s ≫ g = f' ≫ v ≫ t
rw₁ : u ≫ f ≫ t = f' ≫ v ≫ t
rw₂ : (u ≫ f) ≫ t = f' ≫ v ≫ t
rw₃ : (u ≫ f) ≫ t = (f' ≫ v) ≫ t
rw₄ rw₅ : (f' ≫ v) ≫ t = (f' ≫ v) ≫ t
⊢ (u ≫ s) ≫ g = f' ≫ v ≫ t

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

Premises used: CategoryTheory.Category.assoc, CategoryTheory.IsPullback.toCommSq, CategoryTheory.CommSq.w
-- 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
h : IsPullback s f g t
X' Y' : C
f' : X' ⟶ Y'
inst_1 : HasLiftingProperty f' g
u : X' ⟶ X
v : Y' ⟶ Y
sq : CommSq u f' f v
⊢ (u ≫ s) ≫ g = f' ≫ v ≫ t

Tactic:
have w : (u ≫ s) ≫ g = f' ≫ v ≫ t := by
      rw [Category.assoc, h.toCommSq.w, ← Category.assoc, ← Category.assoc, sq.w]
-- 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
h : IsPullback s f g t
X' Y' : C
f' : X' ⟶ Y'
inst_1 : HasLiftingProperty f' g
u : X' ⟶ X
v : Y' ⟶ Y
sq : CommSq u f' f v
w : (u ≫ s) ≫ g = f' ≫ v ≫ t
rw rw₁ : v ≫ t = v ≫ t
⊢ ⋯.lift ≫ g = v ≫ t

Tactic:
rw [CommSq.fac_right]

Premises used: CategoryTheory.CommSq.fac_right
-- 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
h : IsPullback s f g t
X' Y' : C
f' : X' ⟶ Y'
inst_1 : HasLiftingProperty f' g
u : X' ⟶ X
v : Y' ⟶ Y
sq : CommSq u f' f v
w : (u ≫ s) ≫ g = f' ≫ v ≫ t
rw : f' ≫ h.lift ⋯.lift v ⋯ ≫ s = u ≫ s
rw₁ : f' ≫ ⋯.lift = u ≫ s
rw₂ rw₃ : u ≫ s = u ≫ s
⊢ (f' ≫ h.lift ⋯.lift v ⋯) ≫ s = u ≫ s

Tactic:
rw [Category.assoc, h.lift_fst, CommSq.fac_left]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.IsPullback.lift_fst, CategoryTheory.CommSq.fac_left
-- 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
h : IsPullback s f g t
X' Y' : C
f' : X' ⟶ Y'
inst_1 : HasLiftingProperty f' g
u : X' ⟶ X
v : Y' ⟶ Y
sq : CommSq u f' f v
w : (u ≫ s) ≫ g = f' ≫ v ≫ t
rw : f' ≫ h.lift ⋯.lift v ⋯ ≫ f = u ≫ f
rw₁ : f' ≫ v = u ≫ f
rw₂ rw₃ : f' ≫ v = f' ≫ v
⊢ (f' ≫ h.lift ⋯.lift v ⋯) ≫ f = u ≫ f

Tactic:
rw [Category.assoc, h.lift_snd, sq.w]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.IsPullback.lift_snd, CategoryTheory.CommSq.w
-- 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
h : IsPullback s f g t
X' Y' : C
f' : X' ⟶ Y'
inst_1 : HasLiftingProperty f' g
u : X' ⟶ X
v : Y' ⟶ Y
sq : CommSq u f' f v
w : (u ≫ s) ≫ g = f' ≫ v ≫ t
⊢ sq.HasLift

Tactic:
exact ⟨h.lift (CommSq.mk w).lift v (by rw [CommSq.fac_right]),
      h.hom_ext (by rw [Category.assoc, h.lift_fst, CommSq.fac_left])
        (by rw [Category.assoc, h.lift_snd, sq.w]), h.lift_snd _ _ _⟩