awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
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)

Tactic:
obtain ⟨I, hI, e⟩ := isCompact_iff_finite_and_eq_biUnion_affineOpens.mp hUX

Premises used: Iff.mp, AlgebraicGeometry.isCompact_iff_finite_and_eq_biUnion_affineOpens
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
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)
I : Set (↑X.affineOpens : Type u)
hI : I.Finite
e : UX = ⨆ i ∈ I, (↑i : X.Opens)
⊢ Finite.{u + 1} (↑I : Type u)

Tactic:
have := hI.to_subtype
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
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)
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
rwa₁ rwa₂ rwa₃ 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)
⊢ ⨆ (x : (↑I : Type u)), (↑(↑x : (↑X.affineOpens : Type u)) : X.Opens) = UX

Tactic:
rwa [iSup_subtype, eq_comm]

Premises used: iSup_subtype, eq_comm
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
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)
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:
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 _)

Premises used: AlgebraicGeometry.mono_pushoutSection_of_iSup_eq, inferInstance, AlgebraicGeometry.mono_pushoutSection_of_iSup_eq._proof_2, AlgebraicGeometry.Scheme.Hom.flat_appLE, Subtype.val, rfl, Subtype.property, AlgebraicGeometry.isIso_pushoutSection_of_isAffineOpen
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
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)
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)
⊢ 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 _)

Premises used: Iff.mp, AlgebraicGeometry.isCompact_iff_finite_and_eq_biUnion_affineOpens
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
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 ⋯)
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)
⊢ Mono (pushoutSection H hUST hUSX hUY)

Tactic:
rw [← mono_comp_iff_of_isIso (pushoutSymmetry _ _).hom]

Premises used: CategoryTheory.Limits.pushoutSymmetry, CategoryTheory.Iso.hom, CategoryTheory.mono_comp_iff_of_isIso
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
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 ⋯ hUSX hUST ⋯)

Tactic:
this
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
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 ⋯)
h :
  Iso.hom (pushoutSymmetry (Scheme.Hom.appLE f US UT hUST) (Scheme.Hom.appLE iX US UX hUSX)) ≫
      pushoutSection H hUST hUSX hUY =
    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)

Tactic:
convert! this
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
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)
suffices : Mono (pushoutSection ⋯ hUSX hUST ⋯)
⊢ Mono (pushoutSection H hUST hUSX hUY)

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
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
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 ⋯ hUSX hUST ⋯)

Tactic:
mono_pushoutSection_of_isCompact_of_flat_right _ _ _ _ hUS hUX hUT

Premises used: AlgebraicGeometry.mono_pushoutSection_of_isCompact_of_flat_right
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
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 ⋯ hUSX hUST ⋯)

Tactic:
exact mono_pushoutSection_of_isCompact_of_flat_right _ _ _ _ hUS hUX hUT

Premises used: AlgebraicGeometry.mono_pushoutSection_of_isCompact_of_flat_right
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
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)

Tactic:
obtain ⟨I, hI, e⟩ := isCompact_iff_finite_and_eq_biUnion_affineOpens.mp hUX

Premises used: Iff.mp, AlgebraicGeometry.isCompact_iff_finite_and_eq_biUnion_affineOpens
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
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)
rw : (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens) ≤ ⨆ i ∈ I, (↑i : X.Opens)
⊢ (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens) ≤ UX

Tactic:
rw [e]
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
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_1 : (↑I : Type u)
i : ↥X
⊢ i ∈ (↑(↑i_1 : (↑X.affineOpens : Type u)) : X.Opens) → Membership.mem (γ := Opens ↥X) (⨆ i ∈ I, (↑i : X.Opens)) i

Tactic:
aesop
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
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

Tactic:
have hIUX (i : I) : i.1 ≤ UX := by rw [e]; intro i; aesop
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
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
⊢ Finite.{u + 1} (↑I : Type u)

Tactic:
have := hI.to_subtype
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
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
rwa₁ rwa₂ rwa₃ 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)
⊢ ⨆ (i : (↑I : Type u)), (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens) = UX

Tactic:
rwa [iSup_subtype,
    eq_comm]

Premises used: iSup_subtype, eq_comm
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
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)
⊢ IsIso (pushoutSection H hUST hUSX hUY)

Tactic:
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 _)

Premises used: AlgebraicGeometry.IsAffineOpen.isCompact, AlgebraicGeometry.isIso_pushoutSection_of_iSup_eq._proof_3, AlgebraicGeometry.isIso_pushoutSection_of_iSup_eq, SetLike.coe, AlgebraicGeometry.isIso_pushoutSection_of_iSup_eq._proof_2, AlgebraicGeometry.mono_pushoutSection_of_isCompact_of_flat_right, TopologicalSpace.Opens.is_open', inf_le_left, LE.le.trans, AlgebraicGeometry.Scheme.Hom.flat_appLE, Subtype.val, rfl, Subtype.property, AlgebraicGeometry.isIso_pushoutSection_of_isAffineOpen
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
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)
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)
⊢ 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 _)

Premises used: Iff.mp, AlgebraicGeometry.isCompact_iff_finite_and_eq_biUnion_affineOpens
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
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 ⋯)
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)
⊢ IsIso (pushoutSection H hUST hUSX hUY)

Tactic:
rw [← isIso_comp_left_iff (pushoutSymmetry _ _).hom]

Premises used: CategoryTheory.isIso_comp_left_iff, CategoryTheory.Limits.pushoutSymmetry, CategoryTheory.Iso.hom
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
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 ⋯ hUSX hUST ⋯)

Tactic:
this
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
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 ⋯)
h :
  Iso.hom (pushoutSymmetry (Scheme.Hom.appLE f US UT hUST) (Scheme.Hom.appLE iX US UX hUSX)) ≫
      pushoutSection H hUST hUSX hUY =
    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)

Tactic:
convert! this
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
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)
suffices : IsIso (pushoutSection ⋯ hUSX hUST ⋯)
⊢ IsIso (pushoutSection H hUST hUSX hUY)

Tactic:
suffices IsIso (pushoutSection H.flip hUSX hUST (hUY.trans (inf_comm _ _))) by
    rw [← isIso_comp_left_iff (pushoutSymmetry _ _).hom]; convert! this; cat_disch
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
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 ⋯ hUSX hUST ⋯)

Tactic:
isIso_pushoutSection_of_isQuasiSeparated_of_flat_right _ _ _ _ hUS hUX hUT hUT'

Premises used: AlgebraicGeometry.isIso_pushoutSection_of_isQuasiSeparated_of_flat_right
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
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 ⋯ hUSX hUST ⋯)

Tactic:
exact isIso_pushoutSection_of_isQuasiSeparated_of_flat_right _ _ _ _ hUS hUX hUT hUT'

Premises used: AlgebraicGeometry.isIso_pushoutSection_of_isQuasiSeparated_of_flat_right
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
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
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)

Tactic:
obtain ⟨I, hI, e⟩ := isCompact_iff_finite_and_eq_biUnion_affineOpens.mp hUX

Premises used: Iff.mp, AlgebraicGeometry.isCompact_iff_finite_and_eq_biUnion_affineOpens
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
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)
⊢ Finite.{u + 1} (↑I : Type u)

Tactic:
have := hI.to_subtype
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
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
rwa₁ rwa₂ rwa₃ 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)
⊢ ⨆ (i : (↑I : Type u)), (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens) = UX

Tactic:
rwa [iSup_subtype, eq_comm]

Premises used: iSup_subtype, eq_comm
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
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)
⊢ Mono (pushoutSection H hUST hUSX hUY)

Tactic:
exact mono_pushoutSection_of_iSup_eq _ _ _ _ (fun i : I ↦ i) (by rwa [iSup_subtype, eq_comm])
    (fun i ↦ mono_pushoutSection_of_isCompact_of_flat_left _ _ _ _ hUS i.1.2 hUT) hf
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
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 ⋯)
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)
⊢ Mono (pushoutSection H hUST hUSX hUY)

Tactic:
rw [← mono_comp_iff_of_isIso (pushoutSymmetry _ _).hom]

Premises used: CategoryTheory.Limits.pushoutSymmetry, CategoryTheory.Iso.hom, CategoryTheory.mono_comp_iff_of_isIso