mathlib-initiative/mathlib-tactics huggingface dataset:
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 R S M
r : S
x m₁ : M
h₁ : m₁ ∈ N
mem₁ : r • m₁ ∈ {r} • N
m₂ : M
h₂ : m₂ ∈ N
mem₂ : r • m₂ ∈ {r} • N
⊢ r • m₁ + r • m₂ = r • (m₁ + m₂)

Tactic:
by simp

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 R S M
r : S
x : M
⊢ 0 = r • 0

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
a b c : α
inst✝² : Lattice α
inst✝¹ : OrderBot α
inst✝ : IsModularLattice α
h₁ : Disjoint a (b ⊔ c)
h₂ : Disjoint b (a ⊔ c)
⊢ Disjoint c (b ⊔ a)

Tactic:
rw [disjoint_comm]

Goal state after:
α : Type u_1
a b c : α
inst✝² : Lattice α
inst✝¹ : OrderBot α
inst✝ : IsModularLattice α
h₁ : Disjoint a (b ⊔ c)
h₂ : Disjoint b (a ⊔ c)
⊢ Disjoint (b ⊔ a) c
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : IsModularLattice α
a b : α
inst✝¹ : BoundedOrder α
inst✝ : ComplementedLattice α
h : a ≤ b
⊢ ⊥ ≤ a

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : IsModularLattice α
a b : α
inst✝¹ : BoundedOrder α
inst✝ : ComplementedLattice α
h : a ≤ b
⊢ b ≤ ⊤

Tactic:
by simp

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
x : M
p p' : Submodule R M
h✝ : x ∈ span R (↑p ∪ ↑p')
y : M
h : y ∈ ↑p
⊢ 0 ∈ p'

Tactic:
by simp

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
x : M
p p' : Submodule R M
h✝ : x ∈ span R (↑p ∪ ↑p')
y : M
h : y ∈ ↑p
⊢ y + 0 = y

Tactic:
by simp

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
x : M
p p' : Submodule R M
h✝ : x ∈ span R (↑p ∪ ↑p')
y : M
h : y ∈ ↑p'
⊢ 0 ∈ p

Tactic:
by simp

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
x : M
p p' : Submodule R M
h✝ : x ∈ span R (↑p ∪ ↑p')
y : M
h : y ∈ ↑p'
⊢ 0 + y = y

Tactic:
by simp

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
x : M
p p' : Submodule R M
h : x ∈ span R (↑p ∪ ↑p')
⊢ 0 ∈ p

Tactic:
by simp

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
x : M
p p' : Submodule R M
h : x ∈ span R (↑p ∪ ↑p')
⊢ 0 ∈ p' ∧ 0 + 0 = 0

Tactic:
by simp

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
y : M
hy : y ∈ p
z : M
hz : z ∈ p'
⊢ y + z ∈ p ⊔ p'

Tactic:
exact add_mem ((le_sup_left : p ≤ p ⊔ p') hy) ((le_sup_right : p' ≤ p ⊔ p') hz)

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
z : M
⊢ (∃ y ∈ p, ∃ z_1 ∈ p', y + z_1 = z) ↔ ∃ x y, x ∈ p ∧ y ∈ p' ∧ x + y = z

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: α : Type u_3
inst✝ : SemilatticeSup α
⊢ supClosure ∅ = ∅

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: α : Type u_3
inst✝ : SemilatticeSup α
a : α
⊢ supClosure {a} = {a}

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: α : Type u_3
inst✝ : SemilatticeSup α
⊢ supClosure Set.univ = Set.univ

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝ : PartialOrder α
a b : α
h : a ≤ b
⊢ a ⋖ b ↔ IsAtom ⟨b, h⟩

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝ : PartialOrder α
a b : α
h : a ≤ b
⊢ a ⋖ b ↔ IsCoatom ⟨a, h⟩

Tactic:
by simp

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
x y : M
h : x ∈ R ∙ y
⊢ 1 • y = y

Tactic:
by simp

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
x y : M
h : x ∈ R ∙ y
⊢ 0 • y = 0

Tactic:
by simp

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

Goal state before:
pp: case refine_3
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M
h : x ∈ R ∙ y
⊢ ∀ (x y_1 : M), x ∈ R ∙ y → y_1 ∈ R ∙ y → (∃ a, a • y = x) → (∃ a, a • y = y_1) → ∃ a, a • y = x + y_1

pp: case refine_4
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M
h : x ∈ R ∙ y
⊢ ∀ (a : R), ∀ x ∈ R ∙ y, (∃ a, a • y = x) → ∃ a_2, a_2 • y = a • x

Tactic:
· rintro _ _ - - ⟨a, rfl⟩ ⟨b, rfl⟩
      exact ⟨a + b, by simp [add_smul]⟩

Goal state after:
case refine_4
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M
h : x ∈ R ∙ y
⊢ ∀ (a : R), ∀ x ∈ R ∙ y, (∃ a, a • y = x) → ∃ a_2, a_2 • y = a • x
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
y : M
a : R
⊢ y ∈ {y}

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_4
inst✝¹ : BooleanAlgebra α
inst✝ : IsAtomic α
x y : α
h : ∀ (a : α), IsAtom a → a ≤ x → a ≤ y
this : x ⊓ yᶜ = ⊥
⊢ y = yᶜᶜ

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_4
inst✝¹ : BooleanAlgebra α
inst✝ : IsAtomic α
x y : α
h : x = y
⊢ ∀ (a : α), IsAtom a → (a ≤ x ↔ a ≤ x)

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: α : Type u_3
inst✝ : Lattice α
⊢ latticeClosure ∅ = ∅

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: α : Type u_3
inst✝ : Lattice α
a : α
⊢ latticeClosure {a} = {a}

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: α : Type u_3
inst✝ : Lattice α
⊢ latticeClosure Set.univ = Set.univ

Tactic:
by simp

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
x : M
⊢ R ∙ x = ⊥ ↔ x = 0

Tactic:
by simp

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
I : Submodule R M
a : M
⊢ I < I ⊔ R ∙ a ↔ a ∉ I

Tactic:
by simp

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
s : Set M
ht : ↑∅ ⊆ ↑(span R s)
⊢ ↑∅ ⊆ s ∧ ↑∅ ⊆ ↑(span R ↑∅)

Tactic:
by simp

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

Goal state before:
pp: α : Type u
r : α → α → Prop
inst✝ : IsTrans α r
ι : Type u_1
hι : Nonempty ι
f : ι → α
D : Directed r f
s : Finset ι
z x✝ : ι
⊢ x✝ ∈ 0 → r (f x✝) (f z)

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
b : β
⊢ ⇑e ⁻¹' Iio b = Iio (e.symm b)

Tactic:
by
  ext x
  simp [← e.lt_iff_lt]

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
f : Bool → α
⊢ true ≠ false

Tactic:
simp only [Ne, not_false_iff, reduceCtorEq]

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
f : Fin 2 → α
⊢ 0 ≠ 1

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝³ : Lattice α
inst✝² : OrderBot α
inst✝¹ : IsUpperModularLattice α
inst✝ : IsAtomistic α
a b : α
hab : a < b
s : Set α
hsb : IsLUB s b
h : ∀ a ∈ s, IsAtom a
x : α
hx : x ∈ s
hcon : ¬a ⋖ x ⊔ a
⊢ ⊥ ≤ x ⊓ a

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝³ : Lattice α
inst✝² : OrderBot α
inst✝¹ : IsUpperModularLattice α
inst✝ : IsAtomistic α
a b : α
hab : a < b
s : Set α
hsb : IsLUB s b
h : ∀ a ∈ s, IsAtom a
x : α
hx : x ∈ s
hcon : ¬a ⋖ x ⊔ a
⊢ x ⊓ a ≤ x

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝³ : Lattice α
inst✝² : BoundedOrder α
inst✝¹ : IsModularLattice α
inst✝ : ComplementedLattice α
h : IsCoatomic α
⊢ IsStronglyCoatomic α

Tactic:
exact isStronglyCoatomic

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: p : Prop
⊢ IsAtom p ↔ p

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: p : Prop
⊢ IsCoatom p ↔ ¬p

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: ι✝ : Sort u_1
α : Type u_2
β : Type u_3
ι : Type u_4
π : ι → Type u
inst✝² : (i : ι) → PartialOrder (π i)
inst✝¹ : (i : ι) → OrderBot (π i)
inst✝ : ∀ (i : ι), IsAtomic (π i)
b : (i : ι) → π i
h : ¬b = ⊥
i : ι
hi : ¬b i = ⊥
a : π i
ha : IsAtom a
hab : a ≤ b i
⊢ ∀ (j : ι), j ≠ i → ⊥ j ≤ b j

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: ι✝ : Sort u_1
α : Type u_2
β : Type u_3
ι : Type u_4
π : ι → Type u
inst✝² : (i : ι) → PartialOrder (π i)
inst✝¹ : (i : ι) → OrderBot (π i)
inst✝ : ∀ (i : ι), IsAtomistic (π i)
s : (i : ι) → π i
i : ι
j : π i
hj : j ∈ upperBounds (Function.eval i '' {f | (∃ i a, IsAtom a ∧ f = Function.update ⊥ i a) ∧ f ≤ s})
x : π i
x✝ : x ∈ {a | IsAtom a ∧ a ≤ s i}
hx₁ : IsAtom x
hx₂ : x ≤ s i
⊢ Function.eval i (Function.update ⊥ i x) = x

Tactic:
by simp

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

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
k : α
H : ∀ (ι : Type u) (s : ι → α), k ≤ iSup s → ∃ t, k ≤ t.sup s
s : Set α
hs : k ≤ sSup s
t : Finset ↑s
ht : k ≤ t.sup Subtype.val
⊢ ↑(Finset.image Subtype.val t) ⊆ s

Tactic:
by simp

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

Goal state before:
pp: α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
s : Set α
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ t.sup id = x}
⊢ ↑∅ ⊆ s ∧ ∅.sup id = ⊥

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Notation.Indicator

Goal state before:
pp: α : Type u_1
M : Type u_3
inst✝ : One M
t : Set α
s : Set M
⊢ 1 ⁻¹' s ∈ {univ, ∅}

Tactic:
Pi.one_def,

Goal state after:
α : Type u_1
M : Type u_3
inst✝ : One M
t : Set α
s : Set M
⊢ (fun x ↦ 1) ⁻¹' s ∈ {univ, ∅}
Module: Mathlib.Algebra.Notation.Indicator

Goal state before:
pp: α : Type u_1
M : Type u_3
inst✝² : One M
U : Set α
s : Set M
a : M
inst✝¹ : Decidable (a ∈ s)
inst✝ : Decidable (1 ∈ s)
⊢ U.ite ((fun x ↦ a) ⁻¹' s) (1 ⁻¹' s) = (if a ∈ s then U else ∅) ∪ if 1 ∈ s then Uᶜ else ∅

Tactic:
Pi.one_def,

Goal state after:
α : Type u_1
M : Type u_3
inst✝² : One M
U : Set α
s : Set M
a : M
inst✝¹ : Decidable (a ∈ s)
inst✝ : Decidable (1 ∈ s)
⊢ U.ite ((fun x ↦ a) ⁻¹' s) ((fun x ↦ 1) ⁻¹' s) = (if a ∈ s then U else ∅) ∪ if 1 ∈ s then Uᶜ else ∅
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
s : Set α
hs : sSupIndep s
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = t.sup id
x : α
hx₀ : x ∈ s
hx₁ : x ≠ ⊥
hx₂ : x ∉ t
⊢ x ∈ ↑t ∪ {x}

Tactic:
by simp

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

Goal state before:
pp: α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
ι : Type u_3
t : ι → α
ht : iSupIndep t
⊢ {i | t i ≠ ⊥}.Finite

Tactic:
refine Finite.of_finite_image (Finite.subset ?_ (image_subset_range t _)) ht.injOn

Goal state after:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
ι : Type u_3
t : ι → α
ht : iSupIndep t
⊢ (range t).Finite
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedLT α
ι : Type u_3
t : ι → α
ht : iSupIndep t
⊢ {i | t i ≠ ⊥}.Finite

Tactic:
refine Finite.of_finite_image (Finite.subset ?_ (image_subset_range t _)) ht.injOn

Goal state after:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedLT α
ι : Type u_3
t : ι → α
ht : iSupIndep t
⊢ (range t).Finite
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
K : Type u_3
M : Type u_4
M₂ : Type u_5
V✝ : Type u_6
S✝ : Type u_7
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
x : M
p p' : Submodule R M
inst✝⁴ : Semiring R₂
σ₁₂ : R →+* R₂
inst✝³ : AddCommMonoid M₂
inst✝² : Module R₂ M₂
s✝ t : Set M
N : Type u_8
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
V : Submodule R M
f g : ↥V →ₗ[R] N
S : Set M
hV : V = span R S
s : ↑S
⊢ ↑s ∈ S

Tactic:
by simp

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

Goal state before:
pp: α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a : α
s : Set α
h : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
⊢ a ⊓ sSup s = ⨆ b ∈ s, a ⊓ b

Tactic:
h.inf_sSup_eq

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
N : Type u_8
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f g : M →ₗ[R] N
S : Set M
hM : span R S = ⊤
h : f ∘ₗ ⊤.subtype = g ∘ₗ ⊤.subtype
x : M
⊢ x ∈ ⊤

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
K : Type u_3
M : Type u_4
M₂ : Type u_5
V✝ : Type u_6
S✝ : Type u_7
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
x : M
p p' : Submodule R M
inst✝⁴ : Semiring R₂
σ₁₂ : R →+* R₂
inst✝³ : AddCommMonoid M₂
inst✝² : Module R₂ M₂
s✝ t : Set M
N : Type u_8
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
V : Submodule R M
f : ↥V →ₗ[R] N
S : Set M
hV : V = span R S
s : ↑S
⊢ ↑s ∈ S

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
K : Type u_3
M : Type u_4
M₂ : Type u_5
V : Type u_6
S : Type u_7
inst✝⁹ : Semiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
x✝ : M
p✝ p' : Submodule R M
inst✝⁶ : Semiring R₂
σ₁₂ : R →+* R₂
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R₂ M₂
s t : Set M
inst✝³ : Semiring S
inst✝² : SMul R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
p : Submodule R M
x y : ↥p
⊢ ⟨↑(x + y), ⋯⟩ = ⟨↑x, ⋯⟩ + ⟨↑y, ⋯⟩

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
K : Type u_3
M : Type u_4
M₂ : Type u_5
V : Type u_6
S : Type u_7
inst✝⁹ : Semiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
x✝ : M
p✝ p' : Submodule R M
inst✝⁶ : Semiring R₂
σ₁₂ : R →+* R₂
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R₂ M₂
s t✝ : Set M
inst✝³ : Semiring S
inst✝² : SMul R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
p : Submodule R M
t : R
x : ↥p
⊢ ⟨↑(t • x), ⋯⟩ = (RingHom.id R) t • ⟨↑x, ⋯⟩

Tactic:
by simp

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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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 τ₁₂
ι : Type u_8
s : Set ι
p : ι → Submodule R₂ M₂
hp : ⨆ x, p ↑x = ⊤
f : M →ₛₗ[τ₁₂] M₂
hf : Surjective ⇑f
k : ι
hk : k ∈ s
⊢ comap f (map f (⨆ x, comap f (p ↑x))) = ⊤

Tactic:
map_iSup_comap_of_surjective hf,

Goal state after:
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 τ₁₂
ι : Type u_8
s : Set ι
p : ι → Submodule R₂ M₂
hp : ⨆ x, p ↑x = ⊤
f : M →ₛₗ[τ₁₂] M₂
hf : Surjective ⇑f
k : ι
hk : k ∈ s
⊢ comap f (⨆ x, p ↑x) = ⊤
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:
by 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:
by 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:
by simp

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Submodule R M
x : M
⊢ Disjoint s (R ∙ x) ↔ ∀ (r : R), r • x ∈ s → r • x = 0

Tactic:
rw [disjoint_comm]

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Submodule R M
x : M
⊢ Disjoint (R ∙ x) s ↔ ∀ (r : R), r • x ∈ s → r • x = 0
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:
by 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:
by 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:
by simp

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
a : α
b : M
⊢ single a b = 0 ↔ b = 0

Tactic:
classical simp [DFunLike.ext_iff, single_apply]

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:
by 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:
by 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 α
x : M
⊢ (fun f ↦ f a) (single a x) = x

Tactic:
by simp

Goal state after: