awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.LocalAtTarget (goal)
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 ∈ U i ∧ f y = x) → ∃ y ∈ s, f y = x
have tauto : ∀ w ∈ s, f w ∈ U i → f w = x → ∃ y ∈ s, f y = x
Tactic: tauto
-- Lean 4 proof step from Mathlib.Topology.LocalAtTarget (goal)
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)
have refine : ∀ (H : ∀ (i : ι), IsClosedMap ((U i).carrier.restrictPreimage f)) (s : Set α) (hs : IsClosed[inst] s),
  IsClosed[inst_1] (f '' s)
Tactic: refine ⟨fun h i => h.restrictPreimage _, fun H s hs ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.LocalAtTarget (goal)
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
⊢ IsClosed[inst_1] (f '' s)
have rw : ∀ (i : ι), IsClosed[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x : β) ↦ x ∈ U i) ⁻¹' f '' s)
Tactic: rw [hU.isClosed_iff_coe_preimage]
-- Lean 4 proof step from Mathlib.Topology.LocalAtTarget (goal)
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] (Subtype.val (p := fun (x : β) ↦ x ∈ U i) ⁻¹' f '' s)
have 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ᶜ)ᶜ
Tactic: convert! H i _ ⟨⟨_, hs.1, eq_compl_comm.mpr rfl⟩⟩
-- Lean 4 proof step from Mathlib.Topology.LocalAtTarget (goal)
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)
⊢ 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ᶜ)ᶜ
have 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ᶜ)ᶜ
Tactic: ext ⟨x, hx⟩
-- Lean 4 proof step from Mathlib.Topology.LocalAtTarget (goal)
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
⊢ 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ᶜ)ᶜ
have h : (∃ y ∈ s, f y = x) ↔ ∃ y ∈ s, f y ∈ U i ∧ f y = x
Tactic: suffices (∃ y, y ∈ s ∧ f y = x) ↔ ∃ y, y ∈ s ∧ f y ∈ U i ∧ f y = x by simpa [← Subtype.coe_inj]
-- Lean 4 proof step from Mathlib.Topology.LocalAtTarget (goal)
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 ∈ U i ∧ f y = x) → ∃ y ∈ s, f y = x
have tauto : ∀ w ∈ s, f w ∈ U i → f w = x → ∃ y ∈ s, f y = x
Tactic: tauto
-- Lean 4 proof step from Mathlib.Topology.LocalAtTarget (goal)
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
⊢ IsInducing f ↔ ∀ (i : ι), IsInducing ((U i).carrier.restrictPreimage f)
have 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)))
Tactic: simp_rw [← IsInducing.subtypeVal.of_comp_iff, isInducing_iff_nhds, restrictPreimage,
    MapsTo.coe_restrict, restrict_eq, ← Filter.comap_comap]
-- Lean 4 proof step from Mathlib.Topology.LocalAtTarget (goal)
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
⊢ (∀ (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)))
have 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)))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.LocalAtTarget (goal)
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)))
⊢ (∀ (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)))
have 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))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.LocalAtTarget (goal)
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)
⊢ 𝓝 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)))
have mp : 𝓝 x = Filter.comap (Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' (U i).carrier)) (Filter.comap f (𝓝 (f (↑x : α))))
Tactic: rw [Function.comp_apply, ← H, ← IsInducing.subtypeVal.nhds_eq_comap]
-- Lean 4 proof step from Mathlib.Topology.LocalAtTarget (goal)
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 : α))))
⊢ 𝓝 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)))
have mp₁ : 𝓝 x = Filter.comap (Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' (U i).carrier)) (𝓝 (↑x : α))
Tactic: rw [Function.comp_apply, ← H, ← IsInducing.subtypeVal.nhds_eq_comap]
-- Lean 4 proof step from Mathlib.Topology.LocalAtTarget (goal)
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 : α))
⊢ 𝓝 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)))
have mp₂ : 𝓝 x = 𝓝 x
Tactic: rw [Function.comp_apply, ← H, ← IsInducing.subtypeVal.nhds_eq_comap]
-- Lean 4 proof step from Mathlib.Topology.LocalAtTarget (goal)
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 : α
⊢ 𝓝 x = Filter.comap f (𝓝 (f x))
have mpr : ∀ (i : ι) (hi : f x ∈ U i), 𝓝 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])
-- Lean 4 proof step from Mathlib.Topology.LocalAtTarget (goal)
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
⊢ IsOpenEmbedding f ↔ ∀ (i : ι), IsOpenEmbedding ((U i).carrier.restrictPreimage f)
have 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))
Tactic: simp_rw [isOpenEmbedding_iff, forall_and]
-- Lean 4 proof step from Mathlib.Topology.LocalAtTarget (goal)
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 ∧ IsOpen[inst_1] (range f) ↔
    (∀ (x : ι), IsEmbedding ((U x).carrier.restrictPreimage f)) ∧
      ∀ (x : ι), IsOpen[instTopologicalSpaceSubtype] (range ((U x).carrier.restrictPreimage f))
have h₁ : IsEmbedding f ↔ ∀ (x : ι), IsEmbedding ((U x).carrier.restrictPreimage f)
Tactic: apply and_congr
-- Lean 4 proof step from Mathlib.Topology.LocalAtTarget (goal)
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)
⊢ IsEmbedding f ∧ IsOpen[inst_1] (range f) ↔
    (∀ (x : ι), IsEmbedding ((U x).carrier.restrictPreimage f)) ∧
      ∀ (x : ι), IsOpen[instTopologicalSpaceSubtype] (range ((U x).carrier.restrictPreimage f))
have h₂ : IsOpen[inst_1] (range f) ↔ ∀ (x : ι), IsOpen[instTopologicalSpaceSubtype] (range ((U x).carrier.restrictPreimage f))
Tactic: apply and_congr
-- Lean 4 proof step from Mathlib.Topology.LocalAtTarget (goal)
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] (range ((U x).carrier.restrictPreimage f))
have h₂ : IsOpen[inst_1] (range f) ↔
  ∀ (x : ι), IsOpen[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x_1 : β) ↦ x_1 ∈ (U x).carrier) ⁻¹' range f)
Tactic: simp_rw [range_restrictPreimage]
-- Lean 4 proof step from Mathlib.Topology.LocalAtTarget (goal)
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
⊢ IsClosedEmbedding f ↔ ∀ (i : ι), IsClosedEmbedding ((U i).carrier.restrictPreimage f)
have 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))
Tactic: simp_rw [isClosedEmbedding_iff, forall_and]
-- Lean 4 proof step from Mathlib.Topology.LocalAtTarget (goal)
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 ∧ IsClosed[inst_1] (range f) ↔
    (∀ (x : ι), IsEmbedding ((U x).carrier.restrictPreimage f)) ∧
      ∀ (x : ι), IsClosed[instTopologicalSpaceSubtype] (range ((U x).carrier.restrictPreimage f))
have h₁ : IsEmbedding f ↔ ∀ (x : ι), IsEmbedding ((U x).carrier.restrictPreimage f)
Tactic: apply and_congr
-- Lean 4 proof step from Mathlib.Topology.LocalAtTarget (goal)
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)
⊢ IsEmbedding f ∧ IsClosed[inst_1] (range f) ↔
    (∀ (x : ι), IsEmbedding ((U x).carrier.restrictPreimage f)) ∧
      ∀ (x : ι), IsClosed[instTopologicalSpaceSubtype] (range ((U x).carrier.restrictPreimage f))
have h₂ : IsClosed[inst_1] (range f) ↔ ∀ (x : ι), IsClosed[instTopologicalSpaceSubtype] (range ((U x).carrier.restrictPreimage f))
Tactic: apply and_congr
-- Lean 4 proof step from Mathlib.Topology.LocalAtTarget (goal)
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] (range ((U x).carrier.restrictPreimage f))
have h₂ : IsClosed[inst_1] (range f) ↔
  ∀ (x : ι), IsClosed[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x_1 : β) ↦ x_1 ∈ (U x).carrier) ⁻¹' range f)
Tactic: simp_rw [range_restrictPreimage]
-- Lean 4 proof step from Mathlib.Topology.LocalAtTarget (goal)
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
⊢ IsHomeomorph f ↔ ∀ (i : ι), IsHomeomorph ((U i).carrier.restrictPreimage f)
have simp_rw : IsEmbedding f ∧ Function.Surjective f ↔
  ∀ (i : ι), IsEmbedding ((U i).carrier.restrictPreimage f) ∧ Function.Surjective ((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]
-- Lean 4 proof step from Mathlib.Topology.LocalAtTarget (goal)
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)
⊢ IsHomeomorph f ↔ ∀ (i : ι), IsHomeomorph ((U i).carrier.restrictPreimage f)
have simp_rw₁ : IsEmbedding f ∧ Function.Surjective f ↔
  (∀ (x : ι), IsEmbedding ((U x).carrier.restrictPreimage f)) ∧
    ∀ (x : ι), Function.Surjective ((U x).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]
-- Lean 4 proof step from Mathlib.Topology.LocalAtTarget (goal)
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)
⊢ IsHomeomorph f ↔ ∀ (i : ι), IsHomeomorph ((U i).carrier.restrictPreimage f)
have simp_rw₂ : IsEmbedding f ∧ Function.Surjective f ↔
  IsEmbedding f ∧ ∀ (x : ι), Function.Surjective ((U x).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]
-- Lean 4 proof step from Mathlib.Topology.LocalAtTarget (goal)
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)
⊢ IsHomeomorph f ↔ ∀ (i : ι), IsHomeomorph ((U i).carrier.restrictPreimage f)
have simp_rw₃ : (IsEmbedding f ∧ ∀ (i : ι), Function.Surjective ((↑(U i) : Set β).restrictPreimage f)) ↔
  IsEmbedding f ∧ ∀ (x : ι), Function.Surjective ((U x).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]
-- Lean 4 proof step from Mathlib.Topology.LocalAtTarget (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
⊢ DenseRange f ↔ ∀ (i : ι), DenseRange ((U i).carrier.restrictPreimage f)
have 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
Tactic: simp_rw [denseRange_iff_closure_range, Set.range_restrictPreimage,
    ← (U _).2.isOpenEmbedding_subtypeVal.isOpenMap.preimage_closure_eq_closure_preimage
      continuous_subtype_val]
-- Lean 4 proof step from Mathlib.Topology.LocalAtTarget (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
⊢ 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
have simp : closure[inst] (range f) = univ ↔ ∀ (i : ι), {x : β | x ∈ U i} ⊆ closure[inst] (range f)
Tactic: simp only [Opens.carrier_eq_coe, SetLike.coe_sort_coe, preimage_eq_univ_iff,
    Subtype.range_coe_subtype, SetLike.mem_coe]
-- Lean 4 proof step from Mathlib.Topology.LocalAtTarget (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
⊢ closure[inst] (range f) = univ ↔ ∀ (i : ι), {x : β | x ∈ U i} ⊆ closure[inst] (range f)
have rw : (univ ⊆ closure[inst] (range f)) = (⋃ (i : ι), {x : β | x ∈ U i} ⊆ closure[inst] (range f))
Tactic: rw [← iUnion_subset_iff, ← Set.univ_subset_iff, iff_iff_eq]
-- Lean 4 proof step from Mathlib.Topology.LocalAtTarget (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
⊢ (univ ⊆ closure[inst] (range f)) = (⋃ (i : ι), {x : β | x ∈ U i} ⊆ closure[inst] (range f))
have e_a : Eq.{u_2 + 1} (α := Set β) univ (⋃ (i : ι), {x : β | x ∈ U i})
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Topology.LocalAtTarget (goal)
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)
have 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
Tactic: refine ⟨fun hf ↦ fun i ↦ hf.restrictPreimage _, fun hf ↦ fun x y h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.LocalAtTarget (goal)
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)
⊢ ∃ (a' : α), (fun (x1 x2 : α) ↦ x1 ⤳ x2) a' x ∧ f a' = y
have obtain : ∀ (i : ι) (hx : f x ∈ U i), ∃ (a' : α), (fun (x1 x2 : α) ↦ x1 ⤳ x2) a' x ∧ f a' = y
Tactic: obtain ⟨i, hx⟩ := hU.exists_mem (f x)
-- Lean 4 proof step from Mathlib.Topology.LocalAtTarget (goal)
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)
have rwa : (↑(Subtype.mk (p := fun (x : β) ↦ x ∈ U i) y sorry) : β) ⤳
  (↑((U i).carrier.restrictPreimage f (Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' (U i).carrier) x hx)) : β)
Tactic: rwa [subtype_specializes_iff]
-- Lean 4 proof step from Mathlib.Topology.LocalAtTarget (hypothesis)
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
⊢ ∃ (a' : α), (fun (x1 x2 : α) ↦ x1 ⤳ x2) a' x ∧ f a' = y
have h₁ : Subtype.mk (p := fun (x : β) ↦ x ∈ U i) y sorry ⤳
  (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]
-- Lean 4 proof step from Mathlib.Topology.LocalAtTarget (goal)
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' : α), (fun (x1 x2 : α) ↦ x1 ⤳ x2) a' x ∧ f a' = y
have 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 sorry),
  ∃ (a' : α), (fun (x1 x2 : α) ↦ x1 ⤳ x2) a' x ∧ f a' = y
Tactic: obtain ⟨a, ha, heq⟩ := hf i h