awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
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₂
⊢ ∃ (i : ι), f x₁ ∈ U i

Tactic:
simpa using congr(f x₁ ∈ $H)
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
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₂
obtain : ∀ (i : ι) (hxi : f x₁ ∈ U i), x₁ = x₂
⊢ x₁ = x₂

Tactic:
obtain ⟨i, hxi⟩ : ∃ i, f x₁ ∈ U i := by simpa using congr(f x₁ ∈ $H)
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
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₂
i : ι
hxi : f x₁ ∈ U i
⊢ x₁ = x₂

Tactic:
congr(($(@hf i ⟨x₁, hxi⟩ ⟨x₂, show f x₂ ∈ U i from e ▸ hxi⟩ (Subtype.ext e))).1)

Premises used: congrArg, id, Subtype.val, Subtype.ext
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
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₂
i : ι
hxi : f x₁ ∈ U i
⊢ x₁ = x₂

Tactic:
exact congr(($(@hf i ⟨x₁, hxi⟩ ⟨x₂, show f x₂ ∈ U i from e ▸ hxi⟩ (Subtype.ext e))).1)
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Goal:
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
⊢ @Surjective = topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] ↦ Function.Surjective

Tactic:
ext
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Goal:
x x_1 : Scheme
x_2 : x ⟶ x_1
⊢ Surjective x_2 ↔
    topologically (fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] ↦ Function.Surjective) x_2

Tactic:
surjective_iff _

Premises used: AlgebraicGeometry.surjective_iff, AlgebraicGeometry.topologically
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Goal:
x x_1 : Scheme
x_2 : x ⟶ x_1
⊢ Surjective x_2 ↔
    topologically (fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] ↦ Function.Surjective) x_2

Tactic:
exact surjective_iff _

Premises used: AlgebraicGeometry.surjective_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Surjective f
⊢ Function.Surjective (α := ↥X) (β := ↥Y) ⇑f

Tactic:
Surjective.surj

Premises used: AlgebraicGeometry.Surjective.surj
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : IsIso f
⊢ Surjective f

Tactic:
⟨f.homeomorph.surjective⟩

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

Tactic:
⟨g.surjective.comp f.surjective⟩

Premises used: AlgebraicGeometry.Surjective.mk, Function.Surjective.comp, AlgebraicGeometry.Scheme.Hom.surjective
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Goal:
X Y Z : Scheme
f_1 : X ⟶ Y
g : Y ⟶ Z
inst : Nonempty.{u + 1} ↥X
inst_1 : Subsingleton.{u + 1} ↥Y
f : X ⟶ Y
⊢ Surjective f

Tactic:
⟨Function.surjective_to_subsingleton _⟩

Premises used: Function.surjective_to_subsingleton, AlgebraicGeometry.Surjective.mk
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : Surjective f
⊢ Surjective (f ≫ g) ↔ Surjective g

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

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

Tactic:
surjective_eq_topologically ▸ topologically_respectsIso _ (fun e ↦ e.surjective)
    (fun _ _ hf hg ↦ hg.comp hf)

Premises used: Eq.rec, AlgebraicGeometry.topologically_respectsIso, AlgebraicGeometry.surjective_eq_topologically, Function.Surjective.comp, Eq.symm, Homeomorph.surjective
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ MorphismProperty.RespectsIso @Surjective

Tactic:
have : MorphismProperty.RespectsIso @Surjective := inferInstance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
this : MorphismProperty.RespectsIso @Surjective
rw :
  ∀
    (this :
      (topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] ↦ Function.Surjective).RespectsIso),
    IsZariskiLocalAtTarget.{u_1}
      (topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] ↦ Function.Surjective)
⊢ IsZariskiLocalAtTarget @Surjective

Tactic:
rw [surjective_eq_topologically] at this ⊢

Premises used: AlgebraicGeometry.surjective_eq_topologically
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
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)

Tactic:
topologically_isZariskiLocalAtTarget _ (fun _ s _ _ h ↦ h.restrictPreimage s) ?_

Premises used: AlgebraicGeometry.topologically_isZariskiLocalAtTarget, Function.Surjective.restrictPreimage
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
this : (topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] ↦ Function.Surjective).RespectsIso
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
⊢ IsZariskiLocalAtTarget.{u_1}
    (topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] ↦ Function.Surjective)

Tactic:
refine topologically_isZariskiLocalAtTarget _ (fun _ s _ _ h ↦ h.restrictPreimage s) ?_

Premises used: AlgebraicGeometry.topologically_isZariskiLocalAtTarget
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Goal:
X Y Z : Scheme
f : 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 β),
    IsOpenCover U →
      Continuous f → (∀ (i : ι), Function.Surjective ((U i).carrier.restrictPreimage f)) → Function.Surjective f
⊢ ∀ [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:
_
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Goal:
X Y Z : Scheme
f : 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 β),
    IsOpenCover U →
      Continuous[inst, _] f →
        (∀ (i : ι), Function.Surjective ((U i).carrier.restrictPreimage f)) → Function.Surjective f
⊢ ∀ [inst_1 : TopologicalSpace β] (f : α → β) {ι : Type u_1} (U : ι → Opens β),
    IsOpenCover U →
      Continuous[inst, _] f →
        (∀ (i : ι), Function.Surjective ((U i).carrier.restrictPreimage f)) → Function.Surjective f

Tactic:
_
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
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
_ :
  Continuous[inst, inst_1] f →
    (∀ (i : ι), Function.Surjective ((U i).carrier.restrictPreimage f)) → Function.Surjective f
⊢ Continuous[inst, inst_1] f →
    (∀ (i : ι), Function.Surjective ((U i).carrier.restrictPreimage f)) → Function.Surjective f

Tactic:
_
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
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 : ι), x ∈ U i

Tactic:
simpa using congr(x ∈ $H)
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
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 : β
obtain : ∀ (i : ι) (hxi : x ∈ U i), ∃ (a : α), f a = x
⊢ ∃ (a : α), f a = x

Tactic:
obtain ⟨i, hxi⟩ : ∃ i, x ∈ U i := by simpa using congr(x ∈ $H)
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
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
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
⊢ ∃ (a : α), f a = x

Tactic:
obtain ⟨⟨y, _⟩, hy⟩ := hf i ⟨x, hxi⟩

Premises used: Subtype.mk
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
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
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:
⟨y, congr(($hy).1)⟩

Premises used: congrArg, id, Exists.intro, Subtype.val
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
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
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:
exact ⟨y, congr(($hy).1)⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Surjective f
⊢ Eq (α := Set ↥Y) (Set.range (ι := ↥X) ⇑f) Set.univ

Tactic:
simpa [Set.range_eq_univ] using f.surjective

Premises used: Set.range_eq_univ, AlgebraicGeometry.Scheme.Hom.surjective
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
e : X ⟶ Y
inst : Surjective e
hge : e ≫ g = f
rw : Eq (α := Set ↥S) (Set.range (ι := ↥X) ⇑(e ≫ g)) (Set.range (ι := ↥Y) ⇑g)
⊢ Eq (α := Set ↥S) (Set.range (ι := ↥X) ⇑f) (Set.range (ι := ↥Y) ⇑g)

Tactic:
rw [← hge]
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
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) ⇑(e ≫ g)) (Set.range (ι := ↥Y) ⇑g)

Tactic:
simp [Set.range_comp]

Premises used: Set.range_comp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
e : X ⟶ Y
inst : Surjective e
hge : e ≫ g = f
s : ↥S
rw rw₁ :
  Membership.mem (γ := Set ↥S) (Set.range (ι := ↥Y) ⇑g) s ↔ Membership.mem (γ := Set ↥S) (Set.range (ι := ↥Y) ⇑g) s
⊢ Membership.mem (γ := Set ↥S) (Set.range (ι := ↥X) ⇑f) s ↔ Membership.mem (γ := Set ↥S) (Set.range (ι := ↥Y) ⇑g) s

Tactic:
rw [range_eq_range_of_surjective f g e hge]

Premises used: AlgebraicGeometry.range_eq_range_of_surjective
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
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)

Tactic:
⟨fun x ↦ ?_⟩

Premises used: AlgebraicGeometry.Surjective.mk
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
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
refine : ∀ (x : ↥X), ∃ (a : ↥(∐ Y)), (Limits.Sigma.desc f) a = x
⊢ Surjective (X := ∐ Y) (Limits.Sigma.desc f)

Tactic:
refine ⟨fun x ↦ ?_⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
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
⊢ ∀ (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

Premises used: Set.eq_univ_iff_forall, Set.mem_iUnion
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
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
obtain : ∀ (i : ι) (x : ↥(Y i)), ∃ (a : ↥(∐ Y)), Eq (α := ↥X) ((Limits.Sigma.desc f) a : ↥X) ((f i) x : ↥X)
⊢ ∃ (a : ↥(∐ Y)), (Limits.Sigma.desc f) a = x

Tactic:
obtain ⟨i, x, rfl⟩ := H x

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
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) ((Limits.Sigma.desc f) ((Limits.Sigma.ι Y i) x : ↥(∐ Y)) : ↥X) ((f i) x : ↥X)
⊢ ∃ (a : ↥(∐ Y)), Eq (α := ↥X) ((Limits.Sigma.desc f) a : ↥X) ((f i) x : ↥X)

Tactic:
use Limits.Sigma.ι Y i x

Premises used: CategoryTheory.ConcreteCategory.hom, CategoryTheory.Limits.Sigma.ι, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.PresheafedSpace.Hom.base, DFunLike.coe
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
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)
h₁ h₂ : Eq (α := ↥X) ((f i) x : ↥X) ((f i) x : ↥X)
⊢ Eq (α := ↥X) ((Limits.Sigma.desc f) ((Limits.Sigma.ι Y i) x : ↥(∐ Y)) : ↥X) ((f i) x : ↥X)

Tactic:
rw [← Scheme.Hom.comp_apply, Limits.Sigma.ι_desc]

Premises used: AlgebraicGeometry.Scheme.Hom.comp_apply, CategoryTheory.Limits.Sigma.ι_desc
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Goal:
X_1 Y Z : Scheme
f : X_1 ⟶ Y
g : Y ⟶ Z
X : Scheme
P : MorphismProperty Scheme
𝒰 : Scheme.Cover (Scheme.precoverage P) X
⊢ Surjective.{u} (X := ∐ 𝒰.X) (Y := X) (Limits.Sigma.desc fun (i : 𝒰.I₀) ↦ 𝒰.f i)

Tactic:
Surjective.sigmaDesc_of_union_range_eq_univ 𝒰.iUnion_range

Premises used: AlgebraicGeometry.Scheme.Cover.iUnion_range, AlgebraicGeometry.Surjective.sigmaDesc_of_union_range_eq_univ
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
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
rw : Function.Surjective (α := ↥X) (β := ↥S) ⇑f ∧ P f
⊢ Presieve.singleton f ∈ (precoverage P).coverings S

Tactic:
rw [singleton_mem_precoverage_iff]

Premises used: AlgebraicGeometry.Scheme.singleton_mem_precoverage_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
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
⊢ Function.Surjective (α := ↥X) (β := ↥S) ⇑f ∧ P f

Tactic:
⟨f.surjective, hf⟩

Premises used: And.intro, AlgebraicGeometry.Scheme.Hom.surjective
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
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
⊢ Function.Surjective (α := ↥X) (β := ↥S) ⇑f ∧ P f

Tactic:
exact ⟨f.surjective, hf⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Goal:
P : MorphismProperty Scheme
X S : Scheme
f : X ⟶ S
hf : P f
inst : Surjective f
⊢ PreZeroHypercover.presieve₀.{u_1, u, u + 1} (cover (P := P) f hf).toPreZeroHypercover = Presieve.singleton f

Tactic:
simp [cover]

Premises used: AlgebraicGeometry.Scheme.Hom.cover
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Goal:
⊢ (topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap).RespectsIso

Tactic:
topologically_respectsIso _ (fun e ↦ e.isOpenMap) (fun _ _ hf hg ↦ hg.comp hf)

Premises used: IsOpenMap.comp, AlgebraicGeometry.topologically_respectsIso, Homeomorph.isOpenMap
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Goal:
⊢ IsZariskiLocalAtTarget.{u_1}
    (topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap)

Tactic:
topologically_isZariskiLocalAtTarget' _ fun _ _ _ hU _ ↦ hU.isOpenMap_iff_restrictPreimage

Premises used: AlgebraicGeometry.topologically_isZariskiLocalAtTarget', TopologicalSpace.IsOpenCover.isOpenMap_iff_restrictPreimage
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Goal:
⊢ IsZariskiLocalAtSource.{u_1}
    (topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap)

Tactic:
topologically_isZariskiLocalAtSource' (fun _ ↦ _) fun _ _ _ hU _ ↦ hU.isOpenMap_iff_comp

Premises used: TopologicalSpace.IsOpenCover.isOpenMap_iff_comp, AlgebraicGeometry.topologically_isZariskiLocalAtSource'
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Goal:
⊢ (topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] ↦ IsClosedMap).RespectsIso

Tactic:
topologically_respectsIso _ (fun e ↦ e.isClosedMap) (fun _ _ hf hg ↦ hg.comp hf)

Premises used: AlgebraicGeometry.topologically_respectsIso, Homeomorph.isClosedMap, IsClosedMap.comp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Goal:
⊢ IsZariskiLocalAtTarget.{u_1}
    (topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] ↦ IsClosedMap)

Tactic:
topologically_isZariskiLocalAtTarget' _ fun _ _ _ hU _ ↦ hU.isClosedMap_iff_restrictPreimage

Premises used: AlgebraicGeometry.topologically_isZariskiLocalAtTarget', TopologicalSpace.IsOpenCover.isClosedMap_iff_restrictPreimage
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Goal:
⊢ (topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] ↦ IsEmbedding).RespectsIso

Tactic:
topologically_respectsIso _ (fun e ↦ e.isEmbedding) (fun _ _ hf hg ↦ hg.comp hf)

Premises used: Homeomorph.isEmbedding, Topology.IsEmbedding.comp, AlgebraicGeometry.topologically_respectsIso
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Goal:
⊢ IsZariskiLocalAtTarget.{u_1}
    (topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] ↦ IsEmbedding)

Tactic:
topologically_isZariskiLocalAtTarget' _ fun _ _ _ hU ↦ hU.isEmbedding_iff_restrictPreimage

Premises used: AlgebraicGeometry.topologically_isZariskiLocalAtTarget', TopologicalSpace.IsOpenCover.isEmbedding_iff_restrictPreimage
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Goal:
⊢ (topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenEmbedding).RespectsIso

Tactic:
topologically_respectsIso _ (fun e ↦ e.isOpenEmbedding) (fun _ _ hf hg ↦ hg.comp hf)

Premises used: AlgebraicGeometry.topologically_respectsIso, Homeomorph.isOpenEmbedding, Topology.IsOpenEmbedding.comp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Goal:
⊢ IsZariskiLocalAtTarget.{u_1}
    (topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenEmbedding)

Tactic:
topologically_isZariskiLocalAtTarget' _ fun _ _ _ hU ↦ hU.isOpenEmbedding_iff_restrictPreimage

Premises used: AlgebraicGeometry.topologically_isZariskiLocalAtTarget', TopologicalSpace.IsOpenCover.isOpenEmbedding_iff_restrictPreimage
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Goal:
⊢ (topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] ↦ IsClosedEmbedding).RespectsIso

Tactic:
topologically_respectsIso _ (fun e ↦ e.isClosedEmbedding) (fun _ _ hf hg ↦ hg.comp hf)

Premises used: Topology.IsClosedEmbedding.comp, AlgebraicGeometry.topologically_respectsIso, Homeomorph.isClosedEmbedding
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Goal:
⊢ IsZariskiLocalAtTarget.{u_1}
    (topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] ↦ IsClosedEmbedding)

Tactic:
topologically_isZariskiLocalAtTarget' _ fun _ _ _ hU ↦ hU.isClosedEmbedding_iff_restrictPreimage

Premises used: AlgebraicGeometry.topologically_isZariskiLocalAtTarget', TopologicalSpace.IsOpenCover.isClosedEmbedding_iff_restrictPreimage
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Goal:
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
⊢ @IsDominant = topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] ↦ DenseRange

Tactic:
ext
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Goal:
x x_1 : Scheme
x_2 : x ⟶ x_1
⊢ IsDominant x_2 ↔ topologically (fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] ↦ DenseRange) x_2

Tactic:
isDominant_iff _

Premises used: AlgebraicGeometry.topologically, AlgebraicGeometry.isDominant_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Goal:
x x_1 : Scheme
x_2 : x ⟶ x_1
⊢ IsDominant x_2 ↔ topologically (fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] ↦ DenseRange) x_2

Tactic:
exact isDominant_iff _

Premises used: AlgebraicGeometry.isDominant_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsDominant f
⊢ DenseRange (X := ↥Y) (α := ↥X) ⇑f

Tactic:
IsDominant.denseRange

Premises used: AlgebraicGeometry.IsDominant.denseRange