ι : Type u_2
ι' : Type ?u.421677
R : Type u_3
R₂ : Type ?u.421683
K : Type ?u.421686
M : Type u_1
M' : Type ?u.421692
M'' : Type ?u.421695
V : Type u
V' : Type ?u.421700
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 : ι
h : optParam (↑b i ∈ Finset.image (↑b) Finset.univ) (_ : ↑b i ∈ Finset.image (↑b) Finset.univ)
⊢ ↑(↑(Equiv.subtypeEquiv (Equiv.refl M) (_ : ∀ (a : M), a ∈ range ↑b ↔ a ∈ Finset.image (↑b) Finset.univ)).symm
        { val := ↑b i, property := h }) =
    ↑b i
ι : Type u_2
ι' : Type ?u.421677
R : Type u_3
R₂ : Type ?u.421683
K : Type ?u.421686
M : Type u_1
M' : Type ?u.421692
M'' : Type ?u.421695
V : Type u
V' : Type ?u.421700
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 : ι
h : optParam (↑b i ∈ Finset.image (↑b) Finset.univ) (_ : ↑b i ∈ Finset.image (↑b) Finset.univ)
⊢ ↑(reindexFinsetRange b) { val := ↑b i, property := h } = ↑b i
rw [reindexFinsetRange, reindex_apply, reindexRange_apply]
no goals
ι : Type u_2
ι' : Type ?u.421677
R : Type u_3
R₂ : Type ?u.421683
K : Type ?u.421686
M : Type u_1
M' : Type ?u.421692
M'' : Type ?u.421695
V : Type u
V' : Type ?u.421700
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 : ι
h : optParam (↑b i ∈ Finset.image (↑b) Finset.univ) (_ : ↑b i ∈ Finset.image (↑b) Finset.univ)
⊢ ↑(↑(Equiv.subtypeEquiv (Equiv.refl M) (_ : ∀ (a : M), a ∈ range ↑b ↔ a ∈ Finset.image (↑b) Finset.univ)).symm
        { val := ↑b i, property := h }) =
    ↑b i
rfl