awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup (goal)
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
hs : IsPretransitive.{u_1, u_2} ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
g : M
a : α
ha : a ∈ sᶜ ∩ (g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx_1 :
  Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M (s ∩ g • s))) α) (ofFixingSubgroup M (s ∩ g • s)) x
hx : x ∉ g • s
hg'x : Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) (g⁻¹ • x)
hg'a : Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) (g⁻¹ • a)
k : M
hk : Membership.mem (γ := Subgroup M) (fixingSubgroup M s) k
hkax_1 :
  Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (fixingSubgroup M s) x) k hk •
      Subtype.mk (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) (g⁻¹ • a)
        hg'a =
    Subtype.mk (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) (g⁻¹ • x) hg'x
hkax :
  (↑(Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (fixingSubgroup M s) x) k hk •
          Subtype.mk (p := fun (x : α) ↦
            Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) (g⁻¹ • a)
            hg'a) :
      α) =
    g⁻¹ • x
⊢ (↑(HSMul.hSMul (α := ↥(fixingSubgroup M (s ∩ g • s)))
          (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (fixingSubgroup M (s ∩ g • s)) x)
            (g * k * g⁻¹) ⋯)
          (Subtype.mk (p := fun (x : α) ↦
            Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M (s ∩ g • s))) α)
              (ofFixingSubgroup M (s ∩ g • s)) x)
            a ha')) :
      α) =
    x
have h : ∀
  (hkax :
    Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (fixingSubgroup M s) x) k hk •
        (↑(Subtype.mk (p := fun (x : α) ↦
              Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x)
              (g⁻¹ • a) hg'a) :
          α) =
      g⁻¹ • x),
  (↑(HSMul.hSMul (α := ↥(fixingSubgroup M (s ∩ g • s)))
          (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (fixingSubgroup M (s ∩ g • s)) x)
            (g * k * g⁻¹) sorry)
          (Subtype.mk (p := fun (x : α) ↦
            Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M (s ∩ g • s))) α)
              (ofFixingSubgroup M (s ∩ g • s)) x)
            a ha')) :
      α) =
    x
Tactic: rwa [SetLike.val_smul, Subgroup.mk_smul, eq_inv_smul_iff, smul_smul, smul_smul] at hkax
Cleared hypotheses: hkax
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup (goal)
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
hs : IsPretransitive.{u_1, u_2} ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
g : M
a : α
ha : a ∈ sᶜ ∩ (g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx_1 :
  Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M (s ∩ g • s))) α) (ofFixingSubgroup M (s ∩ g • s)) x
hx : x ∉ g • s
hg'x : Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) (g⁻¹ • x)
hg'a : Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) (g⁻¹ • a)
k : M
hk : Membership.mem (γ := Subgroup M) (fixingSubgroup M s) k
hkax :
  Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (fixingSubgroup M s) x) k hk •
      Subtype.mk (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) (g⁻¹ • a)
        hg'a =
    Subtype.mk (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) (g⁻¹ • x) hg'x
⊢ Membership.mem (γ := Subgroup M) (fixingSubgroup M (s ∩ g • s)) (g * k * g⁻¹)
have w : ∀ (hk_1 : ∀ y ∈ s, k • y = y)
  (hkax :
    Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (fixingSubgroup M s) x) k hk •
        Subtype.mk (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) (g⁻¹ • a)
          hg'a =
      Subtype.mk (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) (g⁻¹ • x)
        hg'x),
  ∀ y ∈ s ∩ g • s, (g * k * g⁻¹) • y = y
Tactic: rw [mem_fixingSubgroup_iff] at hk ⊢
Cleared hypotheses: hkax
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup (goal)
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
hs : IsPretransitive.{u_1, u_2} ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
g : M
a : α
ha : a ∈ sᶜ ∩ (g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx_1 :
  Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M (s ∩ g • s))) α) (ofFixingSubgroup M (s ∩ g • s)) x
hx : x ∉ g • s
hg'x : Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) (g⁻¹ • x)
hg'a : Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) (g⁻¹ • a)
k : M
hk_1 : Membership.mem (γ := Subgroup M) (fixingSubgroup M s) k
hk : ∀ y ∈ s, k • y = y
hkax :
  Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (fixingSubgroup M s) x) k hk_1 •
      Subtype.mk (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) (g⁻¹ • a)
        hg'a =
    Subtype.mk (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) (g⁻¹ • x) hg'x
y : α
hy : y ∈ s ∩ g • s
⊢ (g * k * g⁻¹) • y = y
have w : k • g⁻¹ • y = g⁻¹ • y
Tactic: rw [mul_smul, mul_smul, smul_eq_iff_eq_inv_smul g]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup (hypothesis)
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
inst_2 : Finite α
hs : IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
g : M
ha : s ∪ g • s ≠ ⊤
⊢ IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup M (s ∩ g • s)) ↥(ofFixingSubgroup M (s ∩ g • s))
have this : IsPretransitive.{u_1, u_2} ↥(fixingSubgroup M (s ∩ g • s)) ↥(ofFixingSubgroup M (s ∩ g • s))
Tactic: have := IsPretransitive.isPretransitive_ofFixingSubgroup_inter hs.toIsPretransitive ha
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup (goal)
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
inst_2 : Finite α
hs : IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
g : M
ha : s ∪ g • s ≠ ⊤
this : IsPretransitive.{u_1, u_2} ↥(fixingSubgroup M (s ∩ g • s)) ↥(ofFixingSubgroup M (s ∩ g • s))
⊢ IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup M (s ∩ g • s)) ↥(ofFixingSubgroup M (s ∩ g • s))
have apply : Nat.card.{u_2} ↥(ofFixingSubgroup M (s ∩ g • s)) <
  2 *
    Set.ncard.{u_2} (α := ↥(ofFixingSubgroup M (s ∩ g • s)))
      (Set.range (ι := ↥(ofFixingSubgroup M s))
        (⇑(ofFixingSubgroup_of_inclusion M (s := s) (t := s ∩ g • s) sorry :
              MulActionHom (M := ↥(fixingSubgroup M s)) (N := ↥(fixingSubgroup M (s ∩ g • s)))
                (⇑(Subgroup.inclusion sorry) : (a : ↥(fixingSubgroup M s)) → ↥(fixingSubgroup M (s ∩ g • s)))
                ↥(ofFixingSubgroup M s) ↥(ofFixingSubgroup M (s ∩ g • s))) :
          (a : ↥(ofFixingSubgroup M s)) → ↥(ofFixingSubgroup M (s ∩ g • s))))
Tactic: apply IsPreprimitive.of_card_lt (f := ofFixingSubgroup_of_inclusion M Set.inter_subset_left)
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup (goal)
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
inst_2 : Finite α
hs : IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
g : M
ha : s ∪ g • s ≠ ⊤
this : IsPretransitive.{u_1, u_2} ↥(fixingSubgroup M (s ∩ g • s)) ↥(ofFixingSubgroup M (s ∩ g • s))
⊢ Nat.card.{u_2} ↥(ofFixingSubgroup M (s ∩ g • s)) <
    2 *
      Set.ncard.{u_2} (α := ↥(ofFixingSubgroup M (s ∩ g • s)))
        (Set.range (ι := ↥(ofFixingSubgroup M s))
          (⇑(ofFixingSubgroup_of_inclusion M (s := s) (t := s ∩ g • s) ⋯ :
                MulActionHom (M := ↥(fixingSubgroup M s)) (N := ↥(fixingSubgroup M (s ∩ g • s)))
                  (⇑(Subgroup.inclusion ⋯) : (a : ↥(fixingSubgroup M s)) → ↥(fixingSubgroup M (s ∩ g • s)))
                  ↥(ofFixingSubgroup M s) ↥(ofFixingSubgroup M (s ∩ g • s))) :
            (a : ↥(ofFixingSubgroup M s)) → ↥(ofFixingSubgroup M (s ∩ g • s))))
have rw : (sᶜ ∪ (g • s)ᶜ).ncard < 2 * sᶜ.ncard
Tactic: rw [show Nat.card (ofFixingSubgroup M (s ∩ g • s)) = (s ∩ g • s)ᶜ.ncard from
    Nat.card_coe_set_eq _, Set.ncard_range_of_injective ofFixingSubgroup_of_inclusion_injective,
    show Nat.card (ofFixingSubgroup M s) = sᶜ.ncard from Nat.card_coe_set_eq _, Set.compl_inter]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup (goal)
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
inst_2 : Finite α
hs : IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
g : M
ha : s ∪ g • s ≠ ⊤
this : IsPretransitive.{u_1, u_2} ↥(fixingSubgroup M (s ∩ g • s)) ↥(ofFixingSubgroup M (s ∩ g • s))
⊢ (sᶜ ∪ (g • s)ᶜ).ncard < 2 * sᶜ.ncard
have refine_1 : ¬Disjoint sᶜ (g • s)ᶜ
Tactic: refine (Set.ncard_union_lt sᶜ.toFinite (g • s)ᶜ.toFinite ?_).trans_le ?_
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup (goal)
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
inst_2 : Finite α
hs : IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
g : M
ha : s ∪ g • s ≠ ⊤
this : IsPretransitive.{u_1, u_2} ↥(fixingSubgroup M (s ∩ g • s)) ↥(ofFixingSubgroup M (s ∩ g • s))
refine_1 : ¬Disjoint sᶜ (g • s)ᶜ
⊢ (sᶜ ∪ (g • s)ᶜ).ncard < 2 * sᶜ.ncard
have refine_2 : sᶜ.ncard + (g • s)ᶜ.ncard ≤ 2 * sᶜ.ncard
Tactic: refine (Set.ncard_union_lt sᶜ.toFinite (g • s)ᶜ.toFinite ?_).trans_le ?_
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup (goal)
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
inst_2 : Finite α
hs : IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
g : M
ha : s ∪ g • s ≠ ⊤
this : IsPretransitive.{u_1, u_2} ↥(fixingSubgroup M (s ∩ g • s)) ↥(ofFixingSubgroup M (s ∩ g • s))
⊢ ¬Disjoint sᶜ (g • s)ᶜ
have refine_1 : ¬sᶜ ⊆ g • s
Tactic: rwa [Set.disjoint_compl_right_iff_subset, Set.compl_subset_iff_union]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup (goal)
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
inst_2 : Finite α
hs : IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
g : M
ha : s ∪ g • s ≠ ⊤
this : IsPretransitive.{u_1, u_2} ↥(fixingSubgroup M (s ∩ g • s)) ↥(ofFixingSubgroup M (s ∩ g • s))
refine_1 : ¬sᶜ ⊆ g • s
⊢ ¬Disjoint sᶜ (g • s)ᶜ
have refine_1₁ : ¬s ∪ g • s = Set.univ
Tactic: rwa [Set.disjoint_compl_right_iff_subset, Set.compl_subset_iff_union]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup (goal)
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
inst_2 : Finite α
hs : IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
g : M
ha : s ∪ g • s ≠ ⊤
this : IsPretransitive.{u_1, u_2} ↥(fixingSubgroup M (s ∩ g • s)) ↥(ofFixingSubgroup M (s ∩ g • s))
⊢ sᶜ.ncard + (g • s)ᶜ.ncard ≤ 2 * sᶜ.ncard
have refine_2 : sᶜ.ncard + (g • sᶜ).ncard ≤ 2 * sᶜ.ncard
Tactic: rw [← Set.smul_set_compl, Set.ncard_smul_set, two_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup (goal)
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
inst_2 : Finite α
hs : IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
g : M
ha : s ∪ g • s ≠ ⊤
this : IsPretransitive.{u_1, u_2} ↥(fixingSubgroup M (s ∩ g • s)) ↥(ofFixingSubgroup M (s ∩ g • s))
refine_2 : sᶜ.ncard + (g • sᶜ).ncard ≤ 2 * sᶜ.ncard
⊢ sᶜ.ncard + (g • s)ᶜ.ncard ≤ 2 * sᶜ.ncard
have refine_2₁ : sᶜ.ncard + sᶜ.ncard ≤ 2 * sᶜ.ncard
Tactic: rw [← Set.smul_set_compl, Set.ncard_smul_set, two_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup (goal)
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
inst_2 : Finite α
hs : IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
g : M
ha : s ∪ g • s ≠ ⊤
this : IsPretransitive.{u_1, u_2} ↥(fixingSubgroup M (s ∩ g • s)) ↥(ofFixingSubgroup M (s ∩ g • s))
refine_2 : sᶜ.ncard + (g • sᶜ).ncard ≤ 2 * sᶜ.ncard
refine_2₁ : sᶜ.ncard + sᶜ.ncard ≤ 2 * sᶜ.ncard
⊢ sᶜ.ncard + (g • s)ᶜ.ncard ≤ 2 * sᶜ.ncard
have refine_2₂ : sᶜ.ncard + sᶜ.ncard ≤ sᶜ.ncard + sᶜ.ncard
Tactic: rw [← Set.smul_set_compl, Set.ncard_smul_set, two_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup (goal)
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
s : Set α
k : G
hk : Membership.mem (γ := Subgroup G) (fixingSubgroup G s) k
| s
have rw : id '' s
Tactic: rw [← Set.image_id s]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup (goal)
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
s : Set α
k : G
hk : Membership.mem (γ := Subgroup G) (fixingSubgroup G s) k
⊢ k • s = s
have conv_rhs : k • s = id '' s
Tactic: conv_rhs => rw [← Set.image_id s]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup (goal)
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
s : Set α
k : G
hk : Membership.mem (γ := Subgroup G) (fixingSubgroup G s) k
⊢ k • s = id '' s
have h : ∀ a ∈ s, k • a = id a
Tactic: apply Set.image_congr
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer (goal)
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
a : α
g : ↥(stabilizer G a)
x : α
⊢ ¬x = a → ¬g • x = a
have rw : x = g⁻¹ • a → x = a
Tactic: rw [not_imp_not, smul_eq_iff_eq_inv_smul]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer (goal)
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
a : α
g : ↥(stabilizer G a)
x : α
hgx : x = g⁻¹ • a
⊢ x = a
have a₁ : a = x
Tactic: apply symm
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer (goal)
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
a : α
g : ↥(stabilizer G a)
x : α
hgx : x = g⁻¹ • a
⊢ a = x
have a₁ : g • a = a
Tactic: rw [hgx, ← smul_eq_iff_eq_inv_smul]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer (goal)
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
a : α
⊢ HAdd.hAdd (α := ℕ∞) (β := ℕ∞) ((Cardinal.toENat : (a : Cardinal.{u_2}) → ℕ∞) (Cardinal.mk ↥(ofStabilizer G a)) : ℕ∞)
      (1 : ℕ∞) =
    (Cardinal.toENat : (a : Cardinal.{u_2}) → ℕ∞) (Cardinal.mk α)
have rw : HAdd.hAdd (α := ℕ∞) (β := ℕ∞) ((Cardinal.toENat : (a : Cardinal.{u_2}) → ℕ∞) (Cardinal.mk (↑{a} : Type u_2)) : ℕ∞)
    ((Cardinal.toENat : (a : Cardinal.{u_2}) → ℕ∞) (Cardinal.mk (↑{a}ᶜ : Type u_2)) : ℕ∞) =
  HAdd.hAdd (α := ℕ∞) (β := ℕ∞) (1 : ℕ∞)
    ((Cardinal.toENat : (a : Cardinal.{u_2}) → ℕ∞) (Cardinal.mk ↥(ofStabilizer G a)) : ℕ∞)
Tactic: rw [← Cardinal.mk_sum_compl {a}, map_add, add_comm, eq_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer (goal)
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
a : α
⊢ HAdd.hAdd (α := ℕ∞) (β := ℕ∞) ((Cardinal.toENat : (a : Cardinal.{u_2}) → ℕ∞) (Cardinal.mk (↑{a} : Type u_2)) : ℕ∞)
      ((Cardinal.toENat : (a : Cardinal.{u_2}) → ℕ∞) (Cardinal.mk (↑{a}ᶜ : Type u_2)) : ℕ∞) =
    HAdd.hAdd (α := ℕ∞) (β := ℕ∞) (1 : ℕ∞)
      ((Cardinal.toENat : (a : Cardinal.{u_2}) → ℕ∞) (Cardinal.mk ↥(ofStabilizer G a)) : ℕ∞)
have e_a : Eq (α := ℕ∞) ((Cardinal.toENat : (a : Cardinal.{u_2}) → ℕ∞) (Cardinal.mk (↑{a} : Type u_2)) : ℕ∞) (1 : ℕ∞)
Tactic: congr
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer (goal)
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
inst_2 : Finite α
a : α
this : Fintype α := Fintype.ofFinite α
⊢ Nat.card.{u_2} ↥(ofStabilizer G a) + 1 = Nat.card α
have rw : ∀ (x : α),
  Membership.mem (γ := Finset α) {a}ᶜ x ↔
    Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x
Tactic: rw [Nat.subtype_card {a}ᶜ, ← Finset.card_singleton a, Finset.card_compl_add_card,
    Nat.card_eq_fintype_card]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer (goal)
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
inst_2 : Finite α
a : α
let let₁ let₂ : Nat.card.{u_2} ↥(ofStabilizer G a) + 1 = Nat.card α
⊢ Nat.card.{u_2} ↥(ofStabilizer G a) + 1 = Nat.card α
have let₃ : let this := Fintype.ofFinite α;
∀ (x : α),
  Membership.mem (γ := Finset α) {a}ᶜ x ↔
    Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x
Tactic: classical
  let := Fintype.ofFinite α
  rw [Nat.subtype_card {a}ᶜ, ← Finset.card_singleton a, Finset.card_compl_add_card,
    Nat.card_eq_fintype_card]
  simp [mem_ofStabilizer_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer (goal)
Goal:
G : Type u_3
inst : AddGroup G
α : Type u_4
inst_1 : AddAction G α
g h k : G
a b c : α
hg : b = g +ᵥ a
hh : c = h +ᵥ b
hk : c = k +ᵥ a
H : k = h + g
⊢ Eq (α := ↥(AddAction.stabilizer G a) → ↥(AddAction.stabilizer G c))
    (Function.comp (β := ↥(AddAction.stabilizer G b))
      (⇑(AddAction.stabilizerEquivStabilizer hh) : (a : ↥(AddAction.stabilizer G b)) → ↥(AddAction.stabilizer G c))
      (⇑(AddAction.stabilizerEquivStabilizer hg) : (a : ↥(AddAction.stabilizer G a)) → ↥(AddAction.stabilizer G b)))
    (⇑(AddAction.stabilizerEquivStabilizer hk) : (a : ↥(AddAction.stabilizer G a)) → ↥(AddAction.stabilizer G c))
have h₁ : ∀ (x : ↥(AddAction.stabilizer G a)),
  Eq (α := G)
    (↑(Function.comp (β := ↥(AddAction.stabilizer G b))
          (⇑(AddAction.stabilizerEquivStabilizer hh) : (a : ↥(AddAction.stabilizer G b)) → ↥(AddAction.stabilizer G c))
          (⇑(AddAction.stabilizerEquivStabilizer hg) : (a : ↥(AddAction.stabilizer G a)) → ↥(AddAction.stabilizer G b))
          x) :
      G)
    (↑((AddAction.stabilizerEquivStabilizer hk : (a : ↥(AddAction.stabilizer G a)) → ↥(AddAction.stabilizer G c)) x) :
      G)
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer (goal)
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
g h k : G
a b c : α
hg : b = g • a
hh : c = h • b
hk : c = k • a
H : k = h * g
⊢ Eq (α := ↥(stabilizer G a) → ↥(stabilizer G c))
    (Function.comp (β := ↥(stabilizer G b))
      (⇑(stabilizerEquivStabilizer hh) : (a : ↥(stabilizer G b)) → ↥(stabilizer G c))
      (⇑(stabilizerEquivStabilizer hg) : (a : ↥(stabilizer G a)) → ↥(stabilizer G b)))
    (⇑(stabilizerEquivStabilizer hk) : (a : ↥(stabilizer G a)) → ↥(stabilizer G c))
have h₁ : ∀ (x : ↥(stabilizer G a)),
  Eq (α := G)
    (↑(Function.comp (β := ↥(stabilizer G b))
          (⇑(stabilizerEquivStabilizer hh) : (a : ↥(stabilizer G b)) → ↥(stabilizer G c))
          (⇑(stabilizerEquivStabilizer hg) : (a : ↥(stabilizer G a)) → ↥(stabilizer G b)) x) :
      G)
    (↑((stabilizerEquivStabilizer hk : (a : ↥(stabilizer G a)) → ↥(stabilizer G c)) x) : G)
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer (goal)
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
g h k : G
a b c : α
hg : b = g • a
hh : c = h • b
hk : c = k • a
H : k = h * g
⊢ (conjMap hh).comp (conjMap hg) = conjMap hk
have a₁ : ∀ (x : ↥(ofStabilizer G a)),
  Eq.{u_2 + 1} (α := α) (↑(((conjMap hh).comp (conjMap hg) : (a : ↥(ofStabilizer G a)) → ↥(ofStabilizer G c)) x) : α)
    (↑((conjMap hk : (a : ↥(ofStabilizer G a)) → ↥(ofStabilizer G c)) x) : α)
Tactic: ext x
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer (goal)
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
g : G
a b : α
hg : b = g • a
⊢ Function.Bijective (α := ↥(ofStabilizer G a)) (β := ↥(ofStabilizer G b))
    (⇑(conjMap hg) : (a : ↥(ofStabilizer G a)) → ↥(ofStabilizer G b))
have left : Function.Injective (α := ↥(ofStabilizer G a)) (β := ↥(ofStabilizer G b))
  (⇑(conjMap hg) : (a : ↥(ofStabilizer G a)) → ↥(ofStabilizer G b))
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer (goal)
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
g : G
a b : α
hg : b = g • a
left :
  Function.Injective (α := ↥(ofStabilizer G a)) (β := ↥(ofStabilizer G b))
    (⇑(conjMap hg) : (a : ↥(ofStabilizer G a)) → ↥(ofStabilizer G b))
⊢ Function.Bijective (α := ↥(ofStabilizer G a)) (β := ↥(ofStabilizer G b))
    (⇑(conjMap hg) : (a : ↥(ofStabilizer G a)) → ↥(ofStabilizer G b))
have right : Function.Surjective (α := ↥(ofStabilizer G a)) (β := ↥(ofStabilizer G b))
  (⇑(conjMap hg) : (a : ↥(ofStabilizer G a)) → ↥(ofStabilizer G b))
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer (goal)
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
g : G
a b : α
hg : b = g • a
x : α
hx : Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x
y : α
hy : Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) y
hxy :
  Eq (α := ↥(ofStabilizer G b))
    ((conjMap hg : (a : ↥(ofStabilizer G a)) → ↥(ofStabilizer G b))
        (Subtype.mk (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) x hx) :
      ↥(ofStabilizer G b))
    ((conjMap hg : (a : ↥(ofStabilizer G a)) → ↥(ofStabilizer G b))
        (Subtype.mk (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) y hy) :
      ↥(ofStabilizer G b))
⊢ Subtype.mk (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) x hx =
    Subtype.mk (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) y hy
have left : x = y
Tactic: simp only [Subtype.mk_eq_mk]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer (goal)
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
g : G
a b : α
hg : b = g • a
x : α
hx : Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x
y : α
hy : Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) y
hxy :
  Eq (α := ↥(ofStabilizer G b))
    ((conjMap hg : (a : ↥(ofStabilizer G a)) → ↥(ofStabilizer G b))
        (Subtype.mk (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) x hx) :
      ↥(ofStabilizer G b))
    ((conjMap hg : (a : ↥(ofStabilizer G a)) → ↥(ofStabilizer G b))
        (Subtype.mk (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) y hy) :
      ↥(ofStabilizer G b))
⊢ x = y
have left : Eq.{u_2 + 1} (α := α) ((fun (x : α) ↦ g • x) x) ((fun (x : α) ↦ g • x) y)
Tactic: apply (MulAction.injective g)