awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : 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) ↦ g * h) ⁻¹' V
h2s : s.card = index (K₁.carrier ∪ K₂.carrier) V
this :
  ∀ (K : Set G) (hK : K ⊆ ⋃ g ∈ s, (fun (x : G) ↦ g * x) ⁻¹' V),
    index K V ≤ {g ∈ s | ((fun (x : G) ↦ g * x) ⁻¹' V ∩ K).Nonempty}.card
g₁ : G
h_1 : g₁ ∈ s
g₂ : G
h2g₂ : g₂ ∈ K₁.carrier
g₃ : G
h2g₃ : g₃ ∈ K₂.carrier
h1g₃ : g₁ * g₃ ∈ V
h1g₂ : g₁ * g₂ ∈ V
⊢ ∃ x ∈ K₂.carrier, ∃ (y : G), y⁻¹ ∈ V ∧ x * y = g₁⁻¹

Tactic:
⟨_, h2g₃, (g₁ * g₃)⁻¹, ?_, ?_⟩

Premises used: HMul.hMul, Inv.inv, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : 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) ↦ g * h) ⁻¹' V
h2s : s.card = index (K₁.carrier ∪ K₂.carrier) V
this :
  ∀ (K : Set G) (hK : K ⊆ ⋃ g ∈ s, (fun (x : G) ↦ g * x) ⁻¹' V),
    index K V ≤ {g ∈ s | ((fun (x : G) ↦ g * x) ⁻¹' V ∩ K).Nonempty}.card
g₁ : G
h_1 : g₁ ∈ s
g₂ : G
h2g₂ : g₂ ∈ K₁.carrier
g₃ : G
h2g₃ : g₃ ∈ K₂.carrier
h1g₃ : g₁ * g₃ ∈ V
h1g₂ : g₁ * g₂ ∈ V
right : (g₁ * g₃)⁻¹⁻¹ ∈ V
right₁ : g₃ * (g₁ * g₃)⁻¹ = g₁⁻¹
⊢ ∃ x ∈ K₂.carrier, ∃ (y : G), y⁻¹ ∈ V ∧ x * y = g₁⁻¹

Tactic:
refine ⟨_, h2g₃, (g₁ * g₃)⁻¹, ?_, ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : 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) ↦ g * h) ⁻¹' V
h2s : s.card = index (K₁.carrier ∪ K₂.carrier) V
this :
  ∀ (K : Set G) (hK : K ⊆ ⋃ g ∈ s, (fun (x : G) ↦ g * x) ⁻¹' V),
    index K V ≤ {g ∈ s | ((fun (x : G) ↦ g * x) ⁻¹' V ∩ K).Nonempty}.card
g₁ : G
h_1 : g₁ ∈ s
g₂ : G
h2g₂ : g₂ ∈ K₁.carrier
g₃ : G
h2g₃ : g₃ ∈ K₂.carrier
h1g₃ : g₁ * g₃ ∈ V
h1g₂ : g₁ * g₂ ∈ V
⊢ (g₁ * g₃)⁻¹⁻¹ ∈ V

Tactic:
simp only [inv_inv, h1g₃]

Premises used: inv_inv
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : 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) ↦ g * h) ⁻¹' V
h2s : s.card = index (K₁.carrier ∪ K₂.carrier) V
this :
  ∀ (K : Set G) (hK : K ⊆ ⋃ g ∈ s, (fun (x : G) ↦ g * x) ⁻¹' V),
    index K V ≤ {g ∈ s | ((fun (x : G) ↦ g * x) ⁻¹' V ∩ K).Nonempty}.card
g₁ : G
h_1 : g₁ ∈ s
g₂ : G
h2g₂ : g₂ ∈ K₁.carrier
g₃ : G
h2g₃ : g₃ ∈ K₂.carrier
h1g₃ : g₁ * g₃ ∈ V
h1g₂ : g₁ * g₂ ∈ V
⊢ g₃ * (g₁ * g₃)⁻¹ = g₁⁻¹

Tactic:
simp only [mul_inv_rev, mul_inv_cancel_left]

Premises used: mul_inv_rev, mul_inv_cancel_left
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K : Set G
hK : IsCompact K
V : Set G
hV : (interior V).Nonempty
g : G
rcases :
  ∀ (s : Finset G) (h1s : K ⊆ ⋃ g ∈ s, (fun (h : G) ↦ g * h) ⁻¹' V) (h2s : s.card = index K V),
    index ((fun (h : G) ↦ g * h) '' K) V ≤ index K V
⊢ index ((fun (h : G) ↦ g * h) '' K) V ≤ index K V

Tactic:
rcases index_elim hK hV with ⟨s, h1s, h2s⟩

Premises used: MeasureTheory.Measure.haar.index_elim
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : 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) ↦ g * h) ⁻¹' V
h2s : s.card = index K V
rw : index ((fun (h : G) ↦ g * h) '' K) V ≤ s.card
⊢ index ((fun (h : G) ↦ g * h) '' K) V ≤ index K V

Tactic:
rw [← h2s]
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : 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) ↦ g * h) ⁻¹' V
h2s : s.card = index K V
hm :
  s.card ∈
    image.{u_1, 0} (α := Finset G) Finset.card
      {t : Finset G | Subset (α := Set G) ((fun (h : G) ↦ g * h) '' K) (⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V)}
⊢ index ((fun (h : G) ↦ g * h) '' K) V ≤ s.card

Tactic:
apply Nat.sInf_le

Premises used: Nat.sInf_le
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : 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) ↦ g * h) ⁻¹' V
h2s : s.card = index K V
⊢ ∃ (x : Finset G),
    Membership.mem (γ := Set (Finset G))
        {t : Finset G | Subset (α := Set G) ((fun (h : G) ↦ g * h) '' K) (⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V)} x ∧
      x.card = s.card

Tactic:
⟨s.map (Equiv.mulRight g⁻¹).toEmbedding, ?_, Finset.card_map _⟩

Premises used: Finset.card_map, Finset.map, Inv.inv, Equiv.toEmbedding, Equiv.mulRight, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : 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) ↦ g * h) ⁻¹' V
h2s : s.card = index K V
hm :
  Membership.mem (γ := Set (Finset G))
    {t : Finset G | Subset (α := Set G) ((fun (h : G) ↦ g * h) '' K) (⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V)}
    (Finset.map (Equiv.toEmbedding (Equiv.mulRight g⁻¹)) s)
⊢ ∃ (x : Finset G),
    Membership.mem (γ := Set (Finset G))
        {t : Finset G | Subset (α := Set G) ((fun (h : G) ↦ g * h) '' K) (⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V)} x ∧
      x.card = s.card

Tactic:
refine ⟨s.map (Equiv.mulRight g⁻¹).toEmbedding, ?_, Finset.card_map _⟩
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : 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) ↦ g * h) ⁻¹' V
h2s : s.card = index K V
⊢ Subset (α := Set G) ((fun (h : G) ↦ g * h) '' K)
    (⋃ g_1 ∈ Finset.map (Equiv.toEmbedding (Equiv.mulRight g⁻¹)) s, (fun (h : G) ↦ g_1 * h) ⁻¹' V)

Tactic:
Subset.trans (image_mono h1s) ?_

Premises used: Set.Subset.trans, Set.image_mono
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : 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) ↦ g * h) ⁻¹' V
h2s : s.card = index K V
hm :
  Subset.{u_1} (α := Set G) ((fun (h : G) ↦ g * h) '' ⋃ g ∈ s, (fun (h : G) ↦ g * h) ⁻¹' V)
    (⋃ g_1 ∈ Finset.map (Equiv.toEmbedding (Equiv.mulRight g⁻¹)) s, (fun (h : G) ↦ g_1 * h) ⁻¹' V)
⊢ Subset (α := Set G) ((fun (h : G) ↦ g * h) '' K)
    (⋃ g_1 ∈ Finset.map (Equiv.toEmbedding (Equiv.mulRight g⁻¹)) s, (fun (h : G) ↦ g_1 * h) ⁻¹' V)

Tactic:
refine Subset.trans (image_mono h1s) ?_

Premises used: Set.Subset.trans, Set.image_mono
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : 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) ↦ g * h) ⁻¹' V
h2s : s.card = index K V
g₁ g₂ : G
hg₂ : g₂ ∈ s
hg₁ : Membership.mem (γ := Set G) ((fun (h : g₂ ∈ s) ↦ ((fun (h : G) ↦ g₂ * h) ⁻¹' V : Set G)) hg₂) g₁
⊢ g₂ * g₁ ∈ V

Tactic:
simp only [mem_preimage] at hg₁

Premises used: Set.mem_preimage
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : 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) ↦ g * h) ⁻¹' V
h2s : s.card = index K V
g₁ g₂ : G
hg₂ : g₂ ∈ s
hg₁ : g₂ * g₁ ∈ V
hm : ∃ a ∈ s, a * g⁻¹ * (g * g₁) ∈ V
⊢ Membership.mem (γ := Set G)
    (⋃ g_1 ∈ Finset.map (Equiv.toEmbedding (Equiv.mulRight g⁻¹)) s, (fun (h : G) ↦ g_1 * h) ⁻¹' V)
    ((fun (h : G) ↦ g * h) g₁)

Tactic:
simp only [exists_prop, mem_iUnion, Finset.mem_map, Equiv.coe_mulRight,
    exists_exists_and_eq_and, mem_preimage, Equiv.toEmbedding_apply]

Premises used: Set.mem_iUnion, Equiv.toEmbedding_apply, exists_prop, exists_exists_and_eq_and, Equiv.coe_mulRight, Finset.mem_map, Set.mem_preimage
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : 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) ↦ g * h) ⁻¹' V
h2s : s.card = index K V
g₁ g₂ : G
hg₂ : g₂ ∈ s
hg₁ : g₂ * g₁ ∈ V
⊢ ∃ a ∈ s, a * g⁻¹ * (g * g₁) ∈ V

Tactic:
⟨_, hg₂, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : 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) ↦ g * h) ⁻¹' V
h2s : s.card = index K V
g₁ g₂ : G
hg₂ : g₂ ∈ s
hg₁ : g₂ * g₁ ∈ V
hm : g₂ * g⁻¹ * (g * g₁) ∈ V
⊢ ∃ a ∈ s, a * g⁻¹ * (g * g₁) ∈ V

Tactic:
refine ⟨_, hg₂, ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : 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) ↦ 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:
simp only [mul_assoc, hg₁, inv_mul_cancel_left]

Premises used: inv_mul_cancel_left, mul_assoc
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K : Set G
hK : IsCompact K
g : G
V : Set G
hV : (interior V).Nonempty
⊢ index ((fun (h : G) ↦ g * h) '' K) V = index K V

Tactic:
le_antisymm (mul_left_index_le hK hV g) ?_

Premises used: le_antisymm, MeasureTheory.Measure.haar.mul_left_index_le
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K : Set G
hK : IsCompact K
g : G
V : Set G
hV : (interior V).Nonempty
refine : index K V ≤ index ((fun (h : G) ↦ g * h) '' K) V
⊢ index ((fun (h : G) ↦ g * h) '' K) V = index K V

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

Premises used: le_antisymm, MeasureTheory.Measure.haar.mul_left_index_le
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K : Set G
hK : IsCompact K
g : G
V : Set G
hV : (interior V).Nonempty
⊢ index ((fun (h : G) ↦ g⁻¹ * h) '' (fun (x : G) ↦ g * x) '' K) V ≤ index ((fun (x : G) ↦ g * x) '' K) V

Tactic:
mul_left_index_le (hK.image <| continuous_const_mul g) hV g⁻¹

Premises used: continuous_const_mul, Inv.inv, MeasureTheory.Measure.haar.mul_left_index_le, IsCompact.image
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K : Set G
hK : IsCompact K
g : G
V : Set G
hV : (interior V).Nonempty
h : K = (fun (h : G) ↦ g⁻¹ * h) '' (fun (x : G) ↦ g * x) '' K
⊢ index K V ≤ index ((fun (h : G) ↦ g * h) '' K) V

Tactic:
convert! mul_left_index_le (hK.image <| continuous_const_mul g) hV g⁻¹

Premises used: continuous_const_mul, Inv.inv, MeasureTheory.Measure.haar.mul_left_index_le, IsCompact.image
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K : Set G
hK : IsCompact K
g : G
V : Set G
hV : (interior V).Nonempty
h : K = (fun (x : G) ↦ g⁻¹ * (g * x)) '' K
⊢ K = (fun (h : G) ↦ g⁻¹ * h) '' (fun (x : G) ↦ g * x) '' K

Tactic:
rw [image_image]

Premises used: Set.image_image
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K : Set G
hK : IsCompact K
g : G
V : Set G
hV : (interior V).Nonempty
⊢ K = (fun (x : G) ↦ g⁻¹ * (g * x)) '' K

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
K : Compacts G
hU : (interior U).Nonempty
rw :
  (↑(index (↑K : Set G) U) : ℝ) ≤
    HMul.hMul (α := ℝ) (↑(index (↑K : Set G) (↑K₀ : Set G)) : ℝ) (↑(index (↑K₀ : Set G) U) : ℝ)
rw₁ : LT.lt (α := ℝ) 0 (↑(index (↑K₀ : Set G) U) : ℝ)
⊢ HDiv.hDiv (α := ℝ) (↑(index (↑K : Set G) U) : ℝ) (↑(index (↑K₀ : Set G) U) : ℝ) ≤
    (↑(index (↑K : Set G) (↑K₀ : Set G)) : ℝ)

Tactic:
rw [div_le_iff₀]

Premises used: div_le_iff₀
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
K : Compacts G
hU : (interior U).Nonempty
norm_cast : index (↑K : Set G) U ≤ index (↑K : Set G) (↑K₀ : Set G) * index (↑K₀ : Set G) U
⊢ (↑(index (↑K : Set G) U) : ℝ) ≤
    HMul.hMul (α := ℝ) (↑(index (↑K : Set G) (↑K₀ : Set G)) : ℝ) (↑(index (↑K₀ : Set G) U) : ℝ)

Tactic:
norm_cast
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
K : Compacts G
hU : (interior U).Nonempty
norm_cast : 0 < index (↑K₀ : Set G) U
⊢ LT.lt (α := ℝ) 0 (↑(index (↑K₀ : Set G) U) : ℝ)

Tactic:
norm_cast
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
K : Compacts G
hU : (interior U).Nonempty
⊢ index (↑K : Set G) U ≤ index (↑K : Set G) (↑K₀ : Set G) * index (↑K₀ : Set G) U

Tactic:
apply le_index_mul K₀ K hU

Premises used: MeasureTheory.Measure.haar.le_index_mul
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
K : Compacts G
hU : (interior U).Nonempty
⊢ 0 < index (↑K₀ : Set G) U

Tactic:
index_pos K₀ hU

Premises used: MeasureTheory.Measure.haar.index_pos
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
K : Compacts G
hU : (interior U).Nonempty
⊢ 0 < index (↑K₀ : Set G) U

Tactic:
exact index_pos K₀ hU

Premises used: MeasureTheory.Measure.haar.index_pos
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
hU : (interior U).Nonempty
K : Set G
h1K : IsCompact K
h2K : (interior K).Nonempty
ha : LT.lt (α := ℝ) 0 (↑(index (↑{ carrier := K, isCompact' := h1K : Compacts G } : Set G) U) : ℝ)
hb : LT.lt (α := ℝ) 0 (↑(index (↑K₀ : Set G) U) : ℝ)
⊢ 0 < prehaar (↑K₀ : Set G) U { carrier := K, isCompact' := h1K : Compacts G }

Tactic:
apply div_pos

Premises used: div_pos
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
hU : (interior U).Nonempty
K : Set G
h1K : IsCompact K
h2K : (interior K).Nonempty
ha : 0 < index (↑{ carrier := K, isCompact' := h1K : Compacts G } : Set G) U
⊢ LT.lt (α := ℝ) 0 (↑(index (↑{ carrier := K, isCompact' := h1K : Compacts G } : Set G) U) : ℝ)

Tactic:
norm_cast
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
hU : (interior U).Nonempty
K : Set G
h1K : IsCompact K
h2K : (interior K).Nonempty
hb : 0 < index (↑K₀ : Set G) U
⊢ LT.lt (α := ℝ) 0 (↑(index (↑K₀ : Set G) U) : ℝ)

Tactic:
norm_cast
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
hU : (interior U).Nonempty
K : Set G
h1K : IsCompact K
h2K : (interior K).Nonempty
⊢ 0 < index (↑{ carrier := K, isCompact' := h1K : Compacts G } : Set G) U

Tactic:
apply index_pos ⟨⟨K, h1K⟩, h2K⟩ hU

Premises used: TopologicalSpace.Compacts.mk, MeasureTheory.Measure.haar.index_pos, TopologicalSpace.PositiveCompacts.mk
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
hU : (interior U).Nonempty
K : Set G
h1K : IsCompact K
h2K : (interior K).Nonempty
⊢ 0 < index (↑K₀ : Set G) U

Tactic:
index_pos K₀ hU

Premises used: MeasureTheory.Measure.haar.index_pos
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
hU : (interior U).Nonempty
K : Set G
h1K : IsCompact K
h2K : (interior K).Nonempty
⊢ 0 < index (↑K₀ : Set G) U

Tactic:
exact index_pos K₀ hU

Premises used: MeasureTheory.Measure.haar.index_pos
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
hU : (interior U).Nonempty
K₁ K₂ : Compacts G
h : (↑K₁ : Set G) ⊆ K₂.carrier
rw : LE.le (α := ℝ) (↑(index (↑K₁ : Set G) U) : ℝ) (↑(index (↑K₂ : Set G) U) : ℝ)
rw₁ : LT.lt (α := ℝ) 0 (↑(index (↑K₀ : Set G) U) : ℝ)
⊢ HDiv.hDiv (α := ℝ) (↑(index (↑K₁ : Set G) U) : ℝ) (↑(index (↑K₀ : Set G) U) : ℝ) ≤
    HDiv.hDiv (α := ℝ) (↑(index (↑K₂ : Set G) U) : ℝ) (↑(index (↑K₀ : Set G) U) : ℝ)

Tactic:
rw [div_le_div_iff_of_pos_right]

Premises used: div_le_div_iff_of_pos_right
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
hU : (interior U).Nonempty
K₁ K₂ : Compacts G
h : (↑K₁ : Set G) ⊆ K₂.carrier
⊢ LE.le (α := ℝ) (↑(index (↑K₁ : Set G) U) : ℝ) (↑(index (↑K₂ : Set G) U) : ℝ)

Tactic:
mod_cast index_mono K₂.2 h hU

Premises used: cast, TopologicalSpace.Compacts.isCompact', Nat.cast_le._simp_1, MeasureTheory.Measure.haar.index_mono, Eq.symm
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
hU : (interior U).Nonempty
K₁ K₂ : Compacts G
h : (↑K₁ : Set G) ⊆ K₂.carrier
⊢ LE.le (α := ℝ) (↑(index (↑K₁ : Set G) U) : ℝ) (↑(index (↑K₂ : Set G) U) : ℝ)

Tactic:
exact mod_cast index_mono K₂.2 h hU

Premises used: TopologicalSpace.Compacts.isCompact', MeasureTheory.Measure.haar.index_mono
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
hU : (interior U).Nonempty
K₁ K₂ : Compacts G
h : (↑K₁ : Set G) ⊆ K₂.carrier
⊢ LT.lt (α := ℝ) 0 (↑(index (↑K₀ : Set G) U) : ℝ)

Tactic:
mod_cast index_pos K₀ hU

Premises used: congrArg, Nat.cast_lt._simp_1, cast, Nat.cast, MeasureTheory.Measure.haar.index, SetLike.coe, LT.lt, MeasureTheory.Measure.haar.index_pos, congrFun', Nat.cast_zero, Eq.symm, Eq.trans
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
hU : (interior U).Nonempty
K₁ K₂ : Compacts G
h : (↑K₁ : Set G) ⊆ K₂.carrier
⊢ LT.lt (α := ℝ) 0 (↑(index (↑K₀ : Set G) U) : ℝ)

Tactic:
exact mod_cast index_pos K₀ hU

Premises used: MeasureTheory.Measure.haar.index_pos
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
hU : (interior U).Nonempty
⊢ prehaar (↑K₀ : Set G) U K₀.toCompacts = 1

Tactic:
div_self <| ne_of_gt <| mod_cast index_pos K₀ hU

Premises used: ne_of_gt, MeasureTheory.Measure.haar.prehaar, div_self
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
K₁ K₂ : Compacts G
hU : (interior U).Nonempty
rw :
  (↑(index (↑(K₁ ⊔ K₂) : Set G) U) : ℝ) ≤
    HAdd.hAdd (α := ℝ) (↑(index (↑K₁ : Set G) U) : ℝ) (↑(index (↑K₂ : Set G) U) : ℝ)
rw₁ : LT.lt (α := ℝ) 0 (↑(index (↑K₀ : Set G) U) : ℝ)
⊢ HDiv.hDiv (α := ℝ) (↑(index (↑(K₁ ⊔ K₂) : Set G) U) : ℝ) (↑(index (↑K₀ : Set G) U) : ℝ) ≤
    HDiv.hDiv (α := ℝ) (↑(index (↑K₁ : Set G) U) : ℝ) (↑(index (↑K₀ : Set G) U) : ℝ) +
      HDiv.hDiv (α := ℝ) (↑(index (↑K₂ : Set G) U) : ℝ) (↑(index (↑K₀ : Set G) U) : ℝ)

Tactic:
rw [← add_div, div_le_div_iff_of_pos_right]

Premises used: div_le_div_iff_of_pos_right, add_div
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
K₁ K₂ : Compacts G
hU : (interior U).Nonempty
⊢ (↑(index (↑(K₁ ⊔ K₂) : Set G) U) : ℝ) ≤
    HAdd.hAdd (α := ℝ) (↑(index (↑K₁ : Set G) U) : ℝ) (↑(index (↑K₂ : Set G) U) : ℝ)

Tactic:
mod_cast index_union_le K₁ K₂ hU

Premises used: congrArg, Nat.cast_add._simp_1, cast, Nat.cast_le._simp_1, LE.le, Nat.cast, MeasureTheory.Measure.haar.index, SetLike.coe, Max.max, Eq.symm, Eq.trans, MeasureTheory.Measure.haar.index_union_le
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
K₁ K₂ : Compacts G
hU : (interior U).Nonempty
⊢ (↑(index (↑(K₁ ⊔ K₂) : Set G) U) : ℝ) ≤
    HAdd.hAdd (α := ℝ) (↑(index (↑K₁ : Set G) U) : ℝ) (↑(index (↑K₂ : Set G) U) : ℝ)

Tactic:
exact mod_cast index_union_le K₁ K₂ hU

Premises used: MeasureTheory.Measure.haar.index_union_le
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
K₁ K₂ : Compacts G
hU : (interior U).Nonempty
⊢ LT.lt (α := ℝ) 0 (↑(index (↑K₀ : Set G) U) : ℝ)

Tactic:
mod_cast index_pos K₀ hU

Premises used: congrArg, Nat.cast_lt._simp_1, cast, Nat.cast, MeasureTheory.Measure.haar.index, SetLike.coe, LT.lt, MeasureTheory.Measure.haar.index_pos, congrFun', Nat.cast_zero, Eq.symm, Eq.trans
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
K₁ K₂ : Compacts G
hU : (interior U).Nonempty
⊢ LT.lt (α := ℝ) 0 (↑(index (↑K₀ : Set G) U) : ℝ)

Tactic:
exact mod_cast index_pos K₀ hU

Premises used: MeasureTheory.Measure.haar.index_pos
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
K₁ K₂ : Compacts G
hU : (interior U).Nonempty
h : Disjoint (K₁.carrier * U⁻¹) (K₂.carrier * U⁻¹)
rw :
  HDiv.hDiv (α := ℝ) (↑(index (↑(K₁ ⊔ K₂) : Set G) U) : ℝ) (↑(index (↑K₀ : Set G) U) : ℝ) =
    HAdd.hAdd (α := ℝ) (↑(index (↑K₁ : Set G) U) : ℝ) (↑(index (↑K₂ : Set G) U) : ℝ) / (↑(index (↑K₀ : Set G) U) : ℝ)
⊢ HDiv.hDiv (α := ℝ) (↑(index (↑(K₁ ⊔ K₂) : Set G) U) : ℝ) (↑(index (↑K₀ : Set G) U) : ℝ) =
    HDiv.hDiv (α := ℝ) (↑(index (↑K₁ : Set G) U) : ℝ) (↑(index (↑K₀ : Set G) U) : ℝ) +
      HDiv.hDiv (α := ℝ) (↑(index (↑K₂ : Set G) U) : ℝ) (↑(index (↑K₀ : Set G) U) : ℝ)

Tactic:
rw [← add_div]

Premises used: add_div