awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
Goal:
R : Type uR
n : ℕ
M : Fin n.succ → Type v
M₂ : Type v₂
inst : Semiring R
inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_2 : AddCommMonoid M₂
inst_3 : (i : Fin n.succ) → Module.{uR, v} R (M i)
inst_4 : Module R M₂
f : MultilinearMap R M M₂
m : (i : Fin n) → M i.castSucc
x y : M (last n)
simp_rw :
  (f : (a : (i : Fin n.succ) → M i) → M₂) (update (β := M) (snoc (α := M) m x) (last n) (x + y)) =
    HAdd.hAdd (α := M₂) (β := M₂) ((f : (a : (i : Fin n.succ) → M i) → M₂) (snoc (α := M) m x) : M₂)
      ((f : (a : (i : Fin n.succ) → M i) → M₂) (snoc (α := M) m y) : M₂)
⊢ (f : (a : (i : Fin n.succ) → M i) → M₂) (snoc (α := M) m (x + y)) =
    HAdd.hAdd (α := M₂) (β := M₂) ((f : (a : (i : Fin n.succ) → M i) → M₂) (snoc (α := M) m x) : M₂)
      ((f : (a : (i : Fin n.succ) → M i) → M₂) (snoc (α := M) m y) : M₂)
have simp_rw₁ : HAdd.hAdd (α := M₂) (β := M₂)
    ((f : (a : (i : Fin n.succ) → M i) → M₂) (update (β := M) (snoc (α := M) m x) (last n) x) : M₂)
    ((f : (a : (i : Fin n.succ) → M i) → M₂) (update (β := M) (snoc (α := M) m x) (last n) y) : M₂) =
  HAdd.hAdd (α := M₂) (β := M₂) ((f : (a : (i : Fin n.succ) → M i) → M₂) (snoc (α := M) m x) : M₂)
    ((f : (a : (i : Fin n.succ) → M i) → M₂) (snoc (α := M) m y) : M₂)
Tactic: simp_rw [← update_snoc_last x m (x + y), f.map_update_add, update_snoc_last]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
Goal:
R : Type uR
n : ℕ
M : Fin n.succ → Type v
M₂ : Type v₂
inst : Semiring R
inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_2 : AddCommMonoid M₂
inst_3 : (i : Fin n.succ) → Module.{uR, v} R (M i)
inst_4 : Module R M₂
f : MultilinearMap R M M₂
m : (i : Fin n) → M i.castSucc
c : R
x : M (last n)
⊢ (f : (a : (i : Fin n.succ) → M i) → M₂) (snoc (α := M) m (c • x)) =
    HSMul.hSMul (β := M₂) c ((f : (a : (i : Fin n.succ) → M i) → M₂) (snoc (α := M) m x) : M₂)
have simp_rw : (f : (a : (i : Fin n.succ) → M i) → M₂) (update (β := M) (snoc (α := M) m x) (last n) (c • x)) =
  HSMul.hSMul (β := M₂) c ((f : (a : (i : Fin n.succ) → M i) → M₂) (snoc (α := M) m x) : M₂)
Tactic: simp_rw [← update_snoc_last x m (c • x), f.map_update_smul, update_snoc_last]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
Goal:
R : Type uR
n : ℕ
M : Fin n.succ → Type v
M₂ : Type v₂
inst : Semiring R
inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_2 : AddCommMonoid M₂
inst_3 : (i : Fin n.succ) → Module.{uR, v} R (M i)
inst_4 : Module R M₂
f : MultilinearMap R M M₂
m : (i : Fin n) → M i.castSucc
c : R
x : M (last n)
simp_rw :
  (f : (a : (i : Fin n.succ) → M i) → M₂) (update (β := M) (snoc (α := M) m x) (last n) (c • x)) =
    HSMul.hSMul (β := M₂) c ((f : (a : (i : Fin n.succ) → M i) → M₂) (snoc (α := M) m x) : M₂)
⊢ (f : (a : (i : Fin n.succ) → M i) → M₂) (snoc (α := M) m (c • x)) =
    HSMul.hSMul (β := M₂) c ((f : (a : (i : Fin n.succ) → M i) → M₂) (snoc (α := M) m x) : M₂)
have simp_rw₁ : HSMul.hSMul (β := M₂) c
    ((f : (a : (i : Fin n.succ) → M i) → M₂) (update (β := M) (snoc (α := M) m x) (last n) x) : M₂) =
  HSMul.hSMul (β := M₂) c ((f : (a : (i : Fin n.succ) → M i) → M₂) (snoc (α := M) m x) : M₂)
Tactic: simp_rw [← update_snoc_last x m (c • x), f.map_update_smul, update_snoc_last]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (hypothesis)
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' : MultilinearMap R M₁ M₂
inst_11 : (i : ι) → AddCommMonoid (M₁' i)
inst_12 : (i : ι) → Module.{uR, v₁'} R (M₁' i)
inst_13 : (i : ι) → AddCommMonoid (M₁'' i)
inst_14 : (i : ι) → Module.{uR, v₁''} R (M₁'' i)
g : MultilinearMap R M₁' M₂
f : (i : ι) → LinearMap.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ i) (M₁' i)
inst_15 : DecidableEq ι
m : (i : ι) → M₁ i
i : ι
x y : M₁ i
⊢ ((g : (a : (i : ι) → M₁' i) → M₂) fun (i_1 : ι) ↦
      (f i_1 : (a : M₁ i_1) → M₁' i_1) (update (β := M₁) m i (x + y) i_1)) =
    HAdd.hAdd (α := M₂) (β := M₂)
      ((g : (a : (i : ι) → M₁' i) → M₂) fun (i_1 : ι) ↦ (f i_1 : (a : M₁ i_1) → M₁' i_1) (update (β := M₁) m i x i_1) :
        M₂)
      ((g : (a : (i : ι) → M₁' i) → M₂) fun (i_1 : ι) ↦ (f i_1 : (a : M₁ i_1) → M₁' i_1) (update (β := M₁) m i y i_1) :
        M₂)
have this : ∀ (j : ι) (z : M₁ i),
  Eq.{v₁' + 1} (α := M₁' j) ((f j : (a : M₁ j) → M₁' j) (update (β := M₁) m i z j) : M₁' j)
    (update (β := M₁') (fun (k : ι) ↦ (f k : (a : M₁ k) → M₁' k) (m k)) i ((f i : (a : M₁ i) → M₁' i) z) j : M₁' j)
Tactic: have : ∀ j z, f j (update m i z j) = update (fun k => f k (m k)) i (f i z) j := fun j z =>
      Function.apply_update (fun k => f k) _ _ _ _
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (hypothesis)
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' : MultilinearMap R M₁ M₂
inst_11 : (i : ι) → AddCommMonoid (M₁' i)
inst_12 : (i : ι) → Module.{uR, v₁'} R (M₁' i)
inst_13 : (i : ι) → AddCommMonoid (M₁'' i)
inst_14 : (i : ι) → Module.{uR, v₁''} R (M₁'' i)
g : MultilinearMap R M₁' M₂
f : (i : ι) → LinearMap.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ i) (M₁' i)
inst_15 : DecidableEq ι
m : (i : ι) → M₁ i
i : ι
c : R
x : M₁ i
⊢ ((g : (a : (i : ι) → M₁' i) → M₂) fun (i_1 : ι) ↦
      (f i_1 : (a : M₁ i_1) → M₁' i_1) (update (β := M₁) m i (c • x) i_1)) =
    HSMul.hSMul (β := M₂) c
      ((g : (a : (i : ι) → M₁' i) → M₂) fun (i_1 : ι) ↦ (f i_1 : (a : M₁ i_1) → M₁' i_1) (update (β := M₁) m i x i_1) :
        M₂)
have this : ∀ (j : ι) (z : M₁ i),
  Eq.{v₁' + 1} (α := M₁' j) ((f j : (a : M₁ j) → M₁' j) (update (β := M₁) m i z j) : M₁' j)
    (update (β := M₁') (fun (k : ι) ↦ (f k : (a : M₁ k) → M₁' k) (m k)) i ((f i : (a : M₁ i) → M₁' i) z) j : M₁' j)
Tactic: have : ∀ j z, f j (update m i z j) = update (fun k => f k (m k)) i (f i z) j := fun j z =>
      Function.apply_update (fun k => f k) _ _ _ _
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
Goal:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
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 : (i : ι) → AddCommMonoid (M₁' i)
inst_6 : (i : ι) → Module.{uR, v₁'} R (M₁' i)
g : MultilinearMap R M₁' M₂
f : (i : ι) → LinearEquiv.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ i) (M₁' i)
f' : (i : ι) → LinearMap.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ i) (M₁' i) := fun (i : ι) ↦ (↑(f i) : M₁ i →ₗ[R] M₁' i)
⊢ g.compLinearMap (M₁ := M₁) (M₁' := M₁') f' = 0 ↔ g = 0
have rw : g.compLinearMap (M₁ := M₁) (M₁' := M₁') f' = compLinearMap (M₁ := M₁) (M₁' := M₁') 0 f' ↔ g = 0
Tactic: rw [← zero_compLinearMap f', compLinearMap_inj f' fun i => (f i).surjective]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
Goal:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
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 : (i : ι) → AddCommMonoid (M₁' i)
inst_6 : (i : ι) → Module.{uR, v₁'} R (M₁' i)
g : MultilinearMap R M₁' M₂
f : (i : ι) → LinearEquiv.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ i) (M₁' i)
f' : (i : ι) → LinearMap.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ i) (M₁' i) := fun (i : ι) ↦ (↑(f i) : M₁ i →ₗ[R] M₁' i)
rw : g.compLinearMap (M₁ := M₁) (M₁' := M₁') f' = compLinearMap (M₁ := M₁) (M₁' := M₁') 0 f' ↔ g = 0
⊢ g.compLinearMap (M₁ := M₁) (M₁' := M₁') f' = 0 ↔ g = 0
have rw₁ : g = 0 ↔ g = 0
Tactic: rw [← zero_compLinearMap f', compLinearMap_inj f' fun i => (f i).surjective]
-- 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₂
f : MultilinearMap R M₁ M₂
inst_5 : DecidableEq ι
m m' : (i : ι) → M₁ i
t : Finset ι
⊢ Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (t.piecewise (π := M₁) (m + m') m') : M₂)
    (∑ s ∈ t.powerset, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) m m') : M₂)
have revert : ∀ (m' : (i : ι) → M₁ i),
  Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (t.piecewise (π := M₁) (m + m') m') : M₂)
    (∑ s ∈ t.powerset, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) m m') : M₂)
Tactic: revert m'
Cleared hypotheses: m'
-- 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₂
f : MultilinearMap R M₁ M₂
inst_5 : DecidableEq ι
m : (i : ι) → M₁ i
t : Finset ι
⊢ ∀ (m' : (i : ι) → M₁ i),
    Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (t.piecewise (π := M₁) (m + m') m') : M₂)
      (∑ s ∈ t.powerset, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) m m') : M₂)
have refine : ∀ (a : ι) (s : Finset ι),
  a ∉ s →
    (∀ (m' : (i : ι) → M₁ i),
        Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) (m + m') m') : M₂)
          (∑ s ∈ s.powerset, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) m m') : M₂)) →
      ∀ (m' : (i : ι) → M₁ i),
        Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) ((insert a s).piecewise (π := M₁) (m + m') m') : M₂)
          (∑ s ∈ (insert a s).powerset, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) m m') : M₂)
Tactic: refine Finset.induction_on t (by simp) ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (hypothesis)
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₂
f : MultilinearMap R M₁ M₂
inst_5 : DecidableEq ι
m : (i : ι) → M₁ i
t_1 : Finset ι
i : ι
t : Finset ι
hit : i ∉ t
Hrec :
  ∀ (m' : (i : ι) → M₁ i),
    Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (t.piecewise (π := M₁) (m + m') m') : M₂)
      (∑ s ∈ t.powerset, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) m m') : M₂)
m' : (i : ι) → M₁ i
⊢ Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) ((insert i t).piecewise (π := M₁) (m + m') m') : M₂)
    (∑ s ∈ (insert i t).powerset, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) m m') : M₂)
have A : (insert i t).piecewise (π := M₁) (m + m') m' = update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m i + m' i)
Tactic: have A : (insert i t).piecewise (m + m') m' = update (t.piecewise (m + m') m') i (m i + m' i) :=
    t.piecewise_insert _ _ _
-- 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₂
f : MultilinearMap R M₁ M₂
inst_5 : DecidableEq ι
m : (i : ι) → M₁ i
t_1 : Finset ι
i : ι
t : Finset ι
hit : i ∉ t
Hrec :
  ∀ (m' : (i : ι) → M₁ i),
    Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (t.piecewise (π := M₁) (m + m') m') : M₂)
      (∑ s ∈ t.powerset, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) m m') : M₂)
m' : (i : ι) → M₁ i
A : (insert i t).piecewise (π := M₁) (m + m') m' = update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m i + m' i)
⊢ update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m' i) = t.piecewise (π := M₁) (m + m') m'
have h : ∀ (j : ι), update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m' i) j = t.piecewise (π := M₁) (m + m') m' j
Tactic: ext j
-- 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₂
f : MultilinearMap R M₁ M₂
inst_5 : DecidableEq ι
m : (i : ι) → M₁ i
t_1 : Finset ι
i : ι
t : Finset ι
hit : i ∉ t
Hrec :
  ∀ (m' : (i : ι) → M₁ i),
    Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (t.piecewise (π := M₁) (m + m') m') : M₂)
      (∑ s ∈ t.powerset, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) m m') : M₂)
m' : (i : ι) → M₁ i
A : (insert i t).piecewise (π := M₁) (m + m') m' = update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m i + m' i)
j : ι
⊢ update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m' i) j = t.piecewise (π := M₁) (m + m') m' j
have pos : ∀ (h : j = i), update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m' i) j = t.piecewise (π := M₁) (m + m') m' j
Tactic: by_cases h : j = i
-- 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₂
f : MultilinearMap R M₁ M₂
inst_5 : DecidableEq ι
m : (i : ι) → M₁ i
t_1 : Finset ι
i : ι
t : Finset ι
hit : i ∉ t
Hrec :
  ∀ (m' : (i : ι) → M₁ i),
    Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (t.piecewise (π := M₁) (m + m') m') : M₂)
      (∑ s ∈ t.powerset, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) m m') : M₂)
m' : (i : ι) → M₁ i
A : (insert i t).piecewise (π := M₁) (m + m') m' = update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m i + m' i)
j : ι
pos :
  ∀ (h : j = i), update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m' i) j = t.piecewise (π := M₁) (m + m') m' j
⊢ update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m' i) j = t.piecewise (π := M₁) (m + m') m' j
have neg : ∀ (h : ¬j = i), update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m' i) j = t.piecewise (π := M₁) (m + m') m' j
Tactic: by_cases h : j = i
-- 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₂
f : MultilinearMap R M₁ M₂
inst_5 : DecidableEq ι
m : (i : ι) → M₁ i
t_1 : Finset ι
i : ι
t : Finset ι
hit : i ∉ t
Hrec :
  ∀ (m' : (i : ι) → M₁ i),
    Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (t.piecewise (π := M₁) (m + m') m') : M₂)
      (∑ s ∈ t.powerset, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) m m') : M₂)
m' : (i : ι) → M₁ i
A : (insert i t).piecewise (π := M₁) (m + m') m' = update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m i + m' i)
j : ι
h : j = i
⊢ update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m' i) j = t.piecewise (π := M₁) (m + m') m' j
have pos : update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m' i) i = t.piecewise (π := M₁) (m + m') m' i
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (hypothesis)
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₂
f : MultilinearMap R M₁ M₂
inst_5 : DecidableEq ι
m : (i : ι) → M₁ i
t_1 : Finset ι
i : ι
t : Finset ι
hit : i ∉ t
Hrec :
  ∀ (m' : (i : ι) → M₁ i),
    Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (t.piecewise (π := M₁) (m + m') m') : M₂)
      (∑ s ∈ t.powerset, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) m m') : M₂)
m' : (i : ι) → M₁ i
A : (insert i t).piecewise (π := M₁) (m + m') m' = update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m i + m' i)
⊢ Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) ((insert i t).piecewise (π := M₁) (m + m') m') : M₂)
    (∑ s ∈ (insert i t).powerset, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) m m') : M₂)
have B : update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m' i) = t.piecewise (π := M₁) (m + m') m'
Tactic: have B : update (t.piecewise (m + m') m') i (m' i) = t.piecewise (m + m') m' := by
    ext j
    by_cases h : j = i
    · rw [h]
      simp [hit]
    · simp [h]
-- 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₂
f : MultilinearMap R M₁ M₂
inst_5 : DecidableEq ι
m : (i : ι) → M₁ i
t_1 : Finset ι
i : ι
t : Finset ι
hit : i ∉ t
Hrec :
  ∀ (m' : (i : ι) → M₁ i),
    Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (t.piecewise (π := M₁) (m + m') m') : M₂)
      (∑ s ∈ t.powerset, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) m m') : M₂)
m' : (i : ι) → M₁ i
A : (insert i t).piecewise (π := M₁) (m + m') m' = update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m i + m' i)
B : update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m' i) = t.piecewise (π := M₁) (m + m') m'
m'' : (a : ι) → M₁ a := update (β := M₁) m' i (m i)
⊢ update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m i) = t.piecewise (π := M₁) (m + m'') m''
have h : ∀ (j : ι), update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m i) j = t.piecewise (π := M₁) (m + m'') m'' j
Tactic: ext j
-- 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₂
f : MultilinearMap R M₁ M₂
inst_5 : DecidableEq ι
m : (i : ι) → M₁ i
t_1 : Finset ι
i : ι
t : Finset ι
hit : i ∉ t
Hrec :
  ∀ (m' : (i : ι) → M₁ i),
    Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (t.piecewise (π := M₁) (m + m') m') : M₂)
      (∑ s ∈ t.powerset, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) m m') : M₂)
m' : (i : ι) → M₁ i
A : (insert i t).piecewise (π := M₁) (m + m') m' = update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m i + m' i)
B : update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m' i) = t.piecewise (π := M₁) (m + m') m'
m'' : (a : ι) → M₁ a := update (β := M₁) m' i (m i)
j : ι
⊢ update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m i) j = t.piecewise (π := M₁) (m + m'') m'' j
have pos : ∀ (h : j = i), update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m i) j = t.piecewise (π := M₁) (m + m'') m'' j
Tactic: by_cases h : j = i
-- 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₂
f : MultilinearMap R M₁ M₂
inst_5 : DecidableEq ι
m : (i : ι) → M₁ i
t_1 : Finset ι
i : ι
t : Finset ι
hit : i ∉ t
Hrec :
  ∀ (m' : (i : ι) → M₁ i),
    Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (t.piecewise (π := M₁) (m + m') m') : M₂)
      (∑ s ∈ t.powerset, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) m m') : M₂)
m' : (i : ι) → M₁ i
A : (insert i t).piecewise (π := M₁) (m + m') m' = update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m i + m' i)
B : update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m' i) = t.piecewise (π := M₁) (m + m') m'
m'' : (a : ι) → M₁ a := update (β := M₁) m' i (m i)
j : ι
pos :
  ∀ (h : j = i), update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m i) j = t.piecewise (π := M₁) (m + m'') m'' j
⊢ update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m i) j = t.piecewise (π := M₁) (m + m'') m'' j
have neg : ∀ (h : ¬j = i), update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m i) j = t.piecewise (π := M₁) (m + m'') m'' j
Tactic: by_cases h : j = i
-- 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₂
f : MultilinearMap R M₁ M₂
inst_5 : DecidableEq ι
m : (i : ι) → M₁ i
t_1 : Finset ι
i : ι
t : Finset ι
hit : i ∉ t
Hrec :
  ∀ (m' : (i : ι) → M₁ i),
    Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (t.piecewise (π := M₁) (m + m') m') : M₂)
      (∑ s ∈ t.powerset, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) m m') : M₂)
m' : (i : ι) → M₁ i
A : (insert i t).piecewise (π := M₁) (m + m') m' = update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m i + m' i)
B : update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m' i) = t.piecewise (π := M₁) (m + m') m'
m'' : (a : ι) → M₁ a := update (β := M₁) m' i (m i)
j : ι
h : j = i
⊢ update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m i) j = t.piecewise (π := M₁) (m + m'') m'' j
have pos : update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m i) i = t.piecewise (π := M₁) (m + m'') m'' i
Tactic: rw [h]
-- 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₂
f : MultilinearMap R M₁ M₂
inst_5 : DecidableEq ι
m : (i : ι) → M₁ i
t_1 : Finset ι
i : ι
t : Finset ι
hit : i ∉ t
Hrec :
  ∀ (m' : (i : ι) → M₁ i),
    Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (t.piecewise (π := M₁) (m + m') m') : M₂)
      (∑ s ∈ t.powerset, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) m m') : M₂)
m' : (i : ι) → M₁ i
A : (insert i t).piecewise (π := M₁) (m + m') m' = update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m i + m' i)
B : update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m' i) = t.piecewise (π := M₁) (m + m') m'
m'' : (a : ι) → M₁ a := update (β := M₁) m' i (m i)
j : ι
h : ¬j = i
⊢ update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m i) j = t.piecewise (π := M₁) (m + m'') m'' j
have pos : ∀ (h' : j ∈ t), update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m i) j = t.piecewise (π := M₁) (m + m'') m'' j
Tactic: by_cases h' : j ∈ t
-- 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₂
f : MultilinearMap R M₁ M₂
inst_5 : DecidableEq ι
m : (i : ι) → M₁ i
t_1 : Finset ι
i : ι
t : Finset ι
hit : i ∉ t
Hrec :
  ∀ (m' : (i : ι) → M₁ i),
    Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (t.piecewise (π := M₁) (m + m') m') : M₂)
      (∑ s ∈ t.powerset, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) m m') : M₂)
m' : (i : ι) → M₁ i
A : (insert i t).piecewise (π := M₁) (m + m') m' = update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m i + m' i)
B : update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m' i) = t.piecewise (π := M₁) (m + m') m'
m'' : (a : ι) → M₁ a := update (β := M₁) m' i (m i)
j : ι
h : ¬j = i
pos :
  ∀ (h' : j ∈ t), update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m i) j = t.piecewise (π := M₁) (m + m'') m'' j
⊢ update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m i) j = t.piecewise (π := M₁) (m + m'') m'' j
have neg : ∀ (h' : j ∉ t), update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m i) j = t.piecewise (π := M₁) (m + m'') m'' j
Tactic: by_cases h' : j ∈ t