Theorem: rel_of_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
s : Finset ι
H : ∀ i ∈ s, r (f i) (g i)
⊢ r (s.sum f) (s.sum g)
Tactic:
revert H
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
s : Finset ι
⊢ (∀ i ∈ s, r (f i) (g i)) → r (s.sum f) (s.sum g)

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
s : Finset ι
⊢ (∀ i ∈ s, r (f i) (g i)) → r (s.sum f) (s.sum g)
Tactic:
induction s using Finset.induction_on with
| empty => exact fun _ =>  hr_zero
| @insert i s hi hs =>
  intro H
  simp only [Finset.sum_insert hi]
  exact hr_add (H _ (Finset.mem_insert_self _ _))
    (hs (fun _ hi => H _ (Finset.mem_insert_of_mem hi)))
State after:
no goals

State before:
case empty
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
⊢ (∀ i ∈ ∅, r (f i) (g i)) → r (∅.sum f) (∅.sum g)
Tactic:
exact fun _ =>  hr_zero
State after:
no goals

State before:
case insert
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
i : ι
s : Finset ι
hi : i ∉ s
hs : (∀ i ∈ s, r (f i) (g i)) → r (s.sum f) (s.sum g)
⊢ (∀ i_1 ∈ insert i s, r (f i_1) (g i_1)) → r ((insert i s).sum f) ((insert i s).sum g)
Tactic:
intro H
State after:
case insert
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
i : ι
s : Finset ι
hi : i ∉ s
hs : (∀ i ∈ s, r (f i) (g i)) → r (s.sum f) (s.sum g)
H : ∀ i_1 ∈ insert i s, r (f i_1) (g i_1)
⊢ r ((insert i s).sum f) ((insert i s).sum g)

State before:
case insert
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
i : ι
s : Finset ι
hi : i ∉ s
hs : (∀ i ∈ s, r (f i) (g i)) → r (s.sum f) (s.sum g)
H : ∀ i_1 ∈ insert i s, r (f i_1) (g i_1)
⊢ r ((insert i s).sum f) ((insert i s).sum g)
Tactic:
simp only [Finset.sum_insert hi]
State after:
case insert
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
i : ι
s : Finset ι
hi : i ∉ s
hs : (∀ i ∈ s, r (f i) (g i)) → r (s.sum f) (s.sum g)
H : ∀ i_1 ∈ insert i s, r (f i_1) (g i_1)
⊢ r (f i + ∑ x ∈ s, f x) (g i + ∑ x ∈ s, g x)

State before:
case insert
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
i : ι
s : Finset ι
hi : i ∉ s
hs : (∀ i ∈ s, r (f i) (g i)) → r (s.sum f) (s.sum g)
H : ∀ i_1 ∈ insert i s, r (f i_1) (g i_1)
⊢ r (f i + ∑ x ∈ s, f x) (g i + ∑ x ∈ s, g x)
Tactic:
exact hr_add (H _ (Finset.mem_insert_self _ _))
  (hs (fun _ hi => H _ (Finset.mem_insert_of_mem hi)))
State after:
no goals