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

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
p : Type u_4
R : Type u_5
S : Type u_6
A : Type u_7
B : Type u_8
M : Type u_9
N : Type u_10
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : DecidableEq n
inst✝ : Fintype n
a₁✝ a₂✝ : A
b₁✝ b₂✝ : Matrix n n R
i✝ j✝ : n
⊢ a₁✝ * a₂✝ * (b₁✝.map ⇑(algebraMap R A) * b₂✝.map ⇑(algebraMap R A)) i✝ j✝ =
    (a₁✝ • b₁✝.map ⇑(algebraMap R A) * a₂✝ • b₂✝.map ⇑(algebraMap R A)) i✝ j✝

Tactic:
Matrix.mul_apply,

Goal state after:
l : Type u_1
m : Type u_2
n : Type u_3
p : Type u_4
R : Type u_5
S : Type u_6
A : Type u_7
B : Type u_8
M : Type u_9
N : Type u_10
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : DecidableEq n
inst✝ : Fintype n
a₁✝ a₂✝ : A
b₁✝ b₂✝ : Matrix n n R
i✝ j✝ : n
⊢ a₁✝ * a₂✝ * ∑ j, b₁✝.map (⇑(algebraMap R A)) i✝ j * b₂✝.map (⇑(algebraMap R A)) j j✝ =
    ∑ j, (a₁✝ • b₁✝.map ⇑(algebraMap R A)) i✝ j * (a₂✝ • b₂✝.map ⇑(algebraMap R A)) j j✝
Module: Mathlib.RingTheory.Nilpotent.Basic

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
ι : Type u_3
f : ι → R
hf : ∀ (b : ι), IsNilpotent (f b)
h_comm : ∀ (i j : ι), Commute (f i) (f j)
h : HasFiniteSupport f
⊢ IsNilpotent (finsum f)

Tactic:
finsum_def,

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
ι : Type u_3
f : ι → R
hf : ∀ (b : ι), IsNilpotent (f b)
h_comm : ∀ (i j : ι), Commute (f i) (f j)
h : HasFiniteSupport f
⊢ IsNilpotent (if h : HasFiniteSupport f then ∑ i ∈ Finite.toFinset h, f i else 0)
Module: Mathlib.Algebra.Module.SpanRank

Goal state before:
pp: R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p q : Submodule R M
⊢ (p ⊔ q).spanRank ≤ p.spanRank + q.spanRank

Tactic:
apply (FG.spanRank_le_iff_exists_span_set_card_le (p ⊔ q)).mpr
  obtain ⟨sp, ⟨hp₁, rfl⟩⟩ := exists_span_set_card_eq_spanRank p
  obtain ⟨sq, ⟨hq₁, rfl⟩⟩ := exists_span_set_card_eq_spanRank q
  exact ⟨sp ∪ sq, ⟨hp₁ ▸ hq₁ ▸ (Cardinal.mk_union_le sp sq), span_union sp sq⟩⟩

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
h✝ : Nonempty n
this : IsNilpotent (M.charpolyRev.coeff 1)
⊢ IsNilpotent M.trace

Tactic:
by simpa using this

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
r✝ : R
f✝ : R[X]
r c : R
f : R[X]
⊢ (c • f).comp (X + C r) = (RingHom.id R) c • f.comp (X + C r)

Tactic:
simp only [smul_eq_C_mul, C_mul_comp, RingHom.id_apply]

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

Goal state before:
pp: case inr
R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
n a b : ℕ
e : a + b = n
ha : a ≤ p.natDegree
⊢ 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))

Tactic:
cases lt_or_ge (natDegree q) b with
      | inl h => simp only [coeff_eq_zero_of_natDegree_lt h, zero_mul, mul_zero]
      | inr hb =>
        simp only [← e, mul_assoc, mul_comm (r ^ (_ - a)), ← pow_add]
        rw [add_comm (_ - _), tsub_add_tsub_comm ha hb]

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

Goal state before:
pp: case inr
R : Type u_1
inst✝ : CommSemiring R
f g : R[X]
hf : f.Splits
hg✝ : g.natDegree ≤ 1
h : Invertible g.leadingCoeff
hg : g.natDegree = 1
m : Multiset R
hm : f = C f.leadingCoeff * (Multiset.map (fun x ↦ X + C x) m).prod
⊢ (C f.leadingCoeff * (Multiset.map (fun p ↦ p.comp g) (Multiset.map (fun x ↦ X + C x) m)).prod).Splits

Tactic:
refine (Splits.C _).mul (multisetProd ?_)

Goal state after:
case inr
R : Type u_1
inst✝ : CommSemiring R
f g : R[X]
hf : f.Splits
hg✝ : g.natDegree ≤ 1
h : Invertible g.leadingCoeff
hg : g.natDegree = 1
m : Multiset R
hm : f = C f.leadingCoeff * (Multiset.map (fun x ↦ X + C x) m).prod
⊢ ∀ f ∈ Multiset.map (fun p ↦ p.comp g) (Multiset.map (fun x ↦ X + C x) m), f.Splits
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
x : R
| eval x f

Tactic:
rw [hf.eq_prod_roots]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
hf : f.Splits
x : R
| eval x (C f.leadingCoeff * (Multiset.map (fun x ↦ X - C x) f.roots).prod)
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
f : R[X]
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
hf : f.Splits
x : R
| eval x (derivative f)

Tactic:
rw [hf.eq_prod_roots]

Goal state after:
R : Type u_1
inst✝² : CommRing R
f : R[X]
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
hf : f.Splits
x : R
| eval x (derivative (C f.leadingCoeff * (Multiset.map (fun x ↦ X - C x) f.roots).prod))
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
f : R[X]
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain A
inst✝² : IsDomain B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
hf : (map (algebraMap R A) f).Splits
φ : A →ₐ[R] B
hφ : map (algebraMap R B) f ≠ 0
⊢ ⇑φ '' f.rootSet A = f.rootSet B

Tactic:
by
  classical
  replace hφ : (f.map (algebraMap R A)).map (φ : A →+* B) ≠ 0 := by
    rwa [map_map, φ.comp_algebraMap]
  replace hf := hf.roots_map_of_ne_zero hφ
  rw [map_map, φ.comp_algebraMap] at hf
  simp [rootSet, aroots, hf, Multiset.toFinset_map]

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
| f.coeff 0

Tactic:
rw [hf.eq_prod_roots]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
hf : f.Splits
| (C f.leadingCoeff * (Multiset.map (fun x ↦ X - C x) f.roots).prod).coeff 0
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
| f.nextCoeff

Tactic:
rw [hf.eq_prod_roots]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
hf : f.Splits
| (C f.leadingCoeff * (Multiset.map (fun x ↦ X - C x) f.roots).prod).nextCoeff
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: case succ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
ih : ∀ {f g : R[X]}, f ≠ 0 → g ≠ 0 → ∀ (p : R[X]), f * g = p → p.Splits → p.natDegree = n → f.Splits ∧ g.Splits
f g : R[X]
hf₀ : f ≠ 0
hg₀ : g ≠ 0
p : R[X]
hp : f * g = p
h : p.Splits
hn : p.natDegree = n + 1
⊢ f.Splits ∧ g.Splits

Tactic:
| succ n ih =>

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
s : Multiset R
g : R[X]
hg : g.Monic
hg' : g.Splits
this : g = (Multiset.map (fun x ↦ X - C x) g.roots).prod
⊢ (Multiset.map (fun ij ↦ ij.1 - ij.2) (s ×ˢ g.roots)).prod =
    (Multiset.map (fun x ↦ eval x (Multiset.map (fun x ↦ X - C x) g.roots).prod) s).prod

Tactic:
simp_rw [eval_multiset_prod, Multiset.prod_map_product_eq_prod_prod, Multiset.map_map]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
s : Multiset R
g : R[X]
hg : g.Monic
hg' : g.Splits
this : g = (Multiset.map (fun x ↦ X - C x) g.roots).prod
⊢ (Multiset.map (fun x ↦ (Multiset.map (fun x_1 ↦ x - x_1) g.roots).prod) s).prod =
    (Multiset.map (fun x ↦ (Multiset.map (eval x ∘ fun x ↦ X - C x) g.roots).prod) s).prod
Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing A
inst✝⁹ : CommRing B
inst✝⁸ : Algebra R B
inst✝⁷ : Algebra A B
inst✝⁶ : IsIntegralClosure A R B
S : Type u_4
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : Algebra S B
inst✝² : IsScalarTower R S B
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R A B
isIntegral : Algebra.IsIntegral R S
⊢ mk' A ((algebraMap S B) 1) ⋯ = 1

Tactic:
by simp only [map_one, mk'_one]

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

Goal state before:
pp: case refine_2
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
I : Ideal S
r : S
r_non_zero_divisor : ∀ {x : S}, x * r = 0 → x = 0
hr : r ∈ I
p✝ p : R[X]
a : R
⊢ p.coeff 0 = 0 →
    a ≠ 0 →
      (p ≠ 0 → eval₂ f r p = 0 → ∃ i, p.coeff i ≠ 0 ∧ p.coeff i ∈ comap f I) →
        p + C a ≠ 0 → eval₂ f r (p + C a) = 0 → ∃ i, (p + C a).coeff i ≠ 0 ∧ (p + C a).coeff i ∈ comap f I

Tactic:
coeff_eq_zero

Goal state after:
case refine_2
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
I : Ideal S
r : S
r_non_zero_divisor : ∀ {x : S}, x * r = 0 → x = 0
hr : r ∈ I
p✝ p : R[X]
a : R
coeff_eq_zero : p.coeff 0 = 0
⊢ a ≠ 0 →
    (p ≠ 0 → eval₂ f r p = 0 → ∃ i, p.coeff i ≠ 0 ∧ p.coeff i ∈ comap f I) →
      p + C a ≠ 0 → eval₂ f r (p + C a) = 0 → ∃ i, (p + C a).coeff i ≠ 0 ∧ (p + C a).coeff i ∈ comap f I
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
x✝ :
  Flat R M ∧ ∀ (N : Type (max u v)) [inst : AddCommGroup N] [inst_1 : Module R N], Nontrivial N → Nontrivial (N ⊗[R] M)
flat : Flat R M
m : Ideal R
faithful : Nontrivial (ULift.{v, u} (R ⧸ m) ⊗[R] M)
hm : m.IsMaximal
rid : m • ⊤ = ⊤
this✝ : Nontrivial ((R ⧸ m) ⊗[R] M)
this : Nontrivial (M ⧸ m • ⊤)
⊢ Subsingleton (M ⧸ m • ⊤)

Tactic:
Submodule.Quotient.subsingleton_iff

Goal state after:
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝ :
  Flat R M ∧ ∀ (N : Type (max u v)) [inst : AddCommGroup N] [inst_1 : Module R N], Nontrivial N → Nontrivial (N ⊗[R] M)
flat : Flat R M
m : Ideal R
faithful : Nontrivial (ULift.{v, u} (R ⧸ m) ⊗[R] M)
hm : m.IsMaximal
rid : m • ⊤ = ⊤
this✝ : Nontrivial ((R ⧸ m) ⊗[R] M)
this : Nontrivial (M ⧸ m • ⊤)
⊢ m • ⊤ = ⊤
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
inst✝ : Algebra.IsIntegral R S
I : Ideal S
hI : I.IsMaximal
this : (comap (algebraMap R S) I).IsPrime
⊢ IsField (S ⧸ I)

Tactic:
by rwa [← Quotient.maximal_ideal_iff_isField_quotient]

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

Goal state before:
pp: case refine_1.refine_1
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
ht : IsIntegral (↥R[s]) t
a✝ : Nontrivial S
φ : R[X] →ₐ[R] S := aeval s
q : R[X][X]
hqm : q.Monic
hqt : eval₂ φ.toRingHom t q = 0
N : ℕ := q.support.sup fun x ↦ (q.coeff x).natDegree
hN : ∀ (i : ℕ), (q.coeff i).natDegree ≤ N
q' : R[X] := q.sum fun i r ↦ X ^ i * reflect N r
this : ∀ (i : ℕ), (aeval t) (reflect N (q.coeff i)) = t ^ N * (aeval s) (q.coeff i)
i : ℕ
hi : i ∈ q.support
⊢ ((fun i r ↦ X ^ i * reflect N r) i (q.coeff i)).natDegree ≤ q.natDegree + N

Tactic:
natDegree_mul_le,

Goal state after:
case refine_1.refine_1
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
ht : IsIntegral (↥R[s]) t
a✝ : Nontrivial S
φ : R[X] →ₐ[R] S := aeval s
q : R[X][X]
hqm : q.Monic
hqt : eval₂ φ.toRingHom t q = 0
N : ℕ := q.support.sup fun x ↦ (q.coeff x).natDegree
hN : ∀ (i : ℕ), (q.coeff i).natDegree ≤ N
q' : R[X] := q.sum fun i r ↦ X ^ i * reflect N r
this : ∀ (i : ℕ), (aeval t) (reflect N (q.coeff i)) = t ^ N * (aeval s) (q.coeff i)
i : ℕ
hi : i ∈ q.support
⊢ (X ^ i).natDegree + (reflect N (q.coeff i)).natDegree ≤ q.natDegree + N
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: R : Type u_1
A : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
z : A
y : R
hy : y ∈ nonZeroDivisors R
h : IsAlgebraic R (y • z)
p : R[X]
hp : p ≠ 0
eval0 : (aeval (y • z)) p = 0
⊢ (aeval z) (p.comp (C y * X)) = 0

Tactic:
by simpa [aeval_comp, Algebra.smul_def] using eval0

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

Goal state before:
pp: case h
R : Type u
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
M : Ideal R
hgt : ∀ J > M, ∃ Z, (Multiset.map asIdeal Z).prod ≤ J
h_prM : ¬M.IsPrime
htop : ¬M = ⊤
lt_add : ∀ z ∉ M, M < M + R ∙ z
x : R
hx : x ∉ M
y : R
hy : y ∉ M
hxy : x * y ∈ M
Wx : Multiset (PrimeSpectrum R)
h_Wx : (Multiset.map asIdeal Wx).prod ≤ M + R ∙ x
Wy : Multiset (PrimeSpectrum R)
h_Wy : (Multiset.map asIdeal Wy).prod ≤ M + R ∙ y
⊢ (Multiset.map asIdeal Wx).prod * (Multiset.map asIdeal Wy).prod ≤ M

Tactic:
apply le_trans (mul_le_mul' h_Wx h_Wy)

Goal state after:
case h
R : Type u
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
M : Ideal R
hgt : ∀ J > M, ∃ Z, (Multiset.map asIdeal Z).prod ≤ J
h_prM : ¬M.IsPrime
htop : ¬M = ⊤
lt_add : ∀ z ∉ M, M < M + R ∙ z
x : R
hx : x ∉ M
y : R
hy : y ∉ M
hxy : x * y ∈ M
Wx : Multiset (PrimeSpectrum R)
h_Wx : (Multiset.map asIdeal Wx).prod ≤ M + R ∙ x
Wy : Multiset (PrimeSpectrum R)
h_Wy : (Multiset.map asIdeal Wy).prod ≤ M + R ∙ y
⊢ (M + R ∙ x) * (M + R ∙ y) ≤ M
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
K : Type u_4
L : Type u_5
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra R K
inst✝⁶ : Algebra R L
inst✝⁵ : Algebra S L
inst✝⁴ : Algebra.IsAlgebraic R S
inst✝³ : IsFractionRing S L
inst✝² : Algebra K L
inst✝¹ : IsScalarTower R S L
inst✝ : IsScalarTower R K L
a : S
b : Set S
inj : Function.Injective ⇑(algebraMap R L)
h : ↑(Ideal.span {a}) ⊆ ↑(Submodule.span R b)
x : L
hx : x ∈ ↑(Ideal.span {(algebraMap S L) a})
⊢ x ∈ ↑(Submodule.span K (⇑(algebraMap S L) '' b))

Tactic:
obtain ⟨x', rfl⟩ := Ideal.mem_span_singleton.mp hx

Goal state after:
R : Type u_1
inst✝¹⁴ : CommRing R
S : Type u_2
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
K : Type u_4
L : Type u_5
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra R K
inst✝⁶ : Algebra R L
inst✝⁵ : Algebra S L
inst✝⁴ : Algebra.IsAlgebraic R S
inst✝³ : IsFractionRing S L
inst✝² : Algebra K L
inst✝¹ : IsScalarTower R S L
inst✝ : IsScalarTower R K L
a : S
b : Set S
inj : Function.Injective ⇑(algebraMap R L)
h : ↑(Ideal.span {a}) ⊆ ↑(Submodule.span R b)
x' : L
hx : (algebraMap S L) a * x' ∈ ↑(Ideal.span {(algebraMap S L) a})
⊢ (algebraMap S L) a * x' ∈ ↑(Submodule.span K (⇑(algebraMap S L) '' b))
Module: Mathlib.Algebra.Order.Ring.Idempotent

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

Tactic:
hab,

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝ : CommSemigroup S
a b c : { a // IsIdempotentElem a }
hab : ↑a * ↑b = ↑a
hac : ↑a * ↑c = ↑a
⊢ ↑a * ↑b * ↑c = ↑a

Tactic:
hab,

Goal state after:
R : Type u_1
S : Type u_2
inst✝ : CommSemigroup S
a b c : { a // IsIdempotentElem a }
hab : ↑a * ↑b = ↑a
hac : ↑a * ↑c = ↑a
⊢ ↑a * ↑c = ↑a
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
⊢ ⋃ p ∈ I.minimalPrimes, ↑p = {x | ∃ y ∉ I.radical, x * y ∈ I.radical}

Tactic:
by
  ext x
  simp only [Set.mem_iUnion, SetLike.mem_coe, exists_prop, Set.mem_ofPred_eq]
  constructor
  · rintro ⟨p, ⟨⟨hp₁, hp₂⟩, hp₃⟩, hxp⟩
    have : p.map (algebraMap R (Localization.AtPrime p)) ≤ (I.map (algebraMap _ _)).radical := by
      rw [Ideal.radical_eq_sInf, le_sInf_iff]
      rintro q ⟨hq', hq⟩
      obtain ⟨h₁, h₂⟩ := ((IsLocalization.AtPrime.orderIsoOfPrime _ p) ⟨q, hq⟩).2
      rw [Ideal.map_le_iff_le_comap] at hq' ⊢
      exact hp₃ ⟨h₁, hq'⟩ h₂
    obtain ⟨n, hn⟩ := this (Ideal.mem_map_of_mem _ hxp)
    rw [IsLocalization.mem_map_algebraMap_iff (M := p.primeCompl)] at hn
    obtain ⟨⟨a, b⟩, hn⟩ := hn
    rw [← map_pow, ← map_mul, IsLocalization.eq_iff_exists p.primeCompl] at hn
    obtain ⟨t, ht⟩ := hn
    refine ⟨t * b, fun h ↦ (t * b).2 (hp₁.radical_le_iff.mpr hp₂ h), n + 1, ?_⟩
    simp only at ht
    have : (x * (t.1 * b.1)) ^ (n + 1) = (t.1 ^ n * b.1 ^ n * x * t.1) * a := by
      rw [mul_assoc, ← ht]; ring
    rw [this]
    exact I.mul_mem_left _ a.2
  · rintro ⟨y, hy, hx⟩
    obtain ⟨p, hp, hyp⟩ : ∃ p ∈ I.minimalPrimes, y ∉ p := by
      simpa [← Ideal.sInf_minimalPrimes] using hy
    refine ⟨p, hp, (hp.isPrime.mem_or_mem ?_).resolve_right hyp⟩
    exact hp.isPrime.radical_le_iff.mpr hp.le hx

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

Goal state before:
pp: X : Type u_3
inst✝ : TopologicalSpace X
S : Set (Opens X)
hS : IsBasis S
⊢ IsOpenCover fun U ↦ ↑U

Tactic:
by
  ext1
  simp [← hS.2]

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 ∈ ⊤
i : ι
hxi : x ∈ U i
⊢ x ∈ ⨆ V, (↑V).1

Tactic:
obtain ⟨_, ⟨V, hV, rfl⟩, hxV, hVU⟩ := hS.exists_subset_of_mem_open hxi (U i).2

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
V : Opens X
hV : V ∈ S
hxV : x ∈ ↑V
hVU : ↑V ⊆ ↑(U i)
⊢ x ∈ ⨆ V, (↑V).1
Module: Mathlib.Topology.LocalAtTarget

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
⊢ closure[inst✝] (range f) = univ ↔
    ∀ (i : ι), closure[instTopologicalSpaceSubtype] (range ((U i).carrier.restrictPreimage f)) = univ

Tactic:
Set.range_restrictPreimage,

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
⊢ closure[inst✝] (range f) = univ ↔ ∀ (i : ι), closure[instTopologicalSpaceSubtype] (Subtype.val ⁻¹' range f) = univ
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
ι : Type u_4
s : Finset ι
t : ι → Set X
ht : ∀ i ∈ s, IsRetrocompact (t i)
⊢ IsRetrocompact (s.sup t)

Tactic:
induction s using Finset.cons_induction with
  | empty => simp
  | cons i s ih hi =>
    rw [Finset.sup_cons]
    exact (ht _ <| by simp).union <| hi <| Finset.forall_of_forall_cons ht

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

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
⊢ range toCompacts = {⊥}ᶜ

Tactic:
ext K

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
K : Compacts α
⊢ K ∈ range toCompacts ↔ K ∈ {⊥}ᶜ
Module: Mathlib.Topology.Sober

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
S : Set (Set α)
hS : ∀ (s : ↑S), IsOpen ↑s
inst✝ : ∀ (s : ↑S), QuasiSober ↑↑s
hS' : ⋃₀ S = ⊤
⊢ TopologicalSpace.IsOpenCover fun s ↦ { carrier := ↑s, is_open' := ⋯ }

Tactic:
simpa [TopologicalSpace.IsOpenCover, ← SetLike.coe_set_eq, sUnion_eq_iUnion] using hS'

Goal state after:
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: case inr.inr
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
⊢ (if b.factorization p ≤ a.factorization p then p ^ (a.lcm b).factorization p else 1) ∣ p ^ a.factorization p

Tactic:
split_ifs with le

Goal state after:
case pos
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
le : b.factorization p ≤ a.factorization p
⊢ p ^ (a.lcm b).factorization p ∣ p ^ a.factorization p

case neg
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
le : ¬b.factorization p ≤ a.factorization p
⊢ 1 ∣ p ^ a.factorization p
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s t : Set (PrimeSpectrum R)
ht : IsClosed t
h : vanishingIdeal t ≤ vanishingIdeal s
⊢ s ⊆ t

Tactic:
rw [← ht.closure_subset_iff, ← ht.closure_eq]

Goal state after:
R : Type u
inst✝ : CommSemiring R
s t : Set (PrimeSpectrum R)
ht : IsClosed t
h : vanishingIdeal t ≤ vanishingIdeal s
⊢ closure s ⊆ closure t
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsRadical
⊢ IsIrreducible (zeroLocus ↑I) ↔ I ≠ ⊤ ∧ ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I

Tactic:
IsIrreducible

Goal state after:
R : Type u
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsRadical
⊢ (zeroLocus ↑I).Nonempty ∧ IsPreirreducible (zeroLocus ↑I) ↔ I ≠ ⊤ ∧ ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: case inr.inr
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
⊢ (if b.factorization p ≤ a.factorization p then 1 else p ^ (a.lcm b).factorization p) ∣ p ^ b.factorization p

Tactic:
split_ifs with le

Goal state after:
case pos
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
le : b.factorization p ≤ a.factorization p
⊢ 1 ∣ p ^ b.factorization p

case neg
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
le : ¬b.factorization p ≤ a.factorization p
⊢ p ^ (a.lcm b).factorization p ∣ p ^ b.factorization p
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
⊢ IsIrreducible s ↔ (vanishingIdeal s).IsPrime

Tactic:
by
  rw [← isIrreducible_iff_closure, ← zeroLocus_vanishingIdeal_eq_closure,
    isIrreducible_zeroLocus_iff_of_radical _ (isRadical_vanishingIdeal s)]

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case le
G : Type u
inst✝ : Monoid G
h : Subsingleton G
⊢ exponent G ≤ 1

Tactic:
apply exponent_min' _ Nat.one_pos
    simp [eq_iff_true_of_subsingleton]

Goal state after:
Module: Mathlib.GroupTheory.Subgroup.Simple

Goal state before:
pp: case refine_2
G : Type u_1
inst✝³ : Group G
H✝ : Type u_3
inst✝² : Group H✝
inst✝¹ : IsSimpleGroup G
inst✝ : Nontrivial H✝
f : G →* H✝
hf : Function.Surjective ⇑f
H : Subgroup H✝
iH : H.Normal
h : comap f H = ⊤
⊢ H = ⊤

Tactic:
rw [← comap_top f] at h

Goal state after:
case refine_2
G : Type u_1
inst✝³ : Group G
H✝ : Type u_3
inst✝² : Group H✝
inst✝¹ : IsSimpleGroup G
inst✝ : Nontrivial H✝
f : G →* H✝
hf : Function.Surjective ⇑f
H : Subgroup H✝
iH : H.Normal
h : comap f H = comap f ⊤
⊢ H = ⊤
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case refine_2
G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
he : (Set.range orderOf).Finite
⊢ exponent G ≠ 0

Tactic:
· lift Set.range (orderOf (G := G)) to Finset ℕ using he with t ht
    have htpos : 0 < t.prod id := by
      refine Finset.prod_pos fun a ha => ?_
      rw [← Finset.mem_coe, ht] at ha
      obtain ⟨k, rfl⟩ := ha
      exact h k
    suffices exponent G ∣ t.prod id by
      intro h
      rw [h, zero_dvd_iff] at this
      exact htpos.ne' this
    rw [exponent_dvd]
    intro g
    apply Finset.dvd_prod_of_mem id (?_ : orderOf g ∈ _)
    rw [← Finset.mem_coe, ht]
    exact Set.mem_range_self g

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
⊢ exponent G = 0 ↔ (Set.range orderOf).Infinite

Tactic:
by
  have := exponent_ne_zero_iff_range_orderOf_finite h
  rwa [Ne, not_iff_comm, Iff.comm] at this

Goal state after:
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Fact (Nat.Prime p)
hG : IsPGroup p G
g : G
hg : g ≠ 1
k : ℕ
hk : orderOf g = p ^ k
⊢ p ∣ p ^ k

Tactic:
refine dvd_pow_self _ fun hk0 ↦ hg ?_

Goal state after:
p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Fact (Nat.Prime p)
hG : IsPGroup p G
g : G
hg : g ≠ 1
k : ℕ
hk : orderOf g = p ^ k
hk0 : k = 0
⊢ g = 1
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
k : G → ℕ
hk : ∀ (g : G), orderOf g ∣ p ^ k g
this : Fintype G
g : G
left✝ : g ∈ Finset.univ
hg : ∀ x' ∈ Finset.univ, k x' ≤ k g
g' : G
⊢ orderOf g' ∣ p ^ k g

Tactic:
grw [← Nat.pow_dvd_pow p <| hg g' <| Finset.mem_univ g']

Goal state after:
p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
k : G → ℕ
hk : ∀ (g : G), orderOf g ∣ p ^ k g
this : Fintype G
g : G
left✝ : g ∈ Finset.univ
hg : ∀ x' ∈ Finset.univ, k x' ≤ k g
g' : G
⊢ orderOf g' ∣ p ^ k g'