awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
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
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)
⊢ P (X := pullback g f) (pullback.fst g f)

Tactic:
rw [IsZariskiLocalAtSource.iff_of_openCover (P := P) (𝒰.pullback₁ <| pullback.snd g f)]

Premises used: CategoryTheory.Limits.pullback.snd, AlgebraicGeometry.IsZariskiLocalAtSource.iff_of_openCover, CategoryTheory.Precoverage.ZeroHypercover.pullback₁
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
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) 𝒰))
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)
⊢ P
    (PreZeroHypercover.f
        (Precoverage.ZeroHypercover.toPreZeroHypercover (Precoverage.ZeroHypercover.pullback₁ (pullback.snd g f) 𝒰)) i ≫
      pullback.fst g f)

Tactic:
dsimp only [Precoverage.ZeroHypercover.pullback₁_toPreZeroHypercover,
      PreZeroHypercover.pullback₁_X, PreZeroHypercover.pullback₁_f]

Premises used: CategoryTheory.Precoverage.ZeroHypercover.pullback₁_toPreZeroHypercover, CategoryTheory.PreZeroHypercover.pullback₁_X, CategoryTheory.PreZeroHypercover.pullback₁_f
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
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) 𝒰))
refine_2 : P (X := pullback g (𝒰.f i ≫ f)) (pullback.fst g (𝒰.f i ≫ 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)

Tactic:
rw [← pullbackLeftPullbackSndIso_hom_fst, P.cancel_left_of_respectsIso]

Premises used: CategoryTheory.Limits.pullbackLeftPullbackSndIso_hom_fst, CategoryTheory.MorphismProperty.cancel_left_of_respectsIso
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
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 g (𝒰.f i ≫ f)) (pullback.fst g (𝒰.f i ≫ f))

Tactic:
hf i _ _ _ (IsPullback.of_hasPullback ..)

Premises used: CategoryTheory.IsPullback.of_hasPullback
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
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 g (𝒰.f i ≫ f)) (pullback.fst g (𝒰.f i ≫ f))

Tactic:
exact hf i _ _ _ (IsPullback.of_hasPullback ..)

Premises used: CategoryTheory.IsPullback.of_hasPullback
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
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
simp : P (α := ↥X) (β := ↥Z) (Function.comp (β := ↥Y) ⇑g ⇑f)
⊢ topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ P) (f ≫ g)

Tactic:
simp only [topologically, Scheme.Hom.comp_base, TopCat.coe_comp]

Premises used: AlgebraicGeometry.topologically, AlgebraicGeometry.Scheme.Hom.comp_base, TopCat.coe_comp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
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
⊢ P (α := ↥X) (β := ↥Z) (Function.comp (β := ↥Y) ⇑g ⇑f)

Tactic:
hP _ _ hf hg
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
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
⊢ P (α := ↥X) (β := ↥Z) (Function.comp (β := ↥Y) ⇑g ⇑f)

Tactic:
exact hP _ _ hf hg
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
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
IsIso :
  ∀ (he : CategoryTheory.IsIso e), topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ P) e
⊢ MorphismProperty.isomorphisms Scheme e →
    topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ P) e

Tactic:
(he : IsIso e)
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
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
he : IsIso e
⊢ topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ P) e

Tactic:
hP (TopCat.homeoOfIso (asIso e.base))

Premises used: AlgebraicGeometry.topologically, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', TopCat.homeoOfIso, AlgebraicGeometry.PresheafedSpace.Hom.base, CategoryTheory.asIso
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
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
he : IsIso e
⊢ topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ P) e

Tactic:
exact hP (TopCat.homeoOfIso (asIso e.base))

Premises used: AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', TopCat.homeoOfIso, AlgebraicGeometry.PresheafedSpace.Hom.base, CategoryTheory.asIso
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
P : {α β : Type u} → [TopologicalSpace α] → [TopologicalSpace β] → (α → β) → Prop
hP₁ :
  ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α ≃ₜ β),
    P (α := α) (β := β) (⇑f : (a : α) → β)
hP₂ :
  ∀ {α β γ : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : TopologicalSpace γ] (f : α → β)
    (g : β → γ), P f → P g → P (g ∘ f)
⊢ (topologically fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ P).RespectsIso

Tactic:
have : (topologically P).IsStableUnderComposition :=
    topologically_isStableUnderComposition P hP₂
  MorphismProperty.respectsIso_of_isStableUnderComposition (topologically_iso_le P hP₁)

Premises used: AlgebraicGeometry.topologically_iso_le, CategoryTheory.MorphismProperty.respectsIso_of_isStableUnderComposition, AlgebraicGeometry.topologically_isStableUnderComposition
-- 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_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)
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
⊢ IsZariskiLocalAtTarget.{u} (topologically fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ P)

Tactic:
apply IsZariskiLocalAtTarget.mk'

Premises used: AlgebraicGeometry.IsZariskiLocalAtTarget.mk'
-- 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_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
restrict : P (α := ↥(↑(f ⁻¹ᵁ U) : Scheme)) (U.carrier.restrictPreimage ⇑f)
⊢ topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ P) (f ∣_ U)

Tactic:
simp_rw [topologically, morphismRestrict_base]

Premises used: AlgebraicGeometry.morphismRestrict_base, AlgebraicGeometry.topologically
-- 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_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
⊢ P (α := ↥(↑(f ⁻¹ᵁ U) : Scheme)) (U.carrier.restrictPreimage ⇑f)

Tactic:
hP₂ f U.carrier f.continuous U.2 hf

Premises used: CategoryTheory.ConcreteCategory.hom, Set.Mem, setOf, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', TopologicalSpace.Opens.carrier, Set.preimage, AlgebraicGeometry.PresheafedSpace.Hom.base, AlgebraicGeometry.Scheme.Hom.continuous, TopologicalSpace.Opens.is_open', DFunLike.coe
-- 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_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
⊢ P (α := ↥(↑(f ⁻¹ᵁ U) : Scheme)) (U.carrier.restrictPreimage ⇑f)

Tactic:
exact hP₂ f U.carrier f.continuous U.2 hf

Premises used: CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', TopologicalSpace.Opens.carrier, AlgebraicGeometry.PresheafedSpace.Hom.base, AlgebraicGeometry.Scheme.Hom.continuous, TopologicalSpace.Opens.is_open', DFunLike.coe
-- 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_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)
apply : ∀ (i : ι), P (α := (↑(⇑f ⁻¹' (U i).carrier) : Type u)) ((U i).carrier.restrictPreimage ⇑f)
⊢ topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ P) f

Tactic:
apply hP₃ f U hU f.continuous fun i ↦ ?_

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₂ :
  ∀ {α β : 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 : ι
rw : P (α := (↑(⇑f ⁻¹' (U i).carrier) : Type u)) (β := (↑(U i).carrier : Type u)) ⇑(f ∣_ U i)
⊢ P (α := (↑(⇑f ⁻¹' (U i).carrier) : Type u)) ((U i).carrier.restrictPreimage ⇑f)

Tactic:
rw [← morphismRestrict_base]

Premises used: AlgebraicGeometry.morphismRestrict_base
-- 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_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 : Type u)) ⇑(f ∣_ U i)

Tactic:
hf i

Premises used: Set.Mem, setOf, AlgebraicGeometry.topologically, Set.preimage
-- 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_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 : Type u)) ⇑(f ∣_ U i)

Tactic:
exact hf i
-- 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_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)

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

Premises used: Iff.mpr, AlgebraicGeometry.topologically_isZariskiLocalAtTarget
-- 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_1 : TopologicalSpace β] (f : α → β) {ι : Type u} (U : ι → Opens β),
    IsOpenCover U → Continuous f → (P f ↔ ∀ (i : ι), P ((U i).carrier.restrictPreimage f))
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)
⊢ IsZariskiLocalAtTarget.{u} (topologically fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ P)

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

Premises used: Iff.mpr, AlgebraicGeometry.topologically_isZariskiLocalAtTarget
-- 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
⊢ P (s.restrictPreimage f)

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

Premises used: Set.Mem, Function.comp, Equiv.ulift, TopologicalSpace.Opens.mk, 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 :
  ∀ {α β : 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
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))
⊢ P (s.restrictPreimage f)

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

Premises used: Function.comp, Equiv.ulift, TopologicalSpace.Opens.mk, 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 :
  ∀ {α β : 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
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))
⊢ 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:
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 :
  ∀ {α β : 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:
le_iSup (![⊤, Opens.mk s hs] ∘ Equiv.ulift) ⟨0⟩

Premises used: Set.Mem, Function.comp, Equiv.ulift, le_iSup, TopologicalSpace.Opens.mk, Matrix.vecEmpty, Top.top, OfNat.ofNat, ULift.up, DFunLike.coe, Matrix.vecCons