awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.MorphismProperty.Local
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₀
⊢ 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) ⋯ ⋯)
          (pullback.map s (𝒰.f i) t (𝒰.f i) g (𝟙 (𝒰.X i)) (𝟙 S) ⋯ ⋯))
        (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) ⋯ ⋯)
              (pullback.map s (𝒰.f i) t (𝒰.f i) g (𝟙 (𝒰.X i)) (𝟙 S) ⋯ ⋯))
        (equalizer.ι (pullback.map s (𝒰.f i) t (𝒰.f i) f (𝟙 (𝒰.X i)) (𝟙 S) ⋯ ⋯)
            (pullback.map s (𝒰.f i) t (𝒰.f i) g (𝟙 (𝒰.X i)) (𝟙 S) ⋯ ⋯) :
          equalizer (X := pullback s (𝒰.f i)) (Y := 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) ⋯ ⋯) ⟶
            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]
-- Module: Mathlib.CategoryTheory.MorphismProperty.Local
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₀
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) ⋯ ⋯)
          (pullback.map s (𝒰.f i) t (𝒰.f i) g (𝟙 (𝒰.X i)) (𝟙 S) ⋯ ⋯))
        (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) ⋯ ⋯)
              (pullback.map s (𝒰.f i) t (𝒰.f i) g (𝟙 (𝒰.X i)) (𝟙 S) ⋯ ⋯))
        (equalizer.ι (pullback.map s (𝒰.f i) t (𝒰.f i) f (𝟙 (𝒰.X i)) (𝟙 S) ⋯ ⋯)
            (pullback.map s (𝒰.f i) t (𝒰.f i) g (𝟙 (𝒰.X i)) (𝟙 S) ⋯ ⋯) :
          equalizer (X := pullback s (𝒰.f i)) (Y := 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) ⋯ ⋯) ⟶
            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))
⊢ 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:
simpa [this] using equalizer.ι_of_eq (H i)

Premises used: CategoryTheory.Limits.equalizer.ι_of_eq
-- Module: Mathlib.CategoryTheory.MorphismProperty.OfObjectProperty
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P Q : ObjectProperty.{v_1, u_1} C
X Y : C
f : X ⟶ Y
⊢ ofObjectProperty P Q f ↔ P X ∧ Q Y

Tactic:
Iff.rfl

Premises used: CategoryTheory.MorphismProperty.ofObjectProperty, Iff.rfl
-- Module: Mathlib.CategoryTheory.MorphismProperty.OfObjectProperty
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 : C
_ : ∀ ⦃Y : C⦄ (f : X ⟶ Y), ofObjectProperty P Q f → ofObjectProperty P' Q f
⊢ ∀ ⦃Y : C⦄ (f : X ⟶ Y), ofObjectProperty P Q f → ofObjectProperty P' Q f

Tactic:
_
-- Module: Mathlib.CategoryTheory.MorphismProperty.OfObjectProperty
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
⊢ ∀ (f : X ⟶ Y), ofObjectProperty P Q f → ofObjectProperty P' Q f

Tactic:
_
-- Module: Mathlib.CategoryTheory.MorphismProperty.OfObjectProperty
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
this : ∀ (hX : P X) (hY : Q Y), ofObjectProperty P' Q f
⊢ ofObjectProperty P Q f → ofObjectProperty P' Q f

Tactic:
⟨hX, hY⟩
-- Module: Mathlib.CategoryTheory.MorphismProperty.OfObjectProperty
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
hX : P X
hY : Q Y
⊢ ofObjectProperty P' Q f

Tactic:
⟨h _ hX, hY⟩

Premises used: CategoryTheory.MorphismProperty.ofObjectProperty, And.intro
-- Module: Mathlib.CategoryTheory.MorphismProperty.OfObjectProperty
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
hX : P X
hY : Q Y
⊢ ofObjectProperty P' Q f

Tactic:
exact ⟨h _ hX, hY⟩
-- Module: Mathlib.CategoryTheory.MorphismProperty.OfObjectProperty
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 : C
_ : ∀ ⦃Y : C⦄ (f : X ⟶ Y), ofObjectProperty P Q f → ofObjectProperty P Q' f
⊢ ∀ ⦃Y : C⦄ (f : X ⟶ Y), ofObjectProperty P Q f → ofObjectProperty P Q' f

Tactic:
_
-- Module: Mathlib.CategoryTheory.MorphismProperty.OfObjectProperty
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
⊢ ∀ (f : X ⟶ Y), ofObjectProperty P Q f → ofObjectProperty P Q' f

Tactic:
_
-- Module: Mathlib.CategoryTheory.MorphismProperty.OfObjectProperty
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
this : ∀ (hX : P X) (hY : Q Y), ofObjectProperty P Q' f
⊢ ofObjectProperty P Q f → ofObjectProperty P Q' f

Tactic:
⟨hX, hY⟩
-- Module: Mathlib.CategoryTheory.MorphismProperty.OfObjectProperty
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
hX : P X
hY : Q Y
⊢ ofObjectProperty P Q' f

Tactic:
⟨hX, h _ hY⟩

Premises used: CategoryTheory.MorphismProperty.ofObjectProperty, And.intro
-- Module: Mathlib.CategoryTheory.MorphismProperty.OfObjectProperty
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
hX : P X
hY : Q Y
⊢ ofObjectProperty P Q' f

Tactic:
exact ⟨hX, h _ hY⟩
-- Module: Mathlib.CategoryTheory.MorphismProperty.OfObjectProperty
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_2, v_1, u_2, u_1} D C
⊢ ofObjectProperty (P.inverseImage F) (Q.inverseImage F) = (ofObjectProperty P Q).inverseImage F

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.MorphismProperty.OfObjectProperty
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
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
⊢ (ofObjectProperty P Q).map F f → ofObjectProperty (P.map F) (Q.map F) f

Tactic:
⟨X', Y', f', ⟨hX', hY'⟩, ⟨i⟩⟩
-- Module: Mathlib.CategoryTheory.MorphismProperty.OfObjectProperty
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
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', hX', ⟨Comma.leftIso i⟩⟩, ⟨Y', hY', ⟨Comma.rightIso i⟩⟩⟩

Premises used: CategoryTheory.MorphismProperty.ofObjectProperty, CategoryTheory.Comma.leftIso, CategoryTheory.Comma.rightIso, Nonempty.intro, And.intro, Exists.intro
-- Module: Mathlib.CategoryTheory.MorphismProperty.OfObjectProperty
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
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:
exact ⟨⟨X', hX', ⟨Comma.leftIso i⟩⟩, ⟨Y', hY', ⟨Comma.rightIso i⟩⟩⟩
-- Module: Mathlib.CategoryTheory.MorphismProperty.OfObjectProperty
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
this : ∀ (hY : P Y) (hZ : Q Z), ofObjectProperty P Q (i ≫ f)
⊢ ∀ (hf : ofObjectProperty P Q f), ofObjectProperty P Q (i ≫ f)

Tactic:
⟨hY, hZ⟩
-- Module: Mathlib.CategoryTheory.MorphismProperty.OfObjectProperty
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
rw : ∀ (hi : IsIso i) (f : Y ⟶ Z) (hY : P Y) (hZ : Q Z), ofObjectProperty P Q (i ≫ f)
⊢ ofObjectProperty P Q (i ≫ f)

Tactic:
rw [isomorphisms.iff] at hi

Premises used: CategoryTheory.MorphismProperty.isomorphisms.iff
-- Module: Mathlib.CategoryTheory.MorphismProperty.OfObjectProperty
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 : IsIso i
f : Y ⟶ Z
hY : P Y
hZ : Q Z
⊢ ofObjectProperty P Q (i ≫ f)

Tactic:
⟨(P.prop_iff_of_isIso i).mpr hY, hZ⟩

Premises used: CategoryTheory.ObjectProperty.prop_iff_of_isIso, Iff.mpr, CategoryTheory.MorphismProperty.ofObjectProperty, And.intro
-- Module: Mathlib.CategoryTheory.MorphismProperty.OfObjectProperty
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 : IsIso i
f : Y ⟶ Z
hY : P Y
hZ : Q Z
⊢ ofObjectProperty P Q (i ≫ f)

Tactic:
exact ⟨(P.prop_iff_of_isIso i).mpr hY, hZ⟩
-- Module: Mathlib.CategoryTheory.MorphismProperty.OfObjectProperty
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
this : ∀ (hY : P X) (hZ : Q Y), ofObjectProperty P Q (f ≫ i)
⊢ ∀ (hf : ofObjectProperty P Q f), ofObjectProperty P Q (f ≫ i)

Tactic:
⟨hY, hZ⟩
-- Module: Mathlib.CategoryTheory.MorphismProperty.OfObjectProperty
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
rw : ∀ (hi : IsIso i) (f : X ⟶ Y) (hY : P X) (hZ : Q Y), ofObjectProperty P Q (f ≫ i)
⊢ ofObjectProperty P Q (f ≫ i)

Tactic:
rw [isomorphisms.iff] at hi

Premises used: CategoryTheory.MorphismProperty.isomorphisms.iff
-- Module: Mathlib.CategoryTheory.MorphismProperty.OfObjectProperty
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 : IsIso i
f : X ⟶ Y
hY : P X
hZ : Q Y
⊢ ofObjectProperty P Q (f ≫ i)

Tactic:
⟨hY, (Q.prop_iff_of_isIso i).mp hZ⟩

Premises used: CategoryTheory.ObjectProperty.prop_iff_of_isIso, CategoryTheory.MorphismProperty.ofObjectProperty, And.intro, Iff.mp
-- Module: Mathlib.CategoryTheory.MorphismProperty.OfObjectProperty
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 : IsIso i
f : X ⟶ Y
hY : P X
hZ : Q Y
⊢ ofObjectProperty P Q (f ≫ i)

Tactic:
exact ⟨hY, (Q.prop_iff_of_isIso i).mp hZ⟩
-- Module: Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
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
h_map :
  autoParam
    (∀ (X_1 Y_1 : P.Over Q X) (f_1 : X_1 ⟶ Y_1),
      Eq (α := Functor.obj (map (P := P) Q ⋯) X_1 ⟶ Functor.obj (map (P := P) Q ⋯) Y_1)
        (Functor.map (map (P := P) Q ⋯) f_1)
        (CategoryStruct.comp (Y := Functor.obj (map (P := P) Q hf ⋙ map (P := P) Q hg) X_1) (eqToHom ⋯)
          (Functor.map (map (P := P) Q hf ⋙ map (P := P) Q hg) f_1 ≫ eqToHom ⋯)))
    Functor.ext._auto_1
⊢ Eq (α := P.Over Q X ⥤ P.Over Q Z) (map (P := P) Q ⋯) (map (P := P) Q hf ⋙ map (P := P) Q hg)

Tactic:
fapply Functor.ext

Premises used: CategoryTheory.Functor.ext
-- Module: Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
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
⊢ ∀ (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

Tactic:
simp [map, Comma.mapRight, CategoryTheory.Comma.mapRight, Comma.lift]

Premises used: CategoryTheory.MorphismProperty.Over.map, CategoryTheory.Comma.mapRight, CategoryTheory.MorphismProperty.Comma.mapRight, CategoryTheory.MorphismProperty.Comma.lift
-- Module: Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
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
h_map :
  Eq (α :=
    (Functor.obj (map (P := P) Q ⋯) U).toComma (P := P) (Q := Q) (W := ⊤).left ⟶
      (Functor.obj (map (P := P) Q ⋯) V).toComma (P := P) (Q := Q) (W := ⊤).left)
    (CommaMorphism.left (Comma.Hom.toCommaMorphism (P := P) (Q := Q) (W := ⊤) (Functor.map (map (P := P) Q ⋯) 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 ⋯)
          (Functor.map (map (P := P) Q hf ⋙ map (P := P) Q hg) k ≫ eqToHom ⋯))))
⊢ 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 ⋯))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
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).toComma (P := P) (Q := Q) (W := ⊤).left ⟶
      (Functor.obj (map (P := P) Q ⋯) V).toComma (P := P) (Q := Q) (W := ⊤).left)
    (CommaMorphism.left (Comma.Hom.toCommaMorphism (P := P) (Q := Q) (W := ⊤) (Functor.map (map (P := P) Q ⋯) 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 ⋯)
          (Functor.map (map (P := P) Q hf ⋙ map (P := P) Q hg) k ≫ eqToHom ⋯))))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
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
subst : P (𝟙 X)
⊢ P f

Tactic:
subst hf
-- Module: Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
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
⊢ P (𝟙 X)

Tactic:
P.id_mem X

Premises used: CategoryTheory.MorphismProperty.id_mem
-- Module: Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
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
⊢ P (𝟙 X)

Tactic:
exact P.id_mem X

Premises used: CategoryTheory.MorphismProperty.id_mem
-- Module: Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
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
subst : P (f ≫ g)
⊢ P fg

Tactic:
subst hfg
-- Module: Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
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
⊢ P (f ≫ g)

Tactic:
P.comp_mem f g hf hg

Premises used: CategoryTheory.MorphismProperty.comp_mem
-- Module: Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
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
⊢ P (f ≫ g)

Tactic:
exact P.comp_mem f g hf hg

Premises used: CategoryTheory.MorphismProperty.comp_mem
-- Module: Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
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
A : P.Over Q Y
⊢ HasPullback A.toComma (P := P) (Q := Q) (W := ⊤).hom f

Tactic:
HasPullbacksAlong.hasPullback A.hom A.prop

Premises used: CategoryTheory.Comma.hom, CategoryTheory.MorphismProperty.Comma.toComma, CategoryTheory.MorphismProperty.Comma.prop, CategoryTheory.MorphismProperty.HasPullbacksAlong.hasPullback
-- Module: Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
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 X Y Z : T
f : X ⟶ Y
g : Y ⟶ Z
inst_2 : P.HasPullbacksAlong f
inst_3 : P.HasPullbacksAlong g
inst_4 : P.IsStableUnderBaseChangeAlong g
A : P.Over Q Z
⊢ HasPullback (X := pullback A.toComma (P := P) (Q := Q) (W := ⊤).hom g)
    (pullback.snd A.toComma (P := P) (Q := Q) (W := ⊤).hom g) f

Tactic:
HasPullbacksAlong.hasPullback (pullback.snd A.hom g)
  (IsStableUnderBaseChangeAlong.of_isPullback (IsPullback.of_hasPullback A.hom g) A.prop)

Premises used: CategoryTheory.Limits.pullback.snd, CategoryTheory.Comma.hom, CategoryTheory.MorphismProperty.IsStableUnderBaseChangeAlong.of_isPullback, CategoryTheory.MorphismProperty.Comma.toComma, CategoryTheory.MorphismProperty.Comma.prop, CategoryTheory.IsPullback.of_hasPullback, CategoryTheory.MorphismProperty.HasPullbacksAlong.hasPullback
-- Module: Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
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
A B : P.Over Q Y
g : A ⟶ B
⊢ Eq (α :=
    (Over.mk (P := P) Q (A := Limits.pullback A.toComma (P := P) (Q := Q) (W := ⊤).hom f)
              (pullback.snd A.toComma (P := P) (Q := Q) (W := ⊤).hom f) ⋯).toComma
          (P := P) (Q := Q) (W := ⊤).left ⟶
      Functor.obj.{0, v_1, 0, u_1} (Functor.fromPUnit Y) B.toComma (P := P) (Q := Q) (W := ⊤).right)
    ((pullback.fst A.toComma (P := P) (Q := Q) (W := ⊤).hom f ≫ g.toCommaMorphism (P := P) (Q := Q) (W := ⊤).left) ≫
      B.toComma (P := P) (Q := Q) (W := ⊤).hom)
    (pullback.snd A.toComma (P := P) (Q := Q) (W := ⊤).hom f ≫ f)

Tactic:
simp [pullback.condition]

Premises used: CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
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
A B : P.Over Q Y
g : A ⟶ B
⊢ pullback.lift
        (pullback.fst A.toComma (P := P) (Q := Q) (W := ⊤).hom f ≫ g.toCommaMorphism (P := P) (Q := Q) (W := ⊤).left)
        (pullback.snd A.toComma (P := P) (Q := Q) (W := ⊤).hom f) ⋯ ≫
      (Over.mk (P := P) Q (A := Limits.pullback B.toComma (P := P) (Q := Q) (W := ⊤).hom f)
              (pullback.snd B.toComma (P := P) (Q := Q) (W := ⊤).hom f) ⋯).toComma
          (P := P) (Q := Q) (W := ⊤).hom =
    (Over.mk (P := P) Q (A := Limits.pullback A.toComma (P := P) (Q := Q) (W := ⊤).hom f)
            (pullback.snd A.toComma (P := P) (Q := Q) (W := ⊤).hom f) ⋯).toComma
        (P := P) (Q := Q) (W := ⊤).hom

Tactic:
simp
-- Module: Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
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
subst : P.HasPullbacksAlong (f ≫ g)
⊢ P.HasPullbacksAlong fg

Tactic:
subst hfg
-- Module: Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
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
⊢ P.HasPullbacksAlong (f ≫ g)

Tactic:
infer_instance