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

Goal state before:
pp: R : Type u_1
S : Type u_2
B : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : Algebra.IsStandardEtale R S
𝓟 : StandardEtalePresentation R S
n : ℕ
𝓟' : StandardEtalePresentation B (B ⊗[R] S) := 𝓟.baseChange
e : B ⊗[R] S ≃ₐ[B] Localization.Away ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g) := 𝓟'.equivRing.trans 𝓟'.equivAwayAdjoinRoot
a : AdjoinRoot 𝓟'.f
m : ℕ
hx✝ :
  IsIntegral S
    ((Algebra.TensorProduct.comm R B S)
      (e.symm
        (IsLocalization.mk' (Localization.Away ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g)) a
          ⟨(fun x ↦ (AdjoinRoot.mk 𝓟'.f) 𝓟'.g ^ x) m, ⋯⟩)))
hx :
  ∀ (m_1 : ℕ),
    IsIntegral R
      ((aeval 𝓟.x) 𝓟.g ^ (n + m_1) •
        (Algebra.TensorProduct.comm R B S)
          (e.symm
            (IsLocalization.mk' (Localization.Away ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g)) a
              ⟨(fun x ↦ (AdjoinRoot.mk 𝓟'.f) 𝓟'.g ^ x) m, ⋯⟩)))
hfg : IsIntegral R ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g)
heg :
  ∀ (g : R[X]),
    e (1 ⊗ₜ[R] (aeval 𝓟.x) g) =
      (algebraMap (AdjoinRoot 𝓟'.f) (Localization.Away ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g)))
        ((AdjoinRoot.mk 𝓟'.f) (Polynomial.map (algebraMap R B) g))
⊢ ∃ k, IsIntegral R ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g ^ k * a)

Tactic:
have H : ∀ k, e (1 ⊗ₜ (aeval 𝓟.x 𝓟.g ^ k)) = algebraMap _ _ (AdjoinRoot.mk 𝓟'.f 𝓟'.g ^ k) := by
      intro k; convert! congr($(heg 𝓟.g) ^ k) <;>
        simp [← map_pow, 𝓟', StandardEtalePresentation.baseChange]

Goal state after:
R : Type u_1
S : Type u_2
B : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : Algebra.IsStandardEtale R S
𝓟 : StandardEtalePresentation R S
n : ℕ
𝓟' : StandardEtalePresentation B (B ⊗[R] S) := 𝓟.baseChange
e : B ⊗[R] S ≃ₐ[B] Localization.Away ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g) := 𝓟'.equivRing.trans 𝓟'.equivAwayAdjoinRoot
a : AdjoinRoot 𝓟'.f
m : ℕ
hx✝ :
  IsIntegral S
    ((Algebra.TensorProduct.comm R B S)
      (e.symm
        (IsLocalization.mk' (Localization.Away ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g)) a
          ⟨(fun x ↦ (AdjoinRoot.mk 𝓟'.f) 𝓟'.g ^ x) m, ⋯⟩)))
hx :
  ∀ (m_1 : ℕ),
    IsIntegral R
      ((aeval 𝓟.x) 𝓟.g ^ (n + m_1) •
        (Algebra.TensorProduct.comm R B S)
          (e.symm
            (IsLocalization.mk' (Localization.Away ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g)) a
              ⟨(fun x ↦ (AdjoinRoot.mk 𝓟'.f) 𝓟'.g ^ x) m, ⋯⟩)))
hfg : IsIntegral R ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g)
heg :
  ∀ (g : R[X]),
    e (1 ⊗ₜ[R] (aeval 𝓟.x) g) =
      (algebraMap (AdjoinRoot 𝓟'.f) (Localization.Away ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g)))
        ((AdjoinRoot.mk 𝓟'.f) (Polynomial.map (algebraMap R B) g))
H :
  ∀ (k : ℕ),
    e (1 ⊗ₜ[R] ((aeval 𝓟.x) 𝓟.g ^ k)) =
      (algebraMap (AdjoinRoot 𝓟'.f) (Localization.Away ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g))) ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g ^ k)
⊢ ∃ k, IsIntegral R ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g ^ k * a)
Module: Mathlib.RingTheory.Polynomial.DegreeLT

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
m n : ℕ
i : Fin m
⊢ (basisProd R m n) (Fin.castAdd n i) = ((basis R m) i, 0)

Tactic:
by
  rw [basisProd, Basis.reindex_apply, finSumFinEquiv_symm_apply_castAdd, Basis.prod_apply,
    Sum.elim_inl, LinearMap.coe_inl, Function.comp_apply]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.DegreeLT

Goal state before:
pp: case hf
R : Type u_1
inst✝ : CommRing R
r : R
n : ℕ
⊢ Function.Surjective ⇑↑↑(taylorEquiv r)

Tactic:
exact (taylorEquiv r).surjective

Goal state after:
Module: Mathlib.RingTheory.Polynomial.DegreeLT

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
r : R
n : ℕ
⊢ 1 = ↑1

Tactic:
Units.val_one

Goal state after:
R : Type u_1
inst✝ : CommRing R
r : R
n : ℕ
⊢ 1 = 1
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U V : Y.Opens
x : ↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op V))
hx : x ∈ integralClosure ↑Γ(Y, Opposite.unop (Opposite.op V)) ↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op V))
i : Opposite.op V ⟶ Opposite.op U
algInst✝⁴ : Algebra ↑Γ(Y, U) ↑Γ(X, f ⁻¹ᵁ U) := (CommRingCat.Hom.hom (app f U)).toAlgebra
algInst✝³ : Algebra ↑Γ(Y, V) ↑Γ(X, f ⁻¹ᵁ V) := (CommRingCat.Hom.hom (app f V)).toAlgebra
algInst✝² : Algebra ↑Γ(Y, V) ↑Γ(Y, U) := (CommRingCat.Hom.hom (Y.presheaf.map i)).toAlgebra
algInst✝¹ : Algebra ↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op V)) ↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op U)) :=
  (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)).toAlgebra
algInst✝ : Algebra ↑Γ(Y, V) ↑Γ(X, f ⁻¹ᵁ U) := (CommRingCat.Hom.hom (appLE f V (f ⁻¹ᵁ U) ⋯)).toAlgebra
this : IsScalarTower ↑Γ(Y, V) ↑Γ(Y, U) ↑Γ(X, f ⁻¹ᵁ U)
⊢ (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) x ∈
    integralClosure ↑Γ(Y, Opposite.unop (Opposite.op U)) ↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op U))

Tactic:
have : IsScalarTower Γ(Y, V) Γ(X, f ⁻¹ᵁ V) Γ(X, f ⁻¹ᵁ U) := .of_algebraMap_eq' rfl

Goal state after:
X Y : Scheme
f : X ⟶ Y
U V : Y.Opens
x : ↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op V))
hx : x ∈ integralClosure ↑Γ(Y, Opposite.unop (Opposite.op V)) ↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op V))
i : Opposite.op V ⟶ Opposite.op U
algInst✝⁴ : Algebra ↑Γ(Y, U) ↑Γ(X, f ⁻¹ᵁ U) := (CommRingCat.Hom.hom (app f U)).toAlgebra
algInst✝³ : Algebra ↑Γ(Y, V) ↑Γ(X, f ⁻¹ᵁ V) := (CommRingCat.Hom.hom (app f V)).toAlgebra
algInst✝² : Algebra ↑Γ(Y, V) ↑Γ(Y, U) := (CommRingCat.Hom.hom (Y.presheaf.map i)).toAlgebra
algInst✝¹ : Algebra ↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op V)) ↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op U)) :=
  (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)).toAlgebra
algInst✝ : Algebra ↑Γ(Y, V) ↑Γ(X, f ⁻¹ᵁ U) := (CommRingCat.Hom.hom (appLE f V (f ⁻¹ᵁ U) ⋯)).toAlgebra
this✝ : IsScalarTower ↑Γ(Y, V) ↑Γ(Y, U) ↑Γ(X, f ⁻¹ᵁ U)
this : IsScalarTower ↑Γ(Y, V) ↑Γ(X, f ⁻¹ᵁ V) ↑Γ(X, f ⁻¹ᵁ U)
⊢ (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) x ∈
    integralClosure ↑Γ(Y, Opposite.unop (Opposite.op U)) ↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op U))
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
U : ↑Y.affineOpens
⊢ (f ⁻¹ᵁ ↑U).ι ≫ toNormalization f =
    (f ⁻¹ᵁ ↑U).toSpecΓ ≫
      Spec.map (CommRingCat.ofHom (integralClosure ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U)).val.toRingHom) ≫
        (normalizationOpenCover f).f U

Tactic:
← cancel_epi (pullbackRestrictIsoRestrict f U.1).hom,

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
U : ↑Y.affineOpens
⊢ (pullbackRestrictIsoRestrict f ↑U).hom ≫ (f ⁻¹ᵁ ↑U).ι ≫ toNormalization f =
    (pullbackRestrictIsoRestrict f ↑U).hom ≫
      (f ⁻¹ᵁ ↑U).toSpecΓ ≫
        Spec.map (CommRingCat.ofHom (integralClosure ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U)).val.toRingHom) ≫
          (normalizationOpenCover f).f U
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
U : ↑Y.affineOpens
e : ↑(fromNormalization f ⁻¹ᵁ ↑U) ≅ (normalizationOpenCover f).X U :=
  IsOpenImmersion.isoOfRangeEq (fromNormalization f ⁻¹ᵁ ↑U).ι ((normalizationOpenCover f).f U) ⋯
this : Algebra ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U) := (CommRingCat.Hom.hom (app f ↑U)).toAlgebra
⊢ (CommRingCat.Hom.hom ((normalizationDiagramMap f).app (Opposite.op ↑U))).IsIntegral

Tactic:
change (algebraMap Γ(Y, U) (integralClosure Γ(Y, U) Γ(X, f ⁻¹ᵁ U))).IsIntegral

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
U : ↑Y.affineOpens
e : ↑(fromNormalization f ⁻¹ᵁ ↑U) ≅ (normalizationOpenCover f).X U :=
  IsOpenImmersion.isoOfRangeEq (fromNormalization f ⁻¹ᵁ ↑U).ι ((normalizationOpenCover f).f U) ⋯
this : Algebra ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U) := (CommRingCat.Hom.hom (app f ↑U)).toAlgebra
⊢ (algebraMap ↑Γ(Y, ↑U) ↥(integralClosure ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U))).IsIntegral
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : FiniteType R S
p : Ideal S
H : ZariskisMainProperty R p
s : Finset S
hs : adjoin R ↑s = ⊤
r : S
hrp : r ∉ p
hr : IsIntegral R r
m : S → ℕ
hm : ∀ (x : S), IsIntegral R (r ^ m x * x)
t : Set S := insert r {x | ∃ x_1 ∈ s, r ^ m x_1 * x_1 = x}
r' : ↥(adjoin R t) := ⟨r, ⋯⟩
⊢ ∀ x ∈ t, IsIntegral R x

Tactic:
rintro a (rfl | ⟨x, hx, rfl⟩)

Goal state after:
case refine_2.inl
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : FiniteType R S
p : Ideal S
H : ZariskisMainProperty R p
s : Finset S
hs : adjoin R ↑s = ⊤
m : S → ℕ
a : S
hrp : a ∉ p
hr : IsIntegral R a
hm : ∀ (x : S), IsIntegral R (a ^ m x * x)
t : Set S := insert a {x | ∃ x_1 ∈ s, a ^ m x_1 * x_1 = x}
r' : ↥(adjoin R t) := ⟨a, ⋯⟩
⊢ IsIntegral R a

case refine_2.inr
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : FiniteType R S
p : Ideal S
H : ZariskisMainProperty R p
s : Finset S
hs : adjoin R ↑s = ⊤
r : S
hrp : r ∉ p
hr : IsIntegral R r
m : S → ℕ
hm : ∀ (x : S), IsIntegral R (r ^ m x * x)
t : Set S := insert r {x | ∃ x_1 ∈ s, r ^ m x_1 * x_1 = x}
r' : ↥(adjoin R t) := ⟨r, ⋯⟩
x : S
hx : x ∈ s
⊢ IsIntegral R (r ^ m x * x)
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: case a
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
f : MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R) →+* MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R := ⋯
H : ∀ (i : Fin m ⊕ Fin k), (tensorEquivSum R (Fin m) (Fin k) R) (f (X i)) = X i
⊢ RingHom.ker f ≤
    Ideal.span
      (Set.range fun i ↦
        C (X i) - (map C) ((tensorEquivSum R (Fin m) (Fin k) R) ((universalFactorizationMap R n m k hn) (X i))))

Tactic:
intro x hx
    convert_to x - (tensorEquivSum _ _ _ _ (f x)).map C ∈ Ideal.span _ using 1
    · simp_all only [RingHom.mem_ker, map_zero, sub_zero]
    clear hx
    induction x using MvPolynomial.induction_on with
    | add p q _ _ => simp only [map_add, add_sub_add_comm]; exact add_mem ‹_› ‹_›
    | mul_X p i _ => simp only [map_mul, H, map_X, ← sub_mul]; exact Ideal.mul_mem_right _ _ ‹_›
    | C x =>
    induction x using MvPolynomial.induction_on with
    | C a => simp [f]
    | add p q _ _ => simp only [map_add, add_sub_add_comm]; exact add_mem ‹_› ‹_›
    | mul_X p i IH =>
      simp only [map_mul]
      exact Ideal.mul_sub_mul_mem _ IH (Ideal.subset_span ⟨i, by simp [f]⟩)

Goal state after:
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: case h₁
X Y : Scheme
f : X ⟶ Y
inst✝⁵ : QuasiCompact f
inst✝⁴ : QuasiSeparated f
U V : Scheme
iU : U ⟶ X
iV : V ⟶ X
e : IsColimit (BinaryCofan.mk iU iV)
inst✝³ : QuasiCompact iU
inst✝² : QuasiSeparated iU
inst✝¹ : QuasiCompact iV
inst✝ : QuasiSeparated iV
H : iU ≫ (e.coconePointUniqueUpToIso (colimit.isColimit (pair U V))).hom = coprod.inl
⊢ toNormalization (iU ≫ f) ≫
      coprod.inl ≫
        coprod.desc (normalizationDesc (iU ≫ f) (iU ≫ toNormalization f) (fromNormalization f) ⋯)
            (normalizationDesc (iV ≫ f) (iV ≫ toNormalization f) (fromNormalization f) ⋯) ≫
          normalizationDesc f
            ((e.coconePointUniqueUpToIso (colimit.isColimit (pair U V))).hom ≫
              coprod.map (toNormalization (iU ≫ f)) (toNormalization (iV ≫ f)))
            (coprod.desc (fromNormalization (iU ≫ f)) (fromNormalization (iV ≫ f))) ⋯ =
    toNormalization (iU ≫ f) ≫ coprod.inl ≫ 𝟙 (normalization (iU ≫ f) ⨿ normalization (iV ≫ f))

Tactic:
simp [reassoc_of% H]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: case h₂
X Y : Scheme
f : X ⟶ Y
inst✝⁵ : QuasiCompact f
inst✝⁴ : QuasiSeparated f
U V : Scheme
iU : U ⟶ X
iV : V ⟶ X
e : IsColimit (BinaryCofan.mk iU iV)
inst✝³ : QuasiCompact iU
inst✝² : QuasiSeparated iU
inst✝¹ : QuasiCompact iV
inst✝ : QuasiSeparated iV
H : iV ≫ (e.coconePointUniqueUpToIso (colimit.isColimit (pair U V))).hom = coprod.inr
⊢ toNormalization (iV ≫ f) ≫
      coprod.inr ≫
        coprod.desc (normalizationDesc (iU ≫ f) (iU ≫ toNormalization f) (fromNormalization f) ⋯)
            (normalizationDesc (iV ≫ f) (iV ≫ toNormalization f) (fromNormalization f) ⋯) ≫
          normalizationDesc f
            ((e.coconePointUniqueUpToIso (colimit.isColimit (pair U V))).hom ≫
              coprod.map (toNormalization (iU ≫ f)) (toNormalization (iV ≫ f)))
            (coprod.desc (fromNormalization (iU ≫ f)) (fromNormalization (iV ≫ f))) ⋯ =
    toNormalization (iV ≫ f) ≫ coprod.inr ≫ 𝟙 (normalization (iU ≫ f) ⨿ normalization (iV ≫ f))

Tactic:
simp [reassoc_of% H]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
H✝ : IsCoprime f g
hf : f ≠ 0
hg : g ≠ 0
a b : R[X]
e : a * f + b * g = 1
ha : a ≠ 0
hb : b ≠ 0
this : f.resultant (b * g) f.natDegree (b.natDegree + g.natDegree) = f.resultant b * f.resultant g
H : b.natDegree + g.natDegree < (a * f).natDegree
⊢ False

Tactic:
← natDegree_mul hb hg

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
H✝ : IsCoprime f g
hf : f ≠ 0
hg : g ≠ 0
a b : R[X]
e : a * f + b * g = 1
ha : a ≠ 0
hb : b ≠ 0
this : f.resultant (b * g) f.natDegree (b.natDegree + g.natDegree) = f.resultant b * f.resultant g
H : (b * g).natDegree < (a * f).natDegree
⊢ False
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case inr
K : Type u_2
inst✝ : Field K
f g : K[X]
hf : f ≠ 0
H : (C f.leadingCoeff⁻¹ * f).Monic
this : IsUnit (f.leadingCoeff⁻¹ ^ g.natDegree) ∧ IsUnit (f.resultant g) ↔ IsCoprime (C f.leadingCoeff⁻¹ * f) g
⊢ f.resultant g = 0 ↔ (f ≠ 0 ∨ g ≠ 0) ∧ ¬IsCoprime f g

Tactic:
isCoprime_mul_unit_left_left (isUnit_C.mpr (by simp [hf]))

Goal state after:
case inr
K : Type u_2
inst✝ : Field K
f g : K[X]
hf : f ≠ 0
H : (C f.leadingCoeff⁻¹ * f).Monic
this : IsUnit (f.leadingCoeff⁻¹ ^ g.natDegree) ∧ IsUnit (f.resultant g) ↔ IsCoprime f g
⊢ f.resultant g = 0 ↔ (f ≠ 0 ∨ g ≠ 0) ∧ ¬IsCoprime f g
Module: Mathlib.AlgebraicGeometry.IdealSheaf.IrreducibleComponent

Goal state before:
pp: X : Scheme
Z : Set ↥X
hZ : Z ∈ irreducibleComponents ↥X
inst✝ : IsNoetherian X
⊢ X.irreducibleComponentIdeal Z hZ = Hom.ker (X.irreducibleComponentOpen Z).ι

Tactic:
ext
  rfl

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

Goal state before:
pp: case e'_3
R✝¹ R✝ A : CommRingCat
X M G : Scheme
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Bialgebra R T
e_1✝ :
  ((OverClass.asOver (pullback (Spec (of T) ↘ Spec (of R)) (Spec (of S) ↘ Spec (of R))) (Spec (of S)) ⊗
          OverClass.asOver (pullback (Spec (of T) ↘ Spec (of R)) (Spec (of S) ↘ Spec (of R))) (Spec (of S))).left ⟶
      Spec (of T)) =
    (((Over.pullback (Spec.map (ofHom (algebraMap R S)))).obj (Over.mk (Spec.map (ofHom (algebraMap R T)))) ⊗
          (Over.pullback (Spec.map (ofHom (algebraMap R S)))).obj (Over.mk (Spec.map (ofHom (algebraMap R T))))).left ⟶
      Spec (of T))
⊢ (Over.Hom.left
          ((Hom.asOver
                (pullbackSymmetry (Spec (of T) ↘ Spec (of R)) (Spec (of S) ↘ Spec (of R)) ≪≫ pullbackSpecIso' R S T).hom
                (Spec (of S)) ⊗ₘ
              Hom.asOver
                (pullbackSymmetry (Spec (of T) ↘ Spec (of R)) (Spec (of S) ↘ Spec (of R)) ≪≫ pullbackSpecIso' R S T).hom
                (Spec (of S))) ≫
            μ) ≫
        (pullbackSpecIso' R S T).inv) ≫
      pullback.snd (Spec (of S) ↘ Spec (of R)) (Spec (of T) ↘ Spec (of R)) =
    (Over.Hom.left
          (Hom.asOver
              (pullbackSymmetry (Spec (of T) ↘ Spec (of R)) (Spec (of S) ↘ Spec (of R)) ≪≫ pullbackSpecIso' R S T).hom
              (Spec (of S)) ⊗ₘ
            Hom.asOver
              (pullbackSymmetry (Spec (of T) ↘ Spec (of R)) (Spec (of S) ↘ Spec (of R)) ≪≫ pullbackSpecIso' R S T).hom
              (Spec (of S))) ≫
        (pullbackSpecIso S (S ⊗[R] T) (S ⊗[R] T)).hom ≫
          Spec.map (ofHom (mapRingHom (algebraMap R S) includeRight.toRingHom includeRight.toRingHom ⋯ ⋯)) ≫
            (pullbackSpecIso R T T).inv) ≫
      (pullbackSpecIso R T T).hom ≫ Spec.map (ofHom (Bialgebra.comulAlgHom R T).toRingHom)

Tactic:
· simp [pullbackSpecIso', specOverSpec_over, OverClass.asOver, Hom.asOver, ← Spec.map_comp,
          OverClass.asOverHom, mul_spec_asOver_spec_left, ← CommRingCat.ofHom_comp,
          ← Bialgebra.comul_includeRight]

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 c : a✝ ⟶ b✝
x : Hom₂ a b
y : Hom₂ b c
⊢ (conjugateEquiv c.adj a.adj) (x.τl ≫ y.τl) = y.τr ≫ x.τr

Tactic:
simp [← conjugateEquiv_comp c.adj b.adj a.adj y.τl x.τl,
          Hom₂.conjugateEquiv_τl]

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

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
inst✝¹ : Flat f
inst✝ : IsFinite f
x : ↥X
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [Flat f] [IsFinite f] (x : ↥X), (∃ R, Y = Spec R) → 1 ≤ finrank f (f x)
hY : ¬∃ R, Y = Spec R
R : CommRingCat
g : Spec R ⟶ Y
hg : IsOpenImmersion g
y : ↥(Spec R)
hy : g y = f x
⊢ 1 ≤ finrank f (f x)

Tactic:
← hy,

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝¹ : Flat f
inst✝ : IsFinite f
x : ↥X
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [Flat f] [IsFinite f] (x : ↥X), (∃ R, Y = Spec R) → 1 ≤ finrank f (f x)
hY : ¬∃ R, Y = Spec R
R : CommRingCat
g : Spec R ⟶ Y
hg : IsOpenImmersion g
y : ↥(Spec R)
hy : g y = f x
⊢ 1 ≤ finrank f (g y)
Module: Mathlib.RingTheory.OrderOfVanishing.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : KrullDimLE 1 R
x : R
hx : x ∈ nonZeroDivisors R
⊢ KrullDimLE 0 (R ⧸ span {x})

Tactic:
Ring.KrullDimLE,

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : KrullDimLE 1 R
x : R
hx : x ∈ nonZeroDivisors R
⊢ Order.KrullDimLE 0 (PrimeSpectrum (R ⧸ span {x}))
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology

Goal state before:
pp: case h_nhds
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
⊢ ∀ (a : ProjectiveSpectrum 𝒜) (u : Set (ProjectiveSpectrum 𝒜)),
    a ∈ u → IsOpen u → ∃ v ∈ Set.range fun r ↦ ↑(basicOpen 𝒜 r), a ∈ v ∧ v ⊆ u

Tactic:
rintro p U hp ⟨s, hs⟩

Goal state after:
case h_nhds
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
p : ProjectiveSpectrum 𝒜
U : Set (ProjectiveSpectrum 𝒜)
hp : p ∈ U
s : Set A
hs : zeroLocus 𝒜 s = Uᶜ
⊢ ∃ v ∈ Set.range fun r ↦ ↑(basicOpen 𝒜 r), p ∈ v ∧ v ⊆ U
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
F : Finset S
hF : Algebra.adjoin ↥(𝒜 0) ↑F = ⊤
ι₀ : Type (max u_1 u_3) := (x : ↥F) × ↥(DFinsupp.support ((DirectSum.decompose 𝒜) ↑x))
x : ι₀ → S := fun i ↦ ↑(((DirectSum.decompose 𝒜) ↑i.fst) ↑i.snd)
s : S
⊢ s ∈ ↑F → s ∈ ↑(Algebra.adjoin ↥(𝒜 0) ↑(Finset.image x Finset.univ))

Tactic:
hs

Goal state after:
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
F : Finset S
hF : Algebra.adjoin ↥(𝒜 0) ↑F = ⊤
ι₀ : Type (max u_1 u_3) := (x : ↥F) × ↥(DFinsupp.support ((DirectSum.decompose 𝒜) ↑x))
x : ι₀ → S := fun i ↦ ↑(((DirectSum.decompose 𝒜) ↑i.fst) ↑i.snd)
s : S
hs : s ∈ ↑F
⊢ s ∈ ↑(Algebra.adjoin ↥(𝒜 0) ↑(Finset.image x Finset.univ))
Module: Mathlib.RingTheory.GradedAlgebra.Radical

Goal state before:
pp: ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : LinearOrder ι
inst✝³ : IsOrderedCancelAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
hI : IsHomogeneous 𝒜 I
I_ne_top : I ≠ ⊤
homogeneous_mem_or_mem : ∀ {x y : A}, IsHomogeneousElem 𝒜 x → IsHomogeneousElem 𝒜 y → x * y ∈ I → x ∈ I ∨ y ∈ I
x y : A
rid₁ : x ∉ I
rid₂ : y ∉ I
set₁ : Finset ι := ⋯
set₁_eq : set₁ = {i ∈ DFinsupp.support ((decompose 𝒜) x) | (proj 𝒜 i) x ∉ I}
set₂ : Finset ι := ⋯
set₂_eq : set₂ = {i ∈ DFinsupp.support ((decompose 𝒜) y) | (proj 𝒜 i) y ∉ I}
nonempty : ∀ x ∉ I, {i ∈ DFinsupp.support ((decompose 𝒜) x) | (proj 𝒜 i) x ∉ I}.Nonempty
max₁ : ι := ⋯
max₂ : ι := ⋯
mem_max₁ : max₁ ∈ set₁
mem_max₂ : max₂ ∈ set₂
hxy : (proj 𝒜 (max₁ + max₂)) (x * y) ∈ I
antidiag : Finset (ι × ι) := ⋯
ha : antidiag = {z ∈ DFinsupp.support ((decompose 𝒜) x) ×ˢ DFinsupp.support ((decompose 𝒜) y) | z.1 + z.2 = max₁ + max₂}
mem_antidiag : (max₁, max₂) ∈ antidiag
eq_add_sum :
  (proj 𝒜 (max₁ + max₂)) (x * y) =
    (proj 𝒜 max₁) x * (proj 𝒜 max₂) y + ∑ ij ∈ antidiag.erase (max₁, max₂), (proj 𝒜 ij.1) x * (proj 𝒜 ij.2) y
i j : ι
H₁ : ¬(i = max₁ ∧ j = max₂)
H₄ : i + j = max₁ + max₂
H₂ : i ∈ DFinsupp.support ((decompose 𝒜) x)
H₃ : j ∈ DFinsupp.support ((decompose 𝒜) y)
⊢ max₁ < i ↔ max₁ ≤ i

Tactic:
rw [Ne.le_iff_lt]

Goal state after:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : LinearOrder ι
inst✝³ : IsOrderedCancelAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
hI : IsHomogeneous 𝒜 I
I_ne_top : I ≠ ⊤
homogeneous_mem_or_mem : ∀ {x y : A}, IsHomogeneousElem 𝒜 x → IsHomogeneousElem 𝒜 y → x * y ∈ I → x ∈ I ∨ y ∈ I
x y : A
rid₁ : x ∉ I
rid₂ : y ∉ I
set₁ : Finset ι := {i ∈ DFinsupp.support ((decompose 𝒜) x) | (proj 𝒜 i) x ∉ I}
set₁_eq : set₁ = {i ∈ DFinsupp.support ((decompose 𝒜) x) | (proj 𝒜 i) x ∉ I}
set₂ : Finset ι := {i ∈ DFinsupp.support ((decompose 𝒜) y) | (proj 𝒜 i) y ∉ I}
set₂_eq : set₂ = {i ∈ DFinsupp.support ((decompose 𝒜) y) | (proj 𝒜 i) y ∉ I}
nonempty : ∀ x ∉ I, {i ∈ DFinsupp.support ((decompose 𝒜) x) | (proj 𝒜 i) x ∉ I}.Nonempty
max₁ : ι := set₁.max' ⋯
max₂ : ι := set₂.max' ⋯
mem_max₁ : max₁ ∈ set₁
mem_max₂ : max₂ ∈ set₂
hxy : (proj 𝒜 (max₁ + max₂)) (x * y) ∈ I
antidiag : Finset (ι × ι) :=
  {z ∈ DFinsupp.support ((decompose 𝒜) x) ×ˢ DFinsupp.support ((decompose 𝒜) y) | z.1 + z.2 = max₁ + max₂}
ha : antidiag = {z ∈ DFinsupp.support ((decompose 𝒜) x) ×ˢ DFinsupp.support ((decompose 𝒜) y) | z.1 + z.2 = max₁ + max₂}
mem_antidiag : (max₁, max₂) ∈ antidiag
eq_add_sum :
  (proj 𝒜 (max₁ + max₂)) (x * y) =
    (proj 𝒜 max₁) x * (proj 𝒜 max₂) y + ∑ ij ∈ antidiag.erase (max₁, max₂), (proj 𝒜 ij.1) x * (proj 𝒜 ij.2) y
i j : ι
H₁ : ¬(i = max₁ ∧ j = max₂)
H₄ : i + j = max₁ + max₂
H₂ : i ∈ DFinsupp.support ((decompose 𝒜) x)
H₃ : j ∈ DFinsupp.support ((decompose 𝒜) y)
⊢ max₁ ≠ i
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: case map_units
A : Type u_2
σ : Type u_3
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
e d : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : d ≠ 0
this : Algebra (Away 𝒜 f) (Away 𝒜 x) := ⋯
⊢ ∀ (y : ↥(Submonoid.powers (isLocalizationElem hf hg))), IsUnit ((algebraMap (Away 𝒜 f) (Away 𝒜 x)) ↑y)

Tactic:
rintro ⟨r, n, rfl⟩
    rw [map_pow, RingHom.algebraMap_toAlgebra]
    let z : Away 𝒜 x := Away.mk 𝒜 (hx ▸ SetLike.mul_mem_graded hf hg) (d + e)
        (g ^ e * f ^ (2 * e + d)) <| by
      convert!
        SetLike.mul_mem_graded (SetLike.pow_mem_graded e hg)
          (SetLike.pow_mem_graded (2 * e + d) hf) using 2
      ring
    refine (isUnit_iff_exists_inv.mpr ⟨z, ?_⟩).pow _
    ext
    simp only [val_mul, val_one, awayMap_mk, Away.val_mk, z, Localization.mk_mul]
    rw [← Localization.mk_one, Localization.mk_eq_mk_iff, Localization.r_iff_exists]
    use 1
    simp only [OneMemClass.coe_one, one_mul, Submonoid.coe_mul, mul_one, hx]
    ring

Goal state after: