awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R_1 S : Type u
inst : CommRing R_1
inst_1 : CommRing S
inst_2 : Finite ι
R : ι → CommRingCat
⊢ sigmaSpec R =
    Iso.hom
      (colimit.isoColimitCocone
        {
          cocone :=
            Functor.obj (Cocone.precompose (Iso.hom (Iso.symm Discrete.natIsoFunctor)))
              (Scheme.Spec.mapCocone (CommRingCat.piFan R).op),
          isColimit :=
            (Equiv.symm
                  (IsColimit.precomposeHomEquiv (Iso.symm Discrete.natIsoFunctor)
                    (Scheme.Spec.mapCocone (CommRingCat.piFan R).op)) :
                (a : IsColimit (Scheme.Spec.mapCocone (CommRingCat.piFan R).op)) →
                  IsColimit
                    ((Cocone.precompose Discrete.natIsoFunctor.symm.hom).obj
                      (Scheme.Spec.mapCocone (CommRingCat.piFan R).op)))
              (isColimitOfPreserves Scheme.Spec (Fan.IsLimit.op (CommRingCat.piFanIsLimit R))) })
have h : ∀ (b : ι),
  Sigma.ι (C := Scheme) (fun (i : ι) ↦ Spec (R i)) b ≫ sigmaSpec R =
    CategoryStruct.comp (Y := ∐ fun (i : ι) ↦ Spec (R i)) (Sigma.ι (C := Scheme) (fun (i : ι) ↦ Spec (R i)) b)
      (Iso.hom
        (colimit.isoColimitCocone
          {
            cocone :=
              Functor.obj (Cocone.precompose (Iso.hom (Iso.symm Discrete.natIsoFunctor)))
                (Scheme.Spec.mapCocone (CommRingCat.piFan R).op),
            isColimit :=
              (Equiv.symm
                    (IsColimit.precomposeHomEquiv (Iso.symm Discrete.natIsoFunctor)
                      (Scheme.Spec.mapCocone (CommRingCat.piFan R).op)) :
                  (a : IsColimit (Scheme.Spec.mapCocone (CommRingCat.piFan R).op)) →
                    IsColimit
                      ((Cocone.precompose Discrete.natIsoFunctor.symm.hom).obj
                        (Scheme.Spec.mapCocone (CommRingCat.piFan R).op)))
                (isColimitOfPreserves Scheme.Spec (Fan.IsLimit.op (CommRingCat.piFanIsLimit R))) }))
Tactic: ext1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R_1 S : Type u
inst : CommRing R_1
inst_1 : CommRing S
inst_2 : Finite ι
R : ι → CommRingCat
b : ι
⊢ Sigma.ι (C := Scheme) (fun (i : ι) ↦ Spec (R i)) b ≫ sigmaSpec R =
    CategoryStruct.comp (Y := ∐ fun (i : ι) ↦ Spec (R i)) (Sigma.ι (C := Scheme) (fun (i : ι) ↦ Spec (R i)) b)
      (Iso.hom
        (colimit.isoColimitCocone
          {
            cocone :=
              Functor.obj (Cocone.precompose (Iso.hom (Iso.symm Discrete.natIsoFunctor)))
                (Scheme.Spec.mapCocone (CommRingCat.piFan R).op),
            isColimit :=
              (Equiv.symm
                    (IsColimit.precomposeHomEquiv (Iso.symm Discrete.natIsoFunctor)
                      (Scheme.Spec.mapCocone (CommRingCat.piFan R).op)) :
                  (a : IsColimit (Scheme.Spec.mapCocone (CommRingCat.piFan R).op)) →
                    IsColimit
                      ((Cocone.precompose Discrete.natIsoFunctor.symm.hom).obj
                        (Scheme.Spec.mapCocone (CommRingCat.piFan R).op)))
                (isColimitOfPreserves Scheme.Spec (Fan.IsLimit.op (CommRingCat.piFanIsLimit R))) }))
have h : Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun (i : ι) ↦ (↑(R i) : Type u)) b)) =
  Spec.map ((CommRingCat.piFan R).proj b)
Tactic: simp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (hypothesis)
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R_1 S : Type u
inst : CommRing R_1
inst_1 : CommRing S
inst_2 : Finite ι
R : ι → CommRingCat
⊢ IsIso (sigmaSpec R)
have this : sigmaSpec R =
  Iso.hom
    (colimit.isoColimitCocone
      {
        cocone :=
          Functor.obj (Cocone.precompose (Iso.hom (Iso.symm Discrete.natIsoFunctor)))
            (Scheme.Spec.mapCocone (CommRingCat.piFan R).op),
        isColimit :=
          (Equiv.symm
                (IsColimit.precomposeHomEquiv (Iso.symm Discrete.natIsoFunctor)
                  (Scheme.Spec.mapCocone (CommRingCat.piFan R).op)) :
              (a : IsColimit (Scheme.Spec.mapCocone (CommRingCat.piFan R).op)) →
                IsColimit
                  ((Cocone.precompose Discrete.natIsoFunctor.symm.hom).obj
                    (Scheme.Spec.mapCocone (CommRingCat.piFan R).op)))
            (isColimitOfPreserves Scheme.Spec (Fan.IsLimit.op (CommRingCat.piFanIsLimit R))) })
Tactic: have : sigmaSpec R =
      (colimit.isoColimitCocone ⟨_,
        (IsColimit.precomposeHomEquiv Discrete.natIsoFunctor.symm _).symm (isColimitOfPreserves
          Scheme.Spec (Fan.IsLimit.op (CommRingCat.piFanIsLimit R)))⟩).hom := by
    ext1
    simp; rfl
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R_1 S : Type u
inst : CommRing R_1
inst_1 : CommRing S
inst_2 : Finite ι
R : ι → CommRingCat
this :
  sigmaSpec R =
    Iso.hom
      (colimit.isoColimitCocone
        {
          cocone :=
            Functor.obj (Cocone.precompose (Iso.hom (Iso.symm Discrete.natIsoFunctor)))
              (Scheme.Spec.mapCocone (CommRingCat.piFan R).op),
          isColimit :=
            (Equiv.symm
                  (IsColimit.precomposeHomEquiv (Iso.symm Discrete.natIsoFunctor)
                    (Scheme.Spec.mapCocone (CommRingCat.piFan R).op)) :
                (a : IsColimit (Scheme.Spec.mapCocone (CommRingCat.piFan R).op)) →
                  IsColimit
                    ((Cocone.precompose Discrete.natIsoFunctor.symm.hom).obj
                      (Scheme.Spec.mapCocone (CommRingCat.piFan R).op)))
              (isColimitOfPreserves Scheme.Spec (Fan.IsLimit.op (CommRingCat.piFanIsLimit R))) })
⊢ IsIso (sigmaSpec R)
have rw : IsIso (X := ∐ fun (i : ι) ↦ Spec (R i))
  (Iso.hom
    (colimit.isoColimitCocone
      {
        cocone :=
          Functor.obj (Cocone.precompose (Iso.hom (Iso.symm Discrete.natIsoFunctor)))
            (Scheme.Spec.mapCocone (CommRingCat.piFan R).op),
        isColimit :=
          (Equiv.symm
                (IsColimit.precomposeHomEquiv (Iso.symm Discrete.natIsoFunctor)
                  (Scheme.Spec.mapCocone (CommRingCat.piFan R).op)) :
              (a : IsColimit (Scheme.Spec.mapCocone (CommRingCat.piFan R).op)) →
                IsColimit
                  ((Cocone.precompose Discrete.natIsoFunctor.symm.hom).obj
                    (Scheme.Spec.mapCocone (CommRingCat.piFan R).op)))
            (isColimitOfPreserves Scheme.Spec (Fan.IsLimit.op (CommRingCat.piFanIsLimit R))) }))
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Finite σ
inst_3 : ∀ (i : σ), IsAffine.{u} (g i)
⊢ IsAffine.{u} (∐ g)
have obtain : ∀ (ι : Type u) (e : σ ≃ ι), IsAffine.{u} (∐ g)
Tactic: obtain ⟨ι, ⟨e⟩⟩ := Small.equiv_small.{u} (α := σ)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (hypothesis)
Goal:
ι_1 : Type u
f : ι_1 → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Finite σ
inst_3 : ∀ (i : σ), IsAffine.{u} (g i)
ι : Type u
e : σ ≃ ι
⊢ IsAffine.{u} (∐ g)
have this : Finite ι
Tactic: have : Finite ι := e.finite_iff.mp ‹_›
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
ι_1 : Type u
f : ι_1 → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Finite σ
inst_3 : ∀ (i : σ), IsAffine.{u} (g i)
ι : Type u
e : σ ≃ ι
this : Finite ι
i : ι
⊢ IsAffine.{u} ((g ∘ (⇑e.symm : (a : ι) → σ)) i)
have dsimp : IsAffine.{u} (g ((e.symm : (a : ι) → σ) i))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (hypothesis)
Goal:
ι_1 : Type u
f : ι_1 → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Finite σ
inst_3 : ∀ (i : σ), IsAffine.{u} (g i)
ι : Type u
e : σ ≃ ι
this : Finite ι
⊢ IsAffine.{u} (∐ g)
have this₁ : ∀ (i : ι), IsAffine.{u} ((g ∘ (⇑e.symm : (a : ι) → σ)) i)
Tactic: have (i : _) : IsAffine ((g ∘ e.symm) i) := by dsimp; infer_instance
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
ι : Type u
X : Scheme
inst : Finite ι
U : ι → X.Opens
hU : ∀ (i : ι), IsAffineOpen (U i)
hU' : _root_.Pairwise (Disjoint on U)
i j : ι
e : i ≠ j
⊢ Function.onFun (β := Set ↥X) Disjoint (fun (x : ι) ↦ Set.range (ι := ↥(↑(U x) : Scheme)) ⇑((fun (i : ι) ↦ (U i).ι) x))
    i j
have a : Function.onFun (β := Set ↥X) Disjoint (fun (x : ι) ↦ Set.range (ι := ↥(↑(U x) : Scheme)) ⇑((fun (i : ι) ↦ (U i).ι) x)) i
    j ↔
  (Disjoint on U) i j
Tactic: convert! hU' e using 0
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (hypothesis)
Goal:
ι : Type u
X : Scheme
inst : Finite ι
U : ι → X.Opens
hU : ∀ (i : ι), IsAffineOpen (U i)
hU' : _root_.Pairwise (Disjoint on U)
⊢ IsAffineOpen (iSup U)
have this : IsOpenImmersion.{u} (X := ∐ fun (i : ι) ↦ (↑(U i) : Scheme)) (Y := X) (Sigma.desc fun (i : ι) ↦ (U i).ι)
Tactic: have := isOpenImmersion_sigmaDesc _ (fun i ↦ (U i).ι)
    (fun i j e ↦ by convert! hU' e using 0; simp [← Opens.coe_disjoint])
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
ι : Type u
X : Scheme
inst : Finite ι
U : ι → X.Opens
hU : ∀ (i : ι), IsAffineOpen (U i)
hU' : _root_.Pairwise (Disjoint on U)
this : IsOpenImmersion.{u} (X := ∐ fun (i : ι) ↦ (↑(U i) : Scheme)) (Y := X) (Sigma.desc fun (i : ι) ↦ (U i).ι)
⊢ IsAffineOpen (iSup U)
have h : iSup U = Scheme.Hom.opensRange (X := ∐ fun (i : ι) ↦ (↑(U i) : Scheme)) (Sigma.desc fun (i : ι) ↦ (U i).ι)
Tactic: convert! isAffineOpen_opensRange (Sigma.desc fun i ↦ (U i).ι)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
ι : Type u
X : Scheme
inst : Finite ι
U : ι → X.Opens
hU : ∀ (i : ι), IsAffineOpen (U i)
hU' : _root_.Pairwise (Disjoint on U)
this : IsOpenImmersion.{u} (X := ∐ fun (i : ι) ↦ (↑(U i) : Scheme)) (Y := X) (Sigma.desc fun (i : ι) ↦ (U i).ι)
h : iSup U = Scheme.Hom.opensRange (X := ∐ fun (i : ι) ↦ (↑(U i) : Scheme)) (Sigma.desc fun (i : ι) ↦ (U i).ι)
⊢ IsAffineOpen (iSup U)
have convert! : IsAffine.{u} (∐ fun (i : ι) ↦ (↑(U i) : Scheme))
Tactic: convert! isAffineOpen_opensRange (Sigma.desc fun i ↦ (U i).ι)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
ι : Type u
X : Scheme
inst : Finite ι
U : ι → X.Opens
hU : ∀ (i : ι), IsAffineOpen (U i)
hU' : _root_.Pairwise (Disjoint on U)
this : IsOpenImmersion.{u} (X := ∐ fun (i : ι) ↦ (↑(U i) : Scheme)) (Y := X) (Sigma.desc fun (i : ι) ↦ (U i).ι)
⊢ iSup U = Scheme.Hom.opensRange (X := ∐ fun (i : ι) ↦ (↑(U i) : Scheme)) (Sigma.desc fun (i : ι) ↦ (U i).ι)
have h : ∀ (x : ↥X),
  x ∈ (↑(iSup U) : Set ↥X) ↔
    x ∈ (↑(Scheme.Hom.opensRange (X := ∐ fun (i : ι) ↦ (↑(U i) : Scheme)) (Sigma.desc fun (i : ι) ↦ (U i).ι)) : Set ↥X)
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (hypothesis)
Goal:
ι : Type u
X : Scheme
inst : Finite ι
U : ι → X.Opens
hU : ∀ (i : ι), IsAffineOpen (U i)
hU' : _root_.Pairwise (Disjoint on U)
this : IsOpenImmersion.{u} (X := ∐ fun (i : ι) ↦ (↑(U i) : Scheme)) (Y := X) (Sigma.desc fun (i : ι) ↦ (U i).ι)
⊢ IsAffine.{u} (∐ fun (i : ι) ↦ (↑(U i) : Scheme))
have this₁ : ∀ (i : ι), IsAffine.{u} (↑(U i) : Scheme)
Tactic: have (i : _) : IsAffine _ := hU i
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
σ : Type v
X : Scheme
inst : Finite σ
U : σ → X.Opens
hU : ∀ (i : σ), IsAffineOpen (U i)
hU' : _root_.Pairwise (Disjoint on U)
⊢ IsAffineOpen (iSup U)
have obtain : ∀ (ι : Type u) (e : σ ≃ ι), IsAffineOpen (iSup U)
Tactic: obtain ⟨ι, ⟨e⟩⟩ := Small.equiv_small.{u} (α := σ)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (hypothesis)
Goal:
σ : Type v
X : Scheme
inst : Finite σ
U : σ → X.Opens
hU : ∀ (i : σ), IsAffineOpen (U i)
hU' : _root_.Pairwise (Disjoint on U)
ι : Type u
e : σ ≃ ι
⊢ IsAffineOpen (iSup U)
have this : Finite ι
Tactic: have : Finite ι := e.finite_iff.mp ‹_›
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
σ : Type v
X : Scheme
inst : Finite σ
U : σ → X.Opens
hU : ∀ (i : σ), IsAffineOpen (U i)
hU' : _root_.Pairwise (Disjoint on U)
ι : Type u
e : σ ≃ ι
this : Finite ι
⊢ IsAffineOpen (iSup U)
have rw : IsAffineOpen.{u} (X := X) (⨆ (x : ι), U ((e.symm : (a : ι) → σ) x))
Tactic: rw [← e.symm.iSup_congr fun _ ↦ rfl]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
σ : Type v
X : Scheme
s : Set σ
hs : s.Finite
U : σ → X.Opens
hU : ∀ i ∈ s, IsAffineOpen (U i)
hU' : s.Pairwise (Disjoint on U)
⊢ IsAffineOpen.{u} (X := X) (⨆ i ∈ s, U i)
have rw : IsAffineOpen.{u} (X := X) (⨆ (i : (↑s : Type v)), U (↑i : σ))
Tactic: rw [← iSup_subtype'']
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (hypothesis)
Goal:
σ : Type v
X : Scheme
s : Set σ
hs : s.Finite
U : σ → X.Opens
hU : ∀ i ∈ s, IsAffineOpen (U i)
hU' : s.Pairwise (Disjoint on U)
⊢ IsAffineOpen.{u} (X := X) (⨆ (i : (↑s : Type v)), U (↑i : σ))
have this : Finite.{v + 1} (↑s : Type v)
Tactic: have := hs.to_subtype
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
X : Scheme
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
H : Disjoint U V
⊢ IsAffineOpen (U ⊔ V)
have h : U ⊔ V = ⨆ (i : Unit ⊕ Unit), Sum.elim (fun (x : Unit) ↦ U) (fun (x : Unit) ↦ V) i
Tactic: convert!
    iSup_of_disjoint (U := fun i : Unit ⊕ Unit ↦ i.elim (fun _ ↦ U) (fun _ ↦ V)) (by simp_all)
      (by simp_all [_root_.Pairwise, Unique.forall_iff, ← Opens.coe_disjoint, disjoint_comm])
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Finite.{u + 1} ↥X
inst_3 : DiscreteTopology.{u} ↥X
this : IsAffineOpen.{u} (X := X) (⨆ (x : ↥X), { carrier := {x}, is_open' := ⋯ })
⊢ IsAffineOpen.{u} (X := X) ⊤
have h : Eq.{u + 1} (α := X.Opens) ⊤ (⨆ (x : ↥X), { carrier := {x}, is_open' := sorry })
Tactic: convert! this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Finite.{u + 1} ↥X
inst_3 : DiscreteTopology.{u} ↥X
this : IsAffineOpen.{u} (X := X) (⨆ (x : ↥X), { carrier := {x}, is_open' := ⋯ })
⊢ Eq.{u + 1} (α := X.Opens) ⊤ (⨆ (x : ↥X), { carrier := {x}, is_open' := ⋯ })
have h : ∀ (x : ↥X), x ∈ (↑⊤ : Set ↥X) ↔ x ∈ (↑(⨆ (x : ↥X), { carrier := {x}, is_open' := sorry : Opens ↥X }) : Set ↥X)
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
U X Y : Scheme
f : U ⟶ X
g : U ⟶ Y
inst : IsOpenImmersion f
inst_1 : IsOpenImmersion g
i : WalkingPair
⊢ Mono ((span f g ⋙ Scheme.forget).map (WidePushoutShape.Hom.init i))
have rw : Function.Injective (α := (fun (X : Type u_1) ↦ X) ((span f g ⋙ Scheme.forget).obj none)) (β :=
  (fun (X : Type u_1) ↦ X) ((span f g ⋙ Scheme.forget).obj (some i)))
  (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) ((span f g ⋙ Scheme.forget).map (WidePushoutShape.Hom.init i))) :
    (a : (fun (X : Type u_1) ↦ X) ((span f g ⋙ Scheme.forget).obj none)) →
      (fun (X : Type u_1) ↦ X) ((span f g ⋙ Scheme.forget).obj (some i)))
Tactic: rw [mono_iff_injective]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
U X Y : Scheme
f : U ⟶ X
g : U ⟶ Y
inst : IsOpenImmersion f
inst_1 : IsOpenImmersion g
i : WalkingPair
⊢ Function.Injective (α := (fun (X : Type u_1) ↦ X) ((span f g ⋙ Scheme.forget).obj none)) (β :=
    (fun (X : Type u_1) ↦ X) ((span f g ⋙ Scheme.forget).obj (some i)))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) ((span f g ⋙ Scheme.forget).map (WidePushoutShape.Hom.init i))) :
      (a : (fun (X : Type u_1) ↦ X) ((span f g ⋙ Scheme.forget).obj none)) →
        (fun (X : Type u_1) ↦ X) ((span f g ⋙ Scheme.forget).obj (some i)))
have left : Function.Injective (α := (fun (X : Type u_1) ↦ X) ((span f g ⋙ Scheme.forget).obj none)) (β :=
  (fun (X : Type u_1) ↦ X) ((span f g ⋙ Scheme.forget).obj (some WalkingPair.left)))
  (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
        ((span f g ⋙ Scheme.forget).map (WidePushoutShape.Hom.init WalkingPair.left))) :
    (a : (fun (X : Type u_1) ↦ X) ((span f g ⋙ Scheme.forget).obj none)) →
      (fun (X : Type u_1) ↦ X) ((span f g ⋙ Scheme.forget).obj (some WalkingPair.left)))
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
U X Y : Scheme
f : U ⟶ X
g : U ⟶ Y
inst : IsOpenImmersion f
inst_1 : IsOpenImmersion g
i : WalkingPair
left :
  Function.Injective (α := (fun (X : Type u_1) ↦ X) ((span f g ⋙ Scheme.forget).obj none)) (β :=
    (fun (X : Type u_1) ↦ X) ((span f g ⋙ Scheme.forget).obj (some WalkingPair.left)))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
          ((span f g ⋙ Scheme.forget).map (WidePushoutShape.Hom.init WalkingPair.left))) :
      (a : (fun (X : Type u_1) ↦ X) ((span f g ⋙ Scheme.forget).obj none)) →
        (fun (X : Type u_1) ↦ X) ((span f g ⋙ Scheme.forget).obj (some WalkingPair.left)))
⊢ Function.Injective (α := (fun (X : Type u_1) ↦ X) ((span f g ⋙ Scheme.forget).obj none)) (β :=
    (fun (X : Type u_1) ↦ X) ((span f g ⋙ Scheme.forget).obj (some i)))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) ((span f g ⋙ Scheme.forget).map (WidePushoutShape.Hom.init i))) :
      (a : (fun (X : Type u_1) ↦ X) ((span f g ⋙ Scheme.forget).obj none)) →
        (fun (X : Type u_1) ↦ X) ((span f g ⋙ Scheme.forget).obj (some i)))
have right : Function.Injective (α := (fun (X : Type u_1) ↦ X) ((span f g ⋙ Scheme.forget).obj none)) (β :=
  (fun (X : Type u_1) ↦ X) ((span f g ⋙ Scheme.forget).obj (some WalkingPair.right)))
  (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
        ((span f g ⋙ Scheme.forget).map (WidePushoutShape.Hom.init WalkingPair.right))) :
    (a : (fun (X : Type u_1) ↦ X) ((span f g ⋙ Scheme.forget).obj none)) →
      (fun (X : Type u_1) ↦ X) ((span f g ⋙ Scheme.forget).obj (some WalkingPair.right)))
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
U X Y : Scheme
f : U ⟶ X
g : U ⟶ Y
inst : IsOpenImmersion f
inst_1 : IsOpenImmersion g
i j : WalkingSpan
t : i ⟶ j
⊢ IsOpenImmersion ((span f g).map t)
have id : IsOpenImmersion ((span f g).map (WidePushoutShape.Hom.id i))
Tactic: obtain (a | (a | a)) := t
Cleared hypotheses: j, t
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
U X Y : Scheme
f : U ⟶ X
g : U ⟶ Y
inst : IsOpenImmersion f
inst_1 : IsOpenImmersion g
i j : WalkingSpan
t : i ⟶ j
id : IsOpenImmersion ((span f g).map (WidePushoutShape.Hom.id i))
⊢ IsOpenImmersion ((span f g).map t)
have init : IsOpenImmersion ((span f g).map (WidePushoutShape.Hom.init WalkingPair.left))
Tactic: obtain (a | (a | a)) := t
Cleared hypotheses: i, j, t
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
U X Y : Scheme
f : U ⟶ X
g : U ⟶ Y
inst : IsOpenImmersion f
inst_1 : IsOpenImmersion g
i j : WalkingSpan
t : i ⟶ j
id : IsOpenImmersion ((span f g).map (WidePushoutShape.Hom.id i))
init : IsOpenImmersion ((span f g).map (WidePushoutShape.Hom.init WalkingPair.left))
⊢ IsOpenImmersion ((span f g).map t)
have init₁ : IsOpenImmersion ((span f g).map (WidePushoutShape.Hom.init WalkingPair.right))
Tactic: obtain (a | (a | a)) := t
Cleared hypotheses: i, j, t
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
U X Y : Scheme
f : U ⟶ X
g : U ⟶ Y
inst : IsOpenImmersion f
inst_1 : IsOpenImmersion g
i : WalkingSpan
⊢ IsOpenImmersion ((span f g).map (WidePushoutShape.Hom.id i))
have id : IsOpenImmersion (𝟙 ((span f g).obj i))
Tactic: simp only [WidePushoutShape.hom_id, CategoryTheory.Functor.map_id]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (hypothesis)
Goal:
I : Type u_1
inst : Category.{v_1, u_1} I
D : CategoryTheory.Functor.{v_1, u, u_1, u + 1} I Scheme
c : Cone D
hc : IsLimit c
inst_1 : ∀ (i : I), IsAffine.{u} (D.obj i)
α : D ⟶ (D ⋙ Γ.rightOp) ⋙ Scheme.Spec := D.whiskerLeft ΓSpec.adjunction.unit
⊢ IsAffine.{u} c.pt
have this : ∀ (i : I), IsIso (α.app i)
Tactic: have (i : _) : IsIso (α.app i) := IsAffine.affine
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (hypothesis)
Goal:
I : Type u_1
inst : Category.{v_1, u_1} I
D : CategoryTheory.Functor.{v_1, u, u_1, u + 1} I Scheme
c : Cone D
hc : IsLimit c
inst_1 : ∀ (i : I), IsAffine.{u} (D.obj i)
α : D ⟶ (D ⋙ Γ.rightOp) ⋙ Scheme.Spec := D.whiskerLeft ΓSpec.adjunction.unit
this : ∀ (i : I), IsIso (α.app i)
⊢ IsAffine.{u} c.pt
have this₁ : IsIso α
Tactic: have : IsIso α := NatIso.isIso_of_isIso_app α
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
I : Type u_1
inst : Category.{v_1, u_1} I
D : CategoryTheory.Functor.{v_1, u, u_1, u + 1} I Scheme
c : Cone D
hc : IsLimit c
inst_1 : ∀ (i : I), IsAffine.{u} (D.obj i)
α : D ⟶ (D ⋙ Γ.rightOp) ⋙ Scheme.Spec := D.whiskerLeft ΓSpec.adjunction.unit
this_1 : ∀ (i : I), IsIso (α.app i)
this : IsIso α
⊢ IsAffine.{u} c.pt
have have : ∀ (this : c.pt ≅ Spec Γ(c.pt, ⊤)), IsAffine.{u} c.pt
Tactic: have : c.pt ≅ Spec Γ(c.pt, ⊤) := hc.conePointUniqueUpToIso ((IsLimit.postcomposeHomEquiv
    (asIso α).symm _).symm (isLimitOfPreserves (Scheme.Γ.rightOp ⋙ Scheme.Spec) hc))
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.LimitsOver (goal)
Goal:
X_1 : Scheme
P : MorphismProperty Scheme
S : Scheme
U X Y : P.Over ⊤ S
f : U ⟶ X
g : U ⟶ Y
inst : IsOpenImmersion f.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left
inst_1 : IsOpenImmersion g.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left
i : WalkingPair
⊢ Mono
    ((span f g ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).map (WidePushoutShape.Hom.init i))
have rw : Function.Injective (α :=
  (fun (X : Type u) ↦ X) ((span f g ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).obj none))
  (β :=
  (fun (X : Type u) ↦ X) ((span f g ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).obj (some i)))
  (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
        ((span f g ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).map
          (WidePushoutShape.Hom.init i))) :
    (a :
        (fun (X : Type u) ↦ X)
          ((span f g ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).obj none)) →
      (fun (X : Type u) ↦ X)
        ((span f g ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).obj (some i)))
Tactic: rw [mono_iff_injective]