p : ℕ
G : Type u_1
inst✝ : Group G
p₁ p₂ : ℕ
hp₁ : Fact (Nat.Prime p₁)
hp₂ : Fact (Nat.Prime p₂)
hne : p₁ ≠ p₂
H₁ H₂ : Subgroup G
hH₁ : IsPGroup p₁ { x // x ∈ H₁ }
hH₂ : IsPGroup p₂ { x // x ∈ H₂ }
⊢ ∀ {x : G}, x ∈ H₁ → x ∈ H₂ → x = 1
p : ℕ
G : Type u_1
inst✝ : Group G
p₁ p₂ : ℕ
hp₁ : Fact (Nat.Prime p₁)
hp₂ : Fact (Nat.Prime p₂)
hne : p₁ ≠ p₂
H₁ H₂ : Subgroup G
hH₁ : IsPGroup p₁ { x // x ∈ H₁ }
hH₂ : IsPGroup p₂ { x // x ∈ H₂ }
⊢ Disjoint H₁ H₂
rw [Subgroup.disjoint_def]
p : ℕ
G : Type u_1
inst✝ : Group G
p₁ p₂ : ℕ
hp₁ : Fact (Nat.Prime p₁)
hp₂ : Fact (Nat.Prime p₂)
hne : p₁ ≠ p₂
H₁ H₂ : Subgroup G
hH₁ : IsPGroup p₁ { x // x ∈ H₁ }
hH₂ : IsPGroup p₂ { x // x ∈ H₂ }
x : G
hx₁ : x ∈ H₁
hx₂ : x ∈ H₂
⊢ x = 1
p : ℕ
G : Type u_1
inst✝ : Group G
p₁ p₂ : ℕ
hp₁ : Fact (Nat.Prime p₁)
hp₂ : Fact (Nat.Prime p₂)
hne : p₁ ≠ p₂
H₁ H₂ : Subgroup G
hH₁ : IsPGroup p₁ { x // x ∈ H₁ }
hH₂ : IsPGroup p₂ { x // x ∈ H₂ }
⊢ ∀ {x : G}, x ∈ H₁ → x ∈ H₂ → x = 1
intro x hx₁ hx₂
case intro
p : ℕ
G : Type u_1
inst✝ : Group G
p₁ p₂ : ℕ
hp₁ : Fact (Nat.Prime p₁)
hp₂ : Fact (Nat.Prime p₂)
hne : p₁ ≠ p₂
H₁ H₂ : Subgroup G
hH₁ : IsPGroup p₁ { x // x ∈ H₁ }
hH₂ : IsPGroup p₂ { x // x ∈ H₂ }
x : G
hx₁ : x ∈ H₁
hx₂ : x ∈ H₂
n₁ : ℕ
hn₁ : orderOf { val := x, property := hx₁ } = p₁ ^ n₁
⊢ x = 1
p : ℕ
G : Type u_1
inst✝ : Group G
p₁ p₂ : ℕ
hp₁ : Fact (Nat.Prime p₁)
hp₂ : Fact (Nat.Prime p₂)
hne : p₁ ≠ p₂
H₁ H₂ : Subgroup G
hH₁ : IsPGroup p₁ { x // x ∈ H₁ }
hH₂ : IsPGroup p₂ { x // x ∈ H₂ }
x : G
hx₁ : x ∈ H₁
hx₂ : x ∈ H₂
⊢ x = 1
obtain ⟨n₁, hn₁⟩ := iff_orderOf.mp hH₁ ⟨x, hx₁⟩
case intro.intro
p : ℕ
G : Type u_1
inst✝ : Group G
p₁ p₂ : ℕ
hp₁ : Fact (Nat.Prime p₁)
hp₂ : Fact (Nat.Prime p₂)
hne : p₁ ≠ p₂
H₁ H₂ : Subgroup G
hH₁ : IsPGroup p₁ { x // x ∈ H₁ }
hH₂ : IsPGroup p₂ { x // x ∈ H₂ }
x : G
hx₁ : x ∈ H₁
hx₂ : x ∈ H₂
n₁ : ℕ
hn₁ : orderOf { val := x, property := hx₁ } = p₁ ^ n₁
n₂ : ℕ
hn₂ : orderOf { val := x, property := hx₂ } = p₂ ^ n₂
⊢ x = 1
case intro
p : ℕ
G : Type u_1
inst✝ : Group G
p₁ p₂ : ℕ
hp₁ : Fact (Nat.Prime p₁)
hp₂ : Fact (Nat.Prime p₂)
hne : p₁ ≠ p₂
H₁ H₂ : Subgroup G
hH₁ : IsPGroup p₁ { x // x ∈ H₁ }
hH₂ : IsPGroup p₂ { x // x ∈ H₂ }
x : G
hx₁ : x ∈ H₁
hx₂ : x ∈ H₂
n₁ : ℕ
hn₁ : orderOf { val := x, property := hx₁ } = p₁ ^ n₁
⊢ x = 1
obtain ⟨n₂, hn₂⟩ := iff_orderOf.mp hH₂ ⟨x, hx₂⟩
case intro.intro
p : ℕ
G : Type u_1
inst✝ : Group G
p₁ p₂ : ℕ
hp₁ : Fact (Nat.Prime p₁)
hp₂ : Fact (Nat.Prime p₂)
hne : p₁ ≠ p₂
H₁ H₂ : Subgroup G
hH₁ : IsPGroup p₁ { x // x ∈ H₁ }
hH₂ : IsPGroup p₂ { x // x ∈ H₂ }
x : G
hx₁ : x ∈ H₁
hx₂ : x ∈ H₂
n₁ : ℕ
hn₁ : orderOf x = p₁ ^ n₁
n₂ : ℕ
hn₂ : orderOf x = p₂ ^ n₂
⊢ x = 1
case intro.intro
p : ℕ
G : Type u_1
inst✝ : Group G
p₁ p₂ : ℕ
hp₁ : Fact (Nat.Prime p₁)
hp₂ : Fact (Nat.Prime p₂)
hne : p₁ ≠ p₂
H₁ H₂ : Subgroup G
hH₁ : IsPGroup p₁ { x // x ∈ H₁ }
hH₂ : IsPGroup p₂ { x // x ∈ H₂ }
x : G
hx₁ : x ∈ H₁
hx₂ : x ∈ H₂
n₁ : ℕ
hn₁ : orderOf { val := x, property := hx₁ } = p₁ ^ n₁
n₂ : ℕ
hn₂ : orderOf { val := x, property := hx₂ } = p₂ ^ n₂
⊢ x = 1
rw [← orderOf_subgroup, Subgroup.coe_mk] at hn₁ hn₂
case intro.intro
p : ℕ
G : Type u_1
inst✝ : Group G
p₁ p₂ : ℕ
hp₁ : Fact (Nat.Prime p₁)
hp₂ : Fact (Nat.Prime p₂)
hne : p₁ ≠ p₂
H₁ H₂ : Subgroup G
hH₁ : IsPGroup p₁ { x // x ∈ H₁ }
hH₂ : IsPGroup p₂ { x // x ∈ H₂ }
x : G
hx₁ : x ∈ H₁
hx₂ : x ∈ H₂
n₁ : ℕ
hn₁ : orderOf x = p₁ ^ n₁
n₂ : ℕ
hn₂ : orderOf x = p₂ ^ n₂
this : p₁ ^ n₁ = p₂ ^ n₂
⊢ x = 1
case intro.intro
p : ℕ
G : Type u_1
inst✝ : Group G
p₁ p₂ : ℕ
hp₁ : Fact (Nat.Prime p₁)
hp₂ : Fact (Nat.Prime p₂)
hne : p₁ ≠ p₂
H₁ H₂ : Subgroup G
hH₁ : IsPGroup p₁ { x // x ∈ H₁ }
hH₂ : IsPGroup p₂ { x // x ∈ H₂ }
x : G
hx₁ : x ∈ H₁
hx₂ : x ∈ H₂
n₁ : ℕ
hn₁ : orderOf x = p₁ ^ n₁
n₂ : ℕ
hn₂ : orderOf x = p₂ ^ n₂
⊢ x = 1
have : p₁ ^ n₁ = p₂ ^ n₂ := by rw [← hn₁, ← hn₂]
case intro.intro.inl
p : ℕ
G : Type u_1
inst✝ : Group G
p₁ p₂ : ℕ
hp₁ : Fact (Nat.Prime p₁)
hp₂ : Fact (Nat.Prime p₂)
hne : p₁ ≠ p₂
H₁ H₂ : Subgroup G
hH₁ : IsPGroup p₁ { x // x ∈ H₁ }
hH₂ : IsPGroup p₂ { x // x ∈ H₂ }
x : G
hx₁ : x ∈ H₁
hx₂ : x ∈ H₂
n₂ : ℕ
hn₂ : orderOf x = p₂ ^ n₂
hn₁ : orderOf x = p₁ ^ 0
this : p₁ ^ 0 = p₂ ^ n₂
⊢ x = 1

case intro.intro.inr
p : ℕ
G : Type u_1
inst✝ : Group G
p₁ p₂ : ℕ
hp₁ : Fact (Nat.Prime p₁)
hp₂ : Fact (Nat.Prime p₂)
hne : p₁ ≠ p₂
H₁ H₂ : Subgroup G
hH₁ : IsPGroup p₁ { x // x ∈ H₁ }
hH₂ : IsPGroup p₂ { x // x ∈ H₂ }
x : G
hx₁ : x ∈ H₁
hx₂ : x ∈ H₂
n₁ : ℕ
hn₁✝ : orderOf x = p₁ ^ n₁
n₂ : ℕ
hn₂ : orderOf x = p₂ ^ n₂
this : p₁ ^ n₁ = p₂ ^ n₂
hn₁ : n₁ > 0
⊢ x = 1
case intro.intro
p : ℕ
G : Type u_1
inst✝ : Group G
p₁ p₂ : ℕ
hp₁ : Fact (Nat.Prime p₁)
hp₂ : Fact (Nat.Prime p₂)
hne : p₁ ≠ p₂
H₁ H₂ : Subgroup G
hH₁ : IsPGroup p₁ { x // x ∈ H₁ }
hH₂ : IsPGroup p₂ { x // x ∈ H₂ }
x : G
hx₁ : x ∈ H₁
hx₂ : x ∈ H₂
n₁ : ℕ
hn₁ : orderOf x = p₁ ^ n₁
n₂ : ℕ
hn₂ : orderOf x = p₂ ^ n₂
this : p₁ ^ n₁ = p₂ ^ n₂
⊢ x = 1
rcases n₁.eq_zero_or_pos with (rfl | hn₁)
no goals
p : ℕ
G : Type u_1
inst✝ : Group G
p₁ p₂ : ℕ
hp₁ : Fact (Nat.Prime p₁)
hp₂ : Fact (Nat.Prime p₂)
hne : p₁ ≠ p₂
H₁ H₂ : Subgroup G
hH₁ : IsPGroup p₁ { x // x ∈ H₁ }
hH₂ : IsPGroup p₂ { x // x ∈ H₂ }
x : G
hx₁ : x ∈ H₁
hx₂ : x ∈ H₂
n₁ : ℕ
hn₁ : orderOf x = p₁ ^ n₁
n₂ : ℕ
hn₂ : orderOf x = p₂ ^ n₂
⊢ p₁ ^ n₁ = p₂ ^ n₂
rw [← hn₁, ← hn₂]
no goals
case intro.intro.inl
p : ℕ
G : Type u_1
inst✝ : Group G
p₁ p₂ : ℕ
hp₁ : Fact (Nat.Prime p₁)
hp₂ : Fact (Nat.Prime p₂)
hne : p₁ ≠ p₂
H₁ H₂ : Subgroup G
hH₁ : IsPGroup p₁ { x // x ∈ H₁ }
hH₂ : IsPGroup p₂ { x // x ∈ H₂ }
x : G
hx₁ : x ∈ H₁
hx₂ : x ∈ H₂
n₂ : ℕ
hn₂ : orderOf x = p₂ ^ n₂
hn₁ : orderOf x = p₁ ^ 0
this : p₁ ^ 0 = p₂ ^ n₂
⊢ x = 1
simpa using hn₁
no goals
case intro.intro.inr
p : ℕ
G : Type u_1
inst✝ : Group G
p₁ p₂ : ℕ
hp₁ : Fact (Nat.Prime p₁)
hp₂ : Fact (Nat.Prime p₂)
hne : p₁ ≠ p₂
H₁ H₂ : Subgroup G
hH₁ : IsPGroup p₁ { x // x ∈ H₁ }
hH₂ : IsPGroup p₂ { x // x ∈ H₂ }
x : G
hx₁ : x ∈ H₁
hx₂ : x ∈ H₂
n₁ : ℕ
hn₁✝ : orderOf x = p₁ ^ n₁
n₂ : ℕ
hn₂ : orderOf x = p₂ ^ n₂
this : p₁ ^ n₁ = p₂ ^ n₂
hn₁ : n₁ > 0
⊢ x = 1
exact absurd (eq_of_prime_pow_eq hp₁.out.prime hp₂.out.prime hn₁ this) hne