Theorem: rel_of_dsum_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)
f g : (i : ι) → β i
h : (i : ι) → β i →+ A
s : Finset ι
H : ∀ i ∈ s, r ((h i) (f i)) ((h i) (g i))
⊢ r (∑ i ∈ s, (h i) (f i)) (∑ i ∈ s, (h i) (g i))
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 ι
β : ι → Type u_6
inst✝ : (i : ι) → AddCommMonoid (β i)
f g : (i : ι) → β i
h : (i : ι) → β i →+ A
s : Finset ι
⊢ (∀ i ∈ s, r ((h i) (f i)) ((h i) (g i))) → r (∑ i ∈ s, (h i) (f i)) (∑ i ∈ s, (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)
f g : (i : ι) → β i
h : (i : ι) → β i →+ A
s : Finset ι
⊢ (∀ i ∈ s, r ((h i) (f i)) ((h i) (g i))) → r (∑ i ∈ s, (h i) (f i)) (∑ i ∈ s, (h i) (g i))
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 ι
β : ι → Type u_6
inst✝ : (i : ι) → AddCommMonoid (β i)
f g : (i : ι) → β i
h : (i : ι) → β i →+ A
⊢ (∀ i ∈ ∅, r ((h i) (f i)) ((h i) (g i))) → r (∑ i ∈ ∅, (h i) (f i)) (∑ i ∈ ∅, (h i) (g i))
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 ι
β : ι → Type u_6
inst✝ : (i : ι) → AddCommMonoid (β i)
f g : (i : ι) → β i
h : (i : ι) → β i →+ A
i : ι
s : Finset ι
hi : i ∉ s
hs : (∀ i ∈ s, r ((h i) (f i)) ((h i) (g i))) → r (∑ i ∈ s, (h i) (f i)) (∑ i ∈ s, (h i) (g i))
⊢ (∀ i_1 ∈ insert i s, r ((h i_1) (f i_1)) ((h i_1) (g i_1))) →
    r (∑ i ∈ insert i s, (h i) (f i)) (∑ i ∈ insert i s, (h i) (g i))
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 ι
β : ι → Type u_6
inst✝ : (i : ι) → AddCommMonoid (β i)
f g : (i : ι) → β i
h : (i : ι) → β i →+ A
i : ι
s : Finset ι
hi : i ∉ s
hs : (∀ i ∈ s, r ((h i) (f i)) ((h i) (g i))) → r (∑ i ∈ s, (h i) (f i)) (∑ i ∈ s, (h i) (g i))
H : ∀ i_1 ∈ insert i s, r ((h i_1) (f i_1)) ((h i_1) (g i_1))
⊢ r (∑ i ∈ insert i s, (h i) (f i)) (∑ i ∈ insert i s, (h i) (g i))

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 ι
β : ι → Type u_6
inst✝ : (i : ι) → AddCommMonoid (β i)
f g : (i : ι) → β i
h : (i : ι) → β i →+ A
i : ι
s : Finset ι
hi : i ∉ s
hs : (∀ i ∈ s, r ((h i) (f i)) ((h i) (g i))) → r (∑ i ∈ s, (h i) (f i)) (∑ i ∈ s, (h i) (g i))
H : ∀ i_1 ∈ insert i s, r ((h i_1) (f i_1)) ((h i_1) (g i_1))
⊢ r (∑ i ∈ insert i s, (h i) (f i)) (∑ i ∈ insert i s, (h i) (g i))
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 ι
β : ι → Type u_6
inst✝ : (i : ι) → AddCommMonoid (β i)
f g : (i : ι) → β i
h : (i : ι) → β i →+ A
i : ι
s : Finset ι
hi : i ∉ s
hs : (∀ i ∈ s, r ((h i) (f i)) ((h i) (g i))) → r (∑ i ∈ s, (h i) (f i)) (∑ i ∈ s, (h i) (g i))
H : ∀ i_1 ∈ insert i s, r ((h i_1) (f i_1)) ((h i_1) (g i_1))
⊢ r ((h i) (f i) + ∑ i ∈ s, (h i) (f i)) ((h i) (g i) + ∑ i ∈ s, (h i) (g i))

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 ι
β : ι → Type u_6
inst✝ : (i : ι) → AddCommMonoid (β i)
f g : (i : ι) → β i
h : (i : ι) → β i →+ A
i : ι
s : Finset ι
hi : i ∉ s
hs : (∀ i ∈ s, r ((h i) (f i)) ((h i) (g i))) → r (∑ i ∈ s, (h i) (f i)) (∑ i ∈ s, (h i) (g i))
H : ∀ i_1 ∈ insert i s, r ((h i_1) (f i_1)) ((h i_1) (g i_1))
⊢ r ((h i) (f i) + ∑ i ∈ s, (h i) (f i)) ((h i) (g i) + ∑ i ∈ s, (h i) (g i))
Tactic:
exact hr_add (H _ (Finset.mem_insert_self _ _))
  (hs (fun _ hi => H _ (Finset.mem_insert_of_mem hi)))
State after:
no goals