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 : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_3 : AddCommMonoid M₂
inst_4 : (i : Fin n.succ) → Module.{uR, v} R (M i)
inst_5 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_6 : Module R M₂
f_1 f' : MultilinearMap R M₁ M₂
inst_7 : (i : ι) → AddCommMonoid (M₁' i)
inst_8 : (i : ι) → Module.{uR, v₁'} R (M₁' i)
f : MultilinearMap R M₁ M₂
P : ι → Prop
inst_9 : DecidablePred P
h : DecidableEq { a : ι // ¬P a }
m : (i : { a : ι // ¬P a }) → M₁ (↑i : ι)
i : { a : ι // ¬P a }
x y : M₁ (↑i : ι)
H :
  ∀ (v : (i : { a : ι // P a }) → M₁ (↑i : ι)),
    Eq.{v₂ + 1} (α := M₂)
      ((f.domDomRestrict (M₁ := M₁) P (update (β := fun (i : { a : ι // ¬P a }) ↦ M₁ (↑i : ι)) m i (x + y)) :
            (a : (i : { a : ι // P a }) → M₁ (↑i : ι)) → M₂)
          v :
        M₂)
      ((f.domDomRestrict (M₁ := M₁) P (update (β := fun (i : { a : ι // ¬P a }) ↦ M₁ (↑i : ι)) m i x) +
              f.domDomRestrict (M₁ := M₁) P (update (β := fun (i : { a : ι // ¬P a }) ↦ M₁ (↑i : ι)) m i y) :
            (a : (i : { a : ι // P a }) → M₁ (↑i : ι)) → M₂)
          v :
        M₂)
⊢ f.domDomRestrict (M₁ := M₁) P (update (β := fun (i : { a : ι // ¬P a }) ↦ M₁ (↑i : ι)) m i (x + y)) =
    f.domDomRestrict (M₁ := M₁) P (update (β := fun (i : { a : ι // ¬P a }) ↦ M₁ (↑i : ι)) m i x) +
      f.domDomRestrict (M₁ := M₁) P (update (β := fun (i : { a : ι // ¬P a }) ↦ M₁ (↑i : ι)) m i y)

Tactic:
ext v
-- 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 : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_3 : AddCommMonoid M₂
inst_4 : (i : Fin n.succ) → Module.{uR, v} R (M i)
inst_5 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_6 : Module R M₂
f_1 f' : MultilinearMap R M₁ M₂
inst_7 : (i : ι) → AddCommMonoid (M₁' i)
inst_8 : (i : ι) → Module.{uR, v₁'} R (M₁' i)
f : MultilinearMap R M₁ M₂
P : ι → Prop
inst_9 : DecidablePred P
h : DecidableEq { a : ι // ¬P a }
m : (i : { a : ι // ¬P a }) → M₁ (↑i : ι)
i : { a : ι // ¬P a }
x y : M₁ (↑i : ι)
v : (i : { a : ι // P a }) → M₁ (↑i : ι)
⊢ Eq.{v₂ + 1} (α := M₂)
    ((f.domDomRestrict (M₁ := M₁) P (update (β := fun (i : { a : ι // ¬P a }) ↦ M₁ (↑i : ι)) m i (x + y)) :
          (a : (i : { a : ι // P a }) → M₁ (↑i : ι)) → M₂)
        v :
      M₂)
    ((f.domDomRestrict (M₁ := M₁) P (update (β := fun (i : { a : ι // ¬P a }) ↦ M₁ (↑i : ι)) m i x) +
            f.domDomRestrict (M₁ := M₁) P (update (β := fun (i : { a : ι // ¬P a }) ↦ M₁ (↑i : ι)) m i y) :
          (a : (i : { a : ι // P a }) → M₁ (↑i : ι)) → M₂)
        v :
      M₂)

Tactic:
simp [domDomRestrict_aux_right]

Premises used: MultilinearMap.domDomRestrict_aux_right
-- 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 : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_3 : AddCommMonoid M₂
inst_4 : (i : Fin n.succ) → Module.{uR, v} R (M i)
inst_5 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_6 : Module R M₂
f_1 f' : MultilinearMap R M₁ M₂
inst_7 : (i : ι) → AddCommMonoid (M₁' i)
inst_8 : (i : ι) → Module.{uR, v₁'} R (M₁' i)
f : MultilinearMap R M₁ M₂
P : ι → Prop
inst_9 : DecidablePred P
h : DecidableEq { a : ι // ¬P a }
m : (i : { a : ι // ¬P a }) → M₁ (↑i : ι)
i : { a : ι // ¬P a }
x y : M₁ (↑i : ι)
H :
  ∀ (v : (i : { a : ι // P a }) → M₁ (↑i : ι)),
    Eq.{v₂ + 1} (α := M₂)
      ((f.domDomRestrict (M₁ := M₁) P (update (β := fun (i : { a : ι // ¬P a }) ↦ M₁ (↑i : ι)) m i (x + y)) :
            (a : (i : { a : ι // P a }) → M₁ (↑i : ι)) → M₂)
          v :
        M₂)
      ((f.domDomRestrict (M₁ := M₁) P (update (β := fun (i : { a : ι // ¬P a }) ↦ M₁ (↑i : ι)) m i x) +
              f.domDomRestrict (M₁ := M₁) P (update (β := fun (i : { a : ι // ¬P a }) ↦ M₁ (↑i : ι)) m i y) :
            (a : (i : { a : ι // P a }) → M₁ (↑i : ι)) → M₂)
          v :
        M₂)
⊢ f.domDomRestrict (M₁ := M₁) P (update (β := fun (i : { a : ι // ¬P a }) ↦ M₁ (↑i : ι)) m i (x + y)) =
    f.domDomRestrict (M₁ := M₁) P (update (β := fun (i : { a : ι // ¬P a }) ↦ M₁ (↑i : ι)) m i x) +
      f.domDomRestrict (M₁ := M₁) P (update (β := fun (i : { a : ι // ¬P a }) ↦ M₁ (↑i : ι)) m i y)

Tactic:
classical
    ext v
    simp [domDomRestrict_aux_right]

Premises used: MultilinearMap.domDomRestrict_aux_right
-- 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 : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_3 : AddCommMonoid M₂
inst_4 : (i : Fin n.succ) → Module.{uR, v} R (M i)
inst_5 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_6 : Module R M₂
f_1 f' : MultilinearMap R M₁ M₂
inst_7 : (i : ι) → AddCommMonoid (M₁' i)
inst_8 : (i : ι) → Module.{uR, v₁'} R (M₁' i)
f : MultilinearMap R M₁ M₂
P : ι → Prop
inst_9 : DecidablePred P
h : DecidableEq { a : ι // ¬P a }
m : (i : { a : ι // ¬P a }) → M₁ (↑i : ι)
i : { a : ι // ¬P a }
c : R
x : M₁ (↑i : ι)
H :
  ∀ (v : (i : { a : ι // P a }) → M₁ (↑i : ι)),
    Eq.{v₂ + 1} (α := M₂)
      ((f.domDomRestrict (M₁ := M₁) P (update (β := fun (i : { a : ι // ¬P a }) ↦ M₁ (↑i : ι)) m i (c • x)) :
            (a : (i : { a : ι // P a }) → M₁ (↑i : ι)) → M₂)
          v :
        M₂)
      ((c • f.domDomRestrict (M₁ := M₁) P (update (β := fun (i : { a : ι // ¬P a }) ↦ M₁ (↑i : ι)) m i x) :
            (a : (i : { a : ι // P a }) → M₁ (↑i : ι)) → M₂)
          v :
        M₂)
⊢ f.domDomRestrict (M₁ := M₁) P (update (β := fun (i : { a : ι // ¬P a }) ↦ M₁ (↑i : ι)) m i (c • x)) =
    c • f.domDomRestrict (M₁ := M₁) P (update (β := fun (i : { a : ι // ¬P a }) ↦ M₁ (↑i : ι)) m i x)

Tactic:
ext v
-- 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 : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_3 : AddCommMonoid M₂
inst_4 : (i : Fin n.succ) → Module.{uR, v} R (M i)
inst_5 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_6 : Module R M₂
f_1 f' : MultilinearMap R M₁ M₂
inst_7 : (i : ι) → AddCommMonoid (M₁' i)
inst_8 : (i : ι) → Module.{uR, v₁'} R (M₁' i)
f : MultilinearMap R M₁ M₂
P : ι → Prop
inst_9 : DecidablePred P
h : DecidableEq { a : ι // ¬P a }
m : (i : { a : ι // ¬P a }) → M₁ (↑i : ι)
i : { a : ι // ¬P a }
c : R
x : M₁ (↑i : ι)
v : (i : { a : ι // P a }) → M₁ (↑i : ι)
⊢ Eq.{v₂ + 1} (α := M₂)
    ((f.domDomRestrict (M₁ := M₁) P (update (β := fun (i : { a : ι // ¬P a }) ↦ M₁ (↑i : ι)) m i (c • x)) :
          (a : (i : { a : ι // P a }) → M₁ (↑i : ι)) → M₂)
        v :
      M₂)
    ((c • f.domDomRestrict (M₁ := M₁) P (update (β := fun (i : { a : ι // ¬P a }) ↦ M₁ (↑i : ι)) m i x) :
          (a : (i : { a : ι // P a }) → M₁ (↑i : ι)) → M₂)
        v :
      M₂)

Tactic:
simp [domDomRestrict_aux_right]

Premises used: MultilinearMap.domDomRestrict_aux_right
-- 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 : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_3 : AddCommMonoid M₂
inst_4 : (i : Fin n.succ) → Module.{uR, v} R (M i)
inst_5 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_6 : Module R M₂
f_1 f' : MultilinearMap R M₁ M₂
inst_7 : (i : ι) → AddCommMonoid (M₁' i)
inst_8 : (i : ι) → Module.{uR, v₁'} R (M₁' i)
f : MultilinearMap R M₁ M₂
P : ι → Prop
inst_9 : DecidablePred P
h : DecidableEq { a : ι // ¬P a }
m : (i : { a : ι // ¬P a }) → M₁ (↑i : ι)
i : { a : ι // ¬P a }
c : R
x : M₁ (↑i : ι)
H :
  ∀ (v : (i : { a : ι // P a }) → M₁ (↑i : ι)),
    Eq.{v₂ + 1} (α := M₂)
      ((f.domDomRestrict (M₁ := M₁) P (update (β := fun (i : { a : ι // ¬P a }) ↦ M₁ (↑i : ι)) m i (c • x)) :
            (a : (i : { a : ι // P a }) → M₁ (↑i : ι)) → M₂)
          v :
        M₂)
      ((c • f.domDomRestrict (M₁ := M₁) P (update (β := fun (i : { a : ι // ¬P a }) ↦ M₁ (↑i : ι)) m i x) :
            (a : (i : { a : ι // P a }) → M₁ (↑i : ι)) → M₂)
          v :
        M₂)
⊢ f.domDomRestrict (M₁ := M₁) P (update (β := fun (i : { a : ι // ¬P a }) ↦ M₁ (↑i : ι)) m i (c • x)) =
    c • f.domDomRestrict (M₁ := M₁) P (update (β := fun (i : { a : ι // ¬P a }) ↦ M₁ (↑i : ι)) m i x)

Tactic:
classical
    ext v
    simp [domDomRestrict_aux_right]

Premises used: MultilinearMap.domDomRestrict_aux_right
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
ι : Type u_3
M₁ : ι → Type u_1
α : Type u_2
inst : DecidableEq α
s : Set ι
inst_1 : DecidableEq { x : ι // x ∈ s }
e : Equiv.{u_2 + 1, u_3 + 1} α (↑s : Type u_3)
m : α → (i : ι) → M₁ i
a : α
z : (i : ι) → M₁ i
h :
  ∀ (i : (↑s : Type u_3)),
    update (β := fun (a : α) ↦ (i : ι) → M₁ i) m a z ((e.symm : (a : (↑s : Type u_3)) → α) i) (↑i : ι) =
      update (β := fun (j : (↑s : Type u_3)) ↦ M₁ (↑j : ι))
        (fun (j : (↑s : Type u_3)) ↦ m ((e.symm : (a : (↑s : Type u_3)) → α) j) (↑j : ι))
        ((e : (a : α) → (↑s : Type u_3)) a)
        (z (↑((e : (a : α) → (↑s : Type u_3)) a) : ι) : M₁ (↑((e : (a : α) → (↑s : Type u_3)) a) : ι)) i
⊢ Eq (α := (i : (↑s : Type u_3)) → M₁ (↑i : ι))
    (fun (i : (↑s : Type u_3)) ↦
      update (β := fun (a : α) ↦ (i : ι) → M₁ i) m a z ((e.symm : (a : (↑s : Type u_3)) → α) i) (↑i : ι))
    fun (i : (↑s : Type u_3)) ↦
    update (β := fun (j : (↑s : Type u_3)) ↦ M₁ (↑j : ι))
      (fun (j : (↑s : Type u_3)) ↦ m ((e.symm : (a : (↑s : Type u_3)) → α) j) (↑j : ι))
      ((e : (a : α) → (↑s : Type u_3)) a)
      (z (↑((e : (a : α) → (↑s : Type u_3)) a) : ι) : M₁ (↑((e : (a : α) → (↑s : Type u_3)) a) : ι)) i

Tactic:
ext i
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
ι : Type u_3
M₁ : ι → Type u_1
α : Type u_2
inst : DecidableEq α
s : Set ι
inst_1 : DecidableEq { x : ι // x ∈ s }
e : Equiv.{u_2 + 1, u_3 + 1} α (↑s : Type u_3)
m : α → (i : ι) → M₁ i
a : α
z : (i : ι) → M₁ i
i : (↑s : Type u_3)
h :
  update (β := fun (a : α) ↦ (i : ι) → M₁ i) m ((e.symm : (a : (↑s : Type u_3)) → α) i) z
      ((e.symm : (a : (↑s : Type u_3)) → α) i) (↑i : ι) =
    update (β := fun (j : (↑s : Type u_3)) ↦ M₁ (↑j : ι))
      (fun (j : (↑s : Type u_3)) ↦ m ((e.symm : (a : (↑s : Type u_3)) → α) j) (↑j : ι))
      ((e : (a : α) → (↑s : Type u_3)) ((e.symm : (a : (↑s : Type u_3)) → α) i))
      (z (↑((e : (a : α) → (↑s : Type u_3)) ((e.symm : (a : (↑s : Type u_3)) → α) i)) : ι) :
        M₁ (↑((e : (a : α) → (↑s : Type u_3)) ((e.symm : (a : (↑s : Type u_3)) → α) i)) : ι))
      i
h₁ :
  ∀ (hne : a ≠ (e.symm : (a : (↑s : Type u_3)) → α) i),
    update (β := fun (a : α) ↦ (i : ι) → M₁ i) m a z ((e.symm : (a : (↑s : Type u_3)) → α) i) (↑i : ι) =
      update (β := fun (j : (↑s : Type u_3)) ↦ M₁ (↑j : ι))
        (fun (j : (↑s : Type u_3)) ↦ m ((e.symm : (a : (↑s : Type u_3)) → α) j) (↑j : ι))
        ((e : (a : α) → (↑s : Type u_3)) a)
        (z (↑((e : (a : α) → (↑s : Type u_3)) a) : ι) : M₁ (↑((e : (a : α) → (↑s : Type u_3)) a) : ι)) i
⊢ update (β := fun (a : α) ↦ (i : ι) → M₁ i) m a z ((e.symm : (a : (↑s : Type u_3)) → α) i) (↑i : ι) =
    update (β := fun (j : (↑s : Type u_3)) ↦ M₁ (↑j : ι))
      (fun (j : (↑s : Type u_3)) ↦ m ((e.symm : (a : (↑s : Type u_3)) → α) j) (↑j : ι))
      ((e : (a : α) → (↑s : Type u_3)) a)
      (z (↑((e : (a : α) → (↑s : Type u_3)) a) : ι) : M₁ (↑((e : (a : α) → (↑s : Type u_3)) a) : ι)) i

Tactic:
rcases eq_or_ne a (e.symm i) with rfl | hne

Premises used: eq_or_ne, Equiv.symm, DFunLike.coe, rfl
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
ι : Type u_3
M₁ : ι → Type u_1
α : Type u_2
inst : DecidableEq α
s : Set ι
inst_1 : DecidableEq { x : ι // x ∈ s }
e : Equiv.{u_2 + 1, u_3 + 1} α (↑s : Type u_3)
m : α → (i : ι) → M₁ i
z : (i : ι) → M₁ i
i : (↑s : Type u_3)
h :
  update (β := fun (a : α) ↦ (i : ι) → M₁ i) m ((e.symm : (a : (↑s : Type u_3)) → α) i) z
      ((e.symm : (a : (↑s : Type u_3)) → α) i) (↑i : ι) =
    update (β := fun (j : (↑s : Type u_3)) ↦ M₁ (↑j : ι))
      (fun (j : (↑s : Type u_3)) ↦ m ((e.symm : (a : (↑s : Type u_3)) → α) j) (↑j : ι)) i (z (↑i : ι) : M₁ (↑i : ι)) i
h₁ :
  Eq (α := M₁ (↑i : ι)) (z (↑i : ι))
    (update (β := fun (j : (↑s : Type u_3)) ↦ M₁ (↑j : ι))
      (fun (j : (↑s : Type u_3)) ↦ m ((e.symm : (a : (↑s : Type u_3)) → α) j) (↑j : ι)) i (z (↑i : ι) : M₁ (↑i : ι)) i)
h₂ h₃ : Eq (α := M₁ (↑i : ι)) (z (↑i : ι)) (z (↑i : ι))
⊢ update (β := fun (a : α) ↦ (i : ι) → M₁ i) m ((e.symm : (a : (↑s : Type u_3)) → α) i) z
      ((e.symm : (a : (↑s : Type u_3)) → α) i) (↑i : ι) =
    update (β := fun (j : (↑s : Type u_3)) ↦ M₁ (↑j : ι))
      (fun (j : (↑s : Type u_3)) ↦ m ((e.symm : (a : (↑s : Type u_3)) → α) j) (↑j : ι))
      ((e : (a : α) → (↑s : Type u_3)) ((e.symm : (a : (↑s : Type u_3)) → α) i))
      (z (↑((e : (a : α) → (↑s : Type u_3)) ((e.symm : (a : (↑s : Type u_3)) → α) i)) : ι) :
        M₁ (↑((e : (a : α) → (↑s : Type u_3)) ((e.symm : (a : (↑s : Type u_3)) → α) i)) : ι))
      i

Tactic:
rw [Equiv.apply_symm_apply e i, update_self, update_self]

Premises used: Equiv.apply_symm_apply, Function.update_self
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
ι : Type u_3
M₁ : ι → Type u_1
α : Type u_2
inst : DecidableEq α
s : Set ι
inst_1 : DecidableEq { x : ι // x ∈ s }
e : Equiv.{u_2 + 1, u_3 + 1} α (↑s : Type u_3)
m : α → (i : ι) → M₁ i
a : α
z : (i : ι) → M₁ i
i : (↑s : Type u_3)
hne : a ≠ (e.symm : (a : (↑s : Type u_3)) → α) i
h :
  Eq (α := M₁ (↑i : ι)) (m ((e.symm : (a : (↑s : Type u_3)) → α) i) (↑i : ι))
    (update (β := fun (j : (↑s : Type u_3)) ↦ M₁ (↑j : ι))
      (fun (j : (↑s : Type u_3)) ↦ m ((e.symm : (a : (↑s : Type u_3)) → α) j) (↑j : ι))
      ((e : (a : α) → (↑s : Type u_3)) a)
      (z (↑((e : (a : α) → (↑s : Type u_3)) a) : ι) : M₁ (↑((e : (a : α) → (↑s : Type u_3)) a) : ι)) i)
h₁ h₂ :
  Eq (α := M₁ (↑i : ι)) (m ((e.symm : (a : (↑s : Type u_3)) → α) i) (↑i : ι))
    (m ((e.symm : (a : (↑s : Type u_3)) → α) i) (↑i : ι))
⊢ update (β := fun (a : α) ↦ (i : ι) → M₁ i) m a z ((e.symm : (a : (↑s : Type u_3)) → α) i) (↑i : ι) =
    update (β := fun (j : (↑s : Type u_3)) ↦ M₁ (↑j : ι))
      (fun (j : (↑s : Type u_3)) ↦ m ((e.symm : (a : (↑s : Type u_3)) → α) j) (↑j : ι))
      ((e : (a : α) → (↑s : Type u_3)) a)
      (z (↑((e : (a : α) → (↑s : Type u_3)) a) : ι) : M₁ (↑((e : (a : α) → (↑s : Type u_3)) a) : ι)) i

Tactic:
rw [update_of_ne hne.symm, update_of_ne fun h ↦ (Equiv.symm_apply_apply .. ▸ h ▸ hne) rfl]

Premises used: Ne.symm, Function.update_of_ne
-- 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 : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_3 : AddCommMonoid M₂
inst_4 : (i : Fin n.succ) → Module.{uR, v} R (M i)
inst_5 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_6 : Module R M₂
f_1 f' : MultilinearMap R M₁ M₂
inst_7 : (i : ι) → AddCommMonoid (M₁' i)
inst_8 : (i : ι) → Module.{uR, v₁'} R (M₁' i)
α : Type u_1
f : MultilinearMap R M₁ M₂
s : Set ι
e : Equiv.{u_1 + 1, uι + 1} α (↑s : Type uι)
inst_9 : DecidablePred fun (x : ι) ↦ x ∈ s
z : (i : { a : ι // a ∉ s }) → M₁ (↑i : ι)
⊢ ∀ [inst_10 : DecidableEq α] (m : (i : α) → (i : ι) → M₁ i) (i : α) (x y : (i : ι) → M₁ i),
    ((((f.domDomRestrictₗ (M₁ := M₁) fun (i : ι) ↦ i ∈ s :
                (a : (i : { a : ι // a ∉ s }) → M₁ (↑i : ι)) →
                  MultilinearMap R (fun (i : { a : ι // a ∈ s }) ↦ M₁ (↑i : ι)) M₂)
              z :
            MultilinearMap.{uR, uι, v₁, v₂} R (fun (i : { a : ι // a ∈ s }) ↦ M₁ (↑i : ι)) M₂) :
          (a : (i : { a : ι // a ∈ s }) → M₁ (↑i : ι)) → M₂)
        fun (i_1 : { a : ι // a ∈ s }) ↦
        update (β := fun (x : α) ↦ (i : ι) → M₁ i) m i (x + y) ((e.symm : (a : (↑s : Type uι)) → α) i_1) (↑i_1 : ι)) =
      HAdd.hAdd (α := M₂) (β := M₂)
        ((((f.domDomRestrictₗ (M₁ := M₁) fun (i : ι) ↦ i ∈ s :
                    (a : (i : { a : ι // a ∉ s }) → M₁ (↑i : ι)) →
                      MultilinearMap R (fun (i : { a : ι // a ∈ s }) ↦ M₁ (↑i : ι)) M₂)
                  z :
                MultilinearMap.{uR, uι, v₁, v₂} R (fun (i : { a : ι // a ∈ s }) ↦ M₁ (↑i : ι)) M₂) :
              (a : (i : { a : ι // a ∈ s }) → M₁ (↑i : ι)) → M₂)
            fun (i_1 : { a : ι // a ∈ s }) ↦
            update (β := fun (x : α) ↦ (i : ι) → M₁ i) m i x ((e.symm : (a : (↑s : Type uι)) → α) i_1) (↑i_1 : ι) :
          M₂)
        ((((f.domDomRestrictₗ (M₁ := M₁) fun (i : ι) ↦ i ∈ s :
                    (a : (i : { a : ι // a ∉ s }) → M₁ (↑i : ι)) →
                      MultilinearMap R (fun (i : { a : ι // a ∈ s }) ↦ M₁ (↑i : ι)) M₂)
                  z :
                MultilinearMap.{uR, uι, v₁, v₂} R (fun (i : { a : ι // a ∈ s }) ↦ M₁ (↑i : ι)) M₂) :
              (a : (i : { a : ι // a ∈ s }) → M₁ (↑i : ι)) → M₂)
            fun (i_1 : { a : ι // a ∈ s }) ↦
            update (β := fun (x : α) ↦ (i : ι) → M₁ i) m i y ((e.symm : (a : (↑s : Type uι)) → α) i_1) (↑i_1 : ι) :
          M₂)

Tactic:
simp [iteratedFDeriv_aux]

Premises used: MultilinearMap.iteratedFDeriv_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 : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_3 : AddCommMonoid M₂
inst_4 : (i : Fin n.succ) → Module.{uR, v} R (M i)
inst_5 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_6 : Module R M₂
f_1 f' : MultilinearMap R M₁ M₂
inst_7 : (i : ι) → AddCommMonoid (M₁' i)
inst_8 : (i : ι) → Module.{uR, v₁'} R (M₁' i)
α : Type u_1
f : MultilinearMap R M₁ M₂
s : Set ι
e : Equiv.{u_1 + 1, uι + 1} α (↑s : Type uι)
inst_9 : DecidablePred fun (x : ι) ↦ x ∈ s
z : (i : { a : ι // a ∉ s }) → M₁ (↑i : ι)
⊢ ∀ [inst_10 : DecidableEq α] (m : (i : α) → (i : ι) → M₁ i) (i : α) (x y : (i : ι) → M₁ i),
    ((((f.domDomRestrictₗ (M₁ := M₁) fun (i : ι) ↦ i ∈ s :
                (a : (i : { a : ι // a ∉ s }) → M₁ (↑i : ι)) →
                  MultilinearMap R (fun (i : { a : ι // a ∈ s }) ↦ M₁ (↑i : ι)) M₂)
              z :
            MultilinearMap.{uR, uι, v₁, v₂} R (fun (i : { a : ι // a ∈ s }) ↦ M₁ (↑i : ι)) M₂) :
          (a : (i : { a : ι // a ∈ s }) → M₁ (↑i : ι)) → M₂)
        fun (i_1 : { a : ι // a ∈ s }) ↦
        update (β := fun (x : α) ↦ (i : ι) → M₁ i) m i (x + y) ((e.symm : (a : (↑s : Type uι)) → α) i_1) (↑i_1 : ι)) =
      HAdd.hAdd (α := M₂) (β := M₂)
        ((((f.domDomRestrictₗ (M₁ := M₁) fun (i : ι) ↦ i ∈ s :
                    (a : (i : { a : ι // a ∉ s }) → M₁ (↑i : ι)) →
                      MultilinearMap R (fun (i : { a : ι // a ∈ s }) ↦ M₁ (↑i : ι)) M₂)
                  z :
                MultilinearMap.{uR, uι, v₁, v₂} R (fun (i : { a : ι // a ∈ s }) ↦ M₁ (↑i : ι)) M₂) :
              (a : (i : { a : ι // a ∈ s }) → M₁ (↑i : ι)) → M₂)
            fun (i_1 : { a : ι // a ∈ s }) ↦
            update (β := fun (x : α) ↦ (i : ι) → M₁ i) m i x ((e.symm : (a : (↑s : Type uι)) → α) i_1) (↑i_1 : ι) :
          M₂)
        ((((f.domDomRestrictₗ (M₁ := M₁) fun (i : ι) ↦ i ∈ s :
                    (a : (i : { a : ι // a ∉ s }) → M₁ (↑i : ι)) →
                      MultilinearMap R (fun (i : { a : ι // a ∈ s }) ↦ M₁ (↑i : ι)) M₂)
                  z :
                MultilinearMap.{uR, uι, v₁, v₂} R (fun (i : { a : ι // a ∈ s }) ↦ M₁ (↑i : ι)) M₂) :
              (a : (i : { a : ι // a ∈ s }) → M₁ (↑i : ι)) → M₂)
            fun (i_1 : { a : ι // a ∈ s }) ↦
            update (β := fun (x : α) ↦ (i : ι) → M₁ i) m i y ((e.symm : (a : (↑s : Type uι)) → α) i_1) (↑i_1 : ι) :
          M₂)

Tactic:
classical simp [iteratedFDeriv_aux]

Premises used: MultilinearMap.iteratedFDeriv_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 : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_3 : AddCommMonoid M₂
inst_4 : (i : Fin n.succ) → Module.{uR, v} R (M i)
inst_5 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_6 : Module R M₂
f_1 f' : MultilinearMap R M₁ M₂
inst_7 : (i : ι) → AddCommMonoid (M₁' i)
inst_8 : (i : ι) → Module.{uR, v₁'} R (M₁' i)
α : Type u_1
f : MultilinearMap R M₁ M₂
s : Set ι
e : Equiv.{u_1 + 1, uι + 1} α (↑s : Type uι)
inst_9 : DecidablePred fun (x : ι) ↦ x ∈ s
z : (i : { a : ι // a ∉ s }) → M₁ (↑i : ι)
⊢ ∀ [inst_10 : DecidableEq α] (m : (i : α) → (i : ι) → M₁ i) (i : α) (c : R) (x : (i : ι) → M₁ i),
    ((((f.domDomRestrictₗ (M₁ := M₁) fun (i : ι) ↦ i ∈ s :
                (a : (i : { a : ι // a ∉ s }) → M₁ (↑i : ι)) →
                  MultilinearMap R (fun (i : { a : ι // a ∈ s }) ↦ M₁ (↑i : ι)) M₂)
              z :
            MultilinearMap.{uR, uι, v₁, v₂} R (fun (i : { a : ι // a ∈ s }) ↦ M₁ (↑i : ι)) M₂) :
          (a : (i : { a : ι // a ∈ s }) → M₁ (↑i : ι)) → M₂)
        fun (i_1 : { a : ι // a ∈ s }) ↦
        update (β := fun (x : α) ↦ (i : ι) → M₁ i) m i (c • x) ((e.symm : (a : (↑s : Type uι)) → α) i_1) (↑i_1 : ι)) =
      HSMul.hSMul (β := M₂) c
        ((((f.domDomRestrictₗ (M₁ := M₁) fun (i : ι) ↦ i ∈ s :
                    (a : (i : { a : ι // a ∉ s }) → M₁ (↑i : ι)) →
                      MultilinearMap R (fun (i : { a : ι // a ∈ s }) ↦ M₁ (↑i : ι)) M₂)
                  z :
                MultilinearMap.{uR, uι, v₁, v₂} R (fun (i : { a : ι // a ∈ s }) ↦ M₁ (↑i : ι)) M₂) :
              (a : (i : { a : ι // a ∈ s }) → M₁ (↑i : ι)) → M₂)
            fun (i_1 : { a : ι // a ∈ s }) ↦
            update (β := fun (x : α) ↦ (i : ι) → M₁ i) m i x ((e.symm : (a : (↑s : Type uι)) → α) i_1) (↑i_1 : ι) :
          M₂)

Tactic:
simp [iteratedFDeriv_aux]

Premises used: MultilinearMap.iteratedFDeriv_aux