awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.SpecialLinearGroup
Goal:
R : Type u_4
inst : CommRing R
V : Type u_5
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Module.Free R V
inst_4 : Module.Finite R V
ι : Type u_6
inst_5 : Fintype ι
inst_6 : DecidableEq ι
b : Module.Basis ι R V
g : ↥(center (Matrix.SpecialLinearGroup ι R))
h : Nontrivial R
hV : Nontrivial V
hι : ¬IsEmpty ι
this_1 : FaithfulSMul R V
g' : ↥(center (_root_.SpecialLinearGroup R V)) :=
  (centerCongr (toLin_equiv b) :
      (a : ↥(center (Matrix.SpecialLinearGroup ι R))) → ↥(center (_root_.SpecialLinearGroup R V)))
    g
hgg' :
  ∀ (x : V),
    Eq (α := V) (((↑(↑(↑g' : _root_.SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) : (a : V) → V) x : V)
      (((↑(↑((toLin_equiv b : (a : Matrix.SpecialLinearGroup ι R) → _root_.SpecialLinearGroup R V)
                      (↑g : Matrix.SpecialLinearGroup ι R)) :
                  V ≃ₗ[R] V) :
              V →ₗ[R] V) :
            (a : V) → V)
          x :
        V)
x : V
this :
  HSMul.hSMul.{u_4, u_5, u_5} (α := R)
      (↑(↑((centerEquivRootsOfUnity :
                  (a : ↥(center (_root_.SpecialLinearGroup R V))) → ↥(rootsOfUnity (max (Module.finrank R V) 1) R))
                g') :
            Rˣ) :
        R)
      x =
    ((↑(↑g' : _root_.SpecialLinearGroup R V) : V ≃ₗ[R] V) : (a : V) → V) x
neg :
  (HSMul.hSMul.{u_4, u_5, u_5} (α := R) (β := V →ₗ[R] V)
          (↑(↑((center_equiv_rootsOfUnity :
                      (a : ↥(center (Matrix.SpecialLinearGroup ι R))) → ↥(rootsOfUnity (max (Fintype.card ι) 1) R))
                    g) :
                Rˣ) :
            R)
          LinearMap.id :
        (a : V) → V)
      x =
    HSMul.hSMul.{u_4, u_5, u_5} (α := R)
      (↑(↑((center_equiv_rootsOfUnity :
                  (a : ↥(center (Matrix.SpecialLinearGroup ι R))) → ↥(rootsOfUnity (max (Fintype.card ι) 1) R))
                g) :
            Rˣ) :
        R)
      x
⊢ HSMul.hSMul.{u_4, u_5, u_5} (α := R)
      (↑(↑((centerEquivRootsOfUnity :
                  (a : ↥(center (_root_.SpecialLinearGroup R V))) → ↥(rootsOfUnity (max (Module.finrank R V) 1) R))
                g') :
            Rˣ) :
        R)
      x =
    HSMul.hSMul.{u_4, u_5, u_5} (α := R)
      (↑(↑((center_equiv_rootsOfUnity :
                  (a : ↥(center (Matrix.SpecialLinearGroup ι R))) → ↥(rootsOfUnity (max (Fintype.card ι) 1) R))
                g) :
            Rˣ) :
        R)
      x

Tactic:
rw [this, ← LinearEquiv.coe_toLinearMap, hgg',
      Matrix.SpecialLinearGroup.toLin_equiv.toLinearMap_eq,
      Matrix.SpecialLinearGroup.eq_scalar_center_equiv_rootsOfUnity g,
      Matrix.toLin_scalar]

Premises used: Matrix.toLin_scalar, Matrix.SpecialLinearGroup.eq_scalar_center_equiv_rootsOfUnity, Matrix.SpecialLinearGroup.toLin_equiv.toLinearMap_eq, LinearEquiv.coe_toLinearMap
-- Module: Mathlib.LinearAlgebra.SpecialLinearGroup
Goal:
R : Type u_4
inst : CommRing R
V : Type u_5
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Module.Free R V
inst_4 : Module.Finite R V
ι : Type u_6
inst_5 : Fintype ι
inst_6 : DecidableEq ι
b : Module.Basis ι R V
g : ↥(center (Matrix.SpecialLinearGroup ι R))
h : Nontrivial R
hV : Nontrivial V
hι : ¬IsEmpty ι
this_1 : FaithfulSMul R V
g' : ↥(center (_root_.SpecialLinearGroup R V)) :=
  (centerCongr (toLin_equiv b) :
      (a : ↥(center (Matrix.SpecialLinearGroup ι R))) → ↥(center (_root_.SpecialLinearGroup R V)))
    g
hgg' :
  ∀ (x : V),
    Eq (α := V) (((↑(↑(↑g' : _root_.SpecialLinearGroup R V) : V ≃ₗ[R] V) : V →ₗ[R] V) : (a : V) → V) x : V)
      (((↑(↑((toLin_equiv b : (a : Matrix.SpecialLinearGroup ι R) → _root_.SpecialLinearGroup R V)
                      (↑g : Matrix.SpecialLinearGroup ι R)) :
                  V ≃ₗ[R] V) :
              V →ₗ[R] V) :
            (a : V) → V)
          x :
        V)
x : V
this :
  HSMul.hSMul.{u_4, u_5, u_5} (α := R)
      (↑(↑((centerEquivRootsOfUnity :
                  (a : ↥(center (_root_.SpecialLinearGroup R V))) → ↥(rootsOfUnity (max (Module.finrank R V) 1) R))
                g') :
            Rˣ) :
        R)
      x =
    ((↑(↑g' : _root_.SpecialLinearGroup R V) : V ≃ₗ[R] V) : (a : V) → V) x
⊢ (HSMul.hSMul.{u_4, u_5, u_5} (α := R) (β := V →ₗ[R] V)
          (↑(↑((center_equiv_rootsOfUnity :
                      (a : ↥(center (Matrix.SpecialLinearGroup ι R))) → ↥(rootsOfUnity (max (Fintype.card ι) 1) R))
                    g) :
                Rˣ) :
            R)
          LinearMap.id :
        (a : V) → V)
      x =
    HSMul.hSMul.{u_4, u_5, u_5} (α := R)
      (↑(↑((center_equiv_rootsOfUnity :
                  (a : ↥(center (Matrix.SpecialLinearGroup ι R))) → ↥(rootsOfUnity (max (Fintype.card ι) 1) R))
                g) :
            Rˣ) :
        R)
      x

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.StdBasis
Goal:
R : Type u_2
η : Type u_4
ιs : η → Type u_5
Ms : η → Type u_6
inst : Semiring R
inst_1 : (i : η) → AddCommMonoid (Ms i)
inst_2 : (i : η) → Module.{u_2, u_6} R (Ms i)
inst_3 : DecidableEq η
v : (j : η) → ιs j → Ms j
hs : ∀ (i : η), LinearIndependent R (v i)
⊢ LinearIndependent (ι := (i : η) × ιs i) R (M := (i : η) → Ms i)
    (Function.comp (β := Π₀ (i : η), Ms i)
      (⇑(LinearMap.pi (φ := Ms) (DFinsupp.lapply (M := Ms))) : (a : Π₀ (i : η), Ms i) → (i : η) → Ms i)
      fun (ix : (i : η) × ιs i) ↦
      DFinsupp.single (β := Ms) (ix.fst (β := fun (i : η) ↦ ιs i))
        (v (ix.fst (β := fun (i : η) ↦ ιs i)) (ix.snd (β := fun (i : η) ↦ ιs i))))

Tactic:
(DFinsupp.linearIndependent_single _ hs).map_injOn _ DFinsupp.injective_pi_lapply.injOn

Premises used: Function.Injective.injOn, DFinsupp.injective_pi_lapply, LinearIndependent.map_injOn, DFinsupp.linearIndependent_single
-- Module: Mathlib.LinearAlgebra.StdBasis
Goal:
R : Type u_2
η : Type u_4
ιs : η → Type u_5
Ms : η → Type u_6
inst : Semiring R
inst_1 : (i : η) → AddCommMonoid (Ms i)
inst_2 : (i : η) → Module.{u_2, u_6} R (Ms i)
inst_3 : DecidableEq η
v : (j : η) → ιs j → Ms j
hs : ∀ (i : η), LinearIndependent R (v i)
⊢ LinearIndependent R (M := (j : η) → Ms j) fun (ji : (j : η) × ιs j) ↦
    single (M := Ms) (ji.fst (β := fun (j : η) ↦ ιs j))
      (v (ji.fst (β := fun (j : η) ↦ ιs j)) (ji.snd (β := fun (j : η) ↦ ιs j)))

Tactic:
convert! (DFinsupp.linearIndependent_single _ hs).map_injOn _ DFinsupp.injective_pi_lapply.injOn

Premises used: Function.Injective.injOn, DFinsupp.injective_pi_lapply, LinearIndependent.map_injOn, DFinsupp.linearIndependent_single
-- Module: Mathlib.LinearAlgebra.StdBasis
Goal:
ι : Type u_7
R : Type u_8
inst : Semiring R
inst_1 : DecidableEq ι
rw :
  LinearIndependent (ι := (_ : ι) × PUnit.{1}) R (M := (j : ι) → R)
    ((fun (i : ι) ↦ single (M := fun (i : ι) ↦ R) i 1) ∘ (⇑(Equiv.sigmaPUnit ι) : (a : (_ : ι) × PUnit.{1}) → ι))
⊢ LinearIndependent R (M := (j : ι) → R) fun (i : ι) ↦ single (M := fun (i : ι) ↦ R) i 1

Tactic:
rw [← linearIndependent_equiv (Equiv.sigmaPUnit ι)]

Premises used: Equiv.sigmaPUnit, linearIndependent_equiv
-- Module: Mathlib.LinearAlgebra.StdBasis
Goal:
ι : Type u_7
R : Type u_8
inst : Semiring R
inst_1 : DecidableEq ι
⊢ ∀ (i : ι), LinearIndependent (ι := Unit) R (M := R) ((fun (x : ι) (x_1 : Unit) ↦ (1 : R)) i)

Tactic:
simp +contextual [Fintype.linearIndependent_iffₛ]

Premises used: Fintype.linearIndependent_iffₛ
-- Module: Mathlib.LinearAlgebra.StdBasis
Goal:
ι : Type u_7
R : Type u_8
inst : Semiring R
inst_1 : DecidableEq ι
⊢ LinearIndependent (ι := (_ : ι) × PUnit.{1}) R (M := (j : ι) → R)
    ((fun (i : ι) ↦ single (M := fun (i : ι) ↦ R) i 1) ∘ (⇑(Equiv.sigmaPUnit ι) : (a : (_ : ι) × PUnit.{1}) → ι))

Tactic:
exact Pi.linearIndependent_single (fun (_ : ι) (_ : Unit) ↦ (1 : R))
    <| by simp +contextual [Fintype.linearIndependent_iffₛ]

Premises used: Pi.linearIndependent_single, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.StdBasis
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsTorsionFree R M
inst_5 : DecidableEq ι
v : ι → M
hv : ∀ (i : ι), v i ≠ 0
rw :
  LinearIndependent (ι := (_ : ι) × PUnit.{1}) R (M := (j : ι) → M)
    ((fun (i : ι) ↦ single (M := fun (i : ι) ↦ M) i (v i)) ∘ (⇑(Equiv.sigmaPUnit ι) : (a : (_ : ι) × PUnit.{1}) → ι))
⊢ LinearIndependent R (M := (j : ι) → M) fun (i : ι) ↦ single (M := fun (i : ι) ↦ M) i (v i)

Tactic:
rw [← linearIndependent_equiv (Equiv.sigmaPUnit ι)]

Premises used: Equiv.sigmaPUnit, linearIndependent_equiv
-- Module: Mathlib.LinearAlgebra.StdBasis
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsTorsionFree R M
inst_5 : DecidableEq ι
v : ι → M
hv : ∀ (i : ι), v i ≠ 0
⊢ ∀ (i : ι), LinearIndependent.{0, u_2, u_3} (ι := Unit) R (M := M) ((fun (i : ι) (x : Unit) ↦ v i) i)

Tactic:
simp +contextual [hv]
-- Module: Mathlib.LinearAlgebra.StdBasis
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsTorsionFree R M
inst_5 : DecidableEq ι
v : ι → M
hv : ∀ (i : ι), v i ≠ 0
⊢ LinearIndependent (ι := (_ : ι) × PUnit.{1}) R (M := (j : ι) → M)
    ((fun (i : ι) ↦ single (M := fun (i : ι) ↦ M) i (v i)) ∘ (⇑(Equiv.sigmaPUnit ι) : (a : (_ : ι) × PUnit.{1}) → ι))

Tactic:
exact linearIndependent_single (fun i (_ : Unit) ↦ v i) <| by simp +contextual [hv]

Premises used: Pi.linearIndependent_single
-- Module: Mathlib.LinearAlgebra.StdBasis
Goal:
R : Type u_2
η : Type u_4
ιs : η → Type u_5
Ms : η → Type u_6
inst : Semiring R
inst_1 : (i : η) → AddCommMonoid (Ms i)
inst_2 : (i : η) → Module.{u_2, u_6} R (Ms i)
inst_3 : Fintype η
inst_4 : DecidableEq η
s : (j : η) → Basis.{u_5, u_2, u_6} (ιs j) R (Ms j)
j : η
i : ιs j
h :
  ∀ (j' : η) (i' : ιs j'),
    Eq.{u_2 + 1} (α := R)
      (((((Pi.basis (ιs := ιs) (Ms := Ms) s).repr : (a : (j : η) → Ms j) → (j : η) × ιs j →₀ R)
                (single (M := Ms) j ((s j : (a : ιs j) → Ms j) i)) :
              (j : η) × ιs j →₀ R) :
            (a : (j : η) × ιs j) → R)
          (Sigma.mk (β := fun (j : η) ↦ ιs j) j' i') :
        R)
      ((Finsupp.single (Sigma.mk (β := fun (j : η) ↦ ιs j) j i) 1 : (a : (j : η) × ιs j) → R)
          (Sigma.mk (β := fun (j : η) ↦ ιs j) j' i') :
        R)
⊢ Eq (α := (j : η) × ιs j →₀ R)
    (((Pi.basis (ιs := ιs) (Ms := Ms) s).repr : (a : (j : η) → Ms j) → (j : η) × ιs j →₀ R)
        (single (M := Ms) j ((s j : (a : ιs j) → Ms j) i)) :
      (j : η) × ιs j →₀ R)
    (Finsupp.single (Sigma.mk (β := fun (j : η) ↦ ιs j) j i) 1 : (j : η) × ιs j →₀ R)

Tactic:
ext ⟨j', i'⟩
-- Module: Mathlib.LinearAlgebra.StdBasis
Goal:
R : Type u_2
η : Type u_4
ιs : η → Type u_5
Ms : η → Type u_6
inst : Semiring R
inst_1 : (i : η) → AddCommMonoid (Ms i)
inst_2 : (i : η) → Module.{u_2, u_6} R (Ms i)
inst_3 : Fintype η
inst_4 : DecidableEq η
s : (j : η) → Basis.{u_5, u_2, u_6} (ιs j) R (Ms j)
j : η
i : ιs j
j' : η
i' : ιs j'
pos :
  ∀ (hj : j = j'),
    Eq.{u_2 + 1} (α := R)
      (((((Pi.basis (ιs := ιs) (Ms := Ms) s).repr : (a : (j : η) → Ms j) → (j : η) × ιs j →₀ R)
                (single (M := Ms) j ((s j : (a : ιs j) → Ms j) i)) :
              (j : η) × ιs j →₀ R) :
            (a : (j : η) × ιs j) → R)
          (Sigma.mk (β := fun (j : η) ↦ ιs j) j' i') :
        R)
      ((Finsupp.single (Sigma.mk (β := fun (j : η) ↦ ιs j) j i) 1 : (a : (j : η) × ιs j) → R)
          (Sigma.mk (β := fun (j : η) ↦ ιs j) j' i') :
        R)
neg :
  ∀ (hj : ¬j = j'),
    Eq.{u_2 + 1} (α := R)
      (((((Pi.basis (ιs := ιs) (Ms := Ms) s).repr : (a : (j : η) → Ms j) → (j : η) × ιs j →₀ R)
                (single (M := Ms) j ((s j : (a : ιs j) → Ms j) i)) :
              (j : η) × ιs j →₀ R) :
            (a : (j : η) × ιs j) → R)
          (Sigma.mk (β := fun (j : η) ↦ ιs j) j' i') :
        R)
      ((Finsupp.single (Sigma.mk (β := fun (j : η) ↦ ιs j) j i) 1 : (a : (j : η) × ιs j) → R)
          (Sigma.mk (β := fun (j : η) ↦ ιs j) j' i') :
        R)
⊢ Eq.{u_2 + 1} (α := R)
    (((((Pi.basis (ιs := ιs) (Ms := Ms) s).repr : (a : (j : η) → Ms j) → (j : η) × ιs j →₀ R)
              (single (M := Ms) j ((s j : (a : ιs j) → Ms j) i)) :
            (j : η) × ιs j →₀ R) :
          (a : (j : η) × ιs j) → R)
        (Sigma.mk (β := fun (j : η) ↦ ιs j) j' i') :
      R)
    ((Finsupp.single (Sigma.mk (β := fun (j : η) ↦ ιs j) j i) 1 : (a : (j : η) × ιs j) → R)
        (Sigma.mk (β := fun (j : η) ↦ ιs j) j' i') :
      R)

Tactic:
by_cases hj : j = j'
-- Module: Mathlib.LinearAlgebra.StdBasis
Goal:
R : Type u_2
η : Type u_4
ιs : η → Type u_5
Ms : η → Type u_6
inst : Semiring R
inst_1 : (i : η) → AddCommMonoid (Ms i)
inst_2 : (i : η) → Module.{u_2, u_6} R (Ms i)
inst_3 : Fintype η
inst_4 : DecidableEq η
s : (j : η) → Basis.{u_5, u_2, u_6} (ιs j) R (Ms j)
j : η
i : ιs j
j' : η
i' : ιs j'
hj : j = j'
pos :
  ∀ (i' : ιs j),
    Eq.{u_2 + 1} (α := R)
      (((((Pi.basis (ιs := ιs) (Ms := Ms) s).repr : (a : (j : η) → Ms j) → (j : η) × ιs j →₀ R)
                (single (M := Ms) j ((s j : (a : ιs j) → Ms j) i)) :
              (j : η) × ιs j →₀ R) :
            (a : (j : η) × ιs j) → R)
          (Sigma.mk (β := fun (j : η) ↦ ιs j) j i') :
        R)
      ((Finsupp.single (Sigma.mk (β := fun (j : η) ↦ ιs j) j i) 1 : (a : (j : η) × ιs j) → R)
          (Sigma.mk (β := fun (j : η) ↦ ιs j) j i') :
        R)
⊢ Eq.{u_2 + 1} (α := R)
    (((((Pi.basis (ιs := ιs) (Ms := Ms) s).repr : (a : (j : η) → Ms j) → (j : η) × ιs j →₀ R)
              (single (M := Ms) j ((s j : (a : ιs j) → Ms j) i)) :
            (j : η) × ιs j →₀ R) :
          (a : (j : η) × ιs j) → R)
        (Sigma.mk (β := fun (j : η) ↦ ιs j) j' i') :
      R)
    ((Finsupp.single (Sigma.mk (β := fun (j : η) ↦ ιs j) j i) 1 : (a : (j : η) × ιs j) → R)
        (Sigma.mk (β := fun (j : η) ↦ ιs j) j' i') :
      R)

Tactic:
subst hj
-- Module: Mathlib.LinearAlgebra.StdBasis
Goal:
R : Type u_2
η : Type u_4
ιs : η → Type u_5
Ms : η → Type u_6
inst : Semiring R
inst_1 : (i : η) → AddCommMonoid (Ms i)
inst_2 : (i : η) → Module.{u_2, u_6} R (Ms i)
inst_3 : Fintype η
inst_4 : DecidableEq η
s : (j : η) → Basis.{u_5, u_2, u_6} (ιs j) R (Ms j)
j : η
i i' : ιs j
pos :
  Eq.{u_2 + 1} (α := R)
    (((({ toFun := fun (f : (i : η) → Ms i) (i : η) ↦ ((s i).repr : (a : Ms i) → ιs i →₀ R) (f i), map_add' := ⋯,
                  map_smul' := ⋯ } :
                (a : (j : η) → Ms j) → (i : η) → ιs i →₀ R)
              (single (M := Ms) j ((s j : (a : ιs j) → Ms j) i)) j :
            Finsupp.{u_5, u_2} (ιs j) R) :
          (a : ιs j) → R)
        i' :
      R)
    ((Finsupp.single (Sigma.mk (β := fun (j : η) ↦ ιs j) j i) 1 : (a : (j : η) × ιs j) → R)
        (Sigma.mk (β := fun (j : η) ↦ ιs j) j i') :
      R)
⊢ Eq.{u_2 + 1} (α := R)
    (((((Pi.basis (ιs := ιs) (Ms := Ms) s).repr : (a : (j : η) → Ms j) → (j : η) × ιs j →₀ R)
              (single (M := Ms) j ((s j : (a : ιs j) → Ms j) i)) :
            (j : η) × ιs j →₀ R) :
          (a : (j : η) × ιs j) → R)
        (Sigma.mk (β := fun (j : η) ↦ ιs j) j i') :
      R)
    ((Finsupp.single (Sigma.mk (β := fun (j : η) ↦ ιs j) j i) 1 : (a : (j : η) × ιs j) → R)
        (Sigma.mk (β := fun (j : η) ↦ ιs j) j i') :
      R)

Tactic:
simp only [Pi.basis, LinearEquiv.trans_apply,
      LinearEquiv.piCongrRight, Finsupp.sigmaFinsuppLEquivPiFinsupp_symm_apply,
      Basis.repr_symm_apply, LinearEquiv.coe_mk]

Premises used: LinearEquiv.coe_mk, Finsupp.sigmaFinsuppLEquivPiFinsupp_symm_apply, Pi.basis, LinearEquiv.trans_apply, LinearEquiv.piCongrRight, Module.Basis.repr_symm_apply
-- Module: Mathlib.LinearAlgebra.StdBasis
Goal:
R : Type u_2
η : Type u_4
ιs : η → Type u_5
Ms : η → Type u_6
inst : Semiring R
inst_1 : (i : η) → AddCommMonoid (Ms i)
inst_2 : (i : η) → Module.{u_2, u_6} R (Ms i)
inst_3 : Fintype η
inst_4 : DecidableEq η
s : (j : η) → Basis.{u_5, u_2, u_6} (ιs j) R (Ms j)
j : η
i i' : ιs j
pos :
  Eq.{u_2 + 1} (α := R)
    ((Finsupp.single (Sigma.mk (β := fun (j : η) ↦ ιs j) j i) 1 : (a : (j : η) × ιs j) → R)
        (Sigma.mk (β := fun (j : η) ↦ ιs j) j i') :
      R)
    (((({ toFun := fun (f : (i : η) → Ms i) (i : η) ↦ ((s i).repr : (a : Ms i) → ιs i →₀ R) (f i), map_add' := ⋯,
                  map_smul' := ⋯ } :
                (a : (j : η) → Ms j) → (i : η) → ιs i →₀ R)
              (single (M := Ms) j ((s j : (a : ιs j) → Ms j) i)) j :
            Finsupp.{u_5, u_2} (ιs j) R) :
          (a : ιs j) → R)
        i' :
      R)
⊢ Eq.{u_2 + 1} (α := R)
    (((({ toFun := fun (f : (i : η) → Ms i) (i : η) ↦ ((s i).repr : (a : Ms i) → ιs i →₀ R) (f i), map_add' := ⋯,
                  map_smul' := ⋯ } :
                (a : (j : η) → Ms j) → (i : η) → ιs i →₀ R)
              (single (M := Ms) j ((s j : (a : ιs j) → Ms j) i)) j :
            Finsupp.{u_5, u_2} (ιs j) R) :
          (a : ιs j) → R)
        i' :
      R)
    ((Finsupp.single (Sigma.mk (β := fun (j : η) ↦ ιs j) j i) 1 : (a : (j : η) × ιs j) → R)
        (Sigma.mk (β := fun (j : η) ↦ ιs j) j i') :
      R)

Tactic:
symm
-- Module: Mathlib.LinearAlgebra.StdBasis
Goal:
R : Type u_2
η : Type u_4
ιs : η → Type u_5
Ms : η → Type u_6
inst : Semiring R
inst_1 : (i : η) → AddCommMonoid (Ms i)
inst_2 : (i : η) → Module.{u_2, u_6} R (Ms i)
inst_3 : Fintype η
inst_4 : DecidableEq η
s : (j : η) → Basis.{u_5, u_2, u_6} (ιs j) R (Ms j)
j : η
i i' : ιs j
⊢ Eq.{u_2 + 1} (α := R)
    ((Finsupp.single (Sigma.mk (β := fun (j : η) ↦ ιs j) j i) 1 : (a : (j : η) × ιs j) → R)
        (Sigma.mk (β := fun (j : η) ↦ ιs j) j i') :
      R)
    (((({ toFun := fun (f : (i : η) → Ms i) (i : η) ↦ ((s i).repr : (a : Ms i) → ιs i →₀ R) (f i), map_add' := ⋯,
                  map_smul' := ⋯ } :
                (a : (j : η) → Ms j) → (i : η) → ιs i →₀ R)
              (single (M := Ms) j ((s j : (a : ιs j) → Ms j) i)) j :
            Finsupp.{u_5, u_2} (ιs j) R) :
          (a : ιs j) → R)
        i' :
      R)

Tactic:
simp [Finsupp.single_apply]

Premises used: Finsupp.single_apply
-- Module: Mathlib.LinearAlgebra.StdBasis
Goal:
R : Type u_2
η : Type u_4
ιs : η → Type u_5
Ms : η → Type u_6
inst : Semiring R
inst_1 : (i : η) → AddCommMonoid (Ms i)
inst_2 : (i : η) → Module.{u_2, u_6} R (Ms i)
inst_3 : Fintype η
inst_4 : DecidableEq η
s : (j : η) → Basis.{u_5, u_2, u_6} (ιs j) R (Ms j)
j : η
i : ιs j
j' : η
i' : ιs j'
hj : ¬j = j'
neg :
  Eq.{u_2 + 1} (α := R)
    (((({ toFun := fun (f : (i : η) → Ms i) (i : η) ↦ ((s i).repr : (a : Ms i) → ιs i →₀ R) (f i), map_add' := ⋯,
                  map_smul' := ⋯,
                  invFun := fun (f : (i : η) → Finsupp.{u_5, u_2} (ιs i) R) (i : η) ↦
                    ((s i).repr.symm : (a : ιs i →₀ R) → Ms i) (f i),
                  left_inv := ⋯, right_inv := ⋯ } :
                (a : (j : η) → Ms j) → (i : η) → ιs i →₀ R)
              (single (M := Ms) j ((s j : (a : ιs j) → Ms j) i)) j' :
            Finsupp.{u_5, u_2} (ιs j') R) :
          (a : ιs j') → R)
        i' :
      R)
    ((Finsupp.single (Sigma.mk (β := fun (j : η) ↦ ιs j) j i) 1 : (a : (j : η) × ιs j) → R)
        (Sigma.mk (β := fun (j : η) ↦ ιs j) j' i') :
      R)
⊢ Eq.{u_2 + 1} (α := R)
    (((((Pi.basis (ιs := ιs) (Ms := Ms) s).repr : (a : (j : η) → Ms j) → (j : η) × ιs j →₀ R)
              (single (M := Ms) j ((s j : (a : ιs j) → Ms j) i)) :
            (j : η) × ιs j →₀ R) :
          (a : (j : η) × ιs j) → R)
        (Sigma.mk (β := fun (j : η) ↦ ιs j) j' i') :
      R)
    ((Finsupp.single (Sigma.mk (β := fun (j : η) ↦ ιs j) j i) 1 : (a : (j : η) × ιs j) → R)
        (Sigma.mk (β := fun (j : η) ↦ ιs j) j' i') :
      R)

Tactic:
simp only [Pi.basis, LinearEquiv.trans_apply, Finsupp.sigmaFinsuppLEquivPiFinsupp_symm_apply,
    LinearEquiv.piCongrRight]

Premises used: Finsupp.sigmaFinsuppLEquivPiFinsupp_symm_apply, Pi.basis, LinearEquiv.trans_apply, LinearEquiv.piCongrRight
-- Module: Mathlib.LinearAlgebra.StdBasis
Goal:
R : Type u_2
η : Type u_4
ιs : η → Type u_5
Ms : η → Type u_6
inst : Semiring R
inst_1 : (i : η) → AddCommMonoid (Ms i)
inst_2 : (i : η) → Module.{u_2, u_6} R (Ms i)
inst_3 : Fintype η
inst_4 : DecidableEq η
s : (j : η) → Basis.{u_5, u_2, u_6} (ιs j) R (Ms j)
j : η
i : ιs j
j' : η
i' : ιs j'
hj : ¬j = j'
neg :
  Eq.{u_2 + 1} (α := R)
    (((((s j').repr : (a : Ms j') → ιs j' →₀ R) (single (M := Ms) j ((s j : (a : ιs j) → Ms j) i) j') :
            Finsupp.{u_5, u_2} (ιs j') R) :
          (a : ιs j') → R)
        i' :
      R)
    ((Finsupp.single (Sigma.mk (β := fun (j : η) ↦ ιs j) j i) 1 : (a : (j : η) × ιs j) → R)
        (Sigma.mk (β := fun (j : η) ↦ ιs j) j' i') :
      R)
⊢ Eq.{u_2 + 1} (α := R)
    (((({ toFun := fun (f : (i : η) → Ms i) (i : η) ↦ ((s i).repr : (a : Ms i) → ιs i →₀ R) (f i), map_add' := ⋯,
                  map_smul' := ⋯,
                  invFun := fun (f : (i : η) → Finsupp.{u_5, u_2} (ιs i) R) (i : η) ↦
                    ((s i).repr.symm : (a : ιs i →₀ R) → Ms i) (f i),
                  left_inv := ⋯, right_inv := ⋯ } :
                (a : (j : η) → Ms j) → (i : η) → ιs i →₀ R)
              (single (M := Ms) j ((s j : (a : ιs j) → Ms j) i)) j' :
            Finsupp.{u_5, u_2} (ιs j') R) :
          (a : ιs j') → R)
        i' :
      R)
    ((Finsupp.single (Sigma.mk (β := fun (j : η) ↦ ιs j) j i) 1 : (a : (j : η) × ιs j) → R)
        (Sigma.mk (β := fun (j : η) ↦ ιs j) j' i') :
      R)

Tactic:
dsimp
-- Module: Mathlib.LinearAlgebra.StdBasis
Goal:
R : Type u_2
η : Type u_4
ιs : η → Type u_5
Ms : η → Type u_6
inst : Semiring R
inst_1 : (i : η) → AddCommMonoid (Ms i)
inst_2 : (i : η) → Module.{u_2, u_6} R (Ms i)
inst_3 : Fintype η
inst_4 : DecidableEq η
s : (j : η) → Basis.{u_5, u_2, u_6} (ιs j) R (Ms j)
j : η
i : ιs j
j' : η
i' : ιs j'
hj : ¬j = j'
neg : Sigma.mk (β := fun (j : η) ↦ ιs j) j' i' ≠ Sigma.mk (β := fun (j : η) ↦ ιs j) j i
⊢ Eq.{u_2 + 1} (α := R)
    (((((s j').repr : (a : Ms j') → ιs j' →₀ R) (single (M := Ms) j ((s j : (a : ιs j) → Ms j) i) j') :
            Finsupp.{u_5, u_2} (ιs j') R) :
          (a : ιs j') → R)
        i' :
      R)
    ((Finsupp.single (Sigma.mk (β := fun (j : η) ↦ ιs j) j i) 1 : (a : (j : η) × ιs j) → R)
        (Sigma.mk (β := fun (j : η) ↦ ιs j) j' i') :
      R)

Tactic:
rw [Pi.single_eq_of_ne (Ne.symm hj), map_zero, Finsupp.zero_apply,
    Finsupp.single_eq_of_ne]

Premises used: Finsupp.single_eq_of_ne, map_zero, Pi.single_eq_of_ne, Ne.symm, Finsupp.zero_apply
-- Module: Mathlib.LinearAlgebra.StdBasis
Goal:
R : Type u_2
η : Type u_4
ιs : η → Type u_5
Ms : η → Type u_6
inst : Semiring R
inst_1 : (i : η) → AddCommMonoid (Ms i)
inst_2 : (i : η) → Module.{u_2, u_6} R (Ms i)
inst_3 : Fintype η
inst_4 : DecidableEq η
s : (j : η) → Basis.{u_5, u_2, u_6} (ιs j) R (Ms j)
j : η
i : ιs j
hj : ¬j = j
⊢ False

Tactic:
contradiction
-- Module: Mathlib.LinearAlgebra.StdBasis
Goal:
R : Type u_2
η : Type u_4
ιs : η → Type u_5
Ms : η → Type u_6
inst : Semiring R
inst_1 : (i : η) → AddCommMonoid (Ms i)
inst_2 : (i : η) → Module.{u_2, u_6} R (Ms i)
inst_3 : Fintype η
inst_4 : DecidableEq η
s : (j : η) → Basis.{u_5, u_2, u_6} (ιs j) R (Ms j)
ji : (j : η) × ιs j
⊢ Eq (α := (j : η) × ιs j →₀ R)
    (((Pi.basis (ιs := ιs) (Ms := Ms) s).repr : (a : (j : η) → Ms j) → (j : η) × ιs j →₀ R)
        (single (M := Ms) (ji.fst (β := fun (j : η) ↦ ιs j))
          ((s (ji.fst (β := fun (j : η) ↦ ιs j)) : (a : ιs ji.fst) → Ms ji.fst) (ji.snd (β := fun (j : η) ↦ ιs j)))) :
      (j : η) × ιs j →₀ R)
    (Finsupp.single ji 1 : (j : η) × ιs j →₀ R)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.StdBasis
Goal:
R : Type u_2
η : Type u_4
ιs : η → Type u_5
Ms : η → Type u_6
inst : Semiring R
inst_1 : (i : η) → AddCommMonoid (Ms i)
inst_2 : (i : η) → Module.{u_2, u_6} R (Ms i)
inst_3 : Fintype η
s : (j : η) → Basis.{u_5, u_2, u_6} (ιs j) R (Ms j)
x : (j : η) → Ms j
ji : (j : η) × ιs j
⊢ Eq.{u_2 + 1} (α := R)
    (((((Pi.basis (ιs := ιs) (Ms := Ms) s).repr : (a : (j : η) → Ms j) → (j : η) × ιs j →₀ R) x : (j : η) × ιs j →₀ R) :
          (a : (j : η) × ιs j) → R)
        ji :
      R)
    ((((Basis.repr (s (ji.fst (β := fun (j : η) ↦ ιs j))) : (a : Ms ji.fst) → ιs ji.fst →₀ R)
              (x (ji.fst (β := fun (j : η) ↦ ιs j))) :
            Finsupp.{u_5, u_2} (ιs (ji.fst (β := fun (j : η) ↦ ιs j))) R) :
          (a : ιs ji.fst) → R)
        (ji.snd (β := fun (j : η) ↦ ιs j)) :
      R)

Tactic:
rfl

Premises used: rfl