mathlib-initiative/mathlib-tactics huggingface dataset:
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
φ : R[X] →ₐ[R] S
t : S
p : R[X]
hRS : integralClosure R S = ⊥
hφ : φ.Finite
hp : φ p * t ∈ conductor R (φ X)
⊢ ∃ n, p.leadingCoeff ^ n • t ∈ conductor R (φ X)

Tactic:
algebraize [φ.toRingHom]
  have : IsScalarTower R R[X] S := .of_algebraMap_eq' φ.comp_algebraMap.symm
  have (x : _) : ∃ n, p.leadingCoeff ^ n • (t * x) ∈ φ.range := by
    have : φ p * t * x ∈ φ.range := by simpa [← AlgHom.map_adjoin_singleton] using hp x
    obtain ⟨q, n, hn⟩ :=
      exists_isIntegral_leadingCoeff_pow_smul_sub_of_isIntegralElem_of_mul_mem_range φ _ p
        (hφ.to_isIntegral (t * x)) (by convert! this using 1; ring)
    obtain ⟨r, hr : algebraMap _ _ r = _⟩ := hRS.le hn
    exact ⟨n, (C r + q), by simp [← Polynomial.algebraMap_eq, -Polynomial.algebraMap_apply, hr]⟩
  choose n hn using this
  obtain ⟨s, hs⟩ := Module.Finite.fg_top (R := R[X]) (M := S)
  refine ⟨s.sup n, fun x ↦ ?_⟩
  rw [← AlgHom.map_adjoin_singleton, adjoin_X, Algebra.map_top, Algebra.smul_mul_assoc]
  induction hs.ge (Set.mem_univ x) using Submodule.span_induction with
  | mem x h =>
    rw [← Nat.sub_add_cancel (s.le_sup h), pow_add, mul_smul]
    exact Subalgebra.smul_mem _ (hn _) _
  | zero => simp
  | add x y _ _ hx hy => simpa only [mul_add, smul_add] using add_mem hx hy
  | smul a x hx IH =>
    rw [mul_smul_comm, smul_comm, Algebra.smul_def]
    exact mul_mem (AlgHom.mem_range_self _ _) IH

Goal state after:
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
Q : Ideal S
inst✝² : Q.IsPrime
inst✝¹ : Module.Finite R S
inst✝ : IsUnramifiedAt R Q
this : Algebra (Localization.AtPrime (Ideal.under R Q)) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R Q) Q
t : S
htQ : t ∉ Q
htQ' : ∀ Q' ∈ (Ideal.under R Q).primesOver S, Q' ≠ Q → t ∈ Q'
ht : (Ideal.under R Q).ResidueField[(algebraMap S Q.ResidueField) t] = ⊤
⊢ ∃ x,
    (Ideal.under (↥R[x]) Q).primesOver S = {Q} ∧
      Function.Bijective ⇑(algebraMap (Ideal.under (↥R[x]) Q).ResidueField Q.ResidueField)

Tactic:
let p := Q.under R

Goal state after:
R : Type u_1
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
Q : Ideal S
inst✝² : Q.IsPrime
inst✝¹ : Module.Finite R S
inst✝ : IsUnramifiedAt R Q
this : Algebra (Localization.AtPrime (Ideal.under R Q)) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R Q) Q
t : S
htQ : t ∉ Q
htQ' : ∀ Q' ∈ (Ideal.under R Q).primesOver S, Q' ≠ Q → t ∈ Q'
ht : (Ideal.under R Q).ResidueField[(algebraMap S Q.ResidueField) t] = ⊤
p : Ideal R := Ideal.under R Q
⊢ ∃ x,
    (Ideal.under (↥R[x]) Q).primesOver S = {Q} ∧
      Function.Bijective ⇑(algebraMap (Ideal.under (↥R[x]) Q).ResidueField Q.ResidueField)
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: case pos.refine_1
R✝ S✝ : Type u
inst✝⁷ : CommRing R✝
inst✝⁶ : CommRing S✝
inst✝⁵ : Algebra R✝ S✝
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal S
inst✝¹ : p.IsPrime
inst✝ : WeaklyQuasiFiniteAt R p
x : S
hx : R[x] = ⊤
H : integralClosure R S = ⊥
H₀ : Function.Surjective ⇑(aeval x)
f : R[X]
hf : (aeval x) f = 0
n : ℕ
hfn : (algebraMap R S) (f.coeff n) ∉ p
m : ℕ
IH :
  ∀ m_1 < m + 1,
    ∀ (f : R[X]),
      (aeval x) f = 0 → ∀ (n : ℕ), (algebraMap R S) (f.coeff n) ∉ p → f.natDegree = m_1 → ZariskisMainProperty R p
hm : f.natDegree = m + 1
Hfp : (algebraMap R S) f.leadingCoeff ∈ p
a : R
ha : (ofId R S).toRingHom a = f.leadingCoeff • x
⊢ (f.eraseLead + C a * X ^ m).natDegree < m + 1

Tactic:
suffices f.eraseLead.natDegree ≤ m by compute_degree!

Goal state after:
case pos.refine_1
R✝ S✝ : Type u
inst✝⁷ : CommRing R✝
inst✝⁶ : CommRing S✝
inst✝⁵ : Algebra R✝ S✝
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal S
inst✝¹ : p.IsPrime
inst✝ : WeaklyQuasiFiniteAt R p
x : S
hx : R[x] = ⊤
H : integralClosure R S = ⊥
H₀ : Function.Surjective ⇑(aeval x)
f : R[X]
hf : (aeval x) f = 0
n : ℕ
hfn : (algebraMap R S) (f.coeff n) ∉ p
m : ℕ
IH :
  ∀ m_1 < m + 1,
    ∀ (f : R[X]),
      (aeval x) f = 0 → ∀ (n : ℕ), (algebraMap R S) (f.coeff n) ∉ p → f.natDegree = m_1 → ZariskisMainProperty R p
hm : f.natDegree = m + 1
Hfp : (algebraMap R S) f.leadingCoeff ∈ p
a : R
ha : (ofId R S).toRingHom a = f.leadingCoeff • x
⊢ f.eraseLead.natDegree ≤ m
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: R✝ S✝ : Type u
inst✝⁷ : CommRing R✝
inst✝⁶ : CommRing S✝
inst✝⁵ : Algebra R✝ S✝
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal S
inst✝¹ : p.IsPrime
inst✝ : WeaklyQuasiFiniteAt R p
f : R[X] →ₐ[R] S
hf : f.Finite
H : integralClosure R S = ⊥
J : Ideal S := (conductor R (f X)).radical
hp : J ≤ p
⊢ RingHom.ker (Ideal.Quotient.mk J) ≤ p

Tactic:
simpa using hp

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

Goal state before:
pp: case succ
R : Type u_1
inst✝ : CommRing R
f p : R[X]
m n : ℕ
hp : p.natDegree + m ≤ n
hf : f.natDegree ≤ m
k : ℕ
IH :
  ∀ (g : R[X]),
    k ≤ n - m + 1 → f.resultant (g + f * ∑ n ∈ Finset.range k, (monomial n) (p.coeff n)) m n = f.resultant g m n
g : R[X]
H : k + 1 ≤ n - m + 1
⊢ f.resultant (g + f * ∑ x ∈ Finset.range k, (monomial x) (p.coeff x) + f * (monomial k) (p.coeff k)) m n =
    f.resultant g m n

Tactic:
resultant_add_mul_monomial_right,

Goal state after:
case succ
R : Type u_1
inst✝ : CommRing R
f p : R[X]
m n : ℕ
hp : p.natDegree + m ≤ n
hf : f.natDegree ≤ m
k : ℕ
IH :
  ∀ (g : R[X]),
    k ≤ n - m + 1 → f.resultant (g + f * ∑ n ∈ Finset.range k, (monomial n) (p.coeff n)) m n = f.resultant g m n
g : R[X]
H : k + 1 ≤ n - m + 1
⊢ f.resultant (g + f * ∑ x ∈ Finset.range k, (monomial x) (p.coeff x)) m n = f.resultant g m n

case succ.hk
R : Type u_1
inst✝ : CommRing R
f p : R[X]
m n : ℕ
hp : p.natDegree + m ≤ n
hf : f.natDegree ≤ m
k : ℕ
IH :
  ∀ (g : R[X]),
    k ≤ n - m + 1 → f.resultant (g + f * ∑ n ∈ Finset.range k, (monomial n) (p.coeff n)) m n = f.resultant g m n
g : R[X]
H : k + 1 ≤ n - m + 1
⊢ k + m ≤ n

case succ.hf
R : Type u_1
inst✝ : CommRing R
f p : R[X]
m n : ℕ
hp : p.natDegree + m ≤ n
hf : f.natDegree ≤ m
k : ℕ
IH :
  ∀ (g : R[X]),
    k ≤ n - m + 1 → f.resultant (g + f * ∑ n ∈ Finset.range k, (monomial n) (p.coeff n)) m n = f.resultant g m n
g : R[X]
H : k + 1 ≤ n - m + 1
⊢ f.natDegree ≤ m
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
U : ↑Y.affineOpens
⊢ (ker (toNormalization f)).ideal ⟨fromNormalization f ⁻¹ᵁ ↑U, ⋯⟩ = ⊥.ideal ⟨fromNormalization f ⁻¹ᵁ ↑U, ⋯⟩

Tactic:
simp only [ker_apply, IdealSheafData.ideal_bot, Pi.bot_apply]

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
U : ↑Y.affineOpens
⊢ RingHom.ker (CommRingCat.Hom.hom (app (toNormalization f) (fromNormalization f ⁻¹ᵁ ↑U))) = ⊥
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
⊢ (Polynomial.freeMonic R n).coeff n = 1 ∧ ∀ i > n, (Polynomial.freeMonic R n).coeff i = 0

Tactic:
simp +contextual [coeff_freeMonic, not_lt_of_gt, LT.lt.ne']

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
f : MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R) →+* MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R :=
  eval₂Hom (↑(universalFactorizationMap R n m k hn)) (Sum.elim (fun x ↦ X x ⊗ₜ[R] 1) fun x ↦ 1 ⊗ₜ[R] X x)
⊢ RingHom.ker f =
    Ideal.span
      (Set.range fun i ↦
        C (X i) - (map C) ((tensorEquivSum R (Fin m) (Fin k) R) ((universalFactorizationMap R n m k hn) (X i))))

Tactic:
have H (i : _) : tensorEquivSum _ _ _ _ (f (.X i)) = .X i := by aesop

Goal state after:
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
f : MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R) →+* MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R :=
  eval₂Hom (↑(universalFactorizationMap R n m k hn)) (Sum.elim (fun x ↦ X x ⊗ₜ[R] 1) fun x ↦ 1 ⊗ₜ[R] X x)
H : ∀ (i : Fin m ⊕ Fin k), (tensorEquivSum R (Fin m) (Fin k) R) (f (X i)) = X i
⊢ RingHom.ker f =
    Ideal.span
      (Set.range fun i ↦
        C (X i) - (map C) ((tensorEquivSum R (Fin m) (Fin k) R) ((universalFactorizationMap R n m k hn) (X i))))
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: case inr.h₀
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
i : Fin m
j : Fin n
h : ↑i ≤ ↑j
a b : ℕ
e : a + b = ↑j
⊢ (a = ↑i → ¬b = ↑j - ↑i) →
    (if h : b < k then if a < m ∧ a = ↑i then X (Sum.inr ⟨b, ⋯⟩) else 0 else if b = k ∧ a < m ∧ a = ↑i then 1 else 0) =
      0

Tactic:
h

Goal state after:
case inr.h₀
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
i : Fin m
j : Fin n
h✝ : ↑i ≤ ↑j
a b : ℕ
e : a + b = ↑j
h : a = ↑i → ¬b = ↑j - ↑i
⊢ (if h : b < k then if a < m ∧ a = ↑i then X (Sum.inr ⟨b, ⋯⟩) else 0 else if b = k ∧ a < m ∧ a = ↑i then 1 else 0) = 0
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 (map φ (g'.scaleRoots r)) f.natDegree (map φ g').natDegree =
    φ r ^ (f.natDegree * (map φ g').natDegree) * f.resultant (map φ g')

Tactic:
hg',

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 (map φ (g'.scaleRoots r)) f.natDegree g.natDegree =
    φ r ^ (f.natDegree * g.natDegree) * f.resultant g
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 : R[X]) (r : R), ((taylor r) q).resultant ((taylor r) g) = q.resultant g
g : S[X]
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
⊢ φ (((taylor r) f').resultant ((taylor r) g') f.natDegree (map φ g').natDegree) =
    φ (f'.resultant g' f.natDegree (map φ g').natDegree)

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 : R[X]) (r : R), ((taylor r) q).resultant ((taylor r) g) = q.resultant g
g : S[X]
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
⊢ φ (((taylor r) f').resultant ((taylor r) g') f.natDegree g.natDegree) = φ (f'.resultant g' f.natDegree g.natDegree)
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: 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
⊢ (↑(⟨p, hp⟩, ⟨q, hq⟩).1).degree < ?m.186

Tactic:
simpa using hp

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

Goal state before:
pp: 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})
q : PrimeSpectrum S
hq : q ∈ PrimeSpectrum.zeroLocus {g}
e : PrimeSpectrum.comap (algebraMap R S) q = { asIdeal := p, isPrime := inst✝ }
⊢ False

Tactic:
have : q.asIdeal.LiesOver p := ⟨congr(($e).1).symm⟩

Goal state after:
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})
q : PrimeSpectrum S
hq : q ∈ PrimeSpectrum.zeroLocus {g}
e : PrimeSpectrum.comap (algebraMap R S) q = { asIdeal := p, isPrime := inst✝ }
this : q.asIdeal.LiesOver p
⊢ False
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: m n : ℕ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
H : m ≠ 0 ∨ n ≠ 0
a✝ : Nontrivial R
⊢ ∃ p q, p.degree < ↑n ∧ q.degree < ↑m ∧ f * p + g * q = C (f.resultant g m n)

Tactic:
let X := adjSylvester f g ⟨1, by simpa [Polynomial.mem_degreeLT,
    ← Nat.cast_add, Nat.pos_iff_ne_zero, not_and_or, -not_and] using H⟩

Goal state after:
m n : ℕ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
H : m ≠ 0 ∨ n ≠ 0
a✝ : Nontrivial R
X : ↥R[X]_m × ↥R[X]_n := (f.adjSylvester g) ⟨1, ⋯⟩
⊢ ∃ p q, p.degree < ↑n ∧ q.degree < ↑m ∧ f * p + g * q = C (f.resultant g m n)
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
this✝ : IsLocalization.AtPrime (↑(X.presheaf.stalk ↑⟨x, hxV⟩)) (hr.primeIdealOf ⟨x, hxV⟩).asIdeal
this : Algebra ↑(X.presheaf.obj (Opposite.op (toNormalization f ⁻¹ᵁ (normalization f).basicOpen r)))
  ↑(X.presheaf.stalk ↑⟨x, hxV⟩) :=
  X.presheaf.algebra_section_stalk ⟨x, hxV⟩
⊢ (algebraMap ↑(X.presheaf.obj (Opposite.op W)) ↑(X.presheaf.stalk x)).QuasiFinite

Tactic:
@RingHom.quasiFinite_algebraMap

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
this✝ : IsLocalization.AtPrime (↑(X.presheaf.stalk ↑⟨x, hxV⟩)) (hr.primeIdealOf ⟨x, hxV⟩).asIdeal
this : Algebra ↑(X.presheaf.obj (Opposite.op (toNormalization f ⁻¹ᵁ (normalization f).basicOpen r)))
  ↑(X.presheaf.stalk ↑⟨x, hxV⟩) :=
  X.presheaf.algebra_section_stalk ⟨x, hxV⟩
⊢ Algebra.QuasiFinite ↑Γ(X, W) ↑(X.presheaf.stalk x)
Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem

Goal state before:
pp: ⊢ @IsFinite = @IsProper ⊓ @LocallyQuasiFinite

Tactic:
by
  ext
  exact IsFinite.iff_isProper_and_locallyQuasiFinite ..

Goal state after:
Module: Mathlib.RingTheory.Ideal.CotangentBaseChange

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
I : Ideal S
a : S →+* T ⊗[R] S := Algebra.TensorProduct.includeRight.toRingHom
⊢ 0 = (map Algebra.TensorProduct.includeRight.toRingHom I).toCotangent ⟨0, ⋯⟩

Tactic:
exact (map_zero _).symm

Goal state after:
Module: Mathlib.RingTheory.Extension.Cotangent.BaseChange

Goal state before:
pp: case zero
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Extension R S
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra R T
t : T
⊢ (P.tensorCotangentSpace T) 0 = t • (CotangentSpace.map (toBaseChange T)) 0

Tactic:
LinearEquiv.map_zero,

Goal state after:
case zero
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Extension R S
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra R T
t : T
⊢ 0 = t • (CotangentSpace.map (toBaseChange T)) 0
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 ◁ leftZigzag η ε ▷ g ⊗≫ ε ▷ g = g ◁ η ⊗≫ ε ▷ g

Tactic:
h

Goal state after:
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 ◁ ((λ_ f).hom ≫ (ρ_ f).inv) ▷ g ⊗≫ ε ▷ g = g ◁ η ⊗≫ ε ▷ g
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d : B
l : b ⟶ c
r : c ⟶ b
adj : l ⊣ r
g : b ⟶ d
h : c ⟶ d
γ : g ⟶ l ≫ h
⊢ γ ⊗≫ leftZigzag adj.unit adj.counit ▷ h ⊗≫ 𝟙 (l ≫ h) = γ

Tactic:
adj.left_triangle

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c d : B
l : b ⟶ c
r : c ⟶ b
adj : l ⊣ r
g : b ⟶ d
h : c ⟶ d
γ : g ⟶ l ≫ h
⊢ γ ⊗≫ ((λ_ l).hom ≫ (ρ_ l).inv) ▷ h ⊗≫ 𝟙 (l ≫ h) = γ
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d : B
l : b ⟶ c
r : c ⟶ b
adj : l ⊣ r
g : a ⟶ b
h : a ⟶ c
α : g ≫ l ⟶ h
⊢ 𝟙 (g ≫ l) ⊗≫ g ◁ leftZigzag adj.unit adj.counit ⊗≫ α = α

Tactic:
adj.left_triangle

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c d : B
l : b ⟶ c
r : c ⟶ b
adj : l ⊣ r
g : a ⟶ b
h : a ⟶ c
α : g ≫ l ⟶ h
⊢ 𝟙 (g ≫ l) ⊗≫ g ◁ ((λ_ l).hom ≫ (ρ_ l).inv) ⊗≫ α = α
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatMono

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
inst✝² : Flat f
inst✝¹ : LocallyOfFinitePresentation f
inst✝ : Mono f
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [Flat f] [LocallyOfFinitePresentation f] [Mono f], Surjective f → IsOpenImmersion f
hf : ¬Surjective f
U : Y.Opens := { carrier := Set.range ⇑f, is_open' := ⋯ }
hU : IsOpenImmersion U.ι
f' : X ⟶ ↑U := lift U.ι f ⋯
heq : f = f' ≫ U.ι
hflat : Flat f'
hfinpres : LocallyOfFinitePresentation f'
hmono : Mono f'
⊢ IsOpenImmersion f

Tactic:
heq

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝² : Flat f
inst✝¹ : LocallyOfFinitePresentation f
inst✝ : Mono f
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [Flat f] [LocallyOfFinitePresentation f] [Mono f], Surjective f → IsOpenImmersion f
hf : ¬Surjective f
U : Y.Opens := { carrier := Set.range ⇑f, is_open' := ⋯ }
hU : IsOpenImmersion U.ι
f' : X ⟶ ↑U := lift U.ι f ⋯
heq : f = f' ≫ U.ι
hflat : Flat f'
hfinpres : LocallyOfFinitePresentation f'
hmono : Mono f'
⊢ IsOpenImmersion (f' ≫ U.ι)
Module: Mathlib.RingTheory.Flat.Rank

Goal state before:
pp: R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
hg : Function.Bijective ⇑f
h1 : g.Finite
h2 : g.Flat
x : PrimeSpectrum S
algInst✝² : Algebra R S := f.toAlgebra
algInst✝¹ : Algebra S T := g.toAlgebra
algInst✝ : Algebra R T := (g.comp f).toAlgebra
scalarTowerInst✝ : IsScalarTower R S T := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R T))
algebraizeInst✝¹ : Module.Finite S T
algebraizeInst✝ : Module.Flat S T
this : Module.Finite R T
⊢ (g.comp f).finrank (PrimeSpectrum.comap f x) = g.finrank x

Tactic:
have : Module.Flat R T := (RingHom.Flat.of_bijective hg).comp h2

Goal state after:
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
hg : Function.Bijective ⇑f
h1 : g.Finite
h2 : g.Flat
x : PrimeSpectrum S
algInst✝² : Algebra R S := f.toAlgebra
algInst✝¹ : Algebra S T := g.toAlgebra
algInst✝ : Algebra R T := (g.comp f).toAlgebra
scalarTowerInst✝ : IsScalarTower R S T := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R T))
algebraizeInst✝¹ : Module.Finite S T
algebraizeInst✝ : Module.Flat S T
this✝ : Module.Finite R T
this : Module.Flat R T
⊢ (g.comp f).finrank (PrimeSpectrum.comap f x) = g.finrank x
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank

Goal state before:
pp: case inr
X : Scheme
x : ↥X
R : CommRingCat
f : X ⟶ Spec R
inst✝¹ : Flat f
inst✝ : IsFinite f
this :
  ∀ {X : Scheme} (x : ↥X) (R : CommRingCat) (f : X ⟶ Spec R) [Flat f] [IsFinite f],
    (∃ S, X = Spec S) → 1 ≤ finrank f (f x)
hX : ¬∃ S, X = Spec S
x✝ : IsAffine X
heq : f x = (X.isoSpec.inv ≫ f) (X.isoSpec.hom x)
⊢ 1 ≤ finrank (X.isoSpec.inv ≫ f) (f x)

Tactic:
heq

Goal state after:
case inr
X : Scheme
x : ↥X
R : CommRingCat
f : X ⟶ Spec R
inst✝¹ : Flat f
inst✝ : IsFinite f
this :
  ∀ {X : Scheme} (x : ↥X) (R : CommRingCat) (f : X ⟶ Spec R) [Flat f] [IsFinite f],
    (∃ S, X = Spec S) → 1 ≤ finrank f (f x)
hX : ¬∃ S, X = Spec S
x✝ : IsAffine X
heq : f x = (X.isoSpec.inv ≫ f) (X.isoSpec.hom x)
⊢ 1 ≤ finrank (X.isoSpec.inv ≫ f) ((X.isoSpec.inv ≫ f) (X.isoSpec.hom x))
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank

Goal state before:
pp: case inr
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝¹ : Flat f
inst✝ : IsFinite f
h : finrank f = 1
this :
  ∀ {X : Scheme} (R : CommRingCat) (f : X ⟶ Spec R) [Flat f] [IsFinite f], finrank f = 1 → (∃ S, X = Spec S) → IsIso f
hX : ¬∃ S, X = Spec S
x✝ : IsAffine X
⊢ finrank f = 1

Tactic:
h

Goal state after:
case inr
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝¹ : Flat f
inst✝ : IsFinite f
h : finrank f = 1
this :
  ∀ {X : Scheme} (R : CommRingCat) (f : X ⟶ Spec R) [Flat f] [IsFinite f], finrank f = 1 → (∃ S, X = Spec S) → IsIso f
hX : ¬∃ S, X = Spec S
x✝ : IsAffine X
⊢ 1 = 1