mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
⊢ IsUnit A⁻¹ ↔ IsUnit A

Tactic:
isUnit_iff_isUnit_det,

Goal state after:
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
⊢ IsUnit A⁻¹.det ↔ IsUnit A.det
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
b : n → α
h : IsUnit A.det
⊢ A.det • A⁻¹ *ᵥ b = A.cramer b

Tactic:
rw [cramer_eq_adjugate_mulVec, A.nonsing_inv_apply h, ← smul_mulVec, smul_smul,
    h.mul_val_inv, one_smul]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
P : R[X]
hunit : IsUnit (P.coeff 0)
hnil : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (P.coeff i)
⊢ IsUnit P

Tactic:
induction h : P.natDegree using Nat.strong_induction_on generalizing P with | _ k hind

Goal state after:
case h
R : Type u_1
inst✝ : CommRing R
k : ℕ
hind :
  ∀ m < k, ∀ {P : R[X]}, IsUnit (P.coeff 0) → (∀ (i : ℕ), i ≠ 0 → IsNilpotent (P.coeff i)) → P.natDegree = m → IsUnit P
P : R[X]
hunit : IsUnit (P.coeff 0)
hnil : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (P.coeff i)
h : P.natDegree = k
⊢ IsUnit P
Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic

Goal state before:
pp: R : Type u_5
S : Type u_6
T : Type u_7
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra T S
φ : R ≃+* T
h : (algebraMap T S).comp φ.toRingHom = algebraMap R S
a : S
ha : IsIntegral R a
this : Algebra R T := φ.toRingHom.toAlgebra
r : R
t : T
s : S
⊢ (r • t) • s = r • t • s

Tactic:
simp only [Algebra.smul_def, map_mul, ← h, mul_assoc]

Goal state after:
R : Type u_5
S : Type u_6
T : Type u_7
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra T S
φ : R ≃+* T
h : (algebraMap T S).comp φ.toRingHom = algebraMap R S
a : S
ha : IsIntegral R a
this : Algebra R T := φ.toRingHom.toAlgebra
r : R
t : T
s : S
⊢ (algebraMap T S) ((algebraMap R T) r) * ((algebraMap T S) t * s) =
    ((algebraMap T S).comp φ.toRingHom) r * ((algebraMap T S) t * s)
Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic

Goal state before:
pp: case mpr
R : Type u_5
S : Type u_6
T : Type u_7
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra T S
φ : R ≃+* T
h : (algebraMap T S).comp φ.toRingHom = algebraMap R S
a : S
ha : IsIntegral T a
⊢ IsIntegral R a

Tactic:
· have h' : (algebraMap T S) = (algebraMap R S).comp φ.symm.toRingHom := by
      have : RingHomInvPair (φ : R →+* T) φ.symm := RingHomInvPair.of_ringEquiv _
      simp only [← h, RingHom.comp_assoc, RingEquiv.toRingHom_eq_coe, RingHomCompTriple.comp_eq]
    let : Algebra T R := φ.symm.toRingHom.toAlgebra
    let : IsScalarTower T R S :=
      ⟨fun r t s ↦ by simp only [Algebra.smul_def, map_mul, h', mul_assoc]; rfl⟩
    exact IsIntegral.tower_top ha

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
inst✝ : Nontrivial R
hn : Fintype.card n = 2
this✝ : Nonempty n
i : ℕ
hi : 2 < i
this : M.charpoly.coeff i = 0
⊢ M.charpoly.coeff i = (X ^ 2 - C M.trace * X + C M.det).coeff i

Tactic:
by
      simpa [show i ≠ 2 by lia, show 1 ≠ i by lia, show i ≠ 0 by lia, coeff_X, coeff_C]

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
hlifts : ∀ (n : ℕ), p.coeff n ∈ Set.range ⇑f
g : ℕ → R := fun k ↦ Exists.choose ⋯
hg : ∀ (k : ℕ), f (g k) = p.coeff k
q : R[X] := ∑ k ∈ p.support, (monomial k) (g k)
⊢ map f (∑ k ∈ p.support, (monomial k) (g k)) = p

Tactic:
Polynomial.map_sum,

Goal state after:
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
hlifts : ∀ (n : ℕ), p.coeff n ∈ Set.range ⇑f
g : ℕ → R := fun k ↦ Exists.choose ⋯
hg : ∀ (k : ℕ), f (g k) = p.coeff k
q : R[X] := ∑ k ∈ p.support, (monomial k) (g k)
⊢ ∑ i ∈ p.support, map f ((monomial i) (g i)) = p
Module: Mathlib.Algebra.Polynomial.Lifts

Goal state before:
pp: R : Type u
inst✝² : Semiring R
S : Type v
inst✝¹ : Semiring S
f : R →+* S
inst✝ : Nontrivial S
p : S[X]
hlifts : ∀ (n : ℕ), p.coeff n ∈ Set.range ⇑f
hp : p.Monic
g : ℕ → R := fun k ↦ Exists.choose ⋯
hg : ∀ (k : ℕ), f (g k) = p.coeff k
q : R[X] := X ^ p.natDegree + ∑ k ∈ Finset.range p.natDegree, C (g k) * X ^ k
⊢ map f (X ^ p.natDegree) + map f (∑ k ∈ Finset.range p.natDegree, C (g k) * X ^ k) = p

Tactic:
Polynomial.map_sum,

Goal state after:
R : Type u
inst✝² : Semiring R
S : Type v
inst✝¹ : Semiring S
f : R →+* S
inst✝ : Nontrivial S
p : S[X]
hlifts : ∀ (n : ℕ), p.coeff n ∈ Set.range ⇑f
hp : p.Monic
g : ℕ → R := fun k ↦ Exists.choose ⋯
hg : ∀ (k : ℕ), f (g k) = p.coeff k
q : R[X] := X ^ p.natDegree + ∑ k ∈ Finset.range p.natDegree, C (g k) * X ^ k
⊢ map f (X ^ p.natDegree) + ∑ i ∈ Finset.range p.natDegree, map f (C (g i) * X ^ i) = p
Module: Mathlib.Algebra.Polynomial.HasseDeriv

Goal state before:
pp: case succ
R : Type u_1
inst✝ : Semiring R
k✝ k : ℕ
ih : ⇑(k ! • hasseDeriv k) = (⇑derivative)^[k]
f : R[X]
n : ℕ
⊢ (k + 1)! • (↑((n + (k + 1)).choose (k + 1)) * f.coeff (n + (k + 1))) =
    k ! • (↑((n + 1 + k).choose (n + 1)) * f.coeff (n + 1 + k) * (↑n + 1))

Tactic:
simp only [nsmul_eq_mul, factorial_succ, mul_assoc, succ_eq_add_one, ← add_assoc,
    add_right_comm n 1 k, ← cast_succ]

Goal state after:
case succ
R : Type u_1
inst✝ : Semiring R
k✝ k : ℕ
ih : ⇑(k ! • hasseDeriv k) = (⇑derivative)^[k]
f : R[X]
n : ℕ
⊢ ↑((k + 1) * k !) * (↑((n + k + 1).choose (k + 1)) * f.coeff (n + k + 1)) =
    ↑k ! * (↑((n + k + 1).choose (n + 1)) * (f.coeff (n + k + 1) * ↑(n + 1)))
Module: Mathlib.RingTheory.Polynomial.ScaleRoots

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
n : ℕ
⊢ ∀ x ∈ Finset.antidiagonal n,
    p.coeff x.1 * q.coeff x.2 * r ^ (p.natDegree + q.natDegree - n) =
      (p.scaleRoots r).coeff x.1 * (q.scaleRoots r).coeff x.2

Tactic:
simp only [Finset.mem_antidiagonal, coeff_scaleRoots, Prod.forall]

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
n : ℕ
⊢ ∀ (a b : ℕ),
    a + b = n →
      p.coeff a * q.coeff b * r ^ (p.natDegree + q.natDegree - n) =
        p.coeff a * r ^ (p.natDegree - a) * (q.coeff b * r ^ (q.natDegree - b))
Module: Mathlib.RingTheory.TensorProduct.MvPolynomial

Goal state before:
pp: case add
R : Type u
N : Type v
inst✝⁴ : CommSemiring R
σ : Type u_1
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : CommSemiring N
inst✝ : Algebra R N
f : σ → S
p q : MvPolynomial σ R
hp : (aeval fun x ↦ 1 ⊗ₜ[R] f x) p = 1 ⊗ₜ[R] (aeval f) p
hq : (aeval fun x ↦ 1 ⊗ₜ[R] f x) q = 1 ⊗ₜ[R] (aeval f) q
⊢ (aeval fun x ↦ 1 ⊗ₜ[R] f x) (p + q) = 1 ⊗ₜ[R] (aeval f) (p + q)

Tactic:
simp [hp, hq, tmul_add]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
hf : f.Splits
hm : f.Monic
⊢ f = (Multiset.map (fun x ↦ X - C x) f.roots).prod

Tactic:
conv_lhs => rw [hf.eq_prod_roots, hm.leadingCoeff, C_1, one_mul]

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

Goal state before:
pp: case neg.refine_2
R : Type u_5
S : Type u_6
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
f : R →+* S
x : S
p : R[X]
hf : eval₂ f x p = 0
M : Submonoid R
hM : p.leadingCoeff ∈ M
Rₘ : Type u_7
Sₘ : Type u_8
inst✝⁵ : CommRing Rₘ
inst✝⁴ : CommRing Sₘ
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization M Rₘ
inst✝¹ : Algebra S Sₘ
inst✝ : IsLocalization (Submonoid.map f M) Sₘ
triv : ¬1 = 0
this : Nontrivial Rₘ
b : Rₘ
hb : (algebraMap R Rₘ) ↑⟨p.leadingCoeff, hM⟩ * b = 1
⊢ eval₂ ((algebraMap S Sₘ).comp f) ((algebraMap S Sₘ) x) p = 0

Tactic:
← hom_eval₂ _ f (algebraMap S Sₘ) x

Goal state after:
case neg.refine_2
R : Type u_5
S : Type u_6
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
f : R →+* S
x : S
p : R[X]
hf : eval₂ f x p = 0
M : Submonoid R
hM : p.leadingCoeff ∈ M
Rₘ : Type u_7
Sₘ : Type u_8
inst✝⁵ : CommRing Rₘ
inst✝⁴ : CommRing Sₘ
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization M Rₘ
inst✝¹ : Algebra S Sₘ
inst✝ : IsLocalization (Submonoid.map f M) Sₘ
triv : ¬1 = 0
this : Nontrivial Rₘ
b : Rₘ
hb : (algebraMap R Rₘ) ↑⟨p.leadingCoeff, hM⟩ * b = 1
⊢ (algebraMap S Sₘ) (eval₂ f x p) = 0
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: R : Type u_1
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
Rₘ : Type u_3
Sₘ : Type u_4
inst✝⁶ : CommRing Rₘ
inst✝⁵ : CommRing Sₘ
inst✝⁴ : Algebra R Rₘ
inst✝³ : IsLocalization M Rₘ
inst✝² : Algebra S Sₘ
inst✝¹ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝ : Algebra.IsIntegral R S
x : Sₘ
s u : S
v : R
hv : v ∈ ↑M ∧ (algebraMap R S) v = u
hx : x * (algebraMap S Sₘ) ↑(s, ⟨u, ⋯⟩).2 = (algebraMap S Sₘ) (s, ⟨u, ⋯⟩).1
v' : Rₘ
hv' : v' * (algebraMap R Rₘ) ↑⟨v, ⋯⟩ = 1
⊢ (IsLocalization.map Sₘ (algebraMap R S) ⋯).IsIntegralElem x

Tactic:
refine @IsIntegral.of_mul_unit Rₘ _ _ _ (localizationAlgebra M S) x (algebraMap S Sₘ u) v' ?_ ?_

Goal state after:
case refine_1
R : Type u_1
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
Rₘ : Type u_3
Sₘ : Type u_4
inst✝⁶ : CommRing Rₘ
inst✝⁵ : CommRing Sₘ
inst✝⁴ : Algebra R Rₘ
inst✝³ : IsLocalization M Rₘ
inst✝² : Algebra S Sₘ
inst✝¹ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝ : Algebra.IsIntegral R S
x : Sₘ
s u : S
v : R
hv : v ∈ ↑M ∧ (algebraMap R S) v = u
hx : x * (algebraMap S Sₘ) ↑(s, ⟨u, ⋯⟩).2 = (algebraMap S Sₘ) (s, ⟨u, ⋯⟩).1
v' : Rₘ
hv' : v' * (algebraMap R Rₘ) ↑⟨v, ⋯⟩ = 1
⊢ (algebraMap Rₘ Sₘ) v' * (algebraMap S Sₘ) u = 1

case refine_2
R : Type u_1
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
Rₘ : Type u_3
Sₘ : Type u_4
inst✝⁶ : CommRing Rₘ
inst✝⁵ : CommRing Sₘ
inst✝⁴ : Algebra R Rₘ
inst✝³ : IsLocalization M Rₘ
inst✝² : Algebra S Sₘ
inst✝¹ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝ : Algebra.IsIntegral R S
x : Sₘ
s u : S
v : R
hv : v ∈ ↑M ∧ (algebraMap R S) v = u
hx : x * (algebraMap S Sₘ) ↑(s, ⟨u, ⋯⟩).2 = (algebraMap S Sₘ) (s, ⟨u, ⋯⟩).1
v' : Rₘ
hv' : v' * (algebraMap R Rₘ) ↑⟨v, ⋯⟩ = 1
⊢ IsIntegral Rₘ (x * (algebraMap S Sₘ) u)
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: R : Type u_1
inst✝ : Field R
f : R[X]
⊢ f.Splits ↔ f = 0 ∨ ∀ {g : R[X]}, Irreducible g → g ∣ f → g.degree = 1

Tactic:
by
  refine ⟨fun hf ↦ or_iff_not_imp_left.mpr fun h0 g hg hgf ↦
    (hf.of_dvd h0 hgf).degree_eq_one_of_irreducible hg, ?_⟩
  rintro (rfl | hf)
  · aesop
  by_cases hf0 : f = 0
  · simp [hf0]
  obtain ⟨u, hu⟩ := factors_prod hf0
  rw [← hu]
  refine (Splits.multisetProd fun g hg ↦ ?_).mul u.isUnit.splits
  exact Splits.of_degree_eq_one (hf (irreducible_of_factor g hg) (dvd_of_mem_factors hg))

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

Goal state before:
pp: S : Type u_2
inst✝³ : CommRing S
K : Type u_4
inst✝² : CommRing K
inst✝¹ : Algebra S K
inst✝ : IsIntegralClosure S ℤ K
x : K
hx : IsAlgebraic ℤ x
a : ℤ
s : S
ha : a ≠ 0
h : a • x = (algebraMap S K) s
⊢ ∃ m s, m ≠ 0 ∧ m • x = (algebraMap S K) s

Tactic:
obtain ⟨n, rfl | rfl⟩ := a.eq_nat_or_neg

Goal state after:
case inl
S : Type u_2
inst✝³ : CommRing S
K : Type u_4
inst✝² : CommRing K
inst✝¹ : Algebra S K
inst✝ : IsIntegralClosure S ℤ K
x : K
hx : IsAlgebraic ℤ x
s : S
n : ℕ
ha : ↑n ≠ 0
h : ↑n • x = (algebraMap S K) s
⊢ ∃ m s, m ≠ 0 ∧ m • x = (algebraMap S K) s

case inr
S : Type u_2
inst✝³ : CommRing S
K : Type u_4
inst✝² : CommRing K
inst✝¹ : Algebra S K
inst✝ : IsIntegralClosure S ℤ K
x : K
hx : IsAlgebraic ℤ x
s : S
n : ℕ
ha : -↑n ≠ 0
h : -↑n • x = (algebraMap S K) s
⊢ ∃ m s, m ≠ 0 ∧ m • x = (algebraMap S K) s
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
inst✝ : NoZeroDivisors R
y z : S
hy : y ∈ nonZeroDivisors S
alg_y : IsAlgebraic R y
alg_yz : IsAlgebraic R (y * z)
t : S
ht : t ∈ R[y]
r : R
hr : r ≠ 0
eq : y * t = (algebraMap R S) r
this : IsAlgebraic R (y * t * z)
⊢ IsAlgebraic R z

Tactic:
eq,

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : NoZeroDivisors R
y z : S
hy : y ∈ nonZeroDivisors S
alg_y : IsAlgebraic R y
alg_yz : IsAlgebraic R (y * z)
t : S
ht : t ∈ R[y]
r : R
hr : r ≠ 0
eq : y * t = (algebraMap R S) r
this : IsAlgebraic R ((algebraMap R S) r * z)
⊢ IsAlgebraic R z
Module: Mathlib.RingTheory.SurjectiveOnStalks

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
⊢ (algebraMap R S).SurjectiveOnStalks

Tactic:
by
  refine surjectiveOnStalks_of_exists_div fun s ↦ ?_
  obtain ⟨x, s, rfl⟩ := IsLocalization.exists_mk'_eq M s
  exact ⟨x, s, IsLocalization.map_units S s, IsLocalization.mk'_spec' S x s⟩

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Idempotent

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : CommSemiring R
a b : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
eq : (↑a).1 = (↑b).1
⊢ 0 = (↑a).1 * (↑b).2

Tactic:
eq,

Goal state after:
case refine_1
R : Type u_1
inst✝ : CommSemiring R
a b : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
eq : (↑a).1 = (↑b).1
⊢ 0 = (↑b).1 * (↑b).2
Module: Mathlib.Algebra.Order.Ring.Idempotent

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : CommSemiring R
a b : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
eq : (↑a).1 = (↑b).1
⊢ (↑a).1 + (↑b).2 = 1

Tactic:
eq,

Goal state after:
case refine_2
R : Type u_1
inst✝ : CommSemiring R
a b : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
eq : (↑a).1 = (↑b).1
⊢ (↑b).1 + (↑b).2 = 1
Module: Mathlib.Algebra.Order.Ring.Idempotent

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : CommSemiring R
a b : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
eq : (↑a).2 = (↑b).2
⊢ 0 = (↑b).1 * (↑a).2

Tactic:
eq,

Goal state after:
case refine_1
R : Type u_1
inst✝ : CommSemiring R
a b : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
eq : (↑a).2 = (↑b).2
⊢ 0 = (↑b).1 * (↑b).2
Module: Mathlib.Algebra.Order.Ring.Idempotent

Goal state before:
pp: case refine_3
R : Type u_1
inst✝ : CommSemiring R
a b : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
eq : (↑a).2 = (↑b).2
⊢ (↑b).1 + (↑a).2 = 1

Tactic:
eq,

Goal state after:
case refine_3
R : Type u_1
inst✝ : CommSemiring R
a b : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
eq : (↑a).2 = (↑b).2
⊢ (↑b).1 + (↑b).2 = 1
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization

Goal state before:
pp: case mp
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 : ℕ
hn :
  ∃ x_1,
    (algebraMap R (Localization.AtPrime p)) x ^ n * (algebraMap R (Localization.AtPrime p)) ↑x_1.2 =
      (algebraMap R (Localization.AtPrime p)) ↑x_1.1
⊢ ∃ y ∉ I.radical, x * y ∈ I.radical

Tactic:
obtain ⟨⟨a, b⟩, hn⟩ := hn

Goal state after:
case mp
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 : ↥p.primeCompl
hn :
  (algebraMap R (Localization.AtPrime p)) x ^ n * (algebraMap R (Localization.AtPrime p)) ↑(a, b).2 =
    (algebraMap R (Localization.AtPrime p)) ↑(a, b).1
⊢ ∃ y ∉ I.radical, x * y ∈ I.radical
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]

Goal state after:
ι : 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 f ∘ comap (Pi.evalRingHom R i)) = Set.range (comap f)
Module: Mathlib.RingTheory.KrullDimension.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : NoZeroDivisors R
inst✝¹ : Ring.KrullDimLE 1 R
inst✝ : Algebra R S
P : Ideal S
p : R
hP : P ≠ ⊤
hp : Prime p
⊢ P.LiesOver (span {p}) ↔ (algebraMap R S) p ∈ P

Tactic:
have hP : P.under R ≠ ⊤ := Ideal.comap_ne_top _ hP
  simp [Ideal.liesOver_iff, Ideal.IsMaximal.eq_iff_le hp.isMaximal_span_singleton hP]

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

Goal state before:
pp: case mp
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 * ↑(a, b).2) = ↑t * ↑(a, b).1
⊢ ∃ y ∉ I.radical, x * y ∈ I.radical

Tactic:
refine ⟨t * b, fun h ↦ (t * b).2 (hp₁.radical_le_iff.mpr hp₂ h), n + 1, ?_⟩

Goal state after:
case mp
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 * ↑(a, b).2) = ↑t * ↑(a, b).1
⊢ (x * (↑t * ↑b)) ^ (n + 1) ∈ I
Module: Mathlib.RingTheory.Localization.AsSubring

Goal state before:
pp: A : Type u_1
K : Type u_2
inst✝³ : CommRing A
S : Submonoid A
hS : S ≤ A⁰
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
⊢ {x | ∃ a s, ∃ (_ : s ∈ S), x = (algebraMap A K) a * ((algebraMap A K) s)⁻¹} =
    ↑(mapToFractionRing K S (Localization S) hS).range

Tactic:
ext
    symm
    apply mem_range_mapToFractionRing_iff_ofField

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

Goal state before:
pp: case refine_2.refine_2
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Surjective ⇑f
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
hp : ker f ≤ p.asIdeal
⊢ comap f { asIdeal := Ideal.map f p.asIdeal, isPrime := ⋯ } = p

Tactic:
· ext x
      rw [comap_asIdeal, Ideal.mem_comap, Ideal.mem_map_iff_of_surjective f hf]
      refine ⟨?_, fun hx => ⟨x, hx, rfl⟩⟩
      rintro ⟨x', hx', heq⟩
      rw [← sub_sub_cancel x' x]
      refine p.asIdeal.sub_mem hx' (hp ?_)
      rwa [mem_ker, map_sub, sub_eq_zero]

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

Goal state before:
pp: R : Type u
inst✝² : CommRing R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : PrimeSpectrum R
⊢ Nontrivial (p.asIdeal.ResidueField ⊗[R] S) ↔ p ∈ Set.range (comap (algebraMap R S))

Tactic:
let k := p.asIdeal.ResidueField

Goal state after:
R : Type u
inst✝² : CommRing R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : PrimeSpectrum R
k : Type u := p.asIdeal.ResidueField
⊢ Nontrivial (p.asIdeal.ResidueField ⊗[R] S) ↔ p ∈ Set.range (comap (algebraMap R S))
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
⊢ comap f J ≤ K

Tactic:
← sup_eq_left.mpr this,

Goal state after:
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
⊢ comap f J ≤ K ⊔ RingHom.ker f
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
h h' : LE α
c : OrderBot α
bot : α
eq_bot : bot = ⊥
le_eq : ∀ (x y : α), x ≤ y ↔ x ≤ y
x✝ : α
⊢ ⊥ ≤ x✝

Tactic:
by simp [eq_bot, le_eq]

Goal state after:
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
h h' : LE α
c : BoundedOrder α
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
le_eq : ∀ (x y : α), x ≤ y ↔ x ≤ y
x✝ : α
⊢ ⊥ ≤ x✝

Tactic:
by simp [eq_bot, le_eq]

Goal state after:
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : DistribLattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
⊢ ∀ (x y z : α), (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z

Tactic:
intros; simp +instances [eq_le, eq_sup, eq_inf, le_sup_inf]

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

Goal state before:
pp: case mpr
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
y : R
v : Ideal R
hv : v.IsMaximal
⊢ (algebraMap R K) y ∈ Localization.subalgebra.ofField K { asIdeal := v, isMaximal := hv }.asIdeal.primeCompl ⋯

Tactic:
exact ⟨y, 1, v.ne_top_iff_one.mp hv.ne_top, by rw [map_one, inv_one, mul_one]⟩

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

Goal state before:
pp: ι : Type u_1
X : Type u_3
inst✝ : TopologicalSpace X
S : Set (Opens X)
hS : IsBasis S
U : ι → Opens X
hU : IsOpenCover U
x : X
x✝ : x ∈ ⊤
⊢ x ∈ ⨆ V, (↑V).1

Tactic:
obtain ⟨i, hxi⟩ := hU.exists_mem x

Goal state after:
ι : Type u_1
X : Type u_3
inst✝ : TopologicalSpace X
S : Set (Opens X)
hS : IsBasis S
U : ι → Opens X
hU : IsOpenCover U
x : X
x✝ : x ∈ ⊤
i : ι
hxi : x ∈ U i
⊢ x ∈ ⨆ V, (↑V).1
Module: Mathlib.Order.BooleanSubalgebra

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : BooleanAlgebra α
inst✝¹ : BooleanAlgebra β
inst✝ : BooleanAlgebra γ
L✝ M : BooleanSubalgebra α
f✝ : BoundedLatticeHom α β
s t : Set α
a b : α
f : BoundedLatticeHom α β
L : BooleanSubalgebra α
⊢ ∀ {a : β}, a ∈ ⇑f '' ↑L → aᶜ ∈ ⇑f '' ↑L

Tactic:
rintro _ ⟨a, ha, rfl⟩; exact ⟨aᶜ, by simpa [map_compl']⟩

Goal state after:
Module: Mathlib.Topology.QuasiSeparated

Goal state before:
pp: case convert_2
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : IsEmbedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen[inst✝] U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen[inst✝] V
hV'' : IsCompact V
⊢ IsCompact (f ⁻¹' U)

Tactic:
rw [h.isCompact_iff]

Goal state after:
case convert_2
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : IsEmbedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen[inst✝] U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen[inst✝] V
hV'' : IsCompact V
⊢ IsCompact (f '' f ⁻¹' U)
Module: Mathlib.Topology.QuasiSeparated

Goal state before:
pp: case convert_4
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : IsEmbedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen[inst✝] U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen[inst✝] V
hV'' : IsCompact V
⊢ IsCompact (f ⁻¹' V)

Tactic:
rw [h.isCompact_iff]

Goal state after:
case convert_4
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : IsEmbedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen[inst✝] U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen[inst✝] V
hV'' : IsCompact V
⊢ IsCompact (f '' f ⁻¹' V)