awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.Finset (goal)
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 ⋯
⊢ x ∈ s → ((∃ (h : x ∈ s), ¬a x ⋯) ↔ x ∈ s → ∀ (x_1 : x ∈ s), ¬a x x_1)
have e_a₄ : x ∈ s → ∀ (w : x ∈ s), ¬a x sorry → x ∈ s → ∀ (x_1 : x ∈ s), ¬a x x_1
Tactic: tauto
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.Finset (goal)
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
⊢ x ∈ s → ((∃ (h : x ∈ s), ¬a x ⋯) ↔ x ∈ s → ∀ (x_1 : x ∈ s), ¬a x x_1)
have e_a₇ : x ∈ s → x ∉ s → ∃ (h : x ∈ s), ¬a x sorry
Tactic: tauto
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.Finset (goal)
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 ⋯
⊢ x ∈ s → ((∃ (h : x ∈ s), ¬a x ⋯) ↔ x ∈ s → ∀ (x_1 : x ∈ s), ¬a x x_1)
have e_a₈ : x ∈ s → (∀ (x_1 : x ∈ s), ¬a x x_1) → ∃ (h : x ∈ s), ¬a x sorry
Tactic: tauto
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.Finset (goal)
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
inst_1 : DecidableEq ι
f g : ι → R
s : Finset ι
⊢ 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))
have 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)
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)
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.Finset (goal)
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
inst_1 : DecidableEq ι
f g : ι → R
s : Finset ι
⊢ 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))
have 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)
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)
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.Finset (goal)
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
inst_1 : LinearOrder ι
s : Finset ι
f g : ι → R
⊢ ∏ 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)
have 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)
Tactic: refine Finset.induction_on_max s (by simp) ?_
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.Finset (hypothesis)
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)
⊢ ∏ 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)
have ha' : a ∉ s
Tactic: have ha' : a ∉ s := fun ha' => lt_irrefl a (ha a ha')
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.Finset (goal)
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 ∈ 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)
have 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)
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]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.Finset (goal)
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
⊢ 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)
have 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
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.Finset (goal)
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
⊢ 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
have 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
Tactic: rw [add_comm]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.Finset (goal)
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
⊢ 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
have 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
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.Finset (goal)
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
⊢ 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
have 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
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.Finset (goal)
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
⊢ 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
have e_a : ∀ x ∈ insert a s, ¬a < x
Tactic: rw [filter_false_of_mem, prod_empty, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.Finset (goal)
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
⊢ 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
have 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)
Tactic: rw [mul_sum]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.Finset (goal)
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)
have 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
Tactic: refine sum_congr rfl fun i hi => ?_
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.Finset (goal)
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
⊢ 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
have e_a : a ∉ {j ∈ s | i < j}
Tactic: rw [filter_insert, if_neg (ha i hi).not_gt, filter_insert, if_pos (ha i hi), prod_insert,
      mul_left_comm]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.Finset (goal)
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
inst_1 : LinearOrder ι
s : Finset ι
f : ι → R
⊢ ∏ i ∈ s, (1 + f i) = HAdd.hAdd (α := R) 1 (∑ i ∈ s, f i * ∏ j ∈ s with j < i, (1 + f j))
have 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))
Tactic: rw [prod_add_ordered]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.Finset (goal)
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
a b : R
s : Finset ι
⊢ ∑ t ∈ s.powerset, a ^ #t * b ^ (#s - #t) = (a + b) ^ #s
have 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))
Tactic: rw [← prod_const, prod_add]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.Finset (goal)
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))
have refine : ∀ (t : Finset ι) (ht : t ∈ s.powerset), a ^ #t * b ^ (#s - #t) = HMul.hMul (α := R) (∏ i ∈ t, a) (∏ i ∈ s \ t, b)
Tactic: refine Finset.sum_congr rfl fun t ht => ?_
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.Finset (goal)
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
a b : R
s t : Finset ι
ht : t ∈ s.powerset
⊢ a ^ #t * b ^ (#s - #t) = HMul.hMul (α := R) (∏ i ∈ t, a) (∏ i ∈ s \ t, b)
have rw : a ^ #t * b ^ (#s - #t) = a ^ #t * ∏ i ∈ s \ t, b
Tactic: rw [prod_const, prod_const, ← card_sdiff_of_subset (mem_powerset.1 ht)]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.Finset (goal)
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
a b : R
s t : Finset ι
ht : t ∈ s.powerset
rw : a ^ #t * b ^ (#s - #t) = a ^ #t * ∏ i ∈ s \ t, b
⊢ a ^ #t * b ^ (#s - #t) = HMul.hMul (α := R) (∏ i ∈ t, a) (∏ i ∈ s \ t, b)
have rw₁ : a ^ #t * b ^ (#s - #t) = a ^ #t * b ^ #(s \ t)
Tactic: rw [prod_const, prod_const, ← card_sdiff_of_subset (mem_powerset.1 ht)]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.Finset (goal)
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
a b : R
s t : Finset ι
ht : t ∈ s.powerset
rw : a ^ #t * b ^ (#s - #t) = a ^ #t * ∏ i ∈ s \ t, b
rw₁ : a ^ #t * b ^ (#s - #t) = a ^ #t * b ^ #(s \ t)
⊢ a ^ #t * b ^ (#s - #t) = HMul.hMul (α := R) (∏ i ∈ t, a) (∏ i ∈ s \ t, b)
have rw₂ : a ^ #t * b ^ #(s \ t) = a ^ #t * b ^ #(s \ t)
Tactic: rw [prod_const, prod_const, ← card_sdiff_of_subset (mem_powerset.1 ht)]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.Finset (goal)
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
a b : R
s : Finset ι
⊢ ∑ t ∈ s.powerset, a ^ #t * b ^ (#s - #t) = (a + b) ^ #s
have rw : Eq.{u_4 + 1} (α := R) (∑ t ∈ s.powerset, a ^ #t * b ^ (#s - #t)) (∏ _x ∈ s, (a + b))
Tactic: classical
  rw [← prod_const, prod_add]
  refine Finset.sum_congr rfl fun t ht => ?_
  rw [prod_const, prod_const, ← card_sdiff_of_subset (mem_powerset.1 ht)]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.Finset (goal)
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)) (∏ _x ∈ s, (a + b))
⊢ ∑ t ∈ s.powerset, a ^ #t * b ^ (#s - #t) = (a + b) ^ #s
have 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))
Tactic: classical
  rw [← prod_const, prod_add]
  refine Finset.sum_congr rfl fun t ht => ?_
  rw [prod_const, prod_const, ← card_sdiff_of_subset (mem_powerset.1 ht)]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.Finset (goal)
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)) (∏ _x ∈ s, (a + b))
rw₁ rw₂ 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
have rw₄ : ∀ (t : Finset ι) (ht : t ∈ s.powerset), a ^ #t * b ^ (#s - #t) = HMul.hMul (α := R) (∏ i ∈ t, a) (∏ i ∈ s \ t, b)
Tactic: classical
  rw [← prod_const, prod_add]
  refine Finset.sum_congr rfl fun t ht => ?_
  rw [prod_const, prod_const, ← card_sdiff_of_subset (mem_powerset.1 ht)]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.Finset (goal)
Goal:
ι : Type u_1
R : Type u_4
inst : CommRing R
inst_1 : LinearOrder ι
s : Finset ι
f g : ι → R
⊢ ∏ i ∈ s, (f i - g i) =
    HSub.hSub (α := 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)
have simp : ∏ x ∈ s, (f x + -g x) =
  HAdd.hAdd (α := R) (∏ i ∈ s, f i) (-∑ x ∈ s, (g x * ∏ x ∈ s with x < x, (f x + -g x)) * ∏ i ∈ s with x < i, f i)
Tactic: simp only [sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.Finset (goal)
Goal:
ι : Type u_1
R : Type u_4
inst : CommRing R
inst_1 : LinearOrder ι
s : Finset ι
f g : ι → R
⊢ ∏ x ∈ s, (f x + -g x) =
    HAdd.hAdd (α := R) (∏ i ∈ s, f i) (-∑ x ∈ s, (g x * ∏ x ∈ s with x < x, (f x + -g x)) * ∏ i ∈ s with x < i, f i)
have h : Eq.{u_4 + 1} (α := R) (-∑ x ∈ s, (g x * ∏ x ∈ s with x < x, (f x + -g x)) * ∏ i ∈ s with x < i, f i)
  (∑ i ∈ s, (-g i * ∏ j ∈ s with j < i, (f j + -g j)) * ∏ j ∈ s with i < j, f j)
Tactic: convert! prod_add_ordered s f fun i => -g i
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.Finset (goal)
Goal:
ι : Type u_1
R : Type u_4
inst : CommRing R
inst_1 : LinearOrder ι
s : Finset ι
f : ι → R
⊢ ∏ i ∈ s, (1 - f i) = HSub.hSub (α := R) 1 (∑ i ∈ s, f i * ∏ j ∈ s with j < i, (1 - f j))
have rw : HSub.hSub (α := R) (∏ i ∈ s, 1) (∑ i ∈ s, (f i * ∏ j ∈ s with j < i, (1 - f j)) * ∏ j ∈ s with i < j, 1) =
  HSub.hSub (α := R) 1 (∑ i ∈ s, f i * ∏ j ∈ s with j < i, (1 - f j))
Tactic: rw [prod_sub_ordered]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.Finset (goal)
Goal:
R : Type u_4
inst : CommRing R
n k : ℕ
⊢ Eq.{u_4 + 1} (α := R) (∏ i ∈ range k, HSub.hSub (α := R) (↑n : R) (↑i : R)) (↑(∏ i ∈ range k, (n - i)) : R)
have rw : Eq.{u_4 + 1} (α := R) (∏ i ∈ range k, HSub.hSub (α := R) (↑n : R) (↑i : R)) (∏ i ∈ range k, (↑(n - i) : R))
Tactic: rw [prod_natCast]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.Finset (goal)
Goal:
R : Type u_4
inst : CommRing R
n k : ℕ
⊢ Eq.{u_4 + 1} (α := R) (∏ i ∈ range k, HSub.hSub (α := R) (↑n : R) (↑i : R)) (∏ i ∈ range k, (↑(n - i) : R))
have inl : ∀ (hkn : k ≤ n),
  Eq.{u_4 + 1} (α := R) (∏ i ∈ range k, HSub.hSub (α := R) (↑n : R) (↑i : R)) (∏ i ∈ range k, (↑(n - i) : R))
Tactic: rcases le_or_gt k n with hkn | hnk
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.Finset (goal)
Goal:
R : Type u_4
inst : CommRing R
n k : ℕ
inl :
  ∀ (hkn : k ≤ n),
    Eq.{u_4 + 1} (α := R) (∏ i ∈ range k, HSub.hSub (α := R) (↑n : R) (↑i : R)) (∏ i ∈ range k, (↑(n - i) : R))
⊢ Eq.{u_4 + 1} (α := R) (∏ i ∈ range k, HSub.hSub (α := R) (↑n : R) (↑i : R)) (∏ i ∈ range k, (↑(n - i) : R))
have inr : ∀ (hnk : n < k),
  Eq.{u_4 + 1} (α := R) (∏ i ∈ range k, HSub.hSub (α := R) (↑n : R) (↑i : R)) (∏ i ∈ range k, (↑(n - i) : R))
Tactic: rcases le_or_gt k n with hkn | hnk
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.Finset (hypothesis)
Goal:
R : Type u_4
inst : CommRing R
n k : ℕ
hnk : n < k
⊢ Eq.{u_4 + 1} (α := R) (∏ i ∈ range k, HSub.hSub (α := R) (↑n : R) (↑i : R)) (∏ i ∈ range k, (↑(n - i) : R))
have hnk₁ : n ∈ range k
Tactic: rw [← mem_range] at hnk
Cleared hypotheses: hnk
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.Finset (goal)
Goal:
R : Type u_4
inst : CommRing R
n k : ℕ
hnk : n ∈ range k
⊢ Eq.{u_4 + 1} (α := R) (∏ i ∈ range k, HSub.hSub (α := R) (↑n : R) (↑i : R)) (∏ i ∈ range k, (↑(n - i) : R))
have inr : Eq.{u_4 + 1} (α := R) (↑(n - n) : R) 0
Tactic: rw [prod_eq_zero hnk, prod_eq_zero hnk]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.Finset (goal)
Goal:
R : Type u_4
inst : CommRing R
n k : ℕ
hnk : n ∈ range k
inr : Eq.{u_4 + 1} (α := R) (↑(n - n) : R) 0
⊢ Eq.{u_4 + 1} (α := R) (∏ i ∈ range k, HSub.hSub (α := R) (↑n : R) (↑i : R)) (∏ i ∈ range k, (↑(n - i) : R))
have inr₁ : HSub.hSub (α := R) (↑n : R) (↑n : R) = 0
Tactic: rw [prod_eq_zero hnk, prod_eq_zero hnk]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.Finset (goal)
Goal:
ι : Type u_5
s : Finset ι
f : ι → ℕ
n : ℕ
hf : ∀ i ∈ s, n ∣ f i
⊢ (∑ i ∈ s, f i) / n = ∑ i ∈ s, f i / n
have inl : ∀ (hf : ∀ i ∈ s, 0 ∣ f i), HDiv.hDiv (α := ℕ) (∑ i ∈ s, f i) 0 = ∑ i ∈ s, f i / 0
Tactic: obtain rfl | hn := n.eq_zero_or_pos
Cleared hypotheses: n, hf