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₀ : PositiveCompacts G
K₁ K₂ : Compacts G
h : Disjoint K₁.carrier K₂.carrier
h₂ : IsClosed[inst_1] K₂.carrier
U₁ U₂ : Set G
h1U₁ : IsOpen[inst_1] U₁
h1U₂ : IsOpen[inst_1] U₂
h2U₁ : K₁.carrier ⊆ U₁
h2U₂ : K₂.carrier ⊆ U₂
hU : Disjoint U₁ U₂
L₁ : Set G
h1L₁ : Membership.mem (γ := Filter G) (𝓝 1) L₁
V₁ : Set G
h1V₁ : V₁ ⊆ L₁
h2V₁ : IsOpen[inst_1] V₁
h3V₁ : 1 ∈ V₁
h2L₁ : K₁.carrier * V₁ ⊆ U₁
L₂ : Set G
h1L₂ : Membership.mem (γ := Filter G) (𝓝 1) L₂
h2L₂ : K₂.carrier * L₂ ⊆ U₂
rcases :
  ∀ (V₂ : Set G) (h1V₂ : V₂ ⊆ L₂) (h2V₂ : IsOpen[inst_1] V₂) (h3V₂ : 1 ∈ V₂),
    chaar K₀ (K₁ ⊔ K₂) = chaar K₀ K₁ + chaar K₀ K₂
⊢ chaar K₀ (K₁ ⊔ K₂) = chaar K₀ K₁ + chaar K₀ K₂

Tactic:
rcases mem_nhds_iff.mp h1L₂ with ⟨V₂, h1V₂, h2V₂, h3V₂⟩

Premises used: mem_nhds_iff, Iff.mp
-- 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₁ K₂ : Compacts G
h : Disjoint K₁.carrier K₂.carrier
h₂ : IsClosed[inst_1] K₂.carrier
U₁ U₂ : Set G
h1U₁ : IsOpen[inst_1] U₁
h1U₂ : IsOpen[inst_1] U₂
h2U₁ : K₁.carrier ⊆ U₁
h2U₂ : K₂.carrier ⊆ U₂
hU : Disjoint U₁ U₂
L₁ : Set G
h1L₁ : Membership.mem (γ := Filter G) (𝓝 1) L₁
V₁ : Set G
h1V₁ : V₁ ⊆ L₁
h2V₁ : IsOpen[inst_1] V₁
h3V₁ : 1 ∈ V₁
h2L₁ : K₁.carrier * V₁ ⊆ U₁
L₂ : Set G
h1L₂ : Membership.mem (γ := Filter G) (𝓝 1) L₂
h2L₂ : K₂.carrier * L₂ ⊆ U₂
V₂ : Set G
h1V₂ : V₂ ⊆ L₂
h2V₂ : IsOpen[inst_1] V₂
h3V₂ : 1 ∈ V₂
⊢ K₂.carrier * V₂ ⊆ U₂

Tactic:
replace h2L₂ := Subset.trans (mul_subset_mul_left h1V₂) h2L₂
-- 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₁ K₂ : Compacts G
h : Disjoint K₁.carrier K₂.carrier
h₂ : IsClosed[inst_1] K₂.carrier
U₁ U₂ : Set G
h1U₁ : IsOpen[inst_1] U₁
h1U₂ : IsOpen[inst_1] U₂
h2U₁ : K₁.carrier ⊆ U₁
h2U₂ : K₂.carrier ⊆ U₂
hU : Disjoint U₁ U₂
L₁ : Set G
h1L₁ : Membership.mem (γ := Filter G) (𝓝 1) L₁
V₁ : Set G
h1V₁ : V₁ ⊆ L₁
h2V₁ : IsOpen[inst_1] V₁
h3V₁ : 1 ∈ V₁
h2L₁ : K₁.carrier * V₁ ⊆ U₁
L₂ : Set G
h1L₂ : Membership.mem (γ := Filter G) (𝓝 1) L₂
V₂ : Set G
h1V₂ : V₂ ⊆ L₂
h2V₂ : IsOpen[inst_1] V₂
h3V₂ : 1 ∈ V₂
h2L₂ : K₂.carrier * V₂ ⊆ U₂
eval : (Compacts G → ℝ) → ℝ := fun (f : Compacts G → ℝ) ↦ f K₁ + f K₂ - f (K₁ ⊔ K₂)
⊢ Continuous eval

Tactic:
have : Continuous eval :=
    ((continuous_apply K₁).add (continuous_apply K₂)).sub (continuous_apply (K₁ ⊔ K₂))
-- 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₁ K₂ : Compacts G
h : Disjoint K₁.carrier K₂.carrier
h₂ : IsClosed[inst_1] K₂.carrier
U₁ U₂ : Set G
h1U₁ : IsOpen[inst_1] U₁
h1U₂ : IsOpen[inst_1] U₂
h2U₁ : K₁.carrier ⊆ U₁
h2U₂ : K₂.carrier ⊆ U₂
hU : Disjoint U₁ U₂
L₁ : Set G
h1L₁ : Membership.mem (γ := Filter G) (𝓝 1) L₁
V₁ : Set G
h1V₁ : V₁ ⊆ L₁
h2V₁ : IsOpen[inst_1] V₁
h3V₁ : 1 ∈ V₁
h2L₁ : K₁.carrier * V₁ ⊆ U₁
L₂ : Set G
h1L₂ : Membership.mem (γ := Filter G) (𝓝 1) L₂
V₂ : Set G
h1V₂ : V₂ ⊆ L₂
h2V₂ : IsOpen[inst_1] V₂
h3V₂ : 1 ∈ V₂
h2L₂ : K₂.carrier * V₂ ⊆ U₂
eval : (Compacts G → ℝ) → ℝ := fun (f : Compacts G → ℝ) ↦ f K₁ + f K₂ - f (K₁ ⊔ K₂)
this : Continuous eval
rw : chaar K₀ K₁ + chaar K₀ K₂ - chaar K₀ (K₁ ⊔ K₂) = 0
⊢ chaar K₀ (K₁ ⊔ K₂) = chaar K₀ K₁ + chaar K₀ K₂

Tactic:
rw [eq_comm, ← sub_eq_zero]

Premises used: sub_eq_zero, eq_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₁ K₂ : Compacts G
h : Disjoint K₁.carrier K₂.carrier
h₂ : IsClosed[inst_1] K₂.carrier
U₁ U₂ : Set G
h1U₁ : IsOpen[inst_1] U₁
h1U₂ : IsOpen[inst_1] U₂
h2U₁ : K₁.carrier ⊆ U₁
h2U₂ : K₂.carrier ⊆ U₂
hU : Disjoint U₁ U₂
L₁ : Set G
h1L₁ : Membership.mem (γ := Filter G) (𝓝 1) L₁
V₁ : Set G
h1V₁ : V₁ ⊆ L₁
h2V₁ : IsOpen[inst_1] V₁
h3V₁ : 1 ∈ V₁
h2L₁ : K₁.carrier * V₁ ⊆ U₁
L₂ : Set G
h1L₂ : Membership.mem (γ := Filter G) (𝓝 1) L₂
V₂ : Set G
h1V₂ : V₂ ⊆ L₂
h2V₂ : IsOpen[inst_1] V₂
h3V₂ : 1 ∈ V₂
h2L₂ : K₂.carrier * V₂ ⊆ U₂
eval : (Compacts G → ℝ) → ℝ := fun (f : Compacts G → ℝ) ↦ f K₁ + f K₂ - f (K₁ ⊔ K₂)
this : Continuous eval
change : chaar K₀ ∈ eval ⁻¹' {0}
⊢ chaar K₀ K₁ + chaar K₀ K₂ - chaar K₀ (K₁ ⊔ K₂) = 0

Tactic:
change chaar K₀ ∈ eval ⁻¹' {(0 : ℝ)}

Premises used: MeasureTheory.Measure.haar.chaar, OfNat.ofNat
-- 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₁ K₂ : Compacts G
h : Disjoint K₁.carrier K₂.carrier
h₂ : IsClosed[inst_1] K₂.carrier
U₁ U₂ : Set G
h1U₁ : IsOpen[inst_1] U₁
h1U₂ : IsOpen[inst_1] U₂
h2U₁ : K₁.carrier ⊆ U₁
h2U₂ : K₂.carrier ⊆ U₂
hU : Disjoint U₁ U₂
L₁ : Set G
h1L₁ : Membership.mem (γ := Filter G) (𝓝 1) L₁
V₁ : Set G
h1V₁ : V₁ ⊆ L₁
h2V₁ : IsOpen[inst_1] V₁
h3V₁ : 1 ∈ V₁
h2L₁ : K₁.carrier * V₁ ⊆ U₁
L₂ : Set G
h1L₂ : Membership.mem (γ := Filter G) (𝓝 1) L₂
V₂ : Set G
h1V₂ : V₂ ⊆ L₂
h2V₂ : IsOpen[inst_1] V₂
h3V₂ : 1 ∈ V₂
h2L₂ : K₂.carrier * V₂ ⊆ U₂
eval : (Compacts G → ℝ) → ℝ := fun (f : Compacts G → ℝ) ↦ f K₁ + f K₂ - f (K₁ ⊔ K₂)
this : Continuous eval
V : Set G := V₁ ∩ V₂
⊢ 1 ∈ { carrier := V⁻¹, is_open' := ⋯ : Opens G }.carrier

Tactic:
simp only [V, mem_inv, inv_one, h3V₁, h3V₂, mem_inter_iff, true_and]

Premises used: inv_one, Set.mem_inter_iff, true_and, Set.mem_inv
-- 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₁ K₂ : Compacts G
h : Disjoint K₁.carrier K₂.carrier
h₂ : IsClosed[inst_1] K₂.carrier
U₁ U₂ : Set G
h1U₁ : IsOpen[inst_1] U₁
h1U₂ : IsOpen[inst_1] U₂
h2U₁ : K₁.carrier ⊆ U₁
h2U₂ : K₂.carrier ⊆ U₂
hU : Disjoint U₁ U₂
L₁ : Set G
h1L₁ : Membership.mem (γ := Filter G) (𝓝 1) L₁
V₁ : Set G
h1V₁ : V₁ ⊆ L₁
h2V₁ : IsOpen[inst_1] V₁
h3V₁ : 1 ∈ V₁
h2L₁ : K₁.carrier * V₁ ⊆ U₁
L₂ : Set G
h1L₂ : Membership.mem (γ := Filter G) (𝓝 1) L₂
V₂ : Set G
h1V₂ : V₂ ⊆ L₂
h2V₂ : IsOpen[inst_1] V₂
h3V₂ : 1 ∈ V₂
h2L₂ : K₂.carrier * V₂ ⊆ U₂
eval : (Compacts G → ℝ) → ℝ := fun (f : Compacts G → ℝ) ↦ f K₁ + f K₂ - f (K₁ ⊔ K₂)
this : Continuous eval
V : Set G := V₁ ∩ V₂
mem_of_subset_of_mem :
  clPrehaar (↑K₀ : Set G) { carrier := V⁻¹, is_open' := ⋯, mem' := ⋯ : OpenNhdsOf (α := G) 1 } ⊆ eval ⁻¹' {0}
⊢ chaar K₀ ∈ eval ⁻¹' {0}

Tactic:
apply
    mem_of_subset_of_mem _
      (chaar_mem_clPrehaar K₀
        ⟨⟨V⁻¹, (h2V₁.inter h2V₂).preimage continuous_inv⟩, by
          simp only [V, mem_inv, inv_one, h3V₁, h3V₂, mem_inter_iff, true_and]⟩)

Premises used: Set.mem_of_subset_of_mem, TopologicalSpace.OpenNhdsOf.mk, Inv.inv, TopologicalSpace.Opens.mk, IsOpen.inter, IsOpen.preimage, ContinuousInv.continuous_inv, MeasureTheory.Measure.haar.chaar_mem_clPrehaar
-- 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₁ K₂ : Compacts G
h : Disjoint K₁.carrier K₂.carrier
h₂ : IsClosed[inst_1] K₂.carrier
U₁ U₂ : Set G
h1U₁ : IsOpen[inst_1] U₁
h1U₂ : IsOpen[inst_1] U₂
h2U₁ : K₁.carrier ⊆ U₁
h2U₂ : K₂.carrier ⊆ U₂
hU : Disjoint U₁ U₂
L₁ : Set G
h1L₁ : Membership.mem (γ := Filter G) (𝓝 1) L₁
V₁ : Set G
h1V₁ : V₁ ⊆ L₁
h2V₁ : IsOpen[inst_1] V₁
h3V₁ : 1 ∈ V₁
h2L₁ : K₁.carrier * V₁ ⊆ U₁
L₂ : Set G
h1L₂ : Membership.mem (γ := Filter G) (𝓝 1) L₂
V₂ : Set G
h1V₂ : V₂ ⊆ L₂
h2V₂ : IsOpen[inst_1] V₂
h3V₂ : 1 ∈ V₂
h2L₂ : K₂.carrier * V₂ ⊆ U₂
eval : (Compacts G → ℝ) → ℝ := fun (f : Compacts G → ℝ) ↦ f K₁ + f K₂ - f (K₁ ⊔ K₂)
this : Continuous eval
V : Set G := V₁ ∩ V₂
rw :
  prehaar (↑K₀ : Set G) ''
      {U : Set G |
        U ⊆ (↑{ carrier := V⁻¹, is_open' := ⋯, mem' := ⋯ : OpenNhdsOf (α := G) 1 }.toOpens : Set G) ∧
          IsOpen[inst_1] U ∧ 1 ∈ U} ⊆
    eval ⁻¹' {0}
rw₁ : IsClosed (eval ⁻¹' {0})
⊢ closure
      (prehaar (↑K₀ : Set G) ''
        {U : Set G |
          U ⊆ (↑{ carrier := V⁻¹, is_open' := ⋯, mem' := ⋯ : OpenNhdsOf (α := G) 1 }.toOpens : Set G) ∧
            IsOpen[inst_1] U ∧ 1 ∈ U}) ⊆
    eval ⁻¹' {0}

Tactic:
rw [IsClosed.closure_subset_iff]

Premises used: IsClosed.closure_subset_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
K₁ K₂ : Compacts G
h : Disjoint K₁.carrier K₂.carrier
h₂ : IsClosed[inst_1] K₂.carrier
U₁ U₂ : Set G
h1U₁ : IsOpen[inst_1] U₁
h1U₂ : IsOpen[inst_1] U₂
h2U₁ : K₁.carrier ⊆ U₁
h2U₂ : K₂.carrier ⊆ U₂
hU : Disjoint U₁ U₂
L₁ : Set G
h1L₁ : Membership.mem (γ := Filter G) (𝓝 1) L₁
V₁ : Set G
h1V₁ : V₁ ⊆ L₁
h2V₁ : IsOpen[inst_1] V₁
h3V₁ : 1 ∈ V₁
h2L₁ : K₁.carrier * V₁ ⊆ U₁
L₂ : Set G
h1L₂ : Membership.mem (γ := Filter G) (𝓝 1) L₂
V₂ : Set G
h1V₂ : V₂ ⊆ L₂
h2V₂ : IsOpen[inst_1] V₂
h3V₂ : 1 ∈ V₂
h2L₂ : K₂.carrier * V₂ ⊆ U₂
eval : (Compacts G → ℝ) → ℝ := fun (f : Compacts G → ℝ) ↦ f K₁ + f K₂ - f (K₁ ⊔ K₂)
this : Continuous eval
V : Set G := V₁ ∩ V₂
U : Set G
h1U : U ⊆ (↑{ carrier := V⁻¹, is_open' := ⋯, mem' := ⋯ : OpenNhdsOf (α := G) 1 }.toOpens : Set G)
h2U : IsOpen[inst_1] U
h3U : 1 ∈ U
simp : prehaar (↑K₀ : Set G) U K₁ + prehaar (↑K₀ : Set G) U K₂ = prehaar (↑K₀ : Set G) U (K₁ ⊔ K₂)
⊢ prehaar (↑K₀ : Set G) U ∈ eval ⁻¹' {0}

Tactic:
simp only [eval, mem_preimage, sub_eq_zero, mem_singleton_iff]

Premises used: sub_eq_zero, Set.mem_singleton_iff, 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₀ : PositiveCompacts G
K₁ K₂ : Compacts G
h : Disjoint K₁.carrier K₂.carrier
h₂ : IsClosed[inst_1] K₂.carrier
U₁ U₂ : Set G
h1U₁ : IsOpen[inst_1] U₁
h1U₂ : IsOpen[inst_1] U₂
h2U₁ : K₁.carrier ⊆ U₁
h2U₂ : K₂.carrier ⊆ U₂
hU : Disjoint U₁ U₂
L₁ : Set G
h1L₁ : Membership.mem (γ := Filter G) (𝓝 1) L₁
V₁ : Set G
h1V₁ : V₁ ⊆ L₁
h2V₁ : IsOpen[inst_1] V₁
h3V₁ : 1 ∈ V₁
h2L₁ : K₁.carrier * V₁ ⊆ U₁
L₂ : Set G
h1L₂ : Membership.mem (γ := Filter G) (𝓝 1) L₂
V₂ : Set G
h1V₂ : V₂ ⊆ L₂
h2V₂ : IsOpen[inst_1] V₂
h3V₂ : 1 ∈ V₂
h2L₂ : K₂.carrier * V₂ ⊆ U₂
eval : (Compacts G → ℝ) → ℝ := fun (f : Compacts G → ℝ) ↦ f K₁ + f K₂ - f (K₁ ⊔ K₂)
this : Continuous eval
V : Set G := V₁ ∩ V₂
U : Set G
h1U : U ⊆ (↑{ carrier := V⁻¹, is_open' := ⋯, mem' := ⋯ : OpenNhdsOf (α := G) 1 }.toOpens : Set G)
h2U : IsOpen[inst_1] U
h3U : 1 ∈ U
rw : prehaar (↑K₀ : Set G) U (K₁ ⊔ K₂) = prehaar (↑K₀ : Set G) U K₁ + prehaar (↑K₀ : Set G) U K₂
⊢ prehaar (↑K₀ : Set G) U K₁ + prehaar (↑K₀ : Set G) U K₂ = prehaar (↑K₀ : Set G) U (K₁ ⊔ K₂)

Tactic:
rw [eq_comm]

Premises used: eq_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₁ K₂ : Compacts G
h : Disjoint K₁.carrier K₂.carrier
h₂ : IsClosed[inst_1] K₂.carrier
U₁ U₂ : Set G
h1U₁ : IsOpen[inst_1] U₁
h1U₂ : IsOpen[inst_1] U₂
h2U₁ : K₁.carrier ⊆ U₁
h2U₂ : K₂.carrier ⊆ U₂
hU : Disjoint U₁ U₂
L₁ : Set G
h1L₁ : Membership.mem (γ := Filter G) (𝓝 1) L₁
V₁ : Set G
h1V₁ : V₁ ⊆ L₁
h2V₁ : IsOpen[inst_1] V₁
h3V₁ : 1 ∈ V₁
h2L₁ : K₁.carrier * V₁ ⊆ U₁
L₂ : Set G
h1L₂ : Membership.mem (γ := Filter G) (𝓝 1) L₂
V₂ : Set G
h1V₂ : V₂ ⊆ L₂
h2V₂ : IsOpen[inst_1] V₂
h3V₂ : 1 ∈ V₂
h2L₂ : K₂.carrier * V₂ ⊆ U₂
eval : (Compacts G → ℝ) → ℝ := fun (f : Compacts G → ℝ) ↦ f K₁ + f K₂ - f (K₁ ⊔ K₂)
this : Continuous eval
V : Set G := V₁ ∩ V₂
U : Set G
h1U : U ⊆ (↑{ carrier := V⁻¹, is_open' := ⋯, mem' := ⋯ : OpenNhdsOf (α := G) 1 }.toOpens : Set G)
h2U : IsOpen[inst_1] U
h3U : 1 ∈ U
hU₁ : (interior U).Nonempty
h₁ : Disjoint (K₁.carrier * U⁻¹) (K₂.carrier * U⁻¹)
⊢ prehaar (↑K₀ : Set G) U (K₁ ⊔ K₂) = prehaar (↑K₀ : Set G) U K₁ + prehaar (↑K₀ : Set G) U K₂

Tactic:
apply prehaar_sup_eq

Premises used: MeasureTheory.Measure.haar.prehaar_sup_eq
-- 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₁ K₂ : Compacts G
h : Disjoint K₁.carrier K₂.carrier
h₂ : IsClosed[inst_1] K₂.carrier
U₁ U₂ : Set G
h1U₁ : IsOpen[inst_1] U₁
h1U₂ : IsOpen[inst_1] U₂
h2U₁ : K₁.carrier ⊆ U₁
h2U₂ : K₂.carrier ⊆ U₂
hU : Disjoint U₁ U₂
L₁ : Set G
h1L₁ : Membership.mem (γ := Filter G) (𝓝 1) L₁
V₁ : Set G
h1V₁ : V₁ ⊆ L₁
h2V₁ : IsOpen[inst_1] V₁
h3V₁ : 1 ∈ V₁
h2L₁ : K₁.carrier * V₁ ⊆ U₁
L₂ : Set G
h1L₂ : Membership.mem (γ := Filter G) (𝓝 1) L₂
V₂ : Set G
h1V₂ : V₂ ⊆ L₂
h2V₂ : IsOpen[inst_1] V₂
h3V₂ : 1 ∈ V₂
h2L₂ : K₂.carrier * V₂ ⊆ U₂
eval : (Compacts G → ℝ) → ℝ := fun (f : Compacts G → ℝ) ↦ f K₁ + f K₂ - f (K₁ ⊔ K₂)
this : Continuous eval
V : Set G := V₁ ∩ V₂
U : Set G
h1U : U ⊆ (↑{ carrier := V⁻¹, is_open' := ⋯, mem' := ⋯ : OpenNhdsOf (α := G) 1 }.toOpens : Set G)
h2U : IsOpen[inst_1] U
h3U : 1 ∈ U
hU₁ : U.Nonempty
⊢ (interior U).Nonempty

Tactic:
rw [h2U.interior_eq]

Premises used: IsOpen.interior_eq
-- 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₁ K₂ : Compacts G
h : Disjoint K₁.carrier K₂.carrier
h₂ : IsClosed[inst_1] K₂.carrier
U₁ U₂ : Set G
h1U₁ : IsOpen[inst_1] U₁
h1U₂ : IsOpen[inst_1] U₂
h2U₁ : K₁.carrier ⊆ U₁
h2U₂ : K₂.carrier ⊆ U₂
hU : Disjoint U₁ U₂
L₁ : Set G
h1L₁ : Membership.mem (γ := Filter G) (𝓝 1) L₁
V₁ : Set G
h1V₁ : V₁ ⊆ L₁
h2V₁ : IsOpen[inst_1] V₁
h3V₁ : 1 ∈ V₁
h2L₁ : K₁.carrier * V₁ ⊆ U₁
L₂ : Set G
h1L₂ : Membership.mem (γ := Filter G) (𝓝 1) L₂
V₂ : Set G
h1V₂ : V₂ ⊆ L₂
h2V₂ : IsOpen[inst_1] V₂
h3V₂ : 1 ∈ V₂
h2L₂ : K₂.carrier * V₂ ⊆ U₂
eval : (Compacts G → ℝ) → ℝ := fun (f : Compacts G → ℝ) ↦ f K₁ + f K₂ - f (K₁ ⊔ K₂)
this : Continuous eval
V : Set G := V₁ ∩ V₂
U : Set G
h1U : U ⊆ (↑{ carrier := V⁻¹, is_open' := ⋯, mem' := ⋯ : OpenNhdsOf (α := G) 1 }.toOpens : Set G)
h2U : IsOpen[inst_1] U
h3U : 1 ∈ U
⊢ U.Nonempty

Tactic:
⟨1, h3U⟩

Premises used: Set.Nonempty, Exists.intro, OfNat.ofNat
-- 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₁ K₂ : Compacts G
h : Disjoint K₁.carrier K₂.carrier
h₂ : IsClosed[inst_1] K₂.carrier
U₁ U₂ : Set G
h1U₁ : IsOpen[inst_1] U₁
h1U₂ : IsOpen[inst_1] U₂
h2U₁ : K₁.carrier ⊆ U₁
h2U₂ : K₂.carrier ⊆ U₂
hU : Disjoint U₁ U₂
L₁ : Set G
h1L₁ : Membership.mem (γ := Filter G) (𝓝 1) L₁
V₁ : Set G
h1V₁ : V₁ ⊆ L₁
h2V₁ : IsOpen[inst_1] V₁
h3V₁ : 1 ∈ V₁
h2L₁ : K₁.carrier * V₁ ⊆ U₁
L₂ : Set G
h1L₂ : Membership.mem (γ := Filter G) (𝓝 1) L₂
V₂ : Set G
h1V₂ : V₂ ⊆ L₂
h2V₂ : IsOpen[inst_1] V₂
h3V₂ : 1 ∈ V₂
h2L₂ : K₂.carrier * V₂ ⊆ U₂
eval : (Compacts G → ℝ) → ℝ := fun (f : Compacts G → ℝ) ↦ f K₁ + f K₂ - f (K₁ ⊔ K₂)
this : Continuous eval
V : Set G := V₁ ∩ V₂
U : Set G
h1U : U ⊆ (↑{ carrier := V⁻¹, is_open' := ⋯, mem' := ⋯ : OpenNhdsOf (α := G) 1 }.toOpens : Set G)
h2U : IsOpen[inst_1] U
h3U : 1 ∈ U
⊢ U.Nonempty

Tactic:
exact ⟨1, h3U⟩
-- 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₁ K₂ : Compacts G
h : Disjoint K₁.carrier K₂.carrier
h₂ : IsClosed[inst_1] K₂.carrier
U₁ U₂ : Set G
h1U₁ : IsOpen[inst_1] U₁
h1U₂ : IsOpen[inst_1] U₂
h2U₁ : K₁.carrier ⊆ U₁
h2U₂ : K₂.carrier ⊆ U₂
hU : Disjoint U₁ U₂
L₁ : Set G
h1L₁ : Membership.mem (γ := Filter G) (𝓝 1) L₁
V₁ : Set G
h1V₁ : V₁ ⊆ L₁
h2V₁ : IsOpen[inst_1] V₁
h3V₁ : 1 ∈ V₁
h2L₁ : K₁.carrier * V₁ ⊆ U₁
L₂ : Set G
h1L₂ : Membership.mem (γ := Filter G) (𝓝 1) L₂
V₂ : Set G
h1V₂ : V₂ ⊆ L₂
h2V₂ : IsOpen[inst_1] V₂
h3V₂ : 1 ∈ V₂
h2L₂ : K₂.carrier * V₂ ⊆ U₂
eval : (Compacts G → ℝ) → ℝ := fun (f : Compacts G → ℝ) ↦ f K₁ + f K₂ - f (K₁ ⊔ K₂)
this : Continuous eval
V : Set G := V₁ ∩ V₂
U : Set G
h1U : U ⊆ (↑{ carrier := V⁻¹, is_open' := ⋯, mem' := ⋯ : OpenNhdsOf (α := G) 1 }.toOpens : Set G)
h2U : IsOpen[inst_1] U
h3U : 1 ∈ U
⊢ Disjoint (K₁.carrier * U⁻¹) (K₂.carrier * U⁻¹)

Tactic:
disjoint_of_subset ?_ ?_ hU

Premises used: Set.disjoint_of_subset
-- 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₁ K₂ : Compacts G
h : Disjoint K₁.carrier K₂.carrier
h₂ : IsClosed[inst_1] K₂.carrier
U₁ U₂ : Set G
h1U₁ : IsOpen[inst_1] U₁
h1U₂ : IsOpen[inst_1] U₂
h2U₁ : K₁.carrier ⊆ U₁
h2U₂ : K₂.carrier ⊆ U₂
hU : Disjoint U₁ U₂
L₁ : Set G
h1L₁ : Membership.mem (γ := Filter G) (𝓝 1) L₁
V₁ : Set G
h1V₁ : V₁ ⊆ L₁
h2V₁ : IsOpen[inst_1] V₁
h3V₁ : 1 ∈ V₁
h2L₁ : K₁.carrier * V₁ ⊆ U₁
L₂ : Set G
h1L₂ : Membership.mem (γ := Filter G) (𝓝 1) L₂
V₂ : Set G
h1V₂ : V₂ ⊆ L₂
h2V₂ : IsOpen[inst_1] V₂
h3V₂ : 1 ∈ V₂
h2L₂ : K₂.carrier * V₂ ⊆ U₂
eval : (Compacts G → ℝ) → ℝ := fun (f : Compacts G → ℝ) ↦ f K₁ + f K₂ - f (K₁ ⊔ K₂)
this : Continuous eval
V : Set G := V₁ ∩ V₂
U : Set G
h1U : U ⊆ (↑{ carrier := V⁻¹, is_open' := ⋯, mem' := ⋯ : OpenNhdsOf (α := G) 1 }.toOpens : Set G)
h2U : IsOpen[inst_1] U
h3U : 1 ∈ U
h₁ : K₁.carrier * U⁻¹ ⊆ U₁
h₃ : K₂.carrier * U⁻¹ ⊆ U₂
⊢ Disjoint (K₁.carrier * U⁻¹) (K₂.carrier * U⁻¹)

Tactic:
refine disjoint_of_subset ?_ ?_ hU

Premises used: Set.disjoint_of_subset
-- 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₁ K₂ : Compacts G
h : Disjoint K₁.carrier K₂.carrier
h₂ : IsClosed[inst_1] K₂.carrier
U₁ U₂ : Set G
h1U₁ : IsOpen[inst_1] U₁
h1U₂ : IsOpen[inst_1] U₂
h2U₁ : K₁.carrier ⊆ U₁
h2U₂ : K₂.carrier ⊆ U₂
hU : Disjoint U₁ U₂
L₁ : Set G
h1L₁ : Membership.mem (γ := Filter G) (𝓝 1) L₁
V₁ : Set G
h1V₁ : V₁ ⊆ L₁
h2V₁ : IsOpen[inst_1] V₁
h3V₁ : 1 ∈ V₁
h2L₁ : K₁.carrier * V₁ ⊆ U₁
L₂ : Set G
h1L₂ : Membership.mem (γ := Filter G) (𝓝 1) L₂
V₂ : Set G
h1V₂ : V₂ ⊆ L₂
h2V₂ : IsOpen[inst_1] V₂
h3V₂ : 1 ∈ V₂
h2L₂ : K₂.carrier * V₂ ⊆ U₂
eval : (Compacts G → ℝ) → ℝ := fun (f : Compacts G → ℝ) ↦ f K₁ + f K₂ - f (K₁ ⊔ K₂)
this : Continuous eval
V : Set G := V₁ ∩ V₂
U : Set G
h1U : U ⊆ (↑{ carrier := V⁻¹, is_open' := ⋯, mem' := ⋯ : OpenNhdsOf (α := G) 1 }.toOpens : Set G)
h2U : IsOpen[inst_1] U
h3U : 1 ∈ U
⊢ K₁.carrier * U⁻¹ ⊆ U₁

Tactic:
Subset.trans (mul_subset_mul Subset.rfl ?_) h2L₁

Premises used: Set.Subset.trans, Set.Subset.rfl, Set.mul_subset_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
K₁ K₂ : Compacts G
h : Disjoint K₁.carrier K₂.carrier
h₂ : IsClosed[inst_1] K₂.carrier
U₁ U₂ : Set G
h1U₁ : IsOpen[inst_1] U₁
h1U₂ : IsOpen[inst_1] U₂
h2U₁ : K₁.carrier ⊆ U₁
h2U₂ : K₂.carrier ⊆ U₂
hU : Disjoint U₁ U₂
L₁ : Set G
h1L₁ : Membership.mem (γ := Filter G) (𝓝 1) L₁
V₁ : Set G
h1V₁ : V₁ ⊆ L₁
h2V₁ : IsOpen[inst_1] V₁
h3V₁ : 1 ∈ V₁
h2L₁ : K₁.carrier * V₁ ⊆ U₁
L₂ : Set G
h1L₂ : Membership.mem (γ := Filter G) (𝓝 1) L₂
V₂ : Set G
h1V₂ : V₂ ⊆ L₂
h2V₂ : IsOpen[inst_1] V₂
h3V₂ : 1 ∈ V₂
h2L₂ : K₂.carrier * V₂ ⊆ U₂
eval : (Compacts G → ℝ) → ℝ := fun (f : Compacts G → ℝ) ↦ f K₁ + f K₂ - f (K₁ ⊔ K₂)
this : Continuous eval
V : Set G := V₁ ∩ V₂
U : Set G
h1U : U ⊆ (↑{ carrier := V⁻¹, is_open' := ⋯, mem' := ⋯ : OpenNhdsOf (α := G) 1 }.toOpens : Set G)
h2U : IsOpen[inst_1] U
h3U : 1 ∈ U
h₁ : U⁻¹ ⊆ V₁
⊢ K₁.carrier * U⁻¹ ⊆ U₁

Tactic:
refine Subset.trans (mul_subset_mul Subset.rfl ?_) h2L₁

Premises used: Set.Subset.trans, Set.Subset.rfl, Set.mul_subset_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
K₁ K₂ : Compacts G
h : Disjoint K₁.carrier K₂.carrier
h₂ : IsClosed[inst_1] K₂.carrier
U₁ U₂ : Set G
h1U₁ : IsOpen[inst_1] U₁
h1U₂ : IsOpen[inst_1] U₂
h2U₁ : K₁.carrier ⊆ U₁
h2U₂ : K₂.carrier ⊆ U₂
hU : Disjoint U₁ U₂
L₁ : Set G
h1L₁ : Membership.mem (γ := Filter G) (𝓝 1) L₁
V₁ : Set G
h1V₁ : V₁ ⊆ L₁
h2V₁ : IsOpen[inst_1] V₁
h3V₁ : 1 ∈ V₁
h2L₁ : K₁.carrier * V₁ ⊆ U₁
L₂ : Set G
h1L₂ : Membership.mem (γ := Filter G) (𝓝 1) L₂
V₂ : Set G
h1V₂ : V₂ ⊆ L₂
h2V₂ : IsOpen[inst_1] V₂
h3V₂ : 1 ∈ V₂
h2L₂ : K₂.carrier * V₂ ⊆ U₂
eval : (Compacts G → ℝ) → ℝ := fun (f : Compacts G → ℝ) ↦ f K₁ + f K₂ - f (K₁ ⊔ K₂)
this : Continuous eval
V : Set G := V₁ ∩ V₂
U : Set G
h1U : U ⊆ (↑{ carrier := V⁻¹, is_open' := ⋯, mem' := ⋯ : OpenNhdsOf (α := G) 1 }.toOpens : Set G)
h2U : IsOpen[inst_1] U
h3U : 1 ∈ U
⊢ U⁻¹ ⊆ V₁

Tactic:
Subset.trans (inv_subset.mpr h1U) inter_subset_left

Premises used: Iff.mpr, Set.Subset.trans, Set.inter_subset_left, Set.inv_subset
-- 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₁ K₂ : Compacts G
h : Disjoint K₁.carrier K₂.carrier
h₂ : IsClosed[inst_1] K₂.carrier
U₁ U₂ : Set G
h1U₁ : IsOpen[inst_1] U₁
h1U₂ : IsOpen[inst_1] U₂
h2U₁ : K₁.carrier ⊆ U₁
h2U₂ : K₂.carrier ⊆ U₂
hU : Disjoint U₁ U₂
L₁ : Set G
h1L₁ : Membership.mem (γ := Filter G) (𝓝 1) L₁
V₁ : Set G
h1V₁ : V₁ ⊆ L₁
h2V₁ : IsOpen[inst_1] V₁
h3V₁ : 1 ∈ V₁
h2L₁ : K₁.carrier * V₁ ⊆ U₁
L₂ : Set G
h1L₂ : Membership.mem (γ := Filter G) (𝓝 1) L₂
V₂ : Set G
h1V₂ : V₂ ⊆ L₂
h2V₂ : IsOpen[inst_1] V₂
h3V₂ : 1 ∈ V₂
h2L₂ : K₂.carrier * V₂ ⊆ U₂
eval : (Compacts G → ℝ) → ℝ := fun (f : Compacts G → ℝ) ↦ f K₁ + f K₂ - f (K₁ ⊔ K₂)
this : Continuous eval
V : Set G := V₁ ∩ V₂
U : Set G
h1U : U ⊆ (↑{ carrier := V⁻¹, is_open' := ⋯, mem' := ⋯ : OpenNhdsOf (α := G) 1 }.toOpens : Set G)
h2U : IsOpen[inst_1] U
h3U : 1 ∈ U
⊢ U⁻¹ ⊆ V₁

Tactic:
exact Subset.trans (inv_subset.mpr h1U) inter_subset_left

Premises used: Iff.mpr, Set.Subset.trans, Set.inter_subset_left, Set.inv_subset
-- 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₁ K₂ : Compacts G
h : Disjoint K₁.carrier K₂.carrier
h₂ : IsClosed[inst_1] K₂.carrier
U₁ U₂ : Set G
h1U₁ : IsOpen[inst_1] U₁
h1U₂ : IsOpen[inst_1] U₂
h2U₁ : K₁.carrier ⊆ U₁
h2U₂ : K₂.carrier ⊆ U₂
hU : Disjoint U₁ U₂
L₁ : Set G
h1L₁ : Membership.mem (γ := Filter G) (𝓝 1) L₁
V₁ : Set G
h1V₁ : V₁ ⊆ L₁
h2V₁ : IsOpen[inst_1] V₁
h3V₁ : 1 ∈ V₁
h2L₁ : K₁.carrier * V₁ ⊆ U₁
L₂ : Set G
h1L₂ : Membership.mem (γ := Filter G) (𝓝 1) L₂
V₂ : Set G
h1V₂ : V₂ ⊆ L₂
h2V₂ : IsOpen[inst_1] V₂
h3V₂ : 1 ∈ V₂
h2L₂ : K₂.carrier * V₂ ⊆ U₂
eval : (Compacts G → ℝ) → ℝ := fun (f : Compacts G → ℝ) ↦ f K₁ + f K₂ - f (K₁ ⊔ K₂)
this : Continuous eval
V : Set G := V₁ ∩ V₂
U : Set G
h1U : U ⊆ (↑{ carrier := V⁻¹, is_open' := ⋯, mem' := ⋯ : OpenNhdsOf (α := G) 1 }.toOpens : Set G)
h2U : IsOpen[inst_1] U
h3U : 1 ∈ U
⊢ K₂.carrier * U⁻¹ ⊆ U₂

Tactic:
Subset.trans (mul_subset_mul Subset.rfl ?_) h2L₂

Premises used: Set.Subset.trans, Set.Subset.rfl, Set.mul_subset_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
K₁ K₂ : Compacts G
h : Disjoint K₁.carrier K₂.carrier
h₂ : IsClosed[inst_1] K₂.carrier
U₁ U₂ : Set G
h1U₁ : IsOpen[inst_1] U₁
h1U₂ : IsOpen[inst_1] U₂
h2U₁ : K₁.carrier ⊆ U₁
h2U₂ : K₂.carrier ⊆ U₂
hU : Disjoint U₁ U₂
L₁ : Set G
h1L₁ : Membership.mem (γ := Filter G) (𝓝 1) L₁
V₁ : Set G
h1V₁ : V₁ ⊆ L₁
h2V₁ : IsOpen[inst_1] V₁
h3V₁ : 1 ∈ V₁
h2L₁ : K₁.carrier * V₁ ⊆ U₁
L₂ : Set G
h1L₂ : Membership.mem (γ := Filter G) (𝓝 1) L₂
V₂ : Set G
h1V₂ : V₂ ⊆ L₂
h2V₂ : IsOpen[inst_1] V₂
h3V₂ : 1 ∈ V₂
h2L₂ : K₂.carrier * V₂ ⊆ U₂
eval : (Compacts G → ℝ) → ℝ := fun (f : Compacts G → ℝ) ↦ f K₁ + f K₂ - f (K₁ ⊔ K₂)
this : Continuous eval
V : Set G := V₁ ∩ V₂
U : Set G
h1U : U ⊆ (↑{ carrier := V⁻¹, is_open' := ⋯, mem' := ⋯ : OpenNhdsOf (α := G) 1 }.toOpens : Set G)
h2U : IsOpen[inst_1] U
h3U : 1 ∈ U
h₁ : U⁻¹ ⊆ V₂
⊢ K₂.carrier * U⁻¹ ⊆ U₂

Tactic:
refine Subset.trans (mul_subset_mul Subset.rfl ?_) h2L₂

Premises used: Set.Subset.trans, Set.Subset.rfl, Set.mul_subset_mul