Theorem: inf_bot_of_coprime (LeanCourse/MIL/C08_Groups_and_Rings/solutions/Solutions_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:
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 : Nat.Coprime (card (↥H)) (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 : Nat.Coprime (card (↥H)) (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 : Nat.Coprime (card (↥H)) (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 : Nat.Coprime (card (↥H)) (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