G : Type w
inst✝ : TopologicalSpace G
μ : Content G
f : G ≃ₜ G
h : ∀ ⦃K : Compacts G⦄, (fun s => ↑(toFun μ s)) (Compacts.map ↑f (_ : Continuous ↑f) K) = (fun s => ↑(toFun μ s)) K
U : Opens G
K : Compacts G
⊢ ↑K ⊆ ↑(↑(Opens.comap (Homeomorph.toContinuousMap f)) U) →
    (fun s => ↑(toFun μ s)) (↑(Compacts.equiv f) K) = (fun s => ↑(toFun μ s)) K
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
f : G ≃ₜ G
h : ∀ ⦃K : Compacts G⦄, (fun s => ↑(toFun μ s)) (Compacts.map ↑f (_ : Continuous ↑f) K) = (fun s => ↑(toFun μ s)) K
U : Opens G
⊢ innerContent μ (↑(Opens.comap (Homeomorph.toContinuousMap f)) U) = innerContent μ U
refine' (Compacts.equiv f).surjective.iSup_congr _ fun K => iSup_congr_Prop image_subset_iff _
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
f : G ≃ₜ G
h : ∀ ⦃K : Compacts G⦄, (fun s => ↑(toFun μ s)) (Compacts.map ↑f (_ : Continuous ↑f) K) = (fun s => ↑(toFun μ s)) K
U : Opens G
K : Compacts G
hK : ↑K ⊆ ↑(↑(Opens.comap (Homeomorph.toContinuousMap f)) U)
⊢ (fun s => ↑(toFun μ s)) (↑(Compacts.equiv f) K) = (fun s => ↑(toFun μ s)) K
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
f : G ≃ₜ G
h : ∀ ⦃K : Compacts G⦄, (fun s => ↑(toFun μ s)) (Compacts.map ↑f (_ : Continuous ↑f) K) = (fun s => ↑(toFun μ s)) K
U : Opens G
K : Compacts G
⊢ ↑K ⊆ ↑(↑(Opens.comap (Homeomorph.toContinuousMap f)) U) →
    (fun s => ↑(toFun μ s)) (↑(Compacts.equiv f) K) = (fun s => ↑(toFun μ s)) K
intro hK
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
f : G ≃ₜ G
h : ∀ ⦃K : Compacts G⦄, (fun s => ↑(toFun μ s)) (Compacts.map ↑f (_ : Continuous ↑f) K) = (fun s => ↑(toFun μ s)) K
U : Opens G
K : Compacts G
hK : ↑K ⊆ ↑(↑(Opens.comap (Homeomorph.toContinuousMap f)) U)
⊢ ↑(toFun μ (Compacts.map ↑f (_ : Continuous ↑f) K)) = ↑(toFun μ K)
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
f : G ≃ₜ G
h : ∀ ⦃K : Compacts G⦄, (fun s => ↑(toFun μ s)) (Compacts.map ↑f (_ : Continuous ↑f) K) = (fun s => ↑(toFun μ s)) K
U : Opens G
K : Compacts G
hK : ↑K ⊆ ↑(↑(Opens.comap (Homeomorph.toContinuousMap f)) U)
⊢ (fun s => ↑(toFun μ s)) (↑(Compacts.equiv f) K) = (fun s => ↑(toFun μ s)) K
simp only [Equiv.coe_fn_mk, Subtype.mk_eq_mk, Compacts.equiv]
no goals
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
f : G ≃ₜ G
h : ∀ ⦃K : Compacts G⦄, (fun s => ↑(toFun μ s)) (Compacts.map ↑f (_ : Continuous ↑f) K) = (fun s => ↑(toFun μ s)) K
U : Opens G
K : Compacts G
hK : ↑K ⊆ ↑(↑(Opens.comap (Homeomorph.toContinuousMap f)) U)
⊢ ↑(toFun μ (Compacts.map ↑f (_ : Continuous ↑f) K)) = ↑(toFun μ K)
apply h