awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
M : Type u_2
α : Sort u_4
inst : CommMonoid M
f : α → M
a : α
ha : ∀ (x : α), x ≠ a → f x = 1
x : PLift α
⊢ x ∉ (↑{{ down := a : PLift α }} : Set (PLift α)) → x ∉ mulSupport (f ∘ PLift.down)

Tactic:
simpa [PLift.eq_up_iff_down_eq] using ha x.down

Premises used: PLift.down, PLift.eq_up_iff_down_eq
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
M : Type u_2
α : Sort u_4
inst : CommMonoid M
f : α → M
a : α
ha : ∀ (x : α), x ≠ a → f x = 1
⊢ mulSupport (f ∘ PLift.down) ⊆ (↑{{ down := a : PLift α }} : Set (PLift α))

Tactic:
have : mulSupport (f ∘ PLift.down) ⊆ ({PLift.up a} : Finset (PLift α)) := by
    intro x
    contrapose
    simpa [PLift.eq_up_iff_down_eq] using ha x.down
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
M : Type u_2
α : Sort u_4
inst : CommMonoid M
f : α → M
a : α
ha : ∀ (x : α), x ≠ a → f x = 1
this : mulSupport (f ∘ PLift.down) ⊆ (↑{{ down := a : PLift α }} : Set (PLift α))
rw : ∏ i ∈ {{ down := a : PLift α }}, f i.down = f a
rw₁ rw₂ : f { down := a : PLift α }.down = f a
⊢ ∏ᶠ (x : α), f x = f a

Tactic:
rw [finprod_eq_prod_plift_of_mulSupport_subset this, Finset.prod_singleton]

Premises used: Finset.prod_singleton, finprod_eq_prod_plift_of_mulSupport_subset
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
M : Type u_2
α : Sort u_4
inst : CommMonoid M
inst_1 : Unique α
f : α → M
⊢ ∏ᶠ (i : α), f i = f default

Tactic:
finprod_eq_single f default fun _x hx => (hx <| Unique.eq_default _).elim

Premises used: Inhabited.default, False.elim, Unique.eq_default, finprod_eq_single
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
M : Type u_2
inst : CommMonoid M
f : True → M
⊢ ∏ᶠ (i : True), f i = f trivial

Tactic:
@finprod_unique M True _ ⟨⟨trivial⟩, fun _ => rfl⟩ f

Premises used: finprod_unique
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
M : Type u_2
inst : CommMonoid M
p : Prop
inst_1 : Decidable p
f : p → M
pos : ∀ (h : p), ∏ᶠ (i : p), f i = f h
neg : ∀ (h : ¬p), Eq.{u_2 + 1} (α := M) (∏ᶠ (i : p), f i) 1
⊢ Eq.{u_2 + 1} (α := M) (∏ᶠ (i : p), f i) (if h : p then f h else 1)

Tactic:
split_ifs with h
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
M : Type u_2
inst : CommMonoid M
p : Prop
inst_1 : Decidable p
f : p → M
h : p
pos : ∀ (this : Unique p), ∏ᶠ (i : p), f i = f h
⊢ ∏ᶠ (i : p), f i = f h

Tactic:
haveI : Unique p := ⟨⟨h⟩, fun _ => rfl⟩
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
M : Type u_2
inst : CommMonoid M
p : Prop
inst_1 : Decidable p
f : p → M
h : p
this : Unique p
⊢ ∏ᶠ (i : p), f i = f h

Tactic:
finprod_unique f

Premises used: finprod_unique
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
M : Type u_2
inst : CommMonoid M
p : Prop
inst_1 : Decidable p
f : p → M
h : p
this : Unique p
⊢ ∏ᶠ (i : p), f i = f h

Tactic:
exact finprod_unique f

Premises used: finprod_unique
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
M : Type u_2
inst : CommMonoid M
p : Prop
inst_1 : Decidable p
f : p → M
h : ¬p
⊢ IsEmpty p

Tactic:
haveI : IsEmpty p := ⟨h⟩
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
M : Type u_2
inst : CommMonoid M
p : Prop
inst_1 : Decidable p
f : p → M
h : ¬p
this : IsEmpty p
⊢ Eq.{u_2 + 1} (α := M) (∏ᶠ (i : p), f i) 1

Tactic:
finprod_of_isEmpty f

Premises used: finprod_of_isEmpty
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
M : Type u_2
inst : CommMonoid M
p : Prop
inst_1 : Decidable p
f : p → M
h : ¬p
this : IsEmpty p
⊢ Eq.{u_2 + 1} (α := M) (∏ᶠ (i : p), f i) 1

Tactic:
exact finprod_of_isEmpty f

Premises used: finprod_of_isEmpty
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
M : Type u_2
inst : CommMonoid M
p : Prop
inst_1 : Decidable p
x : M
⊢ ∏ᶠ (_ : p), x = if p then x else 1

Tactic:
finprod_eq_dif fun _ => x

Premises used: finprod_eq_dif, ite
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
M : Type u_2
α : Sort u_4
inst : CommMonoid M
f g : α → M
h : ∀ (x : α), f x = g x
⊢ finprod f = finprod g

Tactic:
congr_arg _ <| funext h

Premises used: congr_arg, funext
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
M : Type u_2
inst : CommMonoid M
p q : Prop
f : p → M
g : q → M
hpq : p = q
hfg : ∀ (h : q), f ⋯ = g h
subst : ∀ {g : p → M} (hfg : ∀ (h : p), f ⋯ = g h), finprod f = finprod g
⊢ finprod f = finprod g

Tactic:
subst q
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
M : Type u_2
inst : CommMonoid M
p : Prop
f g : p → M
hfg : ∀ (h : p), f ⋯ = g h
⊢ finprod f = finprod g

Tactic:
finprod_congr hfg

Premises used: finprod_congr
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
M : Type u_2
inst : CommMonoid M
p : Prop
f g : p → M
hfg : ∀ (h : p), f ⋯ = g h
⊢ finprod f = finprod g

Tactic:
exact finprod_congr hfg

Premises used: finprod_congr
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
M : Type u_2
α : Sort u_4
inst : CommMonoid M
f : α → M
p : M → Prop
hp₀ : p 1
hp₁ : ∀ (x y : M), p x → p y → p (x * y)
hp₂ : ∀ (i : α), p (f i)
rw :
  p
    (if h : HasFiniteMulSupport.{u_4, u_2} (α := PLift α) (M := M) ((fun (i : α) ↦ f i) ∘ PLift.down) then
      ∏ i ∈ Finite.toFinset (s := mulSupport.{u_4, u_2} (M := M) ((fun (i : α) ↦ f i) ∘ PLift.down)) h, f i.down
    else 1)
⊢ p (∏ᶠ (i : α), f i)

Tactic:
rw [finprod]

Premises used: finprod
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
M : Type u_2
α : Sort u_4
inst : CommMonoid M
f : α → M
p : M → Prop
hp₀ : p 1
hp₁ : ∀ (x y : M), p x → p y → p (x * y)
hp₂ : ∀ (i : α), p (f i)
pos :
  ∀ (h : HasFiniteMulSupport.{u_4, u_2} (α := PLift α) (M := M) ((fun (i : α) ↦ f i) ∘ PLift.down)),
    p (∏ i ∈ Finite.toFinset (s := mulSupport.{u_4, u_2} (M := M) ((fun (i : α) ↦ f i) ∘ PLift.down)) h, f i.down)
neg : ¬HasFiniteMulSupport.{u_4, u_2} (α := PLift α) (M := M) ((fun (i : α) ↦ f i) ∘ PLift.down) → p 1
⊢ p
    (if h : HasFiniteMulSupport.{u_4, u_2} (α := PLift α) (M := M) ((fun (i : α) ↦ f i) ∘ PLift.down) then
      ∏ i ∈ Finite.toFinset (s := mulSupport.{u_4, u_2} (M := M) ((fun (i : α) ↦ f i) ∘ PLift.down)) h, f i.down
    else 1)

Tactic:
split_ifs
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
M : Type u_2
α : Sort u_4
inst : CommMonoid M
f : α → M
p : M → Prop
hp₀ : p 1
hp₁ : ∀ (x y : M), p x → p y → p (x * y)
hp₂ : ∀ (i : α), p (f i)
h : HasFiniteMulSupport.{u_4, u_2} (α := PLift α) (M := M) ((fun (i : α) ↦ f i) ∘ PLift.down)
⊢ p (∏ i ∈ Finite.toFinset (s := mulSupport.{u_4, u_2} (M := M) ((fun (i : α) ↦ f i) ∘ PLift.down)) h, f i.down)

Tactic:
Finset.prod_induction _ _ hp₁ hp₀ fun i _ => hp₂ _

Premises used: PLift.down, Finset.prod_induction
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
M : Type u_2
α : Sort u_4
inst : CommMonoid M
f : α → M
p : M → Prop
hp₀ : p 1
hp₁ : ∀ (x y : M), p x → p y → p (x * y)
hp₂ : ∀ (i : α), p (f i)
h : ¬HasFiniteMulSupport.{u_4, u_2} (α := PLift α) (M := M) ((fun (i : α) ↦ f i) ∘ PLift.down)
⊢ p 1

Tactic:
hp₀
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
M : Type u_2
α : Sort u_4
inst : CommMonoid M
f : α → M
p : M → Prop
hp₀ : p 1
hp₁ : ∀ (x y : M), p x → p y → p (x * y)
hp₂ : ∀ (i : α), p (f i)
h : HasFiniteMulSupport.{u_4, u_2} (α := PLift α) (M := M) ((fun (i : α) ↦ f i) ∘ PLift.down)
⊢ p (∏ i ∈ Finite.toFinset (s := mulSupport.{u_4, u_2} (M := M) ((fun (i : α) ↦ f i) ∘ PLift.down)) h, f i.down)

Tactic:
exacts [Finset.prod_induction _ _ hp₁ hp₀ fun i _ => hp₂ _, hp₀]

Premises used: Finset.prod_induction
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Sort u_4
R : Type u_7
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
f : α → R
hf : ∀ (x : α), 0 ≤ f x
⊢ LE.le.{u_7} (α := R) 0 (∏ᶠ (x : α), f x)

Tactic:
finprod_induction (fun x => 0 ≤ x) zero_le_one (fun _ _ => mul_nonneg) hf

Premises used: mul_nonneg, finprod_induction, LE.le, zero_le_one, OfNat.ofNat
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Sort u_4
M : Type u_7
inst : CommMonoid M
inst_1 : Preorder M
inst_2 : IsOrderedMonoid M
f : α → M
hf : ∀ (i : α), 1 ≤ f i
⊢ LE.le.{u_7} (α := M) 1 (∏ᶠ (i : α), f i)

Tactic:
finprod_induction _ le_rfl (fun _ _ => one_le_mul) hf

Premises used: le_rfl, finprod_induction, one_le_mul
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Sort u_4
M : Type u_7
inst : CommMonoidWithZero M
inst_1 : Preorder M
inst_2 : ZeroLEOneClass M
inst_3 : PosMulMono M
f : α → M
hf : ∀ (i : α), 1 ≤ f i
⊢ LE.le.{u_7} (α := M) 1 (∏ᶠ (i : α), f i)

Tactic:
finprod_induction _ le_rfl (fun _ _ ↦ one_le_mul_of_one_le_of_one_le) hf

Premises used: le_rfl, finprod_induction, one_le_mul_of_one_le_of_one_le
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
M : Type u_2
N : Type u_3
α : Sort u_4
inst : CommMonoid M
inst_1 : CommMonoid N
f : M →* N
g : α → M
h : HasFiniteMulSupport (g ∘ PLift.down)
rw :
  mulSupport.{u_4, u_3} (M := N) ((fun (x : α) ↦ (f : (a : M) → N) (g x)) ∘ PLift.down) ⊆
    (↑(Finite.toFinset (s := mulSupport (g ∘ PLift.down)) h) : Set (PLift α))
⊢ Eq.{u_3 + 1} (α := N) ((f : (a : M) → N) (∏ᶠ (x : α), g x) : N) (∏ᶠ (x : α), (f : (a : M) → N) (g x) : N)

Tactic:
rw [finprod_eq_prod_plift_of_mulSupport_subset h.coe_toFinset.ge,
    finprod_eq_prod_plift_of_mulSupport_subset, _root_.map_prod]

Premises used: Eq.ge, Set.Finite.coe_toFinset, map_prod, finprod_eq_prod_plift_of_mulSupport_subset
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
M : Type u_2
N : Type u_3
α : Sort u_4
inst : CommMonoid M
inst_1 : CommMonoid N
f : M →* N
g : α → M
h : HasFiniteMulSupport (g ∘ PLift.down)
rw : mulSupport.{u_4, u_3} (M := N) ((fun (x : α) ↦ (f : (a : M) → N) (g x)) ∘ PLift.down) ⊆ mulSupport (g ∘ PLift.down)
⊢ mulSupport.{u_4, u_3} (M := N) ((fun (x : α) ↦ (f : (a : M) → N) (g x)) ∘ PLift.down) ⊆
    (↑(Finite.toFinset (s := mulSupport (g ∘ PLift.down)) h) : Set (PLift α))

Tactic:
rw [h.coe_toFinset]

Premises used: Set.Finite.coe_toFinset
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
M : Type u_2
N : Type u_3
α : Sort u_4
inst : CommMonoid M
inst_1 : CommMonoid N
f : M →* N
g : α → M
h : HasFiniteMulSupport (g ∘ PLift.down)
⊢ mulSupport.{u_4, u_3} (M := N) ((fun (x : α) ↦ (f : (a : M) → N) (g x)) ∘ PLift.down) ⊆ mulSupport (g ∘ PLift.down)

Tactic:
mulSupport_comp_subset f.map_one (g ∘ PLift.down)

Premises used: Function.mulSupport_comp_subset, Function.comp, PLift.down, MonoidHom.map_one
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
M : Type u_2
N : Type u_3
α : Sort u_4
inst : CommMonoid M
inst_1 : CommMonoid N
f : M →* N
g : α → M
h : HasFiniteMulSupport (g ∘ PLift.down)
⊢ mulSupport.{u_4, u_3} (M := N) ((fun (x : α) ↦ (f : (a : M) → N) (g x)) ∘ PLift.down) ⊆ mulSupport (g ∘ PLift.down)

Tactic:
exact mulSupport_comp_subset f.map_one (g ∘ PLift.down)

Premises used: Function.mulSupport_comp_subset, Function.comp, PLift.down, MonoidHom.map_one
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
M : Type u_2
N : Type u_3
inst : CommMonoid M
inst_1 : CommMonoid N
p : Prop
f : M →* N
g : p → M
⊢ Eq.{u_3 + 1} (α := N) ((f : (a : M) → N) (∏ᶠ (x : p), g x) : N) (∏ᶠ (x : p), (f : (a : M) → N) (g x) : N)

Tactic:
f.map_finprod_plift g (Set.toFinite _)

Premises used: Set.toFinite, MonoidHom.map_finprod_plift
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
M : Type u_2
N : Type u_3
α : Sort u_4
inst : CommMonoid M
inst_1 : CommMonoid N
f : M →* N
hf : ∀ (x : M), Eq.{u_3 + 1} (α := N) ((f : (a : M) → N) x : N) (1 : N) → x = 1
g : α → M
pos :
  ∀ (hg : HasFiniteMulSupport (g ∘ PLift.down)),
    Eq.{u_3 + 1} (α := N) ((f : (a : M) → N) (∏ᶠ (i : α), g i) : N) (∏ᶠ (i : α), (f : (a : M) → N) (g i) : N)
neg :
  ∀ (hg : ¬HasFiniteMulSupport (g ∘ PLift.down)),
    Eq.{u_3 + 1} (α := N) ((f : (a : M) → N) (∏ᶠ (i : α), g i) : N) (∏ᶠ (i : α), (f : (a : M) → N) (g i) : N)
⊢ Eq.{u_3 + 1} (α := N) ((f : (a : M) → N) (∏ᶠ (i : α), g i) : N) (∏ᶠ (i : α), (f : (a : M) → N) (g i) : N)

Tactic:
by_cases hg : HasFiniteMulSupport <| g ∘ PLift.down

Premises used: PLift.down, Function.HasFiniteMulSupport
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
M : Type u_2
N : Type u_3
α : Sort u_4
inst : CommMonoid M
inst_1 : CommMonoid N
f : M →* N
hf : ∀ (x : M), Eq.{u_3 + 1} (α := N) ((f : (a : M) → N) x : N) (1 : N) → x = 1
g : α → M
hg : HasFiniteMulSupport (g ∘ PLift.down)
⊢ Eq.{u_3 + 1} (α := N) ((f : (a : M) → N) (∏ᶠ (i : α), g i) : N) (∏ᶠ (i : α), (f : (a : M) → N) (g i) : N)

Tactic:
f.map_finprod_plift g hg

Premises used: MonoidHom.map_finprod_plift
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
M : Type u_2
N : Type u_3
α : Sort u_4
inst : CommMonoid M
inst_1 : CommMonoid N
f : M →* N
hf : ∀ (x : M), Eq.{u_3 + 1} (α := N) ((f : (a : M) → N) x : N) (1 : N) → x = 1
g : α → M
hg : HasFiniteMulSupport (g ∘ PLift.down)
⊢ Eq.{u_3 + 1} (α := N) ((f : (a : M) → N) (∏ᶠ (i : α), g i) : N) (∏ᶠ (i : α), (f : (a : M) → N) (g i) : N)

Tactic:
exact f.map_finprod_plift g hg

Premises used: MonoidHom.map_finprod_plift
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
M : Type u_2
N : Type u_3
α : Sort u_4
inst : CommMonoid M
inst_1 : CommMonoid N
f : M →* N
hf : ∀ (x : M), Eq.{u_3 + 1} (α := N) ((f : (a : M) → N) x : N) (1 : N) → x = 1
g : α → M
hg : ¬HasFiniteMulSupport (g ∘ PLift.down)
neg : ¬HasFiniteMulSupport.{u_4, u_3} (α := PLift α) (M := N) ((fun (i : α) ↦ (f : (a : M) → N) (g i)) ∘ PLift.down)
neg₁ : ¬HasFiniteMulSupport.{u_4, u_2} (α := PLift α) (M := M) ((fun (i : α) ↦ g i) ∘ PLift.down)
⊢ Eq.{u_3 + 1} (α := N) ((f : (a : M) → N) (∏ᶠ (i : α), g i) : N) (∏ᶠ (i : α), (f : (a : M) → N) (g i) : N)

Tactic:
rw [finprod, dif_neg, f.map_one, finprod, dif_neg]

Premises used: dif_neg, finprod, MonoidHom.map_one
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
M : Type u_2
N : Type u_3
α : Sort u_4
inst : CommMonoid M
inst_1 : CommMonoid N
f : M →* N
hf : ∀ (x : M), Eq.{u_3 + 1} (α := N) ((f : (a : M) → N) x : N) (1 : N) → x = 1
g : α → M
hg : ¬HasFiniteMulSupport (g ∘ PLift.down)
⊢ ¬HasFiniteMulSupport.{u_4, u_3} (α := PLift α) (M := N) ((fun (i : α) ↦ (f : (a : M) → N) (g i)) ∘ PLift.down)

Tactic:
Infinite.mono (fun x hx => mt (hf (g x.down)) hx) hg

Premises used: Set.Infinite.mono, mt, PLift.down, Function.HasFiniteMulSupport, Set.Infinite
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
M : Type u_2
N : Type u_3
α : Sort u_4
inst : CommMonoid M
inst_1 : CommMonoid N
f : M →* N
hf : ∀ (x : M), Eq.{u_3 + 1} (α := N) ((f : (a : M) → N) x : N) (1 : N) → x = 1
g : α → M
hg : ¬HasFiniteMulSupport (g ∘ PLift.down)
⊢ ¬HasFiniteMulSupport.{u_4, u_2} (α := PLift α) (M := M) ((fun (i : α) ↦ g i) ∘ PLift.down)

Tactic:
hg
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
M : Type u_2
N : Type u_3
α : Sort u_4
inst : CommMonoid M
inst_1 : CommMonoid N
f : M →* N
hf : ∀ (x : M), Eq.{u_3 + 1} (α := N) ((f : (a : M) → N) x : N) (1 : N) → x = 1
g : α → M
hg : ¬HasFiniteMulSupport (g ∘ PLift.down)
⊢ ¬HasFiniteMulSupport.{u_4, u_3} (α := PLift α) (M := N) ((fun (i : α) ↦ (f : (a : M) → N) (g i)) ∘ PLift.down)

Tactic:
exacts [Infinite.mono (fun x hx => mt (hf (g x.down)) hx) hg, hg]

Premises used: Set.Infinite.mono, mt
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
M : Type u_2
N : Type u_3
α : Sort u_4
inst : CommMonoid M
inst_1 : CommMonoid N
g : M →* N
hg : Injective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑g : (a : M) → N)
f : α → M
⊢ Eq.{u_3 + 1} (α := N) ((g : (a : M) → N) (∏ᶠ (i : α), f i) : N) (∏ᶠ (i : α), (g : (a : M) → N) (f i) : N)

Tactic:
g.map_finprod_of_preimage_one (fun _ => (hg.eq_iff' g.map_one).mp) f

Premises used: MonoidHom.map_finprod_of_preimage_one, Function.Injective.eq_iff', MonoidHom.map_one, Iff.mp
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
M : Type u_2
N : Type u_3
α : Sort u_4
inst : CommMonoid M
inst_1 : CommMonoid N
g : M ≃* N
f : α → M
⊢ Eq.{u_3 + 1} (α := N) ((g : (a : M) → N) (∏ᶠ (i : α), f i) : N) (∏ᶠ (i : α), (g : (a : M) → N) (f i) : N)

Tactic:
g.toMonoidHom.map_finprod_of_injective (EquivLike.injective g) f

Premises used: MulEquiv.toMonoidHom, EquivLike.injective, MonoidHom.map_finprod_of_injective
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
M : Type u_2
N : Type u_3
α : Sort u_4
inst : CommMonoid M
inst_1 : CommMonoid N
F : Type u_7
inst_2 : EquivLike F M N
inst_3 : MulEquivClass F M N
g : F
f : α → M
⊢ Eq.{u_3 + 1} (α := N) ((g : (a : M) → N) (∏ᶠ (i : α), f i) : N) (∏ᶠ (i : α), (g : (a : M) → N) (f i) : N)

Tactic:
MulEquiv.map_finprod (MulEquivClass.toMulEquiv g) f

Premises used: MulEquiv.map_finprod, MulEquivClass.toMulEquiv
-- Module: Mathlib.Algebra.BigOperators.Finprod
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
inr : ∀ (hx : x ≠ 0), HSMul.hSMul.{u_7, u_8, u_8} (α := R) (∑ᶠ (i : ι), f i) x = ∑ᶠ (i : ι), f i • x
⊢ 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)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.BigOperators.Finprod
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
⊢ HSMul.hSMul.{u_7, u_8, u_8} (α := R) (β := M) (∑ᶠ (i : ι), f i) 0 = ∑ᶠ (i : ι), HSMul.hSMul (β := M) (f i) 0

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Finprod
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
hx : x ≠ 0
⊢ HSMul.hSMul.{u_7, u_8, u_8} (α := R) (∑ᶠ (i : ι), f i) x = ∑ᶠ (i : ι), f i • x

Tactic:
((smulAddHom R M).flip x).map_finsum_of_injective (smul_left_injective R hx) _

Premises used: AddMonoidHom.map_finsum_of_injective, smul_left_injective, AddMonoidHom.flip, smulAddHom, DFunLike.coe
-- Module: Mathlib.Algebra.BigOperators.Finprod
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
hx : x ≠ 0
⊢ HSMul.hSMul.{u_7, u_8, u_8} (α := R) (∑ᶠ (i : ι), f i) x = ∑ᶠ (i : ι), f i • x

Tactic:
exact ((smulAddHom R M).flip x).map_finsum_of_injective (smul_left_injective R hx) _

Premises used: AddMonoidHom.map_finsum_of_injective, smul_left_injective, AddMonoidHom.flip, smulAddHom, DFunLike.coe
-- Module: Mathlib.Algebra.BigOperators.Finprod
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)
inr : ∀ (hc : c ≠ 0), HSMul.hSMul (β := M) c (∑ᶠ (i : ι), f i) = ∑ᶠ (i : ι), c • f i
⊢ HSMul.hSMul (β := M) c (∑ᶠ (i : ι), f i) = ∑ᶠ (i : ι), c • f i

Tactic:
rcases eq_or_ne c 0 with (rfl | hc)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.BigOperators.Finprod
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
f : ι → M
⊢ 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:
simp
-- Module: Mathlib.Algebra.BigOperators.Finprod
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
hc : c ≠ 0
⊢ HSMul.hSMul (β := M) c (∑ᶠ (i : ι), f i) = ∑ᶠ (i : ι), c • f i

Tactic:
(smulAddHom R M c).map_finsum_of_injective (smul_right_injective M hc) _

Premises used: AddMonoidHom.map_finsum_of_injective, smul_right_injective, smulAddHom, DFunLike.coe
-- Module: Mathlib.Algebra.BigOperators.Finprod
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
hc : c ≠ 0
⊢ HSMul.hSMul (β := M) c (∑ᶠ (i : ι), f i) = ∑ᶠ (i : ι), c • f i

Tactic:
exact (smulAddHom R M c).map_finsum_of_injective (smul_right_injective M hc) _

Premises used: AddMonoidHom.map_finsum_of_injective, smul_right_injective, smulAddHom, DFunLike.coe
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
G : Type u_1
α : Sort u_4
inst : DivisionCommMonoid G
f : α → G
⊢ Eq.{u_1 + 1} (α := G) (∏ᶠ (x : α), (f x)⁻¹) (∏ᶠ (x : α), f x)⁻¹

Tactic:
((MulEquiv.inv G).map_finprod f).symm

Premises used: MulEquiv.inv, MulEquiv.map_finprod, Eq.symm
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
s : Set α
f : α → M
a : α
⊢ ∏ᶠ (_ : a ∈ s), f a = if a ∈ s then f a else 1

Tactic:
finprod_eq_if (M := M) (p := a ∈ s) (x := f a)

Premises used: finprod_eq_if
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
s : Set α
f : α → M
a : α
⊢ ∏ᶠ (_ : a ∈ s), f a = s.mulIndicator f a

Tactic:
convert! finprod_eq_if (M := M) (p := a ∈ s) (x := f a)

Premises used: finprod_eq_if
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
s : Set α
f : α → M
a : α
⊢ ∏ᶠ (_ : a ∈ s), f a = s.mulIndicator f a

Tactic:
classical convert! finprod_eq_if (M := M) (p := a ∈ s) (x := f a)
-- Module: Mathlib.Algebra.BigOperators.Finprod
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
rw₂ rw₃ : f a = f a
⊢ ∏ᶠ (_ : f a ≠ 1), f a = f a

Tactic:
rw [← mem_mulSupport, finprod_eq_mulIndicator_apply, mulIndicator_mulSupport]

Premises used: Function.mem_mulSupport, Set.mulIndicator_mulSupport, finprod_eq_mulIndicator_apply
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
s : Set α
f : α → M
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (a : α) (_ : a ∈ s), f a) (∏ᶠ (a : α), s.mulIndicator f a)

Tactic:
finprod_congr <| finprod_eq_mulIndicator_apply s f

Premises used: finprod_eq_mulIndicator_apply, finprod_congr
-- Module: Mathlib.Algebra.BigOperators.Finprod
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)
rw₁ rw₂ : Eq.{u_5 + 1} (α := M) (∏ᶠ (a : α), f a) (∏ᶠ (a : α), f a)
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (a : α) (_ : a ∈ mulSupport f), f a) (∏ᶠ (a : α), f a)

Tactic:
rw [finprod_mem_def, mulIndicator_mulSupport]

Premises used: finprod_mem_def, Set.mulIndicator_mulSupport
-- 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 α)
rw : PLift.down ⁻¹' mulSupport f = (⇑(Equiv.symm Equiv.plift) : (a : α) → PLift α) '' mulSupport f
⊢ mulSupport (f ∘ PLift.down) = (⇑(Equiv.symm Equiv.plift) : (a : α) → PLift α) '' mulSupport f

Tactic:
rw [mulSupport_comp_eq_preimage]

Premises used: Function.mulSupport_comp_eq_preimage
-- 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 α)
⊢ PLift.down ⁻¹' mulSupport f = (⇑(Equiv.symm Equiv.plift) : (a : α) → PLift α) '' mulSupport f

Tactic:
(Equiv.plift.symm.image_eq_preimage_symm _).symm

Premises used: Equiv.image_eq_preimage_symm, Equiv.plift, Equiv.symm, Eq.symm
-- 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 α)
⊢ PLift.down ⁻¹' mulSupport f = (⇑(Equiv.symm Equiv.plift) : (a : α) → PLift α) '' mulSupport f

Tactic:
exact (Equiv.plift.symm.image_eq_preimage_symm _).symm

Premises used: Equiv.image_eq_preimage_symm, Equiv.plift, Equiv.symm, Eq.symm
-- 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 α)
⊢ 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