mathlib-initiative/mathlib-tactics huggingface dataset:
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 : ℝ
hT : DominatedFinMeasAdditive μ T C
ι : Type u_7
f : α → E
hf : AEStronglyMeasurable f μ
fs : ι → α → E
l : Filter ι
hfsi : ∀ᶠ (i : ι) in l, Integrable (fs i) μ
hfs : Tendsto (fun i ↦ ∫⁻ (x : α), ‖fs i x - f x‖ₑ ∂μ) l (𝓝 0)
hl : l.NeBot
hfi : Integrable f μ
f_lp : ↥(Lp E 1 μ) := Integrable.toL1 f hfi
F_lp : ι → ↥(Lp E 1 μ) := fun i ↦ if hFi : Integrable (fs i) μ then Integrable.toL1 (fs i) hFi else 0
tendsto_L1 : Tendsto F_lp l (𝓝 f_lp)
this : Tendsto (fun i ↦ setToFun μ T hT ↑↑(F_lp i)) l (𝓝 (setToFun μ T hT f))
i : ι
hi : Integrable (fs i) μ
⊢ ↑↑(Integrable.toL1 (fs i) hi) =ᵐ[μ] fs i

Tactic:
exact hi.coeFn_toL1

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Bounded.Basic

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
f : α →ᵇ ℝ≥0
x : α
⊢ f x ≤ nndist f 0

Tactic:
by
  have key : nndist (f x) ((0 : α →ᵇ ℝ≥0) x) ≤ nndist f 0 := @dist_coe_le_dist α ℝ≥0 _ _ f 0 x
  simp only [coe_zero, Pi.zero_apply] at key
  rwa [NNReal.nndist_zero_eq_val' (f x)] at key

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Bounded.Normed

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : SeminormedAddCommGroup β
inst✝ : TopologicalSpace γ
f : α →ᵇ β
g : C(γ, α)
⊢ 1 * dist f 0 ≤ ‖f‖

Tactic:
one_mul,

Goal state after:
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : SeminormedAddCommGroup β
inst✝ : TopologicalSpace γ
f : α →ᵇ β
g : C(γ, α)
⊢ dist f 0 ≤ ‖f‖
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 𝕜
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : FiniteDimensional 𝕜 E
f : X → E →L[𝕜] F
⊢ Continuous[inst✝¹, _] f ↔
    ∀ (y : E), Continuous[inst✝¹, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun x ↦ (f x) y

Tactic:
← continuousOn_univ,

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 𝕜
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : FiniteDimensional 𝕜 E
f : X → E →L[𝕜] F
⊢ ContinuousOn f univ ↔ ∀ (y : E), ContinuousOn (fun x ↦ (f x) y) univ
Module: Mathlib.Topology.ContinuousMap.Compact

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : CompactSpace α
inst✝ : PseudoMetricSpace β
⊢ ∀ (s : Set (C(α, β) × C(α, β))),
    s ∈ uniformity C(α, β) ↔
      ∃ t ∈ uniformity (α →ᵇ β),
        ∀ (x y : C(α, β)), ((equivBoundedOfCompact α β) x, (equivBoundedOfCompact α β) y) ∈ t → (x, y) ∈ s

Tactic:
simp only [hasBasis_compactConvergenceUniformity.mem_iff, uniformity_basis_dist_le.mem_iff]

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : CompactSpace α
inst✝ : PseudoMetricSpace β
⊢ ∀ (s : Set (C(α, β) × C(α, β))),
    (∃ i,
        (IsCompact i.1 ∧ ∃ i_1, 0 < i_1 ∧ {p | dist p.1 p.2 ≤ i_1} ⊆ i.2) ∧
          {fg | ∀ x ∈ i.1, (fg.1 x, fg.2 x) ∈ i.2} ⊆ s) ↔
      ∃ t,
        (∃ i, 0 < i ∧ {p | dist p.1 p.2 ≤ i} ⊆ t) ∧
          ∀ (x y : C(α, β)), ((equivBoundedOfCompact α β) x, (equivBoundedOfCompact α β) y) ∈ t → (x, y) ∈ s
Module: Mathlib.Topology.MetricSpace.ThickenedIndicator

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x y : α
h : infEDist x E ≤ infEDist y E
h_le : infEDist y E * (↑δ.toNNReal)⁻¹ ≤ 1
⊢ (infEDist y E - infEDist x E) * (↑δ.toNNReal)⁻¹ ≤ (↑δ.toNNReal)⁻¹ * edist x y

Tactic:
mul_comm,

Goal state after:
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x y : α
h : infEDist x E ≤ infEDist y E
h_le : infEDist y E * (↑δ.toNNReal)⁻¹ ≤ 1
⊢ (↑δ.toNNReal)⁻¹ * (infEDist y E - infEDist x E) ≤ (↑δ.toNNReal)⁻¹ * edist x y
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 δ
s t : Finset δ
inst✝ : ∀ (i : δ), SigmaFinite (μ i)
f : ((i : δ) → X i) → ℝ≥0∞
hf : Measurable f
hst : Disjoint s t
x : (i : δ) → X i
e : ((i : ↥s) → X ↑i) × ((i : ↥t) → X ↑i) ≃ᵐ ((i : ↥(s ∪ t)) → X ↑i) := MeasurableEquiv.piFinsetUnion X hst
⊢ ∫⁻ (y : ((i : ↥s) → X ↑i) × ((j : ↥t) → X ↑j)),
      f
        (updateFinset x (s ∪ t)
          ((MeasurableEquiv.piFinsetUnion X hst) y)) ∂(Measure.pi fun i ↦ μ ↑i).prod (Measure.pi fun j ↦ μ ↑j) =
    ∫⁻ (y : (i : ↥s) → X ↑i),
      ∫⁻ (z : (j : ↥t) → X ↑j), f (updateFinset x (s ∪ t) (e (y, z))) ∂Measure.pi fun j ↦ μ ↑j ∂Measure.pi fun i ↦ μ ↑i

Tactic:
apply lintegral_prod
        apply Measurable.aemeasurable
        exact hf.comp <| measurable_updateFinset.comp e.measurable

Goal state after:
Module: Mathlib.Topology.Order.LeftRightLim

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace α
h'α : OrderTopology α
f : α → β
a : α
h : ∃ y, Tendsto f (𝓝[<] a) (𝓝 y)
h' : 𝓝[<] a = ⊥
⊢ Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))

pp: case inr
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace α
h'α : OrderTopology α
f : α → β
a : α
h : ∃ y, Tendsto f (𝓝[<] a) (𝓝 y)
h' : (𝓝[<] a).NeBot
⊢ Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))

Tactic:
· simp [h']

Goal state after:
case inr
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace α
h'α : OrderTopology α
f : α → β
a : α
h : ∃ y, Tendsto f (𝓝[<] a) (𝓝 y)
h' : (𝓝[<] a).NeBot
⊢ Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
Module: Mathlib.Topology.Order.LeftRightLim

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : T3Space β
f : α → β
a : α
h : Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
this : 𝓝[≤] a = 𝓝[<] a ⊔ pure a
s : Set β
s_mem : s ∈ 𝓝 (leftLim f a)
s_closed : IsClosed[inst✝³] s
h' : 𝓝[<] a = ⊥
⊢ ∀ᶠ (x : α) in 𝓝[<] a, leftLim f x ∈ id s

pp: case inr
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : T3Space β
f : α → β
a : α
h : Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
this : 𝓝[≤] a = 𝓝[<] a ⊔ pure a
s : Set β
s_mem : s ∈ 𝓝 (leftLim f a)
s_closed : IsClosed[inst✝³] s
h' : (𝓝[<] a).NeBot
⊢ ∀ᶠ (x : α) in 𝓝[<] a, leftLim f x ∈ id s

Tactic:
· simp [h']

Goal state after:
case inr
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : T3Space β
f : α → β
a : α
h : Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
this : 𝓝[≤] a = 𝓝[<] a ⊔ pure a
s : Set β
s_mem : s ∈ 𝓝 (leftLim f a)
s_closed : IsClosed[inst✝³] s
h' : (𝓝[<] a).NeBot
⊢ ∀ᶠ (x : α) in 𝓝[<] a, leftLim f x ∈ id s
Module: Mathlib.MeasureTheory.Integral.Bochner.Set

Goal state before:
pp: case hμ
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
s t : Set X
μ : Measure X
ht : NullMeasurableSet t μ
hfs : IntegrableOn f s μ
⊢ Integrable f (μ.restrict (s ∩ t))

Tactic:
exact Integrable.mono_measure hfs (Measure.restrict_mono inter_subset_left le_rfl)

Goal state after:
Module: Mathlib.Topology.Order.LeftRightLim

Goal state before:
pp: case refine_2.refine_1
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
x : α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
h : leftLim f x = rightLim f x
h' : leftLim f x = f x
⊢ ContinuousWithinAt f (Iio x) x

Tactic:
exact hf.continuousWithinAt_Iio_iff_leftLim_eq.2 h'

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
f : R → ℝ
hf : Monotone f
x : R
s : Set ℝ
hs : s ∈ 𝓝 (rightLim f x)
l u : ℝ
hlu : rightLim f x ∈ Ioo l u
lus : Ioo l u ⊆ s
hx : ∀ (y : R), y ≤ x
y : R
⊢ y ∈ Ici x → rightLim f y ∈ s

Tactic:
(hy : x ≤ y)

Goal state after:
R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : TopologicalSpace R
f✝ : StieltjesFunction R
inst✝ : OrderTopology R
f : R → ℝ
hf : Monotone f
x : R
s : Set ℝ
hs : s ∈ 𝓝 (rightLim f x)
l u : ℝ
hlu : rightLim f x ∈ Ioo l u
lus : Ioo l u ⊆ s
hx : ∀ (y : R), y ≤ x
y : R
hy : x ≤ y
⊢ rightLim f y ∈ s
Module: Mathlib.MeasureTheory.Measure.Stieltjes

Goal state before:
pp: case a
R : Type u_1
inst✝³ : LinearOrder R
inst✝² : TopologicalSpace R
f : StieltjesFunction R
inst✝¹ : OrderTopology R
inst✝ : CompactIccSpace R
a : R
c d : ℕ → R
s✝ s : Finset ℕ
IH :
  ∀ t ⊂ s,
    ∀ (b : R), Icc a b ⊆ ⋃ i ∈ ↑t, Iotop (c i) (d i) → ofReal (↑f b - ↑f a) ≤ ∑ i ∈ t, ofReal (↑f (d i) - ↑f (c i))
b : R
ab : a ≤ b
i : ℕ
cv : Icc a b ⊆ Iotop (c i) (d i) ∪ ⋃ x ∈ ↑(s.erase i), Iotop (c x) (d x)
is : i ∈ s
bcd : b ∈ Ioc (c i) (d i)
⊢ Icc a (c i) ⊆ ⋃ i_1 ∈ ↑(s.erase i), Iotop (c i_1) (d i_1)

Tactic:
rintro x ⟨h₁, h₂⟩
    apply (cv ⟨h₁, le_trans h₂ (le_of_lt bcd.1)⟩).resolve_left (fun h ↦ ?_)
    order [(Iotop_subset_Ioc h).1]

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

Goal state before:
pp: case pos
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
t : Set X
μ : Measure X
ht_eq : ∀ᵐ (x : X) ∂μ, x ∈ t → f x = 0
hf : AEStronglyMeasurable f (μ.restrict t)
this : ∫ (x : X) in t, AEStronglyMeasurable.mk f hf x ∂μ = 0
⊢ ∫ (x : X) in t, f x ∂μ = ∫ (x : X) in t, AEStronglyMeasurable.mk f hf x ∂μ

Tactic:
exact integral_congr_ae hf.ae_eq_mk

Goal state after:
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
f : X → E
s t : Set X
μ : Measure X
ht_eq : ∀ᵐ (x : X) ∂μ.restrict t, f x = 0
haux : StronglyMeasurable f
H : IntegrableOn f (s ∪ t) μ
k : Set X := f ⁻¹' {0}
hk : MeasurableSet k
h's : IntegrableOn f s μ
A : ∀ (u : Set X), ∫ (x : X) in u ∩ k, f x ∂μ = 0
⊢ ∫ (x : X) in s ∪ t, f x ∂μ = ∫ (x : X) in s, f x ∂μ

Tactic:
rw [← integral_inter_add_sdiff hk h's, ← integral_inter_add_sdiff hk H, A, A, zero_add, zero_add,
    union_sdiff_distrib, union_comm]

Goal state after:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
s t : Set X
μ : Measure X
ht_eq : ∀ᵐ (x : X) ∂μ.restrict t, f x = 0
haux : StronglyMeasurable f
H : IntegrableOn f (s ∪ t) μ
k : Set X := f ⁻¹' {0}
hk : MeasurableSet k
h's : IntegrableOn f s μ
A : ∀ (u : Set X), ∫ (x : X) in u ∩ k, f x ∂μ = 0
⊢ ∫ (x : X) in t \ k ∪ s \ k, f x ∂μ = ∫ (x : X) in s \ k, f x ∂μ
Module: Mathlib.MeasureTheory.Integral.Bochner.Set

Goal state before:
pp: X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
hfi : Integrable f μ
h_meas : NullMeasurableSet {x | 0 ≤ f x} μ
⊢ ∫ (x : X) in {x | 0 ≤ f x}, ‖f x‖ ∂μ + ∫ (x : X) in {x | 0 ≤ f x}ᶜ, ‖f x‖ ∂μ =
    ∫ (x : X) in {x | 0 ≤ f x}, f x ∂μ + ∫ (x : X) in {x | 0 ≤ f x}ᶜ, ‖f x‖ ∂μ

Tactic:
congr 1
      refine setIntegral_congr_fun₀ h_meas fun x hx => ?_
      rw [Real.norm_eq_abs, abs_eq_self.mpr _]
      exact hx

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
g : G
hg : g ∈ K
g₀ : G
h1g₀ : g₀ ∈ s
h2g₀ : g ∈ (fun h ↦ (fun x ↦ g₀ * x) ⁻¹' V) h1g₀
⊢ g ∈ ⋃ g ∈ {g ∈ s | ((fun x ↦ g * x) ⁻¹' V ∩ K).Nonempty}, (fun h ↦ g * h) ⁻¹' V

Tactic:
simp only [mem_preimage] at h2g₀

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 : G
hg : g ∈ K
g₀ : G
h1g₀ : g₀ ∈ s
h2g₀ : g₀ * g ∈ V
⊢ g ∈ ⋃ g ∈ {g ∈ s | ((fun x ↦ g * x) ⁻¹' V ∩ K).Nonempty}, (fun h ↦ g * h) ⁻¹' V
Module: Mathlib.MeasureTheory.Group.FundamentalDomain

Goal state before:
pp: G : Type u_1
α : Type u_3
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MeasurableSpace α
ν : Measure α
hasFun : HasFundamentalDomain G α ν
μ μ' : Measure (Quotient α_mod_G)
inst✝¹ : QuotientMeasureEqMeasurePreimage ν μ
inst✝ : QuotientMeasureEqMeasurePreimage ν μ'
⊢ μ = μ'

Tactic:
obtain ⟨𝓕, h𝓕⟩ := hasFun.ExistsIsFundamentalDomain

Goal state after:
G : Type u_1
α : Type u_3
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MeasurableSpace α
ν : Measure α
hasFun : HasFundamentalDomain G α ν
μ μ' : Measure (Quotient α_mod_G)
inst✝¹ : QuotientMeasureEqMeasurePreimage ν μ
inst✝ : QuotientMeasureEqMeasurePreimage ν μ'
𝓕 : Set α
h𝓕 : IsFundamentalDomain G 𝓕 ν
⊢ μ = μ'
Module: Mathlib.MeasureTheory.Integral.Bochner.Set

Goal state before:
pp: case hf
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
R : ℝ
f : X → ℝ
hR : 0 ≤ R
hfint : IntegrableOn f {x | R < f x} μ
hμ : μ {x | R < f x} ≠ 0
this : IntegrableOn (fun x ↦ R) {x | R < f x} μ
⊢ ∀ᵐ (x : X) ∂μ, x ∈ {x | R < f x} → 0 ≤ f x - R

pp: case hf
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
R : ℝ
f : X → ℝ
hR : 0 ≤ R
hfint : IntegrableOn f {x | R < f x} μ
hμ : μ {x | R < f x} ≠ 0
this : IntegrableOn (fun x ↦ R) {x | R < f x} μ
⊢ NullMeasurableSet {x | 0 ≤ f x - R} (μ.restrict {x | R < f x})

Tactic:
· exact Eventually.of_forall fun x hx => sub_nonneg.2 <| le_of_lt hx

Goal state after:
case hf
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
R : ℝ
f : X → ℝ
hR : 0 ≤ R
hfint : IntegrableOn f {x | R < f x} μ
hμ : μ {x | R < f x} ≠ 0
this : IntegrableOn (fun x ↦ R) {x | R < f x} μ
⊢ NullMeasurableSet {x | 0 ≤ f x - R} (μ.restrict {x | R < f x})
Module: Mathlib.MeasureTheory.Integral.Bochner.Set

Goal state before:
pp: X : Type u_1
mX : MeasurableSpace X
μ : Measure X
R : ℝ
f : X → ℝ
hR : 0 ≤ R
hfint : IntegrableOn f {x | R < f x} μ
hμ : μ {x | R < f x} ≠ 0
⊢ μ.real {x | R < f x} * R < ∫ (x : X) in {x | R < f x}, f x ∂μ

Tactic:
by
  have : IntegrableOn (fun _ => R) {x | ↑R < f x} μ := by
    refine ⟨aestronglyMeasurable_const, lt_of_le_of_lt ?_ hfint.2⟩
    refine setLIntegral_mono_ae hfint.1.enorm <| ae_of_all _ fun x hx => ?_
    simp only [ENNReal.coe_le_coe, Real.nnnorm_of_nonneg hR, enorm_eq_nnnorm,
      Real.nnnorm_of_nonneg (hR.trans <| le_of_lt hx)]
    exact le_of_lt hx
  rw [← sub_pos, ← smul_eq_mul, ← setIntegral_const, ← integral_sub hfint this,
    setIntegral_pos_iff_support_of_nonneg_ae]
  · rw [← pos_iff_ne_zero] at hμ
    rwa [Set.inter_eq_self_of_subset_right]
    exact fun x hx => Ne.symm (ne_of_lt <| sub_pos.2 hx)
  · rw [Pi.zero_def, EventuallyLE, ae_restrict_iff₀]
    · exact Eventually.of_forall fun x hx => sub_nonneg.2 <| le_of_lt hx
    · exact nullMeasurableSet_le aemeasurable_zero (hfint.1.aemeasurable.sub aemeasurable_const)
  · exact Integrable.sub hfint this

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 : Set G
hK : IsCompact K
g : G
V : Set G
hV : (interior V).Nonempty
⊢ index ((fun h ↦ g * h) '' K) V = index K V

Tactic:
refine le_antisymm (mul_left_index_le hK hV g) ?_

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K : Set G
hK : IsCompact K
g : G
V : Set G
hV : (interior V).Nonempty
⊢ index K V ≤ index ((fun h ↦ g * h) '' K) V
Module: Mathlib.MeasureTheory.Group.FundamentalDomain

Goal state before:
pp: G : Type u_1
α : Type u_3
inst✝⁶ : Group G
inst✝⁵ : MulAction G α
inst✝⁴ : MeasurableSpace α
ν : Measure α
inst✝³ : SMulInvariantMeasure G α ν
inst✝² : Countable G
inst✝¹ : MeasurableConstSMul G α
μ : Measure (Quotient α_mod_G)
inst✝ : QuotientMeasureEqMeasurePreimage ν μ
hasFun : HasFundamentalDomain G α ν
h : covolume G α ν ≠ ∞
⊢ IsFiniteMeasure μ

Tactic:
obtain ⟨𝓕, h𝓕⟩ := hasFun.ExistsIsFundamentalDomain

Goal state after:
G : Type u_1
α : Type u_3
inst✝⁶ : Group G
inst✝⁵ : MulAction G α
inst✝⁴ : MeasurableSpace α
ν : Measure α
inst✝³ : SMulInvariantMeasure G α ν
inst✝² : Countable G
inst✝¹ : MeasurableConstSMul G α
μ : Measure (Quotient α_mod_G)
inst✝ : QuotientMeasureEqMeasurePreimage ν μ
hasFun : HasFundamentalDomain G α ν
h : covolume G α ν ≠ ∞
𝓕 : Set α
h𝓕 : IsFundamentalDomain G 𝓕 ν
⊢ IsFiniteMeasure μ
Module: Mathlib.MeasureTheory.Group.FundamentalDomain

Goal state before:
pp: case pos
G : Type u_1
α : Type u_3
inst✝⁷ : Group G
inst✝⁶ : MulAction G α
inst✝⁵ : MeasurableSpace α
ν : Measure α
inst✝⁴ : SMulInvariantMeasure G α ν
inst✝³ : Countable G
inst✝² : MeasurableConstSMul G α
μ : Measure (Quotient α_mod_G)
inst✝¹ : QuotientMeasureEqMeasurePreimage ν μ
inst✝ : IsFiniteMeasure μ
hasFun : HasFundamentalDomain G α ν
⊢ covolume G α ν < ∞

Tactic:
obtain ⟨𝓕, h𝓕⟩ := hasFun.ExistsIsFundamentalDomain

Goal state after:
case pos
G : Type u_1
α : Type u_3
inst✝⁷ : Group G
inst✝⁶ : MulAction G α
inst✝⁵ : MeasurableSpace α
ν : Measure α
inst✝⁴ : SMulInvariantMeasure G α ν
inst✝³ : Countable G
inst✝² : MeasurableConstSMul G α
μ : Measure (Quotient α_mod_G)
inst✝¹ : QuotientMeasureEqMeasurePreimage ν μ
inst✝ : IsFiniteMeasure μ
hasFun : HasFundamentalDomain G α ν
𝓕 : Set α
h𝓕 : IsFundamentalDomain G 𝓕 ν
⊢ covolume G α ν < ∞
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
U : Set G
K₁ K₂ : Compacts G
hU : (interior U).Nonempty
h : Disjoint (K₁.carrier * U⁻¹) (K₂.carrier * U⁻¹)
⊢ prehaar (↑K₀) U (K₁ ⊔ K₂) = prehaar (↑K₀) U K₁ + prehaar (↑K₀) U K₂

Tactic:
by
  simp only [prehaar]; rw [← add_div]
  -- Porting note: Here was `congr`, but `to_additive` failed to generate a theorem.
  refine congr_arg (fun x : ℝ => x / index K₀ U) ?_
  exact mod_cast index_union_eq K₁ K₂ hU h

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

Goal state before:
pp: case hf
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
f_int : Integrable f μ
f_nonneg : 0 ≤ᵐ[μ] f
s : Set X
hs : ∀ x ∈ s, 1 ≤ f x
⊢ AEMeasurable (fun a ↦ ENNReal.ofReal (f a)) μ

pp: case hs
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
f_int : Integrable f μ
f_nonneg : 0 ≤ᵐ[μ] f
s : Set X
hs : ∀ x ∈ s, 1 ≤ f x
⊢ ∀ x ∈ s, 1 ≤ ENNReal.ofReal (f x)

Tactic:
· exact ENNReal.continuous_ofReal.measurable.comp_aemeasurable f_int.1.aemeasurable

Goal state after:
case hs
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
f_int : Integrable f μ
f_nonneg : 0 ≤ᵐ[μ] f
s : Set X
hs : ∀ x ∈ s, 1 ≤ f x
⊢ ∀ x ∈ s, 1 ≤ ENNReal.ofReal (f x)
Module: Mathlib.MeasureTheory.Integral.Bochner.Set

Goal state before:
pp: X : Type u_6
f : X → ℝ
m0 : MeasurableSpace X
μ : Measure X
g : SimpleFunc X ℝ
hf : Integrable f μ
c : ℝ
s : Set X
hs : MeasurableSet s
⊢ Integrable (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const X c) (SimpleFunc.const X 0)) * f) μ

Tactic:
simp only [SimpleFunc.const_zero, SimpleFunc.coe_piecewise, SimpleFunc.coe_const,
    SimpleFunc.coe_zero, Set.piecewise_eq_indicator]

Goal state after:
X : Type u_6
f : X → ℝ
m0 : MeasurableSpace X
μ : Measure X
g : SimpleFunc X ℝ
hf : Integrable f μ
c : ℝ
s : Set X
hs : MeasurableSet s
⊢ Integrable (s.indicator (const X c) * f) μ
Module: Mathlib.Analysis.InnerProductSpace.Defs

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
cd : PreInnerProductSpace.Core 𝕜 F
this : NormedSpace 𝕜 F := Core.toNormedSpace
x : F
⊢ ‖x‖ ^ 2 = re ⟪x, x⟫_𝕜

Tactic:
by
      have h₁ : ‖x‖ ^ 2 = √(re (cd.inner x x)) ^ 2 := rfl
      have h₂ : 0 ≤ re (cd.inner x x) := InnerProductSpace.Core.inner_self_nonneg
      simp [h₁, sq_sqrt, h₂]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : AddCommGroup F
hF : Module 𝕜 F
inst✝² : TopologicalSpace F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousConstSMul 𝕜 F
cd : Core 𝕜 F
h : ContinuousAt (fun v ↦ ⟪v, v⟫_𝕜) 0
h' : IsVonNBounded 𝕜 {v | re ⟪v, v⟫_𝕜 < 1}
this✝ : NormedAddCommGroup F := Core.toNormedAddCommGroupOfTopology h h'
this : NormedSpace 𝕜 F := Core.toNormedSpaceOfTopology h h'
x : F
⊢ ‖x‖ ^ 2 = re ⟪x, x⟫_𝕜

Tactic:
by
      have h₁ : ‖x‖ ^ 2 = √(re (cd.inner x x)) ^ 2 := rfl
      have h₂ : 0 ≤ re (cd.inner x x) := InnerProductSpace.Core.inner_self_nonneg
      simp [h₁, sq_sqrt, h₂]

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
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : μ.IsHaarMeasure
inst✝¹ : μ.InnerRegularCompactLTTop
inst✝ : LocallyCompactSpace G
E : Set G
hE : MeasurableSet E
hEapprox : ∃ K ⊆ E, IsCompact K ∧ 0 < μ K
⊢ E / E ∈ 𝓝 1

Tactic:
by
  /- For any measure `μ` and set `E` containing a compact set `K` of positive measure, there exists
  a neighborhood `V` of the identity such that `v • K \ K` has small measure for all `v ∈ V`, say
  `< μ K`. Then `v • K` and `K` cannot be disjoint, as otherwise `μ (v • K \ K) = μ (v • K) = μ K`.
  This show that `K / K` contains the neighborhood `V` of `1`, and therefore that it is
  itself such a neighborhood. -/
  obtain ⟨K, hKE, hK, K_closed, hKpos⟩ : ∃ K ⊆ E, IsCompact K ∧ IsClosed K ∧ 0 < μ K := by
    obtain ⟨K, hKE, hK_comp, hK_meas⟩ := hEapprox
    exact ⟨closure K, hK_comp.closure_subset_measurableSet hE hKE, hK_comp.closure,
      isClosed_closure, by rwa [hK_comp.measure_closure]⟩
  filter_upwards [eventually_nhds_one_measure_smul_sdiff_lt hK K_closed hKpos.ne' (μ := μ)]
    with g hg
  obtain ⟨_, ⟨x, hxK, rfl⟩, hgxK⟩ : ∃ x ∈ g • K, x ∈ K :=
     not_disjoint_iff.1 fun hd ↦ by simp [hd.symm.sdiff_eq_right, measure_smul] at hg
  simpa using div_mem_div (hKE hgxK) (hKE hxK)

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

Goal state before:
pp: F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
ι₁ : Type u_4
s₁ : Finset ι₁
w₁ : ι₁ → ℝ
v₁ : ι₁ → F
h₁ : ∑ i ∈ s₁, w₁ i = 0
ι₂ : Type u_5
s₂ : Finset ι₂
w₂ : ι₂ → ℝ
v₂ : ι₂ → F
h₂ : ∑ i ∈ s₂, w₂ i = 0
⊢ 0 - ∑ x ∈ s₁, w₁ x * ∑ i ∈ s₂, w₂ i * (‖v₁ x - v₂ i‖ * ‖v₁ x - v₂ i‖ / 2) =
    (-∑ i₁ ∈ s₁, ∑ i₂ ∈ s₂, w₁ i₁ * w₂ i₂ * (‖v₁ i₁ - v₂ i₂‖ * ‖v₁ i₁ - v₂ i₂‖)) / 2

Tactic:
zero_sub,

Goal state after:
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
ι₁ : Type u_4
s₁ : Finset ι₁
w₁ : ι₁ → ℝ
v₁ : ι₁ → F
h₁ : ∑ i ∈ s₁, w₁ i = 0
ι₂ : Type u_5
s₂ : Finset ι₂
w₂ : ι₂ → ℝ
v₂ : ι₂ → F
h₂ : ∑ i ∈ s₂, w₂ i = 0
⊢ -∑ x ∈ s₁, w₁ x * ∑ i ∈ s₂, w₂ i * (‖v₁ x - v₂ i‖ * ‖v₁ x - v₂ i‖ / 2) =
    (-∑ i₁ ∈ s₁, ∑ i₂ ∈ s₂, w₁ i₁ * w₂ i₂ * (‖v₁ i₁ - v₂ i₂‖ * ‖v₁ i₁ - v₂ i₂‖)) / 2
Module: Mathlib.Analysis.InnerProductSpace.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
r : 𝕜
hx : x ≠ 0
hr : r ≠ 0
hx' : ‖x‖ ≠ 0
hr' : ‖r‖ ≠ 0
⊢ ‖r‖ * ‖x‖ / ‖r‖ / ‖x‖ = 1

Tactic:
mul_comm,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
r : 𝕜
hx : x ≠ 0
hr : r ≠ 0
hx' : ‖x‖ ≠ 0
hr' : ‖r‖ ≠ 0
⊢ ‖x‖ * ‖r‖ / ‖r‖ / ‖x‖ = 1