awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
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
⊢ ⊤ ≤
    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:
exact le_iSup (![⊤, Opens.mk s hs] ∘ Equiv.ulift) ⟨0⟩

Premises used: Function.comp, Equiv.ulift, le_iSup, TopologicalSpace.Opens.mk, Matrix.vecEmpty, Top.top, OfNat.ofNat, ULift.up, DFunLike.coe, Matrix.vecCons
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
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)
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
⊢ IsZariskiLocalAtSource.{u} (topologically fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ P)

Tactic:
apply IsZariskiLocalAtSource.mk'

Premises used: AlgebraicGeometry.IsZariskiLocalAtSource.mk'
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
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
X Y : Scheme
f : X ⟶ Y
U : X.Opens
hf : topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ P) f
⊢ topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ P) (U.ι ≫ f)

Tactic:
hP₁ f f.continuous _ hf

Premises used: CategoryTheory.ConcreteCategory.hom, Set.Mem, AlgebraicGeometry.topologically, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.PresheafedSpace.Hom.base, AlgebraicGeometry.Scheme.Hom.continuous, DFunLike.coe
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
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
X Y : Scheme
f : X ⟶ Y
U : X.Opens
hf : topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ P) f
⊢ topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ P) (U.ι ≫ f)

Tactic:
exact hP₁ f f.continuous _ hf

Premises used: CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.PresheafedSpace.Hom.base, AlgebraicGeometry.Scheme.Hom.continuous, DFunLike.coe
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
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
X Y : Scheme
f : X ⟶ Y
ι : Type u
U : ι → X.Opens
hU : iSup U = ⊤
hf : ∀ (i : ι), topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ P) ((U i).ι ≫ f)
⊢ topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ P) f

Tactic:
hP₂ f f.continuous _ hU hf

Premises used: CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.topologically, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.PresheafedSpace.Hom.base, AlgebraicGeometry.Scheme.Hom.continuous, DFunLike.coe
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
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
X Y : Scheme
f : X ⟶ Y
ι : Type u
U : ι → X.Opens
hU : iSup U = ⊤
hf : ∀ (i : ι), topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ P) ((U i).ι ≫ f)
⊢ topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ P) f

Tactic:
exact hP₂ f f.continuous _ hU hf

Premises used: CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.PresheafedSpace.Hom.base, AlgebraicGeometry.Scheme.Hom.continuous, DFunLike.coe
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
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)

Tactic:
topologically_isZariskiLocalAtSource P ?_ (fun f hf _ U hU hf' ↦ (hP f U hU hf).mpr hf')

Premises used: Iff.mpr, AlgebraicGeometry.topologically_isZariskiLocalAtSource
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
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)))
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))
⊢ IsZariskiLocalAtSource.{u} (topologically fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ P)

Tactic:
refine topologically_isZariskiLocalAtSource P ?_ (fun f hf _ U hU hf' ↦ (hP f U hU hf).mpr hf')

Premises used: Iff.mpr, AlgebraicGeometry.topologically_isZariskiLocalAtSource
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
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))

Tactic:
(hP f (![⊤, U] ∘ Equiv.ulift) ?_ hf).mp hs ⟨1⟩

Premises used: Set.Mem, Function.comp, Equiv.ulift, Matrix.vecEmpty, Iff.mp, Top.top, OfNat.ofNat, ULift.up, DFunLike.coe, Matrix.vecCons
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
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
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))
⊢ P (α := ↥U) (f ∘ Subtype.val (p := fun (x : X) ↦ x ∈ U))

Tactic:
refine (hP f (![⊤, U] ∘ Equiv.ulift) ?_ hf).mp hs ⟨1⟩

Premises used: Function.comp, Equiv.ulift, Matrix.vecEmpty, Iff.mp, Top.top, OfNat.ofNat, ULift.up, DFunLike.coe, Matrix.vecCons
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
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
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))
⊢ 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:
rw [IsOpenCover, ← top_le_iff]

Premises used: TopologicalSpace.IsOpenCover, top_le_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
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
⊢ ⊤ ≤
    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:
le_iSup (![⊤, U] ∘ Equiv.ulift) ⟨0⟩

Premises used: Set.Mem, Function.comp, Equiv.ulift, le_iSup, Matrix.vecEmpty, Top.top, OfNat.ofNat, ULift.up, DFunLike.coe, Matrix.vecCons
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
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
⊢ ⊤ ≤
    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:
exact le_iSup (![⊤, U] ∘ Equiv.ulift) ⟨0⟩

Premises used: Function.comp, Equiv.ulift, le_iSup, Matrix.vecEmpty, Top.top, OfNat.ofNat, ULift.up, DFunLike.coe, Matrix.vecCons
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
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
simp : ∀ (x : ↥X), P (CommRingCat.Hom.hom (Scheme.Hom.stalkMap (e ≫ f) x))
⊢ stalkwise (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) (e ≫ f)

Tactic:
simp only [stalkwise, Scheme.Hom.comp_base, TopCat.coe_comp, Function.comp_apply]

Premises used: Function.comp_apply, AlgebraicGeometry.Scheme.Hom.comp_base, TopCat.coe_comp, AlgebraicGeometry.stalkwise
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
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
rw : P (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f (e x) ≫ Scheme.Hom.stalkMap e x))
⊢ P (CommRingCat.Hom.hom (Scheme.Hom.stalkMap (e ≫ f) x))

Tactic:
rw [Scheme.Hom.stalkMap_comp]

Premises used: AlgebraicGeometry.Scheme.Hom.stalkMap_comp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
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 f (e x) ≫ Scheme.Hom.stalkMap e x))

Tactic:
(RingHom.RespectsIso.cancel_right_isIso hP _ _).mpr <| hf (e x)

Premises used: Iff.mpr, CategoryTheory.ConcreteCategory.hom, RingHom.RespectsIso.cancel_right_isIso, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.PresheafedSpace.Hom.base, DFunLike.coe
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
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 f (e x) ≫ Scheme.Hom.stalkMap e x))

Tactic:
exact (RingHom.RespectsIso.cancel_right_isIso hP _ _).mpr <| hf (e x)

Premises used: Iff.mpr, CategoryTheory.ConcreteCategory.hom, RingHom.RespectsIso.cancel_right_isIso, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.PresheafedSpace.Hom.base, DFunLike.coe
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
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
simp : ∀ (x : ↥X), P (CommRingCat.Hom.hom (Scheme.Hom.stalkMap (f ≫ e) x))
⊢ stalkwise (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) (f ≫ e)

Tactic:
simp only [stalkwise, Scheme.Hom.comp_base, TopCat.coe_comp, Function.comp_apply]

Premises used: Function.comp_apply, AlgebraicGeometry.Scheme.Hom.comp_base, TopCat.coe_comp, AlgebraicGeometry.stalkwise
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
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
rw : P (CommRingCat.Hom.hom (Scheme.Hom.stalkMap e (f x) ≫ Scheme.Hom.stalkMap f x))
⊢ P (CommRingCat.Hom.hom (Scheme.Hom.stalkMap (f ≫ e) x))

Tactic:
rw [Scheme.Hom.stalkMap_comp]

Premises used: AlgebraicGeometry.Scheme.Hom.stalkMap_comp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
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 e (f x) ≫ Scheme.Hom.stalkMap f x))

Tactic:
(RingHom.RespectsIso.cancel_left_isIso hP _ _).mpr <| hf x

Premises used: Iff.mpr, RingHom.RespectsIso.cancel_left_isIso
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
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 e (f x) ≫ Scheme.Hom.stalkMap f x))

Tactic:
exact (RingHom.RespectsIso.cancel_left_isIso hP _ _).mpr <| hf x

Premises used: Iff.mpr, RingHom.RespectsIso.cancel_left_isIso
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
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
⊢ (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
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
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)
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
⊢ IsZariskiLocalAtTarget.{u} (stalkwise fun {R S : Type u} [CommRing R] [CommRing S] ↦ P)

Tactic:
apply IsZariskiLocalAtTarget.mk'

Premises used: AlgebraicGeometry.IsZariskiLocalAtTarget.mk'
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
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
U : Y.Opens
hf : stalkwise (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f
x : ↥(↑(f ⁻¹ᵁ U) : Scheme)
⊢ P (CommRingCat.Hom.hom (Scheme.Hom.stalkMap (f ∣_ U) x))

Tactic:
apply ((RingHom.toMorphismProperty P).arrow_mk_iso_iff <|
      morphismRestrictStalkMap f U x).mpr <| hf _

Premises used: Iff.mpr, AlgebraicGeometry.morphismRestrictStalkMap, CategoryTheory.MorphismProperty.arrow_mk_iso_iff, RingHom.toMorphismProperty
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
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
rw : Membership.mem (α := ↥Y) (γ := Y.Opens) ⊤ (f x : ↥Y)
⊢ Membership.mem (α := ↥Y) (iSup U) (f x : ↥Y)

Tactic:
rw [hU]
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
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) (γ := Y.Opens) ⊤ (f x : ↥Y)

Tactic:
trivial
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
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
of_sSup_eq_top :
  ∀ (hy : Membership.mem (α := ↥Y) (iSup U) (f x : ↥Y)), P (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
⊢ P (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))

Tactic:
have hy : f x ∈ iSup U := by rw [hU]; trivial