awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.CommaSites (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : MorphismProperty.{v_1, u_1} C
S : C
inst_1 : P.IsStableUnderComposition
K : Precoverage.{v_1, u_1} C
inst_2 : K.HasIsos
inst_3 : K.IsStableUnderBaseChange
inst_4 : K.IsStableUnderComposition
inst_5 : K.HasPullbacks
H : K ≤ P.precoverage
X : P.Over ⊤ S
R : Presieve (Functor.obj (Over.forget P ⊤ S) X)
hR :
  Membership.mem (γ := Set (Presieve (Functor.obj (Over.forget P ⊤ S) X)))
    ((Precoverage.comap (CategoryTheory.Over.forget S) K).coverings (Functor.obj (Over.forget P ⊤ S) X)) R
⊢ Membership.mem (γ := Set (Presieve (Functor.obj (Over.forget P ⊤ S) X)))
    ((Precoverage.comap (CategoryTheory.Over.forget S) K).coverings (Functor.obj (Over.forget P ⊤ S) X))
    (Presieve.map (Over.forget P ⊤ S) (Presieve.functorPullback (Over.forget P ⊤ S) R))
have H₁ : ∀ (R : Presieve X)
  (hR :
    Membership.mem (γ := Set (Presieve (Functor.obj (Over.forget P ⊤ S) X)))
      ((Precoverage.comap (CategoryTheory.Over.forget S) K).coverings (Functor.obj (Over.forget P ⊤ S) X))
      (Presieve.map (Over.forget P ⊤ S) R)),
  Membership.mem (γ := Set (Presieve (Functor.obj (Over.forget P ⊤ S) X)))
    ((Precoverage.comap (CategoryTheory.Over.forget S) K).coverings (Functor.obj (Over.forget P ⊤ S) X))
    (Presieve.map (Over.forget P ⊤ S)
      (Presieve.functorPullback (Over.forget P ⊤ S) (Presieve.map (Over.forget P ⊤ S) R)))
Tactic: obtain ⟨R, rfl⟩ := MorphismProperty.exists_map_eq_of_presieve _ H hR
Cleared hypotheses: R, hR
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.CommaSites (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : MorphismProperty.{v_1, u_1} C
S : C
inst_1 : P.IsStableUnderComposition
K : Precoverage.{v_1, u_1} C
inst_2 : K.HasIsos
inst_3 : K.IsStableUnderBaseChange
inst_4 : K.IsStableUnderComposition
inst_5 : K.HasPullbacks
H : K ≤ P.precoverage
⊢ Functor.LocallyCoverDense (C := P.Over ⊤ S) (Over.forget P ⊤ S)
    (Precoverage.comap (CategoryTheory.Over.forget S) K).toGrothendieck
have rw : Functor.LocallyCoverDense (C := P.Over ⊤ S) (Over.forget P ⊤ S) (K.toGrothendieck.over S)
Tactic: rw [← over_toGrothendieck_eq_toGrothendieck_comap_forget]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.CommaSites (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : MorphismProperty.{v_1, u_1} C
S : C
inst_1 : P.IsStableUnderComposition
K : Precoverage.{v_1, u_1} C
inst_2 : K.HasIsos
inst_3 : K.IsStableUnderBaseChange
inst_4 : K.IsStableUnderComposition
inst_5 : K.HasPullbacks
H : K ≤ P.precoverage
⊢ Eq (α := GrothendieckTopology (P.Over ⊤ S))
    (Precoverage.toGrothendieck (Precoverage.comap (Over.forget P ⊤ S ⋙ CategoryTheory.Over.forget S) K))
    (Functor.inducedTopology (Over.forget P ⊤ S) (K.toGrothendieck.over S))
have this : Functor.LocallyCoverDense (C := P.Over ⊤ S) (Over.forget P ⊤ S)
  (Precoverage.comap (CategoryTheory.Over.forget S) K).toGrothendieck
Tactic: have : (Over.forget P ⊤ S).LocallyCoverDense
      (K.comap (CategoryTheory.Over.forget S)).toGrothendieck := by
    rw [← over_toGrothendieck_eq_toGrothendieck_comap_forget]
    exact MorphismProperty.locallyCoverDense_forget_of_le (S := S) K H
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.CommaSites (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : MorphismProperty.{v_1, u_1} C
S : C
inst_1 : P.IsStableUnderComposition
K : Precoverage.{v_1, u_1} C
inst_2 : K.HasIsos
inst_3 : K.IsStableUnderBaseChange
inst_4 : K.IsStableUnderComposition
inst_5 : K.HasPullbacks
H : K ≤ P.precoverage
this :
  Functor.LocallyCoverDense (C := P.Over ⊤ S) (Over.forget P ⊤ S)
    (Precoverage.comap (CategoryTheory.Over.forget S) K).toGrothendieck
⊢ Eq (α := GrothendieckTopology (P.Over ⊤ S))
    (Precoverage.toGrothendieck (Precoverage.comap (Over.forget P ⊤ S ⋙ CategoryTheory.Over.forget S) K))
    (Functor.inducedTopology (Over.forget P ⊤ S) (K.toGrothendieck.over S))
have rw : Eq (α := GrothendieckTopology (P.Over ⊤ S))
  (Precoverage.toGrothendieck
    (Precoverage.comap (Over.forget P ⊤ S) (Precoverage.comap (CategoryTheory.Over.forget S) K)))
  (Functor.inducedTopology (Over.forget P ⊤ S) (K.toGrothendieck.over S))
Tactic: rw [Precoverage.comap_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.CommaSites (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : MorphismProperty.{v_1, u_1} C
S : C
inst_1 : P.IsStableUnderComposition
K : Precoverage.{v_1, u_1} C
inst_2 : K.HasIsos
inst_3 : K.IsStableUnderBaseChange
inst_4 : K.IsStableUnderComposition
inst_5 : K.HasPullbacks
H : K ≤ P.precoverage
this :
  Functor.LocallyCoverDense (C := P.Over ⊤ S) (Over.forget P ⊤ S)
    (Precoverage.comap (CategoryTheory.Over.forget S) K).toGrothendieck
⊢ Eq (α := GrothendieckTopology (P.Over ⊤ S))
    (Precoverage.toGrothendieck
      (Precoverage.comap (Over.forget P ⊤ S) (Precoverage.comap (CategoryTheory.Over.forget S) K)))
    (Functor.inducedTopology (Over.forget P ⊤ S) (K.toGrothendieck.over S))
have simp_rw : Eq (α := GrothendieckTopology (P.Over ⊤ S))
  (Precoverage.toGrothendieck
    (Precoverage.comap (Over.forget P ⊤ S) (Precoverage.comap (CategoryTheory.Over.forget S) K)))
  (Functor.inducedTopology (Over.forget P ⊤ S) (Precoverage.comap (CategoryTheory.Over.forget S) K).toGrothendieck)
Tactic: simp_rw [over_toGrothendieck_eq_toGrothendieck_comap_forget]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.CommaSites (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : MorphismProperty.{v_1, u_1} C
S : C
inst_1 : P.IsStableUnderComposition
K : Precoverage.{v_1, u_1} C
inst_2 : K.HasIsos
inst_3 : K.IsStableUnderBaseChange
inst_4 : K.IsStableUnderComposition
inst_5 : K.HasPullbacks
H : K ≤ P.precoverage
this :
  Functor.LocallyCoverDense (C := P.Over ⊤ S) (Over.forget P ⊤ S)
    (Precoverage.comap (CategoryTheory.Over.forget S) K).toGrothendieck
⊢ Eq (α := GrothendieckTopology (P.Over ⊤ S))
    (Precoverage.toGrothendieck
      (Precoverage.comap (Over.forget P ⊤ S) (Precoverage.comap (CategoryTheory.Over.forget S) K)))
    (Functor.inducedTopology (Over.forget P ⊤ S) (Precoverage.comap (CategoryTheory.Over.forget S) K).toGrothendieck)
have H₁ : ∀ {S_1 : P.Over ⊤ S} {R : Presieve (Functor.obj (Over.forget P ⊤ S) S_1)},
  Membership.mem (γ := Set (Presieve (Functor.obj (Over.forget P ⊤ S) S_1)))
      ((Precoverage.comap (CategoryTheory.Over.forget S) K).coverings (Functor.obj (Over.forget P ⊤ S) S_1)) R →
    Membership.mem (γ := Set (Presieve (Functor.obj (Over.forget P ⊤ S) S_1)))
      ((Precoverage.comap (CategoryTheory.Over.forget S) K).coverings (Functor.obj (Over.forget P ⊤ S) S_1))
      (Presieve.map (Over.forget P ⊤ S) (Presieve.functorPullback (Over.forget P ⊤ S) R))
Tactic: apply Precoverage.toGrothendieck_comap_eq_inducedTopology
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.CommaSites (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : MorphismProperty.{v_1, u_1} C
S : C
inst_1 : P.IsStableUnderComposition
K : Precoverage.{v_1, u_1} C
inst_2 : K.HasIsos
inst_3 : K.IsStableUnderBaseChange
inst_4 : K.IsStableUnderComposition
inst_5 : K.HasPullbacks
H : K ≤ P.precoverage
this :
  Functor.LocallyCoverDense (C := P.Over ⊤ S) (Over.forget P ⊤ S)
    (Precoverage.comap (CategoryTheory.Over.forget S) K).toGrothendieck
X : P.Over ⊤ S
R : Presieve (Functor.obj (Over.forget P ⊤ S) X)
hR :
  Membership.mem (γ := Set (Presieve (Functor.obj (Over.forget P ⊤ S) X)))
    ((Precoverage.comap (CategoryTheory.Over.forget S) K).coverings (Functor.obj (Over.forget P ⊤ S) X)) R
⊢ Membership.mem (γ := Set (Presieve (Functor.obj (Over.forget P ⊤ S) X)))
    ((Precoverage.comap (CategoryTheory.Over.forget S) K).coverings (Functor.obj (Over.forget P ⊤ S) X))
    (Presieve.map (Over.forget P ⊤ S) (Presieve.functorPullback (Over.forget P ⊤ S) R))
have H₁ : ∀ (T : Presieve X)
  (hR :
    Membership.mem (γ := Set (Presieve (Functor.obj (Over.forget P ⊤ S) X)))
      ((Precoverage.comap (CategoryTheory.Over.forget S) K).coverings (Functor.obj (Over.forget P ⊤ S) X))
      (Presieve.map (Over.forget P ⊤ S) T)),
  Membership.mem (γ := Set (Presieve (Functor.obj (Over.forget P ⊤ S) X)))
    ((Precoverage.comap (CategoryTheory.Over.forget S) K).coverings (Functor.obj (Over.forget P ⊤ S) X))
    (Presieve.map (Over.forget P ⊤ S)
      (Presieve.functorPullback (Over.forget P ⊤ S) (Presieve.map (Over.forget P ⊤ S) T)))
Tactic: obtain ⟨T, rfl⟩ := MorphismProperty.exists_map_eq_of_presieve K H hR
Cleared hypotheses: R, hR
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Composition (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
inst_1 : W.ContainsIdentities
x y : C
h : x = y
⊢ W (CategoryTheory.eqToHom h)
have subst : W (CategoryTheory.eqToHom sorry)
Tactic: subst h
Cleared hypotheses: y, h
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Composition (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
inst_1 : W.ContainsIdentities
x : C
⊢ W (CategoryTheory.eqToHom ⋯)
have rw : W (𝟙 x)
Tactic: rw [eqToHom_refl]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Composition (goal)
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
⊢ InfSet.sInf W (f ≫ g)
have rw : ∀ (hf : ∀ W_1 ∈ W, W_1 f) (hg : ∀ W_1 ∈ W, W_1 g), ∀ W_1 ∈ W, W_1 (f ≫ g)
Tactic: rw [sInf_iff] at hf hg ⊢
Cleared hypotheses: hf, hg
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Composition (goal)
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
⊢ F₁.map (f ≫ g) ≫ app Z = app X ≫ F₂.map (f ≫ g)
have simp : F₁.map f ≫ app Y ≫ F₂.map g = app X ≫ F₂.map f ≫ F₂.map g
Tactic: simp only [Functor.map_comp, Category.assoc, hg]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Composition (goal)
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
| F₁.map f ≫ app Y
have a : app X ≫ F₂.map f
Tactic: rw [hf]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Composition (goal)
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
⊢ F₁.map f ≫ app Y ≫ F₂.map g = app X ≫ F₂.map f ≫ F₂.map g
have slice_lhs : (app X ≫ F₂.map f) ≫ F₂.map g = app X ≫ F₂.map f ≫ F₂.map g
Tactic: slice_lhs 1 2 => rw [hf]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Composition (goal)
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
⊢ (app X ≫ F₂.map f) ≫ F₂.map g = app X ≫ F₂.map f ≫ F₂.map g
have rw : app X ≫ F₂.map f ≫ F₂.map g = app X ≫ F₂.map f ≫ F₂.map g
Tactic: rw [Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Composition (goal)
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.inv ≫ app X = app Y ≫ F₂.map e.inv
have rw : F₁.map e.hom ≫ F₁.map e.inv ≫ app X = F₁.map e.hom ≫ app Y ≫ F₂.map e.inv
Tactic: rw [← cancel_epi (F₁.map e.hom)]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Composition (goal)
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 ≫ app Y
have a : app X ≫ F₂.map e.hom
Tactic: rw [he]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Composition (goal)
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 = F₁.map e.hom ≫ app Y ≫ F₂.map e.inv
have slice_rhs : F₁.map e.hom ≫ F₁.map e.inv ≫ app X = (app X ≫ F₂.map e.hom) ≫ F₂.map e.inv
Tactic: slice_rhs 1 2 => rw [he]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Composition (hypothesis)
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
⊢ isomorphisms C (f ≫ g)
have hf₁ : IsIso f
Tactic: rw [isomorphisms.iff] at hf hg ⊢
Cleared hypotheses: hf, hg
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Composition (hypothesis)
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
⊢ isomorphisms C (f ≫ g)
have hg₁ : IsIso g
Tactic: rw [isomorphisms.iff] at hf hg ⊢
Cleared hypotheses: hf, hg
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Composition (hypothesis)
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
⊢ monomorphisms C (f ≫ g)
have hf₁ : Mono f
Tactic: rw [monomorphisms.iff] at hf hg ⊢
Cleared hypotheses: hf, hg
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Composition (hypothesis)
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
⊢ monomorphisms C (f ≫ g)
have hg₁ : Mono g
Tactic: rw [monomorphisms.iff] at hf hg ⊢
Cleared hypotheses: hf, hg
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Composition (hypothesis)
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
⊢ epimorphisms C (f ≫ g)
have hf₁ : Epi f
Tactic: rw [epimorphisms.iff] at hf hg ⊢
Cleared hypotheses: hf, hg
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Composition (hypothesis)
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
⊢ epimorphisms C (f ≫ g)
have hg₁ : Epi g
Tactic: rw [epimorphisms.iff] at hf hg ⊢
Cleared hypotheses: hf, hg
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Composition (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
W : Set (MorphismProperty.{v, u} C)
h : ∀ W' ∈ W, W'.IsMultiplicative
⊢ (InfSet.sInf W).IsMultiplicative
have this : (InfSet.sInf W).ContainsIdentities
Tactic: have := ContainsIdentities.sInf (fun W' hW' ↦ (h W' hW').toContainsIdentities)
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Composition (hypothesis)
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).IsMultiplicative
have this₁ : (InfSet.sInf W).IsStableUnderComposition
Tactic: have := IsStableUnderComposition.sInf (fun W' hW' ↦ (h W' hW').toIsStableUnderComposition)
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Composition (goal)
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)
have comp_of : W.multiplicativeClosure ((f ≫ f') ≫ g)
Tactic: rw [← Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Composition (goal)
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
⊢ W.multiplicativeClosure (f ≫ g)
have of : ∀ {x y : C} (f : x ⟶ y) (hf₀ : W f) (f_1 : X ⟶ x) (hf : W.multiplicativeClosure f_1), W.multiplicativeClosure (f_1 ≫ f)
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
Cleared hypotheses: f, hf, hg
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Composition (goal)
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)
⊢ W.multiplicativeClosure (f ≫ g)
have id : ∀ (x : C) (f : X ⟶ x) (hf : W.multiplicativeClosure f), W.multiplicativeClosure (f ≫ 𝟙 x)
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
Cleared hypotheses: f, hf, hg
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Composition (goal)
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)
⊢ W.multiplicativeClosure (f ≫ g)
have 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)
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
Cleared hypotheses: f, hf, hg
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Composition (goal)
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)
have of_comp : W.multiplicativeClosure' (g' ≫ f ≫ g)
Tactic: rw [Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Composition (goal)
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
⊢ W.multiplicativeClosure' (f ≫ g)
have of : ∀ {x y : C} (f : x ⟶ y) (h : W f) (g : y ⟶ Z) (hg : W.multiplicativeClosure' 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)
Cleared hypotheses: g, hf, hg
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Composition (goal)
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)
⊢ W.multiplicativeClosure' (f ≫ g)
have id : ∀ (x : C) (g : x ⟶ Z) (hg : W.multiplicativeClosure' g), W.multiplicativeClosure' (𝟙 x ≫ 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)
Cleared hypotheses: g, hf, hg
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Composition (goal)
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)
⊢ W.multiplicativeClosure' (f ≫ g)
have 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)
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)
Cleared hypotheses: g, hf, hg
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Composition (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
inst_1 : W.IsMultiplicative
⊢ W.multiplicativeClosure = W
have apply : W.multiplicativeClosure ≤ W
Tactic: apply le_antisymm _ <| le_multiplicativeClosure W
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Composition (goal)
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
⊢ W f
have of : ∀ {x y : C} (f : x ⟶ y) (hf₀ : W f), 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
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Composition (goal)
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
⊢ W f
have id : ∀ (x : C), W (𝟙 x)
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
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Composition (goal)
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)
⊢ W f
have comp_of : ∀ {x y z : C} (f : x ⟶ y) (g : y ⟶ z), W.multiplicativeClosure f → ∀ (hg : W g) (hf : W f), W (f ≫ g)
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
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Composition (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
h : W.multiplicativeClosure = W
⊢ W.IsMultiplicative
have rw : W.multiplicativeClosure.IsMultiplicative
Tactic: rw [← h]