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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : IsStandardEtale R S
Sₛ : Type u_4
inst✝⁴ : CommRing Sₛ
inst✝³ : Algebra S Sₛ
inst✝² : Algebra R Sₛ
inst✝¹ : IsScalarTower R S Sₛ
s : S
inst✝ : IsLocalization.Away s Sₛ
P : StandardEtalePresentation R S
p : R[X]
n : ℕ
hp : s * (aeval P.x) P.g ^ n = (aeval P.x) p
P' : StandardEtalePair R := { f := P.f, monic_f := ⋯, g := p * P.g, cond := ⋯ }
S' : Type u_1 := Localization.Away ((AdjoinRoot.mk P.f) P.g)
e : S ≃ₐ[R] S' := P.equivRing.trans P.equivAwayAdjoinRoot
this✝ :
  IsLocalization.Away ((AdjoinRoot.mk P.f) (p * P.g))
    (Localization.Away ((algebraMap (AdjoinRoot P.f) S') ((AdjoinRoot.mk P.f) p)))
H :
  Submonoid.map e.symm.toRingEquiv.toMonoidHom
      (Submonoid.powers ((algebraMap (AdjoinRoot P.f) S') ((AdjoinRoot.mk P.f) p))) =
    Submonoid.powers ((aeval P.x) p)
this : IsLocalization.Away ((aeval P.x) p) Sₛ
e₁ : P'.Ring ≃ₐ[R] Localization.Away ((algebraMap (AdjoinRoot P.f) S') ((AdjoinRoot.mk P.f) p)) :=
  P'.equivAwayAdjoinRoot.trans
    (AlgEquiv.restrictScalars R
      (IsLocalization.algEquiv (Submonoid.powers ((AdjoinRoot.mk P.f) (p * P.g)))
        (Localization.Away ((AdjoinRoot.mk P.f) (p * P.g)))
        (Localization.Away ((algebraMap (AdjoinRoot P.f) S') ((AdjoinRoot.mk P.f) p)))))
e₂ : Localization.Away ((algebraMap (AdjoinRoot P.f) S') ((AdjoinRoot.mk P.f) p)) ≃ₐ[R] Sₛ :=
  let __spread.0 :=
    IsLocalization.ringEquivOfRingEquiv (Localization.Away ((algebraMap (AdjoinRoot P.f) S') ((AdjoinRoot.mk P.f) p)))
      Sₛ e.symm.toRingEquiv H;
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
⊢ IsStandardEtale R Sₛ

Tactic:
exact .of_equiv (e₁.trans e₂)

Goal state after:
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: case inr
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
φ : R[X] →ₐ[R] S
t : S
p : R[X]
hRS : integralClosure R S = ⊥
hφ : φ.Finite
hp : φ p * t ∈ (conductor R (φ X)).radical
i : ℕ
this :
  ∀ (p : R[X]),
    φ p * t ∈ (conductor R (φ X)).radical → ∀ (i : ℕ), i = p.natDegree → p.coeff i • t ∈ (conductor R (φ X)).radical
⊢ p.coeff i • t ∈ (conductor R (φ X)).radical

Tactic:
simp only [forall_eq, coeff_natDegree] at this

Goal state after:
case inr
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
φ : R[X] →ₐ[R] S
t : S
p : R[X]
hRS : integralClosure R S = ⊥
hφ : φ.Finite
hp : φ p * t ∈ (conductor R (φ X)).radical
i : ℕ
this : ∀ (p : R[X]), φ p * t ∈ (conductor R (φ X)).radical → p.leadingCoeff • t ∈ (conductor R (φ X)).radical
⊢ p.coeff i • t ∈ (conductor R (φ X)).radical
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
f g : R[X]
m n : ℕ
φ : R →+* S
⊢ (map φ f).sylvester (map φ g) m n = φ.mapMatrix (f.sylvester g m n)

Tactic:
by
  ext i j; induction j using Fin.addCases <;> simp [sylvester, apply_ite φ]

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

Goal state before:
pp: case neg.inl
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : 0 < f.natDegree
hn : ¬f.natDegree = 0
i : ℕ
hi : i < f.natDegree - 1 + f.natDegree
j : ℕ
hj : j < f.natDegree - 1 + f.natDegree
hi' : i ≠ 2 * f.natDegree - 2
⊢ ((derivative f).sylvester f (f.natDegree - 1) f.natDegree).updateRow ⟨2 * f.natDegree - 2, ⋯⟩
      (fun j ↦ if ↑j = f.natDegree - 2 then 1 else if ↑j = 2 * f.natDegree - 2 then ↑f.natDegree else 0) ⟨i, hi⟩
      ⟨j, hj⟩ =
    (derivative f).sylvester f (f.natDegree - 1) f.natDegree ⟨i, hi⟩ ⟨j, hj⟩

Tactic:
Matrix.updateRow_ne (Fin.ne_of_val_ne hi')

Goal state after:
case neg.inl
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : 0 < f.natDegree
hn : ¬f.natDegree = 0
i : ℕ
hi : i < f.natDegree - 1 + f.natDegree
j : ℕ
hj : j < f.natDegree - 1 + f.natDegree
hi' : i ≠ 2 * f.natDegree - 2
⊢ (derivative f).sylvester f (f.natDegree - 1) f.natDegree ⟨i, hi⟩ ⟨j, hj⟩ =
    (derivative f).sylvester f (f.natDegree - 1) f.natDegree ⟨i, hi⟩ ⟨j, hj⟩
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝² : QuasiCompact f
inst✝¹ : QuasiSeparated f
inst✝ : IsIntegralHom f
U : (normalizationOpenCover f).toPreZeroHypercover.1
e : pullback (toNormalization f) ((normalizationOpenCover f).f U) ≅ ↑(f ⁻¹ᵁ ↑U) :=
  IsOpenImmersion.isoOfRangeEq (pullback.fst (toNormalization f) ((normalizationOpenCover f).f U)) (f ⁻¹ᵁ ↑U).ι ⋯
this : Algebra ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U) := (CommRingCat.Hom.hom (app f ↑U)).toAlgebra
⊢ (CommRingCat.Hom.hom (app f ↑U)).IsIntegral

Tactic:
exact IsIntegralHom.isIntegral_app _ _ U.2

Goal state after:
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : FiniteType R S
q : PrimeSpectrum S
H : IsOpen {⟨q, ⋯⟩}
p : PrimeSpectrum R := PrimeSpectrum.comap (algebraMap R S) q
⊢ QuasiFiniteAt R q.asIdeal

Tactic:
let e := PrimeSpectrum.preimageHomeomorphFiber R S p

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : FiniteType R S
q : PrimeSpectrum S
H : IsOpen {⟨q, ⋯⟩}
p : PrimeSpectrum R := PrimeSpectrum.comap (algebraMap R S) q
e : ↑(PrimeSpectrum.comap (algebraMap R S) ⁻¹' {p}) ≃ₜ PrimeSpectrum (p.asIdeal.Fiber S) :=
  PrimeSpectrum.preimageHomeomorphFiber R S p
⊢ QuasiFiniteAt R q.asIdeal
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : FiniteType R S
q : PrimeSpectrum S
H : QuasiFiniteAt R q.asIdeal
p : PrimeSpectrum R := PrimeSpectrum.comap (algebraMap R S) q
⊢ IsOpen {⟨q, ⋯⟩}

Tactic:
let e := PrimeSpectrum.preimageHomeomorphFiber R S p

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : FiniteType R S
q : PrimeSpectrum S
H : QuasiFiniteAt R q.asIdeal
p : PrimeSpectrum R := PrimeSpectrum.comap (algebraMap R S) q
e : ↑(PrimeSpectrum.comap (algebraMap R S) ⁻¹' {p}) ≃ₜ PrimeSpectrum (p.asIdeal.Fiber S) :=
  PrimeSpectrum.preimageHomeomorphFiber R S p
⊢ IsOpen {⟨q, ⋯⟩}
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
n : ℕ
inst✝ : Nontrivial R
⊢ (freeMonic R n).coeff n ≠ 0

Tactic:
by simp [coeff_freeMonic]

Goal state after:
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
⊢ (fromTensor m k hn p) (MvPolynomial.universalFactorizationMapPresentation R n m k hn).jacobian =
    (-1) ^ n * (↑(factor₁ m k hn p)).resultant ↑(factor₂ m k hn p)

Tactic:
MvPolynomial.universalFactorizationMapPresentation_jacobian

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
⊢ (fromTensor m k hn p)
      ((-1) ^ n *
        (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)
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

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

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

Tactic:
· simp [hx0]

Goal state after:
case neg
R✝ : Type u_1
inst✝¹ : CommRing R✝
R : Type u_1
inst✝ : Field R
f : R[X]
g : R[X]
r : R
x y : R[X]
hx : x ∈ Submonoid.closure ({x | ∃ a, C a = x} ∪ {x | ∃ a, X + C a = x})
hy : y ∈ Submonoid.closure ({x | ∃ a, C a = x} ∪ {x | ∃ a, X + C a = x})
hx' : ((taylor r) x).resultant ((taylor r) g) = x.resultant g
hy' : ((taylor r) y).resultant ((taylor r) g) = y.resultant g
hx0 : ¬x = 0
⊢ ((taylor r) (x * y)).resultant ((taylor r) g) = (x * y).resultant g
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Grp

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : CartesianMonoidalCategory C
M G H X Y : C
inst✝² : MonObj M
inst✝¹ : GrpObj G
inst✝ : GrpObj H
F : Cᵒᵖ ⥤ GrpCat
α : (F ⋙ forget GrpCat).RepresentableBy X
⊢ lift (α.homEquiv'.symm (α.homEquiv (𝟙 X))⁻¹) (𝟙 X) ≫ μ = toUnit X ≫ η

Tactic:
change lift (α.homEquiv'.symm (α.homEquiv (𝟙 X))⁻¹) (𝟙 X) ≫
      α.homEquiv'.symm (α.homEquiv' (fst X X) * α.homEquiv' (snd X X)) =
        toUnit X ≫ α.homEquiv'.symm 1

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : CartesianMonoidalCategory C
M G H X Y : C
inst✝² : MonObj M
inst✝¹ : GrpObj G
inst✝ : GrpObj H
F : Cᵒᵖ ⥤ GrpCat
α : (F ⋙ forget GrpCat).RepresentableBy X
⊢ lift (α.homEquiv'.symm (α.homEquiv (𝟙 X))⁻¹) (𝟙 X) ≫
      α.homEquiv'.symm (α.homEquiv' (fst X X) * α.homEquiv' (snd X X)) =
    toUnit X ≫ α.homEquiv'.symm 1
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
this : Function.Surjective ⇑((AlgebraTensorModule.lTensor T T) f₀)
⊢ Function.Surjective ⇑f₀

Tactic:
rwa [← Module.FaithfullyFlat.lTensor_surjective_iff_surjective _ T]

Goal state after:
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
⊢ f.range ≤ Ideal.map (algebraMap R S) I

Tactic:
rintro - ⟨x, rfl⟩

Goal state after:
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
Module: Mathlib.RingTheory.Finiteness.Descent

Goal state before:
pp: ⊢ CodescendsAlong (fun {R S} [CommRing R] [CommRing S] ↦ Finite) fun {R S} [CommRing R] [CommRing S] ↦ FaithfullyFlat

Tactic:
refine .mk _ finite_respectsIso fun R S T _ _ _ _ _ h h' ↦ ?_

Goal state after:
R S T : Type u_4
x✝⁴ : CommRing R
x✝³ : CommRing S
x✝² : CommRing T
x✝¹ : Algebra R S
x✝ : Algebra R T
h : (algebraMap R S).FaithfullyFlat
h' : (algebraMap S (S ⊗[R] T)).Finite
⊢ (algebraMap R T).Finite
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)
this : FinitePresentation R S
⊢ FormallySmooth R S

Tactic:
formallySmooth_iff

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u_3
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Module.FaithfullyFlat R T
inst✝ : Smooth T (T ⊗[R] S)
this : FinitePresentation R S
⊢ Module.Projective S Ω[S⁄R] ∧ Subsingleton (H1Cotangent R S)
Module: Mathlib.RingTheory.Etale.Descent

Goal state before:
pp: case left
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)
this : FinitePresentation R S
⊢ Module.Projective S Ω[S⁄R]

Tactic:
let _ : Algebra T (S ⊗[R] T) := TensorProduct.rightAlgebra

Goal state after:
case left
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)
this : FinitePresentation R S
x✝ : Algebra T (S ⊗[R] T) := TensorProduct.rightAlgebra
⊢ Module.Projective S Ω[S⁄R]
Module: Mathlib.AlgebraicGeometry.Group.Affine

Goal state before:
pp: R : CommRingCat
⊢ (preservesTerminalIso (algSpec R)).hom = (Over.isoMk (Iso.refl (Spec R)) ⋯).hom

Tactic:
exact toUnit_unique ..

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

Goal state before:
pp: X S Y : Scheme
f : X ⟶ Y
g : Y ⟶ S
inst✝² : IsIso f
inst✝¹ : Flat g
inst✝ : IsFinite g
z : ↥S
e : pullback (f ≫ g) (S.affineOpenCover.f (S.affineOpenCover.idx z)) ≅
  pullback g (S.affineOpenCover.f (S.affineOpenCover.idx z)) :=
  (pullbackRightPullbackFstIso g (S.affineOpenCover.f (S.affineOpenCover.idx z)) f).symm ≪≫
    asIso (pullback.snd f (pullback.fst g (S.affineOpenCover.f (S.affineOpenCover.idx z))))
this :
  e.hom ≫ pullback.snd g (S.affineOpenCover.f (S.affineOpenCover.idx z)) =
    pullback.snd (f ≫ g) (S.affineOpenCover.f (S.affineOpenCover.idx z))
⊢ finrank (f ≫ g) z = finrank g z

Tactic:
finrank,

Goal state after:
X S Y : Scheme
f : X ⟶ Y
g : Y ⟶ S
inst✝² : IsIso f
inst✝¹ : Flat g
inst✝ : IsFinite g
z : ↥S
e : pullback (f ≫ g) (S.affineOpenCover.f (S.affineOpenCover.idx z)) ≅
  pullback g (S.affineOpenCover.f (S.affineOpenCover.idx z)) :=
  (pullbackRightPullbackFstIso g (S.affineOpenCover.f (S.affineOpenCover.idx z)) f).symm ≪≫
    asIso (pullback.snd f (pullback.fst g (S.affineOpenCover.f (S.affineOpenCover.idx z))))
this :
  e.hom ≫ pullback.snd g (S.affineOpenCover.f (S.affineOpenCover.idx z)) =
    pullback.snd (f ≫ g) (S.affineOpenCover.f (S.affineOpenCover.idx z))
⊢ IsAffine.finrank (pullback.snd (f ≫ g) (S.affineOpenCover.f (S.affineOpenCover.idx z))) (Exists.choose ⋯) =
    finrank g z
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank

Goal state before:
pp: X S Y : Scheme
f : X ⟶ Y
g : Y ⟶ S
inst✝² : IsIso f
inst✝¹ : Flat g
inst✝ : IsFinite g
z : ↥S
e : pullback (f ≫ g) (S.affineOpenCover.f (S.affineOpenCover.idx z)) ≅
  pullback g (S.affineOpenCover.f (S.affineOpenCover.idx z)) :=
  (pullbackRightPullbackFstIso g (S.affineOpenCover.f (S.affineOpenCover.idx z)) f).symm ≪≫
    asIso (pullback.snd f (pullback.fst g (S.affineOpenCover.f (S.affineOpenCover.idx z))))
this :
  e.hom ≫ pullback.snd g (S.affineOpenCover.f (S.affineOpenCover.idx z)) =
    pullback.snd (f ≫ g) (S.affineOpenCover.f (S.affineOpenCover.idx z))
⊢ IsAffine.finrank (pullback.snd (f ≫ g) (S.affineOpenCover.f (S.affineOpenCover.idx z))) (Exists.choose ⋯) =
    finrank g z

Tactic:
finrank,

Goal state after:
X S Y : Scheme
f : X ⟶ Y
g : Y ⟶ S
inst✝² : IsIso f
inst✝¹ : Flat g
inst✝ : IsFinite g
z : ↥S
e : pullback (f ≫ g) (S.affineOpenCover.f (S.affineOpenCover.idx z)) ≅
  pullback g (S.affineOpenCover.f (S.affineOpenCover.idx z)) :=
  (pullbackRightPullbackFstIso g (S.affineOpenCover.f (S.affineOpenCover.idx z)) f).symm ≪≫
    asIso (pullback.snd f (pullback.fst g (S.affineOpenCover.f (S.affineOpenCover.idx z))))
this :
  e.hom ≫ pullback.snd g (S.affineOpenCover.f (S.affineOpenCover.idx z)) =
    pullback.snd (f ≫ g) (S.affineOpenCover.f (S.affineOpenCover.idx z))
⊢ IsAffine.finrank (pullback.snd (f ≫ g) (S.affineOpenCover.f (S.affineOpenCover.idx z))) (Exists.choose ⋯) =
    IsAffine.finrank (pullback.snd g (S.affineOpenCover.f (S.affineOpenCover.idx z))) (Exists.choose ⋯)
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 ≤ Module.rankAtStalk (↑S) ((Spec.map φ) x)

Tactic:
Nat.add_one_le_iff,

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
⊢ 0 < Module.rankAtStalk (↑S) ((Spec.map φ) x)
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
⊢ 0 < Module.rankAtStalk (↑S) ((Spec.map φ) x)

Tactic:
PrimeSpectrum.rankAtStalk_pos_iff_mem_range_comap

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
⊢ (Spec.map φ) x ∈ Set.range (PrimeSpectrum.comap (algebraMap ↑R ↑S))
Module: Mathlib.AlgebraicGeometry.OrderOfVanishing

Goal state before:
pp: X : Scheme
inst✝¹ : IsIntegral X
inst✝ : IsLocallyNoetherian X
x : ↥X
hx : coheight x = 1
f : ↑X.functionField
hf : f ≠ 0
n : ℤ
⊢ n ≤ ord f x ↔ ↑(Multiplicative.ofAdd n) ≤ (ordHom x hx) f

Tactic:
ord_eq_unzero_ordHom hx hf

Goal state after:
X : Scheme
inst✝¹ : IsIntegral X
inst✝ : IsLocallyNoetherian X
x : ↥X
hx : coheight x = 1
f : ↑X.functionField
hf : f ≠ 0
n : ℤ
⊢ n ≤ Multiplicative.toAdd (unzero ⋯) ↔ ↑(Multiplicative.ofAdd n) ≤ (ordHom x hx) f
Module: Mathlib.AlgebraicGeometry.PointsPi

Goal state before:
pp: ι : Type u
R : ι → CommRingCat
U : (Spec (CommRingCat.of ((i : ι) → ↑(R i)))).Opens
V : Set ↥(Spec (CommRingCat.of ((i : ι) → ↑(R i))))
hV : ↑(Scheme.Hom.opensRange (sigmaSpec R)) ⊆ V
hV' : IsCompact V
hVU : V ⊆ ↑U
s : Set ↑(CommRingCat.of ((i : ι) → ↑(R i)))
hs : U.carrierᶜ = zeroLocus s
⊢ V ⊆ ⋃ i, (basicOpen ↑i).carrier

Tactic:
simpa [← Set.compl_iInter, ← zeroLocus_iUnion₂ (κ := (· ∈ s)), ← hs]

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 𝒜
⊢ vanishingIdeal ∅ = ⊤

Tactic:
by
  simpa using! (gc_ideal _).u_top

Goal state after:
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
⊢ ∃ s, Algebra.adjoin ↥(𝒜 0) ↑s = ⊤ ∧ ∀ i ∈ s, SetLike.IsHomogeneousElem 𝒜 i

Tactic:
obtain ⟨F, hF⟩ := Algebra.FiniteType.out (R := 𝒜 0) (A := S)

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 = ⊤
⊢ ∃ s, Algebra.adjoin ↥(𝒜 0) ↑s = ⊤ ∧ ∀ i ∈ s, SetLike.IsHomogeneousElem 𝒜 i
Module: Mathlib.Data.FunLike.Graded

Goal state before:
pp: E : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_4
τ : Type u_5
ι : Type u_6
inst✝³ : SetLike σ A
inst✝² : SetLike τ B
𝒜 : ι → σ
ℬ : ι → τ
inst✝¹ : EquivLike E A B
inst✝ : GradedEquivLike E 𝒜 ℬ
e : E
i : ι
y : ↥(ℬ i)
⊢ e (EquivLike.inv e ↑y) ∈ ℬ i

Tactic:
EquivLike.apply_inv_apply

Goal state after:
E : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_4
τ : Type u_5
ι : Type u_6
inst✝³ : SetLike σ A
inst✝² : SetLike τ B
𝒜 : ι → σ
ℬ : ι → τ
inst✝¹ : EquivLike E A B
inst✝ : GradedEquivLike E 𝒜 ℬ
e : E
i : ι
y : ↥(ℬ i)
⊢ ↑y ∈ ℬ i
Module: Mathlib.AlgebraicGeometry.Modules.Sheaf

Goal state before:
pp: X : Scheme
M N : X.Modules
f g : M ⟶ N
H : ∀ (U : X.Opens), Hom.app f U = Hom.app g U
⊢ f = g

Tactic:
by
  apply SheafOfModules.hom_ext
  ext U x
  exact congr($(H U.unop) x)

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)ᵒᵖ
⊢ ((SheafOfModules.forget X.ringCatSheaf).obj (restrict (unit Y.ringCatSheaf) f)).obj U ≅
    ((SheafOfModules.forget X.ringCatSheaf).obj (unit X.ringCatSheaf)).obj U

Tactic:
refine ModuleCat.isoMk
      ((forget₂ CommRingCat RingCat ⋙ forget₂ _ Ab).mapIso (f.appIso U.unop)) ?_

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.ringCatSheaf.obj.obj U)),
    ((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 =
      (((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