mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ (-(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 /
      (P z * (P y - W.negY P) ^ 3) =
    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:
toAffine_slope_of_eq hPz hQz hx hy,

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 /
      (P z * (P y - W.negY P) ^ 3) =
    W.toAffine.negAddY (P x / P z) (Q x / Q z) (P y / P z) (-(eval P) W.polynomialX / P z / (P y - W.negY P))
Module: Mathlib.RingTheory.Extension.Cotangent.Basis

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FinitePresentation R S
α : Type u_4
P : Generators R S α
inst✝ : Finite α
σ : Type u_5
b₀ : Module.Basis σ S P.toExtension.Cotangent
h✝ : Nontrivial S
f : P.toExtension.Cotangent → ↥P.toExtension.ker
hf : ∀ (b : P.toExtension.Cotangent), Extension.Cotangent.mk (f b) = b
v : σ → ↥P.ker := fun i ↦ f (b₀ i)
J : Ideal P.Ring := Ideal.span (Set.range (Subtype.val ∘ v))
hJfg : P.ker.FG
hJ : J ≤ P.ker
⊢ P.ker • P.ker ≤ (Submodule.subtype P.ker).range

Tactic:
by simp [Ideal.mul_le_right]

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
x✝³ x✝² : Type u
x✝¹ : CommRing x✝³
x✝ : CommRing x✝²
⊢ (@Locally fun {R S} [CommRing R] [CommRing S] ↦ IsStandardSmooth) = @RingHom.Smooth

Tactic:
ext f

Goal state after:
X Y : Scheme
f✝ : X ⟶ Y
x✝⁷ x✝⁶ : Type u
x✝⁵ : CommRing x✝⁷
x✝⁴ : CommRing x✝⁶
f x✝³ : Type u
x✝² : CommRing f
x✝¹ : CommRing x✝³
x✝ : f →+* x✝³
⊢ Locally (fun {R S} [CommRing R] [CommRing S] ↦ IsStandardSmooth) x✝ ↔ x✝.Smooth
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Projective R
P Q : Fin 3 → R
u v : R
⊢ ![(u * v) ^ 2 * W'.addX P Q, (u * v) ^ 2 * W'.addY P Q, W'.addZ (u • P) (v • Q)] = (u * v) ^ 2 • W'.addXYZ P Q

Tactic:
addZ_smul,

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Projective R
P Q : Fin 3 → R
u v : R
⊢ ![(u * v) ^ 2 * W'.addX P Q, (u * v) ^ 2 * W'.addY P Q, (u * v) ^ 2 * W'.addZ P Q] = (u * v) ^ 2 • W'.addXYZ P Q
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent

Goal state before:
pp: ⊢ DescendsAlong (@UniversallyOpen) (@Surjective ⊓ @Flat ⊓ @QuasiCompact)

Tactic:
by
  refine IsZariskiLocalAtTarget.descendsAlong_inf_quasiCompact _ _ ?_ ?_
  · rw [inf_comm]
    exact inf_le_inf le_rfl (IsLocalIso.le_of_isZariskiLocalAtSource _)
  refine fun {R} S Y φ g ⟨_, _⟩ hfst ↦ ⟨universally_mk' _ _ fun {T} f _ s hs ↦ ?_⟩
  let p := pullback.fst (pullback.fst (Spec.map φ) f) (pullback.fst (Spec.map φ) g)
  let r : pullback (pullback.fst (Spec.map φ) f) (pullback.fst (Spec.map φ) g) ⟶ pullback f g :=
    pullback.map _ _ _ _ (pullback.snd _ _) (pullback.snd _ _) (Spec.map φ) (pullback.condition ..)
      (pullback.condition ..)
  have : IsOpen ((pullback.snd (Spec.map φ) f).base ⁻¹' ((pullback.fst f g).base '' s)) := by
    rw [← Scheme.image_preimage_eq_of_isPullback (isPullback_map_snd_snd ..)]
    exact p.isOpenMap _ (hs.preimage r.continuous)
  rwa [(Flat.isQuotientMap_of_surjective _).isOpen_preimage] at this

Goal state after:
Module: Mathlib.RingTheory.Conductor

Goal state before:
pp: 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)
z : S
hz : z ∈ R[x]
hy : ⟨z, hz⟩ ∈ comap (algebraMap (↥R[x]) S) (Ideal.map (algebraMap R S) I)
p : R
hp : p ∈ comap (algebraMap R S) (conductor R x)
q : R
hq : q ∈ I
hpq : p + q = 1
temp : (algebraMap R S) p * z + (algebraMap R S) q * z = z
this : z ∈ ⇑(algebraMap (↥R[x]) S) '' ↑(Ideal.map (algebraMap R ↥R[x]) I) ↔ ⟨z, hz⟩ ∈ Ideal.map (algebraMap R ↥R[x]) I
⊢ ⟨z, hz⟩ ∈ Ideal.map (algebraMap R ↥R[x]) I

Tactic:
rw [← this, ← temp]

Goal state after:
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)
z : S
hz : z ∈ R[x]
hy : ⟨z, hz⟩ ∈ comap (algebraMap (↥R[x]) S) (Ideal.map (algebraMap R S) I)
p : R
hp : p ∈ comap (algebraMap R S) (conductor R x)
q : R
hq : q ∈ I
hpq : p + q = 1
temp : (algebraMap R S) p * z + (algebraMap R S) q * z = z
this : z ∈ ⇑(algebraMap (↥R[x]) S) '' ↑(Ideal.map (algebraMap R ↥R[x]) I) ↔ ⟨z, hz⟩ ∈ Ideal.map (algebraMap R ↥R[x]) I
⊢ (algebraMap R S) p * z + (algebraMap R S) q * z ∈ ⇑(algebraMap (↥R[x]) S) '' ↑(Ideal.map (algebraMap R ↥R[x]) I)
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
n : ℕ
a : K
ha : a ≠ 0
⊢ v ↑((monomial n) a) = v RatFunc.X ^ n

Tactic:
simp_all [← RatFunc.algebraMap_eq_C, hv.eq_one]

Goal state after:
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
x : R
hx : x ∈ Ideal.under R p
hx' : x ∉ Ideal.under R q
this✝ : IsLocalHom f.toRingHom
this : IsUnit ((algebraMap R (Localization.AtPrime p)) x)
⊢ IsUnit (IsLocalization.mk' (Localization.AtPrime p) ((algebraMap R S) x) 1)

Tactic:
simpa [IsLocalization.mk'_one]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski

Goal state before:
pp: X : Scheme
U : X.AffineZariskiSite
S : Sieve U
⊢ Sieve.functorPushforward (toOpensFunctor X) S ∈ (Opens.grothendieckTopology ↥X) ((toOpensFunctor X).obj U) ↔
    ∀ x ∈ U.toOpens, ∃ V f, S.arrows f ∧ x ∈ V.toOpens

Tactic:
apply forall₂_congr fun x hxU ↦ ⟨?_, ?_⟩

Goal state after:
X : Scheme
U : X.AffineZariskiSite
S : Sieve U
x : ↥X
hxU : x ∈ (toOpensFunctor X).obj U
⊢ (∃ U_1 f, (Sieve.functorPushforward (toOpensFunctor X) S).arrows f ∧ x ∈ U_1) → ∃ V f, S.arrows f ∧ x ∈ V.toOpens

X : Scheme
U : X.AffineZariskiSite
S : Sieve U
x : ↥X
hxU : x ∈ (toOpensFunctor X).obj U
⊢ (∃ V f, S.arrows f ∧ x ∈ V.toOpens) → ∃ U_1 f, (Sieve.functorPushforward (toOpensFunctor X) S).arrows f ∧ x ∈ U_1
Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski

Goal state before:
pp: X : Scheme
F : X.AffineZariskiSiteᵒᵖ ⥤ CommRingCat
α : (toOpensFunctor X).op ⋙ X.presheaf ⟶ F
H : NatTrans.Coequifibered α
U : X.AffineZariskiSite
⊢ (relativeGluingData H).toBase ⁻¹ᵁ ↑U = Hom.opensRange ((relativeGluingData H).cover.f U)

Tactic:
simpa using! (relativeGluingData H).toBase_preimage_eq_opensRange_ι U

Goal state after:
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
p₁ p₂ : R[X]
n : ℕ
e : (aeval x) (derivative P.f) * (aeval x) p₁ + (aeval x) P.f * (aeval x) p₂ = (aeval x) P.g ^ n
⊢ (aeval x) (derivative P.f) * (a ^ n * (aeval x) p₁) - 1 =
    ((aeval x) P.g * a) ^ n - 1 - (aeval x) P.f * (a ^ n * (aeval x) p₂)

Tactic:
linear_combination a ^ n * e

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

Goal state before:
pp: 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
S : Type u_1
x✝¹ : CommRing S
x✝ : Algebra R S
I : Ideal S
hI : I ^ 2 = ⊥
⊢ Function.Bijective ((Ideal.Quotient.mkₐ R I).comp ∘ ⇑P.homEquiv.symm)

Tactic:
← P.homEquiv.bijective.of_comp_iff'

Goal state after:
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
S : Type u_1
x✝¹ : CommRing S
x✝ : Algebra R S
I : Ideal S
hI : I ^ 2 = ⊥
⊢ Function.Bijective (⇑P.homEquiv ∘ (Ideal.Quotient.mkₐ R I).comp ∘ ⇑P.homEquiv.symm)
Module: Mathlib.RingTheory.Unramified.LocalStructure

Goal state before:
pp: R : Type u_1
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
f : S
P : StandardEtalePair R
φ : P.Ring →ₐ[R] Localization.Away f
hsurj : Function.Surjective ⇑φ
g : S
a : P.Ring
ha : φ a = (algebraMap S (Localization.Away f)) g
⊢ HasStandardEtaleSurjectionOn R (f * g)

Tactic:
have : IsLocalization.Away (f * g) (Localization.Away (φ a)) :=
    ha ▸ .mul' (Localization.Away f) _ _ _

Goal state after:
R : Type u_1
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
f : S
P : StandardEtalePair R
φ : P.Ring →ₐ[R] Localization.Away f
hsurj : Function.Surjective ⇑φ
g : S
a : P.Ring
ha : φ a = (algebraMap S (Localization.Away f)) g
this : IsLocalization.Away (f * g) (Localization.Away (φ a))
⊢ HasStandardEtaleSurjectionOn R (f * g)
Module: Mathlib.RingTheory.Smooth.IntegralClosure

Goal state before:
pp: R : Type u_1
S : Type u_2
B : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : CommRing B
inst✝¹ : Algebra R B
M : Submonoid R
inst✝ : IsLocalization M S
φ : ↥(integralClosure R B) →ₐ[R] ↥(integralClosure S (S ⊗[R] B)) :=
  (Algebra.TensorProduct.includeRight.comp (integralClosure R B).val).codRestrict
    (Subalgebra.restrictScalars R (integralClosure S (S ⊗[R] B))) ⋯
⊢ Function.Bijective ⇑(toIntegralClosure R S B)

Tactic:
let := φ.toAlgebra

Goal state after:
R : Type u_1
S : Type u_2
B : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : CommRing B
inst✝¹ : Algebra R B
M : Submonoid R
inst✝ : IsLocalization M S
φ : ↥(integralClosure R B) →ₐ[R] ↥(integralClosure S (S ⊗[R] B)) :=
  (Algebra.TensorProduct.includeRight.comp (integralClosure R B).val).codRestrict
    (Subalgebra.restrictScalars R (integralClosure S (S ⊗[R] B))) ⋯
this : Algebra ↥(integralClosure R B) ↥(integralClosure S (S ⊗[R] B)) := φ.toAlgebra
⊢ Function.Bijective ⇑(toIntegralClosure R S B)
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
φ : R[X] →ₐ[R] S
t : S
p : R[X]
ht : φ.IsIntegralElem t
hp : φ p * t ∈ φ.range
a : R := p.leadingCoeff
R' : Type u_1 := Localization.Away a
S' : Type u_2 := Localization.Away ((algebraMap R S) a)
this✝ : Algebra R' S' := (Localization.awayMap (algebraMap R S) a).toAlgebra
this : IsScalarTower R R' S'
ha : IsUnit ((algebraMap R R') a)
H : (aeval ((algebraMap S S') (φ X))).comp (mapRingHom (algebraMap R R')) = (algebraMap S S').comp ↑φ
q : R'[X]
hq : IsIntegral R' ((algebraMap S S') t - (aeval ((algebraMap S S') (φ X))) q)
n : ℕ
q' : R[X]
e : map (algebraMap R R') q' = (fun x ↦ a ^ x) n • q
⊢ IsIntegral R' ((algebraMap S S') (a ^ n • t - φ q'))

Tactic:
have : algebraMap S S' (φ q') = (algebraMap R S' a) ^ n * aeval (algebraMap S S' (φ X)) q := by
      simpa [Algebra.smul_def, aeval_algebraMap_apply, aeval_algHom_apply, ← algebraMap_apply] using
        congr(aeval (algebraMap S S' (φ X)) $e)

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
φ : R[X] →ₐ[R] S
t : S
p : R[X]
ht : φ.IsIntegralElem t
hp : φ p * t ∈ φ.range
a : R := p.leadingCoeff
R' : Type u_1 := Localization.Away a
S' : Type u_2 := Localization.Away ((algebraMap R S) a)
this✝¹ : Algebra R' S' := (Localization.awayMap (algebraMap R S) a).toAlgebra
this✝ : IsScalarTower R R' S'
ha : IsUnit ((algebraMap R R') a)
H : (aeval ((algebraMap S S') (φ X))).comp (mapRingHom (algebraMap R R')) = (algebraMap S S').comp ↑φ
q : R'[X]
hq : IsIntegral R' ((algebraMap S S') t - (aeval ((algebraMap S S') (φ X))) q)
n : ℕ
q' : R[X]
e : map (algebraMap R R') q' = (fun x ↦ a ^ x) n • q
this : (algebraMap S S') (φ q') = (algebraMap R S') a ^ n * (aeval ((algebraMap S S') (φ X))) q
⊢ IsIntegral R' ((algebraMap S S') (a ^ n • t - φ q'))
Module: Mathlib.RingTheory.Unramified.LocalStructure

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
Q : Ideal S
inst✝² : Q.IsPrime
inst✝¹ : Module.Finite R S
inst✝ : IsUnramifiedAt R Q
this✝² : Algebra (Localization.AtPrime (Ideal.under R Q)) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R Q) Q
t : S
htQ : t ∉ Q
htQ' : ∀ Q' ∈ (Ideal.under R Q).primesOver S, Q' ≠ Q → t ∈ Q'
ht : (Ideal.under R Q).ResidueField[(algebraMap S Q.ResidueField) t] = ⊤
p : Ideal R := Ideal.under R Q
this✝¹ : Algebra (Localization.AtPrime p) (Localization.AtPrime (Ideal.under (↥R[t]) Q)) :=
  Localization.AtPrime.algebraOfLiesOver p (Ideal.under (↥R[t]) Q)
this✝ : Algebra (Localization.AtPrime (Ideal.under (↥R[t]) Q)) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under (↥R[t]) Q) Q
Q' : Ideal S
x✝ : Q' ∈ (Ideal.under (↥R[t]) Q).primesOver S
left✝ : Q'.IsPrime
right✝ : Q'.LiesOver (Ideal.under (↥R[t]) Q)
H : Q' ∉ {Q}
this : Q'.LiesOver p
⊢ False

Tactic:
exact htQ (SetLike.le_def.mp (Q'.over_def (Q.under (R[t]))).ge
      (x := ⟨t, self_mem_adjoin_singleton _ _⟩) (htQ' Q' ⟨‹_›, ‹_›⟩ H))

Goal state after:
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
⊢ NatTrans.Coequifibered ((toOpensFunctor Y).op.whiskerLeft (normalizationDiagramMap f))

Tactic:
refine coequifibered_iff_forall_isLocalizationAway.mpr fun U r ↦ ?_
  let : Algebra Γ(Y, U.1) Γ(X, f ⁻¹ᵁ U.1) := (f.app U.1).hom.toAlgebra
  let : Algebra Γ(Y, Y.basicOpen r) Γ(X, f ⁻¹ᵁ Y.basicOpen r) :=
    (f.app (U.basicOpen r).1).hom.toAlgebra
  let : Algebra (integralClosure Γ(Y, U.1) Γ(X, f ⁻¹ᵁ U.1))
      (integralClosure Γ(Y, Y.basicOpen r) Γ(X, f ⁻¹ᵁ Y.basicOpen r)) :=
    ((normalizationDiagram f).map (homOfLE (Y.basicOpen_le r)).op).hom.toAlgebra
  let inst : Algebra Γ(X, f ⁻¹ᵁ U.1) Γ(X, f ⁻¹ᵁ Y.basicOpen r) :=
    (X.presheaf.map (homOfLE (f.preimage_mono (Y.basicOpen_le r))).op).hom.toAlgebra
  have : IsLocalization.Away r Γ(Y, Y.basicOpen r) :=
    U.2.isLocalization_basicOpen _
  have : IsLocalization.Away ((algebraMap ↑Γ(Y, U.1) ↑Γ(X, f ⁻¹ᵁ U.1)) r)
      Γ(X, f ⁻¹ᵁ Y.basicOpen r) := by
    let : Algebra Γ(X, f ⁻¹ᵁ U.1) Γ(X, X.basicOpen (f.app _ r)) :=
      (X.presheaf.map (homOfLE (X.basicOpen_le _)).op).hom.toAlgebra
    dsimp +instances [inst]
    rw! (castMode := .all) [f.preimage_basicOpen r]
    exact isLocalization_basicOpen_of_qcqs (f.isCompact_preimage U.2.isCompact)
        (f.isQuasiSeparated_preimage U.2.isQuasiSeparated) (f.app _ r)
  change IsLocalization.Away ((algebraMap Γ(Y, U.1) (integralClosure Γ(Y, U.1) Γ(X, f ⁻¹ᵁ U.1))) r)
    (integralClosure Γ(Y, Y.basicOpen r) Γ(X, f ⁻¹ᵁ Y.basicOpen r))
  let : Algebra ↑Γ(Y, U.1) ↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) :=
    (f.appLE _ _ (f.preimage_mono (Y.basicOpen_le _))).hom.toAlgebra
  have : IsScalarTower Γ(Y, U.1) Γ(X, f ⁻¹ᵁ U.1) Γ(X, f ⁻¹ᵁ Y.basicOpen r) := .of_algebraMap_eq' rfl
  have : IsScalarTower Γ(Y, U.1) Γ(Y, Y.basicOpen r) Γ(X, f ⁻¹ᵁ Y.basicOpen r) :=
    .of_algebraMap_eq' <| by
      simp only [RingHom.algebraMap_toAlgebra, ← CommRingCat.hom_comp, Scheme.Hom.app_eq_appLE,
        Scheme.Hom.map_appLE, AffineZariskiSite.basicOpen]
  have : IsScalarTower (integralClosure Γ(Y, U.1) Γ(X, f ⁻¹ᵁ U.1))
    (integralClosure Γ(Y, Y.basicOpen r) Γ(X, f ⁻¹ᵁ Y.basicOpen r))
    Γ(X, f ⁻¹ᵁ Y.basicOpen r) := .of_algebraMap_eq' rfl
  have : IsScalarTower Γ(Y, U.1) (integralClosure Γ(Y, U.1) Γ(X, f ⁻¹ᵁ U.1))
    (integralClosure Γ(Y, Y.basicOpen r) Γ(X, f ⁻¹ᵁ Y.basicOpen r)) := .of_algebraMap_eq' rfl
  exact IsLocalization.Away.integralClosure r

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case succ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
r : R
m n k : ℕ
hk : k + m ≤ n
hf : f.natDegree ≤ m
hm : m ≠ 0
M₁ : Matrix (Fin (m + n)) (Fin (m + n)) R := f.sylvester (g + f * (monomial k) r) m n
M₂ : Matrix (Fin (m + n)) (Fin (m + n)) R := f.sylvester g m n
M : ℕ → Matrix (Fin (m + n)) (Fin (m + n)) R := fun i ↦ Matrix.of fun j₁ j₂ ↦ if ↑j₂ < i then M₁ j₁ j₂ else M₂ j₁ j₂
i : ℕ
IH : i ≤ m → (M i).det = M₂.det
hi : i + 1 ≤ m
j₁ j₂ : Fin (m + n)
⊢ (if ↑j₂ = i then M₁ j₁ ⟨i, ⋯⟩ - r * f.sylvester g m n j₁ ⟨i + (k + m), ⋯⟩
    else if ↑j₂ < i + 1 then M₁ j₁ j₂ else f.sylvester g m n j₁ j₂) =
    if ↑j₂ < i then M₁ j₁ j₂ else f.sylvester g m n j₁ j₂

Tactic:
obtain rfl | h := eq_or_ne ↑j₂ i

Goal state after:
case succ.inl
R : Type u_1
inst✝ : CommRing R
f g : R[X]
r : R
m n k : ℕ
hk : k + m ≤ n
hf : f.natDegree ≤ m
hm : m ≠ 0
M₁ : Matrix (Fin (m + n)) (Fin (m + n)) R := f.sylvester (g + f * (monomial k) r) m n
M₂ : Matrix (Fin (m + n)) (Fin (m + n)) R := f.sylvester g m n
M : ℕ → Matrix (Fin (m + n)) (Fin (m + n)) R := fun i ↦ Matrix.of fun j₁ j₂ ↦ if ↑j₂ < i then M₁ j₁ j₂ else M₂ j₁ j₂
j₁ j₂ : Fin (m + n)
IH : ↑j₂ ≤ m → (M ↑j₂).det = M₂.det
hi : ↑j₂ + 1 ≤ m
⊢ (if ↑j₂ = ↑j₂ then M₁ j₁ ⟨↑j₂, ⋯⟩ - r * f.sylvester g m n j₁ ⟨↑j₂ + (k + m), ⋯⟩
    else if ↑j₂ < ↑j₂ + 1 then M₁ j₁ j₂ else f.sylvester g m n j₁ j₂) =
    if ↑j₂ < ↑j₂ then M₁ j₁ j₂ else f.sylvester g m n j₁ j₂

case succ.inr
R : Type u_1
inst✝ : CommRing R
f g : R[X]
r : R
m n k : ℕ
hk : k + m ≤ n
hf : f.natDegree ≤ m
hm : m ≠ 0
M₁ : Matrix (Fin (m + n)) (Fin (m + n)) R := f.sylvester (g + f * (monomial k) r) m n
M₂ : Matrix (Fin (m + n)) (Fin (m + n)) R := f.sylvester g m n
M : ℕ → Matrix (Fin (m + n)) (Fin (m + n)) R := fun i ↦ Matrix.of fun j₁ j₂ ↦ if ↑j₂ < i then M₁ j₁ j₂ else M₂ j₁ j₂
i : ℕ
IH : i ≤ m → (M i).det = M₂.det
hi : i + 1 ≤ m
j₁ j₂ : Fin (m + n)
h : ↑j₂ ≠ i
⊢ (if ↑j₂ = i then M₁ j₁ ⟨i, ⋯⟩ - r * f.sylvester g m n j₁ ⟨i + (k + m), ⋯⟩
    else if ↑j₂ < i + 1 then M₁ j₁ j₂ else f.sylvester g m n j₁ j₂) =
    if ↑j₂ < i then M₁ j₁ j₂ else f.sylvester g m n j₁ j₂
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case succ.inl.right
R : Type u_1
inst✝ : CommRing R
f g : R[X]
r : R
m n k : ℕ
hk : k + m ≤ n
hf : f.natDegree ≤ m
hm : m ≠ 0
M₁ : Matrix (Fin (m + n)) (Fin (m + n)) R := f.sylvester (g + f * (monomial k) r) m n
M₂ : Matrix (Fin (m + n)) (Fin (m + n)) R := f.sylvester g m n
M : ℕ → Matrix (Fin (m + n)) (Fin (m + n)) R := fun i ↦ Matrix.of fun j₁ j₂ ↦ if ↑j₂ < i then M₁ j₁ j₂ else M₂ j₁ j₂
j₁ : Fin (m + n)
i : Fin n
IH : ↑(Fin.natAdd m i) ≤ m → (M ↑(Fin.natAdd m i)).det = M₂.det
hi : m + ↑i + 1 ≤ m
⊢ Fin.addCases
        (fun j₁_1 ↦
          if ↑j₁_1 ≤ ↑j₁ ∧ ↑j₁ ≤ ↑j₁_1 + n then g.coeff (↑j₁ - ↑j₁_1) + (f * (monomial k) r).coeff (↑j₁ - ↑j₁_1) else 0)
        (fun j₁_1 ↦ if ↑j₁_1 ≤ ↑j₁ ∧ ↑j₁ ≤ ↑j₁_1 + m then f.coeff (↑j₁ - ↑j₁_1) else 0) (Fin.natAdd m i) -
      r *
        Fin.addCases (fun j₁_1 ↦ if ↑j₁_1 ≤ ↑j₁ ∧ ↑j₁ ≤ ↑j₁_1 + n then g.coeff (↑j₁ - ↑j₁_1) else 0)
          (fun j₁_1 ↦ if ↑j₁_1 ≤ ↑j₁ ∧ ↑j₁ ≤ ↑j₁_1 + m then f.coeff (↑j₁ - ↑j₁_1) else 0)
          ⟨↑(Fin.natAdd m i) + (k + m), ⋯⟩ =
    Fin.addCases (fun j₁_1 ↦ if ↑j₁_1 ≤ ↑j₁ ∧ ↑j₁ ≤ ↑j₁_1 + n then g.coeff (↑j₁ - ↑j₁_1) else 0)
      (fun j₁_1 ↦ if ↑j₁_1 ≤ ↑j₁ ∧ ↑j₁ ≤ ↑j₁_1 + m then f.coeff (↑j₁ - ↑j₁_1) else 0) (Fin.natAdd m i)

Tactic:
have : Fin.mk (n := m + n) (m + ↑i + (k + m)) (by lia) =
              Fin.natAdd m ⟨↑i + (k + m), by lia⟩ := Fin.ext (by simp; lia)

Goal state after:
case succ.inl.right
R : Type u_1
inst✝ : CommRing R
f g : R[X]
r : R
m n k : ℕ
hk : k + m ≤ n
hf : f.natDegree ≤ m
hm : m ≠ 0
M₁ : Matrix (Fin (m + n)) (Fin (m + n)) R := f.sylvester (g + f * (monomial k) r) m n
M₂ : Matrix (Fin (m + n)) (Fin (m + n)) R := f.sylvester g m n
M : ℕ → Matrix (Fin (m + n)) (Fin (m + n)) R := fun i ↦ Matrix.of fun j₁ j₂ ↦ if ↑j₂ < i then M₁ j₁ j₂ else M₂ j₁ j₂
j₁ : Fin (m + n)
i : Fin n
IH : ↑(Fin.natAdd m i) ≤ m → (M ↑(Fin.natAdd m i)).det = M₂.det
hi : m + ↑i + 1 ≤ m
this : ⟨m + ↑i + (k + m), ⋯⟩ = Fin.natAdd m ⟨↑i + (k + m), ⋯⟩
⊢ Fin.addCases
        (fun j₁_1 ↦
          if ↑j₁_1 ≤ ↑j₁ ∧ ↑j₁ ≤ ↑j₁_1 + n then g.coeff (↑j₁ - ↑j₁_1) + (f * (monomial k) r).coeff (↑j₁ - ↑j₁_1) else 0)
        (fun j₁_1 ↦ if ↑j₁_1 ≤ ↑j₁ ∧ ↑j₁ ≤ ↑j₁_1 + m then f.coeff (↑j₁ - ↑j₁_1) else 0) (Fin.natAdd m i) -
      r *
        Fin.addCases (fun j₁_1 ↦ if ↑j₁_1 ≤ ↑j₁ ∧ ↑j₁ ≤ ↑j₁_1 + n then g.coeff (↑j₁ - ↑j₁_1) else 0)
          (fun j₁_1 ↦ if ↑j₁_1 ≤ ↑j₁ ∧ ↑j₁ ≤ ↑j₁_1 + m then f.coeff (↑j₁ - ↑j₁_1) else 0)
          ⟨↑(Fin.natAdd m i) + (k + m), ⋯⟩ =
    Fin.addCases (fun j₁_1 ↦ if ↑j₁_1 ≤ ↑j₁ ∧ ↑j₁ ≤ ↑j₁_1 + n then g.coeff (↑j₁ - ↑j₁_1) else 0)
      (fun j₁_1 ↦ if ↑j₁_1 ≤ ↑j₁ ∧ ↑j₁ ≤ ↑j₁_1 + m then f.coeff (↑j₁ - ↑j₁_1) else 0) (Fin.natAdd m i)
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case succ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
m n : ℕ
r : R
M₁ : Matrix (Fin (m + n)) (Fin (m + n)) R := f.sylvester (C r * g) m n
M₂ : Matrix (Fin (m + n)) (Fin (m + n)) R := f.sylvester g m n
M : ℕ → Matrix (Fin (m + n)) (Fin (m + n)) R := fun i ↦ Matrix.of fun j₁ j₂ ↦ if ↑j₂ < i then M₁ j₁ j₂ else M₂ j₁ j₂
i : ℕ
IH : i ≤ m → (M i).det = r ^ i * M₂.det
hi : i + 1 ≤ m
j₁ j₂ : Fin (m + n)
⊢ (if ↑j₂ = i then r * f.sylvester g m n j₁ ⟨i, ⋯⟩ else if ↑j₂ < i then M₁ j₁ j₂ else f.sylvester g m n j₁ j₂) =
    if ↑j₂ < i + 1 then M₁ j₁ j₂ else f.sylvester g m n j₁ j₂

Tactic:
obtain rfl | h := eq_or_ne ↑j₂ i

Goal state after:
case succ.inl
R : Type u_1
inst✝ : CommRing R
f g : R[X]
m n : ℕ
r : R
M₁ : Matrix (Fin (m + n)) (Fin (m + n)) R := f.sylvester (C r * g) m n
M₂ : Matrix (Fin (m + n)) (Fin (m + n)) R := f.sylvester g m n
M : ℕ → Matrix (Fin (m + n)) (Fin (m + n)) R := fun i ↦ Matrix.of fun j₁ j₂ ↦ if ↑j₂ < i then M₁ j₁ j₂ else M₂ j₁ j₂
j₁ j₂ : Fin (m + n)
IH : ↑j₂ ≤ m → (M ↑j₂).det = r ^ ↑j₂ * M₂.det
hi : ↑j₂ + 1 ≤ m
⊢ (if ↑j₂ = ↑j₂ then r * f.sylvester g m n j₁ ⟨↑j₂, ⋯⟩ else if ↑j₂ < ↑j₂ then M₁ j₁ j₂ else f.sylvester g m n j₁ j₂) =
    if ↑j₂ < ↑j₂ + 1 then M₁ j₁ j₂ else f.sylvester g m n j₁ j₂

case succ.inr
R : Type u_1
inst✝ : CommRing R
f g : R[X]
m n : ℕ
r : R
M₁ : Matrix (Fin (m + n)) (Fin (m + n)) R := f.sylvester (C r * g) m n
M₂ : Matrix (Fin (m + n)) (Fin (m + n)) R := f.sylvester g m n
M : ℕ → Matrix (Fin (m + n)) (Fin (m + n)) R := fun i ↦ Matrix.of fun j₁ j₂ ↦ if ↑j₂ < i then M₁ j₁ j₂ else M₂ j₁ j₂
i : ℕ
IH : i ≤ m → (M i).det = r ^ i * M₂.det
hi : i + 1 ≤ m
j₁ j₂ : Fin (m + n)
h : ↑j₂ ≠ i
⊢ (if ↑j₂ = i then r * f.sylvester g m n j₁ ⟨i, ⋯⟩ else if ↑j₂ < i then M₁ j₁ j₂ else f.sylvester g m n j₁ j₂) =
    if ↑j₂ < i + 1 then M₁ j₁ j₂ else f.sylvester g m n j₁ j₂