awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Composition (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W W' : MorphismProperty.{v, u} C
inst_1 : W'.IsMultiplicative
h : W ≤ W'
X Y : C
f : X ⟶ Y
hf : W.multiplicativeClosure f
⊢ W' f
have of : ∀ {x y : C} (f : x ⟶ y) (hf : W f), W' f
Tactic: induction hf with
    | of _ hf => exact h _ hf
    | id x => exact W'.id_mem _
    | comp_of _ _ _ hg hf => exact W'.comp_mem _ _ hf (h _ hg)
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Composition (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W W' : MorphismProperty.{v, u} C
inst_1 : W'.IsMultiplicative
h : W ≤ W'
X Y : C
f : X ⟶ Y
hf : W.multiplicativeClosure f
of : ∀ {x y : C} (f : x ⟶ y) (hf : W f), W' f
⊢ W' f
have id : ∀ (x : C), W' (𝟙 x)
Tactic: induction hf with
    | of _ hf => exact h _ hf
    | id x => exact W'.id_mem _
    | comp_of _ _ _ hg hf => exact W'.comp_mem _ _ hf (h _ hg)
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Composition (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W W' : MorphismProperty.{v, u} C
inst_1 : W'.IsMultiplicative
h : W ≤ W'
X Y : C
f : X ⟶ Y
hf : W.multiplicativeClosure f
of : ∀ {x y : C} (f : x ⟶ y) (hf : W f), W' f
id : ∀ (x : C), W' (𝟙 x)
⊢ W' f
have comp_of : ∀ {x y z : C} (f : x ⟶ y) (g : y ⟶ z), W.multiplicativeClosure f → ∀ (hg : W g) (hf : W' f), W' (f ≫ g)
Tactic: induction hf with
    | of _ hf => exact h _ hf
    | id x => exact W'.id_mem _
    | comp_of _ _ _ hg hf => exact W'.comp_mem _ _ hf (h _ hg)
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Composition (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
x y : C
f : x ⟶ y
hf : W.multiplicativeClosure' f
⊢ W.multiplicativeClosure f
have of : ∀ {x y : C} (f : x ⟶ y) (h : W f), W.multiplicativeClosure f
Tactic: induction hf with
      | of _ h => exact .of _ h
      | id x => exact .id x
      | of_comp f g hf hg hr => exact W.multiplicativeClosure.comp_mem f g (.of f hf) hr
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Composition (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
x y : C
f : x ⟶ y
hf : W.multiplicativeClosure' f
of : ∀ {x y : C} (f : x ⟶ y) (h : W f), W.multiplicativeClosure f
⊢ W.multiplicativeClosure f
have id : ∀ (x : C), W.multiplicativeClosure (𝟙 x)
Tactic: induction hf with
      | of _ h => exact .of _ h
      | id x => exact .id x
      | of_comp f g hf hg hr => exact W.multiplicativeClosure.comp_mem f g (.of f hf) hr
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Composition (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
x y : C
f : x ⟶ y
hf : W.multiplicativeClosure' f
of : ∀ {x y : C} (f : x ⟶ y) (h : W f), W.multiplicativeClosure f
id : ∀ (x : C), W.multiplicativeClosure (𝟙 x)
⊢ W.multiplicativeClosure f
have of_comp : ∀ {x y z : C} (f : x ⟶ y) (g : y ⟶ z) (hf : W f) (hg : W.multiplicativeClosure' g) (hr : W.multiplicativeClosure g),
  W.multiplicativeClosure (f ≫ g)
Tactic: induction hf with
      | of _ h => exact .of _ h
      | id x => exact .id x
      | of_comp f g hf hg hr => exact W.multiplicativeClosure.comp_mem f g (.of f hf) hr
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Composition (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
W : MorphismProperty.{v, u} C
F : Functor.{v, v', u, u'} C D
X Y : D
f : X ⟶ Y
hf : W.multiplicativeClosure.strictMap F f
⊢ (W.strictMap F).multiplicativeClosure f
have map : ∀ {X Y : C} {f : X ⟶ Y} (hf : W.multiplicativeClosure f), (W.strictMap F).multiplicativeClosure (F.map f)
Tactic: induction hf with | map hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Composition (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
W : MorphismProperty.{v, u} C
F : Functor.{v, v', u, u'} C D
X Y : D
f : X ⟶ Y
X_1 Y_1 : C
f_1 : X_1 ⟶ Y_1
hf : W.multiplicativeClosure f_1
⊢ (W.strictMap F).multiplicativeClosure (F.map f_1)
have map : ∀ {x y : C} (f : x ⟶ y) (hf : W f), (W.strictMap F).multiplicativeClosure (F.map f)
Tactic: induction hf with
  | of f hf => exact le_multiplicativeClosure _ _ ⟨hf⟩
  | id x => simpa using .id (F.obj x)
  | comp_of _ _ hf hg h =>
    simpa using multiplicativeClosure.comp_of _ _ h (strictMap.map hg)
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Composition (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
W : MorphismProperty.{v, u} C
F : Functor.{v, v', u, u'} C D
X Y : D
f : X ⟶ Y
X_1 Y_1 : C
f_1 : X_1 ⟶ Y_1
hf : W.multiplicativeClosure f_1
map : ∀ {x y : C} (f : x ⟶ y) (hf : W f), (W.strictMap F).multiplicativeClosure (F.map f)
⊢ (W.strictMap F).multiplicativeClosure (F.map f_1)
have map₁ : ∀ (x : C), (W.strictMap F).multiplicativeClosure (F.map (𝟙 x))
Tactic: induction hf with
  | of f hf => exact le_multiplicativeClosure _ _ ⟨hf⟩
  | id x => simpa using .id (F.obj x)
  | comp_of _ _ hf hg h =>
    simpa using multiplicativeClosure.comp_of _ _ h (strictMap.map hg)
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Composition (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
W : MorphismProperty.{v, u} C
F : Functor.{v, v', u, u'} C D
X Y : D
f : X ⟶ Y
X_1 Y_1 : C
f_1 : X_1 ⟶ Y_1
hf : W.multiplicativeClosure f_1
map : ∀ {x y : C} (f : x ⟶ y) (hf : W f), (W.strictMap F).multiplicativeClosure (F.map f)
map₁ : ∀ (x : C), (W.strictMap F).multiplicativeClosure (F.map (𝟙 x))
⊢ (W.strictMap F).multiplicativeClosure (F.map f_1)
have map₂ : ∀ {x y z : C} (f : x ⟶ y) (g : y ⟶ z) (hf : W.multiplicativeClosure f) (hg : W g)
  (h : (W.strictMap F).multiplicativeClosure (F.map f)), (W.strictMap F).multiplicativeClosure (F.map (f ≫ g))
Tactic: induction hf with
  | of f hf => exact le_multiplicativeClosure _ _ ⟨hf⟩
  | id x => simpa using .id (F.obj x)
  | comp_of _ _ hf hg h =>
    simpa using multiplicativeClosure.comp_of _ _ h (strictMap.map hg)
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Composition (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
W_1 W W'_1 : MorphismProperty.{v, u} C
W' : ?m.4
P Q : MorphismProperty.{v, u} C
inst_2 : P.HasTwoOutOfThreeProperty
inst_3 : Q.HasTwoOutOfThreeProperty
⊢ (P ⊓ Q).HasTwoOutOfThreeProperty
have this : P.HasOfPostcompProperty (P ⊓ Q)
Tactic: have : P.HasOfPostcompProperty (P ⊓ Q) := .of_le _ _ inf_le_left
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Composition (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
W_1 W W'_1 : MorphismProperty.{v, u} C
W' : ?m.4
P Q : MorphismProperty.{v, u} C
inst_2 : P.HasTwoOutOfThreeProperty
inst_3 : Q.HasTwoOutOfThreeProperty
this : P.HasOfPostcompProperty (P ⊓ Q)
⊢ (P ⊓ Q).HasTwoOutOfThreeProperty
have this₁ : P.HasOfPrecompProperty (P ⊓ Q)
Tactic: have : P.HasOfPrecompProperty (P ⊓ Q) := .of_le _ _ inf_le_left
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Composition (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
W_1 W W'_1 : MorphismProperty.{v, u} C
W' : ?m.4
P Q : MorphismProperty.{v, u} C
inst_2 : P.HasTwoOutOfThreeProperty
inst_3 : Q.HasTwoOutOfThreeProperty
this_1 : P.HasOfPostcompProperty (P ⊓ Q)
this : P.HasOfPrecompProperty (P ⊓ Q)
⊢ (P ⊓ Q).HasTwoOutOfThreeProperty
have this₁ : Q.HasOfPostcompProperty (P ⊓ Q)
Tactic: have : Q.HasOfPostcompProperty (P ⊓ Q) := .of_le _ _ inf_le_right
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Composition (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
W_1 W W'_1 : MorphismProperty.{v, u} C
W' : ?m.4
P Q : MorphismProperty.{v, u} C
inst_2 : P.HasTwoOutOfThreeProperty
inst_3 : Q.HasTwoOutOfThreeProperty
this_1 : P.HasOfPostcompProperty (P ⊓ Q)
this_2 : P.HasOfPrecompProperty (P ⊓ Q)
this : Q.HasOfPostcompProperty (P ⊓ Q)
⊢ (P ⊓ Q).HasTwoOutOfThreeProperty
have this₁ : Q.HasOfPrecompProperty (P ⊓ Q)
Tactic: have : Q.HasOfPrecompProperty (P ⊓ Q) := .of_le _ _ inf_le_right
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Concrete (goal)
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
⊢ Injective.{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)
have 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
Tactic: convert! injective_id
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Concrete (goal)
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)
    (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (f ≫ g)) : (a : CC X) → CC Z)
have rw : 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: rw [hom_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Concrete (goal)
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) (β := CC X)
    (⇑(@ConcreteCategory.hom.{u_2, v, u, u_1} _ inst FC CC _ _ _ _ (𝟙 X)) : (a : CC X) → CC X)
have 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
Tactic: convert! surjective_id
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Concrete (goal)
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)
    (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (f ≫ g)) : (a : CC X) → CC Z)
have 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))
Tactic: rw [hom_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Concrete (goal)
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) (β := CC X)
    (⇑(@ConcreteCategory.hom.{u_2, v, u, u_1} _ inst FC CC _ _ _ _ (𝟙 X)) : (a : CC X) → CC X)
have 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
Tactic: convert! bijective_id
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Concrete (goal)
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)
    (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (f ≫ g)) : (a : CC X) → CC Z)
have 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))
Tactic: rw [hom_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Concrete (goal)
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))
⊢ 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)
have 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) sorry) :
            X.right) :
          X.right) :
      (fun (X : Type u) ↦ X) Y.right)
Tactic: obtain ⟨_, x, rfl⟩ := y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Descent (goal)
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
⊢ P g
have have : ∀ (this : HasPullback f g), P g
Tactic: have : HasPullback f g := h.hasPullback
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Descent (goal)
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
⊢ P g
have apply : P (X := pullback f g) (pullback.fst f g)
Tactic: apply H hf
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Descent (goal)
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
⊢ P (X := pullback f g) (pullback.fst f g)
have rwa : P (CategoryStruct.comp (Y := pullback f g) (Iso.hom h.isoPullback) (pullback.fst f g))
Tactic: rwa [← P.cancel_left_of_respectsIso h.isoPullback.hom, h.isoPullback_hom_fst]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Descent (goal)
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
⊢ P g
have apply : P (snd ≫ g)
Tactic: apply P.of_precomp (W' := Q) _ _ (Q.of_isPullback h hf)
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Descent (goal)
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
⊢ P (snd ≫ g)
have rw : P (fst ≫ f)
Tactic: rw [← h.1.1]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Descent (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P_1 Q_1 W : 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 : HasPullbacks.{v_1, u_1} C
P Q : MorphismProperty.{v_1, u_1} C
inst_2 : P.DescendsAlong Q
inst_3 : P.RespectsIso
inst_4 : Q.IsStableUnderBaseChange
⊢ P.diagonal.DescendsAlong Q
have H : ∀ {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} [inst_5 : HasPullback f g],
  Q f → P.diagonal (X := pullback f g) (pullback.fst f g) → P.diagonal g
Tactic: apply DescendsAlong.mk'
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Descent (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P_1 Q_1 W : MorphismProperty.{v_1, u_1} C
A X_1 Y_1 Z_1 : C
fst : A ⟶ X_1
snd : A ⟶ Y_1
f_1 : X_1 ⟶ Z_1
g_1 : Y_1 ⟶ Z_1
inst_1 : HasPullbacks.{v_1, u_1} C
P Q : MorphismProperty.{v_1, u_1} C
inst_2 : P.DescendsAlong Q
inst_3 : P.RespectsIso
inst_4 : Q.IsStableUnderBaseChange
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_5 : HasPullback f g
hf : Q f
hfst : P.diagonal (X := pullback f g) (pullback.fst f g)
⊢ P.diagonal g
have heq : Eq (α :=
  pullback (X := pullback (X := pullback g g) (pullback.snd g g ≫ g) f) (pullback.fst (pullback.snd g g ≫ g) f)
      (pullback.diagonal g) ⟶
    pullback (X := pullback g g) (pullback.snd g g ≫ g) f)
  (pullback.fst (pullback.fst (pullback.snd g g ≫ g) f) (pullback.diagonal g) :
    pullback (X := pullback (X := pullback g g) (pullback.snd g g ≫ g) f) (pullback.fst (pullback.snd g g ≫ g) f)
        (pullback.diagonal g) ⟶
      pullback (X := pullback g g) (pullback.snd g g ≫ g) f)
  (Iso.hom (pullbackSymmetry (pullback.fst (pullback.snd g g ≫ g) f) (pullback.diagonal g)) ≫
      Iso.hom (pullbackRightPullbackFstIso (pullback.snd g g ≫ g) f (pullback.diagonal g)) ≫
        CategoryStruct.comp (Y := pullback g f) (Iso.hom (pullback.congrHom sorry sorry))
          (Iso.hom (pullbackSymmetry g f) ≫
            CategoryStruct.comp (Y := pullback.diagonalObj (X := pullback f g) (pullback.fst f g))
              (pullback.diagonal (pullback.fst f g) :
                pullback f g ⟶ pullback.diagonalObj (X := pullback f g) (pullback.fst f g))
              (Iso.hom (diagonalObjPullbackFstIso f g) :
                pullback.diagonalObj (X := pullback f g) (pullback.fst f g) ⟶
                  pullback (X := pullback.diagonalObj g) (pullback.snd g g ≫ g) f)) :
    pullback (X := pullback (X := pullback g g) (pullback.snd g g ≫ g) f) (pullback.fst (pullback.snd g g ≫ g) f)
        (pullback.diagonal g) ⟶
      pullback (X := pullback.diagonalObj g) (pullback.snd g g ≫ g) f)
Tactic: have heq : pullback.fst (pullback.fst (pullback.snd g g ≫ g) f) (pullback.diagonal g) =
      (pullbackSymmetry _ _).hom ≫
      (pullbackRightPullbackFstIso _ _ _).hom ≫
      (pullback.congrHom (by simp) rfl).hom ≫
      (pullbackSymmetry _ _).hom ≫
      pullback.diagonal (pullback.fst f g) ≫
      (diagonalObjPullbackFstIso f g).hom := by
    apply pullback.hom_ext
    apply pullback.hom_ext <;> simp [pullback.condition]
    simp [pullback.condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Descent (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P_1 Q_1 W : MorphismProperty.{v_1, u_1} C
A X_1 Y_1 Z_1 : C
fst : A ⟶ X_1
snd : A ⟶ Y_1
f_1 : X_1 ⟶ Z_1
g_1 : Y_1 ⟶ Z_1
inst_1 : HasPullbacks.{v_1, u_1} C
P Q : MorphismProperty.{v_1, u_1} C
inst_2 : P.DescendsAlong Q
inst_3 : P.RespectsIso
inst_4 : Q.IsStableUnderBaseChange
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_5 : HasPullback f g
hf : Q f
hfst : P.diagonal (X := pullback f g) (pullback.fst f g)
heq :
  Eq (α :=
    pullback (X := pullback (X := pullback g g) (pullback.snd g g ≫ g) f) (pullback.fst (pullback.snd g g ≫ g) f)
        (pullback.diagonal g) ⟶
      pullback (X := pullback g g) (pullback.snd g g ≫ g) f)
    (pullback.fst (pullback.fst (pullback.snd g g ≫ g) f) (pullback.diagonal g) :
      pullback (X := pullback (X := pullback g g) (pullback.snd g g ≫ g) f) (pullback.fst (pullback.snd g g ≫ g) f)
          (pullback.diagonal g) ⟶
        pullback (X := pullback g g) (pullback.snd g g ≫ g) f)
    (Iso.hom (pullbackSymmetry (pullback.fst (pullback.snd g g ≫ g) f) (pullback.diagonal g)) ≫
        Iso.hom (pullbackRightPullbackFstIso (pullback.snd g g ≫ g) f (pullback.diagonal g)) ≫
          CategoryStruct.comp (Y := pullback g f) (Iso.hom (pullback.congrHom ⋯ ⋯))
            (Iso.hom (pullbackSymmetry g f) ≫
              CategoryStruct.comp (Y := pullback.diagonalObj (X := pullback f g) (pullback.fst f g))
                (pullback.diagonal (pullback.fst f g) :
                  pullback f g ⟶ pullback.diagonalObj (X := pullback f g) (pullback.fst f g))
                (Iso.hom (diagonalObjPullbackFstIso f g) :
                  pullback.diagonalObj (X := pullback f g) (pullback.fst f g) ⟶
                    pullback (X := pullback.diagonalObj g) (pullback.snd g g ≫ g) f)) :
      pullback (X := pullback (X := pullback g g) (pullback.snd g g ≫ g) f) (pullback.fst (pullback.snd g g ≫ g) f)
          (pullback.diagonal g) ⟶
        pullback (X := pullback.diagonalObj g) (pullback.snd g g ≫ g) f)
⊢ P.diagonal g
have H : P (Y := pullback.diagonalObj g) (pullback.diagonal g)
Tactic: rw [diagonal_iff]