mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : Set E
hs : MeasurableSet s
x : E
h : Tendsto (fun r ↦ μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : μ t ≠ 0
h''t : μ t ≠ ∞
⊢ Tendsto (fun r ↦ μ (s ∩ ({x} + r • t)) / μ ({x} + r • t)) (𝓝[>] 0) (𝓝 1)

Tactic:
have I : ∀ u v, μ u ≠ 0 → μ u ≠ ∞ → MeasurableSet v →
    μ u / μ u - μ (vᶜ ∩ u) / μ u = μ (v ∩ u) / μ u := by
    intro u v uzero utop vmeas
    simp_rw [div_eq_mul_inv]
    rw [← ENNReal.sub_mul]; swap
    · simp only [uzero, ENNReal.inv_eq_top, imp_true_iff, Ne, not_false_iff]
    congr 1
    rw [inter_comm _ u, inter_comm _ u, eq_comm]
    exact ENNReal.eq_sub_of_add_eq' utop (measure_inter_add_sdiff u vmeas)

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : Set E
hs : MeasurableSet s
x : E
h : Tendsto (fun r ↦ μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : μ t ≠ 0
h''t : μ t ≠ ∞
I : ∀ (u v : Set E), μ u ≠ 0 → μ u ≠ ∞ → MeasurableSet v → μ u / μ u - μ (vᶜ ∩ u) / μ u = μ (v ∩ u) / μ u
⊢ Tendsto (fun r ↦ μ (s ∩ ({x} + r • t)) / μ ({x} + r • t)) (𝓝[>] 0) (𝓝 1)
Module: Mathlib.Analysis.InnerProductSpace.PiL2

Goal state before:
pp: η : Type u_7
inst✝⁵ : Fintype η
inst✝⁴ : DecidableEq η
ι : η → Type u_8
inst✝³ : (i : η) → Fintype (ι i)
𝕜 : Type u_9
inst✝² : RCLike 𝕜
E : η → Type u_10
inst✝¹ : (i : η) → NormedAddCommGroup (E i)
inst✝ : (i : η) → InnerProductSpace 𝕜 (E i)
B : (i : η) → OrthonormalBasis (ι i) 𝕜 (E i)
j : (i : η) × ι i
⊢ (Pi.orthonormalBasis B) j = PiLp.single 2 j.fst ((B j.fst) j.snd)

Tactic:
by
  classical
  ext k
  obtain ⟨i, j⟩ := j
  simp only [Pi.orthonormalBasis, coe_ofRepr, LinearIsometryEquiv.symm_trans,
    LinearIsometryEquiv.symm_symm, LinearIsometryEquiv.piLpCongrRight_symm,
    LinearIsometryEquiv.trans_apply, LinearIsometryEquiv.piLpCongrRight_apply,
    LinearIsometryEquiv.piLpCurry_apply, PiLp.ofLp_single, PiLp.toLp_apply,
    Sigma.curry_single (γ := fun _ _ => 𝕜)]
  obtain rfl | hi := Decidable.eq_or_ne i k
  · simp
  · simp [hi]

Goal state after:
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 ι
i : Fin 2
⊢ ∀ (j : Fin 2), inner ℝ (basisOneI i) (basisOneI j) = if i = j then 1 else 0

Tactic:
fin_cases i

Goal state after:
case «0»
ι : 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 ι
⊢ ∀ (j : Fin 2), inner ℝ (basisOneI ((fun i ↦ i) ⟨0, ⋯⟩)) (basisOneI j) = if (fun i ↦ i) ⟨0, ⋯⟩ = j then 1 else 0

case «1»
ι : 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 ι
⊢ ∀ (j : Fin 2), inner ℝ (basisOneI ((fun i ↦ i) ⟨1, ⋯⟩)) (basisOneI j) = if (fun i ↦ i) ⟨1, ⋯⟩ = j then 1 else 0
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 : Set E
A : ι → Submodule 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
n : ℕ
hn : finrank 𝕜 E = n
inst✝ : DecidableEq ι
V : ι → Submodule 𝕜 E
hV : IsInternal V
hV' : OrthogonalFamily 𝕜 (fun i ↦ ↥(V i)) fun i ↦ (V i).subtypeₗᵢ
i : ι
b : Fin (finrank 𝕜 ↥(V i))
⊢ subordinateOrthonormalBasisIndex hn hV ((sigmaOrthonormalBasisIndexEquiv hn hV hV') ⟨i, b⟩) hV' = i

Tactic:
by simp [subordinateOrthonormalBasisIndex_def]

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

Goal state before:
pp: ι : Type u_1
n : ℕ
inst✝ : NeZero n
x✝¹ x✝ : ι → ℤ
h : (fun ν ↦ tag n ν) x✝¹ = (fun ν ↦ tag n ν) x✝
i : ι
this : ↑(x✝¹ i) = ↑(x✝ i)
⊢ x✝¹ i = x✝ i

Tactic:
Int.cast_inj

Goal state after:
ι : Type u_1
n : ℕ
inst✝ : NeZero n
x✝¹ x✝ : ι → ℤ
h : (fun ν ↦ tag n ν) x✝¹ = (fun ν ↦ tag n ν) x✝
i : ι
this : x✝¹ i = x✝ i
⊢ x✝¹ i = x✝ i
Module: Mathlib.Analysis.BoxIntegral.UnitPartition

Goal state before:
pp: ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
ν : ι → ℤ
i : ι
⊢ ENNReal.ofReal ((box n ν).upper i - (box n ν).lower i) ≤ ENNReal.ofReal (1 / ↑n)

Tactic:
box.upper_sub_lower,

Goal state after:
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
ν : ι → ℤ
i : ι
⊢ ENNReal.ofReal (1 / ↑n) ≤ ENNReal.ofReal (1 / ↑n)
Module: Mathlib.Analysis.BoxIntegral.UnitPartition

Goal state before:
pp: ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
ν : ι → ℤ
⊢ ∏ x, ENNReal.ofReal ((box n ν).upper x - (box n ν).lower x) = 1 / ↑n ^ card ι

Tactic:
box.upper_sub_lower,

Goal state after:
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
ν : ι → ℤ
⊢ ∏ x, ENNReal.ofReal (1 / ↑n) = 1 / ↑n ^ card ι
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 ι
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
π : TaggedPrepartition I
πi : (J : Box ι) → Prepartition J
hπi : ∀ J ∈ π, (πi J).IsPartition
J : Box ι
hJ : J ∈ π.boxes
J' : Box ι
hJ' : J' ∈ (πi J).boxes
⊢ (vol J') (f (π.tag (π.biUnionIndex πi J'))) = (vol J') (f (π.tag J))

Tactic:
by rw [Prepartition.biUnionIndex_of_mem _ hJ hJ']

Goal state after:
Module: Mathlib.LinearAlgebra.Orientation

Goal state before:
pp: case e'_4
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : IsEmpty ι
x : M [⋀^ι]→ₗ[R] R
hx : x ≠ 0
h : LinearIndependent R ![x, AlternatingMap.constLinearEquivOfIsEmpty 1]
f : M [⋀^ι]→ₗ[R] R ≃ₗ[R] R := AlternatingMap.constLinearEquivOfIsEmpty.symm
i : Fin (Nat.succ 0).succ
⊢ ![f x, 1] i = (⇑↑f ∘ ![x, AlternatingMap.constLinearEquivOfIsEmpty 1]) i

Tactic:
fin_cases i

Goal state after:
case e'_4.«0»
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : IsEmpty ι
x : M [⋀^ι]→ₗ[R] R
hx : x ≠ 0
h : LinearIndependent R ![x, AlternatingMap.constLinearEquivOfIsEmpty 1]
f : M [⋀^ι]→ₗ[R] R ≃ₗ[R] R := AlternatingMap.constLinearEquivOfIsEmpty.symm
⊢ ![f x, 1] ((fun i ↦ i) ⟨0, ⋯⟩) = (⇑↑f ∘ ![x, AlternatingMap.constLinearEquivOfIsEmpty 1]) ((fun i ↦ i) ⟨0, ⋯⟩)

case e'_4.«1»
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : IsEmpty ι
x : M [⋀^ι]→ₗ[R] R
hx : x ≠ 0
h : LinearIndependent R ![x, AlternatingMap.constLinearEquivOfIsEmpty 1]
f : M [⋀^ι]→ₗ[R] R ≃ₗ[R] R := AlternatingMap.constLinearEquivOfIsEmpty.symm
⊢ ![f x, 1] ((fun i ↦ i) ⟨1, ⋯⟩) = (⇑↑f ∘ ![x, AlternatingMap.constLinearEquivOfIsEmpty 1]) ((fun i ↦ i) ⟨1, ⋯⟩)
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 ι
inst✝ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
⊢ integral I l (-f) vol = -integral I l f vol

Tactic:
by
  classical
  exact if h : Integrable I l f vol then h.hasIntegral.neg.integral_eq
  else by rw [integral, integral, dif_neg h, dif_neg (mt Integrable.of_neg h), neg_zero]

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
⊢ dist ((f n) x) (g x) ≤ dist ((f m) x) (g x)

Tactic:
dist_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
⊢ ↑(nndist ((f n) x) (g x)) ≤ dist ((f m) x) (g x)
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
⊢ ↑(nndist ((f n) x) (g x)) ≤ dist ((f m) x) (g x)

Tactic:
dist_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
⊢ ↑(nndist ((f n) x) (g x)) ≤ ↑(nndist ((f m) x) (g x))
Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace

Goal state before:
pp: case refine_1
U : Type u_4
V : Type u_5
inst✝⁹ : NormedAddCommGroup U
inst✝⁸ : InnerProductSpace ℝ U
inst✝⁷ : MeasurableSpace U
inst✝⁶ : BorelSpace U
inst✝⁵ : FiniteDimensional ℝ U
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MeasurableSpace V
inst✝¹ : BorelSpace V
inst✝ : FiniteDimensional ℝ V
⊢ MeasurePreserving (⇑(stdOrthonormalBasis ℝ U).repr.symm.toMeasurableEquiv) volume volume

Tactic:
exact (LinearIsometryEquiv.measurePreserving _)

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace

Goal state before:
pp: case refine_2
U : Type u_4
V : Type u_5
inst✝⁹ : NormedAddCommGroup U
inst✝⁸ : InnerProductSpace ℝ U
inst✝⁷ : MeasurableSpace U
inst✝⁶ : BorelSpace U
inst✝⁵ : FiniteDimensional ℝ U
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MeasurableSpace V
inst✝¹ : BorelSpace V
inst✝ : FiniteDimensional ℝ V
⊢ MeasurePreserving (⇑(stdOrthonormalBasis ℝ V).repr.symm.toMeasurableEquiv) volume volume

Tactic:
exact (LinearIsometryEquiv.measurePreserving _)

Goal state after:
Module: Mathlib.Analysis.SumOverResidueClass

Goal state before:
pp: R : Type u_1
inst✝² : AddCommGroup R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalAddGroup R
m : ℕ
hm : NeZero m
k : ℕ
f : ℕ → R
⊢ Summable ({n | ↑n = ↑k}.indicator f) ↔ Summable ({n | ↑n = ↑k ∧ k ≤ n}.indicator f)

Tactic:
rw [← (finite_lt_nat k).summable_compl_iff (f := {n : ℕ | (n : ZMod m) = k}.indicator f)]
    simp only [summable_subtype_iff_indicator, indicator_indicator, inter_comm, ofPred_and,
      compl_ofPred, not_lt]

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

Goal state before:
pp: ι : Type u_2
inst✝² : Fintype ι
L : Submodule ℤ (ι → ℝ)
inst✝¹ : DiscreteTopology ↥L
inst✝ : IsZLattice ℝ L
b : Basis ι ℤ ↥L
⊢ covolume L volume = |↑(LinearEquiv.det (Basis.ofZLatticeBasis ℝ L b).equivFun)|⁻¹

Tactic:
covolume_eq_det L b,

Goal state after:
ι : Type u_2
inst✝² : Fintype ι
L : Submodule ℤ (ι → ℝ)
inst✝¹ : DiscreteTopology ↥L
inst✝ : IsZLattice ℝ L
b : Basis ι ℤ ↥L
⊢ |(Matrix.of (Subtype.val ∘ ⇑b)).det| = |↑(LinearEquiv.det (Basis.ofZLatticeBasis ℝ L b).equivFun)|⁻¹
Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics

Goal state before:
pp: α : Type u_1
inst✝ : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), ‖∑ i ∈ Finset.range n, g i‖ = ∑ i ∈ Finset.range n, g i
ε : ℝ
εpos : 0 < ε
⊢ ∀ᶠ (x : ℕ) in atTop, ‖∑ i ∈ Finset.range x, f i‖ ≤ ε * ‖∑ i ∈ Finset.range x, g i‖

Tactic:
obtain ⟨N, hN⟩ : ∃ N : ℕ, ∀ b : ℕ, N ≤ b → ‖f b‖ ≤ ε / 2 * g b := by
    simpa only [A, eventually_atTop] using isLittleO_iff.mp h (half_pos εpos)

Goal state after:
α : Type u_1
inst✝ : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), ‖∑ i ∈ Finset.range n, g i‖ = ∑ i ∈ Finset.range n, g i
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖f b‖ ≤ ε / 2 * g b
⊢ ∀ᶠ (x : ℕ) in atTop, ‖∑ i ∈ Finset.range x, f i‖ ≤ ε * ‖∑ i ∈ Finset.range x, g i‖
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: case refine_1
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
k n : ℕ
⊢ k.succ ≠ 0

Tactic:
simp only [Ne, Nat.succ_ne_zero, not_false_iff]

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

Goal state before:
pp: case inr
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
h : ∀ (q : P), ¬x q = 0 → ¬g • q = p
⊢ f.coeff g • x (g⁻¹ • p) = 0

Tactic:
have := h (g⁻¹ • p)
      aesop

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

Goal state before:
pp: R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : IsLeftCancelAdd R
σ : Type u_3
i : σ
p q r : MvPolynomial σ R
h : p = X i * q + r
hr : ∀ n ∈ r.support, n i = 0
h' : p = X i * q + r
⊢ r = p.modMonomial (Finsupp.single i 1)

Tactic:
rwa [← p.divMonomial_add_modMonomial_single i,
    eq_divMonomial_single h hr, add_right_inj, eq_comm] at h'

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

Goal state before:
pp: case add
R : Type u_1
S : Type u_2
σ : Type u_3
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
x : S
f : R →+* Polynomial S
g : σ → Polynomial S
p✝ p q : MvPolynomial σ R
hp : Polynomial.eval x (eval₂ f g p) = eval₂ ((Polynomial.evalRingHom x).comp f) (fun s ↦ Polynomial.eval x (g s)) p
hq : Polynomial.eval x (eval₂ f g q) = eval₂ ((Polynomial.evalRingHom x).comp f) (fun s ↦ Polynomial.eval x (g s)) q
⊢ Polynomial.eval x (eval₂ f g (p + q)) =
    eval₂ ((Polynomial.evalRingHom x).comp f) (fun s ↦ Polynomial.eval x (g s)) (p + q)

Tactic:
simp [hp, hq]

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

Goal state before:
pp: case mpr.inl
R : Type u_1
σ : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
p : MvPolynomial σ R
i : σ
r : R
hr : r ≠ 0
b : R
hb : b ∣ r
hp : p = C b
⊢ ∃ a ≤ Finsupp.single i 1, b ∣ r ∧ p = (monomial a) b

pp: case mpr.inr
R : Type u_1
σ : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
p : MvPolynomial σ R
i : σ
r : R
hr : r ≠ 0
b : R
hb : b ∣ r
hp : p = b • (monomial (Finsupp.single i 1)) 1
⊢ ∃ a ≤ Finsupp.single i 1, b ∣ r ∧ p = (monomial a) b

Tactic:
· use 0; simp [hb, hp]

Goal state after:
case mpr.inr
R : Type u_1
σ : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
p : MvPolynomial σ R
i : σ
r : R
hr : r ≠ 0
b : R
hb : b ∣ r
hp : p = b • (monomial (Finsupp.single i 1)) 1
⊢ ∃ a ≤ Finsupp.single i 1, b ∣ r ∧ p = (monomial a) b
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 ∈ piFinset fun i ↦ S i | (eval (tail x)) pₖ = 0})) / ∏ i, ↑(#(S i)) =
    ↑(#(S 0)) * ↑(#({xₜ ∈ piFinset fun i ↦ tail S i | (eval xₜ) pₖ = 0})) / (↑(#(S 0)) * ∏ i, ↑(#(S i.succ)))

Tactic:
card_consEquiv_filter_piFinset S fun x ↦ eval x pₖ = 0,

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
⊢ ↑(#(S 0) * #({r ∈ piFinset (tail S) | (eval r) pₖ = 0})) / ∏ i, ↑(#(S i)) =
    ↑(#(S 0)) * ↑(#({xₜ ∈ piFinset fun i ↦ tail S i | (eval xₜ) pₖ = 0})) / (↑(#(S 0)) * ∏ i, ↑(#(S i.succ)))
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
r : R
hr : r ∈ R⁰
f : MvPolynomial σ R
hf : ¬f = 0
⊢ coeff (m.degree f) (C r * f) ≠ 0

Tactic:
rw [← zero_add (degree m f), ← degree_C r, coeff_mul_of_degree_add]

Goal state after:
case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
r : R
hr : r ∈ R⁰
f : MvPolynomial σ R
hf : ¬f = 0
⊢ m.leadingCoeff (C r) * m.leadingCoeff f ≠ 0
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: case mpr
n : ℕ
h0 : n ≠ 0
s : Finset ℕ
hs : s ∈ (normalizedFactors n).toFinset.powerset
⊢ (s.val.prod ∣ n ∧ n ≠ 0) ∧ Squarefree s.val.prod

Tactic:
rw [Finset.mem_powerset, ← Finset.val_le_iff, Multiset.toFinset_val] at hs

Goal state after:
case mpr
n : ℕ
h0 : n ≠ 0
s : Finset ℕ
hs : s.val ≤ (normalizedFactors n).dedup
⊢ (s.val.prod ∣ n ∧ n ≠ 0) ∧ Squarefree s.val.prod
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
i : ℕ × ℕ
hi : i ∈ (i.1 * i.2).divisorsAntidiagonal
h : i.1 * i.2 ≠ 0
⊢ ↑ζ i.1 • f i.2 = f i.2

Tactic:
natCoe_apply,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : MulAction R M
f : ArithmeticFunction M
i : ℕ × ℕ
hi : i ∈ (i.1 * i.2).divisorsAntidiagonal
h : i.1 * i.2 ≠ 0
⊢ ↑(ζ i.1) • f i.2 = f i.2
Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
n : ℕ
⊢ ∑ x ∈ n.divisorsAntidiagonal, ↑ζ x.1 * f x.2 = ∑ x ∈ n.divisorsAntidiagonal, f x.1 * ↑ζ x.2

Tactic:
natCoe_apply,

Goal state after:
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
n : ℕ
⊢ ∑ x ∈ n.divisorsAntidiagonal, ↑(ζ x.1) * f x.2 = ∑ x ∈ n.divisorsAntidiagonal, f x.1 * ↑(ζ x.2)
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
b : ArithmeticFunction M
⊢ 1 • b = b

Tactic:
by
  ext x
  simp_all [← map_div_right_divisors, sum_eq_single 1]

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

Goal state before:
pp: p k : ℕ
hp : Prime p
hk : 0 < k
⊢ (p ^ k).minFac ^ (p ^ k).factorization (p ^ k).minFac = p ^ k

Tactic:
rw [← Nat.prime_iff] at hp

Goal state after:
p k : ℕ
hp : Nat.Prime p
hk : 0 < k
⊢ (p ^ k).minFac ^ (p ^ k).factorization (p ^ k).minFac = p ^ k
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f g : MvPolynomial σ R
⊢ coeff (m.degree f ⊔ m.degree g) (m.sPolynomial f g) = 0

Tactic:
rw [sPolynomial_def, coeff_sub]
  nth_rewrite 1 [← tsub_add_cancel_of_le le_sup_left, coeff_monomial_mul]
  nth_rewrite 1 [← tsub_add_cancel_of_le le_sup_right, coeff_monomial_mul]
  unfold leadingCoeff
  ring

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

Goal state before:
pp: R : Type u_1
inst✝ : CommMonoidWithZero R
f : ℕ → R
⊢ (ArithmeticFunction.prodPrimeFactors f) 1 = 1 ∧
    ∀ {m n : ℕ},
      m ≠ 0 →
        n ≠ 0 →
          m.Coprime n →
            (ArithmeticFunction.prodPrimeFactors f) (m * n) =
              (ArithmeticFunction.prodPrimeFactors f) m * (ArithmeticFunction.prodPrimeFactors f) n

Tactic:
simp only [ne_eq, one_ne_zero, not_false_eq_true, prodPrimeFactors_apply, primeFactors_one,
    prod_empty, true_and]

Goal state after:
R : Type u_1
inst✝ : CommMonoidWithZero R
f : ℕ → R
⊢ ∀ {m n : ℕ},
    ¬m = 0 →
      ¬n = 0 →
        m.Coprime n →
          (ArithmeticFunction.prodPrimeFactors f) (m * n) =
            (ArithmeticFunction.prodPrimeFactors f) m * (ArithmeticFunction.prodPrimeFactors f) n
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: n : ℕ
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiag 3 n
b : Fin 3 → ℕ
hb : b ∈ finMulAntidiag 3 n
hfab : f a ha = f b hb
hfab1 : a 0 * a 1 = b 0 * b 1
hfab2 : a 0 * a 2 = b 0 * b 2
hprods : a 0 * a 1 * a 2 = a 0 * a 1 * b 2
hab2 : a 2 = b 2
hab0 : a 0 = b 0
hab1 : a 1 = b 1
i : Fin 3
⊢ a i = b i

Tactic:
fin_cases i

Goal state after:
case «0»
n : ℕ
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiag 3 n
b : Fin 3 → ℕ
hb : b ∈ finMulAntidiag 3 n
hfab : f a ha = f b hb
hfab1 : a 0 * a 1 = b 0 * b 1
hfab2 : a 0 * a 2 = b 0 * b 2
hprods : a 0 * a 1 * a 2 = a 0 * a 1 * b 2
hab2 : a 2 = b 2
hab0 : a 0 = b 0
hab1 : a 1 = b 1
⊢ a ((fun i ↦ i) ⟨0, ⋯⟩) = b ((fun i ↦ i) ⟨0, ⋯⟩)

case «1»
n : ℕ
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiag 3 n
b : Fin 3 → ℕ
hb : b ∈ finMulAntidiag 3 n
hfab : f a ha = f b hb
hfab1 : a 0 * a 1 = b 0 * b 1
hfab2 : a 0 * a 2 = b 0 * b 2
hprods : a 0 * a 1 * a 2 = a 0 * a 1 * b 2
hab2 : a 2 = b 2
hab0 : a 0 = b 0
hab1 : a 1 = b 1
⊢ a ((fun i ↦ i) ⟨1, ⋯⟩) = b ((fun i ↦ i) ⟨1, ⋯⟩)

case «2»
n : ℕ
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiag 3 n
b : Fin 3 → ℕ
hb : b ∈ finMulAntidiag 3 n
hfab : f a ha = f b hb
hfab1 : a 0 * a 1 = b 0 * b 1
hfab2 : a 0 * a 2 = b 0 * b 2
hprods : a 0 * a 1 * a 2 = a 0 * a 1 * b 2
hab2 : a 2 = b 2
hab0 : a 0 = b 0
hab1 : a 1 = b 1
⊢ a ((fun i ↦ i) ⟨2, ⋯⟩) = b ((fun i ↦ i) ⟨2, ⋯⟩)