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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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