mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.Quiver.Prefunctor

Goal state before:
pp: U : Type u_1
V : Type u_2
inst✝¹ : Quiver U
inst✝ : Quiver V
F G : U ⥤q V
e : F = G
X : U
⊢ F.obj X = G.obj X

Tactic:
cases e; rfl

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
S : Type v₃
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Algebra R S
R' : Type u_6
S' : Type u_7
inst✝⁸ : CommSemiring R'
inst✝⁷ : CommSemiring S'
inst✝⁶ : Algebra R R'
inst✝⁵ : Algebra S S'
inst✝⁴ : Algebra R' S'
inst✝³ : Algebra R S'
inst✝² : IsScalarTower R R' S'
inst✝¹ : IsScalarTower R S S'
inst✝ : IsPushout R S R' S'
a : R'
⊢ (equiv R S R' S').symm ((algebraMap R' S') a) = 1 ⊗ₜ[R] a

Tactic:
rw [(equiv R S R' S').symm_apply_eq, equiv_tmul, map_one, one_mul]

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Path

Goal state before:
pp: V : Type u
inst✝ : Quiver V
a b : V
p : Path a b
e : b ⟶ a
h : nil = p.cons e
⊢ False

Tactic:
by injection h

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Path

Goal state before:
pp: V : Type u
inst✝ : Quiver V
a b : V
p : Path a b
e : b ⟶ a
h : p.cons e = nil
⊢ False

Tactic:
by injection h

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Path

Goal state before:
pp: V : Type u
inst✝ : Quiver V
a b c d : V
p : Path a b
p' : Path a c
e : b ⟶ d
e' : c ⟶ d
h : p.cons e = p'.cons e'
⊢ b = c

Tactic:
by injection h

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Path

Goal state before:
pp: V : Type u
inst✝ : Quiver V
a b c d : V
p : Path a b
p' : Path a c
e : b ⟶ d
e' : c ⟶ d
h : p.cons e = p'.cons e'
⊢ p ≍ p'

Tactic:
by injection h

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Path

Goal state before:
pp: V : Type u
inst✝ : Quiver V
a b c d : V
p : Path a b
p' : Path a c
e : b ⟶ d
e' : c ⟶ d
h : p.cons e = p'.cons e'
⊢ e ≍ e'

Tactic:
by injection h

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
inst✝ : P.IsClosedUnderIsomorphisms
⊢ P.isoClosure = P

Tactic:
by
  apply le_antisymm
  · intro X ⟨Y, hY, ⟨e⟩⟩
    exact prop_of_iso P e.symm hY
  · exact le_isoClosure P

Goal state after:
Module: Mathlib.CategoryTheory.EssentialImage

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
⊢ ⊤.map F = F.essImage

Tactic:
by
  ext Y
  refine ⟨?_, ?_⟩
  · rintro ⟨X, _, ⟨e⟩⟩
    exact ⟨X, ⟨e⟩⟩
  · rintro ⟨X, ⟨e⟩⟩
    exact ⟨X, by simp, ⟨e⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.Equivalence

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
⊢ e.unit.app (e.inverse.obj Y) ≫
      e.inverse.map (e.functor.map (e.unit.app (e.inverse.obj Y))) ≫
        e.inverse.map (e.functor.map (e.inverse.map (e.counitInv.app (e.functor.obj (e.inverse.obj Y))))) ≫
          (((e.inverse.mapIso (e.counitIso.app (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))).hom ≫
                (e.inverse.mapIso
                      (e.counitIso.app (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))).inv ≫
                  e.unitInv.app (e.inverse.obj (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))) ≫
              e.inverse.map (e.functor.map (e.unitInv.app (e.inverse.obj Y)))) ≫
            e.inverse.map (e.counit.app Y) =
    𝟙 (e.inverse.obj Y)

Tactic:
slice_lhs 3 4 =>
    dsimp only [Functor.mapIso_hom, Iso.app_hom]
    rw [← map_comp e.inverse]
    dsimp
    rw [e.counit_naturality, e.counitIso.hom_inv_id_app]
    dsimp only [Functor.comp_obj]
    rw [map_id]

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
⊢ e.unit.app (e.inverse.obj Y) ≫
      e.inverse.map (e.functor.map (e.unit.app (e.inverse.obj Y))) ≫
        (((𝟙 (e.inverse.obj (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y))))) ≫
                (e.inverse.mapIso
                    (e.counitIso.app (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))).inv) ≫
              e.unitInv.app (e.inverse.obj (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))) ≫
            e.inverse.map (e.functor.map (e.unitInv.app (e.inverse.obj Y)))) ≫
          e.inverse.map (e.counit.app Y) =
    𝟙 (e.inverse.obj Y)
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u_1
inst✝² : Category.{v_1, u_1} D
F : C ⥤ D
inst✝¹ : F.EssSurj
inst✝ : F.Full
⊢ ⊤.map F = ⊤

Tactic:
by
  rw [eq_top_iff]
  intro X Y f _
  refine ⟨F.objPreimage X, F.objPreimage Y, F.preimage ?_, ⟨⟨⟩, ⟨?_⟩⟩⟩
  · exact (Functor.objObjPreimageIso F X).hom ≫ f ≫ (Functor.objObjPreimageIso F Y).inv
  · exact Arrow.isoMk' _ _ (Functor.objObjPreimageIso F X) (Functor.objObjPreimageIso F Y)
      (by simp)

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
inst✝ : P.RespectsIso
⊢ P.isoClosure = P

Tactic:
isoClosure_eq_iff

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
inst✝ : P.RespectsIso
⊢ P.RespectsIso
Module: Mathlib.CategoryTheory.Yoneda

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

Tactic:
rw [uliftYonedaEquiv_comp]

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F G : Cᵒᵖ ⥤ Type (max w v₁)
X : Cᵒᵖ
x : F.obj X
f : F ⟶ G
⊢ (ConcreteCategory.hom (f.app (op (unop X)))) (uliftYonedaEquiv (uliftYonedaEquiv.symm x)) =
    uliftYonedaEquiv (uliftYonedaEquiv.symm ((ConcreteCategory.hom (f.app (op (unop X)))) x))
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝² : Category.{v₁, u₁} C✝
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
hF : F.FullyFaithful
X : C
X✝ Y✝ : Cᵒᵖ
f : X✝ ⟶ Y✝
⊢ (F.op ⋙ uliftYoneda.{v₁, v₂, u₂}.obj (F.obj X)).map f ≫
      (Equiv.ulift.trans (hF.homEquiv.symm.trans Equiv.ulift.symm)).toIso.hom =
    (Equiv.ulift.trans (hF.homEquiv.symm.trans Equiv.ulift.symm)).toIso.hom ≫ (uliftYoneda.{v₂, v₁, u₁}.obj X).map f

Tactic:
by ext; exact Equiv.ulift.injective (hF.map_injective (by simp))

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
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
hF : F.FullyFaithful
X X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ (F ⋙ uliftCoyoneda.{v₁, v₂, u₂}.obj (op (F.obj X))).map f ≫
      (Equiv.ulift.trans (hF.homEquiv.symm.trans Equiv.ulift.symm)).toIso.hom =
    (Equiv.ulift.trans (hF.homEquiv.symm.trans Equiv.ulift.symm)).toIso.hom ≫
      (uliftCoyoneda.{v₂, v₁, u₁}.obj (op X)).map f

Tactic:
by ext; exact Equiv.ulift.injective (hF.map_injective (by simp))

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
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
hF : F.FullyFaithful
X✝ Y✝ : Cᵒᵖ
f : X✝ ⟶ Y✝
⊢ (F.op ⋙ uliftCoyoneda.{v₁, v₂, u₂} ⋙ (whiskeringLeft C D (Type (max v₁ v₂))).obj F).map f ≫
      (hF.homNatIso' (unop Y✝)).hom =
    (hF.homNatIso' (unop X✝)).hom ≫ uliftCoyoneda.{v₂, v₁, u₁}.map f

Tactic:
by ext; exact Equiv.ulift.injective (hF.map_injective (by simp))

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst✝ : StrongEpi (f ≫ g)
X Y : C
z : X ⟶ Y
x✝ : Mono z
u : Q ⟶ X
v : R ⟶ Y
sq : CommSq u g z v
h₀ : (f ≫ u) ≫ z = (f ≫ g) ≫ v
⊢ g ≫ ⋯.lift = u

Tactic:
by
            simp only [← cancel_mono z, Category.assoc, CommSq.fac_right, sq.w]

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u
inst✝ : Category.{v, u} J
X : J
tX : IsInitial X
F : J ⥤ C
s : Cone F
m : s.pt ⟶ (coneOfDiagramInitial tX F).pt
w : ∀ (j : J), m ≫ (coneOfDiagramInitial tX F).π.app j = s.π.app j
⊢ m = m ≫ F.map (tX.to X)

Tactic:
tX.hom_ext (tX.to X) (𝟙 _)

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u
inst✝ : Category.{v, u} J
X : J
tX : IsInitial X
F : J ⥤ C
s : Cone F
m : s.pt ⟶ (coneOfDiagramInitial tX F).pt
w : ∀ (j : J), m ≫ (coneOfDiagramInitial tX F).π.app j = s.π.app j
⊢ m = m ≫ F.map (𝟙 X)
Module: Mathlib.CategoryTheory.Limits.Shapes.Products

Goal state before:
pp: β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Unique β
f : β → C
s : Cocone (Discrete.functor f)
m :
  { pt := f default,
        ι :=
          Discrete.natTrans fun x ↦
            match x with
            | { as := j } => eqToHom ⋯ }.pt ⟶
    s.pt
w :
  ∀ (j : Discrete β),
    { pt := f default,
                ι :=
                  Discrete.natTrans fun x ↦
                    match x with
                    | { as := j } => eqToHom ⋯ }.ι.app
          j ≫
        m =
      s.ι.app j
⊢ m = s.ι.app default

Tactic:
specialize w default
        simp_all

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

Goal state before:
pp: case h₀
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : IsIso f
⊢ (pullback.snd f g ≫ pullback.lift (g ≫ inv f) (𝟙 Y) ⋯) ≫ pullback.fst f g = 𝟙 (pullback f g) ≫ pullback.fst f g

pp: case h₁
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : IsIso f
⊢ (pullback.snd f g ≫ pullback.lift (g ≫ inv f) (𝟙 Y) ⋯) ≫ pullback.snd f g = 𝟙 (pullback f g) ≫ pullback.snd f g

Tactic:
· simp [← pullback.condition_assoc]

Goal state after:
case h₁
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : IsIso f
⊢ (pullback.snd f g ≫ pullback.lift (g ≫ inv f) (𝟙 Y) ⋯) ≫ pullback.snd f g = 𝟙 (pullback f g) ≫ pullback.snd f g
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)
⊢ W₂.inverseImage F (F.preimage ((F.objObjPreimageIso h.Z).hom ≫ h.p))

Tactic:
refine (W₂.arrow_mk_iso_iff ?_).1 h.hp

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)
⊢ Arrow.mk h.p ≅ Arrow.mk (F.map (F.preimage ((F.objObjPreimageIso h.Z).hom ≫ h.p)))
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
i : Z ⟶ W
inst✝ : Mono i
⊢ HasPullback (f ≫ i) i

Tactic:
simpa only [Category.id_comp] using hasPullback_of_comp_mono f (𝟙 Z) i

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 : X ⟶ Y
I✝ : C
Fm : I✝ ⟶ Y
m_mono✝¹ : Mono Fm
e✝¹ : X ⟶ I✝
Ffac : e✝¹ ≫ Fm = f
Fm' : I✝ ⟶ Y
m_mono✝ : Mono Fm'
e✝ : X ⟶ I✝
Ffac' : e✝ ≫ Fm' = f
hm :
  { I := I✝, m := Fm, m_mono := m_mono✝¹, e := e✝¹, fac := Ffac }.m =
    eqToHom ⋯ ≫ { I := I✝, m := Fm', m_mono := m_mono✝, e := e✝, fac := Ffac' }.m
⊢ Fm = Fm'

Tactic:
simpa using hm

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
h✝ : f = g
s : Fork f g
m : s.pt ⟶ (idFork h✝).pt
h : m ≫ (idFork h✝).ι = s.ι
⊢ m = s.ι

Tactic:
convert! h
    exact (Category.comp_id _).symm

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

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

Tactic:
rw [zero_of_target_iso_zero g i, zero_of_target_iso_zero h i]

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✝ : PreservesColimit K₁ F
c : Cocone K₂
t : IsColimit c
this : IsColimit ((Cocone.precompose h.hom).obj c)
⊢ F.mapCocone ((Cocone.precompose h.hom).obj c) ≅
    (Cocone.precompose (Functor.isoWhiskerRight h F).hom).obj (F.mapCocone c)

Tactic:
exact Cocone.ext (Iso.refl _)

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✝ : ReflectsColimit K₁ F
c : Cocone K₂
t : IsColimit (F.mapCocone c)
⊢ (Cocone.precompose (Functor.isoWhiskerRight h F).hom).obj (F.mapCocone c) ≅
    F.mapCocone ((Cocone.precompose h.hom).obj c)

Tactic:
exact Cocone.ext (Iso.refl _)

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type w
inst✝¹ : Semiring R
inst✝ : Linear R C
D : Type u'
F : D → C
x✝⁵ x✝⁴ x✝³ : InducedCategory C F
x✝² : R
x✝¹ : x✝⁵ ⟶ x✝⁴
x✝ : x✝⁴ ⟶ x✝³
⊢ (x✝² • x✝¹) ≫ x✝ = x✝² • x✝¹ ≫ x✝

Tactic:
by ext; apply smul_comp

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
R : Type w
inst✝³ : Semiring R
inst✝² : Linear R C
X Y : C
f : X ⟶ Y
inst✝¹ : Epi f
r : R
inst✝ : Invertible r
Z✝ : C
g g' : Y ⟶ Z✝
H : (r • f) ≫ g = (r • f) ≫ g'
⊢ g = g'

Tactic:
by
    rw [smul_comp, smul_comp, ← comp_smul, ← comp_smul, cancel_epi] at H
    simpa [smul_smul] using congr_arg (fun f => ⅟r • f) H

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
P Q R : C
f✝ f' : P ⟶ Q
g g' : Q ⟶ R
X : C
f : End X
⊢ 0 * f = 0

Tactic:
dsimp [mul]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
P Q R : C
f✝ f' : P ⟶ Q
g g' : Q ⟶ R
X : C
f : End X
⊢ f ≫ 0 = 0
Module: Mathlib.CategoryTheory.Preadditive.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
P Q R : C
f✝ f' : P ⟶ Q
g g' : Q ⟶ R
X : C
f : End X
⊢ f * 0 = 0

Tactic:
dsimp [mul]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
P Q R : C
f✝ f' : P ⟶ Q
g g' : Q ⟶ R
X : C
f : End X
⊢ 0 ≫ f = 0
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
t : KernelFork f
lift : (s : KernelFork f) → s.pt ⟶ t.pt
fac : ∀ (s : KernelFork f), lift s ≫ Fork.ι t = Fork.ι s
uniq : ∀ (s : KernelFork f) (m : s.pt ⟶ t.pt), m ≫ Fork.ι t = Fork.ι s → m = lift s
s : Cone (parallelPair f 0)
j : WalkingParallelPair
⊢ lift s ≫ t.π.app j = s.π.app j

Tactic:
by
      cases j
      · exact fac s
      · simp

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 K : C
f : X ⟶ Y
i : K ⟶ X
w : i ≫ f = 0
h : {A : C} → (k : A ⟶ X) → k ≫ f = 0 → { l // l ≫ i = k }
hi : Mono i
A : C
k : A ⟶ X
hk : k ≫ f = 0
m : A ⟶ K
hm : m ≫ i = k
⊢ m ≫ i = ↑(h k hk) ≫ i

Tactic:
(h k hk).2,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
X Y K : C
f : X ⟶ Y
i : K ⟶ X
w : i ≫ f = 0
h : {A : C} → (k : A ⟶ X) → k ≫ f = 0 → { l // l ≫ i = k }
hi : Mono i
A : C
k : A ⟶ X
hk : k ≫ f = 0
m : A ⟶ K
hm : m ≫ i = k
⊢ m ≫ i = k
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 Q : C
f : X ⟶ Y
p : Y ⟶ Q
w : f ≫ p = 0
h : {A : C} → (k : Y ⟶ A) → f ≫ k = 0 → { l // p ≫ l = k }
hp : Epi p
A : C
k : Y ⟶ A
hk : f ≫ k = 0
m : Q ⟶ A
hm : p ≫ m = k
⊢ p ≫ m = p ≫ ↑(h k hk)

Tactic:
(h k hk).2,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
X Y Q : C
f : X ⟶ Y
p : Y ⟶ Q
w : f ≫ p = 0
h : {A : C} → (k : Y ⟶ A) → f ≫ k = 0 → { l // p ≫ l = k }
hp : Epi p
A : C
k : Y ⟶ A
hk : f ≫ k = 0
m : Q ⟶ A
hm : p ≫ m = k
⊢ p ≫ m = k
Module: Mathlib.CategoryTheory.Preadditive.AdditiveFunctor

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : Preadditive C
inst✝³ : Preadditive D
F : C ⥤ D
inst✝² : HasBinaryProducts C
inst✝¹ : PreservesLimitsOfShape (Discrete WalkingPair) F
inst✝ : F.PreservesZeroMorphisms
⊢ F.Additive

Tactic:
have : HasBinaryBiproducts C := HasBinaryBiproducts.of_hasBinaryProducts
  have := preservesBinaryBiproducts_of_preservesBinaryProducts F
  exact Functor.additive_of_preservesBinaryBiproducts F

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

Goal state before:
pp: C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
W X Y Z : C
inst✝¹ : HasBinaryBiproduct W X
inst✝ : HasBinaryBiproduct Y Z
f : W ⟶ Y
g : X ⟶ Z
⊢ inl ≫ map f g = f ≫ inl

Tactic:
by
  rw [biprod.map_eq_map']
  exact IsColimit.ι_map (BinaryBiproduct.isColimit W X) _ _ ⟨WalkingPair.left⟩

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

Goal state before:
pp: μ : Type u_2
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
n x₁ x₂ : μ
⊢ (∃ a ∈ univ.piAntidiag n, { toFun := ⇑(Equiv.boolArrowEquivProd μ), inj' := ⋯ } a = (x₁, x₂)) ↔
    (x₁, x₂) ∈ antidiagonal n

Tactic:
Function.Embedding.coeFn_mk,

Goal state after:
μ : Type u_2
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
n x₁ x₂ : μ
⊢ (∃ a ∈ univ.piAntidiag n, (Equiv.boolArrowEquivProd μ) a = (x₁, x₂)) ↔ (x₁, x₂) ∈ antidiagonal n
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: n : ℕ
c : Composition n
⊢ ∑ i, c.blocksFun i = n

Tactic:
by
  conv_rhs => rw [← c.blocks_sum, ← ofFn_blocksFun, sum_ofFn]

Goal state after:
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
nz : 𝟙 W ≠ 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
h₁ : x = 𝟙 W
⊢ False

Tactic:
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]

Goal state after:
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
nz : 𝟙 W ≠ 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
h₁ : x = 𝟙 W
h₀ : x = 0
⊢ False
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: case mpr.refine_1
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length
h : c.sizeUpTo ↑i ≤ ↑j ∧ ↑j < c.sizeUpTo (↑i).succ
⊢ ↑j < c.sizeUpTo (↑i + 1)

Tactic:
exact h.2

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 t : Finset ι
h : s ⊆ t
n : μ
⊢ s.finsuppAntidiag n ⊆ t.finsuppAntidiag n

Tactic:
by
  intro a
  simp_rw [mem_finsuppAntidiag']
  rintro ⟨hsum, hmem⟩
  exact ⟨hsum, hmem.trans h⟩

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

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

Tactic:
by simp [blocksFun, single]

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

Goal state before:
pp: n✝ n : ℕ
s : Finset (Fin (n - 1))
i : Fin (n - 1)
this : ↑i + 1 ≠ n
⊢ (∃ j ∈ s, ↑i = ↑j) ↔ i ∈ s

Tactic:
← Fin.ext_iff,

Goal state after:
n✝ n : ℕ
s : Finset (Fin (n - 1))
i : Fin (n - 1)
this : ↑i + 1 ≠ n
⊢ (∃ j ∈ s, i = j) ↔ i ∈ s
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x y z : α
h : [x, y, z].Nodup
⊢ (swap x y * swap y z).support = {x, y, z}

Tactic:
simp only [List.not_mem_nil, and_true, List.mem_cons, not_false_iff, List.nodup_cons,
    and_self_iff, List.nodup_nil] at h

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x y z : α
h : ¬(x = y ∨ x = z ∨ False) ∧ ¬(y = z ∨ False)
⊢ (swap x y * swap y z).support = {x, y, z}
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: case succ
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
n : ℕ
hn : (l.rotate n).formPerm = l.formPerm
⊢ ((l.rotate n).rotate 1).formPerm = l.formPerm

Tactic:
formPerm_rotate_one,

Goal state after:
case succ
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
n : ℕ
hn : (l.rotate n).formPerm = l.formPerm
⊢ (l.rotate n).formPerm = l.formPerm

case succ.h
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
n : ℕ
hn : (l.rotate n).formPerm = l.formPerm
⊢ (l.rotate n).Nodup
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f : Perm α
x y : α
n : ℕ
⊢ f.SameCycle x ((f ^ ↑n) y) ↔ f.SameCycle x y

Tactic:
sameCycle_zpow_right

Goal state after:
α : Type u_2
f : Perm α
x y : α
n : ℕ
⊢ f.SameCycle x y ↔ f.SameCycle x y
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: x y : Fin 1
⊢ x ≠ y → (swap x y).signAux = -1

Tactic:
dsimp [signAux, swap, swapCore]
    simp only [eq_iff_true_of_subsingleton, not_true,
               IsEmpty.forall_iff]

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

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
n : ℕ
h : n.Coprime (orderOf σ)
⊢ (σ ^ n).support = σ.support

Tactic:
obtain ⟨m, hm⟩ := exists_pow_eq_self_of_coprime h
  exact
    le_antisymm (support_pow_le σ n)
      (le_trans (ge_of_eq (congr_arg support hm)) (support_pow_le (σ ^ n) m))

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_4
inst✝ : DecidableEq α
f : Perm α
hf : f.IsCycle
x : α
hfx : f x ≠ x
hffx : f (f x) = x
y z : α
hz : f z ≠ z ∧ ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle z y
i : ℤ
hi : (f ^ i) z = x
hyx : y = x
⊢ f y = (swap x (f x)) y

Tactic:
simp [hyx]

Goal state after:
Module: Mathlib.Data.Set.Pairwise.List

Goal state before:
pp: α : Type u_1
r : α → α → Prop
l : List α
inst✝ : Std.Symm r
hl : l.Nodup
⊢ {a | a ∈ l}.Pairwise r ↔ Pairwise r l

Tactic:
induction l with | nil => simp | cons a l ih => ?_
  rw [List.nodup_cons] at hl
  have : ∀ b ∈ l, ¬a = b → r a b ↔ r a b := fun b hb =>
    imp_iff_right (ne_of_mem_of_not_mem hb hl.1).symm
  simp [Set.ofPred_or, Set.pairwise_insert_of_symm, ih hl.2, and_comm, forall₂_congr this]

Goal state after: