Theorem: inf_bot_of_coprime (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 : (card ↥H).Coprime (card ↥K)
⊢ H ⊓ K = ⊥
Tactic:
have D₁ : card (H ⊓ K : Subgroup G) ∣ card H := card_dvd_of_le inf_le_left
State after:
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 = ⊥

State before:
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 = ⊥
Tactic:
have D₂ : card (H ⊓ K : Subgroup G) ∣ card K := card_dvd_of_le inf_le_right
State after:
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 = ⊥

State before:
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 = ⊥
Tactic:
exact eq_bot_iff_card.2 (Nat.eq_one_of_dvd_coprimes h D₁ D₂)
State after:
no goals