α : Type u_1
β : Type u_2
γ : Type ?u.292155
ι : Type ?u.292158
M : Type u_3
M' : Type ?u.292164
N : Type ?u.292167
P : Type ?u.292170
G : Type ?u.292173
H : Type ?u.292176
R : Type ?u.292179
S✝ : Type ?u.292182
inst✝ : AddCommMonoid M
v v₁✝ v₂✝ : α →₀ M
S : Set α
f : α → β
hf : Set.InjOn f S
v₁ : α →₀ M
hv₁ : v₁ ∈ {w | ↑w.support ⊆ S}
v₂ : α →₀ M
hv₂ : v₂ ∈ {w | ↑w.support ⊆ S}
eq : mapDomain f v₁ = mapDomain f v₂
⊢ v₁ = v₂
α : Type u_1
β : Type u_2
γ : Type ?u.292155
ι : Type ?u.292158
M : Type u_3
M' : Type ?u.292164
N : Type ?u.292167
P : Type ?u.292170
G : Type ?u.292173
H : Type ?u.292176
R : Type ?u.292179
S✝ : Type ?u.292182
inst✝ : AddCommMonoid M
v v₁ v₂ : α →₀ M
S : Set α
f : α → β
hf : Set.InjOn f S
⊢ Set.InjOn (mapDomain f) {w | ↑w.support ⊆ S}
intro v₁ hv₁ v₂ hv₂ eq
case h
α : Type u_1
β : Type u_2
γ : Type ?u.292155
ι : Type ?u.292158
M : Type u_3
M' : Type ?u.292164
N : Type ?u.292167
P : Type ?u.292170
G : Type ?u.292173
H : Type ?u.292176
R : Type ?u.292179
S✝ : Type ?u.292182
inst✝ : AddCommMonoid M
v v₁✝ v₂✝ : α →₀ M
S : Set α
f : α → β
hf : Set.InjOn f S
v₁ : α →₀ M
hv₁ : v₁ ∈ {w | ↑w.support ⊆ S}
v₂ : α →₀ M
hv₂ : v₂ ∈ {w | ↑w.support ⊆ S}
eq : mapDomain f v₁ = mapDomain f v₂
a : α
⊢ ↑v₁ a = ↑v₂ a
α : Type u_1
β : Type u_2
γ : Type ?u.292155
ι : Type ?u.292158
M : Type u_3
M' : Type ?u.292164
N : Type ?u.292167
P : Type ?u.292170
G : Type ?u.292173
H : Type ?u.292176
R : Type ?u.292179
S✝ : Type ?u.292182
inst✝ : AddCommMonoid M
v v₁✝ v₂✝ : α →₀ M
S : Set α
f : α → β
hf : Set.InjOn f S
v₁ : α →₀ M
hv₁ : v₁ ∈ {w | ↑w.support ⊆ S}
v₂ : α →₀ M
hv₂ : v₂ ∈ {w | ↑w.support ⊆ S}
eq : mapDomain f v₁ = mapDomain f v₂
⊢ v₁ = v₂
ext a
case pos
α : Type u_1
β : Type u_2
γ : Type ?u.292155
ι : Type ?u.292158
M : Type u_3
M' : Type ?u.292164
N : Type ?u.292167
P : Type ?u.292170
G : Type ?u.292173
H : Type ?u.292176
R : Type ?u.292179
S✝ : Type ?u.292182
inst✝ : AddCommMonoid M
v v₁✝ v₂✝ : α →₀ M
S : Set α
f : α → β
hf : Set.InjOn f S
v₁ : α →₀ M
hv₁ : v₁ ∈ {w | ↑w.support ⊆ S}
v₂ : α →₀ M
hv₂ : v₂ ∈ {w | ↑w.support ⊆ S}
eq : mapDomain f v₁ = mapDomain f v₂
a : α
h : a ∈ v₁.support ∪ v₂.support
⊢ ↑v₁ a = ↑v₂ a

case neg
α : Type u_1
β : Type u_2
γ : Type ?u.292155
ι : Type ?u.292158
M : Type u_3
M' : Type ?u.292164
N : Type ?u.292167
P : Type ?u.292170
G : Type ?u.292173
H : Type ?u.292176
R : Type ?u.292179
S✝ : Type ?u.292182
inst✝ : AddCommMonoid M
v v₁✝ v₂✝ : α →₀ M
S : Set α
f : α → β
hf : Set.InjOn f S
v₁ : α →₀ M
hv₁ : v₁ ∈ {w | ↑w.support ⊆ S}
v₂ : α →₀ M
hv₂ : v₂ ∈ {w | ↑w.support ⊆ S}
eq : mapDomain f v₁ = mapDomain f v₂
a : α
h : ¬a ∈ v₁.support ∪ v₂.support
⊢ ↑v₁ a = ↑v₂ a
case h
α : Type u_1
β : Type u_2
γ : Type ?u.292155
ι : Type ?u.292158
M : Type u_3
M' : Type ?u.292164
N : Type ?u.292167
P : Type ?u.292170
G : Type ?u.292173
H : Type ?u.292176
R : Type ?u.292179
S✝ : Type ?u.292182
inst✝ : AddCommMonoid M
v v₁✝ v₂✝ : α →₀ M
S : Set α
f : α → β
hf : Set.InjOn f S
v₁ : α →₀ M
hv₁ : v₁ ∈ {w | ↑w.support ⊆ S}
v₂ : α →₀ M
hv₂ : v₂ ∈ {w | ↑w.support ⊆ S}
eq : mapDomain f v₁ = mapDomain f v₂
a : α
⊢ ↑v₁ a = ↑v₂ a
by_cases h : a ∈ v₁.support ∪ v₂.support
case a
α : Type u_1
β : Type u_2
γ : Type ?u.292155
ι : Type ?u.292158
M : Type u_3
M' : Type ?u.292164
N : Type ?u.292167
P : Type ?u.292170
G : Type ?u.292173
H : Type ?u.292176
R : Type ?u.292179
S✝ : Type ?u.292182
inst✝ : AddCommMonoid M
v v₁✝ v₂✝ : α →₀ M
S : Set α
f : α → β
hf : Set.InjOn f S
v₁ : α →₀ M
hv₁ : v₁ ∈ {w | ↑w.support ⊆ S}
v₂ : α →₀ M
hv₂ : v₂ ∈ {w | ↑w.support ⊆ S}
eq : mapDomain f v₁ = mapDomain f v₂
a : α
h : a ∈ v₁.support ∪ v₂.support
⊢ a ∈ ↑v₁.support ∪ ↑v₂.support
α : Type u_1
β : Type u_2
γ : Type ?u.292155
ι : Type ?u.292158
M : Type u_3
M' : Type ?u.292164
N : Type ?u.292167
P : Type ?u.292170
G : Type ?u.292173
H : Type ?u.292176
R : Type ?u.292179
S✝ : Type ?u.292182
inst✝ : AddCommMonoid M
v v₁✝ v₂✝ : α →₀ M
S : Set α
f : α → β
hf : Set.InjOn f S
v₁ : α →₀ M
hv₁ : v₁ ∈ {w | ↑w.support ⊆ S}
v₂ : α →₀ M
hv₂ : v₂ ∈ {w | ↑w.support ⊆ S}
eq : mapDomain f v₁ = mapDomain f v₂
a : α
h : a ∈ v₁.support ∪ v₂.support
⊢ a ∈ S
apply Set.union_subset hv₁ hv₂
no goals
case a
α : Type u_1
β : Type u_2
γ : Type ?u.292155
ι : Type ?u.292158
M : Type u_3
M' : Type ?u.292164
N : Type ?u.292167
P : Type ?u.292170
G : Type ?u.292173
H : Type ?u.292176
R : Type ?u.292179
S✝ : Type ?u.292182
inst✝ : AddCommMonoid M
v v₁✝ v₂✝ : α →₀ M
S : Set α
f : α → β
hf : Set.InjOn f S
v₁ : α →₀ M
hv₁ : v₁ ∈ {w | ↑w.support ⊆ S}
v₂ : α →₀ M
hv₂ : v₂ ∈ {w | ↑w.support ⊆ S}
eq : mapDomain f v₁ = mapDomain f v₂
a : α
h : a ∈ v₁.support ∪ v₂.support
⊢ a ∈ ↑v₁.support ∪ ↑v₂.support
exact_mod_cast h
case neg
α : Type u_1
β : Type u_2
γ : Type ?u.292155
ι : Type ?u.292158
M : Type u_3
M' : Type ?u.292164
N : Type ?u.292167
P : Type ?u.292170
G : Type ?u.292173
H : Type ?u.292176
R : Type ?u.292179
S✝ : Type ?u.292182
inst✝ : AddCommMonoid M
v v₁✝ v₂✝ : α →₀ M
S : Set α
f : α → β
hf : Set.InjOn f S
v₁ : α →₀ M
hv₁ : v₁ ∈ {w | ↑w.support ⊆ S}
v₂ : α →₀ M
hv₂ : v₂ ∈ {w | ↑w.support ⊆ S}
eq : mapDomain f v₁ = mapDomain f v₂
a : α
h : ↑v₁ a = 0 ∧ ↑v₂ a = 0
⊢ ↑v₁ a = ↑v₂ a
case neg
α : Type u_1
β : Type u_2
γ : Type ?u.292155
ι : Type ?u.292158
M : Type u_3
M' : Type ?u.292164
N : Type ?u.292167
P : Type ?u.292170
G : Type ?u.292173
H : Type ?u.292176
R : Type ?u.292179
S✝ : Type ?u.292182
inst✝ : AddCommMonoid M
v v₁✝ v₂✝ : α →₀ M
S : Set α
f : α → β
hf : Set.InjOn f S
v₁ : α →₀ M
hv₁ : v₁ ∈ {w | ↑w.support ⊆ S}
v₂ : α →₀ M
hv₂ : v₂ ∈ {w | ↑w.support ⊆ S}
eq : mapDomain f v₁ = mapDomain f v₂
a : α
h : ¬a ∈ v₁.support ∪ v₂.support
⊢ ↑v₁ a = ↑v₂ a
simp only [not_or, mem_union, not_not, mem_support_iff] at h
no goals
case neg
α : Type u_1
β : Type u_2
γ : Type ?u.292155
ι : Type ?u.292158
M : Type u_3
M' : Type ?u.292164
N : Type ?u.292167
P : Type ?u.292170
G : Type ?u.292173
H : Type ?u.292176
R : Type ?u.292179
S✝ : Type ?u.292182
inst✝ : AddCommMonoid M
v v₁✝ v₂✝ : α →₀ M
S : Set α
f : α → β
hf : Set.InjOn f S
v₁ : α →₀ M
hv₁ : v₁ ∈ {w | ↑w.support ⊆ S}
v₂ : α →₀ M
hv₂ : v₂ ∈ {w | ↑w.support ⊆ S}
eq : mapDomain f v₁ = mapDomain f v₂
a : α
h : ↑v₁ a = 0 ∧ ↑v₂ a = 0
⊢ ↑v₁ a = ↑v₂ a
simp [h]