case mk.intro
ι : Type u_2
ι' : Type ?u.390057
R : Type u_3
R₂ : Type ?u.390063
K : Type ?u.390066
M : Type u_1
M' : Type ?u.390072
M'' : Type ?u.390075
V : Type u
V' : Type ?u.390080
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 : ι ≃ ι'
i : ι
⊢ ↑(reindexRange b) { val := ↑b i, property := (_ : ∃ y, ↑b y = ↑b i) } =
    ↑{ val := ↑b i, property := (_ : ∃ y, ↑b y = ↑b i) }
ι : Type u_2
ι' : Type ?u.390057
R : Type u_3
R₂ : Type ?u.390063
K : Type ?u.390066
M : Type u_1
M' : Type ?u.390072
M'' : Type ?u.390075
V : Type u
V' : Type ?u.390080
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 : ι ≃ ι'
x : ↑(range ↑b)
⊢ ↑(reindexRange b) x = ↑x
rcases x with ⟨bi, ⟨i, rfl⟩⟩
no goals
case mk.intro
ι : Type u_2
ι' : Type ?u.390057
R : Type u_3
R₂ : Type ?u.390063
K : Type ?u.390066
M : Type u_1
M' : Type ?u.390072
M'' : Type ?u.390075
V : Type u
V' : Type ?u.390080
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 : ι ≃ ι'
i : ι
⊢ ↑(reindexRange b) { val := ↑b i, property := (_ : ∃ y, ↑b y = ↑b i) } =
    ↑{ val := ↑b i, property := (_ : ∃ y, ↑b y = ↑b i) }
exact b.reindexRange_self i