awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
inst_2 : IsPretransitive G X
B : Set X
a : X
hfB : B.Finite
B' : Set X := ⋂ (k : G), ⋂ (_ : a ∈ k • B), k • B
hfB_ne : B.Nonempty
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : B'.Finite
hag : ∀ (g : G), a ∈ g • B' → B' ≤ g • B'
g : G
hg : a ∈ g • B'
rw : B' ⊆ g • B'
⊢ B' = g • B'

Tactic:
rw [eq_comm, ← mem_stabilizer_iff, mem_stabilizer_set_iff_subset_smul_set hfB']

Premises used: MulAction.mem_stabilizer_set_iff_subset_smul_set, eq_comm, MulAction.mem_stabilizer_iff
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
inst_2 : IsPretransitive G X
B : Set X
a : X
hfB : B.Finite
B' : Set X := ⋂ (k : G), ⋂ (_ : a ∈ k • B), k • B
hfB_ne : B.Nonempty
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : B'.Finite
hag : ∀ (g : G), a ∈ g • B' → B' ≤ g • B'
g : G
hg : a ∈ g • B'
⊢ B' ⊆ g • B'

Tactic:
hag g hg
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
inst_2 : IsPretransitive G X
B : Set X
a : X
hfB : B.Finite
B' : Set X := ⋂ (k : G), ⋂ (_ : a ∈ k • B), k • B
hfB_ne : B.Nonempty
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : B'.Finite
hag : ∀ (g : G), a ∈ g • B' → B' ≤ g • B'
g : G
hg : a ∈ g • B'
⊢ B' ⊆ g • B'

Tactic:
exact hag g hg
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
inst_2 : IsPretransitive G X
B : Set X
a : X
hfB : B.Finite
B' : Set X := ⋂ (k : G), ⋂ (_ : a ∈ k • B), k • B
hfB_ne : B.Nonempty
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : B'.Finite
hag : ∀ (g : G), a ∈ g • B' → B' ≤ g • B'
⊢ ∀ (g : G) (hg : a ∈ g • B'), B' = g • B'

Tactic:
have hag' (g : G) (hg : a ∈ g • B') : B' = g • B' := by
    rw [eq_comm, ← mem_stabilizer_iff, mem_stabilizer_set_iff_subset_smul_set hfB']
    exact hag g hg
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
inst_2 : IsPretransitive G X
B : Set X
a : X
hfB : B.Finite
B' : Set X := ⋂ (k : G), ⋂ (_ : a ∈ k • B), k • B
hfB_ne : B.Nonempty
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : B'.Finite
hag : ∀ (g : G), a ∈ g • B' → B' ≤ g • B'
hag' : ∀ (g : G) (hg : a ∈ g • B'), B' = g • B'
inr :
  ∀ ⦃g : G⦄,
    (HSMul.hSMul (β := Set X) g (⋂ (k : G), ⋂ (_ : a ∈ k • B), k • B) ∩ ⋂ (k : G), ⋂ (_ : a ∈ k • B), k • B).Nonempty →
      HSMul.hSMul (β := Set X) g (⋂ (k : G), ⋂ (_ : a ∈ k • B), k • B) = ⋂ (k : G), ⋂ (_ : a ∈ k • B), k • B
⊢ IsBlock.{u_1, u_2} G (X := X) (⋂ (k : G), ⋂ (_ : a ∈ k • B), k • B)

Tactic:
rw [isBlock_iff_smul_eq_of_nonempty]

Premises used: MulAction.isBlock_iff_smul_eq_of_nonempty
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
inst_2 : IsPretransitive G X
B : Set X
a : X
hfB : B.Finite
B' : Set X := ⋂ (k : G), ⋂ (_ : a ∈ k • B), k • B
hfB_ne : B.Nonempty
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : B'.Finite
hag : ∀ (g : G), a ∈ g • B' → B' ≤ g • B'
hag' : ∀ (g : G) (hg : a ∈ g • B'), B' = g • B'
g : G
b : X
hb' : b ∈ g • B'
hb : b ∈ B'
inr :
  ∀ (k : G) (hk : k • a = b),
    HSMul.hSMul (β := Set X) g (⋂ (k : G), ⋂ (_ : a ∈ k • B), k • B) = ⋂ (k : G), ⋂ (_ : a ∈ k • B), k • B
⊢ HSMul.hSMul (β := Set X) g (⋂ (k : G), ⋂ (_ : a ∈ k • B), k • B) = ⋂ (k : G), ⋂ (_ : a ∈ k • B), k • B

Tactic:
obtain ⟨k : G, hk : k • a = b⟩ := exists_smul_eq G a b

Premises used: MulAction.exists_smul_eq
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
inst_2 : IsPretransitive G X
B : Set X
a : X
hfB : B.Finite
B' : Set X := ⋂ (k : G), ⋂ (_ : a ∈ k • B), k • B
hfB_ne : B.Nonempty
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : B'.Finite
hag : ∀ (g : G), a ∈ g • B' → B' ≤ g • B'
hag' : ∀ (g : G) (hg : a ∈ g • B'), B' = g • B'
g : G
b : X
hb' : b ∈ g • B'
hb : b ∈ B'
k : G
hk : k • a = b
⊢ a ∈ k⁻¹ • B'

Tactic:
⟨b, hb, ?_⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, Set.image
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
inst_2 : IsPretransitive G X
B : Set X
a : X
hfB : B.Finite
B' : Set X := ⋂ (k : G), ⋂ (_ : a ∈ k • B), k • B
hfB_ne : B.Nonempty
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : B'.Finite
hag : ∀ (g : G), a ∈ g • B' → B' ≤ g • B'
hag' : ∀ (g : G) (hg : a ∈ g • B'), B' = g • B'
g : G
b : X
hb' : b ∈ g • B'
hb : b ∈ B'
k : G
hk : k • a = b
refine : (fun (x : X) ↦ k⁻¹ • x) b = a
⊢ a ∈ k⁻¹ • B'

Tactic:
refine ⟨b, hb, ?_⟩
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
inst_2 : IsPretransitive G X
B : Set X
a : X
hfB : B.Finite
B' : Set X := ⋂ (k : G), ⋂ (_ : a ∈ k • B), k • B
hfB_ne : B.Nonempty
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : B'.Finite
hag : ∀ (g : G), a ∈ g • B' → B' ≤ g • B'
hag' : ∀ (g : G) (hg : a ∈ g • B'), B' = g • B'
g : G
b : X
hb' : b ∈ g • B'
hb : b ∈ B'
k : G
hk : k • a = b
⊢ (fun (x : X) ↦ k⁻¹ • x) b = a

Tactic:
simp only [← hk, inv_smul_smul]

Premises used: inv_smul_smul
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
inst_2 : IsPretransitive G X
B : Set X
a : X
hfB : B.Finite
B' : Set X := ⋂ (k : G), ⋂ (_ : a ∈ k • B), k • B
hfB_ne : B.Nonempty
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : B'.Finite
hag : ∀ (g : G), a ∈ g • B' → B' ≤ g • B'
hag' : ∀ (g : G) (hg : a ∈ g • B'), B' = g • B'
g : G
b : X
hb' : b ∈ g • B'
hb : b ∈ B'
k : G
hk : k • a = b
⊢ a ∈ k⁻¹ • B'

Tactic:
have hak : a ∈ k⁻¹ • B' := by
    refine ⟨b, hb, ?_⟩
    simp only [← hk, inv_smul_smul]
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
inst_2 : IsPretransitive G X
B : Set X
a : X
hfB : B.Finite
B' : Set X := ⋂ (k : G), ⋂ (_ : a ∈ k • B), k • B
hfB_ne : B.Nonempty
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : B'.Finite
hag : ∀ (g : G), a ∈ g • B' → B' ≤ g • B'
hag' : ∀ (g : G) (hg : a ∈ g • B'), B' = g • B'
g : G
b : X
hb' : b ∈ g • B'
hb : b ∈ B'
k : G
hk : k • a = b
hak : a ∈ k⁻¹ • B'
rw : b ∈ g • B'
⊢ a ∈ (k⁻¹ * g) • B'

Tactic:
rw [mul_smul, Set.mem_smul_set_iff_inv_smul_mem, inv_inv, hk]

Premises used: inv_inv, Set.mem_smul_set_iff_inv_smul_mem, SemigroupAction.mul_smul
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
inst_2 : IsPretransitive G X
B : Set X
a : X
hfB : B.Finite
B' : Set X := ⋂ (k : G), ⋂ (_ : a ∈ k • B), k • B
hfB_ne : B.Nonempty
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : B'.Finite
hag : ∀ (g : G), a ∈ g • B' → B' ≤ g • B'
hag' : ∀ (g : G) (hg : a ∈ g • B'), B' = g • B'
g : G
b : X
hb' : b ∈ g • B'
hb : b ∈ B'
k : G
hk : k • a = b
hak : a ∈ k⁻¹ • B'
⊢ b ∈ g • B'

Tactic:
hb'

Premises used: Set.Mem
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
inst_2 : IsPretransitive G X
B : Set X
a : X
hfB : B.Finite
B' : Set X := ⋂ (k : G), ⋂ (_ : a ∈ k • B), k • B
hfB_ne : B.Nonempty
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : B'.Finite
hag : ∀ (g : G), a ∈ g • B' → B' ≤ g • B'
hag' : ∀ (g : G) (hg : a ∈ g • B'), B' = g • B'
g : G
b : X
hb' : b ∈ g • B'
hb : b ∈ B'
k : G
hk : k • a = b
hak : a ∈ k⁻¹ • B'
⊢ b ∈ g • B'

Tactic:
exact hb'
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
inst_2 : IsPretransitive G X
B : Set X
a : X
hfB : B.Finite
B' : Set X := ⋂ (k : G), ⋂ (_ : a ∈ k • B), k • B
hfB_ne : B.Nonempty
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : B'.Finite
hag : ∀ (g : G), a ∈ g • B' → B' ≤ g • B'
hag' : ∀ (g : G) (hg : a ∈ g • B'), B' = g • B'
g : G
b : X
hb' : b ∈ g • B'
hb : b ∈ B'
k : G
hk : k • a = b
hak : a ∈ k⁻¹ • B'
⊢ a ∈ (k⁻¹ * g) • B'

Tactic:
have hagk : a ∈ (k⁻¹ * g) • B' := by
    rw [mul_smul, Set.mem_smul_set_iff_inv_smul_mem, inv_inv, hk]
    exact hb'
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
inst_2 : IsPretransitive G X
B : Set X
a : X
hfB : B.Finite
B' : Set X := ⋂ (k : G), ⋂ (_ : a ∈ k • B), k • B
hfB_ne : B.Nonempty
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : B'.Finite
hag : ∀ (g : G), a ∈ g • B' → B' ≤ g • B'
hag' : ∀ (g : G) (hg : a ∈ g • B'), B' = g • B'
g : G
b : X
hb' : b ∈ g • B'
hb : b ∈ B'
k : G
hk : k • a = b
hak : a ∈ k⁻¹ • B'
hagk : a ∈ (k⁻¹ * g) • B'
⊢ B' = k⁻¹ • B'

Tactic:
have hkB' : B' = k⁻¹ • B' := hag' k⁻¹ hak
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
inst_2 : IsPretransitive G X
B : Set X
a : X
hfB : B.Finite
B' : Set X := ⋂ (k : G), ⋂ (_ : a ∈ k • B), k • B
hfB_ne : B.Nonempty
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : B'.Finite
hag : ∀ (g : G), a ∈ g • B' → B' ≤ g • B'
hag' : ∀ (g : G) (hg : a ∈ g • B'), B' = g • B'
g : G
b : X
hb' : b ∈ g • B'
hb : b ∈ B'
k : G
hk : k • a = b
hak : a ∈ k⁻¹ • B'
hagk : a ∈ (k⁻¹ * g) • B'
hkB' : B' = k⁻¹ • B'
⊢ B' = (k⁻¹ * g) • B'

Tactic:
have hgkB' : B' = (k⁻¹ * g) • B' := hag' (k⁻¹ * g) hagk
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
inst_2 : IsPretransitive G X
B : Set X
a : X
hfB : B.Finite
B' : Set X := ⋂ (k : G), ⋂ (_ : a ∈ k • B), k • B
hfB_ne : B.Nonempty
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : B'.Finite
hag : ∀ (g : G), a ∈ g • B' → B' ≤ g • B'
hag' : ∀ (g : G) (hg : a ∈ g • B'), B' = g • B'
g : G
b : X
hb' : b ∈ g • B'
hb : b ∈ B'
k : G
hk : k • a = b
hak : a ∈ k⁻¹ • B'
hagk : a ∈ (k⁻¹ * g) • B'
hkB' : B' = k⁻¹ • B'
hgkB' : B' = (k⁻¹ * g) • B'
⊢ B' = k⁻¹ • g • B'

Tactic:
rw [mul_smul] at hgkB'

Premises used: SemigroupAction.mul_smul
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
inst_2 : IsPretransitive G X
B : Set X
a : X
hfB : B.Finite
B' : Set X := ⋂ (k : G), ⋂ (_ : a ∈ k • B), k • B
hfB_ne : B.Nonempty
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : B'.Finite
hag : ∀ (g : G), a ∈ g • B' → B' ≤ g • B'
hag' : ∀ (g : G) (hg : a ∈ g • B'), B' = g • B'
g : G
b : X
hb' : b ∈ g • B'
hb : b ∈ B'
k : G
hk : k • a = b
hak : a ∈ k⁻¹ • B'
hagk : a ∈ (k⁻¹ * g) • B'
hkB' : B' = k⁻¹ • B'
hgkB' : B' = k⁻¹ • g • B'
⊢ k • B' = B'

Tactic:
rw [← smul_eq_iff_eq_inv_smul] at hkB' hgkB'

Premises used: smul_eq_iff_eq_inv_smul
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
inst_2 : IsPretransitive G X
B : Set X
a : X
hfB : B.Finite
B' : Set X := ⋂ (k : G), ⋂ (_ : a ∈ k • B), k • B
hfB_ne : B.Nonempty
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : B'.Finite
hag : ∀ (g : G), a ∈ g • B' → B' ≤ g • B'
hag' : ∀ (g : G) (hg : a ∈ g • B'), B' = g • B'
g : G
b : X
hb' : b ∈ g • B'
hb : b ∈ B'
k : G
hk : k • a = b
hak : a ∈ k⁻¹ • B'
hagk : a ∈ (k⁻¹ * g) • B'
hkB' : B' = k⁻¹ • B'
hgkB' : B' = k⁻¹ • g • B'
hkB'₁ : k • B' = B'
⊢ k • B' = g • B'

Tactic:
rw [← smul_eq_iff_eq_inv_smul] at hkB' hgkB'

Premises used: smul_eq_iff_eq_inv_smul
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
inst_2 : IsPretransitive G X
B : Set X
a : X
hfB : B.Finite
B' : Set X := ⋂ (k : G), ⋂ (_ : a ∈ k • B), k • B
hfB_ne : B.Nonempty
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : B'.Finite
hag : ∀ (g : G), a ∈ g • B' → B' ≤ g • B'
hag' : ∀ (g : G) (hg : a ∈ g • B'), B' = g • B'
g : G
b : X
hb' : b ∈ g • B'
hb : b ∈ B'
k : G
hk : k • a = b
hak : a ∈ k⁻¹ • B'
hagk : a ∈ (k⁻¹ * g) • B'
hkB' : k • B' = B'
hgkB' : k • B' = g • B'
inr : k • B' = ⋂ (k : G), ⋂ (_ : a ∈ k • B), k • B
inr₁ inr₂ : B' = ⋂ (k : G), ⋂ (_ : a ∈ k • B), k • B
⊢ HSMul.hSMul (β := Set X) g (⋂ (k : G), ⋂ (_ : a ∈ k • B), k • B) = ⋂ (k : G), ⋂ (_ : a ∈ k • B), k • B

Tactic:
rw [← hgkB', hkB']
-- Module: Mathlib.GroupTheory.GroupAction.CardCommute
Goal:
α : Type u_1
β : Type u_2
inst : Group α
inst_1 : MulAction α β
inst_2 : Fintype α
inst_3 : Fintype β
inst_4 : Fintype (Quotient (orbitRel α β))
inst_5 : (b : β) → Fintype ↥(stabilizer α b)
φ : Quotient (orbitRel α β) → β
hφ : LeftInverse Quotient.mk'' φ
ω : Quotient (orbitRel α β)
H : 0 < Fintype.card.{u_1} ↥(stabilizer α (φ ω))
⊢ Fintype.card α / Fintype.card.{u_1} ↥(stabilizer α (φ ω)) =
    Fintype.card.{u_1} (HasQuotient.Quotient α (B := Subgroup α) (stabilizer α (φ ω)))

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

Premises used: Fintype.card_congr, Nat.mul_div_cancel, Subgroup.groupEquivQuotientProdSubgroup, Fintype.card_prod
-- Module: Mathlib.GroupTheory.GroupAction.CardCommute
Goal:
α : Type u_1
β : Type u_2
inst : Group α
inst_1 : MulAction α β
inst_2 : Fintype α
inst_3 : Fintype β
inst_4 : Fintype (Quotient (orbitRel α β))
inst_5 : (b : β) → Fintype ↥(stabilizer α b)
φ : Quotient (orbitRel α β) → β
hφ : LeftInverse Quotient.mk'' φ
ω : Quotient (orbitRel α β)
⊢ Nonempty.{u_1 + 1} ↥(stabilizer α (φ ω))

Tactic:
infer_instance
-- Module: Mathlib.GroupTheory.GroupAction.CardCommute
Goal:
α : Type u_1
β : Type u_2
inst : Group α
inst_1 : MulAction α β
inst_2 : Fintype α
inst_3 : Fintype β
inst_4 : Fintype (Quotient (orbitRel α β))
inst_5 : (b : β) → Fintype ↥(stabilizer α b)
φ : Quotient (orbitRel α β) → β
hφ : LeftInverse Quotient.mk'' φ
ω : Quotient (orbitRel α β)
⊢ 0 < Fintype.card.{u_1} ↥(stabilizer α (φ ω))

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

Premises used: Iff.mpr, Fintype.card_pos_iff
-- Module: Mathlib.GroupTheory.GroupAction.CardCommute
Goal:
α : Type u_1
β : Type u_2
inst : Group α
inst_1 : MulAction α β
inst_2 : Fintype α
inst_3 : Fintype β
inst_4 : Fintype (Quotient (orbitRel α β))
inst_5 : (b : β) → Fintype ↥(stabilizer α b)
φ : Quotient (orbitRel α β) → β
hφ : LeftInverse Quotient.mk'' φ
⊢ ∀ (ω : Quotient (orbitRel α β)),
    Fintype.card α / Fintype.card.{u_1} ↥(stabilizer α (φ ω)) =
      Fintype.card.{u_1} (HasQuotient.Quotient α (B := Subgroup α) (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)
-- Module: Mathlib.GroupTheory.GroupAction.CardCommute
Goal:
α : Type u_1
β : Type u_2
inst : Group α
inst_1 : MulAction α β
inst_2 : Fintype α
inst_3 : Fintype β
inst_4 : Fintype (Quotient (orbitRel α β))
inst_5 : (b : β) → Fintype ↥(stabilizer α b)
φ : Quotient (orbitRel α β) → β
hφ : LeftInverse Quotient.mk'' φ
this :
  ∀ (ω : Quotient (orbitRel α β)),
    Fintype.card α / Fintype.card.{u_1} ↥(stabilizer α (φ ω)) =
      Fintype.card.{u_1} (HasQuotient.Quotient α (B := Subgroup α) (stabilizer α (φ ω)))
simp_rw :
  Fintype.card β =
    ∑ x : Quotient (orbitRel α β), Fintype.card.{u_1} (HasQuotient.Quotient α (B := Subgroup α) (stabilizer α (φ x)))
simp_rw₁ :
  Fintype.card β =
    Fintype.card ((i : Quotient (orbitRel α β)) × HasQuotient.Quotient α (B := Subgroup α) (stabilizer α (φ i)))
⊢ Fintype.card β = ∑ ω : Quotient (orbitRel α β), Fintype.card α / Fintype.card.{u_1} ↥(stabilizer α (φ ω))

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

Premises used: Fintype.card_congr, MulAction.selfEquivSigmaOrbitsQuotientStabilizer', Fintype.card_sigma
-- Module: Mathlib.GroupTheory.GroupAction.CardCommute
Goal:
α : Type u_1
β : Type u_2
inst : Group α
inst_1 : MulAction α β
inst_2 : Fintype α
inst_3 : Fintype β
inst_4 : Fintype (Quotient (orbitRel α β))
inst_5 : (b : β) → Fintype ↥(stabilizer α b)
φ : Quotient (orbitRel α β) → β
hφ : LeftInverse Quotient.mk'' φ
have :
  ∀ (ω : Quotient (orbitRel α β)),
    Fintype.card α / Fintype.card.{u_1} ↥(stabilizer α (φ ω)) =
      Fintype.card.{u_1} (HasQuotient.Quotient α (B := Subgroup α) (stabilizer α (φ ω)))
have₁ :
  ∀
    (this :
      ∀ (ω : Quotient (orbitRel α β)),
        Fintype.card α / Fintype.card.{u_1} ↥(stabilizer α (φ ω)) =
          Fintype.card.{u_1} (HasQuotient.Quotient α (B := Subgroup α) (stabilizer α (φ ω)))),
    Fintype.card β = ∑ ω : Quotient (orbitRel α β), Fintype.card α / Fintype.card.{u_1} ↥(stabilizer α (φ ω))
have₂ :
  ∀ (ω : Quotient (orbitRel α β)),
    Fintype.card α / Fintype.card.{u_1} ↥(stabilizer α (φ ω)) =
      Fintype.card.{u_1} (HasQuotient.Quotient α (B := Subgroup α) (stabilizer α (φ ω)))
have₃ have₄ :
  ∀
    (this :
      ∀ (ω : Quotient (orbitRel α β)),
        Fintype.card α / Fintype.card.{u_1} ↥(stabilizer α (φ ω)) =
          Fintype.card.{u_1} (HasQuotient.Quotient α (B := Subgroup α) (stabilizer α (φ ω)))),
    Fintype.card β = ∑ ω : Quotient (orbitRel α β), Fintype.card α / Fintype.card.{u_1} ↥(stabilizer α (φ ω))
⊢ Fintype.card β = ∑ ω : Quotient (orbitRel α β), Fintype.card α / Fintype.card.{u_1} ↥(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φ)]

Premises used: Fintype.card_sigma
-- Module: Mathlib.GroupTheory.GroupAction.CardCommute
Goal:
α : Type u_1
β : Type u_2
inst : Group α
inst_1 : MulAction α β
inst_2 : Fintype α
inst_3 : Fintype β
inst_4 : Fintype (Quotient (orbitRel α β))
inst_5 : (b : β) → Fintype ↥(stabilizer α b)
⊢ Fintype.card β = ∑ ω : Quotient (orbitRel α β), Fintype.card α / Fintype.card.{u_1} ↥(stabilizer α ω.out)

Tactic:
card_eq_sum_card_group_div_card_stabilizer' α β Quotient.out_eq'

Premises used: Quotient.out_eq', MulAction.card_eq_sum_card_group_div_card_stabilizer'
-- Module: Mathlib.GroupTheory.GroupAction.CardCommute
Goal:
α : Type u_1
β : Type u_2
inst : Mul α
inst_1 : Infinite α
a₁ : α
⊢ ∀ ⦃a₂ : α⦄,
    Eq.{u_1 + 1} (α := { p : α × α // Commute p.1 p.2 })
        ((fun (a : α) ↦ Subtype.mk (p := fun (p : α × α) ↦ Commute p.1 p.2) (a, a) ⋯) a₁)
        ((fun (a : α) ↦ Subtype.mk (p := fun (p : α × α) ↦ Commute p.1 p.2) (a, a) ⋯) a₂) →
      a₁ = a₂

Tactic:
simp
-- Module: Mathlib.GroupTheory.GroupAction.CardCommute
Goal:
G : Type u_3
inst : Group G
inl : ∀ (val : Fintype G), Nat.card.{u_3} { p : G × G // Commute p.1 p.2 } = Nat.card.{u_3} (ConjClasses G) * Nat.card G
inr : Infinite G → Nat.card.{u_3} { p : G × G // Commute p.1 p.2 } = Nat.card.{u_3} (ConjClasses G) * Nat.card G
⊢ Nat.card.{u_3} { p : G × G // Commute p.1 p.2 } = Nat.card.{u_3} (ConjClasses G) * Nat.card G

Tactic:
rcases fintypeOrInfinite G

Premises used: fintypeOrInfinite
-- Module: Mathlib.GroupTheory.GroupAction.CardCommute
Goal:
G : Type u_3
inst : Group G
val : Infinite G
inr : Nat.card.{u_3} { p : G × G // Commute p.1 p.2 } = Nat.card G * Nat.card.{u_3} (ConjClasses G)
inr₁ : 0 = Nat.card G * Nat.card.{u_3} (ConjClasses G)
inr₂ : 0 = 0 * Nat.card.{u_3} (ConjClasses G)
inr₃ inr₄ : Eq (α := ℕ) 0 0
⊢ Nat.card.{u_3} { p : G × G // Commute p.1 p.2 } = Nat.card.{u_3} (ConjClasses G) * Nat.card G

Tactic:
rw [mul_comm, Nat.card_eq_zero_of_infinite, Nat.card_eq_zero_of_infinite, zero_mul]

Premises used: Nat.card_eq_zero_of_infinite, MulZeroClass.zero_mul, mul_comm
-- Module: Mathlib.GroupTheory.GroupAction.CardCommute
Goal:
G : Type u_3
inst : Group G
val : Fintype G
inl : card.{u_3} { p : G × G // Commute p.1 p.2 } = card.{u_3} (ConjClasses G) * card G
⊢ Nat.card.{u_3} { p : G × G // Commute p.1 p.2 } = Nat.card.{u_3} (ConjClasses G) * Nat.card G

Tactic:
simp only [Nat.card_eq_fintype_card]

Premises used: Nat.card_eq_fintype_card
-- Module: Mathlib.GroupTheory.GroupAction.CardCommute
Goal:
G : Type u_3
inst : Group G
val : Fintype G
⊢ card.{u_3} { p : G × G // Commute p.1 p.2 } = card.{u_3} ((a : G) × { b : G // Commute a b })

Tactic:
card_congr (Equiv.subtypeProdEquivSigmaSubtype Commute)

Premises used: Fintype.card_congr, Equiv.subtypeProdEquivSigmaSubtype, Commute
-- Module: Mathlib.GroupTheory.GroupAction.CardCommute
Goal:
G : Type u_3
inst : Group G
val : Fintype G
⊢ card.{u_3} ((a : G) × { b : G // Commute a b }) = ∑ i : G, card.{u_3} { b : G // Commute i b }

Tactic:
card_sigma

Premises used: Fintype.card_sigma
-- Module: Mathlib.GroupTheory.GroupAction.CardCommute
Goal:
G : Type u_3
inst : Group G
val : Fintype G
⊢ Eq (α := ℕ) (∑ i : G, card.{u_3} { b : G // Commute i b })
    (∑ x : ConjAct G, card.{u_3} (↑(MulAction.fixedBy G x) : Type u_3))

Tactic:
sum_equiv ConjAct.toConjAct.toEquiv (fun a ↦ card { b // Commute a b })
              (fun g ↦ card (MulAction.fixedBy G g))
              fun g ↦ card_congr' <| congr_arg _ <| funext fun h ↦ mul_inv_eq_iff_eq_mul.symm.eq

Premises used: MulAction.fixedBy, Commute, ConjAct.toConjAct, Set.Elem, Fintype.card, Subtype, MulEquiv.toEquiv, congr_arg, funext, Fintype.sum_equiv, mul_inv_eq_iff_eq_mul, Iff.eq, Fintype.card_congr', Iff.symm
-- Module: Mathlib.GroupTheory.GroupAction.CardCommute
Goal:
G : Type u_3
inst : Group G
val : Fintype G
⊢ ∑ x : ConjAct G, card.{u_3} (↑(MulAction.fixedBy G x) : Type u_3) =
    card.{u_3} (Quotient (MulAction.orbitRel (ConjAct G) G)) * card.{u_3} (ConjAct G)

Tactic:
MulAction.sum_card_fixedBy_eq_card_orbits_mul_card_group _ _

Premises used: Set.Mem, MulAction.sum_card_fixedBy_eq_card_orbits_mul_card_group
-- Module: Mathlib.GroupTheory.GroupAction.CardCommute
Goal:
G : Type u_3
inst : Group G
val : Fintype G
e_a : card.{u_3} (Quotient (MulAction.orbitRel (ConjAct G) G)) = card.{u_3} (ConjClasses G)
⊢ card.{u_3} (Quotient (MulAction.orbitRel (ConjAct G) G)) * card.{u_3} (ConjAct G) =
    card.{u_3} (ConjClasses G) * card G

Tactic:
congr 1
-- Module: Mathlib.GroupTheory.GroupAction.CardCommute
Goal:
G : Type u_3
inst : Group G
val : Fintype G
e_a : Quotient (MulAction.orbitRel (ConjAct G) G) = ConjClasses G
⊢ card.{u_3} (Quotient (MulAction.orbitRel (ConjAct G) G)) = card.{u_3} (ConjClasses G)

Tactic:
apply card_congr'

Premises used: Fintype.card_congr'
-- Module: Mathlib.GroupTheory.GroupAction.CardCommute
Goal:
G : Type u_3
inst : Group G
val : Fintype G
e_a : MulAction.orbitRel (ConjAct G) G = IsConj.setoid G
⊢ Quotient (MulAction.orbitRel (ConjAct G) G) = ConjClasses G

Tactic:
congr
-- Module: Mathlib.GroupTheory.GroupAction.CardCommute
Goal:
G : Type u_3
inst : Group G
val : Fintype G
e_a : ∀ (a b : G), (MulAction.orbitRel (ConjAct G) G : G → G → Prop) a b ↔ (IsConj.setoid G : G → G → Prop) a b
⊢ MulAction.orbitRel (ConjAct G) G = IsConj.setoid G

Tactic:
ext
-- Module: Mathlib.GroupTheory.GroupAction.CardCommute
Goal:
G : Type u_3
inst : Group G
val : Fintype G
a b : G
⊢ (MulAction.orbitRel (ConjAct G) G : G → G → Prop) a b ↔ (IsConj.setoid G : G → G → Prop) a b

Tactic:
(Setoid.comm' _).trans isConj_iff.symm

Premises used: isConj_iff, Iff.trans, Setoid.comm', Iff.symm
-- Module: Mathlib.GroupTheory.GroupAction.CardCommute
Goal:
G : Type u_3
inst : Group G
val : Fintype G
a b : G
⊢ (MulAction.orbitRel (ConjAct G) G : G → G → Prop) a b ↔ (IsConj.setoid G : G → G → Prop) a b

Tactic:
exact (Setoid.comm' _).trans isConj_iff.symm

Premises used: Iff.trans, Setoid.comm'