mathlib-initiative/mathlib-tactics huggingface dataset:
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
f : MvPolynomial σ S
⊢ IsIntegral (MvPolynomial σ R) f ↔ ∀ (n : σ →₀ ℕ), IsIntegral R (coeff n f)

Tactic:
by
  refine ⟨fun H n ↦ ?mp, fun H ↦ ?mpr⟩
  case mpr =>
    rw [← f.support_sum_monomial_coeff]
    simp_rw [monomial_eq]
    refine IsIntegral.sum _ fun n _ ↦ .mul ((H n).map (Algebra.ofId _ _)).tower_top
      (.prod _ fun i _ ↦ .pow ?_ _)
    convert! isIntegral_algebraMap (x := MvPolynomial.X i)
    simp only [algebraMap_def, map_X]
  unfold IsIntegral at H
  wlog hσ : Finite σ generalizing σ
  · obtain ⟨g, hg⟩ := MvPolynomial.exists_rename_eq_of_vars_subset_range (τ := f.vars) f _
      Subtype.val_injective (by simp)
    by_cases hn : n ∈ Set.range (Finsupp.mapDomain ((↑) : f.vars → σ))
    · obtain ⟨n, rfl⟩ := hn
      simp_rw [← hg, coeff_rename_mapDomain _ Subtype.val_injective]
      exact this (f := g) (RingHom.IsIntegralElem.of_map
        (g := (rename ((↑) : f.vars → σ)).toRingHom) (rename_injective _ Subtype.val_injective)
        (.of_comp (f := (killCompl (f := ((↑) : f.vars → σ)) Subtype.val_injective).toRingHom) <| by
        simp only [AlgHom.toRingHom_eq_coe, algebraMap_def, RingHom.coe_coe, hg]
        convert!
          H.map
            ((rename Subtype.val).comp
                (killCompl (f := ((↑) : f.vars → σ)) Subtype.val_injective)).toRingHom
        · exact RingHom.ext (by simp [MvPolynomial.killCompl_map])
        · nth_rw 1 12 [← hg]; simp)) n (.of_fintype _)
    · rw [← hg, coeff_rename_eq_zero _ _ _ (by grind)]
      exact isIntegral_zero
  revert f n
  apply Finite.induction_empty_option _ _ _ σ
  · intro α β e IH f H n
    have := @IH (rename e.symm f) (.of_map (g := (rename e).toRingHom)
      (rename_injective _ e.injective) <| .of_comp (f := (rename e.symm).toRingHom)
        (by convert H <;> aesop)) (n.embDomain e.symm)
    simpa [Finsupp.embDomain_eq_mapDomain, coeff_rename_mapDomain _ e.symm.injective] using! this
  · intro f H n
    refine .of_map (g := (isEmptyAlgEquiv _ PEmpty).symm.toRingHom)
      (isEmptyAlgEquiv _ PEmpty).symm.injective
      (.of_comp (f := (isEmptyAlgEquiv _ PEmpty).toRingHom) ?_)
    convert! H
    · ext r m <;> simp [Subsingleton.elim m 0, C, X, monomial, coeff, map]
    · obtain rfl := Subsingleton.elim n 0
      have : constantCoeff = (isEmptyAlgEquiv S PEmpty).toRingHom := by aesop
      simpa [-EmbeddingLike.apply_eq_iff_eq, -isEmptyAlgEquiv_apply] using!
        congr((isEmptyAlgEquiv S PEmpty.{w + 1}).symm ($this f))
  · intro α _ IH f H n
    have := IH (IsIntegral.coeff (R := MvPolynomial α R)
      (p := optionEquivLeft _ _ f) (.of_map
      (g := (optionEquivLeft _ _).symm.toRingHom) (optionEquivLeft _ _).symm.injective
      (.of_comp (f := (optionEquivLeft _ _).toRingHom) (by
        convert! H
        · ext i m
          · aesop
          · cases i <;> aesop
        · aesop))) (n .none)) n.some
    rwa [optionEquivLeft_coeff_some_coeff_none] at this

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

Goal state before:
pp: X : Scheme
U : X.AffineZariskiSite
s : Set ↑Γ(X, U.toOpens)
⊢ Sieve.generate (U.presieveOfSections s) ∈ (grothendieckTopology X) U ↔ Ideal.span s = ⊤

Tactic:
← U.2.self_le_iSup_basicOpen_iff,

Goal state after:
X : Scheme
U : X.AffineZariskiSite
s : Set ↑Γ(X, U.toOpens)
⊢ Sieve.generate (U.presieveOfSections s) ∈ (grothendieckTopology X) U ↔ ↑U ≤ ⨆ f, X.basicOpen ↑f
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case f
K✝ : Type u
inst✝¹¹ : CommRing K✝
inst✝¹⁰ : IsDomain K✝
A : Type u_1
k : Type u_2
K : Type u_3
inst✝⁹ : CommRing A
inst✝⁸ : IsDomain A
inst✝⁷ : Field k
inst✝⁶ : Field K
inst✝⁵ : Algebra A[X] k
inst✝⁴ : Algebra A[X] K
inst✝³ : SMul k K
inst✝² : FaithfulSMul A[X] k
inst✝¹ : FaithfulSMul A[X] K
inst✝ : IsScalarTower A[X] k K
b : k
c : K
p q : A[X]
hq : q ≠ 0
⊢ (((algebraMap A[X] A⟮X⟯) p / (algebraMap A[X] A⟮X⟯) q) • b) • c =
    ((algebraMap A[X] A⟮X⟯) p / (algebraMap A[X] A⟮X⟯) q) • b • c

Tactic:
rw [← smul_right_inj hq]

Goal state after:
case f
K✝ : Type u
inst✝¹¹ : CommRing K✝
inst✝¹⁰ : IsDomain K✝
A : Type u_1
k : Type u_2
K : Type u_3
inst✝⁹ : CommRing A
inst✝⁸ : IsDomain A
inst✝⁷ : Field k
inst✝⁶ : Field K
inst✝⁵ : Algebra A[X] k
inst✝⁴ : Algebra A[X] K
inst✝³ : SMul k K
inst✝² : FaithfulSMul A[X] k
inst✝¹ : FaithfulSMul A[X] K
inst✝ : IsScalarTower A[X] k K
b : k
c : K
p q : A[X]
hq : q ≠ 0
⊢ q • (((algebraMap A[X] A⟮X⟯) p / (algebraMap A[X] A⟮X⟯) q) • b) • c =
    q • ((algebraMap A[X] A⟮X⟯) p / (algebraMap A[X] A⟮X⟯) q) • b • c
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case left.e_a.e_6
K : Type u
inst✝ : Field K
x : K⟮X⟯
p q a : K[X]
hq : q ≠ 0
ha : a ≠ 0
ha' : a.leadingCoeff ≠ 0
hainv : a.leadingCoeff⁻¹ ≠ 0
hdeg : (gcd p q).degree ≤ q.degree
hdeg' : (C a.leadingCoeff⁻¹ * gcd p q).degree ≤ q.degree
hdivp : C a.leadingCoeff⁻¹ * gcd p q ∣ p
hdivq : C a.leadingCoeff⁻¹ * gcd p q ∣ q
⊢ a.leadingCoeff * a.leadingCoeff⁻¹ * ((gcd p q).leadingCoeff / q.leadingCoeff) =
    (q.leadingCoeff / (gcd p q).leadingCoeff)⁻¹

Tactic:
mul_inv_cancel₀ ha',

Goal state after:
case left.e_a.e_6
K : Type u
inst✝ : Field K
x : K⟮X⟯
p q a : K[X]
hq : q ≠ 0
ha : a ≠ 0
ha' : a.leadingCoeff ≠ 0
hainv : a.leadingCoeff⁻¹ ≠ 0
hdeg : (gcd p q).degree ≤ q.degree
hdeg' : (C a.leadingCoeff⁻¹ * gcd p q).degree ≤ q.degree
hdivp : C a.leadingCoeff⁻¹ * gcd p q ∣ p
hdivq : C a.leadingCoeff⁻¹ * gcd p q ∣ q
⊢ 1 * ((gcd p q).leadingCoeff / q.leadingCoeff) = (q.leadingCoeff / (gcd p q).leadingCoeff)⁻¹
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case right.e_a.e_6
K : Type u
inst✝ : Field K
x : K⟮X⟯
p q a : K[X]
hq : q ≠ 0
ha : a ≠ 0
ha' : a.leadingCoeff ≠ 0
hainv : a.leadingCoeff⁻¹ ≠ 0
hdeg : (gcd p q).degree ≤ q.degree
hdeg' : (C a.leadingCoeff⁻¹ * gcd p q).degree ≤ q.degree
hdivp : C a.leadingCoeff⁻¹ * gcd p q ∣ p
hdivq : C a.leadingCoeff⁻¹ * gcd p q ∣ q
⊢ a.leadingCoeff * a.leadingCoeff⁻¹ * ((gcd p q).leadingCoeff / q.leadingCoeff) =
    (q.leadingCoeff / (gcd p q).leadingCoeff)⁻¹

Tactic:
mul_inv_cancel₀ ha',

Goal state after:
case right.e_a.e_6
K : Type u
inst✝ : Field K
x : K⟮X⟯
p q a : K[X]
hq : q ≠ 0
ha : a ≠ 0
ha' : a.leadingCoeff ≠ 0
hainv : a.leadingCoeff⁻¹ ≠ 0
hdeg : (gcd p q).degree ≤ q.degree
hdeg' : (C a.leadingCoeff⁻¹ * gcd p q).degree ≤ q.degree
hdivp : C a.leadingCoeff⁻¹ * gcd p q ∣ p
hdivq : C a.leadingCoeff⁻¹ * gcd p q ∣ q
⊢ 1 * ((gcd p q).leadingCoeff / q.leadingCoeff) = (q.leadingCoeff / (gcd p q).leadingCoeff)⁻¹
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝ : Field K
p q : K[X]
⊢ ((algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q).num = C (q / gcd p q).leadingCoeff⁻¹ * (p / gcd p q)

Tactic:
by
  by_cases hq : q = 0
  · simp [hq]
  · exact num_div' p hq

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
⊢ ∃ ε ∈ I, ∃ b, (aeval x) (derivative P.f) * b = 1 + ε

Tactic:
refine ⟨_, ?_, (a ^ n * aeval x p₁), sub_eq_iff_eq_add'.mp rfl⟩
    convert_to (aeval x P.g * a) ^ n - 1 - aeval x P.f * (a ^ n * aeval x p₂) ∈ I
    · linear_combination a ^ n * e
    · exact sub_mem (Ideal.mem_of_dvd _ (sub_one_dvd_pow_sub_one _ _) ha) (I.mul_mem_right _ hf)

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

Goal state before:
pp: K : Type u
inst✝ : Field K
x : K⟮X⟯
hx : x ≠ 0
⊢ x⁻¹.denom ∣ x.num

Tactic:
by
  rw [denom_dvd (num_ne_zero hx)]
  refine ⟨x.denom, ?_⟩
  nth_rw 1 [← x.num_div_denom]
  rw [inv_div]

Goal state after:
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
P : Ideal R
inst✝ : P.IsPrime
x : S
hx : R[x] = ⊤
⊢ Ideal.map (mapRingHom (algebraMap R P.ResidueField)) (RingHom.ker (aeval x).toRingHom) =
    RingHom.ker (aeval (1 ⊗ₜ[R] x)).toRingHom

Tactic:
have hx' : Function.Surjective (aeval (R := R) x) :=
    (AlgHom.range_eq_top _).mp ((adjoin_singleton_eq_range_aeval R x).symm.trans hx)

Goal state after:
R : Type u_1
S : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Ideal R
inst✝ : P.IsPrime
x : S
hx : R[x] = ⊤
hx' : Function.Surjective ⇑(aeval x)
⊢ Ideal.map (mapRingHom (algebraMap R P.ResidueField)) (RingHom.ker (aeval x).toRingHom) =
    RingHom.ker (aeval (1 ⊗ₜ[R] x)).toRingHom
Module: Mathlib.RingTheory.Unramified.LocalStructure

Goal state before:
pp: case inr
R : Type u_1
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Module.Finite R S
Q : Ideal S
inst✝¹ : Q.IsPrime
inst✝ : IsUnramifiedAt R Q
h✝ : Nontrivial S
this✝ : Nontrivial R
P : Ideal R := Ideal.under R Q
this : Algebra (Localization.AtPrime P) (Localization.AtPrime Q) := Localization.AtPrime.algebraOfLiesOver P Q
x : S
hx : R[x] = ⊤
hRx : IsIntegral R x
I : Ideal R[X] := RingHom.ker (aeval x).toRingHom
⊢ ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f

Tactic:
have hx' : Function.Surjective (aeval (R := R) x) :=
    (AlgHom.range_eq_top _).mp ((adjoin_singleton_eq_range_aeval R x).symm.trans hx)

Goal state after:
case inr
R : Type u_1
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Module.Finite R S
Q : Ideal S
inst✝¹ : Q.IsPrime
inst✝ : IsUnramifiedAt R Q
h✝ : Nontrivial S
this✝ : Nontrivial R
P : Ideal R := Ideal.under R Q
this : Algebra (Localization.AtPrime P) (Localization.AtPrime Q) := Localization.AtPrime.algebraOfLiesOver P Q
x : S
hx : R[x] = ⊤
hRx : IsIntegral R x
I : Ideal R[X] := RingHom.ker (aeval x).toRingHom
hx' : Function.Surjective ⇑(aeval x)
⊢ ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f
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
inst✝⁴ : FaithfulSMul R S
inst✝³ : IsIntegrallyClosed R
inst✝² : IsDomain S
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : WeaklyQuasiFiniteAt R P
this✝ : IsDomain R
f : R[X] →ₐ[R] S
hx' : f.Finite
hf' : Function.Injective ⇑f
hx : IsStronglyTranscendental R (f X)
hf : aeval (f X) = f
this : Algebra R[X] S := f.toAlgebra
⊢ False

Tactic:
have := IsScalarTower.of_algebraMap_eq' f.comp_algebraMap.symm

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : FaithfulSMul R S
inst✝³ : IsIntegrallyClosed R
inst✝² : IsDomain S
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : WeaklyQuasiFiniteAt R P
this✝¹ : IsDomain R
f : R[X] →ₐ[R] S
hx' : f.Finite
hf' : Function.Injective ⇑f
hx : IsStronglyTranscendental R (f X)
hf : aeval (f X) = f
this✝ : Algebra R[X] S := f.toAlgebra
this : IsScalarTower R R[X] S
⊢ False
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
Q : Ideal S
inst✝² : Q.IsPrime
inst✝¹ : FinitePresentation R S
inst✝ : IsEtaleAt R Q
f : S
hfQ : f ∉ Q
h : ↑(PrimeSpectrum.basicOpen f) ⊆ etaleLocus R S
g : S
hgQ : g ∉ Q
hg : HasStandardEtaleSurjectionOn R g
⊢ ↑(PrimeSpectrum.basicOpen (f * g)) ⊆ etaleLocus R S

Tactic:
exact .trans (PrimeSpectrum.basicOpen_mul_le_left _ _) h

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
m n : ℕ
i : Fin n
⊢ (basisProd R m n) (Fin.natAdd m i) = (0, (basis R n) i)

Tactic:
by
  rw [basisProd, Basis.reindex_apply, finSumFinEquiv_symm_apply_natAdd, Basis.prod_apply,
    Sum.elim_inr, LinearMap.coe_inr, Function.comp_apply]

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

Goal state before:
pp: 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₂

Tactic:
simp only [↓reduceIte, sylvester, Set.mem_Icc, coeff_add, Fin.eta, Matrix.of_apply,
          lt_self_iff_false, M₁]

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
⊢ 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) j₂ -
      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) ⟨↑j₂ + (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) j₂
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
U : (X.openCoverOfIsOpenCover (fun k ↦ (TopologicalSpace.Opens.comap f.base.hom') ↑k) ⋯).I₀
⊢ (f ⁻¹ᵁ ↑U).toSpecΓ ≫
      Spec.map
          ((normalizationDiagramMap f).app (Opposite.op ↑U) ≫
            CommRingCat.ofHom (integralClosure ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U)).val.toRingHom) ≫
        IsAffineOpen.fromSpec ⋯ =
    (X.openCoverOfIsOpenCover (fun k ↦ (TopologicalSpace.Opens.comap f.base.hom') ↑k) ⋯).f U ≫ f

Tactic:
change (f ⁻¹ᵁ U.1).toSpecΓ ≫ Spec.map (f.app _) ≫ U.2.fromSpec = (f ⁻¹ᵁ U.1).ι ≫ _

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
U : (X.openCoverOfIsOpenCover (fun k ↦ (TopologicalSpace.Opens.comap f.base.hom') ↑k) ⋯).I₀
⊢ (f ⁻¹ᵁ ↑U).toSpecΓ ≫ Spec.map (app f ↑U) ≫ IsAffineOpen.fromSpec ⋯ = (f ⁻¹ᵁ ↑U).ι ≫ f
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: 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 : ℕ
hi : i ≤ m
⊢ (M i).det = M₂.det

Tactic:
induction i with
    | zero => simp [M]; rfl
    | succ i IH =>
      rw [← IH (by lia), ← Matrix.det_updateCol_add_smul_self (i := ⟨i, by lia⟩)
        (j := ⟨i + k + m, by lia⟩) (c := -r) (M (i + 1)) (by simp; lia)]
      congr 1
      ext j₁ j₂
      simp only [Matrix.of_apply, lt_add_iff_pos_right, zero_lt_one, ↓reduceIte, add_assoc,
        add_lt_add_iff_left, Nat.lt_one_iff, Nat.add_eq_zero_iff, hm, and_false, smul_eq_mul,
        Matrix.updateCol_apply, Fin.ext_iff, M, M₂, neg_mul, ← sub_eq_add_neg]
      obtain rfl | h := eq_or_ne ↑j₂ i
      · simp only [↓reduceIte, sylvester, Set.mem_Icc, coeff_add, Fin.eta, Matrix.of_apply,
          lt_self_iff_false, M₁]
        induction j₂ using Fin.addCases with
        | left j₂ =>
          dsimp at hi
          have : Fin.mk (n := m + n) (↑j₂ + (k + m)) (by lia) = .natAdd m ⟨j₂ + k, by lia⟩ :=
            Fin.ext (by simp; lia)
          simp only [Fin.addCases_left, Fin.val_castAdd, this, Fin.addCases_right, mul_ite,
            mul_zero, ← C_mul_X_pow_eq_monomial, ← mul_assoc, coeff_mul_X_pow', ite_add_zero,
            coeff_mul_C, add_assoc, add_eq_left, ← ite_and, ← mul_comm r, tsub_add_eq_tsub_tsub,
            add_sub_assoc, sub_eq_zero]
          split_ifs with h₁ h₂ h₂ <;> try rfl
          · rw [coeff_eq_zero_of_natDegree_lt, mul_zero]
            exact hf.trans_lt (by lia)
          · lia
        | right i =>
          simp only [Fin.val_natAdd] at hi
          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)
          simp only [Fin.addCases_right, Fin.val_natAdd, sub_eq_self, this]
          rw [if_neg, mul_zero]
          lia
      lia

Goal state after:
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
⊢ ker (toNormalization f) = ⊥

Tactic:
refine Scheme.IdealSheafData.ext_of_iSup_eq_top
    (fun U : Y.affineOpens ↦ ⟨f.fromNormalization ⁻¹ᵁ U.1, U.2.preimage _⟩)
    (TopologicalSpace.IsOpenCover.comap (iSup_affineOpens_eq_top _) _) fun U ↦ ?_

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
U : ↑Y.affineOpens
⊢ (ker (toNormalization f)).ideal ⟨fromNormalization f ⁻¹ᵁ ↑U, ⋯⟩ = ⊥.ideal ⟨fromNormalization f ⁻¹ᵁ ↑U, ⋯⟩
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
n : ℕ
hg : g.natDegree ≤ n
hf : f.Splits
hR : IsField R
hfm : f.Monic
hg0 : ¬g = 0
this :
  ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] (f g : R[X]) (n : ℕ),
    g.natDegree ≤ n →
      f.Splits →
        IsField R →
          f.Monic → ¬g = 0 → g.Monic → f.resultant g f.natDegree n = (Multiset.map (fun x ↦ eval x g) f.roots).prod
hgm : ¬g.Monic
inst : Field R := hR.toField
⊢ (C g.leadingCoeff⁻¹ * g).Monic

Tactic:
by rw [Monic, ← coeff_natDegree, natDegree_C_mul (by simp [hg0]), coeff_C_mul]; simp [hg0]

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

Goal state before:
pp: case inr
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
i : Fin k
j : Fin n
h : ↑i ≤ ↑j
⊢ (∑ x ∈ Finset.antidiagonal ↑j,
      if x.2 < k then
        if h : x.1 < m then if x.2 = ↑i then X (Sum.inl ⟨x.1, h⟩) else 0 else if x.1 = m ∧ x.2 = ↑i then 1 else 0
      else 0) =
    if ↑j < ↑i then 0 else if h : ↑j - ↑i < m then X (Sum.inl ⟨↑j - ↑i, h⟩) else if ↑j - ↑i = m then 1 else 0

Tactic:
Finset.sum_eq_single ⟨j.1 - i.1, i.1⟩,

Goal state after:
case inr
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
i : Fin k
j : Fin n
h : ↑i ≤ ↑j
⊢ (if (↑j - ↑i, ↑i).2 < k then
      if h : (↑j - ↑i, ↑i).1 < m then if (↑j - ↑i, ↑i).2 = ↑i then X (Sum.inl ⟨(↑j - ↑i, ↑i).1, h⟩) else 0
      else if (↑j - ↑i, ↑i).1 = m ∧ (↑j - ↑i, ↑i).2 = ↑i then 1 else 0
    else 0) =
    if ↑j < ↑i then 0 else if h : ↑j - ↑i < m then X (Sum.inl ⟨↑j - ↑i, h⟩) else if ↑j - ↑i = m then 1 else 0

case inr.h₀
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
i : Fin k
j : Fin n
h : ↑i ≤ ↑j
⊢ ∀ b ∈ Finset.antidiagonal ↑j,
    b ≠ (↑j - ↑i, ↑i) →
      (if b.2 < k then
          if h : b.1 < m then if b.2 = ↑i then X (Sum.inl ⟨b.1, h⟩) else 0 else if b.1 = m ∧ b.2 = ↑i then 1 else 0
        else 0) =
        0

case inr.h₁
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
i : Fin k
j : Fin n
h : ↑i ≤ ↑j
⊢ (↑j - ↑i, ↑i) ∉ Finset.antidiagonal ↑j →
    (if (↑j - ↑i, ↑i).2 < k then
        if h : (↑j - ↑i, ↑i).1 < m then if (↑j - ↑i, ↑i).2 = ↑i then X (Sum.inl ⟨(↑j - ↑i, ↑i).1, h⟩) else 0
        else if (↑j - ↑i, ↑i).1 = m ∧ (↑j - ↑i, ↑i).2 = ↑i then 1 else 0
      else 0) =
      0
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f g : R[X]
hg : g.natDegree ≠ 0
this :
  ∀ {R : Type u_1} [inst : CommRing R] (f g : R[X]),
    g.natDegree ≠ 0 →
      IsDomain R →
        (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
          g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g
hR : ¬IsDomain R
hf0 : ¬f = 0
hg0 : ¬g = 0
S : Type (max 0 u_1) := MvPolynomial R ℤ
φ : S →+* R := MvPolynomial.eval₂Hom (algebraMap ℤ R) id
hφ : Function.Surjective ⇑φ
f' : S[X]
hf' : map φ f' = f
ef : f'.degree = f.degree
g' : S[X]
hg' : map φ g' = g
eg : g'.degree = g.degree
hfl : f.leadingCoeff = φ f'.leadingCoeff
hgl : g.leadingCoeff = φ g'.leadingCoeff
⊢ g'.natDegree ≠ 0

Tactic:
simpa [natDegree_eq_natDegree eg]

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

Goal state before:
pp: case injective
R✝ : Type u_1
inst✝² : CommRing R✝
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
φ : R →+* S
hφ : Function.Injective ⇑φ
f : R[X]
IH : ∀ (g : S[X]) (r : S), ((taylor r) (map φ f)).resultant ((taylor r) g) = (map φ f).resultant g
g : R[X]
r : R
⊢ φ (((taylor r) f).resultant ((taylor r) g)) = φ (f.resultant g)

Tactic:
have := IH (g.map φ) (φ r)

Goal state after:
case injective
R✝ : Type u_1
inst✝² : CommRing R✝
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
φ : R →+* S
hφ : Function.Injective ⇑φ
f : R[X]
IH : ∀ (g : S[X]) (r : S), ((taylor r) (map φ f)).resultant ((taylor r) g) = (map φ f).resultant g
g : R[X]
r : R
this : ((taylor (φ r)) (map φ f)).resultant ((taylor (φ r)) (map φ g)) = (map φ f).resultant (map φ g)
⊢ φ (((taylor r) f).resultant ((taylor r) g)) = φ (f.resultant g)
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case refine_1
m n : ℕ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
p : R[X]
hp : p ∈ R[X]_m
q : R[X]
hq : q ∈ R[X]_n
⊢ (f * ↑(⟨p, hp⟩, ⟨q, hq⟩).2).degree < ↑(m + n)

pp: case refine_2
m n : ℕ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
p : R[X]
hp : p ∈ R[X]_m
q : R[X]
hq : q ∈ R[X]_n
⊢ (g * ↑(⟨p, hp⟩, ⟨q, hq⟩).1).degree < ↑(m + n)

Tactic:
· by_cases hf' : f = 0; · simp_all
      exact (degree_mul_le _ _).trans_lt (WithBot.add_lt_add_of_le_of_lt (by simpa)
        (degree_le_of_natDegree_le hf) (by simpa using hq))

Goal state after:
case refine_2
m n : ℕ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
p : R[X]
hp : p ∈ R[X]_m
q : R[X]
hq : q ∈ R[X]_n
⊢ (g * ↑(⟨p, hp⟩, ⟨q, hq⟩).1).degree < ↑(m + n)
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: m n : ℕ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
H : m ≠ 0 ∨ n ≠ 0
⊢ ∃ p q, p.degree < ↑n ∧ q.degree < ↑m ∧ f * p + g * q = C (f.resultant g m n)

Tactic:
nontriviality R
  let X := adjSylvester f g ⟨1, by simpa [Polynomial.mem_degreeLT,
    ← Nat.cast_add, Nat.pos_iff_ne_zero, not_and_or, -not_and] using H⟩
  have : ((sylvesterMap f g hf hg X)).1 = _ :=
    congr(($(sylveserMap_comp_adjSylvester f g hf hg) _).1)
  refine ⟨X.2, X.1, by simpa [-SetLike.coe_mem] using X.2.2,
    by simpa [-SetLike.coe_mem] using X.1.2, by simpa [Algebra.smul_def] using this⟩

Goal state after: