α : Type u_1
M : Type u_2
N : Type ?u.325806
P : Type ?u.325809
R : Type u_3
S : Type ?u.325815
inst✝¹² : Semiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R N
inst✝⁶ : AddCommMonoid P
inst✝⁵ : Module R P
α' : Type ?u.325907
M' : Type ?u.325910
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M
inst✝¹ : Module R M'
inst✝ : Module R M
v : α → M
v' : α' → M'
h : Function.Surjective v
x : M
⊢ ∃ a, ↑(Finsupp.total α M R v) a = x
α : Type u_1
M : Type u_2
N : Type ?u.325806
P : Type ?u.325809
R : Type u_3
S : Type ?u.325815
inst✝¹² : Semiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R N
inst✝⁶ : AddCommMonoid P
inst✝⁵ : Module R P
α' : Type ?u.325907
M' : Type ?u.325910
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M
inst✝¹ : Module R M'
inst✝ : Module R M
v : α → M
v' : α' → M'
h : Function.Surjective v
⊢ Function.Surjective ↑(Finsupp.total α M R v)
intro x
case intro
α : Type u_1
M : Type u_2
N : Type ?u.325806
P : Type ?u.325809
R : Type u_3
S : Type ?u.325815
inst✝¹² : Semiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R N
inst✝⁶ : AddCommMonoid P
inst✝⁵ : Module R P
α' : Type ?u.325907
M' : Type ?u.325910
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M
inst✝¹ : Module R M'
inst✝ : Module R M
v : α → M
v' : α' → M'
h : Function.Surjective v
x : M
y : α
hy : v y = x
⊢ ∃ a, ↑(Finsupp.total α M R v) a = x
α : Type u_1
M : Type u_2
N : Type ?u.325806
P : Type ?u.325809
R : Type u_3
S : Type ?u.325815
inst✝¹² : Semiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R N
inst✝⁶ : AddCommMonoid P
inst✝⁵ : Module R P
α' : Type ?u.325907
M' : Type ?u.325910
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M
inst✝¹ : Module R M'
inst✝ : Module R M
v : α → M
v' : α' → M'
h : Function.Surjective v
x : M
⊢ ∃ a, ↑(Finsupp.total α M R v) a = x
obtain ⟨y, hy⟩ := h x
no goals
case intro
α : Type u_1
M : Type u_2
N : Type ?u.325806
P : Type ?u.325809
R : Type u_3
S : Type ?u.325815
inst✝¹² : Semiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R N
inst✝⁶ : AddCommMonoid P
inst✝⁵ : Module R P
α' : Type ?u.325907
M' : Type ?u.325910
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M
inst✝¹ : Module R M'
inst✝ : Module R M
v : α → M
v' : α' → M'
h : Function.Surjective v
x : M
y : α
hy : v y = x
⊢ ∃ a, ↑(Finsupp.total α M R v) a = x
exact ⟨Finsupp.single y 1, by simp [hy]⟩
no goals
α : Type u_1
M : Type u_2
N : Type ?u.325806
P : Type ?u.325809
R : Type u_3
S : Type ?u.325815
inst✝¹² : Semiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R N
inst✝⁶ : AddCommMonoid P
inst✝⁵ : Module R P
α' : Type ?u.325907
M' : Type ?u.325910
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M
inst✝¹ : Module R M'
inst✝ : Module R M
v : α → M
v' : α' → M'
h : Function.Surjective v
x : M
y : α
hy : v y = x
⊢ ↑(Finsupp.total α M R v) (single y 1) = x
simp [hy]