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

Goal state before:
pp: case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (e.functor.map (e.inverse.map (e.functor.map (e.unit.app (e.inverse.obj Y))))) ≫
    e.unitInv.app (e.inverse.obj (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))

pp: case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (e.functor.map (e.unitInv.app (e.inverse.obj Y)))

pp: case a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (e.counit.app Y)

pp: case a
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)

pp: case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (e.counitInv.app (e.functor.obj (e.inverse.obj Y)))

Tactic:
e.unitInv_naturality

Goal state after:
case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.unitInv.app (e.inverse.obj (e.functor.obj (e.inverse.obj Y))) ≫
    e.inverse.map (e.functor.map (e.unit.app (e.inverse.obj Y)))

case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (e.functor.map (e.unitInv.app (e.inverse.obj Y)))

case a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (e.counit.app Y)

case a
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)

case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (e.counitInv.app (e.functor.obj (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
P : MorphismProperty D
F : C ⥤ D
X Y : C
f : X ⟶ Y
⊢ P.inverseImage F f ↔ P (F.map f)

Tactic:
by rfl

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Arrow

Goal state before:
pp: T : Type u
inst✝ : Category.{v, u} T
f g : Arrow T
l : f.right ≅ g.right
r : f.left ≅ g.left
h : g.hom ≫ l.inv = r.inv ≫ f.hom
⊢ r.hom ≫ g.hom = f.hom ≫ l.hom

Tactic:
rwa [Iso.comp_inv_eq, Category.assoc, Iso.eq_inv_comp] at h

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Arrow

Goal state before:
pp: T : Type u
inst✝ : Category.{v, u} T
W X Y Z : T
f : X ⟶ W
g : Z ⟶ Y
e₁ : W ≅ Y
e₂ : X ≅ Z
h : g ≫ e₁.inv = e₂.inv ≫ f
⊢ e₂.hom ≫ g = f ≫ e₁.hom

Tactic:
rwa [Iso.comp_inv_eq, Category.assoc, Iso.eq_inv_comp] at h

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
⊢ (isomorphisms C).op = isomorphisms Cᵒᵖ

Tactic:
by
  ext
  apply isIso_unop_iff

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

Goal state before:
pp: case mp
X Y : Type u
f : X → Y
H : ∀ {Z : Type u} (g h : Y ⟶ Z), ↾f ≫ g = ↾f ≫ h → g = h
g₁ g₂ : Y → Prop
hg : g₁ ∘ f = g₂ ∘ f
⊢ g₁ = g₂

Tactic:
rw [← Equiv.ulift.{u}.symm.injective.comp_left.eq_iff]

Goal state after:
case mp
X Y : Type u
f : X → Y
H : ∀ {Z : Type u} (g h : Y ⟶ Z), ↾f ≫ g = ↾f ≫ h → g = h
g₁ g₂ : Y → Prop
hg : g₁ ∘ f = g₂ ∘ f
⊢ ⇑Equiv.ulift.symm ∘ g₁ = ⇑Equiv.ulift.symm ∘ g₂
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
P : MorphismProperty C
F G : C ⥤ D
e : F ≅ G
X Y : D
f : X ⟶ Y
X' Y' : C
f' : X' ⟶ Y'
hf' : P f'
e' : Arrow.mk (F.map f') ≅ Arrow.mk f
⊢ P.map G f

Tactic:
exact ⟨X', Y', f', hf', ⟨((Functor.mapArrowFunctor _ _).mapIso e.symm).app (Arrow.mk f') ≪≫ e'⟩⟩

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
⊢ isomorphisms C f ↔ IsIso f

Tactic:
by rfl

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
⊢ monomorphisms C f ↔ Mono f

Tactic:
by rfl

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
⊢ epimorphisms C f ↔ Epi f

Tactic:
by rfl

Goal state after:
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
C : Type u₄
inst✝ : Category.{v₄, u₄} C
F : C ⥤ A
L : A ⥤ T
R : B ⥤ T
X✝ Y✝ : Comma (F ⋙ L) R
f : X✝ ⟶ Y✝
⊢ L.map (F.map f.left) ≫ { left := F.obj Y✝.left, right := Y✝.right, hom := Y✝.hom }.hom =
    { left := F.obj X✝.left, right := X✝.right, hom := X✝.hom }.hom ≫ R.map f.right

Tactic:
simpa using! f.w

Goal state after:
Module: Mathlib.Algebra.Category.MonCat.Basic

Goal state before:
pp: X : MonCat
⊢ ofHom (MulEquiv.ulift.symm.toMonoidHom.comp ((Hom.hom (𝟙 X)).comp MulEquiv.ulift.toMonoidHom)) =
    𝟙 (of (ULift.{u, v} ↑X))

Tactic:
by rfl

Goal state after:
Module: Mathlib.Algebra.Category.MonCat.Basic

Goal state before:
pp: X Y Z : MonCat
f : X ⟶ Y
g : Y ⟶ Z
⊢ ofHom (MulEquiv.ulift.symm.toMonoidHom.comp ((Hom.hom (f ≫ g)).comp MulEquiv.ulift.toMonoidHom)) =
    ofHom (MulEquiv.ulift.symm.toMonoidHom.comp ((Hom.hom f).comp MulEquiv.ulift.toMonoidHom)) ≫
      ofHom (MulEquiv.ulift.symm.toMonoidHom.comp ((Hom.hom g).comp MulEquiv.ulift.toMonoidHom))

Tactic:
by rfl

Goal state after:
Module: Mathlib.Algebra.Category.MonCat.Basic

Goal state before:
pp: X : CommMonCat
⊢ ofHom (MulEquiv.ulift.symm.toMonoidHom.comp ((Hom.hom (𝟙 X)).comp MulEquiv.ulift.toMonoidHom)) =
    𝟙 (of (ULift.{u, v} ↑X))

Tactic:
by rfl

Goal state after:
Module: Mathlib.Algebra.Category.MonCat.Basic

Goal state before:
pp: X Y Z : CommMonCat
f : X ⟶ Y
g : Y ⟶ Z
⊢ ofHom (MulEquiv.ulift.symm.toMonoidHom.comp ((Hom.hom (f ≫ g)).comp MulEquiv.ulift.toMonoidHom)) =
    ofHom (MulEquiv.ulift.symm.toMonoidHom.comp ((Hom.hom f).comp MulEquiv.ulift.toMonoidHom)) ≫
      ofHom (MulEquiv.ulift.symm.toMonoidHom.comp ((Hom.hom g).comp MulEquiv.ulift.toMonoidHom))

Tactic:
by rfl

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Basic

Goal state before:
pp: X : GrpCat
⊢ ofHom (MulEquiv.ulift.symm.toMonoidHom.comp ((Hom.hom (𝟙 X)).comp MulEquiv.ulift.toMonoidHom)) =
    𝟙 (of (ULift.{u, v} ↑X))

Tactic:
by rfl

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Basic

Goal state before:
pp: X Y Z : GrpCat
f : X ⟶ Y
g : Y ⟶ Z
⊢ ofHom (MulEquiv.ulift.symm.toMonoidHom.comp ((Hom.hom (f ≫ g)).comp MulEquiv.ulift.toMonoidHom)) =
    ofHom (MulEquiv.ulift.symm.toMonoidHom.comp ((Hom.hom f).comp MulEquiv.ulift.toMonoidHom)) ≫
      ofHom (MulEquiv.ulift.symm.toMonoidHom.comp ((Hom.hom g).comp MulEquiv.ulift.toMonoidHom))

Tactic:
by rfl

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Basic

Goal state before:
pp: X : CommGrpCat
⊢ ofHom (MulEquiv.ulift.symm.toMonoidHom.comp ((Hom.hom (𝟙 X)).comp MulEquiv.ulift.toMonoidHom)) =
    𝟙 (of (ULift.{u, v} ↑X))

Tactic:
by rfl

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Basic

Goal state before:
pp: X Y Z : CommGrpCat
f : X ⟶ Y
g : Y ⟶ Z
⊢ ofHom (MulEquiv.ulift.symm.toMonoidHom.comp ((Hom.hom (f ≫ g)).comp MulEquiv.ulift.toMonoidHom)) =
    ofHom (MulEquiv.ulift.symm.toMonoidHom.comp ((Hom.hom f).comp MulEquiv.ulift.toMonoidHom)) ≫
      ofHom (MulEquiv.ulift.symm.toMonoidHom.comp ((Hom.hom g).comp MulEquiv.ulift.toMonoidHom))

Tactic:
by rfl

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Basic

Goal state before:
pp: X Y : CommRingCat
f : X ⟶ Y
x✝ : IsIso ((forget CommRingCat).map f)
i : (forget CommRingCat).obj X ≅ (forget CommRingCat).obj Y := asIso ((forget CommRingCat).map f)
ff : ↑X →+* ↑Y := Hom.hom f
e : ↑X ≃+* ↑Y :=
  let __src := i.toEquiv;
  { toFun := (↑↑ff).toFun, invFun := __src.invFun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯ }
⊢ IsIso f

Tactic:
exact e.toCommRingCatIso.isIso_hom

Goal state after:
Module: Mathlib.CategoryTheory.Category.Preorder

Goal state before:
pp: X : Type u
inst✝¹ : Preorder X
inst✝ : OrderTop X
x : X
a : x ⟶ ⊤
⊢ a = homOfLE ⋯

Tactic:
by rfl

Goal state after:
Module: Mathlib.CategoryTheory.Category.Preorder

Goal state before:
pp: X : Type u
inst✝¹ : Preorder X
inst✝ : OrderBot X
x : X
a : ⊥ ⟶ x
⊢ a = homOfLE ⋯

Tactic:
by rfl

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ (α_ f (𝟙 b) g).inv ≫ (ρ_ f).hom ▷ g = f ◁ (λ_ g).hom

Tactic:
by rw [← triangle, inv_hom_id_assoc]

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

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
D : Type u₄
inst✝¹ : Category.{v₄, u₄} D
E : Type u₅
inst✝ : Category.{v₅, u₅} E
F : Discrete PUnit.{?u.21 + 1} ⥤ C
⊢ ∀ ⦃X Y : Discrete PUnit.{?u.21 + 1}⦄ (f : X ⟶ Y),
    (((const (Discrete PUnit.{?u.21 + 1})).obj (F.obj { as := PUnit.unit })).map f ≫
        match Y with
        | { as := PUnit.unit } =>
          𝟙 (((const (Discrete PUnit.{?u.21 + 1})).obj (F.obj { as := PUnit.unit })).obj { as := PUnit.unit })) =
      (match X with
        | { as := PUnit.unit } =>
          𝟙 (((const (Discrete PUnit.{?u.21 + 1})).obj (F.obj { as := PUnit.unit })).obj { as := PUnit.unit })) ≫
        F.map f

Tactic:
intro X Y f
              match X, Y, f with
              | .mk A, .mk B, .up g =>
                simp

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

Goal state before:
pp: J : Type w
C✝ : Type u
inst✝² : Category.{v, u} C✝
C : Type u
inst✝¹ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → B ⟶ objs j
inst✝ : HasWidePushout B objs arrows
X : C
f : B ⟶ X
fs : (j : J) → objs j ⟶ X
w : ∀ (j : J), arrows j ≫ fs j = f
g : widePushout B objs arrows ⟶ X
j : J
⊢ arrows j ≫ ι arrows j ≫ g = head arrows ≫ g

Tactic:
rw [← Category.assoc]

Goal state after:
J : Type w
C✝ : Type u
inst✝² : Category.{v, u} C✝
C : Type u
inst✝¹ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → B ⟶ objs j
inst✝ : HasWidePushout B objs arrows
X : C
f : B ⟶ X
fs : (j : J) → objs j ⟶ X
w : ∀ (j : J), arrows j ≫ fs j = f
g : widePushout B objs arrows ⟶ X
j : J
⊢ (arrows j ≫ ι arrows j) ≫ g = head arrows ≫ g
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 : Cone (Discrete.functor f)
j : Discrete β
⊢ s.π.app default ≫
      { pt := f default,
              π :=
                Discrete.natTrans fun x ↦
                  match x with
                  | { as := j } => eqToHom ⋯ }.π.app
        j =
    s.π.app j

Tactic:
obtain rfl := Subsingleton.elim j default
        simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
h : IsTerminal Y
c : BinaryFan X Y
⊢ Nonempty (IsLimit c) ↔ IsIso c.fst

Tactic:
by
  constructor
  · rintro ⟨H⟩
    obtain ⟨l, hl, -⟩ := BinaryFan.IsLimit.lift' H (𝟙 X) (h.from X)
    exact
      ⟨⟨l,
          BinaryFan.IsLimit.hom_ext H (by simpa [hl, -Category.comp_id] using Category.comp_id _)
            (h.hom_ext _ _),
          hl⟩⟩
  · intro
    exact
      ⟨BinaryFan.IsLimit.mk _ (fun f _ => f ≫ inv c.fst) (fun _ _ => by simp)
          (fun _ _ => h.hom_ext _ _) fun _ _ _ e _ => by simp [← e]⟩

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

Goal state before:
pp: case some.left
C : Type u
inst✝ : Category.{v, u} C
F : WalkingCospan ⥤ C
s t : Cone F
i : s.pt ≅ t.pt
w₁ : s.π.app left = i.hom ≫ t.π.app left
w₂ : s.π.app right = i.hom ≫ t.π.app right
⊢ s.π.app (some WalkingPair.left) = i.hom ≫ t.π.app (some WalkingPair.left)

Tactic:
exact w₁

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

Goal state before:
pp: case some.left
C : Type u
inst✝ : Category.{v, u} C
F : WalkingSpan ⥤ C
s t : Cocone F
i : s.pt ≅ t.pt
w₁ : s.ι.app WalkingCospan.left ≫ i.hom = t.ι.app WalkingCospan.left
w₂ : s.ι.app WalkingCospan.right ≫ i.hom = t.ι.app WalkingCospan.right
⊢ s.ι.app (some WalkingPair.left) ≫ i.hom = t.ι.app (some WalkingPair.left)

Tactic:
exact w₁

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
t : PushoutCocone f g
ht : IsColimit t
s : PushoutCocone g f
m : t.pt ⟶ s.pt
h₁ : t.inr ≫ m = s.inl
h₂ : t.inl ≫ m = s.inr
⊢ m = ht.desc s.flip

Tactic:
by
    apply IsColimit.hom_ext ht <;> simp [h₁, h₂]

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty C
data : W₁.FunctorialFactorizationData W₂
f : Arrow C
⊢ data.i.app f ≫ data.p.app f = f.hom

Tactic:
← NatTrans.comp_app,

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty C
data : W₁.FunctorialFactorizationData W₂
f : Arrow C
⊢ (data.i ≫ data.p).app f = f.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 ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasBinaryProduct X Y
W : C
i₁ i₂ : W ⟶ pullback f g
h : i₁ ≫ prod.lift (pullback.fst f g) (pullback.snd f g) = i₂ ≫ prod.lift (pullback.fst f g) (pullback.snd f g)
⊢ i₁ ≫ pullback.snd f g = i₂ ≫ pullback.snd f g

Tactic:
· simpa using congrArg (fun f => f ≫ prod.snd) h

Goal state after:
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 ⟶ Y
g✝ : X ⟶ Z
f : X ⟶ Y
g : X ⟶ Z
h : X ⟶ W
inst✝ : Epi h
x : W ⟶ Y
y : W ⟶ Z
hhx : h ≫ x = f
hhy : h ≫ y = g
s : PushoutCocone f g
hs : IsColimit s
⊢ h ≫ x ≫ s.inl = f ≫ s.inl

Tactic:
rw [← Category.assoc]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f✝ : X ⟶ Y
g✝ : X ⟶ Z
f : X ⟶ Y
g : X ⟶ Z
h : X ⟶ W
inst✝ : Epi h
x : W ⟶ Y
y : W ⟶ Z
hhx : h ≫ x = f
hhy : h ≫ y = g
s : PushoutCocone f g
hs : IsColimit s
⊢ (h ≫ x) ≫ s.inl = f ≫ s.inl
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 ⟶ Y
g✝ : X ⟶ Z
f : X ⟶ Y
g : X ⟶ Z
h : X ⟶ W
inst✝ : Epi h
x : W ⟶ Y
y : W ⟶ Z
hhx : h ≫ x = f
hhy : h ≫ y = g
s : PushoutCocone f g
hs : IsColimit s
reassoc₁ : h ≫ x ≫ s.inl = f ≫ s.inl
⊢ h ≫ y ≫ s.inr = g ≫ s.inr

Tactic:
rw [← Category.assoc]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f✝ : X ⟶ Y
g✝ : X ⟶ Z
f : X ⟶ Y
g : X ⟶ Z
h : X ⟶ W
inst✝ : Epi h
x : W ⟶ Y
y : W ⟶ Z
hhx : h ≫ x = f
hhy : h ≫ y = g
s : PushoutCocone f g
hs : IsColimit s
reassoc₁ : h ≫ x ≫ s.inl = f ≫ s.inl
⊢ (h ≫ y) ≫ s.inr = g ≫ s.inr
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 : C
f : X ⟶ Y
Z : C
⊢ f ≫ hO.from_ Y ≫ hO.to_ Z = hO.from_ X ≫ hO.to_ Z

Tactic:
rw [← Category.assoc]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
O : C
hO : IsZero O
X Y : C
f : X ⟶ Y
Z : C
⊢ (f ≫ hO.from_ Y) ≫ hO.to_ Z = hO.from_ X ≫ hO.to_ Z
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✝ : HasZeroObject C
X Y : C
f : X ⟶ Y
Z : C
⊢ f ≫ default ≫ default = default ≫ default

Tactic:
rw [← Category.assoc]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroObject C
X Y : C
f : X ⟶ Y
Z : C
⊢ (f ≫ default) ≫ default = default ≫ default
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X Y : C
f : X ⟶ Y
i : X ≅ 0
j : Y ≅ 0
⊢ IsIso f

Tactic:
rw [zero_of_source_iso_zero f i]
  exact (isIsoZeroEquivIsoZero _ _).invFun ⟨i, j⟩

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
F : J ⥤ C
G : C ⥤ D
inst✝² : G.ReflectsIsomorphisms
inst✝¹ : HasLimit F
inst✝ : PreservesLimit F G
c : Cone F
t : IsLimit (G.mapCone c)
⊢ IsIso ((limit.isLimit F).lift c)

Tactic:
change IsIso ((Cone.forget _).map ((limit.isLimit F).liftConeMorphism c))

Goal state after:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
J : Type w
inst✝³ : Category.{w', w} J
F : J ⥤ C
G : C ⥤ D
inst✝² : G.ReflectsIsomorphisms
inst✝¹ : HasLimit F
inst✝ : PreservesLimit F G
c : Cone F
t : IsLimit (G.mapCone c)
⊢ IsIso ((Cone.forget F).map ((limit.isLimit F).liftConeMorphism c))
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), PreservesLimitsOfShape J F
J : Type
x✝¹ : SmallCategory J
x✝ : FinCategory J
⊢ PreservesLimitsOfShape J F

Tactic:
have := h (ULiftHom (ULift J)) CategoryTheory.finCategoryUlift
        exact preservesLimitsOfShape_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 uC
inst✝⁵ : Category.{uC', uC} C
inst✝⁴ : HasZeroMorphisms C
D : Type uD
inst✝³ : Category.{uD', uD} D
inst✝² : HasZeroMorphisms D
F : J → C
inst✝¹ : HasFiniteBiproducts C
inst✝ : Finite J
n : ℕ
e : J ≃ Fin n
⊢ HasBiproductsOfShape J C

Tactic:
have : HasBiproductsOfShape (Fin n) C := HasFiniteBiproducts.out n

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
F : J → C
inst✝¹ : HasFiniteBiproducts C
inst✝ : Finite J
n : ℕ
e : J ≃ Fin n
this : HasBiproductsOfShape (Fin n) C
⊢ HasBiproductsOfShape J C
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: case intro
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
β γ : Type
inst✝² : Finite β
ε : β ≃ γ
f : γ → C
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct (f ∘ ⇑ε)
val✝ : Fintype β
g g' : γ
⊢ ι f g' ≫ ((lift fun b ↦ π f (ε b)) ≫ desc fun b ↦ ι f (ε b)) ≫ π f g = ι f g' ≫ 𝟙 (⨁ f) ≫ π f g

Tactic:
by_cases h : g' = g <;>
      simp [Preadditive.sum_comp, biproduct.lift_desc, biproduct.ι_π, comp_dite,
        ← Equiv.eq_symm_apply, h]

Goal state after:
Module: Mathlib.Algebra.Group.TypeTags.Finite

Goal state before:
pp: α : Type u
inst✝ : Finite α
⊢ α ≃ Additive α

Tactic:
by rfl

Goal state after:
Module: Mathlib.Algebra.Group.TypeTags.Finite

Goal state before:
pp: α : Type u
inst✝ : Finite α
⊢ α ≃ Multiplicative α

Tactic:
by rfl

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

Goal state before:
pp: n : ℕ
x : n.Partition
⊢ (∀ i ∈ x.parts, count i x.parts < 2) ↔ x.parts.Nodup

Tactic:
rw [Multiset.nodup_iff_count_le_one]

Goal state after:
n : ℕ
x : n.Partition
⊢ (∀ i ∈ x.parts, count i x.parts < 2) ↔ ∀ (a : ℕ), count a x.parts ≤ 1
Module: Mathlib.GroupTheory.Perm.Support

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

Tactic:
hffx

Goal state after:
α : Type u_1
f : Perm α
x : α
hffx : f (f x) = x
n : ℕ
h : (f ^ n) x = f x
⊢ x = x
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: case mp
n : ℕ
c : Composition n
⊢ c = ones n → c.length = n

Tactic:
rintro rfl
    exact ones_length n

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:
rw [hg, hf]

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:
rw [reverse_append, reverse_single]
      apply cast_heq

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

Goal state before:
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:
· convert! hj1

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

Goal state before:
pp: n : ℕ
⊢ Fintype.card (CompositionAsSet n) = 2 ^ (n - 1)

Tactic:
have : Fintype.card (Finset (Fin (n - 1))) = 2 ^ (n - 1) := by simp
  rw [← this]
  exact Fintype.card_congr (compositionAsSetEquiv n)

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
hl : 1 < l.length
⊢ l.formPerm l[0] = l[1]

Tactic:
by
  rcases l with (_ | ⟨x, _ | ⟨y, tl⟩⟩)
  · simp at hl
  · simp at hl
  · rw [getElem_cons_zero, formPerm_apply_head _ _ _ h, getElem_cons_succ, getElem_cons_zero]

Goal state after:
Module: Mathlib.Data.Fintype.Perm

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
f : Equiv.Perm α
h✝² : f ∈ permsOfList (a :: l)
x : α
h : f ∈ flatMap (fun b ↦ List.map (fun f ↦ Equiv.swap a b * f) (permsOfList l)) l
hx : f x ≠ x
y : α
hy : y ∈ l
hy' : f ∈ List.map (fun f ↦ Equiv.swap a y * f) (permsOfList l)
g : Equiv.Perm α
hg₁ : g ∈ permsOfList l
hg₂ : Equiv.swap a y * g = f
hxa : ¬x = a
hxy : ¬x = y
h✝¹ : ¬f x = a
h✝ : ¬f x = y
⊢ f x ≠ x

Tactic:
exact hx

Goal state after:
Module: Mathlib.Data.Fintype.Perm

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
hl : (a :: l).Nodup
hl' : l.Nodup
hln' : (permsOfList l).Nodup
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → f a = a
i j : ℕ
hi : i < l.length
hj : j < l.length
hij : i < j
x : Equiv.Perm α
hx₁ : x ∈ (fun b ↦ List.map (fun f ↦ Equiv.swap a b * f) (permsOfList l)) l[i]
hx₂ : x ∈ (fun b ↦ List.map (fun f ↦ Equiv.swap a b * f) (permsOfList l)) l[j]
f : Equiv.Perm α
hf : f ∈ permsOfList l ∧ Equiv.swap a l[i] * f = x
g : Equiv.Perm α
hg : g ∈ permsOfList l ∧ Equiv.swap a l[j] * g = x
⊢ x a = l[i]

Tactic:
← hf.2,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
hl : (a :: l).Nodup
hl' : l.Nodup
hln' : (permsOfList l).Nodup
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → f a = a
i j : ℕ
hi : i < l.length
hj : j < l.length
hij : i < j
x : Equiv.Perm α
hx₁ : x ∈ (fun b ↦ List.map (fun f ↦ Equiv.swap a b * f) (permsOfList l)) l[i]
hx₂ : x ∈ (fun b ↦ List.map (fun f ↦ Equiv.swap a b * f) (permsOfList l)) l[j]
f : Equiv.Perm α
hf : f ∈ permsOfList l ∧ Equiv.swap a l[i] * f = x
g : Equiv.Perm α
hg : g ∈ permsOfList l ∧ Equiv.swap a l[j] * g = x
⊢ (Equiv.swap a l[i] * f) a = l[i]
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f : Perm α
x : α
inst✝ : Finite α
k : ℤ
h₀ : 0 < ↑(orderOf f)
h₁ : 0 ≤ k % ↑(orderOf f)
⊢ (f ^ k) x = (f ^ k) x

Tactic:
by rfl

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

Goal state before:
pp: α : Type u_2
f : Perm α
x : α
inst✝ : Finite α
i : ℕ
hi : i + 1 < orderOf f
h : f.SameCycle x ((f ^ (i + 1)) x)
⊢ (f ^ i.succ) x = (f ^ (i + 1)) x

Tactic:
by rfl

Goal state after: