awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
c : M →₀ R
cs : (↑c.support : Set M) ⊆ s
h : Membership.mem (γ := Submodule R M) (span R s) (c.sum fun (mi : M) (r : R) ↦ r • mi)
A : ↥c.support ≃ Fin c.support.card
⊢ ∃ (n : ℕ) (f : Fin n → R) (g : Fin n → (↑s : Type u_2)),
    Eq (α := M) (∑ i : Fin n, f i • (↑(g i) : M)) (c.sum fun (mi : M) (r : R) ↦ r • mi)
have refine_1 : Eq (α := M)
  (∑ i : Fin c.support.card,
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M)
      ((fun (i : Fin c.support.card) ↦
          ((c : (a : M) → R) (↑((A.symm : (a : Fin c.support.card) → ↥c.support) i) : M) : R))
        i)
      (↑((fun (i : Fin c.support.card) ↦
              Subtype.mk (p := fun (x : M) ↦ x ∈ s) (↑((A.symm : (a : Fin c.support.card) → ↥c.support) i) : M) sorry)
            i) :
        M))
  (c.sum fun (mi : M) (r : R) ↦ r • mi)
Tactic: refine ⟨_, fun i ↦ c (A.symm i), fun i ↦ ⟨A.symm i, cs (A.symm i).2⟩, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
c : M →₀ R
cs : (↑c.support : Set M) ⊆ s
h : Membership.mem (γ := Submodule R M) (span R s) (c.sum fun (mi : M) (r : R) ↦ r • mi)
A : ↥c.support ≃ Fin c.support.card
⊢ Eq (α := M)
    (∑ i : Fin c.support.card,
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M)
        ((fun (i : Fin c.support.card) ↦
            ((c : (a : M) → R) (↑((A.symm : (a : Fin c.support.card) → ↥c.support) i) : M) : R))
          i)
        (↑((fun (i : Fin c.support.card) ↦
                Subtype.mk (p := fun (x : M) ↦ x ∈ s) (↑((A.symm : (a : Fin c.support.card) → ↥c.support) i) : M) ⋯)
              i) :
          M))
    (c.sum fun (mi : M) (r : R) ↦ r • mi)
have refine_1 : Eq.{u_2 + 1} (α := M)
  (∑ i : Fin c.support.card,
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M)
      ((fun (i : Fin c.support.card) ↦
          ((c : (a : M) → R) (↑((A.symm : (a : Fin c.support.card) → ↥c.support) i) : M) : R))
        i)
      (↑((fun (i : Fin c.support.card) ↦
              Subtype.mk (p := fun (x : M) ↦ x ∈ s) (↑((A.symm : (a : Fin c.support.card) → ↥c.support) i) : M) sorry)
            i) :
        M))
  (∑ i : ↥c.support, HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((c : (a : M) → R) (↑i : M) : R) (↑i : M))
Tactic: rw [Finsupp.sum, ← Finset.sum_coe_sort c.support]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
⊢ (↑(span R s) : Set M) =
    ⋃ (n : ℕ),
      (fun (f : Fin n → R × M) ↦ ∑ i : Fin n, (f i).1 • (f i).2) '' {f : Fin n → R × M | ∀ (i : Fin n), (f i).2 ∈ s}
have h : ∀ (m : M),
  m ∈ (↑(span R s) : Set M) ↔
    Membership.mem (γ := Set M)
      (⋃ (n : ℕ),
        (fun (f : Fin n → R × M) ↦ ∑ i : Fin n, (f i).1 • (f i).2) '' {f : Fin n → R × M | ∀ (i : Fin n), (f i).2 ∈ s})
      m
Tactic: ext m
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
m : M
⊢ m ∈ (↑(span R s) : Set M) ↔
    Membership.mem (γ := Set M)
      (⋃ (n : ℕ),
        (fun (f : Fin n → R × M) ↦ ∑ i : Fin n, (f i).1 • (f i).2) '' {f : Fin n → R × M | ∀ (i : Fin n), (f i).2 ∈ s})
      m
have h : (∃ (n : ℕ) (f : Fin n → R) (g : Fin n → (↑s : Type u_2)), ∑ i : Fin n, f i • (↑(g i) : M) = m) ↔
  ∃ (i : ℕ) (x : Fin i → R × M), (∀ (i : Fin i), (x i).2 ∈ s) ∧ ∑ i : Fin i, (x i).1 • (x i).2 = m
Tactic: simp only [SetLike.mem_coe, mem_iUnion, mem_image, mem_setOf_eq, mem_span_set']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
m : M
⊢ (∃ (n : ℕ) (f : Fin n → R) (g : Fin n → (↑s : Type u_2)), ∑ i : Fin n, f i • (↑(g i) : M) = m) ↔
    ∃ (i : ℕ) (x : Fin i → R × M), (∀ (i : Fin i), (x i).2 ∈ s) ∧ ∑ i : Fin i, (x i).1 • (x i).2 = m
have h : ∀ (n : ℕ),
  (∃ (f : Fin n → R) (g : Fin n → (↑s : Type u_2)), ∑ i : Fin n, f i • (↑(g i) : M) = m) →
    ∃ (x : Fin n → R × M), (∀ (i : Fin n), (x i).2 ∈ s) ∧ ∑ i : Fin n, (x i).1 • (x i).2 = m
Tactic: refine exists_congr (fun n ↦ ⟨?_, ?_⟩)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
m : M
h :
  ∀ (n : ℕ),
    (∃ (f : Fin n → R) (g : Fin n → (↑s : Type u_2)), ∑ i : Fin n, f i • (↑(g i) : M) = m) →
      ∃ (x : Fin n → R × M), (∀ (i : Fin n), (x i).2 ∈ s) ∧ ∑ i : Fin n, (x i).1 • (x i).2 = m
⊢ (∃ (n : ℕ) (f : Fin n → R) (g : Fin n → (↑s : Type u_2)), ∑ i : Fin n, f i • (↑(g i) : M) = m) ↔
    ∃ (i : ℕ) (x : Fin i → R × M), (∀ (i : Fin i), (x i).2 ∈ s) ∧ ∑ i : Fin i, (x i).1 • (x i).2 = m
have h₁ : ∀ (n : ℕ),
  (∃ (x : Fin n → R × M), (∀ (i : Fin n), (x i).2 ∈ s) ∧ ∑ i : Fin n, (x i).1 • (x i).2 = m) →
    ∃ (f : Fin n → R) (g : Fin n → (↑s : Type u_2)), ∑ i : Fin n, f i • (↑(g i) : M) = m
Tactic: refine exists_congr (fun n ↦ ⟨?_, ?_⟩)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
Goal:
R_1 : Type u_1
M_1 : Type u_2
N : Type u_3
inst : Semiring R_1
inst_1 : AddCommMonoid M_1
inst_2 : Module R_1 M_1
inst_3 : AddCommMonoid N
inst_4 : Module R_1 N
R : Type u_4
M : Type u_5
ι : Type u_6
inst_5 : Ring R
inst_6 : AddCommGroup M
inst_7 : Module R M
i : ι
c : ι → R
h₀ : c i = 0
⊢ (ι →₀ R) ≃ₗ[R] ι →₀ R
have refine_1 : Eq (α := (ι →₀ R) →ₗ[R] ι →₀ R)
  ((linearCombination R fun (j : ι) ↦ HAdd.hAdd (α := ι →₀ R) (single j 1) (single i (c j))) ∘ₗ
    linearCombination R fun (j : ι) ↦ HSub.hSub (α := ι →₀ R) (single j 1) (single i (c j)))
  LinearMap.id
Tactic: refine .ofLinear (linearCombination _ fun j ↦ single j 1 + single i (c j))
    (linearCombination _ fun j ↦ single j 1 - single i (c j)) ?_ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
Goal:
R_1 : Type u_1
M_1 : Type u_2
N : Type u_3
inst : Semiring R_1
inst_1 : AddCommMonoid M_1
inst_2 : Module R_1 M_1
inst_3 : AddCommMonoid N
inst_4 : Module R_1 N
R : Type u_4
M : Type u_5
ι : Type u_6
inst_5 : Ring R
inst_6 : AddCommGroup M
inst_7 : Module R M
i : ι
c : ι → R
h₀ : c i = 0
refine_1 :
  Eq (α := (ι →₀ R) →ₗ[R] ι →₀ R)
    ((linearCombination R fun (j : ι) ↦ HAdd.hAdd (α := ι →₀ R) (single j 1) (single i (c j))) ∘ₗ
      linearCombination R fun (j : ι) ↦ HSub.hSub (α := ι →₀ R) (single j 1) (single i (c j)))
    LinearMap.id
⊢ (ι →₀ R) ≃ₗ[R] ι →₀ R
have refine_2 : Eq (α := (ι →₀ R) →ₗ[R] ι →₀ R)
  ((linearCombination R fun (j : ι) ↦ HSub.hSub (α := ι →₀ R) (single j 1) (single i (c j))) ∘ₗ
    linearCombination R fun (j : ι) ↦ HAdd.hAdd (α := ι →₀ R) (single j 1) (single i (c j)))
  LinearMap.id
Tactic: refine .ofLinear (linearCombination _ fun j ↦ single j 1 + single i (c j))
    (linearCombination _ fun j ↦ single j 1 - single i (c j)) ?_ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
Goal:
R_1 : Type u_1
M_1 : Type u_2
N : Type u_3
inst : Semiring R_1
inst_1 : AddCommMonoid M_1
inst_2 : Module R_1 M_1
inst_3 : AddCommMonoid N
inst_4 : Module R_1 N
R : Type u_4
M : Type u_5
ι : Type u_6
inst_5 : Ring R
inst_6 : AddCommGroup M
inst_7 : Module R M
i : ι
c : ι → R
h₀ : c i = 0
⊢ Eq (α := (ι →₀ R) →ₗ[R] ι →₀ R)
    ((linearCombination R fun (j : ι) ↦ HAdd.hAdd (α := ι →₀ R) (single j 1) (single i (c j))) ∘ₗ
      linearCombination R fun (j : ι) ↦ HSub.hSub (α := ι →₀ R) (single j 1) (single i (c j)))
    LinearMap.id
have refine_1 : ∀ (j k : ι),
  Eq.{u_4 + 1} (α := R)
    (((((linearCombination R fun (j : ι) ↦ HAdd.hAdd (α := ι →₀ R) (single j 1) (single i (c j))) ∘ₗ
                  linearCombination R fun (j : ι) ↦ HSub.hSub (α := ι →₀ R) (single j 1) (single i (c j))) ∘ₗ
                lsingle j :
              (a : R) → ι →₀ R)
            1 :
          (a : ι) → R)
        k :
      R)
    (((LinearMap.id ∘ₗ lsingle j : (a : R) → ι →₀ R) 1 : (a : ι) → R) k : R)
Tactic: ext j k
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
Goal:
R_1 : Type u_1
M_1 : Type u_2
N : Type u_3
inst : Semiring R_1
inst_1 : AddCommMonoid M_1
inst_2 : Module R_1 M_1
inst_3 : AddCommMonoid N
inst_4 : Module R_1 N
R : Type u_4
M : Type u_5
ι : Type u_6
inst_5 : Ring R
inst_6 : AddCommGroup M
inst_7 : Module R M
i : ι
c : ι → R
h₀ : c i = 0
⊢ Eq (α := (ι →₀ R) →ₗ[R] ι →₀ R)
    ((linearCombination R fun (j : ι) ↦ HSub.hSub (α := ι →₀ R) (single j 1) (single i (c j))) ∘ₗ
      linearCombination R fun (j : ι) ↦ HAdd.hAdd (α := ι →₀ R) (single j 1) (single i (c j)))
    LinearMap.id
have refine_2 : ∀ (j k : ι),
  Eq.{u_4 + 1} (α := R)
    (((((linearCombination R fun (j : ι) ↦ HSub.hSub (α := ι →₀ R) (single j 1) (single i (c j))) ∘ₗ
                  linearCombination R fun (j : ι) ↦ HAdd.hAdd (α := ι →₀ R) (single j 1) (single i (c j))) ∘ₗ
                lsingle j :
              (a : R) → ι →₀ R)
            1 :
          (a : ι) → R)
        k :
      R)
    (((LinearMap.id ∘ₗ lsingle j : (a : R) → ι →₀ R) 1 : (a : ι) → R) k : R)
Tactic: ext j k
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
Goal:
R_1 : Type u_1
M_1 : Type u_2
N : Type u_3
inst : Semiring R_1
inst_1 : AddCommMonoid M_1
inst_2 : Module R_1 M_1
inst_3 : AddCommMonoid N
inst_4 : Module R_1 N
R : Type u_4
M : Type u_5
ι : Type u_6
inst_5 : Ring R
inst_6 : AddCommGroup M
inst_7 : Module R M
i : ι
c : ι → R
h₀ : c i = 0
j k : ι
⊢ Eq.{u_4 + 1} (α := R)
    (((((linearCombination R fun (j : ι) ↦ HAdd.hAdd (α := ι →₀ R) (single j 1) (single i (c j))) ∘ₗ
                  linearCombination R fun (j : ι) ↦ HSub.hSub (α := ι →₀ R) (single j 1) (single i (c j))) ∘ₗ
                lsingle j :
              (a : R) → ι →₀ R)
            1 :
          (a : ι) → R)
        k :
      R)
    (((LinearMap.id ∘ₗ lsingle j : (a : R) → ι →₀ R) 1 : (a : ι) → R) k : R)
have refine_1 : Eq.{u_4 + 1} (α := R)
  (((((linearCombination R fun (j : ι) ↦ HAdd.hAdd (α := ι →₀ R) (single j 1) (single i (c j))) ∘ₗ
                linearCombination R fun (j : ι) ↦ HSub.hSub (α := ι →₀ R) (single j 1) (single i (c j))) ∘ₗ
              lsingle j :
            (a : R) → ι →₀ R)
          1 :
        (a : ι) → R)
      i :
    R)
  (((LinearMap.id ∘ₗ lsingle j : (a : R) → ι →₀ R) 1 : (a : ι) → R) i : R)
Tactic: obtain rfl | hk := eq_or_ne i k
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
Goal:
R_1 : Type u_1
M_1 : Type u_2
N : Type u_3
inst : Semiring R_1
inst_1 : AddCommMonoid M_1
inst_2 : Module R_1 M_1
inst_3 : AddCommMonoid N
inst_4 : Module R_1 N
R : Type u_4
M : Type u_5
ι : Type u_6
inst_5 : Ring R
inst_6 : AddCommGroup M
inst_7 : Module R M
i : ι
c : ι → R
h₀ : c i = 0
j k : ι
refine_1 :
  Eq.{u_4 + 1} (α := R)
    (((((linearCombination R fun (j : ι) ↦ HAdd.hAdd (α := ι →₀ R) (single j 1) (single i (c j))) ∘ₗ
                  linearCombination R fun (j : ι) ↦ HSub.hSub (α := ι →₀ R) (single j 1) (single i (c j))) ∘ₗ
                lsingle j :
              (a : R) → ι →₀ R)
            1 :
          (a : ι) → R)
        i :
      R)
    (((LinearMap.id ∘ₗ lsingle j : (a : R) → ι →₀ R) 1 : (a : ι) → R) i : R)
⊢ Eq.{u_4 + 1} (α := R)
    (((((linearCombination R fun (j : ι) ↦ HAdd.hAdd (α := ι →₀ R) (single j 1) (single i (c j))) ∘ₗ
                  linearCombination R fun (j : ι) ↦ HSub.hSub (α := ι →₀ R) (single j 1) (single i (c j))) ∘ₗ
                lsingle j :
              (a : R) → ι →₀ R)
            1 :
          (a : ι) → R)
        k :
      R)
    (((LinearMap.id ∘ₗ lsingle j : (a : R) → ι →₀ R) 1 : (a : ι) → R) k : R)
have refine_1₁ : ∀ (hk : i ≠ k),
  Eq.{u_4 + 1} (α := R)
    (((((linearCombination R fun (j : ι) ↦ HAdd.hAdd (α := ι →₀ R) (single j 1) (single i (c j))) ∘ₗ
                  linearCombination R fun (j : ι) ↦ HSub.hSub (α := ι →₀ R) (single j 1) (single i (c j))) ∘ₗ
                lsingle j :
              (a : R) → ι →₀ R)
            1 :
          (a : ι) → R)
        k :
      R)
    (((LinearMap.id ∘ₗ lsingle j : (a : R) → ι →₀ R) 1 : (a : ι) → R) k : R)
Tactic: obtain rfl | hk := eq_or_ne i k
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
Goal:
R_1 : Type u_1
M_1 : Type u_2
N : Type u_3
inst : Semiring R_1
inst_1 : AddCommMonoid M_1
inst_2 : Module R_1 M_1
inst_3 : AddCommMonoid N
inst_4 : Module R_1 N
R : Type u_4
M : Type u_5
ι : Type u_6
inst_5 : Ring R
inst_6 : AddCommGroup M
inst_7 : Module R M
i : ι
c : ι → R
h₀ : c i = 0
j k : ι
⊢ Eq.{u_4 + 1} (α := R)
    (((((linearCombination R fun (j : ι) ↦ HSub.hSub (α := ι →₀ R) (single j 1) (single i (c j))) ∘ₗ
                  linearCombination R fun (j : ι) ↦ HAdd.hAdd (α := ι →₀ R) (single j 1) (single i (c j))) ∘ₗ
                lsingle j :
              (a : R) → ι →₀ R)
            1 :
          (a : ι) → R)
        k :
      R)
    (((LinearMap.id ∘ₗ lsingle j : (a : R) → ι →₀ R) 1 : (a : ι) → R) k : R)
have refine_2 : Eq.{u_4 + 1} (α := R)
  (((((linearCombination R fun (j : ι) ↦ HSub.hSub (α := ι →₀ R) (single j 1) (single i (c j))) ∘ₗ
                linearCombination R fun (j : ι) ↦ HAdd.hAdd (α := ι →₀ R) (single j 1) (single i (c j))) ∘ₗ
              lsingle j :
            (a : R) → ι →₀ R)
          1 :
        (a : ι) → R)
      i :
    R)
  (((LinearMap.id ∘ₗ lsingle j : (a : R) → ι →₀ R) 1 : (a : ι) → R) i : R)
Tactic: obtain rfl | hk := eq_or_ne i k
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
Goal:
R_1 : Type u_1
M_1 : Type u_2
N : Type u_3
inst : Semiring R_1
inst_1 : AddCommMonoid M_1
inst_2 : Module R_1 M_1
inst_3 : AddCommMonoid N
inst_4 : Module R_1 N
R : Type u_4
M : Type u_5
ι : Type u_6
inst_5 : Ring R
inst_6 : AddCommGroup M
inst_7 : Module R M
i : ι
c : ι → R
h₀ : c i = 0
j k : ι
refine_2 :
  Eq.{u_4 + 1} (α := R)
    (((((linearCombination R fun (j : ι) ↦ HSub.hSub (α := ι →₀ R) (single j 1) (single i (c j))) ∘ₗ
                  linearCombination R fun (j : ι) ↦ HAdd.hAdd (α := ι →₀ R) (single j 1) (single i (c j))) ∘ₗ
                lsingle j :
              (a : R) → ι →₀ R)
            1 :
          (a : ι) → R)
        i :
      R)
    (((LinearMap.id ∘ₗ lsingle j : (a : R) → ι →₀ R) 1 : (a : ι) → R) i : R)
⊢ Eq.{u_4 + 1} (α := R)
    (((((linearCombination R fun (j : ι) ↦ HSub.hSub (α := ι →₀ R) (single j 1) (single i (c j))) ∘ₗ
                  linearCombination R fun (j : ι) ↦ HAdd.hAdd (α := ι →₀ R) (single j 1) (single i (c j))) ∘ₗ
                lsingle j :
              (a : R) → ι →₀ R)
            1 :
          (a : ι) → R)
        k :
      R)
    (((LinearMap.id ∘ₗ lsingle j : (a : R) → ι →₀ R) 1 : (a : ι) → R) k : R)
have refine_2₁ : ∀ (hk : i ≠ k),
  Eq.{u_4 + 1} (α := R)
    (((((linearCombination R fun (j : ι) ↦ HSub.hSub (α := ι →₀ R) (single j 1) (single i (c j))) ∘ₗ
                  linearCombination R fun (j : ι) ↦ HAdd.hAdd (α := ι →₀ R) (single j 1) (single i (c j))) ∘ₗ
                lsingle j :
              (a : R) → ι →₀ R)
            1 :
          (a : ι) → R)
        k :
      R)
    (((LinearMap.id ∘ₗ lsingle j : (a : R) → ι →₀ R) 1 : (a : ι) → R) k : R)
Tactic: obtain rfl | hk := eq_or_ne i k
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
Goal:
R : Type u_4
M : Type u_5
ι : Type u_6
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
i : ι
c : ι → R
h₀ : c i = 0
v : ι → M
⊢ Eq (α := (ι →₀ R) →ₗ[R] M) (linearCombination R v ∘ₗ (↑(addSingleEquiv i c h₀) : (ι →₀ R) →ₗ[R] ι →₀ R))
    (linearCombination R (v + fun (x : ι) ↦ c x • v i))
have h : ∀ (a : ι),
  Eq.{u_5 + 1} (α := M)
    (((linearCombination R v ∘ₗ (↑(addSingleEquiv i c h₀) : (ι →₀ R) →ₗ[R] ι →₀ R)) ∘ₗ lsingle a : (a : R) → M) 1 : M)
    ((linearCombination R (v + fun (x : ι) ↦ c x • v i) ∘ₗ lsingle a : (a : R) → M) 1 : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Pi (goal)
Goal:
R : Type u_1
M : Type u_4
inst : AddCommMonoid M
inst_1 : Semiring R
inst_2 : Module R M
α : Type u_5
inst_3 : Unique α
m : M
⊢ Eq (α := α →₀ M) ((LinearEquiv.symm (finsuppUnique R M α) : (a : M) → α →₀ M) m : α →₀ M) (single default m : α →₀ M)
have h : Eq.{u_4 + 1} (α := M)
  ((((LinearEquiv.symm (finsuppUnique R M α) : (a : M) → α →₀ M) m : α →₀ M) : (a : α) → M) default : M)
  ((single default m : (a : α) → M) default : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Pi (goal)
Goal:
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
R : Type u_5
S : Type u_6
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : AddCommMonoid P
inst_7 : Module R P
x y : α →₀ M
⊢ (⇑(x + y) : (a : α) → M) = HAdd.hAdd (α := α → M) (⇑x : (a : α) → M) (⇑y : (a : α) → M)
have h : ∀ (x_1 : α), (x + y : (a : α) → M) x_1 = HAdd.hAdd (α := α → M) (β := α → M) (⇑x : (a : α) → M) (⇑y : (a : α) → M) x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Pi (goal)
Goal:
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
R : Type u_5
S : Type u_6
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : AddCommMonoid P
inst_7 : Module R P
x : R
y : α →₀ M
⊢ (⇑(x • y) : (a : α) → M) = HSMul.hSMul (α := R) (β := α → M) ((RingHom.id R : (a : R) → R) x : R) (⇑y : (a : α) → M)
have h : ∀ (x_1 : α),
  (x • y : (a : α) → M) x_1 =
    HSMul.hSMul (α := R) (β := α → M) ((RingHom.id R : (a : R) → R) x : R) (⇑y : (a : α) → M) x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Pi (goal)
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : DecidableEq α
x : α
⊢ Eq (α := M →ₗ[R] α → M) (lcoeFun ∘ₗ lsingle x) (LinearMap.single.{u_5, u_1, u_2} R (fun (x : α) ↦ M) x)
have h : ∀ (x_1 : M) (x_2 : α),
  Eq.{u_2 + 1} (α := M) ((lcoeFun ∘ₗ lsingle x : (a : M) → α → M) x_1 x_2 : M)
    (((LinearMap.single.{u_5, u_1, u_2} R (fun (x : α) ↦ M) x : M →ₗ[R] (i : α) → M) : (a : M) → α → M) x_1 x_2 : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Pi (goal)
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid P
inst_4 : Module R P
f : P × M →ₗ[R] M
x : ℕ →₀ P
⊢ Eq (α := P) (((f.prodOfFinsuppNat : (a : ℕ →₀ P) → P × M) x).1 : P) ((x : (a : ℕ) → P) 0 : P)
have simp_rw : Eq (α := P)
  (∑ c ∈ x.support,
      ((HPow.hPow (α := P × M →ₗ[R] P × M) (inr R P M ∘ₗ f) c ∘ₗ inl R P M : (a : P) → P × M) ((x : (a : ℕ) → P) c)).1 :
    P)
  ((x : (a : ℕ) → P) 0 : P)
Tactic: simp_rw [prodOfFinsuppNat, coe_lsum, sum, Prod.fst_sum]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Pi (goal)
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid P
inst_4 : Module R P
f : P × M →ₗ[R] M
x : ℕ →₀ P
⊢ Eq (α := P)
    (∑ c ∈ x.support,
        ((HPow.hPow (α := P × M →ₗ[R] P × M) (inr R P M ∘ₗ f) c ∘ₗ inl R P M : (a : P) → P × M)
            ((x : (a : ℕ) → P) c)).1 :
      P)
    ((x : (a : ℕ) → P) 0 : P)
have rw : Eq (α := P)
  (((HPow.hPow (α := P × M →ₗ[R] P × M) (β := ℕ) (inr R P M ∘ₗ f) 0 ∘ₗ inl R P M : (a : P) → P × M)
        ((x : (a : ℕ) → P) 0)).1 :
    P)
  ((x : (a : ℕ) → P) 0 : P)
Tactic: rw [Finset.sum_eq_single 0 (fun n _ hn ↦ ?_) (by simp)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Pi (goal)
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid P
inst_4 : Module R P
f : P × M →ₗ[R] M
x : ℕ →₀ P
rw :
  Eq (α := P)
    (((HPow.hPow (α := P × M →ₗ[R] P × M) (β := ℕ) (inr R P M ∘ₗ f) 0 ∘ₗ inl R P M : (a : P) → P × M)
          ((x : (a : ℕ) → P) 0)).1 :
      P)
    ((x : (a : ℕ) → P) 0 : P)
⊢ Eq (α := P)
    (∑ c ∈ x.support,
        ((HPow.hPow (α := P × M →ₗ[R] P × M) (inr R P M ∘ₗ f) c ∘ₗ inl R P M : (a : P) → P × M)
            ((x : (a : ℕ) → P) c)).1 :
      P)
    ((x : (a : ℕ) → P) 0 : P)
have rw₁ : ∀ n ∈ x.support,
  ∀ (hn : n ≠ 0),
    Eq.{u_4 + 1} (α := P)
      ((HPow.hPow (α := P × M →ₗ[R] P × M) (inr R P M ∘ₗ f) n ∘ₗ inl R P M : (a : P) → P × M) ((x : (a : ℕ) → P) n)).1 0
Tactic: rw [Finset.sum_eq_single 0 (fun n _ hn ↦ ?_) (by simp)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Pi (goal)
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid P
inst_4 : Module R P
f : P × M →ₗ[R] M
x : ℕ →₀ P
n : ℕ
h : n ∈ x.support
hn : n ≠ 0
⊢ Eq.{u_4 + 1} (α := P)
    ((HPow.hPow (α := P × M →ₗ[R] P × M) (inr R P M ∘ₗ f) n ∘ₗ inl R P M : (a : P) → P × M) ((x : (a : ℕ) → P) n)).1 0
have obtain : ∀ (n : ℕ),
  n.succ ∈ x.support →
    ∀ (hn : n.succ ≠ 0),
      Eq.{u_4 + 1} (α := P)
        ((HPow.hPow (α := P × M →ₗ[R] P × M) (inr R P M ∘ₗ f) n.succ ∘ₗ inl R P M : (a : P) → P × M)
            ((x : (a : ℕ) → P) n.succ)).1
        0
Tactic: obtain ⟨n, rfl⟩ := n.exists_eq_succ_of_ne_zero hn
Cleared hypotheses: n, h, hn
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Pi (goal)
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid P
inst_4 : Module R P
f : P × M →ₗ[R] M
x : ℕ →₀ P
⊢ Eq.{u_2 + 1} (α := M) (((f.prodOfFinsuppNat : (a : ℕ →₀ P) → P × M) x).2 : M)
    ((f : (a : P × M) → M)
        ((f.prodOfFinsuppNat : (a : ℕ →₀ P) → P × M)
            ((comapDomain.addMonoidHom (f := fun (x : ℕ) ↦ x + 1) ⋯ : (a : ℕ →₀ P) → ℕ →₀ P) x) :
          P × M) :
      M)
have simp_rw : Eq.{u_2 + 1} (α := M)
  (∑ c ∈ x.support,
      ((HPow.hPow (α := P × M →ₗ[R] P × M) (inr R P M ∘ₗ f) c ∘ₗ inl R P M : (a : P) → P × M) ((x : (a : ℕ) → P) c)).2 :
    M)
  ((f : (a : P × M) → M)
      (∑
        x_1 ∈
          Finsupp.support.{0, u_4} (M := P)
            ((comapDomain.addMonoidHom (f := fun (x : ℕ) ↦ x + 1) sorry : (a : ℕ →₀ P) → ℕ →₀ P) x),
        (HPow.hPow (α := P × M →ₗ[R] P × M) (inr R P M ∘ₗ f) x_1 ∘ₗ inl R P M : (a : P) → P × M)
          ((((comapDomain.addMonoidHom (f := fun (x : ℕ) ↦ x + 1) sorry : (a : ℕ →₀ P) → ℕ →₀ P) x : ℕ →₀ P) : (a : ℕ) → P)
            x_1)) :
    M)
Tactic: simp_rw [prodOfFinsuppNat, coe_lsum, sum, Prod.snd_sum]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Pi (goal)
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid P
inst_4 : Module R P
f : P × M →ₗ[R] M
x : ℕ →₀ P
⊢ Eq.{u_2 + 1} (α := M)
    (∑ c ∈ x.support,
        ((HPow.hPow (α := P × M →ₗ[R] P × M) (inr R P M ∘ₗ f) c ∘ₗ inl R P M : (a : P) → P × M)
            ((x : (a : ℕ) → P) c)).2 :
      M)
    ((f : (a : P × M) → M)
        (∑
          x_1 ∈
            Finsupp.support.{0, u_4} (M := P)
              ((comapDomain.addMonoidHom (f := fun (x : ℕ) ↦ x + 1) ⋯ : (a : ℕ →₀ P) → ℕ →₀ P) x),
          (HPow.hPow (α := P × M →ₗ[R] P × M) (inr R P M ∘ₗ f) x_1 ∘ₗ inl R P M : (a : P) → P × M)
            ((((comapDomain.addMonoidHom (f := fun (x : ℕ) ↦ x + 1) ⋯ : (a : ℕ →₀ P) → ℕ →₀ P) x : ℕ →₀ P) :
                (a : ℕ) → P)
              x_1)) :
      M)
have rw : Eq.{u_2 + 1} (α := M)
  (∑ x_1 ∈ x.support.preimage (fun (x : ℕ) ↦ x + 1) sorry,
      ((HPow.hPow (α := P × M →ₗ[R] P × M) (inr R P M ∘ₗ f) (x_1 + 1) ∘ₗ inl R P M : (a : P) → P × M)
          ((x : (a : ℕ) → P) (x_1 + 1))).2 :
    M)
  ((f : (a : P × M) → M)
      (∑
        x_1 ∈
          Finsupp.support.{0, u_4} (M := P)
            ((comapDomain.addMonoidHom (f := fun (x : ℕ) ↦ x + 1) sorry : (a : ℕ →₀ P) → ℕ →₀ P) x),
        (HPow.hPow (α := P × M →ₗ[R] P × M) (inr R P M ∘ₗ f) x_1 ∘ₗ inl R P M : (a : P) → P × M)
          ((((comapDomain.addMonoidHom (f := fun (x : ℕ) ↦ x + 1) sorry : (a : ℕ →₀ P) → ℕ →₀ P) x : ℕ →₀ P) : (a : ℕ) → P)
            x_1)) :
    M)
Tactic: rw [← Finset.sum_preimage (· + 1) _ (add_left_injective 1).injOn _ (by simp_all)]