awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
ι : Sort u_6
R : Type u_7
M : Type u_8
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.IsTorsionFree R M
f : ι → R
x : M
⊢ HSMul.hSMul.{u_7, u_8, u_8} (α := R) (∑ᶠ (i : ι), f i) x = ∑ᶠ (i : ι), f i • x
have inl : HSMul.hSMul.{u_7, u_8, u_8} (α := R) (β := M) (∑ᶠ (i : ι), f i) 0 = ∑ᶠ (i : ι), HSMul.hSMul (β := M) (f i) 0
Tactic: rcases eq_or_ne x 0 with (rfl | hx)
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
ι : Sort u_6
R : Type u_7
M : Type u_8
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.IsTorsionFree R M
f : ι → R
x : M
inl : HSMul.hSMul.{u_7, u_8, u_8} (α := R) (β := M) (∑ᶠ (i : ι), f i) 0 = ∑ᶠ (i : ι), HSMul.hSMul (β := M) (f i) 0
⊢ HSMul.hSMul.{u_7, u_8, u_8} (α := R) (∑ᶠ (i : ι), f i) x = ∑ᶠ (i : ι), f i • x
have inr : ∀ (hx : x ≠ 0), HSMul.hSMul.{u_7, u_8, u_8} (α := R) (∑ᶠ (i : ι), f i) x = ∑ᶠ (i : ι), f i • x
Tactic: rcases eq_or_ne x 0 with (rfl | hx)
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
ι : Sort u_6
R : Type u_7
M : Type u_8
inst : Semiring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.IsTorsionFree R M
c : R
f : ι → M
⊢ HSMul.hSMul (β := M) c (∑ᶠ (i : ι), f i) = ∑ᶠ (i : ι), c • f i
have inl : HSMul.hSMul.{u_7, u_8, u_8} (α := R) (β := M) 0 (∑ᶠ (i : ι), f i) =
  ∑ᶠ (i : ι), HSMul.hSMul.{u_7, u_8, u_8} (α := R) 0 (f i)
Tactic: rcases eq_or_ne c 0 with (rfl | hc)
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
ι : Sort u_6
R : Type u_7
M : Type u_8
inst : Semiring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.IsTorsionFree R M
c : R
f : ι → M
inl :
  HSMul.hSMul.{u_7, u_8, u_8} (α := R) (β := M) 0 (∑ᶠ (i : ι), f i) =
    ∑ᶠ (i : ι), HSMul.hSMul.{u_7, u_8, u_8} (α := R) 0 (f i)
⊢ HSMul.hSMul (β := M) c (∑ᶠ (i : ι), f i) = ∑ᶠ (i : ι), c • f i
have inr : ∀ (hc : c ≠ 0), HSMul.hSMul (β := M) c (∑ᶠ (i : ι), f i) = ∑ᶠ (i : ι), c • f i
Tactic: rcases eq_or_ne c 0 with (rfl | hc)
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
a : α
⊢ ∏ᶠ (_ : f a ≠ 1), f a = f a
have rw : ∏ᶠ (_ : a ∈ mulSupport f), f a = f a
Tactic: rw [← mem_mulSupport, finprod_eq_mulIndicator_apply, mulIndicator_mulSupport]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
a : α
rw : ∏ᶠ (_ : a ∈ mulSupport f), f a = f a
⊢ ∏ᶠ (_ : f a ≠ 1), f a = f a
have rw₁ : (mulSupport f).mulIndicator f a = f a
Tactic: rw [← mem_mulSupport, finprod_eq_mulIndicator_apply, mulIndicator_mulSupport]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
a : α
rw : ∏ᶠ (_ : a ∈ mulSupport f), f a = f a
rw₁ : (mulSupport f).mulIndicator f a = f a
⊢ ∏ᶠ (_ : f a ≠ 1), f a = f a
have rw₂ : f a = f a
Tactic: rw [← mem_mulSupport, finprod_eq_mulIndicator_apply, mulIndicator_mulSupport]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (a : α) (_ : a ∈ mulSupport f), f a) (∏ᶠ (a : α), f a)
have rw : Eq.{u_5 + 1} (α := M) (∏ᶠ (a : α), (mulSupport f).mulIndicator f a) (∏ᶠ (a : α), f a)
Tactic: rw [finprod_mem_def, mulIndicator_mulSupport]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
rw : Eq.{u_5 + 1} (α := M) (∏ᶠ (a : α), (mulSupport f).mulIndicator f a) (∏ᶠ (a : α), f a)
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (a : α) (_ : a ∈ mulSupport f), f a) (∏ᶠ (a : α), f a)
have rw₁ : Eq.{u_5 + 1} (α := M) (∏ᶠ (a : α), f a) (∏ᶠ (a : α), f a)
Tactic: rw [finprod_mem_def, mulIndicator_mulSupport]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
s : Finset α
h : mulSupport f ⊆ (↑s : Set α)
⊢ mulSupport (f ∘ PLift.down) = (⇑(Equiv.symm Equiv.plift) : (a : α) → PLift α) '' mulSupport f
have rw : PLift.down ⁻¹' mulSupport f = (⇑(Equiv.symm Equiv.plift) : (a : α) → PLift α) '' mulSupport f
Tactic: rw [mulSupport_comp_eq_preimage]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (hypothesis)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
s : Finset α
h : mulSupport f ⊆ (↑s : Set α)
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α), f i) (∏ i ∈ s, f i)
have A : mulSupport (f ∘ PLift.down) = (⇑(Equiv.symm Equiv.plift) : (a : α) → PLift α) '' mulSupport f
Tactic: have A : mulSupport (f ∘ PLift.down) = Equiv.plift.symm '' mulSupport f := by
    rw [mulSupport_comp_eq_preimage]
    exact (Equiv.plift.symm.image_eq_preimage_symm _).symm
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
s : Finset α
h : mulSupport f ⊆ (↑s : Set α)
A : mulSupport (f ∘ PLift.down) = (⇑(Equiv.symm Equiv.plift) : (a : α) → PLift α) '' mulSupport f
⊢ mulSupport (f ∘ PLift.down) ⊆ (↑(Finset.map (Equiv.toEmbedding (Equiv.symm Equiv.plift)) s) : Set (PLift α))
have rw : Subset (α := Set (PLift α)) ((⇑(Equiv.symm Equiv.plift) : (a : α) → PLift α) '' mulSupport f)
  ((⇑(Equiv.toEmbedding (Equiv.symm Equiv.plift)) : (a : α) → PLift α) '' (↑s : Set α))
Tactic: rw [A, Finset.coe_map]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (hypothesis)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
s : Finset α
h : mulSupport f ⊆ (↑s : Set α)
A : mulSupport (f ∘ PLift.down) = (⇑(Equiv.symm Equiv.plift) : (a : α) → PLift α) '' mulSupport f
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α), f i) (∏ i ∈ s, f i)
have this : mulSupport (f ∘ PLift.down) ⊆ (↑(Finset.map (Equiv.toEmbedding (Equiv.symm Equiv.plift)) s) : Set (PLift α))
Tactic: have : mulSupport (f ∘ PLift.down) ⊆ s.map Equiv.plift.symm.toEmbedding := by
    rw [A, Finset.coe_map]
    exact image_mono h
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
s : Finset α
h : mulSupport f ⊆ (↑s : Set α)
A : mulSupport (f ∘ PLift.down) = (⇑(Equiv.symm Equiv.plift) : (a : α) → PLift α) '' mulSupport f
this : mulSupport (f ∘ PLift.down) ⊆ (↑(Finset.map (Equiv.toEmbedding (Equiv.symm Equiv.plift)) s) : Set (PLift α))
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α), f i) (∏ i ∈ s, f i)
have rw : Eq.{u_5 + 1} (α := M) (∏ i ∈ Finset.map (Equiv.toEmbedding (Equiv.symm Equiv.plift)) s, f i.down) (∏ i ∈ s, f i)
Tactic: rw [finprod_eq_prod_plift_of_mulSupport_subset this]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
s : Finset α
h : mulSupport f ⊆ (↑s : Set α)
A : mulSupport (f ∘ PLift.down) = (⇑(Equiv.symm Equiv.plift) : (a : α) → PLift α) '' mulSupport f
this : mulSupport (f ∘ PLift.down) ⊆ (↑(Finset.map (Equiv.toEmbedding (Equiv.symm Equiv.plift)) s) : Set (PLift α))
⊢ Eq.{u_5 + 1} (α := M) (∏ i ∈ Finset.map (Equiv.toEmbedding (Equiv.symm Equiv.plift)) s, f i.down) (∏ i ∈ s, f i)
have simp : Eq.{u_5 + 1} (α := M) (∏ x ∈ s, f (PLift.down ((Equiv.symm Equiv.plift : (a : α) → PLift α) x))) (∏ i ∈ s, f i)
Tactic: simp only [Finset.prod_map, Equiv.coe_toEmbedding]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
inst_1 : Decidable (HasFiniteMulSupport f)
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α), f i)
    (if h : HasFiniteMulSupport f then ∏ i ∈ Finite.toFinset (s := mulSupport f) h, f i else 1)
have pos : ∀ (h : HasFiniteMulSupport f),
  Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α), f i) (∏ i ∈ Finite.toFinset (s := mulSupport f) h, f i)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
inst_1 : Decidable (HasFiniteMulSupport f)
pos :
  ∀ (h : HasFiniteMulSupport f),
    Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α), f i) (∏ i ∈ Finite.toFinset (s := mulSupport f) h, f i)
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α), f i)
    (if h : HasFiniteMulSupport f then ∏ i ∈ Finite.toFinset (s := mulSupport f) h, f i else 1)
have neg : ∀ (h : ¬HasFiniteMulSupport f), Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α), f i) 1
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
inst_1 : Decidable (HasFiniteMulSupport f)
h : ¬HasFiniteMulSupport f
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α), f i) 1
have neg : ¬HasFiniteMulSupport.{u_1 + 1, u_5} (α := PLift α) (M := M) ((fun (i : α) ↦ f i) ∘ PLift.down)
Tactic: rw [finprod, dif_neg]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
inst_1 : Decidable (HasFiniteMulSupport f)
h : ¬HasFiniteMulSupport f
⊢ ¬HasFiniteMulSupport.{u_1 + 1, u_5} (α := PLift α) (M := M) ((fun (i : α) ↦ f i) ∘ PLift.down)
have neg : ¬Set.Finite.{u_1 + 1} (α := PLift α) (PLift.down ⁻¹' mulSupport.{u_1, u_5} (M := M) fun (i : α) ↦ f i)
Tactic: rw [HasFiniteMulSupport, mulSupport_comp_eq_preimage]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
hf : (mulSupport f).Infinite
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α), f i) 1
have rw : Eq.{u_5 + 1} (α := M) (if h : HasFiniteMulSupport f then ∏ i ∈ Finite.toFinset (s := mulSupport f) h, f i else 1) 1
Tactic: rw [finprod_def]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
hf : (mulSupport f).Infinite
⊢ Eq.{u_5 + 1} (α := M) (if h : (mulSupport f).Finite then ∏ i ∈ h.toFinset (s := mulSupport f), f i else 1) 1
have rw : Eq.{u_5 + 1} (α := M) 1 1
Tactic: rw [dif_neg hf]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
hf : (mulSupport f).Infinite
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α), f i) 1
have rw : Eq.{u_5 + 1} (α := M) (if h : HasFiniteMulSupport f then ∏ i ∈ Finite.toFinset (s := mulSupport f) h, f i else 1) 1
Tactic: classical
  rw [finprod_def]
  simp only [HasFiniteMulSupport]
  rw [dif_neg hf]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
hf : (mulSupport f).Infinite
rw rw₁ rw₂ :
  Eq.{u_5 + 1} (α := M) (if h : HasFiniteMulSupport f then ∏ i ∈ Finite.toFinset (s := mulSupport f) h, f i else 1) 1
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α), f i) 1
have rw₃ : Eq.{u_5 + 1} (α := M) (if h : (mulSupport f).Finite then ∏ i ∈ h.toFinset (s := mulSupport f), f i else 1) 1
Tactic: classical
  rw [finprod_def]
  simp only [HasFiniteMulSupport]
  rw [dif_neg hf]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
R : Type u_7
inst : NonAssocSemiring R
f : α → R
h : Eq.{u_7 + 1} (α := R) (∑ᶠ (i : α), f i) 1
⊢ HasFiniteSupport f
have inl : Subsingleton R → HasFiniteSupport f
Tactic: cases subsingleton_or_nontrivial R
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
R : Type u_7
inst : NonAssocSemiring R
f : α → R
h : Eq.{u_7 + 1} (α := R) (∑ᶠ (i : α), f i) 1
inl : Subsingleton R → HasFiniteSupport f
⊢ HasFiniteSupport f
have inr : Nontrivial R → HasFiniteSupport f
Tactic: cases subsingleton_or_nontrivial R
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
R : Type u_7
inst : NonAssocSemiring R
f : α → R
h : Eq.{u_7 + 1} (α := R) (∑ᶠ (i : α), f i) 1
h_1 : Subsingleton R
⊢ HasFiniteSupport f
have inl : (support f).Finite
Tactic: simp_rw [HasFiniteSupport, Subsingleton.support_eq, finite_empty]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
R : Type u_7
inst : NonAssocSemiring R
f : α → R
h : Eq.{u_7 + 1} (α := R) (∑ᶠ (i : α), f i) 1
h_1 : Subsingleton R
inl : (support f).Finite
⊢ HasFiniteSupport f
have inl₁ : Set.Finite.{u_1} (α := α) ∅
Tactic: simp_rw [HasFiniteSupport, Subsingleton.support_eq, finite_empty]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
R : Type u_7
inst : NonAssocSemiring R
f : α → R
h : Eq.{u_7 + 1} (α := R) (∑ᶠ (i : α), f i) 1
h_1 : Nontrivial R
⊢ HasFiniteSupport f
have inr : Ne.{u_7 + 1} (α := R) (∑ᶠ (i : α), f i) 0
Tactic: apply hasFiniteSupport_of_finsum_ne_zero
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
R : Type u_7
inst : NonAssocSemiring R
f : α → R
h : Eq.{u_7 + 1} (α := R) (∑ᶠ (i : α), f i) 1
h_1 : Nontrivial R
⊢ Ne.{u_7 + 1} (α := R) (∑ᶠ (i : α), f i) 0
have inr : Ne.{u_7 + 1} (α := R) 1 0
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
hf : HasFiniteMulSupport f
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α), f i) (∏ i ∈ Finite.toFinset (s := mulSupport f) hf, f i)
have rw : Eq.{u_5 + 1} (α := M) (if h : HasFiniteMulSupport f then ∏ i ∈ Finite.toFinset (s := mulSupport f) h, f i else 1)
  (∏ i ∈ Finite.toFinset (s := mulSupport f) hf, f i)
Tactic: rw [finprod_def, dif_pos hf]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
hf : HasFiniteMulSupport f
rw :
  Eq.{u_5 + 1} (α := M) (if h : HasFiniteMulSupport f then ∏ i ∈ Finite.toFinset (s := mulSupport f) h, f i else 1)
    (∏ i ∈ Finite.toFinset (s := mulSupport f) hf, f i)
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α), f i) (∏ i ∈ Finite.toFinset (s := mulSupport f) hf, f i)
have rw₁ : Eq.{u_5 + 1} (α := M) (∏ i ∈ Finite.toFinset (s := mulSupport f) hf, f i)
  (∏ i ∈ Finite.toFinset (s := mulSupport f) hf, f i)
Tactic: rw [finprod_def, dif_pos hf]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
hf : HasFiniteMulSupport f
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α), f i) (∏ i ∈ Finite.toFinset (s := mulSupport f) hf, f i)
have classical : Eq.{u_5 + 1} (α := M) (if h : HasFiniteMulSupport f then ∏ i ∈ Finite.toFinset (s := mulSupport f) h, f i else 1)
  (∏ i ∈ Finite.toFinset (s := mulSupport f) hf, f i)
Tactic: classical rw [finprod_def, dif_pos hf]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
hf : HasFiniteMulSupport f
classical :
  Eq.{u_5 + 1} (α := M) (if h : HasFiniteMulSupport f then ∏ i ∈ Finite.toFinset (s := mulSupport f) h, f i else 1)
    (∏ i ∈ Finite.toFinset (s := mulSupport f) hf, f i)
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α), f i) (∏ i ∈ Finite.toFinset (s := mulSupport f) hf, f i)
have classical₁ : Eq.{u_5 + 1} (α := M) (∏ i ∈ Finite.toFinset (s := mulSupport f) hf, f i)
  (∏ i ∈ Finite.toFinset (s := mulSupport f) hf, f i)
Tactic: classical rw [finprod_def, dif_pos hf]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M₀ : Type u_7
inst : CommMonoidWithZero M₀
inst_1 : Nontrivial M₀
inst_2 : NoZeroDivisors M₀
f : α → M₀
h : ∀ (i : α), f i ≠ 0
⊢ Ne.{u_7 + 1} (α := M₀) (∏ᶠ (i : α), f i) 0
have pos : ∀ (h₂ : (mulSupport f).Finite), Ne.{u_7 + 1} (α := M₀) (∏ᶠ (i : α), f i) 0
Tactic: by_cases h₂ : Set.Finite f.mulSupport
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M₀ : Type u_7
inst : CommMonoidWithZero M₀
inst_1 : Nontrivial M₀
inst_2 : NoZeroDivisors M₀
f : α → M₀
h : ∀ (i : α), f i ≠ 0
pos : ∀ (h₂ : (mulSupport f).Finite), Ne.{u_7 + 1} (α := M₀) (∏ᶠ (i : α), f i) 0
⊢ Ne.{u_7 + 1} (α := M₀) (∏ᶠ (i : α), f i) 0
have neg : ∀ (h₂ : ¬(mulSupport f).Finite), Ne.{u_7 + 1} (α := M₀) (∏ᶠ (i : α), f i) 0
Tactic: by_cases h₂ : Set.Finite f.mulSupport
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
p : α → Prop
t : Finset α
h : ∀ {x : α}, f x ≠ 1 → (p x ↔ x ∈ t)
s : Set α := {x : α | p x}
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : p i), f i) (∏ i ∈ t, f i)
have change : Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ∈ s), f i) (∏ i ∈ t, f i)
Tactic: change ∏ᶠ (i : α) (_ : i ∈ s), f i = ∏ i ∈ t, f i
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
p : α → Prop
t : Finset α
h : ∀ {x : α}, f x ≠ 1 → (p x ↔ x ∈ t)
s : Set α := {x : α | p x}
⊢ mulSupport (s.mulIndicator f) ⊆ (↑t : Set α)
have rw : s ∩ mulSupport f ⊆ (↑t : Set α)
Tactic: rw [Set.mulSupport_mulIndicator]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (hypothesis)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
p : α → Prop
t : Finset α
h : ∀ {x : α}, f x ≠ 1 → (p x ↔ x ∈ t)
s : Set α := {x : α | p x}
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ∈ s), f i) (∏ i ∈ t, f i)
have this : mulSupport (s.mulIndicator f) ⊆ (↑t : Set α)
Tactic: have : mulSupport (s.mulIndicator f) ⊆ t := by
    rw [Set.mulSupport_mulIndicator]
    intro x hx
    exact (h hx.2).1 hx.1
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
p : α → Prop
t : Finset α
h : ∀ {x : α}, f x ≠ 1 → (p x ↔ x ∈ t)
s : Set α := {x : α | p x}
this : mulSupport (s.mulIndicator f) ⊆ (↑t : Set α)
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ∈ s), f i) (∏ i ∈ t, f i)
have rw : Eq.{u_5 + 1} (α := M) (∏ i ∈ t, s.mulIndicator f i) (∏ i ∈ t, f i)
Tactic: rw [finprod_mem_def, finprod_eq_prod_of_mulSupport_subset _ this]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
p : α → Prop
t : Finset α
h : ∀ {x : α}, f x ≠ 1 → (p x ↔ x ∈ t)
s : Set α := {x : α | p x}
this : mulSupport (s.mulIndicator f) ⊆ (↑t : Set α)
⊢ Eq.{u_5 + 1} (α := M) (∏ i ∈ t, s.mulIndicator f i) (∏ i ∈ t, f i)
have refine : ∀ (x : α) (hx : x ∈ t) (hxs : x ∉ s), f x = 1
Tactic: refine Finset.prod_congr rfl fun x hx => mulIndicator_apply_eq_self.2 fun hxs => ?_
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
p : α → Prop
t : Finset α
h : ∀ {x : α}, f x ≠ 1 → (p x ↔ x ∈ t)
s : Set α := {x : α | p x}
this : mulSupport (s.mulIndicator f) ⊆ (↑t : Set α)
x : α
hx : x ∈ t
hxs : x ∉ s
⊢ f x = 1
have contrapose! : ∀ (hxs : f x ≠ 1), x ∈ s
Tactic: contrapose! hxs
Cleared hypotheses: hxs
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
a : α
inst_1 : DecidableEq α
hf : HasFiniteMulSupport f
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ≠ a), f i) (∏ i ∈ (Finite.toFinset (s := mulSupport f) hf).erase a, f i)
have h : ∀ {x : α}, f x ≠ 1 → (x ≠ a ↔ x ∈ (Finite.toFinset (s := mulSupport f) hf).erase a)
Tactic: apply finprod_cond_eq_prod_of_cond_iff
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
a : α
inst_1 : DecidableEq α
hf : HasFiniteMulSupport f
x : α
hx : f x ≠ 1
⊢ x ≠ a ↔ x ∈ (Finite.toFinset (s := mulSupport f) hf).erase a
have h : x ≠ a ↔ x ≠ a ∧ f x ≠ 1
Tactic: rw [Finset.mem_erase, Finite.mem_toFinset, mem_mulSupport]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (hypothesis)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
s : Set α
t : Finset α
h : s ∩ mulSupport f = (↑t : Set α) ∩ mulSupport f
x : α
hxf : f x ≠ 1
⊢ x ∈ s ↔ x ∈ t
have hxf₁ : x ∈ mulSupport f
Tactic: rw [← mem_mulSupport] at hxf
Cleared hypotheses: hxf
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
s : Set α
t : Finset α
h : s ∩ mulSupport f = (↑t : Set α) ∩ mulSupport f
x : α
hxf : x ∈ mulSupport f
⊢ x ∈ s ↔ x ∈ t
have refine_1 : ∀ (hx : x ∈ s), x ∈ t
Tactic: refine ⟨fun hx => ?_, fun hx => ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
s : Set α
t : Finset α
h : s ∩ mulSupport f = (↑t : Set α) ∩ mulSupport f
x : α
hxf : x ∈ mulSupport f
refine_1 : ∀ (hx : x ∈ s), x ∈ t
⊢ x ∈ s ↔ x ∈ t
have refine_2 : ∀ (hx : x ∈ t), x ∈ s
Tactic: refine ⟨fun hx => ?_, fun hx => ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
s : Set α
t : Finset α
h : s ∩ mulSupport f = (↑t : Set α) ∩ mulSupport f
x : α
hxf : x ∈ mulSupport f
hx : x ∈ s
⊢ x ∈ t
have refine_1 : x ∈ (↑t : Set α) ∩ mulSupport f
Tactic: refine ((mem_inter_iff x t (mulSupport f)).mp ?_).1
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
s : Set α
t : Finset α
h : s ∩ mulSupport f = (↑t : Set α) ∩ mulSupport f
x : α
hxf : x ∈ mulSupport f
hx : x ∈ s
⊢ x ∈ (↑t : Set α) ∩ mulSupport f
have refine_1 : x ∈ s ∧ x ∈ mulSupport f
Tactic: rw [← Set.ext_iff.mp h x, mem_inter_iff]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
s : Set α
t : Finset α
h : s ∩ mulSupport f = (↑t : Set α) ∩ mulSupport f
x : α
hxf : x ∈ mulSupport f
hx : x ∈ t
⊢ x ∈ s
have refine_2 : x ∈ s ∩ mulSupport f
Tactic: refine ((mem_inter_iff x s (mulSupport f)).mp ?_).1
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
s : Set α
t : Finset α
h : s ∩ mulSupport f = (↑t : Set α) ∩ mulSupport f
x : α
hxf : x ∈ mulSupport f
hx : x ∈ t
⊢ x ∈ s ∩ mulSupport f
have refine_2 : x ∈ (↑t : Set α) ∧ x ∈ mulSupport f
Tactic: rw [Set.ext_iff.mp h x, mem_inter_iff]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
s : Set α
inst_1 : DecidablePred fun (x : α) ↦ x ∈ s
hf : HasFiniteMulSupport f
⊢ s ∩ mulSupport f = (↑({i ∈ Finite.toFinset (s := mulSupport f) hf | i ∈ s}) : Set α) ∩ mulSupport f
have h : ∀ (x : α), x ∈ s ∩ mulSupport f ↔ x ∈ (↑({i ∈ Finite.toFinset (s := mulSupport f) hf | i ∈ s}) : Set α) ∩ mulSupport f
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
s : Set α
hs : s.Finite
⊢ s ∩ mulSupport f = (↑(hs.toFinset (s := s)) : Set α) ∩ mulSupport f
have rw : s ∩ mulSupport f = s ∩ mulSupport f
Tactic: rw [hs.coe_toFinset]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
s : Set α
hs : (s ∩ mulSupport f).Infinite
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ∈ s), f i) 1
have rw : Eq.{u_5 + 1} (α := M) (∏ᶠ (a : α), s.mulIndicator f a) 1
Tactic: rw [finprod_mem_def]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
s : Set α
hs : (s ∩ mulSupport f).Infinite
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (a : α), s.mulIndicator f a) 1
have hf : (mulSupport (s.mulIndicator f)).Infinite
Tactic: apply finprod_of_infinite_mulSupport
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
s : Set α
hs : (s ∩ mulSupport f).Infinite
⊢ (mulSupport (s.mulIndicator f)).Infinite
have hf : ∀ (hs : (mulSupport (s.mulIndicator f)).Infinite), (mulSupport (s.mulIndicator f)).Infinite
Tactic: rwa [← mulSupport_mulIndicator] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
s : Set α
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∩ mulSupport f), f i) (∏ᶠ (i : α) (_ : i ∈ s), f i)
have rw : Eq.{u_5 + 1} (α := M) (∏ᶠ (a : α), (s ∩ mulSupport f).mulIndicator f a) (∏ᶠ (i : α) (_ : i ∈ s), f i)
Tactic: rw [finprod_mem_def, finprod_mem_def, mulIndicator_inter_mulSupport]