have D₂ : card (H ⊓ K : Subgroup G) ∣ card K := card_dvd_of_le inf_le_right
G : Type u_1
inst✝² : Group G
H K : Subgroup G
inst✝¹ : Fintype ↥H
inst✝ : Fintype ↥K
h : (card ↥H).Coprime (card ↥K)
D₁ : card ↥(H ⊓ K) ∣ card ↥H
⊢ H ⊓ K = ⊥
G : Type u_1
inst✝² : Group G
H K : Subgroup G
inst✝¹ : Fintype ↥H
inst✝ : Fintype ↥K
h : (card ↥H).Coprime (card ↥K)
D₁ : card ↥(H ⊓ K) ∣ card ↥H
D₂ : card ↥(H ⊓ K) ∣ card ↥K
⊢ H ⊓ K = ⊥