mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case hfin
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
hg : g ^ (exponent G / p) ≠ 1
k : ℕ
hk : exponent G = p ^ (exponent G).factorization p * k
t : ℕ
ht : (exponent G).factorization p = t.succ
⊢ (g ^ k) ^ p ^ (t + 1) = 1

Tactic:
·

Goal state after:
case hfin
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
hg : g ^ (exponent G / p) ≠ 1
k : ℕ
hk : exponent G = p ^ (exponent G).factorization p * k
t : ℕ
ht : (exponent G).factorization p = t.succ
⊢ (g ^ k) ^ p ^ (t + 1) = 1
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
I : Ideal S
hZ : IsClosed (zeroLocus ↑I)
hf : StableUnderSpecialization (comap f '' zeroLocus ↑I)
⊢ comap f '' zeroLocus ↑I ⊆ zeroLocus ↑(Ideal.comap f I)

pp: case refine_2
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
I : Ideal S
hZ : IsClosed (zeroLocus ↑I)
hf : StableUnderSpecialization (comap f '' zeroLocus ↑I)
p : PrimeSpectrum R
hp : p ∈ zeroLocus ↑(Ideal.comap f I)
⊢ p ∈ comap f '' zeroLocus ↑I

Tactic:
·

Goal state after:
case refine_1
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
I : Ideal S
hZ : IsClosed (zeroLocus ↑I)
hf : StableUnderSpecialization (comap f '' zeroLocus ↑I)
⊢ comap f '' zeroLocus ↑I ⊆ zeroLocus ↑(Ideal.comap f I)
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
I : Ideal S
hZ : IsClosed (zeroLocus ↑I)
hf : StableUnderSpecialization (comap f '' zeroLocus ↑I)
p : PrimeSpectrum R
hp : p ∈ zeroLocus ↑(Ideal.comap f I)
⊢ p ∈ comap f '' zeroLocus ↑I

Tactic:
·

Goal state after:
case refine_2
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
I : Ideal S
hZ : IsClosed (zeroLocus ↑I)
hf : StableUnderSpecialization (comap f '' zeroLocus ↑I)
p : PrimeSpectrum R
hp : p ∈ zeroLocus ↑(Ideal.comap f I)
⊢ p ∈ comap f '' zeroLocus ↑I
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case mp
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)

pp: case mpr
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
⊢ (∀ (I : Ideal R) (h : I ∈ minimalPrimes R), { asIdeal := I, isPrime := ⋯ } ∈ Set.range (comap f)) →
    DenseRange (comap f)

Tactic:
·

Goal state after:
case mp
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)
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

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

pp: case refine_2
G : Type u_2
inst✝ : Group G
g : G
H : Subgroup G
⊢ (∃ n, H = zpowers (g ^ n)) → H ≤ zpowers g

Tactic:
·

Goal state after:
case refine_1
G : Type u_2
inst✝ : Group G
g : G
H : Subgroup G
h : H ≤ zpowers g
⊢ ∃ n, H = zpowers (g ^ n)
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: case refine_1.inl
G : Type u_2
inst✝ : Group G
g : G
n : ℕ
h : zpowers (g ^ ↑n) ≤ zpowers g
⊢ ∃ n_1, zpowers (g ^ ↑n) = zpowers (g ^ n_1)

pp: case refine_1.inr
G : Type u_2
inst✝ : Group G
g : G
n : ℕ
h : zpowers (g ^ (-↑n)) ≤ zpowers g
⊢ ∃ n_1, zpowers (g ^ (-↑n)) = zpowers (g ^ n_1)

Tactic:
·

Goal state after:
case refine_1.inl
G : Type u_2
inst✝ : Group G
g : G
n : ℕ
h : zpowers (g ^ ↑n) ≤ zpowers g
⊢ ∃ n_1, zpowers (g ^ ↑n) = zpowers (g ^ n_1)
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: case refine_1.inr
G : Type u_2
inst✝ : Group G
g : G
n : ℕ
h : zpowers (g ^ (-↑n)) ≤ zpowers g
⊢ ∃ n_1, zpowers (g ^ (-↑n)) = zpowers (g ^ n_1)

Tactic:
·

Goal state after:
case refine_1.inr
G : Type u_2
inst✝ : Group G
g : G
n : ℕ
h : zpowers (g ^ (-↑n)) ≤ zpowers g
⊢ ∃ n_1, zpowers (g ^ (-↑n)) = zpowers (g ^ n_1)
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

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

Tactic:
·

Goal state after:
case refine_2
G : Type u_2
inst✝ : Group G
g : G
H : Subgroup G
⊢ (∃ n, H = zpowers (g ^ n)) → H ≤ zpowers g
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case mpr
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
⊢ (∀ (I : Ideal R) (h : I ∈ minimalPrimes R), { asIdeal := I, isPrime := ⋯ } ∈ Set.range (comap f)) →
    DenseRange (comap f)

Tactic:
·

Goal state after:
case mpr
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
⊢ (∀ (I : Ideal R) (h : I ∈ minimalPrimes R), { asIdeal := I, isPrime := ⋯ } ∈ Set.range (comap f)) →
    DenseRange (comap f)
Module: Mathlib.GroupTheory.Exponent

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

pp: case neg
G : Type u
inst✝ : Monoid G
x y : G
h : Commute x y
hx : orderOf x = 0
hy : ¬orderOf y = 0
⊢ ∃ z ∈ closure {x, y}, orderOf z = (orderOf x).lcm (orderOf y)

pp: case pos
G : Type u
inst✝ : Monoid G
x y : G
h : Commute x y
hx : ¬orderOf x = 0
hy : orderOf y = 0
⊢ ∃ z ∈ closure {x, y}, orderOf z = (orderOf x).lcm (orderOf y)

pp: case neg
G : Type u
inst✝ : Monoid G
x y : G
h : Commute x y
hx : ¬orderOf x = 0
hy : ¬orderOf y = 0
⊢ ∃ z ∈ closure {x, y}, orderOf z = (orderOf x).lcm (orderOf y)

Tactic:
·

Goal state after:
case pos
G : Type u
inst✝ : Monoid G
x y : G
h : Commute x y
hx : orderOf x = 0
hy : orderOf y = 0
⊢ ∃ z ∈ closure {x, y}, orderOf z = (orderOf x).lcm (orderOf y)
Module: Mathlib.GroupTheory.Exponent

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

pp: case pos
G : Type u
inst✝ : Monoid G
x y : G
h : Commute x y
hx : ¬orderOf x = 0
hy : orderOf y = 0
⊢ ∃ z ∈ closure {x, y}, orderOf z = (orderOf x).lcm (orderOf y)

pp: case neg
G : Type u
inst✝ : Monoid G
x y : G
h : Commute x y
hx : ¬orderOf x = 0
hy : ¬orderOf y = 0
⊢ ∃ z ∈ closure {x, y}, orderOf z = (orderOf x).lcm (orderOf y)

Tactic:
·

Goal state after:
case neg
G : Type u
inst✝ : Monoid G
x y : G
h : Commute x y
hx : orderOf x = 0
hy : ¬orderOf y = 0
⊢ ∃ z ∈ closure {x, y}, orderOf z = (orderOf x).lcm (orderOf y)
Module: Mathlib.GroupTheory.Exponent

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

pp: case neg
G : Type u
inst✝ : Monoid G
x y : G
h : Commute x y
hx : ¬orderOf x = 0
hy : ¬orderOf y = 0
⊢ ∃ z ∈ closure {x, y}, orderOf z = (orderOf x).lcm (orderOf y)

Tactic:
·

Goal state after:
case pos
G : Type u
inst✝ : Monoid G
x y : G
h : Commute x y
hx : ¬orderOf x = 0
hy : orderOf y = 0
⊢ ∃ z ∈ closure {x, y}, orderOf z = (orderOf x).lcm (orderOf y)
Module: Mathlib.GroupTheory.Exponent

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

Tactic:
·

Goal state after:
case neg
G : Type u
inst✝ : Monoid G
x y : G
h : Commute x y
hx : ¬orderOf x = 0
hy : ¬orderOf y = 0
⊢ ∃ z ∈ closure {x, y}, orderOf z = (orderOf x).lcm (orderOf y)
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case refine_1
G : Type u_1
inst✝¹ : Monoid G
inst✝ : Nontrivial G
p : ℕ
hp : Nat.Prime p
hG : exponent G = p
g : G
hg : g ≠ 1
⊢ orderOf g = p

pp: case refine_2
G : Type u_1
inst✝¹ : Monoid G
inst✝ : Nontrivial G
p : ℕ
hp : Nat.Prime p
h : ∀ (g : G), g ≠ 1 → orderOf g = p
⊢ exponent G ∣ p

pp: case refine_3
G : Type u_1
inst✝¹ : Monoid G
inst✝ : Nontrivial G
p : ℕ
hp : Nat.Prime p
h : ∀ (g : G), g ≠ 1 → orderOf g = p
⊢ p ∣ exponent G

Tactic:
·

Goal state after:
case refine_1
G : Type u_1
inst✝¹ : Monoid G
inst✝ : Nontrivial G
p : ℕ
hp : Nat.Prime p
hG : exponent G = p
g : G
hg : g ≠ 1
⊢ orderOf g = p
Module: Mathlib.GroupTheory.Exponent

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

pp: case refine_3
G : Type u_1
inst✝¹ : Monoid G
inst✝ : Nontrivial G
p : ℕ
hp : Nat.Prime p
h : ∀ (g : G), g ≠ 1 → orderOf g = p
⊢ p ∣ exponent G

Tactic:
·

Goal state after:
case refine_2
G : Type u_1
inst✝¹ : Monoid G
inst✝ : Nontrivial G
p : ℕ
hp : Nat.Prime p
h : ∀ (g : G), g ≠ 1 → orderOf g = p
⊢ exponent G ∣ p
Module: Mathlib.GroupTheory.Exponent

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

pp: case neg
G : Type u_1
inst✝¹ : Monoid G
inst✝ : Nontrivial G
p : ℕ
hp : Nat.Prime p
h : ∀ (g : G), g ≠ 1 → orderOf g = p
g : G
hg : ¬g = 1
⊢ orderOf g ∣ p

Tactic:
·

Goal state after:
case pos
G : Type u_1
inst✝¹ : Monoid G
inst✝ : Nontrivial G
p : ℕ
hp : Nat.Prime p
h : ∀ (g : G), g ≠ 1 → orderOf g = p
g : G
hg : g = 1
⊢ orderOf g ∣ p
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
  ext p
  suffices e ∉ p.asIdeal ↔ f ∈ p.asIdeal by simpa
  refine ⟨(p.2.mem_or_mem_of_mul_eq_zero mul).resolve_left, fun h₁ h₂ ↦ p.2.1 ?_⟩
  rw [Ideal.eq_top_iff_one, ← add]
  exact add_mem h₂ h₁

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case neg
G : Type u_1
inst✝¹ : Monoid G
inst✝ : Nontrivial G
p : ℕ
hp : Nat.Prime p
h : ∀ (g : G), g ≠ 1 → orderOf g = p
g : G
hg : ¬g = 1
⊢ orderOf g ∣ p

Tactic:
·

Goal state after:
case neg
G : Type u_1
inst✝¹ : Monoid G
inst✝ : Nontrivial G
p : ℕ
hp : Nat.Prime p
h : ∀ (g : G), g ≠ 1 → orderOf g = p
g : G
hg : ¬g = 1
⊢ orderOf g ∣ p
Module: Mathlib.GroupTheory.Exponent

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

Tactic:
·

Goal state after:
case refine_3
G : Type u_1
inst✝¹ : Monoid G
inst✝ : Nontrivial G
p : ℕ
hp : Nat.Prime p
h : ∀ (g : G), g ≠ 1 → orderOf g = p
⊢ p ∣ exponent G
Module: Mathlib.GroupTheory.Exponent

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

pp: case refine_2
G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
he : (Set.range orderOf).Finite
⊢ exponent G ≠ 0

Tactic:
·

Goal state after:
case refine_1
G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
he : exponent G ≠ 0
⊢ (Set.range orderOf).Finite
Module: Mathlib.GroupTheory.Exponent

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

Tactic:
·

Goal state after:
case refine_2
G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
he : (Set.range orderOf).Finite
⊢ exponent G ≠ 0
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case inr
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
this :
  ∀ x ∈ {e | IsIdempotentElem e}, ∀ y ∈ {e | IsIdempotentElem e}, basicOpen x = basicOpen y → x ≠ y → x * y ≠ x → False
ne' : ¬x * y ≠ x
⊢ False

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
⊢ False

Tactic:
·

Goal state after:
case inr
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
this :
  ∀ x ∈ {e | IsIdempotentElem e}, ∀ y ∈ {e | IsIdempotentElem e}, basicOpen x = basicOpen y → x ≠ y → x * y ≠ x → False
ne' : ¬x * y ≠ x
⊢ False
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

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

Tactic:
use g

Goal state after:
case h
α : Type u_1
inst✝ : Group α
h : IsCyclic α
g : α
hg : ∀ (x : α), x ∈ zpowers g
⊢ orderOf g = Nat.card α
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case inl
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
hs : IsClopen s
h✝ : Subsingleton R
⊢ ∃ e f, e * f = 0 ∧ e + f = 1 ∧ s = ↑(basicOpen e) ∧ sᶜ = ↑(basicOpen f)

pp: case inr
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
hs : IsClopen s
h✝ : Nontrivial R
⊢ ∃ e f, e * f = 0 ∧ e + f = 1 ∧ s = ↑(basicOpen e) ∧ sᶜ = ↑(basicOpen f)

Tactic:
·

Goal state after:
case inl
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
hs : IsClopen s
h✝ : Subsingleton R
⊢ ∃ e f, e * f = 0 ∧ e + f = 1 ∧ s = ↑(basicOpen e) ∧ sᶜ = ↑(basicOpen f)
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case refine_1
G : Type u
inst✝¹ : LeftCancelMonoid G
inst✝ : Finite G
_inst : Fintype G := Fintype.ofFinite G
⊢ 0 < Finset.univ.lcm orderOf

pp: case refine_2
G : Type u
inst✝¹ : LeftCancelMonoid G
inst✝ : Finite G
_inst : Fintype G := Fintype.ofFinite G
g : G
⊢ g ^ Finset.univ.lcm orderOf = 1

Tactic:
·

Goal state after:
case refine_1
G : Type u
inst✝¹ : LeftCancelMonoid G
inst✝ : Finite G
_inst : Fintype G := Fintype.ofFinite G
⊢ 0 < Finset.univ.lcm orderOf
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case refine_2
G : Type u
inst✝¹ : LeftCancelMonoid G
inst✝ : Finite G
_inst : Fintype G := Fintype.ofFinite G
g : G
⊢ g ^ Finset.univ.lcm orderOf = 1

Tactic:
·

Goal state after:
case refine_2
G : Type u
inst✝¹ : LeftCancelMonoid G
inst✝ : Finite G
_inst : Fintype G := Fintype.ofFinite G
g : G
⊢ g ^ Finset.univ.lcm orderOf = 1
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

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

pp: case refine_2
α : Type u_1
a : α
inst✝¹ : Group α
inst✝ : Fintype α
ha : ∀ (x : α), x ∈ zpowers a
n : ℤ
y : ZMod (Fintype.card α)
hy : a ^ n = a ^ y.val
⊢ y = ↑n

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
a : α
inst✝¹ : Group α
inst✝ : Fintype α
ha : ∀ (x : α), x ∈ zpowers a
n : ℤ
⊢ a ^ n = a ^ (↑n).val
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: case refine_2
α : Type u_1
a : α
inst✝¹ : Group α
inst✝ : Fintype α
ha : ∀ (x : α), x ∈ zpowers a
n : ℤ
y : ZMod (Fintype.card α)
hy : a ^ n = a ^ y.val
⊢ y = ↑n

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
a : α
inst✝¹ : Group α
inst✝ : Fintype α
ha : ∀ (x : α), x ∈ zpowers a
n : ℤ
y : ZMod (Fintype.card α)
hy : a ^ n = a ^ y.val
⊢ y = ↑n
Module: Mathlib.GroupTheory.PGroup

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

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

Tactic:
·

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

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

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

Tactic:
·

Goal state after:
case refine_1
p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
h : p ≠ 0
x✝ : ∃ n, Nat.card G ∣ p ^ n
n : ℕ
hn : Nat.card G ∣ p ^ n
⊢ (Nat.card G).primeFactors ⊆ p.primeFactors
Module: Mathlib.GroupTheory.PGroup

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

pp: case refine_1.inr
p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
h : p ≠ 0
x✝ : ∃ n, Nat.card G ∣ p ^ n
n : ℕ
hn : Nat.card G ∣ p ^ n
hn0 : n ≠ 0
⊢ (Nat.card G).primeFactors ⊆ p.primeFactors

Tactic:
·

Goal state after:
case refine_1.inl
p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
h : p ≠ 0
x✝ : ∃ n, Nat.card G ∣ p ^ n
hn : Nat.card G ∣ p ^ 0
⊢ (Nat.card G).primeFactors ⊆ p.primeFactors
Module: Mathlib.GroupTheory.PGroup

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

Tactic:
·

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

Goal state before:
pp: case inl
p : ℕ
G : Type u_1
inst✝ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
h✝ : Finite G
⊢ Nat.card G = 1 ∨ p ∣ Nat.card G

pp: case inr
p : ℕ
G : Type u_1
inst✝ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
h✝ : Infinite G
⊢ Nat.card G = 1 ∨ p ∣ Nat.card G

Tactic:
·

Goal state after:
case inl
p : ℕ
G : Type u_1
inst✝ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
h✝ : Finite G
⊢ Nat.card G = 1 ∨ p ∣ Nat.card G
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: case inl.zero
p : ℕ
G : Type u_1
inst✝ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
h✝ : Finite G
hn : Nat.card G = p ^ 0
⊢ p ^ 0 = 1 ∨ p ∣ p ^ 0

pp: case inl.succ
p : ℕ
G : Type u_1
inst✝ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
h✝ : Finite G
n : ℕ
hn : Nat.card G = p ^ (n + 1)
⊢ p ^ (n + 1) = 1 ∨ p ∣ p ^ (n + 1)

Tactic:
·

Goal state after:
case inl.zero
p : ℕ
G : Type u_1
inst✝ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
h✝ : Finite G
hn : Nat.card G = p ^ 0
⊢ p ^ 0 = 1 ∨ p ∣ p ^ 0
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: case inl.succ
p : ℕ
G : Type u_1
inst✝ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
h✝ : Finite G
n : ℕ
hn : Nat.card G = p ^ (n + 1)
⊢ p ^ (n + 1) = 1 ∨ p ∣ p ^ (n + 1)

Tactic:
·

Goal state after:
case inl.succ
p : ℕ
G : Type u_1
inst✝ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
h✝ : Finite G
n : ℕ
hn : Nat.card G = p ^ (n + 1)
⊢ p ^ (n + 1) = 1 ∨ p ∣ p ^ (n + 1)
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: case inr
p : ℕ
G : Type u_1
inst✝ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
h✝ : Infinite G
⊢ Nat.card G = 1 ∨ p ∣ Nat.card G

Tactic:
·

Goal state after:
case inr
p : ℕ
G : Type u_1
inst✝ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
h✝ : Infinite G
⊢ Nat.card G = 1 ∨ p ∣ Nat.card 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
⊢ (fun x ↦ x ^ n) '' ↑I ⊆ ↑(I ^ n ⊔ J ^ n)

pp: case right
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
⊢ (fun x ↦ x ^ n) '' ↑J ⊆ ↑(I ^ n ⊔ J ^ n)

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:
·

Goal state after:
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
⊢ (fun x ↦ x ^ n) '' ↑I ⊆ ↑(I ^ n ⊔ J ^ n)
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case right
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
⊢ (fun x ↦ x ^ n) '' ↑J ⊆ ↑(I ^ n ⊔ J ^ n)

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:
·

Goal state after:
case right
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
⊢ (fun x ↦ x ^ n) '' ↑J ⊆ ↑(I ^ n ⊔ J ^ n)
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:
·

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 ∪ ↑J) = ⊤
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case h
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
hpk' : orderOf (t ^ p ^ k) = orderOf t / p ^ k
a : ℕ
ha : (exponent G).factorization p = k + a + 1
hcoprime : (orderOf (t ^ p ^ k)).Coprime (orderOf g)
⊢ 1 < p ^ (a + 1)

pp: case h
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
hpk' : orderOf (t ^ p ^ k) = orderOf t / p ^ k
a : ℕ
ha : (exponent G).factorization p = k + a + 1
hcoprime : (orderOf (t ^ p ^ k)).Coprime (orderOf g)
⊢ p ^ (orderOf t).factorization p ∣ orderOf t

Tactic:
·

Goal state after:
case h
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
hpk' : orderOf (t ^ p ^ k) = orderOf t / p ^ k
a : ℕ
ha : (exponent G).factorization p = k + a + 1
hcoprime : (orderOf (t ^ p ^ k)).Coprime (orderOf g)
⊢ 1 < p ^ (a + 1)