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

Goal state before:
pp: R : Type u_1
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
p : Ideal S
inst✝² : p.IsPrime
inst✝¹ : FinitePresentation R S
inst✝ : IsSmoothAt R p
⊢ ∃ f ∉ p,
    ∃ n x,
      IsScalarTower R (MvPolynomial (Fin n) R) (Localization.Away f) ∧
        IsStandardEtale (MvPolynomial (Fin n) R) (Localization.Away f)

Tactic:
obtain ⟨f, hfp, H⟩ := IsSmoothAt.exists_notMem_isStandardSmooth R p
  obtain ⟨n, φ, hgC, hg⟩ := RingHom.IsStandardSmooth.exists_etale_mvPolynomial
    (f := algebraMap R (Localization.Away f)) (by simpa [RingHom.isStandardSmooth_algebraMap])
  algebraize [φ]
  have := IsScalarTower.of_algebraMap_eq' hgC.symm
  have : (Ideal.map (algebraMap S (Localization.Away f)) p).IsPrime :=
    IsLocalization.isPrime_of_isPrime_disjoint (.powers f) _ _ ‹_›
      ((Ideal.disjoint_powers_iff_notMem_of_isPrime _).mpr hfp)
  obtain ⟨g₀, hg, H⟩ := IsEtaleAt.exists_isStandardEtale (R := (MvPolynomial (Fin n) R))
    (S := (Localization.Away f)) (p.map (algebraMap _ _))
  obtain ⟨g, ⟨_, m, rfl⟩, hg₀⟩ := IsLocalization.exists_mk'_eq (.powers f) g₀
  replace hg : g ∉ p := by simpa [Submonoid.mem_powers_iff, Ideal.IsPrime.mul_mem_iff_mem_or_mem,
    IsLocalization.mk'_mem_map_algebraMap_iff, mt (‹p.IsPrime›.mem_of_pow_mem _) hfp,
    ← hg₀] using hg
  have : IsLocalization.Away (f * g) (Localization.Away g₀) := by
    suffices IsLocalization.Away (algebraMap _ (Localization.Away f) g) (Localization.Away g₀) from
      .mul' (Localization.Away f) _ _ _
    refine IsLocalization.Away.of_associated (r := g₀)
      ⟨(IsLocalization.Away.algebraMap_pow_isUnit f m).unit, ?_⟩
    simp only [← hg₀, IsUnit.unit_spec, ← map_pow, mul_comm, IsLocalization.mk'_spec'_mk]
  let e : Localization.Away g₀ ≃ₐ[S] Localization.Away (f * g) :=
    IsLocalization.algEquiv (.powers (f * g)) _ _
  let : Algebra (MvPolynomial (Fin n) R) (Localization.Away (f * g)) :=
    (e.toRingHom.comp (algebraMap (MvPolynomial (Fin n) R) _)).toAlgebra
  have : IsScalarTower R (MvPolynomial (Fin n) R) (Localization.Away (f * g)) := by
    refine .of_algebraMap_eq' ?_
    simp only [RingHom.algebraMap_toAlgebra, RingHom.comp_assoc, ← IsScalarTower.algebraMap_eq]
    exact (e.toAlgHom.comp_algebraMap_of_tower (R := R)).symm
  let e' : Localization.Away g₀ ≃ₐ[MvPolynomial (Fin n) R] Localization.Away (f * g) :=
    { __ := e, commutes' r := rfl }
  exact ⟨f * g, ‹p.IsPrime›.mul_notMem ‹_› ‹_›, n, ‹_›, ‹_›, .of_equiv e'⟩

Goal state after:
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.Smooth R S
f : PrimeSpectrum S → S
hfm : ∀ (m : PrimeSpectrum S), f m ∉ m.asIdeal
hf : ∀ (m : PrimeSpectrum S), Function.Bijective ⇑(toIntegralClosure R (Localization.Away (f m)) B)
H : ¬Ideal.span (Set.range f) = ⊤
⊢ False

Tactic:
obtain ⟨m, hm, e⟩ := Ideal.exists_le_maximal _ H

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.Smooth R S
f : PrimeSpectrum S → S
hfm : ∀ (m : PrimeSpectrum S), f m ∉ m.asIdeal
hf : ∀ (m : PrimeSpectrum S), Function.Bijective ⇑(toIntegralClosure R (Localization.Away (f m)) B)
H : ¬Ideal.span (Set.range f) = ⊤
m : Ideal S
hm : m.IsMaximal
e : Ideal.span (Set.range f) ≤ m
⊢ False
Module: Mathlib.RingTheory.ZariskisMainTheorem

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 S
inst✝¹ : p.IsPrime
inst✝ : WeaklyQuasiFiniteAt R p
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
hf : Function.Surjective ⇑f
this : Small.{u, v} S
r : Shrink.{u, v} S
hr : r ∉ Ideal.comap (Shrink.algEquiv R S).toRingEquiv.toRingHom p
H : ∀ (x : Shrink.{u, v} S), ∃ m, IsIntegral R (r ^ m * x)
x : S
m : ℕ
hm : IsIntegral R (r ^ m * (Shrink.algEquiv R S).symm x)
⊢ ∃ m, IsIntegral R ((Shrink.algEquiv R S) r ^ m * x)

Tactic:
exact ⟨m, by simpa [-Shrink.algEquiv_apply, -Shrink.algEquiv_symm_apply]
    using hm.map (Shrink.algEquiv R S).toAlgHom⟩

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Over

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
f : S →ₐ[R] T
Hf : Function.Surjective ⇑f
P : Ideal R
P' : Ideal S
inst✝¹ : P'.IsPrime
inst✝ : P'.LiesOver P
hkP' : ¬RingHom.ker f.toRingHom ≤ P'
H : (P.primesOver S).Finite
⊢ (comap f '' P.primesOver T).ncard < (P.primesOver S).ncard

Tactic:
refine Set.ncard_lt_ncard (Set.ssubset_iff_exists.mpr ⟨?_, P', ⟨‹_›, ‹_›⟩, ?_⟩) H

Goal state after:
case refine_1
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
f : S →ₐ[R] T
Hf : Function.Surjective ⇑f
P : Ideal R
P' : Ideal S
inst✝¹ : P'.IsPrime
inst✝ : P'.LiesOver P
hkP' : ¬RingHom.ker f.toRingHom ≤ P'
H : (P.primesOver S).Finite
⊢ comap f '' P.primesOver T ⊆ P.primesOver S

case refine_2
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
f : S →ₐ[R] T
Hf : Function.Surjective ⇑f
P : Ideal R
P' : Ideal S
inst✝¹ : P'.IsPrime
inst✝ : P'.LiesOver P
hkP' : ¬RingHom.ker f.toRingHom ≤ P'
H : (P.primesOver S).Finite
⊢ P' ∉ comap f '' P.primesOver T
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq S n
this : ∀ i ≥ n, (if i = n then 1 else 0) = (↑p).coeff i
⊢ (fun f ↦ (MonicDegreeEq.freeMonic R n).map f.toRingHom) ((fun p ↦ aeval fun x ↦ (↑p).coeff ↑x) p) = p

Tactic:
by
      ext i; simp +contextual [coeff_freeMonic, apply_dite, this]

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

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
n m k : ℕ
hn✝ hn : n = m + k
a✝¹ : Nontrivial R
a✝ : Nontrivial (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
⊢ (Polynomial.map (↑Algebra.TensorProduct.includeLeft) (freeMonic R m)).natDegree +
      (Polynomial.map (↑Algebra.TensorProduct.includeRight) (freeMonic R k)).natDegree =
    n

Tactic:
simp_rw [(monic_freeMonic R _).natDegree_map, natDegree_freeMonic, hn]

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

Goal state before:
pp: case injective
R✝ : Type u_1
inst✝² : CommRing R✝
R SatisfiesM : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing SatisfiesM
φ : R →+* SatisfiesM
hφ : Function.Injective ⇑φ
f : R[X]
IH :
  ∀ (g₁ g₂ : SatisfiesM[X]),
    (map φ f).resultant (g₁ * g₂) (map φ f).natDegree (g₁.natDegree + g₂.natDegree) =
      (map φ f).resultant g₁ * (map φ f).resultant g₂
g₁ g₂ : R[X]
⊢ f.resultant (g₁ * g₂) f.natDegree (g₁.natDegree + g₂.natDegree) = f.resultant g₁ * f.resultant g₂

Tactic:
| injective R SatisfiesM φ hφ f IH =>

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

Goal state before:
pp: case inr.e_a
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
h✝ : Nontrivial R
this : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (universalFactorizationMap R n m k hn).toAlgebra
⊢ ↑(aeval (universalFactorizationMapPresentation R n m k hn).val)
      ((Polynomial.map (↑((mapAlgHom (Algebra.ofId R (MvPolynomial (Fin n) R))).comp (rename Sum.inl)))
            (freeMonic R m)).resultant
        (Polynomial.map (↑((mapAlgHom (Algebra.ofId R (MvPolynomial (Fin n) R))).comp (rename Sum.inr)))
          (freeMonic R k))
        m k) =
    (Polynomial.map Algebra.TensorProduct.includeLeftRingHom (freeMonic R m)).resultant
      (Polynomial.map (↑Algebra.TensorProduct.includeRight) (freeMonic R k))

Tactic:
← Polynomial.resultant_map_map,

Goal state after:
case inr.e_a
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
h✝ : Nontrivial R
this : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (universalFactorizationMap R n m k hn).toAlgebra
⊢ (Polynomial.map (↑(aeval (universalFactorizationMapPresentation R n m k hn).val))
          (Polynomial.map (↑((mapAlgHom (Algebra.ofId R (MvPolynomial (Fin n) R))).comp (rename Sum.inl)))
            (freeMonic R m))).resultant
      (Polynomial.map (↑(aeval (universalFactorizationMapPresentation R n m k hn).val))
        (Polynomial.map (↑((mapAlgHom (Algebra.ofId R (MvPolynomial (Fin n) R))).comp (rename Sum.inr)))
          (freeMonic R k)))
      m k =
    (Polynomial.map Algebra.TensorProduct.includeLeftRingHom (freeMonic R m)).resultant
      (Polynomial.map (↑Algebra.TensorProduct.includeRight) (freeMonic R k))
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: case inr.inr.inr
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
h✝² : Nontrivial 𝓡
h✝¹ : Nontrivial (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
h✝ : Nontrivial R
this✝ : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (MvPolynomial.universalFactorizationMap R n m k hn).toAlgebra
this : Algebra (MvPolynomial (Fin n) R) R := ((MvPolynomial.mapEquivMonic R R n).symm p).toAlgebra
⊢ (-1) ^ n *
      ↑(fromTensor m k hn p)
        ((map Algebra.TensorProduct.includeLeftRingHom (freeMonic R m)).resultant
          (map Algebra.TensorProduct.includeRight.toRingHom (freeMonic R k))) =
    (-1) ^ n * (↑(factor₁ m k hn p)).resultant ↑(factor₂ m k hn p)

Tactic:
← Polynomial.resultant_map_map,

Goal state after:
case inr.inr.inr
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
h✝² : Nontrivial 𝓡
h✝¹ : Nontrivial (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
h✝ : Nontrivial R
this✝ : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (MvPolynomial.universalFactorizationMap R n m k hn).toAlgebra
this : Algebra (MvPolynomial (Fin n) R) R := ((MvPolynomial.mapEquivMonic R R n).symm p).toAlgebra
⊢ (-1) ^ n *
      (map (↑(fromTensor m k hn p)) (map Algebra.TensorProduct.includeLeftRingHom (freeMonic R m))).resultant
        (map (↑(fromTensor m k hn p)) (map Algebra.TensorProduct.includeRight.toRingHom (freeMonic R k)))
        (map Algebra.TensorProduct.includeLeftRingHom (freeMonic R m)).natDegree
        (map Algebra.TensorProduct.includeRight.toRingHom (freeMonic R k)).natDegree =
    (-1) ^ n * (↑(factor₁ m k hn p)).resultant ↑(factor₂ m k hn p)
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
q : { q // ↑q.1 * ↑q.2 = map (algebraMap R S) ↑p ∧ IsCoprime ↑q.1 ↑q.2 }
f : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) :=
  (UniversalFactorizationRing.homEquiv S m k hn p).symm ⟨↑q, ⋯⟩
a✝ : Nontrivial S
⊢ IsUnit
    (↑f ((-1) ^ n) *
      ↑f ((↑(UniversalFactorizationRing.factor₁ m k hn p)).resultant ↑(UniversalFactorizationRing.factor₂ m k hn p)))

Tactic:
← Polynomial.resultant_map_map,

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
q : { q // ↑q.1 * ↑q.2 = map (algebraMap R S) ↑p ∧ IsCoprime ↑q.1 ↑q.2 }
f : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) :=
  (UniversalFactorizationRing.homEquiv S m k hn p).symm ⟨↑q, ⋯⟩
a✝ : Nontrivial S
⊢ IsUnit
    (↑f ((-1) ^ n) *
      (map ↑f ↑(UniversalFactorizationRing.factor₁ m k hn p)).resultant
        (map ↑f ↑(UniversalFactorizationRing.factor₂ m k hn p))
        (↑(UniversalFactorizationRing.factor₁ m k hn p)).natDegree
        (↑(UniversalFactorizationRing.factor₂ m k hn p)).natDegree)
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case neg
m n : ℕ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
p : R[X]
hp : p ∈ R[X]_m
q : R[X]
hq : q ∈ R[X]_n
hg' : ¬g = 0
⊢ (g * ↑(⟨p, hp⟩, ⟨q, hq⟩).1).degree < ↑(m + n)

Tactic:
exact (degree_mul_le _ _).trans_lt ((WithBot.add_lt_add_of_le_of_lt (by simpa)
        (degree_le_of_natDegree_le hg) (by simpa using hp)).trans_eq (add_comm _ _))

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
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 (fst G G)) ⁻¹' {(Over.Hom.left η) point} \
      ⇑(Over.Hom.left γ) ⁻¹' {(Over.Hom.left (lift η η)) point}).Nonempty
c : Spec (CommRingCat.of K) ⟶ (G ⊗ G).left
hc : c ≫ (G ⊗ G).hom = 𝟙 (Spec (CommRingCat.of K))
hc₃ : c point ∈ closedPoints ↥(G ⊗ G).left
hc₁ : c point ∈ ⇑(Over.Hom.left (fst G G)) ⁻¹' {(Over.Hom.left η) point}
hc₂ : c point ∉ ⇑(Over.Hom.left γ) ⁻¹' {(Over.Hom.left (lift η η)) point}
e : (pointEquivClosedPoint (G ⊗ G).hom) ⟨c, hc⟩ = ⟨c point, hc₃⟩
fc : 𝟙_ (Over S) ⟶ 𝟙_ (Over S) ⊗ G := lift (𝟙 (𝟙_ (Over S))) (Over.homMk c hc ≫ snd G G)
this : c ≫ pullback.fst G.hom G.hom = Over.Hom.left η
⊢ c = Over.Hom.left fc ≫ Over.Hom.left (η ▷ G)

Tactic:
ext <;> simp [fc, S, this]

Goal state after:
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) := ⋯
G' : Over (Spec (CommRingCat.of (AlgebraicClosure K))) := ⋯
this✝² : IsProper G'.hom
this✝¹ : IsIntegral (G' ⊗ G').left
this✝ : GrpObj G' := ⋯
this : GrpObj.commutator G' = toUnit (G' ⊗ G') ≫ η
⊢ (Over.pullback f).map (GrpObj.commutator G) = (Over.pullback f).map (toUnit (G ⊗ G) ≫ η)

Tactic:
rw [← cancel_epi (Functor.Monoidal.μIso (Over.pullback f) G G).hom]

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
this✝¹ : IsIntegral (G' ⊗ G').left
this✝ : GrpObj G' := Functor.grpObjObj
this : GrpObj.commutator G' = toUnit (G' ⊗ G') ≫ η
⊢ (Functor.Monoidal.μIso (Over.pullback f) G G).hom ≫ (Over.pullback f).map (GrpObj.commutator G) =
    (Functor.Monoidal.μIso (Over.pullback f) G G).hom ≫ (Over.pullback f).map (toUnit (G ⊗ G) ≫ η)
Module: Mathlib.AlgebraicGeometry.IdealSheaf.IrreducibleComponent

Goal state before:
pp: X : Scheme
Z : Set ↥X
hZ : Z ∈ irreducibleComponents ↥X
inst✝ : IsNoetherian X
⊢ Z = ⋂ U, X.zeroLocus ↑((Hom.ker (X.irreducibleComponentOpen Z).ι).ideal U)

Tactic:
← IdealSheafData.coe_support_eq_eq_iInter_zeroLocus,

Goal state after:
X : Scheme
Z : Set ↥X
hZ : Z ∈ irreducibleComponents ↥X
inst✝ : IsNoetherian X
⊢ Z = ↑(Hom.ker (X.irreducibleComponentOpen Z).ι).support
Module: Mathlib.RingTheory.Etale.QuasiFinite

Goal state before:
pp: R : Type u
S : Type (max u v)
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Module.Finite R S
p : Ideal R
inst✝ : p.IsPrime
this✝ : IsArtinianRing (p.ResidueField ⊗[R] S)
hpSfin : (p.primesOver S).Finite
IH :
  ∀ m < 0,
    ∀ {R : Type u} {S : Type (max u v)} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
      [Module.Finite R S] (p : Ideal R) [inst_4 : p.IsPrime],
      (p.primesOver S).ncard = m →
        ∃ R' x x_1,
          ∃ (_ : Etale R R'),
            ∃ P,
              ∃ (x_3 : P.IsPrime) (x_4 : P.LiesOver p),
                ∃ n e,
                  ∃ (_ : CompleteOrthogonalIdempotents e),
                    ∃ P',
                      ∃ (_ : ∀ (i : Fin n), (P' i).IsPrime) (_ : ∀ (i : Fin n), (P' i).LiesOver P),
                        Function.Bijective ⇑(Ideal.ResidueField.mapₐ p P (ofId R R') ⋯) ∧
                          (∀ (i : Fin n), e i.castSucc ∉ P' i) ∧
                            ∀ (P'' : Ideal (R' ⊗[R] S)),
                              P''.IsPrime →
                                P''.LiesOver P → e (Fin.last n) ∈ P'' ∧ ∀ (i : Fin n), e i.castSucc ∉ P'' → P'' = P' i
h : (p.primesOver S).ncard = 0
this : p.primesOver S = ∅
⊢ ∀ (i : Fin (0 + 1)), IsIdempotentElem (1 i)

Tactic:
simp [IsIdempotentElem]

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

Goal state before:
pp: B : Type u₁
inst✝ : Bicategory B
a b : B
f : a ⟶ b
g : b ⟶ a
η : 𝟙 a ⟶ f ≫ g
ε : g ≫ f ⟶ 𝟙 b
h : leftZigzag η ε = (λ_ f).hom ≫ (ρ_ f).inv
⊢ (g ◁ η ⊗≫ ε ▷ g) ⊗≫ g ◁ η ⊗≫ ε ▷ g = g ◁ η ⊗≫ ε ▷ g

Tactic:
calc
    _ = g ◁ η ⊗≫ ((ε ▷ g ▷ 𝟙 a) ≫ (𝟙 b ≫ g) ◁ η) ⊗≫ ε ▷ g := by
      bicategory
    _ = 𝟙 _ ⊗≫ g ◁ (η ▷ 𝟙 a ≫ (f ≫ g) ◁ η) ⊗≫ (ε ▷ (g ≫ f) ≫ 𝟙 b ◁ ε) ▷ g ⊗≫ 𝟙 _ := by
      rw [← whisker_exchange]; bicategory
    _ = g ◁ η ⊗≫ g ◁ leftZigzag η ε ▷ g ⊗≫ ε ▷ g := by
      rw [← whisker_exchange, ← whisker_exchange, leftZigzag]; bicategory
    _ = g ◁ η ⊗≫ ε ▷ g := by
      rw [h]; bicategory

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

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

Tactic:
e.inv_hom_id,

Goal state after:
B : Type u
inst✝ : Bicategory B
a✝ b✝ c d a b : Adj B
adj₁ adj₂ : a ⟶ b
e : adj₁ ≅ adj₂
⊢ (𝟙 adj₂).τl = 𝟙 adj₂.l
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Adj

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

Tactic:
e.inv_hom_id,

Goal state after:
B : Type u
inst✝ : Bicategory B
a✝ b✝ c d a b : Adj B
adj₁ adj₂ : a ⟶ b
e : adj₁ ≅ adj₂
⊢ (𝟙 adj₂).τr = 𝟙 adj₂.r
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 𝒜
⊢ GaloisConnection (fun s ↦ zeroLocus 𝒜 s) fun t ↦ ↑(vanishingIdeal t)

Tactic:
by
  have ideal_gc : GaloisConnection Ideal.span _ := (Submodule.gi A _).gc
  simpa [zeroLocus_span, Function.comp_def] using GaloisConnection.compose ideal_gc (gc_ideal 𝒜)

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

Goal state before:
pp: case refine_1
X Y Z T : Scheme
M N K : X.Modules
φ : M ⟶ N
U✝ V : X.Opens
f✝ : X ⟶ Y
g : Y ⟶ Z
inst✝² : IsOpenImmersion f✝
inst✝¹ : IsOpenImmersion g
f : X ⟶ Y
inst✝ : IsOpenImmersion f
U : (TopologicalSpace.Opens ↥X)ᵒᵖ
r : ↑Γ(X, Opposite.unop U)
x : ↑Γ(Y, f ''ᵁ Opposite.unop U)
⊢ (AddCommGrpCat.Hom.hom
        (((forget₂ CommRingCat RingCat ⋙ forget₂ RingCat Ab).mapIso (Hom.appIso f (Opposite.unop U))).hom ≫
          (((SheafOfModules.forget X.ringCatSheaf).obj (unit X.ringCatSheaf)).obj U).smul r))
      x =
    (AddCommGrpCat.Hom.hom
        ((((SheafOfModules.forget X.ringCatSheaf).obj (restrict (unit Y.ringCatSheaf) f)).obj U).smul r ≫
          ((forget₂ CommRingCat RingCat ⋙ forget₂ RingCat Ab).mapIso (Hom.appIso f (Opposite.unop U))).hom))
      x

Tactic:
change r * (f.appIso U.unop).hom x = (f.appIso U.unop).hom ((f.appIso U.unop).inv r * x)

Goal state after:
case refine_1
X Y Z T : Scheme
M N K : X.Modules
φ : M ⟶ N
U✝ V : X.Opens
f✝ : X ⟶ Y
g : Y ⟶ Z
inst✝² : IsOpenImmersion f✝
inst✝¹ : IsOpenImmersion g
f : X ⟶ Y
inst✝ : IsOpenImmersion f
U : (TopologicalSpace.Opens ↥X)ᵒᵖ
r : ↑Γ(X, Opposite.unop U)
x : ↑Γ(Y, f ''ᵁ Opposite.unop U)
⊢ r * (ConcreteCategory.hom (Hom.appIso f (Opposite.unop U)).hom) x =
    (ConcreteCategory.hom (Hom.appIso f (Opposite.unop U)).hom)
      ((ConcreteCategory.hom (Hom.appIso f (Opposite.unop U)).inv) r * x)
Module: Mathlib.RingTheory.GradedAlgebra.Radical

Goal state before:
pp: case a
ι : 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
J : Ideal A
HJ₁ : I ≤ J
HJ₂ : J.IsPrime
⊢ ∃ b ∈ {J | IsHomogeneous 𝒜 J ∧ I ≤ J ∧ J.IsPrime}, b ≤ J

Tactic:
refine ⟨(J.homogeneousCore 𝒜).toIdeal, ?_, J.toIdeal_homogeneousCore_le _⟩

Goal state after:
case a
ι : 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
J : Ideal A
HJ₁ : I ≤ J
HJ₂ : J.IsPrime
⊢ (homogeneousCore 𝒜 J).toIdeal ∈ {J | IsHomogeneous 𝒜 J ∧ I ≤ J ∧ J.IsPrime}
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
⊢ Continuous (ToSpec.toFun f)

Tactic:
rw [PrimeSpectrum.isTopologicalBasis_basic_opens.continuous_iff]

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)