awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₁ ⋯)))
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₂ ⋯)))
⊢ 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 hg : P (X := ((Over.pullback (Over.mk f).hom).obj (Over.mk g')).left) (Y := pullback f' g')
  (Iso.hom (pullbackSymmetry (Over.mk g').hom (Over.mk f).hom) ≫
      Over.Hom.left ((Over.pullback g').map (Over.homMk i₁ sorry)) :
    ((Over.pullback (Over.mk f).hom).obj (Over.mk g')).left ⟶ ((Over.pullback g').obj (Over.mk f')).left)
Tactic: apply P.comp_mem
-- 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 := ((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₂ ⋯)))
have hf : P (X := pullback (Over.mk g).hom (Over.mk f).hom) (Y := ((Over.pullback (Over.mk f).hom).obj (Over.mk g')).left)
  (Over.Hom.left ((Over.pullback (Over.mk f).hom).map (Over.homMk i₂ sorry)))
Tactic: rw [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
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 := ((Over.pullback (Over.mk f).hom).obj (Over.mk g')).left) (Y := pullback f' g')
    (Iso.hom (pullbackSymmetry (Over.mk g').hom (Over.mk f).hom) ≫
        Over.Hom.left ((Over.pullback g').map (Over.homMk i₁ ⋯)) :
      ((Over.pullback (Over.mk f).hom).obj (Over.mk g')).left ⟶ ((Over.pullback g').obj (Over.mk f')).left)
have hg : P (X := pullback (Over.mk f).hom (Over.mk g').hom) (Y := pullback f' g')
  (Over.Hom.left ((Over.pullback g').map (Over.homMk i₁ sorry)) :
    ((Over.pullback g').obj (Over.mk f)).left ⟶ ((Over.pullback g').obj (Over.mk f')).left)
Tactic: rw [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
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hg : Mono g
hcomp : P (f ≫ g)
⊢ P f
have have : ∀
  (this :
    f =
      CategoryStruct.comp (Y := pullback (f ≫ g) g) (Iso.inv (asIso (pullback.fst (f ≫ g) g)))
        (pullback.snd (f ≫ g) g)),
  P f
Tactic: have : f = (asIso (pullback.fst (f ≫ g) g)).inv ≫ pullback.snd (f ≫ g) g := by
      simp [← cancel_mono g, pullback.condition]
-- 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
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hg : Mono g
hcomp : P (f ≫ g)
this :
  f = CategoryStruct.comp (Y := pullback (f ≫ g) g) (Iso.inv (asIso (pullback.fst (f ≫ g) g))) (pullback.snd (f ≫ g) g)
⊢ P f
have rw : P (X := pullback (f ≫ g) g) (pullback.snd (f ≫ g) g)
Tactic: rw [this, cancel_left_of_respectsIso (P := P)]
-- 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.IsStableUnderCobaseChange ↔ P.pushouts ≤ P
have mp : P.IsStableUnderCobaseChange → P.pushouts ≤ 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.IsStableUnderCobaseChange → P.pushouts ≤ P
⊢ P.IsStableUnderCobaseChange ↔ P.pushouts ≤ P
have mpr : P.pushouts ≤ P → P.IsStableUnderCobaseChange
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.IsStableUnderCobaseChange
⊢ P.pushouts ≤ P
have mp : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P.pushouts 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.IsStableUnderCobaseChange
X Y : C
f : X ⟶ Y
⊢ P.pushouts f → P f
have mp : ∀ (w w_1 : C) (w_2 : w ⟶ w_1) (w_3 : w ⟶ X) (w_4 : w_1 ⟶ Y) (h₁ : P w_2) (h₂ : IsPushout w_3 w_2 f 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.pushouts ≤ P
⊢ P.IsStableUnderCobaseChange
have mpr : ∀ {A A' B B' : C} {f : A ⟶ A'} {g : A ⟶ B} {f' : B ⟶ B'} {g' : A' ⟶ B'} (sq : IsPushout g f f' g') (hf : P f), P f'
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P Q : MorphismProperty.{v, u} C
inst_1 : Q.IsStableUnderCobaseChange
⊢ P.pushouts ≤ Q ↔ P ≤ Q
have mp : P.pushouts ≤ Q → P ≤ Q
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P Q : MorphismProperty.{v, u} C
inst_1 : Q.IsStableUnderCobaseChange
mp : P.pushouts ≤ Q → P ≤ Q
⊢ P.pushouts ≤ Q ↔ P ≤ Q
have mpr : P ≤ Q → P.pushouts ≤ Q
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₂ : ∀ (A B A' : C) (f : A ⟶ A') (g : A ⟶ B) [inst_2 : HasPushout f g], P f → P (Y := pushout f g) (pushout.inr f g)
A A' B B' : C
f : A ⟶ A'
g : A ⟶ B
f' : B ⟶ B'
g' : A' ⟶ B'
sq : IsPushout g f f' g'
hf : P f
⊢ P f'
have haveI : ∀ (this : HasPushout f g), P f'
Tactic: haveI : HasPushout f g := sq.flip.hasPushout
-- 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₂ : ∀ (A B A' : C) (f : A ⟶ A') (g : A ⟶ B) [inst_2 : HasPushout f g], P f → P (Y := pushout f g) (pushout.inr f g)
A A' B B' : C
f : A ⟶ A'
g : A ⟶ B
f' : B ⟶ B'
g' : A' ⟶ B'
sq : IsPushout g f f' g'
hf : P f
this : HasPushout f g
e : B' ≅ pushout f g := ⋯.isoPushout
⊢ P f'
have rw : P (Y := pushout f g) (pushout.inr f g)
Tactic: rw [← P.cancel_right_of_respectsIso _ e.hom, sq.flip.inr_isoPushout_hom]
-- 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 : Z ⟶ X) (g : Z ⟶ Y) [HasPushout f g],
    P f → ∃ (T : C) (inl : X ⟶ T) (inr : Y ⟶ T), IsPushout f g inl inr ∧ P inr
⊢ P.IsStableUnderCobaseChange
have refine : ∀ (X Y S : C) (f : X ⟶ S) (g : X ⟶ Y) (x : HasPushout f g) (hg : P f), P (Y := pushout f g) (pushout.inr 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 : Z ⟶ X) (g : Z ⟶ Y) [HasPushout f g],
    P f → ∃ (T : C) (inl : X ⟶ T) (inr : Y ⟶ T), IsPushout f g inl inr ∧ P inr
X Y S : C
f : X ⟶ S
g : X ⟶ Y
h : HasPushout f g
hg : P f
⊢ P (Y := pushout f g) (pushout.inr f g)
have obtain : ∀ (T : C) (inl : S ⟶ T) (inr : Y ⟶ T) (h_1 : IsPushout f g inl inr) (hinl : P inr),
  P (Y := pushout f g) (pushout.inr f g)
Tactic: obtain ⟨T, inl, inr, h, hinl⟩ := 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 : Z ⟶ X) (g : Z ⟶ Y) [HasPushout f g],
    P f → ∃ (T : C) (inl : X ⟶ T) (inr : Y ⟶ T), IsPushout f g inl inr ∧ P inr
X Y S : C
f : X ⟶ S
g : X ⟶ Y
h_1 : HasPushout f g
hg : P f
T : C
inl : S ⟶ T
inr : Y ⟶ T
h : IsPushout f g inl inr
hinl : P inr
⊢ P (Y := pushout f g) (pushout.inr f g)
have rwa : P (Y := pushout f g) (inr ≫ Iso.hom h.isoPushout)
Tactic: rwa [← h.inr_isoPushout_hom, P.cancel_right_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.IsStableUnderCobaseChange
S S' X Y : C
f : S ⟶ S'
v₁₂ : S ⟶ X
v₂₂ : S ⟶ Y
g : Y ⟶ X
hv₁₂ : v₁₂ = v₂₂ ≫ g
inst_2 : HasPushout v₁₂ f
inst_3 : HasPushout v₂₂ f
H : P g
⊢ P (X := pushout v₂₂ f) (Y := pushout v₁₂ f) (pushout.desc (g ≫ pushout.inl v₁₂ f) (pushout.inr v₁₂ f) ⋯)
have subst : ∀ [inst_4 : HasPushout (v₂₂ ≫ g) f],
  P (X := pushout v₂₂ f) (Y := pushout (v₂₂ ≫ g) f)
    (pushout.desc (g ≫ pushout.inl (v₂₂ ≫ g) f) (pushout.inr (v₂₂ ≫ g) 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.IsStableUnderCobaseChange
S S' X Y : C
f : S ⟶ S'
v₂₂ : S ⟶ Y
g : Y ⟶ X
inst_2 : HasPushout v₂₂ f
H : P g
inst_3 : HasPushout (v₂₂ ≫ g) f
⊢ P (X := pushout v₂₂ f) (Y := pushout (v₂₂ ≫ g) f)
    (pushout.desc (g ≫ pushout.inl (v₂₂ ≫ g) f) (pushout.inr (v₂₂ ≫ g) f) ⋯)
have refine : IsPushout (X := pushout v₂₂ f) (P := pushout (v₂₂ ≫ g) f) (pushout.inl v₂₂ f) g
  (pushout.desc (g ≫ pushout.inl (v₂₂ ≫ g) f) (pushout.inr (v₂₂ ≫ g) f) sorry) (pushout.inl (v₂₂ ≫ g) f)
Tactic: refine IsStableUnderCobaseChangeAlong.of_isPushout (f' := pushout.inl (v₂₂ ≫ g) f)
    (f := pushout.inl 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.IsStableUnderCobaseChange
S S' X Y : C
f : S ⟶ S'
v₂₂ : S ⟶ Y
g : Y ⟶ X
inst_2 : HasPushout v₂₂ f
H : P g
inst_3 : HasPushout (v₂₂ ≫ g) f
⊢ IsPushout (X := pushout v₂₂ f) (P := pushout (v₂₂ ≫ g) f) (pushout.inl v₂₂ f) g
    (pushout.desc (g ≫ pushout.inl (v₂₂ ≫ g) f) (pushout.inr (v₂₂ ≫ g) f) ⋯) (pushout.inl (v₂₂ ≫ g) f)
have refine : IsPushout (P := pushout (v₂₂ ≫ g) f) f (v₂₂ ≫ g)
  (CategoryStruct.comp (Y := pushout v₂₂ f) (pushout.inr v₂₂ f)
    (pushout.desc (g ≫ pushout.inl (v₂₂ ≫ g) f) (pushout.inr (v₂₂ ≫ g) f) sorry))
  (pushout.inl (v₂₂ ≫ g) f)
Tactic: refine IsPushout.of_top ?_ (by simp) (IsPushout.of_hasPushout v₂₂ f).flip
-- 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.IsStableUnderCobaseChange
inst_2 : P.IsStableUnderComposition
S X X' Y Y' : C
f : S ⟶ X
g : S ⟶ Y
f' : S ⟶ X'
g' : S ⟶ Y'
i₁ : X ⟶ X'
inst_3 : HasPushoutsAlong f
inst_4 : HasPushoutsAlong g'
i₂ : Y ⟶ Y'
h₁ : P i₁
h₂ : P i₂
e₁ : f' = f ≫ i₁
e₂ : g' = g ≫ i₂
⊢ P (X := pushout f g) (Y := pushout f' g') (pushout.map f g f' g' i₁ i₂ (𝟙 S) ⋯ ⋯)
have have : ∀ (this : HasPushoutsAlong (Under.mk g').hom),
  P (X := pushout f g) (Y := pushout f' g') (pushout.map f g f' g' i₁ i₂ (𝟙 S) sorry sorry)
Tactic: have : HasPushoutsAlong (Under.mk g').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.IsStableUnderCobaseChange
inst_2 : P.IsStableUnderComposition
S X X' Y Y' : C
f : S ⟶ X
g : S ⟶ Y
f' : S ⟶ X'
g' : S ⟶ Y'
i₁ : X ⟶ X'
inst_3 : HasPushoutsAlong f
inst_4 : HasPushoutsAlong g'
i₂ : Y ⟶ Y'
h₁ : P i₁
h₂ : P i₂
e₁ : f' = f ≫ i₁
e₂ : g' = g ≫ i₂
this : HasPushoutsAlong (Under.mk g').hom
⊢ Eq (α := pushout f g ⟶ pushout f' g') (pushout.map f g f' g' i₁ i₂ (𝟙 S) ⋯ ⋯)
    ((Iso.hom (pushoutSymmetry f (Under.mk g).hom) ≫ Under.Hom.right ((Under.pushout f).map (Under.homMk i₂ ⋯))) ≫
      Iso.hom (pushoutSymmetry (Under.mk g').hom f) ≫ Under.Hom.right ((Under.pushout g').map (Under.homMk i₁ ⋯)))
have h₀ : Eq (α := X ⟶ pushout f' g')
  (CategoryStruct.comp (Y := pushout f g) (pushout.inl f g) (pushout.map f g f' g' i₁ i₂ (𝟙 S) sorry sorry))
  (CategoryStruct.comp (Y := pushout f g) (pushout.inl f g)
    ((Iso.hom (pushoutSymmetry f (Under.mk g).hom) ≫ Under.Hom.right ((Under.pushout f).map (Under.homMk i₂ sorry))) ≫
      Iso.hom (pushoutSymmetry (Under.mk g').hom f) ≫ Under.Hom.right ((Under.pushout g').map (Under.homMk i₁ sorry))))
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.IsStableUnderCobaseChange
inst_2 : P.IsStableUnderComposition
S X X' Y Y' : C
f : S ⟶ X
g : S ⟶ Y
f' : S ⟶ X'
g' : S ⟶ Y'
i₁ : X ⟶ X'
inst_3 : HasPushoutsAlong f
inst_4 : HasPushoutsAlong g'
i₂ : Y ⟶ Y'
h₁ : P i₁
h₂ : P i₂
e₁ : f' = f ≫ i₁
e₂ : g' = g ≫ i₂
this : HasPushoutsAlong (Under.mk g').hom
h₀ :
  Eq (α := X ⟶ pushout f' g')
    (CategoryStruct.comp (Y := pushout f g) (pushout.inl f g) (pushout.map f g f' g' i₁ i₂ (𝟙 S) ⋯ ⋯))
    (CategoryStruct.comp (Y := pushout f g) (pushout.inl f g)
      ((Iso.hom (pushoutSymmetry f (Under.mk g).hom) ≫ Under.Hom.right ((Under.pushout f).map (Under.homMk i₂ ⋯))) ≫
        Iso.hom (pushoutSymmetry (Under.mk g').hom f) ≫ Under.Hom.right ((Under.pushout g').map (Under.homMk i₁ ⋯))))
⊢ Eq (α := pushout f g ⟶ pushout f' g') (pushout.map f g f' g' i₁ i₂ (𝟙 S) ⋯ ⋯)
    ((Iso.hom (pushoutSymmetry f (Under.mk g).hom) ≫ Under.Hom.right ((Under.pushout f).map (Under.homMk i₂ ⋯))) ≫
      Iso.hom (pushoutSymmetry (Under.mk g').hom f) ≫ Under.Hom.right ((Under.pushout g').map (Under.homMk i₁ ⋯)))
have h₃ : Eq (α := Y ⟶ pushout f' g')
  (CategoryStruct.comp (Y := pushout f g) (pushout.inr f g) (pushout.map f g f' g' i₁ i₂ (𝟙 S) sorry sorry))
  (CategoryStruct.comp (Y := pushout f g) (pushout.inr f g)
    ((Iso.hom (pushoutSymmetry f (Under.mk g).hom) ≫ Under.Hom.right ((Under.pushout f).map (Under.homMk i₂ sorry))) ≫
      Iso.hom (pushoutSymmetry (Under.mk g').hom f) ≫ Under.Hom.right ((Under.pushout g').map (Under.homMk i₁ sorry))))
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.IsStableUnderCobaseChange
inst_2 : P.IsStableUnderComposition
S X X' Y Y' : C
f : S ⟶ X
g : S ⟶ Y
f' : S ⟶ X'
g' : S ⟶ Y'
i₁ : X ⟶ X'
inst_3 : HasPushoutsAlong f
inst_4 : HasPushoutsAlong g'
i₂ : Y ⟶ Y'
h₁ : P i₁
h₂ : P i₂
e₁ : f' = f ≫ i₁
e₂ : g' = g ≫ i₂
this : HasPushoutsAlong (Under.mk g').hom
⊢ P (X := pushout f g) (Y := pushout f' g') (pushout.map f g f' g' i₁ i₂ (𝟙 S) ⋯ ⋯)
have this₁ : Eq (α := pushout f g ⟶ pushout f' g') (pushout.map f g f' g' i₁ i₂ (𝟙 S) sorry sorry)
  ((Iso.hom (pushoutSymmetry f (Under.mk g).hom) ≫ Under.Hom.right ((Under.pushout f).map (Under.homMk i₂ sorry))) ≫
    Iso.hom (pushoutSymmetry (Under.mk g').hom f) ≫ Under.Hom.right ((Under.pushout g').map (Under.homMk i₁ sorry)))
Tactic: have : pushout.map f g f' g' i₁ i₂ (𝟙 _) (by simp [e₁]) (by simp [e₂]) =
      ((pushoutSymmetry _ _).hom ≫
        ((Under.pushout f).map (Under.homMk _ e₂.symm : Under.mk g ⟶ Under.mk g')).right) ≫
        (pushoutSymmetry _ _).hom ≫
        ((Under.pushout g').map (Under.homMk _ e₁.symm : Under.mk f ⟶ Under.mk f')).right := 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.IsStableUnderCobaseChange
inst_2 : P.IsStableUnderComposition
S X X' Y Y' : C
f : S ⟶ X
g : S ⟶ Y
f' : S ⟶ X'
g' : S ⟶ Y'
i₁ : X ⟶ X'
inst_3 : HasPushoutsAlong f
inst_4 : HasPushoutsAlong g'
i₂ : Y ⟶ Y'
h₁ : P i₁
h₂ : P i₂
e₁ : f' = f ≫ i₁
e₂ : g' = g ≫ i₂
this_1 : HasPushoutsAlong (Under.mk g').hom
this :
  Eq (α := pushout f g ⟶ pushout f' g') (pushout.map f g f' g' i₁ i₂ (𝟙 S) ⋯ ⋯)
    ((Iso.hom (pushoutSymmetry f (Under.mk g).hom) ≫ Under.Hom.right ((Under.pushout f).map (Under.homMk i₂ ⋯))) ≫
      Iso.hom (pushoutSymmetry (Under.mk g').hom f) ≫ Under.Hom.right ((Under.pushout g').map (Under.homMk i₁ ⋯)))
⊢ P (X := pushout f g) (Y := pushout f' g') (pushout.map f g f' g' i₁ i₂ (𝟙 S) ⋯ ⋯)
have rw : P (X := pushout f g) (Y := pushout f' g')
  ((Iso.hom (pushoutSymmetry f (Under.mk g).hom) ≫ Under.Hom.right ((Under.pushout f).map (Under.homMk i₂ sorry))) ≫
    Iso.hom (pushoutSymmetry (Under.mk g').hom f) ≫ Under.Hom.right ((Under.pushout g').map (Under.homMk i₁ sorry)))
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.IsStableUnderCobaseChange
inst_2 : P.IsStableUnderComposition
S X X' Y Y' : C
f : S ⟶ X
g : S ⟶ Y
f' : S ⟶ X'
g' : S ⟶ Y'
i₁ : X ⟶ X'
inst_3 : HasPushoutsAlong f
inst_4 : HasPushoutsAlong g'
i₂ : Y ⟶ Y'
h₁ : P i₁
h₂ : P i₂
e₁ : f' = f ≫ i₁
e₂ : g' = g ≫ i₂
this_1 : HasPushoutsAlong (Under.mk g').hom
this :
  Eq (α := pushout f g ⟶ pushout f' g') (pushout.map f g f' g' i₁ i₂ (𝟙 S) ⋯ ⋯)
    ((Iso.hom (pushoutSymmetry f (Under.mk g).hom) ≫ Under.Hom.right ((Under.pushout f).map (Under.homMk i₂ ⋯))) ≫
      Iso.hom (pushoutSymmetry (Under.mk g').hom f) ≫ Under.Hom.right ((Under.pushout g').map (Under.homMk i₁ ⋯)))
⊢ P (X := pushout f g) (Y := pushout f' g')
    ((Iso.hom (pushoutSymmetry f (Under.mk g).hom) ≫ Under.Hom.right ((Under.pushout f).map (Under.homMk i₂ ⋯))) ≫
      Iso.hom (pushoutSymmetry (Under.mk g').hom f) ≫ Under.Hom.right ((Under.pushout g').map (Under.homMk i₁ ⋯)))
have hf : P (X := pushout f g) (Y := ((Under.pushout f).obj (Under.mk g')).right)
  (Iso.hom (pushoutSymmetry f (Under.mk g).hom) ≫ Under.Hom.right ((Under.pushout f).map (Under.homMk i₂ sorry)))
Tactic: apply P.comp_mem
-- 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.IsStableUnderCobaseChange
inst_2 : P.IsStableUnderComposition
S X X' Y Y' : C
f : S ⟶ X
g : S ⟶ Y
f' : S ⟶ X'
g' : S ⟶ Y'
i₁ : X ⟶ X'
inst_3 : HasPushoutsAlong f
inst_4 : HasPushoutsAlong g'
i₂ : Y ⟶ Y'
h₁ : P i₁
h₂ : P i₂
e₁ : f' = f ≫ i₁
e₂ : g' = g ≫ i₂
this_1 : HasPushoutsAlong (Under.mk g').hom
this :
  Eq (α := pushout f g ⟶ pushout f' g') (pushout.map f g f' g' i₁ i₂ (𝟙 S) ⋯ ⋯)
    ((Iso.hom (pushoutSymmetry f (Under.mk g).hom) ≫ Under.Hom.right ((Under.pushout f).map (Under.homMk i₂ ⋯))) ≫
      Iso.hom (pushoutSymmetry (Under.mk g').hom f) ≫ Under.Hom.right ((Under.pushout g').map (Under.homMk i₁ ⋯)))
hf :
  P (X := pushout f g) (Y := ((Under.pushout f).obj (Under.mk g')).right)
    (Iso.hom (pushoutSymmetry f (Under.mk g).hom) ≫ Under.Hom.right ((Under.pushout f).map (Under.homMk i₂ ⋯)))
⊢ P (X := pushout f g) (Y := pushout f' g')
    ((Iso.hom (pushoutSymmetry f (Under.mk g).hom) ≫ Under.Hom.right ((Under.pushout f).map (Under.homMk i₂ ⋯))) ≫
      Iso.hom (pushoutSymmetry (Under.mk g').hom f) ≫ Under.Hom.right ((Under.pushout g').map (Under.homMk i₁ ⋯)))
have hg : P (X := ((Under.pushout f).obj (Under.mk g')).right) (Y := pushout f' g')
  (Iso.hom (pushoutSymmetry (Under.mk g').hom f) ≫ Under.Hom.right ((Under.pushout g').map (Under.homMk i₁ sorry)))
Tactic: apply P.comp_mem
-- 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.IsStableUnderCobaseChange
inst_2 : P.IsStableUnderComposition
S X X' Y Y' : C
f : S ⟶ X
g : S ⟶ Y
f' : S ⟶ X'
g' : S ⟶ Y'
i₁ : X ⟶ X'
inst_3 : HasPushoutsAlong f
inst_4 : HasPushoutsAlong g'
i₂ : Y ⟶ Y'
h₁ : P i₁
h₂ : P i₂
e₁ : f' = f ≫ i₁
e₂ : g' = g ≫ i₂
this_1 : HasPushoutsAlong (Under.mk g').hom
this :
  Eq (α := pushout f g ⟶ pushout f' g') (pushout.map f g f' g' i₁ i₂ (𝟙 S) ⋯ ⋯)
    ((Iso.hom (pushoutSymmetry f (Under.mk g).hom) ≫ Under.Hom.right ((Under.pushout f).map (Under.homMk i₂ ⋯))) ≫
      Iso.hom (pushoutSymmetry (Under.mk g').hom f) ≫ Under.Hom.right ((Under.pushout g').map (Under.homMk i₁ ⋯)))
⊢ P (X := pushout f g) (Y := ((Under.pushout f).obj (Under.mk g')).right)
    (Iso.hom (pushoutSymmetry f (Under.mk g).hom) ≫ Under.Hom.right ((Under.pushout f).map (Under.homMk i₂ ⋯)))
have hf : P (X := pushout (Under.mk g).hom f) (Y := ((Under.pushout f).obj (Under.mk g')).right)
  (Under.Hom.right ((Under.pushout f).map (Under.homMk i₂ sorry)))
Tactic: rw [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.IsStableUnderCobaseChange
inst_2 : P.IsStableUnderComposition
S X X' Y Y' : C
f : S ⟶ X
g : S ⟶ Y
f' : S ⟶ X'
g' : S ⟶ Y'
i₁ : X ⟶ X'
inst_3 : HasPushoutsAlong f
inst_4 : HasPushoutsAlong g'
i₂ : Y ⟶ Y'
h₁ : P i₁
h₂ : P i₂
e₁ : f' = f ≫ i₁
e₂ : g' = g ≫ i₂
this_1 : HasPushoutsAlong (Under.mk g').hom
this :
  Eq (α := pushout f g ⟶ pushout f' g') (pushout.map f g f' g' i₁ i₂ (𝟙 S) ⋯ ⋯)
    ((Iso.hom (pushoutSymmetry f (Under.mk g).hom) ≫ Under.Hom.right ((Under.pushout f).map (Under.homMk i₂ ⋯))) ≫
      Iso.hom (pushoutSymmetry (Under.mk g').hom f) ≫ Under.Hom.right ((Under.pushout g').map (Under.homMk i₁ ⋯)))
⊢ P (X := ((Under.pushout f).obj (Under.mk g')).right) (Y := pushout f' g')
    (Iso.hom (pushoutSymmetry (Under.mk g').hom f) ≫ Under.Hom.right ((Under.pushout g').map (Under.homMk i₁ ⋯)))
have hg : P (X := pushout f (Under.mk g').hom) (Y := pushout f' g')
  (Under.Hom.right ((Under.pushout g').map (Under.homMk i₁ sorry)) :
    ((Under.pushout g').obj (Under.mk f)).right ⟶ ((Under.pushout g').obj (Under.mk f')).right)
Tactic: rw [P.cancel_left_of_respectsIso]