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 : ℝ
β : 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
⊢ StronglyMeasurable fun x ↦ SimpleFunc.setToSimpleFunc T (s' n x)

Tactic:
[

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 := 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
⊢ StronglyMeasurable fun x ↦ SimpleFunc.setToSimpleFunc T (s' n 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 : ℝ
β : 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)
hf' : ∀ (n : ℕ), StronglyMeasurable (f' n)
x : β
hfx : Integrable (f x) μ
n : ℕ
y : α
⊢ ‖(s' n x) y‖ ≤ ((fun a ↦ ‖f x a‖) + fun a ↦ ‖f x a‖) y

Tactic:
[

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 := 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)
hf' : ∀ (n : ℕ), StronglyMeasurable (f' n)
x : β
hfx : Integrable (f x) μ
n : ℕ
y : α
⊢ ‖(s' n x) y‖ ≤ ((fun a ↦ ‖f x a‖) + fun a ↦ ‖f x a‖) y
Module: Mathlib.MeasureTheory.Measure.Content

Goal state before:
pp: G : Type w
inst✝ : TopologicalSpace G
μ : Content G
K : Compacts G
hK : ↑K ⊆ ↑⊥
this : K = ⊥
⊢ μ K ≤ μ ⊥

Tactic:
this

Goal state after:
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
K : Compacts G
hK : ↑K ⊆ ↑⊥
this : K = ⊥
⊢ μ ⊥ ≤ μ ⊥
Module: Mathlib.MeasureTheory.Group.FundamentalDomain

Goal state before:
pp: G : Type u_1
α : Type u_3
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MeasurableSpace α
s : Set α
μ : Measure α
inst✝¹ : Countable G
inst✝ : SMulInvariantMeasure G α μ
hμ : μ ≠ 0
h : IsFundamentalDomain G s μ
hc : μ s = 0
⊢ ∑' (i : G), μ (i • s) ≤ 0

Tactic:
[

Goal state after:
G : Type u_1
α : Type u_3
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MeasurableSpace α
s : Set α
μ : Measure α
inst✝¹ : Countable G
inst✝ : SMulInvariantMeasure G α μ
hμ : μ ≠ 0
h : IsFundamentalDomain G s μ
hc : μ s = 0
⊢ ∑' (i : G), μ (i • s) ≤ 0
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' \ U) ≤ μ.outerMeasure ↑U'

Tactic:
this

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' + μ.outerMeasure (↑U' \ ↑L') ≤ μ.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
f : X → E
s t : Set X
μ : Measure X
hts : s ⊆ t
h't : ∀ᵐ (x : X) ∂μ, x ∈ t \ s → f x = 0
haux : StronglyMeasurable f
h'aux : IntegrableOn f t μ
k : Set X := f ⁻¹' {0}
hk : MeasurableSet k
⊢ ∫ (x : X) in s ∩ k, f x ∂μ + ∫ (x : X) in s \ k, f x ∂μ = ∫ (x : X) in s, f x ∂μ

Tactic:
by rw [integral_inter_add_sdiff hk (h'aux.mono hts le_rfl)]

Goal state after:
Module: Mathlib.MeasureTheory.Group.FundamentalDomain

Goal state before:
pp: G : Type u_1
α : Type u_3
inst✝⁶ : Group G
inst✝⁵ : MulAction G α
inst✝⁴ : MeasurableSpace α
s : Set α
μ : Measure α
inst✝³ : MeasurableConstSMul G α
inst✝² : SMulInvariantMeasure G α μ
inst✝¹ : Countable G
inst✝ : Finite G
h : IsFundamentalDomain G s μ
t : Set α
this : Fintype G
ht : ∀ (g : G), g • t ∩ s =ᵐ[μ] t ∩ s
⊢ ∑' (g : G), μ (g • t ∩ s) = Nat.card G • μ (t ∩ s)

Tactic:
[

Goal state after:
G : Type u_1
α : Type u_3
inst✝⁶ : Group G
inst✝⁵ : MulAction G α
inst✝⁴ : MeasurableSpace α
s : Set α
μ : Measure α
inst✝³ : MeasurableConstSMul G α
inst✝² : SMulInvariantMeasure G α μ
inst✝¹ : Countable G
inst✝ : Finite G
h : IsFundamentalDomain G s μ
t : Set α
this : Fintype G
ht : ∀ (g : G), g • t ∩ s =ᵐ[μ] t ∩ s
⊢ ∑' (g : G), μ (g • t ∩ s) = Nat.card G • μ (t ∩ s)
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 | f x ≤ 0} = {x | f x < 0} ∪ {x | f x = 0}

Tactic:
[

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 μ
⊢ {x | f x ≤ 0} = {x | f x < 0} ∪ {x | f x = 0}
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
⊢ 𝓝[<] a = ⊥

Tactic:
simp [nhdsLT_eq_bot_iff, ha]

Goal state after:
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
⊢ fundamentalFrontier G (g • s) = g • fundamentalFrontier G s

Tactic:
[

Goal state after:
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
⊢ fundamentalFrontier G (g • s) = g • fundamentalFrontier G s
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:
[

Goal state after:
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
Module: Mathlib.MeasureTheory.Group.FundamentalDomain

Goal state before:
pp: G : Type u_1
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
⊢ Pairwise (Disjoint on fun g ↦ g • fundamentalInterior G s)

Tactic:
refine fun a b hab => disjoint_left.2 ?_

Goal state after:
G : Type u_1
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
a b : G
hab : a ≠ b
⊢ ∀ ⦃a_1 : α⦄, a_1 ∈ (fun g ↦ g • fundamentalInterior G s) a → a_1 ∉ (fun g ↦ g • fundamentalInterior G s) b
Module: Mathlib.MeasureTheory.Group.FundamentalDomain

Goal state before:
pp: G : Type u_1
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
⊢ Pairwise (Disjoint on fun g ↦ g • fundamentalInterior G s)

Tactic:
by
  refine fun a b hab => disjoint_left.2 ?_
  rintro _ ⟨x, hx, rfl⟩ ⟨y, hy, hxy⟩
  rw [mem_fundamentalInterior] at hx hy
  refine hx.2 (a⁻¹ * b) ?_ ?_
  · rwa [Ne, inv_mul_eq_iff_eq_mul, mul_one, eq_comm]
  · simpa [mul_smul, ← hxy, mem_inv_smul_set_iff] using hy.1

Goal state after:
Module: Mathlib.MeasureTheory.Group.FundamentalDomain

Goal state before:
pp: G : Type u_1
α : Type u_3
inst✝⁵ : Countable G
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MeasurableSpace α
μ : Measure α
s : Set α
hs : IsFundamentalDomain G s μ
inst✝¹ : MeasurableConstSMul G α
inst✝ : SMulInvariantMeasure G α μ
⊢ ∀ᵐ (x : α) ∂μ, ∃ g, g • x ∈ fundamentalInterior G s

Tactic:
[

Goal state after:
G : Type u_1
α : Type u_3
inst✝⁵ : Countable G
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MeasurableSpace α
μ : Measure α
s : Set α
hs : IsFundamentalDomain G s μ
inst✝¹ : MeasurableConstSMul G α
inst✝ : SMulInvariantMeasure G α μ
⊢ ∀ᵐ (x : α) ∂μ, ∃ g, g • x ∈ fundamentalInterior G s
Module: Mathlib.MeasureTheory.Group.FundamentalDomain

Goal state before:
pp: G : Type u_1
α : Type u_3
inst✝⁵ : Countable G
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MeasurableSpace α
μ : Measure α
s : Set α
hs : IsFundamentalDomain G s μ
inst✝¹ : MeasurableConstSMul G α
inst✝ : SMulInvariantMeasure G α μ
⊢ (⋃ g, g⁻¹ • s) \ ⋃ g, g⁻¹ • fundamentalFrontier G s ⊆ ⋃ g, g⁻¹ • fundamentalInterior G s

Tactic:
[

Goal state after:
G : Type u_1
α : Type u_3
inst✝⁵ : Countable G
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MeasurableSpace α
μ : Measure α
s : Set α
hs : IsFundamentalDomain G s μ
inst✝¹ : MeasurableConstSMul G α
inst✝ : SMulInvariantMeasure G α μ
⊢ (⋃ g, g⁻¹ • s) \ ⋃ g, g⁻¹ • fundamentalFrontier G s ⊆ ⋃ g, g⁻¹ • fundamentalInterior G s
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
inst✝ : IsFiniteMeasure μ
C : ℝ
hf : ∀ᵐ (x : X) ∂μ, ‖f x‖ ≤ C
s : Set X
hs : MeasurableSet s
hf1 : Integrable f μ
⊢ ‖∫ (x : X), f x ∂μ - ∫ (x : X) in s, f x ∂μ‖ ≤ μ.real sᶜ * C

Tactic:
by
  have h0 : ∫ (x : X), f x ∂μ - ∫ x in s, f x ∂μ = ∫ x in sᶜ, f x ∂μ := by
    rw [sub_eq_iff_eq_add, add_comm, integral_add_compl hs hf1]
  have h1 : ∫ x in sᶜ, ‖f x‖ ∂μ ≤ ∫ _ in sᶜ, C ∂μ :=
    integral_mono_ae hf1.norm.restrict (integrable_const C) (ae_restrict_of_ae hf)
  have h2 : ∫ _ in sᶜ, C ∂μ = μ.real sᶜ * C := by
    rw [setIntegral_const C, smul_eq_mul]
  rw [h0, ← h2]
  exact le_trans (norm_integral_le_integral_norm f) h1

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

Goal state before:
pp: X : Type u_1
mX : MeasurableSpace X
s : Set X
μ : Measure X
f : X → ℝ
hf : 0 ≤ᵐ[μ.restrict s] f
hfi : IntegrableOn f s μ
⊢ 0 < ∫ (x : X) in s, f x ∂μ ↔ 0 < μ (support f ∩ s)

Tactic:
by
  rw [integral_pos_iff_support_of_nonneg_ae hf hfi, Measure.restrict_apply₀]
  rw [support_eq_preimage]
  exact hfi.aestronglyMeasurable.aemeasurable.nullMeasurable (measurableSet_singleton 0).compl

Goal state after:
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
this : IntegrableOn (fun x ↦ R) {x | R < f x} μ
⊢ 0 < μ ((support fun a ↦ f a - R) ∩ {x | R < f x})

Tactic:
rw [← pos_iff_ne_zero] at hμ

Goal state after:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
R : ℝ
f : X → ℝ
hR : 0 ≤ R
hfint : IntegrableOn f {x | R < f x} μ
hμ : 0 < μ {x | R < f x}
this : IntegrableOn (fun x ↦ R) {x | R < f x} μ
⊢ 0 < μ ((support fun a ↦ f a - R) ∩ {x | R < f x})
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 α
i : SigmaFinite ν
μ : Measure (Quotient α_mod_G)
inst✝ : QuotientMeasureEqMeasurePreimage ν μ
A : ℕ → Set α
hA_meas : ∀ (i : ℕ), MeasurableSet (A i)
hA : ∀ (i : ℕ), ν (A i) < ∞
hA' : ⋃ i, A i = univ
n : ℕ
s : Set α
fund_dom_s : IsFundamentalDomain G s ν
this : Quotient.mk α_mod_G ⁻¹' Quotient.mk α_mod_G '' A n = ⋃ g, (fun x ↦ g • x) '' A n
⊢ MeasurableSet (Quotient.mk α_mod_G ⁻¹' Quotient.mk α_mod_G '' A n)

Tactic:
this

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 α
i : SigmaFinite ν
μ : Measure (Quotient α_mod_G)
inst✝ : QuotientMeasureEqMeasurePreimage ν μ
A : ℕ → Set α
hA_meas : ∀ (i : ℕ), MeasurableSet (A i)
hA : ∀ (i : ℕ), ν (A i) < ∞
hA' : ⋃ i, A i = univ
n : ℕ
s : Set α
fund_dom_s : IsFundamentalDomain G s ν
this : Quotient.mk α_mod_G ⁻¹' Quotient.mk α_mod_G '' A n = ⋃ g, (fun x ↦ g • x) '' A n
⊢ MeasurableSet (⋃ g, (fun x ↦ g • x) '' A n)
Module: Mathlib.MeasureTheory.Measure.Stieltjes

Goal state before:
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
l : ℝ
hf : Tendsto (↑f) atBot (𝓝 l)
x : R
this✝ : Nonempty R
val✝ : NoBotOrder R
this : NoMinOrder R
⊢ Tendsto (fun x_1 ↦ f.measure (Ioc x_1 x)) atBot (𝓝 (ofReal (↑f x - l)))

Tactic:
[

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
l : ℝ
hf : Tendsto (↑f) atBot (𝓝 l)
x : R
this✝ : Nonempty R
val✝ : NoBotOrder R
this : NoMinOrder R
⊢ Tendsto (fun x_1 ↦ f.measure (Ioc x_1 x)) atBot (𝓝 (ofReal (↑f x - l)))
Module: Mathlib.MeasureTheory.Measure.Stieltjes

Goal state before:
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
l : ℝ
hf : Tendsto (↑f) atTop (𝓝 l)
x : R
this✝ : Nonempty R
val✝ : NoTopOrder R
this : NoMaxOrder R
⊢ Tendsto (fun x_1 ↦ f.measure (Ico x x_1)) atTop (𝓝 (ofReal (l - leftLim (↑f) x)))

Tactic:
[

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
l : ℝ
hf : Tendsto (↑f) atTop (𝓝 l)
x : R
this✝ : Nonempty R
val✝ : NoTopOrder R
this : NoMaxOrder R
⊢ Tendsto (fun x_1 ↦ f.measure (Ico x x_1)) atTop (𝓝 (ofReal (l - leftLim (↑f) x)))
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
inst✝ : Nonempty R
l u : ℝ
hfl : Tendsto (↑f) atBot (𝓝 l)
hfu : Tendsto (↑f) atTop (𝓝 u)
⊢ Tendsto (fun x ↦ f.measure (Iic x)) atTop (𝓝 (ofReal (u - l)))

Tactic:
[

Goal state after:
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
inst✝ : Nonempty R
l u : ℝ
hfl : Tendsto (↑f) atBot (𝓝 l)
hfu : Tendsto (↑f) atTop (𝓝 u)
⊢ Tendsto (fun x ↦ f.measure (Iic x)) atTop (𝓝 (ofReal (u - l)))
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 z : F
⊢ ⟪x, y + z⟫ = ⟪x, y⟫ + ⟪x, z⟫

Tactic:
rw [← inner_conj_symm, inner_add_left, map_add]; simp only [inner_conj_symm]

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
r : 𝕜
⊢ (starRingEnd 𝕜) ((starRingEnd 𝕜) r * ⟪y, x⟫) = r * ⟪x, y⟫

Tactic:
simp only [conj_conj, inner_conj_symm, map_mul]

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

Goal state before:
pp: X : Type u_1
E : Type u_3
mX : MeasurableSpace X
ι : Type u_5
inst✝¹ : Countable ι
μ : Measure X
inst✝ : NormedAddCommGroup E
f : X → E
s : ι → Set X
hi : ∀ (i : ι), IntegrableOn f (s i) μ
h : Summable fun i ↦ ∫ (x : X) in s i, ‖f x‖ ∂μ
B : ∀ (i : ι), ∫⁻ (a : X) in s i, ↑‖f a‖₊ ∂μ = ENNReal.ofReal (∫ (a : X) in s i, ↑‖f a‖₊ ∂μ)
⊢ ∑' (i : ι), ∫⁻ (a : X) in s i, ‖f a‖ₑ ∂μ < ∞

Tactic:
[

Goal state after:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
ι : Type u_5
inst✝¹ : Countable ι
μ : Measure X
inst✝ : NormedAddCommGroup E
f : X → E
s : ι → Set X
hi : ∀ (i : ι), IntegrableOn f (s i) μ
h : Summable fun i ↦ ∫ (x : X) in s i, ‖f x‖ ∂μ
B : ∀ (i : ι), ∫⁻ (a : X) in s i, ↑‖f a‖₊ ∂μ = ENNReal.ofReal (∫ (a : X) in s i, ↑‖f a‖₊ ∂μ)
⊢ ∑' (i : ι), ∫⁻ (a : X) in s i, ‖f a‖ₑ ∂μ < ∞
Module: Mathlib.MeasureTheory.Integral.Bochner.Set

Goal state before:
pp: X : Type u_1
E : Type u_3
mX : MeasurableSpace X
ι : Type u_5
inst✝¹ : Countable ι
μ : Measure X
inst✝ : NormedAddCommGroup E
f : X → E
s : ι → Set X
hi : ∀ (i : ι), IntegrableOn f (s i) μ
h : Summable fun i ↦ ∫ (x : X) in s i, ‖f x‖ ∂μ
B : ∀ (i : ι), ∫⁻ (a : X) in s i, ↑‖f a‖₊ ∂μ = ENNReal.ofReal (∫ (a : X) in s i, ↑‖f a‖₊ ∂μ)
S' : Summable fun i ↦ NNReal.mk (∫ (x : X) in s i, ↑‖f x‖₊ ∂μ) ⋯
S'' :
  ∑' (a : ι), ↑(NNReal.mk (∫ (x : X) in s a, ↑‖f x‖₊ ∂μ) ⋯) = ↑(∑' (b : ι), NNReal.mk (∫ (x : X) in s b, ↑‖f x‖₊ ∂μ) ⋯)
⊢ ∑' (b : ι), ENNReal.ofReal (∫ (a : X) in s b, ↑‖f a‖₊ ∂μ) < ∞

Tactic:
[

Goal state after:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
ι : Type u_5
inst✝¹ : Countable ι
μ : Measure X
inst✝ : NormedAddCommGroup E
f : X → E
s : ι → Set X
hi : ∀ (i : ι), IntegrableOn f (s i) μ
h : Summable fun i ↦ ∫ (x : X) in s i, ‖f x‖ ∂μ
B : ∀ (i : ι), ∫⁻ (a : X) in s i, ↑‖f a‖₊ ∂μ = ENNReal.ofReal (∫ (a : X) in s i, ↑‖f a‖₊ ∂μ)
S' : Summable fun i ↦ NNReal.mk (∫ (x : X) in s i, ↑‖f x‖₊ ∂μ) ⋯
S'' :
  ∑' (a : ι), ↑(NNReal.mk (∫ (x : X) in s a, ↑‖f x‖₊ ∂μ) ⋯) = ↑(∑' (b : ι), NNReal.mk (∫ (x : X) in s b, ↑‖f x‖₊ ∂μ) ⋯)
⊢ ∑' (b : ι), ENNReal.ofReal (∫ (a : X) in s b, ↑‖f 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
inst✝⁴ : CompactIccSpace R
inst✝³ : MeasurableSpace R
inst✝² : BorelSpace R
inst✝¹ : SecondCountableTopology R
inst✝ : DenselyOrdered R
g : StieltjesFunction R
y : R
hfg : f.measure = g.measure
hy : ↑f y = ↑g y
x : R
⊢ ↑f x = ↑g x

Tactic:
cases le_total x y with
  | inl hxy =>
    have hf := measure_Ioc f x y
    rw [hfg, measure_Ioc g x y, ENNReal.ofReal_eq_ofReal_iff, eq_comm, hy] at hf
    · simpa using hf
    · rw [sub_nonneg]
      exact g.mono hxy
    · rw [sub_nonneg]
      exact f.mono hxy
  | inr hxy =>
    have hf := measure_Ioc f y x
    rw [hfg, measure_Ioc g y x, ENNReal.ofReal_eq_ofReal_iff, eq_comm, hy] at hf
    · simpa using hf
    · rw [sub_nonneg]
      exact g.mono hxy
    · rw [sub_nonneg]
      exact f.mono hxy

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

Goal state before:
pp: case e'_4.e'_6
𝕜 : 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
⊢ ‖⟪x, y⟫‖ ^ 2 * t = t * re ⟪⟪x, y⟫ • x, y⟫

Tactic:
rw [inner_smul_left, mul_comm _ ⟪x, y⟫_𝕜, mul_conj, ← ofReal_pow, ofReal_re]

Goal state after:
case e'_4.e'_6
𝕜 : 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
⊢ ‖⟪x, y⟫‖ ^ 2 * t = t * ‖⟪x, y⟫‖ ^ 2
Module: Mathlib.Analysis.InnerProductSpace.Defs

Goal state before:
pp: 𝕜 : Type u_1
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 F
cd : Core 𝕜 F
tF : TopologicalSpace F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousConstSMul 𝕜 F
h : ContinuousAt (fun v ↦ ⟪v, v⟫) 0
h' : IsVonNBounded 𝕜 {v | re ⟪v, v⟫ < 1}
p : Seminorm 𝕜 F := normSeminorm 𝕜 F
this : p.ball 0 1 = {v | re ⟪v, v⟫ < 1}
⊢ p.ball 0 1 ∈ 𝓝 0 ∧ IsVonNBounded 𝕜 (p.ball 0 1)

Tactic:
this

Goal state after:
𝕜 : Type u_1
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 F
cd : Core 𝕜 F
tF : TopologicalSpace F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousConstSMul 𝕜 F
h : ContinuousAt (fun v ↦ ⟪v, v⟫) 0
h' : IsVonNBounded 𝕜 {v | re ⟪v, v⟫ < 1}
p : Seminorm 𝕜 F := normSeminorm 𝕜 F
this : p.ball 0 1 = {v | re ⟪v, v⟫ < 1}
⊢ {v | re ⟪v, v⟫ < 1} ∈ 𝓝 0 ∧ IsVonNBounded 𝕜 {v | re ⟪v, v⟫ < 1}
Module: Mathlib.Analysis.InnerProductSpace.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v w : E
⊢ ⟪v, w⟫ = ↑‖v‖ ^ 2 ↔ ⟪v, v - w⟫ = 0

Tactic:
inner_sub_right,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v w : E
⊢ ⟪v, w⟫ = ↑‖v‖ ^ 2 ↔ ⟪v, v⟫ - ⟪v, w⟫ = 0
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 y : E
h : ∀ (v : E), ⟪v, x⟫ = ⟪v, y⟫
⊢ ⟪x - y, x - y⟫ = 0

Tactic:
inner_sub_right,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
h : ∀ (v : E), ⟪v, x⟫ = ⟪v, y⟫
⊢ ⟪x - y, x⟫ - ⟪x - y, y⟫ = 0