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

Goal state before:
pp: 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
hUST : UT ≤ f ⁻¹ᵁ US
ι : Type u_1
inst✝ : Finite ι
VX : ι → X.Opens
hT : (CommRingCat.Hom.hom (Scheme.Hom.appLE f US UT hUST)).Flat
this✝ : ∀ (i : ι), VX i ≤ iX ⁻¹ᵁ US
algInst✝¹ : Algebra ↑Γ(S, US) ↑Γ(T, UT) := (CommRingCat.Hom.hom (Scheme.Hom.appLE f US UT hUST)).toAlgebra
algebraizeInst✝ : Module.Flat ↑Γ(S, US) ↑Γ(T, UT)
i : ι
hUSX : iSup VX ≤ iX ⁻¹ᵁ US
hV : ∀ (i : ι), Mono (pushoutSection H hUST ⋯ ⋯)
algInst✝ : Algebra ↑Γ(S, US) ↑Γ(X, iSup VX) := (CommRingCat.Hom.hom (Scheme.Hom.appLE iX US (iSup VX) hUSX)).toAlgebra
this : (i : ι) → Algebra ↑Γ(S, US) ↑Γ(X, VX i) :=
  fun i ↦ (CommRingCat.Hom.hom (Scheme.Hom.appLE iX US (VX i) ⋯)).toAlgebra
⊢ g ⁻¹ᵁ VX i ⊓ iY ⁻¹ᵁ UT ≤ g ⁻¹ᵁ iSup VX ⊓ iY ⁻¹ᵁ UT

Tactic:
;

Goal state after:
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
hUST : UT ≤ f ⁻¹ᵁ US
ι : Type u_1
inst✝ : Finite ι
VX : ι → X.Opens
hT : (CommRingCat.Hom.hom (Scheme.Hom.appLE f US UT hUST)).Flat
this✝ : ∀ (i : ι), VX i ≤ iX ⁻¹ᵁ US
algInst✝¹ : Algebra ↑Γ(S, US) ↑Γ(T, UT) := (CommRingCat.Hom.hom (Scheme.Hom.appLE f US UT hUST)).toAlgebra
algebraizeInst✝ : Module.Flat ↑Γ(S, US) ↑Γ(T, UT)
i : ι
hUSX : iSup VX ≤ iX ⁻¹ᵁ US
hV : ∀ (i : ι), Mono (pushoutSection H hUST ⋯ ⋯)
algInst✝ : Algebra ↑Γ(S, US) ↑Γ(X, iSup VX) := (CommRingCat.Hom.hom (Scheme.Hom.appLE iX US (iSup VX) hUSX)).toAlgebra
this : (i : ι) → Algebra ↑Γ(S, US) ↑Γ(X, VX i) :=
  fun i ↦ (CommRingCat.Hom.hom (Scheme.Hom.appLE iX US (VX i) ⋯)).toAlgebra
⊢ g ⁻¹ᵁ VX i ⊓ iY ⁻¹ᵁ UT ≤ g ⁻¹ᵁ iSup VX ⊓ iY ⁻¹ᵁ UT
Module: Mathlib.AlgebraicGeometry.Morphisms.Flat

Goal state before:
pp: case hUU'
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
hUST : UT ≤ f ⁻¹ᵁ US
ι : Type u_1
inst✝ : Finite ι
VX : ι → X.Opens
hT : (CommRingCat.Hom.hom (Scheme.Hom.appLE f US UT hUST)).Flat
this✝ : ∀ (i : ι), VX i ≤ iX ⁻¹ᵁ US
algInst✝¹ : Algebra ↑Γ(S, US) ↑Γ(T, UT) := ⋯
algebraizeInst✝ : Module.Flat ↑Γ(S, US) ↑Γ(T, UT)
i : ι
hUSX : iSup VX ≤ iX ⁻¹ᵁ US
hV : ∀ (i : ι), Mono (pushoutSection H hUST ⋯ ⋯)
algInst✝ : Algebra ↑Γ(S, US) ↑Γ(X, iSup VX) := ⋯
this : (i : ι) → Algebra ↑Γ(S, US) ↑Γ(X, VX i) := ⋯
⊢ VX i ≤ iSup VX

Tactic:
;

Goal state after:
case hUU'
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
hUST : UT ≤ f ⁻¹ᵁ US
ι : Type u_1
inst✝ : Finite ι
VX : ι → X.Opens
hT : (CommRingCat.Hom.hom (Scheme.Hom.appLE f US UT hUST)).Flat
this✝ : ∀ (i : ι), VX i ≤ iX ⁻¹ᵁ US
algInst✝¹ : Algebra ↑Γ(S, US) ↑Γ(T, UT) := ⋯
algebraizeInst✝ : Module.Flat ↑Γ(S, US) ↑Γ(T, UT)
i : ι
hUSX : iSup VX ≤ iX ⁻¹ᵁ US
hV : ∀ (i : ι), Mono (pushoutSection H hUST ⋯ ⋯)
algInst✝ : Algebra ↑Γ(S, US) ↑Γ(X, iSup VX) := ⋯
this : (i : ι) → Algebra ↑Γ(S, US) ↑Γ(X, VX i) := ⋯
⊢ VX i ≤ iSup VX
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
S X : Scheme
v : n → ↑Γ(X, ⊤)
x✝ : n
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
;

Goal state after:
n : Type u
S X : Scheme
v : n → ↑Γ(X, ⊤)
x✝ : n
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
S X : Scheme
inst✝ : X.Over S
v : n → ↑Γ(X, ⊤)
i : n
⊢ (fun f i ↦ (ConcreteCategory.hom (Scheme.Hom.appTop ↑f)) (coord S i)) ((fun v ↦ ⟨homOfVector (X ↘ S) v, ⋯⟩) v) i = v i

Tactic:
;

Goal state after:
n : Type u
S X : Scheme
inst✝ : X.Over S
v : n → ↑Γ(X, ⊤)
i : n
⊢ (fun f i ↦ (ConcreteCategory.hom (Scheme.Hom.appTop ↑f)) (coord S i)) ((fun v ↦ ⟨homOfVector (X ↘ S) v, ⋯⟩) v) i = v 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:
· intro h
    induction h with
    | rel x y h =>
      obtain ⟨f, h⟩ := h
      exact ⟨y.1, f, 𝟙 _, by simpa using h.symm⟩
    | refl x => exact ⟨x.1, 𝟙 _, 𝟙 _, rfl⟩
    | symm _ _ _ h =>
      obtain ⟨k, f, g, h⟩ := h
      exact ⟨k, g, f, h.symm⟩
    | trans x y z _ _ h h' =>
      obtain ⟨k, f, g, h⟩ := h
      obtain ⟨k', f', g', h'⟩ := h'
      obtain ⟨l, a, b, h''⟩ := span g f'
      refine ⟨l, f ≫ a, g' ≫ b, ?_⟩
      simp only [map_comp, comp_apply, h, ← h']
      simp [← comp_apply, ← map_comp, h'']

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.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
R S : CommRingCat
φ : R ⟶ S
i✝ : n
| (ConcreteCategory.hom (Scheme.Hom.app (map n (Spec.map φ)) ⊤)) (coord (Spec R) i✝)

Tactic:
;

Goal state after:
n : Type u
R S : CommRingCat
φ : R ⟶ S
i✝ : n
| (ConcreteCategory.hom (Scheme.Hom.app (map n (Spec.map φ)) ⊤)) (coord (Spec R) i✝)
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
R S : CommRingCat
φ : R ⟶ S
i✝ : n
| (ConcreteCategory.hom (Scheme.Hom.app (SpecIso n R).inv ⊤)) (coord (Spec R) i✝)

Tactic:
;

Goal state after:
n : Type u
R S : CommRingCat
φ : R ⟶ S
i✝ : n
| (ConcreteCategory.hom (Scheme.Hom.app (SpecIso n R).inv ⊤)) (coord (Spec R) i✝)
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
S✝ : Scheme
R S : CommRingCat
φ : R ⟶ S
this : (SpecIso n R).inv ≫ (SpecIso n R).hom = 𝟙 (Spec (CommRingCat.of (MvPolynomial n ↑R)))
⊢ (SpecIso n S).hom ≫ (Arrow.mk (Spec.map (CommRingCat.ofHom (MvPolynomial.map (CommRingCat.Hom.hom φ))))).hom =
    (Arrow.mk (map n (Spec.map φ))).hom ≫ (SpecIso n R).hom

Tactic:
;

Goal state after:
n : Type u
S✝ : Scheme
R S : CommRingCat
φ : R ⟶ S
this : (SpecIso n R).inv ≫ (SpecIso n R).hom = 𝟙 (Spec (CommRingCat.of (MvPolynomial n ↑R)))
⊢ (SpecIso n S).hom ≫ (Arrow.mk (Spec.map (CommRingCat.ofHom (MvPolynomial.map (CommRingCat.Hom.hom φ))))).hom =
    (Arrow.mk (map n (Spec.map φ))).hom ≫ (SpecIso n R).hom
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n✝ : Type u
S : Scheme
n : Type uᵒᵖ
x✝ : Scheme
⊢ { app := reindex ⇑(ConcreteCategory.hom (𝟙 n).unop), naturality := ⋯ }.app x✝ =
    (𝟙
          { obj := AffineSpace (Opposite.unop n), map := fun {X Y} ↦ map (Opposite.unop n), map_id := ⋯,
            map_comp := ⋯ }).app
      x✝

Tactic:
;

Goal state after:
n✝ : Type u
S : Scheme
n : Type uᵒᵖ
x✝ : Scheme
⊢ { app := reindex ⇑(ConcreteCategory.hom (𝟙 n).unop), naturality := ⋯ }.app x✝ =
    (𝟙
          { obj := AffineSpace (Opposite.unop n), map := fun {X Y} ↦ map (Opposite.unop n), map_id := ⋯,
            map_comp := ⋯ }).app
      x✝
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
S : Scheme
X✝ Y✝ Z✝ : Type uᵒᵖ
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
x✝ : Scheme
⊢ { app := reindex ⇑(ConcreteCategory.hom (f ≫ g).unop), naturality := ⋯ }.app x✝ =
    ({ app := reindex ⇑(ConcreteCategory.hom f.unop), naturality := ⋯ } ≫
          { app := reindex ⇑(ConcreteCategory.hom g.unop), naturality := ⋯ }).app
      x✝

Tactic:
;

Goal state after:
n : Type u
S : Scheme
X✝ Y✝ Z✝ : Type uᵒᵖ
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
x✝ : Scheme
⊢ { app := reindex ⇑(ConcreteCategory.hom (f ≫ g).unop), naturality := ⋯ }.app x✝ =
    ({ app := reindex ⇑(ConcreteCategory.hom f.unop), naturality := ⋯ } ≫
          { app := reindex ⇑(ConcreteCategory.hom g.unop), naturality := ⋯ }).app
      x✝
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
S : Scheme
X✝ Y✝ Z✝ : Type uᵒᵖ
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
x✝ : Scheme
⊢ reindex (⇑(ConcreteCategory.hom (g.unop ≫ f.unop))) x✝ =
    reindex (⇑(ConcreteCategory.hom f.unop)) x✝ ≫ reindex (⇑(ConcreteCategory.hom g.unop)) x✝

Tactic:
;

Goal state after:
n : Type u
S : Scheme
X✝ Y✝ Z✝ : Type uᵒᵖ
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
x✝ : Scheme
⊢ reindex (⇑(ConcreteCategory.hom (g.unop ≫ f.unop))) x✝ =
    reindex (⇑(ConcreteCategory.hom f.unop)) x✝ ≫ reindex (⇑(ConcreteCategory.hom g.unop)) x✝
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: case refine_1
n : ℕ
P : (R : Type u) → [inst : CommRing R] → InductionObj R n → Prop
hP₁ : ∀ (R : Type u) [inst : CommRing R], P R { val := 0 }
hP₂ :
  ∀ (R : Type u) [inst : CommRing R] (e : InductionObj R n) (i : Fin n),
    (e.val i).Monic → (∀ (j : Fin n), j ≠ i → e.val j = 0) → P R e
hP₃ :
  ∀ (R : Type u) [inst : CommRing R] (e : InductionObj R n) (i j : Fin n),
    (e.val i).Monic →
      (e.val i).degree ≤ (e.val j).degree → i ≠ j → P R { val := Function.update e.val j (e.val j %ₘ e.val i) } → P R e
hP₄ :
  ∀ (R : Type u) [inst : CommRing R] (c : R) (i : Fin n) (e : InductionObj R n),
    c = (e.val i).leadingCoeff →
      c ≠ 0 →
        P (Away c)
            { val := Polynomial.C (IsLocalization.Away.invSelf c) • ⇑(mapRingHom (algebraMap R (Away c))) ∘ e.val } →
          P (R ⧸ Ideal.span {c}) { val := ⇑(mapRingHom (algebraMap R (R ⧸ Ideal.span {c}))) ∘ e.val } → P R e
v : DegreeType n
H_IH : ∀ y < v, ∀ {R : Type u} [inst : CommRing R] (e : InductionObj R n), y = e.degree → P R e
R : Type u
inst✝ : CommRing R
e : InductionObj R n
hv : v = e.degree
h✝ : Nontrivial R
he0 : ∃ x, ¬e.val x = 0
H : ¬∃ i, (e.val i).Monic ∧ ∀ (j : Fin n), e.val j ≠ 0 → (e.val i).degree ≤ (e.val j).degree
i : Fin n
hi : e.val i ≠ 0
i_min : ∀ (j : Fin n), e.val j ≠ 0 → (e.val i).degree ≤ (e.val j).degree
j : Fin n
⊢ (Polynomial.degree ∘ { val := ⇑(mapRingHom (algebraMap R (R ⧸ Ideal.span {(e.val i).leadingCoeff}))) ∘ e.val }.val)
      j ≤
    (Polynomial.degree ∘ e.val) j

Tactic:
;

Goal state after:
case refine_1
n : ℕ
P : (R : Type u) → [inst : CommRing R] → InductionObj R n → Prop
hP₁ : ∀ (R : Type u) [inst : CommRing R], P R { val := 0 }
hP₂ :
  ∀ (R : Type u) [inst : CommRing R] (e : InductionObj R n) (i : Fin n),
    (e.val i).Monic → (∀ (j : Fin n), j ≠ i → e.val j = 0) → P R e
hP₃ :
  ∀ (R : Type u) [inst : CommRing R] (e : InductionObj R n) (i j : Fin n),
    (e.val i).Monic →
      (e.val i).degree ≤ (e.val j).degree → i ≠ j → P R { val := Function.update e.val j (e.val j %ₘ e.val i) } → P R e
hP₄ :
  ∀ (R : Type u) [inst : CommRing R] (c : R) (i : Fin n) (e : InductionObj R n),
    c = (e.val i).leadingCoeff →
      c ≠ 0 →
        P (Away c)
            { val := Polynomial.C (IsLocalization.Away.invSelf c) • ⇑(mapRingHom (algebraMap R (Away c))) ∘ e.val } →
          P (R ⧸ Ideal.span {c}) { val := ⇑(mapRingHom (algebraMap R (R ⧸ Ideal.span {c}))) ∘ e.val } → P R e
v : DegreeType n
H_IH : ∀ y < v, ∀ {R : Type u} [inst : CommRing R] (e : InductionObj R n), y = e.degree → P R e
R : Type u
inst✝ : CommRing R
e : InductionObj R n
hv : v = e.degree
h✝ : Nontrivial R
he0 : ∃ x, ¬e.val x = 0
H : ¬∃ i, (e.val i).Monic ∧ ∀ (j : Fin n), e.val j ≠ 0 → (e.val i).degree ≤ (e.val j).degree
i : Fin n
hi : e.val i ≠ 0
i_min : ∀ (j : Fin n), e.val j ≠ 0 → (e.val i).degree ≤ (e.val j).degree
j : Fin n
⊢ (Polynomial.degree ∘ { val := ⇑(mapRingHom (algebraMap R (R ⧸ Ideal.span {(e.val i).leadingCoeff}))) ∘ e.val }.val)
      j ≤
    (Polynomial.degree ∘ e.val) j
Module: Mathlib.AlgebraicGeometry.Morphisms.Flat

Goal state before:
pp: X✝ Y✝ Z : Scheme
f✝ : X✝ ⟶ Y✝
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
ι : Type u
inst✝ : Finite ι
VX : ι → X.Opens
hVU : iSup VX = UX
i j : ι
⊢ VX i ≤ iX ⁻¹ᵁ US

Tactic:
;

Goal state after:
X✝ Y✝ Z : Scheme
f✝ : X✝ ⟶ Y✝
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
ι : Type u
inst✝ : Finite ι
VX : ι → X.Opens
hVU : iSup VX = UX
i j : ι
⊢ VX i ≤ iX ⁻¹ᵁ US
Module: Mathlib.AlgebraicGeometry.Morphisms.Flat

Goal state before:
pp: case refine_1
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
hUST : UT ≤ f ⁻¹ᵁ US
UY : Y.Opens
ι : Type u
inst✝ : Finite ι
VX : ι → X.Opens
hT : (CommRingCat.Hom.hom (Scheme.Hom.appLE f US UT hUST)).Flat
D : CategoryTheory.Pairwise ι ⥤ X.Opens := Pairwise.diagram VX
hUSX : iSup VX ≤ iX ⁻¹ᵁ US
hUY : UY = g ⁻¹ᵁ iSup VX ⊓ iY ⁻¹ᵁ UT
hV : ∀ (i : ι), IsIso (pushoutSection H hUST ⋯ ⋯)
hV' : ∀ (i j : ι), Mono (pushoutSection H hUST ⋯ ⋯)
⊢ ∀ (i : CategoryTheory.Pairwise ι), D.obj i ≤ iSup VX

Tactic:
;

Goal state after:
case refine_1
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
hUST : UT ≤ f ⁻¹ᵁ US
UY : Y.Opens
ι : Type u
inst✝ : Finite ι
VX : ι → X.Opens
hT : (CommRingCat.Hom.hom (Scheme.Hom.appLE f US UT hUST)).Flat
D : CategoryTheory.Pairwise ι ⥤ X.Opens := Pairwise.diagram VX
hUSX : iSup VX ≤ iX ⁻¹ᵁ US
hUY : UY = g ⁻¹ᵁ iSup VX ⊓ iY ⁻¹ᵁ UT
hV : ∀ (i : ι), IsIso (pushoutSection H hUST ⋯ ⋯)
hV' : ∀ (i j : ι), Mono (pushoutSection H hUST ⋯ ⋯)
⊢ ∀ (i : CategoryTheory.Pairwise ι), D.obj i ≤ iSup VX
Module: Mathlib.AlgebraicGeometry.Morphisms.Flat

Goal state before:
pp: case refine_1.single
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
hUST : UT ≤ f ⁻¹ᵁ US
UY : Y.Opens
ι : Type u
inst✝ : Finite ι
VX : ι → X.Opens
hT : (CommRingCat.Hom.hom (Scheme.Hom.appLE f US UT hUST)).Flat
D : CategoryTheory.Pairwise ι ⥤ X.Opens := Pairwise.diagram VX
hUSX : iSup VX ≤ iX ⁻¹ᵁ US
hUY : UY = g ⁻¹ᵁ iSup VX ⊓ iY ⁻¹ᵁ UT
hV : ∀ (i : ι), IsIso (pushoutSection H hUST ⋯ ⋯)
hV' : ∀ (i j : ι), Mono (pushoutSection H hUST ⋯ ⋯)
i : ι
⊢ D.obj (Pairwise.single i) ≤ iSup VX

pp: case refine_1.pair
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
hUST : UT ≤ f ⁻¹ᵁ US
UY : Y.Opens
ι : Type u
inst✝ : Finite ι
VX : ι → X.Opens
hT : (CommRingCat.Hom.hom (Scheme.Hom.appLE f US UT hUST)).Flat
D : CategoryTheory.Pairwise ι ⥤ X.Opens := Pairwise.diagram VX
hUSX : iSup VX ≤ iX ⁻¹ᵁ US
hUY : UY = g ⁻¹ᵁ iSup VX ⊓ iY ⁻¹ᵁ UT
hV : ∀ (i : ι), IsIso (pushoutSection H hUST ⋯ ⋯)
hV' : ∀ (i j : ι), Mono (pushoutSection H hUST ⋯ ⋯)
i j : ι
⊢ D.obj (Pairwise.pair i j) ≤ iSup VX

Tactic:
;

Goal state after:
case refine_1.single
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
hUST : UT ≤ f ⁻¹ᵁ US
UY : Y.Opens
ι : Type u
inst✝ : Finite ι
VX : ι → X.Opens
hT : (CommRingCat.Hom.hom (Scheme.Hom.appLE f US UT hUST)).Flat
D : CategoryTheory.Pairwise ι ⥤ X.Opens := Pairwise.diagram VX
hUSX : iSup VX ≤ iX ⁻¹ᵁ US
hUY : UY = g ⁻¹ᵁ iSup VX ⊓ iY ⁻¹ᵁ UT
hV : ∀ (i : ι), IsIso (pushoutSection H hUST ⋯ ⋯)
hV' : ∀ (i j : ι), Mono (pushoutSection H hUST ⋯ ⋯)
i : ι
⊢ D.obj (Pairwise.single i) ≤ iSup VX

case refine_1.pair
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
hUST : UT ≤ f ⁻¹ᵁ US
UY : Y.Opens
ι : Type u
inst✝ : Finite ι
VX : ι → X.Opens
hT : (CommRingCat.Hom.hom (Scheme.Hom.appLE f US UT hUST)).Flat
D : CategoryTheory.Pairwise ι ⥤ X.Opens := Pairwise.diagram VX
hUSX : iSup VX ≤ iX ⁻¹ᵁ US
hUY : UY = g ⁻¹ᵁ iSup VX ⊓ iY ⁻¹ᵁ UT
hV : ∀ (i : ι), IsIso (pushoutSection H hUST ⋯ ⋯)
hV' : ∀ (i j : ι), Mono (pushoutSection H hUST ⋯ ⋯)
i j : ι
⊢ D.obj (Pairwise.pair i j) ≤ iSup VX
Module: Mathlib.AlgebraicGeometry.Morphisms.Flat

Goal state before:
pp: case refine_2
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
hUST : UT ≤ f ⁻¹ᵁ US
UY : Y.Opens
ι : Type u
inst✝ : Finite ι
VX : ι → X.Opens
hT : (CommRingCat.Hom.hom (Scheme.Hom.appLE f US UT hUST)).Flat
D : CategoryTheory.Pairwise ι ⥤ X.Opens := Pairwise.diagram VX
hUSX : iSup VX ≤ iX ⁻¹ᵁ US
hUY : UY = g ⁻¹ᵁ iSup VX ⊓ iY ⁻¹ᵁ UT
hV : ∀ (i : ι), IsIso (pushoutSection H hUST ⋯ ⋯)
hV' : ∀ (i j : ι), Mono (pushoutSection H hUST ⋯ ⋯)
⊢ iSup VX ≤ iSup D.obj

Tactic:
;

Goal state after:
case refine_2
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
hUST : UT ≤ f ⁻¹ᵁ US
UY : Y.Opens
ι : Type u
inst✝ : Finite ι
VX : ι → X.Opens
hT : (CommRingCat.Hom.hom (Scheme.Hom.appLE f US UT hUST)).Flat
D : CategoryTheory.Pairwise ι ⥤ X.Opens := Pairwise.diagram VX
hUSX : iSup VX ≤ iX ⁻¹ᵁ US
hUY : UY = g ⁻¹ᵁ iSup VX ⊓ iY ⁻¹ᵁ UT
hV : ∀ (i : ι), IsIso (pushoutSection H hUST ⋯ ⋯)
hV' : ∀ (i j : ι), Mono (pushoutSection H hUST ⋯ ⋯)
⊢ iSup VX ≤ iSup D.obj
Module: Mathlib.AlgebraicGeometry.Morphisms.Flat

Goal state before:
pp: case hUU'
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
ι : Type u
inst✝ : Finite ι
VX : ι → X.Opens
hVU : iSup VX = UX
hV : ∀ (i : ι), IsIso (pushoutSection H hUST ⋯ ⋯)
hV' : ∀ (i j : ι), Mono (pushoutSection H hUST ⋯ ⋯)
hT : (CommRingCat.Hom.hom (Scheme.Hom.appLE f US UT hUST)).Flat
D : CategoryTheory.Pairwise ι ⥤ X.Opens := ⋯
h✝ : iSup D.obj = UX
c₀ : Cocone D := ⋯
F : (CategoryTheory.Pairwise ι)ᵒᵖ ⥤ CommRingCat := ⋯
X✝ Y✝ : X.Opens
h : X✝ ⟶ Y✝
⊢ X✝ ≤ Y✝

Tactic:
;

Goal state after:
case hUU'
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
ι : Type u
inst✝ : Finite ι
VX : ι → X.Opens
hVU : iSup VX = UX
hV : ∀ (i : ι), IsIso (pushoutSection H hUST ⋯ ⋯)
hV' : ∀ (i j : ι), Mono (pushoutSection H hUST ⋯ ⋯)
hT : (CommRingCat.Hom.hom (Scheme.Hom.appLE f US UT hUST)).Flat
D : CategoryTheory.Pairwise ι ⥤ X.Opens := ⋯
h✝ : iSup D.obj = UX
c₀ : Cocone D := ⋯
F : (CategoryTheory.Pairwise ι)ᵒᵖ ⥤ CommRingCat := ⋯
X✝ Y✝ : X.Opens
h : X✝ ⟶ Y✝
⊢ X✝ ≤ Y✝
Module: Mathlib.AlgebraicGeometry.Morphisms.Flat

Goal state before:
pp: 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
ι : Type u
inst✝ : Finite ι
VX : ι → X.Opens
hVU : iSup VX = UX
hV : ∀ (i : ι), IsIso (pushoutSection H hUST ⋯ ⋯)
hV' : ∀ (i j : ι), Mono (pushoutSection H hUST ⋯ ⋯)
hT : (CommRingCat.Hom.hom (Scheme.Hom.appLE f US UT hUST)).Flat
D : CategoryTheory.Pairwise ι ⥤ X.Opens := Pairwise.diagram VX
h : iSup D.obj = UX
c₀ : Cocone D := (colimit.cocone D).extend (eqToIso ⋯).hom
F : (CategoryTheory.Pairwise ι)ᵒᵖ ⥤ CommRingCat :=
  Under.lift (D.op ⋙ X.presheaf)
      ((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).map (Scheme.Hom.appLE iX US UX hUSX) ≫
        (Functor.mapCone X.presheaf c₀.op).π) ⋙
    Under.pushout (Scheme.Hom.appLE f US UT hUST) ⋙ Under.forget Γ(T, UT)
G : X.Opens ⥤ Y.Opens :=
  { obj := fun U ↦ g ⁻¹ᵁ U ⊓ iY ⁻¹ᵁ UT, map := fun {X_1 Y_1} h ↦ homOfLE ⋯, map_id := ⋯, map_comp := ⋯ }
i : (CategoryTheory.Pairwise ι)ᵒᵖ
⊢ D.obj (unop i) ≤ iSup D.obj

Tactic:
;

Goal state after:
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
ι : Type u
inst✝ : Finite ι
VX : ι → X.Opens
hVU : iSup VX = UX
hV : ∀ (i : ι), IsIso (pushoutSection H hUST ⋯ ⋯)
hV' : ∀ (i j : ι), Mono (pushoutSection H hUST ⋯ ⋯)
hT : (CommRingCat.Hom.hom (Scheme.Hom.appLE f US UT hUST)).Flat
D : CategoryTheory.Pairwise ι ⥤ X.Opens := Pairwise.diagram VX
h : iSup D.obj = UX
c₀ : Cocone D := (colimit.cocone D).extend (eqToIso ⋯).hom
F : (CategoryTheory.Pairwise ι)ᵒᵖ ⥤ CommRingCat :=
  Under.lift (D.op ⋙ X.presheaf)
      ((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).map (Scheme.Hom.appLE iX US UX hUSX) ≫
        (Functor.mapCone X.presheaf c₀.op).π) ⋙
    Under.pushout (Scheme.Hom.appLE f US UT hUST) ⋙ Under.forget Γ(T, UT)
G : X.Opens ⥤ Y.Opens :=
  { obj := fun U ↦ g ⁻¹ᵁ U ⊓ iY ⁻¹ᵁ UT, map := fun {X_1 Y_1} h ↦ homOfLE ⋯, map_id := ⋯, map_comp := ⋯ }
i : (CategoryTheory.Pairwise ι)ᵒᵖ
⊢ D.obj (unop i) ≤ iSup D.obj
Module: Mathlib.Topology.LocallyFinsupp.Pushforward

Goal state before:
pp: X : Type u_1
Y : Type u_2
R : Type u_3
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
f : X → Y
hf✝ : IsSpectralMap f
w : X → R
inst✝¹ : Semiring R
W : Set Y
hW : IsOpen[inst✝²] W
c✝ : locallyFinsupp X R
inst✝ : PrespectralSpace Y
hf : IsSpectralMap f
c : locallyFinsupp X R
y : Y
x✝ : y ∈ univ
U : Set Y
hU : U ∈ {U | IsOpen[inst✝²] U ∧ IsCompact U} ∧ y ∈ U ∧ U ⊆ ⊤
⊢ f ⁻¹' U ∩ {a | (f ⁻¹' {f a} ∩ locallyFinsuppWithin.support c).Nonempty} ∩ locallyFinsuppWithin.support c ⊆ f ⁻¹' U

Tactic:
;

Goal state after:
X : Type u_1
Y : Type u_2
R : Type u_3
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
f : X → Y
hf✝ : IsSpectralMap f
w : X → R
inst✝¹ : Semiring R
W : Set Y
hW : IsOpen[inst✝²] W
c✝ : locallyFinsupp X R
inst✝ : PrespectralSpace Y
hf : IsSpectralMap f
c : locallyFinsupp X R
y : Y
x✝ : y ∈ univ
U : Set Y
hU : U ∈ {U | IsOpen[inst✝²] U ∧ IsCompact U} ∧ y ∈ U ∧ U ⊆ ⊤
⊢ f ⁻¹' U ∩ {a | (f ⁻¹' {f a} ∩ locallyFinsuppWithin.support c).Nonempty} ∩ locallyFinsuppWithin.support c ⊆ f ⁻¹' U
Module: Mathlib.AlgebraicGeometry.SpreadingOut

Goal state before:
pp: case hy
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥X
hx : x ∈ U
f : ↑Γ(X, U)
hf : x ∈ X.basicOpen f
H : ∀ (x_1 : ↑(X.presheaf.obj (Opposite.op U))), (ConcreteCategory.hom (X.presheaf.germ U x hx)) x_1 = 0 → x_1 = 0
this : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
t : ↑Γ(X, U)
s : ↥(Submonoid.powers f)
ht :
  (algebraMap ↑Γ(X, U) ↑(X.presheaf.obj (Opposite.op (X.basicOpen f)))) t *
      IsLocalization.mk' (↑(X.presheaf.obj (Opposite.op (X.basicOpen f)))) 1 s ∈
    RingHom.ker (ConcreteCategory.hom (X.presheaf.germ (X.basicOpen f) x hf))
⊢ IsUnit (IsLocalization.mk' (↑(X.presheaf.obj (Opposite.op (X.basicOpen f)))) 1 s)

pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥X
hx : x ∈ U
f : ↑Γ(X, U)
hf : x ∈ X.basicOpen f
H : ∀ (x_1 : ↑(X.presheaf.obj (Opposite.op U))), (ConcreteCategory.hom (X.presheaf.germ U x hx)) x_1 = 0 → x_1 = 0
this : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
t : ↑Γ(X, U)
s : ↥(Submonoid.powers f)
ht : (ConcreteCategory.hom (X.presheaf.germ U x ⋯)) t = 0
⊢ IsLocalization.mk' (↑(X.presheaf.obj (Opposite.op (X.basicOpen f)))) t s = 0

Tactic:
;

Goal state after:
case hy
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥X
hx : x ∈ U
f : ↑Γ(X, U)
hf : x ∈ X.basicOpen f
H : ∀ (x_1 : ↑(X.presheaf.obj (Opposite.op U))), (ConcreteCategory.hom (X.presheaf.germ U x hx)) x_1 = 0 → x_1 = 0
this : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
t : ↑Γ(X, U)
s : ↥(Submonoid.powers f)
ht :
  (algebraMap ↑Γ(X, U) ↑(X.presheaf.obj (Opposite.op (X.basicOpen f)))) t *
      IsLocalization.mk' (↑(X.presheaf.obj (Opposite.op (X.basicOpen f)))) 1 s ∈
    RingHom.ker (ConcreteCategory.hom (X.presheaf.germ (X.basicOpen f) x hf))
⊢ IsUnit (IsLocalization.mk' (↑(X.presheaf.obj (Opposite.op (X.basicOpen f)))) 1 s)

X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥X
hx : x ∈ U
f : ↑Γ(X, U)
hf : x ∈ X.basicOpen f
H : ∀ (x_1 : ↑(X.presheaf.obj (Opposite.op U))), (ConcreteCategory.hom (X.presheaf.germ U x hx)) x_1 = 0 → x_1 = 0
this : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
t : ↑Γ(X, U)
s : ↥(Submonoid.powers f)
ht : (ConcreteCategory.hom (X.presheaf.germ U x ⋯)) t = 0
⊢ IsLocalization.mk' (↑(X.presheaf.obj (Opposite.op (X.basicOpen f)))) t s = 0