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

Goal state before:
pp: case succ
n x : ℕ
ih : ∀ (hx : x < n + 2), ↑((finRotate (n + 2) ^ ↑⟨x, hx⟩) 0) = ↑⟨x, hx⟩
hx : x + 1 < n + 2
⊢ ↑((finRotate (n + 2) ^ ↑⟨x + 1, hx⟩) 0) = ↑⟨x + 1, hx⟩

Tactic:
rw [pow_succ', Perm.mul_apply, coe_finRotate_of_ne_last, ih (lt_trans x.lt_succ_self hx)]

Goal state after:
case succ
n x : ℕ
ih : ∀ (hx : x < n + 2), ↑((finRotate (n + 2) ^ ↑⟨x, hx⟩) 0) = ↑⟨x, hx⟩
hx : x + 1 < n + 2
⊢ (finRotate (n + 2) ^ x) 0 ≠ Fin.last (n + 1)
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: case pos
n : ℕ
i j k : Fin n
h : k < i
hij : i ≤ j
⊢ (i.cycleIcc j) k = k

pp: case neg
n : ℕ
i j k : Fin n
h : k < i
hij : ¬i ≤ j
⊢ (i.cycleIcc j) k = k

Tactic:
· simpa [hij] using Perm.extendDomain_apply_not_subtype _ _ (by
      simp [range_natAdd_castLEEmb]; lia)

Goal state after:
case neg
n : ℕ
i j k : Fin n
h : k < i
hij : ¬i ≤ j
⊢ (i.cycleIcc j) k = k
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: case pos
n : ℕ
i j k : Fin n
h : j < k
hij : i ≤ j
kin : k ∈ Set.range ⇑(natAdd_castLEEmb ⋯)
this :
  ((addNatEmb (n - (n - ↑i))).trans (finCongr ⋯).toEmbedding).toEquivRange.symm ⟨k, kin⟩ = subNat (↑i) (Fin.cast ⋯ k) ⋯
⊢ (j - i).castLT ⋯ < subNat (↑i) (Fin.cast ⋯ k) ⋯

Tactic:
exact lt_def.mpr (by simp [sub_val_of_le hij]; lia)

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

Goal state before:
pp: G : Type u_3
inst✝¹ : Group G
inst✝ : Fintype G
p : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ∣ Fintype.card G
hp' : p - 1 ≠ 0
Scard : p ∣ Fintype.card ↑(vectorsProdEqOne G p)
f : ℕ → ↑(vectorsProdEqOne G p) → ↑(vectorsProdEqOne G p) := fun k v ↦ VectorsProdEqOne.rotate v k
hf1 : ∀ (v : ↑(vectorsProdEqOne G p)), f 0 v = v
hf2 : ∀ (j k : ℕ) (v : ↑(vectorsProdEqOne G p)), f k (f j v) = f (j + k) v
hf3 : ∀ (v : ↑(vectorsProdEqOne G p)), f p v = v
σ : ↑(vectorsProdEqOne G p) ≃ ↑(vectorsProdEqOne G p) :=
  { toFun := f 1, invFun := f (p - 1), left_inv := ⋯, right_inv := ⋯ }
hσ : σ ^ p ^ 1 = 1
v₀ : ↑(vectorsProdEqOne G p) := ⟨List.Vector.replicate p 1, ⋯⟩
hv₀ : σ v₀ = v₀
⊢ ∃ x, orderOf x = p

Tactic:
obtain ⟨v, hv1, hv2⟩ := exists_fixed_point_of_prime' Scard hσ hv₀

Goal state after:
G : Type u_3
inst✝¹ : Group G
inst✝ : Fintype G
p : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ∣ Fintype.card G
hp' : p - 1 ≠ 0
Scard : p ∣ Fintype.card ↑(vectorsProdEqOne G p)
f : ℕ → ↑(vectorsProdEqOne G p) → ↑(vectorsProdEqOne G p) := fun k v ↦ VectorsProdEqOne.rotate v k
hf1 : ∀ (v : ↑(vectorsProdEqOne G p)), f 0 v = v
hf2 : ∀ (j k : ℕ) (v : ↑(vectorsProdEqOne G p)), f k (f j v) = f (j + k) v
hf3 : ∀ (v : ↑(vectorsProdEqOne G p)), f p v = v
σ : ↑(vectorsProdEqOne G p) ≃ ↑(vectorsProdEqOne G p) :=
  { toFun := f 1, invFun := f (p - 1), left_inv := ⋯, right_inv := ⋯ }
hσ : σ ^ p ^ 1 = 1
v₀ : ↑(vectorsProdEqOne G p) := ⟨List.Vector.replicate p 1, ⋯⟩
hv₀ : σ v₀ = v₀
v : ↑(vectorsProdEqOne G p)
hv1 : σ v = v
hv2 : v ≠ v₀
⊢ ∃ x, orderOf x = p
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
hc : c ∈ g.cycleFactorsFinset
⊢ Commute k c ↔
    ∃ (hc' : ∀ (x : α), k x ∈ c.support ↔ x ∈ c.support), k.subtypePerm hc' ∈ Subgroup.zpowers (g.subtypePerm ⋯)

Tactic:
rw [IsCycle.commute_iff' (mem_cycleFactorsFinset_iff.mp hc).1]

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
hc : c ∈ g.cycleFactorsFinset
⊢ (∃ (hc' : ∀ (x : α), k x ∈ c.support ↔ x ∈ c.support), k.subtypePerm hc' ∈ Subgroup.zpowers c.subtypePermOfSupport) ↔
    ∃ (hc' : ∀ (x : α), k x ∈ c.support ↔ x ∈ c.support), k.subtypePerm hc' ∈ Subgroup.zpowers (g.subtypePerm ⋯)
Module: Mathlib.Algebra.Category.Ring.Colimits

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
j : J
⊢ coconeFun F j 1 = 1

Tactic:
apply Quot.sound

Goal state after:
J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
j : J
⊢ (colimitSetoid F) (Prequotient.of j 1) one
Module: Mathlib.Algebra.Category.Ring.Colimits

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
j : J
x✝ y✝ : ↑(F.1 j)
⊢ coconeFun F j (x✝ * y✝) = coconeFun F j x✝ * coconeFun F j y✝

Tactic:
apply Quot.sound

Goal state after:
J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
j : J
x✝ y✝ : ↑(F.1 j)
⊢ (colimitSetoid F) (Prequotient.of j (x✝ * y✝)) ((Prequotient.of j x✝).mul (Prequotient.of j y✝))
Module: Mathlib.Algebra.Category.Ring.Colimits

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
j : J
⊢ coconeFun F j 0 = 0

Tactic:
apply Quot.sound

Goal state after:
J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
j : J
⊢ (colimitSetoid F) (Prequotient.of j 0) zero
Module: Mathlib.Algebra.Category.Ring.Colimits

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
j : J
x✝ y✝ : ↑(F.1 j)
⊢ coconeFun F j (x✝ + y✝) = coconeFun F j x✝ + coconeFun F j y✝

Tactic:
apply Quot.sound

Goal state after:
J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
j : J
x✝ y✝ : ↑(F.1 j)
⊢ (colimitSetoid F) (Prequotient.of j (x✝ + y✝)) ((Prequotient.of j x✝).add (Prequotient.of j y✝))
Module: Mathlib.Algebra.Category.Ring.Colimits

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
j j' : J
f : j ⟶ j'
x✝ : ↑(F.obj j)
⊢ (Hom.hom (F.map f ≫ coconeMorphism F j')) x✝ = (Hom.hom (coconeMorphism F j)) x✝

Tactic:
apply Quot.sound

Goal state after:
J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
j j' : J
f : j ⟶ j'
x✝ : ↑(F.obj j)
⊢ (colimitSetoid F) (Prequotient.of j' ((F.map f).hom' x✝)) (Prequotient.of j x✝)
Module: Mathlib.Algebra.Category.Ring.Colimits

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
j : J
⊢ coconeFun F j 1 = 1

Tactic:
apply Quot.sound

Goal state after:
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
j : J
⊢ (colimitSetoid F) (Prequotient.of j 1) one
Module: Mathlib.Algebra.Category.Ring.Colimits

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
j : J
x✝ y✝ : ↑(F.1 j)
⊢ coconeFun F j (x✝ * y✝) = coconeFun F j x✝ * coconeFun F j y✝

Tactic:
apply Quot.sound

Goal state after:
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
j : J
x✝ y✝ : ↑(F.1 j)
⊢ (colimitSetoid F) (Prequotient.of j (x✝ * y✝)) ((Prequotient.of j x✝).mul (Prequotient.of j y✝))
Module: Mathlib.Algebra.Category.Ring.Colimits

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
j : J
⊢ coconeFun F j 0 = 0

Tactic:
apply Quot.sound

Goal state after:
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
j : J
⊢ (colimitSetoid F) (Prequotient.of j 0) zero
Module: Mathlib.Algebra.Category.Ring.Colimits

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
j : J
x✝ y✝ : ↑(F.1 j)
⊢ coconeFun F j (x✝ + y✝) = coconeFun F j x✝ + coconeFun F j y✝

Tactic:
apply Quot.sound

Goal state after:
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
j : J
x✝ y✝ : ↑(F.1 j)
⊢ (colimitSetoid F) (Prequotient.of j (x✝ + y✝)) ((Prequotient.of j x✝).add (Prequotient.of j y✝))
Module: Mathlib.Algebra.Category.Ring.Colimits

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
j j' : J
f : j ⟶ j'
x✝ : ↑(F.obj j)
⊢ (Hom.hom (F.map f ≫ coconeMorphism F j')) x✝ = (Hom.hom (coconeMorphism F j)) x✝

Tactic:
apply Quot.sound

Goal state after:
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
j j' : J
f : j ⟶ j'
x✝ : ↑(F.obj j)
⊢ (colimitSetoid F) (Prequotient.of j' ((F.map f).hom' x✝)) (Prequotient.of j x✝)
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 n n R
i : n
⊢ (adjp s A * A) i i = detp s A

Tactic:
← detp_transpose,

Goal state after:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
s : ℤˣ
A : Matrix n n R
i : n
⊢ (adjp s A * A) i i = detp s Aᵀ
Module: Mathlib.CategoryTheory.Filtered.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
j₁ j₂ : C
f g h : j₁ ⟶ j₂
⊢ ((h ≫ coeqHom g h) ≫ rightToMax (coeq f g) (coeq g h)) ≫
      coeqHom (coeqHom f g ≫ leftToMax (coeq f g) (coeq g h)) (coeqHom g h ≫ rightToMax (coeq f g) (coeq g h)) =
    h ≫
      (coeqHom g h ≫ rightToMax (coeq f g) (coeq g h)) ≫
        coeqHom (coeqHom f g ≫ leftToMax (coeq f g) (coeq g h)) (coeqHom g h ≫ rightToMax (coeq f g) (coeq g h))

Tactic:
simp only [Category.assoc]

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

Goal state before:
pp: case refine_1
R : Type v
inst✝ : CommRing R
n : ℕ
k : Fin (n + 1)
c : Fin n → R
hc : ∀ (i : Fin n), 0 < i.succ → c i = 0
M N : Matrix (Fin n.succ) (Fin n.succ) R
⊢ (∀ (j : Fin n.succ), M 0 j = N 0 j) →
    (∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j) → M.det = N.det

Tactic:
h0

Goal state after:
case refine_1
R : Type v
inst✝ : CommRing R
n : ℕ
k : Fin (n + 1)
c : Fin n → R
hc : ∀ (i : Fin n), 0 < i.succ → c i = 0
M N : Matrix (Fin n.succ) (Fin n.succ) R
h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j
⊢ (∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j) → M.det = N.det
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: case refine_2
R : Type v
inst✝ : CommRing R
n : ℕ
k✝ : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R),
    (∀ (i : Fin n), k.castSucc < i.succ → c i = 0) →
      ∀ {M N : Matrix (Fin n.succ) (Fin n.succ) R},
        (∀ (j : Fin n.succ), M 0 j = N 0 j) →
          (∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j) → M.det = N.det
c : Fin n → R
hc : ∀ (i : Fin n), k.succ < i.succ → c i = 0
M N : Matrix (Fin n.succ) (Fin n.succ) R
⊢ (∀ (j : Fin n.succ), M 0 j = N 0 j) →
    (∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j) → M.det = N.det

Tactic:
h0

Goal state after:
case refine_2
R : Type v
inst✝ : CommRing R
n : ℕ
k✝ : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R),
    (∀ (i : Fin n), k.castSucc < i.succ → c i = 0) →
      ∀ {M N : Matrix (Fin n.succ) (Fin n.succ) R},
        (∀ (j : Fin n.succ), M 0 j = N 0 j) →
          (∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j) → M.det = N.det
c : Fin n → R
hc : ∀ (i : Fin n), k.succ < i.succ → c i = 0
M N : Matrix (Fin n.succ) (Fin n.succ) R
h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j
⊢ (∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j) → M.det = N.det
Module: Mathlib.CategoryTheory.Limits.Types.ColimitType

Goal state before:
pp: case mpr
J : Type u
inst✝ : Category.{v, u} J
F : J ⥤ Type w₀
c : F.CoconeTypes
⊢ (∀ (z : c.pt), ∃ i x, c.ι i x = z) → Function.Surjective (F.descColimitType c)

Tactic:
· intro h z
    obtain ⟨i, x, rfl⟩ := h z
    exact ⟨F.ιColimitType i x, rfl⟩

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

Goal state before:
pp: J : Type u
inst✝ : Category.{v, u} J
F : J ⥤ Type w₀
c : F.CoconeTypes
hc : c.IsColimit
y : c.pt
⊢ ∃ j x, c.ι j x = y

Tactic:
obtain ⟨z, rfl⟩ := hc.equiv.surjective y

Goal state after:
J : Type u
inst✝ : Category.{v, u} J
F : J ⥤ Type w₀
c : F.CoconeTypes
hc : c.IsColimit
z : F.ColimitType
⊢ ∃ j x, c.ι j x = hc.equiv z
Module: Mathlib.CategoryTheory.Limits.Types.Colimits

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
t : Cocone F
h : IsColimit t
x : t.pt
hx : ∀ (x_1 : J) (x_2 : F.obj x_1), ¬(hom (t.ι.app x_1)) x_2 = x
⊢ (↾fun x ↦ { down := True }) = ↾fun y ↦ { down := y ≠ x }

Tactic:
refine h.hom_ext fun j ↦ ?_
    ext y
    simp only [TypeCat.Fun.toFun_apply, comp_apply, hom_ofHom,
      TypeCat.Fun.coe_mk, ne_eq, true_iff]
    exact hx j y

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

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
j : J
x : ↑(F.obj j)
⊢ M.mk F ⟨j, 1⟩ * M.mk F ⟨j, x⟩ = M.mk F ⟨j, x⟩

Tactic:
colimit_mul_mk_eq',

Goal state after:
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
j : J
x : ↑(F.obj j)
⊢ M.mk F ⟨j, 1 * x⟩ = M.mk F ⟨j, x⟩
Module: Mathlib.Algebra.Category.MonCat.FilteredColimits

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
j : J
x : ↑(F.obj j)
⊢ M.mk F ⟨j, x⟩ * M.mk F ⟨j, 1⟩ = M.mk F ⟨j, x⟩

Tactic:
colimit_mul_mk_eq',

Goal state after:
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
j : J
x : ↑(F.obj j)
⊢ M.mk F ⟨j, x * 1⟩ = M.mk F ⟨j, x⟩
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: case convert_2
m : Type u_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
σ : Perm (m ⊕ n)
hσn : σ ∉ (↑(sumCongrHom m n).range).toFinset
⊢ ↑↑(sign σ) * ∏ i, fromBlocks A B 0 D (σ i) i = 0

Tactic:
have h1 : ¬∀ x, ∃ y, Sum.inl y = σ (Sum.inl x) := by
        rw [Set.mem_toFinset] at hσn
        simpa only [Set.MapsTo, Set.mem_range, forall_exists_index, forall_apply_eq_imp_iff] using
          mt mem_sumCongrHom_range_of_perm_mapsTo_inl hσn

Goal state after:
case convert_2
m : Type u_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
σ : Perm (m ⊕ n)
hσn : σ ∉ (↑(sumCongrHom m n).range).toFinset
h1 : ¬∀ (x : m), ∃ y, Sum.inl y = σ (Sum.inl x)
⊢ ↑↑(sign σ) * ∏ i, fromBlocks A B 0 D (σ i) i = 0
Module: Mathlib.CategoryTheory.Functor.Currying

Goal state before:
pp: B : Type u₁
inst✝⁴ : Category.{v₁, u₁} B
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
D : Type u₃
inst✝² : Category.{v₃, u₃} D
E : Type u₄
inst✝¹ : Category.{v₄, u₄} E
H : Type u₅
inst✝ : Category.{v₅, u₅} H
X✝ Y✝ : C ⥤ D ⥤ E
T : X✝ ⟶ Y✝
X Y : C × D
f : X ⟶ Y
⊢ { obj := fun X ↦ (X✝.obj X.1).obj X.2, map := fun {X Y} f ↦ (X✝.map f.1).app X.2 ≫ (X✝.obj Y.1).map f.2, map_id := ⋯,
            map_comp := ⋯ }.map
        f ≫
      (T.app Y.1).app Y.2 =
    (T.app X.1).app X.2 ≫
      { obj := fun X ↦ (Y✝.obj X.1).obj X.2, map := fun {X Y} f ↦ (Y✝.map f.1).app X.2 ≫ (Y✝.obj Y.1).map f.2,
            map_id := ⋯, map_comp := ⋯ }.map
        f

Tactic:
simp only [Category.assoc]

Goal state after:
B : Type u₁
inst✝⁴ : Category.{v₁, u₁} B
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
D : Type u₃
inst✝² : Category.{v₃, u₃} D
E : Type u₄
inst✝¹ : Category.{v₄, u₄} E
H : Type u₅
inst✝ : Category.{v₅, u₅} H
X✝ Y✝ : C ⥤ D ⥤ E
T : X✝ ⟶ Y✝
X Y : C × D
f : X ⟶ Y
⊢ (X✝.map f.1).app X.2 ≫ (X✝.obj Y.1).map f.2 ≫ (T.app Y.1).app Y.2 =
    (T.app X.1).app X.2 ≫ (Y✝.map f.1).app X.2 ≫ (Y✝.obj Y.1).map f.2
Module: Mathlib.CategoryTheory.Functor.Currying

Goal state before:
pp: B : Type u₁
inst✝⁴ : Category.{v₁, u₁} B
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
D : Type u₃
inst✝² : Category.{v₃, u₃} D
E : Type u₄
inst✝¹ : Category.{v₄, u₄} E
H : Type u₅
inst✝ : Category.{v₅, u₅} H
X✝ Y✝ : C × D ⥤ E
T : X✝ ⟶ Y✝
X X' : C
f : X ⟶ X'
⊢ X✝.curryObj.map f ≫ { app := fun Y ↦ T.app (X', Y), naturality := ⋯ } =
    { app := fun Y ↦ T.app (X, Y), naturality := ⋯ } ≫ Y✝.curryObj.map f

Tactic:
by
        ext; dsimp [curryObj]
        rw [NatTrans.naturality]

Goal state after:
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 ι
inst✝ : Fintype ι
x h h' : (i : ι) → M₁ i
⊢ f x - f x +
        ((f.linearDeriv x) h - (f.linearDeriv x) h' +
          (∑ s with 2 ≤ #s, f (s.piecewise h x) - ∑ s with 2 ≤ #s, f (s.piecewise h' x))) -
      (f.linearDeriv x) (h - h') =
    ∑ s with 2 ≤ #s, (f (s.piecewise h x) - f (s.piecewise h' x))

Tactic:
sub_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 ι
inst✝ : Fintype ι
x h h' : (i : ι) → M₁ i
⊢ 0 +
        ((f.linearDeriv x) h - (f.linearDeriv x) h' +
          (∑ s with 2 ≤ #s, f (s.piecewise h x) - ∑ s with 2 ≤ #s, f (s.piecewise h' x))) -
      (f.linearDeriv x) (h - h') =
    ∑ s with 2 ≤ #s, (f (s.piecewise h x) - f (s.piecewise h' x))
Module: Mathlib.CategoryTheory.Limits.Creates

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✝ : J ⥤ C
J' : Type w₁
inst✝¹ : Category.{w'₁, w₁} J'
e : J ≌ J'
F : C ⥤ D
inst✝ : CreatesLimitsOfShape J F
K : J' ⥤ C
c : Cone (K ⋙ F)
hc : IsLimit c
⊢ LiftableCone K F c

Tactic:
refine ⟨(Cone.whiskeringEquivalence e).inverse.obj
          (liftLimit (hc.whiskerEquivalence e)), ?_⟩
        letI inner := (Cone.whiskeringEquivalence (F := K ⋙ F) e).inverse.mapIso
          (liftedLimitMapsToOriginal (K := e.functor ⋙ K) (hc.whiskerEquivalence e))
        refine ?_ ≪≫ inner ≪≫ ((Cone.whiskeringEquivalence e).unitIso.app c).symm
        exact Cone.ext (Iso.refl _)

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

Goal state before:
pp: J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ CommMonCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget CommMonCat).sections
⊢ CreatesLimit F (forget CommMonCat)

Tactic:
set e : forget CommMonCat.{u} ≅ forget₂ CommMonCat.{u} MonCat.{u} ⋙ forget MonCat.{u} :=
    NatIso.ofComponents (fun _ ↦ Iso.refl _) (fun _ ↦ rfl)

Goal state after:
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ CommMonCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget CommMonCat).sections
e : forget CommMonCat ≅ forget₂ CommMonCat MonCat ⋙ forget MonCat :=
  NatIso.ofComponents (fun x ↦ Iso.refl ((forget CommMonCat).obj x)) ⋯
⊢ CreatesLimit F (forget CommMonCat)
Module: Mathlib.Algebra.Category.Grp.Limits

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ CommGrpCat
c : Cone (F ⋙ forget₂ CommGrpCat GrpCat)
hc : IsLimit c
this✝¹ : HasLimit (F ⋙ forget₂ CommGrpCat GrpCat)
this✝ : Small.{u, max u v} ↑(F ⋙ forget CommGrpCat).sections
this : Small.{u, max u v} ↑((F ⋙ forget₂ CommGrpCat GrpCat ⋙ forget₂ GrpCat MonCat) ⋙ forget MonCat).sections
⊢ LiftsToLimit F (forget₂ CommGrpCat GrpCat) c hc

Tactic:
have : Small.{u} ((F ⋙ forget₂ CommGrpCat GrpCat) ⋙ forget GrpCat).sections := this

Goal state after:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ CommGrpCat
c : Cone (F ⋙ forget₂ CommGrpCat GrpCat)
hc : IsLimit c
this✝² : HasLimit (F ⋙ forget₂ CommGrpCat GrpCat)
this✝¹ : Small.{u, max u v} ↑(F ⋙ forget CommGrpCat).sections
this✝ : Small.{u, max u v} ↑((F ⋙ forget₂ CommGrpCat GrpCat ⋙ forget₂ GrpCat MonCat) ⋙ forget MonCat).sections
this : Small.{u, max u v} ↑((F ⋙ forget₂ CommGrpCat GrpCat) ⋙ forget GrpCat).sections
⊢ LiftsToLimit F (forget₂ CommGrpCat GrpCat) c hc
Module: Mathlib.Algebra.Category.Grp.Limits

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
G H : AddCommGrpCat
f : G ⟶ H
⊢ kernel.lift f (ofHom (Hom.hom f).ker.subtype) ⋯ ≫
      ofHom { toFun := fun g ↦ ⟨(ConcreteCategory.hom (kernel.ι f)) g, ⋯⟩, map_zero' := ⋯, map_add' := ⋯ } =
    𝟙 (of ↥(Hom.hom f).ker)

Tactic:
apply AddCommGrpCat.ext
    rintro ⟨x, mem⟩
    refine Subtype.ext ?_
    apply ConcreteCategory.congr_hom (kernel.lift_ι f _ _)

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategoryStruct D
F : D ⥤ C
inst✝ : F.Faithful
fData : InducingFunctorData F
W X Y Z : D
⊢ (fData.μIso (W ⊗ X) Y).inv ▷ F.obj Z ≫
      (fData.μIso W X).inv ▷ F.obj Y ▷ F.obj Z ≫
        (α_ (F.obj W) (F.obj X) (F.obj Y)).hom ▷ F.obj Z ≫
          (α_ (F.obj W) (F.obj X ⊗ F.obj Y) (F.obj Z)).hom ≫
            (((F.obj W ◁ 𝟙 ((F.obj X ⊗ F.obj Y) ⊗ F.obj Z) ≫ F.obj W ◁ (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom) ≫
                  F.obj W ◁ F.obj X ◁ (fData.μIso Y Z).hom) ≫
                F.obj W ◁ (fData.μIso X (Y ⊗ Z)).hom) ≫
              (fData.μIso W (X ⊗ Y ⊗ Z)).hom =
    (fData.μIso (W ⊗ X) Y).inv ▷ F.obj Z ≫
      (α_ (F.obj (W ⊗ X)) (F.obj Y) (F.obj Z)).hom ≫
        F.obj (W ⊗ X) ◁ (fData.μIso Y Z).hom ≫
          (fData.μIso W X).inv ▷ F.obj (Y ⊗ Z) ≫
            (α_ (F.obj W) (F.obj X) (F.obj (Y ⊗ Z))).hom ≫
              F.obj W ◁ (fData.μIso X (Y ⊗ Z)).hom ≫ (fData.μIso W (X ⊗ Y ⊗ Z)).hom

Tactic:
whisker_exchange_assoc

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategoryStruct D
F : D ⥤ C
inst✝ : F.Faithful
fData : InducingFunctorData F
W X Y Z : D
⊢ (fData.μIso (W ⊗ X) Y).inv ▷ F.obj Z ≫
      (fData.μIso W X).inv ▷ F.obj Y ▷ F.obj Z ≫
        (α_ (F.obj W) (F.obj X) (F.obj Y)).hom ▷ F.obj Z ≫
          (α_ (F.obj W) (F.obj X ⊗ F.obj Y) (F.obj Z)).hom ≫
            (((F.obj W ◁ 𝟙 ((F.obj X ⊗ F.obj Y) ⊗ F.obj Z) ≫ F.obj W ◁ (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom) ≫
                  F.obj W ◁ F.obj X ◁ (fData.μIso Y Z).hom) ≫
                F.obj W ◁ (fData.μIso X (Y ⊗ Z)).hom) ≫
              (fData.μIso W (X ⊗ Y ⊗ Z)).hom =
    (fData.μIso (W ⊗ X) Y).inv ▷ F.obj Z ≫
      (α_ (F.obj (W ⊗ X)) (F.obj Y) (F.obj Z)).hom ≫
        (fData.μIso W X).inv ▷ (F.obj Y ⊗ F.obj Z) ≫
          (F.obj W ⊗ F.obj X) ◁ (fData.μIso Y Z).hom ≫
            (α_ (F.obj W) (F.obj X) (F.obj (Y ⊗ Z))).hom ≫
              F.obj W ◁ (fData.μIso X (Y ⊗ Z)).hom ≫ (fData.μIso W (X ⊗ Y ⊗ Z)).hom
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
M N : SemimoduleCat R
x : ↑M
y : ↑(of R R)
⊢ ∀ (z : ↑N),
    (Hom.hom ((associator M (of R R) N).hom ≫ tensorHom (𝟙 M) (leftUnitor N).hom)) (x ⊗ₜ[R] y ⊗ₜ[R] z) =
      (Hom.hom (tensorHom (rightUnitor M).hom (𝟙 N))) (x ⊗ₜ[R] y ⊗ₜ[R] z)

Tactic:
exact TensorProduct.tmul_smul _ _

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f g f' : C
η θ : f ⟶ g
η' θ' : f ≅ g
η_f : 𝟙_ C ⊗ f ≅ f'
η_g : 𝟙_ C ⊗ g ≅ f'
η_hom : η'.hom = η
Θ_hom : θ'.hom = θ
Hη : 𝟙_ C ◁ η' ≪≫ η_g = η_f
Hθ : 𝟙_ C ◁ θ' ≪≫ η_g = η_f
⊢ (λ_ f).inv ≫ η_f.hom ≫ η_g.inv ≫ (λ_ g).hom = θ'.hom

Tactic:
simp [← reassoc_of% (congrArg Iso.hom Hθ)]

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 ⥤ E
inst✝¹ : F.OplaxMonoidal
inst✝ : G.OplaxMonoidal
X Y Z : C
⊢ G.map (δ F (X ⊗ Y) Z) ≫
      δ G (F.obj (X ⊗ Y)) (F.obj Z) ≫
        G.map (δ F X Y) ▷ G.obj (F.obj Z) ≫
          δ G (F.obj X) (F.obj Y) ▷ G.obj (F.obj Z) ≫ (α_ (G.obj (F.obj X)) (G.obj (F.obj Y)) (G.obj (F.obj Z))).hom =
    G.map (F.map (α_ X Y Z).hom) ≫
      G.map (δ F X (Y ⊗ Z)) ≫
        δ G (F.obj X) (F.obj (Y ⊗ Z)) ≫ G.obj (F.obj X) ◁ (G.map (δ F Y Z) ≫ δ G (F.obj Y) (F.obj Z))

Tactic:
δ_natural_left_assoc,

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 ⥤ E
inst✝¹ : F.OplaxMonoidal
inst✝ : G.OplaxMonoidal
X Y Z : C
⊢ G.map (δ F (X ⊗ Y) Z) ≫
      G.map (δ F X Y ▷ F.obj Z) ≫
        δ G (F.obj X ⊗ F.obj Y) (F.obj Z) ≫
          δ G (F.obj X) (F.obj Y) ▷ G.obj (F.obj Z) ≫ (α_ (G.obj (F.obj X)) (G.obj (F.obj Y)) (G.obj (F.obj Z))).hom =
    G.map (F.map (α_ X Y Z).hom) ≫
      G.map (δ F X (Y ⊗ Z)) ≫
        δ G (F.obj X) (F.obj (Y ⊗ Z)) ≫ G.obj (F.obj X) ◁ (G.map (δ F Y Z) ≫ δ G (F.obj Y) (F.obj Z))