mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

Goal state before:
pp: case neg
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
p : R[X]
x : S
h : f (p.coeff 0) = 0
h' : p.natDegree = 0
hp : ¬Polynomial.map f p = 0
⊢ Polynomial.map f p = 0

Tactic:
eq_C_of_natDegree_eq_zero h',

Goal state after:
case neg
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
p : R[X]
x : S
h : f (p.coeff 0) = 0
h' : p.natDegree = 0
hp : ¬Polynomial.map f p = 0
⊢ Polynomial.map f (C (p.coeff 0)) = 0
Module: Mathlib.RingTheory.Ideal.GoingUp

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
S : Type u_2
inst✝⁴ : CommRing S
I : Ideal S
inst✝³ : Algebra R S
inst✝² : Nontrivial R
inst✝¹ : IsDomain S
inst✝ : Algebra.IsIntegral R S
hI : comap (algebraMap R S) I = ⊥
⊢ I = ⊥

Tactic:
by
  refine eq_bot_iff.2 fun x hx => ?_
  by_cases hx0 : x = 0
  · exact hx0.symm ▸ Ideal.zero_mem ⊥
  · exact absurd hI (comap_ne_bot_of_integral_mem hx0 hx (Algebra.IsIntegral.isIntegral x))

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
⊢ nilradical R = iInf asIdeal

Tactic:
apply range_asIdeal R ▸ nilradical_eq_sInf R

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
f : R
I : PrimeSpectrum R
⊢ I ∈ (zeroLocus {f})ᶜ ↔ f ∉ I.asIdeal

Tactic:
rw [Set.mem_compl_iff, mem_zeroLocus, Set.singleton_subset_iff]; rfl

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

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

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

Tactic:
· rw [a.2.1, mul_comm, eq, b.2.1]

Goal state after:
case refine_2
R : Type u_1
inst✝ : CommSemiring R
a b : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
eq : (↑a).1 = (↑b).1
⊢ (↑a).1 + (↑b).2 = 1
Module: Mathlib.RingTheory.KrullDimension.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : ⊥.IsPrime
this : OrderBot (PrimeSpectrum R) := { bot := { asIdeal := ⊥, isPrime := inst✝ }, bot_le := ⋯ }
⊢ (∀ (a : Ideal R) (b : a.IsPrime),
      ¬(PrimeSpectrum.equivSubtype R).symm ⟨a, b⟩ = ⊥ →
        ((PrimeSpectrum.equivSubtype R).symm ⟨a, b⟩).asIdeal.IsMaximal) ↔
    ∀ (I : Ideal R), I.IsPrime → ¬I = ⊥ → I.IsMaximal

Tactic:
PrimeSpectrum.ext_iff

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : ⊥.IsPrime
this : OrderBot (PrimeSpectrum R) := { bot := { asIdeal := ⊥, isPrime := inst✝ }, bot_le := ⋯ }
⊢ (∀ (a : Ideal R) (b : a.IsPrime),
      ¬((PrimeSpectrum.equivSubtype R).symm ⟨a, b⟩).asIdeal = ⊥.asIdeal →
        ((PrimeSpectrum.equivSubtype R).symm ⟨a, b⟩).asIdeal.IsMaximal) ↔
    ∀ (I : Ideal R), I.IsPrime → ¬I = ⊥ → I.IsMaximal
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization

Goal state before:
pp: case mp
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
x : R
p : Ideal R
hxp : x ∈ p
hp₃ : ∀ ⦃y : Ideal R⦄, (fun q ↦ q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y
hp₁ : p.IsPrime
hp₂ : I ≤ p
this : map (algebraMap R (Localization.AtPrime p)) p ≤ (map (algebraMap R (Localization.AtPrime p)) I).radical
n : ℕ
a : ↥I
b t : ↥p.primeCompl
ht : ↑t * (x ^ n * ↑(a, b).2) = ↑t * ↑(a, b).1
⊢ (x * (↑t * ↑b)) ^ (n + 1) ∈ I

Tactic:
simp only at ht

Goal state after:
case mp
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
x : R
p : Ideal R
hxp : x ∈ p
hp₃ : ∀ ⦃y : Ideal R⦄, (fun q ↦ q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y
hp₁ : p.IsPrime
hp₂ : I ≤ p
this : map (algebraMap R (Localization.AtPrime p)) p ≤ (map (algebraMap R (Localization.AtPrime p)) I).radical
n : ℕ
a : ↥I
b t : ↥p.primeCompl
ht : ↑t * (x ^ n * ↑b) = ↑t * ↑a
⊢ (x * (↑t * ↑b)) ^ (n + 1) ∈ I
Module: Mathlib.RingTheory.Spectrum.Prime.RingHom

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Surjective ⇑f
⊢ Set.range (comap f) = zeroLocus ↑(ker f)

Tactic:
by
  rw [← Set.image_univ]
  convert! image_comap_zeroLocus_eq_zeroLocus_comap _ _ hf _
  rw [zeroLocus_bot]

Goal state after:
Module: Mathlib.Order.BooleanSubalgebra

Goal state before:
pp: α : Type u_2
inst✝ : BooleanAlgebra α
L : BooleanSubalgebra α
a b : α
ha : a ∈ L
hb : b ∈ L
⊢ a \ b ∈ L

Tactic:
rw [_root_.sdiff_eq]

Goal state after:
α : Type u_2
inst✝ : BooleanAlgebra α
L : BooleanSubalgebra α
a b : α
ha : a ∈ L
hb : b ∈ L
⊢ a ⊓ bᶜ ∈ L
Module: Mathlib.Topology.Sets.Opens

Goal state before:
pp: case h
X : Type u
inst✝ : TopologicalSpace X
ι : Type u_5
U : ι → Opens X
hU : IsBasis (range U)
W : Opens X
Us : Set (Opens X)
hUs : W = sSup Us
a : ⦃a : Opens X⦄ → a ∈ Us → ι
ha : ∀ ⦃a_1 : Opens X⦄ (a_2 : a_1 ∈ Us), U (a a_2) = a_1
⊢ W = ⨆ k, U ((fun i ↦ a ⋯) k)

Tactic:
simp [hUs, ha, sSup_eq_iSup' Us]

Goal state after:
Module: Mathlib.Topology.QuasiSeparated

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : IsEmbedding f
U V : Set β
⊢ U ⊆ f '' s → IsOpen[inst✝] U → IsCompact U → V ⊆ f '' s → IsOpen[inst✝] V → IsCompact V → IsCompact (U ∩ V)

Tactic:
hU

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : IsEmbedding f
U V : Set β
hU : U ⊆ f '' s
⊢ IsOpen[inst✝] U → IsCompact U → V ⊆ f '' s → IsOpen[inst✝] V → IsCompact V → IsCompact (U ∩ V)
Module: Mathlib.Topology.QuasiSeparated

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s t : Set α
ht : IsQuasiSeparated t
h : s ⊆ t
U V : Set α
⊢ U ⊆ s → IsOpen[inst✝] U → IsCompact U → V ⊆ s → IsOpen[inst✝] V → IsCompact V → IsCompact (U ∩ V)

Tactic:
hU

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
s t : Set α
ht : IsQuasiSeparated t
h : s ⊆ t
U V : Set α
hU : U ⊆ s
⊢ IsOpen[inst✝] U → IsCompact U → V ⊆ s → IsOpen[inst✝] V → IsCompact V → IsCompact (U ∩ V)
Module: Mathlib.Topology.QuasiSeparated

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
h : IsOpenEmbedding f
s : Set α
H : IsQuasiSeparated (f '' s)
U V : Set α
⊢ U ⊆ s → IsOpen[inst✝¹] U → IsCompact U → V ⊆ s → IsOpen[inst✝¹] V → IsCompact V → IsCompact (U ∩ V)

Tactic:
hU

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
h : IsOpenEmbedding f
s : Set α
H : IsQuasiSeparated (f '' s)
U V : Set α
hU : U ⊆ s
⊢ IsOpen[inst✝¹] U → IsCompact U → V ⊆ s → IsOpen[inst✝¹] V → IsCompact V → IsCompact (U ∩ V)
Module: Mathlib.Topology.Spectral.Prespectral

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : PrespectralSpace X
Z U₁ U₂ : Set X
hU₁ : ∀ a ∈ U₁, ∃ t ∈ {U | IsOpen[inst✝¹] U ∧ IsCompact U}, a ∈ t ∧ t ⊆ U₁
hU₂ : ∀ a ∈ U₂, ∃ t ∈ {U | IsOpen[inst✝¹] U ∧ IsCompact U}, a ∈ t ∧ t ⊆ U₂
hU₁Z : (Z ∩ U₁).Nonempty
hU₂Z : (Z ∩ U₂).Nonempty
hU₁₂ : Z ∩ (U₁ ∩ U₂) ⊆ ∅
x₁ : X
hx₁ : x₁ ∈ U₁ ∧ x₁ ∈ Z ∧ x₁ ∉ U₂
x₂ : X
hx₂ : x₂ ∈ U₂ ∧ x₂ ∈ Z ∧ x₂ ∉ U₁
W₁ : Set X
hW₁ : W₁ ∈ {U | IsOpen[inst✝¹] U ∧ IsCompact U} ∧ x₁ ∈ W₁ ∧ W₁ ⊆ U₁
W₂ : Set X
hW₂ : W₂ ∈ {U | IsOpen[inst✝¹] U ∧ IsCompact U} ∧ x₂ ∈ W₂ ∧ W₂ ⊆ U₂
z : X
hz : z ∈ Z
⊢ z ∈ W₁ᶜ ∪ W₂ᶜ

Tactic:
by_contra! hc
    simp only [Set.mem_union, Set.mem_compl_iff, not_or, not_not] at hc
    exact hU₁₂ ⟨hz, hW₁.2.2 hc.1, hW₂.2.2 hc.2⟩

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
algInst✝ : Algebra R S := f.toAlgebra
⊢ (algebraMap R S).FaithfullyFlat ↔ (algebraMap R S).Flat ∧ Function.Surjective (PrimeSpectrum.comap (algebraMap R S))

Tactic:
faithfullyFlat_algebraMap_iff,

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
algInst✝ : Algebra R S := f.toAlgebra
⊢ Module.FaithfullyFlat R S ↔ (algebraMap R S).Flat ∧ Function.Surjective (PrimeSpectrum.comap (algebraMap R S))
Module: Mathlib.RingTheory.Ideal.GoingDown

Goal state before:
pp: case h
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.HasGoingDown R S
q : PrimeSpectrum R
P : Ideal S
inst✝ : P.IsPrime
lo : P.LiesOver (RelSeries.singleton {(a, b) | a < b} q).last.asIdeal
⊢ (RelSeries.singleton {(a, b) | a < b} { asIdeal := P, isPrime := ⋯ }).length =
      (RelSeries.singleton {(a, b) | a < b} q).length ∧
    (RelSeries.singleton {(a, b) | a < b} { asIdeal := P, isPrime := ⋯ }).last = { asIdeal := P, isPrime := ⋯ } ∧
      List.map (PrimeSpectrum.comap (algebraMap R S))
          (RelSeries.singleton {(a, b) | a < b} { asIdeal := P, isPrime := ⋯ }).toList =
        (RelSeries.singleton {(a, b) | a < b} q).toList

Tactic:
simp only [RelSeries.singleton_length, RelSeries.last_singleton, RelSeries.toList_singleton,
      List.map_cons, List.map_nil, List.cons.injEq, and_true, true_and]

Goal state after:
case h
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.HasGoingDown R S
q : PrimeSpectrum R
P : Ideal S
inst✝ : P.IsPrime
lo : P.LiesOver (RelSeries.singleton {(a, b) | a < b} q).last.asIdeal
⊢ PrimeSpectrum.comap (algebraMap R S) { asIdeal := P, isPrime := ⋯ } = q
Module: Mathlib.RingTheory.Ideal.GoingDown

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.HasGoingDown R S
l : RelSeries {(a, b) | a < b}
q : PrimeSpectrum R
lt : (q, l.head) ∈ {(a, b) | a < b}
ih :
  ∀ (P : Ideal S) [inst : P.IsPrime] [lo : P.LiesOver l.last.asIdeal],
    ∃ L,
      L.length = l.length ∧
        RelSeries.last L = { asIdeal := P, isPrime := ⋯ } ∧
          List.map (PrimeSpectrum.comap (algebraMap R S)) (RelSeries.toList L) = l.toList
P : Ideal S
inst✝ : P.IsPrime
lo : P.LiesOver l.last.asIdeal
L : LTSeries (PrimeSpectrum S)
len : L.length = l.length
last : RelSeries.last L = { asIdeal := P, isPrime := ⋯ }
spec : List.map (PrimeSpectrum.comap (algebraMap R S)) (RelSeries.toList L) = l.toList
this : l.toList[0] = PrimeSpectrum.comap (algebraMap R S) (RelSeries.toList L)[0]
⊢ l.toList[0].asIdeal = comap (algebraMap R S) (RelSeries.toList L)[0].asIdeal

Tactic:
PrimeSpectrum.ext_iff

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.HasGoingDown R S
l : RelSeries {(a, b) | a < b}
q : PrimeSpectrum R
lt : (q, l.head) ∈ {(a, b) | a < b}
ih :
  ∀ (P : Ideal S) [inst : P.IsPrime] [lo : P.LiesOver l.last.asIdeal],
    ∃ L,
      L.length = l.length ∧
        RelSeries.last L = { asIdeal := P, isPrime := ⋯ } ∧
          List.map (PrimeSpectrum.comap (algebraMap R S)) (RelSeries.toList L) = l.toList
P : Ideal S
inst✝ : P.IsPrime
lo : P.LiesOver l.last.asIdeal
L : LTSeries (PrimeSpectrum S)
len : L.length = l.length
last : RelSeries.last L = { asIdeal := P, isPrime := ⋯ }
spec : List.map (PrimeSpectrum.comap (algebraMap R S)) (RelSeries.toList L) = l.toList
this : l.toList[0].asIdeal = (PrimeSpectrum.comap (algebraMap R S) (RelSeries.toList L)[0]).asIdeal
⊢ l.toList[0].asIdeal = comap (algebraMap R S) (RelSeries.toList L)[0].asIdeal
Module: Mathlib.RingTheory.Derivation.ToSquareZero

Goal state before:
pp: case refine_2
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
hI : I ^ 2 = ⊥
inst✝ : IsScalarTower R A B
⊢ Function.LeftInverse (fun f ↦ derivationToSquareZeroOfLift I hI ↑f ⋯) fun d ↦ ⟨liftOfDerivationToSquareZero I hI d, ⋯⟩

Tactic:
intro d; ext x; exact add_sub_cancel_right (d x : B) (algebraMap A B x)

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

Goal state before:
pp: case mpr
R : Type u
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsRadical
⊢ (∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I) → ∀ (x y : Ideal R), x ⊓ y ≤ I → x ≤ I ∨ y ≤ I

Tactic:
· simp_rw [or_iff_not_imp_left, SetLike.not_le_iff_exists]
        rintro h s t h' ⟨x, hx, hx'⟩ y hy
        exact h (h' ⟨Ideal.mul_mem_right _ _ hx, Ideal.mul_mem_left _ _ hy⟩) hx'

Goal state after:
Module: Mathlib.Data.ZMod.QuotientGroup

Goal state before:
pp: n : ℕ
A : Type u_1
R : Type u_2
inst✝³ : AddGroup A
inst✝² : Ring R
α : Type u_3
β : Type u_4
inst✝¹ : AddGroup α
a : α
inst✝ : AddAction α β
b : β
⊢ Injective
    ⇑(QuotientAddGroup.map (zmultiples ↑(minimalPeriod (fun x ↦ a +ᵥ x) b)) (stabilizer (↥(zmultiples a)) b)
        ((zmultiplesHom ↥(zmultiples a)) ⟨a, ⋯⟩) ⋯)

Tactic:
by
            rw [← ker_eq_bot_iff, eq_bot_iff]
            refine fun q => induction_on q fun n hn => ?_
            rw [mem_bot, eq_zero_iff, Int.mem_zmultiples_iff, ←
              zsmul_vadd_eq_iff_minimalPeriod_dvd]
            exact (eq_zero_iff _).mp hn

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

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
inst✝ : DiscreteTopology (PrimeSpectrum R)
x : PiLocalization R
f : PrimeSpectrum R → R
hf : ∀ (p : PrimeSpectrum R), ↑(basicOpen (f p)) = {p}
⊢ ∃ a, (toPiLocalization R) a = x

Tactic:
let e := Equiv.ofInjective f fun p q eq ↦ Set.singleton_injective (hf p ▸ eq ▸ hf q)

Goal state after:
R : Type u
inst✝¹ : CommSemiring R
inst✝ : DiscreteTopology (PrimeSpectrum R)
x : PiLocalization R
f : PrimeSpectrum R → R
hf : ∀ (p : PrimeSpectrum R), ↑(basicOpen (f p)) = {p}
e : PrimeSpectrum R ≃ ↑(Set.range f) := Equiv.ofInjective f ⋯
⊢ ∃ a, (toPiLocalization R) a = x
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'
M : Type u_4
inst✝² : Monoid M
inst✝¹ : IsCyclic G
inst✝ : MulDistribMulAction M G
n✝ : ℕ
hn : Nat.card G = n✝
m n : M
g : G
hg : orderOf g = Nat.card G
⊢ g ^ ⋯.choose = (toMonoidHom G m) ((toMonoidHom G n) g)

Tactic:
← (MulDistribMulAction.toMonoidHom G (m * n)).map_cyclic.choose_spec,

Goal state after:
α : Type u_1
G : Type u_2
G' : Type u_3
a : α
inst✝⁵ : Group α
inst✝⁴ : Group G
inst✝³ : Group G'
M : Type u_4
inst✝² : Monoid M
inst✝¹ : IsCyclic G
inst✝ : MulDistribMulAction M G
n✝ : ℕ
hn : Nat.card G = n✝
m n : M
g : G
hg : orderOf g = Nat.card G
⊢ (toMonoidHom G (m * n)) g = (toMonoidHom G m) ((toMonoidHom G n) g)
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case left
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
this : I * J ≤ nilradical R
n : ℕ
hn : I ^ n * J ^ n ≤ ⊥
hnz : n ≠ 0
x : R
hx : x ∈ ↑I
⊢ (fun x ↦ x ^ n) x ∈ ↑(I ^ n ⊔ J ^ n)

Tactic:
exact Ideal.mem_sup_left (Ideal.pow_mem_pow hx n)

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)
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
this✝ : Fintype α
this : Fintype ↑(fixedPoints G α)
key : ∀ (x : α), card { y // Quotient.mk'' y = Quotient.mk'' x } = card ↑(orbit G x)
⊢ ∑ x, ↑(card { x_1 // Quotient.mk'' x_1 = x }) = ∑ x, ↑1

Tactic:
refine
      Eq.symm
        (Finset.sum_bij_ne_zero (fun a _ _ => Quotient.mk'' a.1) (fun _ _ _ => Finset.mem_univ _)
          (fun a₁ _ _ a₂ _ _ h =>
            Subtype.ext (mem_fixedPoints'.mp a₂.2 a₁.1 (Quotient.exact' h)))
          (fun b => Quotient.inductionOn' b fun b _ hb => ?_) fun a ha _ => by
          rw [key, mem_fixedPoints_iff_card_orbit_eq_one.mp a.2])

Goal state after:
p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
this✝ : Fintype α
this : Fintype ↑(fixedPoints G α)
key : ∀ (x : α), card { y // Quotient.mk'' y = Quotient.mk'' x } = card ↑(orbit G x)
b✝ : Quotient (orbitRel G α)
b : α
x✝ : Quotient.mk'' b ∈ Finset.univ
hb : ↑(card { x // Quotient.mk'' x = Quotient.mk'' b }) ≠ 0
⊢ ∃ a, ∃ (_ : a ∈ Finset.univ) (_ : ↑1 ≠ 0), Quotient.mk'' ↑a = Quotient.mk'' b
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
this : I * J ≤ nilradical R
n : ℕ
hn : I ^ n * J ^ n ≤ ⊥
hnz : n ≠ 0
⊢ Ideal.span (↑I ∪ ↑J) = ⊤

Tactic:
Ideal.span_union,

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
this : I * J ≤ nilradical R
n : ℕ
hn : I ^ n * J ^ n ≤ ⊥
hnz : n ≠ 0
⊢ Ideal.span ↑I ⊔ Ideal.span ↑J = ⊤
Module: Mathlib.GroupTheory.PGroup

Goal state before:
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:
exact Subgroup.disjoint_of_coprime_natCard h4

Goal state after:
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Fact (Nat.Prime p)
hG : Nat.card G = p ^ 2
⊢ IsCyclic (G ⧸ center G)

Tactic:
apply isCyclic_of_card_dvd_prime (p := p)

Goal state after:
p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Fact (Nat.Prime p)
hG : Nat.card G = p ^ 2
⊢ Nat.card (G ⧸ center G) ∣ p
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Fact (Nat.Prime p)
hG : Nat.card G = p ^ 2
⊢ p * Nat.card (G ⧸ center G) ∣ p * p

Tactic:
← sq,

Goal state after:
p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Fact (Nat.Prime p)
hG : Nat.card G = p ^ 2
⊢ p * Nat.card (G ⧸ center G) ∣ p ^ 2
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: α : Type u_1
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → #{a | a ^ n = 1} ≤ n
d : ℕ
IH : ∀ m < d, m ∣ Fintype.card α → 0 < #{a | orderOf a = m} → #{a | orderOf a = m} = φ m
hd : d ∣ Fintype.card α
hpos : 0 < #{a | orderOf a = d}
hd0 : d ≠ 0
a : α
ha' : a ∈ {a | orderOf a = d}
ha : orderOf a = d
h1 : ∑ m ∈ d.properDivisors, #{a | orderOf a = m} = ∑ m ∈ d.properDivisors, φ m
⊢ #{x | x ^ orderOf a = 1} = orderOf a

Tactic:
card_pow_eq_one_eq_orderOf_aux hn a

Goal state after:
α : Type u_1
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → #{a | a ^ n = 1} ≤ n
d : ℕ
IH : ∀ m < d, m ∣ Fintype.card α → 0 < #{a | orderOf a = m} → #{a | orderOf a = m} = φ m
hd : d ∣ Fintype.card α
hpos : 0 < #{a | orderOf a = d}
hd0 : d ≠ 0
a : α
ha' : a ∈ {a | orderOf a = d}
ha : orderOf a = d
h1 : ∑ m ∈ d.properDivisors, #{a | orderOf a = m} = ∑ m ∈ d.properDivisors, φ m
⊢ orderOf a = orderOf a
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
⊢ Set.EqOn ((zeroLocus ∘ SetLike.coe) ∘ vanishingIdeal) id (irreducibleComponents (PrimeSpectrum R))

Tactic:
intro s hs

Goal state after:
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
hs : s ∈ irreducibleComponents (PrimeSpectrum R)
⊢ ((zeroLocus ∘ SetLike.coe) ∘ vanishingIdeal) s = id s
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝³ : CommSemiring R
inst✝² : IsLocalRing R
S : Type v
inst✝¹ : CommSemiring S
inst✝ : IsLocalRing S
f : R →+* S
this : IsLocalHom f ↔ Ideal.comap f (maximalIdeal S) = maximalIdeal R
⊢ Ideal.comap f (maximalIdeal S) = maximalIdeal R ↔ PrimeSpectrum.comap f (closedPoint S) = closedPoint R

Tactic:
PrimeSpectrum.ext_iff

Goal state after:
R : Type u
inst✝³ : CommSemiring R
inst✝² : IsLocalRing R
S : Type v
inst✝¹ : CommSemiring S
inst✝ : IsLocalRing S
f : R →+* S
this : IsLocalHom f ↔ Ideal.comap f (maximalIdeal S) = maximalIdeal R
⊢ Ideal.comap f (maximalIdeal S) = maximalIdeal R ↔
    (PrimeSpectrum.comap f (closedPoint S)).asIdeal = (closedPoint R).asIdeal
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 : z * (g⁻¹ * x) * g = g⁻¹ * x * g * z
hz : z ∈ ↑↑P
⊢ ((MulDistribMulAction.toMonoidEnd (MulAut G) G) (MulAut.conj g)) z * x =
    x * ((MulDistribMulAction.toMonoidEnd (MulAut G) G) (MulAut.conj g)) z

Tactic:
← eq_mul_inv_iff_mul_eq,

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 : z * (g⁻¹ * x) = g⁻¹ * 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.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: G : Type u_2
inst✝¹ : Group G
inst✝ : IsCyclic (G ⧸ center G)
⊢ IsMulCommutative G

Tactic:
by
  simp [(QuotientGroup.mk' <| .center G).isMulCommutative_of_isCyclic_of_ker_le_center]

Goal state after:
Module: Mathlib.GroupTheory.Torsion

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : Group G
N : Subgroup G
inst✝ : Group H
f : G →* H
hN : N = f.ker
tH : IsMulTorsion H
tN : IsMulTorsion ↥N
g : G
ngn : ℕ
ngnpos : 0 < ngn
hngn : f g ^ ngn = 1
gn : ↥N
h : ↑gn = g ^ ngn
hmem : ↑gn ∈ f.ker
nn : ℕ
nnpos : 0 < nn
hnn : gn ^ nn = 1
⊢ IsOfFinOrder g

Tactic:
exact isOfFinOrder_iff_pow_eq_one.mpr <| ⟨ngn * nn, mul_pos ngnpos nnpos, by
    rw [pow_mul, ← h, ← Subgroup.coe_pow, hnn, Subgroup.coe_one]⟩

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

Goal state before:
pp: G : Type u_2
inst✝ : AddGroup G
g : G
hg : ∀ (x : G), x ∈ zmultiples g
n : ℕ
hn : Nat.card G = n
i : ℤ
⊢ (i - (i - ↑n * (i / ↑n))) • g = 0

Tactic:
Int.sub_sub_self,

Goal state after:
G : Type u_2
inst✝ : AddGroup G
g : G
hg : ∀ (x : G), x ∈ zmultiples g
n : ℕ
hn : Nat.card G = n
i : ℤ
⊢ (↑n * (i / ↑n)) • g = 0
Module: Mathlib.GroupTheory.Torsion

Goal state before:
pp: G : Type u_1
inst✝ : CommMonoid G
tG : IsMulTorsion G
⊢ torsion G = ⊤

Tactic:
by ext; tauto

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

Goal state before:
pp: G : Type u_2
inst✝¹ : Infinite G
inst✝ : Group G
g : G
hg : zpowers g = ⊤
⊢ ((zpowersHom G) g).ker = ⊥

Tactic:
simp [zpowersHom_ker_eq, ← infinite_zpowers, hg, Set.infinite_univ]

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝¹ : Group G
H : Subgroup G
inst✝ : Finite ↑↑H
x : G
hx : ↑x ∈ MulAction.fixedPoints (↥H) (G ⧸ H)
ha : ∀ {y : G ⧸ H}, y ∈ orbit ↥H ↑x → y = ↑x
n : G
hn : n ∈ H
this : x⁻¹ * n * x ∈ H
⊢ x⁻¹⁻¹ = x

Tactic:
rw [inv_inv]

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

Goal state before:
pp: case inr.inr
M : Type u_4
N : Type u_5
inst✝³ : CommGroup M
inst✝² : Group N
f : M →* N
h : (Nat.card ↥f.ker).Coprime (Nat.card ↥f.range)
inst✝¹ : IsCyclic ↥f.ker
inst✝ : IsCyclic ↥f.range
h✝¹ : Finite ↥f.ker
h✝ : Finite ↥f.range
⊢ IsCyclic M

Tactic:
have := f.finite_iff_finite_ker_range.mpr ⟨‹_›, ‹_›⟩

Goal state after:
case inr.inr
M : Type u_4
N : Type u_5
inst✝³ : CommGroup M
inst✝² : Group N
f : M →* N
h : (Nat.card ↥f.ker).Coprime (Nat.card ↥f.range)
inst✝¹ : IsCyclic ↥f.ker
inst✝ : IsCyclic ↥f.range
h✝¹ : Finite ↥f.ker
h✝ : Finite ↥f.range
this : Finite M
⊢ IsCyclic M