α : Type u_1
β : Type u_3
γ : Type ?u.245637
ι : Type ?u.245640
M : Type u_2
M' : Type ?u.245646
N : Type ?u.245649
P : Type ?u.245652
G : Type ?u.245655
H : Type ?u.245658
R : Type ?u.245661
S : Type ?u.245664
inst✝¹ : Zero M
inst✝ : Zero N
l : α →₀ M
f : α ↪ β
a : β
b : M
hb : b ≠ 0
h : embDomain f l = single a b
h_map_support : map f l.support = {a}
⊢ ∃ x, l = single x b ∧ ↑f x = a
α : Type u_1
β : Type u_3
γ : Type ?u.245637
ι : Type ?u.245640
M : Type u_2
M' : Type ?u.245646
N : Type ?u.245649
P : Type ?u.245652
G : Type ?u.245655
H : Type ?u.245658
R : Type ?u.245661
S : Type ?u.245664
inst✝¹ : Zero M
inst✝ : Zero N
l : α →₀ M
f : α ↪ β
a : β
b : M
hb : b ≠ 0
h : embDomain f l = single a b
⊢ ∃ x, l = single x b ∧ ↑f x = a
have h_map_support : Finset.map f l.support = {a} := by
  rw [← support_embDomain, h, support_single_ne_zero _ hb]
α : Type u_1
β : Type u_3
γ : Type ?u.245637
ι : Type ?u.245640
M : Type u_2
M' : Type ?u.245646
N : Type ?u.245649
P : Type ?u.245652
G : Type ?u.245655
H : Type ?u.245658
R : Type ?u.245661
S : Type ?u.245664
inst✝¹ : Zero M
inst✝ : Zero N
l : α →₀ M
f : α ↪ β
a : β
b : M
hb : b ≠ 0
h : embDomain f l = single a b
h_map_support : map f l.support = {a}
ha : a ∈ map f l.support
⊢ ∃ x, l = single x b ∧ ↑f x = a
α : Type u_1
β : Type u_3
γ : Type ?u.245637
ι : Type ?u.245640
M : Type u_2
M' : Type ?u.245646
N : Type ?u.245649
P : Type ?u.245652
G : Type ?u.245655
H : Type ?u.245658
R : Type ?u.245661
S : Type ?u.245664
inst✝¹ : Zero M
inst✝ : Zero N
l : α →₀ M
f : α ↪ β
a : β
b : M
hb : b ≠ 0
h : embDomain f l = single a b
h_map_support : map f l.support = {a}
⊢ ∃ x, l = single x b ∧ ↑f x = a
have ha : a ∈ Finset.map f l.support := by simp only [h_map_support, Finset.mem_singleton]
case intro.intro
α : Type u_1
β : Type u_3
γ : Type ?u.245637
ι : Type ?u.245640
M : Type u_2
M' : Type ?u.245646
N : Type ?u.245649
P : Type ?u.245652
G : Type ?u.245655
H : Type ?u.245658
R : Type ?u.245661
S : Type ?u.245664
inst✝¹ : Zero M
inst✝ : Zero N
l : α →₀ M
f : α ↪ β
a : β
b : M
hb : b ≠ 0
h : embDomain f l = single a b
h_map_support : map f l.support = {a}
ha : a ∈ map f l.support
c : α
_hc₁ : c ∈ l.support
hc₂ : ↑f c = a
⊢ ∃ x, l = single x b ∧ ↑f x = a
α : Type u_1
β : Type u_3
γ : Type ?u.245637
ι : Type ?u.245640
M : Type u_2
M' : Type ?u.245646
N : Type ?u.245649
P : Type ?u.245652
G : Type ?u.245655
H : Type ?u.245658
R : Type ?u.245661
S : Type ?u.245664
inst✝¹ : Zero M
inst✝ : Zero N
l : α →₀ M
f : α ↪ β
a : β
b : M
hb : b ≠ 0
h : embDomain f l = single a b
h_map_support : map f l.support = {a}
ha : a ∈ map f l.support
⊢ ∃ x, l = single x b ∧ ↑f x = a
rcases Finset.mem_map.1 ha with ⟨c, _hc₁, hc₂⟩
case intro.intro
α : Type u_1
β : Type u_3
γ : Type ?u.245637
ι : Type ?u.245640
M : Type u_2
M' : Type ?u.245646
N : Type ?u.245649
P : Type ?u.245652
G : Type ?u.245655
H : Type ?u.245658
R : Type ?u.245661
S : Type ?u.245664
inst✝¹ : Zero M
inst✝ : Zero N
l : α →₀ M
f : α ↪ β
a : β
b : M
hb : b ≠ 0
h : embDomain f l = single a b
h_map_support : map f l.support = {a}
ha : a ∈ map f l.support
c : α
_hc₁ : c ∈ l.support
hc₂ : ↑f c = a
⊢ l = single c b ∧ ↑f c = a
case intro.intro
α : Type u_1
β : Type u_3
γ : Type ?u.245637
ι : Type ?u.245640
M : Type u_2
M' : Type ?u.245646
N : Type ?u.245649
P : Type ?u.245652
G : Type ?u.245655
H : Type ?u.245658
R : Type ?u.245661
S : Type ?u.245664
inst✝¹ : Zero M
inst✝ : Zero N
l : α →₀ M
f : α ↪ β
a : β
b : M
hb : b ≠ 0
h : embDomain f l = single a b
h_map_support : map f l.support = {a}
ha : a ∈ map f l.support
c : α
_hc₁ : c ∈ l.support
hc₂ : ↑f c = a
⊢ ∃ x, l = single x b ∧ ↑f x = a
use c
case intro.intro.left
α : Type u_1
β : Type u_3
γ : Type ?u.245637
ι : Type ?u.245640
M : Type u_2
M' : Type ?u.245646
N : Type ?u.245649
P : Type ?u.245652
G : Type ?u.245655
H : Type ?u.245658
R : Type ?u.245661
S : Type ?u.245664
inst✝¹ : Zero M
inst✝ : Zero N
l : α →₀ M
f : α ↪ β
a : β
b : M
hb : b ≠ 0
h : embDomain f l = single a b
h_map_support : map f l.support = {a}
ha : a ∈ map f l.support
c : α
_hc₁ : c ∈ l.support
hc₂ : ↑f c = a
⊢ l = single c b

case intro.intro.right
α : Type u_1
β : Type u_3
γ : Type ?u.245637
ι : Type ?u.245640
M : Type u_2
M' : Type ?u.245646
N : Type ?u.245649
P : Type ?u.245652
G : Type ?u.245655
H : Type ?u.245658
R : Type ?u.245661
S : Type ?u.245664
inst✝¹ : Zero M
inst✝ : Zero N
l : α →₀ M
f : α ↪ β
a : β
b : M
hb : b ≠ 0
h : embDomain f l = single a b
h_map_support : map f l.support = {a}
ha : a ∈ map f l.support
c : α
_hc₁ : c ∈ l.support
hc₂ : ↑f c = a
⊢ ↑f c = a
case intro.intro
α : Type u_1
β : Type u_3
γ : Type ?u.245637
ι : Type ?u.245640
M : Type u_2
M' : Type ?u.245646
N : Type ?u.245649
P : Type ?u.245652
G : Type ?u.245655
H : Type ?u.245658
R : Type ?u.245661
S : Type ?u.245664
inst✝¹ : Zero M
inst✝ : Zero N
l : α →₀ M
f : α ↪ β
a : β
b : M
hb : b ≠ 0
h : embDomain f l = single a b
h_map_support : map f l.support = {a}
ha : a ∈ map f l.support
c : α
_hc₁ : c ∈ l.support
hc₂ : ↑f c = a
⊢ l = single c b ∧ ↑f c = a
constructor
no goals
α : Type u_1
β : Type u_3
γ : Type ?u.245637
ι : Type ?u.245640
M : Type u_2
M' : Type ?u.245646
N : Type ?u.245649
P : Type ?u.245652
G : Type ?u.245655
H : Type ?u.245658
R : Type ?u.245661
S : Type ?u.245664
inst✝¹ : Zero M
inst✝ : Zero N
l : α →₀ M
f : α ↪ β
a : β
b : M
hb : b ≠ 0
h : embDomain f l = single a b
⊢ map f l.support = {a}
rw [← support_embDomain, h, support_single_ne_zero _ hb]
no goals
α : Type u_1
β : Type u_3
γ : Type ?u.245637
ι : Type ?u.245640
M : Type u_2
M' : Type ?u.245646
N : Type ?u.245649
P : Type ?u.245652
G : Type ?u.245655
H : Type ?u.245658
R : Type ?u.245661
S : Type ?u.245664
inst✝¹ : Zero M
inst✝ : Zero N
l : α →₀ M
f : α ↪ β
a : β
b : M
hb : b ≠ 0
h : embDomain f l = single a b
h_map_support : map f l.support = {a}
⊢ a ∈ map f l.support
simp only [h_map_support, Finset.mem_singleton]
case intro.intro.left.h
α : Type u_1
β : Type u_3
γ : Type ?u.245637
ι : Type ?u.245640
M : Type u_2
M' : Type ?u.245646
N : Type ?u.245649
P : Type ?u.245652
G : Type ?u.245655
H : Type ?u.245658
R : Type ?u.245661
S : Type ?u.245664
inst✝¹ : Zero M
inst✝ : Zero N
l : α →₀ M
f : α ↪ β
a : β
b : M
hb : b ≠ 0
h : embDomain f l = single a b
h_map_support : map f l.support = {a}
ha : a ∈ map f l.support
c : α
_hc₁ : c ∈ l.support
hc₂ : ↑f c = a
d : α
⊢ ↑l d = ↑(single c b) d
case intro.intro.left
α : Type u_1
β : Type u_3
γ : Type ?u.245637
ι : Type ?u.245640
M : Type u_2
M' : Type ?u.245646
N : Type ?u.245649
P : Type ?u.245652
G : Type ?u.245655
H : Type ?u.245658
R : Type ?u.245661
S : Type ?u.245664
inst✝¹ : Zero M
inst✝ : Zero N
l : α →₀ M
f : α ↪ β
a : β
b : M
hb : b ≠ 0
h : embDomain f l = single a b
h_map_support : map f l.support = {a}
ha : a ∈ map f l.support
c : α
_hc₁ : c ∈ l.support
hc₂ : ↑f c = a
⊢ l = single c b
ext d
case intro.intro.left.h
α : Type u_1
β : Type u_3
γ : Type ?u.245637
ι : Type ?u.245640
M : Type u_2
M' : Type ?u.245646
N : Type ?u.245649
P : Type ?u.245652
G : Type ?u.245655
H : Type ?u.245658
R : Type ?u.245661
S : Type ?u.245664
inst✝¹ : Zero M
inst✝ : Zero N
l : α →₀ M
f : α ↪ β
a : β
b : M
hb : b ≠ 0
h : embDomain f l = single a b
h_map_support : map f l.support = {a}
ha : a ∈ map f l.support
c : α
_hc₁ : c ∈ l.support
hc₂ : ↑f c = a
d : α
⊢ ↑(single a b) (↑f d) = ↑(single c b) d
case intro.intro.left.h
α : Type u_1
β : Type u_3
γ : Type ?u.245637
ι : Type ?u.245640
M : Type u_2
M' : Type ?u.245646
N : Type ?u.245649
P : Type ?u.245652
G : Type ?u.245655
H : Type ?u.245658
R : Type ?u.245661
S : Type ?u.245664
inst✝¹ : Zero M
inst✝ : Zero N
l : α →₀ M
f : α ↪ β
a : β
b : M
hb : b ≠ 0
h : embDomain f l = single a b
h_map_support : map f l.support = {a}
ha : a ∈ map f l.support
c : α
_hc₁ : c ∈ l.support
hc₂ : ↑f c = a
d : α
⊢ ↑l d = ↑(single c b) d
rw [← embDomain_apply f l, h]
case pos
α : Type u_1
β : Type u_3
γ : Type ?u.245637
ι : Type ?u.245640
M : Type u_2
M' : Type ?u.245646
N : Type ?u.245649
P : Type ?u.245652
G : Type ?u.245655
H : Type ?u.245658
R : Type ?u.245661
S : Type ?u.245664
inst✝¹ : Zero M
inst✝ : Zero N
l : α →₀ M
f : α ↪ β
a : β
b : M
hb : b ≠ 0
h : embDomain f l = single a b
h_map_support : map f l.support = {a}
ha : a ∈ map f l.support
c : α
_hc₁ : c ∈ l.support
hc₂ : ↑f c = a
d : α
h_cases : c = d
⊢ ↑(single a b) (↑f d) = ↑(single c b) d

case neg
α : Type u_1
β : Type u_3
γ : Type ?u.245637
ι : Type ?u.245640
M : Type u_2
M' : Type ?u.245646
N : Type ?u.245649
P : Type ?u.245652
G : Type ?u.245655
H : Type ?u.245658
R : Type ?u.245661
S : Type ?u.245664
inst✝¹ : Zero M
inst✝ : Zero N
l : α →₀ M
f : α ↪ β
a : β
b : M
hb : b ≠ 0
h : embDomain f l = single a b
h_map_support : map f l.support = {a}
ha : a ∈ map f l.support
c : α
_hc₁ : c ∈ l.support
hc₂ : ↑f c = a
d : α
h_cases : ¬c = d
⊢ ↑(single a b) (↑f d) = ↑(single c b) d
case intro.intro.left.h
α : Type u_1
β : Type u_3
γ : Type ?u.245637
ι : Type ?u.245640
M : Type u_2
M' : Type ?u.245646
N : Type ?u.245649
P : Type ?u.245652
G : Type ?u.245655
H : Type ?u.245658
R : Type ?u.245661
S : Type ?u.245664
inst✝¹ : Zero M
inst✝ : Zero N
l : α →₀ M
f : α ↪ β
a : β
b : M
hb : b ≠ 0
h : embDomain f l = single a b
h_map_support : map f l.support = {a}
ha : a ∈ map f l.support
c : α
_hc₁ : c ∈ l.support
hc₂ : ↑f c = a
d : α
⊢ ↑(single a b) (↑f d) = ↑(single c b) d
by_cases h_cases : c = d
no goals
case pos
α : Type u_1
β : Type u_3
γ : Type ?u.245637
ι : Type ?u.245640
M : Type u_2
M' : Type ?u.245646
N : Type ?u.245649
P : Type ?u.245652
G : Type ?u.245655
H : Type ?u.245658
R : Type ?u.245661
S : Type ?u.245664
inst✝¹ : Zero M
inst✝ : Zero N
l : α →₀ M
f : α ↪ β
a : β
b : M
hb : b ≠ 0
h : embDomain f l = single a b
h_map_support : map f l.support = {a}
ha : a ∈ map f l.support
c : α
_hc₁ : c ∈ l.support
hc₂ : ↑f c = a
d : α
h_cases : c = d
⊢ ↑(single a b) (↑f d) = ↑(single c b) d
simp only [Eq.symm h_cases, hc₂, single_eq_same]
case neg.hnc
α : Type u_1
β : Type u_3
γ : Type ?u.245637
ι : Type ?u.245640
M : Type u_2
M' : Type ?u.245646
N : Type ?u.245649
P : Type ?u.245652
G : Type ?u.245655
H : Type ?u.245658
R : Type ?u.245661
S : Type ?u.245664
inst✝¹ : Zero M
inst✝ : Zero N
l : α →₀ M
f : α ↪ β
a : β
b : M
hb : b ≠ 0
h : embDomain f l = single a b
h_map_support : map f l.support = {a}
ha : a ∈ map f l.support
c : α
_hc₁ : c ∈ l.support
hc₂ : ↑f c = a
d : α
h_cases : ¬c = d
⊢ ¬a = ↑f d
case neg
α : Type u_1
β : Type u_3
γ : Type ?u.245637
ι : Type ?u.245640
M : Type u_2
M' : Type ?u.245646
N : Type ?u.245649
P : Type ?u.245652
G : Type ?u.245655
H : Type ?u.245658
R : Type ?u.245661
S : Type ?u.245664
inst✝¹ : Zero M
inst✝ : Zero N
l : α →₀ M
f : α ↪ β
a : β
b : M
hb : b ≠ 0
h : embDomain f l = single a b
h_map_support : map f l.support = {a}
ha : a ∈ map f l.support
c : α
_hc₁ : c ∈ l.support
hc₂ : ↑f c = a
d : α
h_cases : ¬c = d
⊢ ↑(single a b) (↑f d) = ↑(single c b) d
rw [single_apply, single_apply, if_neg, if_neg h_cases]
case neg.hnc
α : Type u_1
β : Type u_3
γ : Type ?u.245637
ι : Type ?u.245640
M : Type u_2
M' : Type ?u.245646
N : Type ?u.245649
P : Type ?u.245652
G : Type ?u.245655
H : Type ?u.245658
R : Type ?u.245661
S : Type ?u.245664
inst✝¹ : Zero M
inst✝ : Zero N
l : α →₀ M
f : α ↪ β
a : β
b : M
hb : b ≠ 0
h : embDomain f l = single a b
h_map_support : map f l.support = {a}
ha : a ∈ map f l.support
c : α
_hc₁ : c ∈ l.support
hc₂ : ↑f c = a
d : α
h_cases : ¬c = d
hfd : a = ↑f d
⊢ False
case neg.hnc
α : Type u_1
β : Type u_3
γ : Type ?u.245637
ι : Type ?u.245640
M : Type u_2
M' : Type ?u.245646
N : Type ?u.245649
P : Type ?u.245652
G : Type ?u.245655
H : Type ?u.245658
R : Type ?u.245661
S : Type ?u.245664
inst✝¹ : Zero M
inst✝ : Zero N
l : α →₀ M
f : α ↪ β
a : β
b : M
hb : b ≠ 0
h : embDomain f l = single a b
h_map_support : map f l.support = {a}
ha : a ∈ map f l.support
c : α
_hc₁ : c ∈ l.support
hc₂ : ↑f c = a
d : α
h_cases : ¬c = d
⊢ ¬a = ↑f d
by_contra hfd
no goals
case neg.hnc
α : Type u_1
β : Type u_3
γ : Type ?u.245637
ι : Type ?u.245640
M : Type u_2
M' : Type ?u.245646
N : Type ?u.245649
P : Type ?u.245652
G : Type ?u.245655
H : Type ?u.245658
R : Type ?u.245661
S : Type ?u.245664
inst✝¹ : Zero M
inst✝ : Zero N
l : α →₀ M
f : α ↪ β
a : β
b : M
hb : b ≠ 0
h : embDomain f l = single a b
h_map_support : map f l.support = {a}
ha : a ∈ map f l.support
c : α
_hc₁ : c ∈ l.support
hc₂ : ↑f c = a
d : α
h_cases : ¬c = d
hfd : a = ↑f d
⊢ False
exact h_cases (f.injective (hc₂.trans hfd))
no goals
case intro.intro.right
α : Type u_1
β : Type u_3
γ : Type ?u.245637
ι : Type ?u.245640
M : Type u_2
M' : Type ?u.245646
N : Type ?u.245649
P : Type ?u.245652
G : Type ?u.245655
H : Type ?u.245658
R : Type ?u.245661
S : Type ?u.245664
inst✝¹ : Zero M
inst✝ : Zero N
l : α →₀ M
f : α ↪ β
a : β
b : M
hb : b ≠ 0
h : embDomain f l = single a b
h_map_support : map f l.support = {a}
ha : a ∈ map f l.support
c : α
_hc₁ : c ∈ l.support
hc₂ : ↑f c = a
⊢ ↑f c = a
exact hc₂