mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.AdicCompletion.Functoriality

Goal state before:
pp: case succ
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
h : Function.Surjective ⇑((I • ⊤).mkQ ∘ₗ f)
y : AdicCompletion I N
n : ℕ
xn : { m // Submodule.Quotient.mk (f m) = (eval I N n) y }
⊢ { m // Submodule.Quotient.mk (f m) = (eval I N (n + 1)) y }

Tactic:
choose z hz using exists_smodEq_pow_smul_top_and_mkQ_eq h
          (y' := eval _ _ (n + 1) y) (by simp) xn.2

Goal state after:
case succ
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
h : Function.Surjective ⇑((I • ⊤).mkQ ∘ₗ f)
y : AdicCompletion I N
n : ℕ
xn : { m // Submodule.Quotient.mk (f m) = (eval I N n) y }
z : M
hz : ↑xn ≡ z [SMOD I ^ n • ⊤] ∧ (I ^ (n + 1) • ⊤).mkQ (f z) = (eval I N (n + 1)) y
⊢ { m // Submodule.Quotient.mk (f m) = (eval I N (n + 1)) y }
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
ι' : 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✝¹ : Fintype σ
inst✝ : Fintype σ'
i j : σ
⊢ (Q.comp P).jacobiMatrix (Sum.inr i) (Sum.inr j) = (rename Sum.inr) (P.jacobiMatrix i j)

Tactic:
rw [jacobiMatrix_apply, jacobiMatrix_apply]

Goal state after:
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✝¹ : Fintype σ
inst✝ : Fintype σ'
i j : σ
⊢ (pderiv ((Q.comp P).map (Sum.inr i))) ((Q.comp P).relation (Sum.inr j)) =
    (rename Sum.inr) ((pderiv (P.map i)) (P.relation j))
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
p q : Submodule R M
hpq : IsCompl p q
hker : Disjoint g.ker q
hmap : map g q = ⊤
⊢ Function.Bijective ⇑(p.projectionOnto q hpq ∘ₗ f)

Tactic:
by
  refine ⟨?_, Submodule.projectionOnto_comp_surjective_of_exact hfg _ hmap⟩
  rwa [LinearMap.coe_comp, Set.InjOn.injective_iff ↑(LinearMap.range f) _ subset_rfl]
  simpa [← LinearMap.disjoint_ker_iff_injOn, ← hfg.linearMap_ker_eq]

Goal state after:
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
P : Presentation 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₀
⊢ ∀ a ∈ Ideal.span (Set.range (relationOfHasCoeffs R₀)), (MvPolynomial.aeval P.val) a = 0

Tactic:
simp_rw [← RingHom.mem_ker, ← SetLike.le_def, Ideal.span_le]
      rintro a ⟨i, rfl⟩
      simp

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Nontrivial S
inst✝ : IsStandardSmooth R S
n : ℕ
⊢ IsStandardSmoothOfRelativeDimension n R S ↔ Module.rank S Ω[S⁄R] = ↑n

Tactic:
refine ⟨fun h ↦ IsStandardSmoothOfRelativeDimension.rank_kaehlerDifferential _, fun h ↦ ?_⟩

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Nontrivial S
inst✝ : IsStandardSmooth R S
n : ℕ
h : Module.rank S Ω[S⁄R] = ↑n
⊢ IsStandardSmoothOfRelativeDimension n R S
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Equation P
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z = Q y * P z
hy' : P y * Q z = W.negY Q * P z
⊢ ![0, W.dblY P, W.dblZ P] = W.dblU P • ![0, 1, 0]

Tactic:
dblY_of_Y_eq hP hPz hQz hx hy hy',

Goal state after:
F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Equation P
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z = Q y * P z
hy' : P y * Q z = W.negY Q * P z
⊢ ![0, W.dblU P, W.dblZ P] = W.dblU P • ![0, 1, 0]
Module: Mathlib.RingTheory.Extension.Cotangent.Free

Goal state before:
pp: case hli
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 : PreSubmersivePresentation R S ι σ
inst✝ : Finite σ
b : Module.Basis σ S P.toExtension.Cotangent
hb : ∀ (r : σ), b r = Extension.Cotangent.mk ⟨P.relation r, ⋯⟩
h : Function.Bijective ⇑(P.cotangentRestrict ⋯)
heq :
  (fun j i ↦ (aeval P.val) ((pderiv (P.map i)) (P.relation j))) =
    ⇑(Finsupp.linearEquivFunOnFinite S S σ) ∘ ⇑(P.cotangentRestrict ⋯) ∘ ⇑b
⊢ LinearIndependent S fun j i ↦ (aeval P.val) ((pderiv (P.map i)) (P.relation j))

Tactic:
rw [heq]

Goal state after:
case hli
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 : PreSubmersivePresentation R S ι σ
inst✝ : Finite σ
b : Module.Basis σ S P.toExtension.Cotangent
hb : ∀ (r : σ), b r = Extension.Cotangent.mk ⟨P.relation r, ⋯⟩
h : Function.Bijective ⇑(P.cotangentRestrict ⋯)
heq :
  (fun j i ↦ (aeval P.val) ((pderiv (P.map i)) (P.relation j))) =
    ⇑(Finsupp.linearEquivFunOnFinite S S σ) ∘ ⇑(P.cotangentRestrict ⋯) ∘ ⇑b
⊢ LinearIndependent S (⇑(Finsupp.linearEquivFunOnFinite S S σ) ∘ ⇑(P.cotangentRestrict ⋯) ∘ ⇑b)
Module: Mathlib.RingTheory.Smooth.StandardSmoothOfFree

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
inst✝ : Subsingleton (H1Cotangent R S)
I : Type u_3
b : Module.Basis I S Ω[S⁄R]
hb : Set.range ⇑b ⊆ Set.range ⇑(D R S)
⊢ IsStandardSmooth R S

Tactic:
nontriviality S
  obtain ⟨n, ⟨P⟩⟩ := (FiniteType.iff_exists_generators (R := R) (S := S)).mp inferInstance
  choose f' hf' using hb
  let P := P.extend fun i ↦ f' ⟨i, rfl⟩
  have hb (i : I) : b i = D R S (P.val (Sum.inr i)) := by simp [P, hf']
  have : Function.Bijective (P.cotangentRestrict _) :=
    P.cotangentRestrict_bijective_of_basis_kaehlerDifferential Sum.inl_injective
      Set.isCompl_range_inl_range_inr.symm b hb
  let bcot' : Module.Basis (Fin n) S P.toExtension.Cotangent :=
    .ofRepr (.ofBijective (P.cotangentRestrict _) this)
  have : Finite I := Module.Finite.finite_basis b
  obtain ⟨Q, bcot, hcomp, hbcot⟩ := P.exists_presentation_of_basis_cotangent bcot'
  let P' : PreSubmersivePresentation R S (Unit ⊕ Fin n ⊕ I) (Unit ⊕ Fin n) :=
    { __ := Q
      map := Sum.map _root_.id Sum.inl
      map_inj := Sum.map_injective.mpr ⟨fun _ _ h ↦ h, Sum.inl_injective⟩ }
  have hcompl : IsCompl (Set.range (Sum.inr ∘ Sum.inr)) (Set.range P'.map) := by
    simp [P', ← eq_compl_iff_isCompl, Set.ext_iff, Set.mem_compl_iff]
  have hbij : Function.Bijective (P'.cotangentRestrict P'.map_inj) := by
    apply P'.cotangentRestrict_bijective_of_basis_kaehlerDifferential P'.map_inj hcompl b
    intro k
    simp only [hb, ← hcomp, P', Function.comp_def]
  let P'' : SubmersivePresentation R S _ _ :=
    ⟨P', P'.isUnit_jacobian_of_cotangentRestrict_bijective bcot hbcot hbij⟩
  exact P''.isStandardSmooth

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
hP : W'.Equation P
hPz : P z = 0
⊢ W'.addZ P Q = P y ^ 2 * Q z * Q z

Tactic:
rw [addZ, hPz, X_eq_zero_of_Z_eq_zero hP hPz]
  ring1

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))
⊢ ⇑(aeval P.val) = ⇑(algebraMap P.Ring S)

Tactic:
simp [P.algebraMap_eq]

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
⊢ W.negAddY P Q =
    ((P y * Q z - Q y * P z) *
          ((P y * Q z - Q y * P z) ^ 2 * P z * Q z +
                    W.a₁ * (P y * Q z - Q y * P z) * P z * Q z * (P x * Q z - Q x * P z) -
                  W.a₂ * P z * Q z * (P x * Q z - Q x * P z) ^ 2 -
                P x * Q z * (P x * Q z - Q x * P z) ^ 2 -
              Q x * P z * (P x * Q z - Q x * P z) ^ 2 -
            P x * Q z * (P x * Q z - Q x * P z) ^ 2) +
        P y * Q z * (P x * Q z - Q x * P z) ^ 3) /
      (P z * Q z) ^ 2

Tactic:
rw [← negAddY_eq' hP hQ, mul_div_cancel_right₀ _ <| pow_ne_zero 2 <| mul_ne_zero hPz hQz]

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
⊢ False

Tactic:
let e := (Equiv.optionSubtypeNe i).symm

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
⊢ False
Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth

Goal state before:
pp: X : Scheme
K : Type u
inst✝³ : Field K
inst✝² : PerfectField K
inst✝¹ : IsIntegral X
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : LocallyOfFinitePresentation f
this : (CommRingCat.Hom.hom (stalkMap f (genericPoint ↥X))).EssFiniteType
algInst✝ : Algebra ↑((Spec (CommRingCat.of K)).presheaf.stalk (f (genericPoint ↥X)))
  ↑(X.presheaf.stalk (genericPoint ↥X)) :=
  (CommRingCat.Hom.hom (stalkMap f (genericPoint ↥X))).toAlgebra
algebraizeInst✝ :
  Algebra.EssFiniteType ↑((Spec (CommRingCat.of K)).presheaf.stalk (f (genericPoint ↥X)))
    ↑(X.presheaf.stalk (genericPoint ↥X))
K' : CommRingCat := (Spec.structureSheaf K).presheaf.stalk (f (genericPoint ↥X))
⊢ (CommRingCat.Hom.hom (stalkMap f (genericPoint ↥X))).FormallySmooth

Tactic:
let e : K ≃ₐ[K] K' := IsLocalization.atUnits _ (f (genericPoint X)).asIdeal.primeCompl
      (fun x hx ↦ by aesop (add simp IsUnit.mem_submonoid_iff))

Goal state after:
X : Scheme
K : Type u
inst✝³ : Field K
inst✝² : PerfectField K
inst✝¹ : IsIntegral X
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : LocallyOfFinitePresentation f
this : (CommRingCat.Hom.hom (stalkMap f (genericPoint ↥X))).EssFiniteType
algInst✝ : Algebra ↑((Spec (CommRingCat.of K)).presheaf.stalk (f (genericPoint ↥X)))
  ↑(X.presheaf.stalk (genericPoint ↥X)) :=
  (CommRingCat.Hom.hom (stalkMap f (genericPoint ↥X))).toAlgebra
algebraizeInst✝ :
  Algebra.EssFiniteType ↑((Spec (CommRingCat.of K)).presheaf.stalk (f (genericPoint ↥X)))
    ↑(X.presheaf.stalk (genericPoint ↥X))
K' : CommRingCat := (Spec.structureSheaf K).presheaf.stalk (f (genericPoint ↥X))
e : K ≃ₐ[K] ↑K' := IsLocalization.atUnits (↑(CommRingCat.of K)) (f (genericPoint ↥X)).asIdeal.primeCompl ⋯
⊢ (CommRingCat.Hom.hom (stalkMap f (genericPoint ↥X))).FormallySmooth
Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified

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

pp: X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion (pullback.diagonal f)
hY : ∃ R, Y = Spec R
⊢ FormallyUnramified f

Tactic:
· 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⟩

Goal state after:
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion (pullback.diagonal f)
hY : ∃ R, Y = Spec R
⊢ 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
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
⊢ ∃ i, ∃ σ ∈ F.support, ¬p ∣ σ i

Tactic:
by_contra!
  have (σ) (hσ : σ ∈ F.support) : ∃ σ', σ = p • σ' := by
    choose σ' hσ' using (this · σ hσ)
    exact ⟨⟨σ.support, σ', by simp [hσ', hp.ne_zero]⟩, Finsupp.ext hσ'⟩
  choose! σ' hσ' using this
  have hσ'' (σ : F.support) : σ.1 = p • σ' σ := hσ' σ.1 σ.2
  classical
  replace H (ι : Type u_3) (_ : Fintype ι) (v : ι → K) (hv : LinearIndependent k v) :
      LinearIndependent k (v · ^ p) := by
    simpa only [Finset.coe_image, Finset.coe_univ, Set.image_univ, linearIndepOn_range_iff
      hv.injective] using! H (Finset.univ.image v) (by simpa using! hv.linearIndepOn_id)
  have := mt (H F.support inferInstance (fun s ↦ aeval a (monomial (σ' s) (1 : k)))) (by
    simp_rw [← map_pow, monomial_pow, ← hσ'', one_pow, not_linearIndependent_iff]
    refine ⟨.univ, (F.coeff ·), ?_, by simpa [MvPolynomial.eq_zero_iff] using! hF0⟩
    simp only [← map_smul, ← map_sum, Finset.univ_eq_attach, smul_eq_mul, mul_one]
    rw [F.support.sum_attach (fun i ↦ monomial i (F.coeff i)), support_sum_monomial_coeff, hFa])
  simp only [LinearIndependent, injective_iff_map_eq_zero, not_forall] at this
  obtain ⟨F', hF', hF'0⟩ := this
  let F'' : MvPolynomial ι k := .ofCoeff <| F'.mapDomain fun s ↦ σ' s.1
  have hF''0 : F'' ≠ 0 := ne_of_ne_of_eq (AddMonoidAlgebra.ofCoeff_eq_zero.ne.2 <|
    (Finsupp.mapDomain_injective fun s t h ↦ Subtype.ext
    (Finsupp.ext fun i ↦ by rw [hσ' _ s.2, hσ' _ t.2, h])).ne hF'0) (by simp)
  have hF'' : aeval a F'' = 0 := by
    have : (aeval a).toLinearMap ∘ₗ (AddMonoidAlgebra.coeffLinearEquiv _).symm.toLinearMap ∘ₗ
      Finsupp.lmapDomain k k (fun s : F.support ↦ σ' s) =
        (Finsupp.linearCombination k fun s : F.support ↦ aeval a (monomial (σ' s) (1 : k))) := by
      ext v; simp [monomial]
    simp only [← hF', F'', ← this]; rfl
  suffices hpm : p * F''.totalDegree ≤ F.totalDegree by
    have hF''0' : F''.totalDegree ≠ 0 := by
      contrapose hF''0
      rw [totalDegree_eq_zero_iff_eq_C.mp hF''0, aeval_C, map_eq_zero] at hF''
      rw [totalDegree_eq_zero_iff_eq_C.mp hF''0, hF'', map_zero]
    replace this := hpm.trans ((HF F'' hF''0 hF'').trans_eq (one_mul _).symm)
    exact hp.one_lt.not_ge ((mul_le_mul_iff_of_pos_right hF''0'.bot_lt).mp this)
  rw [totalDegree, Finset.mul_sup₀, Finset.sup_le_iff]
  intro σ hσ
  obtain ⟨σ, hσ₂, rfl⟩ := Finset.mem_image.mp (Finsupp.mapDomain_support hσ)
  refine le_trans ?_ (Finset.le_sup σ.2)
  conv_rhs => rw [hσ' _ σ.2, Finsupp.sum_smul_index (fun _ ↦ rfl), ← Finsupp.mul_sum]

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
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
⊢ ∃ i, (IsTranscendenceBasis k fun j ↦ a ↑j) ∧ IsSeparable (↥(adjoin k (a '' {i}ᶜ))) (a i)

Tactic:
by
  set S := {F : MvPolynomial ι k | F ≠ 0 ∧ F.aeval a = 0}
  obtain ⟨F, ⟨hF₀, hFa⟩, hFmin⟩ :
      ∃ F ∈ S, ∀ G : MvPolynomial ι k, G ≠ 0 → G.aeval a = 0 → totalDegree F ≤ totalDegree G := by
    suffices S.Nonempty from
      ⟨totalDegree.argminOn S this, totalDegree.argminOn_mem ..,
        fun _ h₁ h₂ ↦ totalDegree.argminOn_le S ⟨h₁, h₂⟩⟩
    suffices ¬ AlgebraicIndependent k a by simpa [S, algebraicIndependent_iff, and_comm] using! this
    intro h
    refine h.transcendental_adjoin (i := n) (s := {n}ᶜ) (by simp) ?_
    have : a '' {n}ᶜ = Set.range (ι := {i // i ≠ n}) (a ·) := by aesop
    convert! ha'.isAlgebraic.isAlgebraic _
  have hFirr : Irreducible F := irreducible_of_forall_totalDegree_le hFmin hF₀ hFa
  obtain ⟨i, σ, hσ, hi⟩ := exists_mem_support_not_dvd_of_forall_totalDegree_le p hp H hFmin hF₀ hFa
  have hσi : σ i ≠ 0 := by aesop
  have alg := isAlgebraic_of_mem_vars_of_forall_totalDegree_le hFmin hFa i <|
    (mem_vars_iff_mem_support i).mpr ⟨σ, hσ, by simpa⟩
  have Hi := ha'.of_isAlgebraic_adjoin_image_compl _ i _ alg
  refine ⟨i, Hi, ?_⟩
  let k' := adjoin k (a '' {i}ᶜ)
  have hF₁irr := irreducible_toPolynomialAdjoinImageCompl hFirr i Hi.1
  have := (AlgebraicIndepOn.aevalEquiv (s := {i}ᶜ) Hi.1).uniqueFactorizationMonoid inferInstance
  have coeff_ne := coeff_toPolynomialAdjoinImageCompl_ne_zero hFmin σ hσ i hσi
  open scoped algebraAdjoinAdjoin in
  have hF₂irr := (hF₁irr.isPrimitive fun h ↦ coeff_ne <| Polynomial.coeff_eq_zero_of_natDegree_lt <|
    h.trans_lt <| Nat.pos_iff_ne_zero.2 hσi).irreducible_iff_irreducible_map_fraction_map
    (K := k').1 hF₁irr
  contrapose coeff_ne with Hsep
  have : CharP k' p := (expChar_of_injective_algebraMap (algebraMap k k').injective p).casesOn
    (fun e ↦ (e rfl).elim) (fun _ _ _ ↦ ‹_›) hp.ne_one
  obtain ⟨g, hg, eq⟩ := (((minpoly k' (a i)).separable_or p (minpoly.irreducible
    (isAlgebraic_iff_isIntegral.mp <| isAlgebraic_adjoin_iff.mpr alg))).resolve_left Hsep).2
  replace eq := congr(Polynomial.coeff $eq (σ i))
  rwa [← minpoly.eq_of_irreducible hF₂irr ((Polynomial.aeval_map_algebraMap ..).trans
    (aeval_toPolynomialAdjoinImageCompl_eq_zero hFa i)), Polynomial.coeff_mul_C,
    Polynomial.coeff_expand hp.pos, if_neg hi, eq_mul_inv_iff_mul_eq₀
    (by simpa using hF₂irr.ne_zero), zero_mul, eq_comm,
    Polynomial.coeff_map, map_eq_zero_iff _ (FaithfulSMul.algebraMap_injective ..)] at eq

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Descent

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

Tactic:
rw [heq]

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

Goal state before:
pp: case inr
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
⊢ P g

Tactic:
IsZariskiLocalAtTarget.iff_of_openCover (P := P) Z.affineCover

Goal state after:
case inr
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), P (Scheme.Cover.pullbackHom Z.affineCover g i)
Module: Mathlib.RingTheory.IntegralClosure.GoingDown

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

Tactic:
← Units.eq_mul_inv_iff_mul_eq,

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

Tactic:
by linear_combination this

Goal state after: