awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
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)
⊢ 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 C : update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m i) = t.piecewise (π := M₁) (m + m'') m''
Tactic: have C : 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 [m'', hit]
    · by_cases h' : j ∈ t <;> simp [m'', h, 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)
C : update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m i) = t.piecewise (π := M₁) (m + m'') m''
⊢ 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 rw : HAdd.hAdd (α := M₂) (∑ s ∈ t.powerset, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) m m'))
    (∑ s ∈ t.powerset, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) m m'')) =
  HAdd.hAdd (α := M₂) (∑ t ∈ t.powerset, (f : (a : (i : ι) → M₁ i) → M₂) (t.piecewise (π := M₁) m m'))
    (∑ t ∈ t.powerset, (f : (a : (i : ι) → M₁ i) → M₂) ((insert i t).piecewise (π := M₁) m m'))
Tactic: rw [A, f.map_update_add, B, C, Finset.sum_powerset_insert hit, Hrec, Hrec, add_comm (_ : 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_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)
C : update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m i) = t.piecewise (π := M₁) (m + m'') m''
⊢ HAdd.hAdd (α := M₂) (∑ s ∈ t.powerset, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) m m'))
      (∑ s ∈ t.powerset, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) m m'')) =
    HAdd.hAdd (α := M₂) (∑ t ∈ t.powerset, (f : (a : (i : ι) → M₁ i) → M₂) (t.piecewise (π := M₁) m m'))
      (∑ t ∈ t.powerset, (f : (a : (i : ι) → M₁ i) → M₂) ((insert i t).piecewise (π := M₁) m m'))
have e_a : Eq.{v₂ + 1} (α := M₂) (∑ s ∈ t.powerset, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) m m''))
  (∑ t ∈ t.powerset, (f : (a : (i : ι) → M₁ i) → M₂) ((insert i t).piecewise (π := M₁) m m'))
Tactic: congr 1
-- 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)
C : update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m i) = t.piecewise (π := M₁) (m + m'') m''
⊢ Eq.{v₂ + 1} (α := M₂) (∑ s ∈ t.powerset, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) m m''))
    (∑ t ∈ t.powerset, (f : (a : (i : ι) → M₁ i) → M₂) ((insert i t).piecewise (π := M₁) m m'))
have e_a : ∀ (s : Finset ι) (hs : s ∈ t.powerset),
  Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) m m'') : M₂)
    ((f : (a : (i : ι) → M₁ i) → M₂) ((insert i s).piecewise (π := M₁) m m') : M₂)
Tactic: refine Finset.sum_congr rfl fun s hs => ?_
-- 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)
C : update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m i) = t.piecewise (π := M₁) (m + m'') m''
s : Finset ι
hs : s ∈ t.powerset
⊢ (insert i s).piecewise (π := M₁) m m' = s.piecewise (π := M₁) m m''
have h : ∀ (j : ι), (insert i s).piecewise (π := M₁) m m' j = s.piecewise (π := 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)
C : update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m i) = t.piecewise (π := M₁) (m + m'') m''
s : Finset ι
hs : s ∈ t.powerset
j : ι
⊢ (insert i s).piecewise (π := M₁) m m' j = s.piecewise (π := M₁) m m'' j
have pos : ∀ (h : j = i), (insert i s).piecewise (π := M₁) m m' j = s.piecewise (π := 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)
C : update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m i) = t.piecewise (π := M₁) (m + m'') m''
s : Finset ι
hs : s ∈ t.powerset
j : ι
pos : ∀ (h : j = i), (insert i s).piecewise (π := M₁) m m' j = s.piecewise (π := M₁) m m'' j
⊢ (insert i s).piecewise (π := M₁) m m' j = s.piecewise (π := M₁) m m'' j
have neg : ∀ (h : ¬j = i), (insert i s).piecewise (π := M₁) m m' j = s.piecewise (π := 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)
C : update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m i) = t.piecewise (π := M₁) (m + m'') m''
s : Finset ι
hs : s ∈ t.powerset
j : ι
h : j = i
⊢ (insert i s).piecewise (π := M₁) m m' j = s.piecewise (π := M₁) m m'' j
have pos : (insert i s).piecewise (π := M₁) m m' i = s.piecewise (π := 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)
C : update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m i) = t.piecewise (π := M₁) (m + m'') m''
s : Finset ι
hs : s ∈ t.powerset
j : ι
h : ¬j = i
⊢ (insert i s).piecewise (π := M₁) m m' j = s.piecewise (π := M₁) m m'' j
have pos : ∀ (h' : j ∈ s), (insert i s).piecewise (π := M₁) m m' j = s.piecewise (π := M₁) m m'' j
Tactic: by_cases h' : j ∈ s
-- 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)
C : update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m i) = t.piecewise (π := M₁) (m + m'') m''
s : Finset ι
hs : s ∈ t.powerset
j : ι
h : ¬j = i
pos : ∀ (h' : j ∈ s), (insert i s).piecewise (π := M₁) m m' j = s.piecewise (π := M₁) m m'' j
⊢ (insert i s).piecewise (π := M₁) m m' j = s.piecewise (π := M₁) m m'' j
have neg : ∀ (h' : j ∉ s), (insert i s).piecewise (π := M₁) m m' j = s.piecewise (π := M₁) m m'' j
Tactic: by_cases h' : j ∈ s
-- 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)
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)
C : update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m i) = t.piecewise (π := M₁) (m + m'') m''
s : Finset ι
hs : s ∈ t.powerset
⊢ Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) m m'') : M₂)
    ((f : (a : (i : ι) → M₁ i) → M₂) ((insert i s).piecewise (π := M₁) m m') : M₂)
have this : (insert i s).piecewise (π := M₁) m m' = s.piecewise (π := M₁) m m''
Tactic: have : (insert i s).piecewise m m' = s.piecewise m m'' := by
    ext j
    by_cases h : j = i
    · rw [h]
      simp [m'', Finset.notMem_of_mem_powerset_of_notMem hs hit]
    · by_cases h' : j ∈ s <;> simp [m'', h, 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)
C : update (β := M₁) (t.piecewise (π := M₁) (m + m') m') i (m i) = t.piecewise (π := M₁) (m + m'') m''
s : Finset ι
hs : s ∈ t.powerset
this : (insert i s).piecewise (π := M₁) m m' = s.piecewise (π := M₁) m m''
⊢ Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) m m'') : M₂)
    ((f : (a : (i : ι) → M₁ i) → M₂) ((insert i s).piecewise (π := M₁) m m') : M₂)
have e_a : Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) m m'') : M₂)
  ((f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) m m'') : M₂)
Tactic: rw [this]
-- 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₂
α : ι → Type u_1
g : (i : ι) → α i → M₁ i
inst_5 : DecidableEq ι
inst_6 : Fintype ι
this : (i : ι) → DecidableEq (α i) := fun (i : ι) ↦ Classical.decEq (α i)
n : ℕ
IH :
  ∀ m < n,
    ∀ (A : (i : ι) → Finset (α i)) (h : ∑ i : ι, #(A i) = m),
      Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ ∑ j ∈ A i, g i j : M₂)
        (∑ r ∈ piFinset (δ := α) A, (f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ g i (r i) : M₂)
A : (i : ι) → Finset (α i)
h : ∑ i : ι, #(A i) = n
⊢ Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ ∑ j ∈ A i, g i j : M₂)
    (∑ r ∈ piFinset (δ := α) A, (f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ g i (r i) : M₂)
have pos : ∀ (Ai_empty : ∃ (i : ι), A i = ∅),
  Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ ∑ j ∈ A i, g i j : M₂)
    (∑ r ∈ piFinset (δ := α) A, (f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ g i (r i) : M₂)
Tactic: by_cases! Ai_empty : ∃ i, A 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₂
α : ι → Type u_1
g : (i : ι) → α i → M₁ i
inst_5 : DecidableEq ι
inst_6 : Fintype ι
this : (i : ι) → DecidableEq (α i) := fun (i : ι) ↦ Classical.decEq (α i)
n : ℕ
IH :
  ∀ m < n,
    ∀ (A : (i : ι) → Finset (α i)) (h : ∑ i : ι, #(A i) = m),
      Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ ∑ j ∈ A i, g i j : M₂)
        (∑ r ∈ piFinset (δ := α) A, (f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ g i (r i) : M₂)
A : (i : ι) → Finset (α i)
h : ∑ i : ι, #(A i) = n
pos :
  ∀ (Ai_empty : ∃ (i : ι), A i = ∅),
    Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ ∑ j ∈ A i, g i j : M₂)
      (∑ r ∈ piFinset (δ := α) A, (f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ g i (r i) : M₂)
⊢ Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ ∑ j ∈ A i, g i j : M₂)
    (∑ r ∈ piFinset (δ := α) A, (f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ g i (r i) : M₂)
have neg : ∀ (Ai_empty : ∀ (i : ι), (A i).Nonempty),
  Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ ∑ j ∈ A i, g i j : M₂)
    (∑ r ∈ piFinset (δ := α) A, (f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ g i (r i) : M₂)
Tactic: by_cases! Ai_empty : ∃ i, A 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₂
α : ι → Type u_1
g : (i : ι) → α i → M₁ i
inst_5 : DecidableEq ι
inst_6 : Fintype ι
this : (i : ι) → DecidableEq (α i) := fun (i : ι) ↦ Classical.decEq (α i)
n : ℕ
IH :
  ∀ m < n,
    ∀ (A : (i : ι) → Finset (α i)) (h : ∑ i : ι, #(A i) = m),
      Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ ∑ j ∈ A i, g i j : M₂)
        (∑ r ∈ piFinset (δ := α) A, (f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ g i (r i) : M₂)
A : (i : ι) → Finset (α i)
h : ∑ i : ι, #(A i) = n
Ai_empty : ∃ (i : ι), A i = ∅
⊢ Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ ∑ j ∈ A i, g i j : M₂)
    (∑ r ∈ piFinset (δ := α) A, (f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ g i (r i) : M₂)
have pos : ∀ (i : ι) (hi : Eq.{v₁ + 1} (α := M₁ i) (∑ j ∈ A i, g i j) 0),
  Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ ∑ j ∈ A i, g i j : M₂)
    (∑ r ∈ piFinset (δ := α) A, (f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ g i (r i) : M₂)
Tactic: obtain ⟨i, hi⟩ : ∃ i, ∑ j ∈ A i, g i j = 0 := Ai_empty.imp fun i hi ↦ by simp [hi]
-- 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₂
α : ι → Type u_1
g : (i : ι) → α i → M₁ i
inst_5 : DecidableEq ι
inst_6 : Fintype ι
this : (i : ι) → DecidableEq (α i) := fun (i : ι) ↦ Classical.decEq (α i)
n : ℕ
IH :
  ∀ m < n,
    ∀ (A : (i : ι) → Finset (α i)) (h : ∑ i : ι, #(A i) = m),
      Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ ∑ j ∈ A i, g i j : M₂)
        (∑ r ∈ piFinset (δ := α) A, (f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ g i (r i) : M₂)
A : (i : ι) → Finset (α i)
h : ∑ i : ι, #(A i) = n
Ai_empty : ∃ (i : ι), A i = ∅
i : ι
hi : Eq.{v₁ + 1} (α := M₁ i) (∑ j ∈ A i, g i j) 0
⊢ Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ ∑ j ∈ A i, g i j : M₂)
    (∑ r ∈ piFinset (δ := α) A, (f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ g i (r i) : M₂)
have hpi : piFinset (δ := α) A = ∅
Tactic: have hpi : piFinset A = ∅ := by simpa
-- 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₂
α : ι → Type u_1
g : (i : ι) → α i → M₁ i
inst_5 : DecidableEq ι
inst_6 : Fintype ι
this : (i : ι) → DecidableEq (α i) := fun (i : ι) ↦ Classical.decEq (α i)
n : ℕ
IH :
  ∀ m < n,
    ∀ (A : (i : ι) → Finset (α i)) (h : ∑ i : ι, #(A i) = m),
      Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ ∑ j ∈ A i, g i j : M₂)
        (∑ r ∈ piFinset (δ := α) A, (f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ g i (r i) : M₂)
A : (i : ι) → Finset (α i)
h : ∑ i : ι, #(A i) = n
Ai_empty : ∃ (i : ι), A i = ∅
i : ι
hi : Eq.{v₁ + 1} (α := M₁ i) (∑ j ∈ A i, g i j) 0
hpi : piFinset (δ := α) A = ∅
⊢ Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ ∑ j ∈ A i, g i j : M₂)
    (∑ r ∈ piFinset (δ := α) A, (f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ g i (r i) : M₂)
have pos : Eq.{v₂ + 1} (α := M₂) 0 (∑ r ∈ piFinset (δ := α) A, (f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ g i (r i))
Tactic: rw [f.map_coord_zero i hi, hpi, Finset.sum_empty]