mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Module.ZLattice.Summable

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝² : DiscreteTopology ↥L
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι ℤ ↥L
n : ℕ
r : ℝ
s : ℕ → Finset (ι → ℤ) := fun n ↦ Fintype.piFinset fun i ↦ Icc (-↑n) ↑n
d : ℕ := Fintype.card ι
hr : r < -↑d
hr' : r < 0
hd : 1 ≤ d
hs0 : s 0 = {0}
hs : ∀ {a b : ℕ}, a ≤ b → s a ⊆ s b
this : ∀ (k : ℕ), #(s (k + 1) \ s k) ≤ 2 * d * (2 * k + 3) ^ (d - 1)
ε : ℝ := normBound b
hε : 0 < ε
⊢ 2 * ↑d * 3 ^ (d - 1) * ε ^ r * ∑ k ∈ range (n + 1), ↑k ^ (↑d - 1 + r) ≤
    2 * ↑d * 3 ^ (d - 1) * ε ^ r * ∑' (k : ℕ), ↑k ^ (↑d - 1 + r)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.ZLattice.Summable

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝² : DiscreteTopology ↥L
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι ℤ ↥L
d : ℕ
hd : d = Fintype.card ι
n : ℕ
r : ℝ
hr : r < -↑d
⊢ ∑ p ∈ Fintype.piFinset fun x ↦ Icc (-↑n) ↑n, ‖∑ i, p i • b i‖ ^ r ≤
    2 * ↑d * 3 ^ (d - 1) * normBound b ^ r * ∑' (k : ℕ), ↑k ^ (↑d - 1 + r)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.ZLattice.Summable

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
h✝ : Subsingleton ↥L
r : ℝ
hr : r < -↑(finrank ℤ ↥L)
s : Finset ↥L
⊢ r ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.ZLattice.Summable

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
h✝ : Subsingleton ↥L
r : ℝ
hr✝ : r < -↑(finrank ℤ ↥L)
s : Finset ↥L
hr : r ≠ 0
x✝ : ℕ
⊢ 0 ≤ ↑x✝ ^ (↑(finrank ℤ ↥L) - 1 + r)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.PointwiseSMul

Goal state before:
pp: G : Type u_1
P : Type u_2
R : Type u_3
V : Type u_4
inst✝³ : Group G
inst✝² : MulAction G P
inst✝¹ : Semiring R
inst✝ : Zero V
f : R[G]
x : P → V
p : P
gh : G × P
⊢ gh ∈ Finset.SMulAntidiagonal p ⋯ ↔ f.coeff gh.1 ≠ 0 ∧ x gh.2 ≠ 0 ∧ gh.2 = gh.1⁻¹ • p

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.PointwiseSMul

Goal state before:
pp: G : Type u_1
P : Type u_2
R : Type u_3
V : Type u_4
inst✝⁴ : Group G
inst✝³ : MulAction G P
inst✝² : Semiring R
inst✝¹ : AddCommMonoid V
inst✝ : SMulWithZero R V
f : R[G]
x : P → V
p : P
hp : ((↑f.coeff.support).smulAntidiagonal (Function.support x) p).Finite
s : Set (G × P) := ↑(Finset.SMulAntidiagonal p hp)
x✝¹ : G × P
h₁ : x✝¹ ∈ s
x✝ : G × P
h₂ : x✝ ∈ s
h : x✝¹.1 = x✝.1
⊢ x✝¹ = x✝

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.ZLattice.Summable

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
h✝ : Nontrivial ↥L
I : Type u_1 := Free.ChooseBasisIndex ℤ ↥L
this : Fintype I
b : Basis I ℤ ↥L := Free.chooseBasis ℤ ↥L
d : ℕ := Fintype.card I
⊢ d ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.PointwiseSMul

Goal state before:
pp: G : Type u_1
P : Type u_2
R : Type u_3
V : Type u_4
inst✝⁴ : Group G
inst✝³ : MulAction G P
inst✝² : Semiring R
inst✝¹ : AddCommMonoid V
inst✝ : SMulWithZero R V
f : R[G]
x : P → V
p : P
hp : ((↑f.coeff.support).smulAntidiagonal (Function.support x) p).Finite
s : Set (G × P) := ↑(Finset.SMulAntidiagonal p hp)
h₁ : Set.InjOn Prod.fst s
g : G × P
hg : g ∈ s
⊢ g.1 ∈ ↑f.coeff.support

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.PointwiseSMul

Goal state before:
pp: G : Type u_1
P : Type u_2
R : Type u_3
V : Type u_4
inst✝⁴ : Group G
inst✝³ : MulAction G P
inst✝² : Semiring R
inst✝¹ : AddCommMonoid V
inst✝ : SMulWithZero R V
f : R[G]
x : P → V
p : P
hp : ((↑f.coeff.support).smulAntidiagonal (Function.support x) p).Finite
s : Set (G × P) := ↑(Finset.SMulAntidiagonal p hp)
h₁ : Set.InjOn Prod.fst s
h₂ : Set.MapsTo Prod.fst s ↑f.coeff.support
g : G
hg : g ∈ f.coeff.support
hgn : g ∉ Prod.fst '' s
⊢ f.coeff g = 0 ∨ ∀ (q : P), ¬x q = 0 → ¬g • q = p

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.ZLattice.Summable

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
h✝ : Nontrivial ↥L
I : Type u_1 := Free.ChooseBasisIndex ℤ ↥L
this : Fintype I
b : Basis I ℤ ↥L := Free.chooseBasis ℤ ↥L
d : ℕ := Fintype.card I
hd : d ≠ 0
ε : ℝ := normBound b
⊢ 2 * ↑d * 3 ^ (d - 1) > 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.ZLattice.Summable

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
h✝ : Nontrivial ↥L
I : Type u_1 := Free.ChooseBasisIndex ℤ ↥L
this : Fintype I
b : Basis I ℤ ↥L := Free.chooseBasis ℤ ↥L
d : ℕ := Fintype.card I
hd : d ≠ 0
ε : ℝ := normBound b
r : ℝ
hr : r < -↑d
u : Finset ↥L
e : (I → ℤ) ≃ₗ[ℤ] ↥L := (b.repr ≪≫ₗ Finsupp.linearEquivFunOnFinite ℤ ℤ I).symm
⊢ ↑u = ↑(Finset.image (⇑e.toAddEquiv.toEmbedding) (Finset.image (⇑e.symm.toAddEquiv.toEmbedding) u))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.ZLattice.Summable

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
h✝ : Nontrivial ↥L
I : Type u_1 := Free.ChooseBasisIndex ℤ ↥L
this : Fintype I
b : Basis I ℤ ↥L := Free.chooseBasis ℤ ↥L
d : ℕ := Fintype.card I
hd : d ≠ 0
ε : ℝ := normBound b
r : ℝ
hr : r < -↑d
u : Finset ↥L
e : (I → ℤ) ≃ₗ[ℤ] ↥L := (b.repr ≪≫ₗ Finsupp.linearEquivFunOnFinite ℤ ℤ I).symm
⊢ ↑u = ↑(Finset.image (⇑e.toAddEquiv.toEmbedding) (Finset.image (⇑e.symm.toAddEquiv.toEmbedding) u))

Tactic:
by simpa using (e.image_symm_image _).symm

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.PointwiseSMul

Goal state before:
pp: G : Type u_1
P : Type u_2
R : Type u_3
V : Type u_4
inst✝⁴ : Group G
inst✝³ : MulAction G P
inst✝² : Semiring R
inst✝¹ : AddCommMonoid V
inst✝ : SMulWithZero R V
f : R[G]
x : P → V
p : P
hp : ((↑f.coeff.support).smulAntidiagonal (Function.support x) p).Finite
s : Set (G × P) := ↑(Finset.SMulAntidiagonal p hp)
h₁ : Set.InjOn Prod.fst s
h₂ : Set.MapsTo Prod.fst s ↑f.coeff.support
g : G
hg : g ∈ f.coeff.support
hgn : g ∉ Prod.fst '' s
⊢ f.coeff g • x (g⁻¹ • p) = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.PointwiseSMul

Goal state before:
pp: G : Type u_1
P : Type u_2
R : Type u_3
V : Type u_4
inst✝⁴ : Group G
inst✝³ : MulAction G P
inst✝² : Semiring R
inst✝¹ : AddCommMonoid V
inst✝ : SMulWithZero R V
f : R[G]
x : P → V
p : P
⊢ (f • x) p = ∑ i ∈ f.coeff.support, f.coeff i • x (i⁻¹ • p)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.ToDirectSum

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : Semiring M
inst✝ : (m : M) → Decidable (m ≠ 0)
i : ι
m : M
⊢ ((of (fun x ↦ M) i) m).toAddMonoidAlgebra = AddMonoidAlgebra.single i m

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.ToDirectSum

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : Semiring M
inst✝ : (m : M) → Decidable (m ≠ 0)
f : M[ι]
⊢ f.toDirectSum.toAddMonoidAlgebra = f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.ToDirectSum

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : Semiring M
f g : M[ι]
⊢ (f * g).toDirectSum = f.toDirectSum * g.toDirectSum

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.ToDirectSum

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : Semiring M
inst✝ : (m : M) → Decidable (m ≠ 0)
⊢ toAddMonoidAlgebra 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.ToDirectSum

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : Semiring M
inst✝ : (m : M) → Decidable (m ≠ 0)
f g : ⨁ (x : ι), M
⊢ (f + g).toAddMonoidAlgebra = f.toAddMonoidAlgebra + g.toAddMonoidAlgebra

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.ToDirectSum

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝³ : DecidableEq ι
inst✝² : AddMonoid ι
inst✝¹ : Semiring M
inst✝ : (m : M) → Decidable (m ≠ 0)
n : ℕ
⊢ (↑n).toAddMonoidAlgebra = ↑n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.ZLattice.Summable

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
h✝ : Nontrivial ↥L
I : Type u_1 := Free.ChooseBasisIndex ℤ ↥L
this : Fintype I
b : Basis I ℤ ↥L := Free.chooseBasis ℤ ↥L
d : ℕ := Fintype.card I
hd : d ≠ 0
ε : ℝ := normBound b
r✝ : ℝ
hr✝ : r✝ < -↑d
e : (I → ℤ) ≃ₗ[ℤ] ↥L := (b.repr ≪≫ₗ Finsupp.linearEquivFunOnFinite ℤ ℤ I).symm
u : Finset (I → ℤ)
r : ℝ
hr : 0 < r
hr' : ↑u ⊆ Metric.closedBall 0 r
x : I → ℤ
hx : x ∈ u
⊢ max ⌊r⌋ 0 = ⌊r⌋

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.ToDirectSum

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : Ring M
inst✝ : (m : M) → Decidable (m ≠ 0)
f g : ⨁ (x : ι), M
⊢ (f - g).toAddMonoidAlgebra = f.toAddMonoidAlgebra - g.toAddMonoidAlgebra

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.ToDirectSum

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : Ring M
inst✝ : (m : M) → Decidable (m ≠ 0)
f : ⨁ (x : ι), M
⊢ (-f).toAddMonoidAlgebra = -f.toAddMonoidAlgebra

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.ToDirectSum

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝³ : DecidableEq ι
inst✝² : AddMonoid ι
inst✝¹ : Ring M
inst✝ : (m : M) → Decidable (m ≠ 0)
z : ℤ
⊢ (↑z).toAddMonoidAlgebra = ↑z

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.ToDirectSum

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝³ : DecidableEq ι
inst✝² : Zero ι
inst✝¹ : Semiring M
inst✝ : (m : M) → Decidable (m ≠ 0)
⊢ toAddMonoidAlgebra 1 = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.ToDirectSum

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝³ : DecidableEq ι
inst✝² : AddMonoid ι
inst✝¹ : Semiring M
inst✝ : (m : M) → Decidable (m ≠ 0)
f g : ⨁ (x : ι), M
⊢ (f * g).toAddMonoidAlgebra = f.toAddMonoidAlgebra * g.toAddMonoidAlgebra

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.ToDirectSum

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : Semiring M
f : M[ι]
n : ℕ
⊢ (f ^ n).toDirectSum = f.toDirectSum ^ n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.ToDirectSum

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝³ : DecidableEq ι
inst✝² : AddMonoid ι
inst✝¹ : Semiring M
inst✝ : (m : M) → Decidable (m ≠ 0)
f : ⨁ (x : ι), M
n : ℕ
⊢ (f ^ n).toAddMonoidAlgebra = f.toAddMonoidAlgebra ^ n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.ZLattice.Summable

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
h✝ : Nontrivial ↥L
I : Type u_1 := Free.ChooseBasisIndex ℤ ↥L
this : Fintype I
b : Basis I ℤ ↥L := Free.chooseBasis ℤ ↥L
d : ℕ := Fintype.card I
hd : d ≠ 0
ε : ℝ := normBound b
r : ℝ
hr : r < -↑d
e : (I → ℤ) ≃ₗ[ℤ] ↥L := (b.repr ≪≫ₗ Finsupp.linearEquivFunOnFinite ℤ ℤ I).symm
u : Finset (I → ℤ)
⊢ ∃ n, u ⊆ Fintype.piFinset fun x ↦ Finset.Icc (-↑n) ↑n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Cardinal

Goal state before:
pp: σ : Type u
R : Type v
inst✝² : CommSemiring R
inst✝¹ : Nonempty σ
inst✝ : Nontrivial R
⊢ #(MvPolynomial σ R) = max (max (lift.{u, v} #R) (lift.{v, u} #σ)) ℵ₀

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Cardinal

Goal state before:
pp: σ : Type u
R : Type v
inst✝¹ : CommSemiring R
inst✝ : IsEmpty σ
⊢ #(MvPolynomial σ R) = lift.{u, v} #R

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Cardinal

Goal state before:
pp: σ : Type u
R : Type v
inst✝ : CommSemiring R
⊢ #(MvPolynomial σ R) ≤ max (max (lift.{u, v} #R) (lift.{v, u} #σ)) ℵ₀

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Cardinal

Goal state before:
pp: σ R : Type u
inst✝² : CommSemiring R
inst✝¹ : Nonempty σ
inst✝ : Nontrivial R
⊢ #(MvPolynomial σ R) = max (max #R #σ) ℵ₀

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Cardinal

Goal state before:
pp: σ R : Type u
inst✝¹ : CommSemiring R
inst✝ : IsEmpty σ
⊢ #(MvPolynomial σ R) = #R

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Cardinal

Goal state before:
pp: σ R : Type u
inst✝ : CommSemiring R
⊢ max (max (lift.{u, u} #R) (lift.{u, u} #σ)) ℵ₀ ≤ max (max #R #σ) ℵ₀

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.GetD

Goal state before:
pp: α : Type u
l : List α
d : α
n : ℕ
hn : n < l.length
⊢ l.getD n d = l[n]

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.GetD

Goal state before:
pp: α : Type u
β : Type v
l : List α
x : α
xs : List α
n : ℕ
d : α
i : Fin l.length
⊢ l[i]?.isSome = true

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.GetD

Goal state before:
pp: α : Type u
l : List α
d : α
i : Fin l.length
⊢ l.getD (↑i) d = l[i]?.get ⋯

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.GetD

Goal state before:
pp: α : Type u
β : Type v
l : List α
d : α
n : ℕ
f : α → β
⊢ (map f l).getD n (f d) = f (l.getD n d)

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.GetD

Goal state before:
pp: α : Type u
l : List α
d : α
n : ℕ
hn : l.length ≤ n
⊢ l.getD n d = d

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.GetD

Goal state before:
pp: α : Type u
l : List α
i : ℕ
h : i < l.length
⊢ l.reverse.getD i = l.getD (l.length - 1 - i)

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.GetD

Goal state before:
pp: α : Type u
d : α
n : ℕ
⊢ [d][n]?.getD d = d

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.GetD

Goal state before:
pp: α : Type u
d : α
r n : ℕ
⊢ (replicate r d)[n]?.getD d = d

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.GetD

Goal state before:
pp: α : Type u
x y : α
i n : ℕ
h : i < n
⊢ (replicate n x).getD i y = x

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.GetD

Goal state before:
pp: α : Type u
l l' : List α
d : α
n : ℕ
h : n < l.length
⊢ (l ++ l').getD n d = l.getD n d

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.GetD

Goal state before:
pp: α : Type u
l l' : List α
d : α
n : ℕ
h : l.length ≤ n
⊢ (l ++ l').getD n d = l'.getD (n - l.length) d

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.GetD

Goal state before:
pp: α : Type u
l : List α
d : α
⊢ (Function.Surjective fun x ↦ l.getD x d) ↔ ∀ (x : α), x = d ∨ x ∈ l

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.GetD

Goal state before:
pp: α : Type u
l : List α
inst✝ : Inhabited α
n : ℕ
⊢ l.getI n = l[n]?.getD default

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.GetD

Goal state before:
pp: α : Type u
l : List α
inst✝ : Inhabited α
⊢ l.getI 0 = l.headI

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.ToFinsupp

Goal state before:
pp: M : Type u_1
inst✝¹ : Zero M
l : List M
inst✝ : DecidablePred fun x ↦ l.getD x 0 ≠ 0
n✝ n : ℕ
⊢ n ∈ {i ∈ Finset.range l.length | l.getD i 0 ≠ 0} ↔ l.getD n 0 ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.ToFinsupp

Goal state before:
pp: M : Type u_1
inst✝¹ : Zero M
l : List M
inst✝ : DecidablePred fun x ↦ l.getD x 0 ≠ 0
⊢ l.toFinsupp.support ⊆ Finset.range l.length

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.ToFinsupp

Goal state before:
pp: M : Type u_1
inst✝¹ : Zero M
inst✝ : DecidablePred fun i ↦ [].getD i 0 ≠ 0
⊢ [].toFinsupp = 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.ToFinsupp

Goal state before:
pp: M : Type u_1
inst✝¹ : Zero M
x : M
inst✝ : DecidablePred fun x_1 ↦ [x].getD x_1 0 ≠ 0
⊢ [x].toFinsupp = Finsupp.single 0 x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.ZLattice.Summable

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
h✝ : Nontrivial ↥L
I : Type u_1 := Free.ChooseBasisIndex ℤ ↥L
this : Fintype I
b : Basis I ℤ ↥L := Free.chooseBasis ℤ ↥L
d : ℕ := Fintype.card I
hd : d ≠ 0
ε : ℝ := normBound b
r : ℝ
hr : r < -↑d
e : (I → ℤ) ≃ₗ[ℤ] ↥L := (b.repr ≪≫ₗ Finsupp.linearEquivFunOnFinite ℤ ℤ I).symm
u : Finset (I → ℤ)
n : ℕ
hn : u ⊆ Fintype.piFinset fun x ↦ Finset.Icc (-↑n) ↑n
⊢ ∀ i ∈ Fintype.piFinset fun x ↦ Finset.Icc (-↑n) ↑n, i ∉ u → 0 ≤ ‖↑(e i)‖ ^ r

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.ToFinsupp

Goal state before:
pp: R : Type u_2
inst✝³ : AddZeroClass R
l₁ l₂ : List R
inst✝² : DecidablePred fun x ↦ (l₁ ++ l₂).getD x 0 ≠ 0
inst✝¹ : DecidablePred fun x ↦ l₁.getD x 0 ≠ 0
inst✝ : DecidablePred fun x ↦ l₂.getD x 0 ≠ 0
⊢ (l₁ ++ l₂).toFinsupp = l₁.toFinsupp + Finsupp.embDomain (addLeftEmbedding l₁.length) l₂.toFinsupp

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.ToFinsupp

Goal state before:
pp: R : Type u_2
inst✝² : AddZeroClass R
x : R
xs : List R
inst✝¹ : DecidablePred fun x_1 ↦ (x :: xs).getD x_1 0 ≠ 0
inst✝ : DecidablePred fun x ↦ xs.getD x 0 ≠ 0
⊢ (x :: xs).toFinsupp = Finsupp.single 0 x + Finsupp.embDomain (addRightEmbedding 1) xs.toFinsupp

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.ZLattice.Summable

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
h✝ : Nontrivial ↥L
I : Type u_1 := Free.ChooseBasisIndex ℤ ↥L
this : Fintype I
b : Basis I ℤ ↥L := Free.chooseBasis ℤ ↥L
d : ℕ := Fintype.card I
hd : d ≠ 0
ε : ℝ := normBound b
⊢ ∃ A > 0, ∃ B > 0, ∀ r < -↑d, ∀ (s : Finset ↥L), ∑ z ∈ s, ‖z‖ ^ r ≤ A * B ^ r * ∑' (k : ℕ), ↑k ^ (↑d - 1 + r)

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.ToFinsupp

Goal state before:
pp: R : Type u_2
inst✝² : AddZeroClass R
x : R
xs : List R
inst✝¹ : DecidablePred fun i ↦ (xs ++ [x]).getD i 0 ≠ 0
inst✝ : DecidablePred fun i ↦ xs.getD i 0 ≠ 0
⊢ (xs ++ [x]).toFinsupp = xs.toFinsupp + Finsupp.single xs.length x

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.ToFinsupp

Goal state before:
pp: R : Type u_2
inst✝¹ : AddMonoid R
l : List R
inst✝ : DecidablePred fun x ↦ l.getD x 0 ≠ 0
⊢ l.toFinsupp = (mapIdx (fun n r ↦ Finsupp.single n r) l).sum

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.ZLattice.Covolume

Goal state before:
pp: E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
L : Submodule ℤ E
inst✝² : DiscreteTopology ↥L
inst✝¹ : IsZLattice ℝ L
inst✝ : Nontrivial E
X : Set E
F : E → ℝ
hX : ∀ ⦃x : E⦄ ⦃r : ℝ⦄, x ∈ X → 0 < r → r • x ∈ X
h₁ : ∀ (x : E) ⦃r : ℝ⦄, 0 ≤ r → F (r • x) = r ^ finrank ℝ E * F x
h₂ : Bornology.IsBounded {x | x ∈ X ∧ F x ≤ 1}
h₃ : MeasurableSet {x | x ∈ X ∧ F x ≤ 1}
h₄ : volume (frontier {x | x ∈ X ∧ F x ≤ 1}) = 0
⊢ Tendsto (fun c ↦ ↑(Nat.card ↑({x | x ∈ X ∧ F x ≤ c} ∩ ↑L)) / c) atTop
    (𝓝 (volume.real {x | x ∈ X ∧ F x ≤ 1} / covolume L volume))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.ZLattice.Summable

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
h✝ : Nontrivial ↥L
I : Type u_1 := Free.ChooseBasisIndex ℤ ↥L
this : Fintype I
b : Basis I ℤ ↥L := Free.chooseBasis ℤ ↥L
d : ℕ := Fintype.card I
hd : d ≠ 0
ε : ℝ := normBound b
A : ℝ
hA : A > 0
B : ℝ
hB : B > 0
H : ∀ r < -↑d, ∀ (s : Finset ↥L), ∑ z ∈ s, ‖z‖ ^ r ≤ A * B ^ r * ∑' (k : ℕ), ↑k ^ (↑d - 1 + r)
hA' : A ≤ 1
r : ℝ
hr : r < -↑d
s : Finset ↥L
⊢ 0 ≤ B ^ r

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.ZLattice.Summable

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
h✝ : Nontrivial ↥L
I : Type u_1 := Free.ChooseBasisIndex ℤ ↥L
this : Fintype I
b : Basis I ℤ ↥L := Free.chooseBasis ℤ ↥L
d : ℕ := Fintype.card I
hd : d ≠ 0
ε : ℝ := normBound b
A : ℝ
hA : A > 0
B : ℝ
hB : B > 0
H : ∀ r < -↑d, ∀ (s : Finset ↥L), ∑ z ∈ s, ‖z‖ ^ r ≤ A * B ^ r * ∑' (k : ℕ), ↑k ^ (↑d - 1 + r)
hA' : A ≤ 1
r : ℝ
hr : r < -↑d
s : Finset ↥L
⊢ 0 ≤ ∑' (k : ℕ), ↑k ^ (↑d - 1 + r)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.BoxIntegral.Basic

Goal state before:
pp: ι : Type u
E : Type v
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : Fintype ι
l : IntegrationParams
inst✝¹ : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
hc : ∀ᵐ (x : ι → ℝ) ∂μ.restrict (Box.Icc I), ContinuousWithinAt f (Box.Icc I) x
ε : ℝ
ε0 : ε > 0
ε₁ : ℝ
ε₁0 : 0 < ε₁
hε₁ : 2 * μ.toBoxAdditive I * ε₁ < ε
C : ℝ
hC : ∀ x ∈ Box.Icc I, ‖f x‖ ≤ C
C0 : 0 ≤ C
ε₂ : ℝ
ε₂0 : 0 < ε₂
hε₂ : 4 * C * ε₂ < ε
ε₂0' : ENNReal.ofReal ε₂ ≠ 0
D : Set (ι → ℝ) := {x | x ∈ Box.Icc I ∧ ¬ContinuousWithinAt f (Box.Icc I) x}
μ' : Measure (ι → ℝ) := μ.restrict (Box.Icc I)
μ'D : μ' D = 0
U : Set (ι → ℝ)
UD : U ⊇ D
Uopen : IsOpen U
hU : μ' U < ENNReal.ofReal ε₂
comp : IsCompact (Box.Icc I \ U)
this : ∀ x ∈ Box.Icc I \ U, oscillationWithin f (Box.Icc I) x < ENNReal.ofReal ε₁
r : ℝ
r0 : r > 0
hr : ∀ x ∈ Box.Icc I \ U, ediam (f '' (eball x (ENNReal.ofReal r) ∩ Box.Icc I)) ≤ ENNReal.ofReal ε₁
c₁ c₂ : ℝ≥0
π₁ π₂ : TaggedPrepartition I
h₁ : l.MemBaseSet I c₁ ((fun x x_1 ↦ ⟨r / 2, ⋯⟩) c₁) π₁
h₁p : π₁.IsPartition
h₂ : l.MemBaseSet I c₂ ((fun x x_1 ↦ ⟨r / 2, ⋯⟩) c₂) π₂
h₂p : π₂.IsPartition
μI : μ ↑I < ∞
t₁ : Box ι → ι → ℝ := fun J ↦ (π₁.infPrepartition π₂.toPrepartition).tag J
t₂ : Box ι → ι → ℝ := fun J ↦ (π₂.infPrepartition π₁.toPrepartition).tag J
B : Finset (Box ι) := (π₁.toPrepartition ⊓ π₂.toPrepartition).boxes
B' : Finset (Box ι) := {J ∈ B | ↑J ⊆ U}
hB' : B' ⊆ B
μJ_ne_top : ∀ J ∈ B, μ ↑J ≠ ∞
un : ∀ S ⊆ B, ⋃ J ∈ S, ↑J ⊆ ↑I
⊢ ∀ J ∈ B', ‖μ.toBoxAdditive J • (f (t₁ J) - f (t₂ J))‖ ≤ μ.toBoxAdditive J * (2 * C)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.ZLattice.Summable

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
⊢ ∃ A > 0,
    ∀ r < -↑(finrank ℤ ↥L), ∀ (s : Finset ↥L), ∑ z ∈ s, ‖z‖ ^ r ≤ A ^ r * ∑' (k : ℕ), ↑k ^ (↑(finrank ℤ ↥L) - 1 + r)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.ZLattice.Summable

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
r : ℝ
hr : r < -↑(finrank ℤ ↥L)
x✝ : ↥L
⊢ 0 x✝ ≤ ‖x✝‖ ^ r

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.ZLattice.Summable

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
r : ℝ
hr : r < -↑(finrank ℤ ↥L)
x : E
h✝ : Nontrivial ↥L
H : IsClosed ↑L
t : ↥L
ht : t ∈ {x_1 | (fun i ↦ ‖‖↑i - x‖ ^ r‖ ≤ (1 / 2) ^ r * ‖i‖ ^ r) x_1}ᶜ
ht₁ : ¬‖t‖ = 0
ht₂ : ¬‖↑t - x‖ = 0
this : 0 < finrank ℤ ↥L
⊢ 0 < 2⁻¹ * ‖t‖

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.ZLattice.Summable

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
r : ℝ
hr : r < -↑(finrank ℤ ↥L)
x : E
h✝ : Nontrivial ↥L
H : IsClosed ↑L
t : ↥L
ht : t ∈ {x_1 | (fun i ↦ ‖‖↑i - x‖ ^ r‖ ≤ (1 / 2) ^ r * ‖i‖ ^ r) x_1}ᶜ
ht₁ : ¬‖t‖ = 0
ht₂ : ¬‖↑t - x‖ = 0
this : 0 < finrank ℤ ↥L
⊢ 0 < ‖↑t - x‖

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorial.DoubleFactorial

Goal state before:
pp: n : ℕ
⊢ (n + 1)‼ = (n + 1) * (n - 1)‼

Tactic:
by

Goal state after: