awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
Goal:
ι : Type u_2
γ : Type u_3
B : Type u_5
inst : AddCommMonoid B
A : Type u_16
F : Type u_17
inst_1 : AddZeroClass A
inst_2 : AddCommMonoid F
inst_3 : FunLike F γ B
g : ι →₀ A
k : ι → A → F
x : γ
h0 : Eq.{u_5 + 1} (α := B) ((0 : (a : γ) → B) x : B) (0 : B)
hadd :
  ∀ (f g : F), (f + g : (a : γ) → B) x = HAdd.hAdd (α := B) (β := B) ((f : (a : γ) → B) x : B) ((g : (a : γ) → B) x : B)
⊢ Eq.{u_5 + 1} (α := B) ((∑ a ∈ g.support, k a ((g : (a : ι) → A) a) : (a : γ) → B) x : B)
    (∑ a ∈ g.support, (fun (i : ι) (a : A) ↦ ((k i a : (a : γ) → B) x : B)) a ((g : (a : ι) → A) a) : B)
have induction : ∀ (x_1 : Finset ι),
  Eq.{u_5 + 1} (α := B) ((∑ a ∈ x_1, k a ((g : (a : ι) → A) a) : (a : γ) → B) x : B)
    (∑ a ∈ x_1, (fun (i : ι) (a : A) ↦ ((k i a : (a : γ) → B) x : B)) a ((g : (a : ι) → A) a) : B)
Tactic: induction g.support using Finset.induction with
  | empty => simp [h0]
  | insert i s hi ih => simp [sum_insert hi, hadd, ih]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
Goal:
ι : Type u_2
γ : Type u_3
B : Type u_5
inst : AddCommMonoid B
A : Type u_16
F : Type u_17
inst_1 : AddZeroClass A
inst_2 : AddCommMonoid F
inst_3 : FunLike F γ B
g : ι →₀ A
k : ι → A → F
x : γ
h0 : Eq.{u_5 + 1} (α := B) ((0 : (a : γ) → B) x : B) (0 : B)
hadd :
  ∀ (f g : F), (f + g : (a : γ) → B) x = HAdd.hAdd (α := B) (β := B) ((f : (a : γ) → B) x : B) ((g : (a : γ) → B) x : B)
⊢ Eq.{u_5 + 1} (α := B) ((g.sum k : (a : γ) → B) x : B) (g.sum fun (i : ι) (a : A) ↦ (k i a : (a : γ) → B) x : B)
have unfold : Eq.{u_5 + 1} (α := B) ((∑ a ∈ g.support, k a ((g : (a : ι) → A) a) : (a : γ) → B) x : B)
  (∑ a ∈ g.support, (fun (i : ι) (a : A) ↦ ((k i a : (a : γ) → B) x : B)) a ((g : (a : ι) → A) a) : B)
Tactic: classical
  unfold Finsupp.sum
  induction g.support using Finset.induction with
  | empty => simp [h0]
  | insert i s hi ih => simp [sum_insert hi, hadd, ih]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (hypothesis)
Goal:
f : ℕ →₀ ℕ
nhf : 0 ∉ f.support
x : ℕ
hf : x ∈ f.support
H : x = 0
⊢ False
have hf₁ : 0 ∈ f.support
Tactic: subst H
Cleared hypotheses: x, hf, H
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Fin (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
n : ℕ
σ : Fin n →₀ M
i : M
⊢ ((cons i σ).sum fun (x : Fin (n + 1)) (e : M) ↦ e) = i + σ.sum fun (x : Fin n) (e : M) ↦ e
have rw : ∑ i_1 : Fin (n + 1), (cons i σ : (a : Fin (n + 1)) → M) i_1 = i + ∑ i : Fin n, (σ : (a : Fin n) → M) i
Tactic: rw [sum_fintype _ _ (fun _ => rfl), sum_fintype _ _ (fun _ => rfl)]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Fin (goal)
Goal:
M : Type u_1
N : Type u_2
inst : Zero M
inst_1 : AddCommMonoid N
n : ℕ
σ : Fin n →₀ M
i : M
f : Fin (n + 1) → M → N
h : ∀ (x : Fin (n + 1)), f x 0 = 0
⊢ (cons i σ).sum f = f 0 i + σ.sum (Fin.tail (α := fun (i : Fin (n + 1)) ↦ M → N) f)
have rw : ∑ i_1 : Fin (n + 1), f i_1 ((cons i σ : (a : Fin (n + 1)) → M) i_1) =
  f 0 i + ∑ i : Fin n, Fin.tail (α := fun (i : Fin (n + 1)) ↦ M → N) f i ((σ : (a : Fin n) → M) i)
Tactic: rw [sum_fintype _ _ (fun _ => by apply h), sum_fintype _ _ (fun _ => by apply h)]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Fin (goal)
Goal:
M : Type u_1
N : Type u_2
inst : Zero M
inst_1 : AddCommMonoid N
n : ℕ
σ : Fin n →₀ M
i : M
f : Fin (n + 1) → M → N
h : ∀ (x : Fin (n + 1)), f x 0 = 0
⊢ ∑ i_1 : Fin (n + 1), f i_1 ((cons i σ : (a : Fin (n + 1)) → M) i_1) =
    f 0 i + ∑ i : Fin n, Fin.tail (α := fun (i : Fin (n + 1)) ↦ M → N) f i ((σ : (a : Fin n) → M) i)
have simp_rw : f 0 i + ∑ x : Fin n, f x.succ ((σ : (a : Fin n) → M) x) =
  f 0 i + ∑ i : Fin n, Fin.tail (α := fun (i : Fin (n + 1)) ↦ M → N) f i ((σ : (a : Fin n) → M) i)
Tactic: simp_rw [Fin.sum_univ_succ, cons_zero, cons_succ]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Fin (goal)
Goal:
n : Fin 2 →₀ ℕ
⊢ ofSupportFinite ![(n : (a : Fin 2) → ℕ) 0, (n : (a : Fin 2) → ℕ) 1] ⋯ = n
have rw : Eq (α := ℕ)
    (((ofSupportFinite ![(n : (a : Fin 2) → ℕ) 0, (n : (a : Fin 2) → ℕ) 1] sorry : Fin (Nat.succ 0).succ →₀ ℕ) :
          (a : Fin (Nat.succ 0).succ) → ℕ)
        0 :
      ℕ)
    ((n : (a : Fin (Nat.succ 0).succ) → ℕ) 0 : ℕ) ∧
  Eq (α := ℕ)
    (((ofSupportFinite ![(n : (a : Fin 2) → ℕ) 0, (n : (a : Fin 2) → ℕ) 1] sorry : Fin (Nat.succ 0).succ →₀ ℕ) :
          (a : Fin (Nat.succ 0).succ) → ℕ)
        1 :
      ℕ)
    ((n : (a : Fin (Nat.succ 0).succ) → ℕ) 1 : ℕ)
Tactic: rw [Finsupp.ext_iff, Fin.forall_fin_two]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Fin (goal)
Goal:
M : Type u_1
d : M × M
inst : AddCommMonoid M
⊢ (Finsupp.sum ((Equiv.symm (finTwoArrowEquiv' M) : (a : M × M) → Fin 2 →₀ M) d) fun (x : Fin 2) (n : M) ↦ n) =
    d.1 + d.2
have apply : ∑ a : Fin 2, ((finTwoArrowEquiv M).symm : (a : M × M) → Fin 2 → M) d a = d.1 + d.2
Tactic: apply (Finsupp.equivFunOnFinite_symm_sum _).trans
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
s : Finset ι
a : ι
inst : CommMonoid M
h : a ∉ s
⊢ Eq (α := (f : ι → M) → M) (cons a s h).prod fun (f : ι → M) ↦ f a * ∏ x ∈ s, f x
have h₁ : ∀ (f : ι → M), (cons a s h).prod f = f a * ∏ x ∈ s, f x
Tactic: funext f
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
s : Finset ι
a : ι
inst : CommMonoid M
h : a ∉ s
f : ι → M
⊢ (cons a s h).prod f = f a * ∏ x ∈ s, f x
have h₁ : f a * ∏ x ∈ s, f x = f a * ∏ x ∈ s, f x
Tactic: rw [Finset.prod_cons h]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
s : Finset ι
a : ι
inst : CommMonoid M
inst_1 : DecidableEq ι
h : a ∉ s
⊢ Eq (α := (f : ι → M) → M) (insert a s).prod fun (f : ι → M) ↦ f a * ∏ x ∈ s, f x
have h₁ : ∀ (f : ι → M), (insert a s).prod f = f a * ∏ x ∈ s, f x
Tactic: funext f
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
s : Finset ι
a : ι
inst : CommMonoid M
inst_1 : DecidableEq ι
h : a ∉ s
f : ι → M
⊢ (insert a s).prod f = f a * ∏ x ∈ s, f x
have h₁ : f a * ∏ x ∈ s, f x = f a * ∏ x ∈ s, f x
Tactic: rw [Finset.prod_insert h]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
s : Finset ι
a : ι
inst : CommMonoid M
f : ι → M
inst_1 : DecidableEq ι
h : a ∉ s → f a = 1
⊢ Eq.{u_4 + 1} (α := M) (∏ x ∈ insert a s, f x) (∏ x ∈ s, f x)
have pos : a ∈ s → Eq.{u_4 + 1} (α := M) (∏ x ∈ insert a s, f x) (∏ x ∈ s, f x)
Tactic: by_cases a ∈ s
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
s : Finset ι
a : ι
inst : CommMonoid M
f : ι → M
inst_1 : DecidableEq ι
h : a ∉ s → f a = 1
pos : a ∈ s → Eq.{u_4 + 1} (α := M) (∏ x ∈ insert a s, f x) (∏ x ∈ s, f x)
⊢ Eq.{u_4 + 1} (α := M) (∏ x ∈ insert a s, f x) (∏ x ∈ s, f x)
have neg : a ∉ s → Eq.{u_4 + 1} (α := M) (∏ x ∈ insert a s, f x) (∏ x ∈ s, f x)
Tactic: by_cases a ∈ s
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
a : ι
⊢ Eq (α := (f : ι → M) → M) (Finset.prod {a}) fun (f : ι → M) ↦ f a
have h : ∀ (f : ι → M), Finset.prod {a} f = f a
Tactic: funext f
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
f : ι → M
inst_1 : DecidableEq ι
a b : ι
h : a ≠ b
⊢ ∏ x ∈ {a, b}, f x = f a * f b
have rw : f a * ∏ x ∈ {b}, f x = f a * f b
Tactic: rw [prod_insert (notMem_singleton.2 h), prod_singleton]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
f : ι → M
inst_1 : DecidableEq ι
a b : ι
h : a ≠ b
rw : f a * ∏ x ∈ {b}, f x = f a * f b
⊢ ∏ x ∈ {a, b}, f x = f a * f b
have rw₁ : f a * f b = f a * f b
Tactic: rw [prod_insert (notMem_singleton.2 h), prod_singleton]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
s : Finset ι
f : ι → M
⊢ Eq.{u_4 + 1} (α := M) (∏ x ∈ s.attach, f (↑x : ι)) (∏ x ∈ s, f x)
have rw : Eq.{u_4 + 1} (α := M) (∏ x ∈ image (fun (a : ↥s) ↦ (↑a : ι)) s.attach, f x) (∏ x ∈ s, f x)
Tactic: rw [← prod_image Subtype.coe_injective.injOn, attach_image_val]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
s : Finset ι
f : ι → M
rw : Eq.{u_4 + 1} (α := M) (∏ x ∈ image (fun (a : ↥s) ↦ (↑a : ι)) s.attach, f x) (∏ x ∈ s, f x)
⊢ Eq.{u_4 + 1} (α := M) (∏ x ∈ s.attach, f (↑x : ι)) (∏ x ∈ s, f x)
have rw₁ : Eq.{u_4 + 1} (α := M) (∏ x ∈ s, f x) (∏ x ∈ s, f x)
Tactic: rw [← prod_image Subtype.coe_injective.injOn, attach_image_val]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
s : Finset ι
f : ι → M
⊢ Eq.{u_4 + 1} (α := M) (∏ x ∈ s.attach, f (↑x : ι)) (∏ x ∈ s, f x)
have classical : Eq.{u_4 + 1} (α := M) (∏ x ∈ image (fun (a : ↥s) ↦ (↑a : ι)) s.attach, f x) (∏ x ∈ s, f x)
Tactic: classical rw [← prod_image Subtype.coe_injective.injOn, attach_image_val]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
s : Finset ι
f : ι → M
classical : Eq.{u_4 + 1} (α := M) (∏ x ∈ image (fun (a : ↥s) ↦ (↑a : ι)) s.attach, f x) (∏ x ∈ s, f x)
⊢ Eq.{u_4 + 1} (α := M) (∏ x ∈ s.attach, f (↑x : ι)) (∏ x ∈ s, f x)
have classical₁ : Eq.{u_4 + 1} (α := M) (∏ x ∈ s, f x) (∏ x ∈ s, f x)
Tactic: classical rw [← prod_image Subtype.coe_injective.injOn, attach_image_val]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
s₁ s₂ : Finset ι
inst : CommMonoid M
f g : ι → M
h : s₁ = s₂
⊢ (∀ x ∈ s₂, f x = g x) → s₁.prod f = s₂.prod g
have rw : (∀ x ∈ s₂, f x = g x) → s₂.prod f = s₂.prod g
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
s : Finset ι
inst : CommMonoid M
f : ι → M
inst_1 : Subsingleton.{u_4 + 1} Mˣ
⊢ Eq.{u_4 + 1} (α := M) (∏ i ∈ s, f i) 1 ↔ ∀ i ∈ s, f i = 1
have empty : Eq.{u_4 + 1} (α := M) (∏ i ∈ ∅, f i) 1 ↔ ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → f i = 1
Tactic: induction s using Finset.cons_induction
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
s : Finset ι
inst : CommMonoid M
f : ι → M
inst_1 : Subsingleton.{u_4 + 1} Mˣ
empty : Eq.{u_4 + 1} (α := M) (∏ i ∈ ∅, f i) 1 ↔ ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → f i = 1
⊢ Eq.{u_4 + 1} (α := M) (∏ i ∈ s, f i) 1 ↔ ∀ i ∈ s, f i = 1
have cons : ∀ (a : ι) (s : Finset ι) (h : a ∉ s),
  (Eq.{u_4 + 1} (α := M) (∏ i ∈ s, f i) 1 ↔ ∀ i ∈ s, f i = 1) →
    (Eq.{u_4 + 1} (α := M) (∏ i ∈ cons a s h, f i) 1 ↔ ∀ i ∈ cons a s h, f i = 1)
Tactic: induction s using Finset.cons_induction
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
s₁ s₂ : Finset ι
inst : CommMonoid M
f : ι → M
h : Disjoint s₁ s₂
⊢ ∏ x ∈ s₁.disjUnion s₂ h, f x = HMul.hMul (α := M) (∏ x ∈ s₁, f x) (∏ x ∈ s₂, f x)
have refine : ∏ x ∈ s₁.disjUnion s₂ h, f x =
  fold (fun (x1 x2 : M) ↦ x1 * x2) (HMul.hMul (α := M) 1 1) (fun (x : ι) ↦ f x) (s₁.disjUnion s₂ h)
Tactic: refine Eq.trans ?_ (fold_disjUnion h)
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
s₁ s₂ : Finset ι
inst : CommMonoid M
f : ι → M
h : Disjoint s₁ s₂
⊢ ∏ x ∈ s₁.disjUnion s₂ h, f x =
    fold (fun (x1 x2 : M) ↦ x1 * x2) (HMul.hMul (α := M) 1 1) (fun (x : ι) ↦ f x) (s₁.disjUnion s₂ h)
have rw : Eq.{u_4 + 1} (α := M) (∏ x ∈ s₁.disjUnion s₂ h, f x)
  (fold (fun (x1 x2 : M) ↦ x1 * x2) 1 (fun (x : ι) ↦ f x) (s₁.disjUnion s₂ h))
Tactic: rw [one_mul]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst : CommMonoid M
f : ι → M
s : Finset κ
t : κ → Finset ι
h : (↑s : Set κ).PairwiseDisjoint t
⊢ Eq.{u_4 + 1} (α := M) (∏ x ∈ s.disjiUnion t h, f x) (∏ i ∈ s, ∏ x ∈ t i, f x)
have refine : Eq.{u_4 + 1} (α := M) (∏ x ∈ s.disjiUnion t h, f x)
  (fold (fun (x1 x2 : M) ↦ x1 * x2) (fold (fun (x1 x2 : M) ↦ x1 * x2) 1 (fun (i : κ) ↦ 1) s) (fun (x : ι) ↦ f x)
    (s.disjiUnion t h))
Tactic: refine Eq.trans ?_ (fold_disjiUnion h)
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst : CommMonoid M
f : ι → M
s : Finset κ
t : κ → Finset ι
h : (↑s : Set κ).PairwiseDisjoint t
⊢ Eq.{u_4 + 1} (α := M) (∏ x ∈ s.disjiUnion t h, f x)
    (fold (fun (x1 x2 : M) ↦ x1 * x2) (fold (fun (x1 x2 : M) ↦ x1 * x2) 1 (fun (i : κ) ↦ 1) s) (fun (x : ι) ↦ f x)
      (s.disjiUnion t h))
have dsimp : Eq.{u_4 + 1} (α := M)
  (Multiset.foldr (fun (x1 x2 : M) ↦ x1 * x2) 1 (Multiset.map (fun (x : ι) ↦ f x) (s.val.bind fun (a : κ) ↦ (t a).val)))
  (Multiset.foldr (fun (x1 x2 : M) ↦ x1 * x2)
    (Multiset.foldr (fun (x1 x2 : M) ↦ x1 * x2) 1 (Multiset.map (fun (i : κ) ↦ 1) s.val))
    (Multiset.map (fun (x : ι) ↦ f x) (s.val.bind fun (a : κ) ↦ (t a).val)))
Tactic: dsimp [Finset.prod, Multiset.prod, Multiset.fold, Finset.disjUnion, Finset.fold]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst : CommMonoid M
f : ι → M
s : Finset κ
t : κ → Finset ι
h : (↑s : Set κ).PairwiseDisjoint t
⊢ Eq.{u_4 + 1} (α := M)
    (Multiset.foldr (fun (x1 x2 : M) ↦ x1 * x2) 1
      (Multiset.map (fun (x : ι) ↦ f x) (s.val.bind fun (a : κ) ↦ (t a).val)))
    (Multiset.foldr (fun (x1 x2 : M) ↦ x1 * x2)
      (Multiset.foldr (fun (x1 x2 : M) ↦ x1 * x2) 1 (Multiset.map (fun (i : κ) ↦ 1) s.val))
      (Multiset.map (fun (x : ι) ↦ f x) (s.val.bind fun (a : κ) ↦ (t a).val)))
have e_b : Eq.{u_4 + 1} (α := M) 1 (Multiset.foldr (fun (x1 x2 : M) ↦ x1 * x2) 1 (Multiset.map (fun (i : κ) ↦ 1) s.val))
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
s₁ s₂ : Finset ι
inst : CommMonoid M
f : ι → M
inst_1 : DecidableEq ι
h : Disjoint s₁ s₂
⊢ ∏ x ∈ s₁ ∪ s₂, f x = HMul.hMul (α := M) (∏ x ∈ s₁, f x) (∏ x ∈ s₂, f x)
have rw : ∏ x ∈ s₁ ∪ s₂, f x = HMul.hMul (α := M) (∏ x ∈ s₁ ∪ s₂, f x) (∏ x ∈ ∅, f x)
Tactic: rw [← prod_union_inter, disjoint_iff_inter_eq_empty.mp h]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
s : Finset ι
p : ι → Prop
inst_1 : DecidablePred p
inst_2 : (x : ι) → Decidable ¬p x
f : ι → M
⊢ HMul.hMul (α := M) (∏ x ∈ s with p x, f x) (∏ x ∈ s with ¬p x, f x) = ∏ x ∈ s, f x
have have : ∀ (this : DecidableEq ι), HMul.hMul (α := M) (∏ x ∈ s with p x, f x) (∏ x ∈ s with ¬p x, f x) = ∏ x ∈ s, f x
Tactic: have := Classical.decEq ι
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
s : Finset ι
p : ι → Prop
inst_1 : DecidablePred p
inst_2 : (x : ι) → Decidable ¬p x
f : ι → M
this : DecidableEq ι
⊢ HMul.hMul (α := M) (∏ x ∈ s with p x, f x) (∏ x ∈ s with ¬p x, f x) = ∏ x ∈ s, f x
have rw : Eq.{u_4 + 1} (α := M) (∏ x ∈ filter p s ∪ {a ∈ s | ¬p a}, f x) (∏ x ∈ s, f x)
Tactic: rw [← prod_union (disjoint_filter_filter_not s s p), filter_union_filter_not_eq]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
s : Finset ι
p : ι → Prop
inst_1 : DecidablePred p
inst_2 : (x : ι) → Decidable ¬p x
f : ι → M
this : DecidableEq ι
rw : Eq.{u_4 + 1} (α := M) (∏ x ∈ filter p s ∪ {a ∈ s | ¬p a}, f x) (∏ x ∈ s, f x)
⊢ HMul.hMul (α := M) (∏ x ∈ s with p x, f x) (∏ x ∈ s with ¬p x, f x) = ∏ x ∈ s, f x
have rw₁ : Eq.{u_4 + 1} (α := M) (∏ x ∈ s, f x) (∏ x ∈ s, f x)
Tactic: rw [← prod_union (disjoint_filter_filter_not s s p), filter_union_filter_not_eq]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
s : Finset ι
p : ι → Prop
inst_1 : DecidablePred p
inst_2 : (x : ι) → Decidable ¬p x
f : ι → M
⊢ HMul.hMul (α := M) (∏ x ∈ s with ¬p x, f x) (∏ x ∈ s with p x, f x) = ∏ x ∈ s, f x
have rw : HMul.hMul (α := M) (∏ x ∈ s with p x, f x) (∏ x ∈ s with ¬p x, f x) = ∏ x ∈ s, f x
Tactic: rw [mul_comm, prod_filter_mul_prod_filter_not]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
s : Finset ι
p : ι → Prop
inst_1 : DecidablePred p
inst_2 : (x : ι) → Decidable ¬p x
f : ι → M
rw : HMul.hMul (α := M) (∏ x ∈ s with p x, f x) (∏ x ∈ s with ¬p x, f x) = ∏ x ∈ s, f x
⊢ HMul.hMul (α := M) (∏ x ∈ s with ¬p x, f x) (∏ x ∈ s with p x, f x) = ∏ x ∈ s, f x
have rw₁ : Eq.{u_4 + 1} (α := M) (∏ x ∈ s, f x) (∏ x ∈ s, f x)
Tactic: rw [mul_comm, prod_filter_mul_prod_filter_not]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
s : Finset ι
inst : CommMonoid M
f : ι → M
p q : ι → Prop
inst_1 : DecidablePred p
inst_2 : DecidablePred q
⊢ ∏ x ∈ s with Xor (p x) (q x), f x = HMul.hMul (α := M) (∏ x ∈ s with p x ∧ ¬q x, f x) (∏ x ∈ s with q x ∧ ¬p x, f x)
have rw : Eq.{u_4 + 1} (α := M) (∏ x ∈ s with Xor (p x) (q x), f x) (∏ x ∈ s with p x ∧ ¬q x ∨ q x ∧ ¬p x, f x)
Tactic: rw [← prod_union (disjoint_filter_and_not_filter _ _), ← filter_or]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
s : Finset ι
inst : CommMonoid M
f : ι → M
p q : ι → Prop
inst_1 : DecidablePred p
inst_2 : DecidablePred q
⊢ ∏ x ∈ s with Xor (p x) (q x), f x = HMul.hMul (α := M) (∏ x ∈ s with p x ∧ ¬q x, f x) (∏ x ∈ s with q x ∧ ¬p x, f x)
have classical : Eq.{u_4 + 1} (α := M) (∏ x ∈ s with Xor (p x) (q x), f x) (∏ x ∈ s with p x ∧ ¬q x ∨ q x ∧ ¬p x, f x)
Tactic: classical rw [← prod_union (disjoint_filter_and_not_filter _ _), ← filter_or]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
inst_1 : Fintype ι
s t : Finset ι
h : IsCompl s t
f : ι → M
⊢ Eq.{u_4 + 1} (α := M) (∏ x ∈ s.disjUnion t ⋯, f x) (∏ i : ι, f i)
have rw : Eq.{u_4 + 1} (α := M) (∏ x ∈ ⊤, f x) (∏ i : ι, f i)
Tactic: rw [Finset.disjUnion_eq_union, ← Finset.sup_eq_union, h.sup_eq_top]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
inst_1 : Fintype ι
s t : Finset ι
h : IsCompl s t
f : ι → M
⊢ Eq.{u_4 + 1} (α := M) (∏ x ∈ s.disjUnion t ⋯, f x) (∏ i : ι, f i)
have classical : Eq.{u_4 + 1} (α := M) (∏ x ∈ s ∪ t, f x) (∏ i : ι, f i)
Tactic: classical rw [Finset.disjUnion_eq_union, ← Finset.sup_eq_union, h.sup_eq_top]; rfl
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
inst_1 : Fintype ι
s t : Finset ι
h : IsCompl s t
f : ι → M
classical : Eq.{u_4 + 1} (α := M) (∏ x ∈ s ∪ t, f x) (∏ i : ι, f i)
⊢ Eq.{u_4 + 1} (α := M) (∏ x ∈ s.disjUnion t ⋯, f x) (∏ i : ι, f i)
have classical₁ : Eq.{u_4 + 1} (α := M) (∏ x ∈ s ⊔ t, f x) (∏ i : ι, f i)
Tactic: classical rw [Finset.disjUnion_eq_union, ← Finset.sup_eq_union, h.sup_eq_top]; rfl
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
inst_1 : Fintype ι
s t : Finset ι
h : IsCompl s t
f : ι → M
classical : Eq.{u_4 + 1} (α := M) (∏ x ∈ s ∪ t, f x) (∏ i : ι, f i)
classical₁ : Eq.{u_4 + 1} (α := M) (∏ x ∈ s ⊔ t, f x) (∏ i : ι, f i)
⊢ Eq.{u_4 + 1} (α := M) (∏ x ∈ s.disjUnion t ⋯, f x) (∏ i : ι, f i)
have classical₂ : Eq.{u_4 + 1} (α := M) (∏ x ∈ ⊤, f x) (∏ i : ι, f i)
Tactic: classical rw [Finset.disjUnion_eq_union, ← Finset.sup_eq_union, h.sup_eq_top]; rfl
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
s₁ s₂ : Finset ι
inst : CommMonoid M
f : ι → M
inst_1 : DecidableEq ι
h : s₁ ⊆ s₂
⊢ HMul.hMul (α := M) (∏ x ∈ s₂ \ s₁, f x) (∏ x ∈ s₁, f x) = ∏ x ∈ s₂, f x
have rw : Eq.{u_4 + 1} (α := M) (∏ x ∈ s₂ \ s₁ ∪ s₁, f x) (∏ x ∈ s₂, f x)
Tactic: rw [← prod_union sdiff_disjoint, sdiff_union_of_subset h]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
s₁ s₂ : Finset ι
inst : CommMonoid M
f : ι → M
inst_1 : DecidableEq ι
h : s₁ ⊆ s₂
rw : Eq.{u_4 + 1} (α := M) (∏ x ∈ s₂ \ s₁ ∪ s₁, f x) (∏ x ∈ s₂, f x)
⊢ HMul.hMul (α := M) (∏ x ∈ s₂ \ s₁, f x) (∏ x ∈ s₁, f x) = ∏ x ∈ s₂, f x
have rw₁ : Eq.{u_4 + 1} (α := M) (∏ x ∈ s₂, f x) (∏ x ∈ s₂, f x)
Tactic: rw [← prod_union sdiff_disjoint, sdiff_union_of_subset h]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
s₁ s₂ : Finset ι
inst : CommMonoid M
f g : ι → M
inst_1 : DecidableEq ι
h : s₁ ⊆ s₂
hg : ∀ x ∈ s₂ \ s₁, g x = 1
hfg : ∀ x ∈ s₁, f x = g x
⊢ Eq.{u_4 + 1} (α := M) (∏ i ∈ s₁, f i) (∏ i ∈ s₂, g i)
have rw : Eq.{u_4 + 1} (α := M) (∏ i ∈ s₁, f i) (∏ x ∈ s₁, g x)
Tactic: rw [← prod_sdiff h, prod_eq_one hg, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst : CommMonoid M
s : Finset ι
t : Finset κ
f : ι ⊕ κ → M
⊢ ∏ x ∈ s.disjSum t, f x = HMul.hMul (α := M) (∏ x ∈ s, f (Sum.inl x)) (∏ x ∈ t, f (Sum.inr x))
have rw : HMul.hMul (α := M) (∏ x ∈ s, f ((Embedding.inl : (a : ι) → ι ⊕ κ) x))
    (∏ x ∈ t, f ((Embedding.inr : (a : κ) → ι ⊕ κ) x)) =
  HMul.hMul (α := M) (∏ x ∈ s, f (Sum.inl x)) (∏ x ∈ t, f (Sum.inr x))
Tactic: rw [← map_inl_disjUnion_map_inr, prod_disjUnion, prod_map, prod_map]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst : CommMonoid M
s : Finset (ι ⊕ κ)
f : ι ⊕ κ → M
⊢ ∏ x ∈ s, f x = HMul.hMul (α := M) (∏ x ∈ s.toLeft, f (Sum.inl x)) (∏ x ∈ s.toRight, f (Sum.inr x))
have rw : ∏ x ∈ s.toLeft.disjSum s.toRight, f x =
  HMul.hMul (α := M) (∏ x ∈ (s.toLeft.disjSum s.toRight).toLeft, f (Sum.inl x))
    (∏ x ∈ (s.toLeft.disjSum s.toRight).toRight, f (Sum.inr x))
Tactic: rw [← Finset.toLeft_disjSum_toRight (u := s), Finset.prod_disjSum, Finset.toLeft_disjSum,
    Finset.toRight_disjSum]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst : CommMonoid M
s : Finset (ι ⊕ κ)
f : ι ⊕ κ → M
rw :
  ∏ x ∈ s.toLeft.disjSum s.toRight, f x =
    HMul.hMul (α := M) (∏ x ∈ (s.toLeft.disjSum s.toRight).toLeft, f (Sum.inl x))
      (∏ x ∈ (s.toLeft.disjSum s.toRight).toRight, f (Sum.inr x))
⊢ ∏ x ∈ s, f x = HMul.hMul (α := M) (∏ x ∈ s.toLeft, f (Sum.inl x)) (∏ x ∈ s.toRight, f (Sum.inr x))
have rw₁ : HMul.hMul (α := M) (∏ x ∈ s.toLeft, f (Sum.inl x)) (∏ x ∈ s.toRight, f (Sum.inr x)) =
  HMul.hMul (α := M) (∏ x ∈ (s.toLeft.disjSum s.toRight).toLeft, f (Sum.inl x))
    (∏ x ∈ (s.toLeft.disjSum s.toRight).toRight, f (Sum.inr x))
Tactic: rw [← Finset.toLeft_disjSum_toRight (u := s), Finset.prod_disjSum, Finset.toLeft_disjSum,
    Finset.toRight_disjSum]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst : CommMonoid M
s : Finset (ι ⊕ κ)
f : ι ⊕ κ → M
rw :
  ∏ x ∈ s.toLeft.disjSum s.toRight, f x =
    HMul.hMul (α := M) (∏ x ∈ (s.toLeft.disjSum s.toRight).toLeft, f (Sum.inl x))
      (∏ x ∈ (s.toLeft.disjSum s.toRight).toRight, f (Sum.inr x))
rw₁ :
  HMul.hMul (α := M) (∏ x ∈ s.toLeft, f (Sum.inl x)) (∏ x ∈ s.toRight, f (Sum.inr x)) =
    HMul.hMul (α := M) (∏ x ∈ (s.toLeft.disjSum s.toRight).toLeft, f (Sum.inl x))
      (∏ x ∈ (s.toLeft.disjSum s.toRight).toRight, f (Sum.inr x))
⊢ ∏ x ∈ s, f x = HMul.hMul (α := M) (∏ x ∈ s.toLeft, f (Sum.inl x)) (∏ x ∈ s.toRight, f (Sum.inr x))
have rw₂ : HMul.hMul (α := M) (∏ x ∈ s.toLeft, f (Sum.inl x)) (∏ x ∈ s.toRight, f (Sum.inr x)) =
  HMul.hMul (α := M) (∏ x ∈ s.toLeft, f (Sum.inl x)) (∏ x ∈ (s.toLeft.disjSum s.toRight).toRight, f (Sum.inr x))
Tactic: rw [← Finset.toLeft_disjSum_toRight (u := s), Finset.prod_disjSum, Finset.toLeft_disjSum,
    Finset.toRight_disjSum]