mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.Sites.BigZariski

Goal state before:
pp: x✝⁵ : Scheme
x✝⁴ : Presieve x✝⁵
hR : x✝⁴ ∈ (precoverage IsOpenImmersion).coverings x✝⁵
x✝³ x✝² : Scheme
f : x✝³ ⟶ x✝⁵
x✝¹ : x✝² ⟶ x✝⁵
hf : x✝⁴ f
x✝ : x✝⁴ x✝¹
⊢ PreservesLimit (cospan f x✝¹) forgetToTop

Tactic:
have : IsOpenImmersion f := hR.2 hf

Goal state after:
x✝⁵ : Scheme
x✝⁴ : Presieve x✝⁵
hR : x✝⁴ ∈ (precoverage IsOpenImmersion).coverings x✝⁵
x✝³ x✝² : Scheme
f : x✝³ ⟶ x✝⁵
x✝¹ : x✝² ⟶ x✝⁵
hf : x✝⁴ f
x✝ : x✝⁴ x✝¹
this : IsOpenImmersion f
⊢ PreservesLimit (cospan f x✝¹) forgetToTop
Module: Mathlib.RingTheory.RingHom.Unramified

Goal state before:
pp: R : Type u_3
⊢ ∀ {S : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] (e : R ≃+* S), e.toRingHom.FormallyUnramified

Tactic:
S

Goal state after:
R S : Type u_3
⊢ ∀ [inst : CommRing R] [inst_1 : CommRing S] (e : R ≃+* S), e.toRingHom.FormallyUnramified
Module: Mathlib.RingTheory.RingHom.Unramified

Goal state before:
pp: R : Type u_3
⊢ ∀ (S : Type u_3) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (M : Submonoid R)
    [IsLocalization M S], (fun {R S} [CommRing R] [CommRing S] ↦ FormallyUnramified) (algebraMap R S)

Tactic:
S

Goal state after:
R S : Type u_3
⊢ ∀ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (M : Submonoid R) [IsLocalization M S],
    (fun {R S} [CommRing R] [CommRing S] ↦ FormallyUnramified) (algebraMap R S)
Module: Mathlib.RingTheory.RingHom.Unramified

Goal state before:
pp: R : Type u_3
⊢ ∀ ⦃S : Type u_3⦄ [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
    (∀ (J : Ideal S) (x : J.IsPrime),
        (fun {R S} [CommRing R] [CommRing S] ↦ FormallyUnramified)
          (Localization.localRingHom (Ideal.comap f J) J f ⋯)) →
      (fun {R S} [CommRing R] [CommRing S] ↦ FormallyUnramified) f

Tactic:
S

Goal state after:
R S : Type u_3
⊢ ∀ [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
    (∀ (J : Ideal S) (x : J.IsPrime),
        (fun {R S} [CommRing R] [CommRing S] ↦ FormallyUnramified)
          (Localization.localRingHom (Ideal.comap f J) J f ⋯)) →
      (fun {R S} [CommRing R] [CommRing S] ↦ FormallyUnramified) f
Module: Mathlib.RingTheory.RingHom.Unramified

Goal state before:
pp: R : Type u_3
⊢ ∀ ⦃S : Type u_3⦄ [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) (s : Set S),
    Ideal.span s = ⊤ →
      (∀ (r : ↑s),
          (fun {R S} [CommRing R] [CommRing S] ↦ FormallyUnramified) ((algebraMap S (Localization.Away ↑r)).comp f)) →
        (fun {R S} [CommRing R] [CommRing S] ↦ FormallyUnramified) f

Tactic:
S

Goal state after:
R S : Type u_3
⊢ ∀ [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) (s : Set S),
    Ideal.span s = ⊤ →
      (∀ (r : ↑s),
          (fun {R S} [CommRing R] [CommRing S] ↦ FormallyUnramified) ((algebraMap S (Localization.Away ↑r)).comp f)) →
        (fun {R S} [CommRing R] [CommRing S] ↦ FormallyUnramified) f
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
f : A
⊢ ↑(PrimeSpectrum.basicOpen f) ⊆ etaleLocus R A ↔ FormallyEtale R (Localization.Away f)

Tactic:
rw [etaleLocus_eq_compl_support, Set.subset_inter_iff, Set.subset_compl_comm,
    PrimeSpectrum.basicOpen_eq_zeroLocus_compl, compl_compl, Set.subset_compl_comm, compl_compl,
    ← LocalizedModule.subsingleton_iff_support_subset,
    ← LocalizedModule.subsingleton_iff_support_subset, formallyEtale_iff]

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : A
⊢ Subsingleton (LocalizedModule.Away f Ω[A⁄R]) ∧ Subsingleton (LocalizedModule.Away f (H1Cotangent R A)) ↔
    Subsingleton Ω[Localization.Away f⁄R] ∧ Subsingleton (H1Cotangent R (Localization.Away f))
Module: Mathlib.RingTheory.Smooth.Fiber

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : Module.Flat R S
inst✝⁴ : FinitePresentation R S
p : Ideal R
q : Ideal S
inst✝³ : p.IsPrime
inst✝² : q.IsPrime
inst✝¹ : q.LiesOver p
inst✝ : FormallySmooth p.ResidueField (p.Fiber S)
Rp : Type u_1 := Localization.AtPrime p
Sp : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
Sq : Type u_2 := Localization.AtPrime q
this✝¹ : Algebra (Localization.AtPrime p) (Localization.AtPrime q) := Localization.AtPrime.algebraOfLiesOver p q
f : Sp →ₐ[S] Sq := IsLocalization.liftAlgHom ⋯
algInst✝ : Algebra Sp Sq := f.toAlgebra
this✝ : IsScalarTower R Sp Sq
this : IsScalarTower Rp Sp Sq
⊢ IsSmoothAt R q

Tactic:
have : IsLocalization (algebraMapSubmonoid Sp q.primeCompl) Sq :=
    .isLocalization_of_submonoid_le _ _ (algebraMapSubmonoid S p.primeCompl) _
    (by rintro _ ⟨x, hx, rfl⟩; simp_all [q.over_def p])

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : Module.Flat R S
inst✝⁴ : FinitePresentation R S
p : Ideal R
q : Ideal S
inst✝³ : p.IsPrime
inst✝² : q.IsPrime
inst✝¹ : q.LiesOver p
inst✝ : FormallySmooth p.ResidueField (p.Fiber S)
Rp : Type u_1 := Localization.AtPrime p
Sp : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
Sq : Type u_2 := Localization.AtPrime q
this✝² : Algebra (Localization.AtPrime p) (Localization.AtPrime q) := Localization.AtPrime.algebraOfLiesOver p q
f : Sp →ₐ[S] Sq := IsLocalization.liftAlgHom ⋯
algInst✝ : Algebra Sp Sq := f.toAlgebra
this✝¹ : IsScalarTower R Sp Sq
this✝ : IsScalarTower Rp Sp Sq
this : IsLocalization (algebraMapSubmonoid Sp q.primeCompl) Sq
⊢ IsSmoothAt R q
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
P : PreSubmersivePresentation R S ι σ
inst✝ : Finite σ
⊢ IsUnit P.aevalDifferential ↔ Function.Bijective ⇑P.aevalDifferential

Tactic:
exact Module.End.isUnit_iff P.aevalDifferential

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

Goal state before:
pp: n m : ℕ
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : Finite σ
T : Type u_1
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : IsStandardSmoothOfRelativeDimension n R S
⊢ ∃ ι σ, ∃ (x : Finite σ) (_ : Finite ι), ∃ P, P.dimension = n

Tactic:
obtain ⟨_, _, _, _, P, hP⟩ := ‹IsStandardSmoothOfRelativeDimension n R S›
    exact ⟨_, _, _, inferInstance, P.baseChange T, hP⟩

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

Goal state before:
pp: n m : ℕ
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : Finite σ
T : Type u_1
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : IsStandardSmoothOfRelativeDimension n R S
⊢ ∃ ι σ, ∃ (x : Finite σ) (_ : Finite ι), ∃ P, P.dimension = n

Tactic:
by
    obtain ⟨_, _, _, _, P, hP⟩ := ‹IsStandardSmoothOfRelativeDimension n R S›
    exact ⟨_, _, _, inferInstance, P.baseChange T, hP⟩

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 ι σ
x : ↥P.ker
hx : ∀ (i : σ), (aeval P.val) ((pderiv (P.map i)) ↑x) = 0
this✝ : ↑x ∈ Ideal.span (Set.range P.relation)
c : σ →₀ P.Ring
hc : (c.sum fun i a ↦ a * P.relation i) = ↑x
heq : ∀ (i : σ), ∑ x ∈ c.support, (aeval P.val) (c x) * (aeval P.val) ((pderiv (P.map i)) (P.relation x)) = 0
heq2 : (∑ i ∈ c.support, (aeval P.val) (c i) • fun j ↦ (aeval P.val) ((pderiv (P.map j)) (P.relation i))) = 0
this : ∀ (i : σ), (aeval P.val) (c i) = 0
⊢ ↑x ∈ P.ker ^ 2

Tactic:
← hc

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 ι σ
x : ↥P.ker
hx : ∀ (i : σ), (aeval P.val) ((pderiv (P.map i)) ↑x) = 0
this✝ : ↑x ∈ Ideal.span (Set.range P.relation)
c : σ →₀ P.Ring
hc : (c.sum fun i a ↦ a * P.relation i) = ↑x
heq : ∀ (i : σ), ∑ x ∈ c.support, (aeval P.val) (c x) * (aeval P.val) ((pderiv (P.map i)) (P.relation x)) = 0
heq2 : (∑ i ∈ c.support, (aeval P.val) (c i) • fun j ↦ (aeval P.val) ((pderiv (P.map j)) (P.relation i))) = 0
this : ∀ (i : σ), (aeval P.val) (c i) = 0
⊢ (c.sum fun i a ↦ a * P.relation i) ∈ P.ker ^ 2
Module: Mathlib.RingTheory.Smooth.StandardSmoothCotangent

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Nontrivial S
inst✝ : IsStandardSmooth R S
n : ℕ
h : Module.rank S Ω[S⁄R] = ↑n
w✝² w✝¹ : Type
w✝ : Finite w✝¹
left✝ : Finite w✝²
P : SubmersivePresentation R S w✝² w✝¹
⊢ IsStandardSmoothOfRelativeDimension n R S

Tactic:
refine ⟨_, _, _, ‹_›, ⟨P, ?_⟩⟩

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Nontrivial S
inst✝ : IsStandardSmooth R S
n : ℕ
h : Module.rank S Ω[S⁄R] = ↑n
w✝² w✝¹ : Type
w✝ : Finite w✝¹
left✝ : Finite w✝²
P : SubmersivePresentation R S w✝² w✝¹
⊢ P.dimension = n
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ W'.dblXYZ P = P y ^ 4 • ![0, 1, 0]

Tactic:
by
  erw [dblXYZ, dblX_of_Z_eq_zero hP hPz, dblY_of_Z_eq_zero hP hPz, dblZ_of_Z_eq_zero hPz, smul_fin3,
    mul_zero, mul_one]

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

Goal state before:
pp: case neg
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ✝ : Type u_3
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
x : MvPolynomial ι R ⧸ Ideal.span (Set.range (Subtype.val ∘ D.f ∘ ⇑b))
h✝¹ : ¬x = 0
h✝ : ¬x = -1
⊢ (Ideal.Quotient.mk (Ideal.span (Set.range (Subtype.val ∘ D.f ∘ ⇑b)))) (Function.surjInv ⋯ x) = x

Tactic:
· simp [Function.surjInv_eq]

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
a : ι → K
F : MvPolynomial ι k
HF : ∀ (F' : MvPolynomial ι k), F' ≠ 0 → (aeval a) F' = 0 → F.totalDegree ≤ F'.totalDegree
hF0 : F ≠ 0
hFa : (aeval a) F = 0
this : ∀ (i : ι), ∀ σ ∈ F.support, p ∣ σ i
σ' : (ι →₀ ℕ) → ι →₀ ℕ
hσ' : ∀ σ ∈ F.support, σ = p • σ' σ
hσ'' : ∀ (σ : ↥F.support), ↑σ = p • σ' ↑σ
H : ∀ (ι : Type u_3) (x : Fintype ι) (v : ι → K), LinearIndependent k v → LinearIndependent k fun x ↦ v x ^ p
F' : ↥F.support →₀ k
hF' : (Finsupp.linearCombination k fun s ↦ (aeval a) ((monomial (σ' ↑s)) 1)) F' = 0
hF'0 : ¬F' = 0
F'' : MvPolynomial ι k := AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain (fun s ↦ σ' ↑s) F')
hF''0 : F'' ≠ 0
⊢ ((aeval a).toLinearMap ∘ₗ ↑(AddMonoidAlgebra.coeffLinearEquiv k).symm ∘ₗ Finsupp.lmapDomain k k fun s ↦ σ' ↑s) =
    Finsupp.linearCombination k fun s ↦ (aeval a) ((monomial (σ' ↑s)) 1)

Tactic:
ext v

Goal state after:
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
a : ι → K
F : MvPolynomial ι k
HF : ∀ (F' : MvPolynomial ι k), F' ≠ 0 → (aeval a) F' = 0 → F.totalDegree ≤ F'.totalDegree
hF0 : F ≠ 0
hFa : (aeval a) F = 0
this : ∀ (i : ι), ∀ σ ∈ F.support, p ∣ σ i
σ' : (ι →₀ ℕ) → ι →₀ ℕ
hσ' : ∀ σ ∈ F.support, σ = p • σ' σ
hσ'' : ∀ (σ : ↥F.support), ↑σ = p • σ' ↑σ
H : ∀ (ι : Type u_3) (x : Fintype ι) (v : ι → K), LinearIndependent k v → LinearIndependent k fun x ↦ v x ^ p
F' : ↥F.support →₀ k
hF' : (Finsupp.linearCombination k fun s ↦ (aeval a) ((monomial (σ' ↑s)) 1)) F' = 0
hF'0 : ¬F' = 0
F'' : MvPolynomial ι k := ⋯
hF''0 : F'' ≠ 0
v : ↥F.support
⊢ (((aeval a).toLinearMap ∘ₗ ↑(AddMonoidAlgebra.coeffLinearEquiv k).symm ∘ₗ Finsupp.lmapDomain k k fun s ↦ σ' ↑s) ∘ₗ
        Finsupp.lsingle v)
      1 =
    ((Finsupp.linearCombination k fun s ↦ (aeval a) ((monomial (σ' ↑s)) 1)) ∘ₗ Finsupp.lsingle v) 1
Module: Mathlib.AlgebraicGeometry.Morphisms.Etale

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ HasOfPostcompProperty (@Etale) (@LocallyOfFiniteType ⊓ @FormallyUnramified)

Tactic:
rw [MorphismProperty.hasOfPostcompProperty_iff_le_diagonal]

Goal state after:
X Y : Scheme
f : X ⟶ Y
⊢ @LocallyOfFiniteType ⊓ @FormallyUnramified ≤ diagonal @Etale
Module: Mathlib.AlgebraicGeometry.Morphisms.LocalIso

Goal state before:
pp: case refine_1
⊢ @IsLocalIso ≤ ⨅ P, ⨅ (_ : P.ContainsIdentities), ⨅ (_ : IsZariskiLocalAtSource P), P

pp: case refine_2
⊢ ⨅ P, ⨅ (_ : P.ContainsIdentities), ⨅ (_ : IsZariskiLocalAtSource P), P ≤ @IsLocalIso

Tactic:
· simp only [le_iInf_iff]
    apply le_of_isZariskiLocalAtSource

Goal state after:
case refine_2
⊢ ⨅ P, ⨅ (_ : P.ContainsIdentities), ⨅ (_ : IsZariskiLocalAtSource P), P ≤ @IsLocalIso
Module: Mathlib.RingTheory.RingHom.Injective

Goal state before:
pp: R : Type u_1
⊢ ∀ ⦃S T : Type u_1⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S) (g : S →+* T),
    (fun {R S} [CommRing R] [CommRing S] f ↦ Function.Injective ⇑f) f →
      (fun {R S} [CommRing R] [CommRing S] f ↦ Function.Injective ⇑f) g →
        (fun {R S} [CommRing R] [CommRing S] f ↦ Function.Injective ⇑f) (g.comp f)

Tactic:
S

Goal state after:
R S : Type u_1
⊢ ∀ ⦃T : Type u_1⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S) (g : S →+* T),
    (fun {R S} [CommRing R] [CommRing S] f ↦ Function.Injective ⇑f) f →
      (fun {R S} [CommRing R] [CommRing S] f ↦ Function.Injective ⇑f) g →
        (fun {R S} [CommRing R] [CommRing S] f ↦ Function.Injective ⇑f) (g.comp f)
Module: Mathlib.RingTheory.RingHom.Injective

Goal state before:
pp: R : Type u_1
⊢ ∀ {S : Type u_1} [inst : CommRing R] [inst_1 : CommRing S] (e : R ≃+* S), Function.Injective ⇑e.toRingHom

Tactic:
S

Goal state after:
R S : Type u_1
⊢ ∀ [inst : CommRing R] [inst_1 : CommRing S] (e : R ≃+* S), Function.Injective ⇑e.toRingHom
Module: Mathlib.CategoryTheory.MorphismProperty.Descent

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P Q : MorphismProperty C
inst✝ : P.RespectsIso
H : ∀ {X Y Z : C} {f : Z ⟶ X} {g : Z ⟶ Y} [inst : HasPushout f g], Q f → P (pushout.inl f g) → P g
A X Y Z : C
f : A ⟶ X
g : A ⟶ Y
inl : X ⟶ Z
inr : Y ⟶ Z
h : IsPushout f g inl inr
hf : Q f
hfst : P inl
⊢ P g

Tactic:
have : HasPushout f g := h.hasPushout
    apply H hf
    rwa [← P.cancel_right_of_respectsIso _ h.isoPushout.inv, h.inl_isoPushout_inv]

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

Goal state before:
pp: case H
R : CommRingCat
⊢ ∀ {S : CommRingCat} {Y : Scheme} (φ : R ⟶ S) (g : Y ⟶ Spec R),
    (@Surjective ⊓ @Flat) (Spec.map φ) → isomorphisms Scheme (pullback.fst (Spec.map φ) g) → isomorphisms Scheme g

Tactic:
S

Goal state after:
case H
R S : CommRingCat
⊢ ∀ {Y : Scheme} (φ : R ⟶ S) (g : Y ⟶ Spec R),
    (@Surjective ⊓ @Flat) (Spec.map φ) → isomorphisms Scheme (pullback.fst (Spec.map φ) g) → isomorphisms Scheme g
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent

Goal state before:
pp: case refine_2
P : MorphismProperty Scheme
inst✝¹ : P.IsStableUnderBaseChange
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P fun {R S} [CommRing R] [CommRing S] ↦ Q
h :
  RingHom.CodescendsAlong (fun {R S} [CommRing R] [CommRing S] ↦ Q) fun {R S} [CommRing R] [CommRing S] ↦
    RingHom.FaithfullyFlat
R : CommRingCat
⊢ ∀ {S : CommRingCat} {f : R ⟶ S}, (@Surjective ⊓ @Flat) (Spec.map f) → (CommRingCat.Hom.hom f).FaithfullyFlat

Tactic:
S

Goal state after:
case refine_2
P : MorphismProperty Scheme
inst✝¹ : P.IsStableUnderBaseChange
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P fun {R S} [CommRing R] [CommRing S] ↦ Q
h :
  RingHom.CodescendsAlong (fun {R S} [CommRing R] [CommRing S] ↦ Q) fun {R S} [CommRing R] [CommRing S] ↦
    RingHom.FaithfullyFlat
R S : CommRingCat
⊢ ∀ {f : R ⟶ S}, (@Surjective ⊓ @Flat) (Spec.map f) → (CommRingCat.Hom.hom f).FaithfullyFlat
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) a * (algebraMap R S) p ∈ ⇑(algebraMap (↥R[x]) S) '' ↑(Ideal.map (algebraMap R ↥R[x]) I)

Tactic:
rw [smul_eq_mul, mul_assoc, mul_comm, mul_assoc, Set.mem_image]

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
a : R
ha : a ∈ I
⊢ ∃ x_1 ∈ ↑(Ideal.map (algebraMap R ↥R[x]) I),
    (algebraMap (↥R[x]) S) x_1 = (algebraMap R S) a * ((algebraMap R S) p * l a)
Module: Mathlib.FieldTheory.RatFunc.Defs

Goal state before:
pp: K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
p q p' q' : K[X]
hq : q ≠ 0
hq' : q' ≠ 0
⊢ RatFunc.mk p q = RatFunc.mk p' q' ↔ p * q' = p' * q

Tactic:
rw [mk_def_of_ne _ hq, mk_def_of_ne _ hq', ofFractionRing_injective.eq_iff,
    IsLocalization.mk'_eq_iff_eq',
    (IsFractionRing.injective K[X] (FractionRing K[X])).eq_iff]

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

Goal state before:
pp: case pos
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
P : Sort v
p q : K[X]
f : K[X] → K[X] → P
f0 : ∀ (p : K[X]), f p 0 = f 0 1
H' : ∀ {p q p' q' : K[X]}, q ≠ 0 → q' ≠ 0 → q' * p = q * p' → f p q = f p' q'
H : ∀ {p q p' q' : K[X]}, q ∈ K[X]⁰ → q' ∈ K[X]⁰ → q' * p = q * p' → f p q = f p' q'
hq : q = 0
⊢ (RatFunc.mk p q).liftOn f H = f p q

Tactic:
subst hq

Goal state after:
case pos
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
P : Sort v
p : K[X]
f : K[X] → K[X] → P
f0 : ∀ (p : K[X]), f p 0 = f 0 1
H' : ∀ {p q p' q' : K[X]}, q ≠ 0 → q' ≠ 0 → q' * p = q * p' → f p q = f p' q'
H : ∀ {p q p' q' : K[X]}, q ∈ K[X]⁰ → q' ∈ K[X]⁰ → q' * p = q * p' → f p q = f p' q'
⊢ (RatFunc.mk p 0).liftOn f H = f p 0
Module: Mathlib.RingTheory.LocalRing.ResidueField.Polynomial

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
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
x : R[X]
hx : ∀ (i : ℕ), x.coeff i ∈ I
⊢ x ∈ J

Tactic:
rwa [hJ, Ideal.mem_map_C_iff]

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 : S →ₐ[R] T
hf : f.SurjectiveOnStalks
hq : p = Ideal.comap f q
⊢ WeaklyQuasiFiniteAt R q

Tactic:
subst hq

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
q : Ideal T
inst✝² : q.IsPrime
f : S →ₐ[R] T
hf : f.SurjectiveOnStalks
inst✝¹ : (Ideal.comap f q).IsPrime
inst✝ : WeaklyQuasiFiniteAt R (Ideal.comap f q)
⊢ WeaklyQuasiFiniteAt R q
Module: Mathlib.RingTheory.Polynomial.IsIntegral

Goal state before:
pp: case e'_5
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type w
hσ : Finite σ
f : MvPolynomial PEmpty.{w + 1} S
H : (algebraMap (MvPolynomial PEmpty.{w + 1} R) (MvPolynomial PEmpty.{w + 1} S)).IsIntegralElem f
n : PEmpty.{w + 1} →₀ ℕ
⊢ ((isEmptyAlgEquiv S PEmpty.{w + 1}).symm.toRingEquiv.toRingHom.comp (algebraMap R S)).comp
      (isEmptyAlgEquiv R PEmpty.{w + 1}).toRingEquiv.toRingHom =
    algebraMap (MvPolynomial PEmpty.{w + 1} R) (MvPolynomial PEmpty.{w + 1} S)

Tactic:
ext r m <;> simp [Subsingleton.elim m 0, C, X, monomial, coeff, map]

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)
⊢ QuasiFiniteAt A (Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap A (A ⊗[R] S)) (Ideal.under A q))) q)

