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 : ι) → 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₂
⊢ (fun (f : MultilinearMap.{uR, u_1, v₁, v₂} R (fun (i : ι') ↦ M₁ ((σ.symm : (a : ι') → ι) i)) M₂) ↦
        (mk (M₁ := 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)))
            ⋯ ⋯ :
          MultilinearMap R M₁ M₂))
      ((fun (f : MultilinearMap R M₁ 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))
              ⋯ ⋯ :
            MultilinearMap.{uR, u_1, v₁, v₂} R (fun (i : ι') ↦ M₁ ((σ.symm : (a : ι') → ι) i)) M₂))
        f) =
    f
have H : ∀ (x : (i : ι) → M₁ i),
  Eq.{v₂ + 1} (α := M₂)
    (((fun (f : MultilinearMap.{uR, u_1, v₁, v₂} R (fun (i : ι') ↦ M₁ ((σ.symm : (a : ι') → ι) i)) M₂) ↦
              (mk (M₁ := 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)))
                  sorry sorry :
                MultilinearMap R M₁ M₂))
            ((fun (f : MultilinearMap R M₁ 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 :
                  MultilinearMap.{uR, u_1, v₁, v₂} R (fun (i : ι') ↦ M₁ ((σ.symm : (a : ι') → ι) i)) M₂))
              f) :
          (a : (i : ι) → M₁ i) → M₂)
        x :
      M₂)
    ((f : (a : (i : ι) → M₁ 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₂
⊢ (fun (f : MultilinearMap R M₁ 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))
            ⋯ ⋯ :
          MultilinearMap.{uR, u_1, v₁, v₂} R (fun (i : ι') ↦ M₁ ((σ.symm : (a : ι') → ι) i)) M₂))
      ((fun (f : MultilinearMap.{uR, u_1, v₁, v₂} R (fun (i : ι') ↦ M₁ ((σ.symm : (a : ι') → ι) i)) M₂) ↦
          (mk (M₁ := 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)))
              ⋯ ⋯ :
            MultilinearMap R M₁ M₂))
        f) =
    f
have H : ∀ (x : (i : ι') → M₁ ((σ.symm : (a : ι') → ι) i)),
  Eq.{v₂ + 1} (α := M₂)
    (((fun (f : MultilinearMap R M₁ 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 :
                MultilinearMap.{uR, u_1, v₁, v₂} R (fun (i : ι') ↦ M₁ ((σ.symm : (a : ι') → ι) i)) M₂))
            ((fun (f : MultilinearMap.{uR, u_1, v₁, v₂} R (fun (i : ι') ↦ M₁ ((σ.symm : (a : ι') → ι) i)) M₂) ↦
                (mk (M₁ := 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)))
                    sorry sorry :
                  MultilinearMap R M₁ M₂))
              f) :
          (a : (i : ι') → M₁ ((σ.symm : (a : ι') → ι) i)) → M₂)
        x :
      M₂)
    ((f : (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
ι₂ : Type u_2
σ : ι₁ ≃ ι₂
c : S
f : MultilinearMap.{uR, u_1, v₂, v₃} R (fun (x : ι₁) ↦ M₂) M₃
⊢ Equiv.toFun (AddEquiv.toEquiv (domDomCongrEquiv σ)) (c • f) =
    HSMul.hSMul (α := S) ((RingHom.id S : (a : S) → S) c : S) (Equiv.toFun (AddEquiv.toEquiv (domDomCongrEquiv σ)) f)
have H : ∀ (x : (i : ι₂) → M₂),
  Eq.{v₃ + 1} (α := M₃)
    ((Equiv.toFun (AddEquiv.toEquiv (domDomCongrEquiv σ)) (c • f) : (a : (i : ι₂) → M₂) → M₃) x : M₃)
    ((HSMul.hSMul (α := S) ((RingHom.id S : (a : S) → S) c : S)
            (Equiv.toFun (AddEquiv.toEquiv (domDomCongrEquiv σ)) 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 : 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 : ι)
⊢ 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)
have 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₂)
Tactic: ext v
-- 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 : 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 : ι)
⊢ 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)
have 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₂)
Tactic: classical
    ext v
    simp [domDomRestrict_aux_right]
-- 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 : 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 : ι)
⊢ 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)
have 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₂)
Tactic: ext v
-- 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 : 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 : ι)
⊢ 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)
have 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₂)
Tactic: classical
    ext v
    simp [domDomRestrict_aux_right]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
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
⊢ 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
have 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
Tactic: ext i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
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)
⊢ 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
have 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
Tactic: rcases eq_or_ne a (e.symm i) with rfl | hne
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
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
⊢ 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
have 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
Tactic: rcases eq_or_ne a (e.symm i) with rfl | hne
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
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)
⊢ 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
have 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
Tactic: rw [Equiv.apply_symm_apply e i, update_self, update_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
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
⊢ 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
have 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)
Tactic: rw [Equiv.apply_symm_apply e i, update_self, update_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
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)
⊢ 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
have h₂ : Eq (α := M₁ (↑i : ι)) (z (↑i : ι)) (z (↑i : ι))
Tactic: rw [Equiv.apply_symm_apply e i, update_self, update_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
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
⊢ 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
have 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)
Tactic: rw [update_of_ne hne.symm, update_of_ne fun h ↦ (Equiv.symm_apply_apply .. ▸ h ▸ hne) rfl]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
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)
⊢ 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
have h₁ : Eq (α := M₁ (↑i : ι)) (m ((e.symm : (a : (↑s : Type u_3)) → α) i) (↑i : ι))
  (m ((e.symm : (a : (↑s : Type u_3)) → α) i) (↑i : ι))
Tactic: rw [update_of_ne hne.symm, update_of_ne fun h ↦ (Equiv.symm_apply_apply .. ▸ h ▸ hne) rfl]