mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

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

Tactic:
by

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
⊢ ∃ a, (toPiLocalization R) a = x

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
inst✝ : DiscreteTopology (PrimeSpectrum R)
⊢ Function.Surjective ⇑(MaximalSpectrum.toPiLocalization R)

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x y : PrimeSpectrum R
⊢ x ≤ y ↔ y ∈ closure {x}

Tactic:
by

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

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

Tactic:
by

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
x y : PrimeSpectrum R
h : x ⤳ y
⊢ ∀ (y_1 : ↥y.asIdeal.primeCompl), IsUnit ((algebraMap R (Localization.AtPrime x.asIdeal)) ↑y_1)

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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
Z : Set (PrimeSpectrum S)
hZ : IsClosed Z
hf : StableUnderSpecialization (comap f '' Z)
⊢ IsClosed (comap f '' Z)

Tactic:
by

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
hf : StableUnderSpecialization (Set.range (comap f))
⊢ IsClosed (Set.range (comap f))

Tactic:
by

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

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

Tactic:
by

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
h₁ : Function.Surjective (comap f)
h₂ : SpecializingMap (comap f)
⊢ IsQuotientMap (comap f)

Tactic:
by

Goal state after:
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 ∈ H
⊢ x ∈ ⊥

Tactic:
by

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
h₁ : Function.Surjective (comap f)
h₂ : GeneralizingMap (comap f)
⊢ IsQuotientMap (comap f)

Tactic:
by

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
⊢ vanishingIdeal (Set.range (comap f)) = (RingHom.ker f).radical

Tactic:
by

Goal state after:
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 ∈ ⊥
⊢ x ∈ H

Tactic:
by

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
⊢ closure (Set.range (comap f)) = zeroLocus ↑(RingHom.ker f)

Tactic:
by

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
⊢ DenseRange (comap f) ↔ RingHom.ker f ≤ nilradical R

Tactic:
by

Goal state after:
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
⊢ IsCyclic ↥H

Tactic:
by

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
g : G
n : ℕ
h : zpowers (g ^ ↑n) ≤ zpowers g
⊢ zpowers (g ^ ↑n) = zpowers (g ^ n)

Tactic:
by

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
g : G
n : ℕ
h : zpowers (g ^ (-↑n)) ≤ zpowers g
⊢ zpowers (g ^ (-↑n)) = zpowers (g ^ n)

Tactic:
by

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
g : G
H : Subgroup G
⊢ H ≤ zpowers g ↔ ∃ n, H = zpowers (g ^ n)

Tactic:
by

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
H : DenseRange (comap f)
I : Ideal R
hI : I ∈ minimalPrimes R
⊢ I ∈ (RingHom.ker f).minimalPrimes

Tactic:
by

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
⊢ DenseRange (comap f) ↔ ∀ (I : Ideal R) (h : I ∈ minimalPrimes R), { asIdeal := I, isPrime := ⋯ } ∈ Set.range (comap f)

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x : PrimeSpectrum R
⊢ StableUnderGeneralization {x} ↔ x.asIdeal ∈ minimalPrimes R

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Monoid G
x y : G
h : Commute x y
hx : orderOf x ≠ 0
hy : orderOf y ≠ 0
⊢ orderOf
      (x ^ (orderOf x / (orderOf x).factorizationLCMLeft (orderOf y)) *
        y ^ (orderOf y / (orderOf x).factorizationLCMRight (orderOf y))) =
    (orderOf x).lcm (orderOf y)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
x : α
hx : x ∈ {a | a ^ n = 1}
m : ℕ
hm : g ^ m = x
⊢ g ^ (m * n.gcd (Fintype.card α)) = 1

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
⊢ #{a | a ^ n = 1} ≤ #(↑(zpowers (g ^ (Fintype.card α / n.gcd (Fintype.card α))))).toFinset

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Monoid G
x y : G
h : Commute x y
hx : orderOf x = 0
hy : orderOf y = 0
⊢ x ∈ {x, y}

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Monoid G
x y : G
h : Commute x y
hx : orderOf x = 0
hy : orderOf y = 0
⊢ orderOf x = (orderOf x).lcm (orderOf y)

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s✝ : Set (PrimeSpectrum R)
x✝ : ∃ t, (zeroLocus ↑t)ᶜ = s✝
s : Finset R
e : (zeroLocus ↑s)ᶜ = s✝
⊢ s✝ = (zeroLocus ↑s)ᶜ

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
⊢ IsCompact s ∧ IsOpen s ↔ ∃ t, (zeroLocus ↑t)ᶜ = s

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Monoid G
x y : G
h : Commute x y
hx : orderOf x = 0
hy : ¬orderOf y = 0
⊢ x ∈ {x, y}

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Monoid G
x y : G
h : Commute x y
hx : orderOf x = 0
hy : ¬orderOf y = 0
⊢ orderOf x = (orderOf x).lcm (orderOf y)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Monoid G
x y : G
h : Commute x y
hx : ¬orderOf x = 0
hy : orderOf y = 0
⊢ y ∈ {x, y}

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Monoid G
x y : G
h : Commute x y
hx : ¬orderOf x = 0
hy : orderOf y = 0
⊢ orderOf y = (orderOf x).lcm (orderOf y)

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
m : ℕ
hm : Fintype.card α = n.gcd (Fintype.card α) * m
hm0 : m = 0
⊢ False

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Monoid G
x y : G
h : Commute x y
hx : ¬orderOf x = 0
hy : ¬orderOf y = 0
⊢ x ∈ {x, y}

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Monoid G
x y : G
h : Commute x y
hx : ¬orderOf x = 0
hy : ¬orderOf y = 0
⊢ y ∈ {x, y}

Tactic:
by

Goal state after:
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:
by

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Monoid G
x y : G
h : Commute x y
⊢ ∃ z ∈ closure {x, y}, orderOf z = (orderOf x).lcm (orderOf y)

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
⊢ IsCompact s ∧ IsOpen s ↔ ∃ I, I.FG ∧ (zeroLocus ↑I)ᶜ = s

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
e f : R
mul : e * f = 0
add : e + f = 1
p : PrimeSpectrum R
this : e ∉ p.asIdeal ↔ f ∈ p.asIdeal
⊢ p ∈ ↑(basicOpen e) ↔ p ∈ zeroLocus {f}

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
e f : R
mul : e * f = 0
add : e + f = 1
⊢ ↑(basicOpen e) = zeroLocus {f}

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u_1
inst✝¹ : Monoid G
inst✝ : Nontrivial G
p : ℕ
hp : Nat.Prime p
⊢ exponent G = p ↔ ∀ (g : G), g ≠ 1 → orderOf g = p

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
e f : R
mul : e * f = 0
add : e + f = 1
⊢ zeroLocus {e} = ↑(basicOpen f)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
t : Finset ℕ
ht : ↑t = Set.range orderOf
exponent_ne_zero_iff_range_orderOf_finite : (∀ (g : G), 0 < orderOf g) → (exponent G ≠ 0 ↔ (↑t).Finite)
⊢ 0 < t.prod id

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
⊢ #(↑(zpowers (g ^ (Fintype.card α / n.gcd (Fintype.card α))))).toFinset ≤ n

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : Group α
inst✝¹ : Finite α
inst✝ : IsCyclic α
⊢ ∃ x, ∀ (y : α), y ∈ Submonoid.powers x

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
t : Finset ℕ
ht : ↑t = Set.range orderOf
exponent_ne_zero_iff_range_orderOf_finite : (∀ (g : G), 0 < orderOf g) → (exponent G ≠ 0 ↔ (↑t).Finite)
htpos : 0 < t.prod id
this : exponent G ∣ t.prod id
⊢ exponent G ≠ 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
h : IsCyclic α
⊢ ∃ g, orderOf g = Nat.card α

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x : R
hx : x ∈ {e | IsIdempotentElem e}
y : R
hy : y ∈ {e | IsIdempotentElem e}
eq : basicOpen x = basicOpen y
ne : x ≠ y
ne' : x * y ≠ x
mem : x ∈ Ideal.span {y}
⊢ x * y = x

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
⊢ exponent G ≠ 0 ↔ (Set.range orderOf).Finite

Tactic:
by

Goal state after:
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
⊢ ↑⋯.choose = 1

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
⊢ exponent G = 0 ↔ (Set.range orderOf).Infinite

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x : R
hx : x ∈ {e | IsIdempotentElem e}
y : R
hy : y ∈ {e | IsIdempotentElem e}
eq : basicOpen x = basicOpen y
⊢ x = y

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝¹ : Monoid G
H : Type u_1
inst✝ : Monoid H
e : G →* H
e_inj : Function.Injective ⇑e
g : G
⊢ e (g ^ exponent H) = e 1

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Monoid G
S : Submonoid G
g : G
g_in_s : g ∈ S
⊢ g ^ exponent ↥S = 1

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝¹ : LeftCancelMonoid G
inst✝ : Finite G
⊢ ExponentExists G

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝² : LeftCancelMonoid G
inst✝¹ : Finite G
inst✝ : Nontrivial G
⊢ 1 < exponent G

Tactic:
by

Goal state after:
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
⊢ ↑⋯.choose = ↑⋯.choose * ↑⋯.choose

Tactic:
by

Goal state after:
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
⊢ (Set.range orderOf).Finite

Tactic:
by

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

Goal state before:
pp: G : Type u_2
inst✝³ : Group G
M : Type u_4
inst✝² : Monoid M
inst✝¹ : IsCyclic G
inst✝ : MulDistribMulAction M G
n : ℕ
hn : Nat.card G = n
m : M
g : G
k : ℤ
h : (toMonoidHomZModOfIsCyclic G M hn) m = ↑k
⊢ m • g = g ^ k

Tactic:
by

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
h✝ : Nontrivial R
I : Ideal R
hI : I.FG
J : Ideal R
hJ : J.FG
hI' : zeroLocus ↑I = sᶜ
hJ' : zeroLocus ↑J = s
⊢ I * J ≤ nilradical R

Tactic:
by

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

Goal state before:
pp: α : Type u_1
a : α
inst✝¹ : Group α
inst✝ : Fintype α
ha : ∀ (x : α), x ∈ zpowers a
x : α
⊢ ∃! n, x = a ^ n.val

Tactic:
by

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

Goal state before:
pp: α : Type u_1
a : α
inst✝² : Group α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
ha : ∀ (x : α), x ∈ zpowers a
⊢ image (fun i ↦ a ^ i) (range (orderOf a)) = univ

Tactic:
by

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
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 * J) ^ n ≤ 0
⊢ n ≠ 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
a : α
inst✝² : Group α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
ha : ∀ (x : α), x ∈ zpowers a
⊢ image (fun i ↦ a ^ i) (range (Nat.card α)) = univ

Tactic:
by

Goal state after:
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 : orderOf t < orderOf (t ^ p ^ k * g)
⊢ False

Tactic:
by

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

Goal state before:
pp: G : Type u_2
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsCyclic G
d : ℕ
a b : ZMod d
hGcard : Nat.card G = d
h : ∀ (t : G), t ^ a.val = t ^ b.val
⊢ a = b

Tactic:
by

Goal state after:
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
hpk : p ^ k ∣ orderOf t
⊢ orderOf (t ^ p ^ k) = orderOf t / p ^ k

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝ : Group G
⊢ IsPGroup p G ↔ ∀ (g : G), ∃ k, orderOf g ∣ p ^ k

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Fact (Nat.Prime p)
g : G
⊢ (∃ k, ∃ k_1 ≤ k, orderOf g = p ^ k_1) → ∃ k, orderOf g = p ^ k

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Fact (Nat.Prime p)
g : G
⊢ ∀ (a : ℕ), orderOf g = p ^ a → ∃ k ≤ a, orderOf g = p ^ k

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Fact (Nat.Prime p)
⊢ IsPGroup p G ↔ ∀ (g : G), ∃ k, orderOf g = p ^ k

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝ : Group G
n : ℕ
hG : Nat.card G ∣ p ^ n
⊢ IsPGroup p G

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
h : IsPGroup 0 G
⊢ Nat.card G ∣ 0 ^ 1

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
⊢ IsPGroup p G ↔ ∃ n, Nat.card G ∣ p ^ n

Tactic:
by

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 : IsPGroup p G
g : G
hg : g ≠ 1
⊢ p ∣ orderOf g

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Subsingleton G
⊢ Nat.card G = p ^ 0

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: G : Type u_1
inst✝ : Group G
g : G
⊢ g ^ 0 ^ 1 = 1

Tactic:
by

Goal state after: