case h
α : Type u_1
β : Type u_2
γ : Type ?u.255631
ι : Type ?u.255634
M : Type u_3
M' : Type ?u.255640
N : Type ?u.255643
P : Type ?u.255646
G : Type ?u.255649
H : Type ?u.255652
R : Type ?u.255655
S : Type ?u.255658
inst✝¹ : Zero M
inst✝ : Zero N
f : α ↪ β
a : α
m : M
b : β
⊢ ↑(embDomain f (single a m)) b = ↑(single (↑f a) m) b
α : Type u_1
β : Type u_2
γ : Type ?u.255631
ι : Type ?u.255634
M : Type u_3
M' : Type ?u.255640
N : Type ?u.255643
P : Type ?u.255646
G : Type ?u.255649
H : Type ?u.255652
R : Type ?u.255655
S : Type ?u.255658
inst✝¹ : Zero M
inst✝ : Zero N
f : α ↪ β
a : α
m : M
⊢ embDomain f (single a m) = single (↑f a) m
ext b
case pos
α : Type u_1
β : Type u_2
γ : Type ?u.255631
ι : Type ?u.255634
M : Type u_3
M' : Type ?u.255640
N : Type ?u.255643
P : Type ?u.255646
G : Type ?u.255649
H : Type ?u.255652
R : Type ?u.255655
S : Type ?u.255658
inst✝¹ : Zero M
inst✝ : Zero N
f : α ↪ β
a : α
m : M
b : β
h : b ∈ Set.range ↑f
⊢ ↑(embDomain f (single a m)) b = ↑(single (↑f a) m) b

case neg
α : Type u_1
β : Type u_2
γ : Type ?u.255631
ι : Type ?u.255634
M : Type u_3
M' : Type ?u.255640
N : Type ?u.255643
P : Type ?u.255646
G : Type ?u.255649
H : Type ?u.255652
R : Type ?u.255655
S : Type ?u.255658
inst✝¹ : Zero M
inst✝ : Zero N
f : α ↪ β
a : α
m : M
b : β
h : ¬b ∈ Set.range ↑f
⊢ ↑(embDomain f (single a m)) b = ↑(single (↑f a) m) b
case h
α : Type u_1
β : Type u_2
γ : Type ?u.255631
ι : Type ?u.255634
M : Type u_3
M' : Type ?u.255640
N : Type ?u.255643
P : Type ?u.255646
G : Type ?u.255649
H : Type ?u.255652
R : Type ?u.255655
S : Type ?u.255658
inst✝¹ : Zero M
inst✝ : Zero N
f : α ↪ β
a : α
m : M
b : β
⊢ ↑(embDomain f (single a m)) b = ↑(single (↑f a) m) b
by_cases h : b ∈ Set.range f
case pos.intro
α : Type u_1
β : Type u_2
γ : Type ?u.255631
ι : Type ?u.255634
M : Type u_3
M' : Type ?u.255640
N : Type ?u.255643
P : Type ?u.255646
G : Type ?u.255649
H : Type ?u.255652
R : Type ?u.255655
S : Type ?u.255658
inst✝¹ : Zero M
inst✝ : Zero N
f : α ↪ β
a : α
m : M
a' : α
⊢ ↑(embDomain f (single a m)) (↑f a') = ↑(single (↑f a) m) (↑f a')
case pos
α : Type u_1
β : Type u_2
γ : Type ?u.255631
ι : Type ?u.255634
M : Type u_3
M' : Type ?u.255640
N : Type ?u.255643
P : Type ?u.255646
G : Type ?u.255649
H : Type ?u.255652
R : Type ?u.255655
S : Type ?u.255658
inst✝¹ : Zero M
inst✝ : Zero N
f : α ↪ β
a : α
m : M
b : β
h : b ∈ Set.range ↑f
⊢ ↑(embDomain f (single a m)) b = ↑(single (↑f a) m) b
rcases h with ⟨a', rfl⟩
no goals
case pos.intro
α : Type u_1
β : Type u_2
γ : Type ?u.255631
ι : Type ?u.255634
M : Type u_3
M' : Type ?u.255640
N : Type ?u.255643
P : Type ?u.255646
G : Type ?u.255649
H : Type ?u.255652
R : Type ?u.255655
S : Type ?u.255658
inst✝¹ : Zero M
inst✝ : Zero N
f : α ↪ β
a : α
m : M
a' : α
⊢ ↑(embDomain f (single a m)) (↑f a') = ↑(single (↑f a) m) (↑f a')
simp [single_apply]
case neg
α : Type u_1
β : Type u_2
γ : Type ?u.255631
ι : Type ?u.255634
M : Type u_3
M' : Type ?u.255640
N : Type ?u.255643
P : Type ?u.255646
G : Type ?u.255649
H : Type ?u.255652
R : Type ?u.255655
S : Type ?u.255658
inst✝¹ : Zero M
inst✝ : Zero N
f : α ↪ β
a : α
m : M
b : β
h : ¬b ∈ Set.range ↑f
⊢ 0 = if ↑f a = b then m else 0
case neg
α : Type u_1
β : Type u_2
γ : Type ?u.255631
ι : Type ?u.255634
M : Type u_3
M' : Type ?u.255640
N : Type ?u.255643
P : Type ?u.255646
G : Type ?u.255649
H : Type ?u.255652
R : Type ?u.255655
S : Type ?u.255658
inst✝¹ : Zero M
inst✝ : Zero N
f : α ↪ β
a : α
m : M
b : β
h : ¬b ∈ Set.range ↑f
⊢ ↑(embDomain f (single a m)) b = ↑(single (↑f a) m) b
simp only [embDomain_notin_range, h, single_apply, not_false_iff]
case neg.hnc
α : Type u_1
β : Type u_2
γ : Type ?u.255631
ι : Type ?u.255634
M : Type u_3
M' : Type ?u.255640
N : Type ?u.255643
P : Type ?u.255646
G : Type ?u.255649
H : Type ?u.255652
R : Type ?u.255655
S : Type ?u.255658
inst✝¹ : Zero M
inst✝ : Zero N
f : α ↪ β
a : α
m : M
b : β
h : ¬b ∈ Set.range ↑f
⊢ ¬↑f a = b
case neg
α : Type u_1
β : Type u_2
γ : Type ?u.255631
ι : Type ?u.255634
M : Type u_3
M' : Type ?u.255640
N : Type ?u.255643
P : Type ?u.255646
G : Type ?u.255649
H : Type ?u.255652
R : Type ?u.255655
S : Type ?u.255658
inst✝¹ : Zero M
inst✝ : Zero N
f : α ↪ β
a : α
m : M
b : β
h : ¬b ∈ Set.range ↑f
⊢ 0 = if ↑f a = b then m else 0
rw [if_neg]
case neg.hnc
α : Type u_1
β : Type u_2
γ : Type ?u.255631
ι : Type ?u.255634
M : Type u_3
M' : Type ?u.255640
N : Type ?u.255643
P : Type ?u.255646
G : Type ?u.255649
H : Type ?u.255652
R : Type ?u.255655
S : Type ?u.255658
inst✝¹ : Zero M
inst✝ : Zero N
f : α ↪ β
a : α
m : M
h : ¬↑f a ∈ Set.range ↑f
⊢ False
case neg.hnc
α : Type u_1
β : Type u_2
γ : Type ?u.255631
ι : Type ?u.255634
M : Type u_3
M' : Type ?u.255640
N : Type ?u.255643
P : Type ?u.255646
G : Type ?u.255649
H : Type ?u.255652
R : Type ?u.255655
S : Type ?u.255658
inst✝¹ : Zero M
inst✝ : Zero N
f : α ↪ β
a : α
m : M
b : β
h : ¬b ∈ Set.range ↑f
⊢ ¬↑f a = b
rintro rfl
no goals
case neg.hnc
α : Type u_1
β : Type u_2
γ : Type ?u.255631
ι : Type ?u.255634
M : Type u_3
M' : Type ?u.255640
N : Type ?u.255643
P : Type ?u.255646
G : Type ?u.255649
H : Type ?u.255652
R : Type ?u.255655
S : Type ?u.255658
inst✝¹ : Zero M
inst✝ : Zero N
f : α ↪ β
a : α
m : M
h : ¬↑f a ∈ Set.range ↑f
⊢ False
simp at h