awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsDominant f
inst_1 : IsReduced Y
⊢ IsSchemeTheoreticallyDominant f
have rw : Set.range (ι := ↥X) ⇑f ⊆ (↑(Scheme.Hom.ker f).support : Set ↥Y)
Tactic: rw [isSchemeTheoreticallyDominant_iff, ← Scheme.IdealSheafData.support_eq_top_iff,
    ← SetLike.coe_injective.eq_iff, TopologicalSpace.Closeds.coe_top, ← Set.univ_subset_iff,
    ← f.denseRange.closure_eq, f.ker.support.isClosed.closure_subset_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsSchemeTheoreticallyDominant f
inst_1 : QuasiCompact f
U : Y.Opens
⊢ Function.Injective (α := (↑Γ(Y, U) : Type u_1)) (β := (↑Γ(X, f ⁻¹ᵁ U) : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
          CommRingCat.carrier) (app f U)) :
      (a : (↑Γ(Y, U) : Type u_1)) → (↑Γ(X, f ⁻¹ᵁ U) : Type u_1))
have inr : ∀
  (this :
    ∀ (U : Y.Opens) (hU : IsAffineOpen U),
      Function.Injective (α := (↑Γ(Y, U) : Type u_1)) (β := (↑Γ(X, f ⁻¹ᵁ U) : Type u_1))
        (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier) (app f U)) :
          (a : (↑Γ(Y, U) : Type u_1)) → (↑Γ(X, f ⁻¹ᵁ U) : Type u_1)))
  (hU : ¬IsAffineOpen U),
  Function.Injective (α := (↑Γ(Y, U) : Type u_1)) (β := (↑Γ(X, f ⁻¹ᵁ U) : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
          CommRingCat.carrier) (app f U)) :
      (a : (↑Γ(Y, U) : Type u_1)) → (↑Γ(X, f ⁻¹ᵁ U) : Type u_1))
Tactic: wlog hU : IsAffineOpen U generalizing U
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsSchemeTheoreticallyDominant f
inst_1 : QuasiCompact f
U : Y.Opens
inr :
  ∀
    (this :
      ∀ (U : Y.Opens) (hU : IsAffineOpen U),
        Function.Injective (α := (↑Γ(Y, U) : Type u_1)) (β := (↑Γ(X, f ⁻¹ᵁ U) : Type u_1))
          (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                CommRingCat.carrier) (app f U)) :
            (a : (↑Γ(Y, U) : Type u_1)) → (↑Γ(X, f ⁻¹ᵁ U) : Type u_1)))
    (hU : ¬IsAffineOpen U),
    Function.Injective (α := (↑Γ(Y, U) : Type u_1)) (β := (↑Γ(X, f ⁻¹ᵁ U) : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (app f U)) :
        (a : (↑Γ(Y, U) : Type u_1)) → (↑Γ(X, f ⁻¹ᵁ U) : Type u_1))
⊢ Function.Injective (α := (↑Γ(Y, U) : Type u_1)) (β := (↑Γ(X, f ⁻¹ᵁ U) : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
          CommRingCat.carrier) (app f U)) :
      (a : (↑Γ(Y, U) : Type u_1)) → (↑Γ(X, f ⁻¹ᵁ U) : Type u_1))
have wlog : ∀ (U : Y.Opens) (hU : IsAffineOpen U),
  Function.Injective (α := (↑Γ(Y, U) : Type u_1)) (β := (↑Γ(X, f ⁻¹ᵁ U) : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
          CommRingCat.carrier) (app f U)) :
      (a : (↑Γ(Y, U) : Type u_1)) → (↑Γ(X, f ⁻¹ᵁ U) : Type u_1))
Tactic: wlog hU : IsAffineOpen U generalizing U
Cleared hypotheses: U
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsSchemeTheoreticallyDominant f
inst_1 : QuasiCompact f
U : Y.Opens
hU : IsAffineOpen U
⊢ Function.Injective (α := (↑Γ(Y, U) : Type u_1)) (β := (↑Γ(X, f ⁻¹ᵁ U) : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
          CommRingCat.carrier) (app f U)) :
      (a : (↑Γ(Y, U) : Type u_1)) → (↑Γ(X, f ⁻¹ᵁ U) : Type u_1))
have rw : IdealSheafData.ideal ⊥ (Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) U hU) = ⊥
Tactic: rw [RingHom.injective_iff_ker_eq_bot, ← f.ker_apply ⟨U, hU⟩, f.ker_eq_bot]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsSchemeTheoreticallyDominant f
inst_1 : QuasiCompact f
U : Y.Opens
this :
  ∀ (U : Y.Opens) (hU : IsAffineOpen U),
    Function.Injective (α := (↑Γ(Y, U) : Type u_1)) (β := (↑Γ(X, f ⁻¹ᵁ U) : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (app f U)) :
        (a : (↑Γ(Y, U) : Type u_1)) → (↑Γ(X, f ⁻¹ᵁ U) : Type u_1))
hU : ¬IsAffineOpen U
⊢ Function.Injective (α := (↑Γ(Y, U) : Type u_1)) (β := (↑Γ(X, f ⁻¹ᵁ U) : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
          CommRingCat.carrier) (app f U)) :
      (a : (↑Γ(Y, U) : Type u_1)) → (↑Γ(X, f ⁻¹ᵁ U) : Type u_1))
have inr : ∀ (a : (↑Γ(Y, U) : Type u_1)),
  Eq (α := (↑Γ(X, f ⁻¹ᵁ U) : Type u_1))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier) (app f U) :
            (a : (↑Γ(Y, U) : Type u_1)) → (↑Γ(X, f ⁻¹ᵁ U) : Type u_1))
          a :
        (↑Γ(X, f ⁻¹ᵁ U) : Type u_1))
      (0 : (↑Γ(X, f ⁻¹ᵁ U) : Type u_1)) →
    a = 0
Tactic: rw [injective_iff_map_eq_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsSchemeTheoreticallyDominant f
inst_1 : QuasiCompact f
U : Y.Opens
this :
  ∀ (U : Y.Opens) (hU : IsAffineOpen U),
    Function.Injective (α := (↑Γ(Y, U) : Type u_1)) (β := (↑Γ(X, f ⁻¹ᵁ U) : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (app f U)) :
        (a : (↑Γ(Y, U) : Type u_1)) → (↑Γ(X, f ⁻¹ᵁ U) : Type u_1))
hU : ¬IsAffineOpen U
s : (↑Γ(Y, U) : Type u_1)
hs :
  Eq (α := (↑Γ(X, f ⁻¹ᵁ U) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (app f U) :
          (a : (↑Γ(Y, U) : Type u_1)) → (↑Γ(X, f ⁻¹ᵁ U) : Type u_1))
        s :
      (↑Γ(X, f ⁻¹ᵁ U) : Type u_1))
    (0 : (↑Γ(X, f ⁻¹ᵁ U) : Type u_1))
⊢ s = 0
have inr : ∀ (x : ↥Y) (hx : x ∈ Opposite.unop (Opposite.op U)),
  ∃ (V : TopologicalSpace.Opens ↥Y) (hV : V ≤ Opposite.unop (Opposite.op U)),
    x ∈ V ∧
      Eq (α := (↑(Y.presheaf.obj (Opposite.op V)) : Type u_1))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                CommRingCat.carrier) (Y.presheaf.map (homOfLE hV).op) :
              (a : (↑(Y.presheaf.obj (Opposite.op (Opposite.unop (Opposite.op U)))) : Type u_1)) →
                (↑(Y.presheaf.obj (Opposite.op V)) : Type u_1))
            s :
          (↑(Y.presheaf.obj (Opposite.op V)) : Type u_1))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                CommRingCat.carrier) (Y.presheaf.map (homOfLE hV).op) :
              (a : (↑(Y.presheaf.obj (Opposite.op (Opposite.unop (Opposite.op U)))) : Type u_1)) →
                (↑(Y.presheaf.obj (Opposite.op V)) : Type u_1))
            0 :
          (↑(Y.presheaf.obj (Opposite.op V)) : Type u_1))
Tactic: refine Y.IsSheaf.section_ext fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant (goal)
Goal:
X Y : Scheme
Z : Scheme
S : Scheme
f_1 : X ⟶ S
g_1 : Y ⟶ S
f : X ⟶ S
g : Y ⟶ S
inst : IsSchemeTheoreticallyDominant f
inst_1 : QuasiCompact f
inst_2 : Flat g
⊢ IsSchemeTheoreticallyDominant (X := pullback f g) (pullback.snd f g)
have rw : Scheme.Hom.ker (X := pullback f g) (pullback.snd f g) = ⊥
Tactic: rw [isSchemeTheoreticallyDominant_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant (goal)
Goal:
X Y : Scheme
Z : Scheme
S : Scheme
f_1 : X ⟶ S
g_1 : Y ⟶ S
f : X ⟶ S
g : Y ⟶ S
inst : IsSchemeTheoreticallyDominant f
inst_1 : QuasiCompact f
inst_2 : Flat g
h𝒰 : TopologicalSpace.IsOpenCover (X := ↥Y)
  fun
    (V :
      { x : TopologicalSpace.Opens ↥Y × (↑S.affineOpens : Type u_1) //
        x.1 ∈ Y.affineOpens ∧
          x.1 ≤
            (TopologicalSpace.Opens.comap (TopCat.Hom.hom g.base) :
                (a : TopologicalSpace.Opens ↥S) → TopologicalSpace.Opens ↥Y)
              (↑x.2 : TopologicalSpace.Opens ↥S) }) ↦
  (↑V : TopologicalSpace.Opens ↥Y × (↑S.affineOpens : Type u_1)).1 :=
  ⋯
⊢ Scheme.Hom.ker (X := pullback f g) (pullback.snd f g) = ⊥
have refine : ∀
  (i :
    { x : TopologicalSpace.Opens ↥Y × (↑S.affineOpens : Type u_1) //
      x.1 ∈ Y.affineOpens ∧
        x.1 ≤
          (TopologicalSpace.Opens.comap (TopCat.Hom.hom g.base) :
              (a : TopologicalSpace.Opens ↥S) → TopologicalSpace.Opens ↥Y)
            (↑x.2 : TopologicalSpace.Opens ↥S) }),
  Eq (α :=
    Ideal
      (↑Γ(Y,
            (↑((fun
                      (U :
                        { x : TopologicalSpace.Opens ↥Y × (↑S.affineOpens : Type u_1) //
                          x.1 ∈ Y.affineOpens ∧
                            x.1 ≤
                              (TopologicalSpace.Opens.comap (TopCat.Hom.hom g.base) :
                                  (a : TopologicalSpace.Opens ↥S) → TopologicalSpace.Opens ↥Y)
                                (↑x.2 : TopologicalSpace.Opens ↥S) }) ↦
                    Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens)
                      (↑U : TopologicalSpace.Opens ↥Y × (↑S.affineOpens : Type u_1)).1 sorry)
                  i) :
              Y.Opens)) :
        Type u_1))
    ((Scheme.Hom.ker (X := pullback f g) (pullback.snd f g)).ideal
      ((fun
            (U :
              { x : TopologicalSpace.Opens ↥Y × (↑S.affineOpens : Type u_1) //
                x.1 ∈ Y.affineOpens ∧
                  x.1 ≤
                    (TopologicalSpace.Opens.comap (TopCat.Hom.hom g.base) :
                        (a : TopologicalSpace.Opens ↥S) → TopologicalSpace.Opens ↥Y)
                      (↑x.2 : TopologicalSpace.Opens ↥S) }) ↦
          Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens)
            (↑U : TopologicalSpace.Opens ↥Y × (↑S.affineOpens : Type u_1)).1 sorry)
        i))
    (Scheme.IdealSheafData.ideal ⊥
      ((fun
            (U :
              { x : TopologicalSpace.Opens ↥Y × (↑S.affineOpens : Type u_1) //
                x.1 ∈ Y.affineOpens ∧
                  x.1 ≤
                    (TopologicalSpace.Opens.comap (TopCat.Hom.hom g.base) :
                        (a : TopologicalSpace.Opens ↥S) → TopologicalSpace.Opens ↥Y)
                      (↑x.2 : TopologicalSpace.Opens ↥S) }) ↦
          Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens)
            (↑U : TopologicalSpace.Opens ↥Y × (↑S.affineOpens : Type u_1)).1 sorry)
        i))
Tactic: refine Scheme.IdealSheafData.ext_of_iSup_eq_top (fun U ↦ ⟨_, by exact U.2.1⟩) h𝒰 ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant (goal)
Goal:
X Y : Scheme
Z : Scheme
S : Scheme
f_1 : X ⟶ S
g_1 : Y ⟶ S
f : X ⟶ S
g : Y ⟶ S
inst : IsSchemeTheoreticallyDominant f
inst_1 : QuasiCompact f
inst_2 : Flat g
h𝒰 : TopologicalSpace.IsOpenCover (X := ↥Y)
  fun
    (V :
      { x : TopologicalSpace.Opens ↥Y × (↑S.affineOpens : Type u_1) //
        x.1 ∈ Y.affineOpens ∧
          x.1 ≤
            (TopologicalSpace.Opens.comap (TopCat.Hom.hom g.base) :
                (a : TopologicalSpace.Opens ↥S) → TopologicalSpace.Opens ↥Y)
              (↑x.2 : TopologicalSpace.Opens ↥S) }) ↦
  (↑V : TopologicalSpace.Opens ↥Y × (↑S.affineOpens : Type u_1)).1 :=
  ⋯
V : TopologicalSpace.Opens ↥Y
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hV : (V, Subtype.mk (p := fun (x : TopologicalSpace.Opens ↥S) ↦ x ∈ S.affineOpens) U hU).1 ∈ Y.affineOpens
hVU : V ≤ g ⁻¹ᵁ U
x : (↑Γ(Y, V) : Type u_1)
hx :
  Membership.mem (γ := Submodule (↑Γ(Y, V) : Type u_1) (↑Γ(Y, V) : Type u_1))
    (RingHom.ker (F := (↑Γ(Y, V) : Type u_1) →+* (↑Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V) : Type u_1))
      (CommRingCat.Hom.hom (Scheme.Hom.app (pullback.snd f g) V)))
    x
⊢ Eq (α := (pullback f g).Opens) (pullback.snd f g ⁻¹ᵁ V) (pullback.fst f g ⁻¹ᵁ f ⁻¹ᵁ U ⊓ pullback.snd f g ⁻¹ᵁ V)
have grw : Eq (α := (pullback f g).Opens) (pullback.snd f g ⁻¹ᵁ V) ((pullback.fst f g ≫ f) ⁻¹ᵁ U ⊓ pullback.snd f g ⁻¹ᵁ V)
Tactic: grw [← Scheme.Hom.comp_preimage, pullback.condition, Scheme.Hom.comp_preimage, right_eq_inf,
        hVU]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant (goal)
Goal:
X Y : Scheme
Z : Scheme
S : Scheme
f_1 : X ⟶ S
g_1 : Y ⟶ S
f : X ⟶ S
g : Y ⟶ S
inst : IsSchemeTheoreticallyDominant f
inst_1 : QuasiCompact f
inst_2 : Flat g
h𝒰 : TopologicalSpace.IsOpenCover (X := ↥Y)
  fun
    (V :
      { x : TopologicalSpace.Opens ↥Y × (↑S.affineOpens : Type u_1) //
        x.1 ∈ Y.affineOpens ∧
          x.1 ≤
            (TopologicalSpace.Opens.comap (TopCat.Hom.hom g.base) :
                (a : TopologicalSpace.Opens ↥S) → TopologicalSpace.Opens ↥Y)
              (↑x.2 : TopologicalSpace.Opens ↥S) }) ↦
  (↑V : TopologicalSpace.Opens ↥Y × (↑S.affineOpens : Type u_1)).1 :=
  ⋯
V : TopologicalSpace.Opens ↥Y
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hV : (V, Subtype.mk (p := fun (x : TopologicalSpace.Opens ↥S) ↦ x ∈ S.affineOpens) U hU).1 ∈ Y.affineOpens
hVU : V ≤ g ⁻¹ᵁ U
x : (↑Γ(Y, V) : Type u_1)
hx :
  Membership.mem (γ := Submodule (↑Γ(Y, V) : Type u_1) (↑Γ(Y, V) : Type u_1))
    (RingHom.ker (F := (↑Γ(Y, V) : Type u_1) →+* (↑Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V) : Type u_1))
      (CommRingCat.Hom.hom (Scheme.Hom.app (pullback.snd f g) V)))
    x
grw : Eq (α := (pullback f g).Opens) (pullback.snd f g ⁻¹ᵁ V) ((pullback.fst f g ≫ f) ⁻¹ᵁ U ⊓ pullback.snd f g ⁻¹ᵁ V)
⊢ Eq (α := (pullback f g).Opens) (pullback.snd f g ⁻¹ᵁ V) (pullback.fst f g ⁻¹ᵁ f ⁻¹ᵁ U ⊓ pullback.snd f g ⁻¹ᵁ V)
have grw₁ : Eq (α := (pullback f g).Opens) (pullback.snd f g ⁻¹ᵁ V) ((pullback.snd f g ≫ g) ⁻¹ᵁ U ⊓ pullback.snd f g ⁻¹ᵁ V)
Tactic: grw [← Scheme.Hom.comp_preimage, pullback.condition, Scheme.Hom.comp_preimage, right_eq_inf,
        hVU]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant (goal)
Goal:
X Y : Scheme
Z : Scheme
S : Scheme
f_1 : X ⟶ S
g_1 : Y ⟶ S
f : X ⟶ S
g : Y ⟶ S
inst : IsSchemeTheoreticallyDominant f
inst_1 : QuasiCompact f
inst_2 : Flat g
h𝒰 : TopologicalSpace.IsOpenCover (X := ↥Y)
  fun
    (V :
      { x : TopologicalSpace.Opens ↥Y × (↑S.affineOpens : Type u_1) //
        x.1 ∈ Y.affineOpens ∧
          x.1 ≤
            (TopologicalSpace.Opens.comap (TopCat.Hom.hom g.base) :
                (a : TopologicalSpace.Opens ↥S) → TopologicalSpace.Opens ↥Y)
              (↑x.2 : TopologicalSpace.Opens ↥S) }) ↦
  (↑V : TopologicalSpace.Opens ↥Y × (↑S.affineOpens : Type u_1)).1 :=
  ⋯
V : TopologicalSpace.Opens ↥Y
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hV : (V, Subtype.mk (p := fun (x : TopologicalSpace.Opens ↥S) ↦ x ∈ S.affineOpens) U hU).1 ∈ Y.affineOpens
hVU : V ≤ g ⁻¹ᵁ U
x : (↑Γ(Y, V) : Type u_1)
hx :
  Membership.mem (γ := Submodule (↑Γ(Y, V) : Type u_1) (↑Γ(Y, V) : Type u_1))
    (RingHom.ker (F := (↑Γ(Y, V) : Type u_1) →+* (↑Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V) : Type u_1))
      (CommRingCat.Hom.hom (Scheme.Hom.app (pullback.snd f g) V)))
    x
grw : Eq (α := (pullback f g).Opens) (pullback.snd f g ⁻¹ᵁ V) ((pullback.fst f g ≫ f) ⁻¹ᵁ U ⊓ pullback.snd f g ⁻¹ᵁ V)
grw₁ : Eq (α := (pullback f g).Opens) (pullback.snd f g ⁻¹ᵁ V) ((pullback.snd f g ≫ g) ⁻¹ᵁ U ⊓ pullback.snd f g ⁻¹ᵁ V)
⊢ Eq (α := (pullback f g).Opens) (pullback.snd f g ⁻¹ᵁ V) (pullback.fst f g ⁻¹ᵁ f ⁻¹ᵁ U ⊓ pullback.snd f g ⁻¹ᵁ V)
have grw₂ : Eq (α := (pullback f g).Opens) (pullback.snd f g ⁻¹ᵁ V) (pullback.snd f g ⁻¹ᵁ g ⁻¹ᵁ U ⊓ pullback.snd f g ⁻¹ᵁ V)
Tactic: grw [← Scheme.Hom.comp_preimage, pullback.condition, Scheme.Hom.comp_preimage, right_eq_inf,
        hVU]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant (goal)
Goal:
X Y : Scheme
Z : Scheme
S : Scheme
f_1 : X ⟶ S
g_1 : Y ⟶ S
f : X ⟶ S
g : Y ⟶ S
inst : IsSchemeTheoreticallyDominant f
inst_1 : QuasiCompact f
inst_2 : Flat g
h𝒰 : TopologicalSpace.IsOpenCover (X := ↥Y)
  fun
    (V :
      { x : TopologicalSpace.Opens ↥Y × (↑S.affineOpens : Type u_1) //
        x.1 ∈ Y.affineOpens ∧
          x.1 ≤
            (TopologicalSpace.Opens.comap (TopCat.Hom.hom g.base) :
                (a : TopologicalSpace.Opens ↥S) → TopologicalSpace.Opens ↥Y)
              (↑x.2 : TopologicalSpace.Opens ↥S) }) ↦
  (↑V : TopologicalSpace.Opens ↥Y × (↑S.affineOpens : Type u_1)).1 :=
  ⋯
V : TopologicalSpace.Opens ↥Y
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hV : (V, Subtype.mk (p := fun (x : TopologicalSpace.Opens ↥S) ↦ x ∈ S.affineOpens) U hU).1 ∈ Y.affineOpens
hVU : V ≤ g ⁻¹ᵁ U
x : (↑Γ(Y, V) : Type u_1)
hx :
  Membership.mem (γ := Submodule (↑Γ(Y, V) : Type u_1) (↑Γ(Y, V) : Type u_1))
    (RingHom.ker (F := (↑Γ(Y, V) : Type u_1) →+* (↑Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V) : Type u_1))
      (CommRingCat.Hom.hom (Scheme.Hom.app (pullback.snd f g) V)))
    x
grw : Eq (α := (pullback f g).Opens) (pullback.snd f g ⁻¹ᵁ V) ((pullback.fst f g ≫ f) ⁻¹ᵁ U ⊓ pullback.snd f g ⁻¹ᵁ V)
grw₁ : Eq (α := (pullback f g).Opens) (pullback.snd f g ⁻¹ᵁ V) ((pullback.snd f g ≫ g) ⁻¹ᵁ U ⊓ pullback.snd f g ⁻¹ᵁ V)
grw₂ : Eq (α := (pullback f g).Opens) (pullback.snd f g ⁻¹ᵁ V) (pullback.snd f g ⁻¹ᵁ g ⁻¹ᵁ U ⊓ pullback.snd f g ⁻¹ᵁ V)
⊢ Eq (α := (pullback f g).Opens) (pullback.snd f g ⁻¹ᵁ V) (pullback.fst f g ⁻¹ᵁ f ⁻¹ᵁ U ⊓ pullback.snd f g ⁻¹ᵁ V)
have grw₃ : LE.le (α := (pullback f g).Opens) (pullback.snd f g ⁻¹ᵁ V) (pullback.snd f g ⁻¹ᵁ g ⁻¹ᵁ U)
Tactic: grw [← Scheme.Hom.comp_preimage, pullback.condition, Scheme.Hom.comp_preimage, right_eq_inf,
        hVU]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant (goal)
Goal:
X Y : Scheme
Z : Scheme
S : Scheme
f_1 : X ⟶ S
g_1 : Y ⟶ S
f : X ⟶ S
g : Y ⟶ S
inst : IsSchemeTheoreticallyDominant f
inst_1 : QuasiCompact f
inst_2 : Flat g
h𝒰 : TopologicalSpace.IsOpenCover (X := ↥Y)
  fun
    (V :
      { x : TopologicalSpace.Opens ↥Y × (↑S.affineOpens : Type u_1) //
        x.1 ∈ Y.affineOpens ∧
          x.1 ≤
            (TopologicalSpace.Opens.comap (TopCat.Hom.hom g.base) :
                (a : TopologicalSpace.Opens ↥S) → TopologicalSpace.Opens ↥Y)
              (↑x.2 : TopologicalSpace.Opens ↥S) }) ↦
  (↑V : TopologicalSpace.Opens ↥Y × (↑S.affineOpens : Type u_1)).1 :=
  ⋯
V : TopologicalSpace.Opens ↥Y
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hV : (V, Subtype.mk (p := fun (x : TopologicalSpace.Opens ↥S) ↦ x ∈ S.affineOpens) U hU).1 ∈ Y.affineOpens
hVU : V ≤ g ⁻¹ᵁ U
x : (↑Γ(Y, V) : Type u_1)
hx :
  Membership.mem (γ := Submodule (↑Γ(Y, V) : Type u_1) (↑Γ(Y, V) : Type u_1))
    (RingHom.ker (F := (↑Γ(Y, V) : Type u_1) →+* (↑Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V) : Type u_1))
      (CommRingCat.Hom.hom (Scheme.Hom.app (pullback.snd f g) V)))
    x
grw : Eq (α := (pullback f g).Opens) (pullback.snd f g ⁻¹ᵁ V) ((pullback.fst f g ≫ f) ⁻¹ᵁ U ⊓ pullback.snd f g ⁻¹ᵁ V)
grw₁ : Eq (α := (pullback f g).Opens) (pullback.snd f g ⁻¹ᵁ V) ((pullback.snd f g ≫ g) ⁻¹ᵁ U ⊓ pullback.snd f g ⁻¹ᵁ V)
grw₂ : Eq (α := (pullback f g).Opens) (pullback.snd f g ⁻¹ᵁ V) (pullback.snd f g ⁻¹ᵁ g ⁻¹ᵁ U ⊓ pullback.snd f g ⁻¹ᵁ V)
grw₃ : LE.le (α := (pullback f g).Opens) (pullback.snd f g ⁻¹ᵁ V) (pullback.snd f g ⁻¹ᵁ g ⁻¹ᵁ U)
⊢ Eq (α := (pullback f g).Opens) (pullback.snd f g ⁻¹ᵁ V) (pullback.fst f g ⁻¹ᵁ f ⁻¹ᵁ U ⊓ pullback.snd f g ⁻¹ᵁ V)
have grw₄ : LE.le (α := (pullback f g).Opens) (pullback.snd f g ⁻¹ᵁ g ⁻¹ᵁ U) (pullback.snd f g ⁻¹ᵁ g ⁻¹ᵁ U)
Tactic: grw [← Scheme.Hom.comp_preimage, pullback.condition, Scheme.Hom.comp_preimage, right_eq_inf,
        hVU]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant (hypothesis)
Goal:
X Y : Scheme
Z : Scheme
S : Scheme
f_1 : X ⟶ S
g_1 : Y ⟶ S
f : X ⟶ S
g : Y ⟶ S
inst : IsSchemeTheoreticallyDominant f
inst_1 : QuasiCompact f
inst_2 : Flat g
h𝒰 : TopologicalSpace.IsOpenCover (X := ↥Y)
  fun
    (V :
      { x : TopologicalSpace.Opens ↥Y × (↑S.affineOpens : Type u_1) //
        x.1 ∈ Y.affineOpens ∧
          x.1 ≤
            (TopologicalSpace.Opens.comap (TopCat.Hom.hom g.base) :
                (a : TopologicalSpace.Opens ↥S) → TopologicalSpace.Opens ↥Y)
              (↑x.2 : TopologicalSpace.Opens ↥S) }) ↦
  (↑V : TopologicalSpace.Opens ↥Y × (↑S.affineOpens : Type u_1)).1 :=
  ⋯
V : TopologicalSpace.Opens ↥Y
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hV : (V, Subtype.mk (p := fun (x : TopologicalSpace.Opens ↥S) ↦ x ∈ S.affineOpens) U hU).1 ∈ Y.affineOpens
hVU : V ≤ g ⁻¹ᵁ U
x : (↑Γ(Y, V) : Type u_1)
hx :
  Membership.mem (γ := Submodule (↑Γ(Y, V) : Type u_1) (↑Γ(Y, V) : Type u_1))
    (RingHom.ker (F := (↑Γ(Y, V) : Type u_1) →+* (↑Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V) : Type u_1))
      (CommRingCat.Hom.hom (Scheme.Hom.app (pullback.snd f g) V)))
    x
⊢ Membership.mem (γ := Submodule (↑Γ(Y, V) : Type u_1) (↑Γ(Y, V) : Type u_1)) ⊥ x
have this : Mono (Y := Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V)) (pushoutSection sorry hVU sorry sorry)
Tactic: have := mono_pushoutSection_of_isCompact_of_flat_right
    (.of_hasPullback f g) (UY := pullback.snd f g ⁻¹ᵁ V) hVU le_rfl (by
      grw [← Scheme.Hom.comp_preimage, pullback.condition, Scheme.Hom.comp_preimage, right_eq_inf,
        hVU]) hU hV (f.isCompact_preimage hU.isCompact)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant (hypothesis)
Goal:
X Y : Scheme
Z : Scheme
S : Scheme
f_1 : X ⟶ S
g_1 : Y ⟶ S
f : X ⟶ S
g : Y ⟶ S
inst : IsSchemeTheoreticallyDominant f
inst_1 : QuasiCompact f
inst_2 : Flat g
h𝒰 : TopologicalSpace.IsOpenCover (X := ↥Y)
  fun
    (V :
      { x : TopologicalSpace.Opens ↥Y × (↑S.affineOpens : Type u_1) //
        x.1 ∈ Y.affineOpens ∧
          x.1 ≤
            (TopologicalSpace.Opens.comap (TopCat.Hom.hom g.base) :
                (a : TopologicalSpace.Opens ↥S) → TopologicalSpace.Opens ↥Y)
              (↑x.2 : TopologicalSpace.Opens ↥S) }) ↦
  (↑V : TopologicalSpace.Opens ↥Y × (↑S.affineOpens : Type u_1)).1 :=
  ⋯
V : TopologicalSpace.Opens ↥Y
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hV : (V, Subtype.mk (p := fun (x : TopologicalSpace.Opens ↥S) ↦ x ∈ S.affineOpens) U hU).1 ∈ Y.affineOpens
hVU : V ≤ g ⁻¹ᵁ U
x : (↑Γ(Y, V) : Type u_1)
hx :
  Membership.mem (γ := Submodule (↑Γ(Y, V) : Type u_1) (↑Γ(Y, V) : Type u_1))
    (RingHom.ker (F := (↑Γ(Y, V) : Type u_1) →+* (↑Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V) : Type u_1))
      (CommRingCat.Hom.hom (Scheme.Hom.app (pullback.snd f g) V)))
    x
this : Mono (Y := Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V)) (pushoutSection ⋯ hVU ⋯ ⋯)
⊢ Membership.mem (γ := Submodule (↑Γ(Y, V) : Type u_1) (↑Γ(Y, V) : Type u_1)) ⊥ x
have this₁ : Function.Injective (α := (↑(pushout (Scheme.Hom.appLE f U (f ⁻¹ᵁ U) sorry) (Scheme.Hom.appLE g U V hVU)) : Type u_1)) (β :=
  (↑Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V) : Type u_1))
  (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
        CommRingCat.carrier) (Y := Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V)) (pushoutSection sorry hVU sorry sorry)) :
    (a : (↑(pushout (Scheme.Hom.appLE f U (f ⁻¹ᵁ U) sorry) (Scheme.Hom.appLE g U V hVU)) : Type u_1)) →
      (↑Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V) : Type u_1))
Tactic: rw [@ConcreteCategory.mono_iff_injective_of_preservesPullback] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant (goal)
Goal:
X Y Z S : Scheme
f : X ⟶ S
g : Y ⟶ S
pX : Z ⟶ X
pY : Z ⟶ Y
H : IsPullback pX pY f g
inst : IsSchemeTheoreticallyDominant f
inst_1 : QuasiCompact f
inst_2 : Flat g
⊢ IsSchemeTheoreticallyDominant pY
have rw : IsSchemeTheoreticallyDominant (CategoryStruct.comp (Y := pullback f g) (Iso.hom H.isoPullback) (pullback.snd f g))
Tactic: rw [← H.isoPullback_hom_snd]