no goals
α : Type u_1
β : Type u_2
γ : Type ?u.218890
ι : Type ?u.218893
M : Type u_3
M' : Type ?u.218899
N : Type ?u.218902
P : Type ?u.218905
G : Type ?u.218908
H : Type ?u.218911
R : Type ?u.218914
S : Type ?u.218917
inst✝¹ : Zero M
inst✝ : Zero N
f : α ↪ β
v : α →₀ M
a : β
h : ¬a ∈ Set.range ↑f
⊢ ↑(embDomain f v) a = 0
classical
  refine' dif_neg (mt (fun h => _) h)
  rcases Finset.mem_map.1 h with ⟨a, _h, rfl⟩
  exact Set.mem_range_self a
α : Type u_1
β : Type u_2
γ : Type ?u.218890
ι : Type ?u.218893
M : Type u_3
M' : Type ?u.218899
N : Type ?u.218902
P : Type ?u.218905
G : Type ?u.218908
H : Type ?u.218911
R : Type ?u.218914
S : Type ?u.218917
inst✝¹ : Zero M
inst✝ : Zero N
f : α ↪ β
v : α →₀ M
a : β
h✝ : ¬a ∈ Set.range ↑f
h : a ∈ map f v.support
⊢ a ∈ Set.range ↑f
α : Type u_1
β : Type u_2
γ : Type ?u.218890
ι : Type ?u.218893
M : Type u_3
M' : Type ?u.218899
N : Type ?u.218902
P : Type ?u.218905
G : Type ?u.218908
H : Type ?u.218911
R : Type ?u.218914
S : Type ?u.218917
inst✝¹ : Zero M
inst✝ : Zero N
f : α ↪ β
v : α →₀ M
a : β
h : ¬a ∈ Set.range ↑f
⊢ ↑(embDomain f v) a = 0
refine' dif_neg (mt (fun h => _) h)
case intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.218890
ι : Type ?u.218893
M : Type u_3
M' : Type ?u.218899
N : Type ?u.218902
P : Type ?u.218905
G : Type ?u.218908
H : Type ?u.218911
R : Type ?u.218914
S : Type ?u.218917
inst✝¹ : Zero M
inst✝ : Zero N
f : α ↪ β
v : α →₀ M
a : α
_h : a ∈ v.support
h✝ : ¬↑f a ∈ Set.range ↑f
h : ↑f a ∈ map f v.support
⊢ ↑f a ∈ Set.range ↑f
α : Type u_1
β : Type u_2
γ : Type ?u.218890
ι : Type ?u.218893
M : Type u_3
M' : Type ?u.218899
N : Type ?u.218902
P : Type ?u.218905
G : Type ?u.218908
H : Type ?u.218911
R : Type ?u.218914
S : Type ?u.218917
inst✝¹ : Zero M
inst✝ : Zero N
f : α ↪ β
v : α →₀ M
a : β
h✝ : ¬a ∈ Set.range ↑f
h : a ∈ map f v.support
⊢ a ∈ Set.range ↑f
rcases Finset.mem_map.1 h with ⟨a, _h, rfl⟩
no goals
case intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.218890
ι : Type ?u.218893
M : Type u_3
M' : Type ?u.218899
N : Type ?u.218902
P : Type ?u.218905
G : Type ?u.218908
H : Type ?u.218911
R : Type ?u.218914
S : Type ?u.218917
inst✝¹ : Zero M
inst✝ : Zero N
f : α ↪ β
v : α →₀ M
a : α
_h : a ∈ v.support
h✝ : ¬↑f a ∈ Set.range ↑f
h : ↑f a ∈ map f v.support
⊢ ↑f a ∈ Set.range ↑f
exact Set.mem_range_self a