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

Goal state before:
pp: case refine_1
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
h_mes : μ s ≠ 0
h_nemp : s.Nonempty
u : ℕ → ℝ≥0 := ⋯.choose
K : ConvexBody E := { carrier := s, convex' := h_conv, isCompact' := h_cpt, nonempty' := h_nemp }
S : ℕ → ConvexBody E := fun n ↦ (1 + u n) • K
Z : ℕ → Set E := fun n ↦ ↑(S n) ∩ (↑L \ {0})
h_zero : 0 ∈ K
h_clos : IsClosed (↑L \ {0})
n : ℕ
⊢ S (n + 1) ≤ S n

Tactic:
refine ConvexBody.smul_le_of_le K h_zero ?_

Goal state after:
case refine_1
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
h_mes : μ s ≠ 0
h_nemp : s.Nonempty
u : ℕ → ℝ≥0 := ⋯.choose
K : ConvexBody E := { carrier := s, convex' := h_conv, isCompact' := h_cpt, nonempty' := h_nemp }
S : ℕ → ConvexBody E := fun n ↦ (1 + u n) • K
Z : ℕ → Set E := fun n ↦ ↑(S n) ∩ (↑L \ {0})
h_zero : 0 ∈ K
h_clos : IsClosed (↑L \ {0})
n : ℕ
⊢ 1 + u (n + 1) ≤ 1 + u n
Module: Mathlib.Topology.ContinuousMap.CompactlySupported

Goal state before:
pp: case refine_1
α : Type u_2
inst✝ : TopologicalSpace α
f₁ f₂ : α →C_c ℝ≥0
h : f₁ ≤ f₂
⊢ closure (Function.support (f₂.toContinuousMap - f₁.toContinuousMap).toFun) ⊆
    closure (Function.support f₁.toFun) ∪ closure (Function.support f₂.toFun)

Tactic:
← closure_union

Goal state after:
case refine_1
α : Type u_2
inst✝ : TopologicalSpace α
f₁ f₂ : α →C_c ℝ≥0
h : f₁ ≤ f₂
⊢ closure (Function.support (f₂.toContinuousMap - f₁.toContinuousMap).toFun) ⊆
    closure (Function.support f₁.toFun ∪ Function.support f₂.toFun)
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 : E
t : ℝ
ω : E → E →L[𝕜] F
γab : Path a b
γbc : Path b c
ht₀ : 1 / 2 < t
⊢ 2 • curveIntegralFun ω γbc (1 - 2 * (1 - t)) = 2 • curveIntegralFun ω γbc (2 * t - 1)

Tactic:
congr 2

Goal state after:
case e_a.e_t
𝕜 : 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 : E
t : ℝ
ω : E → E →L[𝕜] F
γab : Path a b
γbc : Path b c
ht₀ : 1 / 2 < t
⊢ 1 - 2 * (1 - t) = 2 * t - 1
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 ∈ s, 0 ≤ g x
⊢ ∃ c ∈ s, ∫ (x : α) in s, f x * g x ∂μ = f c * ∫ (x : α) in s, g x ∂μ

Tactic:
have hg0_ae : ∀ᵐ x ∂(μ.restrict s), 0 ≤ g x := by
    rw [ae_restrict_iff' hs_meas]
    exact ae_of_all μ hg0

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 ∈ s, 0 ≤ g x
hg0_ae : ∀ᵐ (x : α) ∂μ.restrict s, 0 ≤ g x
⊢ ∃ c ∈ s, ∫ (x : α) in s, f x * g x ∂μ = f c * ∫ (x : α) in s, g x ∂μ
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
a : E
r : ℝ
hr : 0 ≤ r
hdf : ∀ᶠ (x : E) in 𝓝 a, DifferentiableAt ℝ f x
hderiv : fderiv ℝ f =O[𝓝 a] fun x ↦ ‖x - a‖ ^ r
C : ℝ
hC₀ : C > 0
hC : ∀ᶠ (x : E) in 𝓝 a, ‖fderiv ℝ f x‖ ≤ C * ‖‖x - a‖ ^ r‖
ε : ℝ
hε₀ : ε > 0
hε : ∀ y ∈ ball a ε, DifferentiableAt ℝ f y ∧ ‖fderiv ℝ f y‖ ≤ C * ‖‖y - a‖ ^ r‖
y : E
hy : y ∈ ball a ε
⊢ ‖f y - f a‖ ≤ C * ‖y - a‖ ^ r * ‖y - a‖

Tactic:
have hsub : closedBall a ‖y - a‖ ⊆ ball a ε :=
    closedBall_subset_ball (mem_ball_iff_norm.mp hy)

Goal state after:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
a : E
r : ℝ
hr : 0 ≤ r
hdf : ∀ᶠ (x : E) in 𝓝 a, DifferentiableAt ℝ f x
hderiv : fderiv ℝ f =O[𝓝 a] fun x ↦ ‖x - a‖ ^ r
C : ℝ
hC₀ : C > 0
hC : ∀ᶠ (x : E) in 𝓝 a, ‖fderiv ℝ f x‖ ≤ C * ‖‖x - a‖ ^ r‖
ε : ℝ
hε₀ : ε > 0
hε : ∀ y ∈ ball a ε, DifferentiableAt ℝ f y ∧ ‖fderiv ℝ f y‖ ≤ C * ‖‖y - a‖ ^ r‖
y : E
hy : y ∈ ball a ε
hsub : closedBall a ‖y - a‖ ⊆ ball a ε
⊢ ‖f y - f a‖ ≤ C * ‖y - a‖ ^ r * ‖y - a‖
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule

Goal state before:
pp: f : ℝ → ℝ
N : ℕ
N_nonzero : 0 < N
a b : ℝ
⊢ (b - a) / ↑N * ((f a + f b) / 2 + ∑ j ∈ Finset.range (N - 1), f (a + (↑(N - 1 - 1 - j) + 1) * (b - a) / ↑N)) =
    (b - a) / ↑N * ((f a + f b) / 2 + ∑ k ∈ Finset.range (N - 1), f (b + (↑k + 1) * (a - b) / ↑N))

Tactic:
congr 2

Goal state after:
case e_a.e_a
f : ℝ → ℝ
N : ℕ
N_nonzero : 0 < N
a b : ℝ
⊢ ∑ j ∈ Finset.range (N - 1), f (a + (↑(N - 1 - 1 - j) + 1) * (b - a) / ↑N) =
    ∑ k ∈ Finset.range (N - 1), f (b + (↑k + 1) * (a - b) / ↑N)
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule

Goal state before:
pp: f : ℝ → ℝ
N : ℕ
a h : ℝ
N_nonzero : 0 < N
⊢ ∑ x ∈ Finset.range N, (↑x + 1 - ↑x) * h / 2 * (f (a + ↑x * h) + f (a + (↑x + 1) * h)) =
    (a + ↑N * h - a) / ↑N *
      ((f a + f (a + ↑N * h)) / 2 + ∑ k ∈ Finset.range (N - 1), f (a + (↑k + 1) * (a + ↑N * h - a) / ↑N))

Tactic:
add_sub_cancel_left,

Goal state after:
f : ℝ → ℝ
N : ℕ
a h : ℝ
N_nonzero : 0 < N
⊢ ∑ x ∈ Finset.range N, 1 * h / 2 * (f (a + ↑x * h) + f (a + (↑x + 1) * h)) =
    ↑N * h / ↑N * ((f a + f (a + ↑N * h)) / 2 + ∑ x ∈ Finset.range (N - 1), f (a + (↑x + 1) * (↑N * h) / ↑N))
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
K₁ K₂ : Compacts X
h : K₁ ≤ K₂
⊢ rieszContentAux Λ K₁ ≤ rieszContentAux Λ K₂

Tactic:
by
  unfold rieszContentAux
  gcongr
  apply rieszContentAux_image_nonempty

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Card

Goal state before:
pp: α : Type u
s : Set (Set α)
i : Ordinal.{u_1}
f : ℕ → Set α
hf : ∀ (n : ℕ), ∃ j < i, f n ∈ generateMeasurableRec s j
⊢ ⋃ n, f n ∈ generateMeasurableRec s i

Tactic:
unfold generateMeasurableRec
  exact mem_union_right _ ⟨fun n => ⟨f n, let ⟨j, hj, hf⟩ := hf n; mem_iUnion₂.2 ⟨j, hj, hf⟩⟩, rfl⟩

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

Goal state before:
pp: 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 * π
θ : ℝ
x✝¹ : θ ∈ Icc 0 (2 * π)
Θ : Fin n → ℝ
x✝ : Θ ∈ Icc 0 fun x ↦ 2 * π
⊢ ((↑(R i) * cexp (↑θ * I) * I * ∏ x, ↑(R (i.succAbove x)) * cexp (↑(Θ x) * I) * I) •
      f fun i_1 ↦ c i_1 + ↑(R i_1) * cexp (↑(i.insertNth θ Θ i_1) * I)) =
    (↑(R i) * cexp (↑θ * I) * I * ∏ x, ↑(R (i.succAbove x)) * cexp (↑(Θ x) * I) * I) •
      f
        (i.insertNth (circleMap (c i) (R i) θ) fun i_1 ↦
          c (i.succAbove i_1) + ↑(R (i.succAbove i_1)) * cexp (↑(Θ i_1) * I))

Tactic:
congr 2

Goal state after:
case e_a
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 * π
θ : ℝ
x✝¹ : θ ∈ Icc 0 (2 * π)
Θ : Fin n → ℝ
x✝ : Θ ∈ Icc 0 fun x ↦ 2 * π
⊢ (fun i_1 ↦ c i_1 + ↑(R i_1) * cexp (↑(i.insertNth θ Θ i_1) * I)) =
    i.insertNth (circleMap (c i) (R i) θ) fun i_1 ↦ c (i.succAbove i_1) + ↑(R (i.succAbove i_1)) * cexp (↑(Θ i_1) * I)
Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
μ : Measure E
inst✝ : IsFiniteMeasure μ
n : ℕ
hint : MemLp id (↑n) μ
k : ℕ
hk : ↑k ≤ ↑n
⊢ Integrable (fun v ↦ ‖v‖ ^ k) μ

Tactic:
refine MemLp.integrable_norm_pow' (hint.mono_exponent (by simp_all))

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

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
μ : Measure E
inst✝ : IsFiniteMeasure μ
n : ℕ
t : E
hint : MemLp id (↑n) μ
x : Fin n → E
h : innerₗ E = ContinuousLinearMap.toLinearMap₁₂ (innerSL ℝ)
k : ℕ
hk : ↑k ≤ ↑n
⊢ Integrable (fun x ↦ ‖x‖ ^ k) μ

Tactic:
refine MemLp.integrable_norm_pow' (hint.mono_exponent (by simp_all))

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

Goal state before:
pp: X : Type u_1
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : OpensMeasurableSpace X
inst✝¹ : T0Space X
inst✝ : CompletelyRegularSpace X
μ : ↑(range diracProba)
F : Filter ↑(range diracProba)
⊢ Tendsto (⇑diracProbaEquiv.symm) F (𝓝 (diracProbaEquiv.symm μ)) ↔ Tendsto id F (𝓝 μ)

Tactic:
by
  have key :=
    tendsto_diracProba_iff_tendsto (F.map diracProbaEquiv.symm) (x := diracProbaEquiv.symm μ)
  rw [← (diracProbaEquiv (X := X)).symm_comp_self, ← tendsto_map'_iff] at key
  simp only [tendsto_map'_iff, map_map, Equiv.self_comp_symm, map_id] at key
  simp only [← key, diracProba_comp_diracProbaEquiv_symm_eq_val]
  convert! tendsto_subtype_rng.symm
  exact apply_rangeSplitting (fun x ↦ diracProba x) μ

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

Goal state before:
pp: Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoEMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ ν : Measure Ω
hLP : levyProkhorovEDist μ ν = 0
s : Set Ω
s_mble : MeasurableSet s
h_finite : ∃ δ > 0, ν (thickening δ s) ≠ ∞
key :
  Tendsto (fun ε ↦ ν (thickening ε.toReal s)) (𝓝[>] 0)
    (𝓝 (ν (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)))
obs :
  Tendsto (fun x ↦ ν (thickening x.toReal s) + x) (𝓝[>] 0)
    (𝓝 (ν (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)))
ε : ℝ≥0∞
ε_pos : ε ∈ Ioi 0
⊢ μ s ≤ ν (thickening ε.toReal s) + ε

Tactic:
exact left_measure_le_of_levyProkhorovEDist_lt (B_mble := s_mble) (hLP ▸ ε_pos)

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

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
β : Type u_2
inst✝ : MeasurableSpace β
μ : ProbabilityMeasure α
ν : ProbabilityMeasure β
⊢ (μ.prod ν).map ⋯ = μ

Tactic:
by
  apply Subtype.ext
  simp only [val_eq_to_measure, toMeasure_map, toMeasure_prod, Measure.map_fst_prod,
             measure_univ, one_smul]

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

Goal state before:
pp: Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
f : Ω →ᵇ ℝ
A : Set ℝ
A_finmeas : volume A ≠ ∞
μ : ProbabilityMeasure Ω
t : ℝ
⊢ Tendsto (fun a ↦ μ (thickening a {a | t ≤ f a})) (𝓝[>] 0) (𝓝 (μ {a | t ≤ f a}))

Tactic:
apply (ENNReal.tendsto_toNNReal _).comp

Goal state after:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
f : Ω →ᵇ ℝ
A : Set ℝ
A_finmeas : volume A ≠ ∞
μ : ProbabilityMeasure Ω
t : ℝ
⊢ Tendsto (fun a ↦ ↑μ (thickening a {a | t ≤ f a})) (𝓝[>] 0) (𝓝 (↑μ {a | t ≤ f a}))

Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
f : Ω →ᵇ ℝ
A : Set ℝ
A_finmeas : volume A ≠ ∞
μ : ProbabilityMeasure Ω
t : ℝ
⊢ ↑μ {a | t ≤ f a} ≠ ∞
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
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
a : ℝ × ℝ
ha : a ∈ U \ s'
⊢ HasFDerivAt g (g' a) a

Tactic:
exact (ContinuousLinearMap.apply ℝ F (1, 0)).hasFDerivAt.comp a (hdη a ha) |>.neg

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar

Goal state before:
pp: G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : MeasurableSpace G
inst✝² : BorelSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : LocallyCompactSpace G
φ ψ : G ≃ₜ* G
⊢ mulEquivHaarChar (ψ.trans φ) = haar.haarScalarFactor (map (⇑ψ) haar) * mulEquivHaarChar φ

Tactic:
mulEquivHaarChar_eq haar (ψ.trans φ)

Goal state after:
G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : MeasurableSpace G
inst✝² : BorelSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : LocallyCompactSpace G
φ ψ : G ≃ₜ* G
⊢ haar.haarScalarFactor (map (⇑(ψ.trans φ)) haar) = haar.haarScalarFactor (map (⇑ψ) haar) * mulEquivHaarChar φ
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
f g : CompactlySupportedContinuousMap B E
⊢ ∫ (c : C), ((H.pushforward μA) f + (H.pushforward μA) g) c ∂μC =
    ∫ (c : C), ((H.pushforward μA) f) c ∂μC + ∫ (c : C), ((H.pushforward μA) g) c ∂μC

Tactic:
exact integral_add (pushforward H μA f).integrable (pushforward H μA g).integrable

Goal state after:
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
b : B
hb : b ∈ U
⊢ (H.inducedMeasure μA μC) U ≠ 0

Tactic:
obtain ⟨K, hK, hb, hKU⟩ := exists_compact_subset hU hb

Goal state after:
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
b : B
hb✝ : b ∈ U
K : Set B
hK : IsCompact K
hb : b ∈ interior K
hKU : K ⊆ U
⊢ (H.inducedMeasure μA μC) U ≠ 0
Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric

Goal state before:
pp: Ω : 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}
B_subset : B ⊆ (⋃ i ∈ JB, thickening (ε / 3) (Es i)) ∪ (⋃ j ∈ Iio N, Es j)ᶜ
ω : Ω
ω_in_U : ∃ i ∈ JB, ω ∈ thickening (ε / 3) (Es i)
⊢ ω ∈ thickening δ B

Tactic:
obtain ⟨k, ⟨B_intersects, _⟩, ω_in_thEk⟩ := ω_in_U

Goal state after:
Ω : 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}
B_subset : B ⊆ (⋃ i ∈ JB, thickening (ε / 3) (Es i)) ∪ (⋃ j ∈ Iio N, Es j)ᶜ
ω : Ω
k : ℕ
ω_in_thEk : ω ∈ thickening (ε / 3) (Es k)
B_intersects : (B ∩ Es k).Nonempty
right✝ : k ∈ Iio N
⊢ ω ∈ thickening δ B
Module: Mathlib.MeasureTheory.Measure.Prokhorov

Goal state before:
pp: case h
E : Type u_1
inst✝⁴ : MeasurableSpace E
inst✝³ : TopologicalSpace E
inst✝² : T2Space E
inst✝¹ : BorelSpace E
inst✝ : CompactSpace E
C : ℝ≥0
f : Ultrafilter (FiniteMeasure E)
hf : {μ | μ.mass ≤ C} ∈ f
Λ : (E →C_c ℝ) → ℝ
h₀Λ : ∀ (g : E →C_c ℝ), Λ g ∈ Icc (-↑C * ‖g.toBoundedContinuousFunction‖) (↑C * ‖g.toBoundedContinuousFunction‖)
hΛ : ∀ (g : E →C_c ℝ), Tendsto (fun μ ↦ ∫ (x : E), g x ∂↑μ) (↑f) (𝓝 (Λ g))
Λ' : (E →C_c ℝ) →ₚ[ℝ] ℝ := ⋯
μlim : Measure E := ⋯
o : E →C_c ℝ := ⋯
this : μlim univ ≤ ENNReal.ofReal (Λ' o)
⊢ Λ' o ≤ ↑C

Tactic:
apply le_of_tendsto (hΛ o)

Goal state after:
case h
E : Type u_1
inst✝⁴ : MeasurableSpace E
inst✝³ : TopologicalSpace E
inst✝² : T2Space E
inst✝¹ : BorelSpace E
inst✝ : CompactSpace E
C : ℝ≥0
f : Ultrafilter (FiniteMeasure E)
hf : {μ | μ.mass ≤ C} ∈ f
Λ : (E →C_c ℝ) → ℝ
h₀Λ : ∀ (g : E →C_c ℝ), Λ g ∈ Icc (-↑C * ‖g.toBoundedContinuousFunction‖) (↑C * ‖g.toBoundedContinuousFunction‖)
hΛ : ∀ (g : E →C_c ℝ), Tendsto (fun μ ↦ ∫ (x : E), g x ∂↑μ) (↑f) (𝓝 (Λ g))
Λ' : (E →C_c ℝ) →ₚ[ℝ] ℝ := ⋯
μlim : Measure E := ⋯
o : E →C_c ℝ := ⋯
this : μlim univ ≤ ENNReal.ofReal (Λ' o)
⊢ ∀ᶠ (c : FiniteMeasure E) in ↑f, ∫ (x : E), o x ∂↑c ≤ ↑C