mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ ∃ k, g ^ p ^ k = 1

Tactic:
]

Goal state after:
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
⊢ ∃ k, g ^ p ^ k = 1
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : exponent G = 0
⊢ exponent G = sSup (Set.range fun g ↦ orderOf g)

Tactic:
]

Goal state after:
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : exponent G = 0
⊢ exponent G = sSup (Set.range fun g ↦ orderOf g)
Module: Mathlib.GroupTheory.Exponent

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

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : ExponentExists G
⊢ exponent G = ?m.48

pp: case H
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : ExponentExists G
⊢ ∀ a ∈ Set.range fun g ↦ orderOf g, a ≤ ?m.48

pp: case H'
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : ExponentExists G
⊢ ∀ w < ?m.48, ∃ a ∈ Set.range fun g ↦ orderOf g, w < a

pp: G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : ExponentExists G
⊢ ℕ

Tactic:
]

Goal state after:
case H
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : ExponentExists G
⊢ ∀ a ∈ Set.range fun g ↦ orderOf g, a ≤ exponent G

case H'
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : ExponentExists G
⊢ ∀ w < exponent G, ∃ a ∈ Set.range fun g ↦ orderOf g, w < a
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:
]

Goal state after:
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
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case refine_2
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
⊢ zeroLocus ↑I ⊆ zeroLocus {x}

Tactic:
]

Goal state after:
case refine_2
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
⊢ zeroLocus ↑I ⊆ zeroLocus {x}
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case H'
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : ExponentExists G
x : ℕ
g : G
hx : x < orderOf g
hg : orderOf g = exponent G
⊢ ∃ a ∈ Set.range fun g ↦ orderOf g, x < a

Tactic:
]

Goal state after:
case H'
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : ExponentExists G
x : ℕ
g : G
hx : x < orderOf g
hg : orderOf g = exponent G
⊢ ∃ a ∈ Set.range fun g ↦ orderOf g, x < a
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 ↥(Subgroup.comap (QuotientGroup.mk' K) (Subgroup.map (QuotientGroup.mk' K) H))

Tactic:
]

Goal state after:
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 ↥(Subgroup.comap (QuotientGroup.mk' K) (Subgroup.map (QuotientGroup.mk' K) H))
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 ↥K

Tactic:
]

Goal state after:
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 ↥K
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case inr
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
this : s = ↑(basicOpen x)
⊢ (zeroLocus {y})ᶜ = (zeroLocus {y})ᶜ

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝¹ : CancelCommMonoid G
inst✝ : Fintype G
⊢ exponent G = iSup orderOf

Tactic:
]

Goal state after:
G : Type u
inst✝¹ : CancelCommMonoid G
inst✝ : Fintype G
⊢ exponent G = iSup orderOf
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₂
n₁ : ℕ
heq₁ : Nat.card ↥H₁ = p₁ ^ n₁
⊢ (p₁ ^ n₁).Coprime (Nat.card ↥H₂)

Tactic:
]

Goal state after:
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₂
n₁ : ℕ
heq₁ : Nat.card ↥H₁ = p₁ ^ n₁
⊢ (p₁ ^ n₁).Coprime (Nat.card ↥H₂)
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
j : ι
hj : ¬∃ n, 0 < n ∧ ∀ (g : M j), g ^ n = 1
⊢ ¬∃ n, 0 < n ∧ ∀ (g : (i : ι) → M i), g ^ n = 1

Tactic:
]

Goal state after:
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
j : ι
hj : ¬∃ n, 0 < n ∧ ∀ (g : M j), g ^ n = 1
⊢ ¬∃ n, 0 < n ∧ ∀ (g : (i : ι) → M i), g ^ n = 1
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
⊢ (∃ b a, a * b = 0 ∧ a + b = 1 ∧ s = ↑(basicOpen a)) ↔ ∃ e f, e * f = 0 ∧ e + f = 1 ∧ s = zeroLocus {e}

Tactic:
]

Goal state after:
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
⊢ (∃ b a, a * b = 0 ∧ a + b = 1 ∧ s = ↑(basicOpen a)) ↔ ∃ e f, e * f = 0 ∧ e + f = 1 ∧ s = zeroLocus {e}
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₂
n₁ n₂ : ℕ
heq₂ : Nat.card ↥H₂ = p₂ ^ n₂
⊢ (p₁ ^ n₁).Coprime (p₂ ^ n₂)

Tactic:
]

Goal state after:
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₂
n₁ n₂ : ℕ
heq₂ : Nat.card ↥H₂ = p₂ ^ n₂
⊢ (p₁ ^ n₁).Coprime (p₂ ^ n₂)
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
e f : R
⊢ (e * f = 0 ∧ e + f = 1) ∧ ?m.63 ↔ (e * f = 0 ∧ e + f = 1) ∧ s = zeroLocus {e}

pp: R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
e f : R
⊢ e * f = 0 ∧ e + f = 1 → (s = ↑(basicOpen f) ↔ ?m.63)

pp: R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
e f : R
⊢ Prop

Tactic:
]

Goal state after:
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
e f : R
⊢ e * f = 0 ∧ e + f = 1 → (s = ↑(basicOpen f) ↔ s = zeroLocus {e})
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
e f : R
mul : e * f = 0
add : e + f = 1
⊢ s = ↑(basicOpen f) ↔ s = ↑(basicOpen f)

Tactic:
]

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
m₁ : M₁
⊢ 1 = 1

Tactic:
]

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 }
⊢ basicOpen ((↑a).1 * (↑b).1) = basicOpen (↑a).1 ↔ a ≤ b

Tactic:
]

Goal state after:
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 }
⊢ basicOpen ((↑a).1 * (↑b).1) = basicOpen (↑a).1 ↔ a ≤ b
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 = basicOpen (↑a).1

Tactic:
]

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 }
h : basicOpen ((↑a).1 * (↑b).1) = basicOpen (↑a).1
⊢ a ⊓ b = a

Tactic:
]

Goal state after:
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 }
h : basicOpen ((↑a).1 * (↑b).1) = basicOpen (↑a).1
⊢ a ⊓ b = a
Module: Mathlib.GroupTheory.Exponent

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

Tactic:
]

Goal state after:
case refine_1
ι : Type u_1
inst✝¹ : Fintype ι
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
m : (i : ι) → M i
i : ι
⊢ orderOf (m i) ∣ univ.lcm fun x ↦ exponent (M x)
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s : Finset R
⊢ IsRetrocompact (zeroLocus ↑s)ᶜ

Tactic:
]

Goal state after:
R : Type u
inst✝ : CommSemiring R
s : Finset R
⊢ IsRetrocompact (zeroLocus ↑s)ᶜ
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

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

Tactic:
]

Goal state after:
case a
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal S
⊢ zeroLocus ↑I ⊆ zeroLocus (⇑f '' ↑(Ideal.comap f I))
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case refine_1.fst
M₁ : Type u_1
M₂ : Type u_2
inst✝¹ : Monoid M₁
inst✝ : Monoid M₂
g : M₁ × M₂
⊢ orderOf g.1 ∣ GCDMonoid.lcm (exponent M₁) (exponent M₂)

Tactic:
]

Goal state after:
case refine_1.fst
M₁ : Type u_1
M₂ : Type u_2
inst✝¹ : Monoid M₁
inst✝ : Monoid M₂
g : M₁ × M₂
⊢ orderOf g.1 ∣ GCDMonoid.lcm (exponent M₁) (exponent M₂)
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case refine_1.snd
M₁ : Type u_1
M₂ : Type u_2
inst✝¹ : Monoid M₁
inst✝ : Monoid M₂
g : M₁ × M₂
⊢ orderOf g.2 ∣ GCDMonoid.lcm (exponent M₁) (exponent M₂)

Tactic:
]

Goal state after:
case refine_1.snd
M₁ : Type u_1
M₂ : Type u_2
inst✝¹ : Monoid M₁
inst✝ : Monoid M₂
g : M₁ × M₂
⊢ orderOf g.2 ∣ GCDMonoid.lcm (exponent M₁) (exponent M₂)
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: case pos
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 : H = ⊤
h1 : Nat.card ↥H = 0
⊢ P ≤ H ∨ Disjoint H P

Tactic:
]

Goal state after:
case pos
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 : H = ⊤
h1 : Nat.card ↥H = 0
⊢ P ≤ H ∨ Disjoint H P
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: case pos
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 : H = ⊤
h1 : Nat.card ↥H = 0
⊢ P ≤ ⊤ ∨ Disjoint ⊤ P

Tactic:
]

Goal state after:
case pos
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 : H = ⊤
h1 : Nat.card ↥H = 0
⊢ P ≤ ⊤ ∨ Disjoint ⊤ P
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 : ∀ (x : S), IsIntegral R x
⊢ f.IsIntegral

Tactic:
]

Goal state after:
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 : ∀ (x : S), IsIntegral R x
⊢ f.IsIntegral
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 * (b * a) * b

Tactic:
]

Goal state after:
G : Type u
inst✝¹ : Monoid G
inst✝ : IsCancelMul G
a b : G
h : ∀ (g : G), g ^ 2 = 1
⊢ a * (a * b) * b = a * (b * a) * b
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 = 1

Tactic:
]

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})
⊢ 1 ∈ Ideal.span {X} ⊔ Ideal.comap (mapRingHom f) (Ideal.span {p})

Tactic:
]

Goal state after:
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})
⊢ 1 ∈ Ideal.span {X} ⊔ Ideal.comap (mapRingHom f) (Ideal.span {p})
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: case pos
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 : H = ⊥
h1 : ¬Nat.card ↥H = 0
h2 : H.index = 0
⊢ P ≤ H ∨ Disjoint H P

Tactic:
]

Goal state after:
case pos
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 : H = ⊥
h1 : ¬Nat.card ↥H = 0
h2 : H.index = 0
⊢ P ≤ H ∨ Disjoint H P
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: case pos
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 : H = ⊥
h1 : ¬Nat.card ↥H = 0
h2 : H.index = 0
⊢ P ≤ ⊥ ∨ Disjoint ⊥ P

Tactic:
]

Goal state after:
case pos
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 : H = ⊥
h1 : ¬Nat.card ↥H = 0
h2 : H.index = 0
⊢ P ≤ ⊥ ∨ Disjoint ⊥ P
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})
⊢ comap (mapRingHom f) '' zeroLocus ↑(Ideal.span {p}) ∩ zeroLocus ↑(Ideal.span {X}) = ∅

Tactic:
]

Goal state after:
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})
⊢ comap (mapRingHom f) '' zeroLocus ↑(Ideal.span {p}) ∩ zeroLocus ↑(Ideal.span {X}) = ∅
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
⊢ Nat.card ↥H * H.index ≠ 0

Tactic:
]

Goal state after:
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
⊢ Nat.card ↥H * H.index ≠ 0
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: case neg.refine_1
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
h3 : (Nat.card ↥H).Coprime (Nat.card ↥P) ∨ H.index.Coprime (Nat.card ↥P)
h4 : H.index.Coprime (Nat.card ↥P)
⊢ H.relIndex P = 1

Tactic:
]

Goal state after:
case neg.refine_1
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
h3 : (Nat.card ↥H).Coprime (Nat.card ↥P) ∨ H.index.Coprime (Nat.card ↥P)
h4 : H.index.Coprime (Nat.card ↥P)
⊢ H.relIndex P = 1
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: α : Type u_1
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → #{a | a ^ n = 1} ≤ n
a : α
b : ↥(zpowers a)
i : ℤ
hi : (fun x ↦ a ^ x) i = ↑b
⊢ 1 = 1

Tactic:
]

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

Goal state before:
pp: case refine_1
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
h : b.coeff 0 = 1
this : b.natTrailingDegree = 0
⊢ 1 = 1

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Fact (Nat.Prime p)
hG : Nat.card G = p ^ 2
⊢ p * Nat.card (G ⧸ center G) ∣ Nat.card ↥(center G) * (center G).index

Tactic:
]

Goal state after:
p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Fact (Nat.Prime p)
hG : Nat.card G = p ^ 2
⊢ p * Nat.card (G ⧸ center G) ∣ Nat.card ↥(center G) * (center G).index
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: p✝ : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
p : ℕ
inst✝ : Fact (Nat.Prime p)
H : Subgroup G
card_eq : Nat.card ↥H = p ^ (Nat.card G).factorization p
⊢ ¬p ^ ((Nat.card G).factorization p + 1) ∣ Nat.card G

Tactic:
]

Goal state after:
p✝ : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
p : ℕ
inst✝ : Fact (Nat.Prime p)
H : Subgroup G
card_eq : Nat.card ↥H = p ^ (Nat.card G).factorization p
⊢ ¬p ^ ((Nat.card G).factorization p + 1) ∣ Nat.card G
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
P : Sylow p G
K : Type u_2
inst✝ : Group K
ϕ : K →* G
N : Subgroup G
hϕ : IsPGroup p ↥ϕ.ker
h : ↑P ≤ ϕ.range
Q : Subgroup K
hQ : IsPGroup p ↥Q
hle : comap ϕ ↑P ≤ Q
⊢ Q = comap ϕ (map ϕ Q)

Tactic:
]

Goal state after:
p : ℕ
G : Type u_1
inst✝¹ : Group G
P : Sylow p G
K : Type u_2
inst✝ : Group K
ϕ : K →* G
N : Subgroup G
hϕ : IsPGroup p ↥ϕ.ker
h : ↑P ≤ ϕ.range
Q : Subgroup K
hQ : IsPGroup p ↥Q
hle : comap ϕ ↑P ≤ Q
⊢ Q = comap ϕ (map ϕ Q)
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
P : Sylow p G
K : Type u_2
inst✝ : Group K
ϕ : K →* G
N : Subgroup G
h : ↑P ≤ N
⊢ ↑P ≤ N

Tactic:
]

Goal state after:
p : ℕ
G : Type u_1
inst✝¹ : Group G
P : Sylow p G
K : Type u_2
inst✝ : Group K
ϕ : K →* G
N : Subgroup G
h : ↑P ≤ N
⊢ ↑P ≤ N
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝ : Group G
N : Subgroup G
P Q : Sylow p G
hP : ↑P ≤ N
hQ : ↑Q ≤ N
h : ∀ (x : ↥N), x ∈ P.subtype hP ↔ x ∈ Q.subtype hQ
⊢ ∀ (x : G), x ∈ P ↔ x ∈ Q

Tactic:
]

Goal state after:
p : ℕ
G : Type u_1
inst✝ : Group G
N : Subgroup G
P Q : Sylow p G
hP : ↑P ≤ N
hQ : ↑Q ≤ N
h : ∀ (x : ↥N), x ∈ P.subtype hP ↔ x ∈ Q.subtype hQ
⊢ ∀ (x : G), x ∈ P ↔ x ∈ Q
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝ : Group G
P : Subgroup G
hP : IsPGroup p ↥P
c : Set (Subgroup G)
hc1 : c ⊆ {Q | IsPGroup p ↥Q}
hc2 : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
Q : Subgroup G
hQ : Q ∈ c
x✝ : ↥{ carrier := ⋃ R, ↑↑R, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
g : G
S : ↑c
hg : g ∈ (fun R ↦ ↑↑R) S
k : ℕ
hk : ↑⟨g, hg⟩ ^ p ^ k = ↑1
⊢ ↑⟨g, ⋯⟩ ^ p ^ k = ↑1

Tactic:
]

Goal state after:
p : ℕ
G : Type u_1
inst✝ : Group G
P : Subgroup G
hP : IsPGroup p ↥P
c : Set (Subgroup G)
hc1 : c ⊆ {Q | IsPGroup p ↥Q}
hc2 : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
Q : Subgroup G
hQ : Q ∈ c
x✝ : ↥{ carrier := ⋃ R, ↑↑R, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
g : G
S : ↑c
hg : g ∈ (fun R ↦ ↑↑R) S
k : ℕ
hk : ↑⟨g, hg⟩ ^ p ^ k = ↑1
⊢ ↑⟨g, ⋯⟩ ^ p ^ k = ↑1
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝ : Group G
ι : Type u_2
s : Set ι
H : ι → Subgroup G
h : ∀ i ∈ s, IsPGroup p ↥(H i)
hn : ∀ i ∈ s, (H i).Normal
⊢ IsPGroup p ↥(⨆ i, H ↑i)

Tactic:
]

Goal state after:
p : ℕ
G : Type u_1
inst✝ : Group G
ι : Type u_2
s : Set ι
H : ι → Subgroup G
h : ∀ i ∈ s, IsPGroup p ↥(H i)
hn : ∀ i ∈ s, (H i).Normal
⊢ IsPGroup p ↥(⨆ i, H ↑i)
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Fact (Nat.Prime p)
hG : Nat.card G = p ^ 2
k : ℕ
hk0 : k > 0
hk : Nat.card ↥(center G) = p ^ k
⊢ p ∣ p ^ k

Tactic:
]

Goal state after:
p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Fact (Nat.Prime p)
hG : Nat.card G = p ^ 2
k : ℕ
hk0 : k > 0
hk : Nat.card ↥(center G) = p ^ k
⊢ p ∣ p ^ k
Module: Mathlib.Algebra.Module.ZMod

Goal state before:
pp: n : ℕ
M : Type u_1
M₁ : Type u_2
inst✝¹ : NeZero n
inst✝ : AddCommMonoid M
h : ∀ (x : M), n • x = 0
c : ℕ
x : M
this : (c % n) • x = c • x
⊢ (c % n) • x = c • x

Tactic:
]

Goal state after:
n : ℕ
M : Type u_1
M₁ : Type u_2
inst✝¹ : NeZero n
inst✝ : AddCommMonoid M
h : ∀ (x : M), n • x = 0
c : ℕ
x : M
this : (c % n) • x = c • x
⊢ (c % n) • x = c • x
Module: Mathlib.Algebra.Module.ZMod

Goal state before:
pp: n : ℕ
M : Type u_1
M₁ : Type u_2
inst✝¹ : NeZero n
inst✝ : AddCommMonoid M
h : ∀ (x : M), n • x = 0
c : ℕ
x : M
⊢ c • x = c • x

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Module.ZMod

Goal state before:
pp: n : ℕ
M : Type u_1
M₁ : Type u_2
F : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₁
inst✝³ : FunLike F M M₁
inst✝² : AddMonoidHomClass F M M₁
inst✝¹ : Module (ZMod n) M
inst✝ : Module (ZMod n) M₁
f : F
c : ZMod n
x : M
⊢ f (↑c.cast • x) = ↑c.cast • f x

Tactic:
]

Goal state after:
n : ℕ
M : Type u_1
M₁ : Type u_2
F : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₁
inst✝³ : FunLike F M M₁
inst✝² : AddMonoidHomClass F M M₁
inst✝¹ : Module (ZMod n) M
inst✝ : Module (ZMod n) M₁
f : F
c : ZMod n
x : M
⊢ f (↑c.cast • x) = ↑c.cast • f x