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 : Set α
t : Finset α
h : s ∩ mulSupport f = (↑t : Set α) ∩ mulSupport f
x : α
hxf : x ∈ mulSupport f
hx : x ∈ t
refine_2 : x ∈ (↑t : Set α) ∧ x ∈ mulSupport f
⊢ x ∈ s ∩ 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 ∈ t
⊢ x ∈ (↑t : Set α) ∧ 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 ∈ t
⊢ x ∈ (↑t : Set α) ∧ 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 α)
h₂ : (↑t : Set α) ⊆ s
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ∈ s), f i) (∏ i ∈ t, f i)

Tactic:
finprod_cond_eq_prod_of_cond_iff _ fun hx => ⟨fun h => h₁ ⟨h, hx⟩, fun h => h₂ h⟩

Premises used: And.intro, Iff.intro, 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
s : Set α
hf : (s ∩ mulSupport f).Finite
⊢ s ∩ mulSupport f = (↑(hf.toFinset (s := s ∩ mulSupport f)) : Set α) ∩ mulSupport f

Tactic:
simp [inter_assoc]

Premises used: Set.inter_assoc
-- Module: Mathlib.Algebra.BigOperators.Finprod
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
h :
  ∀ (x : α), x ∈ s ∩ mulSupport f ↔ x ∈ (↑({i ∈ Finite.toFinset (s := mulSupport f) hf | i ∈ s}) : Set α) ∩ mulSupport f
⊢ s ∩ mulSupport f = (↑({i ∈ Finite.toFinset (s := mulSupport f) hf | i ∈ s}) : Set α) ∩ mulSupport f

Tactic:
ext x
-- Module: Mathlib.Algebra.BigOperators.Finprod
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
x : α
⊢ x ∈ s ∩ mulSupport f ↔ x ∈ (↑({i ∈ Finite.toFinset (s := mulSupport f) hf | i ∈ s}) : Set α) ∩ mulSupport f

Tactic:
simp [and_comm]

Premises used: and_comm
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
s : Set α
inst_1 : Fintype (↑s : Type u_1)
⊢ s ∩ mulSupport f = (↑s.toFinset : Set α) ∩ mulSupport f

Tactic:
simp_rw [coe_toFinset s]

Premises used: Set.coe_toFinset
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
s : Set α
hs : s.Finite
rw rw₁ : s ∩ mulSupport f = s ∩ mulSupport f
⊢ s ∩ mulSupport f = (↑(hs.toFinset (s := s)) : Set α) ∩ mulSupport f

Tactic:
rw [hs.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 α
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ∈ s), f i) (∏ i ∈ s, f i)

Tactic:
finprod_mem_eq_prod_of_inter_mulSupport_eq _ rfl

Premises used: finprod_mem_eq_prod_of_inter_mulSupport_eq, rfl
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
s : Finset α
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ∈ (↑s : Set α)), f i) (∏ i ∈ s, f i)

Tactic:
finprod_mem_eq_prod_of_inter_mulSupport_eq _ rfl

Premises used: finprod_mem_eq_prod_of_inter_mulSupport_eq, rfl
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
s : Set α
hs : (s ∩ mulSupport f).Infinite
rw : Eq.{u_5 + 1} (α := M) (∏ᶠ (a : α), s.mulIndicator f a) 1
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ∈ s), f i) 1

Tactic:
rw [finprod_mem_def]

Premises used: finprod_mem_def
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
s : Set α
hs : (s ∩ mulSupport f).Infinite
hf : (mulSupport (s.mulIndicator f)).Infinite
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (a : α), s.mulIndicator f a) 1

Tactic:
apply finprod_of_infinite_mulSupport

Premises used: finprod_of_infinite_mulSupport
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
s : Set α
hs : (s ∩ mulSupport f).Infinite
hf hf₁ hf₂ hf₃ : ∀ (hs : (mulSupport (s.mulIndicator f)).Infinite), (mulSupport (s.mulIndicator f)).Infinite
⊢ (mulSupport (s.mulIndicator f)).Infinite

Tactic:
rwa [← mulSupport_mulIndicator] at hs

Premises used: Set.mulSupport_mulIndicator
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
s : Set α
h : ∀ x ∈ s, f x = 1
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ∈ s), f i) 1

Tactic:
simp +contextual [h]
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
s : Set α
rw : Eq.{u_5 + 1} (α := M) (∏ᶠ (a : α), (s ∩ mulSupport f).mulIndicator f a) (∏ᶠ (i : α) (_ : i ∈ s), f i)
rw₁ : Eq.{u_5 + 1} (α := M) (∏ᶠ (a : α), (s ∩ mulSupport f).mulIndicator f a) (∏ᶠ (a : α), s.mulIndicator f a)
rw₂ rw₃ : Eq.{u_5 + 1} (α := M) (∏ᶠ (a : α), s.mulIndicator f a) (∏ᶠ (a : α), s.mulIndicator f a)
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∩ mulSupport f), f i) (∏ᶠ (i : α) (_ : i ∈ s), f i)

Tactic:
rw [finprod_mem_def, finprod_mem_def, mulIndicator_inter_mulSupport]

Premises used: finprod_mem_def, Set.mulIndicator_inter_mulSupport
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
s t : Set α
h : s ∩ mulSupport f = t ∩ mulSupport f
rw : Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∩ mulSupport f), f i) (∏ᶠ (i : α) (_ : i ∈ t), f i)
rw₁ : Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ∈ t ∩ mulSupport f), f i) (∏ᶠ (i : α) (_ : i ∈ t), f i)
rw₂ rw₃ : Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ∈ t), f i) (∏ᶠ (i : α) (_ : i ∈ t), f i)
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ∈ s), f i) (∏ᶠ (i : α) (_ : i ∈ t), f i)

Tactic:
rw [← finprod_mem_inter_mulSupport, h, finprod_mem_inter_mulSupport]

Premises used: finprod_mem_inter_mulSupport
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
s t : Set α
h : ∀ x ∈ mulSupport f, x ∈ s ↔ x ∈ t
h₁ : s ∩ mulSupport f = t ∩ mulSupport f
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ∈ s), f i) (∏ᶠ (i : α) (_ : i ∈ t), f i)

Tactic:
apply finprod_mem_inter_mulSupport_eq

Premises used: finprod_mem_inter_mulSupport_eq
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
s t : Set α
h : ∀ x ∈ mulSupport f, x ∈ s ↔ x ∈ t
h₁ : ∀ (x : α), x ∈ s ∩ mulSupport f ↔ x ∈ t ∩ mulSupport f
⊢ s ∩ mulSupport f = t ∩ mulSupport f

Tactic:
ext x
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
s t : Set α
h : ∀ x ∈ mulSupport f, x ∈ s ↔ x ∈ t
x : α
⊢ x ∈ s ∩ mulSupport f ↔ x ∈ t ∩ mulSupport f

Tactic:
and_congr_left (h x)

Premises used: Set.Mem, setOf, Set.inter, and_congr_left
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
s t : Set α
h : ∀ x ∈ mulSupport f, x ∈ s ↔ x ∈ t
x : α
⊢ x ∈ s ∩ mulSupport f ↔ x ∈ t ∩ mulSupport f

Tactic:
exact and_congr_left (h x)

Premises used: and_congr_left
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : Membership.mem (γ := Set α) univ i), f i) (∏ᶠ (i : α), f i)

Tactic:
finprod_congr fun _ => finprod_true _

Premises used: finprod_true, finprod_congr
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f g : α → M
s t : Set α
h₀ : s = t
h₁ : ∀ x ∈ t, f x = g x
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ∈ s), f i) (∏ᶠ (i : α) (_ : i ∈ t), g i)

Tactic:
h₀.symm ▸ finprod_congr fun i => finprod_congr_Prop rfl (h₁ i)

Premises used: Eq.rec, finprod_congr_Prop, finprod_congr, Eq.symm, rfl
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
h : ∀ (x : α), f x = 1
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α), f i) 1

Tactic:
simp +contextual [h]
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
ι : Type u_3
M : Type u_7
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedCancelMonoid M
f : ι → M
p : ι → Prop
h : ∀ (i : ι), p i → 1 ≤ f i
h' : ∃ (i : ι), p i ∧ 1 < f i
hf : (mulSupport f ∩ {i : ι | p i}).Finite
rw : LT.lt.{u_7} (α := M) 1 (∏ i ∈ hf.toFinset (s := mulSupport f ∩ {i : ι | p i}), f i)
h₁ : ∀ {x : ι}, f x ≠ 1 → (p x ↔ x ∈ hf.toFinset (s := mulSupport f ∩ {i : ι | p i}))
⊢ LT.lt.{u_7} (α := M) 1 (∏ᶠ (i : ι) (_ : p i), f i)

Tactic:
rw [finprod_cond_eq_prod_of_cond_iff (t := hf.toFinset)]

Premises used: finprod_cond_eq_prod_of_cond_iff
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
ι : Type u_3
M : Type u_7
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedCancelMonoid M
f : ι → M
p : ι → Prop
h : ∀ (i : ι), p i → 1 ≤ f i
h' : ∃ (i : ι), p i ∧ 1 < f i
hf : (mulSupport f ∩ {i : ι | p i}).Finite
h₁ : ∀ i ∈ hf.toFinset (s := mulSupport f ∩ {i : ι | p i}), 1 ≤ f i
hs : ∃ i ∈ hf.toFinset (s := mulSupport f ∩ {i : ι | p i}), 1 < f i
⊢ LT.lt.{u_7} (α := M) 1 (∏ i ∈ hf.toFinset (s := mulSupport f ∩ {i : ι | p i}), f i)

Tactic:
apply Finset.one_lt_prod'

Premises used: Finset.one_lt_prod'
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
ι : Type u_3
M : Type u_7
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedCancelMonoid M
f : ι → M
p : ι → Prop
h : ∀ (i : ι), p i → 1 ≤ f i
h' : ∃ (i : ι), p i ∧ 1 < f i
hf : (mulSupport f ∩ {i : ι | p i}).Finite
⊢ ∀ i ∈ hf.toFinset (s := mulSupport f ∩ {i : ι | p i}), 1 ≤ f i

Tactic:
simp +contextual [h]
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
ι : Type u_3
M : Type u_7
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedCancelMonoid M
f : ι → M
p : ι → Prop
h : ∀ (i : ι), p i → 1 ≤ f i
h' : ∃ (i : ι), p i ∧ 1 < f i
hf : (mulSupport f ∩ {i : ι | p i}).Finite
⊢ ∃ i ∈ hf.toFinset (s := mulSupport f ∩ {i : ι | p i}), 1 < f i

Tactic:
aesop
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
ι : Type u_3
M : Type u_7
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedCancelMonoid M
f : ι → M
p : ι → Prop
h : ∀ (i : ι), p i → 1 ≤ f i
h' : ∃ (i : ι), p i ∧ 1 < f i
hf : (mulSupport f ∩ {i : ι | p i}).Finite
⊢ ∀ {x : ι}, f x ≠ 1 → (p x ↔ x ∈ hf.toFinset (s := mulSupport f ∩ {i : ι | p i}))

Tactic:
simp +contextual
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
ι : Type u_3
M : Type u_7
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedCancelMonoid M
f : ι → M
h : ∀ (i : ι), 1 ≤ f i
h' : ∃ (i : ι), 1 < f i
hf : HasFiniteMulSupport f
rw : LT.lt.{u_7} (α := M) 1 (∏ᶠ (i : ι) (_ : Membership.mem (γ := Set ι) univ i), f i)
⊢ LT.lt.{u_7} (α := M) 1 (∏ᶠ (i : ι), f i)

Tactic:
rw [← finprod_mem_univ]

Premises used: finprod_mem_univ
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
ι : Type u_3
M : Type u_7
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedCancelMonoid M
f : ι → M
h : ∀ (i : ι), 1 ≤ f i
h' : ∃ (i : ι), 1 < f i
hf : HasFiniteMulSupport f
h₁ : ∀ (i : ι), Membership.mem (γ := Set ι) univ i → 1 ≤ f i
h'₁ : ∃ (i : ι), Membership.mem (γ := Set ι) univ i ∧ 1 < f i
hf₁ : (mulSupport f ∩ {i : ι | Membership.mem (γ := Set ι) univ i}).Finite
⊢ LT.lt.{u_7} (α := M) 1 (∏ᶠ (i : ι) (_ : Membership.mem (γ := Set ι) univ i), f i)

Tactic:
apply one_lt_finprod_cond

Premises used: one_lt_finprod_cond
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
ι : Type u_3
M : Type u_7
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedCancelMonoid M
f : ι → M
h : ∀ (i : ι), 1 ≤ f i
h' : ∃ (i : ι), 1 < f i
hf : HasFiniteMulSupport f
⊢ ∀ (i : ι), Membership.mem (γ := Set ι) univ i → 1 ≤ f i

Tactic:
simpa
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
ι : Type u_3
M : Type u_7
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedCancelMonoid M
f : ι → M
h : ∀ (i : ι), 1 ≤ f i
h' : ∃ (i : ι), 1 < f i
hf : HasFiniteMulSupport f
⊢ ∃ (i : ι), Membership.mem (γ := Set ι) univ i ∧ 1 < f i

Tactic:
simpa
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
ι : Type u_3
M : Type u_7
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedCancelMonoid M
f : ι → M
h : ∀ (i : ι), 1 ≤ f i
h' : ∃ (i : ι), 1 < f i
hf : HasFiniteMulSupport f
⊢ (mulSupport f ∩ {i : ι | Membership.mem (γ := Set ι) univ i}).Finite

Tactic:
simpa
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f g : α → M
inst_1 : PartialOrder M
inst_2 : MulLeftMono M
hf : HasFiniteMulSupport f
hg : HasFiniteMulSupport g
h : f ≤ g
have :
  ∀ (this : Fintype (↑(mulSupport f ∪ mulSupport g) : Type u_1)),
    LE.le.{u_5} (α := M) (∏ᶠ (a : α), f a) (∏ᶠ (a : α), g a)
⊢ LE.le.{u_5} (α := M) (∏ᶠ (a : α), f a) (∏ᶠ (a : α), g a)

Tactic:
have : Fintype ↑(f.mulSupport ∪ g.mulSupport) := (hf.union hg).fintype
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f g : α → M
inst_1 : PartialOrder M
inst_2 : MulLeftMono M
hf : HasFiniteMulSupport f
hg : HasFiniteMulSupport g
h : f ≤ g
this : Fintype (↑(mulSupport f ∪ mulSupport g) : Type u_1)
s : Finset α := (mulSupport f ∪ mulSupport g).toFinset
⊢ mulSupport f ⊆ (↑s : Set α)

Tactic:
grind
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f g : α → M
inst_1 : PartialOrder M
inst_2 : MulLeftMono M
hf : HasFiniteMulSupport f
hg : HasFiniteMulSupport g
h : f ≤ g
this : Fintype (↑(mulSupport f ∪ mulSupport g) : Type u_1)
s : Finset α := (mulSupport f ∪ mulSupport g).toFinset
⊢ mulSupport g ⊆ (↑s : Set α)

Tactic:
grind
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f g : α → M
inst_1 : PartialOrder M
inst_2 : MulLeftMono M
hf : HasFiniteMulSupport f
hg : HasFiniteMulSupport g
h : f ≤ g
this : Fintype (↑(mulSupport f ∪ mulSupport g) : Type u_1)
s : Finset α := (mulSupport f ∪ mulSupport g).toFinset
rw : LE.le.{u_5} (α := M) (∏ i ∈ s, f i) (∏ i ∈ s, g i)
⊢ LE.le.{u_5} (α := M) (∏ᶠ (a : α), f a) (∏ᶠ (a : α), g a)

Tactic:
rw [finprod_eq_finsetProd_of_mulSupport_subset f (show f.mulSupport ⊆ s by grind),
    finprod_eq_finsetProd_of_mulSupport_subset g (show g.mulSupport ⊆ s by grind)]

Premises used: finprod_eq_finsetProd_of_mulSupport_subset
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f g : α → M
inst_1 : PartialOrder M
inst_2 : MulLeftMono M
hf : HasFiniteMulSupport f
hg : HasFiniteMulSupport g
h : f ≤ g
this : Fintype (↑(mulSupport f ∪ mulSupport g) : Type u_1)
s : Finset α := (mulSupport f ∪ mulSupport g).toFinset
⊢ LE.le.{u_5} (α := M) (∏ i ∈ s, f i) (∏ i ∈ s, g i)

Tactic:
Finset.prod_le_prod' fun i _ ↦ h i

Premises used: Finset.prod_le_prod'
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f g : α → M
inst_1 : PartialOrder M
inst_2 : MulLeftMono M
hf : HasFiniteMulSupport f
hg : HasFiniteMulSupport g
h : f ≤ g
this : Fintype (↑(mulSupport f ∪ mulSupport g) : Type u_1)
s : Finset α := (mulSupport f ∪ mulSupport g).toFinset
⊢ LE.le.{u_5} (α := M) (∏ i ∈ s, f i) (∏ i ∈ s, g i)

Tactic:
exact Finset.prod_le_prod' fun i _ ↦ h i

Premises used: Finset.prod_le_prod'
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_7
inst : CommMonoidWithZero M
inst_1 : PartialOrder M
inst_2 : ZeroLEOneClass M
inst_3 : PosMulMono M
f g : α → M
hf : HasFiniteMulSupport f
hf₀ : ∀ (a : α), 0 ≤ f a
hg : HasFiniteMulSupport g
h : f ≤ g
have :
  ∀ (this : Fintype (↑(mulSupport f ∪ mulSupport g) : Type u_1)),
    LE.le.{u_7} (α := M) (∏ᶠ (a : α), f a) (∏ᶠ (a : α), g a)
⊢ LE.le.{u_7} (α := M) (∏ᶠ (a : α), f a) (∏ᶠ (a : α), g a)

Tactic:
have : Fintype ↑(f.mulSupport ∪ g.mulSupport) := (hf.union hg).fintype
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_7
inst : CommMonoidWithZero M
inst_1 : PartialOrder M
inst_2 : ZeroLEOneClass M
inst_3 : PosMulMono M
f g : α → M
hf : HasFiniteMulSupport f
hf₀ : ∀ (a : α), 0 ≤ f a
hg : HasFiniteMulSupport g
h : f ≤ g
this : Fintype (↑(mulSupport f ∪ mulSupport g) : Type u_1)
s : Finset α := (mulSupport f ∪ mulSupport g).toFinset
⊢ mulSupport f ⊆ (↑s : Set α)

Tactic:
grind
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_7
inst : CommMonoidWithZero M
inst_1 : PartialOrder M
inst_2 : ZeroLEOneClass M
inst_3 : PosMulMono M
f g : α → M
hf : HasFiniteMulSupport f
hf₀ : ∀ (a : α), 0 ≤ f a
hg : HasFiniteMulSupport g
h : f ≤ g
this : Fintype (↑(mulSupport f ∪ mulSupport g) : Type u_1)
s : Finset α := (mulSupport f ∪ mulSupport g).toFinset
⊢ mulSupport g ⊆ (↑s : Set α)

Tactic:
grind
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_7
inst : CommMonoidWithZero M
inst_1 : PartialOrder M
inst_2 : ZeroLEOneClass M
inst_3 : PosMulMono M
f g : α → M
hf : HasFiniteMulSupport f
hf₀ : ∀ (a : α), 0 ≤ f a
hg : HasFiniteMulSupport g
h : f ≤ g
this : Fintype (↑(mulSupport f ∪ mulSupport g) : Type u_1)
s : Finset α := (mulSupport f ∪ mulSupport g).toFinset
rw : LE.le.{u_7} (α := M) (∏ i ∈ s, f i) (∏ i ∈ s, g i)
⊢ LE.le.{u_7} (α := M) (∏ᶠ (a : α), f a) (∏ᶠ (a : α), g a)

Tactic:
rw [finprod_eq_finsetProd_of_mulSupport_subset f (show f.mulSupport ⊆ s by grind),
    finprod_eq_finsetProd_of_mulSupport_subset g (show g.mulSupport ⊆ s by grind)]

Premises used: finprod_eq_finsetProd_of_mulSupport_subset
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_7
inst : CommMonoidWithZero M
inst_1 : PartialOrder M
inst_2 : ZeroLEOneClass M
inst_3 : PosMulMono M
f g : α → M
hf : HasFiniteMulSupport f
hf₀ : ∀ (a : α), 0 ≤ f a
hg : HasFiniteMulSupport g
h : f ≤ g
this : Fintype (↑(mulSupport f ∪ mulSupport g) : Type u_1)
s : Finset α := (mulSupport f ∪ mulSupport g).toFinset
⊢ LE.le.{u_7} (α := M) (∏ i ∈ s, f i) (∏ i ∈ s, g i)

Tactic:
Finset.prod_le_prod (fun i _ ↦ hf₀ i) fun i _ ↦ h i

Premises used: Finset.prod_le_prod
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_7
inst : CommMonoidWithZero M
inst_1 : PartialOrder M
inst_2 : ZeroLEOneClass M
inst_3 : PosMulMono M
f g : α → M
hf : HasFiniteMulSupport f
hf₀ : ∀ (a : α), 0 ≤ f a
hg : HasFiniteMulSupport g
h : f ≤ g
this : Fintype (↑(mulSupport f ∪ mulSupport g) : Type u_1)
s : Finset α := (mulSupport f ∪ mulSupport g).toFinset
⊢ LE.le.{u_7} (α := M) (∏ i ∈ s, f i) (∏ i ∈ s, g i)

Tactic:
exact Finset.prod_le_prod (fun i _ ↦ hf₀ i) fun i _ ↦ h i

Premises used: Finset.prod_le_prod
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
M : Type u_7
α : Type u_8
inst : CommMonoidWithZero M
inst_1 : PartialOrder M
inst_2 : ZeroLEOneClass M
inst_3 : PosMulMono M
rw : LE.le.{u_7} (α := M) (∏ᶠ (x : α), 0) (∏ᶠ (x : α), 1)
⊢ LE.le.{u_7} (α := M) (∏ᶠ (x : α), 0) 1

Tactic:
rw [← finprod_one (α := α)]

Premises used: finprod_one
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
M : Type u_7
α : Type u_8
inst : CommMonoidWithZero M
inst_1 : PartialOrder M
inst_2 : ZeroLEOneClass M
inst_3 : PosMulMono M
pos :
  ∀ (H : HasFiniteMulSupport.{u_8, u_7} (M := M) fun (x : α) ↦ 0), LE.le.{u_7} (α := M) (∏ᶠ (x : α), 0) (∏ᶠ (x : α), 1)
neg :
  ∀ (H : ¬HasFiniteMulSupport.{u_8, u_7} (M := M) fun (x : α) ↦ 0), LE.le.{u_7} (α := M) (∏ᶠ (x : α), 0) (∏ᶠ (x : α), 1)
⊢ LE.le.{u_7} (α := M) (∏ᶠ (x : α), 0) (∏ᶠ (x : α), 1)

Tactic:
by_cases H : (fun _ : α ↦ (0 : M)).HasFiniteMulSupport

Premises used: Function.HasFiniteMulSupport, OfNat.ofNat
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
M : Type u_7
α : Type u_8
inst : CommMonoidWithZero M
inst_1 : PartialOrder M
inst_2 : ZeroLEOneClass M
inst_3 : PosMulMono M
H : HasFiniteMulSupport.{u_8, u_7} (M := M) fun (x : α) ↦ 0
⊢ HasFiniteMulSupport.{u_8, u_7} (M := M) fun (x : α) ↦ 1

Tactic:
fun_prop
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
M : Type u_7
α : Type u_8
inst : CommMonoidWithZero M
inst_1 : PartialOrder M
inst_2 : ZeroLEOneClass M
inst_3 : PosMulMono M
H : HasFiniteMulSupport.{u_8, u_7} (M := M) fun (x : α) ↦ 0
⊢ LE.le.{u_7} (α := M) (∏ᶠ (x : α), 0) (∏ᶠ (x : α), 1)

Tactic:
exact finprod_le_finprod H (fun _ ↦ le_rfl) (by fun_prop) fun _ ↦ zero_le_one

Premises used: le_rfl, finprod_le_finprod, zero_le_one
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
M : Type u_7
α : Type u_8
inst : CommMonoidWithZero M
inst_1 : PartialOrder M
inst_2 : ZeroLEOneClass M
inst_3 : PosMulMono M
H : ¬HasFiniteMulSupport.{u_8, u_7} (M := M) fun (x : α) ↦ 0
neg : LE.le.{u_7} (α := M) 1 (∏ᶠ (x : α), 1)
⊢ LE.le.{u_7} (α := M) (∏ᶠ (x : α), 0) (∏ᶠ (x : α), 1)

Tactic:
rw [finprod_of_not_hasFiniteMulSupport H]

Premises used: finprod_of_not_hasFiniteMulSupport
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
M : Type u_7
α : Type u_8
inst : CommMonoidWithZero M
inst_1 : PartialOrder M
inst_2 : ZeroLEOneClass M
inst_3 : PosMulMono M
H : ¬HasFiniteMulSupport.{u_8, u_7} (M := M) fun (x : α) ↦ 0
⊢ LE.le.{u_7} (α := M) 1 (∏ᶠ (x : α), 1)

Tactic:
finprod_one.symm.le

Premises used: Eq.le, Eq.symm, finprod_one
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
M : Type u_7
α : Type u_8
inst : CommMonoidWithZero M
inst_1 : PartialOrder M
inst_2 : ZeroLEOneClass M
inst_3 : PosMulMono M
H : ¬HasFiniteMulSupport.{u_8, u_7} (M := M) fun (x : α) ↦ 0
⊢ LE.le.{u_7} (α := M) 1 (∏ᶠ (x : α), 1)

Tactic:
exact finprod_one.symm.le

Premises used: Eq.le, Eq.symm, finprod_one
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f g : α → M
hf : HasFiniteMulSupport f
hg : HasFiniteMulSupport g
rw :
  Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α), f i * g i)
    (∏ x ∈ Finite.toFinset (s := mulSupport f) hf ∪ Finite.toFinset (s := mulSupport g) hg, f x * g x)
⊢ ∏ᶠ (i : α), f i * g i = HMul.hMul (α := M) (∏ᶠ (i : α), f i) (∏ᶠ (i : α), g i)

Tactic:
rw [finprod_eq_prod_of_mulSupport_toFinset_subset f hf Finset.subset_union_left,
      finprod_eq_prod_of_mulSupport_toFinset_subset g hg Finset.subset_union_right, ←
      Finset.prod_mul_distrib]

Premises used: Finset.prod_mul_distrib, finprod_eq_prod_of_mulSupport_toFinset_subset, Finset.subset_union_left, Finset.subset_union_right
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f g : α → M
hf : HasFiniteMulSupport f
hg : HasFiniteMulSupport g
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α), f i * g i)
    (∏ x ∈ Finite.toFinset (s := mulSupport f) hf ∪ Finite.toFinset (s := mulSupport g) hg, f x * g x)

Tactic:
finprod_eq_prod_of_mulSupport_subset _ ?_

Premises used: finprod_eq_prod_of_mulSupport_subset
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f g : α → M
hf : HasFiniteMulSupport f
hg : HasFiniteMulSupport g
refine :
  (mulSupport.{u_1, u_5} (M := M) fun (i : α) ↦ f i * g i) ⊆
    (↑(Finite.toFinset (s := mulSupport f) hf ∪ Finite.toFinset (s := mulSupport g) hg) : Set α)
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α), f i * g i)
    (∏ x ∈ Finite.toFinset (s := mulSupport f) hf ∪ Finite.toFinset (s := mulSupport g) hg, f x * g x)

Tactic:
refine finprod_eq_prod_of_mulSupport_subset _ ?_

Premises used: finprod_eq_prod_of_mulSupport_subset
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f g : α → M
hf : HasFiniteMulSupport f
hg : HasFiniteMulSupport g
simp : ∀ (x : α), f x * g x ≠ 1 → f x ≠ 1 ∨ g x ≠ 1
⊢ (mulSupport.{u_1, u_5} (M := M) fun (i : α) ↦ f i * g i) ⊆
    (↑(Finite.toFinset (s := mulSupport f) hf ∪ Finite.toFinset (s := mulSupport g) hg) : Set α)

Tactic:
simp only [Finset.coe_union, Finite.coe_toFinset, mulSupport_subset_iff,
      mem_union, mem_mulSupport]

Premises used: Set.mem_union, Function.mem_mulSupport, Function.mulSupport_subset_iff, Set.Finite.coe_toFinset, Finset.coe_union