awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
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 : ι), IsClosedMap ((U i).carrier.restrictPreimage f)
s : Set α
hs : IsClosed[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 : ι), IsClosedMap ((U i).carrier.restrictPreimage f)
s : Set α
hs : IsClosed[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 : ι), IsClosedMap ((U i).carrier.restrictPreimage f)
s : Set α
hs : IsClosed[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
h : Continuous[inst, inst_1] f
simp_rw :
  (∀ (x : α), 𝓝 x = Filter.comap f (𝓝 (f x))) ↔
    ∀ (i : ι) (x : (↑(f ⁻¹' (U i).carrier) : Type u_1)),
      𝓝 x =
        Filter.comap (Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' (U i).carrier))
          (Filter.comap f (𝓝 ((f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' (U i).carrier)) x)))
⊢ IsInducing f ↔ ∀ (i : ι), IsInducing ((U i).carrier.restrictPreimage f)

Tactic:
simp_rw [← IsInducing.subtypeVal.of_comp_iff, isInducing_iff_nhds, restrictPreimage,
    MapsTo.coe_restrict, restrict_eq, ← Filter.comap_comap]

Premises used: Set.restrictPreimage, Set.MapsTo.coe_restrict, Topology.IsInducing.of_comp_iff, Topology.isInducing_iff_nhds, Filter.comap_comap, Set.restrict_eq, Topology.IsInducing.subtypeVal
-- 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 : Continuous[inst, inst_1] f
mp :
  (∀ (x : α), 𝓝 x = Filter.comap f (𝓝 (f x))) →
    ∀ (i : ι) (x : (↑(f ⁻¹' (U i).carrier) : Type u_1)),
      𝓝 x =
        Filter.comap (Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' (U i).carrier))
          (Filter.comap f (𝓝 ((f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' (U i).carrier)) x)))
mpr :
  (∀ (i : ι) (x : (↑(f ⁻¹' (U i).carrier) : Type u_1)),
      𝓝 x =
        Filter.comap (Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' (U i).carrier))
          (Filter.comap f (𝓝 ((f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' (U i).carrier)) x)))) →
    ∀ (x : α), 𝓝 x = Filter.comap f (𝓝 (f x))
⊢ (∀ (x : α), 𝓝 x = Filter.comap f (𝓝 (f x))) ↔
    ∀ (i : ι) (x : (↑(f ⁻¹' (U i).carrier) : Type u_1)),
      𝓝 x =
        Filter.comap (Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' (U i).carrier))
          (Filter.comap f (𝓝 ((f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' (U i).carrier)) x)))

Tactic:
constructor
-- 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 : Continuous[inst, inst_1] f
H : ∀ (x : α), 𝓝 x = Filter.comap f (𝓝 (f x))
i : ι
x : (↑(f ⁻¹' (U i).carrier) : Type u_1)
mp : 𝓝 x = Filter.comap (Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' (U i).carrier)) (Filter.comap f (𝓝 (f (↑x : α))))
mp₁ : 𝓝 x = Filter.comap (Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' (U i).carrier)) (𝓝 (↑x : α))
mp₂ mp₃ : 𝓝 x = 𝓝 x
⊢ 𝓝 x =
    Filter.comap (Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' (U i).carrier))
      (Filter.comap f (𝓝 ((f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' (U i).carrier)) x)))

Tactic:
rw [Function.comp_apply, ← H, ← IsInducing.subtypeVal.nhds_eq_comap]

Premises used: Topology.IsInducing.nhds_eq_comap, Function.comp_apply, Topology.IsInducing.subtypeVal
-- 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 : Continuous[inst, inst_1] f
H :
  ∀ (i : ι) (x : (↑(f ⁻¹' (U i).carrier) : Type u_1)),
    𝓝 x =
      Filter.comap (Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' (U i).carrier))
        (Filter.comap f (𝓝 ((f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' (U i).carrier)) x)))
x : α
⊢ f x ∈ iSup U

Tactic:
simp [hU.iSup_eq_top]

Premises used: TopologicalSpace.IsOpenCover.iSup_eq_top
-- 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 : Continuous[inst, inst_1] f
H :
  ∀ (i : ι) (x : (↑(f ⁻¹' (U i).carrier) : Type u_1)),
    𝓝 x =
      Filter.comap (Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' (U i).carrier))
        (Filter.comap f (𝓝 ((f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' (U i).carrier)) x)))
x : α
mpr : ∀ (i : ι) (hi : f x ∈ U i), 𝓝 x = Filter.comap f (𝓝 (f x))
⊢ 𝓝 x = Filter.comap f (𝓝 (f x))

Tactic:
obtain ⟨i, hi⟩ := Opens.mem_iSup.mp (show f x ∈ iSup U by simp [hU.iSup_eq_top])

Premises used: TopologicalSpace.Opens.mem_iSup, Iff.mp
-- 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 : Continuous[inst, inst_1] f
H :
  ∀ (i : ι) (x : (↑(f ⁻¹' (U i).carrier) : Type u_1)),
    𝓝 x =
      Filter.comap (Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' (U i).carrier))
        (Filter.comap f (𝓝 ((f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' (U i).carrier)) x)))
x : α
i : ι
hi : f x ∈ U i
⊢ 𝓝 x = Filter.comap f (𝓝 (f x))

Tactic:
simpa [← ((h.1 _ (U i).2).isOpenEmbedding_subtypeVal).map_nhds_eq ⟨x, hi⟩, H i ⟨x, hi⟩,
      subtype_coe_map_comap] using preimage_mem_comap ((U i).2.mem_nhds hi)

Premises used: Topology.IsOpenEmbedding.map_nhds_eq, IsOpen.isOpenEmbedding_subtypeVal, Subtype.mk, Filter.subtype_coe_map_comap, IsOpen.mem_nhds, Filter.preimage_mem_comap, TopologicalSpace.Opens.is_open', Continuous.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 : Continuous[inst, inst_1] f
⊢ IsEmbedding f ↔ ∀ (i : ι), IsEmbedding ((U i).carrier.restrictPreimage f)

Tactic:
simpa [isEmbedding_iff, forall_and] using and_congr (hU.isInducing_iff_restrictPreimage h)
    (injective_iff_injective_of_iUnion_eq_univ hU.iSup_set_eq_univ)

Premises used: TopologicalSpace.IsOpenCover.isInducing_iff_restrictPreimage, TopologicalSpace.IsOpenCover.iSup_set_eq_univ, Topology.isEmbedding_iff, Set.injective_iff_injective_of_iUnion_eq_univ, and_congr, forall_and
-- 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 : Continuous[inst, inst_1] f
simp_rw :
  IsEmbedding f ∧ IsOpen[inst_1] (range f) ↔
    (∀ (x : ι), IsEmbedding ((U x).carrier.restrictPreimage f)) ∧
      ∀ (x : ι), IsOpen[instTopologicalSpaceSubtype] (range ((U x).carrier.restrictPreimage f))
⊢ IsOpenEmbedding f ↔ ∀ (i : ι), IsOpenEmbedding ((U i).carrier.restrictPreimage f)

Tactic:
simp_rw [isOpenEmbedding_iff, forall_and]

Premises used: Topology.isOpenEmbedding_iff, forall_and
-- 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 : Continuous[inst, inst_1] f
h₁ : IsEmbedding f ↔ ∀ (x : ι), IsEmbedding ((U x).carrier.restrictPreimage f)
h₂ :
  IsOpen[inst_1] (range f) ↔ ∀ (x : ι), IsOpen[instTopologicalSpaceSubtype] (range ((U x).carrier.restrictPreimage f))
⊢ IsEmbedding f ∧ IsOpen[inst_1] (range f) ↔
    (∀ (x : ι), IsEmbedding ((U x).carrier.restrictPreimage f)) ∧
      ∀ (x : ι), IsOpen[instTopologicalSpaceSubtype] (range ((U x).carrier.restrictPreimage f))

Tactic:
apply and_congr

Premises used: and_congr
-- 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 : Continuous[inst, inst_1] f
⊢ IsEmbedding f ↔ ∀ (x : ι), IsEmbedding ((U x).carrier.restrictPreimage f)

Tactic:
hU.isEmbedding_iff_restrictPreimage h

Premises used: TopologicalSpace.IsOpenCover.isEmbedding_iff_restrictPreimage
-- 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 : Continuous[inst, inst_1] f
⊢ IsEmbedding f ↔ ∀ (x : ι), IsEmbedding ((U x).carrier.restrictPreimage f)

Tactic:
exact hU.isEmbedding_iff_restrictPreimage h

Premises used: TopologicalSpace.IsOpenCover.isEmbedding_iff_restrictPreimage
-- 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 : Continuous[inst, inst_1] f
h₂ :
  IsOpen[inst_1] (range f) ↔
    ∀ (x : ι), IsOpen[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x_1 : β) ↦ x_1 ∈ (U x).carrier) ⁻¹' range f)
⊢ IsOpen[inst_1] (range f) ↔ ∀ (x : ι), IsOpen[instTopologicalSpaceSubtype] (range ((U x).carrier.restrictPreimage f))

Tactic:
simp_rw [range_restrictPreimage]

Premises used: Set.range_restrictPreimage
-- 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 : Continuous[inst, inst_1] f
⊢ IsOpen[inst_1] (range f) ↔
    ∀ (x : ι), IsOpen[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x_1 : β) ↦ x_1 ∈ (U x).carrier) ⁻¹' range f)

Tactic:
hU.isOpen_iff_coe_preimage

Premises used: Set.Mem, 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 : Continuous[inst, inst_1] f
⊢ IsOpen[inst_1] (range f) ↔
    ∀ (x : ι), IsOpen[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x_1 : β) ↦ x_1 ∈ (U x).carrier) ⁻¹' range f)

Tactic:
exact 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 : Continuous[inst, inst_1] f
simp_rw :
  IsEmbedding f ∧ IsClosed[inst_1] (range f) ↔
    (∀ (x : ι), IsEmbedding ((U x).carrier.restrictPreimage f)) ∧
      ∀ (x : ι), IsClosed[instTopologicalSpaceSubtype] (range ((U x).carrier.restrictPreimage f))
⊢ IsClosedEmbedding f ↔ ∀ (i : ι), IsClosedEmbedding ((U i).carrier.restrictPreimage f)

Tactic:
simp_rw [isClosedEmbedding_iff, forall_and]

Premises used: Topology.isClosedEmbedding_iff, forall_and
-- 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 : Continuous[inst, inst_1] f
h₁ : IsEmbedding f ↔ ∀ (x : ι), IsEmbedding ((U x).carrier.restrictPreimage f)
h₂ :
  IsClosed[inst_1] (range f) ↔
    ∀ (x : ι), IsClosed[instTopologicalSpaceSubtype] (range ((U x).carrier.restrictPreimage f))
⊢ IsEmbedding f ∧ IsClosed[inst_1] (range f) ↔
    (∀ (x : ι), IsEmbedding ((U x).carrier.restrictPreimage f)) ∧
      ∀ (x : ι), IsClosed[instTopologicalSpaceSubtype] (range ((U x).carrier.restrictPreimage f))

Tactic:
apply and_congr

Premises used: and_congr
-- 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 : Continuous[inst, inst_1] f
h₂ :
  IsClosed[inst_1] (range f) ↔
    ∀ (x : ι),
      IsClosed[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x_1 : β) ↦ x_1 ∈ (U x).carrier) ⁻¹' range f)
⊢ IsClosed[inst_1] (range f) ↔
    ∀ (x : ι), IsClosed[instTopologicalSpaceSubtype] (range ((U x).carrier.restrictPreimage f))

Tactic:
simp_rw [range_restrictPreimage]

Premises used: Set.range_restrictPreimage
-- 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 : Continuous[inst, inst_1] f
⊢ IsClosed[inst_1] (range f) ↔
    ∀ (x : ι),
      IsClosed[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x_1 : β) ↦ x_1 ∈ (U x).carrier) ⁻¹' range f)

Tactic:
hU.isClosed_iff_coe_preimage

Premises used: Set.Mem, 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 : Continuous[inst, inst_1] f
⊢ IsClosed[inst_1] (range f) ↔
    ∀ (x : ι),
      IsClosed[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x_1 : β) ↦ x_1 ∈ (U x).carrier) ⁻¹' range f)

Tactic:
exact 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 : Continuous[inst, inst_1] f
simp_rw :
  IsEmbedding f ∧ Function.Surjective f ↔
    ∀ (i : ι), IsEmbedding ((U i).carrier.restrictPreimage f) ∧ Function.Surjective ((U i).carrier.restrictPreimage f)
simp_rw₁ :
  IsEmbedding f ∧ Function.Surjective f ↔
    (∀ (x : ι), IsEmbedding ((U x).carrier.restrictPreimage f)) ∧
      ∀ (x : ι), Function.Surjective ((U x).carrier.restrictPreimage f)
simp_rw₂ :
  IsEmbedding f ∧ Function.Surjective f ↔
    IsEmbedding f ∧ ∀ (x : ι), Function.Surjective ((U x).carrier.restrictPreimage f)
simp_rw₃ :
  (IsEmbedding f ∧ ∀ (i : ι), Function.Surjective ((↑(U i) : Set β).restrictPreimage f)) ↔
    IsEmbedding f ∧ ∀ (x : ι), Function.Surjective ((U x).carrier.restrictPreimage f)
⊢ IsHomeomorph f ↔ ∀ (i : ι), IsHomeomorph ((U i).carrier.restrictPreimage f)

Tactic:
simp_rw [isHomeomorph_iff_isEmbedding_surjective, forall_and,
    ← isEmbedding_iff_restrictPreimage hU h,
    surjective_iff_surjective_of_iUnion_eq_univ hU.iSup_set_eq_univ, Opens.carrier_eq_coe]

Premises used: TopologicalSpace.IsOpenCover.iSup_set_eq_univ, isHomeomorph_iff_isEmbedding_surjective, TopologicalSpace.Opens.carrier_eq_coe, TopologicalSpace.IsOpenCover.isEmbedding_iff_restrictPreimage, Set.surjective_iff_surjective_of_iUnion_eq_univ, forall_and
-- Module: Mathlib.Topology.LocalAtTarget
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
simp_rw :
  closure[inst] (range f) = univ ↔
    ∀ (i : ι),
      Eq (α := Set (↑(U i).carrier : Type u_2))
        (Subtype.val (p := fun (x : β) ↦ x ∈ (U i).carrier) ⁻¹' closure[inst] (range f)) univ
⊢ DenseRange f ↔ ∀ (i : ι), DenseRange ((U i).carrier.restrictPreimage f)

Tactic:
simp_rw [denseRange_iff_closure_range, Set.range_restrictPreimage,
    ← (U _).2.isOpenEmbedding_subtypeVal.isOpenMap.preimage_closure_eq_closure_preimage
      continuous_subtype_val]

Premises used: IsOpen.isOpenEmbedding_subtypeVal, Topology.IsOpenEmbedding.isOpenMap, continuous_subtype_val, Set.range_restrictPreimage, IsOpenMap.preimage_closure_eq_closure_preimage, denseRange_iff_closure_range, TopologicalSpace.Opens.is_open'
-- Module: Mathlib.Topology.LocalAtTarget
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
simp : closure[inst] (range f) = univ ↔ ∀ (i : ι), {x : β | x ∈ U i} ⊆ closure[inst] (range f)
⊢ closure[inst] (range f) = univ ↔
    ∀ (i : ι),
      Eq (α := Set (↑(U i).carrier : Type u_2))
        (Subtype.val (p := fun (x : β) ↦ x ∈ (U i).carrier) ⁻¹' closure[inst] (range f)) univ

Tactic:
simp only [Opens.carrier_eq_coe, SetLike.coe_sort_coe, preimage_eq_univ_iff,
    Subtype.range_coe_subtype, SetLike.mem_coe]

Premises used: SetLike.coe_sort_coe, Set.preimage_eq_univ_iff, Subtype.range_coe_subtype, TopologicalSpace.Opens.carrier_eq_coe, SetLike.mem_coe
-- Module: Mathlib.Topology.LocalAtTarget
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
rw : (univ ⊆ closure[inst] (range f)) = (⋃ (i : ι), {x : β | x ∈ U i} ⊆ closure[inst] (range f))
⊢ closure[inst] (range f) = univ ↔ ∀ (i : ι), {x : β | x ∈ U i} ⊆ closure[inst] (range f)

Tactic:
rw [← iUnion_subset_iff, ← Set.univ_subset_iff, iff_iff_eq]

Premises used: Set.univ_subset_iff, Set.iUnion_subset_iff, iff_iff_eq
-- Module: Mathlib.Topology.LocalAtTarget
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
e_a : Eq.{u_2 + 1} (α := Set β) univ (⋃ (i : ι), {x : β | x ∈ U i})
⊢ (univ ⊆ closure[inst] (range f)) = (⋃ (i : ι), {x : β | x ∈ U i} ⊆ closure[inst] (range f))

Tactic:
congr 1
-- Module: Mathlib.Topology.LocalAtTarget
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
⊢ Eq.{u_2 + 1} (α := Set β) univ (⋃ (i : ι), {x : β | x ∈ U i})

Tactic:
hU.iSup_set_eq_univ.symm

Premises used: TopologicalSpace.IsOpenCover.iSup_set_eq_univ, Set.Mem, setOf, Eq.symm
-- Module: Mathlib.Topology.LocalAtTarget
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
⊢ Eq.{u_2 + 1} (α := Set β) univ (⋃ (i : ι), {x : β | x ∈ U i})

Tactic:
exact hU.iSup_set_eq_univ.symm

Premises used: TopologicalSpace.IsOpenCover.iSup_set_eq_univ, Eq.symm
-- 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
⊢ GeneralizingMap f ↔ ∀ (i : ι), GeneralizingMap ((U i).carrier.restrictPreimage f)

Tactic:
⟨fun hf ↦ fun i ↦ hf.restrictPreimage _, fun hf ↦ fun x y h ↦ ?_⟩

Premises used: TopologicalSpace.Opens.carrier, Iff.intro, GeneralizingMap.restrictPreimage
-- 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 :
  ∀ (hf : ∀ (i : ι), GeneralizingMap ((U i).carrier.restrictPreimage f)) (x : α) (y : β)
    (h : (fun (x1 x2 : β) ↦ x1 ⤳ x2) y (f x)), ∃ (a' : α), (fun (x1 x2 : α) ↦ x1 ⤳ x2) a' x ∧ f a' = y
⊢ GeneralizingMap f ↔ ∀ (i : ι), GeneralizingMap ((U i).carrier.restrictPreimage f)

Tactic:
refine ⟨fun hf ↦ fun i ↦ hf.restrictPreimage _, fun hf ↦ fun x y h ↦ ?_⟩
-- 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
hf : ∀ (i : ι), GeneralizingMap ((U i).carrier.restrictPreimage f)
x : α
y : β
h : (fun (x1 x2 : β) ↦ x1 ⤳ x2) y (f x)
obtain : ∀ (i : ι) (hx : f x ∈ U i), ∃ (a' : α), (fun (x1 x2 : α) ↦ x1 ⤳ x2) a' x ∧ f a' = y
⊢ ∃ (a' : α), (fun (x1 x2 : α) ↦ x1 ⤳ x2) a' x ∧ f a' = y

Tactic:
obtain ⟨i, hx⟩ := hU.exists_mem (f x)

Premises used: TopologicalSpace.IsOpenCover.exists_mem
-- 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
hf : ∀ (i : ι), GeneralizingMap ((U i).carrier.restrictPreimage f)
x : α
y : β
h : (fun (x1 x2 : β) ↦ x1 ⤳ x2) y (f x)
i : ι
hx : f x ∈ U i
rwa rwa₁ rwa₂ rwa₃ :
  (↑(Subtype.mk (p := fun (x : β) ↦ x ∈ U i) y ⋯) : β) ⤳
    (↑((U i).carrier.restrictPreimage f (Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' (U i).carrier) x hx)) : β)
⊢ Subtype.mk (p := fun (x : β) ↦ x ∈ U i) y ⋯ ⤳
    (U i).carrier.restrictPreimage f (Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' (U i).carrier) x hx)

Tactic:
rwa [subtype_specializes_iff]

Premises used: subtype_specializes_iff
-- 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
hf : ∀ (i : ι), GeneralizingMap ((U i).carrier.restrictPreimage f)
x : α
y : β
h : (fun (x1 x2 : β) ↦ x1 ⤳ x2) y (f x)
i : ι
hx : f x ∈ U i
⊢ Subtype.mk (p := fun (x : β) ↦ x ∈ U i) y ⋯ ⤳
    (U i).carrier.restrictPreimage f (Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' (U i).carrier) x hx)

Tactic:
have h : (⟨y, (U i).2.stableUnderGeneralization h hx⟩ : U i) ⤳
    (U i).1.restrictPreimage f ⟨x, hx⟩ := by rwa [subtype_specializes_iff]
-- 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
hf : ∀ (i : ι), GeneralizingMap ((U i).carrier.restrictPreimage f)
x : α
y : β
h_1 : (fun (x1 x2 : β) ↦ x1 ⤳ x2) y (f x)
i : ι
hx : f x ∈ U i
h :
  Subtype.mk (p := fun (x : β) ↦ x ∈ U i) y ⋯ ⤳
    (U i).carrier.restrictPreimage f (Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' (U i).carrier) x hx)
obtain :
  ∀ (a : (↑(f ⁻¹' (U i).carrier) : Type u_1)) (ha : a ⤳ Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' (U i).carrier) x hx)
    (heq : (U i).carrier.restrictPreimage f a = Subtype.mk (p := fun (x : β) ↦ x ∈ U i) y ⋯),
    ∃ (a' : α), (fun (x1 x2 : α) ↦ x1 ⤳ x2) a' x ∧ f a' = y
⊢ ∃ (a' : α), (fun (x1 x2 : α) ↦ x1 ⤳ x2) a' x ∧ f a' = y

Tactic:
obtain ⟨a, ha, heq⟩ := hf i h
-- 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
hf : ∀ (i : ι), GeneralizingMap ((U i).carrier.restrictPreimage f)
x : α
y : β
h_1 : (fun (x1 x2 : β) ↦ x1 ⤳ x2) y (f x)
i : ι
hx : f x ∈ U i
h :
  Subtype.mk (p := fun (x : β) ↦ x ∈ U i) y ⋯ ⤳
    (U i).carrier.restrictPreimage f (Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' (U i).carrier) x hx)
a : (↑(f ⁻¹' (U i).carrier) : Type u_1)
ha : a ⤳ Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' (U i).carrier) x hx
heq : (U i).carrier.restrictPreimage f a = Subtype.mk (p := fun (x : β) ↦ x ∈ U i) y ⋯
⊢ ∃ (a' : α), (fun (x1 x2 : α) ↦ x1 ⤳ x2) a' x ∧ f a' = y

Tactic:
⟨a, ?_, congr(($heq).val)⟩

Premises used: congrArg, id, And.intro, Exists.intro, Subtype.val