awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₁ :
  ∀ {X Y : Type u} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : X → Y),
    Continuous f → ∀ (U : Opens X), P f → P (α := ↥U) (f ∘ Subtype.val (p := fun (x : X) ↦ x ∈ U))
hP₂ :
  ∀ {X Y : Type u} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : X → Y),
    Continuous f →
      ∀ {ι : Type u} (U : ι → Opens X),
        IsOpenCover U → (∀ (i : ι), P (α := ↥(U i)) (f ∘ Subtype.val (p := fun (x : X) ↦ x ∈ U i))) → P f
⊢ IsZariskiLocalAtSource.{u} (topologically fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ P)
have restrict : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) (U : X.Opens),
  topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ P) f →
    topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ P) (U.ι ≫ f)
Tactic: apply IsZariskiLocalAtSource.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₁ :
  ∀ {X Y : Type u} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : X → Y),
    Continuous f → ∀ (U : Opens X), P f → P (α := ↥U) (f ∘ Subtype.val (p := fun (x : X) ↦ x ∈ U))
hP₂ :
  ∀ {X Y : Type u} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : X → Y),
    Continuous f →
      ∀ {ι : Type u} (U : ι → Opens X),
        IsOpenCover U → (∀ (i : ι), P (α := ↥(U i)) (f ∘ Subtype.val (p := fun (x : X) ↦ x ∈ U i))) → P f
restrict :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) (U : X.Opens),
    topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ P) f →
      topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ P) (U.ι ≫ f)
⊢ IsZariskiLocalAtSource.{u} (topologically fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ P)
have of_sSup_eq_top : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) {ι : Type u} (U : ι → X.Opens),
  iSup U = ⊤ →
    (∀ (i : ι), topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ P) ((U i).ι ≫ f)) →
      topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ P) f
Tactic: apply IsZariskiLocalAtSource.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 :
  ∀ {X Y : Type u} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : X → Y) {ι : Type u} (U : ι → Opens X),
    IsOpenCover U → Continuous f → (P f ↔ ∀ (i : ι), P (α := ↥(U i)) (f ∘ Subtype.val (p := fun (x : X) ↦ x ∈ U i)))
⊢ IsZariskiLocalAtSource.{u} (topologically fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ P)
have refine : ∀ {X Y : Type u} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : X → Y),
  Continuous f →
    ∀ (U : Opens X),
      (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ (P : (α → β) → Prop)) f →
        (@fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ (P : (α → β) → Prop)) ↥U _ _ _
          (f ∘ Subtype.val (p := fun (x : X) ↦ x ∈ U))
Tactic: refine topologically_isZariskiLocalAtSource P ?_ (fun f hf _ U hU hf' ↦ (hP f U hU hf).mpr hf')
-- 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 :
  ∀ {X Y : Type u} [inst : TopologicalSpace X] [inst_3 : TopologicalSpace Y] (f : X → Y) {ι : Type u} (U : ι → Opens X),
    IsOpenCover U → Continuous f → (P f ↔ ∀ (i : ι), P (α := ↥(U i)) (f ∘ Subtype.val (p := fun (x : X) ↦ x ∈ U i)))
X Y : Type u
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
f : X → Y
hf : Continuous f
U : Opens X
hs : P f
⊢ P (α := ↥U) (f ∘ Subtype.val (p := fun (x : X) ↦ x ∈ U))
have refine : IsOpenCover (ι := ULift.{u, 0} (Fin (Nat.succ 0).succ))
  (![⊤, U] ∘ (⇑Equiv.ulift : (a : ULift.{u, 0} (Fin (Nat.succ 0).succ)) → Fin (Nat.succ 0).succ))
Tactic: refine (hP f (![⊤, U] ∘ Equiv.ulift) ?_ hf).mp hs ⟨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 :
  ∀ {X Y : Type u} [inst : TopologicalSpace X] [inst_3 : TopologicalSpace Y] (f : X → Y) {ι : Type u} (U : ι → Opens X),
    IsOpenCover U → Continuous f → (P f ↔ ∀ (i : ι), P (α := ↥(U i)) (f ∘ Subtype.val (p := fun (x : X) ↦ x ∈ U i)))
X Y : Type u
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
f : X → Y
hf : Continuous f
U : Opens X
hs : P f
⊢ IsOpenCover (ι := ULift.{u, 0} (Fin (Nat.succ 0).succ))
    (![⊤, U] ∘ (⇑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))
    (![⊤, U] ∘ (⇑Equiv.ulift : (a : ULift.{u, 0} (Fin (Nat.succ 0).succ)) → Fin (Nat.succ 0).succ))
Tactic: rw [IsOpenCover, ← top_le_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Constructors (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
X Y Z : Scheme
e : X ⟶ Y
he : IsIso e
f : Y ⟶ Z
hf : stalkwise (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f
⊢ stalkwise (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) (e ≫ f)
have simp : ∀ (x : ↥X), P (CommRingCat.Hom.hom (Scheme.Hom.stalkMap (e ≫ f) x))
Tactic: simp only [stalkwise, Scheme.Hom.comp_base, TopCat.coe_comp, Function.comp_apply]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Constructors (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
X Y Z : Scheme
e : X ⟶ Y
he : IsIso e
f : Y ⟶ Z
hf : stalkwise (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f
x : ↥X
⊢ P (CommRingCat.Hom.hom (Scheme.Hom.stalkMap (e ≫ f) x))
have rw : P (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f (e x) ≫ Scheme.Hom.stalkMap e x))
Tactic: rw [Scheme.Hom.stalkMap_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Constructors (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
X Y Z : Scheme
e : Y ⟶ Z
he : IsIso e
f : X ⟶ Y
hf : stalkwise (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f
⊢ stalkwise (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) (f ≫ e)
have simp : ∀ (x : ↥X), P (CommRingCat.Hom.hom (Scheme.Hom.stalkMap (f ≫ e) x))
Tactic: simp only [stalkwise, Scheme.Hom.comp_base, TopCat.coe_comp, Function.comp_apply]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Constructors (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
X Y Z : Scheme
e : Y ⟶ Z
he : IsIso e
f : X ⟶ Y
hf : stalkwise (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f
x : ↥X
⊢ P (CommRingCat.Hom.hom (Scheme.Hom.stalkMap (f ≫ e) x))
have rw : P (CommRingCat.Hom.hom (Scheme.Hom.stalkMap e (f x) ≫ Scheme.Hom.stalkMap f x))
Tactic: rw [Scheme.Hom.stalkMap_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Constructors (hypothesis)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
⊢ IsZariskiLocalAtTarget.{u} (stalkwise fun {R S : Type u} [CommRing R] [CommRing S] ↦ P)
have hP' : (RingHom.toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).RespectsIso
Tactic: have hP' : (RingHom.toMorphismProperty P).RespectsIso :=
    RingHom.toMorphismProperty_respectsIso_iff.mp hP
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Constructors (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hP' : (RingHom.toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).RespectsIso
this : (stalkwise fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).RespectsIso := ⋯
⊢ IsZariskiLocalAtTarget.{u} (stalkwise fun {R S : Type u} [CommRing R] [CommRing S] ↦ P)
have restrict : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) (U : Y.Opens),
  stalkwise (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f →
    stalkwise (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) (f ∣_ U)
Tactic: apply IsZariskiLocalAtTarget.mk'
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Constructors (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hP' : (RingHom.toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).RespectsIso
this : (stalkwise fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).RespectsIso := ⋯
restrict :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) (U : Y.Opens),
    stalkwise (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f →
      stalkwise (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) (f ∣_ U)
⊢ IsZariskiLocalAtTarget.{u} (stalkwise fun {R S : Type u} [CommRing R] [CommRing S] ↦ P)
have of_sSup_eq_top : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens),
  iSup U = ⊤ →
    (∀ (i : ι), stalkwise fun {R S : Type u} [CommRing R] [CommRing S] ↦ P (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)) →
      stalkwise (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f
Tactic: apply IsZariskiLocalAtTarget.mk'
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Constructors (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hP' : (RingHom.toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).RespectsIso
this : (stalkwise fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).RespectsIso := ⋯
X Y : Scheme
f : X ⟶ Y
ι : Type u
U : ι → Y.Opens
hU : iSup U = ⊤
hf : ∀ (i : ι), stalkwise fun {R S : Type u} [CommRing R] [CommRing S] ↦ P (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)
x : ↥X
⊢ Membership.mem (α := ↥Y) (iSup U) (f x : ↥Y)
have rw : Membership.mem (α := ↥Y) (γ := Y.Opens) ⊤ (f x : ↥Y)
Tactic: rw [hU]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Constructors (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hP' : (RingHom.toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).RespectsIso
this : (stalkwise fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).RespectsIso := ⋯
X Y : Scheme
f : X ⟶ Y
ι : Type u
U : ι → Y.Opens
hU : iSup U = ⊤
hf : ∀ (i : ι), stalkwise fun {R S : Type u} [CommRing R] [CommRing S] ↦ P (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)
x : ↥X
⊢ P (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
have of_sSup_eq_top : ∀ (hy : Membership.mem (α := ↥Y) (iSup U) (f x : ↥Y)), P (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
Tactic: have hy : f x ∈ iSup U := by rw [hU]; trivial
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Constructors (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hP' : (RingHom.toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).RespectsIso
this : (stalkwise fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).RespectsIso := ⋯
X Y : Scheme
f : X ⟶ Y
ι : Type u
U : ι → Y.Opens
hU : iSup U = ⊤
hf : ∀ (i : ι), stalkwise fun {R S : Type u} [CommRing R] [CommRing S] ↦ P (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)
x : ↥X
hy : Membership.mem (α := ↥Y) (iSup U) (f x : ↥Y)
⊢ P (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
have of_sSup_eq_top : ∀ (i : ι) (hi : Membership.mem (α := ↥Y) (U i) (f x : ↥Y)), P (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
Tactic: obtain ⟨i, hi⟩ := Opens.mem_iSup.mp hy
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Constructors (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
this : (stalkwise fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).RespectsIso := ⋯
⊢ IsZariskiLocalAtSource.{u} (stalkwise fun {R S : Type u} [CommRing R] [CommRing S] ↦ P)
have restrict : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) (U : X.Opens),
  stalkwise (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f →
    stalkwise (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) (U.ι ≫ f)
Tactic: apply IsZariskiLocalAtSource.mk'
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Constructors (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
this : (stalkwise fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).RespectsIso := ⋯
restrict :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) (U : X.Opens),
    stalkwise (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f →
      stalkwise (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) (U.ι ≫ f)
⊢ IsZariskiLocalAtSource.{u} (stalkwise fun {R S : Type u} [CommRing R] [CommRing S] ↦ P)
have of_sSup_eq_top : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) {ι : Type u} (U : ι → X.Opens),
  iSup U = ⊤ →
    (∀ (i : ι), stalkwise (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) ((U i).ι ≫ f)) →
      stalkwise (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f
Tactic: apply IsZariskiLocalAtSource.mk'
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Constructors (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
this : (stalkwise fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).RespectsIso := ⋯
X Y : Scheme
f : X ⟶ Y
U : X.Opens
hf : stalkwise (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f
x : ↥(↑U : Scheme)
⊢ P (CommRingCat.Hom.hom (Scheme.Hom.stalkMap (U.ι ≫ f) x))
have restrict : P (R := (↑(Y.presheaf.stalk ((U.ι ≫ f) x)) : Type u)) (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f (U.ι x)))
Tactic: rw [Scheme.Hom.stalkMap_comp, CommRingCat.hom_comp, hP.cancel_right_isIso]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Constructors (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
this : (stalkwise fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).RespectsIso := ⋯
X Y : Scheme
f : X ⟶ Y
ι : Type u
U : ι → X.Opens
hU : iSup U = ⊤
hf : ∀ (i : ι), stalkwise (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) ((U i).ι ≫ f)
x : ↥X
⊢ x ∈ iSup U
have rw : Membership.mem (γ := X.Opens) ⊤ x
Tactic: rw [hU]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Constructors (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
this : (stalkwise fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).RespectsIso := ⋯
X Y : Scheme
f : X ⟶ Y
ι : Type u
U : ι → X.Opens
hU : iSup U = ⊤
hf : ∀ (i : ι), stalkwise (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) ((U i).ι ≫ f)
x : ↥X
⊢ P (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
have of_sSup_eq_top : ∀ (hy : x ∈ iSup U), P (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
Tactic: have hy : x ∈ iSup U := by rw [hU]; trivial
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Constructors (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
this : (stalkwise fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).RespectsIso := ⋯
X Y : Scheme
f : X ⟶ Y
ι : Type u
U : ι → X.Opens
hU : iSup U = ⊤
hf : ∀ (i : ι), stalkwise (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) ((U i).ι ≫ f)
x : ↥X
hy : x ∈ iSup U
⊢ P (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
have of_sSup_eq_top : ∀ (i : ι) (hi : x ∈ U i), P (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
Tactic: obtain ⟨i, hi⟩ := Opens.mem_iSup.mp hy
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Constructors (hypothesis)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S : CommRingCat
φ : R ⟶ S
⊢ stalkwise (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) (Spec.map φ) ↔
    ∀ (p : Ideal (↑S : Type u)) (x : p.IsPrime),
      P (R := Localization.AtPrime (Ideal.comap (CommRingCat.Hom.hom φ) p)) (S := Localization.AtPrime p)
        (Localization.localRingHom (Ideal.comap (CommRingCat.Hom.hom φ) p) p (CommRingCat.Hom.hom φ) ⋯)
have hP' : (RingHom.toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).RespectsIso
Tactic: have hP' : (RingHom.toMorphismProperty P).RespectsIso :=
    RingHom.toMorphismProperty_respectsIso_iff.mp hP
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Constructors (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S : CommRingCat
φ : R ⟶ S
hP' : (RingHom.toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).RespectsIso
⊢ stalkwise (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) (Spec.map φ) ↔
    ∀ (p : Ideal (↑S : Type u)) (x : p.IsPrime),
      P (R := Localization.AtPrime (Ideal.comap (CommRingCat.Hom.hom φ) p)) (S := Localization.AtPrime p)
        (Localization.localRingHom (Ideal.comap (CommRingCat.Hom.hom φ) p) p (CommRingCat.Hom.hom φ) ⋯)
have trans : stalkwise (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) (Spec.map φ) ↔
  ∀ (p : PrimeSpectrum (↑S : Type u)),
    P (R := Localization.AtPrime (Ideal.comap (CommRingCat.Hom.hom φ) p.asIdeal)) (S := Localization.AtPrime p.asIdeal)
      (Localization.localRingHom (Ideal.comap (CommRingCat.Hom.hom φ) p.asIdeal) p.asIdeal (CommRingCat.Hom.hom φ) sorry)
Tactic: trans ∀ (p : PrimeSpectrum S), P (Localization.localRingHom _ p.asIdeal φ.hom rfl)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Constructors (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S : CommRingCat
φ : R ⟶ S
hP' : (RingHom.toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).RespectsIso
trans :
  stalkwise (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) (Spec.map φ) ↔
    ∀ (p : PrimeSpectrum (↑S : Type u)),
      P (R := Localization.AtPrime (Ideal.comap (CommRingCat.Hom.hom φ) p.asIdeal)) (S :=
        Localization.AtPrime p.asIdeal)
        (Localization.localRingHom (Ideal.comap (CommRingCat.Hom.hom φ) p.asIdeal) p.asIdeal (CommRingCat.Hom.hom φ) ⋯)
⊢ stalkwise (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) (Spec.map φ) ↔
    ∀ (p : Ideal (↑S : Type u)) (x : p.IsPrime),
      P (R := Localization.AtPrime (Ideal.comap (CommRingCat.Hom.hom φ) p)) (S := Localization.AtPrime p)
        (Localization.localRingHom (Ideal.comap (CommRingCat.Hom.hom φ) p) p (CommRingCat.Hom.hom φ) ⋯)
have trans₁ : (∀ (p : PrimeSpectrum (↑S : Type u)),
    P (R := Localization.AtPrime (Ideal.comap (CommRingCat.Hom.hom φ) p.asIdeal)) (S := Localization.AtPrime p.asIdeal)
      (Localization.localRingHom (Ideal.comap (CommRingCat.Hom.hom φ) p.asIdeal) p.asIdeal (CommRingCat.Hom.hom φ) sorry)) ↔
  ∀ (p : Ideal (↑S : Type u)) (x : p.IsPrime),
    P (R := Localization.AtPrime (Ideal.comap (CommRingCat.Hom.hom φ) p)) (S := Localization.AtPrime p)
      (Localization.localRingHom (Ideal.comap (CommRingCat.Hom.hom φ) p) p (CommRingCat.Hom.hom φ) sorry)
Tactic: trans ∀ (p : PrimeSpectrum S), P (Localization.localRingHom _ p.asIdeal φ.hom rfl)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Descent (goal)
Goal:
P : MorphismProperty Scheme
X : Scheme
inst : CompactSpace.{u} ↥X
inst_1 : IsZariskiLocalAtSource P
inst_2 : P.ContainsIdentities
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
p : (∐ fun (i : 𝒰.I₀) ↦ 𝒰.X i) ⟶ X := Sigma.desc fun (i : 𝒰.I₀) ↦ 𝒰.f i
⊢ ∃ (Y : Scheme.{u}) (p : Y ⟶ X), Surjective p ∧ P p ∧ IsAffine Y
have refine_1 : ∀ (x : ↥X), ∃ (a : ↥(∐ fun (i : 𝒰.I₀) ↦ 𝒰.X i)), p a = x
Tactic: refine ⟨_, p, ⟨fun x ↦ ?_⟩, ?_, inferInstance⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Descent (goal)
Goal:
P : MorphismProperty Scheme
X : Scheme
inst : CompactSpace.{u} ↥X
inst_1 : IsZariskiLocalAtSource P
inst_2 : P.ContainsIdentities
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
p : (∐ fun (i : 𝒰.I₀) ↦ 𝒰.X i) ⟶ X := Sigma.desc fun (i : 𝒰.I₀) ↦ 𝒰.f i
refine_1 : ∀ (x : ↥X), ∃ (a : ↥(∐ fun (i : 𝒰.I₀) ↦ 𝒰.X i)), p a = x
⊢ ∃ (Y : Scheme.{u}) (p : Y ⟶ X), Surjective p ∧ P p ∧ IsAffine Y
have refine_2 : P p
Tactic: refine ⟨_, p, ⟨fun x ↦ ?_⟩, ?_, inferInstance⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Descent (goal)
Goal:
P : MorphismProperty Scheme
X : Scheme
inst : CompactSpace.{u} ↥X
inst_1 : IsZariskiLocalAtSource P
inst_2 : P.ContainsIdentities
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
p : (∐ fun (i : 𝒰.I₀) ↦ 𝒰.X i) ⟶ X := Sigma.desc fun (i : 𝒰.I₀) ↦ 𝒰.f i
x : ↥X
⊢ ∃ (a : ↥(∐ fun (i : 𝒰.I₀) ↦ 𝒰.X i)), p a = x
have refine_1 : ∀ (i : X.affineCover.finiteSubcover.I₀) (x : ↥(X.affineCover.finiteSubcover.X i)),
  ∃ (a : ↥(∐ fun (i : 𝒰.I₀) ↦ 𝒰.X i)), Eq (α := ↥X) (p a : ↥X) ((X.affineCover.finiteSubcover.f i) x : ↥X)
Tactic: obtain ⟨i, x, rfl⟩ := X.affineCover.finiteSubcover.exists_eq x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Descent (goal)
Goal:
P : MorphismProperty Scheme
X : Scheme
inst : CompactSpace.{u} ↥X
inst_1 : IsZariskiLocalAtSource P
inst_2 : P.ContainsIdentities
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
p : (∐ fun (i : 𝒰.I₀) ↦ 𝒰.X i) ⟶ X := Sigma.desc fun (i : 𝒰.I₀) ↦ 𝒰.f i
i : X.affineCover.finiteSubcover.I₀
x : ↥(X.affineCover.finiteSubcover.X i)
⊢ ∃ (a : ↥(∐ fun (i : 𝒰.I₀) ↦ 𝒰.X i)), Eq (α := ↥X) (p a : ↥X) ((X.affineCover.finiteSubcover.f i) x : ↥X)
have h : Eq (α := ↥X) (p ((Sigma.ι X.affineCover.finiteSubcover.X i) x : ↥(∐ X.affineCover.finiteSubcover.X)) : ↥X)
  ((X.affineCover.finiteSubcover.f i) x : ↥X)
Tactic: use Sigma.ι X.affineCover.finiteSubcover.X i x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Descent (goal)
Goal:
P : MorphismProperty Scheme
X : Scheme
inst : CompactSpace.{u} ↥X
inst_1 : IsZariskiLocalAtSource P
inst_2 : P.ContainsIdentities
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
p : (∐ fun (i : 𝒰.I₀) ↦ 𝒰.X i) ⟶ X := Sigma.desc fun (i : 𝒰.I₀) ↦ 𝒰.f i
i : X.affineCover.finiteSubcover.I₀
x : ↥(X.affineCover.finiteSubcover.X i)
⊢ Eq (α := ↥X) (p ((Sigma.ι X.affineCover.finiteSubcover.X i) x : ↥(∐ X.affineCover.finiteSubcover.X)) : ↥X)
    ((X.affineCover.finiteSubcover.f i) x : ↥X)
have h : Eq (α := ↥X) ((Sigma.ι X.affineCover.finiteSubcover.X i ≫ p) x : ↥X) ((X.affineCover.finiteSubcover.f i) x : ↥X)
Tactic: rw [← Scheme.Hom.comp_apply, Sigma.ι_desc]