mathlib-initiative/mathlib-tactics huggingface dataset:
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
s : Finset n
e : ↥s ⊕ { a // a ∉ s } ≃ n := Equiv.sumCompl fun x ↦ x ∈ s
A : Matrix n n R := of (s.piecewise M 1)
⊢ A.det = (M.submatrix Subtype.val Subtype.val).det

Tactic:
← Matrix.det_submatrix_equiv_self e A

Goal state after:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
s : Finset n
e : ↥s ⊕ { a // a ∉ s } ≃ n := Equiv.sumCompl fun x ↦ x ∈ s
A : Matrix n n R := of (s.piecewise M 1)
⊢ (A.submatrix ⇑e ⇑e).det = (M.submatrix Subtype.val Subtype.val).det
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 : ℕ
D : (n → R[X]) [⋀^n]→ₗ[R[X]] R[X] := detRowAlternating
h_map : ∀ (s : Finset n), (s.piecewise (fun i ↦ M.map (⇑C) i) fun i ↦ 1 i) = map (s.piecewise M 1) ⇑C
h_det : ∀ (s : Finset n), D (s.piecewise (fun i ↦ M.map (⇑C) i) fun i ↦ 1 i) = C (det (s.piecewise M 1))
s : Finset n
n✝ : ℕ
⊢ (s.piecewise (fun i ↦ (X • M.map ⇑C) i) fun i ↦ 1 i) = fun i ↦
    (if i ∈ s then X else 1) • s.piecewise (fun i ↦ M.map (⇑C) i) (fun i ↦ 1 i) i

Tactic:
funext i j

Goal state after:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
D : (n → R[X]) [⋀^n]→ₗ[R[X]] R[X] := detRowAlternating
h_map : ∀ (s : Finset n), (s.piecewise (fun i ↦ M.map (⇑C) i) fun i ↦ 1 i) = map (s.piecewise M 1) ⇑C
h_det : ∀ (s : Finset n), D (s.piecewise (fun i ↦ M.map (⇑C) i) fun i ↦ 1 i) = C (det (s.piecewise M 1))
s : Finset n
n✝ : ℕ
i j : n
⊢ s.piecewise (fun i ↦ (X • M.map ⇑C) i) (fun i ↦ 1 i) i j =
    ((if i ∈ s then X else 1) • s.piecewise (fun i ↦ M.map (⇑C) i) (fun i ↦ 1 i) i) j
Module: Mathlib.RingTheory.Polynomial.ScaleRoots

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
x : R
f : R →+* S
h : f p.leadingCoeff ≠ 0
⊢ map f (p.scaleRoots x) = (map f p).scaleRoots (f x)

Tactic:
by
  ext
  simp [Polynomial.natDegree_map_of_leadingCoeff_ne_zero _ h]

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

Goal state before:
pp: case pos
R : Type u
inst✝¹ : Semiring R
A : Type u_1
inst✝ : Semiring A
p : R[X]
f : R →+* A
z : A
hz : eval₂ f z p = 0
h₁ : Commute (f p.leadingCoeff) z
h₂ : ∀ {r r' : R}, Commute (f r) (f r')
inj : ∀ (x : R), f x = 0 → x = 0
h : p.natDegree = 0
h0 : p.coeff 0 = 0
⊢ eval₂ f (f (C (p.coeff 0)).leadingCoeff * z) (C (p.coeff 0)).integralNormalization = 0

Tactic:
simp [h0]

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

Goal state before:
pp: case e
R : Type u_1
B : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring B
inst✝ : Algebra R B
x y : B
r : R
hr : y * (algebraMap R B) r = 1
p : R[X]
p_monic : p.Monic
hp : eval₂ (algebraMap R B) (x * y) p = 0
⊢ eval₂ (algebraMap R B) x = ⇑(aeval (x * y * (algebraMap R B) r))

Tactic:
rw [mul_assoc, hr, mul_one]

Goal state after:
case e
R : Type u_1
B : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring B
inst✝ : Algebra R B
x y : B
r : R
hr : y * (algebraMap R B) r = 1
p : R[X]
p_monic : p.Monic
hp : eval₂ (algebraMap R B) (x * y) p = 0
⊢ eval₂ (algebraMap R B) x = ⇑(aeval x)
Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

Goal state before:
pp: case mp
S : Type u_4
inst✝ : CommRing S
g✝ : S[X]
mon : g✝.Monic
I : Ideal S[X]
h : g✝ ∈ I
g : S[X] ⧸ I
⊢ g ∈ S[(Ideal.Quotient.mkₐ S I) X] → g ∈ ⊤

pp: case mpr
S : Type u_4
inst✝ : CommRing S
g✝ : S[X]
mon : g✝.Monic
I : Ideal S[X]
h : g✝ ∈ I
g : S[X] ⧸ I
⊢ g ∈ ⊤ → g ∈ S[(Ideal.Quotient.mkₐ S I) X]

Tactic:
· simp only [Algebra.mem_top, implies_true]

Goal state after:
case mpr
S : Type u_4
inst✝ : CommRing S
g✝ : S[X]
mon : g✝.Monic
I : Ideal S[X]
h : g✝ ∈ I
g : S[X] ⧸ I
⊢ g ∈ ⊤ → g ∈ S[(Ideal.Quotient.mkₐ S I) X]
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
a✝ : Nontrivial S
φ : R[X] →ₐ[R] S := aeval s
p : (↥R[s])[X]
hpm : p.Monic
hpt : eval₂ (algebraMap (↥R[s]) S) t p = 0
this : Polynomial.map (algebraMap (↥R[s]) S) p ∈ lifts φ.toRingHom
⊢ φ.IsIntegralElem t

Tactic:
obtain ⟨q, hqp, hqd, hqm⟩ := lifts_and_degree_eq_and_monic this (hpm.map _)

Goal state after:
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
a✝ : Nontrivial S
φ : R[X] →ₐ[R] S := aeval s
p : (↥R[s])[X]
hpm : p.Monic
hpt : eval₂ (algebraMap (↥R[s]) S) t p = 0
this : Polynomial.map (algebraMap (↥R[s]) S) p ∈ lifts φ.toRingHom
q : R[X][X]
hqp : Polynomial.map φ.toRingHom q = Polynomial.map (algebraMap (↥R[s]) S) p
hqd : q.degree = (Polynomial.map (algebraMap (↥R[s]) S) p).degree
hqm : q.Monic
⊢ φ.IsIntegralElem t
Module: Mathlib.RingTheory.Ideal.GoingUp

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Algebra.IsIntegral R S
P : Ideal R
P_max : P.IsMaximal
hP : RingHom.ker (algebraMap R S) ≤ P
⊢ ∃ Q, Q.IsMaximal ∧ comap (algebraMap R S) Q = P

Tactic:
obtain ⟨Q, -, Q_prime, hQ⟩ := exists_ideal_over_prime_of_isIntegral P ⊥ hP
  exact ⟨Q, isMaximal_of_isIntegral_of_isMaximal_comap _ (hQ.symm ▸ P_max), hQ⟩

Goal state after:
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
a : A
ha : IsAlgebraic R a
p : R[X]
h : p ≠ 0
eval0 : (aeval a) p = 0
⊢ (aeval (-a)) (algEquivAevalNegX p) = 0

Tactic:
simpa [← comp_eq_aeval, aeval_comp]

Goal state after:
Module: Mathlib.RingTheory.SurjectiveOnStalks

Goal state before:
pp: case mp
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
P : Ideal S
inst✝ : P.IsPrime
H : Function.Surjective ⇑(Localization.localRingHom (Ideal.comap f P) P f ⋯)
y : S
a : R
t : ↥(Ideal.comap f P).primeCompl
ha :
  (Localization.localRingHom (Ideal.comap f P) P f ⋯)
      (IsLocalization.mk' (Localization.AtPrime (Ideal.comap f P)) a t) =
    IsLocalization.mk' (Localization.AtPrime P) y 1
⊢ ∃ x r, ∃ c ∉ P, f r ∉ P ∧ c * f r * y = c * f x

Tactic:
Localization.localRingHom_mk',

Goal state after:
case mp
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
P : Ideal S
inst✝ : P.IsPrime
H : Function.Surjective ⇑(Localization.localRingHom (Ideal.comap f P) P f ⋯)
y : S
a : R
t : ↥(Ideal.comap f P).primeCompl
ha : IsLocalization.mk' (Localization.AtPrime P) (f a) ⟨f ↑t, ⋯⟩ = IsLocalization.mk' (Localization.AtPrime P) y 1
⊢ ∃ x r, ∃ c ∉ P, f r ∉ P ∧ c * f r * y = c * f x
Module: Mathlib.RingTheory.SurjectiveOnStalks

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
inst✝ : IsLocalization M S
⊢ (algebraMap R S).SurjectiveOnStalks

Tactic:
refine surjectiveOnStalks_of_exists_div fun s ↦ ?_
  obtain ⟨x, s, rfl⟩ := IsLocalization.exists_mk'_eq M s
  exact ⟨x, s, IsLocalization.map_units S s, IsLocalization.mk'_spec' S x s⟩

Goal state after:
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✝ : Flat A B
h : Function.Surjective (PrimeSpectrum.comap (algebraMap A B))
m : Ideal A
hm : m.IsMaximal
m' : PrimeSpectrum B
hm' : PrimeSpectrum.comap (algebraMap A B) m' = { asIdeal := m, isPrime := ⋯ }
⊢ m • ⊤ ≠ ⊤

Tactic:
have : m = Ideal.comap (algebraMap A B) m'.asIdeal := by
    rw [← PrimeSpectrum.comap_asIdeal (algebraMap A B) m', hm']

Goal state after:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Flat A B
h : Function.Surjective (PrimeSpectrum.comap (algebraMap A B))
m : Ideal A
hm : m.IsMaximal
m' : PrimeSpectrum B
hm' : PrimeSpectrum.comap (algebraMap A B) m' = { asIdeal := m, isPrime := ⋯ }
this : m = Ideal.comap (algebraMap A B) m'.asIdeal
⊢ m • ⊤ ≠ ⊤
Module: Mathlib.Algebra.Order.Ring.Idempotent

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

Tactic:
← mul_assoc

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

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

Tactic:
← mul_assoc

Goal state after:
R : Type u_1
S : Type u_2
inst✝ : CommSemigroup S
a b c : { a // IsIdempotentElem a }
hab : ↑a * ↑b = ↑a
hac : ↑a * ↑c = ↑a
⊢ ↑a * ↑b * ↑c = ↑a
Module: Mathlib.Algebra.Order.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a : { a // IsIdempotentElem a }
⊢ ↑a - ↑a * ↑a = 0

Tactic:
a.2.eq,

Goal state after:
R : Type u_1
inst✝ : CommRing R
a : { a // IsIdempotentElem a }
⊢ ↑a - ↑a = 0
Module: Mathlib.RingTheory.Spectrum.Maximal.Localization

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
hf : Function.Bijective ⇑f
r : R
I : MaximalSpectrum S
⊢ (Localization.localRingHom (Ideal.comap f I.asIdeal) I.asIdeal f ⋯)
      (IsLocalization.mk' (Localization.AtPrime (Ideal.comap f I.asIdeal)) r 1) =
    (algebraMap S (Localization.AtPrime I.asIdeal)) (f r)

Tactic:
Localization.localRingHom_mk',

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
hf : Function.Bijective ⇑f
r : R
I : MaximalSpectrum S
⊢ IsLocalization.mk' (Localization.AtPrime I.asIdeal) (f r) ⟨f ↑1, ⋯⟩ =
    (algebraMap S (Localization.AtPrime I.asIdeal)) (f r)
Module: Mathlib.RingTheory.Spectrum.Maximal.Localization

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
r : R
I : PrimeSpectrum S
⊢ (Localization.localRingHom (Ideal.comap f I.asIdeal) I.asIdeal f ⋯)
      (IsLocalization.mk' (Localization.AtPrime (Ideal.comap f I.asIdeal)) r 1) =
    (algebraMap S (Localization.AtPrime I.asIdeal)) (f r)

Tactic:
Localization.localRingHom_mk',

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
r : R
I : PrimeSpectrum S
⊢ IsLocalization.mk' (Localization.AtPrime I.asIdeal) (f r) ⟨f ↑1, ⋯⟩ =
    (algebraMap S (Localization.AtPrime I.asIdeal)) (f r)
Module: Mathlib.Topology.Sets.Opens

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
a : Opens α
s : Set (Opens α)
⊢ ↑(a ⊓ sSup s) = ↑(⨆ b ∈ s, a ⊓ b)

Tactic:
by simp only [coe_inf, coe_iSup, coe_sSup, Set.inter_iUnion₂]

Goal state after:
Module: Mathlib.Topology.LocallyClosed

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ closure[inst✝] (s ∪ (closure[inst✝] s)ᶜ) = univ

Tactic:
closure_union,

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ closure[inst✝] s ∪ closure[inst✝] (closure[inst✝] s)ᶜ = univ
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 X
hs : IsRetrocompact s
hfemb : IsEmbedding f
hfcomp : IsRetrocompact (range f)
U : Set Y
hUcomp : IsCompact U
hUopen : IsOpen[inst✝] U
⊢ IsCompact (range f ∩ U)

Tactic:
exact hfcomp hUcomp hUopen

Goal state after:
Module: Mathlib.Topology.Sober

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
ι : Type u_3
U : ι → Opens α
hU : IsOpenCover U
hU' : ∀ (i : ι), QuasiSober ↥(U i)
⊢ ∀ {S : Set α}, IsIrreducible S → IsClosed S → ∃ x, IsGenericPoint x S

Tactic:
rintro t ⟨⟨x, hx⟩, h⟩ h'

Goal state after:
α : 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
⊢ ∃ x, IsGenericPoint x t
Module: Mathlib.Topology.Constructible

Goal state before:
pp: case open_retrocompact
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsClosedEmbedding f
hfcomp : IsRetrocompact (range f)ᶜ
U : Set X
hUopen : IsOpen[inst✝¹] U
hUcomp : IsRetrocompact U
hfU : IsOpen[inst✝] (f '' U ∪ (range f)ᶜ)
V : Set Y
hVcomp : IsCompact V
hVopen : IsOpen[inst✝] V
⊢ IsCompact (f '' U ∩ V ∪ (range f)ᶜ ∩ V)

Tactic:
← image_inter_preimage

Goal state after:
case open_retrocompact
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsClosedEmbedding f
hfcomp : IsRetrocompact (range f)ᶜ
U : Set X
hUopen : IsOpen[inst✝¹] U
hUcomp : IsRetrocompact U
hfU : IsOpen[inst✝] (f '' U ∪ (range f)ᶜ)
V : Set Y
hVcomp : IsCompact V
hVopen : IsOpen[inst✝] V
⊢ IsCompact (f '' (U ∩ f ⁻¹' V) ∪ (range f)ᶜ ∩ V)
Module: Mathlib.RingTheory.RingHom.Flat

Goal state before:
pp: R S T : CommRingCat
f : R ⟶ S
g : R ⟶ T
hf : Function.Injective ⇑(ConcreteCategory.hom f)
hg : (Hom.hom g).Flat
⊢ Function.Injective ⇑(ConcreteCategory.hom (pushout.inr f g))

Tactic:
algebraize [f.hom, g.hom]
  have : _ = pushout.inr f g := (CommRingCat.isPushout_tensorProduct R S T).inr_isoPushout_hom
  rw [← this]
  exact (CommRingCat.isPushout_tensorProduct R S T).isoPushout.commRingCatIsoToRingEquiv
    |>.injective.comp (Algebra.TensorProduct.includeRight_injective (B := T) hf)

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
f : R →+* S
hf : Surjective ⇑f
⊢ zariskiTopology = TopologicalSpace.induced (comap f) zariskiTopology

Tactic:
by
    simp only [TopologicalSpace.ext_iff, ← isClosed_compl_iff, isClosed_iff_zeroLocus,
      isClosed_induced_iff]
    refine fun s =>
      ⟨fun ⟨F, hF⟩ =>
        ⟨zeroLocus (f ⁻¹' F), ⟨f ⁻¹' F, rfl⟩, by
          rw [preimage_comap_zeroLocus, Function.Surjective.image_preimage hf, hF]⟩,
        ?_⟩
    rintro ⟨-, ⟨F, rfl⟩, hF⟩
    exact ⟨f '' F, hF.symm.trans (preimage_comap_zeroLocus f F)⟩

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

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing M
inst✝³ : Algebra R A
inst✝² : Algebra R M
F : Type u_4
inst✝¹ : FunLike F A M
inst✝ : AlgHomClass F R A M
f : F
f_inv : M → A
hf : Function.RightInverse f_inv ⇑f
d : Derivation R A A
hd : ∀ (x : A), f x = 0 → f (d x) = 0
x : R
y : M
⊢ f (d (f_inv (x • y))) = (RingHom.id R) x • f (d (f_inv y))

Tactic:
by
    suffices f (d (f_inv (x • y) - x • f_inv y)) = 0 by simpa [sub_eq_zero]
    apply hd
    simp [hf _]

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
h✝ : IsCyclic G
σ : G →* G
h : G
hG : ∀ (x : G), x ∈ zpowers h
m : ℤ
hm : (fun x ↦ h ^ x) m = σ h
n : ℤ
⊢ h ^ (m * n) = (fun x ↦ h ^ x) n ^ m

Tactic:
← zpow_mul'

Goal state after:
G : Type u_2
inst✝ : Group G
h✝ : IsCyclic G
σ : G →* G
h : G
hG : ∀ (x : G), x ∈ zpowers h
m : ℤ
hm : (fun x ↦ h ^ x) m = σ h
n : ℤ
⊢ h ^ (m * n) = h ^ (m * n)
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: G : Type u_2
inst✝ : Group G
H : Subgroup G
hp : Fact (Nat.Prime (Nat.card G))
⊢ H = ⊥ ∨ H = ⊤

Tactic:
have : Finite G := Nat.finite_of_card_ne_zero hp.1.ne_zero
  have := card_subgroup_dvd_card H
  rwa [Nat.dvd_prime hp.1, ← eq_bot_iff_card, card_eq_iff_eq_top] at this

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

Goal state before:
pp: case refine_3
ι : Type u_1
R : ι → Type u_2
inst✝ : (i : ι) → CommRing (R i)
⊢ IsOpenMap (sigmaToPi R)

Tactic:
· rw [isOpenMap_sigma]
    intro i
    simp only [sigmaToPi_apply, PrimeSpectrum.isTopologicalBasis_basic_opens.isOpenMap_iff]
    rintro - ⟨f, rfl⟩
    rw [PrimeSpectrum.comap_evalRingHom_basicOpen]
    exact isOpen_basicOpen

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : (exponent G).factorization p = 0
⊢ orderOf 1 = 1

Tactic:
orderOf_one

Goal state after:
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : (exponent G).factorization p = 0
⊢ 1 = 1
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case inr
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : (exponent G).factorization p ≠ 0
⊢ ∃ g, orderOf g = p ^ (exponent G).factorization p

Tactic:
have he : 0 < exponent G :=
    Ne.bot_lt fun ht => by
      rw [ht] at h
      apply h
      rw [bot_eq_zero, Nat.factorization_zero, Finsupp.zero_apply]

Goal state after:
case inr
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : (exponent G).factorization p ≠ 0
he : 0 < exponent G
⊢ ∃ g, orderOf g = p ^ (exponent G).factorization p
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s✝ : Set (PrimeSpectrum R)
x✝ : ∃ I, I.FG ∧ (zeroLocus ↑I)ᶜ = s✝
I : Ideal R
s : Finset R
hs : Ideal.span ↑s = I
e : (zeroLocus ↑I)ᶜ = s✝
⊢ (zeroLocus ↑s)ᶜ = s✝

Tactic:
simpa [hs.symm] using e

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝¹ : Monoid G
inst✝ : IsCancelMul G
h : ∀ (g : G), orderOf g ∣ 2
a b : G
⊢ Commute a b

Tactic:
simp_rw [orderOf_dvd_iff_pow_eq_one] at h

Goal state after:
G : Type u
inst✝¹ : Monoid G
inst✝ : IsCancelMul G
a b : G
h : ∀ (g : G), g ^ 2 = 1
⊢ Commute a b
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
h : IsClosedMap (comap (mapRingHom f))
algInst✝ : Algebra R S := f.toAlgebra
a✝¹ : Nontrivial R
a✝ : Nontrivial S
r : S
p : S[X] := C r * X - 1
H : zeroLocus ↑(Ideal.comap (mapRingHom f) (Ideal.span {p})) = comap (mapRingHom f) '' zeroLocus ↑(Ideal.span {p})
⊢ 1 ∈ Ideal.span {X} ⊔ Ideal.comap (mapRingHom f) (Ideal.span {p})

Tactic:
← Ideal.eq_top_iff_one,

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
h : IsClosedMap (comap (mapRingHom f))
algInst✝ : Algebra R S := f.toAlgebra
a✝¹ : Nontrivial R
a✝ : Nontrivial S
r : S
p : S[X] := C r * X - 1
H : zeroLocus ↑(Ideal.comap (mapRingHom f) (Ideal.span {p})) = comap (mapRingHom f) '' zeroLocus ↑(Ideal.span {p})
⊢ Ideal.span {X} ⊔ Ideal.comap (mapRingHom f) (Ideal.span {p}) = ⊤
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
h : IsClosedMap (comap (mapRingHom f))
algInst✝ : Algebra R S := f.toAlgebra
a✝¹ : Nontrivial R
a✝ : Nontrivial S
r : S
p : S[X] := C r * X - 1
H : zeroLocus ↑(Ideal.comap (mapRingHom f) (Ideal.span {p})) = comap (mapRingHom f) '' zeroLocus ↑(Ideal.span {p})
q : PrimeSpectrum S[X]
hpq : p ∈ q.asIdeal
hXq : X ∈ q.asIdeal
this : 1 ∈ q.asIdeal
⊢ False

Tactic:
exact q.2.ne_top (q.asIdeal.eq_top_iff_one.mpr this)

Goal state after:
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: case neg.refine_1
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
P : Subgroup G
hP : IsPGroup p ↥P
H : Subgroup G
inst✝ : H.Normal
h_cop : (Nat.card ↥H).Coprime H.index
h1 : ¬Nat.card ↥H = 0
h2 : ¬H.index = 0
this : Finite G
h3 : (Nat.card ↥H).Coprime (Nat.card ↥P) ∨ H.index.Coprime (Nat.card ↥P)
h4 : H.index.Coprime (Nat.card ↥P)
⊢ P ≤ H

pp: case neg.refine_2
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
P : Subgroup G
hP : IsPGroup p ↥P
H : Subgroup G
inst✝ : H.Normal
h_cop : (Nat.card ↥H).Coprime H.index
h1 : ¬Nat.card ↥H = 0
h2 : ¬H.index = 0
this : Finite G
h3 : (Nat.card ↥H).Coprime (Nat.card ↥P) ∨ H.index.Coprime (Nat.card ↥P)
h4 : (Nat.card ↥H).Coprime (Nat.card ↥P)
⊢ Disjoint H P

Tactic:
· rw [← Subgroup.relIndex_eq_one]
    exact Nat.eq_one_of_dvd_coprimes h4 (H.relIndex_dvd_index_of_normal P)
      (Subgroup.relIndex_dvd_card H P)

Goal state after:
case neg.refine_2
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
P : Subgroup G
hP : IsPGroup p ↥P
H : Subgroup G
inst✝ : H.Normal
h_cop : (Nat.card ↥H).Coprime H.index
h1 : ¬Nat.card ↥H = 0
h2 : ¬H.index = 0
this : Finite G
h3 : (Nat.card ↥H).Coprime (Nat.card ↥P) ∨ H.index.Coprime (Nat.card ↥P)
h4 : (Nat.card ↥H).Coprime (Nat.card ↥P)
⊢ Disjoint H P
Module: Mathlib.Algebra.Module.ZMod

Goal state before:
pp: n : ℕ
M : Type u_1
M₁ : Type u_2
inst✝¹ : NeZero n
inst✝ : AddCommMonoid M
h : ∀ (x : M), n • x = 0
c : ℕ
x : M
⊢ (c % n + c / n * n) • x = c • x

Tactic:
rw [Nat.mod_add_div']

Goal state after:
Module: Mathlib.GroupTheory.Rank

Goal state before:
pp: G : Type u_1
inst✝ : Group G
g : G
⊢ Nat.card ↥(centralizer {g}) = Nat.card ↥(MulAction.stabilizer (ConjAct G) g)

Tactic:
rw [centralizer_eq_comap_stabilizer]; rfl

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
e : R
he : IsIdempotentElem e
⊢ zeroLocus {e} = ↑(basicOpen (1 - e))

Tactic:
rw [basicOpen_eq_zeroLocus_of_isIdempotentElem _ he.one_sub, sub_sub_cancel]

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
x g : G
hx : x ∈ centralizer ↑P
h1 : ↑P ≤ centralizer ↑(zpowers x)
z : G
hy : g * (z * g⁻¹) * x = x * (g * (z * g⁻¹))
hz : z ∈ ↑↑P
⊢ ((MulDistribMulAction.toMonoidEnd (MulAut G) G) (MulAut.conj g)) z * x =
    x * ((MulDistribMulAction.toMonoidEnd (MulAut G) G) (MulAut.conj g)) z

Tactic:
← mul_assoc

Goal state after:
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
x g : G
hx : x ∈ centralizer ↑P
h1 : ↑P ≤ centralizer ↑(zpowers x)
z : G
hy : g * z * g⁻¹ * x = x * (g * z * g⁻¹)
hz : z ∈ ↑↑P
⊢ ((MulDistribMulAction.toMonoidEnd (MulAut G) G) (MulAut.conj g)) z * x =
    x * ((MulDistribMulAction.toMonoidEnd (MulAut G) G) (MulAut.conj g)) z
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
⊢ List.IsChain (fun x1 x2 ↦ x1 < x2) (toList s)

Tactic:
simp_rw [List.isChain_iff_getElem, s.toList_getElem]

Goal state after:
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
⊢ ∀ (i : ℕ) (_hi : i + 1 < (toList s).length), s.toFun ⟨i, ⋯⟩ < s.toFun ⟨i + 1, ⋯⟩
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
⊢ ↑(if hi : a = a then ⟨v, ⋯⟩ else ⟨u * ↑(μ a), ⋯⟩) + ∑ x ∈ t, ↑(if hi : x = a then ⟨v, ⋯⟩ else ⟨u * ↑(μ x), ⋯⟩) = 1

Tactic:
dif_pos rfl,

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
⊢ ↑⟨v, ⋯⟩ + ∑ x ∈ t, ↑(if hi : x = a then ⟨v, ⋯⟩ else ⟨u * ↑(μ x), ⋯⟩) = 1