Theorem: d1_2_10' (AlgebraI/Subgroups.lean)

State before:
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
H : Subgroup G
⊢ Nat.card (G ⧸ H) = Nat.card G / Nat.card ↥H
Tactic:
have : Fintype H := by classical infer_instance
State after:
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
H : Subgroup G
this : Fintype ↥H
⊢ Nat.card (G ⧸ H) = Nat.card G / Nat.card ↥H

State before:
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
H : Subgroup G
this : Fintype ↥H
⊢ Nat.card (G ⧸ H) = Nat.card G / Nat.card ↥H
Tactic:
have : 0 < Nat.card H := by
  rw [Nat.card_eq_fintype_card, Fintype.card_pos_iff]
  exact ⟨⟨1, one_mem _⟩⟩
State after:
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
H : Subgroup G
this✝ : Fintype ↥H
this : 0 < Nat.card ↥H
⊢ Nat.card (G ⧸ H) = Nat.card G / Nat.card ↥H

State before:
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
H : Subgroup G
this✝ : Fintype ↥H
this : 0 < Nat.card ↥H
⊢ Nat.card (G ⧸ H) = Nat.card G / Nat.card ↥H
Tactic:
rw [← Subgroup.card_mul_index H, Nat.mul_div_cancel_left _ this, Subgroup.index]
State after:
no goals

State before:
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
H : Subgroup G
⊢ Fintype ↥H
Tactic:
classical infer_instance
State after:
no goals

State before:
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
H : Subgroup G
⊢ Fintype ↥H
Tactic:
infer_instance
State after:
no goals

State before:
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
H : Subgroup G
this : Fintype ↥H
⊢ 0 < Nat.card ↥H
Tactic:
rw [Nat.card_eq_fintype_card, Fintype.card_pos_iff]
State after:
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
H : Subgroup G
this : Fintype ↥H
⊢ Nonempty ↥H

State before:
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
H : Subgroup G
this : Fintype ↥H
⊢ Nonempty ↥H
Tactic:
exact ⟨⟨1, one_mem _⟩⟩
State after:
no goals