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

Goal state before:
pp: α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
s : Set α
h : ∀ (t : Finset α), ↑t ⊆ s → sSupIndep ↑t
a : α
ha : a ∈ s
⊢ Disjoint a (sSup (s \ {a}))

Tactic:
rw [disjoint_iff, inf_sSup_eq_iSup_inf_sup_finset, iSup_eq_bot]
    intro t
    rw [iSup_eq_bot, Finset.sup_id_eq_sSup]
    intro ht
    classical
      have h' := (h (insert a t) ?_ (t.mem_insert_self a)).eq_bot
      · rwa [Finset.coe_insert, Set.insert_sdiff_self_of_notMem] at h'
        exact fun con => ((Set.mem_sdiff a).1 (ht con)).2 (Set.mem_singleton a)
      · rw [Finset.coe_insert, Set.insert_subset_iff]
        exact ⟨ha, Set.Subset.trans ht sdiff_subset⟩

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

Goal state before:
pp: R : Type u_1
M : Type u_4
S : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
s : Set M
inst✝³ : Semiring S
inst✝² : SMul R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
⊢ span S s ≤ span S ↑(span R s)

Tactic:
simp

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

Goal state before:
pp: case mp.inl
R : Type u_8
M : Type u_9
inst✝⁴ : Ring R
inst✝³ : IsDomain R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.IsTorsionFree R M
a b : R
hb : b • a • 0 = 0
⊢ ∃ z, z • a • 0 = 0

Tactic:
simp

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

Goal state before:
pp: case hi
ι : Type u_1
β : Type u_2
inst✝² : CommMonoid β
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
κ : ι → Type u_3
t : (i : ι) → Finset (κ i)
f : ((i : ι) → i ∈ univ → κ i) → β
⊢ ∀ a ∈ univ.pi t, (fun i ↦ a i ⋯) ∈ Fintype.piFinset t

Tactic:
simp

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

Goal state before:
pp: case hj
ι : Type u_1
β : Type u_2
inst✝² : CommMonoid β
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
κ : ι → Type u_3
t : (i : ι) → Finset (κ i)
f : ((i : ι) → i ∈ univ → κ i) → β
⊢ ∀ a ∈ Fintype.piFinset t, (fun i x ↦ a i) ∈ univ.pi t

Tactic:
simp

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

Goal state before:
pp: case left_inv
ι : Type u_1
β : Type u_2
inst✝² : CommMonoid β
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
κ : ι → Type u_3
t : (i : ι) → Finset (κ i)
f : ((i : ι) → i ∈ univ → κ i) → β
⊢ ∀ a ∈ univ.pi t, (fun i x ↦ (fun i ↦ a i ⋯) i) = a

Tactic:
simp

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

Goal state before:
pp: case right_inv
ι : Type u_1
β : Type u_2
inst✝² : CommMonoid β
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
κ : ι → Type u_3
t : (i : ι) → Finset (κ i)
f : ((i : ι) → i ∈ univ → κ i) → β
⊢ ∀ a ∈ Fintype.piFinset t, (fun i ↦ (fun i x ↦ a i) i ⋯) = a

Tactic:
simp

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

Goal state before:
pp: case h
ι : Type u_1
β : Type u_2
inst✝² : CommMonoid β
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
κ : ι → Type u_3
t : (i : ι) → Finset (κ i)
f : ((i : ι) → i ∈ univ → κ i) → β
⊢ ∀ a ∈ univ.pi t, f a = f fun a_2 x ↦ (fun i ↦ a i ⋯) a_2

Tactic:
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
a : α
S : Submodule R M
⊢ a • S = span R ↑(a • S)

Tactic:
simp [← smul_span]

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

Goal state before:
pp: ι : Type u_7
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
R : Type u_8
inst✝ : NonAssocSemiring R
x : ι → R
x✝ : ι
⊢ x x✝ = (∑ i, x i • fun j ↦ if i = j then 1 else 0) x✝

Tactic:
simp

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✝ : Fintype I
f : (i : I) → M i
a : I
⊢ (∏ i, Pi.mulSingle i (f i)) a = f a

Tactic:
simp

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

Goal state before:
pp: case inl
α : Type u_2
inst✝ : CompleteLattice α
b : α
h : IsCompactElement b
hbk : b ∈ Iic b
⊢ ⟨b, hbk⟩ = ⊤ ∨ ∃ a, IsCoatom a ∧ ⟨b, hbk⟩ ≤ a

Tactic:
left; ext; simp only [Set.Iic.coe_top]

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

Goal state before:
pp: case e'_3
ι : Type u_8
α : Type u_9
β : Type u_10
inst✝ : CommMonoid α
s : Set β
f f' : ι → β → α
h : ∀ (i : ι), Set.EqOn (f i) (f' i) s
v : Finset ι
x✝ : β
⊢ ∏ i ∈ v, f i x✝ = (∏ i ∈ v, f i) x✝

Tactic:
simp

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

Goal state before:
pp: case e'_4
ι : Type u_8
α : Type u_9
β : Type u_10
inst✝ : CommMonoid α
s : Set β
f f' : ι → β → α
h : ∀ (i : ι), Set.EqOn (f i) (f' i) s
v : Finset ι
x✝ : β
⊢ ∏ i ∈ v, f' i x✝ = (∏ i ∈ v, f' i) x✝

Tactic:
simp

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

Goal state before:
pp: case empty
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 α β
f : ι → F
x : α
⊢ (∏ i ∈ ∅, f i) x = ∏ i ∈ ∅, (f i) x

Tactic:
simp

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
x✝ : α
⊢ (∏ i ∈ s, f i) x✝ = (∏ i ∈ s, ⇑(f i)) x✝

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
a : α
s : Multiset α
l : List α
⊢ (powersetAux' l).zip (List.map (cons a) (powersetAux' l)).reverse ++
      (List.map (cons a) (powersetAux' l)).zip (powersetAux' l).reverse =
    (List.map id (powersetAux' l)).zip (List.map (cons a) (powersetAux' l).reverse) ++
      (List.map (cons a) (powersetAux' l)).zip (List.map id (powersetAux' l).reverse)

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
a : α
s : Multiset α
l : List α
⊢ (powersetAux' l).length = (List.map (cons a) (powersetAux' l)).reverse.length

Tactic:
simp

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

Goal state before:
pp: case empty
α : Type u_1
t : Multiset α
⊢ (0 + t).antidiagonal = (antidiagonal 0).bind fun p ↦ map (fun q ↦ (p.1 + q.1, p.2 + q.2)) t.antidiagonal

Tactic:
simp

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

Goal state before:
pp: M₀ : Type u_4
inst✝² : MonoidWithZero M₀
inst✝¹ : Nontrivial M₀
inst✝ : NoZeroDivisors M₀
⊢ [].prod = 0 ↔ 0 ∈ []

Tactic:
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
x✝ : List κ
⊢ (zipWith (fun i j ↦ a * f i j) [] x✝).sum = a * (zipWith f [] x✝).sum

Tactic:
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
x✝ : List ι
⊢ (zipWith (fun i j ↦ a * f i j) x✝ []).sum = a * (zipWith f x✝ []).sum

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: case empty
α : Type u_1
⊢ ∀ {a : Multiset α}, a ∈ Sections 0 ↔ Rel (fun s a ↦ a ∈ s) 0 a

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
s : Multiset (Multiset α)
⊢ (Sections 0).card = (map card 0).prod

Tactic:
simp

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

Goal state before:
pp: case cons.e'_5.a.e'_4
α : Type u_1
t : Multiset α
a : α
s : Multiset α
ih : (s + t).antidiagonal = s.antidiagonal.bind fun p ↦ map (fun q ↦ (p.1 + q.1, p.2 + q.2)) t.antidiagonal
a✝² : Multiset α × Multiset α
a✝¹ : a✝² ∈ s.antidiagonal
x✝ : Multiset α × Multiset α
a✝ : x✝ ∈ t.antidiagonal
⊢ (((fun x ↦ Prod.map id (cons a) x) ∘ fun q ↦ (a✝².1 + q.1, a✝².2 + q.2)) x✝).2 = (Prod.map id (cons a) a✝²).2 + x✝.2

Tactic:
simp

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

Goal state before:
pp: case cons.e'_6.a.e'_3
α : Type u_1
t : Multiset α
a : α
s : Multiset α
ih : (s + t).antidiagonal = s.antidiagonal.bind fun p ↦ map (fun q ↦ (p.1 + q.1, p.2 + q.2)) t.antidiagonal
a✝² : Multiset α × Multiset α
a✝¹ : a✝² ∈ s.antidiagonal
x✝ : Multiset α × Multiset α
a✝ : x✝ ∈ t.antidiagonal
⊢ (((fun x ↦ Prod.map (cons a) id x) ∘ fun q ↦ (a✝².1 + q.1, a✝².2 + q.2)) x✝).1 = (Prod.map (cons a) id a✝²).1 + x✝.1

Tactic:
simp

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

Goal state before:
pp: M : Type u_2
inst✝¹ : CommMonoid M
inst✝ : HasDistribNeg M
s : Multiset M
⊢ ∀ (a : List M), (map Neg.neg ⟦a⟧).prod = (-1) ^ card ⟦a⟧ * prod ⟦a⟧

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝ : NonUnitalNonAssocSemiring R
a : R
s : Multiset ι
f : ι → R
⊢ (map (fun i ↦ a * f i) 0).sum = a * (map f 0).sum

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝ : NonUnitalNonAssocSemiring R
a : R
s : Multiset ι
f : ι → R
⊢ (map (fun i ↦ f i * a) 0).sum = (map f 0).sum * a

Tactic:
simp

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

Goal state before:
pp: R : Type u_4
inst✝ : CommSemiring R
s : Multiset (Multiset R)
⊢ (map sum 0).prod = (map prod (Sections 0)).sum

Tactic:
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
M' : Type u_8
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
x✝ : M × M'
⊢ x✝ ∈ ⊤.prod ⊤ ↔ x✝ ∈ ⊤

Tactic:
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
M' : Type u_8
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
x : M
y : M'
⊢ (x, y) ∈ ⊥.prod ⊥ ↔ (x, y) ∈ ⊥

Tactic:
simp

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

Goal state before:
pp: case zero_left
R : Type u_9
M : Type u_10
N : Type u_11
P : Type u_12
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
P' : Submodule R P
s : Set M
t : Set N
B : M →ₗ[R] N →ₗ[R] P
hB : ∀ x ∈ s, ∀ y ∈ t, (B x) y ∈ P'
x : M
y v : N
hv : v ∈ span R t
⊢ (B 0) v ∈ P'

Tactic:
simp

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

Goal state before:
pp: case zero_right
R : Type u_9
M : Type u_10
N : Type u_11
P : Type u_12
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
P' : Submodule R P
s : Set M
t : Set N
B : M →ₗ[R] N →ₗ[R] P
hB : ∀ x ∈ s, ∀ y ∈ t, (B x) y ∈ P'
x : M
y : N
u : M
hu : u ∈ span R s
⊢ (B u) 0 ∈ P'

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝¹ : NonAssocSemiring R
inst✝ : DecidableEq ι
s : Finset ι
f : ι → R
i : ι
⊢ (∑ j ∈ s, f j * if i = j then 1 else 0) = if i ∈ s then f i else 0

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝¹ : NonAssocSemiring R
inst✝ : DecidableEq ι
s : Finset ι
f : ι → R
i : ι
⊢ ∑ j ∈ s, (if i = j then 1 else 0) * f j = if i ∈ s then f i else 0

Tactic:
simp

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

Goal state before:
pp: case empty
ι : Type u_1
R : Type u_4
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
κ : ι → Type u_5
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → R
⊢ ∏ a ∈ ∅, ∑ b ∈ t a, f a b = ∑ p ∈ ∅.pi t, ∏ x ∈ ∅.attach, f (↑x) (p ↑x ⋯)

Tactic:
simp

Goal state after:
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
x y : M
hy : y ∈ ↑p
e : f y = f x
⊢ y + (x - y) = x

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
⊢ {x | x ∈ 0 ∧ p x}.Subsingleton

Tactic:
simp

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

Goal state before:
pp: κ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
s : Finset κ
f : κ → R
n : ℕ
⊢ (∑ a ∈ s, f a) ^ n = ∏ i, ∑ j ∈ s, f j

Tactic:
simp

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

Goal state before:
pp: case empty
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
a : α
hp : {x | x ∈ 0 ∧ p x}.Subsingleton
⊢ find? p 0 hp = some a ↔ a ∈ 0 ∧ p a

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
f g : ι → R
s : Finset ι
⊢ ∏ i ∈ s, (f i + g i) = ∏ i ∈ s, ∑ p ∈ {True, False}, if p then f i else g i

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
f g : ι → R
s : Finset ι
⊢ ∀ a ∈ s.pi fun x ↦ {True, False}, {a_1 ∈ s | ∃ (h : a_1 ∈ s), a a_1 h} ∈ s.powerset

Tactic:
simp

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

Goal state before:
pp: case empty
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
hp : {x | x ∈ 0 ∧ p x}.Subsingleton
⊢ find? p 0 hp = none ↔ ∀ (a : α), a ∈ 0 → ¬p a

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝¹ : CommSemiring R
inst✝ : LinearOrder ι
s : Finset ι
f g : ι → R
⊢ ∏ i ∈ ∅, (f i + g i) = ∏ i ∈ ∅, f i + ∑ i ∈ ∅, (g i * ∏ j ∈ ∅ with j < i, (f j + g j)) * ∏ j ∈ ∅ with i < j, f j

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
M : Type u_4
inst✝ : Zero M
f : α →₀ M
⊢ #f.support = 0 ↔ f = 0

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
G : Type u_7
H : Type u_8
inst✝ : Zero M
f : α →₀ M
⊢ ∀ (a : α), f a ≠ 0 → a ∈ f.support

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
M : Type u_4
inst✝ : Zero M
f : α →₀ M
a✝ : α
⊢ (onFinset f.support ⇑f ⋯) a✝ = f a✝

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
M : Type u_4
N : Type u_5
inst✝¹ : Zero M
inst✝ : Zero N
e : M → N
he₀ : e 0 = 0
he : Surjective e
⊢ {g | ∀ (i : α), g i ∈ Set.univ} = Set.univ

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
G : Type u_7
H : Type u_8
inst✝² : Zero M
inst✝¹ : Zero N
inst✝ : Zero O
e : M ≃ N
hf : e 0 = 0
x : ι →₀ M
a✝ : ι
⊢ (mapRange ⇑e.symm ⋯ (mapRange (⇑e) hf x)) a✝ = x a✝

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
G : Type u_7
H : Type u_8
inst✝² : Zero M
inst✝¹ : Zero N
inst✝ : Zero O
e : M ≃ N
hf : e 0 = 0
x : ι →₀ N
a✝ : ι
⊢ (mapRange (⇑e) hf (mapRange ⇑e.symm ⋯ x)) a✝ = x a✝

Tactic:
simp

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

Goal state before:
pp: ι : Type u_3
M : Type u_4
inst✝ : Zero M
x✝ : ι →₀ M
a✝ : ι
⊢ ((equiv (Equiv.refl M) ⋯) x✝) a✝ = ((Equiv.refl (ι →₀ M)) x✝) a✝

Tactic:
simp

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

Goal state before:
pp: ι : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
inst✝² : Zero M
inst✝¹ : Zero N
inst✝ : Zero O
e : M ≃ N
hf : e 0 = 0
f₂ : N ≃ O
hf₂ : f₂ 0 = 0
x✝ : ι →₀ M
a✝ : ι
⊢ ((equiv (e.trans f₂) ⋯) x✝) a✝ = (((equiv e hf).trans (equiv f₂ hf₂)) x✝) a✝

Tactic:
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
⊢ (toSpanSingleton R M 0) 1 = 0 1

Tactic:
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
x y : M
⊢ (toSpanSingleton R M (x + y)) 1 = (toSpanSingleton R M x + toSpanSingleton R M y) 1

Tactic:
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)) 1 = (r • toSpanSingleton R M x) 1

Tactic:
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) 1 = (toSpanSingleton R M₂ (f x)) 1

Tactic:
simp

Goal state after:
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✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Semiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
σ₁₂ : R →+* R₂
s : Set M
f g : M →ₛₗ[σ₁₂] M₂
⊢ Set.EqOn ⇑f ⇑g ↑(span R s) ↔ Set.EqOn (⇑f) (⇑g) s

Tactic:
rw [← le_eqLocus, span_le]

Goal state after:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Semiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
σ₁₂ : R →+* R₂
s : Set M
f g : M →ₛₗ[σ₁₂] M₂
⊢ s ⊆ ↑(f.eqLocus g) ↔ Set.EqOn (⇑f) (⇑g) s
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝⁴ : Ring R
inst✝³ : IsDomain R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.IsTorsionFree R M
x : M
h : x ≠ 0
⊢ (toSpanNonzeroSingleton R M x h) 1 = ⟨x, ⋯⟩

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝¹ : CommSemiring R
inst✝ : LinearOrder ι
s : Finset ι
f : ι → R
⊢ ∏ i ∈ s, 1 + ∑ i ∈ s, (f i * ∏ j ∈ s with j < i, (1 + f j)) * ∏ j ∈ s with i < j, 1 =
    1 + ∑ i ∈ s, f i * ∏ j ∈ s with j < i, (1 + f j)

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝¹ : CommRing R
inst✝ : LinearOrder ι
s : Finset ι
f g : ι → R
⊢ -∑ x ∈ s, (g x * ∏ x ∈ s with x < x, (f x + -g x)) * ∏ i ∈ s with x < i, f i =
    ∑ i ∈ s, (-g i * ∏ j ∈ s with j < i, (f j + -g j)) * ∏ j ∈ s with i < j, f j

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝¹ : CommRing R
inst✝ : LinearOrder ι
s : Finset ι
f : ι → R
⊢ ∏ i ∈ s, 1 - ∑ i ∈ s, (f i * ∏ j ∈ s with j < i, (1 - f j)) * ∏ j ∈ s with i < j, 1 =
    1 - ∑ i ∈ s, f i * ∏ j ∈ s with j < i, (1 - f j)

Tactic:
simp

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

Goal state before:
pp: case inr
R : Type u_4
inst✝ : CommRing R
n k : ℕ
hnk : n ∈ range k
⊢ ↑(n - n) = 0

Tactic:
simp

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

Goal state before:
pp: case inr
R : Type u_4
inst✝ : CommRing R
n k : ℕ
hnk : n ∈ range k
⊢ ↑n - ↑n = 0

Tactic:
simp

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

Goal state before:
pp: case inl
ι : Type u_5
s : Finset ι
f : ι → ℕ
hf : ∀ i ∈ s, 0 ∣ f i
⊢ (∑ i ∈ s, f i) / 0 = ∑ i ∈ s, f i / 0

Tactic:
simp

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

Goal state before:
pp: case inl
ι : Type u_5
s : Finset ι
f : ι → ℤ
hf : ∀ i ∈ s, 0 ∣ f i
⊢ (∑ i ∈ s, f i) / 0 = ∑ i ∈ s, f i / 0

Tactic:
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✝ → α
i✝ : ι
s : Finset ι
f : (i : ι) → i ∈ s → α
i : ι
⊢ i ∈ map (Embedding.subtype fun x ↦ x ∈ s) {i | f ↑i ⋯ ≠ 0} ↔ (if H : i ∈ s then f i H else 0) ≠ 0

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : Zero M
x✝ : ι →₀ M
a✝ : ι
⊢ ((zeroHom (ZeroHom.id M)) x✝) a✝ = ((ZeroHom.id (ι →₀ M)) x✝) a✝

Tactic:
simp

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✝² : Zero M
inst✝¹ : Zero N
inst✝ : Zero O
f : ZeroHom N O
f₂ : ZeroHom M N
x✝ : ι →₀ M
a✝ : ι
⊢ ((zeroHom (f.comp f₂)) x✝) a✝ = (((zeroHom f).comp (zeroHom f₂)) x✝) a✝

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
F : Type u_2
M : Type u_3
N : Type u_4
O : Type u_5
G : Type u_6
H : Type u_7
inst✝¹ : AddZeroClass M
inst✝ : AddZeroClass N
f✝ : M → N
g₁ g₂ : ι →₀ M
f : ι ↪ F
⊢ embDomain f 0 = 0

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
F : Type u_2
M : Type u_3
N : Type u_4
O : Type u_5
G : Type u_6
H : Type u_7
inst✝¹ : AddZeroClass M
inst✝ : AddZeroClass N
f✝ : M → N
g₁ g₂ : ι →₀ M
f : ι ↪ F
v w : ι →₀ M
⊢ embDomain f (v + w) = embDomain f v + embDomain f w

Tactic:
ext b

Goal state after:
ι : Type u_1
F : Type u_2
M : Type u_3
N : Type u_4
O : Type u_5
G : Type u_6
H : Type u_7
inst✝¹ : AddZeroClass M
inst✝ : AddZeroClass N
f✝ : M → N
g₁ g₂ : ι →₀ M
f : ι ↪ F
v w : ι →₀ M
b : F
⊢ (embDomain f (v + w)) b = (embDomain f v + embDomain f w) b
Module: Mathlib.Algebra.Group.Finsupp

Goal state before:
pp: case pos
ι : Type u_1
F : Type u_2
M : Type u_3
N : Type u_4
O : Type u_5
G : Type u_6
H : Type u_7
inst✝¹ : AddZeroClass M
inst✝ : AddZeroClass N
f✝ : M → N
g₁ g₂ : ι →₀ M
f : ι ↪ F
v w : ι →₀ M
a : ι
⊢ (embDomain f (v + w)) (f a) = (embDomain f v + embDomain f w) (f a)

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : AddZeroClass M
a : ι
m₁ m₂ : M
b : ι
⊢ (single a (m₁ + m₂)) b = (single a m₁) b + (single a m₂) b

Tactic:
simp

Goal state after:
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
⊢ {f₁} ∪ {f₂} = {f₁, f₂}

Tactic:
simp

Goal state after:
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
⊢ {f₁} ⊆ {f₁, f₂}

Tactic:
simp

Goal state after:
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
⊢ {f₂} ⊆ {f₁, f₂}

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : Zero M
a✝ a' : α
b : M
a : α
inst✝ : Subsingleton α
f : α →₀ M
⊢ single a ((fun f ↦ f a) f) = f

Tactic:
ext b

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : Zero M
a✝ a' : α
b✝ : M
a : α
inst✝ : Subsingleton α
f : α →₀ M
b : α
⊢ (single a ((fun f ↦ f a) f)) b = f b