mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction

Goal state before:
pp: case refine_1
ι : Type u_1
inst✝ : Fintype ι
I : Box ι
r : (ι → ℝ) → ↑(Ioi 0)
J : Box ι
x✝ : J ≤ I
πi : (J' : Box ι) → TaggedPrepartition J'
hP✝ : ∀ J' ∈ splitCenter J, (πi J').IsPartition
hHen : ∀ J' ∈ splitCenter J, (πi J').IsHenstock
hr : ∀ J' ∈ splitCenter J, (πi J').IsSubordinate r
a✝ : ∀ J' ∈ splitCenter J, (πi J').distortion = J'.distortion
n : Box ι → Box ι → ℕ
hn : ∀ J' ∈ splitCenter J, ∀ J ∈ πi J', ∀ (i : ι), J.upper i - J.lower i = (J'.upper i - J'.lower i) / 2 ^ n J' J
hP : ((splitCenter J).biUnionTagged πi).IsPartition
⊢ ∃ π,
    π.IsPartition ∧
      π.IsHenstock ∧
        π.IsSubordinate r ∧
          (∀ J_1 ∈ π, ∃ m, ∀ (i : ι), J_1.upper i - J_1.lower i = (J.upper i - J.lower i) / 2 ^ m) ∧
            π.distortion = J.distortion

Tactic:
have hsub : ∀ J' ∈ (splitCenter J).biUnionTagged πi, ∃ n : ℕ, ∀ i,
        (J' :).upper i - J'.lower i = (J.upper i - J.lower i) / 2 ^ n := by
      intro J' hJ'
      rcases (splitCenter J).mem_biUnionTagged.1 hJ' with ⟨J₁, h₁, h₂⟩
      refine ⟨n J₁ J' + 1, fun i => ?_⟩
      simp only [hn J₁ h₁ J' h₂, upper_sub_lower_of_mem_splitCenter h₁, pow_succ', div_div]

Goal state after:
case refine_1
ι : Type u_1
inst✝ : Fintype ι
I : Box ι
r : (ι → ℝ) → ↑(Ioi 0)
J : Box ι
x✝ : J ≤ I
πi : (J' : Box ι) → TaggedPrepartition J'
hP✝ : ∀ J' ∈ splitCenter J, (πi J').IsPartition
hHen : ∀ J' ∈ splitCenter J, (πi J').IsHenstock
hr : ∀ J' ∈ splitCenter J, (πi J').IsSubordinate r
a✝ : ∀ J' ∈ splitCenter J, (πi J').distortion = J'.distortion
n : Box ι → Box ι → ℕ
hn : ∀ J' ∈ splitCenter J, ∀ J ∈ πi J', ∀ (i : ι), J.upper i - J.lower i = (J'.upper i - J'.lower i) / 2 ^ n J' J
hP : ((splitCenter J).biUnionTagged πi).IsPartition
hsub :
  ∀ J' ∈ (splitCenter J).biUnionTagged πi, ∃ n, ∀ (i : ι), J'.upper i - J'.lower i = (J.upper i - J.lower i) / 2 ^ n
⊢ ∃ π,
    π.IsPartition ∧
      π.IsHenstock ∧
        π.IsSubordinate r ∧
          (∀ J_1 ∈ π, ∃ m, ∀ (i : ι), J_1.upper i - J_1.lower i = (J.upper i - J.lower i) / 2 ^ m) ∧
            π.distortion = J.distortion
Module: Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction

Goal state before:
pp: case refine_2
ι : Type u_1
inst✝ : Fintype ι
I : Box ι
r : (ι → ℝ) → ↑(Ioi 0)
z : ι → ℝ
x✝ : z ∈ Box.Icc I
⊢ ∀ J ≤ I,
    ∀ (m : ℕ),
      z ∈ Box.Icc J →
        Box.Icc J ⊆ Box.Icc I ∩ closedBall z ↑(r z) →
          (∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / 2 ^ m) →
            ∃ π,
              π.IsPartition ∧
                π.IsHenstock ∧
                  π.IsSubordinate r ∧
                    (∀ J_1 ∈ π, ∃ m, ∀ (i : ι), J_1.upper i - J_1.lower i = (J.upper i - J.lower i) / 2 ^ m) ∧
                      π.distortion = J.distortion

Tactic:
intro J

Goal state after:
case refine_2
ι : Type u_1
inst✝ : Fintype ι
I : Box ι
r : (ι → ℝ) → ↑(Ioi 0)
z : ι → ℝ
x✝ : z ∈ Box.Icc I
J : Box ι
⊢ J ≤ I →
    ∀ (m : ℕ),
      z ∈ Box.Icc J →
        Box.Icc J ⊆ Box.Icc I ∩ closedBall z ↑(r z) →
          (∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / 2 ^ m) →
            ∃ π,
              π.IsPartition ∧
                π.IsHenstock ∧
                  π.IsSubordinate r ∧
                    (∀ J_1 ∈ π, ∃ m, ∀ (i : ι), J_1.upper i - J_1.lower i = (J.upper i - J.lower i) / 2 ^ m) ∧
                      π.distortion = J.distortion
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 : E
⊢ 0 ≤ ∑ x_1, ‖⟪b x_1, x⟫‖ ^ 2

Tactic:
exact Fintype.sum_nonneg fun _ ↦ by positivity

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

Goal state before:
pp: ι : Type u_1
M : Type u_2
n : ℕ
N : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
I₀ : WithTop (Box ι)
I✝ : Box ι
i : ι
R : Type ?u.17
inst✝¹ : Monoid R
inst✝ : DistribMulAction R M
r : R
f : ι →ᵇᵃ[I₀] M
I : Box ι
hI : ↑I ≤ I₀
π : Prepartition I
hπ : π.IsPartition
⊢ ∑ Ji ∈ π.boxes, (r • ⇑f) Ji = (r • ⇑f) I

Tactic:
by
      simp only [Pi.smul_apply, ← smul_sum, sum_partition_boxes _ hI hπ]

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

Goal state before:
pp: ι : Type u_1
M : Type u_2
n : ℕ
N : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
I₀✝ : WithTop (Box ι)
I : Box ι
i✝ : ι
G : Type u
inst✝ : AddCommGroup G
I₀ : Box (Fin (n + 1))
i : Fin (n + 1)
f : ℝ → Box (Fin n) → G
fb : ↑(Set.Icc (I₀.lower i) (I₀.upper i)) → Fin n →ᵇᵃ[↑(I₀.face i)] G
hf : ∀ (x : ℝ) (hx : x ∈ Set.Icc (I₀.lower i) (I₀.upper i)) (J : Box (Fin n)), f x J = (fb ⟨x, hx⟩) J
⊢ ∀ (I : Box (Fin (n + 1))),
    ↑I ≤ ↑I₀ →
      ∀ {i_1 : Fin (n + 1)} {x : ℝ},
        x ∈ Set.Ioo (I.lower i_1) (I.upper i_1) →
          Option.elim' 0 (fun J ↦ f (J.upper i) (J.face i) - f (J.lower i) (J.face i)) (I.splitLower i_1 x) +
              Option.elim' 0 (fun J ↦ f (J.upper i) (J.face i) - f (J.lower i) (J.face i)) (I.splitUpper i_1 x) =
            f (I.upper i) (I.face i) - f (I.lower i) (I.face i)

Tactic:
intro J

Goal state after:
ι : Type u_1
M : Type u_2
n : ℕ
N : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
I₀✝ : WithTop (Box ι)
I : Box ι
i✝ : ι
G : Type u
inst✝ : AddCommGroup G
I₀ : Box (Fin (n + 1))
i : Fin (n + 1)
f : ℝ → Box (Fin n) → G
fb : ↑(Set.Icc (I₀.lower i) (I₀.upper i)) → Fin n →ᵇᵃ[↑(I₀.face i)] G
hf : ∀ (x : ℝ) (hx : x ∈ Set.Icc (I₀.lower i) (I₀.upper i)) (J : Box (Fin n)), f x J = (fb ⟨x, hx⟩) J
J : Box (Fin (n + 1))
⊢ ↑J ≤ ↑I₀ →
    ∀ {i_1 : Fin (n + 1)} {x : ℝ},
      x ∈ Set.Ioo (J.lower i_1) (J.upper i_1) →
        Option.elim' 0 (fun J ↦ f (J.upper i) (J.face i) - f (J.lower i) (J.face i)) (J.splitLower i_1 x) +
            Option.elim' 0 (fun J ↦ f (J.upper i) (J.face i) - f (J.lower i) (J.face i)) (J.splitUpper i_1 x) =
          f (J.upper i) (J.face i) - f (J.lower i) (J.face i)
Module: Mathlib.Analysis.Oscillation

Goal state before:
pp: case right
E : Type u
F : Type v
inst✝¹ : PseudoEMetricSpace F
inst✝ : PseudoEMetricSpace E
K : Set E
f : E → F
D : Set E
ε : ℝ≥0∞
comp : IsCompact K
hK : ∀ x ∈ K, oscillationWithin f D x < ε
S : ℝ → Set E := fun r ↦ {x | ∃ a > r, ediam (f '' (eball x (ENNReal.ofReal a) ∩ D)) ≤ ε}
S_open : ∀ r > 0, IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (S r)
S_cover : K ⊆ ⋃ r, ⋃ (_ : r > 0), S r
S_antitone : ∀ (r₁ r₂ : ℝ), r₁ ≤ r₂ → S r₂ ⊆ S r₁
T : Set ℝ
Tb : T ⊆ Real.lt✝ 0
Tfin : T.Finite
hT : K ⊆ ⋃ i ∈ T, S i
T_nonempty : T.Nonempty
x : E
hx : x ∈ K
r : ℝ
hr : x ∈ ⋃ (_ : r ∈ T), S r
⊢ x ∈ S (⋯.min T_nonempty)

Tactic:
simp only [mem_iUnion, exists_prop] at hr

Goal state after:
case right
E : Type u
F : Type v
inst✝¹ : PseudoEMetricSpace F
inst✝ : PseudoEMetricSpace E
K : Set E
f : E → F
D : Set E
ε : ℝ≥0∞
comp : IsCompact K
hK : ∀ x ∈ K, oscillationWithin f D x < ε
S : ℝ → Set E := fun r ↦ {x | ∃ a > r, ediam (f '' (eball x (ENNReal.ofReal a) ∩ D)) ≤ ε}
S_open : ∀ r > 0, IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (S r)
S_cover : K ⊆ ⋃ r, ⋃ (_ : r > 0), S r
S_antitone : ∀ (r₁ r₂ : ℝ), r₁ ≤ r₂ → S r₂ ⊆ S r₁
T : Set ℝ
Tb : T ⊆ Real.lt✝ 0
Tfin : T.Finite
hT : K ⊆ ⋃ i ∈ T, S i
T_nonempty : T.Nonempty
x : E
hx : x ∈ K
r : ℝ
hr : r ∈ T ∧ x ∈ S r
⊢ x ∈ S (⋯.min T_nonempty)
Module: Mathlib.Analysis.BoxIntegral.UnitPartition

Goal state before:
pp: ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
B : Box ι
ν : ι → ℤ
hν : ν ∈ admissibleIndex n B
hI : box n ν ∈ prepartition n B
⊢ tag n ν ∈ Box.Icc (box n ν)

Tactic:
exact Box.coe_subset_Icc (tag_mem _ _)

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

Goal state before:
pp: case refine_1
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
B : Box ι
r : ℝ
hr : 0 < r
hn : 1 / ↑n ≤ r
ν : ι → ℤ
hν : ν ∈ admissibleIndex n B
hI : box n ν ∈ prepartition n B
x✝ : ι → ℝ
h : x✝ ∈ Box.Icc (box n ν)
⊢ tag n ν ∈ Box.Icc (box n ν)

Tactic:
exact Box.coe_subset_Icc (tag_mem _ _)

Goal state after:
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 ι
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional 𝕜 E
h : finrank 𝕜 E = Fintype.card ι
f : ι → E
hf : Pairwise fun i j ↦ ⟪f i, f j⟫_𝕜 = 0
i : ι
hi : f i ≠ 0
⊢ (gramSchmidtOrthonormalBasis h f) i = (↑‖f i‖)⁻¹ • f i

Tactic:
have H : gramSchmidtNormed 𝕜 f i = (‖f i‖⁻¹ : 𝕜) • f i := by
    rw [gramSchmidtNormed, gramSchmidt_of_orthogonal 𝕜 hf]
  rw [gramSchmidtOrthonormalBasis_apply h, H]
  simpa [H] using hi

Goal state after:
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
h₁ : π₁.IsPartition
h₂ : π₂.IsPartition
⊢ ∑ J ∈ (π₁.infPrepartition π₂.toPrepartition).boxes, (vol J) (f ((π₁.infPrepartition π₂.toPrepartition).tag J)) -
      ∑ J ∈ (π₂.infPrepartition π₁.toPrepartition).boxes, (vol J) (f ((π₂.infPrepartition π₁.toPrepartition).tag J)) =
    ∑ J ∈ (π₁.toPrepartition ⊓ π₂.toPrepartition).boxes,
      ((vol J) (f ((π₁.infPrepartition π₂.toPrepartition).tag J)) -
        (vol J) (f ((π₂.infPrepartition π₁.toPrepartition).tag J)))

Tactic:
Finset.sum_sub_distrib

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 ι
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
π₁ π₂ : TaggedPrepartition I
h₁ : π₁.IsPartition
h₂ : π₂.IsPartition
⊢ ∑ J ∈ (π₁.infPrepartition π₂.toPrepartition).boxes, (vol J) (f ((π₁.infPrepartition π₂.toPrepartition).tag J)) -
      ∑ J ∈ (π₂.infPrepartition π₁.toPrepartition).boxes, (vol J) (f ((π₂.infPrepartition π₁.toPrepartition).tag J)) =
    ∑ x ∈ (π₁.toPrepartition ⊓ π₂.toPrepartition).boxes, (vol x) (f ((π₁.infPrepartition π₂.toPrepartition).tag x)) -
      ∑ x ∈ (π₁.toPrepartition ⊓ π₂.toPrepartition).boxes, (vol x) (f ((π₂.infPrepartition π₁.toPrepartition).tag 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 ι
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
π₁ π₂ : TaggedPrepartition I
h₁ : π₁.IsPartition
h₂ : π₂.IsPartition
⊢ integralSum f vol π₁ - integralSum f vol π₂ =
    ∑ J ∈ (π₁.toPrepartition ⊓ π₂.toPrepartition).boxes,
      ((vol J) (f ((π₁.infPrepartition π₂.toPrepartition).tag J)) -
        (vol J) (f ((π₂.infPrepartition π₁.toPrepartition).tag J)))

Tactic:
rw [← integralSum_inf_partition f vol π₁ h₂, ← integralSum_inf_partition f vol π₂ h₁,
    integralSum, integralSum, Finset.sum_sub_distrib]
  simp only [infPrepartition_toPrepartition, inf_comm]

Goal state after:
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
inst✝ : Fintype ι
I : Box ι
l : IntegrationParams
f₁ f₂ : (ι → ℝ) → E
vol₁ vol₂ : ι →ᵇᵃ[⊤] E →L[ℝ] F
hf : EqOn f₁ f₂ (Box.Icc I)
hvol : EqOn (⇑vol₁) (⇑vol₂) (Set.Iic I)
y : F
π : TaggedPrepartition I
⊢ ↑π.boxes ⊆ Set.Iic I

Tactic:
intro J

Goal state after:
ι : Type u
E : Type v
F : Type w
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : Fintype ι
I : Box ι
l : IntegrationParams
f₁ f₂ : (ι → ℝ) → E
vol₁ vol₂ : ι →ᵇᵃ[⊤] E →L[ℝ] F
hf : EqOn f₁ f₂ (Box.Icc I)
hvol : EqOn (⇑vol₁) (⇑vol₂) (Set.Iic I)
y : F
π : TaggedPrepartition I
J : Box ι
⊢ J ∈ ↑π.boxes → J ∈ Set.Iic I
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
h : ¬Integrable I l f vol
⊢ integral I l (-f) vol = -integral I l f vol

Tactic:
rw [integral, integral, dif_neg h, dif_neg (mt Integrable.of_neg h), neg_zero]

Goal state after:
Module: Mathlib.LinearAlgebra.Orientation

Goal state before:
pp: 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✝¹ : Fintype ι
inst✝ : DecidableEq ι
e : Basis ι R M
i : ι
⊢ (∏ i_1, Function.update 1 i (-1) i_1)⁻¹ • e.orientation = -e.orientation

Tactic:
Finset.prod_update_of_mem (Finset.mem_univ _)

Goal state after:
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✝¹ : Fintype ι
inst✝ : DecidableEq ι
e : Basis ι R M
i : ι
⊢ (-1 * ∏ x ∈ Finset.univ \ {i}, 1 x)⁻¹ • e.orientation = -e.orientation
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
⊢ dist (integralSum f vol π) (∑ J ∈ π₀.boxes, integral J l f vol) ≤ ε + δ

Tactic:
have δ'0 : 0 < δ' := div_pos δ0 H0

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 < δ'
⊢ dist (integralSum f vol π) (∑ J ∈ π₀.boxes, integral J l f vol) ≤ ε + δ
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 ∈ π₀,
    ∃ πi,
      πi.IsPartition ∧ dist (integralSum f vol πi) (integral J l f vol) ≤ δ' ∧ l.MemBaseSet J C (h.convergenceR δ' C) πi

Tactic:
intro J

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 ι
⊢ J ∈ π₀ →
    ∃ πi,
      πi.IsPartition ∧ dist (integralSum f vol πi) (integral J l f vol) ≤ δ' ∧ l.MemBaseSet J C (h.convergenceR δ' C) πi
Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics

Goal state before:
pp: α : Type u_1
l : Filter α
f g : α → ℝ
hfg : f ~[l] g
g_tendsto : Tendsto g l atTop
⊢ (fun n ↦ Real.log (f n)) ~[l] fun n ↦ Real.log (g n)

Tactic:
have hg := g_tendsto.eventually_ne_atTop 0
  have hf := hfg.symm.tendsto_atTop g_tendsto |>.eventually_ne_atTop 0
  rw [isEquivalent_iff_tendsto_one hg] at hfg
  have := hfg.log (by norm_num) |>.congr' <| by
    filter_upwards [hf, hg] with n hf hg using Real.log_div hf hg
  exact IsLittleO.isEquivalent <| calc
    (fun n ↦ Real.log (f n) - Real.log (g n)) =o[l] fun _ ↦ (1 : ℝ) := by simpa
    _ =o[l] fun n ↦ Real.log (g n) := isLittleO_one_left_iff ℝ |>.mpr <|
      tendsto_norm_atTop_atTop.comp <| Real.tendsto_log_atTop.comp g_tendsto

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: ⊢ ¬Summable fun i ↦ 1 / (↑i + 1)

Tactic:
exact_mod_cast mt (_root_.summable_nat_add_iff 1).1 not_summable_one_div_natCast

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]
        congr with k
        push_cast
        rw [Real.mul_rpow (by positivity) (by positivity), mul_pow]
        group

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

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

Tactic:
exact DFinsupp.toFinsupp_neg ..

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommRing R
P : MvPolynomial σ R
H✝ : IsUnit P
n : σ →₀ ℕ
hn : n ≠ 0
i : σ
hi : n i ≠ 0
e : Polynomial (MvPolynomial { b // b ≠ i } R) ≃ₐ[R] MvPolynomial σ R :=
  (optionEquivLeft R { b // b ≠ i }).symm.trans (renameEquiv R (Equiv.optionSubtypeNe i))
H : ∀ (i_1 : { b // ¬b = i } →₀ ℕ), IsNilpotent (coeff i_1 ((e.symm P).coeff (n i)))
⊢ coeff (Finsupp.equivMapDomain (Equiv.optionSubtypeNe i).symm n)
      ((renameEquiv R (Equiv.optionSubtypeNe i)).toRingEquiv.toMulEquiv.symm P) =
    coeff n P

Tactic:
simp [Finsupp.equivMapDomain_eq_mapDomain,
      coeff_rename_mapDomain _ (Equiv.optionSubtypeNe i).symm.injective]

Goal state after:
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
hc : (↑(insert a s)).Pairwise (Commute on x)
ih : ∀ (n : ℕ), s.sum x ^ n = ∑ k, ↑(↑↑k).countPerms * (Multiset.map x ↑↑k).noncommProd ⋯
n : ℕ
⊢ ∑ x_1, ∑ i, x a ^ ↑x_1 * (↑(↑↑i).countPerms * (Multiset.map x ↑↑i).noncommProd ⋯) * ↑(n.choose ↑x_1) =
    ∑ k, ↑(↑↑k).countPerms * (Multiset.map x ↑↑k).noncommProd ⋯

Tactic:
sum_sigma',

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 : ℕ
⊢ ∑ x_1 ∈ univ.sigma fun a ↦ univ,
      x a ^ ↑x_1.fst * (↑(↑↑x_1.snd).countPerms * (Multiset.map x ↑↑x_1.snd).noncommProd ⋯) * ↑(n.choose ↑x_1.fst) =
    ∑ 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
⊢ p = q

Tactic:
by
  suffices ∀ p, (∀ x ∈ Set.pi .univ s, eval x p = 0) → p = 0 by
    rw [← sub_eq_zero, this (p - q)]
    intro x hx
    simp_rw [map_sub, h x hx, sub_self]
  intro p h
  obtain ⟨n, f, hf, p, rfl⟩ := exists_fin_rename p
  suffices p = 0 by rw [this, map_zero]
  refine funext_fin (s ∘ f) (fun _ ↦ hs _) fun x hx ↦ ?_
  choose g hg using fun i ↦ (hs i).nonempty
  convert! h (Function.extend f x g) fun i _ ↦ ?_
  · simp only [eval, eval₂Hom_rename, Function.extend_comp hf]
  obtain ⟨i, rfl⟩ | nex := em (∃ x, f x = i)
  · rw [hf.extend_apply]; exact hx _ ⟨⟩
  · simp_rw [Function.extend, dif_neg nex, hg]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : AddCommMonoid α
inst✝ : DecidableEq α
l : List α
⊢ (l.toFinsupp.sum fun x a ↦ a) = l.sum

Tactic:
match l with
  | nil => simp
  | x :: l =>
    simp only [toFinsupp_cons_eq_single_add_embDomain, sum_cons]
    rw [Finsupp.sum_add_index (by simp) (by simp)]
    simp [Finsupp.sum_embDomain, l.toFinsupp_sum]

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

Goal state before:
pp: k n : ℕ
⊢ (k • {n}).multinomial = Nat.multinomial (Finset.range k) fun x ↦ n

Tactic:
by
  simp [multinomial_nsmul]

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

Goal state before:
pp: case a
σ : Type u_1
R : Type u_2
inst✝² : CommSemiring R
f : MvPolynomial σ R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
hf : ¬f = 0
b : σ →₀ ℕ
hb : b ∈ f.support
⊢ (b.sum fun x e ↦ e) ≤ Finsupp.degree (degLex.degree f)

Tactic:
exact DegLex.monotone_degree (degLex.le_degree hb)

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

Goal state before:
pp: case neg
α : Type u_1
σ : Type u_2
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
a b : σ →₀ ℕ
h : a ≤ b
ha : degree b ≤ degree a
⊢ degree a < degree b ∨ degree a = degree b ∧ toLex a ≤ toLex b

Tactic:
refine Or.inr ⟨le_antisymm ?_ ha, toLex_monotone h⟩

Goal state after:
case neg
α : Type u_1
σ : Type u_2
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
a b : σ →₀ ℕ
h : a ≤ b
ha : degree b ≤ degree a
⊢ degree a ≤ degree b
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
⊢ m.toSyn (m.degree (f + g)) ≤ max (m.toSyn (m.degree f)) (m.toSyn (m.degree g))

Tactic:
by
  conv_rhs => rw [← m.toSyn.apply_symm_apply (_ ⊔ _)]
  rw [degree_le_iff]
  simp only [AddEquiv.apply_symm_apply, le_sup_iff]
  intro b hb
  by_cases hf : b ∈ f.support
  · left
    exact m.le_degree hf
  · right
    apply m.le_degree
    simp only [notMem_support_iff] at hf
    simpa only [mem_support_iff, coeff_add, hf, zero_add] using hb

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.FinsuppEquiv

Goal state before:
pp: ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
n : ℕ
⊢ #(s.finsuppAntidiag n) = (#s + n - 1).choose n

Tactic:
by
  simp [card_eq_of_equiv_fintype (finsuppAntidiagEquiv s n), Sym.card_sym_eq_choose]

Goal state after: