mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Group.Finsupp

Goal state before:
pp: ι : Type u_1
G : Type u_6
inst✝ : AddGroup G
f : ι →₀ G
a : ι
b : G
⊢ f.update a b = f - single a (f a) + single a b

Tactic:
rw [update_eq_erase_add_single, erase_eq_sub_single]

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
    rw [h]
    exact h₁ h

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

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

Tactic:
suffices ∀ y, f y = 0 by rw [this, this, smul_zero]

Goal state after:
case neg
M : Type u_3
M₂ : Type u_4
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid 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✝³ : DivisionSemiring R
inst✝² : DivisionSemiring S
inst✝¹ : Module R M
inst✝ : Module S M₂
n : ℕ
x : M
hR : ↑n = 0
hS : ¬↑n = 0
⊢ ∀ (y : M), f y = 0
Module: Mathlib.Algebra.Order.AbsoluteValue.Basic

Goal state before:
pp: case inr.inr
ι : Type u_1
α : Type u_2
R✝ : Type u_3
S✝ : Type u_4
R : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : DecidablePred fun x ↦ x = 0
inst✝⁴ : NoZeroDivisors R
S : Type u_6
inst✝³ : Semiring S
inst✝² : PartialOrder S
inst✝¹ : IsOrderedRing S
inst✝ : Nontrivial S
x y : R
hx : x ≠ 0
hy : y ≠ 0
⊢ (if x + y = 0 then 0 else 1) ≤ (if x = 0 then 0 else 1) + if y = 0 then 0 else 1

Tactic:
simp only [hx, ↓reduceIte, hy, one_add_one_eq_two]

Goal state after:
case inr.inr
ι : Type u_1
α : Type u_2
R✝ : Type u_3
S✝ : Type u_4
R : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : DecidablePred fun x ↦ x = 0
inst✝⁴ : NoZeroDivisors R
S : Type u_6
inst✝³ : Semiring S
inst✝² : PartialOrder S
inst✝¹ : IsOrderedRing S
inst✝ : Nontrivial S
x y : R
hx : x ≠ 0
hy : y ≠ 0
⊢ (if x + y = 0 then 0 else 1) ≤ 2
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
s : Finset α
f : (a : α) → a ∈ s → M
h : α → M → N
h_zero : ∀ a ∈ s, h a 0 = 1
⊢ (indicator s f).prod h = ∏ x ∈ s.attach, h (↑x) (f ↑x ⋯)

Tactic:
prod_of_support_subset _ (support_indicator_subset _ _) h h_zero,

Goal state after:
α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
s : Finset α
f : (a : α) → a ∈ s → M
h : α → M → N
h_zero : ∀ a ∈ s, h a 0 = 1
⊢ ∏ x ∈ s, h x ((indicator s f) x) = ∏ x ∈ s.attach, h (↑x) (f ↑x ⋯)
Module: Mathlib.Algebra.Order.AbsoluteValue.Basic

Goal state before:
pp: case inr
R : Type u_3
S : Type u_4
inst✝⁴ : Field R
inst✝³ : Semifield S
inst✝² : LinearOrder S
inst✝¹ : IsStrictOrderedRing S
inst✝ : ExistsAddOfLE S
v : AbsoluteValue R S
x : R
hx₀ : x ≠ 0
hx₁ : v x ≠ 1
h : 1 < v x
⊢ ∃ x, 1 < v x

Tactic:
exact ⟨x, h⟩

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 : Injective f
x : α →₀ M
a : α
⊢ ∀ (b : α), x b ≠ 0 → b ≠ a → (single (f b) (x b)) (f a) = 0

Tactic:
intro b _ hba

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 b : α
a✝ : x b ≠ 0
hba : b ≠ a
⊢ (single (f b) (x b)) (f a) = 0
Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
f : ι → R
s : Finset ι
hf : ∀ i ∈ s, 0 ≤ f i
i : ι
hi : i ∈ s
⊢ f i * f i ≤ ∑ j ∈ s, f i * f j

Tactic:
rw [← mul_sum]

Goal state after:
ι : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
f : ι → R
s : Finset ι
hf : ∀ i ∈ s, 0 ≤ f i
i : ι
hi : i ∈ s
⊢ f i * f i ≤ f i * ∑ i ∈ s, f i
Module: Mathlib.Data.Finsupp.Basic

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

Tactic:
refine ⟨fun ⟨y, hy⟩ x hx ↦ hy ▸ Finsupp.mapDomain_of_notMem_range y x hx, fun h ↦ ?_⟩

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
hf : Injective f
x : β →₀ M
h : ∀ b ∉ Set.range f, x b = 0
⊢ x ∈ Set.range (mapDomain f)
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: case cons
α : Type u_2
β : Type u_3
inst✝ : DecidableEq α
f : β → Multiset α
z : β
i : Finset β
hz : z ∉ i
hr : i.sum f = i.sup f ↔ ∀ x ∈ i, ∀ y ∈ i, x ≠ y → Disjoint (f x) (f y)
this : ∀ x ∈ i, x ≠ z
⊢ f z + ∑ x ∈ i, f x = f z ∪ i.sup f ↔ Disjoint (f z) (i.sum f) ∧ Disjoint (f z) (i.sum f) ∧ i.sum f = i.sup f

Tactic:
← and_assoc,

Goal state after:
case cons
α : Type u_2
β : Type u_3
inst✝ : DecidableEq α
f : β → Multiset α
z : β
i : Finset β
hz : z ∉ i
hr : i.sum f = i.sup f ↔ ∀ x ∈ i, ∀ y ∈ i, x ≠ y → Disjoint (f x) (f y)
this : ∀ x ∈ i, x ≠ z
⊢ f z + ∑ x ∈ i, f x = f z ∪ i.sup f ↔ (Disjoint (f z) (i.sum f) ∧ Disjoint (f z) (i.sum f)) ∧ i.sum f = i.sup f
Module: Mathlib.LinearAlgebra.Finsupp.LSum

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type u_4
f : M →ₗ[R] α →₀ R
s : Surjective ⇑f
x a✝ : α
⊢ f ((single x 1).sum fun x r ↦ r • ⋯.choose) = single x 1

Tactic:
rw [sum_single_index, one_smul]

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type u_4
f : M →ₗ[R] α →₀ R
s : Surjective ⇑f
x a✝ : α
⊢ f ⋯.choose = single x 1

R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type u_4
f : M →ₗ[R] α →₀ R
s : Surjective ⇑f
x a✝ : α
⊢ 0 • ⋯.choose = 0
Module: Mathlib.LinearAlgebra.Finsupp.Supported

Goal state before:
pp: α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
R : Type u_5
S : Type u_6
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
s : Set α
F : ↥(supported M R s) ≃ (↑s →₀ M) := restrictSupportEquiv s M
⊢ IsLinearMap R ⇑F

Tactic:
have :
    (F : supported M R s → ↥s →₀ M) =
      (lsubtypeDomain s : (α →₀ M) →ₗ[R] s →₀ M).comp (Submodule.subtype (supported M R s)) :=
    rfl

Goal state after:
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
R : Type u_5
S : Type u_6
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
s : Set α
F : ↥(supported M R s) ≃ (↑s →₀ M) := restrictSupportEquiv s M
this : ⇑F = ⇑(lsubtypeDomain s ∘ₗ (supported M R s).subtype)
⊢ IsLinearMap R ⇑F
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: M : Type u_2
α : Sort u_4
inst✝ : CommMonoid M
f : α → M
hf : HasFiniteMulSupport (f ∘ PLift.down)
s : Finset (PLift α)
hs : Finite.toFinset hf ⊆ s
x : PLift α
x✝ : x ∈ s
hxf : x ∉ Finite.toFinset hf
⊢ f x.down = 1

Tactic:
hf.mem_toFinset,

Goal state after:
M : Type u_2
α : Sort u_4
inst✝ : CommMonoid M
f : α → M
hf : HasFiniteMulSupport (f ∘ PLift.down)
s : Finset (PLift α)
hs : Finite.toFinset hf ⊆ s
x : PLift α
x✝ : x ∈ s
hxf : x ∉ mulSupport (f ∘ PLift.down)
⊢ f x.down = 1
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
p : α → Prop
t : Finset α
h : ∀ {x : α}, f x ≠ 1 → (p x ↔ x ∈ t)
s : Set α := {x | p x}
this : mulSupport (s.mulIndicator f) ⊆ ↑t
x : α
hx : x ∈ t
hxs : f x ≠ 1
⊢ x ∈ s

Tactic:
exact (h hxs).2 hx

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

Goal state before:
pp: case refine_1
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set α
t : Finset α
h : s ∩ mulSupport f = ↑t ∩ mulSupport f
x : α
hxf : x ∈ mulSupport f
hx : x ∈ s
⊢ x ∈ ↑t ∩ mulSupport f

Tactic:
rw [← Set.ext_iff.mp h x, mem_inter_iff]

Goal state after:
case refine_1
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set α
t : Finset α
h : s ∩ mulSupport f = ↑t ∩ mulSupport f
x : α
hxf : x ∈ mulSupport f
hx : x ∈ s
⊢ x ∈ s ∧ x ∈ mulSupport f
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
f : M → ι → R
hadd : ∀ (x y : M), f (x + y) = f x + f y
hsmul : ∀ (c : R) (x : M), f (c • x) = c • f x
f_eq : ∀ (i : ι), f (b i) = ⇑(single i 1)
x : M
i : ι
x✝¹ : R
x✝ : M
⊢ f (x✝¹ • x✝) i = (RingHom.id R) x✝¹ • f x✝ i

Tactic:
simp [hsmul, Pi.smul_apply]

Goal state after:
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
⊢ ∀ (c : R) (x : M), (fun i ↦ (b.reindexRange.repr (c • x)) ⟨b i, ⋯⟩) = c • fun i ↦ (b.reindexRange.repr x) ⟨b i, ⋯⟩

Tactic:
intro c x

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
c : R
x : M
⊢ (fun i ↦ (b.reindexRange.repr (c • x)) ⟨b i, ⋯⟩) = c • fun i ↦ (b.reindexRange.repr x) ⟨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
⊢ ∑ i_1, Pi.single i r i_1 • v i_1 = r • v i

Tactic:
Pi.single_apply,

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 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
inst✝¹ : Fintype ι
inst✝ : DecidableEq M
i : ι
h : b i ∈ Finset.image (⇑b) Finset.univ
⊢ b.reindexFinsetRange ⟨b i, h⟩ = b i

Tactic:
reindexFinsetRange,

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
inst✝¹ : Fintype ι
inst✝ : DecidableEq M
i : ι
h : b i ∈ Finset.image (⇑b) Finset.univ
⊢ (b.reindexRange.reindex ((Equiv.refl M).subtypeEquiv ⋯)) ⟨b i, h⟩ = b 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
inst✝¹ : Fintype ι
inst✝ : DecidableEq M
i : ι
bi : M
hbi : bi ∈ Finset.image (⇑b) Finset.univ
⊢ (b.reindexFinsetRange.repr (b i)) ⟨bi, hbi⟩ = (single ⟨b i, ⋯⟩ 1) ⟨bi, hbi⟩

Tactic:
reindexFinsetRange,

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
inst✝¹ : Fintype ι
inst✝ : DecidableEq M
i : ι
bi : M
hbi : bi ∈ Finset.image (⇑b) Finset.univ
⊢ ((b.reindexRange.reindex ((Equiv.refl M).subtypeEquiv ⋯)).repr (b i)) ⟨bi, hbi⟩ = (single ⟨b i, ⋯⟩ 1) ⟨bi, hbi⟩
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: n : ℕ
x : { x // x ≠ Fin.last n }
⊢ (finSuccAboveEquiv (Fin.last n)).symm x = (↑x).castLT ⋯

Tactic:
← Option.some_inj

Goal state after:
n : ℕ
x : { x // x ≠ Fin.last n }
⊢ some ((finSuccAboveEquiv (Fin.last n)).symm x) = some ((↑x).castLT ⋯)
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: n : ℕ
p : Fin (n + 1)
h : p ≠ Fin.last n
x : { x // x ≠ p }
⊢ (finSuccAboveEquiv p).symm x = (p.castLT ⋯).predAbove ↑x

Tactic:
← Option.some_inj

Goal state after:
n : ℕ
p : Fin (n + 1)
h : p ≠ Fin.last n
x : { x // x ≠ p }
⊢ some ((finSuccAboveEquiv p).symm x) = some ((p.castLT ⋯).predAbove ↑x)
Module: Mathlib.Data.Fin.VecNotation

Goal state before:
pp: α : Type u
n : ℕ
v : Fin n → α
i : Fin n
⊢ vecAlt0 ⋯ (vecAppend ⋯ v v) i = (v ∘ fun n_1 ↦ n_1 + n_1) i

Tactic:
Function.comp,

Goal state after:
α : Type u
n : ℕ
v : Fin n → α
i : Fin n
⊢ vecAlt0 ⋯ (vecAppend ⋯ v v) i = v (i + i)
Module: Mathlib.Data.Fin.VecNotation

Goal state before:
pp: α : Type u
n : ℕ
v : Fin (n + 1) → α
i : Fin (n + 1)
⊢ vecAlt1 ⋯ (vecAppend ⋯ v v) i = (v ∘ fun n_1 ↦ n_1 + n_1 + 1) i

Tactic:
Function.comp,

Goal state after:
α : Type u
n : ℕ
v : Fin (n + 1) → α
i : Fin (n + 1)
⊢ vecAlt1 ⋯ (vecAppend ⋯ v v) i = v (i + i + 1)
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:
by
  convert! @finAddFlip_apply_natAdd n ⟨k - m, by lia⟩ m
  simp [Nat.add_sub_cancel' h₁]

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

Goal state before:
pp: α : Type u
m n : ℕ
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
i : Fin (n + 1)
⊢ vecAlt0 h (vecCons x (vecCons y u)) i = vecCons x (vecAlt0 ⋯ u) i

Tactic:
simp_rw [vecAlt0]

Goal state after:
α : Type u
m n : ℕ
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
i : Fin (n + 1)
⊢ vecCons x (vecCons y u) ⟨↑i + ↑i, ⋯⟩ = vecCons x (vecAlt0 ⋯ u) i
Module: Mathlib.Algebra.Group.Fin.Basic

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

Tactic:
exact val_sub_one_of_ne_zero h

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
⊢ ∏ i ∈ s, f i = ∏ᶠ (a : α) (b : β) (_ : b ∈ Finset.image Prod.snd ({ab ∈ s | ab.1 = a})), f (a, b)

Tactic:
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 : α), ∏ i ∈ Finset.image Prod.snd ({ab ∈ s | ab.1 = a}), f (a, i)
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
a b c p : M
hbc : ∃ m n, m • p + b = n • p + c
m n : ℕ
hab : m • p + a = n • p + b
⊢ ∃ m n, m • p + a = n • p + c

Tactic:
rcases hbc with ⟨k, l, hbc⟩

Goal state after:
M : Type u_1
inst✝ : AddCommMonoid M
a b c p : M
m n : ℕ
hab : m • p + a = n • p + b
k l : ℕ
hbc : k • p + b = l • p + c
⊢ ∃ m n, m • p + a = n • p + c
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n : ℕ
f : Fin (n + 1) → M
a : Fin n
⊢ ∏ i > a.succ, f i = ∏ i > a, f i.succ

Tactic:
simp [← map_succEmb_Ioi]

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

Goal state before:
pp: R : Type u_3
inst✝ : Ring R
m : ℕ
⊢ ∑ n, (-1) ^ ↑n = if Even m then 0 else 1

Tactic:
by
  induction m with
  | zero => simp
  | succ n IH =>
    simp only [Fin.sum_univ_castSucc, Fin.val_castSucc, IH, Fin.val_last, Nat.even_add_one, ite_not]
    split_ifs with h
    · simp [*]
    · simp [(Nat.not_even_iff_odd.mp h).neg_pow]

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

Goal state before:
pp: ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ LinearIndepOn R v s ↔ Injective ⇑(Finsupp.linearCombinationOn ι M R v s)

Tactic:
← linearIndependent_restrict_iff

Goal state after:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ LinearIndependent (ι := ↑s) R (s.domRestrict v) ↔ Injective ⇑(Finsupp.linearCombinationOn ι M R v s)
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: a b d : ℕ
hac : a.Coprime (d * b)
b_dvd_c : b ∣ d * b
⊢ a.gcd d = 1

Tactic:
exact Coprime.coprime_mul_right_right hac

Goal state after:
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: m a b c : ℕ
hm : 0 < m
h : c * a ≡ c * b [MOD m]
⊢ a ≡ b [MOD m / m.gcd c]

Tactic:
by
  let d := gcd m c
  have hmd := gcd_dvd_left m c
  have hcd := gcd_dvd_right m c
  rw [modEq_iff_dvd]
  refine @Int.dvd_of_dvd_mul_right_of_gcd_one (m / d) (c / d) (b - a) ?_ ?_
  · show (m / d : ℤ) ∣ c / d * (b - a)
    rw [mul_comm, ← Int.mul_ediv_assoc (b - a) (Int.natCast_dvd_natCast.mpr hcd), mul_comm]
    apply Int.ediv_dvd_ediv (Int.natCast_dvd_natCast.mpr hmd)
    rw [Int.mul_sub]
    exact modEq_iff_dvd.mp h
  · show Int.gcd (m / d) (c / d) = 1
    simp only [d, ← Int.natCast_div, Int.gcd_natCast_natCast (m / d) (c / d),
      gcd_div hmd hcd, Nat.div_self (gcd_pos_of_pos_left c hm)]

Goal state after:
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: a b c : ℕ
hc : a % c + b % c < c
⊢ (a + b) % c = a % c + b % c

Tactic:
rw [← add_mod_add_ite, if_neg (not_le_of_gt hc), add_zero]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Finite

Goal state before:
pp: α : Type u
β : Type v
inst✝ : Finite α
f : α → β
hf : Surjective f
⊢ Nat.card β ≤ Nat.card α

Tactic:
have : lift.{u} #β ≤ lift.{v} #α := mk_le_of_surjective (ULift.map_surjective.2 hf)
  simpa using! toNat_le_toNat this (by simp)

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Finite

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Finite β
f : α → β
this✝ : Fintype β
this : Fintype α
⊢ Bijective f ↔ Injective f ∧ Nat.card α = Nat.card β

Tactic:
card_eq_fintype_card,

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : Finite β
f : α → β
this✝ : Fintype β
this : Fintype α
⊢ Bijective f ↔ Injective f ∧ Fintype.card α = Nat.card β
Module: Mathlib.SetTheory.Cardinal.Finite

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Finite β
f : α → β
this✝ : Fintype β
this : Fintype α
⊢ Bijective f ↔ Injective f ∧ Fintype.card α = Nat.card β

Tactic:
card_eq_fintype_card,

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : Finite β
f : α → β
this✝ : Fintype β
this : Fintype α
⊢ Bijective f ↔ Injective f ∧ Fintype.card α = Fintype.card β
Module: Mathlib.SetTheory.Cardinal.Finite

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
this✝ : Fintype α
this : Fintype β
⊢ Bijective f ↔ Surjective f ∧ Nat.card α = Nat.card β

Tactic:
card_eq_fintype_card,

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
this✝ : Fintype α
this : Fintype β
⊢ Bijective f ↔ Surjective f ∧ Fintype.card α = Nat.card β
Module: Mathlib.SetTheory.Cardinal.Finite

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
this✝ : Fintype α
this : Fintype β
⊢ Bijective f ↔ Surjective f ∧ Fintype.card α = Nat.card β

Tactic:
card_eq_fintype_card,

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
this✝ : Fintype α
this : Fintype β
⊢ Bijective f ↔ Surjective f ∧ Fintype.card α = Fintype.card β
Module: Mathlib.SetTheory.Cardinal.Finite

Goal state before:
pp: α : Type u_1
a : α
inst✝ : Subsingleton α
this : Fintype α := Fintype.ofSubsingleton a
⊢ Nat.card α = 1

Tactic:
card_eq_fintype_card,

Goal state after:
α : Type u_1
a : α
inst✝ : Subsingleton α
this : Fintype α := Fintype.ofSubsingleton a
⊢ Fintype.card α = 1
Module: Mathlib.SetTheory.Cardinal.Finite

Goal state before:
pp: α : Type u_3
β : Type u_4
⊢ card (α → β) = card β ^ card α

Tactic:
rcases isEmpty_or_nonempty α with α_emp | α_emp

Goal state after:
case inl
α : Type u_3
β : Type u_4
α_emp : IsEmpty α
⊢ card (α → β) = card β ^ card α

case inr
α : Type u_3
β : Type u_4
α_emp : Nonempty α
⊢ card (α → β) = card β ^ card α
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: case refine_2
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : LinearOrder R
inst✝⁴ : CanonicallyOrderedAdd R
inst✝³ : AddRightReflectLE R
inst✝² : IsCancelAdd M
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
h : ∀ (t : Finset ι) (f : ι → R), ∑ i ∈ t, f i • v i = ∑ i ∈ tᶜ, f i • v i → ∀ (i : ι), f i = 0
t₁ t₂ : Finset ι
f : ι → R
ht₁t₂ : Disjoint t₁ t₂
heq : ∑ i ∈ t₁, f i • v i = ∑ i ∈ t₂, f i • v i
⊢ ∑ i ∈ t₁, (if i ∈ t₁ ∨ i ∈ t₂ then f i else 0) • v i = ∑ i ∈ t₁ᶜ, (if i ∈ t₁ ∨ i ∈ t₂ then f i else 0) • v i

Tactic:
rw [← Finset.sum_subset ht₁t₂.le_compl_left]

Goal state after:
case refine_2
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : LinearOrder R
inst✝⁴ : CanonicallyOrderedAdd R
inst✝³ : AddRightReflectLE R
inst✝² : IsCancelAdd M
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
h : ∀ (t : Finset ι) (f : ι → R), ∑ i ∈ t, f i • v i = ∑ i ∈ tᶜ, f i • v i → ∀ (i : ι), f i = 0
t₁ t₂ : Finset ι
f : ι → R
ht₁t₂ : Disjoint t₁ t₂
heq : ∑ i ∈ t₁, f i • v i = ∑ i ∈ t₂, f i • v i
⊢ ∑ i ∈ t₁, (if i ∈ t₁ ∨ i ∈ t₂ then f i else 0) • v i = ∑ x ∈ t₂, (if x ∈ t₁ ∨ x ∈ t₂ then f x else 0) • v x

case refine_2
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : LinearOrder R
inst✝⁴ : CanonicallyOrderedAdd R
inst✝³ : AddRightReflectLE R
inst✝² : IsCancelAdd M
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
h : ∀ (t : Finset ι) (f : ι → R), ∑ i ∈ t, f i • v i = ∑ i ∈ tᶜ, f i • v i → ∀ (i : ι), f i = 0
t₁ t₂ : Finset ι
f : ι → R
ht₁t₂ : Disjoint t₁ t₂
heq : ∑ i ∈ t₁, f i • v i = ∑ i ∈ t₂, f i • v i
⊢ ∀ x ∈ t₁ᶜ, x ∉ t₂ → (if x ∈ t₁ ∨ x ∈ t₂ then f x else 0) • v x = 0
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
h : ∀ (s : Finset ι) (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i
s : Finset ι
f : ι → R
⊢ (∑ i ∈ s, f i • v i = 0 → ∀ i ∈ s, f i = 0) ↔ ∑ i ∈ s, f i • v i = ∑ i ∈ s, 0 i • v i → ∀ i ∈ s, f i = 0 i

Tactic:
simp_rw [Pi.zero_apply, zero_smul, Finset.sum_const_zero]

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case refine_1
α : Type u_1
s : Set α
x : α
h : (s \ {x}).encard = 3
hx : x ∈ s
⊢ ∃ x y z w, x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}

Tactic:
encard_eq_three

Goal state after:
case refine_1
α : Type u_1
s : Set α
x : α
h : ∃ x_1 y z, x_1 ≠ y ∧ x_1 ≠ z ∧ y ≠ z ∧ s \ {x} = {x_1, y, z}
hx : x ∈ s
⊢ ∃ x y z w, x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case refine_1.refine_3
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y z : α
hyz : y ≠ z
hyw : y ≠ x
hzw : z ≠ x
hs : s \ {x} = {y, z, x}
⊢ False

Tactic:
exact (hs.symm.subset (Or.inr (Or.inr rfl))).2 rfl

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

Goal state before:
pp: case refine_2
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
H : ∀ (i : ι) (a : R), a • v i ∈ span R (v '' (univ \ {i})) → a = 0
l : ι →₀ R
hl : (Finsupp.linearCombination R v) l = 0
i : ι
hn : ¬l i = 0
⊢ (Finsupp.linearCombination R v) (Finsupp.single i (l i) - l) = l i • v i

Tactic:
simp [hl]

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
hc : t.encard < s.encard
hf : MapsTo f s t
⊢ ∃ a₁ ∈ s, ∃ a₂ ∈ s, a₁ ≠ a₂ ∧ f a₁ = f a₂

Tactic:
contrapose! hc
  suffices Function.Injective (hf.restrict f) by
    let f' : s ↪ t := ⟨hf.restrict, this⟩
    exact f'.encard_le
  simpa only [hf.restrict_inj, not_imp_not] using! hc

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Finite
⊢ ↑s.ncard = s.encard

Tactic:
rwa [ncard, ENat.natCast_toNat_eq_self, ne_eq, encard_eq_top_iff, Set.Infinite, not_not]

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ (↑s).ncard = s.card

Tactic:
by
  rw [ncard_eq_toFinset_card _, Finset.finite_toSet_toFinset]

Goal state after: