awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Flat (goal)
Goal:
X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
inst : Flat f
hUS : IsAffineOpen US
hUT : IsAffineOpen UT
hUX : IsCompact (↑UX : Set ↥X)
⊢ Mono (pushoutSection H hUST hUSX hUY)
have obtain : ∀ (I : Set (↑X.affineOpens : Type u)) (hI : I.Finite) (e : UX = ⨆ i ∈ I, (↑i : X.Opens)),
  Mono (pushoutSection H hUST hUSX hUY)
Tactic: classical
  obtain ⟨I, hI, e⟩ := isCompact_iff_finite_and_eq_biUnion_affineOpens.mp hUX
  have := hI.to_subtype
  exact mono_pushoutSection_of_iSup_eq (ι := I) H hUST hUSX hUY (·) (by rwa [iSup_subtype, eq_comm])
    (fun i ↦ have := isIso_pushoutSection_of_isAffineOpen H hUST _ rfl hUS hUT i.1.2; inferInstance)
    (f.flat_appLE hUS hUT _)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Flat (goal)
Goal:
X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
inst : Flat f
hUS : IsAffineOpen US
hUT : IsAffineOpen UT
hUX : IsCompact (↑UX : Set ↥X)
obtain :
  ∀ (I : Set (↑X.affineOpens : Type u)) (hI : I.Finite) (e : UX = ⨆ i ∈ I, (↑i : X.Opens)),
    Mono (pushoutSection H hUST hUSX hUY)
⊢ Mono (pushoutSection H hUST hUSX hUY)
have obtain₁ : ∀ (I : Set (↑X.affineOpens : Type u)) (hI : I.Finite) (e : UX = ⨆ i ∈ I, (↑i : X.Opens))
  (this : Finite.{u + 1} (↑I : Type u)), Mono (pushoutSection H hUST hUSX hUY)
Tactic: classical
  obtain ⟨I, hI, e⟩ := isCompact_iff_finite_and_eq_biUnion_affineOpens.mp hUX
  have := hI.to_subtype
  exact mono_pushoutSection_of_iSup_eq (ι := I) H hUST hUSX hUY (·) (by rwa [iSup_subtype, eq_comm])
    (fun i ↦ have := isIso_pushoutSection_of_isAffineOpen H hUST _ rfl hUS hUT i.1.2; inferInstance)
    (f.flat_appLE hUS hUT _)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Flat (goal)
Goal:
X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
inst : Flat iX
hUS : IsAffineOpen US
hUX : IsAffineOpen UX
hUT : IsCompact (↑UT : Set ↥T)
this : Mono (pushoutSection ⋯ hUSX hUST ⋯)
⊢ Mono (pushoutSection H hUST hUSX hUY)
have rw : Mono (X := pushout (Scheme.Hom.appLE f US UT hUST) (Scheme.Hom.appLE iX US UX hUSX))
  (Iso.hom (pushoutSymmetry (Scheme.Hom.appLE f US UT hUST) (Scheme.Hom.appLE iX US UX hUSX)) ≫
    pushoutSection H hUST hUSX hUY)
Tactic: rw [← mono_comp_iff_of_isIso (pushoutSymmetry _ _).hom]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Flat (goal)
Goal:
X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
inst : Flat iX
hUS : IsAffineOpen US
hUX : IsAffineOpen UX
hUT : IsCompact (↑UT : Set ↥T)
this : Mono (pushoutSection ⋯ hUSX hUST ⋯)
⊢ Mono (X := pushout (Scheme.Hom.appLE f US UT hUST) (Scheme.Hom.appLE iX US UX hUSX))
    (Iso.hom (pushoutSymmetry (Scheme.Hom.appLE f US UT hUST) (Scheme.Hom.appLE iX US UX hUSX)) ≫
      pushoutSection H hUST hUSX hUY)
have h : Iso.hom (pushoutSymmetry (Scheme.Hom.appLE f US UT hUST) (Scheme.Hom.appLE iX US UX hUSX)) ≫
    pushoutSection H hUST hUSX hUY =
  pushoutSection sorry hUSX hUST sorry
Tactic: convert! this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Flat (goal)
Goal:
X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
inst : Flat iX
hUS : IsAffineOpen US
hUX : IsAffineOpen UX
hUT : IsCompact (↑UT : Set ↥T)
⊢ Mono (pushoutSection H hUST hUSX hUY)
have suffices : Mono (pushoutSection sorry hUSX hUST sorry)
Tactic: suffices Mono (pushoutSection H.flip hUSX hUST (hUY.trans (inf_comm _ _))) by
    rw [← mono_comp_iff_of_isIso (pushoutSymmetry _ _).hom]; convert! this; cat_disch
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Flat (goal)
Goal:
X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
inst : Flat f
hUS : IsAffineOpen US
hUT : IsAffineOpen UT
hUX : IsCompact (↑UX : Set ↥X)
hUX' : IsQuasiSeparated (↑UX : Set ↥X)
⊢ IsIso (pushoutSection H hUST hUSX hUY)
have obtain : ∀ (I : Set (↑X.affineOpens : Type u)) (hI : I.Finite) (e : UX = ⨆ i ∈ I, (↑i : X.Opens)),
  IsIso (pushoutSection H hUST hUSX hUY)
Tactic: obtain ⟨I, hI, e⟩ := isCompact_iff_finite_and_eq_biUnion_affineOpens.mp hUX
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Flat (goal)
Goal:
X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
inst : Flat f
hUS : IsAffineOpen US
hUT : IsAffineOpen UT
hUX : IsCompact (↑UX : Set ↥X)
hUX' : IsQuasiSeparated (↑UX : Set ↥X)
I : Set (↑X.affineOpens : Type u)
hI : I.Finite
e : UX = ⨆ i ∈ I, (↑i : X.Opens)
i : (↑I : Type u)
⊢ (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens) ≤ UX
have rw : (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens) ≤ ⨆ i ∈ I, (↑i : X.Opens)
Tactic: rw [e]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Flat (hypothesis)
Goal:
X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
inst : Flat f
hUS : IsAffineOpen US
hUT : IsAffineOpen UT
hUX : IsCompact (↑UX : Set ↥X)
hUX' : IsQuasiSeparated (↑UX : Set ↥X)
I : Set (↑X.affineOpens : Type u)
hI : I.Finite
e : UX = ⨆ i ∈ I, (↑i : X.Opens)
⊢ IsIso (pushoutSection H hUST hUSX hUY)
have hIUX : ∀ (i : (↑I : Type u)), (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens) ≤ UX
Tactic: have hIUX (i : I) : i.1 ≤ UX := by rw [e]; intro i; aesop
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Flat (hypothesis)
Goal:
X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
inst : Flat f
hUS : IsAffineOpen US
hUT : IsAffineOpen UT
hUX : IsCompact (↑UX : Set ↥X)
hUX' : IsQuasiSeparated (↑UX : Set ↥X)
I : Set (↑X.affineOpens : Type u)
hI : I.Finite
e : UX = ⨆ i ∈ I, (↑i : X.Opens)
hIUX : ∀ (i : (↑I : Type u)), (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens) ≤ UX
⊢ IsIso (pushoutSection H hUST hUSX hUY)
have this : Finite.{u + 1} (↑I : Type u)
Tactic: have := hI.to_subtype
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Flat (goal)
Goal:
X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
inst : Flat f
hUS : IsAffineOpen US
hUT : IsAffineOpen UT
hUX : IsCompact (↑UX : Set ↥X)
hUX' : IsQuasiSeparated (↑UX : Set ↥X)
I : Set (↑X.affineOpens : Type u)
hI : I.Finite
e : UX = ⨆ i ∈ I, (↑i : X.Opens)
hIUX : ∀ (i : (↑I : Type u)), (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens) ≤ UX
this : Finite.{u + 1} (↑I : Type u)
⊢ ⨆ (i : (↑I : Type u)), (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens) = UX
have rwa : ⨆ (i : (↑X.affineOpens : Type u)),
    ⨆ (h : i ∈ I),
      (↑(↑(Subtype.mk (p := fun (x : (↑X.affineOpens : Type u)) ↦ x ∈ I) i h) : (↑X.affineOpens : Type u)) : X.Opens) =
  UX
Tactic: rwa [iSup_subtype,
    eq_comm]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Flat (goal)
Goal:
X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
inst : Flat f
hUS : IsAffineOpen US
hUT : IsAffineOpen UT
hUX : IsCompact (↑UX : Set ↥X)
hUX' : IsQuasiSeparated (↑UX : Set ↥X)
I : Set (↑X.affineOpens : Type u)
hI : I.Finite
e : UX = ⨆ i ∈ I, (↑i : X.Opens)
hIUX : ∀ (i : (↑I : Type u)), (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens) ≤ UX
this : Finite.{u + 1} (↑I : Type u)
rwa :
  ⨆ (i : (↑X.affineOpens : Type u)),
      ⨆ (h : i ∈ I),
        (↑(↑(Subtype.mk (p := fun (x : (↑X.affineOpens : Type u)) ↦ x ∈ I) i h) : (↑X.affineOpens : Type u)) :
          X.Opens) =
    UX
⊢ ⨆ (i : (↑I : Type u)), (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens) = UX
have rwa₁ : UX =
  ⨆ (i : (↑X.affineOpens : Type u)),
    ⨆ (h : i ∈ I),
      (↑(↑(Subtype.mk (p := fun (x : (↑X.affineOpens : Type u)) ↦ x ∈ I) i h) : (↑X.affineOpens : Type u)) : X.Opens)
Tactic: rwa [iSup_subtype,
    eq_comm]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Flat (goal)
Goal:
X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
inst : Flat f
hUS : IsAffineOpen US
hUT : IsAffineOpen UT
hUX : IsCompact (↑UX : Set ↥X)
hUX' : IsQuasiSeparated (↑UX : Set ↥X)
⊢ IsIso (pushoutSection H hUST hUSX hUY)
have obtain : ∀ (I : Set (↑X.affineOpens : Type u)) (hI : I.Finite) (e : UX = ⨆ i ∈ I, (↑i : X.Opens)),
  IsIso (pushoutSection H hUST hUSX hUY)
Tactic: classical
  obtain ⟨I, hI, e⟩ := isCompact_iff_finite_and_eq_biUnion_affineOpens.mp hUX
  have hIUX (i : I) : i.1 ≤ UX := by rw [e]; intro i; aesop
  have := hI.to_subtype
  exact isIso_pushoutSection_of_iSup_eq H hUST hUSX hUY (fun i : I ↦ i) (by rwa [iSup_subtype,
    eq_comm]) (fun i ↦ isIso_pushoutSection_of_isAffineOpen _ _ _ _ hUS hUT i.1.2) (fun i j ↦
    mono_pushoutSection_of_isCompact_of_flat_right _ _ _ _ hUS hUT (hUX' _ _ (hIUX _) i.1.1.2
    i.1.2.isCompact (hIUX _) j.1.1.2 j.1.2.isCompact))
    (f.flat_appLE hUS hUT _)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Flat (goal)
Goal:
X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
inst : Flat f
hUS : IsAffineOpen US
hUT : IsAffineOpen UT
hUX : IsCompact (↑UX : Set ↥X)
hUX' : IsQuasiSeparated (↑UX : Set ↥X)
obtain :
  ∀ (I : Set (↑X.affineOpens : Type u)) (hI : I.Finite) (e : UX = ⨆ i ∈ I, (↑i : X.Opens)),
    IsIso (pushoutSection H hUST hUSX hUY)
⊢ IsIso (pushoutSection H hUST hUSX hUY)
have obtain₁ : ∀ (I : Set (↑X.affineOpens : Type u)) (hI : I.Finite) (e : UX = ⨆ i ∈ I, (↑i : X.Opens))
  (hIUX : ∀ (i : (↑I : Type u)), (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens) ≤ UX),
  IsIso (pushoutSection H hUST hUSX hUY)
Tactic: classical
  obtain ⟨I, hI, e⟩ := isCompact_iff_finite_and_eq_biUnion_affineOpens.mp hUX
  have hIUX (i : I) : i.1 ≤ UX := by rw [e]; intro i; aesop
  have := hI.to_subtype
  exact isIso_pushoutSection_of_iSup_eq H hUST hUSX hUY (fun i : I ↦ i) (by rwa [iSup_subtype,
    eq_comm]) (fun i ↦ isIso_pushoutSection_of_isAffineOpen _ _ _ _ hUS hUT i.1.2) (fun i j ↦
    mono_pushoutSection_of_isCompact_of_flat_right _ _ _ _ hUS hUT (hUX' _ _ (hIUX _) i.1.1.2
    i.1.2.isCompact (hIUX _) j.1.1.2 j.1.2.isCompact))
    (f.flat_appLE hUS hUT _)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Flat (goal)
Goal:
X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
inst : Flat f
hUS : IsAffineOpen US
hUT : IsAffineOpen UT
hUX : IsCompact (↑UX : Set ↥X)
hUX' : IsQuasiSeparated (↑UX : Set ↥X)
obtain :
  ∀ (I : Set (↑X.affineOpens : Type u)) (hI : I.Finite) (e : UX = ⨆ i ∈ I, (↑i : X.Opens)),
    IsIso (pushoutSection H hUST hUSX hUY)
obtain₁ :
  ∀ (I : Set (↑X.affineOpens : Type u)) (hI : I.Finite) (e : UX = ⨆ i ∈ I, (↑i : X.Opens))
    (hIUX : ∀ (i : (↑I : Type u)), (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens) ≤ UX),
    IsIso (pushoutSection H hUST hUSX hUY)
⊢ IsIso (pushoutSection H hUST hUSX hUY)
have obtain₂ : ∀ (I : Set (↑X.affineOpens : Type u)) (hI : I.Finite) (e : UX = ⨆ i ∈ I, (↑i : X.Opens))
  (hIUX : ∀ (i : (↑I : Type u)), (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens) ≤ UX)
  (this : Finite.{u + 1} (↑I : Type u)), IsIso (pushoutSection H hUST hUSX hUY)
Tactic: classical
  obtain ⟨I, hI, e⟩ := isCompact_iff_finite_and_eq_biUnion_affineOpens.mp hUX
  have hIUX (i : I) : i.1 ≤ UX := by rw [e]; intro i; aesop
  have := hI.to_subtype
  exact isIso_pushoutSection_of_iSup_eq H hUST hUSX hUY (fun i : I ↦ i) (by rwa [iSup_subtype,
    eq_comm]) (fun i ↦ isIso_pushoutSection_of_isAffineOpen _ _ _ _ hUS hUT i.1.2) (fun i j ↦
    mono_pushoutSection_of_isCompact_of_flat_right _ _ _ _ hUS hUT (hUX' _ _ (hIUX _) i.1.1.2
    i.1.2.isCompact (hIUX _) j.1.1.2 j.1.2.isCompact))
    (f.flat_appLE hUS hUT _)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Flat (goal)
Goal:
X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
inst : Flat iX
hUS : IsAffineOpen US
hUX : IsAffineOpen UX
hUT : IsCompact (↑UT : Set ↥T)
hUT' : IsQuasiSeparated (↑UT : Set ↥T)
this : IsIso (pushoutSection ⋯ hUSX hUST ⋯)
⊢ IsIso (pushoutSection H hUST hUSX hUY)
have rw : IsIso (X := pushout (Scheme.Hom.appLE f US UT hUST) (Scheme.Hom.appLE iX US UX hUSX))
  (Iso.hom (pushoutSymmetry (Scheme.Hom.appLE f US UT hUST) (Scheme.Hom.appLE iX US UX hUSX)) ≫
    pushoutSection H hUST hUSX hUY)
Tactic: rw [← isIso_comp_left_iff (pushoutSymmetry _ _).hom]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Flat (goal)
Goal:
X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
inst : Flat iX
hUS : IsAffineOpen US
hUX : IsAffineOpen UX
hUT : IsCompact (↑UT : Set ↥T)
hUT' : IsQuasiSeparated (↑UT : Set ↥T)
this : IsIso (pushoutSection ⋯ hUSX hUST ⋯)
⊢ IsIso (X := pushout (Scheme.Hom.appLE f US UT hUST) (Scheme.Hom.appLE iX US UX hUSX))
    (Iso.hom (pushoutSymmetry (Scheme.Hom.appLE f US UT hUST) (Scheme.Hom.appLE iX US UX hUSX)) ≫
      pushoutSection H hUST hUSX hUY)
have h : Iso.hom (pushoutSymmetry (Scheme.Hom.appLE f US UT hUST) (Scheme.Hom.appLE iX US UX hUSX)) ≫
    pushoutSection H hUST hUSX hUY =
  pushoutSection sorry hUSX hUST sorry
Tactic: convert! this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Flat (goal)
Goal:
X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
inst : Flat iX
hUS : IsAffineOpen US
hUX : IsAffineOpen UX
hUT : IsCompact (↑UT : Set ↥T)
hUT' : IsQuasiSeparated (↑UT : Set ↥T)
⊢ IsIso (pushoutSection H hUST hUSX hUY)
have suffices : IsIso (pushoutSection sorry hUSX hUST sorry)
Tactic: suffices IsIso (pushoutSection H.flip hUSX hUST (hUY.trans (inf_comm _ _))) by
    rw [← isIso_comp_left_iff (pushoutSymmetry _ _).hom]; convert! this; cat_disch
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Flat (goal)
Goal:
X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
inst : Flat iX
hUS : IsAffineOpen US
hUT : IsCompact (↑UT : Set ↥T)
hUX : IsCompact (↑UX : Set ↥X)
hf : (CommRingCat.Hom.hom (Scheme.Hom.appLE f US UT hUST)).Flat
⊢ Mono (pushoutSection H hUST hUSX hUY)
have obtain : ∀ (I : Set (↑X.affineOpens : Type u)) (hI : I.Finite) (e : UX = ⨆ i ∈ I, (↑i : X.Opens)),
  Mono (pushoutSection H hUST hUSX hUY)
Tactic: obtain ⟨I, hI, e⟩ := isCompact_iff_finite_and_eq_biUnion_affineOpens.mp hUX
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Flat (hypothesis)
Goal:
X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
inst : Flat iX
hUS : IsAffineOpen US
hUT : IsCompact (↑UT : Set ↥T)
hUX : IsCompact (↑UX : Set ↥X)
hf : (CommRingCat.Hom.hom (Scheme.Hom.appLE f US UT hUST)).Flat
I : Set (↑X.affineOpens : Type u)
hI : I.Finite
e : UX = ⨆ i ∈ I, (↑i : X.Opens)
⊢ Mono (pushoutSection H hUST hUSX hUY)
have this : Finite.{u + 1} (↑I : Type u)
Tactic: have := hI.to_subtype
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Flat (goal)
Goal:
X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
inst : Flat iX
hUS : IsAffineOpen US
hUT : IsCompact (↑UT : Set ↥T)
hUX : IsCompact (↑UX : Set ↥X)
hf : (CommRingCat.Hom.hom (Scheme.Hom.appLE f US UT hUST)).Flat
I : Set (↑X.affineOpens : Type u)
hI : I.Finite
e : UX = ⨆ i ∈ I, (↑i : X.Opens)
this : Finite.{u + 1} (↑I : Type u)
⊢ ⨆ (i : (↑I : Type u)), (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens) = UX
have rwa : ⨆ (i : (↑X.affineOpens : Type u)),
    ⨆ (h : i ∈ I),
      (↑(↑(Subtype.mk (p := fun (x : (↑X.affineOpens : Type u)) ↦ x ∈ I) i h) : (↑X.affineOpens : Type u)) : X.Opens) =
  UX
Tactic: rwa [iSup_subtype, eq_comm]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Flat (goal)
Goal:
X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
inst : Flat iX
hUS : IsAffineOpen US
hUT : IsCompact (↑UT : Set ↥T)
hUX : IsCompact (↑UX : Set ↥X)
hf : (CommRingCat.Hom.hom (Scheme.Hom.appLE f US UT hUST)).Flat
I : Set (↑X.affineOpens : Type u)
hI : I.Finite
e : UX = ⨆ i ∈ I, (↑i : X.Opens)
this : Finite.{u + 1} (↑I : Type u)
rwa :
  ⨆ (i : (↑X.affineOpens : Type u)),
      ⨆ (h : i ∈ I),
        (↑(↑(Subtype.mk (p := fun (x : (↑X.affineOpens : Type u)) ↦ x ∈ I) i h) : (↑X.affineOpens : Type u)) :
          X.Opens) =
    UX
⊢ ⨆ (i : (↑I : Type u)), (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens) = UX
have rwa₁ : UX =
  ⨆ (i : (↑X.affineOpens : Type u)),
    ⨆ (h : i ∈ I),
      (↑(↑(Subtype.mk (p := fun (x : (↑X.affineOpens : Type u)) ↦ x ∈ I) i h) : (↑X.affineOpens : Type u)) : X.Opens)
Tactic: rwa [iSup_subtype, eq_comm]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Flat (goal)
Goal:
X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
inst : Flat f
hUS : IsAffineOpen US
hUT : IsCompact (↑UT : Set ↥T)
hUX : IsCompact (↑UX : Set ↥X)
hiX : (CommRingCat.Hom.hom (Scheme.Hom.appLE iX US UX hUSX)).Flat
this : Mono (pushoutSection ⋯ hUSX hUST ⋯)
⊢ Mono (pushoutSection H hUST hUSX hUY)
have rw : Mono (X := pushout (Scheme.Hom.appLE f US UT hUST) (Scheme.Hom.appLE iX US UX hUSX))
  (Iso.hom (pushoutSymmetry (Scheme.Hom.appLE f US UT hUST) (Scheme.Hom.appLE iX US UX hUSX)) ≫
    pushoutSection H hUST hUSX hUY)
Tactic: rw [← mono_comp_iff_of_isIso (pushoutSymmetry _ _).hom]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Flat (goal)
Goal:
X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
inst : Flat f
hUS : IsAffineOpen US
hUT : IsCompact (↑UT : Set ↥T)
hUX : IsCompact (↑UX : Set ↥X)
hiX : (CommRingCat.Hom.hom (Scheme.Hom.appLE iX US UX hUSX)).Flat
this : Mono (pushoutSection ⋯ hUSX hUST ⋯)
⊢ Mono (X := pushout (Scheme.Hom.appLE f US UT hUST) (Scheme.Hom.appLE iX US UX hUSX))
    (Iso.hom (pushoutSymmetry (Scheme.Hom.appLE f US UT hUST) (Scheme.Hom.appLE iX US UX hUSX)) ≫
      pushoutSection H hUST hUSX hUY)
have h : Iso.hom (pushoutSymmetry (Scheme.Hom.appLE f US UT hUST) (Scheme.Hom.appLE iX US UX hUSX)) ≫
    pushoutSection H hUST hUSX hUY =
  pushoutSection sorry hUSX hUST sorry
Tactic: convert! this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Flat (goal)
Goal:
X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
inst : Flat f
hUS : IsAffineOpen US
hUT : IsCompact (↑UT : Set ↥T)
hUX : IsCompact (↑UX : Set ↥X)
hiX : (CommRingCat.Hom.hom (Scheme.Hom.appLE iX US UX hUSX)).Flat
⊢ Mono (pushoutSection H hUST hUSX hUY)
have suffices : Mono (pushoutSection sorry hUSX hUST sorry)
Tactic: suffices Mono (pushoutSection H.flip hUSX hUST (hUY.trans (inf_comm _ _))) by
    rw [← mono_comp_iff_of_isIso (pushoutSymmetry _ _).hom]; convert! this; cat_disch
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Flat (goal)
Goal:
X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
inst : Flat f
hUS : IsAffineOpen US
hUT : IsCompact (↑UT : Set ↥T)
hUT' : IsQuasiSeparated (↑UT : Set ↥T)
hUX : IsCompact (↑UX : Set ↥X)
hUX' : IsQuasiSeparated (↑UX : Set ↥X)
hiX : (CommRingCat.Hom.hom (Scheme.Hom.appLE iX US UX hUSX)).Flat
this : IsIso (pushoutSection ⋯ hUSX hUST ⋯)
⊢ IsIso (pushoutSection H hUST hUSX hUY)
have rw : IsIso (X := pushout (Scheme.Hom.appLE f US UT hUST) (Scheme.Hom.appLE iX US UX hUSX))
  (Iso.hom (pushoutSymmetry (Scheme.Hom.appLE f US UT hUST) (Scheme.Hom.appLE iX US UX hUSX)) ≫
    pushoutSection H hUST hUSX hUY)
Tactic: rw [← isIso_comp_left_iff (pushoutSymmetry _ _).hom]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Flat (goal)
Goal:
X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
inst : Flat f
hUS : IsAffineOpen US
hUT : IsCompact (↑UT : Set ↥T)
hUT' : IsQuasiSeparated (↑UT : Set ↥T)
hUX : IsCompact (↑UX : Set ↥X)
hUX' : IsQuasiSeparated (↑UX : Set ↥X)
hiX : (CommRingCat.Hom.hom (Scheme.Hom.appLE iX US UX hUSX)).Flat
this : IsIso (pushoutSection ⋯ hUSX hUST ⋯)
⊢ IsIso (X := pushout (Scheme.Hom.appLE f US UT hUST) (Scheme.Hom.appLE iX US UX hUSX))
    (Iso.hom (pushoutSymmetry (Scheme.Hom.appLE f US UT hUST) (Scheme.Hom.appLE iX US UX hUSX)) ≫
      pushoutSection H hUST hUSX hUY)
have h : Iso.hom (pushoutSymmetry (Scheme.Hom.appLE f US UT hUST) (Scheme.Hom.appLE iX US UX hUSX)) ≫
    pushoutSection H hUST hUSX hUY =
  pushoutSection sorry hUSX hUST sorry
Tactic: convert! this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Flat (goal)
Goal:
X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
inst : Flat f
hUS : IsAffineOpen US
hUT : IsCompact (↑UT : Set ↥T)
hUT' : IsQuasiSeparated (↑UT : Set ↥T)
hUX : IsCompact (↑UX : Set ↥X)
hUX' : IsQuasiSeparated (↑UX : Set ↥X)
hiX : (CommRingCat.Hom.hom (Scheme.Hom.appLE iX US UX hUSX)).Flat
⊢ IsIso (pushoutSection H hUST hUSX hUY)
have suffices : IsIso (pushoutSection sorry hUSX hUST sorry)
Tactic: suffices IsIso (pushoutSection H.flip hUSX hUST (hUY.trans (inf_comm _ _))) by
    rw [← isIso_comp_left_iff (pushoutSymmetry _ _).hom]; convert! this; cat_disch