mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.InnerProductSpace.PiL2

Goal state before:
pp: case e'_3.e'_5
ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst✝⁷ : RCLike 𝕜
E : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
F : Type u_5
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
F' : Type u_6
inst✝² : NormedAddCommGroup F'
inst✝¹ : InnerProductSpace ℝ F'
inst✝ : Fintype ι
v : Basis ι 𝕜 E
hv : Orthonormal 𝕜 ⇑v
x y : E
p : EuclideanSpace 𝕜 ι := toLp 2 (v.equivFun x)
q : EuclideanSpace 𝕜 ι := toLp 2 (v.equivFun y)
key : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ y = ∑ i, q.ofLp i • v i

Tactic:
rw [← v.equivFun.symm_apply_apply y, v.equivFun_symm_apply]

Goal state after:
Module: Mathlib.Analysis.BoxIntegral.Partition.Filter

Goal state before:
pp: ι : Type u_2
l : IntegrationParams
hl : l.bRiemann = false
r : (ι → ℝ) → ↑(Set.Ioi 0)
⊢ l.RCond r

Tactic:
simp [RCond, hl]

Goal state after:
Module: Mathlib.Analysis.BoxIntegral.Partition.Filter

Goal state before:
pp: case refine_2
ι : Type u_1
inst✝ : Fintype ι
I : Box ι
c : ℝ≥0
l : IntegrationParams
r : (ι → ℝ) → ↑(Set.Ioi 0)
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
h : ∀ J ∈ π, l.MemBaseSet J c r (πi J)
hp : ∀ J ∈ π, (πi J).IsPartition
hc : l.bDistortion = true → π.compl.distortion ≤ c
hD : l.bDistortion = true
⊢ ∃ π', π'.iUnion = ↑I \ (π.biUnionTagged πi).iUnion ∧ π'.distortion ≤ c

Tactic:
· refine ⟨_, ?_, hc hD⟩
    rw [π.iUnion_compl, ← π.iUnion_biUnion_partition hp]
    rfl

Goal state after:
Module: Mathlib.Analysis.BoxIntegral.Partition.Filter

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
l : IntegrationParams
h : I ≤ J
⊢ Tendsto (⇑(embedBox I J h)) (toFilteriUnion I ⊤) (toFilteriUnion J (Prepartition.single J I h))

Tactic:
by
  simp only [toFilteriUnion, tendsto_iSup]; intro c
  set π₀ := Prepartition.single J I h
  refine le_iSup_of_le (max c π₀.compl.distortion) ?_
  refine ((l.hasBasis_toFilterDistortioniUnion I c ⊤).tendsto_iff
    (l.hasBasis_toFilterDistortioniUnion J _ _)).2 fun r hr => ?_
  refine ⟨r, hr, fun π hπ => ?_⟩
  rw [mem_ofPred_eq, Prepartition.iUnion_top] at hπ
  refine ⟨⟨hπ.1.1, hπ.1.2, fun hD => le_trans (hπ.1.3 hD) (le_max_left _ _), fun _ => ?_⟩, ?_⟩
  · refine ⟨_, π₀.iUnion_compl.trans ?_, le_max_right _ _⟩
    congr 1
    exact (Prepartition.iUnion_single h).trans hπ.2.symm
  · exact hπ.2.trans (Prepartition.iUnion_single _).symm

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.PiL2

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
this✝ : Unique ι
this : b default = 1 ∨ b default = -1
⊢ (⇑b = fun x ↦ 1) ∨ ⇑b = fun x ↦ -1

Tactic:
rw [eq_const_of_unique b]

Goal state after:
ι : Type u_1
inst✝ : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
this✝ : Unique ι
this : b default = 1 ∨ b default = -1
⊢ (const ι (b default) = fun x ↦ 1) ∨ const ι (b default) = fun x ↦ -1
Module: Mathlib.Analysis.InnerProductSpace.PiL2

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst✝¹⁰ : RCLike 𝕜
E✝ : Type u_4
inst✝⁹ : NormedAddCommGroup E✝
inst✝⁸ : InnerProductSpace 𝕜 E✝
F : Type u_5
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : InnerProductSpace ℝ F
F' : Type u_6
inst✝⁵ : NormedAddCommGroup F'
inst✝⁴ : InnerProductSpace ℝ F'
inst✝³ : Fintype ι
V : Type u_7
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace 𝕜 V
inst✝ : FiniteDimensional 𝕜 V
S : Submodule 𝕜 V
L✝ L : ↥S →ₗᵢ[𝕜] V
d : ℕ := finrank 𝕜 ↥Sᗮ
LS : Submodule 𝕜 V := L.range
E : ↥Sᗮ ≃ₗᵢ[𝕜] ↥LSᗮ
L3 : ↥Sᗮ →ₗᵢ[𝕜] V := LSᗮ.subtypeₗᵢ.comp E.toLinearIsometry
this✝ : CompleteSpace ↥S
this : CompleteSpace V
⊢ V →ₗᵢ[𝕜] V

Tactic:
let p1 := S.orthogonalProjectionOnto.toLinearMap

Goal state after:
ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst✝¹⁰ : RCLike 𝕜
E✝ : Type u_4
inst✝⁹ : NormedAddCommGroup E✝
inst✝⁸ : InnerProductSpace 𝕜 E✝
F : Type u_5
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : InnerProductSpace ℝ F
F' : Type u_6
inst✝⁵ : NormedAddCommGroup F'
inst✝⁴ : InnerProductSpace ℝ F'
inst✝³ : Fintype ι
V : Type u_7
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace 𝕜 V
inst✝ : FiniteDimensional 𝕜 V
S : Submodule 𝕜 V
L✝ L : ↥S →ₗᵢ[𝕜] V
d : ℕ := finrank 𝕜 ↥Sᗮ
LS : Submodule 𝕜 V := L.range
E : ↥Sᗮ ≃ₗᵢ[𝕜] ↥LSᗮ
L3 : ↥Sᗮ →ₗᵢ[𝕜] V := LSᗮ.subtypeₗᵢ.comp E.toLinearIsometry
this✝ : CompleteSpace ↥S
this : CompleteSpace V
p1 : V →ₗ[𝕜] ↥S := ↑S.orthogonalProjectionOnto
⊢ V →ₗᵢ[𝕜] V
Module: Mathlib.Analysis.BoxIntegral.UnitPartition

Goal state before:
pp: ι : Type u_1
n : ℕ
inst✝ : NeZero n
x : ι → ℝ
ν : ι → ℤ
⊢ (∀ (i : ι), ↑(ν i) < ↑n * x i ∧ ↑n * x i ≤ ↑(ν i) + 1) ↔ ∀ (x_1 : ι), index n x x_1 = ν x_1

Tactic:
index_apply,

Goal state after:
ι : Type u_1
n : ℕ
inst✝ : NeZero n
x : ι → ℝ
ν : ι → ℤ
⊢ (∀ (i : ι), ↑(ν i) < ↑n * x i ∧ ↑n * x i ≤ ↑(ν i) + 1) ↔ ∀ (x_1 : ι), ⌈↑n * x x_1⌉ - 1 = ν x_1
Module: Mathlib.Analysis.BoxIntegral.UnitPartition

Goal state before:
pp: ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
B I : Box ι
⊢ (if hI : ∃ ν ∈ admissibleIndex n B, I = box n ν then tag n hI.choose else ⋯.choose) ∈ Box.Icc B

Tactic:
by_cases hI : ∃ ν ∈ admissibleIndex n B, I = box n ν

Goal state after:
case pos
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
B I : Box ι
hI : ∃ ν ∈ admissibleIndex n B, I = box n ν
⊢ (if hI : ∃ ν ∈ admissibleIndex n B, I = box n ν then tag n hI.choose else ⋯.choose) ∈ Box.Icc B

case neg
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
B I : Box ι
hI : ¬∃ ν ∈ admissibleIndex n B, I = box n ν
⊢ (if hI : ∃ ν ∈ admissibleIndex n B, I = box n ν then tag n hI.choose else ⋯.choose) ∈ Box.Icc B
Module: Mathlib.Analysis.BoxIntegral.UnitPartition

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
x : ℝ
a : ℤ
⊢ ↑a < x ↔ ↑a ≤ (↑⌈↑n * x⌉ - 1) / ↑n

Tactic:
have h : 0 < (n : ℝ) := Nat.cast_pos.mpr <| n.pos_of_neZero
  rw [le_div_iff₀' h, le_sub_iff_add_le,
    show (n : ℝ) * a + 1 = (n * a + 1 : ℤ) by norm_cast,
    Int.cast_le, Int.add_one_le_iff, Int.lt_ceil, Int.cast_mul, Int.cast_natCast,
    mul_lt_mul_iff_right₀ h]

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

Goal state before:
pp: ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
B : Box ι
x : ι → ℝ
hx : x ∈ B
l u : ι → ℤ
hl : ∀ (i : ι), B.lower i = ↑(l i)
hu : ∀ (i : ι), B.upper i = ↑(u i)
⊢ (∀ (i : ι), B.lower i ≤ ↑(index n x i) / ↑n) ∧ ∀ (i : ι), (↑(index n x i) + 1) / ↑n ≤ B.upper i

Tactic:
index_apply,

Goal state after:
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
B : Box ι
x : ι → ℝ
hx : x ∈ B
l u : ι → ℤ
hl : ∀ (i : ι), B.lower i = ↑(l i)
hu : ∀ (i : ι), B.upper i = ↑(u i)
⊢ (∀ (i : ι), B.lower i ≤ ↑(⌈↑n * x i⌉ - 1) / ↑n) ∧ ∀ (i : ι), (↑(⌈↑n * x i⌉ - 1) + 1) / ↑n ≤ B.upper i
Module: Mathlib.Analysis.BoxIntegral.UnitPartition

Goal state before:
pp: ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Finite ι
x : ι → ℝ
hx : ∀ (i : ι), ↑n * x i ∈ Set.range ⇑(algebraMap ℤ ℝ)
i : ι
a : ℤ
ha : ↑a = ↑n * x i
⊢ (↑(index n x i) + 1) / ↑n = x i

Tactic:
index_apply,

Goal state after:
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Finite ι
x : ι → ℝ
hx : ∀ (i : ι), ↑n * x i ∈ Set.range ⇑(algebraMap ℤ ℝ)
i : ι
a : ℤ
ha : ↑a = ↑n * x i
⊢ (↑(⌈↑n * x i⌉ - 1) + 1) / ↑n = x i
Module: Mathlib.Algebra.Module.ZLattice.Covolume

Goal state before:
pp: E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : FiniteDimensional ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
L : Submodule ℤ E
inst✝⁴ : DiscreteTopology ↥L
inst✝³ : IsZLattice ℝ L
μ : Measure E
inst✝² : μ.IsAddHaarMeasure
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι ℤ ↥L
b₀ : Basis ι ℝ E
⊢ covolume L μ = |b₀.det (Subtype.val ∘ ⇑b)| * μ.real (fundamentalDomain b₀)

Tactic:
covolume_eq_measure_fundamentalDomain L μ (isAddFundamentalDomain b μ),

Goal state after:
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : FiniteDimensional ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
L : Submodule ℤ E
inst✝⁴ : DiscreteTopology ↥L
inst✝³ : IsZLattice ℝ L
μ : Measure E
inst✝² : μ.IsAddHaarMeasure
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι ℤ ↥L
b₀ : Basis ι ℝ E
⊢ μ.real (fundamentalDomain (Basis.ofZLatticeBasis ℝ L b)) = |b₀.det (Subtype.val ∘ ⇑b)| * μ.real (fundamentalDomain b₀)
Module: Mathlib.Analysis.SumOverResidueClass

Goal state before:
pp: f : ℕ → ℝ
hf : Antitone f
n : ℕ
hn : f n < 0
hs : Summable f
this : ∀ ε > 0, ∃ N, ∀ n ≥ N, |f n| < ε
N : ℕ
H : f (max n N) ≤ f n
⊢ |f n| ≤ |f (max n N)|

Tactic:
rwa [abs_of_neg hn, abs_of_neg (H.trans_lt hn), neg_le_neg_iff]

Goal state after:
Module: Mathlib.Analysis.SumOverResidueClass

Goal state before:
pp: f : ℕ → ℝ
hf : Antitone f
n : ℕ
hn : f n < 0
⊢ ¬Summable f

Tactic:
intro hs
  have := hs.tendsto_atTop_zero
  simp only [Metric.tendsto_atTop, dist_zero_right, Real.norm_eq_abs] at this
  obtain ⟨N, hN⟩ := this (|f n|) (abs_pos_of_neg hn)
  specialize hN (max n N) (n.le_max_right N)
  contrapose! hN; clear hN
  have H : f (max n N) ≤ f n := hf (n.le_max_left N)
  rwa [abs_of_neg hn, abs_of_neg (H.trans_lt hn), neg_le_neg_iff]

Goal state after:
Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics

Goal state before:
pp: case mp
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
D : Type u_2
inst✝ : TopologicalSpace D
f : D → E
hf : Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
c : ℝ
hc : ∀ x ∈ range f, ‖x‖ ≤ c
⊢ f =O[cocompact D] 1

Tactic:
simp only [Set.mem_range, forall_exists_index, forall_apply_eq_imp_iff] at hc

Goal state after:
case mp
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
D : Type u_2
inst✝ : TopologicalSpace D
f : D → E
hf : Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
c : ℝ
hc : ∀ (a : D), ‖f a‖ ≤ c
⊢ f =O[cocompact D] 1
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: b : ℝ
hb : 1 < b
⊢ Summable fun n ↦ |↑n| ^ (-b)

Tactic:
apply Summable.of_nat_of_neg

Goal state after:
case hf₁
b : ℝ
hb : 1 < b
⊢ Summable fun n ↦ |↑↑n| ^ (-b)

case hf₂
b : ℝ
hb : 1 < b
⊢ Summable fun n ↦ |↑(-↑n)| ^ (-b)
Module: Mathlib.Algebra.Module.ZLattice.Summable

Goal state before:
pp: E✝ : Type u_1
inst✝⁴ : NormedAddCommGroup E✝
L✝ : Submodule ℤ E✝
ι✝ : Type u_2
b✝ : Basis ι✝ ℤ ↥L✝
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
ι : Type u_2
b : Basis ι ℤ ↥L
H : IsZLattice ℝ L
⊢ ∃ ε, 0 < ε ∧ ∀ (x : ↥L) (i : ι), ε * ↑|(b.repr x) i| ≤ ‖x‖

Tactic:
have : Finite ι := Module.Finite.finite_basis b

Goal state after:
E✝ : Type u_1
inst✝⁴ : NormedAddCommGroup E✝
L✝ : Submodule ℤ E✝
ι✝ : Type u_2
b✝ : Basis ι✝ ℤ ↥L✝
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
ι : Type u_2
b : Basis ι ℤ ↥L
H : IsZLattice ℝ L
this : Finite ι
⊢ ∃ ε, 0 < ε ∧ ∀ (x : ↥L) (i : ι), ε * ↑|(b.repr x) i| ≤ ‖x‖
Module: Mathlib.Algebra.MonoidAlgebra.Ideal

Goal state before:
pp: k : Type u_1
G : Type u_3
inst✝¹ : Monoid G
inst✝ : Semiring k
s : Set G
x : k[G]
RHS : Ideal k[G] :=
  { carrier := {p | ∀ m ∈ p.coeff.support, ∃ m' ∈ s, ∃ d, m = d * m'}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
hx : x ∈ RHS
d : G
hd : d ∈ s
d2 : G
hi : d2 * d ∈ x.coeff.support
⊢ single (d2 * d) (x.coeff (d2 * d)) ∈ Ideal.span (⇑(of k G) '' s)

Tactic:
simpa using Ideal.mul_mem_left _ (.single d2 <| x.coeff (d2 * d)) (b := of k G d)
      (Ideal.subset_span <| Set.mem_image_of_mem _ hd)

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

Goal state before:
pp: G : Type u_1
P : Type u_2
s : Set G
inst✝¹ : SMul G P
inst✝ : IsLeftCancelSMul G P
hs : s.Finite
t : Set P
p : P
x✝⁴ : G × P
x✝³ : x✝⁴ ∈ s.smulAntidiagonal t p
x✝² : G × P
x✝¹ : x✝² ∈ s.smulAntidiagonal t p
x✝ : x✝⁴.1 = x✝².1
⊢ x✝⁴ = x✝²

Tactic:
grind only [mem_smulAntidiagonal, IsLeftCancelSMul.left_cancel]

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
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 < ε
⊢ ∑ k ∈ range n, ↑(2 * d * (3 * (k + 1)) ^ (d - 1)) * ((↑k + 1) * ε) ^ r =
    2 * ↑d * 3 ^ (d - 1) * ε ^ r * ∑ k ∈ range n, (↑k + 1) ^ (d - 1) * (↑k + 1) ^ r

Tactic:
simp_rw [Finset.mul_sum]

Goal state after:
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 < ε
⊢ ∑ k ∈ range n, ↑(2 * d * (3 * (k + 1)) ^ (d - 1)) * ((↑k + 1) * ε) ^ r =
    ∑ i ∈ range n, 2 * ↑d * 3 ^ (d - 1) * ε ^ r * ((↑i + 1) ^ (d - 1) * (↑i + 1) ^ r)
Module: Mathlib.Data.Nat.Factorial.DoubleFactorial

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

Tactic:
mul_comm (2 * n + 1)‼,

Goal state after:
n : ℕ
⊢ (2 * (n + 1) + 1)‼ = (2 * (n + 1) + 1) * (2 * n + 1)‼
Module: Mathlib.Algebra.MvPolynomial.Coeff

Goal state before:
pp: case neg
R : Type u_1
σ : Type u_2
inst✝ : CommSemiring R
s : σ →₀ ℕ
a : σ →₀ R
n : ℕ
hs : (s.sum fun x m ↦ m) = n
hs' : ¬s.support ⊆ a.support
⊢ 0 = ↑s.multinomial * s.prod fun r m ↦ a r ^ m

Tactic:
rw [Finset.subset_iff] at hs'

Goal state after:
case neg
R : Type u_1
σ : Type u_2
inst✝ : CommSemiring R
s : σ →₀ ℕ
a : σ →₀ R
n : ℕ
hs : (s.sum fun x m ↦ m) = n
hs' : ¬∀ ⦃x : σ⦄, x ∈ s.support → x ∈ a.support
⊢ 0 = ↑s.multinomial * s.prod fun r m ↦ a r ^ m
Module: Mathlib.Algebra.MvPolynomial.Coeff

Goal state before:
pp: R : Type u_1
σ : Type u_2
inst✝ : CommSemiring R
s : σ →₀ ℕ
a : σ →₀ R
n : ℕ
hs : (s.sum fun x m ↦ m) = n
⊢ coeff s ((linearCombination R X) a ^ n) = ↑s.multinomial * s.prod fun r m ↦ a r ^ m

Tactic:
by
  classical
  simp only [sum, linearCombination_apply, Finset.sum_pow_eq_sum_piAntidiag, coeff_sum,
    ← C_eq_coe_nat, coeff_C_mul, smul_eq_C_mul, mul_pow, Finset.prod_mul_distrib, ← map_pow,
    ← map_prod, coeff_prod_X_pow, mul_ite, mul_one, mul_zero]
  rw [Finset.sum_eq_single (s : σ → ℕ)]
  · simp_rw [eq_indicator_self_iff]
    split_ifs with hs'
    · rw [prod_of_support_subset _ hs' _ (by simp), Finsupp.multinomial_of_support_subset hs']
    · rw [Finset.subset_iff] at hs'
      simp only [Finsupp.mem_support_iff, ne_eq, not_forall, Decidable.not_not] at hs'
      obtain ⟨i, hsi, hai⟩ := hs'
      rw [← mul_prod_erase _ i _ (by simpa), hai, zero_pow hsi, zero_mul, mul_zero]
  · simp only [Finset.mem_piAntidiag, ne_eq, Finsupp.mem_support_iff, ite_eq_right_iff, and_imp]
    intro _ _ _ _ hed
    simp [Finsupp.ext_iff] at hed
    grind
  · simp_rw [ite_eq_right_iff]
    intro hs' hs''
    rw [eq_indicator_self_iff] at hs''
    exfalso
    rw [Finset.mem_piAntidiag, not_and_or] at hs'
    rcases hs' with hs' | hs'
    · apply hs'
      rw [← hs, sum_of_support_subset _ hs'' _ (by simp)]
    · grind

Goal state after:
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Semiring R
f : α → R
a : α
s : Finset α
has : a ∉ s
ih :
  ∀ (hc : (↑s).Pairwise (Commute on f)) (n : ℕ),
    (∑ i ∈ s, f i) ^ n = ∑ k ∈ s.piAntidiag n, ↑(multinomial s k) * s.noncommProd (fun i ↦ f i ^ k i) ⋯
hc : (↑(cons a s has)).Pairwise (Commute on f)
n : ℕ
this :
  ∀ p ∈ antidiagonal n,
    ∑ g ∈ s.piAntidiag p.2,
        ↑((g a + p.1 + s.sum g).choose (g a + p.1)) * ↑(multinomial s (g + fun i ↦ if i = a then p.1 else 0)) *
          (f a ^ (g a + p.1) * s.noncommProd (fun i ↦ f i ^ (g i + if i = a then p.1 else 0)) ⋯) =
      ∑ g ∈ s.piAntidiag p.2, ↑(n.choose p.1) * ↑(multinomial s g) * (f a ^ p.1 * s.noncommProd (fun i ↦ f i ^ g i) ⋯)
i : α
hi : i ∈ s
⊢ a ≠ i

Tactic:
by simpa [eq_comm] using ne_of_mem_of_not_mem hi has

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

Goal state before:
pp: case refine_1
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
P : MvPolynomial σ R
inst✝ : Finite σ
this : Fintype σ
⊢ ∀ (α β : Type u_1) [Fintype β] (e : α ≃ β),
    (∀ (x : MvPolynomial α R), IsNilpotent x ↔ ∀ (i : α →₀ ℕ), IsNilpotent (coeff i x)) →
      ∀ (x : MvPolynomial β R), IsNilpotent x ↔ ∀ (i : β →₀ ℕ), IsNilpotent (coeff i x)

Tactic:
intro α β _ e h₁ P

Goal state after:
case refine_1
σ : Type u_1
R : Type u_2
inst✝² : CommRing R
P✝ : MvPolynomial σ R
inst✝¹ : Finite σ
this : Fintype σ
α β : Type u_1
inst✝ : Fintype β
e : α ≃ β
h₁ : ∀ (x : MvPolynomial α R), IsNilpotent x ↔ ∀ (i : α →₀ ℕ), IsNilpotent (coeff i x)
P : MvPolynomial β R
⊢ IsNilpotent P ↔ ∀ (i : β →₀ ℕ), IsNilpotent (coeff i P)
Module: Mathlib.Algebra.MvPolynomial.Nilpotent

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommRing R
n : ℕ
f : Fin n → σ
hf : Function.Injective f
P : MvPolynomial (Fin n) R
⊢ IsNilpotent ((rename f) P) ↔ ∀ (i : σ →₀ ℕ), IsNilpotent (coeff i ((rename f) P))

Tactic:
IsNilpotent.map_iff (rename_injective _ hf),

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommRing R
n : ℕ
f : Fin n → σ
hf : Function.Injective f
P : MvPolynomial (Fin n) R
⊢ IsNilpotent P ↔ ∀ (i : σ →₀ ℕ), IsNilpotent (coeff i ((rename f) P))
Module: Mathlib.Algebra.Order.Ring.Finset

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝³ : LinearOrder R
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : CanonicallyOrderedAdd R
inst✝ : OrderBot R
s : Finset ι
f : ι → R
a : R
⊢ a * s.sup f = s.sup fun x ↦ a * f x

Tactic:
induction s using Finset.induction with

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

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝³ : LinearOrder R
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : CanonicallyOrderedAdd R
inst✝ : OrderBot R
s : Finset ι
f : ι → R
a : R
⊢ s.sup f * a = s.sup fun x ↦ f x * a

Tactic:
induction s using Finset.induction with

Goal state after:
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Semiring R
x : α → R
s : Finset α
hc : (↑s).Pairwise (Commute on x)
⊢ ∀ (n : ℕ), s.sum x ^ n = ∑ k, ↑(↑↑k).countPerms * (Multiset.map x ↑↑k).noncommProd ⋯

Tactic:
induction s using Finset.induction with

Goal state after:
case insert
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Semiring R
x : α → R
a : α
s : Finset α
ha : a ∉ s
ih :
  ∀ (hc : (↑s).Pairwise (Commute on x)) (n : ℕ),
    s.sum x ^ n = ∑ k, ↑(↑↑k).countPerms * (Multiset.map x ↑↑k).noncommProd ⋯
hc : (↑(insert a s)).Pairwise (Commute on x)
⊢ ∀ (n : ℕ), (insert a s).sum x ^ n = ∑ k, ↑(↑↑k).countPerms * (Multiset.map x ↑↑k).noncommProd ⋯
Module: Mathlib.Algebra.MvPolynomial.Expand

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : MvPolynomial σ R
r : R
⊢ (expand p) f = C r ↔ f = C r

Tactic:
rw [← expand_C, expand_inj hp, expand_C]

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

Goal state before:
pp: case inr.succ.refine_2
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
p✝ q✝ : MvPolynomial σ R
inst✝ : IsCancelMulZero R
n✝ : σ →₀ ℕ
hR : Nontrivial R
d : ℕ
hd :
  ∀ (n : σ →₀ ℕ),
    Finsupp.degree n = d →
      ∀ (p q : MvPolynomial σ R), p ∣ (monomial n) 1 * q ↔ ∃ m r, m ≤ n ∧ r ∣ q ∧ p = (monomial m) 1 * r
n : σ →₀ ℕ
hn : Finsupp.degree n = d + 1
p q : MvPolynomial σ R
x✝ : ∃ m r, m ≤ n ∧ r ∣ q ∧ p = (monomial m) 1 * r
m : σ →₀ ℕ
r : MvPolynomial σ R
hmn : m ≤ n
hrq : r ∣ q
hp : p = (monomial m) 1 * r
⊢ p ∣ (monomial n) 1 * q

Tactic:
rw [hp, ← add_tsub_cancel_of_le hmn, ← mul_one 1, ← monomial_mul, mul_one, mul_assoc]
      apply mul_dvd_mul dvd_rfl
      apply dvd_mul_of_dvd_right hrq

Goal state after:
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: case refine_2
n : ℕ
α : Type u_1
inst✝ : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - ↑m)
x : α
hx : x ∉ ↑s
⊢ (Multiset.filter (fun x_1 ↦ x ≠ x_1) ↑(fill x m s)).countPerms = (↑s).countPerms

Tactic:
refine congrArg _ ?_
    rw [coe_fill, coe_replicate, Multiset.filter_add]
    rw [Multiset.filter_eq_self.mpr]
    · rw [add_eq_left]
      rw [Multiset.filter_eq_nil]
      exact fun j hj ↦ by simp [Multiset.mem_replicate.mp hj]
    · exact fun j hj h ↦ hx <| by simpa [h] using hj

Goal state after:
Module: Mathlib.Order.GameAdd

Goal state before:
pp: α : Type u_1
β : Type u_2
rα✝ : α → α → Prop
rβ : β → β → Prop
a : α
b : β
rα : α → α → Prop
a₁ b₁ a₂ b₂ : α
⊢ (Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) =
      (Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂)) ∧
    (Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) =
      (Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂))

Tactic:
simp [or_comm]

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

Goal state before:
pp: case inl
R : Type u_1
σ : Type u_2
n : σ
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
ι : Type u_3
s : Finset ι
f : ι → MvPolynomial σ R
h : ∀ i ∈ s, f i ≠ 0
nontrivial : Subsingleton (MvPolynomial σ R)
⊢ degreeOf n (∏ i ∈ s, f i) = ∑ i ∈ s, degreeOf n (f i)

pp: case inr
R : Type u_1
σ : Type u_2
n : σ
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
ι : Type u_3
s : Finset ι
f : ι → MvPolynomial σ R
h : ∀ i ∈ s, f i ≠ 0
nontrivial : Nontrivial (MvPolynomial σ R)
⊢ degreeOf n (∏ i ∈ s, f i) = ∑ i ∈ s, degreeOf n (f i)

Tactic:
· simp [Subsingleton.eq_zero (α := MvPolynomial σ R)]

Goal state after:
case inr
R : Type u_1
σ : Type u_2
n : σ
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
ι : Type u_3
s : Finset ι
f : ι → MvPolynomial σ R
h : ∀ i ∈ s, f i ≠ 0
nontrivial : Nontrivial (MvPolynomial σ R)
⊢ degreeOf n (∏ i ∈ s, f i) = ∑ i ∈ s, degreeOf n (f i)
Module: Mathlib.Data.Fin.Tuple.Finset

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Type u_1
S : (i : Fin (n + 1)) → Finset (α i)
P : ((i : Fin n) → α i.castSucc) → Prop
inst✝ : DecidablePred P
⊢ map (snocEquiv α).symm.toEmbedding ({r ∈ piFinset S | P (init r)}) = S (last n) ×ˢ {r ∈ piFinset (init S) | P r}

Tactic:
unfold init; ext; simp [Fin.forall_iff_castSucc, and_assoc]

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case mpr
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
hf : f ≠ 0
⊢ m.leadingCoeff f ≠ 0

Tactic:
rw [← support_nonempty] at hf

Goal state after:
case mpr
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
hf : f.support.Nonempty
⊢ m.leadingCoeff f ≠ 0
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
r : R
⊢ (C r).totalDegree = 0

Tactic:
totalDegree_C

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
r : R
⊢ 0 = 0
Module: Mathlib.Data.Sym.Card

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
⊢ #(image (uncurry Sym2.mk) s.offDiag) = (#s * #s - #s) / 2

Tactic:
← offDiag_card,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
⊢ #(image (uncurry Sym2.mk) s.offDiag) = #s.offDiag / 2
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f g : MvPolynomial σ R
h₁ : m.degree f = 0
h₂ : m.degree g = 0
⊢ C (m.leadingCoeff g) * f - C (m.leadingCoeff f) * g = 0

Tactic:
nth_rewrite 1 [degree_eq_zero_iff.mp h₁]

Goal state after:
case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f g : MvPolynomial σ R
h₁ : m.degree f = 0
h₂ : m.degree g = 0
⊢ C (m.leadingCoeff g) * C (m.leadingCoeff f) - C (m.leadingCoeff f) * g = 0