-- Mathlib/MeasureTheory/Measure/Regular.lean
theorem map' {α β} [MeasurableSpace α] [MeasurableSpace β] {μ : Measure α} {pa qa : Set α → Prop}
    (H : InnerRegularWRT μ pa qa) (f : α ≃ᵐ β) {pb qb : Set β → Prop}
    (hAB : ∀ U, qb U → qa (f ⁻¹' U)) (hAB' : ∀ K, pa K → pb (f '' K)) :
    InnerRegularWRT (map f μ) pb qb

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
pa qa : Set α → Prop
H : μ.InnerRegularWRT pa qa
f : α ≃ᵐ β
pb qb : Set β → Prop
hAB : ∀ (U : Set β), qb U → qa (⇑f ⁻¹' U)
hAB' : ∀ (K : Set α), pa K → pb (⇑f '' K)
U : Set β
hU : qb U
r : ℝ≥0∞
hr : r < (map (⇑f) μ) U
⊢ ∃ K ⊆ U, pb K ∧ r < (map (⇑f) μ) K

Tactic:
rw [f.map_apply U] at hr

Result:
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
pa qa : Set α → Prop
H : μ.InnerRegularWRT pa qa
f : α ≃ᵐ β
pb qb : Set β → Prop
hAB : ∀ (U : Set β), qb U → qa (⇑f ⁻¹' U)
hAB' : ∀ (K : Set α), pa K → pb (⇑f '' K)
U : Set β
hU : qb U
r : ℝ≥0∞
hr : r < μ (⇑f ⁻¹' U)
⊢ ∃ K ⊆ U, pb K ∧ r < (map (⇑f) μ) K

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
pa qa : Set α → Prop
H : μ.InnerRegularWRT pa qa
f : α ≃ᵐ β
pb qb : Set β → Prop
hAB : ∀ (U : Set β), qb U → qa (⇑f ⁻¹' U)
hAB' : ∀ (K : Set α), pa K → pb (⇑f '' K)
U : Set β
hU : qb U
r : ℝ≥0∞
hr : r < μ (⇑f ⁻¹' U)
⊢ ∃ K ⊆ U, pb K ∧ r < (map (⇑f) μ) K

Tactic:
rcases H (hAB U hU) r hr with ⟨K, hKU, hKc, hK⟩

Result:
case intro.intro.intro
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
pa qa : Set α → Prop
H : μ.InnerRegularWRT pa qa
f : α ≃ᵐ β
pb qb : Set β → Prop
hAB : ∀ (U : Set β), qb U → qa (⇑f ⁻¹' U)
hAB' : ∀ (K : Set α), pa K → pb (⇑f '' K)
U : Set β
hU : qb U
r : ℝ≥0∞
hr : r < μ (⇑f ⁻¹' U)
K : Set α
hKU : K ⊆ ⇑f ⁻¹' U
hKc : pa K
hK : r < μ K
⊢ ∃ K ⊆ U, pb K ∧ r < (map (⇑f) μ) K

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
pa qa : Set α → Prop
H : μ.InnerRegularWRT pa qa
f : α ≃ᵐ β
pb qb : Set β → Prop
hAB : ∀ (U : Set β), qb U → qa (⇑f ⁻¹' U)
hAB' : ∀ (K : Set α), pa K → pb (⇑f '' K)
⊢ (map (⇑f) μ).InnerRegularWRT pb qb

Tactic:
intro U hU r hr

Result:
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
pa qa : Set α → Prop
H : μ.InnerRegularWRT pa qa
f : α ≃ᵐ β
pb qb : Set β → Prop
hAB : ∀ (U : Set β), qb U → qa (⇑f ⁻¹' U)
hAB' : ∀ (K : Set α), pa K → pb (⇑f '' K)
U : Set β
hU : qb U
r : ℝ≥0∞
hr : r < (map (⇑f) μ) U
⊢ ∃ K ⊆ U, pb K ∧ r < (map (⇑f) μ) K

Proof state:
case intro.intro.intro
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
pa qa : Set α → Prop
H : μ.InnerRegularWRT pa qa
f : α ≃ᵐ β
pb qb : Set β → Prop
hAB : ∀ (U : Set β), qb U → qa (⇑f ⁻¹' U)
hAB' : ∀ (K : Set α), pa K → pb (⇑f '' K)
U : Set β
hU : qb U
r : ℝ≥0∞
hr : r < μ (⇑f ⁻¹' U)
K : Set α
hKU : K ⊆ ⇑f ⁻¹' U
hKc : pa K
hK : r < μ K
⊢ r < (map (⇑f) μ) (⇑f '' K)

Tactic:
rwa [f.map_apply, f.preimage_image]

Result:
no goals

Proof state:
case intro.intro.intro
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
pa qa : Set α → Prop
H : μ.InnerRegularWRT pa qa
f : α ≃ᵐ β
pb qb : Set β → Prop
hAB : ∀ (U : Set β), qb U → qa (⇑f ⁻¹' U)
hAB' : ∀ (K : Set α), pa K → pb (⇑f '' K)
U : Set β
hU : qb U
r : ℝ≥0∞
hr : r < μ (⇑f ⁻¹' U)
K : Set α
hKU : K ⊆ ⇑f ⁻¹' U
hKc : pa K
hK : r < μ K
⊢ ∃ K ⊆ U, pb K ∧ r < (map (⇑f) μ) K

Tactic:
refine ⟨f '' K, image_subset_iff.2 hKU, hAB' _ hKc, ?_⟩

Result:
case intro.intro.intro
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
pa qa : Set α → Prop
H : μ.InnerRegularWRT pa qa
f : α ≃ᵐ β
pb qb : Set β → Prop
hAB : ∀ (U : Set β), qb U → qa (⇑f ⁻¹' U)
hAB' : ∀ (K : Set α), pa K → pb (⇑f '' K)
U : Set β
hU : qb U
r : ℝ≥0∞
hr : r < μ (⇑f ⁻¹' U)
K : Set α
hKU : K ⊆ ⇑f ⁻¹' U
hKc : pa K
hK : r < μ K
⊢ r < (map (⇑f) μ) (⇑f '' K)