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

Goal state before:
pp: α : Type u_4
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
l : Multiset α
n : α
h : ∀ (x : α), x ∈ l → x ≤ n
⊢ fold max ⊥ l ≤ n

Tactic:
induction l using Quotient.inductionOn
  simpa using List.max_le_of_forall_le _ _ h

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

Goal state before:
pp: ι : Type u_1
s : Finset ι
M : Type u_4
inst✝³ : CommMonoidWithZero M
inst✝² : LinearOrder M
inst✝¹ : ZeroLEOneClass M
inst✝ : PosMulMono M
i : ι
hi : i ∈ s
f : ι → M
hf : 0 ≤ f i
x✝² : ι
x✝¹ : x✝² ∈ s
x✝ : x✝² ≠ i
⊢ (if i = x✝² then f i else 1) = 1

Tactic:
grind

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

Goal state before:
pp: ι : Type u_1
s : Finset ι
M : Type u_4
inst✝³ : CommMonoidWithZero M
inst✝² : LinearOrder M
inst✝¹ : ZeroLEOneClass M
inst✝ : PosMulMono M
i : ι
hi : i ∈ s
f : ι → M
hf : 0 ≤ f i
this : f i = ∏ j ∈ s, if i = j then f i else 1
x✝¹ : ι
x✝ : x✝¹ ∈ s
⊢ (if i = x✝¹ then f i else 1) ≤ max (f x✝¹) 1

Tactic:
grind

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : Preorder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
f : ι → R
s t : Finset ι
h : s ⊆ t
hf0 : ∀ i ∈ t, 0 ≤ f i
hf : ∀ i ∈ t, i ∉ s → f i ≤ 1
this : MulPosMono R
⊢ ∀ i ∈ s, 0 ≤ f i

Tactic:
grind

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : Preorder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
f : ι → R
s t : Finset ι
h : s ⊆ t
hf0 : ∀ i ∈ t, 0 ≤ f i
hf : ∀ i ∈ t, i ∉ s → f i ≤ 1
this : MulPosMono R
⊢ ∀ i ∈ t \ s, 0 ≤ f i

Tactic:
grind

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : Preorder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
f : ι → R
s t : Finset ι
h : s ⊆ t
hf0 : ∀ i ∈ t, 0 ≤ f i
hf : ∀ i ∈ t, i ∉ s → f i ≤ 1
this : MulPosMono R
⊢ ∀ i ∈ t \ s, f i ≤ 1

Tactic:
grind

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : Preorder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
f : ι → R
s t : Finset ι
h : s ⊆ t
hf0 : ∀ i ∈ t, 0 ≤ f i
hf : ∀ i ∈ t, i ∉ s → f i ≤ 1
⊢ ∏ i ∈ t, f i ≤ ∏ i ∈ s, f i

Tactic:
by
  have := posMulMono_iff_mulPosMono.1 ‹PosMulMono R›
  classical
  calc
    ∏ i ∈ t, f i = ∏ i ∈ t \ s ∪ s, f i := by rw [sdiff_union_of_subset h]
    _ = (∏ i ∈ t \ s, f i) * ∏ i ∈ s, f i := prod_union sdiff_disjoint
    _ ≤ ∏ i ∈ s, f i :=
      mul_le_of_le_one_left (prod_nonneg (by grind)) (prod_le_one (by grind) (by grind))

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : Preorder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
f : ι → R
hf0 : ∀ (x : ι), 0 ≤ f x
hf : ∀ (x : ι), f x ≤ 1
x✝¹ x✝ : Finset ι
hst : x✝¹ ⊆ x✝
⊢ ∀ i ∈ x✝, 0 ≤ f i

Tactic:
grind

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.List

Goal state before:
pp: case h₂
R : Type u_1
inst✝³ : CommMonoidWithZero R
inst✝² : PartialOrder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
ι : Type u_2
f g : ι → R
a : ι
s : List ι
hind : (∀ (i : ι), i ∈ s → 0 ≤ f i) → (∀ (i : ι), i ∈ s → f i ≤ g i) → (map f s).prod ≤ (map g s).prod
h0 : ∀ (i : ι), i ∈ a :: s → 0 ≤ f i
h : ∀ (i : ι), i ∈ a :: s → f i ≤ g i
this : MulPosMono R
⊢ (map f s).prod ≤ (map g s).prod

Tactic:
grind

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
inst✝ : Zero M
f : α ≃ β
l : α →₀ M
a : β
⊢ l.toFun (f.symm a) ≠ 0 ↔ l (f.symm a) ≠ 0

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
l : α →₀ M
x : α
⊢ (equivMapDomain (Equiv.refl α) l) x = l x

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
x : α →₀ M
a✝ : α
⊢ (equivMapDomain (Equiv.refl α) x) a✝ = (id x) a✝

Tactic:
rfl

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommMonoidWithZero R
inst✝² : PartialOrder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
s : Multiset R
h : ∀ (a : R), a ∈ s → 0 ≤ a
⊢ 0 ≤ s.prod

Tactic:
cases s using Quotient.ind

Goal state after:
case a
R : Type u_1
inst✝³ : CommMonoidWithZero R
inst✝² : PartialOrder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
a✝ : List R
h : ∀ (a : R), a ∈ ⟦a✝⟧ → 0 ≤ a
⊢ 0 ≤ prod ⟦a✝⟧
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
M : Type u_5
inst✝ : Zero M
f : α ≃ β
g : β ≃ γ
l : α →₀ M
x : γ
⊢ (equivMapDomain (f.trans g) l) x = (equivMapDomain g (equivMapDomain f l)) x

Tactic:
rfl

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommMonoidWithZero R
inst✝² : PartialOrder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
s : Multiset R
h : ∀ (a : R), a ∈ s → 1 ≤ a
⊢ 1 ≤ s.prod

Tactic:
cases s using Quotient.ind

Goal state after:
case a
R : Type u_1
inst✝³ : CommMonoidWithZero R
inst✝² : PartialOrder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
a✝ : List R
h : ∀ (a : R), a ∈ ⟦a✝⟧ → 1 ≤ a
⊢ 1 ≤ prod ⟦a✝⟧
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
M : Type u_5
inst✝ : Zero M
f : α ≃ β
g : β ≃ γ
x : α →₀ M
a✝ : γ
⊢ (equivMapDomain (f.trans g) x) a✝ = ((equivMapDomain g ∘ equivMapDomain f) x) a✝

Tactic:
rfl

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommMonoidWithZero R
inst✝² : PartialOrder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
ι : Type u_2
s : Multiset ι
f g : ι → R
h0 : ∀ (i : ι), i ∈ s → 0 ≤ f i
h : ∀ (i : ι), i ∈ s → f i ≤ g i
⊢ (map f s).prod ≤ (map g s).prod

Tactic:
cases s using Quotient.ind

Goal state after:
case a
R : Type u_1
inst✝³ : CommMonoidWithZero R
inst✝² : PartialOrder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
ι : Type u_2
f g : ι → R
a✝ : List ι
h0 : ∀ (i : ι), i ∈ ⟦a✝⟧ → 0 ≤ f i
h : ∀ (i : ι), i ∈ ⟦a✝⟧ → f i ≤ g i
⊢ (map f ⟦a✝⟧).prod ≤ (map g ⟦a✝⟧).prod
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✝ : Zero M
f : α ≃ β
⊢ (α →₀ M) ≃ (β →₀ M)

Tactic:
by
  refine ⟨equivMapDomain f, equivMapDomain f.symm, fun f => ?_, fun f => ?_⟩ <;> ext x <;>
    simp only [equivMapDomain_apply, Equiv.symm_symm, Equiv.symm_apply_apply,
      Equiv.apply_symm_apply]

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

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

Tactic:
cases s using Quotient.ind

Goal state after:
case a
R : Type u_1
inst✝⁴ : CommMonoidWithZero R
inst✝³ : PartialOrder R
inst✝² : ZeroLEOneClass R
inst✝¹ : PosMulStrictMono R
inst✝ : NeZero 1
a✝ : List R
h : ∀ (a : R), a ∈ ⟦a✝⟧ → 0 < a
⊢ 0 < prod ⟦a✝⟧
Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Multiset

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommMonoidWithZero R
inst✝³ : PartialOrder R
inst✝² : ZeroLEOneClass R
inst✝¹ : PosMulStrictMono R
inst✝ : NeZero 1
ι : Type u_3
s : Multiset ι
hs : s ≠ 0
f g : ι → R
h0 : ∀ (i : ι), i ∈ s → 0 < f i
h : ∀ (i : ι), i ∈ s → f i < g i
⊢ (map f s).prod < (map g s).prod

Tactic:
cases s using Quotient.ind

Goal state after:
case a
R : Type u_1
inst✝⁴ : CommMonoidWithZero R
inst✝³ : PartialOrder R
inst✝² : ZeroLEOneClass R
inst✝¹ : PosMulStrictMono R
inst✝ : NeZero 1
ι : Type u_3
f g : ι → R
a✝ : List ι
hs : ⟦a✝⟧ ≠ 0
h0 : ∀ (i : ι), i ∈ ⟦a✝⟧ → 0 < f i
h : ∀ (i : ι), i ∈ ⟦a✝⟧ → f i < g i
⊢ (map f ⟦a✝⟧).prod < (map g ⟦a✝⟧).prod
Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.List

Goal state before:
pp: case c0
R : Type u_1
inst✝⁴ : CommMonoidWithZero R
inst✝³ : PartialOrder R
inst✝² : ZeroLEOneClass R
inst✝¹ : PosMulStrictMono R
inst✝ : NeZero 1
ι : Type u_2
s✝ : List ι
f g : ι → R
a : ι
s : List ι
hs : a :: s ≠ []
h0 : ∀ (i : ι), i ∈ a :: s → 0 < f i
h : ∀ (i : ι), i ∈ a :: s → f i < g i
this : MulPosStrictMono R
⊢ ∀ (a : R), a ∈ map f s → 0 < a

Tactic:
grind

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 : α → β
hif : Set.InjOn f (f ⁻¹' ↑(support 0))
a✝ : α
⊢ (comapDomain f 0 hif) a✝ = 0 a✝

Tactic:
rfl

Goal state after:
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
hl : ↑l.support ⊆ Set.range f
⊢ mapDomain f (comapDomain f l ⋯) =
    mapDomain (⇑{ toFun := f, inj' := hf }) (comapDomain (⇑{ toFun := f, inj' := hf }) l ⋯)

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
x : α
y : M
⊢ (single x y).frange ⊆ {y}

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
f : α →₀ M
⊢ Set.range ⇑f ⊆ insert 0 ↑f.frange

Tactic:
grind

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
inst✝ : Zero M
p✝ p : α → Prop
f : α →₀ M
a : Subtype p
⊢ f ↑a ≠ 0 ↔ (⇑f ∘ Subtype.val) a ≠ 0

Tactic:
rfl

Goal state after:
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

Tactic:
rfl

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Zero γ
a : α
c : γ
val✝ : α
⊢ ((single a c).sumElim 0) (Sum.inl val✝) = (single (Sum.inl a) c) (Sum.inl val✝)

Tactic:
simp [single_apply]

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

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Zero γ
a : α
c : γ
val✝ : β
⊢ ((single a c).sumElim 0) (Sum.inr val✝) = (single (Sum.inl a) c) (Sum.inr val✝)

Tactic:
simp [single_apply]

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Zero γ
b : β
c : γ
val✝ : α
⊢ (sumElim 0 (single b c)) (Sum.inl val✝) = (single (Sum.inr b) c) (Sum.inl val✝)

Tactic:
simp [single_apply]

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

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Zero γ
b : β
c : γ
val✝ : β
⊢ (sumElim 0 (single b c)) (Sum.inr val✝) = (single (Sum.inr b) c) (Sum.inr val✝)

Tactic:
simp [single_apply]

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddMonoid M
a : α
b : β
m₁ m₂ : M
val✝ : α
⊢ ((single a m₁).sumElim (single b m₂)) (Sum.inl val✝) = (single (Sum.inl a) m₁ + single (Sum.inr b) m₂) (Sum.inl val✝)

Tactic:
simp [single_apply]

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✝ : AddMonoid M
a : α
b : β
m₁ m₂ : M
val✝ : β
⊢ ((single a m₁).sumElim (single b m₂)) (Sum.inr val✝) = (single (Sum.inl a) m₁ + single (Sum.inr b) m₂) (Sum.inr val✝)

Tactic:
simp [single_apply]

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

Goal state before:
pp: α : Type u_1
M : Type u_12
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
f : Subtype P →₀ M
⊢ ↑f.extendDomain.support ⊆ {x | P x}

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
M : Type u_12
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
f : α →₀ M
hf : ∀ a ∈ f.support, P a
a✝ : α
⊢ ¬P a✝ → 0 = f a✝

Tactic:
grind

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

Goal state before:
pp: case e'_2
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α ↪ β
x : β →₀ M
⊢ ↑x.support ⊆ Set.range ⇑f ↔ ∀ b ∉ Set.range ⇑f, x b = 0

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
M : Type u_5
inst✝ : AddCommMonoid M
v : α →₀ M
f : α ↪ β
g : β ↪ γ
⊢ embDomain (f.trans g) v = embDomain g (embDomain f v)

Tactic:
simp only [embDomain_eq_mapDomain, ← mapDomain_comp, Embedding.coe_trans]

Goal state after:
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
i : α
h : ∀ (i_1 : α), ¬x i_1 = 0 → f i_1 = f i → x i_1 = 0
⊢ x i = 0 i

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_3
R : Type u_6
inst✝¹ : Zero M
inst✝ : SMulZeroClass R M
f : α → β
r : R
v : β →₀ M
hfv : Set.InjOn f (f ⁻¹' ↑v.support)
hfrv : Set.InjOn f (f ⁻¹' ↑(r • v).support)
a✝ : α
⊢ (comapDomain f (r • v) hfrv) a✝ = (r • comapDomain f v hfv) a✝

Tactic:
rfl

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

Goal state before:
pp: α : Type u_2
s : Finset α
f : α → ℕ
h : ∑ x ∈ s, f x ≤ 1
x y : α
hsx : x ∈ s
hsy : y ∈ s
hfx : f x ≠ 0
hfy : f y ≠ 0
⊢ {x, y} ⊆ s

Tactic:
grind

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

Goal state before:
pp: case refine_1
α : Type u_2
s : Finset α
f : α → ℕ
x y : α
hsx : x ∈ s
hsy : y ∈ s
hfx : f x ≠ 0
hfy : f y ≠ 0
h : (fun s ↦ ∑ x ∈ s, f x) {x, y} ≤ 1
⊢ x = y ∧ f x = 1

Tactic:
grind

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

Goal state before:
pp: α : 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 : α
hsx : x ∈ s
hfx : f x ≠ 0
⊢ ∀ y ∈ s \ {x}, f y = 0

Tactic:
grind

Goal state after:
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:
simp_rw [Finset.sum_cons hz, Finset.sup_cons, Finset.mem_cons, Multiset.sup_eq_union,
      forall_eq_or_imp, Ne, not_true_eq_false, IsEmpty.forall_iff, true_and,
      imp_and, forall_and, ← hr, @eq_comm _ z]
    have := fun x (H : x ∈ i) => ne_of_mem_of_not_mem H hz
    simp +contextual only [this, not_false_iff, true_imp_iff]
    simp_rw [← disjoint_finsetSum_left, ← disjoint_finsetSum_right, disjoint_comm, ← and_assoc,
      and_self_iff]
    exact add_eq_union_left_of_le (Finset.sup_le fun x hx => le_sum_of_mem (mem_map_of_mem f hx))

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:
rfl

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

Goal state before:
pp: M : Type u_2
N : Type u_3
R : Type u_5
R₂ : Type u_6
inst✝⁷ : Semiring R
inst✝⁶ : Semiring R₂
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R₂ N
σ : R →+* R₂
σ_inv : R₂ →+* R
inst✝¹ : RingHomInvPair σ σ_inv
inst✝ : RingHomInvPair σ_inv σ
ι : Type u_9
κ : Type u_10
e₁ : ι ≃ κ
e₂ : M ≃ₛₗ[σ] N
x✝ : κ →₀ N
a✝ : ι
⊢ ((lcongr e₁ e₂).symm x✝) a✝ = ((lcongr e₁.symm e₂.symm) x✝) a✝

Tactic:
rfl

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
α' : Type u_7
f : α → α'
s : Set α
H : ∀ a ∈ s, ∀ b ∈ s, f a = f b → a = b
l : α →₀ M
h₁ : l ∈ ↑(supported M R s)
h₂ : (l.sum fun a ↦ single (f a)) = 0
x : α
this : DecidablePred fun x ↦ x ∈ s
xs : x ∈ s
⊢ 0 (f x) = 0

Tactic:
rfl

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

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
M' : Type u_8
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
v : α → M
v' : α' → M'
f : α → α'
g : M →ₗ[R] M'
h : ∀ (i : α), g (v i) = v' (f i)
l : α
⊢ ((linearCombination R v' ∘ₗ lmapDomain R R f) ∘ₗ lsingle l) 1 = ((g ∘ₗ linearCombination R v) ∘ₗ lsingle l) 1

Tactic:
simp [linearCombination_apply, h]

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝¹ : CommMonoid M
f : α → M
a : α
inst✝ : DecidableEq α
hf : HasFiniteMulSupport f
x : α
hx : f x ≠ 1
⊢ x ≠ a ↔ x ≠ a ∧ f x ≠ 1

Tactic:
grind

Goal state after:
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 ι
v : Basis ι R M
x✝ : M
a✝ : ι
⊢ ((ofEquivFun v.equivFun).repr x✝) a✝ = (v.repr x✝) a✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ Ioo (natAdd m i) (natAdd m j) ⊆ range (natAdd m)

Tactic:
exact Ioo_subset_Ioi_self.trans <| image_natAdd_Ioi m i ▸ image_subset_range _ _

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

Goal state before:
pp: ι : Type u_3
M : Type u_7
inst✝² : CommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedCancelMonoid M
f : ι → M
h : ∀ (i : ι), 1 ≤ f i
h' : ∃ i, 1 < f i
hf : HasFiniteMulSupport f
⊢ 1 < ∏ᶠ (i : ι), f i

Tactic:
← finprod_mem_univ

Goal state after:
ι : Type u_3
M : Type u_7
inst✝² : CommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedCancelMonoid M
f : ι → M
h : ∀ (i : ι), 1 ≤ f i
h' : ∃ i, 1 < f i
hf : HasFiniteMulSupport f
⊢ 1 < ∏ᶠ (i : ι) (_ : i ∈ univ), f i
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

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
v : α → M
f : α → α'
l : α' →₀ R
hf : InjOn f (f ⁻¹' ↑l.support)
⊢ ((comapDomain f l hf).sum fun i a ↦ a • v i) = ∑ i ∈ l.support.preimage f hf, l (f i) • v i

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝² : CommMonoid M
f g : α → M
inst✝¹ : PartialOrder M
inst✝ : MulLeftMono M
hf : HasFiniteMulSupport f
hg : HasFiniteMulSupport g
h : f ≤ g
this : Fintype ↑(mulSupport f ∪ mulSupport g)
s : Finset α := (mulSupport f ∪ mulSupport g).toFinset
⊢ mulSupport f ⊆ ↑s

Tactic:
grind

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

Goal state before:
pp: ι : Type u_10
R : Type u_11
M : Type u_12
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
f : M → ι → R
hadd : ∀ (x y : M), f (x + y) = f x + f y
hsmul : ∀ (c : R) (x : M), f (c • x) = c • f x
f_eq : ∀ (i : ι), f (b i) = ⇑(single i 1)
x : M
i : ι
f_i : M →ₗ[R] R := { toFun := fun x ↦ f x i, map_add' := ⋯, map_smul' := ⋯ }
this : lapply i ∘ₗ ↑b.repr = f_i
⊢ (b.repr x) i = (lapply i ∘ₗ ↑b.repr) x

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝² : CommMonoid M
f g : α → M
inst✝¹ : PartialOrder M
inst✝ : MulLeftMono M
hf : HasFiniteMulSupport f
hg : HasFiniteMulSupport g
h : f ≤ g
this : Fintype ↑(mulSupport f ∪ mulSupport g)
s : Finset α := (mulSupport f ∪ mulSupport g).toFinset
⊢ mulSupport g ⊆ ↑s

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
M : Type u_7
inst✝³ : CommMonoidWithZero M
inst✝² : PartialOrder M
inst✝¹ : ZeroLEOneClass M
inst✝ : PosMulMono M
f g : α → M
hf : HasFiniteMulSupport f
hf₀ : ∀ (a : α), 0 ≤ f a
hg : HasFiniteMulSupport g
h : f ≤ g
this : Fintype ↑(mulSupport f ∪ mulSupport g)
s : Finset α := (mulSupport f ∪ mulSupport g).toFinset
⊢ mulSupport f ⊆ ↑s

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
M : Type u_7
inst✝³ : CommMonoidWithZero M
inst✝² : PartialOrder M
inst✝¹ : ZeroLEOneClass M
inst✝ : PosMulMono M
f g : α → M
hf : HasFiniteMulSupport f
hf₀ : ∀ (a : α), 0 ≤ f a
hg : HasFiniteMulSupport g
h : f ≤ g
this : Fintype ↑(mulSupport f ∪ mulSupport g)
s : Finset α := (mulSupport f ∪ mulSupport g).toFinset
⊢ mulSupport g ⊆ ↑s

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_3
inst✝⁶ : Fintype α
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Semiring S
inst✝¹ : Module S M
inst✝ : SMulCommClass R S M
v : α → M
f g : α → R
⊢ ∑ i, (f + g) i • v i = ∑ x, (f x + g x) • v x

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_3
inst✝⁶ : Fintype α
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Semiring S
inst✝¹ : Module S M
inst✝ : SMulCommClass R S M
v : α → M
r : R
f : α → R
⊢ ∑ i, (r • f) i • v i = ∑ x, ((RingHom.id R) r * f x) • v x

Tactic:
rfl

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

Goal state before:
pp: ι : Type u_10
R : Type u_11
M : Type u_12
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
b : Basis ι R M
inst✝¹ : Fintype ι
inst✝ : DecidableEq M
i : ι
h : b i ∈ Finset.image (⇑b) Finset.univ
⊢ ↑(((Equiv.refl M).subtypeEquiv ⋯).symm ⟨b i, h⟩) = b i

Tactic:
rfl

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

Goal state before:
pp: case hf
α : Type u_1
M : Type u_2
R : Type u_3
inst✝³ : Fintype α
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
x✝ : α → R
x : α
a✝ : x ∈ Finset.univ
hx : x ∉ ((linearEquivFunOnFinite R R α).symm x✝).support
⊢ (fun i ↦ ⇑((fun i ↦ LinearMap.id.smulRight (v i)) i)) x (((linearEquivFunOnFinite R R α).symm x✝) x) = 0

Tactic:
rw [Finsupp.notMem_support_iff.mp hx]

Goal state after:
case hf
α : Type u_1
M : Type u_2
R : Type u_3
inst✝³ : Fintype α
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
x✝ : α → R
x : α
a✝ : x ∈ Finset.univ
hx : x ∉ ((linearEquivFunOnFinite R R α).symm x✝).support
⊢ (fun i ↦ ⇑((fun i ↦ LinearMap.id.smulRight (v i)) i)) x 0 = 0
Module: Mathlib.LinearAlgebra.Basis.Defs

Goal state before:
pp: ι : Type u_10
R : Type u_11
M : Type u_12
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
b : Basis ι R M
inst✝¹ : Fintype ι
inst✝ : DecidableEq M
i : ι
bi : M
hbi : bi ∈ Finset.image (⇑b) Finset.univ
⊢ ((b.reindexRange.reindex ((Equiv.refl M).subtypeEquiv ⋯)).repr (b i)) ⟨bi, hbi⟩ = (single ⟨b i, ⋯⟩ 1) ⟨bi, hbi⟩

Tactic:
repr_reindex,

Goal state after:
ι : Type u_10
R : Type u_11
M : Type u_12
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
b : Basis ι R M
inst✝¹ : Fintype ι
inst✝ : DecidableEq M
i : ι
bi : M
hbi : bi ∈ Finset.image (⇑b) Finset.univ
⊢ (mapDomain (⇑((Equiv.refl M).subtypeEquiv ⋯)) (b.reindexRange.repr (b i))) ⟨bi, hbi⟩ = (single ⟨b i, ⋯⟩ 1) ⟨bi, hbi⟩