mathlib-initiative/mathlib-tactics huggingface dataset:
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)
hq : map f q = p
⊢ ∀ (a : ℕ), p.coeff a ≠ 0 ∧ g a ≠ 0 ↔ p.coeff a ≠ 0

Tactic:
and_iff_left_iff_imp,

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)
hq : map f q = p
⊢ ∀ (a : ℕ), p.coeff a ≠ 0 → g a ≠ 0
Module: Mathlib.Data.Nat.Choose.Vandermonde

Goal state before:
pp: n : ℕ
⊢ ∑ i ∈ range (n + 1), n.choose i ^ 2 = (2 * n).choose n

Tactic:
by
  rw [two_mul, add_choose_eq, sum_antidiagonal_eq_sum_range_succ_mk]
  congr! 1 with _ h
  rw [choose_symm (Finset.mem_range_succ_iff.mp h), sq]

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

Goal state before:
pp: case inl
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
a✝ : Nontrivial R
h✝ : IsEmpty n
⊢ M.charpolyRev.coeff 1 = -M.trace

pp: case inr
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
a✝ : Nontrivial R
h✝ : Nonempty n
⊢ M.charpolyRev.coeff 1 = -M.trace

Tactic:
· simp [charpolyRev, coeff_one]

Goal state after:
case inr
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
a✝ : Nontrivial R
h✝ : Nonempty n
⊢ M.charpolyRev.coeff 1 = -M.trace
Module: Mathlib.Algebra.Polynomial.HasseDeriv

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
k n : ℕ
r : R
⊢ (hasseDeriv k) ((monomial n) r) = (monomial (n - k)) (↑(n.choose k) * r)

Tactic:
ext i
  simp only [hasseDeriv_coeff, coeff_monomial]
  by_cases hnik : n = i + k
  · grind
  · rw [if_neg hnik, mul_zero]
    by_cases! hkn : k ≤ n
    · rw [← tsub_eq_iff_eq_add_of_le hkn] at hnik
      rw [if_neg hnik]
    · rw [Nat.choose_eq_zero_of_lt hkn, Nat.cast_zero, zero_mul, ite_self]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
k l : ℕ
⊢ hasseDeriv k ∘ₗ hasseDeriv l = (k + l).choose k • hasseDeriv (k + l)

Tactic:
by
  ext i : 2
  simp only [LinearMap.smul_apply, comp_apply, LinearMap.coe_comp, smul_monomial, hasseDeriv_apply,
    mul_one, monomial_eq_zero_iff, sum_monomial_index, mul_zero, ←
    tsub_add_eq_tsub_tsub, add_comm l k]
  rw_mod_cast [nsmul_eq_mul]
  rw [← Nat.cast_mul]
  congr 2
  by_cases! hikl : i < k + l
  · rw [choose_eq_zero_of_lt hikl, mul_zero]
    by_cases! hil : i < l
    · rw [choose_eq_zero_of_lt hil, mul_zero]
    · rw [← tsub_lt_iff_right hil] at hikl
      rw [choose_eq_zero_of_lt hikl, zero_mul]
  apply @cast_injective ℚ
  have h1 : l ≤ i := le_of_add_le_right hikl
  have h2 : k ≤ i - l := le_tsub_of_add_le_right hikl
  have h3 : k ≤ k + l := le_self_add
  push_cast
  rw [cast_choose ℚ h1, cast_choose ℚ h2, cast_choose ℚ h3, cast_choose ℚ hikl]
  rw [show i - (k + l) = i - l - k by rw [add_comm]; apply tsub_add_eq_tsub_tsub]
  simp only [add_tsub_cancel_left]
  field

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
D : ℕ → R[X] →+ R[X] := fun k ↦ (hasseDeriv k).toAddMonoidHom
Φ : R[X] →+ R[X] →+ R[X] := mul
m : ℕ
r : R
n : ℕ
s : R
x : ℕ × ℕ
hm : x.1 ≤ m
hn : x.2 ≤ n
⊢ (monomial (m + n - (x.1 + x.2))) (↑(m.choose x.1) * (r * (↑(n.choose x.2) * s))) =
    (monomial (m + n - (x.1 + x.2))) (↑(m.choose x.1) * ↑(n.choose x.2) * (r * s))

Tactic:
← mul_assoc r,

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
D : ℕ → R[X] →+ R[X] := fun k ↦ (hasseDeriv k).toAddMonoidHom
Φ : R[X] →+ R[X] →+ R[X] := mul
m : ℕ
r : R
n : ℕ
s : R
x : ℕ × ℕ
hm : x.1 ≤ m
hn : x.2 ≤ n
⊢ (monomial (m + n - (x.1 + x.2))) (↑(m.choose x.1) * (r * ↑(n.choose x.2) * s)) =
    (monomial (m + n - (x.1 + x.2))) (↑(m.choose x.1) * ↑(n.choose x.2) * (r * s))
Module: Mathlib.RingTheory.Polynomial.ScaleRoots

Goal state before:
pp: R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : R[X]
a : A
r : R
ha : (aeval a) p = 0
⊢ eval₂ (algebraMap R A) ((algebraMap R A) r * a) (p.scaleRoots r) = 0

Tactic:
scaleRoots_eval₂_mul_of_commute,

Goal state after:
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : R[X]
a : A
r : R
ha : (aeval a) p = 0
⊢ (algebraMap R A) r ^ p.natDegree * eval₂ (algebraMap R A) a p = 0

case hsa
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : R[X]
a : A
r : R
ha : (aeval a) p = 0
⊢ Commute ((algebraMap R A) r) a

case hf
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : R[X]
a : A
r : R
ha : (aeval a) p = 0
⊢ ∀ (s₁ s₂ : R), Commute ((algebraMap R A) s₁) ((algebraMap R A) s₂)
Module: Mathlib.RingTheory.Polynomial.IntegralNormalization

Goal state before:
pp: case pos
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
h : ¬p.degree = ↑i
h' : ↑i < p.degree
⊢ 1 ≤ p.natDegree - i

Tactic:
le_tsub_iff_left (coe_lt_degree.mp h').le,

Goal state after:
case pos
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
h : ¬p.degree = ↑i
h' : ↑i < p.degree
⊢ i + 1 ≤ p.natDegree
Module: Mathlib.RingTheory.Polynomial.Subring

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
T : Subring R
p : (↥T)[X]
n : ℕ
⊢ (ofSubring T p).coeff n = ↑(p.coeff n)

Tactic:
simp only [ofSubring, coeff_monomial, finsetSum_coeff, mem_support_iff, Finset.sum_ite_eq',
    Ne, Classical.not_not, ite_eq_left_iff]
  intro h
  rw [h, ZeroMemClass.coe_zero]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f g : R[X]
hf : f.Splits
hg : g.natDegree ≤ 1
h : Invertible g.leadingCoeff
⊢ (f.comp g).Splits

Tactic:
rcases lt_or_eq_of_le hg with hg | hg
  · rw [eq_C_of_natDegree_eq_zero (Nat.lt_one_iff.mp hg)]
    simp
  obtain ⟨m, hm⟩ := splits_iff_exists_multiset'.mp hf
  rw [hm, mul_comp, C_comp, multiset_prod_comp]
  refine (Splits.C _).mul (multisetProd ?_)
  simp only [Multiset.mem_map]
  rintro - ⟨-, ⟨a, -, rfl⟩, rfl⟩
  apply of_natDegree_le_one_of_invertible (by simpa)
  rw [leadingCoeff, hg] at h
  simpa [leadingCoeff, hg]

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

Goal state before:
pp: case pos
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
p : R[X]
x : S
h : eval₂ f x p = 0
h' : ¬1 ≤ p.natDegree
hp : f p.leadingCoeff = 0
⊢ f.IsIntegralElem (f p.leadingCoeff * x)

Tactic:
rw [hp, zero_mul]

Goal state after:
case pos
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
p : R[X]
x : S
h : eval₂ f x p = 0
h' : ¬1 ≤ p.natDegree
hp : f p.leadingCoeff = 0
⊢ f.IsIntegralElem 0
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
⊢ (Multiset.map (fun ij ↦ ij.1 - ij.2) (g.roots ×ˢ s)).prod =
    (Multiset.map (fun ij ↦ -1 * (ij.1 - ij.2)) (s ×ˢ g.roots)).prod

Tactic:
rw [← Multiset.map_swap_product, Multiset.map_map]; simp

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
t s : S
hst : s * t = 1
ht : IsIntegral (↥R[s]) t
a✝ : Nontrivial S
φ : R[X] →ₐ[R] S := aeval s
⊢ φ.IsIntegralElem t

Tactic:
by
    obtain ⟨p, hpm, hpt⟩ := ht
    have : p.map (algebraMap _ S) ∈ lifts φ.toRingHom := (lifts_iff_coeff_lifts _).mpr
      (by simp [← AlgHom.mem_range, φ, ← Algebra.adjoin_singleton_eq_range_aeval])
    obtain ⟨q, hqp, hqd, hqm⟩ := lifts_and_degree_eq_and_monic this (hpm.map _)
    exact ⟨q, hqm, by rw [← eval_map, hqp, eval_map, hpt]⟩

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

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

Tactic:
let H := LinearMap.ker l23 ⧸ LinearMap.range (Submodule.inclusion complex)

Goal state after:
R : Type u
M : Type v
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N1 : Type u_1
inst✝⁵ : AddCommGroup N1
inst✝⁴ : Module R N1
N2 : Type u_2
inst✝³ : AddCommGroup N2
inst✝² : Module R N2
N3 : Type u_3
inst✝¹ : AddCommGroup N3
inst✝ : Module R N3
l12 : N1 →ₗ[R] N2
l23 : N2 →ₗ[R] N3
fl : FaithfullyFlat R M
ex : Function.Exact ⇑(LinearMap.rTensor M l12) ⇑(LinearMap.rTensor M l23)
complex : l12.range ≤ l23.ker
H : Type u_2 := ↥l23.ker ⧸ (Submodule.inclusion complex).range
⊢ l23.ker = l12.range
Module: Mathlib.RingTheory.Ideal.GoingUp

Goal state before:
pp: case mp
R : Type u_3
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal R
hf₁ : RingHom.ker f ≤ I
hf₂ : f.IsIntegral
h : ¬I = ⊤
x✝ : Algebra R S := f.toAlgebra
this : Algebra.IsIntegral R S
m' : Ideal S
left✝¹ : m'.IsMaximal
left✝ : (comap (algebraMap R S) m').IsMaximal
hm : I ≤ comap (algebraMap R S) m'
⊢ ¬map f I = ⊤

Tactic:
rw [← map_le_iff_le_comap] at hm

Goal state after:
case mp
R : Type u_3
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal R
hf₁ : RingHom.ker f ≤ I
hf₂ : f.IsIntegral
h : ¬I = ⊤
x✝ : Algebra R S := f.toAlgebra
this : Algebra.IsIntegral R S
m' : Ideal S
left✝¹ : m'.IsMaximal
left✝ : (comap (algebraMap R S) m').IsMaximal
hm : map (algebraMap R S) I ≤ m'
⊢ ¬map f I = ⊤
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

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

Tactic:
use ({⟨p_id, h_pp⟩} : Multiset (PrimeSpectrum A)), le_top

Goal state after:
case right
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
hA_nont : Nontrivial A
hgt : ∀ J > ⊤, J ≠ ⊥ → ∃ Z, (Multiset.map asIdeal Z).prod ≤ J ∧ (Multiset.map asIdeal Z).prod ≠ ⊥
h_nzI : ⊤ ≠ ⊥
p_id : Ideal A
h_nzp : p_id ≠ ⊥
h_pp : p_id.IsPrime
⊢ (Multiset.map asIdeal {{ asIdeal := p_id, isPrime := h_pp }}).prod ≠ ⊥
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
f : R →ₗ[R] M := (LinearMap.lsmul R M).flip m
a : A
h : a • 1 ⊗ₜ[R] m = a • 0
⊢ ((AlgebraTensorModule.curry (LinearMap.lTensor A f)) a) 1 = ((AlgebraTensorModule.curry 0) a) 1

Tactic:
rw [smul_zero, smul_tmul', smul_eq_mul, mul_one] at h

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
f : R →ₗ[R] M := (LinearMap.lsmul R M).flip m
a : A
h : a ⊗ₜ[R] m = 0
⊢ ((AlgebraTensorModule.curry (LinearMap.lTensor A f)) a) 1 = ((AlgebraTensorModule.curry 0) a) 1
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
g : S →+* T
f : R →+* S
hg : (g.comp f).SurjectiveOnStalks
I : Ideal T
hI : I.IsPrime
this :
  Function.Surjective
    ⇑((Localization.localRingHom (Ideal.comap g I) I g ⋯).comp
        (Localization.localRingHom (Ideal.comap (g.comp f) I) (Ideal.comap g I) f ⋯))
⊢ Function.Surjective ⇑(Localization.localRingHom (Ideal.comap g I) I g ⋯)

Tactic:
RingHom.coe_comp

Goal state after:
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
T : Type u_3
inst✝ : CommRing T
g : S →+* T
f : R →+* S
hg : (g.comp f).SurjectiveOnStalks
I : Ideal T
hI : I.IsPrime
this :
  Function.Surjective
    (⇑(Localization.localRingHom (Ideal.comap g I) I g ⋯) ∘
      ⇑(Localization.localRingHom (Ideal.comap (g.comp f) I) (Ideal.comap g I) f ⋯))
⊢ Function.Surjective ⇑(Localization.localRingHom (Ideal.comap g I) I g ⋯)
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
g : S →+* T
f : R →+* S
hg : (g.comp f).SurjectiveOnStalks
I : Ideal T
hI : I.IsPrime
this : Function.Surjective ⇑(Localization.localRingHom (Ideal.comap (g.comp f) I) I (g.comp f) ⋯)
⊢ Function.Surjective ⇑(Localization.localRingHom (Ideal.comap g I) I g ⋯)

Tactic:
rw [Localization.localRingHom_comp (I.comap (g.comp f)) (I.comap g) _ _ rfl _ rfl,
    RingHom.coe_comp] at this

Goal state after:
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
T : Type u_3
inst✝ : CommRing T
g : S →+* T
f : R →+* S
hg : (g.comp f).SurjectiveOnStalks
I : Ideal T
hI : I.IsPrime
this :
  Function.Surjective
    (⇑(Localization.localRingHom (Ideal.comap g I) I g ⋯) ∘
      ⇑(Localization.localRingHom (Ideal.comap (g.comp f) I) (Ideal.comap g I) f ⋯))
⊢ Function.Surjective ⇑(Localization.localRingHom (Ideal.comap g I) I g ⋯)
Module: Mathlib.RingTheory.SurjectiveOnStalks

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
S : Type u_2
inst✝² : CommRing S
f : R →+* S
inst✝¹ : IsLocalRing S
inst✝ : IsLocalHom f
H : f.SurjectiveOnStalks
x : S
y r : R
c : S
e : c * f r * x = c * f y
hc : IsUnit c
hr : IsUnit (f r)
⊢ ∃ a, f a = x

Tactic:
refine ⟨(isUnit_of_map_unit f r hr).unit⁻¹ * y, ?_⟩

Goal state after:
R : Type u_1
inst✝³ : CommRing R
S : Type u_2
inst✝² : CommRing S
f : R →+* S
inst✝¹ : IsLocalRing S
inst✝ : IsLocalHom f
H : f.SurjectiveOnStalks
x : S
y r : R
c : S
e : c * f r * x = c * f y
hc : IsUnit c
hr : IsUnit (f r)
⊢ f (↑⋯.unit⁻¹ * y) = x
Module: Mathlib.Algebra.Order.Ring.Idempotent

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

Tactic:
mul_mul_mul_comm _ b.1.1,

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
a✝ b✝ a b : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
⊢ (↑a).1 * ((↑a).2 * (↑b).2) + (↑a).2 * (↑a).2 * ((↑b).1 * (↑b).2) = 0
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 }
⊢ (↑a).2 * (↑b).2 + ((↑a).1 * ((↑a).2 * (↑c).2) + (↑a).2 * (↑b).1 * ((↑a).2 * (↑c).2)) =
    (↑a).2 * (↑b).2 + (↑a).2 * ((↑b).1 * (↑c).2)

Tactic:
mul_mul_mul_comm _ b.1.1,

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 }
⊢ (↑a).2 * (↑b).2 + ((↑a).1 * ((↑a).2 * (↑c).2) + (↑a).2 * (↑a).2 * ((↑b).1 * (↑c).2)) =
    (↑a).2 * (↑b).2 + (↑a).2 * ((↑b).1 * (↑c).2)
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 ⊔ c)) = ↑(a ⊓ b ⊔ a ⊓ c)

Tactic:
simp_rw [(· ⊔ ·), (· ⊓ ·), SemilatticeSup.sup, SemilatticeInf.inf, Lattice.inf,
      SemilatticeInf.inf, mul_sub, mul_add, mul_mul_mul_comm]
    rw [a.2]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
S : Type u_3
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I : Ideal R
⊢ (I ⊔ comap f ⊥).minimalPrimes = comap f ∘ map f '' (I ⊔ RingHom.ker f).minimalPrimes

Tactic:
Set.image_congr,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
S : Type u_3
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I : Ideal R
⊢ (I ⊔ comap f ⊥).minimalPrimes = ?m.79 '' (I ⊔ RingHom.ker f).minimalPrimes

R : Type u_1
inst✝¹ : CommRing R
S : Type u_3
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I : Ideal R
⊢ ∀ a ∈ (I ⊔ RingHom.ker f).minimalPrimes, (comap f ∘ map f) a = ?m.79 a

R : Type u_1
inst✝¹ : CommRing R
S : Type u_3
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I : Ideal R
⊢ Ideal R → Ideal R
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
⊢ ∀ (a b : α), le a (sup a b)

Tactic:
by intros; simp [eq_le, eq_sup]

Goal state after:
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
⊢ ∀ (a b : α), le b (sup a b)

Tactic:
by intros; simp [eq_le, eq_sup]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
surj✝ : Function.Surjective ⇑(toPiLocalization R)
surj : Function.Surjective ⇑((toPiLocalization (PiLocalization R)).comp (toPiLocalization R).toRingHom)
⊢ Finite (MaximalSpectrum R)

Tactic:
RingHom.coe_comp

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
surj✝ : Function.Surjective ⇑(toPiLocalization R)
surj : Function.Surjective (⇑(toPiLocalization (PiLocalization R)).toRingHom ∘ ⇑(toPiLocalization R).toRingHom)
⊢ Finite (MaximalSpectrum R)
Module: Mathlib.RingTheory.Spectrum.Maximal.Localization

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
surj : Function.Surjective ⇑((toPiLocalization (PiLocalization R)).comp (toPiLocalization R).toRingHom)
⊢ Finite (PrimeSpectrum R)

Tactic:
RingHom.coe_comp

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
surj : Function.Surjective (⇑(toPiLocalization (PiLocalization R)).toRingHom ∘ ⇑(toPiLocalization R).toRingHom)
⊢ Finite (PrimeSpectrum R)
Module: Mathlib.Topology.LocallyClosed

Goal state before:
pp: case mp
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : X → Y
hf : IsInducing f
⊢ (∃ U Z, (∃ t, IsOpen[inst✝] t ∧ f ⁻¹' t = U) ∧ (∃ t, IsClosed[inst✝] t ∧ f ⁻¹' t = Z) ∧ s = U ∩ Z) →
    ∃ s', (∃ U Z, IsOpen[inst✝] U ∧ IsClosed[inst✝] Z ∧ s' = U ∩ Z) ∧ f ⁻¹' s' = s

Tactic:
rintro ⟨_, _, ⟨U, hU, rfl⟩, ⟨Z, hZ, rfl⟩, rfl⟩
    exact ⟨_, ⟨U, Z, hU, hZ, rfl⟩, rfl⟩

Goal state after:
Module: Mathlib.Topology.NoetherianSpace

Goal state before:
pp: case h
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
s : Closeds α
H : ∀ y < s, ∃ S, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ y = sSup S
h₀ : s ≠ ⊥
h₁ : IsIrreducible ↑s
⊢ {s}.Finite ∧ (∀ t ∈ {s}, IsIrreducible ↑t) ∧ s = sSup {s}

Tactic:
simp [h₁]

Goal state after:
Module: Mathlib.Topology.Sober

Goal state before:
pp: case h.a
α : Type u_1
inst✝ : TopologicalSpace α
ι : Type u_3
U : ι → Opens α
hU : IsOpenCover U
hU' : ∀ (i : ι), QuasiSober ↥(U i)
t : Set α
h : IsPreirreducible t
x : α
hx : x ∈ t
h' : IsClosed t
i : ι
hi : x ∈ U i
H : IsIrreducible (Subtype.val ⁻¹' t)
⊢ closure {↑H.genericPoint} ⊆ t

Tactic:
simpa [h'.closure_subset_iff, h'.closure_eq] using!
        continuous_subtype_val.closure_preimage_subset _ H.isGenericPoint_genericPoint_closure.mem

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
⊢ ComonadicLeftAdjoint (extendScalars f)

Tactic:
have := preservesFiniteLimits_extendScalars_of_flat hf.flat
  have := reflectsIsomorphisms_extendScalars_of_faithfullyFlat hf
  convert!
    Comonad.comonadicOfHasPreservesFSplitEqualizersOfReflectsIsomorphisms
      (extendRestrictScalarsAdj f)
  · exact ⟨inferInstance⟩
  · exact ⟨inferInstance⟩

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I J : Ideal R
⊢ zeroLocus ↑I = zeroLocus ↑J ↔ I.radical = J.radical

Tactic:
by
  constructor
  · intro h; simp_rw [← vanishingIdeal_zeroLocus_eq_radical, h]
  · intro h; rw [← zeroLocus_radical, h, zeroLocus_radical]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring A
inst✝³ : AddCommMonoid M
inst✝² : Algebra R A
inst✝¹ : Module A M
inst✝ : Module R M
D : Derivation R A M
n : ℕ
⊢ D ↑n = 0

Tactic:
rw [← nsmul_one, D.map_smul_of_tower n, map_one_eq_zero, smul_zero]

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case hfin
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : p ∈ (exponent G).factorization.support
he : 0 < exponent G
g : G
hg : g ^ (exponent G / p) ≠ 1
k : ℕ
hk : exponent G = p ^ (exponent G).factorization p * k
t : ℕ
ht : (exponent G).factorization p = t.succ
⊢ (g ^ k) ^ p ^ (t + 1) = 1

Tactic:
rw [← Nat.succ_eq_add_one, ← ht, ← pow_mul, mul_comm, ← hk]

Goal state after:
case hfin
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : p ∈ (exponent G).factorization.support
he : 0 < exponent G
g : G
hg : g ^ (exponent G / p) ≠ 1
k : ℕ
hk : exponent G = p ^ (exponent G).factorization p * k
t : ℕ
ht : (exponent G).factorization p = t.succ
⊢ g ^ exponent G = 1
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: α : Type u_1
G : Type u_2
G' : Type u_3
a : α
inst✝³ : Group α
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : IsCyclic α
H : Subgroup α
this : (a : Prop) → Decidable a
g : α
hg : ∀ (x : α), x ∈ zpowers g
hx✝ : ∃ x ∈ H, x ≠ 1
x✝¹ : α
hx₁ : x✝¹ ∈ H
hx₂ : x✝¹ ≠ 1
k✝ : ℤ
hk✝² : (fun x ↦ g ^ x) k✝ = x✝¹
hk✝¹ : g ^ k✝ = x✝¹
hex : ∃ n, 0 < n ∧ g ^ n ∈ H
x✝ : ↥H
x : α
hx : x ∈ H
k : ℤ
hk✝ : (fun x ↦ g ^ x) k = x
hk : g ^ k = x
hk₂ : g ^ (↑(Nat.find hex) * (k / ↑(Nat.find hex))) ∈ H
hk₃ : g ^ (k % ↑(Nat.find hex)) ∈ H
hk₄ : k % ↑(Nat.find hex) = ↑(k % ↑(Nat.find hex)).natAbs
hk₅ : g ^ (k % ↑(Nat.find hex)).natAbs ∈ H
hk₆ : (k % ↑(Nat.find hex)).natAbs = 0
⊢ ↑((fun x ↦ ⟨g ^ Nat.find hex, ⋯⟩ ^ x) (k / ↑(Nat.find hex))) = ↑⟨x, hx⟩

Tactic:
suffices g ^ ((Nat.find hex : ℤ) * (k / Nat.find hex : ℤ)) = x by simpa [zpow_mul]

Goal state after:
α : Type u_1
G : Type u_2
G' : Type u_3
a : α
inst✝³ : Group α
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : IsCyclic α
H : Subgroup α
this : (a : Prop) → Decidable a
g : α
hg : ∀ (x : α), x ∈ zpowers g
hx✝ : ∃ x ∈ H, x ≠ 1
x✝¹ : α
hx₁ : x✝¹ ∈ H
hx₂ : x✝¹ ≠ 1
k✝ : ℤ
hk✝² : (fun x ↦ g ^ x) k✝ = x✝¹
hk✝¹ : g ^ k✝ = x✝¹
hex : ∃ n, 0 < n ∧ g ^ n ∈ H
x✝ : ↥H
x : α
hx : x ∈ H
k : ℤ
hk✝ : (fun x ↦ g ^ x) k = x
hk : g ^ k = x
hk₂ : g ^ (↑(Nat.find hex) * (k / ↑(Nat.find hex))) ∈ H
hk₃ : g ^ (k % ↑(Nat.find hex)) ∈ H
hk₄ : k % ↑(Nat.find hex) = ↑(k % ↑(Nat.find hex)).natAbs
hk₅ : g ^ (k % ↑(Nat.find hex)).natAbs ∈ H
hk₆ : (k % ↑(Nat.find hex)).natAbs = 0
⊢ g ^ (↑(Nat.find hex) * (k / ↑(Nat.find hex))) = x
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case h
G : Type u
inst✝ : CommMonoid G
hG : ExponentExists G
he : exponent G ≠ 0
hne : (Set.range orderOf).Nonempty
hfin : (Set.range orderOf).Finite
t : G
ht : orderOf t = sSup (Set.range orderOf)
⊢ exponent G ∣ orderOf t

Tactic:
refine Nat.dvd_of_primeFactorsList_subperm he ?_

Goal state after:
case h
G : Type u
inst✝ : CommMonoid G
hG : ExponentExists G
he : exponent G ≠ 0
hne : (Set.range orderOf).Nonempty
hfin : (Set.range orderOf).Finite
t : G
ht : orderOf t = sSup (Set.range orderOf)
⊢ (exponent G).primeFactorsList.Subperm (orderOf t).primeFactorsList
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
h✝ : IsClopen s
e f : R
h : e * f = 0 ∧ e + f = 1 ∧ s = ↑(basicOpen e) ∧ sᶜ = ↑(basicOpen f)
⊢ e * f = 0 ∧ e + f = 1 ∧ s = ↑(basicOpen e)

Tactic:
by simp only [h, and_self]

Goal state after: