mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
f : R
⊢ basicOpen f = ⊥ ↔ IsNilpotent f

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝³ : CommSemiring R
S : Type v
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
⊢ Set.range (comap (algebraMap R S)) = ↑(basicOpen r)

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝³ : CommSemiring R
S : Type v
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
⊢ IsOpen (Set.range (comap (algebraMap R S)))

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
f : R
⊢ IsCompact ↑(basicOpen f)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Monoid G
⊢ Monoid.exponent Gᵐᵒᵖ = Monoid.exponent G

Tactic:
by

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

Goal state before:
pp: a : ℤ
⊢ (AddSubgroup.zmultiples a).index = a.natAbs

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Monoid G
h : ExponentExists G
g : G
⊢ ∃ n, 0 < n ∧ g ^ n = 1

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
ι : Type u_1
f : ι → R
⊢ ⨆ i, basicOpen (f i) = ⊤ ↔ Ideal.span (Set.range f) = ⊤

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s : Set R
⊢ ⨆ i ∈ s, basicOpen i = ⊤ ↔ Ideal.span s = ⊤

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
inst✝ : Algebra R S
f : R
p : PrimeSpectrum R
h : (basicOpen f).carrier = {p}
⊢ f ∈ p.asIdeal.primeCompl

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Monoid G
⊢ exponent G ≠ 0 ↔ ExponentExists G

Tactic:
by

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 : β
⊢ zmultiples ↑(minimalPeriod (fun x ↦ a +ᵥ x) b) ≤
    comap ((zmultiplesHom ↥(zmultiples a)) ⟨a, ⋯⟩) (stabilizer (↥(zmultiples a)) b)

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
inst✝ : Algebra R S
f : R
p : PrimeSpectrum R
h : (basicOpen f).carrier = {p}
⊢ IsLocalization.AtPrime (Localization.Away f) p.asIdeal

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
a : K
n : ℤ
⊢ D (a ^ n) = n • a ^ (n - 1) • D a

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
A : Type u_2
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Module R M
D✝ D1 D2 : Derivation R A M
r : R
a✝ b✝ : A
D : Derivation R A M
a b : A
⊢ (-↑D) (a * b) = a • (-↑D) b + b • (-↑D) a

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Monoid G
⊢ exponent G = sInf {d | 0 < d ∧ ∀ (x : G), x ^ d = 1}

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
A : Type u_2
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Module R M
D D1✝ D2✝ : Derivation R A M
r : R
a✝ b✝ : A
D1 D2 : Derivation R A M
a b : A
⊢ (↑D1 - ↑D2) (a * b) = a • (↑D1 - ↑D2) b + b • (↑D1 - ↑D2) a

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Monoid G
⊢ exponent G = 0 ↔ ∀ n > 0, ∃ g, g ^ n ≠ 1

Tactic:
by

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

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Monoid G
g : G
⊢ g ^ exponent G = 1

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Monoid G
n : ℕ
g : G
⊢ g ^ n = g ^ (n % exponent G + exponent G * (n / exponent G))

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
c : R
⊢ (range (comap (algebraMap R[X] (Away c)[X])))ᶜ = range (comap (mapRingHom (Ideal.Quotient.mk (Ideal.span {c}))))

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Monoid G
n : ℕ
g : G
⊢ g ^ (n % exponent G + exponent G * (n / exponent G)) = g ^ (n % exponent G)

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
i j : R
⊢ IsCompact (↑(basicOpen i) ∩ ↑(basicOpen j))

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: case refine_1
ι : Type u_1
R : ι → Type u_2
inst✝¹ : (i : ι) → CommRing (R i)
inst✝ : DecidableEq ι
i : ι
f : R i
p : PrimeSpectrum ((i : ι) → R i)
⊢ p ∈ comap (Pi.evalRingHom R i) '' ↑(basicOpen f) → p ∈ ↑(basicOpen (Pi.single i f))

Tactic:
rintro ⟨p, hp, rfl⟩
    simpa

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
⊢ IsCyclic α ↔ ∃ g, zpowers g = ⊤

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
H : Subgroup α
⊢ IsCyclic ↥H ↔ ∃ g, zpowers g = H

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
nc : ¬IsCyclic α
⊢ Nontrivial α

Tactic:
by

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
⊢ ∃ m, ∀ (g : G), σ g = g ^ m

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Monoid G
n : ℕ
hpos : 0 < n
hG : ∀ (g : G), g ^ n = 1
⊢ exponent G ≤ n

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Monoid G
m : ℕ
hpos : 0 < m
hm : m < exponent G
⊢ ∃ g, g ^ m ≠ 1

Tactic:
by

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

Goal state before:
pp: α : Type u_5
β : Type u_6
inst✝¹ : AddGroup α
a : α
inst✝ : AddAction α β
b : β
k : ℤ
⊢ (orbitZMultiplesEquiv a b).symm ↑k = k • ⟨a, ⋯⟩ +ᵥ ⟨b, ⋯⟩

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Group α
inst✝ : Finite α
⊢ IsCyclic α ↔ ∃ g, Nat.card α ≤ orderOf g

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case a_eq_b
G : Type u
inst✝ : Monoid G
eq_one : exponent G = 1
a b : G
⊢ a ^ 1 = b

Tactic:
← pow_one b,

Goal state after:
case a_eq_b
G : Type u
inst✝ : Monoid G
eq_one : exponent G = 1
a b : G
⊢ a ^ 1 = b ^ 1
Module: Mathlib.Data.ZMod.QuotientGroup

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝² : Group α
a : α
inst✝¹ : MulAction α β
b : β
inst✝ : Fintype ↑(orbit (↥(zpowers a)) b)
⊢ minimalPeriod (fun x ↦ a • x) b = Fintype.card ↑(orbit (↥(zpowers a)) b)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Monoid G
⊢ exponent G = 1 ↔ Subsingleton G

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Monoid G
n : ℕ
⊢ exponent G ∣ n ↔ ∀ (g : G), g ^ n = 1

Tactic:
rcases n.eq_zero_or_pos with (rfl | hpos)

Goal state after:
case inl
G : Type u
inst✝ : Monoid G
⊢ exponent G ∣ 0 ↔ ∀ (g : G), g ^ 0 = 1

case inr
G : Type u
inst✝ : Monoid G
n : ℕ
hpos : n > 0
⊢ exponent G ∣ n ↔ ∀ (g : G), g ^ n = 1
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:
by

Goal state after:
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:
by
  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: ι : Type u_1
R : ι → Type u_2
inst✝¹ : (i : ι) → CommRing (R i)
inst✝ : DecidableEq ι
i : ι
f : R i
p : PrimeSpectrum ((i : ι) → R i)
hp : p ∈ ↑(basicOpen (Pi.single i f))
x : (i : ι) → R i
hx : x i = 0
⊢ Pi.single i f * x = 0

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
inst✝¹ : (i : ι) → CommRing (R i)
inst✝ : DecidableEq ι
i : ι
f : R i
p : PrimeSpectrum ((i : ι) → R i)
hp : p ∈ ↑(basicOpen (Pi.single i f))
⊢ p ∈ Set.range (comap (Pi.evalRingHom R i))

Tactic:
by

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
p : ℕ
hp : Fact (Nat.Prime p)
h : Nat.card G = p
g : G
hg : g ≠ 1
⊢ zpowers g = ⊤

Tactic:
by

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✝² : Group α
a : α
inst✝¹ : MulAction α β
b : β
inst✝ : Finite ↑(orbit (↥(zpowers a)) b)
⊢ minimalPeriod (fun x ↦ a • x) b ≠ 0

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
inst✝¹ : (i : ι) → CommRing (R i)
inst✝ : DecidableEq ι
i : ι
f : R i
q : PrimeSpectrum (R i)
hp : comap (Pi.evalRingHom R i) q ∈ ↑(basicOpen (Pi.single i f))
⊢ q ∈ ↑(basicOpen f)

Tactic:
by

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
p : ℕ
hp : Fact (Nat.Prime p)
h : Nat.card G = p
g g' : G
hg : g ≠ 1
⊢ g' ∈ zpowers g

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
inst✝¹ : (i : ι) → CommRing (R i)
inst✝ : DecidableEq ι
i : ι
f : R i
q : PrimeSpectrum (R i)
hp : comap (Pi.evalRingHom R i) q ∈ ↑(basicOpen (Pi.single i f))
⊢ comap (Pi.evalRingHom R i) q = comap (Pi.evalRingHom R i) q

Tactic:
by

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
p : ℕ
hp : Fact (Nat.Prime p)
h : Nat.card G = p
g g' : G
hg : g ≠ 1
⊢ g' ∈ Submonoid.powers g

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
inst✝¹ : (i : ι) → CommRing (R i)
inst✝ : DecidableEq ι
i : ι
f : R i
⊢ comap (Pi.evalRingHom R i) '' ↑(basicOpen f) = ↑(basicOpen (Pi.single i f))

Tactic:
by

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

Goal state before:
pp: α : Type u_3
inst✝ : Group α
a : α
⊢ Nat.card ↥(zpowers a) = orderOf a

Tactic:
by

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
p : ℕ
hp : Fact (Nat.Prime p)
h : Nat.card G = p
g : G
hg : g ≠ 1
⊢ Submonoid.powers g = ⊤

Tactic:
by

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

Goal state before:
pp: α : Type u_3
inst✝ : Group α
a : α
⊢ (↑(zpowers a)).Finite ↔ IsOfFinOrder a

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
inst✝¹ : (i : ι) → CommRing (R i)
inst✝ : DecidableEq ι
i : ι
f : R i
⊢ sigmaToPi R '' Sigma.mk i '' ↑(basicOpen f) = ↑(basicOpen (Pi.single i f))

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
p : ℕ
hp : Fact (Nat.Prime p)
h : Nat.card α = p
⊢ IsCyclic α

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
p : ℕ
hp : Fact (Nat.Prime p)
h : Nat.card α ∣ p
⊢ IsCyclic α

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Monoid G
n : ℕ
hpos : n > 0
hG : ∀ (g : G), g ^ n = 1
h : 0 < n % exponent G
h₂ : n % exponent G < exponent G
⊢ exponent G ≤ n % exponent G

Tactic:
by

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

Goal state before:
pp: G : Type u_3
inst✝ : Group G
H : Subgroup G
g : G
q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)
k : ℤ
⊢ (H.quotientEquivSigmaZMod g) (g ^ k • Quotient.out q) = ⟨q, ↑k⟩

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Monoid G
n : ℕ
⊢ exponent G ∣ n ↔ ∀ (g : G), g ^ n = 1

Tactic:
by

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

Goal state before:
pp: G : Type u_2
G' : Type u_3
inst✝³ : Group G
inst✝² : Group G'
F : Type u_4
hH : IsCyclic G'
inst✝¹ : FunLike F G' G
inst✝ : MonoidHomClass F G' G
f : F
hf : Function.Surjective ⇑f
⊢ IsCyclic G

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Monoid G
n : ℕ
⊢ exponent G ∣ n ↔ ∀ (g : G), orderOf g ∣ n

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
f : PrimeSpectrum R → R
hf : ∀ (p : PrimeSpectrum R), ↑(basicOpen (f p)) = {p}
e : PrimeSpectrum R ≃ ↑(Set.range f) := Equiv.ofInjective f ⋯
a : ↑(Set.range f)
⊢ IsLocalization.Away (f (e.symm a)) (Localization.Away ↑a)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
g : α
hx : ∀ (x : α), x ∈ zpowers g
⊢ orderOf g = Nat.card α

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝¹ : Monoid G
inst✝ : Fintype G
⊢ Finset.univ.lcm orderOf ∣ exponent G

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
g : α
hx : ∀ (x : α), x ∈ Submonoid.powers g
⊢ orderOf g = Nat.card α

Tactic:
by

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 = p ^ (exponent G).factorization p

Tactic:
by

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

Goal state before:
pp: G : Type u_3
inst✝² : Group G
H : Subgroup G
g : G
inst✝¹ : Finite (G ⧸ H)
inst✝ : Fintype (Quotient (orbitRel (↥(zpowers g)) (G ⧸ H)))
this✝ : Fintype (G ⧸ H)
this : (q : Quotient (orbitRel (↥(zpowers g)) (G ⧸ H))) → Fintype ↑(orbit (↥(zpowers g)) q.out)
⊢ Fintype.card (G ⧸ H) = Fintype.card ((x : Quotient (orbitRel (↥(zpowers g)) (G ⧸ H))) × ↑(orbit (↥(zpowers g)) x.out))

Tactic:
exact Fintype.card_congr (MulAction.selfEquivSigmaOrbits (zpowers g) (G ⧸ H))

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

Goal state before:
pp: G : Type u_3
inst✝² : Group G
H : Subgroup G
g : G
inst✝¹ : Finite (G ⧸ H)
inst✝ : Fintype (Quotient (orbitRel (↥(zpowers g)) (G ⧸ H)))
⊢ H.index = ∑ q, minimalPeriod (fun x ↦ g • x) q.out

Tactic:
by

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
G_cyclic : IsCyclic G
k : ℕ
k_pos : k ≠ 0
k_lt_card_G : k < Nat.card G
⊢ ∃ a, a ^ k ≠ 1

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
f : PrimeSpectrum R → R
hf : ∀ (p : PrimeSpectrum R), ↑(basicOpen (f p)) = {p}
e : PrimeSpectrum R ≃ ↑(Set.range f) := Equiv.ofInjective f ⋯
loc : ∀ (a : ↑(Set.range f)), IsLocalization.AtPrime (Localization.Away ↑a) (e.symm a).asIdeal
algE : (a : ↑(Set.range f)) → Localization.AtPrime (e.symm a).asIdeal ≃ₐ[R] Localization.Away ↑a :=
  fun a ↦
    IsLocalization.algEquiv (e.symm a).asIdeal.primeCompl (Localization.AtPrime (e.symm a).asIdeal)
      (Localization.Away ↑a)
span_eq : Ideal.span (Set.range f) = ⊤
a : ↑(Set.range f)
⊢ ↑(basicOpen ↑a) = {e.symm a}

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Group α
inst✝ : Infinite α
g : α
h : ∀ (x : α), x ∈ zpowers g
⊢ orderOf g = 0

Tactic:
by

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
ht : exponent G = ⊥
⊢ False

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Subgroup.Simple

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ IsSimpleGroup ↥H ↔ H ≠ ⊥ ∧ ∀ H' ≤ H, (H'.subgroupOf H).Normal → H' = ⊥ ∨ H' = H

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Subgroup.Simple

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
H✝ : Type u_3
inst✝² : Group H✝
inst✝¹ : IsSimpleGroup G
inst✝ : Nontrivial H✝
f : G →* H✝
hf : Function.Surjective ⇑f
H : Subgroup H✝
iH : H.Normal
⊢ H = ⊥ ∨ H = ⊤

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
h : k.natAbs = 0
⊢ x = 1

Tactic:
by

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 : p ∈ (exponent G).factorization.support
he : 0 < exponent G
key : ¬exponent G ∣ exponent G / p
⊢ ∃ g, g ^ (exponent G / p) ≠ 1

Tactic:
by

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 : p ∈ (exponent G).factorization.support
he : 0 < exponent G
⊢ ∃ g, g ^ (exponent G / p) ≠ 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
⊢ g ^ k.natAbs ∈ H

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
f : PrimeSpectrum R → R
hf✝ : ∀ (p : PrimeSpectrum R), ↑(basicOpen (f p)) = {p}
e : PrimeSpectrum R ≃ ↑(Set.range f) := Equiv.ofInjective f ⋯
loc : ∀ (a : ↑(Set.range f)), IsLocalization.AtPrime (Localization.Away ↑a) (e.symm a).asIdeal
algE : (a : ↑(Set.range f)) → Localization.AtPrime (e.symm a).asIdeal ≃ₐ[R] Localization.Away ↑a :=
  fun a ↦
    IsLocalization.algEquiv (e.symm a).asIdeal.primeCompl (Localization.AtPrime (e.symm a).asIdeal)
      (Localization.Away ↑a)
span_eq : Ideal.span (Set.range f) = ⊤
hf : ∀ (a : ↑(Set.range f)), ↑(basicOpen ↑a) = {e.symm a}
a b : ↑(Set.range f)
ne : a ≠ b
⊢ basicOpen (↑a * ↑b) = ⊥

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
f : PrimeSpectrum R → R
hf✝ : ∀ (p : PrimeSpectrum R), ↑(basicOpen (f p)) = {p}
e : PrimeSpectrum R ≃ ↑(Set.range f) := Equiv.ofInjective f ⋯
loc : ∀ (a : ↑(Set.range f)), IsLocalization.AtPrime (Localization.Away ↑a) (e.symm a).asIdeal
algE : (a : ↑(Set.range f)) → Localization.AtPrime (e.symm a).asIdeal ≃ₐ[R] Localization.Away ↑a :=
  fun a ↦
    IsLocalization.algEquiv (e.symm a).asIdeal.primeCompl (Localization.AtPrime (e.symm a).asIdeal)
      (Localization.Away ↑a)
span_eq : Ideal.span (Set.range f) = ⊤
hf : ∀ (a : ↑(Set.range f)), ↑(basicOpen ↑a) = {e.symm a}
a b : ↑(Set.range f)
⊢ (IsLocalization.Away.awayToAwayRight ↑a ↑b) ((algE a) (x (e.symm a))) =
    (IsLocalization.Away.awayToAwayLeft ↑b ↑a) ((algE b) (x (e.symm b)))

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
⊢ g ^ (↑(Nat.find hex) * (k / ↑(Nat.find hex))) ∈ H

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Exponent

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

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
⊢ g ^ (k % ↑(Nat.find hex)) * g ^ (↑(Nat.find hex) * (k / ↑(Nat.find hex))) ∈ H

Tactic:
by

Goal state after: