mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.Haar.Basic

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K : PositiveCompacts G
V : Set G
hV : (interior V).Nonempty
⊢ ¬∃ x ∈ {t | ↑K ⊆ ⋃ g ∈ t, (fun h ↦ g * h) ⁻¹' V}, x.card = 0

pp: G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K : PositiveCompacts G
V : Set G
hV : (interior V).Nonempty
⊢ (Finset.card '' {t | ↑K ⊆ ⋃ g ∈ t, (fun h ↦ g * h) ⁻¹' V}).Nonempty

Tactic:
]

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K : PositiveCompacts G
V : Set G
hV : (interior V).Nonempty
⊢ ¬∃ x ∈ {t | ↑K ⊆ ⋃ g ∈ t, (fun h ↦ g * h) ⁻¹' V}, x.card = 0

G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K : PositiveCompacts G
V : Set G
hV : (interior V).Nonempty
⊢ (Finset.card '' {t | ↑K ⊆ ⋃ g ∈ t, (fun h ↦ g * h) ⁻¹' V}).Nonempty
Module: Mathlib.MeasureTheory.Measure.Haar.Basic

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K : PositiveCompacts G
V : Set G
hV : (interior V).Nonempty
t : Finset G
h1t : t ∈ {t | ↑K ⊆ ⋃ g ∈ t, (fun h ↦ g * h) ⁻¹' V}
h2t : t = ∅
⊢ False

Tactic:
]

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K : PositiveCompacts G
V : Set G
hV : (interior V).Nonempty
t : Finset G
h1t : t ∈ {t | ↑K ⊆ ⋃ g ∈ t, (fun h ↦ g * h) ⁻¹' V}
h2t : t = ∅
⊢ False
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
s t : Set X
μ : Measure X
inst✝ : CompleteSpace E
p : ℝ≥0∞
hs : MeasurableSet s
ht : MeasurableSet t
hμt : μ t ≠ ∞
e : E
⊢ ∫ (x : X) in s, t.indicator (fun x ↦ e) x ∂μ = ∫ (x : X) in s, t.indicator (fun x ↦ e) x ∂μ

Tactic:
]

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

Goal state before:
pp: R : Type u_1
inst✝⁷ : LinearOrder R
inst✝⁶ : TopologicalSpace R
f : StieltjesFunction R
inst✝⁵ : OrderTopology R
inst✝⁴ : CompactIccSpace R
inst✝³ : MeasurableSpace R
inst✝² : BorelSpace R
inst✝¹ : SecondCountableTopology R
inst✝ : DenselyOrdered R
a b : R
⊢ (let __OuterMeasure := f.outer;
      { toOuterMeasure := __OuterMeasure, m_iUnion := ⋯, trim_le := ⋯ })
      (Ioc a b) =
    ofReal (↑f b - ↑f a)

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
a b : R
⊢ (let __OuterMeasure := f.outer;
      { toOuterMeasure := __OuterMeasure, m_iUnion := ⋯, trim_le := ⋯ })
      (Ioc a b) =
    ofReal (↑f b - ↑f a)
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
hs : IsFundamentalDomain G s μ
f : α → ℝ≥0∞
hf : ∀ (γ : G) (x : α), f (γ • x) = f x
⊢ sInf {a | μ {x | a < f x} = 0} ≤ sInf {a | (μ.restrict s) {x | a < f x} = 0}

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
hs : IsFundamentalDomain G s μ
f : α → ℝ≥0∞
hf : ∀ (γ : G) (x : α), f (γ • x) = f x
⊢ sInf {a | μ {x | a < f x} = 0} ≤ sInf {a | (μ.restrict s) {x | a < f x} = 0}
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
s t : Set X
μ : Measure X
inst✝ : CompleteSpace E
p : ℝ≥0∞
hs : MeasurableSet s
ht : MeasurableSet t
hμt : μ t ≠ ∞
e : E
⊢ μ.real (t ∩ s) • e = μ.real (t ∩ s) • e

Tactic:
]

Goal state after:
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✝³ : MeasurableSpace R
inst✝² : BorelSpace R
inst✝¹ : SecondCountableTopology R
inst✝ : DenselyOrdered R
a : R
ha : IsBot a
this : leftLim (↑f) a = ↑f a
⊢ (let __OuterMeasure := f.outer;
      { toOuterMeasure := __OuterMeasure, m_iUnion := ⋯, trim_le := ⋯ })
      {a} ≤
    ⊥

Tactic:
]

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✝³ : MeasurableSpace R
inst✝² : BorelSpace R
inst✝¹ : SecondCountableTopology R
inst✝ : DenselyOrdered R
a : R
ha : IsBot a
this : leftLim (↑f) a = ↑f a
⊢ (let __OuterMeasure := f.outer;
      { toOuterMeasure := __OuterMeasure, m_iUnion := ⋯, trim_le := ⋯ })
      {a} ≤
    ⊥
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
t : Set X
μ : Measure X
inst✝ : CompleteSpace E
p : ℝ≥0∞
ht : MeasurableSet t
hμt : μ t ≠ ∞
e : E
⊢ ∫ (x : X), ↑↑(indicatorConstLp p ht hμt e) x ∂μ = ∫ (x : X), ↑↑(indicatorConstLp p ht hμt e) x ∂μ

Tactic:
]

Goal state after:
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✝³ : MeasurableSpace R
inst✝² : BorelSpace R
inst✝¹ : SecondCountableTopology R
inst✝ : DenselyOrdered R
a : R
ha : IsBot a
this : leftLim (↑f) a = ↑f a
⊢ f.length ({a} \ botSet) ≤ ⊥

Tactic:
]

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✝³ : MeasurableSpace R
inst✝² : BorelSpace R
inst✝¹ : SecondCountableTopology R
inst✝ : DenselyOrdered R
a : R
ha : IsBot a
this : leftLim (↑f) a = ↑f a
⊢ f.length ({a} \ botSet) ≤ ⊥
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
hs : IsFundamentalDomain G s μ
f : α → ℝ≥0∞
hf : ∀ (γ : G) (x : α), f (γ • x) = f x
a : ℝ≥0∞
ha : μ ({x | a < f x} ∩ s) = 0
⊢ a ∈ {a | μ {x | a < f x} = 0}

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
hs : IsFundamentalDomain G s μ
f : α → ℝ≥0∞
hf : ∀ (γ : G) (x : α), f (γ • x) = f x
a : ℝ≥0∞
ha : μ ({x | a < f x} ∩ s) = 0
⊢ a ∈ {a | μ {x | a < f x} = 0}
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
t : Set X
μ : Measure X
inst✝ : CompleteSpace E
p : ℝ≥0∞
ht : MeasurableSet t
hμt : μ t ≠ ∞
e : E
⊢ μ.real t • e = μ.real t • e

Tactic:
]

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

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

Tactic:
]

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K K' V : Set G
hK' : IsCompact K'
h : K ⊆ K'
hV : (interior V).Nonempty
s : Finset G
h1s : K' ⊆ ⋃ g ∈ s, (fun h ↦ g * h) ⁻¹' V
h2s : s.card = index K' V
⊢ ∃ x ∈ {t | K ⊆ ⋃ g ∈ t, (fun h ↦ g * h) ⁻¹' V}, x.card = index K' V
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
Y : Type u_5
inst✝ : MeasurableSpace Y
g : X → Y
f : Y → E
s : Set Y
hs : MeasurableSet s
hf : AEStronglyMeasurable f (Measure.map g μ)
hg : AEMeasurable g μ
⊢ ∫ (x : X) in g ⁻¹' s, f (g x) ∂μ = ∫ (x : X) in g ⁻¹' s, f (g x) ∂μ

pp: X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure X
Y : Type u_5
inst✝ : MeasurableSpace Y
g : X → Y
f : Y → E
s : Set Y
hs : MeasurableSet s
hf : AEStronglyMeasurable f (Measure.map g μ)
hg : AEMeasurable g μ
⊢ Measure.map g (μ.restrict (g ⁻¹' s)) ≤ Measure.map g μ

Tactic:
]

Goal state after:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure X
Y : Type u_5
inst✝ : MeasurableSpace Y
g : X → Y
f : Y → E
s : Set Y
hs : MeasurableSet s
hf : AEStronglyMeasurable f (Measure.map g μ)
hg : AEMeasurable g μ
⊢ Measure.map g (μ.restrict (g ⁻¹' s)) ≤ Measure.map g μ
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
Y : Type u_5
x✝ : MeasurableSpace Y
f : X → Y
hf : MeasurableEmbedding f
g : Y → E
s : Set Y
⊢ ∫ (x : X) in f ⁻¹' s, g (f x) ∂μ = ∫ (x : X) in f ⁻¹' s, g (f x) ∂μ

Tactic:
]

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
hs : IsFundamentalDomain G s μ
f : α → ℝ≥0∞
hf : ∀ (γ : G) (x : α), f (γ • x) = f x
a : ℝ≥0∞
ha : μ ({x | a < f x} ∩ s) = 0
γ : G
x : α
⊢ γ⁻¹ • x ∈ {x | a < f x} ↔ x ∈ {x | a < f x}

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
hs : IsFundamentalDomain G s μ
f : α → ℝ≥0∞
hf : ∀ (γ : G) (x : α), f (γ • x) = f x
a : ℝ≥0∞
ha : μ ({x | a < f x} ∩ s) = 0
γ : G
x : α
⊢ γ⁻¹ • x ∈ {x | a < f x} ↔ x ∈ {x | a < f x}
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
s : Finset G
h1s : K₁.carrier ⊆ ⋃ g ∈ s, (fun h ↦ g * h) ⁻¹' V
h2s : s.card = index K₁.carrier V
t : Finset G
h1t : K₂.carrier ⊆ ⋃ g ∈ t, (fun h ↦ g * h) ⁻¹' V
h2t : t.card = index K₂.carrier V
⊢ index (K₁.carrier ∪ K₂.carrier) V ≤ s.card + t.card

Tactic:
]

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
s : Finset G
h1s : K₁.carrier ⊆ ⋃ g ∈ s, (fun h ↦ g * h) ⁻¹' V
h2s : s.card = index K₁.carrier V
t : Finset G
h1t : K₂.carrier ⊆ ⋃ g ∈ t, (fun h ↦ g * h) ⁻¹' V
h2t : t.card = index K₂.carrier V
⊢ index (K₁.carrier ∪ K₂.carrier) V ≤ s.card + t.card
Module: Mathlib.MeasureTheory.Measure.Stieltjes

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

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
a : R
ha : ¬IsBot a
b : R
hb : b < a
u : ℕ → R
u_mono : StrictMono u
u_lim : Tendsto u atTop (𝓝 a)
u_lt_a : ∀ (n : ℕ), u n < a
A : {a} = ⋂ n, Ioc (u n) a
⊢ Tendsto (fun n ↦ f.measure (Ioc (u n) a)) atTop (𝓝 (f.measure (⋂ n, Ioc (u n) a)))
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 : Set X
μ : Measure X
C : ℝ
hs : (μ.restrict s) univ < ∞
hC : ∀ᵐ (x : X) ∂μ.restrict s, ‖f x‖ ≤ C
⊢ ‖∫ (x : X) in s, f x ∂μ‖ ≤ C * μ.real s

Tactic:
]

Goal state after:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
s : Set X
μ : Measure X
C : ℝ
hs : (μ.restrict s) univ < ∞
hC : ∀ᵐ (x : X) ∂μ.restrict s, ‖f x‖ ≤ C
⊢ ‖∫ (x : X) in s, f x ∂μ‖ ≤ C * μ.real s
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
s : Finset G
h1s : K₁.carrier ⊆ ⋃ g ∈ s, (fun h ↦ g * h) ⁻¹' V
h2s : s.card = index K₁.carrier V
t : Finset G
h1t : K₂.carrier ⊆ ⋃ g ∈ t, (fun h ↦ g * h) ⁻¹' V
h2t : t.card = index K₂.carrier V
⊢ K₁.carrier ∪ K₂.carrier ⊆ (⋃ x ∈ s, (fun h ↦ x * h) ⁻¹' V) ∪ ⋃ x ∈ t, (fun h ↦ x * h) ⁻¹' V

Tactic:
]

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
s : Finset G
h1s : K₁.carrier ⊆ ⋃ g ∈ s, (fun h ↦ g * h) ⁻¹' V
h2s : s.card = index K₁.carrier V
t : Finset G
h1t : K₂.carrier ⊆ ⋃ g ∈ t, (fun h ↦ g * h) ⁻¹' V
h2t : t.card = index K₂.carrier V
⊢ K₁.carrier ∪ K₂.carrier ⊆ (⋃ x ∈ s, (fun h ↦ x * h) ⁻¹' V) ∪ ⋃ x ∈ t, (fun h ↦ x * h) ⁻¹' V
Module: Mathlib.MeasureTheory.Measure.Haar.Basic

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₁ K₂ : 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
⊢ index K₁.carrier V + index K₂.carrier V ≤ s.card

Tactic:
]

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
⊢ index K₁.carrier V + index K₂.carrier V ≤ s.card
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 : Set X
μ : Measure X
C : ℝ
hs : μ s < ∞
hC : ∀ᵐ (x : X) ∂μ, x ∈ s → ‖f x‖ ≤ C
hfm : AEStronglyMeasurable f (μ.restrict s)
a✝ : X
h1 : a✝ ∈ s → ‖f a✝‖ ≤ C
h2 : a✝ ∈ s → f a✝ = AEStronglyMeasurable.mk f hfm a✝
h3 : a✝ ∈ s
⊢ ‖f a✝‖ ≤ C

Tactic:
]

Goal state after:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
s : Set X
μ : Measure X
C : ℝ
hs : μ s < ∞
hC : ∀ᵐ (x : X) ∂μ, x ∈ s → ‖f x‖ ≤ C
hfm : AEStronglyMeasurable f (μ.restrict s)
a✝ : X
h1 : a✝ ∈ s → ‖f a✝‖ ≤ C
h2 : a✝ ∈ s → f a✝ = AEStronglyMeasurable.mk f hfm a✝
h3 : a✝ ∈ s
⊢ ‖f a✝‖ ≤ C
Module: Mathlib.MeasureTheory.Group.FundamentalDomain

Goal state before:
pp: G : Type u_1
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
a b : G
hab : a ≠ b
x : α
hx : x ∈ s ∧ ∀ (g : G), g ≠ 1 → x ∉ g • s
y : α
hy : y ∈ s ∧ ∀ (g : G), g ≠ 1 → y ∉ g • s
hxy : (fun x ↦ b • x) y = (fun x ↦ a • x) x
⊢ False

Tactic:
]

Goal state after:
G : Type u_1
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
a b : G
hab : a ≠ b
x : α
hx : x ∈ s ∧ ∀ (g : G), g ≠ 1 → x ∉ g • s
y : α
hy : y ∈ s ∧ ∀ (g : G), g ≠ 1 → y ∉ g • s
hxy : (fun x ↦ b • x) y = (fun x ↦ a • x) x
⊢ False
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
⊢ K ⊆ ⋃ g ∈ {g ∈ s | ((fun x ↦ g * x) ⁻¹' V ∩ K).Nonempty}, (fun h ↦ g * h) ⁻¹' V

Tactic:
]

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

Goal state before:
pp: case refine_1
G : Type u_1
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
a b : G
hab : a ≠ b
x : α
hx : x ∈ s ∧ ∀ (g : G), g ≠ 1 → x ∉ g • s
y : α
hy : y ∈ s ∧ ∀ (g : G), g ≠ 1 → y ∉ g • s
hxy : (fun x ↦ b • x) y = (fun x ↦ a • x) x
⊢ ¬a = b

Tactic:
]

Goal state after:
case refine_1
G : Type u_1
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
a b : G
hab : a ≠ b
x : α
hx : x ∈ s ∧ ∀ (g : G), g ≠ 1 → x ∉ g • s
y : α
hy : y ∈ s ∧ ∀ (g : G), g ≠ 1 → y ∉ g • s
hxy : (fun x ↦ b • x) y = (fun x ↦ a • x) x
⊢ ¬a = b
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 : Set X
μ : Measure X
C : ℝ
hs : μ s < ∞
hC : ∀ᵐ (x : X) ∂μ, x ∈ s → ‖f x‖ ≤ C
hfm : AEStronglyMeasurable f (μ.restrict s)
A : ∀ᵐ (x : X) ∂μ, x ∈ s → ‖AEStronglyMeasurable.mk f hfm x‖ ≤ C
B : MeasurableSet {x | ‖AEStronglyMeasurable.mk f hfm x‖ ≤ C}
a✝¹ : X
h1 : f a✝¹ = AEStronglyMeasurable.mk f hfm a✝¹
a✝ : ‖AEStronglyMeasurable.mk f hfm a✝¹‖ ≤ C
⊢ ‖AEStronglyMeasurable.mk f hfm a✝¹‖ ≤ C

Tactic:
]

Goal state after:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
s : Set X
μ : Measure X
C : ℝ
hs : μ s < ∞
hC : ∀ᵐ (x : X) ∂μ, x ∈ s → ‖f x‖ ≤ C
hfm : AEStronglyMeasurable f (μ.restrict s)
A : ∀ᵐ (x : X) ∂μ, x ∈ s → ‖AEStronglyMeasurable.mk f hfm x‖ ≤ C
B : MeasurableSet {x | ‖AEStronglyMeasurable.mk f hfm x‖ ≤ C}
a✝¹ : X
h1 : f a✝¹ = AEStronglyMeasurable.mk f hfm a✝¹
a✝ : ‖AEStronglyMeasurable.mk f hfm a✝¹‖ ≤ C
⊢ ‖AEStronglyMeasurable.mk f hfm a✝¹‖ ≤ C
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
s : Set X
μ : Measure X
C : ℝ
hs : μ s < ∞
hC : ∀ᵐ (x : X) ∂μ, x ∈ s → ‖f x‖ ≤ C
hfm : ¬AEStronglyMeasurable f (μ.restrict s)
⊢ ‖0‖ ≤ C * μ.real s

Tactic:
]

Goal state after:
case neg
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
s : Set X
μ : Measure X
C : ℝ
hs : μ s < ∞
hC : ∀ᵐ (x : X) ∂μ, x ∈ s → ‖f x‖ ≤ C
hfm : ¬AEStronglyMeasurable f (μ.restrict s)
⊢ ‖0‖ ≤ C * μ.real s
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
this : ∀ K ⊆ ⋃ g ∈ s, (fun x ↦ g * x) ⁻¹' V, index K V ≤ {g ∈ s | ((fun x ↦ g * x) ⁻¹' V ∩ K).Nonempty}.card
⊢ {x ∈ s | ((fun x_1 ↦ x * x_1) ⁻¹' V ∩ K₁.carrier).Nonempty ∨ ((fun x_1 ↦ x * x_1) ⁻¹' V ∩ K₂.carrier).Nonempty}.card ≤
    s.card

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
this : ∀ K ⊆ ⋃ g ∈ s, (fun x ↦ g * x) ⁻¹' V, index K V ≤ {g ∈ s | ((fun x ↦ g * x) ⁻¹' V ∩ K).Nonempty}.card
⊢ Disjoint ({g ∈ s | ((fun x ↦ g * x) ⁻¹' V ∩ K₁.carrier).Nonempty})
    ({g ∈ s | ((fun x ↦ g * x) ⁻¹' V ∩ K₂.carrier).Nonempty})

Tactic:
]

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
this : ∀ K ⊆ ⋃ g ∈ s, (fun x ↦ g * x) ⁻¹' V, index K V ≤ {g ∈ s | ((fun x ↦ g * x) ⁻¹' V ∩ K).Nonempty}.card
⊢ {x ∈ s | ((fun x_1 ↦ x * x_1) ⁻¹' V ∩ K₁.carrier).Nonempty ∨ ((fun x_1 ↦ x * x_1) ⁻¹' V ∩ K₂.carrier).Nonempty}.card ≤
    s.card

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
this : ∀ K ⊆ ⋃ g ∈ s, (fun x ↦ g * x) ⁻¹' V, index K V ≤ {g ∈ s | ((fun x ↦ g * x) ⁻¹' V ∩ K).Nonempty}.card
⊢ Disjoint ({g ∈ s | ((fun x ↦ g * x) ⁻¹' V ∩ K₁.carrier).Nonempty})
    ({g ∈ s | ((fun x ↦ g * x) ⁻¹' V ∩ K₂.carrier).Nonempty})
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 α
s : Set α
U : Set (Quotient α_mod_G)
meas_U : MeasurableSet U
⊢ μ (Quotient.mk α_mod_G ⁻¹' U ∩ s) = μ (Quotient.mk α_mod_G ⁻¹' U ∩ s)

Tactic:
]

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
μ : 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), f x ∂μ

Tactic:
]

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 α
μ : Measure α
inst✝² : Countable G
s t : Set α
inst✝¹ : SMulInvariantMeasure G α μ
inst✝ : MeasurableConstSMul G α
fund_dom_s : IsFundamentalDomain G s μ
fund_dom_t : IsFundamentalDomain G t μ
U : Set (Quotient α_mod_G)
meas_U : MeasurableSet U
⊢ μ (Quotient.mk α_mod_G ⁻¹' U ∩ s) = μ (Quotient.mk α_mod_G ⁻¹' U ∩ t)

Tactic:
]

Goal state after:
G : Type u_1
α : Type u_3
inst✝⁵ : Group G
inst✝⁴ : MulAction G α
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : Countable G
s t : Set α
inst✝¹ : SMulInvariantMeasure G α μ
inst✝ : MeasurableConstSMul G α
fund_dom_s : IsFundamentalDomain G s μ
fund_dom_t : IsFundamentalDomain G t μ
U : Set (Quotient α_mod_G)
meas_U : MeasurableSet U
⊢ μ (Quotient.mk α_mod_G ⁻¹' U ∩ s) = μ (Quotient.mk α_mod_G ⁻¹' U ∩ t)
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 μ
h0 : ∫ (x : X), f x ∂μ - ∫ (x : X) in s, f x ∂μ = ∫ (x : X) in sᶜ, f x ∂μ
h1 : ∫ (x : X) in sᶜ, ‖f x‖ ∂μ ≤ ∫ (x : X) in sᶜ, C ∂μ
⊢ μ.real sᶜ * C = μ.real sᶜ * C

Tactic:
]

Goal state after: