mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Types.Limits

Goal state before:
pp: J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : Small.{u, max u v} ↑F.sections
x y : (limitCone F).pt
w : (equivShrink ↑F.sections).symm x = (equivShrink ↑F.sections).symm y
⊢ x = y

Tactic:
by

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

Goal state before:
pp: R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i✝ : Fin n.succ
x✝¹ : i✝ ∈ univ
i : Fin n
this : (-1) ^ ↑i = ↑↑(sign i.cycleRange)
σ : Perm (Fin n)
x✝ : σ ∈ univ
⊢ (-1 * ↑(sign σ)) • (A i.succ 0 * ∏ i', A (i.succ.succAbove (i.cycleRange (σ i'))) i'.succ) =
    -1 * (A i.succ 0 * ↑(sign σ) • ∏ i', A (i.succ.succAbove (i.cycleRange (σ i'))) i'.succ)

Tactic:
by

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

Goal state before:
pp: J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : Small.{u, max u v} ↑F.sections
x✝¹ : Cone F
x✝ : x✝¹.pt ⟶ (limitCone F).pt
w : ∀ (j : J), x✝ ≫ (limitCone F).π.app j = x✝¹.π.app j
⊢ x✝ = ↾fun v ↦ (equivShrink ↑F.sections) ⟨fun j ↦ (hom (x✝¹.π.app j)) v, ⋯⟩

Tactic:
by

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

Goal state before:
pp: case insert
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 : (i : ι) → M₁ i
k : ι
s : Finset ι
hk : ∀ x ∈ s, k < x
ih : f a - f (s.piecewise b a) = ∑ i ∈ s, f fun j ↦ if j ∈ s → j < i then a j else if i = j then a j - b j else b j
⊢ f a - f (update (s.piecewise b a) k (b k)) =
    ∑ i ∈ insert k s, f fun j ↦ if j ∈ insert k s → j < i then a j else if i = j then a j - b j else b j

Tactic:
map_update,

Goal state after:
case insert
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 : (i : ι) → M₁ i
k : ι
s : Finset ι
hk : ∀ x ∈ s, k < x
ih : f a - f (s.piecewise b a) = ∑ i ∈ s, f fun j ↦ if j ∈ s → j < i then a j else if i = j then a j - b j else b j
⊢ f a - (f (s.piecewise b a) - f (update (s.piecewise b a) k (s.piecewise b a k - b k))) =
    ∑ i ∈ insert k s, f fun j ↦ if j ∈ insert k s → j < i then a j else if i = j then a j - b j else b j
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
⊢ A.det = ∑ i, (-1) ^ ↑i * A i 0 * (A.submatrix i.succAbove Fin.succ).det

Tactic:
by

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

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type (max v u)
x✝¹ : Cone F
x✝ : x✝¹.pt ⟶ (limitCone F).pt
w : ∀ (j : J), x✝ ≫ (limitCone F).π.app j = x✝¹.π.app j
⊢ x✝ = ↾fun v ↦ ⟨fun j ↦ (hom (x✝¹.π.app j)) v, ⋯⟩

Tactic:
by

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

Goal state before:
pp: J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : HasLimit F
X✝ Y✝ : J ⥤ Type (max u v)
f : X✝ ⟶ Y✝
⊢ lim.map f ≫ (limitEquivSections Y✝).toIso.hom = (limitEquivSections X✝).toIso.hom ≫ (Functor.sectionsFunctor J).map f

Tactic:
by

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

Goal state before:
pp: J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : HasLimit F
x : (j : J) → F.obj j
h : ∀ (j j' : J) (f : j ⟶ j'), (hom (F.map f)) (x j) = x j'
j : J
⊢ (hom (limit.π F j)) (mk F x h) = x j

Tactic:
by

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

Goal state before:
pp: R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
⊢ A.det = ∑ j, (-1) ^ ↑j * A 0 j * (A.submatrix Fin.succ j.succAbove).det

Tactic:
by

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

Goal state before:
pp: J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : HasLimit F
x y : limit F
w : ∀ (j : J), (hom (limit.π F j)) x = (hom (limit.π F j)) y
⊢ x = y

Tactic:
by

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

Goal state before:
pp: R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i : Fin n.succ
⊢ A.det = ↑↑((-1) ^ ↑i * (-1) ^ ↑i) * A.det

Tactic:
by

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

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCat
inst✝ : IsFiltered J
x y z : ↑(R F)
⊢ x * (y + z) = x * y + x * z

Tactic:
by

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

Goal state before:
pp: R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i : Fin n.succ
⊢ ↑↑((-1) ^ ↑i * (-1) ^ ↑i) * A.det = (-1) ^ ↑i * ↑↑(sign i.cycleRange⁻¹) * A.det

Tactic:
by

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

Goal state before:
pp: α β : Type u
f : α ⟶ β
F' : MonoFactorisation f
⊢ lift F' ≫ F'.m = ι f

Tactic:
by

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

Goal state before:
pp: α β : Type u
f : α ⟶ β
⊢ ∀ {X Y : Type u} (f : X ⟶ Y), HasImage f

Tactic:
by

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

Goal state before:
pp: α β : Type u
f✝ : α ⟶ β
f g : Arrow (Type u)
st : f ⟶ g
x : (monoFactorisation f.hom).I
⊢ (ConcreteCategory.hom g.hom) ((ConcreteCategory.hom (Arrow.Hom.left st)) (Classical.choose ⋯)) =
    (ConcreteCategory.hom (Arrow.Hom.right st)) ↑x

Tactic:
by

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

Goal state before:
pp: R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i : Fin n.succ
⊢ A.det = (-1) ^ ↑i * ↑↑(sign i.cycleRange⁻¹) * A.det

Tactic:
by

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

Goal state before:
pp: F : ℕᵒᵖ ⥤ Type u
hF : ∀ (n : ℕ), Function.Surjective ⇑(ConcreteCategory.hom (F.map (homOfLE ⋯).op))
⊢ Function.Surjective ⇑(ConcreteCategory.hom ((limitCone F).π.app (Opposite.op 0)))

Tactic:
by

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

Goal state before:
pp: R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i : Fin n.succ
⊢ A.det = ∑ j, (-1) ^ (↑i + ↑j) * A i j * (A.submatrix i.succAbove j.succAbove).det

Tactic:
by

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

Goal state before:
pp: F : ℕᵒᵖ ⥤ Type u
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Function.Surjective ⇑(ConcreteCategory.hom (F.map (homOfLE ⋯).op))
i : c.pt ≅ (limitCone F).pt := hc.conePointUniqueUpToIso (limitConeIsLimit F)
⊢ c.π.app (Opposite.op 0) = i.hom ≫ (limitCone F).π.app (Opposite.op 0)

Tactic:
by

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

Goal state before:
pp: R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
j : Fin n.succ
⊢ A.det = ∑ i, (-1) ^ (↑i + ↑j) * A i j * (A.submatrix i.succAbove j.succAbove).det

Tactic:
by

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

Goal state before:
pp: R : Type v
inst✝ : CommRing R
A : Matrix (Fin 2) (Fin 2) R
⊢ A.det = A 0 0 * A 1 1 - A 0 1 * A 1 0

Tactic:
by

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

Goal state before:
pp: R : Type v
inst✝ : CommRing R
A : Matrix (Fin 3) (Fin 3) R
⊢ A.det =
    A 0 0 * A 1 1 * A 2 2 - A 0 0 * A 1 2 * A 2 1 - A 0 1 * A 1 0 * A 2 2 + A 0 1 * A 1 2 * A 2 0 +
        A 0 2 * A 1 0 * A 2 1 -
      A 0 2 * A 1 1 * A 2 0

Tactic:
by

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

Goal state before:
pp: F : ℕᵒᵖ ⥤ Type u
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Function.Surjective ⇑(ConcreteCategory.hom (F.map (homOfLE ⋯).op))
⊢ Function.Surjective ⇑(ConcreteCategory.hom (c.π.app (Opposite.op 0)))

Tactic:
by

Goal state after:
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✝ : PreservesLimit F G
c₁ c₂ : Cone F
t : IsLimit c₁
⊢ ∀ (j : J), G.map (t.lift c₂) ≫ (G.mapCone c₁).π.app j = (G.mapCone c₂).π.app j

Tactic:
by

Goal state after:
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✝¹ : PreservesLimit F G
inst✝ : HasLimit F
t : Cone F
⊢ G.map (limit.lift F t) ≫ (preservesLimitIso G F).hom = limit.lift (F ⋙ G) (G.mapCone t)

Tactic:
by

Goal state after:
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✝⁴ : PreservesLimit F G
inst✝³ : HasLimit F
inst✝² : PreservesLimitsOfShape J G
inst✝¹ : HasLimitsOfShape J D
inst✝ : HasLimitsOfShape J C
⊢ ∀ {X Y : J ⥤ C} (f : X ⟶ Y),
    (lim ⋙ G).map f ≫ (preservesLimitIso G Y).hom =
      (preservesLimitIso G X).hom ≫ ((Functor.whiskeringRight J C D).obj G ⋙ lim).map f

Tactic:
by

Goal state after:
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:
by

Goal state after:
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✝ : PreservesColimit F G
c₁ c₂ : Cocone F
t : IsColimit c₁
⊢ ∀ (j : J), (G.mapCocone c₁).ι.app j ≫ G.map (t.desc c₂) = (G.mapCocone c₂).ι.app j

Tactic:
by

Goal state after:
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✝¹ : PreservesColimit F G
inst✝ : HasColimit F
t : Cocone F
⊢ (preservesColimitIso G F).inv ≫ G.map (colimit.desc F t) = colimit.desc (F ⋙ G) (G.mapCocone t)

Tactic:
by

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

Tactic:
by

Goal state after:
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✝⁴ : PreservesColimit F G
inst✝³ : HasColimit F
inst✝² : PreservesColimitsOfShape J G
inst✝¹ : HasColimitsOfShape J D
inst✝ : HasColimitsOfShape J C
⊢ ∀ {X Y : J ⥤ C} (f : X ⟶ Y),
    (colim ⋙ G).map f ≫ (preservesColimitIso G Y).hom =
      (preservesColimitIso G X).hom ≫ ((Functor.whiskeringRight J C D).obj G ⋙ colim).map f

Tactic:
by

Goal state after:
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✝² : HasColimit F
inst✝¹ : HasColimit (F ⋙ G)
inst✝ : IsIso (colimit.post F G)
⊢ IsColimit (G.mapCocone (colimit.cocone F))

Tactic:
by

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

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCat
inst✝ : IsFiltered J
x y z : ↑(R F)
⊢ (x + y) * z = x * z + y * z

Tactic:
by

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

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCat
inst✝ : IsFiltered J
x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
⊢ F.map f ≫
      ofHom
        (let __src :=
          MonCat.Hom.hom ((MonCat.FilteredColimits.colimitCocone (F ⋙ forget₂ SemiRingCat MonCat)).ι.app x✝);
        let __src_1 :=
          AddCommMonCat.Hom.hom
            ((AddCommMonCat.FilteredColimits.colimitCocone (F ⋙ forget₂ SemiRingCat AddCommMonCat)).ι.app x✝);
        { toMonoidHom := __src, map_zero' := ⋯, map_add' := ⋯ }) =
    ofHom
        (let __src :=
          MonCat.Hom.hom ((MonCat.FilteredColimits.colimitCocone (F ⋙ forget₂ SemiRingCat MonCat)).ι.app x✝¹);
        let __src_1 :=
          AddCommMonCat.Hom.hom
            ((AddCommMonCat.FilteredColimits.colimitCocone (F ⋙ forget₂ SemiRingCat AddCommMonCat)).ι.app x✝¹);
        { toMonoidHom := __src, map_zero' := ⋯, map_add' := ⋯ }) ≫
      ((Functor.const J).obj (colimit F)).map f

Tactic:
by

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

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCat
inst✝ : IsFiltered J
t : Cocone F
x : ↑(R F)
⊢ (descMonoidHom t) x = (descAddMonoidHom t) x

Tactic:
by

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

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCat
inst✝ : IsFiltered J
t : Cocone F
⊢ (descMonoidHom t) 1 = 1

Tactic:
by

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

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCat
inst✝ : IsFiltered J
t : Cocone F
x y : ↑(R F)
⊢ (↑(descAddMonoidHom t)).toFun (x * y) = (↑(descAddMonoidHom t)).toFun x * (↑(descAddMonoidHom t)).toFun y

Tactic:
by

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

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCat
inst✝ : IsFiltered J
t : Cocone F
j : J
⊢ (colimitCocone F).ι.app j ≫
      ofHom
        (let __src := descAddMonoidHom t;
        { toFun := (↑__src).toFun, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }) =
    t.ι.app j

Tactic:
by

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

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCat
inst✝ : IsFiltered J
t : Cocone F
m : (colimitCocone F).pt ⟶ t.pt
hm : ∀ (j : J), (colimitCocone F).ι.app j ≫ m = t.ι.app j
⊢ m =
    ofHom
      (let __src := descAddMonoidHom t;
      { toFun := (↑__src).toFun, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ })

Tactic:
by

Goal state after:
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
F : C ⥤ D ⥤ E
X✝ Y✝ Z✝ : C × D
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ (F.map (f ≫ g).1).app X✝.2 ≫ (F.obj Z✝.1).map (f ≫ g).2 =
    ((F.map f.1).app X✝.2 ≫ (F.obj Y✝.1).map f.2) ≫ (F.map g.1).app Y✝.2 ≫ (F.obj Z✝.1).map g.2

Tactic:
by

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

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ CommSemiRingCat
x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
⊢ F.map f ≫
      ofHom
        (SemiRingCat.Hom.hom
          ((SemiRingCat.FilteredColimits.colimitCocone (F ⋙ forget₂ CommSemiRingCat SemiRingCat)).ι.app x✝)) =
    ofHom
        (SemiRingCat.Hom.hom
          ((SemiRingCat.FilteredColimits.colimitCocone (F ⋙ forget₂ CommSemiRingCat SemiRingCat)).ι.app x✝¹)) ≫
      ((Functor.const J).obj (colimit F)).map f

Tactic:
by

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

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ RingCat
x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
⊢ F.map f ≫
      ofHom
        (SemiRingCat.Hom.hom
          ((SemiRingCat.FilteredColimits.colimitCocone (F ⋙ forget₂ RingCat SemiRingCat)).ι.app x✝)) =
    ofHom
        (SemiRingCat.Hom.hom
          ((SemiRingCat.FilteredColimits.colimitCocone (F ⋙ forget₂ RingCat SemiRingCat)).ι.app x✝¹)) ≫
      ((Functor.const J).obj (colimit F)).map f

Tactic:
by

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

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ CommRingCat
x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
⊢ F.map f ≫
      ofHom (RingCat.Hom.hom ((RingCat.FilteredColimits.colimitCocone (F ⋙ forget₂ CommRingCat RingCat)).ι.app x✝)) =
    ofHom (RingCat.Hom.hom ((RingCat.FilteredColimits.colimitCocone (F ⋙ forget₂ CommRingCat RingCat)).ι.app x✝¹)) ≫
      ((Functor.const J).obj (colimit F)).map f

Tactic:
by

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✝ : LinearOrder ι
a b v : (i : ι) → M₁ i
s : Finset ι
⊢ f (s.piecewise a v) - f (s.piecewise b 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:
by

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

Tactic:
map_add_univ,

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

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

Goal state before:
pp: J : Type v
inst✝² : SmallCategory J
F : J ⥤ CommRingCat
inst✝¹ : IsFilteredOrEmpty J
inst✝ : ∀ (i : J), Nontrivial ↑(F.obj i)
c : Cocone F
hc : IsColimit c
⊢ Nontrivial ↑c.pt

Tactic:
by

Goal state after:
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
F : C × D ⥤ E
X : C
Y : D
⊢ F.map (𝟙 X ×ₘ 𝟙 Y) = 𝟙 (F.obj (X, Y))

Tactic:
by

Goal state after:
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
F : C × D ⥤ E
X : C
X✝ Y✝ Z✝ : D
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ F.map (𝟙 X ×ₘ f ≫ g) = F.map (𝟙 X ×ₘ f) ≫ F.map (𝟙 X ×ₘ g)

Tactic:
by

Goal state after:
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
F : C × D ⥤ E
X✝ Y✝ : C
f : X✝ ⟶ Y✝
Y Y' : D
g : Y ⟶ Y'
⊢ { obj := fun Y ↦ F.obj (X✝, Y), map := fun {X Y} g ↦ F.map (𝟙 X✝ ×ₘ g), map_id := ⋯, map_comp := ⋯ }.map g ≫
      F.map (f ×ₘ 𝟙 Y') =
    F.map (f ×ₘ 𝟙 Y) ≫
      { obj := fun Y ↦ F.obj (Y✝, Y), map := fun {X Y} g ↦ F.map (𝟙 Y✝ ×ₘ g), map_id := ⋯, map_comp := ⋯ }.map g

Tactic:
by

Goal state after:
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
F : C × D ⥤ E
X : C
⊢ { app := fun Y ↦ F.map (𝟙 X ×ₘ 𝟙 Y), naturality := ⋯ } =
    𝟙 { obj := fun Y ↦ F.obj (X, Y), map := fun {X_1 Y} g ↦ F.map (𝟙 X ×ₘ g), map_id := ⋯, map_comp := ⋯ }

Tactic:
by

Goal state after:
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
F : C × D ⥤ E
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ { app := fun Y ↦ F.map (f ≫ g ×ₘ 𝟙 Y), naturality := ⋯ } =
    { app := fun Y ↦ F.map (f ×ₘ 𝟙 Y), naturality := ⋯ } ≫ { app := fun Y ↦ F.map (g ×ₘ 𝟙 Y), naturality := ⋯ }

Tactic:
by

Goal state after:
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 : C
Y Y' : D
g : Y ⟶ Y'
⊢ (X✝.curryObj.obj X).map g ≫ T.app (X, Y') = T.app (X, Y) ≫ (Y✝.curryObj.obj X).map g

Tactic:
by

Goal state after:
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

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

Tactic:
by

Goal state after:
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
F : C × D ⥤ E
⊢ ∀ {X Y : C × D} (f : X ⟶ Y),
    ((curry ⋙ uncurry).obj F).map f ≫ (Iso.refl (((curry ⋙ uncurry).obj F).obj Y)).hom =
      (Iso.refl (((curry ⋙ uncurry).obj F).obj X)).hom ≫ ((𝟭 (C × D ⥤ E)).obj F).map f

Tactic:
by

Goal state after:
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
F : B × C ⥤ D
⊢ ∀ (X : B × C), (uncurry.obj (curry.obj F)).obj X = F.obj X

Tactic:
by

Goal state after: