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

Goal state before:
pp: case zero
R : Type u_1
inst✝ : MonoidWithZero R
e : R
idem : IsIdempotentElem e
hn : 1 = 0
⊢ e = 0

Tactic:
rw [← one_mul e, hn, zero_mul]

Goal state after:
Module: Mathlib.RingTheory.Nilpotent.Basic

Goal state before:
pp: R : Type u_1
inst✝ : MonoidWithZero R
⊢ IsRadical 0 ↔ IsReduced R

Tactic:
simp_rw [isReduced_iff, IsNilpotent, exists_imp, ← zero_dvd_iff]
  exact forall_comm

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

Goal state before:
pp: case refine_2.succ
R : Type u_1
inst✝ : CommRing R
P p : R[X]
r : R
hp₀ : p.coeff 0 = 0
x✝ : r ≠ 0
hp : IsNilpotent p → ∀ (i : ℕ), IsNilpotent (p.coeff i)
hpr : IsNilpotent (p + C r)
hr : IsNilpotent (C r)
i : ℕ
⊢ IsNilpotent (p.coeff (i + 1))

Tactic:
apply hp

Goal state after:
case refine_2.succ
R : Type u_1
inst✝ : CommRing R
P p : R[X]
r : R
hp₀ : p.coeff 0 = 0
x✝ : r ≠ 0
hp : IsNilpotent p → ∀ (i : ℕ), IsNilpotent (p.coeff i)
hpr : IsNilpotent (p + C r)
hr : IsNilpotent (C r)
i : ℕ
⊢ IsNilpotent p
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap

Goal state before:
pp: case mpr
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
b : ι → M
inst✝ : DecidableEq ι
A : Matrix ι ι R
f : Module.End R M
h : ∀ (j : ι), ∑ i, A i j • b i = f (b j)
i✝ : ι
⊢ ((PiToModule.fromMatrix R b) A ∘ₗ LinearMap.single R (fun i ↦ R) i✝) 1 =
    ((PiToModule.fromEnd R b) f ∘ₗ LinearMap.single R (fun i ↦ R) i✝) 1

Tactic:
LinearMap.comp_apply,

Goal state after:
case mpr
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
b : ι → M
inst✝ : DecidableEq ι
A : Matrix ι ι R
f : Module.End R M
h : ∀ (j : ι), ∑ i, A i j • b i = f (b j)
i✝ : ι
⊢ ((PiToModule.fromMatrix R b) A) ((LinearMap.single R (fun i ↦ R) i✝) 1) =
    ((PiToModule.fromEnd R b) f) ((LinearMap.single R (fun i ↦ R) i✝) 1)
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap

Goal state before:
pp: ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
b : ι → M
inst✝ : DecidableEq ι
A A' : Matrix ι ι R
f f' : Module.End R M
h : Represents b A f
h' : Represents b A' f'
⊢ ((LinearMap.llcomp R (ι → R) (ι → R) M) (Fintype.linearCombination R b) ∘ₗ algEquivMatrix'.symm.toLinearMap)
      (A * A') =
    (PiToModule.fromEnd R b) (f * f')

Tactic:
LinearMap.comp_apply,

Goal state after:
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
b : ι → M
inst✝ : DecidableEq ι
A A' : Matrix ι ι R
f f' : Module.End R M
h : Represents b A f
h' : Represents b A' f'
⊢ ((LinearMap.llcomp R (ι → R) (ι → R) M) (Fintype.linearCombination R b)) (algEquivMatrix'.symm.toLinearMap (A * A')) =
    (PiToModule.fromEnd R b) (f * f')
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap

Goal state before:
pp: ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
b : ι → M
inst✝ : DecidableEq ι
⊢ ((LinearMap.llcomp R (ι → R) (ι → R) M) (Fintype.linearCombination R b) ∘ₗ algEquivMatrix'.symm.toLinearMap) 1 =
    (PiToModule.fromEnd R b) 1

Tactic:
LinearMap.comp_apply,

Goal state after:
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
b : ι → M
inst✝ : DecidableEq ι
⊢ ((LinearMap.llcomp R (ι → R) (ι → R) M) (Fintype.linearCombination R b)) (algEquivMatrix'.symm.toLinearMap 1) =
    (PiToModule.fromEnd R b) 1
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
c : n ≃ n
hc : c ∈ univ.erase (Equiv.refl n)
⊢ (∏ i, M.charmatrix (c i) i).natDegree ≤ #{x | c x = x}

Tactic:
apply le_trans (Polynomial.natDegree_prod_le univ fun i : n => charmatrix M (c i) i) _

Goal state after:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
c : n ≃ n
hc : c ∈ univ.erase (Equiv.refl n)
⊢ ∑ i, (M.charmatrix (c i) i).natDegree ≤ #{x | c x = x}
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
inst✝ : Nontrivial R
M : Matrix n n R
⊢ M.charpoly.degree = ↑(Fintype.card n)

Tactic:
by
  by_cases h : Fintype.card n = 0
  · rw [h]
    unfold charpoly
    rw [det_eq_one_of_card_eq_zero]
    · simp
    · assumption
  rw [← sub_add_cancel M.charpoly (∏ i : n, (X - C (M i i)))]
  -- Porting note: added `↑` in front of `Fintype.card n`
  have h1 : (∏ i : n, (X - C (M i i))).degree = ↑(Fintype.card n) := by
    rw [degree_eq_iff_natDegree_eq_of_pos (Nat.pos_of_ne_zero h), natDegree_prod']
    · simp_rw [natDegree_X_sub_C]
      rw [← Finset.card_univ, sum_const, smul_eq_mul, mul_one]
    simp_rw [(monic_X_sub_C _).leadingCoeff]
    simp
  rw [degree_add_eq_right_of_degree_lt]
  · exact h1
  rw [h1]
  apply lt_trans (charpoly_sub_diagonal_degree_lt M)
  rw [Nat.cast_lt]
  lia

Goal state after:
Module: Mathlib.Algebra.Module.SpanRank

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
σ : R →+* S
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
L : Type v
inst✝² : AddCommMonoid L
inst✝¹ : Module S L
inst✝ : RingHomSurjective σ
f : M →ₛₗ[σ] L
hf : Function.Injective ⇑f
p : Submodule R M
⊢ Cardinal.toNat (Cardinal.lift.{u, v} (map f p).spanRank) = Cardinal.toNat (Cardinal.lift.{v, u} p.spanRank)

Tactic:
lift_spanRank_map_eq_of_injective f hf p

Goal state after:
R : Type u_1
S : Type u_2
M : Type u
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
σ : R →+* S
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
L : Type v
inst✝² : AddCommMonoid L
inst✝¹ : Module S L
inst✝ : RingHomSurjective σ
f : M →ₛₗ[σ] L
hf : Function.Injective ⇑f
p : Submodule R M
⊢ Cardinal.toNat (Cardinal.lift.{v, u} p.spanRank) = Cardinal.toNat (Cardinal.lift.{v, u} p.spanRank)
Module: Mathlib.Algebra.Module.SpanRank

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid M
inst✝³ : Algebra R S
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
N : Submodule S M
⊢ N.spanRank ≤ (restrictScalars R N).spanRank

Tactic:
obtain ⟨s, hs, e⟩ := (N.restrictScalars R).exists_span_set_card_eq_spanRank

Goal state after:
R : Type u_1
S : Type u_2
M : Type u
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid M
inst✝³ : Algebra R S
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
N : Submodule S M
s : Set M
hs : Cardinal.mk ↑s = (restrictScalars R N).spanRank
e : span R s = restrictScalars R N
⊢ N.spanRank ≤ (restrictScalars R N).spanRank
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
⊢ M.det = (-1) ^ Fintype.card n * (eval ((scalar n) 0) (matPolyEquiv M.charmatrix)).det

Tactic:
matPolyEquiv_charmatrix,

Goal state after:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
⊢ M.det = (-1) ^ Fintype.card n * (eval ((scalar n) 0) (X - C M)).det
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
⊢ (1 + X • M.map ⇑C).det = 1 + M.trace • X + (1 + X • M.map ⇑C).det.divX.divX * X ^ 2

Tactic:
Algebra.smul_def (trace M),

Goal state after:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
⊢ (1 + X • M.map ⇑C).det = 1 + (algebraMap R R[X]) M.trace * X + (1 + X • M.map ⇑C).det.divX.divX * X ^ 2
Module: Mathlib.Data.Nat.Factorial.Cast

Goal state before:
pp: case succ
S : Type u_1
inst✝ : Ring S
n✝ : ℕ
⊢ ↑((n✝ + 1 - 1) * (n✝ + 1).descFactorial 1) = ↑(n✝ + 1) * (↑(n✝ + 1) - 1)

Tactic:
· simp [mul_add, add_mul]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : Semiring S
inst✝ : CommSemiring R
p : S[X]
f : S →+* R
r : R
s : S
hr : eval₂ f r p = 0
⊢ f s ^ p.natDegree * eval₂ f r p = 0

Tactic:
hr,

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : Semiring S
inst✝ : CommSemiring R
p : S[X]
f : S →+* R
r : R
s : S
hr : eval₂ f r p = 0
⊢ f s ^ p.natDegree * 0 = 0
Module: Mathlib.RingTheory.Polynomial.ScaleRoots

Goal state before:
pp: case h
R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
hr : IsUnit r
a b : R[X]
e : a * p + b * q = 1
s : R := ⋯
this : (a * p).natDegree = (b * q).natDegree
⊢ s ^ (a * p).natDegree • s ^ (a.natDegree + p.natDegree - (a * p).natDegree) • a.scaleRoots r * p.scaleRoots r +
      s ^ (a * p).natDegree • s ^ (b.natDegree + q.natDegree - (b * q).natDegree) • b.scaleRoots r * q.scaleRoots r =
    1

Tactic:
simp only [smul_smul, smul_mul_assoc, ← mul_scaleRoots, mul_assoc, ← mul_pow, IsUnit.val_inv_mul,
    one_pow, mul_one, ← smul_add, ← add_scaleRoots_of_natDegree_eq _ _ _ this, e, natDegree_one,
    Nat.sub_zero, one_scaleRoots, one_smul, s]

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

Goal state before:
pp: case e
R : Type u_1
B : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring B
inst✝ : Algebra R B
x y : B
r : R
hr : y * (algebraMap R B) r = 1
p : R[X]
p_monic : p.Monic
hp : eval₂ (algebraMap R B) (x * y) p = 0
⊢ eval₂ (algebraMap R B) x = ⇑(aeval (x * (y * (algebraMap R B) r)))

Tactic:
hr,

Goal state after:
case e
R : Type u_1
B : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring B
inst✝ : Algebra R B
x y : B
r : R
hr : y * (algebraMap R B) r = 1
p : R[X]
p_monic : p.Monic
hp : eval₂ (algebraMap R B) (x * y) p = 0
⊢ eval₂ (algebraMap R B) x = ⇑(aeval (x * 1))
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
K : Type u_4
inst✝³ : CommRing K
inst✝² : Algebra S K
inst✝¹ : Algebra R K
inst✝ : IsIntegralClosure S R K
x : K
hx : IsAlgebraic R x
⊢ ∃ r s, r ≠ 0 ∧ r • x = (algebraMap S K) s

Tactic:
obtain ⟨r, hr, h⟩ := hx.exists_integral_multiple
  obtain ⟨s, hs⟩ := IsIntegralClosure.isIntegral_iff (A := S) |>.mp h
  exact ⟨r, s, hr, hs.symm⟩

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

Goal state before:
pp: case refine_3
R : Type u_1
inst✝¹⁵ : CommRing R
S : Type u_2
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
Rf : Type u_5
Sf : Type u_6
inst✝¹² : CommRing Rf
inst✝¹¹ : CommRing Sf
inst✝¹⁰ : Algebra R Rf
inst✝⁹ : Algebra S Sf
inst✝⁸ : Algebra Rf Sf
inst✝⁷ : Algebra R Sf
inst✝⁶ : IsScalarTower R S Sf
inst✝⁵ : IsScalarTower R Rf Sf
M : Submonoid R
inst✝⁴ : IsLocalization M Rf
inst✝³ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sf
inst✝² : Algebra ↥(integralClosure R S) ↥(integralClosure Rf Sf)
inst✝¹ : IsScalarTower (↥(integralClosure R S)) (↥(integralClosure Rf Sf)) Sf
inst✝ : IsScalarTower R ↥(integralClosure R S) ↥(integralClosure Rf Sf)
a : S
ha : a ∈ integralClosure R S
b : S
hb : b ∈ integralClosure R S
e :
  (algebraMap ↥(integralClosure R S) ↥(integralClosure Rf Sf)) ⟨a, ha⟩ =
    (algebraMap ↥(integralClosure R S) ↥(integralClosure Rf Sf)) ⟨b, hb⟩
this✝ :
  (algebraMap (↥(integralClosure Rf Sf)) Sf) ((algebraMap ↥(integralClosure R S) ↥(integralClosure Rf Sf)) ⟨a, ha⟩) =
    (algebraMap (↥(integralClosure Rf Sf)) Sf) ((algebraMap ↥(integralClosure R S) ↥(integralClosure Rf Sf)) ⟨b, hb⟩)
this : (algebraMap S Sf) a = (algebraMap S Sf) b
⊢ ∃ c, ↑c * ⟨a, ha⟩ = ↑c * ⟨b, hb⟩

Tactic:
obtain ⟨⟨_, m, hm, rfl⟩, h⟩ :=
      (IsLocalization.eq_iff_exists (Algebra.algebraMapSubmonoid S M) _).mp this

Goal state after:
case refine_3
R : Type u_1
inst✝¹⁵ : CommRing R
S : Type u_2
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
Rf : Type u_5
Sf : Type u_6
inst✝¹² : CommRing Rf
inst✝¹¹ : CommRing Sf
inst✝¹⁰ : Algebra R Rf
inst✝⁹ : Algebra S Sf
inst✝⁸ : Algebra Rf Sf
inst✝⁷ : Algebra R Sf
inst✝⁶ : IsScalarTower R S Sf
inst✝⁵ : IsScalarTower R Rf Sf
M : Submonoid R
inst✝⁴ : IsLocalization M Rf
inst✝³ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sf
inst✝² : Algebra ↥(integralClosure R S) ↥(integralClosure Rf Sf)
inst✝¹ : IsScalarTower (↥(integralClosure R S)) (↥(integralClosure Rf Sf)) Sf
inst✝ : IsScalarTower R ↥(integralClosure R S) ↥(integralClosure Rf Sf)
a : S
ha : a ∈ integralClosure R S
b : S
hb : b ∈ integralClosure R S
e :
  (algebraMap ↥(integralClosure R S) ↥(integralClosure Rf Sf)) ⟨a, ha⟩ =
    (algebraMap ↥(integralClosure R S) ↥(integralClosure Rf Sf)) ⟨b, hb⟩
this✝ :
  (algebraMap (↥(integralClosure Rf Sf)) Sf) ((algebraMap ↥(integralClosure R S) ↥(integralClosure Rf Sf)) ⟨a, ha⟩) =
    (algebraMap (↥(integralClosure Rf Sf)) Sf) ((algebraMap ↥(integralClosure R S) ↥(integralClosure Rf Sf)) ⟨b, hb⟩)
this : (algebraMap S Sf) a = (algebraMap S Sf) b
m : R
hm : m ∈ ↑M
h : ↑⟨(algebraMap R S) m, ⋯⟩ * a = ↑⟨(algebraMap R S) m, ⋯⟩ * b
⊢ ∃ c, ↑c * ⟨a, ha⟩ = ↑c * ⟨b, hb⟩
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
alg : Algebra.IsAlgebraic R S
inst✝¹ : IsDomain S
inst✝ : FaithfulSMul R S
σ : Type u
⊢ Module.rank (FractionRing (MvPolynomial σ R)) (FractionRing (MvPolynomial σ S)) = lift.{u, u_2} (Module.rank R S)

Tactic:
by
  have := IsDomain.of_faithfulSMul R S
  rw [rank_fractionRing, rank_mvPolynomial_mvPolynomial]

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

Goal state before:
pp: case neg
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
M : Ideal A
hgt : ∀ J > M, J ≠ ⊥ → ∃ Z, (Multiset.map asIdeal Z).prod ≤ J ∧ (Multiset.map asIdeal Z).prod ≠ ⊥
h_nzI : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
h_prM : ¬M.IsPrime
x : A
hx : x ∉ M
y : A
hy : y ∉ M
h_xy : x * y ∈ M
⊢ ∃ Z, (Multiset.map asIdeal Z).prod ≤ M ∧ (Multiset.map asIdeal Z).prod ≠ ⊥

Tactic:
have lt_add : ∀ z ∉ M, M < M + span A {z} := by
    intro z hz
    refine lt_of_le_of_ne le_sup_left fun m_eq => hz ?_
    rw [m_eq]
    exact mem_sup_right (mem_span_singleton_self z)

Goal state after:
case neg
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
M : Ideal A
hgt : ∀ J > M, J ≠ ⊥ → ∃ Z, (Multiset.map asIdeal Z).prod ≤ J ∧ (Multiset.map asIdeal Z).prod ≠ ⊥
h_nzI : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
h_prM : ¬M.IsPrime
x : A
hx : x ∉ M
y : A
hy : y ∉ M
h_xy : x * y ∈ M
lt_add : ∀ z ∉ M, M < M + A ∙ z
⊢ ∃ Z, (Multiset.map asIdeal Z).prod ≤ M ∧ (Multiset.map asIdeal Z).prod ≠ ⊥
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: case neg
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
M : Ideal A
hgt : ∀ J > M, J ≠ ⊥ → ∃ Z, (Multiset.map asIdeal Z).prod ≤ J ∧ (Multiset.map asIdeal Z).prod ≠ ⊥
h_nzI : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
h_prM : ¬M.IsPrime
x : A
hx : x ∉ M
y : A
hy : y ∉ M
h_xy : x * y ∈ M
lt_add : ∀ z ∉ M, M < M + A ∙ z
⊢ ∃ Z, (Multiset.map asIdeal Z).prod ≤ M ∧ (Multiset.map asIdeal Z).prod ≠ ⊥

Tactic:
obtain ⟨Wx, h_Wx_le, h_Wx_ne⟩ := hgt (M + span A {x}) (lt_add _ hx) (ne_bot_of_gt (lt_add _ hx))

Goal state after:
case neg
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
M : Ideal A
hgt : ∀ J > M, J ≠ ⊥ → ∃ Z, (Multiset.map asIdeal Z).prod ≤ J ∧ (Multiset.map asIdeal Z).prod ≠ ⊥
h_nzI : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
h_prM : ¬M.IsPrime
x : A
hx : x ∉ M
y : A
hy : y ∉ M
h_xy : x * y ∈ M
lt_add : ∀ z ∉ M, M < M + A ∙ z
Wx : Multiset (PrimeSpectrum A)
h_Wx_le : (Multiset.map asIdeal Wx).prod ≤ M + A ∙ x
h_Wx_ne : (Multiset.map asIdeal Wx).prod ≠ ⊥
⊢ ∃ Z, (Multiset.map asIdeal Z).prod ≤ M ∧ (Multiset.map asIdeal Z).prod ≠ ⊥
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: case h.refine_2
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
M : Ideal A
hgt : ∀ J > M, J ≠ ⊥ → ∃ Z, (Multiset.map asIdeal Z).prod ≤ J ∧ (Multiset.map asIdeal Z).prod ≠ ⊥
h_nzI : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
h_prM : ¬M.IsPrime
x : A
hx : x ∉ M
y : A
hy : y ∉ M
h_xy : x * y ∈ M
lt_add : ∀ z ∉ M, M < M + A ∙ z
Wx : Multiset (PrimeSpectrum A)
h_Wx_le : (Multiset.map asIdeal Wx).prod ≤ M + A ∙ x
h_Wx_ne✝ : (Multiset.map asIdeal Wx).prod ≠ ⊥
Wy : Multiset (PrimeSpectrum A)
h_Wy_le : (Multiset.map asIdeal Wy).prod ≤ M + A ∙ y
h_Wx_ne : (Multiset.map asIdeal Wy).prod ≠ ⊥
⊢ ¬((Multiset.map asIdeal Wx).prod = ⊥ ∨ (Multiset.map asIdeal Wy).prod = ⊥)

Tactic:
rintro (hx | hy) <;> contradiction

Goal state after:
Module: Mathlib.RingTheory.SurjectiveOnStalks

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommRing R
S : Type u_2
inst✝⁷ : CommRing S
T : Type u_3
inst✝⁶ : CommRing T
S' : Type u_4
T' : Type u_5
inst✝⁵ : CommRing S'
inst✝⁴ : CommRing T'
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : Algebra R S'
inst✝ : Algebra R T'
f : S →ₐ[R] S'
Hf : f.SurjectiveOnStalks
g : T →ₐ[R] T'
Hg : g.SurjectiveOnStalks
⊢ (Algebra.TensorProduct.map f g).toRingHom =
    (Algebra.TensorProduct.map f (AlgHom.id R T')).comp
      ((Algebra.TensorProduct.comm R T' S).toRingEquiv.toRingHom.comp
        ((Algebra.TensorProduct.map g (AlgHom.id R S)).comp (Algebra.TensorProduct.comm R S T).toRingEquiv.toRingHom))

Tactic:
simp only [AlgHom.toRingHom_eq_coe, RingEquiv.toRingHom_eq_coe,
    AlgEquiv.toRingEquiv_toRingHom, ← AlgEquiv.toAlgHom_toRingHom, ← AlgHom.comp_toRingHom]

Goal state after:
R : Type u_1
inst✝⁸ : CommRing R
S : Type u_2
inst✝⁷ : CommRing S
T : Type u_3
inst✝⁶ : CommRing T
S' : Type u_4
T' : Type u_5
inst✝⁵ : CommRing S'
inst✝⁴ : CommRing T'
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : Algebra R S'
inst✝ : Algebra R T'
f : S →ₐ[R] S'
Hf : f.SurjectiveOnStalks
g : T →ₐ[R] T'
Hg : g.SurjectiveOnStalks
⊢ ↑(Algebra.TensorProduct.map f g) =
    ↑((Algebra.TensorProduct.map f (AlgHom.id R T')).comp
        ((↑(Algebra.TensorProduct.comm R T' S)).comp
          ((Algebra.TensorProduct.map g (AlgHom.id R S)).comp ↑(Algebra.TensorProduct.comm R S T))))
Module: Mathlib.RingTheory.LocalRing.ResidueField.Ideal

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R A
inst✝¹ : Algebra R B
I : Ideal R
inst✝ : I.IsPrime
x y : R
e : (algebraMap (R ⧸ I) I.ResidueField) ((Ideal.Quotient.mk I) x - (Ideal.Quotient.mk I) y) = 0
⊢ ∃ c, ↑c * (Ideal.Quotient.mk I) x = ↑c * (Ideal.Quotient.mk I) y

Tactic:
← map_sub

Goal state after:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R A
inst✝¹ : Algebra R B
I : Ideal R
inst✝ : I.IsPrime
x y : R
e : (algebraMap (R ⧸ I) I.ResidueField) ((Ideal.Quotient.mk I) (x - y)) = 0
⊢ ∃ c, ↑c * (Ideal.Quotient.mk I) x = ↑c * (Ideal.Quotient.mk I) y
Module: Mathlib.RingTheory.Spectrum.Prime.RingHom

Goal state before:
pp: ι : Type u_3
R : ι → Type u_4
inst✝² : (i : ι) → CommRing (R i)
inst✝¹ : _root_.Finite ι
S : Type u_5
inst✝ : CommRing S
f : S →+* (i : ι) → R i
⊢ ⋃ i, Set.range (comap ((Pi.evalRingHom R i).comp f)) = Set.range (comap f)

Tactic:
simp_rw [comap_comp]
  apply subset_antisymm
  · exact Set.iUnion_subset fun _ ↦ Set.range_comp_subset_range _ _
  · rintro _ ⟨p, rfl⟩
    obtain ⟨i, p, rfl⟩ := exists_comap_evalRingHom_eq p
    exact Set.mem_iUnion_of_mem i ⟨p, rfl⟩

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Surjective ⇑f
I : Ideal R
hI : ker f = I
a b : PrimeSpectrum S
⊢ a.asIdeal ≤ b.asIdeal ↔ a ≤ b

Tactic:
PrimeSpectrum.asIdeal_le_asIdeal

Goal state after:
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Surjective ⇑f
I : Ideal R
hI : ker f = I
a b : PrimeSpectrum S
⊢ a ≤ b ↔ a ≤ b
Module: Mathlib.Topology.Sets.Opens

Goal state before:
pp: case mpr.refine_2
α : Type u_2
inst✝ : TopologicalSpace α
B : Set (Opens α)
h : ∀ {U : Opens α} {x : α}, x ∈ U → ∃ U' ∈ B, x ∈ U' ∧ U' ≤ U
⊢ ∀ (a : α) (u : Set α), a ∈ u → IsOpen[inst✝] u → ∃ v ∈ SetLike.coe '' B, a ∈ v ∧ v ⊆ u

Tactic:
· intro x sU hx hsU
      rcases @h ⟨sU, hsU⟩ x hx with ⟨V, hV, H⟩
      exact ⟨V, ⟨V, hV, rfl⟩, H⟩

Goal state after:
Module: Mathlib.Topology.Sets.Opens

Goal state before:
pp: case mp
α : Type u_2
inst✝ : TopologicalSpace α
B : Set (Opens α)
hB : IsBasis B
U : Opens α
⊢ ↑U = ⋃ i ∈ {V | V ∈ B ∧ V ≤ U}, ↑i

Tactic:
hB.open_eq_sUnion' U.isOpen

Goal state after:
case mp
α : Type u_2
inst✝ : TopologicalSpace α
B : Set (Opens α)
hB : IsBasis B
U : Opens α
⊢ ⋃₀ {s | s ∈ SetLike.coe '' B ∧ s ⊆ ↑U} = ⋃ i ∈ {V | V ∈ B ∧ V ≤ U}, ↑i
Module: Mathlib.Topology.Sets.Closeds

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : β → α
hf : IsInducing f
A B : IrreducibleCloseds β
h_images_eq : map f ⋯ A = map f ⋯ B
⊢ ↑A = ↑B

Tactic:
replace h_images_eq : closure (f '' A) = closure (f '' B) := congr($h_images_eq)

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : β → α
hf : IsInducing f
A B : IrreducibleCloseds β
h_images_eq : closure[inst✝¹] (f '' ↑A) = closure[inst✝¹] (f '' ↑B)
⊢ ↑A = ↑B
Module: Mathlib.Order.BooleanSubalgebra

Goal state before:
pp: case h
α : Type u_2
inst✝ : BooleanAlgebra α
s : Set α
isSublattice : IsSublattice s
bot_mem : ⊥ ∈ s
top_mem : ⊤ ∈ s
a : α
t✝¹ : Finset (↑s × ↑s)
x✝⁵ : ↑s × ↑s
t✝ : Finset (↑s × ↑s)
x✝⁴ : ∃ t, (t✝.sup fun x ↦ ↑x.1 \ ↑x.2)ᶜ = t.sup fun x ↦ ↑x.1 \ ↑x.2
x y : ↑s
x✝³ : (x, y) ∉ t✝
tc✝ : Finset (↑s × ↑s)
eq✝ : (t✝.sup fun x ↦ ↑x.1 \ ↑x.2)ᶜ = tc✝.sup fun x ↦ ↑x.1 \ ↑x.2
x✝² : ↑s × ↑s
tc : Finset (↑s × ↑s)
x✝¹ : ∃ t, ((↑x \ ↑y)ᶜ ⊓ tc.sup fun x ↦ ↑x.1 \ ↑x.2) = t.sup fun x ↦ ↑x.1 \ ↑x.2
z w : ↑s
x✝ : (z, w) ∉ tc
t : Finset (↑s × ↑s)
eq : ((↑x \ ↑y)ᶜ ⊓ tc.sup fun x ↦ ↑x.1 \ ↑x.2) = t.sup fun x ↦ ↑x.1 \ ↑x.2
⊢ (((↑x)ᶜ ⊔ ↑y) ⊓ (↑z ⊓ (↑w)ᶜ) ⊔ t.sup fun x ↦ ↑x.1 ⊓ (↑x.2)ᶜ) =
    (↑x)ᶜ ⊓ (↑z ⊓ (↑w)ᶜ) ⊔ ↑y ⊓ ↑z ⊓ (↑w)ᶜ ⊔ t.sup fun x ↦ ↑x.1 ⊓ (↑x.2)ᶜ

Tactic:
inf_sup_right,

Goal state after:
case h
α : Type u_2
inst✝ : BooleanAlgebra α
s : Set α
isSublattice : IsSublattice s
bot_mem : ⊥ ∈ s
top_mem : ⊤ ∈ s
a : α
t✝¹ : Finset (↑s × ↑s)
x✝⁵ : ↑s × ↑s
t✝ : Finset (↑s × ↑s)
x✝⁴ : ∃ t, (t✝.sup fun x ↦ ↑x.1 \ ↑x.2)ᶜ = t.sup fun x ↦ ↑x.1 \ ↑x.2
x y : ↑s
x✝³ : (x, y) ∉ t✝
tc✝ : Finset (↑s × ↑s)
eq✝ : (t✝.sup fun x ↦ ↑x.1 \ ↑x.2)ᶜ = tc✝.sup fun x ↦ ↑x.1 \ ↑x.2
x✝² : ↑s × ↑s
tc : Finset (↑s × ↑s)
x✝¹ : ∃ t, ((↑x \ ↑y)ᶜ ⊓ tc.sup fun x ↦ ↑x.1 \ ↑x.2) = t.sup fun x ↦ ↑x.1 \ ↑x.2
z w : ↑s
x✝ : (z, w) ∉ tc
t : Finset (↑s × ↑s)
eq : ((↑x \ ↑y)ᶜ ⊓ tc.sup fun x ↦ ↑x.1 \ ↑x.2) = t.sup fun x ↦ ↑x.1 \ ↑x.2
⊢ ((↑x)ᶜ ⊓ (↑z ⊓ (↑w)ᶜ) ⊔ ↑y ⊓ (↑z ⊓ (↑w)ᶜ) ⊔ t.sup fun x ↦ ↑x.1 ⊓ (↑x.2)ᶜ) =
    (↑x)ᶜ ⊓ (↑z ⊓ (↑w)ᶜ) ⊔ ↑y ⊓ ↑z ⊓ (↑w)ᶜ ⊔ t.sup fun x ↦ ↑x.1 ⊓ (↑x.2)ᶜ
Module: Mathlib.Topology.Spectral.Hom

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f g : SpectralMap α β
h : f.toFun = g.toFun
⊢ f = g

Tactic:
cases f

Goal state after:
case mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
g : SpectralMap α β
toFun✝ : α → β
spectral'✝ : IsSpectralMap toFun✝
h : { toFun := toFun✝, spectral' := spectral'✝ }.toFun = g.toFun
⊢ { toFun := toFun✝, spectral' := spectral'✝ } = g
Module: Mathlib.Topology.Sober

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
x : α
S : Set α
h : IsGenericPoint x S
f : α → β
hf : Continuous f
⊢ closure (f '' {x}) = closure (f '' closure {x})

Tactic:
closure_image_closure hf

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
x : α
S : Set α
h : IsGenericPoint x S
f : α → β
hf : Continuous f
⊢ closure (f '' {x}) = closure (f '' {x})