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
L' : A' ⥤ T'
R' : B' ⥤ T'
F₁ : A ⥤ A'
F₂ : B ⥤ B'
F : T ⥤ T'
α : F₁ ⋙ L' ⟶ L ⋙ F
β : R ⋙ F ⟶ F₂ ⋙ R'
inst✝⁴ : F₁.EssSurj
inst✝³ : F₂.EssSurj
inst✝² : F.Full
inst✝¹ : IsIso α
inst✝ : IsIso β
X : Comma L' R'
⊢ L'.map (F₁.objObjPreimageIso X.left).hom ≫ X.hom =
    L'.map (F₁.objObjPreimageIso X.left).hom ≫
      X.hom ≫ R'.map (F₂.objObjPreimageIso X.right).inv ≫ R'.map (F₂.objObjPreimageIso X.right).hom

Tactic:
← R'.map_comp,

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
L' : A' ⥤ T'
R' : B' ⥤ T'
F₁ : A ⥤ A'
F₂ : B ⥤ B'
F : T ⥤ T'
α : F₁ ⋙ L' ⟶ L ⋙ F
β : R ⋙ F ⟶ F₂ ⋙ R'
inst✝⁴ : F₁.EssSurj
inst✝³ : F₂.EssSurj
inst✝² : F.Full
inst✝¹ : IsIso α
inst✝ : IsIso β
X : Comma L' R'
⊢ L'.map (F₁.objObjPreimageIso X.left).hom ≫ X.hom =
    L'.map (F₁.objObjPreimageIso X.left).hom ≫
      X.hom ≫ R'.map ((F₂.objObjPreimageIso X.right).inv ≫ (F₂.objObjPreimageIso X.right).hom)
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
adj adj' : F ⊣ G
h : adj.unit = adj'.unit
X : D
⊢ (adj.homEquiv (G.obj X) ((𝟭 D).obj X)) (adj.counit.app X) = (adj.homEquiv (G.obj X) ((𝟭 D).obj X)) (adj'.counit.app X)

Tactic:
rw [Adjunction.homEquiv_unit, Adjunction.homEquiv_unit,
    Adjunction.right_triangle_components, h, Adjunction.right_triangle_components]

Goal state after:
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
adj : CoreHomEquivUnitCounit F G
⊢ (mk' adj).homEquiv = adj.homEquiv

Tactic:
by
  ext
  rw [homEquiv_unit, adj.homEquiv_unit, mk'_unit]

Goal state after:
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_obj : D → C
e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)
he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), (e X' Y) (F.map f ≫ g) = f ≫ (e X Y) g
X' X : C
Y : D
f : X' ⟶ X
g : X ⟶ G_obj Y
⊢ F.map f ≫ (e X Y).symm g = (e X' Y).symm (f ≫ g)

Tactic:
Equiv.eq_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_obj : D → C
e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)
he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), (e X' Y) (F.map f ≫ g) = f ≫ (e X Y) g
X' X : C
Y : D
f : X' ⟶ X
g : X ⟶ G_obj Y
⊢ (e X' Y) (F.map f ≫ (e X Y).symm g) = f ≫ g
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
Z W : C
f : yoneda.obj Z ⟶ yoneda.obj W
⊢ yoneda.map ((ConcreteCategory.hom (f.app (op Z))) (𝟙 (unop (op Z)))) = f

Tactic:
ext X x

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Z W : C
f : yoneda.obj Z ⟶ yoneda.obj W
X : Cᵒᵖ
x : (yoneda.obj Z).obj X
⊢ (ConcreteCategory.hom ((yoneda.map ((ConcreteCategory.hom (f.app (op Z))) (𝟙 (unop (op Z))))).app X)).toFun x =
    (ConcreteCategory.hom (f.app X)).toFun x
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
Z W : Cᵒᵖ
f : coyoneda.obj Z ⟶ coyoneda.obj W
⊢ coyoneda.map (Quiver.Hom.op ((ConcreteCategory.hom (f.app (unop Z))) (𝟙 (unop Z)))) = f

Tactic:
ext X x

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Z W : Cᵒᵖ
f : coyoneda.obj Z ⟶ coyoneda.obj W
X : C
x : (coyoneda.obj Z).obj X
⊢ (ConcreteCategory.hom
          ((coyoneda.map (Quiver.Hom.op ((ConcreteCategory.hom (f.app (unop Z))) (𝟙 (unop Z))))).app X)).toFun
      x =
    (ConcreteCategory.hom (f.app X)).toFun x
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
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝ : F.IsEquivalence
⊢ (F ⋙ G).IsRightAdjoint ↔ G.IsRightAdjoint

Tactic:
by
  refine ⟨fun h ↦ ?_, fun h ↦ inferInstance⟩
  let iso : G ≅ F.asEquivalence.inverse ⋙ F ⋙ G :=
    (Functor.leftUnitor _).symm ≪≫ Functor.isoWhiskerRight (F.asEquivalence.counitIso).symm _ ≪≫
      Functor.associator _ _ _
  exact isRightAdjoint_of_iso iso.symm

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F F' : Cᵒᵖ ⥤ Type v₁
f : F ⟶ F'
x : F.obj (op X)
⊢ yonedaEquiv.symm x ≫ f = yonedaEquiv.symm ((ConcreteCategory.hom (f.app (op X))) x)

Tactic:
apply yonedaEquiv.injective
  simp [yonedaEquiv_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P Q : Cᵒᵖ ⥤ Type v₁
f g : P ⟶ Q
h : ∀ (X : C) (p : yoneda.obj X ⟶ P), p ≫ f = p ≫ g
⊢ f = g

Tactic:
ext X x

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P Q : Cᵒᵖ ⥤ Type v₁
f g : P ⟶ Q
h : ∀ (X : C) (p : yoneda.obj X ⟶ P), p ≫ f = p ≫ g
X : Cᵒᵖ
x : P.obj X
⊢ (ConcreteCategory.hom (f.app X)).toFun x = (ConcreteCategory.hom (g.app X)).toFun x
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P Q : Cᵒᵖ ⥤ Type (max w v₁)
f g : P ⟶ Q
h : ∀ (X : C) (p : uliftYoneda.{w, v₁, u₁}.obj X ⟶ P), p ≫ f = p ≫ g
⊢ f = g

Tactic:
ext X x

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P Q : Cᵒᵖ ⥤ Type (max w v₁)
f g : P ⟶ Q
h : ∀ (X : C) (p : uliftYoneda.{w, v₁, u₁}.obj X ⟶ P), p ≫ f = p ≫ g
X : Cᵒᵖ
x : P.obj X
⊢ (ConcreteCategory.hom (f.app X)).toFun x = (ConcreteCategory.hom (g.app X)).toFun x
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P Q : C ⥤ Type (max w v₁)
f g : P ⟶ Q
h : ∀ (X : Cᵒᵖ) (p : uliftCoyoneda.{w, v₁, u₁}.obj X ⟶ P), p ≫ f = p ≫ g
⊢ f = g

Tactic:
ext X x

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P Q : C ⥤ Type (max w v₁)
f g : P ⟶ Q
h : ∀ (X : Cᵒᵖ) (p : uliftCoyoneda.{w, v₁, u₁}.obj X ⟶ P), p ≫ f = p ≫ g
X : C
x : P.obj X
⊢ (ConcreteCategory.hom (f.app X)).toFun x = (ConcreteCategory.hom (g.app X)).toFun x
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.op Y ⟶ Opposite.op B
g : Opposite.op X ⟶ Opposite.op A
sq : CommSq f p.op i.op g
⊢ sq.HasLift

Tactic:
by
    simp only [CommSq.HasLift.iff_unop, Quiver.Hom.unop_op]
    infer_instance

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

Goal state before:
pp: 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✝ Y✝ : WidePullbackShape ι
f : X✝ ⟶ Y✝
⊢ F.map f ≫
      (match Y✝ with
        | none => base
        | some i => comp i).hom =
    (match X✝ with
        | none => base
        | some i => comp i).hom ≫
      G.map f

Tactic:
rcases f <;> 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
ι : Type u_1
f : ι → Type u_2
g : (i : ι) → f i → C
inst✝¹ : ∀ (i : ι), HasCoproduct (g i)
inst✝ : HasCoproduct fun i ↦ ∐ g i
⊢ ∀ (t : Cofan fun p ↦ g p.fst p.snd)
    (m : (Cofan.mk (∐ fun i ↦ ∐ g i) fun X ↦ Sigma.ι (g X.fst) X.snd ≫ Sigma.ι (fun i ↦ ∐ g i) X.fst).pt ⟶ t.pt),
    (∀ (j : (i : ι) × f i),
        (Cofan.mk (∐ fun i ↦ ∐ g i) fun X ↦ Sigma.ι (g X.fst) X.snd ≫ Sigma.ι (fun i ↦ ∐ g i) X.fst).inj j ≫ m =
          t.inj j) →
      m = Sigma.desc fun b ↦ Sigma.desc fun c ↦ t.inj ⟨b, c⟩

Tactic:
intro s (m : (∐ fun i ↦ ∐ g i) ⟶ _) w; aesop_cat (add norm simp Sigma.forall)

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

Goal state before:
pp: case desc
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y X' : C
c : BinaryCofan X Y
f : X' ⟶ X
inst✝ : IsIso f
h : IsColimit c
⊢ (s : BinaryCofan X' ((pair X Y).obj { as := right })) →
    ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left } ⟶ s.pt

pp: case fac_left
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y X' : C
c : BinaryCofan X Y
f : X' ⟶ X
inst✝ : IsIso f
h : IsColimit c
⊢ ∀ (s : BinaryCofan X' ((pair X Y).obj { as := right })), (f ≫ c.inl) ≫ ?desc s = s.inl

pp: case fac_right
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y X' : C
c : BinaryCofan X Y
f : X' ⟶ X
inst✝ : IsIso f
h : IsColimit c
⊢ ∀ (s : BinaryCofan X' ((pair X Y).obj { as := right })), c.inr ≫ ?desc s = s.inr

pp: case uniq
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y X' : C
c : BinaryCofan X Y
f : X' ⟶ X
inst✝ : IsIso f
h : IsColimit c
⊢ ∀ (s : BinaryCofan X' ((pair X Y).obj { as := right }))
    (m : ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left } ⟶ s.pt),
    (f ≫ c.inl) ≫ m = s.inl → c.inr ≫ m = s.inr → m = ?desc s

Tactic:
· exact fun s => BinaryCofan.IsColimit.desc h (inv f ≫ s.inl) s.inr

Goal state after:
case fac_left
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y X' : C
c : BinaryCofan X Y
f : X' ⟶ X
inst✝ : IsIso f
h : IsColimit c
⊢ ∀ (s : BinaryCofan X' ((pair X Y).obj { as := right })), (f ≫ c.inl) ≫ IsColimit.desc h (inv f ≫ s.inl) s.inr = s.inl

case fac_right
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y X' : C
c : BinaryCofan X Y
f : X' ⟶ X
inst✝ : IsIso f
h : IsColimit c
⊢ ∀ (s : BinaryCofan X' ((pair X Y).obj { as := right })), c.inr ≫ IsColimit.desc h (inv f ≫ s.inl) s.inr = s.inr

case uniq
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y X' : C
c : BinaryCofan X Y
f : X' ⟶ X
inst✝ : IsIso f
h : IsColimit c
⊢ ∀ (s : BinaryCofan X' ((pair X Y).obj { as := right }))
    (m : ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left } ⟶ s.pt),
    (f ≫ c.inl) ≫ m = s.inl → c.inr ≫ m = s.inr → m = IsColimit.desc h (inv f ≫ s.inl) s.inr
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
W✝ X✝ Y✝ Z✝ W X Y Z S T : C
f₁ : S ⟶ W
f₂ : S ⟶ X
inst✝¹ : HasPushout f₁ f₂
g₁ : T ⟶ Y
g₂ : T ⟶ Z
inst✝ : HasPushout g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₁ = i₃ ≫ g₁
eq₂ : f₂ ≫ i₂ = i₃ ≫ g₂
⊢ f₁ ≫ i₁ ≫ inl g₁ g₂ = f₂ ≫ i₂ ≫ inr g₁ g₂

Tactic:
by simp only [reassoc_of% eq₁, reassoc_of% eq₂, condition]

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

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

pp: case h_map
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X Y Z : T
f : X ⟶ Y
g : Y ⟶ Z
⊢ autoParam
    (∀ (X_1 Y_1 : Under Z) (f_1 : X_1 ⟶ Y_1), (map (f ≫ g)).map f_1 = eqToHom ⋯ ≫ (map g ⋙ map f).map f_1 ≫ eqToHom ⋯)
    Functor.ext._auto_1

Tactic:
· simp [Under.map, Comma.mapLeft]

Goal state after:
case h_map
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X Y Z : T
f : X ⟶ Y
g : Y ⟶ Z
⊢ autoParam
    (∀ (X_1 Y_1 : Under Z) (f_1 : X_1 ⟶ Y_1), (map (f ≫ g)).map f_1 = eqToHom ⋯ ≫ (map g ⋙ map f).map f_1 ≫ eqToHom ⋯)
    Functor.ext._auto_1
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
Y : Under X
⊢ Hom.right (mkIdInitial.to Y) = Y.hom

Tactic:
rw [mkIdInitial.hom_ext (mkIdInitial.to Y) (homMk Y.hom)]
  rfl

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasImages C
inst✝¹ : HasPullbacks C
inst✝ : HasEqualizers C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
A B : C
h : A ⟶ B
h_mono : Mono h
x : X✝ ⟶ A
y : image f ⟶ B
sq : CommSq x (factorThruImage f) h y
⊢ factorThruImage f ≫
      image.lift
          { I := pullback h y, m := pullback.snd h y ≫ image.ι f, m_mono := ⋯,
            e := pullback.lift x (factorThruImage f) ⋯, fac := ⋯ } ≫
        pullback.fst h y =
    x

Tactic:
by simp only [image.fac_lift_assoc, pullback.lift_fst]

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)
⊢ (s'.ι ≫ h) ≫ f = (s'.ι ≫ h) ≫ g

Tactic:
simp [s'.condition]

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

Goal state before:
pp: case calc_1
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
inst✝¹ : HasZeroMorphisms E
G : C ⥤ D
inst✝ : G.IsRightAdjoint
X Y : C
adj : G.leftAdjoint ⊣ G := Adjunction.ofIsRightAdjoint G
⊢ G.map 0 = adj.unit.app (G.obj X) ≫ G.map (adj.counit.app X) ≫ G.map 0

Tactic:
rw [Adjunction.right_triangle_components_assoc]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryCoproduct X Y
Z✝ : C
x✝¹ x✝ : X ⟶ Z✝
e : coprod.fst X Y ≫ x✝¹ = coprod.fst X Y ≫ x✝
⊢ x✝¹ = x✝

Tactic:
simpa using congrArg (coprod.inl ≫ ·) e

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
⊢ PreservesColimitsOfShape J F

Tactic:
let : Category (ULiftHom (ULift J)) := ULiftHom.category
        have := h (ULiftHom (ULift J)) CategoryTheory.finCategoryUlift
        exact preservesColimitsOfShape_of_equiv (ULiftHomULiftCategory.equiv J).symm F

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 g : J → C
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
p : (b : J) → f b ⟶ g b
⊢ map p = map' p

Tactic:
ext
  simp only [Discrete.natTrans_app, Limits.IsColimit.ι_map_assoc, Limits.IsLimit.map_π,
    ← Bicone.toCone_π_app_mk, ← Bicone.toCocone_ι_app_mk]
  dsimp
  rw [biproduct.ι_π_assoc, biproduct.ι_π]
  split_ifs with h
  · subst h; simp
  · simp

Goal state after:
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✝ : IsSplitEpi f
c : KernelFork f
i : IsLimit c
⊢ (Fork.ι c ≫
      let c' := KernelFork.ofι (Fork.ι c) ⋯;
      let i' := isKernelCompMono i (section_ f) ⋯;
      let i'' := isLimitForkOfKernelFork i';
      (splitMonoOfIdempotentOfIsLimitFork C ⋯ i'').retraction) =
    𝟙 c.pt

Tactic:
by apply SplitMono.id

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

Goal state before:
pp: case refine_1
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
n✝ : μ
s : Finset ι
n : μ
e : ↥s ≃ Fin #s
⊢ Injective fun f i ↦ if hi : i ∈ s then f (e ⟨i, hi⟩) else 0

Tactic:
rw [Injective]
    rintro f g hfg
    ext i
    simpa using congr_fun hfg (e.symm i)

Goal state after:
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 : ι →₀ μ
hf : f.support ⊆ s
⊢ s.sum ⇑f = n ↔ (f.sum fun x x_1 ↦ x_1) = n

Tactic:
rw [sum_of_support_subset (N := μ) f hf (fun _ x ↦ x) fun _ _ ↦ rfl]

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

Goal state before:
pp: n : ℕ
σ : Type u_1
s : Sym σ n
inst✝ : DecidableEq σ
⊢ ∀ {i : ℕ}, i ∈ map (fun a ↦ count a ↑s) (↑s).dedup → 0 < i

Tactic:
by simp [Multiset.count_pos]

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

Goal state before:
pp: α : Type u_1
f : Perm α
x : α
hfx : f x = x
n : ℕ
⊢ (f ^ n) x = x

Tactic:
pow_apply_eq_self_of_apply_eq_self hfx n

Goal state after:
α : Type u_1
f : Perm α
x : α
hfx : f x = x
n : ℕ
⊢ x = x
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: n : ℕ
c : Composition n
x : (i : Fin c.length) × Fin (c.blocksFun i)
⊢ (fun j ↦ ⟨c.index j, c.invEmbedding j⟩) ((fun x ↦ (c.embedding x.fst) x.snd) x) = x

Tactic:
rcases x with ⟨i, y⟩

Goal state after:
n : ℕ
c : Composition n
i : Fin c.length
y : Fin (c.blocksFun i)
⊢ (fun j ↦ ⟨c.index j, c.invEmbedding j⟩) ((fun x ↦ (c.embedding x.fst) x.snd) ⟨i, y⟩) = ⟨i, y⟩
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: n i : ℕ
⊢ (ones n).sizeUpTo i = min i n

Tactic:
by
  simp [sizeUpTo, ones_blocks, take_replicate]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x : α
hf : f x = x
hg : g x = x
⊢ f (g x) = x

Tactic:
hg,

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x : α
hf : f x = x
hg : g x = x
⊢ f x = x
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
inst✝⁶ : Preadditive C
D : Type u'
inst✝⁵ : Category.{v', u'} D
inst✝⁴ : Preadditive D
F : C ⥤ D
inst✝³ : F.PreservesZeroMorphisms
X Y : C
inst✝² : HasBinaryBiproduct X Y
inst✝¹ : HasBinaryBiproduct (F.obj X) (F.obj Y)
inst✝ : Epi (F.biprodComparison' X Y)
this : Epi (F.splitEpiBiprodComparison X Y).section_
⊢ PreservesBinaryBiproduct X Y F

Tactic:
have : IsIso (biprodComparison F X Y) :=
    IsIso.of_epi_section' (splitEpiBiprodComparison F X Y)

Goal state after:
C : Type u
inst✝⁷ : Category.{v, u} C
inst✝⁶ : Preadditive C
D : Type u'
inst✝⁵ : Category.{v', u'} D
inst✝⁴ : Preadditive D
F : C ⥤ D
inst✝³ : F.PreservesZeroMorphisms
X Y : C
inst✝² : HasBinaryBiproduct X Y
inst✝¹ : HasBinaryBiproduct (F.obj X) (F.obj Y)
inst✝ : Epi (F.biprodComparison' X Y)
this✝ : Epi (F.splitEpiBiprodComparison X Y).section_
this : IsIso (F.biprodComparison X Y)
⊢ PreservesBinaryBiproduct X Y F
Module: Mathlib.Algebra.Order.Antidiag.Finsupp

Goal state before:
pp: ι : Type u_1
μ : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : DecidableEq μ
inst✝³ : AddCommMonoid μ
inst✝² : PartialOrder μ
inst✝¹ : CanonicallyOrderedAdd μ
inst✝ : HasAntidiagonal μ
s : Finset ι
f : ι →₀ μ
⊢ f ∈ s.finsuppAntidiag 0 ↔ f ∈ {0}

Tactic:
simp [finsuppAntidiag, ← DFunLike.coe_fn_eq (g := f), eq_comm]

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

Goal state before:
pp: n✝ : ℕ
c✝ : Composition n✝
m : ℕ
motive : (n : ℕ) → Composition n → Sort u_1
n : ℕ
c : Composition n
zero : motive 0 (ones 0)
single_append : (k n : ℕ) → (c : Composition n) → motive n c → motive (k + 1 + n) ((single (k + 1) ⋯).append c)
blocks tail✝ : List ℕ
blocks_pos : ∀ {i : ℕ}, i ∈ 0 :: tail✝ → 0 < i
⊢ motive (0 :: tail✝).sum { blocks := 0 :: tail✝, blocks_pos := blocks_pos, blocks_sum := ⋯ }

Tactic:
simp at blocks_pos

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
A : i < c.blocks.length
B : i < c.boundaries.card
⊢ (take (i + 1) c.blocks).sum = ↑(c.boundary ⟨i + 1, h⟩)

Tactic:
rw [sum_take_succ _ _ A, IH B]

Goal state after:
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
A : i < c.blocks.length
B : i < c.boundaries.card
⊢ ↑(c.boundary ⟨i, B⟩) + c.blocks[i] = ↑(c.boundary ⟨i + 1, h⟩)
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
i : ℕ
hi : i < c.boundaries.card
H : (take i c.blocks).sum = ↑j
this : c.boundary ⟨i, hi⟩ = j
⊢ j = ↑((c.boundaries.orderIsoOfFin ⋯) ⟨i, hi⟩)

Tactic:
exact this.symm

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

Goal state before:
pp: n : ℕ
c : CompositionAsSet n
⊢ ∀ {i : ℕ}, i ∈ c.blocks → 0 < i

Tactic:
by simp only [blocks, forall_mem_ofFn_iff, blocksFun_pos c, forall_true_iff]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x y : α
hxy : x ≠ y
⊢ (x ::ₘ y ::ₘ 0).Nodup

Tactic:
by simp [hxy]

Goal state after:
Module: Mathlib.Data.List.Iterate

Goal state before:
pp: α : Type u_1
f : α → α
a : α
n : ℕ
⊢ (iterate f a n).length = 0 ↔ n = 0

Tactic:
length_iterate

Goal state after:
α : Type u_1
f : α → α
a : α
n : ℕ
⊢ n = 0 ↔ n = 0
Module: Mathlib.Data.List.Iterate

Goal state before:
pp: α : Type u_1
f : α → α
a : α
n i : ℕ
h : i < (iterate f a n).length
⊢ i < n

Tactic:
length_iterate

Goal state after:
α : Type u_1
f : α → α
a : α
n i : ℕ
h : i < n
⊢ i < n
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
inst✝ : Finite α
f g : Perm α
s : Multiset α
hs : ∀ (x : α), x ∈ s
n : ℕ
e : α ≃ Fin n
⊢ (f * g).signAux3 hs = f.signAux3 hs * g.signAux3 hs ∧ Pairwise fun x y ↦ (swap x y).signAux3 hs = -1

Tactic:
induction s using Quotient.inductionOn with

Goal state after:
case h
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Finite α
f g : Perm α
n : ℕ
e : α ≃ Fin n
l : List α
hs : ∀ (x : α), x ∈ ⟦l⟧
⊢ (f * g).signAux3 hs = f.signAux3 hs * g.signAux3 hs ∧ Pairwise fun x y ↦ (swap x y).signAux3 hs = -1
Module: Mathlib.Data.List.Iterate

Goal state before:
pp: α : Type u_1
f : α → α
a : α
m n : ℕ
⊢ iterate f a (m + n) = iterate f a m ++ iterate f (f^[m] a) n

Tactic:
induction m generalizing a with

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

Goal state before:
pp: α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : Perm α
g : Perm β
e : α ≃ β
h : ∀ (x : α), e (f x) = g (e x)
hg : g = (e.symm.trans f).trans e
⊢ sign f = sign g

Tactic:
hg,

Goal state after:
α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : Perm α
g : Perm β
e : α ≃ β
h : ∀ (x : α), e (f x) = g (e x)
hg : g = (e.symm.trans f).trans e
⊢ sign f = sign ((e.symm.trans f).trans e)
Module: Mathlib.GroupTheory.NoncommPiCoprod

Goal state before:
pp: case intro
G : Type u_1
inst✝³ : Group G
ι : Type u_2
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : Pairwise fun i j ↦ ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : Pairwise fun i j ↦ (Fintype.card (H i)).Coprime (Fintype.card (H j))
val✝ : Fintype ι
this : DecidableEq ι := Classical.decEq ι
i : ι
f : G
hxi : f ∈ ↑((fun i ↦ (ϕ i).range) i).toSubmonoid
hxp : f ∈ ↑(⨆ j, ⨆ (_ : j ≠ i), (fun i ↦ (ϕ i).range) j).toSubmonoid
⊢ f ∈ ⊥

Tactic:
dsimp at hxi hxp

Goal state after:
case intro
G : Type u_1
inst✝³ : Group G
ι : Type u_2
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : Pairwise fun i j ↦ ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : Pairwise fun i j ↦ (Fintype.card (H i)).Coprime (Fintype.card (H j))
val✝ : Fintype ι
this : DecidableEq ι := Classical.decEq ι
i : ι
f : G
hxi : f ∈ Set.range ⇑(ϕ i)
hxp : f ∈ ↑(⨆ j, ⨆ (_ : ¬j = i), (ϕ j).range)
⊢ f ∈ ⊥