-- Mathlib/MeasureTheory/Measure/Haar/Basic.lean
theorem chaar_sup_eq {K₀ : PositiveCompacts G}
    {K₁ K₂ : Compacts G} (h : Disjoint K₁.1 K₂.1) (h₂ : IsClosed K₂.1) :
    chaar K₀ (K₁ ⊔ K₂) = chaar K₀ K₁ + chaar K₀ K₂

Proof state:
case intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
K₁ K₂ : Compacts G
h : Disjoint K₁.carrier K₂.carrier
h₂ : IsClosed K₂.carrier
U₁ U₂ : Set G
h1U₁ : IsOpen U₁
h1U₂ : IsOpen U₂
h2U₁ : K₁.carrier ⊆ U₁
h2U₂ : K₂.carrier ⊆ U₂
hU : Disjoint U₁ U₂
⊢ chaar K₀ (K₁ ⊔ K₂) = chaar K₀ K₁ + chaar K₀ K₂

Tactic:
rcases compact_open_separated_mul_right K₁.2 h1U₁ h2U₁ with ⟨L₁, h1L₁, h2L₁⟩

Result:
case intro.intro.intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
K₁ K₂ : Compacts G
h : Disjoint K₁.carrier K₂.carrier
h₂ : IsClosed K₂.carrier
U₁ U₂ : Set G
h1U₁ : IsOpen U₁
h1U₂ : IsOpen U₂
h2U₁ : K₁.carrier ⊆ U₁
h2U₂ : K₂.carrier ⊆ U₂
hU : Disjoint U₁ U₂
L₁ : Set G
h1L₁ : L₁ ∈ 𝓝 1
h2L₁ : K₁.carrier * L₁ ⊆ U₁
⊢ chaar K₀ (K₁ ⊔ K₂) = chaar K₀ K₁ + chaar K₀ K₂

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
K₁ K₂ : Compacts G
h : Disjoint K₁.carrier K₂.carrier
h₂ : IsClosed K₂.carrier
U₁ U₂ : Set G
h1U₁ : IsOpen U₁
h1U₂ : IsOpen U₂
h2U₁ : K₁.carrier ⊆ U₁
h2U₂ : K₂.carrier ⊆ U₂
hU : Disjoint U₁ U₂
L₁ : Set G
h1L₁ : L₁ ∈ 𝓝 1
V₁ : Set G
h1V₁ : V₁ ⊆ L₁
h2V₁ : IsOpen V₁
h3V₁ : 1 ∈ V₁
h2L₁ : K₁.carrier * V₁ ⊆ U₁
L₂ : Set G
h1L₂ : L₂ ∈ 𝓝 1
h2L₂ : K₂.carrier * L₂ ⊆ U₂
⊢ chaar K₀ (K₁ ⊔ K₂) = chaar K₀ K₁ + chaar K₀ K₂

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

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
K₁ K₂ : Compacts G
h : Disjoint K₁.carrier K₂.carrier
h₂ : IsClosed K₂.carrier
U₁ U₂ : Set G
h1U₁ : IsOpen U₁
h1U₂ : IsOpen U₂
h2U₁ : K₁.carrier ⊆ U₁
h2U₂ : K₂.carrier ⊆ U₂
hU : Disjoint U₁ U₂
L₁ : Set G
h1L₁ : L₁ ∈ 𝓝 1
V₁ : Set G
h1V₁ : V₁ ⊆ L₁
h2V₁ : IsOpen V₁
h3V₁ : 1 ∈ V₁
h2L₁ : K₁.carrier * V₁ ⊆ U₁
L₂ : Set G
h1L₂ : L₂ ∈ 𝓝 1
h2L₂ : K₂.carrier * L₂ ⊆ U₂
V₂ : Set G
h1V₂ : V₂ ⊆ L₂
h2V₂ : IsOpen V₂
h3V₂ : 1 ∈ V₂
⊢ chaar K₀ (K₁ ⊔ K₂) = chaar K₀ K₁ + chaar K₀ K₂

Proof state:
case intro.intro.intro.intro.h
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
K₁ K₂ : Compacts G
h : Disjoint K₁.carrier K₂.carrier
h₂ : IsClosed K₂.carrier
U₁ U₂ : Set G
h1U₁ : IsOpen U₁
h1U₂ : IsOpen U₂
h2U₁ : K₁.carrier ⊆ U₁
h2U₂ : K₂.carrier ⊆ U₂
hU : Disjoint U₁ U₂
L₁ : Set G
h1L₁ : L₁ ∈ 𝓝 1
V₁ : Set G
h1V₁ : V₁ ⊆ L₁
h2V₁ : IsOpen V₁
h3V₁ : 1 ∈ V₁
h2L₁ : K₁.carrier * V₁ ⊆ U₁
L₂ : Set G
h1L₂ : L₂ ∈ 𝓝 1
V₂ : Set G
h1V₂ : V₂ ⊆ L₂
h2V₂ : IsOpen V₂
h3V₂ : 1 ∈ V₂
h2L₂ : K₂.carrier * V₂ ⊆ U₂
eval : (Compacts G → ℝ) → ℝ := fun f => 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' := ⋯ }.toOpens
h2U : IsOpen U
h3U : 1 ∈ U
⊢ Disjoint (K₁.carrier * U⁻¹) (K₂.carrier * U⁻¹)

Tactic:
refine disjoint_of_subset ?_ ?_ hU

Result:
case intro.intro.intro.intro.h.refine_1
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
K₁ K₂ : Compacts G
h : Disjoint K₁.carrier K₂.carrier
h₂ : IsClosed K₂.carrier
U₁ U₂ : Set G
h1U₁ : IsOpen U₁
h1U₂ : IsOpen U₂
h2U₁ : K₁.carrier ⊆ U₁
h2U₂ : K₂.carrier ⊆ U₂
hU : Disjoint U₁ U₂
L₁ : Set G
h1L₁ : L₁ ∈ 𝓝 1
V₁ : Set G
h1V₁ : V₁ ⊆ L₁
h2V₁ : IsOpen V₁
h3V₁ : 1 ∈ V₁
h2L₁ : K₁.carrier * V₁ ⊆ U₁
L₂ : Set G
h1L₂ : L₂ ∈ 𝓝 1
V₂ : Set G
h1V₂ : V₂ ⊆ L₂
h2V₂ : IsOpen V₂
h3V₂ : 1 ∈ V₂
h2L₂ : K₂.carrier * V₂ ⊆ U₂
eval : (Compacts G → ℝ) → ℝ := fun f => 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' := ⋯ }.toOpens
h2U : IsOpen U
h3U : 1 ∈ U
⊢ K₁.carrier * U⁻¹ ⊆ U₁

case intro.intro.intro.intro.h.refine_2
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
K₁ K₂ : Compacts G
h : Disjoint K₁.carrier K₂.carrier
h₂ : IsClosed K₂.carrier
U₁ U₂ : Set G
h1U₁ : IsOpen U₁
h1U₂ : IsOpen U₂
h2U₁ : K₁.carrier ⊆ U₁
h2U₂ : K₂.carrier ⊆ U₂
hU : Disjoint U₁ U₂
L₁ : Set G
h1L₁ : L₁ ∈ 𝓝 1
V₁ : Set G
h1V₁ : V₁ ⊆ L₁
h2V₁ : IsOpen V₁
h3V₁ : 1 ∈ V₁
h2L₁ : K₁.carrier * V₁ ⊆ U₁
L₂ : Set G
h1L₂ : L₂ ∈ 𝓝 1
V₂ : Set G
h1V₂ : V₂ ⊆ L₂
h2V₂ : IsOpen V₂
h3V₂ : 1 ∈ V₂
h2L₂ : K₂.carrier * V₂ ⊆ U₂
eval : (Compacts G → ℝ) → ℝ := fun f => 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' := ⋯ }.toOpens
h2U : IsOpen U
h3U : 1 ∈ U
⊢ K₂.carrier * U⁻¹ ⊆ U₂

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
K₁ K₂ : Compacts G
h : Disjoint K₁.carrier K₂.carrier
h₂ : IsClosed K₂.carrier
U₁ U₂ : Set G
h1U₁ : IsOpen U₁
h1U₂ : IsOpen U₂
h2U₁ : K₁.carrier ⊆ U₁
h2U₂ : K₂.carrier ⊆ U₂
hU : Disjoint U₁ U₂
L₁ : Set G
h1L₁ : L₁ ∈ 𝓝 1
h2L₁ : K₁.carrier * L₁ ⊆ U₁
⊢ chaar K₀ (K₁ ⊔ K₂) = chaar K₀ K₁ + chaar K₀ K₂

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

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
K₁ K₂ : Compacts G
h : Disjoint K₁.carrier K₂.carrier
h₂ : IsClosed K₂.carrier
U₁ U₂ : Set G
h1U₁ : IsOpen U₁
h1U₂ : IsOpen U₂
h2U₁ : K₁.carrier ⊆ U₁
h2U₂ : K₂.carrier ⊆ U₂
hU : Disjoint U₁ U₂
L₁ : Set G
h1L₁ : L₁ ∈ 𝓝 1
h2L₁ : K₁.carrier * L₁ ⊆ U₁
V₁ : Set G
h1V₁ : V₁ ⊆ L₁
h2V₁ : IsOpen V₁
h3V₁ : 1 ∈ V₁
⊢ chaar K₀ (K₁ ⊔ K₂) = chaar K₀ K₁ + chaar K₀ K₂

Proof state:
case intro.intro.intro.intro.h.refine_1
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
K₁ K₂ : Compacts G
h : Disjoint K₁.carrier K₂.carrier
h₂ : IsClosed K₂.carrier
U₁ U₂ : Set G
h1U₁ : IsOpen U₁
h1U₂ : IsOpen U₂
h2U₁ : K₁.carrier ⊆ U₁
h2U₂ : K₂.carrier ⊆ U₂
hU : Disjoint U₁ U₂
L₁ : Set G
h1L₁ : L₁ ∈ 𝓝 1
V₁ : Set G
h1V₁ : V₁ ⊆ L₁
h2V₁ : IsOpen V₁
h3V₁ : 1 ∈ V₁
h2L₁ : K₁.carrier * V₁ ⊆ U₁
L₂ : Set G
h1L₂ : L₂ ∈ 𝓝 1
V₂ : Set G
h1V₂ : V₂ ⊆ L₂
h2V₂ : IsOpen V₂
h3V₂ : 1 ∈ V₂
h2L₂ : K₂.carrier * V₂ ⊆ U₂
eval : (Compacts G → ℝ) → ℝ := fun f => 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' := ⋯ }.toOpens
h2U : IsOpen U
h3U : 1 ∈ U
⊢ U⁻¹ ⊆ V₁

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

Result:
no goals