awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
inst_2 : F.EssSurj
inst_3 : F.Full
X Y : D
f : X ⟶ Y
h : ⊤ f
refine_1 : F.obj (F.objPreimage X) ⟶ F.obj (F.objPreimage Y)
refine_2 :
  Arrow.mk (X := F.obj (F.objPreimage X)) (Y := F.obj (F.objPreimage Y))
      (F.map (F.preimage (Iso.hom (F.objObjPreimageIso X) ≫ f ≫ Iso.inv (F.objObjPreimageIso Y)))) ≅
    Arrow.mk f
⊢ map ⊤ F f

Tactic:
refine ⟨F.objPreimage X, F.objPreimage Y, F.preimage ?_, ⟨⟨⟩, ⟨?_⟩⟩⟩
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
inst_2 : F.EssSurj
inst_3 : F.Full
X Y : D
f : X ⟶ Y
h : ⊤ f
⊢ F.obj (F.objPreimage X) ⟶ F.obj (F.objPreimage Y)

Tactic:
exact (Functor.objObjPreimageIso F X).hom ≫ f ≫ (Functor.objObjPreimageIso F Y).inv

Premises used: CategoryTheory.Functor.objObjPreimageIso, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
inst_2 : F.EssSurj
inst_3 : F.Full
X Y : D
f : X ⟶ Y
h : ⊤ f
⊢ Eq (α := F.obj (F.objPreimage X) ⟶ Y) (Iso.hom (F.objObjPreimageIso X) ≫ f)
    (CategoryStruct.comp (Y := F.obj (F.objPreimage Y))
      (F.map (F.preimage (Iso.hom (F.objObjPreimageIso X) ≫ f ≫ Iso.inv (F.objObjPreimageIso Y))))
      (Iso.hom (F.objObjPreimageIso Y)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
inst_2 : F.EssSurj
inst_3 : F.Full
X Y : D
f : X ⟶ Y
h : ⊤ f
⊢ Arrow.mk (X := F.obj (F.objPreimage X)) (Y := F.obj (F.objPreimage Y))
      (F.map (F.preimage (Iso.hom (F.objObjPreimageIso X) ≫ f ≫ Iso.inv (F.objObjPreimageIso Y)))) ≅
    Arrow.mk f

Tactic:
exact Arrow.isoMk' _ _ (Functor.objObjPreimageIso F X) (Functor.objObjPreimageIso F Y)
      (by simp)

Premises used: CategoryTheory.Functor.objObjPreimageIso, CategoryTheory.Arrow.isoMk'
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
f : Arrow.{v, u} C
⊢ f ∈ P.toSet ↔ P f.hom

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, CategoryTheory.MorphismProperty.toSet
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_3
W : ι → MorphismProperty.{v, u} C
h :
  ∀ (x : Arrow.{v, u} C),
    Membership.mem (γ := Set (Arrow.{v, u} C)) (toSet (⨆ (i : ι), W i)) x ↔
      Membership.mem (γ := Set (Arrow.{v, u} C)) (⋃ (i : ι), (W i).toSet) x
⊢ Eq (α := Set (Arrow.{v, u} C)) (toSet (⨆ (i : ι), W i)) (⋃ (i : ι), (W i).toSet)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_3
W : ι → MorphismProperty.{v, u} C
x : Arrow.{v, u} C
⊢ Membership.mem (γ := Set (Arrow.{v, u} C)) (toSet (⨆ (i : ι), W i)) x ↔
    Membership.mem (γ := Set (Arrow.{v, u} C)) (⋃ (i : ι), (W i).toSet) x

Tactic:
simp [mem_toSet_iff]

Premises used: CategoryTheory.MorphismProperty.mem_toSet_iff
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
W₁ W₂ : MorphismProperty.{v, u} C
⊢ (W₁ ⊔ W₂).toSet = W₁.toSet ∪ W₂.toSet

Tactic:
rfl

Premises used: Set.union, Set.Mem, setOf, CategoryTheory.MorphismProperty.toSet, rfl
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
f : (↑P.toSet : Type (max u v))
⊢ P.homFamily f = (↑f : Arrow C).hom

Tactic:
rfl

Premises used: CategoryTheory.MorphismProperty.homFamily, rfl
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
X Y : C
f : X ⟶ Y
hf : P f
⊢ P.homFamily (Subtype.mk (p := fun (x : Arrow.{v, u} C) ↦ x ∈ P.toSet) (Arrow.mk f) hf) = f

Tactic:
rfl

Premises used: CategoryTheory.MorphismProperty.homFamily, rfl
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
X Y : C
f : X ⟶ Y
⊢ Arrow.mk f ∈ P.toSet ↔ P f

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, CategoryTheory.MorphismProperty.toSet
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
X Y : C
f : X ⟶ Y
hf : P f
X' Y' : C
f' : X' ⟶ Y'
hX : X = X'
hY : Y = Y'
h : f' = eqToHom ⋯ ≫ f ≫ eqToHom hY
rw :
  ∀ (hf : Arrow.mk f ∈ P.toSet) {X' Y' : C} {f' : X' ⟶ Y'} (hX : X = X') (hY : Y = Y')
    (h : f' = eqToHom ⋯ ≫ f ≫ eqToHom hY), Arrow.mk f' ∈ P.toSet
⊢ P f'

Tactic:
rw [← P.arrow_mk_mem_toSet_iff] at hf ⊢

Premises used: CategoryTheory.MorphismProperty.arrow_mk_mem_toSet_iff
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
X Y : C
f : X ⟶ Y
hf : Arrow.mk f ∈ P.toSet
X' Y' : C
f' : X' ⟶ Y'
hX : X = X'
hY : Y = Y'
h : f' = eqToHom ⋯ ≫ f ≫ eqToHom hY
rwa rwa₁ rwa₂ rwa₃ : Arrow.mk f ∈ P.toSet
⊢ Arrow.mk f' ∈ P.toSet

Tactic:
rwa [(Arrow.mk_eq_mk_iff f' f).2 ⟨hX.symm, hY.symm, h⟩]

Premises used: Iff.mpr, Exists.intro, Eq.symm, CategoryTheory.Arrow.mk_eq_mk_iff
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_3
X Y : ι → C
f : (i : ι) → X i ⟶ Y i
A B : C
g : A ⟶ B
mp : ofHoms f g → ∃ (i : ι), Arrow.mk g = Arrow.mk (f i)
mpr : (∃ (i : ι), Arrow.mk g = Arrow.mk (f i)) → ofHoms f g
⊢ ofHoms f g ↔ ∃ (i : ι), Arrow.mk g = Arrow.mk (f i)

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_3
X_1 Y_1 : ι → C
f : (i : ι) → X_1 i ⟶ Y_1 i
X Y : C
i : ι
⊢ ∃ (i_1 : ι), Arrow.mk (f i) = Arrow.mk (f i_1)

Tactic:
⟨i, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_3
X_1 Y_1 : ι → C
f : (i : ι) → X_1 i ⟶ Y_1 i
X Y : C
i : ι
⊢ ∃ (i_1 : ι), Arrow.mk (f i) = Arrow.mk (f i_1)

Tactic:
exact ⟨i, rfl⟩
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_3
X Y : ι → C
f : (i : ι) → X i ⟶ Y i
A B : C
g : A ⟶ B
i : ι
h : Arrow.mk g = Arrow.mk (f i)
mpr : ofHoms f (f i)
⊢ ofHoms f g

Tactic:
rw [← (ofHoms f).arrow_mk_mem_toSet_iff, h, arrow_mk_mem_toSet_iff]

Premises used: CategoryTheory.MorphismProperty.arrow_mk_mem_toSet_iff, CategoryTheory.MorphismProperty.ofHoms
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_3
X Y : ι → C
f : (i : ι) → X i ⟶ Y i
A B : C
g : A ⟶ B
i : ι
h : Arrow.mk g = Arrow.mk (f i)
⊢ ofHoms f (f i)

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), ofHoms P.homFamily f ↔ P f
⊢ ofHoms P.homFamily = P

Tactic:
ext _ _ f
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
X Y : C
f : X ⟶ Y
h : ofHoms P.homFamily f → P f
h₁ : P f → ofHoms P.homFamily f
⊢ ofHoms P.homFamily f ↔ P f

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
X Y : C
f : X ⟶ Y
hf : ofHoms P.homFamily f
⊢ ∃ (i : (↑P.toSet : Type (max u v))), Arrow.mk f = Arrow.mk (P.homFamily i)

Tactic:
rw [ofHoms_iff] at hf

Premises used: CategoryTheory.MorphismProperty.ofHoms_iff
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
X Y : C
f : X ⟶ Y
hf : ∃ (i : (↑P.toSet : Type (max u v))), Arrow.mk f = Arrow.mk (P.homFamily i)
h :
  ∀ (f : Arrow.{v, u} C) (hf : f ∈ P.toSet),
    P (X := (↑(Subtype.mk (p := fun (x : Arrow.{v, u} C) ↦ x ∈ P.toSet) f hf) : Arrow C).left)
      (P.homFamily (Subtype.mk (p := fun (x : Arrow.{v, u} C) ↦ x ∈ P.toSet) f hf))
⊢ P f

Tactic:
obtain ⟨⟨f, hf⟩, ⟨_, _⟩⟩ := hf
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
f : Arrow.{v, u} C
hf : f ∈ P.toSet
⊢ P (X := (↑(Subtype.mk (p := fun (x : Arrow.{v, u} C) ↦ x ∈ P.toSet) f hf) : Arrow C).left)
    (P.homFamily (Subtype.mk (p := fun (x : Arrow.{v, u} C) ↦ x ∈ P.toSet) f hf))

Tactic:
hf

Premises used: Set.Mem, setOf, CategoryTheory.MorphismProperty.homFamily, CategoryTheory.MorphismProperty.toSet
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
f : Arrow.{v, u} C
hf : f ∈ P.toSet
⊢ P (X := (↑(Subtype.mk (p := fun (x : Arrow.{v, u} C) ↦ x ∈ P.toSet) f hf) : Arrow C).left)
    (P.homFamily (Subtype.mk (p := fun (x : Arrow.{v, u} C) ↦ x ∈ P.toSet) f hf))

Tactic:
exact hf
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
X Y : C
f : X ⟶ Y
hf : P f
⊢ ofHoms P.homFamily f

Tactic:
⟨(⟨f, hf⟩ : P.toSet)⟩

Premises used: CategoryTheory.MorphismProperty.homFamily, Subtype.mk, CategoryTheory.MorphismProperty.ofHoms.mk, CategoryTheory.Arrow.mk
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
X Y : C
f : X ⟶ Y
hf : P f
⊢ ofHoms P.homFamily f

Tactic:
exact ⟨(⟨f, hf⟩ : P.toSet)⟩
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
α : Type u_3
ι : α → Type u_4
A B : (a : α) → ι a → C
f : (a : α) → (i : ι a) → A a i ⟶ B a i
h :
  ∀ ⦃f_1 Y : C⦄ (f_2 : f_1 ⟶ Y),
    (⨆ (a : α), ofHoms (f a)) f_2 ↔
      ofHoms (X := fun (j : (a : α) × ι a) ↦ A (j.fst (β := fun (a : α) ↦ ι a)) (j.snd (β := fun (a : α) ↦ ι a))) (Y :=
        fun (j : (a : α) × ι a) ↦ B (j.fst (β := fun (a : α) ↦ ι a)) (j.snd (β := fun (a : α) ↦ ι a)))
        (fun (j : (a : α) × ι a) ↦ f (j.fst (β := fun (a : α) ↦ ι a)) (j.snd (β := fun (a : α) ↦ ι a))) f_2
⊢ Eq (α := MorphismProperty.{v, u} C) (⨆ (a : α), ofHoms (f a))
    (ofHoms (X := fun (j : (a : α) × ι a) ↦ A (j.fst (β := fun (a : α) ↦ ι a)) (j.snd (β := fun (a : α) ↦ ι a))) (Y :=
      fun (j : (a : α) × ι a) ↦ B (j.fst (β := fun (a : α) ↦ ι a)) (j.snd (β := fun (a : α) ↦ ι a)))
      fun (j : (a : α) × ι a) ↦ f (j.fst (β := fun (a : α) ↦ ι a)) (j.snd (β := fun (a : α) ↦ ι a)))

Tactic:
ext f
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
α : Type u_3
ι : α → Type u_4
A B : (a : α) → ι a → C
f_1 : (a : α) → (i : ι a) → A a i ⟶ B a i
f Y : C
f_2 : f ⟶ Y
⊢ (⨆ (a : α), ofHoms (f_1 a)) f_2 ↔
    ofHoms (X := fun (j : (a : α) × ι a) ↦ A (j.fst (β := fun (a : α) ↦ ι a)) (j.snd (β := fun (a : α) ↦ ι a))) (Y :=
      fun (j : (a : α) × ι a) ↦ B (j.fst (β := fun (a : α) ↦ ι a)) (j.snd (β := fun (a : α) ↦ ι a)))
      (fun (j : (a : α) × ι a) ↦ f_1 (j.fst (β := fun (a : α) ↦ ι a)) (j.snd (β := fun (a : α) ↦ ι a))) f_2

Tactic:
simp [ofHoms_iff]

Premises used: CategoryTheory.MorphismProperty.ofHoms_iff
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_3
X Y : ι → C
f : (i : ι) → X i ⟶ Y i
P : MorphismProperty.{v, u} C
⊢ ofHoms f ≤ P ↔ ∀ (i : ι), P (f i)

Tactic:
⟨fun h i ↦ h _ (ofHoms.mk i), fun h _ _ _⟨i⟩ ↦ h i⟩

Premises used: Iff.intro, CategoryTheory.MorphismProperty.ofHoms.mk, _private.0.CategoryTheory.MorphismProperty.ofHoms_le_iff.match_1
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
⊢ single f f

Tactic:
tauto
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
X Y : C
f : X ⟶ Y
⊢ single f ≤ W ↔ W f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
W : Set (MorphismProperty.{v, u} C)
Q : MorphismProperty.{v, u} C
h : ∀ W' ∈ W, W'.RespectsLeft Q
X Y Z : C
x : X ⟶ Y
hi : Q x
x_1 : Y ⟶ Z
hf : InfSet.sInf W x_1
rw : ∀ (hf : ∀ W_1 ∈ W, W_1 x_1), ∀ W_1 ∈ W, W_1 (x ≫ x_1)
⊢ InfSet.sInf W (x ≫ x_1)

Tactic:
rw [sInf_iff] at hf ⊢

Premises used: CategoryTheory.MorphismProperty.sInf_iff
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
W : Set (MorphismProperty.{v, u} C)
Q : MorphismProperty.{v, u} C
h : ∀ W' ∈ W, W'.RespectsLeft Q
X Y Z : C
x : X ⟶ Y
hi : Q x
x_1 : Y ⟶ Z
hf : ∀ W_1 ∈ W, W_1 x_1
⊢ ∀ W_1 ∈ W, W_1 (x ≫ x_1)

Tactic:
fun _ hW' ↦ (h _ hW').precomp _ hi _ (hf _ hW')

Premises used: CategoryTheory.MorphismProperty.RespectsLeft.precomp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
W : Set (MorphismProperty.{v, u} C)
Q : MorphismProperty.{v, u} C
h : ∀ W' ∈ W, W'.RespectsLeft Q
X Y Z : C
x : X ⟶ Y
hi : Q x
x_1 : Y ⟶ Z
hf : ∀ W_1 ∈ W, W_1 x_1
⊢ ∀ W_1 ∈ W, W_1 (x ≫ x_1)

Tactic:
exact fun _ hW' ↦ (h _ hW').precomp _ hi _ (hf _ hW')

Premises used: CategoryTheory.MorphismProperty.RespectsLeft.precomp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
ι : Type u_1
W : ι → MorphismProperty.{v, u} C
Q : MorphismProperty.{v, u} C
inst_1 : ∀ (i : ι), (W i).RespectsLeft Q
⊢ ∀ (W' : MorphismProperty.{v, u} C),
    Membership.mem (γ := Set (MorphismProperty.{v, u} C)) (Set.range fun (i : ι) ↦ W i) W' → W'.RespectsLeft Q

Tactic:
simpa
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
ι : Type u_1
W : ι → MorphismProperty.{v, u} C
Q : MorphismProperty.{v, u} C
inst_1 : ∀ (i : ι), (W i).RespectsLeft Q
⊢ RespectsLeft (InfSet.sInf (Set.range fun (i : ι) ↦ W i)) Q

Tactic:
exact sInf (by simpa)

Premises used: CategoryTheory.MorphismProperty.RespectsLeft.sInf
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
W : Set (MorphismProperty.{v, u} C)
Q : MorphismProperty.{v, u} C
h : ∀ W' ∈ W, W'.RespectsRight Q
X Y Z : C
x : Y ⟶ Z
hi : Q x
x_1 : X ⟶ Y
hf : InfSet.sInf W x_1
rw : ∀ (hf : ∀ W_1 ∈ W, W_1 x_1), ∀ W_1 ∈ W, W_1 (x_1 ≫ x)
⊢ InfSet.sInf W (x_1 ≫ x)

Tactic:
rw [sInf_iff] at hf ⊢

Premises used: CategoryTheory.MorphismProperty.sInf_iff
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
W : Set (MorphismProperty.{v, u} C)
Q : MorphismProperty.{v, u} C
h : ∀ W' ∈ W, W'.RespectsRight Q
X Y Z : C
x : Y ⟶ Z
hi : Q x
x_1 : X ⟶ Y
hf : ∀ W_1 ∈ W, W_1 x_1
⊢ ∀ W_1 ∈ W, W_1 (x_1 ≫ x)

Tactic:
fun _ hW' ↦ (h _ hW').postcomp _ hi _ (hf _ hW')

Premises used: CategoryTheory.MorphismProperty.RespectsRight.postcomp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
W : Set (MorphismProperty.{v, u} C)
Q : MorphismProperty.{v, u} C
h : ∀ W' ∈ W, W'.RespectsRight Q
X Y Z : C
x : Y ⟶ Z
hi : Q x
x_1 : X ⟶ Y
hf : ∀ W_1 ∈ W, W_1 x_1
⊢ ∀ W_1 ∈ W, W_1 (x_1 ≫ x)

Tactic:
exact fun _ hW' ↦ (h _ hW').postcomp _ hi _ (hf _ hW')

Premises used: CategoryTheory.MorphismProperty.RespectsRight.postcomp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
ι : Type u_1
W : ι → MorphismProperty.{v, u} C
Q : MorphismProperty.{v, u} C
inst_1 : ∀ (i : ι), (W i).RespectsRight Q
⊢ ∀ (W' : MorphismProperty.{v, u} C),
    Membership.mem (γ := Set (MorphismProperty.{v, u} C)) (Set.range fun (i : ι) ↦ W i) W' → W'.RespectsRight Q

Tactic:
simpa
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
ι : Type u_1
W : ι → MorphismProperty.{v, u} C
Q : MorphismProperty.{v, u} C
inst_1 : ∀ (i : ι), (W i).RespectsRight Q
⊢ RespectsRight (InfSet.sInf (Set.range fun (i : ι) ↦ W i)) Q

Tactic:
exact sInf (by simpa)

Premises used: CategoryTheory.MorphismProperty.RespectsRight.sInf
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
h : ∀ ⦃X Y : Cᵒᵖ⦄ (f : X ⟶ Y), op (isomorphisms C) f ↔ isomorphisms.{v, u} Cᵒᵖ (X := X) (Y := Y) f
⊢ Eq (α := MorphismProperty.{v, u} Cᵒᵖ) (op (isomorphisms C)) (isomorphisms Cᵒᵖ)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ op (isomorphisms C) f ↔ isomorphisms.{v, u} Cᵒᵖ (X := X) (Y := Y) f

Tactic:
apply isIso_unop_iff

Premises used: CategoryTheory.isIso_unop_iff
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
W : ι → MorphismProperty.{v, u} C
inst_1 : ∀ (i : ι), (W i).RespectsIso
⊢ ∀ (W' : MorphismProperty.{v, u} C),
    Membership.mem (γ := Set (MorphismProperty.{v, u} C)) (Set.range fun (i : ι) ↦ W i) W' → W'.RespectsIso

Tactic:
simpa
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
W : ι → MorphismProperty.{v, u} C
inst_1 : ∀ (i : ι), (W i).RespectsIso
⊢ RespectsIso.{v, u} (C := C) (InfSet.sInf (Set.range fun (i : ι) ↦ W i))

Tactic:
exact sInf (by simpa)

Premises used: CategoryTheory.MorphismProperty.RespectsIso.sInf
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.RespectsIso
X Y Z : C
e : X ⟶ Y
inst_2 : IsIso e
f : Y ⟶ Z
hf : P f
⊢ P (e ≫ f)

Tactic:
RespectsLeft.precomp (Q := isomorphisms C) e ‹IsIso e› f hf

Premises used: CategoryTheory.MorphismProperty.RespectsLeft.precomp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.RespectsIso
X Y Z : C
e : Y ⟶ Z
inst_2 : IsIso e
f : X ⟶ Y
hf : P f
⊢ P (f ≫ e)

Tactic:
RespectsRight.postcomp (Q := isomorphisms C) e ‹IsIso e› f hf

Premises used: CategoryTheory.MorphismProperty.RespectsRight.postcomp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
⊢ P ≤ P.isoClosure

Tactic:
fun _ _ f hf => ⟨_, _, f, hf, ⟨Iso.refl _⟩⟩

Premises used: CategoryTheory.Iso.refl, Nonempty.intro, Exists.intro, CategoryTheory.MorphismProperty.isoClosure, CategoryTheory.Arrow.mk
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
X Y Z : C
e : X ⟶ Y
he : IsIso e
f : Y ⟶ Z
h : P.isoClosure f
w w_1 : C
f' : w ⟶ w_1
hf' : P f'
iso : Arrow.mk f' ≅ Arrow.mk f
⊢ (asIso (Arrow.Hom.left iso.hom) ≪≫ asIso (inv e)).hom ≫ (Arrow.mk (e ≫ f)).hom =
    (Arrow.mk f').hom ≫ (asIso (Arrow.Hom.right iso.hom)).hom

Tactic:
simp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
X Y Z : C
e : Y ⟶ Z
he : IsIso e
f : X ⟶ Y
h : P.isoClosure f
w w_1 : C
f' : w ⟶ w_1
hf' : P f'
iso : Arrow.mk f' ≅ Arrow.mk f
⊢ (asIso (Arrow.Hom.left iso.hom)).hom ≫ (Arrow.mk (f ≫ e)).hom =
    (Arrow.mk f').hom ≫ (asIso (Arrow.Hom.right iso.hom) ≪≫ asIso e).hom

Tactic:
simp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
P Q : MorphismProperty.{v, u} C
h : P ≤ Q
X Y : C
f : X ⟶ Y
this : ∀ (X' Y' : C) (f' : X' ⟶ Y') (hf' : P f') (e : Arrow.mk f' ≅ Arrow.mk f), Q.isoClosure f
⊢ P.isoClosure f → Q.isoClosure f

Tactic:
⟨X', Y', f', hf', ⟨e⟩⟩
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
P Q : MorphismProperty.{v, u} C
h : P ≤ Q
X Y : C
f : X ⟶ Y
X' Y' : C
f' : X' ⟶ Y'
hf' : P f'
e : Arrow.mk f' ≅ Arrow.mk f
⊢ Q.isoClosure f

Tactic:
⟨X', Y', f', h _ hf', ⟨e⟩⟩

Premises used: Nonempty.intro, Exists.intro, CategoryTheory.MorphismProperty.isoClosure
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
P Q : MorphismProperty.{v, u} C
h : P ≤ Q
X Y : C
f : X ⟶ Y
X' Y' : C
f' : X' ⟶ Y'
hf' : P f'
e : Arrow.mk f' ≅ Arrow.mk f
⊢ Q.isoClosure f

Tactic:
exact ⟨X', Y', f', h _ hf', ⟨e⟩⟩
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
hP : P.RespectsIso
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst_1 : IsIso f
h : P (f ≫ g)
⊢ P g

Tactic:
simpa using RespectsIso.precomp P (inv f) (f ≫ g) h

Premises used: CategoryTheory.MorphismProperty.RespectsIso.precomp, CategoryTheory.CategoryStruct.comp, CategoryTheory.inv
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
hP : P.RespectsIso
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst_1 : IsIso g
h : P (f ≫ g)
⊢ P f

Tactic:
simpa using RespectsIso.postcomp P (inv g) (f ≫ g) h

Premises used: CategoryTheory.MorphismProperty.RespectsIso.postcomp, CategoryTheory.CategoryStruct.comp, CategoryTheory.inv
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.RespectsIso
A : Type u_1
B : Type u_2
inst_2 : Category.{v_1, u_1} A
inst_3 : Category.{v_2, u_2} B
L : Functor.{v_1, v, u_1, u} A C
R : Functor.{v_2, v, u_2, u} B C
f g : Comma L R
e : f ≅ g
⊢ P f.hom ↔ P g.hom

Tactic:
simp [← Comma.inv_left_hom_right e.hom, cancel_left_of_respectsIso, cancel_right_of_respectsIso]

Premises used: CategoryTheory.Comma.inv_left_hom_right, CategoryTheory.MorphismProperty.cancel_left_of_respectsIso, CategoryTheory.Iso.hom, CategoryTheory.MorphismProperty.cancel_right_of_respectsIso
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.RespectsIso
f g : Arrow.{v, u} C
e : f ≅ g
⊢ P f.hom ↔ P g.hom

Tactic:
P.comma_iso_iff e

Premises used: CategoryTheory.MorphismProperty.comma_iso_iff
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.RespectsIso
W X Y Z : C
f : W ⟶ X
g : Y ⟶ Z
e : Arrow.mk f ≅ Arrow.mk g
⊢ P f ↔ P g

Tactic:
P.arrow_iso_iff e

Premises used: CategoryTheory.MorphismProperty.arrow_iso_iff
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
hP : ∀ (f g : Arrow.{v, u} C) (x : f ≅ g), P f.hom → P g.hom
X Y Z : C
e : X ⟶ Y
he : IsIso e
f : Y ⟶ Z
hf : P f
⊢ P (e ≫ f)

Tactic:
hP (Arrow.mk f) (Arrow.mk (e ≫ f)) (Arrow.isoMk (asIso (inv e)) (Iso.refl _) ?_) hf

Premises used: CategoryTheory.Iso.refl, CategoryTheory.CategoryStruct.comp, CategoryTheory.inv, CategoryTheory.Arrow.mk, CategoryTheory.asIso, CategoryTheory.Arrow.isoMk
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
hP : ∀ (f g : Arrow.{v, u} C) (x : f ≅ g), P f.hom → P g.hom
X Y Z : C
e : X ⟶ Y
he : IsIso e
f : Y ⟶ Z
hf : P f
refine : (asIso (inv e)).hom ≫ (Arrow.mk (e ≫ f)).hom = (Arrow.mk f).hom ≫ Iso.hom (Iso.refl (Arrow.mk f).right)
⊢ P (e ≫ f)

Tactic:
refine hP (Arrow.mk f) (Arrow.mk (e ≫ f)) (Arrow.isoMk (asIso (inv e)) (Iso.refl _) ?_) hf

Premises used: CategoryTheory.Iso.refl, CategoryTheory.CategoryStruct.comp, CategoryTheory.inv, CategoryTheory.Arrow.mk, CategoryTheory.asIso, CategoryTheory.Arrow.isoMk
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
hP : ∀ (f g : Arrow.{v, u} C) (x : f ≅ g), P f.hom → P g.hom
X Y Z : C
e : X ⟶ Y
he : IsIso e
f : Y ⟶ Z
hf : P f
⊢ (asIso (inv e)).hom ≫ (Arrow.mk (e ≫ f)).hom = (Arrow.mk f).hom ≫ Iso.hom (Iso.refl (Arrow.mk f).right)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
hP : ∀ (f g : Arrow.{v, u} C) (x : f ≅ g), P f.hom → P g.hom
X Y Z : C
e : Y ⟶ Z
he : IsIso e
f : X ⟶ Y
hf : P f
⊢ P (f ≫ e)

Tactic:
hP (Arrow.mk f) (Arrow.mk (f ≫ e)) (Arrow.isoMk (Iso.refl _) (asIso e) ?_) hf

Premises used: CategoryTheory.Iso.refl, CategoryTheory.CategoryStruct.comp, CategoryTheory.Arrow.mk, CategoryTheory.asIso, CategoryTheory.Arrow.isoMk