mathlib-initiative/mathlib-tactics huggingface dataset:
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✝ : DecidableEq ι
⊢ ∏ x ∈ s, f x ≤ ∏ x ∈ t, f x ↔ ∏ i ∈ s, f i ≤ ∏ i ∈ t, f i

pp: ι : Type u_1
M : Type u_4
inst✝³ : CommMonoid M
inst✝² : Preorder M
inst✝¹ : IsOrderedCancelMonoid M
f : ι → M
s t : Finset ι
inst✝ : DecidableEq ι
⊢ Disjoint (t \ s) (s ∩ t)

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✝ : DecidableEq ι
⊢ Disjoint (t \ s) (s ∩ t)
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝² : DecidableEq β
inst✝¹ : AddCommMonoid M
f : α → β
inst✝ : Subsingleton (AddUnits M)
x : α →₀ M
t : β
⊢ ¬(mapDomain f x) t = 0 ↔ ∃ a ∈ x.support, f a = t

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝² : DecidableEq β
inst✝¹ : AddCommMonoid M
f : α → β
inst✝ : Subsingleton (AddUnits M)
x : α →₀ M
t : β
⊢ ¬(mapDomain f x) t = 0 ↔ ∃ a ∈ x.support, f a = t
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : AddCommMonoid M
f : α → β
inst✝ : Subsingleton (AddUnits M)
x : α →₀ M
h : x = 0
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ExistsAddOfLE R
s : Finset ι
f g : ι → R
hg : ∀ i ∈ s, 0 < g i
hg' : ∀ i ∈ s, 0 ≤ g i
H : ∀ i ∈ s, 0 ≤ f i ^ 2 / g i
i : ι
hi : i ∈ s
⊢ f i ^ 2 ≤ f i ^ 2

pp: case h
ι : Type u_1
R : Type u_2
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ExistsAddOfLE R
s : Finset ι
f g : ι → R
hg : ∀ i ∈ s, 0 < g i
hg' : ∀ i ∈ s, 0 ≤ g i
H : ∀ i ∈ s, 0 ≤ f i ^ 2 / g i
i : ι
hi : i ∈ s
⊢ g i ≠ 0

Tactic:
]

Goal state after:
case h
ι : Type u_1
R : Type u_2
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ExistsAddOfLE R
s : Finset ι
f g : ι → R
hg : ∀ i ∈ s, 0 < g i
hg' : ∀ i ∈ s, 0 ≤ g i
H : ∀ i ∈ s, 0 ≤ f i ^ 2 / g i
i : ι
hi : i ∈ s
⊢ g i ≠ 0
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
inst✝ : DecidableEq ι
s t : Finset ι
f : ι → M
⊢ ∏ x ∈ s, f x < ∏ x ∈ t, f x ↔ ∏ i ∈ s, f i < ∏ i ∈ t, f i

pp: ι : Type u_9
M : Type u_10
inst✝³ : CommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedCancelMonoid M
inst✝ : DecidableEq ι
s t : Finset ι
f : ι → M
⊢ Disjoint (t \ s) (s ∩ t)

Tactic:
]

Goal state after:
ι : Type u_9
M : Type u_10
inst✝³ : CommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedCancelMonoid M
inst✝ : DecidableEq ι
s t : Finset ι
f : ι → M
⊢ Disjoint (t \ s) (s ∩ t)
Module: Mathlib.Data.Finsupp.SMulWithZero

Goal state before:
pp: α : Type u_1
M : Type u_5
R : Type u_11
inst✝¹ : Zero M
inst✝ : SMulZeroClass R M
b : R
g : α →₀ M
a : α
⊢ a ∈ (b • g).support → a ∈ g.support

Tactic:
simp only [smul_apply, mem_support_iff, Ne]
  exact mt fun h => h.symm ▸ smul_zero _

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
G : Type u_5
R : Type u_6
inst✝² : Monoid G
inst✝¹ : MulAction G α
inst✝ : AddCommMonoid M
g g' : G
f : α →₀ M
⊢ mapDomain (fun x ↦ g • x) (mapDomain (fun x ↦ g' • x) f) = mapDomain (fun x ↦ g • x) (mapDomain (fun x ↦ g' • x) f)

Tactic:
]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
G : Type u_5
R : Type u_6
inst✝² : Monoid G
inst✝¹ : MulAction G α
inst✝ : AddCommMonoid M
f : α →₀ M
⊢ f = f

Tactic:
]

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

Goal state before:
pp: α : Type u_1
M : Type u_3
G : Type u_5
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : AddCommMonoid M
g : G
f : α →₀ M
a : α
| (g • f) a

Tactic:
rw [← smul_inv_smul g a]

Goal state after:
α : Type u_1
M : Type u_3
G : Type u_5
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : AddCommMonoid M
g : G
f : α →₀ M
a : α
| (g • f) (g • g⁻¹ • a)
Module: Mathlib.Data.Finsupp.SMul

Goal state before:
pp: α : Type u_1
R : Type u_6
inst✝ : MulZeroOneClass R
a : α
b : R
⊢ single a b = single a b

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.BigOperators.GroupWithZero.Action

Goal state before:
pp: case cons
M : Type u_1
N : Type u_2
ι : Type u_4
inst✝⁴ : CommMonoid N
inst✝³ : CommMonoid M
inst✝² : MulAction M N
inst✝¹ : IsScalarTower M N N
inst✝ : SMulCommClass M N N
b : ι → M
f : ι → N
a✝ : ι
s✝ : Finset ι
hj : a✝ ∉ s✝
ih : ∏ i ∈ s✝, b i • f i = (∏ i ∈ s✝, b i) • ∏ i ∈ s✝, f i
⊢ (∏ x ∈ cons a✝ s✝ hj, b x) • ∏ x ∈ cons a✝ s✝ hj, f x = (∏ i ∈ cons a✝ s✝ hj, b i) • ∏ i ∈ cons a✝ s✝ hj, f i

Tactic:
]

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

Goal state before:
pp: case refine_2
α : Type u_2
s : Finset α
f : α → ℕ
h : ∀ (x y : α), x ∈ s → y ∈ s → f x ≠ 0 → f y ≠ 0 → x = y ∧ f x = 1
⊢ ∑ x ∈ s, f x ≤ 1

Tactic:
· by_cases! hx : ∃ x ∈ s, f x ≠ 0
    · obtain ⟨x, hsx, hfx⟩ := hx
      have hs : ∀ y ∈ s \ {x}, f y = 0 := by grind
      simp [← sum_sdiff (singleton_subset_iff.2 hsx), sum_congr rfl hs, (h x x hsx hsx hfx hfx).2]
    · simp [sum_congr rfl hx]

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

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
x : Multiset α
⊢ ((Finset.range (x.card + 1)).sup fun k ↦ powersetCard k x) = ∑ x_1 ∈ Finset.range (x.card + 1), powersetCard x_1 x

Tactic:
]

Goal state after:
α : Type u_2
inst✝ : DecidableEq α
x : Multiset α
⊢ ((Finset.range (x.card + 1)).sup fun k ↦ powersetCard k x) = ∑ x_1 ∈ Finset.range (x.card + 1), powersetCard x_1 x
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
m : Multiset α
⊢ (∀ (x y : α), x ∈ m.toFinset → y ∈ m.toFinset → count x m - 1 ≠ 0 → count y m - 1 ≠ 0 → x = y ∧ count x m - 1 = 1) ↔
    ∀ (x y : α), 1 < count x m → 1 < count y m → x = y ∧ count x m = 2

Tactic:
]

Goal state after:
α : Type u_2
inst✝ : DecidableEq α
m : Multiset α
⊢ (∀ (x y : α), x ∈ m.toFinset → y ∈ m.toFinset → count x m - 1 ≠ 0 → count y m - 1 ≠ 0 → x = y ∧ count x m - 1 = 1) ↔
    ∀ (x y : α), 1 < count x m → 1 < count y m → x = y ∧ count x m = 2
Module: Mathlib.LinearAlgebra.Finsupp.Defs

Goal state before:
pp: R✝ : Type u_1
M✝ : Type u_2
N : Type u_3
inst✝⁷ : Semiring R✝
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R✝ N
ι : Type u_4
R : Type u_5
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End (End R M) M
g : End R (ι →₀ M)
x x✝¹ x✝ : ι →₀ M
h : (mapRange.addMonoidHom ↑f) (g • x✝¹) = (RingHom.id (End R (ι →₀ M))) g • (mapRange.addMonoidHom ↑f) x✝¹
h' : (mapRange.addMonoidHom ↑f) (g • x✝) = (RingHom.id (End R (ι →₀ M))) g • (mapRange.addMonoidHom ↑f) x✝
⊢ (RingHom.id (End R (ι →₀ M))) g • (mapRange.addMonoidHom ↑f) x✝¹ +
      (RingHom.id (End R (ι →₀ M))) g • (mapRange.addMonoidHom ↑f) x✝ =
    (RingHom.id (End R (ι →₀ M))) g • (mapRange.addMonoidHom ↑f) x✝¹ +
      (RingHom.id (End R (ι →₀ M))) g • (mapRange.addMonoidHom ↑f) x✝

Tactic:
]

Goal state after:
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 α
p q : α →₀ M
hp : p ∈ {p | ↑p.support ⊆ s}
hq : q ∈ {p | ↑p.support ⊆ s}
⊢ ↑p.support ∪ ↑q.support ⊆ ↑p.support ∪ ↑q.support

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.Defs

Goal state before:
pp: R✝ : Type u_1
M✝ : Type u_2
N : Type u_3
inst✝⁷ : Semiring R✝
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R✝ N
ι : Type u_4
R : Type u_5
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End (End R M) M
g : End R (ι →₀ M)
x : ι →₀ M
i : ι
m : M
j : ι
⊢ lapply j ∘ₗ g ∘ₗ lsingle i • f m = ((RingHom.id (End R (ι →₀ M))) g • (mapRange.addMonoidHom ↑f) (single i m)) j

Tactic:
]

Goal state after:
R✝ : Type u_1
M✝ : Type u_2
N : Type u_3
inst✝⁷ : Semiring R✝
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R✝ N
ι : Type u_4
R : Type u_5
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End (End R M) M
g : End R (ι →₀ M)
x : ι →₀ M
i : ι
m : M
j : ι
⊢ lapply j ∘ₗ g ∘ₗ lsingle i • f m = ((RingHom.id (End R (ι →₀ M))) g • (mapRange.addMonoidHom ↑f) (single i m)) j
Module: Mathlib.LinearAlgebra.Finsupp.Supported

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : α →₀ M
⊢ ↑p.support ⊆ ↑p.support

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.Supported

Goal state before:
pp: case refine_2
α : Type u_1
R : Type u_5
inst✝ : Semiring R
s : Set α
l : α →₀ R
hl : l ∈ supported R R s
⊢ l.sum single ∈ span R ((fun i ↦ single i 1) '' s)

Tactic:
]

Goal state after:
case refine_2
α : Type u_1
R : Type u_5
inst✝ : Semiring R
s : Set α
l : α →₀ R
hl : l ∈ supported R R s
⊢ l.sum single ∈ span R ((fun i ↦ single i 1) '' s)
Module: Mathlib.LinearAlgebra.Finsupp.Supported

Goal state before:
pp: case refine_2
α : Type u_1
R : Type u_5
inst✝ : Semiring R
s : Set α
l : α →₀ R
hl : l ∈ supported R R s
i : α
il : i ∈ l.support
⊢ l i • single i 1 ∈ span R ((fun i ↦ single i 1) '' s)

Tactic:
]

Goal state after:
case refine_2
α : Type u_1
R : Type u_5
inst✝ : Semiring R
s : Set α
l : α →₀ R
hl : l ∈ supported R R s
i : α
il : i ∈ l.support
⊢ l i • single i 1 ∈ span R ((fun i ↦ single i 1) '' s)
Module: Mathlib.LinearAlgebra.Finsupp.Supported

Goal state before:
pp: case refine_2
α : Type u_1
R : Type u_5
inst✝ : Semiring R
s : Set α
l : α →₀ R
hl : l ∈ supported R R s
i : α
il : i ∈ l.support
⊢ l i • single i 1 ∈ span R ((fun i ↦ single i 1) '' s)

Tactic:
exact smul_mem _ (l i) (subset_span (mem_image_of_mem _ (hl il)))

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.Supported

Goal state before:
pp: α : Type u_1
R : Type u_5
inst✝¹ : Semiring R
inst✝ : Nontrivial R
a : α
s : Set α
h : ↑{a} ⊆ s
⊢ a ∈ s

Tactic:
]

Goal state after:
α : Type u_1
R : Type u_5
inst✝¹ : Semiring R
inst✝ : Nontrivial R
a : α
s : Set α
h : ↑{a} ⊆ s
⊢ a ∈ s
Module: Mathlib.LinearAlgebra.Finsupp.Defs

Goal state before:
pp: R✝ : Type u_1
M✝ : Type u_2
N : Type u_3
inst✝⁷ : Semiring R✝
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R✝ N
ι : Type u_4
R : Type u_5
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i : ι
f : End (End R (ι →₀ M)) (ι →₀ M)
g✝ : End R M
m : M
g : (ι →₀ M) →ₗ[R] ι →₀ M := mapRange.linearMap g✝
⊢ (f (single i (g✝ • m))) i = (f (g • single i m)) i

Tactic:
]

Goal state after:
R✝ : Type u_1
M✝ : Type u_2
N : Type u_3
inst✝⁷ : Semiring R✝
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R✝ N
ι : Type u_4
R : Type u_5
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i : ι
f : End (End R (ι →₀ M)) (ι →₀ M)
g✝ : End R M
m : M
g : (ι →₀ M) →ₗ[R] ι →₀ M := mapRange.linearMap g✝
⊢ (f (single i (g✝ • m))) i = (f (g • single i m)) i
Module: Mathlib.LinearAlgebra.Finsupp.Defs

Goal state before:
pp: R✝ : Type u_1
M✝ : Type u_2
N : Type u_3
inst✝⁷ : Semiring R✝
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R✝ N
ι : Type u_4
R : Type u_5
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i : ι
f : End (End R (ι →₀ M)) (ι →₀ M)
x : ι →₀ M
j : ι
⊢ (lsingle i ∘ₗ lapply j • f x) i = (f x) j

Tactic:
]

Goal state after:
R✝ : Type u_1
M✝ : Type u_2
N : Type u_3
inst✝⁷ : Semiring R✝
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R✝ N
ι : Type u_4
R : Type u_5
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i : ι
f : End (End R (ι →₀ M)) (ι →₀ M)
x : ι →₀ M
j : ι
⊢ (lsingle i ∘ₗ lapply j • f x) i = (f x) j
Module: Mathlib.LinearAlgebra.Finsupp.Supported

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
δ : Type u_7
s : δ → Set α
this✝ : DecidablePred fun x ↦ x ∈ ⋃ i, s i
this : supported M R (⋃ i, s i) ≤ ⨆ i, supported M R (s i)
⊢ supported M R (⋃ i, s i) ≤ ⨆ i, supported M R (s i)

Tactic:
]

Goal state after:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
δ : Type u_7
s : δ → Set α
this✝ : DecidablePred fun x ↦ x ∈ ⋃ i, s i
this : supported M R (⋃ i, s i) ≤ ⨆ i, supported M R (s i)
⊢ supported M R (⋃ i, s i) ≤ ⨆ i, supported M R (s i)
Module: Mathlib.LinearAlgebra.Finsupp.Supported

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
δ : Type u_7
s : δ → Set α
this : DecidablePred fun x ↦ x ∈ ⋃ i, s i
⊢ ⊤ ≤ comap ((supported M R (⋃ i, s i)).subtype ∘ₗ restrictDom M R (⋃ i, s i)) (⨆ i, supported M R (s i))

Tactic:
]

Goal state after:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
δ : Type u_7
s : δ → Set α
this : DecidablePred fun x ↦ x ∈ ⋃ i, s i
⊢ ⊤ ≤ comap ((supported M R (⋃ i, s i)).subtype ∘ₗ restrictDom M R (⋃ i, s i)) (⨆ i, supported M R (s i))
Module: Mathlib.LinearAlgebra.Finsupp.LSum

Goal state before:
pp: α : Type u_1
R : Type u_3
R₂ : Type u_4
M : Type u_5
M₂ : Type u_6
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
σ : R →+* R₂
v : α →₀ M
c : R
h : α → M →ₛₗ[σ] M₂
⊢ (v.sum fun i c_1 ↦ (h i) (c • c_1)) = v.sum fun a b ↦ σ c • (h a) b

pp: α : Type u_1
R : Type u_3
R₂ : Type u_4
M : Type u_5
M₂ : Type u_6
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
σ : R →+* R₂
v : α →₀ M
c : R
h : α → M →ₛₗ[σ] M₂
⊢ ∀ (i : α), (h i) 0 = 0

Tactic:
]

Goal state after:
α : Type u_1
R : Type u_3
R₂ : Type u_4
M : Type u_5
M₂ : Type u_6
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
σ : R →+* R₂
v : α →₀ M
c : R
h : α → M →ₛₗ[σ] M₂
⊢ (v.sum fun i c_1 ↦ (h i) (c • c_1)) = v.sum fun a b ↦ σ c • (h a) b

α : Type u_1
R : Type u_3
R₂ : Type u_4
M : Type u_5
M₂ : Type u_6
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
σ : R →+* R₂
v : α →₀ M
c : R
h : α → M →ₛₗ[σ] M₂
⊢ ∀ (i : α), (h i) 0 = 0
Module: Mathlib.LinearAlgebra.Finsupp.LSum

Goal state before:
pp: α : Type u_1
M✝ : Type u_2
N✝ : Type u_3
P : Type u_4
R✝ : Type u_5
R₂ : Type u_6
R₃ : Type u_7
S✝ : Type u_8
inst✝¹⁷ : Semiring R✝
inst✝¹⁶ : Semiring R₂
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
σ : R✝ →+* R₂
σ_inv : R₂ →+* R✝
R : Type u_9
S : Type u_10
M : Type u_11
N : Type u_12
ι : Type u_13
inst✝⁷ : Semiring S
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module S M
inst✝³ : Module S N
inst✝² : SMulZeroClass R M
inst✝¹ : DistribSMul R N
inst✝ : CompatibleSMul M N R S
f : (ι →₀ M) →ₗ[S] N
r : R
m : ι →₀ M
⊢ (m.sum fun a b ↦ f (single a (r • b))) = m.sum fun a b ↦ r • f (single a b)

Tactic:
]

Goal state after:
α : Type u_1
M✝ : Type u_2
N✝ : Type u_3
P : Type u_4
R✝ : Type u_5
R₂ : Type u_6
R₃ : Type u_7
S✝ : Type u_8
inst✝¹⁷ : Semiring R✝
inst✝¹⁶ : Semiring R₂
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
σ : R✝ →+* R₂
σ_inv : R₂ →+* R✝
R : Type u_9
S : Type u_10
M : Type u_11
N : Type u_12
ι : Type u_13
inst✝⁷ : Semiring S
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module S M
inst✝³ : Module S N
inst✝² : SMulZeroClass R M
inst✝¹ : DistribSMul R N
inst✝ : CompatibleSMul M N R S
f : (ι →₀ M) →ₗ[S] N
r : R
m : ι →₀ M
⊢ (m.sum fun a b ↦ f (single a (r • b))) = m.sum fun a b ↦ r • f (single a b)
Module: Mathlib.LinearAlgebra.Finsupp.Supported

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s t : Set α
⊢ supported M R s ⊔ supported M R t = supported M R s ⊔ supported M R t

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.Supported

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s t : Set α
⊢ supported M R (bif true then s else t) ⊓ supported M R (bif false then s else t) = supported M R s ⊓ supported M R t

Tactic:
]

Goal state after:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s t : Set α
⊢ supported M R (bif true then s else t) ⊓ supported M R (bif false then s else t) = supported M R s ⊓ supported M R t
Module: Mathlib.LinearAlgebra.Finsupp.Supported

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s t : Set α
h : Disjoint s t
⊢ ⊥ = ⊥

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.Supported

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial M
s t : Set α
h : Disjoint (supported M R s) (supported M R t)
x : α
hx1 : x ∈ s
hx2 : x ∈ t
y : M
hy : y ≠ 0
this : y = 0
⊢ False

Tactic:
]

Goal state after:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial M
s t : Set α
h : Disjoint (supported M R s) (supported M R t)
x : α
hx1 : x ∈ s
hx2 : x ∈ t
y : M
hy : y ≠ 0
this : y = 0
⊢ False
Module: Mathlib.LinearAlgebra.Finsupp.Supported

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s t : Set α
h : Codisjoint s t
⊢ ⊤ ≤ ⊤

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.Supported

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial M
s t : Set α
h : ∀ (x : α →₀ M), x ∈ supported M R (s ∪ t)
a : α
x : M
hx : x ≠ 0
⊢ a ∈ ⊤ → a ∈ s ⊔ t

Tactic:
]

Goal state after:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial M
s t : Set α
h : ∀ (x : α →₀ M), x ∈ supported M R (s ∪ t)
a : α
x : M
hx : x ≠ 0
⊢ a ∈ ⊤ → a ∈ s ⊔ t
Module: Mathlib.LinearAlgebra.Finsupp.LSum

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type u_4
f : M →ₗ[R] α →₀ R
s : Surjective ⇑f
x a✝ : α
⊢ f ⋯.choose = single x 1

pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type u_4
f : M →ₗ[R] α →₀ R
s : Surjective ⇑f
x a✝ : α
⊢ 0 • ⋯.choose = 0

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type u_4
f : M →ₗ[R] α →₀ R
s : Surjective ⇑f
x a✝ : α
⊢ f ⋯.choose = single x 1

R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type u_4
f : M →ₗ[R] α →₀ R
s : Surjective ⇑f
x a✝ : α
⊢ 0 • ⋯.choose = 0
Module: Mathlib.LinearAlgebra.Finsupp.LSum

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type u_4
f : M →ₗ[R] α →₀ R
s : Surjective ⇑f
x a✝ : α
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: M : Type u_2
α : Sort u_4
inst✝ : CommMonoid M
f : α → M
hf : HasFiniteMulSupport (f ∘ PLift.down)
s : Finset (PLift α)
hs : Finite.toFinset hf ⊆ s
⊢ ∏ i ∈ Finite.toFinset hf, f i.down = ∏ i ∈ s, f i.down

Tactic:
]

Goal state after:
M : Type u_2
α : Sort u_4
inst✝ : CommMonoid M
f : α → M
hf : HasFiniteMulSupport (f ∘ PLift.down)
s : Finset (PLift α)
hs : Finite.toFinset hf ⊆ s
⊢ ∏ i ∈ Finite.toFinset hf, f i.down = ∏ i ∈ s, f i.down
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: M : Type u_2
α : Sort u_4
inst✝ : CommMonoid M
f : α → M
hf : HasFiniteMulSupport (f ∘ PLift.down)
s : Finset (PLift α)
hs : Finite.toFinset hf ⊆ s
x : PLift α
x✝ : x ∈ s
hxf : (f ∘ PLift.down) x = 1
⊢ f x.down = 1

Tactic:
]

Goal state after:
M : Type u_2
α : Sort u_4
inst✝ : CommMonoid M
f : α → M
hf : HasFiniteMulSupport (f ∘ PLift.down)
s : Finset (PLift α)
hs : Finite.toFinset hf ⊆ s
x : PLift α
x✝ : x ∈ s
hxf : (f ∘ PLift.down) x = 1
⊢ f x.down = 1
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: M : Type u_2
α : Sort u_4
inst✝ : CommMonoid M
f : α → M
s : Finset (PLift α)
hs : mulSupport (f ∘ PLift.down) ⊆ ↑s
x : PLift α
hx : x ∈ mulSupport (f ∘ PLift.down)
⊢ x ∈ s

Tactic:
]

Goal state after:
M : Type u_2
α : Sort u_4
inst✝ : CommMonoid M
f : α → M
s : Finset (PLift α)
hs : mulSupport (f ∘ PLift.down) ⊆ ↑s
x : PLift α
hx : x ∈ mulSupport (f ∘ PLift.down)
⊢ x ∈ s
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 ⇑(lsubtypeDomain s ∘ₗ (supported M R s).subtype)

Tactic:
]

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: M : Type u_2
α : Sort u_4
inst✝ : CommMonoid M
this : (mulSupport fun x ↦ (fun x ↦ 1) x.down) ⊆ ↑∅
⊢ 1 = 1

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: M : Type u_2
α : Sort u_4
inst✝¹ : CommMonoid M
inst✝ : IsEmpty α
f : α → M
⊢ ∏ᶠ (i : α), f i = ∏ᶠ (x : ?m.10), 1

pp: M : Type u_2
α : Sort u_4
inst✝¹ : CommMonoid M
inst✝ : IsEmpty α
f : α → M
⊢ Sort ?u.23

Tactic:
]

Goal state after:
M : Type u_2
α : Sort u_4
inst✝¹ : CommMonoid M
inst✝ : IsEmpty α
f : α → M
⊢ ∏ᶠ (i : α), f i = ∏ᶠ (x : ?m.10), 1

M : Type u_2
α : Sort u_4
inst✝¹ : CommMonoid M
inst✝ : IsEmpty α
f : α → M
⊢ Sort ?u.23
Module: Mathlib.LinearAlgebra.Finsupp.Supported

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α' : Type u_7
f : α → α'
s : Set α'
⊢ supported M R (f ⁻¹' s) ≤ comap (lmapDomain M R f) (supported M R s)

Tactic:
intro l (hl : (l.support : Set α) ⊆ f ⁻¹' s)

Goal state after:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α' : Type u_7
f : α → α'
s : Set α'
l : α →₀ M
hl : ↑l.support ⊆ f ⁻¹' s
⊢ l ∈ comap (lmapDomain M R f) (supported M R s)
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: 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 }}
⊢ f { down := a }.down = f a

Tactic:
]

Goal state after: