awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.MorphismProperty.Concrete
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst_1 : (X Y : C) → FunLike.{u_1 + 1, u_2 + 1, u_2 + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{u_2, v, u, u_1} C FC (CC := CC)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : MorphismProperty.injective C (FC := FC) (CC := CC) f
hg : MorphismProperty.injective C (FC := FC) (CC := CC) g
⊢ Injective.{u_2 + 1, u_2 + 1} (α := CC X) (β := CC Z)
    (Function.comp (β := CC Y) (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) g) : (a : CC Y) → CC Z)
      (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) f) : (a : CC X) → CC Y))

Tactic:
hg.comp hf

Premises used: Function.Injective.comp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Concrete
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst_1 : (X Y : C) → FunLike.{u_1 + 1, u_2 + 1, u_2 + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{u_2, v, u, u_1} C FC (CC := CC)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : MorphismProperty.injective C (FC := FC) (CC := CC) f
hg : MorphismProperty.injective C (FC := FC) (CC := CC) g
⊢ Injective.{u_2 + 1, u_2 + 1} (α := CC X) (β := CC Z)
    (Function.comp (β := CC Y) (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) g) : (a : CC Y) → CC Z)
      (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) f) : (a : CC X) → CC Y))

Tactic:
exact hg.comp hf

Premises used: Function.Injective.comp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Concrete
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst_1 : (X Y : C) → FunLike.{u_1 + 1, u_2 + 1, u_2 + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{u_2, v, u, u_1} C FC (CC := CC)
X : C
⊢ Surjective.{u_2 + 1, u_2 + 1} (α := CC X) id

Tactic:
surjective_id

Premises used: Function.surjective_id
-- Module: Mathlib.CategoryTheory.MorphismProperty.Concrete
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst_1 : (X Y : C) → FunLike.{u_1 + 1, u_2 + 1, u_2 + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{u_2, v, u, u_1} C FC (CC := CC)
X : C
h :
  Eq.{u_2 + 1} (α := CC X → CC X)
    (⇑(@ConcreteCategory.hom.{u_2, v, u, u_1} _ inst FC CC _ _ _ _ (𝟙 X)) : (a : CC X) → CC X) id
⊢ Surjective.{u_2 + 1, u_2 + 1} (α := CC X) (β := CC X)
    (⇑(@ConcreteCategory.hom.{u_2, v, u, u_1} _ inst FC CC _ _ _ _ (𝟙 X)) : (a : CC X) → CC X)

Tactic:
convert! surjective_id

Premises used: Function.surjective_id
-- Module: Mathlib.CategoryTheory.MorphismProperty.Concrete
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst_1 : (X Y : C) → FunLike.{u_1 + 1, u_2 + 1, u_2 + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{u_2, v, u, u_1} C FC (CC := CC)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : MorphismProperty.surjective C (FC := FC) (CC := CC) f
hg : MorphismProperty.surjective C (FC := FC) (CC := CC) g
rw :
  Surjective.{u_2 + 1, u_2 + 1} (α := CC X) (β := CC Z)
    (Function.comp (β := CC Y) (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) g) : (a : CC Y) → CC Z)
      (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) f) : (a : CC X) → CC Y))
⊢ Surjective.{u_2 + 1, u_2 + 1} (α := CC X) (β := CC Z)
    (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (f ≫ g)) : (a : CC X) → CC Z)

Tactic:
rw [hom_comp]

Premises used: CategoryTheory.hom_comp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Concrete
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst_1 : (X Y : C) → FunLike.{u_1 + 1, u_2 + 1, u_2 + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{u_2, v, u, u_1} C FC (CC := CC)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : MorphismProperty.surjective C (FC := FC) (CC := CC) f
hg : MorphismProperty.surjective C (FC := FC) (CC := CC) g
⊢ Surjective.{u_2 + 1, u_2 + 1} (α := CC X) (β := CC Z)
    (Function.comp (β := CC Y) (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) g) : (a : CC Y) → CC Z)
      (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) f) : (a : CC X) → CC Y))

Tactic:
hg.comp hf

Premises used: Function.Surjective.comp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Concrete
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst_1 : (X Y : C) → FunLike.{u_1 + 1, u_2 + 1, u_2 + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{u_2, v, u, u_1} C FC (CC := CC)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : MorphismProperty.surjective C (FC := FC) (CC := CC) f
hg : MorphismProperty.surjective C (FC := FC) (CC := CC) g
⊢ Surjective.{u_2 + 1, u_2 + 1} (α := CC X) (β := CC Z)
    (Function.comp (β := CC Y) (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) g) : (a : CC Y) → CC Z)
      (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) f) : (a : CC X) → CC Y))

Tactic:
exact hg.comp hf

Premises used: Function.Surjective.comp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Concrete
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst_1 : (X Y : C) → FunLike.{u_1 + 1, u_2 + 1, u_2 + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{u_2, v, u, u_1} C FC (CC := CC)
X : C
⊢ Bijective.{u_2 + 1, u_2 + 1} (α := CC X) id

Tactic:
bijective_id

Premises used: Function.bijective_id
-- Module: Mathlib.CategoryTheory.MorphismProperty.Concrete
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst_1 : (X Y : C) → FunLike.{u_1 + 1, u_2 + 1, u_2 + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{u_2, v, u, u_1} C FC (CC := CC)
X : C
h :
  Eq.{u_2 + 1} (α := CC X → CC X)
    (⇑(@ConcreteCategory.hom.{u_2, v, u, u_1} _ inst FC CC _ _ _ _ (𝟙 X)) : (a : CC X) → CC X) id
⊢ Bijective.{u_2 + 1, u_2 + 1} (α := CC X) (β := CC X)
    (⇑(@ConcreteCategory.hom.{u_2, v, u, u_1} _ inst FC CC _ _ _ _ (𝟙 X)) : (a : CC X) → CC X)

Tactic:
convert! bijective_id

Premises used: Function.bijective_id
-- Module: Mathlib.CategoryTheory.MorphismProperty.Concrete
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst_1 : (X Y : C) → FunLike.{u_1 + 1, u_2 + 1, u_2 + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{u_2, v, u, u_1} C FC (CC := CC)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : MorphismProperty.bijective C (FC := FC) (CC := CC) f
hg : MorphismProperty.bijective C (FC := FC) (CC := CC) g
rw :
  Bijective.{u_2 + 1, u_2 + 1} (α := CC X) (β := CC Z)
    (Function.comp (β := CC Y) (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) g) : (a : CC Y) → CC Z)
      (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) f) : (a : CC X) → CC Y))
⊢ Bijective.{u_2 + 1, u_2 + 1} (α := CC X) (β := CC Z)
    (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (f ≫ g)) : (a : CC X) → CC Z)

Tactic:
rw [hom_comp]

Premises used: CategoryTheory.hom_comp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Concrete
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst_1 : (X Y : C) → FunLike.{u_1 + 1, u_2 + 1, u_2 + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{u_2, v, u, u_1} C FC (CC := CC)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : MorphismProperty.bijective C (FC := FC) (CC := CC) f
hg : MorphismProperty.bijective C (FC := FC) (CC := CC) g
⊢ Bijective.{u_2 + 1, u_2 + 1} (α := CC X) (β := CC Z)
    (Function.comp (β := CC Y) (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) g) : (a : CC Y) → CC Z)
      (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) f) : (a : CC X) → CC Y))

Tactic:
hg.comp hf

Premises used: Function.Bijective.comp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Concrete
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst_1 : (X Y : C) → FunLike.{u_1 + 1, u_2 + 1, u_2 + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{u_2, v, u, u_1} C FC (CC := CC)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : MorphismProperty.bijective C (FC := FC) (CC := CC) f
hg : MorphismProperty.bijective C (FC := FC) (CC := CC) g
⊢ Bijective.{u_2 + 1, u_2 + 1} (α := CC X) (β := CC Z)
    (Function.comp (β := CC Y) (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) g) : (a : CC Y) → CC Z)
      (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) f) : (a : CC X) → CC Y))

Tactic:
exact hg.comp hf

Premises used: Function.Bijective.comp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Concrete
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst_1 : (X Y : C) → FunLike.{u_1 + 1, u_2 + 1, u_2 + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{u_2, v, u, u_1} C FC (CC := CC)
⊢ RespectsIso.{v, u} (MorphismProperty.injective C (FC := FC) (CC := CC))

Tactic:
respectsIso_of_isStableUnderComposition
    (fun _ _ f (_ : IsIso f) => ((forget C).mapIso (asIso f)).toEquiv.injective)

Premises used: CategoryTheory.Iso.toEquiv, CategoryTheory.forget, CategoryTheory.MorphismProperty.respectsIso_of_isStableUnderComposition, Equiv.injective, CategoryTheory.Functor.mapIso, CategoryTheory.asIso
-- Module: Mathlib.CategoryTheory.MorphismProperty.Concrete
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst_1 : (X Y : C) → FunLike.{u_1 + 1, u_2 + 1, u_2 + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{u_2, v, u, u_1} C FC (CC := CC)
⊢ RespectsIso.{v, u} (MorphismProperty.surjective C (FC := FC) (CC := CC))

Tactic:
respectsIso_of_isStableUnderComposition
    (fun _ _ f (_ : IsIso f) => ((forget C).mapIso (asIso f)).toEquiv.surjective)

Premises used: CategoryTheory.Iso.toEquiv, CategoryTheory.forget, CategoryTheory.MorphismProperty.respectsIso_of_isStableUnderComposition, Equiv.surjective, CategoryTheory.Functor.mapIso, CategoryTheory.asIso
-- Module: Mathlib.CategoryTheory.MorphismProperty.Concrete
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst_1 : (X Y : C) → FunLike.{u_1 + 1, u_2 + 1, u_2 + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{u_2, v, u, u_1} C FC (CC := CC)
⊢ RespectsIso.{v, u} (MorphismProperty.bijective C (FC := FC) (CC := CC))

Tactic:
respectsIso_of_isStableUnderComposition
    (fun _ _ f (_ : IsIso f) => ((forget C).mapIso (asIso f)).toEquiv.bijective)

Premises used: Equiv.bijective, CategoryTheory.Iso.toEquiv, CategoryTheory.forget, CategoryTheory.MorphismProperty.respectsIso_of_isStableUnderComposition, CategoryTheory.Functor.mapIso, CategoryTheory.asIso
-- Module: Mathlib.CategoryTheory.MorphismProperty.Concrete
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst_1 : (X Y : C) → FunLike.{u_1 + 1, u_2 + 1, u_2 + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{u_2, v, u, u_1} C FC (CC := CC)
X Y : Arrow (Type u)
φ : X ⟶ Y
y : Subtype (α := X.right) (Set.range (ι := X.left) (⇑(TypeCat.Hom.hom X.hom) : (a : X.left) → X.right))
obtain :
  ∀ (x : X.left),
    Set.range (α := Y.right) (ι := Y.left)
      ((⇑(TypeCat.Hom.hom Y.hom) : (a : Y.left) → Y.right) : (a : Y.left) → Y.right)
      ((hom (FC := TypeCat.Fun) (Arrow.Hom.right φ) :
            (a : (fun (X : Type u) ↦ X) X.right) → (fun (X : Type u) ↦ X) Y.right)
          ((↑(Subtype.mk (p := Set.range (ι := X.left) (⇑(TypeCat.Hom.hom X.hom) : (a : X.left) → X.right))
                  ((TypeCat.Hom.hom X.hom : (a : X.left) → X.right) x) ⋯) :
              X.right) :
            X.right) :
        (fun (X : Type u) ↦ X) Y.right)
⊢ Set.range (α := Y.right) (ι := Y.left) ((⇑(TypeCat.Hom.hom Y.hom) : (a : Y.left) → Y.right) : (a : Y.left) → Y.right)
    ((hom (FC := TypeCat.Fun) (Arrow.Hom.right φ) :
          (a : (fun (X : Type u) ↦ X) X.right) → (fun (X : Type u) ↦ X) Y.right)
        (↑y : X.right) :
      (fun (X : Type u) ↦ X) Y.right)

Tactic:
obtain ⟨_, x, rfl⟩ := y

Premises used: rfl
-- Module: Mathlib.CategoryTheory.MorphismProperty.Concrete
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst_1 : (X Y : C) → FunLike.{u_1 + 1, u_2 + 1, u_2 + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{u_2, v, u, u_1} C FC (CC := CC)
X Y : Arrow (Type u)
φ : X ⟶ Y
x : X.left
⊢ Set.range (α := Y.right) (ι := Y.left) ((⇑(TypeCat.Hom.hom Y.hom) : (a : Y.left) → Y.right) : (a : Y.left) → Y.right)
    ((hom (FC := TypeCat.Fun) (Arrow.Hom.right φ) :
          (a : (fun (X : Type u) ↦ X) X.right) → (fun (X : Type u) ↦ X) Y.right)
        ((↑(Subtype.mk (p := Set.range (ι := X.left) (⇑(TypeCat.Hom.hom X.hom) : (a : X.left) → X.right))
                ((TypeCat.Hom.hom X.hom : (a : X.left) → X.right) x) ⋯) :
            X.right) :
          X.right) :
      (fun (X : Type u) ↦ X) Y.right)

Tactic:
⟨φ.left x, congr_hom φ.w x⟩

Premises used: CategoryTheory.ConcreteCategory.hom, setOf, Exists.intro, CategoryTheory.Arrow.Hom.left, Set.range, DFunLike.coe
-- Module: Mathlib.CategoryTheory.MorphismProperty.Concrete
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst_1 : (X Y : C) → FunLike.{u_1 + 1, u_2 + 1, u_2 + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{u_2, v, u, u_1} C FC (CC := CC)
X Y : Arrow (Type u)
φ : X ⟶ Y
x : X.left
⊢ Set.range (α := Y.right) (ι := Y.left) ((⇑(TypeCat.Hom.hom Y.hom) : (a : Y.left) → Y.right) : (a : Y.left) → Y.right)
    ((hom (FC := TypeCat.Fun) (Arrow.Hom.right φ) :
          (a : (fun (X : Type u) ↦ X) X.right) → (fun (X : Type u) ↦ X) Y.right)
        ((↑(Subtype.mk (p := Set.range (ι := X.left) (⇑(TypeCat.Hom.hom X.hom) : (a : X.left) → X.right))
                ((TypeCat.Hom.hom X.hom : (a : X.left) → X.right) x) ⋯) :
            X.right) :
          X.right) :
      (fun (X : Type u) ↦ X) Y.right)

Tactic:
exact ⟨φ.left x, congr_hom φ.w x⟩
-- Module: Mathlib.CategoryTheory.MorphismProperty.Concrete
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst_1 : (X Y : C) → FunLike.{u_1 + 1, u_2 + 1, u_2 + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{u_2, v, u, u_1} C FC (CC := CC)
f g : Arrow (Type u)
φ : f ⟶ g
x : Functor.obj Arrow.leftFunc f
⊢ Eq (α := g.right)
    (↑(TypeCat.Fun.toFun
          (hom (FC := TypeCat.Fun)
            (Functor.map Arrow.leftFunc φ ≫
              ↾fun (x : Functor.obj Arrow.leftFunc g) ↦
                Subtype.mk (p := Set.range (ι := g.left) (⇑(TypeCat.Hom.hom g.hom) : (a : g.left) → g.right))
                  ((hom (FC := TypeCat.Fun) g.hom :
                      (a : (fun (X : Type u) ↦ X) g.left) → (fun (X : Type u) ↦ X) g.right)
                    x)
                  ⋯))
          x) :
      g.right)
    (↑(TypeCat.Fun.toFun
          (hom (FC := TypeCat.Fun)
            ((↾fun (x : Functor.obj Arrow.leftFunc f) ↦
                Subtype.mk (p := Set.range (ι := f.left) (⇑(TypeCat.Hom.hom f.hom) : (a : f.left) → f.right))
                  ((hom (FC := TypeCat.Fun) f.hom :
                      (a : (fun (X : Type u) ↦ X) f.left) → (fun (X : Type u) ↦ X) f.right)
                    x)
                  ⋯) ≫
              Functor.map
                {
                  obj := fun (f : Arrow (Type u)) ↦
                    Subtype (α := f.right)
                      (Set.range (ι := f.left) (⇑(TypeCat.Hom.hom f.hom) : (a : f.left) → f.right)),
                  map := fun {X Y : Arrow (Type u)} (φ : X ⟶ Y) ↦
                    ↾fun
                        (y :
                          Subtype (α := X.right)
                            (Set.range (ι := X.left) (⇑(TypeCat.Hom.hom X.hom) : (a : X.left) → X.right))) ↦
                      Subtype.mk (p := Set.range (ι := Y.left) (⇑(TypeCat.Hom.hom Y.hom) : (a : Y.left) → Y.right))
                        ((hom (FC := TypeCat.Fun) (Arrow.Hom.right φ) :
                            (a : (fun (X : Type u) ↦ X) X.right) → (fun (X : Type u) ↦ X) Y.right)
                          (↑y : X.right))
                        ⋯,
                  map_id := functorialSurjectiveInjectiveFactorizationData._proof_2,
                  map_comp := @functorialSurjectiveInjectiveFactorizationData._proof_3 : Arrow (Type u) ⥤ Type u }
                φ))
          x) :
      g.right)

Tactic:
congr_hom φ.w x

Premises used: CategoryTheory.Arrow.Hom.w, CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.CategoryTheory.MorphismProperty.Concrete
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst_1 : (X Y : C) → FunLike.{u_1 + 1, u_2 + 1, u_2 + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{u_2, v, u, u_1} C FC (CC := CC)
f g : Arrow (Type u)
φ : f ⟶ g
x : Functor.obj Arrow.leftFunc f
⊢ Eq (α := g.right)
    (↑(TypeCat.Fun.toFun
          (hom (FC := TypeCat.Fun)
            (Functor.map Arrow.leftFunc φ ≫
              ↾fun (x : Functor.obj Arrow.leftFunc g) ↦
                Subtype.mk (p := Set.range (ι := g.left) (⇑(TypeCat.Hom.hom g.hom) : (a : g.left) → g.right))
                  ((hom (FC := TypeCat.Fun) g.hom :
                      (a : (fun (X : Type u) ↦ X) g.left) → (fun (X : Type u) ↦ X) g.right)
                    x)
                  ⋯))
          x) :
      g.right)
    (↑(TypeCat.Fun.toFun
          (hom (FC := TypeCat.Fun)
            ((↾fun (x : Functor.obj Arrow.leftFunc f) ↦
                Subtype.mk (p := Set.range (ι := f.left) (⇑(TypeCat.Hom.hom f.hom) : (a : f.left) → f.right))
                  ((hom (FC := TypeCat.Fun) f.hom :
                      (a : (fun (X : Type u) ↦ X) f.left) → (fun (X : Type u) ↦ X) f.right)
                    x)
                  ⋯) ≫
              Functor.map
                {
                  obj := fun (f : Arrow (Type u)) ↦
                    Subtype (α := f.right)
                      (Set.range (ι := f.left) (⇑(TypeCat.Hom.hom f.hom) : (a : f.left) → f.right)),
                  map := fun {X Y : Arrow (Type u)} (φ : X ⟶ Y) ↦
                    ↾fun
                        (y :
                          Subtype (α := X.right)
                            (Set.range (ι := X.left) (⇑(TypeCat.Hom.hom X.hom) : (a : X.left) → X.right))) ↦
                      Subtype.mk (p := Set.range (ι := Y.left) (⇑(TypeCat.Hom.hom Y.hom) : (a : Y.left) → Y.right))
                        ((hom (FC := TypeCat.Fun) (Arrow.Hom.right φ) :
                            (a : (fun (X : Type u) ↦ X) X.right) → (fun (X : Type u) ↦ X) Y.right)
                          (↑y : X.right))
                        ⋯,
                  map_id := functorialSurjectiveInjectiveFactorizationData._proof_2,
                  map_comp := @functorialSurjectiveInjectiveFactorizationData._proof_3 : Arrow (Type u) ⥤ Type u }
                φ))
          x) :
      g.right)

Tactic:
exact congr_hom φ.w x

Premises used: CategoryTheory.Arrow.Hom.w, CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.CategoryTheory.MorphismProperty.Descent
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P Q : MorphismProperty.{v_1, u_1} C
A X Y Z : C
fst : A ⟶ X
snd : A ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
inst_1 : P.DescendsAlong Q
h : IsPullback fst snd f g
hf : Q f
hfst : P fst
⊢ P g

Tactic:
DescendsAlong.of_isPullback h hf hfst

Premises used: CategoryTheory.MorphismProperty.DescendsAlong.of_isPullback
-- Module: Mathlib.CategoryTheory.MorphismProperty.Descent
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P Q : MorphismProperty.{v_1, u_1} C
A X Y Z : C
fst : A ⟶ X
snd : A ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
inst_1 : P.IsStableUnderBaseChange
inst_2 : P.DescendsAlong Q
h : IsPullback fst snd f g
hf : Q f
⊢ P fst ↔ P g

Tactic:
⟨fun hfst ↦ of_isPullback_of_descendsAlong h hf hfst, fun hf ↦ P.of_isPullback h.flip hf⟩

Premises used: CategoryTheory.MorphismProperty.of_isPullback, CategoryTheory.MorphismProperty.of_isPullback_of_descendsAlong, CategoryTheory.IsPullback.flip, Iff.intro
-- Module: Mathlib.CategoryTheory.MorphismProperty.Descent
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P Q : MorphismProperty.{v_1, u_1} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_1 : P.DescendsAlong Q
inst_2 : HasPullback f g
hf : Q f
hfst : P (X := pullback f g) (pullback.fst f g)
⊢ P g

Tactic:
of_isPullback_of_descendsAlong (.of_hasPullback f g) hf hfst

Premises used: CategoryTheory.MorphismProperty.of_isPullback_of_descendsAlong, CategoryTheory.IsPullback.of_hasPullback
-- Module: Mathlib.CategoryTheory.MorphismProperty.Descent
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P Q : MorphismProperty.{v_1, u_1} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_1 : P.IsStableUnderBaseChange
inst_2 : P.DescendsAlong Q
inst_3 : HasPullback f g
hf : Q f
⊢ P (X := pullback f g) (pullback.fst f g) ↔ P g

Tactic:
iff_of_isPullback (.of_hasPullback f g) hf

Premises used: CategoryTheory.MorphismProperty.iff_of_isPullback, CategoryTheory.IsPullback.of_hasPullback
-- Module: Mathlib.CategoryTheory.MorphismProperty.Descent
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P Q : MorphismProperty.{v_1, u_1} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_1 : P.DescendsAlong Q
inst_2 : HasPullback f g
hg : Q g
hsnd : P (X := pullback f g) (pullback.snd f g)
⊢ P f

Tactic:
of_isPullback_of_descendsAlong (IsPullback.of_hasPullback f g).flip hg hsnd

Premises used: CategoryTheory.MorphismProperty.of_isPullback_of_descendsAlong, CategoryTheory.IsPullback.flip, CategoryTheory.IsPullback.of_hasPullback
-- Module: Mathlib.CategoryTheory.MorphismProperty.Descent
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P Q : MorphismProperty.{v_1, u_1} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_1 : P.IsStableUnderBaseChange
inst_2 : P.DescendsAlong Q
inst_3 : HasPullback f g
hg : Q g
⊢ P (X := pullback f g) (pullback.snd f g) ↔ P f

Tactic:
iff_of_isPullback (IsPullback.of_hasPullback f g).flip hg

Premises used: CategoryTheory.MorphismProperty.iff_of_isPullback, CategoryTheory.IsPullback.flip, CategoryTheory.IsPullback.of_hasPullback
-- Module: Mathlib.CategoryTheory.MorphismProperty.Descent
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P Q : MorphismProperty.{v_1, u_1} C
inst_1 : P.RespectsIso
H :
  ∀ {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} [inst_2 : HasPullback f g], Q f → P (X := pullback f g) (pullback.fst f g) → P g
A X Y Z : C
fst : A ⟶ X
snd : A ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
hf : Q f
hfst : P fst
have : ∀ (this : HasPullback f g), P g
⊢ P g

Tactic:
have : HasPullback f g := h.hasPullback
-- Module: Mathlib.CategoryTheory.MorphismProperty.Descent
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P Q : MorphismProperty.{v_1, u_1} C
inst_1 : P.RespectsIso
H :
  ∀ {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} [inst_2 : HasPullback f g], Q f → P (X := pullback f g) (pullback.fst f g) → P g
A X Y Z : C
fst : A ⟶ X
snd : A ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
hf : Q f
hfst : P fst
this : HasPullback f g
apply : P (X := pullback f g) (pullback.fst f g)
⊢ P g

Tactic:
apply H hf
-- Module: Mathlib.CategoryTheory.MorphismProperty.Descent
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P Q : MorphismProperty.{v_1, u_1} C
inst_1 : P.RespectsIso
H :
  ∀ {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} [inst_2 : HasPullback f g], Q f → P (X := pullback f g) (pullback.fst f g) → P g
A X Y Z : C
fst : A ⟶ X
snd : A ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
hf : Q f
hfst : P fst
this : HasPullback f g
rwa : P (CategoryStruct.comp (Y := pullback f g) (Iso.hom h.isoPullback) (pullback.fst f g))
rwa₁ rwa₂ rwa₃ rwa₄ : P fst
⊢ P (X := pullback f g) (pullback.fst f g)

Tactic:
rwa [← P.cancel_left_of_respectsIso h.isoPullback.hom, h.isoPullback_hom_fst]

Premises used: CategoryTheory.IsPullback.isoPullback, CategoryTheory.IsPullback.isoPullback_hom_fst, CategoryTheory.MorphismProperty.cancel_left_of_respectsIso, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.MorphismProperty.Descent
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P Q W : MorphismProperty.{v_1, u_1} C
A_1 X_1 Y_1 Z_1 : C
fst_1 : A_1 ⟶ X_1
snd_1 : A_1 ⟶ Y_1
f_1 : X_1 ⟶ Z_1
g_1 : Y_1 ⟶ Z_1
inst_1 : Q.IsStableUnderBaseChange
inst_2 : P.HasOfPrecompProperty Q
inst_3 : P.RespectsRight Q
A X Y Z : C
fst : A ⟶ X
snd : A ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
hf : Q f
hfst : P fst
apply : P (snd ≫ g)
⊢ P g

Tactic:
apply P.of_precomp (W' := Q) _ _ (Q.of_isPullback h hf)

Premises used: CategoryTheory.MorphismProperty.of_isPullback, CategoryTheory.MorphismProperty.of_precomp