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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra R S
I : Ideal S
f : A →ₐ[R] S ⧸ I
inst✝ : FormallySmooth R A
m : ℕ
T : Type u_3 := S ⧸ I ^ (m + 1 + 1)
J : Ideal T := Ideal.map (Ideal.Quotient.mkₐ R (I ^ (m + 1 + 1))) (I ^ (m + 1))
q : A →ₐ[R] T ⧸ J := (↑(DoubleQuot.quotQuotEquivQuotOfLEₐ R ⋯).symm).comp (liftAdicCompletionAux (m + 1))
⊢ J ^ (m + 1 + 1) = 0

Tactic:
← Ideal.map_pow,

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra R S
I : Ideal S
f : A →ₐ[R] S ⧸ I
inst✝ : FormallySmooth R A
m : ℕ
T : Type u_3 := S ⧸ I ^ (m + 1 + 1)
J : Ideal T := Ideal.map (Ideal.Quotient.mkₐ R (I ^ (m + 1 + 1))) (I ^ (m + 1))
q : A →ₐ[R] T ⧸ J := (↑(DoubleQuot.quotQuotEquivQuotOfLEₐ R ⋯).symm).comp (liftAdicCompletionAux (m + 1))
⊢ Ideal.map (Ideal.Quotient.mkₐ R (I ^ (m + 1 + 1))) ((I ^ (m + 1)) ^ (m + 1 + 1)) = 0
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
P : PreSubmersivePresentation R S ι σ
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
i j : σ
⊢ P.jacobiMatrix i j = (pderiv (P.map i)) (P.relation j)

Tactic:
by
  simp [jacobiMatrix, LinearMap.toMatrix, differential, basis]

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
P : PreSubmersivePresentation R S ι σ
inst✝ : Finite σ
⊢ P.jacobian = LinearMap.det P.aevalDifferential

Tactic:
cases nonempty_fintype σ
  simp [← LinearMap.det_toMatrix', P.aevalDifferential_toMatrix'_eq_mapMatrix_jacobiMatrix,
    jacobian_eq_jacobiMatrix_det, RingHom.map_det, P.algebraMap_eq]

Goal state after:
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
σ : Type u_7
a : κ → ι
b : σ → ι
hg : Function.Surjective ⇑g
v : Basis ι R M
hainj : Function.Injective a
hsa : ∀ (i : κ), s (v (a i)) = 0
hlib : LinearIndependent R (⇑s ∘ ⇑v ∘ b)
hab : Codisjoint (Set.range a) (Set.range b)
k : κ
⊢ (ofSplitExact hs hfg hg v hainj hsa hlib hab) k = g (v (a k))

Tactic:
simp [ofSplitExact]

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

Goal state before:
pp: R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Finite σ
inst✝ : Finite ι
P : SubmersivePresentation R S ι σ
⊢ IsStandardSmooth R S

Tactic:
exact ⟨_, _, _, inferInstance, ⟨P.reindex (Fintype.equivFin _).symm (Fintype.equivFin _).symm⟩⟩

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

Goal state before:
pp: F : Type u
inst✝¹ : Field F
W : Projective F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z ≠ W.negY Q * P z
⊢ W.negDblY P / W.dblZ P =
    W.toAffine.negAddY (P x / P z) (Q x / Q z) (P y / P z)
      (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z))

Tactic:
negDblY_eq hP hPz,

Goal state after:
F : Type u
inst✝¹ : Field F
W : Projective F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z ≠ W.negY Q * P z
⊢ (-(eval P) W.polynomialX *
            ((eval P) W.polynomialX ^ 2 - W.a₁ * (eval P) W.polynomialX * P z * (P y - W.negY P) -
                  W.a₂ * P z ^ 2 * (P y - W.negY P) ^ 2 -
                2 * P x * P z * (P y - W.negY P) ^ 2 -
              P x * P z * (P y - W.negY P) ^ 2) +
          P y * P z ^ 2 * (P y - W.negY P) ^ 3) /
        P z ^ 2 /
      W.dblZ P =
    W.toAffine.negAddY (P x / P z) (Q x / Q z) (P y / P z)
      (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z))
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✝ : Smooth R S
f : (p : Ideal S) → [inst : p.IsPrime] → [IsSmoothAt R p] → S
hf₁ : ∀ (p : Ideal S) [inst : p.IsPrime] [inst_1 : IsSmoothAt R p], f p ∉ p
hf₂ : ∀ (p : Ideal S) [inst : p.IsPrime] [inst_1 : IsSmoothAt R p], IsStandardSmooth R (Localization.Away (f p))
⊢ ∀ x ∈ Set.range fun p ↦ f p.asIdeal, IsStandardSmooth R (Localization.Away x)

Tactic:
simp only [Set.mem_range, forall_exists_index, forall_apply_eq_imp_iff]

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Smooth R S
f : (p : Ideal S) → [inst : p.IsPrime] → [IsSmoothAt R p] → S
hf₁ : ∀ (p : Ideal S) [inst : p.IsPrime] [inst_1 : IsSmoothAt R p], f p ∉ p
hf₂ : ∀ (p : Ideal S) [inst : p.IsPrime] [inst_1 : IsSmoothAt R p], IsStandardSmooth R (Localization.Away (f p))
⊢ ∀ (a : PrimeSpectrum S), IsStandardSmooth R (Localization.Away (f a.asIdeal))
Module: Mathlib.RingTheory.Smooth.NoetherianDescent

Goal state before:
pp: 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
i : D.vars
⊢ ↑(D.q i).coeffs ⊆ Set.range ⇑(MvPolynomial.map (algebraMap (↥(subalgebra R D)) A))

Tactic:
intro q hq
  have : (q.coeffs : Set A) ⊆ ⋃ i, ⋃ x ∈ (D.q i).coeffs, ↑(coeffs x) :=
    Set.subset_iUnion_of_subset i (Set.subset_iUnion₂_of_subset q hq subset_rfl)
  #adaptation_note /-- Before https://github.com/leanprover/lean4/pull/13166
  (replacing grind's canonicalizer with a type-directed normalizer), `grind` closed this goal
  without the `rw`. It is not yet clear whether this is due to defeq abuse in Mathlib or a
  problem in the new canonicalizer; a minimization would help. The original proof was:
  `grind [MvPolynomial.mem_range_map_iff_coeffs_subset, subalgebra,
    Subalgebra.setRange_algebraMap, Algebra.subset_adjoin]` -/
  rw [MvPolynomial.mem_range_map_iff_coeffs_subset, Subalgebra.setRange_algebraMap]
  grind [subalgebra, Algebra.subset_adjoin]

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

Goal state before:
pp: case inl
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 (Sum.inl r) = Extension.Cotangent.mk ⟨D.pres.relation (Sum.inl r), ⋯⟩

Tactic:
basis_inl,

Goal state after:
case inl
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.cotangentEquivProd.symm (cMulXSubOneCotangent S D.gbar, 0) = Extension.Cotangent.mk ⟨D.pres.relation (Sum.inl r), ⋯⟩
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
⊢ ∃ g, g.Etale

Tactic:
let := Fintype.ofFinite
  obtain ⟨ι, σ, _, _, P, e⟩ :=
    Algebra.IsStandardSmoothOfRelativeDimension.out (R := R) (S := S) (n := n)
  let e₀ : σ ⊕ Fin n ≃ ι := ((Equiv.ofInjective _ P.map_inj).sumCongr
      (Finite.equivFinOfCardEq (by rw [Nat.card_coe_set_eq, Set.ncard_compl,
        Set.ncard_range_of_injective P.map_inj, ← e, Algebra.Presentation.dimension])).symm).trans
      (Equiv.Set.sumCompl _)
  let e : MvPolynomial σ (MvPolynomial (Fin n) R) ≃ₐ[R] P.Ring :=
    (MvPolynomial.sumAlgEquiv R _ _).symm.trans (MvPolynomial.renameEquiv _ e₀)
  let φ := e.toAlgHom.comp (IsScalarTower.toAlgHom _ (MvPolynomial (Fin n) R) _)
  algebraize [φ.toRingHom, (algebraMap P.Ring S).comp φ.toRingHom]
  have := IsScalarTower.of_algebraMap_eq' φ.comp_algebraMap.symm
  have : IsScalarTower R (MvPolynomial (Fin n) R) S := .to₁₂₄ _ _ P.Ring _
  refine ⟨IsScalarTower.toAlgHom _ _ _, ?_⟩
  have H : (MvPolynomial.aeval fun x ↦ (algebraMap P.Ring S) (e (MvPolynomial.X x))).toRingHom =
      (algebraMap P.Ring S).comp e.toRingHom := by
    ext
    · simp [e, IsScalarTower.algebraMap_eq R (MvPolynomial (Fin n) R) S]
    · simp [e, @RingHom.algebraMap_toAlgebra (MvPolynomial (Fin n) R) S, φ]
    · simp [e]
  let P' : Algebra.PreSubmersivePresentation (MvPolynomial (Fin n) R) S σ σ :=
  { toGenerators := .ofSurjective (algebraMap _ _ <| e <| .X ·) <| by
      convert! P.algebraMap_surjective.comp e.surjective
      exact congr($H)
    relation := e.symm ∘ P.relation
    span_range_relation_eq_ker := by
      rw [Set.range_comp, ← AlgEquiv.coe_ringEquiv e.symm, AlgEquiv.symm_toRingEquiv,
        ← Ideal.map_span, P.span_range_relation_eq_ker, Ideal.map_symm]
      exact congr(RingHom.ker $H).symm
    map := _
    map_inj := Function.injective_id }
  let P' : Algebra.SubmersivePresentation (MvPolynomial (Fin n) R) S σ σ :=
  { __ := P'
    jacobian_isUnit := by
      convert! P.jacobian_isUnit using 1
      simp_rw [Algebra.PreSubmersivePresentation.jacobian_eq_jacobiMatrix_det, map_det]
      congr 1
      ext i j
      trans algebraMap P.Ring S (e ((e.symm (P.relation j)).pderiv i))
      · simpa [Algebra.PreSubmersivePresentation.jacobiMatrix_apply, P',
          Algebra.Generators.ofSurjective] using congr($H _)
      suffices e ((e.symm (P.relation j)).pderiv i) = (P.relation j).pderiv (P.map i) by
        simp [Algebra.PreSubmersivePresentation.jacobiMatrix_apply, this]
      simp [e, ← MvPolynomial.pderiv_rename e₀.injective, show e₀ (Sum.inl i) = P.map i from rfl] }
  exact etale_algebraMap.mpr (Algebra.Etale.iff_isStandardSmoothOfRelativeDimension_zero.mpr
    ⟨_, _, _, inferInstance, P', by simp [Algebra.Presentation.dimension]⟩)

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

Goal state before:
pp: K : Type u_1
L : Type u_2
ι : Type u_3
inst✝⁴ : Field L
inst✝³ : Field K
inst✝² : Algebra K L
inst✝¹ : PerfectField K
inst✝ : EssFiniteType K L
s : Finset L
hs : IsTranscendenceBasis K Subtype.val
H : Algebra.IsSeparable (↥(IntermediateField.adjoin K ↑s)) L
⊢ Algebra.IsSeparable (↥(IntermediateField.adjoin K (Set.range Subtype.val))) L

Tactic:
convert! H

Goal state after:
case e'_1
K : Type u_1
L : Type u_2
ι : Type u_3
inst✝⁴ : Field L
inst✝³ : Field K
inst✝² : Algebra K L
inst✝¹ : PerfectField K
inst✝ : EssFiniteType K L
s : Finset L
hs : IsTranscendenceBasis K Subtype.val
H : Algebra.IsSeparable (↥(IntermediateField.adjoin K ↑s)) L
x✝ : L
⊢ Set.range Subtype.val = ↑s

case e'_3.e'_2
K : Type u_1
L : Type u_2
ι : Type u_3
inst✝⁴ : Field L
inst✝³ : Field K
inst✝² : Algebra K L
inst✝¹ : PerfectField K
inst✝ : EssFiniteType K L
s : Finset L
hs : IsTranscendenceBasis K Subtype.val
H : Algebra.IsSeparable (↥(IntermediateField.adjoin K ↑s)) L
e_1✝ : ↥(IntermediateField.adjoin K (Set.range Subtype.val)) = ↥(IntermediateField.adjoin K ↑s)
⊢ Set.range Subtype.val = ↑s

case e'_5
K : Type u_1
L : Type u_2
ι : Type u_3
inst✝⁴ : Field L
inst✝³ : Field K
inst✝² : Algebra K L
inst✝¹ : PerfectField K
inst✝ : EssFiniteType K L
s : Finset L
hs : IsTranscendenceBasis K Subtype.val
H : Algebra.IsSeparable (↥(IntermediateField.adjoin K ↑s)) L
e_1✝ : ↥(IntermediateField.adjoin K (Set.range Subtype.val)) = ↥(IntermediateField.adjoin K ↑s)
e_3✝ :
  (IntermediateField.adjoin K (Set.range Subtype.val)).toField.toCommRing ≍
    (IntermediateField.adjoin K ↑s).toField.toCommRing
⊢ Set.range Subtype.val = ↑s
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
a : ι → K
F : MvPolynomial ι k
HF : ∀ (F' : MvPolynomial ι k), F' ≠ 0 → (aeval a) F' = 0 → F.totalDegree ≤ F'.totalDegree
hFa : (aeval a) F = 0
i : ι
hi : i ∈ F.vars
⊢ IsAlgebraic (↥(Algebra.adjoin k (a '' {i}ᶜ))) (a i)

Tactic:
have ⟨σ, hσ, hσi⟩ := (mem_vars_iff_mem_support i).mp hi
  refine ⟨toPolynomialAdjoinImageCompl F a i,
    fun h ↦ coeff_toPolynomialAdjoinImageCompl_ne_zero HF σ hσ i
      (Finsupp.mem_support_iff.mp hσi) ?_, aeval_toPolynomialAdjoinImageCompl_eq_zero hFa ..⟩
  rw [h, Polynomial.coeff_zero]

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ @Etale = affineLocally fun {R S} [CommRing R] [CommRing S] ↦ RingHom.Etale

Tactic:
by
    ext X Y f
    rw [etale_iff, affineLocally_iff_forall_isAffineOpen]

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

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

pp: X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
inst✝¹ : FormallyUnramified f
inst✝ : LocallyOfFiniteType f
hX : (∃ S, X = Spec S) ∧ ∃ R, Y = Spec R
⊢ IsOpenImmersion (pullback.diagonal f)

Tactic:
· let 𝒰Y := Y.affineCover
    let 𝒰X (j : (Y.affineCover.pullback₁ f).I₀) :
        ((Y.affineCover.pullback₁ f).X j).OpenCover := Scheme.affineCover _
    apply IsZariskiLocalAtTarget.of_range_subset_iSup _
      (Scheme.Pullback.range_diagonal_subset_diagonalCoverDiagonalRange f 𝒰Y 𝒰X)
    intro ⟨i, j⟩
    rw [arrow_mk_iso_iff (P := @IsOpenImmersion)
      (Scheme.Pullback.diagonalRestrictIsoDiagonal f 𝒰Y 𝒰X i j)]
    have hu : FormallyUnramified ((𝒰X i).f j ≫ pullback.snd f (𝒰Y.f i)) :=
      comp_mem _ _ _ inferInstance (pullback_snd _ _ inferInstance)
    have hfin : LocallyOfFiniteType ((𝒰X i).f j ≫ pullback.snd f (𝒰Y.f i)) :=
      comp_mem _ _ _ inferInstance (pullback_snd _ _ inferInstance)
    exact this _ ⟨⟨_, rfl⟩, ⟨_, rfl⟩⟩

Goal state after:
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
inst✝¹ : FormallyUnramified f
inst✝ : LocallyOfFiniteType f
hX : (∃ S, X = Spec S) ∧ ∃ R, Y = Spec R
⊢ IsOpenImmersion (pullback.diagonal f)
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
hx : P x * Q z = Q x * P z
⊢ ![0, W.addY P Q, W.addZ P Q] = addU P Q • ![0, 1, 0]

Tactic:
addY_of_X_eq hP hQ hPz hQz hx,

Goal state after:
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
hx : P x * Q z = Q x * P z
⊢ ![0, addU P Q, W.addZ P Q] = addU P Q • ![0, 1, 0]
Module: Mathlib.AlgebraicGeometry.Morphisms.Descent

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

Tactic:
wlog hZ : ∃ R, Z = Spec R generalizing X Y Z

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
⊢ P g

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)
hZ : ∃ R, Z = Spec R
⊢ P g
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Descent

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : FaithfullyFlat R S
H : Function.Surjective ⇑(algebraMap S (S ⊗[R] T))
⊢ Function.Surjective ⇑(algebraMap R T)

Tactic:
by
  have : LinearMap.lTensor S (Algebra.linearMap R T) =
      Algebra.linearMap S (S ⊗[R] T) ∘ₗ (AlgebraTensorModule.rid R S S).toLinearMap := by
    ext; simp
  apply (Module.FaithfullyFlat.lTensor_surjective_iff_surjective R S (Algebra.linearMap R T)).mp
  simpa [this] using! H

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

Goal state before:
pp: P P' : MorphismProperty Scheme
inst✝³ : P'.IsStableUnderBaseChange
inst✝² : P'.IsStableUnderComposition
inst✝¹ : P.IsStableUnderBaseChange
H₁ : @IsLocalIso ⊓ @Surjective ≤ P'
inst✝ : IsZariskiLocalAtTarget P
H :
  ∀ {R S : CommRingCat} {Y : Scheme} (φ : R ⟶ S) (g : Y ⟶ Spec R),
    P' (Spec.map φ) → P (pullback.fst (Spec.map φ) g) → P g
⊢ P.DescendsAlong (P' ⊓ @QuasiCompact)

Tactic:
by
  apply IsZariskiLocalAtTarget.descendsAlong
  intro R X Y f g hf h
  wlog hX : ∃ T, X = Spec T generalizing X
  · have _ : CompactSpace X := by simpa [← quasiCompact_iff_compactSpace f] using hf.2
    obtain ⟨Y, p, hsurj, hP', hY⟩ := X.exists_hom_isAffine_of_isZariskiLocalAtSource @IsLocalIso
    refine this (f := (Y.isoSpec.inv ≫ p) ≫ f) ?_ ?_ ⟨_, rfl⟩
    · rw [Category.assoc, (P' ⊓ @QuasiCompact).cancel_left_of_respectsIso]
      exact ⟨P'.comp_mem _ _ (H₁ _ ⟨hP', hsurj⟩) hf.1, inferInstance⟩
    · rw [← pullbackRightPullbackFstIso_inv_fst f g _, P.cancel_left_of_respectsIso]
      exact P.pullback_fst _ _ h
  obtain ⟨T, rfl⟩ := hX
  obtain ⟨φ, rfl⟩ := Spec.map_surjective f
  exact H φ g hf.1 h

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
b : R
hb' : b ∈ R⁰
hb : ∀ i < (minpoly R s).natDegree, b • s ^ i ∈ (algebraMap R S).range
n : ℕ
⊢ b • s ^ n ∈ (algebraMap R S).range

Tactic:
induction n using Nat.strong_induction_on with

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

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

Tactic:
nth_rw 1 [RatFunc.X, ← aeval_X_left_apply p (R := K)]

Goal state after:
K : Type u_1
inst✝¹ : Field K
Γ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
hv : IsTrivialOn K v
hlt : 1 < v RatFunc.X
p✝ : K[X]
hp : p✝ ≠ 0
p : K[X]
⊢ ↑((aeval X) p) = (aeval ((algebraMap K[X] K⟮X⟯) X)) p
Module: Mathlib.RingTheory.Polynomial.IsIntegral

Goal state before:
pp: R✝ : Type u_1
S : Type u_2
ι : Type u_3
inst✝⁵ : CommRing R✝
inst✝⁴ : CommRing S
inst✝³ : Algebra R✝ S
R : Type u_4
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsIntegrallyClosed R
⊢ IsIntegrallyClosed R[X]

Tactic:
let K := FractionRing R

Goal state after:
R✝ : Type u_1
S : Type u_2
ι : Type u_3
inst✝⁵ : CommRing R✝
inst✝⁴ : CommRing S
inst✝³ : Algebra R✝ S
R : Type u_4
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsIntegrallyClosed R
K : Type u_4 := FractionRing R
⊢ IsIntegrallyClosed R[X]
Module: Mathlib.RingTheory.QuasiFinite.Weakly

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
p : Ideal S
inst✝² : p.IsPrime
inst✝¹ : QuasiFinite R (Localization.AtPrime p ⧸ Ideal.map (algebraMap R (Localization.AtPrime p)) (Ideal.under R p))
q : Ideal T
inst✝ : q.IsPrime
f : Localization.AtPrime p →ₐ[R] Localization.AtPrime q
hf : Function.Surjective ⇑f
⊢ Ideal.under R p ≤
    Ideal.comap (algebraMap R (Localization.AtPrime q))
      (Ideal.map (algebraMap R (Localization.AtPrime q)) (Ideal.under R q))

Tactic:
grw [← Ideal.le_comap_map]

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
p : Ideal S
inst✝² : p.IsPrime
inst✝¹ : QuasiFinite R (Localization.AtPrime p ⧸ Ideal.map (algebraMap R (Localization.AtPrime p)) (Ideal.under R p))
q : Ideal T
inst✝ : q.IsPrime
f : Localization.AtPrime p →ₐ[R] Localization.AtPrime q
hf : Function.Surjective ⇑f
⊢ Ideal.under R p ≤ Ideal.under R q
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 σ
f : MvPolynomial PEmpty.{w + 1} S
H : (algebraMap (MvPolynomial PEmpty.{w + 1} R) (MvPolynomial PEmpty.{w + 1} S)).IsIntegralElem f
n : PEmpty.{w + 1} →₀ ℕ
⊢ (((isEmptyAlgEquiv S PEmpty.{?u.255 + 1}).symm.toRingEquiv.toRingHom.comp (algebraMap R S)).comp
        (isEmptyAlgEquiv R PEmpty.{?u.275 + 1}).toRingEquiv.toRingHom).IsIntegralElem
    ((isEmptyAlgEquiv S PEmpty.{?u.255 + 1}).symm.toRingEquiv.toRingHom (coeff n f))

Tactic:
convert! H

Goal state after:
case e'_5
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type w
hσ : Finite σ
f : MvPolynomial PEmpty.{w + 1} S
H : (algebraMap (MvPolynomial PEmpty.{w + 1} R) (MvPolynomial PEmpty.{w + 1} S)).IsIntegralElem f
n : PEmpty.{w + 1} →₀ ℕ
⊢ ((isEmptyAlgEquiv S PEmpty.{w + 1}).symm.toRingEquiv.toRingHom.comp (algebraMap R S)).comp
      (isEmptyAlgEquiv R PEmpty.{w + 1}).toRingEquiv.toRingHom =
    algebraMap (MvPolynomial PEmpty.{w + 1} R) (MvPolynomial PEmpty.{w + 1} S)

case e'_6
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type w
hσ : Finite σ
f : MvPolynomial PEmpty.{w + 1} S
H : (algebraMap (MvPolynomial PEmpty.{w + 1} R) (MvPolynomial PEmpty.{w + 1} S)).IsIntegralElem f
n : PEmpty.{w + 1} →₀ ℕ
⊢ (isEmptyAlgEquiv S PEmpty.{w + 1}).symm.toRingEquiv.toRingHom (coeff n f) = f