mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Notation.Indicator

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : One M
s : Set α
f : α → M
a : α
t : Set β
g : β → M
b : β
h1 : a ∈ s ↔ b ∈ t
h2 : f a = g b
h✝ : ¬a ∈ s
⊢ s.mulIndicator f a = t.mulIndicator g b

Tactic:
simp_all

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

Goal state before:
pp: ι : Type u_1
M₀ : Type u_4
inst✝² : CommMonoidWithZero M₀
f : ι → M₀
s : Finset ι
inst✝¹ : Nontrivial M₀
inst✝ : NoZeroDivisors M₀
⊢ ∏ x ∈ s, f x = 0 ↔ ∃ a ∈ s, f a = 0

Tactic:
by
  classical
    induction s using Finset.induction_on with
    | empty => exact ⟨Not.elim one_ne_zero, fun ⟨_, H, _⟩ => by simp at H⟩
    | insert _ _ ha ih => rw [prod_insert ha, mul_eq_zero, exists_mem_insert, ih]

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
inst✝³ : Semiring S
inst✝² : SMul R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
p : Submodule R M
q : Submodule S M
h₁ : p ≤ restrictScalars R q
h₂ : q ≤ span S ↑p
⊢ map q.subtype (span S (range ⇑(inclusion h₁))) = q

Tactic:
rw [map_span]

Goal state after:
R : Type u_1
M : Type u_4
S : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Semiring S
inst✝² : SMul R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
p : Submodule R M
q : Submodule S M
h₁ : p ≤ restrictScalars R q
h₂ : q ≤ span S ↑p
⊢ span S (⇑q.subtype '' range ⇑(inclusion h₁)) = q
Module: Mathlib.Algebra.BigOperators.Pi

Goal state before:
pp: case intro
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)
val✝ : Fintype I
k : (i : I) → M i
⊢ ∏ x, g (Pi.mulSingle x (k x)) = h (∏ i, Pi.mulSingle i (k i))

Tactic:
map_prod

Goal state after:
case intro
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)
val✝ : Fintype I
k : (i : I) → M i
⊢ ∏ x, g (Pi.mulSingle x (k x)) = ∏ x, h (Pi.mulSingle x (k x))
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
⊢ map (fun x ↦ (s - x, a ::ₘ x)) s.powerset + map (fun x ↦ (a ::ₘ (s - x), x)) s.powerset =
    map (fun x ↦ (a ::ₘ s - x, x)) s.powerset + map (fun x ↦ (a ::ₘ s - a ::ₘ x, a ::ₘ x)) s.powerset

Tactic:
sub_cons,

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

Goal state before:
pp: case refine_2.refine_1
α : 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
⊢ b ⊔ sSup s ≤ c

Tactic:
simp_all

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
⊢ map f p = f.range ↔ Codisjoint p f.ker

Tactic:
le_antisymm_iff,

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 ∧ f.range ≤ map f p ↔ Codisjoint p f.ker
Module: Mathlib.Algebra.Group.Indicator

Goal state before:
pp: case pos
α : Type u_1
M : Type u_4
inst✝¹ : MulOneClass M
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
f g : α → M
x : α
h : x ∈ s
⊢ (s.mulIndicator f * sᶜ.mulIndicator g) x = s.piecewise f g x

Tactic:
piecewise_eq_of_mem _ _ _ h,

Goal state after:
case pos
α : Type u_1
M : Type u_4
inst✝¹ : MulOneClass M
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
f g : α → M
x : α
h : x ∈ s
⊢ (s.mulIndicator f * sᶜ.mulIndicator g) x = f x
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
g : α →₀ N
f : α → M
h : ∀ (i : α), e (f i) = g i
⊢ ∀ (a : α), (if a ∈ g.support then f a else 0) ≠ 0 → a ∈ g.support

Tactic:
simp_all

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

Goal state before:
pp: K : Type u_3
V : Type u_6
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x : V
s q : Submodule K V
hpq : s < q
hqp : q < K ∙ x ⊔ s
c : K
z : V
hz : z ∈ s
hyq : c • x ∈ q
hyp : c • x + z ∉ s
hc : c ≠ 0
⊢ x ∈ q

Tactic:
q.smul_mem_iff hc

Goal state after:
K : Type u_3
V : Type u_6
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x : V
s q : Submodule K V
hpq : s < q
hqp : q < K ∙ x ⊔ s
c : K
z : V
hz : z ∈ s
hyq : x ∈ q
hyp : c • x + z ∉ s
hc : c ≠ 0
⊢ x ∈ q
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 : M
⊢ toSpanSingleton R M x = 0 ↔ x = 0

Tactic:
by
  rw [← toSpanSingleton_zero, (toSpanSingleton_injective R M).eq_iff]

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

Goal state before:
pp: case inl
ι : Type u_1
M : Type u_3
inst✝¹ : AddZeroClass M
g₁ g₂ : ι →₀ M
inst✝ : DecidableEq ι
h : Disjoint g₁.support g₂.support
a : ι
ha : a ∈ g₁.support ∪ g₂.support
h✝ : a ∈ g₁.support ∧ a ∉ g₂.support
⊢ a ∈ (g₁ + g₂).support

Tactic:
simp_all

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

Goal state before:
pp: case inr
ι : Type u_1
M : Type u_3
inst✝¹ : AddZeroClass M
g₁ g₂ : ι →₀ M
inst✝ : DecidableEq ι
h : Disjoint g₁.support g₂.support
a : ι
ha : a ∈ g₁.support ∪ g₂.support
h✝ : a ∈ g₂.support ∧ a ∉ g₁.support
⊢ a ∈ (g₁ + g₂).support

Tactic:
simp_all

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

Goal state before:
pp: case neg
ι : Type u_1
M : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : DecidableEq ι
f g : ι →₀ M
h : ∀ x ∈ f.support ∩ g.support, AddCommute (f x) (g x)
x : ι
hf : x ∈ f.support
hg : x ∉ g.support
⊢ (f + g) x = (g + f) x

Tactic:
simp_all

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

Goal state before:
pp: case neg
ι : Type u_1
M : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : DecidableEq ι
f g : ι →₀ M
h : ∀ x ∈ f.support ∩ g.support, AddCommute (f x) (g x)
x : ι
hf : x ∉ f.support
⊢ (f + g) x = (g + f) x

Tactic:
simp_all

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : AddZeroClass M
motive : (ι →₀ M) → Prop
f : ι →₀ M
zero : motive 0
add_single : ∀ (a : ι) (b : M) (f : ι →₀ M), a ∉ f.support → b ≠ 0 → motive f → motive (f + single a b)
a✝⁵ : ι
a✝⁴ : M
a✝³ : ι →₀ M
a✝² : a✝⁵ ∉ a✝³.support
a✝¹ : a✝⁴ ≠ 0
a✝ : motive a✝³
⊢ Disjoint (single a✝⁵ a✝⁴).support a✝³.support

Tactic:
simp_all

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

Goal state before:
pp: case pos
ι : 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 : α
hx : x ∈ ⋂ i, s i
⊢ (⋂ i, s i).mulIndicator f x = ⨅ i, (s i).mulIndicator f x

Tactic:
simp_all

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
N : Type u_16
inst✝ : AddCommMonoid N
f : α →₀ N
a : α
⊢ (f.sum fun x v ↦ if a = x then v else 0) = f a

Tactic:
simp_all

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
N : Type u_16
inst✝ : AddCommMonoid N
f : α →₀ N
a : α
⊢ (f.sum fun x v ↦ if a = x then v else 0) = f a

Tactic:
by
  simp_all

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

Goal state before:
pp: case add
α : Type u_1
M : Type u_2
N : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : CommMonoid N
b : Option α → M → N
h_zero : ∀ (o : Option α), b o 0 = 1
h_add : ∀ (o : Option α) (m₁ m₂ : M), b o (m₁ + m₂) = b o m₁ * b o m₂
f₁ f₂ : Option α →₀ M
h₁ : f₁.prod b = b none (f₁ none) * f₁.some.prod fun a ↦ b (Option.some a)
h₂ : f₂.prod b = b none (f₂ none) * f₂.some.prod fun a ↦ b (Option.some a)
⊢ (b none (f₁ none) * f₁.some.prod fun a ↦ b (Option.some a)) * f₂.prod b =
    b none ((f₁ + f₂) none) * (f₁ + f₂).some.prod fun a ↦ b (Option.some a)

pp: case add.h_zero
α : Type u_1
M : Type u_2
N : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : CommMonoid N
b : Option α → M → N
h_zero : ∀ (o : Option α), b o 0 = 1
h_add : ∀ (o : Option α) (m₁ m₂ : M), b o (m₁ + m₂) = b o m₁ * b o m₂
f₁ f₂ : Option α →₀ M
h₁ : f₁.prod b = b none (f₁ none) * f₁.some.prod fun a ↦ b (Option.some a)
h₂ : f₂.prod b = b none (f₂ none) * f₂.some.prod fun a ↦ b (Option.some a)
⊢ ∀ a ∈ f₁.support ∪ f₂.support, b a 0 = 1

pp: case add.h_add
α : Type u_1
M : Type u_2
N : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : CommMonoid N
b : Option α → M → N
h_zero : ∀ (o : Option α), b o 0 = 1
h_add : ∀ (o : Option α) (m₁ m₂ : M), b o (m₁ + m₂) = b o m₁ * b o m₂
f₁ f₂ : Option α →₀ M
h₁ : f₁.prod b = b none (f₁ none) * f₁.some.prod fun a ↦ b (Option.some a)
h₂ : f₂.prod b = b none (f₂ none) * f₂.some.prod fun a ↦ b (Option.some a)
⊢ ∀ a ∈ f₁.support ∪ f₂.support, ∀ (b₁ b₂ : M), b a (b₁ + b₂) = b a b₁ * b a b₂

Tactic:
h₂,

Goal state after:
case add
α : Type u_1
M : Type u_2
N : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : CommMonoid N
b : Option α → M → N
h_zero : ∀ (o : Option α), b o 0 = 1
h_add : ∀ (o : Option α) (m₁ m₂ : M), b o (m₁ + m₂) = b o m₁ * b o m₂
f₁ f₂ : Option α →₀ M
h₁ : f₁.prod b = b none (f₁ none) * f₁.some.prod fun a ↦ b (Option.some a)
h₂ : f₂.prod b = b none (f₂ none) * f₂.some.prod fun a ↦ b (Option.some a)
⊢ (b none (f₁ none) * f₁.some.prod fun a ↦ b (Option.some a)) *
      (b none (f₂ none) * f₂.some.prod fun a ↦ b (Option.some a)) =
    b none ((f₁ + f₂) none) * (f₁ + f₂).some.prod fun a ↦ b (Option.some a)

case add.h_zero
α : Type u_1
M : Type u_2
N : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : CommMonoid N
b : Option α → M → N
h_zero : ∀ (o : Option α), b o 0 = 1
h_add : ∀ (o : Option α) (m₁ m₂ : M), b o (m₁ + m₂) = b o m₁ * b o m₂
f₁ f₂ : Option α →₀ M
h₁ : f₁.prod b = b none (f₁ none) * f₁.some.prod fun a ↦ b (Option.some a)
h₂ : f₂.prod b = b none (f₂ none) * f₂.some.prod fun a ↦ b (Option.some a)
⊢ ∀ a ∈ f₁.support ∪ f₂.support, b a 0 = 1

