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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
⊢ IsPGroup 1 G ↔ Subsingleton G

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.PGroup

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

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝ : Group G
q : ℕ
hpq : p ∣ q
hp : IsPGroup p G
⊢ IsPGroup q G

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝ : Group G
n : ℕ
h : IsPGroup (p ^ n) G
g : G
⊢ ∀ (a : ℕ), g ^ (p ^ n) ^ a = 1 → g ^ p ^ (n * a) = 1

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)
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✝ : Finite G
⊢ IsPGroup p G ↔ ∃ k, ∀ (g : G), 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✝ : Finite G
⊢ IsPGroup p G ↔ ∃ k, ∀ (g : G), g ^ p ^ k = 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, Monoid.exponent 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✝¹ : Finite G
inst✝ : Fact (Nat.Prime p)
⊢ IsPGroup p G ↔ ∃ n, Monoid.exponent 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✝ : Finite G
h : p ≠ 0
⊢ IsPGroup p G ↔ (Nat.card G).primeFactors ⊆ p.primeFactors

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
hG : IsPGroup p G
H : Type u_2
inst✝ : Group H
ϕ : H →* G
hϕ : Function.Injective ⇑ϕ
⊢ IsPGroup p H

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
hG : IsPGroup p G
H : Type u_2
inst✝ : Group H
ϕ : G →* H
hϕ : Function.Surjective ⇑ϕ
⊢ IsPGroup p H

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

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝ : Group G
hG : IsPGroup p G
n : ℕ
hn : p.Coprime n
g : G
⊢ (hG.powEquiv hn).symm g = g ^ (orderOf g).gcdB n

Tactic:
by

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)
H : Subgroup G
inst✝ : H.FiniteIndex
⊢ ∃ n, H.index = p ^ n

Tactic:
by

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)
h✝ : Finite G
n : ℕ
hn : Nat.card G = p ^ (n + 1)
⊢ p ^ (n + 1) = p * p ^ n

Tactic:
by

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)
⊢ Nat.card G = 1 ∨ p ∣ Nat.card G

Tactic:
by

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)
inst✝ : Finite G
hGnt : Nontrivial G
k : ℕ
hk : Nat.card G = p ^ k
hk0 : k = 0
⊢ False

Tactic:
by

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 α
a : α
inst✝ : Finite ↑(orbit G a)
⊢ ∃ n, Nat.card ↑(orbit G a) = p ^ n

Tactic:
let ϕ := orbitEquivQuotientStabilizer G a
  have := Finite.of_equiv (orbit G a) ϕ
  have := (stabilizer G a).finiteIndex_of_finite_quotient
  rw [Nat.card_congr ϕ]
  exact hG.index (stabilizer G a)

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 α
a : α
inst✝ : Finite ↑(orbit G a)
⊢ ∃ n, Nat.card ↑(orbit G a) = p ^ n

Tactic:
by

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 α)
⊢ ∑ _a, 1 = card ↑(fixedPoints G α)

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

Tactic:
by

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 α)
x : α
⊢ card { y // Quotient.mk'' y = Quotient.mk'' x } = card ↑(orbit G x)

Tactic:
by

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)
a : ↑(fixedPoints G α)
ha : a ∈ Finset.univ
x✝ : ↑1 ≠ 0
⊢ ↑1 = ↑(card { x // Quotient.mk'' x = Quotient.mk'' ↑a })

Tactic:
by

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)
b✝ : Quotient (orbitRel G α)
b : α
x✝ : Quotient.mk'' b ∈ Finset.univ
hb : ↑(card { x // Quotient.mk'' x = Quotient.mk'' b }) ≠ 0
k : ℕ
hk : card ↑(orbit G b) = p ^ k
⊢ k = 0

Tactic:
by

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)
b✝ : Quotient (orbitRel G α)
b : α
x✝ : Quotient.mk'' b ∈ Finset.univ
hb : ↑(card { x // Quotient.mk'' x = Quotient.mk'' b }) ≠ 0
k : ℕ
hk : card ↑(orbit G b) = p ^ k
this : k = 0
⊢ card ↑(orbit G b) = 1

Tactic:
by

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 α
⊢ Nat.card α ≡ Nat.card ↑(fixedPoints G α) [MOD p]

Tactic:
by

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_3
inst✝ : MulAction G α
hpα : ¬p ∣ Nat.card α
this : Finite α
⊢ Nonempty ↑(fixedPoints G α)

Tactic:
by

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 α
hpα : p ∣ Nat.card α
a : α
ha : a ∈ fixedPoints G α
hpf : p ∣ Nat.card ↑(fixedPoints G α)
hα : Nontrivial ↑(fixedPoints G α)
b : α
hb : b ∈ fixedPoints G α
hba : ⟨b, hb⟩ ≠ ⟨a, ha⟩
hab : a = b
⊢ ⟨b, hb⟩ = ⟨a, ha⟩

Tactic:
by

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 α
hpα : p ∣ Nat.card α
a : α
ha : a ∈ fixedPoints G α
⊢ ∃ b ∈ fixedPoints G α, a ≠ b

Tactic:
by

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)
inst✝¹ : Nontrivial G
inst✝ : Finite G
this : p ∣ Nat.card G → ∀ {a : G}, a ∈ ↑(Subgroup.center G) → ∃ b ∈ ↑(Subgroup.center G), a ≠ b
⊢ p ∣ Nat.card G

Tactic:
by

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)
inst✝¹ : Nontrivial G
inst✝ : Finite G
⊢ Nontrivial ↥(Subgroup.center G)

Tactic:
by

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)
inst✝¹ : Nontrivial G
inst✝ : Finite G
⊢ ⊥ < Subgroup.center G

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝ : Group G
H K : Subgroup G
hK : IsPGroup p ↥K
hHK : H ≤ K
a b : ↥H
h : (Subgroup.inclusion hHK) a = (Subgroup.inclusion hHK) b
⊢ ↑a = ↑b

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 ^ n * J ^ n ≤ ⊥
hnz : n ≠ 0
⊢ I ^ n ⊔ J ^ n = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
hH : IsPGroup p ↥H
K : Type u_2
inst✝ : Group K
ϕ : G →* K
⊢ IsPGroup p ↥(Subgroup.map ϕ H)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : CommMonoid G
hG : ExponentExists G
⊢ ∃ g, orderOf g = exponent G

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
hH : IsPGroup p ↥H
K : Type u_2
inst✝ : Group K
ϕ : K →* G
hϕ : IsPGroup p ↥ϕ.ker
g : ↥(Subgroup.comap ϕ H)
j : ℕ
hj : ϕ (↑g ^ p ^ j) = ↑1
k : ℕ
hk : ↑g ^ p ^ (j + k) = ↑1
⊢ g ^ p ^ (j + k) = 1

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
hH : IsPGroup p ↥H
K : Type u_2
inst✝ : Group K
ϕ : K →* G
hϕ : IsPGroup p ↥ϕ.ker
⊢ IsPGroup p ↥(Subgroup.comap ϕ H)

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 ^ n * J ^ n ≤ ⊥
hnz : n ≠ 0
x : R
hx : x ∈ I ^ n
y : R
hy : y ∈ J ^ n
add : x + y = 1
mul : x * y = 0
⊢ s = ↑(basicOpen x)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
⊢ exponent G = ⨆ g, orderOf g

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
H K : Subgroup G
hH : IsPGroup p ↥H
hK : IsPGroup p ↥K
inst✝ : K.Normal
⊢ IsPGroup p ↥(H ⊔ K)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : CommMonoid G
⊢ exponent G = if ∃ g, orderOf g = 0 then 0 else ⨆ g, orderOf g

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝¹ : CancelCommMonoid G
inst✝ : Fintype G
⊢ 1 ∈ Finset.image orderOf Finset.univ

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝¹ : CancelCommMonoid G
inst✝ : Fintype G
⊢ exponent G = (Finset.image orderOf Finset.univ).max' ⋯

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Group G
n : ℤ
⊢ ↑(Monoid.exponent G) ∣ n ↔ ∀ (g : G), g ^ n = 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)
hs : IsClopen s
⊢ ∃ e f, e * f = 0 ∧ e + f = 1 ∧ s = ↑(basicOpen e) ∧ sᶜ = ↑(basicOpen f)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Group G
n m : ℤ
⊢ ↑(Monoid.exponent G) ∣ n - m ↔ ∀ (g : G), g ^ n = g ^ m

Tactic:
simp_rw [Group.exponent_dvd_iff_forall_zpow_eq_one, zpow_sub, mul_inv_eq_one]

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Group G
n m : ℤ
⊢ ↑(Monoid.exponent G) ∣ n - m ↔ ∀ (g : G), g ^ n = g ^ m

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
⊢ ∀ (y₁ y₂ : R), IsIdempotentElem y₁ ∧ s = ↑(basicOpen y₁) → IsIdempotentElem y₂ ∧ s = ↑(basicOpen y₂) → y₁ = y₂

Tactic:
rintro x y ⟨hx, rfl⟩ ⟨hy, eq⟩

Goal state after:
R : Type u
inst✝ : CommSemiring R
x y : R
hx : IsIdempotentElem x
hs : IsClopen ↑(basicOpen x)
hy : IsIdempotentElem y
eq : ↑(basicOpen x) = ↑(basicOpen y)
⊢ x = y
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
hs : IsClopen s
⊢ ∃! e, IsIdempotentElem e ∧ s = ↑(basicOpen e)

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)
h✝ : IsClopen s
e f : R
h : e * f = 0 ∧ e + f = 1 ∧ s = ↑(basicOpen e) ∧ sᶜ = ↑(basicOpen f)
⊢ e * f = 0 ∧ e + f = 1 ∧ s = ↑(basicOpen e)

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)
⊢ IsClopen s ↔ ∃ e f, e * f = 0 ∧ e + f = 1 ∧ s = ↑(basicOpen e)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
j : ι
hj : exponent (M j) = 0
⊢ exponent ((i : ι) → M i) = 0

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)
⊢ IsClopen s ↔ ∃ e f, e * f = 0 ∧ e + f = 1 ∧ s = zeroLocus {e}

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
G₂ : Type u_2
inst✝² : Group G₂
p₁ p₂ : ℕ
hp₁ : Fact (Nat.Prime p₁)
hp₂ : Fact (Nat.Prime p₂)
hne : p₁ ≠ p₂
H₁ : Subgroup G
H₂ : Subgroup G₂
inst✝¹ : Finite ↥H₁
inst✝ : Finite ↥H₂
hH₁ : IsPGroup p₁ ↥H₁
hH₂ : IsPGroup p₂ ↥H₂
⊢ (Nat.card ↥H₁).Coprime (Nat.card ↥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
⊢ Function.Bijective fun e ↦ { carrier := ↑(basicOpen (↑e).1), isClopen' := ⋯ }

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: F : Type u_1
M₁ : Type u_2
M₂ : Type u_3
inst✝³ : Monoid M₁
inst✝² : Monoid M₂
inst✝¹ : FunLike F M₁ M₂
inst✝ : MonoidHomClass F M₁ M₂
f : F
hf : Function.Surjective ⇑f
⊢ exponent M₂ ∣ exponent M₁

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
a b : { e // e.1 * e.2 = 0 ∧ e.1 + e.2 = 1 }
x✝ : a ≤ b
⊢ basicOpen ((↑a).1 * (↑b).1) = basicOpen (↑a).1

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I : Ideal R
hI : I.FG
⊢ IsRetrocompact (zeroLocus ↑I)ᶜ

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
⊢ exponent ((i : ι) → M i) = univ.lcm fun x ↦ exponent (M x)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: G : Type u_1
inst✝ : Group G
p₁ p₂ : ℕ
H₁ H₂ : Subgroup G
hH₁ : IsPGroup p₁ ↥H₁
hH₂ : IsPGroup p₂ ↥H₂
h : p₁.Coprime p₂
⊢ Disjoint H₁ 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✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : f.IsIntegral
⊢ IsClosedMap (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✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : f.IsIntegral
x : PrimeSpectrum S
hx : IsClosed {x}
⊢ IsClosed {comap f 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✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal S
x : PrimeSpectrum R
hx : Ideal.comap f I ≤ x.asIdeal
p' : Ideal S
hp' : p'.IsPrime
hp'' : I ≤ p'
hq₁ : Ideal.comap f p' ∈ (Ideal.comap f I).minimalPrimes
hq₂ : Ideal.comap f p' ≤ x.asIdeal
p'' : PrimeSpectrum S := { asIdeal := p', isPrime := hp' }
⊢ comap f { asIdeal := p', isPrime := hp' } ∈ comap f '' zeroLocus ↑I

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal S
⊢ closure (comap f '' zeroLocus ↑I) = zeroLocus ↑(Ideal.comap f I)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: M₁ : Type u_1
M₂ : Type u_2
inst✝¹ : Monoid M₁
inst✝ : Monoid M₂
⊢ exponent (M₁ × M₂) = GCDMonoid.lcm (exponent M₁) (exponent M₂)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
h : IsClosedMap (comap (mapRingHom f))
algInst✝ : Algebra R S := f.toAlgebra
this : Algebra.IsIntegral R S
⊢ f.IsIntegral

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Monoid G
hG : Monoid.exponent G = 2
x : G
⊢ orderOf x = 2 → x ≠ 1

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝¹ : Monoid G
inst✝ : IsCancelMul G
a b : G
h : ∀ (g : G), g ^ 2 = 1
⊢ a * (a * b) * b = a ^ 2 * b ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝¹ : Monoid G
inst✝ : IsCancelMul G
a b : G
h : ∀ (g : G), g ^ 2 = 1
⊢ a ^ 2 * b ^ 2 = 1

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝¹ : Monoid G
inst✝ : IsCancelMul G
a b : G
h : ∀ (g : G), g ^ 2 = 1
⊢ 1 = (a * b) ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝¹ : Monoid G
inst✝ : IsCancelMul G
a b : G
h : ∀ (g : G), g ^ 2 = 1
⊢ (a * b) ^ 2 = a * (b * a) * b

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Exponent

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

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Group G
x y : G
hx : orderOf x = 2
hy : orderOf y = 2
hxy : x ≠ y
⊢ x * y ∉ {x, y, 1}

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: 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
⊢ Finite G

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: 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
⊢ (Nat.card ↥H).Coprime (Nat.card ↥P) ∨ H.index.Coprime (Nat.card ↥P)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
h : IsClosedMap (comap (mapRingHom f))
algInst✝ : Algebra R S := f.toAlgebra
a✝¹ : Nontrivial R
a✝ : Nontrivial S
r : S
p : S[X] := C r * X - 1
this : 1 ∈ Ideal.span {X} ⊔ Ideal.comap (mapRingHom f) (Ideal.span {p})
a b : R[X]
hb : b ∈ Ideal.comap (mapRingHom f) (Ideal.span {p})
e : a * X + b = 1
c : S[X]
hc : map (algebraMap R S) b = p * c
⊢ (X ^ (1 + c.natDegree)).Monic

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
h : IsClosedMap (comap (mapRingHom f))
algInst✝ : Algebra R S := f.toAlgebra
a✝¹ : Nontrivial R
a✝ : Nontrivial S
r : S
p : S[X] := C r * X - 1
this : 1 ∈ Ideal.span {X} ⊔ Ideal.comap (mapRingHom f) (Ideal.span {p})
a b : R[X]
hb : b ∈ Ideal.comap (mapRingHom f) (Ideal.span {p})
e : a * X + b = 1
c : S[X]
hc : map (algebraMap R S) b = p * c
⊢ b.coeff 0 = 1

Tactic:
by

Goal state after: