mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Module.SpanRank

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : RankCondition R
ι : Type u
v : ι → M
hv : Function.Injective v
hs : LinearIndependent R v
x : { s // span R s = span R (Set.range v) }
this : #↑↑x = #↑(Subtype.val ⁻¹' ↑x)
⊢ #ι ≤ #↑(Set.range ⇑(Module.Basis.span hs))

Tactic:
rw [mk_range_eq]

Goal state after:
case refine_1.h
R : Type u_1
M : Type u
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : RankCondition R
ι : Type u
v : ι → M
hv : Function.Injective v
hs : LinearIndependent R v
x : { s // span R s = span R (Set.range v) }
this : #↑↑x = #↑(Subtype.val ⁻¹' ↑x)
⊢ Function.Injective ⇑(Module.Basis.span hs)
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: case neg
R : Type u
inst✝³ : CommRing R
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
⊢ M.charpoly.degree = ↑(Fintype.card n)

Tactic:
rw [← sub_add_cancel M.charpoly (∏ i : n, (X - C (M i i)))]

Goal state after:
case neg
R : Type u
inst✝³ : CommRing R
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
⊢ (M.charpoly - ∏ i, (X - C (M i i)) + ∏ i, (X - C (M i i))).degree = ↑(Fintype.card n)
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: case succ.h₀.succ
R : Type u
inst✝ : CommRing R
n : ℕ
IH : ∀ (M : Matrix (Fin (n + 1)) (Fin (n + 1)) R), eval 0 (derivative (1 + X • M.map ⇑C).det) = M.trace
M : Matrix (Fin (n + 1 + 1)) (Fin (n + 1 + 1)) R
i : Fin (n + 1).succ
a✝ : i ∈ univ
hi : i ≠ 0
⊢ (-1) ^ ↑i * (eval 0 (derivative 0) + M 0 i) * eval 0 (submatrix 1 Fin.succ i.succAbove).det = 0

Tactic:
det_eq_zero_of_column_eq_zero 0,

Goal state after:
case succ.h₀.succ
R : Type u
inst✝ : CommRing R
n : ℕ
IH : ∀ (M : Matrix (Fin (n + 1)) (Fin (n + 1)) R), eval 0 (derivative (1 + X • M.map ⇑C).det) = M.trace
M : Matrix (Fin (n + 1 + 1)) (Fin (n + 1 + 1)) R
i : Fin (n + 1).succ
a✝ : i ∈ univ
hi : i ≠ 0
⊢ (-1) ^ ↑i * (eval 0 (derivative 0) + M 0 i) * eval 0 0 = 0

case succ.h₀.succ
R : Type u
inst✝ : CommRing R
n : ℕ
IH : ∀ (M : Matrix (Fin (n + 1)) (Fin (n + 1)) R), eval 0 (derivative (1 + X • M.map ⇑C).det) = M.trace
M : Matrix (Fin (n + 1 + 1)) (Fin (n + 1 + 1)) R
i : Fin (n + 1).succ
a✝ : i ∈ univ
hi : i ≠ 0
⊢ ∀ (i_1 : Fin (n + 1)), submatrix 1 Fin.succ i.succAbove i_1 0 = 0
Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : IsDomain A
M : Type u_5
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module A M
inst✝¹ : IsScalarTower R A M
inst✝ : Module.IsTorsionFree A M
N : Submodule R M
hN : N ≠ ⊥
hN' : N.FG
x : A
hx : ∀ n ∈ N, x • n ∈ N
A' : Subalgebra R A :=
  { carrier := {x | ∀ n ∈ N, x • n ∈ N}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯,
    algebraMap_mem' := ⋯ }
⊢ { toFun := fun x ↦ (DistribSMul.toLinearMap R M x).restrict ⋯, map_add' := ⋯, map_smul' := ⋯ } 1 = 1

Tactic:
by ext; apply one_smul

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
hM : IsNilpotent M
a✝ : Nontrivial R
p : R[X] := M.charpolyRev
⊢ IsNilpotent (M.charpoly - X ^ Fintype.card n)

Tactic:
have hp : p - 1 = X * (p /ₘ X) := by
    conv_lhs => rw [← modByMonic_add_div p X]
    simp [p, modByMonic_X]

Goal state after:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
hM : IsNilpotent M
a✝ : Nontrivial R
p : R[X] := M.charpolyRev
hp : p - 1 = X * (p /ₘ X)
⊢ IsNilpotent (M.charpoly - X ^ Fintype.card n)
Module: Mathlib.Algebra.Polynomial.HasseDeriv

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n : ℕ
⊢ ((hasseDeriv k) f).coeff n = ↑((n + k).choose k) * f.coeff (n + k)

Tactic:
rw [hasseDeriv_apply, coeff_sum, sum_def, Finset.sum_eq_single (n + k), coeff_monomial]
  · simp
  · #adaptation_note
    /-- Prior to nightly-2025-08-14, this was working as
    `grind [coeff_monomial, Nat.choose_eq_zero_of_lt, Nat.cast_zero, zero_mul]` -/
    intro i _hi hink
    rw [coeff_monomial]
    by_cases hik : i < k
    · simp only [Nat.choose_eq_zero_of_lt hik, ite_self, Nat.cast_zero, zero_mul]
    · grind
  · intro h
    simp only [notMem_support_iff.mp h, monomial_zero_right, mul_zero, coeff_zero]

Goal state after:
Module: Mathlib.Algebra.Polynomial.HasseDeriv

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
this : ((hasseDeriv f.natDegree) f).natDegree ≤ 0
⊢ C (↑(f.natDegree.choose f.natDegree) * f.coeff f.natDegree) = C f.leadingCoeff

Tactic:
Nat.choose_self,

Goal state after:
R : Type u_1
inst✝ : Semiring R
f : R[X]
this : ((hasseDeriv f.natDegree) f).natDegree ≤ 0
⊢ C (↑1 * f.coeff f.natDegree) = C f.leadingCoeff
Module: Mathlib.Algebra.Polynomial.HasseDeriv

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
k : ℕ
f g : R[X]
D : ℕ → R[X] →+ R[X] := fun k ↦ (hasseDeriv k).toAddMonoidHom
Φ : R[X] →+ R[X] →+ R[X] := mul
⊢ (((compHom (D k)).comp Φ) f) g = ∑ ij ∈ antidiagonal k, (((compHom.comp ((compHom Φ) (D ij.1))).flip (D ij.2)) f) g

Tactic:
simp only [← finsetSum_apply]

Goal state after:
R : Type u_1
inst✝ : Semiring R
k : ℕ
f g : R[X]
D : ℕ → R[X] →+ R[X] := fun k ↦ (hasseDeriv k).toAddMonoidHom
Φ : R[X] →+ R[X] →+ R[X] := mul
⊢ (((compHom (D k)).comp Φ) f) g = ((∑ x ∈ antidiagonal k, (compHom.comp ((compHom Φ) (D x.1))).flip (D x.2)) f) g
Module: Mathlib.RingTheory.Polynomial.ScaleRoots

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p : R[X]
r : R
hr : IsUnit r
a : R[X]
⊢ p.scaleRoots r ∣ (p * a).scaleRoots r

Tactic:
← ((hr.pow (natDegree p + natDegree a - natDegree (p * a))).map
    (algebraMap R R[X])).dvd_mul_left,

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
r : R
hr : IsUnit r
a : R[X]
⊢ p.scaleRoots r ∣ (algebraMap R R[X]) (r ^ (p.natDegree + a.natDegree - (p * a).natDegree)) * (p * a).scaleRoots r
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: case inl
R : Type u_1
inst✝ : CommSemiring R
f : R[X]
hf : f.Splits
h : Irreducible f
a✝ : Nontrivial R
hm : f = C f.leadingCoeff * (Multiset.map (fun x ↦ X + C x) 0).prod
⊢ f.natDegree ≤ 1

Tactic:
rw [hm]
    simp

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : A
hx : IsIntegral R x
⊢ R[x] ≤ integralClosure R A

Tactic:
rw [Algebra.adjoin_le_iff]
  simp only [SetLike.mem_coe, Set.singleton_subset_iff]
  exact hx

Goal state after:
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
t s : S
hst : s * t = 1
a✝ : Nontrivial S
φ : R[X] →ₐ[R] S := aeval s
p : (↥R[s])[X]
hpm : p.Monic
hpt : eval₂ (algebraMap (↥R[s]) S) t p = 0
⊢ ∀ (n : ℕ), (Polynomial.map (algebraMap (↥R[s]) S) p).coeff n ∈ Set.range ⇑φ.toRingHom

Tactic:
simp [← AlgHom.mem_range, φ, ← Algebra.adjoin_singleton_eq_range_aeval]

Goal state after:
Module: Mathlib.RingTheory.Ideal.GoingUp

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
p : Ideal R
inst✝² : p.IsPrime
q : Ideal S
inst✝¹ : q.IsPrime
hq : p.primesOver S = {q}
inst✝ : Algebra.IsIntegral R S
x : S
hx : x ∉ q
this : ∀ r ∉ p, ∀ (c : S), c * x ≠ (algebraMap R S) r
Q : Ideal S
hQ : Q.IsPrime
hxQ : span {x} ≤ Q
hQp : Disjoint ↑Q ↑(Algebra.algebraMapSubmonoid S p.primeCompl)
hQp' : under R Q ≤ p
Q' : Ideal S
hQ'Q : Q' ≥ Q
hQ' : Q'.IsPrime
hQ'p : comap (algebraMap R S) Q' = p
⊢ False

Tactic:
obtain rfl : Q' = q := hq.le ⟨hQ', ⟨hQ'p.symm⟩⟩

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
p : Ideal R
inst✝² : p.IsPrime
inst✝¹ : Algebra.IsIntegral R S
x : S
this : ∀ r ∉ p, ∀ (c : S), c * x ≠ (algebraMap R S) r
Q : Ideal S
hQ : Q.IsPrime
hxQ : span {x} ≤ Q
hQp : Disjoint ↑Q ↑(Algebra.algebraMapSubmonoid S p.primeCompl)
hQp' : under R Q ≤ p
Q' : Ideal S
hQ'Q : Q' ≥ Q
hQ' : Q'.IsPrime
hQ'p : comap (algebraMap R S) Q' = p
inst✝ : Q'.IsPrime
hq : p.primesOver S = {Q'}
hx : x ∉ Q'
⊢ False
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Ring A
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
inst✝¹ : NoZeroDivisors S
inst✝ : Algebra.IsAlgebraic R S
a : A
h : IsAlgebraic S a
p : S[X]
hp : p ≠ 0
eval0 : (aeval a) p = 0
hRS : FaithfulSMul R S
this✝¹ : NoZeroDivisors R
this✝ : Nontrivial R
this : IsDomain R
r : R
hr : r ≠ 0
int : ∀ z ∈ Finset.image p.coeff p.support, IsIntegral R (r • z)
s : S
hs : s ∈ ↑(r • p).coeffs
⊢ s ∈ ↑(integralClosure R S).toSubring

Tactic:
obtain ⟨n, hn, rfl⟩ := mem_coeffs_iff.mp hs

Goal state after:
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Ring A
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
inst✝¹ : NoZeroDivisors S
inst✝ : Algebra.IsAlgebraic R S
a : A
h : IsAlgebraic S a
p : S[X]
hp : p ≠ 0
eval0 : (aeval a) p = 0
hRS : FaithfulSMul R S
this✝¹ : NoZeroDivisors R
this✝ : Nontrivial R
this : IsDomain R
r : R
hr : r ≠ 0
int : ∀ z ∈ Finset.image p.coeff p.support, IsIntegral R (r • z)
n : ℕ
hn : n ∈ (r • p).support
hs : (r • p).coeff n ∈ ↑(r • p).coeffs
⊢ (r • p).coeff n ∈ ↑(integralClosure R S).toSubring
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N1 : Type u_1
inst✝⁵ : AddCommGroup N1
inst✝⁴ : Module R N1
N2 : Type u_2
inst✝³ : AddCommGroup N2
inst✝² : Module R N2
N3 : Type u_3
inst✝¹ : AddCommGroup N3
inst✝ : Module R N3
l12 : N1 →ₗ[R] N2
l23 : N2 →ₗ[R] N3
fl : FaithfullyFlat R M
ex : Function.Exact ⇑(LinearMap.rTensor M l12) ⇑(LinearMap.rTensor M l23)
⊢ l23.ker = l12.range

Tactic:
have complex : LinearMap.range l12 ≤ LinearMap.ker l23 := range_le_ker_of_exact_rTensor R M _ _ ex
  -- By the previous lemma we have that range l12 ≤ ker l23 and hence the quotient
  -- H := ker l23 ⧸ range l12 makes sense.
  -- Hence our goal ker l23 = range l12 follows from the claim that H = 0.
  let H := LinearMap.ker l23 ⧸ LinearMap.range (Submodule.inclusion complex)
  suffices triv_coh : Subsingleton H by
    rw [Submodule.Quotient.subsingleton_iff, Submodule.range_inclusion,
      Submodule.comap_subtype_eq_top] at triv_coh
    exact le_antisymm triv_coh complex
  -- Since `M` is faithfully flat, we need only to show that `H ⊗ M` is trivial.
  suffices Subsingleton (H ⊗[R] M) from rTensor_reflects_triviality R M H
  let e : H ⊗[R] M ≃ₗ[R] _ := TensorProduct.quotientTensorEquiv _ _
  -- Note that `H ⊗ M` is isomorphic to `ker l12 ⊗ M ⧸ range ((range l12 ⊗ M) -> (ker l23 ⊗ M))`.
  -- So the problem is reduced to proving surjectivity of `range l12 ⊗ M → ker l23 ⊗ M`.
  rw [e.toEquiv.subsingleton_congr, Submodule.Quotient.subsingleton_iff,
    LinearMap.range_eq_top]
  intro x
  induction x using TensorProduct.induction_on with
  | zero => exact ⟨0, by simp⟩
  -- let `x ⊗ m` be an element in `ker l23 ⊗ M`, then `x ⊗ m` is in the kernel of `l23 ⊗ 𝟙M`.
  -- Since `N1 ⊗ M -l12 ⊗ M-> N2 ⊗ M -l23 ⊗ M-> N3 ⊗ M` is exact, we have that `x ⊗ m` is in
  -- the range of `l12 ⊗ 𝟙M`, i.e. `x ⊗ m = (l12 ⊗ 𝟙M) y` for some `y ∈ N1 ⊗ M` as elements of
  -- `N2 ⊗ M`. We need to prove that `x ⊗ m = (l12 ⊗ 𝟙M) y` still holds in `(ker l23) ⊗ M`.
  -- This is okay because `M` is flat and `ker l23 -> N2` is injective.
  | tmul x m =>
    rcases x with ⟨x, (hx : l23 x = 0)⟩
    have mem : x ⊗ₜ[R] m ∈ LinearMap.ker (l23.rTensor M) := by simp [hx]
    rw [LinearMap.exact_iff.1 ex] at mem
    obtain ⟨y, hy⟩ := mem
    refine ⟨LinearMap.rTensor M (LinearMap.rangeRestrict _ ∘ₗ LinearMap.rangeRestrict l12) y,
      Module.Flat.rTensor_preserves_injective_linearMap (LinearMap.ker l23).subtype
      Subtype.val_injective ?_⟩
    simp only [LinearMap.comp_codRestrict, LinearMap.rTensor_tmul, Submodule.coe_subtype, ← hy]
    rw [← LinearMap.comp_apply, ← LinearMap.rTensor_def, ← LinearMap.rTensor_comp,
      ← LinearMap.comp_apply, ← LinearMap.rTensor_comp, LinearMap.comp_assoc,
      LinearMap.subtype_comp_codRestrict, ← LinearMap.comp_assoc, Submodule.subtype_comp_inclusion,
      LinearMap.subtype_comp_codRestrict]
  | add x y hx hy =>
    obtain ⟨x, rfl⟩ := hx; obtain ⟨y, rfl⟩ := hy
    exact ⟨x + y, by simp⟩

Goal state after:
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: case mp
R : Type u_1
inst✝⁹ : CommRing R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
K : Type u_4
inst✝⁶ : Field K
inst✝⁵ : IsDomain R
inst✝⁴ : Algebra R K
inst✝³ : Algebra S K
inst✝² : Module.IsTorsionFree R K
inst✝¹ : IsFractionRing S K
inst✝ : IsScalarTower R S K
h : ∀ (x : S), IsAlgebraic R x
this✝¹ : Nontrivial S := MulActionWithZero.nontrivial S K
this✝ : Algebra (FractionRing R) K := FractionRing.liftAlgebra R K
this : IsScalarTower R (FractionRing R) K
a b : S
ha : b ∈ nonZeroDivisors S
f : R[X]
hf₁ : f ≠ 0
hf₂ : (aeval b) f = 0
⊢ IsIntegral (FractionRing R) ((algebraMap S K) a / (algebraMap S K) b)

Tactic:
div_eq_mul_inv

Goal state after:
case mp
R : Type u_1
inst✝⁹ : CommRing R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
K : Type u_4
inst✝⁶ : Field K
inst✝⁵ : IsDomain R
inst✝⁴ : Algebra R K
inst✝³ : Algebra S K
inst✝² : Module.IsTorsionFree R K
inst✝¹ : IsFractionRing S K
inst✝ : IsScalarTower R S K
h : ∀ (x : S), IsAlgebraic R x
this✝¹ : Nontrivial S := MulActionWithZero.nontrivial S K
this✝ : Algebra (FractionRing R) K := FractionRing.liftAlgebra R K
this : IsScalarTower R (FractionRing R) K
a b : S
ha : b ∈ nonZeroDivisors S
f : R[X]
hf₁ : f ≠ 0
hf₂ : (aeval b) f = 0
⊢ IsIntegral (FractionRing R) ((algebraMap S K) a * ((algebraMap S K) b)⁻¹)
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: case pos
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
hA_nont : Nontrivial A
hgt : ∀ J > ⊤, J ≠ ⊥ → ∃ Z, (Multiset.map asIdeal Z).prod ≤ J ∧ (Multiset.map asIdeal Z).prod ≠ ⊥
h_nzI : ⊤ ≠ ⊥
⊢ ∃ Z, (Multiset.map asIdeal Z).prod ≤ ⊤ ∧ (Multiset.map asIdeal Z).prod ≠ ⊥

Tactic:
obtain ⟨p_id, h_nzp, h_pp⟩ : ∃ p : Ideal A, p ≠ ⊥ ∧ p.IsPrime := by
      apply Ring.not_isField_iff_exists_prime.mp h_fA

Goal state after:
case pos
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
hA_nont : Nontrivial A
hgt : ∀ J > ⊤, J ≠ ⊥ → ∃ Z, (Multiset.map asIdeal Z).prod ≤ J ∧ (Multiset.map asIdeal Z).prod ≠ ⊥
h_nzI : ⊤ ≠ ⊥
p_id : Ideal A
h_nzp : p_id ≠ ⊥
h_pp : p_id.IsPrime
⊢ ∃ Z, (Multiset.map asIdeal Z).prod ≤ ⊤ ∧ (Multiset.map asIdeal Z).prod ≠ ⊥
Module: Mathlib.RingTheory.LocalRing.ResidueField.Ideal

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : I.IsPrime
⊢ Function.Injective ⇑(algebraMap (R ⧸ I) I.ResidueField)

Tactic:
RingHom.injective_iff_ker_eq_bot

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : I.IsPrime
⊢ RingHom.ker (algebraMap (R ⧸ I) I.ResidueField) = ⊥
Module: Mathlib.RingTheory.Localization.AsSubring

Goal state before:
pp: A : Type u_1
K : Type u_2
inst✝⁶ : CommRing A
S : Submonoid A
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
hS : S ≤ A⁰
x : K
⊢ (∃ a s, ∃ (hs : s ∈ S), x = IsLocalization.mk' K a ⟨s, ⋯⟩) → x ∈ (mapToFractionRing K S B hS).range

Tactic:
by
    rintro ⟨a, s, hs, rfl⟩
    use IsLocalization.mk' _ a ⟨s, hs⟩
    apply IsLocalization.lift_mk'

Goal state after:
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
x : R
p : Ideal R
hxp : x ∈ p
hp₃ : ∀ ⦃y : Ideal R⦄, (fun q ↦ q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y
hp₁ : p.IsPrime
hp₂ : I ≤ p
this : map (algebraMap R (Localization.AtPrime p)) p ≤ (map (algebraMap R (Localization.AtPrime p)) I).radical
n : ℕ
a : ↥I
b t : ↥p.primeCompl
ht : ↑t * (x ^ n * ↑b) = ↑t * ↑a
⊢ (x * (↑t * ↑b)) ^ (n + 1) = ↑t ^ n * ↑b ^ n * x * (↑t * ↑a)

Tactic:
← ht

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
x : R
p : Ideal R
hxp : x ∈ p
hp₃ : ∀ ⦃y : Ideal R⦄, (fun q ↦ q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y
hp₁ : p.IsPrime
hp₂ : I ≤ p
this : map (algebraMap R (Localization.AtPrime p)) p ≤ (map (algebraMap R (Localization.AtPrime p)) I).radical
n : ℕ
a : ↥I
b t : ↥p.primeCompl
ht : ↑t * (x ^ n * ↑b) = ↑t * ↑a
⊢ (x * (↑t * ↑b)) ^ (n + 1) = ↑t ^ n * ↑b ^ n * x * (↑t * (x ^ n * ↑b))
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I J : Ideal S
h : J ∈ I.minimalPrimes
this✝ : J.IsPrime
K : Ideal R
hK : K.IsPrime
e₁ : comap f I ≤ K
e₂ : K ≤ comap f J
this : RingHom.ker f ≤ K
⊢ (map f K).IsPrime ∧ I ≤ map f K

Tactic:
exact ⟨Ideal.map_isPrime_of_surjective hf this, Ideal.le_map_of_comap_le_of_surjective f hf e₁⟩

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Maximal.Localization

Goal state before:
pp: R : Type u_4
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : K
⊢ x ∈ ⨅ v, Localization.subalgebra.ofField K v.asIdeal.primeCompl ⋯ ↔ x ∈ ⊥

Tactic:
rw [Algebra.mem_bot, Algebra.mem_iInf]

Goal state after:
R : Type u_4
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : K
⊢ (∀ (i : MaximalSpectrum R), x ∈ Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯) ↔
    x ∈ range ⇑(algebraMap R K)
Module: Mathlib.Topology.LocallyClosed

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ closure[inst✝] s ∪ closure[inst✝] (closure[inst✝] s)ᶜ = univ

Tactic:
← univ_subset_iff

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ univ ⊆ closure[inst✝] s ∪ closure[inst✝] (closure[inst✝] s)ᶜ
Module: Mathlib.Topology.LocalAtTarget

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
h : Continuous[inst✝¹, inst✝] f
⊢ (∀ (i : ι) (x : ↑(f ⁻¹' (U i).carrier)), 𝓝 x = Filter.comap Subtype.val (Filter.comap f (𝓝 ((f ∘ Subtype.val) x)))) →
    ∀ (x : α), 𝓝 x = Filter.comap f (𝓝 (f x))

Tactic:
intro H x

Goal state after:
case mpr
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
h : Continuous[inst✝¹, inst✝] f
H : ∀ (i : ι) (x : ↑(f ⁻¹' (U i).carrier)), 𝓝 x = Filter.comap Subtype.val (Filter.comap f (𝓝 ((f ∘ Subtype.val) x)))
x : α
⊢ 𝓝 x = Filter.comap f (𝓝 (f x))
Module: Mathlib.Topology.QuasiSeparated

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
ι : Type u_3
b : ι → Set α
basis : IsTopologicalBasis (range b)
isCompact_inter : ∀ (i j : ι), IsCompact (b i ∩ b j)
U V : Set α
hUopen : IsOpen[inst✝] U
hUcomp : IsCompact U
hVopen : IsOpen[inst✝] V
hVcomp : IsCompact V
⊢ IsCompact (U ∩ V)

Tactic:
by
    have aux := isCompact_open_iff_eq_finite_iUnion_of_isTopologicalBasis b basis fun i ↦ by
      simpa using isCompact_inter i i
    obtain ⟨s, hs, rfl⟩ := (aux _).1 ⟨hUcomp, hUopen⟩
    obtain ⟨t, ht, rfl⟩ := (aux _).1 ⟨hVcomp, hVopen⟩
    rw [iUnion₂_inter_iUnion₂]
    exact hs.isCompact_biUnion fun i hi ↦ ht.isCompact_biUnion fun j hj ↦ isCompact_inter ..

Goal state after:
Module: Mathlib.Order.Ideal

Goal state before:
pp: P : Type u_1
inst✝¹ : SemilatticeSup P
inst✝ : OrderBot P
x : P
S✝ S : Set (Ideal P)
s : Ideal P
hs : s ∈ lowerBounds S
⊢ s ≤ sInf S

Tactic:
by rwa [← coe_subset_coe, coe_sInf, subset_iInter₂_iff]

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: case compl
X : Type u_2
inst✝ : TopologicalSpace X
p : (s : Set X) → IsConstructible s → Prop
open_retrocompact : ∀ (U : Set X) (hUopen : IsOpen[inst✝] U) (hUcomp : IsRetrocompact U), p U ⋯
union : ∀ (s : Set X) (hs : IsConstructible s) (t : Set X) (ht : IsConstructible t), p s hs → p t ht → p (s ∪ t) ⋯
compl : ∀ (s : Set X) (hs : IsConstructible s), p s hs → p sᶜ ⋯
s✝ s : Set X
hs : s ∈ BooleanSubalgebra.closure {U | IsOpen[inst✝] U ∧ IsRetrocompact U}
hs' : p s hs
⊢ p sᶜ ⋯

Tactic:
| compl s hs hs' =>

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: case compl
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s✝ : Set Y
hfcont : Continuous[inst✝¹, inst✝] f
hf : ∀ (s : Set Y), IsOpen[inst✝] s → IsRetrocompact s → IsRetrocompact (f ⁻¹' s)
s : Set Y
hs : IsConstructible s
hs' : IsConstructible (f ⁻¹' s)
⊢ IsConstructible (f ⁻¹' sᶜ)

Tactic:
| compl s hs hs' =>

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: case compl
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s✝ : Set X
hfopen : IsOpenEmbedding f
hfcomp : IsRetrocompact (range f)
s : Set X
hs : IsConstructible s
hs' : IsConstructible (f '' s)
⊢ IsConstructible (f '' sᶜ)

Tactic:
| compl s hs hs' =>

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: case compl
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s✝ : Set X
hf : IsClosedEmbedding f
hfcomp : IsRetrocompact (range f)ᶜ
s : Set X
hs : IsConstructible s
hs' : IsConstructible (f '' s)
⊢ IsConstructible (f '' sᶜ)

Tactic:
| compl s hs hs' =>

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s t : Set (PrimeSpectrum R)
hs : IsClosed s
ht : IsClosed t
⊢ s ⊂ t ↔ vanishingIdeal t < vanishingIdeal s

Tactic:
rw [Set.ssubset_def, vanishingIdeal_anti_mono_iff hs, vanishingIdeal_anti_mono_iff ht,
    lt_iff_le_not_ge]

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case mpr
R : Type u
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsRadical
⊢ (∀ {x y : R}, x * y ∈ I → x ∉ I → y ∈ I) → ∀ (x y : Ideal R), x ⊓ y ≤ I → (∃ x_1 ∈ x, x_1 ∉ I) → y ≤ I

Tactic:
rintro h s t h' ⟨x, hx, hx'⟩ y hy

Goal state after:
case mpr
R : Type u
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsRadical
h : ∀ {x y : R}, x * y ∈ I → x ∉ I → y ∈ I
s t : Ideal R
h' : s ⊓ t ≤ I
x : R
hx : x ∈ s
hx' : x ∉ I
y : R
hy : y ∈ t
⊢ y ∈ I
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case refine_2
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
⊢ IsClosedMap ⇑(primeSpectrumProd R S).symm

Tactic:
simp_rw [isClosedMap_sum, primeSpectrumProd_symm_inl, primeSpectrumProd_symm_inr]

Goal state after:
case refine_2
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
⊢ (IsClosedMap fun a ↦ comap (RingHom.fst R S) a) ∧ IsClosedMap fun b ↦ comap (RingHom.snd R S) b
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
h₁ : Function.Surjective (comap f)
h₂ : SpecializingMap (comap f)
⊢ IsQuotientMap (comap f)

Tactic:
by
  rw [Topology.isQuotientMap_iff_isClosed]
  exact ⟨h₁, fun s ↦ ⟨fun hs ↦ hs.preimage (continuous_comap f),
    fun hsc ↦ Set.image_preimage_eq s h₁ ▸ isClosed_image_of_stableUnderSpecialization _ _ hsc
      (h₂.stableUnderSpecialization_image hsc.stableUnderSpecialization)⟩⟩

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
⊢ IsCompact s ∧ IsOpen s ↔ ∃ I, I.FG ∧ (zeroLocus ↑I)ᶜ = s

Tactic:
rw [isCompact_isOpen_iff]

Goal state after:
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
⊢ (∃ t, (zeroLocus ↑t)ᶜ = s) ↔ ∃ I, I.FG ∧ (zeroLocus ↑I)ᶜ = s