awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.MorphismProperty.Composition
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P : MorphismProperty.{v', u'} D
inst_2 : P.ContainsIdentities
F : Functor.{v, v', u, u'} C D
X : C
⊢ P.inverseImage F (𝟙 X)

Tactic:
simpa only [← F.map_id] using P.id_mem (F.obj X)

Premises used: CategoryTheory.Functor.map_id, CategoryTheory.MorphismProperty.id_mem, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.MorphismProperty.Composition
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
ι : Type u_1
W : ι → MorphismProperty.{v, u} C
inst_2 : ∀ (i : ι), (W i).ContainsIdentities
⊢ ∀ (W' : MorphismProperty.{v, u} C),
    Membership.mem (γ := Set (MorphismProperty.{v, u} C)) (Set.range fun (i : ι) ↦ W i) W' → W'.ContainsIdentities

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

Tactic:
exact sInf (by simpa)

Premises used: CategoryTheory.MorphismProperty.ContainsIdentities.sInf
-- Module: Mathlib.CategoryTheory.MorphismProperty.Composition
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
C₁ : Type u_1
C₂ : Type u_2
inst_2 : Category.{v_1, u_1} C₁
inst_3 : Category.{v_2, u_2} C₂
W₁ : MorphismProperty.{v_1, u_1} C₁
W₂ : MorphismProperty.{v_2, u_2} C₂
inst_4 : W₁.ContainsIdentities
inst_5 : W₂.ContainsIdentities
⊢ (W₁.prod W₂).ContainsIdentities (C := C₁ × C₂)

Tactic:
⟨fun _ => ⟨W₁.id_mem _, W₂.id_mem _⟩⟩

Premises used: CategoryTheory.MorphismProperty.ContainsIdentities.mk, Prod.fst, And.intro, CategoryTheory.MorphismProperty.id_mem, Prod.snd
-- Module: Mathlib.CategoryTheory.MorphismProperty.Composition
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
D : Type u'
inst_1 : Category.{v', u'} D
J : Type w
C : J → Type u
inst_2 : (j : J) → Category.{v, u} (C j)
W : (j : J) → MorphismProperty.{v, u} (C j)
inst_3 : ∀ (j : J), (W j).ContainsIdentities
⊢ (pi (C := C) W).ContainsIdentities

Tactic:
⟨fun _ _ => MorphismProperty.id_mem _ _⟩

Premises used: CategoryTheory.MorphismProperty.ContainsIdentities.mk, CategoryTheory.MorphismProperty.id_mem
-- Module: Mathlib.CategoryTheory.MorphismProperty.Composition
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.ContainsIdentities
inst_2 : P.RespectsIso
X Y : C
f : X ⟶ Y
inst_3 : IsIso f
⊢ P f

Tactic:
Category.id_comp f ▸ RespectsIso.postcomp P f (𝟙 X) (P.id_mem X)

Premises used: CategoryTheory.MorphismProperty.RespectsIso.postcomp, CategoryTheory.CategoryStruct.id, Eq.rec, CategoryTheory.MorphismProperty.id_mem, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Composition
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.ContainsIdentities
inst_2 : P.RespectsIso
⊢ isomorphisms C ≤ P

Tactic:
fun _ _ f (_ : IsIso f) ↦ P.of_isIso f

Premises used: CategoryTheory.MorphismProperty.of_isIso
-- Module: Mathlib.CategoryTheory.MorphismProperty.Composition
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
inst_1 : W.IsStableUnderComposition
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : W f
hg : W g
⊢ W (f ≫ g)

Tactic:
IsStableUnderComposition.comp_mem f g hf hg

Premises used: CategoryTheory.MorphismProperty.IsStableUnderComposition.comp_mem
-- Module: Mathlib.CategoryTheory.MorphismProperty.Composition
Goal:
C : Type u
inst : Category.{v, u} C
W : Set (MorphismProperty.{v, u} C)
h : ∀ W' ∈ W, W'.IsStableUnderComposition
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : InfSet.sInf W f
hg : InfSet.sInf W g
rw : ∀ (hf : ∀ W_1 ∈ W, W_1 f) (hg : ∀ W_1 ∈ W, W_1 g), ∀ W_1 ∈ W, W_1 (f ≫ g)
⊢ InfSet.sInf W (f ≫ g)

Tactic:
rw [sInf_iff] at hf hg ⊢

Premises used: CategoryTheory.MorphismProperty.sInf_iff
-- Module: Mathlib.CategoryTheory.MorphismProperty.Composition
Goal:
C : Type u
inst : Category.{v, u} C
W : Set (MorphismProperty.{v, u} C)
h : ∀ W' ∈ W, W'.IsStableUnderComposition
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : ∀ W_1 ∈ W, W_1 f
hg : ∀ W_1 ∈ W, W_1 g
⊢ ∀ W_1 ∈ W, W_1 (f ≫ g)

Tactic:
fun W' hW' ↦ (h W' hW').comp_mem _ _ (hf _ hW') (hg _ hW')

Premises used: CategoryTheory.MorphismProperty.IsStableUnderComposition.comp_mem
-- Module: Mathlib.CategoryTheory.MorphismProperty.Composition
Goal:
C : Type u
inst : Category.{v, u} C
W : Set (MorphismProperty.{v, u} C)
h : ∀ W' ∈ W, W'.IsStableUnderComposition
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : ∀ W_1 ∈ W, W_1 f
hg : ∀ W_1 ∈ W, W_1 g
⊢ ∀ W_1 ∈ W, W_1 (f ≫ g)

Tactic:
exact fun W' hW' ↦ (h W' hW').comp_mem _ _ (hf _ hW') (hg _ hW')

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

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

Tactic:
exact sInf (by simpa)

Premises used: CategoryTheory.MorphismProperty.IsStableUnderComposition.sInf
-- Module: Mathlib.CategoryTheory.MorphismProperty.Composition
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
h : P.StableUnderInverse
⊢ StableUnderInverse.{v, u} (C := Cᵒᵖ) P.op

Tactic:
fun _ _ e he => h e.unop he

Premises used: Quiver.Hom.unop, CategoryTheory.MorphismProperty.op, CategoryTheory.MorphismProperty.StableUnderInverse, CategoryTheory.Iso.unop
-- Module: Mathlib.CategoryTheory.MorphismProperty.Composition
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} Cᵒᵖ
h : StableUnderInverse.{v, u} (C := Cᵒᵖ) P
⊢ P.unop.StableUnderInverse

Tactic:
fun _ _ e he => h e.op he

Premises used: Quiver.Hom.op, CategoryTheory.MorphismProperty.unop, CategoryTheory.Iso.op, CategoryTheory.MorphismProperty.StableUnderInverse
-- Module: Mathlib.CategoryTheory.MorphismProperty.Composition
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.IsStableUnderComposition
hP : isomorphisms C ≤ P
⊢ P.RespectsIso

Tactic:
RespectsIso.mk _
  (fun _ _ hf => P.comp_mem _ _ (hP _ (isomorphisms.infer_property _)) hf)
    (fun _ _ hf => P.comp_mem _ _ hf (hP _ (isomorphisms.infer_property _)))

Premises used: CategoryTheory.MorphismProperty.RespectsIso.mk, CategoryTheory.MorphismProperty.comp_mem, CategoryTheory.MorphismProperty.isomorphisms.infer_property, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.MorphismProperty.Composition
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P : MorphismProperty.{v', u'} D
inst_2 : P.IsStableUnderComposition
F : Functor.{v, v', u, u'} C D
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : P.inverseImage F f
hg : P.inverseImage F g
⊢ P.inverseImage F (f ≫ g)

Tactic:
simpa only [← F.map_comp] using P.comp_mem _ _ hf hg

Premises used: CategoryTheory.MorphismProperty.comp_mem, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Composition
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F₁ F₂ : Functor.{v, v', u, u'} C D
app : (X : C) → F₁.obj X ⟶ F₂.obj X
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : F₁.map f ≫ app Y = app X ≫ F₂.map f
hg : F₁.map g ≫ app Z = app Y ≫ F₂.map g
simp : F₁.map f ≫ app Y ≫ F₂.map g = app X ≫ F₂.map f ≫ F₂.map g
⊢ F₁.map (f ≫ g) ≫ app Z = app X ≫ F₂.map (f ≫ g)

Tactic:
simp only [Functor.map_comp, Category.assoc, hg]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Composition
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F₁ F₂ : Functor.{v, v', u, u'} C D
app : (X : C) → F₁.obj X ⟶ F₂.obj X
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : F₁.map f ≫ app Y = app X ≫ F₂.map f
hg : F₁.map g ≫ app Z = app Y ≫ F₂.map g
a : app X ≫ F₂.map f
| F₁.map f ≫ app Y

Tactic:
rw [hf]
-- Module: Mathlib.CategoryTheory.MorphismProperty.Composition
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F₁ F₂ : Functor.{v, v', u, u'} C D
app : (X : C) → F₁.obj X ⟶ F₂.obj X
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : F₁.map f ≫ app Y = app X ≫ F₂.map f
hg : F₁.map g ≫ app Z = app Y ≫ F₂.map g
slice_lhs : (app X ≫ F₂.map f) ≫ F₂.map g = app X ≫ F₂.map f ≫ F₂.map g
⊢ F₁.map f ≫ app Y ≫ F₂.map g = app X ≫ F₂.map f ≫ F₂.map g

Tactic:
slice_lhs 1 2 => rw [hf]
-- Module: Mathlib.CategoryTheory.MorphismProperty.Composition
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F₁ F₂ : Functor.{v, v', u, u'} C D
app : (X : C) → F₁.obj X ⟶ F₂.obj X
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : F₁.map f ≫ app Y = app X ≫ F₂.map f
hg : F₁.map g ≫ app Z = app Y ≫ F₂.map g
rw rw₁ : app X ≫ F₂.map f ≫ F₂.map g = app X ≫ F₂.map f ≫ F₂.map g
⊢ (app X ≫ F₂.map f) ≫ F₂.map g = app X ≫ F₂.map f ≫ F₂.map g

Tactic:
rw [Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.MorphismProperty.Composition
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F₁ F₂ : Functor.{v, v', u, u'} C D
app : (X : C) → F₁.obj X ⟶ F₂.obj X
X Y : C
e : X ≅ Y
he : F₁.map e.hom ≫ app Y = app X ≫ F₂.map e.hom
rw : F₁.map e.hom ≫ F₁.map e.inv ≫ app X = F₁.map e.hom ≫ app Y ≫ F₂.map e.inv
⊢ F₁.map e.inv ≫ app X = app Y ≫ F₂.map e.inv

Tactic:
rw [← cancel_epi (F₁.map e.hom)]

Premises used: CategoryTheory.Functor.map, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.MorphismProperty.Composition
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F₁ F₂ : Functor.{v, v', u, u'} C D
app : (X : C) → F₁.obj X ⟶ F₂.obj X
X Y : C
e : X ≅ Y
he : F₁.map e.hom ≫ app Y = app X ≫ F₂.map e.hom
a : app X ≫ F₂.map e.hom
| F₁.map e.hom ≫ app Y

Tactic:
rw [he]
-- Module: Mathlib.CategoryTheory.MorphismProperty.Composition
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F₁ F₂ : Functor.{v, v', u, u'} C D
app : (X : C) → F₁.obj X ⟶ F₂.obj X
X Y : C
e : X ≅ Y
he : F₁.map e.hom ≫ app Y = app X ≫ F₂.map e.hom
slice_rhs : F₁.map e.hom ≫ F₁.map e.inv ≫ app X = (app X ≫ F₂.map e.hom) ≫ F₂.map e.inv
⊢ F₁.map e.hom ≫ F₁.map e.inv ≫ app X = F₁.map e.hom ≫ app Y ≫ F₂.map e.inv

Tactic:
slice_rhs 1 2 => rw [he]
-- Module: Mathlib.CategoryTheory.MorphismProperty.Composition
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F₁ F₂ : Functor.{v, v', u, u'} C D
app : (X : C) → F₁.obj X ⟶ F₂.obj X
X Y : C
e : X ≅ Y
he : F₁.map e.hom ≫ app Y = app X ≫ F₂.map e.hom
⊢ F₁.map e.hom ≫ F₁.map e.inv ≫ app X = (app X ≫ F₂.map e.hom) ≫ F₂.map e.inv

Tactic:
simp only [Category.assoc, ← F₁.map_comp_assoc, ← F₂.map_comp, e.hom_inv_id, Functor.map_id,
    Category.id_comp, Category.comp_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.hom_inv_id, CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Functor.map_id, CategoryTheory.Functor.map_comp, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Composition
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
inst_1 : IsMultiplicative.{v, u} (C := Cᵒᵖ) W.op
⊢ W.IsMultiplicative

Tactic:
inferInstanceAs <| IsMultiplicative W.op.unop

Premises used: _private.0.CategoryTheory.MorphismProperty.IsMultiplicative.of_op._proof_1
-- Module: Mathlib.CategoryTheory.MorphismProperty.Composition
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} Cᵒᵖ
inst_1 : W.unop.IsMultiplicative
⊢ IsMultiplicative.{v, u} (C := Cᵒᵖ) W

Tactic:
inferInstanceAs <| IsMultiplicative W.unop.op

Premises used: _private.0.CategoryTheory.MorphismProperty.IsMultiplicative.of_unop._proof_1
-- Module: Mathlib.CategoryTheory.MorphismProperty.Composition
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : isomorphisms C f
hg : isomorphisms C g
⊢ IsIso f

Tactic:
rw [isomorphisms.iff] at hf hg ⊢

Premises used: CategoryTheory.MorphismProperty.isomorphisms.iff
-- Module: Mathlib.CategoryTheory.MorphismProperty.Composition
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : isomorphisms C f
hg : isomorphisms C g
hf₁ : IsIso f
⊢ IsIso g

Tactic:
rw [isomorphisms.iff] at hf hg ⊢

Premises used: CategoryTheory.MorphismProperty.isomorphisms.iff
-- Module: Mathlib.CategoryTheory.MorphismProperty.Composition
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : IsIso f
hg : IsIso g
⊢ IsIso (f ≫ g)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.MorphismProperty.Composition
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : monomorphisms C f
hg : monomorphisms C g
⊢ Mono f

Tactic:
rw [monomorphisms.iff] at hf hg ⊢

Premises used: CategoryTheory.MorphismProperty.monomorphisms.iff
-- Module: Mathlib.CategoryTheory.MorphismProperty.Composition
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : monomorphisms C f
hg : monomorphisms C g
hf₁ : Mono f
⊢ Mono g

Tactic:
rw [monomorphisms.iff] at hf hg ⊢

Premises used: CategoryTheory.MorphismProperty.monomorphisms.iff
-- Module: Mathlib.CategoryTheory.MorphismProperty.Composition
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : Mono f
hg : Mono g
⊢ Mono (f ≫ g)

Tactic:
apply mono_comp

Premises used: CategoryTheory.mono_comp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Composition
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : epimorphisms C f
hg : epimorphisms C g
⊢ Epi f

Tactic:
rw [epimorphisms.iff] at hf hg ⊢

Premises used: CategoryTheory.MorphismProperty.epimorphisms.iff
-- Module: Mathlib.CategoryTheory.MorphismProperty.Composition
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : epimorphisms C f
hg : epimorphisms C g
hf₁ : Epi f
⊢ Epi g

Tactic:
rw [epimorphisms.iff] at hf hg ⊢

Premises used: CategoryTheory.MorphismProperty.epimorphisms.iff
-- Module: Mathlib.CategoryTheory.MorphismProperty.Composition
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : Epi f
hg : Epi g
⊢ Epi (f ≫ g)

Tactic:
apply epi_comp

Premises used: CategoryTheory.epi_comp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Composition
Goal:
C : Type u
inst : Category.{v, u} C
W : Set (MorphismProperty.{v, u} C)
h : ∀ W' ∈ W, W'.IsMultiplicative
⊢ (InfSet.sInf W).ContainsIdentities

Tactic:
have := ContainsIdentities.sInf (fun W' hW' ↦ (h W' hW').toContainsIdentities)
-- Module: Mathlib.CategoryTheory.MorphismProperty.Composition
Goal:
C : Type u
inst : Category.{v, u} C
W : Set (MorphismProperty.{v, u} C)
h : ∀ W' ∈ W, W'.IsMultiplicative
this : (InfSet.sInf W).ContainsIdentities
⊢ (InfSet.sInf W).IsStableUnderComposition

Tactic:
have := IsStableUnderComposition.sInf (fun W' hW' ↦ (h W' hW').toIsStableUnderComposition)
-- Module: Mathlib.CategoryTheory.MorphismProperty.Composition
Goal:
C : Type u
inst : Category.{v, u} C
W : Set (MorphismProperty.{v, u} C)
h : ∀ W' ∈ W, W'.IsMultiplicative
this_1 : (InfSet.sInf W).ContainsIdentities
this : (InfSet.sInf W).IsStableUnderComposition
⊢ (InfSet.sInf W).IsMultiplicative

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.MorphismProperty.Composition
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
ι : Type u_1
W : ι → MorphismProperty.{v, u} C
inst_2 : ∀ (i : ι), (W i).IsMultiplicative
⊢ ∀ (W' : MorphismProperty.{v, u} C),
    Membership.mem (γ := Set (MorphismProperty.{v, u} C)) (Set.range fun (i : ι) ↦ W i) W' → W'.IsMultiplicative

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

Tactic:
exact sInf (by simpa)

Premises used: CategoryTheory.MorphismProperty.IsMultiplicative.sInf
-- Module: Mathlib.CategoryTheory.MorphismProperty.Composition
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F₁ F₂ : Functor.{v, v', u, u'} C D
app : (X : C) → F₁.obj X ⟶ F₂.obj X
x : C
⊢ MorphismProperty.naturalityProperty app (𝟙 x)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Composition
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
W : MorphismProperty.{v, u} C
X Y Z : C
g : Y ⟶ Z
x y : C
f_1 : x ⟶ y
hf₀ : W f_1
f : X ⟶ x
hf : W.multiplicativeClosure f
⊢ W.multiplicativeClosure (f ≫ f_1)

Tactic:
.comp_of f _ hf hf₀

Premises used: CategoryTheory.MorphismProperty.multiplicativeClosure.comp_of
-- Module: Mathlib.CategoryTheory.MorphismProperty.Composition
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
W : MorphismProperty.{v, u} C
X Y Z : C
g : Y ⟶ Z
x y : C
f_1 : x ⟶ y
hf₀ : W f_1
f : X ⟶ x
hf : W.multiplicativeClosure f
⊢ W.multiplicativeClosure (f ≫ f_1)

Tactic:
exact .comp_of f _ hf hf₀
-- Module: Mathlib.CategoryTheory.MorphismProperty.Composition
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
W : MorphismProperty.{v, u} C
X Y Z : C
g : Y ⟶ Z
x : C
f : X ⟶ x
hf id id₁ id₂ id₃ : W.multiplicativeClosure f
⊢ W.multiplicativeClosure (f ≫ 𝟙 x)

Tactic:
rwa [Category.comp_id]

Premises used: CategoryTheory.Category.comp_id
-- Module: Mathlib.CategoryTheory.MorphismProperty.Composition
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
W : MorphismProperty.{v, u} C
X Y Z : C
g_1 : Y ⟶ Z
x y z : C
f' : x ⟶ y
g : y ⟶ z
hf' : W.multiplicativeClosure f'
hg : W g
h_rec : ∀ (f : X ⟶ x) (hf : W.multiplicativeClosure f), W.multiplicativeClosure (f ≫ f')
f : X ⟶ x
hf : W.multiplicativeClosure f
comp_of : W.multiplicativeClosure ((f ≫ f') ≫ g)
⊢ W.multiplicativeClosure (f ≫ f' ≫ g)

Tactic:
rw [← Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.MorphismProperty.Composition
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
W : MorphismProperty.{v, u} C
X Y Z : C
g_1 : Y ⟶ Z
x y z : C
f' : x ⟶ y
g : y ⟶ z
hf' : W.multiplicativeClosure f'
hg : W g
h_rec : ∀ (f : X ⟶ x) (hf : W.multiplicativeClosure f), W.multiplicativeClosure (f ≫ f')
f : X ⟶ x
hf : W.multiplicativeClosure f
⊢ W.multiplicativeClosure ((f ≫ f') ≫ g)

Tactic:
.comp_of (f ≫ f') g (h_rec f hf) hg

Premises used: CategoryTheory.MorphismProperty.multiplicativeClosure.comp_of, CategoryTheory.CategoryStruct.comp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Composition
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
W : MorphismProperty.{v, u} C
X Y Z : C
g_1 : Y ⟶ Z
x y z : C
f' : x ⟶ y
g : y ⟶ z
hf' : W.multiplicativeClosure f'
hg : W g
h_rec : ∀ (f : X ⟶ x) (hf : W.multiplicativeClosure f), W.multiplicativeClosure (f ≫ f')
f : X ⟶ x
hf : W.multiplicativeClosure f
⊢ W.multiplicativeClosure ((f ≫ f') ≫ g)

Tactic:
exact .comp_of (f ≫ f') g (h_rec f hf) hg
-- Module: Mathlib.CategoryTheory.MorphismProperty.Composition
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
W : MorphismProperty.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : W.multiplicativeClosure f
hg : W.multiplicativeClosure g
of :
  ∀ {x y : C} (f : x ⟶ y) (hf₀ : W f) (f_1 : X ⟶ x) (hf : W.multiplicativeClosure f_1),
    W.multiplicativeClosure (f_1 ≫ f)
id : ∀ (x : C) (f : X ⟶ x) (hf : W.multiplicativeClosure f), W.multiplicativeClosure (f ≫ 𝟙 x)
comp_of :
  ∀ {x y z : C} (f' : x ⟶ y) (g : y ⟶ z) (hf' : W.multiplicativeClosure f') (hg : W g)
    (h_rec : ∀ (f : X ⟶ x) (hf : W.multiplicativeClosure f), W.multiplicativeClosure (f ≫ f')) (f : X ⟶ x)
    (hf : W.multiplicativeClosure f), W.multiplicativeClosure (f ≫ f' ≫ g)
⊢ W.multiplicativeClosure (f ≫ g)

Tactic:
induction hg with
    | of _ hf₀ => exact .comp_of f _ hf hf₀
    | id _ => rwa [Category.comp_id]
    | comp_of f' g hf' hg h_rec =>
      rw [← Category.assoc]
      exact .comp_of (f ≫ f') g (h_rec f hf) hg

Premises used: CategoryTheory.Category.assoc, id, CategoryTheory.Category.comp_id
-- Module: Mathlib.CategoryTheory.MorphismProperty.Composition
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
W : MorphismProperty.{v, u} C
X Y Z : C
f : X ⟶ Y
x y : C
f_1 : x ⟶ y
h : W f_1
g : y ⟶ Z
hg : W.multiplicativeClosure' g
⊢ W.multiplicativeClosure' (f_1 ≫ g)

Tactic:
.of_comp _ g h hg

Premises used: CategoryTheory.MorphismProperty.multiplicativeClosure'.of_comp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Composition
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
W : MorphismProperty.{v, u} C
X Y Z : C
f : X ⟶ Y
x y : C
f_1 : x ⟶ y
h : W f_1
g : y ⟶ Z
hg : W.multiplicativeClosure' g
⊢ W.multiplicativeClosure' (f_1 ≫ g)

Tactic:
exact .of_comp _ g h hg
-- Module: Mathlib.CategoryTheory.MorphismProperty.Composition
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
W : MorphismProperty.{v, u} C
X Y Z : C
f : X ⟶ Y
x : C
g : x ⟶ Z
hg id id₁ id₂ id₃ : W.multiplicativeClosure' g
⊢ W.multiplicativeClosure' (𝟙 x ≫ g)

Tactic:
rwa [Category.id_comp]

Premises used: CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Composition
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
W : MorphismProperty.{v, u} C
X Y Z : C
f_1 : X ⟶ Y
x y z : C
g' : x ⟶ y
f : y ⟶ z
hg' : W g'
hf : W.multiplicativeClosure' f
h_rec : ∀ (g : z ⟶ Z) (hg : W.multiplicativeClosure' g), W.multiplicativeClosure' (f ≫ g)
g : z ⟶ Z
hg : W.multiplicativeClosure' g
of_comp : W.multiplicativeClosure' (g' ≫ f ≫ g)
⊢ W.multiplicativeClosure' ((g' ≫ f) ≫ g)

Tactic:
rw [Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.MorphismProperty.Composition
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
W : MorphismProperty.{v, u} C
X Y Z : C
f_1 : X ⟶ Y
x y z : C
g' : x ⟶ y
f : y ⟶ z
hg' : W g'
hf : W.multiplicativeClosure' f
h_rec : ∀ (g : z ⟶ Z) (hg : W.multiplicativeClosure' g), W.multiplicativeClosure' (f ≫ g)
g : z ⟶ Z
hg : W.multiplicativeClosure' g
⊢ W.multiplicativeClosure' (g' ≫ f ≫ g)

Tactic:
.of_comp g' (f ≫ g) hg' (h_rec g hg)

Premises used: CategoryTheory.MorphismProperty.multiplicativeClosure'.of_comp, CategoryTheory.CategoryStruct.comp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Composition
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
W : MorphismProperty.{v, u} C
X Y Z : C
f_1 : X ⟶ Y
x y z : C
g' : x ⟶ y
f : y ⟶ z
hg' : W g'
hf : W.multiplicativeClosure' f
h_rec : ∀ (g : z ⟶ Z) (hg : W.multiplicativeClosure' g), W.multiplicativeClosure' (f ≫ g)
g : z ⟶ Z
hg : W.multiplicativeClosure' g
⊢ W.multiplicativeClosure' (g' ≫ f ≫ g)

Tactic:
exact .of_comp g' (f ≫ g) hg' (h_rec g hg)