Theorem: rel_of_dfinsupp_sum_of_rel_add (DividedPowers/ForMathlib/GradedRingQuot.lean)

State before:
R : Type u_1
inst✝⁹ : CommSemiring R
ι✝ : Type u_2
inst✝⁸ : DecidableEq ι✝
inst✝⁷ : AddCommMonoid ι✝
A✝ : Type u_3
inst✝⁶ : CommSemiring A✝
inst✝⁵ : DecidableEq A✝
inst✝⁴ : Algebra R A✝
𝒜 : ι✝ → Submodule R A✝
rel : A✝ → A✝ → Prop
A : Type u_4
inst✝³ : AddCommMonoid A
r : A → A → Prop
hr_zero : r 0 0
hr_add : ∀ {a b c d : A}, r a c → r b d → r (a + b) (c + d)
ι : Type u_5
inst✝² : DecidableEq ι
β : ι → Type u_6
inst✝¹ : (i : ι) → AddCommMonoid (β i)
inst✝ : (i : ι) → (y : β i) → Decidable (y ≠ 0)
h h' : (i : ι) → β i →+ A
f g : DFinsupp β
H : ∀ (i : ι), r ((h i) (f i)) ((h' i) (g i))
⊢ r (f.sum fun i y => (h i) y) (g.sum fun i y => (h' i) y)
Tactic:
rw [DFinsupp.sum_of_support_le (Finset.subset_union_left f.support g.support),
  DFinsupp.sum_of_support_le (Finset.subset_union_right f.support g.support)]
State after:
R : Type u_1
inst✝⁹ : CommSemiring R
ι✝ : Type u_2
inst✝⁸ : DecidableEq ι✝
inst✝⁷ : AddCommMonoid ι✝
A✝ : Type u_3
inst✝⁶ : CommSemiring A✝
inst✝⁵ : DecidableEq A✝
inst✝⁴ : Algebra R A✝
𝒜 : ι✝ → Submodule R A✝
rel : A✝ → A✝ → Prop
A : Type u_4
inst✝³ : AddCommMonoid A
r : A → A → Prop
hr_zero : r 0 0
hr_add : ∀ {a b c d : A}, r a c → r b d → r (a + b) (c + d)
ι : Type u_5
inst✝² : DecidableEq ι
β : ι → Type u_6
inst✝¹ : (i : ι) → AddCommMonoid (β i)
inst✝ : (i : ι) → (y : β i) → Decidable (y ≠ 0)
h h' : (i : ι) → β i →+ A
f g : DFinsupp β
H : ∀ (i : ι), r ((h i) (f i)) ((h' i) (g i))
⊢ r (∑ i ∈ f.support ∪ g.support, (h i) (f i)) (∑ i ∈ f.support ∪ g.support, (h' i) (g i))

State before:
R : Type u_1
inst✝⁹ : CommSemiring R
ι✝ : Type u_2
inst✝⁸ : DecidableEq ι✝
inst✝⁷ : AddCommMonoid ι✝
A✝ : Type u_3
inst✝⁶ : CommSemiring A✝
inst✝⁵ : DecidableEq A✝
inst✝⁴ : Algebra R A✝
𝒜 : ι✝ → Submodule R A✝
rel : A✝ → A✝ → Prop
A : Type u_4
inst✝³ : AddCommMonoid A
r : A → A → Prop
hr_zero : r 0 0
hr_add : ∀ {a b c d : A}, r a c → r b d → r (a + b) (c + d)
ι : Type u_5
inst✝² : DecidableEq ι
β : ι → Type u_6
inst✝¹ : (i : ι) → AddCommMonoid (β i)
inst✝ : (i : ι) → (y : β i) → Decidable (y ≠ 0)
h h' : (i : ι) → β i →+ A
f g : DFinsupp β
H : ∀ (i : ι), r ((h i) (f i)) ((h' i) (g i))
⊢ r (∑ i ∈ f.support ∪ g.support, (h i) (f i)) (∑ i ∈ f.support ∪ g.support, (h' i) (g i))
Tactic:
exact rel_of_sum_of_rel_add hr_zero hr_add (fun i _ => H i)
State after:
no goals