awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
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_1 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_2 : (i : ι) → AddCommMonoid (M₁ i)
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : AddCommMonoid M'
inst_6 : (i : Fin n.succ) → Module.{uR, v} R (M i)
inst_7 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_8 : Module R M₂
inst_9 : Module R M₃
inst_10 : Module R M'
f f' : MultilinearMap R M₁ M₂
ι₁ : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
σ : ι₁ ≃ ι₂
m : MultilinearMap.{uR, u_1, v₂, v₃} R (fun (x : ι₁) ↦ M₂) M₃
inst_11 : DecidableEq ι₂
v : (i : ι₂) → M₂
i : ι₂
a b : M₂
this : DecidableEq ι₁ := ⋯.decidableEq
simp_rw :
  ((m : (a : (i : ι₁) → M₂) → M₃) fun (i_1 : ι₁) ↦
      update (β := fun (a : ι₁) ↦ M₂) (v ∘ (⇑σ : (a : ι₁) → ι₂)) ((σ.symm : (a : ι₂) → ι₁) i) (a + b) i_1) =
    HAdd.hAdd (α := M₃) (β := M₃)
      ((m : (a : (i : ι₁) → M₂) → M₃) fun (i_1 : ι₁) ↦
          update (β := fun (a : ι₁) ↦ M₂) (v ∘ (⇑σ : (a : ι₁) → ι₂)) ((σ.symm : (a : ι₂) → ι₁) i) a i_1 :
        M₃)
      ((m : (a : (i : ι₁) → M₂) → M₃) fun (i_1 : ι₁) ↦
          update (β := fun (a : ι₁) ↦ M₂) (v ∘ (⇑σ : (a : ι₁) → ι₂)) ((σ.symm : (a : ι₂) → ι₁) i) b i_1 :
        M₃)
⊢ ((m : (a : (i : ι₁) → M₂) → M₃) fun (i_1 : ι₁) ↦
      update (β := fun (x : ι₂) ↦ M₂) v i (a + b) ((σ : (a : ι₁) → ι₂) i_1)) =
    HAdd.hAdd (α := M₃) (β := M₃)
      ((m : (a : (i : ι₁) → M₂) → M₃) fun (i_1 : ι₁) ↦ update (β := fun (x : ι₂) ↦ M₂) v i a ((σ : (a : ι₁) → ι₂) i_1) :
        M₃)
      ((m : (a : (i : ι₁) → M₂) → M₃) fun (i_1 : ι₁) ↦ update (β := fun (x : ι₂) ↦ M₂) v i b ((σ : (a : ι₁) → ι₂) i_1) :
        M₃)

Tactic:
simp_rw [Function.update_apply_equiv_apply v]

Premises used: Function.update_apply_equiv_apply
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
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_1 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_2 : (i : ι) → AddCommMonoid (M₁ i)
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : AddCommMonoid M'
inst_6 : (i : Fin n.succ) → Module.{uR, v} R (M i)
inst_7 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_8 : Module R M₂
inst_9 : Module R M₃
inst_10 : Module R M'
f f' : MultilinearMap R M₁ M₂
ι₁ : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
σ : ι₁ ≃ ι₂
m : MultilinearMap.{uR, u_1, v₂, v₃} R (fun (x : ι₁) ↦ M₂) M₃
inst_11 : DecidableEq ι₂
v : (i : ι₂) → M₂
i : ι₂
a b : M₂
this : DecidableEq ι₁ := ⋯.decidableEq
rw rw₁ :
  HAdd.hAdd (α := M₃) (β := M₃)
      ((m : (a : (i : ι₁) → M₂) → M₃)
          (update (β := fun (x : ι₁) ↦ M₂) (v ∘ (⇑σ : (a : ι₁) → ι₂)) ((σ.symm : (a : ι₂) → ι₁) i) a : (a : ι₁) → M₂) :
        M₃)
      ((m : (a : (i : ι₁) → M₂) → M₃)
          (update (β := fun (x : ι₁) ↦ M₂) (v ∘ (⇑σ : (a : ι₁) → ι₂)) ((σ.symm : (a : ι₂) → ι₁) i) b : (a : ι₁) → M₂) :
        M₃) =
    HAdd.hAdd (α := M₃) (β := M₃)
      ((m : (a : (i : ι₁) → M₂) → M₃) fun (i_1 : ι₁) ↦
          update (β := fun (a : ι₁) ↦ M₂) (v ∘ (⇑σ : (a : ι₁) → ι₂)) ((σ.symm : (a : ι₂) → ι₁) i) a i_1 :
        M₃)
      ((m : (a : (i : ι₁) → M₂) → M₃) fun (i_1 : ι₁) ↦
          update (β := fun (a : ι₁) ↦ M₂) (v ∘ (⇑σ : (a : ι₁) → ι₂)) ((σ.symm : (a : ι₂) → ι₁) i) b i_1 :
        M₃)
⊢ ((m : (a : (i : ι₁) → M₂) → M₃) fun (i_1 : ι₁) ↦
      update (β := fun (a : ι₁) ↦ M₂) (v ∘ (⇑σ : (a : ι₁) → ι₂)) ((σ.symm : (a : ι₂) → ι₁) i) (a + b) i_1) =
    HAdd.hAdd (α := M₃) (β := M₃)
      ((m : (a : (i : ι₁) → M₂) → M₃) fun (i_1 : ι₁) ↦
          update (β := fun (a : ι₁) ↦ M₂) (v ∘ (⇑σ : (a : ι₁) → ι₂)) ((σ.symm : (a : ι₂) → ι₁) i) a i_1 :
        M₃)
      ((m : (a : (i : ι₁) → M₂) → M₃) fun (i_1 : ι₁) ↦
          update (β := fun (a : ι₁) ↦ M₂) (v ∘ (⇑σ : (a : ι₁) → ι₂)) ((σ.symm : (a : ι₂) → ι₁) i) b i_1 :
        M₃)

Tactic:
rw [m.map_update_add]

Premises used: MultilinearMap.map_update_add
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
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_1 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_2 : (i : ι) → AddCommMonoid (M₁ i)
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : AddCommMonoid M'
inst_6 : (i : Fin n.succ) → Module.{uR, v} R (M i)
inst_7 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_8 : Module R M₂
inst_9 : Module R M₃
inst_10 : Module R M'
f f' : MultilinearMap R M₁ M₂
ι₁ : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
σ : ι₁ ≃ ι₂
m : MultilinearMap.{uR, u_1, v₂, v₃} R (fun (x : ι₁) ↦ M₂) M₃
inst_11 : DecidableEq ι₂
v : (i : ι₂) → M₂
i : ι₂
a : R
b : M₂
this : DecidableEq ι₁ := ⋯.decidableEq
simp_rw :
  ((m : (a : (i : ι₁) → M₂) → M₃) fun (i_1 : ι₁) ↦
      update (β := fun (a : ι₁) ↦ M₂) (v ∘ (⇑σ : (a : ι₁) → ι₂)) ((σ.symm : (a : ι₂) → ι₁) i) (a • b) i_1) =
    HSMul.hSMul (β := M₃) a
      ((m : (a : (i : ι₁) → M₂) → M₃) fun (i_1 : ι₁) ↦
          update (β := fun (a : ι₁) ↦ M₂) (v ∘ (⇑σ : (a : ι₁) → ι₂)) ((σ.symm : (a : ι₂) → ι₁) i) b i_1 :
        M₃)
⊢ ((m : (a : (i : ι₁) → M₂) → M₃) fun (i_1 : ι₁) ↦
      update (β := fun (x : ι₂) ↦ M₂) v i (a • b) ((σ : (a : ι₁) → ι₂) i_1)) =
    HSMul.hSMul (β := M₃) a
      ((m : (a : (i : ι₁) → M₂) → M₃) fun (i_1 : ι₁) ↦ update (β := fun (x : ι₂) ↦ M₂) v i b ((σ : (a : ι₁) → ι₂) i_1) :
        M₃)

Tactic:
simp_rw [Function.update_apply_equiv_apply v]

Premises used: Function.update_apply_equiv_apply
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
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_1 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_2 : (i : ι) → AddCommMonoid (M₁ i)
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : AddCommMonoid M'
inst_6 : (i : Fin n.succ) → Module.{uR, v} R (M i)
inst_7 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_8 : Module R M₂
inst_9 : Module R M₃
inst_10 : Module R M'
f f' : MultilinearMap R M₁ M₂
ι₁ : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
σ : ι₁ ≃ ι₂
m : MultilinearMap.{uR, u_1, v₂, v₃} R (fun (x : ι₁) ↦ M₂) M₃
inst_11 : DecidableEq ι₂
v : (i : ι₂) → M₂
i : ι₂
a : R
b : M₂
this : DecidableEq ι₁ := ⋯.decidableEq
rw rw₁ :
  HSMul.hSMul (β := M₃) a
      ((m : (a : (i : ι₁) → M₂) → M₃)
          (update (β := fun (x : ι₁) ↦ M₂) (v ∘ (⇑σ : (a : ι₁) → ι₂)) ((σ.symm : (a : ι₂) → ι₁) i) b : (a : ι₁) → M₂) :
        M₃) =
    HSMul.hSMul (β := M₃) a
      ((m : (a : (i : ι₁) → M₂) → M₃) fun (i_1 : ι₁) ↦
          update (β := fun (a : ι₁) ↦ M₂) (v ∘ (⇑σ : (a : ι₁) → ι₂)) ((σ.symm : (a : ι₂) → ι₁) i) b i_1 :
        M₃)
⊢ ((m : (a : (i : ι₁) → M₂) → M₃) fun (i_1 : ι₁) ↦
      update (β := fun (a : ι₁) ↦ M₂) (v ∘ (⇑σ : (a : ι₁) → ι₂)) ((σ.symm : (a : ι₂) → ι₁) i) (a • b) i_1) =
    HSMul.hSMul (β := M₃) a
      ((m : (a : (i : ι₁) → M₂) → M₃) fun (i_1 : ι₁) ↦
          update (β := fun (a : ι₁) ↦ M₂) (v ∘ (⇑σ : (a : ι₁) → ι₂)) ((σ.symm : (a : ι₂) → ι₁) i) b i_1 :
        M₃)

Tactic:
rw [m.map_update_smul]

Premises used: MultilinearMap.map_update_smul
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
M₂ : Type v₂
M₃ : Type v₃
inst : Semiring R
inst_1 : AddCommMonoid M₂
inst_2 : AddCommMonoid M₃
inst_3 : Module R M₂
inst_4 : Module R M₃
ι₁ : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
σ₁ : ι₁ ≃ ι₂
σ₂ : ι₂ ≃ ι₃
m : MultilinearMap.{uR, u_1, v₂, v₃} R (fun (x : ι₁) ↦ M₂) M₃
⊢ domDomCongr (σ₁.trans σ₂) m = domDomCongr σ₂ (domDomCongr σ₁ m)

Tactic:
rfl

Premises used: Equiv.trans, MultilinearMap.domDomCongr, rfl
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
M₂ : Type v₂
M₃ : Type v₃
inst : Semiring R
inst_1 : AddCommMonoid M₂
inst_2 : AddCommMonoid M₃
inst_3 : Module R M₂
inst_4 : Module R M₃
ι₁ : Type u_1
σ₁ σ₂ : Equiv.Perm ι₁
m : MultilinearMap.{uR, u_1, v₂, v₃} R (fun (x : ι₁) ↦ M₂) M₃
⊢ domDomCongr (σ₂ * σ₁) m = domDomCongr σ₂ (domDomCongr σ₁ m)

Tactic:
rfl

Premises used: Equiv.trans, MultilinearMap.domDomCongr, rfl
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
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_1 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_2 : (i : ι) → AddCommMonoid (M₁ i)
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : AddCommMonoid M'
inst_6 : (i : Fin n.succ) → Module.{uR, v} R (M i)
inst_7 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_8 : Module R M₂
inst_9 : Module R M₃
inst_10 : Module R M'
f f' : MultilinearMap R M₁ M₂
ι₁ : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
σ : ι₁ ≃ ι₂
m : MultilinearMap.{uR, u_1, v₂, v₃} R (fun (x : ι₁) ↦ M₂) M₃
H :
  ∀ (x : (i : ι₁) → M₂),
    Eq.{v₃ + 1} (α := M₃) ((domDomCongr σ.symm (domDomCongr σ m) : (a : (i : ι₁) → M₂) → M₃) x : M₃)
      ((m : (a : (i : ι₁) → M₂) → M₃) x : M₃)
⊢ domDomCongr σ.symm (domDomCongr σ m) = m

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
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_1 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_2 : (i : ι) → AddCommMonoid (M₁ i)
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : AddCommMonoid M'
inst_6 : (i : Fin n.succ) → Module.{uR, v} R (M i)
inst_7 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_8 : Module R M₂
inst_9 : Module R M₃
inst_10 : Module R M'
f f' : MultilinearMap R M₁ M₂
ι₁ : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
σ : ι₁ ≃ ι₂
m : MultilinearMap.{uR, u_1, v₂, v₃} R (fun (x : ι₁) ↦ M₂) M₃
x : (i : ι₁) → M₂
⊢ Eq.{v₃ + 1} (α := M₃) ((domDomCongr σ.symm (domDomCongr σ m) : (a : (i : ι₁) → M₂) → M₃) x : M₃)
    ((m : (a : (i : ι₁) → M₂) → M₃) x : M₃)

Tactic:
simp [domDomCongr]

Premises used: MultilinearMap.domDomCongr
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
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_1 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_2 : (i : ι) → AddCommMonoid (M₁ i)
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : AddCommMonoid M'
inst_6 : (i : Fin n.succ) → Module.{uR, v} R (M i)
inst_7 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_8 : Module R M₂
inst_9 : Module R M₃
inst_10 : Module R M'
f f' : MultilinearMap R M₁ M₂
ι₁ : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
σ : ι₁ ≃ ι₂
m : MultilinearMap.{uR, u_2, v₂, v₃} R (fun (x : ι₂) ↦ M₂) M₃
H :
  ∀ (x : (i : ι₂) → M₂),
    Eq.{v₃ + 1} (α := M₃) ((domDomCongr σ (domDomCongr σ.symm m) : (a : (i : ι₂) → M₂) → M₃) x : M₃)
      ((m : (a : (i : ι₂) → M₂) → M₃) x : M₃)
⊢ domDomCongr σ (domDomCongr σ.symm m) = m

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
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_1 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_2 : (i : ι) → AddCommMonoid (M₁ i)
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : AddCommMonoid M'
inst_6 : (i : Fin n.succ) → Module.{uR, v} R (M i)
inst_7 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_8 : Module R M₂
inst_9 : Module R M₃
inst_10 : Module R M'
f f' : MultilinearMap R M₁ M₂
ι₁ : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
σ : ι₁ ≃ ι₂
m : MultilinearMap.{uR, u_2, v₂, v₃} R (fun (x : ι₂) ↦ M₂) M₃
x : (i : ι₂) → M₂
⊢ Eq.{v₃ + 1} (α := M₃) ((domDomCongr σ (domDomCongr σ.symm m) : (a : (i : ι₂) → M₂) → M₃) x : M₃)
    ((m : (a : (i : ι₂) → M₂) → M₃) x : M₃)

Tactic:
simp [domDomCongr]

Premises used: MultilinearMap.domDomCongr
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
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_1 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_2 : (i : ι) → AddCommMonoid (M₁ i)
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : AddCommMonoid M'
inst_6 : (i : Fin n.succ) → Module.{uR, v} R (M i)
inst_7 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_8 : Module R M₂
inst_9 : Module R M₃
inst_10 : Module R M'
f f' : MultilinearMap R M₁ M₂
ι₁ : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
σ : ι₁ ≃ ι₂
a b : MultilinearMap.{uR, u_1, v₂, v₃} R (fun (x : ι₁) ↦ M₂) M₃
H :
  ∀ (x : (i : ι₂) → M₂),
    Eq.{v₃ + 1} (α := M₃) ((domDomCongr σ (a + b) : (a : (i : ι₂) → M₂) → M₃) x : M₃)
      ((domDomCongr σ a + domDomCongr σ b : (a : (i : ι₂) → M₂) → M₃) x : M₃)
⊢ domDomCongr σ (a + b) = domDomCongr σ a + domDomCongr σ b

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
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_1 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_2 : (i : ι) → AddCommMonoid (M₁ i)
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : AddCommMonoid M'
inst_6 : (i : Fin n.succ) → Module.{uR, v} R (M i)
inst_7 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_8 : Module R M₂
inst_9 : Module R M₃
inst_10 : Module R M'
f f' : MultilinearMap R M₁ M₂
ι₁ : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
σ : ι₁ ≃ ι₂
a b : MultilinearMap.{uR, u_1, v₂, v₃} R (fun (x : ι₁) ↦ M₂) M₃
x : (i : ι₂) → M₂
⊢ Eq.{v₃ + 1} (α := M₃) ((domDomCongr σ (a + b) : (a : (i : ι₂) → M₂) → M₃) x : M₃)
    ((domDomCongr σ a + domDomCongr σ b : (a : (i : ι₂) → M₂) → M₃) x : M₃)

Tactic:
simp [domDomCongr]

Premises used: MultilinearMap.domDomCongr
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
M₂ : Type v₂
M₃ : Type v₃
inst : Semiring R
inst_1 : AddCommMonoid M₂
inst_2 : AddCommMonoid M₃
inst_3 : Module R M₂
inst_4 : Module R M₃
ι₁ : Type u_1
ι₂ : Type u_2
σ : ι₁ ≃ ι₂
f g : MultilinearMap.{uR, u_1, v₂, v₃} R (fun (x : ι₁) ↦ M₂) M₃
⊢ domDomCongr σ f = domDomCongr σ g ↔ f = g

Tactic:
(domDomCongrEquiv σ : _ ≃+ MultilinearMap R (fun _ => M₂) M₃).apply_eq_iff_eq

Premises used: AddEquiv.apply_eq_iff_eq, MultilinearMap.domDomCongr, MultilinearMap.domDomCongrEquiv
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
ι : Sort u_2
inst : DecidableEq ι
P : ι → Prop
inst_1 : DecidablePred P
M₁ : ι → Type u_1
inst_2 : DecidableEq.{max 1 u_2} { a : ι // P a }
x : (i : { a : ι // P a }) → M₁ (↑i : ι)
z : (i : { a : ι // ¬P a }) → M₁ (↑i : ι)
i : { a : ι // P a }
c : M₁ (↑i : ι)
⊢ (fun (j : ι) ↦
      if h : P j then
        update.{max 1 u_2, u_1 + 1} (β := fun (a : { a : ι // P a }) ↦ M₁ (↑a : ι)) x i c
          (Subtype.mk (p := fun (a : ι) ↦ P a) j h)
      else z (Subtype.mk (p := fun (a : ι) ↦ ¬P a) j h)) =
    update (β := M₁)
      (fun (j : ι) ↦
        if h : P j then x (Subtype.mk (p := fun (a : ι) ↦ P a) j h) else z (Subtype.mk (p := fun (a : ι) ↦ ¬P a) j h))
      (↑i : ι) c

Tactic:
grind
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
ι : Sort u_2
inst : DecidableEq ι
P : ι → Prop
inst_1 : DecidablePred P
M₁ : ι → Type u_1
inst_2 : DecidableEq.{max 1 u_2} { a : ι // ¬P a }
x : (i : { a : ι // P a }) → M₁ (↑i : ι)
z : (i : { a : ι // ¬P a }) → M₁ (↑i : ι)
i : { a : ι // ¬P a }
c : M₁ (↑i : ι)
⊢ (fun (j : ι) ↦
      if h : P j then x (Subtype.mk (p := fun (a : ι) ↦ P a) j h)
      else
        update.{max 1 u_2, u_1 + 1} (β := fun (a : { a : ι // ¬P a }) ↦ M₁ (↑a : ι)) z i c
          (Subtype.mk (p := fun (a : ι) ↦ ¬P a) j h)) =
    update (β := M₁)
      (fun (j : ι) ↦
        if h : P j then x (Subtype.mk (p := fun (a : ι) ↦ P a) j h) else z (Subtype.mk (p := fun (a : ι) ↦ ¬P a) j h))
      (↑i : ι) c

Tactic:
simpa only [dite_not] using domDomRestrict_aux _ z (fun j ↦ x ⟨j.1, not_not.mp j.2⟩) i c

Premises used: Classical.not_not, dite_not, Subtype.mk, MultilinearMap.domDomRestrict_aux, Iff.mp, Subtype.val, Subtype.property
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
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_1 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_2 : (i : ι) → AddCommMonoid (M₁ i)
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : AddCommMonoid M'
inst_6 : (i : Fin n.succ) → Module.{uR, v} R (M i)
inst_7 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_8 : Module R M₂
inst_9 : Module R M₃
inst_10 : Module R M'
f_1 f' f : MultilinearMap R M₁ M₂
P : ι → Prop
inst_11 : DecidablePred P
z : (i : { a : ι // ¬P a }) → M₁ (↑i : ι)
inst_12 : DecidableEq { a : ι // P a }
x : (i : { a : ι // P a }) → M₁ (↑i : ι)
i : { a : ι // P a }
a b : M₁ (↑i : ι)
rw :
  (f : (a : (i : ι) → M₁ i) → M₂)
      (update (β := M₁)
        (fun (j : ι) ↦
          if h : P j then x (Subtype.mk (p := fun (a : ι) ↦ P a) j h) else z (Subtype.mk (p := fun (a : ι) ↦ ¬P a) j h))
        (↑i : ι) (a + b)) =
    HAdd.hAdd (α := M₂) (β := M₂)
      ((f : (a : (i : ι) → M₁ i) → M₂) fun (j : ι) ↦
          if h : P j then
            update (β := fun (i : { a : ι // P a }) ↦ M₁ (↑i : ι)) x i a (Subtype.mk (p := fun (a : ι) ↦ P a) j h)
          else z (Subtype.mk (p := fun (a : ι) ↦ ¬P a) j h) :
        M₂)
      ((f : (a : (i : ι) → M₁ i) → M₂) fun (j : ι) ↦
          if h : P j then
            update (β := fun (i : { a : ι // P a }) ↦ M₁ (↑i : ι)) x i b (Subtype.mk (p := fun (a : ι) ↦ P a) j h)
          else z (Subtype.mk (p := fun (a : ι) ↦ ¬P a) j h) :
        M₂)
⊢ ((f : (a : (i : ι) → M₁ i) → M₂) fun (j : ι) ↦
      if h : P j then
        update (β := fun (i : { a : ι // P a }) ↦ M₁ (↑i : ι)) x i (a + b) (Subtype.mk (p := fun (a : ι) ↦ P a) j h)
      else z (Subtype.mk (p := fun (a : ι) ↦ ¬P a) j h)) =
    HAdd.hAdd (α := M₂) (β := M₂)
      ((f : (a : (i : ι) → M₁ i) → M₂) fun (j : ι) ↦
          if h : P j then
            update (β := fun (i : { a : ι // P a }) ↦ M₁ (↑i : ι)) x i a (Subtype.mk (p := fun (a : ι) ↦ P a) j h)
          else z (Subtype.mk (p := fun (a : ι) ↦ ¬P a) j h) :
        M₂)
      ((f : (a : (i : ι) → M₁ i) → M₂) fun (j : ι) ↦
          if h : P j then
            update (β := fun (i : { a : ι // P a }) ↦ M₁ (↑i : ι)) x i b (Subtype.mk (p := fun (a : ι) ↦ P a) j h)
          else z (Subtype.mk (p := fun (a : ι) ↦ ¬P a) j h) :
        M₂)

Tactic:
rw [domDomRestrict_aux]

Premises used: MultilinearMap.domDomRestrict_aux
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
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_1 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_2 : (i : ι) → AddCommMonoid (M₁ i)
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : AddCommMonoid M'
inst_6 : (i : Fin n.succ) → Module.{uR, v} R (M i)
inst_7 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_8 : Module R M₂
inst_9 : Module R M₃
inst_10 : Module R M'
f_1 f' f : MultilinearMap R M₁ M₂
P : ι → Prop
inst_11 : DecidablePred P
z : (i : { a : ι // ¬P a }) → M₁ (↑i : ι)
inst_12 : DecidableEq { a : ι // P a }
x : (i : { a : ι // P a }) → M₁ (↑i : ι)
i : { a : ι // P a }
a b : M₁ (↑i : ι)
rw :
  (f : (a : (i : ι) → M₁ i) → M₂)
      (update (β := M₁)
        (fun (j : ι) ↦
          if h : P j then x (Subtype.mk (p := fun (a : ι) ↦ P a) j h) else z (Subtype.mk (p := fun (a : ι) ↦ ¬P a) j h))
        (↑i : ι) (a + b)) =
    HAdd.hAdd (α := M₂) (β := M₂)
      ((f : (a : (i : ι) → M₁ i) → M₂)
          (update (β := M₁)
            (fun (j : ι) ↦
              if h : P j then x (Subtype.mk (p := fun (a : ι) ↦ P a) j h)
              else z (Subtype.mk (p := fun (a : ι) ↦ ¬P a) j h))
            (↑i : ι) a) :
        M₂)
      ((f : (a : (i : ι) → M₁ i) → M₂) fun (j : ι) ↦
          if h : P j then
            update (β := fun (i : { a : ι // P a }) ↦ M₁ (↑i : ι)) x i b (Subtype.mk (p := fun (a : ι) ↦ P a) j h)
          else z (Subtype.mk (p := fun (a : ι) ↦ ¬P a) j h) :
        M₂)
⊢ (f : (a : (i : ι) → M₁ i) → M₂)
      (update (β := M₁)
        (fun (j : ι) ↦
          if h : P j then x (Subtype.mk (p := fun (a : ι) ↦ P a) j h) else z (Subtype.mk (p := fun (a : ι) ↦ ¬P a) j h))
        (↑i : ι) (a + b)) =
    HAdd.hAdd (α := M₂) (β := M₂)
      ((f : (a : (i : ι) → M₁ i) → M₂) fun (j : ι) ↦
          if h : P j then
            update (β := fun (i : { a : ι // P a }) ↦ M₁ (↑i : ι)) x i a (Subtype.mk (p := fun (a : ι) ↦ P a) j h)
          else z (Subtype.mk (p := fun (a : ι) ↦ ¬P a) j h) :
        M₂)
      ((f : (a : (i : ι) → M₁ i) → M₂) fun (j : ι) ↦
          if h : P j then
            update (β := fun (i : { a : ι // P a }) ↦ M₁ (↑i : ι)) x i b (Subtype.mk (p := fun (a : ι) ↦ P a) j h)
          else z (Subtype.mk (p := fun (a : ι) ↦ ¬P a) j h) :
        M₂)

Tactic:
rw [domDomRestrict_aux]

Premises used: MultilinearMap.domDomRestrict_aux
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
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_1 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_2 : (i : ι) → AddCommMonoid (M₁ i)
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : AddCommMonoid M'
inst_6 : (i : Fin n.succ) → Module.{uR, v} R (M i)
inst_7 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_8 : Module R M₂
inst_9 : Module R M₃
inst_10 : Module R M'
f_1 f' f : MultilinearMap R M₁ M₂
P : ι → Prop
inst_11 : DecidablePred P
z : (i : { a : ι // ¬P a }) → M₁ (↑i : ι)
inst_12 : DecidableEq { a : ι // P a }
x : (i : { a : ι // P a }) → M₁ (↑i : ι)
i : { a : ι // P a }
a b : M₁ (↑i : ι)
rw :
  (f : (a : (i : ι) → M₁ i) → M₂)
      (update (β := M₁)
        (fun (j : ι) ↦
          if h : P j then x (Subtype.mk (p := fun (a : ι) ↦ P a) j h) else z (Subtype.mk (p := fun (a : ι) ↦ ¬P a) j h))
        (↑i : ι) (a + b)) =
    HAdd.hAdd (α := M₂) (β := M₂)
      ((f : (a : (i : ι) → M₁ i) → M₂)
          (update (β := M₁)
            (fun (j : ι) ↦
              if h : P j then x (Subtype.mk (p := fun (a : ι) ↦ P a) j h)
              else z (Subtype.mk (p := fun (a : ι) ↦ ¬P a) j h))
            (↑i : ι) a) :
        M₂)
      ((f : (a : (i : ι) → M₁ i) → M₂)
          (update (β := M₁)
            (fun (j : ι) ↦
              if h : P j then x (Subtype.mk (p := fun (a : ι) ↦ P a) j h)
              else z (Subtype.mk (p := fun (a : ι) ↦ ¬P a) j h))
            (↑i : ι) b) :
        M₂)
⊢ (f : (a : (i : ι) → M₁ i) → M₂)
      (update (β := M₁)
        (fun (j : ι) ↦
          if h : P j then x (Subtype.mk (p := fun (a : ι) ↦ P a) j h) else z (Subtype.mk (p := fun (a : ι) ↦ ¬P a) j h))
        (↑i : ι) (a + b)) =
    HAdd.hAdd (α := M₂) (β := M₂)
      ((f : (a : (i : ι) → M₁ i) → M₂)
          (update (β := M₁)
            (fun (j : ι) ↦
              if h : P j then x (Subtype.mk (p := fun (a : ι) ↦ P a) j h)
              else z (Subtype.mk (p := fun (a : ι) ↦ ¬P a) j h))
            (↑i : ι) a) :
        M₂)
      ((f : (a : (i : ι) → M₁ i) → M₂) fun (j : ι) ↦
          if h : P j then
            update (β := fun (i : { a : ι // P a }) ↦ M₁ (↑i : ι)) x i b (Subtype.mk (p := fun (a : ι) ↦ P a) j h)
          else z (Subtype.mk (p := fun (a : ι) ↦ ¬P a) j h) :
        M₂)

Tactic:
rw [domDomRestrict_aux]

Premises used: MultilinearMap.domDomRestrict_aux