mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.Sites.BigZariski

Goal state before:
pp: P : MorphismProperty Scheme
F : Schemeᵒᵖ ⥤ Type u_1
inst✝¹ : IsZariskiLocalAtSource P
hF : Presieve.IsSheaf zariskiTopology F
S : Scheme
𝒰 : Cover (precoverage P) S
inst✝ : Finite 𝒰.I₀
this✝ : PreservesLimitsOfShape (Discrete (𝒰.I₀ × 𝒰.I₀)) F
this : PreservesLimitsOfShape (Discrete 𝒰.I₀) F
c : Cofan 𝒰.X := Cofan.mk (∐ 𝒰.X) (Sigma.ι 𝒰.X)
⊢ Presieve.ofArrows 𝒰.sigma.X 𝒰.sigma.f = Presieve.singleton (Cofan.IsColimit.desc (coproductIsCoproduct 𝒰.X) 𝒰.f)

Tactic:
rw [← PreZeroHypercover.presieve₀, 𝒰.presieve₀_sigma]

Goal state after:
P : MorphismProperty Scheme
F : Schemeᵒᵖ ⥤ Type u_1
inst✝¹ : IsZariskiLocalAtSource P
hF : Presieve.IsSheaf zariskiTopology F
S : Scheme
𝒰 : Cover (precoverage P) S
inst✝ : Finite 𝒰.I₀
this✝ : PreservesLimitsOfShape (Discrete (𝒰.I₀ × 𝒰.I₀)) F
this : PreservesLimitsOfShape (Discrete 𝒰.I₀) F
c : Cofan 𝒰.X := Cofan.mk (∐ 𝒰.X) (Sigma.ι 𝒰.X)
⊢ Presieve.singleton (Sigma.desc 𝒰.f) = Presieve.singleton (Cofan.IsColimit.desc (coproductIsCoproduct 𝒰.X) 𝒰.f)
Module: Mathlib.RingTheory.RingHom.Smooth

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Bijective ⇑f
⊢ f.FormallySmooth

Tactic:
by
  algebraize [f]
  exact Algebra.FormallySmooth.of_equiv (AlgEquiv.ofBijective (Algebra.ofId R S) hf)

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.Functoriality

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
ι : Type u_6
M : ι → Type u_7
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
⊢ sumInv I M ∘ₗ sum I M = LinearMap.id

Tactic:
ext j x : 2
  apply DirectSum.ext_component (AdicCompletion I R) (fun i ↦ ?_)
  ext n
  simp only [LinearMap.coe_comp, Function.comp_apply, sum_lof, map_mk, component_sumInv,
    mk_apply_coe, AdicCauchySequence.map_apply_coe, Submodule.mkQ_apply, LinearMap.id_comp]
  rw [DirectSum.component.of, DirectSum.component.of]
  split
  · next h => subst h; simp
  · simp

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.Algebra

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m n : ℕ
hmn : m ≤ n
r : AdicCauchySequence I R
x : AdicCauchySequence I M
⊢ ↑r n • Submodule.Quotient.mk (↑x n) = ↑r m • Submodule.Quotient.mk (↑x m)

Tactic:
by
  rw [← Submodule.Quotient.mk_smul, ← Module.Quotient.mk_smul_mk,
    AdicCauchySequence.mk_eq_mk hmn, Ideal.mk_eq_mk I hmn, Module.Quotient.mk_smul_mk,
    Submodule.Quotient.mk_smul]

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.Algebra

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
r : AdicCompletion I R
x : M ⧸ I ^ n • ⊤
⊢ ↑r n • x = (evalₐ I n) r • x

Tactic:
induction r using induction_on; rfl

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
P : PreSubmersivePresentation R S ι σ
T : Type u_1
inst✝² : CommRing T
inst✝¹ : Algebra R T
e : S ≃ₐ[R] T
inst✝ : Finite σ
val✝ : Fintype σ
⊢ (algebraMap (P.ofAlgEquiv e).Ring T) (P.ofAlgEquiv e).jacobiMatrix.det = e ((algebraMap P.Ring S) P.jacobiMatrix.det)

Tactic:
simp only [ofAlgEquiv_toPresentation, Presentation.ofAlgEquiv_toGenerators,
    jacobiMatrix_ofAlgEquiv, Generators.algebraMap_apply, Generators.ofAlgEquiv_val,
    ← AlgHom.coe_coe e, MvPolynomial.comp_aeval_apply]

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
P : PreSubmersivePresentation R S ι σ
T : Type u_1
inst✝² : CommRing T
inst✝¹ : Algebra R T
e : S ≃ₐ[R] T
inst✝ : Finite σ
val✝ : Fintype σ
⊢ (aeval (⇑↑e ∘ P.val)) P.jacobiMatrix.det = (aeval fun i ↦ ↑e (P.val i)) P.jacobiMatrix.det
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
⊢ Etale R S ↔ IsStandardSmoothOfRelativeDimension 0 R S

Tactic:
refine ⟨fun h ↦ ?_, fun _ ↦ inferInstance⟩
  nontriviality S
  suffices h : IsStandardSmooth R S by
    simp [IsStandardSmoothOfRelativeDimension.iff_of_isStandardSmooth]
  rw [IsStandardSmooth.iff_exists_basis_kaehlerDifferential]
  refine ⟨inferInstance, ⟨Empty, Module.Basis.empty Ω[S⁄R], ?_⟩⟩
  simp [Set.range_subset_iff]

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Projective R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
⊢ W'.addZ P Q * (P z * Q z) = (P x * Q z - Q x * P z) ^ 3

Tactic:
by
  linear_combination (norm := (rw [addZ]; ring1))
    Q z ^ 3 * (equation_iff _).mp hP - P z ^ 3 * (equation_iff _).mp hQ

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_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
⊢ D.fhom.toAlgHom = AlgHom.id R P.Ring

Tactic:
ext : 1
  simp [fhom]

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

Goal state before:
pp: n m : ℕ
X Y : Scheme
f : X ⟶ Y
hf : Smooth f
⊢ LocallyOfFinitePresentation f

Tactic:
rw [HasRingHomProperty.eq_affineLocally @LocallyOfFinitePresentation]
  rw [HasRingHomProperty.eq_affineLocally @Smooth] at hf
  exact affineLocally_le (fun hf ↦ hf.finitePresentation) f hf

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
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.totalDegree ≤ ((rename Subtype.val) (F₀.coeff (σ i))).totalDegree
⊢ σ i ≤ ((renameEquiv k (Equiv.optionSubtypeNe i).symm) F).totalDegree

Tactic:
by
        rw [totalDegree_renameEquiv]
        exact (Finsupp.le_degree ..).trans (le_totalDegree hσ)

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'.negAddY P Q = P y ^ 2 * Q z * W'.negY Q

Tactic:
rw [negAddY, hPz, X_eq_zero_of_Z_eq_zero hP hPz, negY]

Goal state after:
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
⊢ -3 * 0 ^ 2 * Q x * Q y + 3 * 0 * Q x ^ 2 * P y - P y ^ 2 * Q y * Q z + P y * Q y ^ 2 * 0 + W'.a₁ * 0 * Q y ^ 2 * 0 -
                              W'.a₁ * Q x * P y ^ 2 * Q z -
                            W'.a₂ * 0 ^ 2 * Q y * Q z +
                          W'.a₂ * Q x ^ 2 * P y * 0 +
                        2 * W'.a₂ * 0 * Q x * P y * Q z -
                      2 * W'.a₂ * 0 * Q x * Q y * 0 -
                    W'.a₃ * P y ^ 2 * Q z ^ 2 +
                  W'.a₃ * Q y ^ 2 * 0 ^ 2 +
                W'.a₄ * 0 * P y * Q z ^ 2 -
              2 * W'.a₄ * 0 * Q y * 0 * Q z +
            2 * W'.a₄ * Q x * P y * 0 * Q z -
          W'.a₄ * Q x * Q y * 0 ^ 2 +
        3 * W'.a₆ * P y * 0 * Q z ^ 2 -
      3 * W'.a₆ * Q y * 0 ^ 2 * Q z =
    P y ^ 2 * Q z * (-Q y - W'.a₁ * Q x - W'.a₃ * Q z)
Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFinitePresentation f
⊢ IsOpen {x | (CommRingCat.Hom.hom (stalkMap f x)).FormallySmooth}

Tactic:
refine isOpen_iff_forall_mem_open.mpr fun x hx ↦ ?_
  obtain ⟨U, hU, V, hV, hVU, hxV, H⟩ := exists_smooth_of_formallySmooth_stalk f x hx
  algebraize [(f.appLE U V hVU).hom]
  exact ⟨V, fun y hy ↦ (formallySmooth_stalkMap_iff U hU V hV hVU hy).mpr
    (inferInstanceAs (Algebra.IsSmoothAt _ _)), V.2, hxV⟩

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
R S : CommRingCat
φ : R ⟶ S
inst✝ : IsOpenImmersion (pullback.diagonal (Spec.map φ))
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom φ).toAlgebra
F : TensorProduct ↑R ↑S ↑S →+* ↑S := (Algebra.TensorProduct.lmul' ↑R).toRingHom
hF : Function.Surjective ⇑F
this : IsOpenImmersion (Spec.map (CommRingCat.ofHom F))
e : ↑(CommRingCat.of (TensorProduct ↑R ↑S ↑S))
he : IsIdempotentElem e
he' : RingHom.ker (CommRingCat.Hom.hom (CommRingCat.ofHom F)) = Ideal.span {e}
x : ↑(CommRingCat.of (TensorProduct ↑R ↑S ↑S))
hx : e * x ∈ KaehlerDifferential.ideal ↑R ↑S
⊢ ↑⟨e * x, hx⟩ ∈ KaehlerDifferential.ideal ↑R ↑S ^ 2

Tactic:
rw [pow_two, Subtype.coe_mk, ← he, mul_assoc]

Goal state after:
X Y : Scheme
f : X ⟶ Y
R S : CommRingCat
φ : R ⟶ S
inst✝ : IsOpenImmersion (pullback.diagonal (Spec.map φ))
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom φ).toAlgebra
F : TensorProduct ↑R ↑S ↑S →+* ↑S := (Algebra.TensorProduct.lmul' ↑R).toRingHom
hF : Function.Surjective ⇑F
this : IsOpenImmersion (Spec.map (CommRingCat.ofHom F))
e : ↑(CommRingCat.of (TensorProduct ↑R ↑S ↑S))
he : IsIdempotentElem e
he' : RingHom.ker (CommRingCat.Hom.hom (CommRingCat.ofHom F)) = Ideal.span {e}
x : ↑(CommRingCat.of (TensorProduct ↑R ↑S ↑S))
hx : e * x ∈ KaehlerDifferential.ideal ↑R ↑S
⊢ e * (e * x) ∈ KaehlerDifferential.ideal ↑R ↑S * KaehlerDifferential.ideal ↑R ↑S
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: R : Type r
S : Type s
A : Type u
B : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
W' : Projective R
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
P : Fin 3 → A
⊢ (W'⁄B).dblXYZ (⇑f ∘ P) = ⇑f ∘ (W'⁄A).dblXYZ P

Tactic:
by
  rw [← RingHom.coe_coe, ← map_dblXYZ, map_baseChange]

Goal state after:
Module: Mathlib.RingTheory.Conductor

Goal state before:
pp: case refine_3
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
I : Ideal R
p : R
z : S
hp : p ∈ comap (algebraMap R S) (conductor R x)
l : R →₀ S
H : l ∈ Finsupp.supported S S ↑I
H' : (l.sum fun i a ↦ a • (algebraMap R S) i) = z
lem :
  ∀ {a : R},
    a ∈ I →
      l a • (algebraMap R S) a * (algebraMap R S) p ∈ ⇑(algebraMap (↥R[x]) S) '' ↑(Ideal.map (algebraMap R ↥R[x]) I)
y : R
hy : y ∈ l.support
⊢ (fun a c ↦ c • (algebraMap R S) a * (algebraMap R S) p) y (l y) ∈
    ⇑(algebraMap (↥R[x]) S) '' ↑(Ideal.map (algebraMap R ↥R[x]) I)

Tactic:
exact lem ((Finsupp.mem_supported _ l).mp H hy)

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

Goal state before:
pp: K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
p q : K[X]
⊢ RatFunc.mk p q =
    { toFractionRing := (algebraMap K[X] (FractionRing K[X])) p / (algebraMap K[X] (FractionRing K[X])) q }

Tactic:
RatFunc.mk

Goal state after:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
p q : K[X]
⊢ { toFractionRing := (algebraMap K[X] (FractionRing K[X])) p / (algebraMap K[X] (FractionRing K[X])) q } =
    { toFractionRing := (algebraMap K[X] (FractionRing K[X])) p / (algebraMap K[X] (FractionRing K[X])) q }
Module: Mathlib.RingTheory.Valuation.IsTrivialOn

Goal state before:
pp: Γ : Type u_1
inst✝³ : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst✝² : CommRing A
K : Type u_3
inst✝¹ : Field K
inst✝ : Algebra A K
v : Valuation K Γ
hv : IsTrivialOn A v
y : K
h0 : ¬y = 0
hy : ¬v y = 1
hlt : 1 < v y
this✝ : IsAlgebraic A y
p : A[X]
hpnt : p ≠ 0
hp : (aeval ((algebraMap K K) y)) p = 0
this : v y ^ p.natDegree = 0
⊢ False

Tactic:
by simp_all

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 ((algebraMap K[X] K⟮X⟯) X)) p

Tactic:
← 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.FieldTheory.RatFunc.AsPolynomial

Goal state before:
pp: case neg
K : Type u_1
inst✝¹ : Field K
Γ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
hv : IsTrivialOn K v
hle : v RatFunc.X ≤ 1
p : K[X]
i : ℕ
h0 : ¬p.coeff i = 0
⊢ i ∈ Finset.range (p.natDegree + 1) → v ↑((monomial i) (p.coeff i)) ≤ 1

Tactic:
simp_all [pow_le_one', ← RatFunc.algebraMap_eq_C, hv.eq_one _ h0]

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
p : R[X]
q : S[X]
hp : p.Monic
hq : q.Monic
H : q ∣ map (algebraMap R S) p
i : ℕ
a✝ : Nontrivial S
T : Type u_2
w✝⁴ : CommRing T
w✝³ : Algebra S T
w✝² : Module.Finite S T
w✝¹ : Module.Free S T
w✝ : Nontrivial T
hqT : (map (algebraMap S T) q).Splits
algInst✝ : Algebra R T := ((algebraMap S T).comp (algebraMap R S)).toAlgebra
scalarTowerInst✝ : IsScalarTower R S T := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R T))
x : T
hx : (map (algebraMap S T) q).IsRoot x
⊢ (aeval x) q = 0

Tactic:
by simp_all

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

Goal state before:
pp: case h
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsDomain R
inst✝ : FaithfulSMul R S
p✝ : S[X]
hp✝ : IsAlmostIntegral R[X] p✝
i : ℕ
q : S[X]
p : R[X]
hp : p ∈ R[X]⁰
hp' : ∀ (n : ℕ), p • q ^ n ∈ (algebraMap R[X] S[X]).range
n : ℕ
r : R[X]
hr : map (algebraMap R S) r = map (algebraMap R S) p * q ^ n
h' : q.leadingCoeff ^ n ≠ 0
h : ¬(map (algebraMap R S) p).leadingCoeff * q.leadingCoeff ^ n = 0
⊢ (map (algebraMap R S) p * q ^ n).leadingCoeff = (map (algebraMap R S) p).leadingCoeff * q.leadingCoeff ^ n

Tactic:
rw [← leadingCoeff_pow' h'] at h ⊢

Goal state after:
case h
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsDomain R
inst✝ : FaithfulSMul R S
p✝ : S[X]
hp✝ : IsAlmostIntegral R[X] p✝
i : ℕ
q : S[X]
p : R[X]
hp : p ∈ R[X]⁰
hp' : ∀ (n : ℕ), p • q ^ n ∈ (algebraMap R[X] S[X]).range
n : ℕ
r : R[X]
hr : map (algebraMap R S) r = map (algebraMap R S) p * q ^ n
h' : q.leadingCoeff ^ n ≠ 0
h : ¬(map (algebraMap R S) p).leadingCoeff * (q ^ n).leadingCoeff = 0
⊢ (map (algebraMap R S) p * q ^ n).leadingCoeff = (map (algebraMap R S) p).leadingCoeff * (q ^ n).leadingCoeff
Module: Mathlib.RingTheory.Polynomial.IsIntegral

