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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝²⁸ : CommRing R
inst✝²⁷ : CommRing S
inst✝²⁶ : Algebra R S
K : Type u_4
L : Type u_5
inst✝²⁵ : Field K
inst✝²⁴ : Field L
inst✝²³ : Algebra R K
inst✝²² : Algebra R L
inst✝²¹ : Algebra S L
inst✝²⁰ : Algebra K L
inst✝¹⁹ : IsScalarTower R K L
inst✝¹⁸ : IsScalarTower R S L
inst✝¹⁷ : IsFractionRing R K
inst✝¹⁶ : IsFractionRing S L
R' : Type u_6
S' : Type u_7
inst✝¹⁵ : CommRing R'
inst✝¹⁴ : CommRing S'
inst✝¹³ : Algebra R R'
inst✝¹² : Algebra R' S'
inst✝¹¹ : Algebra R S'
inst✝¹⁰ : Algebra S' L
inst✝⁹ : Algebra R' L
inst✝⁸ : IsScalarTower R' S' L
inst✝⁷ : Algebra R' K
inst✝⁶ : IsScalarTower R' K L
inst✝⁵ : IsScalarTower R R' S'
inst✝⁴ : FaithfulSMul S' L
inst✝³ : IsIntegralClosure R' R K
inst✝² : IsScalarTower R R' K
f : S →ₐ[R] S'
hf₁ : Function.Surjective ⇑(TensorProduct.lift (ofId R' S') f ⋯)
hf₂ : (algebraMap S' L).comp f.toRingHom = algebraMap S L
x : S
hx' : (aeval x).Finite
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : WeaklyQuasiFiniteAt R P
hx : IsStronglyTranscendental R x
this✝⁷ : IsDomain S'
this✝⁶ : IsDomain R
this✝⁵ : Algebra.IsIntegral R R'
this✝⁴ : FaithfulSMul R' K
this✝³ : FaithfulSMul R R'
this✝² : FaithfulSMul R' L
this✝¹ : FaithfulSMul R' S'
this✝ : IsIntegrallyClosedIn R' K
this : IsIntegrallyClosed R'
g : R' ⊗[R] S →ₐ[R'] S' := TensorProduct.lift (ofId R' S') f ⋯
hf₃ : Function.Injective ⇑f
hf₄ : f.IsIntegral
H₁ : IsStronglyTranscendental R' (f x)
H₂ : (aeval (f x)).Finite
Q : Ideal S'
isPrime✝ : Q.IsPrime
hQ : PrimeSpectrum.comap f.toRingHom { asIdeal := Q, isPrime := isPrime✝ } = { asIdeal := P, isPrime := inst✝¹ }
⊢ P = Ideal.comap TensorProduct.includeRight.toRingHom (Ideal.comap g.toRingHom Q)

Tactic:
rw [Ideal.comap_comap]
    convert! congr(($hQ.symm).1)
    ext; simp [g]

Goal state after:
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: case inr
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal S
inst✝¹ : p.IsPrime
inst✝ : WeaklyQuasiFiniteAt R p
x : S
hx : R[x] = ⊤
this :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal S) [inst_3 : p.IsPrime]
    [WeaklyQuasiFiniteAt R p] (x : S), R[x] = ⊤ → integralClosure R S = ⊥ → ZariskisMainProperty R p
H : ¬integralClosure R S = ⊥
⊢ ZariskisMainProperty R p

Tactic:
let inst : Algebra (integralClosure R S) (Localization.AtPrime p) :=
      OreLocalization.instAlgebra
    have inst : Algebra.WeaklyQuasiFiniteAt (integralClosure R S) p :=
      .of_restrictScalars R (integralClosure R S) _
    refine .restrictScalars (this p x ?_ (integralClosure_idem (R := R)))
    suffices ⊤ ≤ (Algebra.adjoin (integralClosure R S) {x}).restrictScalars R from
      top_le_iff.mp fun x _ ↦ (Subalgebra.mem_restrictScalars _).mp (this trivial)
    refine hx.ge.trans ?_
    rw [Algebra.restrictScalars_adjoin]
    exact Algebra.adjoin_mono (by simp)

Goal state after:
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
U V : Y.AffineZariskiSite
i : U ⟶ V
this :
  (pullbackRestrictIsoRestrict f ↑U).inv ≫
      Cover.trans (Precoverage.ZeroHypercover.pullback₁ f (directedCover Y)) i ≫
        (pullbackRestrictIsoRestrict f ↑V).hom =
    X.homOfLE ⋯
⊢ (f ⁻¹ᵁ U.toOpens).toSpecΓ ≫
      Spec.map (CommRingCat.ofHom ↑(integralClosure ↑Γ(Y, ↑V) ↑Γ(X, f ⁻¹ᵁ ↑V)).val ≫ X.presheaf.map (homOfLE ⋯).op) ≫
        colimit.ι (normalizationGlueData f).functor V =
    (f ⁻¹ᵁ ↑U).toSpecΓ ≫
      Spec.map (CommRingCat.ofHom ↑(integralClosure ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U)).val) ≫
        colimit.ι (normalizationGlueData f).functor U

Tactic:
rw [← colimit.w f.normalizationGlueData.functor i]

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
U V : Y.AffineZariskiSite
i : U ⟶ V
this :
  (pullbackRestrictIsoRestrict f ↑U).inv ≫
      Cover.trans (Precoverage.ZeroHypercover.pullback₁ f (directedCover Y)) i ≫
        (pullbackRestrictIsoRestrict f ↑V).hom =
    X.homOfLE ⋯
⊢ (f ⁻¹ᵁ U.toOpens).toSpecΓ ≫
      Spec.map (CommRingCat.ofHom ↑(integralClosure ↑Γ(Y, ↑V) ↑Γ(X, f ⁻¹ᵁ ↑V)).val ≫ X.presheaf.map (homOfLE ⋯).op) ≫
        colimit.ι (normalizationGlueData f).functor V =
    (f ⁻¹ᵁ ↑U).toSpecΓ ≫
      Spec.map (CommRingCat.ofHom ↑(integralClosure ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U)).val) ≫
        (normalizationGlueData f).functor.map i ≫ colimit.ι (normalizationGlueData f).functor V
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: case refine_2
n : ℕ
IH :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal S) [inst_3 : p.IsPrime]
    [WeaklyQuasiFiniteAt R p] (f : MvPolynomial (Fin n) R →ₐ[R] S), f.Finite → ZariskisMainProperty R p
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal S
inst✝¹ : p.IsPrime
inst✝ : WeaklyQuasiFiniteAt R p
f : MvPolynomial (Fin (n + 1)) R →ₐ[R] S
hf : f.Finite
f' : (MvPolynomial (Fin n) R)[X] →ₐ[R] S := f.comp ↑(MvPolynomial.finSuccEquiv R n).symm
this✝³ : Algebra (MvPolynomial (Fin n) R) S := (f'.comp C).toAlgebra
this✝² : IsScalarTower R (MvPolynomial (Fin n) R) S
f'' : (MvPolynomial (Fin n) R)[X] →ₐ[MvPolynomial (Fin n) R] S := { toRingHom := f'.toRingHom, commutes' := ⋯ }
this✝¹ : WeaklyQuasiFiniteAt (MvPolynomial (Fin n) R) p
this✝ : ZariskisMainProperty (MvPolynomial (Fin n) R) p
r : S
hrp : r ∉ p
hr : IsIntegral (MvPolynomial (Fin n) R) r
m : S → ℕ
hm : ∀ (x : S), IsIntegral (MvPolynomial (Fin n) R) (r ^ m x * x)
s : Finset S
hs : adjoin R ↑s = ⊤
R' : Subalgebra R S := adjoin R ↑(Finset.image (⇑f ∘ MvPolynomial.X ∘ Fin.succ) Finset.univ ∪ r ^ s.sup m • s ∪ {r})
hrR' : r ∈ R'
this : WeaklyQuasiFiniteAt R (Ideal.under (↥R') p)
φ : MvPolynomial (Fin n) R →ₐ[R] ↥R' := MvPolynomial.aeval fun i ↦ ⟨f (MvPolynomial.X i.succ), ⋯⟩
⊢ φ.FiniteType

Tactic:
refine .of_comp_finiteType (f := algebraMap R _) ?_

Goal state after:
case refine_2
n : ℕ
IH :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal S) [inst_3 : p.IsPrime]
    [WeaklyQuasiFiniteAt R p] (f : MvPolynomial (Fin n) R →ₐ[R] S), f.Finite → ZariskisMainProperty R p
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal S
inst✝¹ : p.IsPrime
inst✝ : WeaklyQuasiFiniteAt R p
f : MvPolynomial (Fin (n + 1)) R →ₐ[R] S
hf : f.Finite
f' : (MvPolynomial (Fin n) R)[X] →ₐ[R] S := f.comp ↑(MvPolynomial.finSuccEquiv R n).symm
this✝³ : Algebra (MvPolynomial (Fin n) R) S := (f'.comp C).toAlgebra
this✝² : IsScalarTower R (MvPolynomial (Fin n) R) S
f'' : (MvPolynomial (Fin n) R)[X] →ₐ[MvPolynomial (Fin n) R] S := { toRingHom := f'.toRingHom, commutes' := ⋯ }
this✝¹ : WeaklyQuasiFiniteAt (MvPolynomial (Fin n) R) p
this✝ : ZariskisMainProperty (MvPolynomial (Fin n) R) p
r : S
hrp : r ∉ p
hr : IsIntegral (MvPolynomial (Fin n) R) r
m : S → ℕ
hm : ∀ (x : S), IsIntegral (MvPolynomial (Fin n) R) (r ^ m x * x)
s : Finset S
hs : adjoin R ↑s = ⊤
R' : Subalgebra R S := adjoin R ↑(Finset.image (⇑f ∘ MvPolynomial.X ∘ Fin.succ) Finset.univ ∪ r ^ s.sup m • s ∪ {r})
hrR' : r ∈ R'
this : WeaklyQuasiFiniteAt R (Ideal.under (↥R') p)
φ : MvPolynomial (Fin n) R →ₐ[R] ↥R' := MvPolynomial.aeval fun i ↦ ⟨f (MvPolynomial.X i.succ), ⋯⟩
⊢ (φ.comp (algebraMap R (MvPolynomial (Fin n) R))).FiniteType
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n k : ℕ
⊢ (freeMonic R n).coeff k = if h : k < n then MvPolynomial.X ⟨k, h⟩ else if k = n then 1 else 0

Tactic:
simp only [freeMonic, Polynomial.coeff_add, Polynomial.coeff_X_pow, Polynomial.finsetSum_coeff,
    Polynomial.coeff_C_mul, mul_ite, mul_one, mul_zero]

Goal state after:
R : Type u_1
inst✝ : CommRing R
n k : ℕ
⊢ ((if k = n then 1 else 0) + ∑ x, if k = ↑x then MvPolynomial.X x else 0) =
    if h : k < n then MvPolynomial.X ⟨k, h⟩ else if k = n then 1 else 0
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: case inr.h₀
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
i : Fin m
j : Fin n
h : ↑i ≤ ↑j
⊢ ∀ b ∈ Finset.antidiagonal ↑j,
    b ≠ (↑i, ↑j - ↑i) →
      (if h : b.2 < k then if b.1 < m ∧ b.1 = ↑i then X (Sum.inr ⟨b.2, h⟩) else 0
        else if b.2 = k ∧ b.1 < m ∧ b.1 = ↑i then 1 else 0) =
        0

Tactic:
simp only [Finset.mem_antidiagonal, ne_eq, Prod.forall, Prod.mk.injEq, not_and]
      intro a b e h
      simp [show a ≠ i by lia]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case pos
R✝ : Type u_1
inst✝¹ : CommRing R✝
R : Type u_1
inst✝ : Field R
f : R[X]
hf' : f.Splits
g : R[X]
r : R
hf : f ≠ 0
hg : g ≠ 0
hf0 : ¬f.natDegree = 0
hg0 : g.natDegree = 0
⊢ (f.scaleRoots r).resultant (g.scaleRoots r) f.natDegree g.natDegree = r ^ (f.natDegree * g.natDegree) * f.resultant g

Tactic:
obtain ⟨a, rfl⟩ := natDegree_eq_zero.mp hg0

Goal state after:
case pos
R✝ : Type u_1
inst✝¹ : CommRing R✝
R : Type u_1
inst✝ : Field R
f : R[X]
hf' : f.Splits
r : R
hf : f ≠ 0
hf0 : ¬f.natDegree = 0
a : R
hg : C a ≠ 0
hg0 : (C a).natDegree = 0
⊢ (f.scaleRoots r).resultant ((C a).scaleRoots r) f.natDegree (C a).natDegree =
    r ^ (f.natDegree * (C a).natDegree) * f.resultant (C a)
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case Splits.mul
R✝ : Type u_1
inst✝¹ : CommRing R✝
R : Type u_1
inst✝ : Field R
f : R[X]
g : R[X]
r : R
x y : R[X]
hx : x ∈ Submonoid.closure ({x | ∃ a, C a = x} ∪ {x | ∃ a, X + C a = x})
hy : y ∈ Submonoid.closure ({x | ∃ a, C a = x} ∪ {x | ∃ a, X + C a = x})
hx' : ((taylor r) x).resultant ((taylor r) g) = x.resultant g
hy' : ((taylor r) y).resultant ((taylor r) g) = y.resultant g
⊢ ((taylor r) (x * y)).resultant ((taylor r) g) = (x * y).resultant g

Tactic:
| mul x y hx hy hx' hy' =>

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
r : R
⊢ (C r).discr = 1

Tactic:
let e : Fin ((C r).natDegree - 1 + (C r).natDegree) ≃ Fin 0 := finCongr (by simp)
  simp [discr, ← Matrix.det_reindex_self e]

Goal state after:
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
⊢ IsCommMonObj G

Tactic:
have : JacobsonSpace (G ⊗ G).left := LocallyOfFiniteType.jacobsonSpace (Y := Spec _) (G ⊗ G).hom

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
⊢ IsCommMonObj G
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
X₁ X₂ : CommGrp C
ψ : X₁ ⟶ X₂
Y : (Grp C)ᵒᵖ
f g : unop Y ⟶ X₁.toGrp
⊢ ((f * g) ≫ ψ.hom).hom.hom = (f ≫ ψ.hom * g ≫ ψ.hom).hom.hom

Tactic:
simpa using ((yonedaGrp.map ψ.hom).app (op (unop Y).X)).hom.map_mul f.hom.hom g.hom.hom

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

Goal state before:
pp: R S T : Type u_1
x✝⁴ : CommRing R
x✝³ : CommRing S
x✝² : CommRing T
x✝¹ : Algebra R S
x✝ : Algebra R T
h : (algebraMap R S).FaithfullyFlat
h' : (algebraMap S (S ⊗[R] T)).Etale
⊢ (algebraMap R T).Etale

Tactic:
rw [etale_algebraMap] at h' ⊢

Goal state after:
R S T : Type u_1
x✝⁴ : CommRing R
x✝³ : CommRing S
x✝² : CommRing T
x✝¹ : Algebra R S
x✝ : Algebra R T
h : (algebraMap R S).FaithfullyFlat
h' : Algebra.Etale S (S ⊗[R] T)
⊢ Algebra.Etale R T
Module: Mathlib.RingTheory.Extension.Cotangent.BaseChange

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Module.Flat R T
t : T
x : H1Cotangent R S
⊢ t •
      (Extension.H1Cotangent.map
          ((((Generators.baseChange T (Generators.self R S)).defaultHom
                      (Generators.self T (T ⊗[R] S))).toExtensionHom.comp
                ((Generators.self R S).baseChangeFromBaseChange T)).comp
            (Extension.toBaseChange T)))
        x =
    t • (H1Cotangent.map R T S (T ⊗[R] S)) x

Tactic:
H1Cotangent.map,

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Module.Flat R T
t : T
x : H1Cotangent R S
⊢ t •
      (Extension.H1Cotangent.map
          ((((Generators.baseChange T (Generators.self R S)).defaultHom
                      (Generators.self T (T ⊗[R] S))).toExtensionHom.comp
                ((Generators.self R S).baseChangeFromBaseChange T)).comp
            (Extension.toBaseChange T)))
        x =
    t • (Extension.H1Cotangent.map ((Generators.self R S).defaultHom (Generators.self T (T ⊗[R] S))).toExtensionHom) x
Module: Mathlib.RingTheory.OrderOfVanishing.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsPrincipalIdealRing R
ϖ : R
hϖ : Irreducible ϖ
this : (span {ϖ}).IsMaximal
⊢ IsSimpleModule (R ⧸ span {ϖ}) (R ⧸ span {ϖ})

Tactic:
let := Ideal.Quotient.field (Ideal.span {ϖ})

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsPrincipalIdealRing R
ϖ : R
hϖ : Irreducible ϖ
this✝ : (span {ϖ}).IsMaximal
this : Field (R ⧸ span {ϖ}) := Quotient.field (span {ϖ})
⊢ IsSimpleModule (R ⧸ span {ϖ}) (R ⧸ span {ϖ})
Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian

Goal state before:
pp: R : Type u_2
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : KrullDimLE 1 R
inst✝ : Nontrivial R
x : ↥R⁰
⊢ ↑(Multiplicative.ofAdd ↑(ord R ↑x).toNat) = ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) (ord R ↑x)

Tactic:
← ENat.natCast_lift (ord R x.1) (ord_lt_top x.2),

Goal state after:
R : Type u_2
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : KrullDimLE 1 R
inst✝ : Nontrivial R
x : ↥R⁰
⊢ ↑(Multiplicative.ofAdd ↑(↑((ord R ↑x).lift ⋯)).toNat) =
    ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) ↑((ord R ↑x).lift ⋯)
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
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)

Tactic:
have : Ring.KrullDimLE 1 ↑(X.presheaf.stalk x) := krullDimLE_of_coheight_le hx.le

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
this : Ring.KrullDimLE 1 ↑(X.presheaf.stalk x)
⊢ (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
a b c d e f x y z : B
g₁ : a ⟶ d
h₁ : b ⟶ e
k₁ : c ⟶ f
g₂ : d ⟶ x
h₂ : e ⟶ y
k₂ : f ⟶ z
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : b ⟶ c
r₂ : c ⟶ b
l₃ : d ⟶ e
r₃ : e ⟶ d
l₄ : e ⟶ f
r₄ : f ⟶ e
l₅ : x ⟶ y
r₅ : y ⟶ x
l₆ : y ⟶ z
r₆ : z ⟶ y
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
adj₄ : l₄ ⊣ r₄
adj₅ : l₅ ⊣ r₅
adj₆ : l₆ ⊣ r₆
α : g₁ ≫ l₃ ⟶ l₁ ≫ h₁
β : h₁ ≫ l₄ ⟶ l₂ ≫ k₁
γ : g₂ ≫ l₅ ⟶ l₃ ≫ h₂
δ : h₂ ≫ l₆ ⟶ l₄ ≫ k₂
⊢ (mateEquiv (adj₁.comp adj₂) (adj₅.comp adj₆)) (leftAdjointSquare.comp α β γ δ) =
    rightAdjointSquare.comp ((mateEquiv adj₁ adj₃) α) ((mateEquiv adj₂ adj₄) β) ((mateEquiv adj₃ adj₅) γ)
      ((mateEquiv adj₄ adj₆) δ)

Tactic:
by
  have vcomp :=
    mateEquiv_vcomp (adj₁.comp adj₂) (adj₃.comp adj₄) (adj₅.comp adj₆)
      (leftAdjointSquare.hcomp α β) (leftAdjointSquare.hcomp γ δ)
  have hcomp1 := mateEquiv_hcomp adj₁ adj₃ adj₂ adj₄ α β
  have hcomp2 := mateEquiv_hcomp adj₃ adj₅ adj₄ adj₆ γ δ
  rw [hcomp1, hcomp2] at vcomp
  exact vcomp

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
inst✝³ : AddSubgroupClass σ A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
x : Submonoid A
c1 c2 : NumDenSameDeg 𝒜 x
h : Localization.mk ↑c1.num ⟨↑c1.den, ⋯⟩ = Localization.mk ↑c2.num ⟨↑c2.den, ⋯⟩
c3 c4 : NumDenSameDeg 𝒜 x
h' : Localization.mk ↑c3.num ⟨↑c3.den, ⋯⟩ = Localization.mk ↑c4.num ⟨↑c4.den, ⋯⟩
⊢ Localization.mk (↑c1.num * ↑c3.num) ⟨↑c1.den * ↑c3.den, ⋯⟩ =
    Localization.mk (↑c2.num * ↑c4.num) ⟨↑c2.den * ↑c4.den, ⋯⟩

Tactic:
convert! congr_arg₂ (· * ·) h h' <;> rw [Localization.mk_mul]

Goal state after:
case e'_2
ι : 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 𝒜
x : Submonoid A
c1 c2 : NumDenSameDeg 𝒜 x
h : Localization.mk ↑c1.num ⟨↑c1.den, ⋯⟩ = Localization.mk ↑c2.num ⟨↑c2.den, ⋯⟩
c3 c4 : NumDenSameDeg 𝒜 x
h' : Localization.mk ↑c3.num ⟨↑c3.den, ⋯⟩ = Localization.mk ↑c4.num ⟨↑c4.den, ⋯⟩
⊢ Localization.mk (↑c1.num * ↑c3.num) ⟨↑c1.den * ↑c3.den, ⋯⟩ =
    Localization.mk (↑c1.num * ↑c3.num) (⟨↑c1.den, ⋯⟩ * ⟨↑c3.den, ⋯⟩)

case e'_3
ι : 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 𝒜
x : Submonoid A
c1 c2 : NumDenSameDeg 𝒜 x
h : Localization.mk ↑c1.num ⟨↑c1.den, ⋯⟩ = Localization.mk ↑c2.num ⟨↑c2.den, ⋯⟩
c3 c4 : NumDenSameDeg 𝒜 x
h' : Localization.mk ↑c3.num ⟨↑c3.den, ⋯⟩ = Localization.mk ↑c4.num ⟨↑c4.den, ⋯⟩
⊢ Localization.mk (↑c2.num * ↑c4.num) ⟨↑c2.den * ↑c4.den, ⋯⟩ =
    Localization.mk (↑c2.num * ↑c4.num) (⟨↑c2.den, ⋯⟩ * ⟨↑c4.den, ⋯⟩)
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
inst✝³ : AddSubgroupClass σ A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
f g x : A
hx : x = f * g
n : ι
a : ↥(𝒜 n)
i : ℕ
hi : f ^ i ∈ 𝒜 n
this : (algebraMap A (Localization.Away x)) f * Localization.mk g ⟨f * g, ⋯⟩ = 1
⊢ ↑a • Localization.mk g ⟨f * g, ⋯⟩ ^ i = Localization.mk (↑a * g ^ i) ⟨x ^ i, ⋯⟩

Tactic:
Localization.mk_pow,

Goal state after:
ι : 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 g x : A
hx : x = f * g
n : ι
a : ↥(𝒜 n)
i : ℕ
hi : f ^ i ∈ 𝒜 n
this : (algebraMap A (Localization.Away x)) f * Localization.mk g ⟨f * g, ⋯⟩ = 1
⊢ ↑a • Localization.mk (g ^ i) (⟨f * g, ⋯⟩ ^ i) = Localization.mk (↑a * g ^ i) ⟨x ^ i, ⋯⟩
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic

Goal state before:
pp: case convert_4.mul
σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
ι : Type u_2
f : ι → A
hfn : ∀ (i : ι), ∃ n, f i ∈ 𝒜 n
hf : Algebra.adjoin (↥(𝒜 0)) (Set.range f) = ⊤
x✝ x y : A
hx : x ∈ Algebra.adjoin (↥(𝒜 0)) (Set.range f)
hy : y ∈ Algebra.adjoin (↥(𝒜 0)) (Set.range f)
hx' : x - (GradedRing.projZeroRingHom 𝒜) x ∈ Ideal.span (Set.range f)
hy' : y - (GradedRing.projZeroRingHom 𝒜) y ∈ Ideal.span (Set.range f)
⊢ x * y - (GradedRing.projZeroRingHom 𝒜) (x * y) ∈ Ideal.span (Set.range f)

Tactic:
| mul x y hx hy hx' hy' =>

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 𝒜
f g✝ : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
hm' : 0 < m'
x : A
hx : x = f * g
⊢ (Scheme.Hom.opensRange (awayι 𝒜 f f_deg hm) ⊓ Scheme.Hom.opensRange (awayι 𝒜 g g_deg hm')).carrier =
    (Scheme.Hom.opensRange (awayι 𝒜 x ⋯ ⋯)).carrier

Tactic:
rw [opensRange_awayι, opensRange_awayι, opensRange_awayι, ← basicOpen_mul, hx]

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
⊢ ∃ ι U x, IsOpenCover U ∧ ∀ (i : ι), IsAffineOpen (U i)

Tactic:
choose κ hsub heq using fun i ↦ Opens.isBasis_iff_cover.mp X.isBasis_affineOpens (W i)

Goal state after:
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)
⊢ ∃ ι U x, IsOpenCover U ∧ ∀ (i : ι), IsAffineOpen (U i)
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
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
rid : f ∈ asIdeal f_deg hm q
⊢ 1 ∈ q.asIdeal

Tactic:
by
        convert rid m
        rw [HomogeneousLocalization.ext_iff_val, HomogeneousLocalization.val_one,
          HomogeneousLocalization.val_mk]
        dsimp
        simp_rw [decompose_of_mem_same _ f_deg]
        simp

Goal state after:
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 𝒜
inst✝ : Algebra.FiniteType (↥(𝒜 0)) A
f : A
d : ℕ
hf : f ∈ 𝒜 d
s : Finset A
hs : Algebra.adjoin ↥(𝒜 0) ↑s = ⊤
hs' : ∀ i ∈ s, ∃ n, n ≠ 0 ∧ i ∈ 𝒜 n
dx : ↥s → ℕ
hdx : ∀ (x : ↥s), dx x ≠ 0
hxd : ∀ (x : ↥s), ↑x ∈ 𝒜 (dx x)
hd : d > 0
b : ℕ := ∑ i, dx i
s' : Set (Fin (b + 1) × (↥s → Fin (d + 1))) := {ai | ∑ i, ↑(ai.2 i) * dx i = ↑ai.1 * d}
ai : ↑s'
⊢ ∏ i, ↑i ^ ↑((↑ai).2 i) ∈ 𝒜 (↑(↑ai).1 • d)

Tactic:
convert! SetLike.prod_pow_mem_graded _ _ _ _ fun i _ ↦ hxd i; exact ai.2.symm

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

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

Tactic:
obtain rfl | hx0 := eq_or_ne x 0
  · exact (hxR R.toSubring.zero_mem).elim
  let := invertibleOfNonzero hx0
  let B := R.toSubring[x⁻¹]
  let xinv : B.toSubring := ⟨x⁻¹, subset_adjoin rfl⟩
  have : (maximalIdeal R.toSubring).map (algebraMap _ B) + .span {xinv} ≠ ⊤ := fun eq ↦ hxR <|
    have ⟨p, hp, hpx⟩ := exists_aeval_invOf_eq_zero_of_idealMap_adjoin_sup_span_eq_top _ _
      (maximalIdeal.isMaximal R.toSubring).ne_top eq
    have H : IsUnit p.leadingCoeff := of_not_not fun h ↦ by simpa using sub_mem h hp
    (Subring.isIntegrallyClosedIn_iff).mp ‹_›
      ⟨.C H.unit⁻¹.1 * p, by simp [Polynomial.Monic], by simpa using .inr hpx⟩
  have ⟨V, hV⟩ := Ideal.image_subset_nonunits_valuationSubring (A := B.toSubring) _ this
  refine ⟨V, ⟨fun r hr ↦ hV.1 (B.algebraMap_mem ⟨r, hr⟩),
    ((local_hom_TFAE _).out 3 0).mp fun r hr ↦ ?_⟩, (V.inv_mem_nonunits_iff.mp <|
      hV.2 ⟨_, le_add_self (α := Ideal B) (Ideal.subset_span rfl), rfl⟩).resolve_left hx0⟩
  rw [← V.image_maximalIdeal] at hV
  obtain ⟨⟨r, _⟩, hr, rfl⟩ := hV.2 ⟨_, le_self_add (α := Ideal B) (Ideal.mem_map_of_mem _ hr), rfl⟩
  exact hr

Goal state after: