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

Goal state before:
pp: case some.some.id
J : Type w
C : Type u
inst✝ : Category.{v, u} C
F : WidePullbackShape J ⥤ C
X : C
f : X ⟶ F.obj none
π : (j : J) → X ⟶ F.obj (some j)
w : ∀ (j : J), π j ≫ F.map (Hom.term j) = f
val✝ : J
⊢ (((Functor.const (WidePullbackShape J)).obj X).map (Hom.id (some val✝)) ≫
      match some val✝ with
      | none => f
      | some j => π j) =
    (match some val✝ with
      | none => f
      | some j => π j) ≫
      F.map (Hom.id (some val✝))

Tactic:
simp [w]

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

Goal state before:
pp: case id
J : Type w
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_1
F G : WidePullbackShape ι ⥤ C
base : F.obj none ≅ G.obj none
comp : (i : ι) → F.obj (some i) ≅ G.obj (some i)
w : ∀ (i : ι), F.map (Hom.term i) ≫ base.hom = (comp i).hom ≫ G.map (Hom.term i)
X✝ : WidePullbackShape ι
⊢ F.map (Hom.id X✝) ≫
      (match X✝ with
        | none => base
        | some i => comp i).hom =
    (match X✝ with
        | none => base
        | some i => comp i).hom ≫
      G.map (Hom.id X✝)

Tactic:
simp [w]

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

Goal state before:
pp: case term
J : Type w
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_1
F G : WidePullbackShape ι ⥤ C
base : F.obj none ≅ G.obj none
comp : (i : ι) → F.obj (some i) ≅ G.obj (some i)
w : ∀ (i : ι), F.map (Hom.term i) ≫ base.hom = (comp i).hom ≫ G.map (Hom.term i)
j✝ : ι
⊢ F.map (Hom.term j✝) ≫
      (match none with
        | none => base
        | some i => comp i).hom =
    (match some j✝ with
        | none => base
        | some i => comp i).hom ≫
      G.map (Hom.term j✝)

Tactic:
simp [w]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.HasLimits

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
t : Cone F
P : IsLimit t
s : Cocone F.op
m : t.op.pt ⟶ s.pt
w : ∀ (j : Jᵒᵖ), t.op.ι.app j ≫ m = s.ι.app j
⊢ m = (P.lift s.unop).op

Tactic:
← P.uniq s.unop m.unop

Goal state after:
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
t : Cone F
P : IsLimit t
s : Cocone F.op
m : t.op.pt ⟶ s.pt
w : ∀ (j : Jᵒᵖ), t.op.ι.app j ≫ m = s.ι.app j
⊢ m = m.unop.op

J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
t : Cone F
P : IsLimit t
s : Cocone F.op
m : t.op.pt ⟶ s.pt
w : ∀ (j : Jᵒᵖ), t.op.ι.app j ≫ m = s.ι.app j
⊢ ∀ (j : J), m.unop ≫ t.π.app j = s.unop.π.app j
Module: Mathlib.CategoryTheory.Limits.HasLimits

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
t : Cocone F
P : IsColimit t
s : Cone F.op
m : s.pt ⟶ t.op.pt
w : ∀ (j : Jᵒᵖ), m ≫ t.op.π.app j = s.π.app j
⊢ m = (P.desc s.unop).op

Tactic:
← P.uniq s.unop m.unop

Goal state after:
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
t : Cocone F
P : IsColimit t
s : Cone F.op
m : s.pt ⟶ t.op.pt
w : ∀ (j : Jᵒᵖ), m ≫ t.op.π.app j = s.π.app j
⊢ m = m.unop.op

J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
t : Cocone F
P : IsColimit t
s : Cone F.op
m : s.pt ⟶ t.op.pt
w : ∀ (j : Jᵒᵖ), m ≫ t.op.π.app j = s.π.app j
⊢ ∀ (j : J), t.ι.app j ≫ m.unop = s.unop.ι.app j
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: case none.none.id
J : Type w
C : Type u
inst✝ : Category.{v, u} C
F : WidePushoutShape J ⥤ C
X : C
f : F.obj none ⟶ X
ι : (j : J) → F.obj (some j) ⟶ X
w : ∀ (j : J), F.map (Hom.init j) ≫ ι j = f
⊢ (F.map (Hom.id none) ≫
      match none with
      | none => f
      | some j => ι j) =
    (match none with
      | none => f
      | some j => ι j) ≫
      ((Functor.const (WidePushoutShape J)).obj X).map (Hom.id none)

Tactic:
simp [w]

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

Goal state before:
pp: case none.some.init
J : Type w
C : Type u
inst✝ : Category.{v, u} C
F : WidePushoutShape J ⥤ C
X : C
f : F.obj none ⟶ X
ι : (j : J) → F.obj (some j) ⟶ X
w : ∀ (j : J), F.map (Hom.init j) ≫ ι j = f
val✝ : J
⊢ (F.map (Hom.init val✝) ≫
      match some val✝ with
      | none => f
      | some j => ι j) =
    (match none with
      | none => f
      | some j => ι j) ≫
      ((Functor.const (WidePushoutShape J)).obj X).map (Hom.init val✝)

Tactic:
simp [w]

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

Goal state before:
pp: case some.some.id
J : Type w
C : Type u
inst✝ : Category.{v, u} C
F : WidePushoutShape J ⥤ C
X : C
f : F.obj none ⟶ X
ι : (j : J) → F.obj (some j) ⟶ X
w : ∀ (j : J), F.map (Hom.init j) ≫ ι j = f
val✝ : J
⊢ (F.map (Hom.id (some val✝)) ≫
      match some val✝ with
      | none => f
      | some j => ι j) =
    (match some val✝ with
      | none => f
      | some j => ι j) ≫
      ((Functor.const (WidePushoutShape J)).obj X).map (Hom.id (some val✝))

Tactic:
simp [w]

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

Goal state before:
pp: β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝¹ : Category.{v, u} C
J : Type u_1
f : J → C
inst✝ : HasProduct f
j j' : J
w : j = j'
⊢ f j = f j'

Tactic:
simp [w]

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

Goal state before:
pp: β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝¹ : Category.{v, u} C
J : Type u_1
f : J → C
inst✝ : HasCoproduct f
j j' : J
w : j = j'
⊢ f j = f j'

Tactic:
simp [w]

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasTerminal C
P : C
f g : P ⟶ ⊤_ C
⊢ f = g

Tactic:
by ext ⟨⟨⟩⟩

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasInitial C
P : C
f g : ⊥_ C ⟶ P
⊢ f = g

Tactic:
by ext ⟨⟨⟩⟩

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasInitial C
P : C
⊢ desc (initial.to P) (𝟙 P) ≫ inr = 𝟙 ((⊥_ C) ⨿ P)

Tactic:
apply coprod.hom_ext

Goal state after:
case h₁
C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasInitial C
P : C
⊢ inl ≫ desc (initial.to P) (𝟙 P) ≫ inr = inl ≫ 𝟙 ((⊥_ C) ⨿ P)

case h₂
C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasInitial C
P : C
⊢ inr ≫ desc (initial.to P) (𝟙 P) ≫ inr = inr ≫ 𝟙 ((⊥_ C) ⨿ P)
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasInitial C
P : C
⊢ desc (𝟙 P) (initial.to P) ≫ inl = 𝟙 (P ⨿ ⊥_ C)

Tactic:
apply coprod.hom_ext

Goal state after:
case h₁
C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasInitial C
P : C
⊢ inl ≫ desc (𝟙 P) (initial.to P) ≫ inl = inl ≫ 𝟙 (P ⨿ ⊥_ C)

case h₂
C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasInitial C
P : C
⊢ inr ≫ desc (𝟙 P) (initial.to P) ≫ inl = inr ≫ 𝟙 (P ⨿ ⊥_ C)
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
S : D
T : C ⥤ D
f✝ : StructuredArrow S T
h : f✝.IsUniversal
g : StructuredArrow S T
f : f✝.right ⟶ g.right
w : (fun η ↦ f✝.hom ≫ T.map η = g.hom) f
⊢ f✝.hom ≫ T.map f = f✝.hom ≫ T.map (h.desc g)

Tactic:
simp [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 X)ᵒᵖ
f : Z ⟶ Y
⊢ (Under.Hom.right f.unop).op ≫ (unop Y).hom.op = (unop Z).hom.op

Tactic:
← Under.w f.unop,

Goal state after:
T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : T
Z Y : (Under X)ᵒᵖ
f : Z ⟶ Y
⊢ (Under.Hom.right f.unop).op ≫ (unop Y).hom.op = ((unop Y).hom ≫ Under.Hom.right f.unop).op
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
T : D
S : C ⥤ D
f✝ : CostructuredArrow S T
h : f✝.IsUniversal
g : CostructuredArrow S T
f : g.left ⟶ f✝.left
w : (fun η ↦ S.map η ≫ f✝.hom = g.hom) f
⊢ S.map f ≫ f✝.hom = S.map (h.lift g) ≫ f✝.hom

Tactic:
simp [w]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
F' : MonoFactorisation f
I✝ : C
Fm : I✝ ⟶ Y
m_mono✝ : Mono Fm
e✝ : X ⟶ I✝
Ffac : e✝ ≫ Fm = f
hI : { I := I✝, m := Fm, m_mono := m_mono✝, e := e✝, fac := Ffac }.I = F'.I
hm : { I := I✝, m := Fm, m_mono := m_mono✝, e := e✝, fac := Ffac }.m = eqToHom hI ≫ F'.m
⊢ { I := I✝, m := Fm, m_mono := m_mono✝, e := e✝, fac := Ffac } = F'

Tactic:
obtain ⟨_, Fm', _, Ffac'⟩ := F'

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
I✝¹ : C
Fm : I✝¹ ⟶ Y
m_mono✝¹ : Mono Fm
e✝¹ : X ⟶ I✝¹
Ffac : e✝¹ ≫ Fm = f
I✝ : C
Fm' : I✝ ⟶ Y
m_mono✝ : Mono Fm'
e✝ : X ⟶ I✝
Ffac' : e✝ ≫ Fm' = f
hI :
  { I := I✝¹, m := Fm, m_mono := m_mono✝¹, e := e✝¹, fac := Ffac }.I =
    { I := I✝, m := Fm', m_mono := m_mono✝, e := e✝, fac := Ffac' }.I
hm :
  { I := I✝¹, m := Fm, m_mono := m_mono✝¹, e := e✝¹, fac := Ffac }.m =
    eqToHom hI ≫ { I := I✝, m := Fm', m_mono := m_mono✝, e := e✝, fac := Ffac' }.m
⊢ { I := I✝¹, m := Fm, m_mono := m_mono✝¹, e := e✝¹, fac := Ffac } =
    { I := I✝, m := Fm', m_mono := m_mono✝, e := e✝, fac := Ffac' }
Module: Mathlib.CategoryTheory.Limits.Shapes.Images

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : HasImage f
F' : MonoFactorisation f
l : image f ⟶ F'.I
w : l ≫ F'.m = image.ι f
⊢ l ≫ F'.m = image.lift F' ≫ F'.m

Tactic:
simp [w]

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

Goal state before:
pp: case zero.zero.id
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
P : C
ι : P ⟶ X
w : ι ≫ f = ι ≫ g
⊢ ((Functor.const WalkingParallelPair).obj P).map (WalkingParallelPairHom.id zero) ≫
      WalkingParallelPair.casesOn (motive := fun t ↦
        zero = t → (((Functor.const WalkingParallelPair).obj P).obj zero ⟶ (parallelPair f g).obj zero)) zero
        (fun h ↦ ⋯ ▸ ι) (fun h ↦ ⋯ ▸ ι ≫ f) ⋯ =
    WalkingParallelPair.casesOn (motive := fun t ↦
        zero = t → (((Functor.const WalkingParallelPair).obj P).obj zero ⟶ (parallelPair f g).obj zero)) zero
        (fun h ↦ ⋯ ▸ ι) (fun h ↦ ⋯ ▸ ι ≫ f) ⋯ ≫
      (parallelPair f g).map (WalkingParallelPairHom.id zero)

Tactic:
simp [w]

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

Goal state before:
pp: case zero.one.left
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
P : C
ι : P ⟶ X
w : ι ≫ f = ι ≫ g
⊢ ((Functor.const WalkingParallelPair).obj P).map left ≫
      WalkingParallelPair.casesOn (motive := fun t ↦
        one = t → (((Functor.const WalkingParallelPair).obj P).obj one ⟶ (parallelPair f g).obj one)) one
        (fun h ↦ ⋯ ▸ ι) (fun h ↦ ⋯ ▸ ι ≫ f) ⋯ =
    WalkingParallelPair.casesOn (motive := fun t ↦
        zero = t → (((Functor.const WalkingParallelPair).obj P).obj zero ⟶ (parallelPair f g).obj zero)) zero
        (fun h ↦ ⋯ ▸ ι) (fun h ↦ ⋯ ▸ ι ≫ f) ⋯ ≫
      (parallelPair f g).map left

Tactic:
simp [w]

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

Goal state before:
pp: case zero.one.right
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
P : C
ι : P ⟶ X
w : ι ≫ f = ι ≫ g
⊢ ((Functor.const WalkingParallelPair).obj P).map right ≫
      WalkingParallelPair.casesOn (motive := fun t ↦
        one = t → (((Functor.const WalkingParallelPair).obj P).obj one ⟶ (parallelPair f g).obj one)) one
        (fun h ↦ ⋯ ▸ ι) (fun h ↦ ⋯ ▸ ι ≫ f) ⋯ =
    WalkingParallelPair.casesOn (motive := fun t ↦
        zero = t → (((Functor.const WalkingParallelPair).obj P).obj zero ⟶ (parallelPair f g).obj zero)) zero
        (fun h ↦ ⋯ ▸ ι) (fun h ↦ ⋯ ▸ ι ≫ f) ⋯ ≫
      (parallelPair f g).map right

Tactic:
simp [w]

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

Goal state before:
pp: case one.one.id
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
P : C
ι : P ⟶ X
w : ι ≫ f = ι ≫ g
⊢ ((Functor.const WalkingParallelPair).obj P).map (WalkingParallelPairHom.id one) ≫
      WalkingParallelPair.casesOn (motive := fun t ↦
        one = t → (((Functor.const WalkingParallelPair).obj P).obj one ⟶ (parallelPair f g).obj one)) one
        (fun h ↦ ⋯ ▸ ι) (fun h ↦ ⋯ ▸ ι ≫ f) ⋯ =
    WalkingParallelPair.casesOn (motive := fun t ↦
        one = t → (((Functor.const WalkingParallelPair).obj P).obj one ⟶ (parallelPair f g).obj one)) one
        (fun h ↦ ⋯ ▸ ι) (fun h ↦ ⋯ ▸ ι ≫ f) ⋯ ≫
      (parallelPair f g).map (WalkingParallelPairHom.id one)

Tactic:
simp [w]

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

Goal state before:
pp: case left
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
P : C
π : Y ⟶ P
w : f ≫ π = g ≫ π
⊢ (parallelPair f g).map left ≫ WalkingParallelPair.casesOn one (f ≫ π) π =
    WalkingParallelPair.casesOn zero (f ≫ π) π ≫ ((Functor.const WalkingParallelPair).obj P).map left

Tactic:
simp [w]

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

Goal state before:
pp: case right
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
P : C
π : Y ⟶ P
w : f ≫ π = g ≫ π
⊢ (parallelPair f g).map right ≫ WalkingParallelPair.casesOn one (f ≫ π) π =
    WalkingParallelPair.casesOn zero (f ≫ π) π ≫ ((Functor.const WalkingParallelPair).obj P).map right

Tactic:
simp [w]

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

Goal state before:
pp: case id
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
P : C
π : Y ⟶ P
w : f ≫ π = g ≫ π
i : WalkingParallelPair
⊢ (parallelPair f g).map (WalkingParallelPairHom.id i) ≫ WalkingParallelPair.casesOn i (f ≫ π) π =
    WalkingParallelPair.casesOn i (f ≫ π) π ≫
      ((Functor.const WalkingParallelPair).obj P).map (WalkingParallelPairHom.id i)

Tactic:
simp [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 : X ⟶ Y
t : Fork f g
⊢ t.ι ≫ f = t.ι ≫ g

Tactic:
by
  rw [← t.app_one_eq_ι_comp_left, ← t.app_one_eq_ι_comp_right]

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)
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
      apply Cofork.IsColimit.hom_ext i; rw [Cofork.π_ofπ] at hm; rw [hm]; exact l.2.symm

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:
smul_comp,

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✝¹ : Epi f
r : R
inst✝ : Invertible r
Z✝ : C
g g' : Y ⟶ Z✝
H : r • f ≫ g = (r • f) ≫ g'
⊢ 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✝¹ : Epi f
r : R
inst✝ : Invertible r
Z✝ : C
g g' : Y ⟶ Z✝
H : r • f ≫ g = (r • f) ≫ g'
⊢ g = g'

Tactic:
smul_comp,

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✝¹ : Epi f
r : R
inst✝ : Invertible r
Z✝ : C
g g' : Y ⟶ Z✝
H : r • f ≫ g = r • f ≫ g'
⊢ 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 Z : C
r : Rˣ
f : X ⟶ Y
g : Y ⟶ Z
⊢ (r • f) ≫ g = r • f ≫ g

Tactic:
apply Linear.smul_comp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X Y : C
f : X ⟶ Y
inst✝ : HasColimit (parallelPair f 0)
w : cokernel.π f = 0
R✝ : C
g : Y ⟶ R✝
h : f ≫ g = 0
⊢ g = 0

Tactic:
rw [← cokernel.π_desc f g h, w, Limits.zero_comp]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
f g : X ⟶ Y
P : C
ι : P ⟶ X
w : ι ≫ f = ι ≫ g
⊢ ι ≫ (f - g) = 0

Tactic:
simp [w]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
f g : X ⟶ Y
P : C
π : Y ⟶ P
w : f ≫ π = g ≫ π
⊢ (f - g) ≫ π = 0

Tactic:
simp [w]

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

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
X : C
⊢ ⊤.map P.ι X → P.isoClosure X

Tactic:
rintro ⟨⟨Y, hY⟩, _, ⟨e⟩⟩

Goal state after:
case mp
C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
X Y : C
hY : P Y
left✝ : ⊤ { obj := Y, property := hY }
e : P.ι.obj { obj := Y, property := hY } ≅ X
⊢ P.isoClosure X
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✝¹ : HasKernel f
X' Y' : C
f' : X' ⟶ Y'
inst✝ : HasKernel f'
p : X ≅ X'
q : Y ≅ Y'
w : f ≫ q.hom = p.hom ≫ f'
⊢ (f' ≫ q.inv) ≫ q.hom = (p.inv ≫ f) ≫ q.hom

Tactic:
simp [w]

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
c : CokernelCofork f
i : IsColimit c
W : C
g : W ⟶ X
hg : Epi g
h : W ⟶ Y
hh : h = g ≫ f
s : Cofork h 0
s' : CokernelCofork f := Cofork.ofπ s.π ⋯
l : { l // Cofork.π c ≫ l = Cofork.π s' } := CokernelCofork.IsColimit.desc' i (Cofork.π s') ⋯
m✝ : (CokernelCofork.ofπ (Cofork.π c) ⋯).pt ⟶ s.pt
hm : Cofork.π (CokernelCofork.ofπ (Cofork.π c) ⋯) ≫ m✝ = s.π
⊢ m✝ = ↑l

Tactic:
by
      apply Cofork.IsColimit.hom_ext i; rw [Cofork.π_ofπ] at hm; rw [hm]; exact l.2.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.hom = p.hom ≫ f'
⊢ (f' ≫ q.inv) ≫ q.hom = (p.inv ≫ f) ≫ q.hom

Tactic:
simp [w]

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 : J → C
inst✝ : HasBiproduct f
j j' : J
w : j = j'
⊢ f j = f j'

Tactic:
simp [w]

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

Goal state before:
pp: case one
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
Z : C
l : Y ⟶ Z
s : CokernelCofork f
hs : IsColimit s
i : s.pt ≅ Z
h : Cofork.π s ≫ i.hom = l
⊢ s.ι.app one ≫ i.hom = (CokernelCofork.ofπ l ⋯).ι.app one

Tactic:
· exact h

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

Goal state before:
pp: case neg.h
J : Type w
K : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
g : K → C
e : J ≃ K
w : (j : J) → g (e j) ≅ f j
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
j : J
k : K
h : ¬k = e j
⊢ k ≠ e j

pp: case neg.h
J : Type w
K : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
g : K → C
e : J ≃ K
w : (j : J) → g (e j) ≅ f j
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
j : J
k : K
h : ¬k = e j
⊢ e.symm k ≠ j

Tactic:
· exact h

Goal state after:
case neg.h
J : Type w
K : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
g : K → C
e : J ≃ K
w : (j : J) → g (e j) ≅ f j
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
j : J
k : K
h : ¬k = e j
⊢ e.symm k ≠ j
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
X✝ Y✝ : C
inst✝¹ : HasBinaryBiproduct X✝ Y✝
X Y : C
f : X ⟶ Y
inst✝ : IsSplitMono f
c : CokernelCofork f
i : IsColimit c
⊢ (isCokernelEpiComp i (retraction f) ⋯).desc (cokernelCoforkOfCofork (Cofork.ofπ (𝟙 Y - retraction f ≫ f) ⋯)) ≫
      retraction f =
    0

Tactic:
isCokernelEpiComp_desc

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
X✝ Y✝ : C
inst✝¹ : HasBinaryBiproduct X✝ Y✝
X Y : C
f : X ⟶ Y
inst✝ : IsSplitMono f
c : CokernelCofork f
i : IsColimit c
⊢ i.desc (Cofork.ofπ (Cofork.π (cokernelCoforkOfCofork (Cofork.ofπ (𝟙 Y - retraction f ≫ f) ⋯))) ⋯) ≫ retraction f = 0
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
X✝ Y✝ : C
inst✝¹ : HasBinaryBiproduct X✝ Y✝
X Y : C
f : X ⟶ Y
inst✝ : IsSplitMono f
c : CokernelCofork f
i : IsColimit c
⊢ retraction f ≫ (binaryBiconeOfIsSplitMonoOfCokernel i).inl +
      Cofork.π c ≫
        (isCokernelEpiComp i (retraction f) ⋯).desc (cokernelCoforkOfCofork (Cofork.ofπ (𝟙 Y - retraction f ≫ f) ⋯)) =
    𝟙 Y

Tactic:
isCokernelEpiComp_desc

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
X✝ Y✝ : C
inst✝¹ : HasBinaryBiproduct X✝ Y✝
X Y : C
f : X ⟶ Y
inst✝ : IsSplitMono f
c : CokernelCofork f
i : IsColimit c
⊢ retraction f ≫ (binaryBiconeOfIsSplitMonoOfCokernel i).inl +
      Cofork.π c ≫ i.desc (Cofork.ofπ (Cofork.π (cokernelCoforkOfCofork (Cofork.ofπ (𝟙 Y - retraction f ≫ f) ⋯))) ⋯) =
    𝟙 Y
Module: Mathlib.Algebra.Order.Antidiag.Finsupp

Goal state before:
pp: ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
n : μ
⊢ ∅.finsuppAntidiag n = if n = 0 then {0} else ∅

Tactic:
by split_ifs with hn <;> simp [*]

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.Pi

Goal state before:
pp: ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCancelCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
i : ι
s : Finset ι
hi : i ∉ s
n a c : μ
f : ι → μ
hab : (a, s.sum f) ∈ ↑(antidiagonal n)
g : ι → μ
hcd : (c, s.sum g) ∈ ↑(antidiagonal n)
hfg : ¬s.sum f = s.sum g
hgf : (g + fun j ↦ if j = i then c else 0) = f + fun j ↦ if j = i then a else 0
⊢ s.sum f = s.sum g

Tactic:
by simpa [sum_add_distrib, hi] using congr_arg (∑ j ∈ s, · j) hgf.symm

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.Pi

Goal state before:
pp: case mp
ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
n : ℕ
f : ι → ℕ
⊢ (∃ s_1, (∀ a ∈ s_1, a ∈ s) ∧ s_1.card = n ∧ ∀ (x : ι), Multiset.count x s_1 = f x) →
    s.sum f = n ∧ ∀ (i : ι), ¬f i = 0 → i ∈ s

Tactic:
rintro ⟨m, hm, rfl, hf⟩
    simpa [← hf, Multiset.sum_count_eq_card hm]

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

Goal state before:
pp: case refine_1
n✝ : ℕ
σ : Type u_1
τ : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : DecidableEq τ
n a : ℕ
ha1 : 1 ≤ a
ha : a ≤ n
p : { p // a ∈ p.parts }
⊢ ∀ {i : ℕ}, i ∈ (↑p).parts.erase a → 0 < i

Tactic:
intro _

Goal state after:
case refine_1
n✝ : ℕ
σ : Type u_1
τ : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : DecidableEq τ
n a : ℕ
ha1 : 1 ≤ a
ha : a ≤ n
p : { p // a ∈ p.parts }
i✝ : ℕ
⊢ i✝ ∈ (↑p).parts.erase a → 0 < i✝