awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
Goal:
R S : CommRingCat
φ : R ⟶ S
h : (@Surjective ⊓ @Flat) (Spec.map φ)
T : CommRingCat
this : IsAffine.{u} (Spec T)
ψ : R ⟶ T
hfst : IsIso (X := pullback (Spec.map φ) (Spec.map ψ)) (pullback.fst (Spec.map φ) (Spec.map ψ))
R_1 S_1 : CommRingCat
f : R_1 ⟶ S_1
hf : (@Surjective ⊓ @Flat) (Spec.map f)
refine_1 : Flat (Spec.map f) ∧ Surjective (Spec.map f)
refine_1₁ refine_1₂ refine_1₃ refine_1₄ : Surjective (Spec.map f) ∧ Flat (Spec.map f)
⊢ (CommRingCat.Hom.hom f).FaithfullyFlat

Tactic:
rwa [← flat_and_surjective_SpecMap_iff, and_comm]

Premises used: and_comm, AlgebraicGeometry.flat_and_surjective_SpecMap_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
Goal:
R S : CommRingCat
φ : R ⟶ S
h : (@Surjective ⊓ @Flat) (Spec.map φ)
T : CommRingCat
this : IsAffine.{u} (Spec T)
ψ : R ⟶ T
hfst : IsIso (X := pullback (Spec.map φ) (Spec.map ψ)) (pullback.fst (Spec.map φ) (Spec.map ψ))
refine_2 refine_2₁ :
  ∀ {R S : CommRingCat.{u}} {f : R ⟶ S},
    isomorphisms Scheme (Spec.map f) ↔
      Function.Bijective (α := (↑R : Type u)) (β := (↑S : Type u))
        (⇑(CommRingCat.Hom.hom f) : (a : (↑R : Type u)) → (↑S : Type u))
refine_2₂ : ∀ {R S : CommRingCat.{u}} {f : R ⟶ S}, True
⊢ ∀ {R S : CommRingCat.{u}} {f : R ⟶ S},
    isomorphisms Scheme (Spec.map f) ↔
      (fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦
          Function.Bijective (α := R) (β := S) (⇑f : (a : R) → S))
        (CommRingCat.Hom.hom f)

Tactic:
simp_rw [← isIso_SpecMap_iff, implies_true]

Premises used: AlgebraicGeometry.isIso_SpecMap_iff, implies_true
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
Goal:
H :
  ∀ {X Y Z : Scheme.{u_1}} {f : X ⟶ Z} {g : Y ⟶ Z} [inst : HasPullback f g],
    (@Surjective ⊓ @Flat ⊓ @QuasiCompact) f → IsOpenImmersion (X := pullback f g) (pullback.fst f g) → IsOpenImmersion g
⊢ IsOpenImmersion.DescendsAlong (@Surjective ⊓ @Flat ⊓ @QuasiCompact)

Tactic:
apply DescendsAlong.mk'

Premises used: CategoryTheory.MorphismProperty.DescendsAlong.mk'
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H :
  ∀ [inst : HasPullback f g],
    (@Surjective ⊓ @Flat ⊓ @QuasiCompact) f → IsOpenImmersion (X := pullback f g) (pullback.fst f g) → IsOpenImmersion g
⊢ ∀ [inst : HasPullback f g],
    (@Surjective ⊓ @Flat ⊓ @QuasiCompact) f → IsOpenImmersion (X := pullback f g) (pullback.fst f g) → IsOpenImmersion g

Tactic:
_
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst : HasPullback f g
hf : (@Surjective ⊓ @Flat ⊓ @QuasiCompact) f
hg : IsOpenImmersion (X := pullback f g) (pullback.fst f g)
⊢ UniversallyOpen g

Tactic:
have : UniversallyOpen g :=
    MorphismProperty.of_pullback_fst_of_descendsAlong
      (P := @UniversallyOpen) (Q := @Surjective ⊓ @Flat ⊓ @QuasiCompact) (f := f)
      hf inferInstance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst : HasPullback f g
hf : (@Surjective ⊓ @Flat ⊓ @QuasiCompact) f
hg : IsOpenImmersion (X := pullback f g) (pullback.fst f g)
this : UniversallyOpen g
U : Z.Opens := { carrier := Set.range (ι := ↥Y) ⇑g, is_open' := ⋯ }
f' : pullback f U.ι ⟶ (↑U : Scheme) := pullback.snd f U.ι
⊢ Subset (α := Set ↥Z) (Set.range (ι := ↥Y) ⇑g) (Set.range (ι := ↥(↑U : Scheme)) ⇑U.ι)

Tactic:
simp [U]
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst : HasPullback f g
hf : (@Surjective ⊓ @Flat ⊓ @QuasiCompact) f
hg : IsOpenImmersion (X := pullback f g) (pullback.fst f g)
this : UniversallyOpen g
U : Z.Opens := { carrier := Set.range (ι := ↥Y) ⇑g, is_open' := ⋯ }
f' : pullback f U.ι ⟶ (↑U : Scheme) := pullback.snd f U.ι
g' : Y ⟶ (↑U : Scheme) := IsOpenImmersion.lift U.ι g ⋯
x_1 : ↥(↑U : Scheme)
x : ↥Z
y : ↥Y
hy : g y = x
a : Eq (α := ↥Z) (U.ι (g' y : ↥(↑U : Scheme)) : ↥Z) (U.ι (Subtype.mk (p := fun (x : ↥Z) ↦ x ∈ U) x ⋯) : ↥Z)
⊢ Eq (α := ↥(↑U : Scheme)) (g' y : ↥(↑U : Scheme)) (Subtype.mk (p := fun (x : ↥Z) ↦ x ∈ U) x ⋯ : ↥U)

Tactic:
apply U.ι.injective

Premises used: AlgebraicGeometry.Scheme.Hom.injective, AlgebraicGeometry.Scheme.Opens.ι
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst : HasPullback f g
hf : (@Surjective ⊓ @Flat ⊓ @QuasiCompact) f
hg : IsOpenImmersion (X := pullback f g) (pullback.fst f g)
this : UniversallyOpen g
U : Z.Opens := { carrier := Set.range (ι := ↥Y) ⇑g, is_open' := ⋯ }
f' : pullback f U.ι ⟶ (↑U : Scheme) := pullback.snd f U.ι
g' : Y ⟶ (↑U : Scheme) := IsOpenImmersion.lift U.ι g ⋯
x_1 : ↥(↑U : Scheme)
x : ↥Z
y : ↥Y
hy : g y = x
⊢ Eq (α := ↥Z) (U.ι (g' y : ↥(↑U : Scheme)) : ↥Z) (U.ι (Subtype.mk (p := fun (x : ↥Z) ↦ x ∈ U) x ⋯) : ↥Z)

Tactic:
simp [← Scheme.Hom.comp_apply, g', hy]

Premises used: AlgebraicGeometry.Scheme.Hom.comp_apply
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst : HasPullback f g
hf : (@Surjective ⊓ @Flat ⊓ @QuasiCompact) f
hg : IsOpenImmersion (X := pullback f g) (pullback.fst f g)
this : UniversallyOpen g
U : Z.Opens := { carrier := Set.range (ι := ↥Y) ⇑g, is_open' := ⋯ }
f' : pullback f U.ι ⟶ (↑U : Scheme) := pullback.snd f U.ι
g' : Y ⟶ (↑U : Scheme) := IsOpenImmersion.lift U.ι g ⋯
⊢ Surjective g'

Tactic:
have : Surjective g' := ⟨fun ⟨x, ⟨y, hy⟩⟩ ↦
    ⟨y, by apply U.ι.injective; simp [← Scheme.Hom.comp_apply, g', hy]⟩⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst : HasPullback f g
hf : (@Surjective ⊓ @Flat ⊓ @QuasiCompact) f
hg : IsOpenImmersion (X := pullback f g) (pullback.fst f g)
this_1 : UniversallyOpen g
U : Z.Opens := { carrier := Set.range (ι := ↥Y) ⇑g, is_open' := ⋯ }
f' : pullback f U.ι ⟶ (↑U : Scheme) := pullback.snd f U.ι
g' : Y ⟶ (↑U : Scheme) := IsOpenImmersion.lift U.ι g ⋯
this : Surjective g'
rw : IsOpenImmersion (X := pullback f' g') (pullback.fst f' g') ∧ Surjective (X := pullback f' g') (pullback.fst f' g')
⊢ IsIso (X := pullback f' g') (pullback.fst f' g')

Tactic:
rw [isIso_iff_isOpenImmersion_and_surjective]

Premises used: AlgebraicGeometry.isIso_iff_isOpenImmersion_and_surjective
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst : HasPullback f g
hf : (@Surjective ⊓ @Flat ⊓ @QuasiCompact) f
hg : IsOpenImmersion (X := pullback f g) (pullback.fst f g)
this_1 : UniversallyOpen g
U : Z.Opens := { carrier := Set.range (ι := ↥Y) ⇑g, is_open' := ⋯ }
f' : pullback f U.ι ⟶ (↑U : Scheme) := pullback.snd f U.ι
g' : Y ⟶ (↑U : Scheme) := IsOpenImmersion.lift U.ι g ⋯
this : Surjective g'
⊢ IsOpenImmersion (X := pullback f' g') (pullback.fst f' g') ∧ Surjective (X := pullback f' g') (pullback.fst f' g')

Tactic:
⟨?_, inferInstance⟩

Premises used: inferInstance, And.intro
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst : HasPullback f g
hf : (@Surjective ⊓ @Flat ⊓ @QuasiCompact) f
hg : IsOpenImmersion (X := pullback f g) (pullback.fst f g)
this_1 : UniversallyOpen g
U : Z.Opens := { carrier := Set.range (ι := ↥Y) ⇑g, is_open' := ⋯ }
f' : pullback f U.ι ⟶ (↑U : Scheme) := pullback.snd f U.ι
g' : Y ⟶ (↑U : Scheme) := IsOpenImmersion.lift U.ι g ⋯
this : Surjective g'
refine : IsOpenImmersion (X := pullback f' g') (pullback.fst f' g')
⊢ IsOpenImmersion (X := pullback f' g') (pullback.fst f' g') ∧ Surjective (X := pullback f' g') (pullback.fst f' g')

Tactic:
refine ⟨?_, inferInstance⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst : HasPullback f g
hf : (@Surjective ⊓ @Flat ⊓ @QuasiCompact) f
hg : IsOpenImmersion (X := pullback f g) (pullback.fst f g)
this_1 : UniversallyOpen g
U : Z.Opens := { carrier := Set.range (ι := ↥Y) ⇑g, is_open' := ⋯ }
f' : pullback f U.ι ⟶ (↑U : Scheme) := pullback.snd f U.ι
g' : Y ⟶ (↑U : Scheme) := IsOpenImmersion.lift U.ι g ⋯
this : Surjective g'
rwa rwa₁ rwa₂ rwa₃ : IsOpenImmersion (X := pullback f g) (pullback.fst f g)
⊢ IsOpenImmersion (X := pullback f (g' ≫ U.ι)) (pullback.fst f (g' ≫ U.ι))

Tactic:
rwa [AlgebraicGeometry.IsOpenImmersion.lift_fac]

Premises used: AlgebraicGeometry.IsOpenImmersion.lift_fac
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst : HasPullback f g
hf : (@Surjective ⊓ @Flat ⊓ @QuasiCompact) f
hg : IsOpenImmersion (X := pullback f g) (pullback.fst f g)
this_1 : UniversallyOpen g
U : Z.Opens := { carrier := Set.range (ι := ↥Y) ⇑g, is_open' := ⋯ }
f' : pullback f U.ι ⟶ (↑U : Scheme) := pullback.snd f U.ι
g' : Y ⟶ (↑U : Scheme) := IsOpenImmersion.lift U.ι g ⋯
this : Surjective g'
⊢ IsOpenImmersion (X := pullback f (g' ≫ U.ι)) (pullback.fst f (g' ≫ U.ι))

Tactic:
have : IsOpenImmersion (pullback.fst f (g' ≫ U.ι)) := by
      rwa [AlgebraicGeometry.IsOpenImmersion.lift_fac]
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst : HasPullback f g
hf : (@Surjective ⊓ @Flat ⊓ @QuasiCompact) f
hg : IsOpenImmersion (X := pullback f g) (pullback.fst f g)
this_1 : UniversallyOpen g
U : Z.Opens := { carrier := Set.range (ι := ↥Y) ⇑g, is_open' := ⋯ }
f' : pullback f U.ι ⟶ (↑U : Scheme) := pullback.snd f U.ι
g' : Y ⟶ (↑U : Scheme) := IsOpenImmersion.lift U.ι g ⋯
this_2 : Surjective g'
this : IsOpenImmersion (X := pullback f (g' ≫ U.ι)) (pullback.fst f (g' ≫ U.ι))
rw : IsOpenImmersion (X := pullback f' g') (Iso.hom (pullbackLeftPullbackSndIso f U.ι g') ≫ pullback.fst f (g' ≫ U.ι))
⊢ IsOpenImmersion (X := pullback f' g') (pullback.fst f' g' ≫ pullback.fst f U.ι)

Tactic:
rw [← pullbackLeftPullbackSndIso_hom_fst]

Premises used: CategoryTheory.Limits.pullbackLeftPullbackSndIso_hom_fst
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst : HasPullback f g
hf : (@Surjective ⊓ @Flat ⊓ @QuasiCompact) f
hg : IsOpenImmersion (X := pullback f g) (pullback.fst f g)
this_1 : UniversallyOpen g
U : Z.Opens := { carrier := Set.range (ι := ↥Y) ⇑g, is_open' := ⋯ }
f' : pullback f U.ι ⟶ (↑U : Scheme) := pullback.snd f U.ι
g' : Y ⟶ (↑U : Scheme) := IsOpenImmersion.lift U.ι g ⋯
this_2 : Surjective g'
this : IsOpenImmersion (X := pullback f (g' ≫ U.ι)) (pullback.fst f (g' ≫ U.ι))
⊢ IsOpenImmersion (X := pullback f' g') (Iso.hom (pullbackLeftPullbackSndIso f U.ι g') ≫ pullback.fst f (g' ≫ U.ι))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst : HasPullback f g
hf : (@Surjective ⊓ @Flat ⊓ @QuasiCompact) f
hg : IsOpenImmersion (X := pullback f g) (pullback.fst f g)
this_1 : UniversallyOpen g
U : Z.Opens := { carrier := Set.range (ι := ↥Y) ⇑g, is_open' := ⋯ }
f' : pullback f U.ι ⟶ (↑U : Scheme) := pullback.snd f U.ι
g' : Y ⟶ (↑U : Scheme) := IsOpenImmersion.lift U.ι g ⋯
this_2 : Surjective g'
this : IsOpenImmersion (X := pullback f (g' ≫ U.ι)) (pullback.fst f (g' ≫ U.ι))
⊢ IsOpenImmersion (X := pullback f' g') (pullback.fst f' g' ≫ pullback.fst f U.ι)

Tactic:
have : IsOpenImmersion (pullback.fst f' g' ≫ pullback.fst f U.ι) := by
      rw [← pullbackLeftPullbackSndIso_hom_fst]
      infer_instance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst : HasPullback f g
hf : (@Surjective ⊓ @Flat ⊓ @QuasiCompact) f
hg : IsOpenImmersion (X := pullback f g) (pullback.fst f g)
this_1 : UniversallyOpen g
U : Z.Opens := { carrier := Set.range (ι := ↥Y) ⇑g, is_open' := ⋯ }
f' : pullback f U.ι ⟶ (↑U : Scheme) := pullback.snd f U.ι
g' : Y ⟶ (↑U : Scheme) := IsOpenImmersion.lift U.ι g ⋯
this_2 : Surjective g'
this_3 : IsOpenImmersion (X := pullback f (g' ≫ U.ι)) (pullback.fst f (g' ≫ U.ι))
this : IsOpenImmersion (X := pullback f' g') (pullback.fst f' g' ≫ pullback.fst f U.ι)
⊢ IsOpenImmersion (X := pullback f' g') (pullback.fst f' g')

Tactic:
.of_comp _ (pullback.fst _ _)

Premises used: CategoryTheory.Limits.pullback.fst, AlgebraicGeometry.IsOpenImmersion.of_comp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst : HasPullback f g
hf : (@Surjective ⊓ @Flat ⊓ @QuasiCompact) f
hg : IsOpenImmersion (X := pullback f g) (pullback.fst f g)
this_1 : UniversallyOpen g
U : Z.Opens := { carrier := Set.range (ι := ↥Y) ⇑g, is_open' := ⋯ }
f' : pullback f U.ι ⟶ (↑U : Scheme) := pullback.snd f U.ι
g' : Y ⟶ (↑U : Scheme) := IsOpenImmersion.lift U.ι g ⋯
this_2 : Surjective g'
this_3 : IsOpenImmersion (X := pullback f (g' ≫ U.ι)) (pullback.fst f (g' ≫ U.ι))
this : IsOpenImmersion (X := pullback f' g') (pullback.fst f' g' ≫ pullback.fst f U.ι)
⊢ IsOpenImmersion (X := pullback f' g') (pullback.fst f' g')

Tactic:
exact .of_comp _ (pullback.fst _ _)
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst : HasPullback f g
hf : (@Surjective ⊓ @Flat ⊓ @QuasiCompact) f
hg : IsOpenImmersion (X := pullback f g) (pullback.fst f g)
this_1 : UniversallyOpen g
U : Z.Opens := { carrier := Set.range (ι := ↥Y) ⇑g, is_open' := ⋯ }
f' : pullback f U.ι ⟶ (↑U : Scheme) := pullback.snd f U.ι
g' : Y ⟶ (↑U : Scheme) := IsOpenImmersion.lift U.ι g ⋯
this : Surjective g'
⊢ IsIso (X := pullback f' g') (pullback.fst f' g')

Tactic:
have : IsIso (pullback.fst f' g') := by
    rw [isIso_iff_isOpenImmersion_and_surjective]
    refine ⟨?_, inferInstance⟩
    have : IsOpenImmersion (pullback.fst f (g' ≫ U.ι)) := by
      rwa [AlgebraicGeometry.IsOpenImmersion.lift_fac]
    have : IsOpenImmersion (pullback.fst f' g' ≫ pullback.fst f U.ι) := by
      rw [← pullbackLeftPullbackSndIso_hom_fst]
      infer_instance
    exact .of_comp _ (pullback.fst _ _)
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst : HasPullback f g
hf : (@Surjective ⊓ @Flat ⊓ @QuasiCompact) f
hg : IsOpenImmersion (X := pullback f g) (pullback.fst f g)
this_1 : UniversallyOpen g
U : Z.Opens := { carrier := Set.range (ι := ↥Y) ⇑g, is_open' := ⋯ }
f' : pullback f U.ι ⟶ (↑U : Scheme) := pullback.snd f U.ι
g' : Y ⟶ (↑U : Scheme) := IsOpenImmersion.lift U.ι g ⋯
this_2 : Surjective g'
this : IsIso (X := pullback f' g') (pullback.fst f' g')
apply : (@Surjective ⊓ @Flat ⊓ @QuasiCompact) f'
⊢ IsIso g'

Tactic:
apply MorphismProperty.of_pullback_fst_of_descendsAlong
      (P := isomorphisms Scheme) (Q := @Surjective ⊓ @Flat ⊓ @QuasiCompact) (f := f') ?_ this

Premises used: CategoryTheory.MorphismProperty.of_pullback_fst_of_descendsAlong
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst : HasPullback f g
hf : (@Surjective ⊓ @Flat ⊓ @QuasiCompact) f
hg : IsOpenImmersion (X := pullback f g) (pullback.fst f g)
this_1 : UniversallyOpen g
U : Z.Opens := { carrier := Set.range (ι := ↥Y) ⇑g, is_open' := ⋯ }
f' : pullback f U.ι ⟶ (↑U : Scheme) := pullback.snd f U.ι
g' : Y ⟶ (↑U : Scheme) := IsOpenImmersion.lift U.ι g ⋯
this_2 : Surjective g'
this : IsIso (X := pullback f' g') (pullback.fst f' g')
⊢ (@Surjective ⊓ @Flat ⊓ @QuasiCompact) f'

Tactic:
MorphismProperty.pullback_snd _ _ hf

Premises used: CategoryTheory.MorphismProperty.pullback_snd
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst : HasPullback f g
hf : (@Surjective ⊓ @Flat ⊓ @QuasiCompact) f
hg : IsOpenImmersion (X := pullback f g) (pullback.fst f g)
this_1 : UniversallyOpen g
U : Z.Opens := { carrier := Set.range (ι := ↥Y) ⇑g, is_open' := ⋯ }
f' : pullback f U.ι ⟶ (↑U : Scheme) := pullback.snd f U.ι
g' : Y ⟶ (↑U : Scheme) := IsOpenImmersion.lift U.ι g ⋯
this_2 : Surjective g'
this : IsIso (X := pullback f' g') (pullback.fst f' g')
⊢ (@Surjective ⊓ @Flat ⊓ @QuasiCompact) f'

Tactic:
exact MorphismProperty.pullback_snd _ _ hf

Premises used: CategoryTheory.MorphismProperty.pullback_snd
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst : HasPullback f g
hf : (@Surjective ⊓ @Flat ⊓ @QuasiCompact) f
hg : IsOpenImmersion (X := pullback f g) (pullback.fst f g)
this_1 : UniversallyOpen g
U : Z.Opens := { carrier := Set.range (ι := ↥Y) ⇑g, is_open' := ⋯ }
f' : pullback f U.ι ⟶ (↑U : Scheme) := pullback.snd f U.ι
g' : Y ⟶ (↑U : Scheme) := IsOpenImmersion.lift U.ι g ⋯
this_2 : Surjective g'
this : IsIso (X := pullback f' g') (pullback.fst f' g')
⊢ IsIso g'

Tactic:
have : IsIso g' := by
    apply MorphismProperty.of_pullback_fst_of_descendsAlong
      (P := isomorphisms Scheme) (Q := @Surjective ⊓ @Flat ⊓ @QuasiCompact) (f := f') ?_ this
    exact MorphismProperty.pullback_snd _ _ hf
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst : HasPullback f g
hf : (@Surjective ⊓ @Flat ⊓ @QuasiCompact) f
hg : IsOpenImmersion (X := pullback f g) (pullback.fst f g)
this_1 : UniversallyOpen g
U : Z.Opens := { carrier := Set.range (ι := ↥Y) ⇑g, is_open' := ⋯ }
f' : pullback f U.ι ⟶ (↑U : Scheme) := pullback.snd f U.ι
g' : Y ⟶ (↑U : Scheme) := IsOpenImmersion.lift U.ι g ⋯
this_2 : Surjective g'
this_3 : IsIso (X := pullback f' g') (pullback.fst f' g')
this : IsIso g'
⊢ Subset (α := Set ↥Z) (Set.range (ι := ↥Y) ⇑g) (Set.range (ι := ↥(↑U : Scheme)) ⇑U.ι)

Tactic:
simp [U]
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst : HasPullback f g
hf : (@Surjective ⊓ @Flat ⊓ @QuasiCompact) f
hg : IsOpenImmersion (X := pullback f g) (pullback.fst f g)
this_1 : UniversallyOpen g
U : Z.Opens := { carrier := Set.range (ι := ↥Y) ⇑g, is_open' := ⋯ }
f' : pullback f U.ι ⟶ (↑U : Scheme) := pullback.snd f U.ι
g' : Y ⟶ (↑U : Scheme) := IsOpenImmersion.lift U.ι g ⋯
this_2 : Surjective g'
this_3 : IsIso (X := pullback f' g') (pullback.fst f' g')
this : IsIso g'
H : IsOpenImmersion (IsOpenImmersion.lift U.ι g ⋯ ≫ U.ι)
⊢ IsOpenImmersion g

Tactic:
rw [← IsOpenImmersion.lift_fac U.ι g (by simp [U])]

Premises used: AlgebraicGeometry.Scheme.Opens.ι, AlgebraicGeometry.IsOpenImmersion.lift_fac
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst : HasPullback f g
hf : (@Surjective ⊓ @Flat ⊓ @QuasiCompact) f
hg : IsOpenImmersion (X := pullback f g) (pullback.fst f g)
this_1 : UniversallyOpen g
U : Z.Opens := { carrier := Set.range (ι := ↥Y) ⇑g, is_open' := ⋯ }
f' : pullback f U.ι ⟶ (↑U : Scheme) := pullback.snd f U.ι
g' : Y ⟶ (↑U : Scheme) := IsOpenImmersion.lift U.ι g ⋯
this_2 : Surjective g'
this_3 : IsIso (X := pullback f' g') (pullback.fst f' g')
this : IsIso g'
⊢ IsOpenImmersion (IsOpenImmersion.lift U.ι g ⋯ ≫ U.ι)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
Goal:
P : MorphismProperty Scheme
inst : P.IsStableUnderBaseChange
Q : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
inst_1 : HasRingHomProperty P fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
h :
  RingHom.CodescendsAlong.{u} (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    fun {R S : Type u} [CommRing R] [CommRing S] ↦ RingHom.FaithfullyFlat
⊢ P.DescendsAlong (@Surjective ⊓ @Flat ⊓ @QuasiCompact)

Tactic:
HasRingHomProperty.descendsAlong _ _ _ _ ?_ ?_ h

Premises used: AlgebraicGeometry.HasRingHomProperty.descendsAlong
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
Goal:
P : MorphismProperty Scheme
inst : P.IsStableUnderBaseChange
Q : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
inst_1 : HasRingHomProperty P fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
h :
  RingHom.CodescendsAlong.{u} (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    fun {R S : Type u} [CommRing R] [CommRing S] ↦ RingHom.FaithfullyFlat
refine_1 : @IsLocalIso ⊓ @Surjective ≤ @Surjective ⊓ @Flat
refine_2 :
  ∀ {R S : CommRingCat.{u}} {f : R ⟶ S}, (@Surjective ⊓ @Flat) (Spec.map f) → (CommRingCat.Hom.hom f).FaithfullyFlat
⊢ P.DescendsAlong (@Surjective ⊓ @Flat ⊓ @QuasiCompact)

Tactic:
refine HasRingHomProperty.descendsAlong _ _ _ _ ?_ ?_ h

Premises used: AlgebraicGeometry.HasRingHomProperty.descendsAlong
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
Goal:
P : MorphismProperty Scheme
inst : P.IsStableUnderBaseChange
Q : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
inst_1 : HasRingHomProperty P fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
h :
  RingHom.CodescendsAlong.{u} (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    fun {R S : Type u} [CommRing R] [CommRing S] ↦ RingHom.FaithfullyFlat
refine_1 : @Surjective ⊓ @IsLocalIso ≤ @Surjective ⊓ @Flat
⊢ @IsLocalIso ⊓ @Surjective ≤ @Surjective ⊓ @Flat

Tactic:
rw [inf_comm]

Premises used: inf_comm
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
Goal:
P : MorphismProperty Scheme
inst : P.IsStableUnderBaseChange
Q : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
inst_1 : HasRingHomProperty P fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
h :
  RingHom.CodescendsAlong.{u} (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    fun {R S : Type u} [CommRing R] [CommRing S] ↦ RingHom.FaithfullyFlat
refine_1 : @IsLocalIso ≤ @Flat
⊢ @Surjective ⊓ @IsLocalIso ≤ @Surjective ⊓ @Flat

Tactic:
gcongr
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
Goal:
P : MorphismProperty Scheme
inst : P.IsStableUnderBaseChange
Q : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
inst_1 : HasRingHomProperty P fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
h :
  RingHom.CodescendsAlong.{u} (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    fun {R S : Type u} [CommRing R] [CommRing S] ↦ RingHom.FaithfullyFlat
⊢ @IsLocalIso ≤ @Flat

Tactic:
IsLocalIso.le_of_isZariskiLocalAtSource @Flat

Premises used: AlgebraicGeometry.Flat, AlgebraicGeometry.IsLocalIso.le_of_isZariskiLocalAtSource
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
Goal:
P : MorphismProperty Scheme
inst : P.IsStableUnderBaseChange
Q : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
inst_1 : HasRingHomProperty P fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
h :
  RingHom.CodescendsAlong.{u} (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    fun {R S : Type u} [CommRing R] [CommRing S] ↦ RingHom.FaithfullyFlat
⊢ @IsLocalIso ≤ @Flat

Tactic:
exact IsLocalIso.le_of_isZariskiLocalAtSource @Flat

Premises used: AlgebraicGeometry.Flat, AlgebraicGeometry.IsLocalIso.le_of_isZariskiLocalAtSource
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
Goal:
P : MorphismProperty Scheme
inst : P.IsStableUnderBaseChange
Q : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
inst_1 : HasRingHomProperty P fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
h :
  RingHom.CodescendsAlong.{u} (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    fun {R S : Type u} [CommRing R] [CommRing S] ↦ RingHom.FaithfullyFlat
R S : CommRingCat
f : R ⟶ S
refine_2 : ∀ (hf₁ : Surjective (Spec.map f)) (hf₂ : Flat (Spec.map f)), (CommRingCat.Hom.hom f).FaithfullyFlat
⊢ (@Surjective ⊓ @Flat) (Spec.map f) → (CommRingCat.Hom.hom f).FaithfullyFlat

Tactic:
⟨hf₁, hf₂⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
Goal:
P : MorphismProperty Scheme
inst : P.IsStableUnderBaseChange
Q : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
inst_1 : HasRingHomProperty P fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
h :
  RingHom.CodescendsAlong.{u} (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    fun {R S : Type u} [CommRing R] [CommRing S] ↦ RingHom.FaithfullyFlat
R S : CommRingCat
f : R ⟶ S
hf₁ : Surjective (Spec.map f)
hf₂ : Flat (Spec.map f)
refine_2 : (CommRingCat.Hom.hom f).Flat ∧ Function.Surjective (PrimeSpectrum.comap (CommRingCat.Hom.hom f))
⊢ (CommRingCat.Hom.hom f).FaithfullyFlat

Tactic:
rw [RingHom.FaithfullyFlat.iff_flat_and_comap_surjective]

Premises used: RingHom.FaithfullyFlat.iff_flat_and_comap_surjective