-- Mathlib/LinearAlgebra/LinearIndependent/Defs.lean
theorem LinearIndependent.span_repr_eq [Nontrivial R] (x) :
    Span.repr R (Set.range v) x =
      (hv.repr x).equivMapDomain (Equiv.ofInjective _ hv.injective)

Proof state:
case h.mk.intro
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
hv : LinearIndependent R v
inst✝ : Nontrivial R
x : ↥(span R (range v))
p : Finsupp.equivMapDomain (Equiv.ofInjective v ⋯).symm (Span.repr R (range v) x) = hv.repr x
i : ι
⊢ (Span.repr R (range v) x) ⟨v i, ⋯⟩ = (Finsupp.equivMapDomain (Equiv.ofInjective v ⋯) (hv.repr x)) ⟨v i, ⋯⟩

Tactic:
simp [← p]

Result:
no goals

Proof state:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
hv : LinearIndependent R v
inst✝ : Nontrivial R
x : ↥(span R (range v))
p : Finsupp.equivMapDomain (Equiv.ofInjective v ⋯).symm (Span.repr R (range v) x) = hv.repr x
⊢ Span.repr R (range v) x = Finsupp.equivMapDomain (Equiv.ofInjective v ⋯) (hv.repr x)

Tactic:
ext ⟨_, ⟨i, rfl⟩⟩

Result:
case h.mk.intro
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
hv : LinearIndependent R v
inst✝ : Nontrivial R
x : ↥(span R (range v))
p : Finsupp.equivMapDomain (Equiv.ofInjective v ⋯).symm (Span.repr R (range v) x) = hv.repr x
i : ι
⊢ (Span.repr R (range v) x) ⟨v i, ⋯⟩ = (Finsupp.equivMapDomain (Equiv.ofInjective v ⋯) (hv.repr x)) ⟨v i, ⋯⟩

Proof state:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
hv : LinearIndependent R v
inst✝ : Nontrivial R
x : ↥(span R (range v))
⊢ Span.repr R (range v) x = Finsupp.equivMapDomain (Equiv.ofInjective v ⋯) (hv.repr x)

Tactic:
have p :
  (Span.repr R (Set.range v) x).equivMapDomain (Equiv.ofInjective _ hv.injective).symm =
    hv.repr x := by
  apply (LinearIndependent.linearCombinationEquiv hv).injective
  ext
  simp only [LinearIndependent.linearCombinationEquiv_apply_coe, Equiv.self_comp_ofInjective_symm,
    LinearIndependent.linearCombination_repr, Finsupp.linearCombination_equivMapDomain,
    Span.finsupp_linearCombination_repr]

Result:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
hv : LinearIndependent R v
inst✝ : Nontrivial R
x : ↥(span R (range v))
p : Finsupp.equivMapDomain (Equiv.ofInjective v ⋯).symm (Span.repr R (range v) x) = hv.repr x
⊢ Span.repr R (range v) x = Finsupp.equivMapDomain (Equiv.ofInjective v ⋯) (hv.repr x)

Proof state:
case a
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
hv : LinearIndependent R v
inst✝ : Nontrivial R
x : ↥(span R (range v))
⊢ hv.linearCombinationEquiv (Finsupp.equivMapDomain (Equiv.ofInjective v ⋯).symm (Span.repr R (range v) x)) =
    hv.linearCombinationEquiv (hv.repr x)

Tactic:
ext

Result:
case a.a
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
hv : LinearIndependent R v
inst✝ : Nontrivial R
x : ↥(span R (range v))
⊢ ↑(hv.linearCombinationEquiv (Finsupp.equivMapDomain (Equiv.ofInjective v ⋯).symm (Span.repr R (range v) x))) =
    ↑(hv.linearCombinationEquiv (hv.repr x))

Proof state:
case a.a
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
hv : LinearIndependent R v
inst✝ : Nontrivial R
x : ↥(span R (range v))
⊢ ↑(hv.linearCombinationEquiv (Finsupp.equivMapDomain (Equiv.ofInjective v ⋯).symm (Span.repr R (range v) x))) =
    ↑(hv.linearCombinationEquiv (hv.repr x))

Tactic:
simp only [LinearIndependent.linearCombinationEquiv_apply_coe, Equiv.self_comp_ofInjective_symm,
  LinearIndependent.linearCombination_repr, Finsupp.linearCombination_equivMapDomain,
  Span.finsupp_linearCombination_repr]

Result:
no goals

Proof state:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
hv : LinearIndependent R v
inst✝ : Nontrivial R
x : ↥(span R (range v))
⊢ Finsupp.equivMapDomain (Equiv.ofInjective v ⋯).symm (Span.repr R (range v) x) = hv.repr x

Tactic:
apply (LinearIndependent.linearCombinationEquiv hv).injective

Result:
case a
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
hv : LinearIndependent R v
inst✝ : Nontrivial R
x : ↥(span R (range v))
⊢ hv.linearCombinationEquiv (Finsupp.equivMapDomain (Equiv.ofInjective v ⋯).symm (Span.repr R (range v) x)) =
    hv.linearCombinationEquiv (hv.repr x)