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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
η : 𝟭 C ≅ F ⋙ G
ε : G ⋙ F ≅ 𝟭 D
⊢ 𝟭 C ≅ F ⋙ G

Tactic:
by
  calc
    𝟭 C ≅ F ⋙ G := η
    _ ≅ F ⋙ 𝟭 D ⋙ G := isoWhiskerLeft F (leftUnitor G).symm
    _ ≅ F ⋙ (G ⋙ F) ⋙ G := isoWhiskerLeft F (isoWhiskerRight ε.symm G)
    _ ≅ F ⋙ G ⋙ F ⋙ G := isoWhiskerLeft F (associator G F G)
    _ ≅ (F ⋙ G) ⋙ F ⋙ G := (associator F G (F ⋙ G)).symm
    _ ≅ 𝟭 C ⋙ F ⋙ G := isoWhiskerRight η.symm (F ⋙ G)
    _ ≅ F ⋙ G := leftUnitor (F ⋙ G)

Goal state after:
Module: Mathlib.CategoryTheory.Equivalence

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : F.IsEquivalence
X : D
⊢ F.preimage ((F.objObjPreimageIso X).hom ≫ 𝟙 X ≫ (F.objObjPreimageIso X).inv) = 𝟙 (F.objPreimage X)

Tactic:
by apply F.map_injective; simp

Goal state after:
Module: Mathlib.CategoryTheory.Equivalence

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : F.IsEquivalence
X Y Z : D
f : X ⟶ Y
g : Y ⟶ Z
⊢ F.preimage ((F.objObjPreimageIso X).hom ≫ (f ≫ g) ≫ (F.objObjPreimageIso Z).inv) =
    F.preimage ((F.objObjPreimageIso X).hom ≫ f ≫ (F.objObjPreimageIso Y).inv) ≫
      F.preimage ((F.objObjPreimageIso Y).hom ≫ g ≫ (F.objObjPreimageIso Z).inv)

Tactic:
by apply F.map_injective; simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
⊢ ofHoms P.homFamily = P

Tactic:
ext _ _ f

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ ofHoms P.homFamily f ↔ P f
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
P : MorphismProperty C
F : C ⥤ D
⊢ (P.map F).RespectsIso

Tactic:
map_eq_isoClosure

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
P : MorphismProperty C
F : C ⥤ D
⊢ (P.strictMap F).isoClosure.RespectsIso
Module: Mathlib.CategoryTheory.Types.Basic

Goal state before:
pp: X Y : Type u
f : X → Y
⊢ Mono (↾f) ↔ Function.Injective f

Tactic:
constructor
  · intro H x x' h
    rw [← homOfElement_eq_iff] at h ⊢
    exact (cancel_mono (ofHom f)).mp h
  · refine fun H => ⟨fun g g' h => ConcreteCategory.hom_ext _ _ fun x ↦
      congrFun (H.comp_left ?_) x⟩
    ext y
    exact ConcreteCategory.congr_hom h y

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ (ρ_ f).inv ▷ g ≫ (α_ f (𝟙 b) g).hom = f ◁ (λ_ g).inv

Tactic:
by
  simp [← cancel_mono (f ◁ (λ_ g).hom)]

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ f ◁ g ◁ (λ_ (𝟙 c)).hom ≫ (α_ f g (𝟙 c)).inv = (α_ f g (𝟙 c ≫ 𝟙 c)).inv ≫ (f ≫ g) ◁ (λ_ (𝟙 c)).hom

Tactic:
associator_inv_naturality_right

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ (α_ f g (𝟙 c ≫ 𝟙 c)).inv ≫ (f ≫ g) ◁ (λ_ (𝟙 c)).hom = (α_ f g (𝟙 c ≫ 𝟙 c)).inv ≫ (f ≫ g) ◁ (λ_ (𝟙 c)).hom
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : WalkingSpan ⥤ C
s t : Cocone F
i : s.pt ≅ t.pt
w₁ : s.ι.app WalkingCospan.left ≫ i.hom = t.ι.app WalkingCospan.left
w₂ : s.ι.app WalkingCospan.right ≫ i.hom = t.ι.app WalkingCospan.right
⊢ s ≅ t

Tactic:
apply Cocone.ext i _

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : WalkingSpan ⥤ C
s t : Cocone F
i : s.pt ≅ t.pt
w₁ : s.ι.app WalkingCospan.left ≫ i.hom = t.ι.app WalkingCospan.left
w₂ : s.ι.app WalkingCospan.right ≫ i.hom = t.ι.app WalkingCospan.right
⊢ ∀ (j : WalkingSpan), s.ι.app j ≫ i.hom = t.ι.app j
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: X Y Z W : WalkingParallelPair
f : WalkingParallelPairHom X Y
g : WalkingParallelPairHom Y Z
h : WalkingParallelPairHom Z W
⊢ (f.comp g).comp h = f.comp (g.comp h)

Tactic:
by
  cases f <;> cases g <;> cases h <;> rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback

Goal state before:
pp: case refine_3
C : Type u
inst✝⁵ : Category.{v, u} C
W✝ X✝ Y✝ Z✝ W X Y Z S T : C
f₁ : W ⟶ S
f₂ : X ⟶ S
inst✝⁴ : HasPullback f₁ f₂
g₁ : Y ⟶ T
g₂ : Z ⟶ T
inst✝³ : HasPullback g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
inst✝² : IsIso i₁
inst✝¹ : IsIso i₂
inst✝ : IsIso i₃
⊢ map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂ ≫ map g₁ g₂ f₁ f₂ (inv i₁) (inv i₂) (inv i₃) ⋯ ⋯ = 𝟙 (pullback f₁ f₂)

pp: case refine_4
C : Type u
inst✝⁵ : Category.{v, u} C
W✝ X✝ Y✝ Z✝ W X Y Z S T : C
f₁ : W ⟶ S
f₂ : X ⟶ S
inst✝⁴ : HasPullback f₁ f₂
g₁ : Y ⟶ T
g₂ : Z ⟶ T
inst✝³ : HasPullback g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
inst✝² : IsIso i₁
inst✝¹ : IsIso i₂
inst✝ : IsIso i₃
⊢ map g₁ g₂ f₁ f₂ (inv i₁) (inv i₂) (inv i₃) ⋯ ⋯ ≫ map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂ = 𝟙 (pullback g₁ g₂)

Tactic:
· cat_disch

Goal state after:
case refine_4
C : Type u
inst✝⁵ : Category.{v, u} C
W✝ X✝ Y✝ Z✝ W X Y Z S T : C
f₁ : W ⟶ S
f₂ : X ⟶ S
inst✝⁴ : HasPullback f₁ f₂
g₁ : Y ⟶ T
g₂ : Z ⟶ T
inst✝³ : HasPullback g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
inst✝² : IsIso i₁
inst✝¹ : IsIso i₂
inst✝ : IsIso i₃
⊢ map g₁ g₂ f₁ f₂ (inv i₁) (inv i₂) (inv i₃) ⋯ ⋯ ≫ map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂ = 𝟙 (pullback g₁ g₂)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback

Goal state before:
pp: case refine_4
C : Type u
inst✝⁵ : Category.{v, u} C
W✝ X✝ Y✝ Z✝ W X Y Z S T : C
f₁ : W ⟶ S
f₂ : X ⟶ S
inst✝⁴ : HasPullback f₁ f₂
g₁ : Y ⟶ T
g₂ : Z ⟶ T
inst✝³ : HasPullback g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
inst✝² : IsIso i₁
inst✝¹ : IsIso i₂
inst✝ : IsIso i₃
⊢ map g₁ g₂ f₁ f₂ (inv i₁) (inv i₂) (inv i₃) ⋯ ⋯ ≫ map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂ = 𝟙 (pullback g₁ g₂)

