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

Goal state before:
pp: case left
X Y : Scheme
f : X ⟶ Y
inst✝ : IsSeparated f
S : ValuativeCommSq f
l₁ : Spec (CommRingCat.of S.R) ⟶ X
hl₁ : Spec.map (CommRingCat.ofHom (algebraMap S.R S.K)) ≫ l₁ = S.i₁
hl₁' : l₁ ≫ f = S.i₂
l₂ : Spec (CommRingCat.of S.R) ⟶ X
hl₂ : Spec.map (CommRingCat.ofHom (algebraMap S.R S.K)) ≫ l₂ = S.i₁
hl₂' : l₂ ≫ f = S.i₂
h : l₁ ≫ f = l₂ ≫ f
Z : Scheme := pullback (pullback.diagonal f) (pullback.lift l₁ l₂ h)
g : Z ⟶ Spec (CommRingCat.of S.R) := pullback.snd (pullback.diagonal f) (pullback.lift l₁ l₂ h)
this✝ : IsClosedImmersion g
hZ : IsAffine Z
l : Spec (CommRingCat.of S.K) ⟶ Z := pullback.lift S.i₁ (Spec.map (CommRingCat.ofHom (algebraMap S.R S.K))) ⋯
hg : l ≫ g = Spec.map (CommRingCat.ofHom (algebraMap S.R S.K))
this : Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop g ≫ Scheme.Hom.appTop l))
⊢ Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop g))

Tactic:
]

Goal state after:
case left
X Y : Scheme
f : X ⟶ Y
inst✝ : IsSeparated f
S : ValuativeCommSq f
l₁ : Spec (CommRingCat.of S.R) ⟶ X
hl₁ : Spec.map (CommRingCat.ofHom (algebraMap S.R S.K)) ≫ l₁ = S.i₁
hl₁' : l₁ ≫ f = S.i₂
l₂ : Spec (CommRingCat.of S.R) ⟶ X
hl₂ : Spec.map (CommRingCat.ofHom (algebraMap S.R S.K)) ≫ l₂ = S.i₁
hl₂' : l₂ ≫ f = S.i₂
h : l₁ ≫ f = l₂ ≫ f
Z : Scheme := pullback (pullback.diagonal f) (pullback.lift l₁ l₂ h)
g : Z ⟶ Spec (CommRingCat.of S.R) := pullback.snd (pullback.diagonal f) (pullback.lift l₁ l₂ h)
this✝ : IsClosedImmersion g
hZ : IsAffine Z
l : Spec (CommRingCat.of S.K) ⟶ Z := pullback.lift S.i₁ (Spec.map (CommRingCat.ofHom (algebraMap S.R S.K))) ⋯
hg : l ≫ g = Spec.map (CommRingCat.ofHom (algebraMap S.R S.K))
this : Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop g ≫ Scheme.Hom.appTop l))
⊢ Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop g))
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper

Goal state before:
pp: σ : Type u_1
A : Type u_2
inst✝⁴ : CommRing A
inst✝³ : SetLike σ A
inst✝² : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝¹ : GradedRing 𝒜
inst✝ : Algebra.FiniteType (↥(𝒜 0)) A
x : Finset A
hx : Algebra.adjoin ↥(𝒜 0) ↑x = ⊤
d : (i : A) → i ∈ x → ℕ
hd : ∀ (i : A) (a : i ∈ x), d i a ≠ 0
hxd : ∀ (i : A) (a : i ∈ x), i ∈ 𝒜 (d i a)
H : ∀ (i : ↥x), IsCompact (basicOpen 𝒜 ↑i).carrier
this : ⋃ i, ↑(basicOpen 𝒜 ↑i) = Set.univ
⊢ IsCompact (⋃ i, ↑(basicOpen 𝒜 ↑i))

Tactic:
]

Goal state after:
σ : Type u_1
A : Type u_2
inst✝⁴ : CommRing A
inst✝³ : SetLike σ A
inst✝² : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝¹ : GradedRing 𝒜
inst✝ : Algebra.FiniteType (↥(𝒜 0)) A
x : Finset A
hx : Algebra.adjoin ↥(𝒜 0) ↑x = ⊤
d : (i : A) → i ∈ x → ℕ
hd : ∀ (i : A) (a : i ∈ x), d i a ≠ 0
hxd : ∀ (i : A) (a : i ∈ x), i ∈ 𝒜 (d i a)
H : ∀ (i : ↥x), IsCompact (basicOpen 𝒜 ↑i).carrier
this : ⋃ i, ↑(basicOpen 𝒜 ↑i) = Set.univ
⊢ IsCompact (⋃ i, ↑(basicOpen 𝒜 ↑i))
Module: Mathlib.AlgebraicGeometry.ValuativeCriterion

Goal state before:
pp: case right
X Y : Scheme
f : X ⟶ Y
inst✝ : IsSeparated f
S : ValuativeCommSq f
l₁ : Spec (CommRingCat.of S.R) ⟶ X
hl₁ : Spec.map (CommRingCat.ofHom (algebraMap S.R S.K)) ≫ l₁ = S.i₁
hl₁' : l₁ ≫ f = S.i₂
l₂ : Spec (CommRingCat.of S.R) ⟶ X
hl₂ : Spec.map (CommRingCat.ofHom (algebraMap S.R S.K)) ≫ l₂ = S.i₁
hl₂' : l₂ ≫ f = S.i₂
h : l₁ ≫ f = l₂ ≫ f
Z : Scheme := pullback (pullback.diagonal f) (pullback.lift l₁ l₂ h)
g : Z ⟶ Spec (CommRingCat.of S.R) := pullback.snd (pullback.diagonal f) (pullback.lift l₁ l₂ h)
this : IsAffine Z ∧ Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop g))
hZ : IsAffine Z
⊢ Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop g))

Tactic:
]

Goal state after:
case right
X Y : Scheme
f : X ⟶ Y
inst✝ : IsSeparated f
S : ValuativeCommSq f
l₁ : Spec (CommRingCat.of S.R) ⟶ X
hl₁ : Spec.map (CommRingCat.ofHom (algebraMap S.R S.K)) ≫ l₁ = S.i₁
hl₁' : l₁ ≫ f = S.i₂
l₂ : Spec (CommRingCat.of S.R) ⟶ X
hl₂ : Spec.map (CommRingCat.ofHom (algebraMap S.R S.K)) ≫ l₂ = S.i₁
hl₂' : l₂ ≫ f = S.i₂
h : l₁ ≫ f = l₂ ≫ f
Z : Scheme := pullback (pullback.diagonal f) (pullback.lift l₁ l₂ h)
g : Z ⟶ Spec (CommRingCat.of S.R) := pullback.snd (pullback.diagonal f) (pullback.lift l₁ l₂ h)
this : IsAffine Z ∧ Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop g))
hZ : IsAffine Z
⊢ Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop g))
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: case 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
t : ↑Γ(M, V)
hs : (ConcreteCategory.hom (M.presheaf.map (homOfLE hf).op)) t = 0
i : ι
⊢ (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) ((ConcreteCategory.hom (M.presheaf.map (homOfLE hf).op)) t) = 0

Tactic:
]

Goal state after:
case 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
t : ↑Γ(M, V)
hs : (ConcreteCategory.hom (M.presheaf.map (homOfLE hf).op)) t = 0
i : ι
⊢ (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) ((ConcreteCategory.hom (M.presheaf.map (homOfLE hf).op)) t) = 0
Module: Mathlib.AlgebraicGeometry.Sites.Small

Goal state before:
pp: P : MorphismProperty Scheme
S : Scheme
inst✝³ : P.IsStableUnderBaseChange
inst✝² : P.IsMultiplicative
inst✝¹ : P.RespectsIso
inst✝ : P.HasOfPostcompProperty P
X : P.Over ⊤ S
R : Sieve X
⊢ R ∈ (smallPretopology P P).toGrothendieck X ↔
    ∃ 𝒰 x, ∃ (h : ∀ (j : 𝒰.I₀), P (𝒰.X j ↘ S)), 𝒰.toPresieveOverProp h ≤ R.arrows

Tactic:
]

Goal state after:
P : MorphismProperty Scheme
S : Scheme
inst✝³ : P.IsStableUnderBaseChange
inst✝² : P.IsMultiplicative
inst✝¹ : P.RespectsIso
inst✝ : P.HasOfPostcompProperty P
X : P.Over ⊤ S
R : Sieve X
⊢ R ∈ (smallPretopology P P).toGrothendieck X ↔
    ∃ 𝒰 x, ∃ (h : ∀ (j : 𝒰.I₀), P (𝒰.X j ↘ S)), 𝒰.toPresieveOverProp h ≤ R.arrows
Module: Mathlib.AlgebraicGeometry.ValuativeCriterion

Goal state before:
pp: ⊢ ValuativeCriterion.Uniqueness ⊓ @QuasiSeparated ⊓ (ValuativeCriterion.Existence ⊓ @QuasiCompact) ⊓
      @LocallyOfFiniteType =
    ValuativeCriterion.Existence ⊓ ValuativeCriterion.Uniqueness ⊓ @QuasiCompact ⊓ @QuasiSeparated ⊓
      @LocallyOfFiniteType

Tactic:
]

Goal state after:
⊢ ValuativeCriterion.Uniqueness ⊓ @QuasiSeparated ⊓ (ValuativeCriterion.Existence ⊓ @QuasiCompact) ⊓
      @LocallyOfFiniteType =
    ValuativeCriterion.Existence ⊓ ValuativeCriterion.Uniqueness ⊓ @QuasiCompact ⊓ @QuasiSeparated ⊓
      @LocallyOfFiniteType
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: 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
t : ↑Γ(M, V)
hs : (ConcreteCategory.hom (M.presheaf.map (homOfLE hf).op)) t = 0
n : ι → ℕ
hn : ∀ (i : ι), (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (f ^ n i • t) = 0
i : ι
⊢ basicOpen (g i) ≤ ⨆ i, basicOpen (g i)

Tactic:
]

Goal state after:
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
t : ↑Γ(M, V)
hs : (ConcreteCategory.hom (M.presheaf.map (homOfLE hf).op)) t = 0
n : ι → ℕ
hn : ∀ (i : ι), (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (f ^ n i • t) = 0
i : ι
⊢ basicOpen (g i) ≤ ⨆ i, basicOpen (g i)
Module: Mathlib.AlgebraicGeometry.ValuativeCriterion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝² : QuasiCompact f
inst✝¹ : QuasiSeparated f
inst✝ : LocallyOfFiniteType f
H : ValuativeCriterion f
⊢ (ValuativeCriterion ⊓ @QuasiCompact ⊓ @QuasiSeparated ⊓ @LocallyOfFiniteType) f

Tactic:
]

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝² : QuasiCompact f
inst✝¹ : QuasiSeparated f
inst✝ : LocallyOfFiniteType f
H : ValuativeCriterion f
⊢ (ValuativeCriterion ⊓ @QuasiCompact ⊓ @QuasiSeparated ⊓ @LocallyOfFiniteType) f
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense

Goal state before:
pp: C₀ : Type u₀
C : Type u
inst✝⁵ : Category.{v₀, u₀} C₀
inst✝⁴ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
inst✝³ : IsDenseSubsite J₀ J F
inst✝² : HasPullbacks C
inst✝¹ : F.Full
inst✝ : F.Faithful
S : C
ι : C → Type w
U : (S : C) → ι S → C₀
f : (S : C) → (i : ι S) → F.obj (U S i) ⟶ S
hf : ∀ (S : C), Sieve.ofArrows (fun i ↦ F.obj (U S i)) (f S) ∈ J S
i j : ι S
W₀ : C₀
p₁ : W₀ ⟶ U S i
p₂ : W₀ ⟶ U S j
hp : F.map p₁ ≫ f S i = F.map p₂ ≫ f S j
this : F.IsCoverDense J
⊢ Sieve.functorPushforward F
      ({ I₀ := ι S, X := U S, f := f S, I₁ := fun i j ↦ ι (pullback (f S i) (f S j)),
            Y := fun i j ↦ U (pullback (f S i) (f S j)),
            p₁ := fun i j k ↦ F.preimage (f (pullback (f S i) (f S j)) k ≫ pullback.fst (f S i) (f S j)),
            p₂ := fun i j k ↦ F.preimage (f (pullback (f S i) (f S j)) k ≫ pullback.snd (f S i) (f S j)),
            w := ⋯ }.sieve₁₀
        p₁ p₂) ∈
    J (F.obj W₀)

Tactic:
]

Goal state after:
C₀ : Type u₀
C : Type u
inst✝⁵ : Category.{v₀, u₀} C₀
inst✝⁴ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
inst✝³ : IsDenseSubsite J₀ J F
inst✝² : HasPullbacks C
inst✝¹ : F.Full
inst✝ : F.Faithful
S : C
ι : C → Type w
U : (S : C) → ι S → C₀
f : (S : C) → (i : ι S) → F.obj (U S i) ⟶ S
hf : ∀ (S : C), Sieve.ofArrows (fun i ↦ F.obj (U S i)) (f S) ∈ J S
i j : ι S
W₀ : C₀
p₁ : W₀ ⟶ U S i
p₂ : W₀ ⟶ U S j
hp : F.map p₁ ≫ f S i = F.map p₂ ≫ f S j
this : F.IsCoverDense J
⊢ Sieve.functorPushforward F
      ({ I₀ := ι S, X := U S, f := f S, I₁ := fun i j ↦ ι (pullback (f S i) (f S j)),
            Y := fun i j ↦ U (pullback (f S i) (f S j)),
            p₁ := fun i j k ↦ F.preimage (f (pullback (f S i) (f S j)) k ≫ pullback.fst (f S i) (f S j)),
            p₂ := fun i j k ↦ F.preimage (f (pullback (f S i) (f S j)) k ≫ pullback.snd (f S i) (f S j)),
            w := ⋯ }.sieve₁₀
        p₁ p₂) ∈
    J (F.obj W₀)
Module: Mathlib.AlgebraicGeometry.Sites.Affine

Goal state before:
pp: S : Scheme
P : MorphismProperty Scheme
inst✝³ : P.IsMultiplicative
inst✝² : IsZariskiLocalAtSource P
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : P.HasOfPostcompProperty P
U : P.Over ⊤ S
⊢ ∃ 𝒰 x,
    ∃ (h : ∀ (j : 𝒰.I₀), P (𝒰.X j ↘ S)),
      𝒰.toPresieveOverProp h ≤ (Sieve.coverByImage (MorphismProperty.CostructuredArrow.toOver P Scheme.Spec S) U).arrows

Tactic:
]

Goal state after:
S : Scheme
P : MorphismProperty Scheme
inst✝³ : P.IsMultiplicative
inst✝² : IsZariskiLocalAtSource P
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : P.HasOfPostcompProperty P
U : P.Over ⊤ S
⊢ ∃ 𝒰 x,
    ∃ (h : ∀ (j : 𝒰.I₀), P (𝒰.X j ↘ S)),
      𝒰.toPresieveOverProp h ≤ (Sieve.coverByImage (MorphismProperty.CostructuredArrow.toOver P Scheme.Spec S) U).arrows
Module: Mathlib.AlgebraicGeometry.Sites.Affine

Goal state before:
pp: S : Scheme
P : MorphismProperty Scheme
inst✝³ : P.IsMultiplicative
inst✝² : IsZariskiLocalAtSource P
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : P.HasOfPostcompProperty P
U : P.Over ⊤ S
𝒰 : Cover (precoverage P) U.left := Cover.changeProp U.left.affineCover ⋯
x✝² : (i : 𝒰.I₀) → (𝒰.X i).Over S := fun i ↦ { hom := 𝒰.f i ≫ U.hom }
x✝¹ : Cover.Over S 𝒰 := { over := inferInstance, isOver_map := ⋯ }
X : P.Over ⊤ S
f : X ⟶ U
x✝ : 𝒰.toPresieveOverProp ⋯ f
i : 𝒰.I₀
⊢ { arrows := Presieve.coverByImage (MorphismProperty.CostructuredArrow.toOver P Scheme.Spec S) U,
        downward_closed := ⋯ }.arrows
    (Hom.asOverProp (𝒰.f i) S)

Tactic:
]

Goal state after:
S : Scheme
P : MorphismProperty Scheme
inst✝³ : P.IsMultiplicative
inst✝² : IsZariskiLocalAtSource P
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : P.HasOfPostcompProperty P
U : P.Over ⊤ S
𝒰 : Cover (precoverage P) U.left := Cover.changeProp U.left.affineCover ⋯
x✝² : (i : 𝒰.I₀) → (𝒰.X i).Over S := fun i ↦ { hom := 𝒰.f i ≫ U.hom }
x✝¹ : Cover.Over S 𝒰 := { over := inferInstance, isOver_map := ⋯ }
X : P.Over ⊤ S
f : X ⟶ U
x✝ : 𝒰.toPresieveOverProp ⋯ f
i : 𝒰.I₀
⊢ { arrows := Presieve.coverByImage (MorphismProperty.CostructuredArrow.toOver P Scheme.Spec S) U,
        downward_closed := ⋯ }.arrows
    (Hom.asOverProp (𝒰.f i) S)
Module: Mathlib.AlgebraicGeometry.Sites.Affine

Goal state before:
pp: S : Scheme
P : MorphismProperty Scheme
inst✝³ : P.IsMultiplicative
inst✝² : IsZariskiLocalAtSource P
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : P.HasOfPostcompProperty P
X : P.Over ⊤ S
𝒰 : X.left.AffineOpenCover := X.left.affineOpenCover
𝒱 : Cover (precoverage P) X.left := Cover.changeProp 𝒰.openCover ⋯
x✝ : (i : 𝒱.I₀) → (𝒱.X i).Over S := fun i ↦ { hom := 𝒰.f i ≫ X.hom }
this : Cover.Over S 𝒱 := { over := inferInstance, isOver_map := ⋯ }
⊢ ∃ 𝒰_1 x,
    ∃ (h : ∀ (j : 𝒰_1.I₀), P (𝒰_1.X j ↘ S)),
      𝒰_1.toPresieveOverProp h ≤
        (Sieve.ofArrows
            (fun i ↦
              (MorphismProperty.CostructuredArrow.toOver P Scheme.Spec S).obj
                ((fun i ↦ affineOverMk (𝒰.f i ≫ X.hom) ⋯) i))
            fun i ↦ MorphismProperty.CostructuredArrow.homMk (𝒰.f i) ⋯ ⋯).arrows

Tactic:
]

Goal state after:
S : Scheme
P : MorphismProperty Scheme
inst✝³ : P.IsMultiplicative
inst✝² : IsZariskiLocalAtSource P
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : P.HasOfPostcompProperty P
X : P.Over ⊤ S
𝒰 : X.left.AffineOpenCover := X.left.affineOpenCover
𝒱 : Cover (precoverage P) X.left := Cover.changeProp 𝒰.openCover ⋯
x✝ : (i : 𝒱.I₀) → (𝒱.X i).Over S := fun i ↦ { hom := 𝒰.f i ≫ X.hom }
this : Cover.Over S 𝒱 := { over := inferInstance, isOver_map := ⋯ }
⊢ ∃ 𝒰_1 x,
    ∃ (h : ∀ (j : 𝒰_1.I₀), P (𝒰_1.X j ↘ S)),
      𝒰_1.toPresieveOverProp h ≤
        (Sieve.ofArrows
            (fun i ↦
              (MorphismProperty.CostructuredArrow.toOver P Scheme.Spec S).obj
                ((fun i ↦ affineOverMk (𝒰.f i ≫ X.hom) ⋯) i))
            fun i ↦ MorphismProperty.CostructuredArrow.homMk (𝒰.f i) ⋯ ⋯).arrows
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper

Goal state before:
pp: case right
σ : Type u_1
A : Type u_2
inst✝¹⁰ : CommRing A
inst✝⁹ : SetLike σ A
inst✝⁸ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝⁷ : GradedRing 𝒜
O : Type u_3
inst✝⁶ : CommRing O
inst✝⁵ : IsDomain O
inst✝⁴ : ValuationRing O
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra O K
inst✝¹ : IsFractionRing O K
φ₀ : ↥(𝒜 0) →+* O
ι : Type u_5
inst✝ : Finite ι
x : ι → A
h2 : Algebra.adjoin (↥(𝒜 0)) (Set.range x) = ⊤
j : ι
φ : Away 𝒜 (x j) →+* K
hcomm : (algebraMap O K).comp φ₀ = φ.comp (fromZeroRingHom 𝒜 (Submonoid.powers (x j)))
d : ι → ℕ
hdi : ∀ (i : ι), 0 < d i
hxdi : ∀ (i : ι), x i ∈ 𝒜 (d i)
val✝ : Fintype ι
ψ : ι → ValueGroup O K := fun i ↦ (valuation O K) (φ (Away.isLocalizationElem ⋯ ⋯) ^ ∏ k ∈ Finset.univ.erase i, d k)
this✝¹ : Nonempty ι
Kmax : ValueGroup O K := (Finset.image ψ Finset.univ).max' ⋯
i₀ : ι
hi1 : ψ i₀ = Kmax
hi₀ : ∀ (j : ι), ψ j ≤ ψ i₀
hKmax : 0 < Kmax
this✝ : Algebra (Away 𝒜 (x j)) (Away 𝒜 (x j * x i₀)) := (awayMap 𝒜 ⋯ ⋯).toAlgebra
this : IsLocalization.Away (Away.isLocalizationElem ⋯ ⋯) (Away 𝒜 (x j * x i₀))
hunit : IsUnit (φ (Away.isLocalizationElem ⋯ ⋯))
φ' : Away 𝒜 (x j * x i₀) →+* K := IsLocalization.Away.lift (Away.isLocalizationElem ⋯ ⋯) hunit
hφ'1 : ∀ (s : Away 𝒜 (x j)), φ' ((awayMap 𝒜 ⋯ ⋯) s) = φ s
sx : Away 𝒜 (x i₀)
⊢ (valuation O K) ((φ'.comp (awayMap 𝒜 ⋯ ⋯)) sx) ≤ 1

Tactic:
]

Goal state after:
case right
σ : Type u_1
A : Type u_2
inst✝¹⁰ : CommRing A
inst✝⁹ : SetLike σ A
inst✝⁸ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝⁷ : GradedRing 𝒜
O : Type u_3
inst✝⁶ : CommRing O
inst✝⁵ : IsDomain O
inst✝⁴ : ValuationRing O
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra O K
inst✝¹ : IsFractionRing O K
φ₀ : ↥(𝒜 0) →+* O
ι : Type u_5
inst✝ : Finite ι
x : ι → A
h2 : Algebra.adjoin (↥(𝒜 0)) (Set.range x) = ⊤
j : ι
φ : Away 𝒜 (x j) →+* K
hcomm : (algebraMap O K).comp φ₀ = φ.comp (fromZeroRingHom 𝒜 (Submonoid.powers (x j)))
d : ι → ℕ
hdi : ∀ (i : ι), 0 < d i
hxdi : ∀ (i : ι), x i ∈ 𝒜 (d i)
val✝ : Fintype ι
ψ : ι → ValueGroup O K := fun i ↦ (valuation O K) (φ (Away.isLocalizationElem ⋯ ⋯) ^ ∏ k ∈ Finset.univ.erase i, d k)
this✝¹ : Nonempty ι
Kmax : ValueGroup O K := (Finset.image ψ Finset.univ).max' ⋯
i₀ : ι
hi1 : ψ i₀ = Kmax
hi₀ : ∀ (j : ι), ψ j ≤ ψ i₀
hKmax : 0 < Kmax
this✝ : Algebra (Away 𝒜 (x j)) (Away 𝒜 (x j * x i₀)) := (awayMap 𝒜 ⋯ ⋯).toAlgebra
this : IsLocalization.Away (Away.isLocalizationElem ⋯ ⋯) (Away 𝒜 (x j * x i₀))
hunit : IsUnit (φ (Away.isLocalizationElem ⋯ ⋯))
φ' : Away 𝒜 (x j * x i₀) →+* K := IsLocalization.Away.lift (Away.isLocalizationElem ⋯ ⋯) hunit
hφ'1 : ∀ (s : Away 𝒜 (x j)), φ' ((awayMap 𝒜 ⋯ ⋯) s) = φ s
sx : Away 𝒜 (x i₀)
⊢ (valuation O K) ((φ'.comp (awayMap 𝒜 ⋯ ⋯)) sx) ≤ 1
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: case h.h
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
t : ↑Γ(M, V)
hs : (ConcreteCategory.hom (M.presheaf.map (homOfLE hf).op)) t = 0
n : ι → ℕ
hn : ∀ (i : ι), (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (f ^ n i • t) = 0
i : ι
this✝ : n i ≤ ⨆ i, n i
this : ⨆ i, n i = (⨆ i, n i) - n i + n i
⊢ f ^ ((⨆ i, n i) - n i) • (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (f ^ n i • t) =
    (ConcreteCategory.hom ({ obj := M.presheaf, property := ⋯ }.obj.map (homOfLE ⋯).op)) 0

Tactic:
hn i

Goal state after:
case h.h
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
t : ↑Γ(M, V)
hs : (ConcreteCategory.hom (M.presheaf.map (homOfLE hf).op)) t = 0
n : ι → ℕ
hn : ∀ (i : ι), (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (f ^ n i • t) = 0
i : ι
this✝ : n i ≤ ⨆ i, n i
this : ⨆ i, n i = (⨆ i, n i) - n i + n i
⊢ f ^ ((⨆ i, n i) - n i) • 0 = (ConcreteCategory.hom ({ obj := M.presheaf, property := ⋯ }.obj.map (homOfLE ⋯).op)) 0
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: case h.h
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
t : ↑Γ(M, V)
hs : (ConcreteCategory.hom (M.presheaf.map (homOfLE hf).op)) t = 0
n : ι → ℕ
hn : ∀ (i : ι), (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (f ^ n i • t) = 0
i : ι
this✝ : n i ≤ ⨆ i, n i
this : ⨆ i, n i = (⨆ i, n i) - n i + n i
⊢ f ^ ((⨆ i, n i) - n i) • 0 = (ConcreteCategory.hom ({ obj := M.presheaf, property := ⋯ }.obj.map (homOfLE ⋯).op)) 0

Tactic:
]

Goal state after:
case h.h
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
t : ↑Γ(M, V)
hs : (ConcreteCategory.hom (M.presheaf.map (homOfLE hf).op)) t = 0
n : ι → ℕ
hn : ∀ (i : ι), (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (f ^ n i • t) = 0
i : ι
this✝ : n i ≤ ⨆ i, n i
this : ⨆ i, n i = (⨆ i, n i) - n i + n i
⊢ f ^ ((⨆ i, n i) - n i) • 0 = (ConcreteCategory.hom ({ obj := M.presheaf, property := ⋯ }.obj.map (homOfLE ⋯).op)) 0
Module: Mathlib.CategoryTheory.Limits.Elements

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
A : C ⥤ Type w
I : Type u₁
inst✝³ : Category.{v₁, u₁} I
inst✝² : Small.{w, u₁} I
F : I ⥤ A.Elements
inst✝¹ : HasLimitsOfShape I C
inst✝ : PreservesLimitsOfShape I A
i i' : I
f : i ⟶ i'
⊢ ((Functor.const I).obj ⟨limit (F ⋙ π A), liftedConeElement F⟩).map f ≫ ⟨limit.π (F ⋙ π A) i', ⋯⟩ =
    ⟨limit.π (F ⋙ π A) i, ⋯⟩ ≫ F.map f

Tactic:
by ext; simpa using! (limit.w _ _).symm

Goal state after:
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense

Goal state before:
pp: case hR
C₀ : Type u₀
C : Type u
inst✝² : Category.{v₀, u₀} C₀
inst✝¹ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
inst✝ : IsDenseSubsite J₀ J F
X : C
data : F.OneHypercoverDenseData J₀ J X
i₁ i₂ : data.I₀
W : C
p₁ : W ⟶ F.obj (data.X i₁)
p₂ : W ⟶ F.obj (data.X i₂)
w : p₁ ≫ data.f i₁ = p₂ ≫ data.f i₂
this : F.IsCoverDense J
S : Sieve W :=
  Sieve.bind (Sieve.coverByImage F W).arrows fun Y f hf ↦
    Sieve.pullback (Nonempty.some hf).lift
      (Sieve.functorPushforward F
        (F.imageSieve ((Nonempty.some hf).map ≫ p₁) ⊓ F.imageSieve ((Nonempty.some hf).map ≫ p₂)))
T : Sieve W :=
  Sieve.bind S.arrows fun Z g hg ↦
    Sieve.pullback (Presieve.getFunctorPushforwardStructure ⋯).lift
      (Sieve.functorPushforward F (data.sieve₁₀ (Exists.choose ⋯) (Exists.choose ⋯)))
Y : C
f : Y ⟶ W
hf : (Sieve.coverByImage F W).arrows f
⊢ F.imageSieve ((Nonempty.some hf).map ≫ p₁) ⊓ F.imageSieve ((Nonempty.some hf).map ≫ p₂) ∈ J₀ (Nonempty.some hf).obj

Tactic:
]

Goal state after:
case hR
C₀ : Type u₀
C : Type u
inst✝² : Category.{v₀, u₀} C₀
inst✝¹ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
inst✝ : IsDenseSubsite J₀ J F
X : C
data : F.OneHypercoverDenseData J₀ J X
i₁ i₂ : data.I₀
W : C
p₁ : W ⟶ F.obj (data.X i₁)
p₂ : W ⟶ F.obj (data.X i₂)
w : p₁ ≫ data.f i₁ = p₂ ≫ data.f i₂
this : F.IsCoverDense J
S : Sieve W :=
  Sieve.bind (Sieve.coverByImage F W).arrows fun Y f hf ↦
    Sieve.pullback (Nonempty.some hf).lift
      (Sieve.functorPushforward F
        (F.imageSieve ((Nonempty.some hf).map ≫ p₁) ⊓ F.imageSieve ((Nonempty.some hf).map ≫ p₂)))
T : Sieve W :=
  Sieve.bind S.arrows fun Z g hg ↦
    Sieve.pullback (Presieve.getFunctorPushforwardStructure ⋯).lift
      (Sieve.functorPushforward F (data.sieve₁₀ (Exists.choose ⋯) (Exists.choose ⋯)))
Y : C
f : Y ⟶ W
hf : (Sieve.coverByImage F W).arrows f
⊢ F.imageSieve ((Nonempty.some hf).map ≫ p₁) ⊓ F.imageSieve ((Nonempty.some hf).map ≫ p₂) ∈ J₀ (Nonempty.some hf).obj