mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Etale.Field

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : EssFiniteType K L
⊢ FormallyEtale K L

Tactic:
by
  -- We already know that for field extensions
  -- IsSeparable + EssFiniteType => FormallyUnramified + Finite
  have := FormallyUnramified.of_isSeparable K L
  have := FormallyUnramified.finite_of_free (R := K) (S := L)
  -- We shall show that any `f : L → B/I` can be lifted to `L → B` if `I^2 = ⊥`
  refine FormallyEtale.iff_comp_bijective.mpr fun B _ _ I h ↦ ?_
  refine ⟨FormallyUnramified.iff_comp_injective_of_small.mp
    (FormallyUnramified.of_isSeparable K L) I h, ?_⟩
  intro f
  -- By separability and finiteness, we may assume `L = K(α)` with `p` the minpoly of `α`.
  let pb := Field.powerBasisOfFiniteOfSeparable K L
  -- Let `x : B` such that `f(α) = x` in `B / I`.
  obtain ⟨x, hx⟩ := Ideal.Quotient.mk_surjective (f pb.gen)
  have helper : ∀ x, IsScalarTower.toAlgHom K B (B ⧸ I) x = Ideal.Quotient.mk I x := fun _ ↦ rfl
  -- Then `p(x) = 0 mod I`, and the goal is to find some `ε ∈ I` such that
  -- `p(x + ε) = p(x) + ε p'(x) = 0`, and we will get our lift into `B`.
  have hx' : Ideal.Quotient.mk I (aeval x (minpoly K pb.gen)) = 0 := by
    rw [← helper, ← aeval_algHom_apply, helper, hx, aeval_algHom_apply, minpoly.aeval, map_zero]
  -- Since `p` is separable, `-p'(x)` is invertible in `B ⧸ I`,
  obtain ⟨u, hu⟩ : ∃ u, (aeval x) (derivative (minpoly K pb.gen)) * u + 1 ∈ I := by
    have := (isUnit_iff_ne_zero.mpr ((Algebra.IsSeparable.isSeparable K
      pb.gen).aeval_derivative_ne_zero (minpoly.aeval K _))).map f
    rw [← aeval_algHom_apply, ← hx, ← helper, aeval_algHom_apply, helper] at this
    obtain ⟨u, hu⟩ := Ideal.Quotient.mk_surjective (-this.unit⁻¹ : B ⧸ I)
    use u
    rw [← Ideal.Quotient.eq_zero_iff_mem, map_add, map_mul, map_one, hu, mul_neg,
      IsUnit.mul_val_inv, neg_add_cancel]
  -- And `ε = p(x)/(-p'(x))` works.
  use pb.liftEquiv.symm ⟨x + u * aeval x (minpoly K pb.gen), ?_⟩
  · apply pb.algHom_ext
    simp [hx, hx']
  · rw [← eval_map_algebraMap, Polynomial.eval_add_of_sq_eq_zero, derivative_map,
      ← one_mul (eval x _), eval_map_algebraMap, eval_map_algebraMap, ← mul_assoc, ← add_mul,
      ← Ideal.mem_bot, ← h, pow_two, add_comm]
    · exact Ideal.mul_mem_mul hu (Ideal.Quotient.eq_zero_iff_mem.mp hx')
    rw [← Ideal.mem_bot, ← h]
    apply Ideal.pow_mem_pow
    rw [← Ideal.Quotient.eq_zero_iff_mem, map_mul, hx', mul_zero]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : IsLocalRing S
inst✝⁷ : Algebra R S
P : Type u_3
inst✝⁶ : CommRing P
inst✝⁵ : Algebra R P
inst✝⁴ : Algebra P S
inst✝³ : IsScalarTower R P S
inst✝² : FormallySmooth R P
inst✝¹ : Module.Free P Ω[P⁄R]
inst✝ : Module.Finite P Ω[P⁄R]
h₁ : Function.Surjective ⇑(algebraMap P S)
h₂ : (RingHom.ker (algebraMap P S)).FG
P' : Extension R S :=
  { Ring := P, commRing := inst✝⁶, algebra₁ := inst✝⁵, algebra₂ := inst✝⁴, isScalarTower := inst✝³,
    σ := Function.surjInv h₁, algebraMap_σ := ⋯ }
⊢ FormallySmooth R S ↔ Function.Injective ⇑(cotangentComplexBaseChange R S P (ResidueField S))

Tactic:
Algebra.FormallySmooth.iff_injective_lTensor_residueField P' h₂

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : IsLocalRing S
inst✝⁷ : Algebra R S
P : Type u_3
inst✝⁶ : CommRing P
inst✝⁵ : Algebra R P
inst✝⁴ : Algebra P S
inst✝³ : IsScalarTower R P S
inst✝² : FormallySmooth R P
inst✝¹ : Module.Free P Ω[P⁄R]
inst✝ : Module.Finite P Ω[P⁄R]
h₁ : Function.Surjective ⇑(algebraMap P S)
h₂ : (RingHom.ker (algebraMap P S)).FG
P' : Extension R S :=
  { Ring := P, commRing := inst✝⁶, algebra₁ := inst✝⁵, algebra₂ := inst✝⁴, isScalarTower := inst✝³,
    σ := Function.surjInv h₁, algebraMap_σ := ⋯ }
⊢ Function.Injective ⇑(LinearMap.lTensor (ResidueField S) P'.cotangentComplex) ↔
    Function.Injective ⇑(cotangentComplexBaseChange R S P (ResidueField S))
Module: Mathlib.RingTheory.Smooth.Local

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : IsLocalRing S
inst✝⁷ : Algebra R S
P : Type u_3
inst✝⁶ : CommRing P
inst✝⁵ : Algebra R P
inst✝⁴ : Algebra P S
inst✝³ : IsScalarTower R P S
inst✝² : FormallySmooth R P
inst✝¹ : Module.Free P Ω[P⁄R]
inst✝ : Module.Finite P Ω[P⁄R]
h₁ : Function.Surjective ⇑(algebraMap P S)
h₂ : (RingHom.ker (algebraMap P S)).FG
P' : Extension R S :=
  { Ring := P, commRing := inst✝⁶, algebra₁ := inst✝⁵, algebra₂ := inst✝⁴, isScalarTower := inst✝³,
    σ := Function.surjInv h₁, algebraMap_σ := ⋯ }
⊢ FormallySmooth R S ↔ Function.Injective ⇑(cotangentComplexBaseChange R S P (ResidueField S))

Tactic:
rw [Algebra.FormallySmooth.iff_injective_lTensor_residueField P' h₂]

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : IsLocalRing S
inst✝⁷ : Algebra R S
P : Type u_3
inst✝⁶ : CommRing P
inst✝⁵ : Algebra R P
inst✝⁴ : Algebra P S
inst✝³ : IsScalarTower R P S
inst✝² : FormallySmooth R P
inst✝¹ : Module.Free P Ω[P⁄R]
inst✝ : Module.Finite P Ω[P⁄R]
h₁ : Function.Surjective ⇑(algebraMap P S)
h₂ : (RingHom.ker (algebraMap P S)).FG
P' : Extension R S :=
  { Ring := P, commRing := inst✝⁶, algebra₁ := inst✝⁵, algebra₂ := inst✝⁴, isScalarTower := inst✝³,
    σ := Function.surjInv h₁, algebraMap_σ := ⋯ }
⊢ Function.Injective ⇑(LinearMap.lTensor (ResidueField S) P'.cotangentComplex) ↔
    Function.Injective ⇑(cotangentComplexBaseChange R S P (ResidueField S))
Module: Mathlib.RingTheory.Etale.Field

Goal state before:
pp: case refine_6
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsSeparable K L
B : Type (max u_1 u_2)
x✝¹ : CommRing B
x✝ : Algebra K B
I : Ideal B
h : I ^ 2 = ⊥
f : L →ₐ[K] B ⧸ I
g : (k : L) → ↥K⟮k⟯ →ₐ[K] B
hg₁ : ∀ (k : L), (fun g ↦ (Ideal.Quotient.mkₐ K I).comp g = f.comp (IsScalarTower.toAlgHom K (↥K⟮k⟯) L)) (g k)
hg₂ :
  ∀ (k : L) (y : ↥K⟮k⟯ →ₐ[K] B),
    (fun g ↦ (Ideal.Quotient.mkₐ K I).comp g = f.comp (IsScalarTower.toAlgHom K (↥K⟮k⟯) L)) y → y = g k
hg₃ : ∀ (x y : L) (h : x ∈ K⟮y⟯), (g y) ⟨x, h⟩ = (g x) (IntermediateField.AdjoinSimple.gen K x)
H : ∀ (x y : L), ∃ α, x ∈ K⟮α⟯ ∧ y ∈ K⟮α⟯
x : L
⊢ ((Ideal.Quotient.mkₐ K I).comp
        { toFun := fun x ↦ (g x) (IntermediateField.AdjoinSimple.gen K x), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯,
          map_add' := ⋯, commutes' := ⋯ })
      x =
    f x

Tactic:
simpa using AlgHom.congr_fun (hg₁ x) (IntermediateField.AdjoinSimple.gen K x)

Goal state after:
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
inst✝ : FinitePresentation R A
⊢ IsOpen (etaleLocus R A)

Tactic:
rw [etaleLocus_eq_unramfiedLocus_inter_smoothLocus]
  exact isOpen_unramifiedLocus.inter isOpen_smoothLocus

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

Tactic:
Algebra.TensorProduct.right_algebraMap_apply

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) = (D S (A ⊗[R] S)) (1 ⊗ₜ[R] s * a ⊗ₜ[R] 1)
Module: Mathlib.LinearAlgebra.Basis.Exact

Goal state before:
pp: R : Type u_1
M : Type u_2
K : Type u_3
P : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup K
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R K
inst✝ : Module R P
f : K →ₗ[R] M
g : M →ₗ[R] P
s : M →ₗ[R] K
hs : s ∘ₗ f = LinearMap.id
hfg : Function.Exact ⇑f ⇑g
ι : Type u_5
κ : Type u_6
v : ι → M
a : κ → ι
hainj : Function.Injective a
hsa : ∀ (i : κ), s (v (a i)) = 0
hli : LinearIndependent R v
⊢ ∀ x ∈ Submodule.span R (Set.range (v ∘ a)), x ∈ f.range → x = 0

Tactic:
rintro - hy ⟨y, rfl⟩

Goal state after:
R : Type u_1
M : Type u_2
K : Type u_3
P : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup K
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R K
inst✝ : Module R P
f : K →ₗ[R] M
g : M →ₗ[R] P
s : M →ₗ[R] K
hs : s ∘ₗ f = LinearMap.id
hfg : Function.Exact ⇑f ⇑g
ι : Type u_5
κ : Type u_6
v : ι → M
a : κ → ι
hainj : Function.Injective a
hsa : ∀ (i : κ), s (v (a i)) = 0
hli : LinearIndependent R v
y : K
hy : f y ∈ Submodule.span R (Set.range (v ∘ a))
⊢ f y = 0
Module: Mathlib.RingTheory.Extension.Presentation.Submersive

Goal state before:
pp: case intro.intro
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
ι' : Type u_1
σ' : Type u_2
T : Type u_3
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
Q : PreSubmersivePresentation S T ι' σ'
P : PreSubmersivePresentation R S ι σ
inst✝¹ : Finite σ
inst✝ : Finite σ'
val✝¹ : Fintype σ'
val✝ : Fintype σ
⊢ (aeval (Q.comp P).val) (Q.comp P).jacobiMatrix.toBlocks₁₁.det *
      (aeval (Q.comp P).val) (Q.comp P).jacobiMatrix.toBlocks₂₂.det =
    P.jacobian • Q.jacobian

Tactic:
jacobiMatrix_comp_₁₁_det,

Goal state after:
case intro.intro
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
ι' : Type u_1
σ' : Type u_2
T : Type u_3
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
Q : PreSubmersivePresentation S T ι' σ'
P : PreSubmersivePresentation R S ι σ
inst✝¹ : Finite σ
inst✝ : Finite σ'
val✝¹ : Fintype σ'
val✝ : Fintype σ
⊢ Q.jacobian * (aeval (Q.comp P).val) (Q.comp P).jacobiMatrix.toBlocks₂₂.det = P.jacobian • Q.jacobian
Module: Mathlib.LinearAlgebra.Basis.Exact

Goal state before:
pp: R : Type u_1
M : Type u_2
K : Type u_3
P : Type u_4
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup K
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R M
inst✝³ : Module R K
inst✝² : Module R P
f : K →ₗ[R] M
g : M →ₗ[R] P
hfg : Function.Exact ⇑f ⇑g
hf : Function.Injective ⇑f
q : Submodule R M
E : Type u_8
inst✝¹ : AddCommGroup E
inst✝ : Module R E
i : E →ₗ[R] M
hi : Function.Injective ⇑i
h : IsCompl i.range q
hker : Disjoint g.ker q
hmap : Submodule.map g q = ⊤
⊢ Function.Bijective ⇑(linearProjOfIsCompl q i hi h ∘ₗ f)

Tactic:
LinearMap.linearProjOfIsCompl,

Goal state after:
R : Type u_1
M : Type u_2
K : Type u_3
P : Type u_4
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup K
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R M
inst✝³ : Module R K
inst✝² : Module R P
f : K →ₗ[R] M
g : M →ₗ[R] P
hfg : Function.Exact ⇑f ⇑g
hf : Function.Injective ⇑f
q : Submodule R M
E : Type u_8
inst✝¹ : AddCommGroup E
inst✝ : Module R E
i : E →ₗ[R] M
hi : Function.Injective ⇑i
h : IsCompl i.range q
hker : Disjoint g.ker q
hmap : Submodule.map g q = ⊤
⊢ Function.Bijective ⇑((↑(LinearEquiv.ofInjective i hi).symm ∘ₗ i.range.projectionOnto q h) ∘ₗ f)
Module: Mathlib.RingTheory.Extension.Presentation.Core

Goal state before:
pp: R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
inst✝⁷ : Finite σ
P : SubmersivePresentation R S ι σ
R₀ : Type u_5
inst✝⁶ : CommRing R₀
inst✝⁵ : Algebra R₀ R
inst✝⁴ : Algebra R₀ S
inst✝³ : IsScalarTower R₀ R S
inst✝² : P.HasCoeffs R₀
inst✝¹ : FaithfulSMul R₀ R
inst✝ : Fintype σ
⊢ ∑ i, P.jacobianRelationsOfHasCoeffs R₀ i * Presentation.relationOfHasCoeffs R₀ i =
    P.jacobianOfHasCoeffs R₀ * P.invJacobianOfHasCoeffs R₀ - 1

Tactic:
apply MvPolynomial.map_injective _ (FaithfulSMul.algebraMap_injective R₀ R)

Goal state after:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
inst✝⁷ : Finite σ
P : SubmersivePresentation R S ι σ
R₀ : Type u_5
inst✝⁶ : CommRing R₀
inst✝⁵ : Algebra R₀ R
inst✝⁴ : Algebra R₀ S
inst✝³ : IsScalarTower R₀ R S
inst✝² : P.HasCoeffs R₀
inst✝¹ : FaithfulSMul R₀ R
inst✝ : Fintype σ
⊢ (MvPolynomial.map (algebraMap R₀ R))
      (∑ i, P.jacobianRelationsOfHasCoeffs R₀ i * Presentation.relationOfHasCoeffs R₀ i) =
    (MvPolynomial.map (algebraMap R₀ R)) (P.jacobianOfHasCoeffs R₀ * P.invJacobianOfHasCoeffs R₀ - 1)
Module: Mathlib.RingTheory.Smooth.StandardSmoothCotangent

Goal state before:
pp: R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsStandardSmooth R S
⊢ FormallySmooth R S

Tactic:
rw [Algebra.formallySmooth_iff]
    exact ⟨inferInstance, inferInstance⟩

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
σ✝ : Type u_3
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
x : P.Ring
y : MvPolynomial ι R
z : P.Ring
⊢ (x • (Ideal.Quotient.mk (Ideal.span (Set.range (Subtype.val ∘ D.f ∘ ⇑b)))) y) • (algebraMap P.Ring S) z =
    x • (Ideal.Quotient.mk (Ideal.span (Set.range (Subtype.val ∘ D.f ∘ ⇑b)))) y • (algebraMap P.Ring S) z

Tactic:
simp only [Algebra.smul_def, map_mul, Generators.algebraMap_apply, ← mul_assoc]

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_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
x : P.Ring
y : MvPolynomial ι R
z : P.Ring
⊢ (algebraMap D.T S) ((algebraMap P.Ring D.T) x) *
        (algebraMap D.T S) ((Ideal.Quotient.mk (Ideal.span (Set.range (Subtype.val ∘ D.f ∘ ⇑b)))) y) *
      (aeval P.val) z =
    (aeval P.val) x * (algebraMap D.T S) ((Ideal.Quotient.mk (Ideal.span (Set.range (Subtype.val ∘ D.f ∘ ⇑b)))) y) *
      (aeval P.val) z
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
x : ↥D.presLeft.toExtension.ker
⊢ Extension.Cotangent.mk
      ⟨(RingHom.id (naive (fun x ↦ if x = 0 then 0 else if x = -1 then -1 else Function.surjInv ⋯ x) ⋯).Ring) ↑x, ⋯⟩ =
    Extension.Cotangent.mk ⟨↑x, ⋯⟩

Tactic:
RingHom.id_apply

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
this :
  HasRingHomProperty @Smooth fun {R S} [CommRing R] [CommRing S] ↦
    Locally fun {R S} [CommRing R] [CommRing S] ↦ IsStandardSmooth
a✝ : ↥X
⊢ (∃ a,
      ∃ (h : a ∈ Y.affineOpens),
        ∃ a_1,
          a✝ ∈ a_1 ∧
            ∃ (h_1 : a_1 ∈ X.affineOpens) (h_2 : a_1 ≤ f ⁻¹ᵁ a),
              (CommRingCat.Hom.hom (Scheme.Hom.appLE f a a_1 ⋯)).IsStandardSmooth) ↔
    ∃ U,
      IsAffineOpen U ∧
        ∃ V,
          a✝ ∈ V ∧
            IsAffineOpen V ∧ ∃ (e : V ≤ f ⁻¹ᵁ U), (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).IsStandardSmooth

Tactic:
grind [Scheme.affineOpens]

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

Goal state before:
pp: case h
n m : ℕ
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
a✝ : ↥X
⊢ (∃ U,
      IsAffineOpen U ∧
        ∃ V,
          a✝ ∈ V ∧
            IsAffineOpen V ∧
              ∃ (e : V ≤ f ⁻¹ᵁ U),
                IsStandardSmoothOfRelativeDimension n (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e))) ↔
    ∃ a,
      ∃ (h : a ∈ Y.affineOpens),
        ∃ a_1,
          a✝ ∈ a_1 ∧
            ∃ (h_1 : a_1 ∈ X.affineOpens) (h_2 : a_1 ≤ f ⁻¹ᵁ a),
              IsStandardSmoothOfRelativeDimension n (CommRingCat.Hom.hom (Scheme.Hom.appLE f a a_1 ⋯))

Tactic:
grind [Scheme.affineOpens]

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:
by
  rw [negAddY, hQz, X_eq_zero_of_Z_eq_zero hQ hQz, negY]
  ring1

Goal state after:
Module: Mathlib.FieldTheory.SeparablyGenerated

Goal state before:
pp: k : Type u_1
K : Type u_2
ι : Type u_3
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
p : ℕ
hp : Nat.Prime p
a : ι → K
F : MvPolynomial ι k
HF : ∀ (F' : MvPolynomial ι k), F' ≠ 0 → (aeval a) F' = 0 → F.totalDegree ≤ F'.totalDegree
hF0 : F ≠ 0
hFa : (aeval a) F = 0
this : ∀ (i : ι), ∀ σ ∈ F.support, p ∣ σ i
σ' : (ι →₀ ℕ) → ι →₀ ℕ
hσ' : ∀ σ ∈ F.support, σ = p • σ' σ
hσ'' : ∀ (σ : ↥F.support), ↑σ = p • σ' ↑σ
H : ∀ (ι : Type u_3) (x : Fintype ι) (v : ι → K), LinearIndependent k v → LinearIndependent k fun x ↦ v x ^ p
F' : ↥F.support →₀ k
hF' : (Finsupp.linearCombination k fun s ↦ (aeval a) ((monomial (σ' ↑s)) 1)) F' = 0
hF'0 : ¬F' = 0
F'' : MvPolynomial ι k := AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain (fun s ↦ σ' ↑s) F')
hF''0 : F'' ≠ 0
hF'' : (aeval a) F'' = 0
σ : ↥F.support
hσ₂ : σ ∈ F'.support
hσ : σ' ↑σ ∈ F''.support
| (p • σ' ↑σ).sum fun x e ↦ e

Tactic:
Finsupp.sum_smul_index (fun _ ↦ rfl),

Goal state after:
k : Type u_1
K : Type u_2
ι : Type u_3
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
p : ℕ
hp : Nat.Prime p
a : ι → K
F : MvPolynomial ι k
HF : ∀ (F' : MvPolynomial ι k), F' ≠ 0 → (aeval a) F' = 0 → F.totalDegree ≤ F'.totalDegree
hF0 : F ≠ 0
hFa : (aeval a) F = 0
this : ∀ (i : ι), ∀ σ ∈ F.support, p ∣ σ i
σ' : (ι →₀ ℕ) → ι →₀ ℕ
hσ' : ∀ σ ∈ F.support, σ = p • σ' σ
hσ'' : ∀ (σ : ↥F.support), ↑σ = p • σ' ↑σ
H : ∀ (ι : Type u_3) (x : Fintype ι) (v : ι → K), LinearIndependent k v → LinearIndependent k fun x ↦ v x ^ p
F' : ↥F.support →₀ k
hF' : (Finsupp.linearCombination k fun s ↦ (aeval a) ((monomial (σ' ↑s)) 1)) F' = 0
hF'0 : ¬F' = 0
F'' : MvPolynomial ι k := AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain (fun s ↦ σ' ↑s) F')
hF''0 : F'' ≠ 0
hF'' : (aeval a) F'' = 0
σ : ↥F.support
hσ₂ : σ ∈ F'.support
hσ : σ' ↑σ ∈ F''.support
| (σ' ↑σ).sum fun i a ↦ p * a
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 : ι
hi : (IsTranscendenceBasis k fun j ↦ a ↑j) ∧ IsSeparable (↥(adjoin k (a '' {i}ᶜ))) (a i)
⊢ restrictScalars k (separableClosure (↥(adjoin k (a '' {i}ᶜ))) K) = restrictScalars k ⊤

Tactic:
restrictScalars_top,

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 : adjoin k (Set.range a) = ⊤
ha' : IsTranscendenceBasis k fun i ↦ a ↑i
i : ι
hi : (IsTranscendenceBasis k fun j ↦ a ↑j) ∧ IsSeparable (↥(adjoin k (a '' {i}ᶜ))) (a i)
⊢ restrictScalars k (separableClosure (↥(adjoin k (a '' {i}ᶜ))) K) = ⊤
Module: Mathlib.AlgebraicGeometry.Morphisms.Descent

Goal state before:
pp: case refine_2
P : MorphismProperty Scheme
X : Scheme
inst✝² : CompactSpace ↥X
inst✝¹ : IsZariskiLocalAtSource P
inst✝ : P.ContainsIdentities
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
p : (∐ fun i ↦ 𝒰.X i) ⟶ X := Sigma.desc fun i ↦ 𝒰.f i
⊢ ∀ (i : (sigmaOpenCover fun i ↦ 𝒰.X i).I₀), P ((sigmaOpenCover fun i ↦ 𝒰.X i).f i ≫ p)

Tactic:
exact fun i ↦ by simpa [p] using IsZariskiLocalAtSource.of_isOpenImmersion _

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 (pullback.fst f (g' ≫ U.ι))

Tactic:
AlgebraicGeometry.IsOpenImmersion.lift_fac

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'
⊢ IsOpenImmersion (pullback.fst f g)
Module: Mathlib.RingTheory.Valuation.IsTrivialOn

Goal state before:
pp: case neg
Γ : Type u_1
inst✝³ : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst✝² : CommSemiring A
B : Type u_3
inst✝¹ : Ring B
inst✝ : Algebra A B
v : Valuation B Γ
hv : Valuation.IsTrivialOn A v
w : B
hpos : 1 < v w
p : A[X]
hp : p ≠ 0
i : ℕ
hi : i < p.natDegree
h0 : ¬p.coeff i = 0
⊢ v ((algebraMap A B) (p.coeff i)) * v w ^ i < v ((algebraMap A B) p.leadingCoeff) * v w ^ p.natDegree

Tactic:
simp [hv.eq_one p.leadingCoeff (leadingCoeff_ne_zero.mpr hp),
      hv.eq_one _ h0, pow_lt_pow_right₀ hpos hi]

Goal state after:
Module: Mathlib.RingTheory.Conductor

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
I : Ideal R
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
h_alg : Function.Injective ⇑(algebraMap (↥R[x]) S)
f : ↥R[x] ⧸ Ideal.map (algebraMap R ↥R[x]) I →+* S ⧸ Ideal.map (algebraMap R S) I :=
  Ideal.Quotient.lift (Ideal.map (algebraMap R ↥R[x]) I)
    ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)).comp (algebraMap (↥R[x]) S)) ⋯
u : ↥R[x]
hu : u ∈ ker ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)).comp (algebraMap (↥R[x]) S))
⊢ u ∈ Ideal.map (algebraMap R ↥R[x]) I

Tactic:
rwa [RingHom.mem_ker, RingHom.comp_apply, Ideal.Quotient.eq_zero_iff_mem, ← Ideal.mem_comap,
      comap_map_eq_map_adjoin_of_coprime_conductor hx h_alg] at hu

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
hσ : Finite σ
α : Type w
inst✝ : Fintype α
IH :
  ∀ {f : MvPolynomial α S},
    (algebraMap (MvPolynomial α R) (MvPolynomial α S)).IsIntegralElem f → ∀ (n : α →₀ ℕ), IsIntegral R (coeff n f)
f : MvPolynomial (Option α) S
H : (algebraMap (MvPolynomial (Option α) R) (MvPolynomial (Option α) S)).IsIntegralElem f
n : Option α →₀ ℕ
⊢ (((optionEquivLeft S α).symm.toRingEquiv.toRingHom.comp
            (algebraMap (Polynomial (MvPolynomial α R)) (Polynomial (MvPolynomial α S)))).comp
        (optionEquivLeft R α).toRingEquiv.toRingHom).IsIntegralElem
    ((optionEquivLeft S α).symm.toRingEquiv.toRingHom ((optionEquivLeft S α) f))

Tactic:
convert! H
        · ext i m
          · aesop
          · cases i <;> aesop
        · aesop

Goal state after:
Module: Mathlib.RingTheory.LocalRing.ResidueField.Polynomial

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
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
⊢ RingHom.ker ↑f ≤ RingHom.ker ((aeval (1 ⊗ₜ[R] f X)).comp (mapRingHom (algebraMap R p.ResidueField)))

Tactic:
have : ((aeval (1 ⊗ₜ[R] f X : p.Fiber S)).restrictScalars R).comp
        (mapAlgHom (Algebra.ofId R p.ResidueField)) =
        Algebra.TensorProduct.includeRight.comp f := by ext; simp

Goal state after:
case refine_2
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
this :
  (AlgHom.restrictScalars R (aeval (1 ⊗ₜ[R] f X))).comp (mapAlgHom (Algebra.ofId R p.ResidueField)) =
    Algebra.TensorProduct.includeRight.comp f
⊢ RingHom.ker ↑f ≤ RingHom.ker ((aeval (1 ⊗ₜ[R] f X)).comp (mapRingHom (algebraMap R p.ResidueField)))