-- Mathlib/LinearAlgebra/StdBasis.lean
theorem basis_repr_single [DecidableEq η] (s : ∀ j, Basis (ιs j) R (Ms j)) (j i) :
    (Pi.basis s).repr (Pi.single j (s j i)) = Finsupp.single ⟨j, i⟩ 1

Proof state:
case pos
R : Type u_1
η : Type u_2
ιs : η → Type u_3
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 ⟨j, i⟩ 1) ⟨j, i'⟩ = (Finsupp.single i 1) i'

Tactic:
simp [Finsupp.single_apply]

Result:
no goals

Proof state:
case h.mk
R : Type u_1
η : Type u_2
ιs : η → Type u_3
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 (single j ((s j) i))) ⟨j', i'⟩ = (Finsupp.single ⟨j, i⟩ 1) ⟨j', i'⟩

Tactic:
by_cases hj : j = j'

Result:
case pos
R : Type u_1
η : Type u_2
ιs : η → Type u_3
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 (single j ((s j) i))) ⟨j', i'⟩ = (Finsupp.single ⟨j, i⟩ 1) ⟨j', i'⟩

case neg
R : Type u_1
η : Type u_2
ιs : η → Type u_3
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 (single j ((s j) i))) ⟨j', i'⟩ = (Finsupp.single ⟨j, i⟩ 1) ⟨j', i'⟩

Proof state:
case neg
R : Type u_1
η : Type u_2
ιs : η → Type u_3
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 (single j ((s j) i))) ⟨j', i'⟩ = (Finsupp.single ⟨j, i⟩ 1) ⟨j', i'⟩

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

Result:
case neg
R : Type u_1
η : Type u_2
ιs : η → Type u_3
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'
⊢ ({ toFun := fun f i => (s i).repr (f i), map_add' := ⋯, map_smul' := ⋯, invFun := fun f i => (s i).repr.symm (f i),
          left_inv := ⋯, right_inv := ⋯ }
        (single j ((s j) i)) j')
      i' =
    (Finsupp.single ⟨j, i⟩ 1) ⟨j', i'⟩

Proof state:
case neg.refl
R : Type u_1
η : Type u_2
ιs : η → Type u_3
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

Tactic:
contradiction

Result:
no goals

Proof state:
case neg
R : Type u_1
η : Type u_2
ιs : η → Type u_3
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'
⊢ ({ toFun := fun f i => (s i).repr (f i), map_add' := ⋯, map_smul' := ⋯, invFun := fun f i => (s i).repr.symm (f i),
          left_inv := ⋯, right_inv := ⋯ }
        (single j ((s j) i)) j')
      i' =
    (Finsupp.single ⟨j, i⟩ 1) ⟨j', i'⟩

Tactic:
dsimp

Result:
case neg
R : Type u_1
η : Type u_2
ιs : η → Type u_3
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 (single j ((s j) i) j')) i' = (Finsupp.single ⟨j, i⟩ 1) ⟨j', i'⟩

Proof state:
R : Type u_1
η : Type u_2
ιs : η → Type u_3
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 (single j ((s j) i)) = Finsupp.single ⟨j, i⟩ 1

Tactic:
ext ⟨j', i'⟩

Result:
case h.mk
R : Type u_1
η : Type u_2
ιs : η → Type u_3
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 (single j ((s j) i))) ⟨j', i'⟩ = (Finsupp.single ⟨j, i⟩ 1) ⟨j', i'⟩

Proof state:
case neg
R : Type u_1
η : Type u_2
ιs : η → Type u_3
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 (single j ((s j) i) j')) i' = (Finsupp.single ⟨j, i⟩ 1) ⟨j', i'⟩

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

Result:
case neg
R : Type u_1
η : Type u_2
ιs : η → Type u_3
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'
⊢ ⟨j, i⟩ ≠ ⟨j', i'⟩

Proof state:
case pos
R : Type u_1
η : Type u_2
ιs : η → Type u_3
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 ⟨j, i⟩ 1) ⟨j, i'⟩

Tactic:
symm

Result:
case pos
R : Type u_1
η : Type u_2
ιs : η → Type u_3
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 ⟨j, i⟩ 1) ⟨j, i'⟩ = (Finsupp.single i 1) i'

Proof state:
case pos
R : Type u_1
η : Type u_2
ιs : η → Type u_3
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 (single j ((s j) i))) ⟨j', i'⟩ = (Finsupp.single ⟨j, i⟩ 1) ⟨j', i'⟩

Tactic:
subst hj

Result:
case pos
R : Type u_1
η : Type u_2
ιs : η → Type u_3
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 (single j ((s j) i))) ⟨j, i'⟩ = (Finsupp.single ⟨j, i⟩ 1) ⟨j, i'⟩

Proof state:
case neg
R : Type u_1
η : Type u_2
ιs : η → Type u_3
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'
⊢ ⟨j, i⟩ ≠ ⟨j', i'⟩

Tactic:
rintro ⟨⟩

Result:
case neg.refl
R : Type u_1
η : Type u_2
ιs : η → Type u_3
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