mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Extension.Cotangent.Free

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
κ : Type u_5
P : Generators R S ι
u : σ → ι
hu : Function.Injective u
v : κ → ι
huv : IsCompl (Set.range v) (Set.range u)
b : Module.Basis κ S Ω[S⁄R]
hb : ∀ (k : κ), b k = (D R S) (P.val (v k))
inst✝ : Subsingleton (H1Cotangent R S)
⊢ Disjoint P.toExtension.toKaehler.ker (Submodule.span S (Set.range fun x ↦ P.cotangentSpaceBasis (v x)))

Tactic:
apply disjoint_ker_toKaehler_of_linearIndependent

Goal state after:
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
κ : Type u_5
P : Generators R S ι
u : σ → ι
hu : Function.Injective u
v : κ → ι
huv : IsCompl (Set.range v) (Set.range u)
b : Module.Basis κ S Ω[S⁄R]
hb : ∀ (k : κ), b k = (D R S) (P.val (v k))
inst✝ : Subsingleton (H1Cotangent R S)
⊢ LinearIndependent S fun k ↦ (D R S) (P.val (v k))
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 : R →+* S
e : S ≃+* T
hf : IsStandardSmoothOfRelativeDimension n f
⊢ IsStandardSmoothOfRelativeDimension n (e.toRingHom.comp f)

Tactic:
by
    rw [← zero_add n]
    exact (IsStandardSmoothOfRelativeDimension.equiv e).comp hf

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

Goal state before:
pp: n : ℕ
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Algebra.IsStandardSmoothOfRelativeDimension n R S
this✝¹ : (α : Type) → [_root_.Finite α] → Fintype α := Fintype.ofFinite
ι σ : Type
w✝¹ : _root_.Finite σ
w✝ : _root_.Finite ι
P : Algebra.SubmersivePresentation R S ι σ
e✝ : P.dimension = n
e₀ : σ ⊕ Fin n ≃ ι :=
  ((Equiv.ofInjective P.map ⋯).sumCongr (Finite.equivFinOfCardEq ⋯).symm).trans (Equiv.Set.sumCompl (Set.range P.map))
e : MvPolynomial σ (MvPolynomial (Fin n) R) ≃ₐ[R] P.Ring :=
  (MvPolynomial.sumAlgEquiv R σ (Fin n)).symm.trans (MvPolynomial.renameEquiv R e₀)
φ : MvPolynomial (Fin n) R →ₐ[R] P.Ring :=
  (↑e).comp (IsScalarTower.toAlgHom R (MvPolynomial (Fin n) R) (MvPolynomial σ (MvPolynomial (Fin n) R)))
algInst✝¹ : Algebra (MvPolynomial (Fin n) R) P.Ring := φ.toAlgebra
algInst✝ : Algebra (MvPolynomial (Fin n) R) S := ((algebraMap P.Ring S).comp φ.toRingHom).toAlgebra
scalarTowerInst✝ : IsScalarTower (MvPolynomial (Fin n) R) P.Ring S :=
  IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap (MvPolynomial (Fin n) R) S))
this✝ : IsScalarTower R (MvPolynomial (Fin n) R) P.Ring
this : IsScalarTower R (MvPolynomial (Fin n) R) S
H :
  (MvPolynomial.aeval fun x ↦ (algebraMap P.Ring S) (e (MvPolynomial.X x))).toRingHom =
    (algebraMap P.Ring S).comp e.toRingEquiv.toRingHom
⊢ Function.Surjective ⇑(MvPolynomial.aeval fun x ↦ (algebraMap P.Ring S) (e (MvPolynomial.X x)))

Tactic:
convert! P.algebraMap_surjective.comp e.surjective

Goal state after:
n : ℕ
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Algebra.IsStandardSmoothOfRelativeDimension n R S
this✝¹ : (α : Type) → [_root_.Finite α] → Fintype α := Fintype.ofFinite
ι σ : Type
w✝¹ : _root_.Finite σ
w✝ : _root_.Finite ι
P : Algebra.SubmersivePresentation R S ι σ
e✝ : P.dimension = n
e₀ : σ ⊕ Fin n ≃ ι :=
  ((Equiv.ofInjective P.map ⋯).sumCongr (Finite.equivFinOfCardEq ⋯).symm).trans (Equiv.Set.sumCompl (Set.range P.map))
e : MvPolynomial σ (MvPolynomial (Fin n) R) ≃ₐ[R] P.Ring :=
  (MvPolynomial.sumAlgEquiv R σ (Fin n)).symm.trans (MvPolynomial.renameEquiv R e₀)
φ : MvPolynomial (Fin n) R →ₐ[R] P.Ring :=
  (↑e).comp (IsScalarTower.toAlgHom R (MvPolynomial (Fin n) R) (MvPolynomial σ (MvPolynomial (Fin n) R)))
algInst✝¹ : Algebra (MvPolynomial (Fin n) R) P.Ring := φ.toAlgebra
algInst✝ : Algebra (MvPolynomial (Fin n) R) S := ((algebraMap P.Ring S).comp φ.toRingHom).toAlgebra
scalarTowerInst✝ : IsScalarTower (MvPolynomial (Fin n) R) P.Ring S :=
  IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap (MvPolynomial (Fin n) R) S))
this✝ : IsScalarTower R (MvPolynomial (Fin n) R) P.Ring
this : IsScalarTower R (MvPolynomial (Fin n) R) S
H :
  (MvPolynomial.aeval fun x ↦ (algebraMap P.Ring S) (e (MvPolynomial.X x))).toRingHom =
    (algebraMap P.Ring S).comp e.toRingEquiv.toRingHom
⊢ ⇑(MvPolynomial.aeval fun x ↦ (algebraMap P.Ring S) (e (MvPolynomial.X x))) = ⇑(algebraMap P.Ring S) ∘ ⇑e
Module: Mathlib.RingTheory.Extension.Cotangent.Basis

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
inst✝ : Nontrivial S
r : Unit ⊕ σ
⊢ D.basis r = Extension.Cotangent.mk ⟨D.pres.relation r, ⋯⟩

Tactic:
by
  obtain (r | r) := r
  · rw [basis_inl, cotangentEquivProd_symm_apply]
    exact cotangentCompLocalizationAwayEquiv_symm_inr _ _ _
  · rw [basis_inr, cotangentEquivProd_symm_apply, cotangentCompLocalizationAwayEquiv_symm_inl,
      basisLeft, Module.Basis.map_apply, tensorCotangentEquiv_symm_apply,
      LinearMap.liftBaseChange_tmul, one_smul, Extension.Cotangent.map_mk]
    simp only [Extension.Hom.toAlgHom_apply, Hom.toExtensionHom_toRingHom, AlgHom.toRingHom_eq_coe]
    congr! 2 with x
    simp [pres, Presentation.comp_relation_inr, kerGen, presLeft, Generators.toComp_toAlgHom]
    rfl

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FinitePresentation R S
α : Type u_4
P : Generators R S α
inst✝ : Finite α
σ : Type u_5
b₀ : Module.Basis σ S P.toExtension.Cotangent
h✝ : Nontrivial S
f : P.toExtension.Cotangent → ↥P.toExtension.ker
hf : ∀ (b : P.toExtension.Cotangent), Extension.Cotangent.mk (f b) = b
v : σ → ↥P.ker := fun i ↦ f (b₀ i)
J : Ideal P.Ring := Ideal.span (Set.range (Subtype.val ∘ v))
hJfg : P.ker.FG
hJ : J ≤ P.ker
⊢ J ≤ (Submodule.subtype P.ker).range

Tactic:
by simpa using hJ

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

Goal state before:
pp: R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Locally (fun {R S} [CommRing R] [CommRing S] ↦ IsStandardSmooth) f
⊢ Locally (fun {R S} [CommRing R] [CommRing S] ↦ Smooth) f

Tactic:
exact locally_of_locally (fun hf ↦ hf.smooth) hf

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

Goal state before:
pp: X Y Z S : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ MorphismProperty.RespectsIso @IsProper

Tactic:
by
  rw [isProper_eq]
  infer_instance

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

Goal state before:
pp: X Y Z S : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ MorphismProperty.IsStableUnderComposition @IsProper

Tactic:
by
  rw [isProper_eq]
  infer_instance

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

Goal state before:
pp: X Y Z S : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ MorphismProperty.IsMultiplicative @IsProper

Tactic:
by
  rw [isProper_eq]
  infer_instance

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

Goal state before:
pp: X Y Z S : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ MorphismProperty.IsStableUnderBaseChange @IsProper

Tactic:
by
  rw [isProper_eq]
  infer_instance

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

Goal state before:
pp: X Y Z S : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ IsZariskiLocalAtTarget @IsProper

Tactic:
by
  rw [isProper_eq]
  infer_instance

Goal state after:
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 : 0 = coeff σ F
⊢ False

Tactic:
eq_comm,

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 : coeff σ F = 0
⊢ False
Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth

Goal state before:
pp: X✝ : Scheme
K : Type u
inst✝³ : Field K
inst✝² : PerfectField K
X : Scheme
inst✝¹ : IsReduced X
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : LocallyOfFinitePresentation f
H : CompactSpace ↥X
this✝¹ : IsNoetherian X
x : ↥X
U : X.Opens := { carrier := (⋃₀ (irreducibleComponents ↥X \ {irreducibleComponent x}))ᶜ, is_open' := ⋯ }
hU : closure ↑U = irreducibleComponent x
this✝ : IsIntegral ↑U
this : U.ι (genericPoint ↥↑U) ∈ smoothLocus f
⊢ x ∈ closure (⇑U.ι '' Set.univ)

Tactic:
rw [Set.image_univ, U.range_ι, hU]; exact mem_irreducibleComponent

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

Goal state before:
pp: X✝ : Scheme
K : Type u
inst✝³ : Field K
inst✝² : PerfectField K
X : Scheme
inst✝¹ : IsReduced X
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : LocallyOfFinitePresentation f
H : CompactSpace ↥X
this✝¹ : IsNoetherian X
x : ↥X
U : X.Opens := { carrier := (⋃₀ (irreducibleComponents ↥X \ {irreducibleComponent x}))ᶜ, is_open' := ⋯ }
hU : closure ↑U = irreducibleComponent x
this✝ : IsIntegral ↑U
this : U.ι (genericPoint ↥↑U) ∈ smoothLocus f
⊢ x ∈ closure (⇑U.ι '' Set.univ)

Tactic:
by rw [Set.image_univ, U.range_ι, hU]; exact mem_irreducibleComponent

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

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

Tactic:
wlog hX : ∃ S, X = Spec S generalizing X

Goal state after:
case inr
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝ : IsOpenImmersion (pullback.diagonal f)
this : ∀ {X : Scheme} (f : X ⟶ Spec R) [IsOpenImmersion (pullback.diagonal f)], (∃ S, X = Spec S) → FormallyUnramified f
hX : ¬∃ S, X = Spec S
⊢ FormallyUnramified f

X✝ Y : Scheme
f✝ : X✝ ⟶ Y
R : CommRingCat
X : Scheme
f : X ⟶ Spec R
inst✝ : IsOpenImmersion (pullback.diagonal f)
hX : ∃ S, X = Spec S
⊢ FormallyUnramified 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
n : ι
inst✝ : ExpChar k p
ha' : IsTranscendenceBasis k fun i ↦ a ↑i
S : Set (MvPolynomial ι k) := {F | F ≠ 0 ∧ (aeval a) F = 0}
F : MvPolynomial ι k
hFmin : ∀ (G : MvPolynomial ι k), G ≠ 0 → (aeval a) G = 0 → F.totalDegree ≤ G.totalDegree
hF₀ : F ≠ 0
hFa : (aeval a) F = 0
hFirr : Irreducible F
i : ι
σ : ι →₀ ℕ
hσ : σ ∈ F.support
hi : ¬p ∣ σ i
hσi : σ i ≠ 0
alg : IsAlgebraic (↥(Algebra.adjoin k (a '' {i}ᶜ))) (a i)
Hi : IsTranscendenceBasis k fun x ↦ a ↑x
k' : IntermediateField k K := adjoin k (a '' {i}ᶜ)
hF₁irr : Irreducible (F.toPolynomialAdjoinImageCompl a i)
this✝ : UniqueFactorizationMonoid ↥(Algebra.adjoin k (a '' {i}ᶜ))
hF₂irr :
  Irreducible (Polynomial.map (algebraMap ↥(Algebra.adjoin k (a '' {i}ᶜ)) ↥k') (F.toPolynomialAdjoinImageCompl a i))
Hsep : ¬IsSeparable (↥(adjoin k (a '' {i}ᶜ))) (a i)
this : CharP (↥k') p
g : Polynomial ↥k'
hg : Irreducible g
eq :
  0 = (Polynomial.map (algebraMap ↥(Algebra.adjoin k (a '' {i}ᶜ)) ↥k') (F.toPolynomialAdjoinImageCompl a i)).coeff (σ i)
⊢ (F.toPolynomialAdjoinImageCompl a i).coeff (σ i) = 0

Tactic:
eq_comm,

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
n : ι
inst✝ : ExpChar k p
ha' : IsTranscendenceBasis k fun i ↦ a ↑i
S : Set (MvPolynomial ι k) := {F | F ≠ 0 ∧ (aeval a) F = 0}
F : MvPolynomial ι k
hFmin : ∀ (G : MvPolynomial ι k), G ≠ 0 → (aeval a) G = 0 → F.totalDegree ≤ G.totalDegree
hF₀ : F ≠ 0
hFa : (aeval a) F = 0
hFirr : Irreducible F
i : ι
σ : ι →₀ ℕ
hσ : σ ∈ F.support
hi : ¬p ∣ σ i
hσi : σ i ≠ 0
alg : IsAlgebraic (↥(Algebra.adjoin k (a '' {i}ᶜ))) (a i)
Hi : IsTranscendenceBasis k fun x ↦ a ↑x
k' : IntermediateField k K := adjoin k (a '' {i}ᶜ)
hF₁irr : Irreducible (F.toPolynomialAdjoinImageCompl a i)
this✝ : UniqueFactorizationMonoid ↥(Algebra.adjoin k (a '' {i}ᶜ))
hF₂irr :
  Irreducible (Polynomial.map (algebraMap ↥(Algebra.adjoin k (a '' {i}ᶜ)) ↥k') (F.toPolynomialAdjoinImageCompl a i))
Hsep : ¬IsSeparable (↥(adjoin k (a '' {i}ᶜ))) (a i)
this : CharP (↥k') p
g : Polynomial ↥k'
hg : Irreducible g
eq :
  (Polynomial.map (algebraMap ↥(Algebra.adjoin k (a '' {i}ᶜ)) ↥k') (F.toPolynomialAdjoinImageCompl a i)).coeff (σ i) = 0
⊢ (F.toPolynomialAdjoinImageCompl a i).coeff (σ i) = 0
Module: Mathlib.FieldTheory.SeparablyGenerated

Goal state before:
pp: case refine_1
k : Type u_1
K : Type u_2
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
inst✝¹ : ExpChar k p
inst✝ : Algebra.EssFiniteType k K
s : Finset K
hs : (fun t ↦ IsTranscendenceBasis k Subtype.val) ↑s
Hs :
  ∀ ⦃j : Set K⦄,
    (fun t ↦ IsTranscendenceBasis k Subtype.val) j →
      (fun t ↦ restrictScalars k (separableClosure (↥(adjoin k t)) K)) ↑s ≤
          (fun t ↦ restrictScalars k (separableClosure (↥(adjoin k t)) K)) j →
        (fun t ↦ restrictScalars k (separableClosure (↥(adjoin k t)) K)) j ≤
          (fun t ↦ restrictScalars k (separableClosure (↥(adjoin k t)) K)) ↑s
n : K
hn : ¬IsSeparable (↥(adjoin k ↑s)) n
hns : n ∉ s
i : K
hi₁ : IsTranscendenceBasis k fun j ↦ id ↑j
hi₂ : IsSeparable (↥(adjoin k (insert n ↑s \ {i}))) (id i)
⊢ (fun t ↦ restrictScalars k (separableClosure (↥(adjoin k t)) K)) ↑s ≤
    (fun t ↦ restrictScalars k (separableClosure (↥(adjoin k t)) K)) (insert n ↑s \ {i})

Tactic:
separableClosure_le_separableClosure_iff,

Goal state after:
case refine_1
k : Type u_1
K : Type u_2
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
inst✝¹ : ExpChar k p
inst✝ : Algebra.EssFiniteType k K
s : Finset K
hs : (fun t ↦ IsTranscendenceBasis k Subtype.val) ↑s
Hs :
  ∀ ⦃j : Set K⦄,
    (fun t ↦ IsTranscendenceBasis k Subtype.val) j →
      (fun t ↦ restrictScalars k (separableClosure (↥(adjoin k t)) K)) ↑s ≤
          (fun t ↦ restrictScalars k (separableClosure (↥(adjoin k t)) K)) j →
        (fun t ↦ restrictScalars k (separableClosure (↥(adjoin k t)) K)) j ≤
          (fun t ↦ restrictScalars k (separableClosure (↥(adjoin k t)) K)) ↑s
n : K
hn : ¬IsSeparable (↥(adjoin k ↑s)) n
hns : n ∉ s
i : K
hi₁ : IsTranscendenceBasis k fun j ↦ id ↑j
hi₂ : IsSeparable (↥(adjoin k (insert n ↑s \ {i}))) (id i)
⊢ adjoin k ↑s ≤ restrictScalars k (separableClosure (↥(adjoin k (insert n ↑s \ {i}))) K)
Module: Mathlib.AlgebraicGeometry.Morphisms.Descent

Goal state before:
pp: case a
P P' : MorphismProperty Scheme
inst✝³ : P'.RespectsIso
inst✝² : P'.IsStableUnderComposition
inst✝¹ : P.IsStableUnderBaseChange
H : ∀ {R : CommRingCat} {S X : Scheme} (f : Spec R ⟶ S) (g : X ⟶ S), P' f → P (pullback.fst f g) → P g
X Y Z T : Scheme
inst✝ : IsAffine T
p : T ⟶ X
hp : P' p
f : X ⟶ Z
g : Y ⟶ Z
h : P' f
hf : P (pullback.fst f g)
⊢ P (pullback.fst (T.isoSpec.inv ≫ p) (pullback.fst f g))

Tactic:
exact P.pullback_fst _ _ hf

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

Tactic:
rw [← (isomorphisms Scheme).cancel_left_of_respectsIso Y.isoSpec.inv]
    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
    refine this _ ?_ inferInstance ⟨_, rfl⟩
    change isomorphisms Scheme _
    rwa [heq, (isomorphisms Scheme).cancel_left_of_respectsIso]

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
⊢ p < Ideal.under R Q → ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p

Tactic:
hpQ

Goal state after:
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
⊢ ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p
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)

Goal state after:
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 : Ideal SQ
hP : P.IsPrime
e : Ideal.comap (algebraMap R SQ) P = p
⊢ ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p
Module: Mathlib.RingTheory.IntegralClosure.Algebra.Ideal

Goal state before:
pp: case zero
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Algebra.IsIntegral R S
I : Ideal R
x : S
A : Subalgebra R R[X] := Algebra.adjoin R {x | ∃ r ∈ I, C r * X = x}
this : Algebra R[X] S[X] := algebra R S
⊢ IsIntegral (↥(Algebra.adjoin R {x | ∃ r ∈ I, C r * X = x})) (C 0 * X)

Tactic:
simp [isIntegral_zero]

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.AlmostIntegral

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
H : IsIntegral R s
h : ∃ t ∈ R⁰, t • s ∈ (algebraMap R S).range
⊢ IsAlmostIntegral R s

Tactic:
by
  obtain ⟨b, hb', hb⟩ :
      ∃ b ∈ R⁰, ∀ i < (minpoly R s).natDegree, (b • s ^ i) ∈ (algebraMap R S).range := by
    obtain ⟨t, ht, ht'⟩ := h
    refine ⟨t ^ (minpoly R s).natDegree, pow_mem ht _, fun i hi ↦ ?_⟩
    rw [← Nat.sub_add_cancel hi.le, pow_add, mul_smul, ← smul_pow]
    exact (AlgHom.range (Algebra.ofId _ _)).smul_mem (Subalgebra.pow_mem _ ht' _) _
  refine ⟨b, hb', fun n ↦ ?_⟩
  induction n using Nat.strong_induction_on with | h n IH =>
  obtain hn | hn := lt_or_ge n (minpoly R s).natDegree
  · exact hb _ (by simpa)
  have := minpoly.aeval R s
  rw [Polynomial.aeval_eq_sum_range, Finset.sum_range_succ, add_eq_zero_iff_eq_neg',
    Polynomial.coeff_natDegree, minpoly.monic H, one_smul] at this
  rw [← Nat.sub_add_cancel hn, pow_add, this, mul_neg, smul_neg, Finset.mul_sum, Finset.smul_sum]
  simp_rw [mul_smul_comm, ← pow_add, smul_comm b]
  refine neg_mem (sum_mem fun i hi ↦ (AlgHom.range (Algebra.ofId _ _)).smul_mem (IH _ ?_) _)
  simp only [Finset.mem_range] at hi
  lia

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

Goal state before:
pp: case inl
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
i : ℕ
a✝¹ : Nontrivial R
a✝ : Nontrivial S
hp : IsIntegral R[X] 0
⊢ IsIntegral R (coeff 0 i)

Tactic:
simp [isIntegral_zero]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type w
f : MvPolynomial σ S
H : ∀ (n : σ →₀ ℕ), IsIntegral R (coeff n f)
⊢ IsIntegral (MvPolynomial σ R) (∑ v ∈ f.support, (monomial v) (coeff v f))

Tactic:
simp_rw [monomial_eq]

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type w
f : MvPolynomial σ S
H : ∀ (n : σ →₀ ℕ), IsIntegral R (coeff n f)
⊢ IsIntegral (MvPolynomial σ R) (∑ x ∈ f.support, C (coeff x f) * x.prod fun n e ↦ X n ^ e)
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
inst✝² : WeaklyQuasiFiniteAt R q
inst✝¹ : Algebra (Localization.AtPrime p) (Localization.AtPrime q)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra p q
r : Ideal (S ⧸ Ideal.map (algebraMap R S) (Ideal.under R q)) :=
  Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap R S) (Ideal.under R q))) q
⊢ Module.Finite p.ResidueField q.ResidueField

Tactic:
have : r.LiesOver q :=
    ⟨.trans (by simp [← RingHom.ker_eq_comap_bot, Ideal.map_comap_le])
    (Ideal.comap_map_of_surjective _ Ideal.Quotient.mk_surjective _).symm⟩

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
inst✝² : WeaklyQuasiFiniteAt R q
inst✝¹ : Algebra (Localization.AtPrime p) (Localization.AtPrime q)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra p q
r : Ideal (S ⧸ Ideal.map (algebraMap R S) (Ideal.under R q)) :=
  Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap R S) (Ideal.under R q))) q
this : r.LiesOver q
⊢ Module.Finite p.ResidueField q.ResidueField