mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.RingHom.StandardSmooth

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
T : Type u_1
inst✝ : CommRing T
g : S →+* T
f : R →+* S
hg : g.IsStandardSmooth
hf : f.IsStandardSmooth
algInst✝² : Algebra R S := f.toAlgebra
algInst✝¹ : Algebra S T := g.toAlgebra
algInst✝ : Algebra R T := (g.comp f).toAlgebra
scalarTowerInst✝ : IsScalarTower R S T := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R T))
algebraizeInst✝¹ : Algebra.IsStandardSmooth S T
algebraizeInst✝ : Algebra.IsStandardSmooth R S
⊢ Algebra.IsStandardSmooth R T

Tactic:
exact Algebra.IsStandardSmooth.trans R S T

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
v : ι → L
hb : AlgebraicIndependent K v
this : FormallySmooth K ↥(adjoin K (Set.range v))
⊢ FormallySmooth K ↥(IntermediateField.adjoin K (Set.range v))

Tactic:
have : Algebra.FormallySmooth (adjoin K (Set.range v))
      (IntermediateField.adjoin K (Set.range v)) :=
    .of_isLocalization (nonZeroDivisors _)

Goal state after:
K : Type u_1
L : Type u_2
ι : Type u_3
inst✝² : Field L
inst✝¹ : Field K
inst✝ : Algebra K L
v : ι → L
hb : AlgebraicIndependent K v
this✝ : FormallySmooth K ↥(adjoin K (Set.range v))
this : FormallySmooth ↥(adjoin K (Set.range v)) ↥(IntermediateField.adjoin K (Set.range v))
⊢ FormallySmooth K ↥(IntermediateField.adjoin K (Set.range v))
Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth

Goal state before:
pp: case refine_1
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 : (IsAffineOpen.isoSpec hV).hom ⟨x, hxV⟩ ∈ PrimeSpectrum.basicOpen r
hr : Algebra.Smooth (↑Γ(Y, U)) (Localization.Away r)
⊢ x ∈ X.basicOpen r

Tactic:
← hV.fromSpec_preimage_basicOpen,

Goal state after:
case refine_1
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 : (IsAffineOpen.isoSpec hV).hom ⟨x, hxV⟩ ∈ IsAffineOpen.fromSpec hV ⁻¹ᵁ X.basicOpen r
hr : Algebra.Smooth (↑Γ(Y, U)) (Localization.Away r)
⊢ x ∈ X.basicOpen r
Module: Mathlib.AlgebraicGeometry.Morphisms.Proper

Goal state before:
pp: this : @IsAffineHom ⊓ @IsSeparated = @IsAffineHom
⊢ @IsFinite = @IsAffineHom ⊓ (@IsSeparated ⊓ @UniversallyClosed ⊓ @LocallyOfFiniteType)

Tactic:
inf_assoc,

Goal state after:
this : @IsAffineHom ⊓ @IsSeparated = @IsAffineHom
⊢ @IsFinite = @IsAffineHom ⊓ (@IsSeparated ⊓ (@UniversallyClosed ⊓ @LocallyOfFiniteType))
Module: Mathlib.AlgebraicGeometry.Morphisms.Proper

Goal state before:
pp: this : @IsAffineHom ⊓ @IsSeparated = @IsAffineHom
⊢ @UniversallyClosed ⊓ @IsAffineHom ⊓ @LocallyOfFiniteType = @IsAffineHom ⊓ (@UniversallyClosed ⊓ @LocallyOfFiniteType)

Tactic:
inf_assoc,

Goal state after:
this : @IsAffineHom ⊓ @IsSeparated = @IsAffineHom
⊢ @UniversallyClosed ⊓ (@IsAffineHom ⊓ @LocallyOfFiniteType) =
    @IsAffineHom ⊓ (@UniversallyClosed ⊓ @LocallyOfFiniteType)
Module: Mathlib.FieldTheory.SeparablyGenerated

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

Tactic:
coeff_zero,

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion (pullback.diagonal f)
⊢ FormallyUnramified f

Tactic:
wlog hY : ∃ R, Y = Spec R
  · rw [IsZariskiLocalAtTarget.iff_of_openCover (P := @FormallyUnramified) Y.affineCover]
    intro i
    have inst : IsOpenImmersion (pullback.diagonal (pullback.snd f (Y.affineCover.f i))) :=
      MorphismProperty.pullback_snd (P := .diagonal @IsOpenImmersion) _ _ ‹_›
    exact this (pullback.snd _ _) ⟨_, rfl⟩
  obtain ⟨R, rfl⟩ := hY
  wlog hX : ∃ S, X = Spec S generalizing X
  · rw [IsZariskiLocalAtSource.iff_of_openCover (P := @FormallyUnramified) X.affineCover]
    intro i
    have inst : IsOpenImmersion (pullback.diagonal (X.affineCover.f i ≫ f)) :=
      MorphismProperty.comp_mem (.diagonal @IsOpenImmersion) _ _
        (inferInstanceAs (IsOpenImmersion _)) ‹_›
    exact this (_ ≫ _) ⟨_, rfl⟩
  obtain ⟨S, rfl⟩ := hX
  obtain ⟨φ, rfl : Spec.map φ = f⟩ := Spec.homEquiv.symm.surjective f
  rw [HasRingHomProperty.Spec_iff (P := @FormallyUnramified)]
  algebraize [φ.hom]
  let F := (Algebra.TensorProduct.lmul' R (S := S)).toRingHom
  have hF : Function.Surjective F := fun x ↦ ⟨.mk _ _ _ x 1, by simp [F]⟩
  have : IsOpenImmersion (Spec.map (CommRingCat.ofHom F)) := by
    rwa [← MorphismProperty.cancel_right_of_respectsIso (P := @IsOpenImmersion) _
      (pullbackSpecIso R S S).inv, ← AlgebraicGeometry.diagonal_SpecMap R S]
  obtain ⟨e, he, he'⟩ := (isOpenImmersion_SpecMap_iff_of_surjective _ hF).mp this
  refine ⟨subsingleton_of_forall_eq 0 fun x ↦ ?_⟩
  obtain ⟨⟨x, hx⟩, rfl⟩ := Ideal.toCotangent_surjective _ x
  obtain ⟨x, rfl⟩ := Ideal.mem_span_singleton.mp (he'.le hx)
  refine (Ideal.toCotangent_eq_zero _ _).mpr ?_
  rw [pow_two, Subtype.coe_mk, ← he, mul_assoc]
  exact Ideal.mul_mem_mul (he'.ge (Ideal.mem_span_singleton_self e)) hx

Goal state after:
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✝² : Q.IsStableUnderBaseChange
inst✝¹ : P.HasOfPrecompProperty Q
inst✝ : P.RespectsRight Q
A X Y Z : C
fst : A ⟶ X
snd : A ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
hf : Q f
hfst : P fst
⊢ P (snd ≫ g)

Tactic:
← h.1.1

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✝² : Q.IsStableUnderBaseChange
inst✝¹ : P.HasOfPrecompProperty Q
inst✝ : P.RespectsRight Q
A X Y Z : C
fst : A ⟶ X
snd : A ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
hf : Q f
hfst : P fst
⊢ P (fst ≫ f)
Module: Mathlib.RingTheory.RingHom.Injective

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

Tactic:
intro R S _ _ e

Goal state after:
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : 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 W : MorphismProperty C
Z✝ X✝ Y✝ A✝ : C
f✝ : Z✝ ⟶ X✝
g✝ : Z✝ ⟶ Y✝
inl✝ : X✝ ⟶ A✝
inr✝ : Y✝ ⟶ A✝
inst✝² : Q.IsStableUnderCobaseChange
inst✝¹ : P.HasOfPostcompProperty Q
inst✝ : P.RespectsLeft Q
X Y Z A : C
f : X ⟶ Y
g : X ⟶ Z
inl : Y ⟶ A
inr : Z ⟶ A
h : IsPushout f g inl inr
hf : Q f
hinl : P inl
⊢ P (g ≫ inr)

Tactic:
← h.1.1

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
P Q W : MorphismProperty C
Z✝ X✝ Y✝ A✝ : C
f✝ : Z✝ ⟶ X✝
g✝ : Z✝ ⟶ Y✝
inl✝ : X✝ ⟶ A✝
inr✝ : Y✝ ⟶ A✝
inst✝² : Q.IsStableUnderCobaseChange
inst✝¹ : P.HasOfPostcompProperty Q
inst✝ : P.RespectsLeft Q
X Y Z A : C
f : X ⟶ Y
g : X ⟶ Z
inl : Y ⟶ A
inr : Z ⟶ A
h : IsPushout f g inl inr
hf : Q f
hinl : P inl
⊢ P (f ≫ inl)
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent

Goal state before:
pp: case H.inr
R S : CommRingCat
Y : Scheme
φ : R ⟶ S
g : Y ⟶ Spec R
h : (@Surjective ⊓ @Flat) (Spec.map φ)
hfst : IsIso (pullback.fst (Spec.map φ) g)
this✝ : IsAffine Y
this :
  ∀ {Y : Scheme} (g : Y ⟶ Spec R),
    IsIso (pullback.fst (Spec.map φ) g) → IsAffine Y → (∃ T, Y = Spec T) → isomorphisms Scheme g
hY : ¬∃ T, Y = Spec T
⊢ isomorphisms Scheme (Y.isoSpec.inv ≫ g)

Tactic:
have heq : pullback.fst (Spec.map φ) (Y.isoSpec.inv ≫ g) =
      pullback.map _ _ _ _ (𝟙 _) (Y.isoSpec.inv) (𝟙 _) (by simp) (by simp) ≫
        pullback.fst (Spec.map φ) g := (pullback.lift_fst _ _ _).symm

Goal state after:
case H.inr
R S : CommRingCat
Y : Scheme
φ : R ⟶ S
g : Y ⟶ Spec R
h : (@Surjective ⊓ @Flat) (Spec.map φ)
hfst : IsIso (pullback.fst (Spec.map φ) g)
this✝ : IsAffine Y
this :
  ∀ {Y : Scheme} (g : Y ⟶ Spec R),
    IsIso (pullback.fst (Spec.map φ) g) → IsAffine Y → (∃ T, Y = Spec T) → isomorphisms Scheme g
hY : ¬∃ T, Y = Spec T
heq :
  pullback.fst (Spec.map φ) (Y.isoSpec.inv ≫ g) =
    pullback.map (Spec.map φ) (Y.isoSpec.inv ≫ g) (Spec.map φ) g (𝟙 (Spec S)) Y.isoSpec.inv (𝟙 (Spec R)) ⋯ ⋯ ≫
      pullback.fst (Spec.map φ) g
⊢ isomorphisms Scheme (Y.isoSpec.inv ≫ g)
Module: Mathlib.RingTheory.Algebraic.StronglyTranscendental

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsReduced S
x : S
hx : IsStronglyTranscendental R x
q : Ideal S
hq : q ∈ minimalPrimes S
u : S
p : R[X]
e : (aeval x) p * u ∈ q
this✝¹ : q.IsPrime
this✝ : Ring.KrullDimLE 0 (Localization.AtPrime q)
this : Field (Localization.AtPrime q) := ⋯.toField
m : S
hmq : m ∈ q.primeCompl
hm : ↑⟨m, hmq⟩ * ((aeval x) p * u) = 0
i : ℕ
⊢ (aeval x) p * (u * m) = 0

Tactic:
by linear_combination hm

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

Goal state before:
pp: K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
⊢ Function.Injective ⇑C

Tactic:
← algebraMap_comp_C,

Goal state after:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
⊢ Function.Injective ⇑((algebraMap K[X] K⟮X⟯).comp Polynomial.C)
Module: Mathlib.FieldTheory.RatFunc.AsPolynomial

Goal state before:
pp: K✝ : Type u
K : Type u_1
inst✝ : Field K
⊢ Ideal.span {X} ≠ ⊥

Tactic:
rw [ne_eq, Ideal.span_singleton_eq_bot]; exact Polynomial.X_ne_zero

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
Γ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
hv : IsTrivialOn K v
hlt : 1 < v RatFunc.X
p : K[X]
hp : p ≠ 0
⊢ v ↑p = v RatFunc.X ^ p.natDegree

Tactic:
convert! valuation_aeval_eq_valuation_X_pow_natDegree_of_one_lt_valuation_X .X hlt hp

Goal state after:
K : Type u_1
inst✝¹ : Field K
Γ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
hv : IsTrivialOn K v
hlt : 1 < v RatFunc.X
p : K[X]
hp : p ≠ 0
⊢ coePolynomial = ⇑(aeval RatFunc.X)
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite

Goal state before:
pp: case inr
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
hf : ∀ (x : ↥(Spec R)), LocallyQuasiFinite (Hom.fiberToSpecResidueField f x)
this :
  ∀ {X : Scheme} (R : CommRingCat) (f : X ⟶ Spec R),
    (∀ (x : ↥(Spec R)), LocallyQuasiFinite (Hom.fiberToSpecResidueField f x)) →
      (∃ S, X = Spec S) → id (LocallyQuasiFinite f)
hX : ¬∃ S, X = Spec S
⊢ id (LocallyQuasiFinite f)

Tactic:
refine (IsZariskiLocalAtSource.iff_of_openCover X.affineCover).mpr fun i ↦
      this _ _ (fun x ↦ ?_) ⟨_, rfl⟩
    have (x : _) : IsLocallyArtinian (f.fiber x) :=
      .of_locallyQuasiFinite (f.fiberToSpecResidueField x)
    let g : (X.affineCover.f i ≫ f).fiber x ⟶ f.fiber x :=
      pullback.map _ _ _ _ (X.affineCover.f i) (𝟙 _) (𝟙 _) (by simp) (by simp)
    have : IsClosedImmersion g := .of_isPreimmersion _ (isClosed_discrete _)
    convert (inferInstance : LocallyQuasiFinite <| g ≫ f.fiberToSpecResidueField _)
    simp [g, Hom.fiberToSpecResidueField]

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

Goal state before:
pp: K : Type u
inst✝¹ : CommRing K
R : Type u_1
inst✝ : SMul R (FractionRing K[X])
c : R
p : K⟮X⟯
⊢ (c • p).toFractionRing = c • p.toFractionRing

Tactic:
cases p

Goal state after:
case ofFractionRing
K : Type u
inst✝¹ : CommRing K
R : Type u_1
inst✝ : SMul R (FractionRing K[X])
c : R
toFractionRing✝ : FractionRing K[X]
⊢ (c • { toFractionRing := toFractionRing✝ }).toFractionRing = c • { toFractionRing := toFractionRing✝ }.toFractionRing
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝ : CommRing K
⊢ ∀ (x : K⟮X⟯), 0 • x = 0

Tactic:
smul_tac

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

Goal state before:
pp: K : Type u
inst✝ : CommRing K
x✝ : ℕ
⊢ ∀ (x : K⟮X⟯), (x✝ + 1) • x = x✝ • x + x

Tactic:
smul_tac

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

Goal state before:
pp: K : Type u
inst✝ : CommRing K
⊢ ∀ (a : K⟮X⟯), 0 • a = 0

Tactic:
smul_tac

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

Goal state before:
pp: K : Type u
inst✝ : CommRing K
x✝ : ℕ
⊢ ∀ (a : K⟮X⟯), ↑x✝.succ • a = ↑x✝ • a + a

Tactic:
smul_tac

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

Goal state before:
pp: K : Type u
inst✝ : CommRing K
x✝ : ℕ
⊢ ∀ (a : K⟮X⟯), Int.negSucc x✝ • a = -(↑x✝.succ • a)

Tactic:
smul_tac

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

Goal state before:
pp: case inr
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝ : LocallyOfFiniteType f
H : ∀ (x : ↥(Spec R)), IsDiscrete (⇑f ⁻¹' {x})
this :
  ∀ {X : Scheme} (R : CommRingCat) {f : X ⟶ Spec R} [LocallyOfFiniteType f],
    (∀ (x : ↥(Spec R)), IsDiscrete (⇑f ⁻¹' {x})) → (∃ S, X = Spec S) → id (LocallyQuasiFinite f)
hX : ¬∃ S, X = Spec S
⊢ id (LocallyQuasiFinite f)

Tactic:
exact (IsZariskiLocalAtSource.iff_of_openCover X.affineCover).mpr fun i ↦
      this _ (fun x ↦ (H x).preimage (X.affineCover.f _).continuous.continuousOn
      (X.affineCover.f _).isOpenEmbedding.injective) ⟨_, rfl⟩

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

Goal state before:
pp: X : Scheme
F : X.AffineZariskiSiteᵒᵖ ⥤ CommRingCat
α : (toOpensFunctor X).op ⋙ X.presheaf ⟶ F
H : NatTrans.Coequifibered α
⊢ ∀ ⦃U V : X.AffineZariskiSite⦄ (f : U ⟶ V), IsOpenImmersion ((F.rightOp ⋙ Scheme.Spec).map f)

Tactic:
by
  exact fun U V ↦ (relativeGluingData H).instIsOpenImmersionMapI₀Functor

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

Goal state before:
pp: K : Type u
inst✝⁵ : CommRing K
G₀ : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
F : Type u_5
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : Field L
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : FunLike F R[X] S[X]
φ : R[X] →+* L
hφ : R[X]⁰ ≤ Submonoid.comap φ L⁰
x y : R⟮X⟯
⊢ (↑(liftMonoidWithZeroHom φ.toMonoidWithZeroHom hφ)).toFun (x + y) =
    (↑(liftMonoidWithZeroHom φ.toMonoidWithZeroHom hφ)).toFun x +
      (↑(liftMonoidWithZeroHom φ.toMonoidWithZeroHom hφ)).toFun y

Tactic:
by
      simp only [ZeroHom.toFun_eq_coe, MonoidWithZeroHom.toZeroHom_coe]
      cases subsingleton_or_nontrivial R
      · rw [Subsingleton.elim (x + y) y, Subsingleton.elim x 0, map_zero, zero_add]
      obtain ⟨x⟩ := x
      obtain ⟨y⟩ := y
      cases x using Localization.induction_on with | _ pq
      cases y using Localization.induction_on with | _ p'q'
      obtain ⟨p, q⟩ := pq
      obtain ⟨p', q'⟩ := p'q'
      rw [← ofFractionRing_add, Localization.add_mk]
      simp only [RingHom.toMonoidWithZeroHom_eq_coe,
        liftMonoidWithZeroHom_apply_ofFractionRing_mk]
      rw [div_add_div, div_eq_div_iff]
      · rw [mul_comm _ p, mul_comm _ p', mul_comm _ (φ p'), add_comm]
        simp only [map_add, map_mul, Submonoid.coe_mul]
      all_goals
        try simp only [← map_mul, ← Submonoid.coe_mul]
        exact nonZeroDivisors.ne_zero (hφ (SetLike.coe_mem _))

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

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
inst✝¹ : Algebra R S
inst✝ : Algebra R T
P✝ : StandardEtalePair R
P : StandardEtalePresentation R S
⊢ Function.Injective ⇑↑(P.lift P.x ⋯)

Tactic:
by exact P.lift_bijective.injective

Goal state after:
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
φ : R[X] →ₐ[R] S
t : S
p : R[X]
ht : φ.IsIntegralElem t
hpm : p.Monic
hp : φ p * t ∈ φ.range
⊢ ∃ q, IsIntegral R (t - φ q)

Tactic:
obtain ⟨r, hr : φ r = _⟩ := hp

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
φ : R[X] →ₐ[R] S
t : S
p : R[X]
ht : φ.IsIntegralElem t
hpm : p.Monic
r : R[X]
hr : φ r = φ p * t
⊢ ∃ q, IsIntegral R (t - φ q)
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
φ : R[X] →ₐ[R] S
t : S
p : R[X]
ht : φ.IsIntegralElem t
hp : φ p * t ∈ φ.range
a : R := p.leadingCoeff
R' : Type u_1 := Localization.Away a
S' : Type u_2 := Localization.Away ((algebraMap R S) a)
this✝ : Algebra R' S' := (Localization.awayMap (algebraMap R S) a).toAlgebra
this : IsScalarTower R R' S'
ha : IsUnit ((algebraMap R R') a)
H : (aeval ((algebraMap S S') (φ X))).comp (mapRingHom (algebraMap R R')) = (algebraMap S S').comp ↑φ
⊢ (aeval ((algebraMap S S') (φ X))) (C ↑ha.unit⁻¹ * map (algebraMap R R') p) * (algebraMap S S') t ∈
    (aeval ((algebraMap S S') (φ X))).range

Tactic:
obtain ⟨r, hr : φ r = _⟩ := hp

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
φ : R[X] →ₐ[R] S
t : S
p : R[X]
ht : φ.IsIntegralElem t
a : R := p.leadingCoeff
R' : Type u_1 := Localization.Away a
S' : Type u_2 := Localization.Away ((algebraMap R S) a)
this✝ : Algebra R' S' := (Localization.awayMap (algebraMap R S) a).toAlgebra
this : IsScalarTower R R' S'
ha : IsUnit ((algebraMap R R') a)
H : (aeval ((algebraMap S S') (φ X))).comp (mapRingHom (algebraMap R R')) = (algebraMap S S').comp ↑φ
r : R[X]
hr : φ r = φ p * t
⊢ (aeval ((algebraMap S S') (φ X))) (C ↑ha.unit⁻¹ * map (algebraMap R R') p) * (algebraMap S S') t ∈
    (aeval ((algebraMap S S') (φ X))).range
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝²⁸ : CommRing R
inst✝²⁷ : CommRing S
inst✝²⁶ : Algebra R S
K : Type u_4
L : Type u_5
inst✝²⁵ : Field K
inst✝²⁴ : Field L
inst✝²³ : Algebra R K
inst✝²² : Algebra R L
inst✝²¹ : Algebra S L
inst✝²⁰ : Algebra K L
inst✝¹⁹ : IsScalarTower R K L
inst✝¹⁸ : IsScalarTower R S L
inst✝¹⁷ : IsFractionRing R K
inst✝¹⁶ : IsFractionRing S L
R' : Type u_6
S' : Type u_7
inst✝¹⁵ : CommRing R'
inst✝¹⁴ : CommRing S'
inst✝¹³ : Algebra R R'
inst✝¹² : Algebra R' S'
inst✝¹¹ : Algebra R S'
inst✝¹⁰ : Algebra S' L
inst✝⁹ : Algebra R' L
inst✝⁸ : IsScalarTower R' S' L
inst✝⁷ : Algebra R' K
inst✝⁶ : IsScalarTower R' K L
inst✝⁵ : IsScalarTower R R' S'
inst✝⁴ : FaithfulSMul S' L
inst✝³ : IsIntegralClosure R' R K
inst✝² : IsScalarTower R R' K
f : S →ₐ[R] S'
hf₁ : Function.Surjective ⇑(TensorProduct.lift (ofId R' S') f ⋯)
hf₂ : (algebraMap S' L).comp f.toRingHom = algebraMap S L
x : S
hx' : (aeval x).Finite
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : WeaklyQuasiFiniteAt R P
hx : IsStronglyTranscendental R x
this✝⁵ : IsDomain S'
this✝⁴ : IsDomain R
this✝³ : Algebra.IsIntegral R R'
this✝² : FaithfulSMul R' K
this✝¹ : FaithfulSMul R R'
this✝ : FaithfulSMul R' L
this : FaithfulSMul R' S'
⊢ False

Tactic:
have : IsIntegrallyClosedIn R' K := .of_isIntegralClosure R

Goal state after:
R : Type u_1
S : Type u_2
inst✝²⁸ : CommRing R
inst✝²⁷ : CommRing S
inst✝²⁶ : Algebra R S
K : Type u_4
L : Type u_5
inst✝²⁵ : Field K
inst✝²⁴ : Field L
inst✝²³ : Algebra R K
inst✝²² : Algebra R L
inst✝²¹ : Algebra S L
inst✝²⁰ : Algebra K L
inst✝¹⁹ : IsScalarTower R K L
inst✝¹⁸ : IsScalarTower R S L
inst✝¹⁷ : IsFractionRing R K
inst✝¹⁶ : IsFractionRing S L
R' : Type u_6
S' : Type u_7
inst✝¹⁵ : CommRing R'
inst✝¹⁴ : CommRing S'
inst✝¹³ : Algebra R R'
inst✝¹² : Algebra R' S'
inst✝¹¹ : Algebra R S'
inst✝¹⁰ : Algebra S' L
inst✝⁹ : Algebra R' L
inst✝⁸ : IsScalarTower R' S' L
inst✝⁷ : Algebra R' K
inst✝⁶ : IsScalarTower R' K L
inst✝⁵ : IsScalarTower R R' S'
inst✝⁴ : FaithfulSMul S' L
inst✝³ : IsIntegralClosure R' R K
inst✝² : IsScalarTower R R' K
f : S →ₐ[R] S'
hf₁ : Function.Surjective ⇑(TensorProduct.lift (ofId R' S') f ⋯)
hf₂ : (algebraMap S' L).comp f.toRingHom = algebraMap S L
x : S
hx' : (aeval x).Finite
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : WeaklyQuasiFiniteAt R P
hx : IsStronglyTranscendental R x
this✝⁶ : IsDomain S'
this✝⁵ : IsDomain R
this✝⁴ : Algebra.IsIntegral R R'
this✝³ : FaithfulSMul R' K
this✝² : FaithfulSMul R R'
this✝¹ : FaithfulSMul R' L
this✝ : FaithfulSMul R' S'
this : IsIntegrallyClosedIn R' K
⊢ False
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f g : R[X]
m : ℕ
hf : f.natDegree ≤ m
n : ℕ
⊢ Fin ((m + 1).add n).succ

Tactic:
by exact ((Fin.last m).castAdd (n + 1))

Goal state after:
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
U : Y.Opens
hU : IsAffineOpen U
⊢ app (fromNormalization f) U =
    CommRingCat.ofHom (algebraMap ↑(Y.presheaf.1 (Opposite.op U)) ↥(integralClosure ↑Γ(Y, U) ↑Γ(X, f ⁻¹ᵁ U))) ≫
      (normalizationObjIso f hU).inv

Tactic:
by
  let := (f.app U).hom.toAlgebra
  have : IsIso (((normalizationOpenCover f).f ⟨U, hU⟩).app (f.fromNormalization ⁻¹ᵁ U)) :=
    Scheme.Hom.isIso_app _ _ (by simp [← fromNormalization_preimage])
  have H : ⊤ = ((normalizationOpenCover f).f ⟨U, hU⟩ ≫ fromNormalization f) ⁻¹ᵁ U := by
    rw [f.ι_fromNormalization]; simp
  rw [← cancel_mono (((normalizationOpenCover f).f ⟨U, hU⟩).app (f.fromNormalization ⁻¹ᵁ U)),
    ← Scheme.Hom.comp_app, Scheme.Hom.congr_app (f.ι_fromNormalization ⟨U, hU⟩) U,
    ← cancel_mono (((normalizationOpenCover f).X ⟨U, hU⟩).presheaf.map (eqToHom H).op)]
  dsimp [normalizationObjIso]
  rw [IsAffineOpen.fromSpec_app_self]
  simp only [app_eq_appLE, Category.assoc, map_appLE, appLE_map]
  simp [Scheme.Hom.appLE, ← ΓSpecIso_inv_naturality]
  rfl

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n k : ℕ
h : ¬k < n
x : Fin n
x✝ : x ∈ Finset.univ
⊢ ¬k = ↑x

Tactic:
by cases x; lia

Goal state after: