case h.mk
R : Type u_3
η : Type u_1
ιs : η → Type u_2
Ms : η → Type u_4
inst✝⁴ : Semiring R
inst✝³ : (i : η) → AddCommMonoid (Ms i)
inst✝² : (i : η) → Module R (Ms i)
inst✝¹ : Fintype η
inst✝ : DecidableEq η
s : (j : η) → Basis (ιs j) R (Ms j)
j : η
i : ιs j
j' : η
i' : ιs j'
⊢ ↑(↑(Pi.basis s).repr (↑(stdBasis R Ms j) (↑(s j) i))) { fst := j', snd := i' } =
    ↑(Finsupp.single { fst := j, snd := i } 1) { fst := j', snd := i' }
R : Type u_3
η : Type u_1
ιs : η → Type u_2
Ms : η → Type u_4
inst✝⁴ : Semiring R
inst✝³ : (i : η) → AddCommMonoid (Ms i)
inst✝² : (i : η) → Module R (Ms i)
inst✝¹ : Fintype η
inst✝ : DecidableEq η
s : (j : η) → Basis (ιs j) R (Ms j)
j : η
i : ιs j
⊢ ↑(Pi.basis s).repr (↑(stdBasis R Ms j) (↑(s j) i)) = Finsupp.single { fst := j, snd := i } 1
ext ⟨j', i'⟩
case pos
R : Type u_3
η : Type u_1
ιs : η → Type u_2
Ms : η → Type u_4
inst✝⁴ : Semiring R
inst✝³ : (i : η) → AddCommMonoid (Ms i)
inst✝² : (i : η) → Module R (Ms i)
inst✝¹ : Fintype η
inst✝ : DecidableEq η
s : (j : η) → Basis (ιs j) R (Ms j)
j : η
i : ιs j
j' : η
i' : ιs j'
hj : j = j'
⊢ ↑(↑(Pi.basis s).repr (↑(stdBasis R Ms j) (↑(s j) i))) { fst := j', snd := i' } =
    ↑(Finsupp.single { fst := j, snd := i } 1) { fst := j', snd := i' }

case neg
R : Type u_3
η : Type u_1
ιs : η → Type u_2
Ms : η → Type u_4
inst✝⁴ : Semiring R
inst✝³ : (i : η) → AddCommMonoid (Ms i)
inst✝² : (i : η) → Module R (Ms i)
inst✝¹ : Fintype η
inst✝ : DecidableEq η
s : (j : η) → Basis (ιs j) R (Ms j)
j : η
i : ιs j
j' : η
i' : ιs j'
hj : ¬j = j'
⊢ ↑(↑(Pi.basis s).repr (↑(stdBasis R Ms j) (↑(s j) i))) { fst := j', snd := i' } =
    ↑(Finsupp.single { fst := j, snd := i } 1) { fst := j', snd := i' }
case h.mk
R : Type u_3
η : Type u_1
ιs : η → Type u_2
Ms : η → Type u_4
inst✝⁴ : Semiring R
inst✝³ : (i : η) → AddCommMonoid (Ms i)
inst✝² : (i : η) → Module R (Ms i)
inst✝¹ : Fintype η
inst✝ : DecidableEq η
s : (j : η) → Basis (ιs j) R (Ms j)
j : η
i : ιs j
j' : η
i' : ιs j'
⊢ ↑(↑(Pi.basis s).repr (↑(stdBasis R Ms j) (↑(s j) i))) { fst := j', snd := i' } =
    ↑(Finsupp.single { fst := j, snd := i } 1) { fst := j', snd := i' }
by_cases hj : j = j'
case neg
R : Type u_3
η : Type u_1
ιs : η → Type u_2
Ms : η → Type u_4
inst✝⁴ : Semiring R
inst✝³ : (i : η) → AddCommMonoid (Ms i)
inst✝² : (i : η) → Module R (Ms i)
inst✝¹ : Fintype η
inst✝ : DecidableEq η
s : (j : η) → Basis (ιs j) R (Ms j)
j : η
i : ιs j
j' : η
i' : ιs j'
hj : ¬j = j'
⊢ ↑(↑{
              toLinearMap :=
                {
                  toAddHom :=
                    { toFun := fun f i => ↑(s i).repr (f i),
                      map_add' :=
                        (_ :
                          ∀ (x y : (j : η) → (fun j => Ms j) j),
                            Equiv.toFun (AddEquiv.piCongrRight fun j => toAddEquiv (s j).repr).toEquiv (x + y) =
                              Equiv.toFun (AddEquiv.piCongrRight fun j => toAddEquiv (s j).repr).toEquiv x +
                                Equiv.toFun (AddEquiv.piCongrRight fun j => toAddEquiv (s j).repr).toEquiv y) },
                  map_smul' :=
                    (_ :
                      ∀ (c : R) (f : (i : η) → (fun j => Ms j) i),
                        AddHom.toFun
                            { toFun := fun f i => ↑(s i).repr (f i),
                              map_add' :=
                                (_ :
                                  ∀ (x y : (j : η) → (fun j => Ms j) j),
                                    Equiv.toFun (AddEquiv.piCongrRight fun j => toAddEquiv (s j).repr).toEquiv (x + y) =
                                      Equiv.toFun (AddEquiv.piCongrRight fun j => toAddEquiv (s j).repr).toEquiv x +
                                        Equiv.toFun (AddEquiv.piCongrRight fun j => toAddEquiv (s j).repr).toEquiv y) }
                            (c • f) =
                          ↑(RingHom.id R) c •
                            AddHom.toFun
                              { toFun := fun f i => ↑(s i).repr (f i),
                                map_add' :=
                                  (_ :
                                    ∀ (x y : (j : η) → (fun j => Ms j) j),
                                      Equiv.toFun (AddEquiv.piCongrRight fun j => toAddEquiv (s j).repr).toEquiv
                                          (x + y) =
                                        Equiv.toFun (AddEquiv.piCongrRight fun j => toAddEquiv (s j).repr).toEquiv x +
                                          Equiv.toFun (AddEquiv.piCongrRight fun j => toAddEquiv (s j).repr).toEquiv
                                            y) }
                              f) },
              invFun := fun f i => ↑(LinearEquiv.symm (s i).repr) (f i),
              left_inv :=
                (_ :
                  LeftInverse (AddEquiv.piCongrRight fun j => toAddEquiv (s j).repr).toEquiv.invFun
                    (AddEquiv.piCongrRight fun j => toAddEquiv (s j).repr).toEquiv.toFun),
              right_inv :=
                (_ :
                  Function.RightInverse (AddEquiv.piCongrRight fun j => toAddEquiv (s j).repr).toEquiv.invFun
                    (AddEquiv.piCongrRight fun j => toAddEquiv (s j).repr).toEquiv.toFun) }
          (↑(stdBasis R Ms j) (↑(s j) i)) j')
      i' =
    ↑(Finsupp.single { fst := j, snd := i } 1) { fst := j', snd := i' }
case neg
R : Type u_3
η : Type u_1
ιs : η → Type u_2
Ms : η → Type u_4
inst✝⁴ : Semiring R
inst✝³ : (i : η) → AddCommMonoid (Ms i)
inst✝² : (i : η) → Module R (Ms i)
inst✝¹ : Fintype η
inst✝ : DecidableEq η
s : (j : η) → Basis (ιs j) R (Ms j)
j : η
i : ιs j
j' : η
i' : ιs j'
hj : ¬j = j'
⊢ ↑(↑(Pi.basis s).repr (↑(stdBasis R Ms j) (↑(s j) i))) { fst := j', snd := i' } =
    ↑(Finsupp.single { fst := j, snd := i } 1) { fst := j', snd := i' }
simp only [Pi.basis, LinearEquiv.trans_apply, Finsupp.sigmaFinsuppLEquivPiFinsupp_symm_apply,
  LinearEquiv.piCongrRight]
case neg
R : Type u_3
η : Type u_1
ιs : η → Type u_2
Ms : η → Type u_4
inst✝⁴ : Semiring R
inst✝³ : (i : η) → AddCommMonoid (Ms i)
inst✝² : (i : η) → Module R (Ms i)
inst✝¹ : Fintype η
inst✝ : DecidableEq η
s : (j : η) → Basis (ιs j) R (Ms j)
j : η
i : ιs j
j' : η
i' : ιs j'
hj : ¬j = j'
⊢ ↑(↑(s j').repr (↑(stdBasis R Ms j) (↑(s j) i) j')) i' =
    ↑(Finsupp.single { fst := j, snd := i } 1) { fst := j', snd := i' }
case neg
R : Type u_3
η : Type u_1
ιs : η → Type u_2
Ms : η → Type u_4
inst✝⁴ : Semiring R
inst✝³ : (i : η) → AddCommMonoid (Ms i)
inst✝² : (i : η) → Module R (Ms i)
inst✝¹ : Fintype η
inst✝ : DecidableEq η
s : (j : η) → Basis (ιs j) R (Ms j)
j : η
i : ιs j
j' : η
i' : ιs j'
hj : ¬j = j'
⊢ ↑(↑{
              toLinearMap :=
                {
                  toAddHom :=
                    { toFun := fun f i => ↑(s i).repr (f i),
                      map_add' :=
                        (_ :
                          ∀ (x y : (j : η) → (fun j => Ms j) j),
                            Equiv.toFun (AddEquiv.piCongrRight fun j => toAddEquiv (s j).repr).toEquiv (x + y) =
                              Equiv.toFun (AddEquiv.piCongrRight fun j => toAddEquiv (s j).repr).toEquiv x +
                                Equiv.toFun (AddEquiv.piCongrRight fun j => toAddEquiv (s j).repr).toEquiv y) },
                  map_smul' :=
                    (_ :
                      ∀ (c : R) (f : (i : η) → (fun j => Ms j) i),
                        AddHom.toFun
                            { toFun := fun f i => ↑(s i).repr (f i),
                              map_add' :=
                                (_ :
                                  ∀ (x y : (j : η) → (fun j => Ms j) j),
                                    Equiv.toFun (AddEquiv.piCongrRight fun j => toAddEquiv (s j).repr).toEquiv (x + y) =
                                      Equiv.toFun (AddEquiv.piCongrRight fun j => toAddEquiv (s j).repr).toEquiv x +
                                        Equiv.toFun (AddEquiv.piCongrRight fun j => toAddEquiv (s j).repr).toEquiv y) }
                            (c • f) =
                          ↑(RingHom.id R) c •
                            AddHom.toFun
                              { toFun := fun f i => ↑(s i).repr (f i),
                                map_add' :=
                                  (_ :
                                    ∀ (x y : (j : η) → (fun j => Ms j) j),
                                      Equiv.toFun (AddEquiv.piCongrRight fun j => toAddEquiv (s j).repr).toEquiv
                                          (x + y) =
                                        Equiv.toFun (AddEquiv.piCongrRight fun j => toAddEquiv (s j).repr).toEquiv x +
                                          Equiv.toFun (AddEquiv.piCongrRight fun j => toAddEquiv (s j).repr).toEquiv
                                            y) }
                              f) },
              invFun := fun f i => ↑(LinearEquiv.symm (s i).repr) (f i),
              left_inv :=
                (_ :
                  LeftInverse (AddEquiv.piCongrRight fun j => toAddEquiv (s j).repr).toEquiv.invFun
                    (AddEquiv.piCongrRight fun j => toAddEquiv (s j).repr).toEquiv.toFun),
              right_inv :=
                (_ :
                  Function.RightInverse (AddEquiv.piCongrRight fun j => toAddEquiv (s j).repr).toEquiv.invFun
                    (AddEquiv.piCongrRight fun j => toAddEquiv (s j).repr).toEquiv.toFun) }
          (↑(stdBasis R Ms j) (↑(s j) i)) j')
      i' =
    ↑(Finsupp.single { fst := j, snd := i } 1) { fst := j', snd := i' }
dsimp
case neg
R : Type u_3
η : Type u_1
ιs : η → Type u_2
Ms : η → Type u_4
inst✝⁴ : Semiring R
inst✝³ : (i : η) → AddCommMonoid (Ms i)
inst✝² : (i : η) → Module R (Ms i)
inst✝¹ : Fintype η
inst✝ : DecidableEq η
s : (j : η) → Basis (ιs j) R (Ms j)
j : η
i : ιs j
j' : η
i' : ιs j'
hj : ¬j = j'
⊢ { fst := j, snd := i } ≠ { fst := j', snd := i' }
case neg
R : Type u_3
η : Type u_1
ιs : η → Type u_2
Ms : η → Type u_4
inst✝⁴ : Semiring R
inst✝³ : (i : η) → AddCommMonoid (Ms i)
inst✝² : (i : η) → Module R (Ms i)
inst✝¹ : Fintype η
inst✝ : DecidableEq η
s : (j : η) → Basis (ιs j) R (Ms j)
j : η
i : ιs j
j' : η
i' : ιs j'
hj : ¬j = j'
⊢ ↑(↑(s j').repr (↑(stdBasis R Ms j) (↑(s j) i) j')) i' =
    ↑(Finsupp.single { fst := j, snd := i } 1) { fst := j', snd := i' }
rw [stdBasis_ne _ _ _ _ (Ne.symm hj), LinearEquiv.map_zero, Finsupp.zero_apply,
  Finsupp.single_eq_of_ne]
case neg.refl
R : Type u_3
η : Type u_1
ιs : η → Type u_2
Ms : η → Type u_4
inst✝⁴ : Semiring R
inst✝³ : (i : η) → AddCommMonoid (Ms i)
inst✝² : (i : η) → Module R (Ms i)
inst✝¹ : Fintype η
inst✝ : DecidableEq η
s : (j : η) → Basis (ιs j) R (Ms j)
j : η
i : ιs j
hj : ¬j = j
⊢ False
case neg
R : Type u_3
η : Type u_1
ιs : η → Type u_2
Ms : η → Type u_4
inst✝⁴ : Semiring R
inst✝³ : (i : η) → AddCommMonoid (Ms i)
inst✝² : (i : η) → Module R (Ms i)
inst✝¹ : Fintype η
inst✝ : DecidableEq η
s : (j : η) → Basis (ιs j) R (Ms j)
j : η
i : ιs j
j' : η
i' : ιs j'
hj : ¬j = j'
⊢ { fst := j, snd := i } ≠ { fst := j', snd := i' }
rintro ⟨⟩
no goals
case neg.refl
R : Type u_3
η : Type u_1
ιs : η → Type u_2
Ms : η → Type u_4
inst✝⁴ : Semiring R
inst✝³ : (i : η) → AddCommMonoid (Ms i)
inst✝² : (i : η) → Module R (Ms i)
inst✝¹ : Fintype η
inst✝ : DecidableEq η
s : (j : η) → Basis (ιs j) R (Ms j)
j : η
i : ιs j
hj : ¬j = j
⊢ False
contradiction
case pos
R : Type u_3
η : Type u_1
ιs : η → Type u_2
Ms : η → Type u_4
inst✝⁴ : Semiring R
inst✝³ : (i : η) → AddCommMonoid (Ms i)
inst✝² : (i : η) → Module R (Ms i)
inst✝¹ : Fintype η
inst✝ : DecidableEq η
s : (j : η) → Basis (ιs j) R (Ms j)
j : η
i i' : ιs j
⊢ ↑(↑(Pi.basis s).repr (↑(stdBasis R Ms j) (↑(s j) i))) { fst := j, snd := i' } =
    ↑(Finsupp.single { fst := j, snd := i } 1) { fst := j, snd := i' }
case pos
R : Type u_3
η : Type u_1
ιs : η → Type u_2
Ms : η → Type u_4
inst✝⁴ : Semiring R
inst✝³ : (i : η) → AddCommMonoid (Ms i)
inst✝² : (i : η) → Module R (Ms i)
inst✝¹ : Fintype η
inst✝ : DecidableEq η
s : (j : η) → Basis (ιs j) R (Ms j)
j : η
i : ιs j
j' : η
i' : ιs j'
hj : j = j'
⊢ ↑(↑(Pi.basis s).repr (↑(stdBasis R Ms j) (↑(s j) i))) { fst := j', snd := i' } =
    ↑(Finsupp.single { fst := j, snd := i } 1) { fst := j', snd := i' }
subst hj
case pos
R : Type u_3
η : Type u_1
ιs : η → Type u_2
Ms : η → Type u_4
inst✝⁴ : Semiring R
inst✝³ : (i : η) → AddCommMonoid (Ms i)
inst✝² : (i : η) → Module R (Ms i)
inst✝¹ : Fintype η
inst✝ : DecidableEq η
s : (j : η) → Basis (ιs j) R (Ms j)
j : η
i i' : ιs j
⊢ ↑(Finsupp.single i 1) i' = ↑(Finsupp.single { fst := j, snd := i } 1) { fst := j, snd := i' }
case pos
R : Type u_3
η : Type u_1
ιs : η → Type u_2
Ms : η → Type u_4
inst✝⁴ : Semiring R
inst✝³ : (i : η) → AddCommMonoid (Ms i)
inst✝² : (i : η) → Module R (Ms i)
inst✝¹ : Fintype η
inst✝ : DecidableEq η
s : (j : η) → Basis (ιs j) R (Ms j)
j : η
i i' : ιs j
⊢ ↑(↑(Pi.basis s).repr (↑(stdBasis R Ms j) (↑(s j) i))) { fst := j, snd := i' } =
    ↑(Finsupp.single { fst := j, snd := i } 1) { fst := j, snd := i' }
simp only [Pi.basis, LinearEquiv.trans_apply, Basis.repr_self, stdBasis_same,
  LinearEquiv.piCongrRight, Finsupp.sigmaFinsuppLEquivPiFinsupp_symm_apply,
  Basis.repr_symm_apply, LinearEquiv.coe_mk, ne_eq, Sigma.mk.inj_iff, heq_eq_eq, true_and]
case pos
R : Type u_3
η : Type u_1
ιs : η → Type u_2
Ms : η → Type u_4
inst✝⁴ : Semiring R
inst✝³ : (i : η) → AddCommMonoid (Ms i)
inst✝² : (i : η) → Module R (Ms i)
inst✝¹ : Fintype η
inst✝ : DecidableEq η
s : (j : η) → Basis (ιs j) R (Ms j)
j : η
i i' : ιs j
⊢ ↑(Finsupp.single { fst := j, snd := i } 1) { fst := j, snd := i' } = ↑(Finsupp.single i 1) i'
case pos
R : Type u_3
η : Type u_1
ιs : η → Type u_2
Ms : η → Type u_4
inst✝⁴ : Semiring R
inst✝³ : (i : η) → AddCommMonoid (Ms i)
inst✝² : (i : η) → Module R (Ms i)
inst✝¹ : Fintype η
inst✝ : DecidableEq η
s : (j : η) → Basis (ιs j) R (Ms j)
j : η
i i' : ιs j
⊢ ↑(Finsupp.single i 1) i' = ↑(Finsupp.single { fst := j, snd := i } 1) { fst := j, snd := i' }
symm
no goals
case pos
R : Type u_3
η : Type u_1
ιs : η → Type u_2
Ms : η → Type u_4
inst✝⁴ : Semiring R
inst✝³ : (i : η) → AddCommMonoid (Ms i)
inst✝² : (i : η) → Module R (Ms i)
inst✝¹ : Fintype η
inst✝ : DecidableEq η
s : (j : η) → Basis (ιs j) R (Ms j)
j : η
i i' : ιs j
⊢ ↑(Finsupp.single { fst := j, snd := i } 1) { fst := j, snd := i' } = ↑(Finsupp.single i 1) i'
exact
  Finsupp.single_apply_left
    (fun i i' (h : (⟨j, i⟩ : Σj, ιs j) = ⟨j, i'⟩) => eq_of_heq (Sigma.mk.inj_iff.mp h).2) _ _ _