-- Mathlib/Algebra/BigOperators/Ring/Finset.lean
theorem prod_add_ordered [LinearOrder ι] (s : Finset ι) (f g : ι → α) :
    ∏ i ∈ s, (f i + g i) =
      (∏ i ∈ s, f i) +
        ∑ i ∈ s, g i * (∏ j ∈ s with j < i, (f j + g j)) * ∏ j ∈ s with i < j, f j

Proof state:
ι : Type u_1
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : LinearOrder ι
f g : ι → α
a : ι
s : Finset ι
ha : ∀ x ∈ s, x < a
ihs :
  ∏ i ∈ s, (f i + g i) =
    ∏ i ∈ s, f i + ∑ i ∈ s, (g i * ∏ j ∈ filter (fun j => j < i) s, (f j + g j)) * ∏ j ∈ filter (fun j => i < j) s, f j
⊢ ∏ i ∈ insert a s, (f i + g i) =
    ∏ i ∈ insert a s, f i +
      ∑ i ∈ insert a s,
        (g i * ∏ j ∈ filter (fun j => j < i) (insert a s), (f j + g j)) *
          ∏ j ∈ filter (fun j => i < j) (insert a s), f j

Tactic:
have ha' : a ∉ s := fun ha' => lt_irrefl a (ha a ha')

Result:
ι : Type u_1
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : LinearOrder ι
f g : ι → α
a : ι
s : Finset ι
ha : ∀ x ∈ s, x < a
ihs :
  ∏ i ∈ s, (f i + g i) =
    ∏ i ∈ s, f i + ∑ i ∈ s, (g i * ∏ j ∈ filter (fun j => j < i) s, (f j + g j)) * ∏ j ∈ filter (fun j => i < j) s, f j
ha' : a ∉ s
⊢ ∏ i ∈ insert a s, (f i + g i) =
    ∏ i ∈ insert a s, f i +
      ∑ i ∈ insert a s,
        (g i * ∏ j ∈ filter (fun j => j < i) (insert a s), (f j + g j)) *
          ∏ j ∈ filter (fun j => i < j) (insert a s), f j

Proof state:
case e_a.e_a
ι : Type u_1
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : LinearOrder ι
f g : ι → α
a : ι
s : Finset ι
ha : ∀ x ∈ s, x < a
ihs :
  ∏ i ∈ s, (f i + g i) =
    ∏ i ∈ s, f i + ∑ i ∈ s, (g i * ∏ j ∈ filter (fun j => j < i) s, (f j + g j)) * ∏ j ∈ filter (fun j => i < j) s, f j
ha' : a ∉ s
⊢ ∑ i ∈ s, f a * ((g i * ∏ j ∈ filter (fun j => j < i) s, (f j + g j)) * ∏ j ∈ filter (fun j => i < j) s, f j) =
    ∑ x ∈ s,
      (g x * ∏ j ∈ filter (fun j => j < x) (insert a s), (f j + g j)) * ∏ j ∈ filter (fun j => x < j) (insert a s), f j

Tactic:
refine sum_congr rfl fun i hi => ?_

Result:
case e_a.e_a
ι : Type u_1
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : LinearOrder ι
f g : ι → α
a : ι
s : Finset ι
ha : ∀ x ∈ s, x < a
ihs :
  ∏ i ∈ s, (f i + g i) =
    ∏ i ∈ s, f i + ∑ i ∈ s, (g i * ∏ j ∈ filter (fun j => j < i) s, (f j + g j)) * ∏ j ∈ filter (fun j => i < j) s, f j
ha' : a ∉ s
i : ι
hi : i ∈ s
⊢ f a * ((g i * ∏ j ∈ filter (fun j => j < i) s, (f j + g j)) * ∏ j ∈ filter (fun j => i < j) s, f j) =
    (g i * ∏ j ∈ filter (fun j => j < i) (insert a s), (f j + g j)) * ∏ j ∈ filter (fun j => i < j) (insert a s), f j

Proof state:
case e_a
ι : Type u_1
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : LinearOrder ι
f g : ι → α
a : ι
s : Finset ι
ha : ∀ x ∈ s, x < a
ihs :
  ∏ i ∈ s, (f i + g i) =
    ∏ i ∈ s, f i + ∑ i ∈ s, (g i * ∏ j ∈ filter (fun j => j < i) s, (f j + g j)) * ∏ j ∈ filter (fun j => i < j) s, f j
ha' : a ∉ s
⊢ g a * ∏ i ∈ s, f i +
        g a * ∑ i ∈ s, (g i * ∏ j ∈ filter (fun j => j < i) s, (f j + g j)) * ∏ j ∈ filter (fun j => i < j) s, f j +
      f a * ∑ i ∈ s, (g i * ∏ j ∈ filter (fun j => j < i) s, (f j + g j)) * ∏ j ∈ filter (fun j => i < j) s, f j =
    (g a * ∏ i ∈ s, f i +
          g a * ∑ i ∈ s, (g i * ∏ j ∈ filter (fun j => j < i) s, (f j + g j)) * ∏ j ∈ filter (fun j => i < j) s, f j) *
        ∏ j ∈ filter (fun j => a < j) (insert a s), f j +
      ∑ x ∈ s,
        (g x * ∏ j ∈ filter (fun j => j < x) (insert a s), (f j + g j)) *
          ∏ j ∈ filter (fun j => x < j) (insert a s), f j

Tactic:
congr 1

Result:
case e_a.e_a
ι : Type u_1
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : LinearOrder ι
f g : ι → α
a : ι
s : Finset ι
ha : ∀ x ∈ s, x < a
ihs :
  ∏ i ∈ s, (f i + g i) =
    ∏ i ∈ s, f i + ∑ i ∈ s, (g i * ∏ j ∈ filter (fun j => j < i) s, (f j + g j)) * ∏ j ∈ filter (fun j => i < j) s, f j
ha' : a ∉ s
⊢ g a * ∏ i ∈ s, f i +
      g a * ∑ i ∈ s, (g i * ∏ j ∈ filter (fun j => j < i) s, (f j + g j)) * ∏ j ∈ filter (fun j => i < j) s, f j =
    (g a * ∏ i ∈ s, f i +
        g a * ∑ i ∈ s, (g i * ∏ j ∈ filter (fun j => j < i) s, (f j + g j)) * ∏ j ∈ filter (fun j => i < j) s, f j) *
      ∏ j ∈ filter (fun j => a < j) (insert a s), f j

case e_a.e_a
ι : Type u_1
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : LinearOrder ι
f g : ι → α
a : ι
s : Finset ι
ha : ∀ x ∈ s, x < a
ihs :
  ∏ i ∈ s, (f i + g i) =
    ∏ i ∈ s, f i + ∑ i ∈ s, (g i * ∏ j ∈ filter (fun j => j < i) s, (f j + g j)) * ∏ j ∈ filter (fun j => i < j) s, f j
ha' : a ∉ s
⊢ f a * ∑ i ∈ s, (g i * ∏ j ∈ filter (fun j => j < i) s, (f j + g j)) * ∏ j ∈ filter (fun j => i < j) s, f j =
    ∑ x ∈ s,
      (g x * ∏ j ∈ filter (fun j => j < x) (insert a s), (f j + g j)) * ∏ j ∈ filter (fun j => x < j) (insert a s), f j

Proof state:
ι : Type u_1
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : LinearOrder ι
s : Finset ι
f g : ι → α
⊢ ∏ i ∈ ∅, (f i + g i) =
    ∏ i ∈ ∅, f i + ∑ i ∈ ∅, (g i * ∏ j ∈ filter (fun j => j < i) ∅, (f j + g j)) * ∏ j ∈ filter (fun j => i < j) ∅, f j

Tactic:
simp

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : LinearOrder ι
f g : ι → α
a : ι
s : Finset ι
ha : ∀ x ∈ s, x < a
ihs :
  ∏ i ∈ s, (f i + g i) =
    ∏ i ∈ s, f i + ∑ i ∈ s, (g i * ∏ j ∈ filter (fun j => j < i) s, (f j + g j)) * ∏ j ∈ filter (fun j => i < j) s, f j
ha' : a ∉ s
⊢ f a * ∏ i ∈ s, f i +
      (f a * ∑ i ∈ s, (g i * ∏ j ∈ filter (fun j => j < i) s, (f j + g j)) * ∏ j ∈ filter (fun j => i < j) s, f j +
        (g a * ∏ i ∈ s, f i +
          g a * ∑ i ∈ s, (g i * ∏ j ∈ filter (fun j => j < i) s, (f j + g j)) * ∏ j ∈ filter (fun j => i < j) s, f j)) =
    f a * ∏ x ∈ s, f x +
      ((g a * ∏ i ∈ s, f i +
            g a *
              ∑ i ∈ s, (g i * ∏ j ∈ filter (fun j => j < i) s, (f j + g j)) * ∏ j ∈ filter (fun j => i < j) s, f j) *
          ∏ j ∈ filter (fun j => a < j) (insert a s), f j +
        ∑ x ∈ s,
          (g x * ∏ j ∈ filter (fun j => j < x) (insert a s), (f j + g j)) *
            ∏ j ∈ filter (fun j => x < j) (insert a s), f j)

Tactic:
congr 1

Result:
case e_a
ι : Type u_1
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : LinearOrder ι
f g : ι → α
a : ι
s : Finset ι
ha : ∀ x ∈ s, x < a
ihs :
  ∏ i ∈ s, (f i + g i) =
    ∏ i ∈ s, f i + ∑ i ∈ s, (g i * ∏ j ∈ filter (fun j => j < i) s, (f j + g j)) * ∏ j ∈ filter (fun j => i < j) s, f j
ha' : a ∉ s
⊢ f a * ∑ i ∈ s, (g i * ∏ j ∈ filter (fun j => j < i) s, (f j + g j)) * ∏ j ∈ filter (fun j => i < j) s, f j +
      (g a * ∏ i ∈ s, f i +
        g a * ∑ i ∈ s, (g i * ∏ j ∈ filter (fun j => j < i) s, (f j + g j)) * ∏ j ∈ filter (fun j => i < j) s, f j) =
    (g a * ∏ i ∈ s, f i +
          g a * ∑ i ∈ s, (g i * ∏ j ∈ filter (fun j => j < i) s, (f j + g j)) * ∏ j ∈ filter (fun j => i < j) s, f j) *
        ∏ j ∈ filter (fun j => a < j) (insert a s), f j +
      ∑ x ∈ s,
        (g x * ∏ j ∈ filter (fun j => j < x) (insert a s), (f j + g j)) *
          ∏ j ∈ filter (fun j => x < j) (insert a s), f j

Proof state:
case e_a.e_a
ι : Type u_1
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : LinearOrder ι
f g : ι → α
a : ι
s : Finset ι
ha : ∀ x ∈ s, x < a
ihs :
  ∏ i ∈ s, (f i + g i) =
    ∏ i ∈ s, f i + ∑ i ∈ s, (g i * ∏ j ∈ filter (fun j => j < i) s, (f j + g j)) * ∏ j ∈ filter (fun j => i < j) s, f j
ha' : a ∉ s
⊢ f a * ∑ i ∈ s, (g i * ∏ j ∈ filter (fun j => j < i) s, (f j + g j)) * ∏ j ∈ filter (fun j => i < j) s, f j =
    ∑ x ∈ s,
      (g x * ∏ j ∈ filter (fun j => j < x) (insert a s), (f j + g j)) * ∏ j ∈ filter (fun j => x < j) (insert a s), f j

Tactic:
rw [mul_sum]

Result:
case e_a.e_a
ι : Type u_1
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : LinearOrder ι
f g : ι → α
a : ι
s : Finset ι
ha : ∀ x ∈ s, x < a
ihs :
  ∏ i ∈ s, (f i + g i) =
    ∏ i ∈ s, f i + ∑ i ∈ s, (g i * ∏ j ∈ filter (fun j => j < i) s, (f j + g j)) * ∏ j ∈ filter (fun j => i < j) s, f j
ha' : a ∉ s
⊢ ∑ i ∈ s, f a * ((g i * ∏ j ∈ filter (fun j => j < i) s, (f j + g j)) * ∏ j ∈ filter (fun j => i < j) s, f j) =
    ∑ x ∈ s,
      (g x * ∏ j ∈ filter (fun j => j < x) (insert a s), (f j + g j)) * ∏ j ∈ filter (fun j => x < j) (insert a s), f j