awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
refine :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) (𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X),
    sourceLocalClosure IsOpenImmersion P f ↔ ∀ (i : 𝒰.I₀), sourceLocalClosure IsOpenImmersion P (𝒰.f i ≫ f)
⊢ IsZariskiLocalAtSource.{u} (sourceLocalClosure IsOpenImmersion P)

Tactic:
refine .mk_of_iff fun f 𝒰 ↦ ?_
-- 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
X_1 Y_1 : Scheme
f : X_1 ⟶ Y_1
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X_1
⊢ sourceLocalClosure IsOpenImmersion P f ↔ ∀ (i : 𝒰.I₀), sourceLocalClosure IsOpenImmersion P (𝒰.f i ≫ f)

Tactic:
⟨fun ⟨𝒱, h⟩ ↦ fun i ↦ ⟨𝒱.pullback₁ (𝒰.f i), fun j ↦ ?_⟩, fun h ↦ ?_⟩

Premises used: CategoryTheory.PreZeroHypercover.f, _private.0.AlgebraicGeometry.sourceLocalClosure.iff_forall_exists.match_1, Iff.intro, Exists.intro, CategoryTheory.Precoverage.ZeroHypercover.pullback₁, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- 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
X_1 Y_1 : Scheme
f : X_1 ⟶ Y_1
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X_1
refine_1 :
  sourceLocalClosure IsOpenImmersion P f →
    ∀ (𝒱 : Scheme.Cover (Scheme.precoverage IsOpenImmersion) X_1) (h : ∀ (i : 𝒱.I₀), P (𝒱.f i ≫ f)) (i : 𝒰.I₀)
      (j : (Precoverage.ZeroHypercover.pullback₁ (𝒰.f i) 𝒱).I₀),
      P ((Precoverage.ZeroHypercover.pullback₁ (𝒰.f i) 𝒱).f j ≫ 𝒰.f i ≫ f)
refine_2 :
  ∀ (h : ∀ (i : 𝒰.I₀), sourceLocalClosure IsOpenImmersion P (𝒰.f i ≫ f)), sourceLocalClosure IsOpenImmersion P f
⊢ sourceLocalClosure IsOpenImmersion P f ↔ ∀ (i : 𝒰.I₀), sourceLocalClosure IsOpenImmersion P (𝒰.f i ≫ f)

Tactic:
refine ⟨fun ⟨𝒱, h⟩ ↦ fun i ↦ ⟨𝒱.pullback₁ (𝒰.f i), fun j ↦ ?_⟩, fun h ↦ ?_⟩
-- 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
X_1 Y_1 : Scheme
f : X_1 ⟶ Y_1
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X_1
h_1 : sourceLocalClosure IsOpenImmersion P f
𝒱 : Scheme.Cover (Scheme.precoverage IsOpenImmersion) X_1
h : ∀ (i : 𝒱.I₀), P (𝒱.f i ≫ f)
i : 𝒰.I₀
j : (Precoverage.ZeroHypercover.pullback₁ (𝒰.f i) 𝒱).I₀
⊢ P ((Precoverage.ZeroHypercover.pullback₁ (𝒰.f i) 𝒱).f j ≫ 𝒰.f i ≫ f)

Tactic:
simpa [pullback.condition_assoc] using
      RespectsLeft.precomp (Q := @IsOpenImmersion) _ inferInstance _ (h j)

Premises used: CategoryTheory.MorphismProperty.RespectsLeft.precomp, inferInstance, CategoryTheory.Limits.pullback.condition_assoc
-- 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
X_1 Y_1 : Scheme
f : X_1 ⟶ Y_1
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X_1
h : ∀ (i : 𝒰.I₀), sourceLocalClosure IsOpenImmersion P (𝒰.f i ≫ f)
refine_2 :
  ∀ (𝒱 : (i : 𝒰.I₀) → Scheme.Cover (Scheme.precoverage IsOpenImmersion) (𝒰.X i))
    (h𝒱 : ∀ (i : 𝒰.I₀) (i_1 : (𝒱 i).I₀), P ((𝒱 i).f i_1 ≫ 𝒰.f i ≫ f)), sourceLocalClosure IsOpenImmersion P f
⊢ sourceLocalClosure IsOpenImmersion P f

Tactic:
choose 𝒱 h𝒱 using h
-- 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
X_1 Y_1 : Scheme
f : X_1 ⟶ Y_1
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X_1
𝒱 : (i : 𝒰.I₀) → Scheme.Cover (Scheme.precoverage IsOpenImmersion) (𝒰.X i)
h𝒱 : ∀ (i : 𝒰.I₀) (i_1 : (𝒱 i).I₀), P ((𝒱 i).f i_1 ≫ 𝒰.f i ≫ f)
⊢ sourceLocalClosure IsOpenImmersion P f

Tactic:
⟨𝒰.bind 𝒱, fun i ↦ h𝒱 _ _⟩

Premises used: AlgebraicGeometry.sourceLocalClosure, Sigma.fst, Exists.intro, Sigma.snd, CategoryTheory.Precoverage.ZeroHypercover.bind
-- 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
X_1 Y_1 : Scheme
f : X_1 ⟶ Y_1
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X_1
𝒱 : (i : 𝒰.I₀) → Scheme.Cover (Scheme.precoverage IsOpenImmersion) (𝒰.X i)
h𝒱 : ∀ (i : 𝒰.I₀) (i_1 : (𝒱 i).I₀), P ((𝒱 i).f i_1 ≫ 𝒰.f i ≫ f)
⊢ sourceLocalClosure IsOpenImmersion P f

Tactic:
exact ⟨𝒰.bind 𝒱, fun i ↦ h𝒱 _ _⟩
-- 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.IsStableUnderBaseChange
⊢ (sourceLocalClosure W P).IsStableUnderBaseChange

Tactic:
.mk' fun X Y S f g _ ⟨𝒰, hg⟩ ↦ ⟨𝒰.pullback₁ (pullback.snd f g), fun i ↦ ?_⟩

Premises used: CategoryTheory.Limits.pullback.snd, AlgebraicGeometry.sourceLocalClosure, CategoryTheory.MorphismProperty.IsStableUnderBaseChange.mk', CategoryTheory.Limits.pullback.fst, Exists.intro, CategoryTheory.Precoverage.ZeroHypercover.pullback₁, _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.IsStableUnderBaseChange
refine :
  ∀ (X Y S : Scheme.{u}) (f : X ⟶ S) (g : Y ⟶ S) (x : HasPullback f g),
    sourceLocalClosure W P g →
      ∀ (𝒰 : Scheme.Cover (Scheme.precoverage W) Y) (hg : ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ g))
        (i :
          PreZeroHypercover.I₀ (S := pullback f g)
            (Precoverage.ZeroHypercover.toPreZeroHypercover
              (Precoverage.ZeroHypercover.pullback₁ (pullback.snd f g) 𝒰))),
        P
          (PreZeroHypercover.f
              (Precoverage.ZeroHypercover.toPreZeroHypercover
                (Precoverage.ZeroHypercover.pullback₁ (pullback.snd f g) 𝒰))
              i ≫
            pullback.fst f g)
⊢ (sourceLocalClosure W P).IsStableUnderBaseChange

Tactic:
refine .mk' fun X Y S f g _ ⟨𝒰, hg⟩ ↦ ⟨𝒰.pullback₁ (pullback.snd f g), 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.IsStableUnderBaseChange
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
h : HasPullback f g
h_1 : sourceLocalClosure W P g
𝒰 : Scheme.Cover (Scheme.precoverage W) Y
hg : ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ g)
i :
  PreZeroHypercover.I₀ (S := pullback f g)
    (Precoverage.ZeroHypercover.toPreZeroHypercover (Precoverage.ZeroHypercover.pullback₁ (pullback.snd f g) 𝒰))
⊢ P
    (PreZeroHypercover.f
        (Precoverage.ZeroHypercover.toPreZeroHypercover (Precoverage.ZeroHypercover.pullback₁ (pullback.snd f g) 𝒰)) i ≫
      pullback.fst f g)

Tactic:
simpa [← pullbackLeftPullbackSndIso_hom_fst, P.cancel_left_of_respectsIso] using
    P.pullback_fst _ _ (hg i)

Premises used: CategoryTheory.MorphismProperty.pullback_fst, CategoryTheory.Limits.pullbackLeftPullbackSndIso_hom_fst, CategoryTheory.MorphismProperty.cancel_left_of_respectsIso
-- Module: Mathlib.AlgebraicGeometry.Morphisms.LocalClosure
Goal:
W P Q : MorphismProperty Scheme
X Y : Scheme
inst : W.IsStableUnderBaseChange
inst_1 : Scheme.IsJointlySurjectivePreserving W
inst_2 : W.ContainsIdentities
inst_3 : P.ContainsIdentities
⊢ (sourceLocalClosure W P).ContainsIdentities

Tactic:
⟨fun X ↦ ⟨X.coverOfIsIso (𝟙 X), fun _ ↦ P.id_mem _⟩⟩

Premises used: AlgebraicGeometry.Scheme.coverOfIsIso, CategoryTheory.MorphismProperty.ContainsIdentities.mk, CategoryTheory.CategoryStruct.id, CategoryTheory.PreZeroHypercover.X, Exists.intro, CategoryTheory.MorphismProperty.id_mem, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.AlgebraicGeometry.Morphisms.LocalClosure
Goal:
W P Q : MorphismProperty Scheme
X Y : Scheme
inst : W.IsStableUnderBaseChange
inst_1 : Scheme.IsJointlySurjectivePreserving W
inst_2 : W.IsStableUnderComposition
inst_3 : P.IsStableUnderBaseChange
inst_4 : P.IsStableUnderComposition
⊢ (sourceLocalClosure W P).IsStableUnderComposition

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

Premises used: CategoryTheory.MorphismProperty.IsStableUnderComposition.mk, AlgebraicGeometry.sourceLocalClosure, CategoryTheory.CategoryStruct.comp, _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 : W.IsStableUnderComposition
inst_3 : P.IsStableUnderBaseChange
inst_4 : P.IsStableUnderComposition
refine :
  ∀ {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z),
    sourceLocalClosure W P f →
      sourceLocalClosure W P g →
        ∀ (𝒰 : Scheme.Cover (Scheme.precoverage W) X) (hf : ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ f))
          (𝒱 : Scheme.Cover (Scheme.precoverage W) Y) (hg : ∀ (i : 𝒱.I₀), P (𝒱.f i ≫ g)), sourceLocalClosure W P (f ≫ g)
⊢ (sourceLocalClosure W P).IsStableUnderComposition

Tactic:
refine ⟨fun {X Y Z} f g ⟨𝒰, hf⟩ ⟨𝒱, hg⟩ ↦ ?_⟩
-- 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 : W.IsStableUnderComposition
inst_3 : P.IsStableUnderBaseChange
inst_4 : P.IsStableUnderComposition
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
h : sourceLocalClosure W P f
h_1 : sourceLocalClosure W P g
𝒰 : Scheme.Cover (Scheme.precoverage W) X
hf : ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ f)
𝒱 : Scheme.Cover (Scheme.precoverage W) Y
hg : ∀ (i : 𝒱.I₀), P (𝒱.f i ≫ g)
⊢ sourceLocalClosure W P (f ≫ g)

Tactic:
⟨𝒰.bind fun i ↦ (𝒱.pullback₁ (𝒰.f i ≫ f)), fun ⟨l, r⟩ ↦ ?_⟩

Premises used: CategoryTheory.PreZeroHypercover.f, AlgebraicGeometry.sourceLocalClosure, Exists.intro, CategoryTheory.CategoryStruct.comp, CategoryTheory.Precoverage.ZeroHypercover.pullback₁, _private.0.AlgebraicGeometry.sourceLocalClosure.instIsStableUnderCompositionSchemeOfIsStableUnderBaseChange.match_1, CategoryTheory.Precoverage.ZeroHypercover.bind, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- 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 : W.IsStableUnderComposition
inst_3 : P.IsStableUnderBaseChange
inst_4 : P.IsStableUnderComposition
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
h : sourceLocalClosure W P f
h_1 : sourceLocalClosure W P g
𝒰 : Scheme.Cover (Scheme.precoverage W) X
hf : ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ f)
𝒱 : Scheme.Cover (Scheme.precoverage W) Y
hg : ∀ (i : 𝒱.I₀), P (𝒱.f i ≫ g)
refine :
  ∀ (x : (Precoverage.ZeroHypercover.bind 𝒰 fun (i : 𝒰.I₀) ↦ Precoverage.ZeroHypercover.pullback₁ (𝒰.f i ≫ f) 𝒱).I₀)
    (l : 𝒰.I₀)
    (r :
      PreZeroHypercover.I₀ (C := Scheme) (S := 𝒰.X l)
        ((fun (i : 𝒰.I₀) ↦
            (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage W)
                ((fun (i : 𝒰.I₀) ↦ Precoverage.ZeroHypercover.pullback₁ (𝒰.f i ≫ f) 𝒱) i) :
              PreZeroHypercover (𝒰.X i)))
          l)),
    P (X :=
      (Precoverage.ZeroHypercover.bind 𝒰 fun (i : 𝒰.I₀) ↦ Precoverage.ZeroHypercover.pullback₁ (𝒰.f i ≫ f) 𝒱).X
        (Sigma.mk (β := fun (i : 𝒰.I₀) ↦
          PreZeroHypercover.I₀ (C := Scheme) (S := 𝒰.X i)
            ((fun (i : 𝒰.I₀) ↦
                (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage W)
                    ((fun (i : 𝒰.I₀) ↦ Precoverage.ZeroHypercover.pullback₁ (𝒰.f i ≫ f) 𝒱) i) :
                  PreZeroHypercover (𝒰.X i)))
              i))
          l r))
      ((Precoverage.ZeroHypercover.bind 𝒰 fun (i : 𝒰.I₀) ↦ Precoverage.ZeroHypercover.pullback₁ (𝒰.f i ≫ f) 𝒱).f
          (Sigma.mk (β := fun (i : 𝒰.I₀) ↦
            PreZeroHypercover.I₀ (C := Scheme) (S := 𝒰.X i)
              ((fun (i : 𝒰.I₀) ↦
                  (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage W)
                      ((fun (i : 𝒰.I₀) ↦ Precoverage.ZeroHypercover.pullback₁ (𝒰.f i ≫ f) 𝒱) i) :
                    PreZeroHypercover (𝒰.X i)))
                i))
            l r) ≫
        f ≫ g)
⊢ sourceLocalClosure W P (f ≫ g)

Tactic:
refine ⟨𝒰.bind fun i ↦ (𝒱.pullback₁ (𝒰.f i ≫ f)), fun ⟨l, r⟩ ↦ ?_⟩
-- 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 : W.IsStableUnderComposition
inst_3 : P.IsStableUnderBaseChange
inst_4 : P.IsStableUnderComposition
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
h : sourceLocalClosure W P f
h_1 : sourceLocalClosure W P g
𝒰 : Scheme.Cover (Scheme.precoverage W) X
hf : ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ f)
𝒱 : Scheme.Cover (Scheme.precoverage W) Y
hg : ∀ (i : 𝒱.I₀), P (𝒱.f i ≫ g)
x : (Precoverage.ZeroHypercover.bind 𝒰 fun (i : 𝒰.I₀) ↦ Precoverage.ZeroHypercover.pullback₁ (𝒰.f i ≫ f) 𝒱).I₀
l : 𝒰.I₀
r :
  PreZeroHypercover.I₀ (C := Scheme) (S := 𝒰.X l)
    ((fun (i : 𝒰.I₀) ↦
        (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage W)
            ((fun (i : 𝒰.I₀) ↦ Precoverage.ZeroHypercover.pullback₁ (𝒰.f i ≫ f) 𝒱) i) :
          PreZeroHypercover (𝒰.X i)))
      l)
⊢ P (X :=
    (Precoverage.ZeroHypercover.bind 𝒰 fun (i : 𝒰.I₀) ↦ Precoverage.ZeroHypercover.pullback₁ (𝒰.f i ≫ f) 𝒱).X
      (Sigma.mk (β := fun (i : 𝒰.I₀) ↦
        PreZeroHypercover.I₀ (C := Scheme) (S := 𝒰.X i)
          ((fun (i : 𝒰.I₀) ↦
              (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage W)
                  ((fun (i : 𝒰.I₀) ↦ Precoverage.ZeroHypercover.pullback₁ (𝒰.f i ≫ f) 𝒱) i) :
                PreZeroHypercover (𝒰.X i)))
            i))
        l r))
    ((Precoverage.ZeroHypercover.bind 𝒰 fun (i : 𝒰.I₀) ↦ Precoverage.ZeroHypercover.pullback₁ (𝒰.f i ≫ f) 𝒱).f
        (Sigma.mk (β := fun (i : 𝒰.I₀) ↦
          PreZeroHypercover.I₀ (C := Scheme) (S := 𝒰.X i)
            ((fun (i : 𝒰.I₀) ↦
                (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage W)
                    ((fun (i : 𝒰.I₀) ↦ Precoverage.ZeroHypercover.pullback₁ (𝒰.f i ≫ f) 𝒱) i) :
                  PreZeroHypercover (𝒰.X i)))
              i))
          l r) ≫
      f ≫ g)

Tactic:
simpa [← pullbackRightPullbackFstIso_inv_snd_fst_assoc, pullback.condition_assoc] using
    P.comp_mem _ _ (P.pullback_snd _ _ (hf _)) (hg r)

Premises used: CategoryTheory.Limits.pullback.condition_assoc, CategoryTheory.MorphismProperty.comp_mem, CategoryTheory.Limits.pullbackRightPullbackFstIso_inv_snd_fst_assoc, CategoryTheory.MorphismProperty.pullback_snd
-- Module: Mathlib.AlgebraicGeometry.Morphisms.LocalFlatDescent
Goal:
⊢ DescendsAlong (@LocallyOfFiniteType) (@Surjective ⊓ @Flat ⊓ @QuasiCompact)

Tactic:
HasRingHomProperty.descendsAlong_flat RingHom.FiniteType.codescendsAlong_faithfullyFlat

Premises used: AlgebraicGeometry.HasRingHomProperty.descendsAlong_flat, RingHom.FiniteType.codescendsAlong_faithfullyFlat
-- Module: Mathlib.AlgebraicGeometry.Morphisms.LocalFlatDescent
Goal:
⊢ DescendsAlong (@LocallyOfFinitePresentation) (@Surjective ⊓ @Flat ⊓ @QuasiCompact)

Tactic:
HasRingHomProperty.descendsAlong_flat RingHom.FinitePresentation.codescendsAlong_faithfullyFlat

Premises used: AlgebraicGeometry.HasRingHomProperty.descendsAlong_flat, RingHom.FinitePresentation.codescendsAlong_faithfullyFlat
-- Module: Mathlib.AlgebraicGeometry.Morphisms.LocalFlatDescent
Goal:
⊢ DescendsAlong (@Smooth) (@Surjective ⊓ @Flat ⊓ @QuasiCompact)

Tactic:
HasRingHomProperty.descendsAlong_flat RingHom.Smooth.codescendsAlong_faithfullyFlat

Premises used: AlgebraicGeometry.HasRingHomProperty.descendsAlong_flat, RingHom.Smooth.codescendsAlong_faithfullyFlat
-- Module: Mathlib.AlgebraicGeometry.Morphisms.LocalFlatDescent
Goal:
⊢ DescendsAlong (@FormallyUnramified) (@Surjective ⊓ @Flat ⊓ @QuasiCompact)

Tactic:
HasRingHomProperty.descendsAlong_flat RingHom.FormallyUnramified.codescendsAlong_faithfullyFlat

Premises used: AlgebraicGeometry.HasRingHomProperty.descendsAlong_flat, RingHom.FormallyUnramified.codescendsAlong_faithfullyFlat
-- Module: Mathlib.AlgebraicGeometry.Morphisms.LocalFlatDescent
Goal:
⊢ DescendsAlong (@Etale) (@Surjective ⊓ @Flat ⊓ @QuasiCompact)

Tactic:
HasRingHomProperty.descendsAlong_flat RingHom.Etale.codescendsAlong_faithfullyFlat

Premises used: AlgebraicGeometry.HasRingHomProperty.descendsAlong_flat, RingHom.Etale.codescendsAlong_faithfullyFlat
-- Module: Mathlib.AlgebraicGeometry.Morphisms.LocalIso
Goal:
h : ∀ (x x_1 : Scheme.{u_1}) (x_2 : x ⟶ x_1), IsLocalIso x_2 ↔ sourceLocalClosure IsOpenImmersion IsOpenImmersion x_2
⊢ @IsLocalIso = sourceLocalClosure IsOpenImmersion IsOpenImmersion

Tactic:
ext
-- Module: Mathlib.AlgebraicGeometry.Morphisms.LocalIso
Goal:
x x_1 : Scheme
x_2 : x ⟶ x_1
h :
  (∀ (x_3 : ↥x), ∃ (U : x.Opens), x_3 ∈ U ∧ IsOpenImmersion (U.ι ≫ x_2)) ↔
    sourceLocalClosure IsOpenImmersion IsOpenImmersion x_2
h₁ h₂ :
  (∀ (x_3 : ↥x), ∃ (U : x.Opens), x_3 ∈ U ∧ IsOpenImmersion (U.ι ≫ x_2)) ↔
    ∀ (x_3 : ↥x), ∃ (U : x.Opens), x_3 ∈ U ∧ IsOpenImmersion (U.ι ≫ x_2)
⊢ IsLocalIso x_2 ↔ sourceLocalClosure IsOpenImmersion IsOpenImmersion x_2

Tactic:
rw [isLocalIso_iff, sourceLocalClosure.iff_forall_exists]

Premises used: AlgebraicGeometry.sourceLocalClosure.iff_forall_exists, AlgebraicGeometry.isLocalIso_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.LocalIso
Goal:
X Y : Scheme
f : X ⟶ Y
rw : IsZariskiLocalAtSource.{u_1} (sourceLocalClosure IsOpenImmersion IsOpenImmersion)
⊢ IsZariskiLocalAtSource @IsLocalIso

Tactic:
rw [eq_sourceLocalClosure_isOpenImmersion]

Premises used: AlgebraicGeometry.IsLocalIso.eq_sourceLocalClosure_isOpenImmersion
-- Module: Mathlib.AlgebraicGeometry.Morphisms.LocalIso
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ IsZariskiLocalAtSource.{u_1} (sourceLocalClosure IsOpenImmersion IsOpenImmersion)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.LocalIso
Goal:
X Y : Scheme
f : X ⟶ Y
rw : (sourceLocalClosure IsOpenImmersion IsOpenImmersion).IsMultiplicative
⊢ IsMultiplicative @IsLocalIso

Tactic:
rw [eq_sourceLocalClosure_isOpenImmersion]

Premises used: AlgebraicGeometry.IsLocalIso.eq_sourceLocalClosure_isOpenImmersion
-- Module: Mathlib.AlgebraicGeometry.Morphisms.LocalIso
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ (sourceLocalClosure IsOpenImmersion IsOpenImmersion).IsMultiplicative

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.LocalIso
Goal:
X Y : Scheme
f : X ⟶ Y
rw : (sourceLocalClosure IsOpenImmersion IsOpenImmersion).IsStableUnderBaseChange
⊢ IsStableUnderBaseChange @IsLocalIso

Tactic:
rw [eq_sourceLocalClosure_isOpenImmersion]

Premises used: AlgebraicGeometry.IsLocalIso.eq_sourceLocalClosure_isOpenImmersion
-- Module: Mathlib.AlgebraicGeometry.Morphisms.LocalIso
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ (sourceLocalClosure IsOpenImmersion IsOpenImmersion).IsStableUnderBaseChange

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.LocalIso
Goal:
P : MorphismProperty Scheme
inst : P.ContainsIdentities
inst_1 : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
hf : IsLocalIso f
obtain :
  ∀ (𝒰 : Scheme.Cover (Scheme.precoverage IsOpenImmersion) X) (h : ∀ (i : 𝒰.I₀), IsOpenImmersion (𝒰.f i ≫ f)), P f
⊢ P f

Tactic:
obtain ⟨𝒰, h⟩ := eq_sourceLocalClosure_isOpenImmersion ▸ hf
-- Module: Mathlib.AlgebraicGeometry.Morphisms.LocalIso
Goal:
P : MorphismProperty Scheme
inst : P.ContainsIdentities
inst_1 : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
hf : IsLocalIso f
𝒰 : Scheme.Cover (Scheme.precoverage IsOpenImmersion) X
h : ∀ (i : 𝒰.I₀), IsOpenImmersion (𝒰.f i ≫ f)
rw : ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ f)
⊢ P f

Tactic:
rw [IsZariskiLocalAtSource.iff_of_openCover 𝒰 (P := P)]

Premises used: AlgebraicGeometry.IsZariskiLocalAtSource.iff_of_openCover
-- Module: Mathlib.AlgebraicGeometry.Morphisms.LocalIso
Goal:
P : MorphismProperty Scheme
inst : P.ContainsIdentities
inst_1 : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
hf : IsLocalIso f
𝒰 : Scheme.Cover (Scheme.precoverage IsOpenImmersion) X
h : ∀ (i : 𝒰.I₀), IsOpenImmersion (𝒰.f i ≫ f)
⊢ ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ f)

Tactic:
fun _ ↦ IsZariskiLocalAtSource.of_isOpenImmersion _

Premises used: CategoryTheory.PreZeroHypercover.f, CategoryTheory.CategoryStruct.comp, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover, AlgebraicGeometry.IsZariskiLocalAtSource.of_isOpenImmersion
-- Module: Mathlib.AlgebraicGeometry.Morphisms.LocalIso
Goal:
P : MorphismProperty Scheme
inst : P.ContainsIdentities
inst_1 : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
hf : IsLocalIso f
𝒰 : Scheme.Cover (Scheme.precoverage IsOpenImmersion) X
h : ∀ (i : 𝒰.I₀), IsOpenImmersion (𝒰.f i ≫ f)
⊢ ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ f)

Tactic:
exact fun _ ↦ IsZariskiLocalAtSource.of_isOpenImmersion _

Premises used: AlgebraicGeometry.IsZariskiLocalAtSource.of_isOpenImmersion
-- Module: Mathlib.AlgebraicGeometry.Morphisms.LocalIso
Goal:
⊢ @IsLocalIso = ⨅ (P : MorphismProperty Scheme), ⨅ (_ : P.ContainsIdentities), ⨅ (_ : IsZariskiLocalAtSource P), P

Tactic:
le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.AlgebraicGeometry.Morphisms.LocalIso
Goal:
refine_1 :
  ∀ (i : MorphismProperty Scheme) (i_1 : i.ContainsIdentities) (i_2 : IsZariskiLocalAtSource i), @IsLocalIso ≤ i
⊢ @IsLocalIso ≤ ⨅ (P : MorphismProperty Scheme), ⨅ (_ : P.ContainsIdentities), ⨅ (_ : IsZariskiLocalAtSource P), P

Tactic:
simp only [le_iInf_iff]

Premises used: le_iInf_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.LocalIso
Goal:
⊢ ∀ (i : MorphismProperty Scheme) (i_1 : i.ContainsIdentities) (i_2 : IsZariskiLocalAtSource i), @IsLocalIso ≤ i

Tactic:
apply le_of_isZariskiLocalAtSource

Premises used: AlgebraicGeometry.IsLocalIso.le_of_isZariskiLocalAtSource
-- Module: Mathlib.AlgebraicGeometry.Morphisms.LocalIso
Goal:
⊢ ⨅ (P : MorphismProperty Scheme), ⨅ (_ : P.ContainsIdentities), ⨅ (_ : IsZariskiLocalAtSource P), P ≤ @IsLocalIso

Tactic:
iInf_le_of_le @IsLocalIso (iInf_le_of_le inferInstance (iInf_le _ ?_))

Premises used: CategoryTheory.MorphismProperty, AlgebraicGeometry.IsLocalIso, inferInstance, iInf_le_of_le, iInf_le
-- Module: Mathlib.AlgebraicGeometry.Morphisms.LocalIso
Goal:
refine_2 : IsZariskiLocalAtSource @IsLocalIso
⊢ ⨅ (P : MorphismProperty Scheme), ⨅ (_ : P.ContainsIdentities), ⨅ (_ : IsZariskiLocalAtSource P), P ≤ @IsLocalIso

Tactic:
refine iInf_le_of_le @IsLocalIso (iInf_le_of_le inferInstance (iInf_le _ ?_))
-- Module: Mathlib.AlgebraicGeometry.Morphisms.LocalIso
Goal:
⊢ IsZariskiLocalAtSource @IsLocalIso

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion
Goal:
R S : CommRingCat
f : R ⟶ S
hf :
  Function.Surjective (α := (↑R : Type u_1)) (β := (↑S : Type u_1))
    (⇑(CommRingCat.Hom.hom f) : (a : (↑R : Type u_1)) → (↑S : Type u_1))
mp :
  IsOpenImmersion (Spec.map f) →
    ∃ (e : (↑R : Type u_1)),
      IsIdempotentElem e ∧ Eq (α := Ideal (↑R : Type u_1)) (RingHom.ker (CommRingCat.Hom.hom f)) (Ideal.span {e})
mpr :
  (∃ (e : (↑R : Type u_1)),
      IsIdempotentElem e ∧ Eq (α := Ideal (↑R : Type u_1)) (RingHom.ker (CommRingCat.Hom.hom f)) (Ideal.span {e})) →
    IsOpenImmersion (Spec.map f)
⊢ IsOpenImmersion (Spec.map f) ↔
    ∃ (e : (↑R : Type u_1)),
      IsIdempotentElem e ∧ Eq (α := Ideal (↑R : Type u_1)) (RingHom.ker (CommRingCat.Hom.hom f)) (Ideal.span {e})

Tactic:
constructor