mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.ZMod.QuotientGroup

Goal state before:
pp: a : ℤ
⊢ a.natAbs = a.natAbs

Tactic:
]

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 : ℤ
hn : ¬n = 0
ha : ¬a = 0
h : n = -↑n.natAbs
⊢ (-↑n.natAbs * a ^ (↑(n.natAbs - 1) - ↑(n.natAbs * 2))) • D a = (↑(-↑n.natAbs) * a ^ (-↑n.natAbs - 1)) • D a

Tactic:
]

Goal state after:
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 : ℤ
hn : ¬n = 0
ha : ¬a = 0
h : n = -↑n.natAbs
⊢ (-↑n.natAbs * a ^ (↑(n.natAbs - 1) - ↑(n.natAbs * 2))) • D a = (↑(-↑n.natAbs) * a ^ (-↑n.natAbs - 1)) • D a
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
ι : Type u_1
f : ι → R
⊢ zeroLocus (⋃ i, {f i}) = Set.univᶜ ↔ zeroLocus ↑(Ideal.span (Set.range f)) = ∅

Tactic:
]

Goal state after:
R : Type u
inst✝ : CommSemiring R
ι : Type u_1
f : ι → R
⊢ zeroLocus (⋃ i, {f i}) = Set.univᶜ ↔ zeroLocus ↑(Ideal.span (Set.range f)) = ∅
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Monoid G
⊢ (if h : ExponentExists G then Nat.find h else 0) ≠ 0 ↔ ExponentExists G

Tactic:
]

Goal state after:
G : Type u
inst✝ : Monoid G
⊢ (if h : ExponentExists G then Nat.find h else 0) ≠ 0 ↔ ExponentExists G
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 : β
⊢ minimalPeriod (fun x ↦ a +ᵥ x) b • ⟨a, ⋯⟩ +ᵥ b = b

Tactic:
]

Goal state after:
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 : β
⊢ minimalPeriod (fun x ↦ a +ᵥ x) b • ⟨a, ⋯⟩ +ᵥ b = b
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}
r : R
hr : ∀ m ∈ Submonoid.powers f, m ∉ Ideal.span {r}
q : Ideal R
prime : q.IsPrime
le : Ideal.span {r} ≤ q
disj : Disjoint ↑q ↑(Submonoid.powers f)
this : { asIdeal := q, isPrime := prime } = p
⊢ r ∉ p.asIdeal.primeCompl

Tactic:
]

Goal state after:
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}
r : R
hr : ∀ m ∈ Submonoid.powers f, m ∉ Ideal.span {r}
q : Ideal R
prime : q.IsPrime
le : Ideal.span {r} ≤ q
disj : Disjoint ↑q ↑(Submonoid.powers f)
this : { asIdeal := q, isPrime := prime } = p
⊢ r ∉ p.asIdeal.primeCompl
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case pos
G : Type u
inst✝ : Monoid G
h : ExponentExists G
h' : {d | 0 < d ∧ ∀ (x : G), x ^ d = 1}.Nonempty
⊢ Nat.find h = Nat.find h'

Tactic:
]

Goal state after:
case pos
G : Type u
inst✝ : Monoid G
h : ExponentExists G
h' : {d | 0 < d ∧ ∀ (x : G), x ^ d = 1}.Nonempty
⊢ Nat.find h = Nat.find h'
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 : β
⊢ (QuotientAddGroup.map (zmultiples ↑(minimalPeriod (fun x ↦ a +ᵥ x) b)) (stabilizer (↥(zmultiples a)) b)
        ((zmultiplesHom ↥(zmultiples a)) ⟨a, ⋯⟩) ⋯).ker ≤
    ⊥

Tactic:
]

Goal state after:
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 : β
⊢ (QuotientAddGroup.map (zmultiples ↑(minimalPeriod (fun x ↦ a +ᵥ x) b)) (stabilizer (↥(zmultiples a)) b)
        ((zmultiplesHom ↥(zmultiples a)) ⟨a, ⋯⟩) ⋯).ker ≤
    ⊥
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}
r : R
hr : ∀ m ∈ Submonoid.powers f, m ∉ Ideal.span {r}
q : Ideal R
prime : q.IsPrime
le : Ideal.span {r} ≤ q
disj : Disjoint ↑q ↑(Submonoid.powers f)
this : { asIdeal := q, isPrime := prime } = p
⊢ r ∉ { asIdeal := q, isPrime := prime }.asIdeal.primeCompl

Tactic:
]

Goal state after:
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}
r : R
hr : ∀ m ∈ Submonoid.powers f, m ∉ Ideal.span {r}
q : Ideal R
prime : q.IsPrime
le : Ideal.span {r} ≤ q
disj : Disjoint ↑q ↑(Submonoid.powers f)
this : { asIdeal := q, isPrime := prime } = p
⊢ r ∉ { asIdeal := q, isPrime := prime }.asIdeal.primeCompl
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

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

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : CommRing R
c : R
this✝ : Algebra R[X] (Away c)[X] := (mapRingHom (algebraMap R (Away c))).toAlgebra
this : IsLocalization (Submonoid.powers (C c)) (Away c)[X]
⊢ (range (comap (algebraMap R[X] (Away c)[X])))ᶜ = range (comap (mapRingHom (Ideal.Quotient.mk (Ideal.span {c}))))
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case neg
G : Type u
inst✝ : Monoid G
h : ¬ExponentExists G
this : {d | 0 < d ∧ ∀ (x : G), x ^ d = 1} = ∅
⊢ 0 = 0

Tactic:
]

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 : β
q : ℤ ⧸ zmultiples ↑(minimalPeriod (fun x ↦ a +ᵥ x) b)
n : ℤ
hn :
  ↑n ∈
    (QuotientAddGroup.map (zmultiples ↑(minimalPeriod (fun x ↦ a +ᵥ x) b)) (stabilizer (↥(zmultiples a)) b)
        ((zmultiplesHom ↥(zmultiples a)) ⟨a, ⋯⟩) ⋯).ker
⊢ n • a +ᵥ b = b

Tactic:
]

Goal state after:
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 : β
q : ℤ ⧸ zmultiples ↑(minimalPeriod (fun x ↦ a +ᵥ x) b)
n : ℤ
hn :
  ↑n ∈
    (QuotientAddGroup.map (zmultiples ↑(minimalPeriod (fun x ↦ a +ᵥ x) b)) (stabilizer (↥(zmultiples a)) b)
        ((zmultiplesHom ↥(zmultiples a)) ⟨a, ⋯⟩) ⋯).ker
⊢ n • a +ᵥ b = b
Module: Mathlib.GroupTheory.Exponent

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

Tactic:
]

Goal state after:
G : Type u
inst✝ : Monoid G
⊢ (¬∃ n, 0 < n ∧ ∀ (g : G), g ^ n = 1) ↔ ∀ n > 0, ∃ g, g ^ n ≠ 1
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
c : R
this✝ : Algebra R[X] (Away c)[X] := (mapRingHom (algebraMap R (Away c))).toAlgebra
this : IsLocalization (Submonoid.powers (C c)) (Away c)[X]
surj : Function.Surjective ⇑(mapRingHom (Ideal.Quotient.mk (Ideal.span {c})))
⊢ (↑(basicOpen (C c)))ᶜ = zeroLocus ↑(RingHom.ker (mapRingHom (Ideal.Quotient.mk (Ideal.span {c}))))

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : CommRing R
c : R
this✝ : Algebra R[X] (Away c)[X] := (mapRingHom (algebraMap R (Away c))).toAlgebra
this : IsLocalization (Submonoid.powers (C c)) (Away c)[X]
surj : Function.Surjective ⇑(mapRingHom (Ideal.Quotient.mk (Ideal.span {c})))
⊢ (↑(basicOpen (C c)))ᶜ = zeroLocus ↑(RingHom.ker (mapRingHom (Ideal.Quotient.mk (Ideal.span {c}))))
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Monoid G
n : ℕ
g : G
⊢ g ^ n = g ^ n

Tactic:
]

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
⊢ Nat.find ?hc ≤ n

pp: case hc
G : Type u
inst✝ : Monoid G
n : ℕ
hpos : 0 < n
hG : ∀ (g : G), g ^ n = 1
⊢ ExponentExists G

Tactic:
]

Goal state after:
G : Type u
inst✝ : Monoid G
n : ℕ
hpos : 0 < n
hG : ∀ (g : G), g ^ n = 1
⊢ Nat.find ?hc ≤ n

case hc
G : Type u
inst✝ : Monoid G
n : ℕ
hpos : 0 < n
hG : ∀ (g : G), g ^ n = 1
⊢ ExponentExists G
Module: Mathlib.Data.ZMod.QuotientGroup

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : Group α
a : α
inst✝ : MulAction α β
b : β
k : ℤ
⊢ ⟨a, ⋯⟩ ^ (k % ↑(minimalPeriod (fun x ↦ a • x) b)) • ⟨b, ⋯⟩ = ⟨a, ⋯⟩ ^ k • ⟨b, ⋯⟩

Tactic:
]

Goal state after:
α : Type u_3
β : Type u_4
inst✝¹ : Group α
a : α
inst✝ : MulAction α β
b : β
k : ℤ
⊢ ⟨a, ⋯⟩ ^ (k % ↑(minimalPeriod (fun x ↦ a • x) b)) • ⟨b, ⋯⟩ = ⟨a, ⋯⟩ ^ k • ⟨b, ⋯⟩
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

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

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : Group α
H : Subgroup α
⊢ (∃ g, zpowers g = ⊤) ↔ ∃ g, zpowers g = H
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: G : Type u_2
inst✝ : Group G
h✝ : IsCyclic G
σ : G →* G
h : G
hG : ∀ (x : G), x ∈ zpowers h
m : ℤ
hm : (fun x ↦ h ^ x) m = σ h
n : ℤ
⊢ h ^ (m * n) = h ^ (m * n)

Tactic:
]

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

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

Tactic:
]

Goal state after:
α : Type u_1
inst✝¹ : Group α
inst✝ : Finite α
⊢ (∃ g, orderOf g = Nat.card α) ↔ ∃ g, Nat.card α ≤ orderOf g
Module: Mathlib.Data.ZMod.QuotientGroup

Goal state before:
pp: α : Type u_5
β : Type u_6
inst✝¹ : AddGroup α
a : α
inst✝ : AddAction α β
b : β
k : ℤ
⊢ (k % ↑(minimalPeriod (fun x ↦ a +ᵥ x) b)) • ⟨a, ⋯⟩ +ᵥ ⟨b, ⋯⟩ = k • ⟨a, ⋯⟩ +ᵥ ⟨b, ⋯⟩

Tactic:
]

Goal state after:
α : Type u_5
β : Type u_6
inst✝¹ : AddGroup α
a : α
inst✝ : AddAction α β
b : β
k : ℤ
⊢ (k % ↑(minimalPeriod (fun x ↦ a +ᵥ x) b)) • ⟨a, ⋯⟩ +ᵥ ⟨b, ⋯⟩ = k • ⟨a, ⋯⟩ +ᵥ ⟨b, ⋯⟩
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))
⊢ RingHom.ker (Pi.evalRingHom R i) ≤ p.asIdeal

Tactic:
]

Goal state after:
ι : 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))
⊢ RingHom.ker (Pi.evalRingHom R i) ≤ p.asIdeal
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:
rw [AddAction.orbitZMultiplesEquiv_symm_apply, ZMod.coe_intCast]
  -- Making `a` explicit turns this from ~190000 heartbeats to ~700.
  exact Subtype.ext (zsmul_vadd_mod_minimalPeriod a _ k)

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
⊢ x ∈ p.asIdeal

Tactic:
]

Goal state after:
ι : 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
⊢ x ∈ p.asIdeal
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
⊢ 1 = 1

Tactic:
]

Goal state after:
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 = minimalPeriod (fun x ↦ a • x) b

Tactic:
]

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))
this✝ : Finite G
this : H = ⊥ ∨ Nat.card ↥H = Nat.card G
⊢ H = ⊥ ∨ H = ⊤

Tactic:
card_eq_iff_eq_top

Goal state after:
G : Type u_2
inst✝ : Group G
H : Subgroup G
hp : Fact (Nat.Prime (Nat.card G))
this✝ : Finite G
this : H = ⊥ ∨ H = ⊤
⊢ H = ⊥ ∨ H = ⊤
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))
this✝ : Finite G
this : H = ⊥ ∨ H = ⊤
⊢ H = ⊥ ∨ H = ⊤

Tactic:
]

Goal state after:
G : Type u_2
inst✝ : Group G
H : Subgroup G
hp : Fact (Nat.Prime (Nat.card G))
this✝ : Finite G
this : H = ⊥ ∨ H = ⊤
⊢ H = ⊥ ∨ H = ⊤
Module: Mathlib.Data.ZMod.QuotientGroup

Goal state before:
pp: case intro
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)
val✝ : Fintype ↑(orbit (↥(zpowers a)) b)
this : Nonempty ↑(orbit (↥(zpowers a)) b)
⊢ Fintype.card ↑(orbit (↥(zpowers a)) b) ≠ 0

Tactic:
]

Goal state after:
case intro
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)
val✝ : Fintype ↑(orbit (↥(zpowers a)) b)
this : Nonempty ↑(orbit (↥(zpowers a)) b)
⊢ Fintype.card ↑(orbit (↥(zpowers a)) b) ≠ 0
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

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

Tactic:
]

Goal state after:
G : Type u_2
inst✝ : Group G
g : G
hg : g ≠ 1
hp : Fact (Nat.Prime (Nat.card G))
this : zpowers g = ⊤
⊢ zpowers g = ⊤
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case inr.mp
G : Type u
inst✝ : Monoid G
n : ℕ
hpos : n > 0
h : n % exponent G = 0
g : G
⊢ g ^ n = 1

Tactic:
]

Goal state after:
case inr.mp
G : Type u
inst✝ : Monoid G
n : ℕ
hpos : n > 0
h : n % exponent G = 0
g : G
⊢ g ^ n = 1
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case inr.mp
G : Type u
inst✝ : Monoid G
n : ℕ
hpos : n > 0
h : n % exponent G = 0
g : G
⊢ 1 = 1

Tactic:
]

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
this : Finite G
⊢ g' ∈ zpowers g

Tactic:
]

Goal state after:
G : Type u_2
inst✝ : Group G
p : ℕ
hp : Fact (Nat.Prime p)
h : Nat.card G = p
g g' : G
hg : g ≠ 1
this : Finite G
⊢ g' ∈ zpowers g
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

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

Tactic:
intro hp
    have : p ∈ Set.range (PrimeSpectrum.comap (Pi.evalRingHom R i)) := by
      rw [range_comap_of_surjective _ _ (RingHom.surjective _), mem_zeroLocus,
        SetLike.coe_subset_coe]
      intro x hx
      rw [RingHom.mem_ker, Pi.evalRingHom_apply] at hx
      have : Pi.single i f * x = 0 := by
        ext j
        by_cases h : i = j
        · subst h
          simp [hx]
        · simp [h]
      obtain (h | h) := Ideal.IsPrime.mem_or_mem_of_mul_eq_zero p.isPrime this <;> tauto
    obtain ⟨q, rfl⟩ := this
    exact ⟨q, by simpa using hp, by ext; simp⟩

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

Goal state before:
pp: α : Type u_3
inst✝ : Group α
a : α
this : Nat.card ↑↑(zpowers a) = Function.minimalPeriod (fun x ↦ a • x) 1
⊢ Nat.card ↥(zpowers a) = orderOf a

Tactic:
]

Goal state after:
α : Type u_3
inst✝ : Group α
a : α
this : Nat.card ↑↑(zpowers a) = Function.minimalPeriod (fun x ↦ a • x) 1
⊢ Nat.card ↥(zpowers a) = orderOf a
Module: Mathlib.GroupTheory.Exponent

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

Tactic:
]

Goal state after:
case inr.mpr
G : Type u
inst✝ : Monoid G
n : ℕ
hpos : n > 0
hG : ∀ (g : G), g ^ n = 1
h : 0 < n % exponent G
⊢ False
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)
⊢ ∀ (i : ι), Continuous fun a ↦ sigmaToPi R ⟨i, a⟩

Tactic:
]

Goal state after:
case refine_1
ι : Type u_1
R : ι → Type u_2
inst✝ : (i : ι) → CommRing (R i)
⊢ ∀ (i : ι), Continuous fun a ↦ sigmaToPi R ⟨i, a⟩
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case refine_3
ι : Type u_1
R : ι → Type u_2
inst✝ : (i : ι) → CommRing (R i)
⊢ ∀ (i : ι), IsOpenMap fun a ↦ sigmaToPi R ⟨i, a⟩

Tactic:
]

Goal state after:
case refine_3
ι : Type u_1
R : ι → Type u_2
inst✝ : (i : ι) → CommRing (R i)
⊢ ∀ (i : ι), IsOpenMap fun a ↦ sigmaToPi R ⟨i, a⟩
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 : ℤ
⊢ g ^ k • Quotient.out q = g ^ k • Quotient.out q

Tactic:
]

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

Goal state before:
pp: case refine_3
ι : Type u_1
R : ι → Type u_2
inst✝ : (i : ι) → CommRing (R i)
i : ι
f : R i
⊢ IsOpen ↑(basicOpen (Pi.single i f))

Tactic:
]

Goal state after:
case refine_3
ι : Type u_1
R : ι → Type u_2
inst✝ : (i : ι) → CommRing (R i)
i : ι
f : R i
⊢ IsOpen ↑(basicOpen (Pi.single i f))
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

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

Tactic:
]

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
⊢ Nat.card α = Nat.card α

pp: α : Type u_1
inst✝ : Group α
g : α
hx : ∀ (x : α), x ∈ Submonoid.powers g
⊢ ∀ (x : α), x ∈ zpowers g

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : Group α
g : α
hx : ∀ (x : α), x ∈ Submonoid.powers g
⊢ ∀ (x : α), x ∈ zpowers g
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:
]

Goal state after:
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))
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
⊢ 1 = 1

Tactic:
]

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 : ⊥.factorization p ≠ 0
ht : exponent G = ⊥
⊢ False

Tactic:
]

Goal state after:
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : ⊥.factorization p ≠ 0
ht : exponent G = ⊥
⊢ False
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: case e'_3
G : Type u_2
inst✝ : Group G
k : ℕ
k_pos : k ≠ 0
this : Finite G
a : G
ha : Function.Surjective fun x ↦ a ^ x
k_lt_card_G : a ^ k = 1
⊢ ⊤ ≤ zpowers a

Tactic:
]

Goal state after:
case e'_3
G : Type u_2
inst✝ : Group G
k : ℕ
k_pos : k ≠ 0
this : Finite G
a : G
ha : Function.Surjective fun x ↦ a ^ x
k_lt_card_G : a ^ k = 1
⊢ ⊤ ≤ zpowers a
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 : ⊥.factorization p ≠ 0
ht : exponent G = ⊥
⊢ 0 = 0

Tactic:
]

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
⊢ 0 = 0

Tactic:
]

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

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

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ (H ≠ ⊥ ∧ ∀ H' ≤ H, (H'.subgroupOf H).Normal → H'.subgroupOf H = ⊥ ∨ H'.subgroupOf H = ⊤) ↔
    H ≠ ⊥ ∧ ∀ H' ≤ H, (H'.subgroupOf H).Normal → H' = ⊥ ∨ H' = H
Module: Mathlib.GroupTheory.Subgroup.Simple

Goal state before:
pp: case refine_1
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 : comap f H = ⊥
⊢ H = H

Tactic:
]

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

Goal state before:
pp: case refine_2
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 : comap f H = comap f ⊤
⊢ H = ⊤

Tactic:
]

Goal state after:
case refine_2
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 : comap f H = comap f ⊤
⊢ H = ⊤
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case inr
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, orderOf g = p ^ (exponent G).factorization p

Tactic:
]

Goal state after:
case inr
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, orderOf g = p ^ (exponent G).factorization p
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
⊢ 1 = 1

Tactic:
]

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 : ∃ x, ¬x ^ (exponent G / p) = 1
⊢ ∃ g, g ^ (exponent G / p) ≠ 1

Tactic:
]

Goal state after:
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 : ∃ x, ¬x ^ (exponent G / p) = 1
⊢ ∃ g, g ^ (exponent G / p) ≠ 1
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: case ofNat
α : 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) (Int.ofNat k) = x
hk : g ^ Int.ofNat k = x
⊢ x ∈ H

Tactic:
]

Goal state after:
case ofNat
α : 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) (Int.ofNat k) = x
hk : g ^ Int.ofNat k = x
⊢ x ∈ H