-- Mathlib/LinearAlgebra/Basis/Defs.lean
theorem reindexRange_self (i : ι) (h := Set.mem_range_self i) : b.reindexRange ⟨b i, h⟩ = b i

Proof state:
case neg
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
i : ι
h : optParam (b i ∈ range ⇑b) ⋯
htr : ¬Nontrivial R
this : Subsingleton R := not_nontrivial_iff_subsingleton.mp htr
⊢ b.reindexRange ⟨b i, h⟩ = b i

Tactic:
letI := Module.subsingleton R M

Result:
case neg
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
i : ι
h : optParam (b i ∈ range ⇑b) ⋯
htr : ¬Nontrivial R
this✝ : Subsingleton R := not_nontrivial_iff_subsingleton.mp htr
this : Subsingleton M := Module.subsingleton R M
⊢ b.reindexRange ⟨b i, h⟩ = b i

Proof state:
case neg
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
i : ι
h : optParam (b i ∈ range ⇑b) ⋯
htr : ¬Nontrivial R
this✝ : Subsingleton R := not_nontrivial_iff_subsingleton.mp htr
this : Subsingleton M := Module.subsingleton R M
⊢ b.reindexRange ⟨b i, h⟩ = b i

Tactic:
simp [reindexRange, eq_iff_true_of_subsingleton]

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
i : ι
h : optParam (b i ∈ range ⇑b) ⋯
⊢ b.reindexRange ⟨b i, h⟩ = b i

Tactic:
by_cases htr : Nontrivial R

Result:
case pos
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
i : ι
h : optParam (b i ∈ range ⇑b) ⋯
htr : Nontrivial R
⊢ b.reindexRange ⟨b i, h⟩ = b i

case neg
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
i : ι
h : optParam (b i ∈ range ⇑b) ⋯
htr : ¬Nontrivial R
⊢ b.reindexRange ⟨b i, h⟩ = b i

Proof state:
case pos
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
i : ι
h : optParam (b i ∈ range ⇑b) ⋯
htr : Nontrivial R
⊢ b.reindexRange ⟨b i, h⟩ = b i

Tactic:
letI := htr

Result:
case pos
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
i : ι
h : optParam (b i ∈ range ⇑b) ⋯
htr : Nontrivial R
this : Nontrivial R := htr
⊢ b.reindexRange ⟨b i, h⟩ = b i

Proof state:
case neg
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
i : ι
h : optParam (b i ∈ range ⇑b) ⋯
htr : ¬Nontrivial R
⊢ b.reindexRange ⟨b i, h⟩ = b i

Tactic:
letI : Subsingleton R := not_nontrivial_iff_subsingleton.mp htr

Result:
case neg
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
i : ι
h : optParam (b i ∈ range ⇑b) ⋯
htr : ¬Nontrivial R
this : Subsingleton R := not_nontrivial_iff_subsingleton.mp htr
⊢ b.reindexRange ⟨b i, h⟩ = b i

Proof state:
case pos
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
i : ι
h : optParam (b i ∈ range ⇑b) ⋯
htr : Nontrivial R
this : Nontrivial R := htr
⊢ b.reindexRange ⟨b i, h⟩ = b i

Tactic:
simp [htr, reindexRange, reindex_apply, Equiv.apply_ofInjective_symm b.injective,
  Subtype.coe_mk]

Result:
no goals