internlm/Lean-Github huggingface dataset:
Theorem: MvPolynomial.Finsupp.mapDomain_apply'
Proof state before:
case h.e'_2.h.e'_6
R : Type ?u.13136
ι : Type ?u.13139
inst✝¹ : CommSemiring R
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : AddCommMonoid M
S : Set α
f : α → β
x : α →₀ M
hS : ↑x.support ⊆ S
hf : Set.InjOn f S
a : α
ha✝ : a ∈ S
this : ∀ a_1 ∈ x.support, (if f a_1 = f a then x a_1 else 0) = if f a_1 = f a then x a else 0
ha : a ∈ x.support
h : ∀ i ∈ x.support.erase a, f i ≠ f a
⊢ (∑ i : { x_1 // x_1 ∈ x.support.erase a }, if f ↑i = f a then x ↑i else 0) = 0
Tactic:
conv_lhs =>
  congr; rfl; ext i
  rw [if_neg (h i.1 i.2)]
Proof state after:
case h.e'_2.h.e'_6
R : Type ?u.13136
ι : Type ?u.13139
inst✝¹ : CommSemiring R
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : AddCommMonoid M
S : Set α
f : α → β
x : α →₀ M
hS : ↑x.support ⊆ S
hf : Set.InjOn f S
a : α
ha✝ : a ∈ S
this : ∀ a_1 ∈ x.support, (if f a_1 = f a then x a_1 else 0) = if f a_1 = f a then x a else 0
ha : a ∈ x.support
h : ∀ i ∈ x.support.erase a, f i ≠ f a
⊢ ∑ i : { x_1 // x_1 ∈ x.support.erase a }, 0 = 0
Theorem: MvPolynomial.Finsupp.mapDomain_apply'
Proof state before:
case h.e'_2.h.e'_6
R : Type ?u.13136
ι : Type ?u.13139
inst✝¹ : CommSemiring R
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : AddCommMonoid M
S : Set α
f : α → β
x : α →₀ M
hS : ↑x.support ⊆ S
hf : Set.InjOn f S
a : α
ha✝ : a ∈ S
this : ∀ a_1 ∈ x.support, (if f a_1 = f a then x a_1 else 0) = if f a_1 = f a then x a else 0
ha : a ∈ x.support
h : ∀ i ∈ x.support.erase a, f i ≠ f a
⊢ ∑ i : { x_1 // x_1 ∈ x.support.erase a }, 0 = 0
Tactic:
simp only [Finset.sum_const_zero]
Proof state after:
no goals
Theorem: MvPolynomial.Finsupp.mapDomain_apply'
Proof state before:
R : Type ?u.13136
ι : Type ?u.13139
inst✝¹ : CommSemiring R
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : AddCommMonoid M
S : Set α
f : α → β
x : α →₀ M
hS : ↑x.support ⊆ S
hf : Set.InjOn f S
a : α
ha✝ : a ∈ S
this : ∀ a_1 ∈ x.support, (if f a_1 = f a then x a_1 else 0) = if f a_1 = f a then x a else 0
ha : a ∈ x.support
⊢ ∀ i ∈ x.support.erase a, f i ≠ f a
Tactic:
intro i hi
Proof state after:
R : Type ?u.13136
ι : Type ?u.13139
inst✝¹ : CommSemiring R
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : AddCommMonoid M
S : Set α
f : α → β
x : α →₀ M
hS : ↑x.support ⊆ S
hf : Set.InjOn f S
a : α
ha✝ : a ∈ S
this : ∀ a_1 ∈ x.support, (if f a_1 = f a then x a_1 else 0) = if f a_1 = f a then x a else 0
ha : a ∈ x.support
i : α
hi : i ∈ x.support.erase a
⊢ f i ≠ f a
Theorem: MvPolynomial.Finsupp.mapDomain_apply'
Proof state before:
R : Type ?u.13136
ι : Type ?u.13139
inst✝¹ : CommSemiring R
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : AddCommMonoid M
S : Set α
f : α → β
x : α →₀ M
hS : ↑x.support ⊆ S
hf : Set.InjOn f S
a : α
ha✝ : a ∈ S
this : ∀ a_1 ∈ x.support, (if f a_1 = f a then x a_1 else 0) = if f a_1 = f a then x a else 0
ha : a ∈ x.support
i : α
hi : i ∈ x.support.erase a
⊢ f i ≠ f a
Tactic:
have hix : i ∈ x.support := Finset.mem_of_mem_erase hi
Proof state after:
R : Type ?u.13136
ι : Type ?u.13139
inst✝¹ : CommSemiring R
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : AddCommMonoid M
S : Set α
f : α → β
x : α →₀ M
hS : ↑x.support ⊆ S
hf : Set.InjOn f S
a : α
ha✝ : a ∈ S
this : ∀ a_1 ∈ x.support, (if f a_1 = f a then x a_1 else 0) = if f a_1 = f a then x a else 0
ha : a ∈ x.support
i : α
hi : i ∈ x.support.erase a
hix : i ∈ x.support
⊢ f i ≠ f a
Theorem: MvPolynomial.Finsupp.mapDomain_apply'
Proof state before:
R : Type ?u.13136
ι : Type ?u.13139
inst✝¹ : CommSemiring R
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : AddCommMonoid M
S : Set α
f : α → β
x : α →₀ M
hS : ↑x.support ⊆ S
hf : Set.InjOn f S
a : α
ha✝ : a ∈ S
this : ∀ a_1 ∈ x.support, (if f a_1 = f a then x a_1 else 0) = if f a_1 = f a then x a else 0
ha : a ∈ x.support
i : α
hi : i ∈ x.support.erase a
hix : i ∈ x.support
⊢ f i ≠ f a
Tactic:
have hia : i ≠ a := Finset.ne_of_mem_erase hi
Proof state after:
R : Type ?u.13136
ι : Type ?u.13139
inst✝¹ : CommSemiring R
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : AddCommMonoid M
S : Set α
f : α → β
x : α →₀ M
hS : ↑x.support ⊆ S
hf : Set.InjOn f S
a : α
ha✝ : a ∈ S
this : ∀ a_1 ∈ x.support, (if f a_1 = f a then x a_1 else 0) = if f a_1 = f a then x a else 0
ha : a ∈ x.support
i : α
hi : i ∈ x.support.erase a
hix : i ∈ x.support
hia : i ≠ a
⊢ f i ≠ f a
Theorem: MvPolynomial.Finsupp.mapDomain_apply'
Proof state before:
R : Type ?u.13136
ι : Type ?u.13139
inst✝¹ : CommSemiring R
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : AddCommMonoid M
S : Set α
f : α → β
x : α →₀ M
hS : ↑x.support ⊆ S
hf : Set.InjOn f S
a : α
ha✝ : a ∈ S
this : ∀ a_1 ∈ x.support, (if f a_1 = f a then x a_1 else 0) = if f a_1 = f a then x a else 0
ha : a ∈ x.support
i : α
hi : i ∈ x.support.erase a
hix : i ∈ x.support
hia : i ≠ a
⊢ f i ≠ f a
Tactic:
exact hia ∘ hf (hS hix) (hS ha)
Proof state after:
no goals
Theorem: MvPolynomial.Finsupp.mapDomain_apply'
Proof state before:
case neg
R : Type ?u.13136
ι : Type ?u.13139
inst✝¹ : CommSemiring R
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : AddCommMonoid M
S : Set α
f : α → β
x : α →₀ M
hS : ↑x.support ⊆ S
hf : Set.InjOn f S
a : α
ha✝ : a ∈ S
this : ∀ a_1 ∈ x.support, (if f a_1 = f a then x a_1 else 0) = if f a_1 = f a then x a else 0
ha : a ∉ x.support
⊢ (∑ x_1 ∈ x.support, if f x_1 = f a then x x_1 else 0) = x a
Tactic:
simp at ha
Proof state after:
case neg
R : Type ?u.13136
ι : Type ?u.13139
inst✝¹ : CommSemiring R
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : AddCommMonoid M
S : Set α
f : α → β
x : α →₀ M
hS : ↑x.support ⊆ S
hf : Set.InjOn f S
a : α
ha✝ : a ∈ S
this : ∀ a_1 ∈ x.support, (if f a_1 = f a then x a_1 else 0) = if f a_1 = f a then x a else 0
ha : x a = 0
⊢ (∑ x_1 ∈ x.support, if f x_1 = f a then x x_1 else 0) = x a
Theorem: MvPolynomial.Finsupp.mapDomain_apply'
Proof state before:
case neg
R : Type ?u.13136
ι : Type ?u.13139
inst✝¹ : CommSemiring R
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : AddCommMonoid M
S : Set α
f : α → β
x : α →₀ M
hS : ↑x.support ⊆ S
hf : Set.InjOn f S
a : α
ha✝ : a ∈ S
this : ∀ a_1 ∈ x.support, (if f a_1 = f a then x a_1 else 0) = if f a_1 = f a then x a else 0
ha : x a = 0
⊢ (∑ x_1 ∈ x.support, if f x_1 = f a then x x_1 else 0) = x a
Tactic:
rw [← Finset.sum_coe_sort]
Proof state after:
case neg
R : Type ?u.13136
ι : Type ?u.13139
inst✝¹ : CommSemiring R
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : AddCommMonoid M
S : Set α
f : α → β
x : α →₀ M
hS : ↑x.support ⊆ S
hf : Set.InjOn f S
a : α
ha✝ : a ∈ S
this : ∀ a_1 ∈ x.support, (if f a_1 = f a then x a_1 else 0) = if f a_1 = f a then x a else 0
ha : x a = 0
⊢ (∑ i : { x_1 // x_1 ∈ x.support }, if f ↑i = f a then x ↑i else 0) = x a
Theorem: MvPolynomial.Finsupp.mapDomain_apply'
Proof state before:
case neg
R : Type ?u.13136
ι : Type ?u.13139
inst✝¹ : CommSemiring R
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : AddCommMonoid M
S : Set α
f : α → β
x : α →₀ M
hS : ↑x.support ⊆ S
hf : Set.InjOn f S
a : α
ha✝ : a ∈ S
this : ∀ a_1 ∈ x.support, (if f a_1 = f a then x a_1 else 0) = if f a_1 = f a then x a else 0
ha : x a = 0
⊢ (∑ i : { x_1 // x_1 ∈ x.support }, if f ↑i = f a then x ↑i else 0) = x a
Tactic:
conv_lhs =>
  congr; rfl; ext i
  rw [this i.1 i.2]
Proof state after:
case neg
R : Type ?u.13136
ι : Type ?u.13139
inst✝¹ : CommSemiring R
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : AddCommMonoid M
S : Set α
f : α → β
x : α →₀ M
hS : ↑x.support ⊆ S
hf : Set.InjOn f S
a : α
ha✝ : a ∈ S
this : ∀ a_1 ∈ x.support, (if f a_1 = f a then x a_1 else 0) = if f a_1 = f a then x a else 0
ha : x a = 0
⊢ (∑ i : { x_1 // x_1 ∈ x.support }, if f ↑i = f a then x a else 0) = x a
Theorem: MvPolynomial.Finsupp.mapDomain_apply'
Proof state before:
case neg
R : Type ?u.13136
ι : Type ?u.13139
inst✝¹ : CommSemiring R
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : AddCommMonoid M
S : Set α
f : α → β
x : α →₀ M
hS : ↑x.support ⊆ S
hf : Set.InjOn f S
a : α
ha✝ : a ∈ S
this : ∀ a_1 ∈ x.support, (if f a_1 = f a then x a_1 else 0) = if f a_1 = f a then x a else 0
ha : x a = 0
⊢ (∑ i : { x_1 // x_1 ∈ x.support }, if f ↑i = f a then x a else 0) = x a
Tactic:
simp [ha]
Proof state after:
no goals
Theorem: MvPolynomial.Finsupp.mapDomain_injOn
Proof 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
Proof 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₂
Theorem: MvPolynomial.Finsupp.mapDomain_injOn
Proof 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
Proof 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
Theorem: MvPolynomial.Finsupp.mapDomain_injOn
Proof 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]
Proof 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
Theorem: MvPolynomial.Finsupp.mapDomain_injOn
Proof 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₂
Proof 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
Theorem: MvPolynomial.Finsupp.mapDomain_injOn
Proof 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]
Proof state after:
no goals
Theorem: MvPolynomial.Finsupp.mapDomain_injOn
Proof 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₂
Proof 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
Theorem: MvPolynomial.Finsupp.mapDomain_injOn
Proof 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
Proof 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
Theorem: MvPolynomial.Finsupp.mapDomain_injOn
Proof 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
Proof 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
Theorem: MvPolynomial.Finsupp.mapDomain_injOn
Proof 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
Proof 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
Theorem: MvPolynomial.Finsupp.mapDomain_injOn
Proof 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
Proof state after:
no goals
Theorem: MvPolynomial.Finsupp.mapDomain_injOn
Proof 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
Proof 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
Theorem: MvPolynomial.Finsupp.mapDomain_injOn
Proof 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
Proof state after:
no goals
Theorem: MvPolynomial.Finsupp.mapDomain_injOn
Proof 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
Proof 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
Theorem: MvPolynomial.Finsupp.mapDomain_injOn
Proof 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]
Proof state after:
no goals
Theorem: MvPolynomial.homogenization_zero
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
⊢ homogenization i 0 = 0
Tactic:
simp [homogenization]
Proof state after:
no goals
Theorem: MvPolynomial.homogenization_one
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
⊢ homogenization i 1 = 1
Tactic:
simp only [homogenization, totalDegree_one, zero_tsub, add_zero, Finsupp.single_zero]
Proof state after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
⊢ Finsupp.mapDomain (fun j => j) 1 = 1
Theorem: MvPolynomial.homogenization_one
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
⊢ Finsupp.mapDomain (fun j => j) 1 = 1
Tactic:
erw [Finsupp.mapDomain_single]
Proof state after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
⊢ Finsupp.single 0 1 = 1
Theorem: MvPolynomial.homogenization_one
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
⊢ Finsupp.single 0 1 = 1
Tactic:
rfl
Proof state after:
no goals
Theorem: MvPolynomial.homogenization_C
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
c : R
⊢ homogenization i (C c) = C c
Tactic:
simp only [homogenization, totalDegree_C, zero_tsub]
Proof state after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
c : R
⊢ Finsupp.mapDomain (fun j => j + Finsupp.single i 0) (C c) = C c
Theorem: MvPolynomial.homogenization_C
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
c : R
⊢ Finsupp.mapDomain (fun j => j + Finsupp.single i 0) (C c) = C c
Tactic:
convert Finsupp.mapDomain_single (M := R) using 1
Proof state after:
case h.e'_3
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
c : R
⊢ C c = Finsupp.single (0 + Finsupp.single i 0) c
Theorem: MvPolynomial.homogenization_C
Proof state before:
case h.e'_3
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
c : R
⊢ C c = Finsupp.single (0 + Finsupp.single i 0) c
Tactic:
rw [single_eq_monomial]
Proof state after:
case h.e'_3
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
c : R
⊢ C c = (monomial (0 + Finsupp.single i 0)) c
Theorem: MvPolynomial.homogenization_C
Proof state before:
case h.e'_3
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
c : R
⊢ C c = (monomial (0 + Finsupp.single i 0)) c
Tactic:
have : (0 : ι →₀ ℕ) i = 0 := by simp only [Finsupp.coe_zero, Pi.zero_apply]
Proof state after:
case h.e'_3
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
c : R
this : 0 i = 0
⊢ C c = (monomial (0 + Finsupp.single i 0)) c
Theorem: MvPolynomial.homogenization_C
Proof state before:
case h.e'_3
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
c : R
this : 0 i = 0
⊢ C c = (monomial (0 + Finsupp.single i 0)) c
Tactic:
rw [← this]
Proof state after:
case h.e'_3
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
c : R
this : 0 i = 0
⊢ C c = (monomial (0 + Finsupp.single i (0 i))) c
Theorem: MvPolynomial.homogenization_C
Proof state before:
case h.e'_3
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
c : R
this : 0 i = 0
⊢ C c = (monomial (0 + Finsupp.single i (0 i))) c
Tactic:
simp
Proof state after:
no goals
Theorem: MvPolynomial.homogenization_C
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
c : R
⊢ 0 i = 0
Tactic:
simp only [Finsupp.coe_zero, Pi.zero_apply]
Proof state after:
no goals
Theorem: MvPolynomial.homogenization_monomial
Proof state before:
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
i : ι
s : ι →₀ ℕ
r : R
⊢ homogenization i ((monomial s) r) = (monomial s) r
Tactic:
by_cases hr : r = 0
Proof state after:
case pos
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
i : ι
s : ι →₀ ℕ
r : R
hr : r = 0
⊢ homogenization i ((monomial s) r) = (monomial s) r

case neg
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
i : ι
s : ι →₀ ℕ
r : R
hr : ¬r = 0
⊢ homogenization i ((monomial s) r) = (monomial s) r