case intro
p : ℕ
G : Type u_2
inst✝³ : Group G
G₂ : Type u_1
inst✝² : Group G₂
p₁ p₂ : ℕ
hp₁ : Fact (Nat.Prime p₁)
hp₂ : Fact (Nat.Prime p₂)
hne : p₁ ≠ p₂
H₁ : Subgroup G
H₂ : Subgroup G₂
inst✝¹ : Fintype { x // x ∈ H₁ }
inst✝ : Fintype { x // x ∈ H₂ }
hH₁ : IsPGroup p₁ { x // x ∈ H₁ }
hH₂ : IsPGroup p₂ { x // x ∈ H₂ }
n₁ : ℕ
heq₁ : card { x // x ∈ H₁ } = p₁ ^ n₁
⊢ Nat.coprime (card { x // x ∈ H₁ }) (card { x // x ∈ H₂ })
p : ℕ
G : Type u_2
inst✝³ : Group G
G₂ : Type u_1
inst✝² : Group G₂
p₁ p₂ : ℕ
hp₁ : Fact (Nat.Prime p₁)
hp₂ : Fact (Nat.Prime p₂)
hne : p₁ ≠ p₂
H₁ : Subgroup G
H₂ : Subgroup G₂
inst✝¹ : Fintype { x // x ∈ H₁ }
inst✝ : Fintype { x // x ∈ H₂ }
hH₁ : IsPGroup p₁ { x // x ∈ H₁ }
hH₂ : IsPGroup p₂ { x // x ∈ H₂ }
⊢ Nat.coprime (card { x // x ∈ H₁ }) (card { x // x ∈ H₂ })
obtain ⟨n₁, heq₁⟩ := iff_card.mp hH₁
case intro
p : ℕ
G : Type u_2
inst✝³ : Group G
G₂ : Type u_1
inst✝² : Group G₂
p₁ p₂ : ℕ
hp₁ : Fact (Nat.Prime p₁)
hp₂ : Fact (Nat.Prime p₂)
hne : p₁ ≠ p₂
H₁ : Subgroup G
H₂ : Subgroup G₂
inst✝¹ : Fintype { x // x ∈ H₁ }
inst✝ : Fintype { x // x ∈ H₂ }
hH₁ : IsPGroup p₁ { x // x ∈ H₁ }
hH₂ : IsPGroup p₂ { x // x ∈ H₂ }
n₁ : ℕ
heq₁ : card { x // x ∈ H₁ } = p₁ ^ n₁
⊢ Nat.coprime (p₁ ^ n₁) (card { x // x ∈ H₂ })
case intro
p : ℕ
G : Type u_2
inst✝³ : Group G
G₂ : Type u_1
inst✝² : Group G₂
p₁ p₂ : ℕ
hp₁ : Fact (Nat.Prime p₁)
hp₂ : Fact (Nat.Prime p₂)
hne : p₁ ≠ p₂
H₁ : Subgroup G
H₂ : Subgroup G₂
inst✝¹ : Fintype { x // x ∈ H₁ }
inst✝ : Fintype { x // x ∈ H₂ }
hH₁ : IsPGroup p₁ { x // x ∈ H₁ }
hH₂ : IsPGroup p₂ { x // x ∈ H₂ }
n₁ : ℕ
heq₁ : card { x // x ∈ H₁ } = p₁ ^ n₁
⊢ Nat.coprime (card { x // x ∈ H₁ }) (card { x // x ∈ H₂ })
rw [heq₁]
case intro
p : ℕ
G : Type u_2
inst✝³ : Group G
G₂ : Type u_1
inst✝² : Group G₂
p₁ p₂ : ℕ
hp₁ : Fact (Nat.Prime p₁)
hp₂ : Fact (Nat.Prime p₂)
hne : p₁ ≠ p₂
H₁ : Subgroup G
H₂ : Subgroup G₂
inst✝¹ : Fintype { x // x ∈ H₁ }
inst✝ : Fintype { x // x ∈ H₂ }
hH₁ : IsPGroup p₁ { x // x ∈ H₁ }
hH₂ : IsPGroup p₂ { x // x ∈ H₂ }
n₁ : ℕ
⊢ Nat.coprime (p₁ ^ n₁) (card { x // x ∈ H₂ })
case intro
p : ℕ
G : Type u_2
inst✝³ : Group G
G₂ : Type u_1
inst✝² : Group G₂
p₁ p₂ : ℕ
hp₁ : Fact (Nat.Prime p₁)
hp₂ : Fact (Nat.Prime p₂)
hne : p₁ ≠ p₂
H₁ : Subgroup G
H₂ : Subgroup G₂
inst✝¹ : Fintype { x // x ∈ H₁ }
inst✝ : Fintype { x // x ∈ H₂ }
hH₁ : IsPGroup p₁ { x // x ∈ H₁ }
hH₂ : IsPGroup p₂ { x // x ∈ H₂ }
n₁ : ℕ
heq₁ : card { x // x ∈ H₁ } = p₁ ^ n₁
⊢ Nat.coprime (p₁ ^ n₁) (card { x // x ∈ H₂ })
clear heq₁
case intro.intro
p : ℕ
G : Type u_2
inst✝³ : Group G
G₂ : Type u_1
inst✝² : Group G₂
p₁ p₂ : ℕ
hp₁ : Fact (Nat.Prime p₁)
hp₂ : Fact (Nat.Prime p₂)
hne : p₁ ≠ p₂
H₁ : Subgroup G
H₂ : Subgroup G₂
inst✝¹ : Fintype { x // x ∈ H₁ }
inst✝ : Fintype { x // x ∈ H₂ }
hH₁ : IsPGroup p₁ { x // x ∈ H₁ }
hH₂ : IsPGroup p₂ { x // x ∈ H₂ }
n₁ n₂ : ℕ
heq₂ : card { x // x ∈ H₂ } = p₂ ^ n₂
⊢ Nat.coprime (p₁ ^ n₁) (card { x // x ∈ H₂ })
case intro
p : ℕ
G : Type u_2
inst✝³ : Group G
G₂ : Type u_1
inst✝² : Group G₂
p₁ p₂ : ℕ
hp₁ : Fact (Nat.Prime p₁)
hp₂ : Fact (Nat.Prime p₂)
hne : p₁ ≠ p₂
H₁ : Subgroup G
H₂ : Subgroup G₂
inst✝¹ : Fintype { x // x ∈ H₁ }
inst✝ : Fintype { x // x ∈ H₂ }
hH₁ : IsPGroup p₁ { x // x ∈ H₁ }
hH₂ : IsPGroup p₂ { x // x ∈ H₂ }
n₁ : ℕ
⊢ Nat.coprime (p₁ ^ n₁) (card { x // x ∈ H₂ })
obtain ⟨n₂, heq₂⟩ := iff_card.mp hH₂
case intro.intro
p : ℕ
G : Type u_2
inst✝³ : Group G
G₂ : Type u_1
inst✝² : Group G₂
p₁ p₂ : ℕ
hp₁ : Fact (Nat.Prime p₁)
hp₂ : Fact (Nat.Prime p₂)
hne : p₁ ≠ p₂
H₁ : Subgroup G
H₂ : Subgroup G₂
inst✝¹ : Fintype { x // x ∈ H₁ }
inst✝ : Fintype { x // x ∈ H₂ }
hH₁ : IsPGroup p₁ { x // x ∈ H₁ }
hH₂ : IsPGroup p₂ { x // x ∈ H₂ }
n₁ n₂ : ℕ
heq₂ : card { x // x ∈ H₂ } = p₂ ^ n₂
⊢ Nat.coprime (p₁ ^ n₁) (p₂ ^ n₂)
case intro.intro
p : ℕ
G : Type u_2
inst✝³ : Group G
G₂ : Type u_1
inst✝² : Group G₂
p₁ p₂ : ℕ
hp₁ : Fact (Nat.Prime p₁)
hp₂ : Fact (Nat.Prime p₂)
hne : p₁ ≠ p₂
H₁ : Subgroup G
H₂ : Subgroup G₂
inst✝¹ : Fintype { x // x ∈ H₁ }
inst✝ : Fintype { x // x ∈ H₂ }
hH₁ : IsPGroup p₁ { x // x ∈ H₁ }
hH₂ : IsPGroup p₂ { x // x ∈ H₂ }
n₁ n₂ : ℕ
heq₂ : card { x // x ∈ H₂ } = p₂ ^ n₂
⊢ Nat.coprime (p₁ ^ n₁) (card { x // x ∈ H₂ })
rw [heq₂]
case intro.intro
p : ℕ
G : Type u_2
inst✝³ : Group G
G₂ : Type u_1
inst✝² : Group G₂
p₁ p₂ : ℕ
hp₁ : Fact (Nat.Prime p₁)
hp₂ : Fact (Nat.Prime p₂)
hne : p₁ ≠ p₂
H₁ : Subgroup G
H₂ : Subgroup G₂
inst✝¹ : Fintype { x // x ∈ H₁ }
inst✝ : Fintype { x // x ∈ H₂ }
hH₁ : IsPGroup p₁ { x // x ∈ H₁ }
hH₂ : IsPGroup p₂ { x // x ∈ H₂ }
n₁ n₂ : ℕ
⊢ Nat.coprime (p₁ ^ n₁) (p₂ ^ n₂)
case intro.intro
p : ℕ
G : Type u_2
inst✝³ : Group G
G₂ : Type u_1
inst✝² : Group G₂
p₁ p₂ : ℕ
hp₁ : Fact (Nat.Prime p₁)
hp₂ : Fact (Nat.Prime p₂)
hne : p₁ ≠ p₂
H₁ : Subgroup G
H₂ : Subgroup G₂
inst✝¹ : Fintype { x // x ∈ H₁ }
inst✝ : Fintype { x // x ∈ H₂ }
hH₁ : IsPGroup p₁ { x // x ∈ H₁ }
hH₂ : IsPGroup p₂ { x // x ∈ H₂ }
n₁ n₂ : ℕ
heq₂ : card { x // x ∈ H₂ } = p₂ ^ n₂
⊢ Nat.coprime (p₁ ^ n₁) (p₂ ^ n₂)
clear heq₂
no goals
case intro.intro
p : ℕ
G : Type u_2
inst✝³ : Group G
G₂ : Type u_1
inst✝² : Group G₂
p₁ p₂ : ℕ
hp₁ : Fact (Nat.Prime p₁)
hp₂ : Fact (Nat.Prime p₂)
hne : p₁ ≠ p₂
H₁ : Subgroup G
H₂ : Subgroup G₂
inst✝¹ : Fintype { x // x ∈ H₁ }
inst✝ : Fintype { x // x ∈ H₂ }
hH₁ : IsPGroup p₁ { x // x ∈ H₁ }
hH₂ : IsPGroup p₂ { x // x ∈ H₂ }
n₁ n₂ : ℕ
⊢ Nat.coprime (p₁ ^ n₁) (p₂ ^ n₂)
exact Nat.coprime_pow_primes _ _ hp₁.elim hp₂.elim hne