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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : PrimeSpectrum A
h₁ : LocalizedModule p.asIdeal.primeCompl Ω[A⁄R] ≃ₗ[A] Ω[Localization.AtPrime p.asIdeal⁄R]
h₂ : LocalizedModule p.asIdeal.primeCompl (H1Cotangent R A) ≃ₗ[A] H1Cotangent R (Localization.AtPrime p.asIdeal)
⊢ p ∈ etaleLocus R A ↔
    Subsingleton (LocalizedModule p.asIdeal.primeCompl Ω[A⁄R]) ∧
      Subsingleton (LocalizedModule p.asIdeal.primeCompl (H1Cotangent R A))

Tactic:
exact (Algebra.formallyEtale_iff _ _).trans
    (and_congr h₁.subsingleton_congr.symm h₂.subsingleton_congr.symm)

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

Goal state before:
pp: case tmul.smul
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
x : B
s✝ : S
n✝ : B
a✝ : x • (LinearMap.liftBaseChange S (↑R (map R S A B))) ((derivationTensorProduct R S A B) n✝) = x • (D S B) n✝
⊢ x • (LinearMap.liftBaseChange S (↑R (map R S A B))) ((derivationTensorProduct R S A B) (s✝ • n✝)) =
    x • (D S B) (s✝ • n✝)

pp: case tmul.add
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
x n₁✝ n₂✝ : B
a✝¹ : x • (LinearMap.liftBaseChange S (↑R (map R S A B))) ((derivationTensorProduct R S A B) n₁✝) = x • (D S B) n₁✝
a✝ : x • (LinearMap.liftBaseChange S (↑R (map R S A B))) ((derivationTensorProduct R S A B) n₂✝) = x • (D S B) n₂✝
⊢ x • (LinearMap.liftBaseChange S (↑R (map R S A B))) ((derivationTensorProduct R S A B) (n₁✝ + n₂✝)) =
    x • (D S B) (n₁✝ + n₂✝)

Tactic:
· -- We use the specialized version of `map_smul` here for performance.
        simp only [Derivation.map_smul, LinearMap.map_smul, *, smul_comm x]

Goal state after:
case tmul.add
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
x n₁✝ n₂✝ : B
a✝¹ : x • (LinearMap.liftBaseChange S (↑R (map R S A B))) ((derivationTensorProduct R S A B) n₁✝) = x • (D S B) n₁✝
a✝ : x • (LinearMap.liftBaseChange S (↑R (map R S A B))) ((derivationTensorProduct R S A B) n₂✝) = x • (D S B) n₂✝
⊢ x • (LinearMap.liftBaseChange S (↑R (map R S A B))) ((derivationTensorProduct R S A B) (n₁✝ + n₂✝)) =
    x • (D S B) (n₁✝ + n₂✝)
Module: Mathlib.RingTheory.AdicCompletion.AsTensorProduct

Goal state before:
pp: R : Type u
inst✝⁷ : CommRing R
I : Ideal R
inst✝⁶ : IsNoetherianRing R
M : Type u
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₗ[R] N
inst✝¹ : Module.Finite R M
inst✝ : Module.Finite R N
⊢ AlgebraTensorModule.map LinearMap.id f =
    ↑(ofTensorProductEquivOfFiniteNoetherian I N).symm ∘ₗ map I f ∘ₗ ofTensorProduct I M

Tactic:
ofTensorProduct_naturality I f

Goal state after:
R : Type u
inst✝⁷ : CommRing R
I : Ideal R
inst✝⁶ : IsNoetherianRing R
M : Type u
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₗ[R] N
inst✝¹ : Module.Finite R M
inst✝ : Module.Finite R N
⊢ AlgebraTensorModule.map LinearMap.id f =
    ↑(ofTensorProductEquivOfFiniteNoetherian I N).symm ∘ₗ ofTensorProduct I N ∘ₗ AlgebraTensorModule.map LinearMap.id f
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 : MvPolynomial ι R₀
⊢ (P.tensorModelOfHasCoeffsInv R₀)
      (P.quotientEquiv ((Ideal.Quotient.mk P.ker) ((MvPolynomial.map (algebraMap R₀ R)) x))) =
    1 ⊗ₜ[R₀] (Ideal.Quotient.mk (Ideal.span (Set.range (relationOfHasCoeffs R₀)))) x

Tactic:
simp [tensorModelOfHasCoeffsInv, -quotientEquiv_symm, -quotientEquiv_mk]

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

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
inst✝ : Finite σ
P : SubmersivePresentation R S ι σ
⊢ IsCompl (Set.range Subtype.val) (Set.range P.map)

Tactic:
rw [Subtype.range_coe_subtype]

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
inst✝ : Finite σ
P : SubmersivePresentation R S ι σ
⊢ IsCompl {x | x ∈ (Set.range P.map)ᶜ} (Set.range P.map)
Module: Mathlib.RingTheory.Smooth.StandardSmoothOfFree

Goal state before:
pp: case inr
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : FinitePresentation R S
p : Ideal S
inst✝¹ : p.IsPrime
inst✝ : IsSmoothAt R p
this✝ :
  ∀ (R : Type u_1) {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
    [FinitePresentation R S] (p : Ideal S) [inst_4 : p.IsPrime] [IsSmoothAt R p],
    Smooth R S → ∃ f ∉ p, IsStandardSmooth R (Localization.Away f)
h : ¬Smooth R S
g : S
hg : g ∉ p
hsm : Smooth R (Localization.Away g)
x✝ : (Ideal.map (algebraMap S (Localization.Away g)) p).IsPrime
g' : Localization.Away g
hg' : g' ∉ Ideal.map (algebraMap S (Localization.Away g)) p
hstd : IsStandardSmooth R (Localization.Away g')
this : IsLocalization.Away (g * (IsLocalization.Away.sec g g').1) (Localization.Away g')
e : Localization.Away (g * (IsLocalization.Away.sec g g').1) ≃ₐ[S] Localization.Away g' :=
  Localization.algEquiv (Submonoid.powers (g * (IsLocalization.Away.sec g g').1)) (Localization.Away g')
hmem : (IsLocalization.Away.sec g g').1 ∈ p
⊢ g' ∈ Ideal.map (algebraMap S (Localization.Away g)) p

Tactic:
rw [Ideal.mem_iff_of_associated (IsLocalization.Away.associated_sec_fst g g').symm]

Goal state after:
case inr
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : FinitePresentation R S
p : Ideal S
inst✝¹ : p.IsPrime
inst✝ : IsSmoothAt R p
this✝ :
  ∀ (R : Type u_1) {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
    [FinitePresentation R S] (p : Ideal S) [inst_4 : p.IsPrime] [IsSmoothAt R p],
    Smooth R S → ∃ f ∉ p, IsStandardSmooth R (Localization.Away f)
h : ¬Smooth R S
g : S
hg : g ∉ p
hsm : Smooth R (Localization.Away g)
x✝ : (Ideal.map (algebraMap S (Localization.Away g)) p).IsPrime
g' : Localization.Away g
hg' : g' ∉ Ideal.map (algebraMap S (Localization.Away g)) p
hstd : IsStandardSmooth R (Localization.Away g')
this : IsLocalization.Away (g * (IsLocalization.Away.sec g g').1) (Localization.Away g')
e : Localization.Away (g * (IsLocalization.Away.sec g g').1) ≃ₐ[S] Localization.Away g' :=
  Localization.algEquiv (Submonoid.powers (g * (IsLocalization.Away.sec g g').1)) (Localization.Away g')
hmem : (IsLocalization.Away.sec g g').1 ∈ p
⊢ (algebraMap S (Localization.Away g)) (IsLocalization.Away.sec g g').1 ∈
    Ideal.map (algebraMap S (Localization.Away g)) 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 ι
x : ((localizationAway T g).comp P).toExtension.Cotangent
⊢ (cotangentCompAwaySec g P x) (cMulXSubOneCotangent T g) = x

Tactic:
← basisCotangentAway_apply _ (),

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 ι
x : ((localizationAway T g).comp P).toExtension.Cotangent
⊢ (cotangentCompAwaySec g P x) ((basisCotangentAway T g) ()) = x
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
x : ↥D.presLeft.toExtension.ker
⊢ Extension.Cotangent.mk ⟨D.fhom.toExtensionHom.toAlgHom ↑x, ⋯⟩ = Extension.Cotangent.mk ⟨↑x, ⋯⟩

Tactic:
Extension.Hom.toAlgHom_apply,

Goal state after:
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
x : ↥D.presLeft.toExtension.ker
⊢ Extension.Cotangent.mk ⟨D.fhom.toExtensionHom.toRingHom ↑x, ⋯⟩ = Extension.Cotangent.mk ⟨↑x, ⋯⟩
Module: Mathlib.FieldTheory.SeparablyGenerated

Goal state before:
pp: case refine_1
k : Type u_1
K : Type u_2
ι : Type u_3
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
a : ι → K
F : MvPolynomial ι k
HF : ∀ (F' : MvPolynomial ι k), F' ≠ 0 → (aeval a) F' = 0 → F.totalDegree ≤ F'.totalDegree
σ : ι →₀ ℕ
hσ : σ ∈ F.support
i : ι
hσi : σ i ≠ 0
H✝ : (F.toPolynomialAdjoinImageCompl a i).coeff (σ i) = 0
F₀ : Polynomial (MvPolynomial { b // b ≠ i } k) :=
  (optionEquivLeft k { b // b ≠ i }) ((renameEquiv k (Equiv.optionSubtypeNe i).symm) F)
H : F₀.coeff (σ i) = 0
e : ι ≃ Option { b // b ≠ i } := (Equiv.optionSubtypeNe i).symm
this :
  coeff (Finsupp.mapDomain (⇑e) σ).some
      (((optionEquivLeft k { b // b ≠ i }) ((rename ⇑(Equiv.optionSubtypeNe i).symm) F)).coeff (σ (e.symm none))) =
    coeff σ F
⊢ False

Tactic:
Equiv.symm_symm,

Goal state after:
case refine_1
k : Type u_1
K : Type u_2
ι : Type u_3
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
a : ι → K
F : MvPolynomial ι k
HF : ∀ (F' : MvPolynomial ι k), F' ≠ 0 → (aeval a) F' = 0 → F.totalDegree ≤ F'.totalDegree
σ : ι →₀ ℕ
hσ : σ ∈ F.support
i : ι
hσi : σ i ≠ 0
H✝ : (F.toPolynomialAdjoinImageCompl a i).coeff (σ i) = 0
F₀ : Polynomial (MvPolynomial { b // b ≠ i } k) :=
  (optionEquivLeft k { b // b ≠ i }) ((renameEquiv k (Equiv.optionSubtypeNe i).symm) F)
H : F₀.coeff (σ i) = 0
e : ι ≃ Option { b // b ≠ i } := (Equiv.optionSubtypeNe i).symm
this :
  coeff (Finsupp.mapDomain (⇑e) σ).some
      (((optionEquivLeft k { b // b ≠ i }) ((rename ⇑(Equiv.optionSubtypeNe i).symm) F)).coeff
        (σ ((Equiv.optionSubtypeNe i) none))) =
    coeff σ F
⊢ False
Module: Mathlib.AlgebraicGeometry.Morphisms.Etale

Goal state before:
pp: R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
x✝⁴ : Type ?u.17
x✝³ : Type ?u.16
x✝² : CommRing x✝⁴
x✝¹ : CommRing x✝³
x✝ : x✝⁴ →+* x✝³
⊢ x✝.Etale ↔ RingHom.IsStandardSmoothOfRelativeDimension 0 x✝

Tactic:
apply RingHom.etale_iff_isStandardSmoothOfRelativeDimension_zero

Goal state after:
Module: Mathlib.RingTheory.Conductor

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
I : Ideal R
p : R
z : S
hp : p ∈ comap (algebraMap R S) (conductor R x)
l : R →₀ S
H : l ∈ Finsupp.supported S S ↑I
H' : (l.sum fun i a ↦ a • (algebraMap R S) i) = z
a : R
ha : a ∈ I
⊢ l a * (algebraMap R S) p ∈ R[x]

Tactic:
rw [mul_comm]
      exact mem_conductor_iff.mp (Ideal.mem_comap.mp hp) _

Goal state after:
Module: Mathlib.RingTheory.Conductor

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
I : Ideal R
p : R
z : S
hp : p ∈ comap (algebraMap R S) (conductor R x)
hz' : z ∈ Ideal.map (algebraMap R S) I
⊢ (algebraMap R S) p * z ∈ ⇑(algebraMap (↥R[x]) S) '' ↑(Ideal.map (algebraMap R ↥R[x]) I)

Tactic:
by
  rw [Ideal.map, Ideal.span, Finsupp.mem_span_image_iff_linearCombination] at hz'
  obtain ⟨l, H, H'⟩ := hz'
  rw [Finsupp.linearCombination_apply] at H'
  rw [← H', mul_comm, Finsupp.sum_mul]
  have lem : ∀ {a : R}, a ∈ I → l a • algebraMap R S a * algebraMap R S p ∈
      algebraMap R<x> S '' I.map (algebraMap R R<x>) := by
    intro a ha
    rw [smul_eq_mul, mul_assoc, mul_comm, mul_assoc, Set.mem_image]
    refine Exists.intro
        (algebraMap R R<x> a * ⟨l a * algebraMap R S p,
          show l a * algebraMap R S p ∈ R<x> from ?h⟩) ?_
    case h =>
      rw [mul_comm]
      exact mem_conductor_iff.mp (Ideal.mem_comap.mp hp) _
    · refine ⟨?_, ?_⟩
      · rw [mul_comm]
        apply Ideal.mul_mem_left (I.map (algebraMap R R<x>)) _ (Ideal.mem_map_of_mem _ ha)
      · simp only [map_mul, mul_comm (algebraMap R S p) (l a)]
        rfl
  refine Finset.sum_induction _ (fun u => u ∈ algebraMap R<x> S '' I.map (algebraMap R R<x>))
      (fun a b => ?_) ?_ ?_
  · rintro ⟨z, hz, rfl⟩ ⟨y, hy, rfl⟩
    rw [← map_add]
    exact ⟨z + y, Ideal.add_mem _ (SetLike.mem_coe.mp hz) hy, rfl⟩
  · exact ⟨0, SetLike.mem_coe.mpr <| Ideal.zero_mem _, map_zero _⟩
  · intro y hy
    exact lem ((Finsupp.mem_supported _ l).mp H hy)

Goal state after:
Module: Mathlib.RingTheory.Conductor

Goal state before:
pp: case a
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
I : Ideal R
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
h_alg : Function.Injective ⇑(algebraMap (↥R[x]) S)
⊢ Ideal.map (algebraMap R ↥R[x]) I ≤
    comap (algebraMap (↥R[x]) S) (Ideal.map ((algebraMap (↥R[x]) S).comp (algebraMap R ↥R[x])) I)

Tactic:
← Ideal.map_map

Goal state after:
case a
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
I : Ideal R
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
h_alg : Function.Injective ⇑(algebraMap (↥R[x]) S)
⊢ Ideal.map (algebraMap R ↥R[x]) I ≤
    comap (algebraMap (↥R[x]) S) (Ideal.map (algebraMap (↥R[x]) S) (Ideal.map (algebraMap R ↥R[x]) I))
Module: Mathlib.RingTheory.Conductor

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
I : Ideal R
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
h_alg : Function.Injective ⇑(algebraMap (↥R[x]) S)
r : ↥R[x]
hr : r ∈ Ideal.map (algebraMap R ↥R[x]) I
this : algebraMap R S = (algebraMap (↥R[x]) S).comp (algebraMap R ↥R[x])
⊢ (algebraMap (↥R[x]) S) r ∈ Ideal.map ((algebraMap (↥R[x]) S).comp (algebraMap R ↥R[x])) I

Tactic:
← Ideal.map_map

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
I : Ideal R
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
h_alg : Function.Injective ⇑(algebraMap (↥R[x]) S)
r : ↥R[x]
hr : r ∈ Ideal.map (algebraMap R ↥R[x]) I
this : algebraMap R S = (algebraMap (↥R[x]) S).comp (algebraMap R ↥R[x])
⊢ (algebraMap (↥R[x]) S) r ∈ Ideal.map (algebraMap (↥R[x]) S) (Ideal.map (algebraMap R ↥R[x]) I)
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝⁶ : CommRing K
G₀ : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
F : Type u_5
inst✝⁵ : CommGroupWithZero G₀
inst✝⁴ : Field L
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : FunLike F R[X] S[X]
inst✝ : RingHomClass F R[X] S[X]
φ : F
hφ : R[X]⁰ ≤ Submonoid.comap φ S[X]⁰
⊢ (map φ hφ) 0 = 0

Tactic:
← ofFractionRing_zero,

Goal state after:
K : Type u
inst✝⁶ : CommRing K
G₀ : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
F : Type u_5
inst✝⁵ : CommGroupWithZero G₀
inst✝⁴ : Field L
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : FunLike F R[X] S[X]
inst✝ : RingHomClass F R[X] S[X]
φ : F
hφ : R[X]⁰ ≤ Submonoid.comap φ S[X]⁰
⊢ (map φ hφ) { toFractionRing := 0 } = { toFractionRing := 0 }
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:
by
  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
G₀ : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
F : Type u_5
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : Field L
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : FunLike F R[X] S[X]
φ : R[X] →*₀ G₀
hφ : R[X]⁰ ≤ Submonoid.comap φ G₀⁰
⊢ RatFunc.liftOn 0 (fun p q ↦ φ p / φ q) ⋯ = 0

Tactic:
← ofFractionRing_zero,

Goal state after:
K : Type u
inst✝⁵ : CommRing K
G₀ : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
F : Type u_5
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : Field L
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : FunLike F R[X] S[X]
φ : R[X] →*₀ G₀
hφ : R[X]⁰ ≤ Submonoid.comap φ G₀⁰
⊢ { toFractionRing := 0 }.liftOn (fun p q ↦ φ p / φ q) ⋯ = 0
Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski

Goal state before:
pp: X : Scheme
D : Cover.RelativeGluingData (directedCover X) := relativeGluingData ⋯
F : (directedCover X).I₀ ⥤ Scheme := D.functor
this : (D.functor ⋙ forget).IsLocallyDirected
U : (X.openCoverOfIsOpenCover (fun i ↦ ↑i) ⋯).toPreZeroHypercover.1
e : pullback (colimit.desc F (cocone X)) (↑U).ι ≅ ↑↑U :=
  IsOpenImmersion.isoOfRangeEq (pullback.fst (colimit.desc F (cocone X)) (↑U).ι)
    ((IsAffineOpen.isoSpec ⋯).hom ≫ colimit.ι F U) ⋯
⊢ IsIso (pullback.snd (colimit.desc F (cocone X)) (↑U).ι)

Tactic:
convert! (inferInstance : IsIso e.hom)

Goal state after:
X : Scheme
D : Cover.RelativeGluingData (directedCover X) := relativeGluingData ⋯
F : (directedCover X).I₀ ⥤ Scheme := D.functor
this : (D.functor ⋙ forget).IsLocallyDirected
U : (X.openCoverOfIsOpenCover (fun i ↦ ↑i) ⋯).toPreZeroHypercover.1
e : pullback (colimit.desc F (cocone X)) (↑U).ι ≅ ↑↑U :=
  IsOpenImmersion.isoOfRangeEq (pullback.fst (colimit.desc F (cocone X)) (↑U).ι)
    ((IsAffineOpen.isoSpec ⋯).hom ≫ colimit.ι F U) ⋯
⊢ pullback.snd (colimit.desc F (cocone X)) (↑U).ι = e.hom
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝ : Field K
x : K⟮X⟯
⊢ x.denom.Monic

Tactic:
by
  classical
  induction x using RatFunc.induction_on with
  | f p q hq =>
    rw [denom_div p hq, mul_comm]
    exact Polynomial.monic_mul_leadingCoeff_inv (right_div_gcd_ne_zero hq)

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

Goal state before:
pp: case mpr
K : Type u
inst✝ : Field K
x : K⟮X⟯
p : K[X]
hp : p ≠ 0
⊢ (∃ q, q ≠ 0 ∧ x = (algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q) → x.num ∣ p

Tactic:
· rintro ⟨q, hq, rfl⟩
    exact num_div_dvd p hq

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

Goal state before:
pp: case refine_3
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
⊢ Ideal.span {(algebraMap R[X] (Localization.Away P.g)) P.f} ≤ RingHom.ker (IsLocalization.Away.liftAlgHom P.g ⋯)

Tactic:
simpa [Ideal.span_le] using P.hasMap_X.1

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

Goal state before:
pp: case inr
R : Type u_1
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Module.Finite R S
Q : Ideal S
inst✝¹ : Q.IsPrime
inst✝ : IsUnramifiedAt R Q
h✝ : Nontrivial S
this✝ : Nontrivial R
P : Ideal R := Ideal.under R Q
this : Algebra (Localization.AtPrime P) (Localization.AtPrime Q) := Localization.AtPrime.algebraOfLiesOver P Q
x : S
hx : R[x] = ⊤
hRx : IsIntegral R x
I : Ideal R[X] := RingHom.ker (aeval x).toRingHom
hx' : Function.Surjective ⇑(aeval x)
p : R[X]
hpI : p ∈ I
hp :
  Ideal.span {Polynomial.map (algebraMap R P.ResidueField) p} = Ideal.map (mapRingHom (algebraMap R P.ResidueField)) I
hI' : Ideal.map (mapRingHom (algebraMap R P.ResidueField)) I = RingHom.ker (aeval (1 ⊗ₜ[R] x)).toRingHom
m : P.ResidueField[X] := minpoly P.ResidueField ((algebraMap S Q.ResidueField) x)
hm : Prime m
hmp₁ : m ∣ Polynomial.map (algebraMap R P.ResidueField) p
hmp₂ : ¬m ^ 2 ∣ Polynomial.map (algebraMap R P.ResidueField) p
⊢ ∃ q, q.Monic ∧ (aeval x) q = 0 ∧ (aeval x) (derivative q) ∉ Q

Tactic:
let q := minpoly R x ^ (p.natDegree + 2) + p

Goal state after:
case inr
R : Type u_1
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Module.Finite R S
Q : Ideal S
inst✝¹ : Q.IsPrime
inst✝ : IsUnramifiedAt R Q
h✝ : Nontrivial S
this✝ : Nontrivial R
P : Ideal R := Ideal.under R Q
this : Algebra (Localization.AtPrime P) (Localization.AtPrime Q) := Localization.AtPrime.algebraOfLiesOver P Q
x : S
hx : R[x] = ⊤
hRx : IsIntegral R x
I : Ideal R[X] := RingHom.ker (aeval x).toRingHom
hx' : Function.Surjective ⇑(aeval x)
p : R[X]
hpI : p ∈ I
hp :
  Ideal.span {Polynomial.map (algebraMap R P.ResidueField) p} = Ideal.map (mapRingHom (algebraMap R P.ResidueField)) I
hI' : Ideal.map (mapRingHom (algebraMap R P.ResidueField)) I = RingHom.ker (aeval (1 ⊗ₜ[R] x)).toRingHom
m : P.ResidueField[X] := minpoly P.ResidueField ((algebraMap S Q.ResidueField) x)
hm : Prime m
hmp₁ : m ∣ Polynomial.map (algebraMap R P.ResidueField) p
hmp₂ : ¬m ^ 2 ∣ Polynomial.map (algebraMap R P.ResidueField) p
q : R[X] := minpoly R x ^ (p.natDegree + 2) + p
⊢ ∃ q, q.Monic ∧ (aeval x) q = 0 ∧ (aeval x) (derivative q) ∉ Q
Module: Mathlib.RingTheory.Unramified.LocalStructure

Goal state before:
pp: R : Type u_1
S : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
Q : Ideal S
inst✝⁴ : Q.IsPrime
inst✝³ : Module.Finite R S
inst✝² : IsUnramifiedAt R Q
inst✝¹ : Algebra (Localization.AtPrime (Ideal.under R Q)) (Localization.AtPrime Q)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra (Ideal.under R Q) Q
p : Ideal R := Ideal.under R Q
this✝ : p.IsPrime
this : Module p.ResidueField (p.Fiber S) := leftModule
⊢ ∃ t ∉ Q,
    (∀ Q' ∈ (Ideal.under R Q).primesOver S, Q' ≠ Q → t ∈ Q') ∧
      (Ideal.under R Q).ResidueField[(algebraMap S Q.ResidueField) t] = ⊤

Tactic:
let : SMul p.ResidueField (p.Fiber S) := this.toSMul

Goal state after:
R : Type u_1
S : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
Q : Ideal S
inst✝⁴ : Q.IsPrime
inst✝³ : Module.Finite R S
inst✝² : IsUnramifiedAt R Q
inst✝¹ : Algebra (Localization.AtPrime (Ideal.under R Q)) (Localization.AtPrime Q)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra (Ideal.under R Q) Q
p : Ideal R := Ideal.under R Q
this✝¹ : p.IsPrime
this✝ : Module p.ResidueField (p.Fiber S) := leftModule
this : SMul p.ResidueField (p.Fiber S) := this✝.toSMul
⊢ ∃ t ∉ Q,
    (∀ Q' ∈ (Ideal.under R Q).primesOver S, Q' ≠ Q → t ∈ Q') ∧
      (Ideal.under R Q).ResidueField[(algebraMap S Q.ResidueField) t] = ⊤