R : Type u_2
M : Type u_3
N : Type ?u.781740
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
α : Type u_1
inst✝ : Fintype α
f : M →ₗ[R] α → R
s : Surjective ↑f
x y : α
⊢ ↑(comp (comp f (splittingOfFunOnFintypeSurjective f s)) (single x)) 1 y = ↑(comp id (single x)) 1 y
R : Type u_2
M : Type u_3
N : Type ?u.781740
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
α : Type u_1
inst✝ : Fintype α
f : M →ₗ[R] α → R
s : Surjective ↑f
⊢ comp f (splittingOfFunOnFintypeSurjective f s) = id
refine pi_ext' fun x => ext_ring <| funext fun y => ?_
R : Type u_2
M : Type u_3
N : Type ?u.781740
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
α : Type u_1
inst✝ : Fintype α
f : M →ₗ[R] α → R
s : Surjective ↑f
x y : α
⊢ ↑f
      (sum (↑(LinearEquiv.symm (linearEquivFunOnFinite R R α)) (Pi.single x 1)) fun x r =>
        r • Exists.choose (_ : ∃ a, ↑f a = ↑(Finsupp.single x 1)))
      y =
    Pi.single x 1 y
R : Type u_2
M : Type u_3
N : Type ?u.781740
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
α : Type u_1
inst✝ : Fintype α
f : M →ₗ[R] α → R
s : Surjective ↑f
x y : α
⊢ ↑(comp (comp f (splittingOfFunOnFintypeSurjective f s)) (single x)) 1 y = ↑(comp id (single x)) 1 y
dsimp [splittingOfFunOnFintypeSurjective]
R : Type u_2
M : Type u_3
N : Type ?u.781740
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
α : Type u_1
inst✝ : Fintype α
f : M →ₗ[R] α → R
s : Surjective ↑f
x y : α
⊢ 0 • Exists.choose (_ : ∃ a, ↑f a = ↑(Finsupp.single x 1)) = 0
R : Type u_2
M : Type u_3
N : Type ?u.781740
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
α : Type u_1
inst✝ : Fintype α
f : M →ₗ[R] α → R
s : Surjective ↑f
x y : α
⊢ ↑f
      (sum (↑(LinearEquiv.symm (linearEquivFunOnFinite R R α)) (Pi.single x 1)) fun x r =>
        r • Exists.choose (_ : ∃ a, ↑f a = ↑(Finsupp.single x 1)))
      y =
    Pi.single x 1 y
rw [linearEquivFunOnFinite_symm_single, Finsupp.sum_single_index, one_smul,
  (s (Finsupp.single x 1)).choose_spec, Finsupp.single_eq_pi_single]
no goals
R : Type u_2
M : Type u_3
N : Type ?u.781740
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
α : Type u_1
inst✝ : Fintype α
f : M →ₗ[R] α → R
s : Surjective ↑f
x y : α
⊢ 0 • Exists.choose (_ : ∃ a, ↑f a = ↑(Finsupp.single x 1)) = 0
rw [zero_smul]