G✝ : Type u
A : Type v
x✝ y : G✝
a b : A
n m : ℕ
inst✝⁵ : Group G✝
inst✝⁴ : AddGroup A
inst✝³ : Fintype G✝
G : Type u_1
inst✝² : Group G
H K : Subgroup G
inst✝¹ : Fintype { x // x ∈ H }
inst✝ : Fintype { x // x ∈ K }
h : coprime (Fintype.card { x // x ∈ H }) (Fintype.card { x // x ∈ K })
x : G
hx : x ∈ H ⊓ K
⊢ x = 1
G✝ : Type u
A : Type v
x y : G✝
a b : A
n m : ℕ
inst✝⁵ : Group G✝
inst✝⁴ : AddGroup A
inst✝³ : Fintype G✝
G : Type u_1
inst✝² : Group G
H K : Subgroup G
inst✝¹ : Fintype { x // x ∈ H }
inst✝ : Fintype { x // x ∈ K }
h : coprime (Fintype.card { x // x ∈ H }) (Fintype.card { x // x ∈ K })
⊢ H ⊓ K = ⊥
refine' (H ⊓ K).eq_bot_iff_forall.mpr fun x hx => _
G✝ : Type u
A : Type v
x✝ y : G✝
a b : A
n m : ℕ
inst✝⁵ : Group G✝
inst✝⁴ : AddGroup A
inst✝³ : Fintype G✝
G : Type u_1
inst✝² : Group G
H K : Subgroup G
inst✝¹ : Fintype { x // x ∈ H }
inst✝ : Fintype { x // x ∈ K }
h : coprime (Fintype.card { x // x ∈ H }) (Fintype.card { x // x ∈ K })
x : G
hx : x ∈ H ⊓ K
⊢ orderOf x ∣ Fintype.card { x // x ∈ H } ∧ orderOf x ∣ Fintype.card { x // x ∈ K }
G✝ : Type u
A : Type v
x✝ y : G✝
a b : A
n m : ℕ
inst✝⁵ : Group G✝
inst✝⁴ : AddGroup A
inst✝³ : Fintype G✝
G : Type u_1
inst✝² : Group G
H K : Subgroup G
inst✝¹ : Fintype { x // x ∈ H }
inst✝ : Fintype { x // x ∈ K }
h : coprime (Fintype.card { x // x ∈ H }) (Fintype.card { x // x ∈ K })
x : G
hx : x ∈ H ⊓ K
⊢ x = 1
rw [← orderOf_eq_one_iff, ← Nat.dvd_one, ← h.gcd_eq_one, Nat.dvd_gcd_iff]