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_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₂) 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: classical
    repeat (rw [domDomRestrict_aux])
    simp only [MultilinearMap.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_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 : ι)
repeat repeat₁ 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₂) 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₂)
⊢ ((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: classical
    repeat (rw [domDomRestrict_aux])
    simp only [MultilinearMap.map_update_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
Goal:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : AddCommMonoid M₂
inst_3 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_4 : Module R M₂
inst_5 : DecidableEq ι
inst_6 : Fintype ι
f : MultilinearMap R M₁ M₂
x y : (i : ι) → M₁ i
⊢ Eq.{v₂ + 1} (α := M₂) ((f.linearDeriv (M₁ := M₁) x : (a : (i : ι) → M₁ i) → M₂) y : M₂)
    (∑ i : ι, (f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) x i (y i)) : M₂)
have unfold : Eq.{v₂ + 1} (α := M₂)
  ((∑ i : ι, f.toLinearMap (M₁ := M₁) x i ∘ₗ LinearMap.proj (φ := M₁) i : (a : (i : ι) → M₁ i) → M₂) y : M₂)
  (∑ i : ι, (f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) x i (y i)) : M₂)
Tactic: unfold linearDeriv
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
Goal:
R : Type uR
M₂ : Type v₂
M₃ : Type v₃
M' : Type v'
inst : Semiring R
inst_1 : AddCommMonoid M₂
inst_2 : AddCommMonoid M₃
inst_3 : AddCommMonoid M'
inst_4 : Module R M₂
inst_5 : Module R M₃
inst_6 : Module R M'
ι₁ : Type u_1
ι₂ : Type u_2
σ : ι₁ ≃ ι₂
g : M₂ →ₗ[R] M₃
f : MultilinearMap.{uR, u_1, v', v₂} R (fun (x : ι₁) ↦ M') M₂
⊢ MultilinearMap.domDomCongr σ (g.compMultilinearMap (M₁ := fun (x : ι₁) ↦ M') f) =
    g.compMultilinearMap (M₁ := fun (x : ι₂) ↦ M') (MultilinearMap.domDomCongr σ f)
have H : ∀ (x : (i : ι₂) → M'),
  Eq.{v₃ + 1} (α := M₃)
    ((MultilinearMap.domDomCongr σ (g.compMultilinearMap (M₁ := fun (x : ι₁) ↦ M') f) : (a : (i : ι₂) → M') → M₃) x :
      M₃)
    ((g.compMultilinearMap (M₁ := fun (x : ι₂) ↦ M') (MultilinearMap.domDomCongr σ f) : (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 : ι) → AddCommMonoid (M₁ i)
inst_2 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_3 : AddCommMonoid M₂
inst_4 : Module R M₂
inst_5 : Semiring S
inst_6 : Module S M₂
inst_7 : SMulCommClass R S M₂
inst_8 : AddCommMonoid M₃
inst_9 : Module S M₃
inst_10 : Module R M₃
inst_11 : SMulCommClass R S M₃
inst_12 : LinearMap.CompatibleSMul M₂ M₃ S R
inst_13 : LinearMap.CompatibleSMul M₃ M₂ S R
g : M₂ ≃ₗ[R] M₃
x : MultilinearMap R M₁ M₂
⊢ (LinearMap.compMultilinearMapₗ S (M₁ := M₁) (↑g.symm : M₃ →ₗ[R] M₂) :
        (a : MultilinearMap R M₁ M₃) → MultilinearMap R M₁ M₂)
      (AddHom.toFun (LinearMap.toAddHom (LinearMap.compMultilinearMapₗ S (M₁ := M₁) (↑g : M₂ →ₗ[R] M₃))) x) =
    x
have H : ∀ (x_1 : (i : ι) → M₁ i),
  Eq.{v₂ + 1} (α := M₂)
    ((((LinearMap.compMultilinearMapₗ S (M₁ := M₁) (↑g.symm : M₃ →ₗ[R] M₂) :
                (a : MultilinearMap R M₁ M₃) → MultilinearMap R M₁ M₂)
              (AddHom.toFun (LinearMap.toAddHom (LinearMap.compMultilinearMapₗ S (M₁ := M₁) (↑g : M₂ →ₗ[R] M₃))) x) :
            MultilinearMap R M₁ M₂) :
          (a : (i : ι) → M₁ i) → M₂)
        x_1 :
      M₂)
    ((x : (a : (i : ι) → M₁ i) → M₂) x_1 : 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 : ι) → AddCommMonoid (M₁ i)
inst_2 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_3 : AddCommMonoid M₂
inst_4 : Module R M₂
inst_5 : Semiring S
inst_6 : Module S M₂
inst_7 : SMulCommClass R S M₂
inst_8 : AddCommMonoid M₃
inst_9 : Module S M₃
inst_10 : Module R M₃
inst_11 : SMulCommClass R S M₃
inst_12 : LinearMap.CompatibleSMul M₂ M₃ S R
inst_13 : LinearMap.CompatibleSMul M₃ M₂ S R
g : M₂ ≃ₗ[R] M₃
x : MultilinearMap R M₁ M₃
⊢ AddHom.toFun (LinearMap.toAddHom (LinearMap.compMultilinearMapₗ S (M₁ := M₁) (↑g : M₂ →ₗ[R] M₃)))
      ((LinearMap.compMultilinearMapₗ S (M₁ := M₁) (↑g.symm : M₃ →ₗ[R] M₂) :
          (a : MultilinearMap R M₁ M₃) → MultilinearMap R M₁ M₂)
        x) =
    x
have H : ∀ (x_1 : (i : ι) → M₁ i),
  Eq.{v₃ + 1} (α := M₃)
    ((AddHom.toFun (LinearMap.toAddHom (LinearMap.compMultilinearMapₗ S (M₁ := M₁) (↑g : M₂ →ₗ[R] M₃)))
            ((LinearMap.compMultilinearMapₗ S (M₁ := M₁) (↑g.symm : M₃ →ₗ[R] M₂) :
                (a : MultilinearMap R M₁ M₃) → MultilinearMap R M₁ M₂)
              x) :
          (a : (i : ι) → M₁ i) → M₃)
        x_1 :
      M₃)
    ((x : (a : (i : ι) → M₁ i) → M₃) x_1 : 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 : ι) → AddCommMonoid (M₁ i)
inst_2 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_3 : AddCommMonoid M₂
inst_4 : Module R M₂
inst_5 : Semiring S
inst_6 : Module S M₂
inst_7 : SMulCommClass R S M₂
inst_8 : AddCommMonoid M₃
inst_9 : Module S M₃
inst_10 : Module R M₃
inst_11 : SMulCommClass R S M₃
ι' : Type u_1
σ : ι ≃ ι'
f : MultilinearMap R M₁ M₂
inst_12 : DecidableEq ι'
m : (i : ι') → M₁ ((σ.symm : (a : ι') → ι) i)
i : ι'
this : DecidableEq ι := σ.decidableEq
⊢ ∀ (x y : M₁ ((σ.symm : (a : ι') → ι) i)),
    comp (β := (i : ι) → M₁ i) (⇑f : (a : (i : ι) → M₁ i) → M₂)
        (⇑(Equiv.piCongrLeft' M₁ σ).symm : (a : (b : ι') → M₁ ((σ.symm : (a : ι') → ι) b)) → (a : ι) → M₁ a)
        (update (β := fun (i : ι') ↦ M₁ ((σ.symm : (a : ι') → ι) i)) m i (x + y)) =
      HAdd.hAdd (α := M₂)
        (comp (β := (i : ι) → M₁ i) (⇑f : (a : (i : ι) → M₁ i) → M₂)
          (⇑(Equiv.piCongrLeft' M₁ σ).symm : (a : (b : ι') → M₁ ((σ.symm : (a : ι') → ι) b)) → (a : ι) → M₁ a)
          (update (β := fun (i : ι') ↦ M₁ ((σ.symm : (a : ι') → ι) i)) m i x))
        (comp (β := (i : ι) → M₁ i) (⇑f : (a : (i : ι) → M₁ i) → M₂)
          (⇑(Equiv.piCongrLeft' M₁ σ).symm : (a : (b : ι') → M₁ ((σ.symm : (a : ι') → ι) b)) → (a : ι) → M₁ a)
          (update (β := fun (i : ι') ↦ M₁ ((σ.symm : (a : ι') → ι) i)) m i y))
have rw : ∀ (x y : M₁ ((σ.symm : (a : ι') → ι) ((σ : (a : ι) → ι') ((σ.symm : (a : ι') → ι) i : ι) : ι'))),
  comp (β := (i : ι) → M₁ i) (⇑f : (a : (i : ι) → M₁ i) → M₂)
      (⇑(Equiv.piCongrLeft' M₁ σ).symm : (a : (b : ι') → M₁ ((σ.symm : (a : ι') → ι) b)) → (a : ι) → M₁ a)
      (update (β := fun (i : ι') ↦ M₁ ((σ.symm : (a : ι') → ι) i)) m
        ((σ : (a : ι) → ι') ((σ.symm : (a : ι') → ι) i : ι)) (x + y)) =
    HAdd.hAdd (α := M₂)
      (comp (β := (i : ι) → M₁ i) (⇑f : (a : (i : ι) → M₁ i) → M₂)
        (⇑(Equiv.piCongrLeft' M₁ σ).symm : (a : (b : ι') → M₁ ((σ.symm : (a : ι') → ι) b)) → (a : ι) → M₁ a)
        (update (β := fun (i : ι') ↦ M₁ ((σ.symm : (a : ι') → ι) i)) m
          ((σ : (a : ι) → ι') ((σ.symm : (a : ι') → ι) i : ι)) x))
      (comp (β := (i : ι) → M₁ i) (⇑f : (a : (i : ι) → M₁ i) → M₂)
        (⇑(Equiv.piCongrLeft' M₁ σ).symm : (a : (b : ι') → M₁ ((σ.symm : (a : ι') → ι) b)) → (a : ι) → M₁ a)
        (update (β := fun (i : ι') ↦ M₁ ((σ.symm : (a : ι') → ι) i)) m
          ((σ : (a : ι) → ι') ((σ.symm : (a : ι') → ι) i : ι)) y))
Tactic: rw [← σ.apply_symm_apply i]
-- 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 : ι) → AddCommMonoid (M₁ i)
inst_2 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_3 : AddCommMonoid M₂
inst_4 : Module R M₂
inst_5 : Semiring S
inst_6 : Module S M₂
inst_7 : SMulCommClass R S M₂
inst_8 : AddCommMonoid M₃
inst_9 : Module S M₃
inst_10 : Module R M₃
inst_11 : SMulCommClass R S M₃
ι' : Type u_1
σ : ι ≃ ι'
f : MultilinearMap R M₁ M₂
inst_12 : DecidableEq ι'
m : (i : ι') → M₁ ((σ.symm : (a : ι') → ι) i)
i : ι'
c : R
this : DecidableEq ι := σ.decidableEq
⊢ ∀ (x : M₁ ((σ.symm : (a : ι') → ι) i)),
    comp (β := (i : ι) → M₁ i) (⇑f : (a : (i : ι) → M₁ i) → M₂)
        (⇑(Equiv.piCongrLeft' M₁ σ).symm : (a : (b : ι') → M₁ ((σ.symm : (a : ι') → ι) b)) → (a : ι) → M₁ a)
        (update (β := fun (i : ι') ↦ M₁ ((σ.symm : (a : ι') → ι) i)) m i (c • x)) =
      HSMul.hSMul (β := M₂) c
        (comp (β := (i : ι) → M₁ i) (⇑f : (a : (i : ι) → M₁ i) → M₂)
          (⇑(Equiv.piCongrLeft' M₁ σ).symm : (a : (b : ι') → M₁ ((σ.symm : (a : ι') → ι) b)) → (a : ι) → M₁ a)
          (update (β := fun (i : ι') ↦ M₁ ((σ.symm : (a : ι') → ι) i)) m i x))
have rw : ∀ (x : M₁ ((σ.symm : (a : ι') → ι) ((σ : (a : ι) → ι') ((σ.symm : (a : ι') → ι) i : ι) : ι'))),
  comp (β := (i : ι) → M₁ i) (⇑f : (a : (i : ι) → M₁ i) → M₂)
      (⇑(Equiv.piCongrLeft' M₁ σ).symm : (a : (b : ι') → M₁ ((σ.symm : (a : ι') → ι) b)) → (a : ι) → M₁ a)
      (update (β := fun (i : ι') ↦ M₁ ((σ.symm : (a : ι') → ι) i)) m
        ((σ : (a : ι) → ι') ((σ.symm : (a : ι') → ι) i : ι)) (c • x)) =
    HSMul.hSMul (β := M₂) c
      (comp (β := (i : ι) → M₁ i) (⇑f : (a : (i : ι) → M₁ i) → M₂)
        (⇑(Equiv.piCongrLeft' M₁ σ).symm : (a : (b : ι') → M₁ ((σ.symm : (a : ι') → ι) b)) → (a : ι) → M₁ a)
        (update (β := fun (i : ι') ↦ M₁ ((σ.symm : (a : ι') → ι) i)) m
          ((σ : (a : ι) → ι') ((σ.symm : (a : ι') → ι) i : ι)) x))
Tactic: rw [← σ.apply_symm_apply i]
-- 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 : ι) → AddCommMonoid (M₁ i)
inst_2 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_3 : AddCommMonoid M₂
inst_4 : Module R M₂
inst_5 : Semiring S
inst_6 : Module S M₂
inst_7 : SMulCommClass R S M₂
inst_8 : AddCommMonoid M₃
inst_9 : Module S M₃
inst_10 : Module R M₃
inst_11 : SMulCommClass R S M₃
ι' : Type u_1
σ : ι ≃ ι'
f₁ f₂ : MultilinearMap R M₁ M₂
⊢ mk (M₁ := fun (i : ι') ↦ M₁ ((σ.symm : (a : ι') → ι) i))
      (comp (β := (i : ι) → M₁ i) (⇑(f₁ + f₂) : (a : (i : ι) → M₁ i) → M₂)
        (⇑(Equiv.piCongrLeft' M₁ σ).symm : (a : (b : ι') → M₁ ((σ.symm : (a : ι') → ι) b)) → (a : ι) → M₁ a))
      ⋯ ⋯ =
    HAdd.hAdd (α := MultilinearMap.{uR, u_1, v₁, v₂} R (fun (i : ι') ↦ M₁ ((σ.symm : (a : ι') → ι) i)) M₂)
      (mk (M₁ := fun (i : ι') ↦ M₁ ((σ.symm : (a : ι') → ι) i))
        (comp (β := (i : ι) → M₁ i) (⇑f₁ : (a : (i : ι) → M₁ i) → M₂)
          (⇑(Equiv.piCongrLeft' M₁ σ).symm : (a : (b : ι') → M₁ ((σ.symm : (a : ι') → ι) b)) → (a : ι) → M₁ a))
        ⋯ ⋯)
      (mk (M₁ := fun (i : ι') ↦ M₁ ((σ.symm : (a : ι') → ι) i))
        (comp (β := (i : ι) → M₁ i) (⇑f₂ : (a : (i : ι) → M₁ i) → M₂)
          (⇑(Equiv.piCongrLeft' M₁ σ).symm : (a : (b : ι') → M₁ ((σ.symm : (a : ι') → ι) b)) → (a : ι) → M₁ a))
        ⋯ ⋯)
have H : ∀ (x : (i : ι') → M₁ ((σ.symm : (a : ι') → ι) i)),
  Eq.{v₂ + 1} (α := M₂)
    ((mk (M₁ := fun (i : ι') ↦ M₁ ((σ.symm : (a : ι') → ι) i))
            (comp (β := (i : ι) → M₁ i) (⇑(f₁ + f₂) : (a : (i : ι) → M₁ i) → M₂)
              (⇑(Equiv.piCongrLeft' M₁ σ).symm : (a : (b : ι') → M₁ ((σ.symm : (a : ι') → ι) b)) → (a : ι) → M₁ a))
            sorry sorry :
          (a : (i : ι') → M₁ ((σ.symm : (a : ι') → ι) i)) → M₂)
        x :
      M₂)
    ((HAdd.hAdd (α := MultilinearMap.{uR, u_1, v₁, v₂} R (fun (i : ι') ↦ M₁ ((σ.symm : (a : ι') → ι) i)) M₂)
            (mk (M₁ := fun (i : ι') ↦ M₁ ((σ.symm : (a : ι') → ι) i))
              (comp (β := (i : ι) → M₁ i) (⇑f₁ : (a : (i : ι) → M₁ i) → M₂)
                (⇑(Equiv.piCongrLeft' M₁ σ).symm : (a : (b : ι') → M₁ ((σ.symm : (a : ι') → ι) b)) → (a : ι) → M₁ a))
              sorry sorry)
            (mk (M₁ := fun (i : ι') ↦ M₁ ((σ.symm : (a : ι') → ι) i))
              (comp (β := (i : ι) → M₁ i) (⇑f₂ : (a : (i : ι) → M₁ i) → M₂)
                (⇑(Equiv.piCongrLeft' M₁ σ).symm : (a : (b : ι') → M₁ ((σ.symm : (a : ι') → ι) b)) → (a : ι) → M₁ a))
              sorry sorry) :
          (a : (i : ι') → M₁ ((σ.symm : (a : ι') → ι) i)) → 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 : ι) → AddCommMonoid (M₁ i)
inst_2 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_3 : AddCommMonoid M₂
inst_4 : Module R M₂
inst_5 : Semiring S
inst_6 : Module S M₂
inst_7 : SMulCommClass R S M₂
inst_8 : AddCommMonoid M₃
inst_9 : Module S M₃
inst_10 : Module R M₃
inst_11 : SMulCommClass R S M₃
ι' : Type u_1
σ : ι ≃ ι'
c : S
f : MultilinearMap R M₁ M₂
⊢ mk (M₁ := fun (i : ι') ↦ M₁ ((σ.symm : (a : ι') → ι) i))
      (comp (β := (i : ι) → M₁ i) (⇑(c • f) : (a : (i : ι) → M₁ i) → M₂)
        (⇑(Equiv.piCongrLeft' M₁ σ).symm : (a : (b : ι') → M₁ ((σ.symm : (a : ι') → ι) b)) → (a : ι) → M₁ a))
      ⋯ ⋯ =
    HSMul.hSMul (α := S) (β := MultilinearMap.{uR, u_1, v₁, v₂} R (fun (i : ι') ↦ M₁ ((σ.symm : (a : ι') → ι) i)) M₂)
      ((RingHom.id S : (a : S) → S) c : S)
      (mk (M₁ := fun (i : ι') ↦ M₁ ((σ.symm : (a : ι') → ι) i))
        (comp (β := (i : ι) → M₁ i) (⇑f : (a : (i : ι) → M₁ i) → M₂)
          (⇑(Equiv.piCongrLeft' M₁ σ).symm : (a : (b : ι') → M₁ ((σ.symm : (a : ι') → ι) b)) → (a : ι) → M₁ a))
        ⋯ ⋯)
have H : ∀ (x : (i : ι') → M₁ ((σ.symm : (a : ι') → ι) i)),
  Eq.{v₂ + 1} (α := M₂)
    ((mk (M₁ := fun (i : ι') ↦ M₁ ((σ.symm : (a : ι') → ι) i))
            (comp (β := (i : ι) → M₁ i) (⇑(c • f) : (a : (i : ι) → M₁ i) → M₂)
              (⇑(Equiv.piCongrLeft' M₁ σ).symm : (a : (b : ι') → M₁ ((σ.symm : (a : ι') → ι) b)) → (a : ι) → M₁ a))
            sorry sorry :
          (a : (i : ι') → M₁ ((σ.symm : (a : ι') → ι) i)) → M₂)
        x :
      M₂)
    ((HSMul.hSMul (α := S) (β := MultilinearMap.{uR, u_1, v₁, v₂} R (fun (i : ι') ↦ M₁ ((σ.symm : (a : ι') → ι) i)) M₂)
            ((RingHom.id S : (a : S) → S) c : S)
            (mk (M₁ := fun (i : ι') ↦ M₁ ((σ.symm : (a : ι') → ι) i))
              (comp (β := (i : ι) → M₁ i) (⇑f : (a : (i : ι) → M₁ i) → M₂)
                (⇑(Equiv.piCongrLeft' M₁ σ).symm : (a : (b : ι') → M₁ ((σ.symm : (a : ι') → ι) b)) → (a : ι) → M₁ a))
              sorry sorry) :
          (a : (i : ι') → M₁ ((σ.symm : (a : ι') → ι) i)) → 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 : ι) → AddCommMonoid (M₁ i)
inst_2 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_3 : AddCommMonoid M₂
inst_4 : Module R M₂
inst_5 : Semiring S
inst_6 : Module S M₂
inst_7 : SMulCommClass R S M₂
inst_8 : AddCommMonoid M₃
inst_9 : Module S M₃
inst_10 : Module R M₃
inst_11 : SMulCommClass R S M₃
ι' : Type u_1
σ : ι ≃ ι'
f : MultilinearMap.{uR, u_1, v₁, v₂} R (fun (i : ι') ↦ M₁ ((σ.symm : (a : ι') → ι) i)) M₂
inst_12 : DecidableEq ι
m : (i : ι) → M₁ i
i : ι
this : DecidableEq ι' := σ.symm.decidableEq
⊢ ∀ (x y : M₁ i),
    comp (β := (i : ι') → M₁ ((σ.symm : (a : ι') → ι) i)) (⇑f : (a : (i : ι') → M₁ ((σ.symm : (a : ι') → ι) i)) → M₂)
        (⇑(Equiv.piCongrLeft' M₁ σ) : (a : (a : ι) → M₁ a) → (b : ι') → M₁ ((σ.symm : (a : ι') → ι) b))
        (update (β := M₁) m i (x + y)) =
      HAdd.hAdd (α := M₂)
        (comp (β := (i : ι') → M₁ ((σ.symm : (a : ι') → ι) i))
          (⇑f : (a : (i : ι') → M₁ ((σ.symm : (a : ι') → ι) i)) → M₂)
          (⇑(Equiv.piCongrLeft' M₁ σ) : (a : (a : ι) → M₁ a) → (b : ι') → M₁ ((σ.symm : (a : ι') → ι) b))
          (update (β := M₁) m i x))
        (comp (β := (i : ι') → M₁ ((σ.symm : (a : ι') → ι) i))
          (⇑f : (a : (i : ι') → M₁ ((σ.symm : (a : ι') → ι) i)) → M₂)
          (⇑(Equiv.piCongrLeft' M₁ σ) : (a : (a : ι) → M₁ a) → (b : ι') → M₁ ((σ.symm : (a : ι') → ι) b))
          (update (β := M₁) m i y))
have rw : ∀ (x y : M₁ ((σ.symm : (a : ι') → ι) ((σ : (a : ι) → ι') i : ι'))),
  comp (β := (i : ι') → M₁ ((σ.symm : (a : ι') → ι) i)) (⇑f : (a : (i : ι') → M₁ ((σ.symm : (a : ι') → ι) i)) → M₂)
      (⇑(Equiv.piCongrLeft' M₁ σ) : (a : (a : ι) → M₁ a) → (b : ι') → M₁ ((σ.symm : (a : ι') → ι) b))
      (update (β := M₁) m ((σ.symm : (a : ι') → ι) ((σ : (a : ι) → ι') i : ι')) (x + y)) =
    HAdd.hAdd (α := M₂)
      (comp (β := (i : ι') → M₁ ((σ.symm : (a : ι') → ι) i)) (⇑f : (a : (i : ι') → M₁ ((σ.symm : (a : ι') → ι) i)) → M₂)
        (⇑(Equiv.piCongrLeft' M₁ σ) : (a : (a : ι) → M₁ a) → (b : ι') → M₁ ((σ.symm : (a : ι') → ι) b))
        (update (β := M₁) m ((σ.symm : (a : ι') → ι) ((σ : (a : ι) → ι') i : ι')) x))
      (comp (β := (i : ι') → M₁ ((σ.symm : (a : ι') → ι) i)) (⇑f : (a : (i : ι') → M₁ ((σ.symm : (a : ι') → ι) i)) → M₂)
        (⇑(Equiv.piCongrLeft' M₁ σ) : (a : (a : ι) → M₁ a) → (b : ι') → M₁ ((σ.symm : (a : ι') → ι) b))
        (update (β := M₁) m ((σ.symm : (a : ι') → ι) ((σ : (a : ι) → ι') i : ι')) y))
Tactic: rw [← σ.symm_apply_apply i]
-- 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 : ι) → AddCommMonoid (M₁ i)
inst_2 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_3 : AddCommMonoid M₂
inst_4 : Module R M₂
inst_5 : Semiring S
inst_6 : Module S M₂
inst_7 : SMulCommClass R S M₂
inst_8 : AddCommMonoid M₃
inst_9 : Module S M₃
inst_10 : Module R M₃
inst_11 : SMulCommClass R S M₃
ι' : Type u_1
σ : ι ≃ ι'
f : MultilinearMap.{uR, u_1, v₁, v₂} R (fun (i : ι') ↦ M₁ ((σ.symm : (a : ι') → ι) i)) M₂
inst_12 : DecidableEq ι
m : (i : ι) → M₁ i
i : ι
c : R
this : DecidableEq ι' := σ.symm.decidableEq
⊢ ∀ (x : M₁ i),
    comp (β := (i : ι') → M₁ ((σ.symm : (a : ι') → ι) i)) (⇑f : (a : (i : ι') → M₁ ((σ.symm : (a : ι') → ι) i)) → M₂)
        (⇑(Equiv.piCongrLeft' M₁ σ) : (a : (a : ι) → M₁ a) → (b : ι') → M₁ ((σ.symm : (a : ι') → ι) b))
        (update (β := M₁) m i (c • x)) =
      HSMul.hSMul (β := M₂) c
        (comp (β := (i : ι') → M₁ ((σ.symm : (a : ι') → ι) i))
          (⇑f : (a : (i : ι') → M₁ ((σ.symm : (a : ι') → ι) i)) → M₂)
          (⇑(Equiv.piCongrLeft' M₁ σ) : (a : (a : ι) → M₁ a) → (b : ι') → M₁ ((σ.symm : (a : ι') → ι) b))
          (update (β := M₁) m i x))
have rw : ∀ (x : M₁ ((σ.symm : (a : ι') → ι) ((σ : (a : ι) → ι') i : ι'))),
  comp (β := (i : ι') → M₁ ((σ.symm : (a : ι') → ι) i)) (⇑f : (a : (i : ι') → M₁ ((σ.symm : (a : ι') → ι) i)) → M₂)
      (⇑(Equiv.piCongrLeft' M₁ σ) : (a : (a : ι) → M₁ a) → (b : ι') → M₁ ((σ.symm : (a : ι') → ι) b))
      (update (β := M₁) m ((σ.symm : (a : ι') → ι) ((σ : (a : ι) → ι') i : ι')) (c • x)) =
    HSMul.hSMul (β := M₂) c
      (comp (β := (i : ι') → M₁ ((σ.symm : (a : ι') → ι) i)) (⇑f : (a : (i : ι') → M₁ ((σ.symm : (a : ι') → ι) i)) → M₂)
        (⇑(Equiv.piCongrLeft' M₁ σ) : (a : (a : ι) → M₁ a) → (b : ι') → M₁ ((σ.symm : (a : ι') → ι) b))
        (update (β := M₁) m ((σ.symm : (a : ι') → ι) ((σ : (a : ι) → ι') i : ι')) x))
Tactic: rw [← σ.symm_apply_apply i]