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

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

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
⊢ ↑(basicOpen x) ⊆ s

Tactic:
·

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

Goal state before:
pp: case h
G : Type u
inst✝ : CommMonoid G
hG : ExponentExists G
he : exponent G ≠ 0
hne : (Set.range orderOf).Nonempty
hfin : (Set.range orderOf).Finite
t : G
ht : orderOf t = sSup (Set.range orderOf)
p : ℕ
hp : Nat.Prime p
k : ℕ := (orderOf t).factorization p
hpe : k < (exponent G).factorization p
hk : k = (orderOf t).factorization p
g : G
hg : orderOf g = p ^ (exponent G).factorization p
hpk : p ^ k ∣ orderOf t
hpk' : orderOf (t ^ p ^ k) = orderOf t / p ^ k
a : ℕ
ha : (exponent G).factorization p = k + a + 1
hcoprime : (orderOf (t ^ p ^ k)).Coprime (orderOf g)
⊢ p ^ (orderOf t).factorization p ∣ orderOf t

Tactic:
·

Goal state after:
case h
G : Type u
inst✝ : CommMonoid G
hG : ExponentExists G
he : exponent G ≠ 0
hne : (Set.range orderOf).Nonempty
hfin : (Set.range orderOf).Finite
t : G
ht : orderOf t = sSup (Set.range orderOf)
p : ℕ
hp : Nat.Prime p
k : ℕ := (orderOf t).factorization p
hpe : k < (exponent G).factorization p
hk : k = (orderOf t).factorization p
g : G
hg : orderOf g = p ^ (exponent G).factorization p
hpk : p ^ k ∣ orderOf t
hpk' : orderOf (t ^ p ^ k) = orderOf t / p ^ k
a : ℕ
ha : (exponent G).factorization p = k + a + 1
hcoprime : (orderOf (t ^ p ^ k)).Coprime (orderOf g)
⊢ p ^ (orderOf t).factorization p ∣ orderOf t
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 = sSup (Set.range fun g ↦ orderOf g)

Tactic:
rw [← exponent_eq_zero_iff] at he
    rw [he, Set.Infinite.Nat.sSup_eq_zero <| (exponent_eq_zero_iff_range_orderOf_infinite h).1 he]

Goal state after:
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
⊢ ↑(basicOpen x) ⊆ s

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
⊢ ↑(basicOpen x) ⊆ s
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
⊢ ∀ a ∈ Set.range fun g ↦ orderOf g, a ≤ exponent G

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

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
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case pos
G : Type u
inst✝ : CommMonoid G
h : ∃ g, orderOf g = 0
⊢ exponent G = 0

pp: case neg
G : Type u
inst✝ : CommMonoid G
h : ¬∃ g, orderOf g = 0
⊢ exponent G = ⨆ g, orderOf g

Tactic:
·

Goal state after:
case pos
G : Type u
inst✝ : CommMonoid G
h : ∃ g, orderOf g = 0
⊢ exponent G = 0
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case neg
G : Type u
inst✝ : CommMonoid G
h : ¬∃ g, orderOf g = 0
⊢ exponent G = ⨆ g, orderOf g

Tactic:
·

Goal state after:
case neg
G : Type u
inst✝ : CommMonoid G
h : ¬∃ g, orderOf g = 0
⊢ exponent G = ⨆ g, orderOf g
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

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

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

Tactic:
·

Goal state after:
case refine_1
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
h : IsClopen s
⊢ ∃ e f, e * f = 0 ∧ e + f = 1 ∧ s = ↑(basicOpen e)
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case refine_1
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
x✝¹ x✝ : { e // e.1 * e.2 = 0 ∧ e.1 + e.2 = 1 }
x : R × R
hx : x.1 * x.2 = 0 ∧ x.1 + x.2 = 1
y : R × R
hy : y.1 * y.2 = 0 ∧ y.1 + y.2 = 1
eq :
  (fun e ↦ { carrier := ↑(basicOpen (↑e).1), isClopen' := ⋯ }) ⟨x, hx⟩ =
    (fun e ↦ { carrier := ↑(basicOpen (↑e).1), isClopen' := ⋯ }) ⟨y, hy⟩
⊢ (↑⟨x, hx⟩).1 = (↑⟨y, hy⟩).1

pp: case refine_2
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
s : Clopens (PrimeSpectrum R)
⊢ ∃ a, (fun e ↦ { carrier := ↑(basicOpen (↑e).1), isClopen' := ⋯ }) a = s

Tactic:
·

Goal state after:
case refine_1
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
x✝¹ x✝ : { e // e.1 * e.2 = 0 ∧ e.1 + e.2 = 1 }
x : R × R
hx : x.1 * x.2 = 0 ∧ x.1 + x.2 = 1
y : R × R
hy : y.1 * y.2 = 0 ∧ y.1 + y.2 = 1
eq :
  (fun e ↦ { carrier := ↑(basicOpen (↑e).1), isClopen' := ⋯ }) ⟨x, hx⟩ =
    (fun e ↦ { carrier := ↑(basicOpen (↑e).1), isClopen' := ⋯ }) ⟨y, hy⟩
⊢ (↑⟨x, hx⟩).1 = (↑⟨y, hy⟩).1
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case refine_2
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
s : Clopens (PrimeSpectrum R)
⊢ ∃ a, (fun e ↦ { carrier := ↑(basicOpen (↑e).1), isClopen' := ⋯ }) a = s

Tactic:
·

Goal state after:
case refine_2
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
s : Clopens (PrimeSpectrum R)
⊢ ∃ a, (fun e ↦ { carrier := ↑(basicOpen (↑e).1), isClopen' := ⋯ }) a = s
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)
⊢ exponent ((i : ι) → M i) ∣ univ.lcm fun x ↦ exponent (M x)

pp: case refine_2
ι : Type u_1
inst✝¹ : Fintype ι
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
⊢ (univ.lcm fun x ↦ exponent (M x)) ∣ exponent ((i : ι) → M i)

Tactic:
·

Goal state after:
case refine_1
ι : 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)
Module: Mathlib.GroupTheory.Exponent

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

Tactic:
·

Goal state after:
case refine_2
ι : Type u_1
inst✝¹ : Fintype ι
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
⊢ (univ.lcm fun x ↦ exponent (M x)) ∣ exponent ((i : ι) → M i)
Module: Mathlib.GroupTheory.Exponent

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

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

Goal state after:
case refine_1
M₁ : Type u_1
M₂ : Type u_2
inst✝¹ : Monoid M₁
inst✝ : Monoid M₂
⊢ exponent (M₁ × M₂) ∣ GCDMonoid.lcm (exponent M₁) (exponent M₂)
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
⊢ closure (comap f '' zeroLocus ↑I) ⊆ zeroLocus ↑(Ideal.comap f I)

pp: case a
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal S
⊢ zeroLocus ↑(Ideal.comap f I) ⊆ closure (comap f '' zeroLocus ↑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
⊢ closure (comap f '' zeroLocus ↑I) ⊆ zeroLocus ↑(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₂
⊢ (g ^ GCDMonoid.lcm (exponent M₁) (exponent M₂)).1 = 1.1

pp: case refine_1.snd
M₁ : Type u_1
M₂ : Type u_2
inst✝¹ : Monoid M₁
inst✝ : Monoid M₂
g : M₁ × M₂
⊢ (g ^ GCDMonoid.lcm (exponent M₁) (exponent M₂)).2 = 1.2

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₂
⊢ (g ^ GCDMonoid.lcm (exponent M₁) (exponent M₂)).1 = 1.1
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 : (Nat.card ↥H).Coprime H.index
h1 : Nat.card ↥H = 0
⊢ P ≤ H ∨ Disjoint H P

pp: case neg
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
⊢ 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 : (Nat.card ↥H).Coprime H.index
h1 : Nat.card ↥H = 0
⊢ P ≤ H ∨ Disjoint H P
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 ↑(Ideal.comap f I) ⊆ closure (comap f '' zeroLocus ↑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 ↑(Ideal.comap f I) ⊆ closure (comap f '' zeroLocus ↑I)
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₂
⊢ (g ^ GCDMonoid.lcm (exponent M₁) (exponent M₂)).2 = 1.2

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₂
⊢ (g ^ GCDMonoid.lcm (exponent M₁) (exponent M₂)).2 = 1.2
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:
·

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

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

Tactic:
·

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: 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 : (Nat.card ↥H).Coprime H.index
h1 : ¬Nat.card ↥H = 0
h2 : H.index = 0
⊢ P ≤ H ∨ Disjoint H P

pp: case neg
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
⊢ 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 : (Nat.card ↥H).Coprime H.index
h1 : ¬Nat.card ↥H = 0
h2 : H.index = 0
⊢ P ≤ H ∨ Disjoint H P
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
⊢ (b.reverse * X ^ (1 + c.natDegree)).Monic

pp: case refine_2
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
⊢ eval₂ (algebraMap R S) r (b.reverse * X ^ (1 + c.natDegree)) = 0

Tactic:
·

Goal state after:
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
⊢ (b.reverse * X ^ (1 + c.natDegree)).Monic
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)
⊢ P ≤ H

pp: case neg.refine_2
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 : (Nat.card ↥H).Coprime (Nat.card ↥P)
⊢ Disjoint H P

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)
⊢ P ≤ H
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: case neg.refine_2
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 : (Nat.card ↥H).Coprime (Nat.card ↥P)
⊢ Disjoint H P

Tactic:
·

Goal state after:
case neg.refine_2
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 : (Nat.card ↥H).Coprime (Nat.card ↥P)
⊢ Disjoint H P
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Fact (Nat.Prime p)
P : Subgroup G
hP1 : IsPGroup p ↥P
hP2 : ¬p ∣ P.index
Q : Subgroup G
hQ : IsPGroup p ↥Q
hPQ : P ≤ Q
this : P.FiniteIndex
k : ℕ
hk : Nat.card (↥Q ⧸ P.normalCore.subgroupOf Q) = p ^ k
⊢ Q = P

Tactic:
have h := hk ▸ Nat.Prime.coprime_pow_of_not_dvd (m := k) Fact.out hP2

Goal state after:
p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Fact (Nat.Prime p)
P : Subgroup G
hP1 : IsPGroup p ↥P
hP2 : ¬p ∣ P.index
Q : Subgroup G
hQ : IsPGroup p ↥Q
hPQ : P ≤ Q
this : P.FiniteIndex
k : ℕ
hk : Nat.card (↥Q ⧸ P.normalCore.subgroupOf Q) = p ^ k
h : P.index.Coprime (Nat.card (↥Q ⧸ P.normalCore.subgroupOf Q))
⊢ Q = P
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case refine_2
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
⊢ eval₂ (algebraMap R S) r (b.reverse * X ^ (1 + c.natDegree)) = 0

Tactic:
·

Goal state after:
case refine_2
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
⊢ eval₂ (algebraMap R S) r (b.reverse * X ^ (1 + c.natDegree)) = 0
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: case h.inl
α : Type u_1
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → #{a | a ^ n = 1} ≤ n
IH : ∀ m < 0, m ∣ Fintype.card α → 0 < #{a | orderOf a = m} → #{a | orderOf a = m} = φ m
hd : 0 ∣ Fintype.card α
hpos : 0 < #{a | orderOf a = 0}
⊢ #{a | orderOf a = 0} = φ 0

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 | orderOf a = d} = φ d

Tactic:
·

Goal state after:
case h.inl
α : Type u_1
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → #{a | a ^ n = 1} ≤ n
IH : ∀ m < 0, m ∣ Fintype.card α → 0 < #{a | orderOf a = m} → #{a | orderOf a = m} = φ m
hd : 0 ∣ Fintype.card α
hpos : 0 < #{a | orderOf a = 0}
⊢ #{a | orderOf a = 0} = φ 0
Module: Mathlib.GroupTheory.Rank

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝³ : Group G
inst✝² : Group H
inst✝¹ : FG G
inst✝ : FG H
f : G →* H
hf : Surjective ⇑f
S : Finset G
hS1 : S.card = rank G
hS2 : Subgroup.closure ↑S = ⊤
⊢ rank H ≤ (Finset.image (⇑f) S).card

pp: G : Type u_1
H : Type u_2
inst✝³ : Group G
inst✝² : Group H
inst✝¹ : FG G
inst✝ : FG H
f : G →* H
hf : Surjective ⇑f
S : Finset G
hS1 : S.card = rank G
hS2 : Subgroup.closure ↑S = ⊤
⊢ (Finset.image (⇑f) S).card ≤ rank G

Tactic:
·

Goal state after:
G : Type u_1
H : Type u_2
inst✝³ : Group G
inst✝² : Group H
inst✝¹ : FG G
inst✝ : FG H
f : G →* H
hf : Surjective ⇑f
S : Finset G
hS1 : S.card = rank G
hS2 : Subgroup.closure ↑S = ⊤
⊢ rank H ≤ (Finset.image (⇑f) S).card
Module: Mathlib.GroupTheory.Rank

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝³ : Group G
inst✝² : Group H
inst✝¹ : FG G
inst✝ : FG H
f : G →* H
hf : Surjective ⇑f
S : Finset G
hS1 : S.card = rank G
hS2 : Subgroup.closure ↑S = ⊤
⊢ (Finset.image (⇑f) S).card ≤ rank G

Tactic:
·

Goal state after:
G : Type u_1
H : Type u_2
inst✝³ : Group G
inst✝² : Group H
inst✝¹ : FG G
inst✝ : FG H
f : G →* H
hf : Surjective ⇑f
S : Finset G
hS1 : S.card = rank G
hS2 : Subgroup.closure ↑S = ⊤
⊢ (Finset.image (⇑f) S).card ≤ rank G
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝ : Group G
H : Subgroup G
P : Sylow p G
⊢ P ∈ fixedPoints (↥H) (Sylow p G) ↔ ∀ ⦃x : G⦄, x ∈ H → x ∈ normalizer ↑P

Tactic:
← Sylow.smul_eq_iff_mem_normalizer

Goal state after:
p : ℕ
G : Type u_1
inst✝ : Group G
H : Subgroup G
P : Sylow p G
⊢ P ∈ fixedPoints (↥H) (Sylow p G) ↔ ∀ ⦃x : G⦄, x ∈ H → x • P = P
Module: Mathlib.GroupTheory.Rank

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s : Finset G
t : Finset ↥(closure ↑s) := s.preimage Subtype.val ⋯
ht : closure ↑t = ⊤
H : Set.InjOn Subtype.val ↑t
⊢ t.card ≤ s.card

Tactic:
rw [← Finset.card_image_of_injOn H, Finset.image_preimage]

Goal state after:
G : Type u_1
inst✝ : Group G
s : Finset G
t : Finset ↥(closure ↑s) := s.preimage Subtype.val ⋯
ht : closure ↑t = ⊤
H : Set.InjOn Subtype.val ↑t
⊢ {x ∈ s | x ∈ Set.range Subtype.val}.card ≤ s.card
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case mp
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
⊢ vanishingIdeal s ∈ minimalPrimes R → closure s ∈ irreducibleComponents (PrimeSpectrum R)

pp: case mpr
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
⊢ closure s ∈ irreducibleComponents (PrimeSpectrum R) → vanishingIdeal s ∈ minimalPrimes R

Tactic:
·

Goal state after:
case mp
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
⊢ vanishingIdeal s ∈ minimalPrimes R → closure s ∈ irreducibleComponents (PrimeSpectrum R)
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case mpr
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
⊢ closure s ∈ irreducibleComponents (PrimeSpectrum R) → vanishingIdeal s ∈ minimalPrimes R

Tactic:
·

Goal state after:
case mpr
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
⊢ closure s ∈ irreducibleComponents (PrimeSpectrum R) → vanishingIdeal s ∈ minimalPrimes R
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
d : ℕ
hd : d ∣ Fintype.card α
c : ℕ := Fintype.card α
hc0 : 0 < c
h0 : {a | orderOf a = d} = ∅
⊢ ∑ m ∈ c.divisors, #{a | orderOf a = m} = ∑ m ∈ c.divisors.erase d, #{a | orderOf a = m}

Tactic:
by
      rw [eq_comm]
      refine sum_subset (erase_subset _ _) fun m hm₁ hm₂ => ?_
      have : m = d := by
        contrapose! hm₂
        exact mem_erase_of_ne_of_mem hm₂ hm₁
      simp [this, h0]

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

Goal state before:
pp: case mp
R : Type u
inst✝¹ : CommSemiring R
inst✝ : IsLocalRing R
U : TopologicalSpace.Opens (PrimeSpectrum R)
⊢ closedPoint R ∈ U → U = ⊤

pp: case mpr
R : Type u
inst✝¹ : CommSemiring R
inst✝ : IsLocalRing R
U : TopologicalSpace.Opens (PrimeSpectrum R)
⊢ U = ⊤ → closedPoint R ∈ U

Tactic:
·

Goal state after:
case mp
R : Type u
inst✝¹ : CommSemiring R
inst✝ : IsLocalRing R
U : TopologicalSpace.Opens (PrimeSpectrum R)
⊢ closedPoint R ∈ U → U = ⊤
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case mpr
R : Type u
inst✝¹ : CommSemiring R
inst✝ : IsLocalRing R
U : TopologicalSpace.Opens (PrimeSpectrum R)
⊢ U = ⊤ → closedPoint R ∈ U

Tactic:
·

Goal state after:
case mpr
R : Type u
inst✝¹ : CommSemiring R
inst✝ : IsLocalRing R
U : TopologicalSpace.Opens (PrimeSpectrum R)
⊢ U = ⊤ → closedPoint R ∈ U