awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.GiryMonad (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
m : Measure α
f : α → Measure β
s : Set β
hs : MeasurableSet s
hf : AEMeasurable f m
rw : (join (map f m) : (a : Set β) → ℝ≥0∞) s = ∫⁻ (a : α), (f a : (a : Set β) → ℝ≥0∞) s ∂m
rw₁ : ∫⁻ (μ : Measure β), (μ : (a : Set β) → ℝ≥0∞) s ∂map f m = ∫⁻ (a : α), (f a : (a : Set β) → ℝ≥0∞) s ∂m
⊢ (m.bind f : (a : Set β) → ℝ≥0∞) s = ∫⁻ (a : α), (f a : (a : Set β) → ℝ≥0∞) s ∂m
have rw₂ : ∫⁻ (a : α), (f a : (a : Set β) → ℝ≥0∞) s ∂m = ∫⁻ (a : α), (f a : (a : Set β) → ℝ≥0∞) s ∂m
Tactic: rw [bind, join_apply hs, lintegral_map' (measurable_coe hs).aemeasurable hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.GiryMonad (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
m : Measure α
f : α → Measure β
s : Set β
hs : MeasurableSet s
⊢ (m.bind f : (a : Set β) → ℝ≥0∞) s ≤ ∫⁻ (a : α), (f a : (a : Set β) → ℝ≥0∞) s ∂m
have rw : ∫⁻ (μ : Measure β), (μ : (a : Set β) → ℝ≥0∞) s ∂map f m ≤ ∫⁻ (a : α), (f a : (a : Set β) → ℝ≥0∞) s ∂m
Tactic: rw [bind, join_apply hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.GiryMonad (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
ι : Type u_3
m : ι → Measure α
f : α → Measure β
h : AEMeasurable (_m := mα) f (sum fun (i : ι) ↦ m i)
⊢ bind (mα := mα) (sum fun (i : ι) ↦ m i) f = sum fun (i : ι) ↦ (m i).bind f
have simp_rw : join (map f (sum fun (i : ι) ↦ m i)) = sum fun (i : ι) ↦ join (map f (m i))
Tactic: simp_rw [bind, map_sum h, join_sum]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.GiryMonad (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
ι : Type u_3
m : ι → Measure α
f : α → Measure β
h : AEMeasurable (_m := mα) f (sum fun (i : ι) ↦ m i)
simp_rw : join (map f (sum fun (i : ι) ↦ m i)) = sum fun (i : ι) ↦ join (map f (m i))
⊢ bind (mα := mα) (sum fun (i : ι) ↦ m i) f = sum fun (i : ι) ↦ (m i).bind f
have simp_rw₁ : Eq.{u_2 + 1} (α := Measure β) (join (sum fun (i : ι) ↦ map f (m i))) (sum fun (i : ι) ↦ join (map f (m i)))
Tactic: simp_rw [bind, map_sum h, join_sum]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.GiryMonad (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
R : Type u_3
inst : SMul R ℝ≥0∞
inst_1 : IsScalarTower R ℝ≥0∞ ℝ≥0∞
c : R
m : Measure α
f : α → Measure β
⊢ (c • m).bind f = c • m.bind f
have simp_rw : join (map f (c • m)) = c • join (map f m)
Tactic: simp_rw [bind, Measure.map_smul, join_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.GiryMonad (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
R : Type u_3
inst : SMul R ℝ≥0∞
inst_1 : IsScalarTower R ℝ≥0∞ ℝ≥0∞
c : R
m : Measure α
f : α → Measure β
simp_rw : join (map f (c • m)) = c • join (map f m)
⊢ (c • m).bind f = c • m.bind f
have simp_rw₁ : (HSMul.hSMul (β := Measure (Measure β)) c (map f m)).join = c • join (map f m)
Tactic: simp_rw [bind, Measure.map_smul, join_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.GiryMonad (goal)
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)
⊢ (m.bind f).bind g = m.bind fun (a : α) ↦ (f a).bind g
have 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∞)
Tactic: ext1 s hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.GiryMonad (goal)
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
⊢ 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∞)
have h : ∫⁻ (a : α), ∫⁻ (x : β), (g x : (a : Set γ) → ℝ≥0∞) s ∂f a ∂m = ∫⁻ (a : α), ((f a).bind g : (a : Set γ) → ℝ≥0∞) s ∂m
Tactic: rw [bind_apply hs hg, lintegral_bind hf, bind_apply hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.GiryMonad (goal)
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
⊢ 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∞)
have h₁ : AEMeasurable.{u_1, u_3} (β := Measure γ) (fun (a : α) ↦ (f a).bind g) m
Tactic: rw [bind_apply hs hg, lintegral_bind hf, bind_apply hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.GiryMonad (goal)
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
⊢ 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∞)
have h₂ : AEMeasurable (β := ℝ≥0∞) (fun (a : β) ↦ (g a : (a : Set γ) → ℝ≥0∞) s) (m.bind f)
Tactic: rw [bind_apply hs hg, lintegral_bind hf, bind_apply hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.GiryMonad (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
m : Measure α
⊢ m.bind dirac = m
have h : ∀ (s : Set α) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) (((m.bind dirac : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext1 s hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.GiryMonad (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
m : Measure α
f : α → β
hf : Measurable f
⊢ Eq (α := Measure β) (m.bind fun (x : α) ↦ dirac (f x)) (map f m)
have hg : Measurable.{u_2, u_2} (α := β) (β := Measure β) dirac
Tactic: rw [← bind_dirac (m := m.map f), bind, bind, map_map, Function.comp_def]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.GiryMonad (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure (Measure α)
⊢ μ.join = μ.bind id
have rw : μ.join = join (map id μ)
Tactic: rw [bind, map_id]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.GiryMonad (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure (Measure α)
rw : μ.join = join (map id μ)
⊢ μ.join = μ.bind id
have rw₁ : μ.join = μ.join
Tactic: rw [bind, map_id]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.GiryMonad (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Measurable f
μ : Measure (Measure α)
⊢ Eq (α := Measure β) (join (map (map f) μ)) (map f μ.join)
have 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∞)
Tactic: ext1 s hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.GiryMonad (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Measurable f
μ : Measure (Measure α)
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∞)
have h : ∫⁻ (a : Measure α), ((map f a : Measure β) : (a : Set β) → ℝ≥0∞) s ∂μ =
  ∫⁻ (μ : Measure α), (μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) ∂μ
Tactic: rw [join_apply hs, map_apply hf hs, join_apply (hf hs),
    lintegral_map (measurable_coe hs) (measurable_map f hf)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.GiryMonad (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure (Measure (Measure α))
⊢ μ.bind join = μ.join.join
have rw : μ.bind join = μ.bind fun (a : Measure (Measure α)) ↦ (id a).bind id
Tactic: rw [join_eq_bind, join_eq_bind, bind_bind aemeasurable_id aemeasurable_id]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.GiryMonad (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure (Measure (Measure α))
⊢ μ.bind join = μ.bind fun (a : Measure (Measure α)) ↦ (id a).bind id
have apply : Eq.{u_1 + 1} (α := Measure (Measure α) → Measure α) join fun (a : Measure (Measure α)) ↦ (id a).bind id
Tactic: apply congr_arg (bind μ)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.GiryMonad (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure (Measure (Measure α))
⊢ Eq.{u_1 + 1} (α := Measure (Measure α) → Measure α) join fun (a : Measure (Measure α)) ↦ (id a).bind id
have h : ∀ (ν : Measure (Measure α)), ν.join = (id ν).bind id
Tactic: funext ν
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
K₀ : PositiveCompacts G
U : Set G
⊢ prehaar (↑K₀ : Set G) U ⊥ = 0
have rw : HDiv.hDiv (α := ℝ) (↑(index (↑⊥ : Set G) U) : ℝ) (↑(index (↑K₀ : Set G) U) : ℝ) = 0
Tactic: rw [prehaar, Compacts.coe_bot, index_empty, Nat.cast_zero, zero_div]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (goal)
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
⊢ prehaar (↑K₀ : Set G) U ⊥ = 0
have rw₁ : HDiv.hDiv (α := ℝ) (↑(index ∅ U) : ℝ) (↑(index (↑K₀ : Set G) U) : ℝ) = 0
Tactic: rw [prehaar, Compacts.coe_bot, index_empty, Nat.cast_zero, zero_div]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (goal)
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
⊢ prehaar (↑K₀ : Set G) U ⊥ = 0
have rw₂ : HDiv.hDiv (α := ℝ) (↑0 : ℝ) (↑(index (↑K₀ : Set G) U) : ℝ) = 0
Tactic: rw [prehaar, Compacts.coe_bot, index_empty, Nat.cast_zero, zero_div]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (goal)
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
⊢ prehaar (↑K₀ : Set G) U ⊥ = 0
have rw₃ : HDiv.hDiv (α := ℝ) 0 (↑(index (↑K₀ : Set G) U) : ℝ) = 0
Tactic: rw [prehaar, Compacts.coe_bot, index_empty, Nat.cast_zero, zero_div]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (goal)
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
⊢ prehaar (↑K₀ : Set G) U ⊥ = 0
have rw₄ : Eq (α := ℝ) 0 0
Tactic: rw [prehaar, Compacts.coe_bot, index_empty, Nat.cast_zero, zero_div]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
K₀ : PositiveCompacts G
U : Set G
K : Compacts G
⊢ 0 ≤ prehaar (↑K₀ : Set G) U K
have ha : LE.le (α := ℝ) 0 (↑(index (↑K : Set G) U) : ℝ)
Tactic: apply div_nonneg
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (goal)
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) : ℝ)
⊢ 0 ≤ prehaar (↑K₀ : Set G) U K
have hb : LE.le (α := ℝ) 0 (↑(index (↑K₀ : Set G) U) : ℝ)
Tactic: apply div_nonneg
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
K₀ : PositiveCompacts G
U : Set G
K : Compacts G
⊢ LE.le (α := ℝ) 0 (↑(index (↑K : Set G) U) : ℝ)
have ha : 0 ≤ index (↑K : Set G) U
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
K₀ : PositiveCompacts G
U : Set G
K : Compacts G
⊢ LE.le (α := ℝ) 0 (↑(index (↑K₀ : Set G) U) : ℝ)
have hb : 0 ≤ index (↑K₀ : Set G) U
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (goal)
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
⊢ ∃ (n : ℕ), n ∈ image.{u_1, 0} (α := Finset G) Finset.card {t : Finset G | K ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V}
have 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}
Tactic: rcases compact_covered_by_mul_left_translates hK hV with ⟨t, ht⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (hypothesis)
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), K ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V ∧ t.card = index K V
have 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}
Tactic: have := Nat.sInf_mem (index_defined hK hV)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (goal)
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}
⊢ ∃ (t : Finset G), K ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V ∧ t.card = index K V
have 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
Tactic: rwa [mem_image] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (goal)
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
⊢ index (↑K : Set G) V ≤ index (↑K : Set G) (↑K₀ : Set G) * index (↑K₀ : Set G) V
have 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
Tactic: obtain ⟨s, h1s, h2s⟩ := index_elim K.isCompact K₀.interior_nonempty
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (goal)
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)
⊢ index (↑K : Set G) V ≤ index (↑K : Set G) (↑K₀ : Set G) * index (↑K₀ : Set G) V
have 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
Tactic: obtain ⟨t, h1t, h2t⟩ := index_elim K₀.isCompact hV
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (goal)
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 ≤ index (↑K : Set G) (↑K₀ : Set G) * index (↑K₀ : Set G) V
have rw : index (↑K : Set G) V ≤ t.card * s.card
Tactic: rw [← h2s, ← h2t, mul_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (goal)
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
have refine : index (↑K : Set G) V ≤ (t * s).card
Tactic: refine le_trans ?_ Finset.card_mul_le
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (goal)
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 * s).card
have 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}
Tactic: apply Nat.sInf_le
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (goal)
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}
have hm : Membership.mem (γ := Set (Finset G)) {t : Finset G | (↑K : Set G) ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V} (t * s)
Tactic: refine ⟨_, ?_, rfl⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (goal)
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
have 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)
Tactic: refine Subset.trans h1s ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (goal)
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
⊢ Subset.{u_1} (α := Set G) (⋃ g ∈ s, (fun (h : G) ↦ g * h) ⁻¹' (↑K₀ : Set G))
    (⋃ g ∈ t * s, (fun (h : G) ↦ g * h) ⁻¹' V)
have hm : ∀ (i : G) (j : i ∈ s),
  Subset (α := Set G) ((fun (h : G) ↦ i * h) ⁻¹' (↑K₀ : Set G)) (⋃ g ∈ t * s, (fun (h : G) ↦ g * h) ⁻¹' V)
Tactic: apply iUnion₂_subset
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (goal)
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
g₁ : G
hg₁ : g₁ ∈ s
⊢ Subset (α := Set G) ((fun (h : G) ↦ g₁ * h) ⁻¹' (↑K₀ : Set G)) (⋃ g ∈ t * s, (fun (h : G) ↦ g * h) ⁻¹' V)
have hm : ∀ (a : G), g₁ * a ∈ (↑K₀ : Set G) → Membership.mem (γ := Set G) (⋃ g ∈ t * s, (fun (h : G) ↦ g * h) ⁻¹' V) a
Tactic: rw [preimage_subset_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (hypothesis)
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
g₁ : G
hg₁ : g₁ ∈ s
g₂ : G
hg₂ : g₁ * g₂ ∈ (↑K₀ : Set G)
⊢ Membership.mem (γ := Set G) (⋃ g ∈ t * s, (fun (h : G) ↦ g * h) ⁻¹' V) g₂
have this : Membership.mem (γ := Set G) (⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V) (g₁ * g₂)
Tactic: have := h1t hg₂
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (goal)
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
g₁ : G
hg₁ : g₁ ∈ s
g₂ : G
hg₂ : g₁ * g₂ ∈ (↑K₀ : Set G)
this : Membership.mem (γ := Set G) (⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' V) (g₁ * g₂)
⊢ Membership.mem (γ := Set G) (⋃ g ∈ t * s, (fun (h : G) ↦ g * h) ⁻¹' V) g₂
have hm : ∀ (g₃ : G) (hg₃ : g₃ ∈ t)
  (h2V : Membership.mem (γ := Set G) ((fun (h : g₃ ∈ t) ↦ ((fun (h : G) ↦ g₃ * h) ⁻¹' V : Set G)) hg₃) (g₁ * g₂)),
  Membership.mem (γ := Set G) (⋃ g ∈ t * s, (fun (h : G) ↦ g * h) ⁻¹' V) g₂
Tactic: rcases this with ⟨_, ⟨g₃, rfl⟩, A, ⟨hg₃, rfl⟩, h2V⟩
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (hypothesis)
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
g₁ : G
hg₁ : g₁ ∈ s
g₂ : G
hg₂ : g₁ * g₂ ∈ (↑K₀ : Set G)
g₃ : G
hg₃ : g₃ ∈ t
h2V : Membership.mem (γ := Set G) ((fun (h : g₃ ∈ t) ↦ ((fun (h : G) ↦ g₃ * h) ⁻¹' V : Set G)) hg₃) (g₁ * g₂)
⊢ Membership.mem (γ := Set G) (⋃ g ∈ t * s, (fun (h : G) ↦ g * h) ⁻¹' V) g₂
have h2V₁ : g₃ * g₁ * g₂ ∈ V
Tactic: rw [mem_preimage, ← mul_assoc] at h2V
Cleared hypotheses: h2V