awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
a : α
hf : HasFiniteMulSupport f
rw rw₁ rw₂ : f a * ∏ᶠ (i : α) (_ : i ≠ a), f i = ∏ i ∈ Finite.toFinset (s := mulSupport f) hf, f i
rw₃ :
  ∀ (h : ∀ (x : α), f x ≠ 1 → (x ≠ a ↔ x ∈ Finite.toFinset (s := mulSupport f) hf \ {a})),
    f a * ∏ᶠ (i : α) (_ : i ≠ a), f i = ∏ i ∈ Finite.toFinset (s := mulSupport f) hf, f i
rw₄ :
  ∀ (h : ∀ (x : α), f x ≠ 1 → (x ≠ a ↔ x ∈ Finite.toFinset (s := mulSupport f) hf \ {a})),
    f a * ∏ i ∈ (Finite.toFinset (s := mulSupport f) hf).erase a, f i =
      ∏ i ∈ Finite.toFinset (s := mulSupport f) hf, f i
⊢ f a * ∏ᶠ (i : α) (_ : i ≠ a), f i = ∏ᶠ (i : α), f i
have pos : ∀ (h : ∀ (x : α), f x ≠ 1 → (x ≠ a ↔ x ∈ Finite.toFinset (s := mulSupport f) hf \ {a})) (ha : a ∈ mulSupport f),
  f a * ∏ i ∈ (Finite.toFinset (s := mulSupport f) hf).erase a, f i = ∏ i ∈ Finite.toFinset (s := mulSupport f) hf, f i
Tactic: classical
    rw [finprod_eq_prod _ hf]
    have h : ∀ x : α, f x ≠ 1 → (x ≠ a ↔ x ∈ hf.toFinset \ {a}) := by
      intro x hx
      rw [Finset.mem_sdiff, Finset.mem_singleton, Finite.mem_toFinset, mem_mulSupport]
      grind
    rw [finprod_cond_eq_prod_of_cond_iff f (fun hx => h _ hx), Finset.sdiff_singleton_eq_erase]
    by_cases ha : a ∈ mulSupport f
    · apply Finset.mul_prod_erase _ _ ((Finite.mem_toFinset _).mpr ha)
    · rw [mem_mulSupport, not_not] at ha
      rw [ha, one_mul]
      apply Finset.prod_erase _ ha
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
a : α
hf : HasFiniteMulSupport f
rw rw₁ rw₂ : f a * ∏ᶠ (i : α) (_ : i ≠ a), f i = ∏ i ∈ Finite.toFinset (s := mulSupport f) hf, f i
rw₃ :
  ∀ (h : ∀ (x : α), f x ≠ 1 → (x ≠ a ↔ x ∈ Finite.toFinset (s := mulSupport f) hf \ {a})),
    f a * ∏ᶠ (i : α) (_ : i ≠ a), f i = ∏ i ∈ Finite.toFinset (s := mulSupport f) hf, f i
rw₄ :
  ∀ (h : ∀ (x : α), f x ≠ 1 → (x ≠ a ↔ x ∈ Finite.toFinset (s := mulSupport f) hf \ {a})),
    f a * ∏ i ∈ (Finite.toFinset (s := mulSupport f) hf).erase a, f i =
      ∏ i ∈ Finite.toFinset (s := mulSupport f) hf, f i
pos :
  ∀ (h : ∀ (x : α), f x ≠ 1 → (x ≠ a ↔ x ∈ Finite.toFinset (s := mulSupport f) hf \ {a})) (ha : a ∈ mulSupport f),
    f a * ∏ i ∈ (Finite.toFinset (s := mulSupport f) hf).erase a, f i =
      ∏ i ∈ Finite.toFinset (s := mulSupport f) hf, f i
⊢ f a * ∏ᶠ (i : α) (_ : i ≠ a), f i = ∏ᶠ (i : α), f i
have neg : ∀ (h : ∀ (x : α), f x ≠ 1 → (x ≠ a ↔ x ∈ Finite.toFinset (s := mulSupport f) hf \ {a})) (ha : a ∉ mulSupport f),
  f a * ∏ i ∈ (Finite.toFinset (s := mulSupport f) hf).erase a, f i = ∏ i ∈ Finite.toFinset (s := mulSupport f) hf, f i
Tactic: classical
    rw [finprod_eq_prod _ hf]
    have h : ∀ x : α, f x ≠ 1 → (x ≠ a ↔ x ∈ hf.toFinset \ {a}) := by
      intro x hx
      rw [Finset.mem_sdiff, Finset.mem_singleton, Finite.mem_toFinset, mem_mulSupport]
      grind
    rw [finprod_cond_eq_prod_of_cond_iff f (fun hx => h _ hx), Finset.sdiff_singleton_eq_erase]
    by_cases ha : a ∈ mulSupport f
    · apply Finset.mul_prod_erase _ _ ((Finite.mem_toFinset _).mpr ha)
    · rw [mem_mulSupport, not_not] at ha
      rw [ha, one_mul]
      apply Finset.prod_erase _ ha
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
s : Set α
t : Set β
f : α → β → M
hs : s.Finite
ht : t.Finite
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ∈ s) (j : β) (_ : j ∈ t), f i j)
    (∏ᶠ (j : β) (_ : j ∈ t) (i : α) (_ : i ∈ s), f i j)
have lift : ∀ (s : Finset α),
  Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ∈ (↑s : Set α)) (j : β) (_ : j ∈ t), f i j)
    (∏ᶠ (j : β) (_ : j ∈ t) (i : α) (_ : i ∈ (↑s : Set α)), f i j)
Tactic: lift s to Finset α using hs
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
t : Set β
f : α → β → M
ht : t.Finite
s : Finset α
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ∈ (↑s : Set α)) (j : β) (_ : j ∈ t), f i j)
    (∏ᶠ (j : β) (_ : j ∈ t) (i : α) (_ : i ∈ (↑s : Set α)), f i j)
have lift : ∀ (t : Finset β),
  Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ∈ (↑s : Set α)) (j : β) (_ : j ∈ (↑t : Set β)), f i j)
    (∏ᶠ (j : β) (_ : j ∈ (↑t : Set β)) (i : α) (_ : i ∈ (↑s : Set α)), f i j)
Tactic: lift t to Finset β using ht
Cleared hypotheses: t, ht
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
f : α → β → M
s : Finset α
t : Finset β
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ∈ (↑s : Set α)) (j : β) (_ : j ∈ (↑t : Set β)), f i j)
    (∏ᶠ (j : β) (_ : j ∈ (↑t : Set β)) (i : α) (_ : i ∈ (↑s : Set α)), f i j)
have simp : Eq.{u_5 + 1} (α := M) (∏ i ∈ s, ∏ i_1 ∈ t, f i i_1) (∏ i ∈ t, ∏ i_1 ∈ s, f i_1 i)
Tactic: simp only [finprod_mem_coe_finset]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (hypothesis)
Goal:
α : Type u_1
M₀ : Type u_7
inst : CommMonoidWithZero M₀
f : α → M₀
x : α
hx : f x = 0
hf : HasFiniteMulSupport f
⊢ Eq.{u_7 + 1} (α := M₀) (∏ᶠ (x : α), f x) 0
have a : Nontrivial M₀
Tactic: nontriviality
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M₀ : Type u_7
inst : CommMonoidWithZero M₀
f : α → M₀
x : α
hx : f x = 0
hf : HasFiniteMulSupport f
h : Nontrivial M₀
⊢ Eq.{u_7 + 1} (α := M₀) (∏ᶠ (x : α), f x) 0
have rw : Eq.{u_7 + 1} (α := M₀) (∏ i ∈ Finite.toFinset (s := mulSupport f) hf, f i) 0
Tactic: rw [finprod_eq_prod f hf]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M₀ : Type u_7
inst : CommMonoidWithZero M₀
f : α → M₀
x : α
hx : f x = 0
hf : HasFiniteMulSupport f
h : Nontrivial M₀
⊢ Eq.{u_7 + 1} (α := M₀) (∏ i ∈ Finite.toFinset (s := mulSupport f) hf, f i) 0
have refine : x ∈ mulSupport f
Tactic: refine Finset.prod_eq_zero (hf.mem_toFinset.2 ?_) hx
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
s : Finset β
f : α → β → M
h : ∀ b ∈ s, HasFiniteMulSupport.{u_1, u_5} (M := M) fun (a : α) ↦ f a b
⊢ (mulSupport.{u_1, u_5} (M := M) fun (a : α) ↦ ∏ b ∈ s, f a b) ⊆
    (↑(Finite.toFinset (s := ⋃ i ∈ (↑s : Set β), mulSupport.{u_1, u_5} (M := M) fun (a : α) ↦ f a i) ⋯) : Set α)
have rw : Subset.{u_1} (α := Set α) (mulSupport.{u_1, u_5} (M := M) fun (a : α) ↦ ∏ b ∈ s, f a b)
  (⋃ i ∈ (↑s : Set β), mulSupport.{u_1, u_5} (M := M) fun (a : α) ↦ f a i)
Tactic: rw [Finite.coe_toFinset]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
s : Finset β
f : α → β → M
h : ∀ b ∈ s, HasFiniteMulSupport.{u_1, u_5} (M := M) fun (a : α) ↦ f a b
x : α
hx : Membership.mem (γ := Set α) (mulSupport.{u_1, u_5} (M := M) fun (a : α) ↦ ∏ b ∈ s, f a b) x
⊢ Membership.mem (γ := Set α) (⋃ i ∈ (↑s : Set β), mulSupport.{u_1, u_5} (M := M) fun (a : α) ↦ f a i) x
have simp : ∃ i ∈ s, ¬f x i = 1
Tactic: simp only [exists_prop, mem_iUnion, Ne, mem_mulSupport, Finset.mem_coe]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
s : Finset β
f : α → β → M
h : ∀ b ∈ s, HasFiniteMulSupport.{u_1, u_5} (M := M) fun (a : α) ↦ f a b
x : α
hx : Membership.mem (γ := Set α) (mulSupport.{u_1, u_5} (M := M) fun (a : α) ↦ ∏ b ∈ s, f a b) x
⊢ ∃ i ∈ s, ¬f x i = 1
have contrapose! : ∀ (hx : ∀ (i : β) (_ : i ∈ s), f x i = 1), x ∉ mulSupport.{u_1, u_5} (M := M) fun (a : α) ↦ ∏ b ∈ s, f a b
Tactic: contrapose! hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
s : Finset β
f : α → β → M
h : ∀ b ∈ s, HasFiniteMulSupport.{u_1, u_5} (M := M) fun (a : α) ↦ f a b
x : α
hx : ∀ (i : β) (_ : i ∈ s), f x i = 1
⊢ x ∉ mulSupport.{u_1, u_5} (M := M) fun (a : α) ↦ ∏ b ∈ s, f a b
have rw : ¬Ne.{u_5 + 1} (α := M) (∏ b ∈ s, f x b) 1
Tactic: rw [mem_mulSupport, not_not, Finset.prod_congr rfl hx, Finset.prod_const_one]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
s : Finset β
f : α → β → M
h : ∀ b ∈ s, HasFiniteMulSupport.{u_1, u_5} (M := M) fun (a : α) ↦ f a b
x : α
hx : ∀ (i : β) (_ : i ∈ s), f x i = 1
rw : ¬Ne.{u_5 + 1} (α := M) (∏ b ∈ s, f x b) 1
⊢ x ∉ mulSupport.{u_1, u_5} (M := M) fun (a : α) ↦ ∏ b ∈ s, f a b
have rw₁ : Eq.{u_5 + 1} (α := M) (∏ b ∈ s, f x b) 1
Tactic: rw [mem_mulSupport, not_not, Finset.prod_congr rfl hx, Finset.prod_const_one]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
s : Finset β
f : α → β → M
h : ∀ b ∈ s, HasFiniteMulSupport.{u_1, u_5} (M := M) fun (a : α) ↦ f a b
x : α
hx : ∀ (i : β) (_ : i ∈ s), f x i = 1
rw : ¬Ne.{u_5 + 1} (α := M) (∏ b ∈ s, f x b) 1
rw₁ : Eq.{u_5 + 1} (α := M) (∏ b ∈ s, f x b) 1
⊢ x ∉ mulSupport.{u_1, u_5} (M := M) fun (a : α) ↦ ∏ b ∈ s, f a b
have rw₂ : Eq.{u_5 + 1} (α := M) (∏ x ∈ s, 1) 1
Tactic: rw [mem_mulSupport, not_not, Finset.prod_congr rfl hx, Finset.prod_const_one]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
s : Finset β
f : α → β → M
h : ∀ b ∈ s, HasFiniteMulSupport.{u_1, u_5} (M := M) fun (a : α) ↦ f a b
x : α
hx : ∀ (i : β) (_ : i ∈ s), f x i = 1
rw : ¬Ne.{u_5 + 1} (α := M) (∏ b ∈ s, f x b) 1
rw₁ : Eq.{u_5 + 1} (α := M) (∏ b ∈ s, f x b) 1
rw₂ : Eq.{u_5 + 1} (α := M) (∏ x ∈ s, 1) 1
⊢ x ∉ mulSupport.{u_1, u_5} (M := M) fun (a : α) ↦ ∏ b ∈ s, f a b
have rw₃ : Eq.{u_5 + 1} (α := M) 1 1
Tactic: rw [mem_mulSupport, not_not, Finset.prod_congr rfl hx, Finset.prod_const_one]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (hypothesis)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
s : Finset β
f : α → β → M
h : ∀ b ∈ s, HasFiniteMulSupport.{u_1, u_5} (M := M) fun (a : α) ↦ f a b
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (a : α), ∏ b ∈ s, f a b) (∏ b ∈ s, ∏ᶠ (a : α), f a b)
have hU : (mulSupport.{u_1, u_5} (M := M) fun (a : α) ↦ ∏ b ∈ s, f a b) ⊆
  (↑(Finite.toFinset (s := ⋃ i ∈ (↑s : Set β), mulSupport.{u_1, u_5} (M := M) fun (a : α) ↦ f a i) sorry) : Set α)
Tactic: have hU :
    (mulSupport fun a => ∏ b ∈ s, f a b) ⊆
      (s.finite_toSet.biUnion fun b hb => h b (Finset.mem_coe.1 hb)).toFinset := by
    rw [Finite.coe_toFinset]
    intro x hx
    simp only [exists_prop, mem_iUnion, Ne, mem_mulSupport, Finset.mem_coe]
    contrapose! hx
    rw [mem_mulSupport, not_not, Finset.prod_congr rfl hx, Finset.prod_const_one]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
s : Finset β
f : α → β → M
h : ∀ b ∈ s, HasFiniteMulSupport.{u_1, u_5} (M := M) fun (a : α) ↦ f a b
hU :
  (mulSupport.{u_1, u_5} (M := M) fun (a : α) ↦ ∏ b ∈ s, f a b) ⊆
    (↑(Finite.toFinset (s := ⋃ i ∈ (↑s : Set β), mulSupport.{u_1, u_5} (M := M) fun (a : α) ↦ f a i) ⋯) : Set α)
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (a : α), ∏ b ∈ s, f a b) (∏ b ∈ s, ∏ᶠ (a : α), f a b)
have rw : Eq.{u_5 + 1} (α := M)
  (∏ y ∈ s,
    ∏ x ∈ Finite.toFinset (s := ⋃ i ∈ (↑s : Set β), mulSupport.{u_1, u_5} (M := M) fun (a : α) ↦ f a i) sorry, f x y)
  (∏ b ∈ s, ∏ᶠ (a : α), f a b)
Tactic: rw [finprod_eq_prod_of_mulSupport_subset _ hU, Finset.prod_comm]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
s : Finset β
f : α → β → M
h : ∀ b ∈ s, HasFiniteMulSupport.{u_1, u_5} (M := M) fun (a : α) ↦ f a b
hU :
  (mulSupport.{u_1, u_5} (M := M) fun (a : α) ↦ ∏ b ∈ s, f a b) ⊆
    (↑(Finite.toFinset (s := ⋃ i ∈ (↑s : Set β), mulSupport.{u_1, u_5} (M := M) fun (a : α) ↦ f a i) ⋯) : Set α)
