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

Goal state before:
pp: α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
hf : InjOn f {i | f i ≠ ⊥}
h : ∀ (s : Finset ι), s.SupIndep f
i : ι
⊢ Disjoint (f i) (sSup (f '' {j | j ≠ i}))

Tactic:
[

Goal state after:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
hf : InjOn f {i | f i ≠ ⊥}
h : ∀ (s : Finset ι), s.SupIndep f
i : ι
⊢ Disjoint (f i) (sSup (f '' {j | j ≠ i}))
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:
[

Goal state after:
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)
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
ι : Sort u_8
p : ι → Submodule R M
x : M
⊢ x ∈ (⨆ i, p i).toAddSubmonoid → x ∈ ⨆ i, (p i).toAddSubmonoid

Tactic:
[

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Sort u_8
p : ι → Submodule R M
x : M
⊢ x ∈ (⨆ i, p i).toAddSubmonoid → x ∈ ⨆ i, (p i).toAddSubmonoid
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
s : Set ι
a : α
hs : ∀ t ⊆ s, t.Finite → Disjoint (⨆ i ∈ t, f i) a
⊢ Disjoint (⨆ i ∈ s, f i) a

Tactic:
[

Goal state after:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
s : Set ι
a : α
hs : ∀ t ⊆ s, t.Finite → Disjoint (⨆ i ∈ t, f i) a
⊢ Disjoint (⨆ i ∈ s, f i) a
Module: Mathlib.Algebra.BigOperators.Pi

Goal state before:
pp: ι✝ : Type u_1
κ : Type u_2
M✝ : Type u_3
N : Type u_4
R : Type u_5
α : Type u_6
ι : Type u_7
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
M : ι → Type u_8
inst✝¹ : (i : ι) → CommMonoid (M i)
M' : Type u_9
inst✝ : CommMonoid M'
φ : ((i : ι) → M i) →* M'
⊢ (fun φ ↦ ∏ i, (φ i).comp (evalMonoidHom M i)) ((fun φ i ↦ φ.comp (MonoidHom.mulSingle M i)) φ) = φ

Tactic:
ext
    simp only [MonoidHom.finsetProd_apply, MonoidHom.coe_comp, Function.comp_apply,
      evalMonoidHom_apply, MonoidHom.mulSingle_apply, ← map_prod]
    refine congrArg _ <| funext fun _ ↦ ?_
    rw [Fintype.prod_apply]
    exact Fintype.prod_pi_mulSingle ..

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

Goal state before:
pp: ι : Type u_1
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
M : ι → Type u_7
inst✝ : (i : ι) → CommMonoid (M i)
p : ((i : ι) → M i) → Prop
f : (i : ι) → M i
one : p 1
mul : ∀ (f g : (i : ι) → M i), p f → p g → p (f * g)
mulSingle : ∀ (i : ι) (m : M i), p (Pi.mulSingle i m)
⊢ p f

Tactic:
cases nonempty_fintype ι
  rw [← Finset.univ_prod_mulSingle f]
  exact Finset.prod_induction _ _ mul one (by simp [mulSingle])

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

Goal state before:
pp: case cons
α : 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 ::ₘ s + t).antidiagonal = (a ::ₘ s).antidiagonal.bind fun p ↦ map (fun q ↦ (p.1 + q.1, p.2 + q.2)) t.antidiagonal

Tactic:
[

Goal state after:
case cons
α : 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 ::ₘ s + t).antidiagonal = (a ::ₘ s).antidiagonal.bind fun p ↦ map (fun q ↦ (p.1 + q.1, p.2 + q.2)) t.antidiagonal
Module: Mathlib.Data.Multiset.Antidiagonal

Goal state before:
pp: case cons
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
hs : s.antidiagonal = map (fun t ↦ (s - t, t)) s.powerset
⊢ (a ::ₘ s).antidiagonal = map (fun t ↦ (a ::ₘ s - t, t)) (a ::ₘ s).powerset

Tactic:
[

Goal state after:
case cons
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
hs : s.antidiagonal = map (fun t ↦ (s - t, t)) s.powerset
⊢ (a ::ₘ s).antidiagonal = map (fun t ↦ (a ::ₘ s - t, t)) (a ::ₘ s).powerset
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case pos
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
κ : ι → Type u_4
f : (i : ι) → κ i → α
h_indep : ∀ (i : ι), iSupIndep (f i)
s : Finset ((i : ι) → κ i)
ih : ∀ t ⊂ s, t.SupIndep fun k ↦ ⨅ i, f i (k i)
hs : 1 < s.card
k₁ k₂ : (i : ι) → κ i
left✝¹ : k₁ ∈ s
left✝ : k₂ ∈ s
h : k₁ ≠ k₂
i : ι
hi : k₁ i ≠ k₂ i
⊢ ∀ i_1 ∈ Finset.image (fun x ↦ x i) s, ({c ∈ s | c i = i_1}.sup fun k ↦ ⨅ i, f i (k i)) ≤ f i i_1

Tactic:
[

Goal state after:
case pos
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
κ : ι → Type u_4
f : (i : ι) → κ i → α
h_indep : ∀ (i : ι), iSupIndep (f i)
s : Finset ((i : ι) → κ i)
ih : ∀ t ⊂ s, t.SupIndep fun k ↦ ⨅ i, f i (k i)
hs : 1 < s.card
k₁ k₂ : (i : ι) → κ i
left✝¹ : k₁ ∈ s
left✝ : k₂ ∈ s
h : k₁ ≠ k₂
i : ι
hi : k₁ i ≠ k₂ i
⊢ ∀ i_1 ∈ Finset.image (fun x ↦ x i) s, ({c ∈ s | c i = i_1}.sup fun k ↦ ⨅ i, f i (k i)) ≤ f i i_1
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case refine_2
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
b c : α
hbc : b ≤ c
h : sSup {a | a ≤ c ∧ IsAtom a} = c
zorn : ∃ m, Maximal (fun x ↦ x ∈ {s | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a ∧ a ≤ c}) m
⊢ ∃ s, sSupIndep s ∧ Disjoint b (sSup s) ∧ b ⊔ sSup s = c ∧ ∀ ⦃a : α⦄, a ∈ s → IsAtom a

Tactic:
[

Goal state after:
case refine_2
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
b c : α
hbc : b ≤ c
h : sSup {a | a ≤ c ∧ IsAtom a} = c
zorn : ∃ m, Maximal (fun x ↦ x ∈ {s | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a ∧ a ≤ c}) m
⊢ ∃ s, sSupIndep s ∧ Disjoint b (sSup s) ∧ b ⊔ sSup s = c ∧ ∀ ⦃a : α⦄, a ∈ s → IsAtom a
Module: Mathlib.Algebra.BigOperators.Ring.Finset

Goal state before:
pp: ι : Type u_1
κ : Type u_2
R : Type u_4
inst✝ : NonUnitalNonAssocSemiring R
s : Finset ι
t : Finset κ
f : ι → R
g : κ → R
⊢ (∑ i ∈ s, f i) * ∑ j ∈ t, g j = ∑ i ∈ s, ∑ j ∈ t, f i * g j

Tactic:
[

Goal state after:
ι : Type u_1
κ : Type u_2
R : Type u_4
inst✝ : NonUnitalNonAssocSemiring R
s : Finset ι
t : Finset κ
f : ι → R
g : κ → R
⊢ (∑ i ∈ s, f i) * ∑ j ∈ t, g j = ∑ i ∈ s, ∑ j ∈ t, f i * g j
Module: Mathlib.Algebra.BigOperators.Ring.Finset

Goal state before:
pp: ι : Type u_1
κ : Type u_2
R : Type u_4
inst✝ : NonUnitalNonAssocSemiring R
s : Finset ι
t : Finset κ
f : ι → R
g : κ → R
⊢ (∑ i ∈ s, f i) * ∑ j ∈ t, g j = ∑ i ∈ s, ∑ j ∈ t, f i * g j

Tactic:
sum_mul,

Goal state after:
ι : Type u_1
κ : Type u_2
R : Type u_4
inst✝ : NonUnitalNonAssocSemiring R
s : Finset ι
t : Finset κ
f : ι → R
g : κ → R
⊢ ∑ i ∈ s, f i * ∑ j ∈ t, g j = ∑ i ∈ s, ∑ j ∈ t, f i * g j
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:
[

Goal state after:
ι : 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
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:
[

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 τ₁₂
f : M →ₛₗ[τ₁₂] M₂
p : Submodule R M
⊢ map f p = f.range ↔ Codisjoint p f.ker
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 ∧ f.range ≤ map f p ↔ Codisjoint p f.ker

Tactic:
LinearMap.map_le_range,

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 τ₁₂
f : M →ₛₗ[τ₁₂] M₂
p : Submodule R M
⊢ True ∧ f.range ≤ map f p ↔ Codisjoint p f.ker
Module: Mathlib.Algebra.BigOperators.Ring.Finset

Goal state before:
pp: case insert
ι : Type u_1
R : Type u_4
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
κ : ι → Type u_5
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → R
a : ι
s : Finset ι
ha : a ∉ s
ih : ∏ a ∈ s, ∑ b ∈ t a, f a b = ∑ p ∈ s.pi t, ∏ x ∈ s.attach, f (↑x) (p ↑x ⋯)
h₁ : ∀ x ∈ t a, ∀ y ∈ t a, x ≠ y → Disjoint (image (Pi.cons s a x) (s.pi t)) (image (Pi.cons s a y) (s.pi t))
⊢ (∑ b ∈ t a, f a b) * ∑ p ∈ s.pi t, ∏ x ∈ s.attach, f (↑x) (p ↑x ⋯) =
    ∑ p ∈ (t a).biUnion fun b ↦ image (Pi.cons s a b) (s.pi t), ∏ x ∈ (insert a s).attach, f (↑x) (p ↑x ⋯)

Tactic:
sum_mul,

Goal state after:
case insert
ι : Type u_1
R : Type u_4
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
κ : ι → Type u_5
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → R
a : ι
s : Finset ι
ha : a ∉ s
ih : ∏ a ∈ s, ∑ b ∈ t a, f a b = ∑ p ∈ s.pi t, ∏ x ∈ s.attach, f (↑x) (p ↑x ⋯)
h₁ : ∀ x ∈ t a, ∀ y ∈ t a, x ≠ y → Disjoint (image (Pi.cons s a x) (s.pi t)) (image (Pi.cons s a y) (s.pi t))
⊢ ∑ i ∈ t a, f a i * ∑ p ∈ s.pi t, ∏ x ∈ s.attach, f (↑x) (p ↑x ⋯) =
    ∑ p ∈ (t a).biUnion fun b ↦ image (Pi.cons s a b) (s.pi t), ∏ x ∈ (insert a s).attach, f (↑x) (p ↑x ⋯)
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 τ₁₂
p p' : Submodule R M
f : M →ₛₗ[τ₁₂] M₂
hab : p ≤ p'
h : p ⊔ f.ker < p' ⊔ f.ker
⊢ map f p < map f p'

Tactic:
[

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 τ₁₂
p p' : Submodule R M
f : M →ₛₗ[τ₁₂] M₂
hab : p ≤ p'
h : p ⊔ f.ker < p' ⊔ f.ker
⊢ map f p < map f p'
Module: Mathlib.Algebra.Group.Indicator

Goal state before:
pp: α : Type u_1
M : Type u_4
inst✝ : MulOneClass M
s t : Set α
a : α
h : ¬a ∈ s ∩ t
f : α → M
⊢ (s ∪ t).mulIndicator f a = s.mulIndicator f a * t.mulIndicator f a

Tactic:
← mulIndicator_union_mul_inter_apply f s t,

Goal state after:
α : Type u_1
M : Type u_4
inst✝ : MulOneClass M
s t : Set α
a : α
h : ¬a ∈ s ∩ t
f : α → M
⊢ (s ∪ t).mulIndicator f a = (s ∪ t).mulIndicator f a * (s ∩ t).mulIndicator f a
Module: Mathlib.Algebra.Group.Indicator

Goal state before:
pp: α : Type u_1
G : Type u_6
inst✝ : Group G
s t : Set α
h : s ⊆ t
f : α → G
⊢ (t \ s).mulIndicator f = t.mulIndicator f / s.mulIndicator f

Tactic:
rw [mulIndicator_sdiff h, div_eq_mul_inv]

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₂
hf : Surjective ⇑f
ι : Sort u_8
p : ι → Submodule R M
h : f.ker ≤ ⨅ i, p i
⊢ map f (⨅ i, p i) = map f (⨅ i, comap f (map f (p i)))

Tactic:
[

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 τ₁₂
f : M →ₛₗ[τ₁₂] M₂
hf : Surjective ⇑f
ι : Sort u_8
p : ι → Submodule R M
h : f.ker ≤ ⨅ i, p i
⊢ map f (⨅ i, p i) = map f (⨅ i, comap f (map f (p i)))
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}, (fun a_1 x ↦ a_1 ∈ {a_2 ∈ s | ∃ (h : a_2 ∈ s), a a_2 h}) = a

Tactic:
[

Goal state after:
ι : Type u_1
R : Type u_4
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
f g : ι → R
s : Finset ι
⊢ ∀ a ∈ s.pi fun x ↦ {True, False}, (fun a_1 x ↦ a_1 ∈ {a_2 ∈ s | ∃ (h : a_2 ∈ s), a a_2 h}) = a
Module: Mathlib.Data.Multiset.Find

Goal state before:
pp: case cons.isFalse
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
a x : α
s : Multiset α
ih : ∀ (hp : {x | x ∈ s ∧ p x}.Subsingleton), find? p s hp = some a ↔ a ∈ s ∧ p a
hp : {x_1 | x_1 ∈ x ::ₘ s ∧ p x_1}.Subsingleton
h✝ : ¬p x
⊢ find? p s ⋯ = some a ↔ a ∈ x ::ₘ s ∧ p a

Tactic:
[

Goal state after:
case cons.isFalse
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
a x : α
s : Multiset α
ih : ∀ (hp : {x | x ∈ s ∧ p x}.Subsingleton), find? p s hp = some a ↔ a ∈ s ∧ p a
hp : {x_1 | x_1 ∈ x ::ₘ s ∧ p x_1}.Subsingleton
h✝ : ¬p x
⊢ find? p s ⋯ = some a ↔ a ∈ x ::ₘ s ∧ p a
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.powerset, {x ∈ s | ∃ (_ : x ∈ s), x ∈ a} = a

Tactic:
[

Goal state after:
ι : Type u_1
R : Type u_4
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
f g : ι → R
s : Finset ι
⊢ ∀ a ∈ s.powerset, {x ∈ s | ∃ (_ : x ∈ s), x ∈ a} = a
Module: Mathlib.Data.Multiset.Find

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝² : DecidablePred p
p₁ p₂ : α → Prop
inst✝¹ : DecidablePred p₁
inst✝ : DecidablePred p₂
s : Multiset α
hp₁ : {x | x ∈ s ∧ p₁ x}.Subsingleton
h : ∀ (x : α), x ∈ s → (p₁ x ↔ p₂ x)
⊢ {x | x ∈ s ∧ p₂ x}.Subsingleton

Tactic:
[

Goal state after:
α : Type u_1
p : α → Prop
inst✝² : DecidablePred p
p₁ p₂ : α → Prop
inst✝¹ : DecidablePred p₁
inst✝ : DecidablePred p₂
s : Multiset α
hp₁ : {x | x ∈ s ∧ p₁ x}.Subsingleton
h : ∀ (x : α), x ∈ s → (p₁ x ↔ p₂ x)
⊢ {x | x ∈ s ∧ p₂ x}.Subsingleton
Module: Mathlib.Data.Finsupp.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_4
inst✝ : Zero M
f : α ↪ β
v : α →₀ M
a : α
⊢ (embDomain f v) (f a) = v a

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_4
inst✝ : Zero M
f : α ↪ β
v : α →₀ M
a : α
⊢ (embDomain f v) (f a) = v a
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✝³ : AddCommGroup M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
hf : f.range = ⊤
p : Submodule R M
⊢ map f p = ⊤ ↔ p ⊔ f.ker = ⊤

Tactic:
[

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✝³ : AddCommGroup M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
hf : f.range = ⊤
p : Submodule R M
⊢ map f p = ⊤ ↔ p ⊔ f.ker = ⊤
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
e : R
⊢ IsIdempotentElem (toSpanSingleton R R e) ↔ IsIdempotentElem e

Tactic:
[

Goal state after:
R : Type u_1
inst✝ : Semiring R
e : R
⊢ IsIdempotentElem (toSpanSingleton R R e) ↔ IsIdempotentElem e
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : Module.End R R
⊢ f (f 1) = f 1 ↔ ∀ (x : R), (f * f) x = f x

Tactic:
[

Goal state after:
R : Type u_1
inst✝ : Semiring R
f : Module.End R R
⊢ f (f 1) = f 1 ↔ ∀ (x : R), (f * f) x = f x
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 : Submodule R M
x : M
hx : x ∈ N
y : ↥N
⊢ y ∈ (R ∙ x).submoduleOf N ↔ y ∈ R ∙ ⟨x, hx⟩

Tactic:
[

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
x : M
hx : x ∈ N
y : ↥N
⊢ y ∈ (R ∙ x).submoduleOf N ↔ y ∈ R ∙ ⟨x, hx⟩
Module: Mathlib.Data.Finsupp.Single

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝¹ : Zero M
a a' : α
b : M
inst✝ : Decidable (a = a')
⊢ (single a b) a' = if a = a' then b else 0

Tactic:
[

Goal state after:
α : Type u_1
M : Type u_5
inst✝¹ : Zero M
a a' : α
b : M
inst✝ : Decidable (a = a')
⊢ (single a b) a' = if a = a' then b else 0
Module: Mathlib.Data.Finsupp.Single

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝¹ : Zero M
a a' : α
b : M
inst✝ : Decidable (a = a')
⊢ (single a b) a' = if a' = a then b else 0

Tactic:
single,

Goal state after:
α : Type u_1
M : Type u_5
inst✝¹ : Zero M
a a' : α
b : M
inst✝ : Decidable (a = a')
⊢ { support := if b = 0 then ∅ else {a}, toFun := Pi.single a b, mem_support_toFun := ⋯ } a' = if a' = a then b else 0
Module: Mathlib.Algebra.Group.Finsupp

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : AddCommMonoid M
k l m n : ι
u v : M
hu : u ≠ 0
hv : v ≠ 0
⊢ single k u + single l v = single m u + single n v ↔ k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u + v = 0 ∧ k = l ∧ m = n

Tactic:
[

Goal state after:
ι : Type u_1
M : Type u_3
inst✝ : AddCommMonoid M
k l m n : ι
u v : M
hu : u ≠ 0
hv : v ≠ 0
⊢ single k u + single l v = single m u + single n v ↔ k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u + v = 0 ∧ k = l ∧ m = n
Module: Mathlib.Algebra.Order.Group.Indicator

Goal state before:
pp: α : Type u_2
M : Type u_3
inst✝¹ : Zero M
inst✝ : LinearOrder M
s : Set α
f : α → M
a : α
⊢ s.indicator f a ≤ {a | 0 ≤ f a}.indicator f a

Tactic:
[

Goal state after:
α : Type u_2
M : Type u_3
inst✝¹ : Zero M
inst✝ : LinearOrder M
s : Set α
f : α → M
a : α
⊢ s.indicator f a ≤ {a | 0 ≤ f a}.indicator f a
Module: Mathlib.Algebra.Order.Group.Indicator

Goal state before:
pp: case neg
ι : Sort u_1
α : Type u_2
M : Type u_3
inst✝² : CompleteLattice M
inst✝¹ : One M
inst✝ : Nonempty ι
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
j : ι
hj : x ∉ s j
⊢ 1 = ⨅ i, (s i).mulIndicator f x

Tactic:
refine le_antisymm (by simp only [← h1, le_iInf_iff, bot_le, forall_const]) ?_

Goal state after:
case neg
ι : Sort u_1
α : Type u_2
M : Type u_3
inst✝² : CompleteLattice M
inst✝¹ : One M
inst✝ : Nonempty ι
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
j : ι
hj : x ∉ s j
⊢ ⨅ i, (s i).mulIndicator f x ≤ 1
Module: Mathlib.Algebra.GroupWithZero.Indicator

Goal state before:
pp: ι : Type u_1
M₀ : Type u_4
inst✝ : MulZeroClass M₀
s t : Set ι
f g : ι → M₀
i : ι
⊢ s.indicator (t.indicator fun j ↦ f j * g j) i = s.indicator f i * t.indicator g i

Tactic:
[

Goal state after:
ι : Type u_1
M₀ : Type u_4
inst✝ : MulZeroClass M₀
s t : Set ι
f g : ι → M₀
i : ι
⊢ s.indicator (t.indicator fun j ↦ f j * g j) i = s.indicator f i * t.indicator g i
Module: Mathlib.Algebra.GroupWithZero.Indicator

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M₀ : Type u_4
inst✝ : MulZeroOneClass M₀
s : Set ι
i : ι
t : Set κ
j : κ
⊢ (s ×ˢ t).indicator 1 (i, j) = s.indicator 1 i * t.indicator 1 j

Tactic:
[

Goal state after:
ι : Type u_1
κ : Type u_2
M₀ : Type u_4
inst✝ : MulZeroOneClass M₀
s : Set ι
i : ι
t : Set κ
j : κ
⊢ (s ×ˢ t).indicator 1 (i, j) = s.indicator 1 i * t.indicator 1 j
Module: Mathlib.Algebra.GroupWithZero.Indicator

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

Tactic:
[

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

Goal state before:
pp: case inr
M : Type u_3
M₂ : Type u_4
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup 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✝³ : DivisionRing R
inst✝² : DivisionRing S
inst✝¹ : Module R M
inst✝ : Module S M₂
x : M
n : ℕ
⊢ f ((↑(-↑n))⁻¹ • x) = (↑(-↑n))⁻¹ • f x

Tactic:
[

Goal state after:
case inr
M : Type u_3
M₂ : Type u_4
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup 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✝³ : DivisionRing R
inst✝² : DivisionRing S
inst✝¹ : Module R M
inst✝ : Module S M₂
x : M
n : ℕ
⊢ f ((↑(-↑n))⁻¹ • x) = (↑(-↑n))⁻¹ • f x
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_8
inst✝¹ : Fintype α
inst✝ : AddCommMonoid M
f : α →₀ M
⊢ ⇑(∑ a, single a (f a)) = ⇑f

Tactic:
[

Goal state after:
α : Type u_1
M : Type u_8
inst✝¹ : Fintype α
inst✝ : AddCommMonoid M
f : α →₀ M
⊢ ⇑(∑ a, single a (f a)) = ⇑f
Module: Mathlib.Algebra.Module.Basic

Goal state before:
pp: α : Type u_1
R : Type u_2
inst✝ : MulZeroOneClass R
s : Set α
r : R
a : α
⊢ r • s.indicator 1 a = s.indicator (fun x ↦ r) a

Tactic:
[

Goal state after:
α : Type u_1
R : Type u_2
inst✝ : MulZeroOneClass R
s : Set α
r : R
a : α
⊢ r • s.indicator 1 a = s.indicator (fun x ↦ r) a
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_8
inst✝¹ : AddCommMonoid M
inst✝ : Fintype α
i : α
m : M
⊢ ∑ j, (single i m) j = m

Tactic:
single,

Goal state after:
α : Type u_1
M : Type u_8
inst✝¹ : AddCommMonoid M
inst✝ : Fintype α
i : α
m : M
⊢ ∑ j, { support := if m = 0 then ∅ else {i}, toFun := Pi.single i m, mem_support_toFun := ⋯ } j = m
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_8
inst✝¹ : AddCommMonoid M
inst✝ : Fintype α
i : α
m : M
⊢ ∑ j, (single j m) i = m

Tactic:
[

Goal state after:
α : Type u_1
M : Type u_8
inst✝¹ : AddCommMonoid M
inst✝ : Fintype α
i : α
m : M
⊢ ∑ j, (single j m) i = m
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_8
inst✝¹ : AddCommMonoid M
inst✝ : Fintype α
i : α
m : M
⊢ ∑ j, (single j m) i = m

Tactic:
single,

Goal state after:
α : Type u_1
M : Type u_8
inst✝¹ : AddCommMonoid M
inst✝ : Fintype α
i : α
m : M
⊢ ∑ j, { support := if m = 0 then ∅ else {j}, toFun := Pi.single j m, mem_support_toFun := ⋯ } i = m
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_7
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
v : α →₀ M
f : α ↪ β
g : β → M → N
⊢ ∏ x ∈ v.support, g (f x) ((embDomain f v) (f x)) = ∏ a ∈ v.support, g (f a) (v a)

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_7
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
v : α →₀ M
f : α ↪ β
g : β → M → N
⊢ ∏ x ∈ v.support, g (f x) ((embDomain f v) (f x)) = ∏ a ∈ v.support, g (f a) (v a)
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_8
inst✝¹ : AddCommMonoid M
f1 f2 : α →₀ M
hd : Disjoint f1.support f2.support
β : Type u_16
inst✝ : CommMonoid β
g : α → M → β
this : ∀ {f1 f2 : α →₀ M}, Disjoint f1.support f2.support → ∏ x ∈ f1.support, g x (f1 x + f2 x) = f1.prod g
⊢ (f1 + f2).prod g = f1.prod g * f2.prod g

Tactic:
[

Goal state after:
α : Type u_1
M : Type u_8
inst✝¹ : AddCommMonoid M
f1 f2 : α →₀ M
hd : Disjoint f1.support f2.support
β : Type u_16
inst✝ : CommMonoid β
g : α → M → β
this : ∀ {f1 f2 : α →₀ M}, Disjoint f1.support f2.support → ∏ x ∈ f1.support, g x (f1 x + f2 x) = f1.prod g
⊢ (f1 + f2).prod g = f1.prod g * f2.prod g