Theorem: rel_of_finsupp_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 ι
f g : ι →₀ A
H : ∀ (i : ι), r (f i) (g i)
⊢ r (f.sum fun x x => x) (g.sum fun x x => x)
Tactic:
rw [Finsupp.sum_of_support_subset f (Finset.subset_union_left _ g.support),
  Finsupp.sum_of_support_subset g (Finset.subset_union_right f.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 ι
f g : ι →₀ A
H : ∀ (i : ι), r (f i) (g i)
⊢ r (∑ x ∈ f.support ∪ g.support, f x) (∑ x ∈ f.support ∪ g.support, g x)

case h
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 ι
f g : ι →₀ A
H : ∀ (i : ι), r (f i) (g i)
⊢ ∀ i ∈ f.support ∪ g.support, 0 = 0

case h
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 ι
f g : ι →₀ A
H : ∀ (i : ι), r (f i) (g i)
⊢ ∀ i ∈ f.support ∪ g.support, 0 = 0

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 ι
f g : ι →₀ A
H : ∀ (i : ι), r (f i) (g i)
⊢ r (∑ x ∈ f.support ∪ g.support, f x) (∑ x ∈ f.support ∪ g.support, g x)

case h
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 ι
f g : ι →₀ A
H : ∀ (i : ι), r (f i) (g i)
⊢ ∀ i ∈ f.support ∪ g.support, 0 = 0

case h
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 ι
f g : ι →₀ A
H : ∀ (i : ι), r (f i) (g i)
⊢ ∀ i ∈ f.support ∪ g.support, 0 = 0
Tactic:
exact rel_of_sum_of_rel_add hr_zero hr_add (fun i _ =>  H i)
State after:
case h
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 ι
f g : ι →₀ A
H : ∀ (i : ι), r (f i) (g i)
⊢ ∀ i ∈ f.support ∪ g.support, 0 = 0

case h
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 ι
f g : ι →₀ A
H : ∀ (i : ι), r (f i) (g i)
⊢ ∀ i ∈ f.support ∪ g.support, 0 = 0

State before:
case h
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 ι
f g : ι →₀ A
H : ∀ (i : ι), r (f i) (g i)
⊢ ∀ i ∈ f.support ∪ g.support, 0 = 0

case h
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 ι
f g : ι →₀ A
H : ∀ (i : ι), r (f i) (g i)
⊢ ∀ i ∈ f.support ∪ g.support, 0 = 0
Tactic:
all_goals { intro _ _ ; rfl }
State after:
no goals

State before:
case h
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 ι
f g : ι →₀ A
H : ∀ (i : ι), r (f i) (g i)
⊢ ∀ i ∈ f.support ∪ g.support, 0 = 0
Tactic:
intro _ _
State after:
case h
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 ι
f g : ι →₀ A
H : ∀ (i : ι), r (f i) (g i)
i✝ : ι
a✝ : i✝ ∈ f.support ∪ g.support
⊢ 0 = 0

State before:
case h
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 ι
f g : ι →₀ A
H : ∀ (i : ι), r (f i) (g i)
i✝ : ι
a✝ : i✝ ∈ f.support ∪ g.support
⊢ 0 = 0
Tactic:
rfl
State after:
no goals