mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.ContinuousAffineEquiv

Goal state before:
pp: k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
V₁ : Type u_6
V₂ : Type u_7
inst✝⁸ : Ring k
inst✝⁷ : AddCommGroup V₁
inst✝⁶ : Module k V₁
inst✝⁵ : AddTorsor V₁ P₁
inst✝⁴ : TopologicalSpace P₁
inst✝³ : AddCommGroup V₂
inst✝² : Module k V₂
inst✝¹ : AddTorsor V₂ P₂
inst✝ : TopologicalSpace P₂
⊢ Injective toAffineEquiv

Tactic:
rintro ⟨e, econt, einv_cont⟩ ⟨e', e'cont, e'inv_cont⟩ H

Goal state after:
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
V₁ : Type u_6
V₂ : Type u_7
inst✝⁸ : Ring k
inst✝⁷ : AddCommGroup V₁
inst✝⁶ : Module k V₁
inst✝⁵ : AddTorsor V₁ P₁
inst✝⁴ : TopologicalSpace P₁
inst✝³ : AddCommGroup V₂
inst✝² : Module k V₂
inst✝¹ : AddTorsor V₂ P₂
inst✝ : TopologicalSpace P₂
e : P₁ ≃ᵃ[k] P₂
econt : Continuous e.toFun
einv_cont : Continuous e.invFun
e' : P₁ ≃ᵃ[k] P₂
e'cont : Continuous e'.toFun
e'inv_cont : Continuous e'.invFun
H :
  { toAffineEquiv := e, continuous_toFun := econt, continuous_invFun := einv_cont }.toAffineEquiv =
    { toAffineEquiv := e', continuous_toFun := e'cont, continuous_invFun := e'inv_cont }.toAffineEquiv
⊢ { toAffineEquiv := e, continuous_toFun := econt, continuous_invFun := einv_cont } =
    { toAffineEquiv := e', continuous_toFun := e'cont, continuous_invFun := e'inv_cont }
Module: Mathlib.MeasureTheory.Integral.Bochner.SumMeasure

Goal state before:
pp: ι : Type u_1
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst✝ : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
hf : Integrable f (Measure.sum μ)
⊢ Summable fun i ↦ ∫ (x : X), ‖f x‖ ∂μ i

Tactic:
by
  convert! ENNReal.summable_toReal (f := fun i ↦ ∫⁻ x, ‖f x‖ₑ ∂μ i) ?_ with i
  · rw [← integral_toReal ?_ (by simp)]
    · simp
    · exact (hf.aestronglyMeasurable.mono_measure (Measure.le_sum _ i)).enorm
  rw [← lintegral_sum_measure]
  exact hf.2.ne

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
H : Type u_6
inst✝ : NormedAddCommGroup H
f : α → H
p : ℝ≥0∞
hp1 : p ≠ 0
hp2 : p ≠ ∞
hf : MemLp f p μ
A : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p.toReal) ∂μ = ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ
⊢ (∫⁻ (x : α), ‖f x‖ₑ ^ p.toReal ∂μ) ^ p.toReal⁻¹ =
    ENNReal.ofReal ((∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p.toReal) ∂μ).toReal ^ p.toReal⁻¹)

pp: case hf
α : Type u_1
m : MeasurableSpace α
μ : Measure α
H : Type u_6
inst✝ : NormedAddCommGroup H
f : α → H
p : ℝ≥0∞
hp1 : p ≠ 0
hp2 : p ≠ ∞
hf : MemLp f p μ
A : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p.toReal) ∂μ = ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ
⊢ 0 ≤ᵐ[μ] fun a ↦ ‖f a‖ ^ p.toReal

pp: case hfm
α : Type u_1
m : MeasurableSpace α
μ : Measure α
H : Type u_6
inst✝ : NormedAddCommGroup H
f : α → H
p : ℝ≥0∞
hp1 : p ≠ 0
hp2 : p ≠ ∞
hf : MemLp f p μ
A : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p.toReal) ∂μ = ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ
⊢ AEStronglyMeasurable (fun a ↦ ‖f a‖ ^ p.toReal) μ

Tactic:
rotate_left

Goal state after:
case hf
α : Type u_1
m : MeasurableSpace α
μ : Measure α
H : Type u_6
inst✝ : NormedAddCommGroup H
f : α → H
p : ℝ≥0∞
hp1 : p ≠ 0
hp2 : p ≠ ∞
hf : MemLp f p μ
A : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p.toReal) ∂μ = ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ
⊢ 0 ≤ᵐ[μ] fun a ↦ ‖f a‖ ^ p.toReal

case hfm
α : Type u_1
m : MeasurableSpace α
μ : Measure α
H : Type u_6
inst✝ : NormedAddCommGroup H
f : α → H
p : ℝ≥0∞
hp1 : p ≠ 0
hp2 : p ≠ ∞
hf : MemLp f p μ
A : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p.toReal) ∂μ = ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ
⊢ AEStronglyMeasurable (fun a ↦ ‖f a‖ ^ p.toReal) μ

α : Type u_1
m : MeasurableSpace α
μ : Measure α
H : Type u_6
inst✝ : NormedAddCommGroup H
f : α → H
p : ℝ≥0∞
hp1 : p ≠ 0
hp2 : p ≠ ∞
hf : MemLp f p μ
A : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p.toReal) ∂μ = ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ
⊢ (∫⁻ (x : α), ‖f x‖ₑ ^ p.toReal ∂μ) ^ p.toReal⁻¹ =
    ENNReal.ofReal ((∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p.toReal) ∂μ).toReal ^ p.toReal⁻¹)
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: case pos
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
hE : CompleteSpace E
mα : MeasurableSpace α
f : α → E
hf : StronglyMeasurable f
a : α
s : Set α
hs : MeasurableSet s
inst✝ : Decidable (a ∈ s)
h✝ : a ∈ s
⊢ ∫ (x : α), f x ∂Measure.dirac a = f a

pp: case neg
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
hE : CompleteSpace E
mα : MeasurableSpace α
f : α → E
hf : StronglyMeasurable f
a : α
s : Set α
hs : MeasurableSet s
inst✝ : Decidable (a ∈ s)
h✝ : a ∉ s
⊢ ∫ (x : α), f x ∂0 = 0

Tactic:
· exact integral_dirac' _ _ hf

Goal state after:
case neg
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
hE : CompleteSpace E
mα : MeasurableSpace α
f : α → E
hf : StronglyMeasurable f
a : α
s : Set α
hs : MeasurableSet s
inst✝ : Decidable (a ∈ s)
h✝ : a ∉ s
⊢ ∫ (x : α), f x ∂0 = 0
Module: Mathlib.Analysis.Normed.Module.FiniteDimension

Goal state before:
pp: 𝕜 : Type u
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
F : Type w
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : CompleteSpace 𝕜
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
g : ι → E
t : ι → 𝕜
⊢ ‖((LinearEquiv.piRing 𝕜 E ι 𝕜).symm g) t‖ ≤ Fintype.card ι • ‖g‖ * ‖t‖

Tactic:
LinearEquiv.piRing_symm_apply

Goal state after:
𝕜 : Type u
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
F : Type w
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : CompleteSpace 𝕜
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
g : ι → E
t : ι → 𝕜
⊢ ‖∑ i, t i • g i‖ ≤ Fintype.card ι • ‖g‖ * ‖t‖
Module: Mathlib.Topology.ContinuousMap.Bounded.Basic

Goal state before:
pp: case refine_1.inl
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
δ : Type u_2
inst✝¹ : TopologicalSpace δ
inst✝ : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
x : α
⊢ dist ((extend f g₁ h₁) (f x)) ((extend f g₂ h₂) (f x)) ≤
    max (dist g₁ g₂) (dist (h₁.domRestrict (range ⇑f)ᶜ) (h₂.domRestrict (range ⇑f)ᶜ))

Tactic:
simp only [extend_apply]
      exact (dist_coe_le_dist x).trans (le_max_left _ _)

Goal state after:
Module: Mathlib.Analysis.Normed.Module.FiniteDimension

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
x : E
s : Set E
hx : x ∈ s
hs : s ≠ univ
y : E
hys : y ∈ (interior s)ᶜ
hyd : infDist x sᶜ = dist x y
⊢ infDist x sᶜ = dist y x

Tactic:
rwa [dist_comm]

Goal state after:
Module: Mathlib.Analysis.Normed.Module.FiniteDimension

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
K : Set E
hK : IsCompact K
hx : x ∈ K
⊢ ∃ y ∈ frontier K, infDist x Kᶜ = dist x y

Tactic:
by
  obtain hx' | hx' : x ∈ interior K ∪ frontier K := by
    rw [← closure_eq_interior_union_frontier]
    exact subset_closure hx
  · rw [mem_interior_iff_mem_nhds, Metric.nhds_basis_closedBall.mem_iff] at hx'
    rcases hx' with ⟨r, hr₀, hrK⟩
    have : FiniteDimensional ℝ E :=
      .of_isCompact_closedBall ℝ hr₀
        (hK.of_isClosed_subset Metric.isClosed_closedBall hrK)
    exact exists_mem_frontier_infDist_compl_eq_dist hx hK.ne_univ
  · refine ⟨x, hx', ?_⟩
    rw [frontier_eq_closure_inter_closure] at hx'
    rw [Metric.infDist_zero_of_mem_closure hx'.2, dist_self]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ
hf_nonneg : 0 ≤ᵐ[μ] f
hg_nonneg : 0 ≤ᵐ[μ] g
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
h_left : ∫ (a : α), f a * g a ∂μ = ∫ (a : α), ‖f a‖ * ‖g a‖ ∂μ
h_right_f : ∫ (a : α), f a ^ p ∂μ = ∫ (a : α), ‖f a‖ ^ p ∂μ
⊢ ∫ (a : α), f a * g a ∂μ ≤ (∫ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫ (a : α), g a ^ q ∂μ) ^ (1 / q)

Tactic:
have h_right_g : ∫ a, g a ^ q ∂μ = ∫ a, ‖g a‖ ^ q ∂μ := by
    refine integral_congr_ae ?_
    filter_upwards [hg_nonneg] with x hxg
    rw [Real.norm_of_nonneg hxg]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ
hf_nonneg : 0 ≤ᵐ[μ] f
hg_nonneg : 0 ≤ᵐ[μ] g
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
h_left : ∫ (a : α), f a * g a ∂μ = ∫ (a : α), ‖f a‖ * ‖g a‖ ∂μ
h_right_f : ∫ (a : α), f a ^ p ∂μ = ∫ (a : α), ‖f a‖ ^ p ∂μ
h_right_g : ∫ (a : α), g a ^ q ∂μ = ∫ (a : α), ‖g a‖ ^ q ∂μ
⊢ ∫ (a : α), f a * g a ∂μ ≤ (∫ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫ (a : α), g a ^ q ∂μ) ^ (1 / q)
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 T' : Set α → E →L[ℝ] F
C C' : ℝ
f : α → E
ν : Measure α
hTμ : DominatedFinMeasAdditive μ T C
hTν : DominatedFinMeasAdditive ν T' C'
hμ : Integrable f μ
hν : Integrable f ν
⊢ setToFun (μ + ν) (T - T') ⋯ f = setToFun μ T hTμ f - setToFun ν T' hTν f

Tactic:
simp [sub_eq_add_neg, setToFun_add_measure hTμ hTν.neg hμ hν, setToFun_neg' hTν]

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

Goal state before:
pp: case hbc
α : 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
hF : CompleteSpace F
hf : Integrable f μ
⊢ ‖Integrable.toL1 f hf‖ = (∫⁻ (a : α), ‖f a‖ₑ ∂μ).toReal

Tactic:
Integrable.norm_toL1_eq_lintegral_enorm

Goal state after:
case hbc
α : 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
hF : CompleteSpace F
hf : Integrable f μ
⊢ (∫⁻ (a : α), ‖f a‖ₑ ∂μ).toReal = (∫⁻ (a : α), ‖f a‖ₑ ∂μ).toReal
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: case h₂
α : 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
hF : CompleteSpace F
hf : Integrable f μ
⊢ ‖Integrable.toL1 f hf‖ ≤ (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ).toReal

Tactic:
Integrable.norm_toL1_eq_lintegral_enorm

Goal state after:
case h₂
α : 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
hF : CompleteSpace F
hf : Integrable f μ
⊢ (∫⁻ (a : α), ‖f a‖ₑ ∂μ).toReal ≤ (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ).toReal
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 : ℝ
inst✝¹ : CompleteSpace E
hT : DominatedFinMeasAdditive μ T C
ι : Type u_7
inst✝ : Countable ι
f : ι → α → E
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf' : ∑' (i : ι), ∫⁻ (a : α), ‖f i a‖ₑ ∂μ ≠ ∞
hF : CompleteSpace F
hf'' : ∀ (i : ι), AEMeasurable (fun x ↦ ‖f i x‖ₑ) μ
hhh : ∀ᵐ (a : α) ∂μ, Summable fun n ↦ ↑‖f n a‖₊
this : ∫⁻ (a : α), ∑' (n : ι), ‖f n a‖ₑ ∂μ < ∞
⊢ ∫⁻ (a : α), ‖∑' (n : ι), ‖f n a‖‖ₑ ∂μ = ∫⁻ (a : α), ∑' (n : ι), ‖f n a‖ₑ ∂μ

Tactic:
apply lintegral_congr_ae

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 : ℝ
inst✝¹ : CompleteSpace E
hT : DominatedFinMeasAdditive μ T C
ι : Type u_7
inst✝ : Countable ι
f : ι → α → E
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf' : ∑' (i : ι), ∫⁻ (a : α), ‖f i a‖ₑ ∂μ ≠ ∞
hF : CompleteSpace F
hf'' : ∀ (i : ι), AEMeasurable (fun x ↦ ‖f i x‖ₑ) μ
hhh : ∀ᵐ (a : α) ∂μ, Summable fun n ↦ ↑‖f n a‖₊
this : ∫⁻ (a : α), ∑' (n : ι), ‖f n a‖ₑ ∂μ < ∞
⊢ (fun a ↦ ‖∑' (n : ι), ‖f n a‖‖ₑ) =ᵐ[μ] fun a ↦ ∑' (n : ι), ‖f n a‖ₑ
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 : ℝ
β : Type u_7
mβ : MeasurableSpace β
inst✝ : SFinite μ
hT : DominatedFinMeasAdditive μ T C
h'T : ∀ (s : Set (β × α)), MeasurableSet s → StronglyMeasurable fun x ↦ T (Prod.mk x ⁻¹' s)
f : β → α → E
hf : StronglyMeasurable (Function.uncurry f)
hF : CompleteSpace F
this✝² : MeasurableSpace E := borel E
this✝¹ : BorelSpace E
this✝ : SeparableSpace ↑(range (Function.uncurry f) ∪ {0})
s : ℕ → SimpleFunc (β × α) E := SimpleFunc.approxOn (Function.uncurry f) ⋯ (range (Function.uncurry f) ∪ {0}) 0 ⋯
s' : ℕ → β → SimpleFunc α E := fun n x ↦ (s n).comp (Prod.mk x) ⋯
f' : ℕ → β → F := fun n ↦ {x | Integrable (f x) μ}.indicator fun x ↦ SimpleFunc.setToSimpleFunc T (s' n x)
n : ℕ
this : ∀ (x : β), {x ∈ (s' n x).range | x ≠ 0} ⊆ (s n).range
x : E
x✝ : x ∈ (s n).range
⊢ StronglyMeasurable fun x_1 ↦ (T (Prod.mk x_1 ⁻¹' ⇑(s n) ⁻¹' {x})) x

Tactic:
apply StronglyMeasurable.apply_continuousLinearMap

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 : ℝ
β : Type u_7
mβ : MeasurableSpace β
inst✝ : SFinite μ
hT : DominatedFinMeasAdditive μ T C
h'T : ∀ (s : Set (β × α)), MeasurableSet s → StronglyMeasurable fun x ↦ T (Prod.mk x ⁻¹' s)
f : β → α → E
hf : StronglyMeasurable (Function.uncurry f)
hF : CompleteSpace F
this✝² : MeasurableSpace E := ⋯
this✝¹ : BorelSpace E
this✝ : SeparableSpace ↑(range (Function.uncurry f) ∪ {0})
s : ℕ → SimpleFunc (β × α) E := ⋯
s' : ℕ → β → SimpleFunc α E := ⋯
f' : ℕ → β → F := ⋯
n : ℕ
this : ∀ (x : β), {x ∈ (s' n x).range | x ≠ 0} ⊆ (s n).range
x : E
x✝ : x ∈ (s n).range
⊢ StronglyMeasurable fun a ↦ T (Prod.mk a ⁻¹' ⇑(s n) ⁻¹' {x})
Module: Mathlib.MeasureTheory.Measure.Stieltjes

Goal state before:
pp: case pos
R : Type u_1
inst✝⁴ : LinearOrder R
inst✝³ : TopologicalSpace R
f : StieltjesFunction R
inst✝² : OrderTopology R
inst✝¹ : CompactIccSpace R
inst✝ : DenselyOrdered R
a b : R
hab : a < b
s : ℕ → Set R
hs : Ioc a b ⊆ ⋃ i, s i
ε : ℝ≥0
εpos : 0 < ε
h : ∑' (i : ℕ), f.length (s i) < ∞
δ : ℝ≥0 := ε / 2
δpos : 0 < ↑δ
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), ↑(ε' i) < ↑δ
a' : R
ha' : ↑f a' - ↑f a < ↑δ
aa' : a < a'
this : Nonempty R
i : ℕ
p q' : R
spq : s i \ botSet ⊆ Ioc p q'
hq' : ofReal (↑f q' - ↑f p) < f.length (s i) + ↑(ε' i)
A : Icc a' b ∩ s i ⊆ Ioc p q'
htq' : IsTop q'
x : R
hx : x ∈ Icc a' b ∩ s i
⊢ x ∈ Iotop (p, q').1 (p, q').2

Tactic:
simp only [Iotop, htq', ↓reduceIte, mem_Ioc]

Goal state after:
case pos
R : Type u_1
inst✝⁴ : LinearOrder R
inst✝³ : TopologicalSpace R
f : StieltjesFunction R
inst✝² : OrderTopology R
inst✝¹ : CompactIccSpace R
inst✝ : DenselyOrdered R
a b : R
hab : a < b
s : ℕ → Set R
hs : Ioc a b ⊆ ⋃ i, s i
ε : ℝ≥0
εpos : 0 < ε
h : ∑' (i : ℕ), f.length (s i) < ∞
δ : ℝ≥0 := ε / 2
δpos : 0 < ↑δ
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), ↑(ε' i) < ↑δ
a' : R
ha' : ↑f a' - ↑f a < ↑δ
aa' : a < a'
this : Nonempty R
i : ℕ
p q' : R
spq : s i \ botSet ⊆ Ioc p q'
hq' : ofReal (↑f q' - ↑f p) < f.length (s i) + ↑(ε' i)
A : Icc a' b ∩ s i ⊆ Ioc p q'
htq' : IsTop q'
x : R
hx : x ∈ Icc a' b ∩ s i
⊢ p < x ∧ x ≤ q'
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
⊢ μ.outerMeasure (↑U' ∩ U) + μ.outerMeasure (↑U' \ U) ≤ μ.outerMeasure ↑U'

Tactic:
rw [μ.outerMeasure_of_isOpen ((U' : Set G) ∩ U) (U'.isOpen.inter hU)]

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
⊢ μ.innerContent { carrier := ↑U' ∩ U, is_open' := ⋯ } + μ.outerMeasure (↑U' \ U) ≤ μ.outerMeasure ↑U'
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:
rw [μ.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.Integral.Bochner.Set

Goal state before:
pp: X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure X
inst✝ : PartialOrder E
f : X → E
hf : AEStronglyMeasurable f μ
⊢ ∫ (x : X) in {x | f x < 0}, f x ∂μ = ∫ (x : X) in {x | f x ≤ 0}, f x ∂μ

Tactic:
have h_union : {x | f x ≤ 0} = {x | f x < 0} ∪ {x | f x = 0} := by
    simp_rw [le_iff_lt_or_eq, ofPred_or]

Goal state after:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure X
inst✝ : PartialOrder E
f : X → E
hf : AEStronglyMeasurable f μ
h_union : {x | f x ≤ 0} = {x | f x < 0} ∪ {x | f x = 0}
⊢ ∫ (x : X) in {x | f x < 0}, f x ∂μ = ∫ (x : X) in {x | f x ≤ 0}, f x ∂μ
Module: Mathlib.MeasureTheory.Group.FundamentalDomain

Goal state before:
pp: G : Type u_1
α : Type u_3
E : Type u_5
inst✝⁶ : Group G
inst✝⁵ : MulAction G α
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
s t : Set α
μ : Measure α
inst✝² : MeasurableConstSMul G α
inst✝¹ : SMulInvariantMeasure G α μ
inst✝ : Countable G
hs : IsFundamentalDomain G s μ
ht : IsFundamentalDomain G t μ
f : α → E
hf : ∀ (g : G) (x : α), f (g • x) = f x
⊢ HasFiniteIntegral f (μ.restrict s) ↔ HasFiniteIntegral f (μ.restrict t)

Tactic:
dsimp only [HasFiniteIntegral]
  rw [hs.setLIntegral_eq ht]
  intro g x; rw [hf]

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
inst✝⁵ : OrderTopology R
inst✝⁴ : CompactIccSpace R
inst✝³ : MeasurableSpace R
inst✝² : BorelSpace R
inst✝¹ : SecondCountableTopology R
inst✝ : DenselyOrdered R
a b : R
hab : a ≤ b
⊢ f.measure (Icc a b) = ofReal (↑f b - leftLim (↑f) a)

pp: case inr
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 b : R
hab : b < a
⊢ f.measure (Icc a b) = ofReal (↑f b - leftLim (↑f) a)

Tactic:
· have A : Disjoint {a} (Ioc a b) := by simp
    simp [← Icc_union_Ioc_eq_Icc le_rfl hab, -singleton_union, ← ENNReal.ofReal_add,
      f.mono.leftLim_le, measure_union A measurableSet_Ioc, f.mono hab]

Goal state after:
case inr
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 b : R
hab : b < a
⊢ f.measure (Icc a b) = ofReal (↑f b - leftLim (↑f) a)
Module: Mathlib.MeasureTheory.Measure.Stieltjes

Goal state before:
pp: case inl
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 b : R
hab : b ≤ a
⊢ f.measure (Ioo a b) = ofReal (leftLim (↑f) b - ↑f a)

pp: case inr
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 b : R
hab : a < b
⊢ f.measure (Ioo a b) = ofReal (leftLim (↑f) b - ↑f a)

Tactic:
· simp only [hab, measure_empty, Ioo_eq_empty, not_lt]
    symm
    simp [ENNReal.ofReal_eq_zero, f.mono.leftLim_le hab]

Goal state after:
case inr
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 b : R
hab : a < b
⊢ f.measure (Ioo a b) = ofReal (leftLim (↑f) b - ↑f a)
Module: Mathlib.Analysis.InnerProductSpace.Defs

Goal state before:
pp: 𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
t : ℝ
⊢ ⟪x, ↑t • y⟫ = ⟪x, y⟫ * ↑t

Tactic:
inner_smul_right,

Goal state after:
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
t : ℝ
⊢ ↑t * ⟪x, y⟫ = ⟪x, y⟫ * ↑t
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
eval : (Compacts G → ℝ) → ℝ := fun f ↦ f ⊥
this : Continuous eval
⊢ IsClosed (eval ⁻¹' {0})

Tactic:
apply continuous_iff_isClosed.mp this; exact isClosed_singleton

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₀ : PositiveCompacts G
eval : (Compacts G → ℝ) → ℝ := fun f ↦ f K₀.toCompacts
this : Continuous eval
⊢ IsClosed (eval ⁻¹' {1})

Tactic:
apply continuous_iff_isClosed.mp this; exact isClosed_singleton

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Defs

Goal state before:
pp: 𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
⊢ ⟪⟪x, y⟫ • x - ⟪x, x⟫ • y, ⟪x, y⟫ • x - ⟪x, x⟫ • y⟫ = ↑(normSq x * (normSq x * normSq y - ‖⟪x, y⟫‖ ^ 2))

Tactic:
simp only [inner_sub_sub_self, inner_smul_left, inner_smul_right, conj_ofReal, mul_sub, ←
    ofReal_normSq_eq_inner_self x, ← ofReal_normSq_eq_inner_self y]

Goal state after:
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
⊢ ⟪x, y⟫ * ((starRingEnd 𝕜) ⟪x, y⟫ * ↑(normSq x)) - ↑(normSq x) * ((starRingEnd 𝕜) ⟪x, y⟫ * ⟪x, y⟫) -
        ⟪x, y⟫ * (↑(normSq x) * ⟪y, x⟫) +
      ↑(normSq x) * (↑(normSq x) * ↑(normSq y)) =
    ↑(normSq x * (normSq x * normSq y) - normSq x * ‖⟪x, y⟫‖ ^ 2)
Module: Mathlib.Analysis.InnerProductSpace.Defs

Goal state before:
pp: case e'_4.e'_5
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
t : ℝ
hzero : ¬⟪x, y⟫ = 0
hzero' : ‖⟪x, y⟫‖ ≠ 0
⊢ re ⟪x, x⟫ * t ^ 2 * ‖⟪x, y⟫‖ ^ 2 = t ^ 2 * re ⟪⟪x, y⟫ • x, ⟪x, y⟫ • x⟫

Tactic:
inner_smul_right,

Goal state after:
case e'_4.e'_5
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
t : ℝ
hzero : ¬⟪x, y⟫ = 0
hzero' : ‖⟪x, y⟫‖ ≠ 0
⊢ re ⟪x, x⟫ * t ^ 2 * ‖⟪x, y⟫‖ ^ 2 = t ^ 2 * re (⟪x, y⟫ * ⟪⟪x, y⟫ • x, x⟫)