[GOAL]
G : Type u
inst✝ : Monoid G
⊢ ExponentExists G ↔ exponent G ≠ 0
[PROOFSTEP]
rw [exponent]
[GOAL]
G : Type u
inst✝ : Monoid G
⊢ ExponentExists G ↔ (if h : ExponentExists G then Nat.find h else 0) ≠ 0
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
G : Type u
inst✝ : Monoid G
h : ExponentExists G
⊢ ExponentExists G ↔ Nat.find h ≠ 0
[PROOFSTEP]
simp [h, @not_lt_zero' ℕ]
  --if this isn't done this way, `to_additive` freaks
[GOAL]
case neg
G : Type u
inst✝ : Monoid G
h : ¬ExponentExists G
⊢ ExponentExists G ↔ 0 ≠ 0
[PROOFSTEP]
tauto
[GOAL]
G : Type u
inst✝ : Monoid G
⊢ exponent G = 0 ↔ ¬ExponentExists G
[PROOFSTEP]
simp only [exponentExists_iff_ne_zero, Classical.not_not]
[GOAL]
G : Type u
inst✝ : Monoid G
g : G
⊢ g ^ exponent G = 1
[PROOFSTEP]
by_cases ExponentExists G
[GOAL]
G : Type u
inst✝ : Monoid G
g : G
⊢ g ^ exponent G = 1
[PROOFSTEP]
by_cases ExponentExists G
[GOAL]
case pos
G : Type u
inst✝ : Monoid G
g : G
h : ExponentExists G
⊢ g ^ exponent G = 1
[PROOFSTEP]
simp_rw [exponent, dif_pos h]
[GOAL]
case pos
G : Type u
inst✝ : Monoid G
g : G
h : ExponentExists G
⊢ g ^ Nat.find h = 1
[PROOFSTEP]
exact (Nat.find_spec h).2 g
[GOAL]
case neg
G : Type u
inst✝ : Monoid G
g : G
h : ¬ExponentExists G
⊢ g ^ exponent G = 1
[PROOFSTEP]
simp_rw [exponent, dif_neg h, pow_zero]
[GOAL]
G : Type u
inst✝ : Monoid G
n : ℕ
g : G
⊢ g ^ n = g ^ (n % exponent G + exponent G * (n / exponent G))
[PROOFSTEP]
rw [Nat.mod_add_div]
[GOAL]
G : Type u
inst✝ : Monoid G
n : ℕ
g : G
⊢ g ^ (n % exponent G + exponent G * (n / exponent G)) = g ^ (n % exponent G)
[PROOFSTEP]
simp [pow_add, pow_mul, pow_exponent_eq_one]
[GOAL]
G : Type u
inst✝ : Monoid G
n : ℕ
hpos : 0 < n
hG : ∀ (g : G), g ^ n = 1
⊢ 0 < exponent G
[PROOFSTEP]
have h : ∃ n, 0 < n ∧ ∀ g : G, g ^ n = 1 := ⟨n, hpos, hG⟩
[GOAL]
G : Type u
inst✝ : Monoid G
n : ℕ
hpos : 0 < n
hG : ∀ (g : G), g ^ n = 1
h : ∃ n, 0 < n ∧ ∀ (g : G), g ^ n = 1
⊢ 0 < exponent G
[PROOFSTEP]
rw [exponent, dif_pos]
[GOAL]
G : Type u
inst✝ : Monoid G
n : ℕ
hpos : 0 < n
hG : ∀ (g : G), g ^ n = 1
h : ∃ n, 0 < n ∧ ∀ (g : G), g ^ n = 1
⊢ 0 < Nat.find ?hc
case hc
G : Type u
inst✝ : Monoid G
n : ℕ
hpos : 0 < n
hG : ∀ (g : G), g ^ n = 1
h : ∃ n, 0 < n ∧ ∀ (g : G), g ^ n = 1
⊢ ExponentExists G
[PROOFSTEP]
exact (Nat.find_spec h).1
[GOAL]
G : Type u
inst✝ : Monoid G
n : ℕ
hpos : 0 < n
hG : ∀ (g : G), g ^ n = 1
⊢ exponent G ≤ n
[PROOFSTEP]
rw [exponent, dif_pos]
[GOAL]
G : Type u
inst✝ : Monoid G
n : ℕ
hpos : 0 < n
hG : ∀ (g : G), g ^ n = 1
⊢ Nat.find ?hc ≤ n
[PROOFSTEP]
apply Nat.find_min'
[GOAL]
case h
G : Type u
inst✝ : Monoid G
n : ℕ
hpos : 0 < n
hG : ∀ (g : G), g ^ n = 1
⊢ 0 < n ∧ ∀ (g : G), g ^ n = 1
[PROOFSTEP]
exact ⟨hpos, hG⟩
[GOAL]
case hc
G : Type u
inst✝ : Monoid G
n : ℕ
hpos : 0 < n
hG : ∀ (g : G), g ^ n = 1
⊢ ExponentExists G
[PROOFSTEP]
exact ⟨n, hpos, hG⟩
[GOAL]
G : Type u
inst✝ : Monoid G
m : ℕ
hpos : 0 < m
hm : m < exponent G
⊢ ∃ g, g ^ m ≠ 1
[PROOFSTEP]
by_contra' h
[GOAL]
G : Type u
inst✝ : Monoid G
m : ℕ
hpos : 0 < m
hm : m < exponent G
h : ∀ (g : G), g ^ m = 1
⊢ False
[PROOFSTEP]
have hcon : exponent G ≤ m := exponent_min' m hpos h
[GOAL]
G : Type u
inst✝ : Monoid G
m : ℕ
hpos : 0 < m
hm : m < exponent G
h : ∀ (g : G), g ^ m = 1
hcon : exponent G ≤ m
⊢ False
[PROOFSTEP]
linarith
[GOAL]
G : Type u
inst✝¹ : Monoid G
inst✝ : Subsingleton G
⊢ exponent G = 1
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
G : Type u
inst✝¹ : Monoid G
inst✝ : Subsingleton G
⊢ exponent G ≤ 1
[PROOFSTEP]
apply exponent_min' _ Nat.one_pos
[GOAL]
case a
G : Type u
inst✝¹ : Monoid G
inst✝ : Subsingleton G
⊢ ∀ (g : G), g ^ 1 = 1
[PROOFSTEP]
simp
[GOAL]
case a
G : Type u
inst✝¹ : Monoid G
inst✝ : Subsingleton G
⊢ 1 ≤ exponent G
[PROOFSTEP]
apply Nat.succ_le_of_lt
[GOAL]
case a.h
G : Type u
inst✝¹ : Monoid G
inst✝ : Subsingleton G
⊢ 0 < exponent G
[PROOFSTEP]
apply exponent_pos_of_exists 1 Nat.one_pos
[GOAL]
case a.h
G : Type u
inst✝¹ : Monoid G
inst✝ : Subsingleton G
⊢ ∀ (g : G), g ^ 1 = 1
[PROOFSTEP]
simp
[GOAL]
G✝ : Type u
inst✝¹ : Monoid G✝
G : Type u_1
inst✝ : Monoid G
n : ℕ
hG : ∀ (g : G), g ^ n = 1
⊢ exponent G ∣ n
[PROOFSTEP]
rcases n.eq_zero_or_pos with (rfl | hpos)
[GOAL]
case inl
G✝ : Type u
inst✝¹ : Monoid G✝
G : Type u_1
inst✝ : Monoid G
hG : ∀ (g : G), g ^ 0 = 1
⊢ exponent G ∣ 0
[PROOFSTEP]
exact dvd_zero _
[GOAL]
case inr
G✝ : Type u
inst✝¹ : Monoid G✝
G : Type u_1
inst✝ : Monoid G
n : ℕ
hG : ∀ (g : G), g ^ n = 1
hpos : n > 0
⊢ exponent G ∣ n
[PROOFSTEP]
apply Nat.dvd_of_mod_eq_zero
[GOAL]
case inr.H
G✝ : Type u
inst✝¹ : Monoid G✝
G : Type u_1
inst✝ : Monoid G
n : ℕ
hG : ∀ (g : G), g ^ n = 1
hpos : n > 0
⊢ n % exponent G = 0
[PROOFSTEP]
by_contra h
[GOAL]
case inr.H
G✝ : Type u
inst✝¹ : Monoid G✝
G : Type u_1
inst✝ : Monoid G
n : ℕ
hG : ∀ (g : G), g ^ n = 1
hpos : n > 0
h : ¬n % exponent G = 0
⊢ False
[PROOFSTEP]
have h₁ := Nat.pos_of_ne_zero h
[GOAL]
case inr.H
G✝ : Type u
inst✝¹ : Monoid G✝
G : Type u_1
inst✝ : Monoid G
n : ℕ
hG : ∀ (g : G), g ^ n = 1
hpos : n > 0
h : ¬n % exponent G = 0
h₁ : 0 < n % exponent G
⊢ False
[PROOFSTEP]
have h₂ : n % exponent G < exponent G := Nat.mod_lt _ (exponent_pos_of_exists n hpos hG)
[GOAL]
case inr.H
G✝ : Type u
inst✝¹ : Monoid G✝
G : Type u_1
inst✝ : Monoid G
n : ℕ
hG : ∀ (g : G), g ^ n = 1
hpos : n > 0
h : ¬n % exponent G = 0
h₁ : 0 < n % exponent G
h₂ : n % exponent G < exponent G
⊢ False
[PROOFSTEP]
have h₃ : exponent G ≤ n % exponent G := by
  apply exponent_min' _ h₁
  simp_rw [← pow_eq_mod_exponent]
  exact hG
[GOAL]
G✝ : Type u
inst✝¹ : Monoid G✝
G : Type u_1
inst✝ : Monoid G
n : ℕ
hG : ∀ (g : G), g ^ n = 1
hpos : n > 0
h : ¬n % exponent G = 0
h₁ : 0 < n % exponent G
h₂ : n % exponent G < exponent G
⊢ exponent G ≤ n % exponent G
[PROOFSTEP]
apply exponent_min' _ h₁
[GOAL]
G✝ : Type u
inst✝¹ : Monoid G✝
G : Type u_1
inst✝ : Monoid G
n : ℕ
hG : ∀ (g : G), g ^ n = 1
hpos : n > 0
h : ¬n % exponent G = 0
h₁ : 0 < n % exponent G
h₂ : n % exponent G < exponent G
⊢ ∀ (g : G), g ^ (n % exponent G) = 1
[PROOFSTEP]
simp_rw [← pow_eq_mod_exponent]
[GOAL]
G✝ : Type u
inst✝¹ : Monoid G✝
G : Type u_1
inst✝ : Monoid G
n : ℕ
hG : ∀ (g : G), g ^ n = 1
hpos : n > 0
h : ¬n % exponent G = 0
h₁ : 0 < n % exponent G
h₂ : n % exponent G < exponent G
⊢ ∀ (g : G), g ^ n = 1
[PROOFSTEP]
exact hG
[GOAL]
case inr.H
G✝ : Type u
inst✝¹ : Monoid G✝
G : Type u_1
inst✝ : Monoid G
n : ℕ
hG : ∀ (g : G), g ^ n = 1
hpos : n > 0
h : ¬n % exponent G = 0
h₁ : 0 < n % exponent G
h₂ : n % exponent G < exponent G
h₃ : exponent G ≤ n % exponent G
⊢ False
[PROOFSTEP]
linarith
[GOAL]
G : Type u
inst✝¹ : Monoid G
inst✝ : Fintype G
⊢ Finset.lcm Finset.univ orderOf ∣ exponent G
[PROOFSTEP]
apply Finset.lcm_dvd
[GOAL]
case a
G : Type u
inst✝¹ : Monoid G
inst✝ : Fintype G
⊢ ∀ (b : G), b ∈ Finset.univ → orderOf b ∣ exponent G
[PROOFSTEP]
intro g _
[GOAL]
case a
G : Type u
inst✝¹ : Monoid G
inst✝ : Fintype G
g : G
a✝ : g ∈ Finset.univ
⊢ orderOf g ∣ exponent G
[PROOFSTEP]
exact order_dvd_exponent g
[GOAL]
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
⊢ ∃ g, orderOf g = p ^ ↑(Nat.factorization (exponent G)) p
[PROOFSTEP]
haveI := Fact.mk hp
[GOAL]
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
⊢ ∃ g, orderOf g = p ^ ↑(Nat.factorization (exponent G)) p
[PROOFSTEP]
rcases eq_or_ne ((exponent G).factorization p) 0 with (h | h)
[GOAL]
case inl
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : ↑(Nat.factorization (exponent G)) p = 0
⊢ ∃ g, orderOf g = p ^ ↑(Nat.factorization (exponent G)) p
[PROOFSTEP]
refine' ⟨1, by rw [h, pow_zero, orderOf_one]⟩
[GOAL]
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : ↑(Nat.factorization (exponent G)) p = 0
⊢ orderOf 1 = p ^ ↑(Nat.factorization (exponent G)) p
[PROOFSTEP]
rw [h, pow_zero, orderOf_one]
[GOAL]
case inr
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : ↑(Nat.factorization (exponent G)) p ≠ 0
⊢ ∃ g, orderOf g = p ^ ↑(Nat.factorization (exponent G)) p
[PROOFSTEP]
have he : 0 < exponent G :=
  Ne.bot_lt fun ht => by
    rw [ht] at h
    apply h
    rw [bot_eq_zero, Nat.factorization_zero, Finsupp.zero_apply]
[GOAL]
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : ↑(Nat.factorization (exponent G)) p ≠ 0
ht : exponent G = ⊥
⊢ False
[PROOFSTEP]
rw [ht] at h
[GOAL]
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : ↑(Nat.factorization ⊥) p ≠ 0
ht : exponent G = ⊥
⊢ False
[PROOFSTEP]
apply h
[GOAL]
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : ↑(Nat.factorization ⊥) p ≠ 0
ht : exponent G = ⊥
⊢ ↑(Nat.factorization ⊥) p = 0
[PROOFSTEP]
rw [bot_eq_zero, Nat.factorization_zero, Finsupp.zero_apply]
[GOAL]
case inr
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : ↑(Nat.factorization (exponent G)) p ≠ 0
he : 0 < exponent G
⊢ ∃ g, orderOf g = p ^ ↑(Nat.factorization (exponent G)) p
[PROOFSTEP]
rw [← Finsupp.mem_support_iff] at h
[GOAL]
case inr
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : p ∈ (Nat.factorization (exponent G)).support
he : 0 < exponent G
⊢ ∃ g, orderOf g = p ^ ↑(Nat.factorization (exponent G)) p
[PROOFSTEP]
obtain ⟨g, hg⟩ : ∃ g : G, g ^ (exponent G / p) ≠ 1 :=
  by
  suffices key : ¬exponent G ∣ exponent G / p
  · simpa using mt (exponent_dvd_of_forall_pow_eq_one G (exponent G / p)) key
  exact fun hd =>
    hp.one_lt.not_le
      ((mul_le_iff_le_one_left he).mp <| Nat.le_of_dvd he <| Nat.mul_dvd_of_dvd_div (Nat.dvd_of_mem_factorization h) hd)
[GOAL]
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : p ∈ (Nat.factorization (exponent G)).support
he : 0 < exponent G
⊢ ∃ g, g ^ (exponent G / p) ≠ 1
[PROOFSTEP]
suffices key : ¬exponent G ∣ exponent G / p
[GOAL]
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : p ∈ (Nat.factorization (exponent G)).support
he : 0 < exponent G
key : ¬exponent G ∣ exponent G / p
⊢ ∃ g, g ^ (exponent G / p) ≠ 1
[PROOFSTEP]
simpa using mt (exponent_dvd_of_forall_pow_eq_one G (exponent G / p)) key
[GOAL]
case key
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : p ∈ (Nat.factorization (exponent G)).support
he : 0 < exponent G
⊢ ¬exponent G ∣ exponent G / p
[PROOFSTEP]
exact fun hd =>
  hp.one_lt.not_le
    ((mul_le_iff_le_one_left he).mp <| Nat.le_of_dvd he <| Nat.mul_dvd_of_dvd_div (Nat.dvd_of_mem_factorization h) hd)
[GOAL]
case inr.intro
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : p ∈ (Nat.factorization (exponent G)).support
he : 0 < exponent G
g : G
hg : g ^ (exponent G / p) ≠ 1
⊢ ∃ g, orderOf g = p ^ ↑(Nat.factorization (exponent G)) p
[PROOFSTEP]
obtain ⟨k, hk : exponent G = p ^ _ * k⟩ := Nat.ord_proj_dvd _ _
[GOAL]
case inr.intro.intro
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : p ∈ (Nat.factorization (exponent G)).support
he : 0 < exponent G
g : G
hg : g ^ (exponent G / p) ≠ 1
k : ℕ
hk : exponent G = p ^ ↑(Nat.factorization (exponent G)) p * k
⊢ ∃ g, orderOf g = p ^ ↑(Nat.factorization (exponent G)) p
[PROOFSTEP]
obtain ⟨t, ht⟩ := Nat.exists_eq_succ_of_ne_zero (Finsupp.mem_support_iff.mp h)
[GOAL]
case inr.intro.intro.intro
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : p ∈ (Nat.factorization (exponent G)).support
he : 0 < exponent G
g : G
hg : g ^ (exponent G / p) ≠ 1
k : ℕ
hk : exponent G = p ^ ↑(Nat.factorization (exponent G)) p * k
t : ℕ
ht : ↑(Nat.factorization (exponent G)) p = Nat.succ t
⊢ ∃ g, orderOf g = p ^ ↑(Nat.factorization (exponent G)) p
[PROOFSTEP]
refine' ⟨g ^ k, _⟩
[GOAL]
case inr.intro.intro.intro
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : p ∈ (Nat.factorization (exponent G)).support
he : 0 < exponent G
g : G
hg : g ^ (exponent G / p) ≠ 1
k : ℕ
hk : exponent G = p ^ ↑(Nat.factorization (exponent G)) p * k
t : ℕ
ht : ↑(Nat.factorization (exponent G)) p = Nat.succ t
⊢ orderOf (g ^ k) = p ^ ↑(Nat.factorization (exponent G)) p
[PROOFSTEP]
rw [ht]
[GOAL]
case inr.intro.intro.intro
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : p ∈ (Nat.factorization (exponent G)).support
he : 0 < exponent G
g : G
hg : g ^ (exponent G / p) ≠ 1
k : ℕ
hk : exponent G = p ^ ↑(Nat.factorization (exponent G)) p * k
t : ℕ
ht : ↑(Nat.factorization (exponent G)) p = Nat.succ t
⊢ orderOf (g ^ k) = p ^ Nat.succ t
[PROOFSTEP]
apply orderOf_eq_prime_pow
[GOAL]
case inr.intro.intro.intro.hnot
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : p ∈ (Nat.factorization (exponent G)).support
he : 0 < exponent G
g : G
hg : g ^ (exponent G / p) ≠ 1
k : ℕ
hk : exponent G = p ^ ↑(Nat.factorization (exponent G)) p * k
t : ℕ
ht : ↑(Nat.factorization (exponent G)) p = Nat.succ t
⊢ ¬(g ^ k) ^ p ^ t = 1
[PROOFSTEP]
rwa [hk, mul_comm, ht, pow_succ', ← mul_assoc, Nat.mul_div_cancel _ hp.pos, pow_mul] at hg
[GOAL]
case inr.intro.intro.intro.hfin
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : p ∈ (Nat.factorization (exponent G)).support
he : 0 < exponent G
g : G
hg : g ^ (exponent G / p) ≠ 1
k : ℕ
hk : exponent G = p ^ ↑(Nat.factorization (exponent G)) p * k
t : ℕ
ht : ↑(Nat.factorization (exponent G)) p = Nat.succ t
⊢ (g ^ k) ^ p ^ (t + 1) = 1
[PROOFSTEP]
rw [← Nat.succ_eq_add_one, ← ht, ← pow_mul, mul_comm, ← hk]
[GOAL]
case inr.intro.intro.intro.hfin
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : p ∈ (Nat.factorization (exponent G)).support
he : 0 < exponent G
g : G
hg : g ^ (exponent G / p) ≠ 1
k : ℕ
hk : exponent G = p ^ ↑(Nat.factorization (exponent G)) p * k
t : ℕ
ht : ↑(Nat.factorization (exponent G)) p = Nat.succ t
⊢ g ^ exponent G = 1
[PROOFSTEP]
exact pow_exponent_eq_one g
[GOAL]
G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
⊢ exponent G ≠ 0 ↔ Set.Finite (Set.range orderOf)
[PROOFSTEP]
refine' ⟨fun he => _, fun he => _⟩
[GOAL]
case refine'_1
G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
he : exponent G ≠ 0
⊢ Set.Finite (Set.range orderOf)
[PROOFSTEP]
by_contra h
[GOAL]
case refine'_1
G : Type u
inst✝ : Monoid G
h✝ : ∀ (g : G), 0 < orderOf g
he : exponent G ≠ 0
h : ¬Set.Finite (Set.range orderOf)
⊢ False
[PROOFSTEP]
obtain ⟨m, ⟨t, rfl⟩, het⟩ := Set.Infinite.exists_gt h (exponent G)
[GOAL]
case refine'_1.intro.intro.intro
G : Type u
inst✝ : Monoid G
h✝ : ∀ (g : G), 0 < orderOf g
he : exponent G ≠ 0
h : ¬Set.Finite (Set.range orderOf)
t : G
het : exponent G < orderOf t
⊢ False
[PROOFSTEP]
exact pow_ne_one_of_lt_orderOf' he het (pow_exponent_eq_one t)
[GOAL]
case refine'_2
G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
he : Set.Finite (Set.range orderOf)
⊢ exponent G ≠ 0
[PROOFSTEP]
lift Set.range (orderOf (G := G)) to Finset ℕ using he with t ht
[GOAL]
case refine'_2.intro
G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
t : Finset ℕ
ht : ↑t = Set.range orderOf
exponent_ne_zero_iff_range_orderOf_finite✝ exponent_ne_zero_iff_range_orderOf_finite :
  (∀ (g : G), 0 < orderOf g) → (exponent G ≠ 0 ↔ Set.Finite ↑t)
⊢ exponent G ≠ 0
[PROOFSTEP]
have htpos : 0 < t.prod id := by
  refine' Finset.prod_pos fun a ha => _
  rw [← Finset.mem_coe, ht] at ha
  obtain ⟨k, rfl⟩ := ha
  exact h k
[GOAL]
G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
t : Finset ℕ
ht : ↑t = Set.range orderOf
exponent_ne_zero_iff_range_orderOf_finite✝ exponent_ne_zero_iff_range_orderOf_finite :
  (∀ (g : G), 0 < orderOf g) → (exponent G ≠ 0 ↔ Set.Finite ↑t)
⊢ 0 < Finset.prod t id
[PROOFSTEP]
refine' Finset.prod_pos fun a ha => _
[GOAL]
G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
t : Finset ℕ
ht : ↑t = Set.range orderOf
exponent_ne_zero_iff_range_orderOf_finite✝ exponent_ne_zero_iff_range_orderOf_finite :
  (∀ (g : G), 0 < orderOf g) → (exponent G ≠ 0 ↔ Set.Finite ↑t)
a : ℕ
ha : a ∈ t
⊢ 0 < id a
[PROOFSTEP]
rw [← Finset.mem_coe, ht] at ha
[GOAL]
G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
t : Finset ℕ
ht : ↑t = Set.range orderOf
exponent_ne_zero_iff_range_orderOf_finite✝ exponent_ne_zero_iff_range_orderOf_finite :
  (∀ (g : G), 0 < orderOf g) → (exponent G ≠ 0 ↔ Set.Finite ↑t)
a : ℕ
ha : a ∈ Set.range orderOf
⊢ 0 < id a
[PROOFSTEP]
obtain ⟨k, rfl⟩ := ha
[GOAL]
case intro
G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
t : Finset ℕ
ht : ↑t = Set.range orderOf
exponent_ne_zero_iff_range_orderOf_finite✝ exponent_ne_zero_iff_range_orderOf_finite :
  (∀ (g : G), 0 < orderOf g) → (exponent G ≠ 0 ↔ Set.Finite ↑t)
k : G
⊢ 0 < id (orderOf k)
[PROOFSTEP]
exact h k
[GOAL]
case refine'_2.intro
G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
t : Finset ℕ
ht : ↑t = Set.range orderOf
exponent_ne_zero_iff_range_orderOf_finite✝ exponent_ne_zero_iff_range_orderOf_finite :
  (∀ (g : G), 0 < orderOf g) → (exponent G ≠ 0 ↔ Set.Finite ↑t)
htpos : 0 < Finset.prod t id
⊢ exponent G ≠ 0
[PROOFSTEP]
suffices exponent G ∣ t.prod id by
  intro h
  rw [h, zero_dvd_iff] at this
  exact htpos.ne' this
[GOAL]
G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
t : Finset ℕ
ht : ↑t = Set.range orderOf
exponent_ne_zero_iff_range_orderOf_finite✝ exponent_ne_zero_iff_range_orderOf_finite :
  (∀ (g : G), 0 < orderOf g) → (exponent G ≠ 0 ↔ Set.Finite ↑t)
htpos : 0 < Finset.prod t id
this : exponent G ∣ Finset.prod t id
⊢ exponent G ≠ 0
[PROOFSTEP]
intro h
[GOAL]
G : Type u
inst✝ : Monoid G
h✝ : ∀ (g : G), 0 < orderOf g
t : Finset ℕ
ht : ↑t = Set.range orderOf
exponent_ne_zero_iff_range_orderOf_finite✝ exponent_ne_zero_iff_range_orderOf_finite :
  (∀ (g : G), 0 < orderOf g) → (exponent G ≠ 0 ↔ Set.Finite ↑t)
htpos : 0 < Finset.prod t id
this : exponent G ∣ Finset.prod t id
h : exponent G = 0
⊢ False
[PROOFSTEP]
rw [h, zero_dvd_iff] at this
[GOAL]
G : Type u
inst✝ : Monoid G
h✝ : ∀ (g : G), 0 < orderOf g
t : Finset ℕ
ht : ↑t = Set.range orderOf
exponent_ne_zero_iff_range_orderOf_finite✝ exponent_ne_zero_iff_range_orderOf_finite :
  (∀ (g : G), 0 < orderOf g) → (exponent G ≠ 0 ↔ Set.Finite ↑t)
htpos : 0 < Finset.prod t id
this : Finset.prod t id = 0
h : exponent G = 0
⊢ False
[PROOFSTEP]
exact htpos.ne' this
[GOAL]
case refine'_2.intro
G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
t : Finset ℕ
ht : ↑t = Set.range orderOf
exponent_ne_zero_iff_range_orderOf_finite✝ exponent_ne_zero_iff_range_orderOf_finite :
  (∀ (g : G), 0 < orderOf g) → (exponent G ≠ 0 ↔ Set.Finite ↑t)
htpos : 0 < Finset.prod t id
⊢ exponent G ∣ Finset.prod t id
[PROOFSTEP]
refine' exponent_dvd_of_forall_pow_eq_one _ _ fun g => _
[GOAL]
case refine'_2.intro
G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
t : Finset ℕ
ht : ↑t = Set.range orderOf
exponent_ne_zero_iff_range_orderOf_finite✝ exponent_ne_zero_iff_range_orderOf_finite :
  (∀ (g : G), 0 < orderOf g) → (exponent G ≠ 0 ↔ Set.Finite ↑t)
htpos : 0 < Finset.prod t id
g : G
⊢ g ^ Finset.prod t id = 1
[PROOFSTEP]
rw [pow_eq_mod_orderOf, Nat.mod_eq_zero_of_dvd, pow_zero g]
[GOAL]
case refine'_2.intro
G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
t : Finset ℕ
ht : ↑t = Set.range orderOf
exponent_ne_zero_iff_range_orderOf_finite✝ exponent_ne_zero_iff_range_orderOf_finite :
  (∀ (g : G), 0 < orderOf g) → (exponent G ≠ 0 ↔ Set.Finite ↑t)
htpos : 0 < Finset.prod t id
g : G
⊢ orderOf g ∣ Finset.prod t id
[PROOFSTEP]
apply Finset.dvd_prod_of_mem
[GOAL]
case refine'_2.intro.ha
G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
t : Finset ℕ
ht : ↑t = Set.range orderOf
exponent_ne_zero_iff_range_orderOf_finite✝ exponent_ne_zero_iff_range_orderOf_finite :
  (∀ (g : G), 0 < orderOf g) → (exponent G ≠ 0 ↔ Set.Finite ↑t)
htpos : 0 < Finset.prod t id
g : G
⊢ Function.minimalPeriod (fun x => g * x) 1 ∈ t
[PROOFSTEP]
rw [← Finset.mem_coe, ht]
[GOAL]
case refine'_2.intro.ha
G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
t : Finset ℕ
ht : ↑t = Set.range orderOf
exponent_ne_zero_iff_range_orderOf_finite✝ exponent_ne_zero_iff_range_orderOf_finite :
  (∀ (g : G), 0 < orderOf g) → (exponent G ≠ 0 ↔ Set.Finite ↑t)
htpos : 0 < Finset.prod t id
g : G
⊢ Function.minimalPeriod (fun x => g * x) 1 ∈ Set.range orderOf
[PROOFSTEP]
exact Set.mem_range_self g
[GOAL]
G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
⊢ exponent G = 0 ↔ Set.Infinite (Set.range orderOf)
[PROOFSTEP]
have := exponent_ne_zero_iff_range_orderOf_finite h
[GOAL]
G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
this : exponent G ≠ 0 ↔ Set.Finite (Set.range orderOf)
⊢ exponent G = 0 ↔ Set.Infinite (Set.range orderOf)
[PROOFSTEP]
rwa [Ne.def, not_iff_comm, Iff.comm] at this
[GOAL]
G : Type u
inst✝¹ : Monoid G
inst✝ : Fintype G
⊢ Finset.lcm Finset.univ orderOf = exponent G
[PROOFSTEP]
apply Nat.dvd_antisymm (lcm_orderOf_dvd_exponent G)
[GOAL]
G : Type u
inst✝¹ : Monoid G
inst✝ : Fintype G
⊢ exponent G ∣ Finset.lcm Finset.univ orderOf
[PROOFSTEP]
refine' exponent_dvd_of_forall_pow_eq_one G _ fun g => _
[GOAL]
G : Type u
inst✝¹ : Monoid G
inst✝ : Fintype G
g : G
⊢ g ^ Finset.lcm Finset.univ orderOf = 1
[PROOFSTEP]
obtain ⟨m, hm⟩ : orderOf g ∣ Finset.univ.lcm orderOf := Finset.dvd_lcm (Finset.mem_univ g)
[GOAL]
case intro
G : Type u
inst✝¹ : Monoid G
inst✝ : Fintype G
g : G
m : ℕ
hm : Finset.lcm Finset.univ orderOf = orderOf g * m
⊢ g ^ Finset.lcm Finset.univ orderOf = 1
[PROOFSTEP]
rw [hm, pow_mul, pow_orderOf_eq_one, one_pow]
[GOAL]
G : Type u
inst✝¹ : LeftCancelMonoid G
inst✝ : Finite G
⊢ exponent G ≠ 0
[PROOFSTEP]
cases nonempty_fintype G
[GOAL]
case intro
G : Type u
inst✝¹ : LeftCancelMonoid G
inst✝ : Finite G
val✝ : Fintype G
⊢ exponent G ≠ 0
[PROOFSTEP]
simpa [← lcm_order_eq_exponent, Finset.lcm_eq_zero_iff] using fun x => (orderOf_pos x).ne'
[GOAL]
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
⊢ exponent G = ⨆ (g : G), orderOf g
[PROOFSTEP]
rw [iSup]
[GOAL]
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
⊢ exponent G = sSup (Set.range fun g => orderOf g)
[PROOFSTEP]
rcases eq_or_ne (exponent G) 0 with (he | he)
[GOAL]
case inl
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)
[PROOFSTEP]
rw [he, Set.Infinite.Nat.sSup_eq_zero <| (exponent_eq_zero_iff_range_orderOf_infinite h).1 he]
[GOAL]
case inr
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)
[PROOFSTEP]
have hne : (Set.range (orderOf : G → ℕ)).Nonempty := ⟨1, 1, orderOf_one⟩
[GOAL]
case inr
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : exponent G ≠ 0
hne : Set.Nonempty (Set.range orderOf)
⊢ exponent G = sSup (Set.range fun g => orderOf g)
[PROOFSTEP]
have hfin : (Set.range (orderOf : G → ℕ)).Finite := by rwa [← exponent_ne_zero_iff_range_orderOf_finite h]
[GOAL]
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : exponent G ≠ 0
hne : Set.Nonempty (Set.range orderOf)
⊢ Set.Finite (Set.range orderOf)
[PROOFSTEP]
rwa [← exponent_ne_zero_iff_range_orderOf_finite h]
[GOAL]
case inr
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : exponent G ≠ 0
hne : Set.Nonempty (Set.range orderOf)
hfin : Set.Finite (Set.range orderOf)
⊢ exponent G = sSup (Set.range fun g => orderOf g)
[PROOFSTEP]
obtain ⟨t, ht⟩ := hne.cSup_mem hfin
[GOAL]
case inr.intro
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : exponent G ≠ 0
hne : Set.Nonempty (Set.range orderOf)
hfin : Set.Finite (Set.range orderOf)
t : G
ht : orderOf t = sSup (Set.range orderOf)
⊢ exponent G = sSup (Set.range fun g => orderOf g)
[PROOFSTEP]
apply Nat.dvd_antisymm _
[GOAL]
case inr.intro
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : exponent G ≠ 0
hne : Set.Nonempty (Set.range orderOf)
hfin : Set.Finite (Set.range orderOf)
t : G
ht : orderOf t = sSup (Set.range orderOf)
⊢ sSup (Set.range fun g => orderOf g) ∣ exponent G
[PROOFSTEP]
rw [← ht]
[GOAL]
case inr.intro
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : exponent G ≠ 0
hne : Set.Nonempty (Set.range orderOf)
hfin : Set.Finite (Set.range orderOf)
t : G
ht : orderOf t = sSup (Set.range orderOf)
⊢ orderOf t ∣ exponent G
[PROOFSTEP]
apply order_dvd_exponent
[GOAL]
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : exponent G ≠ 0
hne : Set.Nonempty (Set.range orderOf)
hfin : Set.Finite (Set.range orderOf)
t : G
ht : orderOf t = sSup (Set.range orderOf)
⊢ exponent G ∣ sSup (Set.range fun g => orderOf g)
[PROOFSTEP]
refine' Nat.dvd_of_factors_subperm he _
[GOAL]
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : exponent G ≠ 0
hne : Set.Nonempty (Set.range orderOf)
hfin : Set.Finite (Set.range orderOf)
t : G
ht : orderOf t = sSup (Set.range orderOf)
⊢ Nat.factors (exponent G) <+~ Nat.factors (sSup (Set.range fun g => orderOf g))
[PROOFSTEP]
rw [List.subperm_ext_iff]
[GOAL]
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : exponent G ≠ 0
hne : Set.Nonempty (Set.range orderOf)
hfin : Set.Finite (Set.range orderOf)
t : G
ht : orderOf t = sSup (Set.range orderOf)
⊢ ∀ (x : ℕ),
    x ∈ Nat.factors (exponent G) →
      List.count x (Nat.factors (exponent G)) ≤ List.count x (Nat.factors (sSup (Set.range fun g => orderOf g)))
[PROOFSTEP]
by_contra' h
[GOAL]
G : Type u
inst✝ : CommMonoid G
h✝ : ∀ (g : G), 0 < orderOf g
he : exponent G ≠ 0
hne : Set.Nonempty (Set.range orderOf)
hfin : Set.Finite (Set.range orderOf)
t : G
ht : orderOf t = sSup (Set.range orderOf)
h :
  ∃ x,
    x ∈ Nat.factors (exponent G) ∧
      List.count x (Nat.factors (sSup (Set.range fun g => orderOf g))) < List.count x (Nat.factors (exponent G))
⊢ False
[PROOFSTEP]
obtain ⟨p, hp, hpe⟩ := h
[GOAL]
case intro.intro
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : exponent G ≠ 0
hne : Set.Nonempty (Set.range orderOf)
hfin : Set.Finite (Set.range orderOf)
t : G
ht : orderOf t = sSup (Set.range orderOf)
p : ℕ
hp : p ∈ Nat.factors (exponent G)
hpe : List.count p (Nat.factors (sSup (Set.range fun g => orderOf g))) < List.count p (Nat.factors (exponent G))
⊢ False
[PROOFSTEP]
replace hp := Nat.prime_of_mem_factors hp
[GOAL]
case intro.intro
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : exponent G ≠ 0
hne : Set.Nonempty (Set.range orderOf)
hfin : Set.Finite (Set.range orderOf)
t : G
ht : orderOf t = sSup (Set.range orderOf)
p : ℕ
hpe : List.count p (Nat.factors (sSup (Set.range fun g => orderOf g))) < List.count p (Nat.factors (exponent G))
hp : Nat.Prime p
⊢ False
[PROOFSTEP]
simp only [Nat.factors_count_eq] at hpe
[GOAL]
case intro.intro
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : exponent G ≠ 0
hne : Set.Nonempty (Set.range orderOf)
hfin : Set.Finite (Set.range orderOf)
t : G
ht : orderOf t = sSup (Set.range orderOf)
p : ℕ
hp : Nat.Prime p
hpe : ↑(Nat.factorization (sSup (Set.range fun g => orderOf g))) p < ↑(Nat.factorization (exponent G)) p
⊢ False
[PROOFSTEP]
set k := (orderOf t).factorization p with hk
[GOAL]
case intro.intro
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : exponent G ≠ 0
hne : Set.Nonempty (Set.range orderOf)
hfin : Set.Finite (Set.range orderOf)
t : G
ht : orderOf t = sSup (Set.range orderOf)
p : ℕ
hp : Nat.Prime p
hpe : ↑(Nat.factorization (sSup (Set.range fun g => orderOf g))) p < ↑(Nat.factorization (exponent G)) p
k : ℕ := ↑(Nat.factorization (orderOf t)) p
hk : k = ↑(Nat.factorization (orderOf t)) p
⊢ False
[PROOFSTEP]
obtain ⟨g, hg⟩ := hp.exists_orderOf_eq_pow_factorization_exponent G
[GOAL]
case intro.intro.intro
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : exponent G ≠ 0
hne : Set.Nonempty (Set.range orderOf)
hfin : Set.Finite (Set.range orderOf)
t : G
ht : orderOf t = sSup (Set.range orderOf)
p : ℕ
hp : Nat.Prime p
hpe : ↑(Nat.factorization (sSup (Set.range fun g => orderOf g))) p < ↑(Nat.factorization (exponent G)) p
k : ℕ := ↑(Nat.factorization (orderOf t)) p
hk : k = ↑(Nat.factorization (orderOf t)) p
g : G
hg : orderOf g = p ^ ↑(Nat.factorization (exponent G)) p
⊢ False
[PROOFSTEP]
suffices orderOf t < orderOf (t ^ p ^ k * g) by
  rw [ht] at this
  exact this.not_le (le_csSup hfin.bddAbove <| Set.mem_range_self _)
[GOAL]
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : exponent G ≠ 0
hne : Set.Nonempty (Set.range orderOf)
hfin : Set.Finite (Set.range orderOf)
t : G
ht : orderOf t = sSup (Set.range orderOf)
p : ℕ
hp : Nat.Prime p
hpe : ↑(Nat.factorization (sSup (Set.range fun g => orderOf g))) p < ↑(Nat.factorization (exponent G)) p
k : ℕ := ↑(Nat.factorization (orderOf t)) p
hk : k = ↑(Nat.factorization (orderOf t)) p
g : G
hg : orderOf g = p ^ ↑(Nat.factorization (exponent G)) p
this : orderOf t < orderOf (t ^ p ^ k * g)
⊢ False
[PROOFSTEP]
rw [ht] at this
[GOAL]
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : exponent G ≠ 0
hne : Set.Nonempty (Set.range orderOf)
hfin : Set.Finite (Set.range orderOf)
t : G
ht : orderOf t = sSup (Set.range orderOf)
p : ℕ
hp : Nat.Prime p
hpe : ↑(Nat.factorization (sSup (Set.range fun g => orderOf g))) p < ↑(Nat.factorization (exponent G)) p
k : ℕ := ↑(Nat.factorization (orderOf t)) p
hk : k = ↑(Nat.factorization (orderOf t)) p
g : G
hg : orderOf g = p ^ ↑(Nat.factorization (exponent G)) p
this : sSup (Set.range orderOf) < orderOf (t ^ p ^ k * g)
⊢ False
[PROOFSTEP]
exact this.not_le (le_csSup hfin.bddAbove <| Set.mem_range_self _)
[GOAL]
case intro.intro.intro
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : exponent G ≠ 0
hne : Set.Nonempty (Set.range orderOf)
hfin : Set.Finite (Set.range orderOf)
t : G
ht : orderOf t = sSup (Set.range orderOf)
p : ℕ
hp : Nat.Prime p
hpe : ↑(Nat.factorization (sSup (Set.range fun g => orderOf g))) p < ↑(Nat.factorization (exponent G)) p
k : ℕ := ↑(Nat.factorization (orderOf t)) p
hk : k = ↑(Nat.factorization (orderOf t)) p
g : G
hg : orderOf g = p ^ ↑(Nat.factorization (exponent G)) p
⊢ orderOf t < orderOf (t ^ p ^ k * g)
[PROOFSTEP]
have hpk : p ^ k ∣ orderOf t := Nat.ord_proj_dvd _ _
[GOAL]
case intro.intro.intro
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : exponent G ≠ 0
hne : Set.Nonempty (Set.range orderOf)
hfin : Set.Finite (Set.range orderOf)
t : G
ht : orderOf t = sSup (Set.range orderOf)
p : ℕ
hp : Nat.Prime p
hpe : ↑(Nat.factorization (sSup (Set.range fun g => orderOf g))) p < ↑(Nat.factorization (exponent G)) p
k : ℕ := ↑(Nat.factorization (orderOf t)) p
hk : k = ↑(Nat.factorization (orderOf t)) p
g : G
hg : orderOf g = p ^ ↑(Nat.factorization (exponent G)) p
hpk : p ^ k ∣ orderOf t
⊢ orderOf t < orderOf (t ^ p ^ k * g)
[PROOFSTEP]
have hpk' : orderOf (t ^ p ^ k) = orderOf t / p ^ k := by
  rw [orderOf_pow' t (pow_ne_zero k hp.ne_zero), Nat.gcd_eq_right hpk]
[GOAL]
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : exponent G ≠ 0
hne : Set.Nonempty (Set.range orderOf)
hfin : Set.Finite (Set.range orderOf)
t : G
ht : orderOf t = sSup (Set.range orderOf)
p : ℕ
hp : Nat.Prime p
hpe : ↑(Nat.factorization (sSup (Set.range fun g => orderOf g))) p < ↑(Nat.factorization (exponent G)) p
k : ℕ := ↑(Nat.factorization (orderOf t)) p
hk : k = ↑(Nat.factorization (orderOf t)) p
g : G
hg : orderOf g = p ^ ↑(Nat.factorization (exponent G)) p
hpk : p ^ k ∣ orderOf t
⊢ orderOf (t ^ p ^ k) = orderOf t / p ^ k
[PROOFSTEP]
rw [orderOf_pow' t (pow_ne_zero k hp.ne_zero), Nat.gcd_eq_right hpk]
[GOAL]
case intro.intro.intro
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : exponent G ≠ 0
hne : Set.Nonempty (Set.range orderOf)
hfin : Set.Finite (Set.range orderOf)
t : G
ht : orderOf t = sSup (Set.range orderOf)
p : ℕ
hp : Nat.Prime p
hpe : ↑(Nat.factorization (sSup (Set.range fun g => orderOf g))) p < ↑(Nat.factorization (exponent G)) p
k : ℕ := ↑(Nat.factorization (orderOf t)) p
hk : k = ↑(Nat.factorization (orderOf t)) p
g : G
hg : orderOf g = p ^ ↑(Nat.factorization (exponent G)) p
hpk : p ^ k ∣ orderOf t
hpk' : orderOf (t ^ p ^ k) = orderOf t / p ^ k
⊢ orderOf t < orderOf (t ^ p ^ k * g)
[PROOFSTEP]
obtain ⟨a, ha⟩ := Nat.exists_eq_add_of_lt hpe
[GOAL]
case intro.intro.intro.intro
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : exponent G ≠ 0
hne : Set.Nonempty (Set.range orderOf)
hfin : Set.Finite (Set.range orderOf)
t : G
ht : orderOf t = sSup (Set.range orderOf)
p : ℕ
hp : Nat.Prime p
hpe : ↑(Nat.factorization (sSup (Set.range fun g => orderOf g))) p < ↑(Nat.factorization (exponent G)) p
k : ℕ := ↑(Nat.factorization (orderOf t)) p
hk : k = ↑(Nat.factorization (orderOf t)) p
g : G
hg : orderOf g = p ^ ↑(Nat.factorization (exponent G)) p
hpk : p ^ k ∣ orderOf t
hpk' : orderOf (t ^ p ^ k) = orderOf t / p ^ k
a : ℕ
ha : ↑(Nat.factorization (exponent G)) p = ↑(Nat.factorization (sSup (Set.range fun g => orderOf g))) p + a + 1
⊢ orderOf t < orderOf (t ^ p ^ k * g)
[PROOFSTEP]
have hcoprime : (orderOf (t ^ p ^ k)).coprime (orderOf g) :=
  by
  rw [hg, Nat.coprime_pow_right_iff (pos_of_gt hpe), Nat.coprime_comm]
  apply Or.resolve_right (Nat.coprime_or_dvd_of_prime hp _)
  nth_rw 1 [← pow_one p]
  have : 1 = (Nat.factorization (orderOf (t ^ p ^ k))) p + 1 :=
    by
    rw [hpk', Nat.factorization_div hpk]
    simp [hp]
  rw [this]
    -- Porting note: convert made to_additive complain
  apply Nat.pow_succ_factorization_not_dvd (h <| t ^ p ^ k).ne' hp
[GOAL]
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : exponent G ≠ 0
hne : Set.Nonempty (Set.range orderOf)
hfin : Set.Finite (Set.range orderOf)
t : G
ht : orderOf t = sSup (Set.range orderOf)
p : ℕ
hp : Nat.Prime p
hpe : ↑(Nat.factorization (sSup (Set.range fun g => orderOf g))) p < ↑(Nat.factorization (exponent G)) p
k : ℕ := ↑(Nat.factorization (orderOf t)) p
hk : k = ↑(Nat.factorization (orderOf t)) p
g : G
hg : orderOf g = p ^ ↑(Nat.factorization (exponent G)) p
hpk : p ^ k ∣ orderOf t
hpk' : orderOf (t ^ p ^ k) = orderOf t / p ^ k
a : ℕ
ha : ↑(Nat.factorization (exponent G)) p = ↑(Nat.factorization (sSup (Set.range fun g => orderOf g))) p + a + 1
⊢ Nat.coprime (orderOf (t ^ p ^ k)) (orderOf g)
[PROOFSTEP]
rw [hg, Nat.coprime_pow_right_iff (pos_of_gt hpe), Nat.coprime_comm]
[GOAL]
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : exponent G ≠ 0
hne : Set.Nonempty (Set.range orderOf)
hfin : Set.Finite (Set.range orderOf)
t : G
ht : orderOf t = sSup (Set.range orderOf)
p : ℕ
hp : Nat.Prime p
hpe : ↑(Nat.factorization (sSup (Set.range fun g => orderOf g))) p < ↑(Nat.factorization (exponent G)) p
k : ℕ := ↑(Nat.factorization (orderOf t)) p
hk : k = ↑(Nat.factorization (orderOf t)) p
g : G
hg : orderOf g = p ^ ↑(Nat.factorization (exponent G)) p
hpk : p ^ k ∣ orderOf t
hpk' : orderOf (t ^ p ^ k) = orderOf t / p ^ k
a : ℕ
ha : ↑(Nat.factorization (exponent G)) p = ↑(Nat.factorization (sSup (Set.range fun g => orderOf g))) p + a + 1
⊢ Nat.coprime p (orderOf (t ^ p ^ k))
[PROOFSTEP]
apply Or.resolve_right (Nat.coprime_or_dvd_of_prime hp _)
[GOAL]
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : exponent G ≠ 0
hne : Set.Nonempty (Set.range orderOf)
hfin : Set.Finite (Set.range orderOf)
t : G
ht : orderOf t = sSup (Set.range orderOf)
p : ℕ
hp : Nat.Prime p
hpe : ↑(Nat.factorization (sSup (Set.range fun g => orderOf g))) p < ↑(Nat.factorization (exponent G)) p
k : ℕ := ↑(Nat.factorization (orderOf t)) p
hk : k = ↑(Nat.factorization (orderOf t)) p
g : G
hg : orderOf g = p ^ ↑(Nat.factorization (exponent G)) p
hpk : p ^ k ∣ orderOf t
hpk' : orderOf (t ^ p ^ k) = orderOf t / p ^ k
a : ℕ
ha : ↑(Nat.factorization (exponent G)) p = ↑(Nat.factorization (sSup (Set.range fun g => orderOf g))) p + a + 1
⊢ ¬p ∣ orderOf (t ^ p ^ k)
[PROOFSTEP]
nth_rw 1 [← pow_one p]
[GOAL]
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : exponent G ≠ 0
hne : Set.Nonempty (Set.range orderOf)
hfin : Set.Finite (Set.range orderOf)
t : G
ht : orderOf t = sSup (Set.range orderOf)
p : ℕ
hp : Nat.Prime p
hpe : ↑(Nat.factorization (sSup (Set.range fun g => orderOf g))) p < ↑(Nat.factorization (exponent G)) p
k : ℕ := ↑(Nat.factorization (orderOf t)) p
hk : k = ↑(Nat.factorization (orderOf t)) p
g : G
hg : orderOf g = p ^ ↑(Nat.factorization (exponent G)) p
hpk : p ^ k ∣ orderOf t
hpk' : orderOf (t ^ p ^ k) = orderOf t / p ^ k
a : ℕ
ha : ↑(Nat.factorization (exponent G)) p = ↑(Nat.factorization (sSup (Set.range fun g => orderOf g))) p + a + 1
⊢ ¬p ^ 1 ∣ orderOf (t ^ p ^ k)
[PROOFSTEP]
have : 1 = (Nat.factorization (orderOf (t ^ p ^ k))) p + 1 :=
  by
  rw [hpk', Nat.factorization_div hpk]
  simp [hp]
[GOAL]
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : exponent G ≠ 0
hne : Set.Nonempty (Set.range orderOf)
hfin : Set.Finite (Set.range orderOf)
t : G
ht : orderOf t = sSup (Set.range orderOf)
p : ℕ
hp : Nat.Prime p
hpe : ↑(Nat.factorization (sSup (Set.range fun g => orderOf g))) p < ↑(Nat.factorization (exponent G)) p
k : ℕ := ↑(Nat.factorization (orderOf t)) p
hk : k = ↑(Nat.factorization (orderOf t)) p
g : G
hg : orderOf g = p ^ ↑(Nat.factorization (exponent G)) p
hpk : p ^ k ∣ orderOf t
hpk' : orderOf (t ^ p ^ k) = orderOf t / p ^ k
a : ℕ
ha : ↑(Nat.factorization (exponent G)) p = ↑(Nat.factorization (sSup (Set.range fun g => orderOf g))) p + a + 1
⊢ 1 = ↑(Nat.factorization (orderOf (t ^ p ^ k))) p + 1
[PROOFSTEP]
rw [hpk', Nat.factorization_div hpk]
[GOAL]
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : exponent G ≠ 0
hne : Set.Nonempty (Set.range orderOf)
hfin : Set.Finite (Set.range orderOf)
t : G
ht : orderOf t = sSup (Set.range orderOf)
p : ℕ
hp : Nat.Prime p
hpe : ↑(Nat.factorization (sSup (Set.range fun g => orderOf g))) p < ↑(Nat.factorization (exponent G)) p
k : ℕ := ↑(Nat.factorization (orderOf t)) p
hk : k = ↑(Nat.factorization (orderOf t)) p
g : G
hg : orderOf g = p ^ ↑(Nat.factorization (exponent G)) p
hpk : p ^ k ∣ orderOf t
hpk' : orderOf (t ^ p ^ k) = orderOf t / p ^ k
a : ℕ
ha : ↑(Nat.factorization (exponent G)) p = ↑(Nat.factorization (sSup (Set.range fun g => orderOf g))) p + a + 1
⊢ 1 = ↑(Nat.factorization (orderOf t) - Nat.factorization (p ^ k)) p + 1
[PROOFSTEP]
simp [hp]
[GOAL]
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : exponent G ≠ 0
hne : Set.Nonempty (Set.range orderOf)
hfin : Set.Finite (Set.range orderOf)
t : G
ht : orderOf t = sSup (Set.range orderOf)
p : ℕ
hp : Nat.Prime p
hpe : ↑(Nat.factorization (sSup (Set.range fun g => orderOf g))) p < ↑(Nat.factorization (exponent G)) p
k : ℕ := ↑(Nat.factorization (orderOf t)) p
hk : k = ↑(Nat.factorization (orderOf t)) p
g : G
hg : orderOf g = p ^ ↑(Nat.factorization (exponent G)) p
hpk : p ^ k ∣ orderOf t
hpk' : orderOf (t ^ p ^ k) = orderOf t / p ^ k
a : ℕ
ha : ↑(Nat.factorization (exponent G)) p = ↑(Nat.factorization (sSup (Set.range fun g => orderOf g))) p + a + 1
this : 1 = ↑(Nat.factorization (orderOf (t ^ p ^ k))) p + 1
⊢ ¬p ^ 1 ∣ orderOf (t ^ p ^ k)
[PROOFSTEP]
rw [this]
  -- Porting note: convert made to_additive complain
[GOAL]
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : exponent G ≠ 0
hne : Set.Nonempty (Set.range orderOf)
hfin : Set.Finite (Set.range orderOf)
t : G
ht : orderOf t = sSup (Set.range orderOf)
p : ℕ
hp : Nat.Prime p
hpe : ↑(Nat.factorization (sSup (Set.range fun g => orderOf g))) p < ↑(Nat.factorization (exponent G)) p
k : ℕ := ↑(Nat.factorization (orderOf t)) p
hk : k = ↑(Nat.factorization (orderOf t)) p
g : G
hg : orderOf g = p ^ ↑(Nat.factorization (exponent G)) p
hpk : p ^ k ∣ orderOf t
hpk' : orderOf (t ^ p ^ k) = orderOf t / p ^ k
a : ℕ
ha : ↑(Nat.factorization (exponent G)) p = ↑(Nat.factorization (sSup (Set.range fun g => orderOf g))) p + a + 1
this : 1 = ↑(Nat.factorization (orderOf (t ^ p ^ k))) p + 1
⊢ ¬p ^ (↑(Nat.factorization (orderOf (t ^ p ^ k))) p + 1) ∣ orderOf (t ^ p ^ k)
[PROOFSTEP]
apply Nat.pow_succ_factorization_not_dvd (h <| t ^ p ^ k).ne' hp
[GOAL]
case intro.intro.intro.intro
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : exponent G ≠ 0
hne : Set.Nonempty (Set.range orderOf)
hfin : Set.Finite (Set.range orderOf)
t : G
ht : orderOf t = sSup (Set.range orderOf)
p : ℕ
hp : Nat.Prime p
hpe : ↑(Nat.factorization (sSup (Set.range fun g => orderOf g))) p < ↑(Nat.factorization (exponent G)) p
k : ℕ := ↑(Nat.factorization (orderOf t)) p
hk : k = ↑(Nat.factorization (orderOf t)) p
g : G
hg : orderOf g = p ^ ↑(Nat.factorization (exponent G)) p
hpk : p ^ k ∣ orderOf t
hpk' : orderOf (t ^ p ^ k) = orderOf t / p ^ k
a : ℕ
ha : ↑(Nat.factorization (exponent G)) p = ↑(Nat.factorization (sSup (Set.range fun g => orderOf g))) p + a + 1
hcoprime : Nat.coprime (orderOf (t ^ p ^ k)) (orderOf g)
⊢ orderOf t < orderOf (t ^ p ^ k * g)
[PROOFSTEP]
rw [(Commute.all _ g).orderOf_mul_eq_mul_orderOf_of_coprime hcoprime, hpk', hg, ha, ← ht, ← hk, pow_add, pow_add,
  pow_one, ← mul_assoc, ← mul_assoc, Nat.div_mul_cancel, mul_assoc, lt_mul_iff_one_lt_right <| h t, ← pow_succ']
[GOAL]
case intro.intro.intro.intro
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : exponent G ≠ 0
hne : Set.Nonempty (Set.range orderOf)
hfin : Set.Finite (Set.range orderOf)
t : G
ht : orderOf t = sSup (Set.range orderOf)
p : ℕ
hp : Nat.Prime p
hpe : ↑(Nat.factorization (sSup (Set.range fun g => orderOf g))) p < ↑(Nat.factorization (exponent G)) p
k : ℕ := ↑(Nat.factorization (orderOf t)) p
hk : k = ↑(Nat.factorization (orderOf t)) p
g : G
hg : orderOf g = p ^ ↑(Nat.factorization (exponent G)) p
hpk : p ^ k ∣ orderOf t
hpk' : orderOf (t ^ p ^ k) = orderOf t / p ^ k
a : ℕ
ha : ↑(Nat.factorization (exponent G)) p = ↑(Nat.factorization (sSup (Set.range fun g => orderOf g))) p + a + 1
hcoprime : Nat.coprime (orderOf (t ^ p ^ k)) (orderOf g)
⊢ 1 < p ^ (a + 1)
case intro.intro.intro.intro
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : exponent G ≠ 0
hne : Set.Nonempty (Set.range orderOf)
hfin : Set.Finite (Set.range orderOf)
t : G
ht : orderOf t = sSup (Set.range orderOf)
p : ℕ
hp : Nat.Prime p
hpe : ↑(Nat.factorization (sSup (Set.range fun g => orderOf g))) p < ↑(Nat.factorization (exponent G)) p
k : ℕ := ↑(Nat.factorization (orderOf t)) p
hk : k = ↑(Nat.factorization (orderOf t)) p
g : G
hg : orderOf g = p ^ ↑(Nat.factorization (exponent G)) p
hpk : p ^ k ∣ orderOf t
hpk' : orderOf (t ^ p ^ k) = orderOf t / p ^ k
a : ℕ
ha : ↑(Nat.factorization (exponent G)) p = ↑(Nat.factorization (sSup (Set.range fun g => orderOf g))) p + a + 1
hcoprime : Nat.coprime (orderOf (t ^ p ^ k)) (orderOf g)
⊢ p ^ k ∣ orderOf t
[PROOFSTEP]
exact one_lt_pow hp.one_lt a.succ_ne_zero
[GOAL]
case intro.intro.intro.intro
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : exponent G ≠ 0
hne : Set.Nonempty (Set.range orderOf)
hfin : Set.Finite (Set.range orderOf)
t : G
ht : orderOf t = sSup (Set.range orderOf)
p : ℕ
hp : Nat.Prime p
hpe : ↑(Nat.factorization (sSup (Set.range fun g => orderOf g))) p < ↑(Nat.factorization (exponent G)) p
k : ℕ := ↑(Nat.factorization (orderOf t)) p
hk : k = ↑(Nat.factorization (orderOf t)) p
g : G
hg : orderOf g = p ^ ↑(Nat.factorization (exponent G)) p
hpk : p ^ k ∣ orderOf t
hpk' : orderOf (t ^ p ^ k) = orderOf t / p ^ k
a : ℕ
ha : ↑(Nat.factorization (exponent G)) p = ↑(Nat.factorization (sSup (Set.range fun g => orderOf g))) p + a + 1
hcoprime : Nat.coprime (orderOf (t ^ p ^ k)) (orderOf g)
⊢ p ^ k ∣ orderOf t
[PROOFSTEP]
exact hpk
[GOAL]
G : Type u
inst✝ : CommMonoid G
⊢ exponent G = if ∃ g, orderOf g = 0 then 0 else ⨆ (g : G), orderOf g
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
G : Type u
inst✝ : CommMonoid G
h : ∃ g, orderOf g = 0
⊢ exponent G = 0
[PROOFSTEP]
obtain ⟨g, hg⟩ := h
[GOAL]
case pos.intro
G : Type u
inst✝ : CommMonoid G
g : G
hg : orderOf g = 0
⊢ exponent G = 0
[PROOFSTEP]
exact exponent_eq_zero_of_order_zero hg
[GOAL]
case neg
G : Type u
inst✝ : CommMonoid G
h : ¬∃ g, orderOf g = 0
⊢ exponent G = ⨆ (g : G), orderOf g
[PROOFSTEP]
have := not_exists.mp h
[GOAL]
case neg
G : Type u
inst✝ : CommMonoid G
h : ¬∃ g, orderOf g = 0
this : ∀ (x : G), ¬orderOf x = 0
⊢ exponent G = ⨆ (g : G), orderOf g
[PROOFSTEP]
exact exponent_eq_iSup_orderOf fun g => Ne.bot_lt <| this g
[GOAL]
G : Type u
inst✝¹ : CancelCommMonoid G
inst✝ : Fintype G
⊢ 1 ∈ Finset.image orderOf Finset.univ
[PROOFSTEP]
simp
[GOAL]
G : Type u
inst✝¹ : CancelCommMonoid G
inst✝ : Fintype G
⊢ exponent G = Finset.max' (Finset.image orderOf Finset.univ) (_ : ∃ x, x ∈ Finset.image orderOf Finset.univ)
[PROOFSTEP]
rw [← Finset.Nonempty.cSup_eq_max', Finset.coe_image, Finset.coe_univ, Set.image_univ, ← iSup]
[GOAL]
G : Type u
inst✝¹ : CancelCommMonoid G
inst✝ : Fintype G
⊢ exponent G = iSup orderOf
[PROOFSTEP]
exact exponent_eq_iSup_orderOf orderOf_pos
[GOAL]
G : Type u
inst✝¹ : CommGroup G
inst✝ : Group.FG G
⊢ Nat.card G ∣ Monoid.exponent G ^ Group.rank G
[PROOFSTEP]
obtain ⟨S, hS1, hS2⟩ := Group.rank_spec G
[GOAL]
case intro.intro
G : Type u
inst✝¹ : CommGroup G
inst✝ : Group.FG G
S : Finset G
hS1 : Finset.card S = Group.rank G
hS2 : closure ↑S = ⊤
⊢ Nat.card G ∣ Monoid.exponent G ^ Group.rank G
[PROOFSTEP]
rw [← hS1, ← Fintype.card_coe, ← Finset.card_univ, ← Finset.prod_const]
[GOAL]
case intro.intro
G : Type u
inst✝¹ : CommGroup G
inst✝ : Group.FG G
S : Finset G
hS1 : Finset.card S = Group.rank G
hS2 : closure ↑S = ⊤
⊢ Nat.card G ∣ ∏ _x : { x // x ∈ S }, Monoid.exponent G
[PROOFSTEP]
let f : (∀ g : S, zpowers (g : G)) →* G := noncommPiCoprod fun s t _ x y _ _ => mul_comm x _
[GOAL]
case intro.intro
G : Type u
inst✝¹ : CommGroup G
inst✝ : Group.FG G
S : Finset G
hS1 : Finset.card S = Group.rank G
hS2 : closure ↑S = ⊤
f : ((g : { x // x ∈ S }) → { x // x ∈ zpowers ↑g }) →* G :=
  noncommPiCoprod (_ : ∀ (s t : { x // x ∈ S }), s ≠ t → ∀ (x y : G), x ∈ zpowers ↑s → y ∈ zpowers ↑t → x * y = y * x)
⊢ Nat.card G ∣ ∏ _x : { x // x ∈ S }, Monoid.exponent G
[PROOFSTEP]
have hf : Function.Surjective f :=
  by
  rw [← MonoidHom.range_top_iff_surjective, eq_top_iff, ← hS2, closure_le]
  exact fun g hg => ⟨Pi.mulSingle ⟨g, hg⟩ ⟨g, mem_zpowers g⟩, noncommPiCoprod_mulSingle _ _⟩
[GOAL]
G : Type u
inst✝¹ : CommGroup G
inst✝ : Group.FG G
S : Finset G
hS1 : Finset.card S = Group.rank G
hS2 : closure ↑S = ⊤
f : ((g : { x // x ∈ S }) → { x // x ∈ zpowers ↑g }) →* G :=
  noncommPiCoprod (_ : ∀ (s t : { x // x ∈ S }), s ≠ t → ∀ (x y : G), x ∈ zpowers ↑s → y ∈ zpowers ↑t → x * y = y * x)
⊢ Function.Surjective ↑f
[PROOFSTEP]
rw [← MonoidHom.range_top_iff_surjective, eq_top_iff, ← hS2, closure_le]
[GOAL]
G : Type u
inst✝¹ : CommGroup G
inst✝ : Group.FG G
S : Finset G
hS1 : Finset.card S = Group.rank G
hS2 : closure ↑S = ⊤
f : ((g : { x // x ∈ S }) → { x // x ∈ zpowers ↑g }) →* G :=
  noncommPiCoprod (_ : ∀ (s t : { x // x ∈ S }), s ≠ t → ∀ (x y : G), x ∈ zpowers ↑s → y ∈ zpowers ↑t → x * y = y * x)
⊢ ↑S ⊆ ↑(MonoidHom.range f)
[PROOFSTEP]
exact fun g hg => ⟨Pi.mulSingle ⟨g, hg⟩ ⟨g, mem_zpowers g⟩, noncommPiCoprod_mulSingle _ _⟩
[GOAL]
case intro.intro
G : Type u
inst✝¹ : CommGroup G
inst✝ : Group.FG G
S : Finset G
hS1 : Finset.card S = Group.rank G
hS2 : closure ↑S = ⊤
f : ((g : { x // x ∈ S }) → { x // x ∈ zpowers ↑g }) →* G :=
  noncommPiCoprod (_ : ∀ (s t : { x // x ∈ S }), s ≠ t → ∀ (x y : G), x ∈ zpowers ↑s → y ∈ zpowers ↑t → x * y = y * x)
hf : Function.Surjective ↑f
⊢ Nat.card G ∣ ∏ _x : { x // x ∈ S }, Monoid.exponent G
[PROOFSTEP]
replace hf := nat_card_dvd_of_surjective f hf
[GOAL]
case intro.intro
G : Type u
inst✝¹ : CommGroup G
inst✝ : Group.FG G
S : Finset G
hS1 : Finset.card S = Group.rank G
hS2 : closure ↑S = ⊤
f : ((g : { x // x ∈ S }) → { x // x ∈ zpowers ↑g }) →* G :=
  noncommPiCoprod (_ : ∀ (s t : { x // x ∈ S }), s ≠ t → ∀ (x y : G), x ∈ zpowers ↑s → y ∈ zpowers ↑t → x * y = y * x)
hf : Nat.card G ∣ Nat.card ((g : { x // x ∈ S }) → { x // x ∈ zpowers ↑g })
⊢ Nat.card G ∣ ∏ _x : { x // x ∈ S }, Monoid.exponent G
[PROOFSTEP]
rw [Nat.card_pi] at hf
[GOAL]
case intro.intro
G : Type u
inst✝¹ : CommGroup G
inst✝ : Group.FG G
S : Finset G
hS1 : Finset.card S = Group.rank G
hS2 : closure ↑S = ⊤
f : ((g : { x // x ∈ S }) → { x // x ∈ zpowers ↑g }) →* G :=
  noncommPiCoprod (_ : ∀ (s t : { x // x ∈ S }), s ≠ t → ∀ (x y : G), x ∈ zpowers ↑s → y ∈ zpowers ↑t → x * y = y * x)
hf✝ : Nat.card G ∣ Nat.card ((g : { x // x ∈ S }) → { x // x ∈ zpowers ↑g })
hf : Nat.card G ∣ ∏ a : { x // x ∈ S }, Nat.card { x // x ∈ zpowers ↑a }
⊢ Nat.card G ∣ ∏ _x : { x // x ∈ S }, Monoid.exponent G
[PROOFSTEP]
refine' hf.trans (Finset.prod_dvd_prod_of_dvd _ _ fun g _ => _)
[GOAL]
case intro.intro
G : Type u
inst✝¹ : CommGroup G
inst✝ : Group.FG G
S : Finset G
hS1 : Finset.card S = Group.rank G
hS2 : closure ↑S = ⊤
f : ((g : { x // x ∈ S }) → { x // x ∈ zpowers ↑g }) →* G :=
  noncommPiCoprod (_ : ∀ (s t : { x // x ∈ S }), s ≠ t → ∀ (x y : G), x ∈ zpowers ↑s → y ∈ zpowers ↑t → x * y = y * x)
hf✝ : Nat.card G ∣ Nat.card ((g : { x // x ∈ S }) → { x // x ∈ zpowers ↑g })
hf : Nat.card G ∣ ∏ a : { x // x ∈ S }, Nat.card { x // x ∈ zpowers ↑a }
g : { x // x ∈ S }
x✝ : g ∈ Finset.univ
⊢ Nat.card { x // x ∈ zpowers ↑g } ∣ Monoid.exponent G
[PROOFSTEP]
rw [← order_eq_card_zpowers']
[GOAL]
case intro.intro
G : Type u
inst✝¹ : CommGroup G
inst✝ : Group.FG G
S : Finset G
hS1 : Finset.card S = Group.rank G
hS2 : closure ↑S = ⊤
f : ((g : { x // x ∈ S }) → { x // x ∈ zpowers ↑g }) →* G :=
  noncommPiCoprod (_ : ∀ (s t : { x // x ∈ S }), s ≠ t → ∀ (x y : G), x ∈ zpowers ↑s → y ∈ zpowers ↑t → x * y = y * x)
hf✝ : Nat.card G ∣ Nat.card ((g : { x // x ∈ S }) → { x // x ∈ zpowers ↑g })
hf : Nat.card G ∣ ∏ a : { x // x ∈ S }, Nat.card { x // x ∈ zpowers ↑a }
g : { x // x ∈ S }
x✝ : g ∈ Finset.univ
⊢ orderOf ↑g ∣ Monoid.exponent G
[PROOFSTEP]
exact Monoid.order_dvd_exponent (g : G)


[GOAL]
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a b : G
hb : b ∈ doset a ↑H ↑K
⊢ doset b ↑H ↑K = doset a ↑H ↑K
[PROOFSTEP]
obtain ⟨_, k, ⟨h, a, hh, rfl : _ = _, rfl⟩, hk, rfl⟩ := hb
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
k h a : G
hh : h ∈ ↑H
hk : k ∈ ↑K
⊢ doset ((fun x x_1 => x * x_1) ((fun x x_1 => x * x_1) h a) k) ↑H ↑K = doset a ↑H ↑K
[PROOFSTEP]
rw [doset, doset, ← Set.singleton_mul_singleton, ← Set.singleton_mul_singleton, mul_assoc, mul_assoc,
  Subgroup.singleton_mul_subgroup hk, ← mul_assoc, ← mul_assoc, Subgroup.subgroup_mul_singleton hh]
[GOAL]
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a b : G
h : ¬Disjoint (doset a ↑H ↑K) (doset b ↑H ↑K)
⊢ b ∈ doset a ↑H ↑K
[PROOFSTEP]
rw [Set.not_disjoint_iff] at h
[GOAL]
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a b : G
h : ∃ x, x ∈ doset a ↑H ↑K ∧ x ∈ doset b ↑H ↑K
⊢ b ∈ doset a ↑H ↑K
[PROOFSTEP]
simp only [mem_doset] at *
[GOAL]
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a b : G
h : ∃ x, (∃ x_1, x_1 ∈ ↑H ∧ ∃ y, y ∈ ↑K ∧ x = x_1 * a * y) ∧ ∃ x_1, x_1 ∈ ↑H ∧ ∃ y, y ∈ ↑K ∧ x = x_1 * b * y
⊢ ∃ x, x ∈ ↑H ∧ ∃ y, y ∈ ↑K ∧ b = x * a * y
[PROOFSTEP]
obtain ⟨x, ⟨l, hl, r, hr, hrx⟩, y, hy, ⟨r', hr', rfl⟩⟩ := h
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a b l : G
hl : l ∈ ↑H
r : G
hr : r ∈ ↑K
y : G
hy : y ∈ ↑H
r' : G
hr' : r' ∈ ↑K
hrx : y * b * r' = l * a * r
⊢ ∃ x, x ∈ ↑H ∧ ∃ y, y ∈ ↑K ∧ b = x * a * y
[PROOFSTEP]
refine' ⟨y⁻¹ * l, H.mul_mem (H.inv_mem hy) hl, r * r'⁻¹, K.mul_mem hr (K.inv_mem hr'), _⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a b l : G
hl : l ∈ ↑H
r : G
hr : r ∈ ↑K
y : G
hy : y ∈ ↑H
r' : G
hr' : r' ∈ ↑K
hrx : y * b * r' = l * a * r
⊢ b = y⁻¹ * l * a * (r * r'⁻¹)
[PROOFSTEP]
rwa [mul_assoc, mul_assoc, eq_inv_mul_iff_mul_eq, ← mul_assoc, ← mul_assoc, eq_mul_inv_iff_mul_eq]
[GOAL]
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a b : G
h : ¬Disjoint (doset a ↑H ↑K) (doset b ↑H ↑K)
⊢ doset a ↑H ↑K = doset b ↑H ↑K
[PROOFSTEP]
rw [disjoint_comm] at h
[GOAL]
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a b : G
h : ¬Disjoint (doset b ↑H ↑K) (doset a ↑H ↑K)
⊢ doset a ↑H ↑K = doset b ↑H ↑K
[PROOFSTEP]
have ha : a ∈ doset b H K := mem_doset_of_not_disjoint h
[GOAL]
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a b : G
h : ¬Disjoint (doset b ↑H ↑K) (doset a ↑H ↑K)
ha : a ∈ doset b ↑H ↑K
⊢ doset a ↑H ↑K = doset b ↑H ↑K
[PROOFSTEP]
apply doset_eq_of_mem ha
[GOAL]
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H : Subgroup G
⊢ Setoid.Rel (setoid ↑⊥ ↑H) = Setoid.Rel (QuotientGroup.leftRel H)
[PROOFSTEP]
ext a b
[GOAL]
case h.h.a
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H : Subgroup G
a b : G
⊢ Setoid.Rel (setoid ↑⊥ ↑H) a b ↔ Setoid.Rel (QuotientGroup.leftRel H) a b
[PROOFSTEP]
rw [rel_iff, Setoid.Rel, QuotientGroup.leftRel_apply]
[GOAL]
case h.h.a
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H : Subgroup G
a b : G
⊢ (∃ a_1, a_1 ∈ ⊥ ∧ ∃ b_1, b_1 ∈ H ∧ b = a_1 * a * b_1) ↔ a⁻¹ * b ∈ H
[PROOFSTEP]
constructor
[GOAL]
case h.h.a.mp
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H : Subgroup G
a b : G
⊢ (∃ a_1, a_1 ∈ ⊥ ∧ ∃ b_1, b_1 ∈ H ∧ b = a_1 * a * b_1) → a⁻¹ * b ∈ H
[PROOFSTEP]
rintro ⟨a, rfl : a = 1, b, hb, rfl⟩
[GOAL]
case h.h.a.mp.intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H : Subgroup G
a b : G
hb : b ∈ H
⊢ a⁻¹ * (1 * a * b) ∈ H
[PROOFSTEP]
change a⁻¹ * (1 * a * b) ∈ H
[GOAL]
case h.h.a.mp.intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H : Subgroup G
a b : G
hb : b ∈ H
⊢ a⁻¹ * (1 * a * b) ∈ H
[PROOFSTEP]
rwa [one_mul, inv_mul_cancel_left]
[GOAL]
case h.h.a.mpr
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H : Subgroup G
a b : G
⊢ a⁻¹ * b ∈ H → ∃ a_2, a_2 ∈ ⊥ ∧ ∃ b_1, b_1 ∈ H ∧ b = a_2 * a * b_1
[PROOFSTEP]
rintro (h : a⁻¹ * b ∈ H)
[GOAL]
case h.h.a.mpr
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H : Subgroup G
a b : G
h : a⁻¹ * b ∈ H
⊢ ∃ a_1, a_1 ∈ ⊥ ∧ ∃ b_1, b_1 ∈ H ∧ b = a_1 * a * b_1
[PROOFSTEP]
exact ⟨1, rfl, a⁻¹ * b, h, by rw [one_mul, mul_inv_cancel_left]⟩
[GOAL]
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H : Subgroup G
a b : G
h : a⁻¹ * b ∈ H
⊢ b = 1 * a * (a⁻¹ * b)
[PROOFSTEP]
rw [one_mul, mul_inv_cancel_left]
[GOAL]
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H : Subgroup G
⊢ Setoid.Rel (setoid ↑H ↑⊥) = Setoid.Rel (QuotientGroup.rightRel H)
[PROOFSTEP]
ext a b
[GOAL]
case h.h.a
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H : Subgroup G
a b : G
⊢ Setoid.Rel (setoid ↑H ↑⊥) a b ↔ Setoid.Rel (QuotientGroup.rightRel H) a b
[PROOFSTEP]
rw [rel_iff, Setoid.Rel, QuotientGroup.rightRel_apply]
[GOAL]
case h.h.a
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H : Subgroup G
a b : G
⊢ (∃ a_1, a_1 ∈ H ∧ ∃ b_1, b_1 ∈ ⊥ ∧ b = a_1 * a * b_1) ↔ b * a⁻¹ ∈ H
[PROOFSTEP]
constructor
[GOAL]
case h.h.a.mp
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H : Subgroup G
a b : G
⊢ (∃ a_1, a_1 ∈ H ∧ ∃ b_1, b_1 ∈ ⊥ ∧ b = a_1 * a * b_1) → b * a⁻¹ ∈ H
[PROOFSTEP]
rintro ⟨b, hb, a, rfl : a = 1, rfl⟩
[GOAL]
case h.h.a.mp.intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H : Subgroup G
a b : G
hb : b ∈ H
⊢ b * a * 1 * a⁻¹ ∈ H
[PROOFSTEP]
change b * a * 1 * a⁻¹ ∈ H
[GOAL]
case h.h.a.mp.intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H : Subgroup G
a b : G
hb : b ∈ H
⊢ b * a * 1 * a⁻¹ ∈ H
[PROOFSTEP]
rwa [mul_one, mul_inv_cancel_right]
[GOAL]
case h.h.a.mpr
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H : Subgroup G
a b : G
⊢ b * a⁻¹ ∈ H → ∃ a_2, a_2 ∈ H ∧ ∃ b_1, b_1 ∈ ⊥ ∧ b = a_2 * a * b_1
[PROOFSTEP]
rintro (h : b * a⁻¹ ∈ H)
[GOAL]
case h.h.a.mpr
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H : Subgroup G
a b : G
h : b * a⁻¹ ∈ H
⊢ ∃ a_1, a_1 ∈ H ∧ ∃ b_1, b_1 ∈ ⊥ ∧ b = a_1 * a * b_1
[PROOFSTEP]
exact ⟨b * a⁻¹, h, 1, rfl, by rw [mul_one, inv_mul_cancel_right]⟩
[GOAL]
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H : Subgroup G
a b : G
h : b * a⁻¹ ∈ H
⊢ b = b * a⁻¹ * a * 1
[PROOFSTEP]
rw [mul_one, inv_mul_cancel_right]
[GOAL]
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a b : G
⊢ mk H K a = mk H K b ↔ ∃ h, h ∈ H ∧ ∃ k, k ∈ K ∧ b = h * a * k
[PROOFSTEP]
rw [Quotient.eq'']
[GOAL]
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a b : G
⊢ Setoid.r a b ↔ ∃ h, h ∈ H ∧ ∃ k, k ∈ K ∧ b = h * a * k
[PROOFSTEP]
apply rel_iff
[GOAL]
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g✝ : G
H K : Subgroup G
g : G
⊢ ∃ h k, h ∈ H ∧ k ∈ K ∧ Quotient.out' (mk H K g) = h * g * k
[PROOFSTEP]
have := eq H K (mk H K g : Quotient ↑H ↑K).out' g
[GOAL]
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g✝ : G
H K : Subgroup G
g : G
this : mk H K (Quotient.out' (mk H K g)) = mk H K g ↔ ∃ h, h ∈ H ∧ ∃ k, k ∈ K ∧ g = h * Quotient.out' (mk H K g) * k
⊢ ∃ h k, h ∈ H ∧ k ∈ K ∧ Quotient.out' (mk H K g) = h * g * k
[PROOFSTEP]
rw [out_eq'] at this
[GOAL]
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g✝ : G
H K : Subgroup G
g : G
this : mk H K g = mk H K g ↔ ∃ h, h ∈ H ∧ ∃ k, k ∈ K ∧ g = h * Quotient.out' (mk H K g) * k
⊢ ∃ h k, h ∈ H ∧ k ∈ K ∧ Quotient.out' (mk H K g) = h * g * k
[PROOFSTEP]
obtain ⟨h, h_h, k, hk, T⟩ := this.1 rfl
[GOAL]
case intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g✝ : G
H K : Subgroup G
g : G
this : mk H K g = mk H K g ↔ ∃ h, h ∈ H ∧ ∃ k, k ∈ K ∧ g = h * Quotient.out' (mk H K g) * k
h : G
h_h : h ∈ H
k : G
hk : k ∈ K
T : g = h * Quotient.out' (mk H K g) * k
⊢ ∃ h k, h ∈ H ∧ k ∈ K ∧ Quotient.out' (mk H K g) = h * g * k
[PROOFSTEP]
refine' ⟨h⁻¹, k⁻¹, H.inv_mem h_h, K.inv_mem hk, eq_mul_inv_of_mul_eq (eq_inv_mul_of_mul_eq _)⟩
[GOAL]
case intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g✝ : G
H K : Subgroup G
g : G
this : mk H K g = mk H K g ↔ ∃ h, h ∈ H ∧ ∃ k, k ∈ K ∧ g = h * Quotient.out' (mk H K g) * k
h : G
h_h : h ∈ H
k : G
hk : k ∈ K
T : g = h * Quotient.out' (mk H K g) * k
⊢ h * (Quotient.out' (mk H K g) * k) = g
[PROOFSTEP]
rw [← mul_assoc, ← T]
[GOAL]
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a b : G
h : doset a ↑H ↑K = doset b ↑H ↑K
⊢ mk H K a = mk H K b
[PROOFSTEP]
rw [eq]
[GOAL]
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a b : G
h : doset a ↑H ↑K = doset b ↑H ↑K
⊢ ∃ h, h ∈ H ∧ ∃ k, k ∈ K ∧ b = h * a * k
[PROOFSTEP]
exact mem_doset.mp (h.symm ▸ mem_doset_self H K b)
[GOAL]
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a b : Quotient ↑H.toSubmonoid ↑K
⊢ a ≠ b → Disjoint (doset (Quotient.out' a) ↑H ↑K) (doset (Quotient.out' b) ↑H ↑K)
[PROOFSTEP]
contrapose!
[GOAL]
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a b : Quotient ↑H.toSubmonoid ↑K
⊢ ¬Disjoint (doset (Quotient.out' a) ↑H ↑K) (doset (Quotient.out' b) ↑H ↑K) → a = b
[PROOFSTEP]
intro h
[GOAL]
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a b : Quotient ↑H.toSubmonoid ↑K
h : ¬Disjoint (doset (Quotient.out' a) ↑H ↑K) (doset (Quotient.out' b) ↑H ↑K)
⊢ a = b
[PROOFSTEP]
simpa [out_eq'] using mk_eq_of_doset_eq (eq_of_not_disjoint h)
[GOAL]
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
⊢ ⋃ (q : Quotient ↑H ↑K), quotToDoset H K q = Set.univ
[PROOFSTEP]
ext x
[GOAL]
case h
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
x : G
⊢ x ∈ ⋃ (q : Quotient ↑H ↑K), quotToDoset H K q ↔ x ∈ Set.univ
[PROOFSTEP]
simp only [Set.mem_iUnion, quotToDoset, mem_doset, SetLike.mem_coe, exists_prop, Set.mem_univ, iff_true_iff]
[GOAL]
case h
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
x : G
⊢ ∃ i x_1, x_1 ∈ H ∧ ∃ y, y ∈ K ∧ x = x_1 * Quotient.out' i * y
[PROOFSTEP]
use mk H K x
[GOAL]
case h
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
x : G
⊢ ∃ x_1, x_1 ∈ H ∧ ∃ y, y ∈ K ∧ x = x_1 * Quotient.out' (mk H K x) * y
[PROOFSTEP]
obtain ⟨h, k, h3, h4, h5⟩ := mk_out'_eq_mul H K x
[GOAL]
case h.intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
x h k : G
h3 : h ∈ H
h4 : k ∈ K
h5 : Quotient.out' (mk H K x) = h * x * k
⊢ ∃ x_1, x_1 ∈ H ∧ ∃ y, y ∈ K ∧ x = x_1 * Quotient.out' (mk H K x) * y
[PROOFSTEP]
refine' ⟨h⁻¹, H.inv_mem h3, k⁻¹, K.inv_mem h4, _⟩
[GOAL]
case h.intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
x h k : G
h3 : h ∈ H
h4 : k ∈ K
h5 : Quotient.out' (mk H K x) = h * x * k
⊢ x = h⁻¹ * Quotient.out' (mk H K x) * k⁻¹
[PROOFSTEP]
simp only [h5, Subgroup.coe_mk, ← mul_assoc, one_mul, mul_left_inv, mul_inv_cancel_right]
[GOAL]
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a : G
⊢ ⋃ (k : { x // x ∈ K }), rightCoset (↑H) (a * ↑k) = doset a ↑H ↑K
[PROOFSTEP]
ext x
[GOAL]
case h
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a x : G
⊢ x ∈ ⋃ (k : { x // x ∈ K }), rightCoset (↑H) (a * ↑k) ↔ x ∈ doset a ↑H ↑K
[PROOFSTEP]
simp only [mem_rightCoset_iff, exists_prop, mul_inv_rev, Set.mem_iUnion, mem_doset, Subgroup.mem_carrier,
  SetLike.mem_coe]
[GOAL]
case h
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a x : G
⊢ (∃ i, x * ((↑i)⁻¹ * a⁻¹) ∈ H) ↔ ∃ x_1, x_1 ∈ H ∧ ∃ y, y ∈ K ∧ x = x_1 * a * y
[PROOFSTEP]
constructor
[GOAL]
case h.mp
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a x : G
⊢ (∃ i, x * ((↑i)⁻¹ * a⁻¹) ∈ H) → ∃ x_1, x_1 ∈ H ∧ ∃ y, y ∈ K ∧ x = x_1 * a * y
[PROOFSTEP]
rintro ⟨y, h_h⟩
[GOAL]
case h.mp.intro
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a x : G
y : { x // x ∈ K }
h_h : x * ((↑y)⁻¹ * a⁻¹) ∈ H
⊢ ∃ x_1, x_1 ∈ H ∧ ∃ y, y ∈ K ∧ x = x_1 * a * y
[PROOFSTEP]
refine' ⟨x * (y⁻¹ * a⁻¹), h_h, y, y.2, _⟩
[GOAL]
case h.mp.intro
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a x : G
y : { x // x ∈ K }
h_h : x * ((↑y)⁻¹ * a⁻¹) ∈ H
⊢ x = x * (↑y⁻¹ * a⁻¹) * a * ↑y
[PROOFSTEP]
simp only [← mul_assoc, Subgroup.coe_mk, inv_mul_cancel_right, SubgroupClass.coe_inv]
[GOAL]
case h.mpr
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a x : G
⊢ (∃ x_1, x_1 ∈ H ∧ ∃ y, y ∈ K ∧ x = x_1 * a * y) → ∃ i, x * ((↑i)⁻¹ * a⁻¹) ∈ H
[PROOFSTEP]
rintro ⟨x, hx, y, hy, hxy⟩
[GOAL]
case h.mpr.intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a x✝ x : G
hx : x ∈ H
y : G
hy : y ∈ K
hxy : x✝ = x * a * y
⊢ ∃ i, x✝ * ((↑i)⁻¹ * a⁻¹) ∈ H
[PROOFSTEP]
refine' ⟨⟨y, hy⟩, _⟩
[GOAL]
case h.mpr.intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a x✝ x : G
hx : x ∈ H
y : G
hy : y ∈ K
hxy : x✝ = x * a * y
⊢ x✝ * ((↑{ val := y, property := hy })⁻¹ * a⁻¹) ∈ H
[PROOFSTEP]
simp only [hxy, ← mul_assoc, hx, mul_inv_cancel_right, Subgroup.coe_mk]
[GOAL]
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a : G
⊢ ⋃ (h : { x // x ∈ H }), leftCoset (↑h * a) ↑K = doset a ↑H ↑K
[PROOFSTEP]
ext x
[GOAL]
case h
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a x : G
⊢ x ∈ ⋃ (h : { x // x ∈ H }), leftCoset (↑h * a) ↑K ↔ x ∈ doset a ↑H ↑K
[PROOFSTEP]
simp only [mem_leftCoset_iff, mul_inv_rev, Set.mem_iUnion, mem_doset]
[GOAL]
case h
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a x : G
⊢ (∃ i, a⁻¹ * (↑i)⁻¹ * x ∈ ↑K) ↔ ∃ x_1, x_1 ∈ ↑H ∧ ∃ y, y ∈ ↑K ∧ x = x_1 * a * y
[PROOFSTEP]
constructor
[GOAL]
case h.mp
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a x : G
⊢ (∃ i, a⁻¹ * (↑i)⁻¹ * x ∈ ↑K) → ∃ x_1, x_1 ∈ ↑H ∧ ∃ y, y ∈ ↑K ∧ x = x_1 * a * y
[PROOFSTEP]
rintro ⟨y, h_h⟩
[GOAL]
case h.mp.intro
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a x : G
y : { x // x ∈ H }
h_h : a⁻¹ * (↑y)⁻¹ * x ∈ ↑K
⊢ ∃ x_1, x_1 ∈ ↑H ∧ ∃ y, y ∈ ↑K ∧ x = x_1 * a * y
[PROOFSTEP]
refine' ⟨y, y.2, a⁻¹ * y⁻¹ * x, h_h, _⟩
[GOAL]
case h.mp.intro
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a x : G
y : { x // x ∈ H }
h_h : a⁻¹ * (↑y)⁻¹ * x ∈ ↑K
⊢ x = ↑y * a * (a⁻¹ * ↑y⁻¹ * x)
[PROOFSTEP]
simp only [← mul_assoc, one_mul, mul_right_inv, mul_inv_cancel_right, SubgroupClass.coe_inv]
[GOAL]
case h.mpr
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a x : G
⊢ (∃ x_1, x_1 ∈ ↑H ∧ ∃ y, y ∈ ↑K ∧ x = x_1 * a * y) → ∃ i, a⁻¹ * (↑i)⁻¹ * x ∈ ↑K
[PROOFSTEP]
rintro ⟨x, hx, y, hy, hxy⟩
[GOAL]
case h.mpr.intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a x✝ x : G
hx : x ∈ ↑H
y : G
hy : y ∈ ↑K
hxy : x✝ = x * a * y
⊢ ∃ i, a⁻¹ * (↑i)⁻¹ * x✝ ∈ ↑K
[PROOFSTEP]
refine' ⟨⟨x, hx⟩, _⟩
[GOAL]
case h.mpr.intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a x✝ x : G
hx : x ∈ ↑H
y : G
hy : y ∈ ↑K
hxy : x✝ = x * a * y
⊢ a⁻¹ * (↑{ val := x, property := hx })⁻¹ * x✝ ∈ ↑K
[PROOFSTEP]
simp only [hxy, ← mul_assoc, hy, one_mul, mul_left_inv, Subgroup.coe_mk, inv_mul_cancel_right]
[GOAL]
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H : Subgroup G
⊢ Quotient ↑⊥.toSubmonoid ↑H = (G ⧸ H)
[PROOFSTEP]
unfold Quotient
[GOAL]
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H : Subgroup G
⊢ _root_.Quotient (setoid ↑⊥.toSubmonoid ↑H) = (G ⧸ H)
[PROOFSTEP]
congr
[GOAL]
case e_s
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H : Subgroup G
⊢ setoid ↑⊥.toSubmonoid ↑H = QuotientGroup.leftRel H
[PROOFSTEP]
ext
[GOAL]
case e_s.H
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H : Subgroup G
a✝ b✝ : G
⊢ Setoid.Rel (setoid ↑⊥.toSubmonoid ↑H) a✝ b✝ ↔ Setoid.Rel (QuotientGroup.leftRel H) a✝ b✝
[PROOFSTEP]
simp_rw [← bot_rel_eq_leftRel H]
[GOAL]
case e_s.H
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H : Subgroup G
a✝ b✝ : G
⊢ Setoid.Rel (setoid ↑⊥.toSubmonoid ↑H) a✝ b✝ ↔ Setoid.Rel (setoid ↑⊥ ↑H) a✝ b✝
[PROOFSTEP]
rfl
[GOAL]
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H : Subgroup G
⊢ Quotient ↑H.toSubmonoid ↑⊥ = _root_.Quotient (QuotientGroup.rightRel H)
[PROOFSTEP]
unfold Quotient
[GOAL]
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H : Subgroup G
⊢ _root_.Quotient (setoid ↑H.toSubmonoid ↑⊥) = _root_.Quotient (QuotientGroup.rightRel H)
[PROOFSTEP]
congr
[GOAL]
case e_s
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H : Subgroup G
⊢ setoid ↑H.toSubmonoid ↑⊥ = QuotientGroup.rightRel H
[PROOFSTEP]
ext
[GOAL]
case e_s.H
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H : Subgroup G
a✝ b✝ : G
⊢ Setoid.Rel (setoid ↑H.toSubmonoid ↑⊥) a✝ b✝ ↔ Setoid.Rel (QuotientGroup.rightRel H) a✝ b✝
[PROOFSTEP]
simp_rw [← rel_bot_eq_right_group_rel H]
[GOAL]
case e_s.H
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H : Subgroup G
a✝ b✝ : G
⊢ Setoid.Rel (setoid ↑H.toSubmonoid ↑⊥) a✝ b✝ ↔ Setoid.Rel (setoid ↑H ↑⊥) a✝ b✝
[PROOFSTEP]
rfl