mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare

Goal state before:
pp: case refine_2
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℝ F
a b c d : E
γ₁ : Path a b
γ₂ : Path c d
s : Set (↑I × ↑I)
t : Set E
ω : E → E →L[ℝ] F
dω : E → E →L[ℝ] E →L[ℝ] F
φ : (↑γ₁).Homotopy ↑γ₂
hs : s.Countable
hφt : ∀ a_1 ∈ Ioo 0 1, ∀ b_1 ∈ Ioo 0 1, φ (a_1, b_1) ∈ t
hω : ∀ a_1 ∈ Ioo 0 1, ∀ b_1 ∈ Ioo 0 1, (a_1, b_1) ∉ s → HasFDerivWithinAt ω (dω (φ (a_1, b_1))) t (φ (a_1, b_1))
hωc : ContinuousOn ω (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t)
hdω_symm :
  ∀ a_1 ∈ Ioo 0 1,
    ∀ b_1 ∈ Ioo 0 1,
      (a_1, b_1) ∉ s →
        ∀ u ∈ tangentConeAt ℝ t (φ (a_1, b_1)),
          ∀ v ∈ tangentConeAt ℝ t (φ (a_1, b_1)), ((dω (φ (a_1, b_1))) u) v = ((dω (φ (a_1, b_1))) v) u
U : Set (ℝ × ℝ) := Ioo 0 1 ×ˢ Ioo 0 1
hU : U = Ioo 0 1 ×ˢ Ioo 0 1
hinterior : interior (Icc 0 1) = U
hunique : UniqueDiffOn ℝ (Icc 0 1)
hUopen : IsOpen U
hU_subset : U ⊆ Icc 0 1
hclosure : closure U = Icc 0 1
ψ : ℝ × ℝ → E := fun xy ↦ Set.IccExtend ⋯ (⇑(φ.extend xy.1)) xy.2
hcontdiff : ContDiffOn ℝ 2 ψ (Icc 0 1)
hψ : ψ = fun xy ↦ Set.IccExtend ⋯ (⇑(φ.extend xy.1)) xy.2
hψφ : ∀ (a_1 b_1 : ↑I), ψ (↑a_1, ↑b_1) = φ (a_1, b_1)
hψ_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ψ
hψUt : MapsTo ψ U t
dψ : ℝ × ℝ → ℝ × ℝ →L[ℝ] E := fderivWithin ℝ ψ (Icc 0 1)
s' : Set (ℝ × ℝ) := Prod.map Subtype.val Subtype.val '' s
hs' : s' = Prod.map Subtype.val Subtype.val '' s
hmem_s' : ∀ (x y : ↑I), (↑x, ↑y) ∈ s' ↔ (x, y) ∈ s
hs'c : s'.Countable
hdψ : ∀ a ∈ U, HasFDerivAt ψ (dψ a) a
d2ψ : ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ × ℝ →L[ℝ] E := fderivWithin ℝ dψ (Icc 0 1)
hd2ψ : ∀ a ∈ U, HasFDerivAt dψ (d2ψ a) a
hd2ψ_symm : ∀ a ∈ Icc 0 1, ∀ (x y : ℝ × ℝ), ((d2ψ a) x) y = ((d2ψ a) y) x
η : ℝ × ℝ → ℝ × ℝ →L[ℝ] F := fun a ↦ ω (ψ a) ∘SL dψ a
f : ℝ × ℝ → F := fun a ↦ (η a) (0, 1)
hf : ∀ a ∈ Icc 0 1, f a = (ω (ψ a)) (derivWithin (ψ ∘ fun x ↦ (a.1, x)) I a.2)
g : ℝ × ℝ → F := fun a ↦ -(η a) (1, 0)
hg : ∀ a ∈ Icc 0 1, g a = (ω (ψ a)) (-derivWithin (ψ ∘ fun x ↦ (x, a.2)) I a.1)
dη : ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ × ℝ →L[ℝ] F :=
  fun a ↦ (ContinuousLinearMap.compL ℝ (ℝ × ℝ) E F) (ω (ψ a)) ∘SL d2ψ a + (dω (ψ a)).bilinearComp (dψ a) (dψ a)
hdη : ∀ a ∈ U \ s', HasFDerivAt η (dη a) a
hdη_symm : ∀ a ∈ U \ s', ∀ (u v : ℝ × ℝ), ((dη a) u) v = ((dη a) v) u
f' : ℝ × ℝ → ℝ × ℝ →L[ℝ] F := fun a ↦ (ContinuousLinearMap.apply ℝ F) (0, 1) ∘SL dη a
hf' : ∀ a ∈ U \ s', HasFDerivAt f (f' a) a
g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] F := fun a ↦ -(ContinuousLinearMap.apply ℝ F) (1, 0) ∘SL dη a
hg' : ∀ a ∈ U \ s', HasFDerivAt g (g' a) a
hf'g' : (fun a ↦ (f' a) (1, 0) + (g' a) (0, 1)) =ᵐ[volume.restrict (Icc 0 1)] 0
this : ∫ (a : ℝ × ℝ) in Icc 0 1, (f' a) (1, 0) + (g' a) (0, 1) = 0
⊢ ContinuousOn dψ (Icc 0 1)

Tactic:
· exact hcontdiff.continuousOn_fderivWithin hunique (by decide)

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

Goal state before:
pp: case neg
Ω : Type u_1
inst✝² : PseudoMetricSpace Ω
inst✝¹ : MeasurableSpace Ω
inst✝ : OpensMeasurableSpace Ω
P : ProbabilityMeasure Ω
G : Set Ω
G_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] G
ε : ℝ≥0∞
ε_pos : 0 < ε
easy : ε ≤ ↑P G
ε_top : ¬ε = ∞
aux : ↑P G - ε < liminf (fun Q ↦ ↑Q G) (𝓝 P)
⊢ {Q | ↑P G < ↑Q G + ε} ∈ 𝓝 P

Tactic:
filter_upwards [gt_mem_sets_of_limsInf_gt (α := ℝ≥0∞) isBounded_ge_of_bot
      (show P.toMeasure G - ε < limsInf ((𝓝 P).map (fun Q ↦ Q.toMeasure G)) from aux)] with Q hQ

Goal state after:
Ω : Type u_1
inst✝² : PseudoMetricSpace Ω
inst✝¹ : MeasurableSpace Ω
inst✝ : OpensMeasurableSpace Ω
P : ProbabilityMeasure Ω
G : Set Ω
G_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] G
ε : ℝ≥0∞
ε_pos : 0 < ε
easy : ε ≤ ↑P G
ε_top : ¬ε = ∞
aux : ↑P G - ε < liminf (fun Q ↦ ↑Q G) (𝓝 P)
Q : ProbabilityMeasure Ω
hQ : Q ∈ (fun Q ↦ ↑Q G) ⁻¹' {x | ↑P G - ε < x}
⊢ ↑P G < ↑Q G + ε
Module: Mathlib.MeasureTheory.Measure.Haar.Extension

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
E : Type u_4
inst✝¹⁸ : Group A
inst✝¹⁷ : Group B
inst✝¹⁶ : Group C
inst✝¹⁵ : TopologicalSpace A
inst✝¹⁴ : TopologicalSpace B
inst✝¹³ : TopologicalSpace C
φ : A →* B
ψ : B →* C
H : IsSES φ ψ
inst✝¹² : IsTopologicalGroup A
inst✝¹¹ : IsTopologicalGroup B
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : MeasurableSpace A
inst✝⁸ : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : IsTopologicalGroup C
inst✝⁵ : LocallyCompactSpace B
inst✝⁴ : MeasurableSpace C
inst✝³ : BorelSpace C
μC : Measure C
hμC : μC.IsHaarMeasure
inst✝² : T2Space B
inst✝¹ : MeasurableSpace B
inst✝ : BorelSpace B
U : Set B
hU : IsOpen U
⊢ U.Nonempty → (H.inducedMeasure μA μC) U ≠ 0

Tactic:
by
    rintro ⟨b, hb⟩
    obtain ⟨K, hK, hb, hKU⟩ := exists_compact_subset hU hb
    obtain ⟨f, hf1, hf2, hf3, hf4⟩ := exists_continuousMap_one_of_isCompact_subset_isOpen hK hU hKU
    have hf0 : 0 ≤ H.pushforward μA ⟨f, hf2⟩ := by
      rw [← map_zero (H.pushforward μA)]
      apply pushforward_mono
      exact fun x ↦ (hf4 x).1
    grw [← pos_iff_ne_zero, inducedMeasure,
      ← RealRMK.le_rieszMeasure_tsupport_subset (f := ⟨f, hf2⟩) _ hf4 hf3, ENNReal.ofReal_pos]
    suffices (0 : ℝ) < pushforward H μA ⟨f, hf2⟩ (ψ b) from
      (pushforward H μA ⟨f, hf2⟩).continuous.integral_pos_of_hasCompactSupport_nonneg_nonzero
        (pushforward H μA ⟨f, hf2⟩).hasCompactSupport hf0 this.ne'
    have : (Function.invFun ψ (ψ b))⁻¹ * b ∈ φ.range := by
      simp [← H.mulExact.monoidHom_ker_eq, Function.apply_invFun_apply]
    obtain ⟨a, ha⟩ := this
    replace ha : f (Function.invFun ψ (ψ b) * φ a) ≠ 0 := by simp [ha, hf1 (interior_subset hb)]
    exact (pullback H ⟨f, hf2⟩ _).continuous.integral_pos_of_hasCompactSupport_nonneg_nonzero
      (pullback H ⟨f, hf2⟩ _).hasCompactSupport (fun x ↦ (hf4 _).1) ha

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

Goal state before:
pp: case pos
Ω : Type u_1
inst✝³ : PseudoMetricSpace Ω
inst✝² : MeasurableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
inst✝ : SeparableSpace Ω
P : ProbabilityMeasure Ω
ε : ℝ
ε_pos : ε > 0
third_ε_pos : 0 < ε / 3
third_ε_pos' : 0 < ENNReal.ofReal (ε / 3)
Es : ℕ → Set Ω
Es_mble : ∀ (n : ℕ), MeasurableSet (Es n)
Es_bdd : ∀ (n : ℕ), Bornology.IsBounded (Es n)
Es_diam : ∀ (n : ℕ), diam (Es n) ≤ ε / 3
Es_cover : ⋃ n, Es n = univ
Es_disjoint : Pairwise fun n m ↦ Disjoint (Es n) (Es m)
N : ℕ
hN : ↑P (⋃ j ∈ Iio N, Es j)ᶜ < ENNReal.ofReal (ε / 3)
Js_finite : {J | J ⊆ Iio N}.Finite
Gs : Set (Set Ω) := (fun J ↦ thickening (ε / 3) (⋃ j ∈ J, Es j)) '' {J | J ⊆ Iio N}
Gs_open :
  ∀ (J : Set ℕ), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (thickening (ε / 3) (⋃ j ∈ J, Es j))
mem_nhds_P :
  ∀ (G : Set Ω),
    IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] G → {Q | ↑P G < ↑Q G + ENNReal.ofReal (ε / 3)} ∈ 𝓝 P
Q : ProbabilityMeasure Ω
hQ :
  ∀ i ⊆ Iio N,
    ↑P (⋃ i_2 ∈ i, thickening (ε / 3) (Es i_2)) < ↑Q (⋃ i_2 ∈ i, thickening (ε / 3) (Es i_2)) + ENNReal.ofReal (ε / 3)
δ : ℝ
B : Set Ω
δ_gt : 2 * (ε / 3) < δ
x✝ : MeasurableSet B
JB : Set ℕ := {i | (B ∩ Es i).Nonempty ∧ i ∈ Iio N}
ω : Ω
ω_in_B : ω ∈ B
i : ℕ
hi : ω ∈ Es i
i_small : i ∈ Iio N
⊢ (B ∩ Es i).Nonempty ∧ i < N

Tactic:
exact ⟨Set.nonempty_of_mem <| mem_inter ω_in_B hi, i_small⟩

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

Goal state before:
pp: case inl
E : Type u_1
p : ℝ
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hp : 0 < p
hE : Subsingleton E
⊢ μ {0} = ENNReal.ofReal (μ.real {0} • Real.exp (-‖0‖ ^ p) / Real.Gamma (↑(finrank ℝ E) / p + 1))

Tactic:
finrank_zero_of_subsingleton,

Goal state after:
case inl
E : Type u_1
p : ℝ
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hp : 0 < p
hE : Subsingleton E
⊢ μ {0} = ENNReal.ofReal (μ.real {0} • Real.exp (-‖0‖ ^ p) / Real.Gamma (↑0 / p + 1))
Module: Mathlib.MeasureTheory.Measure.IntegralCharFun

Goal state before:
pp: μ : Measure ℝ
r : ℝ
inst✝ : IsFiniteMeasure μ
hr : 0 < r
h_int : Integrable (Function.uncurry fun x y ↦ cexp (↑x * ↑y * I)) ((volume.restrict (Set.uIoc (-r) r)).prod μ)
⊢ ∫ (x : ℝ), 2 * r * sinc (r * x) ∂μ = 2 * r * ∫ (x : ℝ), sinc (r * x) ∂μ

Tactic:
← integral_const_mul

Goal state after:
μ : Measure ℝ
r : ℝ
inst✝ : IsFiniteMeasure μ
hr : 0 < r
h_int : Integrable (Function.uncurry fun x y ↦ cexp (↑x * ↑y * I)) ((volume.restrict (Set.uIoc (-r) r)).prod μ)
⊢ ∫ (x : ℝ), 2 * r * sinc (r * x) ∂μ = ∫ (a : ℝ), 2 * r * sinc (r * a) ∂μ
Module: Mathlib.MeasureTheory.Measure.IntegralCharFun

Goal state before:
pp: μ : Measure ℝ
r : ℝ
inst✝ : IsProbabilityMeasure μ
hr : 0 < r
integrable_sinc_const_mul : ∀ (r : ℝ), Integrable (fun x ↦ sinc (r * x)) μ
⊢ ∫ (x : ℝ) in {x | 2 < |2 * r⁻¹ * x|}, 1 ∂μ = 2 * ∫ (x : ℝ) in {x | 2 < |2 * r⁻¹ * x|}, 2⁻¹ ∂μ

Tactic:
← integral_const_mul

Goal state after:
μ : Measure ℝ
r : ℝ
inst✝ : IsProbabilityMeasure μ
hr : 0 < r
integrable_sinc_const_mul : ∀ (r : ℝ), Integrable (fun x ↦ sinc (r * x)) μ
⊢ ∫ (x : ℝ) in {x | 2 < |2 * r⁻¹ * x|}, 1 ∂μ = ∫ (a : ℝ) in {x | 2 < |2 * r⁻¹ * x|}, 2 * 2⁻¹ ∂μ
Module: Mathlib.MeasureTheory.Measure.SubFinite

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
inst✝ : IsFiniteMeasure (μ.withDensity g)
hg : Measurable g
hgf : g ≤ᵐ[μ] f
⊢ μ.withDensity (f - g) = μ.withDensity f - μ.withDensity g

Tactic:
by
  ext s hs
  rw [sub_apply hs (withDensity_mono hgf), withDensity_apply _ hs, withDensity_apply _ hs,
    withDensity_apply _ hs, ← lintegral_sub hg _ (ae_restrict_of_ae hgf)]
  · simp
  · simp [← withDensity_apply _ hs]

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

Goal state before:
pp: case mpr
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsZeroOneMeasure μ
⊢ μ univ = 1 → ∃ s, μ s = 1

Tactic:
intro h

Goal state after:
case mpr
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsZeroOneMeasure μ
h : μ univ = 1
⊢ ∃ s, μ s = 1
Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne

Goal state before:
pp: case mp
α : 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 α := ⋯
mBn : MeasurableSet (⋂ n, B n)
hBn : μ (⋂ n, B n) = 1
neBn : (⋂ n, B n).Nonempty
y : α
n : ℕ
hsome : ⋯.some ∈ if μ (A n) = 1 then A n else (A n)ᶜ
hy : y ∈ if μ (A n) = 1 then A n else (A n)ᶜ
⊢ y ∈ A n → neBn.some ∈ A n

Tactic:
intro h

Goal state after:
case mp
α : 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 : α
n : ℕ
hsome : ⋯.some ∈ if μ (A n) = 1 then A n else (A n)ᶜ
hy : y ∈ if μ (A n) = 1 then A n else (A n)ᶜ
h : y ∈ A n
⊢ neBn.some ∈ A n
Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne

Goal state before:
pp: case mpr
α : 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 α := ⋯
mBn : MeasurableSet (⋂ n, B n)
hBn : μ (⋂ n, B n) = 1
neBn : (⋂ n, B n).Nonempty
y : α
n : ℕ
hsome : ⋯.some ∈ if μ (A n) = 1 then A n else (A n)ᶜ
hy : y ∈ if μ (A n) = 1 then A n else (A n)ᶜ
⊢ neBn.some ∈ A n → y ∈ A n

Tactic:
intro h

Goal state after:
case mpr
α : 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 : α
n : ℕ
hsome : ⋯.some ∈ if μ (A n) = 1 then A n else (A n)ᶜ
hy : y ∈ if μ (A n) = 1 then A n else (A n)ᶜ
h : neBn.some ∈ A n
⊢ y ∈ A n
Module: Mathlib.MeasureTheory.SpecificCodomains.WithLp

Goal state before:
pp: X : Type u_1
mX : MeasurableSpace X
μ : Measure X
q : ℝ≥0∞
inst✝⁵ : Fact (1 ≤ q)
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
f : X → WithLp q (E × F)
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hf : Integrable f μ
| (∫ (x : X), f x ∂μ).ofLp.1

Tactic:
1

Goal state after:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
q : ℝ≥0∞
inst✝⁵ : Fact (1 ≤ q)
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
f : X → WithLp q (E × F)
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hf : Integrable f μ
| (∫ (x : X), f x ∂μ).ofLp
Module: Mathlib.MeasureTheory.SpecificCodomains.WithLp

Goal state before:
pp: X : Type u_1
mX : MeasurableSpace X
μ : Measure X
q : ℝ≥0∞
inst✝⁵ : Fact (1 ≤ q)
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
f : X → WithLp q (E × F)
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace E
hf : Integrable f μ
| (∫ (x : X), f x ∂μ).ofLp.2

Tactic:
1

Goal state after:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
q : ℝ≥0∞
inst✝⁵ : Fact (1 ≤ q)
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
f : X → WithLp q (E × F)
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace E
hf : Integrable f μ
| (∫ (x : X), f x ∂μ).ofLp
Module: Mathlib.MeasureTheory.VectorMeasure.Variation.Basic

Goal state before:
pp: X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst✝ : NormedAddCommGroup V
μ : VectorMeasure X V
E : Set X
hE : μ.variation E ≠ ∞
⊢ ‖μ E‖ₑ ≤ μ.variation E

Tactic:
exact enorm_measure_le_variation μ E

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

Goal state before:
pp: α : 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₁
this : IsClosed {s | ‖m₁ s‖ₑ ≤ μ ↑s}
s : MeasuredSets μ
hs : s ∈ C'
⊢ ‖m₁ s‖ₑ ≤ μ ↑s

Tactic:
convert! hm s (C'C s hs)

Goal state after:
α : 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₁
this : IsClosed {s | ‖m₁ s‖ₑ ≤ μ ↑s}
s : MeasuredSets μ
hs : s ∈ C'
⊢ m₁ s = m ↑s
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
hts : s ⊆ t
h't : ∀ x ∈ t \ s, f x = 0
⊢ ∫ᵛ (x : X) in t, f x ∂[B; μ] = ∫ᵛ (x : X) in s, f x ∂[B; μ]

Tactic:
apply setIntegral_eq_of_subset_of_ae_sdiff_eq_zero hs ht hts
  apply (ae_restrict_iff' (ht.diff hs)).2
  filter_upwards with x using h't x

Goal state after:
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.toSignedMeasure =
    (μ.jordanDecompositionOfToSignedMeasureSub ν).toSignedMeasure

Tactic:
rw [SignedMeasure.toSignedMeasure_toJordanDecomposition,
    jordanDecompositionOfToSignedMeasureSub_toSignedMeasure]

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

Goal state before:
pp: case mp
M : Type u_1
N : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
s : Set M
F : Type u_6
inst✝¹ : EquivLike F M N
inst✝ : AddEquivClass F M N
f : F
⊢ IsSemilinearSet (⇑f '' s) → IsSemilinearSet s

Tactic:
intro h

Goal state after:
case mp
M : Type u_1
N : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
s : Set M
F : Type u_6
inst✝¹ : EquivLike F M N
inst✝ : AddEquivClass F M N
f : F
h : IsSemilinearSet (⇑f '' s)
⊢ IsSemilinearSet s
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs

Goal state before:
pp: case mpr
M : Type u_1
N : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
s : Set M
F : Type u_6
inst✝¹ : EquivLike F M N
inst✝ : AddEquivClass F M N
f : F
⊢ IsSemilinearSet s → IsSemilinearSet (⇑f '' s)

Tactic:
intro h

Goal state after:
case mpr
M : Type u_1
N : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
s : Set M
F : Type u_6
inst✝¹ : EquivLike F M N
inst✝ : AddEquivClass F M N
f : F
h : IsSemilinearSet s
⊢ IsSemilinearSet (⇑f '' s)
Module: Mathlib.MeasureTheory.VectorMeasure.Integral

Goal state before:
pp: X : Type u_2
E : Type u_4
F : Type u_5
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
f : X → E
μ : VectorMeasure X F
hf : μ.Integrable f
s : Set X
⊢ (μ.restrict s).Integrable f

Tactic:
by_cases hs : MeasurableSet s
  · simpa [VectorMeasure.Integrable, transpose_restrict, variation_restrict hs] using
      MeasureTheory.Integrable.restrict hf
  · simp [restrict_not_measurable _ hs]

Goal state after:
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
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
β : Type u_10
inst✝ : MeasurableSpace β
φ : X → β
hφ : Measurable φ
f : β → E
hfm : AEStronglyMeasurable f (Measure.map φ μ.variation)
hfi' : μ.Integrable (f ∘ φ)
⊢ ∫ᵛ (y : β), f y ∂[B; μ.map φ] = ∫ᵛ (x : X), f (φ x) ∂[B; μ]

Tactic:
apply setToFun_of_le_map _ _ hfi' hfm hφ variation_map_le
  intro s x hs
  simp [hs, VectorMeasure.map, transpose, hφ]

Goal state after:
Module: Mathlib.ModelTheory.FinitelyGenerated

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

Tactic:
intro h

Goal state after:
case mpr
L : Language
M : Type u_1
inst✝ : L.Structure M
N : L.Substructure M
h : ↑N = ∅ ∨ ∃ s, (closure L).toFun (range s) = N
⊢ ∃ S, S.Countable ∧ (closure L).toFun S = N
Module: Mathlib.ModelTheory.FinitelyGenerated

Goal state before:
pp: L : Language
M : Type u_1
inst✝² : L.Structure M
N : Type u_2
inst✝¹ : L.Structure N
inst✝ : Countable N
h✝ : FG L M
S : Set M
finite_S : S.Finite
closure_S : (closure L).toFun S = ⊤
g : (M →[L] N) → ↑S → N := ⋯
f f' : M →[L] N
h : g f = g f'
⊢ EqOn (⇑f) (⇑f') S

Tactic:
intro x x_in_S

Goal state after:
L : Language
M : Type u_1
inst✝² : L.Structure M
N : Type u_2
inst✝¹ : L.Structure N
inst✝ : Countable N
h✝ : FG L M
S : Set M
finite_S : S.Finite
closure_S : (closure L).toFun S = ⊤
g : (M →[L] N) → ↑S → N := fun f ↦ ⇑f ∘ Subtype.val
f f' : M →[L] N
h : g f = g f'
x : M
x_in_S : x ∈ S
⊢ f x = f' x
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)
x y : Σˣ f
i : ι
hx : x.fst ≤ i
hy : y.fst ≤ i
⊢ x ≈ y ↔ (f x.fst i hx) x.snd = (f y.fst i hy) y.snd

Tactic:
cases x

Goal state after:
case mk
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)
y : Σˣ f
i : ι
hy : y.fst ≤ i
fst✝ : ι
snd✝ : G fst✝
hx : ⟨fst✝, snd✝⟩.fst ≤ i
⊢ ⟨fst✝, snd✝⟩ ≈ y ↔ (f ⟨fst✝, snd✝⟩.fst i hx) ⟨fst✝, snd✝⟩.snd = (f y.fst i hy) y.snd
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ≃ₚ[L] N
g : N ≃ₚ[L] M
⊢ f.symm ≤ g → f ≤ g.symm

Tactic:
intro h

Goal state after:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ≃ₚ[L] N
g : N ≃ₚ[L] M
h : f.symm ≤ g
⊢ f ≤ g.symm
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ≃ₚ[L] N
g : N ≃ₚ[L] M
⊢ f ≤ g.symm → f.symm ≤ g

Tactic:
intro h

Goal state after:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ≃ₚ[L] N
g : N ≃ₚ[L] M
h : f ≤ g.symm
⊢ f.symm ≤ g
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
h_dom : f.dom = g.dom
⊢ (∀ (x : M) (h : x ∈ f.dom), f.cod.subtype (f.toEquiv ⟨x, h⟩) = g.cod.subtype (g.toEquiv ⟨x, ⋯⟩)) → f = g

Tactic:
intro h

Goal state after:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
h_dom : f.dom = g.dom
h : ∀ (x : M) (h : x ∈ f.dom), f.cod.subtype (f.toEquiv ⟨x, h⟩) = g.cod.subtype (g.toEquiv ⟨x, ⋯⟩)
⊢ f = g
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
i : ↑hs.basisSet
⊢ hs.floor hs.base i = 0

Tactic:
simp [floor]

Goal state after:
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ≃ₚ[L] N
A : L.Substructure M
h : A ≤ f.dom
⊢ M ≃ₚ[L] N

Tactic:
let g := (subtype _).comp (f.toEquiv.toEmbedding.comp (A.inclusion h))

Goal state after:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ≃ₚ[L] N
A : L.Substructure M
h : A ≤ f.dom
g : ↥A ↪[L] N := f.cod.subtype.comp (f.toEquiv.toEmbedding.comp (inclusion h))
⊢ M ≃ₚ[L] N
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: case refl
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
cod : L.Substructure N
g : ↥{ carrier := Set.univ, fun_mem := ⋯ } ≃[L] ↥cod
h_cod : { dom := { carrier := Set.univ, fun_mem := ⋯ }, cod := cod, toEquiv := g }.cod = ⊤
⊢ (toEquivOfEqTop ⋯ h_cod).toEmbedding = toEmbeddingOfEqTop ⋯

Tactic:
cases h_cod

Goal state after:
case refl.refl
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
g : ↥{ carrier := Set.univ, fun_mem := ⋯ } ≃[L] ↥{ carrier := Set.univ, fun_mem := ⋯ }
⊢ (toEquivOfEqTop ⋯ ⋯).toEmbedding = toEmbeddingOfEqTop ⋯