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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : UnivLE.{w, w'}
inst✝¹ : UnivLE.{w₂, w₂'}
inst✝ : ReflectsCofilteredLimitsOfSize.{w', w₂', v₁, v₂, u₁, u₂} F
J : Type w₂
x✝¹ : Category.{w, w₂} J
x✝ : IsCofiltered J
e : Shrink.{w₂', w₂} (ShrinkHoms.{w₂} J) ≌ J :=
  ((ShrinkHoms.equivalence J).trans (Shrink.equivalence (ShrinkHoms.{w₂} J))).symm
this : IsCofiltered (Shrink.{w₂', w₂} (ShrinkHoms.{w₂} J))
⊢ ReflectsLimitsOfShape J F

Tactic:
exact reflectsLimitsOfShape_of_equiv e F

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

Goal state before:
pp: J : Type u
inst✝ : Category.{v, u} J
F : J ⥤ Type w₀
c : F.CoconeTypes
a✝ b✝ : (j : J) × F.obj j
w✝ : a✝.fst ⟶ b✝.fst
h✝ : b✝.snd = (ConcreteCategory.hom (F.map w✝)) a✝.snd
⊢ (match a✝ with
    | ⟨j, x⟩ => c.ι j x) =
    match b✝ with
    | ⟨j, x⟩ => c.ι j x

Tactic:
;

Goal state after:
J : Type u
inst✝ : Category.{v, u} J
F : J ⥤ Type w₀
c : F.CoconeTypes
a✝ b✝ : (j : J) × F.obj j
w✝ : a✝.fst ⟶ b✝.fst
h✝ : b✝.snd = (ConcreteCategory.hom (F.map w✝)) a✝.snd
⊢ (match a✝ with
    | ⟨j, x⟩ => c.ι j x) =
    match b✝ with
    | ⟨j, x⟩ => c.ι 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
⊢ ∀ (a b : (j : J) × F.obj j),
    F.ColimitTypeRel a b →
      (match a with
        | ⟨j, x⟩ => c.ι j x) =
        match b with
        | ⟨j, x⟩ => c.ι j x

Tactic:
by rintro _ _ ⟨_, _⟩; aesop

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 : Cocone F
j✝ j'✝ : J
f : j✝ ⟶ j'✝
x : (fun X ↦ X) (F.obj j✝)
⊢ (⇑(ConcreteCategory.hom (c.ι.app j'✝)) ∘ ⇑(ConcreteCategory.hom (F.map f))) x = (ConcreteCategory.hom (c.ι.app j✝)) x

Tactic:
;

Goal state after:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
c : Cocone F
j✝ j'✝ : J
f : j✝ ⟶ j'✝
x : (fun X ↦ X) (F.obj j✝)
⊢ (⇑(ConcreteCategory.hom (c.ι.app j'✝)) ∘ ⇑(ConcreteCategory.hom (F.map f))) x = (ConcreteCategory.hom (c.ι.app j✝)) x
Module: Mathlib.CategoryTheory.Limits.Types.Colimits

Goal state before:
pp: J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : HasColimit F
j : J
x : F.obj j
⊢ (colimitEquivColimitType F) ((hom (colimit.ι F j)) x) = Quot.mk F.ColimitTypeRel ⟨j, x⟩

Tactic:
apply (colimitEquivColimitType F).symm.injective
  simp

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

Goal state before:
pp: case neg
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
i₀ : ι
hi₀ : 1 < #(A i₀)
j₁ j₂ : α i₀
left✝ : j₁ ∈ A i₀
hj₂ : j₂ ∈ A i₀
right✝ : j₁ ≠ j₂
B : (a : ι) → Finset (α a) := update A i₀ (A i₀ \ {j₂})
C : (a : ι) → Finset (α a) := update A i₀ {j₂}
B_subset_A : ∀ (i : ι), B i ⊆ A i
C_subset_A : ∀ (i : ι), C i ⊆ A i
A_eq_BC : (fun i ↦ ∑ j ∈ A i, g i j) = update (fun i ↦ ∑ j ∈ A i, g i j) i₀ (∑ j ∈ B i₀, g i₀ j + ∑ j ∈ C i₀, g i₀ j)
Beq : update (fun i ↦ ∑ j ∈ A i, g i j) i₀ (∑ j ∈ B i₀, g i₀ j) = fun i ↦ ∑ j ∈ B i, g i j
Ceq : update (fun i ↦ ∑ j ∈ A i, g i j) i₀ (∑ j ∈ C i₀, g i₀ j) = fun i ↦ ∑ j ∈ C i, g i j
Brec : (f fun i ↦ ∑ j ∈ B i, g i j) = ∑ r ∈ piFinset B, f fun i ↦ g i (r i)
Crec : (f fun i ↦ ∑ j ∈ C i, g i j) = ∑ r ∈ piFinset C, f fun i ↦ g i (r i)
D : Disjoint (piFinset B) (piFinset C)
pi_BC : piFinset A = piFinset B ∪ piFinset C
⊢ (f fun i ↦ ∑ j ∈ A i, g i j) = ∑ r ∈ piFinset A, f fun i ↦ g i (r i)

Tactic:
A_eq_BC

Goal state after:
case neg
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
i₀ : ι
hi₀ : 1 < #(A i₀)
j₁ j₂ : α i₀
left✝ : j₁ ∈ A i₀
hj₂ : j₂ ∈ A i₀
right✝ : j₁ ≠ j₂
B : (a : ι) → Finset (α a) := update A i₀ (A i₀ \ {j₂})
C : (a : ι) → Finset (α a) := update A i₀ {j₂}
B_subset_A : ∀ (i : ι), B i ⊆ A i
C_subset_A : ∀ (i : ι), C i ⊆ A i
A_eq_BC : (fun i ↦ ∑ j ∈ A i, g i j) = update (fun i ↦ ∑ j ∈ A i, g i j) i₀ (∑ j ∈ B i₀, g i₀ j + ∑ j ∈ C i₀, g i₀ j)
Beq : update (fun i ↦ ∑ j ∈ A i, g i j) i₀ (∑ j ∈ B i₀, g i₀ j) = fun i ↦ ∑ j ∈ B i, g i j
Ceq : update (fun i ↦ ∑ j ∈ A i, g i j) i₀ (∑ j ∈ C i₀, g i₀ j) = fun i ↦ ∑ j ∈ C i, g i j
Brec : (f fun i ↦ ∑ j ∈ B i, g i j) = ∑ r ∈ piFinset B, f fun i ↦ g i (r i)
Crec : (f fun i ↦ ∑ j ∈ C i, g i j) = ∑ r ∈ piFinset C, f fun i ↦ g i (r i)
D : Disjoint (piFinset B) (piFinset C)
pi_BC : piFinset A = piFinset B ∪ piFinset C
⊢ f (update (fun i ↦ ∑ j ∈ A i, g i j) i₀ (∑ j ∈ B i₀, g i₀ j + ∑ j ∈ C i₀, g i₀ j)) =
    ∑ r ∈ piFinset A, f fun i ↦ g i (r i)
Module: Mathlib.CategoryTheory.Limits.Types.Filtered

Goal state before:
pp: J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : IsFilteredOrEmpty J
t : Cocone F
hsurj : ∀ (x : t.pt), ∃ i xi, x = (hom (t.ι.app i)) xi
hinj :
  ∀ (i : J) (x y : (fun X ↦ X) (F.obj i)),
    (hom (t.ι.app i)) x = (hom (t.ι.app i)) y → ∃ k f, (hom (F.map f)) x = (hom (F.map f)) y
i j : J
xi : (fun X ↦ X) (F.obj i)
xj : (fun X ↦ X) (F.obj j)
h : (hom (t.ι.app i)) xi = (hom (t.ι.app j)) xj
k : J
g : IsFiltered.max i j ⟶ k
hg :
  (hom (F.map g)) ((hom (F.map (IsFiltered.leftToMax i j))) xi) =
    (hom (F.map g)) ((hom (F.map (IsFiltered.rightToMax i j))) xj)
⊢ (hom (F.map (IsFiltered.leftToMax i j ≫ g))) xi = (hom (F.map (IsFiltered.rightToMax i j ≫ g))) xj

Tactic:
by simpa using hg

Goal state after:
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 : ι) → AddCommMonoid (M₁ i)
inst✝¹¹ : (i : ι) → Module R (M₁ i)
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : Module R M₂
inst✝⁸ : Semiring S
inst✝⁷ : Module S M₂
inst✝⁶ : SMulCommClass R S M₂
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : Module S M₃
inst✝³ : Module R M₃
inst✝² : SMulCommClass R S M₃
inst✝¹ : LinearMap.CompatibleSMul M₂ M₃ S R
inst✝ : LinearMap.CompatibleSMul M₃ M₂ S R
g : M₂ ≃ₗ[R] M₃
x✝¹ : MultilinearMap R M₁ M₂
x✝ : (i : ι) → M₁ i
⊢ ((LinearMap.compMultilinearMapₗ S ↑g.symm) ((LinearMap.compMultilinearMapₗ S ↑g).toFun x✝¹)) x✝ = x✝¹ x✝

Tactic:
;

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 : ι) → AddCommMonoid (M₁ i)
inst✝¹¹ : (i : ι) → Module R (M₁ i)
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : Module R M₂
inst✝⁸ : Semiring S
inst✝⁷ : Module S M₂
inst✝⁶ : SMulCommClass R S M₂
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : Module S M₃
inst✝³ : Module R M₃
inst✝² : SMulCommClass R S M₃
inst✝¹ : LinearMap.CompatibleSMul M₂ M₃ S R
inst✝ : LinearMap.CompatibleSMul M₃ M₂ S R
g : M₂ ≃ₗ[R] M₃
x✝¹ : MultilinearMap R M₁ M₂
x✝ : (i : ι) → M₁ i
⊢ ((LinearMap.compMultilinearMapₗ S ↑g.symm) ((LinearMap.compMultilinearMapₗ S ↑g).toFun x✝¹)) x✝ = x✝¹ x✝
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 : ι) → AddCommMonoid (M₁ i)
inst✝¹¹ : (i : ι) → Module R (M₁ i)
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : Module R M₂
inst✝⁸ : Semiring S
inst✝⁷ : Module S M₂
inst✝⁶ : SMulCommClass R S M₂
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : Module S M₃
inst✝³ : Module R M₃
inst✝² : SMulCommClass R S M₃
inst✝¹ : LinearMap.CompatibleSMul M₂ M₃ S R
inst✝ : LinearMap.CompatibleSMul M₃ M₂ S R
g : M₂ ≃ₗ[R] M₃
x✝¹ : MultilinearMap R M₁ M₃
x✝ : (i : ι) → M₁ i
⊢ ((LinearMap.compMultilinearMapₗ S ↑g).toFun ((LinearMap.compMultilinearMapₗ S ↑g.symm) x✝¹)) x✝ = x✝¹ x✝

Tactic:
;

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 : ι) → AddCommMonoid (M₁ i)
inst✝¹¹ : (i : ι) → Module R (M₁ i)
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : Module R M₂
inst✝⁸ : Semiring S
inst✝⁷ : Module S M₂
inst✝⁶ : SMulCommClass R S M₂
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : Module S M₃
inst✝³ : Module R M₃
inst✝² : SMulCommClass R S M₃
inst✝¹ : LinearMap.CompatibleSMul M₂ M₃ S R
inst✝ : LinearMap.CompatibleSMul M₃ M₂ S R
g : M₂ ≃ₗ[R] M₃
x✝¹ : MultilinearMap R M₁ M₃
x✝ : (i : ι) → M₁ i
⊢ ((LinearMap.compMultilinearMapₗ S ↑g).toFun ((LinearMap.compMultilinearMapₗ S ↑g.symm) x✝¹)) x✝ = x✝¹ x✝
Module: Mathlib.Algebra.Category.Grp.FilteredColimits

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ GrpCat
x : ↑(G F)
⊢ ∀ (a : (j : J) × ((F ⋙ forget₂ GrpCat MonCat) ⋙ forget MonCat).obj j),
    (Quot.mk ((F ⋙ forget₂ GrpCat MonCat) ⋙ forget MonCat).ColimitTypeRel a)⁻¹ *
        Quot.mk ((F ⋙ forget₂ GrpCat MonCat) ⋙ forget MonCat).ColimitTypeRel a =
      1

Tactic:
;

Goal state after:
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ GrpCat
x : ↑(G F)
⊢ ∀ (a : (j : J) × ((F ⋙ forget₂ GrpCat MonCat) ⋙ forget MonCat).obj j),
    (Quot.mk ((F ⋙ forget₂ GrpCat MonCat) ⋙ forget MonCat).ColimitTypeRel a)⁻¹ *
        Quot.mk ((F ⋙ forget₂ GrpCat MonCat) ⋙ forget MonCat).ColimitTypeRel a =
      1
Module: Mathlib.Algebra.Category.Grp.FilteredColimits

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ GrpCat
⊢ ∀ (a : (j : J) × ((F ⋙ forget₂ GrpCat MonCat) ⋙ forget MonCat).obj j),
    (Quot.mk ((F ⋙ forget₂ GrpCat MonCat) ⋙ forget MonCat).ColimitTypeRel a)⁻¹ *
        Quot.mk ((F ⋙ forget₂ GrpCat MonCat) ⋙ forget MonCat).ColimitTypeRel a =
      1

Tactic:
;

Goal state after:
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ GrpCat
⊢ ∀ (a : (j : J) × ((F ⋙ forget₂ GrpCat MonCat) ⋙ forget MonCat).obj j),
    (Quot.mk ((F ⋙ forget₂ GrpCat MonCat) ⋙ forget MonCat).ColimitTypeRel a)⁻¹ *
        Quot.mk ((F ⋙ forget₂ GrpCat MonCat) ⋙ forget MonCat).ColimitTypeRel a =
      1
Module: Mathlib.Algebra.Category.MonCat.FilteredColimits

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
x' y : (j : J) × ↑(F.obj j)
j₁ : J
x : ↑(F.obj j₁)
hxx' : Types.FilteredColimit.Rel (F ⋙ forget MonCat) ⟨j₁, x⟩ x'
⊢ colimitMulAux F ⟨j₁, x⟩ y = colimitMulAux F x' y

Tactic:
;

Goal state after:
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
x' y : (j : J) × ↑(F.obj j)
j₁ : J
x : ↑(F.obj j₁)
hxx' : Types.FilteredColimit.Rel (F ⋙ forget MonCat) ⟨j₁, x⟩ x'
⊢ colimitMulAux F ⟨j₁, x⟩ y = colimitMulAux F x' y
Module: Mathlib.Algebra.Category.MonCat.FilteredColimits

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
x' : (j : J) × ↑(F.obj j)
j₁ : J
x : ↑(F.obj j₁)
hxx' : Types.FilteredColimit.Rel (F ⋙ forget MonCat) ⟨j₁, x⟩ x'
j₂ : J
y : ↑(F.obj j₂)
⊢ colimitMulAux F ⟨j₁, x⟩ ⟨j₂, y⟩ = colimitMulAux F x' ⟨j₂, y⟩

Tactic:
;

Goal state after:
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
x' : (j : J) × ↑(F.obj j)
j₁ : J
x : ↑(F.obj j₁)
hxx' : Types.FilteredColimit.Rel (F ⋙ forget MonCat) ⟨j₁, x⟩ x'
j₂ : J
y : ↑(F.obj j₂)
⊢ colimitMulAux F ⟨j₁, x⟩ ⟨j₂, y⟩ = colimitMulAux F x' ⟨j₂, y⟩
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✝¹⁰ : CommSemiring R
inst✝⁹ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁸ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : (i : Fin n.succ) → Module R (M i)
inst✝⁵ : (i : ι) → Module R (M₁ i)
inst✝⁴ : Module R M₂
f✝ f' : MultilinearMap R M₁ M₂
inst✝³ : (i : ι) → AddCommMonoid (M₁' i)
inst✝² : (i : ι) → Module R (M₁' i)
α : Type u_1
f : MultilinearMap R M₁ M₂
s : Set ι
e : α ≃ ↑s
inst✝¹ : DecidablePred fun x ↦ x ∈ s
inst✝ : DecidableEq { a // a ∉ s }
m✝ : (i : { a // a ∉ s }) → M₁ ↑i
i✝ : { a // a ∉ s }
x✝ y✝ : M₁ ↑i✝
⊢ { toFun := fun v ↦ ((f.domDomRestrictₗ fun i ↦ i ∈ s) (update m✝ i✝ (x✝ + y✝))) fun i ↦ v (e.symm i) ↑i,
      map_update_add' := ⋯, map_update_smul' := ⋯ } =
    { toFun := fun v ↦ ((f.domDomRestrictₗ fun i ↦ i ∈ s) (update m✝ i✝ x✝)) fun i ↦ v (e.symm i) ↑i,
        map_update_add' := ⋯, map_update_smul' := ⋯ } +
      { toFun := fun v ↦ ((f.domDomRestrictₗ fun i ↦ i ∈ s) (update m✝ i✝ y✝)) fun i ↦ v (e.symm i) ↑i,
        map_update_add' := ⋯, map_update_smul' := ⋯ }

Tactic:
;

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✝¹⁰ : CommSemiring R
inst✝⁹ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁸ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : (i : Fin n.succ) → Module R (M i)
inst✝⁵ : (i : ι) → Module R (M₁ i)
inst✝⁴ : Module R M₂
f✝ f' : MultilinearMap R M₁ M₂
inst✝³ : (i : ι) → AddCommMonoid (M₁' i)
inst✝² : (i : ι) → Module R (M₁' i)
α : Type u_1
f : MultilinearMap R M₁ M₂
s : Set ι
e : α ≃ ↑s
inst✝¹ : DecidablePred fun x ↦ x ∈ s
inst✝ : DecidableEq { a // a ∉ s }
m✝ : (i : { a // a ∉ s }) → M₁ ↑i
i✝ : { a // a ∉ s }
x✝ y✝ : M₁ ↑i✝
⊢ { toFun := fun v ↦ ((f.domDomRestrictₗ fun i ↦ i ∈ s) (update m✝ i✝ (x✝ + y✝))) fun i ↦ v (e.symm i) ↑i,
      map_update_add' := ⋯, map_update_smul' := ⋯ } =
    { toFun := fun v ↦ ((f.domDomRestrictₗ fun i ↦ i ∈ s) (update m✝ i✝ x✝)) fun i ↦ v (e.symm i) ↑i,
        map_update_add' := ⋯, map_update_smul' := ⋯ } +
      { toFun := fun v ↦ ((f.domDomRestrictₗ fun i ↦ i ∈ s) (update m✝ i✝ y✝)) fun i ↦ v (e.symm i) ↑i,
        map_update_add' := ⋯, map_update_smul' := ⋯ }
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✝¹⁰ : CommSemiring R
inst✝⁹ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁸ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : (i : Fin n.succ) → Module R (M i)
inst✝⁵ : (i : ι) → Module R (M₁ i)
inst✝⁴ : Module R M₂
f✝ f' : MultilinearMap R M₁ M₂
inst✝³ : (i : ι) → AddCommMonoid (M₁' i)
inst✝² : (i : ι) → Module R (M₁' i)
α : Type u_1
f : MultilinearMap R M₁ M₂
s : Set ι
e : α ≃ ↑s
inst✝¹ : DecidablePred fun x ↦ x ∈ s
inst✝ : DecidableEq { a // a ∉ s }
m✝ : (i : { a // a ∉ s }) → M₁ ↑i
i✝ : { a // a ∉ s }
x✝¹ y✝ : M₁ ↑i✝
x✝ : α → (i : ι) → M₁ i
⊢ { toFun := fun v ↦ ((f.domDomRestrictₗ fun i ↦ i ∈ s) (update m✝ i✝ (x✝¹ + y✝))) fun i ↦ v (e.symm i) ↑i,
        map_update_add' := ⋯, map_update_smul' := ⋯ }
      x✝ =
    ({ toFun := fun v ↦ ((f.domDomRestrictₗ fun i ↦ i ∈ s) (update m✝ i✝ x✝¹)) fun i ↦ v (e.symm i) ↑i,
          map_update_add' := ⋯, map_update_smul' := ⋯ } +
        { toFun := fun v ↦ ((f.domDomRestrictₗ fun i ↦ i ∈ s) (update m✝ i✝ y✝)) fun i ↦ v (e.symm i) ↑i,
          map_update_add' := ⋯, map_update_smul' := ⋯ })
      x✝

Tactic:
;

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✝¹⁰ : CommSemiring R
inst✝⁹ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁸ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : (i : Fin n.succ) → Module R (M i)
inst✝⁵ : (i : ι) → Module R (M₁ i)
inst✝⁴ : Module R M₂
f✝ f' : MultilinearMap R M₁ M₂
inst✝³ : (i : ι) → AddCommMonoid (M₁' i)
inst✝² : (i : ι) → Module R (M₁' i)
α : Type u_1
f : MultilinearMap R M₁ M₂
s : Set ι
e : α ≃ ↑s
inst✝¹ : DecidablePred fun x ↦ x ∈ s
inst✝ : DecidableEq { a // a ∉ s }
m✝ : (i : { a // a ∉ s }) → M₁ ↑i
i✝ : { a // a ∉ s }
x✝¹ y✝ : M₁ ↑i✝
x✝ : α → (i : ι) → M₁ i
⊢ { toFun := fun v ↦ ((f.domDomRestrictₗ fun i ↦ i ∈ s) (update m✝ i✝ (x✝¹ + y✝))) fun i ↦ v (e.symm i) ↑i,
        map_update_add' := ⋯, map_update_smul' := ⋯ }
      x✝ =
    ({ toFun := fun v ↦ ((f.domDomRestrictₗ fun i ↦ i ∈ s) (update m✝ i✝ x✝¹)) fun i ↦ v (e.symm i) ↑i,
          map_update_add' := ⋯, map_update_smul' := ⋯ } +
        { toFun := fun v ↦ ((f.domDomRestrictₗ fun i ↦ i ∈ s) (update m✝ i✝ y✝)) fun i ↦ v (e.symm i) ↑i,
          map_update_add' := ⋯, map_update_smul' := ⋯ })
      x✝
Module: Mathlib.Algebra.Category.MonCat.FilteredColimits

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
x x' y : (j : J) × ↑(F.obj j)
hxx' : Types.FilteredColimit.Rel (F ⋙ forget MonCat) x x'
⊢ colimitMulAux F x y = colimitMulAux F x' y

Tactic:
by
  obtain ⟨j₁, x⟩ := x; obtain ⟨j₂, y⟩ := y; obtain ⟨j₃, x'⟩ := x'
  obtain ⟨l, f, g, hfg⟩ := hxx'
  replace hfg : F.map f x = F.map g x' := by simpa
  obtain ⟨s, α, β, γ, h₁, h₂, h₃⟩ :=
    IsFiltered.tulip (IsFiltered.leftToMax j₁ j₂) (IsFiltered.rightToMax j₁ j₂)
      (IsFiltered.rightToMax j₃ j₂) (IsFiltered.leftToMax j₃ j₂) f g
  apply M.mk_eq
  use s, α, γ
  simp_rw [map_mul, ← ConcreteCategory.comp_apply, ← F.map_comp, h₁, h₂, h₃, F.map_comp,
    ConcreteCategory.comp_apply, hfg]

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

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
x y' : (j : J) × ↑(F.obj j)
j₁ : J
y : ↑(F.obj j₁)
hyy' : Types.FilteredColimit.Rel (F ⋙ forget MonCat) ⟨j₁, y⟩ y'
⊢ colimitMulAux F x ⟨j₁, y⟩ = colimitMulAux F x y'

Tactic:
;

Goal state after:
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
x y' : (j : J) × ↑(F.obj j)
j₁ : J
y : ↑(F.obj j₁)
hyy' : Types.FilteredColimit.Rel (F ⋙ forget MonCat) ⟨j₁, y⟩ y'
⊢ colimitMulAux F x ⟨j₁, y⟩ = colimitMulAux F x y'
Module: Mathlib.Algebra.Category.MonCat.FilteredColimits

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
y' : (j : J) × ↑(F.obj j)
j₁ : J
y : ↑(F.obj j₁)
hyy' : Types.FilteredColimit.Rel (F ⋙ forget MonCat) ⟨j₁, y⟩ y'
j₂ : J
x : ↑(F.obj j₂)
⊢ colimitMulAux F ⟨j₂, x⟩ ⟨j₁, y⟩ = colimitMulAux F ⟨j₂, x⟩ y'

Tactic:
;

Goal state after:
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
y' : (j : J) × ↑(F.obj j)
j₁ : J
y : ↑(F.obj j₁)
hyy' : Types.FilteredColimit.Rel (F ⋙ forget MonCat) ⟨j₁, y⟩ y'
j₂ : J
x : ↑(F.obj j₂)
⊢ colimitMulAux F ⟨j₂, x⟩ ⟨j₁, y⟩ = colimitMulAux F ⟨j₂, x⟩ y'
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✝¹⁰ : CommSemiring R
inst✝⁹ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁸ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : (i : Fin n.succ) → Module R (M i)
inst✝⁵ : (i : ι) → Module R (M₁ i)
inst✝⁴ : Module R M₂
f✝ f' : MultilinearMap R M₁ M₂
inst✝³ : (i : ι) → AddCommMonoid (M₁' i)
inst✝² : (i : ι) → Module R (M₁' i)
α : Type u_1
f : MultilinearMap R M₁ M₂
s : Set ι
e : α ≃ ↑s
inst✝¹ : DecidablePred fun x ↦ x ∈ s
inst✝ : DecidableEq { a // a ∉ s }
m✝ : (i : { a // a ∉ s }) → M₁ ↑i
i✝ : { a // a ∉ s }
c✝ : R
x✝ : M₁ ↑i✝
⊢ { toFun := fun v ↦ ((f.domDomRestrictₗ fun i ↦ i ∈ s) (update m✝ i✝ (c✝ • x✝))) fun i ↦ v (e.symm i) ↑i,
      map_update_add' := ⋯, map_update_smul' := ⋯ } =
    c✝ •
      { toFun := fun v ↦ ((f.domDomRestrictₗ fun i ↦ i ∈ s) (update m✝ i✝ x✝)) fun i ↦ v (e.symm i) ↑i,
        map_update_add' := ⋯, map_update_smul' := ⋯ }

Tactic:
;

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✝¹⁰ : CommSemiring R
inst✝⁹ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁸ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : (i : Fin n.succ) → Module R (M i)
inst✝⁵ : (i : ι) → Module R (M₁ i)
inst✝⁴ : Module R M₂
f✝ f' : MultilinearMap R M₁ M₂
inst✝³ : (i : ι) → AddCommMonoid (M₁' i)
inst✝² : (i : ι) → Module R (M₁' i)
α : Type u_1
f : MultilinearMap R M₁ M₂
s : Set ι
e : α ≃ ↑s
inst✝¹ : DecidablePred fun x ↦ x ∈ s
inst✝ : DecidableEq { a // a ∉ s }
m✝ : (i : { a // a ∉ s }) → M₁ ↑i
i✝ : { a // a ∉ s }
c✝ : R
x✝ : M₁ ↑i✝
⊢ { toFun := fun v ↦ ((f.domDomRestrictₗ fun i ↦ i ∈ s) (update m✝ i✝ (c✝ • x✝))) fun i ↦ v (e.symm i) ↑i,
      map_update_add' := ⋯, map_update_smul' := ⋯ } =
    c✝ •
      { toFun := fun v ↦ ((f.domDomRestrictₗ fun i ↦ i ∈ s) (update m✝ i✝ x✝)) fun i ↦ v (e.symm i) ↑i,
        map_update_add' := ⋯, map_update_smul' := ⋯ }
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✝¹⁰ : CommSemiring R
inst✝⁹ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁸ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : (i : Fin n.succ) → Module R (M i)
inst✝⁵ : (i : ι) → Module R (M₁ i)
inst✝⁴ : Module R M₂
f✝ f' : MultilinearMap R M₁ M₂
inst✝³ : (i : ι) → AddCommMonoid (M₁' i)
inst✝² : (i : ι) → Module R (M₁' i)
α : Type u_1
f : MultilinearMap R M₁ M₂
s : Set ι
e : α ≃ ↑s
inst✝¹ : DecidablePred fun x ↦ x ∈ s
inst✝ : DecidableEq { a // a ∉ s }
m✝ : (i : { a // a ∉ s }) → M₁ ↑i
i✝ : { a // a ∉ s }
c✝ : R
x✝¹ : M₁ ↑i✝
x✝ : α → (i : ι) → M₁ i
⊢ { toFun := fun v ↦ ((f.domDomRestrictₗ fun i ↦ i ∈ s) (update m✝ i✝ (c✝ • x✝¹))) fun i ↦ v (e.symm i) ↑i,
        map_update_add' := ⋯, map_update_smul' := ⋯ }
      x✝ =
    (c✝ •
        { toFun := fun v ↦ ((f.domDomRestrictₗ fun i ↦ i ∈ s) (update m✝ i✝ x✝¹)) fun i ↦ v (e.symm i) ↑i,
          map_update_add' := ⋯, map_update_smul' := ⋯ })
      x✝

Tactic:
;

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✝¹⁰ : CommSemiring R
inst✝⁹ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁸ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : (i : Fin n.succ) → Module R (M i)
inst✝⁵ : (i : ι) → Module R (M₁ i)
inst✝⁴ : Module R M₂
f✝ f' : MultilinearMap R M₁ M₂
inst✝³ : (i : ι) → AddCommMonoid (M₁' i)
inst✝² : (i : ι) → Module R (M₁' i)
α : Type u_1
f : MultilinearMap R M₁ M₂
s : Set ι
e : α ≃ ↑s
inst✝¹ : DecidablePred fun x ↦ x ∈ s
inst✝ : DecidableEq { a // a ∉ s }
m✝ : (i : { a // a ∉ s }) → M₁ ↑i
i✝ : { a // a ∉ s }
c✝ : R
x✝¹ : M₁ ↑i✝
x✝ : α → (i : ι) → M₁ i
⊢ { toFun := fun v ↦ ((f.domDomRestrictₗ fun i ↦ i ∈ s) (update m✝ i✝ (c✝ • x✝¹))) fun i ↦ v (e.symm i) ↑i,
        map_update_add' := ⋯, map_update_smul' := ⋯ }
      x✝ =
    (c✝ •
        { toFun := fun v ↦ ((f.domDomRestrictₗ fun i ↦ i ∈ s) (update m✝ i✝ x✝¹)) fun i ↦ v (e.symm i) ↑i,
          map_update_add' := ⋯, map_update_smul' := ⋯ })
      x✝