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

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : LinearOrder ι
motive : (ι →₀ M) → Prop
f : ι →₀ M
zero : motive 0
single_add : ∀ (a : ι) (b : M) (f : ι →₀ M), (∀ c ∈ f.support, c < a) → b ≠ 0 → motive f → motive (single a b + f)
⊢ motive f

Tactic:
by
  suffices ∀ (s) (f : ι →₀ M), f.support = s → motive f from this _ _ rfl
  refine fun s => s.induction_on_max (fun f h => ?_) (fun a s hm hf f hs => ?_)
  · rwa [support_eq_empty.1 h]
  · have hs' : (erase a f).support = s := by
      rw [support_erase, hs, erase_insert (fun ha => (hm a ha).false)]
    rw [← single_add_erase a f]
    refine single_add _ _ _ (fun c hc => hm _ <| hs'.symm ▸ hc) ?_ (hf _ hs')
    rw [← mem_support_iff, hs]
    exact mem_insert_self a s

Goal state after:
Module: Mathlib.Algebra.Group.Finsupp

Goal state before:
pp: ι : Type u_1
M : Type u_3
N : Type u_4
O : Type u_5
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
inst✝ : AddCommMonoid O
f : N →+ O
g : M →+ N
x✝ : ι →₀ M
a✝ : ι
⊢ ((addMonoidHom (f.comp g)) x✝) a✝ = (((addMonoidHom f).comp (addMonoidHom g)) x✝) a✝

Tactic:
;

Goal state after:
ι : Type u_1
M : Type u_3
N : Type u_4
O : Type u_5
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
inst✝ : AddCommMonoid O
f : N →+ O
g : M →+ N
x✝ : ι →₀ M
a✝ : ι
⊢ ((addMonoidHom (f.comp g)) x✝) a✝ = (((addMonoidHom f).comp (addMonoidHom g)) x✝) a✝
Module: Mathlib.Algebra.Group.Finsupp

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : AddCommMonoid M
x✝ : ι →₀ M
a✝ : ι
⊢ ((addEquiv (AddEquiv.refl M)) x✝) a✝ = ((AddEquiv.refl (ι →₀ M)) x✝) a✝

Tactic:
;

Goal state after:
ι : Type u_1
M : Type u_3
inst✝ : AddCommMonoid M
x✝ : ι →₀ M
a✝ : ι
⊢ ((addEquiv (AddEquiv.refl M)) x✝) a✝ = ((AddEquiv.refl (ι →₀ M)) x✝) a✝
Module: Mathlib.Algebra.Group.Finsupp

Goal state before:
pp: ι : Type u_1
M : Type u_3
N : Type u_4
O : Type u_5
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
inst✝ : AddCommMonoid O
e₁ : M ≃+ N
e₂ : N ≃+ O
x✝ : ι →₀ M
a✝ : ι
⊢ ((addEquiv (e₁.trans e₂)) x✝) a✝ = (((addEquiv e₁).trans (addEquiv e₂)) x✝) a✝

Tactic:
;

Goal state after:
ι : Type u_1
M : Type u_3
N : Type u_4
O : Type u_5
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
inst✝ : AddCommMonoid O
e₁ : M ≃+ N
e₂ : N ≃+ O
x✝ : ι →₀ M
a✝ : ι
⊢ ((addEquiv (e₁.trans e₂)) x✝) a✝ = (((addEquiv e₁).trans (addEquiv e₂)) x✝) a✝
Module: Mathlib.Data.Finsupp.Option

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
a✝ : α
⊢ (embDomain Embedding.some f).some a✝ = f a✝

Tactic:
;

Goal state after:
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
a✝ : α
⊢ (embDomain Embedding.some f).some a✝ = f a✝
Module: Mathlib.Data.Finsupp.Option

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
a✝ : α
⊢ (embDomain Embedding.some f) (Option.some a✝) = f a✝

Tactic:
;

Goal state after:
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
a✝ : α
⊢ (embDomain Embedding.some f) (Option.some a✝) = f a✝
Module: Mathlib.Algebra.Order.Group.Indicator

Goal state before:
pp: case hf
α : Type u_2
M : Type u_3
inst✝³ : CompleteLattice M
inst✝² : One M
ι : Type u_4
inst✝¹ : Preorder ι
inst✝ : IsDirectedOrder ι
f : ι → α → M
s : ι → Set α
h1 : ⊥ = 1
hf : Monotone f
hs : Monotone s
i : ι
i✝ : α
⊢ 1 i✝ ≤ f i i✝

Tactic:
;

Goal state after:
case hf
α : Type u_2
M : Type u_3
inst✝³ : CompleteLattice M
inst✝² : One M
ι : Type u_4
inst✝¹ : Preorder ι
inst✝ : IsDirectedOrder ι
f : ι → α → M
s : ι → Set α
h1 : ⊥ = 1
hf : Monotone f
hs : Monotone s
i : ι
i✝ : α
⊢ 1 i✝ ≤ f i i✝
Module: Mathlib.Algebra.GroupWithZero.Indicator

Goal state before:
pp: ι : Type u_1
M₀ : Type u_4
inst✝ : MulZeroOneClass M₀
s t : Set ι
x✝ : ι
⊢ (s ∩ t).indicator 1 x✝ = (s ∩ t).indicator (fun j ↦ 1) x✝

Tactic:
;

Goal state after:
ι : Type u_1
M₀ : Type u_4
inst✝ : MulZeroOneClass M₀
s t : Set ι
x✝ : ι
⊢ (s ∩ t).indicator 1 x✝ = (s ∩ t).indicator (fun j ↦ 1) x✝
Module: Mathlib.Algebra.GroupWithZero.Indicator

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M₀ : Type u_4
inst✝ : MulZeroOneClass M₀
s : Set ι
i : ι
t : Set κ
j : κ
⊢ (if i ∈ s ∧ j ∈ t then 1 (i, j) else 0) = (if i ∈ s then 1 i else 0) * if j ∈ t then 1 j else 0

Tactic:
split_ifs with h₀ <;> simp only [Pi.one_apply, mul_one, mul_zero]

Goal state after:
case neg
ι : Type u_1
κ : Type u_2
M₀ : Type u_4
inst✝ : MulZeroOneClass M₀
s : Set ι
i : ι
t : Set κ
j : κ
h₀ : i ∈ s ∧ j ∈ t
h✝¹ : i ∈ s
h✝ : ¬j ∈ t
⊢ 1 = 0

case pos
ι : Type u_1
κ : Type u_2
M₀ : Type u_4
inst✝ : MulZeroOneClass M₀
s : Set ι
i : ι
t : Set κ
j : κ
h₀ : i ∈ s ∧ j ∈ t
h✝¹ : ¬i ∈ s
h✝ : j ∈ t
⊢ 1 = 0

case neg
ι : Type u_1
κ : Type u_2
M₀ : Type u_4
inst✝ : MulZeroOneClass M₀
s : Set ι
i : ι
t : Set κ
j : κ
h₀ : i ∈ s ∧ j ∈ t
h✝¹ : ¬i ∈ s
h✝ : ¬j ∈ t
⊢ 1 = 0

case pos
ι : Type u_1
κ : Type u_2
M₀ : Type u_4
inst✝ : MulZeroOneClass M₀
s : Set ι
i : ι
t : Set κ
j : κ
h₀ : ¬(i ∈ s ∧ j ∈ t)
h✝¹ : i ∈ s
h✝ : j ∈ t
⊢ 0 = 1
Module: Mathlib.Algebra.GroupWithZero.Indicator

Goal state before:
pp: ι : Type u_1
M₀ : Type u_4
inst✝¹ : MulZeroOneClass M₀
s t : Set ι
inst✝ : Nontrivial M₀
h : s.indicator 1 = t.indicator 1
x✝ : ι
⊢ x✝ ∈ s ↔ x✝ ∈ t

Tactic:
;

Goal state after:
ι : Type u_1
M₀ : Type u_4
inst✝¹ : MulZeroOneClass M₀
s t : Set ι
inst✝ : Nontrivial M₀
h : s.indicator 1 = t.indicator 1
x✝ : ι
⊢ x✝ ∈ s ↔ x✝ ∈ t
Module: Mathlib.Algebra.GroupWithZero.Indicator

Goal state before:
pp: ι : Type u_1
M₀ : Type u_4
inst✝¹ : MonoidWithZero M₀
inst✝ : IsReduced M₀
n : ℕ
f : ι → M₀
hn : n ≠ 0
x✝ : ι
⊢ (x✝ ∈ support fun a ↦ f a ^ n) ↔ x✝ ∈ support f

Tactic:
;

Goal state after:
ι : Type u_1
M₀ : Type u_4
inst✝¹ : MonoidWithZero M₀
inst✝ : IsReduced M₀
n : ℕ
f : ι → M₀
hn : n ≠ 0
x✝ : ι
⊢ (x✝ ∈ support fun a ↦ f a ^ n) ↔ x✝ ∈ support f
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
inst✝⁴ : AddCommMonoid A
inst✝³ : AddCommMonoid B
inst✝² : AddCommMonoid C
t : ι → A → C
s : Finset α
f : α → ι →₀ A
i : ι
g : ι →₀ A
k : ι → A → γ → B
x : γ
β : Type u_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst✝¹ : AddZeroClass M
inst✝ : AddCommMonoid N
F : α → M →+ N
x✝¹ : α
x✝ : M
⊢ ((fun F x ↦ F.comp (singleAddHom x))
        ((fun F ↦ { toFun := fun f ↦ f.sum fun x ↦ ⇑(F x), map_zero' := ⋯, map_add' := ⋯ }) F) x✝¹)
      x✝ =
    (F x✝¹) x✝

Tactic:
;

Goal state after:
α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
inst✝⁴ : AddCommMonoid A
inst✝³ : AddCommMonoid B
inst✝² : AddCommMonoid C
t : ι → A → C
s : Finset α
f : α → ι →₀ A
i : ι
g : ι →₀ A
k : ι → A → γ → B
x : γ
β : Type u_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst✝¹ : AddZeroClass M
inst✝ : AddCommMonoid N
F : α → M →+ N
x✝¹ : α
x✝ : M
⊢ ((fun F x ↦ F.comp (singleAddHom x))
        ((fun F ↦ { toFun := fun f ↦ f.sum fun x ↦ ⇑(F x), map_zero' := ⋯, map_add' := ⋯ }) F) x✝¹)
      x✝ =
    (F x✝¹) x✝
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
inst✝⁴ : AddCommMonoid A
inst✝³ : AddCommMonoid B
inst✝² : AddCommMonoid C
t : ι → A → C
s : Finset α
f : α → ι →₀ A
i : ι
g : ι →₀ A
k : ι → A → γ → B
x : γ
β : Type u_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst✝¹ : AddZeroClass M
inst✝ : AddCommMonoid N
F : (α →₀ M) →+ N
x✝¹ : α
x✝ : M
⊢ (((fun F ↦ { toFun := fun f ↦ f.sum fun x ↦ ⇑(F x), map_zero' := ⋯, map_add' := ⋯ })
            ((fun F x ↦ F.comp (singleAddHom x)) F)).comp
        (singleAddHom x✝¹))
      x✝ =
    (F.comp (singleAddHom x✝¹)) x✝

Tactic:
;

Goal state after:
α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
inst✝⁴ : AddCommMonoid A
inst✝³ : AddCommMonoid B
inst✝² : AddCommMonoid C
t : ι → A → C
s : Finset α
f : α → ι →₀ A
i : ι
g : ι →₀ A
k : ι → A → γ → B
x : γ
β : Type u_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst✝¹ : AddZeroClass M
inst✝ : AddCommMonoid N
F : (α →₀ M) →+ N
x✝¹ : α
x✝ : M
⊢ (((fun F ↦ { toFun := fun f ↦ f.sum fun x ↦ ⇑(F x), map_zero' := ⋯, map_add' := ⋯ })
            ((fun F x ↦ F.comp (singleAddHom x)) F)).comp
        (singleAddHom x✝¹))
      x✝ =
    (F.comp (singleAddHom x✝¹)) x✝
Module: Mathlib.Data.Finsupp.Option

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : AddZeroClass M
a b : α →₀ M
i j : M
x : Option α
⊢ (optionElim (i + j) (a + b)) x = (optionElim i a + optionElim j b) x

Tactic:
;

Goal state after:
α : Type u_1
M : Type u_2
inst✝ : AddZeroClass M
a b : α →₀ M
i j : M
x : Option α
⊢ (optionElim (i + j) (a + b)) x = (optionElim i a + optionElim j b) x
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
inst✝⁴ : AddCommMonoid A
inst✝³ : AddCommMonoid B
inst✝² : AddCommMonoid C
t : ι → A → C
s : Finset α
f : α → ι →₀ A
i : ι
g : ι →₀ A
k : ι → A → γ → B
x : γ
β : Type u_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G✝ : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst✝¹ : AddZeroClass M
inst✝ : AddCommMonoid N
F G : α → M →+ N
x✝¹ : α
x✝ : M
⊢ ({ toFun := fun f ↦ f.sum fun x ↦ ⇑((F + G) x), map_zero' := ⋯, map_add' := ⋯ }.comp (singleAddHom x✝¹)) x✝ =
    (({ toFun := fun f ↦ f.sum fun x ↦ ⇑(F x), map_zero' := ⋯, map_add' := ⋯ } +
            { toFun := fun f ↦ f.sum fun x ↦ ⇑(G x), map_zero' := ⋯, map_add' := ⋯ }).comp
        (singleAddHom x✝¹))
      x✝

Tactic:
;

Goal state after:
α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
inst✝⁴ : AddCommMonoid A
inst✝³ : AddCommMonoid B
inst✝² : AddCommMonoid C
t : ι → A → C
s : Finset α
f : α → ι →₀ A
i : ι
g : ι →₀ A
k : ι → A → γ → B
x : γ
β : Type u_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G✝ : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst✝¹ : AddZeroClass M
inst✝ : AddCommMonoid N
F G : α → M →+ N
x✝¹ : α
x✝ : M
⊢ ({ toFun := fun f ↦ f.sum fun x ↦ ⇑((F + G) x), map_zero' := ⋯, map_add' := ⋯ }.comp (singleAddHom x✝¹)) x✝ =
    (({ toFun := fun f ↦ f.sum fun x ↦ ⇑(F x), map_zero' := ⋯, map_add' := ⋯ } +
            { toFun := fun f ↦ f.sum fun x ↦ ⇑(G x), map_zero' := ⋯, map_add' := ⋯ }).comp
        (singleAddHom x✝¹))
      x✝
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 : (mulSupport f).Finite
hg : (mulSupport g).Finite
⊢ (mulSupport fun a ↦ (f a, g a)).Finite

Tactic:
mulSupport_prodMk f g

Goal state after:
α : Type u_1
M : Type u_2
inst✝¹ : One M
M' : Type u_3
inst✝ : One M'
f : α → M
g : α → M'
hf : (mulSupport f).Finite
hg : (mulSupport g).Finite
⊢ (mulSupport f ∪ mulSupport g).Finite
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:
prod_cons,

Goal state after:
α : 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
⊢ (g a).prod h * ∏ x ∈ s, (g x).prod h = (∑ i ∈ cons a s has, g i).prod h
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 ∉ support g
⊢ a ∉ mulSupport fun a ↦ f a ^ g a

Tactic:
;

Goal state after:
α : Type u_1
M : Type u_4
inst✝ : Monoid M
f : α → M
g : α → ℕ
hg : HasFiniteSupport g
a : α
ha : a ∉ support g
⊢ a ∉ mulSupport fun a ↦ f a ^ g a
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:
;

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 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
Module: Mathlib.Algebra.Order.AbsoluteValue.Basic

Goal state before:
pp: case pos
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

pp: case neg
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

Tactic:
;

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

case neg
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
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 (b - a)

Tactic:
;

Goal state after:
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 (b - a)
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

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

Tactic:
;

Goal state after:
f : ℕ →₀ ℕ
nhf : 0 ∉ f.support
hf : 0 ∈ f.support
⊢ False
Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset

Goal state before:
pp: case cons
α : Type u_2
inst✝² : CommMonoid α
inst✝¹ : Preorder α
s t : Multiset α
inst✝ : MulLeftMono α
a✝¹ b✝ : α
as✝ bs✝ : Multiset α
rh : a✝¹ ≤ b✝
a✝ : Rel (fun x1 x2 ↦ x1 ≤ x2) as✝ bs✝
rt : as✝.prod ≤ bs✝.prod
⊢ (a✝¹ ::ₘ as✝).prod ≤ (b✝ ::ₘ bs✝).prod

Tactic:
prod_cons,

Goal state after:
case cons
α : Type u_2
inst✝² : CommMonoid α
inst✝¹ : Preorder α
s t : Multiset α
inst✝ : MulLeftMono α
a✝¹ b✝ : α
as✝ bs✝ : Multiset α
rh : a✝¹ ≤ b✝
a✝ : Rel (fun x1 x2 ↦ x1 ≤ x2) as✝ bs✝
rt : as✝.prod ≤ bs✝.prod
⊢ a✝¹ * as✝.prod ≤ (b✝ ::ₘ bs✝).prod
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:
simpa using hs_nonempty

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:
simpa using hs_nonempty

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

Goal state before:
pp: case mp
α : Type u_1
M : Type u_5
inst✝ : Zero M
a : α
m : M
f : α →₀ M
⊢ (∃ a_1, f a_1 ≠ 0 ∧ { toFun := fun a ↦ (a, f a), inj' := ⋯ } a_1 = (a, m)) → f a = m ∧ m ≠ 0

Tactic:
rintro ⟨b, ha, rfl, -⟩

Goal state after:
case mp
α : Type u_1
M : Type u_5
inst✝ : Zero M
a : α
f : α →₀ M
ha : f a ≠ 0
⊢ f a = f a ∧ f a ≠ 0
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:
;

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

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : Zero M
l : α →₀ M
x : α
⊢ (equivMapDomain (Equiv.refl α) l) x = l x
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:
;

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : Zero M
x : α →₀ M
a✝ : α
⊢ (equivMapDomain (Equiv.refl α) x) a✝ = (id x) 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:
;

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

Goal state after:
α : 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✝
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α ≃ β
a✝ : β
⊢ (equivMapDomain f 0) a✝ = 0 a✝

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α ≃ β
a✝ : β
⊢ (equivMapDomain f 0) a✝ = 0 a✝
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
x : α →₀ M
a : β
h : a ∉ Set.range f
⊢ a ∉ Set.range f

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
x : α →₀ M
a : β
h : a ∉ Set.range f
⊢ a ∉ Set.range f
Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.List

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_2
s : List ι
hs : s ≠ []
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:
match s with
  | [] => contradiction
  | a :: s =>
    simp only [map_cons, prod_cons]
    have := posMulStrictMono_iff_mulPosStrictMono.1 ‹PosMulStrictMono R›
    apply mul_lt_mul
    · apply h
      simp
    · apply prod_map_le_prod_map₀
      · intro i hi
        apply le_of_lt
        apply h0
        simp [hi]
      · intro i hi
        apply le_of_lt
        apply h
        simp [hi]
    · apply prod_pos
      grind
    · apply le_of_lt ((h0 _ _).trans (h _ _)) <;> simp

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 : α → β
x : α →₀ M
b : β
h : b ∉ Set.range f
⊢ (mapDomain f x) b = 0

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
x : α →₀ M
b : β
h : b ∉ Set.range f
⊢ (mapDomain f x) b = 0
Module: Mathlib.Algebra.Order.BigOperators.Ring.Multiset

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : CommMonoidWithZero β
inst✝¹ : PartialOrder β
inst✝ : PosMulMono β
f : α → β
p : α → Prop
h0 : ∀ (a : α), 0 ≤ f a
h_one : f 1 ≤ 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)
a : α
s : Multiset α
hs : (∀ (a : α), a ∈ s → p a) → f s.prod ≤ (map f s).prod
hpsa : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → p a_1
hs0 : ¬s = ∅
hps : ∀ (x : α), x ∈ s → p x
hp_prod : p s.prod
⊢ f (a ::ₘ s).prod ≤ (map f (a ::ₘ s)).prod

Tactic:
prod_cons,

Goal state after:
case neg
α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : CommMonoidWithZero β
inst✝¹ : PartialOrder β
inst✝ : PosMulMono β
f : α → β
p : α → Prop
h0 : ∀ (a : α), 0 ≤ f a
h_one : f 1 ≤ 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)
a : α
s : Multiset α
hs : (∀ (a : α), a ∈ s → p a) → f s.prod ≤ (map f s).prod
hpsa : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → p a_1
hs0 : ¬s = ∅
hps : ∀ (x : α), x ∈ s → p x
hp_prod : p s.prod
⊢ f (a * s.prod) ≤ (map f (a ::ₘ s)).prod