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

Goal state before:
pp: ι : 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 μ
inst✝ : IsFiniteMeasure ν
h :
  ∀ (f : (i : ι) → X i →ᵇ ℝ) (g : (j : κ) → Y j →ᵇ ℝ),
    ∫ (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) ∂ν
⊢ μ = ν

Tactic:
by
  refine ext_of_lintegral_prod_mul_prod_boundedContinuousFunction fun f g ↦ ?_
  rw [← toReal_eq_toReal_iff']
  · simp only [ofNNReal_finsetProd]
    have {μ : Measure ((Π i, X i) × Π j, Y j)} :
        (∫⁻ p, (∏ i, (f i (p.1 i) : ℝ≥0∞)) * ∏ j, (g j (p.2 j) : ℝ≥0∞) ∂μ).toReal =
          ∫ p, (∏ i, (f i (p.1 i)).toReal) * ∏ j, (g j (p.2 j)).toReal ∂μ := by
      rw [integral_eq_lintegral_of_nonneg_ae]
      · simp [Finset.prod_nonneg, ofReal_prod_of_nonneg]
      · exact Eventually.of_forall fun _ ↦ by positivity
      exact AEStronglyMeasurable.mul
        (Finset.aestronglyMeasurable_fun_prod _ fun _ _ ↦
          continuous_coe.aestronglyMeasurable.comp_measurable (by fun_prop))
        (Finset.aestronglyMeasurable_fun_prod _ fun _ _ ↦
          continuous_coe.aestronglyMeasurable.comp_measurable (by fun_prop))
    simp_rw [this]
    exact h (fun i ↦ ⟨⟨fun x ↦ (f i x), by fun_prop⟩, (f i).map_bounded'⟩)
      (fun j ↦ ⟨⟨fun y ↦ (g j y), by fun_prop⟩, (g j).map_bounded'⟩)
  · convert!
    (lintegral_lt_top_of_nnreal μ
        ((∏ i, (f i).compContinuous ⟨Function.eval i ∘ Prod.fst, by fun_prop⟩) *
          (∏ j, (g j).compContinuous ⟨Function.eval j ∘ Prod.snd, by fun_prop⟩))).ne
    simp
  · convert!
    (lintegral_lt_top_of_nnreal ν
        ((∏ i, (f i).compContinuous ⟨Function.eval i ∘ Prod.fst, by fun_prop⟩) *
          (∏ j, (g j).compContinuous ⟨Function.eval j ∘ Prod.snd, by fun_prop⟩))).ne
    simp

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

Goal state before:
pp: case refine_2.inr
E : Type u_1
inst✝³ : MeasurableSpace E
inst✝² : TopologicalSpace E
inst✝¹ : T2Space E
inst✝ : BorelSpace E
u : ℕ → ℝ≥0
K : ℕ → Set E
C : ℝ≥0
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
I :
  ∀ (μ : FiniteMeasure E) (n : ℕ),
    ∑ i ∈ Finset.range (n + 1), μ.restrict (disjointed K i) = μ.restrict ((partialSups K) n)
A : ∀ (n : ℕ), IsCompact ((partialSups K) n)
f : Ultrafilter (FiniteMeasure E)
hf : {μ | μ.mass ≤ C ∧ ∀ (n : ℕ), μ (K n)ᶜ ≤ u n} ∈ f
ν : ℕ → FiniteMeasure E
ν_reg : ∀ (n : ℕ), (↑(ν n)).InnerRegular
νK : ∀ (n : ℕ), (ν n) ((partialSups K) n)ᶜ = 0
hν : ∀ (n : ℕ), Tendsto (fun ρ ↦ ρ.restrict (disjointed K n)) (↑f) (𝓝 (ν n))
B : (Measure.sum fun n ↦ ↑(ν n)) univ ≤ ↑C
μ : FiniteMeasure E := ⟨Measure.sum fun n ↦ ↑(ν n), ⋯⟩
L : Tendsto id (↑f) (𝓝 μ)
n : ℕ
h : Monotone K
⊢ ∑' (i : ℕ), ↑(ν i) (K n)ᶜ ≤ ↑(u n)

Tactic:
have : Tendsto (fun m ↦ ∑ i ∈ Finset.range (m + 1), (ν i : Measure E) (K n)ᶜ) atTop
        (𝓝 (∑' i, (ν i : Measure E) (K n)ᶜ)) :=
      (ENNReal.tendsto_nat_tsum _).comp (tendsto_add_atTop_nat 1)

Goal state after:
case refine_2.inr
E : Type u_1
inst✝³ : MeasurableSpace E
inst✝² : TopologicalSpace E
inst✝¹ : T2Space E
inst✝ : BorelSpace E
u : ℕ → ℝ≥0
K : ℕ → Set E
C : ℝ≥0
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
I :
  ∀ (μ : FiniteMeasure E) (n : ℕ),
    ∑ i ∈ Finset.range (n + 1), μ.restrict (disjointed K i) = μ.restrict ((partialSups K) n)
A : ∀ (n : ℕ), IsCompact ((partialSups K) n)
f : Ultrafilter (FiniteMeasure E)
hf : {μ | μ.mass ≤ C ∧ ∀ (n : ℕ), μ (K n)ᶜ ≤ u n} ∈ f
ν : ℕ → FiniteMeasure E
ν_reg : ∀ (n : ℕ), (↑(ν n)).InnerRegular
νK : ∀ (n : ℕ), (ν n) ((partialSups K) n)ᶜ = 0
hν : ∀ (n : ℕ), Tendsto (fun ρ ↦ ρ.restrict (disjointed K n)) (↑f) (𝓝 (ν n))
B : (Measure.sum fun n ↦ ↑(ν n)) univ ≤ ↑C
μ : FiniteMeasure E := ⟨Measure.sum fun n ↦ ↑(ν n), ⋯⟩
L : Tendsto id (↑f) (𝓝 μ)
n : ℕ
h : Monotone K
this : Tendsto (fun m ↦ ∑ i ∈ Finset.range (m + 1), ↑(ν i) (K n)ᶜ) atTop (𝓝 (∑' (i : ℕ), ↑(ν i) (K n)ᶜ))
⊢ ∑' (i : ℕ), ↑(ν i) (K n)ᶜ ≤ ↑(u n)
Module: Mathlib.MeasureTheory.Measure.WithDensityFinite

Goal state before:
pp: case pos
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
t : Set α
ht : MeasurableSet t
hμt : μ (t ∩ (μ.sigmaFiniteSetWRT μ)ᶜ) = 0
⊢ ∞ * μ (t ∩ (μ.sigmaFiniteSetWRT μ)ᶜ) = ∞ * μ.toFinite (t ∩ (μ.sigmaFiniteSetWRT μ)ᶜ)

Tactic:
hμt,

Goal state after:
case pos
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
t : Set α
ht : MeasurableSet t
hμt : μ (t ∩ (μ.sigmaFiniteSetWRT μ)ᶜ) = 0
⊢ ∞ * 0 = ∞ * μ.toFinite (t ∩ (μ.sigmaFiniteSetWRT μ)ᶜ)
Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsZeroOneMeasure μ
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
hμs : μ s = 1
hμt : μ t = 1
h✝ : μ (s ∩ t) = 0
⊢ 0 + (1 - μ t) ≤ 0

Tactic:
hμt,

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsZeroOneMeasure μ
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
hμs : μ s = 1
hμt : μ t = 1
h✝ : μ (s ∩ t) = 0
⊢ 0 + (1 - 1) ≤ 0
Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne

Goal state before:
pp: α : 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)
hBn : μ (⋂ n, B n) = 1
neBn : (⋂ n, B n).Nonempty
y : α
hy : y ∈ ⋂ n, B n
⊢ y = neBn.some

Tactic:
refine hAsep y (by trivial) neBn.some (by trivial) fun n ↦ ?_

Goal state after:
α : 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)
hBn : μ (⋂ n, B n) = 1
neBn : (⋂ n, B n).Nonempty
y : α
hy : y ∈ ⋂ n, B n
n : ℕ
⊢ y ∈ A n ↔ neBn.some ∈ A n
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
P : Finset (Set X)
Ps : ∀ t ∈ P, t ⊆ s
P_disj : (↑P).PairwiseDisjoint id
P_meas : ∀ t ∈ P, MeasurableSet t
hP : a < ∑ p ∈ P, ‖μ p‖ₑ
⊢ ∑ i ∈ P with 0 ≤ μ i, |μ i| = |μ (⋃ p ∈ {p ∈ P | 0 ≤ μ p}, p)|

Tactic:
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

Goal state after:
X : Type u_1
mX : MeasurableSpace X
μ : SignedMeasure X
s : Set X
hs : MeasurableSet s
a : ℝ≥0∞
ha : a < (variation μ) s
P : Finset (Set X)
Ps : ∀ t ∈ P, t ⊆ s
P_disj : (↑P).PairwiseDisjoint id
P_meas : ∀ t ∈ P, MeasurableSet t
hP : a < ∑ p ∈ P, ‖μ p‖ₑ
A : ∑ x ∈ P with 0 ≤ μ x, |μ x| = μ (⋃ x ∈ {x ∈ P | 0 ≤ μ x}, x)
⊢ ∑ i ∈ P with 0 ≤ μ i, |μ i| = |μ (⋃ p ∈ {p ∈ P | 0 ≤ μ p}, p)|
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:
by
  /- One may almost realize the variation through a partition into finitely many sets.
  As their measures are real numbers, we can group together those of positive measure, and
  also those of negative measure. This gives two measurable sets. Among these two, the one with the
  largest measure in absolute value satisfies the result. -/
  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 b : α
hf : BoundedVariationOn f univ
x₀ : α
⊢ Monotone fun x ↦ variationOnFromTo (Function.rightLim f) univ x₀ x

Tactic:
← monotoneOn_univ

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 b : α
hf : BoundedVariationOn f univ
x₀ : α
⊢ MonotoneOn (fun x ↦ variationOnFromTo (Function.rightLim f) univ x₀ x) univ
Module: Mathlib.MeasureTheory.VectorMeasure.BoundedVariation

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

Tactic:
hm'

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_1.a
α : 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
⊢ Ioc u v ∈ {s | ∃ u v, u ≤ v ∧ s = Ioc u v}
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.JordanSub

Goal state before:
pp: X : Type u_1
mX : MeasurableSpace X
s : Set X
μ ν : Measure X
hs : IsHahnDecomposition μ ν s
⊢ (μ - ν) s = 0

Tactic:
rw [← restrict_eq_zero, restrict_sub_eq_restrict_sub_restrict hs.measurableSet]

Goal state after:
X : Type u_1
mX : MeasurableSpace X
s : Set X
μ ν : Measure X
hs : IsHahnDecomposition μ ν s
⊢ μ.restrict s - ν.restrict s = 0
Module: Mathlib.MeasureTheory.VectorMeasure.SetIntegral

Goal state before:
pp: X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedAddCommGroup G
μ : VectorMeasure X F
f : X → E
s t : Set X
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
hs : MeasurableSet s
ht : MeasurableSet t
ht_eq : ∀ᵐ (x : X) ∂μ.variation, x ∈ t → f x = 0
x : X
hx : x ∈ t → f x = 0
⊢ (s ∪ t).indicator f x = s.indicator f x

Tactic:
simp only [indicator_apply, mem_union]

Goal state after:
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedAddCommGroup G
μ : VectorMeasure X F
f : X → E
s t : Set X
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
hs : MeasurableSet s
ht : MeasurableSet t
ht_eq : ∀ᵐ (x : X) ∂μ.variation, x ∈ t → f x = 0
x : X
hx : x ∈ t → f x = 0
⊢ (if x ∈ s ∨ x ∈ t then f x else 0) = if x ∈ s then f x else 0
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.JordanSub

Goal state before:
pp: X : Type u_1
mX : MeasurableSpace X
μ ν : Measure X
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
⊢ (μ.toSignedMeasure - ν.toSignedMeasure).toJordanDecomposition = μ.jordanDecompositionOfToSignedMeasureSub ν

Tactic:
apply JordanDecomposition.toSignedMeasure_injective
  rw [SignedMeasure.toSignedMeasure_toJordanDecomposition,
    jordanDecompositionOfToSignedMeasureSub_toSignedMeasure]

Goal state after:
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
⊢ ‖μ s‖₊ ≤ μ.bound

Tactic:
rw [← ENNReal.coe_le_coe, ← enorm_eq_nnnorm]

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
⊢ ‖μ s‖ₑ ≤ ↑μ.bound
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
S₁ : Set (Set M)
hS₁ : S₁.Finite
hS₁' : ∀ t ∈ S₁, IsLinearSet t
S₂ : Set (Set M)
hS₂ : S₂.Finite
hS₂' : ∀ t ∈ S₂, IsLinearSet t
s : Set M
hs : s ∈ S₁ ∪ S₂
⊢ IsLinearSet s

Tactic:
mem_union

Goal state after:
M : Type u_1
inst✝ : AddCommMonoid M
S₁ : Set (Set M)
hS₁ : S₁.Finite
hS₁' : ∀ t ∈ S₁, IsLinearSet t
S₂ : Set (Set M)
hS₂ : S₂.Finite
hS₂' : ∀ t ∈ S₂, IsLinearSet t
s : Set M
hs : s ∈ S₁ ∨ s ∈ S₂
⊢ IsLinearSet s
Module: Mathlib.MeasureTheory.VectorMeasure.Integral

Goal state before:
pp: X : Type u_2
F : Type u_5
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
μ : VectorMeasure X F
⊢ (μ.transpose (lsmul ℝ ℝ)).variation = μ.variation

Tactic:
apply variation_transpose_eq

Goal state after:
X : Type u_2
F : Type u_5
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
μ : VectorMeasure X F
⊢ ∀ (x : ℝ) (y : F), ‖((lsmul ℝ ℝ) x) y‖₊ = ‖x‖₊ * ‖y‖₊
Module: Mathlib.MeasureTheory.VectorMeasure.Integral

Goal state before:
pp: X : Type u_2
E : Type u_4
mX : MeasurableSpace X
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
μ : SignedMeasure X
⊢ (transpose μ (lsmul ℝ ℝ).flip).variation = variation μ

Tactic:
apply variation_transpose_eq

Goal state after:
X : Type u_2
E : Type u_4
mX : MeasurableSpace X
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
μ : SignedMeasure X
⊢ ∀ (x : E) (y : ℝ), ‖((lsmul ℝ ℝ).flip x) y‖₊ = ‖x‖₊ * ‖y‖₊
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
S₁ : Set (Set M)
hS₁ : S₁.Finite
hS₁' : ∀ t ∈ S₁, IsProperLinearSet t
S₂ : Set (Set M)
hS₂ : S₂.Finite
hS₂' : ∀ t ∈ S₂, IsProperLinearSet t
s : Set M
hs : s ∈ S₁ ∪ S₂
⊢ IsProperLinearSet s

Tactic:
mem_union

Goal state after:
M : Type u_1
inst✝ : AddCommMonoid M
S₁ : Set (Set M)
hS₁ : S₁.Finite
hS₁' : ∀ t ∈ S₁, IsProperLinearSet t
S₂ : Set (Set M)
hS₂ : S₂.Finite
hS₂' : ∀ t ∈ S₂, IsProperLinearSet t
s : Set M
hs : s ∈ S₁ ∨ s ∈ S₂
⊢ IsProperLinearSet s
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
inst✝ : IsEmpty X
⊢ ∫ᵛ (x : X), f x ∂[B; μ] = 0

Tactic:
simp [eq_zero_of_isEmpty]

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
μ : VectorMeasure X F
B : ι → E →L[ℝ] F →L[ℝ] G
hf : μ.Integrable f
a : ι
s : Finset ι
ha : a ∉ s
ih : ∫ᵛ (x : X), f x ∂[∑ i ∈ s, B i; μ] = ∑ i ∈ s, ∫ᵛ (x : X), f x ∂[B i; μ]
⊢ ∫ᵛ (x : X), f x ∂[B a + ∑ i ∈ s, B i; μ] = ∫ᵛ (x : X), f x ∂[B a; μ] + ∑ i ∈ s, ∫ᵛ (x : X), f x ∂[B i; μ]

Tactic:
rw [integral_add_cbm hf, ih]

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

Goal state before:
pp: case neg.ind
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
f : M → AddSubmonoid M :=
  fun x ↦ if hx : x ∈ s then { carrier := {y | x + y ∈ s}, add_mem' := ⋯, zero_mem' := ⋯ } else ⊥
hf : ∀ x ∈ s, ∀ (y : M), y ∈ f x ↔ x + y ∈ s
g : M → AddSemigroupIdeal M := fun x ↦ AddSemigroupIdeal.closure (↑(f x) \ {0})
hg : ∀ x ∈ s, ∀ y ∈ s, x ≤ y → g x ≤ g y
a : M
ha : MaximalFor (fun x ↦ x ∈ s) g a
x : M
hx : a + x ∈ s
w : M
ih : ∀ y < w, ∀ u ∈ f a, u ≠ 0 → a + x + (y + u) ∈ s → y + u ∈ f a
u : M
hu₁ : u ∈ f a
hu₂ : u ≠ 0
hxy : a + x + (w + u) ∈ s
⊢ w + u ∈ f a

Tactic:
by_cases hw₁ : w = 0

Goal state after:
case pos
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
f : M → AddSubmonoid M :=
  fun x ↦ if hx : x ∈ s then { carrier := {y | x + y ∈ s}, add_mem' := ⋯, zero_mem' := ⋯ } else ⊥
hf : ∀ x ∈ s, ∀ (y : M), y ∈ f x ↔ x + y ∈ s
g : M → AddSemigroupIdeal M := fun x ↦ AddSemigroupIdeal.closure (↑(f x) \ {0})
hg : ∀ x ∈ s, ∀ y ∈ s, x ≤ y → g x ≤ g y
a : M
ha : MaximalFor (fun x ↦ x ∈ s) g a
x : M
hx : a + x ∈ s
w : M
ih : ∀ y < w, ∀ u ∈ f a, u ≠ 0 → a + x + (y + u) ∈ s → y + u ∈ f a
u : M
hu₁ : u ∈ f a
hu₂ : u ≠ 0
hxy : a + x + (w + u) ∈ s
hw₁ : w = 0
⊢ w + u ∈ f a

case neg
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
f : M → AddSubmonoid M :=
  fun x ↦ if hx : x ∈ s then { carrier := {y | x + y ∈ s}, add_mem' := ⋯, zero_mem' := ⋯ } else ⊥
hf : ∀ x ∈ s, ∀ (y : M), y ∈ f x ↔ x + y ∈ s
g : M → AddSemigroupIdeal M := fun x ↦ AddSemigroupIdeal.closure (↑(f x) \ {0})
hg : ∀ x ∈ s, ∀ y ∈ s, x ≤ y → g x ≤ g y
a : M
ha : MaximalFor (fun x ↦ x ∈ s) g a
x : M
hx : a + x ∈ s
w : M
ih : ∀ y < w, ∀ u ∈ f a, u ≠ 0 → a + x + (y + u) ∈ s → y + u ∈ f a
u : M
hu₁ : u ∈ f a
hu₂ : u ≠ 0
hxy : a + x + (w + u) ∈ s
hw₁ : ¬w = 0
⊢ w + u ∈ f a
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✝¹ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
inst✝ : IsDirectedOrder ι
x✝⁴ x✝³ x✝² : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
i : ι
x : G i
j : ι
y : G j
x✝¹ :
  match ⟨i, x⟩ with
  | ⟨i, x⟩ =>
    match ⟨j, y⟩ with
    | ⟨j, y⟩ => ∃ k, ∃ (ik : i ≤ k) (jk : j ≤ k), (f i k ik) x = (f j k jk) y
k : ι
z : G k
x✝ :
  match ⟨j, y⟩ with
  | ⟨i, x⟩ =>
    match ⟨k, z⟩ with
    | ⟨j, y⟩ => ∃ k, ∃ (ik : i ≤ k) (jk : j ≤ k), (f i k ik) x = (f j k jk) y
ij : ι
hiij : i ≤ ij
hjij : j ≤ ij
hij : (f i ij hiij) x = (f j ij hjij) y
jk : ι
hjjk : j ≤ jk
hkjk : k ≤ jk
hjk : (f j jk hjjk) y = (f k jk hkjk) z
⊢ match ⟨i, x⟩ with
  | ⟨i, x⟩ =>
    match ⟨k, z⟩ with
    | ⟨j, y⟩ => ∃ k, ∃ (ik : i ≤ k) (jk : j ≤ k), (f i k ik) x = (f j k jk) y

Tactic:
by
        obtain ⟨ijk, hijijk, hjkijk⟩ := directed_of (· ≤ ·) ij jk
        refine ⟨ijk, le_trans hiij hijijk, le_trans hkjk hjkijk, ?_⟩
        rw [← DirectedSystem.map_map _ hiij hijijk, hij, DirectedSystem.map_map]
        rw [← DirectedSystem.map_map _ hkjk hjkijk, ← hjk, DirectedSystem.map_map]

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

Goal state before:
pp: ι : Type u_3
x y : ι → ℕ
⊢ toRatVec x = toRatVec y ↔ x = y

Tactic:
by
  refine ⟨fun h => ?_, congr_arg toRatVec⟩
  ext i
  simpa [toRatVec] using congr_fun h i

Goal state after: