awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.DFinsupp (goal)
Goal:
ι : Type uι
κ : ι → Type uκ
S : Type uS
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : Semiring R
inst_3 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_4 : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst_5 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_6 : (p : (i : ι) → κ i) → Module.{uR, uN} R (N p)
f : (p : (i : ι) → κ i) → MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) (N p)
x : (i : ι) → Π₀ (j : κ i), M i j
s : (i : ι) → { s : Multiset (κ i) // ∀ (i_1 : κ i), i_1 ∈ s ∨ (x i).toFun (β := fun (j : κ i) ↦ M i j) i_1 = 0 }
p : (i : ι) → κ i
⊢ (∃ (a : (a : ι) → Membership.mem (γ := Finset ι) Finset.univ a → κ a),
      (∀ (a_1 : ι), a a_1 ⋯ ∈ (↑(s a_1) : Multiset (κ a_1))) ∧ (fun (i : ι) ↦ a i ⋯) = p) ∨
    Eq.{uN + 1} (α := N p) ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i : ι) ↦ (x i : (a : κ i) → M i a) (p i)) 0
have simp_rw : ¬Eq.{uN + 1} (α := N p) ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i : ι) ↦ (x i : (a : κ i) → M i a) (p i)) 0 →
  ∃ (a : (a : ι) → Membership.mem (γ := Finset ι) Finset.univ a → κ a),
    (∀ (a_1 : ι), a a_1 sorry ∈ (↑(s a_1) : Multiset (κ a_1))) ∧ (fun (i : ι) ↦ a i sorry) = p
Tactic: simp_rw [or_iff_not_imp_right]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.DFinsupp (goal)
Goal:
ι : Type uι
κ : ι → Type uκ
S : Type uS
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : Semiring R
inst_3 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_4 : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst_5 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_6 : (p : (i : ι) → κ i) → Module.{uR, uN} R (N p)
f : (p : (i : ι) → κ i) → MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) (N p)
x : (i : ι) → Π₀ (j : κ i), M i j
s : (i : ι) → { s : Multiset (κ i) // ∀ (i_1 : κ i), i_1 ∈ s ∨ (x i).toFun (β := fun (j : κ i) ↦ M i j) i_1 = 0 }
p : (i : ι) → κ i
h : Ne.{uN + 1} (α := N p) ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i : ι) ↦ (x i : (a : κ i) → M i a) (p i)) 0
⊢ ∃ (a : (a : ι) → Membership.mem (γ := Finset ι) Finset.univ a → κ a),
    (∀ (a_1 : ι), a a_1 ⋯ ∈ (↑(s a_1) : Multiset (κ a_1))) ∧ (fun (i : ι) ↦ a i ⋯) = p
have refine : ∀ (i : ι),
  ¬Eq (α := M i ((fun (i : ι) (x : Membership.mem (γ := Finset ι) Finset.univ i) ↦ p i) i sorry))
      ((x i).toFun (β := fun (j : κ i) ↦ M i j)
        ((fun (i : ι) (x : Membership.mem (γ := Finset ι) Finset.univ i) ↦ p i) i sorry))
      0
Tactic: refine ⟨fun i _ => p i, fun i => (s i).prop _ |>.resolve_right ?_, rfl⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.DFinsupp (goal)
Goal:
ι : Type uι
κ : ι → Type uκ
S : Type uS
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : Semiring R
inst_3 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_4 : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst_5 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_6 : (p : (i : ι) → κ i) → Module.{uR, uN} R (N p)
f : (p : (i : ι) → κ i) → MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) (N p)
dec : DecidableEq ι
m : (i : ι) → Π₀ (j : κ i), M i j
i : ι
x y : Π₀ (j : κ i), M i j
p : (i : ι) → κ i
⊢ ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
      (Function.update (β := fun (i : ι) ↦ Π₀ (j : κ i), M i j) m i (x + y) i_1 : (a : κ i_1) → M i_1 a) (p i_1)) =
    HAdd.hAdd (α := N p)
      ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
        (Function.update (β := fun (i : ι) ↦ Π₀ (j : κ i), M i j) m i x i_1 : (a : κ i_1) → M i_1 a) (p i_1))
      ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
        (Function.update (β := fun (i : ι) ↦ Π₀ (j : κ i), M i j) m i y i_1 : (a : κ i_1) → M i_1 a) (p i_1))
have simp_rw : ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
    Function.update (β := fun (i : ι) ↦ M i (p i)) (fun (k : ι) ↦ (m k : (a : κ k) → M k a) (p k)) i
      ((x + y : (a : κ i) → M i a) (p i) : M i (p i)) i_1) =
  HAdd.hAdd (α := N p)
    ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
      Function.update (β := fun (i : ι) ↦ M i (p i)) (fun (k : ι) ↦ (m k : (a : κ k) → M k a) (p k)) i
        ((x : (a : κ i) → M i a) (p i) : M i (p i)) i_1)
    ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
      Function.update (β := fun (i : ι) ↦ M i (p i)) (fun (k : ι) ↦ (m k : (a : κ k) → M k a) (p k)) i
        ((y : (a : κ i) → M i a) (p i) : M i (p i)) i_1)
Tactic: simp_rw [Function.apply_update (fun i m => m (p i)) m, DFinsupp.add_apply, (f p).map_update_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.DFinsupp (goal)
Goal:
ι : Type uι
κ : ι → Type uκ
S : Type uS
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : Semiring R
inst_3 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_4 : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst_5 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_6 : (p : (i : ι) → κ i) → Module.{uR, uN} R (N p)
f : (p : (i : ι) → κ i) → MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) (N p)
dec : DecidableEq ι
m : (i : ι) → Π₀ (j : κ i), M i j
i : ι
x y : Π₀ (j : κ i), M i j
p : (i : ι) → κ i
simp_rw :
  ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
      Function.update (β := fun (i : ι) ↦ M i (p i)) (fun (k : ι) ↦ (m k : (a : κ k) → M k a) (p k)) i
        ((x + y : (a : κ i) → M i a) (p i) : M i (p i)) i_1) =
    HAdd.hAdd (α := N p)
      ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
        Function.update (β := fun (i : ι) ↦ M i (p i)) (fun (k : ι) ↦ (m k : (a : κ k) → M k a) (p k)) i
          ((x : (a : κ i) → M i a) (p i) : M i (p i)) i_1)
      ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
        Function.update (β := fun (i : ι) ↦ M i (p i)) (fun (k : ι) ↦ (m k : (a : κ k) → M k a) (p k)) i
          ((y : (a : κ i) → M i a) (p i) : M i (p i)) i_1)
⊢ ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
      (Function.update (β := fun (i : ι) ↦ Π₀ (j : κ i), M i j) m i (x + y) i_1 : (a : κ i_1) → M i_1 a) (p i_1)) =
    HAdd.hAdd (α := N p)
      ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
        (Function.update (β := fun (i : ι) ↦ Π₀ (j : κ i), M i j) m i x i_1 : (a : κ i_1) → M i_1 a) (p i_1))
      ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
        (Function.update (β := fun (i : ι) ↦ Π₀ (j : κ i), M i j) m i y i_1 : (a : κ i_1) → M i_1 a) (p i_1))
have simp_rw₁ : ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
    Function.update (β := fun (i : ι) ↦ M i (p i)) (fun (k : ι) ↦ (m k : (a : κ k) → M k a) (p k)) i
      (HAdd.hAdd (α := M i (p i)) ((x : (a : κ i) → M i a) (p i)) ((y : (a : κ i) → M i a) (p i))) i_1) =
  HAdd.hAdd (α := N p)
    ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
      Function.update (β := fun (i : ι) ↦ M i (p i)) (fun (k : ι) ↦ (m k : (a : κ k) → M k a) (p k)) i
        ((x : (a : κ i) → M i a) (p i) : M i (p i)) i_1)
    ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
      Function.update (β := fun (i : ι) ↦ M i (p i)) (fun (k : ι) ↦ (m k : (a : κ k) → M k a) (p k)) i
        ((y : (a : κ i) → M i a) (p i) : M i (p i)) i_1)
Tactic: simp_rw [Function.apply_update (fun i m => m (p i)) m, DFinsupp.add_apply, (f p).map_update_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.DFinsupp (goal)
Goal:
ι : Type uι
κ : ι → Type uκ
S : Type uS
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : Semiring R
inst_3 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_4 : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst_5 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_6 : (p : (i : ι) → κ i) → Module.{uR, uN} R (N p)
f : (p : (i : ι) → κ i) → MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) (N p)
dec : DecidableEq ι
m : (i : ι) → Π₀ (j : κ i), M i j
i : ι
c : R
x : Π₀ (j : κ i), M i j
p : (i : ι) → κ i
⊢ ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
      (Function.update (β := fun (i : ι) ↦ Π₀ (j : κ i), M i j) m i (c • x) i_1 : (a : κ i_1) → M i_1 a) (p i_1)) =
    HSMul.hSMul (β := N p) c
      ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
        (Function.update (β := fun (i : ι) ↦ Π₀ (j : κ i), M i j) m i x i_1 : (a : κ i_1) → M i_1 a) (p i_1))
have simp_rw : ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
    Function.update (β := fun (i : ι) ↦ M i (p i)) (fun (k : ι) ↦ (m k : (a : κ k) → M k a) (p k)) i
      ((c • x : (a : κ i) → M i a) (p i) : M i (p i)) i_1) =
  HSMul.hSMul (β := N p) c
    ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
      Function.update (β := fun (i : ι) ↦ M i (p i)) (fun (k : ι) ↦ (m k : (a : κ k) → M k a) (p k)) i
        ((x : (a : κ i) → M i a) (p i) : M i (p i)) i_1)
Tactic: simp_rw [Function.apply_update (fun i m => m (p i)) m, DFinsupp.smul_apply,
      (f p).map_update_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.DFinsupp (goal)
Goal:
ι : Type uι
κ : ι → Type uκ
S : Type uS
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : Semiring R
inst_3 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_4 : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst_5 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_6 : (p : (i : ι) → κ i) → Module.{uR, uN} R (N p)
f : (p : (i : ι) → κ i) → MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) (N p)
dec : DecidableEq ι
m : (i : ι) → Π₀ (j : κ i), M i j
i : ι
c : R
x : Π₀ (j : κ i), M i j
p : (i : ι) → κ i
simp_rw :
  ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
      Function.update (β := fun (i : ι) ↦ M i (p i)) (fun (k : ι) ↦ (m k : (a : κ k) → M k a) (p k)) i
        ((c • x : (a : κ i) → M i a) (p i) : M i (p i)) i_1) =
    HSMul.hSMul (β := N p) c
      ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
        Function.update (β := fun (i : ι) ↦ M i (p i)) (fun (k : ι) ↦ (m k : (a : κ k) → M k a) (p k)) i
          ((x : (a : κ i) → M i a) (p i) : M i (p i)) i_1)
⊢ ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
      (Function.update (β := fun (i : ι) ↦ Π₀ (j : κ i), M i j) m i (c • x) i_1 : (a : κ i_1) → M i_1 a) (p i_1)) =
    HSMul.hSMul (β := N p) c
      ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
        (Function.update (β := fun (i : ι) ↦ Π₀ (j : κ i), M i j) m i x i_1 : (a : κ i_1) → M i_1 a) (p i_1))
have simp_rw₁ : ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
    Function.update (β := fun (i : ι) ↦ M i (p i)) (fun (k : ι) ↦ (m k : (a : κ k) → M k a) (p k)) i
      (HSMul.hSMul (β := M i (p i)) c ((x : (a : κ i) → M i a) (p i))) i_1) =
  HSMul.hSMul (β := N p) c
    ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
      Function.update (β := fun (i : ι) ↦ M i (p i)) (fun (k : ι) ↦ (m k : (a : κ k) → M k a) (p k)) i
        ((x : (a : κ i) → M i a) (p i) : M i (p i)) i_1)
Tactic: simp_rw [Function.apply_update (fun i m => m (p i)) m, DFinsupp.smul_apply,
      (f p).map_update_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.DFinsupp (goal)
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : Semiring R
inst_3 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_4 : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst_5 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_6 : (p : (i : ι) → κ i) → Module.{uR, uN} R (N p)
inst_7 : (i : ι) → DecidableEq (κ i)
inst_8 : (i : ι) → (j : κ i) → (x : M i j) → Decidable (x ≠ 0)
inst_9 : (i : (i : ι) → κ i) → (x : N i) → Decidable (x ≠ 0)
f : (p : (i : ι) → κ i) → MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) (N p)
x : (i : ι) → Π₀ (j : κ i), M i j
p : (i : ι) → κ i
hp :
  Membership.mem (γ := Finset ((i : ι) → κ i))
    (DFinsupp.support (β := N)
      ((dfinsuppFamily (κ := κ) (M := M) (N := N) f : (a : (i : ι) → Π₀ (j : κ i), M i j) → Π₀ (t : (i : ι) → κ i), N t)
        x))
    p
⊢ Membership.mem (γ := Finset ((i : ι) → κ i)) (Fintype.piFinset (δ := κ) fun (i : ι) ↦ (x i).support (β := M i)) p
have simp : ∀
  (hp :
    ¬Eq.{uN + 1} (α := N p) ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i : ι) ↦ (x i : (a : κ i) → M i a) (p i)) 0)
  (a : ι), ¬Eq (α := M a (p a)) ((x a : (a_1 : κ a) → M a a_1) (p a)) 0
Tactic: simp only [DFinsupp.mem_support_toFun, dfinsuppFamily_apply_toFun, ne_eq,
    Fintype.mem_piFinset] at hp ⊢
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.DFinsupp (goal)
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : Semiring R
inst_3 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_4 : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst_5 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_6 : (p : (i : ι) → κ i) → Module.{uR, uN} R (N p)
inst_7 : (i : ι) → DecidableEq (κ i)
f : (p : (i : ι) → κ i) → MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) (N p)
p : (i : ι) → κ i
m : (i : ι) → M i (p i)
⊢ Eq (α := Π₀ (t : (i : ι) → κ i), N t)
    ((dfinsuppFamily (κ := κ) (M := M) (N := N) f : (a : (i : ι) → Π₀ (j : κ i), M i j) → Π₀ (t : (i : ι) → κ i), N t)
      fun (i : ι) ↦ DFinsupp.single (β := M i) (p i) (m i))
    (DFinsupp.single (β := N) p ((f p : (a : (i : ι) → M i (p i)) → N p) m))
have h : ∀ (q : (i : ι) → κ i),
  ((dfinsuppFamily (κ := κ) (M := M) (N := N) f : (a : (i : ι) → Π₀ (j : κ i), M i j) → Π₀ (t : (i : ι) → κ i), N t)
          fun (i : ι) ↦ DFinsupp.single (β := M i) (p i) (m i) :
        (a : (i : ι) → κ i) → N a)
      q =
    (DFinsupp.single (β := N) p ((f p : (a : (i : ι) → M i (p i)) → N p) m) : (a : (i : ι) → κ i) → N a) q
Tactic: ext q
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.DFinsupp (goal)
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : Semiring R
inst_3 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_4 : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst_5 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_6 : (p : (i : ι) → κ i) → Module.{uR, uN} R (N p)
inst_7 : (i : ι) → DecidableEq (κ i)
f : (p : (i : ι) → κ i) → MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) (N p)
p : (i : ι) → κ i
m : (i : ι) → M i (p i)
q : (i : ι) → κ i
⊢ ((dfinsuppFamily (κ := κ) (M := M) (N := N) f : (a : (i : ι) → Π₀ (j : κ i), M i j) → Π₀ (t : (i : ι) → κ i), N t)
          fun (i : ι) ↦ DFinsupp.single (β := M i) (p i) (m i) :
        (a : (i : ι) → κ i) → N a)
      q =
    (DFinsupp.single (β := N) p ((f p : (a : (i : ι) → M i (p i)) → N p) m) : (a : (i : ι) → κ i) → N a) q
have h : ∀ (m : (i : ι) → M i (q i)),
  ((dfinsuppFamily (κ := κ) (M := M) (N := N) f : (a : (i : ι) → Π₀ (j : κ i), M i j) → Π₀ (t : (i : ι) → κ i), N t)
          fun (i : ι) ↦ DFinsupp.single (β := M i) (q i) (m i) :
        (a : (i : ι) → κ i) → N a)
      q =
    (DFinsupp.single (β := N) q ((f q : (a : (i : ι) → M i (q i)) → N q) m) : (a : (i : ι) → κ i) → N a) q
Tactic: obtain rfl | hpq := eq_or_ne q p
Cleared hypotheses: p, m
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.DFinsupp (goal)
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : Semiring R
inst_3 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_4 : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst_5 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_6 : (p : (i : ι) → κ i) → Module.{uR, uN} R (N p)
inst_7 : (i : ι) → DecidableEq (κ i)
f : (p : (i : ι) → κ i) → MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) (N p)
p : (i : ι) → κ i
m : (i : ι) → M i (p i)
q : (i : ι) → κ i
h :
  ∀ (m : (i : ι) → M i (q i)),
    ((dfinsuppFamily (κ := κ) (M := M) (N := N) f : (a : (i : ι) → Π₀ (j : κ i), M i j) → Π₀ (t : (i : ι) → κ i), N t)
            fun (i : ι) ↦ DFinsupp.single (β := M i) (q i) (m i) :
          (a : (i : ι) → κ i) → N a)
        q =
      (DFinsupp.single (β := N) q ((f q : (a : (i : ι) → M i (q i)) → N q) m) : (a : (i : ι) → κ i) → N a) q
⊢ ((dfinsuppFamily (κ := κ) (M := M) (N := N) f : (a : (i : ι) → Π₀ (j : κ i), M i j) → Π₀ (t : (i : ι) → κ i), N t)
          fun (i : ι) ↦ DFinsupp.single (β := M i) (p i) (m i) :
        (a : (i : ι) → κ i) → N a)
      q =
    (DFinsupp.single (β := N) p ((f p : (a : (i : ι) → M i (p i)) → N p) m) : (a : (i : ι) → κ i) → N a) q
have h₁ : ∀ (hpq : q ≠ p),
  ((dfinsuppFamily (κ := κ) (M := M) (N := N) f : (a : (i : ι) → Π₀ (j : κ i), M i j) → Π₀ (t : (i : ι) → κ i), N t)
          fun (i : ι) ↦ DFinsupp.single (β := M i) (p i) (m i) :
        (a : (i : ι) → κ i) → N a)
      q =
    (DFinsupp.single (β := N) p ((f p : (a : (i : ι) → M i (p i)) → N p) m) : (a : (i : ι) → κ i) → N a) q
Tactic: obtain rfl | hpq := eq_or_ne q p
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.DFinsupp (goal)
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : Semiring R
inst_3 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_4 : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst_5 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_6 : (p : (i : ι) → κ i) → Module.{uR, uN} R (N p)
inst_7 : (i : ι) → DecidableEq (κ i)
f : (p : (i : ι) → κ i) → MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) (N p)
p : (i : ι) → κ i
m : (i : ι) → M i (p i)
q : (i : ι) → κ i
hpq : q ≠ p
⊢ ((dfinsuppFamily (κ := κ) (M := M) (N := N) f : (a : (i : ι) → Π₀ (j : κ i), M i j) → Π₀ (t : (i : ι) → κ i), N t)
          fun (i : ι) ↦ DFinsupp.single (β := M i) (p i) (m i) :
        (a : (i : ι) → κ i) → N a)
      q =
    (DFinsupp.single (β := N) p ((f p : (a : (i : ι) → M i (p i)) → N p) m) : (a : (i : ι) → κ i) → N a) q
have h : ((dfinsuppFamily (κ := κ) (M := M) (N := N) f : (a : (i : ι) → Π₀ (j : κ i), M i j) → Π₀ (t : (i : ι) → κ i), N t)
        fun (i : ι) ↦ DFinsupp.single (β := M i) (p i) (m i) :
      (a : (i : ι) → κ i) → N a)
    q =
  0
Tactic: rw [DFinsupp.single_eq_of_ne hpq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.DFinsupp (hypothesis)
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : Semiring R
inst_3 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_4 : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst_5 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_6 : (p : (i : ι) → κ i) → Module.{uR, uN} R (N p)
inst_7 : (i : ι) → DecidableEq (κ i)
f : (p : (i : ι) → κ i) → MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) (N p)
p : (i : ι) → κ i
m : (i : ι) → M i (p i)
q : (i : ι) → κ i
hpq : q ≠ p
⊢ ((dfinsuppFamily (κ := κ) (M := M) (N := N) f : (a : (i : ι) → Π₀ (j : κ i), M i j) → Π₀ (t : (i : ι) → κ i), N t)
          fun (i : ι) ↦ DFinsupp.single (β := M i) (p i) (m i) :
        (a : (i : ι) → κ i) → N a)
      q =
    0
have hpq₁ : ∃ (a : ι), q a ≠ p a
Tactic: rw [Function.ne_iff] at hpq
Cleared hypotheses: hpq
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.DFinsupp (goal)
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : Semiring R
inst_3 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_4 : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst_5 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_6 : (p : (i : ι) → κ i) → Module.{uR, uN} R (N p)
inst_7 : (i : ι) → DecidableEq (κ i)
f : (p : (i : ι) → κ i) → MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) (N p)
p : (i : ι) → κ i
m : (i : ι) → M i (p i)
q : (i : ι) → κ i
hpq : ∃ (a : ι), q a ≠ p a
⊢ ((dfinsuppFamily (κ := κ) (M := M) (N := N) f : (a : (i : ι) → Π₀ (j : κ i), M i j) → Π₀ (t : (i : ι) → κ i), N t)
          fun (i : ι) ↦ DFinsupp.single (β := M i) (p i) (m i) :
        (a : (i : ι) → κ i) → N a)
      q =
    0
have h : ∀ (i : ι) (hpqi : q i ≠ p i),
  ((dfinsuppFamily (κ := κ) (M := M) (N := N) f : (a : (i : ι) → Π₀ (j : κ i), M i j) → Π₀ (t : (i : ι) → κ i), N t)
          fun (i : ι) ↦ DFinsupp.single (β := M i) (p i) (m i) :
        (a : (i : ι) → κ i) → N a)
      q =
    0
Tactic: obtain ⟨i, hpqi⟩ := hpq
Cleared hypotheses: hpq
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.DFinsupp (goal)
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : Semiring R
inst_3 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_4 : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst_5 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_6 : (p : (i : ι) → κ i) → Module.{uR, uN} R (N p)
inst_7 : (i : ι) → DecidableEq (κ i)
f : (p : (i : ι) → κ i) → MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) (N p)
p : (i : ι) → κ i
m : (i : ι) → M i (p i)
q : (i : ι) → κ i
i : ι
hpqi : q i ≠ p i
⊢ ((dfinsuppFamily (κ := κ) (M := M) (N := N) f : (a : (i : ι) → Π₀ (j : κ i), M i j) → Π₀ (t : (i : ι) → κ i), N t)
          fun (i : ι) ↦ DFinsupp.single (β := M i) (p i) (m i) :
        (a : (i : ι) → κ i) → N a)
      q =
    0
have h : Eq (α := M i (q i))
  (((fun (i : ι) ↦ (DFinsupp.single (β := M i) (p i) (m i) : Π₀ (i_1 : κ i), M i i_1)) i : (a : κ i) → M i a) (q i)) 0
Tactic: apply (f q).map_coord_zero i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.DFinsupp (goal)
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : Semiring R
inst_3 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_4 : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst_5 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_6 : (p : (i : ι) → κ i) → Module.{uR, uN} R (N p)
inst_7 : (i : ι) → DecidableEq (κ i)
p : (i : ι) → κ i
f : MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) (N p)
x : (i : ι) → Π₀ (j : κ i), M i j
⊢ Eq (α := Π₀ (t : (i : ι) → κ i), N t)
    ((dfinsuppFamily (κ := κ) (M := M) (N := N)
            (Pi.single (M := fun (p : (i : ι) → κ i) ↦
              MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) (N p)) p f) :
          (a : (i : ι) → Π₀ (j : κ i), M i j) → Π₀ (t : (i : ι) → κ i), N t)
        x :
      Π₀ (t : (i : ι) → κ i), N t)
    (DFinsupp.single (β := N) p ((f : (a : (i : ι) → M i (p i)) → N p) fun (i : ι) ↦ (x i : (a : κ i) → M i a) (p i)) :
      Π₀ (i : (i : ι) → κ i), N i)
have h : ∀ (p' : (i : ι) → κ i),
  (((dfinsuppFamily (κ := κ) (M := M) (N := N)
                (Pi.single (M := fun (p : (i : ι) → κ i) ↦
                  MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) (N p)) p f) :
              (a : (i : ι) → Π₀ (j : κ i), M i j) → Π₀ (t : (i : ι) → κ i), N t)
            x :
          Π₀ (t : (i : ι) → κ i), N t) :
        (a : (i : ι) → κ i) → N a)
      p' =
    (DFinsupp.single (β := N) p ((f : (a : (i : ι) → M i (p i)) → N p) fun (i : ι) ↦ (x i : (a : κ i) → M i a) (p i)) :
        (a : (i : ι) → κ i) → N a)
      p'
Tactic: ext p'