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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
I J : Ideal S
inst✝ : I.IsPrime
hIJ : I ≤ J
r : S
hr : r ∈ ↑J \ ↑I
p : R[X]
p_ne_zero : Polynomial.map (Quotient.mk (comap f I)) p ≠ 0
hpI : eval₂ f r p ∈ I
⊢ ∃ i, p.coeff i ∈ ↑(comap f J) \ ↑(comap f I)

Tactic:
by
  obtain ⟨hrJ, hrI⟩ := hr
  have rbar_ne_zero : Ideal.Quotient.mk I r ≠ 0 := mt (Quotient.mk_eq_zero I).mp hrI
  have rbar_mem_J : Ideal.Quotient.mk I r ∈ J.map (Ideal.Quotient.mk I) := mem_map_of_mem _ hrJ
  have quotient_f : ∀ x ∈ I.comap f, (Ideal.Quotient.mk I).comp f x = 0 := by
    simp [Quotient.eq_zero_iff_mem]
  have rbar_root :
    (p.map (Ideal.Quotient.mk (I.comap f))).eval₂ (Quotient.lift (I.comap f) _ quotient_f)
        (Ideal.Quotient.mk I r) =
      0 := by
    convert! Quotient.eq_zero_iff_mem.mpr hpI
    exact _root_.trans (eval₂_map _ _ _) (hom_eval₂ p f (Ideal.Quotient.mk I) r).symm
  obtain ⟨i, ne_zero, mem⟩ :=
    exists_coeff_ne_zero_mem_comap_of_root_mem rbar_ne_zero rbar_mem_J p_ne_zero rbar_root
  rw [coeff_map] at ne_zero mem
  refine ⟨i, (mem_quotient_iff_mem hIJ).mp ?_, mt ?_ ne_zero⟩
  · simpa using mem
  simp [Quotient.eq_zero_iff_mem]

Goal state after:
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✝² : IsDomain S
inst✝¹ : Algebra.IsIntegral R S
P : Ideal R
inst✝ : P.IsPrime
hP : RingHom.ker (algebraMap R S) ≤ P
hP0 : 0 ∉ Algebra.algebraMapSubmonoid S P.primeCompl
Rₚ : Type u_1 := Localization P.primeCompl
Sₚ : Type u_2 := Localization (Algebra.algebraMapSubmonoid S P.primeCompl)
this✝ : IsDomain (Localization (Algebra.algebraMapSubmonoid S P.primeCompl)) :=
  IsLocalization.isDomain_localization (le_nonZeroDivisors_of_noZeroDivisors hP0)
Qₚ : Ideal Sₚ
Qₚ_maximal : Qₚ.IsMaximal
this : Algebra.IsIntegral Rₚ Sₚ
Qₚ_max : (comap (algebraMap Rₚ Sₚ) Qₚ).IsMaximal
⊢ comap (algebraMap R S) (comap (algebraMap S Sₚ) Qₚ) = under R (IsLocalRing.maximalIdeal (Localization P.primeCompl))

Tactic:
comap_comap,

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : Algebra.IsIntegral R S
P : Ideal R
inst✝ : P.IsPrime
hP : RingHom.ker (algebraMap R S) ≤ P
hP0 : 0 ∉ Algebra.algebraMapSubmonoid S P.primeCompl
Rₚ : Type u_1 := Localization P.primeCompl
Sₚ : Type u_2 := Localization (Algebra.algebraMapSubmonoid S P.primeCompl)
this✝ : IsDomain (Localization (Algebra.algebraMapSubmonoid S P.primeCompl)) :=
  IsLocalization.isDomain_localization (le_nonZeroDivisors_of_noZeroDivisors hP0)
Qₚ : Ideal Sₚ
Qₚ_maximal : Qₚ.IsMaximal
this : Algebra.IsIntegral Rₚ Sₚ
Qₚ_max : (comap (algebraMap Rₚ Sₚ) Qₚ).IsMaximal
⊢ comap ((algebraMap S Sₚ).comp (algebraMap R S)) Qₚ = under R (IsLocalRing.maximalIdeal (Localization P.primeCompl))
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
inst✝ : IsReduced R
x✝ : ∃ y, y ≠ 0 ∧ IsIntegral R (y • z)
w✝ : R
hy : w✝ ≠ 0
int : IsIntegral R (w✝ • z)
⊢ ¬IsNilpotent w✝

Tactic:
rwa [isNilpotent_iff_eq_zero]

Goal state after:
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
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
inst✝ : NoZeroDivisors S
int : Algebra.IsIntegral R S
a : A
h : IsAlgebraic S a
hRS : Function.Injective ⇑(algebraMap R S)
this : NoZeroDivisors R
s : S
hs : s ≠ 0
int_s : IsIntegral S (s • a)
h✝ : Nontrivial R
r : R
hr : r ≠ 0
w✝ : S
e : (algebraMap R S) r = s * w✝
⊢ ¬IsNilpotent r

Tactic:
rwa [isNilpotent_iff_eq_zero]

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
⊢ zeroLocus ↑0 = Set.univ

Tactic:
Ideal.zero_eq_bot,

Goal state after:
R : Type u
inst✝ : CommSemiring R
⊢ zeroLocus ↑⊥ = Set.univ
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x : PrimeSpectrum R
⊢ IsMax x ↔ x.asIdeal.IsMaximal

Tactic:
refine ⟨fun hx ↦ ⟨⟨x.2.ne_top, fun I hI ↦ ?_⟩⟩, fun hx y e ↦ (hx.eq_of_le y.2.ne_top e).ge⟩

Goal state after:
R : Type u
inst✝ : CommSemiring R
x : PrimeSpectrum R
hx : IsMax x
I : Ideal R
hI : x.asIdeal < I
⊢ I = ⊤
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
⊢ m = 0

Tactic:
let f : R →ₗ[R] M := (LinearMap.lsmul R M).flip m

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
⊢ m = 0
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
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
inst✝¹ : NoZeroDivisors S
a : A
inst✝ : Algebra.IsAlgebraic R S
ha : IsAlgebraic S a
⊢ IsAlgebraic R a

Tactic:
exact ha.restrictScalars _

Goal state after:
Module: Mathlib.Topology.Compactness.Bases

Goal state before:
pp: case refine_1
X : Type u_1
ι : Type u_2
inst✝ : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
U : Set X
hUc : IsCompact U
hUo : IsOpen U
Y : Type u_1
f' : Y → ι
e : U = ⋃ i, (b ∘ f') i
hf' : ∀ (i : Y), b (f' i) = (b ∘ f') i
t : Finset Y
ht : U ⊆ ⋃ i ∈ t, (b ∘ f') i
⊢ U ⊆ ⋃ i ∈ ↑(Finset.image f' t), b i

pp: case refine_2
X : Type u_1
ι : Type u_2
inst✝ : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
U : Set X
hUc : IsCompact U
hUo : IsOpen U
Y : Type u_1
f' : Y → ι
e : U = ⋃ i, (b ∘ f') i
hf' : ∀ (i : Y), b (f' i) = (b ∘ f') i
t : Finset Y
ht : U ⊆ ⋃ i ∈ t, (b ∘ f') i
⊢ ⋃ i ∈ ↑(Finset.image f' t), b i ⊆ U

Tactic:
· refine Set.Subset.trans ht ?_
    simp only [Set.iUnion_subset_iff]
    intro i hi
    simpa using subset_iUnion₂ (s := fun i _ => b (f' i)) i hi

Goal state after:
case refine_2
X : Type u_1
ι : Type u_2
inst✝ : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
U : Set X
hUc : IsCompact U
hUo : IsOpen U
Y : Type u_1
f' : Y → ι
e : U = ⋃ i, (b ∘ f') i
hf' : ∀ (i : Y), b (f' i) = (b ∘ f') i
t : Finset Y
ht : U ⊆ ⋃ i ∈ t, (b ∘ f') i
⊢ ⋃ i ∈ ↑(Finset.image f' t), b i ⊆ U
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
max : Ideal R
hmax : max.IsMaximal
n d : R
hd : d ∈ { asIdeal := max, isMaximal := hmax }.asIdeal.primeCompl
hrange : (algebraMap R K) n * ((algebraMap R K) d)⁻¹ ∉ range ⇑(algebraMap R K)
hlocal :
  ∀ (i : MaximalSpectrum R),
    (algebraMap R K) n * ((algebraMap R K) d)⁻¹ ∈ Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯
denom : Ideal R := Submodule.comap (LinearMap.toSpanSingleton R K ((algebraMap R K) n * ((algebraMap R K) d)⁻¹)) 1
hdenom : 1 ∉ denom
hle : denom ≤ max
⊢ (LinearMap.toSpanSingleton R K 1) n = (LinearMap.toSpanSingleton R K ((algebraMap R K) n * ((algebraMap R K) d)⁻¹)) d

Tactic:
by simp [Algebra.smul_def, mul_left_comm, mul_inv_cancel₀ <|
      (map_ne_zero_iff _ <| IsFractionRing.injective R K).mpr fun h ↦ hd (h ▸ max.zero_mem :)]

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
⊢ ⨅ v, Localization.subalgebra.ofField K v.asIdeal.primeCompl ⋯ = ⊥

Tactic:
refine bot_unique (.trans (fun _ ↦ ?_) (MaximalSpectrum.iInf_localization_eq_bot R K).le)

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✝ ∈ ⨅ v, Localization.subalgebra.ofField K v.asIdeal.primeCompl ⋯
Module: Mathlib.Topology.LocalAtTarget

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
h : ∀ (x : α), 𝓝 x = comap f (𝓝 (f x))
a : ↑(f ⁻¹' s)
⊢ 𝓝 a = comap Subtype.val (comap f (𝓝 (f ↑a)))

Tactic:
rw [← h, ← IsInducing.subtypeVal.nhds_eq_comap]

Goal state after:
Module: Mathlib.Topology.LocalAtTarget

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
H : IsOpenMap f
s : Set β
⊢ IsOpenMap (s.restrictPreimage f)

Tactic:
by
  intro t
  suffices ∀ u, IsOpen u → Subtype.val ⁻¹' u = t →
    ∃ v, IsOpen v ∧ Subtype.val ⁻¹' v = s.restrictPreimage f '' t by
      simpa [isOpen_induced_iff]
  exact fun u hu e => ⟨f '' u, H u hu, by simp [← e, image_restrictPreimage]⟩

Goal state after:
Module: Mathlib.Topology.LocallyClosed

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
tfae_1_to_2 : IsLocallyClosed s → IsOpen[inst✝] (coborder s)
tfae_2_to_3 : IsOpen[inst✝] (coborder s) → ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)
h : ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)
x : X
hx : x ∈ s
t : Set X
ht : t ∈ 𝓝 x
ht' : IsClosed[instTopologicalSpaceSubtype] (t ↓∩ s)
⊢ ∃ U, x ∈ U ∧ IsOpen[inst✝] U ∧ U ∩ closure[inst✝] s ⊆ s

Tactic:
obtain ⟨U, hUt, hU, hxU⟩ := mem_nhds_iff.mp ht

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
tfae_1_to_2 : IsLocallyClosed s → IsOpen[inst✝] (coborder s)
tfae_2_to_3 : IsOpen[inst✝] (coborder s) → ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)
h : ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)
x : X
hx : x ∈ s
t : Set X
ht : t ∈ 𝓝 x
ht' : IsClosed[instTopologicalSpaceSubtype] (t ↓∩ s)
U : Set X
hUt : U ⊆ t
hU : IsOpen[inst✝] U
hxU : x ∈ U
⊢ ∃ U, x ∈ U ∧ IsOpen[inst✝] U ∧ U ∩ closure[inst✝] s ⊆ s
Module: Mathlib.Topology.Sets.Compacts

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α ≃ₜ β
s : Compacts α
⊢ ↑(Compacts.map ⇑f.symm ⋯ (Compacts.map ⇑f ⋯ s)) = ↑s

Tactic:
simp only [coe_map, ← image_comp, f.symm_comp_self, image_id]

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

Goal state before:
pp: case neg
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra.HasGoingDown R S
p : Ideal R
inst✝³ : p.IsPrime
Q : Ideal S
inst✝² : Q.IsPrime
inst✝¹ : (under R Q).IsPrime
inst✝ : Q.LiesOver (under R Q)
hle : p ≤ under R Q
h : ¬p = under R Q
⊢ ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p

Tactic:
exact Algebra.HasGoingDown.exists_ideal_le_liesOver_of_lt Q (lt_of_le_of_ne hle h)

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

Goal state before:
pp: case refine_3
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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hI : I ^ 2 = ⊥
f : A →ₐ[R] B
e : (Ideal.Quotient.mkₐ R I).comp f = IsScalarTower.toAlgHom R A (B ⧸ I)
x y : A
F : A →ₗ[R] ↥I := diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B) ⋯
this : f x * f y = 0 + (f x * (algebraMap A B) y - (algebraMap A B) x * (algebraMap A B) y) + (algebraMap A B) x * f y
⊢ f x * f y - (algebraMap A B) x * (algebraMap A B) y =
    (algebraMap A B) x * f y - (algebraMap A B) x * (algebraMap A B) y +
      ((algebraMap A B) y * f x - (algebraMap A B) y * (algebraMap A B) x)

Tactic:
simp only [this]

Goal state after:
case refine_3
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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hI : I ^ 2 = ⊥
f : A →ₐ[R] B
e : (Ideal.Quotient.mkₐ R I).comp f = IsScalarTower.toAlgHom R A (B ⧸ I)
x y : A
F : A →ₗ[R] ↥I := diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B) ⋯
this : f x * f y = 0 + (f x * (algebraMap A B) y - (algebraMap A B) x * (algebraMap A B) y) + (algebraMap A B) x * f y
⊢ 0 + (f x * (algebraMap A B) y - (algebraMap A B) x * (algebraMap A B) y) + (algebraMap A B) x * f y -
      (algebraMap A B) x * (algebraMap A B) y =
    (algebraMap A B) x * f y - (algebraMap A B) x * (algebraMap A B) y +
      ((algebraMap A B) y * f x - (algebraMap A B) y * (algebraMap A B) x)
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case h_open
R : Type u
inst✝ : CommSemiring R
⊢ ∀ u ∈ Set.range fun r ↦ ↑(basicOpen r), IsOpen u

pp: case h_nhds
R : Type u
inst✝ : CommSemiring R
⊢ ∀ (a : PrimeSpectrum R) (u : Set (PrimeSpectrum R)),
    a ∈ u → IsOpen u → ∃ v ∈ Set.range fun r ↦ ↑(basicOpen r), a ∈ v ∧ v ⊆ u

Tactic:
· rintro _ ⟨r, rfl⟩
    exact isOpen_basicOpen

Goal state after:
case h_nhds
R : Type u
inst✝ : CommSemiring R
⊢ ∀ (a : PrimeSpectrum R) (u : Set (PrimeSpectrum R)),
    a ∈ u → IsOpen u → ∃ v ∈ Set.range fun r ↦ ↑(basicOpen r), a ∈ v ∧ v ⊆ u
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
H : Subgroup α
⊢ (∃ a, ∃ (b : a ∈ H), zpowers (H.subtype ⟨a, b⟩) = H) ↔ ∃ g, zpowers g = H

Tactic:
coe_subtype,

Goal state after:
α : Type u_1
inst✝ : Group α
H : Subgroup α
⊢ (∃ a, ∃ (_ : a ∈ H), zpowers a = H) ↔ ∃ g, zpowers g = H
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 : α
h : x ∈ ⊥
⊢ 1 ∈ H

Tactic:
exact H.one_mem

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
x : R
⊢ (∀ (a : PrimeSpectrum S), f x ∈ a.asIdeal) ↔ ∀ (p : Submodule S S), Ideal.IsPrime p → f x ∈ p

Tactic:
exact ⟨fun H I hI ↦ H ⟨I, hI⟩, fun H I ↦ H I.1 I.2⟩

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
⊢ zeroLocus ↑(RingHom.ker f) = Set.univ ↔ RingHom.ker f ≤ nilradical R

Tactic:
zeroLocus_eq_univ_iff,

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
⊢ ↑(RingHom.ker f) ⊆ ↑(nilradical R) ↔ RingHom.ker f ≤ nilradical R
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
hs : IsClopen s
h✝ : Nontrivial R
I : Ideal R
hI : I.FG
J : Ideal R
hJ : J.FG
hI' : zeroLocus ↑I = sᶜ
hJ' : zeroLocus ↑J = s
⊢ zeroLocus ↑(I * J) = zeroLocus ↑0

Tactic:
Ideal.zero_eq_bot,

Goal state after:
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
hs : IsClopen s
h✝ : Nontrivial R
I : Ideal R
hI : I.FG
J : Ideal R
hJ : J.FG
hI' : zeroLocus ↑I = sᶜ
hJ' : zeroLocus ↑J = s
⊢ zeroLocus ↑(I * J) = zeroLocus ↑⊥
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: case inl
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
h : IsPGroup 0 G
⊢ ∃ n, Nat.card G ∣ 0 ^ n

pp: case inr
p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
h : IsPGroup p G
hp : p ≠ 0
⊢ ∃ n, Nat.card G ∣ p ^ n

Tactic:
· exact ⟨1, by simp⟩

Goal state after:
case inr
p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
h : IsPGroup p G
hp : p ≠ 0
⊢ ∃ n, Nat.card G ∣ p ^ n
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: case refine_2
p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
h : p ≠ 0
hG : (Nat.card G).primeFactors ⊆ p.primeFactors
⊢ ∃ n, Nat.card G ∣ p ^ n

Tactic:
· refine ⟨Nat.card G, Nat.dvd_prod_primeFactors_pow_self NeZero.out |>.trans ?_⟩
    grw [Finset.prod_dvd_prod_of_subset _ _ (·) hG, p.prod_primeFactors_dvd]

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
hs : IsClopen s
⊢ ∃! e, IsIdempotentElem e ∧ s = ↑(basicOpen e)

Tactic:
refine existsUnique_of_exists_of_unique (exists_idempotent_basicOpen_eq_of_isClopen hs) ?_

Goal state after:
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
hs : IsClopen s
⊢ ∀ (y₁ y₂ : R), IsIdempotentElem y₁ ∧ s = ↑(basicOpen y₁) → IsIdempotentElem y₂ ∧ s = ↑(basicOpen y₂) → y₁ = y₂
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case refine_1.snd
M₁ : Type u_1
M₂ : Type u_2
inst✝¹ : Monoid M₁
inst✝ : Monoid M₂
g : M₁ × M₂
⊢ (g ^ GCDMonoid.lcm (exponent M₁) (exponent M₂)).2 = 1.2

Tactic:
· rw [Prod.pow_snd, Prod.snd_one, ← orderOf_dvd_iff_pow_eq_one]
      exact dvd_trans (Monoid.order_dvd_exponent (g.2)) <| dvd_lcm_right _ _

Goal state after:
Module: Mathlib.GroupTheory.Torsion

Goal state before:
pp: G : Type u_1
inst✝ : CommMonoid G
p : ℕ
hp : Fact (Nat.Prime p)
g : ↥(primaryComponent G p)
⊢ ↑g ∈ primaryComponent G p

Tactic:
exact g.property

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: G : Type u_2
inst✝² : CommGroup G
inst✝¹ : IsCyclic G
inst✝ : Finite G
d : ℕ
⊢ (powMonoidHom d).range.index = (Nat.card G).gcd d

Tactic:
rw [Subgroup.index_range, card_powMonoidHom_ker]

Goal state after:
Module: Mathlib.Order.CompactlyGenerated.Intervals

Goal state before:
pp: α : Type u_2
inst✝ : CompleteLattice α
a : α
b : ↑(Iic a)
h : ∀ (ι : Type u_2) (s : ι → α), ↑b ≤ iSup s → ∃ t, ↑b ≤ ⨆ a ∈ t, s a
ι : Type u_2
s : ι → ↑(Iic a)
hb : ↑b ≤ iSup (Subtype.val ∘ s)
t : Finset ι
ht : ↑b ≤ ⨆ a_1 ∈ t, (Subtype.val ∘ s) a_1
⊢ ↑b ≤ ↑(⨆ a_1 ∈ t, s a_1)

Tactic:
by simpa using ht

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

Goal state before:
pp: ι : 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μ : ↑(μ a) + ∑ x ∈ t, ↑(μ x) = 1
⊢ ↑(μ a) ∈ ⨅ j ∈ t, ⨅ (_ : j ≠ Exists.choose h), I j

Tactic:
have := Submodule.coe_mem (μ a)
      rw [mem_iInf] at this ⊢
      --for some reason `simp only [mem_iInf]` times out
      intro i
      specialize this i
      rw [mem_iInf, mem_iInf] at this ⊢
      intro hi _
      apply this (Finset.subset_cons _ hi)
      rintro rfl
      exact hat hi

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

Goal state before:
pp: ι : 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μ✝ : ↑(μ a) + ∑ x ∈ t, ↑(μ x) = 1
hμ : (if Exists.choose h ∈ t then ↑(μ a) else 0) + ∑ x ∈ t, ↑(μ x) = 1
⊢ ∑ i ∈ t, ↑((Pi.single (Exists.choose h) ⟨↑(μ a), ⋯⟩ + fun i ↦ ⟨↑(μ i), ⋯⟩) i) = 1

pp: ι : 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μ : ↑(μ a) + ∑ x ∈ t, ↑(μ x) = 1
⊢ Decidable (Exists.choose h ∈ t)

Tactic:
← Finset.sum_pi_single',

Goal state after:
ι : 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μ✝ : ↑(μ a) + ∑ x ∈ t, ↑(μ x) = 1
hμ : ∑ a' ∈ t, Pi.single (Exists.choose h) (↑(μ a)) a' + ∑ x ∈ t, ↑(μ x) = 1
⊢ ∑ i ∈ t, ↑((Pi.single (Exists.choose h) ⟨↑(μ a), ⋯⟩ + fun i ↦ ⟨↑(μ i), ⋯⟩) i) = 1
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
this : (normalizer ↑↑(P.subtype ⋯)).Normal → (↑(P.subtype ⋯)).Normal
⊢ normalizer ↑(normalizer ↑P) = normalizer ↑P

Tactic:
coe_subtype,

Goal state after:
G : Type u
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
this :
  (normalizer ↑((↑P).subgroupOf (normalizer ↑(normalizer ↑↑P)))).Normal →
    ((↑P).subgroupOf (normalizer ↑(normalizer ↑↑P))).Normal
⊢ normalizer ↑(normalizer ↑P) = normalizer ↑P
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
i : Fin (s.length + 1)
hx : s.toFun i ∈ s
j : Fin (s.length + 1)
hy : s.toFun j ∈ s
⊢ s.toFun i ≤ s.toFun j ∨ s.toFun j ≤ s.toFun i

Tactic:
s.strictMono.le_iff_le,

Goal state after:
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
i : Fin (s.length + 1)
hx : s.toFun i ∈ s
j : Fin (s.length + 1)
hy : s.toFun j ∈ s
⊢ i ≤ j ∨ s.toFun j ≤ s.toFun i
Module: Mathlib.RingTheory.Coprime.Ideal

Goal state before:
pp: case refine_2.mpr.refine_3
ι : 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 = ⊤
hs : (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
Hb : ∀ b ∈ ↑t, a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → ↥(⨅ j ∈ t, ⨅ (_ : j ≠ i), I j)
hμ : ∑ i ∈ t, ↑(μ i) = 1
u : R
hu : u ∈ I a
v : R
hv : v ∈ ⨅ i ∈ t, I i
huv : u + v = 1
⊢ ∑ i ∈ Finset.cons a t hat, ↑(if hi : i = a then ⟨v, ⋯⟩ else ⟨u * ↑(μ i), ⋯⟩) = 1

Tactic:
Finset.sum_cons,

Goal state after:
case refine_2.mpr.refine_3
ι : 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 = ⊤
hs : (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
Hb : ∀ b ∈ ↑t, a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → ↥(⨅ j ∈ t, ⨅ (_ : j ≠ i), I j)
hμ : ∑ i ∈ t, ↑(μ i) = 1
u : R
hu : u ∈ I a
v : R
hv : v ∈ ⨅ i ∈ t, I i
huv : u + v = 1
⊢ ↑(if hi : a = a then ⟨v, ⋯⟩ else ⟨u * ↑(μ a), ⋯⟩) + ∑ x ∈ t, ↑(if hi : x = a then ⟨v, ⋯⟩ else ⟨u * ↑(μ x), ⋯⟩) = 1
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: case a
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : (↑S).Pairwise fun i j ↦ p i ⊔ p j = ⊤
h : S.Nonempty
⊢ torsionBySet R M ↑(⨅ i ∈ S, p i) ≤ ⨆ i ∈ S, torsionBySet R M ↑(p i)

Tactic:
intro x hx
    rw [mem_iSup_finset_iff_exists_sum]
    obtain ⟨μ, hμ⟩ :=
      (mem_iSup_finset_iff_exists_sum _ _).mp
        ((Ideal.eq_top_iff_one _).mp <| (Ideal.iSup_iInf_eq_top_iff_pairwise h _).mpr hp)
    refine ⟨fun i => ⟨(μ i : R) • x, ?_⟩, ?_⟩
    · rw [mem_torsionBySet_iff] at hx ⊢
      rintro ⟨a, ha⟩
      rw [smul_smul]
      suffices a * μ i ∈ ⨅ i ∈ S, p i from hx ⟨_, this⟩
      rw [mem_iInf]
      intro j
      rw [mem_iInf]
      intro hj
      by_cases ij : j = i
      · rw [ij]
        exact Ideal.mul_mem_right _ _ ha
      · have := coe_mem (μ i)
        simp only [mem_iInf] at this
        exact Ideal.mul_mem_left _ _ (this j hj ij)
    · rw [← Finset.sum_smul, hμ, one_smul]

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
I : Ideal R
x : R
hx : x ∈ I
m : I.Cotangent
⊢ x • m = 0

Tactic:
obtain ⟨m, rfl⟩ := Ideal.toCotangent_surjective _ m

Goal state after:
R : Type u
inst✝ : CommRing R
I : Ideal R
x : R
hx : x ∈ I
m : ↥I
⊢ x • I.toCotangent m = 0