awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.IsSmall (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
h : IsSmall.{w, v, u} W
A B : C
f : A ⟶ B
mp :
  W f →
    ∃ (i : Shrink.{w, max u v} (↑W.toSet : Type (max u v))),
      Arrow.mk f =
        Arrow.mk (X :=
          Arrow.left.{v, u}
            (↑((Equiv.symm (equivShrink (↑W.toSet : Type (max u v))) :
                    (a : Shrink.{w, max u v} (↑W.toSet : Type (max u v))) → (↑W.toSet : Type (max u v)))
                  i) :
              Arrow C))
          (Arrow.hom
            (↑((Equiv.symm (equivShrink (↑W.toSet : Type (max u v))) :
                    (a : Shrink.{w, max u v} (↑W.toSet : Type (max u v))) → (↑W.toSet : Type (max u v)))
                  i) :
              Arrow C))
⊢ W f ↔
    ∃ (i : Shrink.{w, max u v} (↑W.toSet : Type (max u v))),
      Arrow.mk f =
        Arrow.mk (X :=
          Arrow.left.{v, u}
            (↑((Equiv.symm (equivShrink (↑W.toSet : Type (max u v))) :
                    (a : Shrink.{w, max u v} (↑W.toSet : Type (max u v))) → (↑W.toSet : Type (max u v)))
                  i) :
              Arrow C))
          (Arrow.hom
            (↑((Equiv.symm (equivShrink (↑W.toSet : Type (max u v))) :
                    (a : Shrink.{w, max u v} (↑W.toSet : Type (max u v))) → (↑W.toSet : Type (max u v)))
                  i) :
              Arrow C))
have mp₁ : (∃ (i : Shrink.{w, max u v} (↑W.toSet : Type (max u v))),
    Arrow.mk f =
      Arrow.mk (X :=
        Arrow.left.{v, u}
          (↑((Equiv.symm (equivShrink (↑W.toSet : Type (max u v))) :
                  (a : Shrink.{w, max u v} (↑W.toSet : Type (max u v))) → (↑W.toSet : Type (max u v)))
                i) :
            Arrow C))
        (Arrow.hom
          (↑((Equiv.symm (equivShrink (↑W.toSet : Type (max u v))) :
                  (a : Shrink.{w, max u v} (↑W.toSet : Type (max u v))) → (↑W.toSet : Type (max u v)))
                i) :
            Arrow C))) →
  W f
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.IsSmall (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W_1 : MorphismProperty.{v, u} C
α : Type u_1
W : α → MorphismProperty.{v, u} C
inst_1 : Small.{w, u_1} α
inst_2 : ∀ (a : α), IsSmall.{w, v, u} (W a)
⊢ Small.{w, max u v} (↑(iSup W).toSet : Type (max u v))
have rw : Small.{w, max u v} (↑(⋃ (i : α), (W i).toSet) : Type (max u v))
Tactic: rw [toSet_iSup]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.IsSmall (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W_1 : MorphismProperty.{v, u} C
α : Type u_1
W : α → MorphismProperty.{v, u} C
inst_1 : Small.{w, u_1} α
inst_2 : ∀ (a : α), IsSmall.{w, v, u} (W a)
x : (i : α) × (↑(W i).toSet : Type (max u v))
i : α
f : (↑(W i).toSet : Type (max u v))
⊢ Membership.mem (γ := Set (Arrow.{v, u} C)) (⋃ (i : α), (W i).toSet) (↑f : Arrow C)
have rw : ∃ (i_1 : α), (↑f : Arrow C) ∈ (W i_1).toSet
Tactic: rw [Set.mem_iUnion]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.IsSmall (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W_1 : MorphismProperty.{v, u} C
α : Type u_1
W : α → MorphismProperty.{v, u} C
inst_1 : Small.{w, u_1} α
inst_2 : ∀ (a : α), IsSmall.{w, v, u} (W a)
⊢ Small.{w, max u v} (↑(⋃ (i : α), (W i).toSet) : Type (max u v))
have refine : Function.Surjective (β := (↑(⋃ (i : α), (W i).toSet) : Type (max u v)))
  fun (x : (i : α) × (↑(@toSet C inst (W i)) : Type (max u v))) ↦
  match (motive := (i : α) × (↑(@toSet C inst (W i)) : Type (max u v)) → (↑(⋃ (i : α), (W i).toSet) : Type (max u v)))
    x with
  | ⟨i, f⟩ =>
    Subtype.mk (p := fun (x : Arrow.{v, u} C) ↦ Membership.mem (γ := Set (Arrow.{v, u} C)) (⋃ (i : α), (W i).toSet) x)
      (↑f : Arrow C) sorry
Tactic: refine small_of_surjective (f := fun (⟨i, f⟩ : Σ i, (W i).toSet) ↦
      ⟨f, by rw [Set.mem_iUnion]; exact ⟨i, f.prop⟩⟩) ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.IsSmall (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
W_1 : MorphismProperty.{v, u} C
α : Type u_1
W : α → MorphismProperty.{v, u} C
inst_1 : Small.{w, u_1} α
inst_2 : ∀ (a : α), IsSmall.{w, v, u} (W a)
f : Arrow.{v, u} C
hf : Membership.mem (γ := Set (Arrow.{v, u} C)) (⋃ (i : α), (W i).toSet) f
⊢ ∃ (a : (i : α) × (↑(W i).toSet : Type (max u v))),
    (fun (x : (i : α) × (↑(W i).toSet : Type (max u v))) ↦
          (match (motive := (i : α) × (↑(W i).toSet : Type (max u v)) → (↑(⋃ (i : α), (W i).toSet) : Type (max u v)))
              x with
            | ⟨i, f⟩ =>
              Subtype.mk (p := fun (x : Arrow.{v, u} C) ↦
                Membership.mem (γ := Set (Arrow.{v, u} C)) (⋃ (i : α), (W i).toSet) x) (↑f : Arrow C) ⋯ :
            (↑(⋃ (i : α), (W i).toSet) : Type (max u v))))
        a =
      Subtype.mk (p := fun (x : Arrow.{v, u} C) ↦ Membership.mem (γ := Set (Arrow.{v, u} C)) (⋃ (i : α), (W i).toSet) x)
        f hf
have hf₁ : ∃ (i : α), f ∈ (W i).toSet
Tactic: simp only [Set.mem_iUnion] at hf
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.IsSmall (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W_1 : MorphismProperty.{v, u} C
α : Type u_1
W : α → MorphismProperty.{v, u} C
inst_1 : Small.{w, u_1} α
inst_2 : ∀ (a : α), IsSmall.{w, v, u} (W a)
f : Arrow.{v, u} C
hf_1 : Membership.mem (γ := Set (Arrow.{v, u} C)) (⋃ (i : α), (W i).toSet) f
hf : ∃ (i : α), f ∈ (W i).toSet
⊢ ∃ (a : (i : α) × (↑(W i).toSet : Type (max u v))),
    (fun (x : (i : α) × (↑(W i).toSet : Type (max u v))) ↦
          (match (motive := (i : α) × (↑(W i).toSet : Type (max u v)) → (↑(⋃ (i : α), (W i).toSet) : Type (max u v)))
              x with
            | ⟨i, f⟩ =>
              Subtype.mk (p := fun (x : Arrow.{v, u} C) ↦
                Membership.mem (γ := Set (Arrow.{v, u} C)) (⋃ (i : α), (W i).toSet) x) (↑f : Arrow C) ⋯ :
            (↑(⋃ (i : α), (W i).toSet) : Type (max u v))))
        a =
      Subtype.mk (p := fun (x : Arrow.{v, u} C) ↦ Membership.mem (γ := Set (Arrow.{v, u} C)) (⋃ (i : α), (W i).toSet) x)
        f hf_1
have obtain : ∀ (i : α) (hf : f ∈ (W i).toSet),
  ∃ (a : (i : α) × (↑(W i).toSet : Type (max u v))),
    (fun (x : (i : α) × (↑(W i).toSet : Type (max u v))) ↦
          (match (motive := (i : α) × (↑(W i).toSet : Type (max u v)) → (↑(⋃ (i : α), (W i).toSet) : Type (max u v)))
              x with
            | ⟨i, f⟩ =>
              Subtype.mk (p := fun (x : Arrow.{v, u} C) ↦
                Membership.mem (γ := Set (Arrow.{v, u} C)) (⋃ (i : α), (W i).toSet) x) (↑f : Arrow C) sorry :
            (↑(⋃ (i : α), (W i).toSet) : Type (max u v))))
        a =
      Subtype.mk (p := fun (x : Arrow.{v, u} C) ↦ Membership.mem (γ := Set (Arrow.{v, u} C)) (⋃ (i : α), (W i).toSet) x)
        f hf_1
Tactic: obtain ⟨i, hf⟩ := hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.IsSmall (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W_1 : MorphismProperty.{v, u} C
α : Type t
inst_1 : Small.{w, t} α
W : α → MorphismProperty.{v, u} C
inst_2 : ∀ (i : α), IsSmall.{w, v, u} (W i)
⊢ IsSmall.{w, v, u} (C := C) (⨆ (i : α), W i)
have choose : ∀ (α_1 : (i : α) → Type w) (A B : (i : α) → α_1 i → C) (f : (i : α) → (i_1 : α_1 i) → A i i_1 ⟶ B i i_1)
  (hf : ∀ (i : α), W i = ofHoms (f i)), IsSmall.{w, v, u} (C := C) (⨆ (i : α), W i)
Tactic: choose α A B f hf using fun i ↦ (isSmall_iff_eq_ofHoms.{w} (W i)).1 inferInstance
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.IsSmall (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W_1 : MorphismProperty.{v, u} C
α_1 : Type t
inst_1 : Small.{w, t} α_1
W : α_1 → MorphismProperty.{v, u} C
inst_2 : ∀ (i : α_1), IsSmall.{w, v, u} (W i)
α : (i : α_1) → Type w
A B : (i : α_1) → α i → C
f : (i : α_1) → (i_1 : α i) → A i i_1 ⟶ B i i_1
hf : ∀ (i : α_1), W i = ofHoms (f i)
⊢ IsSmall.{w, v, u} (C := C) (⨆ (i : α_1), W i)
have simp : IsSmall.{w, v, u} (C := C)
  (ofHoms (X := fun (j : (a : α_1) × α a) ↦ A (j.fst (β := fun (a : α_1) ↦ α a)) (j.snd (β := fun (a : α_1) ↦ α a)))
    (Y := fun (j : (a : α_1) × α a) ↦ B (j.fst (β := fun (a : α_1) ↦ α a)) (j.snd (β := fun (a : α_1) ↦ α a)))
    fun (j : (a : α_1) × α a) ↦ f (j.fst (β := fun (a : α_1) ↦ α a)) (j.snd (β := fun (a : α_1) ↦ α a)))
Tactic: simp only [hf, iSup_ofHoms]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
h : ∀ (X : C), ∃ (A : C) (B : C) (p : A ⟶ B) (_ : P p) (x : B ⟶ X), IsIso p
X Y : C
f : X ⟶ Y
⊢ isomorphisms C f → P.pushouts f
have IsIso : IsIso f → P.pushouts f
Tactic: (_ : IsIso f)
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
h : ∀ (X : C), ∃ (A : C) (B : C) (p : A ⟶ B) (_ : P p) (x : B ⟶ X), IsIso p
X Y : C
f : X ⟶ Y
h_1 : IsIso f
⊢ P.pushouts f
have obtain : ∀ (A B : C) (p : A ⟶ B) (hp : P p) (g : B ⟶ X), IsIso p → P.pushouts f
Tactic: obtain ⟨A, B, p, hp, g, _⟩ := h X
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
⊢ P.IsStableUnderBaseChange ↔ P.pullbacks ≤ P
have mp : P.IsStableUnderBaseChange → P.pullbacks ≤ P
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
mp : P.IsStableUnderBaseChange → P.pullbacks ≤ P
⊢ P.IsStableUnderBaseChange ↔ P.pullbacks ≤ P
have mpr : P.pullbacks ≤ P → P.IsStableUnderBaseChange
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
h : P.IsStableUnderBaseChange
⊢ P.pullbacks ≤ P
have mp : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P.pullbacks f → P f
Tactic: _
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
h : P.IsStableUnderBaseChange
X Y : C
f : X ⟶ Y
⊢ P.pullbacks f → P f
have mp : ∀ (w w_1 : C) (w_2 : w ⟶ w_1) (w_3 : X ⟶ w) (w_4 : Y ⟶ w_1) (h₁ : P w_2) (h₂ : IsPullback w_3 f w_2 w_4), P f
Tactic: ⟨_, _, _, _, _, h₁, h₂⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
h : P.pullbacks ≤ P
⊢ P.IsStableUnderBaseChange
have mpr : ∀ {X Y Y' S : C} {f : X ⟶ S} {g : Y ⟶ S} {f' : Y' ⟶ Y} {g' : Y' ⟶ X} (sq : IsPullback f' g' g f) (hg : P g), P g'
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.RespectsIso
hP₂ : ∀ (X Y S : C) (f : X ⟶ S) (g : Y ⟶ S) [inst_2 : HasPullback f g], P g → P (X := pullback f g) (pullback.fst f g)
X Y Y' S : C
f : X ⟶ S
g : Y ⟶ S
f' : Y' ⟶ Y
g' : Y' ⟶ X
sq : IsPullback f' g' g f
hg : P g
⊢ P g'
have haveI : ∀ (this : HasPullback f g), P g'
Tactic: haveI : HasPullback f g := sq.flip.hasPullback
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.RespectsIso
hP₂ : ∀ (X Y S : C) (f : X ⟶ S) (g : Y ⟶ S) [inst_2 : HasPullback f g], P g → P (X := pullback f g) (pullback.fst f g)
X Y Y' S : C
f : X ⟶ S
g : Y ⟶ S
f' : Y' ⟶ Y
g' : Y' ⟶ X
sq : IsPullback f' g' g f
hg : P g
this : HasPullback f g
e : Y' ≅ pullback f g := ⋯.isoPullback
⊢ P g'
have rw : P (X := pullback f g) (pullback.fst f g)
Tactic: rw [← P.cancel_left_of_respectsIso e.inv, sq.flip.isoPullback_inv_fst]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.RespectsIso
H :
  ∀ {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [HasPullback f g],
    P g → ∃ (T : C) (fst : T ⟶ X) (snd : T ⟶ Y), IsPullback fst snd f g ∧ P fst
⊢ P.IsStableUnderBaseChange
have refine : ∀ (X Y S : C) (f : X ⟶ S) (g : Y ⟶ S) (x : HasPullback f g) (hg : P g), P (X := pullback f g) (pullback.fst f g)
Tactic: refine .mk' fun X Y S f g _ hg ↦ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.RespectsIso
H :
  ∀ {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [HasPullback f g],
    P g → ∃ (T : C) (fst : T ⟶ X) (snd : T ⟶ Y), IsPullback fst snd f g ∧ P fst
X Y S : C
f : X ⟶ S
g : Y ⟶ S
h : HasPullback f g
hg : P g
⊢ P (X := pullback f g) (pullback.fst f g)
have obtain : ∀ (T : C) (fst : T ⟶ X) (snd : T ⟶ Y) (h_1 : IsPullback fst snd f g) (hfst : P fst),
  P (X := pullback f g) (pullback.fst f g)
Tactic: obtain ⟨T, fst, snd, h, hfst⟩ := H f g hg
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.RespectsIso
H :
  ∀ {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [HasPullback f g],
    P g → ∃ (T : C) (fst : T ⟶ X) (snd : T ⟶ Y), IsPullback fst snd f g ∧ P fst
X Y S : C
f : X ⟶ S
g : Y ⟶ S
h_1 : HasPullback f g
hg : P g
T : C
fst : T ⟶ X
snd : T ⟶ Y
h : IsPullback fst snd f g
hfst : P fst
⊢ P (X := pullback f g) (pullback.fst f g)
have rwa : P (X := pullback f g) (Iso.inv h.isoPullback ≫ fst)
Tactic: rwa [← h.isoPullback_inv_fst, P.cancel_left_of_respectsIso]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.IsStableUnderBaseChange
⊢ P.RespectsIso
have hP : ∀ (f g : Arrow.{v, u} C) (x : f ≅ g), P f.hom → P g.hom
Tactic: apply RespectsIso.of_respects_arrow_iso
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.IsStableUnderBaseChange
S S' X Y : C
f : S' ⟶ S
v₁₂ : X ⟶ S
v₂₂ : Y ⟶ S
g : X ⟶ Y
hv₁₂ : v₁₂ = g ≫ v₂₂
inst_2 : HasPullback v₁₂ f
inst_3 : HasPullback v₂₂ f
H : P g
⊢ P (X := pullback v₁₂ f) (Y := pullback v₂₂ f) (pullback.lift (pullback.fst v₁₂ f ≫ g) (pullback.snd v₁₂ f) ⋯)
have subst : ∀ [inst_4 : HasPullback (g ≫ v₂₂) f],
  P (X := pullback (g ≫ v₂₂) f) (Y := pullback v₂₂ f)
    (pullback.lift (pullback.fst (g ≫ v₂₂) f ≫ g) (pullback.snd (g ≫ v₂₂) f) sorry)
Tactic: subst hv₁₂
Cleared hypotheses: v₁₂, hv₁₂, inst_2
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.IsStableUnderBaseChange
S S' X Y : C
f : S' ⟶ S
v₂₂ : Y ⟶ S
g : X ⟶ Y
inst_2 : HasPullback v₂₂ f
H : P g
inst_3 : HasPullback (g ≫ v₂₂) f
⊢ P (X := pullback (g ≫ v₂₂) f) (Y := pullback v₂₂ f)
    (pullback.lift (pullback.fst (g ≫ v₂₂) f ≫ g) (pullback.snd (g ≫ v₂₂) f) ⋯)
have refine : IsPullback (P := pullback (g ≫ v₂₂) f) (Y := pullback v₂₂ f) (pullback.fst (g ≫ v₂₂) f)
  (pullback.lift (pullback.fst (g ≫ v₂₂) f ≫ g) (pullback.snd (g ≫ v₂₂) f) sorry) g (pullback.fst v₂₂ f)
Tactic: refine of_isPullback (f' := pullback.fst (g ≫ v₂₂) f)
    (f := pullback.fst v₂₂ f) ?_ H
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.IsStableUnderBaseChange
S S' X Y : C
f : S' ⟶ S
v₂₂ : Y ⟶ S
g : X ⟶ Y
inst_2 : HasPullback v₂₂ f
H : P g
inst_3 : HasPullback (g ≫ v₂₂) f
⊢ IsPullback (P := pullback (g ≫ v₂₂) f) (Y := pullback v₂₂ f) (pullback.fst (g ≫ v₂₂) f)
    (pullback.lift (pullback.fst (g ≫ v₂₂) f ≫ g) (pullback.snd (g ≫ v₂₂) f) ⋯) g (pullback.fst v₂₂ f)
have refine : IsPullback (P := pullback (g ≫ v₂₂) f) (pullback.fst (g ≫ v₂₂) f)
  (CategoryStruct.comp (Y := pullback v₂₂ f) (pullback.lift (pullback.fst (g ≫ v₂₂) f ≫ g) (pullback.snd (g ≫ v₂₂) f) sorry)
    (pullback.snd v₂₂ f))
  (g ≫ v₂₂) f
Tactic: refine IsPullback.of_bot ?_ (by simp) (IsPullback.of_hasPullback v₂₂ f)
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.IsStableUnderBaseChange
inst_2 : P.IsStableUnderComposition
S X X' Y Y' : C
f : X ⟶ S
inst_3 : HasPullbacksAlong f
g : Y ⟶ S
f' : X' ⟶ S
g' : Y' ⟶ S
i₁ : X ⟶ X'
inst_4 : HasPullbacksAlong g'
i₂ : Y ⟶ Y'
h₁ : P i₁
h₂ : P i₂
e₁ : f = i₁ ≫ f'
e₂ : g = i₂ ≫ g'
⊢ P (X := pullback f g) (Y := pullback f' g') (pullback.map f g f' g' i₁ i₂ (𝟙 S) ⋯ ⋯)
have have : ∀ (this : HasPullbacksAlong (Over.mk f).hom),
  P (X := pullback f g) (Y := pullback f' g') (pullback.map f g f' g' i₁ i₂ (𝟙 S) sorry sorry)
Tactic: have : HasPullbacksAlong (Over.mk f).hom := by cat_disch
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.IsStableUnderBaseChange
inst_2 : P.IsStableUnderComposition
S X X' Y Y' : C
f : X ⟶ S
inst_3 : HasPullbacksAlong f
g : Y ⟶ S
f' : X' ⟶ S
g' : Y' ⟶ S
i₁ : X ⟶ X'
inst_4 : HasPullbacksAlong g'
i₂ : Y ⟶ Y'
h₁ : P i₁
h₂ : P i₂
e₁ : f = i₁ ≫ f'
e₂ : g = i₂ ≫ g'
this : HasPullbacksAlong (Over.mk f).hom
⊢ Eq (α := pullback f g ⟶ pullback f' g') (pullback.map f g f' g' i₁ i₂ (𝟙 S) ⋯ ⋯)
    ((Iso.hom (pullbackSymmetry (Over.mk f).hom (Over.mk g).hom) ≫
        Over.Hom.left ((Over.pullback (Over.mk f).hom).map (Over.homMk i₂ ⋯))) ≫
      Iso.hom (pullbackSymmetry (Over.mk g').hom (Over.mk f).hom) ≫
        Over.Hom.left ((Over.pullback g').map (Over.homMk i₁ ⋯)))
have h₀ : Eq (α := pullback f g ⟶ X')
  (CategoryStruct.comp (Y := pullback f' g') (pullback.map f g f' g' i₁ i₂ (𝟙 S) sorry sorry) (pullback.fst f' g'))
  (CategoryStruct.comp (Y := pullback f' g')
    ((Iso.hom (pullbackSymmetry (Over.mk f).hom (Over.mk g).hom) ≫
          Over.Hom.left ((Over.pullback (Over.mk f).hom).map (Over.homMk i₂ sorry))) ≫
        Iso.hom (pullbackSymmetry (Over.mk g').hom (Over.mk f).hom) ≫
          Over.Hom.left ((Over.pullback g').map (Over.homMk i₁ sorry)) :
      pullback (Over.mk f).hom (Over.mk g).hom ⟶ ((Over.pullback g').obj (Over.mk f')).left)
    (pullback.fst f' g'))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.IsStableUnderBaseChange
inst_2 : P.IsStableUnderComposition
S X X' Y Y' : C
f : X ⟶ S
inst_3 : HasPullbacksAlong f
g : Y ⟶ S
f' : X' ⟶ S
g' : Y' ⟶ S
i₁ : X ⟶ X'
inst_4 : HasPullbacksAlong g'
i₂ : Y ⟶ Y'
h₁ : P i₁
h₂ : P i₂
e₁ : f = i₁ ≫ f'
e₂ : g = i₂ ≫ g'
this : HasPullbacksAlong (Over.mk f).hom
h₀ :
  Eq (α := pullback f g ⟶ X')
    (CategoryStruct.comp (Y := pullback f' g') (pullback.map f g f' g' i₁ i₂ (𝟙 S) ⋯ ⋯) (pullback.fst f' g'))
    (CategoryStruct.comp (Y := pullback f' g')
      ((Iso.hom (pullbackSymmetry (Over.mk f).hom (Over.mk g).hom) ≫
            Over.Hom.left ((Over.pullback (Over.mk f).hom).map (Over.homMk i₂ ⋯))) ≫
          Iso.hom (pullbackSymmetry (Over.mk g').hom (Over.mk f).hom) ≫
            Over.Hom.left ((Over.pullback g').map (Over.homMk i₁ ⋯)) :
        pullback (Over.mk f).hom (Over.mk g).hom ⟶ ((Over.pullback g').obj (Over.mk f')).left)
      (pullback.fst f' g'))
⊢ Eq (α := pullback f g ⟶ pullback f' g') (pullback.map f g f' g' i₁ i₂ (𝟙 S) ⋯ ⋯)
    ((Iso.hom (pullbackSymmetry (Over.mk f).hom (Over.mk g).hom) ≫
        Over.Hom.left ((Over.pullback (Over.mk f).hom).map (Over.homMk i₂ ⋯))) ≫
      Iso.hom (pullbackSymmetry (Over.mk g').hom (Over.mk f).hom) ≫
        Over.Hom.left ((Over.pullback g').map (Over.homMk i₁ ⋯)))
have h₃ : Eq (α := pullback f g ⟶ Y')
  (CategoryStruct.comp (Y := pullback f' g') (pullback.map f g f' g' i₁ i₂ (𝟙 S) sorry sorry) (pullback.snd f' g'))
  (CategoryStruct.comp (Y := pullback f' g')
    ((Iso.hom (pullbackSymmetry (Over.mk f).hom (Over.mk g).hom) ≫
          Over.Hom.left ((Over.pullback (Over.mk f).hom).map (Over.homMk i₂ sorry))) ≫
        Iso.hom (pullbackSymmetry (Over.mk g').hom (Over.mk f).hom) ≫
          Over.Hom.left ((Over.pullback g').map (Over.homMk i₁ sorry)) :
      pullback (Over.mk f).hom (Over.mk g).hom ⟶ ((Over.pullback g').obj (Over.mk f')).left)
    (pullback.snd f' g'))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Limits (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.IsStableUnderBaseChange
inst_2 : P.IsStableUnderComposition
S X X' Y Y' : C
f : X ⟶ S
inst_3 : HasPullbacksAlong f
g : Y ⟶ S
f' : X' ⟶ S
g' : Y' ⟶ S
i₁ : X ⟶ X'
inst_4 : HasPullbacksAlong g'
i₂ : Y ⟶ Y'
h₁ : P i₁
h₂ : P i₂
e₁ : f = i₁ ≫ f'
e₂ : g = i₂ ≫ g'
this : HasPullbacksAlong (Over.mk f).hom
⊢ P (X := pullback f g) (Y := pullback f' g') (pullback.map f g f' g' i₁ i₂ (𝟙 S) ⋯ ⋯)
have this₁ : Eq (α := pullback f g ⟶ pullback f' g') (pullback.map f g f' g' i₁ i₂ (𝟙 S) sorry sorry)
  ((Iso.hom (pullbackSymmetry (Over.mk f).hom (Over.mk g).hom) ≫
      Over.Hom.left ((Over.pullback (Over.mk f).hom).map (Over.homMk i₂ sorry))) ≫
    Iso.hom (pullbackSymmetry (Over.mk g').hom (Over.mk f).hom) ≫
      Over.Hom.left ((Over.pullback g').map (Over.homMk i₁ sorry)))
Tactic: have : pullback.map f g f' g' i₁ i₂ (𝟙 _) ((Category.comp_id _).trans e₁)
        ((Category.comp_id _).trans e₂) =
      ((pullbackSymmetry _ _).hom ≫
          ((Over.pullback _).map (Over.homMk _ e₂.symm : Over.mk g ⟶ Over.mk g')).left) ≫
        (pullbackSymmetry _ _).hom ≫
          ((Over.pullback g').map (Over.homMk _ e₁.symm : Over.mk f ⟶ Over.mk f')).left := by
    ext <;> simp
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.IsStableUnderBaseChange
inst_2 : P.IsStableUnderComposition
S X X' Y Y' : C
f : X ⟶ S
inst_3 : HasPullbacksAlong f
g : Y ⟶ S
f' : X' ⟶ S
g' : Y' ⟶ S
i₁ : X ⟶ X'
inst_4 : HasPullbacksAlong g'
i₂ : Y ⟶ Y'
h₁ : P i₁
h₂ : P i₂
e₁ : f = i₁ ≫ f'
e₂ : g = i₂ ≫ g'
this_1 : HasPullbacksAlong (Over.mk f).hom
this :
  Eq (α := pullback f g ⟶ pullback f' g') (pullback.map f g f' g' i₁ i₂ (𝟙 S) ⋯ ⋯)
    ((Iso.hom (pullbackSymmetry (Over.mk f).hom (Over.mk g).hom) ≫
        Over.Hom.left ((Over.pullback (Over.mk f).hom).map (Over.homMk i₂ ⋯))) ≫
      Iso.hom (pullbackSymmetry (Over.mk g').hom (Over.mk f).hom) ≫
        Over.Hom.left ((Over.pullback g').map (Over.homMk i₁ ⋯)))
⊢ P (X := pullback f g) (Y := pullback f' g') (pullback.map f g f' g' i₁ i₂ (𝟙 S) ⋯ ⋯)
have rw : P (X := pullback f g) (Y := pullback f' g')
  ((Iso.hom (pullbackSymmetry (Over.mk f).hom (Over.mk g).hom) ≫
        Over.Hom.left ((Over.pullback (Over.mk f).hom).map (Over.homMk i₂ sorry))) ≫
      Iso.hom (pullbackSymmetry (Over.mk g').hom (Over.mk f).hom) ≫
        Over.Hom.left ((Over.pullback g').map (Over.homMk i₁ sorry)) :
    pullback (Over.mk f).hom (Over.mk g).hom ⟶ ((Over.pullback g').obj (Over.mk f')).left)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.IsStableUnderBaseChange
inst_2 : P.IsStableUnderComposition
S X X' Y Y' : C
f : X ⟶ S
inst_3 : HasPullbacksAlong f
g : Y ⟶ S
f' : X' ⟶ S
g' : Y' ⟶ S
i₁ : X ⟶ X'
inst_4 : HasPullbacksAlong g'
i₂ : Y ⟶ Y'
h₁ : P i₁
h₂ : P i₂
e₁ : f = i₁ ≫ f'
e₂ : g = i₂ ≫ g'
this_1 : HasPullbacksAlong (Over.mk f).hom
this :
  Eq (α := pullback f g ⟶ pullback f' g') (pullback.map f g f' g' i₁ i₂ (𝟙 S) ⋯ ⋯)
    ((Iso.hom (pullbackSymmetry (Over.mk f).hom (Over.mk g).hom) ≫
        Over.Hom.left ((Over.pullback (Over.mk f).hom).map (Over.homMk i₂ ⋯))) ≫
      Iso.hom (pullbackSymmetry (Over.mk g').hom (Over.mk f).hom) ≫
        Over.Hom.left ((Over.pullback g').map (Over.homMk i₁ ⋯)))
⊢ P (X := pullback f g) (Y := pullback f' g')
    ((Iso.hom (pullbackSymmetry (Over.mk f).hom (Over.mk g).hom) ≫
          Over.Hom.left ((Over.pullback (Over.mk f).hom).map (Over.homMk i₂ ⋯))) ≫
        Iso.hom (pullbackSymmetry (Over.mk g').hom (Over.mk f).hom) ≫
          Over.Hom.left ((Over.pullback g').map (Over.homMk i₁ ⋯)) :
      pullback (Over.mk f).hom (Over.mk g).hom ⟶ ((Over.pullback g').obj (Over.mk f')).left)
have hf : P (X := pullback f g) (Y := ((Over.pullback (Over.mk f).hom).obj (Over.mk g')).left)
  (Iso.hom (pullbackSymmetry (Over.mk f).hom (Over.mk g).hom) ≫
    Over.Hom.left ((Over.pullback (Over.mk f).hom).map (Over.homMk i₂ sorry)))
Tactic: apply P.comp_mem