mathlib-initiative/mathlib-tactics huggingface dataset:
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
x y z : (j : J) × F.obj j
x✝¹ : FilteredColimit.Rel F x y
x✝ : FilteredColimit.Rel F y z
k : J
f : x.fst ⟶ k
g : y.fst ⟶ k
h : (hom (F.map f)) x.snd = (hom (F.map g)) y.snd
k' : J
f' : y.fst ⟶ k'
g' : z.fst ⟶ k'
h' : (hom (F.map f')) y.snd = (hom (F.map g')) z.snd
l : J
fl : k ⟶ l
gl : k' ⟶ l
h✝ : True
m : J
n : l ⟶ m
hn : (g ≫ fl) ≫ n = (f' ≫ gl) ≫ n
⊢ (hom (F.map (gl ≫ n))) ((hom (F.map f')) y.snd) = (hom (F.map (gl ≫ n))) ((hom (F.map g')) z.snd)

Tactic:
by

Goal state after:
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
x y z : (j : J) × F.obj j
x✝¹ : FilteredColimit.Rel F x y
x✝ : FilteredColimit.Rel F y z
k : J
f : x.fst ⟶ k
g : y.fst ⟶ k
h : (hom (F.map f)) x.snd = (hom (F.map g)) y.snd
k' : J
f' : y.fst ⟶ k'
g' : z.fst ⟶ k'
h' : (hom (F.map f')) y.snd = (hom (F.map g')) z.snd
l : J
fl : k ⟶ l
gl : k' ⟶ l
h✝ : True
m : J
n : l ⟶ m
hn : (g ≫ fl) ≫ n = (f' ≫ gl) ≫ n
⊢ (hom (F.map (gl ≫ n))) ((hom (F.map g')) z.snd) = (hom (F.map (g' ≫ gl ≫ n))) z.snd

Tactic:
by

Goal state after:
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
o : Type u_3
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := {σ | ∀ (x : n × o), (σ x).2 = x.2}
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (σ x).2 = x.2
σ : n × o ≃ n × o
hσ : ∀ (x : n × o), (σ x).2 = x.2
x : n × o
⊢ (σ.symm x).2 = x.2

Tactic:
by

Goal state after:
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
⊢ FilteredColimit.Rel F = Relation.EqvGen F.ColimitTypeRel

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✝¹⁰ : (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₃
ι' : Type u_1
σ : ι ≃ ι'
f : MultilinearMap R M₁ M₂
inst✝ : DecidableEq ι'
m : (i : ι') → M₁ (σ.symm i)
i : ι'
c : R
⊢ ∀ (x : M₁ (σ.symm i)),
    (⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ).symm) (update m i (c • x)) =
      c • (⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ).symm) (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✝⁹ : (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₃
ι' : Type u_1
σ : ι ≃ ι'
f₁ f₂ : MultilinearMap R M₁ M₂
⊢ { toFun := ⇑(f₁ + f₂) ∘ ⇑(Equiv.piCongrLeft' M₁ σ).symm, map_update_add' := ⋯, map_update_smul' := ⋯ } =
    { toFun := ⇑f₁ ∘ ⇑(Equiv.piCongrLeft' M₁ σ).symm, map_update_add' := ⋯, map_update_smul' := ⋯ } +
      { toFun := ⇑f₂ ∘ ⇑(Equiv.piCongrLeft' M₁ σ).symm, map_update_add' := ⋯, map_update_smul' := ⋯ }

Tactic:
by

Goal state after:
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
inst✝ : HasColimit F
i j : J
xi : F.obj i
xj : F.obj j
⊢ (hom ((colimitCocone F).ι.app i)) xi = (hom ((colimitCocone F).ι.app j)) xj ↔ FilteredColimit.Rel F ⟨i, xi⟩ ⟨j, xj⟩

Tactic:
by

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

Goal state before:
pp: case fst
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
R : Type v
inst✝² : CommRing R
o : Type u_3
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := ⋯
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (σ x).2 = x.2
σ : n × o ≃ n × o
hσ : ∀ (x : n × o), (σ x).2 = x.2
hσ' : ∀ (x : n × o), (σ.symm x).2 = x.2
k : o
x : n
⊢ ((σ (x, k)).1, k).1 = (σ (x, k)).1

Tactic:
simp only

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₃
ι' : Type u_1
σ : ι ≃ ι'
c : S
f : MultilinearMap R M₁ M₂
⊢ { toFun := ⇑(c • f) ∘ ⇑(Equiv.piCongrLeft' M₁ σ).symm, map_update_add' := ⋯, map_update_smul' := ⋯ } =
    (RingHom.id S) c • { toFun := ⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ).symm, map_update_add' := ⋯, map_update_smul' := ⋯ }

Tactic:
by

Goal state after:
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
o : Type u_3
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := {σ | ∀ (x : n × o), (σ x).2 = x.2}
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (σ x).2 = x.2
σ : n × o ≃ n × o
hσ : ∀ (x : n × o), (σ x).2 = x.2
hσ' : ∀ (x : n × o), (σ.symm x).2 = x.2
⊢ ∀ (k : o) (x : n), ((σ (x, k)).1, k) = σ (x, k)

Tactic:
by

Goal state after:
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
o : Type u_3
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := {σ | ∀ (x : n × o), (σ x).2 = x.2}
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (σ x).2 = x.2
σ : n × o ≃ n × o
hσ : ∀ (x : n × o), (σ x).2 = x.2
hσ' : ∀ (x : n × o), (σ.symm x).2 = x.2
mk_apply_eq : ∀ (k : o) (x : n), ((σ (x, k)).1, k) = σ (x, k)
⊢ ∀ (k : o) (x : n), ((σ.symm (x, k)).1, k) = σ.symm (x, k)

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✝¹⁰ : (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₃
ι' : Type u_1
σ : ι ≃ ι'
f : MultilinearMap R (fun i ↦ M₁ (σ.symm i)) M₂
inst✝ : DecidableEq ι
m : (i : ι) → M₁ i
i : ι
⊢ ∀ (x y : M₁ i),
    (⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ)) (update m i (x + y)) =
      (⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ)) (update m i x) + (⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ)) (update m i y)

Tactic:
by

Goal state after:
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
ht : IsColimit t
i j : J
xi : F.obj i
xj : F.obj j
⊢ (hom (t.ι.app i)) xi = (hom (t.ι.app j)) xj ↔ ∃ k f g, (hom (F.map f)) xi = (hom (F.map g)) xj

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✝¹⁰ : (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₃
ι' : Type u_1
σ : ι ≃ ι'
f : MultilinearMap R (fun i ↦ M₁ (σ.symm i)) M₂
inst✝ : DecidableEq ι
m : (i : ι) → M₁ i
i : ι
c : R
⊢ ∀ (x : M₁ i),
    (⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ)) (update m i (c • x)) = c • (⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ)) (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✝⁹ : (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₃
ι' : Type u_1
σ : ι ≃ ι'
f : MultilinearMap R M₁ M₂
⊢ (fun f ↦ { toFun := ⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ), map_update_add' := ⋯, map_update_smul' := ⋯ })
      ((fun f ↦ { toFun := ⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ).symm, map_update_add' := ⋯, map_update_smul' := ⋯ }) f) =
    f

Tactic:
by

Goal state after:
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
ht : IsColimit t
i : J
x y : F.obj i
⊢ (hom (t.ι.app i)) x = (hom (t.ι.app i)) y ↔ ∃ j f, (hom (F.map f)) x = (hom (F.map f)) 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✝⁹ : (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₃
ι' : Type u_1
σ : ι ≃ ι'
f : MultilinearMap R (fun i ↦ M₁ (σ.symm i)) M₂
⊢ (fun f ↦ { toFun := ⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ).symm, map_update_add' := ⋯, map_update_smul' := ⋯ })
      ((fun f ↦ { toFun := ⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ), map_update_add' := ⋯, map_update_smul' := ⋯ }) f) =
    f

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✝⁹ : (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₃
ι₁ : Type ?u.71
ι₂ : Type ?u.76
σ : ι₁ ≃ ι₂
c : S
f : MultilinearMap R (fun x ↦ M₂) M₃
⊢ (domDomCongrEquiv σ).toFun (c • f) = (RingHom.id S) c • (domDomCongrEquiv σ).toFun f

Tactic:
by

Goal state after:
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
ht : IsColimit t
x₁ x₂ : t.pt
⊢ ∃ j x₁' x₂', (hom (t.ι.app j)) x₁' = x₁ ∧ (hom (t.ι.app j)) x₂' = x₂

Tactic:
by

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

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ GrpCat
j : J
x y : ↑(F.obj j)
⊢ G.mk F ⟨j, x⟩ * G.mk F ⟨j, y⟩ = G.mk F ⟨j, x * y⟩

Tactic:
by

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

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

Tactic:
by

Goal state after:
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)
⊢ ↑(G F)

Tactic:
by

Goal state after:
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)
⊢ x⁻¹ * x = 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₂
inst✝² : (i : ι) → AddCommMonoid (M₁' i)
inst✝¹ : (i : ι) → Module R (M₁' i)
f : MultilinearMap R M₁ M₂
P : ι → Prop
inst✝ : DecidablePred P
⊢ ∀ [inst : DecidableEq { a // ¬P a }] (m : (i : { a // ¬P a }) → M₁ ↑i) (i : { a // ¬P a }) (x y : M₁ ↑i),
    f.domDomRestrict P (update m i (x + y)) = f.domDomRestrict P (update m i x) + f.domDomRestrict P (update m i 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
j k : J
f : j ⟶ k
x : ↑(F.obj j)
⊢ (ConcreteCategory.hom (F.map (𝟙 ⟨k, (ConcreteCategory.hom (F.map f)) x⟩.fst)))
      ⟨k, (ConcreteCategory.hom (F.map f)) x⟩.snd =
    (ConcreteCategory.hom (F.map f)) ⟨j, x⟩.snd

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
⊢ 1 = M.mk F ⟨j, 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₂
inst✝² : (i : ι) → AddCommMonoid (M₁' i)
inst✝¹ : (i : ι) → Module R (M₁' i)
f : MultilinearMap R M₁ M₂
P : ι → Prop
inst✝ : DecidablePred P
⊢ ∀ [inst : DecidableEq { a // ¬P a }] (m : (i : { a // ¬P a }) → M₁ ↑i) (i : { a // ¬P a }) (c : R) (x : M₁ ↑i),
    f.domDomRestrict P (update m i (c • x)) = c • f.domDomRestrict P (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 : ↑(F.obj j₁)
j₂ : J
y : ↑(F.obj j₂)
j₃ : J
x' : ↑(F.obj j₃)
l : J
f : ⟨j₁, x⟩.fst ⟶ l
g : ⟨j₃, x'⟩.fst ⟶ l
hfg :
  (ConcreteCategory.hom ((F ⋙ forget MonCat).map f)) ⟨j₁, x⟩.snd =
    (ConcreteCategory.hom ((F ⋙ forget MonCat).map g)) ⟨j₃, x'⟩.snd
⊢ (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map g)) x'

Tactic:
by

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

Goal state before:
pp: ι : Type u_3
M₁ : ι → Type u_1
α : Type u_2
inst✝¹ : DecidableEq α
s : Set ι
inst✝ : DecidableEq { x // x ∈ s }
e : α ≃ ↑s
m : α → (i : ι) → M₁ i
a : α
z : (i : ι) → M₁ i
⊢ (fun i ↦ update m a z (e.symm i) ↑i) = fun i ↦ update (fun j ↦ m (e.symm j) ↑j) (e a) (z ↑(e a)) i

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)
α : Type u_1
f : MultilinearMap R M₁ M₂
s : Set ι
e : α ≃ ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
z : (i : { a // a ∉ s }) → M₁ ↑i
⊢ ∀ [inst : DecidableEq α] (m : α → (i : ι) → M₁ i) (i : α) (x y : (i : ι) → M₁ i),
    (((f.domDomRestrictₗ fun i ↦ i ∈ s) z) fun i_1 ↦ update m i (x + y) (e.symm i_1) ↑i_1) =
      (((f.domDomRestrictₗ fun i ↦ i ∈ s) z) fun i_1 ↦ update m i x (e.symm i_1) ↑i_1) +
        ((f.domDomRestrictₗ fun i ↦ i ∈ s) z) fun i_1 ↦ update m i y (e.symm i_1) ↑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₂
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
z : (i : { a // a ∉ s }) → M₁ ↑i
⊢ ∀ [inst : DecidableEq α] (m : α → (i : ι) → M₁ i) (i : α) (c : R) (x : (i : ι) → M₁ i),
    (((f.domDomRestrictₗ fun i ↦ i ∈ s) z) fun i_1 ↦ update m i (c • x) (e.symm i_1) ↑i_1) =
      c • ((f.domDomRestrictₗ fun i ↦ i ∈ s) z) fun i_1 ↦ update m i x (e.symm i_1) ↑i_1

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 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

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)
α : 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:
by

Goal state after:
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
o : Type u_3
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
⊢ (blockDiagonal M).det = ∏ k, (M k).det

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)
α : 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:
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)
e : (i : ι) → M₁ i ≃ₗ[R] M₁' i
x✝ : MultilinearMap R M₁' M₂
⊢ (compLinearMapₗ fun x ↦ ↑(e x).symm) ((compLinearMapₗ fun x ↦ ↑(e x)).toFun x✝) = 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✝⁸ : 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)
e : (i : ι) → M₁ i ≃ₗ[R] M₁' i
x✝ : MultilinearMap R M₁ M₂
⊢ (compLinearMapₗ fun x ↦ ↑(e x)).toFun ((compLinearMapₗ fun x ↦ ↑(e x).symm) x✝) = 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 y' : (j : J) × ↑(F.obj j)
hyy' : Types.FilteredColimit.Rel (F ⋙ forget MonCat) y y'
⊢ colimitMulAux F x y = colimitMulAux F x 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
x y : M F
⊢ M 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 : ↑(R F)
⊢ 0 * x = 0

Tactic:
by

Goal state after: