R : Type u_1
M : Type u_2
N : Type ?u.770436
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
α : Type u_3
f : M →ₗ[R] α →₀ R
s : Surjective ↑f
x y : α
⊢ ↑(↑(comp (comp f (splittingOfFinsuppSurjective f s)) (lsingle x)) 1) y = ↑(↑(comp id (lsingle x)) 1) y
R : Type u_1
M : Type u_2
N : Type ?u.770436
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
α : Type u_3
f : M →ₗ[R] α →₀ R
s : Surjective ↑f
⊢ comp f (splittingOfFinsuppSurjective f s) = id
refine lhom_ext' fun x => ext_ring <| Finsupp.ext fun y => ?_
R : Type u_1
M : Type u_2
N : Type ?u.770436
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
α : Type u_3
f : M →ₗ[R] α →₀ R
s : Surjective ↑f
x y : α
⊢ ↑(↑f (sum (Finsupp.single x 1) fun x r => r • Exists.choose (_ : ∃ a, ↑f a = Finsupp.single x 1))) y =
    ↑(Finsupp.single x 1) y
R : Type u_1
M : Type u_2
N : Type ?u.770436
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
α : Type u_3
f : M →ₗ[R] α →₀ R
s : Surjective ↑f
x y : α
⊢ ↑(↑(comp (comp f (splittingOfFinsuppSurjective f s)) (lsingle x)) 1) y = ↑(↑(comp id (lsingle x)) 1) y
dsimp [splittingOfFinsuppSurjective]
case e_a
R : Type u_1
M : Type u_2
N : Type ?u.770436
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
α : Type u_3
f : M →ₗ[R] α →₀ R
s : Surjective ↑f
x y : α
⊢ ↑f (sum (Finsupp.single x 1) fun x r => r • Exists.choose (_ : ∃ a, ↑f a = Finsupp.single x 1)) = Finsupp.single x 1
R : Type u_1
M : Type u_2
N : Type ?u.770436
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
α : Type u_3
f : M →ₗ[R] α →₀ R
s : Surjective ↑f
x y : α
⊢ ↑(↑f (sum (Finsupp.single x 1) fun x r => r • Exists.choose (_ : ∃ a, ↑f a = Finsupp.single x 1))) y =
    ↑(Finsupp.single x 1) y
congr
case e_a
R : Type u_1
M : Type u_2
N : Type ?u.770436
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
α : Type u_3
f : M →ₗ[R] α →₀ R
s : Surjective ↑f
x y : α
⊢ ↑f (Exists.choose (_ : ∃ a, ↑f a = Finsupp.single x 1)) = Finsupp.single x 1

case e_a
R : Type u_1
M : Type u_2
N : Type ?u.770436
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
α : Type u_3
f : M →ₗ[R] α →₀ R
s : Surjective ↑f
x y : α
⊢ 0 • Exists.choose (_ : ∃ a, ↑f a = Finsupp.single x 1) = 0
case e_a
R : Type u_1
M : Type u_2
N : Type ?u.770436
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
α : Type u_3
f : M →ₗ[R] α →₀ R
s : Surjective ↑f
x y : α
⊢ ↑f (sum (Finsupp.single x 1) fun x r => r • Exists.choose (_ : ∃ a, ↑f a = Finsupp.single x 1)) = Finsupp.single x 1
rw [sum_single_index, one_smul]
no goals
case e_a
R : Type u_1
M : Type u_2
N : Type ?u.770436
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
α : Type u_3
f : M →ₗ[R] α →₀ R
s : Surjective ↑f
x y : α
⊢ ↑f (Exists.choose (_ : ∃ a, ↑f a = Finsupp.single x 1)) = Finsupp.single x 1
exact (s (Finsupp.single x 1)).choose_spec
no goals
case e_a
R : Type u_1
M : Type u_2
N : Type ?u.770436
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
α : Type u_3
f : M →ₗ[R] α →₀ R
s : Surjective ↑f
x y : α
⊢ 0 • Exists.choose (_ : ∃ a, ↑f a = Finsupp.single x 1) = 0
rw [zero_smul]