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

Goal state before:
pp: case mp
P : MorphismProperty Scheme
S : Scheme
inst✝¹ : P.IsStableUnderBaseChange
X : Over S
𝒰 : Cover (precoverage P) X.left
inst✝ : Cover.Over S 𝒰
V : Scheme
f : V ⟶ X.left
⊢ (∃ Y h g, 𝒰.toPresieveOver g ∧ h ≫ g = Over.homMk f ⋯) → ∃ Y h g, Presieve.ofArrows 𝒰.X 𝒰.f g ∧ h ≫ g = f

pp: case mpr
P : MorphismProperty Scheme
S : Scheme
inst✝¹ : P.IsStableUnderBaseChange
X : Over S
𝒰 : Cover (precoverage P) X.left
inst✝ : Cover.Over S 𝒰
V : Scheme
f : V ⟶ X.left
⊢ (∃ Y h g, Presieve.ofArrows 𝒰.X 𝒰.f g ∧ h ≫ g = f) → ∃ Y h g, 𝒰.toPresieveOver g ∧ h ≫ g = Over.homMk f ⋯

Tactic:
·

Goal state after:
case mp
P : MorphismProperty Scheme
S : Scheme
inst✝¹ : P.IsStableUnderBaseChange
X : Over S
𝒰 : Cover (precoverage P) X.left
inst✝ : Cover.Over S 𝒰
V : Scheme
f : V ⟶ X.left
⊢ (∃ Y h g, 𝒰.toPresieveOver g ∧ h ≫ g = Over.homMk f ⋯) → ∃ Y h g, Presieve.ofArrows 𝒰.X 𝒰.f g ∧ h ≫ g = f
Module: Mathlib.AlgebraicGeometry.Sites.Small

Goal state before:
pp: case mpr
P : MorphismProperty Scheme
S : Scheme
inst✝¹ : P.IsStableUnderBaseChange
X : Over S
𝒰 : Cover (precoverage P) X.left
inst✝ : Cover.Over S 𝒰
V : Scheme
f : V ⟶ X.left
⊢ (∃ Y h g, Presieve.ofArrows 𝒰.X 𝒰.f g ∧ h ≫ g = f) → ∃ Y h g, 𝒰.toPresieveOver g ∧ h ≫ g = Over.homMk f ⋯

Tactic:
·

Goal state after:
case mpr
P : MorphismProperty Scheme
S : Scheme
inst✝¹ : P.IsStableUnderBaseChange
X : Over S
𝒰 : Cover (precoverage P) X.left
inst✝ : Cover.Over S 𝒰
V : Scheme
f : V ⟶ X.left
⊢ (∃ Y h g, Presieve.ofArrows 𝒰.X 𝒰.f g ∧ h ≫ g = f) → ∃ Y h g, 𝒰.toPresieveOver g ∧ h ≫ g = Over.homMk f ⋯
Module: Mathlib.AlgebraicGeometry.ValuativeCriterion

Goal state before:
pp: case mp
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
⊢ Existence f✝ → (topologically @SpecializingMap).universally f✝

pp: case mpr
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
⊢ (topologically @SpecializingMap).universally f✝ → Existence f✝

Tactic:
·

Goal state after:
case mp
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
⊢ Existence f✝ → (topologically @SpecializingMap).universally f✝
Module: Mathlib.AlgebraicGeometry.ValuativeCriterion

Goal state before:
pp: case a
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
a✝ : Existence f✝
⊢ ?mp.a✝ ≤ topologically @SpecializingMap

pp: case mp.a
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
a✝ : Existence f✝
⊢ MorphismProperty.universally ?mp.a✝ f✝

pp: case mp.a
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
a✝ : Existence f✝
⊢ MorphismProperty Scheme

Tactic:
·

Goal state after:
case a
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
a✝ : Existence f✝
⊢ ?mp.a✝ ≤ topologically @SpecializingMap
Module: Mathlib.AlgebraicGeometry.ValuativeCriterion

Goal state before:
pp: case mp.a
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
a✝ : Existence f✝
⊢ Existence.universally f✝

Tactic:
·

Goal state after:
case mp.a
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
a✝ : Existence f✝
⊢ Existence.universally f✝
Module: Mathlib.AlgebraicGeometry.ValuativeCriterion

Goal state before:
pp: case mpr
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
⊢ (topologically @SpecializingMap).universally f✝ → Existence f✝

Tactic:
·

Goal state after:
case mpr
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
⊢ (topologically @SpecializingMap).universally f✝ → Existence f✝
Module: Mathlib.AlgebraicGeometry.Sites.Small

Goal state before:
pp: case mp
P : MorphismProperty Scheme
S : Scheme
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
inst✝ : P.RespectsIso
X : Over S
R : Sieve X
⊢ (Sieve.overEquiv X) R ∈ (grothendieckTopology P) X.left → R ∈ (overPretopology P S).toGrothendieck X

pp: case mpr
P : MorphismProperty Scheme
S : Scheme
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
inst✝ : P.RespectsIso
X : Over S
R : Sieve X
⊢ R ∈ (overPretopology P S).toGrothendieck X → (Sieve.overEquiv X) R ∈ (grothendieckTopology P) X.left

Tactic:
·

Goal state after:
case mp
P : MorphismProperty Scheme
S : Scheme
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
inst✝ : P.RespectsIso
X : Over S
R : Sieve X
⊢ (Sieve.overEquiv X) R ∈ (grothendieckTopology P) X.left → R ∈ (overPretopology P S).toGrothendieck X
Module: Mathlib.AlgebraicGeometry.Sites.Small

Goal state before:
pp: case mpr
P : MorphismProperty Scheme
S : Scheme
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
inst✝ : P.RespectsIso
X : Over S
R : Sieve X
⊢ R ∈ (overPretopology P S).toGrothendieck X → (Sieve.overEquiv X) R ∈ (grothendieckTopology P) X.left

Tactic:
·

Goal state after:
case mpr
P : MorphismProperty Scheme
S : Scheme
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
inst✝ : P.RespectsIso
X : Over S
R : Sieve X
⊢ R ∈ (overPretopology P S).toGrothendieck X → (Sieve.overEquiv X) R ∈ (grothendieckTopology P) X.left
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper

Goal state before:
pp: case refine_1
σ : Type u_1
A : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
i j : (affineOpenCover 𝒜).openCover.I₀
⊢ (affineOpenCover 𝒜).f i ≫ toSpecZero 𝒜 = Spec.map (CommRingCat.ofHom (algebraMap (↥(𝒜 0)) (Away 𝒜 ↑i.snd)))

pp: case refine_2
σ : Type u_1
A : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
i j : (affineOpenCover 𝒜).openCover.I₀
⊢ (affineOpenCover 𝒜).f j ≫ toSpecZero 𝒜 = Spec.map (CommRingCat.ofHom (algebraMap (↥(𝒜 0)) (Away 𝒜 ↑j.snd)))

Tactic:
·

Goal state after:
case refine_1
σ : Type u_1
A : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
i j : (affineOpenCover 𝒜).openCover.I₀
⊢ (affineOpenCover 𝒜).f i ≫ toSpecZero 𝒜 = Spec.map (CommRingCat.ofHom (algebraMap (↥(𝒜 0)) (Away 𝒜 ↑i.snd)))
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper

Goal state before:
pp: case refine_2
σ : Type u_1
A : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
i j : (affineOpenCover 𝒜).openCover.I₀
⊢ (affineOpenCover 𝒜).f j ≫ toSpecZero 𝒜 = Spec.map (CommRingCat.ofHom (algebraMap (↥(𝒜 0)) (Away 𝒜 ↑j.snd)))

Tactic:
·

Goal state after:
case refine_2
σ : Type u_1
A : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
i j : (affineOpenCover 𝒜).openCover.I₀
⊢ (affineOpenCover 𝒜).f j ≫ toSpecZero 𝒜 = Spec.map (CommRingCat.ofHom (algebraMap (↥(𝒜 0)) (Away 𝒜 ↑j.snd)))
Module: Mathlib.AlgebraicGeometry.Sites.Small

Goal state before:
pp: case mp
P : MorphismProperty Scheme
S : Scheme
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
inst✝ : P.RespectsIso
X : Over S
R : Sieve X
⊢ R ∈ (overPretopology P S).toGrothendieck X → ∃ 𝒰 x, 𝒰.toPresieveOver ≤ R.arrows

pp: case mpr
P : MorphismProperty Scheme
S : Scheme
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
inst✝ : P.RespectsIso
X : Over S
R : Sieve X
⊢ (∃ 𝒰 x, 𝒰.toPresieveOver ≤ R.arrows) → R ∈ (overPretopology P S).toGrothendieck X

Tactic:
·

Goal state after:
case mp
P : MorphismProperty Scheme
S : Scheme
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
inst✝ : P.RespectsIso
X : Over S
R : Sieve X
⊢ R ∈ (overPretopology P S).toGrothendieck X → ∃ 𝒰 x, 𝒰.toPresieveOver ≤ R.arrows
Module: Mathlib.AlgebraicGeometry.Sites.Small

Goal state before:
pp: case mpr
P : MorphismProperty Scheme
S : Scheme
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
inst✝ : P.RespectsIso
X : Over S
R : Sieve X
⊢ (∃ 𝒰 x, 𝒰.toPresieveOver ≤ R.arrows) → R ∈ (overPretopology P S).toGrothendieck X

Tactic:
·

Goal state after:
case mpr
P : MorphismProperty Scheme
S : Scheme
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
inst✝ : P.RespectsIso
X : Over S
R : Sieve X
⊢ (∃ 𝒰 x, 𝒰.toPresieveOver ≤ R.arrows) → R ∈ (overPretopology P S).toGrothendieck X
Module: Mathlib.AlgebraicGeometry.ValuativeCriterion

Goal state before:
pp: case refine_1
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiSeparated f
hf : ValuativeCriterion.Uniqueness f
S : ValuativeCommSq (pullback.diagonal f)
hc : CommSq S.i₁ (Spec.map (CommRingCat.ofHom (algebraMap S.R S.K))) f (S.i₂ ≫ pullback.fst f f ≫ f)
S' : ValuativeCommSq f :=
  { R := S.R, commRing := S.commRing, domain := ⋯, valuationRing := ⋯, K := S.K, field := S.field, algebra := S.algebra,
    isFractionRing := ⋯, i₁ := S.i₁, i₂ := S.i₂ ≫ pullback.fst f f ≫ f, commSq := hc }
this : Subsingleton ⋯.LiftStruct
S'l₁ : ⋯.LiftStruct := { l := S.i₂ ≫ pullback.fst f f, fac_left := ⋯, fac_right := ⋯ }
S'l₂ : ⋯.LiftStruct := { l := S.i₂ ≫ pullback.snd f f, fac_left := ⋯, fac_right := ⋯ }
h₁₂ : S'l₁ = S'l₂
⊢ Spec.map (CommRingCat.ofHom (algebraMap S.R S.K)) ≫ S.i₂ ≫ pullback.fst f f = S.i₁

pp: case refine_2
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiSeparated f
hf : ValuativeCriterion.Uniqueness f
S : ValuativeCommSq (pullback.diagonal f)
hc : CommSq S.i₁ (Spec.map (CommRingCat.ofHom (algebraMap S.R S.K))) f (S.i₂ ≫ pullback.fst f f ≫ f)
S' : ValuativeCommSq f :=
  { R := S.R, commRing := S.commRing, domain := ⋯, valuationRing := ⋯, K := S.K, field := S.field, algebra := S.algebra,
    isFractionRing := ⋯, i₁ := S.i₁, i₂ := S.i₂ ≫ pullback.fst f f ≫ f, commSq := hc }
this : Subsingleton ⋯.LiftStruct
S'l₁ : ⋯.LiftStruct := { l := S.i₂ ≫ pullback.fst f f, fac_left := ⋯, fac_right := ⋯ }
S'l₂ : ⋯.LiftStruct := { l := S.i₂ ≫ pullback.snd f f, fac_left := ⋯, fac_right := ⋯ }
h₁₂ : S'l₁ = S'l₂
⊢ (S.i₂ ≫ pullback.fst f f) ≫ pullback.diagonal f = S.i₂

Tactic:
·

Goal state after:
case refine_1
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiSeparated f
hf : ValuativeCriterion.Uniqueness f
S : ValuativeCommSq (pullback.diagonal f)
hc : CommSq S.i₁ (Spec.map (CommRingCat.ofHom (algebraMap S.R S.K))) f (S.i₂ ≫ pullback.fst f f ≫ f)
S' : ValuativeCommSq f :=
  { R := S.R, commRing := S.commRing, domain := ⋯, valuationRing := ⋯, K := S.K, field := S.field, algebra := S.algebra,
    isFractionRing := ⋯, i₁ := S.i₁, i₂ := S.i₂ ≫ pullback.fst f f ≫ f, commSq := hc }
this : Subsingleton ⋯.LiftStruct
S'l₁ : ⋯.LiftStruct := { l := S.i₂ ≫ pullback.fst f f, fac_left := ⋯, fac_right := ⋯ }
S'l₂ : ⋯.LiftStruct := { l := S.i₂ ≫ pullback.snd f f, fac_left := ⋯, fac_right := ⋯ }
h₁₂ : S'l₁ = S'l₂
⊢ Spec.map (CommRingCat.ofHom (algebraMap S.R S.K)) ≫ S.i₂ ≫ pullback.fst f f = S.i₁
Module: Mathlib.AlgebraicGeometry.ValuativeCriterion

Goal state before:
pp: case refine_1
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiSeparated f
hf : ValuativeCriterion.Uniqueness f
S : ValuativeCommSq (pullback.diagonal f)
hc : CommSq S.i₁ (Spec.map (CommRingCat.ofHom (algebraMap S.R S.K))) f (S.i₂ ≫ pullback.fst f f ≫ f)
S' : ValuativeCommSq f :=
  { R := S.R, commRing := S.commRing, domain := ⋯, valuationRing := ⋯, K := S.K, field := S.field, algebra := S.algebra,
    isFractionRing := ⋯, i₁ := S.i₁, i₂ := S.i₂ ≫ pullback.fst f f ≫ f, commSq := hc }
this : Subsingleton ⋯.LiftStruct
S'l₁ : ⋯.LiftStruct := { l := S.i₂ ≫ pullback.fst f f, fac_left := ⋯, fac_right := ⋯ }
S'l₂ : ⋯.LiftStruct := { l := S.i₂ ≫ pullback.snd f f, fac_left := ⋯, fac_right := ⋯ }
h₁₂ : S'l₁ = S'l₂
⊢ Spec.map (CommRingCat.ofHom (algebraMap S.R S.K)) ≫ S.i₂ ≫ pullback.fst f f = S.i₁

pp: case refine_2
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiSeparated f
hf : ValuativeCriterion.Uniqueness f
S : ValuativeCommSq (pullback.diagonal f)
hc : CommSq S.i₁ (Spec.map (CommRingCat.ofHom (algebraMap S.R S.K))) f (S.i₂ ≫ pullback.fst f f ≫ f)
S' : ValuativeCommSq f :=
  { R := S.R, commRing := S.commRing, domain := ⋯, valuationRing := ⋯, K := S.K, field := S.field, algebra := S.algebra,
    isFractionRing := ⋯, i₁ := S.i₁, i₂ := S.i₂ ≫ pullback.fst f f ≫ f, commSq := hc }
this : Subsingleton ⋯.LiftStruct
S'l₁ : ⋯.LiftStruct := { l := S.i₂ ≫ pullback.fst f f, fac_left := ⋯, fac_right := ⋯ }
S'l₂ : ⋯.LiftStruct := { l := S.i₂ ≫ pullback.snd f f, fac_left := ⋯, fac_right := ⋯ }
h₁₂ : S'l₁ = S'l₂
⊢ (S.i₂ ≫ pullback.fst f f) ≫ pullback.diagonal f = S.i₂

Tactic:
· simp [← S.commSq.w_assoc]

Goal state after:
case refine_2
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiSeparated f
hf : ValuativeCriterion.Uniqueness f
S : ValuativeCommSq (pullback.diagonal f)
hc : CommSq S.i₁ (Spec.map (CommRingCat.ofHom (algebraMap S.R S.K))) f (S.i₂ ≫ pullback.fst f f ≫ f)
S' : ValuativeCommSq f :=
  { R := S.R, commRing := S.commRing, domain := ⋯, valuationRing := ⋯, K := S.K, field := S.field, algebra := S.algebra,
    isFractionRing := ⋯, i₁ := S.i₁, i₂ := S.i₂ ≫ pullback.fst f f ≫ f, commSq := hc }
this : Subsingleton ⋯.LiftStruct
S'l₁ : ⋯.LiftStruct := { l := S.i₂ ≫ pullback.fst f f, fac_left := ⋯, fac_right := ⋯ }
S'l₂ : ⋯.LiftStruct := { l := S.i₂ ≫ pullback.snd f f, fac_left := ⋯, fac_right := ⋯ }
h₁₂ : S'l₁ = S'l₂
⊢ (S.i₂ ≫ pullback.fst f f) ≫ pullback.diagonal f = S.i₂
Module: Mathlib.AlgebraicGeometry.ValuativeCriterion

Goal state before:
pp: case refine_2
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiSeparated f
hf : ValuativeCriterion.Uniqueness f
S : ValuativeCommSq (pullback.diagonal f)
hc : CommSq S.i₁ (Spec.map (CommRingCat.ofHom (algebraMap S.R S.K))) f (S.i₂ ≫ pullback.fst f f ≫ f)
S' : ValuativeCommSq f :=
  { R := S.R, commRing := S.commRing, domain := ⋯, valuationRing := ⋯, K := S.K, field := S.field, algebra := S.algebra,
    isFractionRing := ⋯, i₁ := S.i₁, i₂ := S.i₂ ≫ pullback.fst f f ≫ f, commSq := hc }
this : Subsingleton ⋯.LiftStruct
S'l₁ : ⋯.LiftStruct := { l := S.i₂ ≫ pullback.fst f f, fac_left := ⋯, fac_right := ⋯ }
S'l₂ : ⋯.LiftStruct := { l := S.i₂ ≫ pullback.snd f f, fac_left := ⋯, fac_right := ⋯ }
h₁₂ : S'l₁ = S'l₂
⊢ (S.i₂ ≫ pullback.fst f f) ≫ pullback.diagonal f = S.i₂

Tactic:
·

Goal state after:
case refine_2
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiSeparated f
hf : ValuativeCriterion.Uniqueness f
S : ValuativeCommSq (pullback.diagonal f)
hc : CommSq S.i₁ (Spec.map (CommRingCat.ofHom (algebraMap S.R S.K))) f (S.i₂ ≫ pullback.fst f f ≫ f)
S' : ValuativeCommSq f :=
  { R := S.R, commRing := S.commRing, domain := ⋯, valuationRing := ⋯, K := S.K, field := S.field, algebra := S.algebra,
    isFractionRing := ⋯, i₁ := S.i₁, i₂ := S.i₂ ≫ pullback.fst f f ≫ f, commSq := hc }
this : Subsingleton ⋯.LiftStruct
S'l₁ : ⋯.LiftStruct := { l := S.i₂ ≫ pullback.fst f f, fac_left := ⋯, fac_right := ⋯ }
S'l₂ : ⋯.LiftStruct := { l := S.i₂ ≫ pullback.snd f f, fac_left := ⋯, fac_right := ⋯ }
h₁₂ : S'l₁ = S'l₂
⊢ (S.i₂ ≫ pullback.fst f f) ≫ pullback.diagonal f = S.i₂
Module: Mathlib.AlgebraicGeometry.ValuativeCriterion

Goal state before:
pp: case refine_2.h₀
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiSeparated f
hf : ValuativeCriterion.Uniqueness f
S : ValuativeCommSq (pullback.diagonal f)
hc : CommSq S.i₁ (Spec.map (CommRingCat.ofHom (algebraMap S.R S.K))) f (S.i₂ ≫ pullback.fst f f ≫ f)
S' : ValuativeCommSq f := ⋯
this : Subsingleton ⋯.LiftStruct
S'l₁ : ⋯.LiftStruct := ⋯
S'l₂ : ⋯.LiftStruct := ⋯
h₁₂ : S'l₁ = S'l₂
⊢ (S.i₂ ≫ pullback.fst f f ≫ pullback.diagonal f) ≫ pullback.fst f f = S.i₂ ≫ pullback.fst f f

pp: case refine_2.h₁
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiSeparated f
hf : ValuativeCriterion.Uniqueness f
S : ValuativeCommSq (pullback.diagonal f)
hc : CommSq S.i₁ (Spec.map (CommRingCat.ofHom (algebraMap S.R S.K))) f (S.i₂ ≫ pullback.fst f f ≫ f)
S' : ValuativeCommSq f := ⋯
this : Subsingleton ⋯.LiftStruct
S'l₁ : ⋯.LiftStruct := ⋯
S'l₂ : ⋯.LiftStruct := ⋯
h₁₂ : S'l₁ = S'l₂
⊢ (S.i₂ ≫ pullback.fst f f ≫ pullback.diagonal f) ≫ pullback.snd f f = S.i₂ ≫ pullback.snd f f

Tactic:
·

Goal state after:
case refine_2.h₀
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiSeparated f
hf : ValuativeCriterion.Uniqueness f
S : ValuativeCommSq (pullback.diagonal f)
hc : CommSq S.i₁ (Spec.map (CommRingCat.ofHom (algebraMap S.R S.K))) f (S.i₂ ≫ pullback.fst f f ≫ f)
S' : ValuativeCommSq f := ⋯
this : Subsingleton ⋯.LiftStruct
S'l₁ : ⋯.LiftStruct := ⋯
S'l₂ : ⋯.LiftStruct := ⋯
h₁₂ : S'l₁ = S'l₂
⊢ (S.i₂ ≫ pullback.fst f f ≫ pullback.diagonal f) ≫ pullback.fst f f = S.i₂ ≫ pullback.fst f f
Module: Mathlib.AlgebraicGeometry.ValuativeCriterion

Goal state before:
pp: case refine_2.h₁
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiSeparated f
hf : ValuativeCriterion.Uniqueness f
S : ValuativeCommSq (pullback.diagonal f)
hc : CommSq S.i₁ (Spec.map (CommRingCat.ofHom (algebraMap S.R S.K))) f (S.i₂ ≫ pullback.fst f f ≫ f)
S' : ValuativeCommSq f := ⋯
this : Subsingleton ⋯.LiftStruct
S'l₁ : ⋯.LiftStruct := ⋯
S'l₂ : ⋯.LiftStruct := ⋯
h₁₂ : S'l₁ = S'l₂
⊢ (S.i₂ ≫ pullback.fst f f ≫ pullback.diagonal f) ≫ pullback.snd f f = S.i₂ ≫ pullback.snd f f

Tactic:
·

Goal state after:
case refine_2.h₁
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiSeparated f
hf : ValuativeCriterion.Uniqueness f
S : ValuativeCommSq (pullback.diagonal f)
hc : CommSq S.i₁ (Spec.map (CommRingCat.ofHom (algebraMap S.R S.K))) f (S.i₂ ≫ pullback.fst f f ≫ f)
S' : ValuativeCommSq f := ⋯
this : Subsingleton ⋯.LiftStruct
S'l₁ : ⋯.LiftStruct := ⋯
S'l₂ : ⋯.LiftStruct := ⋯
h₁₂ : S'l₁ = S'l₂
⊢ (S.i₂ ≫ pullback.fst f f ≫ pullback.diagonal f) ≫ pullback.snd f f = S.i₂ ≫ pullback.snd f f
Module: Mathlib.AlgebraicGeometry.Sites.Small

Goal state before:
pp: P Q : MorphismProperty Scheme
S : Scheme
inst✝³ : P.IsStableUnderBaseChange
inst✝² : P.IsMultiplicative
inst✝¹ : P.RespectsIso
inst✝ : Q.IsStableUnderComposition
hPQ : P ≤ Q
X : Q.Over ⊤ S
⊢ ∀ (T : ↑((overGrothendieckTopology P S) ((MorphismProperty.Over.forget Q ⊤ S).obj X))),
    Sieve.functorPushforward (MorphismProperty.Over.forget Q ⊤ S)
        (Sieve.functorPullback (MorphismProperty.Over.forget Q ⊤ S) ↑T) ∈
      (overGrothendieckTopology P S) ((MorphismProperty.Over.forget Q ⊤ S).obj X)

Tactic:
by
    intro ⟨T, hT⟩
    rw [mem_overGrothendieckTopology] at hT ⊢
    obtain ⟨𝒰, h, hle⟩ := hT
    use 𝒰, h
    rintro - - ⟨i⟩
    have p : Q (𝒰.X i ↘ S) := by
      rw [← comp_over (𝒰.f i) S]
      exact Q.comp_mem _ _ (hPQ _ <| 𝒰.map_prop i) X.prop
    use (𝒰.X i).asOverProp S p, MorphismProperty.Over.homMk (𝒰.f i) (comp_over (𝒰.f i) S), 𝟙 _
    exact ⟨hle _ _ ⟨i⟩, rfl⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.ValuativeCriterion

Goal state before:
pp: case refine_2.h₁
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiSeparated f
hf : ValuativeCriterion.Uniqueness f
S : ValuativeCommSq (pullback.diagonal f)
hc : CommSq S.i₁ (Spec.map (CommRingCat.ofHom (algebraMap S.R S.K))) f (S.i₂ ≫ pullback.fst f f ≫ f)
S' : ValuativeCommSq f := ⋯
this : Subsingleton ⋯.LiftStruct
S'l₁ : ⋯.LiftStruct := ⋯
S'l₂ : ⋯.LiftStruct := ⋯
h₁₂ : S'l₁ = S'l₂
⊢ (S.i₂ ≫ pullback.fst f f ≫ pullback.diagonal f) ≫ pullback.snd f f = S.i₂ ≫ pullback.snd f f

Tactic:
· simp only [Category.assoc, pullback.diagonal_snd, Category.comp_id]
        exact congrArg CommSq.LiftStruct.l h₁₂

Goal state after:
Module: Mathlib.AlgebraicGeometry.Sites.Small

Goal state before:
pp: case refine_1
P Q : MorphismProperty Scheme
S : Scheme
inst✝⁵ : P.IsStableUnderBaseChange
inst✝⁴ : P.IsMultiplicative
inst✝³ : P.RespectsIso
inst✝² : Q.IsStableUnderComposition
inst✝¹ : Q.IsStableUnderBaseChange
inst✝ : Q.HasOfPostcompProperty Q
Y X : Q.Over ⊤ S
f : X ⟶ Y
𝒰 : Cover (precoverage P) Y.left
h : Cover.Over S 𝒰
p : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)
⊢ ∀ (j : (Cover.pullbackCoverOverProp' S 𝒰 f.left ⋯ ⋯ p).I₀),
    Q ((Cover.pullbackCoverOverProp' S 𝒰 f.left ⋯ ⋯ p).X j ↘ S)

pp: case refine_2
P Q : MorphismProperty Scheme
S : Scheme
inst✝⁵ : P.IsStableUnderBaseChange
inst✝⁴ : P.IsMultiplicative
inst✝³ : P.RespectsIso
inst✝² : Q.IsStableUnderComposition
inst✝¹ : Q.IsStableUnderBaseChange
inst✝ : Q.HasOfPostcompProperty Q
Y X : Q.Over ⊤ S
f : X ⟶ Y
𝒰 : Cover (precoverage P) Y.left
h : Cover.Over S 𝒰
p : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)
⊢ Presieve.pullbackArrows f (𝒰.toPresieveOverProp p) =
    (Cover.pullbackCoverOverProp' S 𝒰 f.left ⋯ ⋯ p).toPresieveOverProp ?refine_1

Tactic:
·

Goal state after:
case refine_1
P Q : MorphismProperty Scheme
S : Scheme
inst✝⁵ : P.IsStableUnderBaseChange
inst✝⁴ : P.IsMultiplicative
inst✝³ : P.RespectsIso
inst✝² : Q.IsStableUnderComposition
inst✝¹ : Q.IsStableUnderBaseChange
inst✝ : Q.HasOfPostcompProperty Q
Y X : Q.Over ⊤ S
f : X ⟶ Y
𝒰 : Cover (precoverage P) Y.left
h : Cover.Over S 𝒰
p : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)
⊢ ∀ (j : (Cover.pullbackCoverOverProp' S 𝒰 f.left ⋯ ⋯ p).I₀),
    Q ((Cover.pullbackCoverOverProp' S 𝒰 f.left ⋯ ⋯ p).X j ↘ S)
Module: Mathlib.AlgebraicGeometry.Sites.Small

Goal state before:
pp: case refine_2
P Q : MorphismProperty Scheme
S : Scheme
inst✝⁵ : P.IsStableUnderBaseChange
inst✝⁴ : P.IsMultiplicative
inst✝³ : P.RespectsIso
inst✝² : Q.IsStableUnderComposition
inst✝¹ : Q.IsStableUnderBaseChange
inst✝ : Q.HasOfPostcompProperty Q
Y X : Q.Over ⊤ S
f : X ⟶ Y
𝒰 : Cover (precoverage P) Y.left
h : Cover.Over S 𝒰
p : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)
⊢ Presieve.pullbackArrows f (𝒰.toPresieveOverProp p) =
    (Cover.pullbackCoverOverProp' S 𝒰 f.left ⋯ ⋯ p).toPresieveOverProp ⋯

Tactic:
·

Goal state after:
case refine_2
P Q : MorphismProperty Scheme
S : Scheme
inst✝⁵ : P.IsStableUnderBaseChange
inst✝⁴ : P.IsMultiplicative
inst✝³ : P.RespectsIso
inst✝² : Q.IsStableUnderComposition
inst✝¹ : Q.IsStableUnderBaseChange
inst✝ : Q.HasOfPostcompProperty Q
Y X : Q.Over ⊤ S
f : X ⟶ Y
𝒰 : Cover (precoverage P) Y.left
h : Cover.Over S 𝒰
p : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)
⊢ Presieve.pullbackArrows f (𝒰.toPresieveOverProp p) =
    (Cover.pullbackCoverOverProp' S 𝒰 f.left ⋯ ⋯ p).toPresieveOverProp ⋯
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: case refine_1.refine_1
R : CommRingCat
M : (Spec R).Modules
V : (Spec R).Opens
ι : Type u_1
inst✝ : Finite ι
g : ι → ↑R
hg : V = ⨆ i, basicOpen (g i)
h₁ : ∀ (i : ι), Aux M (basicOpen (g i))
h₂ : ∀ (i j : ι), Aux M (basicOpen (g i * g j))
hgle : ∀ (i : ι), basicOpen (g i) ≤ V
hug : ∀ (i : ι) (m : ℕ), IsUnit ((algebraMap (↑R) (Module.End ↑R ↑Γ(M, basicOpen (g i)))) (g i ^ m))
f : ↑R
hf : basicOpen f ≤ V
s : ↑Γ(M, basicOpen f)
hfgi : ∀ (i : ι), basicOpen (f * g i) ≤ basicOpen (g i)
s' : (i : ι) → ↑Γ(M, basicOpen (f * g i)) := fun i ↦ (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) s
N : ℕ
t : (i : ι) → ↑Γ(M, basicOpen (g i))
ht : ∀ (i : ι), f ^ N • s' i = (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (t i)
K : ℕ
hK :
  ∀ (i j : ι),
    (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (f ^ K • t i) =
      (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (f ^ K • t j)
⊢ Presheaf.IsCompatible { obj := M.presheaf, property := ⋯ }.obj (fun i ↦ basicOpen (g i)) fun i ↦ f ^ K • t i

Tactic:
·

Goal state after:
case refine_1.refine_1
R : CommRingCat
M : (Spec R).Modules
V : (Spec R).Opens
ι : Type u_1
inst✝ : Finite ι
g : ι → ↑R
hg : V = ⨆ i, basicOpen (g i)
h₁ : ∀ (i : ι), Aux M (basicOpen (g i))
h₂ : ∀ (i j : ι), Aux M (basicOpen (g i * g j))
hgle : ∀ (i : ι), basicOpen (g i) ≤ V
hug : ∀ (i : ι) (m : ℕ), IsUnit ((algebraMap (↑R) (Module.End ↑R ↑Γ(M, basicOpen (g i)))) (g i ^ m))
f : ↑R
hf : basicOpen f ≤ V
s : ↑Γ(M, basicOpen f)
hfgi : ∀ (i : ι), basicOpen (f * g i) ≤ basicOpen (g i)
s' : (i : ι) → ↑Γ(M, basicOpen (f * g i)) := fun i ↦ (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) s
N : ℕ
t : (i : ι) → ↑Γ(M, basicOpen (g i))
ht : ∀ (i : ι), f ^ N • s' i = (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (t i)
K : ℕ
hK :
  ∀ (i j : ι),
    (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (f ^ K • t i) =
      (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (f ^ K • t j)
⊢ Presheaf.IsCompatible { obj := M.presheaf, property := ⋯ }.obj (fun i ↦ basicOpen (g i)) fun i ↦ f ^ K • t i