Tactic:
have hφ₃ : φ.toRingHom.comp Algebra.TensorProduct.includeRight.toRingHom =
      Algebra.TensorProduct.includeRight.toRingHom.comp (Ideal.Quotient.mk _) := rfl

Goal state after:
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)))
⊢ QuasiFiniteAt A (Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap A (A ⊗[R] S)) (Ideal.under A q))) q)
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
⊢ p ≤
    Ideal.comap (algebraMap R (Localization.AtPrime p))
      (Ideal.comap (IsScalarTower.toAlgHom R (Localization.AtPrime p) Sq) (Ideal.map (algebraMap R Sq) p))

Tactic:
← Ideal.comap_coe (F := AlgHom _ _ _),

Goal state after:
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
⊢ p ≤
    Ideal.comap (algebraMap R (Localization.AtPrime p))
      (Ideal.comap (↑(IsScalarTower.toAlgHom R (Localization.AtPrime p) Sq)) (Ideal.map (algebraMap R Sq) p))
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
hf : ∀ (x : ↥Y), LocallyQuasiFinite (Hom.fiberToSpecResidueField f x)
this✝ :
  ∀ {X Y : Scheme} (f : X ⟶ Y),
    (∀ (x : ↥Y), LocallyQuasiFinite (Hom.fiberToSpecResidueField f x)) → (∃ R, Y = Spec R) → id (LocallyQuasiFinite f)
hY : ¬∃ R, Y = Spec R
i : Y.affineCover.toPreZeroHypercover.1
x : ↥(Y.affineCover.X i)
this : ∀ (x : ↥Y), IsLocallyArtinian (Hom.fiber f x)
⊢ pullback.snd f (Y.affineCover.f i) ≫ Y.affineCover.f i = pullback.fst f (Y.affineCover.f i) ≫ f

Tactic:
by simp [pullback.condition]

Goal state after: