-- 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 ι
s : Finset ι
f g : ι → α
⊢ ∀ (a : ι) (s : Finset ι),
    (∀ x ∈ s, x < a) →
      ∏ 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:
clear s

Result:
ι : Type u_1
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : LinearOrder ι
f g : ι → α
⊢ ∀ (a : ι) (s : Finset ι),
    (∀ x ∈ s, x < a) →
      ∏ 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

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
⊢ 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

Tactic:
rw [add_comm]

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
⊢ 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

Proof state:
ι : Type u_1
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : LinearOrder ι
s : Finset ι
f g : ι → α
⊢ ∏ 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

Tactic:
refine Finset.induction_on_max s (by simp) ?_

Result:
ι : Type u_1
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : LinearOrder ι
s : Finset ι
f g : ι → α
⊢ ∀ (a : ι) (s : Finset ι),
    (∀ x ∈ s, x < a) →
      ∏ 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

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 : ι
hi : i ∈ s
⊢ a ∉ filter (fun j => i < j) s

Tactic:
exact mt (fun ha => (mem_filter.1 ha).1) ha'

Result:
no goals

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
⊢ ∀ x ∈ insert a s, ¬a < x

Tactic:
exact (forall_mem_insert _ _ _).2 ⟨lt_irrefl a, fun i hi => (ha i hi).not_lt⟩

Result:
no goals

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 : ι
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

Tactic:
rw [filter_insert, if_neg (ha i hi).not_lt, filter_insert, if_pos (ha i hi), prod_insert,
  mul_left_comm]

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
⊢ a ∉ filter (fun j => i < j) s

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
⊢ ∏ 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:
rw [prod_insert ha', prod_insert ha', sum_insert ha', filter_insert, if_neg (lt_irrefl a),
  filter_true_of_mem ha, ihs, add_mul, mul_add, mul_add, add_assoc]

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
⊢ 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)