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

Goal state before:
pp: I : Type w₀
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
x x' : (i : I) → C i
h : x = x'
i : I
⊢ eqToHom h i = eqToHom ⋯

Tactic:
subst h
  rfl

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
e : C ≌ D
W X X' Y : C
f : W ⟶ X
g : X ⟶ Y
f' : W ⟶ X'
g' : X' ⟶ Y
⊢ f ≫ g ≫ e.unit.app Y = f' ≫ g' ≫ e.unit.app Y ↔ f ≫ g = f' ≫ g'

Tactic:
simp only [← Category.assoc, cancel_mono]

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
e : C ≌ D
W X X' Y : D
f : W ⟶ X
g : X ⟶ Y
f' : W ⟶ X'
g' : X' ⟶ Y
⊢ f ≫ g ≫ e.counitInv.app Y = f' ≫ g' ≫ e.counitInv.app Y ↔ f ≫ g = f' ≫ g'

Tactic:
simp only [← Category.assoc, cancel_mono]

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
e : C ≌ D
W X X' Y Y' Z : C
f : W ⟶ X
g : X ⟶ Y
h : Y ⟶ Z
f' : W ⟶ X'
g' : X' ⟶ Y'
h' : Y' ⟶ Z
⊢ f ≫ g ≫ h ≫ e.unit.app Z = f' ≫ g' ≫ h' ≫ e.unit.app Z ↔ f ≫ g ≫ h = f' ≫ g' ≫ h'

Tactic:
simp only [← Category.assoc, cancel_mono]

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
e : C ≌ D
W X X' Y Y' Z : D
f : W ⟶ X
g : X ⟶ Y
h : Y ⟶ Z
f' : W ⟶ X'
g' : X' ⟶ Y'
h' : Y' ⟶ Z
⊢ f ≫ g ≫ h ≫ e.counitInv.app Z = f' ≫ g' ≫ h' ≫ e.counitInv.app Z ↔ f ≫ g ≫ h = f' ≫ g' ≫ h'

Tactic:
simp only [← Category.assoc, cancel_mono]

Goal state after:
Module: Mathlib.CategoryTheory.Category.ULift

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : AsSmall C
h : X = Y
⊢ (eqToHom h).down = eqToHom ⋯

Tactic:
subst h
  rfl

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
F : C ⥤ Type (max w v₁)
f : uliftCoyoneda.{w, v₁, u₁}.obj (op X) ⟶ F
g : X ⟶ Y
⊢ (ConcreteCategory.hom (F.map g)) (uliftCoyonedaEquiv f) = uliftCoyonedaEquiv (uliftCoyoneda.{w, v₁, u₁}.map g.op ≫ f)

Tactic:
simp [uliftCoyonedaEquiv, ← comp_apply, ← f.naturality]

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
A B X Y : Cᵒᵖ
i : A ⟶ B
p : X ⟶ Y
h : HasLiftingProperty i p
f : Opposite.unop Y ⟶ Opposite.unop B
g : Opposite.unop X ⟶ Opposite.unop A
sq : CommSq f p.unop i.unop g
⊢ sq.HasLift

Tactic:
rw [CommSq.HasLift.iff_op]
    simp only [Quiver.Hom.op_unop]
    infer_instance

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

Goal state before:
pp: J : Type u₁
inst✝³ : Category.{v₁, u₁} J
C : Type u
inst✝² : Category.{v, u} C
F G : J ⥤ C
inst✝¹ : HasLimit F
inst✝ : HasLimit G
c : Cone F
α : F ⟶ G
j✝ : J
⊢ lift F c ≫ π F j✝ ≫ α.app j✝ = lift G ((Cone.postcompose α).obj c) ≫ π G j✝

Tactic:
limit.lift_π_assoc,

Goal state after:
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
C : Type u
inst✝² : Category.{v, u} C
F G : J ⥤ C
inst✝¹ : HasLimit F
inst✝ : HasLimit G
c : Cone F
α : F ⟶ G
j✝ : J
⊢ c.π.app j✝ ≫ α.app j✝ = lift G ((Cone.postcompose α).obj c) ≫ π G 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
inst✝¹ : HasLimitsOfShape J C
G : J ⥤ C
α : F ⟶ G
inst✝ : HasLimitsOfShape K C
E : K ⥤ J
⊢ lim.map α ≫ pre G E = pre F E ≫ lim.map (E.whiskerLeft α)

Tactic:
by
  ext
  simp

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
inst✝¹ : HasColimit F
E : K ⥤ J
inst✝ : HasColimit (E ⋙ F)
c : Cocone F
⊢ pre F E ≫ desc F c = desc (E ⋙ F) (Cocone.whisker E c)

Tactic:
by
  ext
  simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : Type u_1
f : J → C
inst✝ : HasCoproduct f
j j' : J
w : j = j'
⊢ eqToHom ⋯ ≫ ι f j' = ι f j

Tactic:
cases w
  simp

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

Goal state before:
pp: J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → B ⟶ objs j
inst✝ : HasWidePushout B objs arrows
X : C
f : B ⟶ X
fs : (j : J) → objs j ⟶ X
w : ∀ (j : J), arrows j ≫ fs j = f
g : widePushout B objs arrows ⟶ X
⊢ (∀ (j : J), ι arrows j ≫ g = fs j) → head arrows ≫ g = f → g = desc f fs w

Tactic:
by
  intro h1 h2
  apply
    (colimit.isColimit (WidePushoutShape.wideSpan B objs arrows)).uniq
      (WidePushoutShape.mkCocone f fs <| w)
  rintro (_ | _)
  · apply h2
  · apply h1

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ X Y : C
c : BinaryFan X Y
x✝ : Discrete WalkingPair
l : WalkingPair
⊢ c.π.app { as := l } = (Iso.refl c.pt).hom ≫ (BinaryFan.mk c.fst c.snd).π.app { as := l }

Tactic:
cases l; repeat simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ X Y : C
c : BinaryCofan X Y
x✝ : Discrete WalkingPair
l : WalkingPair
⊢ c.ι.app { as := l } ≫ (Iso.refl c.pt).hom = (BinaryCofan.mk c.inl c.inr).ι.app { as := l }

Tactic:
cases l; repeat simp

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₂
inst✝² : Category.{v₂, u₂} J
F : J ⥤ C
inst✝¹ : HasColimit F
inst✝ : HasCoproduct F.obj
Z✝ : C
x✝¹ x✝ : colimit F ⟶ Z✝
h : Sigma.desc (colimit.ι F) ≫ x✝¹ = Sigma.desc (colimit.ι F) ≫ x✝
j : J
⊢ colimit.ι F j ≫ x✝¹ = colimit.ι F j ≫ x✝

Tactic:
simpa using Sigma.ι _ j ≫= h

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

Goal state before:
pp: C : Type u
inst✝¹¹ : Category.{v, u} C
X Y : C
D : Type u₂
inst✝¹⁰ : Category.{w, u₂} D
E : Type u₃
inst✝⁹ : Category.{w', u₃} E
F : C ⥤ D
G : D ⥤ E
A✝ A' B B' : C
inst✝⁸ : HasBinaryProduct A✝ B
inst✝⁷ : HasBinaryProduct A' B'
inst✝⁶ : HasBinaryProduct (F.obj A✝) (F.obj B)
inst✝⁵ : HasBinaryProduct (F.obj A') (F.obj B')
inst✝⁴ : HasBinaryProduct (G.obj (F.obj A✝)) (G.obj (F.obj B))
inst✝³ : HasBinaryProduct ((F ⋙ G).obj A✝) ((F ⋙ G).obj B)
inst✝² : HasBinaryProducts C
inst✝¹ : HasBinaryProducts D
A : C
inst✝ : ∀ (B : C), IsIso (prodComparison F A B)
⊢ IsIso { app := fun B ↦ prodComparison F A B, naturality := ⋯ }

Tactic:
apply NatIso.isIso_of_isIso_app

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

Goal state before:
pp: case left.right
C : Type u
inst✝ : Category.{v, u} C
X Y Z P✝ : C
sXY : BinaryFan X Y
sYZ : BinaryFan Y Z
P : IsLimit sXY
Q : IsLimit sYZ
s : BinaryFan sXY.pt Z
R : IsLimit s
t : Cone (pair X sYZ.pt)
m : t.pt ⟶ (BinaryFan.assoc Q s).pt
w : ∀ (j : Discrete WalkingPair), m ≫ (BinaryFan.assoc Q s).π.app j = t.π.app j
h :
  (∀ (j : Discrete WalkingPair), m ≫ s.π.app j = (BinaryFan.assocInv P t).π.app j) → m = R.lift (BinaryFan.assocInv P t)
⊢ (m ≫ s.π.app { as := WalkingPair.left }) ≫ sXY.π.app { as := WalkingPair.right } =
    (BinaryFan.assocInv P t).π.app { as := WalkingPair.left } ≫ sXY.π.app { as := WalkingPair.right }

Tactic:
replace w : m ≫ BinaryFan.IsLimit.lift Q (s.fst ≫ sXY.snd) s.snd = t.π.app ⟨.right⟩ := by
          simpa using! w ⟨.right⟩

Goal state after:
case left.right
C : Type u
inst✝ : Category.{v, u} C
X Y Z P✝ : C
sXY : BinaryFan X Y
sYZ : BinaryFan Y Z
P : IsLimit sXY
Q : IsLimit sYZ
s : BinaryFan sXY.pt Z
R : IsLimit s
t : Cone (pair X sYZ.pt)
m : t.pt ⟶ (BinaryFan.assoc Q s).pt
h :
  (∀ (j : Discrete WalkingPair), m ≫ s.π.app j = (BinaryFan.assocInv P t).π.app j) → m = R.lift (BinaryFan.assocInv P t)
w : m ≫ BinaryFan.IsLimit.lift Q (s.fst ≫ sXY.snd) s.snd = t.π.app { as := WalkingPair.right }
⊢ (m ≫ s.π.app { as := WalkingPair.left }) ≫ sXY.π.app { as := WalkingPair.right } =
    (BinaryFan.assocInv P t).π.app { as := WalkingPair.left } ≫ sXY.π.app { as := WalkingPair.right }
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:
by rw [← t.w fst, Category.assoc, Category.assoc, h₀]

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

Goal state before:
pp: T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
U V W : Over X
f : U.left ⟶ V.left
g : V.left ⟶ W.left
w_f : f ≫ V.hom = U.hom
w_g : g ≫ W.hom = V.hom
⊢ homMk (f ≫ g) ⋯ = homMk f w_f ≫ homMk g w_g

Tactic:
by
  ext
  simp

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

Goal state before:
pp: T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
f g : Over X
h : f = g
⊢ Hom.left (eqToHom h) = eqToHom ⋯

Tactic:
subst h
  rfl

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

Goal state before:
pp: T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
f g : Under X
h : f = g
⊢ Hom.right (eqToHom h) = eqToHom ⋯

Tactic:
subst h
  rfl

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
F : C ⥤ D
d : D
X : C
x : d ⟶ F.obj X
Y : C
y : d ⟶ F.obj Y
f : op (StructuredArrow.mk x) ⟶ op (StructuredArrow.mk y)
⊢ ((𝟭 (StructuredArrow d F)ᵒᵖ).map f ≫
        (StructuredArrow.isoMk (Iso.refl (unop (op (StructuredArrow.mk y))).right) ⋯).op.hom).unop =
    ((StructuredArrow.isoMk (Iso.refl (unop (op (StructuredArrow.mk x))).right) ⋯).op.hom ≫
        (StructuredArrow.toCostructuredArrow F d ⋙ (CostructuredArrow.toStructuredArrow' F d).rightOp).map f).unop

Tactic:
ext; apply Quiver.Hom.op_inj (by simp)

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
F : C ⥤ D
d : D
X : C
x : F.obj X ⟶ d
Y : C
y : F.obj Y ⟶ d
f : op (CostructuredArrow.mk x) ⟶ op (CostructuredArrow.mk y)
⊢ ((𝟭 (CostructuredArrow F d)ᵒᵖ).map f ≫
        (CostructuredArrow.isoMk (Iso.refl (unop (op (CostructuredArrow.mk y))).left) ⋯).op.hom).unop =
    ((CostructuredArrow.isoMk (Iso.refl (unop (op (CostructuredArrow.mk x))).left) ⋯).op.hom ≫
        (CostructuredArrow.toStructuredArrow F d ⋙ (StructuredArrow.toCostructuredArrow' F d).rightOp).map f).unop

Tactic:
ext; apply Quiver.Hom.op_inj (by simp)

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
inst✝¹ : HasInitial C
inst✝ : PreservesColimit (Functor.empty C) G
F : Discrete PEmpty.{1} ⥤ D
⊢ HasColimit F

Tactic:
by
    have := HasColimit.mk ⟨_, isColimitOfHasInitialOfPreservesColimit G⟩
    apply hasColimit_of_iso F.uniqueFromEmpty

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✝ f g : X ⟶ Y
Z : C
h✝ : Z ⟶ X
s : Fork f g
hs : IsLimit s
c : PullbackCone s.ι h✝
hc : IsLimit c
s' : Fork (h✝ ≫ f) (h✝ ≫ g)
m : s'.pt ⟶ (precompFork h✝ s c).pt
h : m ≫ (precompFork h✝ s c).ι = s'.ι
⊢ ∀ (j : WalkingCospan), m ≫ c.π.app j = liftPrecomp h✝ hs hc s' ≫ c.π.app j

Tactic:
apply PullbackCone.equalizer_ext
      · simp only [liftPrecomp, IsLimit.fac, PullbackCone.mk_π_app]
        apply hs.hom_ext
        apply Fork.equalizer_ext
        simp only [Fork.ι_ofι, precompFork] at h
        simp [c.condition, reassoc_of% h]
      · simpa [liftPrecomp] using! h

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✝² : HasZeroMorphisms C
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : F.PreservesZeroMorphisms
X : C
hX : IsZero X
⊢ IsZero (F.obj X)

Tactic:
simp only [IsZero.iff_id_eq_zero] at hX ⊢
  rw [← F.map_id, hX, F.map_zero]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
β : Type w
inst✝¹ : DecidableEq β
f : β → C
inst✝ : HasProduct f
b : β
⊢ ι f b ≫ π f b = 𝟙 (f b)

Tactic:
simp [Pi.ι]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J✝ : Type v
inst✝ : HasFiniteColimits C
J : Type
x✝ : Finite J
⊢ HasColimitsOfShape (WidePushoutShape J) C

Tactic:
by cases nonempty_fintype J; exact HasFiniteColimits.out _

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
⊢ ¬P = ⊥ ↔ ∃ X, P X

Tactic:
simp [← le_bot_iff, not_le_iff_exists]

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
h : ∀ (J : Type w) {𝒥 : SmallCategory J} (x : FinCategory J), PreservesColimitsOfShape J F
J : Type
x✝¹ : SmallCategory J
x✝ : FinCategory J
this✝ : Category.{?u.57, ?u.55} (ULiftHom (ULift.{?u.55, 0} J)) := ULiftHom.category
this : PreservesColimitsOfShape (ULiftHom (ULift.{w, 0} J)) F
⊢ PreservesColimitsOfShape J F

Tactic:
exact preservesColimitsOfShape_of_equiv (ULiftHomULiftCategory.equiv J).symm F

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

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

Tactic:
rintro ⟨Y, hY, ⟨e⟩⟩
    exact ⟨⟨Y, hY⟩, by simp, ⟨e.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✝ : HasZeroObject C
X Y : C
f : X ⟶ Y
hf : ∀ (Z : C) (g : Y ⟶ Z), f ≫ g = 0 → g = 0
s : Cofork f 0
⊢ Cofork.π (CokernelCofork.ofπ 0 ⋯) ≫ 0 = s.π

Tactic:
hf _ _ (CokernelCofork.condition s),

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
inst✝ : HasZeroObject C
X Y : C
f : X ⟶ Y
hf : ∀ (Z : C) (g : Y ⟶ Z), f ≫ g = 0 → g = 0
s : Cofork f 0
⊢ Cofork.π (CokernelCofork.ofπ 0 ⋯) ≫ 0 = 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
K : Type w'
f : J → C
c : Bicone f
g : K ≃ J
⊢ (c.whisker g).IsBilimit ≃ c.IsBilimit

Tactic:
refine equivOfSubsingletonOfSubsingleton (fun hc => ⟨?_, ?_⟩) fun hc => ⟨?_, ?_⟩
  · let := IsLimit.ofIsoLimit hc.isLimit (Bicone.whiskerToCone c g)
    let := (IsLimit.postcomposeHomEquiv (Discrete.functorComp f g).symm _) this
    exact IsLimit.ofWhiskerEquivalence (Discrete.equivalence g) this
  · let := IsColimit.ofIsoColimit hc.isColimit (Bicone.whiskerToCocone c g)
    let := (IsColimit.precomposeHomEquiv (Discrete.functorComp f g) _) this
    exact IsColimit.ofWhiskerEquivalence (Discrete.equivalence g) this
  · apply IsLimit.ofIsoLimit _ (Bicone.whiskerToCone c g).symm
    apply (IsLimit.postcomposeHomEquiv (Discrete.functorComp f g).symm _).symm _
    exact IsLimit.whiskerEquivalence hc.isLimit (Discrete.equivalence g)
  · apply IsColimit.ofIsoColimit _ (Bicone.whiskerToCocone c g).symm
    apply (IsColimit.precomposeHomEquiv (Discrete.functorComp f g) _).symm _
    exact IsColimit.whiskerEquivalence hc.isColimit (Discrete.equivalence g)

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

Goal state before:
pp: J : Type w
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
f : J → C
inst✝ : HasBiproduct f
j j' : J
w : j = j'
⊢ eqToHom ⋯ ≫ ι f j' = ι f j

Tactic:
cases w
  simp

Goal state after:
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
⊢ ∀ x ∈ Finset.univ, m ≫ b.π x ≫ b.ι x = s.π.app { as := x } ≫ b.ι x

Tactic:
intro j _

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
j : J
a✝ : j ∈ Finset.univ
⊢ m ≫ b.π j ≫ b.ι j = s.π.app { as := j } ≫ b.ι j
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
⊢ ∀ x ∈ Finset.univ, (b.π x ≫ b.ι x) ≫ m = b.π x ≫ s.ι.app { as := x }

Tactic:
intro j _

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 : J
a✝ : j ∈ Finset.univ
⊢ (b.π j ≫ b.ι j) ≫ m = b.π j ≫ s.ι.app { as := 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 P' Q Q' X Y : C
b : BinaryBicone X Y
j j' : WalkingPair
⊢ WalkingPair.casesOn j b.inl b.inr ≫ WalkingPair.casesOn j' b.fst b.snd = if h : j = j' then eqToHom ⋯ else 0

Tactic:
by
        rcases j with ⟨⟩ <;> rcases j' with ⟨⟩ <;> simp

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
J K : Type
inst✝² : Finite J
inst✝¹ : HasFiniteBiproducts C
inst✝ : Finite K
f : J → C
g h : K → C
m : (j : J) → (k : K) → f j ⟶ g k
n : (k : K) → g k ⟶ h k
⊢ matrix m ≫ map n = matrix fun j k ↦ m j k ≫ n k

Tactic:
by
  ext
  simp

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
J K : Type
inst✝² : Finite J
inst✝¹ : HasFiniteBiproducts C
inst✝ : Finite K
f g : J → C
h : K → C
m : (k : J) → f k ⟶ g k
n : (j : J) → (k : K) → g j ⟶ h k
⊢ map m ≫ matrix n = matrix fun j k ↦ m j ≫ n j k

Tactic:
by
  ext
  simp

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

Goal state before:
pp: case h₁.h₀
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
⊢ inl ≫ (isoProd X Y).hom ≫ prod.fst = inl ≫ prod.lift fst snd ≫ prod.fst

Tactic:
simp [biprod.isoProd]

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

Goal state before:
pp: case h₁
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
⊢ inr ≫ (isoProd X Y).hom ≫ prod.fst = inr ≫ prod.lift fst snd ≫ prod.fst

Tactic:
simp [biprod.isoProd]

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

Goal state before:
pp: case h₂.h₀
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
⊢ inl ≫ (isoProd X Y).hom ≫ prod.snd = inl ≫ prod.lift fst snd ≫ prod.snd

Tactic:
simp [biprod.isoProd]

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

Goal state before:
pp: case h₁
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
⊢ inr ≫ (isoProd X Y).hom ≫ prod.snd = inr ≫ prod.lift fst snd ≫ prod.snd

Tactic:
simp [biprod.isoProd]

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

Goal state before:
pp: J : Type
inst✝⁴ : Finite J
K : Type
inst✝³ : Finite K
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasFiniteBiproducts C
f : J → C
g : K → C
m : (j : J) → (k : K) → f j ⟶ g k
k : K
j✝ : J
⊢ ι f j✝ ≫ matrix m ≫ π g k = ι f j✝ ≫ desc fun j ↦ m j k

Tactic:
simp [biproduct.matrix]

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

Goal state before:
pp: J : Type
inst✝⁴ : Finite J
K : Type
inst✝³ : Finite K
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasFiniteBiproducts C
f : J → C
g : K → C
m : (j : J) → (k : K) → f j ⟶ g k
j : J
⊢ ι f j ≫ matrix m = lift fun k ↦ m j k

Tactic:
simp [biproduct.matrix]

Goal state after:
Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal

Goal state before:
pp: n : ℕ
| [![n]]

Tactic:
← List.nil_append [![n]]

Goal state after:
n : ℕ
| [] ++ [![n]]
Module: Mathlib.Combinatorics.Enumerative.Partition.Basic

Goal state before:
pp: n : ℕ
σ : Type u_1
s : Sym σ n
inst✝ : DecidableEq σ
⊢ (↑s).card = n

Tactic:
exact s.2

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

Goal state before:
pp: n : ℕ
c : Composition n
i : ℕ
h : c.length ≤ i
⊢ take i c.blocks = c.blocks

Tactic:
exact take_of_length_le h

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

Goal state before:
pp: c c' : (n : ℕ) × Composition n
H : c = c'
⊢ c.snd.blocks = c'.snd.blocks

Tactic:
rw [H]

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

Goal state before:
pp: case mp
n : ℕ
c : Composition n
⊢ c = ones n → ∀ i ∈ c.blocks, i = 1

pp: case mpr
n : ℕ
c : Composition n
⊢ (∀ i ∈ c.blocks, i = 1) → c = ones n

Tactic:
· rintro rfl
    exact fun i => eq_of_mem_replicate

Goal state after:
case mpr
n : ℕ
c : Composition n
⊢ (∀ i ∈ c.blocks, i = 1) → c = ones n
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
⊢ ↑f.support = {x | f x ≠ x}

Tactic:
by
  ext
  simp

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

Goal state before:
pp: n : ℕ
h : 0 < n
i : Fin n
⊢ ((single n h).embedding 0) i = i

Tactic:
by
  ext
  simp

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

Goal state before:
pp: case mp
n : ℕ
h : 0 < n
c : Composition n
H : c = single n h
⊢ c.length = 1

Tactic:
rw [H]

Goal state after:
case mp
n : ℕ
h : 0 < n
c : Composition n
H : c = single n h
⊢ (single n h).length = 1
Module: Mathlib.Logic.Equiv.Fintype

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
f : α ↪ β
⊢ f.toEquivRange = Equiv.ofInjective ⇑f ⋯

Tactic:
by
  ext
  simp

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

Goal state before:
pp: case a.inl
α : Type u_1
inst✝ : DecidableEq α
l : List α
h' : ∀ (x : α), l ≠ [x]
n : ℕ
hn : n < l.length
hx : l[n] ∈ l
H : l[(n + 1) % l.length] = l[n]
hn' : n.succ = l.length
h : ⟨0, ⋯⟩ = ⟨n, hn⟩
⊢ ∃ x, l = [x]

Tactic:
rw [← length_eq_one_iff, ← hn', (Fin.mk.inj_iff.mp h).symm]

Goal state after:
Module: Mathlib.Data.Int.Order.Units

Goal state before:
pp: u : ℤˣ
⊢ u⁻¹ = u

Tactic:
rw [inv_eq_iff_mul_eq_one, units_mul_self]

Goal state after:
Module: Mathlib.Data.Int.Order.Units

Goal state before:
pp: u : ℤˣ
n : ℕ
| u ^ n

Tactic:
rw [← Nat.mod_add_div n 2]

Goal state after:
u : ℤˣ
n : ℕ
| u ^ (n % 2 + 2 * (n / 2))
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: case inl.inl
α : Type u
inst✝ : DecidableEq α
β : Type v
i j : α
σ τ υ : Perm α
hστ : σ = τ
hτυ : τ = υ
⊢ τ = υ ∨ τ = swap i j * υ

Tactic:
hτυ,

Goal state after:
case inl.inl
α : Type u
inst✝ : DecidableEq α
β : Type v
i j : α
σ τ υ : Perm α
hστ : σ = τ
hτυ : τ = υ
⊢ υ = υ ∨ υ = swap i j * υ