mathlib-initiative/mathlib-tactics huggingface dataset:
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)
⊢ ∀ [inst : DecidableEq ι] (m : (i : ι) → M₁ i →ₗ[R] M₁' i) (i : ι) (x y : M₁ i →ₗ[R] M₁' i),
    compLinearMapₗ (update m i (x + y)) = compLinearMapₗ (update m i x) + compLinearMapₗ (update m i 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
x : ↑(R F)
⊢ x * 0 = 0

Tactic:
by

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)
k : J
f : x.fst ⟶ k
g : y.fst ⟶ k
⊢ M.mk F x * M.mk F y = M.mk F ⟨k, (ConcreteCategory.hom (F.map f)) x.snd * (ConcreteCategory.hom (F.map g)) y.snd⟩

Tactic:
by

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✝⁸ : 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)
⊢ ∀ [inst : DecidableEq ι] (m : (i : ι) → M₁ i →ₗ[R] M₁' i) (i : ι) (c : R) (x : M₁ i →ₗ[R] M₁' i),
    compLinearMapₗ (update m i (c • x)) = c • compLinearMapₗ (update m i x)

Tactic:
by

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
j : J
x y : ↑(F.obj j)
⊢ M.mk F ⟨j, x⟩ * M.mk F ⟨j, y⟩ = M.mk F ⟨j, x * y⟩

Tactic:
by

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✝⁸ : 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)
⊢ ∀ (x y : MultilinearMap R M₁' M₂),
    (LinearMap.applyₗ (x + y)).compMultilinearMap compLinearMapMultilinear =
      (LinearMap.applyₗ x).compMultilinearMap compLinearMapMultilinear +
        (LinearMap.applyₗ y).compMultilinearMap compLinearMapMultilinear

Tactic:
by

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✝⁸ : 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)
⊢ ∀ (m : R) (x : MultilinearMap R M₁' M₂),
    (LinearMap.applyₗ (m • x)).compMultilinearMap compLinearMapMultilinear =
      (RingHom.id R) m • (LinearMap.applyₗ x).compMultilinearMap compLinearMapMultilinear

Tactic:
by

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 : M F
⊢ 1 * x = x

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✝⁵ : 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 ι
⊢ f (∅.piecewise (fun i ↦ c i • m i) m) = (∏ i ∈ ∅, c i) • f m

Tactic:
by

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 : M F
⊢ x * 1 = x

Tactic:
by

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 z : M F
⊢ x * y * z = x * (y * z)

Tactic:
by

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
j : J
x y : ↑(F.1 j)
⊢ (ConcreteCategory.hom ((Types.TypeMax.colimitCocone (F ⋙ forget MonCat)).ι.app j)) (x * y) =
    (ConcreteCategory.hom ((Types.TypeMax.colimitCocone (F ⋙ forget MonCat)).ι.app j)) x *
      (ConcreteCategory.hom ((Types.TypeMax.colimitCocone (F ⋙ forget MonCat)).ι.app j)) y

Tactic:
by

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
t : Cocone F
⊢ (F ⋙ forget MonCat).descColimitType ((F ⋙ forget MonCat).coconeTypesEquiv.symm ((forget MonCat).mapCocone t)) 1 = 1

Tactic:
by

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

Goal state before:
pp: case e'_3
m : Type u_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
⊢ (∑ σ, ↑↑(sign σ) * ∏ i, A (σ i) i) * ∑ σ, ↑↑(sign σ) * ∏ i, D (σ i) i =
    ∑ x ∈ (↑(sumCongrHom m n).range).toFinset, ↑↑(sign x) * ∏ i, fromBlocks A B 0 D (x i) i

pp: case convert_2
m : Type u_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
⊢ ∀ x ∈ univ, x ∉ (↑(sumCongrHom m n).range).toFinset → ↑↑(sign x) * ∏ i, fromBlocks A B 0 D (x i) i = 0

Tactic:
· simp_rw [sum_mul_sum, ← sum_product', univ_product_univ]
      refine sum_nbij (fun σ ↦ σ.fst.sumCongr σ.snd) ?_ ?_ ?_ ?_
      · intro σ₁₂ _
        simp
      · intro σ₁ _ σ₂ _
        dsimp only
        intro h
        have h2 : ∀ x, Perm.sumCongr σ₁.fst σ₁.snd x = Perm.sumCongr σ₂.fst σ₂.snd x :=
          DFunLike.congr_fun h
        simp only [Sum.map_inr, Sum.map_inl, Perm.sumCongr_apply, Sum.forall, Sum.inl.injEq,
          Sum.inr.injEq] at h2
        ext x
        · exact h2.left x
        · exact h2.right x
      · intro σ hσ
        rw [mem_coe, Set.mem_toFinset] at hσ
        obtain ⟨σ₁₂, hσ₁₂⟩ := hσ
        use σ₁₂
        rw [← hσ₁₂]
        simp
      · simp only [forall_prop_of_true, Prod.forall, mem_univ]
        intro σ₁ σ₂
        rw [Fintype.prod_sum_type]
        simp_rw [Equiv.sumCongr_apply, Sum.map_inr, Sum.map_inl, fromBlocks_apply₁₁,
          fromBlocks_apply₂₂]
        rw [mul_mul_mul_comm]
        congr
        rw [sign_sumCongr, Units.val_mul, Int.cast_mul]

Goal state after:
case convert_2
m : Type u_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
⊢ ∀ x ∈ univ, x ∉ (↑(sumCongrHom m n).range).toFinset → ↑↑(sign x) * ∏ i, fromBlocks A B 0 D (x i) i = 0
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: m : Type u_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
σ : Perm (m ⊕ n)
hσn : σ ∉ (↑(sumCongrHom m n).range).toFinset
⊢ ¬∀ (x : m), ∃ y, Sum.inl y = σ (Sum.inl x)

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✝⁵ : 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
⊢ update (s.piecewise (fun i ↦ c i • m i) m) j (m j) = s.piecewise (fun i ↦ c i • m i) m

Tactic:
by

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

Goal state before:
pp: m : Type u_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
⊢ (fromBlocks A B 0 D).det = A.det * D.det

Tactic:
by

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
t : Cocone F
x y : M F
⊢ (F ⋙ forget MonCat).descColimitType ((F ⋙ forget MonCat).coconeTypesEquiv.symm ((forget MonCat).mapCocone t))
      (x * y) =
    (F ⋙ forget MonCat).descColimitType ((F ⋙ forget MonCat).coconeTypesEquiv.symm ((forget MonCat).mapCocone t)) x *
      (F ⋙ forget MonCat).descColimitType ((F ⋙ forget MonCat).coconeTypesEquiv.symm ((forget MonCat).mapCocone t)) y

Tactic:
by

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

Goal state before:
pp: m : Type u_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
A : Matrix m m R
C : Matrix n m R
D : Matrix n n R
⊢ (fromBlocks A 0 C D).det = A.det * D.det

Tactic:
by

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
t : Cocone F
m : (colimitCocone F).pt ⟶ t.pt
h : ∀ (j : J), (colimitCocone F).ι.app j ≫ m = t.ι.app j
y : ↑(colimitCocone F).pt
⊢ (ConcreteCategory.hom m) y = (ConcreteCategory.hom (colimitDesc F t)) y

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✝⁵ : 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 ι
⊢ f (s.piecewise (fun i ↦ c i • m i) m) = (∏ i ∈ s, c i) • f m

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✝⁵ : 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✝ : Fintype ι
c : ι → R
m : (i : ι) → M₁ i
⊢ (f fun i ↦ c i • m i) = (∏ i, c i) • f m

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
⊢ (-1) ^ ↑i = ↑↑(sign i.cycleRange)

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✝⁶ : 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:
by

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

Goal state before:
pp: R : Type uR
ι : Type uι
M₂ : Type v₂
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₂
inst✝ : Finite ι
f g : MultilinearMap R (fun x ↦ R) M₂
h : (f fun x ↦ 1) = g fun x ↦ 1
⊢ f = g

Tactic:
by

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✝¹⁰ : 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₂
A : Type u_1
inst✝³ : CommSemiring A
inst✝² : Algebra R A
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
m : ι → A
i : ι
x y : A
⊢ ∏ i_1, update m i (x + y) i_1 = ∏ i_1, update m i x i_1 + ∏ i_1, update m i y i_1

Tactic:
by

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✝¹⁰ : 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₂
A : Type u_1
inst✝³ : CommSemiring A
inst✝² : Algebra R A
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
m : ι → A
i : ι
c : R
x : A
⊢ ∏ i_1, update m i (c • x) i_1 = c • ∏ i_1, update m i x i_1

Tactic:
by

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✝⁸ : 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₂
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
m : Fin n → A
i : Fin n
x y : A
⊢ (List.ofFn (update m i (x + y))).prod = (List.ofFn (update m i x)).prod + (List.ofFn (update m i y)).prod

Tactic:
by

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✝⁸ : 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₂
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
m : Fin n → A
i : Fin n
c : R
x : A
⊢ (List.ofFn (update m i (c • x))).prod = c • (List.ofFn (update m i x)).prod

Tactic:
by

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

Goal state before:
pp: R : Type uR
n : ℕ
inst✝² : CommSemiring R
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
⊢ ((MultilinearMap.mkPiAlgebraFin R n A) fun x ↦ a) = a ^ n

Tactic:
by

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

Goal state before:
pp: R : Type uR
ι : Type uι
M₂ : Type v₂
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₂
inst✝ : Fintype ι
f : MultilinearMap R (fun x ↦ R) M₂
⊢ MultilinearMap.mkPiRing R ι (f fun x ↦ 1) = f

Tactic:
by

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

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ CommMonCat
x y : ↑(M F)
⊢ x * y = y * x

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
s : (j : J) → F.obj j
hs : s ∈ F.sections
x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
⊢ (((Functor.const J).obj PUnit.{u + 1}).map f ≫ ↾fun x ↦ s x✝) = (↾fun x ↦ s x✝¹) ≫ F.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
c : Cone F
x✝ : Nonempty (IsLimit c)
s : (j : J) → F.obj j
hs : s ∈ F.sections
t : IsLimit c
cs : Cone F := coneOfSection ⋯
x : c.pt
hx : (fun x ↦ ∀ (j : J), (hom (c.π.app j)) x = s j) x
j : J
⊢ (↾fun x_1 ↦ x) ≫ c.π.app j = cs.π.app j

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
c✝ : Cone F
h : ∀ s ∈ F.sections, ∃! x, ∀ (j : J), (hom (c✝.π.app j)) x = s j
this : ∀ (c : Cone F) (y : c.pt), ∃! x, ∀ (j : J), (hom (c✝.π.app j)) x = ↑(sectionOfCone c y) j
x : (c : Cone F) → c.pt → c✝.pt
hx :
  ∀ (c : Cone F) (y : c.pt),
    (fun x ↦ ∀ (j : J), (hom (c✝.π.app j)) x = ↑(sectionOfCone c y) j) (x c y) ∧
      ∀ (y_1 : c✝.pt), (fun x ↦ ∀ (j : J), (hom (c✝.π.app j)) x = ↑(sectionOfCone c y) j) y_1 → y_1 = x c y
c : Cone F
j : J
⊢ ↾x c ≫ c✝.π.app j = c.π.app j

Tactic:
by

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

Goal state before:
pp: R : Type uR
ι : Type uι
M₂ : Type v₂
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₂
inst✝ : Fintype ι
z₁ z₂ : M₂
⊢ MultilinearMap.mkPiRing R ι z₁ = MultilinearMap.mkPiRing R ι z₂ ↔ z₁ = z₂

Tactic:
by

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

Goal state before:
pp: R : Type uR
ι : Type uι
M₂ : Type v₂
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₂
inst✝ : Fintype ι
⊢ MultilinearMap.mkPiRing R ι 0 = 0

Tactic:
by

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

Goal state before:
pp: R : Type uR
ι : Type uι
M₂ : Type v₂
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₂
inst✝ : Fintype ι
z : M₂
⊢ MultilinearMap.mkPiRing R ι z = 0 ↔ z = 0

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
c✝ : Cone F
h : ∀ s ∈ F.sections, ∃! x, ∀ (j : J), (hom (c✝.π.app j)) x = s j
this : ∀ (c : Cone F) (y : c.pt), ∃! x, ∀ (j : J), (hom (c✝.π.app j)) x = ↑(sectionOfCone c y) j
x : (c : Cone F) → c.pt → c✝.pt
hx :
  ∀ (c : Cone F) (y : c.pt),
    (fun x ↦ ∀ (j : J), (hom (c✝.π.app j)) x = ↑(sectionOfCone c y) j) (x c y) ∧
      ∀ (y_1 : c✝.pt), (fun x ↦ ∀ (j : J), (hom (c✝.π.app j)) x = ↑(sectionOfCone c y) j) y_1 → y_1 = x c y
c : Cone F
f : c.pt ⟶ c✝.pt
hf : ∀ (j : J), f ≫ c✝.π.app j = c.π.app j
⊢ f = ↾x c

Tactic:
by

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✝³ : AddCommGroup M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f✝ g f : MultilinearMap R M₁ M₂
inst✝ : DecidableEq ι
m : (i : ι) → M₁ i
i : ι
x y : M₁ i
⊢ -f (update m i (x + y)) = -f (update m i x) + -f (update m i y)

Tactic:
by

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✝³ : AddCommGroup M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f✝ g f : MultilinearMap R M₁ M₂
inst✝ : DecidableEq ι
m : (i : ι) → M₁ i
i : ι
c : R
x : M₁ i
⊢ -f (update m i (c • x)) = c • -f (update m i x)

Tactic:
by

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✝³ : AddCommGroup M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f✝ g✝ f g : MultilinearMap R M₁ M₂
inst✝ : DecidableEq ι
m : (i : ι) → M₁ i
i : ι
x y : M₁ i
⊢ f (update m i (x + y)) - g (update m i (x + y)) =
    f (update m i x) - g (update m i x) + (f (update m i y) - g (update m i y))

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
c : Cone F
⊢ Nonempty (IsLimit c) ↔ ∀ s ∈ F.sections, ∃! x, ∀ (j : J), (hom (c.π.app j)) x = s j

Tactic:
by

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✝³ : AddCommGroup M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f✝ g✝ f g : MultilinearMap R M₁ M₂
inst✝ : DecidableEq ι
m : (i : ι) → M₁ i
i : ι
c : R
x : M₁ i
⊢ f (update m i (c • x)) - g (update m i (c • x)) = c • (f (update m i x) - g (update m i x))

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 ι
m : (i : ι) → M₁ i
i : ι
x : M₁ i
⊢ f (update m i (-x)) + f (update m i x) = 0

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 ι
m : (i : ι) → M₁ i
i : ι
x y : M₁ i
⊢ f (update m i (x - y)) = f (update m i x) - f (update m i y)

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
c : Cone F
⊢ Nonempty (IsLimit c) ↔ Function.Bijective (sectionOfCone c)

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 ι
x : (i : ι) → M₁ i
i : ι
v : M₁ i
⊢ f (update x i v) = f x - f (update x i (x i - 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
c : Cone F
t : IsLimit c
x : ↑F.sections
j : J
⊢ (hom (c.π.app j)) ((isLimitEquivSections t).symm x) = ↑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
i✝ : Fin n.succ
x✝¹ : i✝ ∈ univ
i : Fin n
this : (-1) ^ ↑i = ↑↑(sign i.cycleRange)
σ : Perm (Fin n)
x✝ : σ ∈ univ
⊢ (-1 * ↑(sign σ)) • ∏ i', A ((decomposeFin.symm (i.succ, σ)) i') i' =
    (-1 * ↑(sign σ)) • (A i.succ 0 * ∏ i', A (i.succ.succAbove (i.cycleRange (σ i'))) i'.succ)

Tactic:
by

Goal state after: