mathlib-initiative/mathlib-tactics huggingface dataset:
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
hm : f.Monic
x : R
hx : x ∈ f.roots
⊢ eval x (derivative f) = (Multiset.map (fun x_1 ↦ x - x_1) (f.roots.erase x)).prod

Tactic:
← eval_multiset_prod_X_sub_C_derivative hx,

Goal state after:
R : Type u_1
inst✝² : CommRing R
f : R[X]
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
hf : f.Splits
hm : f.Monic
x : R
hx : x ∈ f.roots
⊢ eval x (derivative f) = eval x (derivative (Multiset.map (fun a ↦ X - C a) f.roots).prod)
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
S : Type u_4
inst✝¹ : CommRing S
inst✝ : IsDomain S
f : R[X]
hf : f.Splits
φ : R →+* S
hφ : map φ f ≠ 0
⊢ (map φ f).roots = Multiset.map (⇑φ) f.roots

Tactic:
induction hf using Submonoid.closure_induction with
  | mem p hp => obtain (⟨r, rfl⟩ | ⟨a, rfl⟩) := hp <;> simp
  | one => simp
  | mul x y _ _ hx hy => simp_all [roots_mul, show x * y ≠ 0 by aesop]

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

Goal state before:
pp: 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
g : R[X]
hg₀ : g ≠ 0
a : R
f : R[X]
hf₀ : (X - C a) * f ≠ 0
this : X - C a ∣ (X - C a) * f ∨ X - C a ∣ g
h : ((X - C a) * (f * g)).Splits
hn : (f * g).natDegree = n
ha : eval a ((X - C a) * (f * g)) = 0
⊢ ((X - C a) * f).Splits ∧ g.Splits

Tactic:
have := ih (by aesop) hg₀ (f * g) rfl (splits_X_sub_C_mul_iff.mp h) hn

Goal state after:
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
g : R[X]
hg₀ : g ≠ 0
a : R
f : R[X]
hf₀ : (X - C a) * f ≠ 0
this✝ : X - C a ∣ (X - C a) * f ∨ X - C a ∣ g
h : ((X - C a) * (f * g)).Splits
hn : (f * g).natDegree = n
ha : eval a ((X - C a) * (f * g)) = 0
this : f.Splits ∧ g.Splits
⊢ ((X - C a) * f).Splits ∧ g.Splits
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
f g : R[X]
inst✝ : IsDomain R
hg₀ : g ≠ 0
hg : g.Splits
⊢ (f * g).Splits ↔ f.Splits

Tactic:
by
  simp [splits_mul', *]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
f g : R[X]
inst✝ : IsDomain R
hf₀ : f ≠ 0
hg : f.Splits
⊢ (f * g).Splits ↔ g.Splits

Tactic:
by
  simp [splits_mul', *]

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Algebra.IsIntegral R A
I : Ideal A
inst✝ : I.IsPrime
r : Ideal A
x✝ : (fun q ↦ q.IsPrime ∧ map (algebraMap R A) (under R I) ≤ q) r
hrq : r ≤ I
hr : r.IsPrime
hpr : map (algebraMap R A) (under R I) ≤ r
⊢ I ≤ r

Tactic:
contrapose! hpr

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Algebra.IsIntegral R A
I : Ideal A
inst✝ : I.IsPrime
r : Ideal A
x✝ : (fun q ↦ q.IsPrime ∧ map (algebraMap R A) (under R I) ≤ q) r
hrq : r ≤ I
hr : r.IsPrime
hpr : ¬I ≤ r
⊢ ¬map (algebraMap R A) (under R I) ≤ r
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

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

Tactic:
rw [subset_zeroLocus_iff_le_vanishingIdeal, vanishingIdeal_zeroLocus_eq_radical]

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

Goal state before:
pp: 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 = ⊤
⊢ ∀ z ∉ M, M < M + R ∙ z

Tactic:
intro z hz

Goal state after:
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 = ⊤
z : R
hz : z ∉ M
⊢ M < M + R ∙ z
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)
y' : S
z' : ↥S⁰
hx : (algebraMap S L) a * mk' L y' z' ∈ ↑(Ideal.span {(algebraMap S L) a})
y : S
z : R
hz0 : z ≠ 0
yz_eq : (algebraMap R S) z * y' = y * ↑z'
injRS : Function.Injective ⇑(algebraMap R S)
hz0' : (algebraMap R S) z ∈ S⁰
⊢ mk' L y' z' = mk' L y ⟨(algebraMap R S) z, hz0'⟩

Tactic:
mul_comm _ y'

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)
y' : S
z' : ↥S⁰
hx : (algebraMap S L) a * mk' L y' z' ∈ ↑(Ideal.span {(algebraMap S L) a})
y : S
z : R
hz0 : z ≠ 0
yz_eq : y' * (algebraMap R S) z = y * ↑z'
injRS : Function.Injective ⇑(algebraMap R S)
hz0' : (algebraMap R S) z ∈ S⁰
⊢ mk' L y' z' = mk' L y ⟨(algebraMap R S) z, hz0'⟩
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)
y' : S
z' : ↥S⁰
hx : (algebraMap S L) a * mk' L y' z' ∈ ↑(Ideal.span {(algebraMap S L) a})
y : S
z : R
hz0 : z ≠ 0
yz_eq : y' * (algebraMap R S) z = y * ↑z'
injRS : Function.Injective ⇑(algebraMap R S)
hz0' : (algebraMap R S) z ∈ S⁰
⊢ y * ↑z' = ↑⟨(algebraMap R S) z, hz0'⟩ * y'

Tactic:
mul_comm _ y',

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)
y' : S
z' : ↥S⁰
hx : (algebraMap S L) a * mk' L y' z' ∈ ↑(Ideal.span {(algebraMap S L) a})
y : S
z : R
hz0 : z ≠ 0
yz_eq : y' * (algebraMap R S) z = y * ↑z'
injRS : Function.Injective ⇑(algebraMap R S)
hz0' : (algebraMap R S) z ∈ S⁰
⊢ y * ↑z' = y' * ↑⟨(algebraMap R S) z, hz0'⟩
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

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

Tactic:
intro z hz

Goal state after:
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
M : Ideal A
hgt : ∀ J > M, J ≠ ⊥ → ∃ Z, (Multiset.map asIdeal Z).prod ≤ J ∧ (Multiset.map asIdeal Z).prod ≠ ⊥
h_nzI : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
h_prM : ¬M.IsPrime
x : A
hx : x ∉ M
y : A
hy : y ∉ M
h_xy : x * y ∈ M
z : A
hz : z ∉ M
⊢ M < M + A ∙ z
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✝² : FaithfullyFlat A B
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module A M
⊢ Function.Injective ⇑((TensorProduct.mk A B M) 1)

Tactic:
by
  rw [← Module.FaithfullyFlat.lTensor_injective_iff_injective A B]
  have : (lTensor B <| TensorProduct.mk A B M 1) =
      (TensorProduct.leftComm A B B M).symm.comp (TensorProduct.mk A B (B ⊗[A] M) 1) := by
    apply TensorProduct.ext'
    intro x y
    simp
  rw [this, coe_comp, LinearEquiv.coe_coe, EmbeddingLike.comp_injective]
  exact Algebra.TensorProduct.mk_one_injective_of_isScalarTower _

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

Goal state before:
pp: case intro
ι : Type u_3
R : ι → Type u_4
inst✝¹ : (i : ι) → CommRing (R i)
inst✝ : _root_.Finite ι
p : PrimeSpectrum ((i : ι) → R i)
val✝ : Fintype ι
e : ι → (i : ι) → R i := fun i ↦ Function.update 1 i 0
H : ∏ i, e i = 0
i : ι
hi : e i ∈ p.asIdeal
h₁ : Function.Surjective ⇑(Pi.evalRingHom R i) := RingHomSurjective.is_surjective
⊢ ∃ i q, comap (Pi.evalRingHom R i) q = p

Tactic:
have h₂ : RingHom.ker (Pi.evalRingHom R i) ≤ p.asIdeal := by
    intro x hx
    convert! p.asIdeal.mul_mem_left x hi
    ext j
    by_cases hj : i = j
    · subst hj; simpa [e]
    · simp [e, Function.update_of_ne (.symm hj)]

Goal state after:
case intro
ι : Type u_3
R : ι → Type u_4
inst✝¹ : (i : ι) → CommRing (R i)
inst✝ : _root_.Finite ι
p : PrimeSpectrum ((i : ι) → R i)
val✝ : Fintype ι
e : ι → (i : ι) → R i := fun i ↦ Function.update 1 i 0
H : ∏ i, e i = 0
i : ι
hi : e i ∈ p.asIdeal
h₁ : Function.Surjective ⇑(Pi.evalRingHom R i) := RingHomSurjective.is_surjective
h₂ : ker (Pi.evalRingHom R i) ≤ p.asIdeal
⊢ ∃ i q, comap (Pi.evalRingHom R i) q = p
Module: Mathlib.Topology.LocallyClosed

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set Y
hs : IsLocallyClosed s
f : X → Y
hf : Continuous[inst✝¹, inst✝] f
⊢ IsLocallyClosed (f ⁻¹' s)

Tactic:
obtain ⟨U, Z, hU, hZ, rfl⟩ := hs

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : Continuous[inst✝¹, inst✝] f
U Z : Set Y
hU : IsOpen[inst✝] U
hZ : IsClosed[inst✝] Z
⊢ IsLocallyClosed (f ⁻¹' (U ∩ Z))
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 : α
L M : BooleanSubalgebra α
h : (fun L ↦ L.carrier) L = (fun L ↦ L.carrier) M
⊢ L = M

Tactic:
by obtain ⟨⟨_, _⟩, _⟩ := L; congr

Goal state after:
Module: Mathlib.Topology.LocalAtTarget

Goal state before:
pp: case h₂
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
h : Continuous[inst✝¹, inst✝] f
⊢ IsClosed[inst✝] (range f) ↔
    ∀ (x : ι), IsClosed[instTopologicalSpaceSubtype] (range ((U x).carrier.restrictPreimage f))

Tactic:
simp_rw [range_restrictPreimage]
    exact hU.isClosed_iff_coe_preimage

Goal state after:
Module: Mathlib.Order.BooleanSubalgebra

Goal state before:
pp: α : Type u_2
inst✝ : BooleanAlgebra α
s : Set α
isSublattice : IsSublattice s
bot_mem : ⊥ ∈ s
top_mem : ⊤ ∈ s
p : (g : α) → g ∈ closure s → Prop
sdiff : ∀ (x : α) (hx : x ∈ s) (y : α) (hy : y ∈ s), p (x \ y) ⋯
sup : ∀ (x : α) (hx : x ∈ closure s) (y : α) (hy : y ∈ closure s), p x hx → p y hy → p (x ⊔ y) ⋯
x : α
hx : x ∈ closure s
⊢ p x hx

Tactic:
by
  obtain ⟨t, rfl⟩ := (mem_closure_iff_sup_sdiff isSublattice bot_mem top_mem).mp hx
  revert hx
  classical
  refine t.induction (by simpa using sdiff _ bot_mem _ bot_mem) fun x t _ ih hxt ↦ ?_
  simp only [Finset.sup_insert] at hxt ⊢
  exact sup _ _ _ ((mem_closure_iff_sup_sdiff isSublattice bot_mem top_mem).mpr ⟨_, rfl⟩)
    (sdiff _ x.1.2 _ x.2.2) (ih _)

Goal state after:
Module: Mathlib.Topology.Spectral.Prespectral

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PrespectralSpace Y
f : X → Y
hf : IsOpenEmbedding f
x : X
U : Set X
hx : x ∈ U
hU : IsOpen[inst✝²] U
⊢ ∃ v ∈ {U | IsOpen[inst✝²] U ∧ IsCompact U}, x ∈ v ∧ v ⊆ U

Tactic:
obtain ⟨V, ⟨hoV, hcV⟩, hfx, hVf⟩ : ∃ V ∈ {V | IsOpen V ∧ IsCompact V}, f x ∈ V ∧ V ⊆ f '' U :=
      (PrespectralSpace.isTopologicalBasis (X := Y)).isOpen_iff.mp
        (hf.isOpen_iff_image_isOpen.mp hU) (f x) ⟨x, hx, rfl⟩

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PrespectralSpace Y
f : X → Y
hf : IsOpenEmbedding f
x : X
U : Set X
hx : x ∈ U
hU : IsOpen[inst✝²] U
V : Set Y
hoV : IsOpen[inst✝¹] V
hcV : IsCompact V
hfx : f x ∈ V
hVf : V ⊆ f '' U
⊢ ∃ v ∈ {U | IsOpen[inst✝²] U ∧ IsCompact U}, x ∈ v ∧ v ⊆ U
Module: Mathlib.Topology.Spectral.Prespectral

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PrespectralSpace X
U V : Opens X
⊢ (∀ (W : CompactOpens X), ↑W ⊆ ↑U → ↑W ⊆ ↑V) → U ≤ V

Tactic:
intro H x hxU

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PrespectralSpace X
U V : Opens X
H : ∀ (W : CompactOpens X), ↑W ⊆ ↑U → ↑W ⊆ ↑V
x : X
hxU : x ∈ U
⊢ x ∈ V
Module: Mathlib.Topology.Sets.Compacts

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
⊢ Nontrivial (Compacts α) ↔ Nonempty α

Tactic:
← not_subsingleton_iff_nontrivial,

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
⊢ ¬Subsingleton (Compacts α) ↔ Nonempty α
Module: Mathlib.Topology.Sets.Compacts

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
⊢ Nontrivial (NonemptyCompacts α) ↔ Nontrivial α

Tactic:
← not_subsingleton_iff_nontrivial,

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
⊢ ¬Subsingleton (NonemptyCompacts α) ↔ ¬Subsingleton α
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set Y
hf : IsClosedEmbedding f
hf' : IsCompact (range f)ᶜ
hs : IsRetrocompact s
⊢ IsRetrocompact (f ⁻¹' s)

Tactic:
rintro U hUcomp hUopen
  have hfUopen : IsOpen (f '' U ∪ (range f)ᶜ) := by
    simpa [← range_sdiff_image hf.injective, sdiff_eq, compl_inter, union_comm]
      using (hf.isClosedMap _ hUopen.isClosed_compl).isOpen_compl
  have hfUcomp : IsCompact (f '' U ∪ (range f)ᶜ) := (hUcomp.image hf.continuous).union hf'
  simpa [inter_union_distrib_left, inter_left_comm, inter_eq_right.2 (image_subset_range ..),
    hf.isCompact_iff, image_preimage_inter] using (hs hfUcomp hfUopen).inter_left hf.isClosed_range

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

Goal state before:
pp: a b : ℕ
⊢ ((a.lcm b).factorization.prod fun p n ↦ if b.factorization p ≤ a.factorization p then p ^ n else 1).Coprime
    ((a.lcm b).factorization.prod fun p n ↦ if b.factorization p ≤ a.factorization p then 1 else p ^ n)

Tactic:
refine coprime_prod_left_iff.mpr fun p hp ↦ coprime_prod_right_iff.mpr fun q hq ↦ ?_

Goal state after:
a b p : ℕ
hp : p ∈ (a.lcm b).factorization.support
q : ℕ
hq : q ∈ (a.lcm b).factorization.support
⊢ ((fun p n ↦ if b.factorization p ≤ a.factorization p then p ^ n else 1) p ((a.lcm b).factorization p)).Coprime
    ((fun p n ↦ if b.factorization p ≤ a.factorization p then 1 else p ^ n) q ((a.lcm b).factorization q))
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
Zs : Set (Set (PrimeSpectrum R))
h : Zs ⊆ Set.range zeroLocus
f : ↑Zs → Set R
hf : ∀ (i : ↑Zs), zeroLocus (f i) = ↑i
⊢ ⋂ i, zeroLocus (f i) ∈ Set.range zeroLocus

Tactic:
exact ⟨_, zeroLocus_iUnion _⟩

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
a : K
n : ℤ
hn : ¬n = 0
ha : ¬a = 0
h : n = -↑n.natAbs
⊢ (-↑n.natAbs * a ^ (↑(n.natAbs - 1) - ↑(n.natAbs * 2))) • D a = (↑(-↑n.natAbs) * a ^ (-↑n.natAbs - 1)) • D a

Tactic:
congr 3

Goal state after:
case e_a.e_a
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
a : K
n : ℤ
hn : ¬n = 0
ha : ¬a = 0
h : n = -↑n.natAbs
⊢ -↑n.natAbs = ↑(-↑n.natAbs)

case e_a.e_a.e_a
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
a : K
n : ℤ
hn : ¬n = 0
ha : ¬a = 0
h : n = -↑n.natAbs
⊢ ↑(n.natAbs - 1) - ↑(n.natAbs * 2) = -↑n.natAbs - 1
Module: Mathlib.Data.ZMod.QuotientGroup

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : Group α
a : α
inst✝ : MulAction α β
b : β
k : ℤ
⊢ (orbitZPowersEquiv a b).symm ↑k = ⟨a, ⋯⟩ ^ k • ⟨b, ⋯⟩

Tactic:
orbitZPowersEquiv_symm_apply,

Goal state after:
α : Type u_3
β : Type u_4
inst✝¹ : Group α
a : α
inst✝ : MulAction α β
b : β
k : ℤ
⊢ ⟨a, ⋯⟩ ^ (↑k).cast • ⟨b, ⋯⟩ = ⟨a, ⋯⟩ ^ k • ⟨b, ⋯⟩
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: G : Type u_2
G' : Type u_3
inst✝³ : Group G
inst✝² : Group G'
F : Type u_4
inst✝¹ : FunLike F G' G
inst✝ : MonoidHomClass F G' G
f : F
hf : Function.Surjective ⇑f
x : G'
hx : Function.Surjective fun x_1 ↦ x ^ x_1
n : ℤ
⊢ ∃ a, (fun x_1 ↦ f x ^ x_1) a = f ((fun x_1 ↦ x ^ x_1) n)

Tactic:
exact ⟨n, (map_zpow _ _ _).symm⟩

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case refine_1
G : Type u_1
inst✝¹ : Monoid G
inst✝ : Nontrivial G
p : ℕ
hp : Nat.Prime p
hG : exponent G = p
g : G
hg : ¬g = 1
⊢ orderOf g = p

Tactic:
← orderOf_eq_one_iff

Goal state after:
case refine_1
G : Type u_1
inst✝¹ : Monoid G
inst✝ : Nontrivial G
p : ℕ
hp : Nat.Prime p
hG : exponent G = p
g : G
hg : ¬orderOf g = 1
⊢ orderOf g = p
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: 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)
p : ℕ
hp : Nat.Prime p
k : ℕ := (orderOf t).factorization p
hpe : k < (exponent G).factorization p
hk : k = (orderOf t).factorization p
g : G
hg : orderOf g = p ^ (exponent G).factorization p
this : sSup (Set.range orderOf) < orderOf (t ^ p ^ k * g)
⊢ False

Tactic:
exact this.not_ge (le_csSup hfin.bddAbove <| Set.mem_range_self _)

Goal state after:
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
inst✝ : Finite G
hGnt : Nontrivial G
k : ℕ
hk : Nat.card G = p ^ k
hk0 : k = 0
⊢ False

Tactic:
rw [hk0, pow_zero] at hk; exact Finite.one_lt_card.ne' hk

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
a b : { e // e.1 * e.2 = 0 ∧ e.1 + e.2 = 1 }
h : basicOpen ((↑a).1 * (↑b).1) = basicOpen (↑a).1
⊢ a ≤ b

Tactic:
← inf_eq_left

Goal state after:
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
a b : { e // e.1 * e.2 = 0 ∧ e.1 + e.2 = 1 }
h : basicOpen ((↑a).1 * (↑b).1) = basicOpen (↑a).1
⊢ a ⊓ b = a
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: α : Type u_1
G : Type u_2
G' : Type u_3
a : α
inst✝ : AddGroup G
g : G
hg : ∀ (x : G), x ∈ zmultiples g
n : ℕ
hn : Nat.card G = n
⊢ zmultiples ↑n = ((zmultiplesHom G) g).ker

Tactic:
zmultiplesHom_ker_eq,

Goal state after:
α : Type u_1
G : Type u_2
G' : Type u_3
a : α
inst✝ : AddGroup G
g : G
hg : ∀ (x : G), x ∈ zmultiples g
n : ℕ
hn : Nat.card G = n
⊢ zmultiples ↑n = zmultiples ↑(addOrderOf g)
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: case h.right
G : Type u_2
inst✝¹ : CommGroup G
inst✝ : IsSimpleGroup G
g : G
hg : zpowers g = ⊤
⊢ Nonempty (Additive G ≃+ ZMod (Nat.card G))

Tactic:
· exact ⟨(zmodAddCyclicAddEquiv (G := Additive G) inferInstance).symm⟩

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
hn : (normalizer ↑P).Normal
⊢ (↑P).Normal

Tactic:
by
  rw [← normalizer_eq_top_iff, ← normalizer_sup_eq_top' P le_normalizer, P.coe_coe, sup_idem]

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

Goal state before:
pp: case refine_1
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, ↑(μ i) = 1) ↔ (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
this : Std.Symm fun x1 x2 ↦ I x1 ⊔ I x2 = ⊤
μ : (i : ι) → ↥(⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ i), I j)
hμ : ∑ x ∈ t, ↑(μ x) + ↑(μ a) = 1
b : ι
hb : b ∈ ↑t
ab : a ≠ b
⊢ ∑ x ∈ t, ↑(μ x) ∈ I a

Tactic:
refine sum_mem _ fun x hx => ?_
        have := Submodule.coe_mem (μ x)
        simp only [mem_iInf] at this
        apply this _ (Finset.mem_cons_self _ _)
        rintro rfl
        exact hat hx

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

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSemisimpleModule R M
s : Set (Submodule R M)
ind : iSupIndep Subtype.val
sSup : SupSet.sSup s = ⊤
simple : ∀ m ∈ s, IsSimpleModule R ↥m
⊢ ((DFinsupp.lsum ℕ) fun i ↦ (↑i).subtype).range = ⊤

Tactic:
← Submodule.iSup_eq_range_dfinsupp_lsum,

Goal state after:
R : Type u_2
inst✝³ : Ring R
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSemisimpleModule R M
s : Set (Submodule R M)
ind : iSupIndep Subtype.val
sSup : SupSet.sSup s = ⊤
simple : ∀ m ∈ s, IsSimpleModule R ↥m
⊢ iSup Subtype.val = ⊤
Module: Mathlib.Algebra.Polynomial.Module.Basic

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
⊢ single R n 0 = 0

Tactic:
by simp [single]

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Nakayama

Goal state before:
pp: case insert
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s✝ : Set M
i : M
s : Set M
a✝ : i ∉ s
hs✝ : s.Finite
ih :
  (∃ r, r - 1 ∈ I ∧ N ≤ comap ((LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) → ∃ r, r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0
H : ∃ r, r - 1 ∈ I ∧ N ≤ comap ((LinearMap.lsmul R M) r) (I • span R (insert i s)) ∧ insert i s ⊆ ↑N
⊢ ∃ r, r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0

Tactic:
apply ih

Goal state after:
case insert
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s✝ : Set M
i : M
s : Set M
a✝ : i ∉ s
hs✝ : s.Finite
ih :
  (∃ r, r - 1 ∈ I ∧ N ≤ comap ((LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) → ∃ r, r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0
H : ∃ r, r - 1 ∈ I ∧ N ≤ comap ((LinearMap.lsmul R M) r) (I • span R (insert i s)) ∧ insert i s ⊆ ↑N
⊢ ∃ r, r - 1 ∈ I ∧ N ≤ comap ((LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N
Module: Mathlib.RingTheory.ReesAlgebra

Goal state before:
pp: R : Type u
inst✝ : CommRing R
I : Ideal R
s : Finset R
hs : Ideal.span ↑s = I
⊢ (reesAlgebra I).FG

Tactic:
rw [← adjoin_monomial_eq_reesAlgebra, ← hs]

Goal state after:
R : Type u
inst✝ : CommRing R
I : Ideal R
s : Finset R
hs : Ideal.span ↑s = I
⊢ (Algebra.adjoin R ↑(Submodule.map (monomial 1) (Ideal.span ↑s))).FG
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: case mp
R : Type u
inst✝ : CommRing R
I : Ideal R
H : Subsingleton I.Cotangent
⊢ IsIdempotentElem I

Tactic:
refine (pow_two I).symm.trans (le_antisymm (Ideal.pow_le_self two_ne_zero) ?_)

Goal state after:
case mp
R : Type u
inst✝ : CommRing R
I : Ideal R
H : Subsingleton I.Cotangent
⊢ I ≤ I ^ 2