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

Goal state before:
pp: case refine_1.refine_1
P : MorphismProperty Scheme
inst✝⁸ : P.IsStableUnderBaseChange
inst✝⁷ : P.IsMultiplicative
S : Scheme
J : Type u_1
inst✝⁶ : Category.{v_1, u_1} J
D : J ⥤ P.Over ⊤ S
𝒰 : S.OpenCover
inst✝⁵ : Category.{v_2, ?u.129} 𝒰.I₀
inst✝⁴ : LocallyDirected 𝒰
d : ColimitGluingData D 𝒰
inst✝³ :
  ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), PreservesColimitsOfShape J (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))
inst✝² : Quiver.IsThin 𝒰.I₀
inst✝¹ : Small.{u, ?u.129} 𝒰.I₀
inst✝ : IsZariskiLocalAtTarget P
𝒱 : (a : J) → (D.obj a).left.OpenCover := fun a ↦ Precoverage.ZeroHypercover.pullback₁ (D.obj a).hom 𝒰
a : J
⊢ (i : (𝒱 a).I₀) → (𝒱 a).X i ⟶ Over.left (((Functor.const J).obj d.glued).obj a).toComma

pp: case refine_1.refine_2
P : MorphismProperty Scheme
inst✝⁸ : P.IsStableUnderBaseChange
inst✝⁷ : P.IsMultiplicative
S : Scheme
J : Type u_1
inst✝⁶ : Category.{v_1, u_1} J
D : J ⥤ P.Over ⊤ S
𝒰 : S.OpenCover
inst✝⁵ : Category.{v_2, ?u.129} 𝒰.I₀
inst✝⁴ : LocallyDirected 𝒰
d : ColimitGluingData D 𝒰
inst✝³ :
  ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), PreservesColimitsOfShape J (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))
inst✝² : Quiver.IsThin 𝒰.I₀
inst✝¹ : Small.{u, ?u.129} 𝒰.I₀
inst✝ : IsZariskiLocalAtTarget P
𝒱 : (a : J) → (D.obj a).left.OpenCover := fun a ↦ Precoverage.ZeroHypercover.pullback₁ (D.obj a).hom 𝒰
a : J
⊢ ∀ {i j : (𝒱 a).I₀} (hij : i ⟶ j), Cover.trans (𝒱 a) hij ≫ ?refine_1.refine_1 j = ?refine_1.refine_1 i

pp: case refine_1.refine_3
P : MorphismProperty Scheme
inst✝⁸ : P.IsStableUnderBaseChange
inst✝⁷ : P.IsMultiplicative
S : Scheme
J : Type u_1
inst✝⁶ : Category.{v_1, u_1} J
D : J ⥤ P.Over ⊤ S
𝒰 : S.OpenCover
inst✝⁵ : Category.{v_2, ?u.129} 𝒰.I₀
inst✝⁴ : LocallyDirected 𝒰
d : ColimitGluingData D 𝒰
inst✝³ :
  ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), PreservesColimitsOfShape J (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))
inst✝² : Quiver.IsThin 𝒰.I₀
inst✝¹ : Small.{u, ?u.129} 𝒰.I₀
inst✝ : IsZariskiLocalAtTarget P
𝒱 : (a : J) → (D.obj a).left.OpenCover := fun a ↦ Precoverage.ZeroHypercover.pullback₁ (D.obj a).hom 𝒰
a : J
⊢ ∀ (i : (𝒱 a).I₀),
    ?refine_1.refine_1 i ≫ Over.hom (((Functor.const J).obj d.glued).obj a).toComma =
      (𝒱 a).f i ≫ Over.hom (D.obj a).toComma

Tactic:
·

Goal state after:
case refine_1.refine_1
P : MorphismProperty Scheme
inst✝⁸ : P.IsStableUnderBaseChange
inst✝⁷ : P.IsMultiplicative
S : Scheme
J : Type u_1
inst✝⁶ : Category.{v_1, u_1} J
D : J ⥤ P.Over ⊤ S
𝒰 : S.OpenCover
inst✝⁵ : Category.{v_2, ?u.129} 𝒰.I₀
inst✝⁴ : LocallyDirected 𝒰
d : ColimitGluingData D 𝒰
inst✝³ :
  ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), PreservesColimitsOfShape J (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))
inst✝² : Quiver.IsThin 𝒰.I₀
inst✝¹ : Small.{u, ?u.129} 𝒰.I₀
inst✝ : IsZariskiLocalAtTarget P
𝒱 : (a : J) → (D.obj a).left.OpenCover := fun a ↦ Precoverage.ZeroHypercover.pullback₁ (D.obj a).hom 𝒰
a : J
⊢ (i : (𝒱 a).I₀) → (𝒱 a).X i ⟶ Over.left (((Functor.const J).obj d.glued).obj a).toComma
Module: Mathlib.AlgebraicGeometry.ColimitsOver

Goal state before:
pp: case refine_1.refine_2
P : MorphismProperty Scheme
inst✝⁸ : P.IsStableUnderBaseChange
inst✝⁷ : P.IsMultiplicative
S : Scheme
J : Type u_1
inst✝⁶ : Category.{v_1, u_1} J
D : J ⥤ P.Over ⊤ S
𝒰 : S.OpenCover
inst✝⁵ : Category.{v_2, ?u.129} 𝒰.I₀
inst✝⁴ : LocallyDirected 𝒰
d : ColimitGluingData D 𝒰
inst✝³ :
  ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), PreservesColimitsOfShape J (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))
inst✝² : Quiver.IsThin 𝒰.I₀
inst✝¹ : Small.{u, ?u.129} 𝒰.I₀
inst✝ : IsZariskiLocalAtTarget P
𝒱 : (a : J) → (D.obj a).left.OpenCover := fun a ↦ Precoverage.ZeroHypercover.pullback₁ (D.obj a).hom 𝒰
a : J
⊢ ∀ {i j : (𝒱 a).I₀} (hij : i ⟶ j),
    Cover.trans (𝒱 a) hij ≫ ((d.cocone j).ι.app a).left ≫ colimit.ι d.relativeGluingData.functor j =
      ((d.cocone i).ι.app a).left ≫ colimit.ι d.relativeGluingData.functor i

pp: case refine_1.refine_3
P : MorphismProperty Scheme
inst✝⁸ : P.IsStableUnderBaseChange
inst✝⁷ : P.IsMultiplicative
S : Scheme
J : Type u_1
inst✝⁶ : Category.{v_1, u_1} J
D : J ⥤ P.Over ⊤ S
𝒰 : S.OpenCover
inst✝⁵ : Category.{v_2, ?u.129} 𝒰.I₀
inst✝⁴ : LocallyDirected 𝒰
d : ColimitGluingData D 𝒰
inst✝³ :
  ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), PreservesColimitsOfShape J (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))
inst✝² : Quiver.IsThin 𝒰.I₀
inst✝¹ : Small.{u, ?u.129} 𝒰.I₀
inst✝ : IsZariskiLocalAtTarget P
𝒱 : (a : J) → (D.obj a).left.OpenCover := fun a ↦ Precoverage.ZeroHypercover.pullback₁ (D.obj a).hom 𝒰
a : J
⊢ ∀ (i : (𝒱 a).I₀),
    (((d.cocone i).ι.app a).left ≫ colimit.ι d.relativeGluingData.functor i) ≫
        Over.hom (((Functor.const J).obj d.glued).obj a).toComma =
      (𝒱 a).f i ≫ Over.hom (D.obj a).toComma

Tactic:
·

Goal state after:
case refine_1.refine_2
P : MorphismProperty Scheme
inst✝⁸ : P.IsStableUnderBaseChange
inst✝⁷ : P.IsMultiplicative
S : Scheme
J : Type u_1
inst✝⁶ : Category.{v_1, u_1} J
D : J ⥤ P.Over ⊤ S
𝒰 : S.OpenCover
inst✝⁵ : Category.{v_2, ?u.129} 𝒰.I₀
inst✝⁴ : LocallyDirected 𝒰
d : ColimitGluingData D 𝒰
inst✝³ :
  ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), PreservesColimitsOfShape J (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))
inst✝² : Quiver.IsThin 𝒰.I₀
inst✝¹ : Small.{u, ?u.129} 𝒰.I₀
inst✝ : IsZariskiLocalAtTarget P
𝒱 : (a : J) → (D.obj a).left.OpenCover := fun a ↦ Precoverage.ZeroHypercover.pullback₁ (D.obj a).hom 𝒰
a : J
⊢ ∀ {i j : (𝒱 a).I₀} (hij : i ⟶ j),
    Cover.trans (𝒱 a) hij ≫ ((d.cocone j).ι.app a).left ≫ colimit.ι d.relativeGluingData.functor j =
      ((d.cocone i).ι.app a).left ≫ colimit.ι d.relativeGluingData.functor i
Module: Mathlib.AlgebraicGeometry.ColimitsOver

Goal state before:
pp: case refine_1.refine_3
P : MorphismProperty Scheme
inst✝⁸ : P.IsStableUnderBaseChange
inst✝⁷ : P.IsMultiplicative
S : Scheme
J : Type u_1
inst✝⁶ : Category.{v_1, u_1} J
D : J ⥤ P.Over ⊤ S
𝒰 : S.OpenCover
inst✝⁵ : Category.{v_2, ?u.129} 𝒰.I₀
inst✝⁴ : LocallyDirected 𝒰
d : ColimitGluingData D 𝒰
inst✝³ :
  ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), PreservesColimitsOfShape J (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))
inst✝² : Quiver.IsThin 𝒰.I₀
inst✝¹ : Small.{u, ?u.129} 𝒰.I₀
inst✝ : IsZariskiLocalAtTarget P
𝒱 : (a : J) → (D.obj a).left.OpenCover := fun a ↦ Precoverage.ZeroHypercover.pullback₁ (D.obj a).hom 𝒰
a : J
⊢ ∀ (i : (𝒱 a).I₀),
    (((d.cocone i).ι.app a).left ≫ colimit.ι d.relativeGluingData.functor i) ≫
        Over.hom (((Functor.const J).obj d.glued).obj a).toComma =
      (𝒱 a).f i ≫ Over.hom (D.obj a).toComma

Tactic:
·

Goal state after:
case refine_1.refine_3
P : MorphismProperty Scheme
inst✝⁸ : P.IsStableUnderBaseChange
inst✝⁷ : P.IsMultiplicative
S : Scheme
J : Type u_1
inst✝⁶ : Category.{v_1, u_1} J
D : J ⥤ P.Over ⊤ S
𝒰 : S.OpenCover
inst✝⁵ : Category.{v_2, ?u.129} 𝒰.I₀
inst✝⁴ : LocallyDirected 𝒰
d : ColimitGluingData D 𝒰
inst✝³ :
  ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), PreservesColimitsOfShape J (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))
inst✝² : Quiver.IsThin 𝒰.I₀
inst✝¹ : Small.{u, ?u.129} 𝒰.I₀
inst✝ : IsZariskiLocalAtTarget P
𝒱 : (a : J) → (D.obj a).left.OpenCover := fun a ↦ Precoverage.ZeroHypercover.pullback₁ (D.obj a).hom 𝒰
a : J
⊢ ∀ (i : (𝒱 a).I₀),
    (((d.cocone i).ι.app a).left ≫ colimit.ι d.relativeGluingData.functor i) ≫
        Over.hom (((Functor.const J).obj d.glued).obj a).toComma =
      (𝒱 a).f i ≫ Over.hom (D.obj a).toComma
Module: Mathlib.AlgebraicGeometry.Cover.QuasiCompact

Goal state before:
pp: case refine_1
P : MorphismProperty Scheme
S : Scheme
𝒰 : Scheme.Cover (Scheme.precoverage P) S
inst✝² : P.RespectsLeft IsOpenImmersion
inst✝¹ : CompactSpace ↥S
inst✝ : QuasiCompactCover 𝒰.toPreZeroHypercover
n : ℕ
f : Fin n → 𝒰.I₀
V : (i : Fin n) → (𝒰.X (f i)).Opens
hV : ∀ (i : Fin n), IsAffineOpen (V i)
idx : ↥S → Fin n
x : (x : ↥S) → ↥(𝒰.X (f (idx x)))
hmem : ∀ (x_1 : ↥S), x x_1 ∈ V (idx x_1)
hx : ∀ (x_1 : ↥S), (𝒰.f (f (idx x_1))) (x x_1) = x_1
⊢ Scheme.AffineCover P S

pp: case refine_2
P : MorphismProperty Scheme
S : Scheme
𝒰 : Scheme.Cover (Scheme.precoverage P) S
inst✝² : P.RespectsLeft IsOpenImmersion
inst✝¹ : CompactSpace ↥S
inst✝ : QuasiCompactCover 𝒰.toPreZeroHypercover
n : ℕ
f : Fin n → 𝒰.I₀
V : (i : Fin n) → (𝒰.X (f i)).Opens
hV : ∀ (i : Fin n), IsAffineOpen (V i)
idx : ↥S → Fin n
x : (x : ↥S) → ↥(𝒰.X (f (idx x)))
hmem : ∀ (x_1 : ↥S), x x_1 ∈ V (idx x_1)
hx : ∀ (x_1 : ↥S), (𝒰.f (f (idx x_1))) (x x_1) = x_1
⊢ Scheme.AffineCover.cover ?refine_1 ⟶ 𝒰

pp: case refine_3
P : MorphismProperty Scheme
S : Scheme
𝒰 : Scheme.Cover (Scheme.precoverage P) S
inst✝² : P.RespectsLeft IsOpenImmersion
inst✝¹ : CompactSpace ↥S
inst✝ : QuasiCompactCover 𝒰.toPreZeroHypercover
n : ℕ
f : Fin n → 𝒰.I₀
V : (i : Fin n) → (𝒰.X (f i)).Opens
hV : ∀ (i : Fin n), IsAffineOpen (V i)
idx : ↥S → Fin n
x : (x : ↥S) → ↥(𝒰.X (f (idx x)))
hmem : ∀ (x_1 : ↥S), x x_1 ∈ V (idx x_1)
hx : ∀ (x_1 : ↥S), (𝒰.f (f (idx x_1))) (x x_1) = x_1
⊢ Finite (Scheme.AffineCover.I₀ ?refine_1)

pp: case refine_4
P : MorphismProperty Scheme
S : Scheme
𝒰 : Scheme.Cover (Scheme.precoverage P) S
inst✝² : P.RespectsLeft IsOpenImmersion
inst✝¹ : CompactSpace ↥S
inst✝ : QuasiCompactCover 𝒰.toPreZeroHypercover
n : ℕ
f : Fin n → 𝒰.I₀
V : (i : Fin n) → (𝒰.X (f i)).Opens
hV : ∀ (i : Fin n), IsAffineOpen (V i)
idx : ↥S → Fin n
x : (x : ↥S) → ↥(𝒰.X (f (idx x)))
hmem : ∀ (x_1 : ↥S), x x_1 ∈ V (idx x_1)
hx : ∀ (x_1 : ↥S), (𝒰.f (f (idx x_1))) (x x_1) = x_1
⊢ ∀ (j : (Scheme.AffineCover.cover ?refine_1).I₀), IsOpenImmersion (PreZeroHypercover.Hom.h₀ ?refine_2 j)

Tactic:
·

Goal state after:
case refine_1
P : MorphismProperty Scheme
S : Scheme
𝒰 : Scheme.Cover (Scheme.precoverage P) S
inst✝² : P.RespectsLeft IsOpenImmersion
inst✝¹ : CompactSpace ↥S
inst✝ : QuasiCompactCover 𝒰.toPreZeroHypercover
n : ℕ
f : Fin n → 𝒰.I₀
V : (i : Fin n) → (𝒰.X (f i)).Opens
hV : ∀ (i : Fin n), IsAffineOpen (V i)
idx : ↥S → Fin n
x : (x : ↥S) → ↥(𝒰.X (f (idx x)))
hmem : ∀ (x_1 : ↥S), x x_1 ∈ V (idx x_1)
hx : ∀ (x_1 : ↥S), (𝒰.f (f (idx x_1))) (x x_1) = x_1
⊢ Scheme.AffineCover P S
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: case neg
R✝ : Type u_2
inst✝³ : CommRing R✝
n : ℕ
R : Type u_2
inst✝² : CommRing R
c : InductionObj R n
i j : Fin n
hi : (c.val i).Monic
hle : (c.val i).degree ≤ (c.val j).degree
hne : i ≠ j
H :
  ∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_1 : Algebra R₀ R],
    Statement R₀ R n { val := Function.update c.val j (c.val j %ₘ c.val i) }
R₀ : Type u_1
inst✝¹ : CommRing R₀
inst✝ : Algebra R₀ R
f : R[X]
h✝ : Nontrivial R
S : ConstructibleSetData R
hS :
  comap Polynomial.C ''
      (zeroLocus (Set.range { val := Function.update c.val j (c.val j %ₘ c.val i) }.val) \ zeroLocus {f}) =
    S.toSet
hS' :
  ∀ C ∈ S,
    C.n ≤ { val := Function.update c.val j (c.val j %ₘ c.val i) }.degBound ∧
      ∀ (i_1 : Fin C.n),
        C.g i_1 ∈
          coeffSubmodule R₀ { val := Function.update c.val j (c.val j %ₘ c.val i) } ^
            { val := Function.update c.val j (c.val j %ₘ c.val i) }.powBound
C : BasicConstructibleSetData R
hC : C ∈ S
c' : InductionObj R n := { val := Function.update c.val j (c.val j %ₘ c.val i) }
deg_bound₁ : c'.degBound ≤ c.degBound
k✝ : Fin C.n
hij : coeffSubmodule R₀ c' ≤ coeffSubmodule R₀ c ^ (c.val j).degree.succ
hi' : ¬c.val i = 1
k : Fin n
a✝ : k ∈ Finset.univ
hkj : ¬k = j
⊢ (c.val k).degree.succ ≤ (c.val k).degree.succ

Tactic:
·

Goal state after:
case neg
R✝ : Type u_2
inst✝³ : CommRing R✝
n : ℕ
R : Type u_2
inst✝² : CommRing R
c : InductionObj R n
i j : Fin n
hi : (c.val i).Monic
hle : (c.val i).degree ≤ (c.val j).degree
hne : i ≠ j
H :
  ∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_1 : Algebra R₀ R],
    Statement R₀ R n { val := Function.update c.val j (c.val j %ₘ c.val i) }
R₀ : Type u_1
inst✝¹ : CommRing R₀
inst✝ : Algebra R₀ R
f : R[X]
h✝ : Nontrivial R
S : ConstructibleSetData R
hS :
  comap Polynomial.C ''
      (zeroLocus (Set.range { val := Function.update c.val j (c.val j %ₘ c.val i) }.val) \ zeroLocus {f}) =
    S.toSet
hS' :
  ∀ C ∈ S,
    C.n ≤ { val := Function.update c.val j (c.val j %ₘ c.val i) }.degBound ∧
      ∀ (i_1 : Fin C.n),
        C.g i_1 ∈
          coeffSubmodule R₀ { val := Function.update c.val j (c.val j %ₘ c.val i) } ^
            { val := Function.update c.val j (c.val j %ₘ c.val i) }.powBound
C : BasicConstructibleSetData R
hC : C ∈ S
c' : InductionObj R n := { val := Function.update c.val j (c.val j %ₘ c.val i) }
deg_bound₁ : c'.degBound ≤ c.degBound
k✝ : Fin C.n
hij : coeffSubmodule R₀ c' ≤ coeffSubmodule R₀ c ^ (c.val j).degree.succ
hi' : ¬c.val i = 1
k : Fin n
a✝ : k ∈ Finset.univ
hkj : ¬k = j
⊢ (c.val k).degree.succ ≤ (c.val k).degree.succ
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: R✝ : Type u_2
inst✝³ : CommRing R✝
n : ℕ
R : Type u_2
inst✝² : CommRing R
c : InductionObj R n
i j : Fin n
hi : (c.val i).Monic
hle : (c.val i).degree ≤ (c.val j).degree
hne : i ≠ j
H :
  ∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_1 : Algebra R₀ R],
    Statement R₀ R n { val := Function.update c.val j (c.val j %ₘ c.val i) }
R₀ : Type u_1
inst✝¹ : CommRing R₀
inst✝ : Algebra R₀ R
f : R[X]
h✝ : Nontrivial R
S : ConstructibleSetData R
hS :
  comap Polynomial.C ''
      (zeroLocus (Set.range { val := Function.update c.val j (c.val j %ₘ c.val i) }.val) \ zeroLocus {f}) =
    S.toSet
hS' :
  ∀ C ∈ S,
    C.n ≤ { val := Function.update c.val j (c.val j %ₘ c.val i) }.degBound ∧
      ∀ (i_1 : Fin C.n),
        C.g i_1 ∈
          coeffSubmodule R₀ { val := Function.update c.val j (c.val j %ₘ c.val i) } ^
            { val := Function.update c.val j (c.val j %ₘ c.val i) }.powBound
C : BasicConstructibleSetData R
hC : C ∈ S
c' : InductionObj R n := { val := Function.update c.val j (c.val j %ₘ c.val i) }
deg_bound₁ : c'.degBound ≤ c.degBound
k : Fin C.n
hij : coeffSubmodule R₀ c' ≤ coeffSubmodule R₀ c ^ (c.val j).degree.succ
hi' : ¬c.val i = 1
⊢ (Function.update c.val j (c.val j %ₘ c.val i) j).degree.succ < (c.val j).degree.succ

Tactic:
·

Goal state after:
R✝ : Type u_2
inst✝³ : CommRing R✝
n : ℕ
R : Type u_2
inst✝² : CommRing R
c : InductionObj R n
i j : Fin n
hi : (c.val i).Monic
hle : (c.val i).degree ≤ (c.val j).degree
hne : i ≠ j
H :
  ∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_1 : Algebra R₀ R],
    Statement R₀ R n { val := Function.update c.val j (c.val j %ₘ c.val i) }
R₀ : Type u_1
inst✝¹ : CommRing R₀
inst✝ : Algebra R₀ R
f : R[X]
h✝ : Nontrivial R
S : ConstructibleSetData R
hS :
  comap Polynomial.C ''
      (zeroLocus (Set.range { val := Function.update c.val j (c.val j %ₘ c.val i) }.val) \ zeroLocus {f}) =
    S.toSet
hS' :
  ∀ C ∈ S,
    C.n ≤ { val := Function.update c.val j (c.val j %ₘ c.val i) }.degBound ∧
      ∀ (i_1 : Fin C.n),
        C.g i_1 ∈
          coeffSubmodule R₀ { val := Function.update c.val j (c.val j %ₘ c.val i) } ^
            { val := Function.update c.val j (c.val j %ₘ c.val i) }.powBound
C : BasicConstructibleSetData R
hC : C ∈ S
c' : InductionObj R n := { val := Function.update c.val j (c.val j %ₘ c.val i) }
deg_bound₁ : c'.degBound ≤ c.degBound
k : Fin C.n
hij : coeffSubmodule R₀ c' ≤ coeffSubmodule R₀ c ^ (c.val j).degree.succ
hi' : ¬c.val i = 1
⊢ (Function.update c.val j (c.val j %ₘ c.val i) j).degree.succ < (c.val j).degree.succ
Module: Mathlib.AlgebraicGeometry.ColimitsOver

Goal state before:
pp: case refine_2
P : MorphismProperty Scheme
inst✝⁸ : P.IsStableUnderBaseChange
inst✝⁷ : P.IsMultiplicative
S : Scheme
J : Type u_1
inst✝⁶ : Category.{v_1, u_1} J
D : J ⥤ P.Over ⊤ S
𝒰 : S.OpenCover
inst✝⁵ : Category.{v_2, ?u.129} 𝒰.I₀
inst✝⁴ : LocallyDirected 𝒰
d : ColimitGluingData D 𝒰
inst✝³ :
  ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), PreservesColimitsOfShape J (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))
inst✝² : Quiver.IsThin 𝒰.I₀
inst✝¹ : Small.{u, ?u.129} 𝒰.I₀
inst✝ : IsZariskiLocalAtTarget P
𝒱 : (a : J) → (D.obj a).left.OpenCover := fun a ↦ Precoverage.ZeroHypercover.pullback₁ (D.obj a).hom 𝒰
a b : J
f : a ⟶ b
⊢ D.map f ≫
      {
        toCommaMorphism :=
          (𝒱 b).glueMorphismsOverOfLocallyDirected
            (fun i ↦ ((d.cocone i).ι.app b).left ≫ colimit.ι d.relativeGluingData.functor i) ⋯ ⋯,
        prop_hom_left := trivial, prop_hom_right := trivial } =
    {
        toCommaMorphism :=
          (𝒱 a).glueMorphismsOverOfLocallyDirected
            (fun i ↦ ((d.cocone i).ι.app a).left ≫ colimit.ι d.relativeGluingData.functor i) ⋯ ⋯,
        prop_hom_left := trivial, prop_hom_right := trivial } ≫
      ((Functor.const J).obj d.glued).map f

Tactic:
·

Goal state after:
case refine_2
P : MorphismProperty Scheme
inst✝⁸ : P.IsStableUnderBaseChange
inst✝⁷ : P.IsMultiplicative
S : Scheme
J : Type u_1
inst✝⁶ : Category.{v_1, u_1} J
D : J ⥤ P.Over ⊤ S
𝒰 : S.OpenCover
inst✝⁵ : Category.{v_2, ?u.129} 𝒰.I₀
inst✝⁴ : LocallyDirected 𝒰
d : ColimitGluingData D 𝒰
inst✝³ :
  ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), PreservesColimitsOfShape J (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))
inst✝² : Quiver.IsThin 𝒰.I₀
inst✝¹ : Small.{u, ?u.129} 𝒰.I₀
inst✝ : IsZariskiLocalAtTarget P
𝒱 : (a : J) → (D.obj a).left.OpenCover := fun a ↦ Precoverage.ZeroHypercover.pullback₁ (D.obj a).hom 𝒰
a b : J
f : a ⟶ b
⊢ D.map f ≫
      {
        toCommaMorphism :=
          (𝒱 b).glueMorphismsOverOfLocallyDirected
            (fun i ↦ ((d.cocone i).ι.app b).left ≫ colimit.ι d.relativeGluingData.functor i) ⋯ ⋯,
        prop_hom_left := trivial, prop_hom_right := trivial } =
    {
        toCommaMorphism :=
          (𝒱 a).glueMorphismsOverOfLocallyDirected
            (fun i ↦ ((d.cocone i).ι.app a).left ≫ colimit.ι d.relativeGluingData.functor i) ⋯ ⋯,
        prop_hom_left := trivial, prop_hom_right := trivial } ≫
      ((Functor.const J).obj d.glued).map f
Module: Mathlib.AlgebraicGeometry.Cover.QuasiCompact

Goal state before:
pp: case refine_2
P : MorphismProperty Scheme
S : Scheme
𝒰 : Scheme.Cover (Scheme.precoverage P) S
inst✝² : P.RespectsLeft IsOpenImmersion
inst✝¹ : CompactSpace ↥S
inst✝ : QuasiCompactCover 𝒰.toPreZeroHypercover
n : ℕ
f : Fin n → 𝒰.I₀
V : (i : Fin n) → (𝒰.X (f i)).Opens
hV : ∀ (i : Fin n), IsAffineOpen (V i)
idx : ↥S → Fin n
x : (x : ↥S) → ↥(𝒰.X (f (idx x)))
hmem : ∀ (x_1 : ↥S), x x_1 ∈ V (idx x_1)
hx : ∀ (x_1 : ↥S), (𝒰.f (f (idx x_1))) (x x_1) = x_1
⊢ { I₀ := ULift.{w, 0} (Fin n), X := fun i ↦ Γ(𝒰.X (f i.down), V i.down), f := fun i ↦ ⋯.fromSpec ≫ 𝒰.f (f i.down),
        idx := fun s ↦ { down := idx s }, covers := ⋯, map_prop := ⋯ }.cover ⟶
    𝒰

pp: case refine_3
P : MorphismProperty Scheme
S : Scheme
𝒰 : Scheme.Cover (Scheme.precoverage P) S
inst✝² : P.RespectsLeft IsOpenImmersion
inst✝¹ : CompactSpace ↥S
inst✝ : QuasiCompactCover 𝒰.toPreZeroHypercover
n : ℕ
f : Fin n → 𝒰.I₀
V : (i : Fin n) → (𝒰.X (f i)).Opens
hV : ∀ (i : Fin n), IsAffineOpen (V i)
idx : ↥S → Fin n
x : (x : ↥S) → ↥(𝒰.X (f (idx x)))
hmem : ∀ (x_1 : ↥S), x x_1 ∈ V (idx x_1)
hx : ∀ (x_1 : ↥S), (𝒰.f (f (idx x_1))) (x x_1) = x_1
⊢ Finite
    { I₀ := ULift.{w, 0} (Fin n), X := fun i ↦ Γ(𝒰.X (f i.down), V i.down), f := fun i ↦ ⋯.fromSpec ≫ 𝒰.f (f i.down),
        idx := fun s ↦ { down := idx s }, covers := ⋯, map_prop := ⋯ }.I₀

pp: case refine_4
P : MorphismProperty Scheme
S : Scheme
𝒰 : Scheme.Cover (Scheme.precoverage P) S
inst✝² : P.RespectsLeft IsOpenImmersion
inst✝¹ : CompactSpace ↥S
inst✝ : QuasiCompactCover 𝒰.toPreZeroHypercover
n : ℕ
f : Fin n → 𝒰.I₀
V : (i : Fin n) → (𝒰.X (f i)).Opens
hV : ∀ (i : Fin n), IsAffineOpen (V i)
idx : ↥S → Fin n
x : (x : ↥S) → ↥(𝒰.X (f (idx x)))
hmem : ∀ (x_1 : ↥S), x x_1 ∈ V (idx x_1)
hx : ∀ (x_1 : ↥S), (𝒰.f (f (idx x_1))) (x x_1) = x_1
⊢ ∀
    (j :
      { I₀ := ULift.{w, 0} (Fin n), X := fun i ↦ Γ(𝒰.X (f i.down), V i.down), f := fun i ↦ ⋯.fromSpec ≫ 𝒰.f (f i.down),
            idx := fun s ↦ { down := idx s }, covers := ⋯, map_prop := ⋯ }.cover.I₀),
    IsOpenImmersion (PreZeroHypercover.Hom.h₀ ?refine_2 j)

Tactic:
·

Goal state after:
case refine_2
P : MorphismProperty Scheme
S : Scheme
𝒰 : Scheme.Cover (Scheme.precoverage P) S
inst✝² : P.RespectsLeft IsOpenImmersion
inst✝¹ : CompactSpace ↥S
inst✝ : QuasiCompactCover 𝒰.toPreZeroHypercover
n : ℕ
f : Fin n → 𝒰.I₀
V : (i : Fin n) → (𝒰.X (f i)).Opens
hV : ∀ (i : Fin n), IsAffineOpen (V i)
idx : ↥S → Fin n
x : (x : ↥S) → ↥(𝒰.X (f (idx x)))
hmem : ∀ (x_1 : ↥S), x x_1 ∈ V (idx x_1)
hx : ∀ (x_1 : ↥S), (𝒰.f (f (idx x_1))) (x x_1) = x_1
⊢ { I₀ := ULift.{w, 0} (Fin n), X := fun i ↦ Γ(𝒰.X (f i.down), V i.down), f := fun i ↦ ⋯.fromSpec ≫ 𝒰.f (f i.down),
        idx := fun s ↦ { down := idx s }, covers := ⋯, map_prop := ⋯ }.cover ⟶
    𝒰
Module: Mathlib.AlgebraicGeometry.Cover.QuasiCompact

Goal state before:
pp: case refine_3
P : MorphismProperty Scheme
S : Scheme
𝒰 : Scheme.Cover (Scheme.precoverage P) S
inst✝² : P.RespectsLeft IsOpenImmersion
inst✝¹ : CompactSpace ↥S
inst✝ : QuasiCompactCover 𝒰.toPreZeroHypercover
n : ℕ
f : Fin n → 𝒰.I₀
V : (i : Fin n) → (𝒰.X (f i)).Opens
hV : ∀ (i : Fin n), IsAffineOpen (V i)
idx : ↥S → Fin n
x : (x : ↥S) → ↥(𝒰.X (f (idx x)))
hmem : ∀ (x_1 : ↥S), x x_1 ∈ V (idx x_1)
hx : ∀ (x_1 : ↥S), (𝒰.f (f (idx x_1))) (x x_1) = x_1
⊢ Finite
    { I₀ := ULift.{w, 0} (Fin n), X := fun i ↦ Γ(𝒰.X (f i.down), V i.down), f := fun i ↦ ⋯.fromSpec ≫ 𝒰.f (f i.down),
        idx := fun s ↦ { down := idx s }, covers := ⋯, map_prop := ⋯ }.I₀

pp: case refine_4
P : MorphismProperty Scheme
S : Scheme
𝒰 : Scheme.Cover (Scheme.precoverage P) S
inst✝² : P.RespectsLeft IsOpenImmersion
inst✝¹ : CompactSpace ↥S
inst✝ : QuasiCompactCover 𝒰.toPreZeroHypercover
n : ℕ
f : Fin n → 𝒰.I₀
V : (i : Fin n) → (𝒰.X (f i)).Opens
hV : ∀ (i : Fin n), IsAffineOpen (V i)
idx : ↥S → Fin n
x : (x : ↥S) → ↥(𝒰.X (f (idx x)))
hmem : ∀ (x_1 : ↥S), x x_1 ∈ V (idx x_1)
hx : ∀ (x_1 : ↥S), (𝒰.f (f (idx x_1))) (x x_1) = x_1
⊢ ∀
    (j :
      { I₀ := ULift.{w, 0} (Fin n), X := fun i ↦ Γ(𝒰.X (f i.down), V i.down), f := fun i ↦ ⋯.fromSpec ≫ 𝒰.f (f i.down),
            idx := fun s ↦ { down := idx s }, covers := ⋯, map_prop := ⋯ }.cover.I₀),
    IsOpenImmersion ({ s₀ := fun i ↦ f i.down, h₀ := fun i ↦ ⋯.fromSpec, w₀ := ⋯ }.h₀ j)

Tactic:
·

Goal state after:
case refine_3
P : MorphismProperty Scheme
S : Scheme
𝒰 : Scheme.Cover (Scheme.precoverage P) S
inst✝² : P.RespectsLeft IsOpenImmersion
inst✝¹ : CompactSpace ↥S
inst✝ : QuasiCompactCover 𝒰.toPreZeroHypercover
n : ℕ
f : Fin n → 𝒰.I₀
V : (i : Fin n) → (𝒰.X (f i)).Opens
hV : ∀ (i : Fin n), IsAffineOpen (V i)
idx : ↥S → Fin n
x : (x : ↥S) → ↥(𝒰.X (f (idx x)))
hmem : ∀ (x_1 : ↥S), x x_1 ∈ V (idx x_1)
hx : ∀ (x_1 : ↥S), (𝒰.f (f (idx x_1))) (x x_1) = x_1
⊢ Finite
    { I₀ := ULift.{w, 0} (Fin n), X := fun i ↦ Γ(𝒰.X (f i.down), V i.down), f := fun i ↦ ⋯.fromSpec ≫ 𝒰.f (f i.down),
        idx := fun s ↦ { down := idx s }, covers := ⋯, map_prop := ⋯ }.I₀
Module: Mathlib.AlgebraicGeometry.Cover.QuasiCompact

Goal state before:
pp: case refine_4
P : MorphismProperty Scheme
S : Scheme
𝒰 : Scheme.Cover (Scheme.precoverage P) S
inst✝² : P.RespectsLeft IsOpenImmersion
inst✝¹ : CompactSpace ↥S
inst✝ : QuasiCompactCover 𝒰.toPreZeroHypercover
n : ℕ
f : Fin n → 𝒰.I₀
V : (i : Fin n) → (𝒰.X (f i)).Opens
hV : ∀ (i : Fin n), IsAffineOpen (V i)
idx : ↥S → Fin n
x : (x : ↥S) → ↥(𝒰.X (f (idx x)))
hmem : ∀ (x_1 : ↥S), x x_1 ∈ V (idx x_1)
hx : ∀ (x_1 : ↥S), (𝒰.f (f (idx x_1))) (x x_1) = x_1
⊢ ∀
    (j :
      { I₀ := ULift.{w, 0} (Fin n), X := fun i ↦ Γ(𝒰.X (f i.down), V i.down), f := fun i ↦ ⋯.fromSpec ≫ 𝒰.f (f i.down),
            idx := fun s ↦ { down := idx s }, covers := ⋯, map_prop := ⋯ }.cover.I₀),
    IsOpenImmersion ({ s₀ := fun i ↦ f i.down, h₀ := fun i ↦ ⋯.fromSpec, w₀ := ⋯ }.h₀ j)

Tactic:
·

Goal state after:
case refine_4
P : MorphismProperty Scheme
S : Scheme
𝒰 : Scheme.Cover (Scheme.precoverage P) S
inst✝² : P.RespectsLeft IsOpenImmersion
inst✝¹ : CompactSpace ↥S
inst✝ : QuasiCompactCover 𝒰.toPreZeroHypercover
n : ℕ
f : Fin n → 𝒰.I₀
V : (i : Fin n) → (𝒰.X (f i)).Opens
hV : ∀ (i : Fin n), IsAffineOpen (V i)
idx : ↥S → Fin n
x : (x : ↥S) → ↥(𝒰.X (f (idx x)))
hmem : ∀ (x_1 : ↥S), x x_1 ∈ V (idx x_1)
hx : ∀ (x_1 : ↥S), (𝒰.f (f (idx x_1))) (x x_1) = x_1
⊢ ∀
    (j :
      { I₀ := ULift.{w, 0} (Fin n), X := fun i ↦ Γ(𝒰.X (f i.down), V i.down), f := fun i ↦ ⋯.fromSpec ≫ 𝒰.f (f i.down),
            idx := fun s ↦ { down := idx s }, covers := ⋯, map_prop := ⋯ }.cover.I₀),
    IsOpenImmersion ({ s₀ := fun i ↦ f i.down, h₀ := fun i ↦ ⋯.fromSpec, w₀ := ⋯ }.h₀ j)