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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : FinitePresentation R A
f : A
⊢ ↑(PrimeSpectrum.basicOpen f) ⊆ smoothLocus R A ↔ FormallySmooth R (Localization.Away f)

Tactic:
smoothLocus_eq_compl_support_inter,

Goal state after:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : FinitePresentation R A
f : A
⊢ ↑(PrimeSpectrum.basicOpen f) ⊆ (Module.support A (H1Cotangent R A))ᶜ ∩ Module.freeLocus A Ω[A⁄R] ↔
    FormallySmooth R (Localization.Away f)
Module: Mathlib.RingTheory.Smooth.Locus

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : FinitePresentation R A
x : PrimeSpectrum A
hx : x ∈ smoothLocus R A
f : A
hxf : x ∈ ↑(basicOpen f)
hf : Module.Projective (Localization.Away f) (LocalizedModule.Away f Ω[A⁄R])
Af : Type u_2 := Localization.Away f
this✝³ : FinitePresentation A (Localization.Away f)
this✝² : FinitePresentation R (Localization.Away f)
this✝¹ : LocalizedModule (Submonoid.powers f) Ω[A⁄R] ≃ₗ[A] Ω[Localization.Away f⁄R]
this✝ : LocalizedModule (Submonoid.powers f) Ω[A⁄R] ≃ₗ[Localization.Away f] Ω[Localization.Away f⁄R]
this : Module.Projective (Localization.Away f) Ω[Localization.Away f⁄R]
⊢ IsOpen (smoothLocus R Af)

Tactic:
smoothLocus_eq_compl_support_inter,

Goal state after:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : FinitePresentation R A
x : PrimeSpectrum A
hx : x ∈ smoothLocus R A
f : A
hxf : x ∈ ↑(basicOpen f)
hf : Module.Projective (Localization.Away f) (LocalizedModule.Away f Ω[A⁄R])
Af : Type u_2 := Localization.Away f
this✝³ : FinitePresentation A (Localization.Away f)
this✝² : FinitePresentation R (Localization.Away f)
this✝¹ : LocalizedModule (Submonoid.powers f) Ω[A⁄R] ≃ₗ[A] Ω[Localization.Away f⁄R]
this✝ : LocalizedModule (Submonoid.powers f) Ω[A⁄R] ≃ₗ[Localization.Away f] Ω[Localization.Away f⁄R]
this : Module.Projective (Localization.Away f) Ω[Localization.Away f⁄R]
⊢ IsOpen ((Module.support Af (H1Cotangent R Af))ᶜ ∩ Module.freeLocus Af Ω[Af⁄R])
Module: Mathlib.RingTheory.Etale.Field

Goal state before:
pp: K : Type u_1
A : Type u
inst✝⁹ : Field K
inst✝⁸ : CommRing A
inst✝⁷ : Algebra K A
B : Type u_3
inst✝⁶ : CommRing B
inst✝⁵ : EssFiniteType K A
inst✝⁴ : FormallyEtale K A
inst✝³ : Algebra K B
inst✝² : EssFiniteType K B
inst✝¹ : FormallyEtale K B
inst✝ : IsSepClosed K
f : A →ₐ[K] B
x : A
p : PrimeSpectrum B
heq : ofId K (B ⧸ p.asIdeal) = (Ideal.quotientMapₐ p.asIdeal f ⋯).comp (ofId K (A ⧸ Ideal.comap f p.asIdeal))
h :
  (Ideal.quotientMapₐ p.asIdeal f ⋯) ((Ideal.Quotient.mk (Ideal.comap f p.asIdeal)) x) =
    (Ideal.Quotient.mk p.asIdeal) (f x)
⊢ (AlgEquiv.ofBijective (ofId K (A ⧸ Ideal.comap (↑f) p.asIdeal)) ⋯).symm
      ((Ideal.Quotient.mk (Ideal.comap (↑f) p.asIdeal)) x) =
    (AlgEquiv.ofBijective (ofId K (B ⧸ p.asIdeal)) ⋯).symm ((Ideal.Quotient.mk p.asIdeal) (f x))

Tactic:
apply FaithfulSMul.algebraMap_injective K (B ⧸ p.asIdeal)

Goal state after:
K : Type u_1
A : Type u
inst✝⁹ : Field K
inst✝⁸ : CommRing A
inst✝⁷ : Algebra K A
B : Type u_3
inst✝⁶ : CommRing B
inst✝⁵ : EssFiniteType K A
inst✝⁴ : FormallyEtale K A
inst✝³ : Algebra K B
inst✝² : EssFiniteType K B
inst✝¹ : FormallyEtale K B
inst✝ : IsSepClosed K
f : A →ₐ[K] B
x : A
p : PrimeSpectrum B
heq : ofId K (B ⧸ p.asIdeal) = (Ideal.quotientMapₐ p.asIdeal f ⋯).comp (ofId K (A ⧸ Ideal.comap f p.asIdeal))
h :
  (Ideal.quotientMapₐ p.asIdeal f ⋯) ((Ideal.Quotient.mk (Ideal.comap f p.asIdeal)) x) =
    (Ideal.Quotient.mk p.asIdeal) (f x)
⊢ (algebraMap K (B ⧸ p.asIdeal))
      ((AlgEquiv.ofBijective (ofId K (A ⧸ Ideal.comap (↑f) p.asIdeal)) ⋯).symm
        ((Ideal.Quotient.mk (Ideal.comap (↑f) p.asIdeal)) x)) =
    (algebraMap K (B ⧸ p.asIdeal))
      ((AlgEquiv.ofBijective (ofId K (B ⧸ p.asIdeal)) ⋯).symm ((Ideal.Quotient.mk p.asIdeal) (f x)))
Module: Mathlib.RingTheory.Etale.Locus

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ etaleLocus R A = Set.univ ↔ FormallyEtale R A

Tactic:
rw [etaleLocus_eq_compl_support, ← Set.compl_union, compl_eq_comm, Set.compl_univ, eq_comm,
    ← Set.subset_empty_iff, Set.union_subset_iff, Set.subset_empty_iff, Set.subset_empty_iff,
    Module.support_eq_empty_iff, Module.support_eq_empty_iff, Algebra.formallyEtale_iff]

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
s : S
a : A
⊢ (D S (S ⊗[R] A)) (s ⊗ₜ[R] a) = (tensorKaehlerEquiv R S A (S ⊗[R] A)) ((algebraMap S (S ⊗[R] A)) s ⊗ₜ[A] (D R A) a)

Tactic:
simp only [Algebra.TensorProduct.algebraMap_apply, Algebra.algebraMap_self, RingHom.id_apply,
    tensorKaehlerEquiv_tmul_D]

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
s : S
a : A
⊢ (D S (S ⊗[R] A)) (s ⊗ₜ[R] a) = s ⊗ₜ[R] 1 • (D S (S ⊗[R] A)) ((algebraMap A (S ⊗[R] A)) a)
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
s : S
a : A
⊢ (D S (A ⊗[R] S)) (a ⊗ₜ[R] s) = (tensorKaehlerEquiv R S A (A ⊗[R] S)) ((algebraMap S (A ⊗[R] S)) s ⊗ₜ[A] (D R A) a)

Tactic:
simp only [Algebra.TensorProduct.algebraMap_apply, Algebra.algebraMap_self, RingHom.id_apply,
    tensorKaehlerEquiv_tmul_D]

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
s : S
a : A
⊢ (D S (A ⊗[R] S)) (a ⊗ₜ[R] s) = (algebraMap S (A ⊗[R] S)) s • (D S (A ⊗[R] S)) (a ⊗ₜ[R] 1)
Module: Mathlib.RingTheory.AdicCompletion.AsTensorProduct

Goal state before:
pp: case hf
R : Type u_1
inst✝³ : CommRing R
I : Ideal R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
n : ℕ
p : (Fin n → R) →ₗ[R] M
hp : Function.Surjective ⇑p
f : AdicCompletion I R ⊗[R] (Fin n → R) →ₗ[AdicCompletion I R] AdicCompletion I M := ⋯
g : AdicCompletion I R ⊗[R] (Fin n → R) →ₗ[AdicCompletion I R] AdicCompletion I M := ⋯
hfg : f = g
⊢ Function.Surjective ⇑(ofTensorProduct I (Fin n → R))

Tactic:
· exact (ofTensorProduct_bijective_of_pi_of_fintype I (Fin n)).surjective

Goal state after:
Module: Mathlib.RingTheory.Extension.Presentation.Submersive

Goal state before:
pp: R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
T : Type u_1
inst✝² : CommRing T
inst✝¹ : Algebra R T
P : PreSubmersivePresentation R S ι σ
inst✝ : Finite σ
val✝ : Fintype σ
i j : σ
⊢ (baseChange T P).jacobiMatrix i j = (MvPolynomial.map (algebraMap R T)).mapMatrix P.jacobiMatrix i j

Tactic:
simp only [baseChange, jacobiMatrix_apply, Presentation.baseChange_relation,
      RingHom.mapMatrix_apply, Matrix.map_apply,
      Presentation.baseChange_toGenerators, MvPolynomial.pderiv_map]

Goal state after:
Module: Mathlib.RingTheory.Extension.Presentation.Submersive

Goal state before:
pp: case intro
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
T : Type u_1
inst✝² : CommRing T
inst✝¹ : Algebra R T
P : PreSubmersivePresentation R S ι σ
inst✝ : Finite σ
val✝ : Fintype σ
⊢ (algebraMap (baseChange T P).Ring (T ⊗[R] S)) (baseChange T P).jacobiMatrix.det =
    1 ⊗ₜ[R] (algebraMap P.Ring S) P.jacobiMatrix.det

Tactic:
have h : (baseChange T P).jacobiMatrix =
      (MvPolynomial.map (algebraMap R T)).mapMatrix P.jacobiMatrix := by
    ext i j : 1
    simp only [baseChange, jacobiMatrix_apply, Presentation.baseChange_relation,
      RingHom.mapMatrix_apply, Matrix.map_apply,
      Presentation.baseChange_toGenerators, MvPolynomial.pderiv_map]

Goal state after:
case intro
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
T : Type u_1
inst✝² : CommRing T
inst✝¹ : Algebra R T
P : PreSubmersivePresentation R S ι σ
inst✝ : Finite σ
val✝ : Fintype σ
h : (baseChange T P).jacobiMatrix = (MvPolynomial.map (algebraMap R T)).mapMatrix P.jacobiMatrix
⊢ (algebraMap (baseChange T P).Ring (T ⊗[R] S)) (baseChange T P).jacobiMatrix.det =
    1 ⊗ₜ[R] (algebraMap P.Ring S) P.jacobiMatrix.det
Module: Mathlib.RingTheory.Extension.Cotangent.Free

Goal state before:
pp: case hker
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)
hm : Submodule.span S (Set.range fun i ↦ (D R S) (P.val (v i))) = ⊤
hk : Disjoint P.toExtension.toKaehler.ker (Submodule.span S (Set.range fun x ↦ P.cotangentSpaceBasis (v x)))
inst✝ : Subsingleton (H1Cotangent R S)
f : P.toExtension.Cotangent →ₗ[S] ι →₀ S := ↑P.cotangentSpaceBasis.repr ∘ₗ P.toExtension.cotangentComplex
g : (ι →₀ S) →ₗ[S] Ω[S⁄R] := P.toExtension.toKaehler ∘ₗ ↑P.cotangentSpaceBasis.repr.symm
hfg : Function.Exact ⇑f ⇑g
⊢ Submodule.map (↑P.cotangentSpaceBasis.repr.symm) (P.toExtension.toKaehler ∘ₗ ↑P.cotangentSpaceBasis.repr.symm).ker ⊓
      Submodule.map (↑P.cotangentSpaceBasis.repr.symm) (Submodule.span S (Set.range fun x ↦ Finsupp.single (v x) 1)) =
    Submodule.map ↑P.cotangentSpaceBasis.repr.symm ⊥

Tactic:
Submodule.map_span,

Goal state after:
case hker
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)
hm : Submodule.span S (Set.range fun i ↦ (D R S) (P.val (v i))) = ⊤
hk : Disjoint P.toExtension.toKaehler.ker (Submodule.span S (Set.range fun x ↦ P.cotangentSpaceBasis (v x)))
inst✝ : Subsingleton (H1Cotangent R S)
f : P.toExtension.Cotangent →ₗ[S] ι →₀ S := ↑P.cotangentSpaceBasis.repr ∘ₗ P.toExtension.cotangentComplex
g : (ι →₀ S) →ₗ[S] Ω[S⁄R] := P.toExtension.toKaehler ∘ₗ ↑P.cotangentSpaceBasis.repr.symm
hfg : Function.Exact ⇑f ⇑g
⊢ Submodule.map (↑P.cotangentSpaceBasis.repr.symm) (P.toExtension.toKaehler ∘ₗ ↑P.cotangentSpaceBasis.repr.symm).ker ⊓
      Submodule.span S (⇑↑P.cotangentSpaceBasis.repr.symm '' Set.range fun x ↦ Finsupp.single (v x) 1) =
    Submodule.map ↑P.cotangentSpaceBasis.repr.symm ⊥
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
u : R
⊢ W'.dblXYZ (u • P) = u ^ 4 • W'.dblXYZ P

Tactic:
rw [dblXYZ, dblX_smul, dblY_smul, dblZ_smul, smul_fin3, dblXYZ_X, dblXYZ_Y, dblXYZ_Z]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
ι : Type u_3
κ : Type u_5
P : Generators R S ι
v : κ → ι
h : LinearIndependent S fun k ↦ (D R S) (P.val (v k))
x : P.toExtension.CotangentSpace
hx : x ∈ ↑P.toExtension.toKaehler.ker
hxs : ∃ c, (c.sum fun i a ↦ a • P.cotangentSpaceBasis (v i)) = x
⊢ x = 0

Tactic:
obtain ⟨c, rfl⟩ := hxs

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
ι : Type u_3
κ : Type u_5
P : Generators R S ι
v : κ → ι
h : LinearIndependent S fun k ↦ (D R S) (P.val (v k))
c : κ →₀ S
hx : (c.sum fun i a ↦ a • P.cotangentSpaceBasis (v i)) ∈ ↑P.toExtension.toKaehler.ker
⊢ (c.sum fun i a ↦ a • P.cotangentSpaceBasis (v i)) = 0
Module: Mathlib.RingTheory.Extension.Cotangent.LocalizationAway

Goal state before:
pp: case h
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 ι
Q : Generators S T Unit := localizationAway T g
algInst✝ : Algebra P.Ring ((localizationAway T g).comp P).Ring := ((localizationAway T g).toComp P).toAlgHom.toAlgebra
f : P.Ring ⧸ P.ker ^ 2 := (Ideal.Quotient.mk (P.ker ^ 2)) (P.σ g)
π : ((localizationAway T g).comp P).Ring →ₐ[R] Localization.Away ((Ideal.Quotient.mk (P.ker ^ 2)) (P.σ g)) :=
  compLocalizationAwayAlgHom T g P
x : ↥P.toExtension.ker
hx :
  (lift
        (↑S
          (↑(LinearMap.ringLmapEquivSelf T T (P.toExtension.Cotangent →ₗ[S] (Q.comp P).toExtension.Cotangent)).symm
            (Extension.Cotangent.map (Q.toComp P).toExtensionHom))))
      (((TensorProduct.mk S T P.toExtension.Cotangent) 1) (Extension.Cotangent.mk x)) =
    0
n : ℕ
hm : P.σ g ^ n * ↑x ∈ P.ker ^ 2
⊢ Extension.Cotangent.mk (P.σ g ^ n • x) = 0

Tactic:
Extension.Cotangent.mk_eq_zero_iff

Goal state after:
case h
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 ι
Q : Generators S T Unit := localizationAway T g
algInst✝ : Algebra P.Ring ((localizationAway T g).comp P).Ring := ((localizationAway T g).toComp P).toAlgHom.toAlgebra
f : P.Ring ⧸ P.ker ^ 2 := (Ideal.Quotient.mk (P.ker ^ 2)) (P.σ g)
π : ((localizationAway T g).comp P).Ring →ₐ[R] Localization.Away ((Ideal.Quotient.mk (P.ker ^ 2)) (P.σ g)) :=
  compLocalizationAwayAlgHom T g P
x : ↥P.toExtension.ker
hx :
  (lift
        (↑S
          (↑(LinearMap.ringLmapEquivSelf T T (P.toExtension.Cotangent →ₗ[S] (Q.comp P).toExtension.Cotangent)).symm
            (Extension.Cotangent.map (Q.toComp P).toExtensionHom))))
      (((TensorProduct.mk S T P.toExtension.Cotangent) 1) (Extension.Cotangent.mk x)) =
    0
n : ℕ
hm : P.σ g ^ n * ↑x ∈ P.ker ^ 2
⊢ ↑(P.σ g ^ n • x) ∈ P.toExtension.ker ^ 2
Module: Mathlib.RingTheory.RingHom.StandardSmooth

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
Rᵣ : Type u_2
inst✝² : CommRing Rᵣ
inst✝¹ : Algebra R Rᵣ
r : R
inst✝ : IsLocalization.Away r Rᵣ
r✝ : R
x✝ : Rᵣ
⊢ (have I := (algebraMap R Rᵣ).toAlgebra;
    r✝ • x✝) =
    r✝ • x✝

Tactic:
rw [Algebra.smul_def]

Goal state after:
R : Type u
inst✝³ : CommRing R
Rᵣ : Type u_2
inst✝² : CommRing Rᵣ
inst✝¹ : Algebra R Rᵣ
r : R
inst✝ : IsLocalization.Away r Rᵣ
r✝ : R
x✝ : Rᵣ
⊢ (have I := (algebraMap R Rᵣ).toAlgebra;
    r✝ • x✝) =
    (algebraMap R Rᵣ) r✝ * x✝
Module: Mathlib.RingTheory.Smooth.NoetherianDescent

Goal state before:
pp: case refine_2.refine_2
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
p : D.vars → MvPolynomial D.vars ↥(subalgebra R D)
hp : ∀ (i : D.vars), (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A)) (p i) = D.h i
hf₀ :
  Function.Surjective
    ⇑(Ideal.Quotient.mkₐ (↥(subalgebra R D))
        (Ideal.span (Set.range (Presentation.relationOfHasCoeffs ↥(subalgebra R D)))))
i : D.vars
hinj : Function.Injective ⇑(MvPolynomial.map (algebraMap (↥(subalgebra R D)) A))
t : MvPolynomial D.rels (MvPolynomial D.vars ↥(subalgebra R D))
ht : (MvPolynomial.map (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A))) t = D.q i
⊢ (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A))
      ((eval (Presentation.relationOfHasCoeffs ↥(subalgebra R D))) t) =
    (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A)) (p i - X i)

Tactic:
simp [MvPolynomial.map_eval, Function.comp_def,
        Presentation.map_relationOfHasCoeffs, ht, hq, hp]

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:
simpa using hJ

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:
rw [isProper_eq]

Goal state after:
X Y Z S : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ (@IsSeparated ⊓ @UniversallyClosed ⊓ @LocallyOfFiniteType).RespectsIso
Module: Mathlib.AlgebraicGeometry.Morphisms.Proper

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

Tactic:
rw [isProper_eq]

Goal state after:
X Y Z S : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ (@IsSeparated ⊓ @UniversallyClosed ⊓ @LocallyOfFiniteType).IsStableUnderComposition
Module: Mathlib.AlgebraicGeometry.Morphisms.Proper

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

Tactic:
rw [isProper_eq]

Goal state after:
X Y Z S : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ (@IsSeparated ⊓ @UniversallyClosed ⊓ @LocallyOfFiniteType).IsMultiplicative
Module: Mathlib.AlgebraicGeometry.Morphisms.Proper

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

Tactic:
rw [isProper_eq]

Goal state after:
X Y Z S : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ (@IsSeparated ⊓ @UniversallyClosed ⊓ @LocallyOfFiniteType).IsStableUnderBaseChange
Module: Mathlib.AlgebraicGeometry.Morphisms.Proper

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

Tactic:
rw [isProper_eq]

Goal state after:
X Y Z S : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ IsZariskiLocalAtTarget (@IsSeparated ⊓ @UniversallyClosed ⊓ @LocallyOfFiniteType)
Module: Mathlib.AlgebraicGeometry.Morphisms.Proper

Goal state before:
pp: X : Scheme
K : Type u
inst✝² : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst✝¹ : IsIntegral X
inst✝ : UniversallyClosed f
F : CommRingCat.of K ⟶ Γ(X, ⊤) := (Scheme.ΓSpecIso (CommRingCat.of K)).inv ≫ Scheme.Hom.appTop f
⊢ (CommRingCat.Hom.hom F).IsIntegral

Tactic:
apply RingHom.isIntegral_respectsIso.2 (e := (Scheme.ΓSpecIso _).symm.commRingCatIsoToRingEquiv)

Goal state after:
X : Scheme
K : Type u
inst✝² : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst✝¹ : IsIntegral X
inst✝ : UniversallyClosed f
F : CommRingCat.of K ⟶ Γ(X, ⊤) := ⋯
⊢ (Scheme.Hom.appTop f).hom'.IsIntegral
Module: Mathlib.FieldTheory.SeparablyGenerated

Goal state before:
pp: case refine_2
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₀ : Polynomial (MvPolynomial { b // b ≠ i } k) :=
  (optionEquivLeft k { b // b ≠ i }) ((renameEquiv k (Equiv.optionSubtypeNe i).symm) F)
H :
  (Algebra.adjoin k (a '' {i}ᶜ)).val ((F.toPolynomialAdjoinImageCompl a i).coeff (σ i)) =
    (Algebra.adjoin k (a '' {i}ᶜ)).val 0
⊢ (aeval a) ((rename Subtype.val) (F₀.coeff (σ i))) = 0

Tactic:
simp_rw [toPolynomialAdjoinImageCompl, Polynomial.coe_mapAlgHom, Polynomial.coeff_map,
      AlgHom.coe_toRingHom, map_zero] at H

Goal state after:
case refine_2
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₀ : Polynomial (MvPolynomial { b // b ≠ i } k) :=
  (optionEquivLeft k { b // b ≠ i }) ((renameEquiv k (Equiv.optionSubtypeNe i).symm) F)
H :
  (Algebra.adjoin k (a '' {i}ᶜ)).val
      ((aeval fun j ↦ ⟨a ↑j, ⋯⟩)
        (((optionEquivLeft k { b // b ≠ i }) ((renameEquiv k (Equiv.optionSubtypeNe i).symm) F)).coeff (σ i))) =
    0
⊢ (aeval a) ((rename Subtype.val) (F₀.coeff (σ i))) = 0
Module: Mathlib.AlgebraicGeometry.Morphisms.LocalClosure

Goal state before:
pp: case refine_1
P : MorphismProperty Scheme
X Y : Scheme
inst✝ : P.RespectsIso
f : X ⟶ Y
x✝ : sourceLocalClosure IsOpenImmersion P f
x : ↥X
𝒰 : Scheme.Cover (Scheme.precoverage IsOpenImmersion) X
hf : ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ f)
⊢ P ((Scheme.Hom.isoOpensRange (𝒰.f (𝒰.idx x))).inv ≫ 𝒰.f (𝒰.idx x) ≫ f)

Tactic:
P.cancel_left_of_respectsIso

Goal state after:
case refine_1
P : MorphismProperty Scheme
X Y : Scheme
inst✝ : P.RespectsIso
f : X ⟶ Y
x✝ : sourceLocalClosure IsOpenImmersion P f
x : ↥X
𝒰 : Scheme.Cover (Scheme.precoverage IsOpenImmersion) X
hf : ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ f)
⊢ P (𝒰.f (𝒰.idx x) ≫ 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 : adjoin k (Set.range a) = ⊤
ha' : IsTranscendenceBasis k fun i ↦ a ↑i
⊢ ∃ i, (IsTranscendenceBasis k fun j ↦ a ↑j) ∧ Algebra.IsSeparable (↥(adjoin k (a '' {i}ᶜ))) K

Tactic:
by
  have ⟨i, hi⟩ := exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow p hp H n ha'
  refine ⟨i, hi.1, ?_⟩
  rw [← separableClosure.eq_top_iff, ← (restrictScalars_injective k).eq_iff,
    restrictScalars_top, eq_top_iff, ← ha, adjoin_le_iff]
  rintro _ ⟨x, rfl⟩
  obtain rfl | ne := eq_or_ne x i
  · exact hi.2
  · exact isSeparable_algebraMap (F := adjoin k (a '' {i}ᶜ)) ⟨_, subset_adjoin _ _ ⟨x, ne, rfl⟩⟩

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

Goal state before:
pp: case inr.refine_2
P P' : MorphismProperty Scheme
inst✝² : IsZariskiLocalAtTarget P
inst✝¹ : P'.IsStableUnderBaseChange
H : ∀ {R : CommRingCat} {X Y : Scheme} (f : X ⟶ Spec R) (g : Y ⟶ Spec R), P' f → P (pullback.fst f g) → P g
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : HasPullback f g
h : P' f
hf : P (pullback.fst f g)
this :
  ∀ {X Y Z : Scheme} {f : X ⟶ Z} {g : Y ⟶ Z} [inst : HasPullback f g],
    P' f → P (pullback.fst f g) → (∃ R, Z = Spec R) → P g
hZ : ¬∃ R, Z = Spec R
i : Z.affineCover.toPreZeroHypercover.1
ι : Z.affineCover.X i ⟶ Z := Z.affineCover.f i
e : pullback (pullback.snd f ι) (pullback.snd g ι) ≅ pullback (pullback.fst f g) (pullback.fst f ι) :=
  pullbackLeftPullbackSndIso f ι (pullback.snd g ι) ≪≫
    pullback.congrHom ⋯ ⋯ ≪≫
      (pullbackAssoc f g g ι).symm ≪≫ pullback.congrHom ⋯ ⋯ ≪≫ (pullbackRightPullbackFstIso f ι (pullback.fst f g)).symm
heq : e.hom ≫ pullback.snd (pullback.fst f g) (pullback.fst f ι) = pullback.fst (pullback.snd f ι) (pullback.snd g ι)
⊢ P (e.hom ≫ pullback.snd (pullback.fst f g) (pullback.fst f ι))

Tactic:
P.cancel_left_of_respectsIso

Goal state after:
case inr.refine_2
P P' : MorphismProperty Scheme
inst✝² : IsZariskiLocalAtTarget P
inst✝¹ : P'.IsStableUnderBaseChange
H : ∀ {R : CommRingCat} {X Y : Scheme} (f : X ⟶ Spec R) (g : Y ⟶ Spec R), P' f → P (pullback.fst f g) → P g
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : HasPullback f g
h : P' f
hf : P (pullback.fst f g)
this :
  ∀ {X Y Z : Scheme} {f : X ⟶ Z} {g : Y ⟶ Z} [inst : HasPullback f g],
    P' f → P (pullback.fst f g) → (∃ R, Z = Spec R) → P g
hZ : ¬∃ R, Z = Spec R
i : Z.affineCover.toPreZeroHypercover.1
ι : Z.affineCover.X i ⟶ Z := Z.affineCover.f i
e : pullback (pullback.snd f ι) (pullback.snd g ι) ≅ pullback (pullback.fst f g) (pullback.fst f ι) :=
  pullbackLeftPullbackSndIso f ι (pullback.snd g ι) ≪≫
    pullback.congrHom ⋯ ⋯ ≪≫
      (pullbackAssoc f g g ι).symm ≪≫ pullback.congrHom ⋯ ⋯ ≪≫ (pullbackRightPullbackFstIso f ι (pullback.fst f g)).symm
heq : e.hom ≫ pullback.snd (pullback.fst f g) (pullback.fst f ι) = pullback.fst (pullback.snd f ι) (pullback.snd g ι)
⊢ P (pullback.snd (pullback.fst f g) (pullback.fst f ι))