awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
inst_1 : DecidableEq ι
inst_2 : PartialOrder ι
inst_3 : OrderBot ι
f : κ → ι
g : ι → M
hg_bot : g ⊥ = 1
I : Finset κ
hf_disj : (↑I : Set κ).PairwiseDisjoint f
i j : κ
hdisj : f i = ⊥
hfij : f i = f j
rw : g ⊥ = 1
⊢ g (f i) = 1
have rw₁ : Eq.{u_4 + 1} (α := M) 1 1
Tactic: rw [hdisj, hg_bot]
-- 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 : Unique ι
s : Finset ι
f : ι → M
h : s.Nonempty
⊢ ∏ x ∈ s, f x = f default
have rw : ∏ x ∈ {default}, f x = f default
Tactic: rw [h.eq_singleton_default, Finset.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
inst_1 : Unique ι
s : Finset ι
f : ι → M
h : s.Nonempty
rw : ∏ x ∈ {default}, f x = f default
⊢ ∏ x ∈ s, f x = f default
have rw₁ : f default = f default
Tactic: rw [h.eq_singleton_default, Finset.prod_singleton]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
inst : DecidableEq ι
inst_1 : CancelCommMonoid M
s t : Finset ι
f : ι → M
⊢ HMul.hMul (α := M) (∏ i ∈ t \ s, f i) (∏ i ∈ s, f i) = HMul.hMul (α := M) (∏ i ∈ s \ t, f i) (∏ i ∈ t, f i)
have rw : ∏ x ∈ t \ s ∪ s, f x = HMul.hMul (α := M) (∏ i ∈ s \ t, f i) (∏ i ∈ t, f i)
Tactic: rw [← prod_union disjoint_sdiff_self_left, ← prod_union disjoint_sdiff_self_left,
      sdiff_union_self_eq_union, sdiff_union_self_eq_union, union_comm]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
inst : DecidableEq ι
inst_1 : CancelCommMonoid M
s t : Finset ι
f : ι → M
rw : ∏ x ∈ t \ s ∪ s, f x = HMul.hMul (α := M) (∏ i ∈ s \ t, f i) (∏ i ∈ t, f i)
⊢ HMul.hMul (α := M) (∏ i ∈ t \ s, f i) (∏ i ∈ s, f i) = HMul.hMul (α := M) (∏ i ∈ s \ t, f i) (∏ i ∈ t, f i)
have rw₁ : Eq.{u_4 + 1} (α := M) (∏ x ∈ t \ s ∪ s, f x) (∏ x ∈ s \ t ∪ t, f x)
Tactic: rw [← prod_union disjoint_sdiff_self_left, ← prod_union disjoint_sdiff_self_left,
      sdiff_union_self_eq_union, sdiff_union_self_eq_union, union_comm]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
inst : DecidableEq ι
inst_1 : CancelCommMonoid M
s t : Finset ι
f : ι → M
rw : ∏ x ∈ t \ s ∪ s, f x = HMul.hMul (α := M) (∏ i ∈ s \ t, f i) (∏ i ∈ t, f i)
rw₁ : Eq.{u_4 + 1} (α := M) (∏ x ∈ t \ s ∪ s, f x) (∏ x ∈ s \ t ∪ t, f x)
⊢ HMul.hMul (α := M) (∏ i ∈ t \ s, f i) (∏ i ∈ s, f i) = HMul.hMul (α := M) (∏ i ∈ s \ t, f i) (∏ i ∈ t, f i)
have rw₂ : Eq.{u_4 + 1} (α := M) (∏ x ∈ t ∪ s, f x) (∏ x ∈ s \ t ∪ t, f x)
Tactic: rw [← prod_union disjoint_sdiff_self_left, ← prod_union disjoint_sdiff_self_left,
      sdiff_union_self_eq_union, sdiff_union_self_eq_union, union_comm]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
inst : DecidableEq ι
inst_1 : CancelCommMonoid M
s t : Finset ι
f : ι → M
rw : ∏ x ∈ t \ s ∪ s, f x = HMul.hMul (α := M) (∏ i ∈ s \ t, f i) (∏ i ∈ t, f i)
rw₁ : Eq.{u_4 + 1} (α := M) (∏ x ∈ t \ s ∪ s, f x) (∏ x ∈ s \ t ∪ t, f x)
rw₂ : Eq.{u_4 + 1} (α := M) (∏ x ∈ t ∪ s, f x) (∏ x ∈ s \ t ∪ t, f x)
⊢ HMul.hMul (α := M) (∏ i ∈ t \ s, f i) (∏ i ∈ s, f i) = HMul.hMul (α := M) (∏ i ∈ s \ t, f i) (∏ i ∈ t, f i)
have rw₃ : Eq.{u_4 + 1} (α := M) (∏ x ∈ t ∪ s, f x) (∏ x ∈ s ∪ t, f x)
Tactic: rw [← prod_union disjoint_sdiff_self_left, ← prod_union disjoint_sdiff_self_left,
      sdiff_union_self_eq_union, sdiff_union_self_eq_union, union_comm]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
inst : DecidableEq ι
inst_1 : CancelCommMonoid M
s t : Finset ι
f : ι → M
rw : ∏ x ∈ t \ s ∪ s, f x = HMul.hMul (α := M) (∏ i ∈ s \ t, f i) (∏ i ∈ t, f i)
rw₁ : Eq.{u_4 + 1} (α := M) (∏ x ∈ t \ s ∪ s, f x) (∏ x ∈ s \ t ∪ t, f x)
rw₂ : Eq.{u_4 + 1} (α := M) (∏ x ∈ t ∪ s, f x) (∏ x ∈ s \ t ∪ t, f x)
rw₃ : Eq.{u_4 + 1} (α := M) (∏ x ∈ t ∪ s, f x) (∏ x ∈ s ∪ t, f x)
⊢ HMul.hMul (α := M) (∏ i ∈ t \ s, f i) (∏ i ∈ s, f i) = HMul.hMul (α := M) (∏ i ∈ s \ t, f i) (∏ i ∈ t, f i)
have rw₄ : Eq.{u_4 + 1} (α := M) (∏ x ∈ s ∪ t, f x) (∏ x ∈ s ∪ t, f x)
Tactic: rw [← prod_union disjoint_sdiff_self_left, ← prod_union disjoint_sdiff_self_left,
      sdiff_union_self_eq_union, sdiff_union_self_eq_union, union_comm]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
G : Type u_3
s : Finset ι
inst : CommGroup G
inst_1 : DecidableEq ι
f : ι → G
a : ι
h : a ∈ s
⊢ ∏ x ∈ s.erase a, f x = (∏ x ∈ s, f x) / f a
have rw : (∏ x ∈ s.erase a, f x) * f a = ∏ x ∈ s, f x
Tactic: rw [eq_div_iff_mul_eq', prod_erase_mul _ _ h]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
G : Type u_3
s : Finset ι
inst : CommGroup G
inst_1 : DecidableEq ι
f : ι → G
a : ι
h : a ∈ s
rw : (∏ x ∈ s.erase a, f x) * f a = ∏ x ∈ s, f x
⊢ ∏ x ∈ s.erase a, f x = (∏ x ∈ s, f x) / f a
have rw₁ : Eq.{u_3 + 1} (α := G) (∏ x ∈ s, f x) (∏ x ∈ s, f x)
Tactic: rw [eq_div_iff_mul_eq', prod_erase_mul _ _ h]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
G : Type u_3
inst : CommGroup G
f : ℕ → G
n : ℕ
⊢ ∏ i ∈ range n, f (i + 1) / f i = f n / f 0
have base : f 0 / f 0 = 1
Tactic: apply prod_range_induction
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
G : Type u_3
inst : CommGroup G
f : ℕ → G
n : ℕ
base : f 0 / f 0 = 1
⊢ ∏ i ∈ range n, f (i + 1) / f i = f n / f 0
have step : ∀ k < n, f (k + 1) / f 0 = f k / f 0 * (f (k + 1) / f k)
Tactic: apply prod_range_induction
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
G : Type u_3
inst : CommGroup G
f : ℕ → G
n : ℕ
⊢ ∏ i ∈ range n, f i / f (i + 1) = f 0 / f n
have base : f 0 / f 0 = 1
Tactic: apply prod_range_induction
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
G : Type u_3
inst : CommGroup G
f : ℕ → G
n : ℕ
base : f 0 / f 0 = 1
⊢ ∏ i ∈ range n, f i / f (i + 1) = f 0 / f n
have step : ∀ k < n, f 0 / f (k + 1) = f 0 / f k * (f k / f (k + 1))
Tactic: apply prod_range_induction
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
G : Type u_3
inst : CommGroup G
f : ℕ → G
n : ℕ
⊢ f n = f 0 * ∏ i ∈ range n, f (i + 1) / f i
have rw : f n = f 0 * (f n / f 0)
Tactic: rw [prod_range_div, mul_div_cancel]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
G : Type u_3
inst : CommGroup G
f : ℕ → G
n : ℕ
rw : f n = f 0 * (f n / f 0)
⊢ f n = f 0 * ∏ i ∈ range n, f (i + 1) / f i
have rw₁ : f n = f n
Tactic: rw [prod_range_div, mul_div_cancel]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
G : Type u_3
inst : CommGroup G
f : ℕ → G
n : ℕ
| f n
have rw : f 0 * ∏ i ∈ range n, f (i + 1) / f i
Tactic: rw [Finset.eq_prod_range_div f]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
G : Type u_3
inst : CommGroup G
f : ℕ → G
n : ℕ
⊢ f n = ∏ i ∈ range (n + 1), if i = 0 then f 0 else f i / f (i - 1)
have conv_lhs : f 0 * ∏ i ∈ range n, f (i + 1) / f i = ∏ i ∈ range (n + 1), if i = 0 then f 0 else f i / f (i - 1)
Tactic: conv_lhs => rw [Finset.eq_prod_range_div f]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
G : Type u_3
s₁ s₂ : Finset ι
inst : CommGroup G
inst_1 : DecidableEq ι
f : ι → G
h : s₁ ⊆ s₂
⊢ ∏ x ∈ s₂ \ s₁, f x = HDiv.hDiv (α := G) (∏ x ∈ s₂, f x) (∏ x ∈ s₁, f x)
have rw : HMul.hMul (α := G) (∏ x ∈ s₂ \ s₁, f x) (∏ x ∈ s₁, f x) = ∏ x ∈ s₂, f x
Tactic: rw [eq_div_iff_mul_eq', prod_sdiff h]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
G : Type u_3
s₁ s₂ : Finset ι
inst : CommGroup G
inst_1 : DecidableEq ι
f : ι → G
h : s₁ ⊆ s₂
rw : HMul.hMul (α := G) (∏ x ∈ s₂ \ s₁, f x) (∏ x ∈ s₁, f x) = ∏ x ∈ s₂, f x
⊢ ∏ x ∈ s₂ \ s₁, f x = HDiv.hDiv (α := G) (∏ x ∈ s₂, f x) (∏ x ∈ s₁, f x)
have rw₁ : Eq.{u_3 + 1} (α := G) (∏ x ∈ s₂, f x) (∏ x ∈ s₂, f x)
Tactic: rw [eq_div_iff_mul_eq', prod_sdiff h]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
M : Type u_4
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : Sub M
inst_3 : OrderedSub M
inst_4 : AddLeftMono M
inst_5 : AddLeftReflectLE M
inst_6 : ExistsAddOfLE M
f : ℕ → M
h : Monotone f
n : ℕ
⊢ ∑ i ∈ range n, (f (i + 1) - f i) = f n - f 0
have apply : f 0 - f 0 = 0
Tactic: apply sum_range_induction
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
M : Type u_4
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : Sub M
inst_3 : OrderedSub M
inst_4 : AddLeftMono M
inst_5 : AddLeftReflectLE M
inst_6 : ExistsAddOfLE M
f : ℕ → M
h : Monotone f
n : ℕ
apply : f 0 - f 0 = 0
⊢ ∑ i ∈ range n, (f (i + 1) - f i) = f n - f 0
have apply₁ : ∀ k < n, f (k + 1) - f 0 = f k - f 0 + (f (k + 1) - f k)
Tactic: apply sum_range_induction
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
M : Type u_4
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : Sub M
inst_3 : OrderedSub M
inst_4 : AddLeftMono M
inst_5 : AddLeftReflectLE M
inst_6 : ExistsAddOfLE M
f : ℕ → M
h : Monotone f
n : ℕ
⊢ f 0 - f 0 = 0
have h₁ : f 0 = 0 + f 0
Tactic: apply tsub_eq_of_eq_add
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
M : Type u_4
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : Sub M
inst_3 : OrderedSub M
inst_4 : AddLeftMono M
inst_5 : AddLeftReflectLE M
inst_6 : ExistsAddOfLE M
f : ℕ → M
h : Monotone f
n : ℕ
⊢ f 0 = 0 + f 0
have h₁ : f 0 = f 0
Tactic: rw [zero_add]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (hypothesis)
Goal:
M : Type u_4
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : Sub M
inst_3 : OrderedSub M
inst_4 : AddLeftMono M
inst_5 : AddLeftReflectLE M
inst_6 : ExistsAddOfLE M
f : ℕ → M
h : Monotone f
n_1 n : ℕ
h_1 : n < n_1
⊢ f (n + 1) - f 0 = f n - f 0 + (f (n + 1) - f n)
have h₁ : f n ≤ f (n + 1)
Tactic: have h₁ : f n ≤ f (n + 1) := h (Nat.le_succ _)
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (hypothesis)
Goal:
M : Type u_4
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : Sub M
inst_3 : OrderedSub M
inst_4 : AddLeftMono M
inst_5 : AddLeftReflectLE M
inst_6 : ExistsAddOfLE M
f : ℕ → M
h : Monotone f
n_1 n : ℕ
h_1 : n < n_1
h₁ : f n ≤ f (n + 1)
⊢ f (n + 1) - f 0 = f n - f 0 + (f (n + 1) - f n)
have h₂ : f 0 ≤ f n
Tactic: have h₂ : f 0 ≤ f n := h (Nat.zero_le _)
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
M : Type u_4
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : Sub M
inst_3 : OrderedSub M
inst_4 : AddLeftMono M
inst_5 : AddLeftReflectLE M
inst_6 : ExistsAddOfLE M
f : ℕ → M
h : Monotone f
n_1 n : ℕ
h_1 : n < n_1
h₁ : f n ≤ f (n + 1)
h₂ : f 0 ≤ f n
⊢ f (n + 1) - f 0 = f n - f 0 + (f (n + 1) - f n)
have rw : f (n + 1) - f 0 = f n + (f (n + 1) - f n) - f 0
Tactic: rw [tsub_add_eq_add_tsub h₂, add_tsub_cancel_of_le h₁]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
M : Type u_4
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : Sub M
inst_3 : OrderedSub M
inst_4 : AddLeftMono M
inst_5 : AddLeftReflectLE M
inst_6 : ExistsAddOfLE M
f : ℕ → M
h : Monotone f
n_1 n : ℕ
h_1 : n < n_1
h₁ : f n ≤ f (n + 1)
h₂ : f 0 ≤ f n
rw : f (n + 1) - f 0 = f n + (f (n + 1) - f n) - f 0
⊢ f (n + 1) - f 0 = f n - f 0 + (f (n + 1) - f n)
have rw₁ : f (n + 1) - f 0 = f (n + 1) - f 0
Tactic: rw [tsub_add_eq_add_tsub h₂, add_tsub_cancel_of_le h₁]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
M : Type u_4
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : Sub M
inst_3 : OrderedSub M
inst_4 : AddLeftMono M
inst_5 : AddLeftReflectLE M
inst_6 : ExistsAddOfLE M
f : ℕ → M
h : Monotone f
n : ℕ
case case₁ : ∀ n_1 < n, f (n_1 + 1) - f 0 = f n_1 - f 0 + (f (n_1 + 1) - f n_1)
⊢ ∀ k < n, f (k + 1) - f 0 = f k - f 0 + (f (k + 1) - f k)
have case₂ : ∀ n_1 < n, ∀ (h₁ : f n_1 ≤ f (n_1 + 1)), f (n_1 + 1) - f 0 = f n_1 - f 0 + (f (n_1 + 1) - f n_1)
Tactic: case step =>
    intro n _
    have h₁ : f n ≤ f (n + 1) := h (Nat.le_succ _)
    have h₂ : f 0 ≤ f n := h (Nat.zero_le _)
    rw [tsub_add_eq_add_tsub h₂, add_tsub_cancel_of_le h₁]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
M : Type u_4
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : Sub M
inst_3 : OrderedSub M
inst_4 : AddLeftMono M
inst_5 : AddLeftReflectLE M
inst_6 : ExistsAddOfLE M
f : ℕ → M
h : Monotone f
n : ℕ
case case₁ : ∀ n_1 < n, f (n_1 + 1) - f 0 = f n_1 - f 0 + (f (n_1 + 1) - f n_1)
case₂ : ∀ n_1 < n, ∀ (h₁ : f n_1 ≤ f (n_1 + 1)), f (n_1 + 1) - f 0 = f n_1 - f 0 + (f (n_1 + 1) - f n_1)
⊢ ∀ k < n, f (k + 1) - f 0 = f k - f 0 + (f (k + 1) - f k)
have case₃ : ∀ n_1 < n, ∀ (h₁ : f n_1 ≤ f (n_1 + 1)) (h₂ : f 0 ≤ f n_1), f (n_1 + 1) - f 0 = f n_1 - f 0 + (f (n_1 + 1) - f n_1)
Tactic: case step =>
    intro n _
    have h₁ : f n ≤ f (n + 1) := h (Nat.le_succ _)
    have h₂ : f 0 ≤ f n := h (Nat.zero_le _)
    rw [tsub_add_eq_add_tsub h₂, add_tsub_cancel_of_le h₁]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
s : Finset ι
m : ℕ
f : ι → ℕ
h₁ : ∀ x ∈ s, f x = m
⊢ ∑ x ∈ s, f x = #s * m
have rw : Eq (α := ℕ) (∑ x ∈ s, f x) (∑ _x ∈ s, m)
Tactic: rw [← Nat.nsmul_eq_mul, ← sum_const]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
inst : DecidableEq M
s_1 : Finset ι
t : ι → Finset M
this : DecidableEq ι
a : ι
s : Finset ι
has : a ∉ s
ih : #(s.biUnion t) ≤ ∑ a ∈ s, #(t a)
⊢ #((insert a s).biUnion t) ≤ #(t a) + #(s.biUnion t)
have rw : #(t a ∪ s.biUnion t) ≤ #(t a) + #(s.biUnion t)
Tactic: rw [biUnion_insert]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
M : Type u_4
κ : Type u_6
ι : Type u_7
inst : Fintype ι
inst_1 : Fintype κ
inst_2 : CommMonoid M
inst_3 : DecidableEq κ
g : ι → κ
f : ι → M
⊢ Eq.{u_4 + 1} (α := M) (∏ j : κ, ∏ i : { i : ι // g i = j }, f (↑i : ι)) (∏ i : ι, f i)
have rw : Eq.{u_4 + 1} (α := M) (∏ j : κ, ∏ i : { i : ι // g i = j }, f (↑i : ι)) (∏ j : κ, ∏ i : ι with g i = j, f i)
Tactic: rw [← Finset.prod_fiberwise _ g f]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
M : Type u_4
κ : Type u_6
ι : Type u_7
inst : Fintype ι
inst_1 : Fintype κ
inst_2 : CommMonoid M
inst_3 : DecidableEq κ
g : ι → κ
f : ι → M
⊢ Eq.{u_4 + 1} (α := M) (∏ j : κ, ∏ i : { i : ι // g i = j }, f (↑i : ι)) (∏ j : κ, ∏ i : ι with g i = j, f i)
have e_f : ∀ (j : κ), Eq.{u_4 + 1} (α := M) (∏ i : { i : ι // g i = j }, f (↑i : ι)) (∏ i : ι with g i = j, f i)
Tactic: congr with j
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
M : Type u_4
κ : Type u_6
ι : Type u_7
inst : Fintype ι
inst_1 : Fintype κ
inst_2 : CommMonoid M
inst_3 : DecidableEq κ
g : ι → κ
f : κ → M
⊢ Eq.{u_4 + 1} (α := M) (∏ j : κ, ∏ _i : { i : ι // g i = j }, f j) (∏ i : ι, f (g i))
have rw : Eq.{u_4 + 1} (α := M) (∏ j : κ, ∏ _i : { i : ι // g i = j }, f j) (∏ j : κ, ∏ i : ι with g i = j, f j)
Tactic: rw [← Finset.prod_fiberwise' _ g f]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
M : Type u_4
κ : Type u_6
ι : Type u_7
inst : Fintype ι
inst_1 : Fintype κ
inst_2 : CommMonoid M
inst_3 : DecidableEq κ
g : ι → κ
f : κ → M
⊢ Eq.{u_4 + 1} (α := M) (∏ j : κ, ∏ _i : { i : ι // g i = j }, f j) (∏ j : κ, ∏ i : ι with g i = j, f j)
have e_f : ∀ (j : κ), Eq.{u_4 + 1} (α := M) (∏ _i : { i : ι // g i = j }, f j) (∏ i : ι with g i = j, f j)
Tactic: congr with j
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
M : Type u_4
ι : Type u_7
inst : Fintype ι
inst_1 : CommMonoid M
inst_2 : Unique ι
f : ι → M
⊢ ∏ x : ι, f x = f default
have rw : ∏ x ∈ {default}, f x = f default
Tactic: rw [univ_unique, prod_singleton]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
M : Type u_4
ι : Type u_7
inst : Fintype ι
inst_1 : CommMonoid M
inst_2 : Unique ι
f : ι → M
rw : ∏ x ∈ {default}, f x = f default
⊢ ∏ x : ι, f x = f default
have rw₁ : f default = f default
Tactic: rw [univ_unique, prod_singleton]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
M : Type u_4
ι : Type u_7
inst : Fintype ι
inst_1 : CommMonoid M
inst_2 : Subsingleton ι
f : ι → M
a : ι
⊢ ∏ x : ι, f x = f a
have have : ∀ (this : Unique ι), ∏ x : ι, f x = f a
Tactic: have : Unique ι := uniqueOfSubsingleton a
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
M : Type u_4
ι : Type u_7
inst : Fintype ι
inst_1 : CommMonoid M
inst_2 : Subsingleton ι
f : ι → M
a : ι
this : Unique ι
⊢ ∏ x : ι, f x = f a
have rw : f default = f a
Tactic: rw [prod_unique f, Subsingleton.elim default a]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
M : Type u_4
ι : Type u_7
inst : Fintype ι
inst_1 : CommMonoid M
inst_2 : Subsingleton ι
f : ι → M
a : ι
this : Unique ι
rw : f default = f a
⊢ ∏ x : ι, f x = f a
have rw₁ : f a = f a
Tactic: rw [prod_unique f, Subsingleton.elim default a]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
M : Type u_4
ι : Type u_7
inst : Fintype ι
inst_1 : CommMonoid M
p : ι → Prop
f : ι → M
inst_2 : DecidablePred p
s : Finset ι := Set.toFinset {x : ι | p x}
⊢ HMul.hMul (α := M) (∏ i : { x : ι // p x }, f (↑i : ι)) (∏ i : { x : ι // ¬p x }, f (↑i : ι)) = ∏ i : ι, f i
have rw : HMul.hMul (α := M) (∏ a ∈ s, f a) (∏ a ∈ sᶜ, f a) = ∏ i : ι, f i
Tactic: rw [← Finset.prod_subtype s, ← Finset.prod_subtype sᶜ]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
M : Type u_4
ι : Type u_7
inst : Fintype ι
inst_1 : CommMonoid M
p : ι → Prop
f : ι → M
inst_2 : DecidablePred p
s : Finset ι := Set.toFinset {x : ι | p x}
rw : HMul.hMul (α := M) (∏ a ∈ s, f a) (∏ a ∈ sᶜ, f a) = ∏ i : ι, f i
⊢ HMul.hMul (α := M) (∏ i : { x : ι // p x }, f (↑i : ι)) (∏ i : { x : ι // ¬p x }, f (↑i : ι)) = ∏ i : ι, f i
have h : ∀ (x : ι), x ∈ sᶜ ↔ ¬p x
Tactic: rw [← Finset.prod_subtype s, ← Finset.prod_subtype sᶜ]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
M : Type u_4
ι : Type u_7
inst : Fintype ι
inst_1 : CommMonoid M
p : ι → Prop
f : ι → M
inst_2 : DecidablePred p
s : Finset ι := Set.toFinset {x : ι | p x}
rw : HMul.hMul (α := M) (∏ a ∈ s, f a) (∏ a ∈ sᶜ, f a) = ∏ i : ι, f i
h : ∀ (x : ι), x ∈ sᶜ ↔ ¬p x
⊢ HMul.hMul (α := M) (∏ i : { x : ι // p x }, f (↑i : ι)) (∏ i : { x : ι // ¬p x }, f (↑i : ι)) = ∏ i : ι, f i
have h₁ : ∀ (x : ι), x ∈ s ↔ p x
Tactic: rw [← Finset.prod_subtype s, ← Finset.prod_subtype sᶜ]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
M : Type u_4
ι : Type u_7
inst : Fintype ι
inst_1 : CommMonoid M
p : ι → Prop
f : ι → M
inst_2 : DecidablePred p
let let₁ let₂ :
  HMul.hMul (α := M) (∏ i : { x : ι // p x }, f (↑i : ι)) (∏ i : { x : ι // ¬p x }, f (↑i : ι)) = ∏ i : ι, f i
⊢ HMul.hMul (α := M) (∏ i : { x : ι // p x }, f (↑i : ι)) (∏ i : { x : ι // ¬p x }, f (↑i : ι)) = ∏ i : ι, f i
have let₃ : let s : Finset ι := Set.toFinset {x : ι | p x};
HMul.hMul (α := M) (∏ a ∈ s, f a) (∏ a ∈ sᶜ, f a) = ∏ i : ι, f i
Tactic: classical
    let s := { x | p x }.toFinset
    rw [← Finset.prod_subtype s, ← Finset.prod_subtype sᶜ]
    · exact Finset.prod_mul_prod_compl _ _
    · simp [s]
    · simp [s]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
M : Type u_4
ι : Type u_7
inst : Fintype ι
inst_1 : CommMonoid M
p : ι → Prop
f : ι → M
inst_2 : DecidablePred p
let let₁ let₂ :
  HMul.hMul (α := M) (∏ i : { x : ι // p x }, f (↑i : ι)) (∏ i : { x : ι // ¬p x }, f (↑i : ι)) = ∏ i : ι, f i
let₃ :
  let s : Finset ι := Set.toFinset {x : ι | p x};
  HMul.hMul (α := M) (∏ a ∈ s, f a) (∏ a ∈ sᶜ, f a) = ∏ i : ι, f i
⊢ HMul.hMul (α := M) (∏ i : { x : ι // p x }, f (↑i : ι)) (∏ i : { x : ι // ¬p x }, f (↑i : ι)) = ∏ i : ι, f i
have h : let s : Finset ι := Set.toFinset {x : ι | p x};
∀ (x : ι), x ∈ sᶜ ↔ ¬p x
Tactic: classical
    let s := { x | p x }.toFinset
    rw [← Finset.prod_subtype s, ← Finset.prod_subtype sᶜ]
    · exact Finset.prod_mul_prod_compl _ _
    · simp [s]
    · simp [s]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
M : Type u_4
ι : Type u_7
inst : Fintype ι
inst_1 : CommMonoid M
p : ι → Prop
f : ι → M
inst_2 : DecidablePred p
let let₁ let₂ :
  HMul.hMul (α := M) (∏ i : { x : ι // p x }, f (↑i : ι)) (∏ i : { x : ι // ¬p x }, f (↑i : ι)) = ∏ i : ι, f i
let₃ :
  let s : Finset ι := Set.toFinset {x : ι | p x};
  HMul.hMul (α := M) (∏ a ∈ s, f a) (∏ a ∈ sᶜ, f a) = ∏ i : ι, f i
h :
  let s : Finset ι := Set.toFinset {x : ι | p x};
  ∀ (x : ι), x ∈ sᶜ ↔ ¬p x
⊢ HMul.hMul (α := M) (∏ i : { x : ι // p x }, f (↑i : ι)) (∏ i : { x : ι // ¬p x }, f (↑i : ι)) = ∏ i : ι, f i
have h₁ : let s : Finset ι := Set.toFinset {x : ι | p x};
∀ (x : ι), x ∈ s ↔ p x
Tactic: classical
    let s := { x | p x }.toFinset
    rw [← Finset.prod_subtype s, ← Finset.prod_subtype sᶜ]
    · exact Finset.prod_mul_prod_compl _ _
    · simp [s]
    · simp [s]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (hypothesis)
Goal:
ι : Type u_1
M : Type u_5
inst : DecidableEq ι
inst_1 : CommMonoid M
f : ι → M
a : ι
l : List ι
hl : (a :: l).Nodup
⊢ (a :: l).toFinset.prod f = (map f (a :: l)).prod
have notMem : a ∉ l
Tactic: let ⟨notMem, hl⟩ := List.nodup_cons.mp hl
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (hypothesis)
Goal:
ι : Type u_1
M : Type u_5
inst : DecidableEq ι
inst_1 : CommMonoid M
f : ι → M
a : ι
l : List ι
hl : (a :: l).Nodup
notMem : a ∉ l
⊢ (a :: l).toFinset.prod f = (map f (a :: l)).prod
have hl₁ : l.Nodup
Tactic: let ⟨notMem, hl⟩ := List.nodup_cons.mp hl
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
a : M
s : Finset ι
m : ι → Multiset M
⊢ Membership.mem (γ := Multiset M) (∑ i ∈ s, m i) a ↔ ∃ i ∈ s, a ∈ m i
have empty : Membership.mem (γ := Multiset M) (∑ i ∈ ∅, m i) a ↔ ∃ (i : ι), Membership.mem (γ := Finset ι) ∅ i ∧ a ∈ m i
Tactic: induction s using Finset.cons_induction with grind
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
a : M
s : Finset ι
m : ι → Multiset M
empty : Membership.mem (γ := Multiset M) (∑ i ∈ ∅, m i) a ↔ ∃ (i : ι), Membership.mem (γ := Finset ι) ∅ i ∧ a ∈ m i
⊢ Membership.mem (γ := Multiset M) (∑ i ∈ s, m i) a ↔ ∃ i ∈ s, a ∈ m i
have cons : ∀ (a_1 : ι) (s : Finset ι) (h : a_1 ∉ s),
  (Membership.mem (γ := Multiset M) (∑ i ∈ s, m i) a ↔ ∃ i ∈ s, a ∈ m i) →
    (Membership.mem (γ := Multiset M) (∑ i ∈ Finset.cons a_1 s h, m i) a ↔ ∃ i ∈ Finset.cons a_1 s h, a ∈ m i)
Tactic: induction s using Finset.cons_induction with grind
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
α : Type u_5
inst : CommMonoid M
m : Multiset ι
s : Finset α
f : ι → α → M
⊢ Eq.{u_4 + 1} (α := M) (prod (map (fun (i : ι) ↦ ∏ a ∈ s, f i a) m)) (∏ a ∈ s, prod (map (fun (i : ι) ↦ f i a) m))
have empty : Eq.{u_4 + 1} (α := M) (prod (map (fun (i : ι) ↦ ∏ a ∈ ∅, f i a) m)) (∏ a ∈ ∅, prod (map (fun (i : ι) ↦ f i a) m))
Tactic: induction s using Finset.induction with
  | empty => simp
  | insert a s ha ih => simp [Finset.prod_insert ha, prod_map_mul, ih]
Cleared hypotheses: s