awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
X Y X' Y' : Scheme
f : X ⟶ X'
g : Y ⟶ Y'
hf : P f
hg : P g
⊢ P (X :=
    PreZeroHypercover.X (S := X ⨿ Y)
      (Precoverage.ZeroHypercover.toPreZeroHypercover
        (Precoverage.ZeroHypercover.pullback₁ (coprod.map f g) (coprodOpenCover X' Y')))
      (Sum.inr PUnit.unit))
    (Scheme.Cover.pullbackHom (P := IsOpenImmersion) (coprodOpenCover X' Y') (coprod.map f g) (Sum.inr PUnit.unit) :
      PreZeroHypercover.X (S := X ⨿ Y)
          (Precoverage.ZeroHypercover.toPreZeroHypercover
            (Precoverage.ZeroHypercover.pullback₁ (coprod.map f g) (coprodOpenCover X' Y')))
          (Sum.inr PUnit.unit) ⟶
        (coprodOpenCover X' Y').X (Sum.inr PUnit.unit))
have inr : P (Y := (coprodOpenCover X' Y').X (Sum.inr PUnit.unit))
  (CategoryStruct.comp (Y := pullback (X := X ⨿ Y) (Z := X' ⨿ Y') (coprod.map f g) coprod.inr) (Iso.hom sorry.isoPullback)
    (Scheme.Cover.pullbackHom (P := IsOpenImmersion) (coprodOpenCover X' Y') (coprod.map f g) (Sum.inr PUnit.unit)))
Tactic: rw [← MorphismProperty.cancel_left_of_respectsIso P
      (isPullback_inr_inr_coprodMap f g).flip.isoPullback.hom]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
X Y X' Y' : Scheme
f : X ⟶ X'
g : Y ⟶ Y'
hf : P f
hg : P g
⊢ P (Y := (coprodOpenCover X' Y').X (Sum.inr PUnit.unit))
    (CategoryStruct.comp (Y := pullback (X := X ⨿ Y) (Z := X' ⨿ Y') (coprod.map f g) coprod.inr) (Iso.hom ⋯.isoPullback)
      (Scheme.Cover.pullbackHom (P := IsOpenImmersion) (coprodOpenCover X' Y') (coprod.map f g) (Sum.inr PUnit.unit)))
have h : (coprodOpenCover X' Y').X (Sum.inr PUnit.unit) = Y' →
  CategoryStruct.comp (Y := pullback (X := X ⨿ Y) (Z := X' ⨿ Y') (coprod.map f g) coprod.inr) (Iso.hom sorry.isoPullback)
      (Scheme.Cover.pullbackHom (P := IsOpenImmersion) (coprodOpenCover X' Y') (coprod.map f g) (Sum.inr PUnit.unit)) =
    g
Tactic: convert! hg
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
Goal:
P : MorphismProperty Scheme
inst : P.RespectsIso
restrict : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) (U : X.Opens), P f → P (U.ι ≫ f)
of_sSup_eq_top :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) {ι : Type u} (U : ι → X.Opens), iSup U = ⊤ → (∀ (i : ι), P ((U i).ι ≫ f)) → P f
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X
i : 𝒰.I₀
H : P f
⊢ P (𝒰.f i ≫ f)
have rw : P ((Scheme.Hom.opensRange (𝒰.f i)).ι ≫ f)
Tactic: rw [← IsOpenImmersion.isoOfRangeEq_hom_fac (𝒰.f i) (Scheme.Opens.ι _)
      (congr_arg Opens.carrier (𝒰.f i).opensRange.opensRange_ι.symm), Category.assoc,
      P.cancel_left_of_respectsIso]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
Goal:
P : MorphismProperty Scheme
inst : P.RespectsIso
restrict : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) (U : X.Opens), P f → P (U.ι ≫ f)
of_sSup_eq_top :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) {ι : Type u} (U : ι → X.Opens), iSup U = ⊤ → (∀ (i : ι), P ((U i).ι ≫ f)) → P f
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X
h : ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ f)
⊢ P f
have refine : ∀ (i : 𝒰.I₀), P ((Scheme.Hom.opensRange (𝒰.f i)).ι ≫ f)
Tactic: refine of_sSup_eq_top f _ (Scheme.OpenCover.iSup_opensRange 𝒰) fun i ↦ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
Goal:
P : MorphismProperty Scheme
inst : P.RespectsIso
restrict : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) (U : X.Opens), P f → P (U.ι ≫ f)
of_sSup_eq_top :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) {ι : Type u} (U : ι → X.Opens), iSup U = ⊤ → (∀ (i : ι), P ((U i).ι ≫ f)) → P f
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X
h : ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ f)
i : 𝒰.I₀
⊢ P ((Scheme.Hom.opensRange (𝒰.f i)).ι ≫ f)
have rw : P (𝒰.f i ≫ f)
Tactic: rw [← IsOpenImmersion.isoOfRangeEq_inv_fac (𝒰.f i) (Scheme.Opens.ι _)
      (congr_arg Opens.carrier (𝒰.f i).opensRange.opensRange_ι.symm), Category.assoc,
      P.cancel_left_of_respectsIso]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U : ι → X.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P ((U i).ι ≫ f)
⊢ IsOpenCover.{u, u} (ι := (↑(Set.range U) : Type u)) (Subtype.val (p := fun (x : X.Opens) ↦ x ∈ Set.range U))
have h : ∀ (x : ↥X),
  x ∈ (↑(iSup (ι := (↑(Set.range U) : Type u)) (Subtype.val (p := fun (x : X.Opens) ↦ x ∈ Set.range U))) : Set ↥X) ↔
    x ∈ (↑⊤ : Set ↥X)
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U : ι → X.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P ((U i).ι ≫ f)
⊢ P f
have refine : ∀
  (i :
    (X.openCoverOfIsOpenCover (s := (↑(Set.range U) : Type u)) (Subtype.val (p := fun (x : X.Opens) ↦ x ∈ Set.range U))
        sorry).I₀),
  P
    ((X.openCoverOfIsOpenCover (s := (↑(Set.range U) : Type u)) (Subtype.val (p := fun (x : X.Opens) ↦ x ∈ Set.range U))
            sorry).f
        i ≫
      f)
Tactic: refine (P.iff_of_zeroHypercover_source
    (X.openCoverOfIsOpenCover (s := Set.range U) Subtype.val (by ext; simp [← hU]))).mpr fun i ↦ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U : ι → X.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P ((U i).ι ≫ f)
i :
  (X.openCoverOfIsOpenCover (s := (↑(Set.range U) : Type u)) (Subtype.val (p := fun (x : X.Opens) ↦ x ∈ Set.range U))
      ⋯).I₀
⊢ P
    ((X.openCoverOfIsOpenCover (s := (↑(Set.range U) : Type u)) (Subtype.val (p := fun (x : X.Opens) ↦ x ∈ Set.range U))
            ⋯).f
        i ≫
      f)
have obtain : ∀ (i : ι),
  P (X :=
    (X.openCoverOfIsOpenCover (s := (↑(Set.range U) : Type u)) (Subtype.val (p := fun (x : X.Opens) ↦ x ∈ Set.range U))
          sorry).X
      (Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ Set.range U) (U i) sorry))
    ((X.openCoverOfIsOpenCover (s := (↑(Set.range U) : Type u)) (Subtype.val (p := fun (x : X.Opens) ↦ x ∈ Set.range U))
            sorry).f
        (Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ Set.range U) (U i) sorry) ≫
      f)
Tactic: obtain ⟨_, i, rfl⟩ := i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.OpenCover.{u_1, u} X
H : ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ f)
⊢ P f
have refine : ∀ (i : 𝒰.I₀),
  P (X := (↑((fun (i : 𝒰.I₀) ↦ Scheme.Hom.opensRange (𝒰.f i)) i) : Scheme))
    (Scheme.Opens.ι ((fun (i : 𝒰.I₀) ↦ Scheme.Hom.opensRange (𝒰.f i)) i) ≫ f)
Tactic: refine of_iSup_eq_top (fun i ↦ (𝒰.f i).opensRange) 𝒰.iSup_opensRange fun i ↦ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.OpenCover.{u_1, u} X
H : ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ f)
i : 𝒰.I₀
⊢ P (X := (↑((fun (i : 𝒰.I₀) ↦ Scheme.Hom.opensRange (𝒰.f i)) i) : Scheme))
    (Scheme.Opens.ι ((fun (i : 𝒰.I₀) ↦ Scheme.Hom.opensRange (𝒰.f i)) i) ≫ f)
have rw : P (𝒰.f i ≫ f)
Tactic: rw [← IsOpenImmersion.isoOfRangeEq_inv_fac (𝒰.f i) (Scheme.Opens.ι _)
    (congr_arg Opens.carrier (𝒰.f i).opensRange.opensRange_ι.symm), Category.assoc,
    P.cancel_left_of_respectsIso]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
inst_1 : P.IsMultiplicative
hP : ∀ {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) [IsOpenImmersion g], P (f ≫ g) → P f
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover Y
i : 𝒰.I₀
hf : P f
⊢ P (X := pullback f (𝒰.f i)) (pullback.snd f (𝒰.f i))
have apply : P (X := pullback f (𝒰.f i)) (pullback.snd f (𝒰.f i) ≫ 𝒰.f i)
Tactic: apply hP _ (𝒰.f i)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
inst_1 : P.IsMultiplicative
hP : ∀ {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) [IsOpenImmersion g], P (f ≫ g) → P f
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover Y
i : 𝒰.I₀
hf : P f
⊢ P (X := pullback f (𝒰.f i)) (pullback.snd f (𝒰.f i) ≫ 𝒰.f i)
have rw : P (X := pullback f (𝒰.f i)) (pullback.fst f (𝒰.f i) ≫ f)
Tactic: rw [← pullback.condition]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
inst_1 : P.IsMultiplicative
hP : ∀ {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) [IsOpenImmersion g], P (f ≫ g) → P f
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover Y
h : ∀ (i : 𝒰.I₀), P (X := pullback f (𝒰.f i)) (pullback.snd f (𝒰.f i))
⊢ P f
have rw : ∀ (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀), P ((Precoverage.ZeroHypercover.pullback₁ f 𝒰).f i ≫ f)
Tactic: rw [P.iff_of_zeroHypercover_source (𝒰.pullback₁ f)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
inst_1 : P.IsMultiplicative
hP : ∀ {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) [IsOpenImmersion g], P (f ≫ g) → P f
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover Y
h : ∀ (i : 𝒰.I₀), P (X := pullback f (𝒰.f i)) (pullback.snd f (𝒰.f i))
i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀
⊢ P ((Precoverage.ZeroHypercover.pullback₁ f 𝒰).f i ≫ f)
have rw : P (X := (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i)
  (Scheme.Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i ≫ 𝒰.f i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ Y)
Tactic: rw [← Scheme.Cover.pullbackHom_map]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
X : Scheme
ι : Type v
inst_1 : Small.{u, v} ι
Y : ι → Scheme
f : (i : ι) → Y i ⟶ X
hf : ∀ (i : ι), P (f i)
⊢ P (X := ∐ Y) (Sigma.desc f)
have rw : ∀
  (i :
    PreZeroHypercover.I₀ (S := colimit (Discrete.functor Y))
      (Precoverage.ZeroHypercover.toPreZeroHypercover (Scheme.IsLocallyDirected.openCover (Discrete.functor Y)) :
        PreZeroHypercover.{v, u, u + 1} (colimit (Discrete.functor Y)))),
  P (X :=
    PreZeroHypercover.X
      (Precoverage.ZeroHypercover.toPreZeroHypercover (Scheme.IsLocallyDirected.openCover (Discrete.functor Y))) i)
    (CategoryStruct.comp (Y := colimit (Discrete.functor Y))
        (PreZeroHypercover.f
            (Precoverage.ZeroHypercover.toPreZeroHypercover (Scheme.IsLocallyDirected.openCover (Discrete.functor Y)))
            i :
          PreZeroHypercover.X
              (Precoverage.ZeroHypercover.toPreZeroHypercover (Scheme.IsLocallyDirected.openCover (Discrete.functor Y)))
              i ⟶
            colimit (Discrete.functor Y))
        (Sigma.desc f : ∐ Y ⟶ X) :
      PreZeroHypercover.X
          (Precoverage.ZeroHypercover.toPreZeroHypercover (Scheme.IsLocallyDirected.openCover (Discrete.functor Y))) i ⟶
        X)
Tactic: rw [IsZariskiLocalAtSource.iff_of_openCover (P := P) (Scheme.IsLocallyDirected.openCover _)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
inst_1 : IsZariskiLocalAtTarget P
inst_2 : P.RespectsRight IsOpenImmersion
⊢ P f ↔ ∀ (x : ↥X), ∃ (U : Y.Opens) (V : X.Opens) (_ : x ∈ V.carrier) (e : V ≤ f ⁻¹ᵁ U), P (Scheme.Hom.resLE f U V e)
have refine : ∀ (hf : ∀ (x : ↥X), ∃ (U : Y.Opens) (V : X.Opens) (_ : x ∈ V.carrier) (e : V ≤ f ⁻¹ᵁ U), P (Scheme.Hom.resLE f U V e)),
  P f
Tactic: refine ⟨fun hf x ↦ ⟨⊤, ⊤, trivial, by simp, resLE _ hf⟩, fun hf ↦ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
inst_1 : IsZariskiLocalAtTarget P
inst_2 : P.RespectsRight IsOpenImmersion
hf : ∀ (x : ↥X), ∃ (U : Y.Opens) (V : X.Opens) (_ : x ∈ V.carrier) (e : V ≤ f ⁻¹ᵁ U), P (Scheme.Hom.resLE f U V e)
⊢ P f
have choose : ∀ (U : (x : ↥X) → Y.Opens) (V : (x : ↥X) → X.Opens) (hxU : ∀ (x : ↥X), x ∈ (V x).carrier)
  (e : ∀ (x : ↥X), V x ≤ f ⁻¹ᵁ U x) (hf : ∀ (x : ↥X), P (Scheme.Hom.resLE f (U x) (V x) sorry)), P f
Tactic: choose U V hxU e hf using hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
inst_1 : IsZariskiLocalAtTarget P
inst_2 : P.RespectsRight IsOpenImmersion
U : (x : ↥X) → Y.Opens
V : (x : ↥X) → X.Opens
hxU : ∀ (x : ↥X), x ∈ (V x).carrier
e : ∀ (x : ↥X), V x ≤ f ⁻¹ᵁ U x
hf : ∀ (x : ↥X), P (Scheme.Hom.resLE f (U x) (V x) ⋯)
⊢ P f
have rw : ∀ (i : ↥X), P ((V i).ι ≫ f)
Tactic: rw [IsZariskiLocalAtSource.iff_of_iSup_eq_top (fun x : X ↦ V x) (P := P)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
inst_1 : IsZariskiLocalAtTarget P
inst_2 : P.RespectsRight IsOpenImmersion
U : (x : ↥X) → Y.Opens
V : (x : ↥X) → X.Opens
hxU : ∀ (x : ↥X), x ∈ (V x).carrier
e : ∀ (x : ↥X), V x ≤ f ⁻¹ᵁ U x
hf : ∀ (x : ↥X), P (Scheme.Hom.resLE f (U x) (V x) ⋯)
rw : ∀ (i : ↥X), P ((V i).ι ≫ f)
⊢ P f
have rw₁ : Eq.{u + 1} (α := X.Opens) (⨆ (x : ↥X), V x) ⊤
Tactic: rw [IsZariskiLocalAtSource.iff_of_iSup_eq_top (fun x : X ↦ V x) (P := P)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
inst_1 : IsZariskiLocalAtTarget P
inst_2 : P.RespectsRight IsOpenImmersion
U : (x : ↥X) → Y.Opens
V : (x : ↥X) → X.Opens
hxU : ∀ (x : ↥X), x ∈ (V x).carrier
e : ∀ (x : ↥X), V x ≤ f ⁻¹ᵁ U x
hf : ∀ (x : ↥X), P (Scheme.Hom.resLE f (U x) (V x) ⋯)
x : ↥X
⊢ P ((V x).ι ≫ f)
have rw : P (Scheme.Hom.resLE f (U x) (V x) sorry ≫ (U x).ι)
Tactic: rw [← Scheme.Hom.resLE_comp_ι _ (e x)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
inst_1 : IsZariskiLocalAtTarget P
inst_2 : P.RespectsRight IsOpenImmersion
U : (x : ↥X) → Y.Opens
V : (x : ↥X) → X.Opens
hxU : ∀ (x : ↥X), x ∈ (V x).carrier
e : ∀ (x : ↥X), V x ≤ f ⁻¹ᵁ U x
hf : ∀ (x : ↥X), P (Scheme.Hom.resLE f (U x) (V x) ⋯)
⊢ Eq.{u + 1} (α := X.Opens) (⨆ (x : ↥X), V x) ⊤
have rw : LE.le.{u} (α := X.Opens) ⊤ (⨆ (x : ↥X), V x)
Tactic: rw [eq_top_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
inst_1 : IsZariskiLocalAtTarget P
inst_2 : P.RespectsRight IsOpenImmersion
U : (x : ↥X) → Y.Opens
V : (x : ↥X) → X.Opens
hxU : ∀ (x : ↥X), x ∈ (V x).carrier
e : ∀ (x : ↥X), V x ≤ f ⁻¹ᵁ U x
hf : ∀ (x : ↥X), P (Scheme.Hom.resLE f (U x) (V x) ⋯)
x : ↥X
⊢ Membership.mem (γ := Opens ↥X) (⨆ (x : ↥X), V x) x
have simp : ∃ (i : ↥X), x ∈ V i
Tactic: simp only [Opens.mem_iSup]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
inst_1 : IsZariskiLocalAtTarget P
inst_2 : P.RespectsRight IsOpenImmersion
U : (x : ↥X) → Y.Opens
V : (x : ↥X) → X.Opens
hxU : ∀ (x : ↥X), x ∈ (V x).carrier
e : ∀ (x : ↥X), V x ≤ f ⁻¹ᵁ U x
hf : ∀ (x : ↥X), P (Scheme.Hom.resLE f (U x) (V x) ⋯)
x w : ↥X
⊢ ∃ (i : ↥X), x ∈ V i
have h : x ∈ V x
Tactic: use x, hxU x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
Goal:
P : AffineTargetMorphismProperty
inst : P.toProperty.RespectsIso
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst_1 : IsIso f
inst_2 : IsAffine Z
⊢ P (f ≫ g) ↔ P g
have rw : P.toProperty (f ≫ g) ↔ P g
Tactic: rw [← P.toProperty_apply, ← P.toProperty_apply, P.toProperty.cancel_left_of_respectsIso]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
Goal:
P : AffineTargetMorphismProperty
inst : P.toProperty.RespectsIso
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst_1 : IsIso f
inst_2 : IsAffine Z
rw : P.toProperty (f ≫ g) ↔ P g
⊢ P (f ≫ g) ↔ P g
have rw₁ : P.toProperty (f ≫ g) ↔ P.toProperty g
Tactic: rw [← P.toProperty_apply, ← P.toProperty_apply, P.toProperty.cancel_left_of_respectsIso]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
Goal:
P : AffineTargetMorphismProperty
inst : P.toProperty.RespectsIso
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst_1 : IsIso f
inst_2 : IsAffine Z
rw : P.toProperty (f ≫ g) ↔ P g
rw₁ : P.toProperty (f ≫ g) ↔ P.toProperty g
⊢ P (f ≫ g) ↔ P g
have rw₂ : P.toProperty g ↔ P.toProperty g
Tactic: rw [← P.toProperty_apply, ← P.toProperty_apply, P.toProperty.cancel_left_of_respectsIso]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
Goal:
P : AffineTargetMorphismProperty
inst : P.toProperty.RespectsIso
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst_1 : IsIso g
inst_2 : IsAffine Z
inst_3 : IsAffine Y
⊢ P (f ≫ g) ↔ P f
have rw : P.toProperty (f ≫ g) ↔ P f
Tactic: rw [← P.toProperty_apply, ← P.toProperty_apply,
      P.toProperty.cancel_right_of_respectsIso]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
Goal:
P : AffineTargetMorphismProperty
inst : P.toProperty.RespectsIso
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst_1 : IsIso g
inst_2 : IsAffine Z
inst_3 : IsAffine Y
rw : P.toProperty (f ≫ g) ↔ P f
⊢ P (f ≫ g) ↔ P f
have rw₁ : P.toProperty (f ≫ g) ↔ P.toProperty f
Tactic: rw [← P.toProperty_apply, ← P.toProperty_apply,
      P.toProperty.cancel_right_of_respectsIso]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
Goal:
P : AffineTargetMorphismProperty
inst : P.toProperty.RespectsIso
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst_1 : IsIso g
inst_2 : IsAffine Z
inst_3 : IsAffine Y
rw : P.toProperty (f ≫ g) ↔ P f
rw₁ : P.toProperty (f ≫ g) ↔ P.toProperty f
⊢ P (f ≫ g) ↔ P f
have rw₂ : P.toProperty f ↔ P.toProperty f
Tactic: rw [← P.toProperty_apply, ← P.toProperty_apply,
      P.toProperty.cancel_right_of_respectsIso]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
Goal:
P : AffineTargetMorphismProperty
inst : P.toProperty.RespectsIso
X Y X' Y' : Scheme
f : X ⟶ Y
f' : X' ⟶ Y'
e : Arrow.mk f ≅ Arrow.mk f'
h : IsAffine Y
⊢ P f ↔ P f'
have rw : P.toProperty f ↔ P f'
Tactic: rw [← P.toProperty_apply, ← P.toProperty_apply, P.toProperty.arrow_mk_iso_iff e]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
Goal:
P : AffineTargetMorphismProperty
inst : P.toProperty.RespectsIso
X Y X' Y' : Scheme
f : X ⟶ Y
f' : X' ⟶ Y'
e : Arrow.mk f ≅ Arrow.mk f'
h : IsAffine Y
rw : P.toProperty f ↔ P f'
⊢ P f ↔ P f'
have rw₁ : P.toProperty f ↔ P.toProperty f'
Tactic: rw [← P.toProperty_apply, ← P.toProperty_apply, P.toProperty.arrow_mk_iso_iff e]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
Goal:
P : AffineTargetMorphismProperty
inst : P.toProperty.RespectsIso
X Y X' Y' : Scheme
f : X ⟶ Y
f' : X' ⟶ Y'
e : Arrow.mk f ≅ Arrow.mk f'
h : IsAffine Y
rw : P.toProperty f ↔ P f'
rw₁ : P.toProperty f ↔ P.toProperty f'
⊢ P f ↔ P f'
have rw₂ : P.toProperty f' ↔ P.toProperty f'
Tactic: rw [← P.toProperty_apply, ← P.toProperty_apply, P.toProperty.arrow_mk_iso_iff e]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
Goal:
P : AffineTargetMorphismProperty
h₁ : ∀ {X Y Z : Scheme.{u_1}} (e : X ≅ Y) (f : Y ⟶ Z) [inst : IsAffine Z], P f → P (e.hom ≫ f)
h₂ : ∀ {X Y Z : Scheme.{u_1}} (e : Y ≅ Z) (f : X ⟶ Y) [inst : IsAffine Y], P f → P (f ≫ e.hom)
⊢ P.toProperty.RespectsIso
have hprecomp : ∀ {X Y Z : Scheme.{u_1}} (e : X ≅ Y) (f : Y ⟶ Z), P.toProperty f → P.toProperty (e.hom ≫ f)
Tactic: apply MorphismProperty.RespectsIso.mk
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
Goal:
P : AffineTargetMorphismProperty
h₁ : ∀ {X Y Z : Scheme.{u_1}} (e : X ≅ Y) (f : Y ⟶ Z) [inst : IsAffine Z], P f → P (e.hom ≫ f)
h₂ : ∀ {X Y Z : Scheme.{u_1}} (e : Y ≅ Z) (f : X ⟶ Y) [inst : IsAffine Y], P f → P (f ≫ e.hom)
hprecomp : ∀ {X Y Z : Scheme.{u_1}} (e : X ≅ Y) (f : Y ⟶ Z), P.toProperty f → P.toProperty (e.hom ≫ f)
⊢ P.toProperty.RespectsIso
have hpostcomp : ∀ {X Y Z : Scheme.{u_1}} (e : Y ≅ Z) (f : X ⟶ Y), P.toProperty f → P.toProperty (f ≫ e.hom)
Tactic: apply MorphismProperty.RespectsIso.mk
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
Goal:
P : MorphismProperty Scheme
inst : P.RespectsIso
⊢ (of P).toProperty.RespectsIso
have h₁ : ∀ {X Y Z : Scheme.{u_1}} (e : X ≅ Y) (f : Y ⟶ Z) [inst : IsAffine Z], of P f → of P (e.hom ≫ f)
Tactic: apply respectsIso_mk
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
Goal:
P : MorphismProperty Scheme
inst : P.RespectsIso
h₁ : ∀ {X Y Z : Scheme.{u_1}} (e : X ≅ Y) (f : Y ⟶ Z) [inst : IsAffine Z], of P f → of P (e.hom ≫ f)
⊢ (of P).toProperty.RespectsIso
have h₂ : ∀ {X Y Z : Scheme.{u_1}} (e : Y ≅ Z) (f : X ⟶ Y) [inst : IsAffine Y], of P f → of P (f ≫ e.hom)
Tactic: apply respectsIso_mk
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
Goal:
P : AffineTargetMorphismProperty
inst : P.toProperty.RespectsIso
H :
  ∀ ⦃X Y S : Scheme.{u_1}⦄ [inst : IsAffine S] [inst_3 : IsAffine X] (f : X ⟶ S) (g : Y ⟶ S),
    P g → P (X := pullback f g) (pullback.fst f g)
Z X Y S : Scheme
inst_1 : IsAffine S
inst_2 : IsAffine X
f : X ⟶ S
g : Y ⟶ S
f' : Z ⟶ Y
g' : Z ⟶ X
h : IsPullback g' f' f g
hg : P g
⊢ P g'
have rw : P (X := pullback f g) (pullback.fst f g)
Tactic: rw [← P.cancel_left_of_respectsIso h.isoPullback.inv, h.isoPullback_inv_fst]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
Goal:
P : AffineTargetMorphismProperty
inst : P.IsLocal
X Y UX UY : Scheme
inst_1 : IsAffine UY
f : X ⟶ Y
iY : UY ⟶ Y
inst_2 : IsOpenImmersion iY
iX : UX ⟶ X
f' : UX ⟶ UY
h : IsPullback iX f' f iY
hf : targetAffineLocally P f
⊢ P f'
have rw : P (X := pullback f iY) (pullback.snd f iY)
Tactic: rw [← P.cancel_left_of_respectsIso h.isoPullback.inv, h.isoPullback_inv_snd]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
Goal:
P : AffineTargetMorphismProperty
inst : P.toProperty.RespectsIso
⊢ (targetAffineLocally P).RespectsIso
have hprecomp : ∀ {X Y Z : Scheme.{u_1}} (e : X ≅ Y) (f : Y ⟶ Z), targetAffineLocally P f → targetAffineLocally P (e.hom ≫ f)
Tactic: apply MorphismProperty.RespectsIso.mk
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
Goal:
P : AffineTargetMorphismProperty
inst : P.toProperty.RespectsIso
hprecomp : ∀ {X Y Z : Scheme.{u_1}} (e : X ≅ Y) (f : Y ⟶ Z), targetAffineLocally P f → targetAffineLocally P (e.hom ≫ f)
⊢ (targetAffineLocally P).RespectsIso
have hpostcomp : ∀ {X Y Z : Scheme.{u_1}} (e : Y ≅ Z) (f : X ⟶ Y), targetAffineLocally P f → targetAffineLocally P (f ≫ e.hom)
Tactic: apply MorphismProperty.RespectsIso.mk
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
Goal:
P : AffineTargetMorphismProperty
inst : P.toProperty.RespectsIso
X Y Z : Scheme
e : X ≅ Y
f : Y ⟶ Z
H : targetAffineLocally P f
U : (↑Z.affineOpens : Type u_1)
⊢ P (X := (↑((e.hom ≫ f) ⁻¹ᵁ (↑U : Z.Opens)) : Scheme)) ((e.hom ≫ f) ∣_ (↑U : Z.Opens))
have hprecomp : P (X := (↑(f ⁻¹ᵁ (↑U : Z.Opens)) : Scheme)) (f ∣_ (↑U : Z.Opens))
Tactic: rw [morphismRestrict_comp, P.cancel_left_of_respectsIso]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
Goal:
P : AffineTargetMorphismProperty
inst : P.toProperty.RespectsIso
X Y Z : Scheme
e : Y ≅ Z
f : X ⟶ Y
H : targetAffineLocally P f
U : Z.Opens
hU : IsAffineOpen U
⊢ P (X := (↑((f ≫ e.hom) ⁻¹ᵁ (↑(Subtype.mk (p := fun (x : Z.Opens) ↦ x ∈ Z.affineOpens) U hU) : Z.Opens)) : Scheme))
    ((f ≫ e.hom) ∣_ (↑(Subtype.mk (p := fun (x : Z.Opens) ↦ x ∈ Z.affineOpens) U hU) : Z.Opens))
have hpostcomp : P ((f ≫ e.hom) ∣_ U)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
Goal:
P : AffineTargetMorphismProperty
inst : P.toProperty.RespectsIso
X Y Z : Scheme
e : Y ≅ Z
f : X ⟶ Y
H : targetAffineLocally P f
U : Z.Opens
hU : IsAffineOpen U
⊢ P ((f ≫ e.hom) ∣_ U)
have hpostcomp : ∀ (this : IsAffine.{u_1} (↑(e.hom ⁻¹ᵁ U) : Scheme)), P ((f ≫ e.hom) ∣_ U)
Tactic: haveI : IsAffine _ := hU.preimage_of_isIso e.hom