-- Mathlib/GroupTheory/GroupAction/Quotient.lean
theorem card_eq_sum_card_group_div_card_stabilizer' [Fintype α] [Fintype β] [Fintype Ω]
    [∀ b : β, Fintype <| stabilizer α b] {φ : Ω → β} (hφ : LeftInverse Quotient.mk'' φ) :
    Fintype.card β = ∑ ω : Ω, Fintype.card α / Fintype.card (stabilizer α (φ ω))

Proof state:
α : Type u
β : Type v
inst✝⁵ : Group α
inst✝⁴ : MulAction α β
inst✝³ : Fintype α
inst✝² : Fintype β
inst✝¹ : Fintype (Quotient (orbitRel α β))
inst✝ : (b : β) → Fintype ↥(stabilizer α b)
φ : Quotient (orbitRel α β) → β
hφ : LeftInverse Quotient.mk'' φ
⊢ Fintype.card β = ∑ ω : Quotient (orbitRel α β), Fintype.card α / Fintype.card ↥(stabilizer α (φ ω))

Tactic:
classical
  have : ∀ ω : Ω, Fintype.card α / Fintype.card (stabilizer α (φ ω)) =
      Fintype.card (α ⧸ stabilizer α (φ ω)) := by
    intro ω
    rw [Fintype.card_congr (@Subgroup.groupEquivQuotientProdSubgroup α _ (stabilizer α <| φ ω)),
      Fintype.card_prod, Nat.mul_div_cancel]
    exact Fintype.card_pos_iff.mpr (by infer_instance)
  simp_rw [this, ← Fintype.card_sigma,
    Fintype.card_congr (selfEquivSigmaOrbitsQuotientStabilizer' α β hφ)]

Result:
no goals

Proof state:
case H
α : Type u
β : Type v
inst✝⁵ : Group α
inst✝⁴ : MulAction α β
inst✝³ : Fintype α
inst✝² : Fintype β
inst✝¹ : Fintype (Quotient (orbitRel α β))
inst✝ : (b : β) → Fintype ↥(stabilizer α b)
φ : Quotient (orbitRel α β) → β
hφ : LeftInverse Quotient.mk'' φ
ω : Quotient (orbitRel α β)
⊢ 0 < Fintype.card ↥(stabilizer α (φ ω))

Tactic:
exact Fintype.card_pos_iff.mpr (by infer_instance)

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝⁵ : Group α
inst✝⁴ : MulAction α β
inst✝³ : Fintype α
inst✝² : Fintype β
inst✝¹ : Fintype (Quotient (orbitRel α β))
inst✝ : (b : β) → Fintype ↥(stabilizer α b)
φ : Quotient (orbitRel α β) → β
hφ : LeftInverse Quotient.mk'' φ
ω : Quotient (orbitRel α β)
⊢ Nonempty ↥(stabilizer α (φ ω))

Tactic:
infer_instance

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝⁵ : Group α
inst✝⁴ : MulAction α β
inst✝³ : Fintype α
inst✝² : Fintype β
inst✝¹ : Fintype (Quotient (orbitRel α β))
inst✝ : (b : β) → Fintype ↥(stabilizer α b)
φ : Quotient (orbitRel α β) → β
hφ : LeftInverse Quotient.mk'' φ
ω : Quotient (orbitRel α β)
⊢ Fintype.card α / Fintype.card ↥(stabilizer α (φ ω)) = Fintype.card (α ⧸ stabilizer α (φ ω))

Tactic:
rw [Fintype.card_congr (@Subgroup.groupEquivQuotientProdSubgroup α _ (stabilizer α <| φ ω)),
  Fintype.card_prod, Nat.mul_div_cancel]

Result:
case H
α : Type u
β : Type v
inst✝⁵ : Group α
inst✝⁴ : MulAction α β
inst✝³ : Fintype α
inst✝² : Fintype β
inst✝¹ : Fintype (Quotient (orbitRel α β))
inst✝ : (b : β) → Fintype ↥(stabilizer α b)
φ : Quotient (orbitRel α β) → β
hφ : LeftInverse Quotient.mk'' φ
ω : Quotient (orbitRel α β)
⊢ 0 < Fintype.card ↥(stabilizer α (φ ω))

Proof state:
α : Type u
β : Type v
inst✝⁵ : Group α
inst✝⁴ : MulAction α β
inst✝³ : Fintype α
inst✝² : Fintype β
inst✝¹ : Fintype (Quotient (orbitRel α β))
inst✝ : (b : β) → Fintype ↥(stabilizer α b)
φ : Quotient (orbitRel α β) → β
hφ : LeftInverse Quotient.mk'' φ
⊢ ∀ (ω : Quotient (orbitRel α β)),
    Fintype.card α / Fintype.card ↥(stabilizer α (φ ω)) = Fintype.card (α ⧸ stabilizer α (φ ω))

Tactic:
intro ω

Result:
α : Type u
β : Type v
inst✝⁵ : Group α
inst✝⁴ : MulAction α β
inst✝³ : Fintype α
inst✝² : Fintype β
inst✝¹ : Fintype (Quotient (orbitRel α β))
inst✝ : (b : β) → Fintype ↥(stabilizer α b)
φ : Quotient (orbitRel α β) → β
hφ : LeftInverse Quotient.mk'' φ
ω : Quotient (orbitRel α β)
⊢ Fintype.card α / Fintype.card ↥(stabilizer α (φ ω)) = Fintype.card (α ⧸ stabilizer α (φ ω))

Proof state:
α : Type u
β : Type v
inst✝⁵ : Group α
inst✝⁴ : MulAction α β
inst✝³ : Fintype α
inst✝² : Fintype β
inst✝¹ : Fintype (Quotient (orbitRel α β))
inst✝ : (b : β) → Fintype ↥(stabilizer α b)
φ : Quotient (orbitRel α β) → β
hφ : LeftInverse Quotient.mk'' φ
⊢ Fintype.card β = ∑ ω : Quotient (orbitRel α β), Fintype.card α / Fintype.card ↥(stabilizer α (φ ω))

Tactic:
have : ∀ ω : Ω, Fintype.card α / Fintype.card (stabilizer α (φ ω)) =
    Fintype.card (α ⧸ stabilizer α (φ ω)) := by
  intro ω
  rw [Fintype.card_congr (@Subgroup.groupEquivQuotientProdSubgroup α _ (stabilizer α <| φ ω)),
    Fintype.card_prod, Nat.mul_div_cancel]
  exact Fintype.card_pos_iff.mpr (by infer_instance)

Result:
α : Type u
β : Type v
inst✝⁵ : Group α
inst✝⁴ : MulAction α β
inst✝³ : Fintype α
inst✝² : Fintype β
inst✝¹ : Fintype (Quotient (orbitRel α β))
inst✝ : (b : β) → Fintype ↥(stabilizer α b)
φ : Quotient (orbitRel α β) → β
hφ : LeftInverse Quotient.mk'' φ
this :
  ∀ (ω : Quotient (orbitRel α β)),
    Fintype.card α / Fintype.card ↥(stabilizer α (φ ω)) = Fintype.card (α ⧸ stabilizer α (φ ω))
⊢ Fintype.card β = ∑ ω : Quotient (orbitRel α β), Fintype.card α / Fintype.card ↥(stabilizer α (φ ω))

Proof state:
α : Type u
β : Type v
inst✝⁵ : Group α
inst✝⁴ : MulAction α β
inst✝³ : Fintype α
inst✝² : Fintype β
inst✝¹ : Fintype (Quotient (orbitRel α β))
inst✝ : (b : β) → Fintype ↥(stabilizer α b)
φ : Quotient (orbitRel α β) → β
hφ : LeftInverse Quotient.mk'' φ
this :
  ∀ (ω : Quotient (orbitRel α β)),
    Fintype.card α / Fintype.card ↥(stabilizer α (φ ω)) = Fintype.card (α ⧸ stabilizer α (φ ω))
⊢ Fintype.card β = ∑ ω : Quotient (orbitRel α β), Fintype.card α / Fintype.card ↥(stabilizer α (φ ω))

Tactic:
simp_rw [this, ← Fintype.card_sigma,
  Fintype.card_congr (selfEquivSigmaOrbitsQuotientStabilizer' α β hφ)]

Result:
no goals