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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ IsZariskiLocalAtSource @IsLocalIso

Tactic:
rw [eq_sourceLocalClosure_isOpenImmersion]

Goal state after:
X Y : Scheme
f : X ⟶ Y
⊢ IsZariskiLocalAtSource (sourceLocalClosure IsOpenImmersion IsOpenImmersion)
Module: Mathlib.AlgebraicGeometry.Morphisms.LocalIso

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ IsMultiplicative @IsLocalIso

Tactic:
rw [eq_sourceLocalClosure_isOpenImmersion]

Goal state after:
X Y : Scheme
f : X ⟶ Y
⊢ (sourceLocalClosure IsOpenImmersion IsOpenImmersion).IsMultiplicative
Module: Mathlib.AlgebraicGeometry.Morphisms.LocalIso

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ IsStableUnderBaseChange @IsLocalIso

Tactic:
rw [eq_sourceLocalClosure_isOpenImmersion]

Goal state after:
X Y : Scheme
f : X ⟶ Y
⊢ (sourceLocalClosure IsOpenImmersion IsOpenImmersion).IsStableUnderBaseChange
Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified

Goal state before:
pp: case e'_5
X Y : Scheme
f : X ⟶ Y
inst✝¹ : FormallyUnramified f
inst✝ : LocallyOfFiniteType f
x✝ : ↥X
algInst✝ : Algebra ↑(Y.presheaf.stalk (f x✝)) ↑(X.presheaf.stalk x✝) :=
  (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x✝)).toAlgebra
this : IsLocalHom (algebraMap ↑(Y.presheaf.stalk (f x✝)) ↑(X.presheaf.stalk x✝))
h :
  Algebra.IsSeparable (IsLocalRing.ResidueField ↑(Y.presheaf.stalk (f x✝)))
    (IsLocalRing.ResidueField ↑(X.presheaf.stalk x✝))
e_1✝ : ↑(Y.residueField (f x✝)) = IsLocalRing.ResidueField ↑(Y.presheaf.stalk (f x✝))
e_2✝ : ↑(X.residueField x✝) = IsLocalRing.ResidueField ↑(X.presheaf.stalk x✝)
e_3✝ : CommRingCat.instCommRingObjForgetRingHomCarrier ≍ IsLocalRing.instCommRingResidueField ↑(Y.presheaf.stalk (f x✝))
e_4✝ :
  (X.instFieldCarrierResidueField x✝).toDivisionRing.toRing ≍
    (IsLocalRing.ResidueField.field ↑(X.presheaf.stalk x✝)).toDivisionRing.toRing
x : ↑(Y.presheaf.stalk (f x✝))
⊢ (algebraMap ↑(Y.residueField (f x✝)) ↑(X.residueField x✝)) ((IsLocalRing.residue ↑(Y.presheaf.stalk (f x✝))) x) =
    (algebraMap ↑(Y.residueField (f x✝)) ↑(X.residueField x✝)) ((IsLocalRing.residue ↑(Y.presheaf.stalk (f x✝))) x)

Tactic:
rfl

Goal state after:
Module: Mathlib.FieldTheory.SeparablyGenerated

Goal state before:
pp: k : Type u_1
K : Type u_2
ι : Type u_3
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
p : ℕ
hp : Nat.Prime p
H : ∀ (s : Finset K), LinearIndepOn k id ↑s → LinearIndepOn k (fun x ↦ x ^ p) ↑s
a : ι → K
n : ι
inst✝ : ExpChar k p
ha' : IsTranscendenceBasis k fun i ↦ a ↑i
S : Set (MvPolynomial ι k) := {F | F ≠ 0 ∧ (aeval a) F = 0}
F : MvPolynomial ι k
hFmin : ∀ (G : MvPolynomial ι k), G ≠ 0 → (aeval a) G = 0 → F.totalDegree ≤ G.totalDegree
hF₀ : F ≠ 0
hFa : (aeval a) F = 0
hFirr : Irreducible F
i : ι
σ : ι →₀ ℕ
hσ : σ ∈ F.support
hi : ¬p ∣ σ i
hσi : σ i ≠ 0
alg : IsAlgebraic (↥(Algebra.adjoin k (a '' {i}ᶜ))) (a i)
Hi : IsTranscendenceBasis k fun x ↦ a ↑x
k' : IntermediateField k K := adjoin k (a '' {i}ᶜ)
hF₁irr : Irreducible (F.toPolynomialAdjoinImageCompl a i)
this✝ : UniqueFactorizationMonoid ↥(Algebra.adjoin k (a '' {i}ᶜ))
hF₂irr :
  Irreducible (Polynomial.map (algebraMap ↥(Algebra.adjoin k (a '' {i}ᶜ)) ↥k') (F.toPolynomialAdjoinImageCompl a i))
Hsep : ¬IsSeparable (↥(adjoin k (a '' {i}ᶜ))) (a i)
this : CharP (↥k') p
g : Polynomial ↥k'
hg : Irreducible g
eq :
  0 =
    (Polynomial.map (algebraMap ↥(Algebra.adjoin k (a '' {i}ᶜ)) ↥k') (F.toPolynomialAdjoinImageCompl a i)).coeff (σ i) *
      (Polynomial.map (algebraMap ↥(Algebra.adjoin k (a '' {i}ᶜ)) ↥k')
            (F.toPolynomialAdjoinImageCompl a i)).leadingCoeff⁻¹
⊢ (Polynomial.map (algebraMap ↥(Algebra.adjoin k (a '' {i}ᶜ)) ↥k') (F.toPolynomialAdjoinImageCompl a i)).leadingCoeff ≠
    0

Tactic:
by simpa using hF₂irr.ne_zero

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

Goal state before:
pp: X Y Z' Z : Scheme
i : Z' ⟶ Z
hi : IsNilpotent (Scheme.Hom.ker i)
inst✝¹ : IsClosedImmersion i
f : X ⟶ Y
inst✝ : FormallyUnramified f
g₁ g₂ : Z ⟶ X
hig : i ≫ g₁ = i ≫ g₂
hgf : g₁ ≫ f = g₂ ≫ f
this✝¹ : IsDominant i
x : ↥Z
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : f (g₁ x) ∈ ↑U
V : Opens ↥X
hV : V ∈ X.affineOpens
hxV : g₁ x ∈ ↑V
hVU : V ≤ f ⁻¹ᵁ U
this✝ : g₁.base = g₂.base
W : Opens ↥Z
hW : W ∈ Z.affineOpens
hxW : x ∈ ↑W
hWV : W ≤ g₁ ⁻¹ᵁ V ⊓ g₂ ⁻¹ᵁ V
this : (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).FormallyUnramified
⊢ g₁ ⁻¹ᵁ f ⁻¹ᵁ U ≤ (g₁ ≫ f) ⁻¹ᵁ U

Tactic:
rfl

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

Goal state before:
pp: R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W' : Projective R
f : R →+* S
P Q : Fin 3 → R
⊢ (W'.map f).addZ (⇑f ∘ P) (⇑f ∘ Q) = f (W'.addZ P Q)

Tactic:
simp only [addZ]
  map_simp

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

Goal state before:
pp: ⊢ @Surjective ⊓ (@Surjective ⊓ @Flat ⊓ @QuasiCompact) = @Surjective ⊓ @Flat ⊓ @QuasiCompact

Tactic:
grind

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 y : S
hy : y ∈ ↑(conductor R x)
⊢ y ∈ ↑R[x]

Tactic:
by
  simpa only [mul_one] using! hy 1

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
L : Type u_3
inst✝⁴ : CommRing L
inst✝³ : Algebra S L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R S L
inst✝ : FaithfulSMul S L
x : S
y : L
⊢ (∀ (z : S), y * (algebraMap S L) z ∈ adjoin R (⇑(IsScalarTower.toAlgHom R S L) '' {x})) ↔
    ∀ (z : S), y * (algebraMap S L) z ∈ R[(algebraMap S L) x]

Tactic:
Set.image_singleton

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
L : Type u_3
inst✝⁴ : CommRing L
inst✝³ : Algebra S L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R S L
inst✝ : FaithfulSMul S L
x : S
y : L
⊢ (∀ (z : S), y * (algebraMap S L) z ∈ R[(IsScalarTower.toAlgHom R S L) x]) ↔
    ∀ (z : S), y * (algebraMap S L) z ∈ R[(algebraMap S L) x]
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
L : Type u_3
inst✝⁴ : CommRing L
inst✝³ : Algebra S L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R S L
inst✝ : FaithfulSMul S L
x : S
y : L
⊢ (∀ (z : S), y * (algebraMap S L) z ∈ R[(IsScalarTower.toAlgHom R S L) x]) ↔
    ∀ (z : S), y * (algebraMap S L) z ∈ R[(algebraMap S L) x]

Tactic:
rfl

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:
Ideal.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
p : R
z : S
hp : p ∈ comap (algebraMap R S) (conductor R x)
hz' : z ∈ span (⇑(algebraMap R S) '' ↑I)
⊢ (algebraMap R S) p * z ∈ ⇑(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
p : R
z : S
hp : p ∈ comap (algebraMap R S) (conductor R x)
l : R →₀ S
H : l ∈ Finsupp.supported S S ↑I
H' : (Finsupp.linearCombination S ⇑(algebraMap R S)) l = z
⊢ (algebraMap R S) p * z ∈ ⇑(algebraMap (↥R[x]) S) '' ↑(Ideal.map (algebraMap R ↥R[x]) I)

Tactic:
rw [Finsupp.linearCombination_apply] at H'

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
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
⊢ (algebraMap R S) p * z ∈ ⇑(algebraMap (↥R[x]) S) '' ↑(Ideal.map (algebraMap R ↥R[x]) I)
Module: Mathlib.RingTheory.RingHom.QuasiFinite

Goal state before:
pp: ⊢ OfLocalizationSpanTarget fun {R S} [CommRing R] [CommRing S] ↦ QuasiFinite

Tactic:
rw [RingHom.ofLocalizationSpanTarget_iff_finite]
  introv R hs H
  algebraize [f]
  refine ⟨fun P _ ↦ ?_⟩
  have (r : s) : Module.Finite P.ResidueField (P.Fiber (Localization.Away r.1)) := by
    have : Algebra.QuasiFinite R (Localization.Away r.1) := quasiFinite_algebraMap.mp (H r)
    infer_instance
  let φ (r : s) : P.Fiber S →ₐ[P.ResidueField] P.Fiber (Localization.Away r.1) :=
    Algebra.TensorProduct.map (.id _ _) (IsScalarTower.toAlgHom _ _ _)
  let f : P.Fiber S →ₐ[P.ResidueField] Π r : s, (P.Fiber (Localization.Away r.1)) :=
    AlgHom.pi φ
  have : IsNoetherian P.ResidueField (Π r : s, (P.Fiber (Localization.Away r.1))) :=
    isNoetherian_of_isNoetherianRing_of_finite ..
  suffices Function.Injective f from .of_injective f.toLinearMap this
  rw [injective_iff_map_eq_zero]
  intro a ha
  apply eq_zero_of_localization _ fun J hJ ↦ ?_
  let I := (PrimeSpectrum.primesOverOrderIsoFiber R S P).symm ⟨J, inferInstance⟩
  have : ¬ (s : Set S) ⊆ I.1 := fun h ↦
    Ideal.IsPrime.ne_top' (top_le_iff.mp (hs.symm.trans_le (Ideal.span_le.mpr h)))
  obtain ⟨r, hrs, hrI⟩ := Set.not_subset.mp this
  let ψ : P.Fiber (Localization.Away r) →ₐ[P.ResidueField] Localization.AtPrime J :=
    Algebra.TensorProduct.lift (Algebra.ofId _ _) ⟨IsLocalization.map (M := .powers r)
      (T := J.primeCompl) _ Algebra.TensorProduct.includeRight.toRingHom (by
      simpa [Submonoid.powers_le] using! hrI), by
      simp [IsScalarTower.algebraMap_apply R S (Localization.Away r),
        -Algebra.TensorProduct.algebraMap_apply,
        ← IsScalarTower.algebraMap_apply R _ (Localization.AtPrime J)]⟩ (fun _ _ ↦ .all _ _)
  have hψ : ψ.comp (φ ⟨r, hrs⟩) = IsScalarTower.toAlgHom _ _ _ := by ext; simp [φ, ψ]
  refine congr($hψ a).symm.trans
    (show ψ (f a ⟨r, hrs⟩) = 0 by simp only [ha, Pi.zero_apply, map_zero])

Goal state after:
Module: Mathlib.RingTheory.Conductor

Goal state before:
pp: case refine_2
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
⊢ (algebraMap (↥R[x]) S) ((algebraMap R ↥R[x]) a) * (algebraMap (↥R[x]) S) ⟨l a * (algebraMap R S) p, ⋯⟩ =
    (algebraMap R S) a * (l a * (algebraMap R S) p)

Tactic:
rfl

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
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
h_alg : Function.Injective ⇑(algebraMap (↥R[x]) S)
z : S
hz : z ∈ R[x]
hy : ⟨z, hz⟩ ∈ comap (algebraMap (↥R[x]) S) (Ideal.map (algebraMap R S) I)
p : R
hp : p ∈ comap (algebraMap R S) (conductor R x)
q : R
hq : q ∈ I
hpq : p + q = 1
temp : (algebraMap R S) p * z + (algebraMap R S) q * z = z
this : z ∈ ⇑(algebraMap (↥R[x]) S) '' ↑(Ideal.map (algebraMap R ↥R[x]) I) ↔ ⟨z, hz⟩ ∈ Ideal.map (algebraMap R ↥R[x]) I
a : ↥R[x]
ha : a ∈ ↑(Ideal.map (algebraMap R ↥R[x]) I) ∧ (algebraMap (↥R[x]) S) a = (algebraMap R S) p * z
⊢ (algebraMap (↥R[x]) S) ((algebraMap R ↥R[x]) q) * (algebraMap (↥R[x]) S) ⟨z, hz⟩ = (algebraMap R S) q * z

Tactic:
rfl

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

Goal state before:
pp: K : Type u
inst✝ : CommRing K
x : FractionRing K[X]
⊢ { toFractionRing := x } = { toFractionRing := { toFractionRing := x }.toFractionRing }

Tactic:
rfl

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
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
x✝ : R
⊢ (algebraMap R S) x✝ = ((algebraMap (↥R[x]) S).comp (algebraMap R ↥R[x])) x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.RingTheory.Conductor

Goal state before:
pp: case h
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)
f : ↥R[x] ⧸ Ideal.map (algebraMap R ↥R[x]) I →+* S ⧸ Ideal.map (algebraMap R S) I :=
  Ideal.Quotient.lift (Ideal.map (algebraMap R ↥R[x]) I)
    ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)).comp (algebraMap (↥R[x]) S)) ⋯
y : S ⧸ Ideal.map (algebraMap R S) I
z : S
hz : (Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) z = y
u : S
hu : u ∈ conductor R x
hu' : (Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) u = y
⊢ ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)).comp (algebraMap (↥R[x]) S)) ⟨u, ⋯⟩ =
    (Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) u

Tactic:
rfl

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

Goal state before:
pp: K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
⊢ Transcendental K ((algebraMap (Polynomial K) K⟮X⟯) Polynomial.X)

Tactic:
transcendental_algebraMap_iff (algebraMap_injective K)

Goal state after:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
⊢ Transcendental K Polynomial.X
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
hm₁' : (eval (X ^ m) q).Monic
⊢ p.natDegree < m

Tactic:
grind

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

Goal state before:
pp: case inr
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
hm₁' : (eval (X ^ m) q).Monic
hm₂ : p.natDegree < m
⊢ IsIntegral R (p.coeff i)

Tactic:
have h₀ : algebraMap R[X] S[X] X = X := by simp

Goal state after:
case inr
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
hm₁' : (eval (X ^ m) q).Monic
hm₂ : p.natDegree < m
h₀ : (algebraMap R[X] S[X]) X = X
⊢ IsIntegral R (p.coeff i)
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
σ : Type w
f : MvPolynomial σ S
H : (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)).IsIntegralElem f
n : σ →₀ ℕ
this :
  ∀ {σ : Type w} {f : MvPolynomial σ S},
    (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)).IsIntegralElem f →
      ∀ (n : σ →₀ ℕ), Finite σ → IsIntegral R (coeff n f)
hσ : ¬Finite σ
g : MvPolynomial (↥f.vars) S
hg : (rename Subtype.val) g = f
hn : n ∉ Set.range (Finsupp.mapDomain Subtype.val)
⊢ ∀ (u : ↥f.vars →₀ ℕ), Finsupp.mapDomain Subtype.val u = n → coeff u g = 0

Tactic:
grind

Goal state after:
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✝¹ : WeaklyQuasiFiniteAt R p
q : Ideal T
inst✝ : q.IsPrime
f : Localization.AtPrime p →ₐ[R] Localization.AtPrime q
hf : Function.Surjective ⇑f
⊢ WeaklyQuasiFiniteAt R q

Tactic:
by
  rw [weaklyQuasiFiniteAt_iff] at *
  have H : (p.under R).map (algebraMap R _) ≤
      ((q.under R).map (algebraMap R _)).comap f.toRingHom := by
    rw [Ideal.map_le_iff_le_comap, Ideal.comap_comap, AlgHom.toRingHom_eq_coe,
      AlgHom.comp_algebraMap_of_tower]
    grw [← Ideal.le_comap_map]
    intro x hx
    by_contra hx'
    have : IsLocalHom f.toRingHom := .of_surjective _ hf
    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])
    exact (IsLocalization.AtPrime.isUnit_mk'_iff (Localization.AtPrime p) p
      (algebraMap _ _ x) 1).mp (by simpa [IsLocalization.mk'_one]) hx
  exact .of_surjective_algHom (S := Localization.AtPrime p ⧸
    (p.under R).map (algebraMap R (Localization.AtPrime p))) (Ideal.quotientMapₐ _ f H)
    (Ideal.quotientMap_surjective (H := H) hf)

Goal state after:
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
⊢ (algebraMap R J.ResidueField) x✝ = (algebraMap R[X] J.ResidueField) (C x✝)

Tactic:
rfl

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

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
inst✝⁴ : p.IsPrime
inst✝³ : QuasiFiniteAt R (Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap R S) (Ideal.under R p))) p)
A : Type u_4
inst✝² : CommRing A
inst✝¹ : Algebra R A
q : Ideal (A ⊗[R] S)
inst✝ : q.IsPrime
hq : p = Ideal.comap TensorProduct.includeRight.toRingHom q
φ : A ⊗[R] S →ₐ[A] (A ⧸ Ideal.under A q) ⊗[R] (S ⧸ Ideal.map (algebraMap R S) (Ideal.under R p)) :=
  TensorProduct.map (Ideal.Quotient.mkₐ A (Ideal.under A q))
    (Ideal.Quotient.mkₐ R (Ideal.map (algebraMap R S) (Ideal.under R p)))
hφ₁ : Function.Surjective ⇑φ
hφ₂ : RingHom.ker φ.toRingHom = Ideal.map (algebraMap A (A ⊗[R] S)) (Ideal.under A q)
hφ₃ :
  φ.comp TensorProduct.includeRight.toRingHom =
    TensorProduct.includeRight.comp (Ideal.Quotient.mk (Ideal.map (algebraMap R S) (Ideal.under R p)))
this✝¹ : (Ideal.map φ.toRingHom q).IsPrime
this✝ : QuasiFiniteAt (A ⧸ Ideal.under A q) (Ideal.map φ.toRingHom q)
this : QuasiFiniteAt A (Ideal.map φ.toRingHom q)
e : (A ⊗[R] S ⧸ Ideal.map (algebraMap A (A ⊗[R] S)) (Ideal.under A q)) ≃ₐ[A]
  (A ⧸ Ideal.under A q) ⊗[R] (S ⧸ Ideal.map (algebraMap R S) (Ideal.under R p)) :=
  ((Ideal.map (algebraMap A (A ⊗[R] S)) (Ideal.under A q)).quotientEquivAlg (RingHom.ker φ) AlgEquiv.refl ⋯).trans
    (Ideal.quotientKerAlgEquivOfSurjective hφ₁)
⊢ Ideal.map φ.toRingHom q =
    Ideal.map ((↑e.toRingEquiv).comp (Ideal.Quotient.mk (Ideal.map (algebraMap A (A ⊗[R] S)) (Ideal.under A q)))) q

Tactic:
rfl

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
p : Ideal R
q : Ideal S
inst✝⁴ : q.IsPrime
inst✝³ : p.IsPrime
inst✝² : q.LiesOver p
Q : Ideal (p.Fiber S)
inst✝¹ : Q.IsPrime
hQ : Ideal.comap TensorProduct.includeRight.toRingHom Q = q
inst✝ : QuasiFiniteAt p.ResidueField Q
Sq : Type u_2 := Localization.AtPrime q
this : Algebra (Localization.AtPrime p) (Localization.AtPrime q) := Localization.AtPrime.algebraOfLiesOver p q
⊢ IsLocalRing.maximalIdeal (Localization.AtPrime p) ≤
    Ideal.comap (IsScalarTower.toAlgHom R (Localization.AtPrime p) Sq) (Ideal.map (algebraMap R Sq) p)

Tactic:
rw [← IsLocalization.AtPrime.map_eq_maximalIdeal p, Ideal.map_le_iff_le_comap,
      ← Ideal.comap_coe (F := AlgHom _ _ _), Ideal.comap_comap]
    simpa [← IsScalarTower.algebraMap_eq] using Ideal.le_comap_map

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

Goal state before:
pp: case refine_1.refine_1
R S : CommRingCat
φ : R ⟶ S
hf : ∀ (x : ↥(Spec R)), LocallyQuasiFinite (Hom.fiberToSpecResidueField (Spec.map φ) x)
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom φ).toAlgebra
x : ↥(Spec R)
hP : x.asIdeal.IsPrime
⊢ Spec.map φ = Spec.map (CommRingCat.ofHom (algebraMap ↑R ↑S))

Tactic:
rfl

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

Goal state before:
pp: X : Scheme
⊢ { I₀ := X.AffineZariskiSite, X := fun U ↦ ↑↑U, f := fun U ↦ (↑U).ι }.presieve₀ ∈
    (precoverage IsOpenImmersion).coverings X

Tactic:
presieve₀_mem_precoverage_iff

Goal state after:
X : Scheme
⊢ (∀ (x : ↥X), ∃ i, x ∈ Set.range ⇑({ I₀ := X.AffineZariskiSite, X := fun U ↦ ↑↑U, f := fun U ↦ (↑U).ι }.f i)) ∧
    ∀ (i : { I₀ := X.AffineZariskiSite, X := fun U ↦ ↑↑U, f := fun U ↦ (↑U).ι }.I₀),
      IsOpenImmersion ({ I₀ := X.AffineZariskiSite, X := fun U ↦ ↑↑U, f := fun U ↦ (↑U).ι }.f i)
Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski

Goal state before:
pp: X : Scheme
U V : (directedCover X).I₀
x : ↥(pullback ((directedCover X).f U) ((directedCover X).f V))
a : ↥X := (pullback.fst ((directedCover X).f U) ((directedCover X).f V) ≫ (↑U).ι) x
haU : a ∈ ↑U
haV : a ∈ ↑V
f : ↑Γ(X, ↑U)
g : ↑Γ(X, ↑V)
e : X.basicOpen f = X.basicOpen g
hxf : a ∈ X.basicOpen f
⊢ a = ↑((TopCat.Hom.hom (pullback.fst (↑U).ι (↑V).ι).base) x)

Tactic:
rfl

Goal state after: