mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Presentable.ColimitPresentation

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
J✝ : Type u_1
I✝ : J✝ → Type u_2
inst✝⁵ : Category.{v_1, u_1} J✝
inst✝⁴ : (j : J✝) → Category.{?u.14, u_2} (I✝ j)
D✝ : J✝ ⥤ C
P✝¹ : (j : J✝) → ColimitPresentation (I✝ j) (D✝.obj j)
J : Type w
I : J → Type w
inst✝³ : SmallCategory J
inst✝² : (j : J) → SmallCategory (I j)
D : J ⥤ C
P✝ : (j : J) → ColimitPresentation (I j) (D.obj j)
X : C
P : ColimitPresentation J X
Q : (j : J) → ColimitPresentation (I j) (P.diag.obj j)
inst✝¹ : ∀ (j : J), IsFiltered (I j)
inst✝ : ∀ (j : J) (i : I j), IsFinitelyPresentable ((Q j).diag.obj i)
c : Cocone { obj := fun k ↦ (Q k.fst).diag.obj k.snd, map := fun {k l} f ↦ f.hom, map_id := ⋯, map_comp := ⋯ }
m : { pt := X, ι := { app := fun k ↦ (Q k.fst).ι.app k.snd ≫ P.ι.app k.fst, naturality := ⋯ } }.pt ⟶ c.pt
hm :
  ∀ (j : Total Q),
    { pt := X, ι := { app := fun k ↦ (Q k.fst).ι.app k.snd ≫ P.ι.app k.fst, naturality := ⋯ } }.ι.app j ≫ m = c.ι.app j
j : J
i : I j
⊢ { pt := P.diag.obj j, ι := (Q j).ι }.ι.app i ≫ P.ι.app j ≫ m =
    { pt := P.diag.obj j, ι := (Q j).ι }.ι.app i ≫
      (Q j).isColimit.desc { pt := c.pt, ι := { app := fun i ↦ c.ι.app ⟨j, i⟩, naturality := ⋯ } }

Tactic:
simpa using

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
J✝ : Type u_1
I✝ : J✝ → Type u_2
inst✝⁵ : Category.{v_1, u_1} J✝
inst✝⁴ : (j : J✝) → Category.{?u.14, u_2} (I✝ j)
D✝ : J✝ ⥤ C
P✝¹ : (j : J✝) → ColimitPresentation (I✝ j) (D✝.obj j)
J : Type w
I : J → Type w
inst✝³ : SmallCategory J
inst✝² : (j : J) → SmallCategory (I j)
D : J ⥤ C
P✝ : (j : J) → ColimitPresentation (I j) (D.obj j)
X : C
P : ColimitPresentation J X
Q : (j : J) → ColimitPresentation (I j) (P.diag.obj j)
inst✝¹ : ∀ (j : J), IsFiltered (I j)
inst✝ : ∀ (j : J) (i : I j), IsFinitelyPresentable ((Q j).diag.obj i)
c : Cocone { obj := fun k ↦ (Q k.fst).diag.obj k.snd, map := fun {k l} f ↦ f.hom, map_id := ⋯, map_comp := ⋯ }
m : { pt := X, ι := { app := fun k ↦ (Q k.fst).ι.app k.snd ≫ P.ι.app k.fst, naturality := ⋯ } }.pt ⟶ c.pt
hm :
  ∀ (j : Total Q),
    { pt := X, ι := { app := fun k ↦ (Q k.fst).ι.app k.snd ≫ P.ι.app k.fst, naturality := ⋯ } }.ι.app j ≫ m = c.ι.app j
j : J
i : I j
⊢ (Q j).ι.app i ≫ P.ι.app j ≫ m = c.ι.app ⟨j, i⟩
Module: Mathlib.CategoryTheory.Monoidal.DayConvolution

Goal state before:
pp: C✝ : Type u₁
inst✝¹⁶ : Category.{v₁, u₁} C✝
V✝ : Type u₂
inst✝¹⁵ : Category.{v₂, u₂} V✝
inst✝¹⁴ : MonoidalCategory C✝
inst✝¹³ : MonoidalCategory V✝
C : Type u₁
inst✝¹² : Category.{v₁, u₁} C
V : Type u₂
inst✝¹¹ : Category.{v₂, u₂} V
inst✝¹⁰ : MonoidalCategory C
inst✝⁹ : MonoidalCategory V
D : Type u₃
inst✝⁸ : Category.{v₃, u₃} D
inst✝⁷ : MonoidalCategoryStruct D
inst✝⁶ : LawfulDayConvolutionMonoidalCategoryStruct C V D
inst✝⁵ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)
inst✝⁴ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)
inst✝³ :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorLeft v)
inst✝² :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorRight v)
inst✝¹ :
  ∀ (v : V) (d : C × C),
    Limits.PreservesColimitsOfShape (CostructuredArrow ((𝟭 C).prod (Functor.fromPUnit (𝟙_ C))) d) (tensorRight v)
inst✝ :
  ∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((tensor C).prod (𝟭 C)) d) (tensorRight v)
X✝ Y✝ : D
f : X✝ ⟶ Y✝
⊢ map (𝟙 ((ι C V D).obj (𝟙_ D))) ((ι C V D).map f) ≫
      (DayConvolutionUnit.leftUnitor ((ι C V D).obj (𝟙_ D)) ((ι C V D).obj Y✝)).hom =
    (ι C V D).map (λ_ X✝).hom ≫ (ι C V D).map f

Tactic:
ι_map_leftUnitor_hom_eq_leftUnitor_hom

Goal state after:
C✝ : Type u₁
inst✝¹⁶ : Category.{v₁, u₁} C✝
V✝ : Type u₂
inst✝¹⁵ : Category.{v₂, u₂} V✝
inst✝¹⁴ : MonoidalCategory C✝
inst✝¹³ : MonoidalCategory V✝
C : Type u₁
inst✝¹² : Category.{v₁, u₁} C
V : Type u₂
inst✝¹¹ : Category.{v₂, u₂} V
inst✝¹⁰ : MonoidalCategory C
inst✝⁹ : MonoidalCategory V
D : Type u₃
inst✝⁸ : Category.{v₃, u₃} D
inst✝⁷ : MonoidalCategoryStruct D
inst✝⁶ : LawfulDayConvolutionMonoidalCategoryStruct C V D
inst✝⁵ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)
inst✝⁴ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)
inst✝³ :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorLeft v)
inst✝² :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorRight v)
inst✝¹ :
  ∀ (v : V) (d : C × C),
    Limits.PreservesColimitsOfShape (CostructuredArrow ((𝟭 C).prod (Functor.fromPUnit (𝟙_ C))) d) (tensorRight v)
inst✝ :
  ∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((tensor C).prod (𝟭 C)) d) (tensorRight v)
X✝ Y✝ : D
f : X✝ ⟶ Y✝
⊢ map (𝟙 ((ι C V D).obj (𝟙_ D))) ((ι C V D).map f) ≫
      (DayConvolutionUnit.leftUnitor ((ι C V D).obj (𝟙_ D)) ((ι C V D).obj Y✝)).hom =
    (DayConvolutionUnit.leftUnitor ((ι C V D).obj (𝟙_ D)) ((ι C V D).obj X✝)).hom ≫ (ι C V D).map f
Module: Mathlib.CategoryTheory.MorphismProperty.LocalClosure

Goal state before:
pp: case comp
C : Type u
inst✝³ : Category.{v, u} C
K : Precoverage C
P Q : MorphismProperty C
X✝¹ Y✝¹ : C
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : K.IsStableUnderBaseChange
inst✝ : HasPullbacks C
Y X Z : C
f : X ⟶ Z
X✝ Y✝ : C
f' : X✝ ⟶ Y✝
hf' : sourceLocalClosure K P f'
R : Presieve X✝
hR : R ∈ K.coverings X✝
U✝ : C
g' : U✝ ⟶ X✝
hg' : R g'
ih : ∀ (W : C) (g : Y ⟶ Y✝) (fst : W ⟶ X✝) (snd : W ⟶ Y), IsPullback fst snd f' g → sourceLocalClosure K P snd
W : C
g : Y ⟶ Y✝
fst : W ⟶ U✝
snd : W ⟶ Y
h✝ : IsPullback fst snd (g' ≫ f') g
u : W ⟶ pullback g f' := pullback.lift snd (fst ≫ g') ⋯
h : IsPullback fst (u ≫ pullback.fst g f') (g' ≫ f') g
this : snd = u ≫ pullback.fst g f'
e : W ≅ pullback g' (pullback.snd g f') := ⋯.isoPullback
⊢ Presieve.pullbackArrows (pullback.snd g f') R (e.inv ≫ u)

Tactic:
simpa using

Goal state after:
case comp
C : Type u
inst✝³ : Category.{v, u} C
K : Precoverage C
P Q : MorphismProperty C
X✝¹ Y✝¹ : C
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : K.IsStableUnderBaseChange
inst✝ : HasPullbacks C
Y X Z : C
f : X ⟶ Z
X✝ Y✝ : C
f' : X✝ ⟶ Y✝
hf' : sourceLocalClosure K P f'
R : Presieve X✝
hR : R ∈ K.coverings X✝
U✝ : C
g' : U✝ ⟶ X✝
hg' : R g'
ih : ∀ (W : C) (g : Y ⟶ Y✝) (fst : W ⟶ X✝) (snd : W ⟶ Y), IsPullback fst snd f' g → sourceLocalClosure K P snd
W : C
g : Y ⟶ Y✝
fst : W ⟶ U✝
snd : W ⟶ Y
h✝ : IsPullback fst snd (g' ≫ f') g
u : W ⟶ pullback g f' := pullback.lift snd (fst ≫ g') ⋯
h : IsPullback fst (u ≫ pullback.fst g f') (g' ≫ f') g
this : snd = u ≫ pullback.fst g f'
e : W ≅ pullback g' (pullback.snd g f') := ⋯.isoPullback
⊢ Presieve.pullbackArrows (pullback.snd g f') R (pullback.snd g' (pullback.snd g f'))
Module: Mathlib.CategoryTheory.MorphismProperty.LocalClosure

Goal state before:
pp: case refine_1.of
C : Type u
inst✝⁶ : Category.{v, u} C
K : Precoverage C
P : MorphismProperty C
inst✝⁵ : P.RespectsIso
inst✝⁴ : P.RespectsLeft K.morphismProperty
inst✝³ : K.HasIsos
inst✝² : K.IsStableUnderBaseChange
inst✝¹ : K.IsStableUnderComposition
inst✝ : K.HasPullbacks
X Y : C
f✝ : X ⟶ Y
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : P f
⊢ ∃ R ∈ K.coverings X✝, ∀ (U : C) (g : U ⟶ X✝), R g → P (g ≫ f)

Tactic:
exact ⟨.singleton (𝟙 _), K.mem_coverings_of_isIso _, fun U g ⟨⟩ ↦ by simpa⟩

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Ind

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
hp : P ≤ isFinitelyPresentable C
inst✝ : LocallySmall.{w, v, u} C
X Y : C
f : X ⟶ Y
hf : P.ind.ind f
this : P.underObj ≤ ObjectProperty.isFinitelyPresentable (Under X)
⊢ P.ind f

Tactic:
simpa using

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
hp : P ≤ isFinitelyPresentable C
inst✝ : LocallySmall.{w, v, u} C
X Y : C
f : X ⟶ Y
hf : P.ind.ind f
this : P.underObj ≤ ObjectProperty.isFinitelyPresentable (Under X)
⊢ P.underObj.ind (CategoryTheory.Under.mk f)
Module: Mathlib.CategoryTheory.MorphismProperty.LocalEpi

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : ObjectProperty C
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
hf : P.localEpi f
hg : P.localEpi g
T : C
hT : P T
x✝¹ x✝ : Z✝ ⟶ T
huv : (fun g_1 ↦ (f ≫ g) ≫ g_1) x✝¹ = (fun g_1 ↦ (f ≫ g) ≫ g_1) x✝
⊢ (fun g ↦ f ≫ g) ((fun g_1 ↦ g ≫ g_1) x✝¹) = (fun g ↦ f ≫ g) ((fun g_1 ↦ g ≫ g_1) x✝)

Tactic:
simpa using

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : ObjectProperty C
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
hf : P.localEpi f
hg : P.localEpi g
T : C
hT : P T
x✝¹ x✝ : Z✝ ⟶ T
huv : (fun g_1 ↦ (f ≫ g) ≫ g_1) x✝¹ = (fun g_1 ↦ (f ≫ g) ≫ g_1) x✝
⊢ f ≫ g ≫ x✝¹ = f ≫ g ≫ x✝
Module: Mathlib.CategoryTheory.MorphismProperty.LocalEpi

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : ObjectProperty C
W : MorphismProperty C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
x✝ : W f
hfg : P.localEpi (f ≫ g)
T : C
hT : P T
u v : Z ⟶ T
huv : (fun g_1 ↦ g ≫ g_1) u = (fun g_1 ↦ g ≫ g_1) v
⊢ (fun g_1 ↦ (f ≫ g) ≫ g_1) u = (fun g_1 ↦ (f ≫ g) ≫ g_1) v

Tactic:
simp [huv]

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.LocalEpi

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : ObjectProperty C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hg : P.isLocal g
hfg : P.localEpi (f ≫ g)
T : C
hT : P T
u v : Z ⟶ T
huv : (fun g ↦ f ≫ g) ((fun g_1 ↦ g ≫ g_1) u) = (fun g ↦ f ≫ g) ((fun g_1 ↦ g ≫ g_1) v)
⊢ (fun g_1 ↦ (f ≫ g) ≫ g_1) ?m.71 = (fun g_1 ↦ (f ≫ g) ≫ g_1) ?m.72

Tactic:
simpa using

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : ObjectProperty C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hg : P.isLocal g
hfg : P.localEpi (f ≫ g)
T : C
hT : P T
u v : Z ⟶ T
huv : (fun g ↦ f ≫ g) ((fun g_1 ↦ g ≫ g_1) u) = (fun g ↦ f ≫ g) ((fun g_1 ↦ g ≫ g_1) v)
⊢ f ≫ g ≫ ?m.71 = f ≫ g ≫ ?m.72
Module: Mathlib.CategoryTheory.Subobject.ArtinianObject

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
X : C
h : ∀ (F : ℕ ⥤ (MonoOver X)ᵒᵖ), IsFiltered.IsEventuallyConstant F
F : ℕ →o (Subobject X)ᵒᵈ
n : ℕ
hn : (⋯.functor ⋙ (orderDualEquivalence (Subobject X)).functor ⋙ Subobject.representative.op).IsEventuallyConstantFrom n
m : ℕ
hm : n ≤ m
⊢ F m = F n

Tactic:
simpa using

Goal state after:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
X : C
h : ∀ (F : ℕ ⥤ (MonoOver X)ᵒᵖ), IsFiltered.IsEventuallyConstant F
F : ℕ →o (Subobject X)ᵒᵈ
n : ℕ
hn : (⋯.functor ⋙ (orderDualEquivalence (Subobject X)).functor ⋙ Subobject.representative.op).IsEventuallyConstantFrom n
m : ℕ
hm : n ≤ m
⊢ F m = F n
Module: Mathlib.CategoryTheory.Subobject.ArtinianObject

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y X✝ Y✝ : C
f : X✝ ⟶ Y✝
x✝ : Mono f
hY : isArtinianObject.Is Y✝
⊢ isArtinianObject.Is X✝

Tactic:
exact isArtinianObject_of_mono f

Goal state after:
Module: Mathlib.CategoryTheory.Subobject.NoetherianObject

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
X : C
h : ∀ (F : ℕ ⥤ MonoOver X), IsFiltered.IsEventuallyConstant F
F : ℕ →o Subobject X
n : ℕ
hn : (⋯.functor ⋙ Subobject.representative).IsEventuallyConstantFrom n
m : ℕ
hm : n ≤ m
⊢ F n = F m

Tactic:
simpa using

Goal state after:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
X : C
h : ∀ (F : ℕ ⥤ MonoOver X), IsFiltered.IsEventuallyConstant F
F : ℕ →o Subobject X
n : ℕ
hn : (⋯.functor ⋙ Subobject.representative).IsEventuallyConstantFrom n
m : ℕ
hm : n ≤ m
⊢ F n = F m
Module: Mathlib.CategoryTheory.Preadditive.FreydCategory.RightFreyd

Goal state before:
pp: V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
inst✝ : Preadditive V
u v : Arrow V
f g : u ⟶ v
h : (quotient V).map f = (quotient V).map g
⊢ (quotient V).map f = (quotient V).map g

Tactic:
simpa using

Goal state after:
V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
inst✝ : Preadditive V
u v : Arrow V
f g : u ⟶ v
h : (quotient V).map f = (quotient V).map g
⊢ (quotient V).map f = (quotient V).map g
Module: Mathlib.CategoryTheory.Preadditive.FreydCategory.RightFreyd

Goal state before:
pp: V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
inst✝ : Preadditive V
u v : Arrow V
f g : u ⟶ v
x✝ : Nonempty (RightHomotopy f g)
h : RightHomotopy f g
⊢ (quotient V).map f = (quotient V).map g

Tactic:
simpa using

Goal state after:
V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
inst✝ : Preadditive V
u v : Arrow V
f g : u ⟶ v
x✝ : Nonempty (RightHomotopy f g)
h : RightHomotopy f g
⊢ (quotient V).map f = (quotient V).map g
Module: Mathlib.CategoryTheory.Preadditive.FreydCategory.RightFreyd

Goal state before:
pp: V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
inst✝ : Preadditive V
u v : Arrow V
f : u ⟶ v
h : (quotient V).map f = 0
⊢ (quotient V).map f = (quotient V).map 0

Tactic:
simpa using

Goal state after:
V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
inst✝ : Preadditive V
u v : Arrow V
f : u ⟶ v
h : (quotient V).map f = 0
⊢ (quotient V).map f = 0
Module: Mathlib.CategoryTheory.Preadditive.FreydCategory.RightFreyd

Goal state before:
pp: V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
inst✝ : Preadditive V
u v : Arrow V
f : u ⟶ v
x✝ : Nonempty (RightHomotopy f 0)
h : RightHomotopy f 0
⊢ (quotient V).map f = 0

Tactic:
simpa using

Goal state after:
V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
inst✝ : Preadditive V
u v : Arrow V
f : u ⟶ v
x✝ : Nonempty (RightHomotopy f 0)
h : RightHomotopy f 0
⊢ (quotient V).map f = 0
Module: Mathlib.CategoryTheory.Pi.Monoidal

Goal state before:
pp: I : Type w₁
C : I → Type u₁
inst✝⁶ : (i : I) → Category.{v₁, u₁} (C i)
inst✝⁵ : (i : I) → MonoidalCategory (C i)
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
inst✝³ : MonoidalCategory D
F G : D ⥤ ((i : I) → C i)
inst✝² : F.LaxMonoidal
inst✝¹ : G.LaxMonoidal
τ : (i : I) → F ⋙ eval C i ⟶ G ⋙ eval C i
inst✝ : ∀ (i : I), NatTrans.IsMonoidal (τ i)
i : I
⊢ (Functor.LaxMonoidal.ε F ≫ (NatTrans.pi' τ).app (𝟙_ D)) i = Functor.LaxMonoidal.ε G i

Tactic:
simpa using

Goal state after:
I : Type w₁
C : I → Type u₁
inst✝⁶ : (i : I) → Category.{v₁, u₁} (C i)
inst✝⁵ : (i : I) → MonoidalCategory (C i)
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
inst✝³ : MonoidalCategory D
F G : D ⥤ ((i : I) → C i)
inst✝² : F.LaxMonoidal
inst✝¹ : G.LaxMonoidal
τ : (i : I) → F ⋙ eval C i ⟶ G ⋙ eval C i
inst✝ : ∀ (i : I), NatTrans.IsMonoidal (τ i)
i : I
⊢ Functor.LaxMonoidal.ε F i ≫ (τ i).app (𝟙_ D) = Functor.LaxMonoidal.ε G i
Module: Mathlib.CategoryTheory.Pi.Monoidal

Goal state before:
pp: I : Type w₁
C : I → Type u₁
inst✝⁶ : (i : I) → Category.{v₁, u₁} (C i)
inst✝⁵ : (i : I) → MonoidalCategory (C i)
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
inst✝³ : MonoidalCategory D
F G : D ⥤ ((i : I) → C i)
inst✝² : F.LaxMonoidal
inst✝¹ : G.LaxMonoidal
τ : (i : I) → F ⋙ eval C i ⟶ G ⋙ eval C i
inst✝ : ∀ (i : I), NatTrans.IsMonoidal (τ i)
X Y : D
i : I
⊢ (Functor.LaxMonoidal.μ F X Y ≫ (NatTrans.pi' τ).app (X ⊗ Y)) i =
    (((NatTrans.pi' τ).app X ⊗ₘ (NatTrans.pi' τ).app Y) ≫ Functor.LaxMonoidal.μ G X Y) i

Tactic:
simpa using

Goal state after:
I : Type w₁
C : I → Type u₁
inst✝⁶ : (i : I) → Category.{v₁, u₁} (C i)
inst✝⁵ : (i : I) → MonoidalCategory (C i)
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
inst✝³ : MonoidalCategory D
F G : D ⥤ ((i : I) → C i)
inst✝² : F.LaxMonoidal
inst✝¹ : G.LaxMonoidal
τ : (i : I) → F ⋙ eval C i ⟶ G ⋙ eval C i
inst✝ : ∀ (i : I), NatTrans.IsMonoidal (τ i)
X Y : D
i : I
⊢ Functor.LaxMonoidal.μ F X Y i ≫ (τ i).app (X ⊗ Y) = ((τ i).app X ⊗ₘ (τ i).app Y) ≫ Functor.LaxMonoidal.μ G X Y i
Module: Mathlib.CategoryTheory.Preadditive.HomOrthogonal

Goal state before:
pp: case e'_2.e'_7
C : Type u
inst✝³ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝² : Preadditive C
inst✝¹ : HasFiniteBiproducts C
o : HomOrthogonal s
α : Type
inst✝ : Finite α
f : α → ι
b a : α
j_property✝ : a ∈ f ⁻¹' {f b}
j_property : f a = f b
h : ¬b = a
⊢ biproduct.ι (fun a ↦ s (f a)) a ≫ biproduct.π (fun b ↦ s (f b)) b = 0

Tactic:
simpa using

Goal state after:
case e'_2.e'_7
C : Type u
inst✝³ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝² : Preadditive C
inst✝¹ : HasFiniteBiproducts C
o : HomOrthogonal s
α : Type
inst✝ : Finite α
f : α → ι
b a : α
j_property✝ : a ∈ f ⁻¹' {f b}
j_property : f a = f b
h : ¬b = a
⊢ biproduct.ι (fun a ↦ s (f a)) a ≫ biproduct.π (fun b ↦ s (f b)) b = 0
Module: Mathlib.CategoryTheory.Preadditive.Comma

Goal state before:
pp: A : Type u₁
inst✝⁷ : Category.{v₁, u₁} A
inst✝⁶ : Preadditive A
B : Type u₂
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Preadditive B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
inst✝² : Preadditive T
L : A ⥤ T
inst✝¹ : L.Additive
R : B ⥤ T
inst✝ : R.Additive
u v : Comma L R
x✝¹ : ℕ
x✝ : u ⟶ v
⊢ Int.negSucc x✝¹ • x✝ = -(↑x✝¹.succ • x✝)

Tactic:
by
    simp_rw [HSMul.hSMul, SMul.smul]
    ext <;> dsimp <;> simp [add_nsmul, add_zsmul]

Goal state after:
Module: Mathlib.GroupTheory.EckmannHilton

Goal state before:
pp: X : Type u
m₁ m₂ : X → X → X
e₁ e₂ : X
h₁ : IsUnital m₁ e₁
h₂ : IsUnital m₂ e₂
distrib : ∀ (a b c d : X), m₁ (m₂ a b) (m₂ c d) = m₂ (m₁ a c) (m₁ b d)
⊢ e₁ = e₂

Tactic:
simpa using

Goal state after:
X : Type u
m₁ m₂ : X → X → X
e₁ e₂ : X
h₁ : IsUnital m₁ e₁
h₂ : IsUnital m₂ e₂
distrib : ∀ (a b c d : X), m₁ (m₂ a b) (m₂ c d) = m₂ (m₁ a c) (m₁ b d)
⊢ e₁ = e₂
Module: Mathlib.GroupTheory.EckmannHilton

Goal state before:
pp: X : Type u
m₁ m₂ : X → X → X
e₁ e₂ : X
h₁ : IsUnital m₁ e₁
h₂ : IsUnital m₂ e₂
distrib : ∀ (a b c d : X), m₁ (m₂ a b) (m₂ c d) = m₂ (m₁ a c) (m₁ b d)
a b : X
⊢ m₂ a b = m₂ b a

Tactic:
simpa using

Goal state after:
X : Type u
m₁ m₂ : X → X → X
e₁ e₂ : X
h₁ : IsUnital m₁ e₁
h₂ : IsUnital m₂ e₂
distrib : ∀ (a b c d : X), m₁ (m₂ a b) (m₂ c d) = m₂ (m₁ a c) (m₁ b d)
a b : X
⊢ m₂ a b = m₂ b a
Module: Mathlib.GroupTheory.EckmannHilton

Goal state before:
pp: X : Type u
m₁ m₂ : X → X → X
e₁ e₂ : X
h₁ : IsUnital m₁ e₁
h₂ : IsUnital m₂ e₂
distrib : ∀ (a b c d : X), m₁ (m₂ a b) (m₂ c d) = m₂ (m₁ a c) (m₁ b d)
a b c : X
⊢ m₂ (m₂ a b) c = m₂ a (m₂ b c)

Tactic:
simpa using

Goal state after:
X : Type u
m₁ m₂ : X → X → X
e₁ e₂ : X
h₁ : IsUnital m₁ e₁
h₂ : IsUnital m₂ e₂
distrib : ∀ (a b c d : X), m₁ (m₂ a b) (m₂ c d) = m₂ (m₁ a c) (m₁ b d)
a b c : X
⊢ m₂ (m₂ a b) c = m₂ a (m₂ b c)
Module: Mathlib.CategoryTheory.Preadditive.Schur

Goal state before:
pp: C : Type u_1
inst✝⁸ : Category.{v_1, u_1} C
inst✝⁷ : Preadditive C
𝕜 : Type u_2
inst✝⁶ : Field 𝕜
inst✝⁵ : IsAlgClosed 𝕜
inst✝⁴ : Linear 𝕜 C
inst✝³ : HasKernels C
X Y : C
inst✝² : FiniteDimensional 𝕜 (X ⟶ X)
inst✝¹ : Simple X
inst✝ : Simple Y
h : Nontrivial (X ⟶ Y)
f : X ⟶ Y
nz : f ≠ 0
fi : IsIso f
g : X ⟶ Y
c : 𝕜
w : c • 𝟙 X = g ≫ inv f
⊢ c • f = g

Tactic:
simpa using

Goal state after:
C : Type u_1
inst✝⁸ : Category.{v_1, u_1} C
inst✝⁷ : Preadditive C
𝕜 : Type u_2
inst✝⁶ : Field 𝕜
inst✝⁵ : IsAlgClosed 𝕜
inst✝⁴ : Linear 𝕜 C
inst✝³ : HasKernels C
X Y : C
inst✝² : FiniteDimensional 𝕜 (X ⟶ X)
inst✝¹ : Simple X
inst✝ : Simple Y
h : Nontrivial (X ⟶ Y)
f : X ⟶ Y
nz : f ≠ 0
fi : IsIso f
g : X ⟶ Y
c : 𝕜
w : c • 𝟙 X = g ≫ inv f
⊢ c • f = g
Module: Mathlib.CategoryTheory.Presentable.Adjunction

Goal state before:
pp: C : Type u
D : Type u'
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Category.{v', u'} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
κ : Cardinal.{w}
inst✝³ : Fact κ.IsRegular
P : ObjectProperty C
hP : P.IsCardinalFilteredGenerator κ
inst✝² : G.IsCardinalAccessible κ
inst✝¹ : G.Full
inst✝ : G.Faithful
Y : D
this : F.IsLeftAdjoint
⊢ ∃ J x, ∃ (_ : IsCardinalFiltered J κ), (P.map F).colimitsOfShape J Y

Tactic:
obtain ⟨J, _, _, ⟨hY⟩⟩ := hP.exists_colimitsOfShape (G.obj Y)

Goal state after:
C : Type u
D : Type u'
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Category.{v', u'} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
κ : Cardinal.{w}
inst✝³ : Fact κ.IsRegular
P : ObjectProperty C
hP : P.IsCardinalFilteredGenerator κ
inst✝² : G.IsCardinalAccessible κ
inst✝¹ : G.Full
inst✝ : G.Faithful
Y : D
this : F.IsLeftAdjoint
J : Type w
w✝¹ : SmallCategory J
w✝ : IsCardinalFiltered J κ
hY : P.ColimitOfShape J (G.obj Y)
⊢ ∃ J x, ∃ (_ : IsCardinalFiltered J κ), (P.map F).colimitsOfShape J Y
Module: Mathlib.CategoryTheory.Preadditive.Schur

Goal state before:
pp: case neg
C : Type u_1
inst✝⁸ : Category.{v_1, u_1} C
inst✝⁷ : Preadditive C
𝕜 : Type u_2
inst✝⁶ : Field 𝕜
inst✝⁵ : IsAlgClosed 𝕜
inst✝⁴ : Linear 𝕜 C
inst✝³ : HasKernels C
X Y : C
inst✝² : ∀ (X Y : C), FiniteDimensional 𝕜 (X ⟶ Y)
inst✝¹ : Simple X
inst✝ : Simple Y
h : ¬Nonempty (X ≅ Y)
⊢ finrank 𝕜 (X ⟶ Y) = 0

Tactic:
· exact (finrank_hom_simple_simple_eq_zero_iff 𝕜 X Y).2 (not_nonempty_iff.mp h)

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset

Goal state before:
pp: κ : Cardinal.{u}
inst✝ : Fact κ.IsRegular
X : Type u
hX : Cardinal.mk X = κ
α : Type u := (S : Set X) × (x : PartialOrder ↑S) × ULift.{u, 0} (PLift (IsCardinalFiltered (↑S) κ))
this : (a : α) → PartialOrder ↑a.fst := fun a ↦ a.snd.fst
ι : α → CardinalDirectedPoset κ := fun a ↦ { obj := { carrier := ↑a.fst, str := this a }, property := ⋯ }
J : CardinalDirectedPoset κ
x✝ : hasCardinalLTWithTerminal κ J
hJ : HasCardinalLT (↑J.obj) κ
right✝ : HasTerminal ↑J.obj
⊢ Cardinal.mk ↑J.obj ≤ Cardinal.mk X

Tactic:
simpa using

Goal state after:
κ : Cardinal.{u}
inst✝ : Fact κ.IsRegular
X : Type u
hX : Cardinal.mk X = κ
α : Type u := (S : Set X) × (x : PartialOrder ↑S) × ULift.{u, 0} (PLift (IsCardinalFiltered (↑S) κ))
this : (a : α) → PartialOrder ↑a.fst := fun a ↦ a.snd.fst
ι : α → CardinalDirectedPoset κ := fun a ↦ { obj := { carrier := ↑a.fst, str := this a }, property := ⋯ }
J : CardinalDirectedPoset κ
x✝ : hasCardinalLTWithTerminal κ J
hJ : HasCardinalLT (↑J.obj) κ
right✝ : HasTerminal ↑J.obj
⊢ Cardinal.mk ↑J.obj ≤ κ
Module: Mathlib.Order.Category.PartOrdEmb

Goal state before:
pp: J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ PartOrdEmb
c : Cocone (F ⋙ forget PartOrdEmb)
hc : IsColimit c
x y : CoconePt hc
j : J
x₁ y₁ : ↑(F.obj j)
hx₁ : (ConcreteCategory.hom (c.ι.app j)) x₁ = x
hy₁ : (ConcreteCategory.hom (c.ι.app j)) y₁ = y
h₁ : x₁ ≤ y₁
k : J
y₂ x₂ : ↑(F.obj k)
hy₂ : (ConcreteCategory.hom (c.ι.app k)) y₂ = y
hx₂ : (ConcreteCategory.hom (c.ι.app k)) x₂ = x
h₂ : y₂ ≤ x₂
l : J
a : j ⟶ l
b : k ⟶ l
x₃ y₃ : ↑(F.obj l)
h₃ : x₃ = (ConcreteCategory.hom (F.map a)) x₁
h₄ : x₃ = (ConcreteCategory.hom (F.map b)) x₂
h₅ : y₃ = (ConcreteCategory.hom (F.map a)) y₁
h₆ : y₃ = (ConcreteCategory.hom (F.map b)) y₂
⊢ x₃ ≤ y₃

Tactic:
simpa using

Goal state after:
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ PartOrdEmb
c : Cocone (F ⋙ forget PartOrdEmb)
hc : IsColimit c
x y : CoconePt hc
j : J
x₁ y₁ : ↑(F.obj j)
hx₁ : (ConcreteCategory.hom (c.ι.app j)) x₁ = x
hy₁ : (ConcreteCategory.hom (c.ι.app j)) y₁ = y
h₁ : x₁ ≤ y₁
k : J
y₂ x₂ : ↑(F.obj k)
hy₂ : (ConcreteCategory.hom (c.ι.app k)) y₂ = y
hx₂ : (ConcreteCategory.hom (c.ι.app k)) x₂ = x
h₂ : y₂ ≤ x₂
l : J
a : j ⟶ l
b : k ⟶ l
x₃ y₃ : ↑(F.obj l)
h₃ : x₃ = (ConcreteCategory.hom (F.map a)) x₁
h₄ : x₃ = (ConcreteCategory.hom (F.map b)) x₂
h₅ : y₃ = (ConcreteCategory.hom (F.map a)) y₁
h₆ : y₃ = (ConcreteCategory.hom (F.map b)) y₂
⊢ (ConcreteCategory.hom (F.map a)) x₁ ≤ (ConcreteCategory.hom (F.map a)) y₁