case intro.zero.intro
G : Type u_1
H : Type ?u.192353
inst✝ : CommMonoid G
p : ℕ
hp : Fact (Nat.Prime p)
p' : ℕ
hp' : Fact (Nat.Prime p')
hne : p ≠ p'
g : G
hn : orderOf g = p ^ Nat.zero
n' : ℕ
hn' : orderOf g = p' ^ n'
⊢ g = 1

case intro.succ.intro
G : Type u_1
H : Type ?u.192353
inst✝ : CommMonoid G
p : ℕ
hp : Fact (Nat.Prime p)
p' : ℕ
hp' : Fact (Nat.Prime p')
hne : p ≠ p'
g : G
n : ℕ
hn : orderOf g = p ^ Nat.succ n
n' : ℕ
hn' : orderOf g = p' ^ n'
⊢ g = 1
G : Type u_1
H : Type ?u.192353
inst✝ : CommMonoid G
p : ℕ
hp : Fact (Nat.Prime p)
p' : ℕ
hp' : Fact (Nat.Prime p')
hne : p ≠ p'
⊢ ∀ {x : G}, x ∈ primaryComponent G p → x ∈ primaryComponent G p' → x = 1
rintro g ⟨_ | n, hn⟩ ⟨n', hn'⟩
no goals
case intro.zero.intro
G : Type u_1
H : Type ?u.192353
inst✝ : CommMonoid G
p : ℕ
hp : Fact (Nat.Prime p)
p' : ℕ
hp' : Fact (Nat.Prime p')
hne : p ≠ p'
g : G
hn : orderOf g = p ^ Nat.zero
n' : ℕ
hn' : orderOf g = p' ^ n'
⊢ g = 1
rwa [pow_zero, orderOf_eq_one_iff] at hn
no goals
case intro.succ.intro
G : Type u_1
H : Type ?u.192353
inst✝ : CommMonoid G
p : ℕ
hp : Fact (Nat.Prime p)
p' : ℕ
hp' : Fact (Nat.Prime p')
hne : p ≠ p'
g : G
n : ℕ
hn : orderOf g = p ^ Nat.succ n
n' : ℕ
hn' : orderOf g = p' ^ n'
⊢ g = 1
exact
  absurd (eq_of_prime_pow_eq hp.out.prime hp'.out.prime n.succ_pos (hn.symm.trans hn')) hne