-- Mathlib/Algebra/DirectSum/Module.lean
theorem IsInternal.collectedBasis_coe (h : IsInternal A) {α : ι → Type*}
    (v : ∀ i, Basis (α i) R (A i)) : ⇑(h.collectedBasis v) = fun a : Σi, α i ↦ ↑(v a.1 a.2)

Proof state:
case h
R : Type u
inst✝² : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
A : ι → Submodule R M
h : IsInternal A
α : ι → Type u_2
v : (i : ι) → Basis (α i) R ↥(A i)
a : (i : ι) × α i
⊢ (A a.fst).subtype ((v a.fst) a.snd) = ↑((v a.fst) a.snd)

Tactic:
simp only [Submodule.coe_subtype]

Result:
no goals

Proof state:
case h
R : Type u
inst✝² : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
A : ι → Submodule R M
h : IsInternal A
α : ι → Type u_2
v : (i : ι) → Basis (α i) R ↥(A i)
a : (i : ι) × α i
⊢ (h.collectedBasis v) a = ↑((v a.fst) a.snd)

Tactic:
simp only [IsInternal.collectedBasis, coeLinearMap, Basis.coe_ofRepr, LinearEquiv.trans_symm,
  LinearEquiv.symm_symm, LinearEquiv.trans_apply, sigmaFinsuppLequivDFinsupp_apply,
  sigmaFinsuppEquivDFinsupp_single, LinearEquiv.ofBijective_apply,
  sigmaFinsuppAddEquivDFinsupp_apply]

Result:
case h
R : Type u
inst✝² : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
A : ι → Submodule R M
h : IsInternal A
α : ι → Type u_2
v : (i : ι) → Basis (α i) R ↥(A i)
a : (i : ι) × α i
⊢ (toModule R ι M fun i => (A i).subtype)
      ((DFinsupp.mapRange.linearEquiv fun i => (v i).repr).symm (DFinsupp.single a.fst (single a.snd 1))) =
    ↑((v a.fst) a.snd)

Proof state:
R : Type u
inst✝² : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
A : ι → Submodule R M
h : IsInternal A
α : ι → Type u_2
v : (i : ι) → Basis (α i) R ↥(A i)
⊢ ⇑(h.collectedBasis v) = fun a => ↑((v a.fst) a.snd)

Tactic:
funext a

Result:
case h
R : Type u
inst✝² : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
A : ι → Submodule R M
h : IsInternal A
α : ι → Type u_2
v : (i : ι) → Basis (α i) R ↥(A i)
a : (i : ι) × α i
⊢ (h.collectedBasis v) a = ↑((v a.fst) a.snd)

Proof state:
case h
R : Type u
inst✝² : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
A : ι → Submodule R M
h : IsInternal A
α : ι → Type u_2
v : (i : ι) → Basis (α i) R ↥(A i)
a : (i : ι) × α i
⊢ (toModule R ι M fun i => (A i).subtype)
      (DFinsupp.mapRange (fun i x => (v i).repr.symm x) ⋯ (DFinsupp.single a.fst (single a.snd 1))) =
    ↑((v a.fst) a.snd)

Tactic:
simp only [DFinsupp.mapRange_single, Basis.repr_symm_apply, linearCombination_single, one_smul,
  toModule]

Result:
case h
R : Type u
inst✝² : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
A : ι → Submodule R M
h : IsInternal A
α : ι → Type u_2
v : (i : ι) → Basis (α i) R ↥(A i)
a : (i : ι) × α i
⊢ ((DFinsupp.lsum ℕ) fun i => (A i).subtype) (DFinsupp.single a.fst ((v a.fst) a.snd)) = ↑((v a.fst) a.snd)

Proof state:
case h
R : Type u
inst✝² : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
A : ι → Submodule R M
h : IsInternal A
α : ι → Type u_2
v : (i : ι) → Basis (α i) R ↥(A i)
a : (i : ι) × α i
⊢ (toModule R ι M fun i => (A i).subtype)
      ((DFinsupp.mapRange.linearEquiv fun i => (v i).repr.symm) (DFinsupp.single a.fst (single a.snd 1))) =
    ↑((v a.fst) a.snd)

Tactic:
erw [DFinsupp.mapRange.linearEquiv_apply]

Result:
case h
R : Type u
inst✝² : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
A : ι → Submodule R M
h : IsInternal A
α : ι → Type u_2
v : (i : ι) → Basis (α i) R ↥(A i)
a : (i : ι) × α i
⊢ (toModule R ι M fun i => (A i).subtype)
      (DFinsupp.mapRange (fun i x => (v i).repr.symm x) ⋯ (DFinsupp.single a.fst (single a.snd 1))) =
    ↑((v a.fst) a.snd)

Proof state:
case h
R : Type u
inst✝² : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
A : ι → Submodule R M
h : IsInternal A
α : ι → Type u_2
v : (i : ι) → Basis (α i) R ↥(A i)
a : (i : ι) × α i
⊢ ((DFinsupp.lsum ℕ) fun i => (A i).subtype) (DFinsupp.single a.fst ((v a.fst) a.snd)) = ↑((v a.fst) a.snd)

Tactic:
erw [DFinsupp.lsum_single]

Result:
case h
R : Type u
inst✝² : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
A : ι → Submodule R M
h : IsInternal A
α : ι → Type u_2
v : (i : ι) → Basis (α i) R ↥(A i)
a : (i : ι) × α i
⊢ (A a.fst).subtype ((v a.fst) a.snd) = ↑((v a.fst) a.snd)

Proof state:
case h
R : Type u
inst✝² : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
A : ι → Submodule R M
h : IsInternal A
α : ι → Type u_2
v : (i : ι) → Basis (α i) R ↥(A i)
a : (i : ι) × α i
⊢ (toModule R ι M fun i => (A i).subtype)
      ((DFinsupp.mapRange.linearEquiv fun i => (v i).repr).symm (DFinsupp.single a.fst (single a.snd 1))) =
    ↑((v a.fst) a.snd)

Tactic:
rw [DFinsupp.mapRange.linearEquiv_symm]

Result:
case h
R : Type u
inst✝² : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
A : ι → Submodule R M
h : IsInternal A
α : ι → Type u_2
v : (i : ι) → Basis (α i) R ↥(A i)
a : (i : ι) × α i
⊢ (toModule R ι M fun i => (A i).subtype)
      ((DFinsupp.mapRange.linearEquiv fun i => (v i).repr.symm) (DFinsupp.single a.fst (single a.snd 1))) =
    ↑((v a.fst) a.snd)