awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.BigOperators.Finprod
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
rw :
  Subset (α := Set (PLift α)) ((⇑(Equiv.symm Equiv.plift) : (a : α) → PLift α) '' mulSupport f)
    ((⇑(Equiv.toEmbedding (Equiv.symm Equiv.plift)) : (a : α) → PLift α) '' (↑s : Set α))
⊢ mulSupport (f ∘ PLift.down) ⊆ (↑(Finset.map (Equiv.toEmbedding (Equiv.symm Equiv.plift)) s) : Set (PLift α))

Tactic:
rw [A, Finset.coe_map]

Premises used: Finset.coe_map
-- Module: Mathlib.Algebra.BigOperators.Finprod
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
⊢ Subset (α := Set (PLift α)) ((⇑(Equiv.symm Equiv.plift) : (a : α) → PLift α) '' mulSupport f)
    ((⇑(Equiv.toEmbedding (Equiv.symm Equiv.plift)) : (a : α) → PLift α) '' (↑s : Set α))

Tactic:
image_mono h

Premises used: Set.image_mono
-- Module: Mathlib.Algebra.BigOperators.Finprod
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
⊢ Subset (α := Set (PLift α)) ((⇑(Equiv.symm Equiv.plift) : (a : α) → PLift α) '' mulSupport f)
    ((⇑(Equiv.toEmbedding (Equiv.symm Equiv.plift)) : (a : α) → PLift α) '' (↑s : Set α))

Tactic:
exact image_mono h

Premises used: Set.image_mono
-- Module: Mathlib.Algebra.BigOperators.Finprod
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 α))

Tactic:
have : mulSupport (f ∘ PLift.down) ⊆ s.map Equiv.plift.symm.toEmbedding := by
    rw [A, Finset.coe_map]
    exact image_mono h
-- Module: Mathlib.Algebra.BigOperators.Finprod
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 α))
rw : Eq.{u_5 + 1} (α := M) (∏ i ∈ Finset.map (Equiv.toEmbedding (Equiv.symm Equiv.plift)) s, f i.down) (∏ i ∈ s, f i)
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α), f i) (∏ i ∈ s, f i)

Tactic:
rw [finprod_eq_prod_plift_of_mulSupport_subset this]

Premises used: finprod_eq_prod_plift_of_mulSupport_subset
-- Module: Mathlib.Algebra.BigOperators.Finprod
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 α))
simp : Eq.{u_5 + 1} (α := M) (∏ x ∈ s, f (PLift.down ((Equiv.symm Equiv.plift : (a : α) → PLift α) x))) (∏ i ∈ s, f i)
⊢ Eq.{u_5 + 1} (α := M) (∏ i ∈ Finset.map (Equiv.toEmbedding (Equiv.symm Equiv.plift)) s, f i.down) (∏ i ∈ s, f i)

Tactic:
simp only [Finset.prod_map, Equiv.coe_toEmbedding]

Premises used: Equiv.coe_toEmbedding, Finset.prod_map
-- Module: Mathlib.Algebra.BigOperators.Finprod
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) (∏ x ∈ s, f (PLift.down ((Equiv.symm Equiv.plift : (a : α) → PLift α) x))) (∏ i ∈ s, f i)

Tactic:
congr
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
hf : HasFiniteMulSupport f
s : Finset α
h : Finite.toFinset (s := mulSupport f) hf ⊆ s
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α), f i) (∏ i ∈ s, f i)

Tactic:
finprod_eq_prod_of_mulSupport_subset _ fun _ hx => h <| hf.mem_toFinset.2 hx

Premises used: Iff.mpr, Set.Finite.mem_toFinset, finprod_eq_prod_of_mulSupport_subset
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
s : Set α
h : mulSupport f ⊆ s
hs : s.Finite
rwa rwa₁ rwa₂ rwa₃ : mulSupport f ⊆ s
⊢ mulSupport f ⊆ (↑(hs.toFinset (s := s)) : Set α)

Tactic:
rwa [Set.Finite.coe_toFinset]

Premises used: Set.Finite.coe_toFinset
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
s : Finset α
h : mulSupport f ⊆ (↑s : Set α)
⊢ ⋯.toFinset (s := mulSupport f) ⊆ s

Tactic:
simpa [← Finset.coe_subset, Set.coe_toFinset]

Premises used: Set.coe_toFinset, Finset.coe_subset
-- Module: Mathlib.Algebra.BigOperators.Finprod
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)
neg : ∀ (h : ¬HasFiniteMulSupport f), Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α), f i) 1
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α), f i)
    (if h : HasFiniteMulSupport f then ∏ i ∈ Finite.toFinset (s := mulSupport f) h, f i else 1)

Tactic:
split_ifs with h
-- Module: Mathlib.Algebra.BigOperators.Finprod
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) (∏ i ∈ Finite.toFinset (s := mulSupport f) h, f i)

Tactic:
finprod_eq_prod_of_mulSupport_toFinset_subset _ h (Finset.Subset.refl _)

Premises used: Finset.Subset.refl, finprod_eq_prod_of_mulSupport_toFinset_subset
-- Module: Mathlib.Algebra.BigOperators.Finprod
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) (∏ i ∈ Finite.toFinset (s := mulSupport f) h, f i)

Tactic:
exact finprod_eq_prod_of_mulSupport_toFinset_subset _ h (Finset.Subset.refl _)

Premises used: Finset.Subset.refl, finprod_eq_prod_of_mulSupport_toFinset_subset
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
inst_1 : Decidable (HasFiniteMulSupport f)
h : ¬HasFiniteMulSupport f
neg : ¬HasFiniteMulSupport.{u_1 + 1, u_5} (α := PLift α) (M := M) ((fun (i : α) ↦ f i) ∘ PLift.down)
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α), f i) 1

Tactic:
rw [finprod, dif_neg]

Premises used: dif_neg, finprod
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
inst_1 : Decidable (HasFiniteMulSupport f)
h : ¬HasFiniteMulSupport f
neg : ¬Set.Finite.{u_1 + 1} (α := PLift α) (PLift.down ⁻¹' mulSupport.{u_1, u_5} (M := M) fun (i : α) ↦ f i)
⊢ ¬HasFiniteMulSupport.{u_1 + 1, u_5} (α := PLift α) (M := M) ((fun (i : α) ↦ f i) ∘ PLift.down)

Tactic:
rw [HasFiniteMulSupport, mulSupport_comp_eq_preimage]

Premises used: Function.mulSupport_comp_eq_preimage, Function.HasFiniteMulSupport
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
inst_1 : Decidable (HasFiniteMulSupport f)
h : ¬HasFiniteMulSupport f
⊢ ¬Set.Finite.{u_1 + 1} (α := PLift α) (PLift.down ⁻¹' mulSupport.{u_1, u_5} (M := M) fun (i : α) ↦ f i)

Tactic:
mt (fun hf => hf.of_preimage Equiv.plift.surjective) h

Premises used: mt, Set.Finite.of_preimage, Equiv.plift, Equiv.surjective
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
inst_1 : Decidable (HasFiniteMulSupport f)
h : ¬HasFiniteMulSupport f
⊢ ¬Set.Finite.{u_1 + 1} (α := PLift α) (PLift.down ⁻¹' mulSupport.{u_1, u_5} (M := M) fun (i : α) ↦ f i)

Tactic:
exact mt (fun hf => hf.of_preimage Equiv.plift.surjective) h

Premises used: mt
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
hf : (mulSupport f).Infinite
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

Tactic:
rw [finprod_def]

Premises used: finprod_def
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
hf : (mulSupport f).Infinite
rw rw₁ : Eq.{u_5 + 1} (α := M) 1 1
⊢ Eq.{u_5 + 1} (α := M) (if h : (mulSupport f).Finite then ∏ i ∈ h.toFinset (s := mulSupport f), f i else 1) 1

Tactic:
rw [dif_neg hf]

Premises used: dif_neg
-- Module: Mathlib.Algebra.BigOperators.Finprod
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
rw₃ : Eq.{u_5 + 1} (α := M) (if h : (mulSupport f).Finite then ∏ i ∈ h.toFinset (s := mulSupport f), f i else 1) 1
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α), f i) 1

Tactic:
classical
  rw [finprod_def]
  simp only [HasFiniteMulSupport]
  rw [dif_neg hf]

Premises used: dif_neg, Function.HasFiniteMulSupport, finprod_def
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
hf : ¬HasFiniteMulSupport f
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α), f i) 1

Tactic:
finprod_of_infinite_mulSupport <| Set.not_finite.mp hf

Premises used: Set.not_finite, finprod_of_infinite_mulSupport, Iff.mp
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
h : Ne.{u_5 + 1} (α := M) (∏ᶠ (i : α), f i) 1
⊢ HasFiniteMulSupport f

Tactic:
not_infinite.mp <| (finprod_of_infinite_mulSupport ·).mt h

Premises used: Function.mt, Set.not_infinite, finprod_of_infinite_mulSupport, Iff.mp, Function.HasFiniteMulSupport
-- Module: Mathlib.Algebra.BigOperators.Finprod
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
inr : Nontrivial R → HasFiniteSupport f
⊢ HasFiniteSupport f

Tactic:
cases subsingleton_or_nontrivial R

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.Algebra.BigOperators.Finprod
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
inl₁ : Set.Finite.{u_1} (α := α) ∅
⊢ HasFiniteSupport f

Tactic:
simp_rw [HasFiniteSupport, Subsingleton.support_eq, finite_empty]

Premises used: Set.finite_empty, Function.HasFiniteSupport, Subsingleton.support_eq
-- Module: Mathlib.Algebra.BigOperators.Finprod
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
inr : Ne.{u_7 + 1} (α := R) (∑ᶠ (i : α), f i) 0
⊢ HasFiniteSupport f

Tactic:
apply hasFiniteSupport_of_finsum_ne_zero

Premises used: hasFiniteSupport_of_finsum_ne_zero
-- Module: Mathlib.Algebra.BigOperators.Finprod
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
inr : Ne.{u_7 + 1} (α := R) 1 0
⊢ Ne.{u_7 + 1} (α := R) (∑ᶠ (i : α), f i) 0

Tactic:
rw [h]
-- Module: Mathlib.Algebra.BigOperators.Finprod
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) 1 0

Tactic:
one_ne_zero

Premises used: one_ne_zero
-- Module: Mathlib.Algebra.BigOperators.Finprod
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) 1 0

Tactic:
exact one_ne_zero

Premises used: one_ne_zero
-- Module: Mathlib.Algebra.BigOperators.Finprod
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)
rw₁ rw₂ :
  Eq.{u_5 + 1} (α := M) (∏ i ∈ Finite.toFinset (s := mulSupport f) hf, f i)
    (∏ 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)

Tactic:
rw [finprod_def, dif_pos hf]

Premises used: dif_pos, finprod_def
-- Module: Mathlib.Algebra.BigOperators.Finprod
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)
classical₁ classical₂ :
  Eq.{u_5 + 1} (α := M) (∏ i ∈ Finite.toFinset (s := mulSupport f) hf, f i)
    (∏ 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)

Tactic:
classical rw [finprod_def, dif_pos hf]

Premises used: dif_pos, finprod_def
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
inst_1 : Fintype α
f : α → M
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α), f i) (∏ i : α, f i)

Tactic:
finprod_eq_prod_of_mulSupport_toFinset_subset _ (Set.toFinite _) <| Finset.subset_univ _

Premises used: finprod_eq_prod_of_mulSupport_toFinset_subset, Set.toFinite, Finset.subset_univ
-- Module: Mathlib.Algebra.BigOperators.Finprod
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
neg : ∀ (h₂ : ¬(mulSupport f).Finite), Ne.{u_7 + 1} (α := M₀) (∏ᶠ (i : α), f i) 0
⊢ Ne.{u_7 + 1} (α := M₀) (∏ᶠ (i : α), f i) 0

Tactic:
by_cases h₂ : Set.Finite f.mulSupport

Premises used: Set.Finite, Function.mulSupport
-- Module: Mathlib.Algebra.BigOperators.Finprod
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
h₂ : (mulSupport f).Finite
⊢ Ne.{u_7 + 1} (α := M₀) (∏ᶠ (i : α), f i) 0

Tactic:
grind [finprod_eq_prod f h₂, Finset.prod_ne_zero_iff]

Premises used: Finset.prod_ne_zero_iff, finprod_eq_prod
-- Module: Mathlib.Algebra.BigOperators.Finprod
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
h₂ : ¬(mulSupport f).Finite
⊢ Ne.{u_7 + 1} (α := M₀) (∏ᶠ (i : α), f i) 0

Tactic:
simp [finprod_of_infinite_mulSupport h₂]

Premises used: finprod_of_infinite_mulSupport
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
M : Type u_5
N : Type u_6
inst : CommMonoid M
inst_1 : CommMonoid N
α : Type u_7
F : Type u_8
inst_2 : Fintype α
inst_3 : EquivLike F M N
inst_4 : MulEquivClass F M N
f : F
g : α → M
⊢ Eq.{u_6 + 1} (α := N) ((f : (a : M) → N) (∏ i : α, g i) : N) (∏ i : α, (f : (a : M) → N) (g i) : N)

Tactic:
simp [← finprod_eq_prod_of_fintype, MulEquivClass.map_finprod]

Premises used: MulEquivClass.map_finprod, finprod_eq_prod_of_fintype
-- Module: Mathlib.Algebra.BigOperators.Finprod
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}
change : Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ∈ s), f i) (∏ i ∈ t, f i)
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : p i), f i) (∏ i ∈ t, f i)

Tactic:
change ∏ᶠ (i : α) (_ : i ∈ s), f i = ∏ i ∈ t, f i
-- Module: Mathlib.Algebra.BigOperators.Finprod
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}
rw : s ∩ mulSupport f ⊆ (↑t : Set α)
⊢ mulSupport (s.mulIndicator f) ⊆ (↑t : Set α)

Tactic:
rw [Set.mulSupport_mulIndicator]

Premises used: Set.mulSupport_mulIndicator
-- Module: Mathlib.Algebra.BigOperators.Finprod
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}
x : α
hx : x ∈ s ∩ mulSupport f
⊢ x ∈ (↑t : Set α)

Tactic:
(h hx.2).1 hx.1

Premises used: And.right, And.left, Iff.mp
-- Module: Mathlib.Algebra.BigOperators.Finprod
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}
x : α
hx : x ∈ s ∩ mulSupport f
⊢ x ∈ (↑t : Set α)

Tactic:
exact (h hx.2).1 hx.1

Premises used: And.right, And.left, Iff.mp
-- Module: Mathlib.Algebra.BigOperators.Finprod
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 α)

Tactic:
have : mulSupport (s.mulIndicator f) ⊆ t := by
    rw [Set.mulSupport_mulIndicator]
    intro x hx
    exact (h hx.2).1 hx.1
-- Module: Mathlib.Algebra.BigOperators.Finprod
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 α)
rw : Eq.{u_5 + 1} (α := M) (∏ i ∈ t, s.mulIndicator f i) (∏ i ∈ t, f i)
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ∈ s), f i) (∏ i ∈ t, f i)

Tactic:
rw [finprod_mem_def, finprod_eq_prod_of_mulSupport_subset _ this]

Premises used: finprod_mem_def, finprod_eq_prod_of_mulSupport_subset
-- Module: Mathlib.Algebra.BigOperators.Finprod
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)

Tactic:
Finset.prod_congr rfl fun x hx => mulIndicator_apply_eq_self.2 fun hxs => ?_

Premises used: Iff.mpr, Finset.prod_congr, Set.mulIndicator_apply_eq_self, rfl
-- Module: Mathlib.Algebra.BigOperators.Finprod
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 α)
refine : ∀ (x : α) (hx : x ∈ t) (hxs : x ∉ s), f x = 1
⊢ Eq.{u_5 + 1} (α := M) (∏ i ∈ t, s.mulIndicator f i) (∏ i ∈ t, f i)

Tactic:
refine Finset.prod_congr rfl fun x hx => mulIndicator_apply_eq_self.2 fun hxs => ?_

Premises used: Iff.mpr, Finset.prod_congr, Set.mulIndicator_apply_eq_self, rfl
-- Module: Mathlib.Algebra.BigOperators.Finprod
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
contrapose! : ∀ (hxs : f x ≠ 1), x ∈ s
⊢ f x = 1

Tactic:
contrapose! hxs
-- Module: Mathlib.Algebra.BigOperators.Finprod
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 : f x ≠ 1
⊢ x ∈ s

Tactic:
(h hxs).2 hx

Premises used: Iff.mpr, Set.Mem, setOf
-- Module: Mathlib.Algebra.BigOperators.Finprod
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 : f x ≠ 1
⊢ x ∈ s

Tactic:
exact (h hxs).2 hx

Premises used: Iff.mpr
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
a : α
inst_1 : DecidableEq α
hf : HasFiniteMulSupport f
h : ∀ {x : α}, f x ≠ 1 → (x ≠ a ↔ x ∈ (Finite.toFinset (s := mulSupport f) hf).erase a)
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ≠ a), f i) (∏ i ∈ (Finite.toFinset (s := mulSupport f) hf).erase a, f i)

Tactic:
apply finprod_cond_eq_prod_of_cond_iff

Premises used: finprod_cond_eq_prod_of_cond_iff
-- Module: Mathlib.Algebra.BigOperators.Finprod
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
h : x ≠ a ↔ x ≠ a ∧ f x ≠ 1
⊢ x ≠ a ↔ x ∈ (Finite.toFinset (s := mulSupport f) hf).erase a

Tactic:
rw [Finset.mem_erase, Finite.mem_toFinset, mem_mulSupport]

Premises used: Set.Finite.mem_toFinset, Function.mem_mulSupport, Finset.mem_erase
-- Module: Mathlib.Algebra.BigOperators.Finprod
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 ≠ a ∧ f x ≠ 1

Tactic:
grind
-- Module: Mathlib.Algebra.BigOperators.Finprod
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 ∈ mulSupport f

Tactic:
rw [← mem_mulSupport] at hxf

Premises used: Function.mem_mulSupport
-- Module: Mathlib.Algebra.BigOperators.Finprod
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

Tactic:
⟨fun hx => ?_, fun hx => ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Algebra.BigOperators.Finprod
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
refine_2 : ∀ (hx : x ∈ t), x ∈ s
⊢ x ∈ s ↔ x ∈ t

Tactic:
refine ⟨fun hx => ?_, fun hx => ?_⟩
-- Module: Mathlib.Algebra.BigOperators.Finprod
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

Tactic:
((mem_inter_iff x t (mulSupport f)).mp ?_).1

Premises used: Set.mem_inter_iff, SetLike.coe, And.left, Iff.mp, Function.mulSupport
-- Module: Mathlib.Algebra.BigOperators.Finprod
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
refine_1 : x ∈ (↑t : Set α) ∩ mulSupport f
⊢ x ∈ t

Tactic:
refine ((mem_inter_iff x t (mulSupport f)).mp ?_).1

Premises used: Set.mem_inter_iff, SetLike.coe, And.left, Iff.mp, Function.mulSupport
-- Module: Mathlib.Algebra.BigOperators.Finprod
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
refine_1 : x ∈ s ∧ x ∈ mulSupport f
⊢ x ∈ (↑t : Set α) ∩ mulSupport f

Tactic:
rw [← Set.ext_iff.mp h x, mem_inter_iff]

Premises used: Set.mem_inter_iff, Iff.mp, Set.ext_iff
-- Module: Mathlib.Algebra.BigOperators.Finprod
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 ∈ s ∧ x ∈ mulSupport f

Tactic:
⟨hx, hxf⟩

Premises used: And.intro
-- Module: Mathlib.Algebra.BigOperators.Finprod
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 ∈ s ∧ x ∈ mulSupport f

Tactic:
exact ⟨hx, hxf⟩
-- Module: Mathlib.Algebra.BigOperators.Finprod
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

Tactic:
((mem_inter_iff x s (mulSupport f)).mp ?_).1

Premises used: Set.mem_inter_iff, And.left, Iff.mp, Function.mulSupport
-- Module: Mathlib.Algebra.BigOperators.Finprod
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
refine_2 : x ∈ s ∩ mulSupport f
⊢ x ∈ s

Tactic:
refine ((mem_inter_iff x s (mulSupport f)).mp ?_).1

Premises used: Set.mem_inter_iff, And.left, Iff.mp, Function.mulSupport