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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
inst✝ : IsFiniteMeasure (μ.withDensity g)
hf : Measurable f
hg : Measurable g
t : Set α := {x | f x ≤ g x}
ht : MeasurableSet t
⊢ f - g =ᵐ[μ.restrict t] 0

Tactic:
refine ae_restrict_of_forall_mem ht fun x hx ↦ ?_

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
inst✝ : IsFiniteMeasure (μ.withDensity g)
hf : Measurable f
hg : Measurable g
t : Set α := {x | f x ≤ g x}
ht : MeasurableSet t
x : α
hx : x ∈ t
⊢ (f - g) x = 0 x
Module: Mathlib.MeasureTheory.Order.UpperLower

Goal state before:
pp: case refine_2
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
f : (δ : ℝ) → 0 < δ → ι → ℝ
hf₀ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ closedBall x δ
hf₁ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ interior s
H : Tendsto (fun r ↦ volume (closure s ∩ closedBall x r) / volume (closedBall x r)) (𝓝[>] 0) (𝓝 0)
ε : ℕ → ℝ
hε' : ∀ (n : ℕ), 0 < ε n
hε₀ : Tendsto ε atTop (𝓝[>] 0)
n : ℕ
this : 0 < ε n
⊢ ENNReal.ofReal (4⁻¹ ^ Fintype.card ι) = volume (closedBall (f (ε n) ⋯) (ε n / 4)) / volume (closedBall x (ε n))

Tactic:
rw [Real.volume_pi_closedBall, Real.volume_pi_closedBall, ← ENNReal.ofReal_div_of_pos,
      ← div_pow, mul_div_mul_left _ _ (two_ne_zero' ℝ), div_right_comm, div_self, one_div]

Goal state after:
case refine_2
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
f : (δ : ℝ) → 0 < δ → ι → ℝ
hf₀ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ closedBall x δ
hf₁ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ interior s
H : Tendsto (fun r ↦ volume (closure s ∩ closedBall x r) / volume (closedBall x r)) (𝓝[>] 0) (𝓝 0)
ε : ℕ → ℝ
hε' : ∀ (n : ℕ), 0 < ε n
hε₀ : Tendsto ε atTop (𝓝[>] 0)
n : ℕ
this : 0 < ε n
⊢ ε n ≠ 0

case refine_2
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
f : (δ : ℝ) → 0 < δ → ι → ℝ
hf₀ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ closedBall x δ
hf₁ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ interior s
H : Tendsto (fun r ↦ volume (closure s ∩ closedBall x r) / volume (closedBall x r)) (𝓝[>] 0) (𝓝 0)
ε : ℕ → ℝ
hε' : ∀ (n : ℕ), 0 < ε n
hε₀ : Tendsto ε atTop (𝓝[>] 0)
n : ℕ
this : 0 < ε n
⊢ 0 < (2 * ε n) ^ Fintype.card ι

case refine_2.hr
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
f : (δ : ℝ) → 0 < δ → ι → ℝ
hf₀ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ closedBall x δ
hf₁ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ interior s
H : Tendsto (fun r ↦ volume (closure s ∩ closedBall x r) / volume (closedBall x r)) (𝓝[>] 0) (𝓝 0)
ε : ℕ → ℝ
hε' : ∀ (n : ℕ), 0 < ε n
hε₀ : Tendsto ε atTop (𝓝[>] 0)
n : ℕ
this : 0 < ε n
⊢ 0 ≤ ε n

case refine_2.hr
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
f : (δ : ℝ) → 0 < δ → ι → ℝ
hf₀ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ closedBall x δ
hf₁ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ interior s
H : Tendsto (fun r ↦ volume (closure s ∩ closedBall x r) / volume (closedBall x r)) (𝓝[>] 0) (𝓝 0)
ε : ℕ → ℝ
hε' : ∀ (n : ℕ), 0 < ε n
hε₀ : Tendsto ε atTop (𝓝[>] 0)
n : ℕ
this : 0 < ε n
⊢ 0 ≤ ε n / 4
Module: Mathlib.MeasureTheory.VectorMeasure.Variation.Basic

Goal state before:
pp: X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst✝² : TopologicalSpace V
inst✝¹ : ENormedAddCommMonoid V
inst✝ : T2Space V
μ : VectorMeasure X V
s : Set X
hs : MeasurableSet s
a : ℝ≥0∞
ha : a < preVariationFun (fun x ↦ ‖μ x‖ₑ) s
P : Finpartition ⟨s, hs⟩
hP : a < ∑ p ∈ P.parts, (fun x ↦ ‖μ x‖ₑ) ↑p
i j : Set X
hij : i ≠ j
h'i : MeasurableSet i
i_mem : ⟨i, ⋯⟩ ∈ P.parts
h'j : MeasurableSet j
j_mem : ⟨j, ⋯⟩ ∈ P.parts
⊢ ⟨i, ⋯⟩ ≠ ⟨j, ⋯⟩

Tactic:
by simpa using hij

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.Variation.Basic

Goal state before:
pp: X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst✝² : TopologicalSpace V
inst✝¹ : ENormedAddCommMonoid V
inst✝ : T2Space V
μ : VectorMeasure X V
s : Set X
hs : MeasurableSet s
ε : ℝ≥0∞
hε : 0 < ε
hμ : μ.variation s ≠ ∞
⊢ ∃ P, (∀ t ∈ P, t ⊆ s) ∧ (↑P).PairwiseDisjoint id ∧ (∀ t ∈ P, MeasurableSet t) ∧ μ.variation s ≤ ∑ p ∈ P, ‖μ p‖ₑ + ε

Tactic:
simp only [variation_apply, preVariation, ennrealToMeasure_apply hs, ennrealPreVariation_apply]
    at hμ ⊢

Goal state after:
X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst✝² : TopologicalSpace V
inst✝¹ : ENormedAddCommMonoid V
inst✝ : T2Space V
μ : VectorMeasure X V
s : Set X
hs : MeasurableSet s
ε : ℝ≥0∞
hε : 0 < ε
hμ : preVariationFun (fun x ↦ ‖μ x‖ₑ) s ≠ ∞
⊢ ∃ P,
    (∀ t ∈ P, t ⊆ s) ∧
      (↑P).PairwiseDisjoint id ∧ (∀ t ∈ P, MeasurableSet t) ∧ preVariationFun (fun x ↦ ‖μ x‖ₑ) s ≤ ∑ x ∈ P, ‖μ x‖ₑ + ε
Module: Mathlib.MeasureTheory.VectorMeasure.Variation.Basic

Goal state before:
pp: X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst✝² : TopologicalSpace V
inst✝¹ : ENormedAddCommMonoid V
inst✝ : T2Space V
μ : VectorMeasure X V
s : Set X
hs : MeasurableSet s
ε : ℝ≥0∞
hε : 0 < ε
hμ : preVariationFun (fun x ↦ ‖μ x‖ₑ) s ≠ ∞
P : Finpartition ⟨s, hs⟩
hP : preVariationFun (fun x ↦ ‖μ x‖ₑ) s ≤ ∑ p ∈ P.parts, (fun x ↦ ‖μ x‖ₑ) ↑p + ε
i j : Set X
hij : i ≠ j
h'i : MeasurableSet i
i_mem : ⟨i, ⋯⟩ ∈ P.parts
h'j : MeasurableSet j
j_mem : ⟨j, ⋯⟩ ∈ P.parts
⊢ ⟨i, ⋯⟩ ≠ ⟨j, ⋯⟩

Tactic:
by simpa using hij

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.Variation.Basic

Goal state before:
pp: X : Type u_1
mX : MeasurableSpace X
μ : SignedMeasure X
s : Set X
hs : MeasurableSet s
a : ℝ≥0∞
ha : a < (variation μ) s
⊢ ∃ t ⊆ s, MeasurableSet t ∧ a < 2 * ‖μ t‖ₑ

Tactic:
obtain ⟨P, Ps, P_disj, P_meas, hP⟩ : ∃ (P : Finset (Set X)), (∀ t ∈ P, t ⊆ s) ∧
    ((P : Set (Set X)).PairwiseDisjoint id) ∧
    (∀ t ∈ P, MeasurableSet t) ∧ a < ∑ p ∈ P, ‖μ p‖ₑ := exists_lt_sum_of_lt_variation _ hs ha
  have I : (∑ p ∈ P.filter (fun p ↦ 0 ≤ μ p), ‖μ p‖ₑ) =
      ‖μ (⋃ p ∈ P.filter (fun p ↦ 0 ≤ μ p), p)‖ₑ := by
    simp only [Real.norm_eq_abs, enorm_eq_nnnorm,
      ← ENNReal.ofNNReal_finsetSum, ENNReal.coe_inj, ← NNReal.coe_inj,
      NNReal.coe_sum, coe_nnnorm, Real.norm_eq_abs]
    have A : ∑ x ∈ P with 0 ≤ μ x, |μ x| = μ (⋃ x ∈ P.filter (fun x ↦ 0 ≤ μ x), x) := calc
      _ = ∑ x ∈ P with 0 ≤ μ x, μ x := by
        apply Finset.sum_congr rfl (fun p hp ↦ ?_)
        simp only [Finset.mem_filter] at hp
        simp [hp]
      _ = μ (⋃ x ∈ P.filter (fun x ↦ 0 ≤ μ x), x) := by
        rw [of_biUnion_finset]
        · apply P_disj.subset (by grind)
        · grind
    rw [A, abs_of_nonneg]
    rw [← A]
    exact Finset.sum_nonneg (fun p hp ↦ by positivity)
  have J : (∑ p ∈ P.filter (fun p ↦ ¬ 0 ≤ μ p), ‖μ p‖ₑ) =
      ‖μ (⋃ p ∈ P.filter (fun p ↦ ¬ 0 ≤ μ p), p)‖ₑ := by
    simp only [not_le, enorm_eq_nnnorm, ← ENNReal.ofNNReal_finsetSum,
      ENNReal.coe_inj, ← NNReal.coe_inj, NNReal.coe_sum, coe_nnnorm, Real.norm_eq_abs]
    have A : ∑ x ∈ P with μ x < 0, |μ x| = - μ (⋃ x ∈ P.filter (fun x ↦ μ x < 0), x) := calc
      ∑ x ∈ P with μ x < 0, |μ x|
      _ = ∑ x ∈ P with μ x < 0, -μ x := by
        refine Finset.sum_congr rfl (fun p hp ↦ ?_)
        simp only [Finset.mem_filter] at hp
        simp [hp.2.le]
      _ = -μ (⋃ x ∈ P.filter (fun x ↦ μ x < 0), x) := by
        rw [of_biUnion_finset]
        · simp
        · apply P_disj.subset (by grind)
        · grind
    rw [A, abs_of_nonpos]
    rw [← neg_nonneg, ← A]
    exact Finset.sum_nonneg (fun p hp ↦ by positivity)
  simp_rw [two_mul]
  rw [← Finset.sum_filter_add_sum_filter_not _ (fun p ↦ 0 ≤ μ p), I, J] at hP
  rcases le_total (‖μ (⋃ p ∈ P.filter (fun p ↦ ¬ 0 ≤ μ p), p)‖ₑ)
    (‖μ (⋃ p ∈ P.filter (fun p ↦ 0 ≤ μ p), p)‖ₑ) with h | h
  · refine ⟨⋃ p ∈ P.filter (fun p ↦ 0 ≤ μ p), p, ?_, ?_, ?_⟩
    · simp; grind
    · exact Finset.measurableSet_biUnion _ (by grind)
    · exact hP.trans_le (by gcongr)
  · refine ⟨⋃ p ∈ P.filter (fun p ↦ ¬ 0 ≤ μ p), p, ?_, ?_, ?_⟩
    · simp; grind
    · exact Finset.measurableSet_biUnion _ (by grind)
    · exact hP.trans_le (by gcongr)

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.BoundedVariation

Goal state before:
pp: α : Type u_1
inst✝⁸ : LinearOrder α
inst✝⁷ : DenselyOrdered α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : OrderTopology α
inst✝⁴ : SecondCountableTopology α
inst✝³ : CompactIccSpace α
hα : MeasurableSpace α
inst✝² : BorelSpace α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
f : α → E
a : α
hf : BoundedVariationOn f univ
ha : ¬IsBot a
b : α
hb : b < a
u : ℕ → α
u_mono : StrictMono u
u_lim : Tendsto u atTop (𝓝 a)
u_lt_a : ∀ (n : ℕ), u n < a
A : {a} = ⋂ n, Ioc (u n) a
⊢ Tendsto (fun n ↦ hf.vectorMeasure (Ioc (u n) a)) atTop (𝓝 (hf.vectorMeasure {a}))

Tactic:
rw [A]

Goal state after:
α : Type u_1
inst✝⁸ : LinearOrder α
inst✝⁷ : DenselyOrdered α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : OrderTopology α
inst✝⁴ : SecondCountableTopology α
inst✝³ : CompactIccSpace α
hα : MeasurableSpace α
inst✝² : BorelSpace α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
f : α → E
a : α
hf : BoundedVariationOn f univ
ha : ¬IsBot a
b : α
hb : b < a
u : ℕ → α
u_mono : StrictMono u
u_lim : Tendsto u atTop (𝓝 a)
u_lt_a : ∀ (n : ℕ), u n < a
A : {a} = ⋂ n, Ioc (u n) a
⊢ Tendsto (fun n ↦ hf.vectorMeasure (Ioc (u n) a)) atTop (𝓝 (hf.vectorMeasure (⋂ n, Ioc (u n) a)))
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.JordanSub

Goal state before:
pp: X : Type u_1
mX : MeasurableSpace X
s : Set X
μ ν : Measure X
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hs : IsHahnDecomposition μ ν s
hmeas : MeasurableSet s
⊢ ((ν - μ).restrict s).toSignedMeasure =
    VectorMeasure.restrict ν.toSignedMeasure s - VectorMeasure.restrict μ.toSignedMeasure s

Tactic:
rw [eq_sub_iff_add_eq, toSignedMeasure_restrict_eq_restrict_toSignedMeasure _ _ hmeas,
    ← toSignedMeasure_add]

Goal state after:
X : Type u_1
mX : MeasurableSpace X
s : Set X
μ ν : Measure X
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hs : IsHahnDecomposition μ ν s
hmeas : MeasurableSet s
⊢ ((ν - μ).restrict s + μ.restrict s).toSignedMeasure = VectorMeasure.restrict ν.toSignedMeasure s
Module: Mathlib.MeasureTheory.VectorMeasure.Variation.Semivariation

Goal state before:
pp: X : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
mX : MeasurableSpace X
μ : VectorMeasure X E
s : Set X
hs : MeasurableSet s
h's : μ.semivariation s = ∞
t : Set X
ts : t ⊆ s
t_meas : MeasurableSet t
ht : 2 * ‖μ s‖ₑ + 2 < 2 * ‖μ t‖ₑ
h't : 1 + ‖μ s‖ₑ ≤ ‖μ t‖ₑ
hI : μ.semivariation t = ∞
⊢ μ t = μ s - μ (s \ t)

Tactic:
← of_add_of_sdiff t_meas hs ts

Goal state after:
X : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
mX : MeasurableSpace X
μ : VectorMeasure X E
s : Set X
hs : MeasurableSet s
h's : μ.semivariation s = ∞
t : Set X
ts : t ⊆ s
t_meas : MeasurableSet t
ht : 2 * ‖μ s‖ₑ + 2 < 2 * ‖μ t‖ₑ
h't : 1 + ‖μ s‖ₑ ≤ ‖μ t‖ₑ
hI : μ.semivariation t = ∞
⊢ μ t = μ t + μ (s \ t) - μ (s \ t)
Module: Mathlib.MeasureTheory.VectorMeasure.AddContent

Goal state before:
pp: case refine_2
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
μ : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
m : AddContent E C
hC : IsSetRing C
hCmeas : ∀ s ∈ C, MeasurableSet s
hm : ∀ s ∈ C, ‖m s‖ₑ ≤ μ s
h'C : ∀ (t : Set α) (ε : ℝ≥0∞), MeasurableSet t → 0 < ε → ∃ s ∈ C, μ (s ∆ t) < ε
C' : Set (MeasuredSets μ) := {s | ∃ c ∈ C, ↑s = c}
C'C : ∀ s ∈ C', ↑s ∈ C
C'_dense : Dense C'
m₀ : ↑C' → E := fun x ↦ m ↑↑x
lip : LipschitzWith 1 m₀
m₁ : MeasuredSets μ → E := C'_dense.extend m₀
m₁_lip : LipschitzWith 1 m₁
hBound : ∀ (s : MeasuredSets μ), ‖m₁ s‖ₑ ≤ μ ↑s
hAddit : ∀ (s t : MeasuredSets μ), Disjoint ↑s ↑t → m₁ ⟨↑s ∪ ↑t, ⋯⟩ = m₁ s + m₁ t
m' : Set α → E := fun s ↦ if hs : MeasurableSet s then m₁ ⟨s, hs⟩ else 0
m'' : VectorMeasure α E := of_additive_of_le_measure m' ⋯ ⋯ ⋯
s : Set α
⊢ ‖m'' s‖ₑ ≤ μ s

Tactic:
change ‖m' s‖ₑ ≤ μ s

Goal state after:
case refine_2
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
μ : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
m : AddContent E C
hC : IsSetRing C
hCmeas : ∀ s ∈ C, MeasurableSet s
hm : ∀ s ∈ C, ‖m s‖ₑ ≤ μ s
h'C : ∀ (t : Set α) (ε : ℝ≥0∞), MeasurableSet t → 0 < ε → ∃ s ∈ C, μ (s ∆ t) < ε
C' : Set (MeasuredSets μ) := {s | ∃ c ∈ C, ↑s = c}
C'C : ∀ s ∈ C', ↑s ∈ C
C'_dense : Dense C'
m₀ : ↑C' → E := fun x ↦ m ↑↑x
lip : LipschitzWith 1 m₀
m₁ : MeasuredSets μ → E := C'_dense.extend m₀
m₁_lip : LipschitzWith 1 m₁
hBound : ∀ (s : MeasuredSets μ), ‖m₁ s‖ₑ ≤ μ ↑s
hAddit : ∀ (s t : MeasuredSets μ), Disjoint ↑s ↑t → m₁ ⟨↑s ∪ ↑t, ⋯⟩ = m₁ s + m₁ t
m' : Set α → E := fun s ↦ if hs : MeasurableSet s then m₁ ⟨s, hs⟩ else 0
m'' : VectorMeasure α E := of_additive_of_le_measure m' ⋯ ⋯ ⋯
s : Set α
⊢ ‖m' s‖ₑ ≤ μ s
Module: Mathlib.MeasureTheory.VectorMeasure.AddContent

Goal state before:
pp: case neg
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
μ : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
m : AddContent E C
hC : IsSetSemiring C
hm : ∀ s ∈ C, ‖m s‖ₑ ≤ μ s
h'C : ∀ s ∈ C, MeasurableSet s
M : MeasurableSpace α := generateFrom C
Mle : M ≤ hα
μ' : Measure α := μ.trim Mle
hμ' : μ' = μ.trim Mle
m' : VectorMeasure α E
m'C : ∀ s ∈ C, m' s = m s
hm' : ∀ (s : Set α), ‖m' s‖ₑ ≤ μ' s
m'_le : m'.variation ≤ μ'
this : MeasurableSpace α := hα
m'' : VectorMeasure α E :=
  { measureOf' := fun s ↦ if MeasurableSet s then ∫ᵛ (x : α), μ[s.indicator 1 | M] x ∂•m' else 0, empty' := ⋯,
    not_measurable' := ⋯, m_iUnion' := ⋯ }
s : Set α
hs : ¬MeasurableSet s
⊢ ‖m'' s‖ₑ ≤ μ s

pp: case pos
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
μ : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
m : AddContent E C
hC : IsSetSemiring C
hm : ∀ s ∈ C, ‖m s‖ₑ ≤ μ s
h'C : ∀ s ∈ C, MeasurableSet s
M : MeasurableSpace α := generateFrom C
Mle : M ≤ hα
μ' : Measure α := μ.trim Mle
hμ' : μ' = μ.trim Mle
m' : VectorMeasure α E
m'C : ∀ s ∈ C, m' s = m s
hm' : ∀ (s : Set α), ‖m' s‖ₑ ≤ μ' s
m'_le : m'.variation ≤ μ'
this : MeasurableSpace α := hα
m'' : VectorMeasure α E :=
  { measureOf' := fun s ↦ if MeasurableSet s then ∫ᵛ (x : α), μ[s.indicator 1 | M] x ∂•m' else 0, empty' := ⋯,
    not_measurable' := ⋯, m_iUnion' := ⋯ }
s : Set α
hs : MeasurableSet s
⊢ ‖m'' s‖ₑ ≤ μ s

Tactic:
· simp [not_measurable _ hs]

Goal state after:
case pos
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
μ : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
m : AddContent E C
hC : IsSetSemiring C
hm : ∀ s ∈ C, ‖m s‖ₑ ≤ μ s
h'C : ∀ s ∈ C, MeasurableSet s
M : MeasurableSpace α := generateFrom C
Mle : M ≤ hα
μ' : Measure α := μ.trim Mle
hμ' : μ' = μ.trim Mle
m' : VectorMeasure α E
m'C : ∀ s ∈ C, m' s = m s
hm' : ∀ (s : Set α), ‖m' s‖ₑ ≤ μ' s
m'_le : m'.variation ≤ μ'
this : MeasurableSpace α := hα
m'' : VectorMeasure α E :=
  { measureOf' := fun s ↦ if MeasurableSet s then ∫ᵛ (x : α), μ[s.indicator 1 | M] x ∂•m' else 0, empty' := ⋯,
    not_measurable' := ⋯, m_iUnion' := ⋯ }
s : Set α
hs : MeasurableSet s
⊢ ‖m'' s‖ₑ ≤ μ s
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: M : Type u_1
inst✝⁴ : AddCommMonoid M
inst✝³ : PartialOrder M
inst✝² : WellQuasiOrderedLE M
inst✝¹ : IsOrderedCancelAddMonoid M
inst✝ : CanonicallyOrderedAdd M
s : Set M
hs : IsSlice s
hs' : s.Nonempty
x : M
hx : x ∈ s
⊢ ∀ {a b : M}, a ∈ {y | x + y ∈ s} → b ∈ {y | x + y ∈ s} → a + b ∈ {y | x + y ∈ s}

Tactic:
intro a b ha hb
          simp only [mem_ofPred_eq] at *
          rw [← add_assoc]
          exact hs _ hx _ _ ha hb

Goal state after:
Module: Mathlib.ModelTheory.Equivalence

Goal state before:
pp: L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ : L.BoundedFormula α n
h : φ ⇔[T] ψ
M : T.ModelType
v : α → ↑M
xs : Fin n → ↑M
⊢ φ.Realize v xs ↔ ψ.Realize v xs

Tactic:
← BoundedFormula.realize_iff

Goal state after:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ : L.BoundedFormula α n
h : φ ⇔[T] ψ
M : T.ModelType
v : α → ↑M
xs : Fin n → ↑M
⊢ (φ ⇔ ψ).Realize v xs
Module: Mathlib.ModelTheory.FinitelyGenerated

Goal state before:
pp: case refine_1
L : Language
M : Type u_1
inst✝ : L.Structure M
S : L.Substructure M
h : S.FG
⊢ (map S.subtype.toHom ⊤).FG

Tactic:
rw [← Hom.range_eq_map, range_subtype]
    exact h

Goal state after:
Module: Mathlib.ModelTheory.FinitelyGenerated

Goal state before:
pp: case refine_1
L : Language
M : Type u_1
inst✝ : L.Structure M
S : L.Substructure M
h : S.CG
⊢ (map S.subtype.toHom ⊤).CG

Tactic:
rw [← Hom.range_eq_map, range_subtype]
    exact h

Goal state after:
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
s : Set M
⊢ IsLinearSet s ↔ ∃ a n f, s = a +ᵥ range ⇑f

Tactic:
simp_rw [isLinearSet_iff_exists_fg_eq_vadd, fg_iff_exists_fin_addMonoidHom,
    ← AddMonoidHom.coe_mrange]

Goal state after:
M : Type u_1
inst✝ : AddCommMonoid M
s : Set M
⊢ (∃ a P, (∃ n f, AddMonoidHom.mrange f = P) ∧ s = a +ᵥ ↑P) ↔ ∃ a n f, s = a +ᵥ ↑(AddMonoidHom.mrange f)
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
i : ↑hs.basisSet
x✝ : i ∈ Finset.univ
⊢ ↑⌊(hs.basis.repr (toRatVec x - toRatVec hs.base)) i⌋ • toRatVec ↑i ≤
    (hs.basis.repr (toRatVec x - toRatVec hs.base)) i • hs.basis i

Tactic:
rw [basis_apply]

Goal state after:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
i : ↑hs.basisSet
x✝ : i ∈ Finset.univ
⊢ ↑⌊(hs.basis.repr (toRatVec x - toRatVec hs.base)) i⌋ • toRatVec ↑i ≤
    (hs.basis.repr (toRatVec x - toRatVec hs.base)) i • toRatVec ↑i
Module: Mathlib.ModelTheory.DirectLimit

Goal state before:
pp: L : Language
ι : Type v
inst✝⁵ : Preorder ι
G : ι → Type w
inst✝⁴ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝³ : IsDirectedOrder ι
inst✝² : DirectedSystem G fun i j h ↦ ⇑(f i j h)
inst✝¹ : Nonempty ι
P : Type u₁
inst✝ : L.Structure P
g : (i : ι) → G i ↪[L] P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x
n✝ : ℕ
R : L.Relations n✝
x : Fin n✝ → DirectLimit G f
⊢ RelMap R (Quotient.lift (fun x ↦ (g x.fst) x.snd) ⋯ ∘ x) ↔ RelMap R x

Tactic:
by
    obtain ⟨i, y, rfl⟩ := exists_quotient_mk'_sigma_mk'_eq G f x
    change RelMap R (Quotient.lift _ _ ∘ Quotient.mk _ ∘ Structure.Sigma.mk f i ∘ y) ↔ _
    rw [relMap_quotient_mk'_sigma_mk' G f, ← (g i).map_rel R y, ← Function.comp_assoc,
      Quotient.lift_comp_mk]
    rfl

Goal state after:
Module: Mathlib.Order.CountableDenseLinearOrder

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
f : PartialIso α β
a : α
⊢ ∃ b, ∀ p ∈ ↑f, cmp p.1 a = cmp p.2 b

Tactic:
by_cases h : ∃ b, (a, b) ∈ f.val

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
f : PartialIso α β
a : α
h : ∃ b, (a, b) ∈ ↑f
⊢ ∃ b, ∀ p ∈ ↑f, cmp p.1 a = cmp p.2 b

case neg
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
f : PartialIso α β
a : α
h : ¬∃ b, (a, b) ∈ ↑f
⊢ ∃ b, ∀ p ∈ ↑f, cmp p.1 a = cmp p.2 b
Module: Mathlib.ModelTheory.Fraisse

Goal state before:
pp: case refine_2.succ
L : Language
K : Set (Bundled L.Structure)
hn : K.Nonempty
hc : (Quotient.mk' '' K).Countable
fg : ∀ M ∈ K, Structure.FG L ↑M
hp : Hereditary K
jep : JointEmbedding K
F : ℕ → Quotient equivSetoid
hF : ∀ (a : Bundled L.Structure), (∃ x ∈ K, (Quotient.mk' x).out ≈ a) ↔ ∃ y, (F y).out ≈ a
hF' : ∀ (n : ℕ), (F n).out ∈ K
P : ↑K → ℕ → Bundled L.Structure
hPK : ∀ (N : ↑K) (n : ℕ), P N n ∈ K
hP : ∀ (N : ↑K) (n : ℕ), (fun M N ↦ Nonempty (↑M ↪[L] ↑N)) (↑N) (P N n)
hFP : ∀ (N : ↑K) (n : ℕ), (fun M N ↦ Nonempty (↑M ↪[L] ↑N)) (F (n + 1)).out (P N n)
G : ℕ → ↑K := Nat.rec ⟨(F 0).out, ⋯⟩ fun n N ↦ ⟨P N n, ⋯⟩
f : (i j : ℕ) → i ≤ j → ↑↑(G i) ↪[L] ↑↑(G j) := DirectedSystem.natLERec fun n ↦ Nonempty.some ⋯
N : Bundled L.Structure
KN : N ∈ K
this : (Quotient.mk' N).out ≈ N
n : ℕ
e : ↑(F (n + 1)).out ≃[L] ↑N
⊢ ↑(F (n + 1)).out ↪[L] ↑(P (Nat.rec ⟨(F 0).out, ⋯⟩ (fun n N ↦ ⟨P N n, ⋯⟩) n) n)

Tactic:
exact (hFP _ n).some

Goal state after:
Module: Mathlib.NumberTheory.ADEInequality

Goal state before:
pp: case inr.inl
pqr : Multiset ℕ+
n : ℕ+
H : D' n = pqr
⊢ 1 < sumInv pqr

pp: case inr.inr.inl
pqr : Multiset ℕ+
H : E' 3 = pqr
⊢ 1 < sumInv pqr

pp: case inr.inr.inr.inl
pqr : Multiset ℕ+
H : E' 4 = pqr
⊢ 1 < sumInv pqr

pp: case inr.inr.inr.inr
pqr : Multiset ℕ+
H : E' 5 = pqr
⊢ 1 < sumInv pqr

Tactic:
· rw [← H, D', sumInv_pqr]
    norm_num

Goal state after:
case inr.inr.inl
pqr : Multiset ℕ+
H : E' 3 = pqr
⊢ 1 < sumInv pqr

case inr.inr.inr.inl
pqr : Multiset ℕ+
H : E' 4 = pqr
⊢ 1 < sumInv pqr

case inr.inr.inr.inr
pqr : Multiset ℕ+
H : E' 5 = pqr
⊢ 1 < sumInv pqr
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: n : ℕ
⊢ eval 1 (bernoulli n) = bernoulli' n

Tactic:
by
  simp only [bernoulli, eval_finsetSum]
  simp only [← succ_eq_add_one, sum_range_succ, mul_one, cast_one, choose_self,
    (_root_.bernoulli _).mul_comm, sum_bernoulli, one_pow, mul_one, eval_monomial, one_mul]
  by_cases h : n = 1
  · norm_num [h]
  · simp [h, bernoulli_eq_bernoulli'_of_ne_one h]

Goal state after:
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: ⊢ bernoulli' 0 * ↑(Nat.choose 3 0) * (1 / 4) ^ (3 - 0) + -1 / 2 * ↑(Nat.choose 3 1) * (1 / 4) ^ (3 - 1) +
        _root_.bernoulli 2 * ↑(Nat.choose 3 2) * (1 / 4) ^ (3 - 2) +
      _root_.bernoulli 3 * ↑(Nat.choose 3 3) * (1 / 4) ^ (3 - 3) =
    3 / 64

Tactic:
bernoulli'_zero,

Goal state after:
⊢ 1 * ↑(Nat.choose 3 0) * (1 / 4) ^ (3 - 0) + -1 / 2 * ↑(Nat.choose 3 1) * (1 / 4) ^ (3 - 1) +
        _root_.bernoulli 2 * ↑(Nat.choose 3 2) * (1 / 4) ^ (3 - 2) +
      _root_.bernoulli 3 * ↑(Nat.choose 3 3) * (1 / 4) ^ (3 - 3) =
    3 / 64
Module: Mathlib.NumberTheory.Bertrand

Goal state before:
pp: case h₁.refine_2
n : ℕ
n_large : 2 < n
no_prime : ∀ (p : ℕ), Nat.Prime p → n < p → 2 * n < p
n_pos : 0 < n
n2_pos : 1 ≤ 2 * n
S : Finset ℕ := {p ∈ Finset.range (2 * n / 3 + 1) | Nat.Prime p}
f : ℕ → ℕ := fun x ↦ x ^ n.centralBinom.factorization x
this : ∏ x ∈ S, f x = ∏ x ∈ Finset.range (2 * n / 3 + 1), f x
⊢ ∏ i ∈ S with i ≤ (2 * n).sqrt, 2 * n ≤ (2 * n) ^ (2 * n).sqrt

Tactic:
have : (Finset.Icc 1 (sqrt (2 * n))).card = sqrt (2 * n) := by rw [card_Icc, Nat.add_sub_cancel]

Goal state after:
case h₁.refine_2
n : ℕ
n_large : 2 < n
no_prime : ∀ (p : ℕ), Nat.Prime p → n < p → 2 * n < p
n_pos : 0 < n
n2_pos : 1 ≤ 2 * n
S : Finset ℕ := {p ∈ Finset.range (2 * n / 3 + 1) | Nat.Prime p}
f : ℕ → ℕ := fun x ↦ x ^ n.centralBinom.factorization x
this✝ : ∏ x ∈ S, f x = ∏ x ∈ Finset.range (2 * n / 3 + 1), f x
this : (Finset.Icc 1 (2 * n).sqrt).card = (2 * n).sqrt
⊢ ∏ i ∈ S with i ≤ (2 * n).sqrt, 2 * n ≤ (2 * n) ^ (2 * n).sqrt
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: p M N : ℕ
inst✝ : Fact (Nat.Prime p)
hM : M ≠ 0
e : ℕ := M.factorization p
hv : e ≤ N
M' : ℕ := M / p ^ e
hM'_cop : M'.Coprime p
⊢ pIntegral p (↑p ^ N / ↑M)

Tactic:
have hp_ne : (p : ℚ) ≠ 0 := Nat.cast_ne_zero.mpr (Nat.Prime.ne_zero Fact.out)

Goal state after:
p M N : ℕ
inst✝ : Fact (Nat.Prime p)
hM : M ≠ 0
e : ℕ := M.factorization p
hv : e ≤ N
M' : ℕ := M / p ^ e
hM'_cop : M'.Coprime p
hp_ne : ↑p ≠ 0
⊢ pIntegral p (↑p ^ N / ↑M)
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: p d : ℕ
inst✝ : Fact (Nat.Prime p)
hd : d ≥ 2
hcase : ¬(p = 2 ∧ d = 2)
hp2 : 2 ≤ p
n m : ℕ
hm : Nat.le 2 m
IH : ¬(p = 2 ∧ m = 2) → m + 1 ≤ p ^ (m - 1)
hne' : ¬(p = 2 ∧ m.succ = 2)
hm2 : ¬(p = 2 ∧ m = 2)
⊢ p ^ (m - 1) * p = p ^ m

Tactic:
rw [show m = m - 1 + 1 by lia]; exact pow_succ ..

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
x✝¹ : ℕ
x✝ : x✝¹ ∈ {p ∈ Ioc 0 ⌊x⌋₊ | Nat.Prime p}
⊢ 1 ≤ ↑x✝¹

Tactic:
by aesop

Goal state after: