mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.ContinuousMap.Bounded.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : PseudoMetricSpace β
f g : α →ᵇ β
⊢ dist f g = ⨆ x, dist (f x) (g x)

Tactic:
cases isEmpty_or_nonempty α

Goal state after:
case inl
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : PseudoMetricSpace β
f g : α →ᵇ β
h✝ : IsEmpty α
⊢ dist f g = ⨆ x, dist (f x) (g x)

case inr
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : PseudoMetricSpace β
f g : α →ᵇ β
h✝ : Nonempty α
⊢ dist f g = ⨆ x, dist (f x) (g x)
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
β : Type u_7
x✝¹ : MeasurableSpace β
μ' : Measure β
φ : α → β
T' : Set β → E →L[ℝ] F
hT' : DominatedFinMeasAdditive μ' T' C'
f : β → E
hf : Integrable (f ∘ φ) μ
hfm : StronglyMeasurable f
hφ : Measurable φ
hμ' : μ' ≤ Measure.map φ μ
h : ∀ (s : Set β) (x : E), MeasurableSet s → (T' s) x = (T (φ ⁻¹' s)) x
hF : CompleteSpace F
hfi' : Integrable f μ'
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : SeparableSpace ↑(range f ∪ {0})
i : ℕ
y : E
x✝ : y ∈ (SimpleFunc.approxOn f ⋯ (insert 0 (range f)) 0 ⋯ i).range
hy : y ∉ ((SimpleFunc.approxOn f ⋯ (insert 0 (range f)) 0 ⋯ i).comp φ hφ).range
⊢ (T (⇑(SimpleFunc.approxOn f ⋯ (insert 0 (range f)) 0 ⋯ i) ∘ φ ⁻¹' {y})) y = 0

Tactic:
SimpleFunc.mem_range,

Goal state after:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
β : Type u_7
x✝¹ : MeasurableSpace β
μ' : Measure β
φ : α → β
T' : Set β → E →L[ℝ] F
hT' : DominatedFinMeasAdditive μ' T' C'
f : β → E
hf : Integrable (f ∘ φ) μ
hfm : StronglyMeasurable f
hφ : Measurable φ
hμ' : μ' ≤ Measure.map φ μ
h : ∀ (s : Set β) (x : E), MeasurableSet s → (T' s) x = (T (φ ⁻¹' s)) x
hF : CompleteSpace F
hfi' : Integrable f μ'
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : SeparableSpace ↑(range f ∪ {0})
i : ℕ
y : E
x✝ : y ∈ (SimpleFunc.approxOn f ⋯ (insert 0 (range f)) 0 ⋯ i).range
hy : y ∉ range ⇑((SimpleFunc.approxOn f ⋯ (insert 0 (range f)) 0 ⋯ i).comp φ hφ)
⊢ (T (⇑(SimpleFunc.approxOn f ⋯ (insert 0 (range f)) 0 ⋯ i) ∘ φ ⁻¹' {y})) y = 0
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: α : Type u_1
G : Type u_5
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hc'0 : c' = 0
hμ'0 : μ' = 0
f : ↥(Lp G 1 μ)
⊢ ↑↑(Integrable.toL1 ↑↑f ⋯) =ᵐ[μ'] ↑↑(0 f)

Tactic:
simp_rw [hμ'0]

Goal state after:
α : Type u_1
G : Type u_5
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hc'0 : c' = 0
hμ'0 : μ' = 0
f : ↥(Lp G 1 μ)
⊢ ↑↑(Integrable.toL1 ↑↑f ⋯) =ᵐ[0] ↑↑(0 f)
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: case pos.h_add
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C C' : ℝ
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T C'
f : α → E
hfμ : Integrable f μ
hF : CompleteSpace F
h_int : ∀ (g : α → E), Integrable g μ → Integrable g μ'
⊢ ∀ ⦃f g : α → E⦄,
    Disjoint (Function.support f) (Function.support g) →
      Integrable f μ →
        Integrable g μ →
          setToFun μ T hT f = setToFun μ' T hT' f →
            setToFun μ T hT g = setToFun μ' T hT' g → setToFun μ T hT (f + g) = setToFun μ' T hT' (f + g)

Tactic:
intro f₂

Goal state after:
case pos.h_add
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C C' : ℝ
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T C'
f : α → E
hfμ : Integrable f μ
hF : CompleteSpace F
h_int : ∀ (g : α → E), Integrable g μ → Integrable g μ'
f₂ : α → E
⊢ ∀ ⦃g : α → E⦄,
    Disjoint (Function.support f₂) (Function.support g) →
      Integrable f₂ μ →
        Integrable g μ →
          setToFun μ T hT f₂ = setToFun μ' T hT' f₂ →
            setToFun μ T hT g = setToFun μ' T hT' g → setToFun μ T hT (f₂ + g) = setToFun μ' T hT' (f₂ + g)
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: case pos.h_ae
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C C' : ℝ
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T C'
f : α → E
hfμ : Integrable f μ
hF : CompleteSpace F
h_int : ∀ (g : α → E), Integrable g μ → Integrable g μ'
⊢ ∀ ⦃f g : α → E⦄,
    f =ᵐ[μ] g → Integrable f μ → setToFun μ T hT f = setToFun μ' T hT' f → setToFun μ T hT g = setToFun μ' T hT' g

Tactic:
intro f₂

Goal state after:
case pos.h_ae
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C C' : ℝ
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T C'
f : α → E
hfμ : Integrable f μ
hF : CompleteSpace F
h_int : ∀ (g : α → E), Integrable g μ → Integrable g μ'
f₂ : α → E
⊢ ∀ ⦃g : α → E⦄,
    f₂ =ᵐ[μ] g → Integrable f₂ μ → setToFun μ T hT f₂ = setToFun μ' T hT' f₂ → setToFun μ T hT g = setToFun μ' T hT' g
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ T C
hC : 0 ≤ C
⊢ ‖setToFun μ T hT f‖ₑ ≤ ↑(NNReal.mk C hC) * ∫⁻ (x : α), ‖f x‖ₑ ∂μ

Tactic:
by
  by_cases hF : CompleteSpace F; swap
  · simp [setToFun, hF]
  by_cases hf : Integrable f μ; swap
  · simp [setToFun_undef _ hf]
  apply (ENNReal.toReal_le_toReal (by simp)
    (ENNReal.mul_ne_top (by simp) hf.hasFiniteIntegral.ne)).1
  simp only [toReal_enorm, toReal_mul, coe_toReal, NNReal.coe_mk]
  apply (norm_setToFun_le hT hf hC).trans
  gcongr
  apply le_of_eq
  rw [Integrable.norm_toL1_eq_lintegral_enorm]

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

Goal state before:
pp: δ : Type u_1
X : δ → Type u_3
inst✝³ : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst✝² : DecidableEq δ
inst✝¹ : ∀ (i : δ), SigmaFinite (μ i)
inst✝ : Fintype δ
f : ((i : δ) → X i) → ℝ≥0∞
e : ↥Finset.univ ≃ δ := subtypeUnivEquiv ⋯
x : (i : δ) → X i
⊢ (∫⁻ (y : (i : ↥Finset.univ) → X ↑i), f (updateFinset x Finset.univ y) ∂Measure.pi fun i ↦ μ ↑i) =
    ∫⁻ (a : (b : ↥Finset.univ) → X (e b)), f ((MeasurableEquiv.piCongrLeft X e) a) ∂Measure.pi fun i' ↦ μ (e i')

Tactic:
updateFinset_def

Goal state after:
δ : Type u_1
X : δ → Type u_3
inst✝³ : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst✝² : DecidableEq δ
inst✝¹ : ∀ (i : δ), SigmaFinite (μ i)
inst✝ : Fintype δ
f : ((i : δ) → X i) → ℝ≥0∞
e : ↥Finset.univ ≃ δ := subtypeUnivEquiv ⋯
x : (i : δ) → X i
⊢ (∫⁻ (y : (i : ↥Finset.univ) → X ↑i),
      f fun i ↦ if hi : i ∈ Finset.univ then y ⟨i, hi⟩ else x i ∂Measure.pi fun i ↦ μ ↑i) =
    ∫⁻ (a : (b : ↥Finset.univ) → X (e b)), f ((MeasurableEquiv.piCongrLeft X e) a) ∂Measure.pi fun i' ↦ μ (e i')
Module: Mathlib.MeasureTheory.Integral.Marginal

Goal state before:
pp: δ : Type u_1
X : δ → Type u_3
inst✝³ : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst✝² : DecidableEq δ
inst✝¹ : ∀ (i : δ), SigmaFinite (μ i)
inst✝ : Fintype δ
s : Finset δ
f g : ((i : δ) → X i) → ℝ≥0∞
hf : Measurable f
hg : Measurable g
hfg : ∫⋯∫⁻_s, f ∂μ = ∫⋯∫⁻_s, g ∂μ
⊢ ∫⁻ (x : (i : δ) → X i), f x ∂Measure.pi μ = ∫⁻ (x : (i : δ) → X i), g x ∂Measure.pi μ

Tactic:
rcases isEmpty_or_nonempty (∀ i, X i) with h | ⟨⟨x⟩⟩

Goal state after:
case inl
δ : Type u_1
X : δ → Type u_3
inst✝³ : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst✝² : DecidableEq δ
inst✝¹ : ∀ (i : δ), SigmaFinite (μ i)
inst✝ : Fintype δ
s : Finset δ
f g : ((i : δ) → X i) → ℝ≥0∞
hf : Measurable f
hg : Measurable g
hfg : ∫⋯∫⁻_s, f ∂μ = ∫⋯∫⁻_s, g ∂μ
h : IsEmpty ((i : δ) → X i)
⊢ ∫⁻ (x : (i : δ) → X i), f x ∂Measure.pi μ = ∫⁻ (x : (i : δ) → X i), g x ∂Measure.pi μ

case inr
δ : Type u_1
X : δ → Type u_3
inst✝³ : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst✝² : DecidableEq δ
inst✝¹ : ∀ (i : δ), SigmaFinite (μ i)
inst✝ : Fintype δ
s : Finset δ
f g : ((i : δ) → X i) → ℝ≥0∞
hf : Measurable f
hg : Measurable g
hfg : ∫⋯∫⁻_s, f ∂μ = ∫⋯∫⁻_s, g ∂μ
x : (i : δ) → X i
⊢ ∫⁻ (x : (i : δ) → X i), f x ∂Measure.pi μ = ∫⁻ (x : (i : δ) → X i), g x ∂Measure.pi μ
Module: Mathlib.MeasureTheory.Integral.Marginal

Goal state before:
pp: δ : Type u_1
X : δ → Type u_3
inst✝³ : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst✝² : DecidableEq δ
inst✝¹ : ∀ (i : δ), SigmaFinite (μ i)
inst✝ : Fintype δ
s : Finset δ
f g : ((i : δ) → X i) → ℝ≥0∞
hf : Measurable f
hg : Measurable g
hfg : ∫⋯∫⁻_s, f ∂μ ≤ ∫⋯∫⁻_s, g ∂μ
⊢ ∫⁻ (x : (i : δ) → X i), f x ∂Measure.pi μ ≤ ∫⁻ (x : (i : δ) → X i), g x ∂Measure.pi μ

Tactic:
rcases isEmpty_or_nonempty (∀ i, X i) with h | ⟨⟨x⟩⟩

Goal state after:
case inl
δ : Type u_1
X : δ → Type u_3
inst✝³ : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst✝² : DecidableEq δ
inst✝¹ : ∀ (i : δ), SigmaFinite (μ i)
inst✝ : Fintype δ
s : Finset δ
f g : ((i : δ) → X i) → ℝ≥0∞
hf : Measurable f
hg : Measurable g
hfg : ∫⋯∫⁻_s, f ∂μ ≤ ∫⋯∫⁻_s, g ∂μ
h : IsEmpty ((i : δ) → X i)
⊢ ∫⁻ (x : (i : δ) → X i), f x ∂Measure.pi μ ≤ ∫⁻ (x : (i : δ) → X i), g x ∂Measure.pi μ

case inr
δ : Type u_1
X : δ → Type u_3
inst✝³ : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst✝² : DecidableEq δ
inst✝¹ : ∀ (i : δ), SigmaFinite (μ i)
inst✝ : Fintype δ
s : Finset δ
f g : ((i : δ) → X i) → ℝ≥0∞
hf : Measurable f
hg : Measurable g
hfg : ∫⋯∫⁻_s, f ∂μ ≤ ∫⋯∫⁻_s, g ∂μ
x : (i : δ) → X i
⊢ ∫⁻ (x : (i : δ) → X i), f x ∂Measure.pi μ ≤ ∫⁻ (x : (i : δ) → X i), g x ∂Measure.pi μ
Module: Mathlib.MeasureTheory.Measure.Stieltjes

Goal state before:
pp: R : Type u_1
inst✝⁴ : LinearOrder R
inst✝³ : TopologicalSpace R
inst✝² : OrderTopology R
inst✝¹ : DenselyOrdered R
inst✝ : NoMaxOrder R
f : StieltjesFunction R
x : R
this : rightLim (↑f) x = ⨅ r, ↑f ↑r
⊢ rightLim (↑f) x = ↑f x

Tactic:
f.rightLim_eq

Goal state after:
R : Type u_1
inst✝⁴ : LinearOrder R
inst✝³ : TopologicalSpace R
inst✝² : OrderTopology R
inst✝¹ : DenselyOrdered R
inst✝ : NoMaxOrder R
f : StieltjesFunction R
x : R
this : rightLim (↑f) x = ⨅ r, ↑f ↑r
⊢ ↑f x = ↑f x
Module: Mathlib.MeasureTheory.Measure.Stieltjes

Goal state before:
pp: case inl
R : Type u_1
inst✝¹ : LinearOrder R
inst✝ : TopologicalSpace R
f : StieltjesFunction R
hR : IsEmpty R
⊢ f.length ∅ = 0

Tactic:
simp [length_eq_of_isEmpty]

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

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
β : Type u_7
mβ : MeasurableSpace β
inst✝ : SFinite μ
f : β → α → E
hf : StronglyMeasurable (Function.uncurry f)
⊢ MeasurableSet {x | HasFiniteIntegral (f x) μ}

Tactic:
exact measurableSet_lt (Measurable.lintegral_prod_right hf.enorm) measurable_const

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

Goal state before:
pp: case inl
R : Type u_1
inst✝¹ : LinearOrder R
inst✝ : TopologicalSpace R
f : StieltjesFunction R
s₁ s₂ : Set R
h : s₁ ⊆ s₂
hR : IsEmpty R
⊢ f.length s₁ ≤ f.length s₂

Tactic:
simp [length_eq_of_isEmpty]

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

Goal state before:
pp: case inl
R : Type u_1
inst✝¹ : LinearOrder R
inst✝ : TopologicalSpace R
f : StieltjesFunction R
s : Set R
hR : IsEmpty R
⊢ f.length (s \ botSet) = f.length s

Tactic:
simp [length_eq_of_isEmpty]

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

Goal state before:
pp: G : Type w
inst✝ : TopologicalSpace G
μ : Compacts G → ℝ≥0
mono'✝¹ : ∀ (K₁ K₂ : Compacts G), ↑K₁ ⊆ ↑K₂ → μ K₁ ≤ μ K₂
sup_disjoint'✝¹ : ∀ (K₁ K₂ : Compacts G), Disjoint ↑K₁ ↑K₂ → IsClosed ↑K₁ → IsClosed ↑K₂ → μ (K₁ ⊔ K₂) = μ K₁ + μ K₂
sup_le'✝¹ : ∀ (K₁ K₂ : Compacts G), μ (K₁ ⊔ K₂) ≤ μ K₁ + μ K₂
v : Compacts G → ℝ≥0
mono'✝ : ∀ (K₁ K₂ : Compacts G), ↑K₁ ⊆ ↑K₂ → v K₁ ≤ v K₂
sup_disjoint'✝ : ∀ (K₁ K₂ : Compacts G), Disjoint ↑K₁ ↑K₂ → IsClosed ↑K₁ → IsClosed ↑K₂ → v (K₁ ⊔ K₂) = v K₁ + v K₂
sup_le'✝ : ∀ (K₁ K₂ : Compacts G), v (K₁ ⊔ K₂) ≤ v K₁ + v K₂
h :
  (fun μ s ↦ ↑(μ.toFun s)) { toFun := μ, mono' := mono'✝¹, sup_disjoint' := sup_disjoint'✝¹, sup_le' := sup_le'✝¹ } =
    (fun μ s ↦ ↑(μ.toFun s)) { toFun := v, mono' := mono'✝, sup_disjoint' := sup_disjoint'✝, sup_le' := sup_le'✝ }
⊢ μ = v

Tactic:
ext s : 1

Goal state after:
G : Type w
inst✝ : TopologicalSpace G
μ : Compacts G → ℝ≥0
mono'✝¹ : ∀ (K₁ K₂ : Compacts G), ↑K₁ ⊆ ↑K₂ → μ K₁ ≤ μ K₂
sup_disjoint'✝¹ : ∀ (K₁ K₂ : Compacts G), Disjoint ↑K₁ ↑K₂ → IsClosed ↑K₁ → IsClosed ↑K₂ → μ (K₁ ⊔ K₂) = μ K₁ + μ K₂
sup_le'✝¹ : ∀ (K₁ K₂ : Compacts G), μ (K₁ ⊔ K₂) ≤ μ K₁ + μ K₂
v : Compacts G → ℝ≥0
mono'✝ : ∀ (K₁ K₂ : Compacts G), ↑K₁ ⊆ ↑K₂ → v K₁ ≤ v K₂
sup_disjoint'✝ : ∀ (K₁ K₂ : Compacts G), Disjoint ↑K₁ ↑K₂ → IsClosed ↑K₁ → IsClosed ↑K₂ → v (K₁ ⊔ K₂) = v K₁ + v K₂
sup_le'✝ : ∀ (K₁ K₂ : Compacts G), v (K₁ ⊔ K₂) ≤ v K₁ + v K₂
h :
  (fun μ s ↦ ↑(μ.toFun s)) { toFun := μ, mono' := mono'✝¹, sup_disjoint' := sup_disjoint'✝¹, sup_le' := sup_le'✝¹ } =
    (fun μ s ↦ ↑(μ.toFun s)) { toFun := v, mono' := mono'✝, sup_disjoint' := sup_disjoint'✝, sup_le' := sup_le'✝ }
s : Compacts G
⊢ μ s = v s
Module: Mathlib.MeasureTheory.Measure.Content

Goal state before:
pp: G : Type w
inst✝ : TopologicalSpace G
μ : Content G
U : Opens G
hU : μ.innerContent U ≠ ∞
ε : ℝ≥0
hε : ε ≠ 0
h'ε : ↑ε ≠ 0
h : ↑ε < μ.innerContent U
h₂ : μ.innerContent U - ↑ε < μ.innerContent U
| μ.innerContent U - ↑ε < μ.innerContent U

Tactic:
rhs; rw [innerContent]

Goal state after:
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
U : Opens G
hU : μ.innerContent U ≠ ∞
ε : ℝ≥0
hε : ε ≠ 0
h'ε : ↑ε ≠ 0
h : ↑ε < μ.innerContent U
h₂ : μ.innerContent U - ↑ε < μ.innerContent U
| ⨆ K, ⨆ (_ : ↑K ⊆ ↑U), μ K
Module: Mathlib.MeasureTheory.Measure.Content

Goal state before:
pp: G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : R1Space G
U : ℕ → Opens G
⊢ μ.innerContent (⨆ i, U i) ≤ ∑' (i : ℕ), μ.innerContent (U i)

Tactic:
by
  have h3 : ∀ (t : Finset ℕ) (K : ℕ → Compacts G), μ (t.sup K) ≤ t.sum fun i => μ (K i) := by
    intro t K
    refine Finset.induction_on t ?_ ?_
    · simp only [μ.empty, nonpos_iff_eq_zero, Finset.sum_empty, Finset.sup_empty]
    · intro n s hn ih
      grw [Finset.sup_insert, Finset.sum_insert hn, μ.sup_le, ih]
  refine iSup₂_le fun K hK => ?_
  obtain ⟨t, ht⟩ :=
    K.isCompact.elim_finite_subcover _ (fun i => (U i).isOpen) (by rwa [← Opens.coe_iSup])
  rcases K.isCompact.finite_compact_cover t (SetLike.coe ∘ U) (fun i _ => (U i).isOpen) ht with
    ⟨K', h1K', h2K', h3K'⟩
  let L : ℕ → Compacts G := fun n => ⟨K' n, h1K' n⟩
  convert! le_trans (h3 t L) _
  · ext1
    rw [Compacts.coe_finset_sup, Finset.sup_eq_iSup]
    exact h3K'
  refine le_trans (Finset.sum_le_sum ?_) (ENNReal.sum_le_tsum t)
  intro i _
  refine le_trans ?_ (le_iSup _ (L i))
  refine le_trans ?_ (le_iSup _ (h2K' i))
  rfl

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

Goal state before:
pp: G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : R1Space G
U : Opens G
hU : μ.outerMeasure ↑U ≠ ∞
ε : ℝ≥0
hε : ε ≠ 0
⊢ ∃ K, ↑K ⊆ ↑U ∧ μ.outerMeasure ↑U ≤ μ.outerMeasure ↑K + ↑ε

Tactic:
μ.outerMeasure_opens

Goal state after:
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : R1Space G
U : Opens G
hU : μ.innerContent U ≠ ∞
ε : ℝ≥0
hε : ε ≠ 0
⊢ ∃ K, ↑K ⊆ ↑U ∧ μ.innerContent U ≤ μ.outerMeasure ↑K + ↑ε
Module: Mathlib.MeasureTheory.Measure.Content

Goal state before:
pp: G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : R1Space G
f : G ≃ₜ G
h : ∀ ⦃K : Compacts G⦄, μ (Compacts.map ⇑f ⋯ K) = μ K
A : Set G
⊢ μ.outerMeasure (⇑f ⁻¹' A) = μ.outerMeasure A

Tactic:
by
  refine inducedOuterMeasure_preimage _ μ.innerContent_iUnion_nat μ.innerContent_mono _
    (fun _ => f.isOpen_preimage) ?_
  intro s hs
  convert! μ.innerContent_comap f h ⟨s, hs⟩

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

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : R1Space G
S : MeasurableSpace G
inst✝ : BorelSpace G
U : Set G
hU : U ∈ {s | IsOpen s}
U' : Opens G
this✝ : Nonempty { L // ↑L ⊆ ↑U' ∩ U }
L : Compacts G
L' : Compacts G := { carrier := closure ↑L, isCompact' := ⋯ }
hL : ↑L ⊆ ↑U' ∧ ↑L ⊆ U
hL'U : ↑L' ⊆ U
hL'U' : ↑L' ⊆ ↑U'
this : ↑U' \ U ⊆ ↑U' \ ↑L'
⊢ μ L' + μ.outerMeasure (↑U' \ ↑L') ≤ μ.outerMeasure ↑U'

Tactic:
μ.outerMeasure_of_isOpen (↑U' \ L') (IsOpen.sdiff U'.2 isClosed_closure)

Goal state after:
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : R1Space G
S : MeasurableSpace G
inst✝ : BorelSpace G
U : Set G
hU : U ∈ {s | IsOpen s}
U' : Opens G
this✝ : Nonempty { L // ↑L ⊆ ↑U' ∩ U }
L : Compacts G
L' : Compacts G := { carrier := closure ↑L, isCompact' := ⋯ }
hL : ↑L ⊆ ↑U' ∧ ↑L ⊆ U
hL'U : ↑L' ⊆ U
hL'U' : ↑L' ⊆ ↑U'
this : ↑U' \ U ⊆ ↑U' \ ↑L'
⊢ μ L' + μ.innerContent { carrier := ↑U' \ ↑L', is_open' := ⋯ } ≤ μ.outerMeasure ↑U'
Module: Mathlib.MeasureTheory.Measure.Haar.Basic

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
K : Compacts G
V : Set G
hV : (interior V).Nonempty
s : Finset G
h1s : ↑K ⊆ ⋃ g ∈ s, (fun h ↦ g * h) ⁻¹' ↑K₀
h2s : s.card = index ↑K ↑K₀
t : Finset G
h1t : ↑K₀ ⊆ ⋃ g ∈ t, (fun h ↦ g * h) ⁻¹' V
h2t : t.card = index (↑K₀) V
⊢ index (↑K) V ≤ (t * s).card

Tactic:
apply Nat.sInf_le

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
K : Compacts G
V : Set G
hV : (interior V).Nonempty
s : Finset G
h1s : ↑K ⊆ ⋃ g ∈ s, (fun h ↦ g * h) ⁻¹' ↑K₀
h2s : s.card = index ↑K ↑K₀
t : Finset G
h1t : ↑K₀ ⊆ ⋃ g ∈ t, (fun h ↦ g * h) ⁻¹' V
h2t : t.card = index (↑K₀) V
⊢ (t * s).card ∈ Finset.card '' {t | ↑K ⊆ ⋃ g ∈ t, (fun h ↦ g * h) ⁻¹' V}
Module: Mathlib.MeasureTheory.Measure.Haar.Basic

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K : PositiveCompacts G
V : Set G
hV : (interior V).Nonempty
⊢ 0 < index (↑K) V

Tactic:
classical
  rw [index, Nat.sInf_def, Nat.find_pos, mem_image]
  · rintro ⟨t, h1t, h2t⟩; rw [Finset.card_eq_zero] at h2t; subst h2t
    obtain ⟨g, hg⟩ := K.interior_nonempty
    change g ∈ (∅ : Set G)
    convert! h1t (interior_subset hg); symm
    simp only [Finset.notMem_empty, iUnion_of_empty, iUnion_empty]
  · exact index_defined K.isCompact hV

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

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K K' V : Set G
hK' : IsCompact K'
h : K ⊆ K'
hV : (interior V).Nonempty
s : Finset G
h1s : K' ⊆ ⋃ g ∈ s, (fun h ↦ g * h) ⁻¹' V
h2s : s.card = index K' V
⊢ index K V ≤ index K' V

Tactic:
apply Nat.sInf_le

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K K' V : Set G
hK' : IsCompact K'
h : K ⊆ K'
hV : (interior V).Nonempty
s : Finset G
h1s : K' ⊆ ⋃ g ∈ s, (fun h ↦ g * h) ⁻¹' V
h2s : s.card = index K' V
⊢ index K' V ∈ Finset.card '' {t | K ⊆ ⋃ g ∈ t, (fun h ↦ g * h) ⁻¹' V}
Module: Mathlib.MeasureTheory.Measure.Haar.Basic

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K K' V : Set G
hK' : IsCompact K'
h : K ⊆ K'
hV : (interior V).Nonempty
⊢ index K V ≤ index K' V

Tactic:
by
  rcases index_elim hK' hV with ⟨s, h1s, h2s⟩
  apply Nat.sInf_le; rw [mem_image]; exact ⟨s, Subset.trans h h1s, h2s⟩

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

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : (interior V).Nonempty
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ g ∈ s, (fun h ↦ g * h) ⁻¹' V
h2s : s.card = index (K₁.carrier ∪ K₂.carrier) V
K : Set G
hK : K ⊆ ⋃ g ∈ s, (fun x ↦ g * x) ⁻¹' V
⊢ index K V ≤ {g ∈ s | ((fun x ↦ g * x) ⁻¹' V ∩ K).Nonempty}.card

Tactic:
apply Nat.sInf_le

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : (interior V).Nonempty
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ g ∈ s, (fun h ↦ g * h) ⁻¹' V
h2s : s.card = index (K₁.carrier ∪ K₂.carrier) V
K : Set G
hK : K ⊆ ⋃ g ∈ s, (fun x ↦ g * x) ⁻¹' V
⊢ {g ∈ s | ((fun x ↦ g * x) ⁻¹' V ∩ K).Nonempty}.card ∈ Finset.card '' {t | K ⊆ ⋃ g ∈ t, (fun h ↦ g * h) ⁻¹' V}
Module: Mathlib.MeasureTheory.Group.FundamentalDomain

Goal state before:
pp: G : Type u_1
H : Type u_2
α : Type u_3
inst✝⁴ : Group G
inst✝³ : MulAction G α
s : Set α
inst✝² : Group H
inst✝¹ : MulAction H α
inst✝ : SMulCommClass H G α
g : H
⊢ fundamentalInterior G (g • s) = g • fundamentalInterior G s

Tactic:
by
  simp_rw [fundamentalInterior, smul_set_sdiff, smul_set_iUnion, smul_comm g (_ : G) (_ : Set α)]

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

Goal state before:
pp: R : Type u_1
inst✝⁷ : LinearOrder R
inst✝⁶ : TopologicalSpace R
f : StieltjesFunction R
inst✝⁵ : OrderTopology R
inst✝⁴ : CompactIccSpace R
inst✝³ : MeasurableSpace R
inst✝² : BorelSpace R
inst✝¹ : SecondCountableTopology R
inst✝ : DenselyOrdered R
a : R
ha : ¬IsBot a
b : R
hb : b < a
u : ℕ → R
u_mono : StrictMono u
u_lim : Tendsto u atTop (𝓝 a)
u_lt_a : ∀ (n : ℕ), u n < a
A : {a} = ⋂ n, Ioc (u n) a
L1 : Tendsto (fun n ↦ f.measure (Ioc (u n) a)) atTop (𝓝 (f.measure {a}))
⊢ Tendsto u atTop (𝓝[<] a)

Tactic:
exact
        tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _ u_lim
          (Eventually.of_forall fun n => u_lt_a n)

Goal state after: