mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Independence.Kernel.IndepFun

Goal state before:
pp: α : Type u_1
Ω : Type u_2
ι : Type u_3
β : Type u_4
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
mβ : MeasurableSpace β
X : ι → Ω → α
Y : ι → Ω → β
f : ι → Set Ω
t : ι → Set β
s : Finset ι
inst✝ : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (fun i ω ↦ (X i ω, Y i ω)) κ μ
hf : ∀ i ∈ s, MeasurableSet (f i)
hy✝ : ∀ᵐ (a : α) ∂μ, ∀ i ∉ s, (κ a) (Y i ⁻¹' t i) ≠ 0
ht : ∀ (i : ι), MeasurableSet (t i)
val✝ : Fintype ι
g : ι → Set Ω := fun i' ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
hYt✝ : ∀ (i : ι), MeasurableSet (Y i ⁻¹' t i)
hg✝ : ∀ (i : ι), MeasurableSet (g i)
a : α
hy : ∀ i ∉ s, (κ a) (Y i ⁻¹' t i) ≠ 0
a✝ : IsProbabilityMeasure (κ a)
hYt : (κ a) (⋂ i, Y i ⁻¹' t i) = ∏ i, (κ a) (Y i ⁻¹' t i)
hg : (κ a) (⋂ i, g i) = ∏ i, (κ a) (g i)
⊢ (∏ i, (κ a) (Y i ⁻¹' t i))⁻¹ * ∏ i, (κ a) (g i) = ∏ i, ((κ a) (Y i ⁻¹' t i))⁻¹ * (κ a) (g i)

Tactic:
rw [Finset.prod_mul_distrib, ENNReal.prod_inv_distrib]

Goal state after:
α : Type u_1
Ω : Type u_2
ι : Type u_3
β : Type u_4
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
mβ : MeasurableSpace β
X : ι → Ω → α
Y : ι → Ω → β
f : ι → Set Ω
t : ι → Set β
s : Finset ι
inst✝ : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (fun i ω ↦ (X i ω, Y i ω)) κ μ
hf : ∀ i ∈ s, MeasurableSet (f i)
hy✝ : ∀ᵐ (a : α) ∂μ, ∀ i ∉ s, (κ a) (Y i ⁻¹' t i) ≠ 0
ht : ∀ (i : ι), MeasurableSet (t i)
val✝ : Fintype ι
g : ι → Set Ω := fun i' ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
hYt✝ : ∀ (i : ι), MeasurableSet (Y i ⁻¹' t i)
hg✝ : ∀ (i : ι), MeasurableSet (g i)
a : α
hy : ∀ i ∉ s, (κ a) (Y i ⁻¹' t i) ≠ 0
a✝ : IsProbabilityMeasure (κ a)
hYt : (κ a) (⋂ i, Y i ⁻¹' t i) = ∏ i, (κ a) (Y i ⁻¹' t i)
hg : (κ a) (⋂ i, g i) = ∏ i, (κ a) (g i)
⊢ (↑Finset.univ).Pairwise fun i j ↦ (κ a) (Y i ⁻¹' t i) ≠ 0 ∨ (κ a) (Y j ⁻¹' t j) ≠ ⊤
Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution

Goal state before:
pp: case refine_1
ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω'' : Type u_4
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst✝⁸ : IsProbabilityMeasure μ'
m'' : MeasurableSpace Ω''
μ'' : Measure Ω''
inst✝⁷ : IsProbabilityMeasure μ''
mE : MeasurableSpace E
l : Filter ι
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : SecondCountableTopology E
inst✝⁴ : BorelSpace E
E' : Type u_6
mE' : MeasurableSpace E'
inst✝³ : SeminormedAddCommGroup E'
inst✝² : SecondCountableTopology E'
inst✝¹ : BorelSpace E'
inst✝ : l.IsCountablyGenerated
X : ι → Ω'' → E
Y : ι → Ω'' → E'
Z : Ω' → E
c : E'
hXZ : TendstoInDistribution X l Z (fun x ↦ μ'') μ'
hY : TendstoInMeasure μ'' Y l fun x ↦ c
hY_meas : ∀ (i : ι), AEMeasurable (Y i) μ''
hX : ∀ (i : ι), AEMeasurable (X i) μ''
⊢ TendstoInDistribution (fun n ω ↦ (X n ω, c)) l (fun ω ↦ (Z ω, c)) (fun x ↦ μ'') μ'

Tactic:
exact hXZ.continuous_comp (g := fun x ↦ (x, c)) (by fun_prop)

Goal state after:
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✝¹ : TopologicalSpace β
inst✝ : Zero β
f g : α →C_c β
h : (fun f ↦ f.toFun) f = (fun f ↦ f.toFun) g
⊢ f = g

Tactic:
obtain ⟨⟨_, _⟩, _⟩ := f

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
g : α →C_c β
toFun✝ : α → β
continuous_toFun✝ : Continuous toFun✝
hasCompactSupport'✝ : HasCompactSupport { toFun := toFun✝, continuous_toFun := continuous_toFun✝ }.toFun
h :
  (fun f ↦ f.toFun)
      { toFun := toFun✝, continuous_toFun := continuous_toFun✝, hasCompactSupport' := hasCompactSupport'✝ } =
    (fun f ↦ f.toFun) g
⊢ { toFun := toFun✝, continuous_toFun := continuous_toFun✝, hasCompactSupport' := hasCompactSupport'✝ } = g
Module: Mathlib.Topology.ContinuousMap.CompactlySupported

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : Zero β
γ : Type u_5
inst✝¹ : TopologicalSpace γ
inst✝ : Zero γ
g : C(β, γ)
hg : g 0 = 0
f : α →C_c β
a : α
⊢ (compLeft g f) a = g (f a)

Tactic:
by simp [coe_compLeft hg f]

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 : E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℝ F
ω : E → E →L[𝕜] F
γ : Path a b
x : ℝ
hx : x ∈ Ioo 0 1
⊢ (ω (γ.extend x)) (derivWithin ⇑γ.extend I x) = (ω (γ.extend x)) (deriv (⇑γ.extend) x)

Tactic:
rw [derivWithin_of_mem_nhds (by simpa)]

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 : E
ω : E → E →L[𝕜] F
γab : Path a b
h : CurveIntegrable ω γab
γbc : Path b c
⊢ IntervalIntegrable (curveIntegralFun ω (γab.trans γbc)) volume 0 (1 / 2)

Tactic:
refine .congr_ae ?_ (curveIntegralFun_trans_aeeq_left _ _ _).symm
  simpa [ofNat_smul_eq_nsmul] using! h.comp_mul_left.smul (2 : 𝕜)

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
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℝ F
ω : E → E →L[𝕜] F
a b : E
⊢ ∫ᶜ (x : E) in Path.segment a b, ω x = ∫ (t : ℝ) in 0..1, (ω ((lineMap a b) t)) (b - a)

Tactic:
rw [curveIntegral_def]
  refine intervalIntegral.integral_congr fun t ht ↦ ?_
  rw [uIcc_of_le zero_le_one] at ht
  exact curveIntegralFun_segment ω a b ht

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

Goal state before:

Tactic:
_ ≤ ∑ k ∈ range N, ζ / 12 * h ^ 3 := sum_le_sum this
      _ = N * (ζ / 12 * h ^ 3)          := by simp [sum_const]
      _ = _                             := by push_cast; field

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 : ℝ) in Icc 0 (2 * π),
      ∫ (y : Fin n → ℝ) in Icc 0 fun x ↦ 2 * π,
        (∏ i, ↑(R i) * cexp (↑(e (x, y) i) * I) * I) • f (torusMap c R (e (x, y))) =
    ∮ (x : ℂ) in C(c i, R i), ∯ (y : Fin n → ℂ) in T(c ∘ i.succAbove, R ∘ i.succAbove), f (i.insertNth x y)

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

Goal state after:
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 : ℝ) in Icc 0 (2 * π),
      ∫ (y : Fin n → ℝ) in Icc 0 fun x ↦ 2 * π,
        (∏ i, ↑(R i) * cexp (↑(e (x, y) i) * I) * I) • f (torusMap c R (e (x, y))) =
    ∫ (θ : ℝ) in Icc 0 (2 * π),
      deriv (circleMap (c i) (R i)) θ •
        ∯ (y : Fin n → ℂ) in T(c ∘ i.succAbove, R ∘ i.succAbove), f (i.insertNth (circleMap (c i) (R i) θ) y)

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)
Module: Mathlib.MeasureTheory.MeasurableSpace.Card

Goal state before:
pp: α : Type u
s : Set (Set α)
i : Ordinal.{v}
⊢ #↑(generateMeasurableRec s i) ≤ max (#↑s) 2 ^ ℵ₀

Tactic:
suffices ∀ i ≤ ω₁, #(generateMeasurableRec s i) ≤ max #s 2 ^ ℵ₀ by
    obtain hi | hi := le_or_gt i ω₁
    · exact this i hi
    · rw [generateMeasurableRec_of_omega_one_le s hi.le]
      exact this _ le_rfl

Goal state after:
α : Type u
s : Set (Set α)
i : Ordinal.{v}
⊢ ∀ i ≤ ω_ 1, #↑(generateMeasurableRec s i) ≤ max (#↑s) 2 ^ ℵ₀
Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real

Goal state before:
pp: a' b' ε : ℝ
hε : 0 < ε
⊢ Tendsto (fun N ↦ a' / N * (b' + a' / N)) atTop (𝓝 (0 * (b' + 0)))

Tactic:
apply Tendsto.mul

Goal state after:
case hf
a' b' ε : ℝ
hε : 0 < ε
⊢ Tendsto (HDiv.hDiv a') atTop (𝓝 0)

case hg
a' b' ε : ℝ
hε : 0 < ε
⊢ Tendsto (fun x ↦ b' + a' / x) atTop (𝓝 (b' + 0))
Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic

Goal state before:
pp: case refine_1
E : Type u_3
inst✝⁷ : MeasurableSpace E
μ ν : Measure E
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : BorelSpace E
inst✝³ : SecondCountableTopology E
inst✝² : CompleteSpace E
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : ∀ (x : E), ∫ (v : E), (innerProbChar x) v ∂μ = ∫ (v : E), (innerProbChar x) v ∂ν
⊢ ∀ (v : E), v ≠ 0 → (innerₗ E) v ≠ 0

Tactic:
exact fun v hv ↦ DFunLike.ne_iff.mpr ⟨v, inner_self_ne_zero.mpr hv⟩

Goal state after:
Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real

Goal state before:
pp: 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)
x : X
⊢ 0 ≤ (∑ n, g n) x

Tactic:
simpa using Fintype.sum_nonneg fun n ↦ (hg.2.2.1 n x).1

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

Goal state before:
pp: case mp
X : Type u_1
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
inst✝ : CompletelyRegularSpace X
x : X
L : Filter X
⊢ ¬Tendsto id L (𝓝 x) → ¬Tendsto diracProba L (𝓝 (diracProba x))

Tactic:
exact not_tendsto_diracProba_of_not_tendsto L

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝⁵ : Fintype ι
inst✝⁴ : (i : ι) → MeasurableSpace (α i)
inst✝³ : (i : ι) → TopologicalSpace (α i)
inst✝² : ∀ (i : ι), SecondCountableTopology (α i)
inst✝¹ : ∀ (i : ι), PseudoMetrizableSpace (α i)
inst✝ : ∀ (i : ι), OpensMeasurableSpace (α i)
μ : (i : ι) → ProbabilityMeasure (α i)
⊢ ContinuousAt (fun μ ↦ pi μ) μ

Tactic:
let S : Set (Set (Π i, α i)) := {t | ∃ (s : Π i, Set (α i)), t = univ.pi s ∧
    (∀ i, MeasurableSet (s i)) ∧ (∀ i, μ i (frontier (s i)) = 0)}

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝⁵ : Fintype ι
inst✝⁴ : (i : ι) → MeasurableSpace (α i)
inst✝³ : (i : ι) → TopologicalSpace (α i)
inst✝² : ∀ (i : ι), SecondCountableTopology (α i)
inst✝¹ : ∀ (i : ι), PseudoMetrizableSpace (α i)
inst✝ : ∀ (i : ι), OpensMeasurableSpace (α i)
μ : (i : ι) → ProbabilityMeasure (α i)
S : Set (Set ((i : ι) → α i)) :=
  {t | ∃ s, t = univ.pi s ∧ (∀ (i : ι), MeasurableSet (s i)) ∧ ∀ (i : ι), (μ i) (frontier (s i)) = 0}
⊢ ContinuousAt (fun μ ↦ pi μ) μ
Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric

Goal state before:
pp: case neg
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μs : ℕ → LevyProkhorov (ProbabilityMeasure Ω)
ν : LevyProkhorov (ProbabilityMeasure Ω)
hμs : Tendsto μs atTop (𝓝 ν)
P : ProbabilityMeasure Ω := ν.toMeasure
Ps : ℕ → ProbabilityMeasure Ω := toMeasure ∘ μs
f✝ f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
f_zero : ¬‖f‖ = 0
norm_f_pos : 0 < ‖f‖
δ : ℝ
δ_pos : 0 < δ
εs : ℕ → ℝ
left✝ : StrictAnti εs
εs_pos : ∀ (n : ℕ), 0 < εs n
εs_lim : Tendsto εs atTop (𝓝 0)
⊢ ∀ᶠ (n : ℕ) in atTop, ∫ (x : Ω), f x ∂↑(Ps n) ≤ ∫ (x : Ω), f x ∂↑P + δ

Tactic:
have ε_of_room := Tendsto.add (tendsto_iff_dist_tendsto_zero.mp hμs) εs_lim

Goal state after:
case neg
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μs : ℕ → LevyProkhorov (ProbabilityMeasure Ω)
ν : LevyProkhorov (ProbabilityMeasure Ω)
hμs : Tendsto μs atTop (𝓝 ν)
P : ProbabilityMeasure Ω := ν.toMeasure
Ps : ℕ → ProbabilityMeasure Ω := toMeasure ∘ μs
f✝ f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
f_zero : ¬‖f‖ = 0
norm_f_pos : 0 < ‖f‖
δ : ℝ
δ_pos : 0 < δ
εs : ℕ → ℝ
left✝ : StrictAnti εs
εs_pos : ∀ (n : ℕ), 0 < εs n
εs_lim : Tendsto εs atTop (𝓝 0)
ε_of_room : Tendsto (fun x ↦ dist (μs x) ν + εs x) atTop (𝓝 (0 + 0))
⊢ ∀ᶠ (n : ℕ) in atTop, ∫ (x : Ω), f x ∂↑(Ps n) ≤ ∫ (x : Ω), f x ∂↑P + δ
Module: Mathlib.Topology.Algebra.Group.Extension

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
H : Subgroup G
inst✝ : H.Normal
hH : IsClosed ↑H
⊢ Function.MulExact ⇑H.subtype ⇑(QuotientGroup.mk' H)

Tactic:
simp [Function.MulExact]

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

Goal state before:
pp: G : Type u_1
A : Type u_2
inst✝¹⁰ : Group G
inst✝⁹ : AddCommGroup A
inst✝⁸ : DistribMulAction G A
inst✝⁷ : TopologicalSpace A
inst✝⁶ : IsTopologicalAddGroup A
inst✝⁵ : LocallyCompactSpace A
inst✝⁴ : ContinuousConstSMul G A
inst✝³ : MeasurableSpace A
inst✝² : BorelSpace A
μ : Measure A
inst✝¹ : μ.IsAddHaarMeasure
inst✝ : μ.Regular
s : Set A
hs₀ : μ s ≠ 0
hs : μ s ≠ ∞
g : G
⊢ ↑((distribHaarChar A) g) = μ (g • s) / μ s

Tactic:
rw [← distribHaarChar_mul, ENNReal.mul_div_cancel_right] <;> simp [*]

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 φ.symm = (mulEquivHaarChar φ)⁻¹

Tactic:
symm
  apply inv_eq_of_mul_eq_one_right
  simp [← mulEquivHaarChar_trans]

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

Goal state before:
pp: case refine_2
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 ℝ) →ₚ[ℝ] ℝ := { toFun := Λ, map_add' := ⋯, map_smul' := ⋯, monotone' := ⋯ }
μlim : Measure E := RealRMK.rieszMeasure Λ'
μlim_le : μlim univ ≤ ENNReal.ofReal ↑C
μlim' : FiniteMeasure E := ⟨μlim, ⋯⟩
⊢ Tendsto id (↑f) (𝓝 μlim')

Tactic:
apply FiniteMeasure.tendsto_of_forall_integral_tendsto (fun g ↦ ?_)

Goal state after:
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 ℝ) →ₚ[ℝ] ℝ := { toFun := Λ, map_add' := ⋯, map_smul' := ⋯, monotone' := ⋯ }
μlim : Measure E := RealRMK.rieszMeasure Λ'
μlim_le : μlim univ ≤ ENNReal.ofReal ↑C
μlim' : FiniteMeasure E := ⟨μlim, ⋯⟩
g : E →ᵇ ℝ
⊢ Tendsto (fun i ↦ ∫ (x : E), g x ∂↑(id i)) (↑f) (𝓝 (∫ (x : E), g x ∂↑μlim'))
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
C : ℝ≥0
K : Set E
hK : IsCompact K
f : ↑K → E := Subtype.val
hf : IsClosedEmbedding f
rf : range f = K
F : FiniteMeasure ↑K → FiniteMeasure E := fun μ ↦ μ.map f
T : Set (FiniteMeasure ↑K) := {μ | μ.mass ≤ C}
μ : FiniteMeasure E
hμ : μ ∈ {μ | μ.mass ≤ C ∧ μ Kᶜ = 0}
s : Set E
hs : MeasurableSet s
⊢ ↑μ (s ∩ range Subtype.val) = ↑μ s

Tactic:
rw [← Measure.restrict_apply hs, Measure.restrict_eq_self_of_ae_mem]

Goal state after:
case h₁.hs
E : Type u_1
inst✝³ : MeasurableSpace E
inst✝² : TopologicalSpace E
inst✝¹ : T2Space E
inst✝ : BorelSpace E
C : ℝ≥0
K : Set E
hK : IsCompact K
f : ↑K → E := Subtype.val
hf : IsClosedEmbedding f
rf : range f = K
F : FiniteMeasure ↑K → FiniteMeasure E := fun μ ↦ μ.map f
T : Set (FiniteMeasure ↑K) := {μ | μ.mass ≤ C}
μ : FiniteMeasure E
hμ : μ ∈ {μ | μ.mass ≤ C ∧ μ Kᶜ = 0}
s : Set E
hs : MeasurableSet s
⊢ ∀ᵐ (x : E) ∂↑μ, x ∈ range Subtype.val
Module: Mathlib.MeasureTheory.Measure.TightNormed

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

Tactic:
gcongr with μ hμS

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

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

Tactic:
gcongr with μ hμS

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

Goal state before:
pp: E : Type u_1
mE : MeasurableSpace E
inst✝⁵ : NormedAddCommGroup E
𝕜 : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : BorelSpace E
μ : ℕ → Measure E
inst✝ : ∀ (i : ℕ), IsFiniteMeasure (μ i)
h : ∀ (y : E), ‖y‖ = 1 → Tendsto (fun r ↦ limsup (fun n ↦ (μ n).real {x | r < ‖⟪y, x⟫_𝕜‖}) atTop) atTop (𝓝 0)
C : ℝ≥0
hμ : ∀ᶠ (n : ℕ) in atTop, (μ n) Set.univ ≤ ↑C
z : E
hz : ‖z‖ = 1
r : ℝ
n : ℕ
⊢ (μ n) Set.univ ≤ ↑C → (μ n) {x | r < ‖⟪z, x⟫_𝕜‖} ≤ ↑C

Tactic:
hμn

Goal state after:
E : Type u_1
mE : MeasurableSpace E
inst✝⁵ : NormedAddCommGroup E
𝕜 : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : BorelSpace E
μ : ℕ → Measure E
inst✝ : ∀ (i : ℕ), IsFiniteMeasure (μ i)
h : ∀ (y : E), ‖y‖ = 1 → Tendsto (fun r ↦ limsup (fun n ↦ (μ n).real {x | r < ‖⟪y, x⟫_𝕜‖}) atTop) atTop (𝓝 0)
C : ℝ≥0
hμ : ∀ᶠ (n : ℕ) in atTop, (μ n) Set.univ ≤ ↑C
z : E
hz : ‖z‖ = 1
r : ℝ
n : ℕ
hμn : (μ n) Set.univ ≤ ↑C
⊢ (μ n) {x | r < ‖⟪z, x⟫_𝕜‖} ≤ ↑C
Module: Mathlib.MeasureTheory.Measure.PreVariation

Goal state before:
pp: X : Type u_1
inst✝ : MeasurableSpace X
f : Set X → ℝ≥0∞
s : ℕ → Set X
hs : ∀ (i : ℕ), MeasurableSet (s i)
hs' : Pairwise (Disjoint on s)
P : (i : ℕ) → Finpartition ⟨s i, ⋯⟩
n : ℕ
⊢ ∑ i ∈ Finset.range n, ∑ p ∈ (P i).parts, f ↑p ≤ preVariationFun f (⋃ i, s i)

Tactic:
let s' (i : ℕ) : Subtype MeasurableSet := ⟨s i, hs i⟩
  have hs_disj : Set.PairwiseDisjoint (Finset.range n : Set ℕ) s' := fun i _ j _ hij => by
    simp only [Function.onFun, disjoint_iff, Subtype.ext_iff]
    exact Set.disjoint_iff_inter_eq_empty.mp (hs' hij)
  let Q := Finpartition.combine P hs_disj.supIndep
  have hQ_le : (Finset.range n).sup s' ≤ ⟨⋃ i, s i, MeasurableSet.iUnion hs⟩ := by
    rw [← Subtype.coe_le_coe, Finset.sup_coe (Psup := by measurability), Finset.sup_set_eq_biUnion]
    exact Set.iUnion₂_subset fun i _ => Set.subset_iUnion s i
  let R := Q.extendOfLE hQ_le
  calc ∑ i ∈ Finset.range n, ∑ p ∈ (P i).parts, f p
    _ = ∑ p ∈ Q.parts, f p := (Finpartition.sum_combine P hs_disj.supIndep (fun p => f p)).symm
    _ ≤ ∑ p ∈ R.parts, f p := Finset.sum_le_sum_of_subset (Q.parts_subset_extendOfLE hQ_le)
    _ ≤ preVariationFun f (⋃ i, s i) := sum_le f (MeasurableSet.iUnion hs) R

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

Goal state before:
pp: case inr
X : Type u_1
E : Type u_2
m : MeasurableSpace X
inst✝ : NormedAddCommGroup E
μ : Measure X
p : ℝ≥0∞
one_le_p : Fact (1 ≤ p)
p_ne_top : Fact (p ≠ ∞)
𝒜 : Set (Set X)
h𝒜 : μ.MeasureDense 𝒜
c : E
hc : c ≠ 0
p_pos : 0 < p
s : Set X
ms : MeasurableSet s
hμs : μ s ≠ ∞
ε : ℝ
hε : ε > 0
aux : 0 < (ε / ‖c‖) ^ p.toReal
t : Set X
ht : t ∈ 𝒜
hμt : μ t ≠ ∞
hμst : μ (s ∆ t) < ENNReal.ofReal ((ε / ‖c‖) ^ p.toReal)
⊢ ‖indicatorConstLp p ⋯ ⋯ c‖ < ε

Tactic:
norm_indicatorConstLp p_pos.ne.symm p_ne_top.elim

Goal state after:
case inr
X : Type u_1
E : Type u_2
m : MeasurableSpace X
inst✝ : NormedAddCommGroup E
μ : Measure X
p : ℝ≥0∞
one_le_p : Fact (1 ≤ p)
p_ne_top : Fact (p ≠ ∞)
𝒜 : Set (Set X)
h𝒜 : μ.MeasureDense 𝒜
c : E
hc : c ≠ 0
p_pos : 0 < p
s : Set X
ms : MeasurableSet s
hμs : μ s ≠ ∞
ε : ℝ
hε : ε > 0
aux : 0 < (ε / ‖c‖) ^ p.toReal
t : Set X
ht : t ∈ 𝒜
hμt : μ t ≠ ∞
hμst : μ (s ∆ t) < ENNReal.ofReal ((ε / ‖c‖) ^ p.toReal)
⊢ ‖c‖ * μ.real (s ∆ t) ^ (1 / p.toReal) < ε
Module: Mathlib.MeasureTheory.Measure.SubFinite

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν ξ : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
⊢ μ - ν ≤ ξ ↔ μ ≤ ξ + ν

Tactic:
refine ⟨fun h ↦ ?_, sub_le_of_le_add⟩

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ ν ξ : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : μ - ν ≤ ξ
⊢ μ ≤ ξ + ν