awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Constructors (goal)
Goal:
P : MorphismProperty Scheme
hP₂ :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens),
    IsOpenCover U → (∀ (i : ι), P (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)) → P f
⊢ IsZariskiLocalAtTarget.{u} P.universally
have restrict : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) (U : Y.Opens), P.universally f → P.universally (f ∣_ U)
Tactic: apply IsZariskiLocalAtTarget.mk'
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Constructors (goal)
Goal:
P : MorphismProperty Scheme
hP₂ :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens),
    IsOpenCover U → (∀ (i : ι), P (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)) → P f
restrict : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) (U : Y.Opens), P.universally f → P.universally (f ∣_ U)
⊢ IsZariskiLocalAtTarget.{u} P.universally
have of_sSup_eq_top : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens),
  iSup U = ⊤ → (∀ (i : ι), P.universally (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)) → P.universally f
Tactic: apply IsZariskiLocalAtTarget.mk'
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Constructors (goal)
Goal:
P : MorphismProperty Scheme
hP₂ :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens),
    IsOpenCover U → (∀ (i : ι), P (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)) → P f
X Y : Scheme
f : X ⟶ Y
ι : Type u
U : ι → Y.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P.universally (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)
X' Y' : Scheme
i₁ : X' ⟶ X
i₂ : Y' ⟶ Y
f' : X' ⟶ Y'
h : IsPullback f' i₁ i₂ f
⊢ P f'
have of_sSup_eq_top : IsOpenCover (X := ↥Y') fun (i : ι) ↦ i₂ ⁻¹ᵁ U i
Tactic: apply hP₂ _ (fun i ↦ i₂ ⁻¹ᵁ U i)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Constructors (goal)
Goal:
P : MorphismProperty Scheme
hP₂ :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens),
    IsOpenCover U → (∀ (i : ι), P (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)) → P f
X Y : Scheme
f : X ⟶ Y
ι : Type u
U : ι → Y.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P.universally (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)
X' Y' : Scheme
i₁ : X' ⟶ X
i₂ : Y' ⟶ Y
f' : X' ⟶ Y'
h : IsPullback f' i₁ i₂ f
of_sSup_eq_top : IsOpenCover (X := ↥Y') fun (i : ι) ↦ i₂ ⁻¹ᵁ U i
⊢ P f'
have of_sSup_eq_top₁ : ∀ (i : ι), P (X := (↑(f' ⁻¹ᵁ i₂ ⁻¹ᵁ U i) : Scheme)) (f' ∣_ i₂ ⁻¹ᵁ U i)
Tactic: apply hP₂ _ (fun i ↦ i₂ ⁻¹ᵁ U i)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Constructors (goal)
Goal:
P : MorphismProperty Scheme
hP₂ :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens),
    IsOpenCover U → (∀ (i : ι), P (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)) → P f
X Y : Scheme
f : X ⟶ Y
ι : Type u
U : ι → Y.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P.universally (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)
X' Y' : Scheme
i₁ : X' ⟶ X
i₂ : Y' ⟶ Y
f' : X' ⟶ Y'
h : IsPullback f' i₁ i₂ f
⊢ IsOpenCover (X := ↥Y') fun (i : ι) ↦ i₂ ⁻¹ᵁ U i
have of_sSup_eq_top : ∀ (hU : ⊤ ≤ iSup U), LE.le.{u} (α := Opens ↥Y') ⊤ (⨆ (i : ι), i₂ ⁻¹ᵁ U i)
Tactic: simp only [IsOpenCover, ← top_le_iff] at hU ⊢
Cleared hypotheses: hU
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Constructors (goal)
Goal:
P : MorphismProperty Scheme
hP₂ :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens),
    IsOpenCover U → (∀ (i : ι), P (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)) → P f
X Y : Scheme
f : X ⟶ Y
ι : Type u
U : ι → Y.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P.universally (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)
X' Y' : Scheme
i₁ : X' ⟶ X
i₂ : Y' ⟶ Y
f' : X' ⟶ Y'
h : IsPullback f' i₁ i₂ f
i : ι
⊢ P (X := (↑(f' ⁻¹ᵁ i₂ ⁻¹ᵁ U i) : Scheme)) (f' ∣_ i₂ ⁻¹ᵁ U i)
have of_sSup_eq_top : f' ⁻¹ᵁ i₂ ⁻¹ᵁ U i = i₁ ⁻¹ᵁ f ⁻¹ᵁ U i
Tactic: refine H _ ((X'.isoOfEq ?_).hom ≫ i₁ ∣_ _) (i₂ ∣_ _) _ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Constructors (goal)
Goal:
P : MorphismProperty Scheme
hP₂ :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens),
    IsOpenCover U → (∀ (i : ι), P (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)) → P f
X Y : Scheme
f : X ⟶ Y
ι : Type u
U : ι → Y.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P.universally (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)
X' Y' : Scheme
i₁ : X' ⟶ X
i₂ : Y' ⟶ Y
f' : X' ⟶ Y'
h : IsPullback f' i₁ i₂ f
i : ι
of_sSup_eq_top : f' ⁻¹ᵁ i₂ ⁻¹ᵁ U i = i₁ ⁻¹ᵁ f ⁻¹ᵁ U i
⊢ P (X := (↑(f' ⁻¹ᵁ i₂ ⁻¹ᵁ U i) : Scheme)) (f' ∣_ i₂ ⁻¹ᵁ U i)
have of_sSup_eq_top₁ : IsPullback (P := (↑(f' ⁻¹ᵁ i₂ ⁻¹ᵁ U i) : Scheme)) (f' ∣_ i₂ ⁻¹ᵁ U i) (Iso.hom (X'.isoOfEq sorry) ≫ i₁ ∣_ f ⁻¹ᵁ U i)
  (i₂ ∣_ U i) (f ∣_ U i)
Tactic: refine H _ ((X'.isoOfEq ?_).hom ≫ i₁ ∣_ _) (i₂ ∣_ _) _ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Constructors (goal)
Goal:
P : MorphismProperty Scheme
hP₂ :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens),
    IsOpenCover U → (∀ (i : ι), P (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)) → P f
X Y : Scheme
f : X ⟶ Y
ι : Type u
U : ι → Y.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P.universally (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)
X' Y' : Scheme
i₁ : X' ⟶ X
i₂ : Y' ⟶ Y
f' : X' ⟶ Y'
h : IsPullback f' i₁ i₂ f
i : ι
⊢ IsPullback (P := (↑(f' ⁻¹ᵁ i₂ ⁻¹ᵁ U i) : Scheme)) (f' ∣_ i₂ ⁻¹ᵁ U i) (Iso.hom (X'.isoOfEq ⋯) ≫ i₁ ∣_ f ⁻¹ᵁ U i)
    (i₂ ∣_ U i) (f ∣_ U i)
have of_sSup_eq_top : IsPullback (f' ∣_ i₂ ⁻¹ᵁ U i) ((Iso.hom (X'.isoOfEq sorry) ≫ i₁ ∣_ f ⁻¹ᵁ U i) ≫ (f ⁻¹ᵁ U i).ι) (i₂ ∣_ U i ≫ (U i).ι) f
Tactic: rw [← (isPullback_morphismRestrict f _).paste_vert_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Constructors (goal)
Goal:
P : MorphismProperty Scheme
hP₂ :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens),
    IsOpenCover U → (∀ (i : ι), P (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)) → P f
X Y : Scheme
f : X ⟶ Y
ι : Type u
U : ι → Y.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P.universally (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)
X' Y' : Scheme
i₁ : X' ⟶ X
i₂ : Y' ⟶ Y
f' : X' ⟶ Y'
h : IsPullback f' i₁ i₂ f
i : ι
of_sSup_eq_top :
  IsPullback (f' ∣_ i₂ ⁻¹ᵁ U i) ((Iso.hom (X'.isoOfEq ⋯) ≫ i₁ ∣_ f ⁻¹ᵁ U i) ≫ (f ⁻¹ᵁ U i).ι) (i₂ ∣_ U i ≫ (U i).ι) f
⊢ IsPullback (P := (↑(f' ⁻¹ᵁ i₂ ⁻¹ᵁ U i) : Scheme)) (f' ∣_ i₂ ⁻¹ᵁ U i) (Iso.hom (X'.isoOfEq ⋯) ≫ i₁ ∣_ f ⁻¹ᵁ U i)
    (i₂ ∣_ U i) (f ∣_ U i)
have of_sSup_eq_top₁ : Eq (α := (↑(f' ⁻¹ᵁ i₂ ⁻¹ᵁ U i) : Scheme) ⟶ (↑(U i) : Scheme)) (f' ∣_ i₂ ⁻¹ᵁ U i ≫ i₂ ∣_ U i)
  ((Iso.hom (X'.isoOfEq sorry) ≫ i₁ ∣_ f ⁻¹ᵁ U i) ≫ f ∣_ U i)
Tactic: rw [← (isPullback_morphismRestrict f _).paste_vert_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Constructors (goal)
Goal:
P : MorphismProperty Scheme
hP₂ :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens),
    IsOpenCover U → (∀ (i : ι), P (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)) → P f
X Y : Scheme
f : X ⟶ Y
ι : Type u
U : ι → Y.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P.universally (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)
X' Y' : Scheme
i₁ : X' ⟶ X
i₂ : Y' ⟶ Y
f' : X' ⟶ Y'
h : IsPullback f' i₁ i₂ f
i : ι
⊢ IsPullback (f' ∣_ i₂ ⁻¹ᵁ U i) ((Iso.hom (X'.isoOfEq ⋯) ≫ i₁ ∣_ f ⁻¹ᵁ U i) ≫ (f ⁻¹ᵁ U i).ι) (i₂ ∣_ U i ≫ (U i).ι) f
have of_sSup_eq_top : IsPullback (f' ∣_ i₂ ⁻¹ᵁ U i) ((f' ⁻¹ᵁ i₂ ⁻¹ᵁ U i).ι ≫ i₁) ((i₂ ⁻¹ᵁ U i).ι ≫ i₂) f
Tactic: simp only [Category.assoc, morphismRestrict_ι, Scheme.isoOfEq_hom_ι_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Constructors (goal)
Goal:
P : MorphismProperty Scheme
hP₂ :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens),
    IsOpenCover U → (∀ (i : ι), P (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)) → P f
X Y : Scheme
f : X ⟶ Y
ι : Type u
U : ι → Y.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P.universally (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)
X' Y' : Scheme
i₁ : X' ⟶ X
i₂ : Y' ⟶ Y
f' : X' ⟶ Y'
h : IsPullback f' i₁ i₂ f
i : ι
⊢ Eq (α := (↑(f' ⁻¹ᵁ i₂ ⁻¹ᵁ U i) : Scheme) ⟶ (↑(U i) : Scheme)) (f' ∣_ i₂ ⁻¹ᵁ U i ≫ i₂ ∣_ U i)
    ((Iso.hom (X'.isoOfEq ⋯) ≫ i₁ ∣_ f ⁻¹ᵁ U i) ≫ f ∣_ U i)
have of_sSup_eq_top : (f' ∣_ i₂ ⁻¹ᵁ U i ≫ i₂ ∣_ U i) ≫ (U i).ι = ((Iso.hom (X'.isoOfEq sorry) ≫ i₁ ∣_ f ⁻¹ᵁ U i) ≫ f ∣_ U i) ≫ (U i).ι
Tactic: rw [← cancel_mono (Scheme.Opens.ι _)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Constructors (goal)
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
⊢ IsZariskiLocalAtSource.{u_1} P.universally
have refine : ∀ {X Y : Scheme.{u_1}} (f : X ⟶ Y) (𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X),
  P.universally f ↔ ∀ (i : 𝒰.I₀), P.universally (𝒰.f i ≫ f)
Tactic: refine .mk_of_iff ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Constructors (goal)
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X
⊢ P.universally f ↔ ∀ (i : 𝒰.I₀), P.universally (𝒰.f i ≫ f)
have refine_1 : ∀ (hf : P.universally f) (i : 𝒰.I₀), P.universally (𝒰.f i ≫ f)
Tactic: refine ⟨fun hf i ↦ ?_, fun hf ↦ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Constructors (goal)
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X
refine_1 : ∀ (hf : P.universally f) (i : 𝒰.I₀), P.universally (𝒰.f i ≫ f)
⊢ P.universally f ↔ ∀ (i : 𝒰.I₀), P.universally (𝒰.f i ≫ f)
have refine_2 : ∀ (hf : ∀ (i : 𝒰.I₀), P.universally (𝒰.f i ≫ f)), P.universally f
Tactic: refine ⟨fun hf i ↦ ?_, fun hf ↦ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Constructors (goal)
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X
hf : P.universally f
i : 𝒰.I₀
⊢ P.universally (𝒰.f i ≫ f)
have refine_1 : ∀ {T : Scheme.{u_1}} (f_1 : T ⟶ Y) [inst : HasPullback f_1 (𝒰.f i ≫ f)],
  P (X := pullback f_1 (𝒰.f i ≫ f)) (pullback.fst f_1 (𝒰.f i ≫ f))
Tactic: apply MorphismProperty.universally_mk'
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Constructors (goal)
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X
hf : P.universally f
i : 𝒰.I₀
T : Scheme
g : T ⟶ Y
inst_1 : HasPullback g (𝒰.f i ≫ f)
⊢ P (X := pullback g (𝒰.f i ≫ f)) (pullback.fst g (𝒰.f i ≫ f))
have refine_1 : P (X := pullback (X := pullback g f) (pullback.snd g f) (𝒰.f i))
  (pullback.fst (pullback.snd g f) (𝒰.f i) ≫ pullback.fst g f)
Tactic: rw [← P.cancel_left_of_respectsIso (pullbackLeftPullbackSndIso g f _).hom,
      pullbackLeftPullbackSndIso_hom_fst]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Constructors (goal)
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X
hf : ∀ (i : 𝒰.I₀), P.universally (𝒰.f i ≫ f)
⊢ P.universally f
have refine_2 : ∀ {T : Scheme.{u_1}} (f_1 : T ⟶ Y) [inst : HasPullback f_1 f], P (X := pullback f_1 f) (pullback.fst f_1 f)
Tactic: apply MorphismProperty.universally_mk'
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Constructors (goal)
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X
hf : ∀ (i : 𝒰.I₀), P.universally (𝒰.f i ≫ f)
T : Scheme
g : T ⟶ Y
inst_1 : HasPullback g f
⊢ P (X := pullback g f) (pullback.fst g f)
have refine_2 : ∀
  (i :
    PreZeroHypercover.I₀ (S := pullback g f)
      (Precoverage.ZeroHypercover.toPreZeroHypercover (Precoverage.ZeroHypercover.pullback₁ (pullback.snd g f) 𝒰))),
  P
    (PreZeroHypercover.f
        (Precoverage.ZeroHypercover.toPreZeroHypercover (Precoverage.ZeroHypercover.pullback₁ (pullback.snd g f) 𝒰)) i ≫
      pullback.fst g f)
Tactic: rw [IsZariskiLocalAtSource.iff_of_openCover (P := P) (𝒰.pullback₁ <| pullback.snd g f)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Constructors (goal)
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X
hf : ∀ (i : 𝒰.I₀), P.universally (𝒰.f i ≫ f)
T : Scheme
g : T ⟶ Y
inst_1 : HasPullback g f
i :
  PreZeroHypercover.I₀ (S := pullback g f)
    (Precoverage.ZeroHypercover.toPreZeroHypercover (Precoverage.ZeroHypercover.pullback₁ (pullback.snd g f) 𝒰))
⊢ P
    (PreZeroHypercover.f
        (Precoverage.ZeroHypercover.toPreZeroHypercover (Precoverage.ZeroHypercover.pullback₁ (pullback.snd g f) 𝒰)) i ≫
      pullback.fst g f)
have refine_2 : P (X := pullback (X := pullback g f) (pullback.snd g f) (𝒰.f i))
  (pullback.fst (pullback.snd g f) (𝒰.f i) ≫ pullback.fst g f)
Tactic: dsimp only [Precoverage.ZeroHypercover.pullback₁_toPreZeroHypercover,
      PreZeroHypercover.pullback₁_X, PreZeroHypercover.pullback₁_f]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Constructors (goal)
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X
hf : ∀ (i : 𝒰.I₀), P.universally (𝒰.f i ≫ f)
T : Scheme
g : T ⟶ Y
inst_1 : HasPullback g f
i :
  PreZeroHypercover.I₀ (S := pullback g f)
    (Precoverage.ZeroHypercover.toPreZeroHypercover (Precoverage.ZeroHypercover.pullback₁ (pullback.snd g f) 𝒰))
⊢ P (X := pullback (X := pullback g f) (pullback.snd g f) (𝒰.f i))
    (pullback.fst (pullback.snd g f) (𝒰.f i) ≫ pullback.fst g f)
have refine_2 : P (X := pullback g (𝒰.f i ≫ f)) (pullback.fst g (𝒰.f i ≫ f))
Tactic: rw [← pullbackLeftPullbackSndIso_hom_fst, P.cancel_left_of_respectsIso]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Constructors (goal)
Goal:
P : {α β : Type u} → [TopologicalSpace α] → [TopologicalSpace β] → (α → β) → Prop
hP :
  ∀ {α β γ : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : TopologicalSpace γ] (f : α → β)
    (g : β → γ), P f → P g → P (g ∘ f)
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ P) f
hg : topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ P) g
⊢ topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ P) (f ≫ g)
have simp : P (α := ↥X) (β := ↥Z) (Function.comp (β := ↥Y) ⇑g ⇑f)
Tactic: simp only [topologically, Scheme.Hom.comp_base, TopCat.coe_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Constructors (goal)
Goal:
P : {α β : Type u} → [TopologicalSpace α] → [TopologicalSpace β] → (α → β) → Prop
hP :
  ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α ≃ₜ β),
    P (α := α) (β := β) (⇑f : (a : α) → β)
X Y : Scheme
e : X ⟶ Y
⊢ MorphismProperty.isomorphisms Scheme e →
    topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ P) e
have IsIso : ∀ (he : IsIso e), topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ P) e
Tactic: (he : IsIso e)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Constructors (goal)
Goal:
P : {α β : Type u} → [TopologicalSpace α] → [TopologicalSpace β] → (α → β) → Prop
inst : (topologically fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ P).RespectsIso
hP₂ :
  ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) (s : Set β),
    Continuous f → IsOpen s → P f → P (s.restrictPreimage f)
hP₃ :
  ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) {ι : Type u} (U : ι → Opens β),
    IsOpenCover U → Continuous f → (∀ (i : ι), P ((U i).carrier.restrictPreimage f)) → P f
⊢ IsZariskiLocalAtTarget.{u} (topologically fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ P)
have restrict : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) (U : Y.Opens),
  topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ P) f →
    topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ P) (f ∣_ U)
Tactic: apply IsZariskiLocalAtTarget.mk'
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Constructors (goal)
Goal:
P : {α β : Type u} → [TopologicalSpace α] → [TopologicalSpace β] → (α → β) → Prop
inst : (topologically fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ P).RespectsIso
hP₂ :
  ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) (s : Set β),
    Continuous f → IsOpen s → P f → P (s.restrictPreimage f)
hP₃ :
  ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) {ι : Type u} (U : ι → Opens β),
    IsOpenCover U → Continuous f → (∀ (i : ι), P ((U i).carrier.restrictPreimage f)) → P f
restrict :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) (U : Y.Opens),
    topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ P) f →
      topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ P) (f ∣_ U)
⊢ IsZariskiLocalAtTarget.{u} (topologically fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ P)
have of_sSup_eq_top : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens),
  iSup U = ⊤ →
    (∀ (i : ι),
        topologically fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ P (X := (↑(f ⁻¹ᵁ U i) : Scheme))
          (f ∣_ U i)) →
      topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ P) f
Tactic: apply IsZariskiLocalAtTarget.mk'
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Constructors (goal)
Goal:
P : {α β : Type u} → [TopologicalSpace α] → [TopologicalSpace β] → (α → β) → Prop
inst : (topologically fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ P).RespectsIso
hP₂ :
  ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) (s : Set β),
    Continuous f → IsOpen s → P f → P (s.restrictPreimage f)
hP₃ :
  ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) {ι : Type u} (U : ι → Opens β),
    IsOpenCover U → Continuous f → (∀ (i : ι), P ((U i).carrier.restrictPreimage f)) → P f
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hf : topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ P) f
⊢ topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ P) (f ∣_ U)
have restrict : P (α := ↥(↑(f ⁻¹ᵁ U) : Scheme)) (U.carrier.restrictPreimage ⇑f)
Tactic: simp_rw [topologically, morphismRestrict_base]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Constructors (goal)
Goal:
P : {α β : Type u} → [TopologicalSpace α] → [TopologicalSpace β] → (α → β) → Prop
inst : (topologically fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ P).RespectsIso
hP₂ :
  ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) (s : Set β),
    Continuous f → IsOpen s → P f → P (s.restrictPreimage f)
hP₃ :
  ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) {ι : Type u} (U : ι → Opens β),
    IsOpenCover U → Continuous f → (∀ (i : ι), P ((U i).carrier.restrictPreimage f)) → P f
X Y : Scheme
f : X ⟶ Y
ι : Type u
U : ι → Y.Opens
hU : iSup U = ⊤
hf :
  ∀ (i : ι),
    topologically fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ P (X := (↑(f ⁻¹ᵁ U i) : Scheme))
      (f ∣_ U i)
⊢ topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ P) f
have apply : ∀ (i : ι), P (α := (↑(⇑f ⁻¹' (U i).carrier) : Type u)) ((U i).carrier.restrictPreimage ⇑f)
Tactic: apply hP₃ f U hU f.continuous fun i ↦ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Constructors (goal)
Goal:
P : {α β : Type u} → [TopologicalSpace α] → [TopologicalSpace β] → (α → β) → Prop
inst : (topologically fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ P).RespectsIso
hP₂ :
  ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) (s : Set β),
    Continuous f → IsOpen s → P f → P (s.restrictPreimage f)
hP₃ :
  ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) {ι : Type u} (U : ι → Opens β),
    IsOpenCover U → Continuous f → (∀ (i : ι), P ((U i).carrier.restrictPreimage f)) → P f
X Y : Scheme
f : X ⟶ Y
ι : Type u
U : ι → Y.Opens
hU : iSup U = ⊤
hf :
  ∀ (i : ι),
    topologically fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ P (X := (↑(f ⁻¹ᵁ U i) : Scheme))
      (f ∣_ U i)
i : ι
⊢ P (α := (↑(⇑f ⁻¹' (U i).carrier) : Type u)) ((U i).carrier.restrictPreimage ⇑f)
have rw : P (α := (↑(⇑f ⁻¹' (U i).carrier) : Type u)) (β := (↑(U i).carrier : Type u)) ⇑(f ∣_ U i)
Tactic: rw [← morphismRestrict_base]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Constructors (goal)
Goal:
P : {α β : Type u} → [TopologicalSpace α] → [TopologicalSpace β] → (α → β) → Prop
inst : (topologically fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ P).RespectsIso
hP :
  ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) {ι : Type u} (U : ι → Opens β),
    IsOpenCover U → Continuous f → (P f ↔ ∀ (i : ι), P ((U i).carrier.restrictPreimage f))
⊢ IsZariskiLocalAtTarget.{u} (topologically fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ P)
have refine : ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) (s : Set β),
  Continuous f →
    IsOpen s →
      (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ (P : (α → β) → Prop)) f →
        (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ (P : (α → β) → Prop)) (s.restrictPreimage f)
Tactic: refine topologically_isZariskiLocalAtTarget P ?_ (fun f _ U hU hU' ↦ (hP f U hU hU').mpr)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Constructors (goal)
Goal:
P : {α β : Type u} → [TopologicalSpace α] → [TopologicalSpace β] → (α → β) → Prop
inst : (topologically fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ P).RespectsIso
hP :
  ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_3 : TopologicalSpace β] (f : α → β) {ι : Type u} (U : ι → Opens β),
    IsOpenCover U → Continuous f → (P f ↔ ∀ (i : ι), P ((U i).carrier.restrictPreimage f))
α β : Type u
inst_1 : TopologicalSpace α
inst_2 : TopologicalSpace β
f : α → β
s : Set β
hf : Continuous f
hs : IsOpen s
H : P f
⊢ P (s.restrictPreimage f)
have refine : IsOpenCover (ι := ULift.{u, 0} (Fin (Nat.succ 0).succ))
  (![⊤, { carrier := s, is_open' := hs : Opens β }] ∘
    (⇑Equiv.ulift : (a : ULift.{u, 0} (Fin (Nat.succ 0).succ)) → Fin (Nat.succ 0).succ))
Tactic: refine (hP f (![⊤, Opens.mk s hs] ∘ Equiv.ulift) ?_ hf).mp H ⟨1⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Constructors (goal)
Goal:
P : {α β : Type u} → [TopologicalSpace α] → [TopologicalSpace β] → (α → β) → Prop
inst : (topologically fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ P).RespectsIso
hP :
  ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_3 : TopologicalSpace β] (f : α → β) {ι : Type u} (U : ι → Opens β),
    IsOpenCover U → Continuous f → (P f ↔ ∀ (i : ι), P ((U i).carrier.restrictPreimage f))
α β : Type u
inst_1 : TopologicalSpace α
inst_2 : TopologicalSpace β
f : α → β
s : Set β
hf : Continuous f
hs : IsOpen s
H : P f
⊢ IsOpenCover (ι := ULift.{u, 0} (Fin (Nat.succ 0).succ))
    (![⊤, { carrier := s, is_open' := hs : Opens β }] ∘
      (⇑Equiv.ulift : (a : ULift.{u, 0} (Fin (Nat.succ 0).succ)) → Fin (Nat.succ 0).succ))
have rw : ⊤ ≤
  iSup (ι := ULift.{u, 0} (Fin (Nat.succ 0).succ))
    (![⊤, { carrier := s, is_open' := hs : Opens β }] ∘
      (⇑Equiv.ulift : (a : ULift.{u, 0} (Fin (Nat.succ 0).succ)) → Fin (Nat.succ 0).succ))
Tactic: rw [IsOpenCover, ← top_le_iff]