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

Goal state before:
pp: case hpostcomp
C : Type u
inst✝ : Category.{v, u} C
X Y : C
⊢ ∀ {Z : C} (e : Y ≅ Z) (f : X ⟶ Y), MorphismProperty.epimorphisms C f → MorphismProperty.epimorphisms C (f ≫ e.hom)

Tactic:
Z

Goal state after:
case hpostcomp
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
⊢ ∀ (e : Y ≅ Z) (f : X ⟶ Y), MorphismProperty.epimorphisms C f → MorphismProperty.epimorphisms C (f ≫ e.hom)
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: case hprecomp
C : Type u
inst✝ : Category.{v, u} C
X Y : C
⊢ ∀ {Z : C} (e : X ≅ Y) (f : Y ⟶ Z), MorphismProperty.isomorphisms C f → MorphismProperty.isomorphisms C (e.hom ≫ f)

Tactic:
Z

Goal state after:
case hprecomp
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
⊢ ∀ (e : X ≅ Y) (f : Y ⟶ Z), MorphismProperty.isomorphisms C f → MorphismProperty.isomorphisms C (e.hom ≫ f)
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: case hpostcomp
C : Type u
inst✝ : Category.{v, u} C
X Y : C
⊢ ∀ {Z : C} (e : Y ≅ Z) (f : X ⟶ Y), MorphismProperty.isomorphisms C f → MorphismProperty.isomorphisms C (f ≫ e.hom)

Tactic:
Z

Goal state after:
case hpostcomp
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
⊢ ∀ (e : Y ≅ Z) (f : X ⟶ Y), MorphismProperty.isomorphisms C f → MorphismProperty.isomorphisms C (f ≫ e.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
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝ : F.IsEquivalence
⊢ (F ⋙ G).IsLeftAdjoint ↔ G.IsLeftAdjoint

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 isLeftAdjoint_of_iso iso.symm

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : Cᵒᵖ
Y : Cᵒᵖ ⥤ Type v₁
⊢ ∀ {Y_1 : Cᵒᵖ ⥤ Type v₁} (f : Y ⟶ Y_1),
    ((yoneda.op ⋙ coyoneda).obj X).map f ≫ (yonedaEquiv.trans Equiv.ulift.symm).toIso.hom =
      (yonedaEquiv.trans Equiv.ulift.symm).toIso.hom ≫
        ((evaluation Cᵒᵖ (Type v₁) ⋙
                  (whiskeringRight (Cᵒᵖ ⥤ Type v₁) (Type v₁) (Type (max u₁ v₁))).obj uliftFunctor.{u₁, v₁}).obj
              X).map
          f

Tactic:
Z

Goal state after:
C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : Cᵒᵖ
Y Z : Cᵒᵖ ⥤ Type v₁
⊢ ∀ (f : Y ⟶ Z),
    ((yoneda.op ⋙ coyoneda).obj X).map f ≫ (yonedaEquiv.trans Equiv.ulift.symm).toIso.hom =
      (yonedaEquiv.trans Equiv.ulift.symm).toIso.hom ≫
        ((evaluation Cᵒᵖ (Type v₁) ⋙
                  (whiskeringRight (Cᵒᵖ ⥤ Type v₁) (Type v₁) (Type (max u₁ v₁))).obj uliftFunctor.{u₁, v₁}).obj
              X).map
          f
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Y : Cᵒᵖ
⊢ ∀ {Y_1 : Cᵒᵖ} (f : Y ⟶ Y_1),
    (yoneda.op ⋙ coyoneda).map f ≫ (NatIso.ofComponents (fun x ↦ (yonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯).hom =
      (NatIso.ofComponents (fun x ↦ (yonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯).hom ≫
        (evaluation Cᵒᵖ (Type v₁) ⋙
              (whiskeringRight (Cᵒᵖ ⥤ Type v₁) (Type v₁) (Type (max u₁ v₁))).obj uliftFunctor.{u₁, v₁}).map
          f

Tactic:
Z

Goal state after:
C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Y Z : Cᵒᵖ
⊢ ∀ (f : Y ⟶ Z),
    (yoneda.op ⋙ coyoneda).map f ≫ (NatIso.ofComponents (fun x ↦ (yonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯).hom =
      (NatIso.ofComponents (fun x ↦ (yonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯).hom ≫
        (evaluation Cᵒᵖ (Type v₁) ⋙
              (whiskeringRight (Cᵒᵖ ⥤ Type v₁) (Type v₁) (Type (max u₁ v₁))).obj uliftFunctor.{u₁, v₁}).map
          f
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : Category.{v₁, u₁} C
⊢ ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y),
    (uliftYoneda.{w, v₁, u₁}.op ⋙ coyoneda).map f ≫
        (NatIso.ofComponents (fun x ↦ (uliftYonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯).hom =
      (NatIso.ofComponents (fun x ↦ (uliftYonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯).hom ≫
        (evaluation Cᵒᵖ (Type (max v₁ w)) ⋙
              (whiskeringRight (Cᵒᵖ ⥤ Type (max v₁ w)) (Type (max v₁ w)) (Type (max (max w u₁) v₁))).obj
                uliftFunctor.{u₁, max v₁ w}).map
          f

Tactic:
by
      intros Y Z f
      ext F g
      rw [← ULift.down_inj]
      simpa using (uliftYonedaEquiv_naturality _ _).symm

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
Y : C ⥤ Type v₁
⊢ ∀ {Y_1 : C ⥤ Type v₁} (f : Y ⟶ Y_1),
    ((coyoneda.rightOp ⋙ coyoneda).obj X).map f ≫ (coyonedaEquiv.trans Equiv.ulift.symm).toIso.hom =
      (coyonedaEquiv.trans Equiv.ulift.symm).toIso.hom ≫
        ((evaluation C (Type v₁) ⋙
                  (whiskeringRight (C ⥤ Type v₁) (Type v₁) (Type (max u₁ v₁))).obj uliftFunctor.{u₁, v₁}).obj
              X).map
          f

Tactic:
Z

Goal state after:
C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
Y Z : C ⥤ Type v₁
⊢ ∀ (f : Y ⟶ Z),
    ((coyoneda.rightOp ⋙ coyoneda).obj X).map f ≫ (coyonedaEquiv.trans Equiv.ulift.symm).toIso.hom =
      (coyonedaEquiv.trans Equiv.ulift.symm).toIso.hom ≫
        ((evaluation C (Type v₁) ⋙
                  (whiskeringRight (C ⥤ Type v₁) (Type v₁) (Type (max u₁ v₁))).obj uliftFunctor.{u₁, v₁}).obj
              X).map
          f
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Y : C
⊢ ∀ {Y_1 : C} (f : Y ⟶ Y_1),
    (coyoneda.rightOp ⋙ coyoneda).map f ≫
        (NatIso.ofComponents (fun x ↦ (coyonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯).hom =
      (NatIso.ofComponents (fun x ↦ (coyonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯).hom ≫
        (evaluation C (Type v₁) ⋙
              (whiskeringRight (C ⥤ Type v₁) (Type v₁) (Type (max u₁ v₁))).obj uliftFunctor.{u₁, v₁}).map
          f

Tactic:
Z

Goal state after:
C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Y Z : C
⊢ ∀ (f : Y ⟶ Z),
    (coyoneda.rightOp ⋙ coyoneda).map f ≫
        (NatIso.ofComponents (fun x ↦ (coyonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯).hom =
      (NatIso.ofComponents (fun x ↦ (coyonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯).hom ≫
        (evaluation C (Type v₁) ⋙
              (whiskeringRight (C ⥤ Type v₁) (Type v₁) (Type (max u₁ v₁))).obj uliftFunctor.{u₁, v₁}).map
          f
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
hf : ∀ (T : C), Function.Bijective fun x ↦ f ≫ x
⊢ IsIso f

Tactic:
by
  obtain ⟨g, hg : f ≫ g = 𝟙 X⟩ := (hf X).2 (𝟙 X)
  refine ⟨g, hg, (hf _).1 ?_⟩
  simp only [Category.comp_id, ← Category.assoc, hg, Category.id_comp]

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 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
⊢ sq.HasLift

Tactic:
have fac := sq.w
    rw [assoc] at fac
    exact
      CommSq.HasLift.mk'
        { l := (CommSq.mk (CommSq.mk fac).fac_right).lift
          fac_left := by simp only [assoc, CommSq.fac_left]
          fac_right := by simp only [CommSq.fac_right] }

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
G : K ⥤ C
inst✝ : HasColimit G
e : J ≌ K
w : e.functor ⋙ G ≅ F
j : J
⊢ colimit.ι F j ≫ (isoOfEquivalence e w).hom =
    F.map (e.unit.app j) ≫
      w.inv.app ((e.functor ⋙ e.inverse).obj j) ≫ colimit.ι G (e.functor.obj ((e.functor ⋙ e.inverse).obj j))

Tactic:
simp [HasColimit.isoOfEquivalence]

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

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

Tactic:
dsimp
    rw [← P.uniq s.op m.op]
    · rfl
    · dsimp
      intro j
      rw [← w]
      rfl

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

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

Tactic:
dsimp
    rw [← P.uniq s.op m.op]
    · rfl
    · dsimp
      intro j
      rw [← w]
      rfl

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
s : BinaryCofan X Y
desc : {T : C} → (X ⟶ T) → (Y ⟶ T) → (s.pt ⟶ T)
hd₁ : ∀ {T : C} (f : X ⟶ T) (g : Y ⟶ T), s.inl ≫ desc f g = f
hd₂ : ∀ {T : C} (f : X ⟶ T) (g : Y ⟶ T), s.inr ≫ desc f g = g
uniq : ∀ {T : C} (f : X ⟶ T) (g : Y ⟶ T) (m : s.pt ⟶ T), s.inl ≫ m = f → s.inr ≫ m = g → m = desc f g
⊢ ∀ (s_1 : Cocone (pair X Y)) (j : Discrete WalkingPair), s.ι.app j ≫ desc (inl s_1) (inr s_1) = s_1.ι.app j

Tactic:
rintro t (rfl | rfl)
      · exact hd₁ _ _
      · exact hd₂ _ _

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : WalkingCospan ⥤ C
j : WalkingCospan
⊢ F.obj j = (cospan (F.map inl) (F.map inr)).obj j

Tactic:
rcases j with (⟨⟩ | ⟨⟨⟩⟩)

Goal state after:
case none
C : Type u
inst✝ : Category.{v, u} C
F : WalkingCospan ⥤ C
⊢ F.obj none = (cospan (F.map inl) (F.map inr)).obj none

case some.left
C : Type u
inst✝ : Category.{v, u} C
F : WalkingCospan ⥤ C
⊢ F.obj (some WalkingPair.left) = (cospan (F.map inl) (F.map inr)).obj (some WalkingPair.left)

case some.right
C : Type u
inst✝ : Category.{v, u} C
F : WalkingCospan ⥤ C
⊢ F.obj (some WalkingPair.right) = (cospan (F.map inl) (F.map inr)).obj (some WalkingPair.right)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : WalkingSpan ⥤ C
j : WalkingSpan
⊢ F.obj j = (span (F.map fst) (F.map snd)).obj j

Tactic:
rcases j with (⟨⟩ | ⟨⟨⟩⟩)

Goal state after:
case none
C : Type u
inst✝ : Category.{v, u} C
F : WalkingSpan ⥤ C
⊢ F.obj none = (span (F.map fst) (F.map snd)).obj none

case some.left
C : Type u
inst✝ : Category.{v, u} C
F : WalkingSpan ⥤ C
⊢ F.obj (some WalkingPair.left) = (span (F.map fst) (F.map snd)).obj (some WalkingPair.left)

case some.right
C : Type u
inst✝ : Category.{v, u} C
F : WalkingSpan ⥤ C
⊢ F.obj (some WalkingPair.right) = (span (F.map fst) (F.map snd)).obj (some WalkingPair.right)
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
hY : IsZero Y
e : X ≅ Y
⊢ IsZero X

Tactic:
refine ⟨fun Z => ⟨⟨⟨e.hom ≫ hY.to_ Z⟩, fun f => ?_⟩⟩,
    fun Z => ⟨⟨⟨hY.from_ Z ≫ e.inv⟩, fun f => ?_⟩⟩⟩
  · rw [← cancel_epi e.inv]
    apply hY.eq_of_src
  · rw [← cancel_mono e.hom]
    apply hY.eq_of_tgt

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
X Y : Discrete PUnit.{?u.10 + 1}
⊢ Zero (X ⟶ Y)

Tactic:
repeat (constructor)

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : Mono g
h✝ : f ≫ g = 0
h : f = 0
⊢ f = 0

Tactic:
exact h

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : Epi f
h✝ : f ≫ g = 0
h : g = 0
⊢ g = 0

Tactic:
exact h

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
f g h : Arrow C
inst✝⁴ : HasImage f.hom
inst✝³ : HasImage g.hom
inst✝² : HasImage h.hom
sq1 : f ⟶ g
sq2 : g ⟶ h
inst✝¹ : HasImageMap sq1
inst✝ : HasImageMap sq2
⊢ ((imageMap sq1).map ≫ (imageMap sq2).map) ≫ image.ι h.hom = image.ι f.hom ≫ Arrow.Hom.right (sq1 ≫ sq2)

Tactic:
by
        rw [Category.assoc, ImageMap.map_ι, ImageMap.map_ι_assoc, Arrow.comp_right]

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
O : C
hO : IsZero O
X Y Z : C
f : Y ⟶ Z
⊢ 0 ≫ f = 0

Tactic:
change (hO.from_ X ≫ hO.to_ Y) ≫ f = hO.from_ X ≫ hO.to_ Z
    rw [Category.assoc]
    congr
    apply hO.eq_of_src

Goal state after:
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₁ K₂ : J ⥤ C
F : C ⥤ D
h : K₁ ≅ K₂
inst✝ : PreservesLimit K₁ F
c : Cone K₂
t : IsLimit c
⊢ IsLimit (F.mapCone c)

Tactic:
apply IsLimit.postcomposeInvEquiv (Functor.isoWhiskerRight h F :) _ _
    have := (IsLimit.postcomposeInvEquiv h c).symm t
    apply IsLimit.ofIsoLimit (isLimitOfPreserves F this)
    exact Cone.ext (Iso.refl _)

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 c : β
⊢ ι f b ≫ π f c = if h : b = c then eqToHom ⋯ else 0

Tactic:
grind [CategoryTheory.eqToHom_refl]

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✝ : HasCoproduct f
b c : β
⊢ ι f b ≫ π f c = if h : b = c then eqToHom ⋯ else 0

Tactic:
grind [CategoryTheory.eqToHom_refl]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
f : X ⟶ Y
c : CokernelCofork f
hc : IsColimit c
h : IsZero c.pt
R✝ : C
g : Y ⟶ R✝
hg : f ≫ g = 0
⊢ g = 0

Tactic:
obtain ⟨a, ha⟩ := CokernelCofork.IsColimit.desc' hc _ hg
  rw [← ha, h.eq_of_src a 0, Limits.comp_zero]

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

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

Tactic:
exact h

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

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

Tactic:
subst h
    simp

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

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

Tactic:
exact h

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

Goal state before:
pp: n : ℕ
c : Composition n
⊢ (↑c.blocks).sum = n

Tactic:
by rw [Multiset.sum_coe, c.blocks_sum]

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

Goal state before:
pp: n : ℕ
c : Composition n
j : Fin n
H : ↑j < c.sizeUpTo ↑(c.index j)
⊢ False

Tactic:
set i := c.index j

Goal state after:
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length := c.index j
H : ↑j < c.sizeUpTo ↑i
⊢ False
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
W X Y Z : C
f : W ⊞ X ⟶ Y ⊞ Z
inst✝ : IsIso f
⊢ 𝟙 W = 0 ∨ biprod.inl ≫ f ≫ biprod.fst ≠ 0 ∨ biprod.inl ≫ f ≫ biprod.snd ≠ 0

Tactic:
by_contra! ⟨nz, a₁, a₂⟩
  set x := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
  have h₁ : x = 𝟙 W := by simp [x]
  have h₀ : x = 0 := by
    dsimp [x]
    rw [← Category.id_comp (inv f), Category.assoc, ← biprod.total]
    conv_lhs =>
      slice 2 3
      rw [comp_add]
    simp only [Category.assoc]
    rw [comp_add_assoc, add_comp]
    conv_lhs =>
      congr
      next => skip
      slice 1 3
      rw [a₂]
    simp only [zero_comp, add_zero]
    conv_lhs =>
      slice 1 3
      rw [a₁]
    simp only [zero_comp]
  exact nz (h₁.symm.trans h₀)

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

Goal state before:
pp: n : ℕ
c : Composition n
j : Fin n
i : Fin c.length
⊢ j ∈ Set.range ⇑(c.embedding i) ↔ c.sizeUpTo ↑i ≤ ↑j ∧ ↑j < c.sizeUpTo (↑i).succ

Tactic:
by
  constructor
  · intro h
    rcases Set.mem_range.2 h with ⟨k, hk⟩
    rw [Fin.ext_iff] at hk
    dsimp at hk
    rw [← hk]
    simp [sizeUpTo_succ', k.is_lt]
  · intro h
    apply Set.mem_range.2
    refine ⟨⟨j - c.sizeUpTo i, ?_⟩, ?_⟩
    · rw [tsub_lt_iff_left, ← sizeUpTo_succ']
      · exact h.2
      · exact h.1
    · rw [Fin.ext_iff]
      exact add_tsub_cancel_of_le h.1

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

Goal state before:
pp: case e_4
n : ℕ
c : Composition n
i : Fin c.length
y : Fin (c.blocksFun i)
⊢ ↑(c.invEmbedding ((c.embedding i) y)) = ↑y

Tactic:
exact c.invEmbedding_comp _ _

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

Goal state before:
pp: n : ℕ
c : Composition n
H : ¬c = ones n
length_n : c.length = n
⊢ ∑ i, 1 < ∑ i, c.blocksFun i

Tactic:
obtain ⟨i, hi, i_blocks⟩ : ∃ i ∈ c.blocks, 1 < i := ne_ones_iff.1 H

Goal state after:
n : ℕ
c : Composition n
H : ¬c = ones n
length_n : c.length = n
i : ℕ
hi : i ∈ c.blocks
i_blocks : 1 < i
⊢ ∑ i, 1 < ∑ i, c.blocksFun i
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: case mp
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
⊢ Set.MapsTo (⇑σ) (Set.range Sum.inl) (Set.range Sum.inl) → Set.MapsTo (⇑σ) (Set.range Sum.inr) (Set.range Sum.inr)

Tactic:
intro h
      classical
        rw [← perm_symm_mapsTo_iff_mapsTo] at h
        intro x
        rcases hx : σ x with l | r

Goal state after:
case mp.inl
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (⇑(Equiv.symm σ)) (Set.range Sum.inl) (Set.range Sum.inl)
x : m ⊕ n
l : m
hx : σ x = Sum.inl l
⊢ x ∈ Set.range Sum.inr → Sum.inl l ∈ Set.range Sum.inr

case mp.inr
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (⇑(Equiv.symm σ)) (Set.range Sum.inl) (Set.range Sum.inl)
x : m ⊕ n
r : n
hx : σ x = Sum.inr r
⊢ x ∈ Set.range Sum.inr → Sum.inr r ∈ Set.range Sum.inr
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: case mpr
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
⊢ Set.MapsTo (⇑σ) (Set.range Sum.inr) (Set.range Sum.inr) → Set.MapsTo (⇑σ) (Set.range Sum.inl) (Set.range Sum.inl)

Tactic:
intro h
      classical
        rw [← perm_symm_mapsTo_iff_mapsTo] at h
        intro x
        rcases hx : σ x with l | r

Goal state after:
case mpr.inl
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (⇑(Equiv.symm σ)) (Set.range Sum.inr) (Set.range Sum.inr)
x : m ⊕ n
l : m
hx : σ x = Sum.inl l
⊢ x ∈ Set.range Sum.inl → Sum.inl l ∈ Set.range Sum.inl

case mpr.inr
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (⇑(Equiv.symm σ)) (Set.range Sum.inr) (Set.range Sum.inr)
x : m ⊕ n
r : n
hx : σ x = Sum.inr r
⊢ x ∈ Set.range Sum.inl → Sum.inr r ∈ Set.range Sum.inl
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x : α
h : f (f x) ≠ x
⊢ (swap x (f x) * f).support = f.support \ {x}

Tactic:
by_cases hx : f x = x

Goal state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x : α
h : f (f x) ≠ x
hx : f x = x
⊢ (swap x (f x) * f).support = f.support \ {x}

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x : α
h : f (f x) ≠ x
hx : ¬f x = x
⊢ (swap x (f x) * f).support = f.support \ {x}
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : f.IsSwap
⊢ #f.support = 2

Tactic:
· obtain ⟨x, y, hxy, rfl⟩ := h
    exact card_support_swap hxy

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

Goal state before:
pp: u : ℤˣ
n : ℕ
| u ^ n = u ^ (n % 2)

Tactic:
lhs
    rw [← Nat.mod_add_div n 2]
    rw [pow_add, pow_mul, units_sq, one_pow, mul_one]

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

Goal state before:
pp: case inr
n : ℕ
i j : Fin (n + 1)
ne : i ≠ j
this : ∀ (i j : Fin (n + 1)), i ≠ j → i < j → swap i j ∈ ↑(Submonoid.closure (Set.range fun i ↦ swap i.castSucc i.succ))
lt : ¬i < j
⊢ swap i j ∈ ↑(Submonoid.closure (Set.range fun i ↦ swap i.castSucc i.succ))

Tactic:
swap_comm

Goal state after:
case inr
n : ℕ
i j : Fin (n + 1)
ne : i ≠ j
this : ∀ (i j : Fin (n + 1)), i ≠ j → i < j → swap i j ∈ ↑(Submonoid.closure (Set.range fun i ↦ swap i.castSucc i.succ))
lt : ¬i < j
⊢ swap j i ∈ ↑(Submonoid.closure (Set.range fun i ↦ swap i.castSucc i.succ))
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: n : ℕ
| 1

Tactic:
rw [← @Finset.prod_const_one _ _ (finPairsLT n)]

Goal state after:
n : ℕ
| ∏ _x ∈ finPairsLT n, 1
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f : Perm α
x y : α
hf : f.IsCycle
hx : f x ≠ x
hy : f y ≠ y
g : α
hg : f g ≠ g ∧ ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle g y
a : ℤ
ha : (f ^ a) g = x
b : ℤ
hb : (f ^ b) g = y
⊢ (f ^ (b - a + a)) g = y

Tactic:
sub_add_cancel,

Goal state after:
α : Type u_2
f : Perm α
x y : α
hf : f.IsCycle
hx : f x ≠ x
hy : f y ≠ y
g : α
hg : f g ≠ g ∧ ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle g y
a : ℤ
ha : (f ^ a) g = x
b : ℤ
hb : (f ^ b) g = y
⊢ (f ^ b) g = y
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: case nil.inr
α : Type u_1
inst✝ : DecidableEq α
l' : List α
hl' : l'.Nodup
hl : [].Nodup
h : l'.length ≤ 1
⊢ l'.length ≤ 1

Tactic:
exact h

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

Goal state before:
pp: case cons.nil.inr
α : Type u_1
inst✝ : DecidableEq α
l' : List α
hl' : l'.Nodup
x : α
hl : [x].Nodup
h : l'.length ≤ 1
⊢ l'.length ≤ 1

Tactic:
exact h

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

Goal state before:
pp: case pos
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
H : Subgroup (Perm α) := closure {σ, swap x (σ x)}
h3 : σ ∈ H
h4 : swap x (σ x) ∈ H
step1 : ∀ (n : ℕ), swap ((σ ^ n) x) ((σ ^ (n + 1)) x) ∈ H
step2 : ∀ (n : ℕ), swap x ((σ ^ n) x) ∈ H
step3 : ∀ (y : α), swap x y ∈ H
y z : α
h5 : z = x
⊢ swap y x ∈ H

Tactic:
swap_comm

Goal state after:
case pos
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
H : Subgroup (Perm α) := closure {σ, swap x (σ x)}
h3 : σ ∈ H
h4 : swap x (σ x) ∈ H
step1 : ∀ (n : ℕ), swap ((σ ^ n) x) ((σ ^ (n + 1)) x) ∈ H
step2 : ∀ (n : ℕ), swap x ((σ ^ n) x) ∈ H
step3 : ∀ (y : α), swap x y ∈ H
y z : α
h5 : z = x
⊢ swap x y ∈ H