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

Goal state before:
pp: R : Type u
S : Type v
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : FiniteType R S
p : Ideal R
inst✝³ : p.IsPrime
q✝ : Ideal S
inst✝² : q✝.IsPrime
inst✝¹ : q✝.LiesOver p
inst✝ : QuasiFiniteAt R q✝
s : S
hsq : s ∉ q✝
hRs : IsIntegral R s
hs : ∀ (q' : Ideal S), q'.IsPrime → q' ≠ q✝ → q'.LiesOver p → s ∈ q'
hs₀ :
  ∀ (q' : Ideal ↥(integralClosure R S)),
    q'.IsPrime → q' ≠ Ideal.under (↥(integralClosure R S)) q✝ → q'.LiesOver p → ⟨s, hRs⟩ ∈ q'
f : R[X] := X * minpoly R s
q : p.ResidueField[X]
hq :
  Polynomial.map (algebraMap R p.ResidueField) (minpoly R s) =
    (X - C 0) ^ rootMultiplicity 0 (Polynomial.map (algebraMap R p.ResidueField) (minpoly R s)) * q
hq' : ¬X - C 0 ∣ q
⊢ q.Monic

Tactic:
simpa [((minpoly.monic hRs).map _).leadingCoeff] using! congr(leadingCoeff $hq).symm

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.CommGrp_

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
X : C
G : CommGrp C
H I : (Grp C)ᵒᵖ
f : H ⟶ I
g h : unop H ⟶ G.toGrp
⊢ f.unop ≫ (g * h) = f.unop ≫ g * f.unop ≫ h

Tactic:
ext
      simpa using! ((yonedaGrpObj G.X).map f.unop.hom.hom.op).hom.map_mul g.hom.hom h.hom.hom

Goal state after:
Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem

Goal state before:
pp: case refine_3
X S : Scheme
f : X ⟶ S
inst✝¹ : LocallyOfFiniteType f
inst✝ : IsSeparated f
x : ↥X
s : ↥S
h : f x = s
hx : Scheme.Hom.QuasiFiniteAt f x
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hxU : f x ∈ ↑U
V : TopologicalSpace.Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hUV : V ≤ f ⁻¹ᵁ U
this✝⁵ : (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hUV)).FiniteType
algInst✝ : Algebra ↑Γ(S, U) ↑Γ(X, V) := (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hUV)).toAlgebra
algebraizeInst✝ : Algebra.FiniteType ↑Γ(S, U) ↑Γ(X, V)
this✝⁴ : (IsAffineOpen.primeIdealOf hV ⟨x, hxV⟩).asIdeal.LiesOver (IsAffineOpen.primeIdealOf hU ⟨f x, hxU⟩).asIdeal
this✝³ : Algebra.QuasiFiniteAt (↑Γ(S, U)) (IsAffineOpen.primeIdealOf hV ⟨x, hxV⟩).asIdeal
R : Type u
w✝⁷ : CommRing R
w✝⁶ : Algebra (↑Γ(S, U)) R
w✝⁵ : Algebra.Etale (↑Γ(S, U)) R
P : Ideal R
w✝⁴ : P.IsPrime
w✝³ : P.LiesOver (IsAffineOpen.primeIdealOf hU ⟨f x, hxU⟩).asIdeal
e : R ⊗[↑Γ(S, U)] ↑Γ(X, V)
w✝² : IsIdempotentElem e
P' : Ideal (R ⊗[↑Γ(S, U)] ↑Γ(X, V))
w✝¹ : P'.IsPrime
w✝ : P'.LiesOver P
hP' : Ideal.comap Algebra.TensorProduct.includeRight.toRingHom P' = (IsAffineOpen.primeIdealOf hV ⟨x, hxV⟩).asIdeal
heP' : e ∉ P'
left✝ : Module.Finite R (Localization.Away e)
this✝² : (algebraMap R (Localization.Away e)).Finite
φ : Γ(S, U) ⟶ CommRingCat.of R := CommRingCat.ofHom (algebraMap (↑Γ(S, U)) R)
hφ : (CommRingCat.Hom.hom φ).Etale
this✝¹ : Etale (Spec.map φ)
e₁ : Spec (CommRingCat.of (R ⊗[↑Γ(S, U)] ↑Γ(X, V))) ≅ pullback (Spec.map (Scheme.Hom.appLE f U V hUV)) (Spec.map φ) :=
  (pullbackSpecIso (↑Γ(S, U)) R ↑Γ(X, V)).symm ≪≫
    pullbackSymmetry (Spec.map (CommRingCat.ofHom (algebraMap (↑Γ(S, U)) R)))
      (Spec.map (CommRingCat.ofHom (algebraMap ↑Γ(S, U) ↑Γ(X, V))))
he₁ :
  e₁.hom ≫ pullback.fst (Spec.map (Scheme.Hom.appLE f U V hUV)) (Spec.map φ) =
    Spec.map (CommRingCat.ofHom Algebra.TensorProduct.includeRight.toRingHom)
g : Spec (CommRingCat.of (R ⊗[↑Γ(S, U)] ↑Γ(X, V))) ⟶ pullback f (Spec.map φ ≫ IsAffineOpen.fromSpec hU) :=
  e₁.hom ≫
    pullback.map (Spec.map (Scheme.Hom.appLE f U V hUV)) (Spec.map φ) f (Spec.map φ ≫ IsAffineOpen.fromSpec hU)
      (IsAffineOpen.fromSpec hV) (𝟙 (Spec (CommRingCat.of R))) (IsAffineOpen.fromSpec hU) ⋯ ⋯
W₁ : (pullback f (Spec.map φ ≫ IsAffineOpen.fromSpec hU)).Opens := g ''ᵁ PrimeSpectrum.basicOpen e
this✝ : IsFinite (W₁.ι ≫ pullback.snd f (Spec.map φ ≫ IsAffineOpen.fromSpec hU))
this : IsFinite W₁.ι
W₂ : (pullback f (Spec.map φ ≫ IsAffineOpen.fromSpec hU)).Opens := { carrier := (↑W₁)ᶜ, is_open' := ⋯ }
⊢ IsCompl W₁ W₂

Tactic:
simp [isCompl_iff, disjoint_iff, codisjoint_iff, W₂, SetLike.ext'_iff]

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Descent

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
T : Type u_3
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : FaithfullyFlat R T
inst✝ : Module.Finite T (T ⊗[R] M)
n : ℕ
s : Fin n → T ⊗[R] M
hs : Submodule.span T (Set.range s) = ⊤
k : Fin n → ℕ
t : (i : Fin n) → Fin (k i) → T
m : (i : Fin n) → Fin (k i) → M
h : ∀ (i : Fin n), s i = ∑ j, t i j ⊗ₜ[R] m i j
f₀ : ((i : Fin n) × Fin (k i) → R) →ₗ[R] M :=
  ((Pi.basisFun R ((i : Fin n) × Fin (k i))).constr R) fun x ↦
    match x with
    | ⟨i, j⟩ => m i j
⊢ Set.range s ⊆ ↑((AlgebraTensorModule.lTensor T T) f₀).range

Tactic:
Set.range_subset_iff

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
T : Type u_3
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : FaithfullyFlat R T
inst✝ : Module.Finite T (T ⊗[R] M)
n : ℕ
s : Fin n → T ⊗[R] M
hs : Submodule.span T (Set.range s) = ⊤
k : Fin n → ℕ
t : (i : Fin n) → Fin (k i) → T
m : (i : Fin n) → Fin (k i) → M
h : ∀ (i : Fin n), s i = ∑ j, t i j ⊗ₜ[R] m i j
f₀ : ((i : Fin n) × Fin (k i) → R) →ₗ[R] M :=
  ((Pi.basisFun R ((i : Fin n) × Fin (k i))).constr R) fun x ↦
    match x with
    | ⟨i, j⟩ => m i j
⊢ ∀ (y : Fin n), s y ∈ ↑((AlgebraTensorModule.lTensor T T) f₀).range
Module: Mathlib.AlgebraicGeometry.Group.Affine

Goal state before:
pp: case h₁
R✝ R A : CommRingCat
inst✝¹ : Bialgebra ↑R ↑A
inst✝ : IsCocomm ↑R ↑A
this :
  (pullbackSpecIso ↑R ↑A ↑A).hom ≫
      Spec.map
        (Under.Hom.right (↑(Bialgebra.comulBialgHom ↑R ↑A)).toUnder ≫
          Under.Hom.right (↑↑(Bialgebra.TensorProduct.comm ↑R ↑A ↑A)).toUnder) =
    (pullbackSpecIso ↑R ↑A ↑A).hom ≫ Spec.map (Under.Hom.right (↑(Bialgebra.comulBialgHom ↑R ↑A)).toUnder)
h₁ :
  ↑Algebra.TensorProduct.includeRight =
    (↑(Bialgebra.TensorProduct.comm ↑R ↑A ↑A)).comp Algebra.TensorProduct.includeLeftRingHom
h₂ :
  Algebra.TensorProduct.includeLeftRingHom =
    (↑(Bialgebra.TensorProduct.comm ↑R ↑A ↑A)).comp ↑Algebra.TensorProduct.includeRight
e_1✝ :
  (pullback (Spec A ↘ Spec R) (Spec A ↘ Spec R) ⟶ Spec A) =
    (pullback (Spec.map (CommRingCat.ofHom (algebraMap ↑R ↑A))) (Spec.map (CommRingCat.ofHom (algebraMap ↑R ↑A))) ⟶
      ((algSpec R).obj (op (CommAlgCat.of ↑R ↑A))).left)
⊢ ((pullbackSpecIso ↑R ↑A ↑A).inv ≫ (pullbackSymmetry (Spec A ↘ Spec R) (Spec A ↘ Spec R)).hom) ≫
      pullback.snd (Spec A ↘ Spec R) (Spec A ↘ Spec R) =
    (Spec.map (Under.Hom.right (↑↑(Bialgebra.TensorProduct.comm ↑R ↑A ↑A)).toUnder) ≫ (pullbackSpecIso ↑R ↑A ↑A).inv) ≫
      pullback.snd (Spec A ↘ Spec R) (Spec A ↘ Spec R)

Tactic:
simp [AlgHom.toUnder, specOverSpec, over, OverClass.hom, h₂]; rfl

Goal state after:
Module: Mathlib.RingTheory.Finiteness.ModuleFinitePresentation

Goal state before:
pp: R : Type u
S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Module.FinitePresentation R S
⊢ FinitePresentation R S

Tactic:
obtain ⟨S', _, _, _, _, _, f, hf⟩ := Module.Finite.exists_free_surjective R S

Goal state after:
R : Type u
S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Module.FinitePresentation R S
S' : Type u
w✝⁴ : CommRing S'
w✝³ : Algebra R S'
w✝² : Module.Finite R S'
w✝¹ : Module.Free R S'
w✝ : FinitePresentation R S'
f : S' →ₐ[R] S
hf : Function.Surjective ⇑f
⊢ FinitePresentation R S
Module: Mathlib.RingTheory.Flat.Rank

Goal state before:
pp: case neg
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Flat R S
inst✝¹ : Module.Finite R S
h : ∀ (p : PrimeSpectrum R), rankAtStalk S p ≤ 1
p : Ideal R
inst✝ : p.IsMaximal
hr : ¬rankAtStalk S { asIdeal := p, isPrime := ⋯ } = 0
⊢ finrank (Localization.AtPrime p) (Localization.AtPrime p ⊗[R] S) = 1

Tactic:
grind [rankAtStalk_eq_finrank_tensorProduct ⟨p, inferInstance⟩]

Goal state after:
Module: Mathlib.RingTheory.Flat.Rank

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝¹³ : CommRing R
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
R' : Type u_5
S' : Type u_6
inst✝¹⁰ : CommRing R'
inst✝⁹ : CommRing S'
inst✝⁸ : Algebra R R'
inst✝⁷ : Algebra S S'
inst✝⁶ : Algebra R' S'
inst✝⁵ : Algebra R S'
inst✝⁴ : IsScalarTower R R' S'
inst✝³ : IsScalarTower R S S'
inst✝² : IsPushout R S R' S'
inst✝¹ : Module.Flat R S
inst✝ : Module.Finite R S
x : PrimeSpectrum R'
this✝ : IsPushout R R' S S'
this : Module.rankAtStalk S' = Module.rankAtStalk (R' ⊗[R] S)
⊢ Module.rankAtStalk S' x = Module.rankAtStalk S (PrimeSpectrum.comap (algebraMap R R') x)

Tactic:
rw [Module.rankAtStalk_eq_of_equiv (Algebra.IsPushout.equiv R R' S S').symm.toLinearEquiv,
    Module.rankAtStalk_baseChange]

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

Goal state before:
pp: case succ.hb
R : Type u_1
inst✝ : CommRing R
x : R
hx : x ∈ nonZeroDivisors R
n : ℕ
ih : ord R (x ^ n) = n • ord R x
⊢ x ∈ nonZeroDivisors R

Tactic:
exact hx

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

Goal state before:
pp: X Y : Scheme
U : X.Opens
f : X ⟶ Y
inst✝ : IsOpenImmersion f
x : ↥X
M : Y.Modules
hxU : x ∈ U
⊢ ((restrictFunctor f).obj M).presheaf.germ U x hxU ≫
      (restrictStalkNatIso f x).hom.app M ≫ (restrictStalkNatIso f x).inv.app M =
    ((restrictFunctor f).obj M).presheaf.germ U x hxU

Tactic:
← NatTrans.comp_app,

Goal state after:
X Y : Scheme
U : X.Opens
f : X ⟶ Y
inst✝ : IsOpenImmersion f
x : ↥X
M : Y.Modules
hxU : x ∈ U
⊢ ((restrictFunctor f).obj M).presheaf.germ U x hxU ≫
      ((restrictStalkNatIso f x).hom ≫ (restrictStalkNatIso f x).inv).app M =
    ((restrictFunctor f).obj M).presheaf.germ U x hxU
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 𝒜
⊢ TopologicalSpace.Opens.IsBasis (Set.range (basicOpen 𝒜))

Tactic:
delta TopologicalSpace.Opens.IsBasis
  convert! ProjectiveSpectrum.isTopologicalBasis_basic_opens 𝒜
  exact (Set.range_comp _ _).symm

Goal state after:
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 𝒜
ι : Type u_2
f : ι → A
hf : (HomogeneousIdeal.irrelevant 𝒜).toIdeal ≤ Ideal.span (Set.range f)
x : ↥(Proj 𝒜)
hx : x ∈ ⊤
H : ∀ (i : ι), f i ∈ x.asHomogeneousIdeal
⊢ Set.range f ⊆ ↑x.asHomogeneousIdeal.toSubmodule

Tactic:
Set.range_subset_iff

Goal state after:
σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
ι : Type u_2
f : ι → A
hf : (HomogeneousIdeal.irrelevant 𝒜).toIdeal ≤ Ideal.span (Set.range f)
x : ↥(Proj 𝒜)
hx : x ∈ ⊤
H : ∀ (i : ι), f i ∈ x.asHomogeneousIdeal
⊢ ∀ (y : ι), f y ∈ ↑x.asHomogeneousIdeal.toSubmodule
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic

Goal state before:
pp: case a
σ : 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 = ⊤
⊢ (Set.range fun x ↦ x.snd.fst) ⊆ ↑(HomogeneousIdeal.irrelevant 𝒜).toIdeal

Tactic:
Set.range_subset_iff

Goal state after:
case a
σ : 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 = ⊤
⊢ ∀ (y : (i : ℕ) ×' (r : A) ×' 0 < i ∧ r ∈ 𝒜 i), y.snd.fst ∈ ↑(HomogeneousIdeal.irrelevant 𝒜).toIdeal
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: case neg
ι : 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)
⊢ 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:
rw [← top_le_iff]

Goal state after:
case neg
ι : 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)
⊢ ⊤ ≤ Submodule.span ↥(𝒜 0) {x | ∃ a ai, ∃ (hai : ∑ i, ai i • dv i = a • d), Away.mk 𝒜 hf a (∏ i, v i ^ ai i) ⋯ = x}
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: A : Type u_2
σ : Type u_3
inst✝⁴ : CommRing A
inst✝³ : SetLike σ A
inst✝² : AddSubgroupClass σ A
𝒜 : ℕ → σ
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)
hxd' : ∀ (i : ι'), 0 < dv i
⊢ Algebra.adjoin ↥(𝒜 0)
      {x |
        ∃ a ai, ∃ (hai : ∑ i, ai i • dv i = a • d) (_ : ∀ (i : ι'), ai i ≤ d), Away.mk 𝒜 hf a (∏ i, v i ^ ai i) ⋯ = x} =
    ⊤

Tactic:
rw [← top_le_iff]

Goal state after:
A : Type u_2
σ : Type u_3
inst✝⁴ : CommRing A
inst✝³ : SetLike σ A
inst✝² : AddSubgroupClass σ A
𝒜 : ℕ → σ
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)
hxd' : ∀ (i : ι'), 0 < dv i
⊢ ⊤ ≤
    Algebra.adjoin ↥(𝒜 0)
      {x |
        ∃ a ai, ∃ (hai : ∑ i, ai i • dv i = a • d) (_ : ∀ (i : ι'), ai i ≤ d), Away.mk 𝒜 hf a (∏ i, v i ^ ai i) ⋯ = x}
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: case inr
R : CommRingCat
M : (Spec (CommRingCat.of ↑R)).Modules
U : (Spec (CommRingCat.of ↑R)).Opens
this :
  ∀ (U : (Spec (CommRingCat.of ↑R)).Opens),
    U = PrimeSpectrum.basicOpen 1 →
      tilde.toOpen ((modulesSpecToSheaf.obj M).presheaf.obj (op ⊤)) U ≫
          (modulesSpecToSheaf.map M.fromTildeΓ).hom.app (op U) =
        (modulesSpecToSheaf.obj M).obj.map (homOfLE ⋯).op
hU : ¬U = PrimeSpectrum.basicOpen 1
⊢ (modulesSpecToSheaf.obj M).obj.map (homOfLE ⋯ ≫ homOfLE ⋯).op = (modulesSpecToSheaf.obj M).obj.map (homOfLE ⋯).op

pp: case inr.hU
R : CommRingCat
M : (Spec (CommRingCat.of ↑R)).Modules
U : (Spec (CommRingCat.of ↑R)).Opens
this :
  ∀ (U : (Spec (CommRingCat.of ↑R)).Opens),
    U = PrimeSpectrum.basicOpen 1 →
      tilde.toOpen ((modulesSpecToSheaf.obj M).presheaf.obj (op ⊤)) U ≫
          (modulesSpecToSheaf.map M.fromTildeΓ).hom.app (op U) =
        (modulesSpecToSheaf.obj M).obj.map (homOfLE ⋯).op
hU : ¬U = PrimeSpectrum.basicOpen 1
⊢ PrimeSpectrum.basicOpen 1 = PrimeSpectrum.basicOpen 1

Tactic:
homOfLE_comp

Goal state after:
case inr
R : CommRingCat
M : (Spec (CommRingCat.of ↑R)).Modules
U : (Spec (CommRingCat.of ↑R)).Opens
this :
  ∀ (U : (Spec (CommRingCat.of ↑R)).Opens),
    U = PrimeSpectrum.basicOpen 1 →
      tilde.toOpen ((modulesSpecToSheaf.obj M).presheaf.obj (op ⊤)) U ≫
          (modulesSpecToSheaf.map M.fromTildeΓ).hom.app (op U) =
        (modulesSpecToSheaf.obj M).obj.map (homOfLE ⋯).op
hU : ¬U = PrimeSpectrum.basicOpen 1
⊢ (modulesSpecToSheaf.obj M).obj.map (homOfLE ⋯).op = (modulesSpecToSheaf.obj M).obj.map (homOfLE ⋯).op

case inr.hU
R : CommRingCat
M : (Spec (CommRingCat.of ↑R)).Modules
U : (Spec (CommRingCat.of ↑R)).Opens
this :
  ∀ (U : (Spec (CommRingCat.of ↑R)).Opens),
    U = PrimeSpectrum.basicOpen 1 →
      tilde.toOpen ((modulesSpecToSheaf.obj M).presheaf.obj (op ⊤)) U ≫
          (modulesSpecToSheaf.map M.fromTildeΓ).hom.app (op U) =
        (modulesSpecToSheaf.obj M).obj.map (homOfLE ⋯).op
hU : ¬U = PrimeSpectrum.basicOpen 1
⊢ PrimeSpectrum.basicOpen 1 = PrimeSpectrum.basicOpen 1
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor

Goal state before:
pp: A B C σ τ ψ : Type u
inst✝¹¹ : CommRing A
inst✝¹⁰ : SetLike σ A
inst✝⁹ : AddSubgroupClass σ A
inst✝⁸ : CommRing B
inst✝⁷ : SetLike τ B
inst✝⁶ : AddSubgroupClass τ B
inst✝⁵ : CommRing C
inst✝⁴ : SetLike ψ C
inst✝³ : AddSubgroupClass ψ C
𝒜 : ℕ → σ
ℬ : ℕ → τ
𝒞 : ℕ → ψ
inst✝² : GradedRing 𝒜
inst✝¹ : GradedRing ℬ
inst✝ : GradedRing 𝒞
f : 𝒜 →+*ᵍ ℬ
g : ℬ →+*ᵍ 𝒞
hf : ℬ₊ ≤ HomogeneousIdeal.map f (𝒜₊)
hg : 𝒞₊ ≤ HomogeneousIdeal.map g (ℬ₊)
i : ℕ
s : A
hs : s ∈ 𝒜 i
⊢ basicOpen ℬ (f s) ≤ map f hf ⁻¹ᵁ basicOpen 𝒜 s

Tactic:
by rfl

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

Goal state before:
pp: case refine_1
A : Type u_2
σ : Type u_3
inst✝⁴ : CommRing A
inst✝³ : SetLike σ A
inst✝² : AddSubgroupClass σ A
𝒜 : ℕ → σ
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)
s : Finset ι' := {x | 0 < dv x}
⊢ Set.range v ⊆ ↑(Algebra.adjoin (↥(𝒜 0)) (Set.range (v ∘ Subtype.val)))

Tactic:
Set.range_subset_iff

Goal state after:
case refine_1
A : Type u_2
σ : Type u_3
inst✝⁴ : CommRing A
inst✝³ : SetLike σ A
inst✝² : AddSubgroupClass σ A
𝒜 : ℕ → σ
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)
s : Finset ι' := {x | 0 < dv x}
⊢ ∀ (y : ι'), v y ∈ ↑(Algebra.adjoin (↥(𝒜 0)) (Set.range (v ∘ Subtype.val)))
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: case refine_2
R : CommRingCat
M : (Spec R).Modules
h : IsLocalizing (modulesSpecToSheaf.obj M)
⊢ IsIso
    (tilde.toOpen ((modulesSpecToSheaf.obj M).presheaf.obj (op ⊤)) ⊤ ≫
      (modulesSpecToSheaf.map M.fromTildeΓ).hom.app (op ⊤))

Tactic:
Scheme.Modules.toOpen_fromTildeΓ_app

Goal state after:
case refine_2
R : CommRingCat
M : (Spec R).Modules
h : IsLocalizing (modulesSpecToSheaf.obj M)
⊢ IsIso ((modulesSpecToSheaf.obj M).obj.map (homOfLE ⋯).op)
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: A : Type u_2
σ : Type u_3
inst✝⁴ : CommRing A
inst✝³ : SetLike σ A
inst✝² : AddSubgroupClass σ A
𝒜 : ℕ → σ
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)
⊢ Algebra.adjoin ↥(𝒜 0)
      {x |
        ∃ a ai, ∃ (hai : ∑ i, ai i • dv i = a • d) (_ : ∀ (i : ι'), ai i ≤ d), Away.mk 𝒜 hf a (∏ i, v i ^ ai i) ⋯ = x} =
    ⊤

Tactic:
let s := Finset.univ.filter (0 < dv ·)
  have := Away.adjoin_mk_prod_pow_eq_top_of_pos hf (ι' := s) (v ∘ Subtype.val) ?_
    (dv ∘ Subtype.val) (fun _ ↦ hxd _) (by simp [s])
  swap
  · rw [← top_le_iff, ← hx, Algebra.adjoin_le_iff, Set.range_subset_iff]
    intro i
    rcases (dv i).eq_zero_or_pos with hi | hi
    · exact algebraMap_mem (R := 𝒜 0) _ ⟨v i, hi ▸ hxd i⟩
    exact Algebra.subset_adjoin ⟨⟨i, by simpa [s] using hi⟩, rfl⟩
  rw [← top_le_iff, ← this]
  apply Algebra.adjoin_mono
  rintro _ ⟨a, ai, hai : ∑ x ∈ s.attach, _ = _, h, rfl⟩
  refine ⟨a, fun i ↦ if hi : i ∈ s then ai ⟨i, hi⟩ else 0, ?_, ?_, ?_⟩
  · simpa [Finset.sum_attach_eq_sum_dite] using hai
  · simp [apply_dite, dite_apply, h]
  · congr 1
    change _ = ∏ x ∈ s.attach, _
    simp [Finset.prod_attach_eq_prod_dite]

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
U : (Opens ↑↑(Spec A⁰_ f).toPresheafedSpace)ᵒᵖ
⊢ (Scheme.ΓSpecIso (CommRingCat.of (A⁰_ f))).inv ≫ (Spec A⁰_ f).presheaf.map (homOfLE ⋯).op ≫ (toSpec 𝒜 f).c.app U =
    CommRingCat.ofHom
        (algebraMap (A⁰_ f)
          ((structureSheafInType ↑(unop (op (CommRingCat.of (A⁰_ f)))) ↑(unop (op (CommRingCat.of (A⁰_ f))))).obj.obj
            U)) ≫
      ((ΓSpec.locallyRingedSpaceAdjunction.homEquiv (Proj.restrict ⋯) (op (CommRingCat.of (A⁰_ f))))
              (awayToΓ 𝒜 f).op).c.app
        U

Tactic:
by rfl

Goal state after:
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
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)
i j : ι
hfgigi : basicOpen (f * (g i * g j)) ≤ basicOpen (f * g i)
hfgigj : basicOpen (f * (g i * g j)) ≤ basicOpen (f * g j)
⊢ f ^ N • (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) s -
      f ^ N • (ConcreteCategory.hom (M.presheaf.map (homOfLE hfgigj ≫ homOfLE ⋯).op)) s =
    0

Tactic:
homOfLE_comp

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
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)
i j : ι
hfgigi : basicOpen (f * (g i * g j)) ≤ basicOpen (f * g i)
hfgigj : basicOpen (f * (g i * g j)) ≤ basicOpen (f * g j)
⊢ f ^ N • (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) s -
      f ^ N • (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) s =
    0
Module: Mathlib.AlgebraicGeometry.ValuativeCriterion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiCompact f
hf : ValuativeCriterion.Existence f
⊢ UniversallyClosed f

Tactic:
by
  rw [eq_valuativeCriterion]
  exact ⟨hf, ‹_›⟩

Goal state after: