mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.QuasiAffine

Goal state before:
pp: case refine_2
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsAffineHom f
inst✝ : Y.IsQuasiAffine
this✝¹ : CompactSpace ↥X
this✝ : X.IsQuasiAffine
this :
  ∀ (r : ↑Γ(Y, ⊤)),
    IsPushout (Hom.appTop f) (Y.presheaf.map (homOfLE ⋯).op) (X.presheaf.map (homOfLE ⋯).op)
      (Hom.appLE f (Y.basicOpen r) (X.basicOpen ((ConcreteCategory.hom (Hom.appTop f)) r)) ⋯)
r : Y.openCoverBasicOpenTop.toPreZeroHypercover.1
e : pullback f (Y.basicOpen ↑r).ι ≅ Spec Γ(X, X.basicOpen ((ConcreteCategory.hom (Hom.appTop f)) ↑r)) :=
  pullbackRestrictIsoRestrict f (Y.basicOpen ↑r) ≪≫ X.isoOfEq ⋯ ≪≫ ⋯.isoSpec
⊢ Scheme.Spec.map (X.presheaf.map (homOfLE ⋯).op).op ≫ (Iso.refl (Scheme.Spec.obj (Opposite.op Γ(X, ⊤)))).hom =
    e.symm.hom ≫ (Precoverage.ZeroHypercover.pullback₁ f Y.openCoverBasicOpenTop).f r ≫ X.toSpecΓ

Tactic:
·

Goal state after:
case refine_2
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsAffineHom f
inst✝ : Y.IsQuasiAffine
this✝¹ : CompactSpace ↥X
this✝ : X.IsQuasiAffine
this :
  ∀ (r : ↑Γ(Y, ⊤)),
    IsPushout (Hom.appTop f) (Y.presheaf.map (homOfLE ⋯).op) (X.presheaf.map (homOfLE ⋯).op)
      (Hom.appLE f (Y.basicOpen r) (X.basicOpen ((ConcreteCategory.hom (Hom.appTop f)) r)) ⋯)
r : Y.openCoverBasicOpenTop.toPreZeroHypercover.1
e : pullback f (Y.basicOpen ↑r).ι ≅ Spec Γ(X, X.basicOpen ((ConcreteCategory.hom (Hom.appTop f)) ↑r)) :=
  pullbackRestrictIsoRestrict f (Y.basicOpen ↑r) ≪≫ X.isoOfEq ⋯ ≪≫ ⋯.isoSpec
⊢ Scheme.Spec.map (X.presheaf.map (homOfLE ⋯).op).op ≫ (Iso.refl (Scheme.Spec.obj (Opposite.op Γ(X, ⊤)))).hom =
    e.symm.hom ≫ (Precoverage.ZeroHypercover.pullback₁ f Y.openCoverBasicOpenTop).f r ≫ X.toSpecΓ
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: case h₁
n : Type u
S X : Scheme
inst✝ : X.Over S
f : { f // Scheme.Hom.IsOver f S }
⊢ ↑((fun v ↦ ⟨homOfVector (X ↘ S) v, ⋯⟩) ((fun f i ↦ (ConcreteCategory.hom (Scheme.Hom.appTop ↑f)) (coord S i)) f)) ≫
      𝔸(n; S) ↘ S =
    ↑f ≫ 𝔸(n; S) ↘ S

pp: case h₂
n : Type u
S X : Scheme
inst✝ : X.Over S
f : { f // Scheme.Hom.IsOver f S }
i✝ : n
⊢ (ConcreteCategory.hom
        (Scheme.Hom.appTop
          ↑((fun v ↦ ⟨homOfVector (X ↘ S) v, ⋯⟩)
              ((fun f i ↦ (ConcreteCategory.hom (Scheme.Hom.appTop ↑f)) (coord S i)) f))))
      (coord S i✝) =
    (ConcreteCategory.hom (Scheme.Hom.appTop ↑f)) (coord S i✝)

Tactic:
·

Goal state after:
case h₁
n : Type u
S X : Scheme
inst✝ : X.Over S
f : { f // Scheme.Hom.IsOver f S }
⊢ ↑((fun v ↦ ⟨homOfVector (X ↘ S) v, ⋯⟩) ((fun f i ↦ (ConcreteCategory.hom (Scheme.Hom.appTop ↑f)) (coord S i)) f)) ≫
      𝔸(n; S) ↘ S =
    ↑f ≫ 𝔸(n; S) ↘ S
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: case h₂
n : Type u
S X : Scheme
inst✝ : X.Over S
f : { f // Scheme.Hom.IsOver f S }
i✝ : n
⊢ (ConcreteCategory.hom
        (Scheme.Hom.appTop
          ↑((fun v ↦ ⟨homOfVector (X ↘ S) v, ⋯⟩)
              ((fun f i ↦ (ConcreteCategory.hom (Scheme.Hom.appTop ↑f)) (coord S i)) f))))
      (coord S i✝) =
    (ConcreteCategory.hom (Scheme.Hom.appTop ↑f)) (coord S i✝)

Tactic:
·

Goal state after:
case h₂
n : Type u
S X : Scheme
inst✝ : X.Over S
f : { f // Scheme.Hom.IsOver f S }
i✝ : n
⊢ (ConcreteCategory.hom
        (Scheme.Hom.appTop
          ↑((fun v ↦ ⟨homOfVector (X ↘ S) v, ⋯⟩)
              ((fun f i ↦ (ConcreteCategory.hom (Scheme.Hom.appTop ↑f)) (coord S i)) f))))
      (coord S i✝) =
    (ConcreteCategory.hom (Scheme.Hom.appTop ↑f)) (coord S i✝)
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: case h₁
n : Type u
S : Scheme
inst✝ : IsAffine S
⊢ ((𝔸(n; S).toSpecΓ ≫
          Spec.map (CommRingCat.ofHom (eval₂Hom (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝔸(n; S) ↘ S))) (coord S)))) ≫
        homOfVector (Spec.map (CommRingCat.ofHom C) ≫ S.isoSpec.inv)
          (⇑(ConcreteCategory.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑Γ(S, ⊤)))).inv) ∘ X)) ≫
      𝔸(n; S) ↘ S =
    𝟙 𝔸(n; S) ≫ 𝔸(n; S) ↘ S

pp: case h₂
n : Type u
S : Scheme
inst✝ : IsAffine S
i✝ : n
⊢ (ConcreteCategory.hom
        (Scheme.Hom.appTop
          ((𝔸(n; S).toSpecΓ ≫
              Spec.map
                (CommRingCat.ofHom (eval₂Hom (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝔸(n; S) ↘ S))) (coord S)))) ≫
            homOfVector (Spec.map (CommRingCat.ofHom C) ≫ S.isoSpec.inv)
              (⇑(ConcreteCategory.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑Γ(S, ⊤)))).inv) ∘ X))))
      (coord S i✝) =
    (ConcreteCategory.hom (Scheme.Hom.appTop (𝟙 𝔸(n; S)))) (coord S i✝)

Tactic:
·

Goal state after:
case h₁
n : Type u
S : Scheme
inst✝ : IsAffine S
⊢ ((𝔸(n; S).toSpecΓ ≫
          Spec.map (CommRingCat.ofHom (eval₂Hom (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝔸(n; S) ↘ S))) (coord S)))) ≫
        homOfVector (Spec.map (CommRingCat.ofHom C) ≫ S.isoSpec.inv)
          (⇑(ConcreteCategory.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑Γ(S, ⊤)))).inv) ∘ X)) ≫
      𝔸(n; S) ↘ S =
    𝟙 𝔸(n; S) ≫ 𝔸(n; S) ↘ S
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: case h₂
n : Type u
S : Scheme
inst✝ : IsAffine S
i✝ : n
⊢ (ConcreteCategory.hom
        (Scheme.Hom.appTop
          ((𝔸(n; S).toSpecΓ ≫
              Spec.map
                (CommRingCat.ofHom (eval₂Hom (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝔸(n; S) ↘ S))) (coord S)))) ≫
            homOfVector (Spec.map (CommRingCat.ofHom C) ≫ S.isoSpec.inv)
              (⇑(ConcreteCategory.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑Γ(S, ⊤)))).inv) ∘ X))))
      (coord S i✝) =
    (ConcreteCategory.hom (Scheme.Hom.appTop (𝟙 𝔸(n; S)))) (coord S i✝)

Tactic:
·

Goal state after:
case h₂
n : Type u
S : Scheme
inst✝ : IsAffine S
i✝ : n
⊢ (ConcreteCategory.hom
        (Scheme.Hom.appTop
          ((𝔸(n; S).toSpecΓ ≫
              Spec.map
                (CommRingCat.ofHom (eval₂Hom (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝔸(n; S) ↘ S))) (coord S)))) ≫
            homOfVector (Spec.map (CommRingCat.ofHom C) ≫ S.isoSpec.inv)
              (⇑(ConcreteCategory.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑Γ(S, ⊤)))).inv) ∘ X))))
      (coord S i✝) =
    (ConcreteCategory.hom (Scheme.Hom.appTop (𝟙 𝔸(n; S)))) (coord S i✝)
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: case hC
n : Type u
S : Scheme
inst✝ : IsAffine S
⊢ (CommRingCat.Hom.hom
          (CommRingCat.ofHom (eval₂Hom (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝔸(n; S) ↘ S))) (coord S)) ≫
            Scheme.Hom.app
              (homOfVector (Spec.map (CommRingCat.ofHom C) ≫ S.isoSpec.inv)
                (⇑(ConcreteCategory.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑Γ(S, ⊤)))).inv) ∘ X))
              ⊤)).comp
      C =
    (CommRingCat.Hom.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑Γ(S, ⊤)))).inv).comp C

pp: case hX
n : Type u
S : Scheme
inst✝ : IsAffine S
⊢ ∀ (i : n),
    (CommRingCat.Hom.hom
          (CommRingCat.ofHom (eval₂Hom (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝔸(n; S) ↘ S))) (coord S)) ≫
            Scheme.Hom.app
              (homOfVector (Spec.map (CommRingCat.ofHom C) ≫ S.isoSpec.inv)
                (⇑(ConcreteCategory.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑Γ(S, ⊤)))).inv) ∘ X))
              ⊤))
        (X i) =
      (CommRingCat.Hom.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑Γ(S, ⊤)))).inv) (X i)

Tactic:
·

Goal state after:
case hC
n : Type u
S : Scheme
inst✝ : IsAffine S
⊢ (CommRingCat.Hom.hom
          (CommRingCat.ofHom (eval₂Hom (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝔸(n; S) ↘ S))) (coord S)) ≫
            Scheme.Hom.app
              (homOfVector (Spec.map (CommRingCat.ofHom C) ≫ S.isoSpec.inv)
                (⇑(ConcreteCategory.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑Γ(S, ⊤)))).inv) ∘ X))
              ⊤)).comp
      C =
    (CommRingCat.Hom.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑Γ(S, ⊤)))).inv).comp C
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: case hX
n : Type u
S : Scheme
inst✝ : IsAffine S
⊢ ∀ (i : n),
    (CommRingCat.Hom.hom
          (CommRingCat.ofHom (eval₂Hom (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝔸(n; S) ↘ S))) (coord S)) ≫
            Scheme.Hom.app
              (homOfVector (Spec.map (CommRingCat.ofHom C) ≫ S.isoSpec.inv)
                (⇑(ConcreteCategory.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑Γ(S, ⊤)))).inv) ∘ X))
              ⊤))
        (X i) =
      (CommRingCat.Hom.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑Γ(S, ⊤)))).inv) (X i)

Tactic:
·

Goal state after:
case hX
n : Type u
S : Scheme
inst✝ : IsAffine S
⊢ ∀ (i : n),
    (CommRingCat.Hom.hom
          (CommRingCat.ofHom (eval₂Hom (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝔸(n; S) ↘ S))) (coord S)) ≫
            Scheme.Hom.app
              (homOfVector (Spec.map (CommRingCat.ofHom C) ≫ S.isoSpec.inv)
                (⇑(ConcreteCategory.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑Γ(S, ⊤)))).inv) ∘ X))
              ⊤))
        (X i) =
      (CommRingCat.Hom.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑Γ(S, ⊤)))).inv) (X i)
Module: Mathlib.CategoryTheory.Limits.Types.ColimitTypeFiltered

Goal state before:
pp: case mp
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFiltered J
F : J ⥤ Type w₀
x y : (j : J) × F.obj j
⊢ Relation.EqvGen F.ColimitTypeRel x y →
    ∃ k f g, (ConcreteCategory.hom (F.map f)) x.snd = (ConcreteCategory.hom (F.map g)) y.snd

pp: case mpr
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFiltered J
F : J ⥤ Type w₀
x y : (j : J) × F.obj j
⊢ (∃ k f g, (ConcreteCategory.hom (F.map f)) x.snd = (ConcreteCategory.hom (F.map g)) y.snd) →
    Relation.EqvGen F.ColimitTypeRel x y

Tactic:
·

Goal state after:
case mp
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFiltered J
F : J ⥤ Type w₀
x y : (j : J) × F.obj j
⊢ Relation.EqvGen F.ColimitTypeRel x y →
    ∃ k f g, (ConcreteCategory.hom (F.map f)) x.snd = (ConcreteCategory.hom (F.map g)) y.snd
Module: Mathlib.CategoryTheory.Limits.Types.ColimitTypeFiltered

Goal state before:
pp: case mpr
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFiltered J
F : J ⥤ Type w₀
x y : (j : J) × F.obj j
⊢ (∃ k f g, (ConcreteCategory.hom (F.map f)) x.snd = (ConcreteCategory.hom (F.map g)) y.snd) →
    Relation.EqvGen F.ColimitTypeRel x y

Tactic:
·

Goal state after:
case mpr
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFiltered J
F : J ⥤ Type w₀
x y : (j : J) × F.obj j
⊢ (∃ k f g, (ConcreteCategory.hom (F.map f)) x.snd = (ConcreteCategory.hom (F.map g)) y.snd) →
    Relation.EqvGen F.ColimitTypeRel x y
Module: Mathlib.CategoryTheory.Limits.Types.ColimitTypeFiltered

Goal state before:
pp: case mpr.a
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFiltered J
F : J ⥤ Type w₀
x y : (j : J) × F.obj j
k : J
f : x.fst ⟶ k
f' : y.fst ⟶ k
h : (ConcreteCategory.hom (F.map f)) x.snd = (ConcreteCategory.hom (F.map f')) y.snd
⊢ Relation.EqvGen F.ColimitTypeRel x ⟨k, (ConcreteCategory.hom (F.map f')) y.snd⟩

pp: case mpr.a
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFiltered J
F : J ⥤ Type w₀
x y : (j : J) × F.obj j
k : J
f : x.fst ⟶ k
f' : y.fst ⟶ k
h : (ConcreteCategory.hom (F.map f)) x.snd = (ConcreteCategory.hom (F.map f')) y.snd
⊢ Relation.EqvGen F.ColimitTypeRel ⟨k, (ConcreteCategory.hom (F.map f')) y.snd⟩ y

Tactic:
·

Goal state after:
case mpr.a
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFiltered J
F : J ⥤ Type w₀
x y : (j : J) × F.obj j
k : J
f : x.fst ⟶ k
f' : y.fst ⟶ k
h : (ConcreteCategory.hom (F.map f)) x.snd = (ConcreteCategory.hom (F.map f')) y.snd
⊢ Relation.EqvGen F.ColimitTypeRel x ⟨k, (ConcreteCategory.hom (F.map f')) y.snd⟩
Module: Mathlib.CategoryTheory.Limits.Types.ColimitTypeFiltered

Goal state before:
pp: case mpr.a
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFiltered J
F : J ⥤ Type w₀
x y : (j : J) × F.obj j
k : J
f : x.fst ⟶ k
f' : y.fst ⟶ k
h : (ConcreteCategory.hom (F.map f)) x.snd = (ConcreteCategory.hom (F.map f')) y.snd
⊢ Relation.EqvGen F.ColimitTypeRel ⟨k, (ConcreteCategory.hom (F.map f')) y.snd⟩ y

Tactic:
·

Goal state after:
case mpr.a
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFiltered J
F : J ⥤ Type w₀
x y : (j : J) × F.obj j
k : J
f : x.fst ⟶ k
f' : y.fst ⟶ k
h : (ConcreteCategory.hom (F.map f)) x.snd = (ConcreteCategory.hom (F.map f')) y.snd
⊢ Relation.EqvGen F.ColimitTypeRel ⟨k, (ConcreteCategory.hom (F.map f')) y.snd⟩ y
Module: Mathlib.CategoryTheory.Limits.Types.ColimitTypeFiltered

Goal state before:
pp: case mp
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFiltered J
F : J ⥤ Type w₀
j : J
x y : F.obj j
⊢ (∃ k f f', (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f')) y) →
    ∃ k f, (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f)) y

pp: case mpr
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFiltered J
F : J ⥤ Type w₀
j : J
x y : F.obj j
⊢ (∃ k f, (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f)) y) →
    ∃ k f f', (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f')) y

Tactic:
·

Goal state after:
case mp
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFiltered J
F : J ⥤ Type w₀
j : J
x y : F.obj j
⊢ (∃ k f f', (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f')) y) →
    ∃ k f, (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f)) y
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: case h₁
n : Type u
S S' S'' : Scheme
f : S ⟶ S'
g : S' ⟶ S''
⊢ map n (f ≫ g) ≫ 𝔸(n; S'') ↘ S'' = (map n f ≫ map n g) ≫ 𝔸(n; S'') ↘ S''

pp: case h₂
n : Type u
S S' S'' : Scheme
f : S ⟶ S'
g : S' ⟶ S''
i✝ : n
⊢ (ConcreteCategory.hom (Scheme.Hom.appTop (map n (f ≫ g)))) (coord S'' i✝) =
    (ConcreteCategory.hom (Scheme.Hom.appTop (map n f ≫ map n g))) (coord S'' i✝)

Tactic:
·

Goal state after:
case h₁
n : Type u
S S' S'' : Scheme
f : S ⟶ S'
g : S' ⟶ S''
⊢ map n (f ≫ g) ≫ 𝔸(n; S'') ↘ S'' = (map n f ≫ map n g) ≫ 𝔸(n; S'') ↘ S''
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: case h₂
n : Type u
S S' S'' : Scheme
f : S ⟶ S'
g : S' ⟶ S''
i✝ : n
⊢ (ConcreteCategory.hom (Scheme.Hom.appTop (map n (f ≫ g)))) (coord S'' i✝) =
    (ConcreteCategory.hom (Scheme.Hom.appTop (map n f ≫ map n g))) (coord S'' i✝)

Tactic:
·

Goal state after:
case h₂
n : Type u
S S' S'' : Scheme
f : S ⟶ S'
g : S' ⟶ S''
i✝ : n
⊢ (ConcreteCategory.hom (Scheme.Hom.appTop (map n (f ≫ g)))) (coord S'' i✝) =
    (ConcreteCategory.hom (Scheme.Hom.appTop (map n f ≫ map n g))) (coord S'' i✝)
Module: Mathlib.CategoryTheory.Limits.Types.ColimitTypeFiltered

Goal state before:
pp: case mpr
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFiltered J
F : J ⥤ Type w₀
j : J
x y : F.obj j
⊢ (∃ k f, (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f)) y) →
    ∃ k f f', (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f')) y

Tactic:
·

Goal state after:
case mpr
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFiltered J
F : J ⥤ Type w₀
j : J
x y : F.obj j
⊢ (∃ k f, (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f)) y) →
    ∃ k f f', (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f')) y
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: case h₁
n : Type u
R S : CommRingCat
φ : R ⟶ S
⊢ ((SpecIso n S).inv ≫ map n (Spec.map φ)) ≫ 𝔸(n; Spec R) ↘ Spec R =
    (Spec.map (CommRingCat.ofHom (MvPolynomial.map (CommRingCat.Hom.hom φ))) ≫ (SpecIso n R).inv) ≫
      𝔸(n; Spec R) ↘ Spec R

pp: case h₂
n : Type u
R S : CommRingCat
φ : R ⟶ S
i✝ : n
⊢ (ConcreteCategory.hom (Scheme.Hom.appTop ((SpecIso n S).inv ≫ map n (Spec.map φ)))) (coord (Spec R) i✝) =
    (ConcreteCategory.hom
        (Scheme.Hom.appTop
          (Spec.map (CommRingCat.ofHom (MvPolynomial.map (CommRingCat.Hom.hom φ))) ≫ (SpecIso n R).inv)))
      (coord (Spec R) i✝)

Tactic:
·

Goal state after:
case h₁
n : Type u
R S : CommRingCat
φ : R ⟶ S
⊢ ((SpecIso n S).inv ≫ map n (Spec.map φ)) ≫ 𝔸(n; Spec R) ↘ Spec R =
    (Spec.map (CommRingCat.ofHom (MvPolynomial.map (CommRingCat.Hom.hom φ))) ≫ (SpecIso n R).inv) ≫
      𝔸(n; Spec R) ↘ Spec R
Module: Mathlib.CategoryTheory.Limits.Types.ColimitTypeFiltered

Goal state before:
pp: case mp
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFiltered J
F : J ⥤ Type w₀
c : F.CoconeTypes
⊢ Function.Injective (F.descColimitType c) →
    ∀ (j j' : J) (x : F.obj j) (x' : F.obj j'),
      c.ι j x = c.ι j' x' → ∃ k f f', (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f')) x'

pp: case mpr
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFiltered J
F : J ⥤ Type w₀
c : F.CoconeTypes
⊢ (∀ (j j' : J) (x : F.obj j) (x' : F.obj j'),
      c.ι j x = c.ι j' x' → ∃ k f f', (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f')) x') →
    Function.Injective (F.descColimitType c)

Tactic:
·

Goal state after:
case mp
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFiltered J
F : J ⥤ Type w₀
c : F.CoconeTypes
⊢ Function.Injective (F.descColimitType c) →
    ∀ (j j' : J) (x : F.obj j) (x' : F.obj j'),
      c.ι j x = c.ι j' x' → ∃ k f f', (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f')) x'
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: case h₂
n : Type u
R S : CommRingCat
φ : R ⟶ S
i✝ : n
⊢ (ConcreteCategory.hom (Scheme.Hom.appTop ((SpecIso n S).inv ≫ map n (Spec.map φ)))) (coord (Spec R) i✝) =
    (ConcreteCategory.hom
        (Scheme.Hom.appTop
          (Spec.map (CommRingCat.ofHom (MvPolynomial.map (CommRingCat.Hom.hom φ))) ≫ (SpecIso n R).inv)))
      (coord (Spec R) i✝)

Tactic:
·

Goal state after:
case h₂
n : Type u
R S : CommRingCat
φ : R ⟶ S
i✝ : n
⊢ (ConcreteCategory.hom (Scheme.Hom.appTop ((SpecIso n S).inv ≫ map n (Spec.map φ)))) (coord (Spec R) i✝) =
    (ConcreteCategory.hom
        (Scheme.Hom.appTop
          (Spec.map (CommRingCat.ofHom (MvPolynomial.map (CommRingCat.Hom.hom φ))) ≫ (SpecIso n R).inv)))
      (coord (Spec R) i✝)
Module: Mathlib.CategoryTheory.Limits.Types.ColimitTypeFiltered

Goal state before:
pp: case mpr
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFiltered J
F : J ⥤ Type w₀
c : F.CoconeTypes
⊢ (∀ (j j' : J) (x : F.obj j) (x' : F.obj j'),
      c.ι j x = c.ι j' x' → ∃ k f f', (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f')) x') →
    Function.Injective (F.descColimitType c)

Tactic:
·

Goal state after:
case mpr
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFiltered J
F : J ⥤ Type w₀
c : F.CoconeTypes
⊢ (∀ (j j' : J) (x : F.obj j) (x' : F.obj j'),
      c.ι j x = c.ι j' x' → ∃ k f f', (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f')) x') →
    Function.Injective (F.descColimitType c)
Module: Mathlib.CategoryTheory.Limits.Types.ColimitTypeFiltered

Goal state before:
pp: case mp
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFiltered J
F : J ⥤ Type w₀
c : F.CoconeTypes
⊢ (∀ (j j' : J) (x : F.obj j) (x' : F.obj j'),
      c.ι j x = c.ι j' x' → ∃ k f f', (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f')) x') →
    ∀ (j : J) (x x' : F.obj j),
      c.ι j x = c.ι j x' → ∃ k f, (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f)) x'

pp: case mpr
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFiltered J
F : J ⥤ Type w₀
c : F.CoconeTypes
⊢ (∀ (j : J) (x x' : F.obj j),
      c.ι j x = c.ι j x' → ∃ k f, (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f)) x') →
    ∀ (j j' : J) (x : F.obj j) (x' : F.obj j'),
      c.ι j x = c.ι j' x' → ∃ k f f', (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f')) x'

Tactic:
·

Goal state after:
case mp
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFiltered J
F : J ⥤ Type w₀
c : F.CoconeTypes
⊢ (∀ (j j' : J) (x : F.obj j) (x' : F.obj j'),
      c.ι j x = c.ι j' x' → ∃ k f f', (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f')) x') →
    ∀ (j : J) (x x' : F.obj j),
      c.ι j x = c.ι j x' → ∃ k f, (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f)) x'
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: case inr
n : Type u
S : Scheme
this : ∀ {n : Type u} (S : Scheme), (∃ R, S = Spec R) → topologically (@IsOpenMap) (𝔸(n; S) ↘ S)
hS : ¬∃ R, S = Spec R
⊢ topologically (@IsOpenMap) (𝔸(n; S) ↘ S)

pp: n✝ : Type u
S✝ : Scheme
n : Type u
S : Scheme
hS : ∃ R, S = Spec R
⊢ topologically (@IsOpenMap) (𝔸(n; S) ↘ S)

Tactic:
·

Goal state after:
case inr
n : Type u
S : Scheme
this : ∀ {n : Type u} (S : Scheme), (∃ R, S = Spec R) → topologically (@IsOpenMap) (𝔸(n; S) ↘ S)
hS : ¬∃ R, S = Spec R
⊢ topologically (@IsOpenMap) (𝔸(n; S) ↘ S)
Module: Mathlib.CategoryTheory.Limits.Types.ColimitTypeFiltered

Goal state before:
pp: case mpr
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFiltered J
F : J ⥤ Type w₀
c : F.CoconeTypes
⊢ (∀ (j : J) (x x' : F.obj j),
      c.ι j x = c.ι j x' → ∃ k f, (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f)) x') →
    ∀ (j j' : J) (x : F.obj j) (x' : F.obj j'),
      c.ι j x = c.ι j' x' → ∃ k f f', (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f')) x'

Tactic:
·

Goal state after:
case mpr
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFiltered J
F : J ⥤ Type w₀
c : F.CoconeTypes
⊢ (∀ (j : J) (x x' : F.obj j),
      c.ι j x = c.ι j x' → ∃ k f, (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f)) x') →
    ∀ (j j' : J) (x : F.obj j) (x' : F.obj j'),
      c.ι j x = c.ι j' x' → ∃ k f f', (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f')) x'
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: case inr
n : Type u
S : Scheme
h : IsReduced S
this : ∀ {n : Type u} (S : Scheme) [h : IsReduced S], (∃ R, S = Spec R) → IsReduced 𝔸(n; S)
hS : ¬∃ R, S = Spec R
⊢ IsReduced 𝔸(n; S)

pp: n✝ : Type u
S✝ : Scheme
n : Type u
S : Scheme
h : IsReduced S
hS : ∃ R, S = Spec R
⊢ IsReduced 𝔸(n; S)

Tactic:
·

Goal state after:
case inr
n : Type u
S : Scheme
h : IsReduced S
this : ∀ {n : Type u} (S : Scheme) [h : IsReduced S], (∃ R, S = Spec R) → IsReduced 𝔸(n; S)
hS : ¬∃ R, S = Spec R
⊢ IsReduced 𝔸(n; S)
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: case a
n : Type u
S : Scheme
inst✝ : IsEmpty n
⊢ isomorphisms Scheme (Spec.map (CommRingCat.ofHom C))

pp: case a
n : Type u
S : Scheme
inst✝ : IsEmpty n
⊢ isomorphisms Scheme (terminal.from (Spec (CommRingCat.of (ULift.{u, 0} ℤ))))

Tactic:
·

Goal state after:
case a
n : Type u
S : Scheme
inst✝ : IsEmpty n
⊢ isomorphisms Scheme (Spec.map (CommRingCat.ofHom C))
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: case a
n : Type u
S : Scheme
inst✝ : IsEmpty n
⊢ isomorphisms Scheme (terminal.from (Spec (CommRingCat.of (ULift.{u, 0} ℤ))))

Tactic:
·

Goal state after:
case a
n : Type u
S : Scheme
inst✝ : IsEmpty n
⊢ isomorphisms Scheme (terminal.from (Spec (CommRingCat.of (ULift.{u, 0} ℤ))))
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: case mp
n : Type u
S : Scheme
⊢ IsIntegralHom (𝔸(n; S) ↘ S) → IsEmpty ↥S ∨ IsEmpty n

pp: case mpr
n : Type u
S : Scheme
⊢ IsEmpty ↥S ∨ IsEmpty n → IsIntegralHom (𝔸(n; S) ↘ S)

Tactic:
·

Goal state after:
case mp
n : Type u
S : Scheme
⊢ IsIntegralHom (𝔸(n; S) ↘ S) → IsEmpty ↥S ∨ IsEmpty n
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: case mp.inl
n : Type u
S : Scheme
h : IsIntegralHom (𝔸(n; S) ↘ S)
h✝ : IsEmpty ↥S
⊢ IsEmpty ↥S ∨ IsEmpty n

pp: case mp.inr
n : Type u
S : Scheme
h : IsIntegralHom (𝔸(n; S) ↘ S)
h✝ : Nonempty ↥S
⊢ IsEmpty ↥S ∨ IsEmpty n

Tactic:
·

Goal state after:
case mp.inl
n : Type u
S : Scheme
h : IsIntegralHom (𝔸(n; S) ↘ S)
h✝ : IsEmpty ↥S
⊢ IsEmpty ↥S ∨ IsEmpty n
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: case mp.inr.inr
n : Type u
S : Scheme
h : IsIntegralHom (𝔸(n; S) ↘ S)
h✝ : Nonempty ↥S
this : ∀ {n : Type u} (S : Scheme), IsIntegralHom (𝔸(n; S) ↘ S) → Nonempty ↥S → (∃ R, S = Spec R) → IsEmpty n
hS : ¬∃ R, S = Spec R
⊢ IsEmpty n

pp: n✝ : Type u
S✝ : Scheme
n : Type u
S : Scheme
h : IsIntegralHom (𝔸(n; S) ↘ S)
h✝ : Nonempty ↥S
hS : ∃ R, S = Spec R
⊢ IsEmpty n

Tactic:
·

Goal state after:
case mp.inr.inr
n : Type u
S : Scheme
h : IsIntegralHom (𝔸(n; S) ↘ S)
h✝ : Nonempty ↥S
this : ∀ {n : Type u} (S : Scheme), IsIntegralHom (𝔸(n; S) ↘ S) → Nonempty ↥S → (∃ R, S = Spec R) → IsEmpty n
hS : ¬∃ R, S = Spec R
⊢ IsEmpty n