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

Goal state before:
pp: case neg
R✝ S✝ : Type u
inst✝⁷ : CommRing R✝
inst✝⁶ : CommRing S✝
inst✝⁵ : Algebra R✝ S✝
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal S
inst✝¹ : p.IsPrime
inst✝ : WeaklyQuasiFiniteAt R p
x : S
hx : R[x] = ⊤
H : integralClosure R S = ⊥
H₀ : Function.Surjective ⇑(aeval x)
f : R[X]
hf : (aeval x) f = 0
n : ℕ
hfn : (algebraMap R S) (f.coeff n) ∉ p
m : ℕ
IH :
  ∀ m_1 < m + 1,
    ∀ (f : R[X]),
      (aeval x) f = 0 → ∀ (n : ℕ), (algebraMap R S) (f.coeff n) ∉ p → f.natDegree = m_1 → ZariskisMainProperty R p
hm : f.natDegree = m + 1
Hfp : (algebraMap R S) f.leadingCoeff ∉ p
⊢ ZariskisMainProperty R p

Tactic:
refine zariskisMainProperty_iff_exists_saturation_eq_top.mpr ⟨_, Hfp, isIntegral_algebraMap, ?_⟩
    rw [← top_le_iff, ← hx]
    refine Algebra.adjoin_singleton_le ⟨_, ⟨1, rfl⟩, ?_⟩
    simpa [Algebra.smul_def] using! isIntegral_leadingCoeff_smul f x hf

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

Goal state before:
pp: case pos
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)
j₂ : Fin m
IH : ↑(Fin.castAdd n j₂) ≤ m → (M ↑(Fin.castAdd n j₂)).det = M₂.det
hi : ↑j₂ + 1 ≤ m
this : ⟨↑j₂ + (k + m), ⋯⟩ = Fin.natAdd m ⟨↑j₂ + k, ⋯⟩
h₁ : (↑j₂ ≤ ↑j₁ ∧ ↑j₁ ≤ ↑j₂ + n) ∧ k ≤ ↑j₁ - ↑j₂
h₂ : ↑j₂ + k ≤ ↑j₁ ∧ ↑j₁ ≤ ↑j₂ + (k + m)
⊢ r * f.coeff (↑j₁ - ↑j₂ - k) = r * f.coeff (↑j₁ - ↑j₂ - k)

Tactic:
try rfl

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

Goal state before:
pp: case neg
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)
j₂ : Fin m
IH : ↑(Fin.castAdd n j₂) ≤ m → (M ↑(Fin.castAdd n j₂)).det = M₂.det
hi : ↑j₂ + 1 ≤ m
this : ⟨↑j₂ + (k + m), ⋯⟩ = Fin.natAdd m ⟨↑j₂ + k, ⋯⟩
h₁ : (↑j₂ ≤ ↑j₁ ∧ ↑j₁ ≤ ↑j₂ + n) ∧ k ≤ ↑j₁ - ↑j₂
h₂ : ¬(↑j₂ + k ≤ ↑j₁ ∧ ↑j₁ ≤ ↑j₂ + (k + m))
⊢ r * f.coeff (↑j₁ - ↑j₂ - k) = 0

Tactic:
try rfl

Goal state after:
case neg
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)
j₂ : Fin m
IH : ↑(Fin.castAdd n j₂) ≤ m → (M ↑(Fin.castAdd n j₂)).det = M₂.det
hi : ↑j₂ + 1 ≤ m
this : ⟨↑j₂ + (k + m), ⋯⟩ = Fin.natAdd m ⟨↑j₂ + k, ⋯⟩
h₁ : (↑j₂ ≤ ↑j₁ ∧ ↑j₁ ≤ ↑j₂ + n) ∧ k ≤ ↑j₁ - ↑j₂
h₂ : ¬(↑j₂ + k ≤ ↑j₁ ∧ ↑j₁ ≤ ↑j₂ + (k + m))
⊢ r * f.coeff (↑j₁ - ↑j₂ - k) = 0
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case pos
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)
j₂ : Fin m
IH : ↑(Fin.castAdd n j₂) ≤ m → (M ↑(Fin.castAdd n j₂)).det = M₂.det
hi : ↑j₂ + 1 ≤ m
this : ⟨↑j₂ + (k + m), ⋯⟩ = Fin.natAdd m ⟨↑j₂ + k, ⋯⟩
h₁ : ¬((↑j₂ ≤ ↑j₁ ∧ ↑j₁ ≤ ↑j₂ + n) ∧ k ≤ ↑j₁ - ↑j₂)
h₂ : ↑j₂ + k ≤ ↑j₁ ∧ ↑j₁ ≤ ↑j₂ + (k + m)
⊢ 0 = r * f.coeff (↑j₁ - ↑j₂ - k)

Tactic:
try rfl

Goal state after:
case pos
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)
j₂ : Fin m
IH : ↑(Fin.castAdd n j₂) ≤ m → (M ↑(Fin.castAdd n j₂)).det = M₂.det
hi : ↑j₂ + 1 ≤ m
this : ⟨↑j₂ + (k + m), ⋯⟩ = Fin.natAdd m ⟨↑j₂ + k, ⋯⟩
h₁ : ¬((↑j₂ ≤ ↑j₁ ∧ ↑j₁ ≤ ↑j₂ + n) ∧ k ≤ ↑j₁ - ↑j₂)
h₂ : ↑j₂ + k ≤ ↑j₁ ∧ ↑j₁ ≤ ↑j₂ + (k + m)
⊢ 0 = r * f.coeff (↑j₁ - ↑j₂ - k)
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case neg
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)
j₂ : Fin m
IH : ↑(Fin.castAdd n j₂) ≤ m → (M ↑(Fin.castAdd n j₂)).det = M₂.det
hi : ↑j₂ + 1 ≤ m
this : ⟨↑j₂ + (k + m), ⋯⟩ = Fin.natAdd m ⟨↑j₂ + k, ⋯⟩
h₁ : ¬((↑j₂ ≤ ↑j₁ ∧ ↑j₁ ≤ ↑j₂ + n) ∧ k ≤ ↑j₁ - ↑j₂)
h₂ : ¬(↑j₂ + k ≤ ↑j₁ ∧ ↑j₁ ≤ ↑j₂ + (k + m))
⊢ 0 = 0

Tactic:
try rfl

Goal state after:
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✝¹ : FiniteType R S
p : Ideal S
inst✝ : p.IsPrime
H✝ : ZariskisMainProperty R p
S' : Subalgebra R S
hS' : (Subalgebra.toSubmodule S').FG
r : ↥S'
hrp : ↑r ∉ p
H : Function.Bijective ⇑(Localization.awayMap S'.val.toRingHom r)
this✝¹ : Module.Finite R ↥S'
this✝ : QuasiFinite R (Localization.Away r)
this : QuasiFinite R (Localization.Away ↑r)
f : Localization.Away ↑r →ₐ[S] Localization.AtPrime p := IsLocalization.Away.liftAlgHom ↑r ⋯
x : Localization.AtPrime p
⊢ ∃ s, IsUnit ((AlgHom.restrictScalars R f) s) ∧ x * (AlgHom.restrictScalars R f) s ∈ (AlgHom.restrictScalars R f).range

Tactic:
obtain ⟨x, ⟨s, hs⟩, rfl⟩ := IsLocalization.exists_mk'_eq p.primeCompl x

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FiniteType R S
p : Ideal S
inst✝ : p.IsPrime
H✝ : ZariskisMainProperty R p
S' : Subalgebra R S
hS' : (Subalgebra.toSubmodule S').FG
r : ↥S'
hrp : ↑r ∉ p
H : Function.Bijective ⇑(Localization.awayMap S'.val.toRingHom r)
this✝¹ : Module.Finite R ↥S'
this✝ : QuasiFinite R (Localization.Away r)
this : QuasiFinite R (Localization.Away ↑r)
f : Localization.Away ↑r →ₐ[S] Localization.AtPrime p := IsLocalization.Away.liftAlgHom ↑r ⋯
x s : S
hs : s ∈ p.primeCompl
⊢ ∃ s_1,
    IsUnit ((AlgHom.restrictScalars R f) s_1) ∧
      IsLocalization.mk' (Localization.AtPrime p) x ⟨s, hs⟩ * (AlgHom.restrictScalars R f) s_1 ∈
        (AlgHom.restrictScalars R f).range
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
n : ℕ
hg : g.natDegree ≤ n
hf : f.Splits
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.resultant g f.natDegree n = f.leadingCoeff ^ n * (Multiset.map (fun x ↦ eval x g) f.roots).prod
hR : ¬IsField R
K : Type u_1 := FractionRing R
⊢ f.resultant g f.natDegree n = f.leadingCoeff ^ n * (Multiset.map (fun x ↦ eval x g) f.roots).prod

Tactic:
apply FaithfulSMul.algebraMap_injective R K

Goal state after:
case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
n : ℕ
hg : g.natDegree ≤ n
hf : f.Splits
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.resultant g f.natDegree n = f.leadingCoeff ^ n * (Multiset.map (fun x ↦ eval x g) f.roots).prod
hR : ¬IsField R
K : Type u_1 := ⋯
⊢ (algebraMap R K) (f.resultant g f.natDegree n) =
    (algebraMap R K) (f.leadingCoeff ^ n * (Multiset.map (fun x ↦ eval x g) f.roots).prod)
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

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

Tactic:
simp only [Finset.mem_antidiagonal, ne_eq, ite_eq_right_iff, Prod.forall, Prod.mk.injEq]
      intro a b _ _ _
      simp [show b ≠ i by lia]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
this✝¹ : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (universalFactorizationMap R n m k hn).toAlgebra
this✝ : IsDomain (MvPolynomial (Fin m) ℤ ⊗[ℤ] MvPolynomial (Fin k) ℤ)
this : Algebra (MvPolynomial (Fin n) ℤ) (MvPolynomial (Fin m) ℤ ⊗[ℤ] MvPolynomial (Fin k) ℤ) :=
  (universalFactorizationMap ℤ n m k hn).toAlgebra
F : MvPolynomial (Fin m) ℤ ⊗[ℤ] MvPolynomial (Fin k) ℤ →ₐ[ℤ] MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R :=
  Algebra.TensorProduct.lift (Algebra.TensorProduct.includeLeft.comp (mapAlgHom (Algebra.ofId ℤ R)))
    ((AlgHom.restrictScalars ℤ Algebra.TensorProduct.includeRight).comp (mapAlgHom (Algebra.ofId ℤ R))) ⋯
i : Fin m
p : (MvPolynomial (Fin n) ℤ)[X]
hp : p.Monic
hp' : Polynomial.eval₂ (universalFactorizationMap ℤ n m k hn).toRingHom (X i ⊗ₜ[ℤ] 1) p = 0
⊢ Polynomial.eval₂ (universalFactorizationMap R n m k hn).toRingHom (X i ⊗ₜ[R] 1)
      (Polynomial.map (map (algebraMap ℤ R)) p) =
    0

Tactic:
apply_fun F.toRingHom at hp'

Goal state after:
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
this✝¹ : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (universalFactorizationMap R n m k hn).toAlgebra
this✝ : IsDomain (MvPolynomial (Fin m) ℤ ⊗[ℤ] MvPolynomial (Fin k) ℤ)
this : Algebra (MvPolynomial (Fin n) ℤ) (MvPolynomial (Fin m) ℤ ⊗[ℤ] MvPolynomial (Fin k) ℤ) :=
  (universalFactorizationMap ℤ n m k hn).toAlgebra
F : MvPolynomial (Fin m) ℤ ⊗[ℤ] MvPolynomial (Fin k) ℤ →ₐ[ℤ] MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R :=
  Algebra.TensorProduct.lift (Algebra.TensorProduct.includeLeft.comp (mapAlgHom (Algebra.ofId ℤ R)))
    ((AlgHom.restrictScalars ℤ Algebra.TensorProduct.includeRight).comp (mapAlgHom (Algebra.ofId ℤ R))) ⋯
i : Fin m
p : (MvPolynomial (Fin n) ℤ)[X]
hp : p.Monic
hp' : F.toRingHom (Polynomial.eval₂ (universalFactorizationMap ℤ n m k hn).toRingHom (X i ⊗ₜ[ℤ] 1) p) = F.toRingHom 0
⊢ Polynomial.eval₂ (universalFactorizationMap R n m k hn).toRingHom (X i ⊗ₜ[R] 1)
      (Polynomial.map (map (algebraMap ℤ R)) p) =
    0
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
H : IsCoprime f g
⊢ f.resultant g ≠ 0

Tactic:
by
  obtain rfl | hf := eq_or_ne f 0
  · simp only [isCoprime_zero_left, isUnit_iff] at H
    aesop
  intro e
  simpa [e, hf] using resultant_dvd_leadingCoeff_pow f g H

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
this✝¹ : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (universalFactorizationMap R n m k hn).toAlgebra
this✝ : IsDomain (MvPolynomial (Fin m) ℤ ⊗[ℤ] MvPolynomial (Fin k) ℤ)
this : Algebra (MvPolynomial (Fin n) ℤ) (MvPolynomial (Fin m) ℤ ⊗[ℤ] MvPolynomial (Fin k) ℤ) :=
  (universalFactorizationMap ℤ n m k hn).toAlgebra
F : MvPolynomial (Fin m) ℤ ⊗[ℤ] MvPolynomial (Fin k) ℤ →ₐ[ℤ] MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R :=
  Algebra.TensorProduct.lift (Algebra.TensorProduct.includeLeft.comp (mapAlgHom (Algebra.ofId ℤ R)))
    ((AlgHom.restrictScalars ℤ Algebra.TensorProduct.includeRight).comp (mapAlgHom (Algebra.ofId ℤ R))) ⋯
H₁ : ∀ (i : Fin m), (universalFactorizationMap R n m k hn).IsIntegralElem (X i ⊗ₜ[R] 1)
i : Fin k
p : (MvPolynomial (Fin n) ℤ)[X]
hp : p.Monic
hp' : Polynomial.eval₂ (universalFactorizationMap ℤ n m k hn).toRingHom (1 ⊗ₜ[ℤ] X i) p = 0
⊢ Polynomial.eval₂ (universalFactorizationMap R n m k hn).toRingHom (1 ⊗ₜ[R] X i)
      (Polynomial.map (map (algebraMap ℤ R)) p) =
    0

Tactic:
apply_fun F.toRingHom at hp'

Goal state after:
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
this✝¹ : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (universalFactorizationMap R n m k hn).toAlgebra
this✝ : IsDomain (MvPolynomial (Fin m) ℤ ⊗[ℤ] MvPolynomial (Fin k) ℤ)
this : Algebra (MvPolynomial (Fin n) ℤ) (MvPolynomial (Fin m) ℤ ⊗[ℤ] MvPolynomial (Fin k) ℤ) :=
  (universalFactorizationMap ℤ n m k hn).toAlgebra
F : MvPolynomial (Fin m) ℤ ⊗[ℤ] MvPolynomial (Fin k) ℤ →ₐ[ℤ] MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R :=
  Algebra.TensorProduct.lift (Algebra.TensorProduct.includeLeft.comp (mapAlgHom (Algebra.ofId ℤ R)))
    ((AlgHom.restrictScalars ℤ Algebra.TensorProduct.includeRight).comp (mapAlgHom (Algebra.ofId ℤ R))) ⋯
H₁ : ∀ (i : Fin m), (universalFactorizationMap R n m k hn).IsIntegralElem (X i ⊗ₜ[R] 1)
i : Fin k
p : (MvPolynomial (Fin n) ℤ)[X]
hp : p.Monic
hp' : F.toRingHom (Polynomial.eval₂ (universalFactorizationMap ℤ n m k hn).toRingHom (1 ⊗ₜ[ℤ] X i) p) = F.toRingHom 0
⊢ Polynomial.eval₂ (universalFactorizationMap R n m k hn).toRingHom (1 ⊗ₜ[R] X i)
      (Polynomial.map (map (algebraMap ℤ R)) p) =
    0
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case pos
m n : ℕ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
i : Fin (m + n)
j : Fin m
h₁ : ↑j ≤ ↑i
h₂ : ↑i ≤ ↑j + n
⊢ g.coeff (↑i - ↑j) = g.coeff (↑i - ↑j)

Tactic:
try rfl

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

Goal state before:
pp: case neg
m n : ℕ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
i : Fin (m + n)
j : Fin m
h₁ : ↑j ≤ ↑i
h₂ : ¬↑i ≤ ↑j + n
⊢ g.coeff (↑i - ↑j) = 0

Tactic:
try rfl

Goal state after:
case neg
m n : ℕ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
i : Fin (m + n)
j : Fin m
h₁ : ↑j ≤ ↑i
h₂ : ¬↑i ≤ ↑j + n
⊢ g.coeff (↑i - ↑j) = 0
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case neg
m n : ℕ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
i : Fin (m + n)
j : Fin m
h₁ : ¬↑j ≤ ↑i
⊢ 0 = 0

Tactic:
try rfl

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

Goal state before:
pp: case pos
m n : ℕ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
i : Fin (m + n)
j : Fin n
h₁ : ↑j ≤ ↑i
h₂ : ↑i ≤ ↑j + m
⊢ f.coeff (↑i - ↑j) = f.coeff (↑i - ↑j)

Tactic:
try rfl

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

Goal state before:
pp: case neg
m n : ℕ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
i : Fin (m + n)
j : Fin n
h₁ : ↑j ≤ ↑i
h₂ : ¬↑i ≤ ↑j + m
⊢ f.coeff (↑i - ↑j) = 0

Tactic:
try rfl

Goal state after:
case neg
m n : ℕ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
i : Fin (m + n)
j : Fin n
h₁ : ↑j ≤ ↑i
h₂ : ¬↑i ≤ ↑j + m
⊢ f.coeff (↑i - ↑j) = 0
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case neg
m n : ℕ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
i : Fin (m + n)
j : Fin n
h₁ : ¬↑j ≤ ↑i
⊢ 0 = 0

Tactic:
try rfl

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
i : ℕ
hi : i < 5
j : ℕ
hj : j < 5
⊢ (Matrix.reindex (finCongr ⋯) (finCongr ⋯)) f.sylvesterDeriv ⟨i, hi⟩ ⟨j, hj⟩ =
    !![f.coeff 0, 0, 1 * f.coeff 1, 0, 0;
        f.coeff 1, f.coeff 0, 2 * f.coeff 2, 1 * f.coeff 1, 0;
        f.coeff 2, f.coeff 1, 3 * f.coeff 3, 2 * f.coeff 2, 1 * f.coeff 1;
        f.coeff 3, f.coeff 2, 0, 3 * f.coeff 3, 2 * f.coeff 2;
        0, 1, 0, 0, 3]
      ⟨i, hi⟩ ⟨j, hj⟩

Tactic:
simp only [sylvesterDeriv, hf, OfNat.ofNat_ne_zero, ↓reduceDIte, sylvester, Fin.addCases,
    Nat.add_one_sub_one, Fin.val_castLT, mem_Icc, Fin.val_fin_le, Fin.val_subNat, Fin.val_cast,
    tsub_le_iff_right, coeff_derivative, eq_rec_constant, dite_eq_ite, Nat.reduceMul, Nat.reduceSub,
    Nat.cast_ofNat, Matrix.reindex_apply, finCongr_symm, Matrix.submatrix_apply, finCongr_apply,
    Fin.cast_mk, Matrix.updateRow_apply, Fin.mk.injEq, Matrix.of_apply, Fin.mk_le_mk, one_mul,
    Matrix.cons_val', Matrix.cons_val_fin_one]

Goal state after:
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
i : ℕ
hi : i < 5
j : ℕ
hj : j < 5
⊢ (if i = 4 then if j = 1 then 1 else if j = 4 then 3 else 0
    else
      if j < 2 then if j ≤ i ∧ i ≤ j + 3 then f.coeff (i - j) else 0
      else if j ≤ i + 2 ∧ i ≤ j - 2 + 2 then f.coeff (i - (j - 2) + 1) * (↑(i - (j - 2)) + 1) else 0) =
    Matrix.vecCons (![f.coeff 0, 0, f.coeff 1, 0, 0] ⟨j, hj⟩)
      (fun i ↦
        Matrix.vecCons (![f.coeff 1, f.coeff 0, 2 * f.coeff 2, f.coeff 1, 0] ⟨j, hj⟩)
          (fun i ↦
            Matrix.vecCons (![f.coeff 2, f.coeff 1, 3 * f.coeff 3, 2 * f.coeff 2, f.coeff 1] ⟨j, hj⟩)
              (fun i ↦
                Matrix.vecCons (![f.coeff 3, f.coeff 2, 0, 3 * f.coeff 3, 2 * f.coeff 2] ⟨j, hj⟩)
                  (fun i ↦ ![0, 1, 0, 0, 3] ⟨j, hj⟩) i)
              i)
          i)
      ⟨i, hi⟩
Module: Mathlib.AlgebraicGeometry.Group.Abelian

Goal state before:
pp: K : Type u
inst✝⁴ : Field K
inst✝³ : IsAlgClosed K
G : Over (Spec (CommRingCat.of K))
inst✝² : IsProper G.hom
inst✝¹ : IsIntegral (G ⊗ G).left
inst✝ : GrpObj G
S : Scheme := Spec (CommRingCat.of K)
point : ↥S := IsLocalRing.closedPoint K
hpoint : IsClosed {point}
this✝¹⁰ : Nonempty ↥G.left
this✝⁹ : IsProper (G ⊗ G).hom
this✝⁸ : JacobsonSpace ↥(G ⊗ G).left
this✝⁷ : Surjective G.hom
this✝⁶ : IsProper (Over.Hom.left (fst G G))
this✝⁵ : Surjective (Over.Hom.left (fst G G))
this✝⁴ : IsProper (Over.Hom.left (GrpObj.commutator G) ≫ G.hom)
this✝³ : IsClosedImmersion (Over.Hom.left (lift η η) ≫ Over.Hom.left (fst G G))
this✝² : IsClosedImmersion (Over.Hom.left (lift η η))
γ : G ⊗ G ⟶ G ⊗ G := lift (fst G G) (GrpObj.commutator G)
this✝¹ : IsProper (Over.Hom.left γ ≫ Over.Hom.left (fst G G))
this✝ : IsProper (Over.Hom.left γ)
H✝ : ⇑(Over.Hom.left γ) '' ⇑(Over.Hom.left (fst G G)) ⁻¹' {(Over.Hom.left η) point} ⊆ {(Over.Hom.left (lift η η)) point}
U : G.left.Opens
hηU : (Over.Hom.left η) point ∈ U
H : IsFinite ((Scheme.Hom.imageι (Over.Hom.left γ) ≫ Over.Hom.left (fst G G)) ∣_ U)
x : ↥U
this : ⇑U.ι ⁻¹' {↑x} = {x}
⊢ IsClosed (Set.range ⇑(Over.Hom.left γ))

Tactic:
by exact γ.left.isClosedMap.isClosed_range

Goal state after:
Module: Mathlib.AlgebraicGeometry.LimitsOver

Goal state before:
pp: X✝ : Scheme
P : MorphismProperty Scheme
S : Scheme
U X Y : P.Over ⊤ S
f : U ⟶ X
g : U ⟶ Y
inst✝¹ : IsOpenImmersion f.left
inst✝ : IsOpenImmersion g.left
i j : WalkingSpan
t : i ⟶ j
⊢ IsOpenImmersion ((span f g).map t).left

Tactic:
obtain (a | (a | a)) := t
  · simp only [WidePushoutShape.hom_id, CategoryTheory.Functor.map_id]
    infer_instance
  · simpa
  · simpa

Goal state after:
Module: Mathlib.RingTheory.Finiteness.ModuleFinitePresentation

Goal state before:
pp: R : Type u
S : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Module.Finite R S
inst✝ : Algebra.FinitePresentation R S
R' : Type u
w✝⁴ : CommRing R'
w✝³ : Algebra R R'
w✝² : Module.Finite R R'
w✝¹ : Free R R'
w✝ : Algebra.FinitePresentation R R'
f : R' →ₐ[R] S
hf : Function.Surjective ⇑f
this : Algebra R' S := f.toAlgebra
⊢ FinitePresentation R S

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

Goal state after:
R : Type u
S : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Module.Finite R S
inst✝ : Algebra.FinitePresentation R S
R' : Type u
w✝⁴ : CommRing R'
w✝³ : Algebra R R'
w✝² : Module.Finite R R'
w✝¹ : Free R R'
w✝ : Algebra.FinitePresentation R R'
f : R' →ₐ[R] S
hf : Function.Surjective ⇑f
this✝ : Algebra R' S := f.toAlgebra
this : IsScalarTower R R' S
⊢ FinitePresentation R S
Module: Mathlib.RingTheory.Flat.Rank

Goal state before:
pp: case pos
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Flat R S
inst✝¹ : Module.Finite R S
h : ∀ (p : PrimeSpectrum R), rankAtStalk S p ≤ 1
p : Ideal R
inst✝ : p.IsMaximal
hr : rankAtStalk S { asIdeal := p, isPrime := ⋯ } = 0
⊢ Function.Surjective ⇑(algebraMap (Localization.AtPrime p) (Localization.AtPrime p ⊗[R] S))

Tactic:
have : Subsingleton (Localization.AtPrime p ⊗[R] S) := by
      apply Module.subsingleton_of_rank_zero (R := Localization.AtPrime p)
      simp [← finrank_eq_rank, ← rankAtStalk_eq_finrank_tensorProduct ⟨p, inferInstance⟩, hr]

Goal state after:
case pos
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Flat R S
inst✝¹ : Module.Finite R S
h : ∀ (p : PrimeSpectrum R), rankAtStalk S p ≤ 1
p : Ideal R
inst✝ : p.IsMaximal
hr : rankAtStalk S { asIdeal := p, isPrime := ⋯ } = 0
this : Subsingleton (Localization.AtPrime p ⊗[R] S)
⊢ Function.Surjective ⇑(algebraMap (Localization.AtPrime p) (Localization.AtPrime p ⊗[R] S))
Module: Mathlib.RingTheory.Flat.Rank

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Flat R S
inst✝ : Module.Finite R S
⊢ rankAtStalk S = 1 ↔ Function.Bijective ⇑(algebraMap R S)

Tactic:
Function.Bijective,

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Flat R S
inst✝ : Module.Finite R S
⊢ rankAtStalk S = 1 ↔ Function.Injective ⇑(algebraMap R S) ∧ Function.Surjective ⇑(algebraMap R S)
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank

Goal state before:
pp: R S : CommRingCat
x : ↥(Spec S)
φ : R ⟶ S
inst✝¹ : (CommRingCat.Hom.hom φ).Flat
inst✝ : (CommRingCat.Hom.hom φ).Finite
⊢ 1 ≤ finrank (Spec.map φ) ((Spec.map φ) x)

Tactic:
finrank_SpecMap_eq_finrank ‹_› ‹_›

Goal state after:
R S : CommRingCat
x : ↥(Spec S)
φ : R ⟶ S
inst✝¹ : (CommRingCat.Hom.hom φ).Flat
inst✝ : (CommRingCat.Hom.hom φ).Finite
⊢ 1 ≤ (CommRingCat.Hom.hom φ).finrank ((Spec.map φ) x)
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank

Goal state before:
pp: R S : CommRingCat
φ : R ⟶ S
x : ↥(Spec R)
h : 1 x ≤ finrank (Spec.map φ) x
inst✝¹ : (CommRingCat.Hom.hom φ).Flat
inst✝ : (CommRingCat.Hom.hom φ).Finite
⊢ ∃ a, (Spec.map φ) a = x

Tactic:
finrank_SpecMap_eq_finrank ‹_› ‹_›

Goal state after:
R S : CommRingCat
φ : R ⟶ S
x : ↥(Spec R)
h : 1 x ≤ (CommRingCat.Hom.hom φ).finrank x
inst✝¹ : (CommRingCat.Hom.hom φ).Flat
inst✝ : (CommRingCat.Hom.hom φ).Finite
⊢ ∃ a, (Spec.map φ) a = x
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank

Goal state before:
pp: R S : CommRingCat
φ : R ⟶ S
inst✝² : (CommRingCat.Hom.hom φ).Flat
inst✝¹ : (CommRingCat.Hom.hom φ).Finite
inst✝ : (CommRingCat.Hom.hom φ).FinitePresentation
⊢ IsLocallyConstant (finrank (Spec.map φ))

Tactic:
finrank_SpecMap_eq_finrank ‹_› ‹_›

Goal state after:
R S : CommRingCat
φ : R ⟶ S
inst✝² : (CommRingCat.Hom.hom φ).Flat
inst✝¹ : (CommRingCat.Hom.hom φ).Finite
inst✝ : (CommRingCat.Hom.hom φ).FinitePresentation
⊢ IsLocallyConstant (CommRingCat.Hom.hom φ).finrank