-- Mathlib/LinearAlgebra/Basis/Defs.lean
theorem reindexRange_repr' (x : M) {bi : M} {i : ι} (h : b i = bi) :
    b.reindexRange.repr x ⟨bi, ⟨i, h⟩⟩ = b.repr x i

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
x : M
i : ι
a✝ : Nontrivial R
⊢ ∀ (x y : M),
    (fun x i => (b.reindexRange.repr x) ⟨b i, ⋯⟩) (x + y) =
      (fun x i => (b.reindexRange.repr x) ⟨b i, ⋯⟩) x + (fun x i => (b.reindexRange.repr x) ⟨b i, ⋯⟩) y

Tactic:
intro x y

Result:
ι : 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
x✝ : M
i : ι
a✝ : Nontrivial R
x y : M
⊢ (fun x i => (b.reindexRange.repr x) ⟨b i, ⋯⟩) (x + y) =
    (fun x i => (b.reindexRange.repr x) ⟨b i, ⋯⟩) x + (fun x i => (b.reindexRange.repr x) ⟨b i, ⋯⟩) y

Proof state:
case h.hf
ι : 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
x : M
i✝ : ι
a✝ : Nontrivial R
i j : ι
⊢ Injective fun i => ⟨b i, ⋯⟩

Tactic:
exact fun i j h => b.injective (Subtype.mk.inj h)

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
x : M
i✝ : ι
a✝ : Nontrivial R
i : ι
⊢ (fun x i => (b.reindexRange.repr x) ⟨b i, ⋯⟩) (b i) = ⇑(single i 1)

Tactic:
ext j

Result:
case h
ι : 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
x : M
i✝ : ι
a✝ : Nontrivial R
i j : ι
⊢ (fun x i => (b.reindexRange.repr x) ⟨b i, ⋯⟩) (b i) j = (single i 1) j

Proof state:
case h
ι : 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
x✝ : M
i✝ : ι
a✝ : Nontrivial R
x y : M
i : ι
⊢ (fun x i => (b.reindexRange.repr x) ⟨b i, ⋯⟩) (x + y) i =
    ((fun x i => (b.reindexRange.repr x) ⟨b i, ⋯⟩) x + (fun x i => (b.reindexRange.repr x) ⟨b i, ⋯⟩) y) i

Tactic:
simp only [Pi.add_apply, LinearEquiv.map_add, Finsupp.coe_add]

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
x✝ : M
i : ι
a✝ : Nontrivial R
x y : M
⊢ (fun x i => (b.reindexRange.repr x) ⟨b i, ⋯⟩) (x + y) =
    (fun x i => (b.reindexRange.repr x) ⟨b i, ⋯⟩) x + (fun x i => (b.reindexRange.repr x) ⟨b i, ⋯⟩) y

Tactic:
ext i

Result:
case h
ι : 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
x✝ : M
i✝ : ι
a✝ : Nontrivial R
x y : M
i : ι
⊢ (fun x i => (b.reindexRange.repr x) ⟨b i, ⋯⟩) (x + y) i =
    ((fun x i => (b.reindexRange.repr x) ⟨b i, ⋯⟩) x + (fun x i => (b.reindexRange.repr x) ⟨b i, ⋯⟩) y) i

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
x : M
i : ι
a✝ : Nontrivial R
⊢ ∀ (c : R) (x : M),
    (fun x i => (b.reindexRange.repr x) ⟨b i, ⋯⟩) (c • x) = c • (fun x i => (b.reindexRange.repr x) ⟨b i, ⋯⟩) x

Tactic:
intro c x

Result:
ι : 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
x✝ : M
i : ι
a✝ : Nontrivial R
c : R
x : M
⊢ (fun x i => (b.reindexRange.repr x) ⟨b i, ⋯⟩) (c • x) = c • (fun x i => (b.reindexRange.repr x) ⟨b i, ⋯⟩) x

Proof state:
case h
ι : 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
x : M
i✝ : ι
a✝ : Nontrivial R
i j : ι
⊢ (single ⟨b i, ⋯⟩ 1) ⟨b j, ⋯⟩ = (single i 1) j

Tactic:
apply Finsupp.single_apply_left (f := fun i => (⟨b i, _⟩ : Set.range b))

Result:
case h.hf
ι : 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
x : M
i✝ : ι
a✝ : Nontrivial R
i j : ι
⊢ Injective fun i => ⟨b i, ⋯⟩

Proof state:
case h
ι : 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
x : M
i✝ : ι
a✝ : Nontrivial R
i j : ι
⊢ (fun x i => (b.reindexRange.repr x) ⟨b i, ⋯⟩) (b i) j = (single i 1) j

Tactic:
simp only [reindexRange_repr_self]

Result:
case h
ι : 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
x : M
i✝ : ι
a✝ : Nontrivial R
i j : ι
⊢ (single ⟨b i, ⋯⟩ 1) ⟨b j, ⋯⟩ = (single i 1) j

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
x : M
i : ι
a✝ : Nontrivial R
⊢ (b.reindexRange.repr x) ⟨b i, ⋯⟩ = (b.repr x) i

Tactic:
apply (b.repr_apply_eq (fun x i => b.reindexRange.repr x ⟨b i, _⟩) _ _ _ x i).symm

Result:
ι : 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
x : M
i : ι
a✝ : Nontrivial R
⊢ ∀ (x y : M),
    (fun x i => (b.reindexRange.repr x) ⟨b i, ⋯⟩) (x + y) =
      (fun x i => (b.reindexRange.repr x) ⟨b i, ⋯⟩) x + (fun x i => (b.reindexRange.repr x) ⟨b i, ⋯⟩) y

ι : 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
x : M
i : ι
a✝ : Nontrivial R
⊢ ∀ (c : R) (x : M),
    (fun x i => (b.reindexRange.repr x) ⟨b i, ⋯⟩) (c • x) = c • (fun x i => (b.reindexRange.repr x) ⟨b i, ⋯⟩) x

ι : 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
x : M
i : ι
a✝ : Nontrivial R
⊢ ∀ (i : ι), (fun x i => (b.reindexRange.repr x) ⟨b i, ⋯⟩) (b i) = ⇑(single i 1)

Proof state:
case h
ι : 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
x✝ : M
i✝ : ι
a✝ : Nontrivial R
c : R
x : M
i : ι
⊢ (fun x i => (b.reindexRange.repr x) ⟨b i, ⋯⟩) (c • x) i = (c • (fun x i => (b.reindexRange.repr x) ⟨b i, ⋯⟩) x) i

Tactic:
simp only [Pi.smul_apply, LinearEquiv.map_smul, Finsupp.coe_smul]

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
x✝ : M
i : ι
a✝ : Nontrivial R
c : R
x : M
⊢ (fun x i => (b.reindexRange.repr x) ⟨b i, ⋯⟩) (c • x) = c • (fun x i => (b.reindexRange.repr x) ⟨b i, ⋯⟩) x

Tactic:
ext i

Result:
case h
ι : 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
x✝ : M
i✝ : ι
a✝ : Nontrivial R
c : R
x : M
i : ι
⊢ (fun x i => (b.reindexRange.repr x) ⟨b i, ⋯⟩) (c • x) i = (c • (fun x i => (b.reindexRange.repr x) ⟨b i, ⋯⟩) x) i

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
x : M
i : ι
a✝ : Nontrivial R
⊢ ∀ (i : ι), (fun x i => (b.reindexRange.repr x) ⟨b i, ⋯⟩) (b i) = ⇑(single i 1)

Tactic:
intro i

Result:
ι : 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
x : M
i✝ : ι
a✝ : Nontrivial R
i : ι
⊢ (fun x i => (b.reindexRange.repr x) ⟨b i, ⋯⟩) (b i) = ⇑(single i 1)

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
x bi : M
i : ι
h : b i = bi
a✝ : Nontrivial R
⊢ (b.reindexRange.repr x) ⟨bi, ⋯⟩ = (b.repr x) i

Tactic:
subst h

Result:
ι : 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
x : M
i : ι
a✝ : Nontrivial R
⊢ (b.reindexRange.repr x) ⟨b i, ⋯⟩ = (b.repr x) i

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
x bi : M
i : ι
h : b i = bi
⊢ (b.reindexRange.repr x) ⟨bi, ⋯⟩ = (b.repr x) i

Tactic:
nontriviality

Result:
ι : 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
x bi : M
i : ι
h : b i = bi
a✝ : Nontrivial R
⊢ (b.reindexRange.repr x) ⟨bi, ⋯⟩ = (b.repr x) i