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

Goal state before:
pp: ⊢ HoldsForLocalizationAway fun {R S} [CommRing R] [CommRing S] ↦ Smooth

Tactic:
introv R h
  rw [smooth_algebraMap]
  exact ⟨Algebra.FormallySmooth.of_isLocalization (.powers r),
    IsLocalization.Away.finitePresentation r⟩

Goal state after:
Module: Mathlib.RingTheory.Kaehler.TensorProduct

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : Algebra S B
inst✝¹ : IsScalarTower R A B
inst✝ : IsScalarTower R S B
h : Algebra.IsPushout R S A B
this : Algebra.IsPushout R A S B
e₁ : B ⊗[A] Ω[A⁄R] ≃ₗ[A] Ω[A⁄R] ⊗[R] S :=
  AlgebraTensorModule.congr (↑(Algebra.IsPushout.equiv R A S B).symm) (LinearEquiv.refl A Ω[A⁄R]) ≪≫ₗ
      TensorProduct.comm A (A ⊗[R] S) Ω[A⁄R] ≪≫ₗ
    AlgebraTensorModule.cancelBaseChange R A A Ω[A⁄R] S
e₂ : B ⊗[A] Ω[A⁄R] ≃ₗ[R] Ω[B⁄S] :=
  LinearEquiv.restrictScalars R e₁ ≪≫ₗ TensorProduct.comm R Ω[A⁄R] S ≪≫ₗ
    LinearEquiv.restrictScalars R (tensorKaehlerEquivBase R S A B)
⊢ ∀ (m : B) (x : B ⊗[A] Ω[A⁄R]), (↑e₂).toFun (m • x) = (RingHom.id B) m • (↑e₂).toFun x

Tactic:
intro m x

Goal state after:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : Algebra S B
inst✝¹ : IsScalarTower R A B
inst✝ : IsScalarTower R S B
h : Algebra.IsPushout R S A B
this : Algebra.IsPushout R A S B
e₁ : B ⊗[A] Ω[A⁄R] ≃ₗ[A] Ω[A⁄R] ⊗[R] S :=
  AlgebraTensorModule.congr (↑(Algebra.IsPushout.equiv R A S B).symm) (LinearEquiv.refl A Ω[A⁄R]) ≪≫ₗ
      TensorProduct.comm A (A ⊗[R] S) Ω[A⁄R] ≪≫ₗ
    AlgebraTensorModule.cancelBaseChange R A A Ω[A⁄R] S
e₂ : B ⊗[A] Ω[A⁄R] ≃ₗ[R] Ω[B⁄S] :=
  LinearEquiv.restrictScalars R e₁ ≪≫ₗ TensorProduct.comm R Ω[A⁄R] S ≪≫ₗ
    LinearEquiv.restrictScalars R (tensorKaehlerEquivBase R S A B)
m : B
x : B ⊗[A] Ω[A⁄R]
⊢ (↑e₂).toFun (m • x) = (RingHom.id B) m • (↑e₂).toFun x
Module: Mathlib.RingTheory.AdicCompletion.Algebra

Goal state before:
pp: R : Type u_4
S : Type u_5
inst✝¹ : NonAssocSemiring R
inst✝ : CommRing S
I : Ideal S
f : (n : ℕ) → R →+* S ⧸ I ^ n
hf : ∀ {m n : ℕ} (hle : m ≤ n), (Ideal.Quotient.factorPow I hle).comp (f n) = f m
n : ℕ
x : R
⊢ (evalₐ I n) ((liftRingHom I f ⋯) x) = (f n) x

Tactic:
rw [← factor_eval_eq_evalₐ I _ (le_of_eq (Ideal.mul_top _))]
  simp [liftRingHom, eval]

Goal state after:
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 ι σ
R₀ : Type u_5
inst✝⁴ : CommRing R₀
inst✝³ : Algebra R₀ R
inst✝² : Algebra R₀ S
inst✝¹ : IsScalarTower R₀ R S
inst✝ : P.HasCoeffs R₀
x : σ
⊢ P.relation x ∈ Set.range ⇑(MvPolynomial.map (algebraMap R₀ R))

Tactic:
rw [MvPolynomial.mem_range_map_iff_coeffs_subset]

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 ι σ
R₀ : Type u_5
inst✝⁴ : CommRing R₀
inst✝³ : Algebra R₀ R
inst✝² : Algebra R₀ S
inst✝¹ : IsScalarTower R₀ R S
inst✝ : P.HasCoeffs R₀
x : σ
⊢ ↑(MvPolynomial.coeffs (P.relation x)) ⊆ Set.range ⇑(algebraMap R₀ R)
Module: Mathlib.RingTheory.RingHom.Etale

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ (algebraMap R S).Etale ↔ Algebra.Etale R S

Tactic:
RingHom.Etale,

Goal state after:
R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ Algebra.Etale R S ↔ Algebra.Etale R S
Module: Mathlib.RingTheory.Extension.Cotangent.Basis

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
inst✝ : Nontrivial S
⊢ (Extension.Cotangent.map ((localizationAway S D.gbar).ofComp D.presLeft.toGenerators).toExtensionHom)
      (Extension.Cotangent.mk ⟨D.pres.relation (Sum.inl ()), ⋯⟩) =
    cMulXSubOneCotangent S D.gbar

Tactic:
by
  simp_rw [Extension.Cotangent.map_mk, Generators.Hom.toExtensionHom_toAlgHom_apply]
  congr 2
  have : Nontrivial D.T := inferInstance
  dsimp only [T, Generators.toExtension_Ring, Generators.toExtension_commRing] at this
  rw [pres, presLeft, presRight, Presentation.relation_comp_localizationAway_inl]
  · exact Generators.toAlgHom_ofComp_localizationAway _ _
  · rw [Presentation.naive, Generators.naive_σ];
    simp
  · rw [Presentation.naive, Generators.naive_σ]
    simp

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

Goal state before:
pp: case inl
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
inst✝ : Nontrivial S
r : Unit
⊢ D.basis (Sum.inl r) = Extension.Cotangent.mk ⟨D.pres.relation (Sum.inl r), ⋯⟩

Tactic:
rw [basis_inl, cotangentEquivProd_symm_apply]
    exact cotangentCompLocalizationAwayEquiv_symm_inr _ _ _

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: F : Type u
inst✝¹ : Field F
W : Projective F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ≠ Q x * P z
⊢ W.addX P Q / W.addZ P Q =
    W.toAffine.addX (P x / P z) (Q x / Q z) (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z))

Tactic:
by
  rw [addX_eq hP hQ hPz hQz, addZ_eq hP hQ hPz hQz, toAffine_slope_of_ne hPz hQz hx,
    toAffine_addX_of_ne hPz hQz <| sub_ne_zero.mpr hx]

Goal state after:
Module: Mathlib.RingTheory.Smooth.NoetherianDescent

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
A : Type u
B : Type u_2
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Smooth A B
⊢ ∃ A₀ B₀ x x_1, FiniteType R ↥A₀ ∧ Smooth (↥A₀) B₀ ∧ Nonempty (B ≃ₐ[A] A ⊗[↥A₀] B₀)

Tactic:
obtain ⟨A₀, B₀, _, _, h0, h1, h2⟩ := exists_subalgebra_fg R A B

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
A : Type u
B : Type u_2
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Smooth A B
A₀ : Subalgebra R A
B₀ : Type u
w✝¹ : CommRing B₀
w✝ : Algebra (↥A₀) B₀
h0 : A₀.FG
h1 : Smooth (↥A₀) B₀
h2 : Nonempty (B ≃ₐ[A] A ⊗[↥A₀] B₀)
⊢ ∃ A₀ B₀ x x_1, FiniteType R ↥A₀ ∧ Smooth (↥A₀) B₀ ∧ Nonempty (B ≃ₐ[A] A ⊗[↥A₀] B₀)
Module: Mathlib.RingTheory.RingHom.LocallyStandardSmooth

Goal state before:
pp: R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
⊢ f.Smooth ↔ Locally (fun {R S} [CommRing R] [CommRing S] ↦ IsStandardSmooth) f

Tactic:
refine ⟨fun hf ↦ hf.locally_isStandardSmooth, fun hf ↦ ?_⟩

Goal state after:
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Locally (fun {R S} [CommRing R] [CommRing S] ↦ IsStandardSmooth) f
⊢ f.Smooth
Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth

Goal state before:
pp: case h
n m : ℕ
X Y : Scheme
f : X ⟶ Y
⊢ ∀ {X Y : Scheme} (f : X ⟶ Y),
    SmoothOfRelativeDimension n f ↔
      ∀ (x : ↥X),
        ∃ U V,
          ∃ (_ : x ∈ ↑V) (e : ↑V ≤ f ⁻¹ᵁ ↑U),
            IsStandardSmoothOfRelativeDimension n (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e))

Tactic:
· intro X Y f
    rw [smoothOfRelativeDimension_iff]
    congr!
    simp [Subtype.exists]
    grind [Scheme.affineOpens]

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Descent

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
P : MorphismProperty C
inst✝³ : (isomorphisms C).DescendsAlong P
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : HasEqualizers C
inst✝ : HasPullbacks C
X Y S T : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
v : T ⟶ S
hv : P v
H : pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯ = pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯
⊢ IsIso (equalizer.ι f g)

Tactic:
change MorphismProperty.isomorphisms C _

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
P : MorphismProperty C
inst✝³ : (isomorphisms C).DescendsAlong P
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : HasEqualizers C
inst✝ : HasPullbacks C
X Y S T : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
v : T ⟶ S
hv : P v
H : pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯ = pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯
⊢ isomorphisms C (equalizer.ι f g)
Module: Mathlib.FieldTheory.SeparablyGenerated

Goal state before:
pp: case inr.hi
k : Type u_1
K : Type u_2
inst✝⁴ : Field k
inst✝³ : Field K
inst✝² : Algebra k K
inst✝¹ : PerfectField k
inst✝ : Algebra.EssFiniteType k K
p : ℕ
hp : Fact (Nat.Prime p)
hpk : CharP k p
this✝ : ExpChar k p
this : CharP K p
s : Finset K
hs : LinearIndepOn k id ↑s
⊢ ∀ (r : k), (frobeniusEquiv k p).symm r = 0 → r = 0

Tactic:
simp [frobenius, Algebra.smul_def, mul_pow, ← map_pow, frobeniusEquiv_symm_pow]

Goal state after:
Module: Mathlib.FieldTheory.SeparablyGenerated

Goal state before:
pp: case inr.hj
k : Type u_1
K : Type u_2
inst✝⁴ : Field k
inst✝³ : Field K
inst✝² : Algebra k K
inst✝¹ : PerfectField k
inst✝ : Algebra.EssFiniteType k K
p : ℕ
hp : Fact (Nat.Prime p)
hpk : CharP k p
this✝ : ExpChar k p
this : CharP K p
s : Finset K
hs : LinearIndepOn k id ↑s
⊢ ∀ (m : K), (frobenius K p).toAddMonoidHom m = 0 → m = 0

Tactic:
simp [frobenius, Algebra.smul_def, mul_pow, ← map_pow, frobeniusEquiv_symm_pow]

Goal state after:
Module: Mathlib.FieldTheory.SeparablyGenerated

Goal state before:
pp: case inr.hc
k : Type u_1
K : Type u_2
inst✝⁴ : Field k
inst✝³ : Field K
inst✝² : Algebra k K
inst✝¹ : PerfectField k
inst✝ : Algebra.EssFiniteType k K
p : ℕ
hp : Fact (Nat.Prime p)
hpk : CharP k p
this✝ : ExpChar k p
this : CharP K p
s : Finset K
hs : LinearIndepOn k id ↑s
⊢ ∀ (r : k) (m : K),
    (frobenius K p).toAddMonoidHom ((frobeniusEquiv k p).symm r • m) = r • (frobenius K p).toAddMonoidHom m

Tactic:
simp [frobenius, Algebra.smul_def, mul_pow, ← map_pow, frobeniusEquiv_symm_pow]

Goal state after:
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Descent

Goal state before:
pp: R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : (algebraMap R S).FaithfullyFlat
H : Function.Injective ⇑(algebraMap S (S ⊗[R] T))
⊢ Function.Injective ⇑(algebraMap R T)

Tactic:
faithfullyFlat_algebraMap_iff

Goal state after:
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Module.FaithfullyFlat R S
H : Function.Injective ⇑(algebraMap S (S ⊗[R] T))
⊢ Function.Injective ⇑(algebraMap R T)
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Descent

Goal state before:
pp: R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : (algebraMap R S).FaithfullyFlat
H : Function.Surjective ⇑(algebraMap S (S ⊗[R] T))
⊢ Function.Surjective ⇑(algebraMap R T)

Tactic:
faithfullyFlat_algebraMap_iff

Goal state after:
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Module.FaithfullyFlat R S
H : Function.Surjective ⇑(algebraMap S (S ⊗[R] T))
⊢ Function.Surjective ⇑(algebraMap R T)
Module: Mathlib.RingTheory.RingHom.QuasiFinite

Goal state before:
pp: R S : Type u_6
inst✝¹ : CommRing R
inst✝ : CommRing S
f✝ : R →+* S
s : Finset S
hs : Ideal.span ↑s = ⊤
H : ∀ (r : ↥s), (fun {R S} [CommRing R] [CommRing S] ↦ QuasiFinite) ((algebraMap S (Localization.Away ↑r)).comp f✝)
algInst✝ : Algebra R S := f✝.toAlgebra
P : Ideal R
x✝ : P.IsPrime
this✝ : ∀ (r : ↥s), Module.Finite P.ResidueField (P.Fiber (Localization.Away ↑r))
φ : (r : ↥s) → P.Fiber S →ₐ[P.ResidueField] P.Fiber (Localization.Away ↑r) :=
  fun r ↦
    Algebra.TensorProduct.map (AlgHom.id P.ResidueField P.ResidueField)
      (IsScalarTower.toAlgHom R S (Localization.Away ↑r))
f : P.Fiber S →ₐ[P.ResidueField] (r : ↥s) → P.Fiber (Localization.Away ↑r) := AlgHom.pi φ
this : IsNoetherian P.ResidueField ((r : ↥s) → P.Fiber (Localization.Away ↑r))
⊢ Module.Finite P.ResidueField (P.Fiber S)

Tactic:
suffices Function.Injective f from .of_injective f.toLinearMap this

Goal state after:
R S : Type u_6
inst✝¹ : CommRing R
inst✝ : CommRing S
f✝ : R →+* S
s : Finset S
hs : Ideal.span ↑s = ⊤
H : ∀ (r : ↥s), (fun {R S} [CommRing R] [CommRing S] ↦ QuasiFinite) ((algebraMap S (Localization.Away ↑r)).comp f✝)
algInst✝ : Algebra R S := f✝.toAlgebra
P : Ideal R
x✝ : P.IsPrime
this✝ : ∀ (r : ↥s), Module.Finite P.ResidueField (P.Fiber (Localization.Away ↑r))
φ : (r : ↥s) → P.Fiber S →ₐ[P.ResidueField] P.Fiber (Localization.Away ↑r) :=
  fun r ↦
    Algebra.TensorProduct.map (AlgHom.id P.ResidueField P.ResidueField)
      (IsScalarTower.toAlgHom R S (Localization.Away ↑r))
f : P.Fiber S →ₐ[P.ResidueField] (r : ↥s) → P.Fiber (Localization.Away ↑r) := AlgHom.pi φ
this : IsNoetherian P.ResidueField ((r : ↥s) → P.Fiber (Localization.Away ↑r))
⊢ Function.Injective ⇑f
Module: Mathlib.RingTheory.Algebraic.StronglyTranscendental

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
M : Submonoid R
inst✝¹ : IsLocalization M S
inst✝ : IsScalarTower R S T
x : T
h : IsStronglyTranscendental R x
⊢ IsStronglyTranscendental S x

Tactic:
intro t p hp

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
M : Submonoid R
inst✝¹ : IsLocalization M S
inst✝ : IsScalarTower R S T
x : T
h : IsStronglyTranscendental R x
t : T
p : S[X]
hp : (aeval x) p * t = 0
⊢ map (algebraMap S T) p * C t = 0
Module: Mathlib.RingTheory.Algebraic.StronglyTranscendental

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
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
x : T
h : IsStronglyTranscendental S x
⊢ IsStronglyTranscendental R x

Tactic:
intro t p hp

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
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
x : T
h : IsStronglyTranscendental S x
t : T
p : R[X]
hp : (aeval x) p * t = 0
⊢ map (algebraMap R T) p * C t = 0
Module: Mathlib.RingTheory.Algebraic.StronglyTranscendental

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
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
x : T
h : IsStronglyTranscendental R x
H : Function.Surjective ⇑(algebraMap R S)
⊢ IsStronglyTranscendental S x

Tactic:
intro t p hp

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
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
x : T
h : IsStronglyTranscendental R x
H : Function.Surjective ⇑(algebraMap R S)
t : T
p : S[X]
hp : (aeval x) p * t = 0
⊢ map (algebraMap S T) p * C t = 0
Module: Mathlib.RingTheory.QuasiFinite.Weakly

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
p : Ideal S
inst✝² : p.IsPrime
inst✝¹ : QuasiFinite R (Localization.AtPrime p ⧸ Ideal.map (algebraMap R (Localization.AtPrime p)) (Ideal.under R p))
q : Ideal T
inst✝ : q.IsPrime
f : Localization.AtPrime p →ₐ[R] Localization.AtPrime q
hf : Function.Surjective ⇑f
x : R
hx : x ∈ Ideal.under R p
hx' : x ∉ Ideal.under R q
this : IsLocalHom f.toRingHom
⊢ False

Tactic:
have := this.1 (algebraMap _ _ x) (by
      suffices IsUnit (IsLocalization.mk' (M := q.primeCompl) (Localization.AtPrime q)
        (algebraMap _ _ x) 1) by simpa [IsLocalization.mk'_one] using! this
      simpa [IsLocalization.AtPrime.isUnit_mk'_iff])

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
p : Ideal S
inst✝² : p.IsPrime
inst✝¹ : QuasiFinite R (Localization.AtPrime p ⧸ Ideal.map (algebraMap R (Localization.AtPrime p)) (Ideal.under R p))
q : Ideal T
inst✝ : q.IsPrime
f : Localization.AtPrime p →ₐ[R] Localization.AtPrime q
hf : Function.Surjective ⇑f
x : R
hx : x ∈ Ideal.under R p
hx' : x ∉ Ideal.under R q
this✝ : IsLocalHom f.toRingHom
this : IsUnit ((algebraMap R (Localization.AtPrime p)) x)
⊢ False
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite

Goal state before:
pp: R S : CommRingCat
φ : R ⟶ S
inst✝¹ : IsArtinianRing ↑R
inst✝ : (CommRingCat.Hom.hom φ).QuasiFinite
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom φ).toAlgebra
algebraizeInst✝ : Algebra.QuasiFinite ↑R ↑S
this : Module.Finite ↑R ↑S
⊢ IsArtinianRing ↑S

Tactic:
exact .of_finite R S

Goal state after:
Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski

Goal state before:
pp: case refine_1
X : Scheme
U : X.AffineZariskiSite
P : Presieve U
x✝¹ : X.AffineZariskiSite
V : X.Opens
hV : IsAffineOpen V
x✝ : ⟨V, hV⟩ ⟶ U
f : ↑Γ(X, U.toOpens)
hf : X.basicOpen f = toOpens ⟨V, hV⟩
⊢ U.presieveOfSections (sectionsOfPresieve P) { down := { down := ⋯ } } → P { down := { down := ⋯ } }

Tactic:
rintro ⟨_, H, rfl⟩
    exact H

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

Goal state before:
pp: K : Type u
inst✝⁴ : CommRing K
R : Type u_1
inst✝³ : IsDomain K
inst✝² : Monoid R
inst✝¹ : DistribMulAction R K[X]
inst✝ : IsScalarTower R K[X] K[X]
c : R
p q : K[X]
⊢ RatFunc.mk (c • p) q = c • RatFunc.mk p q

Tactic:
let : SMulZeroClass R (FractionRing K[X]) := inferInstance
  by_cases hq : q = 0
  · rw [hq, mk_zero, mk_zero, ← ofFractionRing_smul, smul_zero]
  · rw [mk_eq_localization_mk _ hq, mk_eq_localization_mk _ hq, ← Localization.smul_mk, ←
      ofFractionRing_smul]

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

Goal state before:
pp: K : Type u
inst✝ : Field K
x : K⟮X⟯
p q : K[X]
hq : q ≠ 0
⊢ (algebraMap K[X] K⟮X⟯) (x.num * q) = (algebraMap K[X] K⟮X⟯) (p * x.denom) ↔
    x = (algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q

Tactic:
eq_div_iff (algebraMap_ne_zero hq)

Goal state after:
K : Type u
inst✝ : Field K
x : K⟮X⟯
p q : K[X]
hq : q ≠ 0
⊢ (algebraMap K[X] K⟮X⟯) (x.num * q) = (algebraMap K[X] K⟮X⟯) (p * x.denom) ↔
    x * (algebraMap K[X] K⟮X⟯) q = (algebraMap K[X] K⟮X⟯) p
Module: Mathlib.RingTheory.Etale.StandardEtale

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
P✝ : StandardEtalePair R
P : StandardEtalePresentation R S
algInst✝ : Algebra R (P.map (algebraMap R T)).Ring :=
  ((algebraMap T (P.map (algebraMap R T)).Ring).comp (algebraMap R T)).toAlgebra
scalarTowerInst✝ : IsScalarTower R T (P.map (algebraMap R T)).Ring :=
  IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R (P.map (algebraMap R T)).Ring))
⊢ Function.Bijective ⇑((P.map (algebraMap R T)).lift (1 ⊗ₜ[R] P.x) ⋯)

Tactic:
have H : P.HasMap (P.map (algebraMap R T)).X := by
      simpa [StandardEtalePair.HasMap] using (P.map (algebraMap R T)).hasMap_X

Goal state after:
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
P✝ : StandardEtalePair R
P : StandardEtalePresentation R S
algInst✝ : Algebra R (P.map (algebraMap R T)).Ring :=
  ((algebraMap T (P.map (algebraMap R T)).Ring).comp (algebraMap R T)).toAlgebra
scalarTowerInst✝ : IsScalarTower R T (P.map (algebraMap R T)).Ring :=
  IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R (P.map (algebraMap R T)).Ring))
H : P.HasMap (P.map (algebraMap R T)).X
⊢ Function.Bijective ⇑((P.map (algebraMap R T)).lift (1 ⊗ₜ[R] P.x) ⋯)
Module: Mathlib.RingTheory.Smooth.IntegralClosure

Goal state before:
pp: R : Type u_1
B : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing B
inst✝ : Algebra R B
σ : Type u_4
x : MvPolynomial σ R ⊗[R] B
hx : x ∈ integralClosure (MvPolynomial σ R) (MvPolynomial σ R ⊗[R] B)
e₀ : MvPolynomial σ R ⊗[R] B ≃ₐ[R] MvPolynomial σ B :=
  (Algebra.TensorProduct.comm R (MvPolynomial σ R) B).trans
    (AlgEquiv.restrictScalars R (MvPolynomial.algebraTensorAlgEquiv R B))
e₁ : MvPolynomial σ R ⊗[R] ↥(integralClosure R B) ≃ₐ[R] MvPolynomial σ ↥(integralClosure R B) :=
  (Algebra.TensorProduct.comm R (MvPolynomial σ R) ↥(integralClosure R B)).trans
    (AlgEquiv.restrictScalars R (MvPolynomial.algebraTensorAlgEquiv R ↥(integralClosure R B)))
e : MvPolynomial σ R ⊗[R] B ≃ₐ[MvPolynomial σ R] MvPolynomial σ B :=
  let __RingEquiv := e₀.toRingEquiv;
  { toEquiv := __RingEquiv.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
this : ∀ (n : σ →₀ ℕ), IsIntegral R (MvPolynomial.coeff n (e x))
y : MvPolynomial σ R ⊗[R] ↥(integralClosure R B)
hy : (MvPolynomial.map (integralClosure R B).val.toRingHom) (e₁ y) = e x
⊢ e₀
      ((Algebra.TensorProduct.map (AlgHom.id (MvPolynomial σ R) (MvPolynomial σ R)) (integralClosure R B).val)
        (e₁.symm (e₁ y))) =
    (MvPolynomial.map ↑(integralClosure R B).val) (e₁ y)

Tactic:
simp only [AlgEquiv.symm_apply_apply]

Goal state after:
R : Type u_1
B : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing B
inst✝ : Algebra R B
σ : Type u_4
x : MvPolynomial σ R ⊗[R] B
hx : x ∈ integralClosure (MvPolynomial σ R) (MvPolynomial σ R ⊗[R] B)
e₀ : MvPolynomial σ R ⊗[R] B ≃ₐ[R] MvPolynomial σ B :=
  (Algebra.TensorProduct.comm R (MvPolynomial σ R) B).trans
    (AlgEquiv.restrictScalars R (MvPolynomial.algebraTensorAlgEquiv R B))
e₁ : MvPolynomial σ R ⊗[R] ↥(integralClosure R B) ≃ₐ[R] MvPolynomial σ ↥(integralClosure R B) :=
  (Algebra.TensorProduct.comm R (MvPolynomial σ R) ↥(integralClosure R B)).trans
    (AlgEquiv.restrictScalars R (MvPolynomial.algebraTensorAlgEquiv R ↥(integralClosure R B)))
e : MvPolynomial σ R ⊗[R] B ≃ₐ[MvPolynomial σ R] MvPolynomial σ B :=
  let __RingEquiv := e₀.toRingEquiv;
  { toEquiv := __RingEquiv.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
this : ∀ (n : σ →₀ ℕ), IsIntegral R (MvPolynomial.coeff n (e x))
y : MvPolynomial σ R ⊗[R] ↥(integralClosure R B)
hy : (MvPolynomial.map (integralClosure R B).val.toRingHom) (e₁ y) = e x
⊢ e₀ ((Algebra.TensorProduct.map (AlgHom.id (MvPolynomial σ R) (MvPolynomial σ R)) (integralClosure R B).val) y) =
    (MvPolynomial.map ↑(integralClosure R B).val) (e₁ y)
Module: Mathlib.RingTheory.Smooth.IntegralClosure

Goal state before:
pp: R : Type u_1
S : Type u_2
B : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : CommRing B
inst✝¹ : Algebra R B
M : Submonoid R
inst✝ : IsLocalization M S
⊢ Function.Bijective ⇑(toIntegralClosure R S B)

Tactic:
let φ : integralClosure R B →ₐ[R] integralClosure S (S ⊗[R] B) :=
    AlgHom.codRestrict (Algebra.TensorProduct.includeRight.comp (integralClosure R B).val)
      ((integralClosure S (S ⊗[R] B)).restrictScalars R) fun ⟨x, hx⟩ ↦ by
    refine .of_comp (f := algebraMap R S) ?_
    convert!
      RingHom.IsIntegralElem.map hx
        (Algebra.TensorProduct.includeRight : B →ₐ[R] S ⊗[R] B).toRingHom
    simp [← IsScalarTower.algebraMap_eq]

Goal state after:
R : Type u_1
S : Type u_2
B : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : CommRing B
inst✝¹ : Algebra R B
M : Submonoid R
inst✝ : IsLocalization M S
φ : ↥(integralClosure R B) →ₐ[R] ↥(integralClosure S (S ⊗[R] B)) :=
  (Algebra.TensorProduct.includeRight.comp (integralClosure R B).val).codRestrict
    (Subalgebra.restrictScalars R (integralClosure S (S ⊗[R] B))) ⋯
⊢ Function.Bijective ⇑(toIntegralClosure R S B)