Tactic:
· cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝³ : Category.{v₁, u₁} T
D : Type u₂
inst✝² : Category.{v₂, u₂} D
X : T
f✝ g : Over X
φ : f✝ ⟶ g
F : T ⥤ D
inst✝¹ : F.Faithful
inst✝ : F.Full
A B : Over X
f : (post F).obj A ⟶ (post F).obj B
a : A.left ⟶ B.left
ha : F.map a = Hom.left f
⊢ F.map (a ≫ B.hom) = F.map A.hom

Tactic:
simp [ha, dsimp% f.w]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback

Goal state before:
pp: case refine_3
C : Type u
inst✝⁵ : Category.{v, u} C
W✝ X✝ Y✝ Z✝ W X Y Z S T : C
f₁ : S ⟶ W
f₂ : S ⟶ X
inst✝⁴ : HasPushout f₁ f₂
g₁ : T ⟶ Y
g₂ : T ⟶ Z
inst✝³ : HasPushout g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₁ = i₃ ≫ g₁
eq₂ : f₂ ≫ i₂ = i₃ ≫ g₂
inst✝² : IsIso i₁
inst✝¹ : IsIso i₂
inst✝ : IsIso i₃
⊢ map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂ ≫ map g₁ g₂ f₁ f₂ (inv i₁) (inv i₂) (inv i₃) ⋯ ⋯ = 𝟙 (pushout f₁ f₂)

pp: case refine_4
C : Type u
inst✝⁵ : Category.{v, u} C
W✝ X✝ Y✝ Z✝ W X Y Z S T : C
f₁ : S ⟶ W
f₂ : S ⟶ X
inst✝⁴ : HasPushout f₁ f₂
g₁ : T ⟶ Y
g₂ : T ⟶ Z
inst✝³ : HasPushout g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₁ = i₃ ≫ g₁
eq₂ : f₂ ≫ i₂ = i₃ ≫ g₂
inst✝² : IsIso i₁
inst✝¹ : IsIso i₂
inst✝ : IsIso i₃
⊢ map g₁ g₂ f₁ f₂ (inv i₁) (inv i₂) (inv i₃) ⋯ ⋯ ≫ map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂ = 𝟙 (pushout g₁ g₂)

Tactic:
· cat_disch

Goal state after:
case refine_4
C : Type u
inst✝⁵ : Category.{v, u} C
W✝ X✝ Y✝ Z✝ W X Y Z S T : C
f₁ : S ⟶ W
f₂ : S ⟶ X
inst✝⁴ : HasPushout f₁ f₂
g₁ : T ⟶ Y
g₂ : T ⟶ Z
inst✝³ : HasPushout g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₁ = i₃ ≫ g₁
eq₂ : f₂ ≫ i₂ = i₃ ≫ g₂
inst✝² : IsIso i₁
inst✝¹ : IsIso i₂
inst✝ : IsIso i₃
⊢ map g₁ g₂ f₁ f₂ (inv i₁) (inv i₂) (inv i₃) ⋯ ⋯ ≫ map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂ = 𝟙 (pushout g₁ g₂)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback

Goal state before:
pp: case refine_4
C : Type u
inst✝⁵ : Category.{v, u} C
W✝ X✝ Y✝ Z✝ W X Y Z S T : C
f₁ : S ⟶ W
f₂ : S ⟶ X
inst✝⁴ : HasPushout f₁ f₂
g₁ : T ⟶ Y
g₂ : T ⟶ Z
inst✝³ : HasPushout g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₁ = i₃ ≫ g₁
eq₂ : f₂ ≫ i₂ = i₃ ≫ g₂
inst✝² : IsIso i₁
inst✝¹ : IsIso i₂
inst✝ : IsIso i₃
⊢ map g₁ g₂ f₁ f₂ (inv i₁) (inv i₂) (inv i₃) ⋯ ⋯ ≫ map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂ = 𝟙 (pushout g₁ g₂)

Tactic:
· cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
Y : Under X
⊢ Hom.right (mkIdInitial.to Y) = Y.hom

Tactic:
by
  rw [mkIdInitial.hom_ext (mkIdInitial.to Y) (homMk Y.hom)]
  rfl

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝³ : Category.{v₁, u₁} T
D : Type u₂
inst✝² : Category.{v₂, u₂} D
X : T
f✝ g : Under X
φ : f✝ ⟶ g
F : T ⥤ D
inst✝¹ : F.Faithful
inst✝ : F.Full
A B : Under X
f : (post F).obj A ⟶ (post F).obj B
a : A.right ⟶ B.right
ha : F.map a = Hom.right f
⊢ F.map (A.hom ≫ a) = F.map B.hom

Tactic:
simp [ha, dsimp% f.w]

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : T
Z Y : Under (op X)
f : Z ⟶ Y
⊢ (Hom.right f).unop ≫ (unop (op (Over.mk Z.hom.unop))).hom = (unop (op (Over.mk Y.hom.unop))).hom

Tactic:
dsimp; rw [← unop_comp, Under.w]

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 : WalkingParallelPair ⥤ C
p : F.obj zero ⟶ G.obj zero
q : F.obj one ⟶ G.obj one
hl : F.map left ≫ q = p ≫ G.map left
hr : F.map right ≫ q = p ≫ G.map right
⊢ ∀ ⦃X Y : WalkingParallelPair⦄ (f : X ⟶ Y),
    F.map f ≫ WalkingParallelPair.casesOn Y p q = WalkingParallelPair.casesOn X p q ≫ G.map f

Tactic:
rintro _ _ (_ | _); all_goals cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
e : E
f : StructuredArrow e G
X✝ Y✝ : StructuredArrow f (pre e F G)
φ : X✝ ⟶ Y✝
⊢ (mk (Hom.right X✝.hom)).hom ≫ F.map (Hom.right (Hom.right φ)) = (mk (Hom.right Y✝.hom)).hom

Tactic:
rw [← w φ, comp_right]
    simp

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 : WalkingParallelPair ⥤ C
p : F.obj zero ≅ G.obj zero
q : F.obj one ≅ G.obj one
hl : F.map left ≫ q.hom = p.hom ≫ G.map left
hr : F.map right ≫ q.hom = p.hom ≫ G.map right
⊢ ∀ {X Y : WalkingParallelPair} (f : X ⟶ Y),
    F.map f ≫ (WalkingParallelPair.casesOn Y p q).hom = (WalkingParallelPair.casesOn X p q).hom ≫ G.map f

Tactic:
rintro _ _ (_ | _); all_goals cat_disch

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

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
X Y : C
hY : IsZero Y
e : X ≅ Y
Z : C
f : Z ⟶ X
⊢ f = default

Tactic:
· rw [← cancel_mono e.hom]
    apply hY.eq_of_tgt

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Semi

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
M : SemimoduleCat R
inst✝ : Subsingleton ↑M
X : SemimoduleCat R
f : X ⟶ M
⊢ f = default

Tactic:
ext x
    subsingleton

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
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
inst✝¹ : HasEqualizer f g
inst✝ : HasEqualizer (G.map f) (G.map g)
⊢ G.map (equalizer.ι f g) ≫ G.map f = G.map (equalizer.ι f g) ≫ G.map g

Tactic:
by simp only [← G.map_comp]; rw [equalizer.condition]

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
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
inst✝¹ : HasEqualizer f g
inst✝ : HasEqualizer (G.map f) (G.map g)
Z : C
h : Z ⟶ X
w : h ≫ f = h ≫ g
⊢ G.map (equalizer.lift h w) ≫ equalizerComparison f g G = equalizer.lift (G.map h) ⋯

Tactic:
apply equalizer.hom_ext
  simp [← G.map_comp]

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

Goal state before:
pp: case left_inv
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X Y : C
⊢ autoParam
    (Function.LeftInverse (fun a ↦ And.casesOn a fun hX hY ↦ ((idZeroEquivIsoZero X) hX, (idZeroEquivIsoZero Y) hY)) ⋯)
    Equiv.left_inv._autoParam

pp: case right_inv
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X Y : C
⊢ autoParam
    (Function.RightInverse (fun a ↦ And.casesOn a fun hX hY ↦ ((idZeroEquivIsoZero X) hX, (idZeroEquivIsoZero Y) hY)) ⋯)
    Equiv.right_inv._autoParam

Tactic:
· cat_disch

Goal state after:
case right_inv
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X Y : C
⊢ autoParam
    (Function.RightInverse (fun a ↦ And.casesOn a fun hX hY ↦ ((idZeroEquivIsoZero X) hX, (idZeroEquivIsoZero Y) hY)) ⋯)
    Equiv.right_inv._autoParam
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

Goal state before:
pp: case right_inv
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X Y : C
⊢ autoParam
    (Function.RightInverse (fun a ↦ And.casesOn a fun hX hY ↦ ((idZeroEquivIsoZero X) hX, (idZeroEquivIsoZero Y) hY)) ⋯)
    Equiv.right_inv._autoParam

Tactic:
· cat_disch

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasInitial C
X : C
f : X ⟶ ⊥_ C
⊢ f ≫ 𝟙 (⊥_ C) = f ≫ 0

Tactic:
congr!; subsingleton

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasTerminal C
X : C
f : ⊤_ C ⟶ X
⊢ 𝟙 (⊤_ C) ≫ f = 0 ≫ f

Tactic:
congr!; subsingleton

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)
⊢ IsIso ((colimit.isColimit F).descCoconeMorphism c)

Tactic:
suffices IsIso ((Cocone.functoriality F G).map
      (IsColimit.descCoconeMorphism (colimit.isColimit F) c)) from by
        apply isIso_of_reflects_iso _ (Cocone.functoriality F G)

Goal state after:
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)
⊢ IsIso ((Cocone.functoriality F G).map ((colimit.isColimit F).descCoconeMorphism c))
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasBinaryCoproducts D
i : ∀ {X Y : C}, IsIso (coprodComparison G X Y)
⊢ ∀ {K : Discrete WalkingPair ⥤ C}, PreservesColimit K G

Tactic:
intro K
    have : PreservesColimit (pair (K.obj ⟨WalkingPair.left⟩) (K.obj ⟨WalkingPair.right⟩)) G :=
      PreservesColimitPair.of_iso_coprod_comparison ..
    apply preservesColimit_of_iso_diagram G (diagramIsoPair K).symm

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝¹ : HasCokernel f
X' Y' : C
f' : X' ⟶ Y'
inst✝ : HasCokernel f'
p : X ⟶ X'
q : Y ⟶ Y'
w : f ≫ q = p ≫ f'
⊢ f ≫ q ≫ π f' = 0

Tactic:
have : f ≫ q ≫ π f' = p ≫ f' ≫ π f' := by
      simp only [← Category.assoc]
      apply congrArg (· ≫ π f') w
    simp [this]

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

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : Category.{v_2, u_2} D
inst✝⁷ : Category.{v_3, u_3} E
inst✝⁶ : Preadditive C
inst✝⁵ : Preadditive D
inst✝⁴ : Preadditive E
F : C ⥤ D
inst✝³ : F.Additive
inst✝² : F.Full
inst✝¹ : F.EssSurj
G : D ⥤ E
inst✝ : (F ⋙ G).Additive
X Y : D
f g : X ⟶ Y
f' : F.objPreimage X ⟶ F.objPreimage Y
hf' : F.map f' = (F.objObjPreimageIso X).hom ≫ f ≫ (F.objObjPreimageIso Y).inv
⊢ G.map (f + g) = G.map f + G.map g

Tactic:
obtain ⟨g', hg'⟩ := F.map_surjective ((F.objObjPreimageIso X).hom ≫ g ≫
      (F.objObjPreimageIso Y).inv)

Goal state after:
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : Category.{v_2, u_2} D
inst✝⁷ : Category.{v_3, u_3} E
inst✝⁶ : Preadditive C
inst✝⁵ : Preadditive D
inst✝⁴ : Preadditive E
F : C ⥤ D
inst✝³ : F.Additive
inst✝² : F.Full
inst✝¹ : F.EssSurj
G : D ⥤ E
inst✝ : (F ⋙ G).Additive
X Y : D
f g : X ⟶ Y
f' : F.objPreimage X ⟶ F.objPreimage Y
hf' : F.map f' = (F.objObjPreimageIso X).hom ≫ f ≫ (F.objObjPreimageIso Y).inv
g' : F.objPreimage X ⟶ F.objPreimage Y
hg' : F.map g' = (F.objObjPreimageIso X).hom ≫ g ≫ (F.objObjPreimageIso Y).inv
⊢ G.map (f + g) = G.map f + G.map g
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
J : Type u_1
inst✝ : Fintype J
f : J → C
b : Bicone f
total : ∑ j, b.π j ≫ b.ι j = 𝟙 b.pt
s : Cocone (Discrete.functor f)
m : b.toCocone.pt ⟶ s.pt
h : ∀ (j : Discrete J), b.toCocone.ι.app j ≫ m = s.ι.app j
⊢ (∑ j, b.π j ≫ b.ι j) ≫ m = ∑ j, b.π j ≫ s.ι.app { as := j }

Tactic:
sum_comp

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
J : Type u_1
inst✝ : Fintype J
f : J → C
b : Bicone f
total : ∑ j, b.π j ≫ b.ι j = 𝟙 b.pt
s : Cocone (Discrete.functor f)
m : b.toCocone.pt ⟶ s.pt
h : ∀ (j : Discrete J), b.toCocone.ι.app j ≫ m = s.ι.app j
⊢ ∑ j, (b.π j ≫ b.ι j) ≫ m = ∑ j, b.π j ≫ s.ι.app { as := j }
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts

Goal state before:
pp: case left
J : Type w
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
D : Type uD
inst✝¹ : Category.{uD', uD} D
inst✝ : HasZeroMorphisms D
P P' Q Q' X Y : C
b : BinaryBicone X Y
j' : WalkingPair
⊢ WalkingPair.casesOn WalkingPair.left b.inl b.inr ≫ WalkingPair.casesOn j' b.fst b.snd =
    if h : WalkingPair.left = j' then eqToHom ⋯ else 0

Tactic:
rcases j' with ⟨⟩

Goal state after:
case left.left
J : Type w
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
D : Type uD
inst✝¹ : Category.{uD', uD} D
inst✝ : HasZeroMorphisms D
P P' Q Q' X Y : C
b : BinaryBicone X Y
⊢ WalkingPair.casesOn WalkingPair.left b.inl b.inr ≫ WalkingPair.casesOn WalkingPair.left b.fst b.snd =
    if h : WalkingPair.left = WalkingPair.left then eqToHom ⋯ else 0

case left.right
J : Type w
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
D : Type uD
inst✝¹ : Category.{uD', uD} D
inst✝ : HasZeroMorphisms D
P P' Q Q' X Y : C
b : BinaryBicone X Y
⊢ WalkingPair.casesOn WalkingPair.left b.inl b.inr ≫ WalkingPair.casesOn WalkingPair.right b.fst b.snd =
    if h : WalkingPair.left = WalkingPair.right then eqToHom ⋯ else 0
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts

Goal state before:
pp: case right
J : Type w
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
D : Type uD
inst✝¹ : Category.{uD', uD} D
inst✝ : HasZeroMorphisms D
P P' Q Q' X Y : C
b : BinaryBicone X Y
j' : WalkingPair
⊢ WalkingPair.casesOn WalkingPair.right b.inl b.inr ≫ WalkingPair.casesOn j' b.fst b.snd =
    if h : WalkingPair.right = j' then eqToHom ⋯ else 0

Tactic:
rcases j' with ⟨⟩

Goal state after:
case right.left
J : Type w
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
D : Type uD
inst✝¹ : Category.{uD', uD} D
inst✝ : HasZeroMorphisms D
P P' Q Q' X Y : C
b : BinaryBicone X Y
⊢ WalkingPair.casesOn WalkingPair.right b.inl b.inr ≫ WalkingPair.casesOn WalkingPair.left b.fst b.snd =
    if h : WalkingPair.right = WalkingPair.left then eqToHom ⋯ else 0

case right.right
J : Type w
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
D : Type uD
inst✝¹ : Category.{uD', uD} D
inst✝ : HasZeroMorphisms D
P P' Q Q' X Y : C
b : BinaryBicone X Y
⊢ WalkingPair.casesOn WalkingPair.right b.inl b.inr ≫ WalkingPair.casesOn WalkingPair.right b.fst b.snd =
    if h : WalkingPair.right = WalkingPair.right then eqToHom ⋯ else 0
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Goal state before:
pp: J✝ : Type w
C✝ : Type uC
inst✝⁷ : Category.{uC', uC} C✝
inst✝⁶ : HasZeroMorphisms C✝
D : Type uD
inst✝⁵ : Category.{uD', uD} D
inst✝⁴ : HasZeroMorphisms D
F : J✝ → C✝
J : Type w
K : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
i : J
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct (Subtype.restrict (fun j ↦ j ≠ i) f)
s : Fork (π f i) 0
⊢ (s.ι ≫ toSubtype f fun j ↦ j ≠ i) ≫ Fork.ι (KernelFork.ofι (fromSubtype f fun j ↦ j ≠ i) ⋯) = s.ι

Tactic:
apply biproduct.hom_ext

Goal state after:
J✝ : Type w
C✝ : Type uC
inst✝⁷ : Category.{uC', uC} C✝
inst✝⁶ : HasZeroMorphisms C✝
D : Type uD
inst✝⁵ : Category.{uD', uD} D
inst✝⁴ : HasZeroMorphisms D
F : J✝ → C✝
J : Type w
K : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
i : J
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct (Subtype.restrict (fun j ↦ j ≠ i) f)
s : Fork (π f i) 0
⊢ ∀ (j : J),
    ((s.ι ≫ toSubtype f fun j ↦ j ≠ i) ≫ Fork.ι (KernelFork.ofι (fromSubtype f fun j ↦ j ≠ i) ⋯)) ≫ π f j = s.ι ≫ π f j
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts

Goal state before:
pp: J : Type w
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
D : Type uD
inst✝¹ : Category.{uD', uD} D
inst✝ : HasZeroMorphisms D
P Q P' Q' : C
b : BinaryBicone P Q
hb : b.IsBilimit
eP : P ≅ P'
eQ : Q ≅ Q'
⊢ (Cocone.precompose (mapPairIso eP eQ).inv).obj b.toCocone ≅ (b.ofIso eP eQ).toCocone

Tactic:
exact BinaryCofan.ext (Iso.refl _) (by simp [BinaryCofan.inl])
      (by simp [BinaryCofan.inr])

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

Goal state before:
pp: J : Type w
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
D : Type uD
inst✝¹ : Category.{uD', uD} D
inst✝ : HasZeroMorphisms D
P Q X Y : C
c : BinaryBicone X Y
i : IsColimit c.toCocone
s : Cofork c.inl 0
⊢ Cofork.π c.inlCokernelCofork ≫ c.inr ≫ s.π = s.π

Tactic:
apply BinaryCofan.IsColimit.hom_ext i <;> simp

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

Goal state before:
pp: J : Type w
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
D : Type uD
inst✝¹ : Category.{uD', uD} D
inst✝ : HasZeroMorphisms D
P Q X Y : C
c : BinaryBicone X Y
i : IsColimit c.toCocone
s : Cofork c.inr 0
⊢ Cofork.π c.inrCokernelCofork ≫ c.inl ≫ s.π = s.π

Tactic:
apply BinaryCofan.IsColimit.hom_ext i <;> simp

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Basic

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
M : ModuleCat R
inst✝ : Subsingleton ↑M
X : ModuleCat R
f : X ⟶ M
⊢ f = default

Tactic:
ext x
    subsingleton

Goal state after: