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

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
inst✝ : SFinite μ
hf : AEMeasurable f (μ.restrict s)
hg : AEMeasurable g (μ.restrict s)
hs : MeasurableSet s
⊢ (μ.prod volume) (regionBetween f g s) = ∫⁻ (y : α) in s, ofReal ((g - f) y) ∂μ

Tactic:
by
  have h₁ :
    (fun y => ENNReal.ofReal ((g - f) y)) =ᵐ[μ.restrict s] fun y =>
      ENNReal.ofReal ((AEMeasurable.mk g hg - AEMeasurable.mk f hf) y) :=
    (hg.ae_eq_mk.sub hf.ae_eq_mk).fun_comp ENNReal.ofReal
  have h₂ :
    (μ.restrict s).prod volume (regionBetween f g s) =
      (μ.restrict s).prod volume
        (regionBetween (AEMeasurable.mk f hf) (AEMeasurable.mk g hg) s) := by
    apply measure_congr
    apply EventuallyEq.rfl.inter
    exact
      ((quasiMeasurePreserving_fst.ae_eq_comp hf.ae_eq_mk).comp₂ _ EventuallyEq.rfl).inter
        (EventuallyEq.rfl.comp₂ _ <| quasiMeasurePreserving_fst.ae_eq_comp hg.ae_eq_mk)
  rw [lintegral_congr_ae h₁, ←
    volume_regionBetween_eq_lintegral' hf.measurable_mk hg.measurable_mk hs]
  convert! h₂ using 1
  · rw [Measure.restrict_prod_eq_prod_univ]
    exact (Measure.restrict_eq_self _ (regionBetween_subset f g s)).symm
  · rw [Measure.restrict_prod_eq_prod_univ]
    exact
      (Measure.restrict_eq_self _
          (regionBetween_subset (AEMeasurable.mk f hf) (AEMeasurable.mk g hg) s)).symm

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
f_mble : AEMeasurable f μ
g_mble : AEMeasurable g μ
s : Set α
s_mble : NullMeasurableSet s μ
⊢ NullMeasurableSet {p | p.1 ∈ s ∧ p.2 ∈ Ioo (f p.1) (g p.1)} (μ.prod volume)

Tactic:
by
  refine NullMeasurableSet.inter
          (s_mble.preimage quasiMeasurePreserving_fst) (NullMeasurableSet.inter ?_ ?_)
  · exact nullMeasurableSet_lt (by fun_prop) measurable_snd.aemeasurable
  · exact nullMeasurableSet_lt measurable_snd.aemeasurable (by fun_prop)

Goal state after:
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
r : ℝ
hr : r ≠ 0
s : Set E
⊢ (ENNReal.ofReal |(r ^ finrank ℝ E)⁻¹| • μ) s = ENNReal.ofReal |(r ^ finrank ℝ E)⁻¹| * μ s

Tactic:
coe_smul,

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
r : ℝ
hr : r ≠ 0
s : Set E
⊢ (ENNReal.ofReal |(r ^ finrank ℝ E)⁻¹| • ⇑μ) s = ENNReal.ofReal |(r ^ finrank ℝ E)⁻¹| * μ s
Module: Mathlib.Algebra.Module.ZLattice.Basic

Goal state before:
pp: E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁶ : NormedField K
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace K E
b : Basis ι K E
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : FloorRing K
inst✝ : Fintype ι
y : ↥(span ℤ (Set.range ⇑b))
x : E
⊢ y +ᵥ x ∈ fundamentalDomain b ↔ x + ↑y = x + ↑(-floor b x)

Tactic:
NegMemClass.coe_neg,

Goal state after:
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁶ : NormedField K
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace K E
b : Basis ι K E
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : FloorRing K
inst✝ : Fintype ι
y : ↥(span ℤ (Set.range ⇑b))
x : E
⊢ y +ᵥ x ∈ fundamentalDomain b ↔ x + ↑y = x + -↑(floor b x)
Module: Mathlib.Analysis.BoxIntegral.Partition.Basic

Goal state before:
pp: ι : Type u_1
I : Box ι
π : Prepartition I
boxes : Finset (WithBot (Box ι))
le_of_mem : ∀ J ∈ boxes, J ≤ ↑I
pairwise_disjoint : (↑boxes).Pairwise Disjoint
H : ∀ J ∈ boxes, J ≠ ⊥ → ∃ J' ∈ π, J ≤ ↑J'
J : Box ι
hJ : ↑J ∈ boxes
⊢ ∃ J' ∈ π, J ≤ J'

Tactic:
simpa only [WithBot.coe_le_coe] using H J hJ WithBot.coe_ne_bot

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

Goal state before:

Tactic:
‖x‖
  _ = √(∑ i, ‖⟪b i, x⟫‖ ^ 2) := by rw [sum_sq_norm_inner_right, Real.sqrt_sq (by positivity)]
  _ ≤ √(∑ _ : ι, (⨆ j, ‖⟪b j, x⟫‖) ^ 2) := by
    gcongr with i
    exact le_ciSup (f := fun j ↦ ‖⟪b j, x⟫‖) (by simp) i
  _ = √(Fintype.card ι) * ⨆ i, ‖⟪b i, x⟫‖ := by
    simp only [Finset.sum_const, Finset.card_univ, nsmul_eq_mul, Nat.cast_nonneg, Real.sqrt_mul]
    congr
    rw [Real.sqrt_sq]
    cases isEmpty_or_nonempty ι
    · simp
    · exact le_ciSup_of_le (by simp) (Nonempty.some inferInstance) (by positivity)

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

Goal state before:
pp: ι : Type u_1
I : Box ι
i : ι
x : ℝ
⊢ I.splitUpper i x = ⊥ ↔ I.upper i ≤ x

Tactic:
rw [splitUpper, mk'_eq_bot, exists_update_iff I.lower fun j y => I.upper j ≤ y]

Goal state after:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
⊢ (I.upper i ≤ max x (I.lower i) ∨ ∃ x, x ≠ i ∧ I.upper x ≤ I.lower x) ↔ I.upper i ≤ x
Module: Mathlib.Analysis.InnerProductSpace.PiL2

Goal state before:
pp: case e'_3.e'_4
ι : 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)
⊢ x = ∑ i, p.ofLp i • v i

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 x, v.equivFun_symm_apply]

Goal state after:
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
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 : ι → E
hon : Orthonormal 𝕜 v
hsp : (span 𝕜 (range v))ᗮ = ⊥
this✝ : FiniteDimensional 𝕜 ↥(span 𝕜 (range v))
this : CompleteSpace ↥(span 𝕜 (range v))
⊢ span 𝕜 (range v) = ⊤

Tactic:
rwa [orthogonal_eq_bot_iff] at hsp

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

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_3
inst✝³ : RCLike 𝕜
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x : EuclideanSpace 𝕜 ι
⊢ ((EuclideanSpace.basisFun ι 𝕜).equiv b (Equiv.refl ι)) x = ∑ i, x.ofLp i • b i

Tactic:
by
  simp_rw [equiv_apply, EuclideanSpace.basisFun_repr, Equiv.refl_apply]

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

Goal state before:
pp: case pos
ι : Type u_1
M : Type u_2
n : ℕ
N : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
I₀✝ : WithTop (Box ι)
I✝ : Box ι
i : ι
inst✝ : Finite ι
f : Box ι → M
I₀ : WithTop (Box ι)
hf :
  ∀ (I : Box ι),
    ↑I ≤ I₀ →
      ∀ {i : ι} {x : ℝ},
        x ∈ Set.Ioo (I.lower i) (I.upper i) →
          Option.elim' 0 f (I.splitLower i x) + Option.elim' 0 f (I.splitUpper i x) = f I
I : Box ι
hI : ↑I ≤ I₀
a : ι × ℝ
s : Finset (ι × ℝ)
a✝ : a ∉ s
ihs : ∑ J ∈ (splitMany I s).boxes, f J = f I
J' : Box ι
hJ' : J' ∈ (splitMany I s).boxes
h : a.2 ∈ Set.Ioo (J'.lower a.1) (J'.upper a.1)
⊢ ∑ J' ∈ (split J' a.1 a.2).boxes, f J' = f J'

Tactic:
rw [sum_split_boxes]

Goal state after:
case pos
ι : Type u_1
M : Type u_2
n : ℕ
N : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
I₀✝ : WithTop (Box ι)
I✝ : Box ι
i : ι
inst✝ : Finite ι
f : Box ι → M
I₀ : WithTop (Box ι)
hf :
  ∀ (I : Box ι),
    ↑I ≤ I₀ →
      ∀ {i : ι} {x : ℝ},
        x ∈ Set.Ioo (I.lower i) (I.upper i) →
          Option.elim' 0 f (I.splitLower i x) + Option.elim' 0 f (I.splitUpper i x) = f I
I : Box ι
hI : ↑I ≤ I₀
a : ι × ℝ
s : Finset (ι × ℝ)
a✝ : a ∉ s
ihs : ∑ J ∈ (splitMany I s).boxes, f J = f I
J' : Box ι
hJ' : J' ∈ (splitMany I s).boxes
h : a.2 ∈ Set.Ioo (J'.lower a.1) (J'.upper a.1)
⊢ Option.elim' 0 f (J'.splitLower a.1 a.2) + Option.elim' 0 f (J'.splitUpper a.1 a.2) = f J'
Module: Mathlib.Analysis.BoxIntegral.UnitPartition

Goal state before:
pp: ι : Type u_1
n : ℕ
inst✝ : NeZero n
ν : ι → ℤ
⊢ tag n ν ∈ box n ν

Tactic:
refine mem_box_iff.mpr fun _ ↦ ?_

Goal state after:
ι : Type u_1
n : ℕ
inst✝ : NeZero n
ν : ι → ℤ
x✝ : ι
⊢ ↑(ν x✝) / ↑n < tag n ν x✝ ∧ tag n ν x✝ ≤ (↑(ν x✝) + 1) / ↑n
Module: Mathlib.Analysis.BoxIntegral.Integrability

Goal state before:
pp: ι : Type u
E : Type v
inst✝³ : Fintype ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
l : IntegrationParams
hl : l.bRiemann = false
s : Set (ι → ℝ)
hs : MeasurableSet s
I : Box ι
y : E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
ε : ℝ≥0
ε0 : 0 < ε
A : μ (s ∩ Box.Icc I) ≠ ∞
B : μ (s ∩ ↑I) ≠ ∞
F : Set (ι → ℝ)
hFs : F ⊆ s ∩ Box.Icc I
hFc : IsClosed F
hμF : μ ((s ∩ Box.Icc I) \ F) < ↑ε
U : Set (ι → ℝ)
hsU : s ∩ Box.Icc I ⊆ U
hUo : IsOpen U
hUt : μ U < ∞
hμU : μ (U \ (s ∩ Box.Icc I)) < ↑ε
rs : (ι → ℝ) → ↑(Set.Ioi 0)
hrsU : ∀ x ∈ s ∩ Box.Icc I, closedBall x ↑(rs x) ⊆ U
x : ι → ℝ
hx : x ∈ Box.Icc I \ s
⊢ ∃ r, closedBall x ↑r ⊆ Fᶜ

Tactic:
obtain ⟨r, hr₀, hr⟩ :=
      nhds_basis_closedBall.mem_iff.1 (hFc.isOpen_compl.mem_nhds fun hx' => hx.2 (hFs hx').1)
    exact ⟨⟨r, hr₀⟩, hr⟩

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

Goal state before:
pp: ι : Type u_1
n : ℕ
inst✝ : NeZero n
⊢ Function.Injective fun ν ↦ box n ν

Tactic:
intro _ _ h
  contrapose! h
  exact Box.ne_of_disjoint_coe (disjoint.mp 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)
⊢ (B.lower ≤ fun i ↦ ↑(index n x i) / ↑n) ∧ (box n (index n x)).upper ≤ B.upper

Tactic:
box_upper,

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)
⊢ (B.lower ≤ fun i ↦ ↑(index n x i) / ↑n) ∧ (fun i ↦ (↑(index n x i) + 1) / ↑n) ≤ B.upper
Module: Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
f : ι → E
hf : Pairwise fun x1 x2 ↦ ⟪f x1, f x2⟫_𝕜 = 0
i : ι
⊢ f i - ∑ i_1 < i, (𝕜 ∙ gramSchmidt 𝕜 f i_1).starProjection (f i) = f i - 0

pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
f : ι → E
hf : Pairwise fun x1 x2 ↦ ⟪f x1, f x2⟫_𝕜 = 0
i : ι
⊢ f i - 0 = f i

Tactic:
· congr
    apply Finset.sum_eq_zero
    intro j hj
    rw [Submodule.starProjection_apply, Submodule.coe_eq_zero]
    suffices span 𝕜 (f '' Set.Iic j) ⟂ 𝕜 ∙ f i by
      apply orthogonalProjectionOnto_apply_of_mem_orthogonal
      rw [mem_orthogonal_singleton_iff_inner_left, ← mem_orthogonal_singleton_iff_inner_right]
      exact this (gramSchmidt_mem_span 𝕜 f (le_refl j))
    rw [isOrtho_span]
    rintro u ⟨k, hk, rfl⟩ v (rfl : v = f i)
    apply hf
    exact (lt_of_le_of_lt hk (Finset.mem_Iio.mp hj)).ne

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
f : ι → E
hf : Pairwise fun x1 x2 ↦ ⟪f x1, f x2⟫_𝕜 = 0
i : ι
⊢ f i - 0 = f i
Module: Mathlib.LinearAlgebra.Orientation

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_4
inst✝ : Finite ι
e : Basis ι R M
x : Orientation R M ι
f : M ≃ₗ[R] M
⊢ (Orientation.map ι f) x = (LinearEquiv.det f)⁻¹ • x

Tactic:
cases nonempty_fintype ι
  let := Classical.decEq ι
  induction x using Module.Ray.ind with | h g hg =>
  rw [Orientation.map_apply, smul_rayOfNeZero, ray_eq_iff, Units.smul_def,
    (g.compLinearMap f.symm).eq_smul_basis_det e, g.eq_smul_basis_det e,
    AlternatingMap.compLinearMap_apply, AlternatingMap.smul_apply,
    show (fun i ↦ (LinearEquiv.symm f).toLinearMap (e i)) = (LinearEquiv.symm f).toLinearMap ∘ e
    by rfl, Basis.det_comp, Basis.det_self, mul_one, smul_eq_mul, mul_comm, mul_smul,
    LinearEquiv.coe_inv_det]

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

Goal state before:
pp: case mpr
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
e f : OrthonormalBasis ι ℝ E
h : e.toBasis.orientation = f.toBasis.orientation
⊢ e.toBasis.det ⇑f.toBasis • f.toBasis.det = f.toBasis.det

Tactic:
simp [e.det_to_matrix_orthonormalBasis_of_same_orientation f h]

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = 0)
⊢ ¬rayOfNeZero ℝ (-AlternatingMap.constLinearEquivOfIsEmpty 1) ⋯ =
      rayOfNeZero ℝ (AlternatingMap.constLinearEquivOfIsEmpty 1) ⋯

Tactic:
rw [ray_eq_iff, SameRay.sameRay_comm]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = 0)
⊢ ¬SameRay ℝ (AlternatingMap.constLinearEquivOfIsEmpty 1) (-AlternatingMap.constLinearEquivOfIsEmpty 1)
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 < ε
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖f b‖ ≤ ε / 2 * g b
this : (fun x ↦ ∑ i ∈ Finset.range N, f i) =o[atTop] fun n ↦ ∑ i ∈ Finset.range n, g i
n : ℕ
hn : ‖∑ i ∈ Finset.range N, f i‖ ≤ ε / 2 * ‖∑ i ∈ Finset.range n, g i‖
Nn : n ∈ Set.Ici N
⊢ ‖∑ i ∈ Finset.range N, f i‖ + ∑ i ∈ Finset.range n, ε / 2 * g i ≤
    ε / 2 * ‖∑ i ∈ Finset.range n, g i‖ + ε / 2 * ∑ i ∈ Finset.range n, g i

Tactic:
by rw [← mul_sum]; gcongr

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: p : ℕ
⊢ (Summable fun n ↦ 1 / ↑n ^ p) ↔ 1 < p

Tactic:
by
  refine ⟨fun h ↦ summable_one_div_nat_pow.mp (h.comp_injective Nat.cast_injective),
    fun h ↦ .of_nat_of_neg (summable_one_div_nat_pow.mpr h)
      (((summable_one_div_nat_pow.mpr h).mul_left <| 1 / (-1 : ℝ) ^ p).congr fun n ↦ ?_)⟩
  rw [Int.cast_neg, Int.cast_natCast, neg_eq_neg_one_mul (n : ℝ), mul_pow, mul_one_div, div_div]

Goal state after:
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
this✝ : Finite ι
b' : Basis ι ℝ E := Basis.ofZLatticeBasis ℝ L b
e : E ≃L[ℝ] ι → ℝ := (b'.repr ≪≫ₗ Finsupp.linearEquivFunOnFinite ℝ ℝ ι).toContinuousLinearEquiv
this : IsOpen (⇑e ⁻¹' Set.univ.pi fun x ↦ Set.Ioo (-1) 1)
⊢ ∃ ε, 0 < ε ∧ ∀ (x : ↥L) (i : ι), ε * ↑|(b.repr x) i| ≤ ‖x‖

Tactic:
obtain ⟨ε, hε, hε'⟩ := Metric.isOpen_iff.mp this 0 (by simp)

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 ι
b' : Basis ι ℝ E := Basis.ofZLatticeBasis ℝ L b
e : E ≃L[ℝ] ι → ℝ := (b'.repr ≪≫ₗ Finsupp.linearEquivFunOnFinite ℝ ℝ ι).toContinuousLinearEquiv
this : IsOpen (⇑e ⁻¹' Set.univ.pi fun x ↦ Set.Ioo (-1) 1)
ε : ℝ
hε : ε > 0
hε' : Metric.ball 0 ε ⊆ ⇑e ⁻¹' Set.univ.pi fun x ↦ Set.Ioo (-1) 1
⊢ ∃ ε, 0 < ε ∧ ∀ (x : ↥L) (i : ι), ε * ↑|(b.repr x) i| ≤ ‖x‖
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
k n : ℕ
⊢ ((↑k + 1) ^ 2)⁻¹ + ∑ i ∈ Ioc k.succ (max (k + 1) n), (↑i ^ 2)⁻¹ ≤ ((↑k + 1) ^ 2)⁻¹ + (↑k + 1)⁻¹

Tactic:
refine add_le_add le_rfl ((sum_Ioc_inv_sq_le_sub ?_ (le_max_left _ _)).trans ?_)

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

case refine_2
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
k n : ℕ
⊢ (↑k.succ)⁻¹ - (↑(max k.succ n))⁻¹ ≤ (↑k + 1)⁻¹
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.1 ∈ f.coeff.support ∧ x gh.2 ≠ 0 ∧ gh.1 • gh.2 = p ↔ f.coeff gh.1 ≠ 0 ∧ x gh.2 ≠ 0 ∧ gh.1 • gh.2 = p

Tactic:
Finsupp.mem_support_iff

Goal state after:
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
⊢ f.coeff gh.1 ≠ 0 ∧ x gh.2 ≠ 0 ∧ gh.1 • gh.2 = p ↔ f.coeff gh.1 ≠ 0 ∧ x gh.2 ≠ 0 ∧ gh.1 • gh.2 = p
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:
let to_hom : AddMonoidAlgebra M ι →+ ⨁ _ : ι, M :=
  { toFun := toDirectSum
    map_zero' := toDirectSum_zero
    map_add' := toDirectSum_add }
  change to_hom (f * g) = to_hom f * to_hom g
  revert f g
  rw [AddMonoidHom.map_mul_iff]
  ext xi xv yi yv : 4
  simp [to_hom, AddMonoidAlgebra.single_mul_single, DirectSum.of_mul_of]

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

Goal state before:
pp: σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst✝ : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R
g : MvPolynomial τ R →ₐ[R] MvPolynomial υ R
x : υ → R
i : σ
this : g = aeval fun i ↦ g (X i)
⊢ g (f (X i)) = (aeval fun i ↦ g (X i)) (f (X i))

Tactic:
rw [← this]

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

Goal state before:
pp: case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
r s : R
i j : σ →₀ ℕ
x : MvPolynomial σ R
hx : ∀ (m : σ →₀ ℕ), coeff m ((monomial j) s) = coeff m ((monomial i) r * x)
hi✝ : (if j = i then s else 0) = if i ≤ i then r * coeff (i - i) x else 0
hi : i ≤ j
hj : s = r * coeff (j - i) x
⊢ (s = 0 ∨ i ≤ j) ∧ r ∣ s

pp: case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
r s : R
i j : σ →₀ ℕ
x : MvPolynomial σ R
hx : ∀ (m : σ →₀ ℕ), coeff m ((monomial j) s) = coeff m ((monomial i) r * x)
hi✝ : (if j = i then s else 0) = if i ≤ i then r * coeff (i - i) x else 0
hi : ¬i ≤ j
hj : s = 0
⊢ (s = 0 ∨ i ≤ j) ∧ r ∣ s

Tactic:
· exact ⟨Or.inr hi, _, hj⟩

Goal state after:
case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
r s : R
i j : σ →₀ ℕ
x : MvPolynomial σ R
hx : ∀ (m : σ →₀ ℕ), coeff m ((monomial j) s) = coeff m ((monomial i) r * x)
hi✝ : (if j = i then s else 0) = if i ≤ i then r * coeff (i - i) x else 0
hi : ¬i ≤ j
hj : s = 0
⊢ (s = 0 ∨ i ≤ j) ∧ r ∣ s
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: 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 ⋯

Tactic:
specialize ih (hc.mono <| s.subset_insert a)

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
hc : (↑(insert a s)).Pairwise (Commute on x)
ih : ∀ (n : ℕ), s.sum x ^ n = ∑ k, ↑(↑↑k).countPerms * (Multiset.map x ↑↑k).noncommProd ⋯
n : ℕ
⊢ (insert a s).sum x ^ n = ∑ k, ↑(↑↑k).countPerms * (Multiset.map x ↑↑k).noncommProd ⋯
Module: Mathlib.Data.DFinsupp.WellFounded

Goal state before:
pp: case neg
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → x j = if j ∈ p then x₁ j else x₂ j
hp : i ∉ p
hs : s i (x i) (x₂ i)
⊢ ∃ a',
    InvImage (GameAdd (DFinsupp.Lex r s) (DFinsupp.Lex r s)) snd a' (p, x₁, x₂) ∧
      (fun x ↦ x.2.1.piecewise x.2.2 x.1) a' = x

Tactic:
· refine ⟨⟨{ j | r j i ∧ j ∈ p }, x₁, piecewise x₂ x { j | r j i }⟩,
      .snd ⟨i, fun j hj ↦ ?_, ?_⟩, ?_⟩ <;> simp only [piecewise_apply, Set.mem_ofPred_eq]
    · exact if_pos hj
    · split_ifs with hi
      · rwa [hr i hi, if_neg hp] at hs
      · assumption
    · ext1 j
      simp only [piecewise_apply, Set.mem_ofPred_eq]
      split_ifs with h₁ h₂ <;> try rfl
      · rw [hr j h₁.1, if_pos h₁.2]
      · rw [hr j h₂, if_neg]
        simpa [h₂] using h₁

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

Goal state before:
pp: R : Type u_1
σ : Type u_2
n : σ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : NoZeroDivisors R
hp : p ≠ 0
hq : q ≠ 0
⊢ ((optionEquivLeft R { b // b ≠ n }) ((renameEquiv R (optionSubtypeNe n).symm) p) *
        (optionEquivLeft R { b // b ≠ n }) ((renameEquiv R (optionSubtypeNe n).symm) q)).natDegree =
    ((optionEquivLeft R { b // b ≠ n }) ((renameEquiv R (optionSubtypeNe n).symm) p)).natDegree +
      ((optionEquivLeft R { b // b ≠ n }) ((renameEquiv R (optionSubtypeNe n).symm) q)).natDegree

Tactic:
rw [Polynomial.natDegree_mul] <;> simpa [-renameEquiv_apply, EmbeddingLike.map_eq_zero_iff]

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

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

Tactic:
rintro ⟨hb, hp | hp⟩

Goal state after:
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

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