mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : HasZeroObject D
inst✝¹ : HasZeroMorphisms D
G : C ⥤ D
hG : IsZero G
J : Type u_1
inst✝ : Category.{v_1, u_1} J
K : J ⥤ C
c✝ : Cocone K
x✝ : IsColimit c✝
⊢ IsColimit (G.mapCocone c✝)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: C : Type u
X✝ Y✝ : C
inst✝² : Category.{v, u} C
f✝ g : X✝ ⟶ Y✝
inst✝¹ : IsSplitEpi f✝
X Y : C
f : X ⟶ Y
inst✝ : IsSplitEpi f
s : Cofork (𝟙 X) (f ≫ section_ f)
m✝ : (coconeOfIsSplitEpi f).pt ⟶ s.pt
hm : (coconeOfIsSplitEpi f).π ≫ m✝ = s.π
⊢ m✝ = section_ f ≫ s.π

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
c : Cofork f g
i : IsColimit c
W : C
h : W ⟶ X
hm : Epi h
⊢ (h ≫ f) ≫ c.π = (h ≫ g) ≫ c.π

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
c : Cofork f g
i : IsColimit c
W : C
h : W ⟶ X
hm : Epi h
s : Cofork (h ≫ f) (h ≫ g)
⊢ f ≫ s.π = g ≫ s.π

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K✝ : J✝ ⥤ C
J : Type w'
𝒥 : Category.{w, w'} J
K : J ⥤ C
c : Cone K
h : IsLimit ((𝟭 C).mapCone c)
⊢ ∀ (s : Cone K) (j : J),
    h.lift { pt := s.pt, π := { app := fun j ↦ s.π.app j, naturality := ⋯ } } ≫ c.π.app j = s.π.app j

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Basic

Goal state before:
pp: case mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w'
𝒥 : Category.{w, w'} J
obj✝ : J → C
map✝ : {X Y : J} → (X ⟶ Y) → (obj✝ X ⟶ obj✝ Y)
map_id✝ : ∀ (X : J), map✝ (𝟙 X) = 𝟙 (obj✝ X)
map_comp✝ : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), map✝ (f ≫ g) = map✝ f ≫ map✝ g
pt✝ : C
app✝ :
  (X : J) →
    ((Functor.const J).obj pt✝).obj X ⟶ { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.obj X
naturality✝ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y),
    ((Functor.const J).obj pt✝).map f ≫ app✝ Y =
      app✝ X ≫ { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.map f
h : IsLimit ((𝟭 C).mapCone { pt := pt✝, π := { app := app✝, naturality := naturality✝ } })
⊢ ∀ (s : Cone { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ })
    (m : s.pt ⟶ { pt := pt✝, π := { app := app✝, naturality := naturality✝ } }.pt),
    (∀ (j : J), m ≫ { pt := pt✝, π := { app := app✝, naturality := naturality✝ } }.π.app j = s.π.app j) →
      m = h.lift { pt := s.pt, π := { app := fun j ↦ s.π.app j, naturality := ⋯ } }

Tactic:
intro s m w

Goal state after:
case mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w'
𝒥 : Category.{w, w'} J
obj✝ : J → C
map✝ : {X Y : J} → (X ⟶ Y) → (obj✝ X ⟶ obj✝ Y)
map_id✝ : ∀ (X : J), map✝ (𝟙 X) = 𝟙 (obj✝ X)
map_comp✝ : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), map✝ (f ≫ g) = map✝ f ≫ map✝ g
pt✝ : C
app✝ :
  (X : J) →
    ((Functor.const J).obj pt✝).obj X ⟶ { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.obj X
naturality✝ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y),
    ((Functor.const J).obj pt✝).map f ≫ app✝ Y =
      app✝ X ≫ { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.map f
h : IsLimit ((𝟭 C).mapCone { pt := pt✝, π := { app := app✝, naturality := naturality✝ } })
s : Cone { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }
m : s.pt ⟶ { pt := pt✝, π := { app := app✝, naturality := naturality✝ } }.pt
w : ∀ (j : J), m ≫ { pt := pt✝, π := { app := app✝, naturality := naturality✝ } }.π.app j = s.π.app j
⊢ m = h.lift { pt := s.pt, π := { app := fun j ↦ s.π.app j, naturality := ⋯ } }
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
c : Cofork f g
i : IsColimit c
W : C
h : W ⟶ X
hm✝ : Epi h
s : Cofork (h ≫ f) (h ≫ g)
s' : Cofork f g := Cofork.ofπ s.π ⋯
l : { l // c.π ≫ l = s'.π } := Cofork.IsColimit.desc' i s'.π ⋯
m✝ : (Cofork.ofπ c.π ⋯).pt ⟶ s.pt
hm : (Cofork.ofπ c.π ⋯).π ≫ m✝ = s.π
⊢ m✝ = ↑l

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: C : Type u
X✝ Y : C
inst✝ : Category.{v, u} C
f✝ g : X✝ ⟶ Y
X : C
f : X ⟶ X
hf : f ≫ f = f
c : Cofork (𝟙 X) f
i : IsColimit c
⊢ 𝟙 X ≫ f = f ≫ f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: C : Type u
X✝ Y : C
inst✝ : Category.{v, u} C
f✝ g : X✝ ⟶ Y
X : C
f : X ⟶ X
hf : f ≫ f = f
c : Cofork (𝟙 X) f
i : IsColimit c
this : Epi c.π := epi_of_isColimit_cofork i
⊢ (c.π ≫ i.desc (Cofork.ofπ f ⋯)) ≫ c.π = c.π

Tactic:
Cofork.IsColimit.π_desc,

Goal state after:
C : Type u
X✝ Y : C
inst✝ : Category.{v, u} C
f✝ g : X✝ ⟶ Y
X : C
f : X ⟶ X
hf : f ≫ f = f
c : Cofork (𝟙 X) f
i : IsColimit c
this : Epi c.π := epi_of_isColimit_cofork i
⊢ (Cofork.ofπ f ⋯).π ≫ c.π = c.π
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: C : Type u
X✝ Y : C
inst✝ : Category.{v, u} C
f✝ g : X✝ ⟶ Y
X : C
f : X ⟶ X
hf : f ≫ f = f
c : Cofork (𝟙 X) f
i : IsColimit c
⊢ i.desc (Cofork.ofπ f ⋯) ≫ c.π = 𝟙 c.pt

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K✝ : J✝ ⥤ C
J : Type w'
𝒥 : Category.{w, w'} J
K : J ⥤ C
c : Cone K
h : IsLimit ((𝟭 C).mapCone c)
⊢ ∀ (s : Cone K) (m : s.pt ⟶ c.pt),
    (∀ (j : J), m ≫ c.π.app j = s.π.app j) →
      m = h.lift { pt := s.pt, π := { app := fun j ↦ s.π.app j, naturality := ⋯ } }

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K✝ : J✝ ⥤ C
J : Type w'
𝒥 : Category.{w, w'} J
K : J ⥤ C
c : Cocone K
h : IsColimit ((𝟭 C).mapCocone c)
⊢ ∀ (s : Cocone K) (j : J),
    c.ι.app j ≫ h.desc { pt := s.pt, ι := { app := fun j ↦ s.ι.app j, naturality := ⋯ } } = s.ι.app j

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Basic

Goal state before:
pp: case mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w'
𝒥 : Category.{w, w'} J
obj✝ : J → C
map✝ : {X Y : J} → (X ⟶ Y) → (obj✝ X ⟶ obj✝ Y)
map_id✝ : ∀ (X : J), map✝ (𝟙 X) = 𝟙 (obj✝ X)
map_comp✝ : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), map✝ (f ≫ g) = map✝ f ≫ map✝ g
pt✝ : C
app✝ :
  (X : J) →
    { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.obj X ⟶ ((Functor.const J).obj pt✝).obj X
naturality✝ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y),
    { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.map f ≫ app✝ Y =
      app✝ X ≫ ((Functor.const J).obj pt✝).map f
h : IsColimit ((𝟭 C).mapCocone { pt := pt✝, ι := { app := app✝, naturality := naturality✝ } })
⊢ ∀ (s : Cocone { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ })
    (m : { pt := pt✝, ι := { app := app✝, naturality := naturality✝ } }.pt ⟶ s.pt),
    (∀ (j : J), { pt := pt✝, ι := { app := app✝, naturality := naturality✝ } }.ι.app j ≫ m = s.ι.app j) →
      m = h.desc { pt := s.pt, ι := { app := fun j ↦ s.ι.app j, naturality := ⋯ } }

Tactic:
intro s m w

Goal state after:
case mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w'
𝒥 : Category.{w, w'} J
obj✝ : J → C
map✝ : {X Y : J} → (X ⟶ Y) → (obj✝ X ⟶ obj✝ Y)
map_id✝ : ∀ (X : J), map✝ (𝟙 X) = 𝟙 (obj✝ X)
map_comp✝ : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), map✝ (f ≫ g) = map✝ f ≫ map✝ g
pt✝ : C
app✝ :
  (X : J) →
    { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.obj X ⟶ ((Functor.const J).obj pt✝).obj X
naturality✝ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y),
    { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.map f ≫ app✝ Y =
      app✝ X ≫ ((Functor.const J).obj pt✝).map f
h : IsColimit ((𝟭 C).mapCocone { pt := pt✝, ι := { app := app✝, naturality := naturality✝ } })
s : Cocone { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }
m : { pt := pt✝, ι := { app := app✝, naturality := naturality✝ } }.pt ⟶ s.pt
w : ∀ (j : J), { pt := pt✝, ι := { app := app✝, naturality := naturality✝ } }.ι.app j ≫ m = s.ι.app j
⊢ m = h.desc { pt := s.pt, ι := { app := fun j ↦ s.ι.app j, naturality := ⋯ } }
Module: Mathlib.CategoryTheory.Limits.Preserves.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K✝ : J✝ ⥤ C
J : Type w'
𝒥 : Category.{w, w'} J
K : J ⥤ C
c : Cocone K
h : IsColimit ((𝟭 C).mapCocone c)
⊢ ∀ (s : Cocone K) (m : c.pt ⟶ s.pt),
    (∀ (j : J), c.ι.app j ≫ m = s.ι.app j) →
      m = h.desc { pt := s.pt, ι := { app := fun j ↦ s.ι.app j, naturality := ⋯ } }

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Basic

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
K : J ⥤ C
E : Type u₃
ℰ : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : PreservesLimit K (F ⋙ G)
inst✝ : ReflectsLimit (K ⋙ F) G
c✝ : Cone K
h : IsLimit c✝
⊢ IsLimit (F.mapCone c✝)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Basic

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K₁ K₂ : J ⥤ C
F : C ⥤ D
h : K₁ ≅ K₂
inst✝ : ReflectsLimit K₁ F
c : Cone K₂
t : IsLimit (F.mapCone c)
⊢ IsLimit c

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Basic

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
J' : Type w₂
inst✝¹ : Category.{w₂', w₂} J'
e : J ≌ J'
F : C ⥤ D
inst✝ : ReflectsLimitsOfShape J F
K : J' ⥤ C
c : Cone K
t : IsLimit (F.mapCone c)
⊢ IsLimit c

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Basic

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
J : Type w
inst✝³ : Category.{w', w} J
F : J ⥤ C
G : C ⥤ D
inst✝² : G.ReflectsIsomorphisms
inst✝¹ : HasLimit F
inst✝ : PreservesLimit F G
c : Cone F
t : IsLimit (G.mapCone c)
this : IsIso ((limit.isLimit F).lift c)
⊢ IsLimit c

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Basic

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
J : Type w
inst✝³ : Category.{w', w} J
F : J ⥤ C
G : C ⥤ D
inst✝² : G.ReflectsIsomorphisms
inst✝¹ : HasLimit F
inst✝ : PreservesLimit F G
c : Cone F
t : IsLimit (G.mapCone c)
this : IsIso ((limit.isLimit F).liftConeMorphism c)
⊢ IsIso ((Cone.forget F).map ((limit.isLimit F).liftConeMorphism c))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Basic

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
J : Type w
inst✝³ : Category.{w', w} J
F : J ⥤ C
G : C ⥤ D
inst✝² : G.ReflectsIsomorphisms
inst✝¹ : HasLimit F
inst✝ : PreservesLimit F G
c : Cone F
t : IsLimit (G.mapCone c)
this : IsIso ((Cone.functoriality F G).map ((limit.isLimit F).liftConeMorphism c))
⊢ IsIso ((limit.isLimit F).liftConeMorphism c)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Basic

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
J : Type w
inst✝³ : Category.{w', w} J
F : J ⥤ C
G : C ⥤ D
inst✝² : G.ReflectsIsomorphisms
inst✝¹ : HasLimit F
inst✝ : PreservesLimit F G
c : Cone F
t : IsLimit (G.mapCone c)
⊢ Nonempty (IsLimit c)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Basic

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
K : J ⥤ C
E : Type u₃
ℰ : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : PreservesColimit K (F ⋙ G)
inst✝ : ReflectsColimit (K ⋙ F) G
c : Cocone K
h : IsColimit c
⊢ IsColimit (F.mapCocone c)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Basic

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K₁ K₂ : J ⥤ C
F : C ⥤ D
h : K₁ ≅ K₂
inst✝ : ReflectsColimit K₁ F
c : Cocone K₂
t : IsColimit (F.mapCocone c)
⊢ IsColimit c

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Basic

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
J' : Type w₂
inst✝¹ : Category.{w₂', w₂} J'
e : J ≌ J'
F : C ⥤ D
inst✝ : ReflectsColimitsOfShape J F
K✝ : J' ⥤ C
c : Cocone K✝
t : IsColimit (F.mapCocone c)
⊢ IsColimit c

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Basic

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
J : Type w
inst✝³ : Category.{w', w} J
F : J ⥤ C
G : C ⥤ D
inst✝² : G.ReflectsIsomorphisms
inst✝¹ : HasColimit F
inst✝ : PreservesColimit F G
c : Cocone F
t : IsColimit (G.mapCocone c)
this : IsIso ((colimit.isColimit F).desc c)
⊢ IsColimit c

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Basic

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
J : Type w
inst✝³ : Category.{w', w} J
F : J ⥤ C
G : C ⥤ D
inst✝² : G.ReflectsIsomorphisms
inst✝¹ : HasColimit F
inst✝ : PreservesColimit F G
c : Cocone F
t : IsColimit (G.mapCocone c)
this : IsIso ((colimit.isColimit F).descCoconeMorphism c)
⊢ IsIso ((Cocone.forget F).map ((colimit.isColimit F).descCoconeMorphism c))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Basic

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
J : Type w
inst✝³ : Category.{w', w} J
F : J ⥤ C
G : C ⥤ D
inst✝² : G.ReflectsIsomorphisms
inst✝¹ : HasColimit F
inst✝ : PreservesColimit F G
c : Cocone F
t : IsColimit (G.mapCocone c)
this : IsIso ((Cocone.functoriality F G).map ((colimit.isColimit F).descCoconeMorphism c))
⊢ IsIso ((colimit.isColimit F).descCoconeMorphism c)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Basic

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
J : Type w
inst✝³ : Category.{w', w} J
F : J ⥤ C
G : C ⥤ D
inst✝² : G.ReflectsIsomorphisms
inst✝¹ : HasColimit F
inst✝ : PreservesColimit F G
c : Cocone F
t : IsColimit (G.mapCocone c)
⊢ Nonempty (IsColimit c)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Basic

Goal state before:
pp: C : Type u_1
D : Type u_2
J : Type u_3
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Category.{v_3, u_3} J
K : J ⥤ C
L L' : C ⥤ D
α : L ⟶ L'
inst✝² : IsIso (K.whiskerLeft α)
c : Cocone K
hc : IsColimit c
inst✝¹ : PreservesColimit K L
inst✝ : PreservesColimit K L'
⊢ IsIso (α.app c.pt)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Basic

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J✝ : Type w
inst✝² : Category.{w', w} J✝
K✝ : J✝ ⥤ C
F : C ⥤ D
inst✝¹ : F.Full
inst✝ : F.Faithful
J : Type w'
𝒥₁ : Category.{w, w'} J
K : J ⥤ C
c : Cone K
t : IsLimit (F.mapCone c)
⊢ ∀ (s : Cone K) (m : s ⟶ c),
    m = (Cone.functoriality K F).preimage (t.liftConeMorphism ((Cone.functoriality K F).obj s))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Basic

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J✝ : Type w
inst✝² : Category.{w', w} J✝
K✝ : J✝ ⥤ C
F : C ⥤ D
inst✝¹ : F.Full
inst✝ : F.Faithful
J : Type w'
𝒥₁ : Category.{w, w'} J
K : J ⥤ C
c : Cocone K
t : IsColimit (F.mapCocone c)
⊢ ∀ (s : Cocone K) (m : c ⟶ s),
    m = (Cocone.functoriality K F).preimage (t.descCoconeMorphism ((Cocone.functoriality K F).obj s))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Linear.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X _Y _Z : C
r : ℕ
f : X ⟶ _Y
g : _Y ⟶ _Z
⊢ (r • f) ≫ g = r • f ≫ g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Linear.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
_X _Y Z : C
f : _X ⟶ _Y
r : ℕ
g : _Y ⟶ Z
⊢ f ≫ (r • g) = r • f ≫ g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Linear.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X _Y _Z : C
r : ℤ
f : X ⟶ _Y
g : _Y ⟶ _Z
⊢ (r • f) ≫ g = r • f ≫ g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Linear.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
_X _Y Z : C
f : _X ⟶ _Y
r : ℤ
g : _Y ⟶ Z
⊢ f ≫ (r • g) = r • f ≫ g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Linear.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type w
inst✝¹ : Semiring R
inst✝ : Linear R C
D : Type u'
F : D → C
x✝⁵ x✝⁴ x✝³ : InducedCategory C F
x✝² : R
x✝¹ : x✝⁵ ⟶ x✝⁴
x✝ : x✝⁴ ⟶ x✝³
⊢ (x✝² • x✝¹) ≫ x✝ = x✝² • x✝¹ ≫ x✝

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Linear.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type w
inst✝¹ : Semiring R
inst✝ : Linear R C
D : Type u'
F : D → C
x✝⁵ x✝⁴ x✝³ : InducedCategory C F
x✝² : x✝⁵ ⟶ x✝⁴
x✝¹ : R
x✝ : x✝⁴ ⟶ x✝³
⊢ x✝² ≫ (x✝¹ • x✝) = x✝¹ • x✝² ≫ x✝

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Linear.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type w
inst✝¹ : Semiring R
inst✝ : Linear R C
D : Type u'
F : D → C
X Y : InducedCategory C F
⊢ ∀ (m : R) (x : X ⟶ Y),
    InducedCategory.homAddEquiv.toFun (m • x) = (RingHom.id R) m • InducedCategory.homAddEquiv.toFun x

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Linear.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type w
inst✝¹ : Semiring R
inst✝ : Linear R C
X Y Z : C
f : X ⟶ Y
⊢ ∀ (x y : Y ⟶ Z), f ≫ (x + y) = f ≫ x + f ≫ y

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Linear.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type w
inst✝¹ : Semiring R
inst✝ : Linear R C
X Y Z : C
f : X ⟶ Y
⊢ ∀ (m : R) (x : Y ⟶ Z), f ≫ (m • x) = (RingHom.id R) m • f ≫ x

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Linear.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type w
inst✝¹ : Semiring R
inst✝ : Linear R C
X Y Z : C
g : Y ⟶ Z
⊢ ∀ (x y : X ⟶ Y), (x + y) ≫ g = x ≫ g + y ≫ g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Linear.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type w
inst✝¹ : Semiring R
inst✝ : Linear R C
X Y Z : C
g : Y ⟶ Z
⊢ ∀ (m : R) (x : X ⟶ Y), (m • x) ≫ g = (RingHom.id R) m • x ≫ g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Linear.Basic

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
R : Type w
inst✝³ : Semiring R
inst✝² : Linear R C
X Y : C
f : X ⟶ Y
inst✝¹ : Epi f
r : R
inst✝ : Invertible r
Z✝ : C
g g' : Y ⟶ Z✝
H : (r • f) ≫ g = (r • f) ≫ g'
⊢ g = g'

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.FinCategory.Basic

Goal state before:
pp: α : Type u_1
X Y : Discrete α
⊢ Fintype (X ⟶ Y)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Linear.Basic

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
R : Type w
inst✝³ : Semiring R
inst✝² : Linear R C
X Y : C
f : X ⟶ Y
inst✝¹ : Mono f
r : R
inst✝ : Invertible r
Z✝ : C
g g' : Z✝ ⟶ X
H : g ≫ (r • f) = g' ≫ (r • f)
⊢ g = g'

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Linear.Basic

Goal state before:
pp: C✝ : Type u
inst✝⁷ : Category.{v, u} C✝
inst✝⁶ : Preadditive C✝
R : Type w
inst✝⁵ : Semiring R
inst✝⁴ : Linear R C✝
k : Type u_1
C : Type u_2
inst✝³ : Category.{v_1, u_2} C
inst✝² : Semiring k
inst✝¹ : Preadditive C
inst✝ : Linear k C
X Y W Z : C
f₁ : X ≅ Y
f₂ : W ≅ Z
x : X ⟶ W
⊢ (leftComp k W f₁.hom ∘ₗ rightComp k Y f₂.symm.hom) ((rightComp k Y f₂.hom ∘ₗ leftComp k W f₁.symm.hom).toFun x) = x

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Linear.Basic

Goal state before:
pp: C✝ : Type u
inst✝⁷ : Category.{v, u} C✝
inst✝⁶ : Preadditive C✝
R : Type w
inst✝⁵ : Semiring R
inst✝⁴ : Linear R C✝
k : Type u_1
C : Type u_2
inst✝³ : Category.{v_1, u_2} C
inst✝² : Semiring k
inst✝¹ : Preadditive C
inst✝ : Linear k C
X Y W Z : C
f₁ : X ≅ Y
f₂ : W ≅ Z
x : Y ⟶ Z
⊢ (rightComp k Y f₂.hom ∘ₗ leftComp k W f₁.symm.hom).toFun ((leftComp k W f₁.hom ∘ₗ rightComp k Y f₂.symm.hom) x) = x

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
D : Type u'
F : D → C
x✝⁵ x✝⁴ x✝³ : InducedCategory C F
x✝² x✝¹ : x✝⁵ ⟶ x✝⁴
x✝ : x✝⁴ ⟶ x✝³
⊢ (x✝² + x✝¹) ≫ x✝ = x✝² ≫ x✝ + x✝¹ ≫ x✝

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Linear.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type w
inst✝¹ : Semiring R
inst✝ : Linear R C
X Y Z : C
r : Rˣ
f : X ⟶ Y
g : Y ⟶ Z
⊢ (r • f) ≫ g = r • f ≫ g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
D : Type u'
F : D → C
x✝⁵ x✝⁴ x✝³ : InducedCategory C F
x✝² : x✝⁵ ⟶ x✝⁴
x✝¹ x✝ : x✝⁴ ⟶ x✝³
⊢ x✝² ≫ (x✝¹ + x✝) = x✝² ≫ x✝¹ + x✝² ≫ x✝

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Linear.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type w
inst✝¹ : Semiring R
inst✝ : Linear R C
X Y Z : C
f : X ⟶ Y
r : Rˣ
g : Y ⟶ Z
⊢ f ≫ (r • g) = r • f ≫ g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
D : Type u'
F : D → C
X Y : InducedCategory C F
⊢ ∀ (x y : X ⟶ Y),
    InducedCategory.homEquiv.toFun (x + y) = InducedCategory.homEquiv.toFun x + InducedCategory.homEquiv.toFun y

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Linear.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
S : Type w
inst✝¹ : CommSemiring S
inst✝ : Linear S C
X Y Z : C
⊢ ∀ (x y : X ⟶ Y), leftComp S Z (x + y) = leftComp S Z x + leftComp S Z y

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
Z : ObjectProperty C
x✝⁵ x✝⁴ x✝³ : Z.FullSubcategory
x✝² x✝¹ : x✝⁵ ⟶ x✝⁴
x✝ : x✝⁴ ⟶ x✝³
⊢ (x✝² + x✝¹) ≫ x✝ = x✝² ≫ x✝ + x✝¹ ≫ x✝

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Linear.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
S : Type w
inst✝¹ : CommSemiring S
inst✝ : Linear S C
X Y Z : C
⊢ ∀ (m : S) (x : X ⟶ Y), leftComp S Z (m • x) = (RingHom.id S) m • leftComp S Z x

Tactic:
by

Goal state after: