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

Goal state before:
pp: R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p q r : Submodule R M
h : p ⊓ q ≤ p ⊓ r
⊢ comap p.subtype q ≤ comap p.subtype r

Tactic:
by simpa using comap_mono (f := p.subtype) h

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Pointwise

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Monoid S
inst✝¹ : DistribMulAction S M
N : Submodule R M
inst✝ : SMulCommClass S R M
a : S
p : (x : M) → x ∈ a • N → Prop
smul₀ : ∀ (s : M) (hs : s ∈ N), p (a • s) ⋯
x : M
hx : x ∈ a • N
smul₁ : ∀ (r : R) (m : M) (mem : m ∈ {a} • N), p m ⋯ → p (r • m) ⋯
add : ∀ (x y : M) (hx : x ∈ {a} • N) (hy : y ∈ {a} • N), p x ⋯ → p y ⋯ → p (x + y) ⋯
zero : p 0 ⋯
p' : (x : M) → x ∈ {a} • N → Prop := fun x hx ↦ p x ⋯
⊢ p x hx

Tactic:
refine Submodule.set_smul_inductionOn (motive := p') _ (N.singleton_set_smul a ▸ hx)
      (fun r n hr hn ↦ ?_) smul₁ add zero

Goal state after:
R : Type u_2
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Monoid S
inst✝¹ : DistribMulAction S M
N : Submodule R M
inst✝ : SMulCommClass S R M
a : S
p : (x : M) → x ∈ a • N → Prop
smul₀ : ∀ (s : M) (hs : s ∈ N), p (a • s) ⋯
x : M
hx : x ∈ a • N
smul₁ : ∀ (r : R) (m : M) (mem : m ∈ {a} • N), p m ⋯ → p (r • m) ⋯
add : ∀ (x y : M) (hx : x ∈ {a} • N) (hy : y ∈ {a} • N), p x ⋯ → p y ⋯ → p (x + y) ⋯
zero : p 0 ⋯
p' : (x : M) → x ∈ {a} • N → Prop := fun x hx ↦ p x ⋯
r : S
n : M
hr : r ∈ {a}
hn : n ∈ N
⊢ p' (r • n) ⋯
Module: Mathlib.Data.Finset.Lattice.Prod

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Finset β
t : Finset γ
f : β × γ → α
⊢ (s ×ˢ t).sup f = t.sup fun i' ↦ s.sup fun i ↦ f (i, i')

Tactic:
sup_product_left,

Goal state after:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Finset β
t : Finset γ
f : β × γ → α
⊢ (s.sup fun i ↦ t.sup fun i' ↦ f (i, i')) = t.sup fun i' ↦ s.sup fun i ↦ f (i, i')
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
p p' : Submodule R M
h : x ∈ span R (↑p ∪ ↑p')
⊢ ∃ y ∈ p, ∃ z ∈ p', y + z = 0

Tactic:
exact ⟨0, by simp, 0, by simp⟩

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

Goal state before:
pp: case a
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
S : Set (Submodule R M) := ⋯
⊢ p ≤ sSup {T | ∃ m ∈ p, m ≠ 0 ∧ T = R ∙ m}

Tactic:
intro m

Goal state after:
case a
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
S : Set (Submodule R M) := {T | ∃ m ∈ p, m ≠ 0 ∧ T = R ∙ m}
m : M
⊢ m ∈ p → m ∈ sSup {T | ∃ m ∈ p, m ≠ 0 ∧ T = R ∙ m}
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
i : ι
a✝ : i ∈ {i | t i ≠ ⊥}
j : ι
hj : t j ≠ ⊥
h : t i = t j
contra : i ≠ j
this : t j ≤ ⨆ k, ⨆ (_ : k ≠ i), t k
ht : Disjoint (t i) (t j)
⊢ t j = ⊥

Tactic:
rwa [h, disjoint_self] at ht

Goal state after:
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case mp
α : Type u
inst✝ : CompleteLattice α
k : α
H : ∀ (s : Set α), k ≤ sSup s → ∃ t, ↑t ⊆ s ∧ k ≤ t.sup id
ι : Type u
s : ι → α
hs : k ≤ iSup s
t : Finset α
ht : ↑t ⊆ range s
ht' : k ≤ t.sup id
this : ∀ (x : ↥t), ∃ i, s i = ↑x
⊢ ∃ t, k ≤ t.sup s

Tactic:
choose f hf using this

Goal state after:
case mp
α : Type u
inst✝ : CompleteLattice α
k : α
H : ∀ (s : Set α), k ≤ sSup s → ∃ t, ↑t ⊆ s ∧ k ≤ t.sup id
ι : Type u
s : ι → α
hs : k ≤ iSup s
t : Finset α
ht : ↑t ⊆ range s
ht' : k ≤ t.sup id
f : ↥t → ι
hf : ∀ (x : ↥t), s (f x) = ↑x
⊢ ∃ t, k ≤ t.sup s
Module: Mathlib.Data.FunLike.IsApply

Goal state before:
pp: F : Type u_3
α : Type u_5
β : Type u_6
inst✝³ : FunLike F α β
inst✝² : Mul F
inst✝¹ : Mul β
inst✝ : IsMulApply F α β
f g : F
⊢ ⇑(f * g) = ⇑f * ⇑g

Tactic:
by
  ext; simp

Goal state after:
Module: Mathlib.Data.FunLike.IsApply

Goal state before:
pp: F : Type u_3
α : Type u_5
β : Type u_6
inst✝³ : FunLike F α β
inst✝² : Div F
inst✝¹ : Div β
inst✝ : IsDivApply F α β
f g : F
⊢ ⇑(f / g) = ⇑f / ⇑g

Tactic:
by
  ext; simp

Goal state after:
Module: Mathlib.Data.FunLike.IsApply

Goal state before:
pp: F : Type u_3
α : Type u_5
β : Type u_6
inst✝³ : FunLike F α β
inst✝² : Inv F
inst✝¹ : Inv β
inst✝ : IsInvApply F α β
f : F
⊢ ⇑f⁻¹ = (⇑f)⁻¹

Tactic:
by
  ext; simp

Goal state after:
Module: Mathlib.Data.FunLike.IsApply

Goal state before:
pp: M : Type u_1
F : Type u_3
α : Type u_5
β : Type u_6
inst✝³ : FunLike F α β
inst✝² : SMul M F
inst✝¹ : SMul M β
inst✝ : IsSMulApply M F α β
n : M
f : F
⊢ ⇑(n • f) = n • ⇑f

Tactic:
by
  ext; simp

Goal state after:
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
b : α
⊢ sSup {c | IsCompactElement c ∧ c ≤ b} = b

Tactic:
rcases IsCompactlyGenerated.exists_sSup_eq b with ⟨s, hs, rfl⟩

Goal state after:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
s : Set α
hs : ∀ x ∈ s, IsCompactElement x
⊢ sSup {c | IsCompactElement c ∧ c ≤ sSup s} = sSup s
Module: Mathlib.Data.FunLike.IsApply

Goal state before:
pp: M : Type u_1
F : Type u_3
α : Type u_5
β : Type u_6
inst✝³ : FunLike F α β
inst✝² : Pow F M
inst✝¹ : Pow β M
inst✝ : IsPowApply M F α β
f : F
n : M
⊢ ⇑(f ^ n) = ⇑f ^ n

Tactic:
by
  ext; simp

Goal state after:
Module: Mathlib.Data.FunLike.IsApply

Goal state before:
pp: F' : Type u_4
α : Type u_5
inst✝² : FunLike F' α α
inst✝¹ : One F'
inst✝ : IsOneApplyEqSelf F' α
⊢ ⇑1 = id

Tactic:
by
  ext; simp

Goal state after:
Module: Mathlib.Data.FunLike.IsApply

Goal state before:
pp: F' : Type u_4
α : Type u_5
inst✝² : FunLike F' α α
inst✝¹ : Mul F'
inst✝ : IsMulApplyEqComp F' α
f g : F'
⊢ ⇑(f * g) = ⇑f ∘ ⇑g

Tactic:
by
  ext; simp

Goal state after:
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
α : Type u_8
inst✝² : Monoid α
inst✝¹ : DistribMulAction α M
inst✝ : SMulCommClass α R M
s : Set α
t : Set M
⊢ s • span R t = span R (s • t)

Tactic:
simp_rw [set_smul_eq_iSup, smul_span, iSup_span, Set.iUnion_smul_set]

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

Goal state before:
pp: F : Type u_8
α : Type u_9
β : Type u_10
ι : Type u_11
inst✝⁴ : FunLike F α β
inst✝³ : CommMonoid β
inst✝² : CommMonoid F
inst✝¹ : IsOneApply F α β
inst✝ : IsMulApply F α β
s : Finset ι
f : ι → F
⊢ ⇑(∏ i ∈ s, f i) = ∏ i ∈ s, ⇑(f i)

Tactic:
by
  ext; simp

Goal state after:
Module: Mathlib.Algebra.BigOperators.Ring.List

Goal state before:
pp: ι : Type u_1
κ : Type u_2
R : Type u_5
inst✝ : NonUnitalNonAssocSemiring R
f : ι → κ → R
a : R
i : ι
l₁ : List ι
j : κ
l₂ : List κ
⊢ (zipWith (fun i j ↦ a * f i j) (i :: l₁) (j :: l₂)).sum = a * (zipWith f (i :: l₁) (j :: l₂)).sum

Tactic:
by simp [sum_zipWith_distrib_left, mul_add]

Goal state after:
Module: Mathlib.Data.Multiset.Sections

Goal state before:
pp: α : Type u_1
s✝ t : Multiset (Multiset α)
a : Multiset α
s : Multiset (Multiset α)
ih : (s + t).Sections = s.Sections.bind fun m ↦ map (fun x ↦ m + x) t.Sections
⊢ (a ::ₘ s + t).Sections = (a ::ₘ s).Sections.bind fun m ↦ map (fun x ↦ m + x) t.Sections

Tactic:
by
    simp [ih, bind_assoc, map_bind, bind_map]

Goal state after:
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case refine_1
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
b c✝ : α
hbc : b ≤ c✝
h : sSup {a | a ≤ c✝ ∧ IsAtom a} = c✝
c : Set (Set α)
hc1 : c ⊆ {s | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a ∧ a ≤ c✝}
hc2 : IsChain (fun x1 x2 ↦ x1 ⊆ x2) c
⊢ Disjoint b (sSup (⋃₀ c))

Tactic:
rw [sSup_sUnion, ← sSup_image, DirectedOn.disjoint_sSup_right]
    · rintro _ ⟨s, hs, rfl⟩
      exact (hc1 hs).2.1
    · rw [directedOn_image]
      exact hc2.directedOn.mono @fun s t => sSup_le_sSup

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

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝¹ : AddCommMonoidWithOne R
p : ι → Prop
inst✝ : DecidablePred p
s : Finset ι
⊢ ↑(#({x ∈ s | p x})) = ∑ x ∈ s with p x, 1 + 0

Tactic:
add_zero,

Goal state after:
ι : Type u_1
R : Type u_4
inst✝¹ : AddCommMonoidWithOne R
p : ι → Prop
inst✝ : DecidablePred p
s : Finset ι
⊢ ↑(#({x ∈ s | p x})) = ∑ x ∈ s with p x, 1
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
p : Submodule R M
⊢ map f p = f.range ↔ Codisjoint p f.ker

Tactic:
by
  simp_rw [le_antisymm_iff, LinearMap.map_le_range, true_and, ← map_top, map_le_iff_le_comap,
    comap_map_eq, codisjoint_iff_le_sup]

Goal state after:
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: K : Type u_3
V : Type u_6
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Submodule K V
x : V
hx : x ≠ 0
⊢ Disjoint s (K ∙ x) ↔ x ∉ s

Tactic:
simp [disjoint_span_singleton, hx]

Goal state after:
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: K : Type u_3
V : Type u_6
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Submodule K V
x : V
hx : x ∉ s
⊢ Disjoint s (K ∙ x)

Tactic:
simp [disjoint_span_singleton, hx]

Goal state after:
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M
⊢ toSpanSingleton R M (x + y) = toSpanSingleton R M x + toSpanSingleton R M y

Tactic:
by
  ext; simp

Goal state after:
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_8
inst✝² : Monoid S
inst✝¹ : DistribMulAction S M
inst✝ : SMulCommClass R S M
r : S
x : M
⊢ toSpanSingleton R M (r • x) = r • toSpanSingleton R M x

Tactic:
by
  ext; simp

Goal state after:
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: R : Type u_1
M : Type u_4
M₂ : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M →ₗ[R] M₂
x : M
⊢ f ∘ₗ toSpanSingleton R M x = toSpanSingleton R M₂ (f x)

Tactic:
by
  ext; simp

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

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝ : CommSemiring R
a b : R
s : Finset ι
⊢ ∑ t ∈ s.powerset, a ^ #t * b ^ (#s - #t) = (a + b) ^ #s

Tactic:
← prod_const,

Goal state after:
ι : Type u_1
R : Type u_4
inst✝ : CommSemiring R
a b : R
s : Finset ι
⊢ ∑ t ∈ s.powerset, a ^ #t * b ^ (#s - #t) = ∏ _x ∈ s, (a + b)
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✝² : Zero M
inst✝¹ : Zero N
inst✝ : Zero O
f : ZeroHom N O
f₂ : ZeroHom M N
⊢ zeroHom (f.comp f₂) = (zeroHom f).comp (zeroHom f₂)

Tactic:
by
  ext; simp

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : AddZeroClass M
a : ι
b : M
f : ι →₀ M
ha : a ∉ f.support
hb : b ≠ 0
H : (single a b).support = {a}
⊢ (single a b + f).support = cons a f.support ha

Tactic:
support_add_eq,

Goal state after:
ι : Type u_1
M : Type u_3
inst✝ : AddZeroClass M
a : ι
b : M
f : ι →₀ M
ha : a ∉ f.support
hb : b ≠ 0
H : (single a b).support = {a}
⊢ (single a b).support ∪ f.support = cons a f.support ha

ι : Type u_1
M : Type u_3
inst✝ : AddZeroClass M
a : ι
b : M
f : ι →₀ M
ha : a ∉ f.support
hb : b ≠ 0
H : (single a b).support = {a}
⊢ Disjoint (single a b).support f.support
Module: Mathlib.Algebra.Group.Finsupp

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : AddZeroClass M
a : ι
b : M
f : ι →₀ M
ha : a ∉ f.support
hb : b ≠ 0
H : (single a b).support = {a}
⊢ (f + single a b).support = cons a f.support ha

Tactic:
support_add_eq,

Goal state after:
ι : Type u_1
M : Type u_3
inst✝ : AddZeroClass M
a : ι
b : M
f : ι →₀ M
ha : a ∉ f.support
hb : b ≠ 0
H : (single a b).support = {a}
⊢ f.support ∪ (single a b).support = cons a f.support ha

ι : Type u_1
M : Type u_3
inst✝ : AddZeroClass M
a : ι
b : M
f : ι →₀ M
ha : a ∉ f.support
hb : b ≠ 0
H : (single a b).support = {a}
⊢ Disjoint f.support (single a b).support
Module: Mathlib.Algebra.Group.Finsupp

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : DecidableEq ι
f₁ f₂ : ι
g₁ g₂ : M
H : f₁ ≠ f₂
hg₁ : g₁ ≠ 0
hg₂ : g₂ ≠ 0
⊢ (single f₁ g₁ + single f₂ g₂).support = {f₁, f₂}

Tactic:
support_add_eq,

Goal state after:
ι : Type u_1
M : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : DecidableEq ι
f₁ f₂ : ι
g₁ g₂ : M
H : f₁ ≠ f₂
hg₁ : g₁ ≠ 0
hg₂ : g₂ ≠ 0
⊢ (single f₁ g₁).support ∪ (single f₂ g₂).support = {f₁, f₂}

ι : Type u_1
M : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : DecidableEq ι
f₁ f₂ : ι
g₁ g₂ : M
H : f₁ ≠ f₂
hg₁ : g₁ ≠ 0
hg₂ : g₂ ≠ 0
⊢ Disjoint (single f₁ g₁).support (single f₂ g₂).support
Module: Mathlib.Data.Finsupp.Single

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α ↪ β
a : α
m : M
⊢ embDomain f (single a m) = single (f a) m

Tactic:
classical
    ext b
    by_cases h : b ∈ Set.range f <;> grind

Goal state after:
Module: Mathlib.Algebra.Order.Group.Indicator

Goal state before:
pp: case pos
α : 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
a : α
ha : a ∈ ⋃ i, s i
⊢ (⋃ i, s i).mulIndicator (⨆ i, f i) a ≤ (⨆ i, (s i).mulIndicator (f i)) a

Tactic:
obtain ⟨i, hi⟩ : ∃ i, a ∈ s i := by simpa using ha
    rw [mulIndicator_of_mem ha, iSup_apply, iSup_apply]
    refine iSup_le fun j ↦ ?_
    obtain ⟨k, hik, hjk⟩ := exists_ge_ge i j
    refine le_iSup_of_le k <| (hf hjk _).trans_eq ?_
    rw [mulIndicator_of_mem (hs hik hi)]

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

Goal state before:
pp: case neg
M : Type u_3
M₂ : Type u_4
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₂
F : Type u_5
inst✝⁵ : FunLike F M M₂
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst✝³ : DivisionSemiring R
inst✝² : DivisionSemiring S
inst✝¹ : Module R M
inst✝ : Module S M₂
n : ℕ
hR : ↑n = 0
hS : ¬↑n = 0
x : M
⊢ f x = 0

Tactic:
← inv_smul_smul₀ hS (f x),

Goal state after:
case neg
M : Type u_3
M₂ : Type u_4
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₂
F : Type u_5
inst✝⁵ : FunLike F M M₂
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst✝³ : DivisionSemiring R
inst✝² : DivisionSemiring S
inst✝¹ : Module R M
inst✝ : Module S M₂
n : ℕ
hR : ↑n = 0
hS : ¬↑n = 0
x : M
⊢ (↑n)⁻¹ • ↑n • f x = 0
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
  simp only [HasFiniteMulSupport] at hf ⊢
  refine (Set.finite_iUnion hf).subset fun i hi ↦ ?_
  simp only [mem_mulSupport, Set.mem_iUnion] at hi ⊢
  exact ne_iff.mp hi

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:
by
  cases s using Quotient.ind
  simp only [quot_mk_to_coe, mem_coe, prod_coe] at *
  apply List.prod_nonneg h

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

Goal state before:
pp: case h₂.h0
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
⊢ ∀ (i : ι), i ∈ s → 0 ≤ f i

Tactic:
intro i hi
        apply le_of_lt
        apply h0
        simp [hi]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α ↪ β
l : α →₀ M
⊢ comapDomain (⇑f) (embDomain f l) ⋯ = l

Tactic:
by
  ext; simp

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

Tactic:
rw [eq_single_iff, comapDomain_apply, comapDomain_support, ← Finset.coe_subset, coe_preimage,
      support_single _ hm, coe_singleton, coe_singleton, single_eq_same]
    rw [support_single _ hm, coe_singleton] at hif
    exact ⟨fun x hx => hif hx rfl hx, rfl⟩

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : CommMonoid α
inst✝² : AddCommMonoid β
inst✝¹ : Preorder β
inst✝ : AddLeftMono β
s : Finset ι
f : ι → α
g : α → β
h_one : g 1 ≤ 0
h_mul : ∀ (a b : α), g (a * b) ≤ g a + g b
⊢ (Multiset.map g (Multiset.map (fun x ↦ f x) s.val)).sum = ∑ x ∈ s, g (f x)

Tactic:
Multiset.map_map,

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : CommMonoid α
inst✝² : AddCommMonoid β
inst✝¹ : Preorder β
inst✝ : AddLeftMono β
s : Finset ι
f : ι → α
g : α → β
h_one : g 1 ≤ 0
h_mul : ∀ (a b : α), g (a * b) ≤ g a + g b
⊢ (Multiset.map (g ∘ fun x ↦ f x) s.val).sum = ∑ x ∈ s, g (f x)
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Zero γ
f : α →₀ γ
g : β →₀ γ
⊢ comapDomain Sum.inl (f.sumElim g) ⋯ = f

Tactic:
by
  ext; simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Zero γ
f : α →₀ γ
g : β →₀ γ
⊢ comapDomain Sum.inr (f.sumElim g) ⋯ = g

Tactic:
by
  ext; simp

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 γ
inst✝ : AddMonoid M
α : Type u_12
β : Type u_13
⊢ ∀ (x y : α ⊕ β →₀ M),
    sumFinsuppEquivProdFinsupp.toFun (x + y) = sumFinsuppEquivProdFinsupp.toFun x + sumFinsuppEquivProdFinsupp.toFun y

Tactic:
by
      intros
      ext <;>
        simp only [Equiv.toFun_as_coe, Prod.fst_add, Prod.snd_add, add_apply,
          snd_sumFinsuppEquivProdFinsupp, fst_sumFinsuppEquivProdFinsupp]

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

Goal state before:

Tactic:
_ = ∑ i ∈ s, 2 * r i * (∑ j ∈ s, g j) * (∑ j ∈ s, r j) := by
          simp_rw [mul_assoc, ← mul_sum, ← sum_mul]; ring
      _ ≤ ∑ i ∈ s, (f i * (∑ j ∈ s, g j) ^ 2 + g i * (∑ j ∈ s, r j) ^ 2) := by
          gcongr with i hi
          have ht : (r i * (∑ j ∈ s, g j) * (∑ j ∈ s, r j)) ^ 2 ≤
              (f i * (∑ j ∈ s, g j) ^ 2) * (g i * (∑ j ∈ s, r j) ^ 2) := by
            grw [mul_mul_mul_comm, ← mul_pow, mul_assoc, mul_pow, ht i hi]
            exact sq_nonneg _
          refine le_of_eq_of_le ?_ (two_mul_le_add_of_sq_le_mul
            (mul_nonneg (hf i hi) (sq_nonneg _)) (mul_nonneg (hg i hi) (sq_nonneg _)) ht)
          repeat rw [mul_assoc]
      _ = _ := by simp_rw [sum_add_distrib, ← sum_mul]; ring

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

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

Tactic:
simp only [Multiset.map_map, Function.comp_apply]

Goal state after:
Module: Mathlib.Data.Finset.Fin

Goal state before:
pp: n : ℕ
s : Finset ℕ
h : ∀ m ∈ s, m < n
⊢ ↑(s.attachFin h) = Fin.val ⁻¹' ↑s

Tactic:
by
  ext; simp

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
hf : (mulSupport f).Infinite
⊢ ∏ᶠ (i : α), f i = 1

Tactic:
rw [finprod_def]
  simp only [HasFiniteMulSupport]
  rw [dif_neg hf]

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

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

Tactic:
HasFiniteSupport,

Goal state after:
case inl
α : Type u_1
R : Type u_7
inst✝ : NonAssocSemiring R
f : α → R
h : ∑ᶠ (i : α), f i = 1
h✝ : Subsingleton R
⊢ (support f).Finite
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n m : ℕ
i : Fin n
⊢ natAdd m ⁻¹' Ici (natAdd m i) = Ici i

Tactic:
by
  ext; simp

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
v : α → M
s : Set α
x : M
hx : ∃ x_1 ∈ s, v x_1 = x
i : α
hi : i ∈ s ∧ v i = x
⊢ (linearCombination R v) (single i 1) = x

Tactic:
by simp [hi.2]

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

Goal state before:
pp: n m : ℕ
i : Fin n
⊢ natAdd m ⁻¹' Ioi (natAdd m i) = Ioi i

Tactic:
by
  ext; simp

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

Goal state before:
pp: n m : ℕ
i : Fin n
⊢ natAdd m ⁻¹' Iic (natAdd m i) = Iic i

Tactic:
by
  ext; simp

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

Goal state before:
pp: n m : ℕ
i : Fin n
⊢ natAdd m ⁻¹' Iio (natAdd m i) = Iio i

Tactic:
by
  ext; simp

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

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ natAdd m ⁻¹' Icc (natAdd m i) (natAdd m j) = Icc i j

Tactic:
by
  ext; simp

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

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ natAdd m ⁻¹' Ico (natAdd m i) (natAdd m j) = Ico i j

Tactic:
by
  ext; simp

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

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ natAdd m ⁻¹' Ioc (natAdd m i) (natAdd m j) = Ioc i j

Tactic:
by
  ext; simp

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

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ natAdd m ⁻¹' Ioo (natAdd m i) (natAdd m j) = Ioo i j

Tactic:
by
  ext; simp

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

Goal state before:
pp: case refine_2
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set α
t : Finset α
h : s ∩ mulSupport f = ↑t ∩ mulSupport f
x : α
hxf : x ∈ mulSupport f
hx : x ∈ t
⊢ x ∈ s

Tactic:
refine ((mem_inter_iff x s (mulSupport f)).mp ?_).1

Goal state after:
case refine_2
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set α
t : Finset α
h : s ∩ mulSupport f = ↑t ∩ mulSupport f
x : α
hxf : x ∈ mulSupport f
hx : x ∈ t
⊢ x ∈ s ∩ mulSupport f
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n m : ℕ
i : Fin n
⊢ (fun x ↦ x.addNat m) ⁻¹' Ici (i.addNat m) = Ici i

Tactic:
by
  ext; simp

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

Goal state before:
pp: n m : ℕ
i : Fin n
⊢ (fun x ↦ x.addNat m) ⁻¹' Ioi (i.addNat m) = Ioi i

Tactic:
by
  ext; simp

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

Goal state before:
pp: n m : ℕ
i : Fin n
⊢ (fun x ↦ x.addNat m) ⁻¹' Iic (i.addNat m) = Iic i

Tactic:
by
  ext; simp

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

Goal state before:
pp: n m : ℕ
i : Fin n
⊢ (fun x ↦ x.addNat m) ⁻¹' Iio (i.addNat m) = Iio i

Tactic:
by
  ext; simp

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

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ (fun x ↦ x.addNat m) ⁻¹' Icc (i.addNat m) (j.addNat m) = Icc i j

Tactic:
by
  ext; simp

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

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ (fun x ↦ x.addNat m) ⁻¹' Ico (i.addNat m) (j.addNat m) = Ico i j

Tactic:
by
  ext; simp

Goal state after: