mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite

Goal state before:
pp: case inr
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝ : LocallyOfFiniteType f
hf : ∀ (x : ↥(Spec R)), (⇑f ⁻¹' {x}).Finite
this :
  ∀ {X : Scheme} (R : CommRingCat) (f : X ⟶ Spec R) [LocallyOfFiniteType f],
    (∀ (x : ↥(Spec R)), (⇑f ⁻¹' {x}).Finite) → (∃ S, X = Spec S) → id (LocallyQuasiFinite f)
hX : ¬∃ S, X = Spec S
⊢ id (LocallyQuasiFinite f)

Tactic:
exact (IsZariskiLocalAtSource.iff_of_openCover X.affineCover).mpr fun i ↦ this _ _
      (fun x ↦ ((hf x).preimage (X.affineCover.f _).isOpenEmbedding.injective.injOn :)) ⟨_, rfl⟩

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFiniteType f
hf : ∀ (x : ↥Y), (⇑f ⁻¹' {x}).Finite
⊢ LocallyQuasiFinite f

Tactic:
change id _ -- avoid typeclass synthesis from getting stuck on the wlog hypothesis.
  wlog hY : ∃ R, Y = Spec R
  · refine (IsZariskiLocalAtTarget.iff_of_openCover Y.affineCover).mpr fun i ↦
      this (f := pullback.snd _ _) (fun x ↦ ?_) ⟨_, rfl⟩
    convert!
      (hf (Y.affineCover.f i x)).preimage
        (pullback.fst f (Y.affineCover.f i)).isOpenEmbedding.injective.injOn
    ext
    simp [← (Y.affineCover.f i).isOpenEmbedding.injective.eq_iff, ← Scheme.Hom.comp_apply,
      -Hom.comp_base, pullback.condition]
  obtain ⟨R, rfl⟩ := hY
  wlog hX : ∃ S, X = Spec S
  · exact (IsZariskiLocalAtSource.iff_of_openCover X.affineCover).mpr fun i ↦ this _ _
      (fun x ↦ ((hf x).preimage (X.affineCover.f _).isOpenEmbedding.injective.injOn :)) ⟨_, rfl⟩
  obtain ⟨S, rfl⟩ := hX
  obtain ⟨φ, rfl⟩ := Spec.map_surjective f
  simp only [HasRingHomProperty.Spec_iff, id_eq] at *
  algebraize [φ.hom]
  exact (Algebra.QuasiFinite.iff_finite_comap_preimage_singleton).mpr hf

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝³ : CommRing K
inst✝² : IsDomain K
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R K[X]
c : R
x : K⟮X⟯
⊢ c • x =
    { toFun := fun x ↦ RatFunc.mk ((algebraMap R K[X]) x) 1, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯,
          map_add' := ⋯ }
        c *
      x

Tactic:
induction x using RatFunc.induction_on' with | _ p q hq
    rw [RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk, mk_one', ← mk_smul,
      mk_def_of_ne (c • p) hq, mk_def_of_ne p hq, ← ofFractionRing_mul,
      IsLocalization.mul_mk'_eq_mk'_of_mul, Algebra.smul_def]

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
⊢ Function.Injective ⇑(algebraMap K[X] K⟮X⟯)

Tactic:
by
  rw [← ofFractionRing_comp_algebraMap]
  exact ofFractionRing_injective.comp (IsFractionRing.injective _ _)

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case neg
k : Type u_3
K : Type u_4
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : Algebra.IsAlgebraic k K
hf : ¬Module.Finite k⟮X⟯ K⟮X⟯
⊢ Module.finrank k⟮X⟯ K⟮X⟯ = Module.finrank k K

Tactic:
have hf' : ¬ Module.Finite k K := by
      rwa [← Module.rank_lt_aleph0_iff, ← rank_ratFunc_ratFunc, Module.rank_lt_aleph0_iff]
    rw [Module.finrank_of_not_finite hf, Module.finrank_of_not_finite hf']

Goal state after:
Module: Mathlib.RingTheory.Unramified.LocalStructure

Goal state before:
pp: case e_5
R : Type u_1
S : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
P : Ideal R
inst✝⁵ : P.IsPrime
Q : Ideal S
inst✝⁴ : Q.IsPrime
inst✝³ : Q.LiesOver P
inst✝² : IsUnramifiedAt R Q
x : S
p : R[X]
inst✝¹ : Algebra (Localization.AtPrime P) (Localization.AtPrime Q)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra P Q
hp₁ : Ideal.span {Polynomial.map (algebraMap R P.ResidueField) p} = RingHom.ker (aeval (1 ⊗ₜ[R] x)).toRingHom
hp₂ : R[x] = ⊤
Q' : Ideal (P.Fiber S) := ⋯
this✝⁴ : Q'.LiesOver Q
this✝³ : Q'.LiesOver P
this✝² : Algebra (Localization.AtPrime Q) (Localization.AtPrime Q') := ⋯
this✝¹ : Algebra (Localization.AtPrime P) (Localization.AtPrime Q') := ⋯
this✝ : IsUnramifiedAt P.ResidueField Q'
this : Function.Surjective ⇑(aeval (1 ⊗ₜ[R] x))
⊢ IsLocalRing.ResidueField.instAlgebra = IsLocalRing.ResidueField.algebra (Localization.AtPrime Q')

pp: case e_6
R : Type u_1
S : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
P : Ideal R
inst✝⁵ : P.IsPrime
Q : Ideal S
inst✝⁴ : Q.IsPrime
inst✝³ : Q.LiesOver P
inst✝² : IsUnramifiedAt R Q
x : S
p : R[X]
inst✝¹ : Algebra (Localization.AtPrime P) (Localization.AtPrime Q)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra P Q
hp₁ : Ideal.span {Polynomial.map (algebraMap R P.ResidueField) p} = RingHom.ker (aeval (1 ⊗ₜ[R] x)).toRingHom
hp₂ : R[x] = ⊤
Q' : Ideal (P.Fiber S) := ⋯
this✝⁴ : Q'.LiesOver Q
this✝³ : Q'.LiesOver P
this✝² : Algebra (Localization.AtPrime Q) (Localization.AtPrime Q') := ⋯
this✝¹ : Algebra (Localization.AtPrime P) (Localization.AtPrime Q') := ⋯
this✝ : IsUnramifiedAt P.ResidueField Q'
this : Function.Surjective ⇑(aeval (1 ⊗ₜ[R] x))
⊢ (IsScalarTower.toAlgHom P.ResidueField Q.ResidueField Q'.ResidueField) ((algebraMap S Q.ResidueField) x) =
    (algebraMap (P.Fiber S) Q'.ResidueField) (1 ⊗ₜ[R] x)

Tactic:
· apply algebra_ext; intros r; congr 1; ext x; simp [← IsScalarTower.algebraMap_apply]

Goal state after:
case e_6
R : Type u_1
S : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
P : Ideal R
inst✝⁵ : P.IsPrime
Q : Ideal S
inst✝⁴ : Q.IsPrime
inst✝³ : Q.LiesOver P
inst✝² : IsUnramifiedAt R Q
x : S
p : R[X]
inst✝¹ : Algebra (Localization.AtPrime P) (Localization.AtPrime Q)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra P Q
hp₁ : Ideal.span {Polynomial.map (algebraMap R P.ResidueField) p} = RingHom.ker (aeval (1 ⊗ₜ[R] x)).toRingHom
hp₂ : R[x] = ⊤
Q' : Ideal (P.Fiber S) := ⋯
this✝⁴ : Q'.LiesOver Q
this✝³ : Q'.LiesOver P
this✝² : Algebra (Localization.AtPrime Q) (Localization.AtPrime Q') := ⋯
this✝¹ : Algebra (Localization.AtPrime P) (Localization.AtPrime Q') := ⋯
this✝ : IsUnramifiedAt P.ResidueField Q'
this : Function.Surjective ⇑(aeval (1 ⊗ₜ[R] x))
⊢ (IsScalarTower.toAlgHom P.ResidueField Q.ResidueField Q'.ResidueField) ((algebraMap S Q.ResidueField) x) =
    (algebraMap (P.Fiber S) Q'.ResidueField) (1 ⊗ₜ[R] x)
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
p : Ideal S
⊢ ZariskisMainProperty R p ↔ ∃ r ∉ p, ∀ (x : S), ∃ m, IsIntegral R (r ^ m * x)

Tactic:
refine zariskisMainProperty_iff.trans (exists_congr fun r ↦ and_congr_right fun hrp ↦
    and_iff_right_of_imp fun H ↦ ?_)
  obtain ⟨n, hn⟩ := H r
  rw [← pow_succ] at hn
  exact (IsIntegral.pow_iff (by simp)).mp hn

Goal state after:
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: case h.zero
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
IH :
  ∀ m < 0,
    ∀ (f : R[X]),
      (aeval x) f = 0 → ∀ (n : ℕ), (algebraMap R S) (f.coeff n) ∉ p → f.natDegree = m → ZariskisMainProperty R p
hm : f.natDegree = 0
⊢ ZariskisMainProperty R p

pp: case h.succ
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
⊢ ZariskisMainProperty R p

Tactic:
· obtain ⟨r, rfl⟩ := natDegree_eq_zero.mp hm
    cases n <;> aesop

Goal state after:
case h.succ
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
⊢ ZariskisMainProperty R p
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 = ⊥
hp : conductor R (f X) ≤ p
⊢ False

Tactic:
← ‹p.IsPrime›.isRadical.radical_le_iff

Goal state after:
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 = ⊥
hp : (conductor R (f X)).radical ≤ p
⊢ False
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
U : ↑Y.affineOpens
e : ↑(fromNormalization f ⁻¹ᵁ ↑U) ≅ (normalizationOpenCover f).X U :=
  IsOpenImmersion.isoOfRangeEq (fromNormalization f ⁻¹ᵁ ↑U).ι ((normalizationOpenCover f).f U) ⋯
⊢ IsIntegralHom ((e.inv ≫ fromNormalization f ∣_ ↑U) ≫ (IsAffineOpen.isoSpec ⋯).hom)

Tactic:
have : (f.normalizationDiagramMap.app (.op U)).hom.IsIntegral := by
    let := (f.app U).hom.toAlgebra
    change (algebraMap Γ(Y, U) (integralClosure Γ(Y, U) Γ(X, f ⁻¹ᵁ U))).IsIntegral
    exact algebraMap_isIntegral_iff.mpr inferInstance

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
U : ↑Y.affineOpens
e : ↑(fromNormalization f ⁻¹ᵁ ↑U) ≅ (normalizationOpenCover f).X U :=
  IsOpenImmersion.isoOfRangeEq (fromNormalization f ⁻¹ᵁ ↑U).ι ((normalizationOpenCover f).f U) ⋯
this : (CommRingCat.Hom.hom ((normalizationDiagramMap f).app (Opposite.op ↑U))).IsIntegral
⊢ IsIntegralHom ((e.inv ≫ fromNormalization f ∣_ ↑U) ≫ (IsAffineOpen.isoSpec ⋯).hom)
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case inr
P : {R : Type u} → [inst : CommRing R] → R[X] → Prop
Splits : ∀ (R : Type u) [inst : Field R] (p : R[X]), p.Splits → P p
injective :
  ∀ (R S : Type u) [inst : CommRing R] [inst_1 : CommRing S] (φ : R →+* S),
    Function.Injective ⇑φ → ∀ (p : R[X]), P (map φ p) → P p
surjective :
  ∀ (R S : Type u) [inst : CommRing R] [inst_1 : CommRing S] (φ : R →+* S),
    Function.Surjective ⇑φ → ∀ (p : S[X]), (∀ (q : R[X]), P q) → P p
R : Type u
inst✝ : CommRing R
p : R[X]
hR✝ : IsDomain R
this : ∀ {R : Type u} [inst : CommRing R] (p : R[X]), IsDomain R → IsField R → P p
hR : ¬IsField R
⊢ P p

Tactic:
exact injective _ _ _ (FaithfulSMul.algebraMap_injective R (FractionRing R)) _
      (this _ inferInstance (Field.toIsField _))

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R[X]
m n : ℕ
hm : f.natDegree ≤ m
⊢ f.resultant (X ^ n) m n = (-1) ^ (m * n) * f.coeff 0 ^ n

Tactic:
convert! resultant_X_sub_C_pow_right f 0 m n hm

Goal state after:
case e'_2.e'_4
R : Type u_1
inst✝ : CommRing R
f : R[X]
m n : ℕ
hm : f.natDegree ≤ m
⊢ X = X - C 0

case e'_3
R : Type u_1
inst✝ : CommRing R
f : R[X]
m n : ℕ
hm : f.natDegree ≤ m
⊢ f.coeff 0 = eval 0 f
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 (fst G G)) ⁻¹' {(Over.Hom.left η) point} \
      ⇑(Over.Hom.left γ) ⁻¹' {(Over.Hom.left (lift η η)) point}).Nonempty
⊢ False

Tactic:
obtain ⟨c₀, ⟨hc₁, hc₂⟩, hc₃⟩ := nonempty_inter_closedPoints H <| by
      rw [Set.sdiff_eq_compl_inter, ← Set.image_singleton, ← Set.image_singleton];
      refine (IsOpen.isLocallyClosed ?_).inter (IsClosed.isLocallyClosed ?_)
      · exact (((lift η[G] η[G]).left.isClosedMap _ hpoint).preimage γ.left.continuous).isOpen_compl
      · exact (η[G].left.isClosedMap _ hpoint).preimage (fst G G).left.continuous

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 (fst G G)) ⁻¹' {(Over.Hom.left η) point} \
      ⇑(Over.Hom.left γ) ⁻¹' {(Over.Hom.left (lift η η)) point}).Nonempty
c₀ : ↥(G ⊗ G).left
hc₃ : c₀ ∈ closedPoints ↥(G ⊗ G).left
hc₁ : c₀ ∈ ⇑(Over.Hom.left (fst G G)) ⁻¹' {(Over.Hom.left η) point}
hc₂ : c₀ ∉ ⇑(Over.Hom.left γ) ⁻¹' {(Over.Hom.left (lift η η)) point}
⊢ False
Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝² : LocallyOfFiniteType f
inst✝¹ : IsSeparated f
inst✝ : QuasiCompact f
x : ↥X
hx : QuasiFiniteAt f x
T : Scheme
fT : T ⟶ Y
left✝¹ : Etale fT
u : ↥T
hu : fT u = f x
V W : (pullback f fT).Opens
v : ↥V
hVW : IsCompl V W
left✝ : IsFinite (V.ι ≫ pullback.snd f fT)
hv₂ : (pullback.fst f fT) ↑v = x
hVW' : ↑W = (↑V)ᶜ
this✝ : IsClosedImmersion V.ι
this : IsClosedImmersion W.ι
⊢ ∃ U, (toNormalization (pullback.snd f fT)) ↑v ∈ U ∧ IsIso (toNormalization (pullback.snd f fT) ∣_ U)

Tactic:
obtain ⟨H⟩ := nonempty_isColimit_binaryCofanMk_of_isCompl V.ι W.ι (by simpa)

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝² : LocallyOfFiniteType f
inst✝¹ : IsSeparated f
inst✝ : QuasiCompact f
x : ↥X
hx : QuasiFiniteAt f x
T : Scheme
fT : T ⟶ Y
left✝¹ : Etale fT
u : ↥T
hu : fT u = f x
V W : (pullback f fT).Opens
v : ↥V
hVW : IsCompl V W
left✝ : IsFinite (V.ι ≫ pullback.snd f fT)
hv₂ : (pullback.fst f fT) ↑v = x
hVW' : ↑W = (↑V)ᶜ
this✝ : IsClosedImmersion V.ι
this : IsClosedImmersion W.ι
H : IsColimit (BinaryCofan.mk V.ι W.ι)
⊢ ∃ U, (toNormalization (pullback.snd f fT)) ↑v ∈ U ∧ IsIso (toNormalization (pullback.snd f fT) ∣_ U)
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
W : TopologicalSpace.Opens ↥X
hW : W ∈ X.affineOpens
hxW : x ∈ ↑W
hWV : W ≤ toNormalization f ⁻¹ᵁ V y
this : IsAffine ↑W
V' : (normalization f).Opens := opensRange (X.homOfLE hWV ≫ toNormalization f ∣_ V y ≫ (V y).ι)
hV' : IsAffineOpen V'
hV'V : V' ≤ V y
⊢ toNormalization f ⁻¹ᵁ V' = W

Tactic:
have : (f.toNormalization ⁻¹ᵁ V y).ι ⁻¹ᵁ f.toNormalization ⁻¹ᵁ V' =
          (f.toNormalization ⁻¹ᵁ V y).ι ⁻¹ᵁ W := by
        rw [← Scheme.Hom.comp_preimage, ← morphismRestrict_ι]
        simp only [V', opensRange_comp, Scheme.Hom.preimage_image_eq, opensRange_homOfLE]

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
W : TopologicalSpace.Opens ↥X
hW : W ∈ X.affineOpens
hxW : x ∈ ↑W
hWV : W ≤ toNormalization f ⁻¹ᵁ V y
this✝ : IsAffine ↑W
V' : (normalization f).Opens := opensRange (X.homOfLE hWV ≫ toNormalization f ∣_ V y ≫ (V y).ι)
hV' : IsAffineOpen V'
hV'V : V' ≤ V y
this : (toNormalization f ⁻¹ᵁ V y).ι ⁻¹ᵁ toNormalization f ⁻¹ᵁ V' = (toNormalization f ⁻¹ᵁ V y).ι ⁻¹ᵁ W
⊢ toNormalization f ⁻¹ᵁ V' = W
Module: Mathlib.AlgebraicGeometry.Group.Abelian

Goal state before:
pp: K : Type u
inst✝³ : Field K
G : Over (Spec (CommRingCat.of K))
inst✝² : IsProper G.hom
inst✝¹ : GeometricallyIntegral G.hom
inst✝ : GrpObj G
f : Spec (CommRingCat.of (AlgebraicClosure K)) ⟶ Spec (CommRingCat.of K) :=
  Spec.map (CommRingCat.ofHom (algebraMap K (AlgebraicClosure K)))
G' : Over (Spec (CommRingCat.of (AlgebraicClosure K))) := (Over.pullback f).obj G
this✝² : IsProper G'.hom
this✝¹ : IsIntegral (G' ⊗ G').left
this✝ : GrpObj G' := Functor.grpObjObj
this : IsCommMonObj G'
⊢ IsCommMonObj G

Tactic:
rw [isCommMonObj_iff_commutator_eq_toUnit_η] at this ⊢

Goal state after:
K : Type u
inst✝³ : Field K
G : Over (Spec (CommRingCat.of K))
inst✝² : IsProper G.hom
inst✝¹ : GeometricallyIntegral G.hom
inst✝ : GrpObj G
f : Spec (CommRingCat.of (AlgebraicClosure K)) ⟶ Spec (CommRingCat.of K) :=
  Spec.map (CommRingCat.ofHom (algebraMap K (AlgebraicClosure K)))
G' : Over (Spec (CommRingCat.of (AlgebraicClosure K))) := (Over.pullback f).obj G
this✝² : IsProper G'.hom
this✝¹ : IsIntegral (G' ⊗ G').left
this✝ : GrpObj G' := Functor.grpObjObj
this : GrpObj.commutator G' = toUnit (G' ⊗ G') ≫ η
⊢ GrpObj.commutator G = toUnit (G ⊗ G) ≫ η
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
⊢ Function.Surjective ⇑((AlgebraTensorModule.lTensor T T) f₀)

Tactic:
← LinearMap.range_eq_top,

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
⊢ ((AlgebraTensorModule.lTensor T T) f₀).range = ⊤
Module: Mathlib.RingTheory.Extension.Cotangent.BaseChange

Goal state before:
pp: 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✝
P : Extension R S
T : Type u_4
inst✝¹ : CommRing T
inst✝ : Algebra R T
this✝² : Algebra P.Ring P.baseChange.Ring := P.algebraBaseChange T
this✝¹ : Algebra S (T ⊗[R] S) := TensorProduct.rightAlgebra
this✝ : Algebra P.Ring (T ⊗[R] S) := compHom (T ⊗[R] S) (algebraMap P.Ring S)
this : IsScalarTower R P.Ring (T ⊗[R] S)
PT : Extension T (T ⊗[R] S) := P.baseChange
⊢ IsPushout R T P.Ring PT.Ring

Tactic:
convert! TensorProduct.isPushout (R := R) (T := P.Ring) (S := T)

Goal state after:
case e'_13
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✝
P : Extension R S
T : Type u_4
inst✝¹ : CommRing T
inst✝ : Algebra R T
this✝² : Algebra P.Ring P.baseChange.Ring := ⋯
this✝¹ : Algebra S (T ⊗[R] S) := ⋯
this✝ : Algebra P.Ring (T ⊗[R] S) := ⋯
this : IsScalarTower R P.Ring (T ⊗[R] S)
PT : Extension T (T ⊗[R] S) := ⋯
e_7✝ : PT.Ring = T ⊗[R] P.Ring
e_9✝ : CommRing.toCommSemiring ≍ TensorProduct.instCommSemiring
⊢ PT.instRingOfIsScalarTower = TensorProduct.instAlgebra
Module: Mathlib.RingTheory.Extension.Cotangent.BaseChange

Goal state before:
pp: case hf₂
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
inst✝ : Module.Flat R T
⊢ Function.Injective ⇑(↑R h1Cotangentι)

Tactic:
exact h1Cotangentι_injective

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

Goal state before:
pp: case hg₂
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
inst✝ : Module.Flat R T
⊢ Function.Injective ⇑h1Cotangentι

Tactic:
exact h1Cotangentι_injective

Goal state after:
Module: Mathlib.Topology.Sheaves.Module

Goal state before:
pp: X : TopCat
U : Opens ↑X
R : TopCat.Sheaf RingCat X
⊢ SheafOfModules (Sheaf.over R U) ≌ SheafOfModules (U.sheafRestrict.obj R)

Tactic:
refine SheafOfModules.pushforwardPushforwardEquivalence (eqv := U.overEquivalence.symm)
    (U.overPullbackSheafEquivOver.app _).inv (U.sheafRestrictSheafEquivOver.app _).inv rfl ?_
  ext : 2
  simp [overPullbackSheafEquivOver, sheafRestrictSheafEquivOver, eqToHom_map, overEquivalence,
    IsOpenMap.functor]

Goal state after:
Module: Mathlib.RingTheory.OrderOfVanishing.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra S R
a : S
h : IsUnit a
x : R
⊢ ord R ((algebraMap S R) a * x) = ord R x

Tactic:
exact ord_mul_of_isUnit_left (RingHom.isUnit_map (algebraMap S R) h) x

Goal state after:
Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : IsNoetherianRing R
inst✝³ : KrullDimLE 1 R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : R
hx : x ≠ 0
⊢ 1 ≤ (ordFrac R) ((algebraMap R K) x)

Tactic:
obtain ⟨m, hm⟩ := ENat.ne_top_iff_exists.mp (ord_ne_top (a := x) (by simpa))

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : IsNoetherianRing R
inst✝³ : KrullDimLE 1 R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : R
hx : x ≠ 0
m : ℕ
hm : ↑m = ord R x
⊢ 1 ≤ (ordFrac R) ((algebraMap R K) x)
Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian

Goal state before:
pp: case hb
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDiscreteValuationRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x y : K
h1 : x + y ≠ 0
⊢ 0 < (valuation K (IsDiscreteValuationRing.maximalIdeal R)) (x + y)

Tactic:
simpa [WithZero.pos_iff_ne_zero]

Goal state after: