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
X Y Z : C
e : X ≅ Y
f : Y ⟶ Z
hf : P.universally f
X' Z' : C
i₁ : X' ⟶ X
i₂ : Z' ⟶ Z
f' : X' ⟶ Z'
H : IsPullback f' i₁ i₂ (e.hom ≫ f)
rw : i₁ = (i₁ ≫ e.hom) ≫ e.inv
rw₁ : i₁ = i₁ ≫ e.hom ≫ e.inv
rw₂ : i₁ = i₁ ≫ 𝟙 X
⊢ 𝟙 X' ≫ i₁ = (i₁ ≫ e.hom) ≫ e.inv
have rw₃ : i₁ = i₁
Tactic: rw [Category.id_comp, Category.assoc, e.hom_inv_id, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
X Y Z : C
e : X ≅ Y
f : Y ⟶ Z
hf : P.universally f
X' Z' : C
i₁ : X' ⟶ X
i₂ : Z' ⟶ Z
f' : X' ⟶ Z'
H : IsPullback f' i₁ i₂ (e.hom ≫ f)
⊢ P f'
have hprecomp : ∀ (this : IsPullback (𝟙 X') (i₁ ≫ e.hom) i₁ e.inv), P f'
Tactic: have : IsPullback (𝟙 _) (i₁ ≫ e.hom) i₁ e.inv :=
      IsPullback.of_horiz_isIso
        ⟨by rw [Category.id_comp, Category.assoc, e.hom_inv_id, Category.comp_id]⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
X Y Z : C
e : Y ≅ Z
f : X ⟶ Y
hf : P.universally f
X' Z' : C
i₁ : X' ⟶ X
i₂ : Z' ⟶ Z
f' : X' ⟶ Z'
H : IsPullback f' i₁ i₂ (f ≫ e.hom)
⊢ P f'
have hpostcomp : ∀ (this : IsPullback (𝟙 Z') i₂ (i₂ ≫ e.inv) e.inv), P f'
Tactic: have : IsPullback (𝟙 _) i₂ (i₂ ≫ e.inv) e.inv :=
      IsPullback.of_horiz_isIso ⟨Category.id_comp _⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
P : MorphismProperty.{v, u} C
hP : P.IsStableUnderComposition
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : P.universally f
hg : P.universally g
X' Z' : C
i₁ : X' ⟶ X
i₂ : Z' ⟶ Z
f' : X' ⟶ Z'
H : IsPullback f' i₁ i₂ (f ≫ g)
⊢ P f'
have have : ∀ (this : CategoryStruct.comp (Y := pullback i₂ g) (pullback.lift f' (i₁ ≫ f) sorry) (pullback.fst i₂ g) = f'), P f'
Tactic: have := pullback.lift_fst _ _ (H.w.trans (Category.assoc _ _ _).symm)
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
P : MorphismProperty.{v, u} C
hP : P.IsStableUnderComposition
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : P.universally f
hg : P.universally g
X' Z' : C
i₁ : X' ⟶ X
i₂ : Z' ⟶ Z
f' : X' ⟶ Z'
H : IsPullback f' i₁ i₂ (f ≫ g)
this : CategoryStruct.comp (Y := pullback i₂ g) (pullback.lift f' (i₁ ≫ f) ⋯) (pullback.fst i₂ g) = f'
⊢ P f'
have rw : ∀
  (H_1 :
    IsPullback (CategoryStruct.comp (Y := pullback i₂ g) (pullback.lift f' (i₁ ≫ f) sorry) (pullback.fst i₂ g)) i₁ i₂
      (f ≫ g))
  (this : CategoryStruct.comp (Y := pullback i₂ g) (pullback.lift f' (i₁ ≫ f) sorry) (pullback.fst i₂ g) = f'),
  P (CategoryStruct.comp (Y := pullback i₂ g) (pullback.lift f' (i₁ ≫ f) sorry) (pullback.fst i₂ g))
Tactic: rw [← this] at H ⊢
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
P : MorphismProperty.{v, u} C
hP : P.IsStableUnderComposition
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : P.universally f
hg : P.universally g
X' Z' : C
i₁ : X' ⟶ X
i₂ : Z' ⟶ Z
f' : X' ⟶ Z'
H_1 : IsPullback f' i₁ i₂ (f ≫ g)
H :
  IsPullback (CategoryStruct.comp (Y := pullback i₂ g) (pullback.lift f' (i₁ ≫ f) ⋯) (pullback.fst i₂ g)) i₁ i₂ (f ≫ g)
this : CategoryStruct.comp (Y := pullback i₂ g) (pullback.lift f' (i₁ ≫ f) ⋯) (pullback.fst i₂ g) = f'
⊢ P (CategoryStruct.comp (Y := pullback i₂ g) (pullback.lift f' (i₁ ≫ f) ⋯) (pullback.fst i₂ g))
have apply : P (Y := pullback i₂ g) (pullback.lift f' (i₁ ≫ f) sorry)
Tactic: apply P.comp_mem _ _ _ (hg _ _ _ <| IsPullback.of_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
X Y : C
f : X ⟶ Y
hf : P.universally f
⊢ f ≫ 𝟙 Y = 𝟙 X ≫ f
have rw : f = 𝟙 X ≫ f
Tactic: rw [Category.comp_id, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
X Y : C
f : X ⟶ Y
hf : P.universally f
rw : f = 𝟙 X ≫ f
⊢ f ≫ 𝟙 Y = 𝟙 X ≫ f
have rw₁ : f = f
Tactic: rw [Category.comp_id, Category.id_comp]
-- 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
⊢ (P ⊓ Q).universally = P.universally ⊓ Q.universally
have h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (P ⊓ Q).universally f ↔ (P.universally ⊓ Q.universally) f
Tactic: ext X Y f
-- 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
X Y : C
f : X ⟶ Y
⊢ (P ⊓ Q).universally f ↔ P.universally f ∧ Q.universally f
have h : (∀ ⦃X' Y' : C⦄ (i₁ : X' ⟶ X) (i₂ : Y' ⟶ Y) (f' : X' ⟶ Y'), IsPullback f' i₁ i₂ f → (P ⊓ Q) f') ↔
  ∀ (x x_1 : C) (x_2 : x ⟶ X) (x_3 : x_1 ⟶ Y) (x_4 : x ⟶ x_1) (x_5 : IsPullback x_4 x_2 x_3 f), P x_4 ∧ Q x_4
Tactic: simp_rw [universally, ← forall_and]
-- 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
X Y : C
g : X ⟶ Y
H : ∀ {T : C} (f : T ⟶ Y) [inst_2 : HasPullback f g], P (X := pullback f g) (pullback.fst f g)
X' Y' : C
i₁ : X' ⟶ X
i₂ : Y' ⟶ Y
f' : X' ⟶ Y'
h : IsPullback f' i₁ i₂ g
⊢ P f'
have have : ∀ (this : HasPullback i₂ g), P f'
Tactic: have := h.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
X Y : C
g : X ⟶ Y
H : ∀ {T : C} (f : T ⟶ Y) [inst_2 : HasPullback f g], P (X := pullback f g) (pullback.fst f g)
X' Y' : C
i₁ : X' ⟶ X
i₂ : Y' ⟶ Y
f' : X' ⟶ Y'
h : IsPullback f' i₁ i₂ g
this : HasPullback i₂ g
⊢ P f'
have rw : P (X := pullback i₂ g) (pullback.fst i₂ g)
Tactic: rw [← h.isoPullback_hom_fst, P.cancel_left_of_respectsIso]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Local (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
K : Precoverage.{v, u} C
inst_1 : K.HasPullbacks
inst_2 : P.IsLocalAtTarget K
X Y : C
f : X ⟶ Y
𝒰 : K.ZeroHypercover Y
X' : C
i : 𝒰.I₀
fst : X' ⟶ X
snd : X' ⟶ 𝒰.X i
h : IsPullback fst snd f (𝒰.f i)
hf : P f
⊢ P snd
have rw : P (X := pullback f (𝒰.f i)) (pullback.snd f (𝒰.f i))
Tactic: rw [← P.cancel_left_of_respectsIso h.isoPullback.inv, h.isoPullback_inv_snd]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Local (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
K : Precoverage.{v, u} C
inst_1 : K.HasPullbacks
inst_2 : P.IsLocalAtTarget K
X Y : C
f : X ⟶ Y
𝒰 : Precoverage.ZeroHypercover.{w, v, u} K Y
inst_3 : 𝒰.Small
h : ∀ (i : 𝒰.I₀), P (X := pullback f (𝒰.f i)) (pullback.snd f (𝒰.f i))
⊢ P f
have rw : ∀ (i : 𝒰.restrictIndexOfSmall.I₀),
  P (X := pullback f (𝒰.restrictIndexOfSmall.f i)) (pullback.snd f (𝒰.restrictIndexOfSmall.f i))
Tactic: rw [IsLocalAtTarget.iff_of_zeroHypercover (P := P) 𝒰.restrictIndexOfSmall]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Local (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
K : Precoverage.{v, u} C
inst_1 : P.IsLocalAtSource K
X Y : C
f : X ⟶ Y
𝒰 : Precoverage.ZeroHypercover.{w, v, u} K X
inst_2 : 𝒰.Small
h : ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ f)
⊢ P f
have rw : ∀ (i : 𝒰.restrictIndexOfSmall.I₀), P (𝒰.restrictIndexOfSmall.f i ≫ f)
Tactic: rw [IsLocalAtSource.iff_of_zeroHypercover (P := P) 𝒰.restrictIndexOfSmall]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Local (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasEqualizers.{v, u} C
inst_2 : HasPullbacks.{v, u} C
X Y S : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
J : Precoverage.{v, u} C
𝒰 : J.ZeroHypercover S
inst_3 : J.IsStableUnderBaseChange
inst_4 : MorphismProperty.IsLocalAtTarget (MorphismProperty.isomorphisms C) J
H :
  ∀ (i : 𝒰.I₀),
    Eq (α := pullback s (𝒰.f i) ⟶ pullback t (𝒰.f i)) (pullback.map s (𝒰.f i) t (𝒰.f i) f (𝟙 (𝒰.X i)) (𝟙 S) ⋯ ⋯)
      (pullback.map s (𝒰.f i) t (𝒰.f i) g (𝟙 (𝒰.X i)) (𝟙 S) ⋯ ⋯)
⊢ f = g
have suffices : IsIso (X := equalizer f g) (equalizer.ι f g)
Tactic: suffices IsIso (equalizer.ι f g) from Limits.eq_of_epi_equalizer
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Local (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasEqualizers.{v, u} C
inst_2 : HasPullbacks.{v, u} C
X Y S : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
J : Precoverage.{v, u} C
𝒰 : J.ZeroHypercover S
inst_3 : J.IsStableUnderBaseChange
inst_4 : MorphismProperty.IsLocalAtTarget (MorphismProperty.isomorphisms C) J
H :
  ∀ (i : 𝒰.I₀),
    Eq (α := pullback s (𝒰.f i) ⟶ pullback t (𝒰.f i)) (pullback.map s (𝒰.f i) t (𝒰.f i) f (𝟙 (𝒰.X i)) (𝟙 S) ⋯ ⋯)
      (pullback.map s (𝒰.f i) t (𝒰.f i) g (𝟙 (𝒰.X i)) (𝟙 S) ⋯ ⋯)
⊢ MorphismProperty.isomorphisms C (X := equalizer f g) (equalizer.ι f g)
have rw : ∀ (i : (Precoverage.ZeroHypercover.pullback₁ s 𝒰).I₀),
  MorphismProperty.isomorphisms C (X :=
    pullback (X := equalizer f g) (equalizer.ι f g) ((Precoverage.ZeroHypercover.pullback₁ s 𝒰).f i))
    (pullback.snd (equalizer.ι f g) ((Precoverage.ZeroHypercover.pullback₁ s 𝒰).f i))
Tactic: rw [(MorphismProperty.isomorphisms C).iff_of_zeroHypercover_target (𝒰.pullback₁ s)]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Local (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasEqualizers.{v, u} C
inst_2 : HasPullbacks.{v, u} C
X Y S : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
J : Precoverage.{v, u} C
𝒰 : J.ZeroHypercover S
inst_3 : J.IsStableUnderBaseChange
inst_4 : MorphismProperty.IsLocalAtTarget (MorphismProperty.isomorphisms C) J
H :
  ∀ (i : 𝒰.I₀),
    Eq (α := pullback s (𝒰.f i) ⟶ pullback t (𝒰.f i)) (pullback.map s (𝒰.f i) t (𝒰.f i) f (𝟙 (𝒰.X i)) (𝟙 S) ⋯ ⋯)
      (pullback.map s (𝒰.f i) t (𝒰.f i) g (𝟙 (𝒰.X i)) (𝟙 S) ⋯ ⋯)
i : (Precoverage.ZeroHypercover.pullback₁ s 𝒰).I₀
⊢ MorphismProperty.isomorphisms C (X :=
    pullback (X := equalizer f g) (equalizer.ι f g) ((Precoverage.ZeroHypercover.pullback₁ s 𝒰).f i))
    (pullback.snd (equalizer.ι f g) ((Precoverage.ZeroHypercover.pullback₁ s 𝒰).f i))
have this : Eq (α :=
  pullback (X := equalizer f g) (Y := pullback s (𝒰.f i)) (equalizer.ι f g) (pullback.fst s (𝒰.f i)) ⟶
    pullback s (𝒰.f i))
  (pullback.snd (equalizer.ι f g) (pullback.fst s (𝒰.f i)) :
    pullback (X := equalizer f g) (Y := pullback s (𝒰.f i)) (equalizer.ι f g) (pullback.fst s (𝒰.f i)) ⟶
      pullback s (𝒰.f i))
  (CategoryStruct.comp (Y :=
      equalizer (X := pullback s (𝒰.f i)) (Y := pullback t (𝒰.f i))
        (pullback.map s (𝒰.f i) t (𝒰.f i) f (𝟙 (𝒰.X i)) (𝟙 S) sorry sorry)
        (pullback.map s (𝒰.f i) t (𝒰.f i) g (𝟙 (𝒰.X i)) (𝟙 S) sorry sorry))
      (Iso.inv (equalizerPullbackMapIso hf hg (𝒰.f i)) :
        pullback (X := equalizer f g) (Y := pullback s (𝒰.f i)) (equalizer.ι f g) (pullback.fst s (𝒰.f i)) ⟶
          equalizer (X := pullback s (𝒰.f i)) (Y := pullback t (𝒰.f i))
            (pullback.map s (𝒰.f i) t (𝒰.f i) f (𝟙 (𝒰.X i)) (𝟙 S) sorry sorry)
            (pullback.map s (𝒰.f i) t (𝒰.f i) g (𝟙 (𝒰.X i)) (𝟙 S) sorry sorry))
      (equalizer.ι (pullback.map s (𝒰.f i) t (𝒰.f i) f (𝟙 (𝒰.X i)) (𝟙 S) sorry sorry)
          (pullback.map s (𝒰.f i) t (𝒰.f i) g (𝟙 (𝒰.X i)) (𝟙 S) sorry sorry) :
        equalizer (X := pullback s (𝒰.f i)) (Y := pullback t (𝒰.f i))
            (pullback.map s (𝒰.f i) t (𝒰.f i) f (𝟙 (𝒰.X i)) (𝟙 S) sorry sorry)
            (pullback.map s (𝒰.f i) t (𝒰.f i) g (𝟙 (𝒰.X i)) (𝟙 S) sorry sorry) ⟶
          pullback s (𝒰.f i)) :
    pullback (X := equalizer f g) (Y := pullback s (𝒰.f i)) (equalizer.ι f g) (pullback.fst s (𝒰.f i)) ⟶
      pullback s (𝒰.f i))
Tactic: have : pullback.snd (equalizer.ι f g) (pullback.fst s (𝒰.f i)) =
      (equalizerPullbackMapIso hf hg _).inv ≫ equalizer.ι _ _ := by
    ext <;> simp [pullback.condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.OfObjectProperty (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P Q P' : ObjectProperty.{v_1, u_1} C
h : P ≤ P'
X Y : C
f : X ⟶ Y
⊢ ofObjectProperty P Q f → ofObjectProperty P' Q f
have this : ∀ (hX : P X) (hY : Q Y), ofObjectProperty P' Q f
Tactic: ⟨hX, hY⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.OfObjectProperty (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P Q Q' : ObjectProperty.{v_1, u_1} C
h : Q ≤ Q'
X Y : C
f : X ⟶ Y
⊢ ofObjectProperty P Q f → ofObjectProperty P Q' f
have this : ∀ (hX : P X) (hY : Q Y), ofObjectProperty P Q' f
Tactic: ⟨hX, hY⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.OfObjectProperty (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P Q : ObjectProperty.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
X Y : D
f : X ⟶ Y
⊢ (ofObjectProperty P Q).map F f → ofObjectProperty (P.map F) (Q.map F) f
have this : ∀ (X' Y' : C) (f' : X' ⟶ Y') (hX' : P X') (hY' : Q Y') (i : Arrow.mk (F.map f') ≅ Arrow.mk f),
  ofObjectProperty (P.map F) (Q.map F) f
Tactic: ⟨X', Y', f', ⟨hX', hY'⟩, ⟨i⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.OfObjectProperty (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P Q : ObjectProperty.{v_1, u_1} C
inst_1 : P.IsClosedUnderIsomorphisms
X Y Z : C
i : X ⟶ Y
hi : isomorphisms C i
f : Y ⟶ Z
⊢ ∀ (hf : ofObjectProperty P Q f), ofObjectProperty P Q (i ≫ f)
have this : ∀ (hY : P Y) (hZ : Q Z), ofObjectProperty P Q (i ≫ f)
Tactic: ⟨hY, hZ⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.OfObjectProperty (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P Q : ObjectProperty.{v_1, u_1} C
inst_1 : P.IsClosedUnderIsomorphisms
X Y Z : C
i : X ⟶ Y
hi : isomorphisms C i
f : Y ⟶ Z
hY : P Y
hZ : Q Z
⊢ ofObjectProperty P Q (i ≫ f)
have rw : ∀ (hi : IsIso i) (f : Y ⟶ Z) (hY : P Y) (hZ : Q Z), ofObjectProperty P Q (i ≫ f)
Tactic: rw [isomorphisms.iff] at hi
Cleared hypotheses: hi, f, hY, hZ
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.OfObjectProperty (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P Q : ObjectProperty.{v_1, u_1} C
inst_1 : Q.IsClosedUnderIsomorphisms
X Y Z : C
i : Y ⟶ Z
hi : isomorphisms C i
f : X ⟶ Y
⊢ ∀ (hf : ofObjectProperty P Q f), ofObjectProperty P Q (f ≫ i)
have this : ∀ (hY : P X) (hZ : Q Y), ofObjectProperty P Q (f ≫ i)
Tactic: ⟨hY, hZ⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.OfObjectProperty (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P Q : ObjectProperty.{v_1, u_1} C
inst_1 : Q.IsClosedUnderIsomorphisms
X Y Z : C
i : Y ⟶ Z
hi : isomorphisms C i
f : X ⟶ Y
hY : P X
hZ : Q Y
⊢ ofObjectProperty P Q (f ≫ i)
have rw : ∀ (hi : IsIso i) (f : X ⟶ Y) (hY : P X) (hZ : Q Y), ofObjectProperty P Q (f ≫ i)
Tactic: rw [isomorphisms.iff] at hi
Cleared hypotheses: hi, f, hY, hZ
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.OverAdjunction (goal)
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
P Q : MorphismProperty.{v_1, u_1} T
inst_1 : Q.IsMultiplicative
X Y Z : T
inst_2 : P.IsStableUnderComposition
f : X ⟶ Y
hf : P f
g : Y ⟶ Z
hg : P g
⊢ Eq (α := P.Over Q X ⥤ P.Over Q Z) (map (P := P) Q ⋯) (map (P := P) Q hf ⋙ map (P := P) Q hg)
have h_obj : ∀ (X_1 : P.Over Q X), Functor.obj (map (P := P) Q sorry) X_1 = Functor.obj (map (P := P) Q hf ⋙ map (P := P) Q hg) X_1
Tactic: fapply Functor.ext
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.OverAdjunction (goal)
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
P Q : MorphismProperty.{v_1, u_1} T
inst_1 : Q.IsMultiplicative
X Y Z : T
inst_2 : P.IsStableUnderComposition
f : X ⟶ Y
hf : P f
g : Y ⟶ Z
hg : P g
h_obj :
  ∀ (X_1 : P.Over Q X), Functor.obj (map (P := P) Q ⋯) X_1 = Functor.obj (map (P := P) Q hf ⋙ map (P := P) Q hg) X_1
⊢ Eq (α := P.Over Q X ⥤ P.Over Q Z) (map (P := P) Q ⋯) (map (P := P) Q hf ⋙ map (P := P) Q hg)
have h_map : autoParam
  (∀ (X_1 Y_1 : P.Over Q X) (f_1 : X_1 ⟶ Y_1),
    Eq (α := Functor.obj (map (P := P) Q sorry) X_1 ⟶ Functor.obj (map (P := P) Q sorry) Y_1)
      (Functor.map (map (P := P) Q sorry) f_1)
      (CategoryStruct.comp (Y := Functor.obj (map (P := P) Q hf ⋙ map (P := P) Q hg) X_1) (eqToHom sorry)
        (Functor.map (map (P := P) Q hf ⋙ map (P := P) Q hg) f_1 ≫ eqToHom sorry)))
  Functor.ext._auto_1
Tactic: fapply Functor.ext
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.OverAdjunction (goal)
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
P Q : MorphismProperty.{v_1, u_1} T
inst_1 : Q.IsMultiplicative
X Y Z : T
inst_2 : P.IsStableUnderComposition
f : X ⟶ Y
hf : P f
g : Y ⟶ Z
hg : P g
U V : P.Over Q X
k : U ⟶ V
⊢ Eq (α := Functor.obj (map (P := P) Q ⋯) U ⟶ Functor.obj (map (P := P) Q ⋯) V) (Functor.map (map (P := P) Q ⋯) k)
    (CategoryStruct.comp (Y := Functor.obj (map (P := P) Q hf ⋙ map (P := P) Q hg) U) (eqToHom ⋯)
      (Functor.map (map (P := P) Q hf ⋙ map (P := P) Q hg) k ≫ eqToHom ⋯))
have h_map : Eq (α :=
  (Functor.obj (map (P := P) Q sorry) U).toComma (P := P) (Q := Q) (W := ⊤).left ⟶
    (Functor.obj (map (P := P) Q sorry) V).toComma (P := P) (Q := Q) (W := ⊤).left)
  (CommaMorphism.left (Comma.Hom.toCommaMorphism (P := P) (Q := Q) (W := ⊤) (Functor.map (map (P := P) Q sorry) k)))
  (CommaMorphism.left
    (Comma.Hom.toCommaMorphism (P := P) (Q := Q) (W := ⊤)
      (CategoryStruct.comp (Y := Functor.obj (map (P := P) Q hf ⋙ map (P := P) Q hg) U) (eqToHom sorry)
        (Functor.map (map (P := P) Q hf ⋙ map (P := P) Q hg) k ≫ eqToHom sorry))))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.OverAdjunction (goal)
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
P Q : MorphismProperty.{v_1, u_1} T
inst_1 : Q.IsMultiplicative
X_1 Y Z : T
inst_2 : P.IsStableUnderComposition
inst_3 : P.IsMultiplicative
inst_4 : Q.RespectsIso
X : T
f : optParam (X ⟶ X) (𝟙 X)
hf : autoParam (f = 𝟙 X) mapId._auto_1
⊢ P f
have subst : P (𝟙 X)
Tactic: subst hf
Cleared hypotheses: f, hf
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.OverAdjunction (goal)
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
P Q : MorphismProperty.{v_1, u_1} T
inst_1 : Q.IsMultiplicative
X Y Z : T
inst_2 : P.IsStableUnderComposition
f : X ⟶ Y
hf : P f
g : Y ⟶ Z
hg : P g
inst_3 : Q.RespectsIso
fg : optParam (X ⟶ Z) (f ≫ g)
hfg : autoParam (fg = f ≫ g) mapComp._auto_1
⊢ P fg
have subst : P (f ≫ g)
Tactic: subst hfg
Cleared hypotheses: fg, hfg
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.OverAdjunction (goal)
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
P Q : MorphismProperty.{v_1, u_1} T
inst_1 : Q.IsMultiplicative
X Y Z : T
f : X ⟶ Y
g : Y ⟶ Z
inst_2 : P.IsStableUnderBaseChangeAlong f
inst_3 : P.IsStableUnderBaseChangeAlong g
inst_4 : P.HasPullbacksAlong f
inst_5 : P.HasPullbacksAlong g
inst_6 : Q.RespectsIso
inst_7 : Q.IsStableUnderBaseChange
fg : optParam (X ⟶ Z) (f ≫ g)
hfg : autoParam (fg = f ≫ g) pullbackComp._auto_1
⊢ P.HasPullbacksAlong fg
have subst : P.HasPullbacksAlong (f ≫ g)
Tactic: subst hfg
Cleared hypotheses: fg, hfg
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.OverAdjunction (goal)
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
P Q : MorphismProperty.{v_1, u_1} T
inst_1 : Q.IsMultiplicative
X Y Z : T
f : X ⟶ Y
g : Y ⟶ Z
inst_2 : P.IsStableUnderBaseChangeAlong f
inst_3 : P.IsStableUnderBaseChangeAlong g
inst_4 : P.HasPullbacksAlong f
inst_5 : P.HasPullbacksAlong g
inst_6 : Q.RespectsIso
inst_7 : Q.IsStableUnderBaseChange
fg : optParam (X ⟶ Z) (f ≫ g)
hfg : autoParam (fg = f ≫ g) pullbackComp._auto_1
this : P.HasPullbacksAlong fg
⊢ P.IsStableUnderBaseChangeAlong fg
have subst : ∀ (this : P.HasPullbacksAlong (f ≫ g)), P.IsStableUnderBaseChangeAlong (f ≫ g)
Tactic: subst hfg
Cleared hypotheses: fg, hfg, this
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.OverAdjunction (goal)
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
P Q : MorphismProperty.{v_1, u_1} T
inst_1 : Q.IsMultiplicative
X Y Z : T
f : X ⟶ Y
g : Y ⟶ Z
inst_2 : P.IsStableUnderBaseChangeAlong f
inst_3 : P.IsStableUnderBaseChangeAlong g
inst_4 : P.HasPullbacksAlong f
inst_5 : P.HasPullbacksAlong g
inst_6 : Q.RespectsIso
inst_7 : Q.IsStableUnderBaseChange
fg : X ⟶ Z
hfg : fg = f ≫ g
⊢ P.HasPullbacksAlong fg
have subst : P.HasPullbacksAlong (f ≫ g)
Tactic: subst hfg
Cleared hypotheses: fg, hfg
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.OverAdjunction (goal)
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
P Q : MorphismProperty.{v_1, u_1} T
inst_1 : Q.IsMultiplicative
X Y Z : T
f : X ⟶ Y
inst_2 : P.HasPullbacksAlong f
inst_3 : P.IsStableUnderBaseChangeAlong f
inst_4 : Q.IsStableUnderBaseChange
g : X ⟶ Y
h : f = g
this : P.HasPullbacksAlong g
⊢ P.IsStableUnderBaseChangeAlong g
have subst : ∀ (this : P.HasPullbacksAlong f), P.IsStableUnderBaseChangeAlong f
Tactic: subst h
Cleared hypotheses: g, h, this
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.OverAdjunction (goal)
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
P Q : MorphismProperty.{v_1, u_1} T
inst_1 : Q.IsMultiplicative
X Y : T
f : X ⟶ Y
inst_2 : P.HasPullbacksAlong f
g : X ⟶ Y
inst_3 : P.IsStableUnderBaseChangeAlong f
inst_4 : Q.IsStableUnderBaseChange
h : f = g
A : P.Over Q Y
⊢ Eq (α :=
    (Functor.obj (pullback P Q f) A).toComma (P := P) (Q := Q) (W := ⊤).left ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 T) A.toComma (P := P) (Q := Q) (W := ⊤).left)
    (CommaMorphism.left
        (Comma.Hom.toCommaMorphism (P := P) (Q := Q) (W := ⊤)
          (NatTrans.app (Iso.hom (pullbackCongr (P := P) (Q := Q) h)) A)) ≫
      pullback.fst A.toComma (P := P) (Q := Q) (W := ⊤).hom g)
    (pullback.fst A.toComma (P := P) (Q := Q) (W := ⊤).hom f)
have subst : Eq (α :=
  (Functor.obj (pullback P Q f) A).toComma (P := P) (Q := Q) (W := ⊤).left ⟶
    Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 T) A.toComma (P := P) (Q := Q) (W := ⊤).left)
  (CommaMorphism.left
      (Comma.Hom.toCommaMorphism (P := P) (Q := Q) (W := ⊤)
        (NatTrans.app (Iso.hom (pullbackCongr (P := P) (Q := Q) sorry)) A)) ≫
    pullback.fst A.toComma (P := P) (Q := Q) (W := ⊤).hom f)
  (pullback.fst A.toComma (P := P) (Q := Q) (W := ⊤).hom f)
Tactic: subst h
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.OverAdjunction (goal)
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
P Q : MorphismProperty.{v_1, u_1} T
inst_1 : Q.IsMultiplicative
X_1 Y_1 Z_1 : T
inst_2 : P.IsStableUnderComposition
X Y Z : T
f : X ⟶ Y
hPf : P f
hQf : Q f
g : Y ⟶ Z
inst_3 : P.IsStableUnderBaseChangeAlong f
inst_4 : P.IsStableUnderBaseChangeAlong g
inst_5 : Q.IsStableUnderBaseChange
inst_6 : HasPullbacks.{v_1, u_1} T
fg : optParam (X ⟶ Z) (f ≫ g)
hfg : autoParam (f ≫ g = fg) pullbackMapHomPullback._auto_1
⊢ P.IsStableUnderBaseChangeAlong fg
have subst : P.IsStableUnderBaseChangeAlong (f ≫ g)
Tactic: subst hfg
Cleared hypotheses: fg, hfg
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.OverAdjunction (goal)
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
P Q : MorphismProperty.{v_1, u_1} T
inst_1 : Q.IsMultiplicative
X Y Z : T
inst_2 : P.IsStableUnderComposition
inst_3 : Q.IsStableUnderBaseChange
f : X ⟶ Y
inst_4 : P.HasPullbacksAlong f
inst_5 : P.IsStableUnderBaseChangeAlong f
inst_6 : Q.HasOfPostcompProperty Q
hPf : P f
hQf : Q f
A : P.Over Q X
⊢ Q (Y := (Functor.obj (map (P := P) Q hPf ⋙ pullback P Q f) A).toComma (P := P) (Q := Q) (W := ⊤).left)
    (pullback.lift (𝟙 (Functor.obj (𝟭 (P.Over Q X)) A).toComma (P := P) (Q := Q) (W := ⊤).left)
      A.toComma (P := P) (Q := Q) (W := ⊤).hom ⋯)
have hg : Q (X := (Functor.obj (map (P := P) Q hPf ⋙ pullback P Q f) A).toComma (P := P) (Q := Q) (W := ⊤).left)
  (pullback.fst (Functor.obj (map (P := P) Q hPf) A).toComma (P := P) (Q := Q) (W := ⊤).hom f)
Tactic: apply Q.of_postcomp (W' := Q)