awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
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_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)
⊢ 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:
ext j k
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
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)
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)
⊢ 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

Premises used: eq_or_ne, rfl
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
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)
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)
⊢ 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

Premises used: eq_or_ne, rfl
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
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 : ι
⊢ 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:
simp [h₀]
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
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 : ι
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:
simp [hk]
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
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 : ι
⊢ 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:
simp [h₀]
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
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 : ι
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:
simp [hk]
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
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
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)
⊢ Eq (α := (ι →₀ R) →ₗ[R] M) (linearCombination R v ∘ₗ (↑(addSingleEquiv i c h₀) : (ι →₀ R) →ₗ[R] ι →₀ R))
    (linearCombination R (v + fun (x : ι) ↦ c x • v i))

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
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
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:
simp [addSingleEquiv]

Premises used: Finsupp.addSingleEquiv
-- Module: Mathlib.LinearAlgebra.Finsupp.Pi
Goal:
R : Type u_1
α : Type u_3
M : Type u_4
inst : AddCommMonoid M
inst_1 : Semiring R
inst_2 : Module R M
a : α
inst_3 : Subsingleton α
m : M
b : α
⊢ (((LinearEquiv.symm (uniqueLinearEquiv R M a) : (a : M) → α →₀ M) m : α →₀ M) : (a : α) → M) b = m

Tactic:
simp [Subsingleton.elim b a]

Premises used: Subsingleton.elim
-- Module: Mathlib.LinearAlgebra.Finsupp.Pi
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 α
f : α →₀ M
⊢ Eq.{u_4 + 1} (α := M) ((finsuppUnique R M α : (a : α →₀ M) → M) f : M) ((f : (a : α) → M) default : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Finsupp.Pi
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
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)
⊢ Eq (α := α →₀ M) ((LinearEquiv.symm (finsuppUnique R M α) : (a : M) → α →₀ M) m : α →₀ M) (single default m : α →₀ M)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Finsupp.Pi
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.{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:
simp [LinearEquiv.finsuppUnique, Equiv.funUnique, single, Pi.single,
    equivFunOnFinite, Function.update]

Premises used: Function.update, Finsupp.LinearEquiv.finsuppUnique, Finsupp.equivFunOnFinite, Pi.single, Equiv.funUnique, Finsupp.single
-- Module: Mathlib.LinearAlgebra.Finsupp.Pi
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
h :
  ∀ (x_1 : α), (x + y : (a : α) → M) x_1 = HAdd.hAdd (α := α → M) (β := α → M) (⇑x : (a : α) → M) (⇑y : (a : α) → M) x_1
⊢ (⇑(x + y) : (a : α) → M) = HAdd.hAdd (α := α → M) (⇑x : (a : α) → M) (⇑y : (a : α) → M)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Finsupp.Pi
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_1 : α
⊢ (x + y : (a : α) → M) x_1 = HAdd.hAdd (α := α → M) (β := α → M) (⇑x : (a : α) → M) (⇑y : (a : α) → M) x_1

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Finsupp.Pi
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
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
⊢ (⇑(x • y) : (a : α) → M) = HSMul.hSMul (α := R) (β := α → M) ((RingHom.id R : (a : R) → R) x : R) (⇑y : (a : α) → M)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Finsupp.Pi
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_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:
simp
-- Module: Mathlib.LinearAlgebra.Finsupp.Pi
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : α →₀ M
⊢ Eq (α := α → M) ((lcoeFun : (a : α →₀ M) → α → M) f : α → M) ((⇑f : (a : α) → M) : (a : α) → M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Finsupp.Pi
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 : α
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)
⊢ Eq (α := M →ₗ[R] α → M) (lcoeFun ∘ₗ lsingle x) (LinearMap.single.{u_5, u_1, u_2} R (fun (x : α) ↦ M) x)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Finsupp.Pi
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 : α
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:
simp [single_eq_pi_single]

Premises used: Finsupp.single_eq_pi_single
-- Module: Mathlib.LinearAlgebra.Finsupp.Pi
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
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)
⊢ Eq (α := P) (((f.prodOfFinsuppNat : (a : ℕ →₀ P) → P × M) x).1 : P) ((x : (a : ℕ) → P) 0 : P)

Tactic:
simp_rw [prodOfFinsuppNat, coe_lsum, sum, Prod.fst_sum]

Premises used: Finsupp.sum, Finsupp.coe_lsum, LinearMap.prodOfFinsuppNat, Prod.fst_sum
-- Module: Mathlib.LinearAlgebra.Finsupp.Pi
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
⊢ 0 ∉ x.support →
    Eq.{u_4 + 1} (α := 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
      0

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Finsupp.Pi
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)
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
⊢ 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:
rw [Finset.sum_eq_single 0 (fun n _ hn ↦ ?_) (by simp)]

Premises used: Finset.sum_eq_single, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.Finsupp.Pi
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)
    (((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:
simp
-- Module: Mathlib.LinearAlgebra.Finsupp.Pi
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
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
⊢ 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:
obtain ⟨n, rfl⟩ := n.exists_eq_succ_of_ne_zero hn

Premises used: Nat.exists_eq_succ_of_ne_zero, rfl
-- Module: Mathlib.LinearAlgebra.Finsupp.Pi
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.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:
simp [pow_succ']

Premises used: pow_succ'
-- Module: Mathlib.LinearAlgebra.Finsupp.Pi
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
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) ⋯ : (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)
⊢ 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)

Tactic:
simp_rw [prodOfFinsuppNat, coe_lsum, sum, Prod.snd_sum]

Premises used: Finsupp.sum, Prod.snd_sum, Finsupp.coe_lsum, LinearMap.prodOfFinsuppNat
-- Module: Mathlib.LinearAlgebra.Finsupp.Pi
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
⊢ ∀ x_1 ∈ x.support,
    (x_1 ∉ Set.range fun (x : ℕ) ↦ x + 1) →
      Eq.{u_2 + 1} (α := M)
        ((HPow.hPow (α := P × M →ₗ[R] P × M) (inr R P M ∘ₗ f) x_1 ∘ₗ inl R P M : (a : P) → P × M)
            ((x : (a : ℕ) → P) x_1)).2
        0

Tactic:
simp_all
-- Module: Mathlib.LinearAlgebra.Finsupp.Pi
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.{u_2 + 1} (α := M)
    (∑ x_1 ∈ x.support.preimage (fun (x : ℕ) ↦ x + 1) ⋯,
        ((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) ⋯ : (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)
⊢ 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)

Tactic:
rw [← Finset.sum_preimage (· + 1) _ (add_left_injective 1).injOn _ (by simp_all)]

Premises used: Function.Injective.injOn, Finset.sum_preimage, HAdd.hAdd, add_left_injective, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.Finsupp.Pi
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)
    (∑ x_1 ∈ x.support.preimage (fun (x : ℕ) ↦ x + 1) ⋯,
        ((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) ⋯ : (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)

Tactic:
simp [pow_succ']

Premises used: pow_succ'
-- Module: Mathlib.LinearAlgebra.Finsupp.Pi
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
inj : Injective (α := P × M) (β := M) (⇑f : (a : P × M) → M)
x y : ℕ →₀ P
s : Finset ℕ := x.support ∪ y.support
inl :
  ∀ (eq : s = ∅),
    Eq (α := P × M) ((f.prodOfFinsuppNat : (a : ℕ →₀ P) → P × M) x : P × M)
        ((f.prodOfFinsuppNat : (a : ℕ →₀ P) → P × M) y : P × M) →
      x = y
inr :
  ∀ (ne : s.Nonempty),
    Eq (α := P × M) ((f.prodOfFinsuppNat : (a : ℕ →₀ P) → P × M) x : P × M)
        ((f.prodOfFinsuppNat : (a : ℕ →₀ P) → P × M) y : P × M) →
      x = y
⊢ Eq (α := P × M) ((f.prodOfFinsuppNat : (a : ℕ →₀ P) → P × M) x : P × M)
      ((f.prodOfFinsuppNat : (a : ℕ →₀ P) → P × M) y : P × M) →
    x = y

Tactic:
obtain eq | ne := s.eq_empty_or_nonempty

Premises used: Finset.eq_empty_or_nonempty
-- Module: Mathlib.LinearAlgebra.Finsupp.Pi
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
inj : Injective (α := P × M) (β := M) (⇑f : (a : P × M) → M)
x y : ℕ →₀ P
s : Finset ℕ := x.support ∪ y.support
eq : s = ∅
⊢ Eq (α := P × M) ((f.prodOfFinsuppNat : (a : ℕ →₀ P) → P × M) x : P × M)
      ((f.prodOfFinsuppNat : (a : ℕ →₀ P) → P × M) y : P × M) →
    x = y

Tactic:
simp_all [s]