⊢ Eq.{u_5 + 1} (α := M)
    (∏ y ∈ s,
      ∏ x ∈ Finite.toFinset (s := ⋃ i ∈ (↑s : Set β), mulSupport.{u_1, u_5} (M := M) fun (a : α) ↦ f a i) ⋯, f x y)
    (∏ b ∈ s, ∏ᶠ (a : α), f a b)
have refine : ∀ (b : β) (hb : b ∈ s),
  (mulSupport.{u_1, u_5} (M := M) fun (x : α) ↦ f x b) ⊆
    (↑(Finite.toFinset (s := ⋃ i ∈ (↑s : Set β), mulSupport.{u_1, u_5} (M := M) fun (a : α) ↦ f a i) sorry) : Set α)
Tactic: refine Finset.prod_congr rfl fun b hb => (finprod_eq_prod_of_mulSupport_subset _ ?_).symm
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
s : Finset β
f : α → β → M
h : ∀ b ∈ s, HasFiniteMulSupport.{u_1, u_5} (M := M) fun (a : α) ↦ f a b
hU :
  (mulSupport.{u_1, u_5} (M := M) fun (a : α) ↦ ∏ b ∈ s, f a b) ⊆
    (↑(Finite.toFinset (s := ⋃ i ∈ (↑s : Set β), mulSupport.{u_1, u_5} (M := M) fun (a : α) ↦ f a i) ⋯) : Set α)
b : β
hb : b ∈ s
a : α
ha : Membership.mem (γ := Set α) (mulSupport.{u_1, u_5} (M := M) fun (x : α) ↦ f x b) a
⊢ a ∈ (↑(Finite.toFinset (s := ⋃ i ∈ (↑s : Set β), mulSupport.{u_1, u_5} (M := M) fun (a : α) ↦ f a i) ⋯) : Set α)
have simp : ∃ (i : β) (_ : i ∈ (↑s : Set β)), Membership.mem (γ := Set α) (mulSupport.{u_1, u_5} (M := M) fun (a : α) ↦ f a i) a
Tactic: simp only [Finite.coe_toFinset, mem_iUnion]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
inst_1 : DecidableEq α
f : β → α
s : Finset β
g : β → M
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (x : α), ∏ y ∈ s with f y = x, g y) (∏ k ∈ s, g k)
have rw : Eq.{u_5 + 1} (α := M) (∏ i ∈ Finset.image f s, ∏ y ∈ s with f y = i, g y) (∏ k ∈ s, g k)
Tactic: rw [finprod_eq_finsetProd_of_mulSupport_subset]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
inst_1 : DecidableEq α
f : β → α
s : Finset β
g : β → M
rw : Eq.{u_5 + 1} (α := M) (∏ i ∈ Finset.image f s, ∏ y ∈ s with f y = i, g y) (∏ k ∈ s, g k)
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (x : α), ∏ y ∈ s with f y = x, g y) (∏ k ∈ s, g k)
have s₁ : Finset α
Tactic: rw [finprod_eq_finsetProd_of_mulSupport_subset]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
inst_1 : DecidableEq α
f : β → α
s : Finset β
g : β → M
rw : Eq.{u_5 + 1} (α := M) (∏ i ∈ Finset.image f s, ∏ y ∈ s with f y = i, g y) (∏ k ∈ s, g k)
s₁ : Finset α
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (x : α), ∏ y ∈ s with f y = x, g y) (∏ k ∈ s, g k)
have h : (mulSupport.{u_1, u_5} (M := M) fun (x : α) ↦ ∏ y ∈ s with f y = x, g y) ⊆ (↑(Finset.image f s) : Set α)
Tactic: rw [finprod_eq_finsetProd_of_mulSupport_subset]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
inst_1 : DecidableEq α
f : β → α
s : Finset β
g : β → M
⊢ Eq.{u_5 + 1} (α := M) (∏ i ∈ Finset.image f s, ∏ y ∈ s with f y = i, g y) (∏ k ∈ s, g k)
have eq : ∀ i ∈ s, Eq.{u_5 + 1} (α := M) (∏ y ∈ s with f y = f i, g y) (∏ j ∈ s with f j = f i, g j)
Tactic: rw [Finset.prod_image']
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (hypothesis)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
inst_1 : DecidableEq α
f : β → α
s : Finset β
g : β → M
x : α
hx : Membership.mem (γ := Set α) (mulSupport.{u_1, u_5} (M := M) fun (x : α) ↦ ∏ y ∈ s with f y = x, g y) x
⊢ x ∈ (↑(Finset.image f s) : Set α)
have hx₁ : Ne.{u_5 + 1} (α := M) (∏ y ∈ s with f y = x, g y) 1
Tactic: rw [mem_mulSupport] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
inst_1 : DecidableEq α
f : β → α
s : Finset β
g : β → M
x : α
hx : Ne.{u_5 + 1} (α := M) (∏ y ∈ s with f y = x, g y) 1
⊢ x ∈ (↑(Finset.image f s) : Set α)
have h : ∀ (a : β) (h : a ∈ {y ∈ s | f y = x}), x ∈ (↑(Finset.image f s) : Set α)
Tactic: obtain ⟨a, h, -⟩ := Finset.exists_ne_one_of_prod_ne_one hx
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
inst_1 : DecidableEq α
f : β → α
s : Finset β
g : β → M
x : α
hx : Ne.{u_5 + 1} (α := M) (∏ y ∈ s with f y = x, g y) 1
a : β
h : a ∈ {y ∈ s | f y = x}
⊢ x ∈ (↑(Finset.image f s) : Set α)
have h₁ : ∀ (h : a ∈ s ∧ f a = x), ∃ x_1 ∈ s, f x_1 = x
Tactic: simp only [Finset.mem_filter, Finset.coe_image, mem_image, SetLike.mem_coe] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
R : Type u_7
inst : NonUnitalNonAssocSemiring R
inst_1 : NoZeroDivisors R
f : α → R
r : R
⊢ r * ∑ᶠ (a : α), f a = ∑ᶠ (a : α), r * f a
have pos : ∀ (hr : r = 0), r * ∑ᶠ (a : α), f a = ∑ᶠ (a : α), r * f a
Tactic: by_cases hr : r = 0
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
R : Type u_7
inst : NonUnitalNonAssocSemiring R
inst_1 : NoZeroDivisors R
f : α → R
r : R
pos : ∀ (hr : r = 0), r * ∑ᶠ (a : α), f a = ∑ᶠ (a : α), r * f a
⊢ r * ∑ᶠ (a : α), f a = ∑ᶠ (a : α), r * f a
have neg : ∀ (hr : ¬r = 0), r * ∑ᶠ (a : α), f a = ∑ᶠ (a : α), r * f a
Tactic: by_cases hr : r = 0
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
R : Type u_7
inst : NonUnitalNonAssocSemiring R
inst_1 : NoZeroDivisors R
f : α → R
r : R
hr : ¬r = 0
⊢ r * ∑ᶠ (a : α), f a = ∑ᶠ (a : α), r * f a
have pos : ∀ (h : (support f).Finite), r * ∑ᶠ (a : α), f a = ∑ᶠ (a : α), r * f a
Tactic: by_cases h : f.support.Finite
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
R : Type u_7
inst : NonUnitalNonAssocSemiring R
inst_1 : NoZeroDivisors R
f : α → R
r : R
hr : ¬r = 0
pos : ∀ (h : (support f).Finite), r * ∑ᶠ (a : α), f a = ∑ᶠ (a : α), r * f a
⊢ r * ∑ᶠ (a : α), f a = ∑ᶠ (a : α), r * f a
have neg : ∀ (h : ¬(support f).Finite), r * ∑ᶠ (a : α), f a = ∑ᶠ (a : α), r * f a
Tactic: by_cases h : f.support.Finite
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
R : Type u_7
inst : NonUnitalNonAssocSemiring R
inst_1 : NoZeroDivisors R
s : Set α
f : α → R
r : R
⊢ r * ∑ᶠ (a : α) (_ : a ∈ s), f a = ∑ᶠ (a : α) (_ : a ∈ s), r * f a
have rw : Eq.{u_7 + 1} (α := R) (∑ᶠ (a : α), r * ∑ᶠ (_ : a ∈ s), f a) (∑ᶠ (a : α) (_ : a ∈ s), r * f a)
Tactic: rw [mul_finsum]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
R : Type u_7
inst : NonUnitalNonAssocSemiring R
inst_1 : NoZeroDivisors R
s : Set α
f : α → R
r : R
⊢ Eq.{u_7 + 1} (α := R) (∑ᶠ (a : α), r * ∑ᶠ (_ : a ∈ s), f a) (∑ᶠ (a : α) (_ : a ∈ s), r * f a)
have e_f : Eq (α := α → R) (fun (a : α) ↦ r * ∑ᶠ (_ : a ∈ s), f a) fun (a : α) ↦ ∑ᶠ (_ : a ∈ s), r * f a
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
R : Type u_7
inst : NonUnitalNonAssocSemiring R
inst_1 : NoZeroDivisors R
s : Set α
f : α → R
r : R
⊢ Eq (α := α → R) (fun (a : α) ↦ r * ∑ᶠ (_ : a ∈ s), f a) fun (a : α) ↦ ∑ᶠ (_ : a ∈ s), r * f a
have e_f : ∀ (a : α), r * ∑ᶠ (_ : a ∈ s), f a = ∑ᶠ (_ : a ∈ s), r * f a
Tactic: ext a
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
R : Type u_7
inst : NonUnitalNonAssocSemiring R
inst_1 : NoZeroDivisors R
s : Set α
f : α → R
r : R
a : α
⊢ r * ∑ᶠ (_ : a ∈ s), f a = ∑ᶠ (_ : a ∈ s), r * f a
have pos : ∀ (h : a ∈ s), r * ∑ᶠ (_ : a ∈ s), f a = ∑ᶠ (_ : a ∈ s), r * f a
Tactic: by_cases h : a ∈ s
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
R : Type u_7
inst : NonUnitalNonAssocSemiring R
inst_1 : NoZeroDivisors R
s : Set α
f : α → R
r : R
a : α
pos : ∀ (h : a ∈ s), r * ∑ᶠ (_ : a ∈ s), f a = ∑ᶠ (_ : a ∈ s), r * f a
⊢ r * ∑ᶠ (_ : a ∈ s), f a = ∑ᶠ (_ : a ∈ s), r * f a
have neg : ∀ (h : a ∉ s), r * ∑ᶠ (_ : a ∈ s), f a = ∑ᶠ (_ : a ∈ s), r * f a
Tactic: by_cases h : a ∈ s
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
R : Type u_7
inst : NonUnitalNonAssocSemiring R
inst_1 : NoZeroDivisors R
f : α → R
r : R
⊢ (∑ᶠ (a : α), f a) * r = ∑ᶠ (a : α), f a * r
have pos : ∀ (hr : r = 0), (∑ᶠ (a : α), f a) * r = ∑ᶠ (a : α), f a * r
Tactic: by_cases hr : r = 0
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
R : Type u_7
inst : NonUnitalNonAssocSemiring R
inst_1 : NoZeroDivisors R
f : α → R
r : R
pos : ∀ (hr : r = 0), (∑ᶠ (a : α), f a) * r = ∑ᶠ (a : α), f a * r
⊢ (∑ᶠ (a : α), f a) * r = ∑ᶠ (a : α), f a * r
have neg : ∀ (hr : ¬r = 0), (∑ᶠ (a : α), f a) * r = ∑ᶠ (a : α), f a * r
Tactic: by_cases hr : r = 0
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
R : Type u_7
inst : NonUnitalNonAssocSemiring R
inst_1 : NoZeroDivisors R
f : α → R
r : R
hr : ¬r = 0
⊢ (∑ᶠ (a : α), f a) * r = ∑ᶠ (a : α), f a * r
have pos : ∀ (h : (support f).Finite), (∑ᶠ (a : α), f a) * r = ∑ᶠ (a : α), f a * r
Tactic: by_cases h : f.support.Finite
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
R : Type u_7
inst : NonUnitalNonAssocSemiring R
inst_1 : NoZeroDivisors R
f : α → R
r : R
hr : ¬r = 0
pos : ∀ (h : (support f).Finite), (∑ᶠ (a : α), f a) * r = ∑ᶠ (a : α), f a * r
⊢ (∑ᶠ (a : α), f a) * r = ∑ᶠ (a : α), f a * r
have neg : ∀ (h : ¬(support f).Finite), (∑ᶠ (a : α), f a) * r = ∑ᶠ (a : α), f a * r
Tactic: by_cases h : f.support.Finite
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
R : Type u_7
inst : NonUnitalNonAssocSemiring R
inst_1 : NoZeroDivisors R
s : Set α
f : α → R
r : R
⊢ (∑ᶠ (a : α) (_ : a ∈ s), f a) * r = ∑ᶠ (a : α) (_ : a ∈ s), f a * r
have rw : Eq.{u_7 + 1} (α := R) (∑ᶠ (a : α), (∑ᶠ (_ : a ∈ s), f a) * r) (∑ᶠ (a : α) (_ : a ∈ s), f a * r)
Tactic: rw [finsum_mul]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
R : Type u_7
inst : NonUnitalNonAssocSemiring R
inst_1 : NoZeroDivisors R
s : Set α
f : α → R
r : R
⊢ Eq.{u_7 + 1} (α := R) (∑ᶠ (a : α), (∑ᶠ (_ : a ∈ s), f a) * r) (∑ᶠ (a : α) (_ : a ∈ s), f a * r)
have e_f : Eq (α := α → R) (fun (a : α) ↦ (∑ᶠ (_ : a ∈ s), f a) * r) fun (a : α) ↦ ∑ᶠ (_ : a ∈ s), f a * r
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
R : Type u_7
inst : NonUnitalNonAssocSemiring R
inst_1 : NoZeroDivisors R
s : Set α
f : α → R
r : R
⊢ Eq (α := α → R) (fun (a : α) ↦ (∑ᶠ (_ : a ∈ s), f a) * r) fun (a : α) ↦ ∑ᶠ (_ : a ∈ s), f a * r
have e_f : ∀ (a : α), (∑ᶠ (_ : a ∈ s), f a) * r = ∑ᶠ (_ : a ∈ s), f a * r
Tactic: ext a
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
R : Type u_7
inst : NonUnitalNonAssocSemiring R
inst_1 : NoZeroDivisors R
s : Set α
f : α → R
r : R
a : α
⊢ (∑ᶠ (_ : a ∈ s), f a) * r = ∑ᶠ (_ : a ∈ s), f a * r
have pos : ∀ (h : a ∈ s), (∑ᶠ (_ : a ∈ s), f a) * r = ∑ᶠ (_ : a ∈ s), f a * r
Tactic: by_cases h : a ∈ s
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
R : Type u_7
inst : NonUnitalNonAssocSemiring R
inst_1 : NoZeroDivisors R
s : Set α
f : α → R
r : R
a : α
pos : ∀ (h : a ∈ s), (∑ᶠ (_ : a ∈ s), f a) * r = ∑ᶠ (_ : a ∈ s), f a * r
⊢ (∑ᶠ (_ : a ∈ s), f a) * r = ∑ᶠ (_ : a ∈ s), f a * r
have neg : ∀ (h : a ∉ s), (∑ᶠ (_ : a ∈ s), f a) * r = ∑ᶠ (_ : a ∈ s), f a * r
Tactic: by_cases h : a ∈ s
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
N : Type u_6
inst : CommMonoid N
α : Type u_7
ι : Type u_8
f : ι → α → N
hf : HasFiniteMulSupport f
a : α
⊢ HasFiniteMulSupport.{u_8, u_6} (M := N) fun (i : ι) ↦ f i a
have funProp : Eq.{u_6 + 1} (α := N) (1 a) 1
Tactic: fun_prop (disch := simp)
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (hypothesis)
Goal:
N : Type u_6
inst : CommMonoid N
α : Type u_7
ι : Type u_8
f : ι → α → N
hf : HasFiniteMulSupport f
a : α
⊢ Eq.{u_6 + 1} (α := N) ((∏ᶠ (i : ι), f i) a) (∏ᶠ (i : ι), f i a)
have hf' : HasFiniteMulSupport.{u_8, u_6} (M := N) fun (i : ι) ↦ f i a
Tactic: have hf' : HasFiniteMulSupport fun i ↦ f i a := by fun_prop (disch := simp)