awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
inst : MeasurableSpace γ
m : Measure α
f : α → Measure β
g : β → Measure γ
hf : AEMeasurable f m
hg : AEMeasurable g (m.bind f)
h :
  ∀ (s : Set γ) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) (((m.bind f).bind g : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
      (((m.bind fun (a : α) ↦ (f a).bind g : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
⊢ (m.bind f).bind g = m.bind fun (a : α) ↦ (f a).bind g

Tactic:
ext1 s hs
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
inst : MeasurableSpace γ
m : Measure α
f : α → Measure β
g : β → Measure γ
hf : AEMeasurable f m
hg : AEMeasurable g (m.bind f)
s : Set γ
hs : MeasurableSet s
h : ∫⁻ (a : α), ∫⁻ (x : β), (g x : (a : Set γ) → ℝ≥0∞) s ∂f a ∂m = ∫⁻ (a : α), ((f a).bind g : (a : Set γ) → ℝ≥0∞) s ∂m
h₁ : AEMeasurable.{u_1, u_3} (β := Measure γ) (fun (a : α) ↦ (f a).bind g) m
h₂ : AEMeasurable (β := ℝ≥0∞) (fun (a : β) ↦ (g a : (a : Set γ) → ℝ≥0∞) s) (m.bind f)
⊢ Eq (α := ℝ≥0∞) (((m.bind f).bind g : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    (((m.bind fun (a : α) ↦ (f a).bind g : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [bind_apply hs hg, lintegral_bind hf, bind_apply hs]

Premises used: MeasureTheory.Measure.bind_apply, MeasureTheory.Measure.lintegral_bind
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
inst : MeasurableSpace γ
m : Measure α
f : α → Measure β
g : β → Measure γ
hf : AEMeasurable f m
hg : AEMeasurable g (m.bind f)
s : Set γ
hs : MeasurableSet s
⊢ ∫⁻ (a : α), ∫⁻ (x : β), (g x : (a : Set γ) → ℝ≥0∞) s ∂f a ∂m = ∫⁻ (a : α), ((f a).bind g : (a : Set γ) → ℝ≥0∞) s ∂m

Tactic:
lintegral_congr_ae <| (hf.ae_of_bind hg).mono fun a ha ↦ .symm <| bind_apply hs ha

Premises used: MeasureTheory.Measure.bind_apply, AEMeasurable.ae_of_bind, MeasureTheory.lintegral_congr_ae, Filter.Eventually.mono, Eq.symm
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
inst : MeasurableSpace γ
m : Measure α
f : α → Measure β
g : β → Measure γ
hf : AEMeasurable f m
hg : AEMeasurable g (m.bind f)
s : Set γ
hs : MeasurableSet s
⊢ ∫⁻ (a : α), ∫⁻ (x : β), (g x : (a : Set γ) → ℝ≥0∞) s ∂f a ∂m = ∫⁻ (a : α), ((f a).bind g : (a : Set γ) → ℝ≥0∞) s ∂m

Tactic:
exact lintegral_congr_ae <| (hf.ae_of_bind hg).mono fun a ha ↦ .symm <| bind_apply hs ha

Premises used: AEMeasurable.ae_of_bind, MeasureTheory.lintegral_congr_ae, Filter.Eventually.mono
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
inst : MeasurableSpace γ
m : Measure α
f : α → Measure β
g : β → Measure γ
hf : AEMeasurable f m
hg : AEMeasurable g (m.bind f)
s : Set γ
hs : MeasurableSet s
⊢ AEMeasurable.{u_1, u_3} (β := Measure γ) (fun (a : α) ↦ (f a).bind g) m

Tactic:
(aemeasurable_bind hg).comp_aemeasurable hf

Premises used: MeasureTheory.Measure.join, MeasureTheory.Measure.bind, MeasureTheory.Measure.ofMeasurable, MeasureTheory.Measure.aemeasurable_bind, AEMeasurable.comp_aemeasurable
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
inst : MeasurableSpace γ
m : Measure α
f : α → Measure β
g : β → Measure γ
hf : AEMeasurable f m
hg : AEMeasurable g (m.bind f)
s : Set γ
hs : MeasurableSet s
⊢ AEMeasurable.{u_1, u_3} (β := Measure γ) (fun (a : α) ↦ (f a).bind g) m

Tactic:
exact (aemeasurable_bind hg).comp_aemeasurable hf

Premises used: MeasureTheory.Measure.aemeasurable_bind, AEMeasurable.comp_aemeasurable
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
inst : MeasurableSpace γ
m : Measure α
f : α → Measure β
g : β → Measure γ
hf : AEMeasurable f m
hg : AEMeasurable g (m.bind f)
s : Set γ
hs : MeasurableSet s
⊢ AEMeasurable (β := ℝ≥0∞) (fun (a : β) ↦ (g a : (a : Set γ) → ℝ≥0∞) s) (m.bind f)

Tactic:
(measurable_coe hs).comp_aemeasurable hg

Premises used: MeasureTheory.Measure.measurable_coe, Measurable.comp_aemeasurable
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
inst : MeasurableSpace γ
m : Measure α
f : α → Measure β
g : β → Measure γ
hf : AEMeasurable f m
hg : AEMeasurable g (m.bind f)
s : Set γ
hs : MeasurableSet s
⊢ AEMeasurable (β := ℝ≥0∞) (fun (a : β) ↦ (g a : (a : Set γ) → ℝ≥0∞) s) (m.bind f)

Tactic:
exact (measurable_coe hs).comp_aemeasurable hg

Premises used: MeasureTheory.Measure.measurable_coe, Measurable.comp_aemeasurable
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → Measure β
hf : Measurable f
a : α
⊢ bind (mα := mα) (dirac a) f = f a

Tactic:
simp [bind, map_dirac' hf]

Premises used: MeasureTheory.Measure.bind, MeasureTheory.Measure.map_dirac'
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
mα : MeasurableSpace α
m : Measure α
h :
  ∀ (s : Set α) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) (((m.bind dirac : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ m.bind dirac = m

Tactic:
ext1 s hs
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
mα : MeasurableSpace α
m : Measure α
s : Set α
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) (((m.bind dirac : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp only [bind_apply hs measurable_dirac.aemeasurable, dirac_apply' _ hs, lintegral_indicator hs,
    Pi.one_apply, lintegral_one, restrict_apply, MeasurableSet.univ, univ_inter]

Premises used: MeasureTheory.Measure.bind_apply, Measurable.aemeasurable, Pi.one_apply, MeasureTheory.Measure.restrict_apply, MeasureTheory.Measure.dirac_apply', Set.univ_inter, MeasureTheory.lintegral_indicator, MeasureTheory.Measure.measurable_dirac, MeasurableSet.univ, MeasureTheory.lintegral_one
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
m : Measure α
f : α → β
hf : Measurable f
hg : Measurable.{u_2, u_2} (α := β) (β := Measure β) dirac
hf₁ : Measurable f
⊢ Eq (α := Measure β) (m.bind fun (x : α) ↦ dirac (f x)) (map f m)

Tactic:
rw [← bind_dirac (m := m.map f), bind, bind, map_map, Function.comp_def]

Premises used: MeasureTheory.Measure.bind, Function.comp_def, MeasureTheory.Measure.bind_dirac, MeasureTheory.Measure.map_map
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
m : Measure α
f : α → β
hf : Measurable f
⊢ Measurable.{u_2, u_2} (α := β) (β := Measure β) dirac

Tactic:
measurable_dirac

Premises used: MeasureTheory.Measure.measurable_dirac
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
m : Measure α
f : α → β
hf : Measurable f
⊢ Measurable f

Tactic:
hf
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
m : Measure α
f : α → β
hf : Measurable f
⊢ Measurable.{u_2, u_2} (α := β) (β := Measure β) dirac

Tactic:
exacts [measurable_dirac, hf]

Premises used: MeasureTheory.Measure.measurable_dirac
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure (Measure α)
rw : μ.join = join (map id μ)
rw₁ rw₂ : μ.join = μ.join
⊢ μ.join = μ.bind id

Tactic:
rw [bind, map_id]

Premises used: MeasureTheory.Measure.map_id, MeasureTheory.Measure.bind
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Measurable f
μ : Measure (Measure α)
h :
  ∀ (s : Set β) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) (((join (map (map f) μ) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
      (((map f μ.join : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := Measure β) (join (map (map f) μ)) (map f μ.join)

Tactic:
ext1 s hs
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Measurable f
μ : Measure (Measure α)
s : Set β
hs : MeasurableSet s
h :
  ∫⁻ (a : Measure α), ((map f a : Measure β) : (a : Set β) → ℝ≥0∞) s ∂μ =
    ∫⁻ (μ : Measure α), (μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) ∂μ
⊢ Eq (α := ℝ≥0∞) (((join (map (map f) μ) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    (((map f μ.join : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [join_apply hs, map_apply hf hs, join_apply (hf hs),
    lintegral_map (measurable_coe hs) (measurable_map f hf)]

Premises used: MeasureTheory.Measure.measurable_coe, MeasureTheory.Measure.measurable_map, MeasureTheory.Measure.map_apply, MeasureTheory.lintegral_map, MeasureTheory.Measure.join_apply
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Measurable f
μ : Measure (Measure α)
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (a : Measure α), ((map f a : Measure β) : (a : Set β) → ℝ≥0∞) s ∂μ =
    ∫⁻ (μ : Measure α), (μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) ∂μ

Tactic:
simp_rw [map_apply hf hs]

Premises used: MeasureTheory.Measure.map_apply
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure (Measure (Measure α))
rw : μ.bind join = μ.bind fun (a : Measure (Measure α)) ↦ (id a).bind id
⊢ μ.bind join = μ.join.join

Tactic:
rw [join_eq_bind, join_eq_bind, bind_bind aemeasurable_id aemeasurable_id]

Premises used: MeasureTheory.Measure.join_eq_bind, MeasureTheory.Measure.bind_bind, aemeasurable_id
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure (Measure (Measure α))
apply : Eq.{u_1 + 1} (α := Measure (Measure α) → Measure α) join fun (a : Measure (Measure α)) ↦ (id a).bind id
⊢ μ.bind join = μ.bind fun (a : Measure (Measure α)) ↦ (id a).bind id

Tactic:
apply congr_arg (bind μ)

Premises used: MeasureTheory.Measure.bind, congr_arg
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure (Measure (Measure α))
h : ∀ (ν : Measure (Measure α)), ν.join = (id ν).bind id
⊢ Eq.{u_1 + 1} (α := Measure (Measure α) → Measure α) join fun (a : Measure (Measure α)) ↦ (id a).bind id

Tactic:
funext ν
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure (Measure (Measure α))
ν : Measure (Measure α)
⊢ ν.join = (id ν).bind id

Tactic:
join_eq_bind ν

Premises used: MeasureTheory.Measure.join_eq_bind
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure (Measure (Measure α))
ν : Measure (Measure α)
⊢ ν.join = (id ν).bind id

Tactic:
exact join_eq_bind ν

Premises used: MeasureTheory.Measure.join_eq_bind
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
⊢ join (map dirac μ) = μ

Tactic:
bind_dirac

Premises used: MeasureTheory.Measure.bind, MeasureTheory.Measure.bind_dirac
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
V : Set G
⊢ index ∅ V = 0

Tactic:
simp [index]

Premises used: MeasureTheory.Measure.haar.index
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
K₀ : PositiveCompacts G
U : Set G
rw : HDiv.hDiv (α := ℝ) (↑(index (↑⊥ : Set G) U) : ℝ) (↑(index (↑K₀ : Set G) U) : ℝ) = 0
rw₁ : HDiv.hDiv (α := ℝ) (↑(index ∅ U) : ℝ) (↑(index (↑K₀ : Set G) U) : ℝ) = 0
rw₂ : HDiv.hDiv (α := ℝ) (↑0 : ℝ) (↑(index (↑K₀ : Set G) U) : ℝ) = 0
rw₃ : HDiv.hDiv (α := ℝ) 0 (↑(index (↑K₀ : Set G) U) : ℝ) = 0
rw₄ rw₅ : Eq (α := ℝ) 0 0
⊢ prehaar (↑K₀ : Set G) U ⊥ = 0

Tactic:
rw [prehaar, Compacts.coe_bot, index_empty, Nat.cast_zero, zero_div]

Premises used: zero_div, TopologicalSpace.Compacts.coe_bot, MeasureTheory.Measure.haar.index_empty, Nat.cast_zero, MeasureTheory.Measure.haar.prehaar
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
K₀ : PositiveCompacts G
U : Set G
K : Compacts G
ha : LE.le (α := ℝ) 0 (↑(index (↑K : Set G) U) : ℝ)
hb : LE.le (α := ℝ) 0 (↑(index (↑K₀ : Set G) U) : ℝ)
⊢ 0 ≤ prehaar (↑K₀ : Set G) U K

Tactic:
apply div_nonneg

Premises used: div_nonneg
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
K₀ : PositiveCompacts G
U : Set G
K : Compacts G
ha : 0 ≤ index (↑K : Set G) U
⊢ LE.le (α := ℝ) 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
K₀ : PositiveCompacts G
U : Set G
K : Compacts G
hb : 0 ≤ index (↑K₀ : Set G) U
⊢ LE.le (α := ℝ) 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
K₀ : PositiveCompacts G
U : Set G
K : Compacts G
⊢ 0 ≤ index (↑K : Set G) U

Tactic:
apply zero_le

Premises used: zero_le
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
K₀ : PositiveCompacts G
U : Set G
K : Compacts G
⊢ 0 ≤ index (↑K₀ : Set G) U

Tactic:
apply zero_le

Premises used: zero_le
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
K₀ : Set G
f : Compacts G → ℝ
⊢ Membership.mem (γ := Set (Compacts G → ℝ)) (haarProduct K₀) f ↔
    ∀ (K : Compacts G), Membership.mem (γ := Set ℝ) (Icc 0 (↑(index (↑K : Set G) K₀) : ℝ)) (f K)

Tactic:
simp only [haarProduct, Set.pi, forall_prop_of_true, mem_univ, mem_setOf_eq]

Premises used: MeasureTheory.Measure.haar.haarProduct, Set.mem_setOf_eq, forall_prop_of_true, Set.mem_univ, Set.pi
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K V : Set G
hK : IsCompact K
hV : (interior V).Nonempty
rcases :
  ∀ (t : Finset G) (ht : K ⊆ ⋃ g ∈ t, (fun (x : G) ↦ g * x) ⁻¹' V),
    ∃ (n : ℕ), n ∈ image.{u_1, 0} (α := Finset G) Finset.card {t : Finset G | K ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V}
⊢ ∃ (n : ℕ), n ∈ image.{u_1, 0} (α := Finset G) Finset.card {t : Finset G | K ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V}

Tactic:
rcases compact_covered_by_mul_left_translates hK hV with ⟨t, ht⟩

Premises used: compact_covered_by_mul_left_translates
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K V : Set G
hK : IsCompact K
hV : (interior V).Nonempty
t : Finset G
ht : K ⊆ ⋃ g ∈ t, (fun (x : G) ↦ g * x) ⁻¹' V
⊢ ∃ (n : ℕ), n ∈ image.{u_1, 0} (α := Finset G) Finset.card {t : Finset G | K ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V}

Tactic:
⟨t.card, t, ht, rfl⟩

Premises used: And.intro, Exists.intro, Finset.card, rfl
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K V : Set G
hK : IsCompact K
hV : (interior V).Nonempty
t : Finset G
ht : K ⊆ ⋃ g ∈ t, (fun (x : G) ↦ g * x) ⁻¹' V
⊢ ∃ (n : ℕ), n ∈ image.{u_1, 0} (α := Finset G) Finset.card {t : Finset G | K ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V}

Tactic:
exact ⟨t.card, t, ht, rfl⟩
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K V : Set G
hK : IsCompact K
hV : (interior V).Nonempty
⊢ sInf (image.{u_1, 0} (α := Finset G) Finset.card {t : Finset G | K ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V}) ∈
    image.{u_1, 0} (α := Finset G) Finset.card {t : Finset G | K ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V}

Tactic:
have := Nat.sInf_mem (index_defined hK hV)
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
K V : Set G
hK : IsCompact K
hV : (interior V).Nonempty
this :
  sInf (image.{u_1, 0} (α := Finset G) Finset.card {t : Finset G | K ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V}) ∈
    image.{u_1, 0} (α := Finset G) Finset.card {t : Finset G | K ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V}
rwa rwa₁ rwa₂ rwa₃ :
  ∀
    (this :
      ∃ (x : Finset G),
        Membership.mem (γ := Set (Finset G)) {t : Finset G | K ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V} x ∧
          x.card =
            sInf
              (image.{u_1, 0} (α := Finset G) Finset.card {t : Finset G | K ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V})),
    ∃ (t : Finset G), K ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V ∧ t.card = index K V
⊢ ∃ (t : Finset G), K ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V ∧ t.card = index K V

Tactic:
rwa [mem_image] at this

Premises used: Set.mem_image
-- 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
K : Compacts G
V : Set G
hV : (interior V).Nonempty
obtain :
  ∀ (s : Finset G) (h1s : (↑K : Set G) ⊆ ⋃ g ∈ s, (fun (h : G) ↦ g * h) ⁻¹' (↑K₀ : Set G))
    (h2s : s.card = index (↑K : Set G) (↑K₀ : Set G)),
    index (↑K : Set G) V ≤ index (↑K : Set G) (↑K₀ : Set G) * index (↑K₀ : Set G) V
⊢ index (↑K : Set G) V ≤ index (↑K : Set G) (↑K₀ : Set G) * index (↑K₀ : Set G) V

Tactic:
obtain ⟨s, h1s, h2s⟩ := index_elim K.isCompact K₀.interior_nonempty

Premises used: MeasureTheory.Measure.haar.index_elim, TopologicalSpace.PositiveCompacts.interior_nonempty, TopologicalSpace.Compacts.isCompact
-- 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
K : Compacts G
V : Set G
hV : (interior V).Nonempty
s : Finset G
h1s : (↑K : Set G) ⊆ ⋃ g ∈ s, (fun (h : G) ↦ g * h) ⁻¹' (↑K₀ : Set G)
h2s : s.card = index (↑K : Set G) (↑K₀ : Set G)
obtain :
  ∀ (t : Finset G) (h1t : (↑K₀ : Set G) ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V) (h2t : t.card = index (↑K₀ : Set G) V),
    index (↑K : Set G) V ≤ index (↑K : Set G) (↑K₀ : Set G) * index (↑K₀ : Set G) V
⊢ index (↑K : Set G) V ≤ index (↑K : Set G) (↑K₀ : Set G) * index (↑K₀ : Set G) V

Tactic:
obtain ⟨t, h1t, h2t⟩ := index_elim K₀.isCompact hV

Premises used: MeasureTheory.Measure.haar.index_elim, TopologicalSpace.PositiveCompacts.isCompact
-- 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
K : Compacts G
V : Set G
hV : (interior V).Nonempty
s : Finset G
h1s : (↑K : Set G) ⊆ ⋃ g ∈ s, (fun (h : G) ↦ g * h) ⁻¹' (↑K₀ : Set G)
h2s : s.card = index (↑K : Set G) (↑K₀ : Set G)
t : Finset G
h1t : (↑K₀ : Set G) ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V
h2t : t.card = index (↑K₀ : Set G) V
rw : index (↑K : Set G) V ≤ t.card * s.card
⊢ index (↑K : Set G) V ≤ index (↑K : Set G) (↑K₀ : Set G) * index (↑K₀ : Set G) V

Tactic:
rw [← h2s, ← h2t, mul_comm]

Premises used: mul_comm
-- 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
K : Compacts G
V : Set G
hV : (interior V).Nonempty
s : Finset G
h1s : (↑K : Set G) ⊆ ⋃ g ∈ s, (fun (h : G) ↦ g * h) ⁻¹' (↑K₀ : Set G)
h2s : s.card = index (↑K : Set G) (↑K₀ : Set G)
t : Finset G
h1t : (↑K₀ : Set G) ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V
h2t : t.card = index (↑K₀ : Set G) V
⊢ index (↑K : Set G) V ≤ t.card * s.card

Tactic:
le_trans ?_ Finset.card_mul_le

Premises used: Finset.card_mul_le, le_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
K : Compacts G
V : Set G
hV : (interior V).Nonempty
s : Finset G
h1s : (↑K : Set G) ⊆ ⋃ g ∈ s, (fun (h : G) ↦ g * h) ⁻¹' (↑K₀ : Set G)
h2s : s.card = index (↑K : Set G) (↑K₀ : Set G)
t : Finset G
h1t : (↑K₀ : Set G) ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V
h2t : t.card = index (↑K₀ : Set G) V
refine : index (↑K : Set G) V ≤ (t * s).card
⊢ index (↑K : Set G) V ≤ t.card * s.card

Tactic:
refine le_trans ?_ Finset.card_mul_le

Premises used: Finset.card_mul_le, le_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
K : Compacts G
V : Set G
hV : (interior V).Nonempty
s : Finset G
h1s : (↑K : Set G) ⊆ ⋃ g ∈ s, (fun (h : G) ↦ g * h) ⁻¹' (↑K₀ : Set G)
h2s : s.card = index (↑K : Set G) (↑K₀ : Set G)
t : Finset G
h1t : (↑K₀ : Set G) ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V
h2t : t.card = index (↑K₀ : Set G) V
hm :
  (t * s).card ∈
    image.{u_1, 0} (α := Finset G) Finset.card {t : Finset G | (↑K : Set G) ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V}
⊢ index (↑K : Set G) V ≤ (t * 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₀ : PositiveCompacts G
K : Compacts G
V : Set G
hV : (interior V).Nonempty
s : Finset G
h1s : (↑K : Set G) ⊆ ⋃ g ∈ s, (fun (h : G) ↦ g * h) ⁻¹' (↑K₀ : Set G)
h2s : s.card = index (↑K : Set G) (↑K₀ : Set G)
t : Finset G
h1t : (↑K₀ : Set G) ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V
h2t : t.card = index (↑K₀ : Set G) V
⊢ (t * s).card ∈
    image.{u_1, 0} (α := Finset G) Finset.card {t : Finset G | (↑K : Set G) ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V}

Tactic:
⟨_, ?_, rfl⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, Set.image, rfl
-- 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
K : Compacts G
V : Set G
hV : (interior V).Nonempty
s : Finset G
h1s : (↑K : Set G) ⊆ ⋃ g ∈ s, (fun (h : G) ↦ g * h) ⁻¹' (↑K₀ : Set G)
h2s : s.card = index (↑K : Set G) (↑K₀ : Set G)
t : Finset G
h1t : (↑K₀ : Set G) ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V
h2t : t.card = index (↑K₀ : Set G) V
hm : Membership.mem (γ := Set (Finset G)) {t : Finset G | (↑K : Set G) ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V} (t * s)
⊢ (t * s).card ∈
    image.{u_1, 0} (α := Finset G) Finset.card {t : Finset G | (↑K : Set G) ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V}

Tactic:
refine ⟨_, ?_, rfl⟩
-- 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
K : Compacts G
V : Set G
hV : (interior V).Nonempty
s : Finset G
h1s : (↑K : Set G) ⊆ ⋃ g ∈ s, (fun (h : G) ↦ g * h) ⁻¹' (↑K₀ : Set G)
h2s : s.card = index (↑K : Set G) (↑K₀ : Set G)
t : Finset G
h1t : (↑K₀ : Set G) ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V
h2t : t.card = index (↑K₀ : Set G) V
⊢ (↑K : Set G) ⊆ ⋃ g ∈ t * s, (fun (h : G) ↦ g * h) ⁻¹' V

Tactic:
Subset.trans h1s ?_

Premises used: Set.Subset.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
K : Compacts G
V : Set G
hV : (interior V).Nonempty
s : Finset G
h1s : (↑K : Set G) ⊆ ⋃ g ∈ s, (fun (h : G) ↦ g * h) ⁻¹' (↑K₀ : Set G)
h2s : s.card = index (↑K : Set G) (↑K₀ : Set G)
t : Finset G
h1t : (↑K₀ : Set G) ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V
h2t : t.card = index (↑K₀ : Set G) V
hm :
  Subset.{u_1} (α := Set G) (⋃ g ∈ s, (fun (h : G) ↦ g * h) ⁻¹' (↑K₀ : Set G))
    (⋃ g ∈ t * s, (fun (h : G) ↦ g * h) ⁻¹' V)
⊢ (↑K : Set G) ⊆ ⋃ g ∈ t * s, (fun (h : G) ↦ g * h) ⁻¹' V

Tactic:
refine Subset.trans h1s ?_

Premises used: Set.Subset.trans