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

Goal state before:
pp: A : Type u₁
inst✝⁵ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁴ : Category.{v₂, u₂} B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
A' : Type u₄
inst✝² : Category.{v₄, u₄} A'
B' : Type u₅
inst✝¹ : Category.{v₅, u₅} B'
T' : Type u₆
inst✝ : Category.{v₆, u₆} T'
L : A ⥤ T
R : B ⥤ T
L₁ L₂ L₃ : A ⥤ T
R₁ R₂ R₃ : B ⥤ T
X Y : Comma L₁ R₁
l : X.left ≅ Y.left
r : X.right ≅ Y.right
h : L₁.map l.hom ≫ Y.hom = X.hom ≫ R₁.map r.hom
⊢ X.hom = (L₁.mapIso l).hom ≫ Y.hom ≫ R₁.map r.inv

Tactic:
L₁.mapIso_hom,

Goal state after:
A : Type u₁
inst✝⁵ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁴ : Category.{v₂, u₂} B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
A' : Type u₄
inst✝² : Category.{v₄, u₄} A'
B' : Type u₅
inst✝¹ : Category.{v₅, u₅} B'
T' : Type u₆
inst✝ : Category.{v₆, u₆} T'
L : A ⥤ T
R : B ⥤ T
L₁ L₂ L₃ : A ⥤ T
R₁ R₂ R₃ : B ⥤ T
X Y : Comma L₁ R₁
l : X.left ≅ Y.left
r : X.right ≅ Y.right
h : L₁.map l.hom ≫ Y.hom = X.hom ≫ R₁.map r.hom
⊢ X.hom = L₁.map l.hom ≫ Y.hom ≫ R₁.map r.inv
Module: Mathlib.CategoryTheory.Endomorphism

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X✝ X Y : C
h : X ≅ Y
⊢ ∀ (x y : Aut X),
    { hom := h.inv ≫ (x * y).hom ≫ h.hom, inv := h.inv ≫ (x * y).inv ≫ h.hom, hom_inv_id := ⋯, inv_hom_id := ⋯ } =
      { hom := h.inv ≫ x.hom ≫ h.hom, inv := h.inv ≫ x.inv ≫ h.hom, hom_inv_id := ⋯, inv_hom_id := ⋯ } *
        { hom := h.inv ≫ y.hom ≫ h.hom, inv := h.inv ≫ y.inv ≫ h.hom, hom_inv_id := ⋯, inv_hom_id := ⋯ }

Tactic:
simp [Aut_mul_def]

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

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
h : IsLimit t
W : C
π : (const J).obj W ⟶ F
j✝ j'✝ : J
f : j✝ ⟶ j'✝
⊢ (fun j ↦ π.app j) j✝ ≫ F.map f = (fun j ↦ π.app j) j'✝

Tactic:
convert! ← (π.naturality f).symm; apply id_comp

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

Goal state before:
pp: J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
X : C
h : F.cocones.CorepresentableBy X
Y : C
f : X ⟶ Y
⊢ coconeOfHom h f = (colimitCocone h).extend f

Tactic:
dsimp [coconeOfHom, colimitCocone, Cocone.extend]

Goal state after:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
X : C
h : F.cocones.CorepresentableBy X
Y : C
f : X ⟶ Y
⊢ { pt := Y, ι := h.homEquiv f } = { pt := Y, ι := h.homEquiv (𝟙 X) ≫ (const J).map f }
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : SmallCategory C
⊢ ∀ {X Y : C} (f : X ⟶ Y),
    (coyoneda.rightOp ⋙ coyoneda).map f ≫ (NatIso.ofComponents (fun x ↦ coyonedaEquiv.toIso) ⋯).hom =
      (NatIso.ofComponents (fun x ↦ coyonedaEquiv.toIso) ⋯).hom ≫ (evaluation C (Type u₁)).map f

Tactic:
by
    intro X Y f
    ext a b
    simp [coyonedaEquiv, ← NatTrans.naturality_apply]

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:
by
  simp [uliftCoyonedaEquiv, ← comp_apply, ← f.naturality]

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
hX : IsInitial X
hY : IsInitial Y
f : X ⟶ Y
⊢ IsIso f

Tactic:
by
  refine ⟨⟨IsInitial.to hY X, ?_⟩⟩
  simp only [IsInitial.to_comp, IsInitial.to_self, and_true]
  apply IsInitial.hom_ext hX

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)
k : K
⊢ ι (E ⋙ F) k ≫ pre F E = ι F (E.obj k)

Tactic:
simp [colimit.pre]

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u₂
inst✝⁴ : Category.{w, u₂} D
F : C ⥤ D
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')
f : A ⟶ A'
g : B ⟶ B'
⊢ prod.lift (F.map (prod.map f g) ≫ F.map prod.fst) (F.map (prod.map f g) ≫ F.map prod.snd) =
    prod.lift (F.map (prod.fst ≫ f)) (F.map (prod.snd ≫ g))

Tactic:
←
    F.map_comp,

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u₂
inst✝⁴ : Category.{w, u₂} D
F : C ⥤ D
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')
f : A ⟶ A'
g : B ⟶ B'
⊢ prod.lift (F.map (prod.map f g ≫ prod.fst)) (F.map (prod.map f g) ≫ F.map prod.snd) =
    prod.lift (F.map (prod.fst ≫ f)) (F.map (prod.snd ≫ g))
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan

Goal state before:
pp: case none
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y Z X' Y' Z' : C
iX : X ≅ X'
iY : Y ≅ Y'
iZ : Z ≅ Z'
F G : WalkingCospan ⥤ C
z : F.obj WalkingCospan.one ⟶ G.obj WalkingCospan.one
l : F.obj WalkingCospan.left ⟶ G.obj WalkingCospan.left
r : F.obj WalkingCospan.right ⟶ G.obj WalkingCospan.right
hl : F.map inl ≫ z = l ≫ G.map inl
hr : F.map inr ≫ z = r ≫ G.map inr
⊢ F.obj none ⟶ G.obj none

pp: case some.left
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y Z X' Y' Z' : C
iX : X ≅ X'
iY : Y ≅ Y'
iZ : Z ≅ Z'
F G : WalkingCospan ⥤ C
z : F.obj WalkingCospan.one ⟶ G.obj WalkingCospan.one
l : F.obj WalkingCospan.left ⟶ G.obj WalkingCospan.left
r : F.obj WalkingCospan.right ⟶ G.obj WalkingCospan.right
hl : F.map inl ≫ z = l ≫ G.map inl
hr : F.map inr ≫ z = r ≫ G.map inr
⊢ F.obj (some WalkingPair.left) ⟶ G.obj (some WalkingPair.left)

pp: case some.right
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y Z X' Y' Z' : C
iX : X ≅ X'
iY : Y ≅ Y'
iZ : Z ≅ Z'
F G : WalkingCospan ⥤ C
z : F.obj WalkingCospan.one ⟶ G.obj WalkingCospan.one
l : F.obj WalkingCospan.left ⟶ G.obj WalkingCospan.left
r : F.obj WalkingCospan.right ⟶ G.obj WalkingCospan.right
hl : F.map inl ≫ z = l ≫ G.map inl
hr : F.map inr ≫ z = r ≫ G.map inr
⊢ F.obj (some WalkingPair.right) ⟶ G.obj (some WalkingPair.right)

Tactic:
exacts [z, l, r]

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

Goal state before:
pp: case none
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y Z X' Y' Z' : C
iX : X ≅ X'
iY : Y ≅ Y'
iZ : Z ≅ Z'
F G : WalkingCospan ⥤ C
z : F.obj WalkingCospan.one ≅ G.obj WalkingCospan.one
l : F.obj WalkingCospan.left ≅ G.obj WalkingCospan.left
r : F.obj WalkingCospan.right ≅ G.obj WalkingCospan.right
hl : F.map inl ≫ z.hom = l.hom ≫ G.map inl
hr : F.map inr ≫ z.hom = r.hom ≫ G.map inr
⊢ F.obj none ≅ G.obj none

pp: case some.left
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y Z X' Y' Z' : C
iX : X ≅ X'
iY : Y ≅ Y'
iZ : Z ≅ Z'
F G : WalkingCospan ⥤ C
z : F.obj WalkingCospan.one ≅ G.obj WalkingCospan.one
l : F.obj WalkingCospan.left ≅ G.obj WalkingCospan.left
r : F.obj WalkingCospan.right ≅ G.obj WalkingCospan.right
hl : F.map inl ≫ z.hom = l.hom ≫ G.map inl
hr : F.map inr ≫ z.hom = r.hom ≫ G.map inr
⊢ F.obj (some WalkingPair.left) ≅ G.obj (some WalkingPair.left)

pp: case some.right
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y Z X' Y' Z' : C
iX : X ≅ X'
iY : Y ≅ Y'
iZ : Z ≅ Z'
F G : WalkingCospan ⥤ C
z : F.obj WalkingCospan.one ≅ G.obj WalkingCospan.one
l : F.obj WalkingCospan.left ≅ G.obj WalkingCospan.left
r : F.obj WalkingCospan.right ≅ G.obj WalkingCospan.right
hl : F.map inl ≫ z.hom = l.hom ≫ G.map inl
hr : F.map inr ≫ z.hom = r.hom ≫ G.map inr
⊢ F.obj (some WalkingPair.right) ≅ G.obj (some WalkingPair.right)

Tactic:
exacts [z, l, r]

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

Goal state before:
pp: case none
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y Z X' Y' Z' : C
iX : X ≅ X'
iY : Y ≅ Y'
iZ : Z ≅ Z'
F G : WalkingSpan ⥤ C
z : F.obj WalkingSpan.zero ⟶ G.obj WalkingSpan.zero
l : F.obj WalkingSpan.left ⟶ G.obj WalkingSpan.left
r : F.obj WalkingSpan.right ⟶ G.obj WalkingSpan.right
hl : F.map fst ≫ l = z ≫ G.map fst
hr : F.map snd ≫ r = z ≫ G.map snd
⊢ F.obj none ⟶ G.obj none

pp: case some.left
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y Z X' Y' Z' : C
iX : X ≅ X'
iY : Y ≅ Y'
iZ : Z ≅ Z'
F G : WalkingSpan ⥤ C
z : F.obj WalkingSpan.zero ⟶ G.obj WalkingSpan.zero
l : F.obj WalkingSpan.left ⟶ G.obj WalkingSpan.left
r : F.obj WalkingSpan.right ⟶ G.obj WalkingSpan.right
hl : F.map fst ≫ l = z ≫ G.map fst
hr : F.map snd ≫ r = z ≫ G.map snd
⊢ F.obj (some WalkingPair.left) ⟶ G.obj (some WalkingPair.left)

pp: case some.right
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y Z X' Y' Z' : C
iX : X ≅ X'
iY : Y ≅ Y'
iZ : Z ≅ Z'
F G : WalkingSpan ⥤ C
z : F.obj WalkingSpan.zero ⟶ G.obj WalkingSpan.zero
l : F.obj WalkingSpan.left ⟶ G.obj WalkingSpan.left
r : F.obj WalkingSpan.right ⟶ G.obj WalkingSpan.right
hl : F.map fst ≫ l = z ≫ G.map fst
hr : F.map snd ≫ r = z ≫ G.map snd
⊢ F.obj (some WalkingPair.right) ⟶ G.obj (some WalkingPair.right)

Tactic:
exacts [z, l, r]

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

Goal state before:
pp: case none
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y Z X' Y' Z' : C
iX : X ≅ X'
iY : Y ≅ Y'
iZ : Z ≅ Z'
F G : WalkingSpan ⥤ C
z : F.obj WalkingSpan.zero ≅ G.obj WalkingSpan.zero
l : F.obj WalkingSpan.left ≅ G.obj WalkingSpan.left
r : F.obj WalkingSpan.right ≅ G.obj WalkingSpan.right
hl : F.map fst ≫ l.hom = z.hom ≫ G.map fst
hr : F.map snd ≫ r.hom = z.hom ≫ G.map snd
⊢ F.obj none ≅ G.obj none

pp: case some.left
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y Z X' Y' Z' : C
iX : X ≅ X'
iY : Y ≅ Y'
iZ : Z ≅ Z'
F G : WalkingSpan ⥤ C
z : F.obj WalkingSpan.zero ≅ G.obj WalkingSpan.zero
l : F.obj WalkingSpan.left ≅ G.obj WalkingSpan.left
r : F.obj WalkingSpan.right ≅ G.obj WalkingSpan.right
hl : F.map fst ≫ l.hom = z.hom ≫ G.map fst
hr : F.map snd ≫ r.hom = z.hom ≫ G.map snd
⊢ F.obj (some WalkingPair.left) ≅ G.obj (some WalkingPair.left)

pp: case some.right
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y Z X' Y' Z' : C
iX : X ≅ X'
iY : Y ≅ Y'
iZ : Z ≅ Z'
F G : WalkingSpan ⥤ C
z : F.obj WalkingSpan.zero ≅ G.obj WalkingSpan.zero
l : F.obj WalkingSpan.left ≅ G.obj WalkingSpan.left
r : F.obj WalkingSpan.right ≅ G.obj WalkingSpan.right
hl : F.map fst ≫ l.hom = z.hom ≫ G.map fst
hr : F.map snd ≫ r.hom = z.hom ≫ G.map snd
⊢ F.obj (some WalkingPair.right) ≅ G.obj (some WalkingPair.right)

Tactic:
exacts [z, l, r]

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
F : D ⥤ T
X : T
Y : Over X
X✝ Y✝ : CostructuredArrow (toOver F X) Y
f : X✝ ⟶ Y✝
⊢ F.map f.left.left ≫ (mk (Over.Hom.left Y✝.hom)).hom = (mk (Over.Hom.left X✝.hom)).hom

Tactic:
by rw [← CostructuredArrow.w f]; dsimp

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
e : f ≅ g
⊢ Hom.right e.hom ≫ Hom.right e.inv = 𝟙 f.right

Tactic:
simp [← Under.comp_right]

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
e : f ≅ g
⊢ Hom.right e.inv ≫ Hom.right e.hom = 𝟙 g.right

Tactic:
simp [← Under.comp_right]

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

Goal state before:
pp: T : Type u₁
inst✝ : Category.{v₁, u₁} T
X Y Z : T
f : X ⟶ Y
g : Y ⟶ Z
⊢ map (f ≫ g) = map g ⋙ map f

Tactic:
by
  fapply Functor.ext
  · simp [Under.map, Comma.mapLeft]
  · intro U V k
    ext
    simp

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 f' : X ⟶ Y
inst✝¹ : HasImage f
inst✝ : HasImage f'
h : f = f'
⊢ (image.eqToHom h ≫ image.eqToHom ⋯) ≫ image.ι f = 𝟙 (image f) ≫ image.ι f

Tactic:
subst h
          simp [image.eqToHom, Category.assoc, Category.id_comp]

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 : Fork f g
i : IsLimit c
Z : C
h : Y ⟶ Z
hm : Mono h
this : c.ι ≫ f ≫ h = c.ι ≫ g ≫ h
⊢ c.ι ≫ f ≫ h = c.ι ≫ g ≫ h

Tactic:
by simp [this]

Goal state after:
Module: Mathlib.Algebra.Group.Ext

Goal state before:
pp: M : Type u
m₁ m₂ : Monoid M
h_mul : HMul.hMul = HMul.hMul
this : m₁.toMulOneClass = m₂.toMulOneClass
h₁ : One.one = One.one
f : M →* M := { toFun := id, map_one' := h₁, map_mul' := ⋯ }
⊢ NPow.npow = NPow.npow

Tactic:
ext n x

Goal state after:
M : Type u
m₁ m₂ : Monoid M
h_mul : HMul.hMul = HMul.hMul
this : m₁.toMulOneClass = m₂.toMulOneClass
h₁ : One.one = One.one
f : M →* M := { toFun := id, map_one' := h₁, map_mul' := ⋯ }
n : ℕ
x : M
⊢ NPow.npow n x = NPow.npow n x
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products

Goal state before:
pp: case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
f : J → C
P : C
g : (j : J) → f j ⟶ P
⊢ (Cocone.precompose (Discrete.natIso fun j ↦ Iso.refl (G.obj (f j.as))).hom).obj (G.mapCocone (Cofan.mk P g)) ≅
    Cofan.mk (G.obj P) fun j ↦ G.map (g j)

Tactic:
refine Cocone.ext (Iso.refl _) fun j => by dsimp; cases j; simp

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
G : C ⥤ D
inst✝ : G.PreservesZeroMorphisms
X✝ Y✝ : Bicone F
f : X✝ ⟶ Y✝
j : J
⊢ { pt := G.obj X✝.pt, π := fun j ↦ G.map (X✝.π j), ι := fun j ↦ G.map (X✝.ι j), ι_π := ⋯ }.ι j ≫ G.map f.hom =
    { pt := G.obj Y✝.pt, π := fun j ↦ G.map (Y✝.π j), ι := fun j ↦ G.map (Y✝.ι j), ι_π := ⋯ }.ι j

Tactic:
simp [-BiconeMorphism.wι, ← f.wι j]

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

Goal state before:
pp: case neg
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
⊢ ι g k ≫ (desc fun k ↦ eqToHom ⋯ ≫ (w (e.symm k)).hom ≫ ι f (e.symm k)) ≫ π f j =
    ι g k ≫ (lift fun j ↦ π g (e j) ≫ (w j).hom) ≫ π f j

Tactic:
simp only [ι_desc_assoc, Category.assoc, lift_π]
    rw [biproduct.ι_π_ne, biproduct.ι_π_ne_assoc]
    · simp
    · exact h
    · rintro rfl
      simp at h

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

Goal state before:
pp: case h₀
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X Y : C
inst✝ : HasBinaryBiproduct X Y
T : C
f : T ⟶ X
g : T ⟶ Y
⊢ lift f g ≫ fst = (f ≫ inl + g ≫ inr) ≫ fst

Tactic:
simp [add_comp]

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

Goal state before:
pp: case h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X Y : C
inst✝ : HasBinaryBiproduct X Y
T : C
f : T ⟶ X
g : T ⟶ Y
⊢ lift f g ≫ snd = (f ≫ inl + g ≫ inr) ≫ snd

Tactic:
simp [add_comp]

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

Goal state before:
pp: C✝ : Type u
inst✝⁴ : Category.{v, u} C✝
inst✝³ : Preadditive C✝
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
a b : Preadditive C
X Y : C
f g : X ⟶ Y
h₁ : f + g = biprod.lift (𝟙 X) (𝟙 X) ≫ biprod.desc f g
⊢ f + g = f + g

Tactic:
have h₂ := @biprod.add_eq_lift_id_desc _ _ b _ _ f g
      (by convert! (inferInstance : HasBinaryBiproduct X X); subsingleton)

Goal state after:
C✝ : Type u
inst✝⁴ : Category.{v, u} C✝
inst✝³ : Preadditive C✝
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
a b : Preadditive C
X Y : C
f g : X ⟶ Y
h₁ : f + g = biprod.lift (𝟙 X) (𝟙 X) ≫ biprod.desc f g
h₂ : f + g = biprod.lift (𝟙 X) (𝟙 X) ≫ biprod.desc f g
⊢ f + g = f + g
Module: Mathlib.Order.Fin.Tuple

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Type u_2
inst✝ : (i : Fin (n + 1)) → LE (α i)
x✝¹ : α 0 × ((i : Fin n) → α (succAbove 0 i))
x✝ : Fin (n + 1)
⊢ (insertNthOrderIso α 0) x✝¹ x✝ = (consOrderIso α) x✝¹ x✝

Tactic:
simp [insertNthOrderIso]

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

Goal state before:
pp: case cons
k n✝ x₀ : ℕ
x : Fin n✝ → ℕ
ih : ∀ {n : ℕ}, x ∈ antidiagonalTuple n✝ n ↔ ∑ i, x i = n
n : ℕ
⊢ Fin.cons x₀ x ∈ antidiagonalTuple (n✝ + 1) n ↔ ∑ i, Fin.cons x₀ x i = n

Tactic:
| cons x₀ x ih =>

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

Goal state before:
pp: case zero
n : ℕ
⊢ (antidiagonalTuple 0 n).Nodup

Tactic:
cases n <;> simp

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

Goal state before:
pp: case succ
k : ℕ
ih : ∀ (n : ℕ), (antidiagonalTuple k n).Nodup
n : ℕ
⊢ (antidiagonalTuple (k + 1) n).Nodup

Tactic:
simp_rw [antidiagonalTuple, List.nodup_flatMap]

Goal state after:
case succ
k : ℕ
ih : ∀ (n : ℕ), (antidiagonalTuple k n).Nodup
n : ℕ
⊢ (∀ x ∈ antidiagonal n, (map (fun x_1 ↦ Fin.cons x.1 x_1) (antidiagonalTuple k x.2)).Nodup) ∧
    Pairwise (Function.onFun Disjoint fun ni ↦ map (fun x ↦ Fin.cons ni.1 x) (antidiagonalTuple k ni.2))
      (antidiagonal n)
Module: Mathlib.Algebra.Order.Antidiag.Finsupp

Goal state before:
pp: ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s : Finset ι
n : μ
f : ι →₀ μ
⊢ f.support ⊆ s → (s.sum ⇑f = n ↔ (f.sum fun x x_1 ↦ x_1) = n)

Tactic:
rintro hf

Goal state after:
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s : Finset ι
n : μ
f : ι →₀ μ
hf : f.support ⊆ s
⊢ s.sum ⇑f = n ↔ (f.sum fun x x_1 ↦ x_1) = n
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: n : ℕ
c : Composition n
⊢ 0 ∈ c.boundaries

Tactic:
by
    simp only [boundaries, Finset.mem_univ, Finset.mem_map]
    exact ⟨0, And.intro True.intro rfl⟩

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

Goal state before:
pp: n : ℕ
c : Composition n
j : Fin n
i : Fin c.length := c.index j
H : ↑j < c.sizeUpTo ↑i
i_pos : 0 < ↑i
i₁ : ℕ := (↑i).pred
i₁_lt_i : i₁ < ↑i
⊢ False

Tactic:
have i₁_succ : i₁ + 1 = i := Nat.succ_pred_eq_of_pos i_pos

Goal state after:
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length := c.index j
H : ↑j < c.sizeUpTo ↑i
i_pos : 0 < ↑i
i₁ : ℕ := (↑i).pred
i₁_lt_i : i₁ < ↑i
i₁_succ : i₁ + 1 = ↑i
⊢ False
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: case mp
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length
h : j ∈ Set.range ⇑(c.embedding i)
k : Fin (c.blocksFun i)
hk : ↑((c.embedding i) k) = ↑j
⊢ c.sizeUpTo ↑i ≤ ↑j ∧ ↑j < c.sizeUpTo (↑i).succ

Tactic:
dsimp at hk

Goal state after:
case mp
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length
h : j ∈ Set.range ⇑(c.embedding i)
k : Fin (c.blocksFun i)
hk : c.sizeUpTo ↑i + ↑k = ↑j
⊢ c.sizeUpTo ↑i ≤ ↑j ∧ ↑j < c.sizeUpTo (↑i).succ
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
p : Perm α
n : ℤ
x : α
⊢ ¬(p ^ n) x = x → ¬p x = x

Tactic:
intro hx H

Goal state after:
α : Type u_1
p : Perm α
n : ℤ
x : α
hx : ¬(p ^ n) x = x
H : p x = x
⊢ False
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: α : Type u_1
ns : List ℕ
⊢ ∀ {l : List α}, ns.sum = l.length → (l.splitWrtCompositionAux ns).flatten = l

Tactic:
by
  induction ns with
  | nil => exact fun h ↦ (length_eq_zero_iff.1 h.symm).symm
  | cons n ns IH =>
    intro l h; rw [sum_cons] at h
    simp only [splitWrtCompositionAux_cons]; dsimp
    rw [IH]
    · simp
    · rw [length_drop, ← h, add_tsub_cancel_left]

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

Goal state before:
pp: case succ
n : ℕ
c : CompositionAsSet n
i : ℕ
IH : ∀ (h : i < c.boundaries.card), (take i c.blocks).sum = ↑(c.boundary ⟨i, h⟩)
h : i + 1 < c.boundaries.card
⊢ (take (i + 1) c.blocks).sum = ↑(c.boundary ⟨i + 1, h⟩)

Tactic:
have A : i < c.blocks.length := by
      rw [c.card_boundaries_eq_succ_length] at h
      simp [blocks, Nat.lt_of_succ_lt_succ h]
    have B : i < c.boundaries.card := lt_of_lt_of_le A (by simp [blocks, length])
    rw [sum_take_succ _ _ A, IH B]
    simp [blocks, blocksFun]

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

Goal state before:
pp: case intro.refine_1.refine_1
α : Type u
inst✝ : Finite α
σ τ : Perm α
hd1 : σ.Disjoint τ
val✝ : Fintype α
f : Perm α
hc1 : IsConj σ (f * σ * f⁻¹)
g : Perm α
hc2 : IsConj τ (g * τ * g⁻¹)
hd2 : (f * σ * f⁻¹).Disjoint (g * τ * g⁻¹)
hd1' : ↑(σ * τ).support = ↑σ.support ∪ ↑τ.support
hd2' : ↑(f * σ * f⁻¹ * (g * τ * g⁻¹)).support = ↑(f * σ * f⁻¹).support ∪ ↑(g * τ * g⁻¹).support
hd1'' : _root_.Disjoint ↑σ.support ↑τ.support
hd2'' : _root_.Disjoint ↑(f * σ * f⁻¹).support ↑(g * τ * g⁻¹).support
a : α
⊢ a ∈ ↑σ.support ↔ f a ∈ ↑(f * σ * f⁻¹).support

Tactic:
simp only [Set.mem_image, toEmbedding_apply, exists_eq_right, support_conj, coe_map,
        apply_eq_iff_eq]

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

Goal state before:
pp: case intro.refine_1.refine_2
α : Type u
inst✝ : Finite α
σ τ : Perm α
hd1 : σ.Disjoint τ
val✝ : Fintype α
f : Perm α
hc1 : IsConj σ (f * σ * f⁻¹)
g : Perm α
hc2 : IsConj τ (g * τ * g⁻¹)
hd2 : (f * σ * f⁻¹).Disjoint (g * τ * g⁻¹)
hd1' : ↑(σ * τ).support = ↑σ.support ∪ ↑τ.support
hd2' : ↑(f * σ * f⁻¹ * (g * τ * g⁻¹)).support = ↑(f * σ * f⁻¹).support ∪ ↑(g * τ * g⁻¹).support
hd1'' : _root_.Disjoint ↑σ.support ↑τ.support
hd2'' : _root_.Disjoint ↑(f * σ * f⁻¹).support ↑(g * τ * g⁻¹).support
a : α
⊢ a ∈ ↑τ.support ↔ g a ∈ ↑(g * τ * g⁻¹).support

Tactic:
simp only [Set.mem_image, toEmbedding_apply, exists_eq_right, support_conj, coe_map,
        apply_eq_iff_eq]

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

Goal state before:
pp: case intro.refine_2
α : Type u
inst✝ : Finite α
σ τ : Perm α
hd1 : σ.Disjoint τ
val✝ : Fintype α
f : Perm α
hc1 : IsConj σ (f * σ * f⁻¹)
g : Perm α
hc2 : IsConj τ (g * τ * g⁻¹)
hd2 : (f * σ * f⁻¹).Disjoint (g * τ * g⁻¹)
hd1' : ↑(σ * τ).support = ↑σ.support ∪ ↑τ.support
hd2' : ↑(f * σ * f⁻¹ * (g * τ * g⁻¹)).support = ↑(f * σ * f⁻¹).support ∪ ↑(g * τ * g⁻¹).support
hd1'' : _root_.Disjoint ↑σ.support ↑τ.support
hd2'' : _root_.Disjoint ↑(f * σ * f⁻¹).support ↑(g * τ * g⁻¹).support
x : α
hx : x ∈ ↑(σ * τ).support
⊢ ↑((Set.union hd2'').symm (Sum.map (⇑(subtypeEquiv f ⋯)) (⇑(subtypeEquiv g ⋯)) ((Set.union hd1'') ⟨(σ * τ) x, ⋯⟩))) =
    (f * σ * f⁻¹ * (g * τ * g⁻¹))
      ↑((Set.union hd2'').symm (Sum.map (⇑(subtypeEquiv f ⋯)) (⇑(subtypeEquiv g ⋯)) ((Set.union hd1'') ⟨x, ⋯⟩)))

Tactic:
hd1',

Goal state after:
case intro.refine_2
α : Type u
inst✝ : Finite α
σ τ : Perm α
hd1 : σ.Disjoint τ
val✝ : Fintype α
f : Perm α
hc1 : IsConj σ (f * σ * f⁻¹)
g : Perm α
hc2 : IsConj τ (g * τ * g⁻¹)
hd2 : (f * σ * f⁻¹).Disjoint (g * τ * g⁻¹)
hd1' : ↑(σ * τ).support = ↑σ.support ∪ ↑τ.support
hd2' : ↑(f * σ * f⁻¹ * (g * τ * g⁻¹)).support = ↑(f * σ * f⁻¹).support ∪ ↑(g * τ * g⁻¹).support
hd1'' : _root_.Disjoint ↑σ.support ↑τ.support
hd2'' : _root_.Disjoint ↑(f * σ * f⁻¹).support ↑(g * τ * g⁻¹).support
x : α
hx✝ : x ∈ ↑(σ * τ).support
hx : x ∈ ↑σ.support ∪ ↑τ.support
⊢ ↑((Set.union hd2'').symm (Sum.map (⇑(subtypeEquiv f ⋯)) (⇑(subtypeEquiv g ⋯)) ((Set.union hd1'') ⟨(σ * τ) x, ⋯⟩))) =
    (f * σ * f⁻¹ * (g * τ * g⁻¹))
      ↑((Set.union hd2'').symm (Sum.map (⇑(subtypeEquiv f ⋯)) (⇑(subtypeEquiv g ⋯)) ((Set.union hd1'') ⟨x, ⋯⟩)))