awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Integral (goal)
Goal:
Z S_1 : Scheme
R S : CommRingCat
f : Spec S ⟶ Spec R
⊢ IsIntegralHom f → topologically (@IsClosedMap) f
have obtain : ∀ (φ : R ⟶ S), IsIntegralHom (Spec.map φ) → topologically (@IsClosedMap) (Spec.map φ)
Tactic: obtain ⟨φ, rfl⟩ := Spec.map_surjective f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Integral (goal)
Goal:
Z S_1 : Scheme
R S : CommRingCat
φ : R ⟶ S
⊢ IsIntegralHom (Spec.map φ) → topologically (@IsClosedMap) (Spec.map φ)
have rw : (CommRingCat.Hom.hom φ).IsIntegral → topologically (@IsClosedMap) (Spec.map φ)
Tactic: rw [SpecMap_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Integral (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ IsIntegralHom f ↔ UniversallyClosed f ∧ IsAffineHom f
have refine : UniversallyClosed f ∧ IsAffineHom f → ∀ (H₁ : UniversallyClosed f) (H₂ : IsAffineHom f), IsIntegralHom f
Tactic: refine ⟨fun _ ↦ ⟨inferInstance, inferInstance⟩, fun ⟨H₁, H₂⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Integral (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
H₁ : UniversallyClosed f
H₂ : IsAffineHom f
⊢ IsIntegralHom f
have inr : ∀
  (this :
    ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} (H₁ : UniversallyClosed f) (H₂ : IsAffineHom f)
      (hY : ∃ (R : CommRingCat.{u}), Y = Spec R), IsIntegralHom f)
  (hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R), IsIntegralHom f
Tactic: wlog hY : ∃ R, Y = Spec R
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Integral (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
H₁ : UniversallyClosed f
H₂ : IsAffineHom f
inr :
  ∀
    (this :
      ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} (H₁ : UniversallyClosed f) (H₂ : IsAffineHom f)
        (hY : ∃ (R : CommRingCat.{u}), Y = Spec R), IsIntegralHom f)
    (hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R), IsIntegralHom f
⊢ IsIntegralHom f
have wlog : ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} (H₁ : UniversallyClosed f) (H₂ : IsAffineHom f)
  (hY : ∃ (R : CommRingCat.{u}), Y = Spec R), IsIntegralHom f
Tactic: wlog hY : ∃ R, Y = Spec R
Cleared hypotheses: X, Y, f, H₁, H₂
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Integral (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
H₁ : UniversallyClosed f
H₂ : IsAffineHom f
this :
  ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} (H₁ : UniversallyClosed f) (H₂ : IsAffineHom f)
    (hY : ∃ (R : CommRingCat.{u}), Y = Spec R), IsIntegralHom f
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
⊢ IsIntegralHom f
have inr : ∀ (i : Y.affineCover.toPreZeroHypercover.1),
  IsIntegralHom (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 := @IsIntegralHom) Y.affineCover]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Integral (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
H₁ : UniversallyClosed f
H₂ : IsAffineHom f
this :
  ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} (H₁ : UniversallyClosed f) (H₂ : IsAffineHom f)
    (hY : ∃ (R : CommRingCat.{u}), Y = Spec R), IsIntegralHom f
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
⊢ ∀ (i : Y.affineCover.toPreZeroHypercover.1),
    IsIntegralHom (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)
have H₃ : ∀ (i : Y.affineCover.toPreZeroHypercover.1),
  UniversallyClosed (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 := @UniversallyClosed) Y.affineCover] at H₁
Cleared hypotheses: H₁, H₂, this, hY
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Integral (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
H₁ :
  ∀ (i : Y.affineCover.toPreZeroHypercover.1),
    UniversallyClosed (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)
H₂ : IsAffineHom f
this :
  ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} (H₁ : UniversallyClosed f) (H₂ : IsAffineHom f)
    (hY : ∃ (R : CommRingCat.{u}), Y = Spec R), IsIntegralHom f
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
⊢ ∀ (i : Y.affineCover.toPreZeroHypercover.1),
    IsIntegralHom (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)
have H₃ : ∀ (i : Y.affineCover.toPreZeroHypercover.1),
  IsAffineHom (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 := @IsAffineHom) Y.affineCover] at H₂
Cleared hypotheses: H₂, this, hY
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Integral (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
H₁ : UniversallyClosed f
H₂ : IsAffineHom f
hY : ∃ (R : CommRingCat.{u}), Y = Spec R
⊢ IsIntegralHom f
have obtain : ∀ (R : CommRingCat.{u}) {f : X ⟶ Spec R} (H₁ : UniversallyClosed f) (H₂ : IsAffineHom f), IsIntegralHom f
Tactic: obtain ⟨R, rfl⟩ := hY
Cleared hypotheses: Y, f, H₁, H₂, hY
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Integral (goal)
Goal:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
H₁ : UniversallyClosed f
H₂ : IsAffineHom f
⊢ IsIntegralHom f
have inr : ∀
  (this :
    ∀ {X : Scheme.{u}} (R : CommRingCat.{u}) {f : X ⟶ Spec R} (H₁ : UniversallyClosed f) (H₂ : IsAffineHom f)
      (hX : ∃ (S : CommRingCat.{u}), X = Spec S), IsIntegralHom f)
  (hX : ¬∃ (S : CommRingCat.{u}), X = Spec S), IsIntegralHom f
Tactic: wlog hX : ∃ S, X = Spec S
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Integral (goal)
Goal:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
H₁ : UniversallyClosed f
H₂ : IsAffineHom f
inr :
  ∀
    (this :
      ∀ {X : Scheme.{u}} (R : CommRingCat.{u}) {f : X ⟶ Spec R} (H₁ : UniversallyClosed f) (H₂ : IsAffineHom f)
        (hX : ∃ (S : CommRingCat.{u}), X = Spec S), IsIntegralHom f)
    (hX : ¬∃ (S : CommRingCat.{u}), X = Spec S), IsIntegralHom f
⊢ IsIntegralHom f
have wlog : ∀ {X : Scheme.{u}} (R : CommRingCat.{u}) {f : X ⟶ Spec R} (H₁ : UniversallyClosed f) (H₂ : IsAffineHom f)
  (hX : ∃ (S : CommRingCat.{u}), X = Spec S), IsIntegralHom f
Tactic: wlog hX : ∃ S, X = Spec S
Cleared hypotheses: X, R, f, H₁, H₂
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Integral (hypothesis)
Goal:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
H₁ : UniversallyClosed f
H₂ : IsAffineHom f
this :
  ∀ {X : Scheme.{u}} (R : CommRingCat.{u}) {f : X ⟶ Spec R} (H₁ : UniversallyClosed f) (H₂ : IsAffineHom f)
    (hX : ∃ (S : CommRingCat.{u}), X = Spec S), IsIntegralHom f
hX : ¬∃ (S : CommRingCat.{u}), X = Spec S
⊢ IsIntegralHom f
have inst : IsAffine X
Tactic: have inst : IsAffine X := isAffine_of_isAffineHom f
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Integral (goal)
Goal:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
H₁ : UniversallyClosed f
H₂ : IsAffineHom f
this :
  ∀ {X : Scheme.{u}} (R : CommRingCat.{u}) {f : X ⟶ Spec R} (H₁ : UniversallyClosed f) (H₂ : IsAffineHom f)
    (hX : ∃ (S : CommRingCat.{u}), X = Spec S), IsIntegralHom f
hX : ¬∃ (S : CommRingCat.{u}), X = Spec S
inst : IsAffine X
⊢ IsIntegralHom f
have inr : IsIntegralHom (X.isoSpec.inv ≫ f)
Tactic: rw [← cancel_left_of_respectsIso (P := @IsIntegralHom) X.isoSpec.inv]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Integral (goal)
Goal:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
H₁ : UniversallyClosed f
H₂ : IsAffineHom f
hX : ∃ (S : CommRingCat.{u}), X = Spec S
⊢ IsIntegralHom f
have obtain : ∀ (S : CommRingCat.{u}) {f : Spec S ⟶ Spec R} (H₁ : UniversallyClosed f) (H₂ : IsAffineHom f), IsIntegralHom f
Tactic: obtain ⟨S, rfl⟩ := hX
Cleared hypotheses: X, f, H₁, H₂, hX
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Integral (goal)
Goal:
R S : CommRingCat
f : Spec S ⟶ Spec R
H₁ : UniversallyClosed f
H₂ : IsAffineHom f
⊢ IsIntegralHom f
have obtain : ∀ (φ : R ⟶ S) (H₁ : UniversallyClosed (Spec.map φ)) (H₂ : IsAffineHom (Spec.map φ)), IsIntegralHom (Spec.map φ)
Tactic: obtain ⟨φ, rfl⟩ : ∃ φ, Spec.map φ = f := ⟨_, Spec.map_preimage _⟩
Cleared hypotheses: f, H₁, H₂
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Integral (goal)
Goal:
R S : CommRingCat
φ : R ⟶ S
H₁ : UniversallyClosed (Spec.map φ)
H₂ : IsAffineHom (Spec.map φ)
⊢ IsIntegralHom (Spec.map φ)
have rw : (CommRingCat.Hom.hom φ).IsIntegral
Tactic: rw [SpecMap_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Integral (goal)
Goal:
R S : CommRingCat
φ : R ⟶ S
H₁ : UniversallyClosed (Spec.map φ)
H₂ : IsAffineHom (Spec.map φ)
⊢ (CommRingCat.Hom.hom φ).IsIntegral
have h : IsClosedMap (PrimeSpectrum.comap (Polynomial.mapRingHom (CommRingCat.Hom.hom φ)))
Tactic: apply PrimeSpectrum.isIntegral_of_isClosedMap_comap_mapRingHom
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Integral (goal)
Goal:
⊢ @IsIntegralHom = @UniversallyClosed ⊓ @IsAffineHom
have h : ∀ (x x_1 : Scheme.{u_1}) (x_2 : x ⟶ x_1), IsIntegralHom x_2 ↔ (@UniversallyClosed ⊓ @IsAffineHom) x_2
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.IsIso (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ IsIso f ↔ IsOpenImmersion f ∧ Surjective f
have rw : IsIso f ↔ IsOpenImmersion f ∧ Function.Surjective (α := ↥X) (β := ↥Y) ⇑f
Tactic: rw [surjective_iff, ← TopCat.epi_iff_surjective, isIso_iff_isOpenImmersion_and_epi_base]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.IsIso (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
rw : IsIso f ↔ IsOpenImmersion f ∧ Function.Surjective (α := ↥X) (β := ↥Y) ⇑f
⊢ IsIso f ↔ IsOpenImmersion f ∧ Surjective f
have rw₁ : IsIso f ↔ IsOpenImmersion f ∧ Epi f.base
Tactic: rw [surjective_iff, ← TopCat.epi_iff_surjective, isIso_iff_isOpenImmersion_and_epi_base]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.IsIso (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
rw : IsIso f ↔ IsOpenImmersion f ∧ Function.Surjective (α := ↥X) (β := ↥Y) ⇑f
rw₁ : IsIso f ↔ IsOpenImmersion f ∧ Epi f.base
⊢ IsIso f ↔ IsOpenImmersion f ∧ Surjective f
have rw₂ : IsOpenImmersion f ∧ Epi f.base ↔ IsOpenImmersion f ∧ Epi f.base
Tactic: rw [surjective_iff, ← TopCat.epi_iff_surjective, isIso_iff_isOpenImmersion_and_epi_base]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.IsIso (goal)
Goal:
⊢ isomorphisms Scheme = IsOpenImmersion ⊓ @Surjective
have h : ∀ ⦃X Y : Scheme.{u_1}⦄ (f : X ⟶ Y), isomorphisms Scheme f ↔ (IsOpenImmersion ⊓ @Surjective) f
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.IsIso (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ isomorphisms Scheme f ↔ (IsOpenImmersion ⊓ @Surjective) f
have h : IsOpenImmersion f ∧ Surjective f ↔ (IsOpenImmersion ⊓ @Surjective) f
Tactic: rw [isomorphisms.iff, isIso_iff_isOpenImmersion_and_surjective]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.IsIso (goal)
Goal:
⊢ isomorphisms Scheme =
    inverseImage (isomorphisms TopCat) Scheme.forgetToTop ⊓
      stalkwise fun {R S : Type u_1} [CommRing R] [CommRing S] (f : R →+* S) ↦
        Function.Bijective (α := R) (β := S) (⇑f : (a : R) → S)
have rw : (((topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] ↦ Topology.IsOpenEmbedding) ⊓
      topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] ↦ Function.Surjective) ⊓
    stalkwise fun {R S : Type u_1} [CommRing R] [CommRing S] (x : R →+* S) ↦
      Function.Bijective (α := R) (β := S) (⇑x : (a : R) → S)) =
  inverseImage (isomorphisms TopCat) Scheme.forgetToTop ⊓
    stalkwise fun {R S : Type u_1} [CommRing R] [CommRing S] (f : R →+* S) ↦
      Function.Bijective (α := R) (β := S) (⇑f : (a : R) → S)
Tactic: rw [isomorphisms_eq_isOpenImmersion_inf_surjective, isOpenImmersion_eq_inf,
    surjective_eq_topologically, inf_right_comm]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.IsIso (goal)
Goal:
⊢ (((topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] ↦ Topology.IsOpenEmbedding) ⊓
        topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] ↦ Function.Surjective) ⊓
      stalkwise fun {R S : Type u_1} [CommRing R] [CommRing S] (x : R →+* S) ↦
        Function.Bijective (α := R) (β := S) (⇑x : (a : R) → S)) =
    inverseImage (isomorphisms TopCat) Scheme.forgetToTop ⊓
      stalkwise fun {R S : Type u_1} [CommRing R] [CommRing S] (f : R →+* S) ↦
        Function.Bijective (α := R) (β := S) (⇑f : (a : R) → S)
have e_a : ((topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] ↦ Topology.IsOpenEmbedding) ⊓
    topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] ↦ Function.Surjective) =
  inverseImage (isomorphisms TopCat) Scheme.forgetToTop
Tactic: congr 1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.IsIso (goal)
Goal:
⊢ ((topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] ↦ Topology.IsOpenEmbedding) ⊓
      topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] ↦ Function.Surjective) =
    inverseImage (isomorphisms TopCat) Scheme.forgetToTop
have e_a : ∀ ⦃X Y : Scheme.{u_1}⦄ (f : X ⟶ Y),
  ((topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] ↦ Topology.IsOpenEmbedding) ⊓
        topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] ↦ Function.Surjective)
      f ↔
    inverseImage (isomorphisms TopCat) Scheme.forgetToTop f
Tactic: ext X Y f
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.IsIso (goal)
Goal:
⊢ HasAffineProperty.{u_1} (isomorphisms Scheme) fun (X x : Scheme.{u_1}) (f : X ⟶ x) (x_1 : IsAffine x) ↦
    IsAffine X ∧ IsIso (Scheme.Hom.appTop f)
have h : ∀ (X Y : Scheme.{u_1}) (f : X ⟶ Y) (hY : IsAffine Y),
  IsAffine X ∧ IsIso (Scheme.Hom.appTop f) ↔ AffineTargetMorphismProperty.of (isomorphisms Scheme) f
Tactic: convert! HasAffineProperty.of_isZariskiLocalAtTarget (isomorphisms Scheme) with X Y f hY
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.IsIso (goal)
Goal:
R S : CommRingCat
f : R ⟶ S
⊢ IsIso (Spec.map f) ↔
    Function.Bijective (α := (↑R : Type u)) (β := (↑S : Type u))
      (⇑(CommRingCat.Hom.hom f) : (a : (↑R : Type u)) → (↑S : Type u))
have rw : IsIso (Spec.map f) ↔ IsIso f
Tactic: rw [← ConcreteCategory.isIso_iff_bijective]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.IsIso (goal)
Goal:
R S : CommRingCat
f : R ⟶ S
⊢ IsIso (Spec.map f) ↔ IsIso f
have refine : ∀ (h : IsIso (Spec.map f)), IsIso f
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ inferInstance⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.IsIso (goal)
Goal:
R S : CommRingCat
f : R ⟶ S
h : IsIso (Spec.map f)
⊢ IsIso f
have rw : IsIso (Scheme.Hom.appTop (Spec.map f))
Tactic: rw [← isomorphisms.iff, (isomorphisms _).arrow_mk_iso_iff (arrowIsoΓSpecOfIsAffine f),
    isomorphisms.iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.LocalClosure (goal)
Goal:
P : MorphismProperty Scheme
X Y : Scheme
inst : P.RespectsIso
f : X ⟶ Y
⊢ sourceLocalClosure IsOpenImmersion P f ↔ ∀ (x : ↥X), ∃ (U : X.Opens), x ∈ U ∧ P (U.ι ≫ f)
have refine_1 : sourceLocalClosure IsOpenImmersion P f →
  ∀ (x : ↥X) (𝒰 : Scheme.Cover (Scheme.precoverage IsOpenImmersion) X) (hf : ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ f)),
    ∃ (U : X.Opens), x ∈ U ∧ P (U.ι ≫ f)
Tactic: refine ⟨fun ⟨𝒰, hf⟩ x ↦ ?_, fun H ↦ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.LocalClosure (goal)
Goal:
P : MorphismProperty Scheme
X Y : Scheme
inst : P.RespectsIso
f : X ⟶ Y
refine_1 :
  sourceLocalClosure IsOpenImmersion P f →
    ∀ (x : ↥X) (𝒰 : Scheme.Cover (Scheme.precoverage IsOpenImmersion) X) (hf : ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ f)),
      ∃ (U : X.Opens), x ∈ U ∧ P (U.ι ≫ f)
⊢ sourceLocalClosure IsOpenImmersion P f ↔ ∀ (x : ↥X), ∃ (U : X.Opens), x ∈ U ∧ P (U.ι ≫ f)
have refine_2 : ∀ (H : ∀ (x : ↥X), ∃ (U : X.Opens), x ∈ U ∧ P (U.ι ≫ f)), sourceLocalClosure IsOpenImmersion P f
Tactic: refine ⟨fun ⟨𝒰, hf⟩ x ↦ ?_, fun H ↦ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.LocalClosure (goal)
Goal:
P : MorphismProperty Scheme
X Y : Scheme
inst : P.RespectsIso
f : X ⟶ Y
h : sourceLocalClosure IsOpenImmersion P f
x : ↥X
𝒰 : Scheme.Cover (Scheme.precoverage IsOpenImmersion) X
hf : ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ f)
⊢ ∃ (U : X.Opens), x ∈ U ∧ P (U.ι ≫ f)
have refine_1 : P ((Scheme.Hom.opensRange (X := 𝒰.X (𝒰.idx x)) (𝒰.f (𝒰.idx x))).ι ≫ f)
Tactic: refine ⟨(𝒰.f (𝒰.idx x)).opensRange, 𝒰.covers x, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.LocalClosure (goal)
Goal:
P : MorphismProperty Scheme
X Y : Scheme
inst : P.RespectsIso
f : X ⟶ Y
h : sourceLocalClosure IsOpenImmersion P f
x : ↥X
𝒰 : Scheme.Cover (Scheme.precoverage IsOpenImmersion) X
hf : ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ f)
⊢ P ((Scheme.Hom.opensRange (X := 𝒰.X (𝒰.idx x)) (𝒰.f (𝒰.idx x))).ι ≫ f)
have refine_1 : P (X := 𝒰.X (𝒰.idx x)) (𝒰.f (𝒰.idx x) ≫ f)
Tactic: rw [← Scheme.Hom.isoOpensRange_inv_comp, Category.assoc, P.cancel_left_of_respectsIso]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.LocalClosure (goal)
Goal:
P : MorphismProperty Scheme
X Y : Scheme
inst : P.RespectsIso
f : X ⟶ Y
H : ∀ (x : ↥X), ∃ (U : X.Opens), x ∈ U ∧ P (U.ι ≫ f)
⊢ sourceLocalClosure IsOpenImmersion P f
have refine_2 : ∀ (U : (x : ↥X) → X.Opens) (hx : ∀ (x : ↥X), x ∈ U x) (hf : ∀ (x : ↥X), P ((U x).ι ≫ f)),
  sourceLocalClosure IsOpenImmersion P f
Tactic: choose U hx hf using H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.LocalClosure (goal)
Goal:
W P Q : MorphismProperty Scheme
X Y : Scheme
inst : W.IsStableUnderBaseChange
inst_1 : Scheme.IsJointlySurjectivePreserving W
inst_2 : P.RespectsLeft Q
inst_3 : Q.IsStableUnderBaseChange
⊢ (sourceLocalClosure W P).RespectsLeft Q
have refine : ∀ {X Y : Scheme.{u}} (Z : Scheme.{u}) (f : X ⟶ Y) (hf : Q f) (g : Y ⟶ Z),
  sourceLocalClosure W P g →
    ∀ (𝒰 : Scheme.Cover (Scheme.precoverage W) Y) (hg : ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ g))
      (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀), P ((Precoverage.ZeroHypercover.pullback₁ f 𝒰).f i ≫ f ≫ g)
Tactic: refine ⟨fun {X Y} Z f hf g ⟨𝒰, hg⟩ ↦ ⟨𝒰.pullback₁ f, fun i ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.LocalClosure (goal)
Goal:
W P Q : MorphismProperty Scheme
X Y : Scheme
inst : W.IsStableUnderBaseChange
inst_1 : Scheme.IsJointlySurjectivePreserving W
inst_2 : P.RespectsRight Q
⊢ (sourceLocalClosure W P).RespectsRight Q
have refine : ∀ {X Y : Scheme.{u}} (Z : Scheme.{u}) (f : Y ⟶ Z) (hf : Q f) (g : X ⟶ Y),
  sourceLocalClosure W P g →
    ∀ (𝒰 : Scheme.Cover (Scheme.precoverage W) X) (hg : ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ g)) (i : 𝒰.I₀), P (𝒰.f i ≫ g ≫ f)
Tactic: refine ⟨fun {X Y} Z f hf g ⟨𝒰, hg⟩ ↦ ⟨𝒰, fun i ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.LocalClosure (goal)
Goal:
W P Q : MorphismProperty Scheme
X_1 Y_1 : Scheme
inst : W.IsStableUnderBaseChange
inst_1 : Scheme.IsJointlySurjectivePreserving W
inst_2 : P.RespectsRight Q
X Y Z : Scheme
f : Y ⟶ Z
hf : Q f
g : X ⟶ Y
h : sourceLocalClosure W P g
𝒰 : Scheme.Cover (Scheme.precoverage W) X
hg : ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ g)
i : 𝒰.I₀
⊢ P (𝒰.f i ≫ g ≫ f)
have rw : P ((𝒰.f i ≫ g) ≫ f)
Tactic: rw [← Category.assoc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.LocalClosure (goal)
Goal:
W P Q : MorphismProperty Scheme
X Y : Scheme
inst : W.IsStableUnderBaseChange
inst_1 : Scheme.IsJointlySurjectivePreserving W
inst_2 : P.RespectsIso
inst_3 : P.RespectsLeft IsOpenImmersion
⊢ IsZariskiLocalAtSource.{u} (sourceLocalClosure IsOpenImmersion P)
have refine : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) (𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X),
  sourceLocalClosure IsOpenImmersion P f ↔ ∀ (i : 𝒰.I₀), sourceLocalClosure IsOpenImmersion P (𝒰.f i ≫ f)
Tactic: refine .mk_of_iff fun f 𝒰 ↦ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.LocalClosure (goal)
Goal:
W P Q : MorphismProperty Scheme
X Y : Scheme
inst : W.IsStableUnderBaseChange
inst_1 : Scheme.IsJointlySurjectivePreserving W
inst_2 : P.RespectsIso
inst_3 : P.RespectsLeft IsOpenImmersion
X_1 Y_1 : Scheme
f : X_1 ⟶ Y_1
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X_1
⊢ sourceLocalClosure IsOpenImmersion P f ↔ ∀ (i : 𝒰.I₀), sourceLocalClosure IsOpenImmersion P (𝒰.f i ≫ f)
have refine_1 : sourceLocalClosure IsOpenImmersion P f →
  ∀ (𝒱 : Scheme.Cover (Scheme.precoverage IsOpenImmersion) X_1) (h : ∀ (i : 𝒱.I₀), P (𝒱.f i ≫ f)) (i : 𝒰.I₀)
    (j : (Precoverage.ZeroHypercover.pullback₁ (𝒰.f i) 𝒱).I₀),
    P ((Precoverage.ZeroHypercover.pullback₁ (𝒰.f i) 𝒱).f j ≫ 𝒰.f i ≫ f)
Tactic: refine ⟨fun ⟨𝒱, h⟩ ↦ fun i ↦ ⟨𝒱.pullback₁ (𝒰.f i), fun j ↦ ?_⟩, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.LocalClosure (goal)
Goal:
W P Q : MorphismProperty Scheme
X Y : Scheme
inst : W.IsStableUnderBaseChange
inst_1 : Scheme.IsJointlySurjectivePreserving W
inst_2 : P.RespectsIso
inst_3 : P.RespectsLeft IsOpenImmersion
X_1 Y_1 : Scheme
f : X_1 ⟶ Y_1
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X_1
refine_1 :
  sourceLocalClosure IsOpenImmersion P f →
    ∀ (𝒱 : Scheme.Cover (Scheme.precoverage IsOpenImmersion) X_1) (h : ∀ (i : 𝒱.I₀), P (𝒱.f i ≫ f)) (i : 𝒰.I₀)
      (j : (Precoverage.ZeroHypercover.pullback₁ (𝒰.f i) 𝒱).I₀),
      P ((Precoverage.ZeroHypercover.pullback₁ (𝒰.f i) 𝒱).f j ≫ 𝒰.f i ≫ f)
⊢ sourceLocalClosure IsOpenImmersion P f ↔ ∀ (i : 𝒰.I₀), sourceLocalClosure IsOpenImmersion P (𝒰.f i ≫ f)
have refine_2 : ∀ (h : ∀ (i : 𝒰.I₀), sourceLocalClosure IsOpenImmersion P (𝒰.f i ≫ f)), sourceLocalClosure IsOpenImmersion P f
Tactic: refine ⟨fun ⟨𝒱, h⟩ ↦ fun i ↦ ⟨𝒱.pullback₁ (𝒰.f i), fun j ↦ ?_⟩, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.LocalClosure (goal)
Goal:
W P Q : MorphismProperty Scheme
X Y : Scheme
inst : W.IsStableUnderBaseChange
inst_1 : Scheme.IsJointlySurjectivePreserving W
inst_2 : P.RespectsIso
inst_3 : P.RespectsLeft IsOpenImmersion
X_1 Y_1 : Scheme
f : X_1 ⟶ Y_1
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X_1
h : ∀ (i : 𝒰.I₀), sourceLocalClosure IsOpenImmersion P (𝒰.f i ≫ f)
⊢ sourceLocalClosure IsOpenImmersion P f
have refine_2 : ∀ (𝒱 : (i : 𝒰.I₀) → Scheme.Cover (Scheme.precoverage IsOpenImmersion) (𝒰.X i))
  (h𝒱 : ∀ (i : 𝒰.I₀) (i_1 : (𝒱 i).I₀), P ((𝒱 i).f i_1 ≫ 𝒰.f i ≫ f)), sourceLocalClosure IsOpenImmersion P f
Tactic: choose 𝒱 h𝒱 using h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.LocalClosure (goal)
Goal:
W P Q : MorphismProperty Scheme
X Y : Scheme
inst : W.IsStableUnderBaseChange
inst_1 : Scheme.IsJointlySurjectivePreserving W
inst_2 : P.IsStableUnderBaseChange
⊢ (sourceLocalClosure W P).IsStableUnderBaseChange
have refine : ∀ (X Y S : Scheme.{u}) (f : X ⟶ S) (g : Y ⟶ S) (x : HasPullback f g),
  sourceLocalClosure W P g →
    ∀ (𝒰 : Scheme.Cover (Scheme.precoverage W) Y) (hg : ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ g))
      (i :
        PreZeroHypercover.I₀ (S := pullback f g)
          (Precoverage.ZeroHypercover.toPreZeroHypercover (Precoverage.ZeroHypercover.pullback₁ (pullback.snd f g) 𝒰))),
      P
        (PreZeroHypercover.f
            (Precoverage.ZeroHypercover.toPreZeroHypercover (Precoverage.ZeroHypercover.pullback₁ (pullback.snd f g) 𝒰))
            i ≫
          pullback.fst f g)
Tactic: refine .mk' fun X Y S f g _ ⟨𝒰, hg⟩ ↦ ⟨𝒰.pullback₁ (pullback.snd f g), fun i ↦ ?_⟩