awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
hf : diagonal (@Surjective) f
x₁ x₂ : ↥X
e : Eq (α := ↥Y) (f x₁ : ↥Y) (f x₂ : ↥Y)
t : ↥X
ht₁ : (pullback.fst f f) ((pullback.diagonal f) t : ↥(pullback.diagonalObj f)) = x₁
ht₂ : (pullback.snd f f) ((pullback.diagonal f) t : ↥(pullback.diagonalObj f)) = x₂
a : (pullback.fst f f) ((pullback.diagonal f) t : ↥(pullback.diagonalObj f)) = x₂
a₁ :
  Eq (α := ↥X) ((pullback.fst f f) ((pullback.diagonal f) t : ↥(pullback.diagonalObj f)) : ↥X)
    ((pullback.snd f f) ((pullback.diagonal f) t : ↥(pullback.diagonalObj f)) : ↥X)
⊢ x₁ = x₂
have a₂ : Eq (α := ↥X) ((CategoryStruct.comp (Y := pullback f f) (pullback.diagonal f) (pullback.fst f f)) t : ↥X)
  ((pullback.snd f f) ((pullback.diagonal f) t : ↥(pullback.diagonalObj f)) : ↥X)
Tactic: rw [← ht₁, ← ht₂, ← Scheme.Hom.comp_apply, ← Scheme.Hom.comp_apply, pullback.diagonal_fst,
      pullback.diagonal_snd]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
hf : diagonal (@Surjective) f
x₁ x₂ : ↥X
e : Eq (α := ↥Y) (f x₁ : ↥Y) (f x₂ : ↥Y)
t : ↥X
ht₁ : (pullback.fst f f) ((pullback.diagonal f) t : ↥(pullback.diagonalObj f)) = x₁
ht₂ : (pullback.snd f f) ((pullback.diagonal f) t : ↥(pullback.diagonalObj f)) = x₂
a : (pullback.fst f f) ((pullback.diagonal f) t : ↥(pullback.diagonalObj f)) = x₂
a₁ :
  Eq (α := ↥X) ((pullback.fst f f) ((pullback.diagonal f) t : ↥(pullback.diagonalObj f)) : ↥X)
    ((pullback.snd f f) ((pullback.diagonal f) t : ↥(pullback.diagonalObj f)) : ↥X)
a₂ :
  Eq (α := ↥X) ((CategoryStruct.comp (Y := pullback f f) (pullback.diagonal f) (pullback.fst f f)) t : ↥X)
    ((pullback.snd f f) ((pullback.diagonal f) t : ↥(pullback.diagonalObj f)) : ↥X)
⊢ x₁ = x₂
have a₃ : Eq (α := ↥X) ((CategoryStruct.comp (Y := pullback f f) (pullback.diagonal f) (pullback.fst f f)) t : ↥X)
  ((CategoryStruct.comp (Y := pullback f f) (pullback.diagonal f) (pullback.snd f f)) t : ↥X)
Tactic: rw [← ht₁, ← ht₂, ← Scheme.Hom.comp_apply, ← Scheme.Hom.comp_apply, pullback.diagonal_fst,
      pullback.diagonal_snd]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
hf : diagonal (@Surjective) f
x₁ x₂ : ↥X
e : Eq (α := ↥Y) (f x₁ : ↥Y) (f x₂ : ↥Y)
t : ↥X
ht₁ : (pullback.fst f f) ((pullback.diagonal f) t : ↥(pullback.diagonalObj f)) = x₁
ht₂ : (pullback.snd f f) ((pullback.diagonal f) t : ↥(pullback.diagonalObj f)) = x₂
a : (pullback.fst f f) ((pullback.diagonal f) t : ↥(pullback.diagonalObj f)) = x₂
a₁ :
  Eq (α := ↥X) ((pullback.fst f f) ((pullback.diagonal f) t : ↥(pullback.diagonalObj f)) : ↥X)
    ((pullback.snd f f) ((pullback.diagonal f) t : ↥(pullback.diagonalObj f)) : ↥X)
a₂ :
  Eq (α := ↥X) ((CategoryStruct.comp (Y := pullback f f) (pullback.diagonal f) (pullback.fst f f)) t : ↥X)
    ((pullback.snd f f) ((pullback.diagonal f) t : ↥(pullback.diagonalObj f)) : ↥X)
a₃ :
  Eq (α := ↥X) ((CategoryStruct.comp (Y := pullback f f) (pullback.diagonal f) (pullback.fst f f)) t : ↥X)
    ((CategoryStruct.comp (Y := pullback f f) (pullback.diagonal f) (pullback.snd f f)) t : ↥X)
⊢ x₁ = x₂
have a₄ : Eq (α := ↥X) ((𝟙 X) t : ↥X) ((CategoryStruct.comp (Y := pullback f f) (pullback.diagonal f) (pullback.snd f f)) t : ↥X)
Tactic: rw [← ht₁, ← ht₂, ← Scheme.Hom.comp_apply, ← Scheme.Hom.comp_apply, pullback.diagonal_fst,
      pullback.diagonal_snd]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
hf : diagonal (@Surjective) f
x₁ x₂ : ↥X
e : Eq (α := ↥Y) (f x₁ : ↥Y) (f x₂ : ↥Y)
t : ↥X
ht₁ : (pullback.fst f f) ((pullback.diagonal f) t : ↥(pullback.diagonalObj f)) = x₁
ht₂ : (pullback.snd f f) ((pullback.diagonal f) t : ↥(pullback.diagonalObj f)) = x₂
a : (pullback.fst f f) ((pullback.diagonal f) t : ↥(pullback.diagonalObj f)) = x₂
a₁ :
  Eq (α := ↥X) ((pullback.fst f f) ((pullback.diagonal f) t : ↥(pullback.diagonalObj f)) : ↥X)
    ((pullback.snd f f) ((pullback.diagonal f) t : ↥(pullback.diagonalObj f)) : ↥X)
a₂ :
  Eq (α := ↥X) ((CategoryStruct.comp (Y := pullback f f) (pullback.diagonal f) (pullback.fst f f)) t : ↥X)
    ((pullback.snd f f) ((pullback.diagonal f) t : ↥(pullback.diagonalObj f)) : ↥X)
a₃ :
  Eq (α := ↥X) ((CategoryStruct.comp (Y := pullback f f) (pullback.diagonal f) (pullback.fst f f)) t : ↥X)
    ((CategoryStruct.comp (Y := pullback f f) (pullback.diagonal f) (pullback.snd f f)) t : ↥X)
a₄ :
  Eq (α := ↥X) ((𝟙 X) t : ↥X)
    ((CategoryStruct.comp (Y := pullback f f) (pullback.diagonal f) (pullback.snd f f)) t : ↥X)
⊢ x₁ = x₂
have a₅ : Eq (α := ↥X) ((𝟙 X) t : ↥X) ((𝟙 X) t : ↥X)
Tactic: rw [← ht₁, ← ht₂, ← Scheme.Hom.comp_apply, ← Scheme.Hom.comp_apply, pullback.diagonal_fst,
      pullback.diagonal_snd]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ UniversallyInjective f ↔ Surjective (Y := pullback.diagonalObj f) (pullback.diagonal f)
have rw : diagonal (@Surjective) f ↔ Surjective (Y := pullback.diagonalObj f) (pullback.diagonal f)
Tactic: rw [universallyInjective_eq_diagonal]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen (goal)
Goal:
⊢ @UniversallyOpen = (topologically @IsOpenMap).universally
have h : ∀ (X Y : Scheme.{u_1}) (f : X ⟶ Y), UniversallyOpen f ↔ (topologically @IsOpenMap).universally f
Tactic: ext X Y f
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ UniversallyOpen f ↔ (topologically @IsOpenMap).universally f
have h : (topologically @IsOpenMap).universally f ↔ (topologically @IsOpenMap).universally f
Tactic: rw [universallyOpen_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
⊢ UniversallyOpen f
have rw : (topologically @IsOpenMap).universally f
Tactic: rw [eq]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
X' Y' : Scheme
i₁ : X' ⟶ X
i₂ : Y' ⟶ Y
f' : X' ⟶ Y'
hf : IsPullback f' i₁ i₂ f
⊢ topologically (@IsOpenMap) f'
have hf' : IsOpenImmersion f'
Tactic: have hf' : IsOpenImmersion f' := MorphismProperty.of_isPullback hf.flip inferInstance
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ IsStableUnderComposition @UniversallyOpen
have rw : (topologically @IsOpenMap).universally.IsStableUnderComposition
Tactic: rw [eq]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ IsZariskiLocalAtTarget @UniversallyOpen
have rw : IsZariskiLocalAtTarget.{u_1} (topologically @IsOpenMap).universally
Tactic: rw [eq]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ IsZariskiLocalAtTarget.{u_1} (topologically @IsOpenMap).universally
have hP₂ : ∀ {X Y : Scheme.{u_1}} (f : X ⟶ Y) {ι : Type u_1} (U : ι → Y.Opens),
  IsOpenCover U →
    (∀ (i : ι), topologically @IsOpenMap (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)) → topologically (@IsOpenMap) f
Tactic: apply universally_isZariskiLocalAtTarget
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen (hypothesis)
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
f : X ⟶ Y
ι : Type u_1
U : ι → Y.Opens
hU : IsOpenCover U
H : ∀ (i : ι), topologically @IsOpenMap (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)
⊢ topologically (@IsOpenMap) f
have H₁ : ∀ (i : ι), IsOpenMap (X := ↥(↑(f ⁻¹ᵁ U i) : Scheme)) ((U i).carrier.restrictPreimage ⇑f)
Tactic: simp_rw [topologically, morphismRestrict_base] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ IsZariskiLocalAtSource @UniversallyOpen
have rw : IsZariskiLocalAtSource.{u_1} (topologically @IsOpenMap).universally
Tactic: rw [eq]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFinitePresentation f
hf : GeneralizingMap (X := ↥X) (Y := ↥Y) ⇑f
⊢ topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap) f
have inr : ∀
  (this :
    ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [LocallyOfFinitePresentation f] (hf : GeneralizingMap (X := ↥X) (Y := ↥Y) ⇑f)
      (hY : ∃ (R : CommRingCat.{u}), Y = Spec R),
      topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap) f)
  (hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R),
  topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap) f
Tactic: wlog hY : ∃ R, Y = Spec R
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFinitePresentation f
hf : GeneralizingMap (X := ↥X) (Y := ↥Y) ⇑f
inr :
  ∀
    (this :
      ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [LocallyOfFinitePresentation f] (hf : GeneralizingMap (X := ↥X) (Y := ↥Y) ⇑f)
        (hY : ∃ (R : CommRingCat.{u}), Y = Spec R),
        topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap) f)
    (hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R),
    topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap) f
⊢ topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap) f
have wlog : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [LocallyOfFinitePresentation f] (hf : GeneralizingMap (X := ↥X) (Y := ↥Y) ⇑f)
  (hY : ∃ (R : CommRingCat.{u}), Y = Spec R),
  topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap) f
Tactic: wlog hY : ∃ R, Y = Spec R
Cleared hypotheses: inst, hf
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFinitePresentation f
hf : GeneralizingMap (X := ↥X) (Y := ↥Y) ⇑f
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [LocallyOfFinitePresentation f] (hf : GeneralizingMap (X := ↥X) (Y := ↥Y) ⇑f)
    (hY : ∃ (R : CommRingCat.{u}), Y = Spec R),
    topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap) f
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
⊢ topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap) f
have inr : ∀ (i : Y.affineCover.toPreZeroHypercover.1),
  topologically fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap (X :=
    (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
    (Scheme.Cover.pullbackHom (P := IsOpenImmersion) Y.affineCover f i :
      (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i ⟶ Y.affineCover.X i)
Tactic: rw [IsZariskiLocalAtTarget.iff_of_openCover (P := topologically IsOpenMap) Y.affineCover]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFinitePresentation f
hf : GeneralizingMap (X := ↥X) (Y := ↥Y) ⇑f
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [LocallyOfFinitePresentation f] (hf : GeneralizingMap (X := ↥X) (Y := ↥Y) ⇑f)
    (hY : ∃ (R : CommRingCat.{u}), Y = Spec R),
    topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap) f
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
i : Y.affineCover.toPreZeroHypercover.1
⊢ topologically fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap (X :=
    (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i) (pullback.snd f (Y.affineCover.f i))
have inr : GeneralizingMap (X := ↥((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)) (Y := ↥(Y.affineCover.X i))
  ⇑(pullback.snd f (Y.affineCover.f i))
Tactic: refine this _ ?_ ⟨_, rfl⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen (goal)
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFinitePresentation f
hf : GeneralizingMap (X := ↥X) (Y := ↥Y) ⇑f
hY : ∃ (R : CommRingCat.{u}), Y = Spec R
⊢ topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap) f
have obtain : ∀ (R : CommRingCat.{u}) (f : X ⟶ Spec R) [LocallyOfFinitePresentation f]
  (hf : GeneralizingMap (X := ↥X) (Y := ↥(Spec R)) ⇑f),
  topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap) f
Tactic: obtain ⟨R, rfl⟩ := hY
Cleared hypotheses: Y, f, inst, hf, hY
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen (goal)
Goal:
X_1 Y : Scheme
f_1 : X_1 ⟶ Y
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst : LocallyOfFinitePresentation f
hf : GeneralizingMap (X := ↥X) (Y := ↥(Spec R)) ⇑f
⊢ topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap) f
have inr : ∀
  (this :
    ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) {X : Scheme.{u}} (R : CommRingCat.{u}) (f : X ⟶ Spec R)
      [LocallyOfFinitePresentation f] (hf : GeneralizingMap (X := ↥X) (Y := ↥(Spec R)) ⇑f)
      (hX : ∃ (S : CommRingCat.{u}), X = Spec S),
      topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap) f)
  (hX : ¬∃ (S : CommRingCat.{u}), X = Spec S),
  topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap) f
Tactic: wlog hX : ∃ S, X = Spec S
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen (goal)
Goal:
X_1 Y : Scheme
f_1 : X_1 ⟶ Y
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst : LocallyOfFinitePresentation f
hf : GeneralizingMap (X := ↥X) (Y := ↥(Spec R)) ⇑f
inr :
  ∀
    (this :
      ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) {X : Scheme.{u}} (R : CommRingCat.{u}) (f : X ⟶ Spec R)
        [LocallyOfFinitePresentation f] (hf : GeneralizingMap (X := ↥X) (Y := ↥(Spec R)) ⇑f)
        (hX : ∃ (S : CommRingCat.{u}), X = Spec S),
        topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap) f)
    (hX : ¬∃ (S : CommRingCat.{u}), X = Spec S),
    topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap) f
⊢ topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap) f
have wlog : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) {X : Scheme.{u}} (R : CommRingCat.{u}) (f : X ⟶ Spec R) [LocallyOfFinitePresentation f]
  (hf : GeneralizingMap (X := ↥X) (Y := ↥(Spec R)) ⇑f) (hX : ∃ (S : CommRingCat.{u}), X = Spec S),
  topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap) f
Tactic: wlog hX : ∃ S, X = Spec S
Cleared hypotheses: X, R, f, inst, hf
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen (goal)
Goal:
X_1 Y : Scheme
f_1 : X_1 ⟶ Y
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst : LocallyOfFinitePresentation f
hf : GeneralizingMap (X := ↥X) (Y := ↥(Spec R)) ⇑f
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) {X : Scheme.{u}} (R : CommRingCat.{u}) (f : X ⟶ Spec R)
    [LocallyOfFinitePresentation f] (hf : GeneralizingMap (X := ↥X) (Y := ↥(Spec R)) ⇑f)
    (hX : ∃ (S : CommRingCat.{u}), X = Spec S),
    topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap) f
hX : ¬∃ (S : CommRingCat.{u}), X = Spec S
⊢ topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap) f
have inr : ∀ (i : X.affineCover.I₀),
  topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap) (X.affineCover.f i ≫ f)
Tactic: rw [IsZariskiLocalAtSource.iff_of_openCover (P := topologically IsOpenMap) X.affineCover]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen (goal)
Goal:
X_1 Y : Scheme
f_1 : X_1 ⟶ Y
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst : LocallyOfFinitePresentation f
hf : GeneralizingMap (X := ↥X) (Y := ↥(Spec R)) ⇑f
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) {X : Scheme.{u}} (R : CommRingCat.{u}) (f : X ⟶ Spec R)
    [LocallyOfFinitePresentation f] (hf : GeneralizingMap (X := ↥X) (Y := ↥(Spec R)) ⇑f)
    (hX : ∃ (S : CommRingCat.{u}), X = Spec S),
    topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap) f
hX : ¬∃ (S : CommRingCat.{u}), X = Spec S
i : X.affineCover.I₀
⊢ topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap) (X.affineCover.f i ≫ f)
have inr : GeneralizingMap (X := ↥(X.affineCover.X i)) (Y := ↥(Spec R)) ⇑(X.affineCover.f i ≫ f)
Tactic: refine this f _ _ ?_ ⟨_, rfl⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen (goal)
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X_2 Y : Scheme
f_2 : X_2 ⟶ Y
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst : LocallyOfFinitePresentation f
hf : GeneralizingMap (X := ↥X) (Y := ↥(Spec R)) ⇑f
hX : ∃ (S : CommRingCat.{u}), X = Spec S
⊢ topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap) f
have obtain : ∀ (S : CommRingCat.{u}) (f : Spec S ⟶ Spec R) [LocallyOfFinitePresentation f]
  (hf : GeneralizingMap (X := ↥(Spec S)) (Y := ↥(Spec R)) ⇑f),
  topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap) f
Tactic: obtain ⟨S, rfl⟩ := hX
Cleared hypotheses: X, f, inst, hf, hX
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen (goal)
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
f_2 : X ⟶ Y
R S : CommRingCat
f : Spec S ⟶ Spec R
inst : LocallyOfFinitePresentation f
hf : GeneralizingMap (X := ↥(Spec S)) (Y := ↥(Spec R)) ⇑f
⊢ topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap) f
have obtain : ∀ (φ : R ⟶ S) [LocallyOfFinitePresentation (Spec.map φ)]
  (hf : GeneralizingMap (X := ↥(Spec S)) (Y := ↥(Spec R)) ⇑(Spec.map φ)),
  topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap) (Spec.map φ)
Tactic: obtain ⟨φ, rfl⟩ := Spec.map_surjective f
Cleared hypotheses: f, inst, hf
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen (goal)
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
f : X ⟶ Y
R S : CommRingCat
φ : R ⟶ S
inst : LocallyOfFinitePresentation (Spec.map φ)
hf : GeneralizingMap (X := ↥(Spec S)) (Y := ↥(Spec R)) ⇑(Spec.map φ)
algInst : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom φ).toAlgebra
⊢ topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap) (Spec.map φ)
have convert_6 : Algebra.HasGoingDown.{u, u} (↑R : Type u) (↑S : Type u)
Tactic: convert! PrimeSpectrum.isOpenMap_comap_of_hasGoingDown_of_finitePresentation
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen (goal)
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
f : X ⟶ Y
R S : CommRingCat
φ : R ⟶ S
inst : LocallyOfFinitePresentation (Spec.map φ)
hf : GeneralizingMap (X := ↥(Spec S)) (Y := ↥(Spec R)) ⇑(Spec.map φ)
algInst : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom φ).toAlgebra
convert_6 : Algebra.HasGoingDown.{u, u} (↑R : Type u) (↑S : Type u)
⊢ topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap) (Spec.map φ)
have convert_7 : Algebra.FinitePresentation.{u, u} (↑R : Type u) (↑S : Type u)
Tactic: convert! PrimeSpectrum.isOpenMap_comap_of_hasGoingDown_of_finitePresentation
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen (goal)
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
f : X ⟶ Y
R S : CommRingCat
φ : R ⟶ S
inst : LocallyOfFinitePresentation (Spec.map φ)
hf : GeneralizingMap (X := ↥(Spec S)) (Y := ↥(Spec R)) ⇑(Spec.map φ)
algInst : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom φ).toAlgebra
⊢ Algebra.HasGoingDown.{u, u} (↑R : Type u) (↑S : Type u)
have convert_6 : GeneralizingMap.{u, u} (X := PrimeSpectrum (↑S : Type u)) (Y := PrimeSpectrum (↑R : Type u))
  (PrimeSpectrum.comap (algebraMap (↑R : Type u) (↑S : Type u)))
Tactic: rwa [Algebra.HasGoingDown.iff_generalizingMap_primeSpectrumComap]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
⊢ GeneralizingMap (X := ↥X) (Y := ↥Y) ⇑f
have this : HasRingHomProperty.{u} (topologically fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ GeneralizingMap)
  fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦
  topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ GeneralizingMap)
    (Spec.map (CommRingCat.ofHom f))
Tactic: have := HasRingHomProperty.of_isZariskiLocalAtSource_of_isZariskiLocalAtTarget.{u}
    (topologically GeneralizingMap)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
this :
  HasRingHomProperty.{u} (topologically fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ GeneralizingMap)
    fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦
    topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ GeneralizingMap)
      (Spec.map (CommRingCat.ofHom f))
⊢ topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ GeneralizingMap) f
have rw : ∀ (U : (↑Y.affineOpens : Type u)) (V : (↑X.affineOpens : Type u)) (e : (↑V : X.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens)),
  topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ GeneralizingMap)
    (Spec.map (CommRingCat.ofHom (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U : Y.Opens) (↑V : X.Opens) e))))
Tactic: rw [HasRingHomProperty.iff_appLE (P := topologically GeneralizingMap)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
this :
  HasRingHomProperty.{u} (topologically fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ GeneralizingMap)
    fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦
    topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ GeneralizingMap)
      (Spec.map (CommRingCat.ofHom f))
U : (↑Y.affineOpens : Type u)
V : (↑X.affineOpens : Type u)
e : (↑V : X.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens)
algInst : Algebra (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, (↑V : X.Opens)) : Type u) :=
  (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U : Y.Opens) (↑V : X.Opens) e)).toAlgebra
⊢ topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ GeneralizingMap)
    (Spec.map (CommRingCat.ofHom (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U : Y.Opens) (↑V : X.Opens) e))))
have apply : Algebra.HasGoingDown.{u, u} (↑(CommRingCat.of (↑Γ(Y, (↑U : Y.Opens)) : Type u)) : Type u)
  (↑(CommRingCat.of (↑Γ(X, (↑V : X.Opens)) : Type u)) : Type u)
Tactic: apply Algebra.HasGoingDown.iff_generalizingMap_primeSpectrumComap.mp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
this :
  HasRingHomProperty.{u} (topologically fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ GeneralizingMap)
    fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦
    topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ GeneralizingMap)
      (Spec.map (CommRingCat.ofHom f))
U : (↑Y.affineOpens : Type u)
V : (↑X.affineOpens : Type u)
e : (↑V : X.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens)
algInst : Algebra (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, (↑V : X.Opens)) : Type u) :=
  (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U : Y.Opens) (↑V : X.Opens) e)).toAlgebra
⊢ Algebra.HasGoingDown.{u, u} (↑(CommRingCat.of (↑Γ(Y, (↑U : Y.Opens)) : Type u)) : Type u)
    (↑(CommRingCat.of (↑Γ(X, (↑V : X.Opens)) : Type u)) : Type u)
have convert_6 : Module.Flat.{u, u} (↑(CommRingCat.of (↑Γ(Y, (↑U : Y.Opens)) : Type u)) : Type u)
  (↑(CommRingCat.of (↑Γ(X, (↑V : X.Opens)) : Type u)) : Type u)
Tactic: convert! Algebra.HasGoingDown.of_flat
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen (goal)
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
f : X ⟶ Y
inst : IsIntegral Y
inst_1 : Subsingleton.{u + 1} ↥Y
⊢ UniversallyOpen f
have inr : ∀ (this : ∀ {X : Scheme.{u}} (f : X ⟶ Y) (hX : ∃ (S : CommRingCat.{u}), X = Spec S), UniversallyOpen f)
  (hX : ¬∃ (S : CommRingCat.{u}), X = Spec S), UniversallyOpen f
Tactic: wlog hX : ∃ S, X = Spec S generalizing X