Goal state before:
pp: case inr
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : S[X]
hp : IsIntegral R[X] p
i : ℕ
a✝¹ : Nontrivial R
a✝ : Nontrivial S
hp0 : p ≠ 0
q : R[X][X] := minpoly R[X] p
m : ℕ := (q.support.sup fun i ↦ (q.coeff i).natDegree) + p.natDegree + 1
hm₁ : ∀ (i : ℕ), (q.coeff i).natDegree < m
hm₁' : (eval (X ^ m) q).Monic
hm₂ : p.natDegree < m
h₀ : (algebraMap R[X] S[X]) X = X
this✝ : (Polynomial.map (algebraMap R[X] S[X]) ((taylor (X ^ m)) q)).IsRoot (p - X ^ m)
this : X ^ m - p ∣ Polynomial.map (algebraMap R S) (eval (X ^ m) q)
⊢ IsIntegral R (p.coeff i)

Tactic:
have := (isIntegral_coeff_of_dvd _ _ hm₁'
    ((monic_X_pow _).sub_of_left (by simpa [← natDegree_lt_iff_degree_lt, hp0])) this i).neg

Goal state after:
case inr
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : S[X]
hp : IsIntegral R[X] p
i : ℕ
a✝¹ : Nontrivial R
a✝ : Nontrivial S
hp0 : p ≠ 0
q : R[X][X] := minpoly R[X] p
m : ℕ := (q.support.sup fun i ↦ (q.coeff i).natDegree) + p.natDegree + 1
hm₁ : ∀ (i : ℕ), (q.coeff i).natDegree < m
hm₁' : (eval (X ^ m) q).Monic
hm₂ : p.natDegree < m
h₀ : (algebraMap R[X] S[X]) X = X
this✝¹ : (Polynomial.map (algebraMap R[X] S[X]) ((taylor (X ^ m)) q)).IsRoot (p - X ^ m)
this✝ : X ^ m - p ∣ Polynomial.map (algebraMap R S) (eval (X ^ m) q)
this : IsIntegral R (-(X ^ m - p).coeff i)
⊢ IsIntegral R (p.coeff i)
Module: Mathlib.RingTheory.QuasiFinite.Weakly

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
q : Ideal S
inst✝ : q.IsPrime
⊢ WeaklyQuasiFiniteAt R q ↔
    QuasiFinite R (Localization.AtPrime q ⧸ Ideal.map (algebraMap R (Localization.AtPrime q)) (Ideal.under R q))

Tactic:
let q' := q.map (Ideal.Quotient.mk ((q.under R).map (algebraMap R S)))

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
q : Ideal S
inst✝ : q.IsPrime
q' : Ideal (S ⧸ Ideal.map (algebraMap R S) (Ideal.under R q)) :=
  Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap R S) (Ideal.under R q))) q
⊢ WeaklyQuasiFiniteAt R q ↔
    QuasiFinite R (Localization.AtPrime q ⧸ Ideal.map (algebraMap R (Localization.AtPrime q)) (Ideal.under R q))
Module: Mathlib.RingTheory.QuasiFinite.Weakly

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P Q : Ideal S
inst✝² : P.IsPrime
inst✝¹ : Q.IsPrime
h₁ : P ≤ Q
h₂ : Ideal.under R P = Ideal.under R Q
inst✝ : WeaklyQuasiFiniteAt R Q
this : (Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap R S) (Ideal.under R Q))) P).IsPrime
⊢ Ideal.under R (Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap R S) (Ideal.under R Q))) P) =
    Ideal.under R (Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap R S) (Ideal.under R Q))) Q)

Tactic:
rw [← Ideal.under_under (B := S), ← Ideal.under_under (A := R) (B := S) (C := S ⧸ _)]
      dsimp [Ideal.under] at h₂ ⊢
      simp [Ideal.map_comap_le]
      simp [Ideal.map_comap_le, ← h₂]

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
x : ↥X
hx : QuasiFiniteAt f x
V : X.Opens
hV : IsAffineOpen V
U : Y.Opens
hU : IsAffineOpen U
hVU : V ≤ f ⁻¹ᵁ U
hxV : x ∈ V.carrier
algInst✝¹ : Algebra ↑Γ(Y, U) ↑Γ(X, V) := (CommRingCat.Hom.hom (appLE f U V hVU)).toAlgebra
algInst✝ : Algebra ↑(Y.presheaf.obj (Opposite.op U)) ↑(Y.presheaf.stalk (f x)) :=
  (CommRingCat.Hom.hom (Y.presheaf.germ U (f x) ⋯)).toAlgebra
this : IsLocalization.AtPrime (↑(Y.presheaf.stalk ↑⟨f x, ⋯⟩)) (hU.primeIdealOf ⟨f x, ⋯⟩).asIdeal
⊢ (algebraMap ↑(Y.presheaf.obj (Opposite.op U)) ↑(Y.presheaf.stalk (f x))).QuasiFinite

Tactic:
RingHom.quasiFinite_algebraMap

Goal state after:
X Y : Scheme
f : X ⟶ Y
x : ↥X
hx : QuasiFiniteAt f x
V : X.Opens
hV : IsAffineOpen V
U : Y.Opens
hU : IsAffineOpen U
hVU : V ≤ f ⁻¹ᵁ U
hxV : x ∈ V.carrier
algInst✝¹ : Algebra ↑Γ(Y, U) ↑Γ(X, V) := (CommRingCat.Hom.hom (appLE f U V hVU)).toAlgebra
algInst✝ : Algebra ↑(Y.presheaf.obj (Opposite.op U)) ↑(Y.presheaf.stalk (f x)) :=
  (CommRingCat.Hom.hom (Y.presheaf.germ U (f x) ⋯)).toAlgebra
this : IsLocalization.AtPrime (↑(Y.presheaf.stalk ↑⟨f x, ⋯⟩)) (hU.primeIdealOf ⟨f x, ⋯⟩).asIdeal
⊢ Algebra.QuasiFinite ↑(Y.presheaf.obj (Opposite.op U)) ↑(Y.presheaf.stalk (f x))
Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski

Goal state before:
pp: case e'_2.e'_1.e'_5.e'_3.e'_5.e'_3.e'_3
X : Scheme
D : Cover.RelativeGluingData (directedCover X) := ⋯
F : (directedCover X).I₀ ⥤ Scheme := ⋯
this : (D.functor ⋙ forget).IsLocallyDirected
U : (X.openCoverOfIsOpenCover (fun i ↦ ↑i) ⋯).toPreZeroHypercover.1
e_1✝ : (cocone X).pt.Opens = X.Opens
e_2✝³ :
  Preorder.smallCategory (TopologicalSpace.Opens ↥(cocone X).pt) ≍ Preorder.smallCategory (TopologicalSpace.Opens ↥X)
e_2✝² : ↑(cocone X).pt.toPresheafedSpace = ↑X.toPresheafedSpace
e_4✝ : (cocone X).pt.toPresheafedSpace = X.toPresheafedSpace
e_2✝¹ : (cocone X).pt.toLocallyRingedSpace = X.toLocallyRingedSpace
e_2✝ : (cocone X).pt = X
⊢ colimit.desc F (cocone X) = D.toBase

Tactic:
delta cocone

Goal state after:
case e'_2.e'_1.e'_5.e'_3.e'_5.e'_3.e'_3
X : Scheme
D : Cover.RelativeGluingData (directedCover X) := relativeGluingData ⋯
F : (directedCover X).I₀ ⥤ Scheme := D.functor
this : (D.functor ⋙ forget).IsLocallyDirected
U : (X.openCoverOfIsOpenCover (fun i ↦ ↑i) ⋯).toPreZeroHypercover.1
e_1✝ : (cocone X).pt.Opens = X.Opens
e_2✝³ :
  Preorder.smallCategory (TopologicalSpace.Opens ↥(cocone X).pt) ≍ Preorder.smallCategory (TopologicalSpace.Opens ↥X)
e_2✝² : ↑(cocone X).pt.toPresheafedSpace = ↑X.toPresheafedSpace
e_4✝ : (cocone X).pt.toPresheafedSpace = X.toPresheafedSpace
e_2✝¹ : (cocone X).pt.toLocallyRingedSpace = X.toLocallyRingedSpace
e_2✝ : (cocone X).pt = X
⊢ colimit.desc F { pt := X, ι := { app := fun U ↦ ⋯.fromSpec, naturality := ⋯ } } = D.toBase
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
x : ↥X
⊢ QuasiFiniteAt f x ↔ LocallyQuasiFinite (Spec.map (stalkMap f x) ≫ Y.fromSpecStalk (f x))

Tactic:
LocallyQuasiFinite.comp_iff,

Goal state after:
X Y : Scheme
f : X ⟶ Y
x : ↥X
⊢ QuasiFiniteAt f x ↔ LocallyQuasiFinite (Spec.map (stalkMap f x))
Module: Mathlib.RingTheory.Etale.StandardEtale

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : StandardEtalePair R
x : S
h : P.HasMap x
⊢ IsUnit ((aeval x) (derivative P.f))

Tactic:
obtain ⟨p₁, p₂, n, e⟩ := P.cond

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : StandardEtalePair R
x : S
h : P.HasMap x
p₁ p₂ : R[X]
n : ℕ
e : derivative P.f * p₁ + P.f * p₂ = P.g ^ n
⊢ IsUnit ((aeval x) (derivative P.f))
Module: Mathlib.RingTheory.Etale.StandardEtale

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : StandardEtalePair R
I : Ideal S
hI : I ^ 2 = ⊥
x : S
hx : P.HasMap ((Ideal.Quotient.mk I) x)
hf : (aeval x) P.f ∈ I
a : S
ha : (aeval x) P.g * a - 1 ∈ I
⊢ ∃! ε, ε ∈ I ∧ P.HasMap (x + ε)

Tactic:
obtain ⟨p₁, p₂, n, e⟩ := P.cond

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : StandardEtalePair R
I : Ideal S
hI : I ^ 2 = ⊥
x : S
hx : P.HasMap ((Ideal.Quotient.mk I) x)
hf : (aeval x) P.f ∈ I
a : S
ha : (aeval x) P.g * a - 1 ∈ I
p₁ p₂ : R[X]
n : ℕ
e : derivative P.f * p₁ + P.f * p₂ = P.g ^ n
⊢ ∃! ε, ε ∈ I ∧ P.HasMap (x + ε)
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝ : Field K
x : K⟮X⟯
⊢ (algebraMap K[X] K⟮X⟯) x.num / (algebraMap K[X] K⟮X⟯) x.denom = x

Tactic:
classical
  induction x using RatFunc.induction_on with | _ p q hq
  have q_div_ne_zero : q / gcd p q ≠ 0 := right_div_gcd_ne_zero hq
  rw [num_div p q, denom_div p hq, map_mul, map_mul, mul_div_mul_left,
    div_eq_div_iff, ← map_mul, ← map_mul, mul_comm _ q, ←
    EuclideanDomain.mul_div_assoc, ← EuclideanDomain.mul_div_assoc, mul_comm]
  · apply gcd_dvd_right
  · apply gcd_dvd_left
  · exact algebraMap_ne_zero q_div_ne_zero
  · exact algebraMap_ne_zero hq
  · refine algebraMap_ne_zero (mt Polynomial.C_eq_zero.mp ?_)
    exact inv_ne_zero (Polynomial.leadingCoeff_ne_zero.mpr q_div_ne_zero)

Goal state after:
Module: Mathlib.RingTheory.Etale.StandardEtale

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
P : StandardEtalePair R
⊢ IsUnit
    ((aeval ((algebraMap (AdjoinRoot P.f) (Localization.Away ((AdjoinRoot.mk P.f) P.g))) (AdjoinRoot.root P.f))) P.g)

Tactic:
rw [aeval_algebraMap_apply, AdjoinRoot.aeval_eq]

Goal state after:
case refine_2
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
P : StandardEtalePair R
⊢ IsUnit ((algebraMap (AdjoinRoot P.f) (Localization.Away ((AdjoinRoot.mk P.f) P.g))) ((AdjoinRoot.mk P.f) P.g))