case h
α : Type u_1
β : Type u_2
γ : Type ?u.311579
ι : Type ?u.311582
M : Type u_3
M' : Type ?u.311588
N : Type ?u.311591
P : Type ?u.311594
G : Type ?u.311597
H : Type ?u.311600
R : Type ?u.311603
S : Type ?u.311606
inst✝ : AddCommMonoid M
f : α → β
hf : Injective f
l : β →₀ M
hl : ↑l.support ⊆ Set.range f
a : β
⊢ ↑(mapDomain f (comapDomain f l (_ : Set.InjOn f (f ⁻¹' ↑l.support)))) a = ↑l a
α : Type u_1
β : Type u_2
γ : Type ?u.311579
ι : Type ?u.311582
M : Type u_3
M' : Type ?u.311588
N : Type ?u.311591
P : Type ?u.311594
G : Type ?u.311597
H : Type ?u.311600
R : Type ?u.311603
S : Type ?u.311606
inst✝ : AddCommMonoid M
f : α → β
hf : Injective f
l : β →₀ M
hl : ↑l.support ⊆ Set.range f
⊢ mapDomain f (comapDomain f l (_ : Set.InjOn f (f ⁻¹' ↑l.support))) = l
ext a
case pos
α : Type u_1
β : Type u_2
γ : Type ?u.311579
ι : Type ?u.311582
M : Type u_3
M' : Type ?u.311588
N : Type ?u.311591
P : Type ?u.311594
G : Type ?u.311597
H : Type ?u.311600
R : Type ?u.311603
S : Type ?u.311606
inst✝ : AddCommMonoid M
f : α → β
hf : Injective f
l : β →₀ M
hl : ↑l.support ⊆ Set.range f
a : β
h_cases : a ∈ Set.range f
⊢ ↑(mapDomain f (comapDomain f l (_ : Set.InjOn f (f ⁻¹' ↑l.support)))) a = ↑l a

case neg
α : Type u_1
β : Type u_2
γ : Type ?u.311579
ι : Type ?u.311582
M : Type u_3
M' : Type ?u.311588
N : Type ?u.311591
P : Type ?u.311594
G : Type ?u.311597
H : Type ?u.311600
R : Type ?u.311603
S : Type ?u.311606
inst✝ : AddCommMonoid M
f : α → β
hf : Injective f
l : β →₀ M
hl : ↑l.support ⊆ Set.range f
a : β
h_cases : ¬a ∈ Set.range f
⊢ ↑(mapDomain f (comapDomain f l (_ : Set.InjOn f (f ⁻¹' ↑l.support)))) a = ↑l a
case h
α : Type u_1
β : Type u_2
γ : Type ?u.311579
ι : Type ?u.311582
M : Type u_3
M' : Type ?u.311588
N : Type ?u.311591
P : Type ?u.311594
G : Type ?u.311597
H : Type ?u.311600
R : Type ?u.311603
S : Type ?u.311606
inst✝ : AddCommMonoid M
f : α → β
hf : Injective f
l : β →₀ M
hl : ↑l.support ⊆ Set.range f
a : β
⊢ ↑(mapDomain f (comapDomain f l (_ : Set.InjOn f (f ⁻¹' ↑l.support)))) a = ↑l a
by_cases h_cases : a ∈ Set.range f
case pos.intro
α : Type u_1
β : Type u_2
γ : Type ?u.311579
ι : Type ?u.311582
M : Type u_3
M' : Type ?u.311588
N : Type ?u.311591
P : Type ?u.311594
G : Type ?u.311597
H : Type ?u.311600
R : Type ?u.311603
S : Type ?u.311606
inst✝ : AddCommMonoid M
f : α → β
hf : Injective f
l : β →₀ M
hl : ↑l.support ⊆ Set.range f
a : β
h_cases : a ∈ Set.range f
b : α
hb : f b = a
⊢ ↑(mapDomain f (comapDomain f l (_ : Set.InjOn f (f ⁻¹' ↑l.support)))) a = ↑l a
case pos
α : Type u_1
β : Type u_2
γ : Type ?u.311579
ι : Type ?u.311582
M : Type u_3
M' : Type ?u.311588
N : Type ?u.311591
P : Type ?u.311594
G : Type ?u.311597
H : Type ?u.311600
R : Type ?u.311603
S : Type ?u.311606
inst✝ : AddCommMonoid M
f : α → β
hf : Injective f
l : β →₀ M
hl : ↑l.support ⊆ Set.range f
a : β
h_cases : a ∈ Set.range f
⊢ ↑(mapDomain f (comapDomain f l (_ : Set.InjOn f (f ⁻¹' ↑l.support)))) a = ↑l a
rcases Set.mem_range.1 h_cases with ⟨b, hb⟩
no goals
case pos.intro
α : Type u_1
β : Type u_2
γ : Type ?u.311579
ι : Type ?u.311582
M : Type u_3
M' : Type ?u.311588
N : Type ?u.311591
P : Type ?u.311594
G : Type ?u.311597
H : Type ?u.311600
R : Type ?u.311603
S : Type ?u.311606
inst✝ : AddCommMonoid M
f : α → β
hf : Injective f
l : β →₀ M
hl : ↑l.support ⊆ Set.range f
a : β
h_cases : a ∈ Set.range f
b : α
hb : f b = a
⊢ ↑(mapDomain f (comapDomain f l (_ : Set.InjOn f (f ⁻¹' ↑l.support)))) a = ↑l a
rw [hb.symm, mapDomain_apply hf, comapDomain_apply]
case neg
α : Type u_1
β : Type u_2
γ : Type ?u.311579
ι : Type ?u.311582
M : Type u_3
M' : Type ?u.311588
N : Type ?u.311591
P : Type ?u.311594
G : Type ?u.311597
H : Type ?u.311600
R : Type ?u.311603
S : Type ?u.311606
inst✝ : AddCommMonoid M
f : α → β
hf : Injective f
l : β →₀ M
hl : ↑l.support ⊆ Set.range f
a : β
h_cases : ¬a ∈ Set.range f
⊢ 0 = ↑l a
case neg
α : Type u_1
β : Type u_2
γ : Type ?u.311579
ι : Type ?u.311582
M : Type u_3
M' : Type ?u.311588
N : Type ?u.311591
P : Type ?u.311594
G : Type ?u.311597
H : Type ?u.311600
R : Type ?u.311603
S : Type ?u.311606
inst✝ : AddCommMonoid M
f : α → β
hf : Injective f
l : β →₀ M
hl : ↑l.support ⊆ Set.range f
a : β
h_cases : ¬a ∈ Set.range f
⊢ ↑(mapDomain f (comapDomain f l (_ : Set.InjOn f (f ⁻¹' ↑l.support)))) a = ↑l a
rw [mapDomain_notin_range _ _ h_cases]
case neg
α : Type u_1
β : Type u_2
γ : Type ?u.311579
ι : Type ?u.311582
M : Type u_3
M' : Type ?u.311588
N : Type ?u.311591
P : Type ?u.311594
G : Type ?u.311597
H : Type ?u.311600
R : Type ?u.311603
S : Type ?u.311606
inst✝ : AddCommMonoid M
f : α → β
hf : Injective f
l : β →₀ M
hl : ↑l.support ⊆ Set.range f
a : β
h_cases : ¬a ∈ Set.range f
h_contr : ¬0 = ↑l a
⊢ False
case neg
α : Type u_1
β : Type u_2
γ : Type ?u.311579
ι : Type ?u.311582
M : Type u_3
M' : Type ?u.311588
N : Type ?u.311591
P : Type ?u.311594
G : Type ?u.311597
H : Type ?u.311600
R : Type ?u.311603
S : Type ?u.311606
inst✝ : AddCommMonoid M
f : α → β
hf : Injective f
l : β →₀ M
hl : ↑l.support ⊆ Set.range f
a : β
h_cases : ¬a ∈ Set.range f
⊢ 0 = ↑l a
by_contra h_contr
no goals
case neg
α : Type u_1
β : Type u_2
γ : Type ?u.311579
ι : Type ?u.311582
M : Type u_3
M' : Type ?u.311588
N : Type ?u.311591
P : Type ?u.311594
G : Type ?u.311597
H : Type ?u.311600
R : Type ?u.311603
S : Type ?u.311606
inst✝ : AddCommMonoid M
f : α → β
hf : Injective f
l : β →₀ M
hl : ↑l.support ⊆ Set.range f
a : β
h_cases : ¬a ∈ Set.range f
h_contr : ¬0 = ↑l a
⊢ False
apply h_cases (hl <| Finset.mem_coe.2 <| mem_support_iff.2 fun h => h_contr h.symm)