internlm/Lean-Github huggingface dataset:
Theorem: MvPolynomial.Finsupp.sum_update_add
Proof state before:
R : Type ?u.11
ι : Type u_3
inst✝² : CommSemiring R
α : Type u_1
β : Type u_2
inst✝¹ : AddCommMonoid α
inst✝ : AddCommMonoid β
f : ι →₀ α
i : ι
a : α
g : ι → α → β
hg : ∀ (i : ι), g i 0 = 0
hgg : ∀ (a : ι) (b₁ b₂ : α), g a (b₁ + b₂) = g a b₁ + g a b₂
⊢ (((Finsupp.erase i f).sum fun i => g i) + (Finsupp.single i a).sum fun i => g i) + g i (f i) =
    (Finsupp.erase i f + Finsupp.single i (f i)).sum g + g i a
Tactic:
rw [Finsupp.sum_add_index (fun i _ => hg i) fun i _ => hgg i]
Proof state after:
R : Type ?u.11
ι : Type u_3
inst✝² : CommSemiring R
α : Type u_1
β : Type u_2
inst✝¹ : AddCommMonoid α
inst✝ : AddCommMonoid β
f : ι →₀ α
i : ι
a : α
g : ι → α → β
hg : ∀ (i : ι), g i 0 = 0
hgg : ∀ (a : ι) (b₁ b₂ : α), g a (b₁ + b₂) = g a b₁ + g a b₂
⊢ (((Finsupp.erase i f).sum fun i => g i) + (Finsupp.single i a).sum fun i => g i) + g i (f i) =
    (((Finsupp.erase i f).sum fun i => g i) + (Finsupp.single i (f i)).sum fun i => g i) + g i a
Theorem: MvPolynomial.Finsupp.sum_update_add
Proof state before:
R : Type ?u.11
ι : Type u_3
inst✝² : CommSemiring R
α : Type u_1
β : Type u_2
inst✝¹ : AddCommMonoid α
inst✝ : AddCommMonoid β
f : ι →₀ α
i : ι
a : α
g : ι → α → β
hg : ∀ (i : ι), g i 0 = 0
hgg : ∀ (a : ι) (b₁ b₂ : α), g a (b₁ + b₂) = g a b₁ + g a b₂
⊢ (((Finsupp.erase i f).sum fun i => g i) + (Finsupp.single i a).sum fun i => g i) + g i (f i) =
    (((Finsupp.erase i f).sum fun i => g i) + (Finsupp.single i (f i)).sum fun i => g i) + g i a
Tactic:
rw [add_assoc]
Proof state after:
R : Type ?u.11
ι : Type u_3
inst✝² : CommSemiring R
α : Type u_1
β : Type u_2
inst✝¹ : AddCommMonoid α
inst✝ : AddCommMonoid β
f : ι →₀ α
i : ι
a : α
g : ι → α → β
hg : ∀ (i : ι), g i 0 = 0
hgg : ∀ (a : ι) (b₁ b₂ : α), g a (b₁ + b₂) = g a b₁ + g a b₂
⊢ ((Finsupp.erase i f).sum fun i => g i) + (((Finsupp.single i a).sum fun i => g i) + g i (f i)) =
    (((Finsupp.erase i f).sum fun i => g i) + (Finsupp.single i (f i)).sum fun i => g i) + g i a
Theorem: MvPolynomial.Finsupp.sum_update_add
Proof state before:
R : Type ?u.11
ι : Type u_3
inst✝² : CommSemiring R
α : Type u_1
β : Type u_2
inst✝¹ : AddCommMonoid α
inst✝ : AddCommMonoid β
f : ι →₀ α
i : ι
a : α
g : ι → α → β
hg : ∀ (i : ι), g i 0 = 0
hgg : ∀ (a : ι) (b₁ b₂ : α), g a (b₁ + b₂) = g a b₁ + g a b₂
⊢ ((Finsupp.erase i f).sum fun i => g i) + (((Finsupp.single i a).sum fun i => g i) + g i (f i)) =
    (((Finsupp.erase i f).sum fun i => g i) + (Finsupp.single i (f i)).sum fun i => g i) + g i a
Tactic:
rw [add_assoc]
Proof state after:
R : Type ?u.11
ι : Type u_3
inst✝² : CommSemiring R
α : Type u_1
β : Type u_2
inst✝¹ : AddCommMonoid α
inst✝ : AddCommMonoid β
f : ι →₀ α
i : ι
a : α
g : ι → α → β
hg : ∀ (i : ι), g i 0 = 0
hgg : ∀ (a : ι) (b₁ b₂ : α), g a (b₁ + b₂) = g a b₁ + g a b₂
⊢ ((Finsupp.erase i f).sum fun i => g i) + (((Finsupp.single i a).sum fun i => g i) + g i (f i)) =
    ((Finsupp.erase i f).sum fun i => g i) + (((Finsupp.single i (f i)).sum fun i => g i) + g i a)
Theorem: MvPolynomial.Finsupp.sum_update_add
Proof state before:
R : Type ?u.11
ι : Type u_3
inst✝² : CommSemiring R
α : Type u_1
β : Type u_2
inst✝¹ : AddCommMonoid α
inst✝ : AddCommMonoid β
f : ι →₀ α
i : ι
a : α
g : ι → α → β
hg : ∀ (i : ι), g i 0 = 0
hgg : ∀ (a : ι) (b₁ b₂ : α), g a (b₁ + b₂) = g a b₁ + g a b₂
⊢ ((Finsupp.erase i f).sum fun i => g i) + (((Finsupp.single i a).sum fun i => g i) + g i (f i)) =
    ((Finsupp.erase i f).sum fun i => g i) + (((Finsupp.single i (f i)).sum fun i => g i) + g i a)
Tactic:
congr 1
Proof state after:
case e_a
R : Type ?u.11
ι : Type u_3
inst✝² : CommSemiring R
α : Type u_1
β : Type u_2
inst✝¹ : AddCommMonoid α
inst✝ : AddCommMonoid β
f : ι →₀ α
i : ι
a : α
g : ι → α → β
hg : ∀ (i : ι), g i 0 = 0
hgg : ∀ (a : ι) (b₁ b₂ : α), g a (b₁ + b₂) = g a b₁ + g a b₂
⊢ ((Finsupp.single i a).sum fun i => g i) + g i (f i) = ((Finsupp.single i (f i)).sum fun i => g i) + g i a
Theorem: MvPolynomial.Finsupp.sum_update_add
Proof state before:
case e_a
R : Type ?u.11
ι : Type u_3
inst✝² : CommSemiring R
α : Type u_1
β : Type u_2
inst✝¹ : AddCommMonoid α
inst✝ : AddCommMonoid β
f : ι →₀ α
i : ι
a : α
g : ι → α → β
hg : ∀ (i : ι), g i 0 = 0
hgg : ∀ (a : ι) (b₁ b₂ : α), g a (b₁ + b₂) = g a b₁ + g a b₂
⊢ ((Finsupp.single i a).sum fun i => g i) + g i (f i) = ((Finsupp.single i (f i)).sum fun i => g i) + g i a
Tactic:
rw [add_comm]
Proof state after:
case e_a
R : Type ?u.11
ι : Type u_3
inst✝² : CommSemiring R
α : Type u_1
β : Type u_2
inst✝¹ : AddCommMonoid α
inst✝ : AddCommMonoid β
f : ι →₀ α
i : ι
a : α
g : ι → α → β
hg : ∀ (i : ι), g i 0 = 0
hgg : ∀ (a : ι) (b₁ b₂ : α), g a (b₁ + b₂) = g a b₁ + g a b₂
⊢ (g i (f i) + (Finsupp.single i a).sum fun i => g i) = ((Finsupp.single i (f i)).sum fun i => g i) + g i a
Theorem: MvPolynomial.Finsupp.sum_update_add
Proof state before:
case e_a
R : Type ?u.11
ι : Type u_3
inst✝² : CommSemiring R
α : Type u_1
β : Type u_2
inst✝¹ : AddCommMonoid α
inst✝ : AddCommMonoid β
f : ι →₀ α
i : ι
a : α
g : ι → α → β
hg : ∀ (i : ι), g i 0 = 0
hgg : ∀ (a : ι) (b₁ b₂ : α), g a (b₁ + b₂) = g a b₁ + g a b₂
⊢ (g i (f i) + (Finsupp.single i a).sum fun i => g i) = ((Finsupp.single i (f i)).sum fun i => g i) + g i a
Tactic:
rw [Finsupp.sum_single_index (hg _)]
Proof state after:
case e_a
R : Type ?u.11
ι : Type u_3
inst✝² : CommSemiring R
α : Type u_1
β : Type u_2
inst✝¹ : AddCommMonoid α
inst✝ : AddCommMonoid β
f : ι →₀ α
i : ι
a : α
g : ι → α → β
hg : ∀ (i : ι), g i 0 = 0
hgg : ∀ (a : ι) (b₁ b₂ : α), g a (b₁ + b₂) = g a b₁ + g a b₂
⊢ g i (f i) + g i a = ((Finsupp.single i (f i)).sum fun i => g i) + g i a
Theorem: MvPolynomial.Finsupp.sum_update_add
Proof state before:
case e_a
R : Type ?u.11
ι : Type u_3
inst✝² : CommSemiring R
α : Type u_1
β : Type u_2
inst✝¹ : AddCommMonoid α
inst✝ : AddCommMonoid β
f : ι →₀ α
i : ι
a : α
g : ι → α → β
hg : ∀ (i : ι), g i 0 = 0
hgg : ∀ (a : ι) (b₁ b₂ : α), g a (b₁ + b₂) = g a b₁ + g a b₂
⊢ g i (f i) + g i a = ((Finsupp.single i (f i)).sum fun i => g i) + g i a
Tactic:
rw [Finsupp.sum_single_index (hg _)]
Proof state after:
no goals
Theorem: MvPolynomial.Finsupp.support_mapDomain
Proof state before:
R : Type ?u.8691
ι : Type ?u.8694
inst✝¹ : CommSemiring R
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : AddCommMonoid M
f : α ↪ β
v : α →₀ M
⊢ (Finsupp.mapDomain (⇑f) v).support ⊆ Finset.map f v.support
Tactic:
classical
rw [Finsupp.mapDomain]
refine' Finset.Subset.trans Finsupp.support_sum _
simp only [Finsupp.mem_support_iff, Finset.biUnion_subset_iff_forall_subset, Ne]
intro x hx
apply Finset.Subset.trans Finsupp.support_single_subset
simp [hx]
Proof state after:
no goals
Theorem: MvPolynomial.Finsupp.support_mapDomain
Proof state before:
R : Type ?u.8691
ι : Type ?u.8694
inst✝¹ : CommSemiring R
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : AddCommMonoid M
f : α ↪ β
v : α →₀ M
⊢ (Finsupp.mapDomain (⇑f) v).support ⊆ Finset.map f v.support
Tactic:
rw [Finsupp.mapDomain]
Proof state after:
R : Type ?u.8691
ι : Type ?u.8694
inst✝¹ : CommSemiring R
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : AddCommMonoid M
f : α ↪ β
v : α →₀ M
⊢ (v.sum fun a => Finsupp.single (f a)).support ⊆ Finset.map f v.support
Theorem: MvPolynomial.Finsupp.support_mapDomain
Proof state before:
R : Type ?u.8691
ι : Type ?u.8694
inst✝¹ : CommSemiring R
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : AddCommMonoid M
f : α ↪ β
v : α →₀ M
⊢ (v.sum fun a => Finsupp.single (f a)).support ⊆ Finset.map f v.support
Tactic:
refine' Finset.Subset.trans Finsupp.support_sum _
Proof state after:
R : Type ?u.8691
ι : Type ?u.8694
inst✝¹ : CommSemiring R
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : AddCommMonoid M
f : α ↪ β
v : α →₀ M
⊢ (v.support.biUnion fun a => (Finsupp.single (f a) (v a)).support) ⊆ Finset.map f v.support
Theorem: MvPolynomial.Finsupp.support_mapDomain
Proof state before:
R : Type ?u.8691
ι : Type ?u.8694
inst✝¹ : CommSemiring R
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : AddCommMonoid M
f : α ↪ β
v : α →₀ M
⊢ (v.support.biUnion fun a => (Finsupp.single (f a) (v a)).support) ⊆ Finset.map f v.support
Tactic:
simp only [Finsupp.mem_support_iff, Finset.biUnion_subset_iff_forall_subset, Ne]
Proof state after:
R : Type ?u.8691
ι : Type ?u.8694
inst✝¹ : CommSemiring R
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : AddCommMonoid M
f : α ↪ β
v : α →₀ M
⊢ ∀ (x : α), ¬v x = 0 → (Finsupp.single (f x) (v x)).support ⊆ Finset.map f v.support
Theorem: MvPolynomial.Finsupp.support_mapDomain
Proof state before:
R : Type ?u.8691
ι : Type ?u.8694
inst✝¹ : CommSemiring R
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : AddCommMonoid M
f : α ↪ β
v : α →₀ M
⊢ ∀ (x : α), ¬v x = 0 → (Finsupp.single (f x) (v x)).support ⊆ Finset.map f v.support
Tactic:
intro x hx
Proof state after:
R : Type ?u.8691
ι : Type ?u.8694
inst✝¹ : CommSemiring R
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : AddCommMonoid M
f : α ↪ β
v : α →₀ M
x : α
hx : ¬v x = 0
⊢ (Finsupp.single (f x) (v x)).support ⊆ Finset.map f v.support
Theorem: MvPolynomial.Finsupp.support_mapDomain
Proof state before:
R : Type ?u.8691
ι : Type ?u.8694
inst✝¹ : CommSemiring R
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : AddCommMonoid M
f : α ↪ β
v : α →₀ M
x : α
hx : ¬v x = 0
⊢ (Finsupp.single (f x) (v x)).support ⊆ Finset.map f v.support
Tactic:
apply Finset.Subset.trans Finsupp.support_single_subset
Proof state after:
R : Type ?u.8691
ι : Type ?u.8694
inst✝¹ : CommSemiring R
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : AddCommMonoid M
f : α ↪ β
v : α →₀ M
x : α
hx : ¬v x = 0
⊢ {f x} ⊆ Finset.map f v.support
Theorem: MvPolynomial.Finsupp.support_mapDomain
Proof state before:
R : Type ?u.8691
ι : Type ?u.8694
inst✝¹ : CommSemiring R
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : AddCommMonoid M
f : α ↪ β
v : α →₀ M
x : α
hx : ¬v x = 0
⊢ {f x} ⊆ Finset.map f v.support
Tactic:
simp [hx]
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
⊢ (Finsupp.mapDomain f x) (f a) = x a
Tactic:
rw [Finsupp.mapDomain]
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
⊢ (x.sum fun a => Finsupp.single (f a)) (f a) = x 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
⊢ (x.sum fun a => Finsupp.single (f a)) (f a) = x a
Tactic:
simp only [Finsupp.sum_apply]
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
⊢ (x.sum fun a₁ b => (Finsupp.single (f a₁) b) (f a)) = x 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
⊢ (x.sum fun a₁ b => (Finsupp.single (f a₁) b) (f a)) = x a
Tactic:
rw [Finsupp.sum]
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
⊢ ∑ a_1 ∈ x.support, (Finsupp.single (f a_1) (x a_1)) (f a) = x 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
⊢ ∑ a_1 ∈ x.support, (Finsupp.single (f a_1) (x a_1)) (f a) = x a
Tactic:
simp_rw [Finsupp.single_apply]
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
⊢ (∑ 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:
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
⊢ (∑ x_1 ∈ x.support, if f x_1 = f a then x x_1 else 0) = x a
Tactic:
have : ∀ (a_1 : α) (_ : 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 := by
  intro a_1 ha_1
  split_ifs with hh
  rw [hf _ ha hh]
  exact hS ha_1
  rfl
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
⊢ (∑ 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:
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
⊢ (∑ x_1 ∈ x.support, if f x_1 = f a then x x_1 else 0) = x a
Tactic:
by_cases ha : a ∈ x.support
Proof state after:
case pos
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

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
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
⊢ ∀ 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
Tactic:
intro a_1 ha_1
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
a_1 : α
ha_1 : 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
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
a_1 : α
ha_1 : 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
Tactic:
split_ifs with hh
Proof state after:
case pos
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
a_1 : α
ha_1 : a_1 ∈ x.support
hh : f a_1 = f a
⊢ x a_1 = x a

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
a_1 : α
ha_1 : a_1 ∈ x.support
hh : ¬f a_1 = f a
⊢ 0 = 0
Theorem: MvPolynomial.Finsupp.mapDomain_apply'
Proof state before:
case pos
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
a_1 : α
ha_1 : a_1 ∈ x.support
hh : f a_1 = f a
⊢ x a_1 = x a

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
a_1 : α
ha_1 : a_1 ∈ x.support
hh : ¬f a_1 = f a
⊢ 0 = 0
Tactic:
rw [hf _ ha hh]
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
a_1 : α
ha_1 : a_1 ∈ x.support
hh : f a_1 = f a
⊢ a_1 ∈ S

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
a_1 : α
ha_1 : a_1 ∈ x.support
hh : ¬f a_1 = f a
⊢ 0 = 0
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
a_1 : α
ha_1 : a_1 ∈ x.support
hh : f a_1 = f a
⊢ a_1 ∈ S

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
a_1 : α
ha_1 : a_1 ∈ x.support
hh : ¬f a_1 = f a
⊢ 0 = 0
Tactic:
exact hS ha_1
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
a_1 : α
ha_1 : a_1 ∈ x.support
hh : ¬f a_1 = f a
⊢ 0 = 0
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
a_1 : α
ha_1 : a_1 ∈ x.support
hh : ¬f a_1 = f a
⊢ 0 = 0
Tactic:
rfl
Proof state after:
no goals
Theorem: MvPolynomial.Finsupp.mapDomain_apply'
Proof state before:
case pos
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:
rw [← Finset.add_sum_erase _ _ ha]
Proof state after:
case pos
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
⊢ ((if f a = f a then x a else 0) + ∑ x_1 ∈ x.support.erase a, if f x_1 = f a then x x_1 else 0) = x a
Theorem: MvPolynomial.Finsupp.mapDomain_apply'
Proof state before:
case pos
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
⊢ ((if f a = f a then x a else 0) + ∑ x_1 ∈ x.support.erase a, if f x_1 = f a then x x_1 else 0) = x a
Tactic:
simp only [if_true, eq_self_iff_true]
Proof state after:
case pos
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 a + ∑ x_1 ∈ x.support.erase a, if f x_1 = f a then x x_1 else 0) = x a
Theorem: MvPolynomial.Finsupp.mapDomain_apply'
Proof state before:
case pos
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 a + ∑ x_1 ∈ x.support.erase a, if f x_1 = f a then x x_1 else 0) = x a
Tactic:
convert add_zero (x a)
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
⊢ (∑ x_1 ∈ x.support.erase a, if f x_1 = f a then x x_1 else 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
⊢ (∑ x_1 ∈ x.support.erase a, if f x_1 = f a then x x_1 else 0) = 0
Tactic:
have h : ∀ i ∈ x.support.erase a, f i ≠ f a := by
  intro i hi
  have hix : i ∈ x.support := Finset.mem_of_mem_erase hi
  have hia : i ≠ a := Finset.ne_of_mem_erase hi
  exact hia ∘ hf (hS hix) (hS ha)
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
⊢ (∑ x_1 ∈ x.support.erase a, if f x_1 = f a then x x_1 else 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
⊢ (∑ x_1 ∈ x.support.erase a, if f x_1 = f a then x x_1 else 0) = 0
Tactic:
rw [← Finset.sum_coe_sort]
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 }, if f ↑i = f a then x ↑i else 0) = 0