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

Goal state before:
pp: α : Type u_1
R : Type u_2
inst✝ : MulZeroOneClass R
s : Set α
r : R
a : α
⊢ r • s.indicator 1 a = s.indicator (fun x ↦ r) a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_8
inst✝¹ : Fintype α
inst✝ : AddCommMonoid M
f : α →₀ M
⊢ ∑ a, single a (f a) = f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_8
inst✝¹ : AddCommMonoid M
inst✝ : Fintype α
i : α
m : M
⊢ ∑ j, (single i m) j = m

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_8
inst✝¹ : AddCommMonoid M
inst✝ : Fintype α
i : α
m : M
⊢ ∑ x, Pi.single x m i = m

Tactic:
classical rw [Finset.sum_pi_single]

Goal state after:
α : Type u_1
M : Type u_8
inst✝¹ : AddCommMonoid M
inst✝ : Fintype α
i : α
m : M
⊢ (if i ∈ univ then m else 0) = m
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_8
inst✝¹ : AddCommMonoid M
inst✝ : Fintype α
i : α
m : M
⊢ ∑ j, (single j m) i = m

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: ι : Type u_2
A : Type u_4
B : Type u_5
inst✝¹ : AddCommMonoid A
inst✝ : AddCommMonoid B
f₁ f₂ : ι
g₁ g₂ : A
F : ι → A → B
H : f₁ ≠ f₂
HF : ∀ (f : ι), F f 0 = 0
⊢ (single f₁ g₁ + single f₂ g₂).sum F = F f₁ g₁ + F f₂ g₂

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_8
inst✝¹ : Fintype α
inst✝ : AddCommMonoid M
f : α → M
⊢ ((equivFunOnFinite.symm f).sum fun x n ↦ n) = ∑ a, f a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_8
N : Type u_10
P : Type u_11
inst✝² : AddZeroClass M
inst✝¹ : AddCommMonoid N
inst✝ : AddCommMonoid P
g : N →+ P
f : α → M →+ N
a : α
⊢ liftAddHom.symm (g.comp (liftAddHom f)) a = g.comp (f a)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.FiniteSupport.Basic

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : One M
⊢ HasFiniteMulSupport 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_7
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
v : α →₀ M
f : α ↪ β
g : β → M → N
⊢ (embDomain f v).prod g = v.prod fun a b ↦ g (f a) b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.FiniteSupport.Basic

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝¹ : One M
M' : Type u_3
inst✝ : One M'
f : α → M
g : α → M'
hf : HasFiniteMulSupport f
hg : HasFiniteMulSupport g
⊢ HasFiniteMulSupport fun a ↦ (f a, g a)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.FiniteSupport.Basic

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝¹ : One M
ι : Type u_3
inst✝ : Finite α
f : ι → α → M
hf : ∀ (a : α), HasFiniteMulSupport fun x ↦ f x a
⊢ HasFiniteMulSupport f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.FiniteSupport.Basic

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝¹ : One M
inst✝ : SemilatticeSup M
ι : Type u_3
f : ι → α → M
s : Finset ι
hf : ∀ i ∈ s, HasFiniteMulSupport (f i)
hs : s.Nonempty
⊢ HasFiniteMulSupport fun a ↦ s.sup' hs fun x ↦ f x a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
ι : Type u_2
M : Type u_8
N : Type u_10
inst✝¹ : AddCommMonoid M
inst✝ : CommMonoid N
s✝ : Finset ι
g : ι → α →₀ M
h : α → M → N
h_zero : ∀ (a : α), h a 0 = 1
h_add : ∀ (a : α) (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ * h a b₂
a : ι
s : Finset ι
has : a ∉ s
ih : ∏ i ∈ s, (g i).prod h = (∑ i ∈ s, g i).prod h
⊢ ∏ i ∈ cons a s has, (g i).prod h = (∑ i ∈ cons a s has, g i).prod h

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.FiniteSupport.Basic

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝¹ : One M
inst✝ : SemilatticeInf M
ι : Type u_3
f : ι → α → M
s : Finset ι
hf : ∀ i ∈ s, HasFiniteMulSupport (f i)
hs : s.Nonempty
⊢ HasFiniteMulSupport fun a ↦ s.inf' hs fun x ↦ f x a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.FiniteSupport.Basic

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : One M
β : Type u_3
f : β → M
g : α → β
hg : Injective g
hf : HasFiniteMulSupport f
⊢ HasFiniteMulSupport (f ∘ g)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.FiniteSupport.Basic

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝¹ : One M
β : Type u_3
f : β → M
g : α → β
inst✝ : One β
hfg : HasFiniteMulSupport (f ∘ g)
h : f 1 = 1
hf : Injective f
⊢ HasFiniteMulSupport g

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.FiniteSupport.Basic

Goal state before:
pp: α : Type u_1
M : Type u_4
inst✝ : Monoid M
f : α → M
g : α → ℕ
hg : HasFiniteSupport g
a : α
ha : a ∈ mulSupport fun a ↦ f a ^ g a
⊢ a ∈ support g

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.FiniteSupport.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
⊢ (Function.support fun x ↦ count x s) ⊆ ↑s.toFinset

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid N
f : Multiset (α →₀ M)
h : α → M → N
h₀ : ∀ (a : α), h a 0 = 0
h₁ : ∀ (a : α) (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ + h a b₂
a : α →₀ M
s : Multiset (α →₀ M)
ih : s.sum.sum h = (Multiset.map (fun g ↦ g.sum h) s).sum
⊢ (a ::ₘ s).sum.sum h = (Multiset.map (fun g ↦ g.sum h) (a ::ₘ s)).sum

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.AbsoluteValue.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
R✝ : Type u_3
S✝ : Type u_4
R : Type u_5
S : Type u_6
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : PartialOrder S
abv g : AbsoluteValue R S
toFun✝ : R → S
map_mul'✝ : ∀ (x y : R), toFun✝ (x * y) = toFun✝ x * toFun✝ y
nonneg'✝ : ∀ (x : R), 0 ≤ { toFun := toFun✝, map_mul' := map_mul'✝ }.toFun x
eq_zero'✝ : ∀ (x : R), { toFun := toFun✝, map_mul' := map_mul'✝ }.toFun x = 0 ↔ x = 0
add_le'✝ :
  ∀ (x y : R),
    { toFun := toFun✝, map_mul' := map_mul'✝ }.toFun (x + y) ≤
      { toFun := toFun✝, map_mul' := map_mul'✝ }.toFun x + { toFun := toFun✝, map_mul' := map_mul'✝ }.toFun y
h :
  (fun f ↦ f.toFun)
      { toFun := toFun✝, map_mul' := map_mul'✝, nonneg' := nonneg'✝, eq_zero' := eq_zero'✝, add_le' := add_le'✝ } =
    (fun f ↦ f.toFun) g
⊢ { toFun := toFun✝, map_mul' := map_mul'✝, nonneg' := nonneg'✝, eq_zero' := eq_zero'✝, add_le' := add_le'✝ } = g

Tactic:
obtain ⟨⟨_, _⟩, _⟩ := g

Goal state after:
ι : Type u_1
α : Type u_2
R✝ : Type u_3
S✝ : Type u_4
R : Type u_5
S : Type u_6
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : PartialOrder S
abv : AbsoluteValue R S
toFun✝¹ : R → S
map_mul'✝¹ : ∀ (x y : R), toFun✝¹ (x * y) = toFun✝¹ x * toFun✝¹ y
nonneg'✝¹ : ∀ (x : R), 0 ≤ { toFun := toFun✝¹, map_mul' := map_mul'✝¹ }.toFun x
eq_zero'✝¹ : ∀ (x : R), { toFun := toFun✝¹, map_mul' := map_mul'✝¹ }.toFun x = 0 ↔ x = 0
add_le'✝¹ :
  ∀ (x y : R),
    { toFun := toFun✝¹, map_mul' := map_mul'✝¹ }.toFun (x + y) ≤
      { toFun := toFun✝¹, map_mul' := map_mul'✝¹ }.toFun x + { toFun := toFun✝¹, map_mul' := map_mul'✝¹ }.toFun y
toFun✝ : R → S
map_mul'✝ : ∀ (x y : R), toFun✝ (x * y) = toFun✝ x * toFun✝ y
nonneg'✝ : ∀ (x : R), 0 ≤ { toFun := toFun✝, map_mul' := map_mul'✝ }.toFun x
eq_zero'✝ : ∀ (x : R), { toFun := toFun✝, map_mul' := map_mul'✝ }.toFun x = 0 ↔ x = 0
add_le'✝ :
  ∀ (x y : R),
    { toFun := toFun✝, map_mul' := map_mul'✝ }.toFun (x + y) ≤
      { toFun := toFun✝, map_mul' := map_mul'✝ }.toFun x + { toFun := toFun✝, map_mul' := map_mul'✝ }.toFun y
h :
  (fun f ↦ f.toFun)
      { toFun := toFun✝¹, map_mul' := map_mul'✝¹, nonneg' := nonneg'✝¹, eq_zero' := eq_zero'✝¹, add_le' := add_le'✝¹ } =
    (fun f ↦ f.toFun)
      { toFun := toFun✝, map_mul' := map_mul'✝, nonneg' := nonneg'✝, eq_zero' := eq_zero'✝, add_le' := add_le'✝ }
⊢ { toFun := toFun✝¹, map_mul' := map_mul'✝¹, nonneg' := nonneg'✝¹, eq_zero' := eq_zero'✝¹, add_le' := add_le'✝¹ } =
    { toFun := toFun✝, map_mul' := map_mul'✝, nonneg' := nonneg'✝, eq_zero' := eq_zero'✝, add_le' := add_le'✝ }
Module: Mathlib.Algebra.Order.AbsoluteValue.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
R✝ : Type u_3
S✝ : Type u_4
R : Type u_5
S : Type u_6
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : PartialOrder S
abv f g : AbsoluteValue R S
h : (fun f ↦ f.toFun) f = (fun f ↦ f.toFun) g
⊢ f = g

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.AbsoluteValue.Basic

Goal state before:
pp: R : Type u_5
S : Type u_6
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : PartialOrder S
abv : AbsoluteValue R S
inst✝ : AddLeftMono S
l : List R
⊢ abv l.sum ≤ (List.map (⇑abv) l).sum

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.AbsoluteValue.Basic

Goal state before:
pp: R : Type u_5
S : Type u_6
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : PartialOrder S
abv : AbsoluteValue R S
x : R
⊢ abv x ≤ 0 ↔ x = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.AbsoluteValue.Basic

Goal state before:
pp: R : Type u_5
S : Type u_6
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : PartialOrder S
abv : AbsoluteValue R S
h : IsLeftRegular (abv 1)
⊢ (fun x ↦ abv 1 * x) (abv 1) = (fun x ↦ abv 1 * x) 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.AbsoluteValue.Basic

Goal state before:
pp: R : Type u_5
S : Type u_6
inst✝² : Ring R
inst✝¹ : Semiring S
inst✝ : PartialOrder S
abv : AbsoluteValue R S
a b c : R
⊢ abv (a - c) ≤ abv (a - b) + abv (b - c)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_16
ι : Type u_17
M : Type u_18
inst✝¹ : DecidableEq α
inst✝ : AddCommMonoid M
g : ι → α →₀ M
s : Finset ι
h : ∀ (i₁ i₂ : ι), i₁ ≠ i₂ → Disjoint (g i₁).support (g i₂).support
⊢ (∑ i ∈ s, g i).support = s.biUnion fun i ↦ (g i).support

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_8
inst✝¹ : AddCommMonoid M
f1 f2 : α →₀ M
hd✝ : Disjoint f1.support f2.support
β : Type u_16
inst✝ : CommMonoid β
g : α → M → β
f1✝ f2✝ : α →₀ M
hd : Disjoint f1✝.support f2✝.support
x : α
hx : x ∈ f1✝.support
⊢ g x (f1✝ x + f2✝ x) = g x (f1✝ x)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.AbsoluteValue.Basic

Goal state before:
pp: R : Type u_5
S : Type u_6
inst✝⁴ : Semiring R
inst✝³ : Semiring S
inst✝² : PartialOrder S
abv : AbsoluteValue R S
inst✝¹ : IsDomain S
inst✝ : IsOrderedRing S
n : ℕ
⊢ abv ↑n ≤ ↑n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.AbsoluteValue.Basic

Goal state before:
pp: R : Type u_5
S : Type u_6
inst✝³ : Ring R
inst✝² : Ring S
inst✝¹ : PartialOrder S
inst✝ : IsOrderedRing S
abv : AbsoluteValue R S
a b : R
⊢ abv a ≤ abv (a - b) + abv b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.AbsoluteValue.Basic

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝⁴ : CommRing S
inst✝³ : PartialOrder S
inst✝² : IsOrderedRing S
inst✝¹ : Ring R
abv : AbsoluteValue R S
inst✝ : NoZeroDivisors S
a : R
ha : ¬a = 0
⊢ abv (-a) * abv (-a) = abv a * abv a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.AbsoluteValue.Basic

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝⁴ : CommRing S
inst✝³ : PartialOrder S
inst✝² : IsOrderedRing S
inst✝¹ : Ring R
abv : AbsoluteValue R S
inst✝ : NoZeroDivisors S
a : R
⊢ abv (-a) = abv a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.AbsoluteValue.Basic

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝⁴ : CommRing S
inst✝³ : PartialOrder S
inst✝² : IsOrderedRing S
inst✝¹ : Ring R
abv : AbsoluteValue R S
inst✝ : NoZeroDivisors S
a b : R
⊢ abv (a - b) = abv (b - a)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_8
inst✝¹ : AddCommMonoid M
f1 f2 : α →₀ M
hd : Disjoint f1.support f2.support
β : Type u_16
inst✝ : CommMonoid β
g : α → M → β
⊢ (f1 + f2).prod g = f1.prod g * f2.prod g

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.AbsoluteValue.Basic

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝⁴ : CommRing S
inst✝³ : PartialOrder S
inst✝² : IsOrderedRing S
inst✝¹ : Ring R
abv : AbsoluteValue R S
inst✝ : NoZeroDivisors S
a b : R
⊢ abv a - abv b ≤ abv (a + b)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.AbsoluteValue.Basic

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝⁴ : CommRing S
inst✝³ : PartialOrder S
inst✝² : IsOrderedRing S
inst✝¹ : Ring R
abv : AbsoluteValue R S
inst✝ : NoZeroDivisors S
a b : R
⊢ abv (a - b) ≤ abv a + abv b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.AbsoluteValue.Basic

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝⁴ : CommRing S
inst✝³ : PartialOrder S
inst✝² : IsOrderedRing S
inst✝¹ : Ring R
abv : AbsoluteValue R S
inst✝ : NoZeroDivisors S
x : ℤ
⊢ abv ↑x.natAbs = abv ↑x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.AbsoluteValue.Basic

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝⁴ : CommRing S
inst✝³ : PartialOrder S
inst✝² : IsOrderedRing S
inst✝¹ : Ring R
inst✝ : NoZeroDivisors S
f g : AbsoluteValue R S
⊢ (∀ (n : ℕ), f ↑n = g ↑n) ↔ ∀ (n : ℤ), f ↑n = g ↑n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.AbsoluteValue.Basic

Goal state before:
pp: R : Type u_5
S : Type u_6
inst✝³ : Ring R
inst✝² : CommRing S
inst✝¹ : LinearOrder S
inst✝ : IsStrictOrderedRing S
abv : AbsoluteValue R S
a b : R
⊢ abv b - abv a ≤ abv (a - b)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.AbsoluteValue.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
R✝ : Type u_3
S✝ : Type u_4
R : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : DecidablePred fun x ↦ x = 0
inst✝⁴ : NoZeroDivisors R
S : Type u_6
inst✝³ : Semiring S
inst✝² : PartialOrder S
inst✝¹ : IsOrderedRing S
inst✝ : Nontrivial S
x y : R
⊢ (if x * y = 0 then 0 else 1) = (if x = 0 then 0 else 1) * if y = 0 then 0 else 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
f1 f2 : α →₀ M
g1 g2 : α → M → N
h1 : f1.support ⊆ f2.support
h2 : ∀ a ∈ f1.support, g1 a (f1 a) ∣ g2 a (f2 a)
⊢ f1.prod g1 ∣ f2.prod g2

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.AbsoluteValue.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
R✝ : Type u_3
S✝ : Type u_4
R : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : DecidablePred fun x ↦ x = 0
inst✝⁴ : NoZeroDivisors R
S : Type u_6
inst✝³ : Semiring S
inst✝² : PartialOrder S
inst✝¹ : IsOrderedRing S
inst✝ : Nontrivial S
x : R
⊢ 0 ≤ if x = 0 then 0 else 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.AbsoluteValue.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
R✝ : Type u_3
S✝ : Type u_4
R : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : DecidablePred fun x ↦ x = 0
inst✝⁴ : NoZeroDivisors R
S : Type u_6
inst✝³ : Semiring S
inst✝² : PartialOrder S
inst✝¹ : IsOrderedRing S
inst✝ : Nontrivial S
x : R
⊢ (if x = 0 then 0 else 1) = 0 ↔ x = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.AbsoluteValue.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
R✝ : Type u_3
S✝ : Type u_4
R : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : DecidablePred fun x ↦ x = 0
inst✝⁴ : NoZeroDivisors R
S : Type u_6
inst✝³ : Semiring S
inst✝² : PartialOrder S
inst✝¹ : IsOrderedRing S
inst✝ : Nontrivial S
x y : R
⊢ (if x + y = 0 then 0 else 1) ≤ (if x = 0 then 0 else 1) + if y = 0 then 0 else 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_8
inst✝ : AddCommMonoid M
s : Finset α
f : (a : α) → a ∈ s → M
⊢ indicator s f = ∑ x ∈ s.attach, single (↑x) (f ↑x ⋯)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.AbsoluteValue.Basic

Goal state before:
pp: R : Type u_5
inst✝⁶ : Semiring R
S : Type u_6
inst✝⁵ : Semiring S
inst✝⁴ : PartialOrder S
inst✝³ : IsOrderedRing S
inst✝² : DecidablePred fun x ↦ x = 0
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial S
v : AbsoluteValue R S
⊢ v.IsNontrivial ↔ v ≠ AbsoluteValue.trivial

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.AbsoluteValue.Basic

Goal state before:
pp: R : Type u_5
inst✝² : Semiring R
S : Type u_6
inst✝¹ : Semiring S
inst✝ : PartialOrder S
v : AbsoluteValue R S
⊢ ¬v.IsNontrivial ↔ ∀ (x : R), x ≠ 0 → v x = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.AbsoluteValue.Basic

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝⁴ : Field R
inst✝³ : Semifield S
inst✝² : LinearOrder S
inst✝¹ : IsStrictOrderedRing S
inst✝ : ExistsAddOfLE S
v : AbsoluteValue R S
h : v.IsNontrivial
⊢ ∃ x, 1 < v x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
s : Finset α
f : (a : α) → a ∈ s → M
h : α → M → N
h_zero : ∀ a ∈ s, h a 0 = 1
⊢ (indicator s f).prod h = ∏ x ∈ s.attach, h (↑x) (f ↑x ⋯)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
s : Finset α
f : α → M
h : α → M → N
h_zero : ∀ a ∈ s, h a 0 = 1
⊢ (indicator s fun x x_1 ↦ f x).prod h = ∏ x ∈ s, h x (f x)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
f : α →₀ M
g : α → M → N
n₁ n₂ : N
a : α
ha : a ∈ f.support
h : g a (f a) * n₁ = g a (f a) * n₂
⊢ f.prod g * n₁ = f.prod g * n₂

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.AbsoluteValue.Basic

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝⁴ : Field R
inst✝³ : Semifield S
inst✝² : LinearOrder S
inst✝¹ : IsStrictOrderedRing S
inst✝ : ExistsAddOfLE S
v : AbsoluteValue R S
h : v.IsNontrivial
⊢ ∃ x, x ≠ 0 ∧ v x < 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.AbsoluteValue.Basic

Goal state before:
pp: S : Type u_5
inst✝³ : Ring S
inst✝² : PartialOrder S
R : Type u_6
inst✝¹ : Ring R
abv : R → S
inst✝ : IsAbsoluteValue abv
a b c : R
⊢ abv (a - c) ≤ abv (a - b) + abv (b - c)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: ι : 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
⊢ (g.sum k) x = g.sum fun i a ↦ (k i a) x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
R : Type u_14
S : Type u_15
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
b : S
s : α →₀ R
f : α → R → S
⊢ s.sum f * b = s.sum fun a c ↦ f a c * b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
R : Type u_14
S : Type u_15
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
b : S
s : α →₀ R
f : α → R → S
⊢ b * s.sum f = s.sum fun a c ↦ b * f a c

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: f : ℕ →₀ ℕ
nhf : 0 ∉ f.support
x✝ : ℕ
hf : x✝ ∈ f.support
H : x✝ = 0
⊢ False

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝² : CommMonoid α
inst✝¹ : Preorder α
s : Multiset α
inst✝ : MulLeftMono α
l : List α
hl : ∀ (x : α), x ∈ ⟦l⟧ → 1 ≤ x
⊢ 1 ≤ prod ⟦l⟧

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝² : CommMonoid α
inst✝¹ : Preorder α
s : Multiset α
inst✝ : IsOrderedMonoid α
l : List α
hl : ∀ (x : α), x ∈ ⟦l⟧ → 1 ≤ x
x : α
hx : x ∈ ⟦l⟧
⊢ x ≤ prod ⟦l⟧

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝² : CommMonoid α
inst✝¹ : Preorder α
inst✝ : MulLeftMono α
s : Multiset α
n : α
h : ∀ (x : α), x ∈ s → x ≤ n
⊢ s.prod ≤ n ^ s.card

Tactic:
by

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

Goal state before:
pp: α : Type u_4
inst✝² : CommMonoid α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
s : Multiset α
⊢ ∀ (a : List α), (∀ (x : α), x ∈ ⟦a⟧ → 1 ≤ x) → prod ⟦a⟧ = 1 → ∀ (x : α), x ∈ ⟦a⟧ → x = 1

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝² : CommMonoid α
inst✝¹ : Preorder α
s t : Multiset α
inst✝ : MulLeftMono α
h : Rel (fun x1 x2 ↦ x1 ≤ x2) s t
⊢ s.prod ≤ t.prod

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝² : CommMonoid α
inst✝¹ : Preorder α
s : Multiset α
a : α
inst✝ : MulLeftMono α
h : ∀ (x : α), x ∈ s → a ≤ x
⊢ a ^ s.card ≤ s.prod

Tactic:
by

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : CommMonoid α
inst✝² : CommMonoid β
inst✝¹ : Preorder β
inst✝ : IsOrderedMonoid β
f : α → β
p : α → Prop
h_one : f 1 ≤ 1
hp_one : p 1
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
l : List α
hps : ∀ (a : α), a ∈ ⟦l⟧ → p a
⊢ ∀ (a : α), a ∈ l → p a

Tactic:
by

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : CommMonoid α
inst✝² : CommMonoid β
inst✝¹ : Preorder β
inst✝ : IsOrderedMonoid β
f : α → β
p : α → Prop
h_one : f 1 ≤ 1
hp_one : p 1
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
s : Multiset α
hps : ∀ (a : α), a ∈ s → p a
⊢ f s.prod ≤ (map f s).prod

Tactic:
by

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : CommMonoid α
inst✝² : CommMonoid β
inst✝¹ : Preorder β
inst✝ : IsOrderedMonoid β
f : α → β
h_one : f 1 ≤ 1
h_mul : ∀ (a b : α), f (a * b) ≤ f a * f b
s : Multiset α
⊢ f s.prod ≤ (map f s).prod

Tactic:
by

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : CommMonoid α
inst✝² : CommMonoid β
inst✝¹ : Preorder β
inst✝ : IsOrderedMonoid β
f : α → β
p : α → Prop
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
l : List α
hs_nonempty : ⟦l⟧ ≠ ∅
hs : ∀ (a : α), a ∈ ⟦l⟧ → p a
⊢ l ≠ []

Tactic:
by

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : CommMonoid α
inst✝² : CommMonoid β
inst✝¹ : Preorder β
inst✝ : IsOrderedMonoid β
f : α → β
p : α → Prop
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
l : List α
hs_nonempty : ⟦l⟧ ≠ ∅
hs : ∀ (a : α), a ∈ ⟦l⟧ → p a
⊢ ∀ (a : α), a ∈ l → p a

Tactic:
by

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : CommMonoid α
inst✝² : CommMonoid β
inst✝¹ : Preorder β
inst✝ : IsOrderedMonoid β
f : α → β
p : α → Prop
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
s : Multiset α
hs_nonempty : s ≠ ∅
hs : ∀ (a : α), a ∈ s → p a
⊢ f s.prod ≤ (map f s).prod

Tactic:
by

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : CommMonoid α
inst✝² : CommMonoid β
inst✝¹ : Preorder β
inst✝ : IsOrderedMonoid β
f : α → β
h_mul : ∀ (a b : α), f (a * b) ≤ f a * f b
l : List α
hs_nonempty : ⟦l⟧ ≠ ∅
⊢ l ≠ ∅

Tactic:
by

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : CommMonoid α
inst✝² : CommMonoid β
inst✝¹ : Preorder β
inst✝ : IsOrderedMonoid β
f : α → β
h_mul : ∀ (a b : α), f (a * b) ≤ f a * f b
s : Multiset α
hs_nonempty : s ≠ ∅
⊢ f s.prod ≤ (map f s).prod

Tactic:
by

Goal state after: