awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : Surjective f
⊢ IsDominant f

Tactic:
⟨f.surjective.denseRange⟩

Premises used: Function.Surjective.denseRange, AlgebraicGeometry.IsDominant.mk, AlgebraicGeometry.Scheme.Hom.surjective
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : IsDominant f
inst_1 : IsDominant g
⊢ IsDominant (f ≫ g)

Tactic:
⟨g.denseRange.comp f.denseRange g.continuous⟩

Premises used: AlgebraicGeometry.Scheme.Hom.denseRange, AlgebraicGeometry.IsDominant.mk, AlgebraicGeometry.Scheme.Hom.continuous, DenseRange.comp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
H : IsDominant (f ≫ g)
rw :
  ∀ (H : Subset (α := Set ↥Z) Set.univ (closure (Set.range (ι := ↥X) ⇑(f ≫ g)))),
    Subset (α := Set ↥Z) Set.univ (closure (Set.range (ι := ↥Y) ⇑g))
⊢ IsDominant g

Tactic:
rw [isDominant_iff, denseRange_iff_closure_range, ← Set.univ_subset_iff] at H ⊢

Premises used: Set.univ_subset_iff, AlgebraicGeometry.isDominant_iff, denseRange_iff_closure_range
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
H : Subset (α := Set ↥Z) Set.univ (closure (Set.range (ι := ↥X) ⇑(f ≫ g)))
⊢ Subset (α := Set ↥Z) Set.univ (closure (Set.range (ι := ↥Y) ⇑g))

Tactic:
H.trans (closure_mono (Set.range_comp_subset_range f g))

Premises used: Set.range_comp_subset_range, CategoryTheory.ConcreteCategory.hom, HasSubset.Subset.trans, closure_mono, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.PresheafedSpace.Hom.base, DFunLike.coe
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
H : Subset (α := Set ↥Z) Set.univ (closure (Set.range (ι := ↥X) ⇑(f ≫ g)))
⊢ Subset (α := Set ↥Z) Set.univ (closure (Set.range (ι := ↥Y) ⇑g))

Tactic:
exact H.trans (closure_mono (Set.range_comp_subset_range f g))

Premises used: Set.range_comp_subset_range, CategoryTheory.ConcreteCategory.hom, HasSubset.Subset.trans, closure_mono, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.PresheafedSpace.Hom.base, DFunLike.coe
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : IsDominant f
⊢ IsDominant (f ≫ g) ↔ IsDominant g

Tactic:
⟨fun _ ↦ of_comp f g, fun _ ↦ inferInstance⟩

Premises used: AlgebraicGeometry.IsDominant.of_comp, inferInstance, Iff.intro
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ MorphismProperty.RespectsIso @IsDominant

Tactic:
MorphismProperty.respectsIso_of_isStableUnderComposition fun _ _ f (_ : IsIso f) ↦ inferInstance

Premises used: inferInstance, CategoryTheory.MorphismProperty.respectsIso_of_isStableUnderComposition
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ IsZariskiLocalAtTarget @IsDominant

Tactic:
have : MorphismProperty.RespectsIso (topologically DenseRange) :=
    dominant_eq_topologically ▸ IsDominant.respectsIso
  dominant_eq_topologically ▸ topologically_isZariskiLocalAtTarget' DenseRange
    fun _ _ _ hU _ ↦ hU.denseRange_iff_restrictPreimage

Premises used: AlgebraicGeometry.IsDominant.respectsIso, AlgebraicGeometry.topologically_isZariskiLocalAtTarget', Eq.rec, TopologicalSpace.IsOpenCover.denseRange_iff_restrictPreimage, DenseRange, Eq.symm, AlgebraicGeometry.dominant_eq_topologically
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsDominant f
hf : IsClosed (X := ↥Y) (Set.range (ι := ↥X) ⇑f)
rw : Eq (α := Set ↥Y) (Set.range (ι := ↥X) ⇑f) Set.univ
rw₁ : Eq (α := Set ↥Y) (closure (Set.range (ι := ↥X) ⇑f)) Set.univ
rw₂ rw₃ : Eq.{u + 1} (α := Set ↥Y) Set.univ Set.univ
⊢ Function.Surjective (α := ↥X) (β := ↥Y) ⇑f

Tactic:
rw [← Set.range_eq_univ, ← hf.closure_eq, f.denseRange.closure_range]

Premises used: Set.range_eq_univ, AlgebraicGeometry.Scheme.Hom.denseRange, IsClosed.closure_eq, DenseRange.closure_range
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
H : IsDominant (f ≫ g)
inst : IsOpenImmersion g
rw :
  ∀ (H : Dense (X := ↥Z) (Set.range (ι := ↥X) ⇑(f ≫ g))) [IsOpenImmersion g], Dense (X := ↥Y) (Set.range (ι := ↥X) ⇑f)
⊢ IsDominant f

Tactic:
rw [isDominant_iff, DenseRange] at H ⊢

Premises used: AlgebraicGeometry.isDominant_iff, DenseRange
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
H : Dense (X := ↥Z) (Set.range (ι := ↥X) ⇑(f ≫ g))
inst : IsOpenImmersion g
⊢ Dense (X := ↥Z) (Set.image (α := ↥Y) (⇑g) (Set.range (ι := ↥X) ⇑f))

Tactic:
simp only [Scheme.Hom.comp_base, TopCat.coe_comp, Set.range_comp] at H

Premises used: Set.range_comp, AlgebraicGeometry.Scheme.Hom.comp_base, TopCat.coe_comp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : IsOpenImmersion g
H : Dense (X := ↥Z) (Set.image (α := ↥Y) (⇑g) (Set.range (ι := ↥X) ⇑f))
⊢ Dense (X := ↥Y) (Set.preimage (β := ↥Z) (⇑g) (Set.image (α := ↥Y) (⇑g) (Set.range (ι := ↥X) ⇑f)))

Tactic:
H.preimage g.isOpenEmbedding.isOpenMap

Premises used: Topology.IsOpenEmbedding.isOpenMap, AlgebraicGeometry.Scheme.Hom.isOpenEmbedding, Dense.preimage
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : IsOpenImmersion g
H : Dense (X := ↥Z) (Set.image (α := ↥Y) (⇑g) (Set.range (ι := ↥X) ⇑f))
h :
  Eq (α := Set ↥Y) (Set.range (ι := ↥X) ⇑f)
    (Set.preimage (β := ↥Z) (⇑g) (Set.image (α := ↥Y) (⇑g) (Set.range (ι := ↥X) ⇑f)))
⊢ Dense (X := ↥Y) (Set.range (ι := ↥X) ⇑f)

Tactic:
convert! H.preimage g.isOpenEmbedding.isOpenMap using 1

Premises used: Topology.IsOpenEmbedding.isOpenMap, AlgebraicGeometry.Scheme.Hom.isOpenEmbedding, Dense.preimage
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : IsOpenImmersion g
H : Dense (X := ↥Z) (Set.image (α := ↥Y) (⇑g) (Set.range (ι := ↥X) ⇑f))
h h₁ : Eq (α := Set ↥Y) (Set.range (ι := ↥X) ⇑f) (Set.range (ι := ↥X) ⇑f)
⊢ Eq (α := Set ↥Y) (Set.range (ι := ↥X) ⇑f)
    (Set.preimage (β := ↥Z) (⇑g) (Set.image (α := ↥Y) (⇑g) (Set.range (ι := ↥X) ⇑f)))

Tactic:
rw [Set.preimage_image_eq _ g.isOpenEmbedding.injective]

Premises used: Topology.IsOpenEmbedding.toIsEmbedding, AlgebraicGeometry.Scheme.Hom.isOpenEmbedding, Topology.IsEmbedding.injective, Set.preimage_image_eq
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Goal:
X : Scheme
U : X.Opens
hU : Dense (↑U : Set ↥X)
⊢ DenseRange (X := ↥X) (α := ↥(↑U : Scheme)) ⇑U.ι

Tactic:
simpa [DenseRange] using hU

Premises used: DenseRange
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Goal:
X : Scheme
U V : X.Opens
hU : Dense (↑U : Set ↥X)
hU' : U ≤ V
⊢ IsDominant (X.homOfLE hU' ≫ V.ι)

Tactic:
simpa using Opens.isDominant_ι hU

Premises used: AlgebraicGeometry.Opens.isDominant_ι
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Goal:
hP₁ :
  ∀ {α β : Type u_1} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α ≃ₜ β),
    SpecializingMap (X := α) (Y := β) (⇑f : (a : α) → β)
hP₂ :
  ∀ {α β γ : Type u_1} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : TopologicalSpace γ]
    (f : α → β) (g : β → γ), SpecializingMap f → SpecializingMap g → SpecializingMap (g ∘ f)
⊢ (topologically @SpecializingMap).RespectsIso

Tactic:
apply topologically_respectsIso

Premises used: AlgebraicGeometry.topologically_respectsIso
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Goal:
α β : Type u_1
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α ≃ₜ β
⊢ SpecializingMap (X := α) (Y := β) (⇑f : (a : α) → β)

Tactic:
f.isClosedMap.specializingMap

Premises used: Homeomorph.isClosedMap, IsClosedMap.specializingMap
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Goal:
α β : Type u_1
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α ≃ₜ β
⊢ SpecializingMap (X := α) (Y := β) (⇑f : (a : α) → β)

Tactic:
exact f.isClosedMap.specializingMap

Premises used: Homeomorph.isClosedMap, IsClosedMap.specializingMap
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Goal:
α β γ : Type u_1
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
f : α → β
g : β → γ
hf : SpecializingMap f
hg : SpecializingMap g
⊢ SpecializingMap (g ∘ f)

Tactic:
hf.comp hg

Premises used: SpecializingMap.comp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Goal:
α β γ : Type u_1
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
f : α → β
g : β → γ
hf : SpecializingMap f
hg : SpecializingMap g
⊢ SpecializingMap (g ∘ f)

Tactic:
exact hf.comp hg

Premises used: SpecializingMap.comp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Goal:
hP₂ :
  ∀ {α β : Type u_1} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) (s : Set β),
    Continuous f → IsOpen s → SpecializingMap f → SpecializingMap (s.restrictPreimage f)
hP₃ :
  ∀ {α β : Type u_1} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) {ι : Type u_1}
    (U : ι → Opens β),
    IsOpenCover U → Continuous f → (∀ (i : ι), SpecializingMap ((U i).carrier.restrictPreimage f)) → SpecializingMap f
⊢ IsZariskiLocalAtTarget.{u_1} (topologically @SpecializingMap)

Tactic:
apply topologically_isZariskiLocalAtTarget

Premises used: AlgebraicGeometry.topologically_isZariskiLocalAtTarget
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Goal:
α β : Type u_1
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set β
h : Continuous[inst, inst_1] f
h_1 : IsOpen[inst_1] s
hf : SpecializingMap f
hP₂ :
  ∀ (hf : ∀ (x : α), closure[inst_1] {f x} ⊆ f '' closure[inst] {x}) (x : (↑(f ⁻¹' s) : Type u_1)),
    closure[instTopologicalSpaceSubtype] {s.restrictPreimage f x} ⊆
      s.restrictPreimage f '' closure[instTopologicalSpaceSubtype] {x}
⊢ SpecializingMap (s.restrictPreimage f)

Tactic:
rw [specializingMap_iff_closure_singleton_subset] at hf ⊢

Premises used: specializingMap_iff_closure_singleton_subset
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Goal:
α β : Type u_1
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set β
h : Continuous[inst, inst_1] f
h_1 : IsOpen[inst_1] s
hf : ∀ (x : α), closure[inst_1] {f x} ⊆ f '' closure[inst] {x}
x : α
hx : x ∈ f ⁻¹' s
hP₂ :
  ∀ (y : β) (hy : y ∈ s),
    Membership.mem (γ := Set (↑s : Type u_1))
        (closure[instTopologicalSpaceSubtype] {s.restrictPreimage f (Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' s) x hx)})
        (Subtype.mk (p := fun (x : β) ↦ x ∈ s) y hy) →
      Subtype.mk (p := fun (x : β) ↦ x ∈ s) y hy ∈
        s.restrictPreimage f '' closure[instTopologicalSpaceSubtype] {Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' s) x hx}
⊢ closure[instTopologicalSpaceSubtype] {s.restrictPreimage f (Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' s) x hx)} ⊆
    s.restrictPreimage f '' closure[instTopologicalSpaceSubtype] {Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' s) x hx}

Tactic:
⟨y, hy⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Goal:
α β : Type u_1
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set β
h : Continuous[inst, inst_1] f
h_1 : IsOpen[inst_1] s
hf : ∀ (x : α), closure[inst_1] {f x} ⊆ f '' closure[inst] {x}
x : α
hx : x ∈ f ⁻¹' s
y : β
hy : y ∈ s
hcl :
  Membership.mem (γ := Set (↑s : Type u_1))
    (closure[instTopologicalSpaceSubtype] {s.restrictPreimage f (Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' s) x hx)})
    (Subtype.mk (p := fun (x : β) ↦ x ∈ s) y hy)
⊢ Membership.mem (γ := Set β) (closure[inst_1] {f x}) y

Tactic:
simp only [closure_subtype, Set.restrictPreimage_mk, Set.image_singleton] at hcl

Premises used: Set.image_singleton, closure_subtype, Set.restrictPreimage_mk
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Goal:
α β : Type u_1
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set β
h : Continuous[inst, inst_1] f
h_1 : IsOpen[inst_1] s
hf : ∀ (x : α), closure[inst_1] {f x} ⊆ f '' closure[inst] {x}
x : α
hx : x ∈ f ⁻¹' s
y : β
hy : y ∈ s
hcl : Membership.mem (γ := Set β) (closure[inst_1] {f x}) y
hP₂ :
  ∀ (a : α) (ha : Membership.mem (γ := Set α) (closure[inst] {x}) a) (hay : f a = y),
    Subtype.mk (p := fun (x : β) ↦ x ∈ s) y hy ∈
      s.restrictPreimage f '' closure[instTopologicalSpaceSubtype] {Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' s) x hx}
⊢ Subtype.mk (p := fun (x : β) ↦ x ∈ s) y hy ∈
    s.restrictPreimage f '' closure[instTopologicalSpaceSubtype] {Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' s) x hx}

Tactic:
obtain ⟨a, ha, hay⟩ := hf x hcl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Goal:
α β : Type u_1
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set β
h : Continuous[inst, inst_1] f
h_1 : IsOpen[inst_1] s
hf : ∀ (x : α), closure[inst_1] {f x} ⊆ f '' closure[inst] {x}
x : α
hx : x ∈ f ⁻¹' s
y : β
hy : y ∈ s
hcl : Membership.mem (γ := Set β) (closure[inst_1] {f x}) y
a : α
ha : Membership.mem (γ := Set α) (closure[inst] {x}) a
hay : f a = y
hP₂ :
  ∀ (hcl : f x ⤳ y) (a : α) (ha : Membership.mem (γ := Set α) (closure[inst] {x}) a) (hay : f a = y),
    Subtype.mk (p := fun (x : β) ↦ x ∈ s) y hy ∈
      s.restrictPreimage f '' closure[instTopologicalSpaceSubtype] {Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' s) x hx}
⊢ Subtype.mk (p := fun (x : β) ↦ x ∈ s) y hy ∈
    s.restrictPreimage f '' closure[instTopologicalSpaceSubtype] {Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' s) x hx}

Tactic:
rw [← specializes_iff_mem_closure] at hcl

Premises used: specializes_iff_mem_closure
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Goal:
α β : Type u_1
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set β
h : Continuous[inst, inst_1] f
h_1 : IsOpen[inst_1] s
hf : ∀ (x : α), closure[inst_1] {f x} ⊆ f '' closure[inst] {x}
x : α
hx : x ∈ f ⁻¹' s
y : β
hy : y ∈ s
hcl : f x ⤳ y
a : α
ha : Membership.mem (γ := Set α) (closure[inst] {x}) a
hay : f a = y
⊢ a ∈ f ⁻¹' s

Tactic:
simp [hay, hy]
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Goal:
α β : Type u_1
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set β
h : Continuous[inst, inst_1] f
h_1 : IsOpen[inst_1] s
hf : ∀ (x : α), closure[inst_1] {f x} ⊆ f '' closure[inst] {x}
x : α
hx : x ∈ f ⁻¹' s
y : β
hy : y ∈ s
hcl : f x ⤳ y
a : α
ha : Membership.mem (γ := Set α) (closure[inst] {x}) a
hay : f a = y
⊢ Membership.mem (γ := Set (↑(f ⁻¹' s) : Type u_1))
    (closure[instTopologicalSpaceSubtype] {Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' s) x hx})
    (Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' s) a ⋯)

Tactic:
simpa [closure_subtype]

Premises used: closure_subtype
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Goal:
α β : Type u_1
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set β
h : Continuous[inst, inst_1] f
h_1 : IsOpen[inst_1] s
hf : ∀ (x : α), closure[inst_1] {f x} ⊆ f '' closure[inst] {x}
x : α
hx : x ∈ f ⁻¹' s
y : β
hy : y ∈ s
hcl : f x ⤳ y
a : α
ha : Membership.mem (γ := Set α) (closure[inst] {x}) a
hay : f a = y
⊢ s.restrictPreimage f (Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' s) a ⋯) = Subtype.mk (p := fun (x : β) ↦ x ∈ s) y hy

Tactic:
simpa
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Goal:
α β : Type u_1
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set β
h : Continuous[inst, inst_1] f
h_1 : IsOpen[inst_1] s
hf : ∀ (x : α), closure[inst_1] {f x} ⊆ f '' closure[inst] {x}
x : α
hx : x ∈ f ⁻¹' s
y : β
hy : y ∈ s
hcl : f x ⤳ y
a : α
ha : Membership.mem (γ := Set α) (closure[inst] {x}) a
hay : f a = y
⊢ Subtype.mk (p := fun (x : β) ↦ x ∈ s) y hy ∈
    s.restrictPreimage f '' closure[instTopologicalSpaceSubtype] {Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' s) x hx}

Tactic:
exact ⟨⟨a, by simp [hay, hy]⟩, by simpa [closure_subtype], by simpa⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Goal:
α β : Type u_1
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
ι : Type u_1
U : ι → Opens β
hU : IsOpenCover U
h : Continuous[inst, inst_1] f
hsp : ∀ (i : ι), SpecializingMap ((U i).carrier.restrictPreimage f)
hP₃ :
  ∀
    (hsp :
      ∀ (i : ι) (x : (↑(f ⁻¹' (U i).carrier) : Type u_1)),
        closure[instTopologicalSpaceSubtype] {(U i).carrier.restrictPreimage f x} ⊆
          (U i).carrier.restrictPreimage f '' closure[instTopologicalSpaceSubtype] {x})
    (x : α), closure[inst_1] {f x} ⊆ f '' closure[inst] {x}
⊢ SpecializingMap f

Tactic:
simp_rw [specializingMap_iff_closure_singleton_subset] at hsp ⊢

Premises used: specializingMap_iff_closure_singleton_subset
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Goal:
α β : Type u_1
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
ι : Type u_1
U : ι → Opens β
hU : IsOpenCover U
h : Continuous[inst, inst_1] f
hsp :
  ∀ (i : ι) (x : (↑(f ⁻¹' (U i).carrier) : Type u_1)),
    closure[instTopologicalSpaceSubtype] {(U i).carrier.restrictPreimage f x} ⊆
      (U i).carrier.restrictPreimage f '' closure[instTopologicalSpaceSubtype] {x}
x : α
y : β
hy : Membership.mem (γ := Set β) (closure[inst_1] {f x}) y
⊢ ∃ (i : ι), y ∈ U i

Tactic:
have : ∃ i, y ∈ U i := Opens.mem_iSup.mp (hU ▸ Opens.mem_top _)
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Goal:
α β : Type u_1
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
ι : Type u_1
U : ι → Opens β
hU : IsOpenCover U
h : Continuous[inst, inst_1] f
hsp :
  ∀ (i : ι) (x : (↑(f ⁻¹' (U i).carrier) : Type u_1)),
    closure[instTopologicalSpaceSubtype] {(U i).carrier.restrictPreimage f x} ⊆
      (U i).carrier.restrictPreimage f '' closure[instTopologicalSpaceSubtype] {x}
x : α
y : β
hy : Membership.mem (γ := Set β) (closure[inst_1] {f x}) y
this : ∃ (i : ι), y ∈ U i
hP₃ : ∀ (i : ι) (hi : y ∈ U i), y ∈ f '' closure[inst] {x}
⊢ y ∈ f '' closure[inst] {x}

Tactic:
obtain ⟨i, hi⟩ := this
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Goal:
α β : Type u_1
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
ι : Type u_1
U : ι → Opens β
hU : IsOpenCover U
h : Continuous[inst, inst_1] f
hsp :
  ∀ (i : ι) (x : (↑(f ⁻¹' (U i).carrier) : Type u_1)),
    closure[instTopologicalSpaceSubtype] {(U i).carrier.restrictPreimage f x} ⊆
      (U i).carrier.restrictPreimage f '' closure[instTopologicalSpaceSubtype] {x}
x : α
y : β
hy : Membership.mem (γ := Set β) (closure[inst_1] {f x}) y
i : ι
hi : y ∈ U i
hP₃ : ∀ (hy : f x ⤳ y) (i : ι) (hi : y ∈ U i), y ∈ f '' closure[inst] {x}
⊢ y ∈ f '' closure[inst] {x}

Tactic:
rw [← specializes_iff_mem_closure] at hy

Premises used: specializes_iff_mem_closure
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Goal:
α β : Type u_1
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
ι : Type u_1
U : ι → Opens β
hU : IsOpenCover U
h : Continuous[inst, inst_1] f
hsp :
  ∀ (i : ι) (x : (↑(f ⁻¹' (U i).carrier) : Type u_1)),
    closure[instTopologicalSpaceSubtype] {(U i).carrier.restrictPreimage f x} ⊆
      (U i).carrier.restrictPreimage f '' closure[instTopologicalSpaceSubtype] {x}
x : α
y : β
hy : f x ⤳ y
i : ι
hi : y ∈ U i
⊢ f x ∈ U i

Tactic:
have hfx : f x ∈ U i := (U i).2.stableUnderGeneralization hy hi
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Goal:
α β : Type u_1
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
ι : Type u_1
U : ι → Opens β
hU : IsOpenCover U
h : Continuous[inst, inst_1] f
hsp :
  ∀ (i : ι) (x : (↑(f ⁻¹' (U i).carrier) : Type u_1)),
    closure[instTopologicalSpaceSubtype] {(U i).carrier.restrictPreimage f x} ⊆
      (U i).carrier.restrictPreimage f '' closure[instTopologicalSpaceSubtype] {x}
x : α
y : β
hy : f x ⤳ y
i : ι
hi : y ∈ U i
hfx : f x ∈ U i
simp : Membership.mem (γ := Set β) (closure[inst_1] {f x}) y
⊢ Membership.mem (γ := Set ↥(U i))
    (closure[instTopologicalSpaceSubtype] {Subtype.mk (p := fun (x : β) ↦ x ∈ U i) (f x) hfx})
    (Subtype.mk (p := fun (x : β) ↦ x ∈ U i) y hi)

Tactic:
simp only [closure_subtype, Set.image_singleton]

Premises used: Set.image_singleton, closure_subtype
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Goal:
α β : Type u_1
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
ι : Type u_1
U : ι → Opens β
hU : IsOpenCover U
h : Continuous[inst, inst_1] f
hsp :
  ∀ (i : ι) (x : (↑(f ⁻¹' (U i).carrier) : Type u_1)),
    closure[instTopologicalSpaceSubtype] {(U i).carrier.restrictPreimage f x} ⊆
      (U i).carrier.restrictPreimage f '' closure[instTopologicalSpaceSubtype] {x}
x : α
y : β
hy : f x ⤳ y
i : ι
hi : y ∈ U i
hfx : f x ∈ U i
rwa rwa₁ rwa₂ rwa₃ : f x ⤳ y
⊢ Membership.mem (γ := Set β) (closure[inst_1] {f x}) y

Tactic:
rwa [← specializes_iff_mem_closure]

Premises used: specializes_iff_mem_closure
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Goal:
α β : Type u_1
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
ι : Type u_1
U : ι → Opens β
hU : IsOpenCover U
h : Continuous[inst, inst_1] f
hsp :
  ∀ (i : ι) (x : (↑(f ⁻¹' (U i).carrier) : Type u_1)),
    closure[instTopologicalSpaceSubtype] {(U i).carrier.restrictPreimage f x} ⊆
      (U i).carrier.restrictPreimage f '' closure[instTopologicalSpaceSubtype] {x}
x : α
y : β
hy : f x ⤳ y
i : ι
hi : y ∈ U i
hfx : f x ∈ U i
⊢ Membership.mem (γ := Set ↥(U i))
    (closure[instTopologicalSpaceSubtype] {Subtype.mk (p := fun (x : β) ↦ x ∈ U i) (f x) hfx})
    (Subtype.mk (p := fun (x : β) ↦ x ∈ U i) y hi)

Tactic:
have hy : (⟨y, hi⟩ : U i) ∈ closure {⟨f x, hfx⟩} := by
      simp only [closure_subtype, Set.image_singleton]
      rwa [← specializes_iff_mem_closure]
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Goal:
α β : Type u_1
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
ι : Type u_1
U : ι → Opens β
hU : IsOpenCover U
h : Continuous[inst, inst_1] f
hsp :
  ∀ (i : ι) (x : (↑(f ⁻¹' (U i).carrier) : Type u_1)),
    closure[instTopologicalSpaceSubtype] {(U i).carrier.restrictPreimage f x} ⊆
      (U i).carrier.restrictPreimage f '' closure[instTopologicalSpaceSubtype] {x}
x : α
y : β
hy_1 : f x ⤳ y
i : ι
hi : y ∈ U i
hfx : f x ∈ U i
hy :
  Membership.mem (γ := Set ↥(U i))
    (closure[instTopologicalSpaceSubtype] {Subtype.mk (p := fun (x : β) ↦ x ∈ U i) (f x) hfx})
    (Subtype.mk (p := fun (x : β) ↦ x ∈ U i) y hi)
hP₃ :
  ∀ (a : (↑(f ⁻¹' (U i).carrier) : Type u_1))
    (ha :
      Membership.mem (γ := Set (↑(f ⁻¹' (U i).carrier) : Type u_1))
        (closure[instTopologicalSpaceSubtype] {Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' (U i).carrier) x hfx}) a)
    (hay : (U i).carrier.restrictPreimage f a = Subtype.mk (p := fun (x : β) ↦ x ∈ U i) y hi),
    y ∈ f '' closure[inst] {x}
⊢ y ∈ f '' closure[inst] {x}

Tactic:
obtain ⟨a, ha, hay⟩ := hsp i ⟨x, hfx⟩ hy

Premises used: Subtype.mk
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Goal:
α β : Type u_1
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
ι : Type u_1
U : ι → Opens β
hU : IsOpenCover U
h : Continuous[inst, inst_1] f
hsp :
  ∀ (i : ι) (x : (↑(f ⁻¹' (U i).carrier) : Type u_1)),
    closure[instTopologicalSpaceSubtype] {(U i).carrier.restrictPreimage f x} ⊆
      (U i).carrier.restrictPreimage f '' closure[instTopologicalSpaceSubtype] {x}
x : α
y : β
hy_1 : f x ⤳ y
i : ι
hi : y ∈ U i
hfx : f x ∈ U i
hy :
  Membership.mem (γ := Set ↥(U i))
    (closure[instTopologicalSpaceSubtype] {Subtype.mk (p := fun (x : β) ↦ x ∈ U i) (f x) hfx})
    (Subtype.mk (p := fun (x : β) ↦ x ∈ U i) y hi)
a : (↑(f ⁻¹' (U i).carrier) : Type u_1)
ha :
  Membership.mem (γ := Set (↑(f ⁻¹' (U i).carrier) : Type u_1))
    (closure[instTopologicalSpaceSubtype] {Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' (U i).carrier) x hfx}) a
hay : (U i).carrier.restrictPreimage f a = Subtype.mk (p := fun (x : β) ↦ x ∈ U i) y hi
⊢ Membership.mem (γ := Set α)
    (closure[inst]
      (Set.image (α := { a : α // a ∈ f ⁻¹' (U i).carrier }) (Subtype.val (p := fun (a : α) ↦ a ∈ f ⁻¹' (U i).carrier))
        {Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' (U i).carrier) x hfx}))
    (↑a : α)

Tactic:
rw [closure_subtype] at ha

Premises used: closure_subtype