mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case Splits
R✝ : Type u_1
inst✝¹ : CommRing R✝
R : Type u_1
inst✝ : Field R
f : R[X]
hff : f.Splits
g₁ g₂ : R[X]
⊢ f.leadingCoeff ^ (g₁.natDegree + g₂.natDegree) *
      ((Multiset.map (fun i ↦ eval i g₁) f.roots).prod * (Multiset.map (fun i ↦ eval i g₂) f.roots).prod) =
    f.leadingCoeff ^ g₁.natDegree * (Multiset.map (fun x ↦ eval x g₁) f.roots).prod *
      (f.leadingCoeff ^ g₂.natDegree * (Multiset.map (fun x ↦ eval x g₂) f.roots).prod)

Tactic:
ring_nf

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

Goal state before:
pp: case surjective
R✝ : Type u_1
inst✝² : CommRing R✝
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
φ : R →+* S
hφ : Function.Surjective ⇑φ
f : S[X]
IH :
  ∀ (q g₁ g₂ : R[X]), q.resultant (g₁ * g₂) q.natDegree (g₁.natDegree + g₂.natDegree) = q.resultant g₁ * q.resultant g₂
g₁ g₂ : S[X]
f' : R[X]
hf' : map φ f' = f
e : f'.degree = f.degree
g₁' : R[X]
hg₁ : map φ g₁' = g₁
e₁ : g₁'.degree = g₁.degree
g₂' : R[X]
hg₂ : map φ g₂' = g₂
e₂ : g₂'.degree = g₂.degree
⊢ f.resultant (g₁ * g₂) f.natDegree (g₁.natDegree + g₂.natDegree) = f.resultant g₁ * f.resultant g₂

Tactic:
← hg₁,

Goal state after:
case surjective
R✝ : Type u_1
inst✝² : CommRing R✝
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
φ : R →+* S
hφ : Function.Surjective ⇑φ
f : S[X]
IH :
  ∀ (q g₁ g₂ : R[X]), q.resultant (g₁ * g₂) q.natDegree (g₁.natDegree + g₂.natDegree) = q.resultant g₁ * q.resultant g₂
g₁ g₂ : S[X]
f' : R[X]
hf' : map φ f' = f
e : f'.degree = f.degree
g₁' : R[X]
hg₁ : map φ g₁' = g₁
e₁ : g₁'.degree = g₁.degree
g₂' : R[X]
hg₂ : map φ g₂' = g₂
e₂ : g₂'.degree = g₂.degree
⊢ f.resultant (map φ g₁' * g₂) f.natDegree ((map φ g₁').natDegree + g₂.natDegree) =
    f.resultant (map φ g₁') * f.resultant g₂
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f₁ f₂ g : R[X]
n : ℕ
hn : g.natDegree ≤ n
⊢ (-1) ^ ((f₁.natDegree + f₂.natDegree) * n) *
      ((-1) ^ (n * f₁.natDegree) * f₁.resultant g f₁.natDegree n * g.resultant f₂ n) =
    f₁.resultant g f₁.natDegree n * ((-1) ^ (f₂.natDegree * n) * g.resultant f₂ n)

Tactic:
ring_nf

Goal state after:
R : Type u_1
inst✝ : CommRing R
f₁ f₂ g : R[X]
n : ℕ
hn : g.natDegree ≤ n
⊢ f₁.resultant g f₁.natDegree n * g.resultant f₂ n * (-1) ^ (f₁.natDegree * n * 2) * (-1) ^ (f₂.natDegree * n) =
    f₁.resultant g f₁.natDegree n * g.resultant f₂ n * (-1) ^ (f₂.natDegree * n)
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case neg
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 rfl | hr := eq_or_ne r 0

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

case neg.inr
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
hr : r ≠ 0
⊢ (f.scaleRoots r).resultant (g.scaleRoots r) f.natDegree g.natDegree = r ^ (f.natDegree * g.natDegree) * f.resultant g
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: case tmul.refine_1.mul_X
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
this✝¹ : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (universalFactorizationMap R n m k hn).toAlgebra
this✝ : IsDomain (MvPolynomial (Fin m) ℤ ⊗[ℤ] MvPolynomial (Fin k) ℤ)
this : Algebra (MvPolynomial (Fin n) ℤ) (MvPolynomial (Fin m) ℤ ⊗[ℤ] MvPolynomial (Fin k) ℤ) :=
  (universalFactorizationMap ℤ n m k hn).toAlgebra
F : MvPolynomial (Fin m) ℤ ⊗[ℤ] MvPolynomial (Fin k) ℤ →ₐ[ℤ] MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R :=
  Algebra.TensorProduct.lift (Algebra.TensorProduct.includeLeft.comp (mapAlgHom (Algebra.ofId ℤ R)))
    ((AlgHom.restrictScalars ℤ Algebra.TensorProduct.includeRight).comp (mapAlgHom (Algebra.ofId ℤ R))) ⋯
H₁ : ∀ (i : Fin m), (universalFactorizationMap R n m k hn).IsIntegralElem (X i ⊗ₜ[R] 1)
H₂ : ∀ (i : Fin k), (universalFactorizationMap R n m k hn).IsIntegralElem (1 ⊗ₜ[R] X i)
y : MvPolynomial (Fin k) R
p : MvPolynomial (Fin m) R
i : Fin m
IH : (universalFactorizationMap R n m k hn).IsIntegralElem (p ⊗ₜ[R] 1)
⊢ (universalFactorizationMap R n m k hn).IsIntegralElem ((p * X i) ⊗ₜ[R] 1)

Tactic:
simpa [← map_mul] using! IH.mul _ (H₁ i)

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

Goal state before:
pp: case refine_1
R : Type u
S : Type v
T : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra.FiniteType R T
inst✝¹ : Algebra.IsIntegral R S
f : S →ₐ[R] T
g : S
hg : Function.Surjective ⇑(awayMapₐ f g)
p : Ideal R
inst✝ : p.IsPrime
hgp : IsUnit (1 ⊗ₜ[R] g)
this : IsClosed (PrimeSpectrum.comap (algebraMap R S) '' PrimeSpectrum.zeroLocus {g})
r : R
hpr : { asIdeal := p, isPrime := inst✝ } ∈ ↑(PrimeSpectrum.basicOpen r)
hrg : ↑(PrimeSpectrum.basicOpen r) ⊆ (PrimeSpectrum.comap (algebraMap R S) '' PrimeSpectrum.zeroLocus {g})ᶜ
⊢ (awayMapₐ (Algebra.ofId R T) r).IsIntegral

Tactic:
have : IsLocalization.Away (f.toRingHom (algebraMap R S r))
        (Localization.Away (algebraMap R T r)) := by
      simp only [AlgHom.toRingHom_eq_coe, RingHom.coe_coe, AlgHom.commutes]; infer_instance

Goal state after:
case refine_1
R : Type u
S : Type v
T : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra.FiniteType R T
inst✝¹ : Algebra.IsIntegral R S
f : S →ₐ[R] T
g : S
hg : Function.Surjective ⇑(awayMapₐ f g)
p : Ideal R
inst✝ : p.IsPrime
hgp : IsUnit (1 ⊗ₜ[R] g)
this✝ : IsClosed (PrimeSpectrum.comap (algebraMap R S) '' PrimeSpectrum.zeroLocus {g})
r : R
hpr : { asIdeal := p, isPrime := inst✝ } ∈ ↑(PrimeSpectrum.basicOpen r)
hrg : ↑(PrimeSpectrum.basicOpen r) ⊆ (PrimeSpectrum.comap (algebraMap R S) '' PrimeSpectrum.zeroLocus {g})ᶜ
this : IsLocalization.Away (f.toRingHom ((algebraMap R S) r)) (Away ((algebraMap R T) r))
⊢ (awayMapₐ (Algebra.ofId R T) r).IsIntegral
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case neg.refine_1
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.Monic
hf0 : ¬f.natDegree = 0
H : IsUnit (f.resultant g)
p q : R[X]
hp : p.degree < ↑g.natDegree
hq : q.degree < ↑f.natDegree
e : f * p + g * q = C (f.resultant g)
⊢ IsCoprime f g

Tactic:
exact ⟨C (H.unit⁻¹).1 * p, C (H.unit⁻¹).1 * q, by simp only [mul_assoc, ← mul_add, mul_comm p,
      mul_comm q, e, ← map_mul, IsUnit.val_inv_mul, map_one]⟩

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 2
e : Fin (f.natDegree - 1 + f.natDegree) ≃ Fin 3 := finCongr ⋯
this : (Matrix.reindex e e) f.sylvesterDeriv = !![f.coeff 0, f.coeff 1, 0; f.coeff 1, 2 * f.coeff 2, f.coeff 1; 1, 0, 2]
⊢ (f.coeff 0 * (2 * f.coeff 2) * 2 - f.coeff 0 * f.coeff 1 * 0 - f.coeff 1 * f.coeff 1 * 2 + f.coeff 1 * f.coeff 1 * 1 +
          0 * f.coeff 1 * 0 -
        0 * (2 * f.coeff 2) * 1) *
      (-1) ^ (2 * (2 - 1) / 2) =
    f.coeff 1 ^ 2 - 4 * f.coeff 0 * f.coeff 2

Tactic:
ring_nf

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : 0 < f.natDegree
⊢ (-1) ^ ((f.natDegree - 1) * f.natDegree) * (f.leadingCoeff * f.sylvesterDeriv.det) =
    (-1) ^ ((f.natDegree - 1) * f.natDegree / 2) * f.leadingCoeff *
      (f.sylvesterDeriv.det * (-1) ^ ((f.natDegree - 1) * f.natDegree / 2))

Tactic:
ring_nf

Goal state after:
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : 0 < f.natDegree
⊢ f.leadingCoeff * f.sylvesterDeriv.det * (-1) ^ ((f.natDegree - 1) * f.natDegree) =
    f.leadingCoeff * f.sylvesterDeriv.det * (-1) ^ ((f.natDegree - 1) * f.natDegree / 2 * 2)
Module: Mathlib.RingTheory.Etale.QuasiFinite

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

Tactic:
set m' := rootMultiplicity 0 ((minpoly R s).map (algebraMap R p.ResidueField))

Goal state after:
R : Type u
S : Type v
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : FiniteType R S
p : Ideal R
inst✝³ : p.IsPrime
q✝ : Ideal S
inst✝² : q✝.IsPrime
inst✝¹ : q✝.LiesOver p
inst✝ : QuasiFiniteAt R q✝
s : S
hsq : s ∉ q✝
hRs : IsIntegral R s
hs : ∀ (q' : Ideal S), q'.IsPrime → q' ≠ q✝ → q'.LiesOver p → s ∈ q'
hs₀ :
  ∀ (q' : Ideal ↥(integralClosure R S)),
    q'.IsPrime → q' ≠ Ideal.under (↥(integralClosure R S)) q✝ → q'.LiesOver p → ⟨s, hRs⟩ ∈ q'
f : R[X] := X * minpoly R s
q : p.ResidueField[X]
hq' : ¬X - C 0 ∣ q
hqm : q.Monic
m' : ℕ := rootMultiplicity 0 (Polynomial.map (algebraMap R p.ResidueField) (minpoly R s))
hq : Polynomial.map (algebraMap R p.ResidueField) (minpoly R s) = (X - C 0) ^ m' * q
⊢ ∃ m f b,
    f.Monic ∧
      b.Monic ∧
        IsCoprime (X ^ (m + 1)) b ∧ Polynomial.map (algebraMap R p.ResidueField) f = X ^ (m + 1) * b ∧ (aeval s) f = 0
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
e : Fin (f.natDegree - 1 + f.natDegree) ≃ Fin 5 := finCongr ⋯
⊢ (f.coeff 0 *
          (f.coeff 0 * (3 * f.coeff 3 * (3 * f.coeff 3) * 3) +
              -(2 * f.coeff 2 *
                  (f.coeff 1 * (3 * f.coeff 3) * 3 - 2 * f.coeff 2 * f.coeff 2 * 3 + 2 * f.coeff 2 * (2 * f.coeff 2) -
                    f.coeff 1 * (3 * f.coeff 3))) +
            f.coeff 1 * (-(3 * f.coeff 3 * f.coeff 2 * 3) + 3 * f.coeff 3 * (2 * f.coeff 2))) +
        f.coeff 1 *
          (f.coeff 1 *
                (f.coeff 1 * (3 * f.coeff 3) * 3 - 2 * f.coeff 2 * f.coeff 2 * 3 + 2 * f.coeff 2 * (2 * f.coeff 2) -
                  f.coeff 1 * (3 * f.coeff 3)) +
              -(f.coeff 0 * (f.coeff 2 * (3 * f.coeff 3) * 3 - 2 * f.coeff 2 * f.coeff 3 * 3)) +
            f.coeff 1 *
              (f.coeff 2 * f.coeff 2 * 3 - f.coeff 2 * (2 * f.coeff 2) - f.coeff 1 * f.coeff 3 * 3 +
                f.coeff 1 * f.coeff 3))) *
      (-1) ^ 3 =
    f.coeff 2 ^ 2 * f.coeff 1 ^ 2 - 4 * f.coeff 3 * f.coeff 1 ^ 3 - 4 * f.coeff 2 ^ 3 * f.coeff 0 -
        27 * f.coeff 3 ^ 2 * f.coeff 0 ^ 2 +
      18 * f.coeff 3 * f.coeff 2 * f.coeff 1 * f.coeff 0

Tactic:
ring_nf

Goal state after:
Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝² : LocallyOfFiniteType f
inst✝¹ : IsSeparated f
inst✝ : QuasiCompact f
V : { x // QuasiFiniteAt f x } → (normalization f).Opens
hxV✝ : ∀ (x : { x // QuasiFiniteAt f x }), (toNormalization f) ↑x ∈ V x
hV : ∀ (x : { x // QuasiFiniteAt f x }), IsIso (toNormalization f ∣_ V x)
𝒰 : (↑(⨆ i, V i)).OpenCover := Opens.iSupOpenCover V
this✝¹ : IsIso (toNormalization f ∣_ ⨆ x, V x)
x : ↥X
y : ↑{x | QuasiFiniteAt f x}
hxVy : (toNormalization f) x ∈ V y
U : Y.Opens
r : ↑Γ(normalization f, fromNormalization f ⁻¹ᵁ U)
hU : IsAffineOpen U
hr : IsAffineOpen (toNormalization f ⁻¹ᵁ (normalization f).basicOpen r)
hxV : x ∈ toNormalization f ⁻¹ᵁ (normalization f).basicOpen r
hrV : (normalization f).basicOpen r ≤ V y
W : X.Opens := toNormalization f ⁻¹ᵁ (normalization f).basicOpen r
H : W ≤ f ⁻¹ᵁ U
H' :
  appLE (fromNormalization f) U ((normalization f).basicOpen r) ⋯ ≫
      app (toNormalization f) ((normalization f).basicOpen r) =
    appLE f U W H
this✝ : IsIso (app (toNormalization f) ((normalization f).basicOpen r))
this : (CommRingCat.Hom.hom (appLE f U W H)).QuasiFinite
hxU : f x ∈ U
⊢ QuasiFiniteAt f x

Tactic:
refine .of_comp (g := (Y.presheaf.germ U _ hxU).hom) ?_

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝² : LocallyOfFiniteType f
inst✝¹ : IsSeparated f
inst✝ : QuasiCompact f
V : { x // QuasiFiniteAt f x } → (normalization f).Opens
hxV✝ : ∀ (x : { x // QuasiFiniteAt f x }), (toNormalization f) ↑x ∈ V x
hV : ∀ (x : { x // QuasiFiniteAt f x }), IsIso (toNormalization f ∣_ V x)
𝒰 : (↑(⨆ i, V i)).OpenCover := Opens.iSupOpenCover V
this✝¹ : IsIso (toNormalization f ∣_ ⨆ x, V x)
x : ↥X
y : ↑{x | QuasiFiniteAt f x}
hxVy : (toNormalization f) x ∈ V y
U : Y.Opens
r : ↑Γ(normalization f, fromNormalization f ⁻¹ᵁ U)
hU : IsAffineOpen U
hr : IsAffineOpen (toNormalization f ⁻¹ᵁ (normalization f).basicOpen r)
hxV : x ∈ toNormalization f ⁻¹ᵁ (normalization f).basicOpen r
hrV : (normalization f).basicOpen r ≤ V y
W : X.Opens := toNormalization f ⁻¹ᵁ (normalization f).basicOpen r
H : W ≤ f ⁻¹ᵁ U
H' :
  appLE (fromNormalization f) U ((normalization f).basicOpen r) ⋯ ≫
      app (toNormalization f) ((normalization f).basicOpen r) =
    appLE f U W H
this✝ : IsIso (app (toNormalization f) ((normalization f).basicOpen r))
this : (CommRingCat.Hom.hom (appLE f U W H)).QuasiFinite
hxU : f x ∈ U
⊢ ((CommRingCat.Hom.hom (stalkMap f x)).comp (CommRingCat.Hom.hom (Y.presheaf.germ U (f x) hxU))).QuasiFinite
Module: Mathlib.RingTheory.Finiteness.Descent

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✝ : Module.FaithfullyFlat R S
I : Ideal R
hI : (Ideal.map (algebraMap R S) I).FG
f : S ⊗[R] ↥I →ₗ[S] S := ↑(AlgebraTensorModule.rid R S S) ∘ₗ (AlgebraTensorModule.lTensor S S) (Submodule.subtype I)
hf : Function.Injective ⇑f
x : S ⊗[R] ↥I
⊢ f x ∈ Ideal.map (algebraMap R S) I

Tactic:
induction x with
      | zero => simp
      | add _ _ _ _ => simp_all [Ideal.add_mem]
      | tmul s x =>
        have : f (s ⊗ₜ[R] x) = s • f (1 ⊗ₜ x) := by simp [f]
        rw [this]
        apply Ideal.mul_mem_left
        simpa [f, Algebra.smul_def] using Ideal.mem_map_of_mem _ x.2

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

Goal state before:
pp: R✝ R A : CommRingCat
inst✝¹ : Algebra ↑R ↑A
inst✝ : Algebra.FiniteType ↑R ↑A
⊢ LocallyOfFiniteType (Spec A ↘ Spec R)

Tactic:
rw [specOverSpec_over, HasRingHomProperty.Spec_iff (P := @LocallyOfFiniteType)]

Goal state after:
R✝ R A : CommRingCat
inst✝¹ : Algebra ↑R ↑A
inst✝ : Algebra.FiniteType ↑R ↑A
⊢ (CommRingCat.Hom.hom (CommRingCat.ofHom (algebraMap ↑R ↑A))).FiniteType
Module: Mathlib.AlgebraicGeometry.Group.Affine

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

Tactic:
simp only [mul_spec_asOver_spec_left, ← Category.assoc, algSpec, Equivalence.op_functor,
      comp_obj, op_obj, commAlgCatEquivUnder_functor_obj, Over.opEquivOpUnder_inverse_obj,
      CommRingCat.mkUnder_hom, Over.post_obj, Spec_obj, Over.mk_left, Over.mk_hom, Spec_map,
      Quiver.Hom.unop_op, Spec.map_comp]

Goal state after:
case e'_2
R✝ R A : CommRingCat
inst✝¹ : Bialgebra ↑R ↑A
inst✝ : IsCocomm ↑R ↑A
this :
  (pullbackSpecIso ↑R ↑A ↑A).hom ≫
      Spec.map
        (Under.Hom.right (↑(Bialgebra.comulBialgHom ↑R ↑A)).toUnder ≫
          Under.Hom.right (↑↑(Bialgebra.TensorProduct.comm ↑R ↑A ↑A)).toUnder) =
    (pullbackSpecIso ↑R ↑A ↑A).hom ≫ Spec.map (Under.Hom.right (↑(Bialgebra.comulBialgHom ↑R ↑A)).toUnder)
h₁ :
  ↑Algebra.TensorProduct.includeRight =
    (↑(Bialgebra.TensorProduct.comm ↑R ↑A ↑A)).comp Algebra.TensorProduct.includeLeftRingHom
h₂ :
  Algebra.TensorProduct.includeLeftRingHom =
    (↑(Bialgebra.TensorProduct.comm ↑R ↑A ↑A)).comp ↑Algebra.TensorProduct.includeRight
e_1✝ :
  (pullback (Spec A ↘ Spec R) (Spec A ↘ Spec R) ⟶ Spec A) =
    (pullback (Spec.map (CommRingCat.ofHom (algebraMap ↑R ↑A))) (Spec.map (CommRingCat.ofHom (algebraMap ↑R ↑A))) ⟶
      ((algSpec R).obj (op (CommAlgCat.of ↑R ↑A))).left)
⊢ ((pullbackSymmetry (Spec A ↘ Spec R) (Spec A ↘ Spec R)).hom ≫ (pullbackSpecIso ↑R ↑A ↑A).hom) ≫
      Spec.map (CommRingCat.ofHom ↑(Bialgebra.comulAlgHom ↑R ↑A)) =
    ((pullbackSpecIso ↑R ↑A ↑A).hom ≫ Spec.map (Under.Hom.right (↑↑(Bialgebra.TensorProduct.comm ↑R ↑A ↑A)).toUnder)) ≫
      Spec.map (Under.Hom.right (↑(Bialgebra.comulBialgHom ↑R ↑A)).toUnder)
Module: Mathlib.Tactic.CategoryTheory.Bicategory.Normalize

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b : B
f g h i j : a ⟶ b
α : f ≅ g
η : g ⟶ h
ηs : h ⟶ i
θ : i ⟶ j
ι : h ⟶ j
e_ι : ηs ≫ θ = ι
⊢ (α.hom ≫ η ≫ ηs) ≫ θ = α.hom ≫ η ≫ ι

Tactic:
by
  simp [e_ι]

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

Goal state before:
pp: 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
⊢ rankAtStalk S = 1 ↔ Function.Bijective ⇑(algebraMap R S)

Tactic:
rw [Function.Bijective, ← rankAtStalk_pos_iff_algebraMap_injective,
    ← rankAtStalk_le_one_iff_surjective]
  refine ⟨fun h ↦ by simp [h], fun h ↦ ?_⟩
  ext p
  rw [Pi.one_apply]
  grind

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

Goal state before:
pp: X S T : Scheme
f : X ⟶ S
g : T ⟶ S
inst✝² : IsAffine T
t : ↥T
inst✝¹ : Flat f
inst✝ : IsFinite f
i : Spec (S.affineOpenCover.X (S.affineOpenCover.idx (g t))) ⟶ S := ⋯
R : CommRingCat
u : Spec R ⟶ pullback i g
hu : IsOpenImmersion u
z : ↥(Spec R)
hyl : (pullback.fst (S.affineOpenCover.f (S.affineOpenCover.idx (g t))) g) (u z) = Exists.choose ⋯
hyr : (pullback.snd (S.affineOpenCover.f (S.affineOpenCover.idx (g t))) g) (u z) = t
⊢ finrank f (g t) = IsAffine.finrank (pullback.snd (pullback.snd f g) (u ≫ pullback.snd i g)) z

Tactic:
refine (IsAffine.finrank_of_isPullback _ _ ?_ ?_ ?_ _ _ ?_).symm

Goal state after:
case refine_1
X S T : Scheme
f : X ⟶ S
g : T ⟶ S
inst✝² : IsAffine T
t : ↥T
inst✝¹ : Flat f
inst✝ : IsFinite f
i : Spec (S.affineOpenCover.X (S.affineOpenCover.idx (g t))) ⟶ S := S.affineOpenCover.f (S.affineOpenCover.idx (g t))
R : CommRingCat
u : Spec R ⟶ pullback i g
hu : IsOpenImmersion u
z : ↥(Spec R)
hyl : (pullback.fst (S.affineOpenCover.f (S.affineOpenCover.idx (g t))) g) (u z) = Exists.choose ⋯
hyr : (pullback.snd (S.affineOpenCover.f (S.affineOpenCover.idx (g t))) g) (u z) = t
⊢ pullback (pullback.snd f g) (u ≫ pullback.snd i g) ⟶ pullback f (S.affineOpenCover.f (S.affineOpenCover.idx (g t)))

case refine_2
X S T : Scheme
f : X ⟶ S
g : T ⟶ S
inst✝² : IsAffine T
t : ↥T
inst✝¹ : Flat f
inst✝ : IsFinite f
i : Spec (S.affineOpenCover.X (S.affineOpenCover.idx (g t))) ⟶ S := S.affineOpenCover.f (S.affineOpenCover.idx (g t))
R : CommRingCat
u : Spec R ⟶ pullback i g
hu : IsOpenImmersion u
z : ↥(Spec R)
hyl : (pullback.fst (S.affineOpenCover.f (S.affineOpenCover.idx (g t))) g) (u z) = Exists.choose ⋯
hyr : (pullback.snd (S.affineOpenCover.f (S.affineOpenCover.idx (g t))) g) (u z) = t
⊢ Spec R ⟶ Spec (S.affineOpenCover.X (S.affineOpenCover.idx (g t)))

case refine_3
X S T : Scheme
f : X ⟶ S
g : T ⟶ S
inst✝² : IsAffine T
t : ↥T
inst✝¹ : Flat f
inst✝ : IsFinite f
i : Spec (S.affineOpenCover.X (S.affineOpenCover.idx (g t))) ⟶ S := S.affineOpenCover.f (S.affineOpenCover.idx (g t))
R : CommRingCat
u : Spec R ⟶ pullback i g
hu : IsOpenImmersion u
z : ↥(Spec R)
hyl : (pullback.fst (S.affineOpenCover.f (S.affineOpenCover.idx (g t))) g) (u z) = Exists.choose ⋯
hyr : (pullback.snd (S.affineOpenCover.f (S.affineOpenCover.idx (g t))) g) (u z) = t
⊢ IsPullback ?refine_1 (pullback.snd (pullback.snd f g) (u ≫ pullback.snd i g))
    (pullback.snd f (S.affineOpenCover.f (S.affineOpenCover.idx (g t)))) ?refine_2

case refine_4
X S T : Scheme
f : X ⟶ S
g : T ⟶ S
inst✝² : IsAffine T
t : ↥T
inst✝¹ : Flat f
inst✝ : IsFinite f
i : Spec (S.affineOpenCover.X (S.affineOpenCover.idx (g t))) ⟶ S := S.affineOpenCover.f (S.affineOpenCover.idx (g t))
R : CommRingCat
u : Spec R ⟶ pullback i g
hu : IsOpenImmersion u
z : ↥(Spec R)
hyl : (pullback.fst (S.affineOpenCover.f (S.affineOpenCover.idx (g t))) g) (u z) = Exists.choose ⋯
hyr : (pullback.snd (S.affineOpenCover.f (S.affineOpenCover.idx (g t))) g) (u z) = t
⊢ ?refine_2 z = Exists.choose ⋯
Module: Mathlib.AlgebraicGeometry.Morphisms.SmoothFiber

Goal state before:
pp: X✝ Y : Scheme
f✝ : X✝ ⟶ Y
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝¹ : LocallyOfFinitePresentation f
inst✝ : Flat f
h : ∀ (y : ↥(Spec R)), Smooth (Scheme.Hom.fiberToSpecResidueField f y)
⊢ Smooth f

Tactic:
wlog h : ∃ S, X = Spec S generalizing f X

Goal state after:
case inr
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝¹ : LocallyOfFinitePresentation f
inst✝ : Flat f
h✝ : ∀ (y : ↥(Spec R)), Smooth (Scheme.Hom.fiberToSpecResidueField f y)
this :
  ∀ {X : Scheme} (f : X ⟶ Spec R) [LocallyOfFinitePresentation f] [Flat f],
    (∀ (y : ↥(Spec R)), Smooth (Scheme.Hom.fiberToSpecResidueField f y)) → (∃ S, X = Spec S) → Smooth f
h : ¬∃ S, X = Spec S
⊢ Smooth f

X✝ Y : Scheme
f✝ : X✝ ⟶ Y
R : CommRingCat
X : Scheme
f : X ⟶ Spec R
inst✝¹ : LocallyOfFinitePresentation f
inst✝ : Flat f
h✝ : ∀ (y : ↥(Spec R)), Smooth (Scheme.Hom.fiberToSpecResidueField f y)
h : ∃ S, X = Spec S
⊢ Smooth f
Module: Mathlib.AlgebraicGeometry.PointsPi

Goal state before:
pp: ι : Type u
R : ι → CommRingCat
I : Ideal ((i : ι) → ↑(R i))
f : (∐ fun i ↦ Spec (R i)) ⟶ Spec (CommRingCat.of (((i : ι) → ↑(R i)) ⧸ I))
hf : f ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)) = sigmaSpec R
x : (i : ι) → ↑(R i)
hx : x ∈ I
i : ι
⊢ x i = 0 i

Tactic:
simpa [← Category.assoc, Ideal.Quotient.eq_zero_iff_mem.mpr hx] using
    congr((Spec.preimage (Sigma.ι (Spec <| R ·) i ≫ $hf)).hom x).symm

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 𝒜
f : A
z : ProjectiveSpectrum 𝒜
⊢ f ∉ z.asHomogeneousIdeal ↔ ∃ u ∈ Set.range fun i ↦ basicOpen 𝒜 ((GradedRing.proj 𝒜 i) f), z ∈ u

Tactic:
constructor <;> intro hz

Goal state after:
case mp
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
z : ProjectiveSpectrum 𝒜
hz : f ∉ z.asHomogeneousIdeal
⊢ ∃ u ∈ Set.range fun i ↦ basicOpen 𝒜 ((GradedRing.proj 𝒜 i) f), z ∈ u

case mpr
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
z : ProjectiveSpectrum 𝒜
hz : ∃ u ∈ Set.range fun i ↦ basicOpen 𝒜 ((GradedRing.proj 𝒜 i) f), z ∈ u
⊢ f ∉ z.asHomogeneousIdeal