mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ (vecMulVec u v).det = 0

Tactic:
have huv' : uv'.det = 0 := by
    refine detRowAlternating.map_eq_zero_of_eq _ ?_ hij
    simp [uv', hij]

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).det = 0
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
c' : F.CoconeTypes
f : c.pt → c'.pt
hf : ∀ (j : J) (x : F.obj j), c'.ι j x = f (c.ι j x)
hc' : c'.IsColimit
h₁ : Function.Bijective (F.descColimitType c)
x : F.ColimitType
⊢ (f ∘ F.descColimitType c) x = F.descColimitType c' x

Tactic:
obtain ⟨j, x, rfl⟩ := F.ιColimitType_jointly_surjective x

Goal state after:
J : Type u
inst✝ : Category.{v, u} J
F : J ⥤ Type w₀
c : F.CoconeTypes
hc : c.IsColimit
c' : F.CoconeTypes
f : c.pt → c'.pt
hf : ∀ (j : J) (x : F.obj j), c'.ι j x = f (c.ι j x)
hc' : c'.IsColimit
h₁ : Function.Bijective (F.descColimitType c)
j : J
x : F.obj j
⊢ (f ∘ F.descColimitType c) (F.ιColimitType j x) = F.descColimitType c' (F.ιColimitType j x)
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.IsColimitCore
G : J ⥤ Type w₀'
e : (j : J) → G.obj j ≃ F.obj j
naturality :
  ∀ {j j' : J} (f : j ⟶ j'), ⇑(e j') ∘ ⇑(ConcreteCategory.hom (G.map f)) = ⇑(ConcreteCategory.hom (F.map f)) ∘ ⇑(e j)
T : Type w₂
f g : (c.precompose (fun {j'} ↦ ⇑(e j')) ⋯).pt → T
h : ∀ (j : J), f ∘ (c.precompose (fun {j'} ↦ ⇑(e j')) ⋯).ι j = g ∘ (c.precompose (fun {j'} ↦ ⇑(e j')) ⋯).ι j
j : J
y : G.obj j
⊢ (f ∘ c.ι j) ((e j) y) = (g ∘ c.ι j) ((e j) y)

Tactic:
exact congr_fun (h j) y

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

Goal state before:
pp: case refine_2._hc
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
hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j
M' : Matrix (Fin n.succ) (Fin n.succ) R := M.updateRow k.succ (N k.succ)
hM' : M' = M.updateRow k.succ (N k.succ)
hM : M = M'.updateRow k.succ (M' k.succ + c k • M k.castSucc)
k_ne_succ : k.castSucc ≠ k.succ
M_k : M k.castSucc = M' k.castSucc
⊢ ∀ (i : Fin n), k.castSucc < i.succ → update c k 0 i = 0

Tactic:
intro i

Goal state after:
case refine_2._hc
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
hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j
M' : Matrix (Fin n.succ) (Fin n.succ) R := M.updateRow k.succ (N k.succ)
hM' : M' = M.updateRow k.succ (N k.succ)
hM : M = M'.updateRow k.succ (M' k.succ + c k • M k.castSucc)
k_ne_succ : k.castSucc ≠ k.succ
M_k : M k.castSucc = M' k.castSucc
i : Fin n
⊢ k.castSucc < i.succ → update c k 0 i = 0
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: case refine_2._hsucc
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
hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j
M' : Matrix (Fin n.succ) (Fin n.succ) R := M.updateRow k.succ (N k.succ)
hM' : M' = M.updateRow k.succ (N k.succ)
hM : M = M'.updateRow k.succ (M' k.succ + c k • M k.castSucc)
k_ne_succ : k.castSucc ≠ k.succ
M_k : M k.castSucc = M' k.castSucc
⊢ ∀ (i : Fin n) (j : Fin n.succ), M' i.succ j = N i.succ j + update c k 0 i * M' i.castSucc j

Tactic:
intro i

Goal state after:
case refine_2._hsucc
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
hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j
M' : Matrix (Fin n.succ) (Fin n.succ) R := M.updateRow k.succ (N k.succ)
hM' : M' = M.updateRow k.succ (N k.succ)
hM : M = M'.updateRow k.succ (M' k.succ + c k • M k.castSucc)
k_ne_succ : k.castSucc ≠ k.succ
M_k : M k.castSucc = M' k.castSucc
i : Fin n
⊢ ∀ (j : Fin n.succ), M' i.succ j = N i.succ j + update c k 0 i * M' i.castSucc j
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst✝¹¹ : Semiring R
inst✝¹⁰ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁹ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : AddCommMonoid M₃
inst✝⁶ : AddCommMonoid M'
inst✝⁵ : (i : Fin n.succ) → Module R (M i)
inst✝⁴ : (i : ι) → Module R (M₁ i)
inst✝³ : Module R M₂
inst✝² : Module R M₃
inst✝¹ : Module R M'
f f' : MultilinearMap R M₁ M₂
ι₁ : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
σ : ι₁ ≃ ι₂
m : MultilinearMap R (fun x ↦ M₂) M₃
inst✝ : DecidableEq ι₂
v : ι₂ → M₂
i : ι₂
a b : M₂
this : DecidableEq ι₁ := ⋯.decidableEq
⊢ (m fun i_1 ↦ update (v ∘ ⇑σ) (σ.symm i) (a + b) i_1) =
    (m fun i_1 ↦ update (v ∘ ⇑σ) (σ.symm i) a i_1) + m fun i_1 ↦ update (v ∘ ⇑σ) (σ.symm i) b i_1

Tactic:
m.map_update_add

Goal state after:
R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst✝¹¹ : Semiring R
inst✝¹⁰ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁹ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : AddCommMonoid M₃
inst✝⁶ : AddCommMonoid M'
inst✝⁵ : (i : Fin n.succ) → Module R (M i)
inst✝⁴ : (i : ι) → Module R (M₁ i)
inst✝³ : Module R M₂
inst✝² : Module R M₃
inst✝¹ : Module R M'
f f' : MultilinearMap R M₁ M₂
ι₁ : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
σ : ι₁ ≃ ι₂
m : MultilinearMap R (fun x ↦ M₂) M₃
inst✝ : DecidableEq ι₂
v : ι₂ → M₂
i : ι₂
a b : M₂
this : DecidableEq ι₁ := ⋯.decidableEq
⊢ m (update (v ∘ ⇑σ) (σ.symm i) a) + m (update (v ∘ ⇑σ) (σ.symm i) b) =
    (m fun i_1 ↦ update (v ∘ ⇑σ) (σ.symm i) a i_1) + m fun i_1 ↦ update (v ∘ ⇑σ) (σ.symm i) b i_1
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
⊢ MonCat.FilteredColimits.M.mk (F ⋙ forget₂ SemiRingCat MonCat)
      ⟨j,
        (ConcreteCategory.hom ((F ⋙ forget₂ SemiRingCat MonCat).map (𝟙 j))) ⟨j, 0⟩.snd *
          (ConcreteCategory.hom ((F ⋙ forget₂ SemiRingCat MonCat).map (𝟙 j))) ⟨j, x⟩.snd⟩ =
    AddMonCat.FilteredColimits.M.mk ((F ⋙ forget₂ SemiRingCat AddCommMonCat) ⋙ forget₂ AddCommMonCat AddMonCat) ⟨j, 0⟩

Tactic:
CategoryTheory.Functor.map_id

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
⊢ MonCat.FilteredColimits.M.mk (F ⋙ forget₂ SemiRingCat MonCat)
      ⟨j,
        (ConcreteCategory.hom (𝟙 ((F ⋙ forget₂ SemiRingCat MonCat).obj ⟨j, 0⟩.fst))) ⟨j, 0⟩.snd *
          (ConcreteCategory.hom (𝟙 ((F ⋙ forget₂ SemiRingCat MonCat).obj ⟨j, 0⟩.fst))) ⟨j, x⟩.snd⟩ =
    AddMonCat.FilteredColimits.M.mk ((F ⋙ forget₂ SemiRingCat AddCommMonCat) ⋙ forget₂ AddCommMonCat AddMonCat) ⟨j, 0⟩
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
⊢ MonCat.FilteredColimits.M.mk (F ⋙ forget₂ SemiRingCat MonCat)
      ⟨j,
        (ConcreteCategory.hom ((F ⋙ forget₂ SemiRingCat MonCat).map (𝟙 j))) ⟨j, x⟩.snd *
          (ConcreteCategory.hom ((F ⋙ forget₂ SemiRingCat MonCat).map (𝟙 j))) ⟨j, 0⟩.snd⟩ =
    AddMonCat.FilteredColimits.M.mk ((F ⋙ forget₂ SemiRingCat AddCommMonCat) ⋙ forget₂ AddCommMonCat AddMonCat) ⟨j, 0⟩

Tactic:
CategoryTheory.Functor.map_id

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
⊢ MonCat.FilteredColimits.M.mk (F ⋙ forget₂ SemiRingCat MonCat)
      ⟨j,
        (ConcreteCategory.hom (𝟙 ((F ⋙ forget₂ SemiRingCat MonCat).obj ⟨j, x⟩.fst))) ⟨j, x⟩.snd *
          (ConcreteCategory.hom (𝟙 ((F ⋙ forget₂ SemiRingCat MonCat).obj ⟨j, x⟩.fst))) ⟨j, 0⟩.snd⟩ =
    AddMonCat.FilteredColimits.M.mk ((F ⋙ forget₂ SemiRingCat AddCommMonCat) ⋙ forget₂ AddCommMonCat AddMonCat) ⟨j, 0⟩
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: case pos
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 ι
c : ι → R
m : (i : ι) → M₁ i
s✝ : Finset ι
j : ι
s : Finset ι
j_notMem_s : j ∉ s
Hrec : f (s.piecewise (fun i ↦ c i • m i) m) = (∏ i ∈ s, c i) • f m
i : ι
h : i = j
⊢ update (s.piecewise (fun i ↦ c i • m i) m) j (m j) i = s.piecewise (fun i ↦ c i • m i) m i

pp: case neg
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 ι
c : ι → R
m : (i : ι) → M₁ i
s✝ : Finset ι
j : ι
s : Finset ι
j_notMem_s : j ∉ s
Hrec : f (s.piecewise (fun i ↦ c i • m i) m) = (∏ i ∈ s, c i) • f m
i : ι
h : ¬i = j
⊢ update (s.piecewise (fun i ↦ c i • m i) m) j (m j) i = s.piecewise (fun i ↦ c i • m i) m i

Tactic:
· rw [h]
      simp [j_notMem_s]

Goal state after:
case neg
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 ι
c : ι → R
m : (i : ι) → M₁ i
s✝ : Finset ι
j : ι
s : Finset ι
j_notMem_s : j ∉ s
Hrec : f (s.piecewise (fun i ↦ c i • m i) m) = (∏ i ∈ s, c i) • f m
i : ι
h : ¬i = j
⊢ update (s.piecewise (fun i ↦ c i • m i) m) j (m j) i = s.piecewise (fun i ↦ c i • m i) m i
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
t : IsLimit c
x : ↑F.sections
j : J
⊢ (hom (c.π.app j)) ((isLimitEquivSections t).symm x) = ↑x j

Tactic:
conv_rhs => rw [← (isLimitEquivSections t).right_inv x]

Goal state after:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
c : Cone F
t : IsLimit c
x : ↑F.sections
j : J
⊢ (hom (c.π.app j)) ((isLimitEquivSections t).symm x) =
    ↑((isLimitEquivSections t).toFun ((isLimitEquivSections t).invFun x)) j
Module: Mathlib.CategoryTheory.Limits.Preserves.Limits

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
inst✝³ : Category.{w', w} J
F : J ⥤ C
inst✝² : HasLimit F
inst✝¹ : HasLimit (F ⋙ G)
inst✝ : IsIso (limit.post F G)
⊢ IsLimit (G.mapCone (limit.cone F))

Tactic:
convert! IsLimit.ofPointIso (limit.isLimit (F ⋙ G))
    assumption

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategoryStruct C
id_tensorHom_id : ∀ (X₁ X₂ : C), 𝟙 X₁ ⊗ₘ 𝟙 X₂ = 𝟙 (X₁ ⊗ X₂)
id_tensorHom : ∀ (X : C) {Y₁ Y₂ : C} (f : Y₁ ⟶ Y₂), 𝟙 X ⊗ₘ f = X ◁ f
tensorHom_id : ∀ {X₁ X₂ : C} (f : X₁ ⟶ X₂) (Y : C), f ⊗ₘ 𝟙 Y = f ▷ Y
tensorHom_comp_tensorHom :
  ∀ {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁) (g₂ : Y₂ ⟶ Z₂),
    (f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂) = f₁ ≫ g₁ ⊗ₘ f₂ ≫ g₂
associator_naturality :
  ∀ {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃),
    ((f₁ ⊗ₘ f₂) ⊗ₘ f₃) ≫ (α_ Y₁ Y₂ Y₃).hom = (α_ X₁ X₂ X₃).hom ≫ (f₁ ⊗ₘ f₂ ⊗ₘ f₃)
leftUnitor_naturality : ∀ {X Y : C} (f : X ⟶ Y), (𝟙 (𝟙_ C) ⊗ₘ f) ≫ (λ_ Y).hom = (λ_ X).hom ≫ f
rightUnitor_naturality : ∀ {X Y : C} (f : X ⟶ Y), (f ⊗ₘ 𝟙 (𝟙_ C)) ≫ (ρ_ Y).hom = (ρ_ X).hom ≫ f
pentagon :
  ∀ (W X Y Z : C),
    ((α_ W X Y).hom ⊗ₘ 𝟙 Z) ≫ (α_ W (X ⊗ Y) Z).hom ≫ (𝟙 W ⊗ₘ (α_ X Y Z).hom) =
      (α_ (W ⊗ X) Y Z).hom ≫ (α_ W X (Y ⊗ Z)).hom
triangle : ∀ (X Y : C), (α_ X (𝟙_ C) Y).hom ≫ (𝟙 X ⊗ₘ (λ_ Y).hom) = (ρ_ X).hom ⊗ₘ 𝟙 Y
X₁✝ Y₁✝ X₂✝ Y₂✝ : C
f✝ : X₁✝ ⟶ Y₁✝
g✝ : X₂✝ ⟶ Y₂✝
⊢ f✝ ⊗ₘ g✝ = f✝ ▷ X₂✝ ≫ Y₁✝ ◁ g✝

Tactic:
simp [← id_tensorHom, ← tensorHom_id, tensorHom_comp_tensorHom]

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

Goal state before:
pp: case intro
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 : C
j : J
val✝ : Fintype J
⊢ (rightDistributor f X).hom ≫ biproduct.π (fun j ↦ f j ⊗ X) j = biproduct.π f j ▷ X

Tactic:
simp [rightDistributor_hom, Preadditive.sum_comp, biproduct.ι_π, comp_dite]

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.toLaxMonoidal = b.toLaxMonoidal
⊢ (εIso F).hom ≫ η F = (εIso F).hom ≫ η F

Tactic:
εIso_hom,

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.toLaxMonoidal = b.toLaxMonoidal
⊢ ε F ≫ η F = ε F ≫ η F
Module: Mathlib.CategoryTheory.Limits.Opposites

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
F : J ⥤ Cᵒᵖ
inst✝ : HasLimit F
j : Jᵒᵖ
⊢ colimit.ι F.leftOp j ≫ (colimitLeftOpIsoUnopLimit F).hom = (limit.π F (unop j)).unop

Tactic:
by
  simp [colimitLeftOpIsoUnopLimit]

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 : C
⊢ (β_ (𝟙_ C) X).hom ≫ (ρ_ X).hom ≫ (λ_ X).inv = 𝟙 (𝟙_ C ⊗ X)

Tactic:
rw [braiding_tensorUnit_left]

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ ((λ_ X).hom ≫ (ρ_ X).inv) ≫ (ρ_ X).hom ≫ (λ_ X).inv = 𝟙 (𝟙_ C ⊗ 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 G : C ⥤ D
inst✝ : F.Monoidal
i : F ≅ G
X Y Z : C
⊢ (i.inv.app X ⊗ₘ i.inv.app Y) ▷ G.obj Z ≫
      LaxMonoidal.μ F X Y ▷ G.obj Z ≫
        i.hom.app (X ⊗ Y) ▷ G.obj Z ≫
          (i.inv.app (X ⊗ Y) ⊗ₘ i.inv.app Z) ≫
            LaxMonoidal.μ F (X ⊗ Y) Z ≫
              OplaxMonoidal.δ F (X ⊗ Y) Z ≫
                OplaxMonoidal.δ F X Y ▷ F.obj Z ≫
                  (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom ≫
                    F.obj X ◁ LaxMonoidal.μ F Y Z ≫ LaxMonoidal.μ F X (Y ⊗ Z) ≫ i.hom.app (X ⊗ Y ⊗ Z) =
    (α_ (G.obj X) (G.obj Y) (G.obj Z)).hom ≫
      G.obj X ◁ (i.inv.app Y ⊗ₘ i.inv.app Z) ≫
        G.obj X ◁ LaxMonoidal.μ F Y Z ≫
          G.obj X ◁ i.hom.app (Y ⊗ Z) ≫
            (i.inv.app X ⊗ₘ i.inv.app (Y ⊗ Z)) ≫ LaxMonoidal.μ F X (Y ⊗ Z) ≫ i.hom.app (X ⊗ Y ⊗ Z)

Tactic:
Functor.OplaxMonoidal.associativity_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 G : C ⥤ D
inst✝ : F.Monoidal
i : F ≅ G
X Y Z : C
⊢ (i.inv.app X ⊗ₘ i.inv.app Y) ▷ G.obj Z ≫
      LaxMonoidal.μ F X Y ▷ G.obj Z ≫
        i.hom.app (X ⊗ Y) ▷ G.obj Z ≫
          (i.inv.app (X ⊗ Y) ⊗ₘ i.inv.app Z) ≫
            LaxMonoidal.μ F (X ⊗ Y) Z ≫
              F.map (α_ X Y Z).hom ≫
                OplaxMonoidal.δ F X (Y ⊗ Z) ≫
                  F.obj X ◁ OplaxMonoidal.δ F Y Z ≫
                    F.obj X ◁ LaxMonoidal.μ F Y Z ≫ LaxMonoidal.μ F X (Y ⊗ Z) ≫ i.hom.app (X ⊗ Y ⊗ Z) =
    (α_ (G.obj X) (G.obj Y) (G.obj Z)).hom ≫
      G.obj X ◁ (i.inv.app Y ⊗ₘ i.inv.app Z) ≫
        G.obj X ◁ LaxMonoidal.μ F Y Z ≫
          G.obj X ◁ i.hom.app (Y ⊗ Z) ≫
            (i.inv.app X ⊗ₘ i.inv.app (Y ⊗ Z)) ≫ LaxMonoidal.μ F X (Y ⊗ Z) ≫ i.hom.app (X ⊗ Y ⊗ Z)
Module: Mathlib.Algebra.Category.Grp.Colimits

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
inst✝ : DecidableEq J
j j' : J
f : j ⟶ j'
x : ↑(F.obj j)
⊢ ((QuotientAddGroup.mk' (Relations F)).comp (DFinsupp.singleAddHom (fun j ↦ ↑(F.obj j)) j'))
        ((ConcreteCategory.hom (F.map f)) x) -
      ((QuotientAddGroup.mk' (Relations F)).comp (DFinsupp.singleAddHom (fun j ↦ ↑(F.obj j)) j)) x =
    0

Tactic:
erw [← (QuotientAddGroup.mk' (Relations F)).map_sub, ← AddMonoidHom.mem_ker]

Goal state after:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
inst✝ : DecidableEq J
j j' : J
f : j ⟶ j'
x : ↑(F.obj j)
⊢ (DFinsupp.singleAddHom (fun j ↦ ↑(F.obj j)) j') ((ConcreteCategory.hom (F.map f)) x) -
      (DFinsupp.singleAddHom (fun j ↦ ↑(F.obj j)) j) x ∈
    (QuotientAddGroup.mk' (Relations F)).ker
Module: Mathlib.CategoryTheory.Adjunction.Mates

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
D : Type u₄
E : Type u₅
F : Type u₆
inst✝⁵ : Category.{v₁, u₁} A
inst✝⁴ : Category.{v₂, u₂} B
inst✝³ : Category.{v₃, u₃} C
inst✝² : Category.{v₄, u₄} D
inst✝¹ : Category.{v₅, u₅} E
inst✝ : Category.{v₆, u₆} F
G₁ : A ⥤ C
G₂ : C ⥤ E
H₁ : B ⥤ D
H₂ : D ⥤ F
L₁ : A ⥤ B
R₁ : B ⥤ A
L₂ : C ⥤ D
R₂ : D ⥤ C
L₃ : E ⥤ F
R₃ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
α : TwoSquare G₁ L₁ L₂ H₁
β : TwoSquare G₂ L₂ L₃ H₂
b : B
⊢ adj₃.unit.app (G₂.obj (G₁.obj (R₁.obj b))) ≫
      R₃.map (β.natTrans.app (G₁.obj (R₁.obj b))) ≫
        R₃.map (H₂.map (α.natTrans.app (R₁.obj b))) ≫ R₃.map (H₂.map (H₁.map (adj₁.counit.app b))) =
    ((adj₃.unit.app (G₂.obj (G₁.obj (R₁.obj b))) ≫
          R₃.map
            (L₃.map (G₂.map (adj₂.unit.app (G₁.obj (R₁.obj b))) ≫ G₂.map (R₂.map (α.natTrans.app (R₁.obj b)))) ≫
              L₃.map (G₂.map (R₂.map (H₁.map (adj₁.counit.app b)))))) ≫
        R₃.map (β.natTrans.app (R₂.obj (H₁.obj b)))) ≫
      R₃.map (H₂.map (adj₂.counit.app (H₁.obj b)))

Tactic:
R₃.map_comp

Goal state after:
A : Type u₁
B : Type u₂
C : Type u₃
D : Type u₄
E : Type u₅
F : Type u₆
inst✝⁵ : Category.{v₁, u₁} A
inst✝⁴ : Category.{v₂, u₂} B
inst✝³ : Category.{v₃, u₃} C
inst✝² : Category.{v₄, u₄} D
inst✝¹ : Category.{v₅, u₅} E
inst✝ : Category.{v₆, u₆} F
G₁ : A ⥤ C
G₂ : C ⥤ E
H₁ : B ⥤ D
H₂ : D ⥤ F
L₁ : A ⥤ B
R₁ : B ⥤ A
L₂ : C ⥤ D
R₂ : D ⥤ C
L₃ : E ⥤ F
R₃ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
α : TwoSquare G₁ L₁ L₂ H₁
β : TwoSquare G₂ L₂ L₃ H₂
b : B
⊢ adj₃.unit.app (G₂.obj (G₁.obj (R₁.obj b))) ≫
      R₃.map (β.natTrans.app (G₁.obj (R₁.obj b))) ≫
        R₃.map (H₂.map (α.natTrans.app (R₁.obj b))) ≫ R₃.map (H₂.map (H₁.map (adj₁.counit.app b))) =
    ((adj₃.unit.app (G₂.obj (G₁.obj (R₁.obj b))) ≫
          R₃.map (L₃.map (G₂.map (adj₂.unit.app (G₁.obj (R₁.obj b))) ≫ G₂.map (R₂.map (α.natTrans.app (R₁.obj b))))) ≫
            R₃.map (L₃.map (G₂.map (R₂.map (H₁.map (adj₁.counit.app b)))))) ≫
        R₃.map (β.natTrans.app (R₂.obj (H₁.obj b)))) ≫
      R₃.map (H₂.map (adj₂.counit.app (H₁.obj b)))
Module: Mathlib.CategoryTheory.Adjunction.Mates

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
D : Type u₄
E : Type u₅
F : Type u₆
inst✝⁵ : Category.{v₁, u₁} A
inst✝⁴ : Category.{v₂, u₂} B
inst✝³ : Category.{v₃, u₃} C
inst✝² : Category.{v₄, u₄} D
inst✝¹ : Category.{v₅, u₅} E
inst✝ : Category.{v₆, u₆} F
G₁ : A ⥤ C
G₂ : C ⥤ E
H₁ : B ⥤ D
H₂ : D ⥤ F
L₁ : A ⥤ B
R₁ : B ⥤ A
L₂ : C ⥤ D
R₂ : D ⥤ C
L₃ : E ⥤ F
R₃ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
α : TwoSquare G₁ L₁ L₂ H₁
β : TwoSquare G₂ L₂ L₃ H₂
b : B
⊢ adj₃.unit.app (G₂.obj (G₁.obj (R₁.obj b))) ≫
      R₃.map (β.natTrans.app (G₁.obj (R₁.obj b))) ≫
        R₃.map (H₂.map (α.natTrans.app (R₁.obj b))) ≫ R₃.map (H₂.map (H₁.map (adj₁.counit.app b))) =
    adj₃.unit.app (G₂.obj (G₁.obj (R₁.obj b))) ≫
      (R₃.map (β.app (G₁.obj (R₁.obj b))) ≫
          R₃.map
            ((L₂ ⋙ H₂).map (adj₂.unit.app (G₁.obj (R₁.obj b)) ≫ R₂.map (α.natTrans.app (R₁.obj b))) ≫
              (L₂ ⋙ H₂).map (R₂.map (H₁.map (adj₁.counit.app b))))) ≫
        R₃.map (H₂.map (adj₂.counit.app (H₁.obj b)))

Tactic:
R₃.map_comp

Goal state after:
A : Type u₁
B : Type u₂
C : Type u₃
D : Type u₄
E : Type u₅
F : Type u₆
inst✝⁵ : Category.{v₁, u₁} A
inst✝⁴ : Category.{v₂, u₂} B
inst✝³ : Category.{v₃, u₃} C
inst✝² : Category.{v₄, u₄} D
inst✝¹ : Category.{v₅, u₅} E
inst✝ : Category.{v₆, u₆} F
G₁ : A ⥤ C
G₂ : C ⥤ E
H₁ : B ⥤ D
H₂ : D ⥤ F
L₁ : A ⥤ B
R₁ : B ⥤ A
L₂ : C ⥤ D
R₂ : D ⥤ C
L₃ : E ⥤ F
R₃ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
α : TwoSquare G₁ L₁ L₂ H₁
β : TwoSquare G₂ L₂ L₃ H₂
b : B
⊢ adj₃.unit.app (G₂.obj (G₁.obj (R₁.obj b))) ≫
      R₃.map (β.natTrans.app (G₁.obj (R₁.obj b))) ≫
        R₃.map (H₂.map (α.natTrans.app (R₁.obj b))) ≫ R₃.map (H₂.map (H₁.map (adj₁.counit.app b))) =
    adj₃.unit.app (G₂.obj (G₁.obj (R₁.obj b))) ≫
      (R₃.map (β.app (G₁.obj (R₁.obj b))) ≫
          R₃.map ((L₂ ⋙ H₂).map (adj₂.unit.app (G₁.obj (R₁.obj b)) ≫ R₂.map (α.natTrans.app (R₁.obj b)))) ≫
            R₃.map ((L₂ ⋙ H₂).map (R₂.map (H₁.map (adj₁.counit.app b))))) ≫
        R₃.map (H₂.map (adj₂.counit.app (H₁.obj b)))
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
g : N →+* M
⊢ c.comap g = ker (c.mk'.comp g)

Tactic:
ker_comp,

Goal state after:
M : Type u_1
N : Type u_2
inst✝¹ : NonAssocSemiring M
inst✝ : NonAssocSemiring N
c : RingCon M
g : N →+* M
⊢ c.comap g = (ker c.mk').comap g
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
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : M →ₗ[R] A
⊢ ringCon R M ≤ RingCon.ker ((FreeAlgebra.lift R) ⇑f).toRingHom

Tactic:
by
        grw [ringCon, RingCon.ringConGen_le]
        intro x y h
        induction h <;>
          simp [Algebra.smul_def, FreeAlgebra.lift_ι_apply,
            map_mul, AlgHom.commutes, map_add, RingCon.ker]

Goal state after: