awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.LocalAtTarget
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set β
h : IsClosedEmbedding f
⊢ IsClosedEmbedding (s.restrictPreimage f)

Tactic:
⟨h.1.restrictPreimage s,
    (s.range_restrictPreimage f).symm ▸ IsInducing.subtypeVal.isClosed_preimage _ h.isClosed_range⟩

Premises used: Topology.IsInducing.isClosed_preimage, Set.range_restrictPreimage, Eq.rec, Topology.IsClosedEmbedding.toIsEmbedding, Topology.IsEmbedding.restrictPreimage, Eq.symm, Topology.IsClosedEmbedding.mk, Topology.IsClosedEmbedding.isClosed_range, Topology.IsInducing.subtypeVal
-- Module: Mathlib.Topology.LocalAtTarget
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
H : IsClosedMap f
s : Set β
t : Set (↑(f ⁻¹' s) : Type u_1)
this :
  ∀ (u : Set α),
    IsClosed[inst] u →
      Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' s) ⁻¹' u = t →
        ∃ (v : Set β), IsClosed[inst_1] v ∧ Subtype.val (p := fun (x : β) ↦ x ∈ s) ⁻¹' v = s.restrictPreimage f '' t
⊢ IsClosed[instTopologicalSpaceSubtype] t → IsClosed[instTopologicalSpaceSubtype] (s.restrictPreimage f '' t)

Tactic:
simpa [isClosed_induced_iff]

Premises used: isClosed_induced_iff
-- Module: Mathlib.Topology.LocalAtTarget
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
H : IsClosedMap f
s : Set β
t : Set (↑(f ⁻¹' s) : Type u_1)
suffices :
  ∀ (u : Set α),
    IsClosed[inst] u →
      Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' s) ⁻¹' u = t →
        ∃ (v : Set β), IsClosed[inst_1] v ∧ Subtype.val (p := fun (x : β) ↦ x ∈ s) ⁻¹' v = s.restrictPreimage f '' t
⊢ IsClosed[instTopologicalSpaceSubtype] t → IsClosed[instTopologicalSpaceSubtype] (s.restrictPreimage f '' t)

Tactic:
suffices ∀ u, IsClosed u → Subtype.val ⁻¹' u = t →
    ∃ v, IsClosed v ∧ Subtype.val ⁻¹' v = s.restrictPreimage f '' t by
      simpa [isClosed_induced_iff]
-- Module: Mathlib.Topology.LocalAtTarget
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
H : IsClosedMap f
s : Set β
t : Set (↑(f ⁻¹' s) : Type u_1)
u : Set α
hu : IsClosed[inst] u
e : Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' s) ⁻¹' u = t
⊢ Subtype.val (p := fun (x : β) ↦ x ∈ s) ⁻¹' f '' u = s.restrictPreimage f '' t

Tactic:
simp [← e, image_restrictPreimage]

Premises used: Set.image_restrictPreimage
-- Module: Mathlib.Topology.LocalAtTarget
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
H : IsClosedMap f
s : Set β
t : Set (↑(f ⁻¹' s) : Type u_1)
⊢ ∀ (u : Set α),
    IsClosed[inst] u →
      Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' s) ⁻¹' u = t →
        ∃ (v : Set β), IsClosed[inst_1] v ∧ Subtype.val (p := fun (x : β) ↦ x ∈ s) ⁻¹' v = s.restrictPreimage f '' t

Tactic:
exact fun u hu e => ⟨f '' u, H u hu, by simp [← e, image_restrictPreimage]⟩
-- Module: Mathlib.Topology.LocalAtTarget
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
H : IsOpenMap f
s : Set β
t : Set (↑(f ⁻¹' s) : Type u_1)
this :
  ∀ (u : Set α),
    IsOpen[inst] u →
      Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' s) ⁻¹' u = t →
        ∃ (v : Set β), IsOpen[inst_1] v ∧ Subtype.val (p := fun (x : β) ↦ x ∈ s) ⁻¹' v = s.restrictPreimage f '' t
⊢ IsOpen[instTopologicalSpaceSubtype] t → IsOpen[instTopologicalSpaceSubtype] (s.restrictPreimage f '' t)

Tactic:
simpa [isOpen_induced_iff]

Premises used: isOpen_induced_iff
-- Module: Mathlib.Topology.LocalAtTarget
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
H : IsOpenMap f
s : Set β
t : Set (↑(f ⁻¹' s) : Type u_1)
suffices :
  ∀ (u : Set α),
    IsOpen[inst] u →
      Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' s) ⁻¹' u = t →
        ∃ (v : Set β), IsOpen[inst_1] v ∧ Subtype.val (p := fun (x : β) ↦ x ∈ s) ⁻¹' v = s.restrictPreimage f '' t
⊢ IsOpen[instTopologicalSpaceSubtype] t → IsOpen[instTopologicalSpaceSubtype] (s.restrictPreimage f '' t)

Tactic:
suffices ∀ u, IsOpen u → Subtype.val ⁻¹' u = t →
    ∃ v, IsOpen v ∧ Subtype.val ⁻¹' v = s.restrictPreimage f '' t by
      simpa [isOpen_induced_iff]
-- Module: Mathlib.Topology.LocalAtTarget
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
H : IsOpenMap f
s : Set β
t : Set (↑(f ⁻¹' s) : Type u_1)
u : Set α
hu : IsOpen[inst] u
e : Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' s) ⁻¹' u = t
⊢ Subtype.val (p := fun (x : β) ↦ x ∈ s) ⁻¹' f '' u = s.restrictPreimage f '' t

Tactic:
simp [← e, image_restrictPreimage]

Premises used: Set.image_restrictPreimage
-- Module: Mathlib.Topology.LocalAtTarget
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
H : IsOpenMap f
s : Set β
t : Set (↑(f ⁻¹' s) : Type u_1)
⊢ ∀ (u : Set α),
    IsOpen[inst] u →
      Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' s) ⁻¹' u = t →
        ∃ (v : Set β), IsOpen[inst_1] v ∧ Subtype.val (p := fun (x : β) ↦ x ∈ s) ⁻¹' v = s.restrictPreimage f '' t

Tactic:
exact fun u hu e => ⟨f '' u, H u hu, by simp [← e, image_restrictPreimage]⟩
-- Module: Mathlib.Topology.LocalAtTarget
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
H : GeneralizingMap f
s : Set β
x : (↑(f ⁻¹' s) : Type u_1)
y : (↑s : Type u_2)
h : y ⤳ s.restrictPreimage f x
obtain :
  ∀ (a : α) (ha : a ⤳ (↑x : α)) (hy : f a = (↑y : β)),
    ∃ (a' : (↑(f ⁻¹' s) : Type u_1)),
      (fun (x1 x2 : (↑(f ⁻¹' s) : Type u_1)) ↦ x1 ⤳ x2) a' x ∧ s.restrictPreimage f a' = y
⊢ ∃ (a' : (↑(f ⁻¹' s) : Type u_1)), (fun (x1 x2 : (↑(f ⁻¹' s) : Type u_1)) ↦ x1 ⤳ x2) a' x ∧ s.restrictPreimage f a' = y

Tactic:
obtain ⟨a, ha, hy⟩ := H (h.map <| continuous_subtype_val (p := (· ∈ s)))

Premises used: continuous_subtype_val, Specializes.map
-- Module: Mathlib.Topology.LocalAtTarget
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
H : GeneralizingMap f
s : Set β
x : (↑(f ⁻¹' s) : Type u_1)
y : (↑s : Type u_2)
h : y ⤳ s.restrictPreimage f x
a : α
ha : a ⤳ (↑x : α)
hy : f a = (↑y : β)
⊢ a ∈ f ⁻¹' s

Tactic:
simp [hy]
-- Module: Mathlib.Topology.LocalAtTarget
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
H : GeneralizingMap f
s : Set β
x : (↑(f ⁻¹' s) : Type u_1)
y : (↑s : Type u_2)
h : y ⤳ s.restrictPreimage f x
a : α
ha : a ⤳ (↑x : α)
hy : f a = (↑y : β)
h₁ :
  (fun (x1 x2 : (↑(f ⁻¹' s) : Type u_1)) ↦ x1 ⤳ x2) (Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' s) a ⋯) x ∧
    s.restrictPreimage f (Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' s) a ⋯) = y
⊢ ∃ (a' : (↑(f ⁻¹' s) : Type u_1)), (fun (x1 x2 : (↑(f ⁻¹' s) : Type u_1)) ↦ x1 ⤳ x2) a' x ∧ s.restrictPreimage f a' = y

Tactic:
use ⟨a, by simp [hy]⟩
-- Module: Mathlib.Topology.LocalAtTarget
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
H : GeneralizingMap f
s : Set β
x : (↑(f ⁻¹' s) : Type u_1)
y : (↑s : Type u_2)
h : y ⤳ s.restrictPreimage f x
a : α
ha : a ⤳ (↑x : α)
hy : f a = (↑y : β)
⊢ (fun (x1 x2 : (↑(f ⁻¹' s) : Type u_1)) ↦ x1 ⤳ x2) (Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' s) a ⋯) x ∧
    s.restrictPreimage f (Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' s) a ⋯) = y

Tactic:
simp [hy, subtype_specializes_iff, ha]

Premises used: subtype_specializes_iff
-- Module: Mathlib.Topology.LocalAtTarget
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
H : IsProperMap f
s : Set β
rw :
  Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] (s.restrictPreimage f) ∧
    IsClosedMap (s.restrictPreimage f) ∧ ∀ (y : (↑s : Type u_2)), IsCompact (s.restrictPreimage f ⁻¹' {y})
⊢ IsProperMap (s.restrictPreimage f)

Tactic:
rw [isProperMap_iff_isClosedMap_and_compact_fibers]

Premises used: isProperMap_iff_isClosedMap_and_compact_fibers
-- Module: Mathlib.Topology.LocalAtTarget
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
H : IsProperMap f
s : Set β
⊢ Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] (s.restrictPreimage f) ∧
    IsClosedMap (s.restrictPreimage f) ∧ ∀ (y : (↑s : Type u_2)), IsCompact (s.restrictPreimage f ⁻¹' {y})

Tactic:
⟨H.continuous.restrictPreimage, H.isClosedMap.restrictPreimage _, fun y ↦ ?_⟩

Premises used: IsProperMap.isClosedMap, IsClosedMap.restrictPreimage, And.intro, IsProperMap.continuous, Continuous.restrictPreimage
-- Module: Mathlib.Topology.LocalAtTarget
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
H : IsProperMap f
s : Set β
refine : ∀ (y : (↑s : Type u_2)), IsCompact (s.restrictPreimage f ⁻¹' {y})
⊢ Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] (s.restrictPreimage f) ∧
    IsClosedMap (s.restrictPreimage f) ∧ ∀ (y : (↑s : Type u_2)), IsCompact (s.restrictPreimage f ⁻¹' {y})

Tactic:
refine ⟨H.continuous.restrictPreimage, H.isClosedMap.restrictPreimage _, fun y ↦ ?_⟩
-- Module: Mathlib.Topology.LocalAtTarget
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
H : IsProperMap f
s : Set β
y : (↑s : Type u_2)
rw : IsCompact (f ⁻¹' {(↑y : β)})
⊢ IsCompact (s.restrictPreimage f ⁻¹' {y})

Tactic:
rw [IsEmbedding.subtypeVal.isCompact_iff, image_val_preimage_restrictPreimage, image_singleton]

Premises used: Set.image_singleton, Topology.IsEmbedding.isCompact_iff, Topology.IsEmbedding.subtypeVal, Set.image_val_preimage_restrictPreimage
-- Module: Mathlib.Topology.LocalAtTarget
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
H : IsProperMap f
s : Set β
y : (↑s : Type u_2)
⊢ IsCompact (f ⁻¹' {(↑y : β)})

Tactic:
H.isCompact_preimage isCompact_singleton

Premises used: IsProperMap.isCompact_preimage, isCompact_singleton
-- Module: Mathlib.Topology.LocalAtTarget
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
H : IsProperMap f
s : Set β
y : (↑s : Type u_2)
⊢ IsCompact (f ⁻¹' {(↑y : β)})

Tactic:
exact H.isCompact_preimage isCompact_singleton

Premises used: IsProperMap.isCompact_preimage, isCompact_singleton
-- Module: Mathlib.Topology.LocalAtTarget
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
H : IsOpenQuotientMap f
s : Set β
⊢ IsOpenQuotientMap (s.restrictPreimage f)

Tactic:
⟨H.surjective.restrictPreimage _, H.continuous.restrictPreimage, H.isOpenMap.restrictPreimage _⟩

Premises used: IsOpenQuotientMap.continuous, IsOpenMap.restrictPreimage, IsOpenQuotientMap.mk, IsOpenQuotientMap.surjective, Function.Surjective.restrictPreimage, IsOpenQuotientMap.isOpenMap, Continuous.restrictPreimage
-- Module: Mathlib.Topology.LocalAtTarget
Goal:
β : Type u_2
inst : TopologicalSpace β
ι : Type u_3
U : ι → Opens β
s : Set β
hU : IsOpenCover U
mp : IsOpen[inst] s → ∀ (i : ι), IsOpen[inst] (s ∩ (↑(U i) : Set β))
mpr : (∀ (i : ι), IsOpen[inst] (s ∩ (↑(U i) : Set β))) → IsOpen[inst] s
⊢ IsOpen[inst] s ↔ ∀ (i : ι), IsOpen[inst] (s ∩ (↑(U i) : Set β))

Tactic:
constructor
-- Module: Mathlib.Topology.LocalAtTarget
Goal:
β : Type u_2
inst : TopologicalSpace β
ι : Type u_3
U : ι → Opens β
s : Set β
hU : IsOpenCover U
⊢ IsOpen[inst] s → ∀ (i : ι), IsOpen[inst] (s ∩ (↑(U i) : Set β))

Tactic:
fun H i ↦ H.inter (U i).isOpen

Premises used: TopologicalSpace.Opens.isOpen, IsOpen.inter
-- Module: Mathlib.Topology.LocalAtTarget
Goal:
β : Type u_2
inst : TopologicalSpace β
ι : Type u_3
U : ι → Opens β
s : Set β
hU : IsOpenCover U
⊢ IsOpen[inst] s → ∀ (i : ι), IsOpen[inst] (s ∩ (↑(U i) : Set β))

Tactic:
exact fun H i ↦ H.inter (U i).isOpen
-- Module: Mathlib.Topology.LocalAtTarget
Goal:
β : Type u_2
inst : TopologicalSpace β
ι : Type u_3
U : ι → Opens β
s : Set β
hU : IsOpenCover U
H : ∀ (i : ι), IsOpen[inst] (s ∩ (↑(U i) : Set β))
⊢ IsOpen[inst] s

Tactic:
simpa [← inter_iUnion, hU.iSup_set_eq_univ] using isOpen_iUnion H

Premises used: TopologicalSpace.IsOpenCover.iSup_set_eq_univ, isOpen_iUnion, Set.inter_iUnion
-- Module: Mathlib.Topology.LocalAtTarget
Goal:
β : Type u_2
inst : TopologicalSpace β
ι : Type u_3
U : ι → Opens β
s : Set β
hU : IsOpenCover U
⊢ IsOpen[inst] s ↔ ∀ (i : ι), IsOpen[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x : β) ↦ x ∈ U i) ⁻¹' s)

Tactic:
simp [hU.isOpen_iff_inter (s := s), (U _).2.isOpenEmbedding_subtypeVal.isOpen_iff_image_isOpen,
    image_preimage_eq_inter_range]

Premises used: IsOpen.isOpenEmbedding_subtypeVal, Topology.IsOpenEmbedding.isOpen_iff_image_isOpen, Set.image_preimage_eq_inter_range, TopologicalSpace.Opens.is_open', TopologicalSpace.IsOpenCover.isOpen_iff_inter
-- Module: Mathlib.Topology.LocalAtTarget
Goal:
β : Type u_2
inst : TopologicalSpace β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
s : Set β
⊢ IsClosed[inst] s ↔ ∀ (i : ι), IsClosed[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x : β) ↦ x ∈ U i) ⁻¹' s)

Tactic:
simpa using hU.isOpen_iff_coe_preimage (s := sᶜ)

Premises used: TopologicalSpace.IsOpenCover.isOpen_iff_coe_preimage
-- Module: Mathlib.Topology.LocalAtTarget
Goal:
β : Type u_2
inst : TopologicalSpace β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
s : Set β
⊢ ∀ (i : ι),
    Eq (α := Set ↥(U i)) (coborder (Subtype.val (p := fun (x : β) ↦ x ∈ U i) ⁻¹' s))
      (Subtype.val (p := fun (x : β) ↦ x ∈ U i) ⁻¹' coborder s)

Tactic:
have (i : _) : coborder ((↑) ⁻¹' s : Set (U i)) = Subtype.val ⁻¹' coborder s :=
    (U i).isOpen.isOpenEmbedding_subtypeVal.coborder_preimage _
-- Module: Mathlib.Topology.LocalAtTarget
Goal:
β : Type u_2
inst : TopologicalSpace β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
s : Set β
this :
  ∀ (i : ι),
    Eq (α := Set ↥(U i)) (coborder (Subtype.val (p := fun (x : β) ↦ x ∈ U i) ⁻¹' s))
      (Subtype.val (p := fun (x : β) ↦ x ∈ U i) ⁻¹' coborder s)
⊢ IsLocallyClosed s ↔ ∀ (i : ι), IsLocallyClosed (X := ↥(U i)) (Subtype.val (p := fun (x : β) ↦ x ∈ U i) ⁻¹' s)

Tactic:
simp [isLocallyClosed_iff_isOpen_coborder, hU.isOpen_iff_coe_preimage, this]

Premises used: TopologicalSpace.IsOpenCover.isOpen_iff_coe_preimage, isLocallyClosed_iff_isOpen_coborder
-- Module: Mathlib.Topology.LocalAtTarget
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
⊢ IsOpenMap f ↔ ∀ (i : ι), IsOpenMap ((U i).carrier.restrictPreimage f)

Tactic:
⟨fun h i ↦ h.restrictPreimage _, fun H s hs ↦ ?_⟩

Premises used: IsOpenMap.restrictPreimage, TopologicalSpace.Opens.carrier, Iff.intro
-- Module: Mathlib.Topology.LocalAtTarget
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
refine :
  ∀ (H : ∀ (i : ι), IsOpenMap ((U i).carrier.restrictPreimage f)) (s : Set α) (hs : IsOpen[inst] s),
    IsOpen[inst_1] (f '' s)
⊢ IsOpenMap f ↔ ∀ (i : ι), IsOpenMap ((U i).carrier.restrictPreimage f)

Tactic:
refine ⟨fun h i ↦ h.restrictPreimage _, fun H s hs ↦ ?_⟩
-- Module: Mathlib.Topology.LocalAtTarget
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
H : ∀ (i : ι), IsOpenMap ((U i).carrier.restrictPreimage f)
s : Set α
hs : IsOpen[inst] s
rw : ∀ (i : ι), IsOpen[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x : β) ↦ x ∈ U i) ⁻¹' f '' s)
⊢ IsOpen[inst_1] (f '' s)

Tactic:
rw [hU.isOpen_iff_coe_preimage]

Premises used: TopologicalSpace.IsOpenCover.isOpen_iff_coe_preimage
-- Module: Mathlib.Topology.LocalAtTarget
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
H : ∀ (i : ι), IsOpenMap ((U i).carrier.restrictPreimage f)
s : Set α
hs : IsOpen[inst] s
i : ι
⊢ IsOpen[instTopologicalSpaceSubtype]
    ((U i).carrier.restrictPreimage f '' Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' (U i).carrier) ⁻¹' s)

Tactic:
H i _ (hs.preimage continuous_subtype_val)

Premises used: continuous_subtype_val, IsOpen.preimage
-- Module: Mathlib.Topology.LocalAtTarget
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
H : ∀ (i : ι), IsOpenMap ((U i).carrier.restrictPreimage f)
s : Set α
hs : IsOpen[inst] s
i : ι
h :
  ↥(U i) = (↑(U i).carrier : Type u_2) →
    Subtype.val (p := fun (x : β) ↦ x ∈ U i) ⁻¹' f '' s =
      (U i).carrier.restrictPreimage f '' Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' (U i).carrier) ⁻¹' s
⊢ IsOpen[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x : β) ↦ x ∈ U i) ⁻¹' f '' s)

Tactic:
convert! H i _ (hs.preimage continuous_subtype_val)

Premises used: continuous_subtype_val, IsOpen.preimage
-- Module: Mathlib.Topology.LocalAtTarget
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
H : ∀ (i : ι), IsOpenMap ((U i).carrier.restrictPreimage f)
s : Set α
hs : IsOpen[inst] s
i : ι
e_1 : ↥(U i) = (↑(U i).carrier : Type u_2)
h :
  ∀ (x : β) (hx : x ∈ U i),
    Membership.mem (γ := Set ↥(U i)) (Subtype.val (p := fun (x : β) ↦ x ∈ U i) ⁻¹' f '' s)
        (Subtype.mk (p := fun (x : β) ↦ x ∈ U i) x hx) ↔
      Subtype.mk (p := fun (x : β) ↦ x ∈ U i) x hx ∈
        (U i).carrier.restrictPreimage f '' Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' (U i).carrier) ⁻¹' s
⊢ Subtype.val (p := fun (x : β) ↦ x ∈ U i) ⁻¹' f '' s =
    (U i).carrier.restrictPreimage f '' Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' (U i).carrier) ⁻¹' s

Tactic:
ext ⟨x, hx⟩
-- Module: Mathlib.Topology.LocalAtTarget
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
H : ∀ (i : ι), IsOpenMap ((U i).carrier.restrictPreimage f)
s : Set α
hs : IsOpen[inst] s
i : ι
e_1 : ↥(U i) = (↑(U i).carrier : Type u_2)
x : β
hx : x ∈ U i
this : (∃ y ∈ s, f y = x) ↔ ∃ y ∈ s, f y ∈ U i ∧ f y = x
⊢ Membership.mem (γ := Set ↥(U i)) (Subtype.val (p := fun (x : β) ↦ x ∈ U i) ⁻¹' f '' s)
      (Subtype.mk (p := fun (x : β) ↦ x ∈ U i) x hx) ↔
    Subtype.mk (p := fun (x : β) ↦ x ∈ U i) x hx ∈
      (U i).carrier.restrictPreimage f '' Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' (U i).carrier) ⁻¹' s

Tactic:
simpa [← Subtype.coe_inj]

Premises used: Subtype.coe_inj
-- Module: Mathlib.Topology.LocalAtTarget
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
H : ∀ (i : ι), IsOpenMap ((U i).carrier.restrictPreimage f)
s : Set α
hs : IsOpen[inst] s
i : ι
e_1 : ↥(U i) = (↑(U i).carrier : Type u_2)
x : β
hx : x ∈ U i
h : (∃ y ∈ s, f y = x) ↔ ∃ y ∈ s, f y ∈ U i ∧ f y = x
⊢ Membership.mem (γ := Set ↥(U i)) (Subtype.val (p := fun (x : β) ↦ x ∈ U i) ⁻¹' f '' s)
      (Subtype.mk (p := fun (x : β) ↦ x ∈ U i) x hx) ↔
    Subtype.mk (p := fun (x : β) ↦ x ∈ U i) x hx ∈
      (U i).carrier.restrictPreimage f '' Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' (U i).carrier) ⁻¹' s

Tactic:
suffices (∃ y, y ∈ s ∧ f y = x) ↔ ∃ y, y ∈ s ∧ f y ∈ U i ∧ f y = x by simpa [← Subtype.coe_inj]
-- Module: Mathlib.Topology.LocalAtTarget
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
H : ∀ (i : ι), IsOpenMap ((U i).carrier.restrictPreimage f)
s : Set α
hs : IsOpen[inst] s
i : ι
e_1 : ↥(U i) = (↑(U i).carrier : Type u_2)
x : β
hx : x ∈ U i
tauto tauto₁ tauto₂ tauto₃ tauto₄ tauto₅ tauto₆ tauto₇ : ∀ w ∈ s, f w ∈ U i → f w = x → ∃ y ∈ s, f y = x
⊢ (∃ y ∈ s, f y ∈ U i ∧ f y = x) → ∃ y ∈ s, f y = x

Tactic:
tauto
-- Module: Mathlib.Topology.LocalAtTarget
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
H : ∀ (i : ι), IsOpenMap ((U i).carrier.restrictPreimage f)
s : Set α
hs : IsOpen[inst] s
i : ι
e_1 : ↥(U i) = (↑(U i).carrier : Type u_2)
x : β
hx : x ∈ U i
⊢ (∃ y ∈ s, f y = x) ↔ ∃ y ∈ s, f y ∈ U i ∧ f y = x

Tactic:
exact ⟨fun ⟨a, b, c⟩ ↦ ⟨a, b, c.symm ▸ hx, c⟩, by tauto⟩
-- Module: Mathlib.Topology.LocalAtTarget
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
⊢ IsClosedMap f ↔ ∀ (i : ι), IsClosedMap ((U i).carrier.restrictPreimage f)

Tactic:
⟨fun h i => h.restrictPreimage _, fun H s hs ↦ ?_⟩

Premises used: IsClosedMap.restrictPreimage, TopologicalSpace.Opens.carrier, Iff.intro
-- Module: Mathlib.Topology.LocalAtTarget
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
refine :
  ∀ (H : ∀ (i : ι), IsClosedMap ((U i).carrier.restrictPreimage f)) (s : Set α) (hs : IsClosed[inst] s),
    IsClosed[inst_1] (f '' s)
⊢ IsClosedMap f ↔ ∀ (i : ι), IsClosedMap ((U i).carrier.restrictPreimage f)

Tactic:
refine ⟨fun h i => h.restrictPreimage _, fun H s hs ↦ ?_⟩
-- Module: Mathlib.Topology.LocalAtTarget
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
H : ∀ (i : ι), IsClosedMap ((U i).carrier.restrictPreimage f)
s : Set α
hs : IsClosed[inst] s
rw : ∀ (i : ι), IsClosed[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x : β) ↦ x ∈ U i) ⁻¹' f '' s)
⊢ IsClosed[inst_1] (f '' s)

Tactic:
rw [hU.isClosed_iff_coe_preimage]

Premises used: TopologicalSpace.IsOpenCover.isClosed_iff_coe_preimage
-- Module: Mathlib.Topology.LocalAtTarget
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
H : ∀ (i : ι), IsClosedMap ((U i).carrier.restrictPreimage f)
s : Set α
hs : IsClosed[inst] s
i : ι
⊢ IsClosed[instTopologicalSpaceSubtype]
    ((U i).carrier.restrictPreimage f '' (Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' (U i).carrier) ⁻¹' sᶜ)ᶜ)

Tactic:
H i _ ⟨⟨_, hs.1, eq_compl_comm.mpr rfl⟩⟩

Premises used: Iff.mpr, IsClosed.isOpen_compl, And.intro, Exists.intro, IsClosed.mk, rfl, eq_compl_comm
-- Module: Mathlib.Topology.LocalAtTarget
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
H : ∀ (i : ι), IsClosedMap ((U i).carrier.restrictPreimage f)
s : Set α
hs : IsClosed[inst] s
i : ι
h :
  ↥(U i) = (↑(U i).carrier : Type u_2) →
    Subtype.val (p := fun (x : β) ↦ x ∈ U i) ⁻¹' f '' s =
      (U i).carrier.restrictPreimage f '' (Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' (U i).carrier) ⁻¹' sᶜ)ᶜ
⊢ IsClosed[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x : β) ↦ x ∈ U i) ⁻¹' f '' s)

Tactic:
convert! H i _ ⟨⟨_, hs.1, eq_compl_comm.mpr rfl⟩⟩

Premises used: Iff.mpr, IsClosed.isOpen_compl, And.intro, Exists.intro, IsClosed.mk, rfl, eq_compl_comm
-- Module: Mathlib.Topology.LocalAtTarget
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
H : ∀ (i : ι), IsClosedMap ((U i).carrier.restrictPreimage f)
s : Set α
hs : IsClosed[inst] s
i : ι
e_1 : ↥(U i) = (↑(U i).carrier : Type u_2)
h :
  ∀ (x : β) (hx : x ∈ U i),
    Membership.mem (γ := Set ↥(U i)) (Subtype.val (p := fun (x : β) ↦ x ∈ U i) ⁻¹' f '' s)
        (Subtype.mk (p := fun (x : β) ↦ x ∈ U i) x hx) ↔
      Subtype.mk (p := fun (x : β) ↦ x ∈ U i) x hx ∈
        (U i).carrier.restrictPreimage f '' (Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' (U i).carrier) ⁻¹' sᶜ)ᶜ
⊢ Subtype.val (p := fun (x : β) ↦ x ∈ U i) ⁻¹' f '' s =
    (U i).carrier.restrictPreimage f '' (Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' (U i).carrier) ⁻¹' sᶜ)ᶜ

Tactic:
ext ⟨x, hx⟩