-- Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean
theorem measurable_of_isClosed {f : δ → γ} (hf : ∀ s, IsClosed s → MeasurableSet (f ⁻¹' s)) :
    Measurable f

Proof state:
case hf
γ : Type u_3
δ : Type u_5
inst✝³ : TopologicalSpace γ
inst✝² : MeasurableSpace γ
inst✝¹ : BorelSpace γ
inst✝ : MeasurableSpace δ
f : δ → γ
hf : ∀ (s : Set γ), IsClosed s → MeasurableSet (f ⁻¹' s)
⊢ ∀ (s : Set γ), IsOpen s → MeasurableSet (f ⁻¹' s)

Tactic:
intro s hs

Result:
case hf
γ : Type u_3
δ : Type u_5
inst✝³ : TopologicalSpace γ
inst✝² : MeasurableSpace γ
inst✝¹ : BorelSpace γ
inst✝ : MeasurableSpace δ
f : δ → γ
hf : ∀ (s : Set γ), IsClosed s → MeasurableSet (f ⁻¹' s)
s : Set γ
hs : IsOpen s
⊢ MeasurableSet (f ⁻¹' s)

Proof state:
case hf
γ : Type u_3
δ : Type u_5
inst✝³ : TopologicalSpace γ
inst✝² : MeasurableSpace γ
inst✝¹ : BorelSpace γ
inst✝ : MeasurableSpace δ
f : δ → γ
hf : ∀ (s : Set γ), IsClosed s → MeasurableSet (f ⁻¹' s)
s : Set γ
hs : IsOpen s
⊢ MeasurableSet (f ⁻¹' s)

Tactic:
rw [← MeasurableSet.compl_iff, ← preimage_compl]

Result:
case hf
γ : Type u_3
δ : Type u_5
inst✝³ : TopologicalSpace γ
inst✝² : MeasurableSpace γ
inst✝¹ : BorelSpace γ
inst✝ : MeasurableSpace δ
f : δ → γ
hf : ∀ (s : Set γ), IsClosed s → MeasurableSet (f ⁻¹' s)
s : Set γ
hs : IsOpen s
⊢ MeasurableSet (f ⁻¹' sᶜ)

Proof state:
γ : Type u_3
δ : Type u_5
inst✝³ : TopologicalSpace γ
inst✝² : MeasurableSpace γ
inst✝¹ : BorelSpace γ
inst✝ : MeasurableSpace δ
f : δ → γ
hf : ∀ (s : Set γ), IsClosed s → MeasurableSet (f ⁻¹' s)
⊢ Measurable f

Tactic:
apply measurable_of_isOpen

Result:
case hf
γ : Type u_3
δ : Type u_5
inst✝³ : TopologicalSpace γ
inst✝² : MeasurableSpace γ
inst✝¹ : BorelSpace γ
inst✝ : MeasurableSpace δ
f : δ → γ
hf : ∀ (s : Set γ), IsClosed s → MeasurableSet (f ⁻¹' s)
⊢ ∀ (s : Set γ), IsOpen s → MeasurableSet (f ⁻¹' s)

Proof state:
case hf
γ : Type u_3
δ : Type u_5
inst✝³ : TopologicalSpace γ
inst✝² : MeasurableSpace γ
inst✝¹ : BorelSpace γ
inst✝ : MeasurableSpace δ
f : δ → γ
hf : ∀ (s : Set γ), IsClosed s → MeasurableSet (f ⁻¹' s)
s : Set γ
hs : IsOpen s
⊢ MeasurableSet (f ⁻¹' sᶜ)

Tactic:
apply hf

Result:
case hf.a
γ : Type u_3
δ : Type u_5
inst✝³ : TopologicalSpace γ
inst✝² : MeasurableSpace γ
inst✝¹ : BorelSpace γ
inst✝ : MeasurableSpace δ
f : δ → γ
hf : ∀ (s : Set γ), IsClosed s → MeasurableSet (f ⁻¹' s)
s : Set γ
hs : IsOpen s
⊢ IsClosed sᶜ

Proof state:
case hf.a
γ : Type u_3
δ : Type u_5
inst✝³ : TopologicalSpace γ
inst✝² : MeasurableSpace γ
inst✝¹ : BorelSpace γ
inst✝ : MeasurableSpace δ
f : δ → γ
hf : ∀ (s : Set γ), IsClosed s → MeasurableSet (f ⁻¹' s)
s : Set γ
hs : IsOpen s
⊢ IsOpen s

Tactic:
exact hs

Result:
no goals

Proof state:
case hf.a
γ : Type u_3
δ : Type u_5
inst✝³ : TopologicalSpace γ
inst✝² : MeasurableSpace γ
inst✝¹ : BorelSpace γ
inst✝ : MeasurableSpace δ
f : δ → γ
hf : ∀ (s : Set γ), IsClosed s → MeasurableSet (f ⁻¹' s)
s : Set γ
hs : IsOpen s
⊢ IsClosed sᶜ

Tactic:
rw [isClosed_compl_iff]

Result:
case hf.a
γ : Type u_3
δ : Type u_5
inst✝³ : TopologicalSpace γ
inst✝² : MeasurableSpace γ
inst✝¹ : BorelSpace γ
inst✝ : MeasurableSpace δ
f : δ → γ
hf : ∀ (s : Set γ), IsClosed s → MeasurableSet (f ⁻¹' s)
s : Set γ
hs : IsOpen s
⊢ IsOpen s