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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst✝⁵ : Ring R
inst✝⁴ : Ring R₂
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
p : Submodule R M
⊢ (∀ x ∈ p, f x = 0 → x = 0) ↔ Set.InjOn ⇑f ↑p

Tactic:
Set.injOn_iff_map_eq_zero

Goal state after:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst✝⁵ : Ring R
inst✝⁴ : Ring R₂
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
p : Submodule R M
⊢ (∀ x ∈ p, f x = 0 → x = 0) ↔ ∀ a ∈ p, f a = 0 → a = 0
Module: Mathlib.Algebra.Group.Subsemigroup.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : Mul M
inst✝ : Mul N
s : Subsemigroup N
x : M × N
⊢ x ∈ ⊤.prod s ↔ x ∈ comap (MulHom.snd M N) s

Tactic:
by simp [mem_prod, MulHom.coe_snd]

Goal state after:
Module: Mathlib.Algebra.Group.Subsemigroup.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
g : N →ₙ* P
f : M →ₙ* N
⊢ map g f.srange = (g.comp f).srange

Tactic:
simpa only [srange_eq_map] using (⊤ : Subsemigroup M).map_map g f

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

Goal state before:
pp: R : Type u
inst✝ : NonAssocSemiring R
M : Submonoid R
x✝ : R
⊢ x✝ ∈ M.subsemiringClosure ↔ x✝ ∈ Subsemiring.closure ↑M

Tactic:
refine
    ⟨fun hx => ?_, fun hx =>
      (Subsemiring.mem_closure.mp hx) M.subsemiringClosure fun s sM => ?_⟩
  <;> rintro - ⟨H1, rfl⟩

Goal state after:
case refine_1
R : Type u
inst✝ : NonAssocSemiring R
M : Submonoid R
x✝ : R
hx : x✝ ∈ M.subsemiringClosure
H1 : Subsemiring R
⊢ x✝ ∈ (fun t ↦ ⋂ (_ : t ∈ {S | ↑M ⊆ ↑S}), ↑t) H1

case refine_2
R : Type u
inst✝ : NonAssocSemiring R
M : Submonoid R
x✝ : R
hx : x✝ ∈ Subsemiring.closure ↑M
s : R
sM : s ∈ ↑M
H1 : AddSubmonoid R
⊢ s ∈ (fun t ↦ ⋂ (_ : t ∈ {S | ↑M ⊆ ↑S}), ↑t) H1
Module: Mathlib.RingTheory.NonUnitalSubring.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : NonUnitalNonAssocRing R
inst✝ : NonUnitalNonAssocRing S
f : R →ₙ+* S
⊢ ↑f.range = ↑⊤ ↔ Set.range ⇑f = Set.univ

Tactic:
rw [coe_range, coe_top]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Algebra R A
inst✝¹ : IsDomain R
inst✝ : IsDomain A
⊢ FaithfulSMul R A ↔ Injective ⇑(algebraMap R A)

Tactic:
faithfulSMul_iff_algebraMap_injective

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Algebra R A
inst✝¹ : IsDomain R
inst✝ : IsDomain A
⊢ Injective ⇑(algebraMap R A) ↔ Injective ⇑(algebraMap R A)
Module: Mathlib.Algebra.Prime.Defs

Goal state before:
pp: case succ
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
hp : Prime p
a : M
n : ℕ
ih : p ∣ a ^ n → p ∣ a
h : p ∣ a ^ (n + 1)
⊢ p ∣ a

Tactic:
rw [pow_succ'] at h

Goal state after:
case succ
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
hp : Prime p
a : M
n : ℕ
ih : p ∣ a ^ n → p ∣ a
h : p ∣ a * a ^ n
⊢ p ∣ a
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : NonAssocRing R
inst✝ : NonAssocRing S
f : R →+* S
⊢ ↑f.range = ↑⊤ ↔ Set.range ⇑f = Set.univ

Tactic:
rw [coe_range, coe_top]

Goal state after:
Module: Mathlib.Algebra.Group.Irreducible.Lemmas

Goal state before:
pp: case refine_1
M : Type u_2
inst✝ : Monoid M
y : M
u : Mˣ
x✝ : ¬IsUnit y
h : ∀ ⦃a b : M⦄, ↑u * y = a * b → IsUnit a ∨ IsUnit b
A B : M
HAB : y = A * B
⊢ ↑u * y = ↑u * A * B

Tactic:
rw [mul_assoc, ← HAB]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
x : M
u v : Mˣ
⊢ x * ↑(u * v) = x * ↑u * ↑v

Tactic:
Units.val_mul,

Goal state after:
M : Type u_1
inst✝ : Monoid M
x : M
u v : Mˣ
⊢ x * (↑u * ↑v) = x * ↑u * ↑v
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: case succ
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p : M
hp : Prime p
n : ℕ
ih : ∀ {q : M}, q ∣ p ^ n ↔ ∃ i, i ≤ n ∧ q ~ᵤ p ^ i
q : M
h : q ∣ p ^ (n + 1)
⊢ ∃ i, i ≤ n + 1 ∧ q ~ᵤ p ^ i

Tactic:
rw [pow_succ'] at h

Goal state after:
case succ
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p : M
hp : Prime p
n : ℕ
ih : ∀ {q : M}, q ∣ p ^ n ↔ ∃ i, i ≤ n ∧ q ~ᵤ p ^ i
q : M
h : q ∣ p * p ^ n
⊢ ∃ i, i ≤ n + 1 ∧ q ~ᵤ p ^ i
Module: Mathlib.Algebra.Algebra.Equiv

Goal state before:
pp: R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e : A₁ ≃ₐ[R] A₂
e₁ : A₁ ≃ₐ[R] A₁'
e₂ : A₂ ≃ₐ[R] A₂'
f : A₁' →ₐ[R] A₂'
⊢ (fun f ↦ ((↑e₂).comp f).comp ↑e₁.symm) ((fun f ↦ ((↑e₂.symm).comp f).comp ↑e₁) f) = f

Tactic:
by
    simp only [AlgHom.comp_assoc, comp_symm]
    simp only [← AlgHom.comp_assoc, comp_symm, AlgHom.id_comp, AlgHom.comp_id]

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
module_M : Module R M
module_M₂ : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
f : M →ₛₗ[σ₁₂] M₂
inst✝¹ : RingHomInvPair σ₁₂ σ₂₁
inst✝ : RingHomInvPair σ₂₁ σ₁₂
h : Injective ⇑f
x : ↥f.range
⊢ f ((ofInjective f h).symm x) = ↑x

Tactic:
obtain ⟨-, ⟨y, rfl⟩⟩ := x
  have : ⟨f y, LinearMap.mem_range_self f y⟩ = LinearEquiv.ofInjective f h y := rfl
  simp [this]

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Prod

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

Tactic:
by
  rw [sup'_product_left, Finset.sup'_comm]

Goal state after:
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : IsModularLattice α
a b c : α
inst✝¹ : BoundedOrder α
inst✝ : ComplementedLattice α
x✝ : ↑(Ici a)
x : α
hx : x ∈ Ici a
⊢ ∃ b, IsCompl ⟨x, hx⟩ b

Tactic:
simp_rw [Set.Ici.isCompl_iff]
    obtain ⟨y, rfl, hcodisjoint⟩ := exists_inf_eq_and_codisjoint hx
    exact ⟨⟨y, inf_le_right⟩, rfl, hcodisjoint⟩

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

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

Tactic:
Set.mem_add

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p p' : Submodule R M
x✝ : M
⊢ (∃ y ∈ p, ∃ z ∈ p', y + z = x✝) ↔ ∃ x ∈ ↑p, ∃ y ∈ ↑p', x + y = x✝
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
s : Set α
⊢ (∃ x, sᶜ = {x}) ↔ ∃ x, s = {x}ᶜ

Tactic:
@eq_comm _ s,

Goal state after:
α : Type u_2
s : Set α
⊢ (∃ x, sᶜ = {x}) ↔ ∃ x, {x}ᶜ = s
Module: Mathlib.Algebra.Algebra.Tower

Goal state before:
pp: R✝ : Type u
S✝ : Type v
A : Type w
B : Type u₁
M✝ : Type v₁
inst✝¹³ : CommSemiring R✝
inst✝¹² : Semiring A
inst✝¹¹ : Algebra R✝ A
inst✝¹⁰ : AddCommMonoid M✝
inst✝⁹ : Module R✝ M✝
inst✝⁸ : Module A M✝
inst✝⁷ : IsScalarTower R✝ A M✝
R : Type u_1
S : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Ring S
inst✝⁴ : AddCommGroup M
inst✝³ : Algebra R S
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
h : Function.Surjective ⇑(algebraMap R S)
N : Submodule R M
⊢ ∀ (c : S) {x : M}, x ∈ N.carrier → c • x ∈ N.carrier

Tactic:
simpa [h.forall] using N.2

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

Goal state before:
pp: ι : Sort u_1
α : Type u_2
inst✝¹ : CompleteLattice α
f : ι → α
inst✝ : IsCompactlyGenerated α
a : α
h : Directed (fun x1 x2 ↦ x1 ≤ x2) f
⊢ sSup (range fun i ↦ f i) ⊓ a = ⨆ i, f i ⊓ a

Tactic:
h.directedOn_range.sSup_inf_eq,

Goal state after:
ι : Sort u_1
α : Type u_2
inst✝¹ : CompleteLattice α
f : ι → α
inst✝ : IsCompactlyGenerated α
a : α
h : Directed (fun x1 x2 ↦ x1 ≤ x2) f
⊢ ⨆ b ∈ range f, b ⊓ a = ⨆ i, f i ⊓ a
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
s : Set (Set α)
hs : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) s
h : ∀ a ∈ s, sSupIndep a
⊢ ∀ (i : ↑s), sSupIndep ↑i

Tactic:
simpa using h

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

Goal state before:
pp: I : Type u_7
inst✝³ : DecidableEq I
M : I → Type u_8
inst✝² : (i : I) → CommMonoid (M i)
inst✝¹ : Finite I
N : Type u_9
inst✝ : CommMonoid N
g h : ((i : I) → M i) →* N
H : ∀ (i : I) (x : M i), g (Pi.mulSingle i x) = h (Pi.mulSingle i x)
⊢ g = h

Tactic:
cases nonempty_fintype I
  ext k
  rw [← Finset.univ_prod_mulSingle k, map_prod, map_prod]
  simp only [H]

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

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝ : CommSemiring R
s : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h1 : g i + h i = f i
h2 : ∀ j ∈ s, j ≠ i → g j = f j
h3 : ∀ j ∈ s, j ≠ i → h j = f j
⊢ ∏ i ∈ s, g i + ∏ i ∈ s, h i = ∏ i ∈ s, f i

Tactic:
by
  classical
    simp_rw [prod_eq_mul_prod_sdiff_singleton_of_mem hi, ← h1, right_distrib]
    congr 2 <;> apply prod_congr rfl <;> simpa

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

Goal state before:
pp: α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
b c : α
hbc : b ≤ c
h : sSup {a | a ≤ c ∧ IsAtom a} = c
s : Set α
s_max : ∀ ⦃t : Set α⦄, t ∈ {s | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a ∧ a ≤ c} → s ⊆ t → s = t
s_ind : sSupIndep s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ a ∈ s, IsAtom a ∧ a ≤ c
a : α
ha : a ∈ {a | a ≤ c ∧ IsAtom a}
con : Disjoint a (b ⊔ sSup s)
a_dis_Sup_s : Disjoint a (sSup s)
x : α
hx : x ∈ s ∪ {a}
⊢ IsAtom x ∧ x ≤ c

Tactic:
rw [Set.mem_union, Set.mem_singleton_iff] at hx
    obtain hx | rfl := hx
    · exact s_atoms x hx
    · exact ha.symm

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

Goal state before:
pp: α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
⊢ sSup {a | a ≤ ⊤ ∧ IsAtom a} = ⊤

Tactic:
simpa using h

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

Goal state before:
pp: case e_a.e_a
ι : Type u_1
R : Type u_4
inst✝¹ : CommSemiring R
inst✝ : LinearOrder ι
f g : ι → R
a : ι
s : Finset ι
ha : ∀ x ∈ s, x < a
ihs : ∏ i ∈ s, (f i + g i) = ∏ i ∈ s, f i + ∑ i ∈ s, (g i * ∏ j ∈ s with j < i, (f j + g j)) * ∏ j ∈ s with i < j, f j
ha' : a ∉ s
i : ι
hi : i ∈ s
⊢ a ∉ {j ∈ s | i < j}

Tactic:
exact mt (fun ha => (mem_filter.1 ha).1) ha'

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

Goal state before:
pp: R : Type u_4
inst✝ : CommRing R
n k : ℕ
⊢ ∏ i ∈ range k, (↑n - ↑i) = ↑(∏ i ∈ range k, (n - i))

Tactic:
rw [prod_natCast]
  rcases le_or_gt k n with hkn | hnk
  · exact prod_congr rfl fun i hi => (Nat.cast_sub <| (mem_range.1 hi).le.trans hkn).symm
  · rw [← mem_range] at hnk
    rw [prod_eq_zero hnk, prod_eq_zero hnk] <;> simp

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝¹ : Zero α
s t : Finset ι
f : (i : ι) → i ∈ s → α
inst✝ : DecidableEq ι
⊢ (indicator t fun i x ↦ (indicator s f) i) = indicator (s ∩ t) fun i hi ↦ f i ⋯

Tactic:
by
  grind [indicator_apply]

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
f : α →₀ M
a : α
b : M
⊢ f = single a b ↔ f.support ⊆ {a} ∧ f a = b

Tactic:
refine ⟨fun h => h.symm ▸ ⟨support_single_subset, single_eq_same⟩, ?_⟩
  rintro ⟨h, rfl⟩
  ext x
  by_cases hx : x = a <;> simp only [hx, single_eq_same, single_eq_of_ne, Ne, not_false_iff]
  exact notMem_support_iff.1 (mt (fun hx => (mem_singleton.1 (h hx))) hx)

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : AddZeroClass M
f : ι →₀ M
a : ι
b : M
⊢ f.update a b = single a b + erase a f

Tactic:
classical
    ext j
    rcases eq_or_ne j a with (rfl | h)
    · simp
    · simp [h, erase_ne]

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : AddZeroClass M
f : ι →₀ M
a : ι
b : M
⊢ f.update a b = erase a f + single a b

Tactic:
classical
    ext j
    rcases eq_or_ne j a with (rfl | h)
    · simp
    · simp [h, erase_ne]

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

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : Zero M
y : M
f : α →₀ M
h : y ≠ 0
⊢ optionElim y f ≠ 0

Tactic:
by
  contrapose h with c
  have : f.optionElim y none = (0 : Option α →₀ M) none := by
    rw [c]
  simp only [optionElim_apply_eq_elim, Option.elim_none, coe_zero, Pi.zero_apply] at this
  exact this

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

Goal state before:
pp: case mpr
α : Type u_1
M : Type u_2
inst✝ : Zero M
y : M
f : α →₀ M
h : f ≠ 0 ∨ y ≠ 0
⊢ optionElim y f ≠ 0

Tactic:
cases h with
    | inl h => exact optionElim_ne_zero_of_right y f h
    | inr h => exact optionElim_ne_zero_of_left y f h

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

Goal state before:
pp: case pos
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 : ℕ
x : M
hR : ¬↑n = 0
hS : ↑n = 0
⊢ f ((↑n)⁻¹ • x) = (↑n)⁻¹ • f x

Tactic:
suffices ∀ y, f y = 0 by simp [this]

Goal state after:
case pos
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 : ℕ
x : M
hR : ¬↑n = 0
hS : ↑n = 0
⊢ ∀ (y : M), f y = 0
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
⊢ optionElim (i + j) (a + b) = optionElim i a + optionElim j b

Tactic:
by
  ext x; cases x <;> simp

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
⊢ f i = ∏ j ∈ s, if i = j then f i else 1

Tactic:
rw [prod_eq_single_of_mem i hi fun _ _ _ ↦ by grind]

Goal state after:
ι : 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
⊢ f i = if i = i then f i else 1
Module: Mathlib.Algebra.Order.BigOperators.Ring.Multiset

Goal state before:
pp: α : 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)
s : Multiset α
hps : ∀ (a : α), a ∈ s → p a
⊢ f s.prod ≤ (map f s).prod

Tactic:
revert s
  refine Multiset.induction (by simp [h_one]) ?_
  intro a s hs hpsa
  by_cases hs0 : s = ∅
  · simp [hs0]
  · have hps : ∀ x, x ∈ s → p x := fun x hx ↦ hpsa x (mem_cons_of_mem hx)
    have hp_prod : p s.prod := prod_induction_nonempty p hp_mul hs0 hps
    rw [prod_cons, map_cons, prod_cons]
    exact (h_mul a s.prod (hpsa a (mem_cons_self a s)) hp_prod).trans
      (by gcongr; exacts [h0 _, hs hps])

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α ↪ β
g : β →₀ M
hg : ↑g.support ⊆ Set.range ⇑f
a : α
⊢ (embDomain f (comapDomain (⇑f) g ⋯)) (f a) = g (f a)

Tactic:
rw [embDomain_apply_self, comapDomain_apply]

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

Goal state before:
pp: case pos
α : 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✝ : α → Prop
inst✝¹ : DecidablePred p✝
f✝ : α →₀ M
p : α → Prop
inst✝ : DecidablePred p
f : α →₀ M
a : α
h : p a
⊢ a ∈ Finset.filter p f.support ↔ f a ≠ 0

Tactic:
simp only [h, mem_filter, mem_support_iff]

Goal state after:
case pos
α : 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✝ : α → Prop
inst✝¹ : DecidablePred p✝
f✝ : α →₀ M
p : α → Prop
inst✝ : DecidablePred p
f : α →₀ M
a : α
h : p a
⊢ f a ≠ 0 ∧ True ↔ f a ≠ 0
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: case neg
α : 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✝ : α → Prop
inst✝¹ : DecidablePred p✝
f✝ : α →₀ M
p : α → Prop
inst✝ : DecidablePred p
f : α →₀ M
a : α
h : ¬p a
⊢ a ∈ Finset.filter p f.support ↔ 0 ≠ 0

Tactic:
simp only [h, mem_filter, mem_support_iff]

Goal state after:
case neg
α : 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✝ : α → Prop
inst✝¹ : DecidablePred p✝
f✝ : α →₀ M
p : α → Prop
inst✝ : DecidablePred p
f : α →₀ M
a : α
h : ¬p a
⊢ f a ≠ 0 ∧ False ↔ 0 ≠ 0
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: case refine_1
ι : Type u_1
N : Type u_5
inst✝² : CommMonoid N
inst✝¹ : Preorder N
inst✝ : MulLeftMono N
s : Finset ι
f : ι → N
n : N
h : ∀ x ∈ s, f x ≤ n
⊢ ∀ x ∈ Multiset.map f s.val, x ≤ n

Tactic:
simpa using h

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

Goal state before:
pp: α : Type u_1
s : Set α
M : Type u_12
inst✝ : AddCommMonoid M
a : ↑s
x : M
⊢ ↑((restrictSupportEquiv s M).symm (single a x)) = single (↑a) x

Tactic:
classical simp

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : LinearOrder M
f g : ι → M
s : Finset ι
inst✝ : MulLeftMono M
Hlt : ∏ i ∈ s, f i < ∏ i ∈ s, g i
⊢ ∃ i ∈ s, f i < g i

Tactic:
by
  contrapose! Hlt with Hle
  exact prod_le_prod' Hle

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

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

Tactic:
by
  rw [smul_single, smul_eq_mul, mul_one]

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : SemilatticeSup α
inst✝³ : OrderBot α
inst✝² : AddCommMonoid β
inst✝¹ : Preorder β
inst✝ : AddLeftMono β
f : α → β
zero : f ⊥ = 0
ih : ∀ {s t : α}, f (s ⊔ t) ≤ f s + f t
s : ι → α
t : Finset ι
⊢ f (t.sup s) ≤ ∑ i ∈ t, f (s i)

Tactic:
by
  classical
  refine t.induction_on zero.le fun i t it h ↦ ?_
  simpa only [sup_insert, Finset.sum_insert it] using ih.trans (by gcongr)

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

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

Tactic:
Multiset.join,

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

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

Tactic:
by
  rw [← m.toFinset_sum_count_eq, m.toFinset.card_eq_sum_ones, ← tsub_le_iff_left,
    ← Finset.sum_tsub_distrib _ (by simp [one_le_count_iff_mem]), Finset.sum_le_one_iff]
  simp only [← pos_iff_ne_zero, Nat.sub_pos_iff_lt, mem_toFinset, Nat.pred_eq_succ_iff]
  exact ⟨fun h x y hx hy ↦ h x y (one_le_count_iff_mem.mp hx.le)
    (one_le_count_iff_mem.mp hy.le) hx hy, fun h x y _ _ hx hy ↦ h x y hx hy⟩

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

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

Tactic:
simpa using h

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : Semiring R
S : Type u_4
inst✝⁴ : Semiring S
inst✝³ : Module R S
inst✝² : SMulCommClass R R S
inst✝¹ : IsScalarTower R S S
inst✝ : SMulCommClass R S S
M N : Submodule R S
ι : Type u_5
m : ι → ↥M
hc : ∀ (i : ι) (n : ↥N), Commute ↑(m i) ↑n
⊢ mulLeftMap N m = N.mulRightMap m

Tactic:
ext i n; simp [(hc i n).eq]

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 : Set α
i : ↑s
a : M
⊢ ↑((supportedEquivFinsupp s).symm (single i a)) = single (↑i) a

Tactic:
classical simp

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
b : Basis ι R M
i j : ι
inst✝ : Decidable (i = j)
⊢ (single i 1) j = if i = j then 1 else 0

Tactic:
Finsupp.single_apply

Goal state after:
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
b : Basis ι R M
i j : ι
inst✝ : Decidable (i = j)
⊢ (if i = j then 1 else 0) = if i = j then 1 else 0
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s t : Set α
h : s ∩ mulSupport f = t ∩ mulSupport f
⊢ ∏ᶠ (i : α) (_ : i ∈ s), f i = ∏ᶠ (i : α) (_ : i ∈ t), f i

Tactic:
← finprod_mem_inter_mulSupport,

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s t : Set α
h : s ∩ mulSupport f = t ∩ mulSupport f
⊢ ∏ᶠ (i : α) (_ : i ∈ s ∩ mulSupport f), f i = ∏ᶠ (i : α) (_ : i ∈ t), f i
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 = (RingHom.id R) r • ∑ i, f i • v i

Tactic:
simp_rw [Finset.smul_sum, smul_smul]; rfl

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

Goal state before:
pp: case refine_1
α : Type u_1
M : Type u_2
R : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
x : M
s : Finset α
x✝ : ∃ c, ∑ i, c i • v ↑i = x
c : ↥s → R
hc : ∑ i, c i • v ↑i = x
⊢ ∑ i ∈ s, (fun i ↦ if h : i ∈ s then c ⟨i, h⟩ else 0) i • v i = ∑ i, c i • v ↑i

Tactic:
← Finset.sum_coe_sort (s := s)

Goal state after:
case refine_1
α : Type u_1
M : Type u_2
R : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
x : M
s : Finset α
x✝ : ∃ c, ∑ i, c i • v ↑i = x
c : ↥s → R
hc : ∑ i, c i • v ↑i = x
⊢ ∑ i, (fun i ↦ if h : i ∈ s then c ⟨i, h⟩ else 0) ↑i • v ↑i = ∑ i, c i • v ↑i
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: case refine_2
α : Type u_1
M : Type u_2
R : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
x : M
s : Finset α
x✝ : ∃ c, ∑ i ∈ s, c i • v i = x
c : α → R
hc : ∑ i ∈ s, c i • v i = x
⊢ ∑ i, (fun i ↦ c ↑i) i • v ↑i = ∑ i ∈ s, c i • v i

Tactic:
← Finset.sum_coe_sort (s := s)

Goal state after:
case refine_2
α : Type u_1
M : Type u_2
R : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
x : M
s : Finset α
x✝ : ∃ c, ∑ i ∈ s, c i • v i = x
c : α → R
hc : ∑ i ∈ s, c i • v i = x
⊢ ∑ i, (fun i ↦ c ↑i) i • v ↑i = ∑ i, c ↑i • v ↑i