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

Goal state before:
pp: case pos
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
hdeg : ¬P.natDegree = 0
P₁ : R[X] := P.eraseLead
hP₁ : P₁ = P.eraseLead
hdeg₂ : P.eraseLead.natDegree < P.natDegree
i : ℕ
hi : i ≠ 0
H : i ≤ P₁.natDegree
⊢ IsNilpotent (P₁.coeff i)

pp: case neg
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
hdeg : ¬P.natDegree = 0
P₁ : R[X] := P.eraseLead
hP₁ : P₁ = P.eraseLead
hdeg₂ : P.eraseLead.natDegree < P.natDegree
i : ℕ
hi : i ≠ 0
H : P₁.natDegree < i
⊢ IsNilpotent (P₁.coeff i)

Tactic:
· simp_rw [P₁, eraseLead_coeff_of_ne _ (ne_of_lt (lt_of_le_of_lt H hdeg₂)), hnil i hi]

Goal state after:
case neg
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
hdeg : ¬P.natDegree = 0
P₁ : R[X] := P.eraseLead
hP₁ : P₁ = P.eraseLead
hdeg₂ : P.eraseLead.natDegree < P.natDegree
i : ℕ
hi : i ≠ 0
H : P₁.natDegree < i
⊢ IsNilpotent (P₁.coeff i)
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 : Submodule R M
hp : ¬p.FG
⊢ p.spanFinrank = 0

Tactic:
refine toNat_eq_zero.2 ?_

Goal state after:
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
hp : ¬p.FG
⊢ p.spanRank = 0 ∨ ℵ₀ ≤ p.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
k : ℕ
h : Fintype.card n - 1 ≤ k
⊢ (M.charpoly - ∏ i, (X - C (M i i))).coeff k = 0

Tactic:
apply Polynomial.coeff_eq_zero_of_degree_lt

Goal state after:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
h : Fintype.card n - 1 ≤ k
⊢ (M.charpoly - ∏ i, (X - C (M i i))).degree < ↑k
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
hq : map f q = p
⊢ (∑ i, C (g ↑i) * X ^ ↑i).degree < ↑p.natDegree

Tactic:
degree_sum_fin_lt

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
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
hq : map f q = p
h : q.Monic
⊢ ∃ q, map f q = p ∧ q.degree = p.degree ∧ q.Monic

Tactic:
exact ⟨q, hq, hq ▸ (h.degree_map f).symm, h⟩

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : IsAddTorsionFree R
p : R[X]
n : ℕ
⊢ ((hasseDeriv n) p).natDegree = p.natDegree - n

Tactic:
refine map_natDegree_eq_sub (fun h => hasseDeriv_eq_zero_of_lt_natDegree _ _) ?_
  simp only [Ne, hasseDeriv_monomial, natDegree_monomial, ite_eq_right_iff]
  simp +contextual [← nsmul_eq_mul, Nat.choose_eq_zero_iff, le_of_lt]

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
T : Subring R
i : ℕ
⊢ ↑((toSubring 1 T ⋯).coeff i) = ↑(coeff 1 i)

Tactic:
rw [coeff_toSubring', coeff_one, coeff_one, apply_ite Subtype.val, ZeroMemClass.coe_zero,
      OneMemClass.coe_one]

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

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : CommSemiring R
S : Submonoid R[X] := MonoidHom.mrange C
hS : ↑S = {x | ∃ a, C a = x}
a : R
mg : Multiset R[X]
hg : mg.prod ∈ Submonoid.closure {x | ∃ a, X + C a = x}
j : R[X] → R
hj : ∀ y ∈ mg, X + C (j y) = y
hmg : mg = Multiset.map (fun x ↦ X + C x) (Multiset.map j mg)
⊢ ∃ m, C a * (Multiset.map (fun x ↦ X + C x) (Multiset.map j mg)).prod = C a * (Multiset.map (fun x ↦ X + C x) m).prod

Tactic:
use mg.map j

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
f : R[X]
A : Type u_2
B : Type u_3
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
hf : (map (algebraMap R A) f).Splits
e : A →ₐ[R] B
⊢ (map (algebraMap R B) f).Splits

Tactic:
by
  rw [← e.comp_algebraMap, ← map_map]
  apply hf.map

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
a : R
⊢ (X - C a).Splits

Tactic:
simpa using! Splits.X_add_C (-a)

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

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
hf : f.Splits
hf0 : ¬f.leadingCoeff = 0
m : Multiset R
hm : f = C f.leadingCoeff * (Multiset.map (fun x ↦ X - C x) m).prod
⊢ (Multiset.map (fun x ↦ X - C x) m).prod.roots = m

Tactic:
roots_multiset_prod_X_sub_C

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
hf : f.Splits
hf0 : ¬f.leadingCoeff = 0
m : Multiset R
hm : f = C f.leadingCoeff * (Multiset.map (fun x ↦ X - C x) m).prod
⊢ m = m
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
⊢ (IsLocalization.map Sₘ (algebraMap R S) ⋯).IsIntegral

Tactic:
by
  intro x
  obtain ⟨⟨s, ⟨u, hu⟩⟩, hx⟩ := surj (Algebra.algebraMapSubmonoid S M) x
  obtain ⟨v, hv⟩ := hu
  obtain ⟨v', hv'⟩ := isUnit_iff_exists_inv'.1 (map_units Rₘ ⟨v, hv.1⟩)
  refine @IsIntegral.of_mul_unit Rₘ _ _ _ (localizationAlgebra M S) x (algebraMap S Sₘ u) v' ?_ ?_
  · replace hv' := congr_arg (@algebraMap Rₘ Sₘ _ _ (localizationAlgebra M S)) hv'
    rw [map_mul, map_one, localizationAlgebraMap_def, IsLocalization.map_eq] at hv'
    exact hv.2 ▸ hv'
  · obtain ⟨p, hp⟩ := Algebra.IsIntegral.isIntegral (R := R) s
    exact hx.symm ▸ is_integral_localization_at_leadingCoeff p hp.2 (hp.1.symm ▸ M.one_mem)

Goal state after:
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic

Goal state before:
pp: case pos
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
fl : FaithfullyFlat R M
N : Type u_1
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : Nontrivial N
n : N
hn : n ≠ 0
I : Ideal R := (R ∙ n).annihilator
I_ne_top : 1 ∈ I
⊢ Nontrivial (N ⊗[R] M)

Tactic:
Submodule.mem_annihilator_span_singleton,

Goal state after:
case pos
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
fl : FaithfullyFlat R M
N : Type u_1
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : Nontrivial N
n : N
hn : n ≠ 0
I : Ideal R := (R ∙ n).annihilator
I_ne_top : 1 • n = 0
⊢ Nontrivial (N ⊗[R] M)
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
s : S
a : A
ha : IsAlgebraic R a
inst✝ : FaithfulSMul R S
p : R[X]
h : p ≠ 0
eval0 : (aeval a) p = 0
⊢ (aeval (Algebra.TensorProduct.includeRight a)) (map (algebraMap R S) p) = 0

Tactic:
← AlgHom.coe_toRingHom (A := A),

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
s : S
a : A
ha : IsAlgebraic R a
inst✝ : FaithfulSMul R S
p : R[X]
h : p ≠ 0
eval0 : (aeval a) p = 0
⊢ (aeval (↑Algebra.TensorProduct.includeRight a)) (map (algebraMap R S) p) = 0
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic

Goal state before:
pp: case mpr
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
A : Type u_1
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : FaithfullyFlat R A
m : M
⊢ m = 0 → 1 ⊗ₜ[R] m = 0

pp: case mp
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
A : Type u_1
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : FaithfullyFlat R A
m : M
⊢ 1 ⊗ₜ[R] m = 0 → m = 0

Tactic:
· rintro rfl; rw [tmul_zero]

Goal state after:
case mp
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
A : Type u_1
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : FaithfullyFlat R A
m : M
⊢ 1 ⊗ₜ[R] m = 0 → m = 0
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic

Goal state before:
pp: case mp
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
A : Type u_1
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : FaithfullyFlat R A
m : M
h : 1 ⊗ₜ[R] m = 0
f : R →ₗ[R] M := (LinearMap.lsmul R M).flip m
⊢ m = 0

Tactic:
suffices f = 0 by simpa [f] using DFunLike.congr_fun this 1

Goal state after:
case mp
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
A : Type u_1
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : FaithfullyFlat R A
m : M
h : 1 ⊗ₜ[R] m = 0
f : R →ₗ[R] M := (LinearMap.lsmul R M).flip m
⊢ f = 0
Module: Mathlib.RingTheory.LocalRing.ResidueField.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : IsLocalRing R
inst✝⁴ : CommRing S
inst✝³ : IsLocalRing S
inst✝² : CommRing T
inst✝¹ : IsLocalRing T
f : R →+* S
inst✝ : IsLocalHom f
a : R
ha : a ∈ maximalIdeal R
⊢ ((Ideal.Quotient.mk (maximalIdeal S)).comp f) a = 0

Tactic:
by
    unfold ResidueField
    rw [RingHom.comp_apply, Ideal.Quotient.eq_zero_iff_mem]
    exact map_nonunit f a ha

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

Goal state before:
pp: case hx
R : Type u_5
S : Type u_6
K : Type u_7
L : Type u_8
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : Field K
inst✝⁹ : CommRing L
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R K
inst✝⁶ : Algebra R L
inst✝⁵ : Algebra S L
inst✝⁴ : Algebra K L
inst✝³ : IsScalarTower R S L
inst✝² : IsScalarTower R K L
inst✝¹ : IsFractionRing S L
inst✝ : Algebra.IsIntegral R S
x : S
s : ↥S⁰
⊢ (algebraMap K L).IsIntegralElem ((algebraMap S L) x)

Tactic:
apply IsIntegral.tower_top (R := R)

Goal state after:
case hx
R : Type u_5
S : Type u_6
K : Type u_7
L : Type u_8
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : Field K
inst✝⁹ : CommRing L
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R K
inst✝⁶ : Algebra R L
inst✝⁵ : Algebra S L
inst✝⁴ : Algebra K L
inst✝³ : IsScalarTower R S L
inst✝² : IsScalarTower R K L
inst✝¹ : IsFractionRing S L
inst✝ : Algebra.IsIntegral R S
x : S
s : ↥S⁰
⊢ IsIntegral R ((algebraMap S L) x)
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: case hy
R : Type u_5
S : Type u_6
K : Type u_7
L : Type u_8
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : Field K
inst✝⁹ : CommRing L
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R K
inst✝⁶ : Algebra R L
inst✝⁵ : Algebra S L
inst✝⁴ : Algebra K L
inst✝³ : IsScalarTower R S L
inst✝² : IsScalarTower R K L
inst✝¹ : IsFractionRing S L
inst✝ : Algebra.IsIntegral R S
x : S
s : ↥S⁰
⊢ IsIntegral K ⅟(mk' L 1 s)

Tactic:
apply IsIntegral.tower_top (R := R)

Goal state after:
case hy
R : Type u_5
S : Type u_6
K : Type u_7
L : Type u_8
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : Field K
inst✝⁹ : CommRing L
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R K
inst✝⁶ : Algebra R L
inst✝⁵ : Algebra S L
inst✝⁴ : Algebra K L
inst✝³ : IsScalarTower R S L
inst✝² : IsScalarTower R K L
inst✝¹ : IsFractionRing S L
inst✝ : Algebra.IsIntegral R S
x : S
s : ↥S⁰
⊢ IsIntegral R ⅟(mk' L 1 s)
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : IsLocalRing A
inst✝² : IsLocalRing B
inst✝¹ : Flat A B
inst✝ : IsLocalHom (algebraMap A B)
m : Ideal A
hm : m.IsMaximal
eqt : Submodule.restrictScalars A (Ideal.map (algebraMap A B) (IsLocalRing.maximalIdeal A)) = ⊤
this :
  Submodule.restrictScalars A (Ideal.map (algebraMap A B) (IsLocalRing.maximalIdeal A)) ≤
    Submodule.restrictScalars A (IsLocalRing.maximalIdeal B)
⊢ False

Tactic:
rw [eqt, top_le_iff, Submodule.restrictScalars_eq_top_iff] at this

Goal state after:
A : Type u_1
B : Type u_2
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : IsLocalRing A
inst✝² : IsLocalRing B
inst✝¹ : Flat A B
inst✝ : IsLocalHom (algebraMap A B)
m : Ideal A
hm : m.IsMaximal
eqt : Submodule.restrictScalars A (Ideal.map (algebraMap A B) (IsLocalRing.maximalIdeal A)) = ⊤
this : IsLocalRing.maximalIdeal B = ⊤
⊢ False
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : IsDomain B
inst✝² : Flat A B
inst✝¹ : Algebra.IsIntegral A B
inst✝ : FaithfulSMul A B
⊢ FaithfullyFlat A B

Tactic:
refine Module.FaithfullyFlat.of_comap_surjective fun P ↦ ?_

Goal state after:
A : Type u_1
B : Type u_2
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : IsDomain B
inst✝² : Flat A B
inst✝¹ : Algebra.IsIntegral A B
inst✝ : FaithfulSMul A B
P : PrimeSpectrum A
⊢ ∃ a, PrimeSpectrum.comap (algebraMap A B) a = P
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
⊢ map (algebraMap R (Localization.AtPrime p)) p ≤
    sInf {J | map (algebraMap R (Localization.AtPrime p)) I ≤ J ∧ J.IsPrime}

Tactic:
le_sInf_iff

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
⊢ ∀ b ∈ {J | map (algebraMap R (Localization.AtPrime p)) I ≤ J ∧ J.IsPrime},
    map (algebraMap R (Localization.AtPrime p)) p ≤ b
Module: Mathlib.RingTheory.KrullDimension.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : ⊥.IsPrime
⊢ KrullDimLE 1 R ↔ ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → I.IsMaximal

Tactic:
let : OrderBot (PrimeSpectrum R) := { bot := ⟨⊥, ‹_›⟩, bot_le I := bot_le (a := I.1) }
  simp_rw [Ring.KrullDimLE, Order.krullDimLE_iff, Nat.cast_one,
    Order.krullDim_le_one_iff_forall_isMax, (PrimeSpectrum.equivSubtype R).forall_congr_left,
    Subtype.forall, PrimeSpectrum.isMax_iff, forall_comm (α := _ ≠ ⊥),
    ne_eq, PrimeSpectrum.ext_iff]
  rfl

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b c : { x // IsIdempotentElem x }
⊢ ↑a * ↑b + ↑a * ↑c - ↑a * (↑b * ↑c) = ↑a * ↑b + ↑a * ↑c - ↑a * ↑b * (↑a * ↑c)

Tactic:
mul_mul_mul_comm

Goal state after:
R : Type u_1
inst✝ : CommRing R
a b c : { x // IsIdempotentElem x }
⊢ ↑a * ↑b + ↑a * ↑c - ↑a * (↑b * ↑c) = ↑a * ↑b + ↑a * ↑c - ↑a * ↑a * (↑b * ↑c)
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p : Ideal R
hp : p ∈ minimalPrimes R
⊢ ∀ ⦃a : R⦄, a ∈ p → a ∉ nonZeroDivisors R

Tactic:
mem_nonZeroDivisors_iff_right,

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
p : Ideal R
hp : p ∈ minimalPrimes R
⊢ ∀ ⦃a : R⦄, a ∈ p → ¬∀ (x : R), x * a = 0 → x = 0
Module: Mathlib.RingTheory.Spectrum.Prime.RingHom

Goal state before:
pp: case h
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
h : Nontrivial (p.asIdeal.ResidueField ⊗[R] S)
m : Ideal (k ⊗[R] S)
hm : m.IsMaximal
⊢ (comap (algebraMap R k) (comap Algebra.TensorProduct.includeLeftRingHom { asIdeal := m, isPrime := ⋯ })).asIdeal =
    p.asIdeal

Tactic:
simp [Ideal.eq_bot_of_prime, k, ← RingHom.ker_eq_comap_bot]

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:
Algebra.mem_bot,

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
⊢ x ∈ ⨅ v, Localization.subalgebra.ofField K v.asIdeal.primeCompl ⋯ ↔ x ∈ range ⇑(algebraMap R K)
Module: Mathlib.Topology.Compactness.Bases

Goal state before:
pp: case mpr.left
X : Type u_1
ι : Type u_2
inst✝ : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsCompact (b i)
s : Set ι
hs : s.Finite
⊢ IsCompact (⋃ i ∈ s, b i)

pp: case mpr.right
X : Type u_1
ι : Type u_2
inst✝ : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsCompact (b i)
s : Set ι
hs : s.Finite
⊢ IsOpen (⋃ i ∈ s, b i)

Tactic:
· exact hs.isCompact_biUnion fun i _ => hb' i

Goal state after:
case mpr.right
X : Type u_1
ι : Type u_2
inst✝ : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsCompact (b i)
s : Set ι
hs : s.Finite
⊢ IsOpen (⋃ i ∈ s, b i)
Module: Mathlib.Topology.LocallyClosed

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : X → Y
hf : IsInducing f
⊢ IsLocallyClosed s ↔ ∃ s', IsLocallyClosed s' ∧ f ⁻¹' s' = s

Tactic:
simp_rw [IsLocallyClosed, hf.isOpen_iff, hf.isClosed_iff]
  constructor
  · rintro ⟨_, _, ⟨U, hU, rfl⟩, ⟨Z, hZ, rfl⟩, rfl⟩
    exact ⟨_, ⟨U, Z, hU, hZ, rfl⟩, rfl⟩
  · rintro ⟨_, ⟨U, Z, hU, hZ, rfl⟩, rfl⟩
    exact ⟨_, _, ⟨U, hU, rfl⟩, ⟨Z, hZ, rfl⟩, rfl⟩

Goal state after:
Module: Mathlib.Topology.LocalAtTarget

Goal state before:
pp: β : Type u_2
inst✝ : TopologicalSpace β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
s : Set β
this : ∀ (i : ι), coborder (Subtype.val ⁻¹' s) = Subtype.val ⁻¹' coborder s
⊢ IsLocallyClosed s ↔ ∀ (i : ι), IsLocallyClosed (Subtype.val ⁻¹' s)

Tactic:
simp [isLocallyClosed_iff_isOpen_coborder, hU.isOpen_iff_coe_preimage, this]

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

Goal state before:
pp: case refine_1
α : Type u_2
inst✝ : TopologicalSpace α
s : Opens α
⊢ (∀ (ι : Type u_2) (s_1 : ι → Opens α), s ≤ iSup s_1 → ∃ t, s ≤ t.sup s_1) →
    ∀ {ι : Type u_2} (U : ι → Set α), (∀ (i : ι), IsOpen[inst✝] (U i)) → ↑s ⊆ ⋃ i, U i → ∃ t, ↑s ⊆ ⋃ i ∈ t, U i

Tactic:
introv H hU hU'

Goal state after:
case refine_1
α : Type u_2
inst✝ : TopologicalSpace α
s : Opens α
H : ∀ (ι : Type u_2) (s_1 : ι → Opens α), s ≤ iSup s_1 → ∃ t, s ≤ t.sup s_1
ι : Type u_2
U : ι → Set α
hU : ∀ (i : ι), IsOpen[inst✝] (U i)
hU' : ↑s ⊆ ⋃ i, U i
⊢ ∃ t, ↑s ⊆ ⋃ i ∈ t, U i
Module: Mathlib.Topology.LocalAtTarget

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
hf : ∀ (i : ι), GeneralizingMap ((U i).carrier.restrictPreimage f)
x : α
y : β
h : (fun x1 x2 ↦ x1 ⤳ x2) y (f x)
i : ι
hx : f x ∈ U i
⊢ ∃ a', (fun x1 x2 ↦ x1 ⤳ x2) a' x ∧ f a' = y

Tactic:
have h : (⟨y, (U i).2.stableUnderGeneralization h hx⟩ : U i) ⤳
    (U i).1.restrictPreimage f ⟨x, hx⟩ := by rwa [subtype_specializes_iff]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
hf : ∀ (i : ι), GeneralizingMap ((U i).carrier.restrictPreimage f)
x : α
y : β
h✝ : (fun x1 x2 ↦ x1 ⤳ x2) y (f x)
i : ι
hx : f x ∈ U i
h : ⟨y, ⋯⟩ ⤳ (U i).carrier.restrictPreimage f ⟨x, hx⟩
⊢ ∃ a', (fun x1 x2 ↦ x1 ⤳ x2) a' x ∧ f a' = y
Module: Mathlib.Topology.NoetherianSpace

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
⊢ NoetherianSpace α ↔ WellFoundedLT (Closeds α)

Tactic:
simp_rw [isWellFounded_iff]

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
⊢ (WellFounded fun x1 x2 ↦ x2 < x1) ↔ WellFounded fun x1 x2 ↦ x1 < x2
Module: Mathlib.Topology.NoetherianSpace

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
s : Closeds α
H : ∀ y < s, ∃ S, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ y = sSup S
h₀ : s ≠ ⊥
z₂ : Set α
hz₂ : IsClosed[inst✝¹] z₂
hz₂' : ¬↑s ⊆ z₂
z₁ : Closeds α
h : ↑s ⊆ ↑z₁ ∪ z₂
hz₁' : ¬↑s ⊆ ↑z₁
⊢ ∃ S, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ s = sSup S

Tactic:
lift z₂ to Closeds α using hz₂

Goal state after:
case neg
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
s : Closeds α
H : ∀ y < s, ∃ S, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ y = sSup S
h₀ : s ≠ ⊥
z₁ : Closeds α
hz₁' : ¬↑s ⊆ ↑z₁
z₂ : Closeds α
hz₂' : ¬↑s ⊆ ↑z₂
h : ↑s ⊆ ↑z₁ ∪ ↑z₂
⊢ ∃ S, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ s = sSup S
Module: Mathlib.Topology.NoetherianSpace

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
s : Closeds α
⊢ ∃ S, (∀ (k : ↥S), IsIrreducible ↑↑k) ∧ s = S.sup id

Tactic:
simpa [Set.exists_finite_iff_finset, Finset.sup_id_eq_sSup]
    using NoetherianSpace.exists_finite_set_closeds_irreducible s

Goal state after:
Module: Mathlib.Order.Ideal

Goal state before:
pp: P : Type u_1
inst✝² : LE P
inst✝¹ : IsDirectedOrder P
inst✝ : Nonempty P
I : Ideal P
hI : IsCoatom I
x✝ : Ideal P
hJ : I < x✝
⊢ ↑x✝ = univ

Tactic:
by simp [hI.2 _ hJ]

Goal state after:
Module: Mathlib.Topology.QuasiSeparated

Goal state before:
pp: α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : QuasiSeparatedSpace α
inst✝ : CompactSpace α
s : Set (Set α)
hf : s.Finite
ho : ∀ t ∈ s, IsOpen[inst✝²] t ∨ IsClosed[inst✝²] t
hc : ∀ t ∈ s, IsCompact t
⊢ IsCompact (⋂₀ s)

Tactic:
obtain (rfl | hne) := s.eq_empty_or_nonempty
  · simp [CompactSpace.isCompact_univ]
  · exact QuasiSeparatedSpace.isCompact_sInter_of_nonempty hf hne ho hc

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Descent

Goal state before:
pp: A B : Type u
inst✝¹ : CommRing A
inst✝ : CommRing B
f : A →+* B
hf : f.FaithfullyFlat
⊢ (extendScalars f).ReflectsIsomorphisms

Tactic:
refine ⟨fun {M N} g h ↦ ?_⟩

Goal state after:
A B : Type u
inst✝¹ : CommRing A
inst✝ : CommRing B
f : A →+* B
hf : f.FaithfullyFlat
M N : ModuleCat A
g : M ⟶ N
h : IsIso ((extendScalars f).map g)
⊢ IsIso g
Module: Mathlib.RingTheory.Ideal.GoingDown

Goal state before:
pp: case refine_1
R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h : HasGoingDown R S
⊢ GeneralizingMap (PrimeSpectrum.comap (algebraMap R S))

Tactic:
Q

Goal state after:
case refine_1
R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h : HasGoingDown R S
Q : PrimeSpectrum S
⊢ ∀ ⦃b : PrimeSpectrum R⦄,
    (fun x1 x2 ↦ x1 ⤳ x2) b (PrimeSpectrum.comap (algebraMap R S) Q) →
      ∃ a', (fun x1 x2 ↦ x1 ⤳ x2) a' Q ∧ PrimeSpectrum.comap (algebraMap R S) a' = b
Module: Mathlib.RingTheory.Derivation.ToSquareZero

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I : Ideal B
f₁ f₂ : A →ₐ[R] B
e : (Ideal.Quotient.mkₐ R I).comp f₁ = (Ideal.Quotient.mkₐ R I).comp f₂
x : A
⊢ (f₁.toLinearMap - f₂.toLinearMap) x ∈ Submodule.restrictScalars R I

Tactic:
simpa [Ideal.Quotient.eq] using congr($e x)

Goal state after:
Module: Mathlib.RingTheory.RingHom.Flat

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ (algebraMap R S).Flat ↔ Module.Flat R S

Tactic:
rw [RingHom.Flat, toAlgebra_algebraMap]

Goal state after: