Theorem: l1_2_25' (AlgebraI/Subgroups.lean)

State before:
G : Type u_1
inst✝ : Group G
⊢ d1224 G ∣ Nat.card G
Tactic:
cases fintypeOrInfinite G
State after:
case inl
G : Type u_1
inst✝ : Group G
val✝ : Fintype G
⊢ d1224 G ∣ Nat.card G

case inr
G : Type u_1
inst✝ : Group G
val✝ : Infinite G
⊢ d1224 G ∣ Nat.card G

State before:
case inl
G : Type u_1
inst✝ : Group G
val✝ : Fintype G
⊢ d1224 G ∣ Nat.card G
Tactic:
rw [Nat.card_eq_fintype_card]
State after:
case inl
G : Type u_1
inst✝ : Group G
val✝ : Fintype G
⊢ d1224 G ∣ Fintype.card G

State before:
case inl
G : Type u_1
inst✝ : Group G
val✝ : Fintype G
⊢ d1224 G ∣ Fintype.card G
Tactic:
exact l1_2_25
State after:
no goals

State before:
case inr
G : Type u_1
inst✝ : Group G
val✝ : Infinite G
⊢ d1224 G ∣ Nat.card G
Tactic:
rw [Nat.card_eq_zero_of_infinite]
State after:
case inr
G : Type u_1
inst✝ : Group G
val✝ : Infinite G
⊢ d1224 G ∣ 0

State before:
case inr
G : Type u_1
inst✝ : Group G
val✝ : Infinite G
⊢ d1224 G ∣ 0
Tactic:
exact dvd_zero _
State after:
no goals