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

Goal state before:
pp: K : Type u
inst✝⁴ : Field K
inst✝³ : IsAlgClosed K
G : Over (Spec (CommRingCat.of K))
inst✝² : IsProper G.hom
inst✝¹ : IsIntegral (G ⊗ G).left
inst✝ : GrpObj G
S : Scheme := Spec (CommRingCat.of K)
point : ↥S := IsLocalRing.closedPoint K
hpoint : IsClosed {point}
this✝¹⁰ : Nonempty ↥G.left
this✝⁹ : IsProper (G ⊗ G).hom
this✝⁸ : JacobsonSpace ↥(G ⊗ G).left
this✝⁷ : Surjective G.hom
this✝⁶ : IsProper (Over.Hom.left (fst G G))
this✝⁵ : Surjective (Over.Hom.left (fst G G))
this✝⁴ : IsProper (Over.Hom.left (GrpObj.commutator G) ≫ G.hom)
this✝³ : IsClosedImmersion (Over.Hom.left (lift η η) ≫ Over.Hom.left (fst G G))
this✝² : IsClosedImmersion (Over.Hom.left (lift η η))
γ : G ⊗ G ⟶ G ⊗ G := lift (fst G G) (GrpObj.commutator G)
this✝¹ : IsProper (Over.Hom.left γ ≫ Over.Hom.left (fst G G))
this✝ : IsProper (Over.Hom.left γ)
H✝ : ⇑(Over.Hom.left γ) '' ⇑(Over.Hom.left (fst G G)) ⁻¹' {(Over.Hom.left η) point} ⊆ {(Over.Hom.left (lift η η)) point}
U : G.left.Opens
hηU : (Over.Hom.left η) point ∈ U
H : IsFinite ((Scheme.Hom.imageι (Over.Hom.left γ) ≫ Over.Hom.left (fst G G)) ∣_ U)
x : ↥U
this : ⇑U.ι ⁻¹' {↑x} = {x}
⊢ ⇑(pullback.fst G.hom G.hom) ⁻¹' {↑x} ∩ Set.range ⇑(Over.Hom.left γ) ⊆
    ⇑(pullback.fst G.hom G.hom) ⁻¹' {↑x} ∩ ⇑(pullback.fst G.hom G.hom) ⁻¹' ↑U ∩ closure (Set.range ⇑(Over.Hom.left γ))

Tactic:
← Set.preimage_inter,

Goal state after:
K : Type u
inst✝⁴ : Field K
inst✝³ : IsAlgClosed K
G : Over (Spec (CommRingCat.of K))
inst✝² : IsProper G.hom
inst✝¹ : IsIntegral (G ⊗ G).left
inst✝ : GrpObj G
S : Scheme := Spec (CommRingCat.of K)
point : ↥S := IsLocalRing.closedPoint K
hpoint : IsClosed {point}
this✝¹⁰ : Nonempty ↥G.left
this✝⁹ : IsProper (G ⊗ G).hom
this✝⁸ : JacobsonSpace ↥(G ⊗ G).left
this✝⁷ : Surjective G.hom
this✝⁶ : IsProper (Over.Hom.left (fst G G))
this✝⁵ : Surjective (Over.Hom.left (fst G G))
this✝⁴ : IsProper (Over.Hom.left (GrpObj.commutator G) ≫ G.hom)
this✝³ : IsClosedImmersion (Over.Hom.left (lift η η) ≫ Over.Hom.left (fst G G))
this✝² : IsClosedImmersion (Over.Hom.left (lift η η))
γ : G ⊗ G ⟶ G ⊗ G := lift (fst G G) (GrpObj.commutator G)
this✝¹ : IsProper (Over.Hom.left γ ≫ Over.Hom.left (fst G G))
this✝ : IsProper (Over.Hom.left γ)
H✝ : ⇑(Over.Hom.left γ) '' ⇑(Over.Hom.left (fst G G)) ⁻¹' {(Over.Hom.left η) point} ⊆ {(Over.Hom.left (lift η η)) point}
U : G.left.Opens
hηU : (Over.Hom.left η) point ∈ U
H : IsFinite ((Scheme.Hom.imageι (Over.Hom.left γ) ≫ Over.Hom.left (fst G G)) ∣_ U)
x : ↥U
this : ⇑U.ι ⁻¹' {↑x} = {x}
⊢ ⇑(pullback.fst G.hom G.hom) ⁻¹' {↑x} ∩ Set.range ⇑(Over.Hom.left γ) ⊆
    ⇑(pullback.fst G.hom G.hom) ⁻¹' ({↑x} ∩ ↑U) ∩ closure (Set.range ⇑(Over.Hom.left γ))
Module: Mathlib.AlgebraicGeometry.Group.Abelian

Goal state before:
pp: K : Type u
inst✝³ : Field K
G : Over (Spec (CommRingCat.of K))
inst✝² : IsProper G.hom
inst✝¹ : GeometricallyIntegral G.hom
inst✝ : GrpObj G
f : Spec (CommRingCat.of (AlgebraicClosure K)) ⟶ Spec (CommRingCat.of K) :=
  Spec.map (CommRingCat.ofHom (algebraMap K (AlgebraicClosure K)))
G' : Over (Spec (CommRingCat.of (AlgebraicClosure K))) := (Over.pullback f).obj G
⊢ IsProper G'.hom

Tactic:
dsimp [G']

Goal state after:
K : Type u
inst✝³ : Field K
G : Over (Spec (CommRingCat.of K))
inst✝² : IsProper G.hom
inst✝¹ : GeometricallyIntegral G.hom
inst✝ : GrpObj G
f : Spec (CommRingCat.of (AlgebraicClosure K)) ⟶ Spec (CommRingCat.of K) :=
  Spec.map (CommRingCat.ofHom (algebraMap K (AlgebraicClosure K)))
G' : Over (Spec (CommRingCat.of (AlgebraicClosure K))) := (Over.pullback f).obj G
⊢ IsProper (pullback.snd G.hom f)
Module: Mathlib.AlgebraicGeometry.Group.Abelian

Goal state before:
pp: K : Type u
inst✝³ : Field K
G : Over (Spec (CommRingCat.of K))
inst✝² : IsProper G.hom
inst✝¹ : GeometricallyIntegral G.hom
inst✝ : GrpObj G
f : Spec (CommRingCat.of (AlgebraicClosure K)) ⟶ Spec (CommRingCat.of K) :=
  Spec.map (CommRingCat.ofHom (algebraMap K (AlgebraicClosure K)))
G' : Over (Spec (CommRingCat.of (AlgebraicClosure K))) := (Over.pullback f).obj G
this : IsProper G'.hom
⊢ IsIntegral (G' ⊗ G').left

Tactic:
dsimp [G']

Goal state after:
K : Type u
inst✝³ : Field K
G : Over (Spec (CommRingCat.of K))
inst✝² : IsProper G.hom
inst✝¹ : GeometricallyIntegral G.hom
inst✝ : GrpObj G
f : Spec (CommRingCat.of (AlgebraicClosure K)) ⟶ Spec (CommRingCat.of K) :=
  Spec.map (CommRingCat.ofHom (algebraMap K (AlgebraicClosure K)))
G' : Over (Spec (CommRingCat.of (AlgebraicClosure K))) := (Over.pullback f).obj G
this : IsProper G'.hom
⊢ IsIntegral (pullback (pullback.snd G.hom f) (pullback.snd G.hom f))
Module: Mathlib.RingTheory.Etale.QuasiFinite

Goal state before:
pp: case refine_3
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
R' : Type u
w✝⁶ : CommRing R'
w✝⁵ : Algebra R R'
w✝⁴ : Etale R R'
P : Ideal R'
w✝³ : P.IsPrime
w✝² : P.LiesOver p
e : R' ⊗[R] S
he : IsIdempotentElem e
e₀ : R' ⊗[R] ↥(integralClosure R S)
he₀ : IsIdempotentElem e₀
he₀e : (TensorProduct.map (AlgHom.id R' R') (integralClosure R S).val) e₀ = e
P' : Ideal (R' ⊗[R] S)
w✝¹ : P'.IsPrime
w✝ : 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] ↥(integralClosure R S))),
    P''.IsPrime →
      P''.LiesOver P →
        e₀ ∉ P'' → P'' = Ideal.comap (TensorProduct.map (AlgHom.id R' R') (integralClosure R S).val).toRingHom P'
H : ∀ (P'' : Ideal (R' ⊗[R] S)), P''.IsPrime → P''.LiesOver P → e ∉ P'' → P'' = P'
g : ↥(integralClosure R S)
hgq : ↑g ∉ q
hg : Function.Bijective ⇑(Localization.awayMap (integralClosure R S).val.toRingHom g)
f : R'
hfP : f ∉ P
hf :
  Module.Finite (Localization.Away f)
    (Localization.Away ((TensorProduct.map (ofId R' (Localization.Away f)) (AlgHom.id R S)) e))
Pf : Ideal (Localization.Away f) := Ideal.map (algebraMap R' (Localization.Away f)) P
this✝⁷ : Pf.IsPrime
this✝⁶ : Pf.LiesOver P
φ : R' ⊗[R] S →ₐ[R'] Localization.Away f ⊗[R] S := TensorProduct.map (ofId R' (Localization.Away f)) (AlgHom.id R S)
this✝⁵ : Algebra (R' ⊗[R] S) (Localization.Away f ⊗[R] S) := φ.toAlgebra
this✝⁴ : IsScalarTower R' (R' ⊗[R] S) (Localization.Away f ⊗[R] S) :=
  IsScalarTower.of_algebraMap_eq' (Eq.symm (AlgHom.comp_algebraMap φ))
this✝³ : IsLocalization.Away (f ⊗ₜ[R] 1) (Localization.Away f ⊗[R] S)
P'f : Ideal (Localization.Away f ⊗[R] S) := Ideal.map (algebraMap (R' ⊗[R] S) (Localization.Away f ⊗[R] S)) P'
hP'f : Disjoint ↑(Submonoid.powers (f ⊗ₜ[R] 1)) ↑P'
this✝² : P'f.IsPrime
this✝¹ : P'f.LiesOver P'
this✝ : P'f.LiesOver P
this : P'f.LiesOver Pf
⊢ Function.Bijective ⇑(Ideal.ResidueField.mapₐ P Pf (IsScalarTower.toAlgHom R R' (Localization.Away f)) ⋯)

Tactic:
exact (RingHom.surjectiveOnStalks_of_isLocalization (.powers f)
      _).residueFieldMap_bijective _ _ _

Goal state after:
Module: Mathlib.AlgebraicGeometry.Group.Affine

Goal state before:
pp: R : CommRingCat
⊢ Over.Hom.left (Over.homMk (𝟙 (Spec R)) ⋯) = Over.Hom.left (OplaxMonoidal.η (algSpec R))

Tactic:
rw [Functor.OplaxMonoidal.η_of_cartesianMonoidalCategory, ← preservesTerminalIso_hom,
        preservesTerminalIso_algSpec]; rfl

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d : Adj B
α : a ⟶ b
β β' : b ⟶ c
y : β ⟶ β'
⊢ (conjugateEquiv (α ≫ β').adj (α ≫ β).adj) (α.l ◁ y.τl) = y.τr ▷ α.r

Tactic:
simp [conjugateEquiv_whiskerLeft, Hom₂.conjugateEquiv_τl]

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

Goal state before:
pp: case pos
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
⊢ Function.Surjective ⇑(algebraMap (Localization.AtPrime p) (Localization.AtPrime p ⊗[R] S))

Tactic:
have : Subsingleton (Localization.AtPrime p ⊗[R] S) := by
      apply Module.subsingleton_of_rank_zero (R := Localization.AtPrime p)
      simp [← finrank_eq_rank, ← rankAtStalk_eq_finrank_tensorProduct ⟨p, inferInstance⟩, hr]
    exact Function.surjective_to_subsingleton _

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : IsNoetherianRing R
inst✝³ : KrullDimLE 1 R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : R
hx : x ≠ 0
m : ℕ
hm : ↑m = ord R x
⊢ Multiplicative.ofAdd 0 ≤ Multiplicative.ofAdd ↑m

Tactic:
Multiplicative.ofAdd_le,

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : IsNoetherianRing R
inst✝³ : KrullDimLE 1 R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : R
hx : x ≠ 0
m : ℕ
hm : ↑m = ord R x
⊢ 0 ≤ ↑m
Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDiscreteValuationRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
a : K
⊢ (ordFrac R) a =
    (MonoidWithZero.inverse.comp
        (IsDedekindDomain.HeightOneSpectrum.valuation K (IsDiscreteValuationRing.maximalIdeal R)).toMonoidWithZeroHom)
      a

Tactic:
by_cases ha : a = 0

Goal state after:
case pos
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDiscreteValuationRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
a : K
ha : a = 0
⊢ (ordFrac R) a =
    (MonoidWithZero.inverse.comp
        (IsDedekindDomain.HeightOneSpectrum.valuation K (IsDiscreteValuationRing.maximalIdeal R)).toMonoidWithZeroHom)
      a

case neg
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDiscreteValuationRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
a : K
ha : ¬a = 0
⊢ (ordFrac R) a =
    (MonoidWithZero.inverse.comp
        (IsDedekindDomain.HeightOneSpectrum.valuation K (IsDiscreteValuationRing.maximalIdeal R)).toMonoidWithZeroHom)
      a
Module: Mathlib.AlgebraicGeometry.OrderOfVanishing

Goal state before:
pp: case neg
X : Scheme
inst✝² : IsIntegral X
inst✝¹ : IsLocallyNoetherian X
x : ↥X
U : X.Opens
inst✝ : Nonempty ↥↑U
hxU : x ∈ U
a : ↑Γ(X, U)
ha : a ≠ 0
f : ↑X.functionField
hx : coheight x = 1
hf : ¬f = 0
this : a • f ≠ 0
⊢ (ordHom x hx) f ≤ (ordHom x hx) (a • f)

Tactic:
algebraize [(X.presheaf.germ U x hxU).hom]

Goal state after:
case neg
X : Scheme
inst✝² : IsIntegral X
inst✝¹ : IsLocallyNoetherian X
x : ↥X
U : X.Opens
inst✝ : Nonempty ↥↑U
hxU : x ∈ U
a : ↑Γ(X, U)
ha : a ≠ 0
f : ↑X.functionField
hx : coheight x = 1
hf : ¬f = 0
this : a • f ≠ 0
algInst✝ : Algebra ↑(X.presheaf.obj (Opposite.op U)) ↑(X.presheaf.stalk x) :=
  (CommRingCat.Hom.hom (X.presheaf.germ U x hxU)).toAlgebra
⊢ (ordHom x hx) f ≤ (ordHom x hx) (a • f)
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
c d : B
l₁ l₂ : c ⟶ d
r₁ r₂ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
α : r₁ ⟶ r₂
⊢ (λ_ l₂).inv ≫ (mateEquiv adj₁ adj₂).symm ((ρ_ r₁).hom ≫ α ≫ (λ_ r₂).inv) ≫ (ρ_ l₁).hom =
    (λ_ l₂).inv ≫ adj₁.unit ▷ l₂ ≫ (α_ l₁ r₁ l₂).hom ≫ l₁ ◁ α ▷ l₂ ≫ l₁ ◁ adj₂.counit ≫ (ρ_ l₁).hom

Tactic:
mateEquiv_symm_apply'

Goal state after:
B : Type u
inst✝ : Bicategory B
c d : B
l₁ l₂ : c ⟶ d
r₁ r₂ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
α : r₁ ⟶ r₂
⊢ (λ_ l₂).inv ≫
      (𝟙 (𝟙 c ≫ l₂) ⊗≫
          adj₁.unit ▷ 𝟙 c ▷ l₂ ⊗≫ l₁ ◁ ((ρ_ r₁).hom ≫ α ≫ (λ_ r₂).inv) ▷ l₂ ⊗≫ l₁ ◁ 𝟙 d ◁ adj₂.counit ⊗≫ 𝟙 (l₁ ≫ 𝟙 d)) ≫
        (ρ_ l₁).hom =
    (λ_ l₂).inv ≫ adj₁.unit ▷ l₂ ≫ (α_ l₁ r₁ l₂).hom ≫ l₁ ◁ α ▷ l₂ ≫ l₁ ◁ adj₂.counit ≫ (ρ_ l₁).hom
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
c : B
l r : c ⟶ c
adj : l ⊣ r
α : r ⟶ 𝟙 c
⊢ (λ_ (𝟙 c)).inv ≫ (mateEquiv adj (Adjunction.id c)).symm ((ρ_ r).hom ≫ α ≫ (λ_ (𝟙 c)).inv) ≫ (ρ_ l).hom =
    adj.unit ≫ l ◁ α ≫ (ρ_ l).hom

Tactic:
mateEquiv_symm_apply'

Goal state after:
B : Type u
inst✝ : Bicategory B
c : B
l r : c ⟶ c
adj : l ⊣ r
α : r ⟶ 𝟙 c
⊢ (λ_ (𝟙 c)).inv ≫
      (𝟙 (𝟙 c ≫ 𝟙 c) ⊗≫
          adj.unit ▷ 𝟙 c ▷ 𝟙 c ⊗≫
            l ◁ ((ρ_ r).hom ≫ α ≫ (λ_ (𝟙 c)).inv) ▷ 𝟙 c ⊗≫ l ◁ 𝟙 c ◁ (Adjunction.id c).counit ⊗≫ 𝟙 (l ≫ 𝟙 c)) ≫
        (ρ_ l).hom =
    adj.unit ≫ l ◁ α ≫ (ρ_ l).hom
Module: Mathlib.AlgebraicGeometry.PointsPi

Goal state before:
pp: ι : Type u
R : ι → CommRingCat
X : Scheme
inst✝ : IsAffine X
⊢ Function.Surjective (pointsPi R X)

Tactic:
rintro f

Goal state after:
ι : Type u
R : ι → CommRingCat
X : Scheme
inst✝ : IsAffine X
f : (i : ι) → Spec (R i) ⟶ X
⊢ ∃ a, pointsPi R X a = f
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 𝒜
γ : Sort u_3
t : γ → Set (ProjectiveSpectrum 𝒜)
⊢ (vanishingIdeal (⋃ i, t i)).toIdeal = (⨅ i, vanishingIdeal (t i)).toIdeal

Tactic:
convert! (gc_ideal 𝒜).u_iInf; exact HomogeneousIdeal.toIdeal_iInf _

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 : Set (ProjectiveSpectrum 𝒜)
⊢ vanishingIdeal (closure t) = vanishingIdeal t

Tactic:
have : (vanishingIdeal (zeroLocus 𝒜 (vanishingIdeal t))).toIdeal = _ := (gc_ideal 𝒜).u_l_u_eq_u t

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
t : Set (ProjectiveSpectrum 𝒜)
this : (vanishingIdeal (zeroLocus 𝒜 ↑(vanishingIdeal t))).toIdeal = (vanishingIdeal t).toIdeal
⊢ vanishingIdeal (closure t) = vanishingIdeal t
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic

Goal state before:
pp: case e_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' : ℕ
H : f t = x
h0d : 0 < d
hd : t ∈ 𝒜 d
H' : f t' = x'
h0d' : 0 < d'
hd' : t' ∈ 𝒜 d'
s : A
hts : t * s = t'
n : ℕ
hn : d + n = d'
hs : s ∈ 𝒜 n
hx'x : PrimeSpectrum.basicOpen x' ≤ PrimeSpectrum.basicOpen x
⊢ (Spec Γ(X, ⊤)).homOfLE hx'x ≫
      (basicOpenIsoSpecAway x).hom ≫
        Spec.map (CommRingCat.ofHom (IsLocalization.map (Localization.Away x) f ⋯)) ≫
          Spec.map (CommRingCat.ofHom (algebraMap (Away 𝒜 t) (Localization.Away t))) ≫ awayι 𝒜 t hd h0d =
    (basicOpenIsoSpecAway x').hom ≫
      Spec.map (CommRingCat.ofHom (IsLocalization.map (Localization.Away x') f ⋯)) ≫
        Spec.map (CommRingCat.ofHom (algebraMap (Away 𝒜 t') (Localization.Away t'))) ≫ awayι 𝒜 t' hd' h0d'

Tactic:
simp only [← Iso.inv_comp_eq]

Goal state after:
case e_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' : ℕ
H : f t = x
h0d : 0 < d
hd : t ∈ 𝒜 d
H' : f t' = x'
h0d' : 0 < d'
hd' : t' ∈ 𝒜 d'
s : A
hts : t * s = t'
n : ℕ
hn : d + n = d'
hs : s ∈ 𝒜 n
hx'x : PrimeSpectrum.basicOpen x' ≤ PrimeSpectrum.basicOpen x
⊢ (basicOpenIsoSpecAway x').inv ≫
      (Spec Γ(X, ⊤)).homOfLE hx'x ≫
        (basicOpenIsoSpecAway x).hom ≫
          Spec.map (CommRingCat.ofHom (IsLocalization.map (Localization.Away x) f ⋯)) ≫
            Spec.map (CommRingCat.ofHom (algebraMap (Away 𝒜 t) (Localization.Away t))) ≫ awayι 𝒜 t hd h0d =
    Spec.map (CommRingCat.ofHom (IsLocalization.map (Localization.Away x') f ⋯)) ≫
      Spec.map (CommRingCat.ofHom (algebraMap (Away 𝒜 t') (Localization.Away t'))) ≫ awayι 𝒜 t' hd' h0d'
Module: Mathlib.RingTheory.LocalRing.LocalSubring

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
K : Type u_3
inst✝¹ : Field K
A : Subring K
P : Ideal ↥A
inst✝ : P.IsPrime
x : ↥A
s : ↥P.primeCompl
y : ↥A
t : ↥P.primeCompl
e :
  (IsLocalization.liftAlgHom ⋯) (IsLocalization.mk' (Localization.AtPrime P) x s) =
    (IsLocalization.liftAlgHom ⋯) (IsLocalization.mk' (Localization.AtPrime P) y t)
⊢ IsLocalization.mk' (Localization.AtPrime P) x s = IsLocalization.mk' (Localization.AtPrime P) y t

Tactic:
have H : ∀ x : P.primeCompl, x.1 ≠ 0 := by rintro ⟨x, hx⟩ rfl; aesop

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
K : Type u_3
inst✝¹ : Field K
A : Subring K
P : Ideal ↥A
inst✝ : P.IsPrime
x : ↥A
s : ↥P.primeCompl
y : ↥A
t : ↥P.primeCompl
e :
  (IsLocalization.liftAlgHom ⋯) (IsLocalization.mk' (Localization.AtPrime P) x s) =
    (IsLocalization.liftAlgHom ⋯) (IsLocalization.mk' (Localization.AtPrime P) y t)
H : ∀ (x : ↥P.primeCompl), ↑x ≠ 0
⊢ IsLocalization.mk' (Localization.AtPrime P) x s = IsLocalization.mk' (Localization.AtPrime P) y t
Module: Mathlib.RingTheory.Valuation.LocalSubring

Goal state before:
pp: K : Type u_3
inst✝ : Field K
R : LocalSubring K
hR : IsMax R
x : K
hx : x ∉ R.toSubring
hx0 : x ≠ 0
this✝ : Invertible x := invertibleOfNonzero hx0
S : Subalgebra (↥R.toSubring) K := (↥R.toSubring)[x]
this : R.toSubring < S.toSubring
p : Polynomial ↥R.toSubring
hp : p.leadingCoeff - 1 ∈ maximalIdeal ↥R.toSubring
hpx : (Polynomial.aeval ⅟x) p = 0
⊢ IsIntegral (↥R.toSubring) x⁻¹

Tactic:
have H : IsUnit p.leadingCoeff := of_not_not fun h ↦ by simpa using sub_mem h hp

Goal state after:
K : Type u_3
inst✝ : Field K
R : LocalSubring K
hR : IsMax R
x : K
hx : x ∉ R.toSubring
hx0 : x ≠ 0
this✝ : Invertible x := invertibleOfNonzero hx0
S : Subalgebra (↥R.toSubring) K := (↥R.toSubring)[x]
this : R.toSubring < S.toSubring
p : Polynomial ↥R.toSubring
hp : p.leadingCoeff - 1 ∈ maximalIdeal ↥R.toSubring
hpx : (Polynomial.aeval ⅟x) p = 0
H : IsUnit p.leadingCoeff
⊢ IsIntegral (↥R.toSubring) x⁻¹
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
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
x : ↑↑(Spec A⁰_ f).toPresheafedSpace
z : ↑(CommRingCat.of (A⁰_ f))
⊢ z ∈ ((ConcreteCategory.hom (toSpec 𝒜 f)) (FromSpec.toFun f_deg hm x)).asIdeal ↔ z ∈ x.asIdeal

Tactic:
obtain ⟨z, rfl⟩ := HomogeneousLocalization.mk_surjective z

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
x : ↑↑(Spec A⁰_ f).toPresheafedSpace
z : HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f)
⊢ HomogeneousLocalization.mk z ∈ ((ConcreteCategory.hom (toSpec 𝒜 f)) (FromSpec.toFun f_deg hm x)).asIdeal ↔
    HomogeneousLocalization.mk z ∈ x.asIdeal
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme

Goal state before:
pp: case exists_of_eq
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
this : Algebra (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal) := (mapId 𝒜 ⋯).toAlgebra
z : A⁰_ f
y : NumDenSameDeg 𝒜 (Submonoid.powers f)
e :
  (algebraMap (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal)) (HomogeneousLocalization.mk y) =
    (algebraMap (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal)) z
⊢ ∃ c, ↑c * HomogeneousLocalization.mk y = ↑c * z

Tactic:
obtain ⟨z, rfl⟩ := HomogeneousLocalization.mk_surjective z

Goal state after:
case exists_of_eq
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
this : Algebra (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal) := (mapId 𝒜 ⋯).toAlgebra
y z : NumDenSameDeg 𝒜 (Submonoid.powers f)
e :
  (algebraMap (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal)) (HomogeneousLocalization.mk y) =
    (algebraMap (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal)) (HomogeneousLocalization.mk z)
⊢ ∃ c, ↑c * HomogeneousLocalization.mk y = ↑c * HomogeneousLocalization.mk z
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 𝒜
d e : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : 0 < d
n : ℕ
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun x_1 ↦ x ^ x_1) j ∈ 𝒜 n
hfg : ¬(f * g) ^ j = 0
this : n = j * (d + e)
⊢ a * g ^ (j * (d - 1)) ∈ 𝒜 (j * (d * (e + 1)))

Tactic:
convert SetLike.mul_mem_graded ha (SetLike.pow_mem_graded _ hg)

Goal state after:
case e'_4
σ : Type u_1
A : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
d e : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : 0 < d
n : ℕ
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun x_1 ↦ x ^ x_1) j ∈ 𝒜 n
hfg : ¬(f * g) ^ j = 0
this : n = j * (d + e)
⊢ j * (d * (e + 1)) = n + (j * (d - 1)) • e
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
⊢ IsProper f

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

Goal state after:
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
inst✝¹ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
X : C
X₀ : C₀
f : F.obj X₀ ⟶ X
Y₀ : C₀
g : Y₀ ⟶ X₀
i : (data X).I₀
p : F.obj Y₀ ⟶ F.obj ((data X).X i)
fac : p ≫ (data X).f i = F.map g ≫ f
hg : ((data X).sieve f).arrows g
⊢ ⋯.amalgamate ⟨(data X).sieve f, ⋯⟩ (fun x ↦ restriction.res data G₀ (Nonempty.some ⋯)) ⋯ ≫ G₀.obj.map g.op =
    presheafObjπ data G₀ X i ≫ IsDenseSubsite.mapPreimage J F G₀ p

Tactic:
rw [G₀.2.amalgamate_map _ _ _ ⟨_, g, hg⟩]

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
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
X : C
X₀ : C₀
f : F.obj X₀ ⟶ X
Y₀ : C₀
g : Y₀ ⟶ X₀
i : (data X).I₀
p : F.obj Y₀ ⟶ F.obj ((data X).X i)
fac : p ≫ (data X).f i = F.map g ≫ f
hg : ((data X).sieve f).arrows g
⊢ restriction.res data G₀ (Nonempty.some ⋯) = presheafObjπ data G₀ X i ≫ IsDenseSubsite.mapPreimage J F G₀ p
Module: Mathlib.AlgebraicGeometry.Sites.Fpqc

Goal state before:
pp: X : Scheme
⊢ Presieve.IsSheaf fpqcTopology (yoneda.obj X)

Tactic:
rw [fpqcTopology_eq_propQCTopology, isSheaf_type_propQCTopology_iff]

Goal state after:
X : Scheme
⊢ Presieve.IsSheaf zariskiTopology (yoneda.obj X) ∧
    ∀ {R S : CommRingCat} (f : R ⟶ S),
      Flat (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor (yoneda.obj X) (Presieve.singleton (Spec.map f))