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

Goal state before:
pp: case map_mul
R : Type u_1
I : Type u_2
A : I → Type u_3
inst✝³ : CommRing R
inst✝² : (i : I) → CommRing (A i)
inst✝¹ : (i : I) → Algebra R (A i)
inst✝ : Finite I
val✝ : Fintype I
H : ∀ (i : I), FormallySmooth R (A i)
B : Type (max u_1 u_2 u_3)
x✝¹ : CommRing B
x✝ : Algebra R B
J : Ideal B
hJ : J ^ 2 = ⊥
g : ((i : I) → A i) →ₐ[R] B ⧸ J
hJ' : ∀ x ∈ RingHom.ker (Ideal.Quotient.mk J), IsNilpotent x
e : I → B
he : CompleteOrthogonalIdempotents e
he' : ∀ (i : I), (Ideal.Quotient.mk J) (e i) = g (Pi.single i 1)
iso : B ≃ₐ[R] (i : I) → B ⧸ Ideal.span {1 - e i} := ⋯
J' : (i : I) → Ideal (B ⧸ Ideal.span {1 - e i}) := ⋯
ι : (i : I) → B ⧸ J →ₐ[R] (B ⧸ Ideal.span {1 - e i}) ⧸ J' i := ⋯
hι : ∀ (i : I) (x : B ⧸ J), (ι i) x = 0 → (Ideal.Quotient.mk J) (e i) * x = 0
i : I
⊢ ∀ (x y : A i),
    (((ι i).comp g).toLinearMap ∘ₗ LinearMap.single R A i) (x * y) =
      (((ι i).comp g).toLinearMap ∘ₗ LinearMap.single R A i) x *
        (((ι i).comp g).toLinearMap ∘ₗ LinearMap.single R A i) y

Tactic:
intro x y; simp [Pi.single_mul]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing A
inst✝ : Algebra R A
a : A
⊢ 0 ⊗ₜ[R] (a • 0) = 0 ⊗ₜ[R] 0

Tactic:
smul_zero

Goal state after:
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing A
inst✝ : Algebra R A
a : A
⊢ 0 ⊗ₜ[R] 0 = 0 ⊗ₜ[R] 0
Module: Mathlib.RingTheory.AdicCompletion.Algebra

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
r : AdicCompletion I R
x : M ⧸ I ^ n • ⊤
⊢ ↑r n • x = (evalₐ I n) r • x

Tactic:
by
  induction r using induction_on; rfl

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra R S
I : Ideal S
f : A →ₐ[R] S ⧸ I
inst✝ : FormallySmooth R A
m : ℕ
T : Type u_3 := S ⧸ I ^ (m + 1 + 1)
J : Ideal T := Ideal.map (Ideal.Quotient.mkₐ R (I ^ (m + 1 + 1))) (I ^ (m + 1))
q : A →ₐ[R] T ⧸ J := (↑(DoubleQuot.quotQuotEquivQuotOfLEₐ R ⋯).symm).comp (liftAdicCompletionAux (m + 1))
⊢ J ^ (m + 1 + 1) = 0

Tactic:
rw [← Ideal.map_pow, Submodule.zero_eq_bot, ← pow_mul]

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra R S
I : Ideal S
f : A →ₐ[R] S ⧸ I
inst✝ : FormallySmooth R A
m : ℕ
T : Type u_3 := S ⧸ I ^ (m + 1 + 1)
J : Ideal T := Ideal.map (Ideal.Quotient.mkₐ R (I ^ (m + 1 + 1))) (I ^ (m + 1))
q : A →ₐ[R] T ⧸ J := (↑(DoubleQuot.quotQuotEquivQuotOfLEₐ R ⋯).symm).comp (liftAdicCompletionAux (m + 1))
⊢ Ideal.map (Ideal.Quotient.mkₐ R (I ^ (m + 1 + 1))) (I ^ ((m + 1) * (m + 1 + 1))) = ⊥
Module: Mathlib.RingTheory.Extension.Presentation.Submersive

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
⊢ (localizationAway S r).jacobiMatrix = Matrix.diagonal fun x ↦ C r

Tactic:
by
  have h : (pderiv ()) (C r * X () - 1) = C r := by simp
  ext (i : Unit) (j : Unit) : 1
  rwa [jacobiMatrix_apply]

Goal state after:
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 : P.Ring
⊢ (compLocalizationAwayAlgHom T g P) (((localizationAway T g).toComp P).toAlgHom x) =
    (algebraMap P.Ring (Localization.Away ((Ideal.Quotient.mk (P.ker ^ 2)) (P.σ g)))) x

Tactic:
simp only [toComp_toAlgHom, compLocalizationAwayAlgHom, comp,
    localizationAway, AlgHom.toRingHom_eq_coe, aeval_rename,
    Sum.elim_comp_inr, ← IsScalarTower.toAlgHom_apply (R := R), ← comp_aeval_apply,
    aeval_X_left_apply]

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

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
σ✝ : Type u_3
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
⊢ Function.Surjective ⇑(algebraMap P.Ring D.T)

pp: case refine_3
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
⊢ IsUnit ((algebraMap P.Ring S) D.g)

Tactic:
· simp [T, Ideal.Quotient.mk_surjective]

Goal state after:
case refine_3
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
⊢ IsUnit ((algebraMap P.Ring S) D.g)
Module: Mathlib.RingTheory.RingHom.StandardSmooth

Goal state before:
pp: n : ℕ
R S T : Type u_2
x✝² : CommRing R
x✝¹ : CommRing S
x✝ : CommRing T
f : S →+* T
e : R ≃+* S
hf : IsStandardSmoothOfRelativeDimension n f
⊢ IsStandardSmoothOfRelativeDimension n (f.comp e.toRingHom)

Tactic:
rw [← add_zero n]

Goal state after:
n : ℕ
R S T : Type u_2
x✝² : CommRing R
x✝¹ : CommRing S
x✝ : CommRing T
f : S →+* T
e : R ≃+* S
hf : IsStandardSmoothOfRelativeDimension n f
⊢ IsStandardSmoothOfRelativeDimension (n + 0) (f.comp e.toRingHom)
Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
x : ↥X
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
hVU : V ≤ f ⁻¹ᵁ U
hx : x ∈ V
this✝¹ : Algebra ↑Γ(Y, U) ↑Γ(X, V) := (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).toAlgebra
p : Ideal ↑Γ(Y, U) := (hU.primeIdealOf ⟨f x, ⋯⟩).asIdeal
q : Ideal ↑Γ(X, V) := (hV.primeIdealOf ⟨x, hx⟩).asIdeal
this✝ : q.LiesOver p
this : Algebra (Localization.AtPrime p) (Localization.AtPrime q) := Localization.AtPrime.algebraOfLiesOver p q
⊢ (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).FormallySmooth ↔
    hV.primeIdealOf ⟨x, hx⟩ ∈ Algebra.smoothLocus ↑Γ(Y, U) ↑Γ(X, V)

Tactic:
trans Algebra.FormallySmooth (Localization.AtPrime p) (Localization.AtPrime q)

Goal state after:
X Y : Scheme
f : X ⟶ Y
x : ↥X
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
hVU : V ≤ f ⁻¹ᵁ U
hx : x ∈ V
this✝¹ : Algebra ↑Γ(Y, U) ↑Γ(X, V) := ⋯
p : Ideal ↑Γ(Y, U) := ⋯
q : Ideal ↑Γ(X, V) := ⋯
this✝ : q.LiesOver p
this : Algebra (Localization.AtPrime p) (Localization.AtPrime q) := ⋯
⊢ (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).FormallySmooth ↔
    Algebra.FormallySmooth (Localization.AtPrime p) (Localization.AtPrime q)

X Y : Scheme
f : X ⟶ Y
x : ↥X
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
hVU : V ≤ f ⁻¹ᵁ U
hx : x ∈ V
this✝¹ : Algebra ↑Γ(Y, U) ↑Γ(X, V) := ⋯
p : Ideal ↑Γ(Y, U) := ⋯
q : Ideal ↑Γ(X, V) := ⋯
this✝ : q.LiesOver p
this : Algebra (Localization.AtPrime p) (Localization.AtPrime q) := ⋯
⊢ Algebra.FormallySmooth (Localization.AtPrime p) (Localization.AtPrime q) ↔
    hV.primeIdealOf ⟨x, hx⟩ ∈ Algebra.smoothLocus ↑Γ(Y, U) ↑Γ(X, V)
Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth

Goal state before:
pp: case refine_2
X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFinitePresentation f
x : ↥X
H : (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).FormallySmooth
U : TopologicalSpace.Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : f x ∈ ↑U
V : TopologicalSpace.Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hVU : ↑V ⊆ ⇑f ⁻¹' U.carrier
this✝ : (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).FinitePresentation
algInst✝ : Algebra ↑Γ(Y, U) ↑Γ(X, V) := (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).toAlgebra
algebraizeInst✝ : Algebra.FinitePresentation ↑Γ(Y, U) ↑Γ(X, V)
this : Algebra.IsSmoothAt (↑Γ(Y, U)) (IsAffineOpen.primeIdealOf hV ⟨x, hxV⟩).asIdeal
r : ↑Γ(X, V)
hrx : r ∉ (IsAffineOpen.primeIdealOf hV ⟨x, hxV⟩).asIdeal
hr : Algebra.Smooth (↑Γ(Y, U)) (Localization.Away r)
⊢ (CommRingCat.Hom.hom (Scheme.Hom.appLE f U (X.basicOpen r) ⋯)).Smooth

Tactic:
have := hV.isLocalization_basicOpen r
    rw [← RingHom.smooth_algebraMap] at hr
    convert!
      RingHom.Smooth.propertyIsLocal.respectsIso.1 _
        (IsLocalization.algEquiv (.powers r) _ Γ(X, X.basicOpen r)).toRingEquiv hr
    ext
    dsimp
    simp only [IsScalarTower.algebraMap_apply Γ(Y, U) Γ(X, V) (Localization _),
      IsLocalization.map_eq]
    simp only [algebraMap_toAlgebra, RingHomCompTriple.comp_apply, ← ConcreteCategory.comp_apply,
      Scheme.Hom.appLE_map]

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'.negAddY P Q = -(Q y ^ 2 * P z) * W'.negY P

Tactic:
rw [negAddY, hQz, X_eq_zero_of_Z_eq_zero hQ hQz, negY]

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 * Q y + 3 * P x * 0 ^ 2 * P y - P y ^ 2 * Q y * 0 + P y * Q y ^ 2 * P z +
                                W'.a₁ * P x * Q y ^ 2 * P z -
                              W'.a₁ * 0 * P y ^ 2 * 0 -
                            W'.a₂ * P x ^ 2 * Q y * 0 +
                          W'.a₂ * 0 ^ 2 * P y * P z +
                        2 * W'.a₂ * P x * 0 * P y * 0 -
                      2 * W'.a₂ * P x * 0 * Q y * P z -
                    W'.a₃ * P y ^ 2 * 0 ^ 2 +
                  W'.a₃ * Q y ^ 2 * P z ^ 2 +
                W'.a₄ * P x * P y * 0 ^ 2 -
              2 * W'.a₄ * P x * Q y * P z * 0 +
            2 * W'.a₄ * 0 * P y * P z * 0 -
          W'.a₄ * 0 * Q y * P z ^ 2 +
        3 * W'.a₆ * P y * P z * 0 ^ 2 -
      3 * W'.a₆ * Q y * P z ^ 2 * 0 =
    -(Q y ^ 2 * P z) * (-P y - W'.a₁ * P x - W'.a₃ * P z)
Module: Mathlib.AlgebraicGeometry.Morphisms.LocalClosure

Goal state before:
pp: W P Q : MorphismProperty Scheme
X✝ Y✝ : Scheme
inst✝² : W.IsStableUnderBaseChange
inst✝¹ : Scheme.IsJointlySurjectivePreserving W
inst✝ : P.RespectsRight Q
X Y Z : Scheme
f : Y ⟶ Z
hf : Q f
g : X ⟶ Y
x✝ : sourceLocalClosure W P g
𝒰 : Scheme.Cover (Scheme.precoverage W) X
hg : ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ g)
i : 𝒰.I₀
⊢ P (𝒰.f i ≫ g ≫ f)

Tactic:
← Category.assoc

Goal state after:
W P Q : MorphismProperty Scheme
X✝ Y✝ : Scheme
inst✝² : W.IsStableUnderBaseChange
inst✝¹ : Scheme.IsJointlySurjectivePreserving W
inst✝ : P.RespectsRight Q
X Y Z : Scheme
f : Y ⟶ Z
hf : Q f
g : X ⟶ Y
x✝ : sourceLocalClosure W P g
𝒰 : Scheme.Cover (Scheme.precoverage W) X
hg : ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ g)
i : 𝒰.I₀
⊢ P ((𝒰.f i ≫ g) ≫ f)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

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

Tactic:
erw [addY, negY_of_Z_ne_zero <| addZ_ne_zero_of_X_ne hP hQ hx, addX_of_Z_ne_zero hP hQ hPz hQz hx,
    negAddY_of_Z_ne_zero hP hQ hPz hQz hx, Affine.addY]

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

Goal state before:
pp: X Y Z' Z : Scheme
i : Z' ⟶ Z
inst✝¹ : IsClosedImmersion i
f : X ⟶ Y
inst✝ : FormallyUnramified f
g₁ g₂ : Z ⟶ X
hig : i ≫ g₁ = i ≫ g₂
hgf : g₁ ≫ f = g₂ ≫ f
n : ℕ
hn : Scheme.Hom.ker i ^ n = 0
⊢ closure (Set.range ⇑i) = Set.univ

Tactic:
← i.support_ker,

Goal state after:
X Y Z' Z : Scheme
i : Z' ⟶ Z
inst✝¹ : IsClosedImmersion i
f : X ⟶ Y
inst✝ : FormallyUnramified f
g₁ g₂ : Z ⟶ X
hig : i ≫ g₁ = i ≫ g₂
hgf : g₁ ≫ f = g₂ ≫ f
n : ℕ
hn : Scheme.Hom.ker i ^ n = 0
⊢ ↑(Scheme.Hom.ker i).support = Set.univ
Module: Mathlib.CategoryTheory.MorphismProperty.Descent

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
P✝ Q✝ W : MorphismProperty C
A X✝ Y✝ Z✝ : C
fst : A ⟶ X✝
snd : A ⟶ Y✝
f✝ : X✝ ⟶ Z✝
g✝ : Y✝ ⟶ Z✝
inst✝⁴ : HasPullbacks C
P Q : MorphismProperty C
inst✝³ : P.DescendsAlong Q
inst✝² : P.RespectsIso
inst✝¹ : Q.IsStableUnderBaseChange
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : HasPullback f g
hf : Q f
hfst : P.diagonal (pullback.fst f g)
heq :
  pullback.fst (pullback.fst (pullback.snd g g ≫ g) f) (pullback.diagonal g) =
    (pullbackSymmetry (pullback.fst (pullback.snd g g ≫ g) f) (pullback.diagonal g)).hom ≫
      (pullbackRightPullbackFstIso (pullback.snd g g ≫ g) f (pullback.diagonal g)).hom ≫
        (pullback.congrHom ⋯ ⋯).hom ≫
          (pullbackSymmetry g f).hom ≫ pullback.diagonal (pullback.fst f g) ≫ (diagonalObjPullbackFstIso f g).hom
⊢ P.diagonal g

Tactic:
diagonal_iff

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
P✝ Q✝ W : MorphismProperty C
A X✝ Y✝ Z✝ : C
fst : A ⟶ X✝
snd : A ⟶ Y✝
f✝ : X✝ ⟶ Z✝
g✝ : Y✝ ⟶ Z✝
inst✝⁴ : HasPullbacks C
P Q : MorphismProperty C
inst✝³ : P.DescendsAlong Q
inst✝² : P.RespectsIso
inst✝¹ : Q.IsStableUnderBaseChange
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : HasPullback f g
hf : Q f
hfst : P.diagonal (pullback.fst f g)
heq :
  pullback.fst (pullback.fst (pullback.snd g g ≫ g) f) (pullback.diagonal g) =
    (pullbackSymmetry (pullback.fst (pullback.snd g g ≫ g) f) (pullback.diagonal g)).hom ≫
      (pullbackRightPullbackFstIso (pullback.snd g g ≫ g) f (pullback.diagonal g)).hom ≫
        (pullback.congrHom ⋯ ⋯).hom ≫
          (pullbackSymmetry g f).hom ≫ pullback.diagonal (pullback.fst f g) ≫ (diagonalObjPullbackFstIso f g).hom
⊢ P (pullback.diagonal g)
Module: Mathlib.RingTheory.RingHom.Injective

Goal state before:
pp: ⊢ RingHom.StableUnderComposition fun {R S} [CommRing R] [CommRing S] f ↦ Function.Injective ⇑f

Tactic:
by
  intro R S T _ _ _ f g hf hg
  simp only [RingHom.coe_comp]
  exact Function.Injective.comp hg hf

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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
hf : f.IsStandardOpenImmersion
hg : g.IsStandardOpenImmersion
⊢ (g.comp f).IsStandardOpenImmersion

Tactic:
by
  algebraize [f, g, g.comp f]
  obtain ⟨r, hr⟩ := hf
  obtain ⟨s, hs⟩ := hg
  exact .trans _ S _

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

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : HasPullback f g
hf : (@Surjective ⊓ @Flat ⊓ @QuasiCompact) f
hg : IsOpenImmersion (pullback.fst f g)
this✝ : UniversallyOpen g
U : Z.Opens := { carrier := Set.range ⇑g, is_open' := ⋯ }
f' : pullback f U.ι ⟶ ↑U := pullback.snd f U.ι
g' : Y ⟶ ↑U := IsOpenImmersion.lift U.ι g ⋯
this : Surjective g'
⊢ IsOpenImmersion g

Tactic:
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 _ _)

Goal state after:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : HasPullback f g
hf : (@Surjective ⊓ @Flat ⊓ @QuasiCompact) f
hg : IsOpenImmersion (pullback.fst f g)
this✝¹ : UniversallyOpen g
U : Z.Opens := { carrier := Set.range ⇑g, is_open' := ⋯ }
f' : pullback f U.ι ⟶ ↑U := pullback.snd f U.ι
g' : Y ⟶ ↑U := IsOpenImmersion.lift U.ι g ⋯
this✝ : Surjective g'
this : IsIso (pullback.fst f' g')
⊢ IsOpenImmersion g
Module: Mathlib.RingTheory.Algebraic.StronglyTranscendental

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing T
inst✝ : Algebra R T
x : S
f : S →ₐ[R] T
hf : Function.Injective ⇑f
h : IsStronglyTranscendental R (f x)
u : S
p : R[X]
hp : (aeval x) p * u = 0
this : map (↑f) (map (algebraMap R S) p * C u) = 0
⊢ map (algebraMap R S) p * C u = 0

Tactic:
← coe_mapRingHom,

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
x : S
f : S →ₐ[R] T
hf : Function.Injective ⇑f
h : IsStronglyTranscendental R (f x)
u : S
p : R[X]
hp : (aeval x) p * u = 0
this : (mapRingHom ↑f) (map (algebraMap R S) p * C u) = 0
⊢ map (algebraMap R S) p * C u = 0
Module: Mathlib.RingTheory.IntegralClosure.GoingDown

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
p q : R[X]
hp : p.Monic
hq : q.Monic
H : q ∣ p
i : ℕ
hi : i ≠ q.natDegree
P : Ideal R
hPJ : Ideal.span {x | ∃ i < p.natDegree, p.coeff i = x} ≤ P
hP : P.IsPrime
this : map (Ideal.Quotient.mk P) p = X ^ p.natDegree
j : ℕ
hj : j ≤ p.natDegree
a : (R ⧸ P)[X]ˣ
ha : map (Ideal.Quotient.mk P) q * ↑a = X ^ j
r : R ⧸ P
hr : IsUnit r
e : C r = ↑a⁻¹
⊢ q.coeff i ∈ P

Tactic:
rw [← Units.eq_mul_inv_iff_mul_eq, ← e] at ha

Goal state after:
R : Type u_1
inst✝ : CommRing R
p q : R[X]
hp : p.Monic
hq : q.Monic
H : q ∣ p
i : ℕ
hi : i ≠ q.natDegree
P : Ideal R
hPJ : Ideal.span {x | ∃ i < p.natDegree, p.coeff i = x} ≤ P
hP : P.IsPrime
this : map (Ideal.Quotient.mk P) p = X ^ p.natDegree
j : ℕ
hj : j ≤ p.natDegree
a : (R ⧸ P)[X]ˣ
r : R ⧸ P
ha : map (Ideal.Quotient.mk P) q = X ^ j * C r
hr : IsUnit r
e : C r = ↑a⁻¹
⊢ q.coeff i ∈ P
Module: Mathlib.FieldTheory.RatFunc.AsPolynomial

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
f : L
h : Transcendental K f
g : K[X]
⊢ (algEquivOfTranscendental f h).symm ((aeval (AdjoinSimple.gen K f)) g) = (algebraMap K[X] K⟮X⟯) g

Tactic:
by
  simp [algEquivOfTranscendental, ← algebraMap_eq_gen_self, aeval_algebraMap_apply]

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

Goal state before:
pp: K✝ : Type u
K : Type u_1
inst✝ : Field K
⊢ (Ideal.span {X}).IsPrime

Tactic:
Ideal.span_singleton_prime

Goal state after:
K✝ : Type u
K : Type u_1
inst✝ : Field K
⊢ Prime X

K✝ : Type u
K : Type u_1
inst✝ : Field K
⊢ X ≠ 0
Module: Mathlib.RingTheory.Polynomial.IsIntegral

Goal state before:
pp: case pos
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
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
n : ↥f.vars →₀ ℕ
⊢ IsIntegral R (coeff (Finsupp.mapDomain Subtype.val n) ((rename Subtype.val) g))

Tactic:
coeff_rename_mapDomain _ Subtype.val_injective

Goal state after:
case pos
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
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
n : ↥f.vars →₀ ℕ
⊢ IsIntegral R (coeff n g)
Module: Mathlib.RingTheory.QuasiFinite.Polynomial

Goal state before:
pp: case inr
R : Type u_1
inst✝¹ : CommRing R
P : Ideal R[X]
inst✝ : P.IsPrime
H : Algebra.WeaklyQuasiFiniteAt R P
this :
  ∀ {R : Type u_1} [inst : CommRing R] (P : Ideal R[X]) [inst_1 : P.IsPrime],
    Algebra.WeaklyQuasiFiniteAt R P → IsField R → False
hR : ¬IsField R
⊢ False

Tactic:
let p := P.under R
    obtain ⟨Q, hQ⟩ := (PrimeSpectrum.preimageEquivFiber R R[X]
        ⟨p, inferInstance⟩).symm.surjective ⟨⟨P, ‹_›⟩, rfl⟩
    have inst : Algebra.WeaklyQuasiFiniteAt p.ResidueField Q.asIdeal :=
      .baseChange P Q.asIdeal congr($(hQ.symm).1.1)
    exact this (Q.asIdeal.comap (polyEquivTensor' R p.ResidueField).toRingHom)
      inferInstance (Field.toIsField _)

Goal state after:
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

Goal state after:
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)) ⋯)).comp
      (Ideal.Quotient.mkₐ p.ResidueField (Ideal.map (mapRingHom (algebraMap R p.ResidueField)) (RingHom.ker ↑f))) =
    (AlgHom.id p.ResidueField
          (p.ResidueField[X] ⧸ Ideal.map (mapRingHom (algebraMap R p.ResidueField)) (RingHom.ker ↑f))).comp
      (Ideal.Quotient.mkₐ p.ResidueField (Ideal.map (mapRingHom (algebraMap R p.ResidueField)) (RingHom.ker ↑f)))
Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski

Goal state before:
pp: X : Scheme
U : X.AffineZariskiSite
S : Sieve U
⊢ S ∈ (grothendieckTopology X) U ↔ ∀ x ∈ U.toOpens, ∃ V f, S.arrows f ∧ x ∈ V.toOpens

Tactic:
rw [grothendieckTopology, Functor.mem_inducedTopology_iff_of_isCoverDense]
  apply forall₂_congr fun x hxU ↦ ⟨?_, ?_⟩
  · rintro ⟨V, f, ⟨W, g, h, hg, rfl⟩, hxV⟩
    exact ⟨W, g, hg, h.le hxV⟩
  · rintro ⟨W, g, hg, hxW⟩
    exact ⟨W.toOpens, homOfLE (toOpens_mono g.le), ⟨W, g, 𝟙 _, hg, rfl⟩, hxW⟩

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

Goal state before:
pp: case pos
K : Type u
inst✝⁴ : CommRing K
R : Type u_1
inst✝³ : IsDomain K
inst✝² : Monoid R
inst✝¹ : DistribMulAction R K[X]
inst✝ : IsScalarTower R K[X] K[X]
c : R
p q : K[X]
this : SMulZeroClass R (FractionRing K[X]) := inferInstance
hq : q = 0
⊢ { toFractionRing := 0 } = { toFractionRing := c • 0 }

Tactic:
smul_zero

Goal state after:
case pos
K : Type u
inst✝⁴ : CommRing K
R : Type u_1
inst✝³ : IsDomain K
inst✝² : Monoid R
inst✝¹ : DistribMulAction R K[X]
inst✝ : IsScalarTower R K[X] K[X]
c : R
p q : K[X]
this : SMulZeroClass R (FractionRing K[X]) := inferInstance
hq : q = 0
⊢ { toFractionRing := 0 } = { toFractionRing := 0 }