awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
inst_1 : DecidableEq ι
f g : ι → R
s : Finset ι
simp_rw : ∀ (a : Finset ι) (ha : a ⊆ s) (a_1 : ι), (a_1 ∈ s ∧ ∃ (_ : a_1 ∈ s), a_1 ∈ a) ↔ a_1 ∈ a
⊢ ∀ (a : Finset ι) (ha : a ∈ s.powerset),
    (fun (f : (a : ι) → a ∈ s → Prop)
            (x :
              Membership.mem (γ := Finset ((a : ι) → a ∈ s → Prop))
                (s.pi (β := fun (a : ι) ↦ Prop) fun (x : ι) ↦ {True, False}) f) ↦
          {a ∈ s | ∃ (h : a ∈ s), f a h})
        ((fun (t : Finset ι) (x : t ∈ s.powerset) (a : ι) (x_1 : a ∈ s) ↦ a ∈ t) a ha) ⋯ =
      a

Tactic:
simp_rw [Finset.ext_iff, mem_filter, mem_powerset]

Premises used: Finset.ext_iff, Finset.mem_powerset, Finset.mem_filter
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
inst_1 : DecidableEq ι
f g : ι → R
s : Finset ι
tauto tauto₁ tauto₂ tauto₃ tauto₄ : ∀ a ⊆ s, ∀ (a_1 : ι), (a_1 ∈ s ∧ ∃ (_ : a_1 ∈ s), a_1 ∈ a) ↔ a_1 ∈ a
mp : ∀ a ⊆ s, ∀ (a_1 : ι), (a_1 ∈ s ∧ ∃ (_ : a_1 ∈ s), a_1 ∈ a) → a_1 ∈ a
mpr : ∀ a ⊆ s, ∀ a_1 ∈ a, a_1 ∈ s ∧ ∃ (_ : a_1 ∈ s), a_1 ∈ a
mp₁ mp₂ mp₃ : ∀ a ⊆ s, ∀ a_1 ∈ s, a_1 ∈ s → a_1 ∈ a → a_1 ∈ a
mpr₁ mpr₂ : ∀ a ⊆ s, ∀ a_1 ∈ a, a_1 ∈ s ∧ ∃ (_ : a_1 ∈ s), a_1 ∈ a
mpr₃ : ∀ a ⊆ s, ∀ a_1 ∈ a, a_1 ∈ s
mpr₄ : ∀ a ⊆ s, ∀ a_1 ∈ a, ∃ (_ : a_1 ∈ s), a_1 ∈ a
mpr₅ mpr₆ mpr₇ : ∀ a ⊆ s, ∀ a_1 ∈ a, a_1 ∈ s
mpr₈ mpr₉ mpr₁₀ : ∀ a ⊆ s, ∀ a_1 ∈ a, ∃ (_ : a_1 ∈ s), a_1 ∈ a
mpr₁₁ mpr₁₂ : ∀ a ⊆ s, ∀ a_1 ∈ a, a_1 ∈ s
mpr₁₃ mpr₁₄ : ∀ a ⊆ s, ∀ a_1 ∈ a, ∃ (_ : a_1 ∈ s), a_1 ∈ a
⊢ ∀ (a : Finset ι) (ha : a ⊆ s) (a_1 : ι), (a_1 ∈ s ∧ ∃ (_ : a_1 ∈ s), a_1 ∈ a) ↔ a_1 ∈ a

Tactic:
tauto
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
inst_1 : DecidableEq ι
f g : ι → R
s : Finset ι
a : (a : ι) → a ∈ s → Prop
h : Membership.mem (γ := Finset ((a : ι) → a ∈ s → Prop)) (s.pi (β := fun (a : ι) ↦ Prop) fun (x : ι) ↦ {True, False}) a
simp :
  HMul.hMul (α := R) (∏ x ∈ s with ∃ (h : x ∈ s), a x ⋯, f x) (∏ x ∈ s with ∃ (h : x ∈ s), ¬a x ⋯, g x) =
    HMul.hMul (α := R) (∏ x ∈ s with ∃ (h : x ∈ s), a x h, f x) (∏ x ∈ s \ {a_1 ∈ s | ∃ (h : a_1 ∈ s), a a_1 h}, g x)
⊢ (∏ a_1 ∈ s.attach, if a (↑a_1 : ι) ⋯ then f (↑a_1 : ι) else g (↑a_1 : ι)) =
    HMul.hMul (α := R)
      (∏
        a ∈
          (fun (f : (a : ι) → a ∈ s → Prop)
                (x :
                  Membership.mem (γ := Finset ((a : ι) → a ∈ s → Prop))
                    (s.pi (β := fun (a : ι) ↦ Prop) fun (x : ι) ↦ {True, False}) f) ↦
              {a ∈ s | ∃ (h : a ∈ s), f a h})
            a h,
        f a)
      (∏
        a ∈
          s \
            (fun (f : (a : ι) → a ∈ s → Prop)
                  (x :
                    Membership.mem (γ := Finset ((a : ι) → a ∈ s → Prop))
                      (s.pi (β := fun (a : ι) ↦ Prop) fun (x : ι) ↦ {True, False}) f) ↦
                {a ∈ s | ∃ (h : a ∈ s), f a h})
              a h,
        g a)

Tactic:
simp only [prod_ite, filter_attach', prod_map, Function.Embedding.coeFn_mk,
            Subtype.map_coe, id_eq, prod_attach]

Premises used: Finset.prod_ite, Function.Embedding.coeFn_mk, Finset.prod_attach, Finset.prod_map, Finset.filter_attach', Subtype.map_coe, id_eq
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
inst_1 : DecidableEq ι
f g : ι → R
s : Finset ι
a : (a : ι) → a ∈ s → Prop
h : Membership.mem (γ := Finset ((a : ι) → a ∈ s → Prop)) (s.pi (β := fun (a : ι) ↦ Prop) fun (x : ι) ↦ {True, False}) a
e_a : ∀ (x : ι), x ∈ {x ∈ s | ∃ (h : x ∈ s), ¬a x ⋯} ↔ x ∈ s \ {a_1 ∈ s | ∃ (h : a_1 ∈ s), a a_1 h}
⊢ HMul.hMul (α := R) (∏ x ∈ s with ∃ (h : x ∈ s), a x ⋯, f x) (∏ x ∈ s with ∃ (h : x ∈ s), ¬a x ⋯, g x) =
    HMul.hMul (α := R) (∏ x ∈ s with ∃ (h : x ∈ s), a x h, f x) (∏ x ∈ s \ {a_1 ∈ s | ∃ (h : a_1 ∈ s), a a_1 h}, g x)

Tactic:
congr 2 with x
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
inst_1 : DecidableEq ι
f g : ι → R
s : Finset ι
a : (a : ι) → a ∈ s → Prop
h : Membership.mem (γ := Finset ((a : ι) → a ∈ s → Prop)) (s.pi (β := fun (a : ι) ↦ Prop) fun (x : ι) ↦ {True, False}) a
x : ι
e_a : x ∈ s → ((∃ (h : x ∈ s), ¬a x ⋯) ↔ x ∈ s → ∀ (x_1 : x ∈ s), ¬a x x_1)
⊢ x ∈ {x ∈ s | ∃ (h : x ∈ s), ¬a x ⋯} ↔ x ∈ s \ {a_1 ∈ s | ∃ (h : a_1 ∈ s), a a_1 h}

Tactic:
simp only [mem_filter, mem_sdiff, not_and, not_exists, and_congr_right_iff]

Premises used: not_exists, and_congr_right_iff, Finset.mem_sdiff, Finset.mem_filter, not_and
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
inst_1 : DecidableEq ι
f g : ι → R
s : Finset ι
a : (a : ι) → a ∈ s → Prop
h : Membership.mem (γ := Finset ((a : ι) → a ∈ s → Prop)) (s.pi (β := fun (a : ι) ↦ Prop) fun (x : ι) ↦ {True, False}) a
x : ι
e_a e_a₁ : x ∈ s → ((∃ (h : x ∈ s), ¬a x ⋯) ↔ x ∈ s → ∀ (x_1 : x ∈ s), ¬a x x_1)
e_a₂ : x ∈ s → (∃ (h : x ∈ s), ¬a x ⋯) → x ∈ s → ∀ (x_1 : x ∈ s), ¬a x x_1
e_a₃ : x ∈ s → (x ∈ s → ∀ (x_1 : x ∈ s), ¬a x x_1) → ∃ (h : x ∈ s), ¬a x ⋯
e_a₄ e_a₅ e_a₆ : x ∈ s → ∀ (w : x ∈ s), ¬a x ⋯ → x ∈ s → ∀ (x_1 : x ∈ s), ¬a x x_1
e_a₇ : x ∈ s → x ∉ s → ∃ (h : x ∈ s), ¬a x ⋯
e_a₈ e_a₉ e_a₁₀ : x ∈ s → (∀ (x_1 : x ∈ s), ¬a x x_1) → ∃ (h : x ∈ s), ¬a x ⋯
e_a₁₁ e_a₁₂ : x ∈ s → ∀ (w : x ∈ s), ¬a x ⋯ → x ∈ s → ∀ (x_1 : x ∈ s), ¬a x x_1
e_a₁₃ : x ∈ s → ∀ (w : x ∈ s), ¬a x ⋯ → x ∈ s → ∀ (x_1 : x ∈ s), a x x_1 → False
e_a₁₄ e_a₁₅ e_a₁₆ : x ∈ s → (∀ (x_1 : x ∈ s), ¬a x x_1) → ∃ (h : x ∈ s), ¬a x ⋯
e_a₁₇ : x ∈ s → ∀ (w : x ∈ s), ¬a x ⋯ → x ∈ s → ∀ (x_1 : x ∈ s), a x x_1 → False
e_a₁₈ e_a₁₉ e_a₂₀ e_a₂₁ e_a₂₂ e_a₂₃ e_a₂₄ e_a₂₅ : x ∈ s → (∀ (x_1 : x ∈ s), ¬a x x_1) → ∃ (h : x ∈ s), ¬a x ⋯
⊢ x ∈ s → ((∃ (h : x ∈ s), ¬a x ⋯) ↔ x ∈ s → ∀ (x_1 : x ∈ s), ¬a x x_1)

Tactic:
tauto
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
inst_1 : DecidableEq ι
f g : ι → R
s : Finset ι
i : Eq.{u_4 + 1} (α := R) (∏ i ∈ s, (f i + g i)) (∏ i ∈ s, ∑ p ∈ {True, False}, if p then f i else g i)
⊢ Eq.{u_4 + 1} (α := R) (∏ i ∈ s, (f i + g i)) (∑ t ∈ s.powerset, HMul.hMul (α := R) (∏ i ∈ t, f i) (∏ i ∈ s \ t, g i))

Tactic:
calc
    ∏ i ∈ s, (f i + g i) =
        ∏ i ∈ s, ∑ p ∈ ({True, False} : Finset Prop), if p then f i else g i := by simp
    _ = ∑ p ∈ (s.pi fun _ => {True, False} : Finset (∀ a ∈ s, Prop)),
          ∏ a ∈ s.attach, if p a.1 a.2 then f a.1 else g a.1 := prod_sum _ _ _
    _ = ∑ t ∈ s.powerset, (∏ a ∈ t, f a) * ∏ a ∈ s \ t, g a :=
      sum_bij'
        (fun f _ ↦ {a ∈ s | ∃ h : a ∈ s, f a h})
        (fun t _ a _ => a ∈ t)
        (by simp)
        (by simp [Classical.em])
        (by simp_rw [mem_filter, funext_iff, eq_iff_iff, mem_pi, mem_insert]; tauto)
        (by simp_rw [Finset.ext_iff, mem_filter, mem_powerset]; tauto)
        (fun a _ ↦ by
          simp only [prod_ite, filter_attach', prod_map, Function.Embedding.coeFn_mk,
            Subtype.map_coe, id_eq, prod_attach]
          congr 2 with x
          simp only [mem_filter, mem_sdiff, not_and, not_exists, and_congr_right_iff]
          tauto)

Premises used: False, Exists, Insert.insert, Finset.pi, True, Finset.attach, Finset.sum_bij', Finset.powerset, Finset.prod_sum, Singleton.singleton, Finset.filter
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
inst_1 : DecidableEq ι
f g : ι → R
s : Finset ι
i : Eq.{u_4 + 1} (α := R) (∏ i ∈ s, (f i + g i)) (∏ i ∈ s, ∑ p ∈ {True, False}, if p then f i else g i)
⊢ Eq.{u_4 + 1} (α := R) (∏ i ∈ s, (f i + g i)) (∑ t ∈ s.powerset, HMul.hMul (α := R) (∏ i ∈ t, f i) (∏ i ∈ s \ t, g i))

Tactic:
classical
  calc
    ∏ i ∈ s, (f i + g i) =
        ∏ i ∈ s, ∑ p ∈ ({True, False} : Finset Prop), if p then f i else g i := by simp
    _ = ∑ p ∈ (s.pi fun _ => {True, False} : Finset (∀ a ∈ s, Prop)),
          ∏ a ∈ s.attach, if p a.1 a.2 then f a.1 else g a.1 := prod_sum _ _ _
    _ = ∑ t ∈ s.powerset, (∏ a ∈ t, f a) * ∏ a ∈ s \ t, g a :=
      sum_bij'
        (fun f _ ↦ {a ∈ s | ∃ h : a ∈ s, f a h})
        (fun t _ a _ => a ∈ t)
        (by simp)
        (by simp [Classical.em])
        (by simp_rw [mem_filter, funext_iff, eq_iff_iff, mem_pi, mem_insert]; tauto)
        (by simp_rw [Finset.ext_iff, mem_filter, mem_powerset]; tauto)
        (fun a _ ↦ by
          simp only [prod_ite, filter_attach', prod_map, Function.Embedding.coeFn_mk,
            Subtype.map_coe, id_eq, prod_attach]
          congr 2 with x
          simp only [mem_filter, mem_sdiff, not_and, not_exists, and_congr_right_iff]
          tauto)

Premises used: False, Exists, Insert.insert, Finset.pi, True, Finset.attach, Finset.sum_bij', Finset.powerset, Finset.prod_sum, Singleton.singleton, Finset.filter
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
f : ι → R
s : Finset ι
⊢ Eq.{u_4 + 1} (α := R) (∏ i ∈ s, (1 + f i)) (∑ t ∈ s.powerset, ∏ i ∈ t, f i)

Tactic:
simp only [add_comm (1 : R), prod_add, prod_const_one, mul_one]

Premises used: Finset.prod_add, add_comm, Finset.prod_const_one, mul_one, OfNat.ofNat
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
f : ι → R
s : Finset ι
⊢ Eq.{u_4 + 1} (α := R) (∏ i ∈ s, (1 + f i)) (∑ t ∈ s.powerset, ∏ i ∈ t, f i)

Tactic:
classical simp only [add_comm (1 : R), prod_add, prod_const_one, mul_one]

Premises used: Finset.prod_add, add_comm, Finset.prod_const_one, mul_one, OfNat.ofNat
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
f : ι → R
s : Finset ι
⊢ Eq.{u_4 + 1} (α := R) (∏ i ∈ s, (f i + 1)) (∑ t ∈ s.powerset, ∏ i ∈ t, f i)

Tactic:
simp only [prod_add, prod_const_one, mul_one]

Premises used: Finset.prod_add, Finset.prod_const_one, mul_one
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
f : ι → R
s : Finset ι
⊢ Eq.{u_4 + 1} (α := R) (∏ i ∈ s, (f i + 1)) (∑ t ∈ s.powerset, ∏ i ∈ t, f i)

Tactic:
classical simp only [prod_add, prod_const_one, mul_one]

Premises used: Finset.prod_add, Finset.prod_const_one, mul_one
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
inst_1 : LinearOrder ι
s : Finset ι
f g : ι → R
⊢ ∏ i ∈ ∅, (f i + g i) =
    HAdd.hAdd (α := R) (∏ i ∈ ∅, f i) (∑ i ∈ ∅, (g i * ∏ j ∈ ∅ with j < i, (f j + g j)) * ∏ j ∈ ∅ with i < j, f j)

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
inst_1 : LinearOrder ι
s : Finset ι
f g : ι → R
refine :
  ∀ (a : ι) (s : Finset ι),
    (∀ x ∈ s, x < a) →
      ∏ i ∈ s, (f i + g i) =
          HAdd.hAdd (α := R) (∏ i ∈ s, f i)
            (∑ i ∈ s, (g i * ∏ j ∈ s with j < i, (f j + g j)) * ∏ j ∈ s with i < j, f j) →
        ∏ i ∈ insert a s, (f i + g i) =
          HAdd.hAdd (α := R) (∏ i ∈ insert a s, f i)
            (∑ i ∈ insert a s, (g i * ∏ j ∈ insert a s with j < i, (f j + g j)) * ∏ j ∈ insert a s with i < j, f j)
⊢ ∏ i ∈ s, (f i + g i) =
    HAdd.hAdd (α := R) (∏ i ∈ s, f i) (∑ i ∈ s, (g i * ∏ j ∈ s with j < i, (f j + g j)) * ∏ j ∈ s with i < j, f j)

Tactic:
refine Finset.induction_on_max s (by simp) ?_
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
inst_1 : LinearOrder ι
f g : ι → R
a : ι
s : Finset ι
ha : ∀ x ∈ s, x < a
ihs :
  ∏ i ∈ s, (f i + g i) =
    HAdd.hAdd (α := R) (∏ i ∈ s, f i) (∑ i ∈ s, (g i * ∏ j ∈ s with j < i, (f j + g j)) * ∏ j ∈ s with i < j, f j)
⊢ a ∉ s

Tactic:
have ha' : a ∉ s := fun ha' => lt_irrefl a (ha a ha')
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
inst_1 : LinearOrder ι
f g : ι → R
a : ι
s : Finset ι
ha : ∀ x ∈ s, x < a
ihs :
  ∏ i ∈ s, (f i + g i) =
    HAdd.hAdd (α := R) (∏ i ∈ s, f i) (∑ i ∈ s, (g i * ∏ j ∈ s with j < i, (f j + g j)) * ∏ j ∈ s with i < j, f j)
ha' : a ∉ s
rw :
  f a * ∏ i ∈ s, f i +
      (f a * ∑ i ∈ s, (g i * ∏ j ∈ s with j < i, (f j + g j)) * ∏ j ∈ s with i < j, f j +
        (g a * ∏ i ∈ s, f i + g a * ∑ i ∈ s, (g i * ∏ j ∈ s with j < i, (f j + g j)) * ∏ j ∈ s with i < j, f j)) =
    f a * ∏ x ∈ s, f x +
      ((g a * ∏ i ∈ s, f i + g a * ∑ i ∈ s, (g i * ∏ j ∈ s with j < i, (f j + g j)) * ∏ j ∈ s with i < j, f j) *
          ∏ j ∈ insert a s with a < j, f j +
        ∑ x ∈ s, (g x * ∏ j ∈ insert a s with j < x, (f j + g j)) * ∏ j ∈ insert a s with x < j, f j)
⊢ ∏ i ∈ insert a s, (f i + g i) =
    HAdd.hAdd (α := R) (∏ i ∈ insert a s, f i)
      (∑ i ∈ insert a s, (g i * ∏ j ∈ insert a s with j < i, (f j + g j)) * ∏ j ∈ insert a s with i < j, 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]

Premises used: add_mul, lt_irrefl, Finset.prod_insert, add_assoc, Finset.filter_true_of_mem, Finset.filter_insert, mul_add, Finset.sum_insert, if_neg
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
inst_1 : LinearOrder ι
f g : ι → R
a : ι
s : Finset ι
ha : ∀ x ∈ s, x < a
ihs :
  ∏ i ∈ s, (f i + g i) =
    HAdd.hAdd (α := R) (∏ i ∈ s, f i) (∑ i ∈ s, (g i * ∏ j ∈ s with j < i, (f j + g j)) * ∏ j ∈ s with i < j, f j)
ha' : a ∉ s
e_a :
  f a * ∑ i ∈ s, (g i * ∏ j ∈ s with j < i, (f j + g j)) * ∏ j ∈ s with i < j, f j +
      (g a * ∏ i ∈ s, f i + g a * ∑ i ∈ s, (g i * ∏ j ∈ s with j < i, (f j + g j)) * ∏ j ∈ s with i < j, f j) =
    (g a * ∏ i ∈ s, f i + g a * ∑ i ∈ s, (g i * ∏ j ∈ s with j < i, (f j + g j)) * ∏ j ∈ s with i < j, f j) *
        ∏ j ∈ insert a s with a < j, f j +
      ∑ x ∈ s, (g x * ∏ j ∈ insert a s with j < x, (f j + g j)) * ∏ j ∈ insert a s with x < j, f j
⊢ f a * ∏ i ∈ s, f i +
      (f a * ∑ i ∈ s, (g i * ∏ j ∈ s with j < i, (f j + g j)) * ∏ j ∈ s with i < j, f j +
        (g a * ∏ i ∈ s, f i + g a * ∑ i ∈ s, (g i * ∏ j ∈ s with j < i, (f j + g j)) * ∏ j ∈ s with i < j, f j)) =
    f a * ∏ x ∈ s, f x +
      ((g a * ∏ i ∈ s, f i + g a * ∑ i ∈ s, (g i * ∏ j ∈ s with j < i, (f j + g j)) * ∏ j ∈ s with i < j, f j) *
          ∏ j ∈ insert a s with a < j, f j +
        ∑ x ∈ s, (g x * ∏ j ∈ insert a s with j < x, (f j + g j)) * ∏ j ∈ insert a s with x < j, f j)

Tactic:
congr 1
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
inst_1 : LinearOrder ι
f g : ι → R
a : ι
s : Finset ι
ha : ∀ x ∈ s, x < a
ihs :
  ∏ i ∈ s, (f i + g i) =
    HAdd.hAdd (α := R) (∏ i ∈ s, f i) (∑ i ∈ s, (g i * ∏ j ∈ s with j < i, (f j + g j)) * ∏ j ∈ s with i < j, f j)
ha' : a ∉ s
e_a :
  g a * ∏ i ∈ s, f i + g a * ∑ i ∈ s, (g i * ∏ j ∈ s with j < i, (f j + g j)) * ∏ j ∈ s with i < j, f j +
      f a * ∑ i ∈ s, (g i * ∏ j ∈ s with j < i, (f j + g j)) * ∏ j ∈ s with i < j, f j =
    (g a * ∏ i ∈ s, f i + g a * ∑ i ∈ s, (g i * ∏ j ∈ s with j < i, (f j + g j)) * ∏ j ∈ s with i < j, f j) *
        ∏ j ∈ insert a s with a < j, f j +
      ∑ x ∈ s, (g x * ∏ j ∈ insert a s with j < x, (f j + g j)) * ∏ j ∈ insert a s with x < j, f j
⊢ f a * ∑ i ∈ s, (g i * ∏ j ∈ s with j < i, (f j + g j)) * ∏ j ∈ s with i < j, f j +
      (g a * ∏ i ∈ s, f i + g a * ∑ i ∈ s, (g i * ∏ j ∈ s with j < i, (f j + g j)) * ∏ j ∈ s with i < j, f j) =
    (g a * ∏ i ∈ s, f i + g a * ∑ i ∈ s, (g i * ∏ j ∈ s with j < i, (f j + g j)) * ∏ j ∈ s with i < j, f j) *
        ∏ j ∈ insert a s with a < j, f j +
      ∑ x ∈ s, (g x * ∏ j ∈ insert a s with j < x, (f j + g j)) * ∏ j ∈ insert a s with x < j, f j

Tactic:
rw [add_comm]

Premises used: add_comm
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
inst_1 : LinearOrder ι
f g : ι → R
a : ι
s : Finset ι
ha : ∀ x ∈ s, x < a
ihs :
  ∏ i ∈ s, (f i + g i) =
    HAdd.hAdd (α := R) (∏ i ∈ s, f i) (∑ i ∈ s, (g i * ∏ j ∈ s with j < i, (f j + g j)) * ∏ j ∈ s with i < j, f j)
ha' : a ∉ s
e_a :
  g a * ∏ i ∈ s, f i + g a * ∑ i ∈ s, (g i * ∏ j ∈ s with j < i, (f j + g j)) * ∏ j ∈ s with i < j, f j =
    (g a * ∏ i ∈ s, f i + g a * ∑ i ∈ s, (g i * ∏ j ∈ s with j < i, (f j + g j)) * ∏ j ∈ s with i < j, f j) *
      ∏ j ∈ insert a s with a < j, f j
e_a₁ :
  f a * ∑ i ∈ s, (g i * ∏ j ∈ s with j < i, (f j + g j)) * ∏ j ∈ s with i < j, f j =
    ∑ x ∈ s, (g x * ∏ j ∈ insert a s with j < x, (f j + g j)) * ∏ j ∈ insert a s with x < j, f j
⊢ g a * ∏ i ∈ s, f i + g a * ∑ i ∈ s, (g i * ∏ j ∈ s with j < i, (f j + g j)) * ∏ j ∈ s with i < j, f j +
      f a * ∑ i ∈ s, (g i * ∏ j ∈ s with j < i, (f j + g j)) * ∏ j ∈ s with i < j, f j =
    (g a * ∏ i ∈ s, f i + g a * ∑ i ∈ s, (g i * ∏ j ∈ s with j < i, (f j + g j)) * ∏ j ∈ s with i < j, f j) *
        ∏ j ∈ insert a s with a < j, f j +
      ∑ x ∈ s, (g x * ∏ j ∈ insert a s with j < x, (f j + g j)) * ∏ j ∈ insert a s with x < j, f j

Tactic:
congr 1
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
inst_1 : LinearOrder ι
f g : ι → R
a : ι
s : Finset ι
ha : ∀ x ∈ s, x < a
ihs :
  ∏ i ∈ s, (f i + g i) =
    HAdd.hAdd (α := R) (∏ i ∈ s, f i) (∑ i ∈ s, (g i * ∏ j ∈ s with j < i, (f j + g j)) * ∏ j ∈ s with i < j, f j)
ha' : a ∉ s
e_a : ∀ x ∈ insert a s, ¬a < x
⊢ g a * ∏ i ∈ s, f i + g a * ∑ i ∈ s, (g i * ∏ j ∈ s with j < i, (f j + g j)) * ∏ j ∈ s with i < j, f j =
    (g a * ∏ i ∈ s, f i + g a * ∑ i ∈ s, (g i * ∏ j ∈ s with j < i, (f j + g j)) * ∏ j ∈ s with i < j, f j) *
      ∏ j ∈ insert a s with a < j, f j

Tactic:
rw [filter_false_of_mem, prod_empty, mul_one]

Premises used: Finset.prod_empty, Finset.filter_false_of_mem, mul_one
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
inst_1 : LinearOrder ι
f g : ι → R
a : ι
s : Finset ι
ha : ∀ x ∈ s, x < a
ihs :
  ∏ i ∈ s, (f i + g i) =
    HAdd.hAdd (α := R) (∏ i ∈ s, f i) (∑ i ∈ s, (g i * ∏ j ∈ s with j < i, (f j + g j)) * ∏ j ∈ s with i < j, f j)
ha' : a ∉ s
⊢ ∀ x ∈ insert a s, ¬a < x

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

Premises used: Iff.mpr, lt_irrefl, Finset.forall_mem_insert, And.intro, LT.lt.not_gt
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
inst_1 : LinearOrder ι
f g : ι → R
a : ι
s : Finset ι
ha : ∀ x ∈ s, x < a
ihs :
  ∏ i ∈ s, (f i + g i) =
    HAdd.hAdd (α := R) (∏ i ∈ s, f i) (∑ i ∈ s, (g i * ∏ j ∈ s with j < i, (f j + g j)) * ∏ j ∈ s with i < j, 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_gt⟩
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
inst_1 : LinearOrder ι
f g : ι → R
a : ι
s : Finset ι
ha : ∀ x ∈ s, x < a
ihs :
  ∏ i ∈ s, (f i + g i) =
    HAdd.hAdd (α := R) (∏ i ∈ s, f i) (∑ i ∈ s, (g i * ∏ j ∈ s with j < i, (f j + g j)) * ∏ j ∈ s with i < j, f j)
ha' : a ∉ s
e_a :
  Eq.{u_4 + 1} (α := R) (∑ i ∈ s, f a * ((g i * ∏ j ∈ s with j < i, (f j + g j)) * ∏ j ∈ s with i < j, f j))
    (∑ x ∈ s, (g x * ∏ j ∈ insert a s with j < x, (f j + g j)) * ∏ j ∈ insert a s with x < j, f j)
⊢ f a * ∑ i ∈ s, (g i * ∏ j ∈ s with j < i, (f j + g j)) * ∏ j ∈ s with i < j, f j =
    ∑ x ∈ s, (g x * ∏ j ∈ insert a s with j < x, (f j + g j)) * ∏ j ∈ insert a s with x < j, f j

Tactic:
rw [mul_sum]

Premises used: Finset.mul_sum
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
inst_1 : LinearOrder ι
f g : ι → R
a : ι
s : Finset ι
ha : ∀ x ∈ s, x < a
ihs :
  ∏ i ∈ s, (f i + g i) =
    HAdd.hAdd (α := R) (∏ i ∈ s, f i) (∑ i ∈ s, (g i * ∏ j ∈ s with j < i, (f j + g j)) * ∏ j ∈ s with i < j, f j)
ha' : a ∉ s
⊢ Eq.{u_4 + 1} (α := R) (∑ i ∈ s, f a * ((g i * ∏ j ∈ s with j < i, (f j + g j)) * ∏ j ∈ s with i < j, f j))
    (∑ x ∈ s, (g x * ∏ j ∈ insert a s with j < x, (f j + g j)) * ∏ j ∈ insert a s with x < j, f j)

Tactic:
sum_congr rfl fun i hi => ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
inst_1 : LinearOrder ι
f g : ι → R
a : ι
s : Finset ι
ha : ∀ x ∈ s, x < a
ihs :
  ∏ i ∈ s, (f i + g i) =
    HAdd.hAdd (α := R) (∏ i ∈ s, f i) (∑ i ∈ s, (g i * ∏ j ∈ s with j < i, (f j + g j)) * ∏ j ∈ s with i < j, f j)
ha' : a ∉ s
e_a :
  ∀ (i : ι) (hi : i ∈ s),
    f a * ((g i * ∏ j ∈ s with j < i, (f j + g j)) * ∏ j ∈ s with i < j, f j) =
      (g i * ∏ j ∈ insert a s with j < i, (f j + g j)) * ∏ j ∈ insert a s with i < j, f j
⊢ Eq.{u_4 + 1} (α := R) (∑ i ∈ s, f a * ((g i * ∏ j ∈ s with j < i, (f j + g j)) * ∏ j ∈ s with i < j, f j))
    (∑ x ∈ s, (g x * ∏ j ∈ insert a s with j < x, (f j + g j)) * ∏ j ∈ insert a s with x < j, f j)

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

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
inst_1 : LinearOrder ι
f g : ι → R
a : ι
s : Finset ι
ha : ∀ x ∈ s, x < a
ihs :
  ∏ i ∈ s, (f i + g i) =
    HAdd.hAdd (α := R) (∏ i ∈ s, f i) (∑ i ∈ s, (g i * ∏ j ∈ s with j < i, (f j + g j)) * ∏ j ∈ s with i < j, f j)
ha' : a ∉ s
i : ι
hi : i ∈ s
e_a : a ∉ {j ∈ s | i < j}
⊢ f a * ((g i * ∏ j ∈ s with j < i, (f j + g j)) * ∏ j ∈ s with i < j, f j) =
    (g i * ∏ j ∈ insert a s with j < i, (f j + g j)) * ∏ j ∈ insert a s with i < j, f j

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

Premises used: Finset.prod_insert, mul_left_comm, if_pos, Finset.filter_insert, LT.lt.not_gt, if_neg
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
inst_1 : LinearOrder ι
f g : ι → R
a : ι
s : Finset ι
ha : ∀ x ∈ s, x < a
ihs :
  ∏ i ∈ s, (f i + g i) =
    HAdd.hAdd (α := R) (∏ i ∈ s, f i) (∑ i ∈ s, (g i * ∏ j ∈ s with j < i, (f j + g j)) * ∏ j ∈ s with i < j, f j)
ha' : a ∉ s
i : ι
hi : i ∈ s
⊢ a ∉ {j ∈ s | i < j}

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

Premises used: mt, And.left, Iff.mp, Finset.mem_filter
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
inst_1 : LinearOrder ι
f g : ι → R
a : ι
s : Finset ι
ha : ∀ x ∈ s, x < a
ihs :
  ∏ i ∈ s, (f i + g i) =
    HAdd.hAdd (α := R) (∏ i ∈ s, f i) (∑ i ∈ s, (g i * ∏ j ∈ s with j < i, (f j + g j)) * ∏ j ∈ s with i < j, f j)
ha' : a ∉ s
i : ι
hi : i ∈ s
⊢ a ∉ {j ∈ s | i < j}

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

Premises used: mt, And.left, Iff.mp, Finset.mem_filter
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
inst_1 : LinearOrder ι
s : Finset ι
f : ι → R
rw :
  HAdd.hAdd (α := R) (∏ i ∈ s, 1) (∑ i ∈ s, (f i * ∏ j ∈ s with j < i, (1 + f j)) * ∏ j ∈ s with i < j, 1) =
    HAdd.hAdd (α := R) 1 (∑ i ∈ s, f i * ∏ j ∈ s with j < i, (1 + f j))
⊢ ∏ i ∈ s, (1 + f i) = HAdd.hAdd (α := R) 1 (∑ i ∈ s, f i * ∏ j ∈ s with j < i, (1 + f j))

Tactic:
rw [prod_add_ordered]

Premises used: Finset.prod_add_ordered
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
inst_1 : LinearOrder ι
s : Finset ι
f : ι → R
⊢ HAdd.hAdd (α := R) (∏ i ∈ s, 1) (∑ i ∈ s, (f i * ∏ j ∈ s with j < i, (1 + f j)) * ∏ j ∈ s with i < j, 1) =
    HAdd.hAdd (α := R) 1 (∑ i ∈ s, f i * ∏ j ∈ s with j < i, (1 + f j))

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
a b : R
s : Finset ι
rw :
  Eq.{u_4 + 1} (α := R) (∑ t ∈ s.powerset, a ^ #t * b ^ (#s - #t))
    (∑ t ∈ s.powerset, HMul.hMul (α := R) (∏ i ∈ t, a) (∏ i ∈ s \ t, b))
⊢ ∑ t ∈ s.powerset, a ^ #t * b ^ (#s - #t) = (a + b) ^ #s

Tactic:
rw [← prod_const, prod_add]

Premises used: Finset.prod_add, Finset.prod_const
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
a b : R
s : Finset ι
⊢ Eq.{u_4 + 1} (α := R) (∑ t ∈ s.powerset, a ^ #t * b ^ (#s - #t))
    (∑ t ∈ s.powerset, HMul.hMul (α := R) (∏ i ∈ t, a) (∏ i ∈ s \ t, b))

Tactic:
Finset.sum_congr rfl fun t ht => ?_

Premises used: Finset.sum_congr, rfl