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

Goal state before:
pp: case h_map
C : Type u₂
inst✝ : Category.{v₂, u₂} C
I : Type u₁
G F : Discrete I ⥤ C
h : ∀ (i : I), G.obj { as := i } = F.obj { as := i }
⊢ autoParam (∀ (X Y : Discrete I) (f : X ⟶ Y), G.map f = eqToHom ⋯ ≫ F.map f ≫ eqToHom ⋯) Functor.ext._auto_1

Tactic:
intro ⟨X⟩ ⟨Y⟩ ⟨⟨p⟩⟩

Goal state after:
case h_map
C : Type u₂
inst✝ : Category.{v₂, u₂} C
I : Type u₁
G F : Discrete I ⥤ C
h : ∀ (i : I), G.obj { as := i } = F.obj { as := i }
X Y : I
p : { as := X }.as = { as := Y }.as
⊢ G.map { down := { down := p } } = eqToHom ⋯ ≫ F.map { down := { down := p } } ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.Pi.Basic

Goal state before:
pp: I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
X Y : (i : I) → C i
f : X ≅ Y
i : I
⊢ 𝟙 X i = 𝟙 (X i)

Tactic:
id_apply

Goal state after:
I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
X Y : (i : I) → C i
f : X ≅ Y
i : I
⊢ 𝟙 (X i) = 𝟙 (X i)
Module: Mathlib.CategoryTheory.Pi.Basic

Goal state before:
pp: I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
X Y : (i : I) → C i
f : X ≅ Y
i : I
⊢ 𝟙 Y i = 𝟙 (Y i)

Tactic:
id_apply

Goal state after:
I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
X Y : (i : I) → C i
f : X ≅ Y
i : I
⊢ 𝟙 (Y i) = 𝟙 (Y i)
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: case refine_2
C : Type u
inst✝³ : Category.{v, u} C
D : Type u_1
inst✝² : Category.{v_1, u_1} D
F : C ⥤ D
inst✝¹ : F.EssSurj
inst✝ : F.Full
X Y : D
f : X ⟶ Y
a✝ : ⊤ f
⊢ Arrow.mk (F.map (F.preimage ((F.objObjPreimageIso X).hom ≫ f ≫ (F.objObjPreimageIso Y).inv))) ≅ Arrow.mk f

Tactic:
· exact Arrow.isoMk' _ _ (Functor.objObjPreimageIso F X) (Functor.objObjPreimageIso F Y)
      (by simp)

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

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_3
X Y : ι → C
f : (i : ι) → X i ⟶ Y i
A B : C
g : A ⟶ B
i : ι
h : Arrow.mk g = Arrow.mk (f i)
⊢ ofHoms f g

Tactic:
← (ofHoms f).arrow_mk_mem_toSet_iff,

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_3
X Y : ι → C
f : (i : ι) → X i ⟶ Y i
A B : C
g : A ⟶ B
i : ι
h : Arrow.mk g = Arrow.mk (f i)
⊢ Arrow.mk g ∈ (ofHoms f).toSet
Module: Mathlib.CategoryTheory.Comma.Arrow

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
F G : C ⥤ D
h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), F.mapArrow.obj (mk f) = G.mapArrow.obj (mk f)
X Y : C
f : X ⟶ Y
⊢ F.map f = eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯

Tactic:
have := h f

Goal state after:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
F G : C ⥤ D
h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), F.mapArrow.obj (mk f) = G.mapArrow.obj (mk f)
X Y : C
f : X ⟶ Y
this : F.mapArrow.obj (mk f) = G.mapArrow.obj (mk f)
⊢ F.map f = eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.Adjunction.Basic

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
F G : C ⥤ D
H : D ⥤ C
adj : F ⊣ H
iso : F ≅ G
X : C
⊢ G.map ((adj.unit ≫ whiskerRight iso.hom H).app X) ≫ (H.whiskerLeft iso.inv ≫ adj.counit).app (G.obj X) = 𝟙 (G.obj X)

Tactic:
by
    simp only [Functor.id_obj, Functor.comp_obj, NatTrans.comp_app, Functor.whiskerRight_app,
      Functor.map_comp, Functor.whiskerLeft_app, Category.assoc, NatTrans.naturality_assoc]
    simp [← Functor.comp_map]

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Cᵒᵖ ⥤ Type v₁
Y : C
r : F.RepresentableBy Y
X X' : Cᵒᵖ
f : X ⟶ X'
⊢ (yoneda.obj Y).map f ≫ r.homEquiv.toIso.hom = r.homEquiv.toIso.hom ≫ F.map f

Tactic:
ext g
    dsimp
    apply r.homEquiv_comp

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : C ⥤ Type v₁
X✝ : C
r : F.CorepresentableBy X✝
X X' : C
f : X ⟶ X'
⊢ (coyoneda.obj (op X✝)).map f ≫ r.homEquiv.toIso.hom = r.homEquiv.toIso.hom ≫ F.map f

Tactic:
ext g
    dsimp
    apply r.homEquiv_comp

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F : Cᵒᵖ ⥤ Type v₁
η : yoneda.obj X ⟶ F
Y : Cᵒᵖ
f : (yoneda.obj X).obj Y
⊢ (ConcreteCategory.hom
          (((fun ξ ↦ { app := fun x ↦ ↾fun f ↦ (ConcreteCategory.hom (F.map (Quiver.Hom.op f))) ξ, naturality := ⋯ })
                ((fun η ↦ (ConcreteCategory.hom (η.app (op X))) (𝟙 X)) η)).app
            Y)).toFun
      f =
    (ConcreteCategory.hom (η.app Y)).toFun f

Tactic:
simp [← NatTrans.naturality_apply]

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : Cᵒᵖ
F : Cᵒᵖ ⥤ Type v₁
Y : Cᵒᵖ
G : Cᵒᵖ ⥤ Type v₁
f : (X, F) ⟶ (Y, G)
a : yoneda.obj (unop X) ⟶ F
⊢ (ConcreteCategory.hom (f.2.app Y)) ((ConcreteCategory.hom (a.app Y)) (𝟙 (unop Y) ≫ f.1.unop)) =
    (ConcreteCategory.hom (f.2.app Y))
      ((ConcreteCategory.hom (F.map f.1)) ((ConcreteCategory.hom (a.app X)) (𝟙 (unop X))))

Tactic:
simp [← NatTrans.naturality_apply]

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : SmallCategory C
F : Cᵒᵖ ⥤ Type u₁
X Y : Cᵒᵖ
f : X ⟶ Y
a : ((yoneda ⋙ (whiskeringLeft Cᵒᵖ (Cᵒᵖ ⥤ Type u₁)ᵒᵖ (Type u₁)).obj yoneda.op).obj F).obj X
⊢ (ConcreteCategory.hom (a.app Y)) (𝟙 (unop Y) ≫ f.unop) =
    (ConcreteCategory.hom (F.map f)) ((ConcreteCategory.hom (a.app X)) (𝟙 (unop X)))

Tactic:
simp [← NatTrans.naturality_apply]

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F : Cᵒᵖ ⥤ Type (max w v₁)
τ : uliftYoneda.{w, v₁, u₁}.obj X ⟶ F
Y : C
y : (yoneda.obj X).obj (op Y)
⊢ (ConcreteCategory.hom
          (((fun x ↦
                  { app := fun Y ↦ ↾fun y ↦ (ConcreteCategory.hom (F.map (Quiver.Hom.op y.down))) x, naturality := ⋯ })
                ((fun τ ↦ (ConcreteCategory.hom (τ.app (op X))) { down := 𝟙 (unop (op X)) }) τ)).app
            (op Y))).toFun
      { down := y } =
    (ConcreteCategory.hom (τ.app (op Y))).toFun { down := y }

Tactic:
simp [← NatTrans.naturality_apply]

Goal state after:
Module: Mathlib.CategoryTheory.Skeletal

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : Skeleton C
h : X ≅ Y
this : Quotient.out X ≈ Quotient.out Y
⊢ X = Y

Tactic:
simpa using! Quotient.sound this

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F : C ⥤ Type v₁
η : coyoneda.obj (op X) ⟶ F
Y : C
x : X ⟶ Y
⊢ (ConcreteCategory.hom
          (((fun ξ ↦ { app := fun x ↦ ↾fun x_1 ↦ (ConcreteCategory.hom (F.map x_1)) ξ, naturality := ⋯ })
                ((fun η ↦ (ConcreteCategory.hom (η.app X)) (𝟙 X)) η)).app
            Y)).toFun
      x =
    (ConcreteCategory.hom (η.app Y)).toFun x

Tactic:
simp [← NatTrans.naturality_apply]

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F : C ⥤ Type v₁
Y : C
G : C ⥤ Type v₁
f : (X, F) ⟶ (Y, G)
a : coyoneda.obj (op X) ⟶ F
⊢ (ConcreteCategory.hom (f.2.app Y)) ((ConcreteCategory.hom (a.app Y)) (f.1 ≫ 𝟙 Y)) =
    (ConcreteCategory.hom (f.2.app Y)) ((ConcreteCategory.hom (F.map f.1)) ((ConcreteCategory.hom (a.app X)) (𝟙 X)))

Tactic:
simp [← NatTrans.naturality_apply]

Goal state after:
Module: Mathlib.CategoryTheory.EssentiallySmall

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Quiver.IsThin C
⊢ EssentiallySmall.{w, v, u} C ↔ Small.{w, u} (Skeleton C)

Tactic:
simp [essentiallySmall_iff, CategoryTheory.locallySmall_of_thin]

Goal state after:
Module: Mathlib.CategoryTheory.EssentiallySmall

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Small.{w, u} C
inst✝ : LocallySmall.{w, v, u} C
φ : Arrow C → (s : C) × (t : C) × (s ⟶ t) := fun f ↦ ⟨f.left, ⟨f.right, f.hom⟩⟩
s t : C
f : (𝟭 C).obj s ⟶ (𝟭 C).obj t
t' : C
f' : (𝟭 C).obj s ⟶ (𝟭 C).obj t'
h :
  Arrow.right { left := s, right := t, hom := f } = Arrow.right { left := s, right := t', hom := f' } ∧
    Arrow.hom { left := s, right := t, hom := f } ≍ Arrow.hom { left := s, right := t', hom := f' }
⊢ { left := s, right := t, hom := f } = { left := s, right := t', hom := f' }

Tactic:
obtain rfl : t = t' := h.1

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Small.{w, u} C
inst✝ : LocallySmall.{w, v, u} C
φ : Arrow C → (s : C) × (t : C) × (s ⟶ t) := fun f ↦ ⟨f.left, ⟨f.right, f.hom⟩⟩
s t : C
f f' : (𝟭 C).obj s ⟶ (𝟭 C).obj t
h :
  Arrow.right { left := s, right := t, hom := f } = Arrow.right { left := s, right := t, hom := f' } ∧
    Arrow.hom { left := s, right := t, hom := f } ≍ Arrow.hom { left := s, right := t, hom := f' }
⊢ { left := s, right := t, hom := f } = { left := s, right := t, hom := f' }
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝² : Category.{v₁, u₁} C✝
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
hF : F.FullyFaithful
X : C
X✝ Y✝ : Cᵒᵖ
f : X✝ ⟶ Y✝
⊢ (F.op ⋙ uliftYoneda.{v₁, v₂, u₂}.obj (F.obj X)).map f ≫
      (Equiv.ulift.trans (hF.homEquiv.symm.trans Equiv.ulift.symm)).toIso.hom =
    (Equiv.ulift.trans (hF.homEquiv.symm.trans Equiv.ulift.symm)).toIso.hom ≫ (uliftYoneda.{v₂, v₁, u₁}.obj X).map f

Tactic:
ext; exact Equiv.ulift.injective (hF.map_injective (by simp))

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝² : Category.{v₁, u₁} C✝
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
hF : F.FullyFaithful
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ (F ⋙ uliftYoneda.{v₁, v₂, u₂} ⋙ (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max v₁ v₂))).obj F.op).map f ≫ (hF.homNatIso Y✝).hom =
    (hF.homNatIso X✝).hom ≫ uliftYoneda.{v₂, v₁, u₁}.map f

Tactic:
ext; exact Equiv.ulift.injective (hF.map_injective (by simp))

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝² : Category.{v₁, u₁} C✝
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
hF : F.FullyFaithful
X X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ (F ⋙ uliftCoyoneda.{v₁, v₂, u₂}.obj (op (F.obj X))).map f ≫
      (Equiv.ulift.trans (hF.homEquiv.symm.trans Equiv.ulift.symm)).toIso.hom =
    (Equiv.ulift.trans (hF.homEquiv.symm.trans Equiv.ulift.symm)).toIso.hom ≫
      (uliftCoyoneda.{v₂, v₁, u₁}.obj (op X)).map f

Tactic:
ext; exact Equiv.ulift.injective (hF.map_injective (by simp))

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝² : Category.{v₁, u₁} C✝
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
hF : F.FullyFaithful
X✝ Y✝ : Cᵒᵖ
f : X✝ ⟶ Y✝
⊢ (F.op ⋙ uliftCoyoneda.{v₁, v₂, u₂} ⋙ (whiskeringLeft C D (Type (max v₁ v₂))).obj F).map f ≫
      (hF.homNatIso' (unop Y✝)).hom =
    (hF.homNatIso' (unop X✝)).hom ≫ uliftCoyoneda.{v₂, v₁, u₁}.map f

Tactic:
ext; exact Equiv.ulift.injective (hF.map_injective (by simp))

Goal state after:
Module: Mathlib.CategoryTheory.Functor.EpiMono

Goal state before:
pp: case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
hF₁ : F.PreservesEpimorphisms
hF₂ : F.ReflectsEpimorphisms
⊢ Epi (F.map f) → Epi f

pp: case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
hF₁ : F.PreservesEpimorphisms
hF₂ : F.ReflectsEpimorphisms
⊢ Epi f → Epi (F.map f)

Tactic:
· exact F.epi_of_epi_map

Goal state after:
case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
hF₁ : F.PreservesEpimorphisms
hF₂ : F.ReflectsEpimorphisms
⊢ Epi f → Epi (F.map f)
Module: Mathlib.CategoryTheory.PUnit

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
h : ∀ (x y : C), Nonempty (Unique (x ⟶ y))
p : C
this : (x y : C) → Unique (x ⟶ y)
⊢ Nonempty (C ≌ Discrete PUnit.{w + 1})

Tactic:
refine
      Nonempty.intro
        (CategoryTheory.Equivalence.mk ((Functor.const _).obj ⟨⟨⟩⟩)
          ((@Functor.const <| Discrete PUnit).obj p) ?_ (by apply Functor.punitExt))

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
h : ∀ (x y : C), Nonempty (Unique (x ⟶ y))
p : C
this : (x y : C) → Unique (x ⟶ y)
⊢ 𝟭 C ≅ (Functor.const C).obj { as := PUnit.unit } ⋙ (Functor.const (Discrete PUnit.{w + 1})).obj p
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
t : PushoutCocone f g
W : C
k l : t.pt ⟶ W
h₀ : t.inl ≫ k = t.inl ≫ l
h₁ : t.inr ≫ k = t.inr ≫ l
⊢ t.ι.app none ≫ k = t.ι.app none ≫ l

Tactic:
rw [← t.w fst, Category.assoc, Category.assoc, h₀]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f✝ : X ⟶ Z
g : Y ⟶ Z
f : X ⟶ Y
inst✝ : Mono f
s : PullbackCone f f
m : s.pt ⟶ X
m₁ : m ≫ 𝟙 X = s.fst
x✝ : m ≫ 𝟙 X = s.snd
⊢ m = s.fst

Tactic:
simpa using m₁

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f✝ : X ⟶ Y
g : X ⟶ Z
f : X ⟶ Y
inst✝ : Epi f
s : PushoutCocone f f
m : Y ⟶ s.pt
m₁ : 𝟙 Y ≫ m = s.inl
x✝ : 𝟙 Y ≫ m = s.inr
⊢ m = s.inl

Tactic:
simpa using m₁

Goal state after:
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✝ : Cone K
x✝ : IsLimit c✝
⊢ IsLimit (G.mapCone c✝)

Tactic:
by
    rw [Functor.isZero_iff] at hG
    exact IsLimit.ofIsZero _ ((K ⋙ G).isZero (fun X ↦ hG _)) (hG _)

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)
⊢ (f ≫ section_ f) ≫ s.π = s.π

Tactic:
← s.condition,

Goal state after:
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)
⊢ 𝟙 X ≫ s.π = s.π
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:
comp_smul,

Goal state after:
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 : r • g ≫ f = g' ≫ (r • f)
⊢ g = g'
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 : r • g ≫ f = g' ≫ (r • f)
⊢ g = g'

Tactic:
comp_smul,

Goal state after:
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 : r • g ≫ f = r • g' ≫ f
⊢ g = g'
Module: Mathlib.CategoryTheory.Preadditive.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
P Q R : C
f✝ f' : P ⟶ Q
g g' : Q ⟶ R
X : C
f : End X
⊢ f * 0 = 0

Tactic:
by dsimp [mul]; exact HasZeroMorphisms.zero_comp _ f

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
s : Cofork f 0
j : WalkingParallelPair
⊢ s.ι.app j ≫ (Iso.refl s.pt).hom = (Cofork.ofπ s.π ⋯).ι.app j

Tactic:
by cases j <;> cat_disch

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
P : C
π π' : Y ⟶ P
w : f ≫ π = 0
h : π = π'
j : WalkingParallelPair
⊢ (CokernelCofork.ofπ π w).ι.app j ≫ (Iso.refl (CokernelCofork.ofπ π w).pt).hom = (CokernelCofork.ofπ π' ⋯).ι.app j

Tactic:
by cases j <;> cat_disch

Goal state after:
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 g : J → C
inst✝² : HasBiproduct f
inst✝¹ : HasBiproduct g
p : (j : J) → f j ⟶ g j
inst✝ : ∀ (j : J), Epi (p j)
⊢ Epi (map p)

Tactic:
have : biproduct.map p =
      (biproduct.isoCoproduct _).hom ≫ Sigma.map p ≫ (biproduct.isoCoproduct _).inv := by
    ext
    simp only [map_π, isoCoproduct_hom, isoCoproduct_inv, Category.assoc, ι_desc_assoc, ι_π_assoc]
    split
    · subst_vars
      simp
    · simp_all

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 g : J → C
inst✝² : HasBiproduct f
inst✝¹ : HasBiproduct g
p : (j : J) → f j ⟶ g j
inst✝ : ∀ (j : J), Epi (p j)
this : map p = (isoCoproduct f).hom ≫ Sigma.map p ≫ (isoCoproduct g).inv
⊢ Epi (map p)
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 : Cone (Discrete.functor f)
m : s.pt ⟶ b.toCone.pt
h : ∀ (j : Discrete J), m ≫ b.toCone.π.app j = s.π.app j
⊢ ∑ j, m ≫ b.π j ≫ b.ι j = ∑ j, s.π.app { as := j } ≫ b.ι j

Tactic:
apply Finset.sum_congr rfl

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 : Cone (Discrete.functor f)
m : s.pt ⟶ b.toCone.pt
h : ∀ (j : Discrete J), m ≫ b.toCone.π.app j = s.π.app j
⊢ ∀ x ∈ Finset.univ, m ≫ b.π x ≫ b.ι x = s.π.app { as := x } ≫ b.ι x
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:
apply Finset.sum_congr rfl

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
⊢ ∀ x ∈ Finset.univ, (b.π x ≫ b.ι x) ≫ m = b.π x ≫ s.ι.app { as := x }
Module: Mathlib.Algebra.Group.Pointwise.Finset.Scalar

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : DecidableEq β
inst✝ : SMul α β
s : Finset β
a : α
x : β
⊢ x ∈ a • s ↔ ∃ y ∈ s, a • y = x

Tactic:
simp only [Finset.smul_finset_def, mem_image]

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Partition.Basic

Goal state before:
pp: case h
n : ℕ
b : List ℕ
hb₁ : ∀ {i : ℕ}, i ∈ ⟦b⟧ → 0 < i
hb₂ : sum ⟦b⟧ = n
⊢ ∃ a, ofComposition n a = { parts := ⟦b⟧, parts_pos := hb₁, parts_sum := hb₂ }

Tactic:
exact ⟨⟨b, hb₁, by simpa using hb₂⟩, Partition.ext rfl⟩

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: n : ℕ
c : Composition n
n' : ℕ
c' : Composition n'
H : ⟨n, c⟩.snd.blocks = ⟨n', c'⟩.snd.blocks
⊢ ⟨n, c⟩ = ⟨n', c'⟩

Tactic:
have : n = n' := by rw [← c.blocks_sum, ← c'.blocks_sum, H]

Goal state after:
n : ℕ
c : Composition n
n' : ℕ
c' : Composition n'
H : ⟨n, c⟩.snd.blocks = ⟨n', c'⟩.snd.blocks
this : n = n'
⊢ ⟨n, c⟩ = ⟨n', c'⟩
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: case mpr
n : ℕ
hn : 0 < n
c : Composition n
i : Fin c.length
hi : n ≤ c.blocksFun i
⊢ c = single n hn

Tactic:
eq_single_iff_length

Goal state after:
case mpr
n : ℕ
hn : 0 < n
c : Composition n
i : Fin c.length
hi : n ≤ c.blocksFun i
⊢ c.length = 1
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: n✝¹ : ℕ
c✝¹ : Composition n✝¹
m : ℕ
motive : (n : ℕ) → Composition n → Sort u_1
n✝ : ℕ
c✝ : Composition n✝
zero : motive 0 (ones 0)
append_single : (k n : ℕ) → (c : Composition n) → motive n c → motive (n + (k + 1)) (c.append (single (k + 1) ⋯))
k n : ℕ
c : Composition n
ih : motive n c.reverse
⊢ motive (k + 1 + n) ((single (k + 1) ⋯).append c).reverse

Tactic:
convert! append_single k n c.reverse ih using 1

Goal state after:
case e'_1
n✝¹ : ℕ
c✝¹ : Composition n✝¹
m : ℕ
motive : (n : ℕ) → Composition n → Sort u_1
n✝ : ℕ
c✝ : Composition n✝
zero : motive 0 (ones 0)
append_single : (k n : ℕ) → (c : Composition n) → motive n c → motive (n + (k + 1)) (c.append (single (k + 1) ⋯))
k n : ℕ
c : Composition n
ih : motive n c.reverse
⊢ k + 1 + n = n + (k + 1)

case e'_2
n✝¹ : ℕ
c✝¹ : Composition n✝¹
m : ℕ
motive : (n : ℕ) → Composition n → Sort u_1
n✝ : ℕ
c✝ : Composition n✝
zero : motive 0 (ones 0)
append_single : (k n : ℕ) → (c : Composition n) → motive n c → motive (n + (k + 1)) (c.append (single (k + 1) ⋯))
k n : ℕ
c : Composition n
ih : motive n c.reverse
e_1✝ : k + 1 + n = n + (k + 1)
⊢ ((single (k + 1) ⋯).append c).reverse ≍ c.reverse.append (single (k + 1) ⋯)
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: n✝ n : ℕ
c : CompositionAsSet (n + 1)
j : Fin (n + 1)
i_mem : j.succ ∈ c.boundaries
i_ne_last : j.succ ≠ Fin.last (n + 1)
⊢ ∃ k, k.castSucc = j

Tactic:
simpa [Fin.exists_castSucc_eq] using! i_ne_last

Goal state after:
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : #f.support = 2
x y : α
hmem : ¬x = y
hins : {x, y} = f.support
ht : #{y} = 1
a : α
key : ∀ (b : α), f b ≠ b ↔ b = x ∨ b = y
⊢ f a = (swap x y) a

Tactic:
by_cases ha : f a = a

Goal state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : #f.support = 2
x y : α
hmem : ¬x = y
hins : {x, y} = f.support
ht : #{y} = 1
a : α
key : ∀ (b : α), f b ≠ b ↔ b = x ∨ b = y
ha : f a = a
⊢ f a = (swap x y) a

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : #f.support = 2
x y : α
hmem : ¬x = y
hins : {x, y} = f.support
ht : #{y} = 1
a : α
key : ∀ (b : α), f b ≠ b ↔ b = x ∨ b = y
ha : ¬f a = a
⊢ f a = (swap x y) a