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

Goal state before:
pp: case mp
R : Type u
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsRadical
h : ∀ (x y : Ideal R), x ⊓ y ≤ I → x ≤ I ∨ y ≤ I
x y : R
h' : (Ideal.span {x} * Ideal.span {y}).radical ≤ I
⊢ (Ideal.span {x} ⊓ Ideal.span {y}).radical ≤ I

Tactic:
simpa using

Goal state after:
case mp
R : Type u
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsRadical
h : ∀ (x y : Ideal R), x ⊓ y ≤ I → x ≤ I ∨ y ≤ I
x y : R
h' : (Ideal.span {x} * Ideal.span {y}).radical ≤ I
⊢ (Ideal.span {x}).radical ⊓ (Ideal.span {y}).radical ≤ I
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : IsDomain R
⊢ IrreducibleSpace (PrimeSpectrum R)

Tactic:
simpa using

Goal state after:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : IsDomain R
⊢ Ideal.IsPrime ⊥
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
S✝ : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S✝
S : Set (PrimeSpectrum R)
h₁ : IsIrreducible S
h₂ : IsClosed S
⊢ IsGenericPoint { asIdeal := vanishingIdeal S, isPrime := ⋯ } S

Tactic:
IsGenericPoint,

Goal state after:
R : Type u
S✝ : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S✝
S : Set (PrimeSpectrum R)
h₁ : IsIrreducible S
h₂ : IsClosed S
⊢ closure {{ asIdeal := vanishingIdeal S, isPrime := ⋯ }} = S
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p✝ : PrimeSpectrum (R × S)
h : p✝ ∈ zeroLocus ↑(RingHom.ker (RingHom.fst R S))
p : Ideal R
hp : p.IsPrime
eq : p✝.asIdeal = p.prod ⊤
⊢ (comap (RingHom.fst R S) { asIdeal := p, isPrime := hp }).asIdeal = p✝.asIdeal

Tactic:
simpa using

Goal state after:
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p✝ : PrimeSpectrum (R × S)
h : p✝ ∈ zeroLocus ↑(RingHom.ker (RingHom.fst R S))
p : Ideal R
hp : p.IsPrime
eq : p✝.asIdeal = p.prod ⊤
⊢ Ideal.comap (RingHom.fst R S) p = p✝.asIdeal
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case refine_2.inr
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p✝ : PrimeSpectrum (R × S)
h : p✝ ∈ zeroLocus ↑(RingHom.ker (RingHom.fst R S))
p : Ideal S
hp : p.IsPrime
eq : p✝.asIdeal = ⊤.prod p
⊢ 1 ∈ p

Tactic:
simpa using

Goal state after:
case refine_2.inr
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p✝ : PrimeSpectrum (R × S)
h : p✝ ∈ zeroLocus ↑(RingHom.ker (RingHom.fst R S))
p : Ideal S
hp : p.IsPrime
eq : p✝.asIdeal = ⊤.prod p
⊢ 1 ∈ p
Module: Mathlib.RingTheory.Derivation.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing M
inst✝³ : Algebra R A
inst✝² : Algebra R M
F : Type u_4
inst✝¹ : FunLike F A M
inst✝ : AlgHomClass F R A M
f : F
f_inv : M → A
hf : Function.RightInverse f_inv ⇑f
d : Derivation R A A
hd : ∀ (x : A), f x = 0 → f (d x) = 0
x y : M
⊢ f (d (f_inv (x + y))) = f (d (f_inv x)) + f (d (f_inv y))

Tactic:
by
    suffices f (d (f_inv (x + y) - (f_inv x + f_inv y))) = 0 by simpa [sub_eq_zero]
    apply hd
    simp [hf _]

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

Goal state before:
pp: case refine_2.inl
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p✝ : PrimeSpectrum (R × S)
h : p✝ ∈ zeroLocus ↑(RingHom.ker (RingHom.snd R S))
p : Ideal R
hp : p.IsPrime
eq : p✝.asIdeal = p.prod ⊤
⊢ 1 ∈ p

Tactic:
simpa using

Goal state after:
case refine_2.inl
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p✝ : PrimeSpectrum (R × S)
h : p✝ ∈ zeroLocus ↑(RingHom.ker (RingHom.snd R S))
p : Ideal R
hp : p.IsPrime
eq : p✝.asIdeal = p.prod ⊤
⊢ 1 ∈ p
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p✝ : PrimeSpectrum (R × S)
h : p✝ ∈ zeroLocus ↑(RingHom.ker (RingHom.snd R S))
p : Ideal S
hp : p.IsPrime
eq : p✝.asIdeal = ⊤.prod p
⊢ (comap (RingHom.snd R S) { asIdeal := p, isPrime := hp }).asIdeal = p✝.asIdeal

Tactic:
simpa using

Goal state after:
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p✝ : PrimeSpectrum (R × S)
h : p✝ ∈ zeroLocus ↑(RingHom.ker (RingHom.snd R S))
p : Ideal S
hp : p.IsPrime
eq : p✝.asIdeal = ⊤.prod p
⊢ Ideal.comap (RingHom.snd R S) p = p✝.asIdeal
Module: Mathlib.RingTheory.Derivation.Basic

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : CommSemiring A
inst✝³ : Algebra R A
M : Type u_3
inst✝² : AddCancelCommMonoid M
inst✝¹ : Module R M
inst✝ : Module A M
D : A →ₗ[R] M
h : ∀ (a b : A), D (a * b) = a • D b + b • D a
⊢ D 1 + D 1 = D 1

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : CommSemiring A
inst✝³ : Algebra R A
M : Type u_3
inst✝² : AddCancelCommMonoid M
inst✝¹ : Module R M
inst✝ : Module A M
D : A →ₗ[R] M
h : ∀ (a b : A), D (a * b) = a • D b + b • D a
⊢ D 1 + D 1 = D 1
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
f : R
n : ℕ
hn : 0 < n
⊢ ↑(basicOpen (f ^ n)) = ↑(basicOpen f)

Tactic:
simpa using

Goal state after:
R : Type u
inst✝ : CommSemiring R
f : R
n : ℕ
hn : 0 < n
⊢ zeroLocus {f ^ n} = zeroLocus {f}
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) / a ^ ↑(n.natAbs * 2))) • D a = (↑(-↑n.natAbs) * a ^ (-↑n.natAbs - 1)) • D a

Tactic:
rw [← zpow_sub₀ ha]

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
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
i j : R
⊢ IsCompact (↑(basicOpen i) ∩ ↑(basicOpen j))

Tactic:
simpa using

Goal state after:
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
i j : R
⊢ IsCompact ↑(basicOpen (i * j))
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:
simpa using

Goal state after:
ι : 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))
⊢ f ∉ q.asIdeal
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
  classical
  refine .of_continuous_injective_isOpenMap ?_ ?_ ?_
  · rw [continuous_sigma_iff]
    intro i
    exact continuous_comap (Pi.evalRingHom R i)
  · exact sigmaToPi_injective R
  · rw [isOpenMap_sigma]
    intro i
    simp only [sigmaToPi_apply, PrimeSpectrum.isTopologicalBasis_basic_opens.isOpenMap_iff]
    rintro - ⟨f, rfl⟩
    rw [PrimeSpectrum.comap_evalRingHom_basicOpen]
    exact isOpen_basicOpen

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:
have : Finite G := Nat.finite_of_card_ne_zero (Nat.ne_zero_of_lt k_lt_card_G)

Goal state after:
G : Type u_2
inst✝ : Group G
G_cyclic : IsCyclic G
k : ℕ
k_pos : k ≠ 0
k_lt_card_G : k < Nat.card G
this : Finite G
⊢ ∃ a, a ^ k ≠ 1
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

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

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
x : α
hx : x ∈ {a | a ^ n = 1}
m : ℕ
hm : g ^ m = x
⊢ x ^ n = 1
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

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

Tactic:
simpa using

Goal state after:
R : Type u
inst✝ : CommSemiring R
s✝ : Set (PrimeSpectrum R)
x✝ : ∃ s, s.Finite ∧ s✝ = (zeroLocus s)ᶜ
s : Set R
hs : s.Finite
e : s✝ = (zeroLocus s)ᶜ
⊢ (zeroLocus s)ᶜ = s✝
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

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

Tactic:
simpa using

Goal state after:
R : Type u
inst✝ : CommSemiring R
s✝ : Set (PrimeSpectrum R)
x✝ : ∃ t, (zeroLocus ↑t)ᶜ = s✝
s : Finset R
e : (zeroLocus ↑s)ᶜ = s✝
⊢ s✝ = (zeroLocus ↑s)ᶜ
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

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

Tactic:
simpa using

Goal state after:
R : Type u
inst✝ : CommSemiring R
s✝ : Set (PrimeSpectrum R)
x✝ : ∃ t, (zeroLocus ↑t)ᶜ = s✝
s : Finset R
e : (zeroLocus ↑s)ᶜ = s✝
⊢ (zeroLocus ↑s)ᶜ = s✝
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

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

Tactic:
simpa using

Goal state after:
R : Type u
inst✝ : CommSemiring R
s✝ : Set (PrimeSpectrum R)
x✝ : ∃ I, I.FG ∧ (zeroLocus ↑I)ᶜ = s✝
I : Ideal R
s : Finset R
hs : Ideal.span ↑s = I
e : (zeroLocus ↑I)ᶜ = s✝
⊢ (zeroLocus ↑s)ᶜ = s✝
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
g : G
hg : g ≠ 1
⊢ p ∣ exponent G

Tactic:
simpa using

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

Tactic:
simpa using

Goal state after:
case refine_1
G : Type u
inst✝¹ : LeftCancelMonoid G
inst✝ : Finite G
_inst : Fintype G := Fintype.ofFinite G
⊢ ∀ (x : G), IsOfFinOrder x
Module: Mathlib.GroupTheory.Exponent

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

Tactic:
by
  rw [Nat.one_lt_iff_ne_zero_and_ne_one]
  exact ⟨exponent_ne_zero_of_finite, mt exp_eq_one_iff.mp (not_subsingleton G)⟩

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

Goal state before:
pp: G : Type u_2
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsCyclic G
g : G
hg : ∀ (x : G), x ∈ zpowers g
a b : ZMod (Nat.card G)
h : ↑a.val = ↑b.val
⊢ a = b

Tactic:
simpa using

Goal state after:
G : Type u_2
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsCyclic G
g : G
hg : ∀ (x : G), x ∈ zpowers g
a b : ZMod (Nat.card G)
h : ↑a.val = ↑b.val
⊢ a = b
Module: Mathlib.GroupTheory.PGroup

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

Tactic:
simpa using

Goal state after:
G : Type u_1
inst✝ : Group G
⊢ (∀ (g : G), g = 1) → Subsingleton G
Module: Mathlib.GroupTheory.PGroup

Goal state before:
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:
grw [← Nat.primeFactors_pow p hn0, Nat.primeFactors_mono hn <| pow_ne_zero n h]

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:
simp only [Quotient.eq'']

Goal state after:
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 // (orbitRel G α) y x } = card ↑(orbit G x)
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case h.h
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
j : ι
hj : ∀ (n : ℕ), 0 < n → ∃ g, g ^ n ≠ 1
n : ℕ
hn : 0 < n
m : M j
hm : m ^ n ≠ 1
h : Pi.mulSingle j m ^ n = 1
⊢ m ^ n = 1

Tactic:
simpa using

Goal state after:
case h.h
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
j : ι
hj : ∀ (n : ℕ), 0 < n → ∃ g, g ^ n ≠ 1
n : ℕ
hn : 0 < n
m : M j
hm : m ^ n ≠ 1
h : Pi.mulSingle j m ^ n = 1
⊢ m ^ n = 1
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

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

Tactic:
simpa using

Goal state after:
R : Type u
inst✝ : CommSemiring R
f : R
⊢ IsRetrocompact (zeroLocus {f})ᶜ
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:
simpa using

Goal state after:
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}
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case refine_2
M₁ : Type u_1
M₂ : Type u_2
inst✝¹ : Monoid M₁
inst✝ : Monoid M₂
⊢ exponent M₁ ∣ exponent (M₁ × M₂)

pp: case refine_3
M₁ : Type u_1
M₂ : Type u_2
inst✝¹ : Monoid M₁
inst✝ : Monoid M₂
⊢ exponent M₂ ∣ exponent (M₁ × M₂)

Tactic:
· exact MonoidHom.exponent_dvd (f := MonoidHom.fst M₁ M₂) Prod.fst_surjective

Goal state after:
case refine_3
M₁ : Type u_1
M₂ : Type u_2
inst✝¹ : Monoid M₁
inst✝ : Monoid M₂
⊢ exponent M₂ ∣ exponent (M₁ × M₂)
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: n : ℕ
G : Type u_2
inst✝¹ : AddCommGroup G
inst✝ : Module (ZMod n) G
⊢ IsPGroup n (Multiplicative G)

Tactic:
simpa using

Goal state after:
n : ℕ
G : Type u_2
inst✝¹ : AddCommGroup G
inst✝ : Module (ZMod n) G
⊢ ∀ (a : G), ∃ k, Multiplicative.ofAdd a ^ n ^ k = 1
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝ : Group G
g : G
P : Sylow p G
h : G
x✝ : h ∈ g • P
a : G
b : a ∈ ↑↑P
c : ((MulDistribMulAction.toMonoidEnd (MulAut G) G) (MulAut.conj g)) a = h
⊢ g⁻¹ * ((MulDistribMulAction.toMonoidEnd (MulAut G) G) (MulAut.conj g)) a * g ∈ ↑P

Tactic:
simpa using

Goal state after:
p : ℕ
G : Type u_1
inst✝ : Group G
g : G
P : Sylow p G
h : G
x✝ : h ∈ g • P
a : G
b : a ∈ ↑↑P
c : ((MulDistribMulAction.toMonoidEnd (MulAut G) G) (MulAut.conj g)) a = h
⊢ a ∈ P
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: case h.inr
α : Type u_1
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → #{a | a ^ n = 1} ≤ n
d : ℕ
IH : ∀ m < d, m ∣ Fintype.card α → 0 < #{a | orderOf a = m} → #{a | orderOf a = m} = φ m
hd : d ∣ Fintype.card α
hpos : 0 < #{a | orderOf a = d}
hd0 : d ≠ 0
a : α
ha' : a ∈ {a | orderOf a = d}
ha : orderOf a = d
h1 : ∑ m ∈ d.properDivisors, #{a | orderOf a = m} = ∑ m ∈ d.properDivisors, φ m
h2 : ∑ m ∈ d.divisors, #{a | orderOf a = m} = ∑ m ∈ d.divisors, φ m
⊢ #{a | orderOf a = d} = φ d

Tactic:
simpa using

Goal state after:
case h.inr
α : Type u_1
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → #{a | a ^ n = 1} ≤ n
d : ℕ
IH : ∀ m < d, m ∣ Fintype.card α → 0 < #{a | orderOf a = m} → #{a | orderOf a = m} = φ m
hd : d ∣ Fintype.card α
hpos : 0 < #{a | orderOf a = d}
hd0 : d ≠ 0
a : α
ha' : a ∈ {a | orderOf a = d}
ha : orderOf a = d
h1 : ∑ m ∈ d.properDivisors, #{a | orderOf a = m} = ∑ m ∈ d.properDivisors, φ m
h2 : ∑ m ∈ d.divisors, #{a | orderOf a = m} = ∑ m ∈ d.divisors, φ m
⊢ #{a | orderOf a = d} = φ d
Module: Mathlib.GroupTheory.Rank

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : FG G
h : rank G = 0
s : Finset G
hs : s = ∅
hs' : Subgroup.closure ↑s = ⊤
⊢ Subsingleton G

Tactic:
simpa using

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : FG G
h : rank G = 0
s : Finset G
hs : s = ∅
hs' : Subgroup.closure ↑s = ⊤
⊢ Subsingleton G
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
hs : s ∈ irreducibleComponents (PrimeSpectrum R)
⊢ ((zeroLocus ∘ SetLike.coe) ∘ vanishingIdeal) s = id s

Tactic:
simpa using

Goal state after:
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
hs : s ∈ irreducibleComponents (PrimeSpectrum R)
⊢ IsClosed s
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: G : Type u_2
G' : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : IsCyclic G'
f : G →* G'
hf : f.ker ≤ center G
a b : G
x : G'
y : G
hxy : f y = x
hx : ∀ (a : ↥f.range), a ∈ zpowers ⟨x, ⋯⟩
m : ℤ
hm : (fun x_1 ↦ ⟨x, ⋯⟩ ^ x_1) m = ⟨f a, ⋯⟩
n : ℤ
hn : (fun x_1 ↦ ⟨x, ⋯⟩ ^ x_1) n = ⟨f b, ⋯⟩
⊢ x ^ m = f a

Tactic:
simpa using

Goal state after:
G : Type u_2
G' : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : IsCyclic G'
f : G →* G'
hf : f.ker ≤ center G
a b : G
x : G'
y : G
hxy : f y = x
hx : ∀ (a : ↥f.range), a ∈ zpowers ⟨x, ⋯⟩
m : ℤ
hm : (fun x_1 ↦ ⟨x, ⋯⟩ ^ x_1) m = ⟨f a, ⋯⟩
n : ℤ
hn : (fun x_1 ↦ ⟨x, ⋯⟩ ^ x_1) n = ⟨f b, ⋯⟩
⊢ x ^ m = f a
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: G : Type u_2
G' : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : IsCyclic G'
f : G →* G'
hf : f.ker ≤ center G
a b : G
x : G'
y : G
hxy : f y = x
hx : ∀ (a : ↥f.range), a ∈ zpowers ⟨x, ⋯⟩
m : ℤ
hm✝ : (fun x_1 ↦ ⟨x, ⋯⟩ ^ x_1) m = ⟨f a, ⋯⟩
n : ℤ
hn : (fun x_1 ↦ ⟨x, ⋯⟩ ^ x_1) n = ⟨f b, ⋯⟩
hm : x ^ m = f a
⊢ x ^ n = f b

Tactic:
simpa using

Goal state after:
G : Type u_2
G' : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : IsCyclic G'
f : G →* G'
hf : f.ker ≤ center G
a b : G
x : G'
y : G
hxy : f y = x
hx : ∀ (a : ↥f.range), a ∈ zpowers ⟨x, ⋯⟩
m : ℤ
hm✝ : (fun x_1 ↦ ⟨x, ⋯⟩ ^ x_1) m = ⟨f a, ⋯⟩
n : ℤ
hn : (fun x_1 ↦ ⟨x, ⋯⟩ ^ x_1) n = ⟨f b, ⋯⟩
hm : x ^ m = f a
⊢ x ^ n = f b
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: α : Type u_1
G : Type u_2
G' : Type u_3
a : α
p : ℕ
hp : Fact (Nat.Prime p)
⊢ Nat.Prime (Nat.card (ZMod p))

Tactic:
simpa using

Goal state after:
α : Type u_1
G : Type u_2
G' : Type u_3
a : α
p : ℕ
hp : Fact (Nat.Prime p)
⊢ Nat.Prime p
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
p : ℕ
hp : Nat.Prime p
hα : Nat.card α = p ^ 2
this✝¹ : Finite α
this✝ : Nontrivial α
h_cyc : ¬IsCyclic α
g : α
hg : g ≠ 1
this : orderOf g ∈ (p ^ 2).divisors
⊢ ∃ a < 3, p ^ a = orderOf g

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : Group α
p : ℕ
hp : Nat.Prime p
hα : Nat.card α = p ^ 2
this✝¹ : Finite α
this✝ : Nontrivial α
h_cyc : ¬IsCyclic α
g : α
hg : g ≠ 1
this : orderOf g ∈ (p ^ 2).divisors
⊢ ∃ a < 3, p ^ a = orderOf g
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
p : ℕ
hp : Nat.Prime p
hα : Nat.card α = p ^ 2
this✝² : Finite α
this✝¹ : Nontrivial α
h_cyc : ¬IsCyclic α
g : α
hg : g ≠ 1
this✝ : orderOf g ∈ (p ^ 2).divisors
this : ∃ a < 3, p ^ a = orderOf g
⊢ ?m.163

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : Group α
p : ℕ
hp : Nat.Prime p
hα : Nat.card α = p ^ 2
this✝² : Finite α
this✝¹ : Nontrivial α
h_cyc : ¬IsCyclic α
g : α
hg : g ≠ 1
this✝ : orderOf g ∈ (p ^ 2).divisors
this : ∃ a < 3, p ^ a = orderOf g
⊢ ?m.163
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: G : Type u_2
inst✝ : AddGroup G
g : G
hg : ∀ (x : G), x ∈ zmultiples g
n : ℕ
hn : Nat.card G = n
⊢ (zmodAddEquivOfGenerator hg hn) 1 = g

Tactic:
simpa using

Goal state after:
G : Type u_2
inst✝ : AddGroup G
g : G
hg : ∀ (x : G), x ∈ zmultiples g
n : ℕ
hn : Nat.card G = n
⊢ (zmodAddEquivOfGenerator hg hn) 1 = g
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: G : Type u_2
inst✝ : AddGroup G
g : G
hg : ∀ (x : G), x ∈ zmultiples g
n : ℕ
hn : Nat.card G = n
⊢ (zmodAddEquivOfGenerator hg hn).symm g = 1

Tactic:
simpa using

Goal state after:
G : Type u_2
inst✝ : AddGroup G
g : G
hg : ∀ (x : G), x ∈ zmultiples g
n : ℕ
hn : Nat.card G = n
⊢ (zmodAddEquivOfGenerator hg hn).symm g = 1
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: case h
G : Type u_2
inst✝¹ : CommGroup G
inst✝ : IsSimpleGroup G
g : G
hg : zpowers g = ⊤
⊢ Nat.Prime (orderOf g) ∧ Nonempty (Additive G ≃+ ZMod (orderOf g))

Tactic:
rw [orderOf_eq_card_of_zpowers_eq_top hg]

Goal state after:
case h
G : Type u_2
inst✝¹ : CommGroup G
inst✝ : IsSimpleGroup G
g : G
hg : zpowers g = ⊤
⊢ Nat.Prime (Nat.card G) ∧ Nonempty (Additive G ≃+ ZMod (Nat.card G))
Module: Mathlib.GroupTheory.Torsion

Goal state before:
pp: G : Type u_1
inst✝ : CommGroup G
p : ℕ
g : ↥(primaryComponent G p)
x✝ : ℕ
hk : ↑g ^ p ^ x✝ = 1
⊢ ↑(g ^ p ^ x✝) = ↑1

Tactic:
simpa using

Goal state after:
G : Type u_1
inst✝ : CommGroup G
p : ℕ
g : ↥(primaryComponent G p)
x✝ : ℕ
hk : ↑g ^ p ^ x✝ = 1
⊢ ↑g ^ p ^ x✝ = 1
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: G : Type u_2
inst✝¹ : Infinite G
inst✝ : AddGroup G
g : G
hg : zmultiples g = ⊤
⊢ Function.Bijective ⇑((zmultiplesHom G) g)

Tactic:
refine ⟨(AddMonoidHom.ker_eq_bot_iff _).mp ?_, AddMonoidHom.range_eq_top.mp hg⟩
  simp [zmultiplesHom_ker_eq, ← infinite_zmultiples, hg, Set.infinite_univ]

Goal state after:
Module: Mathlib.Order.Atoms.Finite

Goal state before:
pp: α : Type u_1
inst✝³ : LE α
inst✝² : BoundedOrder α
inst✝¹ : IsSimpleOrder α
inst✝ : DecidableEq α
a✝ : α
⊢ a✝ ∈ Finset.univ ↔ a✝ ∈ {⊤, ⊥}

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝³ : LE α
inst✝² : BoundedOrder α
inst✝¹ : IsSimpleOrder α
inst✝ : DecidableEq α
a✝ : α
⊢ a✝ = ⊤ ∨ a✝ = ⊥
Module: Mathlib.Order.Atoms.Finite

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a b : α
hab : a < b
⊢ ∃ x, a ⋖ x ∧ x ≤ b

Tactic:
obtain ⟨x, hx, hxmin⟩ := (LocallyFiniteOrder.finsetIoc a b).exists_minimal
      ⟨b, by simpa [LocallyFiniteOrder.finset_mem_Ioc]⟩

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a b : α
hab : a < b
x : α
hx : x ∈ LocallyFiniteOrder.finsetIoc a b
hxmin : ∀ ⦃y : α⦄, (fun x ↦ x ∈ LocallyFiniteOrder.finsetIoc a b) y → y ≤ x → x ≤ y
⊢ ∃ x, a ⋖ x ∧ x ≤ b
Module: Mathlib.Order.Atoms.Finite

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
a : α
inst✝ : IsStronglyAtomic α
ha : (Set.Ici a).Infinite
hfin : {x | a ⋖ x}.Finite
h : ∀ (b : α), a ⋖ b → (Set.Ici b).Finite
⊢ ∀ i ∈ {x | a ⋖ x}, (Set.Ici i).Finite

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝¹ : PartialOrder α
a : α
inst✝ : IsStronglyAtomic α
ha : (Set.Ici a).Infinite
hfin : {x | a ⋖ x}.Finite
h : ∀ (b : α), a ⋖ b → (Set.Ici b).Finite
⊢ ∀ (i : α), a ⋖ i → (Set.Ici i).Finite