mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: case insert
ι : Type u_2
γ : Type u_3
B : Type u_5
inst✝³ : AddCommMonoid B
A : Type u_16
F : Type u_17
inst✝² : AddZeroClass A
inst✝¹ : AddCommMonoid F
inst✝ : FunLike F γ B
g : ι →₀ A
k : ι → A → F
x : γ
h0 : 0 x = 0
hadd : ∀ (f g : F), (f + g) x = f x + g x
i : ι
s : Finset ι
hi : i ∉ s
ih : (∑ a ∈ s, k a (g a)) x = ∑ a ∈ s, (fun i a ↦ (k i a) x) a (g a)
⊢ (∑ a ∈ insert i s, k a (g a)) x = ∑ a ∈ insert i s, (fun i a ↦ (k i a) x) a (g a)

Tactic:
| insert i s hi ih =>

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

Goal state before:
pp: case mk
ι : Type u_1
α : Type u_2
inst✝² : CommMonoid α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedMonoid α
s : Multiset ι
f g : ι → α
l : List ι
⊢ max (map f (Quot.mk (⇑(List.isSetoid ι)) l)).prod (map g (Quot.mk (⇑(List.isSetoid ι)) l)).prod ≤
    (map (fun i ↦ max (f i) (g i)) (Quot.mk (⇑(List.isSetoid ι)) l)).prod

Tactic:
[

Goal state after:
case mk
ι : Type u_1
α : Type u_2
inst✝² : CommMonoid α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedMonoid α
s : Multiset ι
f g : ι → α
l : List ι
⊢ max (map f (Quot.mk (⇑(List.isSetoid ι)) l)).prod (map g (Quot.mk (⇑(List.isSetoid ι)) l)).prod ≤
    (map (fun i ↦ max (f i) (g i)) (Quot.mk (⇑(List.isSetoid ι)) l)).prod
Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset

Goal state before:
pp: case mk
ι : Type u_1
α : Type u_2
inst✝² : CommMonoid α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedMonoid α
s : Multiset ι
f g : ι → α
l : List ι
⊢ (map (fun i ↦ min (f i) (g i)) (Quot.mk (⇑(List.isSetoid ι)) l)).prod ≤
    min (map f (Quot.mk (⇑(List.isSetoid ι)) l)).prod (map g (Quot.mk (⇑(List.isSetoid ι)) l)).prod

Tactic:
[

Goal state after:
case mk
ι : Type u_1
α : Type u_2
inst✝² : CommMonoid α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedMonoid α
s : Multiset ι
f g : ι → α
l : List ι
⊢ (map (fun i ↦ min (f i) (g i)) (Quot.mk (⇑(List.isSetoid ι)) l)).prod ≤
    min (map f (Quot.mk (⇑(List.isSetoid ι)) l)).prod (map g (Quot.mk (⇑(List.isSetoid ι)) l)).prod
Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset

Goal state before:
pp: case refine_3
ι : Type u_1
R : Type u_2
inst✝⁴ : CommMonoidWithZero R
inst✝³ : PartialOrder R
inst✝² : ZeroLEOneClass R
inst✝¹ : PosMulStrictMono R
inst✝ : Nontrivial R
f g : ι → R
s : Finset ι
hf : ∀ i ∈ s, 0 < f i
hfg : ∀ i ∈ s, f i ≤ g i
i : ι
hi : i ∈ s
hilt : f i < g i
this : MulPosStrictMono R
⊢ 0 ≤ g i

Tactic:
· exact (hf i hi).le.trans hilt.le

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
a : α
m : M
f : α →₀ M
⊢ (a, m) ∈ f.graph ↔ f a = m ∧ m ≠ 0

Tactic:
[

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : Zero M
a : α
m : M
f : α →₀ M
⊢ (a, m) ∈ f.graph ↔ f a = m ∧ m ≠ 0
Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.List

Goal state before:
pp: case cons
R : Type u_1
inst✝⁴ : CommMonoidWithZero R
inst✝³ : PartialOrder R
inst✝² : ZeroLEOneClass R
inst✝¹ : PosMulStrictMono R
inst✝ : NeZero 1
a : R
s : List R
hind : (∀ (a : R), a ∈ s → 0 < a) → 0 < s.prod
h : 0 < a ∧ ∀ (a : R), a ∈ s → 0 < a
⊢ 0 < a * s.prod

Tactic:
exact mul_pos h.1 (hind h.2)

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
⊢ image Prod.fst f.graph = f.support

Tactic:
[

Goal state after:
α : Type u_1
M : Type u_5
inst✝¹ : Zero M
inst✝ : DecidableEq α
f : α →₀ M
⊢ image Prod.fst f.graph = f.support
Module: Mathlib.Algebra.Order.BigOperators.Ring.List

Goal state before:
pp: α : Type u_2
inst✝⁴ : CommSemiring α
inst✝³ : PartialOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
x : α
xs : List α
⊢ 0 < (x :: xs).prod ↔ ∀ (x_1 : α), x_1 ∈ x :: xs → 0 < x_1

Tactic:
[

Goal state after:
α : Type u_2
inst✝⁴ : CommSemiring α
inst✝³ : PartialOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
x : α
xs : List α
⊢ 0 < (x :: xs).prod ↔ ∀ (x_1 : α), x_1 ∈ x :: xs → 0 < x_1
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
S : Set α
f : α → β
x : α →₀ M
hS : ↑x.support ⊆ S
hf : Set.InjOn f S
a : α
ha : a ∈ S
⊢ ∑ a_1 ∈ x.support, (single (f a_1) (x a_1)) (f a) = x a

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
S : Set α
f : α → β
x : α →₀ M
hS : ↑x.support ⊆ S
hf : Set.InjOn f S
a : α
ha : a ∈ S
⊢ ∑ a_1 ∈ x.support, (single (f a_1) (x a_1)) (f a) = x a
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq β
f : α → β
s : α →₀ M
hf : Set.InjOn f ↑s.support
hx_w : α
hx_h_left : ¬s hx_w = 0
⊢ hx_w ∈ ↑s.support

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq β
f : α → β
s : α →₀ M
hf : Set.InjOn f ↑s.support
hx_w : α
hx_h_left : ¬s hx_w = 0
⊢ hx_w ∈ ↑s.support
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
hf : Surjective f
x : β →₀ M
⊢ mapDomain (f ∘ surjInv hf) x = x

Tactic:
(rightInverse_surjInv hf).id,

Goal state after:
case h
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
hf : Surjective f
x : β →₀ M
⊢ mapDomain id x = x
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
S : Set α
f : α → β
hf : Set.InjOn f S
v₁ : α →₀ M
hv₁ : v₁ ∈ {w | ↑w.support ⊆ S}
v₂ : α →₀ M
hv₂ : v₂ ∈ {w | ↑w.support ⊆ S}
eq : mapDomain f v₁ = mapDomain f v₂
a : α
h : a ∈ v₁.support ∪ v₂.support
⊢ (mapDomain f v₁) (f a) = v₂ a

pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
S : Set α
f : α → β
hf : Set.InjOn f S
v₁ : α →₀ M
hv₁ : v₁ ∈ {w | ↑w.support ⊆ S}
v₂ : α →₀ M
hv₂ : v₂ ∈ {w | ↑w.support ⊆ S}
eq : mapDomain f v₁ = mapDomain f v₂
a : α
h : a ∈ v₁.support ∪ v₂.support
⊢ a ∈ S

Tactic:
← mapDomain_apply' S _ hv₂ hf _,

Goal state after:
case pos
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
S : Set α
f : α → β
hf : Set.InjOn f S
v₁ : α →₀ M
hv₁ : v₁ ∈ {w | ↑w.support ⊆ S}
v₂ : α →₀ M
hv₂ : v₂ ∈ {w | ↑w.support ⊆ S}
eq : mapDomain f v₁ = mapDomain f v₂
a : α
h : a ∈ v₁.support ∪ v₂.support
⊢ (mapDomain f v₁) (f a) = (mapDomain f v₂) (f a)

α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
S : Set α
f : α → β
hf : Set.InjOn f S
v₁ : α →₀ M
hv₁ : v₁ ∈ {w | ↑w.support ⊆ S}
v₂ : α →₀ M
hv₂ : v₂ ∈ {w | ↑w.support ⊆ S}
eq : mapDomain f v₁ = mapDomain f v₂
a : α
h : a ∈ v₁.support ∪ v₂.support
⊢ a ∈ S

α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
S : Set α
f : α → β
hf : Set.InjOn f S
v₁ : α →₀ M
hv₁ : v₁ ∈ {w | ↑w.support ⊆ S}
v₂ : α →₀ M
hv₂ : v₂ ∈ {w | ↑w.support ⊆ S}
eq : mapDomain f v₁ = mapDomain f v₂
a : α
h : a ∈ v₁.support ∪ v₂.support
⊢ a ∈ S
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_1
M : Type u_4
N : Type u_5
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
inst✝¹ : Preorder N
inst✝ : IsOrderedMonoid N
f : M → N
p : M → Prop
h_one : f 1 ≤ 1
h_mul : ∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y
hp_mul : ∀ (x y : M), p x → p y → p (x * y)
g : ι → M
s : Finset ι
hs : ∀ i ∈ s, p (g i)
⊢ f (∏ i ∈ s, g i) ≤ ∏ i ∈ s, f (g i)

Tactic:
rcases eq_empty_or_nonempty s with (rfl | hs_nonempty)
  · simp [h_one]
  · exact le_prod_nonempty_of_submultiplicative_on_pred f p h_mul hp_mul g s hs_nonempty hs

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α → β
l : β →₀ M
hf : Set.BijOn f (f ⁻¹' ↑l.support) ↑l.support
⊢ l.support.preimage f ⋯ = ∅ → l.support = ∅

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α → β
l : β →₀ M
hf : Set.BijOn f (f ⁻¹' ↑l.support) ↑l.support
⊢ l.support.preimage f ⋯ = ∅ → l.support = ∅
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α → β
a : α
hif : Set.InjOn f (f ⁻¹' ↑(single (f a) 0).support)
⊢ comapDomain f (single (f a) 0) hif = single a 0

Tactic:
[

Goal state after:
case inl
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α → β
a : α
hif : Set.InjOn f (f ⁻¹' ↑(single (f a) 0).support)
⊢ comapDomain f (single (f a) 0) hif = single a 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✝ : 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
⊢ ∏ i ∈ s, g i + ∏ i ∈ s, h i ≤ ∏ i ∈ s, f i

Tactic:
[

Goal state after:
ι : 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
⊢ ∏ i ∈ s, g i + ∏ i ∈ s, h i ≤ ∏ i ∈ s, f i
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
⊢ (filter p f).prod g * (filter (fun a ↦ ¬p a) f).prod g = f.prod g

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
⊢ (filter p f).prod g * (filter (fun a ↦ ¬p a) f).prod g = f.prod g
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
p : α → Prop
f g : α →₀ M
⊢ subtypeDomain p f = subtypeDomain p g ↔ ∀ (x : α), p x → f x = g x

Tactic:
[

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : Zero M
p : α → Prop
f g : α →₀ M
⊢ subtypeDomain p f = subtypeDomain p g ↔ ∀ (x : α), p x → f x = g x
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
inst✝¹ : AddZeroClass M
p✝ : α → Prop
v v' : α →₀ M
p : α → Prop
inst✝ : DecidablePred p
f g : α →₀ M
⊢ ⇑(filter p (f + g)) = ⇑(filter p f + filter p g)

Tactic:
[

Goal state after:
α : 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
inst✝¹ : AddZeroClass M
p✝ : α → Prop
v v' : α →₀ M
p : α → Prop
inst✝ : DecidablePred p
f g : α →₀ M
⊢ ⇑(filter p (f + g)) = ⇑(filter p f + filter p g)
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
⊢ ∏ i ∈ s, g i + ∏ i ∈ s, h i ≤ ∏ i ∈ s, 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
⊢ ∏ i ∈ s, g i + ∏ i ∈ s, h i ≤ ∏ i ∈ s, f i
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: case neg
α : Type u_1
M : Type u_5
inst✝ : AddCommMonoid M
s✝ : Multiset (α →₀ M)
a : α
f : α →₀ M
s : Multiset (α →₀ M)
ih : a ∈ s.sum.support → ∃ f ∈ s, a ∈ f.support
ha : a ∈ (f ::ₘ s).sum.support
h : a ∉ f.support
⊢ ∃ f_1 ∈ f ::ₘ s, a ∈ f_1.support

Tactic:
[

Goal state after:
case neg
α : Type u_1
M : Type u_5
inst✝ : AddCommMonoid M
s✝ : Multiset (α →₀ M)
a : α
f : α →₀ M
s : Multiset (α →₀ M)
ih : a ∈ s.sum.support → ∃ f ∈ s, a ∈ f.support
ha : a ∈ (f ::ₘ s).sum.support
h : a ∉ f.support
⊢ ∃ f_1 ∈ f ::ₘ s, a ∈ f_1.support
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
s : Finset α
B : Finset (Finset α)
n : ℕ
h : ∀ a ∈ s, #({b ∈ B | a ∈ b}) ≤ n
⊢ ∑ t ∈ B, #(s ∩ t) ≤ ∑ x ∈ s, #({b ∈ B | x ∈ b})

Tactic:
[

Goal state after:
α : Type u_2
inst✝ : DecidableEq α
s : Finset α
B : Finset (Finset α)
n : ℕ
h : ∀ a ∈ s, #({b ∈ B | a ∈ b}) ≤ n
⊢ ∑ t ∈ B, #(s ∩ t) ≤ ∑ x ∈ s, #({b ∈ B | x ∈ b})
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : Zero M
inst✝ : DecidableEq α
f : α × β →₀ M
⊢ f.curry.support = image Prod.fst f.support

Tactic:
unfold Finsupp.curry; congr!

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
B : Finset (Finset α)
n : ℕ
inst✝ : Fintype α
h : ∀ (a : α), #({b ∈ B | a ∈ b}) ≤ n
⊢ ∑ s ∈ B, #s = ∑ s ∈ B, #(univ ∩ s)

Tactic:
[

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
B : Finset (Finset α)
n : ℕ
inst✝ : Fintype α
h : ∀ (a : α), #({b ∈ B | a ∈ b}) ≤ n
⊢ ∑ s ∈ B, #s = ∑ s ∈ B, #(univ ∩ s)
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
s : Finset α
B : Finset (Finset α)
n : ℕ
h : ∀ a ∈ s, n ≤ #({b ∈ B | a ∈ b})
⊢ ∑ x ∈ s, #({b ∈ B | x ∈ b}) ≤ ∑ t ∈ B, #(s ∩ t)

Tactic:
[

Goal state after:
α : Type u_2
inst✝ : DecidableEq α
s : Finset α
B : Finset (Finset α)
n : ℕ
h : ∀ a ∈ s, n ≤ #({b ∈ B | a ∈ b})
⊢ ∑ x ∈ s, #({b ∈ B | x ∈ b}) ≤ ∑ t ∈ B, #(s ∩ t)
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 ∈ s, g i) * (∑ i ∈ s, r i) ^ 2 + (∑ i ∈ s, g i) * (∑ i ∈ s, r i) ^ 2 =
    ∑ i ∈ s, (2 * r i * ∑ j ∈ s, g j) * ∑ j ∈ s, r j

Tactic:
[

Goal state after:
ι : 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 ∈ s, g i) * (∑ i ∈ s, r i) ^ 2 + (∑ i ∈ s, g i) * (∑ i ∈ s, r i) ^ 2 =
    ∑ i ∈ s, (2 * r i * ∑ j ∈ s, g j) * ∑ j ∈ s, r j
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
B : Finset (Finset α)
n : ℕ
inst✝ : Fintype α
h : ∀ (a : α), n ≤ #({b ∈ B | a ∈ b})
⊢ ∑ s ∈ B, #(univ ∩ s) = ∑ s ∈ B, #s

Tactic:
[

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
B : Finset (Finset α)
n : ℕ
inst✝ : Fintype α
h : ∀ (a : α), n ≤ #({b ∈ B | a ∈ b})
⊢ ∑ s ∈ B, #(univ ∩ s) = ∑ s ∈ B, #s
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
B : Finset (Finset α)
n : ℕ
inst✝ : Fintype α
h : ∀ (a : α), #({b ∈ B | a ∈ b}) = n
⊢ ∑ s ∈ B, #s = Fintype.card α * n

Tactic:
[

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
B : Finset (Finset α)
n : ℕ
inst✝ : Fintype α
h : ∀ (a : α), #({b ∈ B | a ∈ b}) = n
⊢ ∑ s ∈ B, #s = Fintype.card α * n
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
M : Type u_12
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
f : Subtype P →₀ M
g : { a // ¬P a } →₀ M
⊢ Disjoint (map (Embedding.subtype P) f.support) (map (Embedding.subtype fun a ↦ ¬P a) g.support)

Tactic:
[

Goal state after:
α : 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
M : Type u_12
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
f : Subtype P →₀ M
g : { a // ¬P a } →₀ M
⊢ Disjoint (map (Embedding.subtype P) f.support) (map (Embedding.subtype fun a ↦ ¬P a) g.support)
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
inst✝ : AddCommMonoid M
e : α ≃ β
v : α →₀ M
⊢ equivMapDomain e.symm (equivMapDomain e v) = v

Tactic:
[

Goal state after:
α : 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
inst✝ : AddCommMonoid M
e : α ≃ β
v : α →₀ M
⊢ equivMapDomain e.symm (equivMapDomain e v) = v
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
inst✝ : AddCommMonoid M
e : α ≃ β
v : β →₀ M
⊢ equivMapDomain e (equivMapDomain e.symm v) = v

Tactic:
[

Goal state after:
α : 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
inst✝ : AddCommMonoid M
e : α ≃ β
v : β →₀ M
⊢ equivMapDomain e (equivMapDomain e.symm v) = v
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
⊢ l.support = l.splitSupport.sigma fun i ↦ (l.split i).support

Tactic:
[

Goal state after:
ι : Type u_4
M : Type u_5
αs : ι → Type u_12
inst✝ : Zero M
l : (i : ι) × αs i →₀ M
⊢ l.support = l.splitSupport.sigma fun i ↦ (l.split i).support
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 ∈ s, (f i * (∑ j ∈ s, g j) ^ 2 + g i * (∑ j ∈ s, r j) ^ 2) =
    (∑ i ∈ s, g i) * (∑ i ∈ s, r i) ^ 2 + (∑ i ∈ s, g i) * ((∑ i ∈ s, f i) * ∑ i ∈ s, g i)

Tactic:
[

Goal state after:
ι : 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 ∈ s, (f i * (∑ j ∈ s, g j) ^ 2 + g i * (∑ j ∈ s, r j) ^ 2) =
    (∑ i ∈ s, g i) * (∑ i ∈ s, r i) ^ 2 + (∑ i ∈ s, g i) * ((∑ i ∈ s, f i) * ∑ i ∈ s, g i)
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : LinearOrder M
s : Finset ι
inst✝ : IsOrderedCancelMonoid M
f : ι → M
h₁ : ∏ i ∈ s, f i = 1
h₂ : ∃ i ∈ s, f i ≠ 1
⊢ ∃ i ∈ s, 1 < f i

Tactic:
contrapose! h₁

Goal state after:
ι : Type u_1
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : LinearOrder M
s : Finset ι
inst✝ : IsOrderedCancelMonoid M
f : ι → M
h₂ : ∃ i ∈ s, f i ≠ 1
h₁ : ∀ i ∈ s, f i ≤ 1
⊢ ∏ i ∈ s, f i ≠ 1
Module: Mathlib.Algebra.BigOperators.GroupWithZero.Action

Goal state before:
pp: M : Type u_1
N : Type u_2
ι : Type u_4
inst✝⁴ : CommMonoid N
inst✝³ : Monoid M
inst✝² : MulAction M N
inst✝¹ : IsScalarTower M N N
inst✝ : SMulCommClass M N N
s : Finset ι
b : M
f : ι → N
this : Multiset.map (fun x ↦ b • f x) s.val = Multiset.map (fun x ↦ b • x) (Multiset.map f s.val)
⊢ b ^ #s • ∏ x ∈ s, f x = ∏ x ∈ s, b • f x

Tactic:
[

Goal state after:
M : Type u_1
N : Type u_2
ι : Type u_4
inst✝⁴ : CommMonoid N
inst✝³ : Monoid M
inst✝² : MulAction M N
inst✝¹ : IsScalarTower M N N
inst✝ : SMulCommClass M N N
s : Finset ι
b : M
f : ι → N
this : Multiset.map (fun x ↦ b • f x) s.val = Multiset.map (fun x ↦ b • x) (Multiset.map f s.val)
⊢ b ^ #s • ∏ x ∈ s, f x = ∏ x ∈ s, b • f x
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: case cons
α : Type u_2
β : Type u_3
inst✝ : DecidableEq α
f : β → Multiset α
z : β
i : Finset β
hz : z ∉ i
hr : i.sum f = i.sup f ↔ ∀ x ∈ i, ∀ y ∈ i, x ≠ y → Disjoint (f x) (f y)
⊢ (Finset.cons z i hz).sum f = (Finset.cons z i hz).sup f ↔
    ∀ x ∈ Finset.cons z i hz, ∀ y ∈ Finset.cons z i hz, x ≠ y → Disjoint (f x) (f y)

Tactic:
[

Goal state after:
case cons
α : Type u_2
β : Type u_3
inst✝ : DecidableEq α
f : β → Multiset α
z : β
i : Finset β
hz : z ∉ i
hr : i.sum f = i.sup f ↔ ∀ x ∈ i, ∀ y ∈ i, x ≠ y → Disjoint (f x) (f y)
⊢ (Finset.cons z i hz).sum f = (Finset.cons z i hz).sup f ↔
    ∀ x ∈ Finset.cons z i hz, ∀ y ∈ Finset.cons z i hz, x ≠ y → Disjoint (f x) (f y)
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: case cons
α : Type u_2
β : Type u_3
inst✝ : DecidableEq α
f : β → Multiset α
z : β
i : Finset β
hz : z ∉ i
hr : i.sum f = i.sup f ↔ ∀ x ∈ i, ∀ y ∈ i, x ≠ y → Disjoint (f x) (f y)
this : ∀ x ∈ i, x ≠ z
⊢ f z + ∑ x ∈ i, f x = f z ∪ i.sup f ↔
    (∀ a ∈ i, Disjoint (f z) (f a)) ∧ (∀ x ∈ i, Disjoint (f x) (f z)) ∧ i.sum f = i.sup f

Tactic:
[

Goal state after:
case cons
α : Type u_2
β : Type u_3
inst✝ : DecidableEq α
f : β → Multiset α
z : β
i : Finset β
hz : z ∉ i
hr : i.sum f = i.sup f ↔ ∀ x ∈ i, ∀ y ∈ i, x ≠ y → Disjoint (f x) (f y)
this : ∀ x ∈ i, x ≠ z
⊢ f z + ∑ x ∈ i, f x = f z ∪ i.sup f ↔
    (∀ a ∈ i, Disjoint (f z) (f a)) ∧ (∀ x ∈ i, Disjoint (f x) (f z)) ∧ i.sum f = i.sup f
Module: Mathlib.LinearAlgebra.Finsupp.Supported

Goal state before:
pp: α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
R : Type u_5
S : Type u_6
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
s : Set α
F : ↥(supported M R s) ≃ (↑s →₀ M) := restrictSupportEquiv s M
this : ⇑F = ⇑(lsubtypeDomain s ∘ₗ (supported M R s).subtype)
⊢ IsLinearMap R ⇑F

Tactic:
this

Goal state after:
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
R : Type u_5
S : Type u_6
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
s : Set α
F : ↥(supported M R s) ≃ (↑s →₀ M) := restrictSupportEquiv s M
this : ⇑F = ⇑(lsubtypeDomain s ∘ₗ (supported M R s).subtype)
⊢ IsLinearMap R ⇑(lsubtypeDomain s ∘ₗ (supported M R s).subtype)
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: case inl
α : Type u_1
R : Type u_7
inst✝ : NonAssocSemiring R
f : α → R
h : ∑ᶠ (i : α), f i = 1
h✝ : Subsingleton R
⊢ HasFiniteSupport f

Tactic:
[

Goal state after:
case inl
α : Type u_1
R : Type u_7
inst✝ : NonAssocSemiring R
f : α → R
h : ∑ᶠ (i : α), f i = 1
h✝ : Subsingleton R
⊢ HasFiniteSupport f
Module: Mathlib.LinearAlgebra.Basis.Defs

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : Type u_6
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Fintype ι
b : Basis ι R M
c : ι → R
⊢ ⇑(b.repr (∑ i, c i • b i)) = c

Tactic:
[

Goal state after:
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Fintype ι
b : Basis ι R M
c : ι → R
⊢ ⇑(b.repr (∑ i, c i • b i)) = c
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝¹ : CommMonoid M
f : α → M
s : Set α
inst✝ : Fintype ↑s
⊢ s ∩ mulSupport f = ↑s.toFinset ∩ mulSupport f

Tactic:
[

Goal state after:
α : Type u_1
M : Type u_5
inst✝¹ : CommMonoid M
f : α → M
s : Set α
inst✝ : Fintype ↑s
⊢ s ∩ mulSupport f = ↑s.toFinset ∩ mulSupport f
Module: Mathlib.LinearAlgebra.Basis.Defs

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : Type u_6
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Finite ι
e : M ≃ₗ[R] ι → R
j : M
x✝ : ι
⊢ (ofEquivFun e).equivFun j x✝ = e j x✝

Tactic:
[

Goal state after:
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Finite ι
e : M ≃ₗ[R] ι → R
j : M
x✝ : ι
⊢ (ofEquivFun e).equivFun j x✝ = e j x✝
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n : ℕ
i x✝ : Fin n
⊢ x✝ ∈ rev ⁻¹' Ici i ↔ x✝ ∈ Iic i.rev

Tactic:
simp [le_rev_iff]

Goal state after: