α : Type u_1
β : Type ?u.481748
γ : Type ?u.481751
ι : Type ?u.481754
M : Type u_2
M' : Type ?u.481760
N : Type ?u.481763
P : Type ?u.481766
G : Type ?u.481769
H : Type ?u.481772
R : Type ?u.481775
S : Type ?u.481778
inst✝ : Zero M
f : α →₀ M
y : M
⊢ (∃ a, a ∈ f.support ∧ ↑f a = y) ↔ y ≠ 0 ∧ ∃ x, ↑f x = y
α : Type u_1
β : Type ?u.481748
γ : Type ?u.481751
ι : Type ?u.481754
M : Type u_2
M' : Type ?u.481760
N : Type ?u.481763
P : Type ?u.481766
G : Type ?u.481769
H : Type ?u.481772
R : Type ?u.481775
S : Type ?u.481778
inst✝ : Zero M
f : α →₀ M
y : M
⊢ y ∈ frange f ↔ y ≠ 0 ∧ ∃ x, ↑f x = y
rw [frange, @Finset.mem_image _ _ (Classical.decEq _) _ f.support]
no goals
α : Type u_1
β : Type ?u.481748
γ : Type ?u.481751
ι : Type ?u.481754
M : Type u_2
M' : Type ?u.481760
N : Type ?u.481763
P : Type ?u.481766
G : Type ?u.481769
H : Type ?u.481772
R : Type ?u.481775
S : Type ?u.481778
inst✝ : Zero M
f : α →₀ M
y : M
⊢ (∃ a, a ∈ f.support ∧ ↑f a = y) ↔ y ≠ 0 ∧ ∃ x, ↑f x = y
exact ⟨fun ⟨x, hx1, hx2⟩ => ⟨hx2 ▸ mem_support_iff.1 hx1, x, hx2⟩, fun ⟨hy, x, hx⟩ =>
  ⟨x, mem_support_iff.2 (hx.symm ▸ hy), hx⟩⟩