G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : T2Space G
f : G ≃ₜ G
h : ∀ ⦃K : Compacts G⦄, (fun s => ↑(toFun μ s)) (Compacts.map ↑f (_ : Continuous ↑f) K) = (fun s => ↑(toFun μ s)) K
A : Set G
⊢ ∀ (s : Set G) (hs : IsOpen s),
    innerContent μ { carrier := ↑f.toEquiv ⁻¹' s, is_open' := (_ : IsOpen (↑f.toEquiv ⁻¹' s)) } =
      innerContent μ { carrier := s, is_open' := hs }
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : T2Space G
f : G ≃ₜ G
h : ∀ ⦃K : Compacts G⦄, (fun s => ↑(toFun μ s)) (Compacts.map ↑f (_ : Continuous ↑f) K) = (fun s => ↑(toFun μ s)) K
A : Set G
⊢ ↑(Content.outerMeasure μ) (↑f ⁻¹' A) = ↑(Content.outerMeasure μ) A
refine' inducedOuterMeasure_preimage _ μ.innerContent_iUnion_nat μ.innerContent_mono _
  (fun _ => f.isOpen_preimage) _
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : T2Space G
f : G ≃ₜ G
h : ∀ ⦃K : Compacts G⦄, (fun s => ↑(toFun μ s)) (Compacts.map ↑f (_ : Continuous ↑f) K) = (fun s => ↑(toFun μ s)) K
A s : Set G
hs : IsOpen s
⊢ innerContent μ { carrier := ↑f.toEquiv ⁻¹' s, is_open' := (_ : IsOpen (↑f.toEquiv ⁻¹' s)) } =
    innerContent μ { carrier := s, is_open' := hs }
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : T2Space G
f : G ≃ₜ G
h : ∀ ⦃K : Compacts G⦄, (fun s => ↑(toFun μ s)) (Compacts.map ↑f (_ : Continuous ↑f) K) = (fun s => ↑(toFun μ s)) K
A : Set G
⊢ ∀ (s : Set G) (hs : IsOpen s),
    innerContent μ { carrier := ↑f.toEquiv ⁻¹' s, is_open' := (_ : IsOpen (↑f.toEquiv ⁻¹' s)) } =
      innerContent μ { carrier := s, is_open' := hs }
intro s hs
no goals
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : T2Space G
f : G ≃ₜ G
h : ∀ ⦃K : Compacts G⦄, (fun s => ↑(toFun μ s)) (Compacts.map ↑f (_ : Continuous ↑f) K) = (fun s => ↑(toFun μ s)) K
A s : Set G
hs : IsOpen s
⊢ innerContent μ { carrier := ↑f.toEquiv ⁻¹' s, is_open' := (_ : IsOpen (↑f.toEquiv ⁻¹' s)) } =
    innerContent μ { carrier := s, is_open' := hs }
convert μ.innerContent_comap f h ⟨s, hs⟩