mathlib-initiative/mathlib-tactics huggingface dataset:
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 : α →C_c β
f' : α → β
h : f' = ⇑f
⊢ HasCompactSupport f'

Tactic:
simp_rw [h]

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
f : α →C_c β
f' : α → β
h : f' = ⇑f
⊢ HasCompactSupport ⇑f
Module: Mathlib.Topology.ContinuousMap.CompactlySupported

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : TopologicalSpace α
Λ : (α →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
f g : α →C_c ℝ
h : α →C_c ℝ≥0
hh : (f + g).nnrealPart + h = f.nnrealPart + g.nnrealPart ∧ (-f + -g).nnrealPart + h = (-f).nnrealPart + (-g).nnrealPart
⊢ ↑(Λ (f.nnrealPart + g.nnrealPart)) - ↑(Λ ((-f).nnrealPart + (-g).nnrealPart)) =
    ↑(Λ f.nnrealPart) - ↑(Λ (-f).nnrealPart) + (↑(Λ g.nnrealPart) - ↑(Λ (-g).nnrealPart))

Tactic:
simp only [map_add, NNReal.coe_add]

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : TopologicalSpace α
Λ : (α →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
f g : α →C_c ℝ
h : α →C_c ℝ≥0
hh : (f + g).nnrealPart + h = f.nnrealPart + g.nnrealPart ∧ (-f + -g).nnrealPart + h = (-f).nnrealPart + (-g).nnrealPart
⊢ ↑(Λ f.nnrealPart) + ↑(Λ g.nnrealPart) - (↑(Λ (-f).nnrealPart) + ↑(Λ (-g).nnrealPart)) =
    ↑(Λ f.nnrealPart) - ↑(Λ (-f).nnrealPart) + (↑(Λ g.nnrealPart) - ↑(Λ (-g).nnrealPart))
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
γbc : Path b c
⊢ curveIntegralFun ω (γab.trans γbc) =ᵐ[volume.restrict (Ι 0 (1 / 2))] fun t ↦ 2 • curveIntegralFun ω γab (2 * t)

Tactic:
rw [uIoc_of_le (by positivity), ← restrict_Ioo_eq_restrict_Ioc]
  filter_upwards [ae_restrict_mem measurableSet_Ioo] with t ⟨ht₀, ht⟩
  exact curveIntegralFun_trans_of_lt_half ω γab γbc ht

Goal state after:
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 : Compacts X
V : Set X
hVcp : IsCompact V
hKsubintV : K.carrier ⊆ interior V
⊢ closure (interior V) ⊆ closure V

Tactic:
exact closure_mono interior_subset

Goal state after:
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
disj : Disjoint ↑K₁ ↑K₂
b : ℝ≥0
f : X →C_c ℝ≥0
hf : f ∈ {f | ∀ x ∈ K₁ ⊔ K₂, 1 ≤ f x}
Λf_eq_b : Λ f = b
hsuppf : ∀ x ∈ K₁ ⊔ K₂, x ∈ support ⇑f
hsubsuppf : ↑K₁ ∪ ↑K₂ ⊆ tsupport ⇑f
g₁ g₂ : X →C_c ℝ≥0
hg₁ : EqOn (⇑g₁) 1 K₁.carrier
hg₂ : EqOn (⇑g₂) 1 K₂.carrier
sum_g : EqOn (⇑(g₁ + g₂)) 1 (tsupport f.toFun)
f_eq_sum : f = g₁ * f + g₂ * f
⊢ rieszContentAux Λ K₁ + rieszContentAux Λ K₂ ≤ b

Tactic:
rw [← Λf_eq_b, f_eq_sum, map_add]

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
K₁ K₂ : Compacts X
disj : Disjoint ↑K₁ ↑K₂
b : ℝ≥0
f : X →C_c ℝ≥0
hf : f ∈ {f | ∀ x ∈ K₁ ⊔ K₂, 1 ≤ f x}
Λf_eq_b : Λ f = b
hsuppf : ∀ x ∈ K₁ ⊔ K₂, x ∈ support ⇑f
hsubsuppf : ↑K₁ ∪ ↑K₂ ⊆ tsupport ⇑f
g₁ g₂ : X →C_c ℝ≥0
hg₁ : EqOn (⇑g₁) 1 K₁.carrier
hg₂ : EqOn (⇑g₂) 1 K₂.carrier
sum_g : EqOn (⇑(g₁ + g₂)) 1 (tsupport f.toFun)
f_eq_sum : f = g₁ * f + g₂ * f
⊢ rieszContentAux Λ K₁ + rieszContentAux Λ K₂ ≤ Λ (g₁ * f) + Λ (g₂ * f)
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 : Compacts X
⊢ (∀ (i : Compacts X), ↑K ⊆ interior ↑i → rieszContentAux Λ K ≤ rieszContentAux Λ i) ∧
    ⨅ K', ⨅ (_ : ↑K ⊆ interior ↑K'), ↑(rieszContentAux Λ K') ≤ ↑(rieszContentAux Λ K)

Tactic:
refine ⟨fun K' hK' ↦ rieszContentAux_mono Λ (hK'.trans interior_subset), ?_⟩

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
K : Compacts X
⊢ ⨅ K', ⨅ (_ : ↑K ⊆ interior ↑K'), ↑(rieszContentAux Λ K') ≤ ↑(rieszContentAux Λ K)
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 : Compacts X
b : ℝ≥0∞
hb : ∀ (i : Compacts X), b ≤ ⨅ (_ : ↑K ⊆ interior ↑i), ↑(rieszContentAux Λ i)
this : b < ∞
ε : ℝ≥0
hε : 0 < ↑ε
f : X →C_c ℝ≥0
hfleoneonK : ∀ x ∈ K, 1 ≤ f x
hfle : ↑(Λ f) < ↑(sInf (⇑Λ '' {f | ∀ x ∈ K, 1 ≤ f x}) + NNReal.mk ↑ε ⋯)
α : ℝ≥0
hα : 1 < α
⊢ b.toNNReal ≤ Λ (α • f)

Tactic:
set K' := f ⁻¹' Ici α⁻¹

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
K : Compacts X
b : ℝ≥0∞
hb : ∀ (i : Compacts X), b ≤ ⨅ (_ : ↑K ⊆ interior ↑i), ↑(rieszContentAux Λ i)
this : b < ∞
ε : ℝ≥0
hε : 0 < ↑ε
f : X →C_c ℝ≥0
hfleoneonK : ∀ x ∈ K, 1 ≤ f x
hfle : ↑(Λ f) < ↑(sInf (⇑Λ '' {f | ∀ x ∈ K, 1 ≤ f x}) + NNReal.mk ↑ε ⋯)
α : ℝ≥0
hα : 1 < α
K' : Set X := ⇑f ⁻¹' Ici α⁻¹
⊢ b.toNNReal ≤ Λ (α • f)
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_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)
this :
  (((∫ (x : ℝ) in 0..1, g (x, 1)) - ∫ (x : ℝ) in 0..1, g (x, 0)) + ∫ (y : ℝ) in 0..1, f (1, y)) -
      ∫ (y : ℝ) in 0..1, f (0, y) =
    0
hfi :
  ∀ (s : ↑I),
    ∫ (t : ℝ) in 0..1, f (↑s, t) = ∫ᶜ (x : E) in { toContinuousMap := φ.curry s, source' := ⋯, target' := ⋯ }, ω x
hf₀ : ∫ (t : ℝ) in 0..1, f (0, t) = ∫ᶜ (x : E) in γ₁, ω x
hf₁ : ∫ (t : ℝ) in 0..1, f (1, t) = curveIntegral ω γ₂
hgi : ∀ (t : ↑I), ∫ᶜ (x : E) in φ.evalAt t, ω x = -∫ (s : ℝ) in 0..1, g (s, ↑t)
⊢ (∫ (t : ℝ) in 0..1, f (0, t)) + -∫ (s : ℝ) in 0..1, g (s, ↑1) =
    (∫ (t : ℝ) in 0..1, f (1, t)) + -∫ (s : ℝ) in 0..1, g (s, ↑0)

Tactic:
linear_combination (norm := {dsimp; abel}) -this

Goal state after:
Module: Mathlib.Topology.Separation.CompletelyRegular

Goal state before:
pp: case refine_2
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompletelyRegularSpace X
hX : #X < 𝔠
x : X
s : Set X
hxs : x ∈ s
hs : IsOpen[inst✝¹] s
f : X → ↑I
hfc : Continuous[inst✝¹, _] f
hf₀ : f x = 0
hf₁ : EqOn f 1 sᶜ
R : Set ↑I := range f
hR : #↑R < #↑I
r : ↑I
hr : r ∈ Rᶜ
hr' : ∀ (x : X), f x ≠ r
hrclopen : f ⁻¹' Iio r = f ⁻¹' Iic r
⊢ f ⁻¹' Iio r ⊆ s

Tactic:
refine preimage_subset_iff.mpr (fun x ↦ ?_)

Goal state after:
case refine_2
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompletelyRegularSpace X
hX : #X < 𝔠
x✝ : X
s : Set X
hxs : x✝ ∈ s
hs : IsOpen[inst✝¹] s
f : X → ↑I
hfc : Continuous[inst✝¹, _] f
hf₀ : f x✝ = 0
hf₁ : EqOn f 1 sᶜ
R : Set ↑I := range f
hR : #↑R < #↑I
r : ↑I
hr : r ∈ Rᶜ
hr' : ∀ (x : X), f x ≠ r
hrclopen : f ⁻¹' Iio r = f ⁻¹' Iic r
x : X
⊢ f x ∈ Iio r → x ∈ s
Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric

Goal state before:
pp: Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : PseudoEMetricSpace Ω
μ ν : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
⊢ max (μ univ) (ν univ) < ∞

Tactic:
simp [measure_lt_top]

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
g : G
⊢ μ.addHaarScalarFactor ((DomMulAct.mk g)⁻¹ • μ) = (distribHaarChar A) g

Tactic:
rw [← addHaarScalarFactor_domSMul _ _ (DomMulAct.mk g)]

Goal state after:
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
g : G
⊢ (DomMulAct.mk g • μ).addHaarScalarFactor (DomMulAct.mk g • (DomMulAct.mk g)⁻¹ • μ) = (distribHaarChar A) 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
b : B
this : (map (fun x ↦ b * x) (H.inducedMeasure μA μC)).Regular
f : CompactlySupportedContinuousMap B ℝ
h : ∀ (x : B), f (b * x) = (f.comp (Homeomorph.mulLeft b).toCocompactMap) x
⊢ ∫ (x : C), ((H.pushforward μA) (f.comp (Homeomorph.mulLeft b).toCocompactMap)) ((ψ b)⁻¹ * x) ∂μC =
    ∫ (c : C), ((H.pushforward μA) f) c ∂μC

Tactic:
congr with c

Goal state after:
case e_f
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
b : B
this : (map (fun x ↦ b * x) (H.inducedMeasure μA μC)).Regular
f : CompactlySupportedContinuousMap B ℝ
h : ∀ (x : B), f (b * x) = (f.comp (Homeomorph.mulLeft b).toCocompactMap) x
c : C
⊢ ((H.pushforward μA) (f.comp (Homeomorph.mulLeft b).toCocompactMap)) ((ψ b)⁻¹ * c) = ((H.pushforward μA) f) c
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
K : Set B
hK : IsCompact K
hb : b ∈ interior K
hKU : K ⊆ U
f : C(B, ℝ)
hf1 : Set.EqOn (⇑f) 1 K
hf2 : IsCompact (tsupport ⇑f)
hf3 : tsupport ⇑f ⊆ U
hf4 : ∀ (x : B), f x ∈ Set.Icc 0 1
hf0 : 0 ≤ (H.pushforward μA) { toContinuousMap := f, hasCompactSupport' := hf2 }
a : A
ha : φ a = (Function.invFun (⇑ψ) (ψ b))⁻¹ * b
⊢ f (Function.invFun (⇑ψ) (ψ b) * φ a) ≠ 0

Tactic:
simp [ha, hf1 (interior_subset hb)]

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

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
p : ℝ
hp : 1 ≤ p
h₁ : 0 < p
⊢ volume {x | ∑ i, |x i| ^ p < 1} = ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma (↑(card ι) / p + 1))

Tactic:
have : (ENNReal.ofReal p).toReal = p := toReal_ofReal (le_of_lt h₁)

Goal state after:
ι : Type u_1
inst✝ : Fintype ι
p : ℝ
hp : 1 ≤ p
h₁ : 0 < p
this : (ENNReal.ofReal p).toReal = p
⊢ volume {x | ∑ i, |x i| ^ p < 1} = ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma (↑(card ι) / p + 1))
Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : 0 < p
⊢ volume {x | (∑ i, |x i| ^ p) ^ (1 / p) ≤ r} =
    ENNReal.ofReal r ^ card ι * ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma (↑(card ι) / p + 1))

Tactic:
have : (ENNReal.ofReal p).toReal = p := toReal_ofReal (le_of_lt h₁)

Goal state after:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : 0 < p
this : (ENNReal.ofReal p).toReal = p
⊢ volume {x | (∑ i, |x i| ^ p) ^ (1 / p) ≤ r} =
    ENNReal.ofReal r ^ card ι * ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma (↑(card ι) / p + 1))
Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
p : ℝ
hp : 1 ≤ p
h₁ : 0 < p
⊢ volume {x | ∑ i, ‖x i‖ ^ p < 1} =
    ENNReal.ofReal ((π * Real.Gamma (2 / p + 1)) ^ card ι / Real.Gamma (2 * ↑(card ι) / p + 1))

Tactic:
have : (ENNReal.ofReal p).toReal = p := toReal_ofReal (le_of_lt h₁)

Goal state after:
ι : Type u_1
inst✝ : Fintype ι
p : ℝ
hp : 1 ≤ p
h₁ : 0 < p
this : (ENNReal.ofReal p).toReal = p
⊢ volume {x | ∑ i, ‖x i‖ ^ p < 1} =
    ENNReal.ofReal ((π * Real.Gamma (2 / p + 1)) ^ card ι / Real.Gamma (2 * ↑(card ι) / p + 1))
Module: Mathlib.MeasureTheory.Measure.Prokhorov

Goal state before:
pp: E : Type u_1
inst✝³ : MeasurableSpace E
inst✝² : TopologicalSpace E
inst✝¹ : T2Space E
inst✝ : BorelSpace E
u : ℕ → ℝ≥0
K : ℕ → Set E
C : ℝ≥0
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
h : NormalSpace E ∨ Monotone K
I :
  ∀ (μ : FiniteMeasure E) (n : ℕ),
    ∑ i ∈ Finset.range (n + 1), μ.restrict (disjointed K i) = μ.restrict ((partialSups K) n)
A : ∀ (n : ℕ), IsCompact ((partialSups K) n)
f : Ultrafilter (FiniteMeasure E)
hf : {μ | μ.mass ≤ C ∧ ∀ (n : ℕ), μ (K n)ᶜ ≤ u n} ∈ f
n : ℕ
ρ : FiniteMeasure E
hρ : ρ.mass ≤ C ∧ ∀ (n : ℕ), ρ (K n)ᶜ ≤ u n
⊢ ρ (disjointed K n) ≤ C ∧ ↑ρ (((partialSups K) n)ᶜ ∩ disjointed K n) = 0

Tactic:
refine ⟨(apply_le_mass ρ _).trans hρ.1, ?_⟩

Goal state after:
E : Type u_1
inst✝³ : MeasurableSpace E
inst✝² : TopologicalSpace E
inst✝¹ : T2Space E
inst✝ : BorelSpace E
u : ℕ → ℝ≥0
K : ℕ → Set E
C : ℝ≥0
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
h : NormalSpace E ∨ Monotone K
I :
  ∀ (μ : FiniteMeasure E) (n : ℕ),
    ∑ i ∈ Finset.range (n + 1), μ.restrict (disjointed K i) = μ.restrict ((partialSups K) n)
A : ∀ (n : ℕ), IsCompact ((partialSups K) n)
f : Ultrafilter (FiniteMeasure E)
hf : {μ | μ.mass ≤ C ∧ ∀ (n : ℕ), μ (K n)ᶜ ≤ u n} ∈ f
n : ℕ
ρ : FiniteMeasure E
hρ : ρ.mass ≤ C ∧ ∀ (n : ℕ), ρ (K n)ᶜ ≤ u n
⊢ ↑ρ (((partialSups K) n)ᶜ ∩ disjointed K n) = 0
Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : 0 < p
⊢ volume {x | (∑ i, ‖x i‖ ^ p) ^ (1 / p) ≤ r} =
    ENNReal.ofReal r ^ (2 * card ι) *
      ENNReal.ofReal ((π * Real.Gamma (2 / p + 1)) ^ card ι / Real.Gamma (2 * ↑(card ι) / p + 1))

Tactic:
have : (ENNReal.ofReal p).toReal = p := toReal_ofReal (le_of_lt h₁)

Goal state after:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : 0 < p
this : (ENNReal.ofReal p).toReal = p
⊢ volume {x | (∑ i, ‖x i‖ ^ p) ^ (1 / p) ≤ r} =
    ENNReal.ofReal r ^ (2 * card ι) *
      ENNReal.ofReal ((π * Real.Gamma (2 / p + 1)) ^ card ι / Real.Gamma (2 * ↑(card ι) / p + 1))
Module: Mathlib.MeasureTheory.Measure.Prokhorov

Goal state before:
pp: E : Type u_1
inst✝³ : MeasurableSpace E
inst✝² : TopologicalSpace E
inst✝¹ : T2Space E
inst✝ : BorelSpace E
u : ℕ → ℝ≥0
K : ℕ → Set E
C : ℝ≥0
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
h : NormalSpace E ∨ Monotone K
I :
  ∀ (μ : FiniteMeasure E) (n : ℕ),
    ∑ i ∈ Finset.range (n + 1), μ.restrict (disjointed K i) = μ.restrict ((partialSups K) n)
A : ∀ (n : ℕ), IsCompact ((partialSups K) n)
f : Ultrafilter (FiniteMeasure E)
hf : {μ | μ.mass ≤ C ∧ ∀ (n : ℕ), μ (K n)ᶜ ≤ u n} ∈ f
ν : ℕ → FiniteMeasure E
ν_reg : ∀ (n : ℕ), (↑(ν n)).InnerRegular
νK : ∀ (n : ℕ), (ν n) ((partialSups K) n)ᶜ = 0
hν : ∀ (n : ℕ), Tendsto (fun ρ ↦ ρ.restrict (disjointed K n)) (↑f) (𝓝 (ν n))
B : (Measure.sum fun n ↦ ↑(ν n)) univ ≤ ↑C
μ : FiniteMeasure E := ⟨Measure.sum fun n ↦ ↑(ν n), ⋯⟩
g : E →ᵇ ℝ
ε : ℝ
εpos : ε > 0
I1 : ∀ᶠ (n : ℕ) in atTop, dist (∫ (x : E), g x ∂∑ i ∈ Finset.range (n + 1), ↑(ν i)) (∫ (x : E), g x ∂↑μ) < ε / 3
I2 : ∀ᶠ (n : ℕ) in atTop, ‖g‖ * ↑(u n) < ε / 3
n : ℕ
hn : dist (∫ (x : E), g x ∂∑ i ∈ Finset.range (n + 1), ↑(ν i)) (∫ (x : E), g x ∂↑μ) < ε / 3
h'n : ‖g‖ * ↑(u n) < ε / 3
this✝ :
  Tendsto (fun ρ ↦ ∫ (x : E), g x ∂↑(∑ i ∈ Finset.range (n + 1), ρ.restrict (disjointed K i))) (↑f)
    (𝓝 (∫ (x : E), g x ∂↑(∑ i ∈ Finset.range (n + 1), ν i)))
ρ : FiniteMeasure E
hρ :
  dist (∫ (x : E), g x ∂↑(∑ i ∈ Finset.range (n + 1), ρ.restrict (disjointed K i)))
      (∫ (x : E), g x ∂↑(∑ i ∈ Finset.range (n + 1), ν i)) <
    ε / 3
h'ρ : ρ.mass ≤ C ∧ ∀ (n : ℕ), ρ (K n)ᶜ ≤ u n
this : ρ = ρ.restrict ((partialSups K) n)ᶜ + ∑ i ∈ Finset.range (n + 1), ρ.restrict (disjointed K i)
⊢ ∫ (x : E), ‖g x‖ ∂↑(ρ.restrict ((partialSups K) n)ᶜ) ≤ ∫ (x : E), ‖g‖ ∂↑(ρ.restrict ((partialSups K) n)ᶜ)

Tactic:
apply integral_mono_of_nonneg
          · filter_upwards with x using by positivity
          · simp
          · filter_upwards with x using norm_coe_le_norm g x

Goal state after:
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) {x | r < ‖⟪y, x⟫_𝕜‖}) atTop) atTop (𝓝 0)
y : E
hy : ¬y = 0
h' : Tendsto (fun r ↦ limsup (fun n ↦ (μ n) {x | ‖y‖⁻¹ * r < ‖⟪(↑‖y‖)⁻¹ • y, x⟫_𝕜‖}) atTop) atTop (𝓝 0)
r : ℝ
n : ℕ
x : E
⊢ r < ‖⟪y, x⟫_𝕜‖ ↔ ‖y‖⁻¹ * r < ‖⟪(↑‖y‖)⁻¹ • y, x⟫_𝕜‖

Tactic:
inner_smul_left

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) {x | r < ‖⟪y, x⟫_𝕜‖}) atTop) atTop (𝓝 0)
y : E
hy : ¬y = 0
h' : Tendsto (fun r ↦ limsup (fun n ↦ (μ n) {x | ‖y‖⁻¹ * r < ‖⟪(↑‖y‖)⁻¹ • y, x⟫_𝕜‖}) atTop) atTop (𝓝 0)
r : ℝ
n : ℕ
x : E
⊢ r < ‖⟪y, x⟫_𝕜‖ ↔ ‖y‖⁻¹ * r < ‖(starRingEnd 𝕜) (↑‖y‖)⁻¹ * ⟪y, x⟫_𝕜‖
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
u : ℕ → ℝ≥0
K : ℕ → Set E
C : ℝ≥0
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
I :
  ∀ (μ : FiniteMeasure E) (n : ℕ),
    ∑ i ∈ Finset.range (n + 1), μ.restrict (disjointed K i) = μ.restrict ((partialSups K) n)
A : ∀ (n : ℕ), IsCompact ((partialSups K) n)
f : Ultrafilter (FiniteMeasure E)
hf : {μ | μ.mass ≤ C ∧ ∀ (n : ℕ), μ (K n)ᶜ ≤ u n} ∈ f
ν : ℕ → FiniteMeasure E
ν_reg : ∀ (n : ℕ), (↑(ν n)).InnerRegular
νK : ∀ (n : ℕ), (ν n) ((partialSups K) n)ᶜ = 0
hν : ∀ (n : ℕ), Tendsto (fun ρ ↦ ρ.restrict (disjointed K n)) (↑f) (𝓝 (ν n))
B : (Measure.sum fun n ↦ ↑(ν n)) univ ≤ ↑C
μ : FiniteMeasure E := ⋯
L : Tendsto id (↑f) (𝓝 μ)
n : ℕ
h : NormalSpace E
this✝ : (↑μ).InnerRegular
g : E → ℝ
g_cont : Continuous[inst✝², _] g
gK : EqOn g 0 (K n)
g_nonneg : 0 ≤ g
g_le : g ≤ 1
this : Tendsto (fun ρ ↦ ∫ (x : E), g x ∂↑ρ) (↑f) (𝓝 (∫ (x : E), g x ∂↑μ))
ρ : FiniteMeasure E
hρ : ρ.mass ≤ C ∧ ∀ (n : ℕ), ρ (K n)ᶜ ≤ u n
⊢ g ≤ᵐ[↑ρ] (K n)ᶜ.indicator 1

Tactic:
· filter_upwards [] with x
        by_cases hx : x ∈ (K n)ᶜ
        · simpa [hx] using g_le x
        · simp only [hx, not_false_eq_true, indicator_of_notMem]
          apply le_of_eq
          apply gK
          simpa using hx

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

Goal state before:
pp: case inl
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 𝒜
⊢ {x | ∃ s, ∃ (hs : MeasurableSet s) (hμs : μ s ≠ ∞), indicatorConstLp p hs hμs 0 = x} ⊆
    {x | ∃ s, ∃ (hs : s ∈ 𝒜) (hμs : μ s ≠ ∞), indicatorConstLp p ⋯ hμs 0 = x}

Tactic:
rintro - ⟨s, ms, hμs, rfl⟩

Goal state after:
case inl
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 𝒜
s : Set X
ms : MeasurableSet s
hμs : μ s ≠ ∞
⊢ indicatorConstLp p ms hμs 0 ∈ {x | ∃ s, ∃ (hs : s ∈ 𝒜) (hμs : μ s ≠ ∞), indicatorConstLp p ⋯ hμs 0 = x}
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
⊢ {x | ∃ s, ∃ (hs : MeasurableSet s) (hμs : μ s ≠ ∞), indicatorConstLp p hs hμs c = x} ⊆
    closure {x | ∃ s, ∃ (hs : s ∈ 𝒜) (hμs : μ s ≠ ∞), indicatorConstLp p ⋯ hμs c = x}

Tactic:
rintro - ⟨s, ms, hμs, rfl⟩

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 ≠ ∞
⊢ indicatorConstLp p ms hμs c ∈ closure {x | ∃ s, ∃ (hs : s ∈ 𝒜) (hμs : μ s ≠ ∞), indicatorConstLp p ⋯ hμs c = x}
Module: Mathlib.MeasureTheory.Measure.ResolventTransform

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁵ : NormedField 𝕜
inst✝⁴ : NormedRing A
inst✝³ : NormedAlgebra ℝ A
inst✝² : NormedAlgebra 𝕜 A
m𝕜 : MeasurableSpace 𝕜
inst✝¹ : MeasurableSingletonClass 𝕜
inst✝ : CompleteSpace A
x : 𝕜
a : A
⊢ resolventTransform (dirac x) a = resolvent a x

Tactic:
by
  simp [resolventTransform_def]

Goal state after: