mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Group.GeometryOfNumbers

Goal state before:
pp: E : Type u_1
inst✝⁸ : MeasurableSpace E
μ : Measure E
F s : Set E
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : Nontrivial E
inst✝² : μ.IsAddHaarMeasure
L : AddSubgroup E
inst✝¹ : Countable ↥L
inst✝ : DiscreteTopology ↥L
fund : IsAddFundamentalDomain (↥L) F μ
h_symm : ∀ x ∈ s, -x ∈ s
h_conv : Convex ℝ s
h_cpt : IsCompact s
h : μ F * 2 ^ finrank ℝ E ≤ μ s
⊢ ∃ x, x ≠ 0 ∧ ↑x ∈ s

Tactic:
by
  have h_mes : μ s ≠ 0 := fun hμ ↦ fund.measure_ne_zero (NeZero.ne μ) <| by simpa [hμ] using h
  have h_nemp : s.Nonempty := nonempty_of_measure_ne_zero h_mes
  let u : ℕ → ℝ≥0 := (exists_seq_strictAnti_tendsto 0).choose
  let K : ConvexBody E := ⟨s, h_conv, h_cpt, h_nemp⟩
  let S : ℕ → ConvexBody E := fun n => (1 + u n) • K
  let Z : ℕ → Set E := fun n => (S n) ∩ (L \ {0})
  -- The convex bodies `S n` have volume strictly larger than `μ s` and thus we can apply
  -- `exists_ne_zero_mem_lattice_of_measure_mul_two_pow_lt_measure` to them and obtain that
  -- `S n` contains a nonzero point of `L`. Since the intersection of the `S n` is equal to `s`,
  -- it follows that `s` contains a nonzero point of `L`.
  have h_zero : 0 ∈ K := K.zero_mem_of_symmetric h_symm
  suffices Set.Nonempty (⋂ n, Z n) by
    simp_rw [Z, S, ConvexBody.coe_smul', NNReal.smul_def, ← Set.iInter_inter, NNReal.coe_add,
      NNReal.coe_one] at this
    rw [K.iInter_smul_eq_self h_zero] at this
    · obtain ⟨x, hx⟩ := this
      exact ⟨⟨x, by simp_all⟩, by aesop⟩
    · exact (exists_seq_strictAnti_tendsto (0 : ℝ≥0)).choose_spec.2.2
  have h_clos : IsClosed ((L : Set E) \ {0}) := by
    rsuffices ⟨U, hU⟩ : ∃ U : Set E, IsOpen U ∧ U ∩ L = {0}
    · rw [sdiff_eq_sdiff_iff_inf_eq_inf (z := U).mpr (by simp [Set.inter_comm .. ▸ hU.2, zero_mem])]
      exact AddSubgroup.isClosed_of_discrete.sdiff hU.1
    exact isOpen_inter_eq_singleton_of_mem_discrete ⟨inferInstance⟩ (zero_mem L)
  refine IsCompact.nonempty_iInter_of_sequence_nonempty_isCompact_isClosed Z (fun n => ?_)
    (fun n => ?_) ((S 0).isCompact.inter_right h_clos) (fun n => (S n).isClosed.inter h_clos)
  · refine Set.inter_subset_inter_left _ (SetLike.coe_subset_coe.mpr ?_)
    refine ConvexBody.smul_le_of_le K h_zero ?_
    rw [add_le_add_iff_left]
    exact le_of_lt <| (exists_seq_strictAnti_tendsto (0 : ℝ≥0)).choose_spec.1 (Nat.lt_add_one n)
  · suffices μ F * 2 ^ finrank ℝ E < μ (S n : Set E) by
      have h_symm' : ∀ x ∈ S n, -x ∈ S n := by
        rintro _ ⟨y, hy, rfl⟩
        exact ⟨-y, h_symm _ hy, by simp⟩
      obtain ⟨x, hx_nz, hx_mem⟩ := exists_ne_zero_mem_lattice_of_measure_mul_two_pow_lt_measure
        fund h_symm' (S n).convex this
      exact ⟨x, hx_mem, by simp_all⟩
    refine lt_of_le_of_lt h ?_
    rw [ConvexBody.coe_smul', NNReal.smul_def, addHaar_smul_of_nonneg _ (NNReal.coe_nonneg _)]
    rw [show μ s < _ ↔ 1 * μ s < _ by rw [one_mul]]
    dsimp [K]
    gcongr
    · exact h_cpt.measure_ne_top
    rw [ofReal_pow (by positivity)]
    refine one_lt_pow₀ ?_ (ne_of_gt finrank_pos)
    simp [u, (exists_seq_strictAnti_tendsto (0 : ℝ≥0)).choose_spec.2.1 n]

Goal state after:
Module: Mathlib.MeasureTheory.Function.UnifTight

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ℕ → α → β
g : α → β
haef : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
hf : ∀ (n : ℕ), StronglyMeasurable (AEStronglyMeasurable.mk (f n) ⋯)
hff' : ∀ (n : ℕ), f n =ᵐ[μ] AEStronglyMeasurable.mk (f n) ⋯
hg : StronglyMeasurable (AEStronglyMeasurable.mk g ⋯)
hgg' : g =ᵐ[μ] AEStronglyMeasurable.mk g ⋯
hg'' : MemLp (AEStronglyMeasurable.mk g ⋯) p μ
haefg' : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ AEStronglyMeasurable.mk (f n) ⋯ x) atTop (𝓝 (AEStronglyMeasurable.mk g ⋯ x))
f' : ℕ → α → β := fun n ↦ AEStronglyMeasurable.mk (f n) ⋯
hui' : UnifIntegrable f' p μ
hut' : UnifTight f' p μ
⊢ Tendsto (fun n ↦ eLpNorm (f n - g) p μ) atTop (𝓝 0)

Tactic:
set g' := hg'.aestronglyMeasurable.mk (μ := μ)

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ℕ → α → β
g : α → β
haef : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
hf : ∀ (n : ℕ), StronglyMeasurable (AEStronglyMeasurable.mk (f n) ⋯)
hff' : ∀ (n : ℕ), f n =ᵐ[μ] AEStronglyMeasurable.mk (f n) ⋯
f' : ℕ → α → β := fun n ↦ AEStronglyMeasurable.mk (f n) ⋯
hui' : UnifIntegrable f' p μ
hut' : UnifTight f' p μ
g' : α → β := AEStronglyMeasurable.mk g ⋯
hg : StronglyMeasurable g'
hgg' : g =ᵐ[μ] g'
hg'' : MemLp g' p μ
haefg' : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ AEStronglyMeasurable.mk (f n) ⋯ x) atTop (𝓝 (g' x))
⊢ Tendsto (fun n ↦ eLpNorm (f n - g) p μ) atTop (𝓝 0)
Module: Mathlib.Topology.ContinuousMap.CompactlySupported

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁷ : TopologicalSpace α
inst✝⁶ : R1Space α
inst✝⁵ : Group α
inst✝⁴ : TopologicalSpace β
inst✝³ : R1Space β
inst✝² : Group β
inst✝¹ : ContinuousMul β
inst✝ : NormedAddCommGroup γ
φ : α →* β
hφ : Topology.IsClosedEmbedding ⇑φ
f : β →C_c γ
b : β
⊢ HasCompactSupport fun a ↦ f (b * φ a)

Tactic:
by
    obtain ⟨K, hK, hf⟩ := exists_compact_iff_hasCompactSupport.mpr f.hasCompactSupport
    refine exists_compact_iff_hasCompactSupport.mp ⟨φ ⁻¹' (b⁻¹ • K),
      hφ.isCompact_preimage (hK.smul b⁻¹), fun x hx ↦ hf _ ?_⟩
    simpa [Set.mem_smul_set_iff_inv_smul_mem] using hx

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

Goal state before:
pp: p q : ℝ
hp : 1 ≤ p
hq : -2 < q
⊢ -π ≤ π

Tactic:
linarith [pi_nonneg]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
a b c d : E
ω : E → E →L[𝕜] F
γ : Path a b
hc : c = a
hd : d = b
⊢ curveIntegralFun ω (γ.cast hc hd) = curveIntegralFun ω γ

Tactic:
by
  ext t
  simp only [curveIntegralFun_def', Path.extend_cast]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
a b c d : E
ω : E → E →L[𝕜] F
γ : Path a b
hc : c = a
hd : d = b
⊢ CurveIntegrable ω (γ.cast hc hd) ↔ CurveIntegrable ω γ

Tactic:
by
  simp [CurveIntegrable]

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

Goal state before:
pp: p q b : ℝ
hp : 1 ≤ p
hq : -2 < q
hb : 0 < b
⊢ -π ≤ π

Tactic:
linarith [pi_nonneg]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
s : Set α
f g : α → ℝ
μ : Measure α
hs_conn : IsConnected s
hs_meas : MeasurableSet s
hf : ContinuousOn f s
hg : IntegrableOn g s μ
hfg : IntegrableOn (fun x ↦ f x * g x) s μ
hg0 : ∀ᵐ (x : α) ∂μ.restrict s, 0 ≤ g x
ρ : α → ENNReal := fun x ↦ ENNReal.ofReal (g x)
ν : Measure α := μ.withDensity ρ
⊢ AEMeasurable ρ (μ.restrict s)

Tactic:
apply AEMeasurable.ennreal_ofReal

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
s : Set α
f g : α → ℝ
μ : Measure α
hs_conn : IsConnected s
hs_meas : MeasurableSet s
hf : ContinuousOn f s
hg : IntegrableOn g s μ
hfg : IntegrableOn (fun x ↦ f x * g x) s μ
hg0 : ∀ᵐ (x : α) ∂μ.restrict s, 0 ≤ g x
ρ : α → ENNReal := ⋯
ν : Measure α := ⋯
⊢ AEMeasurable g (μ.restrict s)
Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁸ : RCLike 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
a b : E
ω : E → E →L[𝕜] F
γ : Path a b
𝕝 : Type u_4
inst✝³ : RCLike 𝕝
inst✝² : NormedSpace 𝕝 F
inst✝¹ : NormedSpace 𝕝 E
inst✝ : LinearMap.CompatibleSMul E F 𝕝 𝕜
⊢ CurveIntegrable (fun t ↦ ContinuousLinearMap.restrictScalars 𝕝 (ω t)) γ ↔ CurveIntegrable ω γ

Tactic:
by
  simp [CurveIntegrable]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral

Goal state before:
pp: case hfB.hf
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b C : ℝ
hab : a ≤ b
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hnorm : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ C
s : Set ℝ := ⋯
hsm : MeasurableSet s
t : ℝ
ht : t ∈ Ioo a b → ‖deriv f t‖ ≤ C
ht_mem : t ∈ Ioo a b
⊢ t ∉ s → ‖deriv f t‖ ≤ 0

Tactic:
· simp only [s, norm_le_zero_iff]
          exact not_imp_comm.2 fun h ↦ subset_toMeasurable _ _ h

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral

Goal state before:
pp: case hnorm
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
a b : E
C : ℝ
hfc : ContinuousOn f (segment ℝ a b)
hfd : ∀ t ∈ Ioo 0 1, LineDifferentiableAt ℝ f ((lineMap a b) t) (b - a)
hf' : ∀ᵐ (t : ℝ), t ∈ Ioo 0 1 → ‖lineDeriv ℝ f ((lineMap a b) t) (b - a)‖ ≤ C
g : ℝ → F := ⋯
hgc : ContinuousOn g (Icc 0 1)
hdg : ∀ t ∈ Ioo 0 1, HasDerivAt g (lineDeriv ℝ f ((lineMap a b) t) (b - a)) t
⊢ ∀ᵐ (t : ℝ), t ∈ Ioo 0 1 → ‖deriv g t‖ ≤ C

Tactic:
exact hf'.mono fun t ht ht_mem ↦ by simpa only [(hdg t ht_mem).deriv] using ht ht_mem

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule

Goal state before:
pp: f : ℝ → ℝ
N : ℕ
a h : ℝ
N_nonzero : 0 < N
⊢ trapezoidal_integral f N a (a + ↑N * h) + trapezoidal_integral f 1 (a + ↑N * h) (a + (↑N + 1) * h) =
    trapezoidal_integral f (N + 1) a (a + (↑N + 1) * h)

Tactic:
← Nat.cast_add_one,

Goal state after:
f : ℝ → ℝ
N : ℕ
a h : ℝ
N_nonzero : 0 < N
⊢ trapezoidal_integral f N a (a + ↑N * h) + trapezoidal_integral f 1 (a + ↑N * h) (a + ↑(N + 1) * h) =
    trapezoidal_integral f (N + 1) a (a + ↑(N + 1) * h)
Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
K1 K2 : Compacts X
ε : ℝ≥0
⊢ 0 < ε → rieszContentAux Λ (K1 ⊔ K2) ≤ rieszContentAux Λ K1 + rieszContentAux Λ K2 + ε

Tactic:
εpos

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
K1 K2 : Compacts X
ε : ℝ≥0
εpos : 0 < ε
⊢ rieszContentAux Λ (K1 ⊔ K2) ≤ rieszContentAux Λ K1 + rieszContentAux Λ K2 + ε
Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare

Goal state before:
pp: 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 ∈ Ioo 0 1, ∀ b_1 ∈ Ioo 0 1, φ (a, b_1) ∈ t
hω : ∀ a ∈ Ioo 0 1, ∀ b_1 ∈ Ioo 0 1, (a, b_1) ∉ s → HasFDerivWithinAt ω (dω (φ (a, b_1))) t (φ (a, b_1))
hωc : ContinuousOn ω (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t)
hdω_symm :
  ∀ a ∈ Ioo 0 1,
    ∀ b_1 ∈ Ioo 0 1,
      (a, b_1) ∉ s →
        ∀ u ∈ tangentConeAt ℝ t (φ (a, b_1)),
          ∀ v ∈ tangentConeAt ℝ t (φ (a, b_1)), ((dω (φ (a, b_1))) u) v = ((dω (φ (a, 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 b_1 : ↑I), ψ (↑a, ↑b_1) = φ (a, 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
a : ℝ × ℝ
ha : a ∈ Icc 0 1
⊢ ∀ (x y : ℝ × ℝ), ((d2ψ a) x) y = ((d2ψ a) y) x

Tactic:
exact (hcontdiff a ha).isSymmSndFDerivWithinAt (by simp) hunique
      (by simp [hinterior, hclosure, ha]) ha

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

Goal state before:
pp: case hf
n : ℕ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : (Fin (n + 1) → ℂ) → E
c : Fin (n + 1) → ℂ
R : Fin (n + 1) → ℝ
hf : TorusIntegrable f c R
i : Fin (n + 1)
e : ℝ × (Fin n → ℝ) ≃ᵐ (Fin (n + 1) → ℝ) := (MeasurableEquiv.piFinSuccAbove (fun x ↦ ℝ) i).symm
hem : MeasurePreserving (⇑e) volume volume
heπ : (⇑e ⁻¹' Icc 0 fun x ↦ 2 * π) = Icc 0 (2 * π) ×ˢ Icc 0 fun x ↦ 2 * π
⊢ IntegrableOn (fun x ↦ (∏ i, ↑(R i) * cexp (↑(e x i) * I) * I) • f (torusMap c R (e x)))
    (Icc 0 (2 * π) ×ˢ Icc 0 fun x ↦ 2 * π) (volume.prod volume)

Tactic:
have := hf.function_integrable

Goal state after:
case hf
n : ℕ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : (Fin (n + 1) → ℂ) → E
c : Fin (n + 1) → ℂ
R : Fin (n + 1) → ℝ
hf : TorusIntegrable f c R
i : Fin (n + 1)
e : ℝ × (Fin n → ℝ) ≃ᵐ (Fin (n + 1) → ℝ) := (MeasurableEquiv.piFinSuccAbove (fun x ↦ ℝ) i).symm
hem : MeasurePreserving (⇑e) volume volume
heπ : (⇑e ⁻¹' Icc 0 fun x ↦ 2 * π) = Icc 0 (2 * π) ×ˢ Icc 0 fun x ↦ 2 * π
this : IntegrableOn (fun θ ↦ (∏ i, ↑(R i) * cexp (↑(θ i) * I) * I) • f (torusMap c R θ)) (Icc 0 fun x ↦ 2 * π) volume
⊢ IntegrableOn (fun x ↦ (∏ i, ↑(R i) * cexp (↑(e x i) * I) * I) • f (torusMap c R (e x)))
    (Icc 0 (2 * π) ×ˢ Icc 0 fun x ↦ 2 * π) (volume.prod volume)
Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real

Goal state before:
pp: case h.refine_3
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
f : X →C_c ℝ
a ε : ℝ
hε : 0 < ε
N : ℕ
hf : range ⇑f ⊆ Ioo a (a + ↑N * ε)
b : ℝ := a + ↑N * ε
y : Fin N → ℝ := fun n ↦ a + ε * (↑↑n + 1)
hy : ∀ {n m : Fin N}, n < m → y n + ε ≤ y m
E : Fin N → Set X := fun n ↦ ⇑f ⁻¹' Ioc (y n - ε) (y n) ∩ tsupport ⇑f
n✝ : Fin N
x✝ : X
hx : x✝ ∈ E n✝
⊢ a + ε * ↑↑n✝ < f x✝ ∧ f x✝ ≤ a + ε * (↑↑n✝ + 1)

Tactic:
simp only [mem_inter_iff, mem_preimage, mem_Ioc, E, y] at hx

Goal state after:
case h.refine_3
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
f : X →C_c ℝ
a ε : ℝ
hε : 0 < ε
N : ℕ
hf : range ⇑f ⊆ Ioo a (a + ↑N * ε)
b : ℝ := a + ↑N * ε
y : Fin N → ℝ := fun n ↦ a + ε * (↑↑n + 1)
hy : ∀ {n m : Fin N}, n < m → y n + ε ≤ y m
E : Fin N → Set X := fun n ↦ ⇑f ⁻¹' Ioc (y n - ε) (y n) ∩ tsupport ⇑f
n✝ : Fin N
x✝ : X
hx : (a + ε * (↑↑n✝ + 1) - ε < f x✝ ∧ f x✝ ≤ a + ε * (↑↑n✝ + 1)) ∧ x✝ ∈ tsupport ⇑f
⊢ a + ε * ↑↑n✝ < f x✝ ∧ f x✝ ≤ a + ε * (↑↑n✝ + 1)
Module: Mathlib.MeasureTheory.Measure.FiniteMeasureExt

Goal state before:
pp: E : Type u_1
𝕜 : Type u_2
inst✝⁷ : RCLike 𝕜
inst✝⁶ : MeasurableSpace E
inst✝⁵ : PseudoEMetricSpace E
inst✝⁴ : BorelSpace E
inst✝³ : CompleteSpace E
inst✝² : SecondCountableTopology E
P P' : Measure E
inst✝¹ : IsFiniteMeasure P
inst✝ : IsFiniteMeasure P'
A : StarSubalgebra 𝕜 (E →ᵇ 𝕜)
hA : (StarSubalgebra.map (toContinuousMapStarₐ 𝕜) A).SeparatesPoints
heq : ∀ g ∈ A, ∫ (x : E), g x ∂P = ∫ (x : E), g x ∂P'
A_toReal : Subalgebra ℝ (E →ᵇ ℝ) :=
  Subalgebra.comap (AlgHom.compLeftContinuousBounded ℝ ofRealAm ⋯) (Subalgebra.restrictScalars ℝ A.toSubalgebra)
hA_toReal : (Subalgebra.map (toContinuousMapₐ ℝ) A_toReal).SeparatesPoints
g : E →ᵇ ℝ
hgA_toReal : g ∈ A_toReal
⊢ ↑(∫ (x : E), g x ∂P) = ↑(∫ (x : E), g x ∂P')

Tactic:
← integral_ofReal,

Goal state after:
E : Type u_1
𝕜 : Type u_2
inst✝⁷ : RCLike 𝕜
inst✝⁶ : MeasurableSpace E
inst✝⁵ : PseudoEMetricSpace E
inst✝⁴ : BorelSpace E
inst✝³ : CompleteSpace E
inst✝² : SecondCountableTopology E
P P' : Measure E
inst✝¹ : IsFiniteMeasure P
inst✝ : IsFiniteMeasure P'
A : StarSubalgebra 𝕜 (E →ᵇ 𝕜)
hA : (StarSubalgebra.map (toContinuousMapStarₐ 𝕜) A).SeparatesPoints
heq : ∀ g ∈ A, ∫ (x : E), g x ∂P = ∫ (x : E), g x ∂P'
A_toReal : Subalgebra ℝ (E →ᵇ ℝ) :=
  Subalgebra.comap (AlgHom.compLeftContinuousBounded ℝ ofRealAm ⋯) (Subalgebra.restrictScalars ℝ A.toSubalgebra)
hA_toReal : (Subalgebra.map (toContinuousMapₐ ℝ) A_toReal).SeparatesPoints
g : E →ᵇ ℝ
hgA_toReal : g ∈ A_toReal
⊢ ∫ (x : E), ↑(g x) ∂P = ↑(∫ (x : E), g x ∂P')
Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝ : IsProbabilityMeasure P
X : Ω → ℝ
hX : AEMeasurable X P
hint : MemLp id 2 (Measure.map X P)
t : ℝ
⊢ taylorWithinEval (charFun (Measure.map X P)) 2 univ 0 t =
    1 + ↑(∫ (x : Ω), X x ∂P) * ↑t * I - ↑(∫ (x : Ω), (X ^ 2) x ∂P) * ↑t ^ 2 / 2

Tactic:
have : IsProbabilityMeasure (P.map X) := Measure.isProbabilityMeasure_map hX
  convert! taylorWithinEval_charFun_zero hint t with x
  simp only [Pi.pow_apply, Nat.reduceAdd, Finset.sum_range_succ, Finset.range_one,
    Finset.sum_singleton, Nat.factorial_zero, Nat.cast_one, inv_one, pow_zero, mul_one,
    integral_const, probReal_univ, smul_eq_mul, ofReal_one, Nat.factorial_one, pow_one, one_mul,
    Nat.factorial_two, Nat.cast_ofNat]
  rw [integral_map, integral_map]
  any_goals fun_prop
  simp [field]
  ring

Goal state after:
Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic

Goal state before:
pp: E : Type u_2
mE : MeasurableSpace E
μ : Measure E
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
t : E
⊢ ∫ (x : E), cexp (↑⟪x, t⟫ * I) ∂μ = ∫ (v : E), cexp (2 * ↑π * ((2 * ↑π)⁻¹ * ↑⟪v, t⟫) * I) ∂μ

Tactic:
congr with x

Goal state after:
case e_f
E : Type u_2
mE : MeasurableSpace E
μ : Measure E
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
t x : E
⊢ cexp (↑⟪x, t⟫ * I) = cexp (2 * ↑π * ((2 * ↑π)⁻¹ * ↑⟪x, t⟫) * I)
Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real

Goal state before:
pp: case calc_5
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : MeasurableSpace X
inst✝¹ : BorelSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst✝ : LocallyCompactSpace X
f : X →C_c ℝ
μ : Measure X := rieszMeasure Λ
K : Set X := tsupport ⇑f
ε : ℝ
hε : 0 < ε
a b : ℝ
hab : a < b ∧ range ⇑f ⊆ Ioo a b
N : ℕ
hN : 0 < N
ε' : ℝ := (b - a) / ↑N
hε' : 0 < ε' ∧ ε' * (2 * μ.real K + |a| + b + ε') ≤ ε
E : Fin N → Set X
hE :
  tsupport ⇑f = ⋃ j, E j ∧
    univ.PairwiseDisjoint E ∧
      (∀ (n : Fin N), ∀ x ∈ E n, a + ε' * ↑↑n < f x ∧ f x ≤ a + ε' * (↑↑n + 1)) ∧ ∀ (n : Fin N), MeasurableSet (E n)
y : Fin N → ℝ := fun n ↦ a + ε' * (↑↑n + 1)
hE' : ∀ (n : Fin N), μ (E n) ≠ ∞
V : Fin N → Opens X
hV : ∀ (n : Fin N), E n ⊆ ↑(V n) ∧ (∀ x ∈ V n, f x < y n + ε') ∧ μ ↑(V n) ≤ μ (E n) + ENNReal.ofReal (ε' / ↑N)
g : Fin N → X →C_c ℝ
hg :
  (∀ (n : Fin N), tsupport ⇑(g n) ⊆ (V n).carrier) ∧
    EqOn (∑ n, ⇑(g n)) 1 (tsupport f.toFun) ∧
      (∀ (n : Fin N) (x : X), (g n) x ∈ Icc 0 1) ∧ ∀ (n : Fin N), HasCompactSupport ⇑(g n)
this : ∀ (n : Fin N), (|a| + y n + ε') * μ.real (E n) = (|a| + 2 * ε') * μ.real (E n) + (y n - ε') * μ.real (E n)
⊢ ∑ x, ((|a| + 2 * ε') * μ.real (E x) + (y x - ε') * μ.real (E x) + (|a| + y x + ε') * (ε' / ↑N)) - |a| * μ.real K =
    ∑ n, (y n - ε') * μ.real (E n) + 2 * ε' * μ.real K + ε' / ↑N * ∑ n, (|a| + y n + ε')

Tactic:
have : ∑ i, μ.real (E i) = μ.real K := by
      suffices h : μ K = ∑ i, (μ (E i)) by
        simp only [measureReal_def, h]
        exact Eq.symm <| ENNReal.toReal_sum <| fun n _ ↦ hE' n
      dsimp [K]; rw [hE.1]
      rw [measure_iUnion (fun m n hmn ↦ hE.2.1 trivial trivial hmn) hE.2.2.2]
      exact tsum_fintype fun b ↦ μ (E b)

Goal state after:
case calc_5
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : MeasurableSpace X
inst✝¹ : BorelSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst✝ : LocallyCompactSpace X
f : X →C_c ℝ
μ : Measure X := rieszMeasure Λ
K : Set X := tsupport ⇑f
ε : ℝ
hε : 0 < ε
a b : ℝ
hab : a < b ∧ range ⇑f ⊆ Ioo a b
N : ℕ
hN : 0 < N
ε' : ℝ := (b - a) / ↑N
hε' : 0 < ε' ∧ ε' * (2 * μ.real K + |a| + b + ε') ≤ ε
E : Fin N → Set X
hE :
  tsupport ⇑f = ⋃ j, E j ∧
    univ.PairwiseDisjoint E ∧
      (∀ (n : Fin N), ∀ x ∈ E n, a + ε' * ↑↑n < f x ∧ f x ≤ a + ε' * (↑↑n + 1)) ∧ ∀ (n : Fin N), MeasurableSet (E n)
y : Fin N → ℝ := fun n ↦ a + ε' * (↑↑n + 1)
hE' : ∀ (n : Fin N), μ (E n) ≠ ∞
V : Fin N → Opens X
hV : ∀ (n : Fin N), E n ⊆ ↑(V n) ∧ (∀ x ∈ V n, f x < y n + ε') ∧ μ ↑(V n) ≤ μ (E n) + ENNReal.ofReal (ε' / ↑N)
g : Fin N → X →C_c ℝ
hg :
  (∀ (n : Fin N), tsupport ⇑(g n) ⊆ (V n).carrier) ∧
    EqOn (∑ n, ⇑(g n)) 1 (tsupport f.toFun) ∧
      (∀ (n : Fin N) (x : X), (g n) x ∈ Icc 0 1) ∧ ∀ (n : Fin N), HasCompactSupport ⇑(g n)
this✝ : ∀ (n : Fin N), (|a| + y n + ε') * μ.real (E n) = (|a| + 2 * ε') * μ.real (E n) + (y n - ε') * μ.real (E n)
this : ∑ i, μ.real (E i) = μ.real K
⊢ ∑ x, ((|a| + 2 * ε') * μ.real (E x) + (y x - ε') * μ.real (E x) + (|a| + y x + ε') * (ε' / ↑N)) - |a| * μ.real K =
    ∑ n, (y n - ε') * μ.real (E n) + 2 * ε' * μ.real K + ε' / ↑N * ∑ n, (|a| + y n + ε')
Module: Mathlib.MeasureTheory.Measure.FiniteMeasurePi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝² : Fintype ι
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → FiniteMeasure (α i)
β : ι → Type u_3
inst✝ : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → α i → β i
f_mble : ∀ (i : ι), AEMeasurable (f i) ↑(μ i)
⊢ ((pi μ).map fun x i ↦ f i (x i)) = pi fun i ↦ (μ i).map (f i)

Tactic:
apply Subtype.ext

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝² : Fintype ι
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → FiniteMeasure (α i)
β : ι → Type u_3
inst✝ : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → α i → β i
f_mble : ∀ (i : ι), AEMeasurable (f i) ↑(μ i)
⊢ ↑((pi μ).map fun x i ↦ f i (x i)) = ↑(pi fun i ↦ (μ i).map (f i))
Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric

Goal state before:
pp: Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : PseudoEMetricSpace Ω
inst✝² : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsProbabilityMeasure ν
δ : ℝ≥0∞
h : ∀ (ε : ℝ≥0∞) (B : Set Ω), δ < ε → ε < ∞ → MeasurableSet B → μ B ≤ ν (thickening ε.toReal B) + ε
⊢ levyProkhorovEDist μ ν ≤ δ

Tactic:
by
  apply levyProkhorovEDist_le_of_forall μ ν δ
  intro ε B ε_gt ε_lt_top B_mble
  refine ⟨h ε B ε_gt ε_lt_top B_mble, ?_⟩
  have B_subset := subset_compl_thickening_compl_thickening_self ε.toReal B
  apply (measure_mono (μ := ν) B_subset).trans
  rw [prob_compl_eq_one_sub isOpen_thickening.measurableSet]
  have Tc_mble := (isOpen_thickening (δ := ε.toReal) (E := B)).isClosed_compl.measurableSet
  specialize h ε (thickening ε.toReal B)ᶜ ε_gt ε_lt_top Tc_mble
  rw [prob_compl_eq_one_sub isOpen_thickening.measurableSet] at h
  have almost := add_le_add (c := μ (thickening ε.toReal B)) h rfl.le
  rw [tsub_add_cancel_of_le prob_le_one, add_assoc] at almost
  apply (tsub_le_tsub_right almost _).trans
  rw [ENNReal.add_sub_cancel_left (measure_ne_top ν _), add_comm ε]

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

Goal state before:
pp: Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : PseudoMetricSpace Ω
inst✝² : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : 0 ≤ᵐ[μ] ⇑f
key : (fun t ↦ μ.real {a | t ≤ f a}) ≤ fun t ↦ ν.real (thickening ε {a | t ≤ f a}) + ε
intble₁ : IntegrableOn (fun t ↦ μ.real {a | t ≤ f a}) (Ioc 0 ‖f‖) volume
t : ℝ
⊢ ν.real (thickening ε {a | t ≤ f a}) ≤ ν.real univ

Tactic:
exact ENNReal.toReal_mono (by finiteness) <| measure_mono (subset_univ _)

Goal state after: