awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Dimension.Subsingleton
Goal:
R : Type u_1
inst : Semiring R
inst_1 : Nontrivial R
⊢ Module.rank R PUnit.{u_3 + 1} = 0

Tactic:
rank_subsingleton' _ _

Premises used: rank_subsingleton'
-- Module: Mathlib.LinearAlgebra.Dimension.Subsingleton
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
⊢ Module.rank R ↥⊥ = 0

Tactic:
rank_subsingleton' _ _

Premises used: rank_subsingleton'
-- Module: Mathlib.LinearAlgebra.Dimension.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
M' : Submodule R M
hN : M' ≤ torsion R M
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.LinearAlgebra.Dimension.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
M' : Submodule R M
hN : M' ≤ torsion R M
h : Nontrivial R
rw : ⨆ (ι : { s : Set M // LinearIndepOn R id s }), Cardinal.mk (↑(↑ι : Set M) : Type u_2) ≤ Module.rank R (M ⧸ M')
⊢ Module.rank R M ≤ Module.rank R (M ⧸ M')

Tactic:
rw [Module.rank]

Premises used: Module.rank
-- Module: Mathlib.LinearAlgebra.Dimension.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
M' : Submodule R M
hN : M' ≤ torsion R M
h : Nontrivial R
⊢ ⨆ (ι : { s : Set M // LinearIndepOn R id s }), Cardinal.mk (↑(↑ι : Set M) : Type u_2) ≤ Module.rank R (M ⧸ M')

Tactic:
ciSup_le fun ⟨s, hs⟩ ↦ LinearIndependent.cardinal_le_rank (v := (M'.mkQ ·)) ?_

Premises used: _private.0.rank_quotient_eq_of_le_torsion.match_1, LinearIndependent.cardinal_le_rank, Cardinal.mk, Set.Elem, LE.le, HasQuotient.Quotient, Module.rank, Subtype.val, ciSup_le
-- Module: Mathlib.LinearAlgebra.Dimension.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
M' : Submodule R M
hN : M' ≤ torsion R M
h : Nontrivial R
refine :
  ∀ (x : { s : Set M // LinearIndepOn R id s }) (s : Set M) (hs : LinearIndepOn R id s),
    LinearIndependent R (M := M ⧸ M')
      fun (x : (↑(↑(Subtype.mk (p := fun (s : Set M) ↦ LinearIndepOn R id s) s hs) : Set M) : Type u_2)) ↦
      (M'.mkQ : (a : M) → M ⧸ M') (↑x : M)
⊢ ⨆ (ι : { s : Set M // LinearIndepOn R id s }), Cardinal.mk (↑(↑ι : Set M) : Type u_2) ≤ Module.rank R (M ⧸ M')

Tactic:
refine ciSup_le fun ⟨s, hs⟩ ↦ LinearIndependent.cardinal_le_rank (v := (M'.mkQ ·)) ?_

Premises used: ciSup_le
-- Module: Mathlib.LinearAlgebra.Dimension.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
M' : Submodule R M
hN : M' ≤ torsion R M
h : Nontrivial R
x : { s : Set M // LinearIndepOn R id s }
s : Set M
hs : LinearIndepOn R id s
⊢ ∀ (s_1 : Finset (↑s : Type u_2)) (g : (↑s : Type u_2) → R),
    Eq (α := M) (∑ i ∈ s_1, g i • id (↑i : M)) 0 → ∀ i ∈ s_1, g i = 0

Tactic:
rw [LinearIndepOn, linearIndependent_iff'] at hs

Premises used: linearIndependent_iff', LinearIndepOn
-- Module: Mathlib.LinearAlgebra.Dimension.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
M' : Submodule R M
hN : M' ≤ torsion R M
h : Nontrivial R
x : { s : Set M // LinearIndepOn R id s }
s : Set M
hs_1 : LinearIndepOn R id s
hs :
  ∀ (s_1 : Finset (↑s : Type u_2)) (g : (↑s : Type u_2) → R),
    Eq (α := M) (∑ i ∈ s_1, g i • id (↑i : M)) 0 → ∀ i ∈ s_1, g i = 0
simp_rw :
  ∀ (s_1 : Finset (↑s : Type u_2)) (g : (↑s : Type u_2) → R), ∑ x ∈ s_1, g x • (↑x : M) ∈ M' → ∀ i ∈ s_1, g i = 0
⊢ LinearIndependent R (M := M ⧸ M')
    fun (x : (↑(↑(Subtype.mk (p := fun (s : Set M) ↦ LinearIndepOn R id s) s hs_1) : Set M) : Type u_2)) ↦
    (M'.mkQ : (a : M) → M ⧸ M') (↑x : M)

Tactic:
simp_rw [linearIndependent_iff', ← map_smul, ← map_sum, mkQ_apply, Quotient.mk_eq_zero]

Premises used: linearIndependent_iff', Submodule.mkQ_apply, map_sum, Submodule.Quotient.mk_eq_zero, map_smul
-- Module: Mathlib.LinearAlgebra.Dimension.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
M' : Submodule R M
hN : M' ≤ torsion R M
h : Nontrivial R
x : { s : Set M // LinearIndepOn R id s }
s : Set M
hs_1 : LinearIndepOn R id s
hs :
  ∀ (s_1 : Finset (↑s : Type u_2)) (g : (↑s : Type u_2) → R),
    Eq (α := M) (∑ i ∈ s_1, g i • id (↑i : M)) 0 → ∀ i ∈ s_1, g i = 0
t : Finset (↑s : Type u_2)
g : (↑s : Type u_2) → R
hg : ∑ x ∈ t, g x • (↑x : M) ∈ M'
i : (↑s : Type u_2)
hi : i ∈ t
obtain : ∀ (r : ↥(nonZeroDivisors R)) (hg : HSMul.hSMul (β := M) r (∑ x ∈ t, g x • (↑x : M)) = 0), g i = 0
⊢ g i = 0

Tactic:
obtain ⟨r, hg⟩ := hN hg
-- Module: Mathlib.LinearAlgebra.Dimension.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
M' : Submodule R M
hN : M' ≤ torsion R M
h : Nontrivial R
x : { s : Set M // LinearIndepOn R id s }
s : Set M
hs_1 : LinearIndepOn R id s
hs :
  ∀ (s_1 : Finset (↑s : Type u_2)) (g : (↑s : Type u_2) → R),
    Eq (α := M) (∑ i ∈ s_1, g i • id (↑i : M)) 0 → ∀ i ∈ s_1, g i = 0
t : Finset (↑s : Type u_2)
g : (↑s : Type u_2) → R
hg_1 : ∑ x ∈ t, g x • (↑x : M) ∈ M'
i : (↑s : Type u_2)
hi : i ∈ t
r : ↥(nonZeroDivisors R)
hg : HSMul.hSMul (β := M) r (∑ x ∈ t, g x • (↑x : M)) = 0
⊢ Eq (α := M) (∑ x ∈ t, ((↑r : R) * g x) • (↑x : M)) 0

Tactic:
simp_rw [Finset.smul_sum, Submonoid.smul_def, smul_smul] at hg

Premises used: smul_smul, Submonoid.smul_def, Finset.smul_sum
-- Module: Mathlib.LinearAlgebra.Dimension.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
M' : Submodule R M
hN : M' ≤ torsion R M
h : Nontrivial R
x : { s : Set M // LinearIndepOn R id s }
s : Set M
hs_1 : LinearIndepOn R id s
hs :
  ∀ (s_1 : Finset (↑s : Type u_2)) (g : (↑s : Type u_2) → R),
    Eq (α := M) (∑ i ∈ s_1, g i • id (↑i : M)) 0 → ∀ i ∈ s_1, g i = 0
t : Finset (↑s : Type u_2)
g : (↑s : Type u_2) → R
hg_1 : ∑ x ∈ t, g x • (↑x : M) ∈ M'
i : (↑s : Type u_2)
hi : i ∈ t
r : ↥(nonZeroDivisors R)
hg : Eq (α := M) (∑ x ∈ t, ((↑r : R) * g x) • (↑x : M)) 0
⊢ g i = 0

Tactic:
r.prop.2 _ (mul_comm (g i) r ▸ hs t _ hg i hi)

Premises used: Eq.rec, And.right, Subtype.prop, mul_comm, Eq.symm, Subtype.val
-- Module: Mathlib.LinearAlgebra.Dimension.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
M' : Submodule R M
hN : M' ≤ torsion R M
h : Nontrivial R
x : { s : Set M // LinearIndepOn R id s }
s : Set M
hs_1 : LinearIndepOn R id s
hs :
  ∀ (s_1 : Finset (↑s : Type u_2)) (g : (↑s : Type u_2) → R),
    Eq (α := M) (∑ i ∈ s_1, g i • id (↑i : M)) 0 → ∀ i ∈ s_1, g i = 0
t : Finset (↑s : Type u_2)
g : (↑s : Type u_2) → R
hg_1 : ∑ x ∈ t, g x • (↑x : M) ∈ M'
i : (↑s : Type u_2)
hi : i ∈ t
r : ↥(nonZeroDivisors R)
hg : Eq (α := M) (∑ x ∈ t, ((↑r : R) * g x) • (↑x : M)) 0
⊢ g i = 0

Tactic:
exact r.prop.2 _ (mul_comm (g i) r ▸ hs t _ hg i hi)

Premises used: And.right, Subtype.prop
-- Module: Mathlib.LinearAlgebra.Dimension.Torsion.Finite
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
rw : (∀ (x : M), ∃ (a : R), a ≠ 0 ∧ a • x = 0) ↔ ∀ ⦃x : M⦄, ∃ (a : ↥(nonZeroDivisors R)), a • x = 0
⊢ Module.rank R M = 0 ↔ Module.IsTorsion R M

Tactic:
rw [Module.IsTorsion, rank_eq_zero_iff]

Premises used: Module.IsTorsion, rank_eq_zero_iff
-- Module: Mathlib.LinearAlgebra.Dimension.Torsion.Finite
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
⊢ (∀ (x : M), ∃ (a : R), a ≠ 0 ∧ a • x = 0) ↔ ∀ ⦃x : M⦄, ∃ (a : ↥(nonZeroDivisors R)), a • x = 0

Tactic:
simp [mem_nonZeroDivisors_iff_ne_zero]

Premises used: mem_nonZeroDivisors_iff_ne_zero
-- Module: Mathlib.LinearAlgebra.Dimension.Torsion.Finite
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : StrongRankCondition R
inst_5 : Module.Finite R M
rw : finrank R M = 0 ↔ Eq.{u_2 + 2} (α := Cardinal.{u_2}) (↑(finrank R M) : Cardinal.{u_2}) 0
⊢ finrank R M = 0 ↔ IsTorsion R M

Tactic:
rw [← rank_eq_zero_iff_isTorsion (R := R), ← finrank_eq_rank]

Premises used: rank_eq_zero_iff_isTorsion, Module.finrank_eq_rank
-- Module: Mathlib.LinearAlgebra.Dimension.Torsion.Finite
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : StrongRankCondition R
inst_5 : Module.Finite R M
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : finrank R M = 0 ↔ finrank R M = 0
⊢ finrank R M = 0 ↔ Eq.{u_2 + 2} (α := Cardinal.{u_2}) (↑(finrank R M) : Cardinal.{u_2}) 0

Tactic:
norm_cast
-- Module: Mathlib.LinearAlgebra.DirectSum.Basis
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_2
M : ι → Type u_3
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_1, u_3} R (M i)
inst_3 : ∀ (i : ι), Free.{u_1, u_3} R (M i)
⊢ Free R (⨁ (i : ι), M i)

Tactic:
Module.Free.dfinsupp R M

Premises used: Module.Free.dfinsupp, DirectSum
-- Module: Mathlib.LinearAlgebra.DirectSum.Finite
Goal:
R : Type u_1
ι : Type u_2
inst : Semiring R
inst_1 : Finite ι
M : ι → Type u_3
inst_2 : (i : ι) → AddCommMonoid (M i)
inst_3 : (i : ι) → Module.{u_1, u_3} R (M i)
inst_4 : ∀ (i : ι), Module.Finite.{u_1, u_3} R (M i)
⊢ Module.Finite R (Π₀ (i : ι), M i)

Tactic:
letI : Fintype ι := Fintype.ofFinite _
  Module.Finite.equiv DFinsupp.linearEquivFunOnFintype.symm

Premises used: DFinsupp.linearEquivFunOnFintype, LinearEquiv.symm, Module.Finite.equiv
-- Module: Mathlib.LinearAlgebra.DirectSum.Finite
Goal:
R : Type u_1
ι : Type u_2
inst : Semiring R
inst_1 : Finite ι
M : ι → Type u_3
inst_2 : (i : ι) → AddCommMonoid (M i)
inst_3 : (i : ι) → Module.{u_1, u_3} R (M i)
inst_4 : ∀ (i : ι), Module.Finite.{u_1, u_3} R (M i)
⊢ Module.Finite R (⨁ (i : ι), M i)

Tactic:
Module.Finite.instDFinsupp M

Premises used: Module.Finite.instDFinsupp, DirectSum
-- Module: Mathlib.LinearAlgebra.DirectSum.Finsupp
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
N : Type u_4
inst_7 : AddCommMonoid N
inst_8 : Module R N
ι : Type u_5
inst_9 : DecidableEq ι
n : N
⊢ Eq (α := ι →₀ M ⊗[R] N)
    (((finsuppLeft R S M N ι : (ι →₀ M) ⊗[R] N ≃ₗ[S] ι →₀ M ⊗[R] N) : (a : (ι →₀ M) ⊗[R] N) → ι →₀ M ⊗[R] N)
        (0 ⊗ₜ[R] n) :
      ι →₀ M ⊗[R] N)
    (Finsupp.sum 0 fun (i : ι) (m : M) ↦ Finsupp.single i (m ⊗ₜ[R] n) : ι →₀ M ⊗[R] N)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.DirectSum.Finsupp
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
N : Type u_4
inst_7 : AddCommMonoid N
inst_8 : Module R N
ι : Type u_5
inst_9 : DecidableEq ι
n : N
f g : ι →₀ M
hf :
  Eq (α := ι →₀ M ⊗[R] N)
    (((finsuppLeft R S M N ι : (ι →₀ M) ⊗[R] N ≃ₗ[S] ι →₀ M ⊗[R] N) : (a : (ι →₀ M) ⊗[R] N) → ι →₀ M ⊗[R] N)
        (f ⊗ₜ[R] n) :
      ι →₀ M ⊗[R] N)
    (f.sum fun (i : ι) (m : M) ↦ Finsupp.single i (m ⊗ₜ[R] n) : ι →₀ M ⊗[R] N)
hg :
  Eq (α := ι →₀ M ⊗[R] N)
    (((finsuppLeft R S M N ι : (ι →₀ M) ⊗[R] N ≃ₗ[S] ι →₀ M ⊗[R] N) : (a : (ι →₀ M) ⊗[R] N) → ι →₀ M ⊗[R] N)
        (g ⊗ₜ[R] n) :
      ι →₀ M ⊗[R] N)
    (g.sum fun (i : ι) (m : M) ↦ Finsupp.single i (m ⊗ₜ[R] n) : ι →₀ M ⊗[R] N)
⊢ Eq (α := ι →₀ M ⊗[R] N)
    (((finsuppLeft R S M N ι : (ι →₀ M) ⊗[R] N ≃ₗ[S] ι →₀ M ⊗[R] N) : (a : (ι →₀ M) ⊗[R] N) → ι →₀ M ⊗[R] N)
        ((f + g) ⊗ₜ[R] n) :
      ι →₀ M ⊗[R] N)
    ((f + g).sum fun (i : ι) (m : M) ↦ Finsupp.single i (m ⊗ₜ[R] n) : ι →₀ M ⊗[R] N)

Tactic:
simp [add_tmul, map_add, hf, hg, Finsupp.sum_add_index]

Premises used: map_add, TensorProduct.add_tmul, Finsupp.sum_add_index
-- Module: Mathlib.LinearAlgebra.DirectSum.Finsupp
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
N : Type u_4
inst_7 : AddCommMonoid N
inst_8 : Module R N
ι : Type u_5
inst_9 : DecidableEq ι
n : N
a : ι
b : M
⊢ Eq (α := ι →₀ M ⊗[R] N)
    (((finsuppLeft R S M N ι : (ι →₀ M) ⊗[R] N ≃ₗ[S] ι →₀ M ⊗[R] N) : (a : (ι →₀ M) ⊗[R] N) → ι →₀ M ⊗[R] N)
        (Finsupp.single a b ⊗ₜ[R] n) :
      ι →₀ M ⊗[R] N)
    (Finsupp.sum (Finsupp.single a b) fun (i : ι) (m : M) ↦ Finsupp.single i (m ⊗ₜ[R] n) : ι →₀ M ⊗[R] N)

Tactic:
simp [finsuppLeft]

Premises used: TensorProduct.finsuppLeft
-- Module: Mathlib.LinearAlgebra.DirectSum.Finsupp
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
N : Type u_4
inst_7 : AddCommMonoid N
inst_8 : Module R N
ι : Type u_5
inst_9 : DecidableEq ι
p : ι →₀ M
n : N
zero :
  Eq (α := ι →₀ M ⊗[R] N)
    (((finsuppLeft R S M N ι : (ι →₀ M) ⊗[R] N ≃ₗ[S] ι →₀ M ⊗[R] N) : (a : (ι →₀ M) ⊗[R] N) → ι →₀ M ⊗[R] N)
        (0 ⊗ₜ[R] n) :
      ι →₀ M ⊗[R] N)
    (Finsupp.sum 0 fun (i : ι) (m : M) ↦ Finsupp.single i (m ⊗ₜ[R] n) : ι →₀ M ⊗[R] N)
add :
  ∀ (f g : ι →₀ M)
    (hf :
      Eq (α := ι →₀ M ⊗[R] N)
        (((finsuppLeft R S M N ι : (ι →₀ M) ⊗[R] N ≃ₗ[S] ι →₀ M ⊗[R] N) : (a : (ι →₀ M) ⊗[R] N) → ι →₀ M ⊗[R] N)
            (f ⊗ₜ[R] n) :
          ι →₀ M ⊗[R] N)
        (f.sum fun (i : ι) (m : M) ↦ Finsupp.single i (m ⊗ₜ[R] n) : ι →₀ M ⊗[R] N))
    (hg :
      Eq (α := ι →₀ M ⊗[R] N)
        (((finsuppLeft R S M N ι : (ι →₀ M) ⊗[R] N ≃ₗ[S] ι →₀ M ⊗[R] N) : (a : (ι →₀ M) ⊗[R] N) → ι →₀ M ⊗[R] N)
            (g ⊗ₜ[R] n) :
          ι →₀ M ⊗[R] N)
        (g.sum fun (i : ι) (m : M) ↦ Finsupp.single i (m ⊗ₜ[R] n) : ι →₀ M ⊗[R] N)),
    Eq (α := ι →₀ M ⊗[R] N)
      (((finsuppLeft R S M N ι : (ι →₀ M) ⊗[R] N ≃ₗ[S] ι →₀ M ⊗[R] N) : (a : (ι →₀ M) ⊗[R] N) → ι →₀ M ⊗[R] N)
          ((f + g) ⊗ₜ[R] n) :
        ι →₀ M ⊗[R] N)
      ((f + g).sum fun (i : ι) (m : M) ↦ Finsupp.single i (m ⊗ₜ[R] n) : ι →₀ M ⊗[R] N)
single :
  ∀ (a : ι) (b : M),
    Eq (α := ι →₀ M ⊗[R] N)
      (((finsuppLeft R S M N ι : (ι →₀ M) ⊗[R] N ≃ₗ[S] ι →₀ M ⊗[R] N) : (a : (ι →₀ M) ⊗[R] N) → ι →₀ M ⊗[R] N)
          (Finsupp.single a b ⊗ₜ[R] n) :
        ι →₀ M ⊗[R] N)
      (Finsupp.sum (Finsupp.single a b) fun (i : ι) (m : M) ↦ Finsupp.single i (m ⊗ₜ[R] n) : ι →₀ M ⊗[R] N)
⊢ Eq (α := ι →₀ M ⊗[R] N)
    (((finsuppLeft R S M N ι : (ι →₀ M) ⊗[R] N ≃ₗ[S] ι →₀ M ⊗[R] N) : (a : (ι →₀ M) ⊗[R] N) → ι →₀ M ⊗[R] N)
        (p ⊗ₜ[R] n) :
      ι →₀ M ⊗[R] N)
    (p.sum fun (i : ι) (m : M) ↦ Finsupp.single i (m ⊗ₜ[R] n) : ι →₀ M ⊗[R] N)

Tactic:
induction p using Finsupp.induction_linear with
  | zero => simp
  | add f g hf hg => simp [add_tmul, map_add, hf, hg, Finsupp.sum_add_index]
  | single => simp [finsuppLeft]

Premises used: LinearMap.single, map_add, TensorProduct.add_tmul, Submodule.zero, Finsupp.sum_add_index, Submodule.add, TensorProduct.finsuppLeft
-- Module: Mathlib.LinearAlgebra.DirectSum.Finsupp
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
N : Type u_4
inst_7 : AddCommMonoid N
inst_8 : Module R N
ι : Type u_5
inst_9 : DecidableEq ι
p : ι →₀ M
n : N
i : ι
⊢ Eq.{u_3 + 1} (α := M) ((p : (a : ι) → M) i : M) (0 : M) →
    Eq (α := M ⊗[R] N) ((Finsupp.single i (0 ⊗ₜ[R] n) : (a : ι) → M ⊗[R] N) i : M ⊗[R] N) (0 : M ⊗[R] N)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.DirectSum.Finsupp
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
N : Type u_4
inst_7 : AddCommMonoid N
inst_8 : Module R N
ι : Type u_5
inst_9 : DecidableEq ι
p : ι →₀ M
n : N
i : ι
rw :
  Eq (α := M ⊗[R] N) ((p.sum fun (i : ι) (m : M) ↦ Finsupp.single i (m ⊗ₜ[R] n) : (a : ι) → M ⊗[R] N) i : M ⊗[R] N)
    ((p : (a : ι) → M) i ⊗ₜ[R] n : M ⊗[R] N)
rw₁ :
  Eq (α := M ⊗[R] N) (p.sum fun (a₁ : ι) (b : M) ↦ (Finsupp.single a₁ (b ⊗ₜ[R] n) : (a : ι) → M ⊗[R] N) i : M ⊗[R] N)
    ((p : (a : ι) → M) i ⊗ₜ[R] n : M ⊗[R] N)
rw₂ :
  Eq (α := M ⊗[R] N)
    (((Finsupp.single i ((p : (a : ι) → M) i ⊗ₜ[R] n) : ι →₀ M ⊗[R] N) : (a : ι) → M ⊗[R] N) i : M ⊗[R] N)
    ((p : (a : ι) → M) i ⊗ₜ[R] n : M ⊗[R] N)
rw₃ rw₄ : Eq (α := M ⊗[R] N) ((p : (a : ι) → M) i ⊗ₜ[R] n : M ⊗[R] N) ((p : (a : ι) → M) i ⊗ₜ[R] n : M ⊗[R] N)
⊢ Eq (α := M ⊗[R] N)
    (((((finsuppLeft R S M N ι : (ι →₀ M) ⊗[R] N ≃ₗ[S] ι →₀ M ⊗[R] N) : (a : (ι →₀ M) ⊗[R] N) → ι →₀ M ⊗[R] N)
              (p ⊗ₜ[R] n) :
            ι →₀ M ⊗[R] N) :
          (a : ι) → M ⊗[R] N)
        i :
      M ⊗[R] N)
    ((p : (a : ι) → M) i ⊗ₜ[R] n : M ⊗[R] N)

Tactic:
rw [finsuppLeft_apply_tmul, Finsupp.sum_apply,
    Finsupp.sum_eq_single i (fun _ _ ↦ Finsupp.single_eq_of_ne') (by simp), Finsupp.single_eq_same]

Premises used: Finsupp.single_eq_same, Finsupp.sum_eq_single, TensorProduct.finsuppLeft_apply_tmul, Finsupp.sum_apply
-- Module: Mathlib.LinearAlgebra.DirectSum.Finsupp
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
N : Type u_4
inst_7 : AddCommMonoid N
inst_8 : Module R N
ι : Type u_5
inst_9 : DecidableEq ι
i : ι
⊢ Eq (α := M ⊗[R] N)
    ((((finsuppLeft R S M N ι : (ι →₀ M) ⊗[R] N ≃ₗ[S] ι →₀ M ⊗[R] N) : (a : (ι →₀ M) ⊗[R] N) → ι →₀ M ⊗[R] N) 0 :
          (a : ι) → M ⊗[R] N)
        i :
      M ⊗[R] N)
    ((rTensor N (Finsupp.lapply i) : (a : (ι →₀ M) ⊗[R] N) → M ⊗[R] N) 0 : M ⊗[R] N)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.DirectSum.Finsupp
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
N : Type u_4
inst_7 : AddCommMonoid N
inst_8 : Module R N
ι : Type u_5
inst_9 : DecidableEq ι
i : ι
f : ι →₀ M
n : N
⊢ Eq (α := M ⊗[R] N)
    (((((finsuppLeft R S M N ι : (ι →₀ M) ⊗[R] N ≃ₗ[S] ι →₀ M ⊗[R] N) : (a : (ι →₀ M) ⊗[R] N) → ι →₀ M ⊗[R] N)
              (f ⊗ₜ[R] n) :
            ι →₀ M ⊗[R] N) :
          (a : ι) → M ⊗[R] N)
        i :
      M ⊗[R] N)
    ((rTensor N (Finsupp.lapply i) : (a : (ι →₀ M) ⊗[R] N) → M ⊗[R] N) (f ⊗ₜ[R] n) : M ⊗[R] N)

Tactic:
simp only [finsuppLeft_apply_tmul_apply, rTensor_tmul, Finsupp.lapply_apply]

Premises used: LinearMap.rTensor_tmul, Finsupp.lapply_apply, TensorProduct.finsuppLeft_apply_tmul_apply
-- Module: Mathlib.LinearAlgebra.DirectSum.Finsupp
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
N : Type u_4
inst_7 : AddCommMonoid N
inst_8 : Module R N
ι : Type u_5
inst_9 : DecidableEq ι
i : ι
x y : (ι →₀ M) ⊗[R] N
hx :
  Eq (α := M ⊗[R] N)
    (((((finsuppLeft R S M N ι : (ι →₀ M) ⊗[R] N ≃ₗ[S] ι →₀ M ⊗[R] N) : (a : (ι →₀ M) ⊗[R] N) → ι →₀ M ⊗[R] N) x :
            ι →₀ M ⊗[R] N) :
          (a : ι) → M ⊗[R] N)
        i :
      M ⊗[R] N)
    ((rTensor N (Finsupp.lapply i) : (a : (ι →₀ M) ⊗[R] N) → M ⊗[R] N) x : M ⊗[R] N)
hy :
  Eq (α := M ⊗[R] N)
    (((((finsuppLeft R S M N ι : (ι →₀ M) ⊗[R] N ≃ₗ[S] ι →₀ M ⊗[R] N) : (a : (ι →₀ M) ⊗[R] N) → ι →₀ M ⊗[R] N) y :
            ι →₀ M ⊗[R] N) :
          (a : ι) → M ⊗[R] N)
        i :
      M ⊗[R] N)
    ((rTensor N (Finsupp.lapply i) : (a : (ι →₀ M) ⊗[R] N) → M ⊗[R] N) y : M ⊗[R] N)
⊢ Eq (α := M ⊗[R] N)
    (((((finsuppLeft R S M N ι : (ι →₀ M) ⊗[R] N ≃ₗ[S] ι →₀ M ⊗[R] N) : (a : (ι →₀ M) ⊗[R] N) → ι →₀ M ⊗[R] N) (x + y) :
            ι →₀ M ⊗[R] N) :
          (a : ι) → M ⊗[R] N)
        i :
      M ⊗[R] N)
    ((rTensor N (Finsupp.lapply i) : (a : (ι →₀ M) ⊗[R] N) → M ⊗[R] N) (x + y) : M ⊗[R] N)

Tactic:
simp [map_add, hx, hy]

Premises used: map_add
-- Module: Mathlib.LinearAlgebra.DirectSum.Finsupp
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
N : Type u_4
inst_7 : AddCommMonoid N
inst_8 : Module R N
ι : Type u_5
inst_9 : DecidableEq ι
t : (ι →₀ M) ⊗[R] N
i : ι
zero :
  Eq (α := M ⊗[R] N)
    ((((finsuppLeft R S M N ι : (ι →₀ M) ⊗[R] N ≃ₗ[S] ι →₀ M ⊗[R] N) : (a : (ι →₀ M) ⊗[R] N) → ι →₀ M ⊗[R] N) 0 :
          (a : ι) → M ⊗[R] N)
        i :
      M ⊗[R] N)
    ((rTensor N (Finsupp.lapply i) : (a : (ι →₀ M) ⊗[R] N) → M ⊗[R] N) 0 : M ⊗[R] N)
tmul :
  ∀ (f : ι →₀ M) (n : N),
    Eq (α := M ⊗[R] N)
      (((((finsuppLeft R S M N ι : (ι →₀ M) ⊗[R] N ≃ₗ[S] ι →₀ M ⊗[R] N) : (a : (ι →₀ M) ⊗[R] N) → ι →₀ M ⊗[R] N)
                (f ⊗ₜ[R] n) :
              ι →₀ M ⊗[R] N) :
            (a : ι) → M ⊗[R] N)
          i :
        M ⊗[R] N)
      ((rTensor N (Finsupp.lapply i) : (a : (ι →₀ M) ⊗[R] N) → M ⊗[R] N) (f ⊗ₜ[R] n) : M ⊗[R] N)
add :
  ∀ (x y : (ι →₀ M) ⊗[R] N)
    (hx :
      Eq (α := M ⊗[R] N)
        (((((finsuppLeft R S M N ι : (ι →₀ M) ⊗[R] N ≃ₗ[S] ι →₀ M ⊗[R] N) : (a : (ι →₀ M) ⊗[R] N) → ι →₀ M ⊗[R] N) x :
                ι →₀ M ⊗[R] N) :
              (a : ι) → M ⊗[R] N)
            i :
          M ⊗[R] N)
        ((rTensor N (Finsupp.lapply i) : (a : (ι →₀ M) ⊗[R] N) → M ⊗[R] N) x : M ⊗[R] N))
    (hy :
      Eq (α := M ⊗[R] N)
        (((((finsuppLeft R S M N ι : (ι →₀ M) ⊗[R] N ≃ₗ[S] ι →₀ M ⊗[R] N) : (a : (ι →₀ M) ⊗[R] N) → ι →₀ M ⊗[R] N) y :
                ι →₀ M ⊗[R] N) :
              (a : ι) → M ⊗[R] N)
            i :
          M ⊗[R] N)
        ((rTensor N (Finsupp.lapply i) : (a : (ι →₀ M) ⊗[R] N) → M ⊗[R] N) y : M ⊗[R] N)),
    Eq (α := M ⊗[R] N)
      (((((finsuppLeft R S M N ι : (ι →₀ M) ⊗[R] N ≃ₗ[S] ι →₀ M ⊗[R] N) : (a : (ι →₀ M) ⊗[R] N) → ι →₀ M ⊗[R] N)
                (x + y) :
              ι →₀ M ⊗[R] N) :
            (a : ι) → M ⊗[R] N)
          i :
        M ⊗[R] N)
      ((rTensor N (Finsupp.lapply i) : (a : (ι →₀ M) ⊗[R] N) → M ⊗[R] N) (x + y) : M ⊗[R] N)
⊢ Eq (α := M ⊗[R] N)
    (((((finsuppLeft R S M N ι : (ι →₀ M) ⊗[R] N ≃ₗ[S] ι →₀ M ⊗[R] N) : (a : (ι →₀ M) ⊗[R] N) → ι →₀ M ⊗[R] N) t :
            ι →₀ M ⊗[R] N) :
          (a : ι) → M ⊗[R] N)
        i :
      M ⊗[R] N)
    ((rTensor N (Finsupp.lapply i) : (a : (ι →₀ M) ⊗[R] N) → M ⊗[R] N) t : M ⊗[R] N)

Tactic:
induction t with
  | zero => simp
  | tmul f n => simp only [finsuppLeft_apply_tmul_apply, rTensor_tmul, Finsupp.lapply_apply]
  | add x y hx hy => simp [map_add, hx, hy]

Premises used: LinearMap.rTensor_tmul, map_add, Finsupp.lapply_apply, Submodule.zero, TensorProduct.tmul, Submodule.add, TensorProduct.finsuppLeft_apply_tmul_apply
-- Module: Mathlib.LinearAlgebra.DirectSum.Finsupp
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
N : Type u_4
inst_7 : AddCommMonoid N
inst_8 : Module R N
ι : Type u_5
inst_9 : DecidableEq ι
i : ι
m : M
n : N
⊢ Eq (α := (ι →₀ M) ⊗[R] N)
    (((LinearEquiv.symm (finsuppLeft R S M N ι) : (ι →₀ M ⊗[R] N) ≃ₗ[S] (ι →₀ M) ⊗[R] N) :
          (a : ι →₀ M ⊗[R] N) → (ι →₀ M) ⊗[R] N)
        (Finsupp.single i (m ⊗ₜ[R] n)) :
      (ι →₀ M) ⊗[R] N)
    (Finsupp.single i m ⊗ₜ[R] n : (ι →₀ M) ⊗[R] N)

Tactic:
simp [finsuppLeft]

Premises used: TensorProduct.finsuppLeft
-- Module: Mathlib.LinearAlgebra.DirectSum.Finsupp
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
N : Type u_4
inst_7 : AddCommMonoid N
inst_8 : Module R N
ι : Type u_5
inst_9 : DecidableEq ι
m : M
⊢ Eq (α := ι →₀ M ⊗[R] N)
    (((finsuppRight R S M N ι : M ⊗[R] (ι →₀ N) ≃ₗ[S] ι →₀ M ⊗[R] N) : (a : M ⊗[R] (ι →₀ N)) → ι →₀ M ⊗[R] N)
        (m ⊗ₜ[R] 0) :
      ι →₀ M ⊗[R] N)
    (Finsupp.sum 0 fun (i : ι) (n : N) ↦ Finsupp.single i (m ⊗ₜ[R] n) : ι →₀ M ⊗[R] N)

Tactic:
simp