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

Goal state before:
pp: β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
val✝ : Fintype β
x : β
hx : f x ≠ x
a b : ℕ
hx' : (f ^ a) x = (f ^ b) x
hab : a ≤ b
⊢ f ^ a = f ^ b

Tactic:
suffices f ^ (b - a) = 1 by
        rw [pow_sub _ hab, mul_inv_eq_one] at this
        rw [this]

Goal state after:
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
val✝ : Fintype β
x : β
hx : f x ≠ x
a b : ℕ
hx' : (f ^ a) x = (f ^ b) x
hab : a ≤ b
⊢ f ^ (b - a) = 1
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f : Perm α
s : Set α
x : α
hf : f.IsCycleOn s
hx : f x ∈ s
⊢ x ∈ s

Tactic:
by simpa using hf.1.perm_inv.1 hx

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

Goal state before:
pp: case inr
α : Type u_2
f : Perm α
s : Finset α
hf : f.IsCycleOn ↑s
h✝ : (↑s).Nontrivial
⊢ (↑(range #s)).PairwiseDisjoint fun k ↦ map { toFun := fun i ↦ (i, (f ^ k) i), inj' := ⋯ } s

Tactic:
classical
    rintro m hm n hn hmn
    simp only [disjoint_left, Function.onFun, mem_map, Function.Embedding.coeFn_mk,
      not_exists, not_and, forall_exists_index, and_imp, Prod.forall, Prod.mk_inj]
    rintro _ _ _ - rfl rfl a ha rfl h
    rw [hf.pow_apply_eq_pow_apply ha] at h
    rw [mem_coe, mem_range] at hm hn
    exact hmn.symm (h.eq_of_lt_of_lt hn hm)

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

Goal state before:
pp: α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c.IsCycle
hc' : ∀ (x : α), g x ∈ c.support ↔ x ∈ c.support
i : ℤ
hi : (fun x ↦ c.subtypePermOfSupport ^ x) i = g.subtypePerm hc'
x : α
hx : x ∈ c.support
hi' : ∀ x ∈ c.support, g x = (c ^ i) x
⊢ g (c x) = c (g x)

Tactic:
rw [hi' x hx, hi' (c x) (apply_mem_support.mpr hx)]

Goal state after:
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c.IsCycle
hc' : ∀ (x : α), g x ∈ c.support ↔ x ∈ c.support
i : ℤ
hi : (fun x ↦ c.subtypePermOfSupport ^ x) i = g.subtypePerm hc'
x : α
hx : x ∈ c.support
hi' : ∀ x ∈ c.support, g x = (c ^ i) x
⊢ (c ^ i) (c x) = c ((c ^ i) x)
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c.IsCycle
hc' : ∀ (x : α), g x ∈ c.support ↔ x ∈ c.support
k : ℤ
⊢ c.subtypePermOfSupport ^ k = g.subtypePerm ⋯ ↔ c ^ k = ofSubtype (g.subtypePerm ⋯)

Tactic:
rw [subtypePermOfSupport, subtypePerm_zpow c k]

Goal state after:
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c.IsCycle
hc' : ∀ (x : α), g x ∈ c.support ↔ x ∈ c.support
k : ℤ
⊢ (c ^ k).subtypePerm ⋯ = g.subtypePerm ⋯ ↔ c ^ k = ofSubtype (g.subtypePerm ⋯)
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
G : Type u_2
inst✝ : Group G
n : ℕ
⊢ Unique ↑(vectorsProdEqOne G 0)

Tactic:
rw [zero_eq]
  exact Set.uniqueSingleton Vector.nil

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
s : ↑(vectorsProdEqOne G p)
⊢ f 1 (f (p - 1) s) = s

Tactic:
rw [hf2, tsub_add_cancel_of_le hp.out.one_lt.le, hf3]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f p : Perm α
⊢ p ∈ f.cycleFactorsFinset ↔ p.IsCycle ∧ ∀ a ∈ p.support, p a = f a

Tactic:
by
  obtain ⟨l, hl, hl'⟩ := f.cycleFactorsFinset.exists_list_nodup_eq
  rw [← hl']
  rw [eq_comm, cycleFactorsFinset_eq_list_toFinset hl] at hl'
  simpa [List.mem_toFinset, Ne, ← hl'.right.right] using
    mem_list_cycles_iff hl'.left hl'.right.left

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

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝ : CommRing R
σ : Perm (Fin n)
f : Fin n → Fin n → R
hf : ∀ (i j : Fin n), f i j = -f j i
⊢ ∏ x ∈ Finset.univ.sigma Finset.Iio, f (σ x.snd) (σ x.fst) =
    ∏ x ∈ Finset.univ.sigma Finset.Iio, ↑↑(if σ⁻¹ x.snd < σ⁻¹ x.fst then 1 else -1) * f x.snd x.fst

Tactic:
set D := (Finset.univ : Finset (Fin n)).sigma Finset.Iio with hD

Goal state after:
n : ℕ
R : Type u_1
inst✝ : CommRing R
σ : Perm (Fin n)
f : Fin n → Fin n → R
hf : ∀ (i j : Fin n), f i j = -f j i
D : Finset ((_ : Fin n) × Fin n) := Finset.univ.sigma Finset.Iio
hD : D = Finset.univ.sigma Finset.Iio
⊢ ∏ x ∈ D, f (σ x.snd) (σ x.fst) = ∏ x ∈ D, ↑↑(if σ⁻¹ x.snd < σ⁻¹ x.fst then 1 else -1) * f x.snd x.fst
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
⊢ f = g → (g.IsCycle ↔ f.IsCycle)

Tactic:
rintro rfl

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
⊢ f.IsCycle ↔ f.IsCycle
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : Perm α
⊢ IsConj σ τ ↔ σ.partition = τ.partition

Tactic:
rw [isConj_iff_cycleType_eq]
  refine ⟨fun h => ?_, fun h => ?_⟩
  · rw [Nat.Partition.ext_iff, parts_partition, parts_partition, ← sum_cycleType, ← sum_cycleType,
      h]
  · rw [← filter_parts_partition_eq_cycleType, ← filter_parts_partition_eq_cycleType, h]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h : σ.IsThreeCycle
⊢ σ ≠ 1

Tactic:
rintro rfl

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h : IsThreeCycle 1
⊢ False
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h : #σ.support = 3
h0 : σ.cycleType = 0
⊢ σ.IsThreeCycle

pp: case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h : #σ.support = 3
h0 : ¬σ.cycleType = 0
⊢ σ.IsThreeCycle

Tactic:
· rw [← sum_cycleType, h0, sum_zero] at h
    exact (ne_of_lt zero_lt_three h).elim

Goal state after:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h : #σ.support = 3
h0 : ¬σ.cycleType = 0
⊢ σ.IsThreeCycle
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : c ∈ g.cycleFactorsFinset
x : α
⊢ c = g.cycleOf x → x ∈ c.support

Tactic:
rintro rfl

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
x : α
hc : g.cycleOf x ∈ g.cycleFactorsFinset
⊢ x ∈ (g.cycleOf x).support
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case neg
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : c ∈ g.cycleFactorsFinset
c' : Perm α
hc' : c' ∈ g.cycleFactorsFinset
hcc' : ¬c = c'
⊢ c ≠ c'

Tactic:
exact hcc'

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
⊢ g.support = {a, g a, g (g a)} → a ∈ g.support

pp: case mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
⊢ a ∈ g.support → g.support = {a, g a, g (g a)}

Tactic:
· intro hg; simp [hg]

Goal state after:
case mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
⊢ a ∈ g.support → g.support = {a, g a, g (g a)}
Module: Mathlib.LinearAlgebra.Multilinear.Basis

Goal state before:
pp: case intro
ι : Type u_1
R : Type u_2
inst✝⁵ : CommSemiring R
M : ι → Type u_3
inst✝⁴ : (i : ι) → AddCommMonoid (M i)
inst✝³ : (i : ι) → Module R (M i)
N : Type u_4
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : Finite ι
f g : MultilinearMap R M N
ιM : ι → Type u_5
e : (i : ι) → Basis (ιM i) R (M i)
h : ∀ (v : (i : ι) → ιM i), (f fun i ↦ (e i) (v i)) = g fun i ↦ (e i) (v i)
val✝ : Fintype ι
⊢ f = g

Tactic:
ext m

Goal state after:
case intro
ι : Type u_1
R : Type u_2
inst✝⁵ : CommSemiring R
M : ι → Type u_3
inst✝⁴ : (i : ι) → AddCommMonoid (M i)
inst✝³ : (i : ι) → Module R (M i)
N : Type u_4
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : Finite ι
f g : MultilinearMap R M N
ιM : ι → Type u_5
e : (i : ι) → Basis (ιM i) R (M i)
h : ∀ (v : (i : ι) → ιM i), (f fun i ↦ (e i) (v i)) = g fun i ↦ (e i) (v i)
val✝ : Fintype ι
m : (i : ι) → M i
⊢ f m = g m
Module: Mathlib.LinearAlgebra.Multilinear.DFinsupp

Goal state before:
pp: case ha
ι : Type uι
κ : ι → Type uκ
R : Type uR
ι' : Type u_1
inst✝⁶ : DecidableEq ι
inst✝⁵ : Fintype ι
inst✝⁴ : CommSemiring R
inst✝³ : (i : ι) → Fintype (κ i)
inst✝² : (i : ι) → DecidableEq (κ i)
inst✝¹ : DecidableEq ι'
inst✝ : Fintype ι'
f✝ : Π₀ (x : ((i : ι) → κ i) × ι'), R
x : (i : ι) → Π₀ (x : κ i), R
p : ((i : ι) → κ i) × ι'
r : R
f : Π₀ (i : ((i : ι) → κ i) × ι'), R
hfx : (freeDFinsuppEquiv f) x = ∑ p, f p • DFinsupp.single p.2 (∏ i, (x i) (p.1 i))
⊢ (freeDFinsuppEquiv (DFinsupp.single p r + f)) x =
    ∑ p_1, (DFinsupp.single p r + f) p_1 • DFinsupp.single p_1.2 (∏ i, (x i) (p_1.1 i))

Tactic:
simp [Finset.sum_add_distrib, add_smul, hfx]

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
a b : R
h : IsDetpBalanced 1 a b
⊢ a = b

Tactic:
simpa [IsDetpBalanced] using h

Goal state after:
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)
⊢ (ConcreteCategory.hom (coconeMorphism F j')) ((ConcreteCategory.hom (F.map f)) x) =
    (ConcreteCategory.hom (F.map f ≫ coconeMorphism F j')) x

Tactic:
comp_apply

Goal state after:
J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
j j' : J
f : j ⟶ j'
x : ↑(F.obj j)
⊢ (ConcreteCategory.hom (coconeMorphism F j')) ((ConcreteCategory.hom (F.map f)) x) =
    (ConcreteCategory.hom (coconeMorphism F j')) ((ConcreteCategory.hom (F.map f)) x)
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)
⊢ (ConcreteCategory.hom (coconeMorphism F j')) ((ConcreteCategory.hom (F.map f)) x) =
    (ConcreteCategory.hom (F.map f ≫ coconeMorphism F j')) x

Tactic:
comp_apply

Goal state after:
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
j j' : J
f : j ⟶ j'
x : ↑(F.obj j)
⊢ (ConcreteCategory.hom (coconeMorphism F j')) ((ConcreteCategory.hom (F.map f)) x) =
    (ConcreteCategory.hom (coconeMorphism F j')) ((ConcreteCategory.hom (F.map f)) 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
A B : Matrix n n R
d : n → R
hAB : A * B = diagonal d
s t : ℤˣ
σ : Perm n
hσ : sign σ = s
τ : Perm n
hτ : sign τ = t
k : n
hk : ¬k = τ (σ k)
⊢ IsAddUnit ((A k (σ k) * B (σ k) (τ (σ k))) • ∏ x ∈ univ.erase k, A x (σ x) * B (σ x) (τ (σ x)))

Tactic:
exact (isAddUnit_mul hAB k (τ (σ k)) (σ k) hk).smul_right _

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
α : Type u
inst✝ : SemilatticeInf α
X Y : α
f g : X ⟶ Y
⊢ 𝟙 X ≫ f = 𝟙 X ≫ g

Tactic:
by
    apply ULift.ext
    subsingleton

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
α : Type u
inst✝¹ : Preorder α
inst✝ : IsCodirectedOrder α
X Y : α
f g : X ⟶ Y
⊢ 𝟙 X ≫ f = 𝟙 X ≫ g

Tactic:
by
    apply ULift.ext
    subsingleton

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : Discrete PUnit.{u_1 + 1}
f g : X ⟶ Y
⊢ { down := { down := ⋯ } } ≫ f = { down := { down := ⋯ } } ≫ g

Tactic:
by
    apply ULift.ext
    subsingleton

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

Goal state before:
pp: case mp.mk
J : Type u
inst✝ : Category.{v, u} J
F : J ⥤ Type w₀
c : F.CoconeTypes
h : Function.Surjective (F.descColimitType c)
w✝ : F.ColimitType
i : J
x : F.obj i
⊢ ∃ i_1 x_1, c.ι i_1 x_1 = F.descColimitType c (Quot.mk F.ColimitTypeRel ⟨i, x⟩)

Tactic:
exact ⟨i, x, rfl⟩

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

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
c : F.CoconeTypes
hc : c.IsColimit
s : Cocone F
j : J
⊢ ((F.coconeTypesEquiv c).ι.app j ≫ ↾fun x ↦ hc.desc (F.coconeTypesEquiv.symm s) x) = s.ι.app j

Tactic:
ext x
          exact congr_fun (hc.fac (F.coconeTypesEquiv.symm s) j) x

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
o : Type u_3
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
⊢ ∑ σ, ↑↑(sign σ) * ∏ i, blockDiagonal M (σ i) i = ∏ x, ∑ σ, ↑↑(sign σ) * ∏ i, M x (σ i) i

Tactic:
Finset.prod_sum

Goal state after:
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
R : Type v
inst✝² : CommRing R
o : Type u_3
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
⊢ ∑ σ, ↑↑(sign σ) * ∏ i, blockDiagonal M (σ i) i =
    ∑ p ∈ univ.pi fun x ↦ univ, ∏ x ∈ univ.attach, ↑↑(sign (p ↑x ⋯)) * ∏ i, M (↑x) ((p ↑x ⋯) i) i
Module: Mathlib.Algebra.Category.MonCat.FilteredColimits

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
j₁ : J
y : ↑(F.obj j₁)
j₂ : J
x : ↑(F.obj j₂)
j₃ : J
y' : ↑(F.obj j₃)
l : J
f : ⟨j₁, y⟩.fst ⟶ l
g : ⟨j₃, y'⟩.fst ⟶ l
hfg :
  (ConcreteCategory.hom ((F ⋙ forget MonCat).map f)) ⟨j₁, y⟩.snd =
    (ConcreteCategory.hom ((F ⋙ forget MonCat).map g)) ⟨j₃, y'⟩.snd
⊢ colimitMulAux F ⟨j₂, x⟩ ⟨j₁, y⟩ = colimitMulAux F ⟨j₂, x⟩ ⟨j₃, y'⟩

Tactic:
simp only [Functor.comp_obj, Functor.comp_map, ConcreteCategory.hom_ofHom,
    TypeCat.Fun.coe_mk] at hfg

Goal state after:
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
j₁ : J
y : ↑(F.obj j₁)
j₂ : J
x : ↑(F.obj j₂)
j₃ : J
y' : ↑(F.obj j₃)
l : J
f : ⟨j₁, y⟩.fst ⟶ l
g : ⟨j₃, y'⟩.fst ⟶ l
hfg : (ConcreteCategory.hom (F.map f)) y = (ConcreteCategory.hom (F.map g)) y'
⊢ colimitMulAux F ⟨j₂, x⟩ ⟨j₁, y⟩ = colimitMulAux F ⟨j₂, x⟩ ⟨j₃, y'⟩
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✝ : LinearOrder ι
a b v : (i : ι) → M₁ i
s : Finset ι
⊢ f (s.piecewise a v) - f (s.piecewise b (s.piecewise a v)) =
    ∑ i ∈ s, f fun j ↦ if j ∈ s then if j < i then a j else if j = i then a j - b j else b j else v j

Tactic:
map_sub_map_piecewise

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✝ : LinearOrder ι
a b v : (i : ι) → M₁ i
s : Finset ι
⊢ (∑ i ∈ s, f fun j ↦ if j ∈ s → j < i then s.piecewise a v j else if i = j then s.piecewise a v j - b j else b j) =
    ∑ i ∈ s, f fun j ↦ if j ∈ s then if j < i then a j else if j = i then a j - b j else b j else v j
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
K : Type u₂
inst✝ : Category.{v₂, u₂} K
F : J ⥤ K ⥤ C
c : Cone F
t : (k : K) → IsLimit (((evaluation K C).obj k).mapCone c)
s : Cone F
m : s.pt ⟶ c.pt
w : ∀ (j : J), m ≫ c.π.app j = s.π.app j
⊢ m =
    { app := fun k ↦ (t k).lift { pt := s.pt.obj k, π := whiskerRight s.π ((evaluation K C).obj k) }, naturality := ⋯ }

Tactic:
by
    ext x
    exact (t x).hom_ext fun j =>
      (congr_app (w j) x).trans
        ((t x).fac ⟨s.pt.obj _, whiskerRight s.π ((evaluation K C).obj _)⟩ j).symm

Goal state after:
Module: Mathlib.CategoryTheory.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X : Cᵒᵖ
P Q : C ⥤ Type w
α : shrinkCoyoneda.{w, v, u}.obj X ⟶ P
β : P ⟶ Q
⊢ shrinkCoyonedaEquiv (α ≫ β) = (ConcreteCategory.hom (β.app (unop X))) (shrinkCoyonedaEquiv α)

Tactic:
simp [shrinkCoyonedaEquiv]

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

Goal state before:
pp: case refine_2
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ MonCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget MonCat).sections
s : Cone F
⊢ ∀ (x y : ↑s.1),
    EquivLike.coe (equivShrink ↑(F ⋙ forget MonCat).sections)
        ⟨fun j ↦ (ConcreteCategory.hom (((forget MonCat).mapCone s).π.app j)) (x * y), ⋯⟩ =
      EquivLike.coe (equivShrink ↑(F ⋙ forget MonCat).sections)
          ⟨fun j ↦ (ConcreteCategory.hom (((forget MonCat).mapCone s).π.app j)) x, ⋯⟩ *
        EquivLike.coe (equivShrink ↑(F ⋙ forget MonCat).sections)
          ⟨fun j ↦ (ConcreteCategory.hom (((forget MonCat).mapCone s).π.app j)) y, ⋯⟩

Tactic:
· intro x y
    simp [← equivShrink_mul]
    rfl

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

Goal state before:
pp: case refine_2.refine_1
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ MonCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget MonCat).sections
c : Cone (F ⋙ forget MonCat)
t : IsLimit c
this : Small.{u, max u v} ↑(F ⋙ forget MonCat).sections
s✝ : Cone F
⊢ s✝.pt ⟶
    {
          liftedCone :=
            { pt := of (Types.Small.limitCone (F ⋙ forget MonCat)).pt,
              π := { app := fun j ↦ ofHom (limitπMonoidHom F j), naturality := ⋯ } },
          validLift :=
            Cone.ext ((Types.isLimitEquivSections t).trans (equivShrink ↑(F ⋙ forget MonCat).sections)).symm.toIso
              ⋯ }.liftedCone.pt

Tactic:
refine ofHom
      { toFun := (Types.Small.limitConeIsLimit.{v, u} _).lift ((forget MonCat).mapCone _),
        map_one' := by simp; rfl, map_mul' := ?_ }

Goal state after:
case refine_2.refine_1
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ MonCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget MonCat).sections
c : Cone (F ⋙ forget MonCat)
t : IsLimit c
this : Small.{u, max u v} ↑(F ⋙ forget MonCat).sections
s✝ : Cone F
⊢ ∀ (x y : ↑s✝.1),
    (ConcreteCategory.hom ((Types.Small.limitConeIsLimit (F ⋙ forget MonCat)).lift ((forget MonCat).mapCone s✝)))
        (x * y) =
      (ConcreteCategory.hom ((Types.Small.limitConeIsLimit (F ⋙ forget MonCat)).lift ((forget MonCat).mapCone s✝))) x *
        (ConcreteCategory.hom ((Types.Small.limitConeIsLimit (F ⋙ forget MonCat)).lift ((forget MonCat).mapCone s✝))) y
Module: Mathlib.CategoryTheory.Monoidal.Category

Goal state before:
pp: J : Type u_1
inst✝² : Category.{v_1, u_1} J
C : Type u_2
inst✝¹ : Category.{v_2, u_2} C
inst✝ : MonoidalCategory C
F G F' G' : J ⥤ C
α : F ⟶ F'
β : G ⟶ G'
X' Y' : J
f : X' ⟶ Y'
X : J
⊢ F.obj X ◁ G.map f ≫ (α.app X ⊗ₘ β.app Y') = (α.app X ⊗ₘ β.app X') ≫ F'.obj X ◁ G'.map f

Tactic:
by
  simpa using tensor_naturality α β (𝟙 X) 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
X₁ X₂ : D
⊢ F.map (𝟙 X₁ ⊗ₘ 𝟙 X₂) = F.map (𝟙 (X₁ ⊗ X₂))

Tactic:
by cases fData; cat_disch

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
X₁✝ Y₁✝ Z₁✝ X₂✝ Y₂✝ Z₂✝ : D
f₁ : X₁✝ ⟶ Y₁✝
f₂ : X₂✝ ⟶ Y₂✝
g₁ : Y₁✝ ⟶ Z₁✝
g₂ : Y₂✝ ⟶ Z₂✝
⊢ F.map ((f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂)) = F.map (f₁ ≫ g₁ ⊗ₘ f₂ ≫ g₂)

Tactic:
by cases fData; cat_disch

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
X Y : D
⊢ F.map ((α_ X (𝟙_ D) Y).hom ≫ X ◁ (λ_ Y).hom) = F.map ((ρ_ X).hom ▷ Y)

Tactic:
by cases fData; cat_disch

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

Goal state before:
pp: case refine_2
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ SemiRingCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget SemiRingCat).sections
s : Cone F
⊢ ∀ (x y : ↑s.1),
    EquivLike.coe (equivShrink ↑(F ⋙ forget SemiRingCat).sections)
        ⟨fun j ↦ (ConcreteCategory.hom (((forget SemiRingCat).mapCone s).π.app j)) (x * y), ⋯⟩ =
      EquivLike.coe (equivShrink ↑(F ⋙ forget SemiRingCat).sections)
          ⟨fun j ↦ (ConcreteCategory.hom (((forget SemiRingCat).mapCone s).π.app j)) x, ⋯⟩ *
        EquivLike.coe (equivShrink ↑(F ⋙ forget SemiRingCat).sections)
          ⟨fun j ↦ (ConcreteCategory.hom (((forget SemiRingCat).mapCone s).π.app j)) y, ⋯⟩

pp: case refine_3
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ SemiRingCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget SemiRingCat).sections
s : Cone F
⊢ EquivLike.coe (equivShrink ↑(F ⋙ forget SemiRingCat).sections)
      ⟨fun j ↦ (ConcreteCategory.hom (((forget SemiRingCat).mapCone s).π.app j)) 0, ⋯⟩ =
    0

pp: case refine_4
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ SemiRingCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget SemiRingCat).sections
s : Cone F
⊢ ∀ (x y : ↑s.1),
    EquivLike.coe (equivShrink ↑(F ⋙ forget SemiRingCat).sections)
        ⟨fun j ↦ (ConcreteCategory.hom (((forget SemiRingCat).mapCone s).π.app j)) (x + y), ⋯⟩ =
      EquivLike.coe (equivShrink ↑(F ⋙ forget SemiRingCat).sections)
          ⟨fun j ↦ (ConcreteCategory.hom (((forget SemiRingCat).mapCone s).π.app j)) x, ⋯⟩ +
        EquivLike.coe (equivShrink ↑(F ⋙ forget SemiRingCat).sections)
          ⟨fun j ↦ (ConcreteCategory.hom (((forget SemiRingCat).mapCone s).π.app j)) y, ⋯⟩

Tactic:
· intro x y
    simp [← equivShrink_mul]
    rfl

Goal state after:
case refine_3
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ SemiRingCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget SemiRingCat).sections
s : Cone F
⊢ EquivLike.coe (equivShrink ↑(F ⋙ forget SemiRingCat).sections)
      ⟨fun j ↦ (ConcreteCategory.hom (((forget SemiRingCat).mapCone s).π.app j)) 0, ⋯⟩ =
    0

case refine_4
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ SemiRingCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget SemiRingCat).sections
s : Cone F
⊢ ∀ (x y : ↑s.1),
    EquivLike.coe (equivShrink ↑(F ⋙ forget SemiRingCat).sections)
        ⟨fun j ↦ (ConcreteCategory.hom (((forget SemiRingCat).mapCone s).π.app j)) (x + y), ⋯⟩ =
      EquivLike.coe (equivShrink ↑(F ⋙ forget SemiRingCat).sections)
          ⟨fun j ↦ (ConcreteCategory.hom (((forget SemiRingCat).mapCone s).π.app j)) x, ⋯⟩ +
        EquivLike.coe (equivShrink ↑(F ⋙ forget SemiRingCat).sections)
          ⟨fun j ↦ (ConcreteCategory.hom (((forget SemiRingCat).mapCone s).π.app j)) y, ⋯⟩
Module: Mathlib.CategoryTheory.Linear.LinearFunctor

Goal state before:
pp: R : Type u_1
inst✝⁷ : Semiring R
C : Type u_2
D : Type u_3
inst✝⁶ : Category.{v_1, u_2} C
inst✝⁵ : Category.{v_2, u_3} D
inst✝⁴ : Preadditive C
inst✝³ : Preadditive D
inst✝² : CategoryTheory.Linear R C
inst✝¹ : CategoryTheory.Linear R D
F G : C ⥤ D
e : F ≅ G
inst✝ : Linear R F
⊢ Linear R G

Tactic:
exact
    { map_smul := fun f r => by
        simp only [← NatIso.naturality_1 e (r • f), F.map_smul, Linear.smul_comp,
          NatTrans.naturality, Linear.comp_smul, Iso.inv_hom_id_app_assoc] }

Goal state after: