mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.ObjectProperty.LimitsClosure

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
P : ObjectProperty C
α : Type t
J : α → Type u'
inst✝⁵ : (a : α) → Category.{v', u'} (J a)
inst✝⁴ : ObjectProperty.EssentiallySmall.{w, v, u} P
inst✝³ : LocallySmall.{w, v, u} C
inst✝² : Small.{w, t} α
inst✝¹ : ∀ (a : α), Small.{w, u'} (J a)
inst✝ : ∀ (a : α), LocallySmall.{w, v', u'} (J a)
⊢ ObjectProperty.EssentiallySmall.{w, v, u} (P.limitsClosure J)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.Shift

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
P : ObjectProperty C
A : Type u_2
inst✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : P.IsClosedUnderIsomorphisms
⊢ P.shift 0 = P

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : ObjectProperty C
inst✝ : P.IsClosedUnderBinaryProducts
X Y : C
B : BinaryFan X Y
hB : IsLimit B
hX : P X
hY : P Y
⊢ ∀ (j : Discrete WalkingPair), P ((Limits.pair X Y).obj j)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.Shift

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
P : ObjectProperty C
A : Type u_2
inst✝² : AddMonoid A
inst✝¹ : HasShift C A
a b c : A
h : a + b = c
inst✝ : P.IsClosedUnderIsomorphisms
⊢ (P.shift b).shift a = P.shift c

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : ObjectProperty C
inst✝ : P.IsClosedUnderLimitsOfShape (Discrete PEmpty.{1})
X : C
hX : IsTerminal X
⊢ ∀ (j : Discrete PEmpty.{1}), P ((Functor.empty C).obj j)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.Shift

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
P Q : ObjectProperty C
A : Type u_2
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a : A
⊢ (P ⊔ Q).shift a = P.shift a ⊔ Q.shift a

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
P : ObjectProperty C
inst✝² : HasTerminal C
inst✝¹ : P.IsClosedUnderLimitsOfShape (Discrete PEmpty.{1})
inst✝ : P.IsClosedUnderBinaryProducts
X Y : C
e : X ≅ Y
hX : P X
⊢ ∀ {T : C} (f : T ⟶ ⊤_ C) (g : T ⟶ X), (g ≫ e.hom) ≫ (BinaryFan.mk (terminal.from Y) e.inv).fst = f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.Shift

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
A : Type u_2
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
ι : Sort u_4
P : ι → ObjectProperty C
a : A
⊢ (⨆ i, P i).shift a = ⨆ i, (P i).shift a

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
P : ObjectProperty C
inst✝² : HasTerminal C
inst✝¹ : P.IsClosedUnderLimitsOfShape (Discrete PEmpty.{1})
inst✝ : P.IsClosedUnderBinaryProducts
X Y : C
e : X ≅ Y
hX : P X
⊢ ∀ {T : C} (f : T ⟶ ⊤_ C) (g : T ⟶ X), (g ≫ e.hom) ≫ (BinaryFan.mk (terminal.from Y) e.inv).snd = g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.Shift

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
P Q : ObjectProperty C
A : Type u_2
inst✝³ : AddMonoid A
inst✝² : HasShift C A
E : Type u_3
inst✝¹ : Category.{v_2, u_3} E
inst✝ : HasShift E A
a : A
x✝¹ : C
x✝ : ⊤ x✝¹
⊢ ⊤.shift a x✝¹

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.Shift

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
P Q : ObjectProperty C
A : Type u_2
inst✝⁴ : AddMonoid A
inst✝³ : HasShift C A
E : Type u_3
inst✝² : Category.{v_2, u_3} E
inst✝¹ : HasShift E A
a : A
inst✝ : P.IsStableUnderShiftBy a
⊢ P.isoClosure ≤ P.isoClosure.shift a

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
P : ObjectProperty C
inst✝² : HasTerminal C
inst✝¹ : P.IsClosedUnderLimitsOfShape (Discrete PEmpty.{1})
inst✝ : P.IsClosedUnderBinaryProducts
X Y : C
e : X ≅ Y
hX : P X
⊢ ∀ {T : C} (f : T ⟶ ⊤_ C) (g : T ⟶ X) (m : T ⟶ (BinaryFan.mk (terminal.from Y) e.inv).pt),
    m ≫ (BinaryFan.mk (terminal.from Y) e.inv).fst = f →
      m ≫ (BinaryFan.mk (terminal.from Y) e.inv).snd = g → m = g ≫ e.hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.Shift

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
P : ObjectProperty C
G : Type u_4
inst✝³ : AddGroup G
inst✝² : HasShift C G
inst✝¹ : P.IsStableUnderShift G
inst✝ : P.IsClosedUnderIsomorphisms
X : C
g : G
hX : P ((shiftFunctor C g).obj X)
⊢ g + -g = 0

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
P : ObjectProperty C
inst✝² : HasTerminal C
inst✝¹ : P.IsClosedUnderLimitsOfShape (Discrete PEmpty.{1})
inst✝ : P.IsClosedUnderBinaryProducts
X Y : C
e : X ≅ Y
hX : P X
⊢ P Y

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.Shift

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
P : ObjectProperty C
G : Type u_4
inst✝³ : AddGroup G
inst✝² : HasShift C G
inst✝¹ : P.IsStableUnderShift G
inst✝ : P.IsClosedUnderIsomorphisms
X : C
g : G
⊢ P ((shiftFunctor C g).obj X) ↔ P X

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.Shift

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
P : ObjectProperty C
A : Type u_2
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
⊢ P ≤ P.shiftClosure A

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasTerminal C
P Q : ObjectProperty C
inst✝¹ : Q.IsClosedUnderBinaryProducts
inst✝ : Q.IsClosedUnderLimitsOfShape (Discrete PEmpty.{1})
⊢ P.binaryProductsClosure ≤ Q ↔ P ≤ Q

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.Shift

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
P Q : ObjectProperty C
A : Type u_2
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
h : P ≤ Q
⊢ P.shiftClosure A ≤ Q.shiftClosure A

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.Shift

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
P : ObjectProperty C
A : Type u_2
inst✝³ : AddMonoid A
inst✝² : HasShift C A
inst✝¹ : P.IsClosedUnderIsomorphisms
inst✝ : P.IsStableUnderShift A
⊢ P.shiftClosure A = P

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : ObjectProperty C
H : ∀ (J : Type w) [Finite J], P.IsClosedUnderLimitsOfShape (Discrete J)
J : Type
x✝ : Finite J
⊢ P.IsClosedUnderLimitsOfShape (Discrete J)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.Shift

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
P Q : ObjectProperty C
A : Type u_2
inst✝³ : AddMonoid A
inst✝² : HasShift C A
inst✝¹ : Q.IsClosedUnderIsomorphisms
inst✝ : Q.IsStableUnderShift A
h : P ≤ Q
⊢ Q.shiftClosure A ≤ Q

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
P : ObjectProperty C
inst✝¹ : P.IsClosedUnderFiniteProducts
J : Type u_2
inst✝ : Finite J
⊢ P.IsClosedUnderLimitsOfShape (Discrete J)

Tactic:
obtain ⟨n, ⟨e⟩⟩ := Finite.exists_equiv_fin J

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
P : ObjectProperty C
inst✝¹ : P.IsClosedUnderFiniteProducts
J : Type u_2
inst✝ : Finite J
n : ℕ
e : J ≃ Fin n
⊢ P.IsClosedUnderLimitsOfShape (Discrete J)
Module: Mathlib.CategoryTheory.ObjectProperty.Shift

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
P Q : ObjectProperty C
A : Type u_2
inst✝³ : AddMonoid A
inst✝² : HasShift C A
E : Type u_3
inst✝¹ : Category.{v_2, u_3} E
inst✝ : HasShift E A
⊢ ∀ {X Y : C} (x : X ≅ Y), P.shiftClosure A X → P.shiftClosure A Y

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
P : ObjectProperty C
inst✝¹ : P.IsClosedUnderFiniteProducts
J : Type u_2
inst✝ : Finite J
⊢ P.IsClosedUnderLimitsOfShape (Discrete J)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.Shift

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
P Q : ObjectProperty C
A : Type u_2
inst✝³ : AddMonoid A
inst✝² : HasShift C A
E : Type u_3
inst✝¹ : Category.{v_2, u_3} E
inst✝ : HasShift E A
a : A
⊢ P.shiftClosure A ≤ (P.shiftClosure A).shift a

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.Shift

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
P : ObjectProperty C
A : Type u_2
inst✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : P.IsClosedUnderIsomorphisms
h : P.shiftClosure A = P
⊢ P.IsStableUnderShift A

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y Z : C
z₁ : Hom W X Y
z₂ : Hom W Y Z
⊢ Hom W X Z

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
P : ObjectProperty C
inst✝¹ : P.IsClosedUnderFiniteProducts
J : Type u_2
inst✝ : Finite J
f : J → C
F : Fan f
hF : IsLimit F
h : ∀ (j : J), P (f j)
⊢ ∀ (j : Discrete J), P ((Discrete.functor f).obj j)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
P : ObjectProperty C
inst✝¹ : P.ContainsZero
inst✝ : P.IsClosedUnderIsomorphisms
X : C
p : P.LimitOfShape (Discrete PEmpty.{1}) X
Z : C
hZ : IsZero Z
hZ₂ : P Z
⊢ ∀ (j : Discrete PEmpty.{1}),
    ((Cone.postcompose p.diag.uniqueFromEmpty.hom).obj { pt := X, π := p.π }).π.app j =
      (Iso.refl ((Cone.postcompose p.diag.uniqueFromEmpty.hom).obj { pt := X, π := p.π }).pt).hom ≫
        (asEmptyCone X).π.app j

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
P : ObjectProperty C
inst✝¹ : P.ContainsZero
inst✝ : P.IsClosedUnderIsomorphisms
X : C
p : P.LimitOfShape (Discrete PEmpty.{1}) X
Z : C
hZ : IsZero Z
hZ₂ : P Z
⊢ (Cone.postcompose p.diag.uniqueFromEmpty.hom).obj { pt := X, π := p.π } ≅ asEmptyCone X

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
P : ObjectProperty C
inst✝¹ : P.ContainsZero
inst✝ : P.IsClosedUnderIsomorphisms
⊢ P.limitsOfShape (Discrete PEmpty.{1}) ≤ P

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
P : ObjectProperty C
inst✝² : HasFiniteProducts C
inst✝¹ : P.IsClosedUnderLimitsOfShape (Discrete PEmpty.{1})
inst✝ : P.IsClosedUnderBinaryProducts
⊢ P.IsClosedUnderFiniteProducts

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : ObjectProperty C
inst✝ : P.IsClosedUnderBinaryCoproducts
X Y : C
B : BinaryCofan X Y
hB : IsColimit B
hX : P X
hY : P Y
⊢ ∀ (j : Discrete WalkingPair), P ((Limits.pair X Y).obj j)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : ObjectProperty C
inst✝ : P.IsClosedUnderColimitsOfShape (Discrete PEmpty.{1})
X : C
hX : IsInitial X
⊢ ∀ (j : Discrete PEmpty.{1}), P ((Functor.empty C).obj j)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.Shift

Goal state before:
pp: C : Type u_1
inst✝⁷ : Category.{v_1, u_1} C
P Q : ObjectProperty C
A : Type u_2
inst✝⁶ : AddMonoid A
inst✝⁵ : HasShift C A
E : Type u_3
inst✝⁴ : Category.{v_2, u_3} E
inst✝³ : HasShift E A
inst✝² : P.IsClosedUnderIsomorphisms
G : Type u_4
inst✝¹ : AddGroup G
inst✝ : HasShift C G
a : G
X : C
b : G
hb : P.shift b X
⊢ (P.shift (-a + b)).shift a X

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
z : W.LeftFraction X Y
⊢ z.f ≫ (ofHom W z.f).s = (ofHom W (𝟙 X)).s ≫ (ofHom W z.f).f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.Shift

Goal state before:
pp: C : Type u_1
inst✝⁷ : Category.{v_1, u_1} C
P Q : ObjectProperty C
A : Type u_2
inst✝⁶ : AddMonoid A
inst✝⁵ : HasShift C A
E : Type u_3
inst✝⁴ : Category.{v_2, u_3} E
inst✝³ : HasShift E A
inst✝² : P.IsClosedUnderIsomorphisms
G : Type u_4
inst✝¹ : AddGroup G
inst✝ : HasShift C G
a : G
⊢ ⨆ a, P.shift a ≤ (⨆ a, P.shift a).shift a

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
P : ObjectProperty C
inst✝² : HasInitial C
inst✝¹ : P.IsClosedUnderColimitsOfShape (Discrete PEmpty.{1})
inst✝ : P.IsClosedUnderBinaryCoproducts
X Y : C
e : X ≅ Y
hX : P X
⊢ ∀ {T : C} (f : ⊥_ C ⟶ T) (g : X ⟶ T), (BinaryCofan.mk (initial.to Y) e.hom).inl ≫ e.inv ≫ g = f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
P : ObjectProperty C
inst✝² : HasInitial C
inst✝¹ : P.IsClosedUnderColimitsOfShape (Discrete PEmpty.{1})
inst✝ : P.IsClosedUnderBinaryCoproducts
X Y : C
e : X ≅ Y
hX : P X
⊢ ∀ {T : C} (f : ⊥_ C ⟶ T) (g : X ⟶ T), (BinaryCofan.mk (initial.to Y) e.hom).inr ≫ e.inv ≫ g = g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
P : ObjectProperty C
inst✝² : HasInitial C
inst✝¹ : P.IsClosedUnderColimitsOfShape (Discrete PEmpty.{1})
inst✝ : P.IsClosedUnderBinaryCoproducts
X Y : C
e : X ≅ Y
hX : P X
⊢ ∀ {T : C} (f : ⊥_ C ⟶ T) (g : X ⟶ T) (m : (BinaryCofan.mk (initial.to Y) e.hom).pt ⟶ T),
    (BinaryCofan.mk (initial.to Y) e.hom).inl ≫ m = f →
      (BinaryCofan.mk (initial.to Y) e.hom).inr ≫ m = g → m = e.inv ≫ g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
P : ObjectProperty C
inst✝² : HasInitial C
inst✝¹ : P.IsClosedUnderColimitsOfShape (Discrete PEmpty.{1})
inst✝ : P.IsClosedUnderBinaryCoproducts
X Y : C
e : X ≅ Y
hX : P X
⊢ P Y

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
⊢ ∀ {X Y : Localization W} (f : Hom W X Y), (Hom.mk (ofHom W (𝟙 X))).comp f = f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasInitial C
P Q : ObjectProperty C
inst✝¹ : Q.IsClosedUnderBinaryCoproducts
inst✝ : Q.IsClosedUnderColimitsOfShape (Discrete PEmpty.{1})
⊢ P.binaryCoproductsClosure ≤ Q ↔ P ≤ Q

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.Shift

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
P : ObjectProperty C
inst✝² : P.IsClosedUnderIsomorphisms
G : Type u_4
inst✝¹ : AddGroup G
inst✝ : HasShift C G
⊢ P.shiftClosure G = ⨆ x, P.shift x

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : ObjectProperty C
H : ∀ (J : Type w) [Finite J], P.IsClosedUnderColimitsOfShape (Discrete J)
J : Type
x✝ : Finite J
⊢ P.IsClosedUnderColimitsOfShape (Discrete J)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
P : ObjectProperty C
inst✝¹ : P.IsClosedUnderFiniteCoproducts
J : Type u_2
inst✝ : Finite J
⊢ P.IsClosedUnderColimitsOfShape (Discrete J)

Tactic:
obtain ⟨n, ⟨e⟩⟩ := Finite.exists_equiv_fin J

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
P : ObjectProperty C
inst✝¹ : P.IsClosedUnderFiniteCoproducts
J : Type u_2
inst✝ : Finite J
n : ℕ
e : J ≃ Fin n
⊢ P.IsClosedUnderColimitsOfShape (Discrete J)
Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
P : ObjectProperty C
inst✝¹ : P.IsClosedUnderFiniteCoproducts
J : Type u_2
inst✝ : Finite J
⊢ P.IsClosedUnderColimitsOfShape (Discrete J)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
P : ObjectProperty C
inst✝¹ : P.IsClosedUnderFiniteCoproducts
J : Type u_2
inst✝ : Finite J
f : J → C
F : Cofan f
hF : IsColimit F
h : ∀ (j : J), P (f j)
⊢ ∀ (j : Discrete J), P ((Discrete.functor f).obj j)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
z : W.LeftFraction X Y
⊢ (ofHom W (𝟙 Y)).f ≫ (ofInv z.s ⋯).s = z.s ≫ (ofInv z.s ⋯).f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
P : ObjectProperty C
inst✝¹ : P.ContainsZero
inst✝ : P.IsClosedUnderIsomorphisms
X : C
p : P.ColimitOfShape (Discrete PEmpty.{1}) X
Z : C
hZ : IsZero Z
hZ₂ : P Z
⊢ ∀ (j : Discrete PEmpty.{1}),
    ((Cocone.precompose p.diag.uniqueFromEmpty.inv).obj { pt := X, ι := p.ι }).ι.app j ≫
        (Iso.refl ((Cocone.precompose p.diag.uniqueFromEmpty.inv).obj { pt := X, ι := p.ι }).pt).hom =
      (asEmptyCocone X).ι.app j

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
⊢ ∀ {X Y : Localization W} (f : Hom W X Y), f.comp (Hom.mk (ofHom W (𝟙 Y))) = f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
P : ObjectProperty C
inst✝¹ : P.ContainsZero
inst✝ : P.IsClosedUnderIsomorphisms
X : C
p : P.ColimitOfShape (Discrete PEmpty.{1}) X
Z : C
hZ : IsZero Z
hZ₂ : P Z
⊢ (Cocone.precompose p.diag.uniqueFromEmpty.inv).obj { pt := X, ι := p.ι } ≅ asEmptyCocone X

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
P : ObjectProperty C
inst✝¹ : P.ContainsZero
inst✝ : P.IsClosedUnderIsomorphisms
⊢ P.colimitsOfShape (Discrete PEmpty.{1}) ≤ P

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.ShiftAdditive

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
P : ObjectProperty C
A : Type u_2
inst✝⁴ : AddMonoid A
inst✝³ : HasShift C A
inst✝² : P.IsStableUnderShift A
inst✝¹ : Preadditive C
n : A
inst✝ : (shiftFunctor C n).Additive
⊢ (shiftFunctor P.FullSubcategory n).Additive

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
P : ObjectProperty C
inst✝² : HasFiniteCoproducts C
inst✝¹ : P.IsClosedUnderColimitsOfShape (Discrete PEmpty.{1})
inst✝ : P.IsClosedUnderBinaryCoproducts
⊢ P.IsClosedUnderFiniteCoproducts

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X₁ X₂ X₃ X₄ : C
z₁ : W.LeftFraction X₁ X₂
z₂ : W.LeftFraction X₂ X₃
z₃ : W.LeftFraction X₃ X₄
z₁₂ : W.LeftFraction z₁.Y' z₂.Y'
fac₁₂ : z₂.f ≫ z₁₂.s = z₁.s ≫ z₁₂.f
z₂₃ : W.LeftFraction z₂.Y' z₃.Y'
fac₂₃ : z₃.f ≫ z₂₃.s = z₂.s ≫ z₂₃.f
z' : W.LeftFraction z₁₂.Y' z₂₃.Y'
fac : z₂₃.f ≫ z'.s = z₁₂.s ≫ z'.f
⊢ z₃.f ≫ { Y' := z'.Y', f := z'.f, s := z₂₃.s ≫ z'.s, hs := ⋯ }.s =
    { Y' := z₁₂.Y', f := z₁.f ≫ z₁₂.f, s := z₂.s ≫ z₁₂.s, hs := ⋯ }.s ≫
      { Y' := z'.Y', f := z'.f, s := z₂₃.s ≫ z'.s, hs := ⋯ }.f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X₁ X₂ X₃ X₄ : C
z₁ : W.LeftFraction X₁ X₂
z₂ : W.LeftFraction X₂ X₃
z₃ : W.LeftFraction X₃ X₄
z₁₂ : W.LeftFraction z₁.Y' z₂.Y'
fac₁₂ : z₂.f ≫ z₁₂.s = z₁.s ≫ z₁₂.f
z₂₃ : W.LeftFraction z₂.Y' z₃.Y'
fac₂₃ : z₃.f ≫ z₂₃.s = z₂.s ≫ z₂₃.f
z' : W.LeftFraction z₁₂.Y' z₂₃.Y'
fac : z₂₃.f ≫ z'.s = z₁₂.s ≫ z'.f
⊢ { Y' := z₂₃.Y', f := z₂.f ≫ z₂₃.f, s := z₃.s ≫ z₂₃.s, hs := ⋯ }.f ≫
      { Y' := z'.Y', f := z₁₂.f ≫ z'.f, s := z'.s, hs := ⋯ }.s =
    z₁.s ≫ { Y' := z'.Y', f := z₁₂.f ≫ z'.f, s := z'.s, hs := ⋯ }.f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
⊢ ∀ {W_1 X Y Z : Localization W} (f : Hom W W_1 X) (g : Hom W X Y) (h : Hom W Y Z),
    (f.comp g).comp h = f.comp (g.comp h)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ (ofHom W g).f ≫ (ofHom W g).s = (ofHom W f).s ≫ (ofHom W g).f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ Hom.mk (ofHom W (f ≫ g)) = Hom.mk (ofHom W f) ≫ Hom.mk (ofHom W g)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y Z : C
z₁ : W.LeftFraction X Y
z₂ : W.LeftFraction Y Z
z₃ : W.LeftFraction z₁.Y' z₂.Y'
h₃ : z₂.f ≫ z₃.s = z₁.s ≫ z₃.f
⊢ homMk z₁ ≫ homMk z₂ = homMk (z₁.comp₀ z₂ z₃)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y Y' : C
f : X ⟶ Y'
s : Y ⟶ Y'
hs : W s
⊢ (ofInv s hs).f ≫ (ofHom W (𝟙 (ofHom W f).Y')).s = (ofHom W f).s ≫ (ofHom W (𝟙 (ofHom W f).Y')).f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y Y' : C
f : X ⟶ Y'
s : Y ⟶ Y'
hs : W s
⊢ (Q W).map f ≫ Qinv s hs = homMk { Y' := Y', f := f, s := s, hs := hs }

Tactic:
by

Goal state after: