mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Etale.QuasiFinite

Goal state before:
pp: R : Type u
S : Type (max u v)
inst✝¹⁹ : CommRing R
inst✝¹⁸ : CommRing S
inst✝¹⁷ : Algebra R S
p : Ideal R
inst✝¹⁶ : p.IsPrime
q : Ideal S
R' : Type u
inst✝¹⁵ : CommRing R'
inst✝¹⁴ : Algebra R R'
inst✝¹³ : Etale R R'
P : Ideal R'
inst✝¹² : P.IsPrime
inst✝¹¹ : P.LiesOver p
e : R' ⊗[R] S
P' : Ideal (R' ⊗[R] S)
inst✝¹⁰ : P'.IsPrime
inst✝⁹ : P'.LiesOver P
hP'q : Ideal.comap TensorProduct.includeRight.toRingHom P' = q
heP' : e ∉ P'
hpP : Function.Bijective ⇑(Ideal.ResidueField.mapₐ p P (ofId R R') ⋯)
H : ∀ (P'' : Ideal (R' ⊗[R] S)), P''.IsPrime → P''.LiesOver P → e ∉ P'' → P'' = P'
R'' : Type u
inst✝⁸ : CommRing R''
inst✝⁷ : Algebra R' R''
inst✝⁶ : Algebra R R''
inst✝⁵ : IsScalarTower R R' R''
inst✝⁴ : Etale R' R''
Q : Ideal R''
inst✝³ : Q.IsPrime
inst✝² : Q.LiesOver P
n : ℕ
e' : Fin (n + 1 + 1) → R'' ⊗[R] S
he' : CompleteOrthogonalIdempotents e'
he'0 : e' 0 = (TensorProduct.map (ofId R' R'') (AlgHom.id R S)) e
Q' : Fin n → Ideal (R'' ⊗[R] S)
inst✝¹ : ∀ (i : Fin n), (Q' i).IsPrime
inst✝ : ∀ (i : Fin n), (Q' i).LiesOver Q
hPQ : Function.Bijective ⇑(Ideal.ResidueField.mapₐ P Q (ofId R' R'') ⋯)
hQ' : ∀ (i : Fin n), e' i.succ.castSucc ∉ Q' i
H' :
  ∀ (P'' : Ideal (R'' ⊗[R] S)),
    e' 0 ∈ P'' →
      P''.IsPrime → P''.LiesOver Q → e' (Fin.last (n + 1)) ∈ P'' ∧ ∀ (i : Fin n), e' i.succ.castSucc ∉ P'' → P'' = Q' i
φ : R' ⊗[R] S →ₐ[R'] R'' ⊗[R] S := TensorProduct.map (ofId R' R'') (AlgHom.id R S)
this : Q.LiesOver p
⊢ Function.Bijective ⇑(Ideal.ResidueField.mapₐ p Q (ofId R R'') ⋯)

Tactic:
convert hPQ.comp hpP

Goal state after:
R : Type u
S : Type (max u v)
inst✝¹⁹ : CommRing R
inst✝¹⁸ : CommRing S
inst✝¹⁷ : Algebra R S
p : Ideal R
inst✝¹⁶ : p.IsPrime
q : Ideal S
R' : Type u
inst✝¹⁵ : CommRing R'
inst✝¹⁴ : Algebra R R'
inst✝¹³ : Etale R R'
P : Ideal R'
inst✝¹² : P.IsPrime
inst✝¹¹ : P.LiesOver p
e : R' ⊗[R] S
P' : Ideal (R' ⊗[R] S)
inst✝¹⁰ : P'.IsPrime
inst✝⁹ : P'.LiesOver P
hP'q : Ideal.comap TensorProduct.includeRight.toRingHom P' = q
heP' : e ∉ P'
hpP : Function.Bijective ⇑(Ideal.ResidueField.mapₐ p P (ofId R R') ⋯)
H : ∀ (P'' : Ideal (R' ⊗[R] S)), P''.IsPrime → P''.LiesOver P → e ∉ P'' → P'' = P'
R'' : Type u
inst✝⁸ : CommRing R''
inst✝⁷ : Algebra R' R''
inst✝⁶ : Algebra R R''
inst✝⁵ : IsScalarTower R R' R''
inst✝⁴ : Etale R' R''
Q : Ideal R''
inst✝³ : Q.IsPrime
inst✝² : Q.LiesOver P
n : ℕ
e' : Fin (n + 1 + 1) → R'' ⊗[R] S
he' : CompleteOrthogonalIdempotents e'
he'0 : e' 0 = (TensorProduct.map (ofId R' R'') (AlgHom.id R S)) e
Q' : Fin n → Ideal (R'' ⊗[R] S)
inst✝¹ : ∀ (i : Fin n), (Q' i).IsPrime
inst✝ : ∀ (i : Fin n), (Q' i).LiesOver Q
hPQ : Function.Bijective ⇑(Ideal.ResidueField.mapₐ P Q (ofId R' R'') ⋯)
hQ' : ∀ (i : Fin n), e' i.succ.castSucc ∉ Q' i
H' :
  ∀ (P'' : Ideal (R'' ⊗[R] S)),
    e' 0 ∈ P'' →
      P''.IsPrime → P''.LiesOver Q → e' (Fin.last (n + 1)) ∈ P'' ∧ ∀ (i : Fin n), e' i.succ.castSucc ∉ P'' → P'' = Q' i
φ : R' ⊗[R] S →ₐ[R'] R'' ⊗[R] S := TensorProduct.map (ofId R' R'') (AlgHom.id R S)
this : Q.LiesOver p
⊢ ⇑(Ideal.ResidueField.mapₐ p Q (ofId R R'') ⋯) =
    ⇑(Ideal.ResidueField.mapₐ P Q (ofId R' R'') ⋯) ∘ ⇑(Ideal.ResidueField.mapₐ p P (ofId R R') ⋯)
Module: Mathlib.AlgebraicGeometry.Group.Affine

Goal state before:
pp: R : CommRingCat
⊢ PreservesColimitsOfSize.{w, v, u, u, u + 1, u + 1} (algΓ R)

Tactic:
unfold algΓ; infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ F : StrictlyUnitaryPseudofunctor B C
G : StrictlyUnitaryPseudofunctor C D
x✝ : B
⊢ (F.comp G.toPseudofunctor).map (𝟙 x✝) = 𝟙 ((F.comp G.toPseudofunctor).obj x✝)

Tactic:
by simp [StrictlyUnitaryPseudofunctor.map_id]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Adj

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a✝ b✝ c d a b : Adj B
adj₁ adj₂ : a ⟶ b
e : adj₁ ≅ adj₂
⊢ e.inv.τr ≫ e.hom.τr = 𝟙 adj₁.r

Tactic:
by rw [← comp_τr, e.hom_inv_id, id_τr]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank

Goal state before:
pp: X S Y T : Scheme
f : X ⟶ S
inst✝³ : IsAffine S
inst✝² : IsAffine T
f' : Y ⟶ T
g' : Y ⟶ X
g : T ⟶ S
h : IsPullback g' f' f g
inst✝¹ : Flat f
inst✝ : IsFinite f
t : ↥T
this✝ : IsAffine X
this : IsPushout (Scheme.Hom.appTop f) (Scheme.Hom.appTop g) (Scheme.Hom.appTop g') (Scheme.Hom.appTop f')
⊢ (CommRingCat.Hom.hom (Scheme.Hom.appTop f')).finrank (T.isoSpec.hom t) =
    (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).finrank (S.isoSpec.hom (g t))

Tactic:
CommRingCat.finrank_eq_of_isPushout this f.flat_appTop f.finite_appTop (T.isoSpec.hom t),

Goal state after:
X S Y T : Scheme
f : X ⟶ S
inst✝³ : IsAffine S
inst✝² : IsAffine T
f' : Y ⟶ T
g' : Y ⟶ X
g : T ⟶ S
h : IsPullback g' f' f g
inst✝¹ : Flat f
inst✝ : IsFinite f
t : ↥T
this✝ : IsAffine X
this : IsPushout (Scheme.Hom.appTop f) (Scheme.Hom.appTop g) (Scheme.Hom.appTop g') (Scheme.Hom.appTop f')
⊢ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).finrank
      (PrimeSpectrum.comap (CommRingCat.Hom.hom (Scheme.Hom.appTop g)) (T.isoSpec.hom t)) =
    (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).finrank (S.isoSpec.hom (g t))
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank

Goal state before:
pp: R S : CommRingCat
x : ↥(Spec S)
φ : R ⟶ S
inst✝¹ : (CommRingCat.Hom.hom φ).Flat
inst✝ : (CommRingCat.Hom.hom φ).Finite
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom φ).toAlgebra
algebraizeInst✝¹ : Module.Flat ↑R ↑S
algebraizeInst✝ : Module.Finite ↑R ↑S
⊢ 1 ≤ (CommRingCat.Hom.hom φ).finrank ((Spec.map φ) x)

Tactic:
← RingHom.algebraMap_toAlgebra φ.hom,

Goal state after:
R S : CommRingCat
x : ↥(Spec S)
φ : R ⟶ S
inst✝¹ : (CommRingCat.Hom.hom φ).Flat
inst✝ : (CommRingCat.Hom.hom φ).Finite
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom φ).toAlgebra
algebraizeInst✝¹ : Module.Flat ↑R ↑S
algebraizeInst✝ : Module.Finite ↑R ↑S
⊢ 1 ≤ (algebraMap ↑R ↑S).finrank ((Spec.map φ) x)
Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors

Goal state before:
pp: case inr
R : Type u_1
inst✝ : CommRing R
σ : Type u_3
a✝ : Nontrivial R
h✝ : Infinite σ
⊢ ringKrullDim R + ↑(ENat.card σ) ≤ ringKrullDim (MvPolynomial σ R)

Tactic:
simp only [ENat.card_eq_top_of_infinite, WithBot.coe_top]

Goal state after:
case inr
R : Type u_1
inst✝ : CommRing R
σ : Type u_3
a✝ : Nontrivial R
h✝ : Infinite σ
⊢ ringKrullDim R + ⊤ ≤ ringKrullDim (MvPolynomial σ R)
Module: Mathlib.RingTheory.OrderOfVanishing.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a x : R
this : span {a * x} ≤ span {x}
⊢ Module.length R (R ⧸ span {x}) ≤ Module.length R (R ⧸ span {a * x})

Tactic:
let g : (R ⧸ Ideal.span {a * x}) →ₗ[R] (R ⧸ Ideal.span {x}) := Submodule.factor this
    refine Module.length_le_of_surjective (Submodule.factor this) (Submodule.factor_surjective this)

Goal state after:
Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x : R
⊢ ord R x = (IsDiscreteValuationRing.addVal R) x

Tactic:
by
  by_cases hx : x = 0
  · simp only [ord, hx, AddValuation.map_zero]
    subst hx
    by_contra!
    rw [Module.length_ne_top_iff, isFiniteLength_iff_isNoetherian_isArtinian] at this
    have art := this.2
    rw [Ideal.span_singleton_zero] at art
    have : IsArtinianRing R :=
      (LinearEquiv.isArtinian_iff (Submodule.quotEquivOfEqBot ⊥ rfl).symm).mpr art
    exact IsDiscreteValuationRing.not_krullDimLE_zero R inferInstance
  obtain ⟨ϖ, hϖ⟩ := IsDiscreteValuationRing.exists_irreducible R
  obtain ⟨m, α, rfl⟩ := IsDiscreteValuationRing.eq_unit_mul_pow_irreducible hx hϖ
  rw [ord_mul, ord_pow, ord_of_irreducible hϖ]
  · simp [IsDiscreteValuationRing.addVal_uniformizer hϖ]
  all_goals simp_all [Irreducible.ne_zero hϖ]

Goal state after:
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
t t' : Set (ProjectiveSpectrum 𝒜)
f : A
hf : ∀ x ∈ t, f ∈ x.asHomogeneousIdeal
g : A
hg : ∀ x ∈ t', g ∈ x.asHomogeneousIdeal
x : ProjectiveSpectrum 𝒜
hxt : x ∈ t
hxt' : x ∈ t'
⊢ f + g ∈ x.asHomogeneousIdeal

Tactic:
apply Submodule.add_mem

Goal state after:
case h₁
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
t t' : Set (ProjectiveSpectrum 𝒜)
f : A
hf : ∀ x ∈ t, f ∈ x.asHomogeneousIdeal
g : A
hg : ∀ x ∈ t', g ∈ x.asHomogeneousIdeal
x : ProjectiveSpectrum 𝒜
hxt : x ∈ t
hxt' : x ∈ t'
⊢ f ∈ x.asHomogeneousIdeal.toSubmodule

case h₂
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
t t' : Set (ProjectiveSpectrum 𝒜)
f : A
hf : ∀ x ∈ t, f ∈ x.asHomogeneousIdeal
g : A
hg : ∀ x ∈ t', g ∈ x.asHomogeneousIdeal
x : ProjectiveSpectrum 𝒜
hxt : x ∈ t
hxt' : x ∈ t'
⊢ g ∈ x.asHomogeneousIdeal.toSubmodule
Module: Mathlib.RingTheory.GradedAlgebra.FiniteType

Goal state before:
pp: S : Type u_1
σ : Type u_2
ι : Type u_3
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : CommRing S
inst✝³ : SetLike σ S
inst✝² : AddSubgroupClass σ S
𝒜 : ι → σ
inst✝¹ : GradedRing 𝒜
inst✝ : Algebra.FiniteType (↥(𝒜 0)) S
⊢ ∃ s, Algebra.adjoin ↥(𝒜 0) ↑s = ⊤ ∧ ∀ i ∈ s, ∃ n, n ≠ 0 ∧ i ∈ 𝒜 n

Tactic:
by
  obtain ⟨s, h₁, h₂⟩ := exists_finset_adjoin_eq_top_and_homogeneous 𝒜
  choose! n hn using h₂
  refine ⟨s.filter (n · ≠ 0), ?_, by simpa using fun i hi hin ↦ ⟨n i, hin, hn i hi⟩⟩
  rw [← top_le_iff, ← h₁, Algebra.adjoin_le_iff]
  rintro i hi
  by_cases hi0 : n i = 0
  · exact Subalgebra.algebraMap_mem
      (Algebra.adjoin (𝒜 0) (s.filter (n · ≠ 0) : Set S)) ⟨i, hi0 ▸ hn i hi⟩
  · exact Algebra.subset_adjoin (by simpa [hi0] using hi)

Goal state after:
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝¹ : CommRing A
inst✝ : SetLike σ A
𝒜 : ι → σ
x : Submonoid A
f : HomogeneousLocalization 𝒜 x
⊢ f.den • f.val = (algebraMap A (at x)) f.num

Tactic:
rw [eq_num_div_den, Localization.mk_eq_mk', IsLocalization.smul_mk']

Goal state after:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝¹ : CommRing A
inst✝ : SetLike σ A
𝒜 : ι → σ
x : Submonoid A
f : HomogeneousLocalization 𝒜 x
⊢ IsLocalization.mk' (at x) (f.den * f.num) ⟨f.den, ⋯⟩ = (algebraMap A (at x)) f.num
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic

Goal state before:
pp: σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
X : Scheme
f✝ : A →+* ↑Γ(X, ⊤)
x x' : ↑Γ(X, ⊤)
t t' : A
d d' : ℕ
f : A →+* ↑Γ(X, ⊤)
hf : Ideal.map f (HomogeneousIdeal.irrelevant 𝒜).toIdeal = ⊤
H : Ideal.span (Set.range fun x ↦ x.snd.fst) = (HomogeneousIdeal.irrelevant 𝒜).toIdeal
⊢ X.zeroLocus (Set.range fun x ↦ f x.snd.fst) = ∅

Tactic:
rw [← Scheme.zeroLocus_span, Set.range_comp', ← Ideal.map_span, H, hf]

Goal state after:
σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
X : Scheme
f✝ : A →+* ↑Γ(X, ⊤)
x x' : ↑Γ(X, ⊤)
t t' : A
d d' : ℕ
f : A →+* ↑Γ(X, ⊤)
hf : Ideal.map f (HomogeneousIdeal.irrelevant 𝒜).toIdeal = ⊤
H : Ideal.span (Set.range fun x ↦ x.snd.fst) = (HomogeneousIdeal.irrelevant 𝒜).toIdeal
⊢ X.zeroLocus ↑⊤ = ∅
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: case neg.zero
ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : SetLike σ A
inst✝⁴ : AddSubgroupClass σ A
inst✝³ : AddCommMonoid ι
inst✝² : DecidableEq ι
𝒜 : ι → σ
inst✝¹ : GradedRing 𝒜
f : A
d : ι
hf : f ∈ 𝒜 d
ι' : Type u_4
inst✝ : Fintype ι'
v : ι' → A
hx : Algebra.adjoin (↥(𝒜 0)) (Set.range v) = ⊤
dv : ι' → ι
hxd : ∀ (i : ι'), v i ∈ 𝒜 (dv i)
HH : ¬Subsingleton (Away 𝒜 f)
n : ι
a : A
j : ℕ
hb' : (fun x ↦ f ^ x) j ∈ 𝒜 n
hfj : ¬f ^ j = 0
⊢ mk { deg := n, num := ((decompose 𝒜) 0) n, den := ⟨f ^ j, hb'⟩, den_mem := ⋯ } ∈
    Submodule.span ↥(𝒜 0) {x | ∃ a ai, ∃ (hai : ∑ i, ai i • dv i = a • d), Away.mk 𝒜 hf a (∏ i, v i ^ ai i) ⋯ = x}

Tactic:
convert! zero_mem (Submodule.span (𝒜 0) _)
    ext; simp [Localization.mk_zero]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: R : CommRingCat
M✝ M : ModuleCat ↑R
⊢ Function.Bijective ⇑(ConcreteCategory.hom (ModuleCat.ofHom (StructureSheaf.toOpenₗ ↑R ↑M ⊤)))

Tactic:
exact StructureSheaf.toOpenₗ_top_bijective

Goal state after:
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: R : CommRingCat
M✝ M : ModuleCat ↑R
⊢ IsIso (toOpen M ⊤)

Tactic:
rw [toOpen, isIso_comp_right_iff, ConcreteCategory.isIso_iff_bijective]
  exact StructureSheaf.toOpenₗ_top_bijective

Goal state after:
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor

Goal state before:
pp: A : Type u_1
B : Type u_2
σ : Type u_4
τ : Type u_5
inst✝⁷ : CommRing A
inst✝⁶ : SetLike σ A
inst✝⁵ : AddSubgroupClass σ A
inst✝⁴ : CommRing B
inst✝³ : SetLike τ B
inst✝² : AddSubgroupClass τ B
𝒜 : ℕ → σ
ℬ : ℕ → τ
inst✝¹ : GradedRing 𝒜
inst✝ : GradedRing ℬ
f : 𝒜 →+*ᵍ ℬ
hf : ℬ₊ ≤ HomogeneousIdeal.map f (𝒜₊)
U : Opens (ProjectiveSpectrum 𝒜)
V : Opens (ProjectiveSpectrum ℬ)
hUV : V.carrier ⊆ ⇑(ProjectiveSpectrum.comap f hf) ⁻¹' U.carrier
s : (x : ↥U) → AtPrime 𝒜 (↑x).asHomogeneousIdeal.toSubmodule
hs : (ProjectiveSpectrum.StructureSheaf.isLocallyFraction 𝒜).pred s
p : ↑(top ℬ)
hpV : p ∈ V
W : Opens ↑(top 𝒜)
m : ↑⟨(ProjectiveSpectrum.comap f hf) p, ⋯⟩ ∈ W
iWU : W ⟶ U
i : ℕ
a b : ↥(𝒜 i)
hb : ∀ (x : ↥W), ↑b ∉ (↑x).asHomogeneousIdeal
x✝ : ↥((Opens.comap (ProjectiveSpectrum.comap f hf)) W ⊓ V)
q : ↑(top ℬ)
hqW : q ∈ ↑((Opens.comap (ProjectiveSpectrum.comap f hf)) W)
h_frac :
  (fun x ↦ s (iWU x)) ⟨(ProjectiveSpectrum.comap f hf) q, hqW⟩ =
    HomogeneousLocalization.mk { deg := i, num := a, den := b, den_mem := ⋯ }
hqV : q ∈ ↑V
⊢ val
      ((fun x ↦
          comapStructureSheafFun f hf U V hUV s ((((Opens.comap (ProjectiveSpectrum.comap f hf)) W).infLERight V) x))
        ⟨q, ⋯⟩) =
    (HomogeneousLocalization.mk
        { deg := i, num := (f.gradedAddHom i) a, den := (f.gradedAddHom i) b, den_mem := ⋯ }).val

Tactic:
simp_all [comapStructureSheafFun]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: X : Scheme
M : X.Modules
inst✝ : SheafOfModules.IsQuasicoherent M
I : Type u
W : I → TopologicalSpace.Opens ↥X
cov : (Opens.grothendieckTopology ↥X).CoversTop W
pres : (i : I) → (SheafOfModules.over M (W i)).Presentation
κ : I → Set (TopologicalSpace.Opens ↥X)
hsub : ∀ (i : I), κ i ⊆ X.affineOpens
heq : ∀ (i : I), W i = sSup (κ i)
i : (i : I) × ↑(κ i)
⊢ ↑i.snd ≤ W i.fst

Tactic:
by simp [heq, le_sSup]

Goal state after:
Module: Mathlib.RingTheory.Valuation.LocalSubring

Goal state before:
pp: case inl
K : Type u_3
inst✝¹ : Field K
R : LocalSubring K
inst✝ : IsIntegrallyClosedIn (↥R.toSubring) K
hxR : 0 ∉ R.toSubring
⊢ ∃ V, R ≤ V.toLocalSubring ∧ 0 ∉ V

Tactic:
exact (hxR R.toSubring.zero_mem).elim

Goal state after:
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
x : ↑↑(Proj.restrict ⋯).toPresheafedSpace
⊢ awayToSection 𝒜 f ≫
      (structureSheaf 𝒜).obj.map (homOfLE ⋯).op ≫
        Proj.presheaf.germ (⋯.functor.obj ⊤) ((ConcreteCategory.hom (pbo f).inclusion') x) ⋯ =
    CommRingCat.ofHom (HomogeneousLocalization.mapId 𝒜 ⋯) ≫ («Proj».stalkIso' 𝒜 ↑x).toCommRingCatIso.inv

Tactic:
simp only [Proj.toLocallyRingedSpace, Proj.toSheafedSpace]

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
x : ↑↑(Proj.restrict ⋯).toPresheafedSpace
⊢ awayToSection 𝒜 f ≫
      (structureSheaf 𝒜).obj.map (homOfLE ⋯).op ≫
        Presheaf.germ (structureSheaf 𝒜).obj (⋯.functor.obj ⊤) ((ConcreteCategory.hom (pbo f).inclusion') x) ⋯ =
    CommRingCat.ofHom (HomogeneousLocalization.mapId 𝒜 ⋯) ≫ («Proj».stalkIso' 𝒜 ↑x).toCommRingCatIso.inv
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
x : ↥(pbo f)
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
a : A⁰_ f
⊢ (ConcreteCategory.hom
        (CommRingCat.ofHom (mapId 𝒜 ⋯) ≫
          («Proj».stalkIso' 𝒜 ↑x).toCommRingCatIso.inv ≫ (Proj.restrictStalkIso ⋯ x).inv))
      a =
    ((CommRingCat.Hom.hom
            ((specStalkEquiv 𝒜 f x f_deg hm).hom ≫
              («Proj».stalkIso' 𝒜 ↑x).toCommRingCatIso.inv ≫ (Proj.restrictStalkIso ⋯ x).inv)).comp
        (algebraMap (A⁰_ f)
          ↑((«Spec».structureSheaf (A⁰_ f)).presheaf.stalk ((ConcreteCategory.hom (toSpec 𝒜 f).base) x))))
      a

Tactic:
← toStalk_specStalkEquiv,

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
x : ↥(pbo f)
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
a : A⁰_ f
⊢ (ConcreteCategory.hom
        ((StructureSheaf.toStalk (A⁰_ f) ((ConcreteCategory.hom (toSpec 𝒜 f).base) x) ≫
            (specStalkEquiv 𝒜 f x ?f_deg ?hm).hom) ≫
          («Proj».stalkIso' 𝒜 ↑x).toCommRingCatIso.inv ≫ (Proj.restrictStalkIso ⋯ x).inv))
      a =
    ((CommRingCat.Hom.hom
            ((specStalkEquiv 𝒜 f x f_deg hm).hom ≫
              («Proj».stalkIso' 𝒜 ↑x).toCommRingCatIso.inv ≫ (Proj.restrictStalkIso ⋯ x).inv)).comp
        (algebraMap (A⁰_ f)
          ↑((«Spec».structureSheaf (A⁰_ f)).presheaf.stalk ((ConcreteCategory.hom (toSpec 𝒜 f).base) x))))
      a

case m
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
x : ↥(pbo f)
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
a : A⁰_ f
⊢ ℕ

case f_deg
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
x : ↥(pbo f)
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
a : A⁰_ f
⊢ f ∈ 𝒜 ?m

case hm
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
x : ↥(pbo f)
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
a : A⁰_ f
⊢ 0 < ?m
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
A : Type u'
inst✝ : Category.{v', u'} A
X : C
data : F.PreOneHypercoverDenseData X
i₁ i₂ : data.I₀
W₀ : C₀
p₁ : W₀ ⟶ data.X i₁
p₂ : W₀ ⟶ data.X i₂
⊢ ∀ {Y Z : C₀} {f : Y ⟶ W₀},
    (∃ j h, f ≫ p₁ = h ≫ data.p₁ j ∧ f ≫ p₂ = h ≫ data.p₂ j) →
      ∀ (g : Z ⟶ Y), ∃ j h, (g ≫ f) ≫ p₁ = h ≫ data.p₁ j ∧ (g ≫ f) ≫ p₂ = h ≫ data.p₂ j

Tactic:
rintro Z Z' g ⟨j, h, fac₁, fac₂⟩ φ
    exact ⟨j, φ ≫ h, by simpa using φ ≫= fac₁, by simpa using φ ≫= fac₂⟩

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

Goal state before:
pp: case refine_3.inr.refine_2
P : MorphismProperty Scheme
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
F : Schemeᵒᵖ ⥤ Type u_1
inst✝ : IsZariskiLocalAtSource P
x✝ :
  Presieve.IsSheaf zariskiTopology F ∧
    ∀ {R S : CommRingCat} (f : R ⟶ S),
      P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
hzar : Presieve.IsSheaf zariskiTopology F
hff :
  ∀ {R S : CommRingCat} (f : R ⟶ S),
    P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
T : Scheme
𝒰 : Cover (propQCPrecoverage P) T
this : ∀ ⦃T : Scheme⦄ (𝒰 : Cover (propQCPrecoverage P) T), (∃ R, T = Spec R) → Presieve.IsSheafFor F 𝒰.presieve₀
hT : ¬∃ R, T = Spec R
⊢ ∀ ⦃i j : T.affineOneHypercover.I₀⦄ (k : T.affineOneHypercover.I₁ i j),
    Presieve.IsSeparatedFor F
      (Sieve.pullback (T.affineOneHypercover.p₁ k ≫ T.affineOneHypercover.f i) (Sieve.generate 𝒰.presieve₀)).arrows

Tactic:
intro i j k

Goal state after:
case refine_3.inr.refine_2
P : MorphismProperty Scheme
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
F : Schemeᵒᵖ ⥤ Type u_1
inst✝ : IsZariskiLocalAtSource P
x✝ :
  Presieve.IsSheaf zariskiTopology F ∧
    ∀ {R S : CommRingCat} (f : R ⟶ S),
      P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
hzar : Presieve.IsSheaf zariskiTopology F
hff :
  ∀ {R S : CommRingCat} (f : R ⟶ S),
    P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
T : Scheme
𝒰 : Cover (propQCPrecoverage P) T
this : ∀ ⦃T : Scheme⦄ (𝒰 : Cover (propQCPrecoverage P) T), (∃ R, T = Spec R) → Presieve.IsSheafFor F 𝒰.presieve₀
hT : ¬∃ R, T = Spec R
i j : T.affineOneHypercover.I₀
k : T.affineOneHypercover.I₁ i j
⊢ Presieve.IsSeparatedFor F
    (Sieve.pullback (T.affineOneHypercover.p₁ k ≫ T.affineOneHypercover.f i) (Sieve.generate 𝒰.presieve₀)).arrows
Module: Mathlib.CategoryTheory.Abelian.CommSq

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h₁ : IsPushout t l r b
X₅ : C
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₂ : IsPullback t l r' b'
k : X₄ ⟶ X₅
fac₁ : r ≫ k = r'
fac₂ : b ≫ k = b'
inst✝ : Mono r'
T₀ : C
x₄ : T₀ ⟶ X₄
hx₄ : x₄ ≫ k = 0
T₁ : C
π : T₁ ⟶ T₀
w✝ : Epi π
x₂ : T₁ ⟶ X₂
x₃ : T₁ ⟶ X₃
eq : π ≫ x₄ = x₂ ≫ r + x₃ ≫ b
⊢ π ≫ x₄ ≫ k = 0

Tactic:
hx₄,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h₁ : IsPushout t l r b
X₅ : C
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₂ : IsPullback t l r' b'
k : X₄ ⟶ X₅
fac₁ : r ≫ k = r'
fac₂ : b ≫ k = b'
inst✝ : Mono r'
T₀ : C
x₄ : T₀ ⟶ X₄
hx₄ : x₄ ≫ k = 0
T₁ : C
π : T₁ ⟶ T₀
w✝ : Epi π
x₂ : T₁ ⟶ X₂
x₃ : T₁ ⟶ X₃
eq : π ≫ x₄ = x₂ ≫ r + x₃ ≫ b
⊢ π ≫ 0 = 0
Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
J : Type u'
inst✝³ : Category.{v', u'} J
inst✝² : HasColimitsOfShape J C
inst✝¹ : HasExactColimitsOfShape J C
inst✝ : HasZeroMorphisms C
S : ShortComplex (J ⥤ C)
hS : S.Exact
c₁ : Cocone S.X₁
hc₁ : IsColimit c₁
c₂ : Cocone S.X₂
hc₂ : IsColimit c₂
c₃ : Cocone S.X₃
hc₃ : IsColimit c₃
f : c₁.pt ⟶ c₂.pt
g : c₂.pt ⟶ c₃.pt
hf : ∀ (j : J), c₁.ι.app j ≫ f = S.f.app j ≫ c₂.ι.app j
hg : ∀ (j : J), c₂.ι.app j ≫ g = S.g.app j ≫ c₃.ι.app j
j : J
⊢ (S.f ≫ S.g).app j ≫ c₃.ι.app j = 0

Tactic:
S.zero,

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
J : Type u'
inst✝³ : Category.{v', u'} J
inst✝² : HasColimitsOfShape J C
inst✝¹ : HasExactColimitsOfShape J C
inst✝ : HasZeroMorphisms C
S : ShortComplex (J ⥤ C)
hS : S.Exact
c₁ : Cocone S.X₁
hc₁ : IsColimit c₁
c₂ : Cocone S.X₂
hc₂ : IsColimit c₂
c₃ : Cocone S.X₃
hc₃ : IsColimit c₃
f : c₁.pt ⟶ c₂.pt
g : c₂.pt ⟶ c₃.pt
hf : ∀ (j : J), c₁.ι.app j ≫ f = S.f.app j ≫ c₂.ι.app j
hg : ∀ (j : J), c₂.ι.app j ≫ g = S.g.app j ≫ c₃.ι.app j
j : J
⊢ NatTrans.app 0 j ≫ c₃.ι.app j = 0