Theorem: inf_bot_of_coprime (LeanCourse/MIL/C08_Groups_and_Rings/S01_Groups.lean)

State before:
G : Type u_1
inst✝² : Group G
H K : Subgroup G
inst✝¹ : Fintype (↥H)
inst✝ : Fintype (↥K)
h : Nat.Coprime (card (↥H)) (card (↥K))
⊢ H ⊓ K = ⊥
Tactic:
sorry
State after:
no goals