awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.MorphismProperty.IsSmall
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
i : Shrink.{w, max u v} (↑W.toSet : Type (max u v))
hi :
  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:
simp only [← W.arrow_mk_mem_toSet_iff, hi, Arrow.mk_eq, Subtype.coe_prop]

Premises used: Subtype.coe_prop, CategoryTheory.MorphismProperty.arrow_mk_mem_toSet_iff, CategoryTheory.Arrow.mk_eq
-- Module: Mathlib.CategoryTheory.MorphismProperty.IsSmall
Goal:
C : Type u
inst : Category.{v, u} C
w : Type w
w_1 w_2 : w → C
w_3 : (i : w) → w_1 i ⟶ w_2 i
⊢ IsSmall.{w, v, u} (ofHoms w_3)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.MorphismProperty.IsSmall
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)
rw : Small.{w, max u v} (↑(⋃ (i : α), (W i).toSet) : Type (max u v))
⊢ Small.{w, max u v} (↑(iSup W).toSet : Type (max u v))

Tactic:
rw [toSet_iSup]

Premises used: CategoryTheory.MorphismProperty.toSet_iSup
-- Module: Mathlib.CategoryTheory.MorphismProperty.IsSmall
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))
rw : ∃ (i_1 : α), (↑f : Arrow C) ∈ (W i_1).toSet
⊢ Membership.mem (γ := Set (Arrow.{v, u} C)) (⋃ (i : α), (W i).toSet) (↑f : Arrow C)

Tactic:
rw [Set.mem_iUnion]

Premises used: Set.mem_iUnion
-- Module: Mathlib.CategoryTheory.MorphismProperty.IsSmall
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))
⊢ ∃ (i_1 : α), (↑f : Arrow C) ∈ (W i_1).toSet

Tactic:
⟨i, f.prop⟩

Premises used: Subtype.prop, Exists.intro
-- Module: Mathlib.CategoryTheory.MorphismProperty.IsSmall
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))
⊢ ∃ (i_1 : α), (↑f : Arrow C) ∈ (W i_1).toSet

