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

Goal state before:
pp: case neg
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ τ : Perm α
hd : σ.Disjoint τ
a✝ : σ.IsCycle
hσ : ∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}
hτ : ∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}
f : Perm α
hf : f.IsCycle ∧ ∀ a ∈ f.support, f a = σ a
x : α
hx : σ x = x
hfx : ¬f x = x
⊢ σ (f⁻¹ x) = x

Tactic:
← hf.right _ (mem_support.mpr hfx)

Goal state after:
case neg
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ τ : Perm α
hd : σ.Disjoint τ
a✝ : σ.IsCycle
hσ : ∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}
hτ : ∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}
f : Perm α
hf : f.IsCycle ∧ ∀ a ∈ f.support, f a = σ a
x : α
hx : f x = x
hfx : ¬f x = x
⊢ σ (f⁻¹ x) = x
Module: Mathlib.GroupTheory.Perm.Cycle.Type

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

Tactic:
simpa [notMem_support] using! h

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

Goal state before:
pp: case neg
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ τ : Perm α
hd : σ.Disjoint τ
a✝ : σ.IsCycle
hσ : ∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}
hτ : ∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}
f : Perm α
hf : f.IsCycle ∧ ∀ a ∈ f.support, f a = τ a
x : α
hx : τ x = x
hfx : ¬f x = x
⊢ τ (f⁻¹ x) = x

Tactic:
← hf.right _ (mem_support.mpr hfx)

Goal state after:
case neg
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ τ : Perm α
hd : σ.Disjoint τ
a✝ : σ.IsCycle
hσ : ∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}
hτ : ∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}
f : Perm α
hf : f.IsCycle ∧ ∀ a ∈ f.support, f a = τ a
x : α
hx : f x = x
hfx : ¬f x = x
⊢ τ (f⁻¹ x) = x
Module: Mathlib.Algebra.Category.Ring.Colimits

Goal state before:
pp: case a.symm
J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
s : Cocone F
x✝¹ y✝ x y : Prequotient F
x✝ : Relation F x y
ih : descFunLift F s x = descFunLift F s y
⊢ descFunLift F s y = descFunLift F s x

Tactic:
| symm x y _ ih =>

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

Goal state before:
pp: case pos
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁶ : Semiring R
inst✝⁵ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁴ : AddCommMonoid M₂
inst✝³ : (i : ι) → Module R (M₁ i)
inst✝² : Module R M₂
f : MultilinearMap R M₁ M₂
α : ι → Type u_1
g : (i : ι) → α i → M₁ i
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
this : (i : ι) → DecidableEq (α i) := fun i ↦ Classical.decEq (α i)
n : ℕ
IH :
  ∀ m < n,
    ∀ (A : (i : ι) → Finset (α i)),
      ∑ i, #(A i) = m → (f fun i ↦ ∑ j ∈ A i, g i j) = ∑ r ∈ piFinset A, f fun i ↦ g i (r i)
A : (i : ι) → Finset (α i)
h : ∑ i, #(A i) = n
Ai_empty : ∀ (i : ι), (A i).Nonempty
Ai_singleton : ∀ (i : ι), #(A i) ≤ 1
⊢ (f fun i ↦ ∑ j ∈ A i, g i j) = ∑ r ∈ piFinset A, f fun i ↦ g i (r i)

Tactic:
have Ai_card : ∀ i, #(A i) = 1 := by
      intro i
      have pos : #(A i) ≠ 0 := by rw [Finset.card_ne_zero]; exact Ai_empty i
      have : #(A i) ≤ 1 := Ai_singleton i
      exact le_antisymm this (Nat.succ_le_of_lt (_root_.pos_iff_ne_zero.mpr pos))
    have :
      ∀ r : ∀ i, α i, r ∈ piFinset A → (f fun i => g i (r i)) = f fun i => ∑ j ∈ A i, g i j := by
      intro r hr
      congr with i
      have : ∀ j ∈ A i, g i j = g i (r i) := by
        intro j hj
        congr
        apply Finset.card_le_one_iff.1 (Ai_singleton i) hj
        exact mem_piFinset.mp hr i
      simp only [Finset.sum_congr rfl this, Finset.sum_const, Ai_card i, one_nsmul]
    simp only [Finset.sum_congr rfl this, Ai_card, card_piFinset, prod_const_one, one_nsmul,
      Finset.sum_const]

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

Goal state before:
pp: case a.symm
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝¹ y✝ x y : Prequotient F
x✝ : Relation F x y
ih : descFunLift F s x = descFunLift F s y
⊢ descFunLift F s y = descFunLift F s x

Tactic:
| symm x y _ ih =>

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFiltered C
O : Finset C
H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
S : C
f : ∀ {X : C}, X ∈ O → Nonempty (X ⟶ S)
⊢ ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f_1 : X ⟶ Y},
    ⟨X, ⟨Y, ⟨mX, ⟨mY, f_1⟩⟩⟩⟩ ∈ ∅ → f_1 ≫ (fun {X} mX ↦ ⋯.some) mY = (fun {X} mX ↦ ⋯.some) mX

Tactic:
by rintro - - - - - ⟨⟩

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
H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
S : C
f : ∀ {X : C}, X ∈ O → Nonempty (S ⟶ X)
⊢ ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f_1 : X ⟶ Y},
    ⟨X, ⟨Y, ⟨mX, ⟨mY, f_1⟩⟩⟩⟩ ∈ ∅ → (fun {X} mX ↦ ⋯.some) mX ≫ f_1 = (fun {X} mX ↦ ⋯.some) mY

Tactic:
by rintro - - - - - ⟨⟩

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

Goal state before:
pp: n✝ : Type u_1
m : Type u_2
R : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n✝
inst✝ : CommSemiring R
s : ℤˣ
A✝ B✝ : Matrix n✝ n✝ R
i j : n✝
a b c : R
n : ℕ
A B : Matrix (Fin n) (Fin n) R
hAB : A * B = 1
h0 : 1 + (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) = detp 1 A * detp 1 B + detp (-1) A * detp (-1) B
h : B * (A + (detp 1 A • adjp (-1) B + detp (-1) A • adjp 1 B)) = B * (detp 1 A • adjp 1 B + detp (-1) A • adjp (-1) B)
⊢ B * A = 1

Tactic:
simp only [mul_add, Matrix.mul_smul] at h

Goal state after:
n✝ : Type u_1
m : Type u_2
R : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n✝
inst✝ : CommSemiring R
s : ℤˣ
A✝ B✝ : Matrix n✝ n✝ R
i j : n✝
a b c : R
n : ℕ
A B : Matrix (Fin n) (Fin n) R
hAB : A * B = 1
h0 : 1 + (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) = detp 1 A * detp 1 B + detp (-1) A * detp (-1) B
h :
  B * A + (detp 1 A • (B * adjp (-1) B) + detp (-1) A • (B * adjp 1 B)) =
    detp 1 A • (B * adjp 1 B) + detp (-1) A • (B * adjp (-1) B)
⊢ B * A = 1
Module: Mathlib.CategoryTheory.Filtered.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
h : ∀ {J : Type w} [inst : SmallCategory J] [FinCategory J] (F : J ⥤ C), Nonempty (Cone F)
⊢ IsCofiltered C

Tactic:
have : Nonempty C := by
    obtain ⟨c⟩ := h (Functor.empty _)
    exact ⟨c.pt⟩
  have : IsCofilteredOrEmpty C := by
    refine ⟨?_, ?_⟩
    · intro X Y
      obtain ⟨c⟩ := h (ULiftHom.down ⋙ ULift.downFunctor ⋙ pair X Y)
      exact ⟨c.pt, c.π.app ⟨⟨WalkingPair.left⟩⟩, c.π.app ⟨⟨WalkingPair.right⟩⟩, trivial⟩
    · intro X Y f g
      obtain ⟨c⟩ := h (ULiftHom.down ⋙ ULift.downFunctor ⋙ parallelPair f g)
      refine ⟨c.pt, c.π.app ⟨WalkingParallelPair.zero⟩, ?_⟩
      have h₁ := c.π.naturality ⟨WalkingParallelPairHom.left⟩
      have h₂ := c.π.naturality ⟨WalkingParallelPairHom.right⟩
      simp_all
  apply IsCofiltered.mk

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

Goal state before:
pp: R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁶ : CommSemiring R
inst✝⁵ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁴ : AddCommMonoid M₂
inst✝³ : (i : ι) → Module R (M₁ i)
inst✝² : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : (i : ι) → M₁ i
i : ι
c : R
x : M₁ i
⊢ f (update (c • m) i x) = c ^ (Fintype.card ι - 1) • f (update m i x)

Tactic:
have : f ((Finset.univ.erase i).piecewise (c • update m i x) (update m i x)) =
      (∏ _i ∈ Finset.univ.erase i, c) • f (update m i x) :=
    map_piecewise_smul f _ _ _

Goal state after:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁶ : CommSemiring R
inst✝⁵ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁴ : AddCommMonoid M₂
inst✝³ : (i : ι) → Module R (M₁ i)
inst✝² : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : (i : ι) → M₁ i
i : ι
c : R
x : M₁ i
this :
  f ((Finset.univ.erase i).piecewise (c • update m i x) (update m i x)) =
    (∏ _i ∈ Finset.univ.erase i, c) • f (update m i x)
⊢ f (update (c • m) i x) = c ^ (Fintype.card ι - 1) • f (update m i x)
Module: Mathlib.CategoryTheory.Limits.Types.Yoneda

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
X : C
a : limit (F.op ⋙ yoneda.obj X)
x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
⊢ F.map f ≫ (ConcreteCategory.hom (limit.π (F.op ⋙ yoneda.obj X) (op x✝))) a =
    (ConcreteCategory.hom (limit.π (F.op ⋙ yoneda.obj X) (op x✝¹))) a ≫ ((const J).obj X).map f

Tactic:
simpa using (limit.w_apply (F.op ⋙ yoneda.obj X) f.op a)

Goal state after:
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 : Cocone F
t : (k : K) → IsColimit (((evaluation K C).obj k).mapCocone c)
s : Cocone F
X Y : K
f : X ⟶ Y
j : J
⊢ (((evaluation K C).obj X).mapCocone c).ι.app j ≫
      c.pt.map f ≫ (t Y).desc { pt := s.pt.obj Y, ι := whiskerRight s.ι ((evaluation K C).obj Y) } =
    (((evaluation K C).obj X).mapCocone c).ι.app j ≫
      (t X).desc { pt := s.pt.obj X, ι := whiskerRight s.ι ((evaluation K C).obj X) } ≫ s.pt.map f

Tactic:
(t X).fac_assoc _ j

Goal state after:
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 : Cocone F
t : (k : K) → IsColimit (((evaluation K C).obj k).mapCocone c)
s : Cocone F
X Y : K
f : X ⟶ Y
j : J
⊢ (((evaluation K C).obj X).mapCocone c).ι.app j ≫
      c.pt.map f ≫ (t Y).desc { pt := s.pt.obj Y, ι := whiskerRight s.ι ((evaluation K C).obj Y) } =
    { pt := s.pt.obj X, ι := whiskerRight s.ι ((evaluation K C).obj X) }.ι.app j ≫ s.pt.map f
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
H : J ⥤ K ⥤ C
inst✝ : HasLimitsOfShape J C
k : K
W : C
f g : W ⟶ (limit H).obj k
w : ∀ (j : J), f ≫ (limit.π H j).app k = g ≫ (limit.π H j).app k
⊢ f = g

Tactic:
apply (cancel_mono (limitObjIsoLimitCompEvaluation H k).hom).1
  ext j
  simpa using w j

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
V W X Y Z : C
f : V ⟶ W
g : X ⟶ Y
h : Y ⟶ Z
⊢ V ◁ g ≫ (f ⊗ₘ h) = f ⊗ₘ g ≫ h

Tactic:
simp [tensorHom_def']

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 : 𝟙_ C ⟶ Y
g : X ⟶ Z
⊢ (λ_ X).inv ≫ (f ⊗ₘ g) = g ≫ (λ_ Z).inv ≫ f ▷ Z

Tactic:
simp [tensorHom_def']

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

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

Tactic:
simp [tensorHom_def']

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

Goal state before:
pp: case h₂
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
E' : Type u₄
inst✝¹⁰ : Category.{v₄, u₄} E'
inst✝⁹ : MonoidalCategory E'
F₁ F₂ F₃ : C ⥤ D
τ : F₁ ⟶ F₂
inst✝⁸ : F₁.LaxMonoidal
inst✝⁷ : F₂.LaxMonoidal
inst✝⁶ : F₃.LaxMonoidal
F G : C ⥤ D
H K : C ⥤ E
α : F ⟶ G
β : H ⟶ K
inst✝⁵ : F.LaxMonoidal
inst✝⁴ : G.LaxMonoidal
inst✝³ : IsMonoidal α
inst✝² : H.LaxMonoidal
inst✝¹ : K.LaxMonoidal
inst✝ : IsMonoidal β
X Y : C
⊢ (μ (F.prod' H) X Y ≫ (prod' α β).app (X ⊗ Y)).2 = (((prod' α β).app X ⊗ₘ (prod' α β).app Y) ≫ μ (G.prod' K) X Y).2

Tactic:
· simp only [prod_comp_snd, prod'_μ_snd, prod'_app_snd,
        prodMonoidal_tensorHom, IsMonoidal.tensor]

Goal state after:
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 : C ⥤ D
inst✝⁶ : Linear R F
E : Type u_4
inst✝⁵ : Category.{v_3, u_4} E
inst✝⁴ : Preadditive E
inst✝³ : CategoryTheory.Linear R E
G : D ⥤ E
inst✝² : F.Full
inst✝¹ : F.EssSurj
inst✝ : Linear R (F ⋙ G)
X Y : D
f : X ⟶ Y
r : R
⊢ G.map (r • f) = r • G.map f

Tactic:
obtain ⟨X', Y', eX, eY, f', rfl⟩ :
      ∃ (X' Y' : C) (eX : F.obj X' ≅ X) (eY : F.obj Y' ≅ Y)
        (f' : X' ⟶ Y'), f = eX.inv ≫ F.map f' ≫ eY.hom := by
    obtain ⟨f', hf'⟩ :=
      F.map_surjective ((F.objObjPreimageIso X).hom ≫ f ≫ (F.objObjPreimageIso Y).inv)
    exact ⟨_, _, F.objObjPreimageIso X, F.objObjPreimageIso Y, f', by cat_disch⟩

Goal state after:
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 : C ⥤ D
inst✝⁶ : Linear R F
E : Type u_4
inst✝⁵ : Category.{v_3, u_4} E
inst✝⁴ : Preadditive E
inst✝³ : CategoryTheory.Linear R E
G : D ⥤ E
inst✝² : F.Full
inst✝¹ : F.EssSurj
inst✝ : Linear R (F ⋙ G)
X Y : D
r : R
X' Y' : C
eX : F.obj X' ≅ X
eY : F.obj Y' ≅ Y
f' : X' ⟶ Y'
⊢ G.map (r • eX.inv ≫ F.map f' ≫ eY.hom) = r • G.map (eX.inv ≫ F.map f' ≫ eY.hom)
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
D : Type u_2
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : Preadditive D
inst✝³ : MonoidalCategory D
F : D ⥤ C
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : F.Additive
X✝ Y✝ Z✝ : D
f✝ g✝ : Y✝ ⟶ Z✝
⊢ F.map (X✝ ◁ (f✝ + g✝)) = F.map (X✝ ◁ f✝ + X✝ ◁ g✝)

Tactic:
simp only [Functor.Monoidal.map_whiskerLeft, Functor.map_add, Preadditive.comp_add,
        Preadditive.add_comp, MonoidalPreadditive.whiskerLeft_add]

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
P Q R S : C
J : Type u_2
s : Finset J
f : P ⟶ Q
g : J → (R ⟶ S)
⊢ (∑ j ∈ s, g j) ⊗ₘ f = ∑ j ∈ s, g j ⊗ₘ f

Tactic:
simp only [tensorHom_def, sum_whiskerRight, Preadditive.sum_comp]

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
F : C ⥤ D
inst✝ : F.LaxMonoidal
X : C
Y : D
f : Y ⟶ F.obj X
⊢ (ε F ⊗ₘ f) ≫ μ F (𝟙_ C) X = 𝟙_ D ◁ f ≫ (λ_ (F.obj X)).hom ≫ F.map (λ_ X).inv

Tactic:
simp [tensorHom_def']

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
F : C ⥤ D
inst✝ : F.LaxMonoidal
X : C
Y : D
f : Y ⟶ F.obj X
⊢ 𝟙_ D ◁ f ≫ (λ_ (F.obj X)).hom = (ε F ⊗ₘ f) ≫ μ F (𝟙_ C) X ≫ F.map (λ_ X).hom

Tactic:
simp [tensorHom_def']

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
F : C ⥤ D
inst✝ : F.OplaxMonoidal
X : C
Y : D
f : F.obj X ⟶ Y
⊢ δ F X (𝟙_ C) ≫ (f ⊗ₘ η F) = F.map (ρ_ X).hom ≫ (ρ_ (F.obj X)).inv ≫ f ▷ 𝟙_ D

Tactic:
simp [tensorHom_def']

Goal state after:
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
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
comm : h ≫ f = k ≫ g
inst✝ : PreservesLimit (cospan f g) G
l : IsLimit (PullbackCone.mk h k comm)
⊢ G.map h ≫ G.map f = G.map k ≫ G.map g

Tactic:
by rw [← G.map_comp, ← G.map_comp, comm]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
Y : Cᵒᵖ
X : C
f : Opposite.unop Y ⟶ Opposite.unop (Opposite.op X)
⊢ identities Cᵒᵖ (Opposite.op f) ↔ identities C f

Tactic:
exact ⟨fun ⟨_⟩ ↦ ⟨_⟩, fun ⟨_⟩ ↦ ⟨_⟩⟩

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'
e : C ≌ D
inst✝⁵ : e.functor.Monoidal
inst✝⁴ : e.inverse.Monoidal
inst✝³ : e.IsMonoidal
e' : D ≌ E
inst✝² : e'.functor.Monoidal
inst✝¹ : e'.inverse.Monoidal
inst✝ : e'.IsMonoidal
⊢ (e.trans e').IsMonoidal

Tactic:
dsimp [Equivalence.IsMonoidal]
  rw [trans_toAdjunction]
  infer_instance

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

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
a✝ : Π₀ (j : J), ↑(F.obj j)
w✝³ w✝² : J
w✝¹ : w✝³ ⟶ w✝²
w✝ : ↑(F.obj w✝³)
eq : a✝ = DFinsupp.single w✝² ((ConcreteCategory.hom (F.map w✝¹)) w✝) - DFinsupp.single w✝³ w✝
⊢ (ConcreteCategory.hom (F.map w✝¹ ≫ c.ι.app w✝²)) w✝ - (Hom.hom (c.ι.app w✝³)) w✝ = 0

Tactic:
rw [c.ι.naturality]

Goal state after:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
a✝ : Π₀ (j : J), ↑(F.obj j)
w✝³ w✝² : J
w✝¹ : w✝³ ⟶ w✝²
w✝ : ↑(F.obj w✝³)
eq : a✝ = DFinsupp.single w✝² ((ConcreteCategory.hom (F.map w✝¹)) w✝) - DFinsupp.single w✝³ w✝
⊢ (ConcreteCategory.hom (c.ι.app w✝³ ≫ ((Functor.const J).obj c.pt).map w✝¹)) w✝ - (Hom.hom (c.ι.app w✝³)) w✝ = 0
Module: Mathlib.Algebra.Category.ModuleCat.Colimits

Goal state before:
pp: R : Type w
inst✝² : Ring R
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ ModuleCat R
inst✝ : HasColimit (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat)
s : Cocone F
r : R
j : J
⊢ colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) j ≫
      colimit.desc (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) ((forget₂ (ModuleCat R) AddCommGrpCat).mapCocone s) ≫
        s.pt.smul r =
    colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) j ≫
      (colimitCocone F).pt.smul r ≫
        colimit.desc (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) ((forget₂ (ModuleCat R) AddCommGrpCat).mapCocone s)

Tactic:
rw [colimit.ι_desc_assoc]

Goal state after:
R : Type w
inst✝² : Ring R
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ ModuleCat R
inst✝ : HasColimit (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat)
s : Cocone F
r : R
j : J
⊢ ((forget₂ (ModuleCat R) AddCommGrpCat).mapCocone s).ι.app j ≫ s.pt.smul r =
    colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) j ≫
      (colimitCocone F).pt.smul r ≫
        colimit.desc (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) ((forget₂ (ModuleCat R) AddCommGrpCat).mapCocone s)
Module: Mathlib.Algebra.Category.ModuleCat.Colimits

Goal state before:
pp: R✝ : Type w
inst✝⁴ : Ring R✝
J : Type u
inst✝³ : Category.{v, u} J
F : J ⥤ ModuleCat R✝
R : Type w
inst✝² : CommRing R
M ι : Type u
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Cocone (Discrete.functor fun x ↦ of R M)
f : (finsuppCocone R M ι).pt ⟶ s.pt
h : ∀ (j : Discrete ι), (finsuppCocone R M ι).ι.app j ≫ f = s.ι.app j
⊢ f = ↟((Finsupp.lsum R) fun i ↦ Hom.hom (s.ι.app { as := i }))

Tactic:
by
    ext : 1
    exact Finsupp.lhom_ext' fun i ↦ LinearMap.ext fun x ↦ by simpa using! congr($(h ⟨i⟩) (x : M))

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

Goal state before:
pp: J : Type u
inst✝² : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝¹ : DecidableEq J
inst✝ : Small.{w, max w u} (Quot F)
x✝² x✝¹ : J
x✝ : x✝² ⟶ x✝¹
⊢ F.map x✝ ≫ ofHom (Shrink.addEquiv.symm.toAddMonoidHom.comp (Quot.ι F x✝¹)) =
    ofHom (Shrink.addEquiv.symm.toAddMonoidHom.comp (Quot.ι F x✝²)) ≫
      ((Functor.const J).obj (of (Shrink.{w, max u w} (Quot F)))).map x✝

Tactic:
by
        ext
        dsimp
        change Shrink.addEquiv.symm _ = _
        rw [Quot.map_ι]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C
⊢ tensorμ X₁ X₂ Y₁ Y₂ ▷ (Z₁ ⊗ Z₂) ≫ tensorμ (X₁ ⊗ Y₁) (X₂ ⊗ Y₂) Z₁ Z₂ ≫ ((α_ X₁ Y₁ Z₁).hom ⊗ₘ (α_ X₂ Y₂ Z₂).hom) =
    (α_ (X₁ ⊗ X₂) (Y₁ ⊗ Y₂) (Z₁ ⊗ Z₂)).hom ≫ (X₁ ⊗ X₂) ◁ tensorμ Y₁ Y₂ Z₁ Z₂ ≫ tensorμ X₁ X₂ (Y₁ ⊗ Z₁) (Y₂ ⊗ Z₂)

Tactic:
dsimp only [tensor_obj, prodMonoidal_tensorObj, tensorμ]
  simp only [braiding_tensor_left_hom, braiding_tensor_right_hom]
  calc
    _ = 𝟙 _ ⊗≫
      X₁ ◁ ((β_ X₂ Y₁).hom ▷ (Y₂ ⊗ Z₁) ≫ (Y₁ ⊗ X₂) ◁ (β_ Y₂ Z₁).hom) ▷ Z₂ ⊗≫
        X₁ ◁ Y₁ ◁ (β_ X₂ Z₁).hom ▷ Y₂ ▷ Z₂ ⊗≫ 𝟙 _ := by monoidal
    _ = _ := by rw [← whisker_exchange]; monoidal

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : NonAssocSemiring M
inst✝ : NonAssocSemiring N
c : RingCon M
f : N →+* M
hf : Surjective ⇑f
d : RingCon N
hcd : d = c.comap f
x : N
⊢ (c.comapQuotientEquivOfSurj f hf hcd).symm ↑(f x) = ↑x

Tactic:
← c.comapQuotientEquivOfSurj_mk hf hcd x,

Goal state after:
M : Type u_1
N : Type u_2
inst✝¹ : NonAssocSemiring M
inst✝ : NonAssocSemiring N
c : RingCon M
f : N →+* M
hf : Surjective ⇑f
d : RingCon N
hcd : d = c.comap f
x : N
⊢ (c.comapQuotientEquivOfSurj f hf hcd).symm ((c.comapQuotientEquivOfSurj f hf hcd) ↑x) = ↑x
Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
C : TensorAlgebra R M → Prop
algebraMap : ∀ (r : R), C ((Algebra.algebraMap R (TensorAlgebra R M)) r)
ι : ∀ (x : M), C ((TensorAlgebra.ι R) x)
mul : ∀ (a b : TensorAlgebra R M), C a → C b → C (a * b)
add : ∀ (a b : TensorAlgebra R M), C a → C b → C (a + b)
a : TensorAlgebra R M
⊢ C a

Tactic:
let s : Subalgebra R (TensorAlgebra R M) :=
    { carrier := {a | C a}
      mul_mem' := @mul
      add_mem' := @add
      algebraMap_mem' := algebraMap }
  let of : M →ₗ[R] s := (TensorAlgebra.ι R).codRestrict (Subalgebra.toSubmodule s) ι
  have of_apply {x : M} : of x = (TensorAlgebra.ι R) x := by rfl
  -- the mapping through the subalgebra is the identity
  have of_id : AlgHom.id R (TensorAlgebra R M) = s.val.comp (lift R of) := by
    ext
    simp [of_apply]
  -- finding a proof is finding an element of the subalgebra
  rw [← AlgHom.id_apply (R := R) a, of_id]
  exact Subtype.prop (lift R of a)

Goal state after:
Module: Mathlib.Algebra.Category.AlgCat.TensorAlgebra

Goal state before:
pp: R✝ : Type u
inst✝² : CommRing R✝
R : Type v
inst✝¹ : CommRing R
inst✝ : Small.{u, v} R
⊢ (forget₂ (AlgCat R) (ModuleCat R)).IsRightAdjoint

Tactic:
let e : AlgCat.{u} R ≌ AlgCat.{u} (Shrink.{u} R) :=
    restrictScalarsEquivalenceOfRingEquiv (Shrink.ringEquiv R)

Goal state after:
R✝ : Type u
inst✝² : CommRing R✝
R : Type v
inst✝¹ : CommRing R
inst✝ : Small.{u, v} R
e : AlgCat R ≌ AlgCat (Shrink.{u, v} R) := restrictScalarsEquivalenceOfRingEquiv (Shrink.ringEquiv R)
⊢ (forget₂ (AlgCat R) (ModuleCat R)).IsRightAdjoint