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 ι
κ : ι → Type u_5
s : Finset ι
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → R
⊢ Eq.{u_4 + 1} (α := R) (∏ a ∈ s, ∑ b ∈ t a, f a b) (∑ p ∈ s.pi (β := κ) t, ∏ x ∈ s.attach, f (↑x : ι) (p (↑x : ι) ⋯))
have empty : Eq.{u_4 + 1} (α := R) (∏ a ∈ ∅, ∑ b ∈ t a, f a b) (∑ p ∈ pi (β := κ) ∅ t, ∏ x ∈ attach ∅, f (↑x : ι) (p (↑x : ι) sorry))
Tactic: induction s using Finset.induction with
  | empty => simp
  | insert a s ha ih =>
    have h₁ : ∀ x ∈ t a, ∀ y ∈ t a, x ≠ y →
      Disjoint (image (Pi.cons s a x) (pi s t)) (image (Pi.cons s a y) (pi s t)) := by
      intro x _ y _ h
      simp only [disjoint_iff_ne, mem_image]
      rintro _ ⟨p₂, _, eq₂⟩ _ ⟨p₃, _, eq₃⟩ eq
      have : Pi.cons s a x p₂ a (mem_insert_self _ _)
              = Pi.cons s a y p₃ a (mem_insert_self _ _) := by rw [eq₂, eq₃, eq]
      rw [Pi.cons_same, Pi.cons_same] at this
      exact h this
    rw [prod_insert ha, pi_insert ha, ih, sum_mul, sum_biUnion h₁]
    refine sum_congr rfl fun b _ => ?_
    have h₂ : ∀ p₁ ∈ pi s t, ∀ p₂ ∈ pi s t, Pi.cons s a b p₁ = Pi.cons s a b p₂ → p₁ = p₂ :=
      fun p₁ _ p₂ _ eq => Pi.cons_injective ha eq
    rw [sum_image h₂, mul_sum]
    refine sum_congr rfl fun g _ => ?_
    rw [attach_insert, prod_insert, prod_image]
    · simp only [Pi.cons_same]
      congr with ⟨v, hv⟩
      congr
      exact (Pi.cons_ne (by rintro rfl; exact ha hv)).symm
    · exact fun _ _ _ _ => Subtype.ext ∘ Subtype.mk.inj
    · simpa only [mem_image, mem_attach, Subtype.mk.injEq, true_and,
        Subtype.exists, exists_prop, exists_eq_right] using ha
Cleared hypotheses: s
-- 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 ι
κ : ι → Type u_5
s : Finset ι
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → R
empty :
  Eq.{u_4 + 1} (α := R) (∏ a ∈ ∅, ∑ b ∈ t a, f a b) (∑ p ∈ pi (β := κ) ∅ t, ∏ x ∈ attach ∅, f (↑x : ι) (p (↑x : ι) ⋯))
⊢ Eq.{u_4 + 1} (α := R) (∏ a ∈ s, ∑ b ∈ t a, f a b) (∑ p ∈ s.pi (β := κ) t, ∏ x ∈ s.attach, f (↑x : ι) (p (↑x : ι) ⋯))
have insert : ∀ (a : ι) (s : Finset ι) (ha : a ∉ s)
  (ih :
    Eq.{u_4 + 1} (α := R) (∏ a ∈ s, ∑ b ∈ t a, f a b)
      (∑ p ∈ s.pi (β := κ) t, ∏ x ∈ s.attach, f (↑x : ι) (p (↑x : ι) sorry))),
  Eq.{u_4 + 1} (α := R) (∏ a ∈ insert a s, ∑ b ∈ t a, f a b)
    (∑ p ∈ (insert a s).pi (β := κ) t, ∏ x ∈ (insert a s).attach, f (↑x : ι) (p (↑x : ι) sorry))
Tactic: induction s using Finset.induction with
  | empty => simp
  | insert a s ha ih =>
    have h₁ : ∀ x ∈ t a, ∀ y ∈ t a, x ≠ y →
      Disjoint (image (Pi.cons s a x) (pi s t)) (image (Pi.cons s a y) (pi s t)) := by
      intro x _ y _ h
      simp only [disjoint_iff_ne, mem_image]
      rintro _ ⟨p₂, _, eq₂⟩ _ ⟨p₃, _, eq₃⟩ eq
      have : Pi.cons s a x p₂ a (mem_insert_self _ _)
              = Pi.cons s a y p₃ a (mem_insert_self _ _) := by rw [eq₂, eq₃, eq]
      rw [Pi.cons_same, Pi.cons_same] at this
      exact h this
    rw [prod_insert ha, pi_insert ha, ih, sum_mul, sum_biUnion h₁]
    refine sum_congr rfl fun b _ => ?_
    have h₂ : ∀ p₁ ∈ pi s t, ∀ p₂ ∈ pi s t, Pi.cons s a b p₁ = Pi.cons s a b p₂ → p₁ = p₂ :=
      fun p₁ _ p₂ _ eq => Pi.cons_injective ha eq
    rw [sum_image h₂, mul_sum]
    refine sum_congr rfl fun g _ => ?_
    rw [attach_insert, prod_insert, prod_image]
    · simp only [Pi.cons_same]
      congr with ⟨v, hv⟩
      congr
      exact (Pi.cons_ne (by rintro rfl; exact ha hv)).symm
    · exact fun _ _ _ _ => Subtype.ext ∘ Subtype.mk.inj
    · simpa only [mem_image, mem_attach, Subtype.mk.injEq, true_and,
        Subtype.exists, exists_prop, exists_eq_right] using ha
Cleared hypotheses: s
-- 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 ι
κ : ι → Type u_5
s : Finset ι
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → R
⊢ Eq.{u_4 + 1} (α := R) (∏ a ∈ s, ∑ b ∈ t a, f a b) (∑ p ∈ s.pi (β := κ) t, ∏ x ∈ s.attach, f (↑x : ι) (p (↑x : ι) ⋯))
have empty : Eq.{u_4 + 1} (α := R) (∏ a ∈ ∅, ∑ b ∈ t a, f a b) (∑ p ∈ pi (β := κ) ∅ t, ∏ x ∈ attach ∅, f (↑x : ι) (p (↑x : ι) sorry))
Tactic: classical
  induction s using Finset.induction with
  | empty => simp
  | insert a s ha ih =>
    have h₁ : ∀ x ∈ t a, ∀ y ∈ t a, x ≠ y →
      Disjoint (image (Pi.cons s a x) (pi s t)) (image (Pi.cons s a y) (pi s t)) := by
      intro x _ y _ h
      simp only [disjoint_iff_ne, mem_image]
      rintro _ ⟨p₂, _, eq₂⟩ _ ⟨p₃, _, eq₃⟩ eq
      have : Pi.cons s a x p₂ a (mem_insert_self _ _)
              = Pi.cons s a y p₃ a (mem_insert_self _ _) := by rw [eq₂, eq₃, eq]
      rw [Pi.cons_same, Pi.cons_same] at this
      exact h this
    rw [prod_insert ha, pi_insert ha, ih, sum_mul, sum_biUnion h₁]
    refine sum_congr rfl fun b _ => ?_
    have h₂ : ∀ p₁ ∈ pi s t, ∀ p₂ ∈ pi s t, Pi.cons s a b p₁ = Pi.cons s a b p₂ → p₁ = p₂ :=
      fun p₁ _ p₂ _ eq => Pi.cons_injective ha eq
    rw [sum_image h₂, mul_sum]
    refine sum_congr rfl fun g _ => ?_
    rw [attach_insert, prod_insert, prod_image]
    · simp only [Pi.cons_same]
      congr with ⟨v, hv⟩
      congr
      exact (Pi.cons_ne (by rintro rfl; exact ha hv)).symm
    · exact fun _ _ _ _ => Subtype.ext ∘ Subtype.mk.inj
    · simpa only [mem_image, mem_attach, Subtype.mk.injEq, true_and,
        Subtype.exists, exists_prop, exists_eq_right] using ha
Cleared hypotheses: s
-- 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 ι
κ : ι → Type u_5
s : Finset ι
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → R
empty :
  Eq.{u_4 + 1} (α := R) (∏ a ∈ ∅, ∑ b ∈ t a, f a b) (∑ p ∈ pi (β := κ) ∅ t, ∏ x ∈ attach ∅, f (↑x : ι) (p (↑x : ι) ⋯))
⊢ Eq.{u_4 + 1} (α := R) (∏ a ∈ s, ∑ b ∈ t a, f a b) (∑ p ∈ s.pi (β := κ) t, ∏ x ∈ s.attach, f (↑x : ι) (p (↑x : ι) ⋯))
have insert : ∀ (a : ι) (s : Finset ι) (ha : a ∉ s)
  (ih :
    Eq.{u_4 + 1} (α := R) (∏ a ∈ s, ∑ b ∈ t a, f a b)
      (∑ p ∈ s.pi (β := κ) t, ∏ x ∈ s.attach, f (↑x : ι) (p (↑x : ι) sorry))),
  Eq.{u_4 + 1} (α := R) (∏ a ∈ insert a s, ∑ b ∈ t a, f a b)
    (∑ p ∈ (insert a s).pi (β := κ) t, ∏ x ∈ (insert a s).attach, f (↑x : ι) (p (↑x : ι) sorry))
Tactic: classical
  induction s using Finset.induction with
  | empty => simp
  | insert a s ha ih =>
    have h₁ : ∀ x ∈ t a, ∀ y ∈ t a, x ≠ y →
      Disjoint (image (Pi.cons s a x) (pi s t)) (image (Pi.cons s a y) (pi s t)) := by
      intro x _ y _ h
      simp only [disjoint_iff_ne, mem_image]
      rintro _ ⟨p₂, _, eq₂⟩ _ ⟨p₃, _, eq₃⟩ eq
      have : Pi.cons s a x p₂ a (mem_insert_self _ _)
              = Pi.cons s a y p₃ a (mem_insert_self _ _) := by rw [eq₂, eq₃, eq]
      rw [Pi.cons_same, Pi.cons_same] at this
      exact h this
    rw [prod_insert ha, pi_insert ha, ih, sum_mul, sum_biUnion h₁]
    refine sum_congr rfl fun b _ => ?_
    have h₂ : ∀ p₁ ∈ pi s t, ∀ p₂ ∈ pi s t, Pi.cons s a b p₁ = Pi.cons s a b p₂ → p₁ = p₂ :=
      fun p₁ _ p₂ _ eq => Pi.cons_injective ha eq
    rw [sum_image h₂, mul_sum]
    refine sum_congr rfl fun g _ => ?_
    rw [attach_insert, prod_insert, prod_image]
    · simp only [Pi.cons_same]
      congr with ⟨v, hv⟩
      congr
      exact (Pi.cons_ne (by rintro rfl; exact ha hv)).symm
    · exact fun _ _ _ _ => Subtype.ext ∘ Subtype.mk.inj
    · simpa only [mem_image, mem_attach, Subtype.mk.injEq, true_and,
        Subtype.exists, exists_prop, exists_eq_right] using ha
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.Finset (goal)
Goal:
ι : Type u_1
κ : Type u_2
R : Type u_4
inst : CommSemiring R
inst_1 : DecidableEq ι
inst_2 : Fintype ι
s : Finset κ
g : ι → κ → R
⊢ Eq.{u_4 + 1} (α := R) (∑ f ∈ piFinset (δ := fun (x : ι) ↦ κ) fun (x : ι) ↦ s, ∏ i : ι, g i (f i))
    (∏ i : ι, ∑ j ∈ s, g i j)
have rw : Eq.{u_4 + 1} (α := R) (∏ i : ι, ∑ j ∈ s, g i j) (∏ i : ι, ∑ j ∈ s, g i j)
Tactic: rw [← prod_univ_sum]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.Finset (goal)
Goal:
κ : Type u_2
R : Type u_4
inst : CommSemiring R
s : Finset κ
f : κ → R
n : ℕ
⊢ HPow.hPow (α := R) (∑ a ∈ s, f a) n =
    ∑ p ∈ piFinset (δ := fun (_i : Fin n) ↦ κ) fun (_i : Fin n) ↦ s, ∏ i : Fin n, f (p i)
have h : HPow.hPow (α := R) (∑ a ∈ s, f a) n = ∏ i : Fin n, ∑ j ∈ s, f j
Tactic: convert! @prod_univ_sum (Fin n) _ _ _ _ _ (fun _i ↦ s) fun _i d ↦ f d
-- 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)
    (ha :
      Membership.mem (γ := Finset ((a : ι) → a ∈ s → Prop)) (s.pi (β := fun (a : ι) ↦ Prop) fun (x : ι) ↦ {True, False})
        a),
    (fun (t : Finset ι) (x : t ∈ s.powerset) (a : ι) (x_1 : a ∈ s) ↦ a ∈ t)
        ((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 ha)
        ⋯ =
      a
have simp_rw : ∀ (a : (a : ι) → a ∈ s → Prop)
  (ha : ∀ (a_1 : ι) (h : a_1 ∈ s), a a_1 h = True ∨ Membership.mem (γ := Finset Prop) {False} (a a_1 h)) (x : ι)
  (x_1 : x ∈ s), (x ∈ s ∧ ∃ (h : x ∈ s), a x h) ↔ a x x_1
Tactic: simp_rw [mem_filter, funext_iff, eq_iff_iff, mem_pi, mem_insert]
-- 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 ι
tauto tauto₁ tauto₂ tauto₃ tauto₄ :
  ∀ (a : (a : ι) → a ∈ s → Prop),
    (∀ (a_1 : ι) (h : a_1 ∈ s), a a_1 h = True ∨ Membership.mem (γ := Finset Prop) {False} (a a_1 h)) →
      ∀ (x : ι) (x_1 : x ∈ s), (x ∈ s ∧ ∃ (h : x ∈ s), a x h) ↔ a x x_1
⊢ ∀ (a : (a : ι) → a ∈ s → Prop)
    (ha : ∀ (a_1 : ι) (h : a_1 ∈ s), a a_1 h = True ∨ Membership.mem (γ := Finset Prop) {False} (a a_1 h)) (x : ι)
    (x_1 : x ∈ s), (x ∈ s ∧ ∃ (h : x ∈ s), a x h) ↔ a x x_1
have mp : ∀ (a : (a : ι) → a ∈ s → Prop),
  (∀ (a_1 : ι) (h : a_1 ∈ s), a a_1 h = True ∨ Membership.mem (γ := Finset Prop) {False} (a a_1 h)) →
    ∀ (x : ι) (x_1 : x ∈ s), (x ∈ s ∧ ∃ (h : x ∈ s), a x h) → 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 ι
tauto tauto₁ tauto₂ tauto₃ tauto₄ :
  ∀ (a : (a : ι) → a ∈ s → Prop),
    (∀ (a_1 : ι) (h : a_1 ∈ s), a a_1 h = True ∨ Membership.mem (γ := Finset Prop) {False} (a a_1 h)) →
      ∀ (x : ι) (x_1 : x ∈ s), (x ∈ s ∧ ∃ (h : x ∈ s), a x h) ↔ a x x_1
mp :
  ∀ (a : (a : ι) → a ∈ s → Prop),
    (∀ (a_1 : ι) (h : a_1 ∈ s), a a_1 h = True ∨ Membership.mem (γ := Finset Prop) {False} (a a_1 h)) →
      ∀ (x : ι) (x_1 : x ∈ s), (x ∈ s ∧ ∃ (h : x ∈ s), a x h) → a x x_1
⊢ ∀ (a : (a : ι) → a ∈ s → Prop)
    (ha : ∀ (a_1 : ι) (h : a_1 ∈ s), a a_1 h = True ∨ Membership.mem (γ := Finset Prop) {False} (a a_1 h)) (x : ι)
    (x_1 : x ∈ s), (x ∈ s ∧ ∃ (h : x ∈ s), a x h) ↔ a x x_1
have mpr : ∀ (a : (a : ι) → a ∈ s → Prop),
  (∀ (a_1 : ι) (h : a_1 ∈ s), a a_1 h = True ∨ Membership.mem (γ := Finset Prop) {False} (a a_1 h)) →
    ∀ (x : ι) (x_1 : x ∈ s), a x x_1 → x ∈ s ∧ ∃ (h : x ∈ s), a x h
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 ι
tauto tauto₁ tauto₂ tauto₃ tauto₄ :
  ∀ (a : (a : ι) → a ∈ s → Prop),
    (∀ (a_1 : ι) (h : a_1 ∈ s), a a_1 h = True ∨ Membership.mem (γ := Finset Prop) {False} (a a_1 h)) →
      ∀ (x : ι) (x_1 : x ∈ s), (x ∈ s ∧ ∃ (h : x ∈ s), a x h) ↔ a x x_1
mp :
  ∀ (a : (a : ι) → a ∈ s → Prop),
    (∀ (a_1 : ι) (h : a_1 ∈ s), a a_1 h = True ∨ Membership.mem (γ := Finset Prop) {False} (a a_1 h)) →
      ∀ (x : ι) (x_1 : x ∈ s), (x ∈ s ∧ ∃ (h : x ∈ s), a x h) → a x x_1
mpr :
  ∀ (a : (a : ι) → a ∈ s → Prop),
    (∀ (a_1 : ι) (h : a_1 ∈ s), a a_1 h = True ∨ Membership.mem (γ := Finset Prop) {False} (a a_1 h)) →
      ∀ (x : ι) (x_1 : x ∈ s), a x x_1 → x ∈ s ∧ ∃ (h : x ∈ s), a x h
⊢ ∀ (a : (a : ι) → a ∈ s → Prop)
    (ha : ∀ (a_1 : ι) (h : a_1 ∈ s), a a_1 h = True ∨ Membership.mem (γ := Finset Prop) {False} (a a_1 h)) (x : ι)
    (x_1 : x ∈ s), (x ∈ s ∧ ∃ (h : x ∈ s), a x h) ↔ a x x_1
have mp₁ : ∀ (a : (a : ι) → a ∈ s → Prop),
  (∀ (a_1 : ι) (h : a_1 ∈ s), a a_1 h = True ∨ Membership.mem (γ := Finset Prop) {False} (a a_1 h)) →
    ∀ (x : ι) (x_1 : x ∈ s), x ∈ s → ∀ (w : x ∈ s), a x w → 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 ι
tauto tauto₁ tauto₂ tauto₃ tauto₄ :
  ∀ (a : (a : ι) → a ∈ s → Prop),
    (∀ (a_1 : ι) (h : a_1 ∈ s), a a_1 h = True ∨ Membership.mem (γ := Finset Prop) {False} (a a_1 h)) →
      ∀ (x : ι) (x_1 : x ∈ s), (x ∈ s ∧ ∃ (h : x ∈ s), a x h) ↔ a x x_1
mp :
  ∀ (a : (a : ι) → a ∈ s → Prop),
    (∀ (a_1 : ι) (h : a_1 ∈ s), a a_1 h = True ∨ Membership.mem (γ := Finset Prop) {False} (a a_1 h)) →
      ∀ (x : ι) (x_1 : x ∈ s), (x ∈ s ∧ ∃ (h : x ∈ s), a x h) → a x x_1
mpr :
  ∀ (a : (a : ι) → a ∈ s → Prop),
    (∀ (a_1 : ι) (h : a_1 ∈ s), a a_1 h = True ∨ Membership.mem (γ := Finset Prop) {False} (a a_1 h)) →
      ∀ (x : ι) (x_1 : x ∈ s), a x x_1 → x ∈ s ∧ ∃ (h : x ∈ s), a x h
mp₁ mp₂ mp₃ :
  ∀ (a : (a : ι) → a ∈ s → Prop),
    (∀ (a_1 : ι) (h : a_1 ∈ s), a a_1 h = True ∨ Membership.mem (γ := Finset Prop) {False} (a a_1 h)) →
      ∀ (x : ι) (x_1 : x ∈ s), x ∈ s → ∀ (w : x ∈ s), a x w → a x x_1
mpr₁ mpr₂ :
  ∀ (a : (a : ι) → a ∈ s → Prop),
    (∀ (a_1 : ι) (h : a_1 ∈ s), a a_1 h = True ∨ Membership.mem (γ := Finset Prop) {False} (a a_1 h)) →
      ∀ (x : ι) (x_1 : x ∈ s), a x x_1 → x ∈ s ∧ ∃ (h : x ∈ s), a x h
⊢ ∀ (a : (a : ι) → a ∈ s → Prop)
    (ha : ∀ (a_1 : ι) (h : a_1 ∈ s), a a_1 h = True ∨ Membership.mem (γ := Finset Prop) {False} (a a_1 h)) (x : ι)
    (x_1 : x ∈ s), (x ∈ s ∧ ∃ (h : x ∈ s), a x h) ↔ a x x_1
have mpr₃ : ∀ (a : (a : ι) → a ∈ s → Prop),
  (∀ (a_1 : ι) (h : a_1 ∈ s), a a_1 h = True ∨ Membership.mem (γ := Finset Prop) {False} (a a_1 h)) →
    ∀ (x : ι) (x_1 : x ∈ s), a x x_1 → x ∈ s
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 ι
tauto tauto₁ tauto₂ tauto₃ tauto₄ :
  ∀ (a : (a : ι) → a ∈ s → Prop),
    (∀ (a_1 : ι) (h : a_1 ∈ s), a a_1 h = True ∨ Membership.mem (γ := Finset Prop) {False} (a a_1 h)) →
      ∀ (x : ι) (x_1 : x ∈ s), (x ∈ s ∧ ∃ (h : x ∈ s), a x h) ↔ a x x_1
mp :
  ∀ (a : (a : ι) → a ∈ s → Prop),
    (∀ (a_1 : ι) (h : a_1 ∈ s), a a_1 h = True ∨ Membership.mem (γ := Finset Prop) {False} (a a_1 h)) →
      ∀ (x : ι) (x_1 : x ∈ s), (x ∈ s ∧ ∃ (h : x ∈ s), a x h) → a x x_1
mpr :
  ∀ (a : (a : ι) → a ∈ s → Prop),
    (∀ (a_1 : ι) (h : a_1 ∈ s), a a_1 h = True ∨ Membership.mem (γ := Finset Prop) {False} (a a_1 h)) →
      ∀ (x : ι) (x_1 : x ∈ s), a x x_1 → x ∈ s ∧ ∃ (h : x ∈ s), a x h
mp₁ mp₂ mp₃ :
  ∀ (a : (a : ι) → a ∈ s → Prop),
    (∀ (a_1 : ι) (h : a_1 ∈ s), a a_1 h = True ∨ Membership.mem (γ := Finset Prop) {False} (a a_1 h)) →
      ∀ (x : ι) (x_1 : x ∈ s), x ∈ s → ∀ (w : x ∈ s), a x w → a x x_1
mpr₁ mpr₂ :
  ∀ (a : (a : ι) → a ∈ s → Prop),
    (∀ (a_1 : ι) (h : a_1 ∈ s), a a_1 h = True ∨ Membership.mem (γ := Finset Prop) {False} (a a_1 h)) →
      ∀ (x : ι) (x_1 : x ∈ s), a x x_1 → x ∈ s ∧ ∃ (h : x ∈ s), a x h
mpr₃ :
  ∀ (a : (a : ι) → a ∈ s → Prop),
    (∀ (a_1 : ι) (h : a_1 ∈ s), a a_1 h = True ∨ Membership.mem (γ := Finset Prop) {False} (a a_1 h)) →
      ∀ (x : ι) (x_1 : x ∈ s), a x x_1 → x ∈ s
⊢ ∀ (a : (a : ι) → a ∈ s → Prop)
    (ha : ∀ (a_1 : ι) (h : a_1 ∈ s), a a_1 h = True ∨ Membership.mem (γ := Finset Prop) {False} (a a_1 h)) (x : ι)
    (x_1 : x ∈ s), (x ∈ s ∧ ∃ (h : x ∈ s), a x h) ↔ a x x_1
have mpr₄ : ∀ (a : (a : ι) → a ∈ s → Prop),
  (∀ (a_1 : ι) (h : a_1 ∈ s), a a_1 h = True ∨ Membership.mem (γ := Finset Prop) {False} (a a_1 h)) →
    ∀ (x : ι) (x_1 : x ∈ s), a x x_1 → ∃ (h : x ∈ s), a x h
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 : 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
have simp_rw : ∀ (a : Finset ι) (ha : a ⊆ s) (a_1 : ι), (a_1 ∈ s ∧ ∃ (_ : a_1 ∈ s), a_1 ∈ a) ↔ a_1 ∈ a
Tactic: simp_rw [Finset.ext_iff, mem_filter, mem_powerset]
-- 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 ι
tauto tauto₁ tauto₂ tauto₃ tauto₄ : ∀ a ⊆ s, ∀ (a_1 : ι), (a_1 ∈ s ∧ ∃ (_ : a_1 ∈ s), a_1 ∈ a) ↔ a_1 ∈ a
⊢ ∀ (a : Finset ι) (ha : a ⊆ s) (a_1 : ι), (a_1 ∈ s ∧ ∃ (_ : a_1 ∈ s), a_1 ∈ a) ↔ a_1 ∈ a
have mp : ∀ a ⊆ s, ∀ (a_1 : ι), (a_1 ∈ s ∧ ∃ (_ : a_1 ∈ s), a_1 ∈ a) → a_1 ∈ a
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 ι
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
⊢ ∀ (a : Finset ι) (ha : a ⊆ s) (a_1 : ι), (a_1 ∈ s ∧ ∃ (_ : a_1 ∈ s), a_1 ∈ a) ↔ a_1 ∈ a
have mpr : ∀ a ⊆ s, ∀ a_1 ∈ a, a_1 ∈ s ∧ ∃ (_ : a_1 ∈ s), a_1 ∈ a
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 ι
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
⊢ ∀ (a : Finset ι) (ha : a ⊆ s) (a_1 : ι), (a_1 ∈ s ∧ ∃ (_ : a_1 ∈ s), a_1 ∈ a) ↔ a_1 ∈ a
have mp₁ : ∀ a ⊆ s, ∀ a_1 ∈ s, a_1 ∈ s → a_1 ∈ a → a_1 ∈ a
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 ι
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
⊢ ∀ (a : Finset ι) (ha : a ⊆ s) (a_1 : ι), (a_1 ∈ s ∧ ∃ (_ : a_1 ∈ s), a_1 ∈ a) ↔ a_1 ∈ a
have mpr₃ : ∀ a ⊆ s, ∀ a_1 ∈ a, a_1 ∈ s
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 ι
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
⊢ ∀ (a : Finset ι) (ha : a ⊆ s) (a_1 : ι), (a_1 ∈ s ∧ ∃ (_ : a_1 ∈ s), a_1 ∈ a) ↔ a_1 ∈ a
have mpr₄ : ∀ a ⊆ s, ∀ a_1 ∈ a, ∃ (_ : a_1 ∈ s), a_1 ∈ a
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
⊢ (∏ 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)
have simp : HMul.hMul (α := R) (∏ x ∈ s with ∃ (h : x ∈ s), a x sorry, f x) (∏ x ∈ s with ∃ (h : x ∈ s), ¬a x sorry, 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: simp only [prod_ite, filter_attach', prod_map, Function.Embedding.coeFn_mk,
            Subtype.map_coe, id_eq, prod_attach]
-- 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
⊢ 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)
have e_a : ∀ (x : ι), x ∈ {x ∈ s | ∃ (h : x ∈ s), ¬a x sorry} ↔ x ∈ s \ {a_1 ∈ s | ∃ (h : a_1 ∈ s), a a_1 h}
Tactic: congr 2 with x
-- 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 : ι
⊢ x ∈ {x ∈ s | ∃ (h : x ∈ s), ¬a x ⋯} ↔ x ∈ s \ {a_1 ∈ s | ∃ (h : a_1 ∈ s), a a_1 h}
have e_a : x ∈ s → ((∃ (h : x ∈ s), ¬a x sorry) ↔ x ∈ s → ∀ (x_1 : x ∈ s), ¬a x x_1)
Tactic: simp only [mem_filter, mem_sdiff, not_and, not_exists, and_congr_right_iff]
-- 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)
⊢ x ∈ s → ((∃ (h : x ∈ s), ¬a x ⋯) ↔ x ∈ s → ∀ (x_1 : x ∈ s), ¬a x x_1)
have e_a₂ : x ∈ s → (∃ (h : 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
⊢ x ∈ s → ((∃ (h : x ∈ s), ¬a x ⋯) ↔ x ∈ s → ∀ (x_1 : x ∈ s), ¬a x x_1)
have e_a₃ : x ∈ s → (x ∈ s → ∀ (x_1 : x ∈ s), ¬a x x_1) → ∃ (h : x ∈ s), ¬a x sorry
Tactic: tauto