Tactic:
exact ⟨i, f.prop⟩
-- Module: Mathlib.CategoryTheory.MorphismProperty.IsSmall
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)
refine :
  Function.Surjective (β := (↑(⋃ (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) ⋯
⊢ Small.{w, max u v} (↑(⋃ (i : α), (W i).toSet) : Type (max u v))

Tactic:
refine small_of_surjective (f := fun (⟨i, f⟩ : Σ i, (W i).toSet) ↦
      ⟨f, by rw [Set.mem_iUnion]; exact ⟨i, f.prop⟩⟩) ?_

Premises used: small_of_surjective
-- Module: Mathlib.CategoryTheory.MorphismProperty.IsSmall
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
⊢ ∃ (i : α), f ∈ (W i).toSet

Tactic:
simp only [Set.mem_iUnion] at hf

Premises used: Set.mem_iUnion
-- Module: Mathlib.CategoryTheory.MorphismProperty.IsSmall
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
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) ⋯ :
              (↑(⋃ (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
⊢ ∃ (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

Tactic:
obtain ⟨i, hf⟩ := hf
-- Module: Mathlib.CategoryTheory.MorphismProperty.IsSmall
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
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) ⋯ :
            (↑(⋃ (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:
⟨⟨i, ⟨_, hf⟩⟩, rfl⟩

Premises used: Subtype.mk, Exists.intro, Sigma.mk, rfl
-- Module: Mathlib.CategoryTheory.MorphismProperty.IsSmall
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
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) ⋯ :
            (↑(⋃ (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:
exact ⟨⟨i, ⟨_, hf⟩⟩, rfl⟩
-- Module: Mathlib.CategoryTheory.MorphismProperty.IsSmall
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)
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)
⊢ 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
-- Module: Mathlib.CategoryTheory.MorphismProperty.IsSmall
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)
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)))
⊢ IsSmall.{w, v, u} (C := C) (⨆ (i : α_1), W i)

Tactic:
simp only [hf, iSup_ofHoms]

Premises used: CategoryTheory.MorphismProperty.iSup_ofHoms
-- Module: Mathlib.CategoryTheory.MorphismProperty.IsSmall
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)
    (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:
infer_instance
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
A B X Y : C
f : A ⟶ X
q : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : IsPullback f q p g
hp : P p
⊢ P.pullbacks q

Tactic:
⟨_, _, _, _, _, hp, sq⟩

Premises used: CategoryTheory.MorphismProperty.pullbacks, Exists.intro
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
A B : C
q : A ⟶ B
hq : P q
⊢ P.pullbacks q

Tactic:
P.pullbacks_mk IsPullback.of_id_fst hq

Premises used: CategoryTheory.IsPullback.of_id_fst, CategoryTheory.MorphismProperty.pullbacks_mk
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
A B : C
q : A ⟶ B
hq : P q
⊢ P.pullbacks q

Tactic:
exact P.pullbacks_mk IsPullback.of_id_fst hq

Premises used: CategoryTheory.IsPullback.of_id_fst, CategoryTheory.MorphismProperty.pullbacks_mk
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
a b : MorphismProperty.{v, u} C
h : a ≤ b
X Y : C
f : X ⟶ Y
w w_1 : C
w_2 : w ⟶ w_1
w_3 : X ⟶ w
w_4 : Y ⟶ w_1
hp : a w_2
sq : IsPullback w_3 f w_2 w_4
⊢ b.pullbacks f

Tactic:
⟨_, _, _, _, _, h _ hp, sq⟩

Premises used: CategoryTheory.MorphismProperty.pullbacks, Exists.intro
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
a b : MorphismProperty.{v, u} C
h : a ≤ b
X Y : C
f : X ⟶ Y
w w_1 : C
w_2 : w ⟶ w_1
w_3 : X ⟶ w
w_4 : Y ⟶ w_1
hp : a w_2
sq : IsPullback w_3 f w_2 w_4
⊢ b.pullbacks f

Tactic:
exact ⟨_, _, _, _, _, h _ hp, sq⟩
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
A B X Y : C
f : A ⟶ X
q : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : IsPushout f q p g
hq : P q
⊢ P.pushouts p

Tactic:
⟨_, _, _, _, _, hq, sq⟩

Premises used: CategoryTheory.MorphismProperty.pushouts, Exists.intro
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
X Y : C
p : X ⟶ Y
hp : P p
⊢ P.pushouts p

Tactic:
P.pushouts_mk IsPushout.of_id_fst hp

Premises used: CategoryTheory.MorphismProperty.pushouts_mk, CategoryTheory.IsPushout.of_id_fst
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
X Y : C
p : X ⟶ Y
hp : P p
⊢ P.pushouts p

Tactic:
exact P.pushouts_mk IsPushout.of_id_fst hp

Premises used: CategoryTheory.MorphismProperty.pushouts_mk, CategoryTheory.IsPushout.of_id_fst
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
a b : MorphismProperty.{v, u} C
h : a ≤ b
X Y : C
f : X ⟶ Y
w w_1 : C
w_2 : w ⟶ w_1
w_3 : w ⟶ X
w_4 : w_1 ⟶ Y
hp : a w_2
sq : IsPushout w_3 w_2 f w_4
⊢ b.pushouts f

Tactic:
⟨_, _, _, _, _, h _ hp, sq⟩

Premises used: CategoryTheory.MorphismProperty.pushouts, Exists.intro
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
a b : MorphismProperty.{v, u} C
h : a ≤ b
X Y : C
f : X ⟶ Y
w w_1 : C
w_2 : w ⟶ w_1
w_3 : w ⟶ X
w_4 : w_1 ⟶ Y
hp : a w_2
sq : IsPushout w_3 w_2 f w_4
⊢ b.pushouts f

Tactic:
exact ⟨_, _, _, _, _, h _ hp, sq⟩
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
q q' : Arrow.{v, u} C
e : q ≅ q'
A B : C
p : A ⟶ B
f : A ⟶ q.left
g : B ⟶ q.right
hp : P p
h : IsPushout f p q.hom g
⊢ P.pushouts q'.hom

Tactic:
⟨A, B, p, f ≫ e.hom.left, g ≫ e.hom.right, hp,
      IsPushout.paste_horiz h (IsPushout.of_horiz_isIso ⟨e.hom.w⟩)⟩

Premises used: CategoryTheory.IsPushout.of_horiz_isIso, CategoryTheory.MorphismProperty.pushouts, CategoryTheory.Arrow.Hom.right, CategoryTheory.CommSq.mk, CategoryTheory.Arrow.Hom.w, CategoryTheory.IsPushout.paste_horiz, Exists.intro, CategoryTheory.CategoryStruct.comp, CategoryTheory.Arrow.Hom.left, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
q q' : Arrow.{v, u} C
e : q ≅ q'
A B : C
p : A ⟶ B
f : A ⟶ q.left
g : B ⟶ q.right
hp : P p
h : IsPushout f p q.hom g
⊢ P.pushouts q'.hom

Tactic:
exact ⟨A, B, p, f ≫ e.hom.left, g ≫ e.hom.right, hp,
      IsPushout.paste_horiz h (IsPushout.of_horiz_isIso ⟨e.hom.w⟩)⟩
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
q q' : Arrow.{v, u} C
e : q ≅ q'
X Y : C
p : X ⟶ Y
f : q.left ⟶ X
g : q.right ⟶ Y
hp : P p
h : IsPullback f q.hom p g
⊢ P.pullbacks q'.hom

Tactic:
⟨X, Y, p, e.inv.left ≫ f, e.inv.right ≫ g, hp,
      IsPullback.paste_horiz (IsPullback.of_horiz_isIso ⟨e.inv.w⟩) h⟩

Premises used: CategoryTheory.MorphismProperty.pullbacks, CategoryTheory.Arrow.Hom.right, CategoryTheory.CommSq.mk, CategoryTheory.Arrow.Hom.w, Exists.intro, CategoryTheory.CategoryStruct.comp, CategoryTheory.Arrow.Hom.left, CategoryTheory.IsPullback.paste_horiz, CategoryTheory.Iso.inv, CategoryTheory.IsPullback.of_horiz_isIso
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
q q' : Arrow.{v, u} C
e : q ≅ q'
X Y : C
p : X ⟶ Y
f : q.left ⟶ X
g : q.right ⟶ Y
hp : P p
h : IsPullback f q.hom p g
⊢ P.pullbacks q'.hom

Tactic:
exact ⟨X, Y, p, e.inv.left ≫ f, e.inv.right ≫ g, hp,
      IsPullback.paste_horiz (IsPullback.of_horiz_isIso ⟨e.inv.w⟩) h⟩
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
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), CategoryTheory.IsIso p
X Y : C
f : X ⟶ Y
IsIso : CategoryTheory.IsIso f → P.pushouts f
⊢ isomorphisms C f → P.pushouts f

Tactic:
(_ : IsIso f)
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
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
obtain : ∀ (A B : C) (p : A ⟶ B) (hp : P p) (g : B ⟶ X), IsIso p → P.pushouts f
⊢ P.pushouts f

Tactic:
obtain ⟨A, B, p, hp, g, _⟩ := h X
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
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
A B : C
p : A ⟶ B
hp : P p
g : B ⟶ X
h_2 : IsIso p
⊢ (p ≫ g) ≫ Iso.hom (Iso.refl X) = Iso.hom (Iso.refl A) ≫ p ≫ g

Tactic:
simp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
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
A B : C
p : A ⟶ B
hp : P p
g : B ⟶ X
h_2 : IsIso p
⊢ 𝟙 A ≫ (asIso p).hom = Iso.hom (Iso.refl A) ≫ p

Tactic:
simp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
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
A B : C
p : A ⟶ B
hp : P p
g : B ⟶ X
h_2 : IsIso p
⊢ 𝟙 X ≫ (asIso f).hom = Iso.hom (Iso.refl X) ≫ f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
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
A B : C
p : A ⟶ B
hp : P p
g : B ⟶ X
h_2 : IsIso p
⊢ (p ≫ g) ≫ (asIso f).hom = (asIso p).hom ≫ g ≫ f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
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
A B : C
p : A ⟶ B
hp : P p
g : B ⟶ X
h_2 : IsIso p
⊢ P.pushouts f

Tactic:
exact ⟨A, B, p, p ≫ g, g ≫ f, hp, (IsPushout.of_id_snd (f := p ≫ g)).of_iso
    (Iso.refl _) (Iso.refl _) (asIso p) (asIso f) (by simp) (by simp) (by simp) (by simp)⟩
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
X Y Y' S : C
f : X ⟶ S
g : Y ⟶ S
f' : Y' ⟶ Y
g' : Y' ⟶ X
h : IsPullback f' g' g f
w w_1 : C
w_2 : w ⟶ w_1
w_3 : Y ⟶ w
w_4 : S ⟶ w_1
hp : P w_2
hq : IsPullback w_3 g w_2 w_4
⊢ P.pullbacks g'

Tactic:
P.pullbacks_mk (h.paste_horiz hq) hp

Premises used: CategoryTheory.MorphismProperty.pullbacks_mk, CategoryTheory.IsPullback.paste_horiz
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
X Y Y' S : C
f : X ⟶ S
g : Y ⟶ S
f' : Y' ⟶ Y
g' : Y' ⟶ X
h : IsPullback f' g' g f
w w_1 : C
w_2 : w ⟶ w_1
w_3 : Y ⟶ w
w_4 : S ⟶ w_1
hp : P w_2
hq : IsPullback w_3 g w_2 w_4
⊢ P.pullbacks g'

Tactic:
exact P.pullbacks_mk (h.paste_horiz hq) hp

Premises used: CategoryTheory.MorphismProperty.pullbacks_mk, CategoryTheory.IsPullback.paste_horiz
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
A A' B B' : C
f : A ⟶ A'
g : A ⟶ B
f' : B ⟶ B'
g' : A' ⟶ B'
h : IsPushout g f f' g'
w w_1 : C
w_2 : w ⟶ w_1
w_3 : w ⟶ A
w_4 : w_1 ⟶ A'
hp : P w_2
hq : IsPushout w_3 w_2 f w_4
⊢ P.pushouts f'

Tactic:
P.pushouts_mk (hq.paste_horiz h) hp

Premises used: CategoryTheory.MorphismProperty.pushouts_mk, CategoryTheory.IsPushout.paste_horiz
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
A A' B B' : C
f : A ⟶ A'
g : A ⟶ B
f' : B ⟶ B'
g' : A' ⟶ B'
h : IsPushout g f f' g'
w w_1 : C
w_2 : w ⟶ w_1
w_3 : w ⟶ A
w_4 : w_1 ⟶ A'
hp : P w_2
hq : IsPushout w_3 w_2 f w_4
⊢ P.pushouts f'

Tactic:
exact P.pushouts_mk (hq.paste_horiz h) hp

Premises used: CategoryTheory.MorphismProperty.pushouts_mk, CategoryTheory.IsPushout.paste_horiz
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
mp : P.IsStableUnderBaseChange → P.pullbacks ≤ P
mpr : P.pullbacks ≤ P → P.IsStableUnderBaseChange
⊢ P.IsStableUnderBaseChange ↔ P.pullbacks ≤ P

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
h : P.IsStableUnderBaseChange
mp : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P.pullbacks f → P f
⊢ P.pullbacks ≤ P

Tactic:
_
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
h : P.IsStableUnderBaseChange
X : C
mp : ∀ ⦃Y : C⦄ (f : X ⟶ Y), P.pullbacks f → P f
⊢ ∀ ⦃Y : C⦄ (f : X ⟶ Y), P.pullbacks f → P f

Tactic:
_
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
h : P.IsStableUnderBaseChange
X Y : C
mp : ∀ (f : X ⟶ Y), P.pullbacks f → P f
⊢ ∀ (f : X ⟶ Y), P.pullbacks f → P f

Tactic:
_
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
h : P.IsStableUnderBaseChange
X Y : C
f : X ⟶ Y
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
⊢ P.pullbacks f → P f

Tactic:
⟨_, _, _, _, _, h₁, h₂⟩
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
h : P.IsStableUnderBaseChange
X Y : C
f : X ⟶ Y
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:
of_isPullback h₂ h₁

Premises used: CategoryTheory.MorphismProperty.of_isPullback
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
h : P.IsStableUnderBaseChange
X Y : C
f : X ⟶ Y
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:
exact of_isPullback h₂ h₁

Premises used: CategoryTheory.MorphismProperty.of_isPullback
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
h : P.pullbacks ≤ P
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'
⊢ P.IsStableUnderBaseChange

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
h : P.pullbacks ≤ P
X : C
mpr : ∀ {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'
⊢ ∀ {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:
_
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
h : P.pullbacks ≤ P
X Y : C
mpr : ∀ {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'
⊢ ∀ {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:
_
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
h : P.pullbacks ≤ P
X Y Y' : C
mpr : ∀ {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'
⊢ ∀ {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:
_