mathlib-initiative/mathlib-tactics huggingface dataset:
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₀) ((MvPolynomial.aeval P.val) x) =
    1 ⊗ₜ[R₀] (Ideal.Quotient.mk (Ideal.span (Set.range (relationOfHasCoeffs R₀)))) x

Tactic:
rw [← MvPolynomial.aeval_map_algebraMap R, ← Generators.algebraMap_apply, ← quotientEquiv_mk]
  simp [tensorModelOfHasCoeffsInv, -quotientEquiv_symm, -quotientEquiv_mk]

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

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hQ : W'.Equation Q
hQz : Q z = 0
⊢ W'.addZ P Q = -(Q y ^ 2 * P z) * P z

Tactic:
rw [addZ, hQz, X_eq_zero_of_Z_eq_zero hQ hQz]

Goal state after:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hQ : W'.Equation Q
hQz : Q z = 0
⊢ -3 * P x ^ 2 * 0 * 0 + 3 * P x * 0 ^ 2 * P z + P y ^ 2 * 0 ^ 2 - Q y ^ 2 * P z ^ 2 + W'.a₁ * P x * P y * 0 ^ 2 -
                  W'.a₁ * 0 * Q y * P z ^ 2 -
                W'.a₂ * P x ^ 2 * 0 ^ 2 +
              W'.a₂ * 0 ^ 2 * P z ^ 2 +
            W'.a₃ * P y * P z * 0 ^ 2 -
          W'.a₃ * Q y * P z ^ 2 * 0 -
        W'.a₄ * P x * P z * 0 ^ 2 +
      W'.a₄ * 0 * P z ^ 2 * 0 =
    -(Q y ^ 2 * P z) * P z
Module: Mathlib.RingTheory.RingHom.StandardSmooth

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

Tactic:
introv h

Goal state after:
case h₂
R S T : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : (algebraMap R T).IsStandardSmooth
⊢ (algebraMap S (S ⊗[R] T)).IsStandardSmooth
Module: Mathlib.RingTheory.RingHom.StandardSmooth

Goal state before:
pp: case h₁
n : ℕ
⊢ RespectsIso (@IsStandardSmoothOfRelativeDimension n)

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

Tactic:
· exact isStandardSmoothOfRelativeDimension_respectsIso

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

Goal state before:
pp: case h₂
n : ℕ
⊢ ∀ ⦃R S T : Type u_2⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
    [inst_4 : Algebra R T],
    IsStandardSmoothOfRelativeDimension n (algebraMap R T) →
      IsStandardSmoothOfRelativeDimension n (algebraMap S (S ⊗[R] T))

Tactic:
introv h

Goal state after:
case h₂
n : ℕ
R S T : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : IsStandardSmoothOfRelativeDimension n (algebraMap R T)
⊢ IsStandardSmoothOfRelativeDimension n (algebraMap S (S ⊗[R] T))
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
D : DescentAux A B
inst✝¹ : Finite D.vars
inst✝ : Finite D.rels
⊢ (subalgebra R D).FG

Tactic:
by
  refine Subalgebra.fg_def.mpr ⟨_, ?_, rfl⟩
  refine .union ?_ (.union (.union ?_ ?_) ?_)
  · exact Presentation.finite_coeffs
  · refine Set.finite_iUnion fun i ↦ Finset.finite_toSet _
  · refine Set.finite_iUnion fun i ↦ ?_
    exact Set.Finite.biUnion (Finset.finite_toSet _) (fun i hi ↦ Finset.finite_toSet _)
  · refine Set.finite_iUnion fun i ↦ ?_
    exact Set.Finite.biUnion (Finset.finite_toSet _) (fun i hi ↦ Finset.finite_toSet _)

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

Goal state before:
pp: K : Type u_1
L : Type u_2
ι : Type u_3
inst✝⁴ : Field L
inst✝³ : Field K
inst✝² : Algebra K L
inst✝¹ : PerfectField K
inst✝ : EssFiniteType K L
⊢ FormallySmooth K L

Tactic:
obtain ⟨s, hs, H⟩ := exists_isTranscendenceBasis_and_isSeparable_of_perfectField K L
  have : Algebra.IsSeparable (↥(IntermediateField.adjoin K (Set.range ((↑) : s → L)))) L := by
    convert! H <;> simp
  exact .of_algebraicIndependent_of_isSeparable hs.1

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
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
⊢ (F.toPolynomialAdjoinImageCompl a i).coeff (σ i) ≠ 0

Tactic:
intro H
  let F₀ := optionEquivLeft k _ (renameEquiv k (Equiv.optionSubtypeNe i).symm F)
  have H := HF (rename (↑) (F₀.coeff (σ i))) ?_ ?_
  · have : (F₀.coeff (σ i)).totalDegree + σ i ≤ _ :=
      totalDegree_coeff_optionEquivLeft_add_le _ _ _ (σ i) <| by
        rw [totalDegree_renameEquiv]
        exact (Finsupp.le_degree ..).trans (le_totalDegree hσ)
    rw [totalDegree_renameEquiv] at this
    simpa [hσi] using (this.trans H).trans (totalDegree_rename_le _ _)
  · refine (map_eq_zero_iff _ (rename_injective _ Subtype.val_injective)).not.mpr fun H ↦ ?_
    let e := (Equiv.optionSubtypeNe i).symm
    have : coeff _ (F₀.coeff _) = _ :=
      optionEquivLeft_coeff_some_coeff_none _ _ (σ.equivMapDomain e) (renameEquiv k e F)
    dsimp only [F₀] at this
    rw [renameEquiv_apply, Finsupp.equivMapDomain_eq_mapDomain, coeff_rename_mapDomain _
      e.injective, Finsupp.mapDomain_equiv_apply, Equiv.symm_symm, Equiv.optionSubtypeNe_none,
      ← renameEquiv_apply, H, coeff_zero, eq_comm, ← notMem_support_iff] at this
    exact this hσ
  · apply_fun Subalgebra.val _ at H
    simp_rw [toPolynomialAdjoinImageCompl, Polynomial.coe_mapAlgHom, Polynomial.coeff_map,
      AlgHom.coe_toRingHom, map_zero] at H
    simp_rw [← H, ← AlgHom.comp_apply]
    congr; ext; simp

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝² : Flat f
inst✝¹ : FormallyUnramified f
inst✝ : LocallyOfFinitePresentation f
⊢ Etale f

Tactic:
rw [Etale.iff_flat_and_formallyUnramified]

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝² : Flat f
inst✝¹ : FormallyUnramified f
inst✝ : LocallyOfFinitePresentation f
⊢ Flat f ∧ FormallyUnramified f ∧ LocallyOfFinitePresentation f
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
inst✝ : ExpChar k p
s : Set ι
n : ι
ha : IsTranscendenceBasis k fun i ↦ a ↑i
hn : n ∉ s
e₁ : { j // j ≠ ⟨n, ⋯⟩ } ≃ ↑s :=
  { toFun := fun x ↦ ⟨↑↑x, ⋯⟩, invFun := fun x ↦ ⟨⟨↑x, ⋯⟩, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
i : ↑(insert n s)
hi : IsTranscendenceBasis k fun j ↦ a ↑↑j
hi' : IsSeparable (↥(adjoin k ((fun i ↦ a ↑i) '' {i}ᶜ))) (a ↑i)
⊢ ∃ i, (IsTranscendenceBasis k fun j ↦ a ↑j) ∧ IsSeparable (↥(adjoin k (a '' (insert n s \ {i})))) (a i)

Tactic:
let e₂ : {j // j ≠ i} ≃ ↥(insert n s \ {i.1}) := ⟨fun x ↦ ⟨x, x.1.2, fun h ↦ x.2 (Subtype.ext h)⟩,
    fun x ↦ ⟨⟨x, x.2.1⟩, fun h ↦ x.2.2 congr($h.1)⟩, fun _ ↦ rfl, fun _ ↦ rfl⟩

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
H : ∀ (s : Finset K), LinearIndepOn k id ↑s → LinearIndepOn k (fun x ↦ x ^ p) ↑s
a : ι → K
inst✝ : ExpChar k p
s : Set ι
n : ι
ha : IsTranscendenceBasis k fun i ↦ a ↑i
hn : n ∉ s
e₁ : { j // j ≠ ⟨n, ⋯⟩ } ≃ ↑s :=
  { toFun := fun x ↦ ⟨↑↑x, ⋯⟩, invFun := fun x ↦ ⟨⟨↑x, ⋯⟩, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
i : ↑(insert n s)
hi : IsTranscendenceBasis k fun j ↦ a ↑↑j
hi' : IsSeparable (↥(adjoin k ((fun i ↦ a ↑i) '' {i}ᶜ))) (a ↑i)
e₂ : { j // j ≠ i } ≃ ↑(insert n s \ {↑i}) :=
  { toFun := fun x ↦ ⟨↑↑x, ⋯⟩, invFun := fun x ↦ ⟨⟨↑x, ⋯⟩, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
⊢ ∃ i, (IsTranscendenceBasis k fun j ↦ a ↑j) ∧ IsSeparable (↥(adjoin k (a '' (insert n s \ {i})))) (a i)
Module: Mathlib.RingTheory.RingHom.OpenImmersion

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ (algebraMap R S).IsStandardOpenImmersion ↔ Algebra.IsStandardOpenImmersion R S

Tactic:
rw [IsStandardOpenImmersion, toAlgebra_algebraMap]

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

Goal state before:
pp: ⊢ ∀ ⦃R S T : Type u⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
    [inst_4 : Algebra R T],
    (algebraMap R T).IsStandardOpenImmersion → (algebraMap S (TensorProduct R S T)).IsStandardOpenImmersion

Tactic:
introv h

Goal state after:
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : (algebraMap R T).IsStandardOpenImmersion
⊢ (algebraMap S (TensorProduct R S T)).IsStandardOpenImmersion
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent

Goal state before:
pp: ⊢ IsOpenImmersion.DescendsAlong (@Surjective ⊓ @Flat ⊓ @QuasiCompact)

Tactic:
apply DescendsAlong.mk'
  intro X Y Z f g _ hf hg
  have : UniversallyOpen g :=
    MorphismProperty.of_pullback_fst_of_descendsAlong
      (P := @UniversallyOpen) (Q := @Surjective ⊓ @Flat ⊓ @QuasiCompact) (f := f)
      hf inferInstance
  let U : Z.Opens := ⟨Set.range g.base, g.isOpenMap.isOpen_range⟩
  let f' := pullback.snd f U.ι
  let g' : Y ⟶ U := IsOpenImmersion.lift U.ι g (by simp [U])
  have : Surjective g' := ⟨fun ⟨x, ⟨y, hy⟩⟩ ↦
    ⟨y, by apply U.ι.injective; simp [← Scheme.Hom.comp_apply, g', hy]⟩⟩
  have : IsIso (pullback.fst f' g') := by
    rw [isIso_iff_isOpenImmersion_and_surjective]
    refine ⟨?_, inferInstance⟩
    have : IsOpenImmersion (pullback.fst f (g' ≫ U.ι)) := by
      rwa [AlgebraicGeometry.IsOpenImmersion.lift_fac]
    have : IsOpenImmersion (pullback.fst f' g' ≫ pullback.fst f U.ι) := by
      rw [← pullbackLeftPullbackSndIso_hom_fst]
      infer_instance
    exact .of_comp _ (pullback.fst _ _)
  have : IsIso g' := by
    apply MorphismProperty.of_pullback_fst_of_descendsAlong
      (P := isomorphisms Scheme) (Q := @Surjective ⊓ @Flat ⊓ @QuasiCompact) (f := f') ?_ this
    exact MorphismProperty.pullback_snd _ _ hf
  rw [← IsOpenImmersion.lift_fac U.ι g (by simp [U])]
  infer_instance

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.GoingDown

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : IsDomain S
inst✝⁴ : FaithfulSMul R S
inst✝³ : Algebra.IsIntegral R S
inst✝² : IsIntegrallyClosed R
this✝ : IsDomain R
p : Ideal R
inst✝¹ : p.IsPrime
Q : Ideal S
inst✝ : Q.IsPrime
hpQ : p < Ideal.under R Q
SQ : Type u_2 := Localization.AtPrime Q
this : Ideal.comap (algebraMap R SQ) (Ideal.map (algebraMap R SQ) p) ≤ p
⊢ ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p

Tactic:
obtain ⟨P, hP, e⟩ :=
      (Ideal.comap_map_eq_self_iff_of_isPrime _).mp (this.antisymm Ideal.le_comap_map)
    refine ⟨P.under S, ?_, inferInstance, ⟨by rw [Ideal.under_under, ← e]⟩⟩
    exact (Ideal.comap_mono (IsLocalRing.le_maximalIdeal_of_isPrime P)).trans_eq
      Localization.AtPrime.under_maximalIdeal

Goal state after:
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
⊢ { toFractionRing := IsLocalization.mk' (FractionRing K[X]) p ⟨q, ⋯⟩ } =
      { toFractionRing := IsLocalization.mk' (FractionRing K[X]) p' ⟨q', ⋯⟩ } ↔
    p * q' = p' * q

Tactic:
ofFractionRing_injective.eq_iff,

Goal state after:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
p q p' q' : K[X]
hq : q ≠ 0
hq' : q' ≠ 0
⊢ IsLocalization.mk' (FractionRing K[X]) p ⟨q, ⋯⟩ = IsLocalization.mk' (FractionRing K[X]) p' ⟨q', ⋯⟩ ↔ p * q' = p' * q
Module: Mathlib.RingTheory.Conductor

Goal state before:
pp: case refine_1
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)) ⋯
u : ↥R[x]
hu : u ∈ ker ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)).comp (algebraMap (↥R[x]) S))
⊢ u ∈ Ideal.map (algebraMap R ↥R[x]) I

Tactic:
RingHom.mem_ker,

Goal state after:
case refine_1
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)) ⋯
u : ↥R[x]
hu : ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)).comp (algebraMap (↥R[x]) S)) u = 0
⊢ u ∈ Ideal.map (algebraMap R ↥R[x]) I
Module: Mathlib.RingTheory.QuasiFinite.Polynomial

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
f : R[X] →ₐ[R] S
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : Algebra.WeaklyQuasiFiniteAt R P
algInst✝ : Algebra R[X] S := f.toAlgebra
⊢ Ideal.under R P ≤ Ideal.comap ((↑f).comp C) P

Tactic:
← algebraMap_eq,

Goal state after:
case refine_1
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
f : R[X] →ₐ[R] S
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : Algebra.WeaklyQuasiFiniteAt R P
algInst✝ : Algebra R[X] S := f.toAlgebra
⊢ Ideal.under R P ≤ Ideal.comap ((↑f).comp (algebraMap R R[X])) P
Module: Mathlib.RingTheory.LocalRing.ResidueField.Polynomial

Goal state before:
pp: case refine_3
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
f : R[X] →ₐ[R] S
hf : Function.Surjective ⇑f
p : Ideal R
inst✝ : p.IsPrime
⊢ (Algebra.TensorProduct.lift
          (Algebra.ofId p.ResidueField
            (p.ResidueField[X] ⧸ Ideal.map (mapRingHom (algebraMap R p.ResidueField)) (RingHom.ker ↑f)))
          (f.liftOfSurjective hf
            ((Ideal.Quotient.mkₐ R (Ideal.map (mapRingHom (algebraMap R p.ResidueField)) (RingHom.ker ↑f))).comp
              (mapAlgHom (Algebra.ofId R p.ResidueField)))
            ⋯)
          ⋯).comp
      (Ideal.Quotient.liftₐ (Ideal.map (mapRingHom (algebraMap R p.ResidueField)) (RingHom.ker ↑f))
        (aeval (1 ⊗ₜ[R] f X)) ⋯) =
    AlgHom.id p.ResidueField (p.ResidueField[X] ⧸ Ideal.map (mapRingHom (algebraMap R p.ResidueField)) (RingHom.ker ↑f))

Tactic:
apply Ideal.Quotient.algHom_ext
    ext
    simp

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]
inst✝ : MonoidHomClass F R[X] S[X]
φ : F
hφ : R[X]⁰ ≤ Submonoid.comap φ S[X]⁰
⊢ RatFunc.liftOn 1 (fun n d ↦ if h : φ d ∈ S[X]⁰ then { toFractionRing := Localization.mk (φ n) ⟨φ d, h⟩ } else 0) ⋯ = 1

Tactic:
simp_rw [← ofFractionRing_one, ← Localization.mk_one, liftOn_ofFractionRing_mk,
      OneMemClass.coe_one, map_one, OneMemClass.one_mem, dite_true, ofFractionRing.injEq,
      Localization.mk_one, Localization.mk_eq_monoidOf_mk', Submonoid.LocalizationMap.mk'_self]

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

Goal state before:
pp: X : Scheme
U V : X.AffineZariskiSite
f : U ⟶ V
⊢ Spec.map (X.presheaf.map ((toOpensFunctor X).map f).op) ≫ ⋯.fromSpec = ⋯.fromSpec ≫ 𝟙 X

Tactic:
V.2.map_fromSpec U.2

Goal state after:
X : Scheme
U V : X.AffineZariskiSite
f : U ⟶ V
⊢ ⋯.fromSpec = ⋯.fromSpec ≫ 𝟙 X
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝ : Field K
x : K⟮X⟯
p q a : K[X]
hq : q ≠ 0
ha : a ≠ 0
ha' : a.leadingCoeff ≠ 0
hainv : a.leadingCoeff⁻¹ ≠ 0
hdeg : (gcd p q).degree ≤ q.degree
⊢ (C a.leadingCoeff⁻¹ * gcd p q).degree ≤ q.degree

Tactic:
rw [Polynomial.degree_mul, Polynomial.degree_C hainv, zero_add]

Goal state after:
K : Type u
inst✝ : Field K
x : K⟮X⟯
p q a : K[X]
hq : q ≠ 0
ha : a ≠ 0
ha' : a.leadingCoeff ≠ 0
hainv : a.leadingCoeff⁻¹ ≠ 0
hdeg : (gcd p q).degree ≤ q.degree
⊢ (gcd p q).degree ≤ q.degree
Module: Mathlib.RingTheory.Etale.StandardEtale

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : StandardEtalePair R
x : S
h : P.HasMap x
p₁ p₂ : R[X]
n : ℕ
e : derivative P.f * p₁ + P.f * p₂ = P.g ^ n
⊢ IsUnit ((aeval x) (derivative P.f))

Tactic:
have : aeval x P.f.derivative ∣ aeval x P.g ^ n :=
    ⟨_, by simpa [h.1] using congr(aeval x $e.symm)⟩

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : StandardEtalePair R
x : S
h : P.HasMap x
p₁ p₂ : R[X]
n : ℕ
e : derivative P.f * p₁ + P.f * p₂ = P.g ^ n
this : (aeval x) (derivative P.f) ∣ (aeval x) P.g ^ n
⊢ IsUnit ((aeval x) (derivative P.f))
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
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
w : P.ResidueField[X]
h₁ : Polynomial.map (algebraMap R P.ResidueField) q = Polynomial.map (algebraMap R P.ResidueField) p * w
h₂ : ¬m ∣ w
hm' : derivative m ≠ 0
this : ¬m ∣ derivative (Polynomial.map (algebraMap R P.ResidueField) q)
⊢ (aeval x) (derivative q) ∉ RingHom.ker (algebraMap S Q.ResidueField)

Tactic:
RingHom.mem_ker,

Goal state after:
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
w : P.ResidueField[X]
h₁ : Polynomial.map (algebraMap R P.ResidueField) q = Polynomial.map (algebraMap R P.ResidueField) p * w
h₂ : ¬m ∣ w
hm' : derivative m ≠ 0
this : ¬m ∣ derivative (Polynomial.map (algebraMap R P.ResidueField) q)
⊢ ¬(algebraMap S Q.ResidueField) ((aeval x) (derivative q)) = 0
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
φ : S[X] →ₐ[R] B
hφ : Function.Surjective ⇑φ
f : S[X]
hf : f.Monic
hf' : ∀ (i : ℕ), IsIntegral R (f.coeff i)
hfx : RingHom.ker φ.toRingHom = Ideal.span {f}
h✝ : Nontrivial B
hfd : f.natDegree ≠ 0
algInst✝¹ : Algebra S B := (φ.comp C).toAlgebra
this : Nontrivial S
y : S[X]
hy : IsIntegral R (φ y)
S' : Type u_2
w✝⁴ : CommRing S'
w✝³ : Algebra S S'
w✝² : Module.Finite S S'
w✝¹ : Module.Free S S'
w✝ : Nontrivial S'
hS' : (Polynomial.map (algebraMap S S') f).Splits
m : Multiset S'
hm : Polynomial.map (algebraMap S S') f = (Multiset.map (fun x ↦ X - C x) m).prod
algInst✝ : Algebra R S' := ((algebraMap S S').comp (algebraMap R S)).toAlgebra
scalarTowerInst✝ : IsScalarTower R S S' := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R S'))
hm' : ∀ a ∈ m, IsIntegral R a
hmc : m.card = f.natDegree
⊢ ∀
    x ∈
      Multiset.map
        (fun i ↦
          (Multiset.map (fun x ↦ X - C x) (m.erase i)).prod * derivative (X - C i) *
              Polynomial.map (algebraMap S S') y -
            (Multiset.map (fun x ↦ X - C x) (m.erase i)).prod * C ((aeval i) y))
        m,
    (Multiset.map (fun x ↦ X - C x) m).prod ∣ x

Tactic:
simp only [derivative_sub, derivative_X, derivative_C, sub_zero, mul_one, ← mul_sub,
        Multiset.mem_map, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]

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
φ : S[X] →ₐ[R] B
hφ : Function.Surjective ⇑φ
f : S[X]
hf : f.Monic
hf' : ∀ (i : ℕ), IsIntegral R (f.coeff i)
hfx : RingHom.ker φ.toRingHom = Ideal.span {f}
h✝ : Nontrivial B
hfd : f.natDegree ≠ 0
algInst✝¹ : Algebra S B := (φ.comp C).toAlgebra
this : Nontrivial S
y : S[X]
hy : IsIntegral R (φ y)
S' : Type u_2
w✝⁴ : CommRing S'
w✝³ : Algebra S S'
w✝² : Module.Finite S S'
w✝¹ : Module.Free S S'
w✝ : Nontrivial S'
hS' : (Polynomial.map (algebraMap S S') f).Splits
m : Multiset S'
hm : Polynomial.map (algebraMap S S') f = (Multiset.map (fun x ↦ X - C x) m).prod
algInst✝ : Algebra R S' := ((algebraMap S S').comp (algebraMap R S)).toAlgebra
scalarTowerInst✝ : IsScalarTower R S S' := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R S'))
hm' : ∀ a ∈ m, IsIntegral R a
hmc : m.card = f.natDegree
⊢ ∀ a ∈ m,
    (Multiset.map (fun x ↦ X - C x) m).prod ∣
      (Multiset.map (fun x ↦ X - C x) (m.erase a)).prod * (Polynomial.map (algebraMap S S') y - C ((aeval a) y))
Module: Mathlib.RingTheory.Polynomial.DegreeLT

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
m n : ℕ
i : Fin m
⊢ ((basis R m).prod (basis R n)) (Sum.inl i) = ((basis R m) i, 0)

Tactic:
Basis.prod_apply,

Goal state after:
R : Type u_1
inst✝ : Semiring R
m n : ℕ
i : Fin m
⊢ Sum.elim (⇑(LinearMap.inl R (↥R[X]_m) ↥R[X]_n) ∘ ⇑(basis R m)) (⇑(LinearMap.inr R (↥R[X]_m) ↥R[X]_n) ∘ ⇑(basis R n))
      (Sum.inl i) =
    ((basis R m) i, 0)
Module: Mathlib.RingTheory.Polynomial.DegreeLT

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
m n : ℕ
i : Fin n
⊢ ((basis R m).prod (basis R n)) (Sum.inr i) = (0, (basis R n) i)

Tactic:
Basis.prod_apply,

Goal state after:
R : Type u_1
inst✝ : Semiring R
m n : ℕ
i : Fin n
⊢ Sum.elim (⇑(LinearMap.inl R (↥R[X]_m) ↥R[X]_n) ∘ ⇑(basis R m)) (⇑(LinearMap.inr R (↥R[X]_m) ↥R[X]_n) ∘ ⇑(basis R n))
      (Sum.inr i) =
    (0, (basis R n) i)