-- Mathlib/Topology/LocallyClosed.lean
nonrec
lemma Topology.IsInducing.isLocallyClosed_iff {s : Set X}
    {f : X → Y} (hf : IsInducing f) :
    IsLocallyClosed s ↔ ∃ s' : Set Y, IsLocallyClosed s' ∧ f ⁻¹' s' = s

Proof state:
case mp.intro.intro.intro.intro.intro.intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsInducing f
U : Set Y
hU : IsOpen U
Z : Set Y
hZ : IsClosed Z
⊢ ∃ s', (∃ U Z, IsOpen U ∧ IsClosed Z ∧ s' = U ∩ Z) ∧ f ⁻¹' s' = f ⁻¹' U ∩ f ⁻¹' Z

Tactic:
exact ⟨_, ⟨U, Z, hU, hZ, rfl⟩, rfl⟩

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : X → Y
hf : IsInducing f
⊢ IsLocallyClosed s ↔ ∃ s', IsLocallyClosed s' ∧ f ⁻¹' s' = s

Tactic:
simp_rw [IsLocallyClosed, hf.isOpen_iff, hf.isClosed_iff]

Result:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : X → Y
hf : IsInducing f
⊢ (∃ U Z, (∃ t, IsOpen t ∧ f ⁻¹' t = U) ∧ (∃ t, IsClosed t ∧ f ⁻¹' t = Z) ∧ s = U ∩ Z) ↔
    ∃ s', (∃ U Z, IsOpen U ∧ IsClosed Z ∧ s' = U ∩ Z) ∧ f ⁻¹' s' = s

Proof state:
case mpr
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : X → Y
hf : IsInducing f
⊢ (∃ s', (∃ U Z, IsOpen U ∧ IsClosed Z ∧ s' = U ∩ Z) ∧ f ⁻¹' s' = s) →
    ∃ U Z, (∃ t, IsOpen t ∧ f ⁻¹' t = U) ∧ (∃ t, IsClosed t ∧ f ⁻¹' t = Z) ∧ s = U ∩ Z

Tactic:
rintro ⟨_, ⟨U, Z, hU, hZ, rfl⟩, rfl⟩

Result:
case mpr.intro.intro.intro.intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsInducing f
U Z : Set Y
hU : IsOpen U
hZ : IsClosed Z
⊢ ∃ U_1 Z_1, (∃ t, IsOpen t ∧ f ⁻¹' t = U_1) ∧ (∃ t, IsClosed t ∧ f ⁻¹' t = Z_1) ∧ f ⁻¹' (U ∩ Z) = U_1 ∩ Z_1

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : X → Y
hf : IsInducing f
⊢ (∃ U Z, (∃ t, IsOpen t ∧ f ⁻¹' t = U) ∧ (∃ t, IsClosed t ∧ f ⁻¹' t = Z) ∧ s = U ∩ Z) ↔
    ∃ s', (∃ U Z, IsOpen U ∧ IsClosed Z ∧ s' = U ∩ Z) ∧ f ⁻¹' s' = s

Tactic:
constructor

Result:
case mp
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : X → Y
hf : IsInducing f
⊢ (∃ U Z, (∃ t, IsOpen t ∧ f ⁻¹' t = U) ∧ (∃ t, IsClosed t ∧ f ⁻¹' t = Z) ∧ s = U ∩ Z) →
    ∃ s', (∃ U Z, IsOpen U ∧ IsClosed Z ∧ s' = U ∩ Z) ∧ f ⁻¹' s' = s

case mpr
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : X → Y
hf : IsInducing f
⊢ (∃ s', (∃ U Z, IsOpen U ∧ IsClosed Z ∧ s' = U ∩ Z) ∧ f ⁻¹' s' = s) →
    ∃ U Z, (∃ t, IsOpen t ∧ f ⁻¹' t = U) ∧ (∃ t, IsClosed t ∧ f ⁻¹' t = Z) ∧ s = U ∩ Z

Proof state:
case mp
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : X → Y
hf : IsInducing f
⊢ (∃ U Z, (∃ t, IsOpen t ∧ f ⁻¹' t = U) ∧ (∃ t, IsClosed t ∧ f ⁻¹' t = Z) ∧ s = U ∩ Z) →
    ∃ s', (∃ U Z, IsOpen U ∧ IsClosed Z ∧ s' = U ∩ Z) ∧ f ⁻¹' s' = s

Tactic:
rintro ⟨_, _, ⟨U, hU, rfl⟩, ⟨Z, hZ, rfl⟩, rfl⟩

Result:
case mp.intro.intro.intro.intro.intro.intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsInducing f
U : Set Y
hU : IsOpen U
Z : Set Y
hZ : IsClosed Z
⊢ ∃ s', (∃ U Z, IsOpen U ∧ IsClosed Z ∧ s' = U ∩ Z) ∧ f ⁻¹' s' = f ⁻¹' U ∩ f ⁻¹' Z

Proof state:
case mpr.intro.intro.intro.intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsInducing f
U Z : Set Y
hU : IsOpen U
hZ : IsClosed Z
⊢ ∃ U_1 Z_1, (∃ t, IsOpen t ∧ f ⁻¹' t = U_1) ∧ (∃ t, IsClosed t ∧ f ⁻¹' t = Z_1) ∧ f ⁻¹' (U ∩ Z) = U_1 ∩ Z_1

Tactic:
exact ⟨_, _, ⟨U, hU, rfl⟩, ⟨Z, hZ, rfl⟩, rfl⟩

Result:
no goals