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 α
a : α
f : α → β → M
b : β
h : ¬a ∈ s
⊢ s.mulIndicator f a b = s.mulIndicator (fun i ↦ f i b) a

Tactic:
simp [h]

Goal state after:
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
⊢ (U.mulIndicator fun x ↦ a) ⁻¹' s ∈ {univ, U, Uᶜ, ∅}

Tactic:
rw [mulIndicator_const_preimage_eq_union]
    split_ifs <;> simp

Goal state after:
Module: Mathlib.Data.FunLike.IsApply

Goal state before:
pp: case mpr
F : Type u_3
α : Type u_5
β : Type u_6
inst✝³ : FunLike F α β
inst✝² : One F
inst✝¹ : One β
inst✝ : IsOneApply F α β
f : F
h : f = 1
⊢ ⇑f = 1

Tactic:
simp [h]

Goal state after:
Module: Mathlib.Data.FunLike.IsApply

Goal state before:
pp: case mpr
F' : Type u_4
α : Type u_5
inst✝² : FunLike F' α α
inst✝¹ : One F'
inst✝ : IsOneApplyEqSelf F' α
f : F'
h : f = 1
⊢ ⇑f = id

Tactic:
simp [h]

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

Goal state before:
pp: case neg
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a : α
s : Set α
h : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
hs : ¬s.Nonempty
⊢ ∀ (c : α), IsCompactElement c → c ≤ a ⊓ sSup s → c ≤ ⨆ b ∈ s, a ⊓ b

Tactic:
· rw [Set.not_nonempty_iff_eq_empty] at hs
        simp [hs]

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

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

Tactic:
exact ⟨ha, Set.Subset.trans ht sdiff_subset⟩

Goal state after:
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
⊢ s.SupIndep fun k ↦ ⨅ i, f i (k i)

pp: case neg
α : 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
⊢ s.SupIndep fun k ↦ ⨅ i, f i (k i)

Tactic:
swap

Goal state after:
case neg
α : 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
⊢ s.SupIndep fun k ↦ ⨅ i, f i (k i)

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
⊢ s.SupIndep fun k ↦ ⨅ i, f i (k i)
Module: Mathlib.Algebra.BigOperators.Ring.Multiset

Goal state before:
pp: R : Type u_4
inst✝ : NonUnitalSemiring R
s✝ : Multiset R
a x : R
s : Multiset R
ih : (∀ (x : R), x ∈ s → a ∣ x) → a ∣ s.sum
h : ∀ (x_1 : R), x_1 ∈ x ::ₘ s → a ∣ x_1
⊢ a ∣ x + s.sum

Tactic:
exact dvd_add (h _ (mem_cons_self _ _)) (ih fun y hy ↦ h _ <| mem_cons.2 <| Or.inr hy)

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_9
s : Set ι
p : ι → Submodule R M
x✝¹ : ↥(⨆ i ∈ s, p i)
x : M
hx : x ∈ ⨆ i ∈ s, p i
x✝ : ⟨x, hx⟩ ∈ ⊤
this : ∀ i ∈ s, map (⨆ i ∈ s, p i).subtype (comap (⨆ i ∈ s, p i).subtype (p i)) = p i
⊢ x ∈ map (⨆ i ∈ s, p i).subtype (⨆ i ∈ s, comap (⨆ i ∈ s, p i).subtype (p i))

Tactic:
simpa only [map_iSup, biSup_congr this]

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

pp: case refine_1
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
b c✝ : α
hbc : b ≤ c✝
h : sSup {a | a ≤ c✝ ∧ IsAtom a} = c✝
c : Set (Set α)
hc1 : c ⊆ {s | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a ∧ a ≤ c✝}
hc2 : IsChain (fun x1 x2 ↦ x1 ⊆ x2) c
⊢ Disjoint b (sSup (⋃₀ c))

Tactic:
swap

Goal state after:
case refine_1
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
b c✝ : α
hbc : b ≤ c✝
h : sSup {a | a ≤ c✝ ∧ IsAtom a} = c✝
c : Set (Set α)
hc1 : c ⊆ {s | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a ∧ a ≤ c✝}
hc2 : IsChain (fun x1 x2 ↦ x1 ⊆ x2) c
⊢ Disjoint b (sSup (⋃₀ c))

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.LinearAlgebra.Span.Basic

Goal state before:
pp: R : Type u_8
M : Type u_9
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s t p : Submodule R M
hsp : s ≤ p
hnsp : -s ≤ p
x : M
⊢ x ∈ (s ⊔ t) ⊓ p ↔ x ∈ s ⊔ t ⊓ p

Tactic:
simp only [mem_sup, mem_inf]

Goal state after:
R : Type u_8
M : Type u_9
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s t p : Submodule R M
hsp : s ≤ p
hnsp : -s ≤ p
x : M
⊢ (∃ y ∈ s, ∃ z ∈ t, y + z = x) ∧ x ∈ p ↔ ∃ y ∈ s, ∃ z, (z ∈ t ∧ z ∈ p) ∧ y + z = x
Module: Mathlib.Algebra.BigOperators.Ring.Finset

Goal state before:
pp: ι : Type u_1
M : Type u_3
s : Finset ι
inst✝¹ : CommMonoid M
inst✝ : HasDistribNeg M
f : ι → M
⊢ ∏ x ∈ s, -f x = (-1) ^ #s * ∏ x ∈ s, f x

Tactic:
simpa using (s.1.map f).prod_map_neg

Goal state after:
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
⊢ (fun i ↦ (t \ s).mulIndicator f i * s.mulIndicator f i) = t.mulIndicator f

Tactic:
← mulIndicator_union_of_disjoint,

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

case h
α : Type u_1
G : Type u_6
inst✝ : Group G
s t : Set α
h : s ⊆ t
f : α → G
⊢ Disjoint (t \ s) s
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
p q : Submodule R₂ M₂
h : p ⋖ q
N : Submodule R M
h₁ : comap f p < N
h₂ : N < comap f q
⊢ False

Tactic:
refine h.2 (lt_map_of_comap_lt_of_surjective hf h₁) ?_

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
p q : Submodule R₂ M₂
h : p ⋖ q
N : Submodule R M
h₁ : comap f p < N
h₂ : N < comap f q
⊢ map f N < q
Module: Mathlib.Algebra.Group.Indicator

Goal state before:
pp: case pos
ι : Type u_6
inst✝¹ : DecidableEq ι
M : Type u_7
inst✝ : One M
i : ι
f : ι → M
j : ι
h : j = i
⊢ f j = f i

Tactic:
simp [h]

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

Goal state before:
pp: case neg
ι : Type u_6
inst✝¹ : DecidableEq ι
M : Type u_7
inst✝ : One M
i : ι
f : ι → M
j : ι
h : ¬j = i
⊢ 1 = 1

Tactic:
simp [h]

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

Goal state before:
pp: case pos
ι : Type u_1
α : Type u_2
inst✝ : Zero α
a : ι
f : (j : ι) → j ∈ {a} → α
j : ι
h : j = a
⊢ f j ⋯ = f a ⋯

Tactic:
simp [h]

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

Goal state before:
pp: case neg
ι : Type u_1
α : Type u_2
inst✝ : Zero α
a : ι
f : (j : ι) → j ∈ {a} → α
j : ι
h : ¬j = a
⊢ 0 = 0

Tactic:
simp [h]

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

Goal state before:
pp: case neg
α : Type u_1
M : Type u_5
inst✝ : Zero M
f : α →₀ M
a : α
h : f.support ⊆ {a}
x : α
hx : ¬x = a
⊢ f x = 0

Tactic:
exact notMem_support_iff.1 (mt (fun hx => (mem_singleton.1 (h hx))) hx)

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝¹ : Zero M
inst✝ : DecidableEq α
a a' : α
f : α →₀ M
⊢ (erase a f) a' = if a' = a then 0 else f a'

Tactic:
by
  rw [erase, coe_mk]
  simp only [ite_eq_ite]

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

Goal state before:
pp: case h.left
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
l : α →₀ M
f : α ↪ β
a : β
b : M
hb : b ≠ 0
h : embDomain f l = single a b
h_map_support : map f l.support = {a}
ha : a ∈ map f l.support
c : α
_hc₁ : c ∈ l.support
hc₂ : f c = a
d : α
⊢ l d = (single c b) d

Tactic:
← embDomain_apply_self f l,

Goal state after:
case h.left
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
l : α →₀ M
f : α ↪ β
a : β
b : M
hb : b ≠ 0
h : embDomain f l = single a b
h_map_support : map f l.support = {a}
ha : a ∈ map f l.support
c : α
_hc₁ : c ∈ l.support
hc₂ : f c = a
d : α
⊢ (embDomain f l) (f d) = (single c b) d
Module: Mathlib.Algebra.Group.Finsupp

Goal state before:
pp: case inr
ι : Type u_1
G : Type u_6
inst✝ : AddGroup G
f : ι →₀ G
a a' : ι
h : a' ≠ a
⊢ (erase a f) a' = (f - single a (f a)) a'

Tactic:
simp [h]

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

Goal state before:
pp: case refine_1
α : Type u_2
M : Type u_3
inst✝³ : CompleteLattice M
inst✝² : One M
ι : Type u_4
inst✝¹ : Preorder ι
inst✝ : IsDirectedOrder ι
f : ι → α → M
s : ι → Set α
h1 : ⊥ = 1
hf : Monotone f
hs : Monotone s
i : ι
⊢ (s i).mulIndicator (f i) ≤ (⋃ i, s i).mulIndicator (⨆ i, f i)

Tactic:
grw [← le_iSup f i, ← subset_iUnion s i]
    intro; simp [← h1]

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

Goal state before:
pp: α : Type u_2
M : Type u_3
inst✝³ : CompleteLattice M
inst✝² : One M
ι : Type u_4
inst✝¹ : Preorder ι
inst✝ : IsDirectedOrder ι
f : ι → α → M
s : ι → Set α
h1 : ⊥ = 1
hf : Monotone f
hs : Monotone s
a : α
ha : a ∈ ⋃ i, s i
⊢ ∃ i, a ∈ s i

Tactic:
by simpa using ha

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

Goal state before:
pp: case refine_2
α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
f : α →₀ M
a : α
g : α → M → N
h₀ : ∀ (b : α), f b ≠ 0 → b ≠ a → g b (f b) = 1
h₁ : f a = 0 → g a 0 = 1
h : a ∉ f.support
⊢ g a (f a) = 1

Tactic:
simp only [notMem_support_iff] at h

Goal state after:
case refine_2
α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
f : α →₀ M
a : α
g : α → M → N
h₀ : ∀ (b : α), f b ≠ 0 → b ≠ a → g b (f b) = 1
h₁ : f a = 0 → g a 0 = 1
h : f a = 0
⊢ g a (f a) = 1
Module: Mathlib.Algebra.Order.AbsoluteValue.Basic

Goal state before:
pp: R : Type u_5
S : Type u_6
inst✝² : Ring R
inst✝¹ : Semiring S
inst✝ : PartialOrder S
abv : AbsoluteValue R S
a b c : R
⊢ abv (a - c) ≤ abv (a - b) + abv (b - c)

Tactic:
by
  simpa [sub_eq_add_neg, add_assoc] using abv.add_le (a - b) (b - c)

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

Goal state before:
pp: α : Type u_2
inst✝² : CommMonoid α
inst✝¹ : Preorder α
s t : Multiset α
inst✝ : MulLeftMono α
h : Rel (fun x1 x2 ↦ x1 ≤ x2) s t
⊢ s.prod ≤ t.prod

Tactic:
induction h with
  | zero => rfl
  | cons rh _ rt =>
    rw [prod_cons, prod_cons]
    exact mul_le_mul' rh rt

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
⊢ graph 0 = ∅

Tactic:
simp [graph]

Goal state after:
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 : Surjective f
x : β →₀ M
⊢ mapDomain f (mapDomain (surjInv hf) x) = x

Tactic:
← mapDomain_comp,

Goal state after:
case h
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
hf : Surjective f
x : β →₀ M
⊢ mapDomain (f ∘ surjInv hf) x = x
Module: Mathlib.Algebra.Order.BigOperators.Ring.Multiset

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : CommMonoidWithZero β
inst✝¹ : PartialOrder β
inst✝ : PosMulMono β
f : α → β
p : α → Prop
h0 : ∀ (a : α), 0 ≤ f a
h_one : f 1 ≤ 1
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
s : Multiset α
hs : (∀ (a : α), a ∈ s → p a) → f s.prod ≤ (map f s).prod
hpsa : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → p a_1
hs0 : ¬s = ∅
hps : ∀ (x : α), x ∈ s → p x
hp_prod : p s.prod
⊢ f (a ::ₘ s).prod ≤ (map f (a ::ₘ s)).prod

Tactic:
rw [prod_cons, map_cons, prod_cons]

Goal state after:
case neg
α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : CommMonoidWithZero β
inst✝¹ : PartialOrder β
inst✝ : PosMulMono β
f : α → β
p : α → Prop
h0 : ∀ (a : α), 0 ≤ f a
h_one : f 1 ≤ 1
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
s : Multiset α
hs : (∀ (a : α), a ∈ s → p a) → f s.prod ≤ (map f s).prod
hpsa : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → p a_1
hs0 : ¬s = ∅
hps : ∀ (x : α), x ∈ s → p x
hp_prod : p s.prod
⊢ f (a * s.prod) ≤ f a * (map f s).prod
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_5
N : Type u_6
inst✝² : Zero M
p : α → Prop
inst✝¹ : DecidablePred p
f : α →₀ M
inst✝ : CommMonoid N
g : α → M → N
x : α
hx : x ∈ {x ∈ f.support | p x}
⊢ g x ((filter p f) x) = g x (f x)

Tactic:
Finset.mem_filter

Goal state after:
α : Type u_1
M : Type u_5
N : Type u_6
inst✝² : Zero M
p : α → Prop
inst✝¹ : DecidablePred p
f : α →₀ M
inst✝ : CommMonoid N
g : α → M → N
x : α
hx : x ∈ f.support ∧ p x
⊢ g x ((filter p f) x) = g x (f x)
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_1
N : Type u_5
inst✝³ : CommMonoid N
inst✝² : Preorder N
s : Finset ι
ι' : Type u_9
inst✝¹ : DecidableEq ι'
inst✝ : MulLeftMono N
g : ι → ι'
f : ι' → N
hf : ∀ u ∈ image g s, 1 ≤ f u
a : ι'
hag : a ∈ image g s
i : ι
hi : i ∈ s
hig : g i = a
⊢ #({a_1 ∈ s | g a_1 = a}) ≠ 0

Tactic:
← Nat.pos_iff_ne_zero,

Goal state after:
ι : Type u_1
N : Type u_5
inst✝³ : CommMonoid N
inst✝² : Preorder N
s : Finset ι
ι' : Type u_9
inst✝¹ : DecidableEq ι'
inst✝ : MulLeftMono N
g : ι → ι'
f : ι' → N
hf : ∀ u ∈ image g s, 1 ≤ f u
a : ι'
hag : a ∈ image g s
i : ι
hi : i ∈ s
hig : g i = a
⊢ 0 < #({a_1 ∈ s | g a_1 = a})
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: case pos
α : Type u_1
M : Type u_12
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
f : Subtype P →₀ M
a : α
h : P a
⊢ f.extendDomain a = f ⟨a, h⟩

Tactic:
simp [h]

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

Goal state before:
pp: α : Type u_1
s : Set α
M : Type u_12
inst✝¹ : AddCommMonoid M
inst✝ : DecidablePred fun x ↦ x ∈ s
f : ↑s →₀ M
⊢ ↑((restrictSupportEquiv s M).symm f) = f.extendDomain

Tactic:
by
  rw [restrictSupportEquiv, Equiv.coe_fn_symm_mk, Subtype.coe_mk]; congr

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : LinearOrder M
s : Finset ι
inst✝ : IsOrderedCancelMonoid M
f : ι → M
h₁ : ∀ i ∈ s, f i ≤ 1
i : ι
m : i ∈ s
i_ne : f i ≠ 1
⊢ ∏ i ∈ s, f i < 1

Tactic:
calc
    ∏ j ∈ s, f j < ∏ j ∈ s, 1 := prod_lt_prod' h₁ ⟨i, m, (h₁ i m).lt_of_ne i_ne⟩
    _ = 1 := prod_const_one

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

Goal state before:
pp: α : Type u_1
M : Type u_5
R : Type u_11
inst✝¹ : Zero M
inst✝ : SMulZeroClass R M
b : R
g : α →₀ M
a : α
⊢ a ∈ (b • g).support → a ∈ g.support

Tactic:
simp only [smul_apply, mem_support_iff, Ne]

Goal state after:
α : Type u_1
M : Type u_5
R : Type u_11
inst✝¹ : Zero M
inst✝ : SMulZeroClass R M
b : R
g : α →₀ M
a : α
⊢ ¬b • g a = 0 → ¬g a = 0
Module: Mathlib.Data.Finsupp.SMul

Goal state before:
pp: case pos
α : Type u_1
M : Type u_3
R : Type u_6
inst✝² : Zero M
inst✝¹ : MonoidWithZero R
inst✝ : MulActionWithZero R M
a b : α
f : α → M
r : R
h : a = b
⊢ (single a r) b • f a = (single a (r • f b)) b

Tactic:
simp [h]

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

Goal state before:
pp: case neg
α : Type u_1
M : Type u_3
R : Type u_6
inst✝² : Zero M
inst✝¹ : MonoidWithZero R
inst✝ : MulActionWithZero R M
a b : α
f : α → M
r : R
h : ¬a = b
⊢ (single a r) b • f a = (single a (r • f b)) b

Tactic:
simp [h]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
G : Type u_5
R : Type u_6
inst✝² : Monoid G
inst✝¹ : MulAction G α
inst✝ : AddCommMonoid M
g g' : G
f : α →₀ M
⊢ mapDomain ((fun x ↦ g • x) ∘ fun x ↦ g' • x) f = mapDomain (fun x ↦ g • x) (mapDomain (fun x ↦ g' • x) f)

Tactic:
mapDomain_comp

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
G : Type u_5
R : Type u_6
inst✝² : Monoid G
inst✝¹ : MulAction G α
inst✝ : AddCommMonoid M
g g' : G
f : α →₀ M
⊢ mapDomain (fun x ↦ g • x) (mapDomain (fun x ↦ g' • x) f) = mapDomain (fun x ↦ g • x) (mapDomain (fun x ↦ g' • x) f)
Module: Mathlib.LinearAlgebra.Finsupp.Supported

Goal state before:
pp: case pos
α : Type u_1
M : Type u_2
R : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
l : ↥(supported M R s)
a : α
h : a ∈ s
⊢ ↑((restrictDom M R s ∘ₗ (supported M R s).subtype) l) a = ↑(LinearMap.id l) a

Tactic:
simp [h]

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

Goal state before:
pp: case neg
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
δ : Type u_7
s : δ → Set α
this : DecidablePred fun x ↦ x ∈ ⋃ i, s i
x : α
a : M
l : α →₀ M
a✝¹ : x ∉ l.support
a✝ : a ≠ 0
ih : l ∈ comap ((supported M R (⋃ i, s i)).subtype ∘ₗ restrictDom M R (⋃ i, s i)) (⨆ i, supported M R (s i))
h : ¬∃ i, x ∈ s i
⊢ single x a ∈ comap ((supported M R (⋃ i, s i)).subtype ∘ₗ restrictDom M R (⋃ i, s i)) (⨆ i, supported M R (s i))

Tactic:
simp [h]

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

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

Tactic:
rw [← preimage_val_Ioo_val, image_preimage_eq_inter_range, range_val, inter_eq_left]
  exact fun k hk ↦ hk.2.trans j.is_lt

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

Goal state before:
pp: ι : Type u_7
N₀ : Type u_8
M₀ : Type u_9
inst✝² : CommMonoidWithZero M₀
inst✝¹ : Nontrivial M₀
inst✝ : NoZeroDivisors M₀
n : N₀
f : ι → N₀ → M₀
h : ∀ (i : ι), f i n ≠ 0
⊢ (∏ᶠ (i : ι), f i) n ≠ 0

Tactic:
by_cases h₂ : f.mulSupport.Finite
  · rw [finprod_eq_prod f h₂]
    grind [Finset.prod_apply, Finset.prod_ne_zero_iff]
  · simp [finprod_of_infinite_mulSupport h₂]

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

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
x : M
⊢ x ∈ span R (Set.range v) ↔ ∃ c, (c.sum fun i a ↦ a • v i) = x

Tactic:
by
  simp only [← Finsupp.range_linearCombination, LinearMap.mem_range, linearCombination_apply]

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

Goal state before:
pp: n m : ℕ
i : Fin n
⊢ (fun x ↦ x.addNat m) '' Ici i = Ici (i.addNat m)

Tactic:
rw [← preimage_addNat_Ici_addNat, image_preimage_eq_of_subset]
  intro j hj
  have : (i : ℕ) + m ≤ j := hj
  refine ⟨⟨j - m, by lia⟩, ?_⟩
  simp (disch := lia)

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

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset α
f : α → R
g : α → M
hf : ∀ (a : α), f a ≠ 0 → a ∈ s
x : α
a✝ : x ∈ s
h : f x = 0
⊢ f x • g x = 0

Tactic:
simp [h]

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

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset α
f : α → R
g : α → M
hf : ∀ (a : α), f a ≠ 0 → a ∈ s
⊢ (linearCombination R g) (onFinset s f hf) = ∑ x ∈ s, f x • g x

Tactic:
classical
  simp only [linearCombination_apply, Finsupp.sum, Finsupp.onFinset_apply, Finsupp.support_onFinset]
  rw [Finset.sum_filter_of_ne]
  intro x _ h
  contrapose h
  simp [h]

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

Goal state before:
pp: case pos.succ
α : Type u
m n o : ℕ
ho : o + 1 = m + 1 + n
x : α
u : Fin m → α
v : Fin n → α
i : ℕ
hi : i + 1 < o + 1
h✝ : ↑⟨i + 1, hi⟩ < m + 1
h : i < m
⊢ vecCons x u ⟨↑⟨i + 1, hi⟩, h✝⟩ = vecCons x (fun i ↦ if h : ↑i < m then u ⟨↑i, h⟩ else v ⟨↑i - m, ⋯⟩) ⟨i + 1, hi⟩

Tactic:
simp [h]

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

Goal state before:
pp: m n k : ℕ
h₁ : m ≤ k
h₂ : k < m + n
⊢ finAddFlip ⟨k, h₂⟩ = ⟨k - m, ⋯⟩

Tactic:
convert! @finAddFlip_apply_natAdd n ⟨k - m, by lia⟩ m

Goal state after:
case e'_2.e'_2
m n k : ℕ
h₁ : m ≤ k
h₂ : k < m + n
⊢ k = ↑(Fin.natAdd m ⟨k - m, ⋯⟩)
Module: Mathlib.Algebra.Group.Fin.Basic

Goal state before:
pp: case pos
n✝ : ℕ
a : Fin (n✝ + 1 + 1)
h : a = 0
⊢ ↑(a - 1) = n✝ + 1

Tactic:
simp [h]

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

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
⊢ i < (finRotate (n + 1)) i ↔ i ≠ Fin.last n

Tactic:
simpa using Fin.lt_last_iff_ne_last

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

Goal state before:
pp: case hf
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
γ : Type u_7
f : α × β × γ → M
h : HasFiniteMulSupport f
a : α
⊢ HasFiniteMulSupport fun b ↦ f (a, b)

Tactic:
simp [h]

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

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
p : Submodule R M
h : p = ⊤
⊢ ∀ (i : ι), b i ∈ p

Tactic:
simp [h]

Goal state after:
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case inl
x y : ℕ∞
h : x = 1
⊢ x ^ y = 1

Tactic:
simp [h]

Goal state after:
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case inr
x y : ℕ∞
h : y = 0
⊢ x ^ y = 1

Tactic:
simp [h]

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

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
p : M
⊢ 0 • p + p = 1 • p + 0

Tactic:
by simp [one_nsmul]

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
M' : Type u_5
v : ι → M
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
f : M →ₗ[R] M'
hv : Injective ⇑(f ∘ₗ Finsupp.linearCombination R v)
⊢ Disjoint (span R (range v)) f.ker

Tactic:
rw [disjoint_iff_inf_le, ← Set.image_univ, Finsupp.span_image_eq_map_linearCombination,
    map_inf_eq_map_inf_comap, (LinearMap.ker_comp _ _).symm.trans
      (LinearMap.ker_eq_bot_of_injective hv), inf_bot_eq, map_bot]

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

Goal state before:
pp: G : Type u_1
inst✝ : AddCommGroup G
a b : G
⊢ 1 • (b - a) + a = 0 • (b - a) + b

Tactic:
by simp [one_nsmul]

Goal state after: