mathlib-initiative/mathlib-tactics huggingface dataset:
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
p1 : V →ₗ[𝕜] ↥S := ↑S.orthogonalProjectionOnto
p2 : V →ₗ[𝕜] ↥Sᗮ := ↑Sᗮ.orthogonalProjectionOnto
M : V →ₗ[𝕜] V := L.toLinearMap ∘ₗ p1 + L3.toLinearMap ∘ₗ p2
M_norm_map : ∀ (x : V), ‖M x‖ = ‖x‖
⊢ V →ₗᵢ[𝕜] V

Tactic:
exact
    { toLinearMap := M
      norm_map' := M_norm_map }

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

Goal state before:
pp: ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst✝ : Fintype ι
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ⊆ ↑B
this : Fintype ↑(s ∩ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))
⊢ ∑ i ∈ (s ∩ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))).toFinset, F i / ↑n ^ card ι =
    ∑ J ∈ (prepartition n B).boxes, (volume.toBoxAdditive.toSMul J) (s.indicator F ((prepartition n B).tag J))

Tactic:
Set.indicator_apply,

Goal state after:
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst✝ : Fintype ι
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ⊆ ↑B
this : Fintype ↑(s ∩ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))
⊢ ∑ i ∈ (s ∩ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))).toFinset, F i / ↑n ^ card ι =
    ∑ x ∈ (prepartition n B).boxes,
      (volume.toBoxAdditive.toSMul x) (if (prepartition n B).tag x ∈ s then F ((prepartition n B).tag x) else 0)
Module: Mathlib.Analysis.BoxIntegral.Integrability

Goal state before:
pp: ι : Type u
E : Type v
inst✝³ : Fintype ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
l : IntegrationParams
I : Box ι
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
hl : l.bRiemann = false
ε : ℝ≥0
ε0 : 0 < ε
δ : ℕ → ℝ≥0
δ0 : ∀ (i : ℕ), 0 < δ i
c : ℝ≥0
hδc : HasSum δ c
hcε : c < ε
this : Fact (μ ↑I < ∞)
hf : (μ.restrict ↑I) {x | f x ≠ 0} = 0
N : (ι → ℝ) → ℕ := fun x ↦ ⌈‖f x‖⌉₊
N0 : ∀ {x : ι → ℝ}, N x = 0 ↔ f x = 0
n : ℕ
⊢ ∃ U, N ⁻¹' {n} ⊆ U ∧ IsOpen U ∧ (μ.restrict ↑I) U < ↑(δ n) / ↑n

Tactic:
by
    refine (N ⁻¹' {n}).exists_isOpen_lt_of_lt _ ?_
    rcases n with - | n
    · simp [ENNReal.div_zero (ENNReal.coe_pos.2 (δ0 _)).ne']
    · refine (measure_mono_null ?_ hf).le.trans_lt ?_
      · exact fun x hxN hxf => n.succ_ne_zero ((Eq.symm hxN).trans <| N0.2 hxf)
      · simp [(δ0 _).ne']

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

Goal state before:
pp: ι : Type u_1
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst✝ : Fintype ι
hF : Continuous F
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ : volume (frontier s) = 0
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ⊆ ↑B
ε : ℝ
hε : ε > 0
h₁ : ∃ C, ∀ x ∈ Box.Icc B, ‖s.indicator F x‖ ≤ C
⊢ ∀ᵐ (x : ι → ℝ), ContinuousAt (s.indicator F) x

Tactic:
filter_upwards [compl_mem_ae_iff.mpr hs₃] with _ h
      using (hF.continuousOn).continuousAt_indicator h

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

Goal state before:
pp: ι : Type u
E : Type v
inst✝⁴ : Fintype ι
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
I : Box ι
l : IntegrationParams
hl : l.bRiemann = false
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
g : (ι → ℝ) → E
hg : StronglyMeasurable g
this : SeparableSpace ↑(Set.range g ∪ {0})
hgi : IntegrableOn g (↑I) μ
f : ℕ → SimpleFunc (ι → ℝ) E := SimpleFunc.approxOn g ⋯ (Set.range g ∪ {0}) 0 ⋯
hfi : ∀ (n : ℕ), IntegrableOn (⇑(f n)) (↑I) μ
hfi' : ∀ (n : ℕ), BoxIntegral.Integrable I l (⇑(f n)) μ.toBoxAdditive.toSMul
x : ι → ℝ
m n : ℕ
hmn : m ≤ n
⊢ ‖(f n) x - g x‖ ≤ ‖(f m) x - g x‖

Tactic:
rw [← dist_eq_norm, ← dist_eq_norm, dist_nndist, dist_nndist, NNReal.coe_le_coe, ←
      ENNReal.coe_le_coe, ← edist_nndist, ← edist_nndist]

Goal state after:
ι : Type u
E : Type v
inst✝⁴ : Fintype ι
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
I : Box ι
l : IntegrationParams
hl : l.bRiemann = false
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
g : (ι → ℝ) → E
hg : StronglyMeasurable g
this : SeparableSpace ↑(Set.range g ∪ {0})
hgi : IntegrableOn g (↑I) μ
f : ℕ → SimpleFunc (ι → ℝ) E := SimpleFunc.approxOn g ⋯ (Set.range g ∪ {0}) 0 ⋯
hfi : ∀ (n : ℕ), IntegrableOn (⇑(f n)) (↑I) μ
hfi' : ∀ (n : ℕ), BoxIntegral.Integrable I l (⇑(f n)) μ.toBoxAdditive.toSMul
x : ι → ℝ
m n : ℕ
hmn : m ≤ n
⊢ edist ((f n) x) (g x) ≤ edist ((f m) x) (g x)
Module: Mathlib.Analysis.BoxIntegral.Basic

Goal state before:
pp: ι : Type u
E : Type v
F : Type w
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
I : Box ι
π : TaggedPrepartition I
inst✝¹ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
c : ℝ≥0
ε : ℝ
inst✝ : CompleteSpace F
h : Integrable I l f vol
h0 : 0 < ε
hπ : l.MemBaseSet I c (h.convergenceR ε c) π
π₀ : Prepartition I
hU : π.iUnion = π₀.iUnion
δ : ℝ
δ0 : 0 < δ
δ' : ℝ := δ / (↑(#π₀.boxes) + 1)
H0 : 0 < ↑(#π₀.boxes) + 1
δ'0 : 0 < δ'
C : ℝ≥0 := max π₀.distortion π₀.compl.distortion
J : Box ι
hJ : J ∈ π₀
Hle : J ≤ I
HJi : Integrable J l f vol
r : (ι → ℝ) → ↑(Set.Ioi 0) := fun x ↦ min (h.convergenceR δ' C x) (HJi.convergenceR δ' C x)
hJd : J.distortion ≤ C
πJ : TaggedPrepartition J
hC : l.MemBaseSet J C r πJ
hp : πJ.IsPartition
hC₁ : l.MemBaseSet J C (HJi.convergenceR δ' C) πJ
⊢ ∃ πi,
    πi.IsPartition ∧ dist (integralSum f vol πi) (integral J l f vol) ≤ δ' ∧ l.MemBaseSet J C (h.convergenceR δ' C) πi

Tactic:
have hC₂ : l.MemBaseSet J C (h.convergenceR δ' C) πJ := by
      refine hC.mono J le_rfl le_rfl fun x _ => ?_; exact min_le_left _ _

Goal state after:
ι : Type u
E : Type v
F : Type w
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
I : Box ι
π : TaggedPrepartition I
inst✝¹ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
c : ℝ≥0
ε : ℝ
inst✝ : CompleteSpace F
h : Integrable I l f vol
h0 : 0 < ε
hπ : l.MemBaseSet I c (h.convergenceR ε c) π
π₀ : Prepartition I
hU : π.iUnion = π₀.iUnion
δ : ℝ
δ0 : 0 < δ
δ' : ℝ := δ / (↑(#π₀.boxes) + 1)
H0 : 0 < ↑(#π₀.boxes) + 1
δ'0 : 0 < δ'
C : ℝ≥0 := max π₀.distortion π₀.compl.distortion
J : Box ι
hJ : J ∈ π₀
Hle : J ≤ I
HJi : Integrable J l f vol
r : (ι → ℝ) → ↑(Set.Ioi 0) := fun x ↦ min (h.convergenceR δ' C x) (HJi.convergenceR δ' C x)
hJd : J.distortion ≤ C
πJ : TaggedPrepartition J
hC : l.MemBaseSet J C r πJ
hp : πJ.IsPartition
hC₁ : l.MemBaseSet J C (HJi.convergenceR δ' C) πJ
hC₂ : l.MemBaseSet J C (h.convergenceR δ' C) πJ
⊢ ∃ πi,
    πi.IsPartition ∧ dist (integralSum f vol πi) (integral J l f vol) ≤ δ' ∧ l.MemBaseSet J C (h.convergenceR δ' C) πi
Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace

Goal state before:
pp: ι : Type u_4
F : Type u_5
inst✝⁵ : Fintype ι
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
b : OrthonormalBasis ι ℝ F
⊢ b.toBasis.addHaar = volume

Tactic:
rw [Basis.addHaar_eq_iff]

Goal state after:
ι : Type u_4
F : Type u_5
inst✝⁵ : Fintype ι
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
b : OrthonormalBasis ι ℝ F
⊢ volume ↑b.toBasis.parallelepiped = 1
Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics

Goal state before:
pp: case h
α : Type u_1
u v : α → ℝ
l : Filter α
hv : 0 ≤ v
h : u ~[l] v
r : ℝ
φ : α → ℝ
hφ : Tendsto φ l (𝓝 1)
huφv : u =ᶠ[l] φ * v
hφr : Tendsto ((fun x ↦ x ^ r) ∘ φ) l (𝓝 1)
⊢ u ^ r =ᶠ[l] (fun x ↦ x ^ r) ∘ φ * v ^ r

Tactic:
conv => enter [3]; change fun x ↦ φ x ^ r * v x ^ r

Goal state after:
case h
α : Type u_1
u v : α → ℝ
l : Filter α
hv : 0 ≤ v
h : u ~[l] v
r : ℝ
φ : α → ℝ
hφ : Tendsto φ l (𝓝 1)
huφv : u =ᶠ[l] φ * v
hφr : Tendsto ((fun x ↦ x ^ r) ∘ φ) l (𝓝 1)
⊢ u ^ r =ᶠ[l] fun x ↦ φ x ^ r * v x ^ r
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: M : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedAddMonoid M
f : ℕ → M
u : ℕ → ℕ
C : ℕ
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
h_nonneg : ∀ (n : ℕ), 0 ≤ f n
hu : Monotone u
h_succ_diff : SuccDiffBounded C u
n : ℕ
⊢ ∑ k ∈ range (n + 1), (u (k + 1) - u k) • f (u k) ≤ (u 1 - u 0) • f (u 0) + C • ∑ k ∈ Ico (u 0 + 1) (u n + 1), f k

Tactic:
rw [sum_range_succ', add_comm]
  gcongr
  suffices ∑ k ∈ range n, (u (k + 2) - u (k + 1)) • f (u (k + 1)) ≤
  C • ∑ k ∈ range n, ((u (k + 1) - u k) • f (u (k + 1))) by
    refine this.trans (nsmul_le_nsmul_right ?_ _)
    exact sum_schlomilch_le' hf h_pos hu n
  have : ∀ k ∈ range n, (u (k + 2) - u (k + 1)) • f (u (k + 1)) ≤
    C • ((u (k + 1) - u k) • f (u (k + 1))) := by
    intro k _
    rw [smul_smul]
    gcongr
    · exact h_nonneg (u (k + 1))
    exact mod_cast h_succ_diff k
  convert! sum_le_sum this
  simp [smul_sum]

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: a s : ℝ
hnorm : Tendsto (fun n ↦ ‖↑n‖) atTop atTop
⊢ (fun x ↦ ↑x + ?m.78) =ᶠ[atTop] fun n ↦ |↑n + a|

Tactic:
filter_upwards [eventually_gt_atTop (Nat.ceil |a|)] with _ hn
      rw [abs_of_pos]
      linarith [lt_of_abs_lt ((abs_neg a).symm ▸ Nat.lt_of_ceil_lt hn)]

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: a s : ℝ
⊢ (Summable fun n ↦ 1 / |↑n + a| ^ s) ↔ 1 < s

Tactic:
simp_rw [summable_int_iff_summable_nat_and_neg, ← abs_neg (↑(-_ : ℤ) + a), neg_add,
    Int.cast_neg, neg_neg, Int.cast_natCast, summable_one_div_nat_add_rpow, and_self]

Goal state after:
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✝ x y : k[G]
hy : y ∈ {p | ∀ m ∈ p.coeff.support, ∃ m' ∈ s, ∃ d, m = d * m'}
xm ym : G
hym : ym ∈ y.coeff.support
hm✝¹ : xm * ym ∈ (x.coeff.sum fun i n ↦ y.coeff.sum fun i_1 n_1 ↦ (single (i * i_1) (n * n_1)).coeff).support
hm✝ : xm * ym ∈ (y.coeff.sum fun i n ↦ (single (xm * i) (x.coeff xm * n)).coeff).support
hm : xm * ym ∈ (single (xm * ym) (x.coeff xm * y.coeff ym)).coeff.support
sm : G
p : sm ∈ s ∧ ∃ d, ym = d * sm
⊢ (∃ d, ym = d * sm) → ∃ d, xm * ym = d * sm

Tactic:
rintro ⟨d, rfl⟩

Goal state after:
k : Type u_1
G : Type u_3
inst✝¹ : Monoid G
inst✝ : Semiring k
s : Set G
x✝ x y : k[G]
hy : y ∈ {p | ∀ m ∈ p.coeff.support, ∃ m' ∈ s, ∃ d, m = d * m'}
xm sm d : G
hym : d * sm ∈ y.coeff.support
hm✝¹ : xm * (d * sm) ∈ (x.coeff.sum fun i n ↦ y.coeff.sum fun i_1 n_1 ↦ (single (i * i_1) (n * n_1)).coeff).support
hm✝ : xm * (d * sm) ∈ (y.coeff.sum fun i n ↦ (single (xm * i) (x.coeff xm * n)).coeff).support
hm : xm * (d * sm) ∈ (single (xm * (d * sm)) (x.coeff xm * y.coeff (d * sm))).coeff.support
p : sm ∈ s ∧ ∃ d_1, d * sm = d_1 * sm
⊢ ∃ d_1, xm * (d * sm) = d_1 * sm
Module: Mathlib.Algebra.MonoidAlgebra.Ideal

Goal state before:
pp: k : Type u_1
A : Type u_2
inst✝¹ : AddMonoid A
inst✝ : Semiring k
s : Set A
x✝ x y : k[A]
hy : y ∈ {p | ∀ m ∈ p.coeff.support, ∃ m' ∈ s, ∃ d, m = d + m'}
xm ym : A
hym : ym ∈ y.coeff.support
hm✝¹ : xm + ym ∈ (x.coeff.sum fun i n ↦ y.coeff.sum fun i_1 n_1 ↦ (single (i + i_1) (n * n_1)).coeff).support
hm✝ : xm + ym ∈ (y.coeff.sum fun i n ↦ (single (xm + i) (x.coeff xm * n)).coeff).support
hm : xm + ym ∈ (single (xm + ym) (x.coeff xm * y.coeff ym)).coeff.support
sm : A
⊢ (∃ d, ym = d + sm) → ∃ d, xm + ym = d + sm

Tactic:
rintro ⟨d, rfl⟩

Goal state after:
k : Type u_1
A : Type u_2
inst✝¹ : AddMonoid A
inst✝ : Semiring k
s : Set A
x✝ x y : k[A]
hy : y ∈ {p | ∀ m ∈ p.coeff.support, ∃ m' ∈ s, ∃ d, m = d + m'}
xm sm d : A
hym : d + sm ∈ y.coeff.support
hm✝¹ : xm + (d + sm) ∈ (x.coeff.sum fun i n ↦ y.coeff.sum fun i_1 n_1 ↦ (single (i + i_1) (n * n_1)).coeff).support
hm✝ : xm + (d + sm) ∈ (y.coeff.sum fun i n ↦ (single (xm + i) (x.coeff xm * n)).coeff).support
hm : xm + (d + sm) ∈ (single (xm + (d + sm)) (x.coeff xm * y.coeff (d + sm))).coeff.support
⊢ ∃ d_1, xm + (d + sm) = d_1 + sm
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
i : σ
hsi : ¬s i = 0
hai : a i = 0
⊢ 0 = ↑s.multinomial * 0

Tactic:
mul_zero

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
i : σ
hsi : ¬s i = 0
hai : a i = 0
⊢ 0 = 0
Module: Mathlib.Algebra.MvPolynomial.Division

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
s' s : σ →₀ ℕ
x : MvPolynomial σ R
h : ¬s ≤ s'
⊢ ¬∃ d, s' = s + d

Tactic:
rintro ⟨d, rfl⟩

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
s : σ →₀ ℕ
x : MvPolynomial σ R
d : σ →₀ ℕ
h : ¬s ≤ s + d
⊢ False
Module: Mathlib.Algebra.MvPolynomial.Division

Goal state before:
pp: case inr.succ.refine_1
σ : 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
i : σ
hi : i ∈ n.support
n' : σ →₀ ℕ := n - Finsupp.single i 1
hp : p ∣ (monomial (n' + Finsupp.single i 1)) 1 * q
hn' : n' + Finsupp.single i 1 = n
hnn' : n' ≤ n
hd' : Finsupp.degree n' = d
⊢ ∃ m r, m ≤ n ∧ r ∣ q ∧ p = (monomial m) 1 * r

Tactic:
monomial_add_single,

Goal state after:
case inr.succ.refine_1
σ : 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
i : σ
hi : i ∈ n.support
n' : σ →₀ ℕ := n - Finsupp.single i 1
hp : p ∣ (monomial n') 1 * X i ^ 1 * q
hn' : n' + Finsupp.single i 1 = n
hnn' : n' ≤ n
hd' : Finsupp.degree n' = d
⊢ ∃ m r, m ≤ n ∧ r ∣ q ∧ p = (monomial m) 1 * r
Module: Mathlib.Data.Nat.Choose.Multinomial

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

Tactic:
mul_zero

Goal state after:
case empty.succ
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Semiring R
x : α → R
hc : (↑∅).Pairwise (Commute on x)
n : ℕ
⊢ 0 = ∑ k, ↑(↑↑k).countPerms * (Multiset.map x ↑↑k).noncommProd ⋯
Module: Mathlib.Algebra.MvPolynomial.Funext

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
σ : Type u_2
p q : MvPolynomial σ R
s : σ → Set R
hs : ∀ (i : σ), (s i).Infinite
h : ∀ x ∈ Set.univ.pi s, (eval x) p = (eval x) q
this : ∀ (p : MvPolynomial σ R), (∀ x ∈ Set.univ.pi s, (eval x) p = 0) → p = 0
x : σ → R
hx : x ∈ Set.univ.pi s
⊢ (eval x) (p - q) = 0

Tactic:
map_sub,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
σ : Type u_2
p q : MvPolynomial σ R
s : σ → Set R
hs : ∀ (i : σ), (s i).Infinite
h : ∀ x ∈ Set.univ.pi s, (eval x) p = (eval x) q
this : ∀ (p : MvPolynomial σ R), (∀ x ∈ Set.univ.pi s, (eval x) p = 0) → p = 0
x : σ → R
hx : x ∈ Set.univ.pi s
⊢ (eval x) p - (eval x) q = 0
Module: Mathlib.Data.Finsupp.MonomialOrder

Goal state before:
pp: α : Type u_1
N : Type u_2
inst✝³ : LinearOrder α
inst✝² : AddCommMonoid N
inst✝¹ : PartialOrder N
inst✝ : IsOrderedCancelAddMonoid N
a b c : Lex (α →₀ N)
h : a + b ≤ a + c
⊢ b ≤ c

Tactic:
by simpa only [add_le_add_iff_left] using h

Goal state after:
Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c : DegLex (α →₀ ℕ)
h :
  degree (ofDegLex (a + b)) < degree (ofDegLex (a + c)) ∨
    degree (ofDegLex (a + b)) = degree (ofDegLex (a + c)) ∧ toLex (ofDegLex (a + b)) ≤ toLex (ofDegLex (a + c))
⊢ degree (ofDegLex b) < degree (ofDegLex c) ∨
    degree (ofDegLex b) = degree (ofDegLex c) ∧ toLex (ofDegLex b) ≤ toLex (ofDegLex c)

Tactic:
simpa only [ofDegLex_add, map_add, add_lt_add_iff_left, add_right_inj, toLex_add,
      add_le_add_iff_left] using h

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

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : m.degree f ≠ m.degree g
⊢ m.toSyn (m.degree (f + g)) = max (m.toSyn (m.degree f)) (m.toSyn (m.degree g))

Tactic:
by_cases h' : m.degree g ≺[m] m.degree f
  · simp [degree_add_of_lt h', le_of_lt h']
  · rw [not_lt, le_iff_eq_or_lt, Classical.or_iff_not_imp_left, EmbeddingLike.apply_eq_iff_eq] at h'
    rw [add_comm, degree_add_of_lt (h' h), right_eq_sup]
    simp only [le_of_lt (h' h)]

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

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
⊢ ∀ c ∈ (f * g).support, m.toSyn c ≤ m.toSyn (m.degree f + m.degree g)

Tactic:
intro c

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
c : σ →₀ ℕ
⊢ c ∈ (f * g).support → m.toSyn c ≤ m.toSyn (m.degree f + m.degree g)
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
c : σ →₀ ℕ
hc : m.toSyn (m.degree f + m.degree g) < m.toSyn c
d e : σ →₀ ℕ
hde : d + e = c
hd : ¬m.toSyn (m.degree f) < m.toSyn d
this : m.toSyn (m.degree g) < m.toSyn e
⊢ coeff d f * 0 = 0

Tactic:
mul_zero

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
c : σ →₀ ℕ
hc : m.toSyn (m.degree f + m.degree g) < m.toSyn c
d e : σ →₀ ℕ
hde : d + e = c
hd : ¬m.toSyn (m.degree f) < m.toSyn d
this : m.toSyn (m.degree g) < m.toSyn e
⊢ 0 = 0
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
a b : σ →₀ ℕ
ha : m.toSyn (m.degree f) ≤ m.toSyn a
hb : m.toSyn (m.degree g) ≤ m.toSyn b
c d : σ →₀ ℕ
h : (c, d) ≠ (a, b)
hcd : c + d = a + b
hf : ¬m.toSyn (m.degree f) < m.toSyn c
this : m.toSyn (m.degree g) < m.toSyn d
⊢ coeff (c, d).1 f * 0 = 0

Tactic:
mul_zero

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
a b : σ →₀ ℕ
ha : m.toSyn (m.degree f) ≤ m.toSyn a
hb : m.toSyn (m.degree g) ≤ m.toSyn b
c d : σ →₀ ℕ
h : (c, d) ≠ (a, b)
hcd : c + d = a + b
hf : ¬m.toSyn (m.degree f) < m.toSyn c
this : m.toSyn (m.degree g) < m.toSyn d
⊢ 0 = 0
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
r : R
f : MvPolynomial σ R
⊢ m.toSyn (m.degree (r • f)) ≤ m.toSyn (m.degree f)

Tactic:
by
  rw [smul_eq_C_mul]
  apply le_of_le_of_eq degree_mul_le
  simp

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

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ m.Monic (m.leadingTerm p) ↔ m.Monic p

Tactic:
by simp [leadingTerm, Monic]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
n : ℕ
p : MvPolynomial (Fin (n + 1)) R
hp : p ≠ 0
S : Fin (n + 1) → Finset R
p' : Polynomial (MvPolynomial (Fin n) R) := (finSuccEquiv R n) p
hp' : p' = (finSuccEquiv R n) p
k : ℕ := p'.natDegree
hk : k = p'.natDegree
pₖ : MvPolynomial (Fin n) R := p'.leadingCoeff
hpₖ : pₖ = p'.leadingCoeff
hp'₀ : p' ≠ 0
hpₖ₀ : pₖ ≠ 0
xₜ : Fin n → R
hxₜ : xₜ ∈ {xₜ ∈ piFinset fun i ↦ tail S i | (eval xₜ) pₖ ≠ 0}
pₓ : Polynomial R := Polynomial.map (eval xₜ) p'
hpₓ : pₓ = Polynomial.map (eval xₜ) p'
hpₓdeg : pₓ.natDegree = k
h : pₓ = 0
⊢ (eval xₜ) p'.leadingCoeff = 0

Tactic:
Polynomial.leadingCoeff,

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
n : ℕ
p : MvPolynomial (Fin (n + 1)) R
hp : p ≠ 0
S : Fin (n + 1) → Finset R
p' : Polynomial (MvPolynomial (Fin n) R) := (finSuccEquiv R n) p
hp' : p' = (finSuccEquiv R n) p
k : ℕ := p'.natDegree
hk : k = p'.natDegree
pₖ : MvPolynomial (Fin n) R := p'.leadingCoeff
hpₖ : pₖ = p'.leadingCoeff
hp'₀ : p' ≠ 0
hpₖ₀ : pₖ ≠ 0
xₜ : Fin n → R
hxₜ : xₜ ∈ {xₜ ∈ piFinset fun i ↦ tail S i | (eval xₜ) pₖ ≠ 0}
pₓ : Polynomial R := Polynomial.map (eval xₜ) p'
hpₓ : pₓ = Polynomial.map (eval xₜ) p'
hpₓdeg : pₓ.natDegree = k
h : pₓ = 0
⊢ (eval xₜ) (p'.coeff p'.natDegree) = 0
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : f ≠ 0 ∧ g ≠ 0
⊢ m.toWithBotSyn (m.withBotDegree (f + g)) ≤
    max (m.toWithBotSyn (m.withBotDegree f)) (m.toWithBotSyn (m.withBotDegree g))

Tactic:
simpa [withBotDegree_le_withBotDegree_iff, h] using degree_add_le (R := R)

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : MulAction R M
f : ArithmeticFunction M
x : ℕ
⊢ ∑ x_1 ∈ x.divisors, f ({ toFun := fun d ↦ (x / d, d), inj' := ⋯ } x_1).2 = ∑ i ∈ x.divisors, f i

Tactic:
Function.Embedding.coeFn_mk

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : MulAction R M
f : ArithmeticFunction M
x : ℕ
⊢ ∑ x_1 ∈ x.divisors, f (x / x_1, x_1).2 = ∑ i ∈ x.divisors, f i
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r s : ArithmeticFunction R
x : ArithmeticFunction M
x✝ : ℕ
⊢ ((r + s) • x) x✝ = (r • x + s • x) x✝

Tactic:
simp only [add_smul, sum_add_distrib, smul_apply, add_apply]

Goal state after:
Module: Mathlib.Data.Nat.Factorization.PrimePow

Goal state before:
pp: n : ℕ
hn : n ≠ 1
h : ∃ p, Nat.Prime p ∧ n / p ^ n.factorization p = 1
⊢ IsPrimePow n

Tactic:
rcases h with ⟨p, pp, h⟩

Goal state after:
n : ℕ
hn : n ≠ 1
p : ℕ
pp : Nat.Prime p
h : n / p ^ n.factorization p = 1
⊢ IsPrimePow n
Module: Mathlib.Data.Nat.Factorization.PrimePow

Goal state before:
pp: case mpr.inr
n p : ℕ
hp : Nat.Prime p
hn : p ∣ n
hn₀ : n ≠ 0
hq : ∀ (y : ℕ), Nat.Prime y → y ∣ n → y = p
q : ℕ
hq' : q ∈ n.primeFactorsList
⊢ List.count q n.primeFactorsList ≤ List.count q (List.replicate (n.factorization p) p)

Tactic:
Nat.mem_primeFactorsList hn₀

Goal state after:
case mpr.inr
n p : ℕ
hp : Nat.Prime p
hn : p ∣ n
hn₀ : n ≠ 0
hq : ∀ (y : ℕ), Nat.Prime y → y ∣ n → y = p
q : ℕ
hq' : Nat.Prime q ∧ q ∣ n
⊢ List.count q n.primeFactorsList ≤ List.count q (List.replicate (n.factorization p) p)
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: n : ℕ
hn : Squarefree n
t : Finset ℕ
ht : t ⊆ n.primeFactors
⊢ n = ∏ x ∈ n.primeFactors, x

Tactic:
prod_primeFactors_of_squarefree hn

Goal state after:
n : ℕ
hn : Squarefree n
t : Finset ℕ
ht : t ⊆ n.primeFactors
⊢ n = n
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: case succ
n : ℕ
h : Ω (n + 1) = 1
x : ℕ
hx : (n + 1).primeFactorsList = [x]
⊢ Nat.Prime x

Tactic:
apply prime_of_mem_primeFactorsList

Goal state after:
case succ.a
n : ℕ
h : Ω (n + 1) = 1
x : ℕ
hx : (n + 1).primeFactorsList = [x]
⊢ x ∈ primeFactorsList ?succ.n

case succ.n
n : ℕ
h : Ω (n + 1) = 1
x : ℕ
hx : (n + 1).primeFactorsList = [x]
⊢ ℕ