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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
h : Function.Surjective ⇑((I • ⊤).mkQ ∘ₗ f)
y : AdicCompletion I N
n : ℕ
⊢ { m // Submodule.Quotient.mk (f m) = (eval I N n) y }

Tactic:
by
    induction n with
    | zero =>
      use 0
      apply_fun (Submodule.Quotient.equiv (I ^ 0 • ⊤) ⊤ (.refl R N) (by simp)).toEquiv
      exact Subsingleton.elim _ _
    | succ n xn =>
      choose z hz using exists_smodEq_pow_smul_top_and_mkQ_eq h
          (y' := eval _ _ (n + 1) y) (by simp) xn.2
      exact ⟨z, hz.2⟩

Goal state after:
Module: Mathlib.RingTheory.Extension.Presentation.Submersive

Goal state before:
pp: R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
ι' : Type u_1
σ' : Type u_2
T : Type u_3
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
Q : PreSubmersivePresentation S T ι' σ'
P : PreSubmersivePresentation R S ι σ
inst✝¹ : Fintype σ
inst✝ : Fintype σ'
i : σ'
j : σ
hmem : (Q.comp P).map (Sum.inl i) ∈ vars ((Q.comp P).relation (Sum.inr j))
⊢ False

Tactic:
apply MvPolynomial.vars_rename at hmem

Goal state after:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
ι' : Type u_1
σ' : Type u_2
T : Type u_3
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
Q : PreSubmersivePresentation S T ι' σ'
P : PreSubmersivePresentation R S ι σ
inst✝¹ : Fintype σ
inst✝ : Fintype σ'
i : σ'
j : σ
hmem : (Q.comp P).map (Sum.inl i) ∈ Finset.image Sum.inr (vars (P.relation j))
⊢ False
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hP : W.Equation P
hPz : P z ≠ 0
⊢ W.negDblY P = W.negDblY P * P z ^ 2 / P z ^ 2

Tactic:
mul_div_cancel_right₀ _ <| pow_ne_zero 2 hPz

Goal state after:
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hP : W.Equation P
hPz : P z ≠ 0
⊢ W.negDblY P = W.negDblY P
Module: Mathlib.RingTheory.Extension.Presentation.Submersive

Goal state before:
pp: case intro.intro
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
P : PreSubmersivePresentation R S ι σ
ι' : Type u_1
σ' : Type u_2
e : ι' ≃ ι
f : σ' ≃ σ
inst✝¹ : Finite σ
inst✝ : Finite σ'
val✝¹ : Fintype σ
val✝ : Fintype σ'
⊢ (P.reindex e f).jacobian = P.jacobian

Tactic:
PreSubmersivePresentation.jacobian_eq_jacobiMatrix_det

Goal state after:
case intro.intro
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
P : PreSubmersivePresentation R S ι σ
ι' : Type u_1
σ' : Type u_2
e : ι' ≃ ι
f : σ' ≃ σ
inst✝¹ : Finite σ
inst✝ : Finite σ'
val✝¹ : Fintype σ
val✝ : Fintype σ'
⊢ (algebraMap (P.reindex e f).Ring S) (P.reindex e f).jacobiMatrix.det = (algebraMap P.Ring S) P.jacobiMatrix.det
Module: Mathlib.RingTheory.Extension.Presentation.Submersive

Goal state before:
pp: R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Finite σ
P : SubmersivePresentation R S ι σ
this : Fintype σ
⊢ (LinearMap.toMatrix' P.aevalDifferential).det = (algebraMap P.Ring S) P.jacobiMatrix.det

Tactic:
aevalDifferential_toMatrix'_eq_mapMatrix_jacobiMatrix,

Goal state after:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Finite σ
P : SubmersivePresentation R S ι σ
this : Fintype σ
⊢ ((aeval P.val).mapMatrix P.jacobiMatrix).det = (algebraMap P.Ring S) P.jacobiMatrix.det
Module: Mathlib.RingTheory.Extension.Presentation.Core

Goal state before:
pp: R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P✝ : Presentation R S ι σ
inst✝⁶ : Finite σ
P : SubmersivePresentation R S ι σ
R₀ : Type u_5
inst✝⁵ : CommRing R₀
inst✝⁴ : Algebra R₀ R
inst✝³ : Algebra R₀ S
inst✝² : IsScalarTower R₀ R S
inst✝¹ : P.HasCoeffs R₀
inst✝ : FaithfulSMul R₀ R
this✝ : Fintype σ := Fintype.ofFinite σ
this :
  (Ideal.Quotient.mk (Ideal.span (Set.range (Presentation.relationOfHasCoeffs R₀)))) (P.jacobianOfHasCoeffs R₀) *
      (Ideal.Quotient.mk (Ideal.span (Set.range (Presentation.relationOfHasCoeffs R₀)))) (P.invJacobianOfHasCoeffs R₀) =
    1
⊢ (P.ofHasCoeffs R₀).jacobian =
    (Ideal.Quotient.mk (Ideal.span (Set.range (Presentation.relationOfHasCoeffs R₀)))) (P.jacobianOfHasCoeffs R₀)

Tactic:
PreSubmersivePresentation.jacobian_eq_jacobiMatrix_det

Goal state after:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P✝ : Presentation R S ι σ
inst✝⁶ : Finite σ
P : SubmersivePresentation R S ι σ
R₀ : Type u_5
inst✝⁵ : CommRing R₀
inst✝⁴ : Algebra R₀ R
inst✝³ : Algebra R₀ S
inst✝² : IsScalarTower R₀ R S
inst✝¹ : P.HasCoeffs R₀
inst✝ : FaithfulSMul R₀ R
this✝ : Fintype σ := Fintype.ofFinite σ
this :
  (Ideal.Quotient.mk (Ideal.span (Set.range (Presentation.relationOfHasCoeffs R₀)))) (P.jacobianOfHasCoeffs R₀) *
      (Ideal.Quotient.mk (Ideal.span (Set.range (Presentation.relationOfHasCoeffs R₀)))) (P.invJacobianOfHasCoeffs R₀) =
    1
⊢ (algebraMap (P.ofHasCoeffs R₀).Ring (Presentation.ModelOfHasCoeffs R₀)) (P.ofHasCoeffs R₀).jacobiMatrix.det =
    (Ideal.Quotient.mk (Ideal.span (Set.range (Presentation.relationOfHasCoeffs R₀)))) (P.jacobianOfHasCoeffs R₀)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Equation P
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z = Q y * P z
hy' : P y * Q z = W.negY Q * P z
⊢ W.negDblY P = W.negDblY P * P z ^ 2 / P z ^ 2

Tactic:
mul_div_cancel_right₀ _ <| pow_ne_zero 2 hPz

Goal state after:
F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Equation P
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z = Q y * P z
hy' : P y * Q z = W.negY Q * P z
⊢ W.negDblY P = W.negDblY P
Module: Mathlib.RingTheory.Extension.Cotangent.LocalizationAway

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
ι : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
g : S
inst✝ : IsLocalization.Away g T
P : Generators R S ι
f : P.Ring
h : (algebraMap P.Ring S) f = g
⊢ Ideal.span {C g * X () - 1} =
    Ideal.span
      {((localizationAway T g).ofComp P).toAlgHom ((rename Sum.inr) f) *
            ((localizationAway T g).ofComp P).val (Sum.inl ()) -
          1}

Tactic:
toAlgHom_ofComp_rename,

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
ι : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
g : S
inst✝ : IsLocalization.Away g T
P : Generators R S ι
f : P.Ring
h : (algebraMap P.Ring S) f = g
⊢ Ideal.span {C g * X () - 1} =
    Ideal.span {C ((algebraMap P.Ring S) f) * ((localizationAway T g).ofComp P).val (Sum.inl ()) - 1}
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Equation P
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z = Q y * P z
hy' : P y * Q z = W.negY Q * P z
⊢ W.dblY P = W.dblY P * P z ^ 2 / P z ^ 2

Tactic:
mul_div_cancel_right₀ _ <| pow_ne_zero 2 hPz

Goal state after:
F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Equation P
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z = Q y * P z
hy' : P y * Q z = W.negY Q * P z
⊢ W.dblY P = W.dblY P
Module: Mathlib.RingTheory.Extension.Cotangent.LocalizationAway

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
ι : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
g : S
inst✝ : IsLocalization.Away g T
P : Generators R S ι
f : P.Ring
h : (algebraMap P.Ring S) f = g
this :
  (localizationAway T g).ker =
    Ideal.map ((localizationAway T g).ofComp P).toAlgHom (Ideal.span {(rename Sum.inr) f * X (Sum.inl ()) - 1})
⊢ RingHom.ker ((localizationAway T g).ofComp P).toAlgHom ⊔
      (Ideal.span {(rename Sum.inr) f * X (Sum.inl ()) - 1} ⊔ RingHom.ker ((localizationAway T g).ofComp P).toAlgHom) =
    RingHom.ker ((localizationAway T g).ofComp P).toAlgHom ⊔ Ideal.span {(rename Sum.inr) f * X (Sum.inl ()) - 1}

Tactic:
← sup_assoc

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
ι : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
g : S
inst✝ : IsLocalization.Away g T
P : Generators R S ι
f : P.Ring
h : (algebraMap P.Ring S) f = g
this :
  (localizationAway T g).ker =
    Ideal.map ((localizationAway T g).ofComp P).toAlgHom (Ideal.span {(rename Sum.inr) f * X (Sum.inl ()) - 1})
⊢ RingHom.ker ((localizationAway T g).ofComp P).toAlgHom ⊔ Ideal.span {(rename Sum.inr) f * X (Sum.inl ()) - 1} ⊔
      RingHom.ker ((localizationAway T g).ofComp P).toAlgHom =
    RingHom.ker ((localizationAway T g).ofComp P).toAlgHom ⊔ Ideal.span {(rename Sum.inr) f * X (Sum.inl ()) - 1}
Module: Mathlib.RingTheory.Extension.Cotangent.LocalizationAway

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
ι : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
g : S
inst✝ : IsLocalization.Away g T
P : Generators R S ι
⊢ Function.Injective
    ⇑(LinearMap.liftBaseChange T (Extension.Cotangent.map ((localizationAway T g).toComp P).toExtensionHom))

Tactic:
set Q := Generators.localizationAway T g
  algebraize [((Generators.localizationAway T g).toComp P).toAlgHom.toRingHom]
  let f : P.Ring ⧸ P.ker ^ 2 := P.σ g
  let π := compLocalizationAwayAlgHom T g P
  refine IsLocalizedModule.injective_of_map_zero (Submonoid.powers g)
    (TensorProduct.mk S T P.toExtension.Cotangent 1) (fun x hx ↦ ?_)
  obtain ⟨x, rfl⟩ := Algebra.Extension.Cotangent.mk_surjective x
  suffices h : algebraMap P.Ring (Localization.Away f) x.val = 0 by
    rw [IsScalarTower.algebraMap_apply _ (P.Ring ⧸ P.ker ^ 2) _,
      IsLocalization.map_eq_zero_iff (Submonoid.powers f) (Localization.Away f)] at h
    obtain ⟨⟨m, ⟨n, rfl⟩⟩, hm⟩ := h
    rw [IsLocalizedModule.eq_zero_iff (Submonoid.powers g)]
    use ⟨g ^ n, n, rfl⟩
    dsimp [f] at hm
    rw [← map_pow, ← map_mul, Ideal.Quotient.eq_zero_iff_mem] at hm
    simp only [Submonoid.smul_def]
    rw [show g = algebraMap P.Ring S (P.σ g) by simp, ← map_pow, algebraMap_smul, ← map_smul,
      Extension.Cotangent.mk_eq_zero_iff]
    simpa using! hm
  rw [← compLocalizationAwayAlgHom_toAlgHom_toComp (T := T)]
  apply sq_ker_comp_le_ker_compLocalizationAwayAlgHom
  simpa only [LinearEquiv.coe_coe, LinearMap.ringLmapEquivSelf_symm_apply,
    mk_apply, lift.tmul, LinearMap.coe_restrictScalars, LinearMap.coe_smulRight,
    Module.End.one_apply, LinearMap.smul_apply, one_smul, Algebra.Extension.Cotangent.map_mk,
    Extension.Cotangent.mk_eq_zero_iff] using! hx

Goal state after:
Module: Mathlib.RingTheory.RingHom.StandardSmooth

Goal state before:
pp: case h₁
⊢ RespectsIso @IsStandardSmooth

pp: case h₂
⊢ ∀ ⦃R S T : Type u_2⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
    [inst_4 : Algebra R T], (algebraMap R T).IsStandardSmooth → (algebraMap S (S ⊗[R] T)).IsStandardSmooth

Tactic:
· exact isStandardSmooth_respectsIso

Goal state after:
case h₂
⊢ ∀ ⦃R S T : Type u_2⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
    [inst_4 : Algebra R T], (algebraMap R T).IsStandardSmooth → (algebraMap S (S ⊗[R] T)).IsStandardSmooth
Module: Mathlib.RingTheory.RingHom.StandardSmooth

Goal state before:
pp: n : ℕ
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Algebra.IsStandardSmoothOfRelativeDimension n R S
this : (α : Type) → [_root_.Finite α] → Fintype α := Fintype.ofFinite
ι σ : Type
w✝¹ : _root_.Finite σ
w✝ : _root_.Finite ι
P : Algebra.SubmersivePresentation R S ι σ
e : P.dimension = n
⊢ Nat.card ι - (Set.range P.map).ncard = n

Tactic:
Set.ncard_range_of_injective P.map_inj,

Goal state after:
n : ℕ
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Algebra.IsStandardSmoothOfRelativeDimension n R S
this : (α : Type) → [_root_.Finite α] → Fintype α := Fintype.ofFinite
ι σ : Type
w✝¹ : _root_.Finite σ
w✝ : _root_.Finite ι
P : Algebra.SubmersivePresentation R S ι σ
e : P.dimension = n
⊢ Nat.card ι - Nat.card σ = n
Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth

Goal state before:
pp: case hQi
X Y : Scheme
f : X ⟶ Y
this :
  HasRingHomProperty @Smooth fun {R S} [CommRing R] [CommRing S] ↦
    Locally fun {R S} [CommRing R] [CommRing S] ↦ IsStandardSmooth
⊢ RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ IsStandardSmooth

Tactic:
· exact isStandardSmooth_respectsIso

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

Goal state before:
pp: case refine_1
X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFinitePresentation f
x : ↥X
H : (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).FormallySmooth
U : TopologicalSpace.Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : f x ∈ ↑U
V : TopologicalSpace.Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hVU : ↑V ⊆ ⇑f ⁻¹' U.carrier
this✝ : (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).FinitePresentation
algInst✝ : Algebra ↑Γ(Y, U) ↑Γ(X, V) := (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).toAlgebra
algebraizeInst✝ : Algebra.FinitePresentation ↑Γ(Y, U) ↑Γ(X, V)
this : Algebra.IsSmoothAt (↑Γ(Y, U)) (IsAffineOpen.primeIdealOf hV ⟨x, hxV⟩).asIdeal
r : ↑Γ(X, V)
hrx : r ∉ (IsAffineOpen.primeIdealOf hV ⟨x, hxV⟩).asIdeal
hr : Algebra.Smooth (↑Γ(Y, U)) (Localization.Away r)
⊢ x ∈ X.basicOpen r

Tactic:
rwa [← PrimeSpectrum.mem_basicOpen, IsAffineOpen.primeIdealOf,
      ← hV.fromSpec_preimage_basicOpen, Scheme.Hom.mem_preimage, ← Scheme.Hom.comp_apply,
      IsAffineOpen.isoSpec_hom, IsAffineOpen.toSpecΓ_fromSpec] at hrx

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ IsProper f ↔ (@IsSeparated ⊓ @UniversallyClosed ⊓ @LocallyOfFiniteType) f

Tactic:
isProper_iff,

Goal state after:
X Y : Scheme
f : X ⟶ Y
⊢ IsSeparated f ∧ UniversallyClosed f ∧ LocallyOfFiniteType f ↔
    (@IsSeparated ⊓ @UniversallyClosed ⊓ @LocallyOfFiniteType) f
Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFinitePresentation f
x : ↥X
H : (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).FormallySmooth
U : TopologicalSpace.Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : f x ∈ ↑U
V : TopologicalSpace.Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hVU : ↑V ⊆ ⇑f ⁻¹' U.carrier
this✝¹ : (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).FinitePresentation
algInst✝ : Algebra ↑Γ(Y, U) ↑Γ(X, V) := (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).toAlgebra
algebraizeInst✝ : Algebra.FinitePresentation ↑Γ(Y, U) ↑Γ(X, V)
this✝ : Algebra.IsSmoothAt (↑Γ(Y, U)) (IsAffineOpen.primeIdealOf hV ⟨x, hxV⟩).asIdeal
r : ↑Γ(X, V)
hrx : r ∉ (IsAffineOpen.primeIdealOf hV ⟨x, hxV⟩).asIdeal
hr : (algebraMap (↑Γ(Y, U)) (Localization.Away r)).Smooth
this : IsLocalization.Away r ↑Γ(X, X.basicOpen r)
x✝ : ↑Γ(Y, U)
⊢ (CommRingCat.Hom.hom (Scheme.Hom.appLE f U (X.basicOpen r) ⋯)) x✝ =
    (IsLocalization.map (↑Γ(X, X.basicOpen r)) (RingHom.id ↑Γ(X, V)) ⋯)
      ((algebraMap (↑Γ(Y, U)) (Localization.Away r)) x✝)

Tactic:
simp only [IsScalarTower.algebraMap_apply Γ(Y, U) Γ(X, V) (Localization _),
      IsLocalization.map_eq]

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFinitePresentation f
x : ↥X
H : (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).FormallySmooth
U : TopologicalSpace.Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : f x ∈ ↑U
V : TopologicalSpace.Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hVU : ↑V ⊆ ⇑f ⁻¹' U.carrier
this✝¹ : (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).FinitePresentation
algInst✝ : Algebra ↑Γ(Y, U) ↑Γ(X, V) := (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).toAlgebra
algebraizeInst✝ : Algebra.FinitePresentation ↑Γ(Y, U) ↑Γ(X, V)
this✝ : Algebra.IsSmoothAt (↑Γ(Y, U)) (IsAffineOpen.primeIdealOf hV ⟨x, hxV⟩).asIdeal
r : ↑Γ(X, V)
hrx : r ∉ (IsAffineOpen.primeIdealOf hV ⟨x, hxV⟩).asIdeal
hr : (algebraMap (↑Γ(Y, U)) (Localization.Away r)).Smooth
this : IsLocalization.Away r ↑Γ(X, X.basicOpen r)
x✝ : ↑Γ(Y, U)
⊢ (CommRingCat.Hom.hom (Scheme.Hom.appLE f U (X.basicOpen r) ⋯)) x✝ =
    (algebraMap ↑Γ(X, V) ↑Γ(X, X.basicOpen r)) ((RingHom.id ↑Γ(X, V)) ((algebraMap ↑Γ(Y, U) ↑Γ(X, V)) x✝))
Module: Mathlib.AlgebraicGeometry.Morphisms.LocalClosure

Goal state before:
pp: W P Q : MorphismProperty Scheme
X Y : Scheme
inst✝³ : W.IsStableUnderBaseChange
inst✝² : Scheme.IsJointlySurjectivePreserving W
inst✝¹ : P.RespectsIso
inst✝ : P.RespectsLeft IsOpenImmersion
⊢ IsZariskiLocalAtSource (sourceLocalClosure IsOpenImmersion P)

Tactic:
refine .mk_of_iff_of_zeroHypercover fun f 𝒰 ↦ ?_
  refine ⟨fun ⟨𝒱, h⟩ ↦ fun i ↦ ⟨𝒱.pullback₁ (𝒰.f i), fun j ↦ ?_⟩, fun h ↦ ?_⟩
  · simpa [pullback.condition_assoc] using
      RespectsLeft.precomp (Q := @IsOpenImmersion) _ inferInstance _ (h j)
  · choose 𝒱 h𝒱 using h
    exact ⟨(Scheme.Cover.ulift 𝒰).bind (fun i ↦ Scheme.Cover.ulift (𝒱 _)), fun i ↦ h𝒱 _ _⟩

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

Goal state before:
pp: case h
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsDomain R
inst✝ : FaithfulSMul R S
i : ℕ
H : ∀ {q : S[X]}, IsAlmostIntegral R[X] q → IsAlmostIntegral R q.leadingCoeff
n : ℕ
IH : ∀ m < n, ∀ {p : S[X]}, IsAlmostIntegral R[X] p → p.natDegree = m → IsAlmostIntegral R (p.coeff i)
p : S[X]
hp : IsAlmostIntegral R[X] p
hn : p.natDegree = n
⊢ IsAlmostIntegral R (p.coeff i)

Tactic:
by_cases hp' : p.natDegree = 0
  · obtain ⟨p, rfl⟩ := natDegree_eq_zero.mp hp'
    simp only [coeff_C]
    split_ifs with h
    · simpa using H hp
    · exact (completeIntegralClosure R S).zero_mem
  by_cases hi : i = p.natDegree
  · simp [hi, H hp]
  have : IsAlmostIntegral R[X] p.eraseLead := by
    rw [← self_sub_monomial_natDegree_leadingCoeff, ← mem_completeIntegralClosure,
      ← C_mul_X_pow_eq_monomial, ← map_X (algebraMap R S), ← Polynomial.map_pow]
    refine sub_mem hp (mul_mem ?_ (algebraMap_mem (R := R[X]) _ _))
    obtain ⟨r, hr, hr'⟩ := H hp
    refine ⟨C r, by simpa using hr, fun n ↦ ?_⟩
    obtain ⟨s, hs⟩ := hr' n
    exact ⟨C s, by simp [Algebra.smul_def, hs]⟩
  simpa [hi, eraseLead_coeff_of_ne] using
    IH (p := p.eraseLead) _ (p.eraseLead_natDegree_le.trans_lt (by lia)) this rfl

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : S[X]
hp : IsIntegral R[X] p
i✝ : ℕ
a✝¹ : Nontrivial R
a✝ : Nontrivial S
hp0 : p ≠ 0
q : R[X][X] := minpoly R[X] p
m : ℕ := (q.support.sup fun i ↦ (q.coeff i).natDegree) + p.natDegree + 1
hm₁ : ∀ (i : ℕ), (q.coeff i).natDegree < m
i : ℕ
hi : i < q.natDegree
⊢ (q.coeff i).natDegree + m * i < m * (i + 1)

Tactic:
have := hm₁ i

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : S[X]
hp : IsIntegral R[X] p
i✝ : ℕ
a✝¹ : Nontrivial R
a✝ : Nontrivial S
hp0 : p ≠ 0
q : R[X][X] := minpoly R[X] p
m : ℕ := (q.support.sup fun i ↦ (q.coeff i).natDegree) + p.natDegree + 1
hm₁ : ∀ (i : ℕ), (q.coeff i).natDegree < m
i : ℕ
hi : i < q.natDegree
this : (q.coeff i).natDegree < m
⊢ (q.coeff i).natDegree + m * i < m * (i + 1)
Module: Mathlib.RingTheory.LocalRing.ResidueField.Polynomial

Goal state before:
pp: case refine_3.h₁
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
I : Ideal R
inst✝⁴ : I.IsPrime
J : Ideal R[X]
inst✝³ : J.IsPrime
inst✝² : J.LiesOver I
inst✝¹ : Algebra (Localization.AtPrime I) (Localization.AtPrime J)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra I J
hJ : J = Ideal.map C I
f : J.ResidueField →+* RatFunc I.ResidueField :=
  Ideal.ResidueField.lift J
    ((algebraMap I.ResidueField[X] (RatFunc I.ResidueField)).comp (mapRingHom (algebraMap R I.ResidueField))) ⋯ ⋯
hf : f.comp (algebraMap I.ResidueField J.ResidueField) = algebraMap I.ResidueField (RatFunc I.ResidueField)
x✝ : R
⊢ (((↑((RatFunc.liftAlgHom (aeval ((algebraMap R[X] J.ResidueField) X)) ⋯).comp
                  { toRingHom := f, commutes' := ⋯ })).comp
            (algebraMap R[X] J.ResidueField)).comp
        C)
      x✝ =
    (((↑(AlgHom.id I.ResidueField J.ResidueField)).comp (algebraMap R[X] J.ResidueField)).comp C) x✝

pp: case h₂
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
I : Ideal R
inst✝⁴ : I.IsPrime
J : Ideal R[X]
inst✝³ : J.IsPrime
inst✝² : J.LiesOver I
inst✝¹ : Algebra (Localization.AtPrime I) (Localization.AtPrime J)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra I J
hJ : J = Ideal.map C I
f : J.ResidueField →+* RatFunc I.ResidueField := ⋯
hf : f.comp (algebraMap I.ResidueField J.ResidueField) = algebraMap I.ResidueField (RatFunc I.ResidueField)
⊢ ((↑((RatFunc.liftAlgHom (aeval ((algebraMap R[X] J.ResidueField) X)) ⋯).comp { toRingHom := f, commutes' := ⋯ })).comp
        (algebraMap R[X] J.ResidueField))
      X =
    ((↑(AlgHom.id I.ResidueField J.ResidueField)).comp (algebraMap R[X] J.ResidueField)) X

Tactic:
· simp [f, RatFunc.liftAlgHom, ← IsScalarTower.algebraMap_apply]; rfl

Goal state after:
case h₂
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
I : Ideal R
inst✝⁴ : I.IsPrime
J : Ideal R[X]
inst✝³ : J.IsPrime
inst✝² : J.LiesOver I
inst✝¹ : Algebra (Localization.AtPrime I) (Localization.AtPrime J)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra I J
hJ : J = Ideal.map C I
f : J.ResidueField →+* RatFunc I.ResidueField := ⋯
hf : f.comp (algebraMap I.ResidueField J.ResidueField) = algebraMap I.ResidueField (RatFunc I.ResidueField)
⊢ ((↑((RatFunc.liftAlgHom (aeval ((algebraMap R[X] J.ResidueField) X)) ⋯).comp { toRingHom := f, commutes' := ⋯ })).comp
        (algebraMap R[X] J.ResidueField))
      X =
    ((↑(AlgHom.id I.ResidueField J.ResidueField)).comp (algebraMap R[X] J.ResidueField)) X
Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski

Goal state before:
pp: X : Scheme
F : X.AffineZariskiSiteᵒᵖ ⥤ CommRingCat
α : (toOpensFunctor X).op ⋙ X.presheaf ⟶ F
⊢ NatTrans.Coequifibered α ↔
    ∀ (U : X.AffineZariskiSite) (f : ↑Γ(X, ↑U)),
      IsPushout (X.presheaf.map (homOfLE ⋯).op) (α.app (Opposite.op U)) (α.app (Opposite.op (U.basicOpen f)))
        (F.map (homOfLE ⋯).op)

pp: X : Scheme
F : X.AffineZariskiSiteᵒᵖ ⥤ CommRingCat
α : (toOpensFunctor X).op ⋙ X.presheaf ⟶ F
⊢ (∀ (U : X.AffineZariskiSite) (f : ↑Γ(X, ↑U)),
      IsPushout (X.presheaf.map (homOfLE ⋯).op) (α.app (Opposite.op U)) (α.app (Opposite.op (U.basicOpen f)))
        (F.map (homOfLE ⋯).op)) ↔
    ∀ (U : X.AffineZariskiSite) (f : ↑Γ(X, ↑U)),
      IsLocalization.Away ((ConcreteCategory.hom (α.app (Opposite.op U))) f) ↑(F.obj (Opposite.op (U.basicOpen f)))

Tactic:
· refine ⟨fun H U f ↦ H (homOfLE (U.basicOpen_le f)).op, fun H ⟨V⟩ ⟨U⟩ ⟨f, hf⟩ ↦ ?_⟩
    obtain rfl : V.basicOpen f = U := Subtype.ext hf
    exact H V f

Goal state after:
X : Scheme
F : X.AffineZariskiSiteᵒᵖ ⥤ CommRingCat
α : (toOpensFunctor X).op ⋙ X.presheaf ⟶ F
⊢ (∀ (U : X.AffineZariskiSite) (f : ↑Γ(X, ↑U)),
      IsPushout (X.presheaf.map (homOfLE ⋯).op) (α.app (Opposite.op U)) (α.app (Opposite.op (U.basicOpen f)))
        (F.map (homOfLE ⋯).op)) ↔
    ∀ (U : X.AffineZariskiSite) (f : ↑Γ(X, ↑U)),
      IsLocalization.Away ((ConcreteCategory.hom (α.app (Opposite.op U))) f) ↑(F.obj (Opposite.op (U.basicOpen f)))