Theorem: RingConGen.Rel.sum (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
α : Type u_4
inst✝¹ : Ring α
r : RingCon α
ι : Type u_5
inst✝ : DecidableEq ι
a b : ι → α
s : Finset ι
hs : ∀ i ∈ s, r (a i) (b i)
⊢ RingConGen.Rel (⇑r) (s.sum a) (s.sum b)
Tactic:
revert hs
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
α : Type u_4
inst✝¹ : Ring α
r : RingCon α
ι : Type u_5
inst✝ : DecidableEq ι
a b : ι → α
s : Finset ι
⊢ (∀ i ∈ s, r (a i) (b i)) → RingConGen.Rel (⇑r) (s.sum a) (s.sum b)

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
α : Type u_4
inst✝¹ : Ring α
r : RingCon α
ι : Type u_5
inst✝ : DecidableEq ι
a b : ι → α
s : Finset ι
⊢ (∀ i ∈ s, r (a i) (b i)) → RingConGen.Rel (⇑r) (s.sum a) (s.sum b)
Tactic:
induction' s using Finset.induction_on with j t hj ht hjt
State after:
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
α : Type u_4
inst✝¹ : Ring α
r : RingCon α
ι : Type u_5
inst✝ : DecidableEq ι
a b : ι → α
⊢ (∀ i ∈ ∅, r (a i) (b i)) → RingConGen.Rel (⇑r) (∅.sum a) (∅.sum b)

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
α : Type u_4
inst✝¹ : Ring α
r : RingCon α
ι : Type u_5
inst✝ : DecidableEq ι
a b : ι → α
j : ι
t : Finset ι
hj : j ∉ t
ht : (∀ i ∈ t, r (a i) (b i)) → RingConGen.Rel (⇑r) (t.sum a) (t.sum b)
⊢ (∀ i ∈ insert j t, r (a i) (b i)) → RingConGen.Rel (⇑r) ((insert j t).sum a) ((insert j t).sum b)

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
α : Type u_4
inst✝¹ : Ring α
r : RingCon α
ι : Type u_5
inst✝ : DecidableEq ι
a b : ι → α
⊢ (∀ i ∈ ∅, r (a i) (b i)) → RingConGen.Rel (⇑r) (∅.sum a) (∅.sum b)

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
α : Type u_4
inst✝¹ : Ring α
r : RingCon α
ι : Type u_5
inst✝ : DecidableEq ι
a b : ι → α
j : ι
t : Finset ι
hj : j ∉ t
ht : (∀ i ∈ t, r (a i) (b i)) → RingConGen.Rel (⇑r) (t.sum a) (t.sum b)
⊢ (∀ i ∈ insert j t, r (a i) (b i)) → RingConGen.Rel (⇑r) ((insert j t).sum a) ((insert j t).sum b)
Tactic:
. exact fun _ =>  RingConGen.Rel.refl _
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
α : Type u_4
inst✝¹ : Ring α
r : RingCon α
ι : Type u_5
inst✝ : DecidableEq ι
a b : ι → α
j : ι
t : Finset ι
hj : j ∉ t
ht : (∀ i ∈ t, r (a i) (b i)) → RingConGen.Rel (⇑r) (t.sum a) (t.sum b)
⊢ (∀ i ∈ insert j t, r (a i) (b i)) → RingConGen.Rel (⇑r) ((insert j t).sum a) ((insert j t).sum b)

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
α : Type u_4
inst✝¹ : Ring α
r : RingCon α
ι : Type u_5
inst✝ : DecidableEq ι
a b : ι → α
j : ι
t : Finset ι
hj : j ∉ t
ht : (∀ i ∈ t, r (a i) (b i)) → RingConGen.Rel (⇑r) (t.sum a) (t.sum b)
⊢ (∀ i ∈ insert j t, r (a i) (b i)) → RingConGen.Rel (⇑r) ((insert j t).sum a) ((insert j t).sum b)
Tactic:
. intro hs
  simp only [Finset.sum_insert hj]
  apply RingConGen.Rel.add
  . exact RingConGen.Rel.of _ _ (hs j (Finset.mem_insert_self j t))
  . exact ht (fun i hi =>  hs i (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
α : Type u_4
inst✝¹ : Ring α
r : RingCon α
ι : Type u_5
inst✝ : DecidableEq ι
a b : ι → α
⊢ (∀ i ∈ ∅, r (a i) (b i)) → RingConGen.Rel (⇑r) (∅.sum a) (∅.sum b)
Tactic:
exact fun _ =>  RingConGen.Rel.refl _
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
α : Type u_4
inst✝¹ : Ring α
r : RingCon α
ι : Type u_5
inst✝ : DecidableEq ι
a b : ι → α
j : ι
t : Finset ι
hj : j ∉ t
ht : (∀ i ∈ t, r (a i) (b i)) → RingConGen.Rel (⇑r) (t.sum a) (t.sum b)
⊢ (∀ i ∈ insert j t, r (a i) (b i)) → RingConGen.Rel (⇑r) ((insert j t).sum a) ((insert j t).sum b)
Tactic:
intro hs
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
α : Type u_4
inst✝¹ : Ring α
r : RingCon α
ι : Type u_5
inst✝ : DecidableEq ι
a b : ι → α
j : ι
t : Finset ι
hj : j ∉ t
ht : (∀ i ∈ t, r (a i) (b i)) → RingConGen.Rel (⇑r) (t.sum a) (t.sum b)
hs : ∀ i ∈ insert j t, r (a i) (b i)
⊢ RingConGen.Rel (⇑r) ((insert j t).sum a) ((insert j t).sum b)

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
α : Type u_4
inst✝¹ : Ring α
r : RingCon α
ι : Type u_5
inst✝ : DecidableEq ι
a b : ι → α
j : ι
t : Finset ι
hj : j ∉ t
ht : (∀ i ∈ t, r (a i) (b i)) → RingConGen.Rel (⇑r) (t.sum a) (t.sum b)
hs : ∀ i ∈ insert j t, r (a i) (b i)
⊢ RingConGen.Rel (⇑r) ((insert j t).sum a) ((insert j t).sum b)
Tactic:
simp only [Finset.sum_insert hj]
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
α : Type u_4
inst✝¹ : Ring α
r : RingCon α
ι : Type u_5
inst✝ : DecidableEq ι
a b : ι → α
j : ι
t : Finset ι
hj : j ∉ t
ht : (∀ i ∈ t, r (a i) (b i)) → RingConGen.Rel (⇑r) (t.sum a) (t.sum b)
hs : ∀ i ∈ insert j t, r (a i) (b i)
⊢ RingConGen.Rel (⇑r) (a j + ∑ x ∈ t, a x) (b j + ∑ x ∈ t, b 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
α : Type u_4
inst✝¹ : Ring α
r : RingCon α
ι : Type u_5
inst✝ : DecidableEq ι
a b : ι → α
j : ι
t : Finset ι
hj : j ∉ t
ht : (∀ i ∈ t, r (a i) (b i)) → RingConGen.Rel (⇑r) (t.sum a) (t.sum b)
hs : ∀ i ∈ insert j t, r (a i) (b i)
⊢ RingConGen.Rel (⇑r) (a j + ∑ x ∈ t, a x) (b j + ∑ x ∈ t, b x)
Tactic:
apply RingConGen.Rel.add
State after:
case insert.a
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
α : Type u_4
inst✝¹ : Ring α
r : RingCon α
ι : Type u_5
inst✝ : DecidableEq ι
a b : ι → α
j : ι
t : Finset ι
hj : j ∉ t
ht : (∀ i ∈ t, r (a i) (b i)) → RingConGen.Rel (⇑r) (t.sum a) (t.sum b)
hs : ∀ i ∈ insert j t, r (a i) (b i)
⊢ RingConGen.Rel (⇑r) (a j) (b j)

case insert.a
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
α : Type u_4
inst✝¹ : Ring α
r : RingCon α
ι : Type u_5
inst✝ : DecidableEq ι
a b : ι → α
j : ι
t : Finset ι
hj : j ∉ t
ht : (∀ i ∈ t, r (a i) (b i)) → RingConGen.Rel (⇑r) (t.sum a) (t.sum b)
hs : ∀ i ∈ insert j t, r (a i) (b i)
⊢ RingConGen.Rel (⇑r) (∑ x ∈ t, a x) (∑ x ∈ t, b x)

State before:
case insert.a
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
α : Type u_4
inst✝¹ : Ring α
r : RingCon α
ι : Type u_5
inst✝ : DecidableEq ι
a b : ι → α
j : ι
t : Finset ι
hj : j ∉ t
ht : (∀ i ∈ t, r (a i) (b i)) → RingConGen.Rel (⇑r) (t.sum a) (t.sum b)
hs : ∀ i ∈ insert j t, r (a i) (b i)
⊢ RingConGen.Rel (⇑r) (a j) (b j)

case insert.a
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
α : Type u_4
inst✝¹ : Ring α
r : RingCon α
ι : Type u_5
inst✝ : DecidableEq ι
a b : ι → α
j : ι
t : Finset ι
hj : j ∉ t
ht : (∀ i ∈ t, r (a i) (b i)) → RingConGen.Rel (⇑r) (t.sum a) (t.sum b)
hs : ∀ i ∈ insert j t, r (a i) (b i)
⊢ RingConGen.Rel (⇑r) (∑ x ∈ t, a x) (∑ x ∈ t, b x)
Tactic:
. exact RingConGen.Rel.of _ _ (hs j (Finset.mem_insert_self j t))
State after:
case insert.a
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
α : Type u_4
inst✝¹ : Ring α
r : RingCon α
ι : Type u_5
inst✝ : DecidableEq ι
a b : ι → α
j : ι
t : Finset ι
hj : j ∉ t
ht : (∀ i ∈ t, r (a i) (b i)) → RingConGen.Rel (⇑r) (t.sum a) (t.sum b)
hs : ∀ i ∈ insert j t, r (a i) (b i)
⊢ RingConGen.Rel (⇑r) (∑ x ∈ t, a x) (∑ x ∈ t, b x)

State before:
case insert.a
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
α : Type u_4
inst✝¹ : Ring α
r : RingCon α
ι : Type u_5
inst✝ : DecidableEq ι
a b : ι → α
j : ι
t : Finset ι
hj : j ∉ t
ht : (∀ i ∈ t, r (a i) (b i)) → RingConGen.Rel (⇑r) (t.sum a) (t.sum b)
hs : ∀ i ∈ insert j t, r (a i) (b i)
⊢ RingConGen.Rel (⇑r) (∑ x ∈ t, a x) (∑ x ∈ t, b x)
Tactic:
. exact ht (fun i hi =>  hs i (Finset.mem_insert_of_mem hi))
State after:
no goals

State before:
case insert.a
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
α : Type u_4
inst✝¹ : Ring α
r : RingCon α
ι : Type u_5
inst✝ : DecidableEq ι
a b : ι → α
j : ι
t : Finset ι
hj : j ∉ t
ht : (∀ i ∈ t, r (a i) (b i)) → RingConGen.Rel (⇑r) (t.sum a) (t.sum b)
hs : ∀ i ∈ insert j t, r (a i) (b i)
⊢ RingConGen.Rel (⇑r) (a j) (b j)
Tactic:
exact RingConGen.Rel.of _ _ (hs j (Finset.mem_insert_self j t))
State after:
no goals

State before:
case insert.a
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
α : Type u_4
inst✝¹ : Ring α
r : RingCon α
ι : Type u_5
inst✝ : DecidableEq ι
a b : ι → α
j : ι
t : Finset ι
hj : j ∉ t
ht : (∀ i ∈ t, r (a i) (b i)) → RingConGen.Rel (⇑r) (t.sum a) (t.sum b)
hs : ∀ i ∈ insert j t, r (a i) (b i)
⊢ RingConGen.Rel (⇑r) (∑ x ∈ t, a x) (∑ x ∈ t, b x)
Tactic:
exact ht (fun i hi =>  hs i (Finset.mem_insert_of_mem hi))
State after:
no goals