-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u_2
V : Type u_3
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
W : Submodule R V
m : Type u_4
n : Type u_5
bW : Basis.{u_4, u_2, u_3} m R ↥W
bQ : Basis.{u_5, u_2, u_3} n R (V ⧸ W)
w : ↥W
i : m
refine_1 :
  ∀ (x y : ↥W),
    (fun (w : ↥W) (i : m) ↦
          (((((bW.sumQuot bQ).repr : (a : V) → m ⊕ n →₀ R) ((W.subtype : (a : ↥W) → V) w) : m ⊕ n →₀ R) :
                (a : m ⊕ n) → R)
              (Sum.inl i) :
            R))
        (x + y) =
      HAdd.hAdd (α := m → R)
        ((fun (w : ↥W) (i : m) ↦
            (((((bW.sumQuot bQ).repr : (a : V) → m ⊕ n →₀ R) ((W.subtype : (a : ↥W) → V) w) : m ⊕ n →₀ R) :
                  (a : m ⊕ n) → R)
                (Sum.inl i) :
              R))
          x)
        ((fun (w : ↥W) (i : m) ↦
            (((((bW.sumQuot bQ).repr : (a : V) → m ⊕ n →₀ R) ((W.subtype : (a : ↥W) → V) w) : m ⊕ n →₀ R) :
                  (a : m ⊕ n) → R)
                (Sum.inl i) :
              R))
          y)
refine_2 :
  ∀ (c : R) (x : ↥W),
    (fun (w : ↥W) (i : m) ↦
          (((((bW.sumQuot bQ).repr : (a : V) → m ⊕ n →₀ R) ((W.subtype : (a : ↥W) → V) w) : m ⊕ n →₀ R) :
                (a : m ⊕ n) → R)
              (Sum.inl i) :
            R))
        (c • x) =
      HSMul.hSMul (β := m → R) c
        ((fun (w : ↥W) (i : m) ↦
            (((((bW.sumQuot bQ).repr : (a : V) → m ⊕ n →₀ R) ((W.subtype : (a : ↥W) → V) w) : m ⊕ n →₀ R) :
                  (a : m ⊕ n) → R)
                (Sum.inl i) :
              R))
          x)
refine_3 :
  ∀ (i : m),
    Eq (α := m → R)
      ((fun (w : ↥W) (i : m) ↦
          (((((bW.sumQuot bQ).repr : (a : V) → m ⊕ n →₀ R) ((W.subtype : (a : ↥W) → V) w) : m ⊕ n →₀ R) :
                (a : m ⊕ n) → R)
              (Sum.inl i) :
            R))
        ((bW : (a : m) → ↥W) i))
      (⇑(Finsupp.single i 1) : (a : m) → R)
refine_1₁ :
  ∀ (x y : ↥W),
    (fun (w : ↥W) (i : m) ↦
          (((((bW.sumQuot bQ).repr : (a : V) → m ⊕ n →₀ R) ((W.subtype : (a : ↥W) → V) w) : m ⊕ n →₀ R) :
                (a : m ⊕ n) → R)
              (Sum.inl i) :
            R))
        (x + y) =
      HAdd.hAdd (α := m → R)
        ((fun (w : ↥W) (i : m) ↦
            (((((bW.sumQuot bQ).repr : (a : V) → m ⊕ n →₀ R) ((W.subtype : (a : ↥W) → V) w) : m ⊕ n →₀ R) :
                  (a : m ⊕ n) → R)
                (Sum.inl i) :
              R))
          x)
        ((fun (w : ↥W) (i : m) ↦
            (((((bW.sumQuot bQ).repr : (a : V) → m ⊕ n →₀ R) ((W.subtype : (a : ↥W) → V) w) : m ⊕ n →₀ R) :
                  (a : m ⊕ n) → R)
                (Sum.inl i) :
              R))
          y)
refine_2₁ :
  ∀ (c : R) (x : ↥W),
    (fun (w : ↥W) (i : m) ↦
          (((((bW.sumQuot bQ).repr : (a : V) → m ⊕ n →₀ R) ((W.subtype : (a : ↥W) → V) w) : m ⊕ n →₀ R) :
                (a : m ⊕ n) → R)
              (Sum.inl i) :
            R))
        (c • x) =
      HSMul.hSMul (β := m → R) c
        ((fun (w : ↥W) (i : m) ↦
            (((((bW.sumQuot bQ).repr : (a : V) → m ⊕ n →₀ R) ((W.subtype : (a : ↥W) → V) w) : m ⊕ n →₀ R) :
                  (a : m ⊕ n) → R)
                (Sum.inl i) :
              R))
          x)
refine_3₁ :
  ∀ (i : m),
    Eq (α := m → R)
      ((fun (w : ↥W) (i : m) ↦
          (((((bW.sumQuot bQ).repr : (a : V) → m ⊕ n →₀ R) ((W.subtype : (a : ↥W) → V) w) : m ⊕ n →₀ R) :
                (a : m ⊕ n) → R)
              (Sum.inl i) :
            R))
        ((bW : (a : m) → ↥W) i))
      (⇑(Finsupp.single i 1) : (a : m) → R)
refine_1₂ :
  ∀ (x y : ↥W),
    (fun (w : ↥W) (i : m) ↦
          (((((bW.sumQuot bQ).repr : (a : V) → m ⊕ n →₀ R) ((W.subtype : (a : ↥W) → V) w) : m ⊕ n →₀ R) :
                (a : m ⊕ n) → R)
              (Sum.inl i) :
            R))
        (x + y) =
      HAdd.hAdd (α := m → R)
        ((fun (w : ↥W) (i : m) ↦
            (((((bW.sumQuot bQ).repr : (a : V) → m ⊕ n →₀ R) ((W.subtype : (a : ↥W) → V) w) : m ⊕ n →₀ R) :
                  (a : m ⊕ n) → R)
                (Sum.inl i) :
              R))
          x)
        ((fun (w : ↥W) (i : m) ↦
            (((((bW.sumQuot bQ).repr : (a : V) → m ⊕ n →₀ R) ((W.subtype : (a : ↥W) → V) w) : m ⊕ n →₀ R) :
                  (a : m ⊕ n) → R)
                (Sum.inl i) :
              R))
          y)
refine_2₂ :
  ∀ (c : R) (x : ↥W),
    (fun (w : ↥W) (i : m) ↦
          (((((bW.sumQuot bQ).repr : (a : V) → m ⊕ n →₀ R) ((W.subtype : (a : ↥W) → V) w) : m ⊕ n →₀ R) :
                (a : m ⊕ n) → R)
              (Sum.inl i) :
            R))
        (c • x) =
      HSMul.hSMul (β := m → R) c
        ((fun (w : ↥W) (i : m) ↦
            (((((bW.sumQuot bQ).repr : (a : V) → m ⊕ n →₀ R) ((W.subtype : (a : ↥W) → V) w) : m ⊕ n →₀ R) :
                  (a : m ⊕ n) → R)
                (Sum.inl i) :
              R))
          x)
refine_3₂ :
  ∀ (i : m),
    Eq (α := m → R)
      ((fun (w : ↥W) (i : m) ↦
          (((((bW.sumQuot bQ).repr : (a : V) → m ⊕ n →₀ R) ((W.subtype : (a : ↥W) → V) w) : m ⊕ n →₀ R) :
                (a : m ⊕ n) → R)
              (Sum.inl i) :
            R))
        ((bW : (a : m) → ↥W) i))
      (⇑(Finsupp.single i 1) : (a : m) → R)
refine_1₃ :
  ∀ (x y : ↥W),
    (fun (w : ↥W) (i : m) ↦
          (((((bW.sumQuot bQ).repr : (a : V) → m ⊕ n →₀ R) ((W.subtype : (a : ↥W) → V) w) : m ⊕ n →₀ R) :
                (a : m ⊕ n) → R)
              (Sum.inl i) :
            R))
        (x + y) =
      HAdd.hAdd (α := m → R)
        ((fun (w : ↥W) (i : m) ↦
            (((((bW.sumQuot bQ).repr : (a : V) → m ⊕ n →₀ R) ((W.subtype : (a : ↥W) → V) w) : m ⊕ n →₀ R) :
                  (a : m ⊕ n) → R)
                (Sum.inl i) :
              R))
          x)
        ((fun (w : ↥W) (i : m) ↦
            (((((bW.sumQuot bQ).repr : (a : V) → m ⊕ n →₀ R) ((W.subtype : (a : ↥W) → V) w) : m ⊕ n →₀ R) :
                  (a : m ⊕ n) → R)
                (Sum.inl i) :
              R))
          y)
refine_2₃ :
  ∀ (c : R) (x : ↥W),
    (fun (w : ↥W) (i : m) ↦
          (((((bW.sumQuot bQ).repr : (a : V) → m ⊕ n →₀ R) ((W.subtype : (a : ↥W) → V) w) : m ⊕ n →₀ R) :
                (a : m ⊕ n) → R)
              (Sum.inl i) :
            R))
        (c • x) =
      HSMul.hSMul (β := m → R) c
        ((fun (w : ↥W) (i : m) ↦
            (((((bW.sumQuot bQ).repr : (a : V) → m ⊕ n →₀ R) ((W.subtype : (a : ↥W) → V) w) : m ⊕ n →₀ R) :
                  (a : m ⊕ n) → R)
                (Sum.inl i) :
              R))
          x)
refine_3₃ :
  ∀ (i : m),
    Eq (α := m → R)
      ((fun (w : ↥W) (i : m) ↦
          (((((bW.sumQuot bQ).repr : (a : V) → m ⊕ n →₀ R) ((W.subtype : (a : ↥W) → V) w) : m ⊕ n →₀ R) :
                (a : m ⊕ n) → R)
              (Sum.inl i) :
            R))
        ((bW : (a : m) → ↥W) i))
      (⇑(Finsupp.single i 1) : (a : m) → R)
⊢ Eq.{u_2 + 1} (α := R)
    (((((bW.sumQuot bQ).repr : (a : V) → m ⊕ n →₀ R) (↑w : V) : m ⊕ n →₀ R) : (a : m ⊕ n) → R) (Sum.inl i) : R)
    ((((bW.repr : (a : ↥W) → m →₀ R) w : m →₀ R) : (a : m) → R) i : R)

Tactic:
classical
  refine Eq.symm <| (bW.repr_apply_eq
      (fun w i => (sumQuot bW bQ).repr (W.subtype w) (Sum.inl i)) ?_ ?_ ?_ w i) <;>
  aesop (add simp Finsupp.single_apply)

Premises used: Module.Basis.sumQuot, Sum.inl, Module.Basis.repr, Module.Basis.repr_apply_eq, Submodule.subtype, Finsupp.single_apply, Eq.symm, DFunLike.coe