case h.mk
ι : Type u_3
ι' : Type ?u.425289
R : Type u_1
R₂ : Type ?u.425295
K : Type ?u.425298
M : Type u_2
M' : Type ?u.425304
M'' : Type ?u.425307
V : Type u
V' : Type ?u.425312
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
b b₁ : Basis ι R M
i✝ : ι
c : R
x : M
b' : Basis ι' R M'
e : ι ≃ ι'
inst✝¹ : Fintype ι
inst✝ : DecidableEq M
i : ι
bi : M
hbi : bi ∈ Finset.image (↑b) Finset.univ
⊢ ↑(↑(reindexFinsetRange b).repr (↑b i)) { val := bi, property := hbi } =
    ↑(Finsupp.single { val := ↑b i, property := (_ : ↑b i ∈ Finset.image (↑b) Finset.univ) } 1)
      { val := bi, property := hbi }
ι : Type u_3
ι' : Type ?u.425289
R : Type u_1
R₂ : Type ?u.425295
K : Type ?u.425298
M : Type u_2
M' : Type ?u.425304
M'' : Type ?u.425307
V : Type u
V' : Type ?u.425312
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
b b₁ : Basis ι R M
i✝ : ι
c : R
x : M
b' : Basis ι' R M'
e : ι ≃ ι'
inst✝¹ : Fintype ι
inst✝ : DecidableEq M
i : ι
⊢ ↑(reindexFinsetRange b).repr (↑b i) =
    Finsupp.single { val := ↑b i, property := (_ : ↑b i ∈ Finset.image (↑b) Finset.univ) } 1
ext ⟨bi, hbi⟩
case h.mk
ι : Type u_3
ι' : Type ?u.425289
R : Type u_1
R₂ : Type ?u.425295
K : Type ?u.425298
M : Type u_2
M' : Type ?u.425304
M'' : Type ?u.425307
V : Type u
V' : Type ?u.425312
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
b b₁ : Basis ι R M
i✝ : ι
c : R
x : M
b' : Basis ι' R M'
e : ι ≃ ι'
inst✝¹ : Fintype ι
inst✝ : DecidableEq M
i : ι
bi : M
hbi : bi ∈ Finset.image (↑b) Finset.univ
⊢ ↑(Finsupp.single { val := ↑b i, property := (_ : ↑b i ∈ range ↑b) } 1)
      (↑(Equiv.subtypeEquiv (Equiv.refl M) (_ : ∀ (a : M), a ∈ range ↑b ↔ a ∈ Finset.image (↑b) Finset.univ)).symm
        { val := bi, property := hbi }) =
    ↑(Finsupp.single { val := ↑b i, property := (_ : ↑b i ∈ Finset.image (↑b) Finset.univ) } 1)
      { val := bi, property := hbi }
case h.mk
ι : Type u_3
ι' : Type ?u.425289
R : Type u_1
R₂ : Type ?u.425295
K : Type ?u.425298
M : Type u_2
M' : Type ?u.425304
M'' : Type ?u.425307
V : Type u
V' : Type ?u.425312
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
b b₁ : Basis ι R M
i✝ : ι
c : R
x : M
b' : Basis ι' R M'
e : ι ≃ ι'
inst✝¹ : Fintype ι
inst✝ : DecidableEq M
i : ι
bi : M
hbi : bi ∈ Finset.image (↑b) Finset.univ
⊢ ↑(↑(reindexFinsetRange b).repr (↑b i)) { val := bi, property := hbi } =
    ↑(Finsupp.single { val := ↑b i, property := (_ : ↑b i ∈ Finset.image (↑b) Finset.univ) } 1)
      { val := bi, property := hbi }
rw [reindexFinsetRange, repr_reindex, Finsupp.mapDomain_equiv_apply, reindexRange_repr_self]
no goals
case h.mk
ι : Type u_3
ι' : Type ?u.425289
R : Type u_1
R₂ : Type ?u.425295
K : Type ?u.425298
M : Type u_2
M' : Type ?u.425304
M'' : Type ?u.425307
V : Type u
V' : Type ?u.425312
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
b b₁ : Basis ι R M
i✝ : ι
c : R
x : M
b' : Basis ι' R M'
e : ι ≃ ι'
inst✝¹ : Fintype ι
inst✝ : DecidableEq M
i : ι
bi : M
hbi : bi ∈ Finset.image (↑b) Finset.univ
⊢ ↑(Finsupp.single { val := ↑b i, property := (_ : ↑b i ∈ range ↑b) } 1)
      (↑(Equiv.subtypeEquiv (Equiv.refl M) (_ : ∀ (a : M), a ∈ range ↑b ↔ a ∈ Finset.image (↑b) Finset.univ)).symm
        { val := bi, property := hbi }) =
    ↑(Finsupp.single { val := ↑b i, property := (_ : ↑b i ∈ Finset.image (↑b) Finset.univ) } 1)
      { val := bi, property := hbi }
simp [Finsupp.single_apply]