awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : SurjectiveOnStalks f
hf : Function.Injective (α := ↥X) (β := ↥Y) ⇑f
h₁ :
  Function.Injective (α :=
    (↑(↑((Scheme.forgetToLocallyRingedSpace ⋙ LocallyRingedSpace.forgetToSheafedSpace).obj X).toPresheafedSpace :
          TopCat) :
      Type u))
    (β :=
    (↑(↑((Scheme.forgetToLocallyRingedSpace ⋙ LocallyRingedSpace.forgetToSheafedSpace).obj Y).toPresheafedSpace :
          TopCat) :
      Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
          ((Scheme.forgetToLocallyRingedSpace ⋙ LocallyRingedSpace.forgetToSheafedSpace).map f).hom.base) :
      (a :
          (↑(↑((Scheme.forgetToLocallyRingedSpace ⋙ LocallyRingedSpace.forgetToSheafedSpace).obj X).toPresheafedSpace :
                TopCat) :
            Type u)) →
        (↑(↑((Scheme.forgetToLocallyRingedSpace ⋙ LocallyRingedSpace.forgetToSheafedSpace).obj Y).toPresheafedSpace :
              TopCat) :
          Type u))
⊢ Mono ((Scheme.forgetToLocallyRingedSpace ⋙ LocallyRingedSpace.forgetToSheafedSpace).map f)
have h₂ : ∀
  (x :
    (↑(↑((Scheme.forgetToLocallyRingedSpace ⋙ LocallyRingedSpace.forgetToSheafedSpace).obj X).toPresheafedSpace :
          TopCat) :
      Type u)),
  Epi (X :=
    ((Scheme.forgetToLocallyRingedSpace ⋙ LocallyRingedSpace.forgetToSheafedSpace).obj Y).presheaf.stalk
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            ((Scheme.forgetToLocallyRingedSpace ⋙ LocallyRingedSpace.forgetToSheafedSpace).map f).hom.base :
          (a :
              (↑(↑((Scheme.forgetToLocallyRingedSpace ⋙ LocallyRingedSpace.forgetToSheafedSpace).obj
                          X).toPresheafedSpace :
                    TopCat) :
                Type u)) →
            (↑(↑((Scheme.forgetToLocallyRingedSpace ⋙ LocallyRingedSpace.forgetToSheafedSpace).obj
                        Y).toPresheafedSpace :
                  TopCat) :
              Type u))
        x))
    (PresheafedSpace.Hom.stalkMap
      ((Scheme.forgetToLocallyRingedSpace ⋙ LocallyRingedSpace.forgetToSheafedSpace).map f).hom x)
Tactic: apply SheafedSpace.mono_of_base_injective_of_stalk_epi
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap (goal)
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ IsZariskiLocalAtTarget.{u_1}
    (topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] ↦ Function.Injective)
have refine : ∀ {α β : Type u_1} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) (ι : Type u_1)
  (U : ι → Opens β) (H : IsOpenCover U),
  Continuous f →
    ∀ (hf : ∀ (i : ι), Function.Injective ((U i).carrier.restrictPreimage f)) (x₁ x₂ : α) (e : f x₁ = f x₂), x₁ = x₂
Tactic: refine topologically_isZariskiLocalAtTarget _ (fun _ s _ _ h ↦ h.restrictPreimage s)
    fun f ι U H _ hf x₁ x₂ e ↦ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap (goal)
Goal:
X Y Z : Scheme
f_1 : X ⟶ Y
g : Y ⟶ Z
α β : Type u_1
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
ι : Type u_1
U : ι → Opens β
H : IsOpenCover U
h : Continuous[inst, inst_1] f
hf : ∀ (i : ι), Function.Injective ((U i).carrier.restrictPreimage f)
x₁ x₂ : α
e : f x₁ = f x₂
⊢ x₁ = x₂
have obtain : ∀ (i : ι) (hxi : f x₁ ∈ U i), x₁ = x₂
Tactic: obtain ⟨i, hxi⟩ : ∃ i, f x₁ ∈ U i := by simpa using congr(f x₁ ∈ $H)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap (goal)
Goal:
⊢ @Surjective = topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] ↦ Function.Surjective
have h : ∀ (x x_1 : Scheme.{u_1}) (x_2 : x ⟶ x_1),
  Surjective x_2 ↔
    topologically (fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] ↦ Function.Surjective) x_2
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap (hypothesis)
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ IsZariskiLocalAtTarget @Surjective
have this : MorphismProperty.RespectsIso @Surjective
Tactic: have : MorphismProperty.RespectsIso @Surjective := inferInstance
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap (goal)
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
this : MorphismProperty.RespectsIso @Surjective
⊢ IsZariskiLocalAtTarget @Surjective
have rw : ∀
  (this :
    (topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] ↦ Function.Surjective).RespectsIso),
  IsZariskiLocalAtTarget.{u_1}
    (topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] ↦ Function.Surjective)
Tactic: rw [surjective_eq_topologically] at this ⊢
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap (goal)
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
this : (topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] ↦ Function.Surjective).RespectsIso
⊢ IsZariskiLocalAtTarget.{u_1}
    (topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] ↦ Function.Surjective)
have refine : ∀ {α β : Type u_1} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) {ι : Type u_1}
  (U : ι → Opens β),
  IsOpenCover U →
    Continuous f → (∀ (i : ι), Function.Surjective ((U i).carrier.restrictPreimage f)) → Function.Surjective f
Tactic: refine topologically_isZariskiLocalAtTarget _ (fun _ s _ _ h ↦ h.restrictPreimage s) ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap (goal)
Goal:
X Y Z : Scheme
f_1 : X ⟶ Y
g : Y ⟶ Z
this : (topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] ↦ Function.Surjective).RespectsIso
α β : Type u_1
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
ι : Type u_1
U : ι → Opens β
H : IsOpenCover U
h : Continuous[inst, inst_1] f
hf : ∀ (i : ι), Function.Surjective ((U i).carrier.restrictPreimage f)
x : β
⊢ ∃ (a : α), f a = x
have obtain : ∀ (i : ι) (hxi : x ∈ U i), ∃ (a : α), f a = x
Tactic: obtain ⟨i, hxi⟩ : ∃ i, x ∈ U i := by simpa using congr(x ∈ $H)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap (goal)
Goal:
X Y Z : Scheme
f_1 : X ⟶ Y
g : Y ⟶ Z
this : (topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] ↦ Function.Surjective).RespectsIso
α β : Type u_1
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
ι : Type u_1
U : ι → Opens β
H : IsOpenCover U
h : Continuous[inst, inst_1] f
hf : ∀ (i : ι), Function.Surjective ((U i).carrier.restrictPreimage f)
x : β
i : ι
hxi : x ∈ U i
⊢ ∃ (a : α), f a = x
have obtain : ∀ (y : α) (property : y ∈ f ⁻¹' (U i).carrier)
  (hy :
    (U i).carrier.restrictPreimage f (Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' (U i).carrier) y property) =
      Subtype.mk (p := fun (x : β) ↦ x ∈ (U i).carrier) x hxi),
  ∃ (a : α), f a = x
Tactic: obtain ⟨⟨y, _⟩, hy⟩ := hf i ⟨x, hxi⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap (goal)
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
e : X ⟶ Y
inst : Surjective e
hge : e ≫ g = f
⊢ Eq (α := Set ↥S) (Set.range (ι := ↥X) ⇑f) (Set.range (ι := ↥Y) ⇑g)
have rw : Eq (α := Set ↥S) (Set.range (ι := ↥X) ⇑(e ≫ g)) (Set.range (ι := ↥Y) ⇑g)
Tactic: rw [← hge]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap (goal)
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
e : X ⟶ Y
inst : Surjective e
hge : e ≫ g = f
s : ↥S
⊢ Membership.mem (γ := Set ↥S) (Set.range (ι := ↥X) ⇑f) s ↔ Membership.mem (γ := Set ↥S) (Set.range (ι := ↥Y) ⇑g) s
have rw : Membership.mem (γ := Set ↥S) (Set.range (ι := ↥Y) ⇑g) s ↔ Membership.mem (γ := Set ↥S) (Set.range (ι := ↥Y) ⇑g) s
Tactic: rw [range_eq_range_of_surjective f g e hge]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap (goal)
Goal:
X : Scheme
ι : Type v
inst : Small.{u, v} ι
Y : ι → Scheme
f : (i : ι) → Y i ⟶ X
H : Eq.{u + 1} (α := Set ↥X) (⋃ (i : ι), Set.range (ι := ↥(Y i)) ⇑(f i)) Set.univ
⊢ Surjective (X := ∐ Y) (Limits.Sigma.desc f)
have refine : ∀ (x : ↥X), ∃ (a : ↥(∐ Y)), (Limits.Sigma.desc f) a = x
Tactic: refine ⟨fun x ↦ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap (hypothesis)
Goal:
X : Scheme
ι : Type v
inst : Small.{u, v} ι
Y : ι → Scheme
f : (i : ι) → Y i ⟶ X
H : Eq.{u + 1} (α := Set ↥X) (⋃ (i : ι), Set.range (ι := ↥(Y i)) ⇑(f i)) Set.univ
x : ↥X
⊢ ∃ (a : ↥(∐ Y)), (Limits.Sigma.desc f) a = x
have H₁ : ∀ (x : ↥X), ∃ (i : ι), Membership.mem (γ := Set ↥X) (Set.range (ι := ↥(Y i)) ⇑(f i)) x
Tactic: simp_rw [Set.eq_univ_iff_forall, Set.mem_iUnion] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap (goal)
Goal:
X : Scheme
ι : Type v
inst : Small.{u, v} ι
Y : ι → Scheme
f : (i : ι) → Y i ⟶ X
x : ↥X
H : ∀ (x : ↥X), ∃ (i : ι), Membership.mem (γ := Set ↥X) (Set.range (ι := ↥(Y i)) ⇑(f i)) x
⊢ ∃ (a : ↥(∐ Y)), (Limits.Sigma.desc f) a = x
have obtain : ∀ (i : ι) (x : ↥(Y i)), ∃ (a : ↥(∐ Y)), Eq (α := ↥X) ((Limits.Sigma.desc f) a : ↥X) ((f i) x : ↥X)
Tactic: obtain ⟨i, x, rfl⟩ := H x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap (goal)
Goal:
X : Scheme
ι : Type v
inst : Small.{u, v} ι
Y : ι → Scheme
f : (i : ι) → Y i ⟶ X
H : ∀ (x : ↥X), ∃ (i : ι), Membership.mem (γ := Set ↥X) (Set.range (ι := ↥(Y i)) ⇑(f i)) x
i : ι
x : ↥(Y i)
⊢ ∃ (a : ↥(∐ Y)), Eq (α := ↥X) ((Limits.Sigma.desc f) a : ↥X) ((f i) x : ↥X)
have h : Eq (α := ↥X) ((Limits.Sigma.desc f) ((Limits.Sigma.ι Y i) x : ↥(∐ Y)) : ↥X) ((f i) x : ↥X)
Tactic: use Limits.Sigma.ι Y i x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap (goal)
Goal:
X : Scheme
ι : Type v
inst : Small.{u, v} ι
Y : ι → Scheme
f : (i : ι) → Y i ⟶ X
H : ∀ (x : ↥X), ∃ (i : ι), Membership.mem (γ := Set ↥X) (Set.range (ι := ↥(Y i)) ⇑(f i)) x
i : ι
x : ↥(Y i)
⊢ Eq (α := ↥X) ((Limits.Sigma.desc f) ((Limits.Sigma.ι Y i) x : ↥(∐ Y)) : ↥X) ((f i) x : ↥X)
have h : Eq (α := ↥X) ((CategoryStruct.comp (Y := ∐ Y) (Limits.Sigma.ι Y i) (Limits.Sigma.desc f)) x : ↥X) ((f i) x : ↥X)
Tactic: rw [← Scheme.Hom.comp_apply, Limits.Sigma.ι_desc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap (goal)
Goal:
X : Scheme
ι : Type v
inst : Small.{u, v} ι
Y : ι → Scheme
f : (i : ι) → Y i ⟶ X
H : ∀ (x : ↥X), ∃ (i : ι), Membership.mem (γ := Set ↥X) (Set.range (ι := ↥(Y i)) ⇑(f i)) x
i : ι
x : ↥(Y i)
h : Eq (α := ↥X) ((CategoryStruct.comp (Y := ∐ Y) (Limits.Sigma.ι Y i) (Limits.Sigma.desc f)) x : ↥X) ((f i) x : ↥X)
⊢ Eq (α := ↥X) ((Limits.Sigma.desc f) ((Limits.Sigma.ι Y i) x : ↥(∐ Y)) : ↥X) ((f i) x : ↥X)
have h₁ : Eq (α := ↥X) ((f i) x : ↥X) ((f i) x : ↥X)
Tactic: rw [← Scheme.Hom.comp_apply, Limits.Sigma.ι_desc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap (goal)
Goal:
X_1 Y Z : Scheme
f_1 : X_1 ⟶ Y
g : Y ⟶ Z
P : MorphismProperty Scheme
X S : Scheme
f : X ⟶ S
hf : P f
inst : Surjective f
⊢ Presieve.singleton f ∈ (precoverage P).coverings S
have rw : Function.Surjective (α := ↥X) (β := ↥S) ⇑f ∧ P f
Tactic: rw [singleton_mem_precoverage_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap (goal)
Goal:
⊢ @IsDominant = topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] ↦ DenseRange
have h : ∀ (x x_1 : Scheme.{u_1}) (x_2 : x ⟶ x_1),
  IsDominant x_2 ↔ topologically (fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] ↦ DenseRange) x_2
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap (goal)
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
H : IsDominant (f ≫ g)
⊢ IsDominant g
have rw : ∀ (H : Subset (α := Set ↥Z) Set.univ (closure (Set.range (ι := ↥X) ⇑(f ≫ g)))),
  Subset (α := Set ↥Z) Set.univ (closure (Set.range (ι := ↥Y) ⇑g))
Tactic: rw [isDominant_iff, denseRange_iff_closure_range, ← Set.univ_subset_iff] at H ⊢
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsDominant f
hf : IsClosed (X := ↥Y) (Set.range (ι := ↥X) ⇑f)
⊢ Function.Surjective (α := ↥X) (β := ↥Y) ⇑f
have rw : Eq (α := Set ↥Y) (Set.range (ι := ↥X) ⇑f) Set.univ
Tactic: rw [← Set.range_eq_univ, ← hf.closure_eq, f.denseRange.closure_range]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap (goal)
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
⊢ Function.Surjective (α := ↥X) (β := ↥Y) ⇑f
have rw₁ : Eq (α := Set ↥Y) (closure (Set.range (ι := ↥X) ⇑f)) Set.univ
Tactic: rw [← Set.range_eq_univ, ← hf.closure_eq, f.denseRange.closure_range]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap (goal)
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
⊢ Function.Surjective (α := ↥X) (β := ↥Y) ⇑f
have rw₂ : Eq.{u + 1} (α := Set ↥Y) Set.univ Set.univ
Tactic: rw [← Set.range_eq_univ, ← hf.closure_eq, f.denseRange.closure_range]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap (goal)
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
H : IsDominant (f ≫ g)
inst : IsOpenImmersion g
⊢ IsDominant f
have rw : ∀ (H : Dense (X := ↥Z) (Set.range (ι := ↥X) ⇑(f ≫ g))) [IsOpenImmersion g], Dense (X := ↥Y) (Set.range (ι := ↥X) ⇑f)
Tactic: rw [isDominant_iff, DenseRange] at H ⊢
Cleared hypotheses: H, inst
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap (hypothesis)
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 := ↥Y) (Set.range (ι := ↥X) ⇑f)
have H₁ : 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
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap (goal)
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.range (ι := ↥X) ⇑f)
have h : Eq (α := Set ↥Y) (Set.range (ι := ↥X) ⇑f)
  (Set.preimage (β := ↥Z) (⇑g) (Set.image (α := ↥Y) (⇑g) (Set.range (ι := ↥X) ⇑f)))
Tactic: convert! H.preimage g.isOpenEmbedding.isOpenMap using 1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap (goal)
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))
⊢ Eq (α := Set ↥Y) (Set.range (ι := ↥X) ⇑f)
    (Set.preimage (β := ↥Z) (⇑g) (Set.image (α := ↥Y) (⇑g) (Set.range (ι := ↥X) ⇑f)))
have h : Eq (α := Set ↥Y) (Set.range (ι := ↥X) ⇑f) (Set.range (ι := ↥X) ⇑f)
Tactic: rw [Set.preimage_image_eq _ g.isOpenEmbedding.injective]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap (goal)
Goal:
⊢ (topologically @SpecializingMap).RespectsIso
have hP₁ : ∀ {α β : Type u_1} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α ≃ₜ β),
  SpecializingMap (X := α) (Y := β) (⇑f : (a : α) → β)
Tactic: apply topologically_respectsIso
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap (goal)
Goal:
hP₁ :
  ∀ {α β : Type u_1} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α ≃ₜ β),
    SpecializingMap (X := α) (Y := β) (⇑f : (a : α) → β)
⊢ (topologically @SpecializingMap).RespectsIso
have hP₂ : ∀ {α β γ : Type u_1} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : TopologicalSpace γ] (f : α → β)
  (g : β → γ), SpecializingMap f → SpecializingMap g → SpecializingMap (g ∘ f)
Tactic: apply topologically_respectsIso
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap (goal)
Goal:
⊢ IsZariskiLocalAtTarget.{u_1} (topologically @SpecializingMap)
have hP₂ : ∀ {α β : Type u_1} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) (s : Set β),
  Continuous f → IsOpen s → SpecializingMap f → SpecializingMap (s.restrictPreimage f)
Tactic: apply topologically_isZariskiLocalAtTarget
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap (goal)
Goal:
hP₂ :
  ∀ {α β : Type u_1} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) (s : Set β),
    Continuous f → IsOpen s → SpecializingMap f → SpecializingMap (s.restrictPreimage f)
⊢ IsZariskiLocalAtTarget.{u_1} (topologically @SpecializingMap)
have 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
Tactic: apply topologically_isZariskiLocalAtTarget
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap (goal)
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
⊢ SpecializingMap (s.restrictPreimage f)
have 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}
Tactic: rw [specializingMap_iff_closure_singleton_subset] at hf ⊢
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap (goal)
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
⊢ 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}
have 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}
Tactic: ⟨y, hy⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap (hypothesis)
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)
⊢ Subtype.mk (p := fun (x : β) ↦ x ∈ s) y hy ∈
    s.restrictPreimage f '' closure[instTopologicalSpaceSubtype] {Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' s) x hx}
have hcl₁ : Membership.mem (γ := Set β) (closure[inst_1] {f x}) y
Tactic: simp only [closure_subtype, Set.restrictPreimage_mk, Set.image_singleton] at hcl
Cleared hypotheses: hcl
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap (goal)
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
⊢ Subtype.mk (p := fun (x : β) ↦ x ∈ s) y hy ∈
    s.restrictPreimage f '' closure[instTopologicalSpaceSubtype] {Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' s) x hx}
have 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}
Tactic: obtain ⟨a, ha, hay⟩ := hf x hcl
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap (goal)
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
⊢ Subtype.mk (p := fun (x : β) ↦ x ∈ s) y hy ∈
    s.restrictPreimage f '' closure[instTopologicalSpaceSubtype] {Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' s) x hx}
have 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}
Tactic: rw [← specializes_iff_mem_closure] at hcl
Cleared hypotheses: hcl, a, ha, hay
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap (goal)
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)
⊢ SpecializingMap f
have 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}
Tactic: simp_rw [specializingMap_iff_closure_singleton_subset] at hsp ⊢
Cleared hypotheses: hsp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap (hypothesis)
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
⊢ y ∈ f '' closure[inst] {x}
have this : ∃ (i : ι), y ∈ U i
Tactic: have : ∃ i, y ∈ U i := Opens.mem_iSup.mp (hU ▸ Opens.mem_top _)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap (goal)
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
⊢ y ∈ f '' closure[inst] {x}
have hP₃ : ∀ (i : ι) (hi : y ∈ U i), y ∈ f '' closure[inst] {x}
Tactic: obtain ⟨i, hi⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap (goal)
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
⊢ y ∈ f '' closure[inst] {x}
have hP₃ : ∀ (hy : f x ⤳ y) (i : ι) (hi : y ∈ U i), y ∈ f '' closure[inst] {x}
Tactic: rw [← specializes_iff_mem_closure] at hy
Cleared hypotheses: hy, i, hi