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

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₂
⊢ (f.update i a).sum g + g i (f i) = f.sum g + g i a
Tactic:
classical
simp_rw [Finsupp.update_eq_erase_add_single]
rw [Finsupp.sum_add_index (fun i _ => hg i) fun i _ => hgg i]
conv_rhs => rw [← Finsupp.update_self f i]
rw [Finsupp.update_eq_erase_add_single]
rw [Finsupp.sum_add_index (fun i _ => hg i) fun i _ => hgg i]
rw [add_assoc]
rw [add_assoc]
congr 1
rw [add_comm]
rw [Finsupp.sum_single_index (hg _)]
rw [Finsupp.sum_single_index (hg _)]
State after:
no goals

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₂
⊢ (f.update i a).sum g + g i (f i) = f.sum g + g i a
Tactic:
simp_rw [Finsupp.update_eq_erase_add_single]
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 + Finsupp.single i a).sum g + g i (f i) = f.sum g + g i a

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 + Finsupp.single i a).sum g + g i (f i) = f.sum g + g i a
Tactic:
rw [Finsupp.sum_add_index (fun i _ => hg i) fun i _ => hgg i]
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) = f.sum g + g i a

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) = f.sum g + g i a
Tactic:
conv_rhs => rw [← Finsupp.update_self f i]
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) =
    (f.update i (f i)).sum g + g i a

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) =
    (f.update i (f i)).sum g + g i a
Tactic:
rw [Finsupp.update_eq_erase_add_single]
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 + Finsupp.single i (f i)).sum g + g i a

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]
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

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]
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

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]
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)

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
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

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]
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

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 _)]
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

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 _)]
State after:
no goals