mathlib-initiative/mathlib-tactics huggingface dataset:
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_obj : C → D
e : (X : C) → (Y : D) → (F_obj X ⟶ Y) ≃ (X ⟶ G.obj Y)
he : ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y), (e X Y') (h ≫ g) = (e X Y) h ≫ G.map g
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
f' : Y✝ ⟶ Z✝
| f ≫ (e Y✝ (F_obj Z✝)) ((e Y✝ (F_obj Z✝)).symm (f' ≫ (e Z✝ (F_obj Z✝)) (𝟙 (F_obj Z✝))))

Tactic:
Equiv.apply_symm_apply

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
F_obj : C → D
e : (X : C) → (Y : D) → (F_obj X ⟶ Y) ≃ (X ⟶ G.obj Y)
he : ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y), (e X Y') (h ≫ g) = (e X Y) h ≫ G.map g
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
f' : Y✝ ⟶ Z✝
| f ≫ f' ≫ (e Z✝ (F_obj Z✝)) (𝟙 (F_obj Z✝))
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
| h.homEquiv f

Tactic:
← Category.id_comp f

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
| h.homEquiv (𝟙 X ≫ f)
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 : Cocone F
X : C
h : F.cocones.CorepresentableBy X
s : Cocone F
m : (colimitCocone h).pt ⟶ s.pt
w : ∀ (j : J), (colimitCocone h).ι.app j ≫ m = s.ι.app j
⊢ m = homOfCocone h s

Tactic:
← homOfCocone_coconeOfHom h m

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
X : C
h : F.cocones.CorepresentableBy X
s : Cocone F
m : (colimitCocone h).pt ⟶ s.pt
w : ∀ (j : J), (colimitCocone h).ι.app j ≫ m = s.ι.app j
⊢ homOfCocone h (coconeOfHom h m) = homOfCocone h s
Module: Mathlib.CategoryTheory.Bicategory.Strict.Basic

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g h : b ⟶ c
η : g = h
⊢ f ◁ eqToHom η = eqToHom ⋯

Tactic:
cases η
  simp only [whiskerLeft_id, eqToHom_refl]

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
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : Small.{w, u'} D
inst✝ : LocallySmall.{w, v', u'} D
⊢ Small.{w, max (max (max u' u) v') v} (C ⥤ D)

Tactic:
refine small_of_injective (f := fun F (f : Arrow C) ↦ Arrow.mk (F.map f.hom))
    (fun F G h ↦ Functor.ext (fun X ↦ ?_) (fun X Y f ↦ ?_))

Goal state after:
case refine_1
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Small.{w, u} C
inst✝³ : LocallySmall.{w, v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : Small.{w, u'} D
inst✝ : LocallySmall.{w, v', u'} D
F G : C ⥤ D
h : (fun F f ↦ Arrow.mk (F.map f.hom)) F = (fun F f ↦ Arrow.mk (F.map f.hom)) G
X : C
⊢ F.obj X = G.obj X

case refine_2
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Small.{w, u} C
inst✝³ : LocallySmall.{w, v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : Small.{w, u'} D
inst✝ : LocallySmall.{w, v', u'} D
F G : C ⥤ D
h : (fun F f ↦ Arrow.mk (F.map f.hom)) F = (fun F f ↦ Arrow.mk (F.map f.hom)) G
X Y : C
f : X ⟶ Y
⊢ F.map f = eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.LiftingProperties.Basic

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
A B B' X Y Y' : C
i : A ⟶ B
i' : B ⟶ B'
p : X ⟶ Y
p' : Y ⟶ Y'
inst✝¹ : HasLiftingProperty i p
inst✝ : HasLiftingProperty i' p
f : A ⟶ X
g : B' ⟶ Y
sq : CommSq f (i ≫ i') p g
fac : f ≫ p = i ≫ i' ≫ g
⊢ ⋯.lift ≫ p = g

Tactic:
by simp only [CommSq.fac_right]

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : C
hI : IsInitial I
h : ∀ (X : C), Mono (hI.to X)
I' X : C
hI' : IsInitial I'
⊢ Mono (hI'.to X)

Tactic:
rw [hI'.hom_ext (hI'.to X) ((hI'.uniqueUpToIso hI).hom ≫ hI.to X)]

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : C
hI : IsInitial I
h : ∀ (X : C), Mono (hI.to X)
I' X : C
hI' : IsInitial I'
⊢ Mono ((hI'.uniqueUpToIso hI).hom ≫ hI.to X)
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)
inst✝ : IsIso (pre F E)
k : K
⊢ ι F (E.obj k) ≫ inv (pre F E) = ι (E ⋙ F) k

Tactic:
simp [IsIso.comp_inv_eq]

Goal state after:
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
⊢ t.ι.app WalkingSpan.zero = f ≫ t.inl

Tactic:
have w := t.ι.naturality WalkingSpan.Hom.fst

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
t : PushoutCocone f g
w :
  (span f g).map fst ≫ t.ι.app WalkingSpan.left =
    t.ι.app WalkingSpan.zero ≫ ((Functor.const WalkingSpan).obj t.pt).map fst
⊢ t.ι.app WalkingSpan.zero = f ≫ t.inl
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 S' S'' : D
Y Y' Y'' : C
T T' : C ⥤ D
A : Type u₃
inst✝¹ : Category.{v₃, u₃} A
B : Type u₄
inst✝ : Category.{v₄, u₄} B
L : D
R : C ⥤ D
L' : B
R' : A ⥤ B
F✝ : C ⥤ A
G✝ : D ⥤ B
α✝ : L' ⟶ G✝.obj L
β✝ : R ⋙ G✝ ⟶ F✝ ⋙ R'
F : C ≌ A
G : D ≌ B
α : L' ⟶ G.functor.obj L
α' : L ⟶ G.inverse.obj L'
β : R ⋙ G.functor ⟶ F.functor ⋙ R'
β' : R' ⋙ G.inverse ⟶ F.inverse ⋙ R
hαα' : α ≫ G.functor.map α' = G.counitIso.inv.app L'
hα'α : α' ≫ G.inverse.map α = G.unitIso.hom.app L
hββ' :
  R.rightUnitor.hom ≫ R.leftUnitor.inv ≫ Functor.whiskerRight F.unitIso.hom R ≫ (F.functor.associator F.inverse R).hom =
    R.whiskerLeft G.unitIso.hom ≫
      (R.associator G.functor G.inverse).inv ≫
        Functor.whiskerRight β G.inverse ≫ (F.functor.associator R' G.inverse).hom ≫ F.functor.whiskerLeft β'
hβ'β :
  Functor.whiskerRight β' G.functor ≫
      (F.inverse.associator R G.functor).hom ≫
        F.inverse.whiskerLeft β ≫ (F.inverse.associator F.functor R').inv ≫ Functor.whiskerRight F.counitIso.hom R' =
    (R'.associator G.inverse G.functor).hom ≫ R'.whiskerLeft G.counitIso.hom ≫ R'.rightUnitor.hom ≫ R'.leftUnitor.inv
⊢ (R.rightUnitor.hom ≫ R.leftUnitor.inv) ≫ Functor.whiskerRight F.unitIso.hom R =
    R.whiskerLeft G.unitIso.hom ≫
      (R.associator G.functor G.inverse).inv ≫
        Functor.whiskerRight β G.inverse ≫
          (F.functor.associator R' G.inverse).hom ≫ F.functor.whiskerLeft β' ≫ (F.functor.associator F.inverse R).inv

Tactic:
ext X
    simpa using congr($(hββ').app X)

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
Y : T
X : D
Y✝ Z✝ : StructuredArrow X (proj Y F)
m : Y✝ ⟶ Z✝
⊢ Y✝.hom ≫ (proj X (proj Y F) ⋙ proj Y F).map m = Z✝.hom

Tactic:
have := m.w; cat_disch

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

Goal state before:
pp: T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ T
Y : T
X : D
Y✝ Z✝ : StructuredArrow Y (Under.forget X ⋙ F)
m : Y✝ ⟶ Z✝
⊢ Y✝.hom ≫ F.map ((proj Y (Under.forget X ⋙ F) ⋙ Under.forget X).map m) = Z✝.hom

Tactic:
have := m.w; cat_disch

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

Goal state before:
pp: T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : T × T
Y✝ Z✝ : StructuredArrow X.2 (Under.forget X.1)
m : Y✝ ⟶ Z✝
⊢ (Y✝.right.hom, Y✝.hom) ≫ (Functor.diag T).map ((proj X.2 (Under.forget X.1) ⋙ Under.forget X.1).map m) =
    (Z✝.right.hom, Z✝.hom)

Tactic:
have := m.w; cat_disch

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

Goal state before:
pp: T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : T ⥤ D
Y : D
X : T
Y✝ Z✝ : CostructuredArrow (proj F Y) X
m : Y✝ ⟶ Z✝
⊢ (proj (proj F Y) X ⋙ proj F Y).map m ≫ Z✝.hom = Y✝.hom

Tactic:
have := m.w; cat_disch

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

Goal state before:
pp: T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : T ⥤ D
Y : D
X : T
Y✝ Z✝ : CostructuredArrow (Over.forget X ⋙ F) Y
m : Y✝ ⟶ Z✝
⊢ F.map ((proj (Over.forget X ⋙ F) Y ⋙ Over.forget X).map m) ≫ Z✝.hom = Y✝.hom

Tactic:
have := m.w; cat_disch

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

Goal state before:
pp: T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : T × T
Y✝ Z✝ : CostructuredArrow (Over.forget X.1) X.2
m : Y✝ ⟶ Z✝
⊢ (Functor.diag T).map ((proj (Over.forget X.1) X.2 ⋙ Over.forget X.1).map m) ≫ (Z✝.left.hom, Z✝.hom) =
    (Y✝.left.hom, Y✝.hom)

Tactic:
have := m.w; cat_disch

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

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
W₁ W₂ : MorphismProperty C
F : D ⥤ C
inst✝² : F.IsEquivalence
inst✝¹ : W₁.RespectsIso
inst✝ : W₂.RespectsIso
X Y : D
f : X ⟶ Y
h : W₁.MapFactorizationData W₂ (F.map f)
⊢ Arrow.mk h.i ≅ Arrow.mk (F.map (F.preimage (h.i ≫ (F.objObjPreimageIso h.Z).inv)))

Tactic:
refine Arrow.isoMk (Iso.refl _) (F.objObjPreimageIso h.Z).symm ?_

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
W₁ W₂ : MorphismProperty C
F : D ⥤ C
inst✝² : F.IsEquivalence
inst✝¹ : W₁.RespectsIso
inst✝ : W₂.RespectsIso
X Y : D
f : X ⟶ Y
h : W₁.MapFactorizationData W₂ (F.map f)
⊢ (Iso.refl (Arrow.mk h.i).left).hom ≫ (Arrow.mk (F.map (F.preimage (h.i ≫ (F.objObjPreimageIso h.Z).inv)))).hom =
    (Arrow.mk h.i).hom ≫ (F.objObjPreimageIso h.Z).symm.hom
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono

Goal state before:
pp: case h₁
C✝ : Type u
inst✝³ : Category.{v, u} C✝
W✝ X✝ Y✝ Z✝ : C✝
C : Type u_1
inst✝² : Category.{v_1, u_1} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝¹ : HasPushout f g
inst✝ : HasBinaryCoproduct Y Z
W : C
i₁ i₂ : pushout f g ⟶ W
h : coprod.desc (pushout.inl f g) (pushout.inr f g) ≫ i₁ = coprod.desc (pushout.inl f g) (pushout.inr f g) ≫ i₂
⊢ pushout.inr f g ≫ i₁ = pushout.inr f g ≫ i₂

Tactic:
simpa using congrArg (fun f => coprod.inr ≫ f) h

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
P : C
ι : P ⟶ X✝
w : ι ≫ f = ι ≫ g
X : WalkingParallelPair
⊢ ((Functor.const WalkingParallelPair).obj P).obj X ⟶ (parallelPair f g).obj X

Tactic:
by
        cases X
        · exact ι
        · exact ι ≫ f

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✝¹ : HasTerminal C
inst✝ : PreservesLimit (Functor.empty C) G
F : Discrete PEmpty.{1} ⥤ D
⊢ HasLimit F

Tactic:
have := HasLimit.mk ⟨_, isLimitOfHasTerminalOfPreservesLimit G⟩
  apply hasLimit_of_iso F.uniqueFromEmpty.symm

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroObject C
inst✝¹ : HasEqualizers C
X Y : C
f : X ⟶ Y
h : f = 0
inst✝ : HasImage f
⊢ ι f = 0

Tactic:
rw [image.eq_fac h]

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroObject C
inst✝¹ : HasEqualizers C
X Y : C
f : X ⟶ Y
h : f = 0
inst✝ : HasImage f
⊢ (eqToIso h).hom ≫ ι 0 = 0
Module: Mathlib.CategoryTheory.Limits.Preserves.Basic

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J✝ : Type w
inst✝² : Category.{w', w} J✝
K✝ : J✝ ⥤ C
F : C ⥤ D
inst✝¹ : F.Full
inst✝ : F.Faithful
J : Type w'
𝒥₁ : Category.{w, w'} J
K : J ⥤ C
c : Cone K
t : IsLimit (F.mapCone c)
⊢ ∀ (s : Cone K) (m : s ⟶ c),
    m = (Cone.functoriality K F).preimage (t.liftConeMorphism ((Cone.functoriality K F).obj s))

Tactic:
by
              apply fun s m => (Cone.functoriality K F).map_injective _
              intro s m
              rw [Functor.map_preimage]
              apply t.uniq_cone_morphism

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✝
X Y : C
f : X ⟶ Y
hf : f = 0
⊢ 𝟙 X ≫ f = 0

Tactic:
rw [hf, comp_zero]

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
⊢ f ≫ s.π = 0 ≫ s.π

Tactic:
apply hg.left_cancellation

Goal state after:
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
⊢ g ≫ f ≫ s.π = g ≫ 0 ≫ s.π
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Goal state before:
pp: J : Type w
C : Type uC
inst✝¹ : Category.{uC', uC} C
inst✝ : HasZeroMorphisms C
f : J → C
t : Bicone f
ht : IsLimit t.toCone
j : J
j' : Discrete J
⊢ t.ι j ≫ t.toCone.π.app j' = ht.lift (Fan.mk (f j) fun j' ↦ if h : j = j' then eqToHom ⋯ else 0) ≫ t.toCone.π.app j'

Tactic:
ht.fac

Goal state after:
J : Type w
C : Type uC
inst✝¹ : Category.{uC', uC} C
inst✝ : HasZeroMorphisms C
f : J → C
t : Bicone f
ht : IsLimit t.toCone
j : J
j' : Discrete J
⊢ t.ι j ≫ t.toCone.π.app j' = (Fan.mk (f j) fun j' ↦ if h : j = j' then eqToHom ⋯ else 0).π.app j'
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Goal state before:
pp: J : Type w
C : Type uC
inst✝¹ : Category.{uC', uC} C
inst✝ : HasZeroMorphisms C
f : J → C
t : Bicone f
ht : IsColimit t.toCocone
j : J
j' : Discrete J
⊢ t.toCocone.ι.app j' ≫ t.π j =
    t.toCocone.ι.app j' ≫ ht.desc (Cofan.mk (f j) fun j' ↦ if h : j' = j then eqToHom ⋯ else 0)

Tactic:
ht.fac

Goal state after:
J : Type w
C : Type uC
inst✝¹ : Category.{uC', uC} C
inst✝ : HasZeroMorphisms C
f : J → C
t : Bicone f
ht : IsColimit t.toCocone
j : J
j' : Discrete J
⊢ t.toCocone.ι.app j' ≫ t.π j = (Cofan.mk (f j) fun j' ↦ if h : j' = j then eqToHom ⋯ else 0).ι.app j'
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts

Goal state before:
pp: J : Type w
C : Type uC
inst✝⁴ : Category.{uC', uC} C
inst✝³ : HasZeroMorphisms C
D : Type uD
inst✝² : Category.{uD', uD} D
inst✝¹ : HasZeroMorphisms D
P Q : C
F : C ⥤ D
inst✝ : F.PreservesZeroMorphisms
X✝ Y✝ : BinaryBicone P Q
f : X✝ ⟶ Y✝
⊢ F.map f.hom ≫
      { pt := F.obj Y✝.pt, fst := F.map Y✝.fst, snd := F.map Y✝.snd, inl := F.map Y✝.inl, inr := F.map Y✝.inr,
          inl_fst := ⋯, inl_snd := ⋯, inr_fst := ⋯, inr_snd := ⋯ }.fst =
    { pt := F.obj X✝.pt, fst := F.map X✝.fst, snd := F.map X✝.snd, inl := F.map X✝.inl, inr := F.map X✝.inr,
        inl_fst := ⋯, inl_snd := ⋯, inr_fst := ⋯, inr_snd := ⋯ }.fst

Tactic:
simp [-BinaryBiconeMorphism.wfst, ← f.wfst]

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

Goal state before:
pp: J : Type w
C : Type uC
inst✝⁷ : Category.{uC', uC} C
inst✝⁶ : HasZeroMorphisms C
D : Type uD
inst✝⁵ : Category.{uD', uD} D
inst✝⁴ : HasZeroMorphisms D
P Q W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst✝³ : Mono f
inst✝² : Mono g
inst✝¹ : HasBinaryBiproduct W X
inst✝ : HasBinaryBiproduct Y Z
⊢ Mono (map f g)

Tactic:
show coprod.map f g = (biprod.isoCoprod _ _).inv ≫ biprod.map f g ≫
    (biprod.isoCoprod _ _).hom by simp

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
P Q W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst✝³ : Mono f
inst✝² : Mono g
inst✝¹ : HasBinaryBiproduct W X
inst✝ : HasBinaryBiproduct Y Z
⊢ Mono ((biprod.isoCoprod W X).inv ≫ biprod.map f g ≫ (biprod.isoCoprod Y Z).hom)
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
inst✝² : HasBinaryBiproducts C
X₁ X₂ Y₁ Y₂ : C
f₁₁ : X₁ ⟶ Y₁
f₁₂ : X₁ ⟶ Y₂
f₂₁ : X₂ ⟶ Y₁
f₂₂ : X₂ ⟶ Y₂
inst✝¹ : IsIso f₁₁
inst✝ : IsIso (ofComponents f₁₁ f₁₂ f₂₁ f₂₂)
L : X₁ ⊞ X₂ ≅ X₁ ⊞ X₂
R : Y₁ ⊞ Y₂ ≅ Y₁ ⊞ Y₂
g : X₂ ⟶ Y₂
w : L.hom ≫ ofComponents f₁₁ f₁₂ f₂₁ f₂₂ ≫ R.hom = biprod.map f₁₁ g
⊢ IsIso (biprod.map f₁₁ g)

Tactic:
rw [← w]
    infer_instance

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
σ τ : Type
inst✝³ : Finite τ
S : σ → C
inst✝² : HasBiproduct S
T : τ → C
inst✝¹ : HasBiproduct T
s : σ
f : ⨁ S ⟶ ⨁ T
inst✝ : IsIso f
val✝ : Fintype τ
z : ∀ (t : τ), biproduct.ι S s ≫ f ≫ biproduct.π T t = 0
reassoced : ∀ {t : τ} {W : C} (h : T t ⟶ W), biproduct.ι S s ≫ f ≫ biproduct.π T t ≫ h = 0 ≫ h
x : S s ⟶ S s := biproduct.ι S s ≫ f ≫ inv f ≫ biproduct.π S s
h₁ : x = 𝟙 (S s)
⊢ biproduct.ι S s ≫ f ≫ (∑ j, biproduct.π T j ≫ biproduct.ι T j) ≫ inv f ≫ biproduct.π S s = 0

Tactic:
simp only [comp_sum_assoc]

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
σ τ : Type
inst✝³ : Finite τ
S : σ → C
inst✝² : HasBiproduct S
T : τ → C
inst✝¹ : HasBiproduct T
s : σ
f : ⨁ S ⟶ ⨁ T
inst✝ : IsIso f
val✝ : Fintype τ
z : ∀ (t : τ), biproduct.ι S s ≫ f ≫ biproduct.π T t = 0
reassoced : ∀ {t : τ} {W : C} (h : T t ⟶ W), biproduct.ι S s ≫ f ≫ biproduct.π T t ≫ h = 0 ≫ h
x : S s ⟶ S s := biproduct.ι S s ≫ f ≫ inv f ≫ biproduct.π S s
h₁ : x = 𝟙 (S s)
⊢ (∑ j, biproduct.ι S s ≫ f ≫ biproduct.π T j ≫ biproduct.ι T j) ≫ inv f ≫ biproduct.π S s = 0
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: case inr
α : Type u_1
σ τ : Perm α
hστ : σ.Disjoint τ
a : α
h : (σ * τ) a = a
hτ : τ a = a
⊢ σ a = a ∧ τ a = a

Tactic:
· exact ⟨(congr_arg σ hτ).symm.trans h, hτ⟩

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

Goal state before:
pp: n : ℕ
i : Fin (ones n).length
h : 0 < (ones n).blocksFun i
⊢ ((ones n).embedding i) ⟨0, h⟩ = ⟨↑i, ⋯⟩

Tactic:
by
  ext
  simpa using i.2.le

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

Goal state before:
pp: 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) ⋯)

Tactic:
reverse_append,

Goal state after:
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)
⊢ (c.reverse.append (single (k + 1) ⋯).reverse).cast ⋯ ≍ c.reverse.append (single (k + 1) ⋯)
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), g x ∈ s ↔ x ∈ s
hc : c.support ⊆ s
h : ∀ a ∈ s, c a = g a
a : α
ha : a ∈ s
⊢ (ofSubtype (g.subtypePerm hg)) a = c a

pp: case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), g x ∈ s ↔ x ∈ s
hc : c.support ⊆ s
h : ∀ a ∈ s, c a = g a
a : α
ha : a ∉ s
⊢ (ofSubtype (g.subtypePerm hg)) a = c a

Tactic:
· rw [h a ha, ofSubtype_apply_of_mem (p := (· ∈ s)) _ ha, subtypePerm_apply]

Goal state after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), g x ∈ s ↔ x ∈ s
hc : c.support ⊆ s
h : ∀ a ∈ s, c a = g a
a : α
ha : a ∉ s
⊢ (ofSubtype (g.subtypePerm hg)) a = c a
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: case cons.succ
α : Type u_1
n : ℕ
ns : List ℕ
IH :
  ∀ (l : List α) {i : ℕ} (hi : i < (l.splitWrtCompositionAux ns).length),
    (l.splitWrtCompositionAux ns)[i] = drop (take i ns).sum (take (take (i + 1) ns).sum l)
l : List α
i : ℕ
hi : i + 1 < (l.splitWrtCompositionAux (n :: ns)).length
⊢ (l.splitWrtCompositionAux (n :: ns))[i + 1] =
    drop (take (i + 1) (n :: ns)).sum (take (take (i + 1 + 1) (n :: ns)).sum l)

Tactic:
· simp only [splitWrtCompositionAux, getElem_cons_succ, IH, take,
          sum_cons, splitAt_eq, drop_take, drop_drop]
      rw [Nat.add_sub_add_left]

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

Goal state before:
pp: n✝ n : ℕ
c : CompositionAsSet n
i : Fin n.succ
⊢ i ∈
      ((fun s ↦
            { boundaries := {i | i = 0 ∨ i = Fin.last n ∨ ∃ j, ∃ (_ : j ∈ s), ↑i = ↑j + 1}.toFinset, zero_mem := ⋯,
              getLast_mem := ⋯ })
          ((fun c ↦ {i | ⟨1 + ↑i, ⋯⟩ ∈ c.boundaries}.toFinset) c)).boundaries ↔
    i ∈ c.boundaries

Tactic:
simp only [add_comm, Set.toFinset_ofPred, Finset.mem_univ,
     Finset.mem_filter, true_and, exists_prop]

Goal state after:
n✝ n : ℕ
c : CompositionAsSet n
i : Fin n.succ
⊢ (i = 0 ∨ i = Fin.last n ∨ ∃ j, ⟨↑j + 1, ⋯⟩ ∈ c.boundaries ∧ ↑i = ↑j + 1) ↔ i ∈ c.boundaries
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: case mp.inl
n✝ n : ℕ
c : CompositionAsSet n
⊢ 0 ∈ c.boundaries

Tactic:
exact c.zero_mem

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

Goal state before:
pp: case mp.inl
n✝ n : ℕ
c : CompositionAsSet n
⊢ 0 ∈ c.boundaries

pp: case mp.inr.inl
n✝ n : ℕ
c : CompositionAsSet n
⊢ Fin.last n ∈ c.boundaries

pp: case mp.inr.inr
n✝ n : ℕ
c : CompositionAsSet n
i : Fin n.succ
j : Fin (n - 1)
hj1 : ⟨↑j + 1, ⋯⟩ ∈ c.boundaries
hj2 : ↑i = ↑j + 1
⊢ i ∈ c.boundaries

Tactic:
· exact c.zero_mem

Goal state after:
case mp.inr.inl
n✝ n : ℕ
c : CompositionAsSet n
⊢ Fin.last n ∈ c.boundaries

case mp.inr.inr
n✝ n : ℕ
c : CompositionAsSet n
i : Fin n.succ
j : Fin (n - 1)
hj1 : ⟨↑j + 1, ⋯⟩ ∈ c.boundaries
hj2 : ↑i = ↑j + 1
⊢ i ∈ c.boundaries
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : ¬f = 1
⊢ #f.support ≠ 1

Tactic:
exact ne_of_gt (one_lt_card_support_of_ne_one h)

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : f.Disjoint g
⊢ #(f * g).support = #f.support + #g.support

Tactic:
rw [← Finset.card_union_of_disjoint]

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : f.Disjoint g
⊢ #(f * g).support = #(f.support ∪ g.support)

α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : f.Disjoint g
⊢ _root_.Disjoint f.support g.support