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

Goal state before:
pp: 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.scaleRoots r).natDegree =
    r ^ (f.natDegree * g.natDegree) * f.resultant g

Tactic:
rw [resultant_eq_prod_eval _ _ _ le_rfl hf',
      resultant_eq_prod_eval _ _ _ le_rfl (hf'.scaleRoots _),
      roots_scaleRoots _ (isUnit_iff_ne_zero.mpr hr)]

Goal state after:
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).leadingCoeff ^ (g.scaleRoots r).natDegree *
      (Multiset.map (fun x ↦ eval x (g.scaleRoots r)) (Multiset.map (fun x ↦ r * x) f.roots)).prod =
    r ^ (f.natDegree * g.natDegree) * (f.leadingCoeff ^ g.natDegree * (Multiset.map (fun x ↦ eval x g) f.roots).prod)
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case inr.inr.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 : R[X]) (r : R),
    q ≠ 0 →
      g ≠ 0 →
        (q.scaleRoots r).resultant (g.scaleRoots r) q.natDegree g.natDegree =
          r ^ (q.natDegree * g.natDegree) * q.resultant g
g : S[X]
hf : f ≠ 0
hg : g ≠ 0
f' : R[X]
hf' : map φ f' = f
ef : f'.degree = f.degree
g' : R[X]
hg' : map φ g' = g
eg : g'.degree = g.degree
r : R
hfl : f.leadingCoeff = φ f'.leadingCoeff
hgl : g.leadingCoeff = φ g'.leadingCoeff
⊢ ((map φ f').scaleRoots (φ r)).resultant (g.scaleRoots (φ r)) (map φ f').natDegree g.natDegree =
    φ r ^ ((map φ f').natDegree * g.natDegree) * (map φ f').resultant g

Tactic:
← map_scaleRoots _ _ _ (by simpa [← hfl]),

Goal state after:
case inr.inr.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 : R[X]) (r : R),
    q ≠ 0 →
      g ≠ 0 →
        (q.scaleRoots r).resultant (g.scaleRoots r) q.natDegree g.natDegree =
          r ^ (q.natDegree * g.natDegree) * q.resultant g
g : S[X]
hf : f ≠ 0
hg : g ≠ 0
f' : R[X]
hf' : map φ f' = f
ef : f'.degree = f.degree
g' : R[X]
hg' : map φ g' = g
eg : g'.degree = g.degree
r : R
hfl : f.leadingCoeff = φ f'.leadingCoeff
hgl : g.leadingCoeff = φ g'.leadingCoeff
⊢ (map φ (f'.scaleRoots r)).resultant (g.scaleRoots (φ r)) (map φ f').natDegree g.natDegree =
    φ r ^ ((map φ f').natDegree * g.natDegree) * (map φ f').resultant g
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hg : g.natDegree ≠ 0
this :
  ∀ {R : Type u_1} [inst : CommRing R] (f g : R[X]),
    g.natDegree ≠ 0 →
      IsDomain R →
        (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
          g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g
hR : ¬IsDomain R
hf0 : ¬f = 0
hg0 : ¬g = 0
S : Type (max 0 u_1) := MvPolynomial R ℤ
φ : S →+* R := MvPolynomial.eval₂Hom (algebraMap ℤ R) id
hφ : Function.Surjective ⇑φ
f' : S[X]
hf' : map φ f' = f
ef : f'.degree = f.degree
g' : S[X]
hg' : map φ g' = g
eg : g'.degree = g.degree
hfl : f.leadingCoeff = φ f'.leadingCoeff
hgl : g.leadingCoeff = φ g'.leadingCoeff
⊢ ((map φ f').scaleRoots (φ g'.leadingCoeff)).resultant g.integralNormalization f'.natDegree g'.natDegree =
    φ g'.leadingCoeff ^ (f'.natDegree * (g'.natDegree - 1)) * (map φ f').resultant g f'.natDegree g'.natDegree

Tactic:
← map_scaleRoots _ _ _ (by simpa [← hfl]),

Goal state after:
case neg
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hg : g.natDegree ≠ 0
this :
  ∀ {R : Type u_1} [inst : CommRing R] (f g : R[X]),
    g.natDegree ≠ 0 →
      IsDomain R →
        (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
          g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g
hR : ¬IsDomain R
hf0 : ¬f = 0
hg0 : ¬g = 0
S : Type (max 0 u_1) := MvPolynomial R ℤ
φ : S →+* R := MvPolynomial.eval₂Hom (algebraMap ℤ R) id
hφ : Function.Surjective ⇑φ
f' : S[X]
hf' : map φ f' = f
ef : f'.degree = f.degree
g' : S[X]
hg' : map φ g' = g
eg : g'.degree = g.degree
hfl : f.leadingCoeff = φ f'.leadingCoeff
hgl : g.leadingCoeff = φ g'.leadingCoeff
⊢ (map φ (f'.scaleRoots g'.leadingCoeff)).resultant g.integralNormalization f'.natDegree g'.natDegree =
    φ g'.leadingCoeff ^ (f'.natDegree * (g'.natDegree - 1)) * (map φ f').resultant g f'.natDegree g'.natDegree
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
T : Type u_4
inst✝¹ : CommRing T
inst✝ : Algebra R T
f : 𝓡' →ₐ[R] S
g : S →ₐ[R] T
⊢ ↑(↑((homEquiv T m k hn p) (g.comp f))).1 = ↑((↑((homEquiv S m k hn p) f)).1.map ↑g)

Tactic:
simp [homEquiv, UniversalFactorizationRing.homEquiv, Polynomial.map_map]

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
T : Type u_4
inst✝¹ : CommRing T
inst✝ : Algebra R T
f : 𝓡' →ₐ[R] S
g : S →ₐ[R] T
⊢ map ↑((g.comp f).comp (IsScalarTower.toAlgHom R 𝓡 𝓡')) ↑(UniversalFactorizationRing.factor₁ m k hn p) =
    map ((↑g).comp ↑(f.comp (IsScalarTower.toAlgHom R 𝓡 𝓡'))) ↑(UniversalFactorizationRing.factor₁ m k hn p)
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
T : Type u_4
inst✝¹ : CommRing T
inst✝ : Algebra R T
f : 𝓡' →ₐ[R] S
g : S →ₐ[R] T
⊢ ↑(↑((homEquiv T m k hn p) (g.comp f))).2 = ↑((↑((homEquiv S m k hn p) f)).2.map ↑g)

Tactic:
simp [homEquiv, UniversalFactorizationRing.homEquiv, Polynomial.map_map]

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
T : Type u_4
inst✝¹ : CommRing T
inst✝ : Algebra R T
f : 𝓡' →ₐ[R] S
g : S →ₐ[R] T
⊢ map ↑((g.comp f).comp (IsScalarTower.toAlgHom R 𝓡 𝓡')) ↑(UniversalFactorizationRing.factor₂ m k hn p) =
    map ((↑g).comp ↑(f.comp (IsScalarTower.toAlgHom R 𝓡 𝓡'))) ↑(UniversalFactorizationRing.factor₂ m k hn p)
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
r : R
e : Fin ((C r).natDegree - 1 + (C r).natDegree) ≃ Fin 0 := finCongr ⋯
⊢ (C r).discr = 1

Tactic:
simp [discr, ← Matrix.det_reindex_self e]

Goal state after:
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'
⊢ ∃ 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:
let f := X * minpoly R s

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
⊢ ∃ 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.CategoryTheory.Monoidal.Cartesian.Grp

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
G : C
inst✝ : GrpObj G
⊢ μ = μ

Tactic:
change lift (fst G G) (snd G G) ≫ μ = μ

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
G : C
inst✝ : GrpObj G
⊢ lift (fst G G) (snd G G) ≫ μ = μ
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Grp

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : CartesianMonoidalCategory C
D : Type u_1
inst✝³ : Category.{v_1, u_1} D
inst✝² : CartesianMonoidalCategory D
F : C ⥤ D
inst✝¹ : F.Monoidal
X G : C
f : X ⟶ G
inst✝ : GrpObj G
⊢ F.map f⁻¹ = (F.map f)⁻¹

Tactic:
by
  rw [eq_inv_iff_mul_eq_one, ← Functor.map_mul, inv_mul_cancel, Functor.map_one]

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
T : Type u_3
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : FaithfullyFlat R T
inst✝ : Module.Finite T (T ⊗[R] M)
n : ℕ
s : Fin n → T ⊗[R] M
hs : Submodule.span T (Set.range s) = ⊤
k : Fin n → ℕ
t : (i : Fin n) → Fin (k i) → T
m : (i : Fin n) → Fin (k i) → M
h : ∀ (i : Fin n), s i = ∑ j, t i j ⊗ₜ[R] m i j
f₀ : ((i : Fin n) × Fin (k i) → R) →ₗ[R] M :=
  ((Pi.basisFun R ((i : Fin n) × Fin (k i))).constr R) fun x ↦
    match x with
    | ⟨i, j⟩ => m i j
⊢ ∀ (y : Fin n), s y ∈ ↑((AlgebraTensorModule.lTensor T T) f₀).range

Tactic:
intro i

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
T : Type u_3
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : FaithfullyFlat R T
inst✝ : Module.Finite T (T ⊗[R] M)
n : ℕ
s : Fin n → T ⊗[R] M
hs : Submodule.span T (Set.range s) = ⊤
k : Fin n → ℕ
t : (i : Fin n) → Fin (k i) → T
m : (i : Fin n) → Fin (k i) → M
h : ∀ (i : Fin n), s i = ∑ j, t i j ⊗ₜ[R] m i j
f₀ : ((i : Fin n) × Fin (k i) → R) →ₗ[R] M :=
  ((Pi.basisFun R ((i : Fin n) × Fin (k i))).constr R) fun x ↦
    match x with
    | ⟨i, j⟩ => m i j
i : Fin n
⊢ s i ∈ ↑((AlgebraTensorModule.lTensor T T) f₀).range
Module: Mathlib.RingTheory.Etale.Descent

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.FaithfullyFlat R T
inst✝ : Smooth T (T ⊗[R] S)
⊢ Smooth R S

Tactic:
by
  have : Algebra.FinitePresentation R S := .of_finitePresentation_tensorProduct_of_faithfullyFlat T
  refine ⟨?_, .of_finitePresentation_tensorProduct_of_faithfullyFlat T⟩
  rw [formallySmooth_iff]
  constructor
  · let _ : Algebra T (S ⊗[R] T) := TensorProduct.rightAlgebra
    let e : S ⊗[R] T ≃ₐ[T] T ⊗[R] S :=
      .ofRingEquiv (f := TensorProduct.comm R S T) <| by simp [RingHom.algebraMap_toAlgebra]
    have : FormallySmooth T (S ⊗[R] T) := .of_equiv e.symm
    let e' : (S ⊗[R] T) ⊗[S] Ω[S⁄R] ≃ₗ[S ⊗[R] T] Ω[S ⊗[R] T⁄T] :=
      KaehlerDifferential.tensorKaehlerEquiv R T S (S ⊗[R] T)
    have : Module.Flat (S ⊗[R] T) ((S ⊗[R] T) ⊗[S] Ω[S⁄R]) := .of_linearEquiv e'
    have : Module.Flat S Ω[S⁄R] := Module.Flat.of_flat_tensorProduct _ _ (S ⊗[R] T)
    exact Module.Flat.projective_of_finitePresentation
  · have : Subsingleton (T ⊗[R] H1Cotangent R S) := (tensorH1CotangentOfFlat R S T).subsingleton
    exact Module.FaithfullyFlat.lTensor_reflects_triviality R T (H1Cotangent R S)

Goal state after:
Module: Mathlib.AlgebraicGeometry.LimitsOver

Goal state before:
pp: X : Scheme
P : MorphismProperty Scheme
inst✝⁵ : IsZariskiLocalAtSource P
S : Scheme
J : Type u_1
inst✝⁴ : Category.{v_1, u_1} J
F : J ⥤ P.Over ⊤ S
inst✝³ : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f).left
inst✝² : (F ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).IsLocallyDirected
inst✝¹ : Quiver.IsThin J
inst✝ : Small.{u, u_1} J
this : HasColimit (F ⋙ MorphismProperty.Over.forget P ⊤ S)
e : (colimit (F ⋙ MorphismProperty.Over.forget P ⊤ S)).left ≅
  colimit ((F ⋙ MorphismProperty.Over.forget P ⊤ S) ⋙ Over.forget S) :=
  preservesColimitIso (Over.forget S) (F ⋙ MorphismProperty.Over.forget P ⊤ S)
𝒰 : (colimit (F ⋙ MorphismProperty.Over.forget P ⊤ S)).left.OpenCover :=
  Scheme.Cover.pushforwardIso
    (Scheme.IsLocallyDirected.openCover ((F ⋙ MorphismProperty.Over.forget P ⊤ S) ⋙ Over.forget S)) e.inv
⊢ ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ (colimit (F ⋙ MorphismProperty.Over.forget P ⊤ S)).hom)

Tactic:
intro i

Goal state after:
X : Scheme
P : MorphismProperty Scheme
inst✝⁵ : IsZariskiLocalAtSource P
S : Scheme
J : Type u_1
inst✝⁴ : Category.{v_1, u_1} J
F : J ⥤ P.Over ⊤ S
inst✝³ : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f).left
inst✝² : (F ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).IsLocallyDirected
inst✝¹ : Quiver.IsThin J
inst✝ : Small.{u, u_1} J
this : HasColimit (F ⋙ MorphismProperty.Over.forget P ⊤ S)
e : (colimit (F ⋙ MorphismProperty.Over.forget P ⊤ S)).left ≅
  colimit ((F ⋙ MorphismProperty.Over.forget P ⊤ S) ⋙ Over.forget S) :=
  preservesColimitIso (Over.forget S) (F ⋙ MorphismProperty.Over.forget P ⊤ S)
𝒰 : (colimit (F ⋙ MorphismProperty.Over.forget P ⊤ S)).left.OpenCover :=
  Scheme.Cover.pushforwardIso
    (Scheme.IsLocallyDirected.openCover ((F ⋙ MorphismProperty.Over.forget P ⊤ S) ⋙ Over.forget S)) e.inv
i : 𝒰.I₀
⊢ P (𝒰.f i ≫ (colimit (F ⋙ MorphismProperty.Over.forget P ⊤ S)).hom)
Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
S : StrictPseudofunctorCore B C
a✝ b✝ c✝ : B
f : a✝ ⟶ b✝
x✝¹ x✝ : b✝ ⟶ c✝
η : x✝¹ ⟶ x✝
⊢ S.map₂ (f ◁ η) = (eqToIso ⋯).hom ≫ S.map f ◁ S.map₂ η ≫ (eqToIso ⋯).inv

Tactic:
by
    simpa using S.map₂_whisker_left f η

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor

Goal state before:
pp: B : Type u₁
inst✝⁴ : Bicategory B
C : Type u₂
inst✝³ : Bicategory C
D : Type u₃
inst✝² : Bicategory D
inst✝¹ : Strict B
inst✝ : Strict C
S : StrictPseudofunctorPreCore B C
a✝ b✝ c✝ : B
f : a✝ ⟶ b✝
x✝¹ x✝ : b✝ ⟶ c✝
η : x✝¹ ⟶ x✝
⊢ S.map₂ (f ◁ η) = (eqToIso ⋯).hom ≫ S.map f ◁ S.map₂ η ≫ (eqToIso ⋯).inv

Tactic:
by
    simpa using S.map₂_whisker_left f η

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
S : StrictlyUnitaryPseudofunctorCore B C
a✝ b✝ c✝ : B
f : a✝ ⟶ b✝
x✝¹ x✝ : b✝ ⟶ c✝
η : x✝¹ ⟶ x✝
⊢ S.map₂ (f ◁ η) = (S.mapComp f x✝¹).hom ≫ S.map f ◁ S.map₂ η ≫ (S.mapComp f x✝).inv

Tactic:
by
    simpa using S.map₂_whisker_left f η

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✝¹ : Module.Flat R S
inst✝ : Module.Finite R S
⊢ Function.Surjective (comap (algebraMap R S)) ↔ Function.Injective ⇑(algebraMap R S)

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦
    have : FaithfulSMul R S := (faithfulSMul_iff_algebraMap_injective R S).mpr h
    Algebra.IsIntegral.comap_surjective _ _⟩
  apply injective_of_isLocalization_isMaximal (fun P _ ↦ Localization.AtPrime P)
    (fun P _ ↦ Localization.AtPrime P ⊗[R] S)
  intro p _
  rw [← faithfulSMul_iff_algebraMap_injective]
  obtain ⟨⟨Q, _⟩, hQ⟩ := h ⟨p, inferInstance⟩
  have : Q.LiesOver p := ⟨congr($(hQ).asIdeal).symm⟩
  let := Localization.AtPrime.algebraOfLiesOver p Q
  have : Nontrivial (Localization.AtPrime p ⊗[R] S) := by
    let f : Localization.AtPrime p ⊗[R] S →ₐ[R] Localization.AtPrime Q :=
      Algebra.TensorProduct.lift (IsScalarTower.toAlgHom R _ _)
        (IsScalarTower.toAlgHom R S _) (fun _ _ ↦ Commute.all _ _)
    exact f.domain_nontrivial
  infer_instance

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

Goal state before:
pp: R S : CommRingCat
x : ↥(Spec S)
φ : R ⟶ S
inst✝¹ : (CommRingCat.Hom.hom φ).Flat
inst✝ : (CommRingCat.Hom.hom φ).Finite
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom φ).toAlgebra
algebraizeInst✝¹ : Module.Flat ↑R ↑S
algebraizeInst✝ : Module.Finite ↑R ↑S
⊢ 1 ≤ (algebraMap ↑R ↑S).finrank ((Spec.map φ) x)

Tactic:
RingHom.finrank_algebraMap,

Goal state after:
R S : CommRingCat
x : ↥(Spec S)
φ : R ⟶ S
inst✝¹ : (CommRingCat.Hom.hom φ).Flat
inst✝ : (CommRingCat.Hom.hom φ).Finite
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom φ).toAlgebra
algebraizeInst✝¹ : Module.Flat ↑R ↑S
algebraizeInst✝ : Module.Finite ↑R ↑S
⊢ 1 ≤ Module.rankAtStalk (↑S) ((Spec.map φ) x)
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank

Goal state before:
pp: case refine_1.inr
X Y : Scheme
f : X ⟶ Y
inst✝¹ : Flat f
inst✝ : IsFinite f
h : 1 ≤ finrank f
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [Flat f] [IsFinite f], 1 ≤ finrank f → (∃ R, Y = Spec R) → Surjective f
hY : ¬∃ R, Y = Spec R
⊢ ∀ (i : Y.affineCover.toPreZeroHypercover.1), Surjective (Cover.pullbackHom Y.affineCover f i)

Tactic:
intro i

Goal state after:
case refine_1.inr
X Y : Scheme
f : X ⟶ Y
inst✝¹ : Flat f
inst✝ : IsFinite f
h : 1 ≤ finrank f
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [Flat f] [IsFinite f], 1 ≤ finrank f → (∃ R, Y = Spec R) → Surjective f
hY : ¬∃ R, Y = Spec R
i : Y.affineCover.toPreZeroHypercover.1
⊢ Surjective (Cover.pullbackHom Y.affineCover f i)
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
inst✝¹ : Flat f
inst✝ : IsFinite f
h : finrank f = 1
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [Flat f] [IsFinite f], finrank f = 1 → (∃ R, Y = Spec R) → IsIso f
hY : ¬∃ R, Y = Spec R
⊢ ∀ (i : Y.affineCover.toPreZeroHypercover.1),
    MorphismProperty.isomorphisms Scheme (Cover.pullbackHom Y.affineCover f i)

Tactic:
intro i

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝¹ : Flat f
inst✝ : IsFinite f
h : finrank f = 1
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [Flat f] [IsFinite f], finrank f = 1 → (∃ R, Y = Spec R) → IsIso f
hY : ¬∃ R, Y = Spec R
i : Y.affineCover.toPreZeroHypercover.1
⊢ MorphismProperty.isomorphisms Scheme (Cover.pullbackHom Y.affineCover f i)
Module: Mathlib.AlgebraicGeometry.Morphisms.SmoothFiber

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
inst✝¹ : LocallyOfFinitePresentation f
inst✝ : Flat f
h✝ : ∀ (y : ↥Y), Smooth (Scheme.Hom.fiberToSpecResidueField f y)
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [LocallyOfFinitePresentation f] [Flat f],
    (∀ (y : ↥Y), Smooth (Scheme.Hom.fiberToSpecResidueField f y)) → (∃ R, Y = Spec R) → Smooth f
h : ¬∃ R, Y = Spec R
⊢ ∀ (i : Y.affineCover.toPreZeroHypercover.1), Smooth (Scheme.Cover.pullbackHom Y.affineCover f i)

Tactic:
intro i

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝¹ : LocallyOfFinitePresentation f
inst✝ : Flat f
h✝ : ∀ (y : ↥Y), Smooth (Scheme.Hom.fiberToSpecResidueField f y)
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [LocallyOfFinitePresentation f] [Flat f],
    (∀ (y : ↥Y), Smooth (Scheme.Hom.fiberToSpecResidueField f y)) → (∃ R, Y = Spec R) → Smooth f
h : ¬∃ R, Y = Spec R
i : Y.affineCover.toPreZeroHypercover.1
⊢ Smooth (Scheme.Cover.pullbackHom Y.affineCover f i)
Module: Mathlib.AlgebraicGeometry.Morphisms.SmoothFiber

Goal state before:
pp: 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
⊢ ∀ (i : X.affineCover.I₀), Smooth (X.affineCover.f i ≫ f)

Tactic:
intro i

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
i : X.affineCover.I₀
⊢ Smooth (X.affineCover.f i ≫ f)
Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
σ : Type u_3
a✝ : Nontrivial R
h✝ : Infinite σ
n : ℕ
ι : Fin (n + 1) → σ := ⋯
this : Function.Surjective (Function.invFun ι)
⊢ ↑n ≤ ↑n + 1

Tactic:
norm_cast

Goal state after:
R : Type u_1
inst✝ : CommRing R
σ : Type u_3
a✝ : Nontrivial R
h✝ : Infinite σ
n : ℕ
ι : Fin (n + 1) → σ := ⇑(Infinite.natEmbedding σ) ∘ Fin.val
this : Function.Surjective (Function.invFun ι)
⊢ n ≤ n + 1
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
c d : B
l₁ l₂ l₃ : c ⟶ d
r₁ r₂ r₃ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
α : r₁ ⟶ r₂
β : r₂ ⟶ r₃
⊢ (conjugateEquiv adj₂ adj₃).symm β ≫ (conjugateEquiv adj₁ adj₂).symm α = (conjugateEquiv adj₁ adj₃).symm (α ≫ β)

Tactic:
rw [Equiv.eq_symm_apply, ← conjugateEquiv_comp _ adj₂]

Goal state after:
B : Type u
inst✝ : Bicategory B
c d : B
l₁ l₂ l₃ : c ⟶ d
r₁ r₂ r₃ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
α : r₁ ⟶ r₂
β : r₂ ⟶ r₃
⊢ (conjugateEquiv adj₁ adj₂) ((conjugateEquiv adj₁ adj₂).symm α) ≫
      (conjugateEquiv adj₂ adj₃) ((conjugateEquiv adj₂ adj₃).symm β) =
    α ≫ β
Module: Mathlib.RingTheory.GradedAlgebra.Radical

Goal state before:
pp: case I_ne_top
ι : 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
h : I.IsPrime
⊢ (Ideal.homogeneousCore 𝒜 I).toIdeal ≠ ⊤

pp: case homogeneous_mem_or_mem
ι : 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
h : I.IsPrime
⊢ ∀ {x y : A},
    IsHomogeneousElem 𝒜 x →
      IsHomogeneousElem 𝒜 y →
        x * y ∈ (Ideal.homogeneousCore 𝒜 I).toIdeal →
          x ∈ (Ideal.homogeneousCore 𝒜 I).toIdeal ∨ y ∈ (Ideal.homogeneousCore 𝒜 I).toIdeal

Tactic:
· exact ne_top_of_le_ne_top h.ne_top (Ideal.toIdeal_homogeneousCore_le 𝒜 I)

Goal state after:
case homogeneous_mem_or_mem
ι : 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
h : I.IsPrime
⊢ ∀ {x y : A},
    IsHomogeneousElem 𝒜 x →
      IsHomogeneousElem 𝒜 y →
        x * y ∈ (Ideal.homogeneousCore 𝒜 I).toIdeal →
          x ∈ (Ideal.homogeneousCore 𝒜 I).toIdeal ∨ y ∈ (Ideal.homogeneousCore 𝒜 I).toIdeal
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
z : HomogeneousLocalization 𝒜 x
n : ℕ
c1 c2 : NumDenSameDeg 𝒜 x
h : Localization.mk ↑c1.num ⟨↑c1.den, ⋯⟩ = Localization.mk ↑c2.num ⟨↑c2.den, ⋯⟩
⊢ (Setoid.ker (embedding 𝒜 x)) (c1 ^ n) (c2 ^ n)

Tactic:
change Localization.mk _ _ = Localization.mk _ _
          simp only [num_pow, den_pow]
          convert! congr_arg (fun z : at x => z ^ n) h <;> rw [Localization.mk_pow] <;> rfl

Goal state after:
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
x : ↑(Proj.restrict ⋯).toTopCat
⊢ (carrier x).IsPrime

Tactic:
refine Ideal.IsPrime.comap _ (hK := ?_)

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
x : ↑(Proj.restrict ⋯).toTopCat
⊢ (Ideal.map (algebraMap A (Away f)) (↑x).asHomogeneousIdeal.toIdeal).IsPrime