Theorem: MvPolynomial.Finsupp.mapDomain_injOn (FltRegular/ReadyForMathlib/Homogenization.lean)

State before:
R : Type ?u.35750
ι : Type ?u.35753
inst✝¹ : CommSemiring R
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : AddCommMonoid M
S : Set α
f : α → β
hf : Set.InjOn f S
⊢ Set.InjOn (Finsupp.mapDomain f) {w | ↑w.support ⊆ S}
Tactic:
intro v₁ hv₁ v₂ hv₂ eq
State after:
R : Type ?u.35750
ι : Type ?u.35753
inst✝¹ : CommSemiring R
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : AddCommMonoid 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 : Finsupp.mapDomain f v₁ = Finsupp.mapDomain f v₂
⊢ v₁ = v₂

State before:
R : Type ?u.35750
ι : Type ?u.35753
inst✝¹ : CommSemiring R
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : AddCommMonoid 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 : Finsupp.mapDomain f v₁ = Finsupp.mapDomain f v₂
⊢ v₁ = v₂
Tactic:
ext a
State after:
case h
R : Type ?u.35750
ι : Type ?u.35753
inst✝¹ : CommSemiring R
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : AddCommMonoid 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 : Finsupp.mapDomain f v₁ = Finsupp.mapDomain f v₂
a : α
⊢ v₁ a = v₂ a

State before:
case h
R : Type ?u.35750
ι : Type ?u.35753
inst✝¹ : CommSemiring R
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : AddCommMonoid 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 : Finsupp.mapDomain f v₁ = Finsupp.mapDomain f v₂
a : α
⊢ v₁ a = v₂ a
Tactic:
have : Finsupp.mapDomain f v₁ (f a) = Finsupp.mapDomain f v₂ (f a) := by rw [eq]
State after:
case h
R : Type ?u.35750
ι : Type ?u.35753
inst✝¹ : CommSemiring R
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : AddCommMonoid 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 : Finsupp.mapDomain f v₁ = Finsupp.mapDomain f v₂
a : α
this : (Finsupp.mapDomain f v₁) (f a) = (Finsupp.mapDomain f v₂) (f a)
⊢ v₁ a = v₂ a

State before:
case h
R : Type ?u.35750
ι : Type ?u.35753
inst✝¹ : CommSemiring R
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : AddCommMonoid 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 : Finsupp.mapDomain f v₁ = Finsupp.mapDomain f v₂
a : α
this : (Finsupp.mapDomain f v₁) (f a) = (Finsupp.mapDomain f v₂) (f a)
⊢ v₁ a = v₂ a
Tactic:
rw [Set.mem_setOf_eq] at hv₁ hv₂
State after:
case h
R : Type ?u.35750
ι : Type ?u.35753
inst✝¹ : CommSemiring R
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : AddCommMonoid M
S : Set α
f : α → β
hf : Set.InjOn f S
v₁ : α →₀ M
hv₁ : ↑v₁.support ⊆ S
v₂ : α →₀ M
hv₂ : ↑v₂.support ⊆ S
eq : Finsupp.mapDomain f v₁ = Finsupp.mapDomain f v₂
a : α
this : (Finsupp.mapDomain f v₁) (f a) = (Finsupp.mapDomain f v₂) (f a)
⊢ v₁ a = v₂ a

State before:
R : Type ?u.35750
ι : Type ?u.35753
inst✝¹ : CommSemiring R
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : AddCommMonoid 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 : Finsupp.mapDomain f v₁ = Finsupp.mapDomain f v₂
a : α
⊢ (Finsupp.mapDomain f v₁) (f a) = (Finsupp.mapDomain f v₂) (f a)
Tactic:
rw [eq]
State after:
no goals

State before:
case h
R : Type ?u.35750
ι : Type ?u.35753
inst✝¹ : CommSemiring R
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : AddCommMonoid M
S : Set α
f : α → β
hf : Set.InjOn f S
v₁ : α →₀ M
hv₁ : ↑v₁.support ⊆ S
v₂ : α →₀ M
hv₂ : ↑v₂.support ⊆ S
eq : Finsupp.mapDomain f v₁ = Finsupp.mapDomain f v₂
a : α
this : (Finsupp.mapDomain f v₁) (f a) = (Finsupp.mapDomain f v₂) (f a)
⊢ v₁ a = v₂ a
Tactic:
have hu : (v₁.support ∪ v₂.support : Set α) ⊆ S := Set.union_subset hv₁ hv₂
State after:
case h
R : Type ?u.35750
ι : Type ?u.35753
inst✝¹ : CommSemiring R
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : AddCommMonoid M
S : Set α
f : α → β
hf : Set.InjOn f S
v₁ : α →₀ M
hv₁ : ↑v₁.support ⊆ S
v₂ : α →₀ M
hv₂ : ↑v₂.support ⊆ S
eq : Finsupp.mapDomain f v₁ = Finsupp.mapDomain f v₂
a : α
this : (Finsupp.mapDomain f v₁) (f a) = (Finsupp.mapDomain f v₂) (f a)
hu : ↑v₁.support ∪ ↑v₂.support ⊆ S
⊢ v₁ a = v₂ a

State before:
case h
R : Type ?u.35750
ι : Type ?u.35753
inst✝¹ : CommSemiring R
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : AddCommMonoid M
S : Set α
f : α → β
hf : Set.InjOn f S
v₁ : α →₀ M
hv₁ : ↑v₁.support ⊆ S
v₂ : α →₀ M
hv₂ : ↑v₂.support ⊆ S
eq : Finsupp.mapDomain f v₁ = Finsupp.mapDomain f v₂
a : α
this : (Finsupp.mapDomain f v₁) (f a) = (Finsupp.mapDomain f v₂) (f a)
hu : ↑v₁.support ∪ ↑v₂.support ⊆ S
⊢ v₁ a = v₂ a
Tactic:
by_cases h : a ∈ v₁.support ∪ v₂.support
State after:
case pos
R : Type ?u.35750
ι : Type ?u.35753
inst✝¹ : CommSemiring R
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : AddCommMonoid M
S : Set α
f : α → β
hf : Set.InjOn f S
v₁ : α →₀ M
hv₁ : ↑v₁.support ⊆ S
v₂ : α →₀ M
hv₂ : ↑v₂.support ⊆ S
eq : Finsupp.mapDomain f v₁ = Finsupp.mapDomain f v₂
a : α
this : (Finsupp.mapDomain f v₁) (f a) = (Finsupp.mapDomain f v₂) (f a)
hu : ↑v₁.support ∪ ↑v₂.support ⊆ S
h : a ∈ v₁.support ∪ v₂.support
⊢ v₁ a = v₂ a

case neg
R : Type ?u.35750
ι : Type ?u.35753
inst✝¹ : CommSemiring R
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : AddCommMonoid M
S : Set α
f : α → β
hf : Set.InjOn f S
v₁ : α →₀ M
hv₁ : ↑v₁.support ⊆ S
v₂ : α →₀ M
hv₂ : ↑v₂.support ⊆ S
eq : Finsupp.mapDomain f v₁ = Finsupp.mapDomain f v₂
a : α
this : (Finsupp.mapDomain f v₁) (f a) = (Finsupp.mapDomain f v₂) (f a)
hu : ↑v₁.support ∪ ↑v₂.support ⊆ S
h : a ∉ v₁.support ∪ v₂.support
⊢ v₁ a = v₂ a

State before:
case pos
R : Type ?u.35750
ι : Type ?u.35753
inst✝¹ : CommSemiring R
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : AddCommMonoid M
S : Set α
f : α → β
hf : Set.InjOn f S
v₁ : α →₀ M
hv₁ : ↑v₁.support ⊆ S
v₂ : α →₀ M
hv₂ : ↑v₂.support ⊆ S
eq : Finsupp.mapDomain f v₁ = Finsupp.mapDomain f v₂
a : α
this : (Finsupp.mapDomain f v₁) (f a) = (Finsupp.mapDomain f v₂) (f a)
hu : ↑v₁.support ∪ ↑v₂.support ⊆ S
h : a ∈ v₁.support ∪ v₂.support
⊢ v₁ a = v₂ a
Tactic:
rwa [mapDomain_apply' S _ hv₁ hf _, mapDomain_apply' S _ hv₂ hf _] at this
State after:
R : Type ?u.35750
ι : Type ?u.35753
inst✝¹ : CommSemiring R
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : AddCommMonoid M
S : Set α
f : α → β
hf : Set.InjOn f S
v₁ : α →₀ M
hv₁ : ↑v₁.support ⊆ S
v₂ : α →₀ M
hv₂ : ↑v₂.support ⊆ S
eq : Finsupp.mapDomain f v₁ = Finsupp.mapDomain f v₂
a : α
this : v₁ a = (Finsupp.mapDomain f v₂) (f a)
hu : ↑v₁.support ∪ ↑v₂.support ⊆ S
h : a ∈ v₁.support ∪ v₂.support
⊢ a ∈ S

R : Type ?u.35750
ι : Type ?u.35753
inst✝¹ : CommSemiring R
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : AddCommMonoid M
S : Set α
f : α → β
hf : Set.InjOn f S
v₁ : α →₀ M
hv₁ : ↑v₁.support ⊆ S
v₂ : α →₀ M
hv₂ : ↑v₂.support ⊆ S
eq : Finsupp.mapDomain f v₁ = Finsupp.mapDomain f v₂
a : α
this : (Finsupp.mapDomain f v₁) (f a) = (Finsupp.mapDomain f v₂) (f a)
hu : ↑v₁.support ∪ ↑v₂.support ⊆ S
h : a ∈ v₁.support ∪ v₂.support
⊢ a ∈ S

State before:
R : Type ?u.35750
ι : Type ?u.35753
inst✝¹ : CommSemiring R
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : AddCommMonoid M
S : Set α
f : α → β
hf : Set.InjOn f S
v₁ : α →₀ M
hv₁ : ↑v₁.support ⊆ S
v₂ : α →₀ M
hv₂ : ↑v₂.support ⊆ S
eq : Finsupp.mapDomain f v₁ = Finsupp.mapDomain f v₂
a : α
this : v₁ a = (Finsupp.mapDomain f v₂) (f a)
hu : ↑v₁.support ∪ ↑v₂.support ⊆ S
h : a ∈ v₁.support ∪ v₂.support
⊢ a ∈ S
Tactic:
apply hu
State after:
case a
R : Type ?u.35750
ι : Type ?u.35753
inst✝¹ : CommSemiring R
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : AddCommMonoid M
S : Set α
f : α → β
hf : Set.InjOn f S
v₁ : α →₀ M
hv₁ : ↑v₁.support ⊆ S
v₂ : α →₀ M
hv₂ : ↑v₂.support ⊆ S
eq : Finsupp.mapDomain f v₁ = Finsupp.mapDomain f v₂
a : α
this : v₁ a = (Finsupp.mapDomain f v₂) (f a)
hu : ↑v₁.support ∪ ↑v₂.support ⊆ S
h : a ∈ v₁.support ∪ v₂.support
⊢ a ∈ ↑v₁.support ∪ ↑v₂.support

State before:
case a
R : Type ?u.35750
ι : Type ?u.35753
inst✝¹ : CommSemiring R
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : AddCommMonoid M
S : Set α
f : α → β
hf : Set.InjOn f S
v₁ : α →₀ M
hv₁ : ↑v₁.support ⊆ S
v₂ : α →₀ M
hv₂ : ↑v₂.support ⊆ S
eq : Finsupp.mapDomain f v₁ = Finsupp.mapDomain f v₂
a : α
this : v₁ a = (Finsupp.mapDomain f v₂) (f a)
hu : ↑v₁.support ∪ ↑v₂.support ⊆ S
h : a ∈ v₁.support ∪ v₂.support
⊢ a ∈ ↑v₁.support ∪ ↑v₂.support
Tactic:
exact_mod_cast h
State after:
no goals

State before:
R : Type ?u.35750
ι : Type ?u.35753
inst✝¹ : CommSemiring R
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : AddCommMonoid M
S : Set α
f : α → β
hf : Set.InjOn f S
v₁ : α →₀ M
hv₁ : ↑v₁.support ⊆ S
v₂ : α →₀ M
hv₂ : ↑v₂.support ⊆ S
eq : Finsupp.mapDomain f v₁ = Finsupp.mapDomain f v₂
a : α
this : (Finsupp.mapDomain f v₁) (f a) = (Finsupp.mapDomain f v₂) (f a)
hu : ↑v₁.support ∪ ↑v₂.support ⊆ S
h : a ∈ v₁.support ∪ v₂.support
⊢ a ∈ S
Tactic:
apply hu
State after:
case a
R : Type ?u.35750
ι : Type ?u.35753
inst✝¹ : CommSemiring R
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : AddCommMonoid M
S : Set α
f : α → β
hf : Set.InjOn f S
v₁ : α →₀ M
hv₁ : ↑v₁.support ⊆ S
v₂ : α →₀ M
hv₂ : ↑v₂.support ⊆ S
eq : Finsupp.mapDomain f v₁ = Finsupp.mapDomain f v₂
a : α
this : (Finsupp.mapDomain f v₁) (f a) = (Finsupp.mapDomain f v₂) (f a)
hu : ↑v₁.support ∪ ↑v₂.support ⊆ S
h : a ∈ v₁.support ∪ v₂.support
⊢ a ∈ ↑v₁.support ∪ ↑v₂.support

State before:
case a
R : Type ?u.35750
ι : Type ?u.35753
inst✝¹ : CommSemiring R
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : AddCommMonoid M
S : Set α
f : α → β
hf : Set.InjOn f S
v₁ : α →₀ M
hv₁ : ↑v₁.support ⊆ S
v₂ : α →₀ M
hv₂ : ↑v₂.support ⊆ S
eq : Finsupp.mapDomain f v₁ = Finsupp.mapDomain f v₂
a : α
this : (Finsupp.mapDomain f v₁) (f a) = (Finsupp.mapDomain f v₂) (f a)
hu : ↑v₁.support ∪ ↑v₂.support ⊆ S
h : a ∈ v₁.support ∪ v₂.support
⊢ a ∈ ↑v₁.support ∪ ↑v₂.support
Tactic:
exact_mod_cast h
State after:
no goals

State before:
case neg
R : Type ?u.35750
ι : Type ?u.35753
inst✝¹ : CommSemiring R
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : AddCommMonoid M
S : Set α
f : α → β
hf : Set.InjOn f S
v₁ : α →₀ M
hv₁ : ↑v₁.support ⊆ S
v₂ : α →₀ M
hv₂ : ↑v₂.support ⊆ S
eq : Finsupp.mapDomain f v₁ = Finsupp.mapDomain f v₂
a : α
this : (Finsupp.mapDomain f v₁) (f a) = (Finsupp.mapDomain f v₂) (f a)
hu : ↑v₁.support ∪ ↑v₂.support ⊆ S
h : a ∉ v₁.support ∪ v₂.support
⊢ v₁ a = v₂ a
Tactic:
simp only [not_or, mem_union, Classical.not_not, Finsupp.mem_support_iff] at h
State after:
case neg
R : Type ?u.35750
ι : Type ?u.35753
inst✝¹ : CommSemiring R
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : AddCommMonoid M
S : Set α
f : α → β
hf : Set.InjOn f S
v₁ : α →₀ M
hv₁ : ↑v₁.support ⊆ S
v₂ : α →₀ M
hv₂ : ↑v₂.support ⊆ S
eq : Finsupp.mapDomain f v₁ = Finsupp.mapDomain f v₂
a : α
this : (Finsupp.mapDomain f v₁) (f a) = (Finsupp.mapDomain f v₂) (f a)
hu : ↑v₁.support ∪ ↑v₂.support ⊆ S
h : v₁ a = 0 ∧ v₂ a = 0
⊢ v₁ a = v₂ a

State before:
case neg
R : Type ?u.35750
ι : Type ?u.35753
inst✝¹ : CommSemiring R
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : AddCommMonoid M
S : Set α
f : α → β
hf : Set.InjOn f S
v₁ : α →₀ M
hv₁ : ↑v₁.support ⊆ S
v₂ : α →₀ M
hv₂ : ↑v₂.support ⊆ S
eq : Finsupp.mapDomain f v₁ = Finsupp.mapDomain f v₂
a : α
this : (Finsupp.mapDomain f v₁) (f a) = (Finsupp.mapDomain f v₂) (f a)
hu : ↑v₁.support ∪ ↑v₂.support ⊆ S
h : v₁ a = 0 ∧ v₂ a = 0
⊢ v₁ a = v₂ a
Tactic:
simp [h]
State after:
no goals