case mk
ι : Type u_2
ι' : Type ?u.423699
R : Type u_3
R₂ : Type ?u.423705
K : Type ?u.423708
M : Type u_1
M' : Type ?u.423714
M'' : Type ?u.423717
V : Type u
V' : Type ?u.423722
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
bi : M
hbi : bi ∈ Finset.image (↑b) Finset.univ
⊢ ↑(reindexFinsetRange b) { val := bi, property := hbi } = ↑{ val := bi, property := hbi }
ι : Type u_2
ι' : Type ?u.423699
R : Type u_3
R₂ : Type ?u.423705
K : Type ?u.423708
M : Type u_1
M' : Type ?u.423714
M'' : Type ?u.423717
V : Type u
V' : Type ?u.423722
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
x : { x // x ∈ Finset.image (↑b) Finset.univ }
⊢ ↑(reindexFinsetRange b) x = ↑x
rcases x with ⟨bi, hbi⟩
case mk.intro.intro
ι : Type u_2
ι' : Type ?u.423699
R : Type u_3
R₂ : Type ?u.423705
K : Type ?u.423708
M : Type u_1
M' : Type ?u.423714
M'' : Type ?u.423717
V : Type u
V' : Type ?u.423722
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 : ι
hbi : ↑b i ∈ Finset.image (↑b) Finset.univ
⊢ ↑(reindexFinsetRange b) { val := ↑b i, property := hbi } = ↑{ val := ↑b i, property := hbi }
case mk
ι : Type u_2
ι' : Type ?u.423699
R : Type u_3
R₂ : Type ?u.423705
K : Type ?u.423708
M : Type u_1
M' : Type ?u.423714
M'' : Type ?u.423717
V : Type u
V' : Type ?u.423722
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
bi : M
hbi : bi ∈ Finset.image (↑b) Finset.univ
⊢ ↑(reindexFinsetRange b) { val := bi, property := hbi } = ↑{ val := bi, property := hbi }
rcases Finset.mem_image.mp hbi with ⟨i, -, rfl⟩
no goals
case mk.intro.intro
ι : Type u_2
ι' : Type ?u.423699
R : Type u_3
R₂ : Type ?u.423705
K : Type ?u.423708
M : Type u_1
M' : Type ?u.423714
M'' : Type ?u.423717
V : Type u
V' : Type ?u.423722
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 : ι
hbi : ↑b i ∈ Finset.image (↑b) Finset.univ
⊢ ↑(reindexFinsetRange b) { val := ↑b i, property := hbi } = ↑{ val := ↑b i, property := hbi }
exact b.reindexFinsetRange_self i