awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Integral
Goal:
R S : CommRingCat
φ : R ⟶ S
H₁ : UniversallyClosed (Spec.map φ)
H₂ : IsAffineHom (Spec.map φ)
h : IsClosedMap (PrimeSpectrum.comap (Polynomial.mapRingHom (CommRingCat.Hom.hom φ)))
⊢ (CommRingCat.Hom.hom φ).IsIntegral

Tactic:
apply PrimeSpectrum.isIntegral_of_isClosedMap_comap_mapRingHom

Premises used: PrimeSpectrum.isIntegral_of_isClosedMap_comap_mapRingHom
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Integral
Goal:
R S : CommRingCat
φ : R ⟶ S
H₁ : UniversallyClosed (Spec.map φ)
H₂ : IsAffineHom (Spec.map φ)
algInst : Algebra (↑R : Type u) (↑S : Type u) := φ.hom'.toAlgebra
algInst_1 : Algebra (Polynomial (↑R : Type u)) (Polynomial (↑S : Type u)) := (Polynomial.mapRingHom φ.hom').toAlgebra
⊢ IsClosedMap (PrimeSpectrum.comap (Polynomial.mapRingHom (CommRingCat.Hom.hom φ)))

Tactic:
H₁.universally_isClosedMap (Spec.map (CommRingCat.ofHom Polynomial.C))
    (Spec.map (CommRingCat.ofHom Polynomial.C)) (Spec.map _)
    (isPullback_SpecMap_of_isPushout _ _ _ _
    (CommRingCat.isPushout_of_isPushout R S (Polynomial R) (Polynomial S))).flip

Premises used: Polynomial.C, CommRingCat.carrier, Set.Mem, setOf, CommRingCat.ofHom, AlgebraicGeometry.Spec.map, CommRingCat.isPushout_of_isPushout, AlgebraicGeometry.topologically, AlgebraicGeometry.isPullback_SpecMap_of_isPushout, Polynomial, AlgebraicGeometry.UniversallyClosed.universally_isClosedMap, Polynomial.mapRingHom, CategoryTheory.IsPullback.flip, PrimeSpectrum.comap
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Integral
Goal:
R S : CommRingCat
φ : R ⟶ S
H₁ : UniversallyClosed (Spec.map φ)
H₂ : IsAffineHom (Spec.map φ)
algInst : Algebra (↑R : Type u) (↑S : Type u) := φ.hom'.toAlgebra
algInst_1 : Algebra (Polynomial (↑R : Type u)) (Polynomial (↑S : Type u)) := (Polynomial.mapRingHom φ.hom').toAlgebra
⊢ IsClosedMap (PrimeSpectrum.comap (Polynomial.mapRingHom (CommRingCat.Hom.hom φ)))

Tactic:
exact H₁.universally_isClosedMap (Spec.map (CommRingCat.ofHom Polynomial.C))
    (Spec.map (CommRingCat.ofHom Polynomial.C)) (Spec.map _)
    (isPullback_SpecMap_of_isPushout _ _ _ _
    (CommRingCat.isPushout_of_isPushout R S (Polynomial R) (Polynomial S))).flip

Premises used: Polynomial.C, CommRingCat.carrier, CommRingCat.ofHom, AlgebraicGeometry.Spec.map, CommRingCat.isPushout_of_isPushout, AlgebraicGeometry.isPullback_SpecMap_of_isPushout, Polynomial, AlgebraicGeometry.UniversallyClosed.universally_isClosedMap, CategoryTheory.IsPullback.flip
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Integral
Goal:
h : ∀ (x x_1 : Scheme.{u_1}) (x_2 : x ⟶ x_1), IsIntegralHom x_2 ↔ (@UniversallyClosed ⊓ @IsAffineHom) x_2
⊢ @IsIntegralHom = @UniversallyClosed ⊓ @IsAffineHom

Tactic:
ext
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Integral
Goal:
x x_1 : Scheme
x_2 : x ⟶ x_1
⊢ IsIntegralHom x_2 ↔ (@UniversallyClosed ⊓ @IsAffineHom) x_2

Tactic:
iff_universallyClosed_and_isAffineHom

Premises used: AlgebraicGeometry.IsIntegralHom.iff_universallyClosed_and_isAffineHom
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Integral
Goal:
x x_1 : Scheme
x_2 : x ⟶ x_1
⊢ IsIntegralHom x_2 ↔ (@UniversallyClosed ⊓ @IsAffineHom) x_2

Tactic:
exact iff_universallyClosed_and_isAffineHom

Premises used: AlgebraicGeometry.IsIntegralHom.iff_universallyClosed_and_isAffineHom
-- Module: Mathlib.AlgebraicGeometry.Morphisms.IsIso
Goal:
X Y : Scheme
f : X ⟶ Y
rw : IsIso f ↔ IsOpenImmersion f ∧ Function.Surjective (α := ↥X) (β := ↥Y) ⇑f
rw₁ : IsIso f ↔ IsOpenImmersion f ∧ Epi f.base
rw₂ rw₃ : IsOpenImmersion f ∧ Epi f.base ↔ IsOpenImmersion f ∧ Epi f.base
⊢ IsIso f ↔ IsOpenImmersion f ∧ Surjective f

Tactic:
rw [surjective_iff, ← TopCat.epi_iff_surjective, isIso_iff_isOpenImmersion_and_epi_base]

Premises used: AlgebraicGeometry.surjective_iff, AlgebraicGeometry.isIso_iff_isOpenImmersion_and_epi_base, TopCat.epi_iff_surjective
-- Module: Mathlib.AlgebraicGeometry.Morphisms.IsIso
Goal:
h : ∀ ⦃X Y : Scheme.{u_1}⦄ (f : X ⟶ Y), isomorphisms Scheme f ↔ (IsOpenImmersion ⊓ @Surjective) f
⊢ isomorphisms Scheme = IsOpenImmersion ⊓ @Surjective

Tactic:
ext
-- Module: Mathlib.AlgebraicGeometry.Morphisms.IsIso
Goal:
X Y : Scheme
f : X ⟶ Y
h : IsOpenImmersion f ∧ Surjective f ↔ (IsOpenImmersion ⊓ @Surjective) f
⊢ isomorphisms Scheme f ↔ (IsOpenImmersion ⊓ @Surjective) f

Tactic:
rw [isomorphisms.iff, isIso_iff_isOpenImmersion_and_surjective]

Premises used: CategoryTheory.MorphismProperty.isomorphisms.iff, AlgebraicGeometry.isIso_iff_isOpenImmersion_and_surjective
-- Module: Mathlib.AlgebraicGeometry.Morphisms.IsIso
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ IsOpenImmersion f ∧ Surjective f ↔ (IsOpenImmersion ⊓ @Surjective) f

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.IsIso
Goal:
rw :
  (((topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] ↦ Topology.IsOpenEmbedding) ⊓
        topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] ↦ Function.Surjective) ⊓
      stalkwise fun {R S : Type u_1} [CommRing R] [CommRing S] (x : R →+* S) ↦
        Function.Bijective (α := R) (β := S) (⇑x : (a : R) → S)) =
    inverseImage (isomorphisms TopCat) Scheme.forgetToTop ⊓
      stalkwise fun {R S : Type u_1} [CommRing R] [CommRing S] (f : R →+* S) ↦
        Function.Bijective (α := R) (β := S) (⇑f : (a : R) → S)
⊢ isomorphisms Scheme =
    inverseImage (isomorphisms TopCat) Scheme.forgetToTop ⊓
      stalkwise fun {R S : Type u_1} [CommRing R] [CommRing S] (f : R →+* S) ↦
        Function.Bijective (α := R) (β := S) (⇑f : (a : R) → S)

Tactic:
rw [isomorphisms_eq_isOpenImmersion_inf_surjective, isOpenImmersion_eq_inf,
    surjective_eq_topologically, inf_right_comm]

Premises used: AlgebraicGeometry.isOpenImmersion_eq_inf, inf_right_comm, AlgebraicGeometry.isomorphisms_eq_isOpenImmersion_inf_surjective, AlgebraicGeometry.surjective_eq_topologically
-- Module: Mathlib.AlgebraicGeometry.Morphisms.IsIso
Goal:
e_a :
  ((topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] ↦ Topology.IsOpenEmbedding) ⊓
      topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] ↦ Function.Surjective) =
    inverseImage (isomorphisms TopCat) Scheme.forgetToTop
⊢ (((topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] ↦ Topology.IsOpenEmbedding) ⊓
        topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] ↦ Function.Surjective) ⊓
      stalkwise fun {R S : Type u_1} [CommRing R] [CommRing S] (x : R →+* S) ↦
        Function.Bijective (α := R) (β := S) (⇑x : (a : R) → S)) =
    inverseImage (isomorphisms TopCat) Scheme.forgetToTop ⊓
      stalkwise fun {R S : Type u_1} [CommRing R] [CommRing S] (f : R →+* S) ↦
        Function.Bijective (α := R) (β := S) (⇑f : (a : R) → S)

Tactic:
congr 1
-- Module: Mathlib.AlgebraicGeometry.Morphisms.IsIso
Goal:
e_a :
  ∀ ⦃X Y : Scheme.{u_1}⦄ (f : X ⟶ Y),
    ((topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] ↦ Topology.IsOpenEmbedding) ⊓
          topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] ↦ Function.Surjective)
        f ↔
      inverseImage (isomorphisms TopCat) Scheme.forgetToTop f
⊢ ((topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] ↦ Topology.IsOpenEmbedding) ⊓
      topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] ↦ Function.Surjective) =
    inverseImage (isomorphisms TopCat) Scheme.forgetToTop

Tactic:
ext X Y f
-- Module: Mathlib.AlgebraicGeometry.Morphisms.IsIso
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ ((topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] ↦ Topology.IsOpenEmbedding) ⊓
        topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] ↦ Function.Surjective)
      f ↔
    inverseImage (isomorphisms TopCat) Scheme.forgetToTop f

Tactic:
⟨fun H ↦ inferInstanceAs (IsIso (TopCat.isoOfHomeo
    (H.1.1.toHomeomorphOfSurjective H.2)).hom), fun (_ : IsIso f.base) ↦
    let e := (TopCat.homeoOfIso <| asIso f.base); ⟨e.isOpenEmbedding, e.surjective⟩⟩

Premises used: Topology.IsOpenEmbedding.toIsEmbedding, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', CategoryTheory.Iso.isIso_hom, TopCat.homeoOfIso, And.right, And.left, TopCat.isoOfHomeo, And.intro, Iff.intro, AlgebraicGeometry.PresheafedSpace.Hom.base, Homeomorph.isOpenEmbedding, Homeomorph.surjective, Topology.IsEmbedding.toHomeomorphOfSurjective, CategoryTheory.asIso
-- Module: Mathlib.AlgebraicGeometry.Morphisms.IsIso
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ ((topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] ↦ Topology.IsOpenEmbedding) ⊓
        topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] ↦ Function.Surjective)
      f ↔
    inverseImage (isomorphisms TopCat) Scheme.forgetToTop f

Tactic:
exact ⟨fun H ↦ inferInstanceAs (IsIso (TopCat.isoOfHomeo
    (H.1.1.toHomeomorphOfSurjective H.2)).hom), fun (_ : IsIso f.base) ↦
    let e := (TopCat.homeoOfIso <| asIso f.base); ⟨e.isOpenEmbedding, e.surjective⟩⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.IsIso
Goal:
⊢ IsZariskiLocalAtTarget.{u_1} (isomorphisms Scheme)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.IsIso
Goal:
⊢ HasAffineProperty.{u_1} (isomorphisms Scheme) (AffineTargetMorphismProperty.of (isomorphisms Scheme))

Tactic:
HasAffineProperty.of_isZariskiLocalAtTarget (isomorphisms Scheme)

Premises used: AlgebraicGeometry.Scheme, CategoryTheory.MorphismProperty.isomorphisms, AlgebraicGeometry.HasAffineProperty.of_isZariskiLocalAtTarget
-- Module: Mathlib.AlgebraicGeometry.Morphisms.IsIso
Goal:
h :
  ∀ (X Y : Scheme.{u_1}) (f : X ⟶ Y) (hY : IsAffine Y),
    IsAffine X ∧ IsIso (Scheme.Hom.appTop f) ↔ AffineTargetMorphismProperty.of (isomorphisms Scheme) f
⊢ HasAffineProperty.{u_1} (isomorphisms Scheme) fun (X x : Scheme.{u_1}) (f : X ⟶ x) (x_1 : IsAffine x) ↦
    IsAffine X ∧ IsIso (Scheme.Hom.appTop f)

Tactic:
convert! HasAffineProperty.of_isZariskiLocalAtTarget (isomorphisms Scheme) with X Y f hY

Premises used: AlgebraicGeometry.Scheme, CategoryTheory.MorphismProperty.isomorphisms, AlgebraicGeometry.HasAffineProperty.of_isZariskiLocalAtTarget
-- Module: Mathlib.AlgebraicGeometry.Morphisms.IsIso
Goal:
X Y : Scheme
f : X ⟶ Y
hY : IsAffine Y
⊢ IsAffine X ∧ IsIso (Scheme.Hom.appTop f) ↔ AffineTargetMorphismProperty.of (isomorphisms Scheme) f

Tactic:
⟨fun ⟨_, _⟩ ↦ (arrow_mk_iso_iff (isomorphisms _) (arrowIsoSpecΓOfIsAffine f)).mpr
    (inferInstanceAs (IsIso (Spec.map (f.appTop)))),
    fun (_ : IsIso f) ↦ ⟨.of_isIso f, inferInstance⟩⟩

Premises used: Iff.mpr, AlgebraicGeometry.Scheme, _private.0.AlgebraicGeometry.instHasAffinePropertyIsomorphismsSchemeAndIsAffineIsIsoCommRingCatAppTop._proof_1, AlgebraicGeometry.IsAffine.of_isIso, AlgebraicGeometry.AffineTargetMorphismProperty.of, AlgebraicGeometry.arrowIsoSpecΓOfIsAffine, inferInstance, CategoryTheory.MorphismProperty.isomorphisms, CategoryTheory.MorphismProperty.arrow_mk_iso_iff, _private.0.AlgebraicGeometry.instHasAffinePropertyIsomorphismsSchemeAndIsAffineIsIsoCommRingCatAppTop.match_1, And.intro, Iff.intro
-- Module: Mathlib.AlgebraicGeometry.Morphisms.IsIso
Goal:
X Y : Scheme
f : X ⟶ Y
hY : IsAffine Y
⊢ IsAffine X ∧ IsIso (Scheme.Hom.appTop f) ↔ AffineTargetMorphismProperty.of (isomorphisms Scheme) f

Tactic:
exact ⟨fun ⟨_, _⟩ ↦ (arrow_mk_iso_iff (isomorphisms _) (arrowIsoSpecΓOfIsAffine f)).mpr
    (inferInstanceAs (IsIso (Spec.map (f.appTop)))),
    fun (_ : IsIso f) ↦ ⟨.of_isIso f, inferInstance⟩⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.IsIso
Goal:
⊢ IsZariskiLocalAtTarget.{u_1} (monomorphisms Scheme)

Tactic:
diagonal_isomorphisms (C := Scheme).symm ▸ inferInstance

Premises used: Eq.rec, inferInstance, CategoryTheory.MorphismProperty.diagonal_isomorphisms, Eq.symm
-- Module: Mathlib.AlgebraicGeometry.Morphisms.IsIso
Goal:
R S : CommRingCat
f : R ⟶ S
rw : IsIso (Spec.map f) ↔ IsIso f
⊢ IsIso (Spec.map f) ↔
    Function.Bijective (α := (↑R : Type u)) (β := (↑S : Type u))
      (⇑(CommRingCat.Hom.hom f) : (a : (↑R : Type u)) → (↑S : Type u))

Tactic:
rw [← ConcreteCategory.isIso_iff_bijective]

Premises used: CategoryTheory.ConcreteCategory.isIso_iff_bijective
-- Module: Mathlib.AlgebraicGeometry.Morphisms.IsIso
Goal:
R S : CommRingCat
f : R ⟶ S
⊢ IsIso (Spec.map f) ↔ IsIso f

Tactic:
⟨fun h ↦ ?_, fun h ↦ inferInstance⟩

Premises used: inferInstance, Iff.intro
-- Module: Mathlib.AlgebraicGeometry.Morphisms.IsIso
Goal:
R S : CommRingCat
f : R ⟶ S
refine : ∀ (h : IsIso (Spec.map f)), IsIso f
⊢ IsIso (Spec.map f) ↔ IsIso f

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ inferInstance⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.IsIso
Goal:
R S : CommRingCat
f : R ⟶ S
h : IsIso (Spec.map f)
rw : IsIso (Scheme.Hom.appTop (Spec.map f))
⊢ IsIso f

Tactic:
rw [← isomorphisms.iff, (isomorphisms _).arrow_mk_iso_iff (arrowIsoΓSpecOfIsAffine f),
    isomorphisms.iff]

Premises used: CategoryTheory.MorphismProperty.isomorphisms.iff, CategoryTheory.MorphismProperty.isomorphisms, CategoryTheory.MorphismProperty.arrow_mk_iso_iff, AlgebraicGeometry.arrowIsoΓSpecOfIsAffine
-- Module: Mathlib.AlgebraicGeometry.Morphisms.IsIso
Goal:
R S : CommRingCat
f : R ⟶ S
h : IsIso (Spec.map f)
⊢ IsIso (Scheme.Hom.appTop (Spec.map f))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.LocalClosure
Goal:
W P : MorphismProperty Scheme
X Y : Scheme
f : X ⟶ Y
hf : sourceLocalClosure W P f
i : hf.cover (W := W) (P := P).I₀
⊢ P (hf.cover (W := W) (P := P).f i ≫ f)

Tactic:
hf.choose_spec i

Premises used: Exists.choose_spec
-- Module: Mathlib.AlgebraicGeometry.Morphisms.LocalClosure
Goal:
W P : MorphismProperty Scheme
inst : W.ContainsIdentities
inst_1 : W.RespectsIso
X Y : Scheme
f : X ⟶ Y
hf : P f
⊢ ∀
    (i :
      (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage W)
          (Scheme.coverOfIsIso (P := W) (𝟙 X))).I₀),
    P
      ((Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage W)
              (Scheme.coverOfIsIso (P := W) (𝟙 X))).f
          i ≫
        f)

Tactic:
simpa
-- Module: Mathlib.AlgebraicGeometry.Morphisms.LocalClosure
Goal:
P : MorphismProperty Scheme
X Y : Scheme
inst : P.RespectsIso
f : X ⟶ Y
⊢ sourceLocalClosure IsOpenImmersion P f ↔ ∀ (x : ↥X), ∃ (U : X.Opens), x ∈ U ∧ P (U.ι ≫ f)

Tactic:
⟨fun ⟨𝒰, hf⟩ x ↦ ?_, fun H ↦ ?_⟩

Premises used: Membership.mem, Exists, _private.0.AlgebraicGeometry.sourceLocalClosure.iff_forall_exists.match_1, And, Iff.intro, CategoryTheory.CategoryStruct.comp, AlgebraicGeometry.Scheme.Opens.ι
-- Module: Mathlib.AlgebraicGeometry.Morphisms.LocalClosure
Goal:
P : MorphismProperty Scheme
X Y : Scheme
inst : P.RespectsIso
f : X ⟶ Y
refine_1 :
  sourceLocalClosure IsOpenImmersion P f →
    ∀ (x : ↥X) (𝒰 : Scheme.Cover (Scheme.precoverage IsOpenImmersion) X) (hf : ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ f)),
      ∃ (U : X.Opens), x ∈ U ∧ P (U.ι ≫ f)
refine_2 : ∀ (H : ∀ (x : ↥X), ∃ (U : X.Opens), x ∈ U ∧ P (U.ι ≫ f)), sourceLocalClosure IsOpenImmersion P f
⊢ sourceLocalClosure IsOpenImmersion P f ↔ ∀ (x : ↥X), ∃ (U : X.Opens), x ∈ U ∧ P (U.ι ≫ f)

Tactic:
refine ⟨fun ⟨𝒰, hf⟩ x ↦ ?_, fun H ↦ ?_⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.LocalClosure
Goal:
P : MorphismProperty Scheme
X Y : Scheme
inst : P.RespectsIso
f : X ⟶ Y
h : sourceLocalClosure IsOpenImmersion P f
x : ↥X
𝒰 : Scheme.Cover (Scheme.precoverage IsOpenImmersion) X
hf : ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ f)
⊢ ∃ (U : X.Opens), x ∈ U ∧ P (U.ι ≫ f)

Tactic:
⟨(𝒰.f (𝒰.idx x)).opensRange, 𝒰.covers x, ?_⟩

Premises used: CategoryTheory.PreZeroHypercover.f, AlgebraicGeometry.Scheme.Hom.opensRange, AlgebraicGeometry.Scheme.Cover.covers, And.intro, Exists.intro, AlgebraicGeometry.Scheme.Cover.idx, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.AlgebraicGeometry.Morphisms.LocalClosure
Goal:
P : MorphismProperty Scheme
X Y : Scheme
inst : P.RespectsIso
f : X ⟶ Y
h : sourceLocalClosure IsOpenImmersion P f
x : ↥X
𝒰 : Scheme.Cover (Scheme.precoverage IsOpenImmersion) X
hf : ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ f)
refine_1 : P ((Scheme.Hom.opensRange (X := 𝒰.X (𝒰.idx x)) (𝒰.f (𝒰.idx x))).ι ≫ f)
⊢ ∃ (U : X.Opens), x ∈ U ∧ P (U.ι ≫ f)

Tactic:
refine ⟨(𝒰.f (𝒰.idx x)).opensRange, 𝒰.covers x, ?_⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.LocalClosure
Goal:
P : MorphismProperty Scheme
X Y : Scheme
inst : P.RespectsIso
f : X ⟶ Y
h : sourceLocalClosure IsOpenImmersion P f
x : ↥X
𝒰 : Scheme.Cover (Scheme.precoverage IsOpenImmersion) X
hf : ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ f)
refine_1 : P (X := 𝒰.X (𝒰.idx x)) (𝒰.f (𝒰.idx x) ≫ f)
⊢ P ((Scheme.Hom.opensRange (X := 𝒰.X (𝒰.idx x)) (𝒰.f (𝒰.idx x))).ι ≫ f)

Tactic:
rw [← Scheme.Hom.isoOpensRange_inv_comp, Category.assoc, P.cancel_left_of_respectsIso]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.MorphismProperty.cancel_left_of_respectsIso, AlgebraicGeometry.Scheme.Hom.isoOpensRange_inv_comp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.LocalClosure
Goal:
P : MorphismProperty Scheme
X Y : Scheme
inst : P.RespectsIso
f : X ⟶ Y
h : sourceLocalClosure IsOpenImmersion P f
x : ↥X
𝒰 : Scheme.Cover (Scheme.precoverage IsOpenImmersion) X
hf : ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ f)
⊢ P (X := 𝒰.X (𝒰.idx x)) (𝒰.f (𝒰.idx x) ≫ f)

Tactic:
apply hf
-- Module: Mathlib.AlgebraicGeometry.Morphisms.LocalClosure
Goal:
P : MorphismProperty Scheme
X Y : Scheme
inst : P.RespectsIso
f : X ⟶ Y
H : ∀ (x : ↥X), ∃ (U : X.Opens), x ∈ U ∧ P (U.ι ≫ f)
refine_2 :
  ∀ (U : (x : ↥X) → X.Opens) (hx : ∀ (x : ↥X), x ∈ U x) (hf : ∀ (x : ↥X), P ((U x).ι ≫ f)),
    sourceLocalClosure IsOpenImmersion P f
⊢ sourceLocalClosure IsOpenImmersion P f

Tactic:
choose U hx hf using H
-- Module: Mathlib.AlgebraicGeometry.Morphisms.LocalClosure
Goal:
P : MorphismProperty Scheme
X Y : Scheme
inst : P.RespectsIso
f : X ⟶ Y
U : (x : ↥X) → X.Opens
hx : ∀ (x : ↥X), x ∈ U x
hf : ∀ (x : ↥X), P ((U x).ι ≫ f)
⊢ sourceLocalClosure IsOpenImmersion P f

Tactic:
⟨.mkOfCovers X (fun x ↦ U x) (fun _ ↦ (U _).ι) (fun x ↦ ⟨x, ⟨x, hx x⟩, rfl⟩)
      fun _ ↦ inferInstance, hf⟩

Premises used: AlgebraicGeometry.PresheafedSpace.carrier, AlgebraicGeometry.sourceLocalClosure, inferInstance, Subtype.mk, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, TopCat.carrier, Exists.intro, AlgebraicGeometry.Scheme.Opens.ι, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, AlgebraicGeometry.Scheme.Opens.toScheme, AlgebraicGeometry.Scheme.Cover.mkOfCovers, rfl, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.Morphisms.LocalClosure
Goal:
P : MorphismProperty Scheme
X Y : Scheme
inst : P.RespectsIso
f : X ⟶ Y
U : (x : ↥X) → X.Opens
hx : ∀ (x : ↥X), x ∈ U x
hf : ∀ (x : ↥X), P ((U x).ι ≫ f)
⊢ sourceLocalClosure IsOpenImmersion P f

Tactic:
exact ⟨.mkOfCovers X (fun x ↦ U x) (fun _ ↦ (U _).ι) (fun x ↦ ⟨x, ⟨x, hx x⟩, rfl⟩)
      fun _ ↦ inferInstance, hf⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.LocalClosure
Goal:
W P Q : MorphismProperty Scheme
X Y : Scheme
inst : W.IsStableUnderBaseChange
inst_1 : Scheme.IsJointlySurjectivePreserving W
inst_2 : P.RespectsLeft Q
inst_3 : Q.IsStableUnderBaseChange
⊢ (sourceLocalClosure W P).RespectsLeft Q

Tactic:
⟨fun {X Y} Z f hf g ⟨𝒰, hg⟩ ↦ ⟨𝒰.pullback₁ f, fun i ↦ ?_⟩⟩

Premises used: AlgebraicGeometry.sourceLocalClosure, Exists.intro, CategoryTheory.CategoryStruct.comp, CategoryTheory.Precoverage.ZeroHypercover.pullback₁, CategoryTheory.MorphismProperty.RespectsLeft.mk, _private.0.AlgebraicGeometry.sourceLocalClosure.instRespectsLeftSchemeOfIsStableUnderBaseChange.match_1
-- Module: Mathlib.AlgebraicGeometry.Morphisms.LocalClosure
Goal:
W P Q : MorphismProperty Scheme
X Y : Scheme
inst : W.IsStableUnderBaseChange
inst_1 : Scheme.IsJointlySurjectivePreserving W
inst_2 : P.RespectsLeft Q
inst_3 : Q.IsStableUnderBaseChange
refine :
  ∀ {X Y : Scheme.{u}} (Z : Scheme.{u}) (f : X ⟶ Y) (hf : Q f) (g : Y ⟶ Z),
    sourceLocalClosure W P g →
      ∀ (𝒰 : Scheme.Cover (Scheme.precoverage W) Y) (hg : ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ g))
        (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀), P ((Precoverage.ZeroHypercover.pullback₁ f 𝒰).f i ≫ f ≫ g)
⊢ (sourceLocalClosure W P).RespectsLeft Q

Tactic:
refine ⟨fun {X Y} Z f hf g ⟨𝒰, hg⟩ ↦ ⟨𝒰.pullback₁ f, fun i ↦ ?_⟩⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.LocalClosure
Goal:
W P Q : MorphismProperty Scheme
X_1 Y_1 : Scheme
inst : W.IsStableUnderBaseChange
inst_1 : Scheme.IsJointlySurjectivePreserving W
inst_2 : P.RespectsLeft Q
inst_3 : Q.IsStableUnderBaseChange
X Y Z : Scheme
f : X ⟶ Y
hf : Q f
g : Y ⟶ Z
h : sourceLocalClosure W P g
𝒰 : Scheme.Cover (Scheme.precoverage W) Y
hg : ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ g)
i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀
⊢ P ((Precoverage.ZeroHypercover.pullback₁ f 𝒰).f i ≫ f ≫ g)

Tactic:
simpa [pullback.condition_assoc] using
    RespectsLeft.precomp (Q := Q) _ (Q.pullback_snd _ _ hf) _ (hg i)

Premises used: CategoryTheory.MorphismProperty.RespectsLeft.precomp, CategoryTheory.Limits.pullback.condition_assoc, CategoryTheory.MorphismProperty.pullback_snd
-- Module: Mathlib.AlgebraicGeometry.Morphisms.LocalClosure
Goal:
W P Q : MorphismProperty Scheme
X Y : Scheme
inst : W.IsStableUnderBaseChange
inst_1 : Scheme.IsJointlySurjectivePreserving W
inst_2 : P.RespectsRight Q
⊢ (sourceLocalClosure W P).RespectsRight Q

Tactic:
⟨fun {X Y} Z f hf g ⟨𝒰, hg⟩ ↦ ⟨𝒰, fun i ↦ ?_⟩⟩

Premises used: AlgebraicGeometry.sourceLocalClosure, Exists.intro, CategoryTheory.CategoryStruct.comp, _private.0.AlgebraicGeometry.sourceLocalClosure.instRespectsLeftSchemeOfIsStableUnderBaseChange.match_1, CategoryTheory.MorphismProperty.RespectsRight.mk
-- Module: Mathlib.AlgebraicGeometry.Morphisms.LocalClosure
Goal:
W P Q : MorphismProperty Scheme
X Y : Scheme
inst : W.IsStableUnderBaseChange
inst_1 : Scheme.IsJointlySurjectivePreserving W
inst_2 : P.RespectsRight Q
refine :
  ∀ {X Y : Scheme.{u}} (Z : Scheme.{u}) (f : Y ⟶ Z) (hf : Q f) (g : X ⟶ Y),
    sourceLocalClosure W P g →
      ∀ (𝒰 : Scheme.Cover (Scheme.precoverage W) X) (hg : ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ g)) (i : 𝒰.I₀), P (𝒰.f i ≫ g ≫ f)
⊢ (sourceLocalClosure W P).RespectsRight Q

Tactic:
refine ⟨fun {X Y} Z f hf g ⟨𝒰, hg⟩ ↦ ⟨𝒰, fun i ↦ ?_⟩⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.LocalClosure
Goal:
W P Q : MorphismProperty Scheme
X_1 Y_1 : Scheme
inst : W.IsStableUnderBaseChange
inst_1 : Scheme.IsJointlySurjectivePreserving W
inst_2 : P.RespectsRight Q
X Y Z : Scheme
f : Y ⟶ Z
hf : Q f
g : X ⟶ Y
h : sourceLocalClosure W P g
𝒰 : Scheme.Cover (Scheme.precoverage W) X
hg : ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ g)
i : 𝒰.I₀
rw : P ((𝒰.f i ≫ g) ≫ f)
⊢ P (𝒰.f i ≫ g ≫ f)

Tactic:
rw [← Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.AlgebraicGeometry.Morphisms.LocalClosure
Goal:
W P Q : MorphismProperty Scheme
X_1 Y_1 : Scheme
inst : W.IsStableUnderBaseChange
inst_1 : Scheme.IsJointlySurjectivePreserving W
inst_2 : P.RespectsRight Q
X Y Z : Scheme
f : Y ⟶ Z
hf : Q f
g : X ⟶ Y
h : sourceLocalClosure W P g
𝒰 : Scheme.Cover (Scheme.precoverage W) X
hg : ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ g)
i : 𝒰.I₀
⊢ P ((𝒰.f i ≫ g) ≫ f)

Tactic:
RespectsRight.postcomp _ hf _ (hg i)

Premises used: CategoryTheory.MorphismProperty.RespectsRight.postcomp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.LocalClosure
Goal:
W P Q : MorphismProperty Scheme
X_1 Y_1 : Scheme
inst : W.IsStableUnderBaseChange
inst_1 : Scheme.IsJointlySurjectivePreserving W
inst_2 : P.RespectsRight Q
X Y Z : Scheme
f : Y ⟶ Z
hf : Q f
g : X ⟶ Y
h : sourceLocalClosure W P g
𝒰 : Scheme.Cover (Scheme.precoverage W) X
hg : ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ g)
i : 𝒰.I₀
⊢ P ((𝒰.f i ≫ g) ≫ f)

Tactic:
exact RespectsRight.postcomp _ hf _ (hg i)

Premises used: CategoryTheory.MorphismProperty.RespectsRight.postcomp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.LocalClosure
Goal:
W P Q : MorphismProperty Scheme
X Y : Scheme
inst : W.IsStableUnderBaseChange
inst_1 : Scheme.IsJointlySurjectivePreserving W
inst_2 : P.RespectsIso
inst_3 : P.RespectsLeft IsOpenImmersion
⊢ IsZariskiLocalAtSource.{u} (sourceLocalClosure IsOpenImmersion P)

Tactic:
.mk_of_iff fun f 𝒰 ↦ ?_

Premises used: CategoryTheory.MorphismProperty.IsLocalAtSource.mk_of_iff