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
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) (h : W f) (g : y ⟶ Z) (hg : W.multiplicativeClosure' g), W.multiplicativeClosure' (f ≫ g)
id : ∀ (x : C) (g : x ⟶ Z) (hg : W.multiplicativeClosure' g), W.multiplicativeClosure' (𝟙 x ≫ g)
of_comp :
  ∀ {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)
⊢ W.multiplicativeClosure' (f ≫ g)

Tactic:
induction hf with
    | of _ h => exact .of_comp _ g h hg
    | id _ => rwa [Category.id_comp]
    | of_comp g' f hg' hf h_rec =>
      rw [Category.assoc]
      exact .of_comp g' (f ≫ g) hg' (h_rec g hg)

Premises used: CategoryTheory.Category.assoc, id, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Composition
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
⊢ W ≤ W.multiplicativeClosure

Tactic:
fun {_ _} _ hf ↦ .of _ hf

Premises used: CategoryTheory.MorphismProperty.multiplicativeClosure.of
-- Module: Mathlib.CategoryTheory.MorphismProperty.Composition
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
inst_1 : W.IsMultiplicative
apply : W.multiplicativeClosure ≤ W
⊢ W.multiplicativeClosure = W

Tactic:
apply le_antisymm _ <| le_multiplicativeClosure W

Premises used: le_antisymm, CategoryTheory.MorphismProperty.le_multiplicativeClosure
-- Module: Mathlib.CategoryTheory.MorphismProperty.Composition
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
inst_1 : W.IsMultiplicative
X : C
_ : ∀ ⦃Y : C⦄ (f : X ⟶ Y), W.multiplicativeClosure f → W f
⊢ ∀ ⦃Y : C⦄ (f : X ⟶ Y), W.multiplicativeClosure f → W f

Tactic:
_
-- Module: Mathlib.CategoryTheory.MorphismProperty.Composition
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
inst_1 : W.IsMultiplicative
X Y : C
_ : ∀ (f : X ⟶ Y), W.multiplicativeClosure f → W f
⊢ ∀ (f : X ⟶ Y), W.multiplicativeClosure f → W f

Tactic:
_
-- Module: Mathlib.CategoryTheory.MorphismProperty.Composition
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
inst_1 : W.IsMultiplicative
X Y : C
f : X ⟶ Y
x y : C
f_1 : x ⟶ y
hf₀ : W f_1
⊢ W f_1

Tactic:
hf₀
-- Module: Mathlib.CategoryTheory.MorphismProperty.Composition
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
inst_1 : W.IsMultiplicative
X Y : C
f : X ⟶ Y
x y : C
f_1 : x ⟶ y
hf₀ : W f_1
⊢ W f_1

Tactic:
exact hf₀
-- Module: Mathlib.CategoryTheory.MorphismProperty.Composition
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
inst_1 : W.IsMultiplicative
X Y : C
f : X ⟶ Y
x : C
⊢ W (𝟙 x)

Tactic:
W.id_mem x

Premises used: CategoryTheory.MorphismProperty.id_mem
-- Module: Mathlib.CategoryTheory.MorphismProperty.Composition
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
inst_1 : W.IsMultiplicative
X Y : C
f : X ⟶ Y
x : C
⊢ W (𝟙 x)

Tactic:
exact W.id_mem x

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

Tactic:
W.comp_mem _ _ hf hg

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

Tactic:
exact W.comp_mem _ _ hf hg

Premises used: CategoryTheory.MorphismProperty.comp_mem
-- Module: Mathlib.CategoryTheory.MorphismProperty.Composition
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
inst_1 : W.IsMultiplicative
X Y : C
f : X ⟶ Y
hf : W.multiplicativeClosure f
of : ∀ {x y : C} (f : x ⟶ y) (hf₀ : W f), W f
id : ∀ (x : C), W (𝟙 x)
comp_of : ∀ {x y z : C} (f : x ⟶ y) (g : y ⟶ z), W.multiplicativeClosure f → ∀ (hg : W g) (hf : W f), W (f ≫ g)
⊢ W f

Tactic:
induction hf with
  | of _ hf₀ => exact hf₀
  | id x => exact W.id_mem x
  | comp_of _ _ _ hg hf => exact W.comp_mem _ _ hf hg

Premises used: id
-- Module: Mathlib.CategoryTheory.MorphismProperty.Composition
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
h : W.multiplicativeClosure = W
rw : W.multiplicativeClosure.IsMultiplicative
⊢ W.IsMultiplicative

Tactic:
rw [← h]
-- Module: Mathlib.CategoryTheory.MorphismProperty.Composition
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
h : W.multiplicativeClosure = W
⊢ W.multiplicativeClosure.IsMultiplicative

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.MorphismProperty.Composition
Goal:
C : Type u
inst : Category.{v, u} C
W W' : MorphismProperty.{v, u} C
inst_1 : W'.IsMultiplicative
h : W ≤ W'
X : C
_ : ∀ ⦃Y : C⦄ (f : X ⟶ Y), W.multiplicativeClosure f → W' f
⊢ ∀ ⦃Y : C⦄ (f : X ⟶ Y), W.multiplicativeClosure f → W' f

Tactic:
_
-- Module: Mathlib.CategoryTheory.MorphismProperty.Composition
Goal:
C : Type u
inst : Category.{v, u} C
W W' : MorphismProperty.{v, u} C
inst_1 : W'.IsMultiplicative
h : W ≤ W'
X Y : C
_ : ∀ (f : X ⟶ Y), W.multiplicativeClosure f → W' f
⊢ ∀ (f : X ⟶ Y), W.multiplicativeClosure f → W' f

Tactic:
_
-- Module: Mathlib.CategoryTheory.MorphismProperty.Composition
Goal:
C : Type u
inst : Category.{v, u} C
W W' : MorphismProperty.{v, u} C
inst_1 : W'.IsMultiplicative
h : W ≤ W'
X Y : C
f : X ⟶ Y
x y : C
f_1 : x ⟶ y
hf : W f_1
⊢ W' f_1

Tactic:
h _ hf
-- Module: Mathlib.CategoryTheory.MorphismProperty.Composition
Goal:
C : Type u
inst : Category.{v, u} C
W W' : MorphismProperty.{v, u} C
inst_1 : W'.IsMultiplicative
h : W ≤ W'
X Y : C
f : X ⟶ Y
x y : C
f_1 : x ⟶ y
hf : W f_1
⊢ W' f_1

Tactic:
exact h _ hf
-- Module: Mathlib.CategoryTheory.MorphismProperty.Composition
Goal:
C : Type u
inst : Category.{v, u} C
W W' : MorphismProperty.{v, u} C
inst_1 : W'.IsMultiplicative
h : W ≤ W'
X Y : C
f : X ⟶ Y
x : C
⊢ W' (𝟙 x)

Tactic:
W'.id_mem _

Premises used: CategoryTheory.MorphismProperty.id_mem
-- Module: Mathlib.CategoryTheory.MorphismProperty.Composition
Goal:
C : Type u
inst : Category.{v, u} C
W W' : MorphismProperty.{v, u} C
inst_1 : W'.IsMultiplicative
h : W ≤ W'
X Y : C
f : X ⟶ Y
x : C
⊢ W' (𝟙 x)

Tactic:
exact W'.id_mem _

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

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

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

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

Premises used: CategoryTheory.MorphismProperty.comp_mem
-- Module: Mathlib.CategoryTheory.MorphismProperty.Composition
Goal:
C : Type u
inst : Category.{v, u} C
W W' : MorphismProperty.{v, u} C
inst_1 : W'.IsMultiplicative
h : W ≤ W'
X Y : C
f : X ⟶ Y
hf : W.multiplicativeClosure f
of : ∀ {x y : C} (f : x ⟶ y) (hf : W f), W' f
id : ∀ (x : C), W' (𝟙 x)
comp_of : ∀ {x y z : C} (f : x ⟶ y) (g : y ⟶ z), W.multiplicativeClosure f → ∀ (hg : W g) (hf : W' f), W' (f ≫ g)
⊢ W' f

Tactic:
induction hf with
    | of _ hf => exact h _ hf
    | id x => exact W'.id_mem _
    | comp_of _ _ _ hg hf => exact W'.comp_mem _ _ hf (h _ hg)

Premises used: id, CategoryTheory.MorphismProperty.id_mem
-- Module: Mathlib.CategoryTheory.MorphismProperty.Composition
Goal:
C : Type u
inst : Category.{v, u} C
x W' : MorphismProperty.{v, u} C
h : x ≤ W'
⊢ x.multiplicativeClosure ≤ W'.multiplicativeClosure

Tactic:
simpa using h.trans W'.le_multiplicativeClosure

Premises used: LE.le.trans, CategoryTheory.MorphismProperty.le_multiplicativeClosure
-- Module: Mathlib.CategoryTheory.MorphismProperty.Composition
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
x y : C
f : x ⟶ y
x_1 y_1 : C
f_1 : x_1 ⟶ y_1
h : W f_1
⊢ W.multiplicativeClosure f_1

Tactic:
.of _ h

Premises used: CategoryTheory.MorphismProperty.multiplicativeClosure.of
-- Module: Mathlib.CategoryTheory.MorphismProperty.Composition
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
x y : C
f : x ⟶ y
x_1 y_1 : C
f_1 : x_1 ⟶ y_1
h : W f_1
⊢ W.multiplicativeClosure f_1

Tactic:
exact .of _ h
-- Module: Mathlib.CategoryTheory.MorphismProperty.Composition
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
x_1 y : C
f : x_1 ⟶ y
x : C
⊢ W.multiplicativeClosure (𝟙 x)

Tactic:
.id x

Premises used: CategoryTheory.MorphismProperty.multiplicativeClosure.id
-- Module: Mathlib.CategoryTheory.MorphismProperty.Composition
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
x_1 y : C
f : x_1 ⟶ y
x : C
⊢ W.multiplicativeClosure (𝟙 x)

Tactic:
exact .id x
-- Module: Mathlib.CategoryTheory.MorphismProperty.Composition
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
x y : C
f_1 : x ⟶ y
x_1 y_1 z : C
f : x_1 ⟶ y_1
g : y_1 ⟶ z
hf : W f
hg : W.multiplicativeClosure' g
hr : W.multiplicativeClosure g
⊢ W.multiplicativeClosure (f ≫ g)

Tactic:
W.multiplicativeClosure.comp_mem f g (.of f hf) hr

Premises used: CategoryTheory.MorphismProperty.multiplicativeClosure, CategoryTheory.MorphismProperty.multiplicativeClosure.of, CategoryTheory.MorphismProperty.comp_mem
-- Module: Mathlib.CategoryTheory.MorphismProperty.Composition
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
x y : C
f_1 : x ⟶ y
x_1 y_1 z : C
f : x_1 ⟶ y_1
g : y_1 ⟶ z
hf : W f
hg : W.multiplicativeClosure' g
hr : W.multiplicativeClosure g
⊢ W.multiplicativeClosure (f ≫ g)

Tactic:
exact W.multiplicativeClosure.comp_mem f g (.of f hf) hr

Premises used: CategoryTheory.MorphismProperty.multiplicativeClosure, CategoryTheory.MorphismProperty.multiplicativeClosure.of, CategoryTheory.MorphismProperty.comp_mem
-- Module: Mathlib.CategoryTheory.MorphismProperty.Composition
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
x y : C
f : x ⟶ y
hf : W.multiplicativeClosure' f
of : ∀ {x y : C} (f : x ⟶ y) (h : W f), W.multiplicativeClosure f
id : ∀ (x : C), W.multiplicativeClosure (𝟙 x)
of_comp :
  ∀ {x y z : C} (f : x ⟶ y) (g : y ⟶ z) (hf : W f) (hg : W.multiplicativeClosure' g) (hr : W.multiplicativeClosure g),
    W.multiplicativeClosure (f ≫ g)
⊢ W.multiplicativeClosure f

Tactic:
induction hf with
      | of _ h => exact .of _ h
      | id x => exact .id x
      | of_comp f g hf hg hr => exact W.multiplicativeClosure.comp_mem f g (.of f hf) hr

Premises used: 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
F : Functor.{v, v', u, u'} C D
X : D
_ : ∀ ⦃Y : D⦄ (f : X ⟶ Y), W.multiplicativeClosure.strictMap F f → (W.strictMap F).multiplicativeClosure f
⊢ ∀ ⦃Y : D⦄ (f : X ⟶ Y), W.multiplicativeClosure.strictMap F f → (W.strictMap F).multiplicativeClosure f

Tactic:
_
-- 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
F : Functor.{v, v', u, u'} C D
X Y : D
f : X ⟶ Y
hf : W.multiplicativeClosure.strictMap F f
map : ∀ {X Y : C} {f : X ⟶ Y} (hf : W.multiplicativeClosure f), (W.strictMap F).multiplicativeClosure (F.map f)
⊢ (W.strictMap F).multiplicativeClosure f

Tactic:
induction hf with | map hf

Premises used: CategoryTheory.MorphismProperty.map
-- 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
F : Functor.{v, v', u, u'} C D
X Y : D
f_1 : X ⟶ Y
X_1 Y_1 : C
f_2 : X_1 ⟶ Y_1
x y : C
f : x ⟶ y
hf : W f
⊢ (W.strictMap F).multiplicativeClosure (F.map f)

Tactic:
le_multiplicativeClosure _ _ ⟨hf⟩

Premises used: CategoryTheory.MorphismProperty.strictMap.map, CategoryTheory.MorphismProperty.le_multiplicativeClosure
-- 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
F : Functor.{v, v', u, u'} C D
X Y : D
f_1 : X ⟶ Y
X_1 Y_1 : C
f_2 : X_1 ⟶ Y_1
x y : C
f : x ⟶ y
hf : W f
⊢ (W.strictMap F).multiplicativeClosure (F.map f)

Tactic:
exact le_multiplicativeClosure _ _ ⟨hf⟩

Premises used: CategoryTheory.MorphismProperty.le_multiplicativeClosure
-- 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
F : Functor.{v, v', u, u'} C D
X Y : D
f : X ⟶ Y
X_1 Y_1 : C
f_1 : X_1 ⟶ Y_1
x : C
⊢ (W.strictMap F).multiplicativeClosure (F.map (𝟙 x))

Tactic:
simpa using .id (F.obj x)
-- 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
F : Functor.{v, v', u, u'} C D
X Y : D
f : X ⟶ Y
X_1 Y_1 : C
f_1 : X_1 ⟶ Y_1
x y z : C
f_2 : x ⟶ y
g : y ⟶ z
hf : W.multiplicativeClosure f_2
hg : W g
h : (W.strictMap F).multiplicativeClosure (F.map f_2)
⊢ (W.strictMap F).multiplicativeClosure (F.map (f_2 ≫ g))

Tactic:
simpa using multiplicativeClosure.comp_of _ _ h (strictMap.map hg)

Premises used: CategoryTheory.MorphismProperty.multiplicativeClosure.comp_of, CategoryTheory.MorphismProperty.strictMap.map
-- 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
F : Functor.{v, v', u, u'} C D
X Y : D
f : X ⟶ Y
X_1 Y_1 : C
f_1 : X_1 ⟶ Y_1
hf : W.multiplicativeClosure f_1
map : ∀ {x y : C} (f : x ⟶ y) (hf : W f), (W.strictMap F).multiplicativeClosure (F.map f)
map₁ : ∀ (x : C), (W.strictMap F).multiplicativeClosure (F.map (𝟙 x))
map₂ :
  ∀ {x y z : C} (f : x ⟶ y) (g : y ⟶ z) (hf : W.multiplicativeClosure f) (hg : W g)
    (h : (W.strictMap F).multiplicativeClosure (F.map f)), (W.strictMap F).multiplicativeClosure (F.map (f ≫ g))
⊢ (W.strictMap F).multiplicativeClosure (F.map f_1)

Tactic:
induction hf with
  | of f hf => exact le_multiplicativeClosure _ _ ⟨hf⟩
  | id x => simpa using .id (F.obj x)
  | comp_of _ _ hf hg h =>
    simpa using multiplicativeClosure.comp_of _ _ h (strictMap.map hg)

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

Tactic:
HasOfPostcompProperty.of_postcomp f g hg hfg

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

Tactic:
HasOfPrecompProperty.of_precomp f g hf hfg

Premises used: CategoryTheory.MorphismProperty.HasOfPrecompProperty.of_precomp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Composition
Goal:
C : Type u
inst : Category.{v, u} C
W W' : MorphismProperty.{v, u} C
inst_1 : W.RespectsRight W'
inst_2 : W.HasOfPostcompProperty W'
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hg : W' g
⊢ W (f ≫ g) ↔ W f

Tactic:
⟨W.of_postcomp f g hg, fun hf ↦ RespectsRight.postcomp _ hg _ hf⟩

Premises used: CategoryTheory.MorphismProperty.RespectsRight.postcomp, Iff.intro, CategoryTheory.MorphismProperty.of_postcomp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Composition
Goal:
C : Type u
inst : Category.{v, u} C
W W' : MorphismProperty.{v, u} C
inst_1 : W.RespectsLeft W'
inst_2 : W.HasOfPrecompProperty W'
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : W' f
⊢ W (f ≫ g) ↔ W g

Tactic:
⟨W.of_precomp f g hf, fun hg ↦ RespectsLeft.precomp _ hf _ hg⟩

Premises used: CategoryTheory.MorphismProperty.RespectsLeft.precomp, CategoryTheory.MorphismProperty.of_precomp, Iff.intro
-- Module: Mathlib.CategoryTheory.MorphismProperty.Composition
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
W_1 W W'_1 : MorphismProperty.{v, u} C
W' : ?m.4
P Q : MorphismProperty.{v, u} C
inst_2 : P.HasTwoOutOfThreeProperty
inst_3 : Q.HasTwoOutOfThreeProperty
⊢ P.HasOfPostcompProperty (P ⊓ Q)

Tactic:
have : P.HasOfPostcompProperty (P ⊓ Q) := .of_le _ _ inf_le_left
-- Module: Mathlib.CategoryTheory.MorphismProperty.Composition
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
W_1 W W'_1 : MorphismProperty.{v, u} C
W' : ?m.4
P Q : MorphismProperty.{v, u} C
inst_2 : P.HasTwoOutOfThreeProperty
inst_3 : Q.HasTwoOutOfThreeProperty
this : P.HasOfPostcompProperty (P ⊓ Q)
⊢ P.HasOfPrecompProperty (P ⊓ Q)

Tactic:
have : P.HasOfPrecompProperty (P ⊓ Q) := .of_le _ _ inf_le_left
-- Module: Mathlib.CategoryTheory.MorphismProperty.Composition
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
W_1 W W'_1 : MorphismProperty.{v, u} C
W' : ?m.4
P Q : MorphismProperty.{v, u} C
inst_2 : P.HasTwoOutOfThreeProperty
inst_3 : Q.HasTwoOutOfThreeProperty
this_1 : P.HasOfPostcompProperty (P ⊓ Q)
this : P.HasOfPrecompProperty (P ⊓ Q)
⊢ Q.HasOfPostcompProperty (P ⊓ Q)

Tactic:
have : Q.HasOfPostcompProperty (P ⊓ Q) := .of_le _ _ inf_le_right
-- Module: Mathlib.CategoryTheory.MorphismProperty.Composition
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
W_1 W W'_1 : MorphismProperty.{v, u} C
W' : ?m.4
P Q : MorphismProperty.{v, u} C
inst_2 : P.HasTwoOutOfThreeProperty
inst_3 : Q.HasTwoOutOfThreeProperty
this_1 : P.HasOfPostcompProperty (P ⊓ Q)
this_2 : P.HasOfPrecompProperty (P ⊓ Q)
this : Q.HasOfPostcompProperty (P ⊓ Q)
⊢ Q.HasOfPrecompProperty (P ⊓ Q)

Tactic:
have : Q.HasOfPrecompProperty (P ⊓ Q) := .of_le _ _ inf_le_right
-- Module: Mathlib.CategoryTheory.MorphismProperty.Composition
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
W_1 W W'_1 : MorphismProperty.{v, u} C
W' : ?m.4
P Q : MorphismProperty.{v, u} C
inst_2 : P.HasTwoOutOfThreeProperty
inst_3 : Q.HasTwoOutOfThreeProperty
this_1 : P.HasOfPostcompProperty (P ⊓ Q)
this_2 : P.HasOfPrecompProperty (P ⊓ Q)
this_3 : Q.HasOfPostcompProperty (P ⊓ Q)
this : Q.HasOfPrecompProperty (P ⊓ Q)
⊢ (P ⊓ Q).HasTwoOutOfThreeProperty

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
W : MorphismProperty.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hg : IsIso g
hfg : IsIso (f ≫ g)
⊢ isomorphisms C f

Tactic:
simpa using (inferInstance : IsIso ((f ≫ g) ≫ inv g))

Premises used: inferInstance
-- 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 : IsIso f
hfg : IsIso (f ≫ g)
⊢ isomorphisms C g

Tactic:
simpa using (inferInstance : IsIso (inv f ≫ (f ≫ g)))

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.MorphismProperty.Composition
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
W_1 : MorphismProperty.{v, u} C
F : Functor.{v, v', u, u'} C D
W : MorphismProperty.{v', u'} D
inst_2 : W.HasTwoOutOfThreeProperty
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hg : W.inverseImage F g
hfg : W.inverseImage F (f ≫ g)
⊢ W (F.map f ≫ F.map g)

Tactic:
simpa using hfg
-- Module: Mathlib.CategoryTheory.MorphismProperty.Composition
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
W_1 : MorphismProperty.{v, u} C
F : Functor.{v, v', u, u'} C D
W : MorphismProperty.{v', u'} D
inst_2 : W.HasTwoOutOfThreeProperty
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : W.inverseImage F f
hfg : W.inverseImage F (f ≫ g)
⊢ W (F.map f ≫ F.map g)

Tactic:
simpa using hfg
-- Module: Mathlib.CategoryTheory.MorphismProperty.Concrete
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst_1 : (X Y : C) → FunLike.{u_1 + 1, u_2 + 1, u_2 + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{u_2, v, u, u_1} C FC (CC := CC)
⊢ Eq (α := MorphismProperty.{v, u} C) (MorphismProperty.bijective C (FC := FC) (CC := CC))
    (MorphismProperty.injective C (FC := FC) (CC := CC) ⊓ MorphismProperty.surjective C (FC := FC) (CC := CC))

Tactic:
rfl

Premises used: CategoryTheory.MorphismProperty.bijective, CategoryTheory.MorphismProperty.injective, Function.Bijective, rfl, CategoryTheory.MorphismProperty.surjective
-- Module: Mathlib.CategoryTheory.MorphismProperty.Concrete
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst_1 : (X Y : C) → FunLike.{u_1 + 1, u_2 + 1, u_2 + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{u_2, v, u, u_1} C FC (CC := CC)
X : C
⊢ Injective.{u_2 + 1, u_2 + 1} (α := CC X) id

Tactic:
injective_id

Premises used: Function.injective_id
-- Module: Mathlib.CategoryTheory.MorphismProperty.Concrete
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst_1 : (X Y : C) → FunLike.{u_1 + 1, u_2 + 1, u_2 + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{u_2, v, u, u_1} C FC (CC := CC)
X : C
h :
  Eq.{u_2 + 1} (α := CC X → CC X)
    (⇑(@ConcreteCategory.hom.{u_2, v, u, u_1} _ inst FC CC _ _ _ _ (𝟙 X)) : (a : CC X) → CC X) id
⊢ Injective.{u_2 + 1, u_2 + 1} (α := CC X) (β := CC X)
    (⇑(@ConcreteCategory.hom.{u_2, v, u, u_1} _ inst FC CC _ _ _ _ (𝟙 X)) : (a : CC X) → CC X)

Tactic:
convert! injective_id

Premises used: Function.injective_id
-- Module: Mathlib.CategoryTheory.MorphismProperty.Concrete
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst_1 : (X Y : C) → FunLike.{u_1 + 1, u_2 + 1, u_2 + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{u_2, v, u, u_1} C FC (CC := CC)
X : C
⊢ Eq.{u_2 + 1} (α := CC X → CC X)
    (⇑(@ConcreteCategory.hom.{u_2, v, u, u_1} _ inst FC CC _ _ _ _ (𝟙 X)) : (a : CC X) → CC X) id

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.MorphismProperty.Concrete
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst_1 : (X Y : C) → FunLike.{u_1 + 1, u_2 + 1, u_2 + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{u_2, v, u, u_1} C FC (CC := CC)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : MorphismProperty.injective C (FC := FC) (CC := CC) f
hg : MorphismProperty.injective C (FC := FC) (CC := CC) g
rw :
  Injective.{u_2 + 1, u_2 + 1} (α := CC X) (β := CC Z)
    (Function.comp (β := CC Y) (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) g) : (a : CC Y) → CC Z)
      (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) f) : (a : CC X) → CC Y))
⊢ Injective.{u_2 + 1, u_2 + 1} (α := CC X) (β := CC Z)
    (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (f ≫ g)) : (a : CC X) → CC Z)

Tactic:
rw [hom_comp]

Premises used: CategoryTheory.hom_comp