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✝¹⁰ : Semiring R
inst✝⁹ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁸ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : (i : Fin n.succ) → Module R (M i)
inst✝³ : (i : ι) → Module R (M₁ i)
inst✝² : Module R M₂
inst✝¹ : Module R M₃
inst✝ : Module R M'
f f' : MultilinearMap R M₁ M₂
ι₁ : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
σ : ι₁ ≃ ι₂
a b : MultilinearMap R (fun x ↦ M₂) M₃
⊢ domDomCongr σ (a + b) = domDomCongr σ a + domDomCongr σ b

Tactic:
ext

Goal state after:
R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst✝¹⁰ : Semiring R
inst✝⁹ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁸ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : (i : Fin n.succ) → Module R (M i)
inst✝³ : (i : ι) → Module R (M₁ i)
inst✝² : Module R M₂
inst✝¹ : Module R M₃
inst✝ : Module R M'
f f' : MultilinearMap R M₁ M₂
ι₁ : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
σ : ι₁ ≃ ι₂
a b : MultilinearMap R (fun x ↦ M₂) M₃
x✝ : ι₂ → M₂
⊢ (domDomCongr σ (a + b)) x✝ = (domDomCongr σ a + domDomCongr σ b) x✝
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: R : Type v
inst✝ : CommRing R
n : ℕ
A B : Matrix (Fin (n + 1)) (Fin (n + 1)) R
c : Fin n → R
A_zero : ∀ (i : Fin (n + 1)), A i 0 = B i 0
A_succ : ∀ (i : Fin (n + 1)) (j : Fin n), A i j.succ = B i j.succ + c j * A i j.castSucc
⊢ A.det = B.det

Tactic:
← det_transpose A,

Goal state after:
R : Type v
inst✝ : CommRing R
n : ℕ
A B : Matrix (Fin (n + 1)) (Fin (n + 1)) R
c : Fin n → R
A_zero : ∀ (i : Fin (n + 1)), A i 0 = B i 0
A_succ : ∀ (i : Fin (n + 1)) (j : Fin n), A i j.succ = B i j.succ + c j * A i j.castSucc
⊢ Aᵀ.det = B.det
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: R : Type uR
M₂ : Type v₂
M₃ : Type v₃
M' : Type v'
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : AddCommMonoid M'
inst✝² : Module R M₂
inst✝¹ : Module R M₃
inst✝ : Module R M'
ι₁ : Type u_1
ι₂ : Type u_2
σ : ι₁ ≃ ι₂
g : M₂ →ₗ[R] M₃
f : MultilinearMap R (fun x ↦ M') M₂
⊢ MultilinearMap.domDomCongr σ (g.compMultilinearMap f) = g.compMultilinearMap (MultilinearMap.domDomCongr σ f)

Tactic:
ext

Goal state after:
R : Type uR
M₂ : Type v₂
M₃ : Type v₃
M' : Type v'
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : AddCommMonoid M'
inst✝² : Module R M₂
inst✝¹ : Module R M₃
inst✝ : Module R M'
ι₁ : Type u_1
ι₂ : Type u_2
σ : ι₁ ≃ ι₂
g : M₂ →ₗ[R] M₃
f : MultilinearMap R (fun x ↦ M') M₂
x✝ : ι₂ → M'
⊢ (MultilinearMap.domDomCongr σ (g.compMultilinearMap f)) x✝ =
    (g.compMultilinearMap (MultilinearMap.domDomCongr σ f)) 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₂
⊢ (LinearMap.compMultilinearMapₗ S ↑g.symm) ((LinearMap.compMultilinearMapₗ S ↑g).toFun x✝) = x✝

Tactic:
ext

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₃
⊢ (LinearMap.compMultilinearMapₗ S ↑g).toFun ((LinearMap.compMultilinearMapₗ S ↑g.symm) x✝) = x✝

Tactic:
ext

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.CategoryTheory.Limits.Types.Filtered

Goal state before:
pp: J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : IsFilteredOrEmpty J
j : J
x : F.obj j
j' : J
y : F.obj j'
⊢ FilteredColimit.Rel F ⟨j, x⟩ ⟨j', y⟩ ↔ Relation.EqvGen F.ColimitTypeRel ⟨j, x⟩ ⟨j', y⟩

Tactic:
constructor

Goal state after:
case mp
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : IsFilteredOrEmpty J
j : J
x : F.obj j
j' : J
y : F.obj j'
⊢ FilteredColimit.Rel F ⟨j, x⟩ ⟨j', y⟩ → Relation.EqvGen F.ColimitTypeRel ⟨j, x⟩ ⟨j', y⟩

case mpr
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : IsFilteredOrEmpty J
j : J
x : F.obj j
j' : J
y : F.obj j'
⊢ Relation.EqvGen F.ColimitTypeRel ⟨j, x⟩ ⟨j', y⟩ → FilteredColimit.Rel F ⟨j, 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✝¹¹ : 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:
ext

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

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

case snd
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).2 = (σ (x, k)).2
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:
ext

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₃
ι' : Type u_1
σ : ι ≃ ι'
c : S
f : MultilinearMap R M₁ M₂
x✝ : (i : ι') → M₁ (σ.symm i)
⊢ { toFun := ⇑(c • f) ∘ ⇑(Equiv.piCongrLeft' M₁ σ).symm, map_update_add' := ⋯, map_update_smul' := ⋯ } x✝ =
    ((RingHom.id S) c • { toFun := ⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ).symm, map_update_add' := ⋯, map_update_smul' := ⋯ })
      x✝
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
⊢ (∃ k f g, (hom (F.map f)) x = (hom (F.map g)) y) ↔ ∃ j f, (hom (F.map f)) x = (hom (F.map f)) y

Tactic:
constructor

Goal state after:
case mp
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
⊢ (∃ k f g, (hom (F.map f)) x = (hom (F.map g)) y) → ∃ j f, (hom (F.map f)) x = (hom (F.map f)) y

case mpr
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
⊢ (∃ j f, (hom (F.map f)) x = (hom (F.map f)) y) → ∃ k f g, (hom (F.map f)) x = (hom (F.map g)) 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✝¹¹ : 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:
ext

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₃
ι' : Type u_1
σ : ι ≃ ι'
f : MultilinearMap R M₁ M₂
x✝ : (i : ι) → M₁ i
⊢ ((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))
      x✝ =
    f 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₃
ι' : 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:
ext

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₃
ι' : Type u_1
σ : ι ≃ ι'
f : MultilinearMap R (fun i ↦ M₁ (σ.symm i)) M₂
x✝ : (i : ι') → M₁ (σ.symm i)
⊢ ((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))
      x✝ =
    f 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₃
ι₁ : 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:
ext

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₃
ι₁ : Type ?u.71
ι₂ : Type ?u.76
σ : ι₁ ≃ ι₂
c : S
f : MultilinearMap R (fun x ↦ M₂) M₃
x✝ : ι₂ → M₂
⊢ ((domDomCongrEquiv σ).toFun (c • f)) x✝ = ((RingHom.id S) c • (domDomCongrEquiv σ).toFun f) 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✝⁹ : 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
    intro h m i x y
    classical
    ext v
    simp [domDomRestrict_aux_right]

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

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.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:
ext

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✝