mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: case neg
α : 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
hf : Integrable f μ
hF : ¬CompleteSpace F
⊢ ‖setToFun μ T hT f‖ ≤ max C 0 * ‖Integrable.toL1 f hf‖

Tactic:
simp only [setToFun, hF, ↓reduceDIte, norm_zero]

Goal state after:
case neg
α : 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
hf : Integrable f μ
hF : ¬CompleteSpace F
⊢ 0 ≤ max C 0 * ‖Integrable.toL1 f hf‖
Module: Mathlib.MeasureTheory.Integral.Marginal

Goal state before:
pp: 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
⊢ (∫⋯∫⁻_Finset.univ, f ∂μ) x ≤ (∫⋯∫⁻_Finset.univ, g ∂μ) x

Tactic:
lmarginal_le_of_subset (Finset.subset_univ s) hf hg hfg x

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

Goal state before:
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) (𝓝 ((𝓝[<] a).limUnder f))

Tactic:
exact tendsto_nhds_limUnder h

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 α
inst✝ : OrderTopology α
f : α → β
a : α
A : (𝓝 (f a) ⊓ map f (𝓝[≤] a)).NeBot
h' : 𝓝[<] a = ⊥
⊢ MapClusterPt (leftLim f a) (𝓝[≤] a) f

pp: case inr
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → β
a : α
A : (𝓝 (f a) ⊓ map f (𝓝[≤] a)).NeBot
h' : (𝓝[<] a).NeBot
⊢ MapClusterPt (leftLim f a) (𝓝[≤] a) f

Tactic:
· simp only [MapClusterPt, ClusterPt, h', leftLim_eq_of_eq_bot, A]

Goal state after:
case inr
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → β
a : α
A : (𝓝 (f a) ⊓ map f (𝓝[≤] a)).NeBot
h' : (𝓝[<] a).NeBot
⊢ MapClusterPt (leftLim f a) (𝓝[≤] a) f
Module: Mathlib.Topology.Order.LeftRightLim

Goal state before:
pp: case inr.refine_2
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x ≤ y
this✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
h' : (𝓝[<] x).NeBot
z : α
⊢ z < x → f z ≤ f y

Tactic:
hz

Goal state after:
case inr.refine_2
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x ≤ y
this✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
h' : (𝓝[<] x).NeBot
z : α
hz : z < x
⊢ f z ≤ f y
Module: Mathlib.Topology.Order.LeftRightLim

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x < y
this✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
h' : (𝓝[<] y).NeBot
z : α
⊢ z < y → f z ≤ f y

Tactic:
hz

Goal state after:
case inr
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x < y
this✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
h' : (𝓝[<] y).NeBot
z : α
hz : z < y
⊢ f z ≤ f y
Module: Mathlib.Topology.Order.LeftRightLim

Goal state before:

Tactic:
rightLim f x ≤ f a := hf.rightLim_le xa
    _ ≤ leftLim f y := hf.le_leftLim ay

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

Goal state before:
pp: case refine_2
α : 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
inst✝ : Countable ι
F : ι → α → E
f : α → E
bound : ι → α → ℝ
hF_meas : ∀ (n : ι), AEStronglyMeasurable (F n) μ
h_bound : ∀ (n : ι), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound n a
bound_summable : ∀ᵐ (a : α) ∂μ, Summable fun n ↦ bound n a
bound_integrable : Integrable (fun a ↦ ∑' (n : ι), bound n a) μ
h_lim : ∀ᵐ (a : α) ∂μ, HasSum (fun n ↦ F n a) (f a)
hb_nonneg : ∀ᵐ (a : α) ∂μ, ∀ (n : ι), 0 ≤ bound n a
hb_le_tsum : ∀ (n : ι), bound n ≤ᵐ[μ] fun a ↦ ∑' (n : ι), bound n a
hF_integrable : ∀ (n : ι), Integrable (F n) μ
s : Finset ι
⊢ ∀ᵐ (a : α) ∂μ, ‖∑ i ∈ s, F i a‖ ≤ ∑' (n : ι), bound n a

Tactic:
filter_upwards [eventually_countable_forall.2 h_bound, hb_nonneg, bound_summable]
      with a hFa ha0 has

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 : ℝ
hT : DominatedFinMeasAdditive μ T C
ι : Type u_7
inst✝ : Countable ι
F : ι → α → E
f : α → E
bound : ι → α → ℝ
hF_meas : ∀ (n : ι), AEStronglyMeasurable (F n) μ
h_bound : ∀ (n : ι), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound n a
bound_summable : ∀ᵐ (a : α) ∂μ, Summable fun n ↦ bound n a
bound_integrable : Integrable (fun a ↦ ∑' (n : ι), bound n a) μ
h_lim : ∀ᵐ (a : α) ∂μ, HasSum (fun n ↦ F n a) (f a)
hb_nonneg : ∀ᵐ (a : α) ∂μ, ∀ (n : ι), 0 ≤ bound n a
hb_le_tsum : ∀ (n : ι), bound n ≤ᵐ[μ] fun a ↦ ∑' (n : ι), bound n a
hF_integrable : ∀ (n : ι), Integrable (F n) μ
s : Finset ι
a : α
hFa : ∀ (i : ι), ‖F i a‖ ≤ bound i a
ha0 : ∀ (n : ι), 0 ≤ bound n a
has : Summable fun n ↦ bound n a
⊢ ‖∑ i ∈ s, F i a‖ ≤ ∑' (n : ι), bound n a
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
y₀ : R
hy₀ : x < y₀
y : R
xy : x < y
h'y : Ioo x y ⊆ f ⁻¹' Ioo l u
z : R
⊢ z ∈ Ico x y → rightLim f z ∈ s

Tactic:
hz

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
y₀ : R
hy₀ : x < y₀
y : R
xy : x < y
h'y : Ioo x y ⊆ f ⁻¹' Ioo l u
z : R
hz : z ∈ Ico x y
⊢ rightLim f z ∈ s
Module: Mathlib.MeasureTheory.Measure.Stieltjes

Goal state before:
pp: case inl
R : Type u_1
inst✝¹ : LinearOrder R
inst✝ : TopologicalSpace R
f : StieltjesFunction R
a b : R
this : Nonempty R
a' b' : R
h : Ioc a b \ botSet ⊆ Ioc a' b'
ab : b ≤ a
⊢ (↑f b - ↑f a).toNNReal ≤ (↑f b' - ↑f a').toNNReal

Tactic:
Real.toNNReal_of_nonpos (sub_nonpos.2 (f.mono ab))

Goal state after:
case inl
R : Type u_1
inst✝¹ : LinearOrder R
inst✝ : TopologicalSpace R
f : StieltjesFunction R
a b : R
this : Nonempty R
a' b' : R
h : Ioc a b \ botSet ⊆ Ioc a' b'
ab : b ≤ a
⊢ 0 ≤ (↑f b' - ↑f a').toNNReal
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
μ : Measure X
ι : Type u_5
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set X
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
h_mono : Monotone s
hfi : IntegrableOn f (⋃ n, s n) μ
hne : atTop.NeBot
this : IsDirectedOrder ι
hfi' : ∫⁻ (x : X) in ⋃ n, s n, ↑‖f x‖₊ ∂μ < ∞
⊢ Tendsto (fun i ↦ ∫ (x : X) in s i, f x ∂μ) atTop (𝓝 (∫ (x : X) in ⋃ n, s n, f x ∂μ))

Tactic:
set S := ⋃ i, s i

Goal state after:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set X
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
h_mono : Monotone s
hne : atTop.NeBot
this : IsDirectedOrder ι
S : Set X := ⋃ i, s i
hfi : IntegrableOn f S μ
hfi' : ∫⁻ (x : X) in S, ↑‖f x‖₊ ∂μ < ∞
⊢ Tendsto (fun i ↦ ∫ (x : X) in s i, f x ∂μ) atTop (𝓝 (∫ (x : X) in S, f x ∂μ))
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
μ : Measure X
ι : Type u_5
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set X
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
h_mono : Monotone s
hne : atTop.NeBot
this✝ : IsDirectedOrder ι
S : Set X := ⋃ i, s i
hfi : IntegrableOn f S μ
hfi' : (μ.withDensity fun x ↦ ↑‖f x‖₊) S < ∞
hSm : NullMeasurableSet S μ
hsub : ∀ {i : ι}, s i ⊆ S
ν : Measure X := μ.withDensity fun x ↦ ‖f x‖ₑ
hν : ν = μ.withDensity fun x ↦ ‖f x‖ₑ
ε : ℝ≥0
ε0 : 0 < ↑ε
this : ∀ᶠ (i : ι) in atTop, ν (s i) ∈ Icc (ν S - ↑ε) (ν S + ↑ε)
i : ι
hi : ν (s i) ∈ Icc (ν S - ↑ε) (ν S + ↑ε)
⊢ ↑‖∫ (x : X) in S \ s i, f x ∂μ‖₊ ≤ ↑ε

Tactic:
NNReal.coe_le_coe,

Goal state after:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set X
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
h_mono : Monotone s
hne : atTop.NeBot
this✝ : IsDirectedOrder ι
S : Set X := ⋃ i, s i
hfi : IntegrableOn f S μ
hfi' : (μ.withDensity fun x ↦ ↑‖f x‖₊) S < ∞
hSm : NullMeasurableSet S μ
hsub : ∀ {i : ι}, s i ⊆ S
ν : Measure X := μ.withDensity fun x ↦ ‖f x‖ₑ
hν : ν = μ.withDensity fun x ↦ ‖f x‖ₑ
ε : ℝ≥0
ε0 : 0 < ↑ε
this : ∀ᶠ (i : ι) in atTop, ν (s i) ∈ Icc (ν S - ↑ε) (ν S + ↑ε)
i : ι
hi : ν (s i) ∈ Icc (ν S - ↑ε) (ν S + ↑ε)
⊢ ‖∫ (x : X) in S \ s i, f x ∂μ‖₊ ≤ ε
Module: Mathlib.MeasureTheory.Integral.Bochner.Set

Goal state before:
pp: case e'_5
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set X
hsm : ∀ (i : ι), MeasurableSet (s i)
h_anti : Antitone s
hne : atTop.NeBot
this✝ : IsDirectedOrder ι
i₀ : ι
hi₀ : IntegrableOn f (s i₀) μ
this :
  Tendsto (fun x ↦ ∫ (x : X) in s i₀, f x ∂μ - ∫ (x : X) in s i₀ \ s x, f x ∂μ) atTop
    (𝓝 (∫ (x : X) in s i₀, f x ∂μ - ∫ (x : X) in ⋃ i, s i₀ \ s i, f x ∂μ))
⊢ ∫ (x : X) in ⋂ n, s n, f x ∂μ = ∫ (x : X) in s i₀, f x ∂μ - ∫ (x : X) in ⋃ i, s i₀ \ s i, f x ∂μ

pp: case convert_2
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set X
hsm : ∀ (i : ι), MeasurableSet (s i)
h_anti : Antitone s
hne : atTop.NeBot
this✝ : IsDirectedOrder ι
i₀ : ι
hi₀ : IntegrableOn f (s i₀) μ
this :
  Tendsto (fun x ↦ ∫ (x : X) in s i₀, f x ∂μ - ∫ (x : X) in s i₀ \ s x, f x ∂μ) atTop
    (𝓝 (∫ (x : X) in s i₀, f x ∂μ - ∫ (x : X) in ⋃ i, s i₀ \ s i, f x ∂μ))
i : ι
hi : i₀ ≤ i
⊢ ∫ (x : X) in s i₀, f x ∂μ - ∫ (x : X) in s i₀ \ s i, f x ∂μ = ∫ (x : X) in s i, f x ∂μ

Tactic:
· rw [← sdiff_iInter, setIntegral_sdiff _ hi₀ (iInter_subset _ _), sub_sub_cancel]
      exact .iInter_of_antitone h_anti hsm

Goal state after:
case convert_2
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set X
hsm : ∀ (i : ι), MeasurableSet (s i)
h_anti : Antitone s
hne : atTop.NeBot
this✝ : IsDirectedOrder ι
i₀ : ι
hi₀ : IntegrableOn f (s i₀) μ
this :
  Tendsto (fun x ↦ ∫ (x : X) in s i₀, f x ∂μ - ∫ (x : X) in s i₀ \ s x, f x ∂μ) atTop
    (𝓝 (∫ (x : X) in s i₀, f x ∂μ - ∫ (x : X) in ⋃ i, s i₀ \ s i, f x ∂μ))
i : ι
hi : i₀ ≤ i
⊢ ∫ (x : X) in s i₀, f x ∂μ - ∫ (x : X) in s i₀ \ s i, f x ∂μ = ∫ (x : X) in s i, f x ∂μ
Module: Mathlib.MeasureTheory.Measure.Content

Goal state before:
pp: G : Type w
inst✝ : TopologicalSpace G
⊢ Function.Injective fun μ s ↦ ↑(μ.toFun s)

Tactic:
by
    rintro ⟨μ, _, _⟩ ⟨v, _, _⟩ h; congr!; ext s : 1; exact ENNReal.coe_injective <| congr_fun h s

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

Goal state before:
pp: case neg
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 : Integrable f (μ.restrict t)
⊢ AEStronglyMeasurable f (μ.restrict t)

Tactic:
exact hf.1

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) μ
⊢ ∫ (x : X) in s ∪ t, f x ∂μ = ∫ (x : X) in s, f x ∂μ

Tactic:
let k := f ⁻¹' {0}
  have hk : MeasurableSet k := by borelize E; exact haux.measurable (measurableSet_singleton _)
  have h's : IntegrableOn f s μ := H.mono subset_union_left le_rfl
  have A : ∀ u : Set X, ∫ x in u ∩ k, f x ∂μ = 0 := fun u =>
    setIntegral_eq_zero_of_forall_eq_zero fun x hx => hx.2
  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]
  apply setIntegral_congr_set
  rw [union_ae_eq_right]
  apply measure_mono_null sdiff_subset
  rw [measure_eq_zero_iff_ae_notMem]
  filter_upwards [ae_imp_of_ae_restrict ht_eq] with x hx h'x using h'x.2 (hx h'x.1)

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 }
⊢ (⨆ x, μ ↑x) + μ.outerMeasure (↑U' \ U) ≤ μ.outerMeasure ↑U'

Tactic:
rw [ENNReal.iSup_add]

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 }
⊢ ⨆ i, μ ↑i + μ.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
A : Set G
hA : MeasurableSet A
r : ℝ≥0∞
hr : μ.measure A < r
⊢ ∃ U ⊇ A, IsOpen U ∧ μ.measure U < r

Tactic:
μ.measure_apply hA,

Goal state after:
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : R1Space G
S : MeasurableSpace G
inst✝ : BorelSpace G
A : Set G
hA : MeasurableSet A
r : ℝ≥0∞
hr : μ.outerMeasure A < r
⊢ ∃ U ⊇ A, IsOpen U ∧ μ.measure U < r
Module: Mathlib.MeasureTheory.Integral.Bochner.Set

Goal state before:
pp: E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
X : Type u_5
m m0 : MeasurableSpace X
μ : Measure X
hm : m ≤ m0
f : X → E
hf_meas : StronglyMeasurable f
s : Set X
hs : MeasurableSet s
⊢ ∫ (x : X), f x ∂(μ.restrict s).trim hm = ∫ (x : X) in s, f x ∂μ.trim hm

Tactic:
restrict_trim hm μ

Goal state after:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
X : Type u_5
m m0 : MeasurableSpace X
μ : Measure X
hm : m ≤ m0
f : X → E
hf_meas : StronglyMeasurable f
s : Set X
hs : MeasurableSet s
⊢ ∫ (x : X), f x ∂(μ.restrict s).trim hm = ∫ (x : X), f x ∂(μ.restrict s).trim hm

E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
X : Type u_5
m m0 : MeasurableSpace X
μ : Measure X
hm : m ≤ m0
f : X → E
hf_meas : StronglyMeasurable f
s : Set X
hs : MeasurableSet s
⊢ MeasurableSet s
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 : ℝ
⊢ (starRingEnd 𝕜) ↑t * ⟪x, y⟫ = ⟪x, y⟫ * ↑t

Tactic:
conj_ofReal,

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.Integral.Bochner.Set

Goal state before:
pp: X : Type u_1
F : Type u_4
mX : MeasurableSpace X
𝕜 : Type u_5
inst✝³ : NormedRing 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : Module 𝕜 F
inst✝ : IsBoundedSMul 𝕜 F
p : ℝ≥0∞
μ : Measure X
c : 𝕜
f : ↥(Lp F p μ)
s : Set X
⊢ ∀ᵐ (x : X) ∂μ.restrict s,
    ↑↑(MemLp.toLp ↑↑f ⋯) x = ↑↑f x →
      ↑↑(c • f) x = (c • ↑↑f) x → ↑↑(MemLp.toLp ↑↑(c • f) ⋯) x = ↑↑(c • MemLp.toLp ↑↑f ⋯) x

Tactic:
refine (MemLp.coeFn_toLp ((Lp.memLp (c • f)).restrict s)).mp ?_

Goal state after:
X : Type u_1
F : Type u_4
mX : MeasurableSpace X
𝕜 : Type u_5
inst✝³ : NormedRing 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : Module 𝕜 F
inst✝ : IsBoundedSMul 𝕜 F
p : ℝ≥0∞
μ : Measure X
c : 𝕜
f : ↥(Lp F p μ)
s : Set X
⊢ ∀ᵐ (x : X) ∂μ.restrict s,
    ↑↑(MemLp.toLp ↑↑(c • f) ⋯) x = ↑↑(c • f) x →
      ↑↑(MemLp.toLp ↑↑f ⋯) x = ↑↑f x →
        ↑↑(c • f) x = (c • ↑↑f) x → ↑↑(MemLp.toLp ↑↑(c • f) ⋯) x = ↑↑(c • MemLp.toLp ↑↑f ⋯) x
Module: Mathlib.Analysis.InnerProductSpace.Defs

Goal state before:
pp: case pos
𝕜 : 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
⊢ 0 ≤ normSq x * (t * t) + 2 * ‖⟪x, y⟫‖ * t + normSq y

pp: case neg
𝕜 : 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
⊢ 0 ≤ normSq x * (t * t) + 2 * ‖⟪x, y⟫‖ * t + normSq y

Tactic:
· simp only [← sq, hzero, norm_zero, mul_zero, zero_mul, add_zero]
    obtain ⟨hx, hy⟩ : (0 ≤ normSqF x ∧ 0 ≤ normSqF y) := ⟨inner_self_nonneg, inner_self_nonneg⟩
    positivity

Goal state after:
case neg
𝕜 : 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
⊢ 0 ≤ normSq x * (t * t) + 2 * ‖⟪x, y⟫‖ * t + normSq y
Module: Mathlib.Analysis.InnerProductSpace.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
r : ℝ
⊢ (starRingEnd 𝕜) ↑r * ⟪x, y⟫ = r • ⟪x, y⟫

Tactic:
conj_ofReal,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
r : ℝ
⊢ ↑r * ⟪x, y⟫ = r • ⟪x, y⟫
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₁ K₂ : Compacts G
h : Disjoint K₁.carrier K₂.carrier
h₂ : IsClosed[inst✝¹] K₂.carrier
U₁ U₂ : Set G
h1U₁ : IsOpen[inst✝¹] U₁
h1U₂ : IsOpen[inst✝¹] U₂
h2U₁ : K₁.carrier ⊆ U₁
h2U₂ : K₂.carrier ⊆ U₂
hU : Disjoint U₁ U₂
L₁ : Set G
h1L₁ : L₁ ∈ 𝓝 1
V₁ : Set G
h1V₁ : V₁ ⊆ L₁
h2V₁ : IsOpen[inst✝¹] V₁
h3V₁ : 1 ∈ V₁
h2L₁ : K₁.carrier * V₁ ⊆ U₁
L₂ : Set G
h1L₂ : L₂ ∈ 𝓝 1
V₂ : Set G
h1V₂ : V₂ ⊆ L₂
h2V₂ : IsOpen[inst✝¹] V₂
h3V₂ : 1 ∈ V₂
h2L₂ : K₂.carrier * V₂ ⊆ U₂
eval : (Compacts G → ℝ) → ℝ := fun f ↦ f K₁ + f K₂ - f (K₁ ⊔ K₂)
this : Continuous eval
V : Set G := V₁ ∩ V₂
⊢ 1 ∈ { carrier := V⁻¹, is_open' := ⋯ }.carrier

Tactic:
by
          simp only [V, mem_inv, inv_one, h3V₁, h3V₂, mem_inter_iff, true_and]

Goal state after:
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
⊢ ⟪x, x⟫ = 0 ↔ x = 0

Tactic:
by
  rw [inner_self_eq_norm_sq_to_K, sq_eq_zero_iff, ofReal_eq_zero, norm_eq_zero]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ ‖x + y‖ * ‖x + y‖ + ‖x - y‖ * ‖x - y‖ = 2 * (‖x‖ * ‖x‖ + ‖y‖ * ‖y‖)

Tactic:
simp only [← @inner_self_eq_norm_mul_norm 𝕜]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ re ⟪x + y, x + y⟫ + re ⟪x - y, x - y⟫ = 2 * (re ⟪x, x⟫ + re ⟪y, y⟫)
Module: Mathlib.Analysis.InnerProductSpace.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ ⟪x, y⟫ = (↑‖x + y‖ ^ 2 - ↑‖x - y‖ ^ 2 + (↑‖x - I • y‖ ^ 2 - ↑‖x + I • y‖ ^ 2) * I) / 4

Tactic:
rw [← re_add_im ⟪x, y⟫, re_inner_eq_norm_add_mul_self_sub_norm_sub_mul_self_div_four,
    im_inner_eq_norm_sub_i_smul_mul_self_sub_norm_add_i_smul_mul_self_div_four]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ ↑((‖x + y‖ * ‖x + y‖ - ‖x - y‖ * ‖x - y‖) / 4) + ↑((‖x - I • y‖ * ‖x - I • y‖ - ‖x + I • y‖ * ‖x + I • y‖) / 4) * I =
    (↑‖x + y‖ ^ 2 - ↑‖x - y‖ ^ 2 + (↑‖x - I • y‖ ^ 2 - ↑‖x + I • y‖ ^ 2) * I) / 4
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
⊢ ⟪∑ i₁ ∈ s₁, w₁ i₁ • v₁ i₁, ∑ i₂ ∈ s₂, w₂ i₂ • v₂ i₂⟫_ℝ =
    (-∑ i₁ ∈ s₁, ∑ i₂ ∈ s₂, w₁ i₁ * w₂ i₂ * (‖v₁ i₁ - v₂ i₂‖ * ‖v₁ i₁ - v₂ i₂‖)) / 2

Tactic:
simp_rw [sum_inner, inner_sum, real_inner_smul_left, real_inner_smul_right,
    real_inner_eq_norm_mul_self_add_norm_mul_self_sub_norm_sub_mul_self_div_two, ← div_sub_div_same,
    add_div, mul_sub_left_distrib, left_distrib, Finset.sum_sub_distrib,
    Finset.sum_add_distrib, ← Finset.mul_sum, ← Finset.sum_mul, h₁, h₂, zero_mul,
    mul_zero, Finset.sum_const_zero, zero_add, zero_sub, Finset.mul_sum, neg_div,
    Finset.sum_div, mul_div_assoc, mul_assoc]

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

Goal state before:
pp: F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
⊢ ⟪x, y⟫_ℝ / (‖x‖ * ‖y‖) = 1 ↔ x ≠ 0 ∧ ∃ r, 0 < r ∧ y = r • x

Tactic:
by
  constructor
  · intro h
    have hx₀ : x ≠ 0 := fun h₀ => by simp [h₀] at h
    have hy₀ : y ≠ 0 := fun h₀ => by simp [h₀] at h
    refine ⟨hx₀, ‖y‖ / ‖x‖, div_pos (norm_pos_iff.2 hy₀) (norm_pos_iff.2 hx₀), ?_⟩
    exact ((inner_eq_norm_mul_iff_div hx₀).1 (eq_of_div_eq_one h)).symm
  · rintro ⟨hx, ⟨r, ⟨hr, rfl⟩⟩⟩
    exact real_inner_div_norm_mul_norm_eq_one_of_ne_zero_of_pos_mul hx hr

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hv : Orthonormal 𝕜 v
l : ι → 𝕜
s : Finset ι
i : ι
hi : i ∈ s
⊢ ⟪v i, ∑ i ∈ s, l i • v i⟫ = l i

Tactic:
simp [inner_sum, inner_smul_right, orthonormal_iff_ite.mp hv, hi]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
η : Type u_5
s : η → Set E
hs : Directed (fun x1 x2 ↦ x1 ⊆ x2) s
h : ∀ (i : η), Orthonormal 𝕜 fun x ↦ ↑x
⊢ Orthonormal 𝕜 fun x ↦ ↑x

Tactic:
orthonormal_subtype_iff_ite

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
η : Type u_5
s : η → Set E
hs : Directed (fun x1 x2 ↦ x1 ⊆ x2) s
h : ∀ (i : η), Orthonormal 𝕜 fun x ↦ ↑x
⊢ ∀ v ∈ ⋃ i, s i, ∀ w ∈ ⋃ i, s i, ⟪v, w⟫ = if v = w then 1 else 0