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

Goal state before:
pp: n : ℕ
IH :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal S) [inst_3 : p.IsPrime]
    [WeaklyQuasiFiniteAt R p] (f : MvPolynomial (Fin n) R →ₐ[R] S), f.Finite → ZariskisMainProperty R p
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 : MvPolynomial (Fin (n + 1)) R →ₐ[R] S
hf : f.Finite
f' : (MvPolynomial (Fin n) R)[X] →ₐ[R] S := f.comp ↑(MvPolynomial.finSuccEquiv R n).symm
this✝⁴ : Algebra (MvPolynomial (Fin n) R) S := (f'.comp C).toAlgebra
this✝³ : IsScalarTower R (MvPolynomial (Fin n) R) S
f'' : (MvPolynomial (Fin n) R)[X] →ₐ[MvPolynomial (Fin n) R] S := { toRingHom := f'.toRingHom, commutes' := ⋯ }
this✝² : WeaklyQuasiFiniteAt (MvPolynomial (Fin n) R) p
this✝¹ : ZariskisMainProperty (MvPolynomial (Fin n) R) p
r : S
hrp : r ∉ p
hr : IsIntegral (MvPolynomial (Fin n) R) r
m : S → ℕ
hm : ∀ (x : S), IsIntegral (MvPolynomial (Fin n) R) (r ^ m x * x)
s : Finset S
hs : adjoin R ↑s = ⊤
R' : Subalgebra R S := adjoin R ↑(Finset.image (⇑f ∘ MvPolynomial.X ∘ Fin.succ) Finset.univ ∪ r ^ s.sup m • s ∪ {r})
hrR' : r ∈ R'
this✝ : WeaklyQuasiFiniteAt R (Ideal.under (↥R') p)
φ : MvPolynomial (Fin n) R →ₐ[R] ↥R' := MvPolynomial.aeval fun i ↦ ⟨f (MvPolynomial.X i.succ), ⋯⟩
this : ZariskisMainProperty R (Ideal.under (↥R') p)
⊢ Submonoid.powers r ≤ R'.toSubmonoid

Tactic:
by simpa [Submonoid.powers_le]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
this : ↑(ker (toNormalization f)).support = ↑⊤
⊢ IsDominant (toNormalization f)

Tactic:
Scheme.Hom.support_ker,

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
this : closure (Set.range ⇑(toNormalization f)) = ↑⊤
⊢ IsDominant (toNormalization f)
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: n : ℕ
IH :
  ∀ m < n,
    ∀ {K : Type u_3} [inst : Field K] (f g : K[X]),
      f.Monic →
        g.Monic →
          f.Splits →
            g.Splits →
              g.natDegree ≤ f.natDegree →
                f.natDegree + g.natDegree = m →
                  f.resultant g = (Multiset.map (fun ij ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots)).prod
K : Type u_3
inst✝ : Field K
f g : K[X]
hf : f.Monic
hg : g.Monic
hf' : f.Splits
hg' : g.Splits
hfg : g.natDegree ≤ f.natDegree
hN : f.natDegree + g.natDegree = n
hr✝ : ¬g ∣ f
r : K[X] := C (f %ₘ g).leadingCoeff⁻¹ * (f %ₘ g)
hr₀ : f %ₘ g ≠ 0
hrd : r.natDegree < g.natDegree
hr : r.Monic
L : Type u_3 := r.SplittingField
⊢ (map (algebraMap K L) r).natDegree ≤ (map (algebraMap K L) g).natDegree

Tactic:
by simpa [r, natDegree_C_mul, hr₀] using hrd.le

Goal state after:
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: case refine_3
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : FiniteType R S
p : Ideal S
H : ZariskisMainProperty R p
s : Finset S
hs : adjoin R ↑s = ⊤
r : S
hrp : r ∉ p
hr : IsIntegral R r
m : S → ℕ
hm : ∀ (x : S), IsIntegral R (r ^ m x * x)
t : Set S := insert r {x | ∃ x_1 ∈ s, r ^ m x_1 * x_1 = x}
r' : ↥(adjoin R t) := ⟨r, ⋯⟩
⊢ ∃ r, ↑r ∉ p ∧ Function.Bijective ⇑(Localization.awayMap (adjoin R t).val.toRingHom r)

Tactic:
refine ⟨r', hrp,
    IsLocalization.map_injective_of_injective _ _ _ Subtype.val_injective, ?_⟩

Goal state after:
case refine_3
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : FiniteType R S
p : Ideal S
H : ZariskisMainProperty R p
s : Finset S
hs : adjoin R ↑s = ⊤
r : S
hrp : r ∉ p
hr : IsIntegral R r
m : S → ℕ
hm : ∀ (x : S), IsIntegral R (r ^ m x * x)
t : Set S := insert r {x | ∃ x_1 ∈ s, r ^ m x_1 * x_1 = x}
r' : ↥(adjoin R t) := ⟨r, ⋯⟩
⊢ Function.Surjective ⇑(Localization.awayMap (adjoin R t).val.toRingHom r')
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
⊢ QuasiFiniteAt R q.asIdeal ↔ IsOpen {⟨q, ⋯⟩}

Tactic:
refine ⟨fun H ↦ ?_, .of_isOpen_singleton_fiber q⟩
  let p := q.comap (algebraMap R S)
  let e := PrimeSpectrum.preimageHomeomorphFiber R S p
  rw [← e.isOpen_image, Set.image_singleton]
  suffices Algebra.QuasiFiniteAt p.asIdeal.ResidueField (e ⟨q, rfl⟩).asIdeal from
    (QuasiFiniteAt.isClopen_singleton (R := p.asIdeal.ResidueField) _).isOpen
  exact .baseChange q.asIdeal _ congr($(e.symm_apply_apply ⟨q, rfl⟩).1.asIdeal).symm

Goal state after:
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
inst✝⁴ : QuasiCompact f✝
inst✝³ : QuasiSeparated f✝
X S Y : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝² : QuasiCompact f
inst✝¹ : QuasiSeparated f
inst✝ : Smooth g
x : ↥(pullback (fromNormalization f) g)
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hxU : (pullback.snd (fromNormalization f) g ≫ g) x ∈ ↑U
V : TopologicalSpace.Opens ↥Y
hV : V ∈ Y.affineOpens
hxV : (pullback.snd (fromNormalization f) g) x ∈ ↑V
hVU : V ≤ g ⁻¹ᵁ U
W : (pullback (fromNormalization f) g).Opens := pullback.snd (fromNormalization f) g ⁻¹ᵁ V
this✝¹ : IsIso (pushoutSection ⋯ hVU ⋯ ⋯)
this✝ : (CommRingCat.Hom.hom (appLE g U V hVU)).Smooth
algInst✝² : Algebra ↑Γ(S, U) ↑Γ(X, f ⁻¹ᵁ U) := (CommRingCat.Hom.hom (app f U)).toAlgebra
algInst✝¹ : Algebra ↑Γ(S, U) ↑Γ(Y, V) := (CommRingCat.Hom.hom (appLE g U V hVU)).toAlgebra
algInst✝ : Algebra ↑Γ(Y, V) ↑Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V) :=
  (CommRingCat.Hom.hom (app (pullback.snd f g) V)).toAlgebra
algebraizeInst✝ : Algebra.Smooth ↑Γ(S, U) ↑Γ(Y, V)
this : IsIso (pushoutSection ⋯ hVU ⋯ ⋯)
e₀ : CommRingCat.of
    (↑(Y.presheaf.1 (Opposite.op V)) ⊗[↑(S.presheaf.1 (Opposite.op U))] ↑(X.presheaf.1 (Opposite.op (f ⁻¹ᵁ U)))) ≅
  Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V) :=
  ⋯.isoPushout ≪≫ pushout.congrHom ⋯ ⋯ ≪≫ asIso (pushoutSection ⋯ hVU ⋯ ⋯)
r : ↑Γ(Y, V)
⊢ e₀.commRingCatIsoToRingEquiv.toFun ((algebraMap (↑Γ(Y, V)) (↑Γ(Y, V) ⊗[↑Γ(S, U)] ↑Γ(X, f ⁻¹ᵁ U))) r) =
    (algebraMap ↑Γ(Y, V) ↑Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V)) r

Tactic:
by
        change (CommRingCat.ofHom Algebra.TensorProduct.includeLeftRingHom ≫ e₀.hom) r =
          (pullback.snd f g).app V r
        congr 2
        simp [e₀, pushout.inr_desc_assoc, Scheme.Hom.app_eq_appLE]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
r : R
g : R[X]
m n : ℕ
hn : g.natDegree ≤ n
⊢ ((X - C r) ^ m).resultant g m n = eval r g ^ m

Tactic:
nontriviality R
  convert! resultant_pow_left _ _ _ _ _ _ <;> simp [natDegree_pow', hn]

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

Goal state before:
pp: 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
⊢ φ f'.leadingCoeff ≠ 0

Tactic:
simpa [← hfl]

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

Goal state before:
pp: 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
⊢ φ f'.leadingCoeff ≠ 0

Tactic:
simpa [← hfl]

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

Goal state before:
pp: R : Type u_1
R' : Type u_2
S : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing R'
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R R'
inst✝⁷ : Algebra R S
p : Ideal R
q : Ideal R'
inst✝⁶ : p.IsPrime
inst✝⁵ : q.IsPrime
inst✝⁴ : q.LiesOver p
H : Function.Bijective ⇑(ResidueField.mapₐ p q (Algebra.ofId R R') ⋯)
P₁ P₂ : Ideal (R' ⊗[R] S)
inst✝³ : P₁.IsPrime
inst✝² : P₂.IsPrime
inst✝¹ : P₁.LiesOver q
inst✝ : P₂.LiesOver q
H₂ : comap Algebra.TensorProduct.includeRight.toRingHom P₁ = comap Algebra.TensorProduct.includeRight.toRingHom P₂
⊢ P₁ = P₂

Tactic:
refine congr_arg Subtype.val ((Ideal.fiberIsoOfBijectiveResidueField
  (S := S) H).injective (a₁ := ⟨P₁, ‹_›, ‹_›⟩) (a₂ := ⟨P₂, ‹_›, ‹_›⟩) (by ext1; simpa))

Goal state after:
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
b₁ : Module.Basis (Fin (m + n)) R (↥R[X]_m × ↥R[X]_n) :=
  ((degreeLT.basis R m).prod (degreeLT.basis R n)).reindex finSumFinEquiv
b₂ : Module.Basis (Fin (m + n)) R ↥R[X]_(m + n) := degreeLT.basis R (m + n)
this :
  (Matrix.toLin b₁ b₁)
      (((LinearMap.toMatrix b₁ b₂) (f.sylvesterMap g hf hg)).adjugate *
        (LinearMap.toMatrix b₁ b₂) (f.sylvesterMap g hf hg)) =
    (Matrix.toLin b₁ b₁) (((LinearMap.toMatrix b₁ b₂) (f.sylvesterMap g hf hg)).det • 1)
⊢ f.adjSylvester g ∘ₗ f.sylvesterMap g hf hg = f.resultant g m n • LinearMap.id

Tactic:
rwa [Matrix.toLin_mul b₁ b₂ b₁, Matrix.toLin_toMatrix, map_smul,
    toMatrix_sylvesterMap', Matrix.toLin_one, ← resultant] at this

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

Goal state before:
pp: K : Type u
inst✝⁴ : Field K
inst✝³ : IsAlgClosed K
G : Over (Spec (CommRingCat.of K))
inst✝² : IsProper G.hom
inst✝¹ : IsIntegral (G ⊗ G).left
inst✝ : GrpObj G
S : Scheme := Spec (CommRingCat.of K)
point : ↥S := IsLocalRing.closedPoint K
hpoint : IsClosed {point}
this✝¹⁰ : Nonempty ↥G.left
this✝⁹ : IsProper (G ⊗ G).hom
this✝⁸ : JacobsonSpace ↥(G ⊗ G).left
this✝⁷ : Surjective G.hom
this✝⁶ : IsProper (Over.Hom.left (fst G G))
this✝⁵ : Surjective (Over.Hom.left (fst G G))
this✝⁴ : IsProper (Over.Hom.left (GrpObj.commutator G) ≫ G.hom)
this✝³ : IsClosedImmersion (Over.Hom.left (lift η η) ≫ Over.Hom.left (fst G G))
this✝² : IsClosedImmersion (Over.Hom.left (lift η η))
γ : G ⊗ G ⟶ G ⊗ G := lift (fst G G) (GrpObj.commutator G)
this✝¹ : IsProper (Over.Hom.left γ ≫ Over.Hom.left (fst G G))
this✝ : IsProper (Over.Hom.left γ)
H✝ : ⇑(Over.Hom.left γ) '' ⇑(Over.Hom.left (fst G G)) ⁻¹' {(Over.Hom.left η) point} ⊆ {(Over.Hom.left (lift η η)) point}
U : G.left.Opens
hηU : (Over.Hom.left η) point ∈ U
H : IsFinite ((Scheme.Hom.imageι (Over.Hom.left γ) ≫ Over.Hom.left (fst G G)) ∣_ U)
x : ↥U
this : ⇑U.ι ⁻¹' {↑x} = {x}
⊢ ⇑(pullback.fst G.hom G.hom) ⁻¹' {↑x} ∩ Set.range ⇑(Over.Hom.left γ) ⊆
    ⇑(pullback.fst G.hom G.hom) ⁻¹' {↑x} ∩
      (⇑(pullback.fst G.hom G.hom) ⁻¹' ↑U ∩ ↑(Scheme.Hom.ker (Over.Hom.left γ)).support)

Tactic:
Scheme.Hom.support_ker,

Goal state after:
K : Type u
inst✝⁴ : Field K
inst✝³ : IsAlgClosed K
G : Over (Spec (CommRingCat.of K))
inst✝² : IsProper G.hom
inst✝¹ : IsIntegral (G ⊗ G).left
inst✝ : GrpObj G
S : Scheme := Spec (CommRingCat.of K)
point : ↥S := IsLocalRing.closedPoint K
hpoint : IsClosed {point}
this✝¹⁰ : Nonempty ↥G.left
this✝⁹ : IsProper (G ⊗ G).hom
this✝⁸ : JacobsonSpace ↥(G ⊗ G).left
this✝⁷ : Surjective G.hom
this✝⁶ : IsProper (Over.Hom.left (fst G G))
this✝⁵ : Surjective (Over.Hom.left (fst G G))
this✝⁴ : IsProper (Over.Hom.left (GrpObj.commutator G) ≫ G.hom)
this✝³ : IsClosedImmersion (Over.Hom.left (lift η η) ≫ Over.Hom.left (fst G G))
this✝² : IsClosedImmersion (Over.Hom.left (lift η η))
γ : G ⊗ G ⟶ G ⊗ G := lift (fst G G) (GrpObj.commutator G)
this✝¹ : IsProper (Over.Hom.left γ ≫ Over.Hom.left (fst G G))
this✝ : IsProper (Over.Hom.left γ)
H✝ : ⇑(Over.Hom.left γ) '' ⇑(Over.Hom.left (fst G G)) ⁻¹' {(Over.Hom.left η) point} ⊆ {(Over.Hom.left (lift η η)) point}
U : G.left.Opens
hηU : (Over.Hom.left η) point ∈ U
H : IsFinite ((Scheme.Hom.imageι (Over.Hom.left γ) ≫ Over.Hom.left (fst G G)) ∣_ U)
x : ↥U
this : ⇑U.ι ⁻¹' {↑x} = {x}
⊢ ⇑(pullback.fst G.hom G.hom) ⁻¹' {↑x} ∩ Set.range ⇑(Over.Hom.left γ) ⊆
    ⇑(pullback.fst G.hom G.hom) ⁻¹' {↑x} ∩ (⇑(pullback.fst G.hom G.hom) ⁻¹' ↑U ∩ closure (Set.range ⇑(Over.Hom.left γ)))
Module: Mathlib.AlgebraicGeometry.Group.Abelian

Goal state before:
pp: K : Type u
inst✝⁴ : Field K
inst✝³ : IsAlgClosed K
G : Over (Spec (CommRingCat.of K))
inst✝² : IsProper G.hom
inst✝¹ : IsIntegral (G ⊗ G).left
inst✝ : GrpObj G
S : Scheme := Spec (CommRingCat.of K)
point : ↥S := IsLocalRing.closedPoint K
hpoint : IsClosed {point}
this✝⁹ : Nonempty ↥G.left
this✝⁸ : IsProper (G ⊗ G).hom
this✝⁷ : JacobsonSpace ↥(G ⊗ G).left
this✝⁶ : Surjective G.hom
this✝⁵ : IsProper (Over.Hom.left (fst G G))
this✝⁴ : Surjective (Over.Hom.left (fst G G))
this✝³ : IsProper (Over.Hom.left (GrpObj.commutator G) ≫ G.hom)
this✝² : IsClosedImmersion (Over.Hom.left (lift η η) ≫ Over.Hom.left (fst G G))
this✝¹ : IsClosedImmersion (Over.Hom.left (lift η η))
γ : G ⊗ G ⟶ G ⊗ G := lift (fst G G) (GrpObj.commutator G)
this✝ : IsProper (Over.Hom.left γ ≫ Over.Hom.left (fst G G))
this : IsProper (Over.Hom.left γ)
H✝¹ :
  ⇑(Over.Hom.left γ) '' ⇑(Over.Hom.left (fst G G)) ⁻¹' {(Over.Hom.left η) point} ⊆ {(Over.Hom.left (lift η η)) point}
U : G.left.Opens
hηU : (Over.Hom.left η) point ∈ U
H✝ : IsFinite ((Scheme.Hom.imageι (Over.Hom.left γ) ≫ Over.Hom.left (fst G G)) ∣_ U)
H : ∀ (x : ↥U), (⇑(pullback.fst G.hom G.hom) ⁻¹' {↑x} ∩ Set.range ⇑(Over.Hom.left γ)).Finite
y : ↥(G ⊗ G).left
hyU : y ∈ ↑(Over.Hom.left (fst G G) ⁻¹ᵁ U)
hy : IsClosed {y}
⊢ IsClosed {(Over.Hom.left (fst G G)) y}

Tactic:
simpa using (fst G G).left.isClosedMap _ hy

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
⊢ ((CommRingCat.Hom.hom (stalkMap f x)).comp (CommRingCat.Hom.hom (Y.presheaf.germ U (f x) hxU))).QuasiFinite

Tactic:
← CommRingCat.hom_comp,

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 (Y.presheaf.germ U (f x) hxU ≫ stalkMap f x)).QuasiFinite
Module: Mathlib.RingTheory.Finiteness.Descent

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

Tactic:
refine le_antisymm ?_ ?_

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

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
Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFiniteType f
⊢ quasiFiniteLocus f = ⊤ ↔ LocallyQuasiFinite f

Tactic:
refine ⟨fun H ↦ locallyQuasiFinite_iff_isDiscrete_preimage_singleton.mpr fun x ↦ ?_,
    fun _ ↦ f.quasiFiniteLocus_eq_top⟩
  rw [isDiscrete_iff_discreteTopology, discreteTopology_iff_isOpen_singleton]
  rintro ⟨a, rfl⟩
  rw [← (f.fiberHomeo _).symm.isOpen_image, Set.image_singleton]
  exact (H.ge (Set.mem_univ a)).isClopen_singleton_asFiber.isOpen

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
inst✝ : Module.Flat R T
⊢ Function.Injective ⇑(tensorCotangentHom R T I)

Tactic:
let a : S →+* T ⊗[R] S := Algebra.TensorProduct.includeRight.toRingHom
  let f : (I.map a).Cotangent →ₗ[T] T ⊗[R] S ⧸ (I.map a) ^ 2 :=
    (Ideal.cotangentToQuotientSquare _).restrictScalars T
  suffices h : Function.Injective (f ∘ₗ tensorCotangentHom R T I) from .of_comp h
  let g : T ⊗[R] I.Cotangent →ₗ[T] T ⊗[R] (S ⧸ I ^ 2) :=
    AlgebraTensorModule.lTensor T T I.cotangentToQuotientSquare
  let hₐ : T ⊗[R] (S ⧸ I ^ 2) ≃ₐ[T] T ⊗[R] S ⧸ (I.map a) ^ 2 :=
    (Algebra.TensorProduct.tensorQuotientEquiv _ _ _ _).trans
      (Ideal.quotientEquivAlgOfEq T (Ideal.map_pow _ _ _))
  have : f ∘ₗ tensorCotangentHom R T I = hₐ.toLinearMap ∘ₗ g := by
    ext x
    obtain ⟨x, rfl⟩ := I.toCotangent_surjective x
    dsimp [f, g, hₐ]
    rw [tensorCotangentHom_tmul, one_smul, Ideal.toCotangent_to_quotient_square]
    simp
  rw [this, LinearMap.coe_comp]
  apply hₐ.injective.comp
  · apply Module.Flat.lTensor_preserves_injective_linearMap (M := T)
      (I.cotangentToQuotientSquare.restrictScalars R)
    apply cotangentToQuotientSquare_injective

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 : StrictlyUnitaryLaxFunctorCore B C
a✝ b✝ c✝ d✝ : B
f : a✝ ⟶ b✝
g : b✝ ⟶ c✝
h : c✝ ⟶ d✝
⊢ S.mapComp f g ▷ S.map h ≫ S.mapComp (f ≫ g) h ≫ S.map₂ (α_ f g h).hom =
    (α_ (S.map f) (S.map g) (S.map h)).hom ≫ S.map f ◁ S.mapComp g h ≫ S.mapComp f (g ≫ h)

Tactic:
simpa using S.map₂_associator f g h

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
S : StrictPseudofunctorCore B C
a✝ b✝ c✝ d✝ : B
f : a✝ ⟶ b✝
g : b✝ ⟶ c✝
h : c✝ ⟶ d✝
⊢ S.map₂ (α_ f g h).hom =
    (eqToIso ⋯).hom ≫
      (eqToIso ⋯).hom ▷ S.map h ≫ (α_ (S.map f) (S.map g) (S.map h)).hom ≫ S.map f ◁ (eqToIso ⋯).inv ≫ (eqToIso ⋯).inv

Tactic:
simpa using S.map₂_associator f g h

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✝ d✝ : B
f : a✝ ⟶ b✝
g : b✝ ⟶ c✝
h : c✝ ⟶ d✝
⊢ S.map₂ (α_ f g h).hom =
    (S.mapComp (f ≫ g) h).hom ≫
      (S.mapComp f g).hom ▷ S.map h ≫
        (α_ (S.map f) (S.map g) (S.map h)).hom ≫ S.map f ◁ (S.mapComp g h).inv ≫ (S.mapComp f (g ≫ h)).inv

Tactic:
simpa using S.map₂_associator f g h

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

Goal state before:
pp: R✝ R A : CommRingCat
X M G : Scheme
inst✝² : G.Over (Spec R)
inst✝¹ : GrpObj (G.asOver (Spec R))
inst✝ : IsAffine G
⊢ HopfAlgebra ↑R ↑Γ(G, ⊤)

Tactic:
have : GrpObj ((algSpec R).obj <| .op <| CommAlgCat.of R Γ(G, ⊤)) :=
    .ofIso <| G.isoSpec.asOver (Spec R)

Goal state after:
R✝ R A : CommRingCat
X M G : Scheme
inst✝² : G.Over (Spec R)
inst✝¹ : GrpObj (G.asOver (Spec R))
inst✝ : IsAffine G
this : GrpObj ((algSpec R).obj (op (CommAlgCat.of ↑R ↑Γ(G, ⊤))))
⊢ HopfAlgebra ↑R ↑Γ(G, ⊤)
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
⊢ IsOpenImmersion f

pp: X Y : Scheme
f : X ⟶ Y
inst✝² : Flat f
inst✝¹ : LocallyOfFinitePresentation f
inst✝ : Mono f
hf : Surjective f
⊢ IsOpenImmersion f

Tactic:
· let U : Y.Opens := ⟨Set.range f.base, f.isOpenMap.isOpen_range⟩
    -- needed to prevent `wlog` to go in a typeclass loop
    have hU : IsOpenImmersion U.ι := U.instIsOpenImmersionι
    let f' := hU.lift U.ι f (by simp [U])
    have heq : f = f' ≫ U.ι := by simp [f']
    have hflat : Flat f' :=
      of_postcomp (W := @Flat) f' U.ι hU (by rwa [← heq])
    have hfinpres : LocallyOfFinitePresentation f' :=
      of_postcomp (W := @LocallyOfFinitePresentation) f' U.ι hU (by rwa [← heq])
    have hmono : Mono f' := mono_of_mono_fac heq.symm
    rw [heq]
    have := this f' ⟨fun ⟨x, ⟨y, hy⟩⟩ ↦
      ⟨y, by apply U.ι.injective; simp [← Scheme.Hom.comp_apply, f', hy]⟩⟩
    infer_instance

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝² : Flat f
inst✝¹ : LocallyOfFinitePresentation f
inst✝ : Mono f
hf : Surjective f
⊢ IsOpenImmersion f
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
y : ↥(Y.affineCover.X i)
⊢ finrank (pullback.snd f (Y.affineCover.f i)) y = 1 y

Tactic:
finrank_pullback_snd,

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
y : ↥(Y.affineCover.X i)
⊢ finrank f ((Y.affineCover.f i) y) = 1 y