no goals
α : Type u
β : Type v
γ : Type w
inst✝⁶ inst✝⁵ : Group α
inst✝⁴ : MulAction α β
x : β
inst✝³ : Fintype α
inst✝² : Fintype β
inst✝¹ : Fintype (Quotient (orbitRel α β))
inst✝ : (b : β) → Fintype { x // x ∈ stabilizer α b }
φ : Quotient (orbitRel α β) → β
hφ : LeftInverse Quotient.mk'' φ
⊢ Fintype.card β = ∑ ω : Quotient (orbitRel α β), Fintype.card α / Fintype.card { x // x ∈ stabilizer α (φ ω) }
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φ)]
α : Type u
β : Type v
γ : Type w
inst✝⁶ inst✝⁵ : Group α
inst✝⁴ : MulAction α β
x : β
inst✝³ : Fintype α
inst✝² : Fintype β
inst✝¹ : Fintype (Quotient (orbitRel α β))
inst✝ : (b : β) → Fintype { x // x ∈ stabilizer α b }
φ : Quotient (orbitRel α β) → β
hφ : LeftInverse Quotient.mk'' φ
this :
  ∀ (ω : Quotient (orbitRel α β)),
    Fintype.card α / Fintype.card { x // x ∈ stabilizer α (φ ω) } = Fintype.card (α ⧸ stabilizer α (φ ω))
⊢ Fintype.card β = ∑ ω : Quotient (orbitRel α β), Fintype.card α / Fintype.card { x // x ∈ stabilizer α (φ ω) }
α : Type u
β : Type v
γ : Type w
inst✝⁶ inst✝⁵ : Group α
inst✝⁴ : MulAction α β
x : β
inst✝³ : Fintype α
inst✝² : Fintype β
inst✝¹ : Fintype (Quotient (orbitRel α β))
inst✝ : (b : β) → Fintype { x // x ∈ stabilizer α b }
φ : Quotient (orbitRel α β) → β
hφ : LeftInverse Quotient.mk'' φ
⊢ Fintype.card β = ∑ ω : Quotient (orbitRel α β), Fintype.card α / Fintype.card { x // x ∈ stabilizer α (φ ω) }
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)
no goals
α : Type u
β : Type v
γ : Type w
inst✝⁶ inst✝⁵ : Group α
inst✝⁴ : MulAction α β
x : β
inst✝³ : Fintype α
inst✝² : Fintype β
inst✝¹ : Fintype (Quotient (orbitRel α β))
inst✝ : (b : β) → Fintype { x // x ∈ stabilizer α b }
φ : Quotient (orbitRel α β) → β
hφ : LeftInverse Quotient.mk'' φ
this :
  ∀ (ω : Quotient (orbitRel α β)),
    Fintype.card α / Fintype.card { x // x ∈ stabilizer α (φ ω) } = Fintype.card (α ⧸ stabilizer α (φ ω))
⊢ Fintype.card β = ∑ ω : Quotient (orbitRel α β), Fintype.card α / Fintype.card { x // x ∈ stabilizer α (φ ω) }
simp_rw [this, ← Fintype.card_sigma,
  Fintype.card_congr (selfEquivSigmaOrbitsQuotientStabilizer' α β hφ)]
α : Type u
β : Type v
γ : Type w
inst✝⁶ inst✝⁵ : Group α
inst✝⁴ : MulAction α β
x : β
inst✝³ : Fintype α
inst✝² : Fintype β
inst✝¹ : Fintype (Quotient (orbitRel α β))
inst✝ : (b : β) → Fintype { x // x ∈ stabilizer α b }
φ : Quotient (orbitRel α β) → β
hφ : LeftInverse Quotient.mk'' φ
ω : Quotient (orbitRel α β)
⊢ Fintype.card α / Fintype.card { x // x ∈ stabilizer α (φ ω) } = Fintype.card (α ⧸ stabilizer α (φ ω))
α : Type u
β : Type v
γ : Type w
inst✝⁶ inst✝⁵ : Group α
inst✝⁴ : MulAction α β
x : β
inst✝³ : Fintype α
inst✝² : Fintype β
inst✝¹ : Fintype (Quotient (orbitRel α β))
inst✝ : (b : β) → Fintype { x // x ∈ stabilizer α b }
φ : Quotient (orbitRel α β) → β
hφ : LeftInverse Quotient.mk'' φ
⊢ ∀ (ω : Quotient (orbitRel α β)),
    Fintype.card α / Fintype.card { x // x ∈ stabilizer α (φ ω) } = Fintype.card (α ⧸ stabilizer α (φ ω))
intro ω
case H
α : Type u
β : Type v
γ : Type w
inst✝⁶ inst✝⁵ : Group α
inst✝⁴ : MulAction α β
x : β
inst✝³ : Fintype α
inst✝² : Fintype β
inst✝¹ : Fintype (Quotient (orbitRel α β))
inst✝ : (b : β) → Fintype { x // x ∈ stabilizer α b }
φ : Quotient (orbitRel α β) → β
hφ : LeftInverse Quotient.mk'' φ
ω : Quotient (orbitRel α β)
⊢ 0 < Fintype.card { x // x ∈ stabilizer α (φ ω) }
α : Type u
β : Type v
γ : Type w
inst✝⁶ inst✝⁵ : Group α
inst✝⁴ : MulAction α β
x : β
inst✝³ : Fintype α
inst✝² : Fintype β
inst✝¹ : Fintype (Quotient (orbitRel α β))
inst✝ : (b : β) → Fintype { x // x ∈ stabilizer α b }
φ : Quotient (orbitRel α β) → β
hφ : LeftInverse Quotient.mk'' φ
ω : Quotient (orbitRel α β)
⊢ Fintype.card α / Fintype.card { x // x ∈ stabilizer α (φ ω) } = Fintype.card (α ⧸ stabilizer α (φ ω))
rw [Fintype.card_congr (@Subgroup.groupEquivQuotientProdSubgroup α _ (stabilizer α <| φ ω)),
  Fintype.card_prod, Nat.mul_div_cancel]
no goals
case H
α : Type u
β : Type v
γ : Type w
inst✝⁶ inst✝⁵ : Group α
inst✝⁴ : MulAction α β
x : β
inst✝³ : Fintype α
inst✝² : Fintype β
inst✝¹ : Fintype (Quotient (orbitRel α β))
inst✝ : (b : β) → Fintype { x // x ∈ stabilizer α b }
φ : Quotient (orbitRel α β) → β
hφ : LeftInverse Quotient.mk'' φ
ω : Quotient (orbitRel α β)
⊢ 0 < Fintype.card { x // x ∈ stabilizer α (φ ω) }
exact Fintype.card_pos_iff.mpr (by infer_instance)
no goals
α : Type u
β : Type v
γ : Type w
inst✝⁶ inst✝⁵ : Group α
inst✝⁴ : MulAction α β
x : β
inst✝³ : Fintype α
inst✝² : Fintype β
inst✝¹ : Fintype (Quotient (orbitRel α β))
inst✝ : (b : β) → Fintype { x // x ∈ stabilizer α b }
φ : Quotient (orbitRel α β) → β
hφ : LeftInverse Quotient.mk'' φ
ω : Quotient (orbitRel α β)
⊢ Nonempty { x // x ∈ stabilizer α (φ ω) }
infer_instance