mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_1
N : Type u_5
inst✝² : CommMonoid N
inst✝¹ : Preorder N
f : ι → N
s t : Finset ι
inst✝ : MulLeftMono N
h : s ⊆ t
hf : ∀ i ∈ t, i ∉ s → 1 ≤ f i
⊢ ∏ i ∈ t, f i = ∏ i ∈ t, f i

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
f : ι → R
s : Finset ι
hf : ∀ i ∈ s, 0 ≤ f i
i : ι
hi : i ∈ s
⊢ f i * f i ≤ f i * ∑ i ∈ s, f i

Tactic:
]

Goal state after:
ι : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
f : ι → R
s : Finset ι
hf : ∀ i ∈ s, 0 ≤ f i
i : ι
hi : i ∈ s
⊢ f i * f i ≤ f i * ∑ i ∈ s, f i
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α ↪ β
g : β →₀ M
hg : ↑g.support ⊆ Set.range ⇑f
a : α
⊢ g (f a) = g (f a)

Tactic:
]

Goal state after:
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α ↪ β
g : β →₀ M
b : β
hb : b ∉ Set.range ⇑f
hg : g b = 0
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α → β
a : α
m : M
hif : Set.InjOn f (f ⁻¹' ↑(single (f a) m).support)
hm : m ≠ 0
⊢ f ⁻¹' {f a} ⊆ {a} ∧ m = m

Tactic:
]

Goal state after:
case inr
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α → β
a : α
m : M
hif : Set.InjOn f (f ⁻¹' ↑(single (f a) m).support)
hm : m ≠ 0
⊢ f ⁻¹' {f a} ⊆ {a} ∧ m = m
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α → β
a : α
m : M
hif : Set.InjOn f (f ⁻¹' {f a})
hm : m ≠ 0
⊢ f ⁻¹' {f a} ⊆ {a} ∧ m = m

Tactic:
]

Goal state after:
case inr
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α → β
a : α
m : M
hif : Set.InjOn f (f ⁻¹' {f a})
hm : m ≠ 0
⊢ f ⁻¹' {f a} ⊆ {a} ∧ m = m
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
hf : Injective f
l : α →₀ M
a✝ : α
⊢ l a✝ = l a✝

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset

Goal state before:
pp: case refine_1
ι : Type u_1
R : Type u_2
inst✝² : CommSemiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
s : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ j ∈ s, j ≠ i → g j ≤ f j
hhf : ∀ j ∈ s, j ≠ i → h j ≤ f j
hg : ∀ i ∈ s, 0 ≤ g i
hh : ∀ i ∈ s, 0 ≤ h i
⊢ g i * ∏ i ∈ s \ {i}, g i + h i * ∏ i ∈ s \ {i}, h i ≤ g i * ∏ i ∈ s \ {i}, f i + h i * ∏ i ∈ s \ {i}, f i

Tactic:
]

Goal state after:
case refine_1
ι : Type u_1
R : Type u_2
inst✝² : CommSemiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
s : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ j ∈ s, j ≠ i → g j ≤ f j
hhf : ∀ j ∈ s, j ≠ i → h j ≤ f j
hg : ∀ i ∈ s, 0 ≤ g i
hh : ∀ i ∈ s, 0 ≤ h i
⊢ g i * ∏ i ∈ s \ {i}, g i + h i * ∏ i ∈ s \ {i}, h i ≤ g i * ∏ i ∈ s \ {i}, f i + h i * ∏ i ∈ s \ {i}, f i
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_1
N : Type u_5
inst✝² : CommMonoid N
inst✝¹ : PartialOrder N
f : ι → N
s✝ : Finset ι
inst✝ : MulLeftMono N
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, 1 ≤ f i) → (∏ i ∈ s, f i = 1 ↔ ∀ i ∈ s, f i = 1)
H : ∀ i ∈ insert a s, 1 ≤ f i
this : ∀ i ∈ s, 1 ≤ f i
⊢ (f a = 1 ∧ ∀ i ∈ s, f i = 1) ↔ f a = 1 ∧ ∀ x ∈ s, f x = 1

Tactic:
]

Goal state after:
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝¹ : Zero M
inst✝ : DecidableEq α
f : α →₀ M
a a✝ : α
⊢ (if a = a✝ then f a✝ else 0) = if a = a✝ then f a else 0

Tactic:
]

Goal state after:
α : Type u_1
M : Type u_5
inst✝¹ : Zero M
inst✝ : DecidableEq α
f : α →₀ M
a a✝ : α
⊢ (if a = a✝ then f a✝ else 0) = if a = a✝ then f a else 0
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝¹ : Zero M
p : α → Prop
inst✝ : DecidablePred p
⊢ ∅ = ∅

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_1
N : Type u_5
inst✝² : CommMonoid N
inst✝¹ : PartialOrder N
f : ι → N
s : Finset ι
inst✝ : MulLeftMono N
hf : ∀ x ∈ s, 1 ≤ f x
⊢ 1 < ∏ x ∈ s, f x ↔ ∃ x ∈ s, 1 < f x

Tactic:
have hsum : 1 ≤ ∏ x ∈ s, f x := one_le_prod' hf

Goal state after:
ι : Type u_1
N : Type u_5
inst✝² : CommMonoid N
inst✝¹ : PartialOrder N
f : ι → N
s : Finset ι
inst✝ : MulLeftMono N
hf : ∀ x ∈ s, 1 ≤ f x
hsum : 1 ≤ ∏ x ∈ s, f x
⊢ 1 < ∏ x ∈ s, f x ↔ ∃ x ∈ s, 1 < f x
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_5
N : Type u_6
inst✝² : Zero M
p : α → Prop
inst✝¹ : DecidablePred p
f : α →₀ M
inst✝ : CommMonoid N
g : α → M → N
x : α
hx : x ∈ f.support ∧ p x
⊢ g x ((filter p f) x) = g x (f x)

Tactic:
]

Goal state after:
α : Type u_1
M : Type u_5
N : Type u_6
inst✝² : Zero M
p : α → Prop
inst✝¹ : DecidablePred p
f : α →₀ M
inst✝ : CommMonoid N
g : α → M → N
x : α
hx : x ∈ f.support ∧ p x
⊢ g x ((filter p f) x) = g x (f x)
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_5
N : Type u_6
inst✝² : Zero M
p : α → Prop
inst✝¹ : DecidablePred p
f : α →₀ M
inst✝ : CommMonoid N
g : α → M → N
x : α
hx : x ∈ f.support ∧ p x
⊢ g x (f x) = g x (f x)

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_1
N : Type u_5
inst✝² : CommMonoid N
inst✝¹ : PartialOrder N
f : ι → N
s : Finset ι
inst✝ : MulLeftMono N
hf : ∀ x ∈ s, 1 ≤ f x
hsum : 1 ≤ ∏ x ∈ s, f x
⊢ (∃ x, ¬(x ∈ s → f x = 1)) ↔ ∃ x ∈ s, 1 < f x

Tactic:
]

Goal state after:
ι : Type u_1
N : Type u_5
inst✝² : CommMonoid N
inst✝¹ : PartialOrder N
f : ι → N
s : Finset ι
inst✝ : MulLeftMono N
hf : ∀ x ∈ s, 1 ≤ f x
hsum : 1 ≤ ∏ x ∈ s, f x
⊢ (∃ x, ¬(x ∈ s → f x = 1)) ↔ ∃ x ∈ s, 1 < f x
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
f : α →₀ M
y : M
⊢ (∃ a ∈ f.support, f a = y) ↔ y ≠ 0 ∧ y ∈ Set.range ⇑f

Tactic:
]

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : Zero M
f : α →₀ M
y : M
⊢ (∃ a ∈ f.support, f a = y) ↔ y ≠ 0 ∧ y ∈ Set.range ⇑f
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
p : α → Prop
D : DecidablePred p
f : α →₀ M
⊢ (subtypeDomain p f).support = Finset.subtype p f.support

pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
p : α → Prop
D : DecidablePred p
f : α →₀ M
⊢ DecidablePred p

Tactic:
]

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : Zero M
p : α → Prop
D : DecidablePred p
f : α →₀ M
⊢ (subtypeDomain p f).support = Finset.subtype p f.support

α : Type u_1
M : Type u_5
inst✝ : Zero M
p : α → Prop
D : DecidablePred p
f : α →₀ M
⊢ DecidablePred p
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_1
N : Type u_5
inst✝² : CommMonoid N
inst✝¹ : Preorder N
f : ι → N
s : Finset ι
inst✝ : MulLeftMono N
i j : ι
hf : ∀ i ∈ s, 1 ≤ f i
hi : i ∈ s
hj : j ∈ s
hne : i ≠ j
⊢ f i * f j = f i * f j

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_1
N : Type u_5
inst✝³ : CommMonoid N
inst✝² : Preorder N
s : Finset ι
ι' : Type u_9
inst✝¹ : DecidableEq ι'
inst✝ : MulLeftMono N
g : ι → ι'
f : ι' → N
hf : ∀ u ∈ image g s, 1 ≤ f u
⊢ ∏ u ∈ image g s, f u ≤ ∏ b ∈ image g s, f b ^ #({a ∈ s | g a = b})

Tactic:
]

Goal state after:
ι : Type u_1
N : Type u_5
inst✝³ : CommMonoid N
inst✝² : Preorder N
s : Finset ι
ι' : Type u_9
inst✝¹ : DecidableEq ι'
inst✝ : MulLeftMono N
g : ι → ι'
f : ι' → N
hf : ∀ u ∈ image g s, 1 ≤ f u
⊢ ∏ u ∈ image g s, f u ≤ ∏ b ∈ image g s, f b ^ #({a ∈ s | g a = b})
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝¹ : AddCommMonoid M
p : α → Prop
inst✝ : DecidablePred p
f : α →₀ M
x : α
hx : x ∈ Finset.filter p f.support
⊢ single x (f x) = single x (f x)

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_1
N : Type u_5
inst✝³ : CommMonoid N
inst✝² : Preorder N
s : Finset ι
ι' : Type u_9
inst✝¹ : DecidableEq ι'
inst✝ : MulLeftMono N
g : ι → ι'
f : ι' → N
hf : ∀ u ∈ image g s, 1 ≤ f u
a : ι'
hag : a ∈ image g s
i : ι
hi : i ∈ s
hig : g i = a
⊢ {a_1 ∈ s | g a_1 = a}.Nonempty

Tactic:
]

Goal state after:
ι : Type u_1
N : Type u_5
inst✝³ : CommMonoid N
inst✝² : Preorder N
s : Finset ι
ι' : Type u_9
inst✝¹ : DecidableEq ι'
inst✝ : MulLeftMono N
g : ι → ι'
f : ι' → N
hf : ∀ u ∈ image g s, 1 ≤ f u
a : ι'
hag : a ∈ image g s
i : ι
hi : i ∈ s
hig : g i = a
⊢ {a_1 ∈ s | g a_1 = a}.Nonempty
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : CommMonoid α
inst✝² : AddCommMonoid β
inst✝¹ : Preorder β
inst✝ : AddLeftMono β
s : Finset ι
f : ι → α
g : α → β
h_one : g 1 ≤ 0
h_mul : ∀ (a b : α), g (a * b) ≤ g a + g b
⊢ ∑ a ∈ s, g (f a) = ∑ x ∈ s, g (f x)

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ExistsAddOfLE R
s : Finset ι
f : ι → R
⊢ (∀ i ∈ s, f i * f i = 0) ↔ ∀ i ∈ s, f i = 0

Tactic:
]

Goal state after:
ι : Type u_1
R : Type u_2
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ExistsAddOfLE R
s : Finset ι
f : ι → R
⊢ (∀ i ∈ s, f i * f i = 0) ↔ ∀ i ∈ s, f i = 0
Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝² : CommSemiring R
inst✝¹ : PartialOrder R
inst✝ : CanonicallyOrderedAdd R
f g h : ι → R
s : Finset ι
i : ι
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ j ∈ s, j ≠ i → g j ≤ f j
hhf : ∀ j ∈ s, j ≠ i → h j ≤ f j
⊢ g i * ∏ i ∈ s \ {i}, g i + h i * ∏ i ∈ s \ {i}, h i ≤ g i * ∏ i ∈ s \ {i}, f i + h i * ∏ i ∈ s \ {i}, f i

Tactic:
]

Goal state after:
ι : Type u_1
R : Type u_2
inst✝² : CommSemiring R
inst✝¹ : PartialOrder R
inst✝ : CanonicallyOrderedAdd R
f g h : ι → R
s : Finset ι
i : ι
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ j ∈ s, j ≠ i → g j ≤ f j
hhf : ∀ j ∈ s, j ≠ i → h j ≤ f j
⊢ g i * ∏ i ∈ s \ {i}, g i + h i * ∏ i ∈ s \ {i}, h i ≤ g i * ∏ i ∈ s \ {i}, f i + h i * ∏ i ∈ s \ {i}, f i
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_1
G : Type u_9
inst✝² : AddCommGroup G
inst✝¹ : LinearOrder G
inst✝ : AddLeftMono G
f : ι → G
s : Finset ι
hf : ∀ i ∈ s, 0 ≤ f i
⊢ ∑ i ∈ s, f i = ∑ i ∈ s, f i

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_1
G : Type u_9
inst✝² : AddCommGroup G
inst✝¹ : LinearOrder G
inst✝ : AddLeftMono G
f : ι → G
s : Finset ι
hf : ∀ (i : ι), 0 ≤ f i
⊢ ∑ i ∈ s, f i = ∑ i ∈ s, f i

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝ : DecidableEq β
f : α → β
s : Finset α
t : Finset β
Hf : ∀ a ∈ s, f a ∈ t
n : ℕ
hn : ∀ b ∈ t, n ≤ #({a ∈ s | f a = b})
⊢ #s = #s

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset

Goal state before:
pp: case inl
ι : Type u_1
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ExistsAddOfLE R
s : Finset ι
r f g : ι → R
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
ht : ∀ i ∈ s, r i ^ 2 ≤ f i * g i
h : ∑ i ∈ s, g i = 0
ht' : ∑ i ∈ s, r i = 0
⊢ 0 ^ 2 ≤ (∑ i ∈ s, f i) * 0

Tactic:
]

Goal state after:
case inl
ι : Type u_1
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ExistsAddOfLE R
s : Finset ι
r f g : ι → R
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
ht : ∀ i ∈ s, r i ^ 2 ≤ f i * g i
h : ∑ i ∈ s, g i = 0
ht' : ∑ i ∈ s, r i = 0
⊢ 0 ^ 2 ≤ (∑ i ∈ s, f i) * 0
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
a : α × β
m : M
⊢ (single a m).curry = (single (a.1, a.2) m).curry

Tactic:
]

Goal state after:
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
N : Type u_6
inst✝¹ : Zero M
inst✝ : AddCommMonoid N
f : α × β →₀ M
g : α → β → M → N
⊢ (f.sum fun p c ↦ g p.1 p.2 c) = f.sum fun p c ↦ g p.1 p.2 c

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : DecidableEq α
s : Finset ι
f : ι → Finset α
hs : (↑s).PairwiseDisjoint f
hf : ∀ i ∈ s, (f i).Nonempty
⊢ ∑ x ∈ s, 1 ≤ ∑ u ∈ s, #(f u)

Tactic:
]

Goal state after:
ι : Type u_1
α : Type u_2
inst✝ : DecidableEq α
s : Finset ι
f : ι → Finset α
hs : (↑s).PairwiseDisjoint f
hf : ∀ i ∈ s, (f i).Nonempty
⊢ ∑ x ∈ s, 1 ≤ ∑ u ∈ s, #(f u)
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : DecidableEq α
s : Finset ι
f : ι → Finset α
hs : (↑s).PairwiseDisjoint f
⊢ #({a ∈ s | ¬f a = ∅}) + #({i ∈ s | f i = ∅}) ≤ #(s.biUnion f) + #({i ∈ s | f i = ∅})

Tactic:
]

Goal state after:
ι : Type u_1
α : Type u_2
inst✝ : DecidableEq α
s : Finset ι
f : ι → Finset α
hs : (↑s).PairwiseDisjoint f
⊢ #({a ∈ s | ¬f a = ∅}) + #({i ∈ s | f i = ∅}) ≤ #(s.biUnion f) + #({i ∈ s | f i = ∅})
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : DecidableEq α
s : Finset ι
f : ι → Finset α
hs : (↑s).PairwiseDisjoint f
⊢ #(s.biUnion f) + #({i ∈ s | f i = ∅}) ≤ #(s.biUnion f) + #({i ∈ s | f i = ∅})

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : DecidableEq α
s : Finset ι
f : ι → Finset α
hf : Injective f
hs : (↑s).PairwiseDisjoint f
⊢ #(s.biUnion f) + 1 ≤ #(s.biUnion f) + 1

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : Preorder M
inst✝ : CanonicallyOrderedMul M
f : ι → M
s t : Finset ι
h : ∀ x ∈ s, f x ≠ 1 → x ∈ t
this : IsOrderedMonoid M
⊢ ∏ x ∈ s, f x = ∏ x ∈ s, f x

pp: ι : Type u_1
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : Preorder M
inst✝ : CanonicallyOrderedMul M
f : ι → M
s t : Finset ι
h : ∀ x ∈ s, f x ≠ 1 → x ∈ t
this : IsOrderedMonoid M
⊢ Disjoint ({x ∈ s | f x = 1}) ({x ∈ s | f x ≠ 1})

Tactic:
]

Goal state after:
ι : Type u_1
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : Preorder M
inst✝ : CanonicallyOrderedMul M
f : ι → M
s t : Finset ι
h : ∀ x ∈ s, f x ≠ 1 → x ∈ t
this : IsOrderedMonoid M
⊢ Disjoint ({x ∈ s | f x = 1}) ({x ∈ s | f x ≠ 1})
Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ExistsAddOfLE R
s : Finset ι
r f g : ι → R
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
ht : ∀ i ∈ s, r i ^ 2 ≤ f i * g i
h : 0 < ∑ i ∈ s, g i
i : ι
hi : i ∈ s
⊢ f i * g i * ((∑ j ∈ s, g j) * ∑ j ∈ s, r j) ^ 2 ≤ f i * g i * ((∑ j ∈ s, g j) * ∑ j ∈ s, r j) ^ 2

pp: case ha
ι : Type u_1
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ExistsAddOfLE R
s : Finset ι
r f g : ι → R
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
ht : ∀ i ∈ s, r i ^ 2 ≤ f i * g i
h : 0 < ∑ i ∈ s, g i
i : ι
hi : i ∈ s
⊢ 0 ≤ ((∑ j ∈ s, g j) * ∑ j ∈ s, r j) ^ 2

Tactic:
]

Goal state after:
case ha
ι : Type u_1
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ExistsAddOfLE R
s : Finset ι
r f g : ι → R
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
ht : ∀ i ∈ s, r i ^ 2 ≤ f i * g i
h : 0 < ∑ i ∈ s, g i
i : ι
hi : i ∈ s
⊢ 0 ≤ ((∑ j ∈ s, g j) * ∑ j ∈ s, r j) ^ 2
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: case neg
α : Type u_1
M : Type u_12
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
f : Subtype P →₀ M
a : α
h : ¬P a
⊢ f.extendDomain a = 0

pp: case neg.h
α : Type u_1
M : Type u_12
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
f : Subtype P →₀ M
a : α
h : ¬P a
⊢ a ∉ Set.range ⇑(Embedding.subtype P)

Tactic:
]

Goal state after:
case neg
α : Type u_1
M : Type u_12
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
f : Subtype P →₀ M
a : α
h : ¬P a
⊢ f.extendDomain a = 0

case neg.h
α : Type u_1
M : Type u_12
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
f : Subtype P →₀ M
a : α
h : ¬P a
⊢ a ∉ Set.range ⇑(Embedding.subtype P)
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_9
M : Type u_10
inst✝⁴ : DecidableEq ι
inst✝³ : CommMonoid M
inst✝² : PartialOrder M
inst✝¹ : CanonicallyOrderedMul M
inst✝ : MulLeftStrictMono M
S S' : Finset ι
f : ι → M
d d' : ι
hd_mem : d ∈ S
hS' : S' ⊆ S.erase d ∪ {d'}
hlt : f d' < f d
hd_not : d ∉ S'
hd'S : d' ∉ S
⊢ (∏ x ∈ S.erase d, f x) * f d' = (∏ x ∈ S.erase d, f x) * f d'

Tactic:
]

Goal state after:
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
s : Set α
M : Type u_12
inst✝¹ : AddCommMonoid M
inst✝ : DecidablePred fun x ↦ x ∈ s
f : ↑s →₀ M
⊢ f.extendDomain = f.extendDomain

Tactic:
]

Goal state after:
α : Type u_1
s : Set α
M : Type u_12
inst✝¹ : AddCommMonoid M
inst✝ : DecidablePred fun x ↦ x ∈ s
f : ↑s →₀ M
⊢ f.extendDomain = f.extendDomain
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝³ : CommMonoid M
inst✝² : Preorder M
inst✝¹ : IsOrderedCancelMonoid M
f : ι → M
s t : Finset ι
inst✝ : MulLeftStrictMono M
h : s ⊆ t
i : ι
ht : i ∈ t
hs : i ∉ s
hlt : 1 < f i
hle : ∀ j ∈ t, j ∉ s → 1 ≤ f j
⊢ ∏ j ∈ s, f j < f i * ∏ x ∈ s, f x

Tactic:
]

Goal state after:
ι : Type u_1
M : Type u_4
inst✝³ : CommMonoid M
inst✝² : Preorder M
inst✝¹ : IsOrderedCancelMonoid M
f : ι → M
s t : Finset ι
inst✝ : MulLeftStrictMono M
h : s ⊆ t
i : ι
ht : i ∈ t
hs : i ∉ s
hlt : 1 < f i
hle : ∀ j ∈ t, j ∉ s → 1 ≤ f j
⊢ ∏ j ∈ s, f j < f i * ∏ x ∈ s, f x
Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset

Goal state before:
pp: case h
ι : Type u_1
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ExistsAddOfLE R
s : Finset ι
r f g : ι → R
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
ht✝ : ∀ i ∈ s, r i ^ 2 ≤ f i * g i
h : 0 < ∑ i ∈ s, g i
i : ι
hi : i ∈ s
ht : ((r i * ∑ j ∈ s, g j) * ∑ j ∈ s, r j) ^ 2 ≤ f i * (∑ j ∈ s, g j) ^ 2 * (g i * (∑ j ∈ s, r j) ^ 2)
⊢ 2 * r i * ((∑ j ∈ s, g j) * ∑ j ∈ s, r j) = 2 * ((r i * ∑ j ∈ s, g j) * ∑ j ∈ s, r j)

Tactic:
]

Goal state after:
case h
ι : Type u_1
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ExistsAddOfLE R
s : Finset ι
r f g : ι → R
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
ht✝ : ∀ i ∈ s, r i ^ 2 ≤ f i * g i
h : 0 < ∑ i ∈ s, g i
i : ι
hi : i ∈ s
ht : ((r i * ∑ j ∈ s, g j) * ∑ j ∈ s, r j) ^ 2 ≤ f i * (∑ j ∈ s, g j) ^ 2 * (g i * (∑ j ∈ s, r j) ^ 2)
⊢ 2 * r i * ((∑ j ∈ s, g j) * ∑ j ∈ s, r j) = 2 * ((r i * ∑ j ∈ s, g j) * ∑ j ∈ s, r j)
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: ι : Type u_4
M : Type u_5
αs : ι → Type u_12
inst✝ : Zero M
l : (i : ι) × αs i →₀ M
i : ι
x : αs i
⊢ l ⟨i, x⟩ = l ⟨i, x⟩

Tactic:
]

Goal state after:
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: ι : Type u_4
M : Type u_5
αs : ι → Type u_12
inst✝ : Zero M
l : (i : ι) × αs i →₀ M
i : ι
⊢ (∃ a ∈ l.support, a.fst = i) ↔
    ∃ x, x ∈ { support := l.support.preimage (Sigma.mk i) ⋯, toFun := fun a ↦ l ⟨i, a⟩, mem_support_toFun := ⋯ }.support

Tactic:
]

Goal state after:
ι : Type u_4
M : Type u_5
αs : ι → Type u_12
inst✝ : Zero M
l : (i : ι) × αs i →₀ M
i : ι
⊢ (∃ a ∈ l.support, a.fst = i) ↔
    ∃ x, x ∈ { support := l.support.preimage (Sigma.mk i) ⋯, toFun := fun a ↦ l ⟨i, a⟩, mem_support_toFun := ⋯ }.support
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝³ : CommMonoid M
inst✝² : Preorder M
inst✝¹ : IsOrderedCancelMonoid M
f : ι → M
s : Finset ι
inst✝ : MulLeftStrictMono M
i j : ι
hij : j ≠ i
hi : i ∈ s
hj : j ∈ s
hlt : 1 < f j
hle : ∀ k ∈ s, k ≠ i → 1 ≤ f k
⊢ f i = f i

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝³ : CommMonoid M
inst✝² : Preorder M
inst✝¹ : IsOrderedCancelMonoid M
f : ι → M
s : Finset ι
inst✝ : MulLeftStrictMono M
h : ∀ i ∈ s, 1 < f i
hs : s.Nonempty
⊢ 1 ≤ 1

Tactic:
]

Goal state after:
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
G : Type u_8
H : Type u_9
R : Type u_10
S : Type u_11
αs : ι → Type u_12
inst✝¹ : Zero M
l : (i : ι) × αs i →₀ M
inst✝ : Zero N
g : (i : ι) → (αs i →₀ M) → N
hg : ∀ (i : ι) (x : αs i →₀ M), x = 0 ↔ g i x = 0
i : ι
⊢ g i (l.split i) = 0 ↔ g i (l.split i) = 0

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝³ : CommMonoid M
inst✝² : Preorder M
inst✝¹ : IsOrderedCancelMonoid M
f : ι → M
s : Finset ι
inst✝ : MulLeftStrictMono M
h : ∀ i ∈ s, f i < 1
hs : s.Nonempty
⊢ 1 ≤ 1

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset

Goal state before:
pp: case h
ι : Type u_1
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ExistsAddOfLE R
s : Finset ι
r f g : ι → R
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
ht✝ : ∀ i ∈ s, r i ^ 2 ≤ f i * g i
h : 0 < ∑ i ∈ s, g i
i : ι
hi : i ∈ s
ht : ((r i * ∑ j ∈ s, g j) * ∑ j ∈ s, r j) ^ 2 ≤ f i * (∑ j ∈ s, g j) ^ 2 * (g i * (∑ j ∈ s, r j) ^ 2)
⊢ 2 * (r i * ((∑ j ∈ s, g j) * ∑ j ∈ s, r j)) = 2 * ((r i * ∑ j ∈ s, g j) * ∑ j ∈ s, r j)

Tactic:
]

Goal state after:
case h
ι : Type u_1
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ExistsAddOfLE R
s : Finset ι
r f g : ι → R
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
ht✝ : ∀ i ∈ s, r i ^ 2 ≤ f i * g i
h : 0 < ∑ i ∈ s, g i
i : ι
hi : i ∈ s
ht : ((r i * ∑ j ∈ s, g j) * ∑ j ∈ s, r j) ^ 2 ≤ f i * (∑ j ∈ s, g j) ^ 2 * (g i * (∑ j ∈ s, r j) ^ 2)
⊢ 2 * (r i * ((∑ j ∈ s, g j) * ∑ j ∈ s, r j)) = 2 * ((r i * ∑ j ∈ s, g j) * ∑ j ∈ s, r j)
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_9
M : Type u_10
inst✝² : CommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedCancelMonoid M
s✝ : Finset ι
f g : ι → M
a : ι
s : Finset ι
ha : a ∉ s
ih : ∏ i ∈ s, f i = ∏ i ∈ s, g i ↔ ∀ i ∈ s, f i = g i
H : ∀ i ∈ insert a s, f i ≤ g i
⊢ f a * ∏ x ∈ s, f x = g a * ∏ x ∈ s, g x ↔ f a = g a ∧ ∏ i ∈ s, f i = ∏ i ∈ s, g i

Tactic:
]

Goal state after:
ι : Type u_9
M : Type u_10
inst✝² : CommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedCancelMonoid M
s✝ : Finset ι
f g : ι → M
a : ι
s : Finset ι
ha : a ∉ s
ih : ∏ i ∈ s, f i = ∏ i ∈ s, g i ↔ ∀ i ∈ s, f i = g i
H : ∀ i ∈ insert a s, f i ≤ g i
⊢ f a * ∏ x ∈ s, f x = g a * ∏ x ∈ s, g x ↔ f a = g a ∧ ∏ i ∈ s, f i = ∏ i ∈ s, g i
Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset

Goal state before:
pp: case h
ι : Type u_1
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ExistsAddOfLE R
s : Finset ι
r f g : ι → R
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
ht✝ : ∀ i ∈ s, r i ^ 2 ≤ f i * g i
h : 0 < ∑ i ∈ s, g i
i : ι
hi : i ∈ s
ht : ((r i * ∑ j ∈ s, g j) * ∑ j ∈ s, r j) ^ 2 ≤ f i * (∑ j ∈ s, g j) ^ 2 * (g i * (∑ j ∈ s, r j) ^ 2)
⊢ 2 * (r i * ((∑ j ∈ s, g j) * ∑ j ∈ s, r j)) = 2 * (r i * ((∑ j ∈ s, g j) * ∑ j ∈ s, r j))

Tactic:
]

Goal state after:
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: case e'_1.e'_4
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α ↪ β
x : β →₀ M
x✝ : α →₀ M
a✝ : β
⊢ (mapDomain (⇑f) x✝) a✝ = (mapDomain (⇑f) x✝) a✝

Tactic:
]

Goal state after: