mathlib-initiative/mathlib-tactics huggingface dataset:
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
d : ℕ
hd : d ∣ Fintype.card α
c : ℕ := Fintype.card α
hc0 : 0 < c
h0 : {a | orderOf a = d} = ∅
m : ℕ
hm : m ∈ c.divisors.erase d
hmc : m ∣ c
h1 : #{a | orderOf a = m} = 0
⊢ #{a | orderOf a = m} ≤ φ m

pp: case h.inr
α : 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 : ℕ
hm : m ∈ c.divisors.erase d
hmc : m ∣ c
h1 : #{a | orderOf a = m} > 0
⊢ #{a | orderOf a = m} ≤ φ m

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
d : ℕ
hd : d ∣ Fintype.card α
c : ℕ := Fintype.card α
hc0 : 0 < c
h0 : {a | orderOf a = d} = ∅
m : ℕ
hm : m ∈ c.divisors.erase d
hmc : m ∣ c
h1 : #{a | orderOf a = m} = 0
⊢ #{a | orderOf a = m} ≤ φ m
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 : ℕ
hd : d ∣ Fintype.card α
c : ℕ := Fintype.card α
hc0 : 0 < c
h0 : {a | orderOf a = d} = ∅
m : ℕ
hm : m ∈ c.divisors.erase d
hmc : m ∣ c
h1 : #{a | orderOf a = m} > 0
⊢ #{a | orderOf a = m} ≤ φ m

Tactic:
·

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 : ℕ
hd : d ∣ Fintype.card α
c : ℕ := Fintype.card α
hc0 : 0 < c
h0 : {a | orderOf a = d} = ∅
m : ℕ
hm : m ∈ c.divisors.erase d
hmc : m ∣ c
h1 : #{a | orderOf a = m} > 0
⊢ #{a | orderOf a = m} ≤ φ m
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: case refine_1
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : IsSimpleGroup α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
hα : orderOf g ≠ 1
n : ℕ
⊢ Subgroup.zpowers (g ^ n) = ⊥ → orderOf g ∣ n

pp: case refine_2
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : IsSimpleGroup α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
hα : orderOf g ≠ 1
n : ℕ
h : Subgroup.zpowers (g ^ n) = ⊤
⊢ n.Coprime (orderOf g)

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : IsSimpleGroup α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
hα : orderOf g ≠ 1
n : ℕ
⊢ Subgroup.zpowers (g ^ n) = ⊥ → orderOf g ∣ n
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: case refine_2
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : IsSimpleGroup α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
hα : orderOf g ≠ 1
n : ℕ
h : Subgroup.zpowers (g ^ n) = ⊤
⊢ n.Coprime (orderOf g)

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : IsSimpleGroup α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
hα : orderOf g ≠ 1
n : ℕ
h : Subgroup.zpowers (g ^ n) = ⊤
⊢ n.Coprime (orderOf g)
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: case h1
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : IsSimpleGroup α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
hα : orderOf g ≠ 1
h : ∀ (n : ℕ), orderOf g ∣ n ∨ n.Coprime (orderOf g)
⊢ 1 < orderOf g

pp: case h
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : IsSimpleGroup α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
hα : orderOf g ≠ 1
h : ∀ (n : ℕ), orderOf g ∣ n ∨ n.Coprime (orderOf g)
⊢ ∀ m < orderOf g, m ≠ 0 → (orderOf g).Coprime m

Tactic:
·

Goal state after:
case h1
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : IsSimpleGroup α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
hα : orderOf g ≠ 1
h : ∀ (n : ℕ), orderOf g ∣ n ∨ n.Coprime (orderOf g)
⊢ 1 < orderOf g
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: case h
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : IsSimpleGroup α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
hα : orderOf g ≠ 1
h : ∀ (n : ℕ), orderOf g ∣ n ∨ n.Coprime (orderOf g)
⊢ ∀ m < orderOf g, m ≠ 0 → (orderOf g).Coprime m

Tactic:
·

Goal state after:
case h
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : IsSimpleGroup α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
hα : orderOf g ≠ 1
h : ∀ (n : ℕ), orderOf g ∣ n ∨ n.Coprime (orderOf g)
⊢ ∀ m < orderOf g, m ≠ 0 → (orderOf g).Coprime m
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: case inr
A : Type u_4
inst✝³ : AddCommGroup A
inst✝² : LinearOrder A
inst✝¹ : IsOrderedAddMonoid A
inst✝ : Nontrivial A
g : A
hs : Function.Surjective fun x ↦ x • g
h_ne : g ≠ 0
this :
  ∀ {A : Type u_4} [inst : AddCommGroup A] [inst_1 : LinearOrder A] [IsOrderedAddMonoid A] [Nontrivial A] (g : A),
    (Function.Surjective fun x ↦ x • g) → g ≠ 0 → 0 < g → Nonempty (A ≃+o ℤ)
hg' : ¬0 < g
⊢ Nonempty (A ≃+o ℤ)

pp: A : Type u_4
inst✝³ : AddCommGroup A
inst✝² : LinearOrder A
inst✝¹ : IsOrderedAddMonoid A
inst✝ : Nontrivial A
g : A
hs : Function.Surjective fun x ↦ x • g
h_ne : g ≠ 0
hg' : 0 < g
⊢ Nonempty (A ≃+o ℤ)

Tactic:
·

Goal state after:
case inr
A : Type u_4
inst✝³ : AddCommGroup A
inst✝² : LinearOrder A
inst✝¹ : IsOrderedAddMonoid A
inst✝ : Nontrivial A
g : A
hs : Function.Surjective fun x ↦ x • g
h_ne : g ≠ 0
this :
  ∀ {A : Type u_4} [inst : AddCommGroup A] [inst_1 : LinearOrder A] [IsOrderedAddMonoid A] [Nontrivial A] (g : A),
    (Function.Surjective fun x ↦ x • g) → g ≠ 0 → 0 < g → Nonempty (A ≃+o ℤ)
hg' : ¬0 < g
⊢ Nonempty (A ≃+o ℤ)
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: case inl
α : Type u_1
inst✝ : Group α
this✝ : Finite α
this : Nontrivial α
h_cyc : IsCyclic α
hp : Nat.Prime 0
hα : Nat.card α = 0 ^ 2
h_exp : exponent α = 0
⊢ False

pp: case inr
α : Type u_1
inst✝ : Group α
this✝ : Finite α
this : Nontrivial α
h_cyc : IsCyclic α
hp : Nat.Prime 1
hα : Nat.card α = 1 ^ 2
h_exp : exponent α = 1
⊢ False

Tactic:
·

Goal state after:
case inl
α : Type u_1
inst✝ : Group α
this✝ : Finite α
this : Nontrivial α
h_cyc : IsCyclic α
hp : Nat.Prime 0
hα : Nat.card α = 0 ^ 2
h_exp : exponent α = 0
⊢ False
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: case inr
α : Type u_1
inst✝ : Group α
this✝ : Finite α
this : Nontrivial α
h_cyc : IsCyclic α
hp : Nat.Prime 1
hα : Nat.card α = 1 ^ 2
h_exp : exponent α = 1
⊢ False

Tactic:
·

Goal state after:
case inr
α : Type u_1
inst✝ : Group α
this✝ : Finite α
this : Nontrivial α
h_cyc : IsCyclic α
hp : Nat.Prime 1
hα : Nat.card α = 1 ^ 2
h_exp : exponent α = 1
⊢ False
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: case «0»
α : 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
a : ℕ
ha : 0 < 3
ha' : p ^ 0 = orderOf g
⊢ orderOf g = p

pp: case «1»
α : 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
a : ℕ
ha : 1 < 3
ha' : p ^ 1 = orderOf g
⊢ orderOf g = p

pp: case «2»
α : 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
a : ℕ
ha : 2 < 3
ha' : p ^ 2 = orderOf g
⊢ orderOf g = p

Tactic:
·

Goal state after:
case «0»
α : 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
a : ℕ
ha : 0 < 3
ha' : p ^ 0 = orderOf g
⊢ orderOf g = p
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: case «1»
α : 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
a : ℕ
ha : 1 < 3
ha' : p ^ 1 = orderOf g
⊢ orderOf g = p

pp: case «2»
α : 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
a : ℕ
ha : 2 < 3
ha' : p ^ 2 = orderOf g
⊢ orderOf g = p

Tactic:
·

Goal state after:
case «1»
α : 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
a : ℕ
ha : 1 < 3
ha' : p ^ 1 = orderOf g
⊢ orderOf g = p
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: case «2»
α : 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
a : ℕ
ha : 2 < 3
ha' : p ^ 2 = orderOf g
⊢ orderOf g = p

Tactic:
·

Goal state after:
case «2»
α : 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
a : ℕ
ha : 2 < 3
ha' : p ^ 2 = orderOf g
⊢ orderOf g = 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
this : ∃ a < 3, p ^ a = orderOf g
a : ℕ
ha : 2 < 3
ha' : p ^ 2 = orderOf g
⊢ orderOf g = Nat.card α

Tactic:
by lia

Goal state after:
Module: Mathlib.GroupTheory.Torsion

Goal state before:
pp: case zero
G : Type u_1
inst✝ : CommMonoid G
p : ℕ
hp : Fact (Nat.Prime p)
p' : ℕ
hp' : Fact (Nat.Prime p')
hne : p ≠ p'
g : G
hg' : ∃ n, orderOf g = p' ^ n
hn : orderOf g = p ^ 0
⊢ g = 1

pp: case succ
G : Type u_1
inst✝ : CommMonoid G
p : ℕ
hp : Fact (Nat.Prime p)
p' : ℕ
hp' : Fact (Nat.Prime p')
hne : p ≠ p'
g : G
hg' : ∃ n, orderOf g = p' ^ n
n : ℕ
hn : orderOf g = p ^ (n + 1)
⊢ g = 1

Tactic:
·

Goal state after:
case zero
G : Type u_1
inst✝ : CommMonoid G
p : ℕ
hp : Fact (Nat.Prime p)
p' : ℕ
hp' : Fact (Nat.Prime p')
hne : p ≠ p'
g : G
hg' : ∃ n, orderOf g = p' ^ n
hn : orderOf g = p ^ 0
⊢ g = 1
Module: Mathlib.GroupTheory.Torsion

Goal state before:
pp: case succ
G : Type u_1
inst✝ : CommMonoid G
p : ℕ
hp : Fact (Nat.Prime p)
p' : ℕ
hp' : Fact (Nat.Prime p')
hne : p ≠ p'
g : G
hg' : ∃ n, orderOf g = p' ^ n
n : ℕ
hn : orderOf g = p ^ (n + 1)
⊢ g = 1

Tactic:
·

Goal state after:
case succ
G : Type u_1
inst✝ : CommMonoid G
p : ℕ
hp : Fact (Nat.Prime p)
p' : ℕ
hp' : Fact (Nat.Prime p')
hne : p ≠ p'
g : G
hg' : ∃ n, orderOf g = p' ^ n
n : ℕ
hn : orderOf g = p ^ (n + 1)
⊢ g = 1
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: case h.left
G : Type u_2
inst✝¹ : CommGroup G
inst✝ : IsSimpleGroup G
g : G
hg : zpowers g = ⊤
⊢ Nat.Prime (Nat.card G)

pp: case h.right
G : Type u_2
inst✝¹ : CommGroup G
inst✝ : IsSimpleGroup G
g : G
hg : zpowers g = ⊤
⊢ Nonempty (Additive G ≃+ ZMod (Nat.card G))

Tactic:
·

Goal state after:
case h.left
G : Type u_2
inst✝¹ : CommGroup G
inst✝ : IsSimpleGroup G
g : G
hg : zpowers g = ⊤
⊢ Nat.Prime (Nat.card G)
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

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

Tactic:
·

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

Goal state before:
pp: case inl
M : Type u_4
N : Type u_5
inst✝³ : CommGroup M
inst✝² : Group N
f : M →* N
h : (Nat.card ↥f.ker).Coprime (Nat.card ↥f.range)
inst✝¹ : IsCyclic ↥f.ker
inst✝ : IsCyclic ↥f.range
h✝ : Infinite ↥f.ker
⊢ IsCyclic M

pp: case inr
M : Type u_4
N : Type u_5
inst✝³ : CommGroup M
inst✝² : Group N
f : M →* N
h : (Nat.card ↥f.ker).Coprime (Nat.card ↥f.range)
inst✝¹ : IsCyclic ↥f.ker
inst✝ : IsCyclic ↥f.range
h✝ : Finite ↥f.ker
⊢ IsCyclic M

Tactic:
·

Goal state after:
case inl
M : Type u_4
N : Type u_5
inst✝³ : CommGroup M
inst✝² : Group N
f : M →* N
h : (Nat.card ↥f.ker).Coprime (Nat.card ↥f.range)
inst✝¹ : IsCyclic ↥f.ker
inst✝ : IsCyclic ↥f.range
h✝ : Infinite ↥f.ker
⊢ IsCyclic M
Module: Mathlib.RingTheory.Coprime.Ideal

Goal state before:
pp: case refine_1
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
⊢ ∀ (a : ι), (∃ μ, ∑ i ∈ {a}, ↑(μ i) = 1) ↔ (↑{a}).Pairwise fun i j ↦ I i ⊔ I j = ⊤

pp: case refine_2
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
⊢ ∀ (a : ι) (s : Finset ι) (h : a ∉ s),
    s.Nonempty →
      ((∃ μ, ∑ i ∈ s, ↑(μ i) = 1) ↔ (↑s).Pairwise fun i j ↦ I i ⊔ I j = ⊤) →
        ((∃ μ, ∑ i ∈ Finset.cons a s h, ↑(μ i) = 1) ↔ (↑(Finset.cons a s h)).Pairwise fun i j ↦ I i ⊔ I j = ⊤)

Tactic:
·

Goal state after:
case refine_1
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
⊢ ∀ (a : ι), (∃ μ, ∑ i ∈ {a}, ↑(μ i) = 1) ↔ (↑{a}).Pairwise fun i j ↦ I i ⊔ I j = ⊤
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: case inr.inl
M : Type u_4
N : Type u_5
inst✝³ : CommGroup M
inst✝² : Group N
f : M →* N
h : (Nat.card ↥f.ker).Coprime (Nat.card ↥f.range)
inst✝¹ : IsCyclic ↥f.ker
inst✝ : IsCyclic ↥f.range
h✝¹ : Finite ↥f.ker
h✝ : Infinite ↥f.range
⊢ IsCyclic M

pp: case inr.inr
M : Type u_4
N : Type u_5
inst✝³ : CommGroup M
inst✝² : Group N
f : M →* N
h : (Nat.card ↥f.ker).Coprime (Nat.card ↥f.range)
inst✝¹ : IsCyclic ↥f.ker
inst✝ : IsCyclic ↥f.range
h✝¹ : Finite ↥f.ker
h✝ : Finite ↥f.range
⊢ IsCyclic M

Tactic:
·

Goal state after:
case inr.inl
M : Type u_4
N : Type u_5
inst✝³ : CommGroup M
inst✝² : Group N
f : M →* N
h : (Nat.card ↥f.ker).Coprime (Nat.card ↥f.range)
inst✝¹ : IsCyclic ↥f.ker
inst✝ : IsCyclic ↥f.range
h✝¹ : Finite ↥f.ker
h✝ : Infinite ↥f.range
⊢ IsCyclic M
Module: Mathlib.RingTheory.Coprime.Ideal

Goal state before:
pp: case refine_1.refine_1
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a i : ι
h : i = a
⊢ 1 ∈ ⨅ j ∈ {a}, ⨅ (_ : j ≠ i), I j

pp: case refine_1.refine_2
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
⊢ ↑((fun i ↦ if h : i = a then ⟨1, ⋯⟩ else 0) a) = 1

Tactic:
·

Goal state after:
case refine_1.refine_1
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a i : ι
h : i = a
⊢ 1 ∈ ⨅ j ∈ {a}, ⨅ (_ : j ≠ i), I j
Module: Mathlib.RingTheory.Coprime.Ideal

Goal state before:
pp: case refine_1.refine_2
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
⊢ ↑((fun i ↦ if h : i = a then ⟨1, ⋯⟩ else 0) a) = 1

Tactic:
·

Goal state after:
case refine_1.refine_2
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
⊢ ↑((fun i ↦ if h : i = a then ⟨1, ⋯⟩ else 0) a) = 1
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: case inr.inr.hm
M : Type u_4
N : Type u_5
inst✝³ : CommGroup M
inst✝² : Group N
f : M →* N
h : (Nat.card ↥f.ker).Coprime (Nat.card ↥f.range)
inst✝¹ : IsCyclic ↥f.ker
inst✝ : IsCyclic ↥f.range
h✝¹ : Finite ↥f.ker
h✝ : Finite ↥f.range
this : Finite M
⊢ Monoid.exponent ↥f.ker ∣ Monoid.exponent M

pp: case inr.inr.hn
M : Type u_4
N : Type u_5
inst✝³ : CommGroup M
inst✝² : Group N
f : M →* N
h : (Nat.card ↥f.ker).Coprime (Nat.card ↥f.range)
inst✝¹ : IsCyclic ↥f.ker
inst✝ : IsCyclic ↥f.range
h✝¹ : Finite ↥f.ker
h✝ : Finite ↥f.range
this : Finite M
⊢ Monoid.exponent ↥f.range ∣ Monoid.exponent M

Tactic:
·

Goal state after:
case inr.inr.hm
M : Type u_4
N : Type u_5
inst✝³ : CommGroup M
inst✝² : Group N
f : M →* N
h : (Nat.card ↥f.ker).Coprime (Nat.card ↥f.range)
inst✝¹ : IsCyclic ↥f.ker
inst✝ : IsCyclic ↥f.range
h✝¹ : Finite ↥f.ker
h✝ : Finite ↥f.range
this : Finite M
⊢ Monoid.exponent ↥f.ker ∣ Monoid.exponent M
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: case inr.inr.hm
M : Type u_4
N : Type u_5
inst✝³ : CommGroup M
inst✝² : Group N
f : M →* N
h : (Nat.card ↥f.ker).Coprime (Nat.card ↥f.range)
inst✝¹ : IsCyclic ↥f.ker
inst✝ : IsCyclic ↥f.range
h✝¹ : Finite ↥f.ker
h✝ : Finite ↥f.range
this : Finite M
⊢ Monoid.exponent ↥f.ker ∣ Monoid.exponent M

Tactic:
exact Monoid.exponent_dvd_of_monoidHom _ f.ker.subtype_injective

Goal state after:
Module: Mathlib.Order.CompactlyGenerated.Intervals

Goal state before:
pp: case refine_1
ι : Type u_1
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a : α
x✝ : ↑(Iic a)
s : Set α
hs : ∀ x ∈ s, IsCompactElement x
hx✝ : sSup s ≤ a
hx : ∀ b ∈ s, b ≤ a
f : ↑s → ↑(Iic a) := fun y ↦ ⟨↑y, ⋯⟩
⊢ ∀ x ∈ range f, IsCompactElement x

pp: case refine_2
ι : Type u_1
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a : α
x✝ : ↑(Iic a)
s : Set α
hs : ∀ x ∈ s, IsCompactElement x
hx✝ : sSup s ≤ a
hx : ∀ b ∈ s, b ≤ a
f : ↑s → ↑(Iic a) := fun y ↦ ⟨↑y, ⋯⟩
⊢ sSup (range f) = ⟨sSup s, hx✝⟩

Tactic:
·

Goal state after:
case refine_1
ι : Type u_1
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a : α
x✝ : ↑(Iic a)
s : Set α
hs : ∀ x ∈ s, IsCompactElement x
hx✝ : sSup s ≤ a
hx : ∀ b ∈ s, b ≤ a
f : ↑s → ↑(Iic a) := fun y ↦ ⟨↑y, ⋯⟩
⊢ ∀ x ∈ range f, IsCompactElement x
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: case inr.inr.hn
M : Type u_4
N : Type u_5
inst✝³ : CommGroup M
inst✝² : Group N
f : M →* N
h : (Nat.card ↥f.ker).Coprime (Nat.card ↥f.range)
inst✝¹ : IsCyclic ↥f.ker
inst✝ : IsCyclic ↥f.range
h✝¹ : Finite ↥f.ker
h✝ : Finite ↥f.range
this : Finite M
⊢ Monoid.exponent ↥f.range ∣ Monoid.exponent M

Tactic:
·

Goal state after:
case inr.inr.hn
M : Type u_4
N : Type u_5
inst✝³ : CommGroup M
inst✝² : Group N
f : M →* N
h : (Nat.card ↥f.ker).Coprime (Nat.card ↥f.range)
inst✝¹ : IsCyclic ↥f.ker
inst✝ : IsCyclic ↥f.range
h✝¹ : Finite ↥f.ker
h✝ : Finite ↥f.range
this : Finite M
⊢ Monoid.exponent ↥f.range ∣ Monoid.exponent M
Module: Mathlib.Order.CompactlyGenerated.Intervals

Goal state before:
pp: case refine_2
ι : Type u_1
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a : α
x✝ : ↑(Iic a)
s : Set α
hs : ∀ x ∈ s, IsCompactElement x
hx✝ : sSup s ≤ a
hx : ∀ b ∈ s, b ≤ a
f : ↑s → ↑(Iic a) := fun y ↦ ⟨↑y, ⋯⟩
⊢ sSup (range f) = ⟨sSup s, hx✝⟩

Tactic:
·

Goal state after:
case refine_2
ι : Type u_1
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a : α
x✝ : ↑(Iic a)
s : Set α
hs : ∀ x ∈ s, IsCompactElement x
hx✝ : sSup s ≤ a
hx : ∀ b ∈ s, b ≤ a
f : ↑s → ↑(Iic a) := fun y ↦ ⟨↑y, ⋯⟩
⊢ sSup (range f) = ⟨sSup s, hx✝⟩
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: case inl
M : Type u_4
N : Type u_5
inst✝³ : AddGroup M
inst✝² : AddGroup N
inst✝¹ : Infinite M
inst✝ : Nontrivial N
hMN : IsAddCyclic (ZMod 0 × ZMod (Nat.card N))
h✝ : Infinite N
⊢ False

pp: case inr
M : Type u_4
N : Type u_5
inst✝³ : AddGroup M
inst✝² : AddGroup N
inst✝¹ : Infinite M
inst✝ : Nontrivial N
hMN : IsAddCyclic (ZMod 0 × ZMod (Nat.card N))
h✝ : Finite N
⊢ False

Tactic:
·

Goal state after:
case inl
M : Type u_4
N : Type u_5
inst✝³ : AddGroup M
inst✝² : AddGroup N
inst✝¹ : Infinite M
inst✝ : Nontrivial N
hMN : IsAddCyclic (ZMod 0 × ZMod (Nat.card N))
h✝ : Infinite N
⊢ False
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: case refine_1
M : Type u_4
N : Type u_5
inst✝¹ : Group M
inst✝ : Group N
h : IsCyclic (M × N)
⊢ (Nat.card M).Coprime (Nat.card N)

pp: case refine_2
M : Type u_4
N : Type u_5
inst✝¹ : Group M
inst✝ : Group N
x✝ : IsCyclic M ∧ IsCyclic N ∧ (Nat.card M).Coprime (Nat.card N)
hM : IsCyclic M
hN : IsCyclic N
h : (Nat.card M).Coprime (Nat.card N)
⊢ IsCyclic (M × N)

Tactic:
·

Goal state after:
case refine_1
M : Type u_4
N : Type u_5
inst✝¹ : Group M
inst✝ : Group N
h : IsCyclic (M × N)
⊢ (Nat.card M).Coprime (Nat.card N)
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: case refine_1.inl
M : Type u_4
N : Type u_5
inst✝¹ : Group M
inst✝ : Group N
h : IsCyclic (M × N)
h✝ : Infinite M
⊢ (Nat.card M).Coprime (Nat.card N)

pp: case refine_1.inr
M : Type u_4
N : Type u_5
inst✝¹ : Group M
inst✝ : Group N
h : IsCyclic (M × N)
h✝ : Finite M
⊢ (Nat.card M).Coprime (Nat.card N)

Tactic:
·

Goal state after:
case refine_1.inl
M : Type u_4
N : Type u_5
inst✝¹ : Group M
inst✝ : Group N
h : IsCyclic (M × N)
h✝ : Infinite M
⊢ (Nat.card M).Coprime (Nat.card N)
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: case refine_1.inl.inl
M : Type u_4
N : Type u_5
inst✝¹ : Group M
inst✝ : Group N
h : IsCyclic (M × N)
h✝¹ : Infinite M
h✝ : Subsingleton N
⊢ (Nat.card M).Coprime (Nat.card N)

pp: case refine_1.inl.inr
M : Type u_4
N : Type u_5
inst✝¹ : Group M
inst✝ : Group N
h : IsCyclic (M × N)
h✝¹ : Infinite M
h✝ : Nontrivial N
⊢ (Nat.card M).Coprime (Nat.card N)

Tactic:
·

Goal state after:
case refine_1.inl.inl
M : Type u_4
N : Type u_5
inst✝¹ : Group M
inst✝ : Group N
h : IsCyclic (M × N)
h✝¹ : Infinite M
h✝ : Subsingleton N
⊢ (Nat.card M).Coprime (Nat.card N)
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: case refine_1.inr.inl
M : Type u_4
N : Type u_5
inst✝¹ : Group M
inst✝ : Group N
h : IsCyclic (M × N)
h✝¹ : Finite M
h✝ : Infinite N
⊢ (Nat.card M).Coprime (Nat.card N)

pp: case refine_1.inr.inr
M : Type u_4
N : Type u_5
inst✝¹ : Group M
inst✝ : Group N
h : IsCyclic (M × N)
h✝¹ : Finite M
h✝ : Finite N
⊢ (Nat.card M).Coprime (Nat.card N)

Tactic:
·

Goal state after:
case refine_1.inr.inl
M : Type u_4
N : Type u_5
inst✝¹ : Group M
inst✝ : Group N
h : IsCyclic (M × N)
h✝¹ : Finite M
h✝ : Infinite N
⊢ (Nat.card M).Coprime (Nat.card N)
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: case refine_1.inr.inl.inl
M : Type u_4
N : Type u_5
inst✝¹ : Group M
inst✝ : Group N
h : IsCyclic (M × N)
h✝² : Finite M
h✝¹ : Infinite N
h✝ : Subsingleton M
⊢ (Nat.card M).Coprime (Nat.card N)

pp: case refine_1.inr.inl.inr
M : Type u_4
N : Type u_5
inst✝¹ : Group M
inst✝ : Group N
h : IsCyclic (M × N)
h✝² : Finite M
h✝¹ : Infinite N
h✝ : Nontrivial M
⊢ (Nat.card M).Coprime (Nat.card N)

Tactic:
·

Goal state after:
case refine_1.inr.inl.inl
M : Type u_4
N : Type u_5
inst✝¹ : Group M
inst✝ : Group N
h : IsCyclic (M × N)
h✝² : Finite M
h✝¹ : Infinite N
h✝ : Subsingleton M
⊢ (Nat.card M).Coprime (Nat.card N)
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: case refine_2
M : Type u_4
N : Type u_5
inst✝¹ : Group M
inst✝ : Group N
x✝ : IsCyclic M ∧ IsCyclic N ∧ (Nat.card M).Coprime (Nat.card N)
hM : IsCyclic M
hN : IsCyclic N
h : (Nat.card M).Coprime (Nat.card N)
⊢ IsCyclic (M × N)

Tactic:
·

Goal state after:
case refine_2
M : Type u_4
N : Type u_5
inst✝¹ : Group M
inst✝ : Group N
x✝ : IsCyclic M ∧ IsCyclic N ∧ (Nat.card M).Coprime (Nat.card N)
hM : IsCyclic M
hN : IsCyclic N
h : (Nat.card M).Coprime (Nat.card N)
⊢ IsCyclic (M × N)
Module: Mathlib.Order.CompactlyGenerated.Intervals

Goal state before:
pp: case refine_1
ι : Type u_1
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
s : Set ι
f : ι → α
h' : ⨆ i ∈ s, f i = ⊤
i : ι
hi : i ∈ s
h : IsAtomistic ↑(Iic (f i))
u : Set ↑(Iic (f i))
hu : ⊤ = sSup u
hu' : ∀ a ∈ u, IsAtom a
⊢ f i = sSup (Subtype.val '' u)

pp: case refine_2
ι : Type u_1
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
s : Set ι
f : ι → α
h' : ⨆ i ∈ s, f i = ⊤
i : ι
hi : i ∈ s
h : IsAtomistic ↑(Iic (f i))
u : Set ↑(Iic (f i))
hu : ⊤ = sSup u
hu' : ∀ a ∈ u, IsAtom a
⊢ ∀ a ∈ Subtype.val '' u, IsAtom a

Tactic:
·

Goal state after:
case refine_1
ι : Type u_1
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
s : Set ι
f : ι → α
h' : ⨆ i ∈ s, f i = ⊤
i : ι
hi : i ∈ s
h : IsAtomistic ↑(Iic (f i))
u : Set ↑(Iic (f i))
hu : ⊤ = sSup u
hu' : ∀ a ∈ u, IsAtom a
⊢ f i = sSup (Subtype.val '' u)