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

Goal state before:
pp: case refine_3
ι : Type u_1
κ : Type u_2
X : ι → Type u_5
Y : κ → Type u_6
mX : (i : ι) → MeasurableSpace (X i)
inst✝⁸ : (i : ι) → TopologicalSpace (X i)
inst✝⁷ : ∀ (i : ι), BorelSpace (X i)
inst✝⁶ : ∀ (i : ι), HasOuterApproxClosed (X i)
mY : (j : κ) → MeasurableSpace (Y j)
inst✝⁵ : (j : κ) → TopologicalSpace (Y j)
inst✝⁴ : ∀ (j : κ), BorelSpace (Y j)
inst✝³ : ∀ (j : κ), HasOuterApproxClosed (Y j)
inst✝² : Fintype ι
inst✝¹ : Fintype κ
μ ν : Measure (((i : ι) → X i) × ((j : κ) → Y j))
inst✝ : IsFiniteMeasure μ
h :
  ∀ (f : (i : ι) → X i →ᵇ ℝ≥0) (g : (j : κ) → Y j →ᵇ ℝ≥0),
    ∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)), ↑(∏ i, (f i) (p.1 i)) * ↑(∏ j, (g j) (p.2 j)) ∂μ =
      ∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)), ↑(∏ i, (f i) (p.1 i)) * ↑(∏ j, (g j) (p.2 j)) ∂ν
hμν : μ univ = ν univ
this : IsFiniteMeasure ν
π : Set (Set (((i : ι) → X i) × ((j : κ) → Y j))) :=
  image2 (fun s t ↦ s ×ˢ t) (univ.pi '' univ.pi fun x ↦ {s | IsClosed[inst✝⁸ x] s})
    (univ.pi '' univ.pi fun x ↦ {t | IsClosed[inst✝⁵ x] t})
s₁ : (i : ι) → Set (X i)
hs₁ : s₁ ∈ univ.pi fun x ↦ {s | IsClosed[inst✝⁸ x] s}
t₁ : (i : κ) → Set (Y i)
ht₁ : t₁ ∈ univ.pi fun x ↦ {t | IsClosed[inst✝⁵ x] t}
s₂ : (i : ι) → Set (X i)
hs₂ : s₂ ∈ univ.pi fun x ↦ {s | IsClosed[inst✝⁸ x] s}
t₂ : (i : κ) → Set (Y i)
ht₂ : t₂ ∈ univ.pi fun x ↦ {t | IsClosed[inst✝⁵ x] t}
⊢ (fun s t ↦ s ×ˢ t) (univ.pi fun i ↦ s₁ i ∩ s₂ i) (univ.pi fun j ↦ t₁ j ∩ t₂ j) =
    (fun s t ↦ s ×ˢ t) (univ.pi s₁) (univ.pi t₁) ∩ (fun s t ↦ s ×ˢ t) (univ.pi s₂) (univ.pi t₂)

Tactic:
simp [Set.pi_inter_distrib, Set.prod_inter_prod]

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

Goal state before:
pp: ι : Type u_1
inst✝¹ : Nonempty ι
inst✝ : Fintype ι
x : EuclideanSpace ℝ ι
r : ℝ
hr : 0 ≤ r
this : volume (Metric.ball 0 1) = ENNReal.ofReal (√π ^ card ι / Gamma (↑(card ι) / 2 + 1))
⊢ volume (Metric.ball x r) = ENNReal.ofReal r ^ card ι * ENNReal.ofReal (√π ^ card ι / Gamma (↑(card ι) / 2 + 1))

Tactic:
by
      rw [Measure.addHaar_ball _ _ hr, this, ofReal_pow hr, finrank_euclideanSpace]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.TightNormed

Goal state before:
pp: case h
E : Type u_1
mE : MeasurableSpace E
S : Set (Measure E)
inst✝⁴ : NormedAddCommGroup E
𝕜 : Type u_2
ι : Type u_3
inst✝³ : RCLike 𝕜
inst✝² : Fintype ι
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
b : OrthonormalBasis ι 𝕜 E
h : ∀ (i : ι), Tendsto (fun r ↦ ⨆ μ ∈ S, μ {x | r < ‖⟪b i, x⟫_𝕜‖}) atTop (𝓝 0)
hE : Nontrivial E
h_rank : 0 < ↑(Fintype.card ι)
this✝ : Nonempty ι
this : ProperSpace E
r : ℝ
μ : Measure E
hμS : μ ∈ S
i : ι
a✝ : i ∈ Finset.univ
⊢ μ {x | r / √↑(Fintype.card ι) < ‖⟪b i, x⟫_𝕜‖} ≤ ⨆ μ ∈ S, μ {x | r / √↑(Fintype.card ι) < ‖⟪b i, x⟫_𝕜‖}

Tactic:
exact le_biSup (fun μ ↦ μ {x | r / √(Fintype.card ι) < ‖⟪b i, x⟫_𝕜‖}) hμS

Goal state after:
Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd

Goal state before:
pp: ι : Type u_1
T : Type u_4
X : ι → Type u_5
mX : (i : ι) → MeasurableSpace (X i)
inst✝⁸ : (i : ι) → TopologicalSpace (X i)
inst✝⁷ : ∀ (i : ι), BorelSpace (X i)
inst✝⁶ : ∀ (i : ι), HasOuterApproxClosed (X i)
mT : MeasurableSpace T
inst✝⁵ : TopologicalSpace T
inst✝⁴ : BorelSpace T
inst✝³ : HasOuterApproxClosed T
inst✝² : Fintype ι
μ ν : Measure (((i : ι) → X i) × T)
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h :
  ∀ (f : (i : ι) → X i →ᵇ ℝ) (g : T →ᵇ ℝ),
    ∫ (p : ((i : ι) → X i) × T), (∏ i, (f i) (p.1 i)) * g p.2 ∂μ =
      ∫ (p : ((i : ι) → X i) × T), (∏ i, (f i) (p.1 i)) * g p.2 ∂ν
e : ((i : ι) → X i) × T ≃ᵐ ((i : ι) → X i) × (Unit → T) :=
  { toFun := fun p ↦ (fun i ↦ p.1 i, fun x ↦ p.2), invFun := fun p ↦ (fun i ↦ p.1 i, p.2 ()), left_inv := ⋯,
    right_inv := ⋯, measurable_toFun := ⋯, measurable_invFun := ⋯ }
f : (i : ι) → X i →ᵇ ℝ
g : Unit → T →ᵇ ℝ
⊢ ∫ (p : ((i : ι) → X i) × (Unit → T)), (∏ i, (f i) (p.1 i)) * ∏ j, (g j) (p.2 j) ∂Measure.map (⇑e) μ =
    ∫ (p : ((i : ι) → X i) × (Unit → T)), (∏ i, (f i) (p.1 i)) * ∏ j, (g j) (p.2 j) ∂Measure.map (⇑e) ν

Tactic:
integral_map_equiv,

Goal state after:
ι : Type u_1
T : Type u_4
X : ι → Type u_5
mX : (i : ι) → MeasurableSpace (X i)
inst✝⁸ : (i : ι) → TopologicalSpace (X i)
inst✝⁷ : ∀ (i : ι), BorelSpace (X i)
inst✝⁶ : ∀ (i : ι), HasOuterApproxClosed (X i)
mT : MeasurableSpace T
inst✝⁵ : TopologicalSpace T
inst✝⁴ : BorelSpace T
inst✝³ : HasOuterApproxClosed T
inst✝² : Fintype ι
μ ν : Measure (((i : ι) → X i) × T)
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h :
  ∀ (f : (i : ι) → X i →ᵇ ℝ) (g : T →ᵇ ℝ),
    ∫ (p : ((i : ι) → X i) × T), (∏ i, (f i) (p.1 i)) * g p.2 ∂μ =
      ∫ (p : ((i : ι) → X i) × T), (∏ i, (f i) (p.1 i)) * g p.2 ∂ν
e : ((i : ι) → X i) × T ≃ᵐ ((i : ι) → X i) × (Unit → T) :=
  { toFun := fun p ↦ (fun i ↦ p.1 i, fun x ↦ p.2), invFun := fun p ↦ (fun i ↦ p.1 i, p.2 ()), left_inv := ⋯,
    right_inv := ⋯, measurable_toFun := ⋯, measurable_invFun := ⋯ }
f : (i : ι) → X i →ᵇ ℝ
g : Unit → T →ᵇ ℝ
⊢ ∫ (x : ((i : ι) → X i) × T), (∏ i, (f i) ((e x).1 i)) * ∏ j, (g j) ((e x).2 j) ∂μ =
    ∫ (p : ((i : ι) → X i) × (Unit → T)), (∏ i, (f i) (p.1 i)) * ∏ j, (g j) (p.2 j) ∂Measure.map (⇑e) ν
Module: Mathlib.MeasureTheory.Measure.PreVariation

Goal state before:
pp: X : Type u_1
inst✝ : MeasurableSpace X
f : Set X → ℝ≥0∞
s : Set X
hs : MeasurableSet s
ε : ℝ≥0
hε : 0 < ε
h : preVariationFun f s ≠ ∞
ε' : ℝ≥0 := min ε (preVariationFun f s).toNNReal
hε' : ↑ε' ≤ preVariationFun f s
this : ε' ≤ ε
hw : preVariationFun f s ≠ 0
⊢ 0 < ε ∧ 0 < (preVariationFun f s).toNNReal

Tactic:
exact ⟨hε, toNNReal_pos hw h⟩

Goal state after:
Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd

Goal state before:
pp: κ : Type u_2
Z : Type u_3
Y : κ → Type u_6
mY : (j : κ) → MeasurableSpace (Y j)
inst✝⁸ : (j : κ) → TopologicalSpace (Y j)
inst✝⁷ : ∀ (j : κ), BorelSpace (Y j)
inst✝⁶ : ∀ (j : κ), HasOuterApproxClosed (Y j)
mZ : MeasurableSpace Z
inst✝⁵ : TopologicalSpace Z
inst✝⁴ : BorelSpace Z
inst✝³ : HasOuterApproxClosed Z
inst✝² : Fintype κ
μ ν : Measure (Z × ((j : κ) → Y j))
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h :
  ∀ (f : Z →ᵇ ℝ) (g : (j : κ) → Y j →ᵇ ℝ),
    ∫ (p : Z × ((j : κ) → Y j)), f p.1 * ∏ j, (g j) (p.2 j) ∂μ =
      ∫ (p : Z × ((j : κ) → Y j)), f p.1 * ∏ j, (g j) (p.2 j) ∂ν
e : Z × ((i : κ) → Y i) ≃ᵐ ((i : κ) → Y i) × Z := MeasurableEquiv.prodComm
f : (i : κ) → Y i →ᵇ ℝ
g : Z →ᵇ ℝ
⊢ ∫ (p : ((i : κ) → Y i) × Z), (∏ i, (f i) (p.1 i)) * g p.2 ∂Measure.map (⇑e) μ =
    ∫ (p : ((i : κ) → Y i) × Z), (∏ i, (f i) (p.1 i)) * g p.2 ∂Measure.map (⇑e) ν

Tactic:
integral_map_equiv,

Goal state after:
κ : Type u_2
Z : Type u_3
Y : κ → Type u_6
mY : (j : κ) → MeasurableSpace (Y j)
inst✝⁸ : (j : κ) → TopologicalSpace (Y j)
inst✝⁷ : ∀ (j : κ), BorelSpace (Y j)
inst✝⁶ : ∀ (j : κ), HasOuterApproxClosed (Y j)
mZ : MeasurableSpace Z
inst✝⁵ : TopologicalSpace Z
inst✝⁴ : BorelSpace Z
inst✝³ : HasOuterApproxClosed Z
inst✝² : Fintype κ
μ ν : Measure (Z × ((j : κ) → Y j))
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h :
  ∀ (f : Z →ᵇ ℝ) (g : (j : κ) → Y j →ᵇ ℝ),
    ∫ (p : Z × ((j : κ) → Y j)), f p.1 * ∏ j, (g j) (p.2 j) ∂μ =
      ∫ (p : Z × ((j : κ) → Y j)), f p.1 * ∏ j, (g j) (p.2 j) ∂ν
e : Z × ((i : κ) → Y i) ≃ᵐ ((i : κ) → Y i) × Z := MeasurableEquiv.prodComm
f : (i : κ) → Y i →ᵇ ℝ
g : Z →ᵇ ℝ
⊢ ∫ (x : Z × ((i : κ) → Y i)), (∏ i, (f i) ((e x).1 i)) * g (e x).2 ∂μ =
    ∫ (p : ((i : κ) → Y i) × Z), (∏ i, (f i) (p.1 i)) * g p.2 ∂Measure.map (⇑e) ν
Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd

Goal state before:
pp: Z : Type u_3
T : Type u_4
mZ : MeasurableSpace Z
inst✝⁷ : TopologicalSpace Z
inst✝⁶ : BorelSpace Z
inst✝⁵ : HasOuterApproxClosed Z
mT : MeasurableSpace T
inst✝⁴ : TopologicalSpace T
inst✝³ : BorelSpace T
inst✝² : HasOuterApproxClosed T
μ ν : Measure (Z × T)
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : ∀ (f : Z →ᵇ ℝ) (g : T →ᵇ ℝ), ∫ (p : Z × T), f p.1 * g p.2 ∂μ = ∫ (p : Z × T), f p.1 * g p.2 ∂ν
e : Z × T ≃ᵐ (Unit → Z) × (Unit → T) :=
  ((MeasurableEquiv.funUnique Unit Z).prodCongr (MeasurableEquiv.funUnique Unit T)).symm
f : Unit → Z →ᵇ ℝ
g : Unit → T →ᵇ ℝ
⊢ ∫ (p : (Unit → Z) × (Unit → T)), (∏ i, (f i) (p.1 i)) * ∏ j, (g j) (p.2 j) ∂Measure.map (⇑e) μ =
    ∫ (p : (Unit → Z) × (Unit → T)), (∏ i, (f i) (p.1 i)) * ∏ j, (g j) (p.2 j) ∂Measure.map (⇑e) ν

Tactic:
integral_map_equiv,

Goal state after:
Z : Type u_3
T : Type u_4
mZ : MeasurableSpace Z
inst✝⁷ : TopologicalSpace Z
inst✝⁶ : BorelSpace Z
inst✝⁵ : HasOuterApproxClosed Z
mT : MeasurableSpace T
inst✝⁴ : TopologicalSpace T
inst✝³ : BorelSpace T
inst✝² : HasOuterApproxClosed T
μ ν : Measure (Z × T)
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : ∀ (f : Z →ᵇ ℝ) (g : T →ᵇ ℝ), ∫ (p : Z × T), f p.1 * g p.2 ∂μ = ∫ (p : Z × T), f p.1 * g p.2 ∂ν
e : Z × T ≃ᵐ (Unit → Z) × (Unit → T) :=
  ((MeasurableEquiv.funUnique Unit Z).prodCongr (MeasurableEquiv.funUnique Unit T)).symm
f : Unit → Z →ᵇ ℝ
g : Unit → T →ᵇ ℝ
⊢ ∫ (x : Z × T), (∏ i, (f i) ((e x).1 i)) * ∏ j, (g j) ((e x).2 j) ∂μ =
    ∫ (p : (Unit → Z) × (Unit → T)), (∏ i, (f i) (p.1 i)) * ∏ j, (g j) (p.2 j) ∂Measure.map (⇑e) ν
Module: Mathlib.MeasureTheory.Measure.PreVariation

Goal state before:
pp: X : Type u_1
inst✝ : MeasurableSpace X
f : Set X → ℝ≥0∞
hf : IsSigmaSubadditiveSetFun f
hf' : f ∅ = 0
s : ℕ → Set X
hs : ∀ (i : ℕ), MeasurableSet (s i)
hs' : Pairwise (Disjoint on s)
b : ℝ≥0∞
Q : Finpartition ⟨⋃ i, s i, ⋯⟩
hQ : b < ∑ p ∈ Q.parts, f ↑p
s' : ℕ → Subtype MeasurableSet := fun i ↦ ⟨s i, ⋯⟩
P : (i : ℕ) → Finpartition (s' i) := fun i ↦ Q.restrict ⋯
splitting : ∑ q ∈ Q.parts, f ↑q ≤ ∑' (i : ℕ), ∑ p ∈ (P i).parts, f ↑p
n : ℕ
hn : b < ∑ a ∈ Finset.range n, ∑ p ∈ (P a).parts, f ↑p
⊢ ∃ I, b < ∑ i ∈ I, preVariationFun f (s i)

Tactic:
have bound (i : ℕ) : ∑ p ∈ (P i).parts, f p ≤ preVariationFun f (s i) := sum_le f (hs i) (P i)

Goal state after:
X : Type u_1
inst✝ : MeasurableSpace X
f : Set X → ℝ≥0∞
hf : IsSigmaSubadditiveSetFun f
hf' : f ∅ = 0
s : ℕ → Set X
hs : ∀ (i : ℕ), MeasurableSet (s i)
hs' : Pairwise (Disjoint on s)
b : ℝ≥0∞
Q : Finpartition ⟨⋃ i, s i, ⋯⟩
hQ : b < ∑ p ∈ Q.parts, f ↑p
s' : ℕ → Subtype MeasurableSet := fun i ↦ ⟨s i, ⋯⟩
P : (i : ℕ) → Finpartition (s' i) := fun i ↦ Q.restrict ⋯
splitting : ∑ q ∈ Q.parts, f ↑q ≤ ∑' (i : ℕ), ∑ p ∈ (P i).parts, f ↑p
n : ℕ
hn : b < ∑ a ∈ Finset.range n, ∑ p ∈ (P a).parts, f ↑p
bound : ∀ (i : ℕ), ∑ p ∈ (P i).parts, f ↑p ≤ preVariationFun f (s i)
⊢ ∃ I, b < ∑ i ∈ I, preVariationFun f (s i)
Module: Mathlib.MeasureTheory.Measure.SeparableMeasure

Goal state before:
pp: X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
h𝒜 : μ.MeasureDense 𝒜
t : Set X
ht : t ∈ 𝒜
hμt : μ (∅ ∆ t) < ENNReal.ofReal 1
⊢ t = ∅ ∆ t

Tactic:
rw [← bot_eq_empty, bot_symmDiff]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne

Goal state before:
pp: case neg
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsZeroOneMeasure μ
inst✝¹ : StandardBorelSpace α
inst✝ : NeZero μ
this : IsProbabilityMeasure μ
A : ℕ → Set α
hAm : ∀ (n : ℕ), MeasurableSet (A n)
hAsep : ∀ x ∈ univ, ∀ y ∈ univ, (∀ (n : ℕ), x ∈ A n ↔ y ∈ A n) → x = y
B : ℕ → Set α := fun n ↦ if h : μ (A n) = 1 then A n else (A n)ᶜ
mBn : MeasurableSet (⋂ n, B n)
n : ℕ
h : ¬μ (A n) = 1
⊢ μ (A n)ᶜᶜ = 0

Tactic:
rw [compl_compl]
      rcases μ.zero_one (A n) with (h₀ | h₁)
      · exact h₀
      · simp_all

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Prokhorov

Goal state before:
pp: case h
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
inst✝² : PseudoMetricSpace 𝓧
inst✝¹ : OpensMeasurableSpace 𝓧
inst✝ : SecondCountableTopology 𝓧
S : Set (ProbabilityMeasure 𝓧)
U : ℕ → Set 𝓧
O : ∀ (i : ℕ), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U i)
Cov : ⋃ i, U i = univ
hcomp : IsCompact (closure[ProbabilityMeasure.instTopologicalSpace] S)
ε : ℝ
hε' : 0 ≤ ε
hε : 0 < ε
hεbound : ε ≤ 1
μ : ℕ → ProbabilityMeasure 𝓧
hμInS : ∀ (k : ℕ), μ k ∈ S
hcontradiction : ∀ (k : ℕ), ↑((μ k) (⋃ i, ⋃ (_ : i ≤ k), U i)) ≤ 1 - ↑(NNReal.mk ε hε')
μlim : ProbabilityMeasure 𝓧
left✝ : μlim ∈ closure[ProbabilityMeasure.instTopologicalSpace] S
sub : ℕ → ℕ
hsubmono : StrictMono sub
hμconverges : Tendsto (μ ∘ sub) atTop (𝓝 μlim)
n : ℕ
⊢ ∀ (a : ℝ),
    (∀ᶠ (x : ℝ) in Filter.map (fun k ↦ ↑((μ (sub k)) (⋃ i, ⋃ (_ : i ≤ sub k), U i))) atTop, (fun x1 x2 ↦ x1 ≥ x2) x a) →
      (fun x1 x2 ↦ x1 ≥ x2) 1 a

Tactic:
simpa [eventually_map, eventually_atTop, forall_exists_index] using
            fun _ d hyp ↦ (hyp d (by simp)).trans (by simp)

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 b : α
hf : BoundedVariationOn f univ
x₀ : α
⊢ Monotone fun x ↦ variationOnFromTo (Function.rightLim f) univ x₀ x

Tactic:
rw [← monotoneOn_univ]
    exact variationOnFromTo.monotoneOn hf.rightLim.locallyBoundedVariationOn (mem_univ _)

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

Goal state before:
pp: case inr
α : 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
hf : BoundedVariationOn f univ
h'α : Nonempty α
m : AddContent E {s | ∃ u v, u ≤ v ∧ s = Ioc u v} := AddContent.onIoc (Function.rightLim f)
A : ∀ s ∈ {s | ∃ u v, u ≤ v ∧ s = Ioc u v}, ‖m s‖ₑ ≤ hf.measureAux s
B : hα = generateFrom {s | ∃ u v, u ≤ v ∧ s = Ioc u v}
m' : VectorMeasure α E
hm' : ∀ s ∈ {s | ∃ u v, u ≤ v ∧ s = Ioc u v}, m' s = m s
h'm' : ∀ (s : Set α), ‖m' s‖ₑ ≤ hf.measureAux s
⊢ ∃ m,
    (∀ (u v : α), u ≤ v → m (Ioc u v) = Function.rightLim f v - Function.rightLim f u) ∧
      m botSet = 0 ∧ ∀ (s : Set α), ‖m s‖ₑ ≤ hf.measureAux s

Tactic:
refine ⟨m', fun u v huv ↦ ?_, ?_, h'm'⟩

Goal state after:
case inr.refine_1
α : 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
hf : BoundedVariationOn f univ
h'α : Nonempty α
m : AddContent E {s | ∃ u v, u ≤ v ∧ s = Ioc u v} := AddContent.onIoc (Function.rightLim f)
A : ∀ s ∈ {s | ∃ u v, u ≤ v ∧ s = Ioc u v}, ‖m s‖ₑ ≤ hf.measureAux s
B : hα = generateFrom {s | ∃ u v, u ≤ v ∧ s = Ioc u v}
m' : VectorMeasure α E
hm' : ∀ s ∈ {s | ∃ u v, u ≤ v ∧ s = Ioc u v}, m' s = m s
h'm' : ∀ (s : Set α), ‖m' s‖ₑ ≤ hf.measureAux s
u v : α
huv : u ≤ v
⊢ m' (Ioc u v) = Function.rightLim f v - Function.rightLim f u

case inr.refine_2
α : 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
hf : BoundedVariationOn f univ
h'α : Nonempty α
m : AddContent E {s | ∃ u v, u ≤ v ∧ s = Ioc u v} := AddContent.onIoc (Function.rightLim f)
A : ∀ s ∈ {s | ∃ u v, u ≤ v ∧ s = Ioc u v}, ‖m s‖ₑ ≤ hf.measureAux s
B : hα = generateFrom {s | ∃ u v, u ≤ v ∧ s = Ioc u v}
m' : VectorMeasure α E
hm' : ∀ s ∈ {s | ∃ u v, u ≤ v ∧ s = Ioc u v}, m' s = m s
h'm' : ∀ (s : Set α), ‖m' s‖ₑ ≤ hf.measureAux s
⊢ m' botSet = 0
Module: Mathlib.MeasureTheory.VectorMeasure.Prod

Goal state before:
pp: X : Type u_2
Y : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
mX : MeasurableSpace X
mY : MeasurableSpace Y
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
μ : VectorMeasure X E
ν : VectorMeasure Y F
inst✝¹ : CompleteSpace G
inst✝ : IsFiniteMeasure μ.variation
B : F →L[ℝ] E →L[ℝ] G
s : Set (X × Y)
hs : MeasurableSet s
⊢ (μ.prod ν B.flip) s = ∫ᵛ (x : X), ν (Prod.mk x ⁻¹' s) ∂[B; μ]

Tactic:
simp [prod_apply_eq_integral hs]

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

Goal state before:
pp: X : Type u_1
mX : MeasurableSpace X
μ : SignedMeasure X
r : Set X
hr : MeasurableSet r
s : Set X
hs : MeasurableSet s
hpos : 0 ≤[s] μ
hneg : μ ≤[sᶜ] 0
hposPart : μ.toJordanDecomposition.posPart = μ.toMeasureOfZeroLE s hs hpos
hnegPart : μ.toJordanDecomposition.negPart = μ.toMeasureOfLEZero sᶜ ⋯ hneg
⊢ (μ.toMeasureOfZeroLE s hs hpos) r + (μ.toMeasureOfLEZero sᶜ ⋯ hneg) r = ‖μ (s ∩ r)‖ₑ + ‖μ (sᶜ ∩ r)‖ₑ

Tactic:
μ.toMeasureOfZeroLE_apply_eq_enorm hs hpos hr,

Goal state after:
X : Type u_1
mX : MeasurableSpace X
μ : SignedMeasure X
r : Set X
hr : MeasurableSet r
s : Set X
hs : MeasurableSet s
hpos : 0 ≤[s] μ
hneg : μ ≤[sᶜ] 0
hposPart : μ.toJordanDecomposition.posPart = μ.toMeasureOfZeroLE s hs hpos
hnegPart : μ.toJordanDecomposition.negPart = μ.toMeasureOfLEZero sᶜ ⋯ hneg
⊢ ‖μ (s ∩ r)‖ₑ + (μ.toMeasureOfLEZero sᶜ ⋯ hneg) r = ‖μ (s ∩ r)‖ₑ + ‖μ (sᶜ ∩ r)‖ₑ
Module: Mathlib.MeasureTheory.VectorMeasure.WithDensityVec

Goal state before:
pp: case neg
X : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
μ : VectorMeasure X F
f : X → E
B : E →L[ℝ] F →L[ℝ] G
hf : ¬μ.Integrable f
⊢ (μ.withDensity f B).variation ≤ (μ.transpose B).variation.withDensity fun x ↦ ‖f x‖ₑ

Tactic:
· simp [withDensity, hf, Measure.zero_le ]

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

Goal state before:
pp: case insert
ι : Type u_1
X : Type u_2
E : Type u_4
F : Type u_5
G : Type u_6
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f : X → E
B : E →L[ℝ] F →L[ℝ] G
μ : ι → VectorMeasure X F
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, (μ i).Integrable f) → ∫ᵛ (x : X), f x ∂[B; ∑ i ∈ s, μ i] = ∑ i ∈ s, ∫ᵛ (x : X), f x ∂[B; μ i]
hf : (μ a).Integrable f ∧ ∀ a ∈ s, (μ a).Integrable f
⊢ ∫ᵛ (x : X), f x ∂[B; μ a + ∑ i ∈ s, μ i] = ∫ᵛ (x : X), f x ∂[B; μ a] + ∑ i ∈ s, ∫ᵛ (x : X), f x ∂[B; μ i]

Tactic:
rw [integral_add_vectorMeasure hf.1 (Integrable.finsetSum_vectorMeasure hf.2), ih hf.2]

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

Goal state before:
pp: case hfg
X : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
mX : MeasurableSpace X
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
μ : VectorMeasure X F
f : X → E
B : E →L[ℝ] F →L[ℝ] G
inst✝ : CompleteSpace G
hf : μ.Integrable f
hB : ∀ (x : E) (y : F), ‖(B x) y‖₊ = ‖B.flip y‖₊ * ‖x‖₊
s : Set X
hs : MeasurableSet s
ε : NNReal
εpos : 0 < ε
δ : NNReal := ε / 3
δpos : 0 < δ
g : X →ₛ E
hg : eLpNorm (f - ⇑g) 1 (μ.transpose B).variation ≤ ↑δ
gmem : MemLp (⇑g) 1 μ.variation
a : X
⊢ ‖f a‖ₑ ≤ ‖f a - g a‖ₑ + ‖g a‖ₑ

Tactic:
show f a = (f a - g a) + g a by abel

Goal state after:
case hfg
X : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
mX : MeasurableSpace X
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
μ : VectorMeasure X F
f : X → E
B : E →L[ℝ] F →L[ℝ] G
inst✝ : CompleteSpace G
hf : μ.Integrable f
hB : ∀ (x : E) (y : F), ‖(B x) y‖₊ = ‖B.flip y‖₊ * ‖x‖₊
s : Set X
hs : MeasurableSet s
ε : NNReal
εpos : 0 < ε
δ : NNReal := ε / 3
δpos : 0 < δ
g : X →ₛ E
hg : eLpNorm (f - ⇑g) 1 (μ.transpose B).variation ≤ ↑δ
gmem : MemLp (⇑g) 1 μ.variation
a : X
⊢ ‖f a - g a + g a‖ₑ ≤ ‖f a - g a‖ₑ + ‖g a‖ₑ
Module: Mathlib.MeasureTheory.VectorMeasure.Integral

Goal state before:
pp: X : Type u_2
E : Type u_4
F : Type u_5
G : Type u_6
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f : X → E
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
le_ae : ∀ᵐ (a : X) ∂μ.variation, 0 ≤ ‖f a‖
h : AEStronglyMeasurable f μ.variation
⊢ ‖B‖ * (∫⁻ (a : X), ENNReal.ofReal ‖f a‖ ∂μ.variation).toReal = ‖B‖ * ∫ (a : X), ‖f a‖ ∂μ.variation

Tactic:
rw [integral_eq_lintegral_of_nonneg_ae le_ae <| h.norm]

Goal state after:
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability

Goal state before:
pp: case func.inl
α : Type u_1
A : Set ℕ
inst✝ : Fintype α
l : ℕ
ts : Fin l → presburger[[↑A]].Term α
f : presburger.Functions l
k : Fin l → ℕ
u : Fin l → α → ℕ
ih : ∀ (a : Fin l) (v : α → ℕ), Term.realize v (ts a) = k a + u a ⬝ᵥ v
⊢ ∃ k u, ∀ (v : α → ℕ), (Structure.funMap (Sum.inl f) fun i ↦ Term.realize v (ts i)) = k + u ⬝ᵥ v

Tactic:
cases f with
      | zero =>
        refine ⟨0, 0, fun v => ?_⟩
        rw [withConstants_funMap_sumInl]
        simp
      | one =>
        refine ⟨1, 0, fun v => ?_⟩
        rw [withConstants_funMap_sumInl]
        simp [ih]
      | add =>
        refine ⟨k 0 + k 1, u 0 + u 1, fun v => ?_⟩
        rw [withConstants_funMap_sumInl, add_dotProduct, add_left_comm, add_assoc, add_left_comm,
          ← add_assoc]
        simp [ih]

Goal state after:
Module: Mathlib.ModelTheory.Complexity

Goal state before:
pp: case neg
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
n : ℕ
inst✝ : Nonempty M
ψ : L.BoundedFormula α n
v : α → M
n✝ : ℕ
φ✝ : L.BoundedFormula α (n✝ + 1)
h✝ : φ✝.IsPrenex
ih :
  ∀ {φ : L.BoundedFormula α (n✝ + 1)},
    φ.IsQF → ∀ {xs : Fin (n✝ + 1) → M}, (φ.toPrenexImpRight φ✝).Realize v xs ↔ (φ ⟹ φ✝).Realize v xs
φ : L.BoundedFormula α n✝
hφ : φ.IsQF
xs : Fin n✝ → M
h' : φ.Realize v xs → ∃ a, φ✝.Realize v (snoc xs a)
h : ¬φ.Realize v xs
⊢ ∃ a, φ.Realize v xs → φ✝.Realize v (snoc xs a)

Tactic:
inhabit M

Goal state after:
case neg
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
n : ℕ
inst✝ : Nonempty M
ψ : L.BoundedFormula α n
v : α → M
n✝ : ℕ
φ✝ : L.BoundedFormula α (n✝ + 1)
h✝ : φ✝.IsPrenex
ih :
  ∀ {φ : L.BoundedFormula α (n✝ + 1)},
    φ.IsQF → ∀ {xs : Fin (n✝ + 1) → M}, (φ.toPrenexImpRight φ✝).Realize v xs ↔ (φ ⟹ φ✝).Realize v xs
φ : L.BoundedFormula α n✝
hφ : φ.IsQF
xs : Fin n✝ → M
h' : φ.Realize v xs → ∃ a, φ✝.Realize v (snoc xs a)
h : ¬φ.Realize v xs
inhabited_h : Inhabited M
⊢ ∃ a, φ.Realize v xs → φ✝.Realize v (snoc xs a)
Module: Mathlib.ModelTheory.FinitelyGenerated

Goal state before:
pp: case mpr.inr
L : Language
M : Type u_1
inst✝ : L.Structure M
N : L.Substructure M
h : ∃ s, (closure L).toFun (range s) = N
⊢ ∃ S, S.Countable ∧ (closure L).toFun S = N

Tactic:
obtain ⟨f, rfl⟩ := h

Goal state after:
case mpr.inr
L : Language
M : Type u_1
inst✝ : L.Structure M
f : ℕ → M
⊢ ∃ S, S.Countable ∧ (closure L).toFun S = (closure L).toFun (range f)
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddMonoid.FG M
F : Type u_5
G : Type u_6
inst✝³ : FunLike F M N
inst✝² : AddMonoidHomClass F M N
inst✝¹ : FunLike G M N
inst✝ : AddMonoidHomClass G M N
a b : N
f : F
g : G
n : ℕ
h : (Fin n → ℕ) →+ M
hh : Function.Surjective ⇑h
⊢ IsSemilinearSet (⇑h '' {a_1 | a + f (h a_1) = b + g (h a_1)})

Tactic:
apply IsSemilinearSet.image

Goal state after:
M : Type u_1
N : Type u_2
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddMonoid.FG M
F : Type u_5
G : Type u_6
inst✝³ : FunLike F M N
inst✝² : AddMonoidHomClass F M N
inst✝¹ : FunLike G M N
inst✝ : AddMonoidHomClass G M N
a b : N
f : F
g : G
n : ℕ
h : (Fin n → ℕ) →+ M
hh : Function.Surjective ⇑h
⊢ IsSemilinearSet {a_1 | a + f (h a_1) = b + g (h a_1)}
Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt

Goal state before:
pp: n : ℕ
⊢ (Λ * ↑ζ) n = log n

Tactic:
coe_mul_zeta_apply,

Goal state after:
n : ℕ
⊢ ∑ i ∈ n.divisors, Λ i = log n