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

Goal state before:
pp: case h
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 ∈ s | ((fun x ↦ g * x) ⁻¹' V ∩ K).Nonempty}), g ∈ (fun h ↦ g₀ * h) ⁻¹' V

Tactic:
;

Goal state after:
case h
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 ∈ s | ((fun x ↦ g * x) ⁻¹' V ∩ K).Nonempty}), g ∈ (fun h ↦ g₀ * h) ⁻¹' V
Module: Mathlib.MeasureTheory.Measure.Haar.Basic

Goal state before:
pp: case h.h
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 ∈ (fun h ↦ g₀ * h) ⁻¹' V

pp: case h.w
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 ∈ s | ((fun x ↦ g * x) ⁻¹' V ∩ K).Nonempty}

Tactic:
;

Goal state after:
case h.h
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 ∈ (fun h ↦ g₀ * h) ⁻¹' V

case h.w
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 ∈ s | ((fun x ↦ g * x) ⁻¹' V ∩ K).Nonempty}
Module: Mathlib.MeasureTheory.Measure.Haar.Basic

Goal state before:
pp: case h.w
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
⊢ ((fun x ↦ g₀ * x) ⁻¹' V ∩ K).Nonempty

Tactic:
;

Goal state after:
case h.w
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
⊢ ((fun x ↦ g₀ * x) ⁻¹' V ∩ K).Nonempty
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⁻¹ • 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⁻¹ • 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 : Set G
hK : IsCompact K
V : Set G
hV : (interior V).Nonempty
g : G
s : Finset G
h1s : K ⊆ ⋃ g ∈ s, (fun h ↦ g * h) ⁻¹' V
h2s : s.card = index K V
⊢ index ((fun h ↦ g * h) '' K) V ≤ index K V

Tactic:
;

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K : Set G
hK : IsCompact K
V : Set G
hV : (interior V).Nonempty
g : G
s : Finset G
h1s : K ⊆ ⋃ g ∈ s, (fun h ↦ g * h) ⁻¹' V
h2s : s.card = index K V
⊢ index ((fun h ↦ g * h) '' K) V ≤ index K 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 : Set G
hK : IsCompact K
V : Set G
hV : (interior V).Nonempty
g : G
s : Finset G
h1s : K ⊆ ⋃ g ∈ s, (fun h ↦ g * h) ⁻¹' V
h2s : s.card = index K V
⊢ s.card ∈ Finset.card '' {t | (fun h ↦ g * h) '' K ⊆ ⋃ g ∈ t, (fun h ↦ g * h) ⁻¹' V}

Tactic:
;

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K : Set G
hK : IsCompact K
V : Set G
hV : (interior V).Nonempty
g : G
s : Finset G
h1s : K ⊆ ⋃ g ∈ s, (fun h ↦ g * h) ⁻¹' V
h2s : s.card = index K V
⊢ s.card ∈ Finset.card '' {t | (fun h ↦ g * h) '' K ⊆ ⋃ g ∈ t, (fun h ↦ g * 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 : Set G
hK : IsCompact K
V : Set G
hV : (interior V).Nonempty
g : G
s : Finset G
h1s : K ⊆ ⋃ g ∈ s, (fun h ↦ g * h) ⁻¹' V
h2s : s.card = index K V
⊢ (fun h ↦ g * h) '' K ⊆ ⋃ g_1 ∈ Finset.map (Equiv.toEmbedding (Equiv.mulRight g⁻¹)) s, (fun h ↦ g_1 * h) ⁻¹' V

Tactic:
;

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K : Set G
hK : IsCompact K
V : Set G
hV : (interior V).Nonempty
g : G
s : Finset G
h1s : K ⊆ ⋃ g ∈ s, (fun h ↦ g * h) ⁻¹' V
h2s : s.card = index K V
⊢ (fun h ↦ g * h) '' K ⊆ ⋃ g_1 ∈ Finset.map (Equiv.toEmbedding (Equiv.mulRight g⁻¹)) s, (fun h ↦ g_1 * 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 : Set G
hK : IsCompact K
V : Set G
hV : (interior V).Nonempty
g : G
s : Finset G
h1s : K ⊆ ⋃ g ∈ s, (fun h ↦ g * h) ⁻¹' V
h2s : s.card = index K V
g₁ g₂ : G
hg₂ : g₂ ∈ s
hg₁ : g₂ * g₁ ∈ V
⊢ g₂ * g⁻¹ * (g * g₁) ∈ V

Tactic:
;

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K : Set G
hK : IsCompact K
V : Set G
hV : (interior V).Nonempty
g : G
s : Finset G
h1s : K ⊆ ⋃ g ∈ s, (fun h ↦ g * h) ⁻¹' V
h2s : s.card = index K V
g₁ g₂ : G
hg₂ : g₂ ∈ s
hg₁ : g₂ * g₁ ∈ V
⊢ g₂ * g⁻¹ * (g * g₁) ∈ 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₀ : PositiveCompacts G
U : Set G
K : Compacts G
hU : (interior U).Nonempty
⊢ ↑(index (↑K) U) / ↑(index (↑K₀) U) ≤ ↑(index ↑K ↑K₀)

Tactic:
;

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
K : Compacts G
hU : (interior U).Nonempty
⊢ ↑(index (↑K) U) / ↑(index (↑K₀) U) ≤ ↑(index ↑K ↑K₀)
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
inst✝³ : PartialOrder E
inst✝² : IsOrderedAddMonoid E
inst✝¹ : IsOrderedModule ℝ E
μ : Measure X
f g : X → E
s : Set X
inst✝ : ClosedIciTopology E
hf : IntegrableOn f s μ
hg : IntegrableOn g s μ
hs : MeasurableSet s
h : ∀ᵐ (x : X) ∂μ, x ∈ s → f x ≤ g x
⊢ f ≤ᵐ[μ.restrict s] g

Tactic:
;

Goal state after:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : PartialOrder E
inst✝² : IsOrderedAddMonoid E
inst✝¹ : IsOrderedModule ℝ E
μ : Measure X
f g : X → E
s : Set X
inst✝ : ClosedIciTopology E
hf : IntegrableOn f s μ
hg : IntegrableOn g s μ
hs : MeasurableSet s
h : ∀ᵐ (x : X) ∂μ, x ∈ s → f x ≤ g x
⊢ f ≤ᵐ[μ.restrict s] 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
inst✝³ : PartialOrder E
inst✝² : IsOrderedAddMonoid E
inst✝¹ : IsOrderedModule ℝ E
μ : Measure X
f g : X → E
s : Set X
inst✝ : ClosedIciTopology E
hf : IntegrableOn f s μ
hg : IntegrableOn g s μ
hs : NullMeasurableSet s μ
h : ∀ᵐ (x : X) ∂μ, x ∈ s → f x ≤ g x
⊢ ∫ (x : X) in toMeasurable μ s, f x ∂μ ≤ ∫ (x : X) in s, g x ∂μ

Tactic:
setIntegral_congr_set hs.toMeasurable_ae_eq.symm

Goal state after:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : PartialOrder E
inst✝² : IsOrderedAddMonoid E
inst✝¹ : IsOrderedModule ℝ E
μ : Measure X
f g : X → E
s : Set X
inst✝ : ClosedIciTopology E
hf : IntegrableOn f s μ
hg : IntegrableOn g s μ
hs : NullMeasurableSet s μ
h : ∀ᵐ (x : X) ∂μ, x ∈ s → f x ≤ g x
⊢ ∫ (x : X) in toMeasurable μ s, f x ∂μ ≤ ∫ (x : X) in toMeasurable μ s, g 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₀ : PositiveCompacts G
U : Set G
hU : (interior U).Nonempty
K₁ K₂ : Compacts G
h : ↑K₁ ⊆ K₂.carrier
⊢ ↑(index (↑K₁) U) / ↑(index (↑K₀) U) ≤ ↑(index (↑K₂) U) / ↑(index (↑K₀) U)

Tactic:
;

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
hU : (interior U).Nonempty
K₁ K₂ : Compacts G
h : ↑K₁ ⊆ K₂.carrier
⊢ ↑(index (↑K₁) U) / ↑(index (↑K₀) U) ≤ ↑(index (↑K₂) U) / ↑(index (↑K₀) U)
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
⊢ ↑(index (↑(K₁ ⊔ K₂)) U) / ↑(index (↑K₀) U) ≤ ↑(index (↑K₁) U) / ↑(index (↑K₀) U) + ↑(index (↑K₂) U) / ↑(index (↑K₀) U)

Tactic:
;

Goal state after:
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
⊢ ↑(index (↑(K₁ ⊔ K₂)) U) / ↑(index (↑K₀) U) ≤ ↑(index (↑K₁) U) / ↑(index (↑K₀) U) + ↑(index (↑K₂) U) / ↑(index (↑K₀) U)
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⁻¹)
⊢ ↑(index (↑(K₁ ⊔ K₂)) U) / ↑(index (↑K₀) U) = ↑(index (↑K₁) U) / ↑(index (↑K₀) U) + ↑(index (↑K₂) U) / ↑(index (↑K₀) U)

Tactic:
;

Goal state after:
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⁻¹)
⊢ ↑(index (↑(K₁ ⊔ K₂)) U) / ↑(index (↑K₀) U) = ↑(index (↑K₁) U) / ↑(index (↑K₀) U) + ↑(index (↑K₂) U) / ↑(index (↑K₀) U)
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
hU : (interior U).Nonempty
K : Set G
hK : IsCompact K
a✝ : { carrier := K, isCompact' := hK } ∈ univ
⊢ prehaar (↑K₀) U { carrier := K, isCompact' := hK } ∈
    (fun K ↦ Icc 0 ↑(index ↑K ↑K₀)) { carrier := K, isCompact' := hK }

Tactic:
;

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
hU : (interior U).Nonempty
K : Set G
hK : IsCompact K
a✝ : { carrier := K, isCompact' := hK } ∈ univ
⊢ prehaar (↑K₀) U { carrier := K, isCompact' := hK } ∈
    (fun K ↦ Icc 0 ↑(index ↑K ↑K₀)) { carrier := K, isCompact' := hK }
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
hU : (interior U).Nonempty
K : Set G
hK : IsCompact K
a✝ : { carrier := K, isCompact' := hK } ∈ univ
⊢ 0 ≤ prehaar (↑K₀) U { carrier := K, isCompact' := hK } ∧
    prehaar (↑K₀) U { carrier := K, isCompact' := hK } ≤ ↑(index ↑{ carrier := K, isCompact' := hK } ↑K₀)

Tactic:
;

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
hU : (interior U).Nonempty
K : Set G
hK : IsCompact K
a✝ : { carrier := K, isCompact' := hK } ∈ univ
⊢ 0 ≤ prehaar (↑K₀) U { carrier := K, isCompact' := hK } ∧
    prehaar (↑K₀) U { carrier := K, isCompact' := hK } ≤ ↑(index ↑{ carrier := K, isCompact' := hK } ↑K₀)
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
⊢ ∀ (i : Compacts G), IsCompact (Icc 0 ↑(index ↑i ↑K₀))

Tactic:
;

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
⊢ ∀ (i : Compacts G), IsCompact (Icc 0 ↑(index ↑i ↑K₀))
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 : Compacts G
⊢ IsCompact (Icc 0 ↑(index ↑K ↑K₀))

Tactic:
;

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
K : Compacts G
⊢ IsCompact (Icc 0 ↑(index ↑K ↑K₀))
Module: Mathlib.Analysis.InnerProductSpace.Defs

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹ : RCLike 𝕜
inst✝ : SeminormedAddCommGroup E
c : InnerProductSpace 𝕜 E
x : E
⊢ 0 ≤ ‖x‖ ^ 2

Tactic:
;

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹ : RCLike 𝕜
inst✝ : SeminormedAddCommGroup E
c : InnerProductSpace 𝕜 E
x : E
⊢ 0 ≤ ‖x‖ ^ 2
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
this : IsCompact (haarProduct ↑K₀)
t : Finset (OpenNhdsOf 1)
V₀ : Set G := ⋂ V ∈ t, V.carrier
V : Set G
hV₁ : IsOpen[inst✝¹] V
hV₂ : 1 ∈ { carrier := V, is_open' := hV₁ }.carrier
a✝ : { carrier := V, is_open' := hV₁, mem' := hV₂ } ∈ t
⊢ IsOpen[inst✝¹] { carrier := V, is_open' := hV₁, mem' := hV₂ }.carrier

Tactic:
;

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (haarProduct ↑K₀)
t : Finset (OpenNhdsOf 1)
V₀ : Set G := ⋂ V ∈ t, V.carrier
V : Set G
hV₁ : IsOpen[inst✝¹] V
hV₂ : 1 ∈ { carrier := V, is_open' := hV₁ }.carrier
a✝ : { carrier := V, is_open' := hV₁, mem' := hV₂ } ∈ t
⊢ IsOpen[inst✝¹] { carrier := V, is_open' := hV₁, mem' := hV₂ }.carrier
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
⊢ (starRingEnd 𝕜) ⟪y, x⟫ + (starRingEnd 𝕜) ⟪z, x⟫ = ⟪x, y⟫ + ⟪x, z⟫

Tactic:
;

Goal state after:
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y z : F
⊢ (starRingEnd 𝕜) ⟪y, x⟫ + (starRingEnd 𝕜) ⟪z, x⟫ = ⟪x, y⟫ + ⟪x, z⟫
Module: Mathlib.MeasureTheory.Integral.Bochner.Set

Goal state before:
pp: case pos
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
s : Set X
hs : ∀ x ∈ s, f x ≤ 1
h's : ∀ x ∈ sᶜ, f x ≤ 0
H : Integrable f μ
⊢ ENNReal.ofReal (∫ (x : X), f x ∂μ) ≤ μ s

pp: case neg
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
s : Set X
hs : ∀ x ∈ s, f x ≤ 1
h's : ∀ x ∈ sᶜ, f x ≤ 0
H : ¬Integrable f μ
⊢ ENNReal.ofReal (∫ (x : X), f x ∂μ) ≤ μ s

Tactic:
;

Goal state after:
case pos
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
s : Set X
hs : ∀ x ∈ s, f x ≤ 1
h's : ∀ x ∈ sᶜ, f x ≤ 0
H : Integrable f μ
⊢ ENNReal.ofReal (∫ (x : X), f x ∂μ) ≤ μ s

case neg
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
s : Set X
hs : ∀ x ∈ s, f x ≤ 1
h's : ∀ x ∈ sᶜ, f x ≤ 0
H : ¬Integrable f μ
⊢ ENNReal.ofReal (∫ (x : X), f x ∂μ) ≤ μ 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₀ : PositiveCompacts G
this : IsCompact (haarProduct ↑K₀)
t : Finset (OpenNhdsOf 1)
V₀ : Set G := ⋂ V ∈ t, V.carrier
h1V₀ : IsOpen[inst✝¹] V₀
⊢ ∀ i ∈ t, 1 ∈ i.carrier

Tactic:
;

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (haarProduct ↑K₀)
t : Finset (OpenNhdsOf 1)
V₀ : Set G := ⋂ V ∈ t, V.carrier
h1V₀ : IsOpen[inst✝¹] V₀
⊢ ∀ i ∈ t, 1 ∈ i.carrier
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
this : IsCompact (haarProduct ↑K₀)
t : Finset (OpenNhdsOf 1)
V₀ : Set G := ⋂ V ∈ t, V.carrier
h1V₀ : IsOpen[inst✝¹] V₀
V : Set G
hV₁ : IsOpen[inst✝¹] V
hV₂ : 1 ∈ { carrier := V, is_open' := hV₁ }.carrier
i✝ : { carrier := V, is_open' := hV₁, mem' := hV₂ } ∈ t
⊢ 1 ∈ { carrier := V, is_open' := hV₁, mem' := hV₂ }.carrier

Tactic:
;

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (haarProduct ↑K₀)
t : Finset (OpenNhdsOf 1)
V₀ : Set G := ⋂ V ∈ t, V.carrier
h1V₀ : IsOpen[inst✝¹] V₀
V : Set G
hV₁ : IsOpen[inst✝¹] V
hV₂ : 1 ∈ { carrier := V, is_open' := hV₁ }.carrier
i✝ : { carrier := V, is_open' := hV₁, mem' := hV₂ } ∈ t
⊢ 1 ∈ { carrier := V, is_open' := hV₁, mem' := hV₂ }.carrier
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 : F
⊢ (starRingEnd 𝕜) 0 = 0

Tactic:
;

Goal state after:
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x : F
⊢ (starRingEnd 𝕜) 0 = 0
Module: Mathlib.MeasureTheory.Measure.Haar.Basic

Goal state before:
pp: case left
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (haarProduct ↑K₀)
t : Finset (OpenNhdsOf 1)
V₀ : Set G := ⋯
h1V₀ : IsOpen[inst✝¹] V₀
h2V₀ : 1 ∈ V₀
⊢ (interior V₀).Nonempty

Tactic:
;

Goal state after:
case left
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (haarProduct ↑K₀)
t : Finset (OpenNhdsOf 1)
V₀ : Set G := ⋯
h1V₀ : IsOpen[inst✝¹] V₀
h2V₀ : 1 ∈ V₀
⊢ (interior V₀).Nonempty
Module: Mathlib.MeasureTheory.Measure.Haar.Basic

Goal state before:
pp: case h
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (haarProduct ↑K₀)
t : Finset (OpenNhdsOf 1)
V₀ : Set G := ⋯
h1V₀ : IsOpen[inst✝¹] V₀
h2V₀ : 1 ∈ V₀
⊢ 1 ∈ interior V₀

Tactic:
;

Goal state after:
case h
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (haarProduct ↑K₀)
t : Finset (OpenNhdsOf 1)
V₀ : Set G := ⋯
h1V₀ : IsOpen[inst✝¹] V₀
h2V₀ : 1 ∈ V₀
⊢ 1 ∈ interior V₀
Module: Mathlib.MeasureTheory.Measure.Haar.Basic

Goal state before:
pp: case right
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (haarProduct ↑K₀)
t : Finset (OpenNhdsOf 1)
V₀ : Set G := ⋂ V ∈ t, V.carrier
h1V₀ : IsOpen[inst✝¹] V₀
h2V₀ : 1 ∈ V₀
⊢ ∀ i ∈ t, prehaar (↑K₀) V₀ ∈ clPrehaar (↑K₀) i

Tactic:
;

Goal state after:
case right
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (haarProduct ↑K₀)
t : Finset (OpenNhdsOf 1)
V₀ : Set G := ⋂ V ∈ t, V.carrier
h1V₀ : IsOpen[inst✝¹] V₀
h2V₀ : 1 ∈ V₀
⊢ ∀ i ∈ t, prehaar (↑K₀) V₀ ∈ clPrehaar (↑K₀) i