mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n : ℕ
i j : Fin n
hij : i ≤ j
inst✝ : NeZero n
⊢ j.cycleIcc i = 1

Tactic:
rcases Fin.lt_or_eq_of_le hij with hij | hij
  · simp [hij]
  · rw [hij, ← cycleIcc_eq]

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

Goal state before:
pp: case mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
hg : g = swap a (g a) * swap (g a) (g (g a))
hx : g a = a
⊢ False

Tactic:
apply hg3.isCycle.ne_one

Goal state after:
case mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
hg : g = swap a (g a) * swap (g a) (g (g a))
hx : g a = a
⊢ g = 1
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: case pos.inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
hg3 : g.IsThreeCycle
x : α
ha : x ∈ g.support
ha' : g.support = {x, g x, g (g x)}
ha'' : [x, g x, g (g x)].Nodup
⊢ g x = (swap x (g x)) ((swap (g x) (g (g x))) x)

Tactic:
rw [swap_apply_of_ne_of_ne (x := x) (by grind) (by grind)]
      simp

Goal state after:
Module: Mathlib.LinearAlgebra.Alternating.Basic

Goal state before:
pp: case neg
ι : Type u_7
ι₁ : Type u_10
inst✝⁵ : Finite ι
R' : Type u_11
N₁ : Type u_12
N₂ : Type u_13
inst✝⁴ : CommSemiring R'
inst✝³ : AddCommMonoid N₁
inst✝² : AddCommMonoid N₂
inst✝¹ : Module R' N₁
inst✝ : Module R' N₂
f g : N₁ [⋀^ι]→ₗ[R'] N₂
e : Basis ι₁ R' N₁
h : ∀ (v : ι → ι₁), Function.Injective v → (f fun i ↦ e (v i)) = g fun i ↦ e (v i)
v : ι → ι₁
hi : ¬Function.Injective v
this : ¬Function.Injective fun i ↦ e (v i)
⊢ (↑f fun i ↦ e (v i)) = ↑g fun i ↦ e (v i)

Tactic:
rw [coe_multilinearMap, coe_multilinearMap, f.map_eq_zero_of_not_injective _ this,
      g.map_eq_zero_of_not_injective _ this]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse

Goal state before:
pp: n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
s : ℤˣ
A : Matrix (Option n) (Option n) R
⊢ A none none * detp s (A.submatrix some some) + ∑ i, A none (some i) * adjp s A (some i) none =
    A none none * detp s (A.submatrix some some) +
      ∑ k, A none (some k) * detp (-s) (A.submatrix some (Function.update some k none))

Tactic:
adjp_some_none

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: n : Type u_2
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
inst✝ : Nontrivial n
u v : n → R
i j : n
hij : i ≠ j
uv' : Matrix n n R := ((vecMulVec u v).updateRow i v).updateRow j v
huv' : uv'.det = 0
⊢ vecMulVec u v = (vecMulVec (update u j (u j)) v).updateRow i (u i • v)

Tactic:
update_eq_self,

Goal state after:
n : Type u_2
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
inst✝ : Nontrivial n
u v : n → R
i j : n
hij : i ≠ j
uv' : Matrix n n R := ((vecMulVec u v).updateRow i v).updateRow j v
huv' : uv'.det = 0
⊢ vecMulVec u v = (vecMulVec u v).updateRow i (u i • v)
Module: Mathlib.CategoryTheory.Filtered.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofilteredOrEmpty C
i j j' : C
f : j ⟶ i
f' : j' ⟶ i
K : C
G : K ⟶ j
G' : K ⟶ j'
h✝ : True
k : C
e : k ⟶ K
he : e ≫ G ≫ f = e ≫ G' ≫ f'
⊢ (e ≫ G) ≫ f = (e ≫ G') ≫ f'

Tactic:
simpa only [Category.assoc] using he

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofiltered C
O : Finset C
⊢ ∃ S, ∀ {X : C}, X ∈ O → Nonempty (S ⟶ X)

Tactic:
classical
  induction O using Finset.induction with
  | empty => exact ⟨Classical.choice IsCofiltered.nonempty, by simp⟩
  | insert X O' nm h =>
    obtain ⟨S', w'⟩ := h
    use min X S'
    rintro Y mY
    obtain rfl | h := eq_or_ne Y X
    · exact ⟨minToLeft _ _⟩
    · exact ⟨minToRight _ _ ≫ (w' (Finset.mem_of_mem_insert_of_ne mY h)).some⟩

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

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
c : Cone F
⊢ Nonempty (IsLimit c) ↔ Function.Bijective (sectionOfCone c)

Tactic:
isLimit_iff,

Goal state after:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
c : Cone F
⊢ (∀ s ∈ F.sections, ∃! x, ∀ (j : J), (hom (c.π.app j)) x = s j) ↔ Function.Bijective (sectionOfCone c)
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → AddCommGroup (M₁ i)
inst✝³ : AddCommGroup M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝ : DecidableEq ι
x : (i : ι) → M₁ i
i : ι
v : M₁ i
⊢ f (update x i v) = f x - (f (update x i (x i)) - f (update x i v))

Tactic:
update_eq_self,

Goal state after:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → AddCommGroup (M₁ i)
inst✝³ : AddCommGroup M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝ : DecidableEq ι
x : (i : ι) → M₁ i
i : ι
v : M₁ i
⊢ f (update x i v) = f x - (f x - f (update x i v))
Module: Mathlib.Algebra.Category.Ring.FilteredColimits

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCat
inst✝ : IsFiltered J
j₁ : J
x : ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj j₁
j₂ : J
y : ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj j₂
j₃ : J
z : ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj j₃
k : J := IsFiltered.max₃ j₁ j₂ j₃
f : j₁ ⟶ IsFiltered.max₃ j₁ j₂ j₃ := IsFiltered.firstToMax₃ j₁ j₂ j₃
g : j₂ ⟶ IsFiltered.max₃ j₁ j₂ j₃ := IsFiltered.secondToMax₃ j₁ j₂ j₃
h : j₃ ⟶ IsFiltered.max₃ j₁ j₂ j₃ := IsFiltered.thirdToMax₃ j₁ j₂ j₃
⊢ (Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel ⟨j₁, x⟩ +
        Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel ⟨j₂, y⟩) *
      Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel ⟨j₃, z⟩ =
    Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel ⟨j₁, x⟩ *
        Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel ⟨j₃, z⟩ +
      Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel ⟨j₂, y⟩ *
        Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel ⟨j₃, z⟩

Tactic:
colimit_add_mk_eq _ ⟨j₁, _⟩ ⟨j₂, _⟩ k f g,

Goal state after:
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCat
inst✝ : IsFiltered J
j₁ : J
x : ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj j₁
j₂ : J
y : ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj j₂
j₃ : J
z : ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj j₃
k : J := IsFiltered.max₃ j₁ j₂ j₃
f : j₁ ⟶ IsFiltered.max₃ j₁ j₂ j₃ := IsFiltered.firstToMax₃ j₁ j₂ j₃
g : j₂ ⟶ IsFiltered.max₃ j₁ j₂ j₃ := IsFiltered.secondToMax₃ j₁ j₂ j₃
h : j₃ ⟶ IsFiltered.max₃ j₁ j₂ j₃ := IsFiltered.thirdToMax₃ j₁ j₂ j₃
⊢ AddMonCat.FilteredColimits.M.mk ((F ⋙ forget₂ SemiRingCat AddCommMonCat) ⋙ forget₂ AddCommMonCat AddMonCat)
        ⟨k,
          (ConcreteCategory.hom (((F ⋙ forget₂ SemiRingCat AddCommMonCat) ⋙ forget₂ AddCommMonCat AddMonCat).map f))
              ⟨j₁, x⟩.snd +
            (ConcreteCategory.hom (((F ⋙ forget₂ SemiRingCat AddCommMonCat) ⋙ forget₂ AddCommMonCat AddMonCat).map g))
              ⟨j₂, y⟩.snd⟩ *
      Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel ⟨j₃, z⟩ =
    Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel ⟨j₁, x⟩ *
        Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel ⟨j₃, z⟩ +
      Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel ⟨j₂, y⟩ *
        Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel ⟨j₃, z⟩
Module: Mathlib.CategoryTheory.Limits.Yoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : Type w
inst✝ : Category.{t, w} J
F : J ⥤ C
c : Cone F
hc : (X : Cᵒᵖ) → IsLimit ((coyoneda.obj X).mapCone c)
s : Cone F
m : s.pt ⟶ c.pt
hm : ∀ (j : J), m ≫ c.π.app j = s.π.app j
⊢ m = (hom ((hc (op s.pt)).lift ((coyoneda.obj (op s.pt)).mapCone s))) (𝟙 (unop (op s.pt)))

Tactic:
apply (Types.isLimitEquivSections (hc (op s.pt))).injective

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
J : Type w
inst✝ : Category.{t, w} J
F : J ⥤ C
c : Cone F
hc : (X : Cᵒᵖ) → IsLimit ((coyoneda.obj X).mapCone c)
s : Cone F
m : s.pt ⟶ c.pt
hm : ∀ (j : J), m ≫ c.π.app j = s.π.app j
⊢ (Types.isLimitEquivSections (hc (op s.pt))) m =
    (Types.isLimitEquivSections (hc (op s.pt)))
      ((hom ((hc (op s.pt)).lift ((coyoneda.obj (op s.pt)).mapCone s))) (𝟙 (unop (op s.pt))))
Module: Mathlib.CategoryTheory.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X✝ Y✝ : Cᵒᵖ
f : shrinkCoyoneda.{w, v, u}.obj X✝ ⟶ shrinkCoyoneda.{w, v, u}.obj Y✝
⊢ shrinkCoyoneda.{w, v, u}.map (shrinkCoyonedaObjObjEquiv (shrinkCoyonedaEquiv f)).op = f

Tactic:
obtain ⟨f, rfl⟩ := shrinkCoyonedaEquiv.symm.surjective f

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X✝ Y✝ : Cᵒᵖ
f : (shrinkCoyoneda.{w, v, u}.obj Y✝).obj (unop X✝)
⊢ shrinkCoyoneda.{w, v, u}.map (shrinkCoyonedaObjObjEquiv (shrinkCoyonedaEquiv (shrinkCoyonedaEquiv.symm f))).op =
    shrinkCoyonedaEquiv.symm f
Module: Mathlib.Algebra.Category.Grp.Limits

Goal state before:
pp: G H : AddCommGrpCat
f : G ⟶ H
⊢ (kernelIsoKer f).hom ≫ ofHom (Hom.hom f).ker.subtype = kernel.ι f

Tactic:
by ext; rfl

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
X Y Z : C
f : Y ⟶ Z
inst✝ : IsIso f
⊢ X ◁ inv f ≫ X ◁ f = 𝟙 (X ⊗ Z)

Tactic:
by
  rw [← whiskerLeft_comp, IsIso.inv_hom_id, whiskerLeft_id]

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

Goal state before:
pp: R : Type u_1
inst✝¹⁴ : Semiring R
C : Type u_2
inst✝¹³ : Category.{v_1, u_2} C
inst✝¹² : Preadditive C
inst✝¹¹ : Linear R C
inst✝¹⁰ : MonoidalCategory C
inst✝⁹ : MonoidalPreadditive C
inst✝⁸ : MonoidalLinear R C
D : Type u_3
inst✝⁷ : Category.{v_2, u_3} D
inst✝⁶ : Preadditive D
inst✝⁵ : Linear R D
inst✝⁴ : MonoidalCategory D
inst✝³ : MonoidalPreadditive D
F : D ⥤ C
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : Functor.Linear R F
X Y Z : D
r : R
f : Y ⟶ Z
⊢ F.map (X ◁ (r • f)) = F.map (r • X ◁ f)

Tactic:
Functor.Monoidal.map_whiskerLeft

Goal state after:
R : Type u_1
inst✝¹⁴ : Semiring R
C : Type u_2
inst✝¹³ : Category.{v_1, u_2} C
inst✝¹² : Preadditive C
inst✝¹¹ : Linear R C
inst✝¹⁰ : MonoidalCategory C
inst✝⁹ : MonoidalPreadditive C
inst✝⁸ : MonoidalLinear R C
D : Type u_3
inst✝⁷ : Category.{v_2, u_3} D
inst✝⁶ : Preadditive D
inst✝⁵ : Linear R D
inst✝⁴ : MonoidalCategory D
inst✝³ : MonoidalPreadditive D
F : D ⥤ C
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : Functor.Linear R F
X Y Z : D
r : R
f : Y ⟶ Z
⊢ Functor.OplaxMonoidal.δ F X Y ≫ F.obj X ◁ F.map (r • f) ≫ Functor.LaxMonoidal.μ F X Z = F.map (r • X ◁ f)
Module: Mathlib.CategoryTheory.Monoidal.Preadditive

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Finite J
f : J → C
X Y : C
g h : X ⟶ (⨁ f) ⊗ Y
w : ∀ (j : J), g ≫ biproduct.π f j ▷ Y = h ≫ biproduct.π f j ▷ Y
⊢ g = h

Tactic:
cases nonempty_fintype J
  apply (cancel_mono (rightDistributor f Y).hom).mp
  ext
  simp [w]

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Finite J
f : J → C
X Y Z : C
g h : X ⟶ ((⨁ f) ⊗ Y) ⊗ Z
w : ∀ (j : J), g ≫ biproduct.π f j ▷ Y ▷ Z = h ≫ biproduct.π f j ▷ Y ▷ Z
⊢ g = h

Tactic:
apply (cancel_mono (α_ _ _ _).hom).mp
  ext
  simp [w]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: case μ
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F : C ⥤ D
a b : F.Monoidal
eq : a.toOplaxMonoidal = b.toOplaxMonoidal
x✝¹ x✝ : C
⊢ μ F x✝¹ x✝ ≫ (μIso F x✝¹ x✝).inv = μ F x✝¹ x✝ ≫ (μIso F x✝¹ x✝).inv

Tactic:
μIso_inv,

Goal state after:
case μ
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F : C ⥤ D
a b : F.Monoidal
eq : a.toOplaxMonoidal = b.toOplaxMonoidal
x✝¹ x✝ : C
⊢ μ F x✝¹ x✝ ≫ δ F x✝¹ x✝ = μ F x✝¹ x✝ ≫ δ F x✝¹ x✝
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : F.OplaxMonoidal
X : D
⊢ (adj.homEquiv (𝟙_ C ⊗ G.obj X) X).symm (λ_ (G.obj X)).hom =
    (adj.homEquiv (𝟙_ C ⊗ G.obj X) X).symm
      ((adj.homEquiv (𝟙_ C) (𝟙_ D)) (η F) ▷ G.obj X ≫
        (adj.homEquiv (G.obj (𝟙_ D) ⊗ G.obj X) (𝟙_ D ⊗ X))
            (δ F (G.obj (𝟙_ D)) (G.obj X) ≫ (adj.counit.app (𝟙_ D) ⊗ₘ adj.counit.app X)) ≫
          G.map (λ_ X).hom)

Tactic:
homEquiv_counit,

Goal state after:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : F.OplaxMonoidal
X : D
⊢ F.map (λ_ (G.obj X)).hom ≫ adj.counit.app X =
    (adj.homEquiv (𝟙_ C ⊗ G.obj X) X).symm
      ((adj.homEquiv (𝟙_ C) (𝟙_ D)) (η F) ▷ G.obj X ≫
        (adj.homEquiv (G.obj (𝟙_ D) ⊗ G.obj X) (𝟙_ D ⊗ X))
            (δ F (G.obj (𝟙_ D)) (G.obj X) ≫ (adj.counit.app (𝟙_ D) ⊗ₘ adj.counit.app X)) ≫
          G.map (λ_ X).hom)
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : F.OplaxMonoidal
X : D
⊢ F.map (λ_ (G.obj X)).hom ≫ adj.counit.app X =
    (adj.homEquiv (𝟙_ C ⊗ G.obj X) X).symm
      ((adj.homEquiv (𝟙_ C) (𝟙_ D)) (η F) ▷ G.obj X ≫
        (adj.homEquiv (G.obj (𝟙_ D) ⊗ G.obj X) (𝟙_ D ⊗ X))
            (δ F (G.obj (𝟙_ D)) (G.obj X) ≫ (adj.counit.app (𝟙_ D) ⊗ₘ adj.counit.app X)) ≫
          G.map (λ_ X).hom)

Tactic:
homEquiv_counit,

Goal state after:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : F.OplaxMonoidal
X : D
⊢ F.map (λ_ (G.obj X)).hom ≫ adj.counit.app X =
    F.map
        ((adj.homEquiv (𝟙_ C) (𝟙_ D)) (η F) ▷ G.obj X ≫
          (adj.homEquiv (G.obj (𝟙_ D) ⊗ G.obj X) (𝟙_ D ⊗ X))
              (δ F (G.obj (𝟙_ D)) (G.obj X) ≫ (adj.counit.app (𝟙_ D) ⊗ₘ adj.counit.app X)) ≫
            G.map (λ_ X).hom) ≫
      adj.counit.app X
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
X✝ Y Z : C
f : X✝ ⟶ Y
g : X✝ ⟶ Z
inst✝² : HasPushout f g
inst✝¹ : HasPushout (G.map f) (G.map g)
inst✝ : PreservesColimit (span f g) G
c : PushoutCocone f g
X : C
⊢ ∀ (j : WalkingCospan),
    ((Cone.postcompose (isoWhiskerRight (cospanOp f g).symm (yoneda.obj X)).hom).obj
              (Cone.whisker walkingSpanOpEquiv.symm.functor ((yoneda.obj X).mapCone (Cocone.op c)))).π.app
        j =
      (Iso.refl
            ((Cone.postcompose (isoWhiskerRight (cospanOp f g).symm (yoneda.obj X)).hom).obj
                (Cone.whisker walkingSpanOpEquiv.symm.functor ((yoneda.obj X).mapCone (Cocone.op c)))).pt).hom ≫
        ((yoneda.obj X).mapCone c.op).π.app j

Tactic:
by rintro (_ | _ | _) <;> cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : F.OplaxMonoidal
X : D
⊢ (adj.homEquiv (G.obj X ⊗ 𝟙_ C) X).symm (ρ_ (G.obj X)).hom =
    (adj.homEquiv (G.obj X ⊗ 𝟙_ C) X).symm
      (G.obj X ◁ (adj.homEquiv (𝟙_ C) (𝟙_ D)) (η F) ≫
        (adj.homEquiv (G.obj X ⊗ G.obj (𝟙_ D)) (X ⊗ 𝟙_ D))
            (δ F (G.obj X) (G.obj (𝟙_ D)) ≫ (adj.counit.app X ⊗ₘ adj.counit.app (𝟙_ D))) ≫
          G.map (ρ_ X).hom)

Tactic:
homEquiv_counit,

Goal state after:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : F.OplaxMonoidal
X : D
⊢ F.map (ρ_ (G.obj X)).hom ≫ adj.counit.app X =
    (adj.homEquiv (G.obj X ⊗ 𝟙_ C) X).symm
      (G.obj X ◁ (adj.homEquiv (𝟙_ C) (𝟙_ D)) (η F) ≫
        (adj.homEquiv (G.obj X ⊗ G.obj (𝟙_ D)) (X ⊗ 𝟙_ D))
            (δ F (G.obj X) (G.obj (𝟙_ D)) ≫ (adj.counit.app X ⊗ₘ adj.counit.app (𝟙_ D))) ≫
          G.map (ρ_ X).hom)
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : F.OplaxMonoidal
X : D
⊢ F.map (ρ_ (G.obj X)).hom ≫ adj.counit.app X =
    (adj.homEquiv (G.obj X ⊗ 𝟙_ C) X).symm
      ((G.obj X ◁ adj.unit.app (𝟙_ C) ≫ G.obj X ◁ G.map (η F)) ≫
        (adj.unit.app (G.obj X ⊗ G.obj (𝟙_ D)) ≫
            G.map (δ F (G.obj X) (G.obj (𝟙_ D)) ≫ (adj.counit.app X ⊗ₘ adj.counit.app (𝟙_ D)))) ≫
          G.map (ρ_ X).hom)

Tactic:
homEquiv_counit,

Goal state after:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : F.OplaxMonoidal
X : D
⊢ F.map (ρ_ (G.obj X)).hom ≫ adj.counit.app X =
    F.map
        ((G.obj X ◁ adj.unit.app (𝟙_ C) ≫ G.obj X ◁ G.map (η F)) ≫
          (adj.unit.app (G.obj X ⊗ G.obj (𝟙_ D)) ≫
              G.map (δ F (G.obj X) (G.obj (𝟙_ D)) ≫ (adj.counit.app X ⊗ₘ adj.counit.app (𝟙_ D)))) ≫
            G.map (ρ_ X).hom) ≫
      adj.counit.app X
Module: Mathlib.CategoryTheory.ConcreteCategory.EpiMono

Goal state before:
pp: case mp
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
h : MorphismProperty.surjective C = epimorphisms C
⊢ ∀ {X Y : C} (f : X ⟶ Y) [Epi f], Epi ((forget C).map f)

Tactic:
rintro _ _ f (hf : epimorphisms C f)

Goal state after:
case mp
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
h : MorphismProperty.surjective C = epimorphisms C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : epimorphisms C f
⊢ Epi ((forget C).map f)
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : G.LaxMonoidal
X Y Z : C
| (adj.unit.app (X ⊗ Y) ⊗ₘ adj.unit.app Z) ≫
    μ G (F.obj (X ⊗ Y)) (F.obj Z) ≫
      G.map
        ((adj.homEquiv (X ⊗ Y) (F.obj X ⊗ F.obj Y)).symm
              ((adj.unit.app X ⊗ₘ adj.unit.app Y) ≫ μ G (F.obj X) (F.obj Y)) ▷
            F.obj Z ≫
          (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom)

Tactic:
homEquiv_counit,

Goal state after:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : G.LaxMonoidal
X Y Z : C
| (adj.unit.app (X ⊗ Y) ⊗ₘ adj.unit.app Z) ≫
    μ G (F.obj (X ⊗ Y)) (F.obj Z) ≫
      G.map
        ((F.map ((adj.unit.app X ⊗ₘ adj.unit.app Y) ≫ μ G (F.obj X) (F.obj Y)) ≫ adj.counit.app (F.obj X ⊗ F.obj Y)) ▷
            F.obj Z ≫
          (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom)
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : Cᵒᵖ
f : X ⟶ Z
g : X ⟶ Y
inst✝ : HasPushout f g
⊢ ((pushoutIsoOpPullback f g).inv.unop ≫ pullback.fst f.unop g.unop).op = (pushout.inl f g).unop.op

Tactic:
by simp [← pushoutIsoOpPullback_inl_hom]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : G.LaxMonoidal
X Y Z : C
| (α_ X Y Z).hom ≫
    (adj.unit.app X ⊗ₘ adj.unit.app (Y ⊗ Z)) ≫
      G.obj (F.obj X) ◁
          G.map
            ((adj.homEquiv (Y ⊗ Z) (F.obj Y ⊗ F.obj Z)).symm
              ((adj.unit.app Y ⊗ₘ adj.unit.app Z) ≫ μ G (F.obj Y) (F.obj Z))) ≫
        μ G (F.obj X) (F.obj Y ⊗ F.obj Z)

Tactic:
homEquiv_counit,

Goal state after:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : G.LaxMonoidal
X Y Z : C
| (α_ X Y Z).hom ≫
    (adj.unit.app X ⊗ₘ adj.unit.app (Y ⊗ Z)) ≫
      G.obj (F.obj X) ◁
          G.map
            (F.map ((adj.unit.app Y ⊗ₘ adj.unit.app Z) ≫ μ G (F.obj Y) (F.obj Z)) ≫
              adj.counit.app (F.obj Y ⊗ F.obj Z)) ≫
        μ G (F.obj X) (F.obj Y ⊗ F.obj Z)
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : MonoidalCategory C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : MonoidalCategory D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : F.Monoidal
inst✝¹ : G.Monoidal
inst✝ : adj.IsMonoidal
⊢ ε G ≫ G.map (ε F) = adj.unit.app (𝟙_ C)

Tactic:
by
  simp [← adj.unit_app_unit_comp_map_η]

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

Goal state before:
pp: J : Type u
inst✝² : Category.{v, u} J
inst✝¹ : DecidableEq J
F : J ⥤ AddCommGrpCat
inst✝ : Small.{w, max u w} (Quot F)
⊢ desc F (colimitCocone F) = Shrink.addEquiv.symm.toAddMonoidHom

Tactic:
refine Quot.addMonoidHom_ext F (fun j x ↦ ?_)
  simpa only [colimitCocone_pt, AddEquiv.toAddMonoidHom_eq_coe, AddMonoidHom.coe_coe]
    using! Quot.ι_desc F (colimitCocone F) j x

Goal state after:
Module: Mathlib.RingTheory.Congruence.Hom

Goal state before:
pp: case trans
M : Type u_1
N : Type u_2
inst✝¹ : NonAssocSemiring M
inst✝ : NonAssocSemiring N
c : RingCon M
f : M →+* N
h : ker f ≤ c
hf : Surjective ⇑f
this : Equivalence (Relation.Map ⇑c.toSetoid ⇑f ⇑f)
i✝¹ i✝ x✝ y✝ z✝ : N
a✝¹ : RingConGen.Rel (Relation.Map ⇑c ⇑f ⇑f) x✝ y✝
a✝ : RingConGen.Rel (Relation.Map ⇑c ⇑f ⇑f) y✝ z✝
h₁ : Relation.Map (⇑c) (⇑f) (⇑f) x✝ y✝
h₂ : Relation.Map (⇑c) (⇑f) (⇑f) y✝ z✝
⊢ Relation.Map (⇑c) (⇑f) (⇑f) x✝ z✝

Tactic:
exact this.trans h₁ h₂

Goal state after: