awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
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
⊢ ((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₃)
have 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₃)
Tactic: rw [m.map_update_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
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₃
⊢ domDomCongr σ.symm (domDomCongr σ m) = m
have 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₃)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
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₃
⊢ domDomCongr σ (domDomCongr σ.symm m) = m
have 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₃)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
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₃
⊢ domDomCongr σ (a + b) = domDomCongr σ a + domDomCongr σ b
have 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₃)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
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 : ι)
⊢ ((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₂)
have 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₂)
Tactic: rw [domDomRestrict_aux]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
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 : ι)
⊢ (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₂)
have 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₂)
Tactic: rw [domDomRestrict_aux]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
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 : ι)
⊢ (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₂)
have 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₂)
Tactic: rw [domDomRestrict_aux]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
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 : ι)
⊢ ((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₂)
have repeat : (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₂)
Tactic: repeat (rw [domDomRestrict_aux])
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
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 : ι)
⊢ ((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₂)
have repeat : (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: classical
    repeat (rw [domDomRestrict_aux])
    simp only [MultilinearMap.map_update_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
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_1 : (i : { a : ι // ¬P a }) → M₁ (↑i : ι)
inst_12 : DecidableEq { a : ι // P a }
z : (i : { a : ι // P a }) → M₁ (↑i : ι)
i : { a : ι // P a }
c : R
a : M₁ (↑i : ι)
⊢ ((f : (a : (i : ι) → M₁ i) → M₂) fun (j : ι) ↦
      if h : P j then
        update (β := fun (i : { a : ι // P a }) ↦ M₁ (↑i : ι)) z i (c • a) (Subtype.mk (p := fun (a : ι) ↦ P a) j h)
      else z_1 (Subtype.mk (p := fun (a : ι) ↦ ¬P a) j h)) =
    HSMul.hSMul (β := M₂) c
      ((f : (a : (i : ι) → M₁ i) → M₂) fun (j : ι) ↦
          if h : P j then
            update (β := fun (i : { a : ι // P a }) ↦ M₁ (↑i : ι)) z i a (Subtype.mk (p := fun (a : ι) ↦ P a) j h)
          else z_1 (Subtype.mk (p := fun (a : ι) ↦ ¬P a) j h) :
        M₂)
have rw : (f : (a : (i : ι) → M₁ i) → M₂)
    (update (β := M₁)
      (fun (j : ι) ↦
        if h : P j then z (Subtype.mk (p := fun (a : ι) ↦ P a) j h) else z_1 (Subtype.mk (p := fun (a : ι) ↦ ¬P a) j h))
      (↑i : ι) (c • a)) =
  HSMul.hSMul (β := M₂) c
    ((f : (a : (i : ι) → M₁ i) → M₂) fun (j : ι) ↦
        if h : P j then
          update (β := fun (i : { a : ι // P a }) ↦ M₁ (↑i : ι)) z i a (Subtype.mk (p := fun (a : ι) ↦ P a) j h)
        else z_1 (Subtype.mk (p := fun (a : ι) ↦ ¬P a) j h) :
      M₂)
Tactic: rw [domDomRestrict_aux]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
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_1 : (i : { a : ι // ¬P a }) → M₁ (↑i : ι)
inst_12 : DecidableEq { a : ι // P a }
z : (i : { a : ι // P a }) → M₁ (↑i : ι)
i : { a : ι // P a }
c : R
a : M₁ (↑i : ι)
⊢ (f : (a : (i : ι) → M₁ i) → M₂)
      (update (β := M₁)
        (fun (j : ι) ↦
          if h : P j then z (Subtype.mk (p := fun (a : ι) ↦ P a) j h)
          else z_1 (Subtype.mk (p := fun (a : ι) ↦ ¬P a) j h))
        (↑i : ι) (c • a)) =
    HSMul.hSMul (β := M₂) c
      ((f : (a : (i : ι) → M₁ i) → M₂) fun (j : ι) ↦
          if h : P j then
            update (β := fun (i : { a : ι // P a }) ↦ M₁ (↑i : ι)) z i a (Subtype.mk (p := fun (a : ι) ↦ P a) j h)
          else z_1 (Subtype.mk (p := fun (a : ι) ↦ ¬P a) j h) :
        M₂)
have rw : (f : (a : (i : ι) → M₁ i) → M₂)
    (update (β := M₁)
      (fun (j : ι) ↦
        if h : P j then z (Subtype.mk (p := fun (a : ι) ↦ P a) j h) else z_1 (Subtype.mk (p := fun (a : ι) ↦ ¬P a) j h))
      (↑i : ι) (c • a)) =
  HSMul.hSMul (β := M₂) c
    ((f : (a : (i : ι) → M₁ i) → M₂)
        (update (β := M₁)
          (fun (j : ι) ↦
            if h : P j then z (Subtype.mk (p := fun (a : ι) ↦ P a) j h)
            else z_1 (Subtype.mk (p := fun (a : ι) ↦ ¬P a) j h))
          (↑i : ι) a) :
      M₂)
Tactic: rw [domDomRestrict_aux]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
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_1 : (i : { a : ι // ¬P a }) → M₁ (↑i : ι)
inst_12 : DecidableEq { a : ι // P a }
z : (i : { a : ι // P a }) → M₁ (↑i : ι)
i : { a : ι // P a }
c : R
a : M₁ (↑i : ι)
⊢ ((f : (a : (i : ι) → M₁ i) → M₂) fun (j : ι) ↦
      if h : P j then
        update (β := fun (i : { a : ι // P a }) ↦ M₁ (↑i : ι)) z i (c • a) (Subtype.mk (p := fun (a : ι) ↦ P a) j h)
      else z_1 (Subtype.mk (p := fun (a : ι) ↦ ¬P a) j h)) =
    HSMul.hSMul (β := M₂) c
      ((f : (a : (i : ι) → M₁ i) → M₂) fun (j : ι) ↦
          if h : P j then
            update (β := fun (i : { a : ι // P a }) ↦ M₁ (↑i : ι)) z i a (Subtype.mk (p := fun (a : ι) ↦ P a) j h)
          else z_1 (Subtype.mk (p := fun (a : ι) ↦ ¬P a) j h) :
        M₂)
have repeat : (f : (a : (i : ι) → M₁ i) → M₂)
    (update (β := M₁)
      (fun (j : ι) ↦
        if h : P j then z (Subtype.mk (p := fun (a : ι) ↦ P a) j h) else z_1 (Subtype.mk (p := fun (a : ι) ↦ ¬P a) j h))
      (↑i : ι) (c • a)) =
  HSMul.hSMul (β := M₂) c
    ((f : (a : (i : ι) → M₁ i) → M₂)
        (update (β := M₁)
          (fun (j : ι) ↦
            if h : P j then z (Subtype.mk (p := fun (a : ι) ↦ P a) j h)
            else z_1 (Subtype.mk (p := fun (a : ι) ↦ ¬P a) j h))
          (↑i : ι) a) :
      M₂)
Tactic: repeat (rw [domDomRestrict_aux])