case add.h_add
α : Type u_1
M : Type u_2
N : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : CommMonoid N
b : Option α → M → N
h_zero : ∀ (o : Option α), b o 0 = 1
h_add : ∀ (o : Option α) (m₁ m₂ : M), b o (m₁ + m₂) = b o m₁ * b o m₂
f₁ f₂ : Option α →₀ M
h₁ : f₁.prod b = b none (f₁ none) * f₁.some.prod fun a ↦ b (Option.some a)
h₂ : f₂.prod b = b none (f₂ none) * f₂.some.prod fun a ↦ b (Option.some a)
⊢ ∀ a ∈ f₁.support ∪ f₂.support, ∀ (b₁ b₂ : M), b a (b₁ + b₂) = b a b₁ * b a b₂
Module: Mathlib.Algebra.FiniteSupport.Basic

Goal state before:
pp: α : Type u_1
M : Type u_4
inst✝ : Monoid M
f : α → M
g : α → ℕ
hg : HasFiniteSupport g
a : α
ha : a ∉ support g
⊢ a ∉ mulSupport fun a ↦ f a ^ g a

Tactic:
simp_all

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

Goal state before:
pp: α : Type u_1
M : Type u_8
inst✝ : AddCommMonoid M
s : Finset α
f : (a : α) → a ∈ s → M
⊢ ∀ x ∈ s, x ∉ (indicator s f).support → single x ((indicator s f) x) = 0

Tactic:
· intro i _ hi
    rw [notMem_support_iff.mp hi, single_zero]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
G : Type u_8
H : Type u_9
R : Type u_10
S : Type u_11
inst✝ : Zero M
f : α ≃ β
l : α →₀ M
a : β
⊢ a ∈ map f.toEmbedding l.support ↔ l (f.symm a) ≠ 0

Tactic:
simp only [Finset.mem_map_equiv, mem_support_toFun]

Goal state after:
α : 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
f : α ≃ β
l : α →₀ M
a : β
⊢ l.toFun (f.symm a) ≠ 0 ↔ l (f.symm a) ≠ 0
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: case h₁
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
hf : Injective f
x : α →₀ M
a : α
a✝ : x a = 0
⊢ 0 (f a) = 0

Tactic:
Pi.zero_apply

Goal state after:
case h₁
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
hf : Injective f
x : α →₀ M
a : α
a✝ : x a = 0
⊢ 0 = 0
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
x : α →₀ M
b : β
h : b ∉ Set.range f
⊢ (mapDomain f x) b = 0

Tactic:
exact mapDomain_of_notMem_range _ _ h

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
S : Set α
f : α → β
hf : Set.InjOn f S
v₁ : α →₀ M
hv₁ : v₁ ∈ {w | ↑w.support ⊆ S}
v₂ : α →₀ M
hv₂ : v₂ ∈ {w | ↑w.support ⊆ S}
eq : mapDomain f v₁ = mapDomain f v₂
a : α
h : a ∉ v₁.support ∪ v₂.support
⊢ v₁ a = v₂ a

Tactic:
simp_all

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

Goal state before:
pp: case h₂
α : Type u_1
M : Type u_5
inst✝¹ : Zero M
inst✝ : DecidableEq α
f : α →₀ M
a a✝¹ : α
a✝ : a = a✝¹
⊢ a✝¹ = a

Tactic:
simp_all

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
x : α
f : α →₀ M
h : x ∈ f.support
⊢ f x ∈ f.frange

Tactic:
simp_all

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
x : α
f : α →₀ M
h : x ∈ f.support
⊢ f x ∈ f.frange

Tactic:
by
  simp_all

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
G : Type u_8
H : Type u_9
R : Type u_10
S : Type u_11
inst✝ : Zero M
p✝ p : α → Prop
f : α →₀ M
a : Subtype p
⊢ a ∈ Finset.subtype p f.support ↔ (⇑f ∘ Subtype.val) a ≠ 0

Tactic:
simp only [@mem_subtype _ _ (Classical.decPred p), mem_support_iff]; rfl

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

Goal state before:
pp: case h1
ι : Type u_1
R : Type u_2
inst✝² : CommSemiring R
inst✝¹ : PartialOrder R
inst✝ : CanonicallyOrderedAdd R
f g h : ι → R
s : Finset ι
i : ι
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ j ∈ s, j ≠ i → g j ≤ f j
hhf : ∀ j ∈ s, j ≠ i → h j ≤ f j
j : ι
hj : j ∈ s \ {i}
⊢ g j ≤ f j

Tactic:
simp_all

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

Goal state before:
pp: case h1
ι : Type u_1
R : Type u_2
inst✝² : CommSemiring R
inst✝¹ : PartialOrder R
inst✝ : CanonicallyOrderedAdd R
f g h : ι → R
s : Finset ι
i : ι
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ j ∈ s, j ≠ i → g j ≤ f j
hhf : ∀ j ∈ s, j ≠ i → h j ≤ f j
j : ι
hj : j ∈ s \ {i}
⊢ h j ≤ f j

Tactic:
simp_all

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : Zero M
f : α × β →₀ M
p : α → Prop
inst✝ : DecidablePred p
⊢ (filter (fun a ↦ p a.1) f).curry = filter p f.curry

Tactic:
ext a b
  simp [filter_apply, apply_ite (DFunLike.coe · b)]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M✝ : Type u_5
N : Type u_6
P✝ : Type u_7
G : Type u_8
H : Type u_9
R : Type u_10
S : Type u_11
M : Type u_12
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
f : Subtype P →₀ M
g : { a // ¬P a } →₀ M
a : α
⊢ a ∈ (map (Embedding.subtype P) f.support).disjUnion (map (Embedding.subtype fun a ↦ ¬P a) g.support) ⋯ ↔
    (if h : P a then f ⟨a, h⟩ else g ⟨a, h⟩) ≠ 0

Tactic:
by_cases ha : P a <;> simp [ha]

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

Goal state before:
pp: α : Type u_1
M : Type u_3
R : Type u_6
inst✝⁴ : Semiring R
inst✝³ : IsDomain R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.IsTorsionFree R M
b : R
hb : b ≠ 0
g : α →₀ M
a : α
⊢ a ∈ (b • g).support ↔ a ∈ g.support

Tactic:
simp [Finsupp.smul_apply, hb]

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

Goal state before:
pp: n : ℕ
i : Fin n
⊢ val '' Iic i = Iic ↑i

Tactic:
rw [← preimage_val_Iic_val, image_preimage_eq_of_subset]
  simp [range_val]

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

Goal state before:
pp: n : ℕ
i : Fin n
⊢ rev ⁻¹' Iio i = Ioi i.rev

Tactic:
ext; simp [rev_lt_iff]

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

Goal state before:
pp: M : Type u_7
α : Type u_8
inst✝³ : CommMonoidWithZero M
inst✝² : PartialOrder M
inst✝¹ : ZeroLEOneClass M
inst✝ : PosMulMono M
⊢ ∏ᶠ (x : α), 0 ≤ 1

Tactic:
← finprod_one (α := α)

Goal state after:
M : Type u_7
α : Type u_8
inst✝³ : CommMonoidWithZero M
inst✝² : PartialOrder M
inst✝¹ : ZeroLEOneClass M
inst✝ : PosMulMono M
⊢ ∏ᶠ (x : α), 0 ≤ ∏ᶠ (x : α), 1
Module: Mathlib.LinearAlgebra.Basis.Defs

Goal state before:
pp: ι : Type u_10
R : Type u_11
M : Type u_12
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
x : M
i✝ : ι
a✝ : Nontrivial R
i j : ι
⊢ (single ⟨b i, ⋯⟩ 1) ⟨b j, ⋯⟩ = (single i 1) j

Tactic:
apply Finsupp.single_apply_left (f := fun i => (⟨b i, _⟩ : Set.range b))

Goal state after:
ι : Type u_10
R : Type u_11
M : Type u_12
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
x : M
i✝ : ι
a✝ : Nontrivial R
i j : ι
⊢ Injective fun i ↦ ⟨b 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
v : α → M
inst✝ : DecidableEq α
i : α
r : R
⊢ ∑ x, (if x = i then r else 0) • v x = r • v i

Tactic:
ite_smul,

Goal state after:
α : Type u_1
M : Type u_2
R : Type u_3
inst✝⁴ : Fintype α
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
v : α → M
inst✝ : DecidableEq α
i : α
r : R
⊢ (∑ x, if x = i then r • v x else 0 • v x) = r • v i
Module: Mathlib.LinearAlgebra.Basis.Defs

Goal state before:
pp: ι : Type u_10
R : Type u_11
M : Type u_12
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
i : ι
f : ι →₀ R
⊢ (b.coord i) (b.repr.symm f) = f i

Tactic:
simp only [repr_symm_apply, coord_apply, repr_linearCombination]

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

Goal state before:
pp: n : ℕ
j : Fin n
p : Fin n → Prop
inst✝ : DecidablePred p
hp : ∀ (i j : Fin n), j ≤ i → p i → p j
h1 : ∀ (k : Fin n), ¬p k → #{i | p i} ≤ ↑k
h : p j
hc : #{i | p i} ≤ ↑j
q : Fin n → Prop := fun x ↦ ↑x < #{i | p i}
⊢ #(filter p univ) ≤ #(filter q univ)

Tactic:
rw [card_filter_val_lt]; grind

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

Goal state before:
pp: α : Type u_1
ι : Type u_3
M : Type u_5
inst✝ : CommMonoid M
f : α → M
I : Set ι
t : ι → Set α
h : I.PairwiseDisjoint t
hI : I.Finite
ht : ∀ i ∈ I, (t i).Finite
this : Fintype ↑I
⊢ ∏ᶠ (a : α) (_ : a ∈ ⋃ x ∈ I, t x), f a = ∏ᶠ (i : ι) (_ : i ∈ I) (j : α) (_ : j ∈ t i), f j

Tactic:
rw [biUnion_eq_iUnion, finprod_mem_iUnion, ← finprod_set_coe_eq_finprod_mem]

Goal state after:
case h
α : Type u_1
ι : Type u_3
M : Type u_5
inst✝ : CommMonoid M
f : α → M
I : Set ι
t : ι → Set α
h : I.PairwiseDisjoint t
hI : I.Finite
ht : ∀ i ∈ I, (t i).Finite
this : Fintype ↑I
⊢ Pairwise (Disjoint on fun x ↦ t ↑x)

case ht
α : Type u_1
ι : Type u_3
M : Type u_5
inst✝ : CommMonoid M
f : α → M
I : Set ι
t : ι → Set α
h : I.PairwiseDisjoint t
hI : I.Finite
ht : ∀ i ∈ I, (t i).Finite
this : Fintype ↑I
⊢ ∀ (i : ↑I), (t ↑i).Finite
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: case pos
α : Type u_1
R : Type u_7
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NoZeroDivisors R
f : α → R
r : R
hr : r = 0
⊢ r * ∑ᶠ (a : α), f a = ∑ᶠ (a : α), r * f a

Tactic:
simp_all

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

Goal state before:
pp: case pos
α : Type u_1
R : Type u_7
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NoZeroDivisors R
s : Set α
f : α → R
r : R
a : α
h : a ∈ s
⊢ r * ∑ᶠ (_ : a ∈ s), f a = ∑ᶠ (_ : a ∈ s), r * f a

Tactic:
simp_all

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

Goal state before:
pp: case neg
α : Type u_1
R : Type u_7
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NoZeroDivisors R
s : Set α
f : α → R
r : R
a : α
h : a ∉ s
⊢ r * ∑ᶠ (_ : a ∈ s), f a = ∑ᶠ (_ : a ∈ s), r * f a

Tactic:
simp_all

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

Goal state before:
pp: case pos
α : Type u_1
R : Type u_7
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NoZeroDivisors R
f : α → R
r : R
hr : r = 0
⊢ (∑ᶠ (a : α), f a) * r = ∑ᶠ (a : α), f a * r

Tactic:
simp_all

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

Goal state before:
pp: case pos
α : Type u_1
R : Type u_7
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NoZeroDivisors R
s : Set α
f : α → R
r : R
a : α
h : a ∈ s
⊢ (∑ᶠ (_ : a ∈ s), f a) * r = ∑ᶠ (_ : a ∈ s), f a * r

Tactic:
simp_all

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

Goal state before:
pp: case neg
α : Type u_1
R : Type u_7
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NoZeroDivisors R
s : Set α
f : α → R
r : R
a : α
h : a ∉ s
⊢ (∑ᶠ (_ : a ∈ s), f a) * r = ∑ᶠ (_ : a ∈ s), f a * r

Tactic:
simp_all

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝² : CommMonoid M
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset (α × β)
f : α × β → M
this : ∀ (a : α), ∏ i ∈ Finset.image Prod.snd ({ab ∈ s | ab.1 = a}), f (a, i) = {x ∈ s | x.1 = a}.prod f
⊢ ∏ᶠ (ab : α × β) (_ : ab ∈ s), f ab =
    ∏ᶠ (a : α) (b : β) (_ : b ∈ Finset.image Prod.snd ({ab ∈ s | ab.1 = a})), f (a, b)

Tactic:
rw [finprod_mem_finset_eq_prod]

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝² : CommMonoid M
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset (α × β)
f : α × β → M
this : ∀ (a : α), ∏ i ∈ Finset.image Prod.snd ({ab ∈ s | ab.1 = a}), f (a, i) = {x ∈ s | x.1 = a}.prod f
⊢ ∏ i ∈ s, f i = ∏ᶠ (a : α) (b : β) (_ : b ∈ Finset.image Prod.snd ({ab ∈ s | ab.1 = a})), f (a, b)
Module: Mathlib.Logic.Equiv.Fin.Rotate

Goal state before:
pp: n : ℕ
k i : Fin n
⊢ (fun i ↦ i - k) ((fun i ↦ i + k) i) = i

Tactic:
by have := NeZero.of_pos k.pos; simp

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Rotate

Goal state before:
pp: n : ℕ
k i : Fin n
⊢ (fun i ↦ i + k) ((fun i ↦ i - k) i) = i

Tactic:
by have := NeZero.of_pos k.pos; simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
f : α × β → M
hf : HasFiniteMulSupport f
h₁ : ∀ (a : α × β), ∏ᶠ (_ : a ∈ Finite.toFinset hf), f a = f a
h₂ : ∏ᶠ (a : α × β), f a = ∏ᶠ (a : α × β) (_ : a ∈ Finite.toFinset hf), f a
⊢ ∏ᶠ (ab : α × β), f ab = ∏ᶠ (a : α) (b : β), f (a, b)

Tactic:
h₂,

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
f : α × β → M
hf : HasFiniteMulSupport f
h₁ : ∀ (a : α × β), ∏ᶠ (_ : a ∈ Finite.toFinset hf), f a = f a
h₂ : ∏ᶠ (a : α × β), f a = ∏ᶠ (a : α × β) (_ : a ∈ Finite.toFinset hf), f a
⊢ ∏ᶠ (a : α × β) (_ : a ∈ Finite.toFinset hf), f a = ∏ᶠ (a : α) (b : β), f (a, b)
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: x y : ℕ∞
h : x ≠ 0
⊢ 0 < x ^ y

Tactic:
rw [← Order.one_le_iff_pos]

Goal state after:
x y : ℕ∞
h : x ≠ 0
⊢ 1 ≤ x ^ y