awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s t : Set α
a : α
ha : Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) a
ha' :
  Membership.mem (γ :=
    SubMulAction.{u_1, u_2}
      ↥(fixingSubgroup ↥(fixingSubgroup M s) (α := ↥(ofFixingSubgroup M s))
          (Subtype.val (p := fun (x : α) ↦
              Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) ⁻¹'
            t))
      ↥(ofFixingSubgroup M s))
    (ofFixingSubgroup (↥(fixingSubgroup M s))
      (Subtype.val (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) ⁻¹'
        t))
    (Subtype.mk (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) a ha)
hy : a ∈ s ∪ t
right : ∀ (h : a ∈ s), False
right₁ : ∀ (h : a ∈ t), False
⊢ False

Tactic:
rcases (Set.mem_union a s t).mp hy with h | h

Premises used: Set.mem_union, Iff.mp
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s t : Set α
a : α
ha : Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) a
ha' :
  Membership.mem (γ :=
    SubMulAction.{u_1, u_2}
      ↥(fixingSubgroup ↥(fixingSubgroup M s) (α := ↥(ofFixingSubgroup M s))
          (Subtype.val (p := fun (x : α) ↦
              Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) ⁻¹'
            t))
      ↥(ofFixingSubgroup M s))
    (ofFixingSubgroup (↥(fixingSubgroup M s))
      (Subtype.val (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) ⁻¹'
        t))
    (Subtype.mk (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) a ha)
hy : a ∈ s ∪ t
h : a ∈ s
⊢ False

Tactic:
ha h
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s t : Set α
a : α
ha : Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) a
ha' :
  Membership.mem (γ :=
    SubMulAction.{u_1, u_2}
      ↥(fixingSubgroup ↥(fixingSubgroup M s) (α := ↥(ofFixingSubgroup M s))
          (Subtype.val (p := fun (x : α) ↦
              Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) ⁻¹'
            t))
      ↥(ofFixingSubgroup M s))
    (ofFixingSubgroup (↥(fixingSubgroup M s))
      (Subtype.val (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) ⁻¹'
        t))
    (Subtype.mk (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) a ha)
hy : a ∈ s ∪ t
h : a ∈ s
⊢ False

Tactic:
exact ha h
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s t : Set α
a : α
ha : Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) a
ha' :
  Membership.mem (γ :=
    SubMulAction.{u_1, u_2}
      ↥(fixingSubgroup ↥(fixingSubgroup M s) (α := ↥(ofFixingSubgroup M s))
          (Subtype.val (p := fun (x : α) ↦
              Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) ⁻¹'
            t))
      ↥(ofFixingSubgroup M s))
    (ofFixingSubgroup (↥(fixingSubgroup M s))
      (Subtype.val (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) ⁻¹'
        t))
    (Subtype.mk (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) a ha)
hy : a ∈ s ∪ t
h : a ∈ t
right :
  Membership.mem (γ := Set ↥(ofFixingSubgroup M s))
    (Subtype.val (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) ⁻¹'
      t)
    (Subtype.mk (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) a ha)
⊢ False

Tactic:
apply ha'
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s t : Set α
a : α
ha : Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) a
ha' :
  Membership.mem (γ :=
    SubMulAction.{u_1, u_2}
      ↥(fixingSubgroup ↥(fixingSubgroup M s) (α := ↥(ofFixingSubgroup M s))
          (Subtype.val (p := fun (x : α) ↦
              Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) ⁻¹'
            t))
      ↥(ofFixingSubgroup M s))
    (ofFixingSubgroup (↥(fixingSubgroup M s))
      (Subtype.val (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) ⁻¹'
        t))
    (Subtype.mk (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) a ha)
hy : a ∈ s ∪ t
h : a ∈ t
⊢ Membership.mem (γ := Set ↥(ofFixingSubgroup M s))
    (Subtype.val (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) ⁻¹'
      t)
    (Subtype.mk (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) a ha)

Tactic:
simpa only [Set.mem_preimage]

Premises used: Set.mem_preimage
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s t : Set α
hst : t ⊆ s
x : α
hx : Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x
y : α
hy : Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) y
hxy :
  Eq (α := ↥(ofFixingSubgroup M t))
    ((ofFixingSubgroup_of_inclusion M (s := s) (t := t) hst : (a : ↥(ofFixingSubgroup M s)) → ↥(ofFixingSubgroup M t))
        (Subtype.mk (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) x hx) :
      ↥(ofFixingSubgroup M t))
    ((ofFixingSubgroup_of_inclusion M (s := s) (t := t) hst : (a : ↥(ofFixingSubgroup M s)) → ↥(ofFixingSubgroup M t))
        (Subtype.mk (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) y hy) :
      ↥(ofFixingSubgroup M t))
rw :
  ∀
    (hxy :
      Eq.{u_2 + 1} (α := α)
        (↑((ofFixingSubgroup_of_inclusion M (s := s) (t := t) hst :
                (a : ↥(ofFixingSubgroup M s)) → ↥(ofFixingSubgroup M t))
              (Subtype.mk (p := fun (x : α) ↦
                Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) x
                hx)) :
          α)
        (↑((ofFixingSubgroup_of_inclusion M (s := s) (t := t) hst :
                (a : ↥(ofFixingSubgroup M s)) → ↥(ofFixingSubgroup M t))
              (Subtype.mk (p := fun (x : α) ↦
                Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) y
                hy)) :
          α)),
    (↑(Subtype.mk (p := fun (x : α) ↦
            Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) x hx) :
        α) =
      (↑(Subtype.mk (p := fun (x : α) ↦
            Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) y hy) :
        α)
⊢ Subtype.mk (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) x hx =
    Subtype.mk (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) y hy

Tactic:
rw [← SetLike.coe_eq_coe] at hxy ⊢

Premises used: SetLike.coe_eq_coe
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s t : Set α
hst : t ⊆ s
x : α
hx : Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x
y : α
hy : Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) y
hxy :
  Eq.{u_2 + 1} (α := α)
    (↑((ofFixingSubgroup_of_inclusion M (s := s) (t := t) hst : (a : ↥(ofFixingSubgroup M s)) → ↥(ofFixingSubgroup M t))
          (Subtype.mk (p := fun (x : α) ↦
            Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) x hx)) :
      α)
    (↑((ofFixingSubgroup_of_inclusion M (s := s) (t := t) hst : (a : ↥(ofFixingSubgroup M s)) → ↥(ofFixingSubgroup M t))
          (Subtype.mk (p := fun (x : α) ↦
            Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) y hy)) :
      α)
⊢ (↑(Subtype.mk (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) x hx) :
      α) =
    (↑(Subtype.mk (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) y hy) :
      α)

Tactic:
hxy
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s t : Set α
hst : t ⊆ s
x : α
hx : Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x
y : α
hy : Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) y
hxy :
  Eq.{u_2 + 1} (α := α)
    (↑((ofFixingSubgroup_of_inclusion M (s := s) (t := t) hst : (a : ↥(ofFixingSubgroup M s)) → ↥(ofFixingSubgroup M t))
          (Subtype.mk (p := fun (x : α) ↦
            Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) x hx)) :
      α)
    (↑((ofFixingSubgroup_of_inclusion M (s := s) (t := t) hst : (a : ↥(ofFixingSubgroup M s)) → ↥(ofFixingSubgroup M t))
          (Subtype.mk (p := fun (x : α) ↦
            Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) y hy)) :
      α)
⊢ (↑(Subtype.mk (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) x hx) :
      α) =
    (↑(Subtype.mk (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) y hy) :
      α)

Tactic:
exact hxy
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s_1 s t : Set α
a : α
x : ↥(ofFixingSubgroup M {a})
⊢ Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) (↑x : α)

Tactic:
simp
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
a : α
⊢ Bijective (α := ↥(ofFixingSubgroup M {a})) (β := ↥(ofStabilizer M a))
    (⇑(ofFixingSubgroup_of_singleton M a) : (a_1 : ↥(ofFixingSubgroup M {a})) → ↥(ofStabilizer M a))

Tactic:
⟨fun _ _ ↦ id, fun x ↦ ⟨x, rfl⟩⟩

Premises used: id, And.intro, Exists.intro, Function.Bijective, rfl
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s_1 s t : Set α
hst : s = t
x_1 : ↥(ofFixingSubgroup M s)
x : α
hx rw : Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x
⊢ Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M t)) α) (ofFixingSubgroup M t) x

Tactic:
rw [← hst]
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s_1 s t : Set α
hst : s = t
x_1 : ↥(ofFixingSubgroup M s)
x : α
hx : Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x
⊢ Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x

Tactic:
hx
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s_1 s t : Set α
hst : s = t
x_1 : ↥(ofFixingSubgroup M s)
x : α
hx : Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x
⊢ Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x

Tactic:
exact hx
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s t : Set α
hst : s = t
x : ↥(ofFixingSubgroup M s)
⊢ (↑((ofFixingSubgroup_of_eq M (s := s) (t := t) hst : (a : ↥(ofFixingSubgroup M s)) → ↥(ofFixingSubgroup M t)) x) :
      α) =
    (↑x : α)

Tactic:
rfl

Premises used: Set.Mem, setOf, Not, rfl
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s t : Set α
hst : s = t
x x_1 : ↥(ofFixingSubgroup M s)
hxy :
  Eq (α := ↥(ofFixingSubgroup M t))
    ((ofFixingSubgroup_of_eq M (s := s) (t := t) hst : (a : ↥(ofFixingSubgroup M s)) → ↥(ofFixingSubgroup M t)) x :
      ↥(ofFixingSubgroup M t))
    ((ofFixingSubgroup_of_eq M (s := s) (t := t) hst : (a : ↥(ofFixingSubgroup M s)) → ↥(ofFixingSubgroup M t)) x_1 :
      ↥(ofFixingSubgroup M t))
⊢ x = x_1

Tactic:
simpa [← SetLike.coe_eq_coe] using hxy

Premises used: SetLike.coe_eq_coe
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s t : Set α
hst : s = t
x_1 : ↥(ofFixingSubgroup M t)
x : α
hxt rwa rwa₁ rwa₂ rwa₃ :
  Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M t)) α) (ofFixingSubgroup M t) x
⊢ Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x

Tactic:
rwa [hst]
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s t : Set α
hst : s = t
x_1 : ↥(ofFixingSubgroup M t)
x : α
hxt : Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M t)) α) (ofFixingSubgroup M t) x
⊢ (ofFixingSubgroup_of_eq M (s := s) (t := t) hst : (a : ↥(ofFixingSubgroup M s)) → ↥(ofFixingSubgroup M t))
      (Subtype.mk (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) x ⋯) =
    Subtype.mk (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M t)) α) (ofFixingSubgroup M t) x) x hxt

Tactic:
simp [← SetLike.coe_eq_coe]

Premises used: SetLike.coe_eq_coe
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
n : ℕ
inst_2 : Finite.{u_2 + 1} (↑s : Type u_2)
x : Fin n ↪ ↥(ofFixingSubgroup M s)
⊢ Nat.card (Fin s.ncard) = Nat.card.{u_2} (↑s : Type u_2)

Tactic:
simp [Nat.card_coe_set_eq]

Premises used: Nat.card_coe_set_eq
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
n : ℕ
inst_2 : Finite.{u_2 + 1} (↑s : Type u_2)
x : Fin n ↪ ↥(ofFixingSubgroup M s)
⊢ Nonempty.{max 1 (u_2 + 1)} (Fin s.ncard ≃ (↑s : Type u_2))

Tactic:
have : Nonempty (Fin (s.ncard) ≃ s) :=
    Finite.card_eq.mp (by simp [Nat.card_coe_set_eq])
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
n : ℕ
inst_2 : Finite.{u_2 + 1} (↑s : Type u_2)
x : Fin n ↪ ↥(ofFixingSubgroup M s)
this : Nonempty.{max 1 (u_2 + 1)} (Fin s.ncard ≃ (↑s : Type u_2))
y : Fin s.ncard ↪ (↑s : Type u_2) := (Classical.choice this).toEmbedding
apply :
  Disjoint (α := Set α)
    (Set.range (ι := Fin s.ncard) (⇑(y.trans (subtype fun (x : α) ↦ x ∈ s)) : (a : Fin s.ncard) → α))
    (Set.range (ι := Fin n)
      (⇑(x.trans
            (subtype fun (x : α) ↦
              Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x)) :
        (a : Fin n) → α))
⊢ Fin (s.ncard + n) ↪ α

Tactic:
apply Fin.Embedding.append (x := y.trans (subtype _)) (y := x.trans (subtype _))

Premises used: Fin.Embedding.append
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
n : ℕ
inst_2 : Finite.{u_2 + 1} (↑s : Type u_2)
x : Fin n ↪ ↥(ofFixingSubgroup M s)
this : Nonempty.{max 1 (u_2 + 1)} (Fin s.ncard ≃ (↑s : Type u_2))
y : Fin s.ncard ↪ (↑s : Type u_2) := (Classical.choice this).toEmbedding
rw :
  ∀ ⦃a : α⦄,
    Membership.mem (γ := Set α)
        (Set.range (ι := Fin s.ncard) (⇑(y.trans (subtype fun (x : α) ↦ x ∈ s)) : (a : Fin s.ncard) → α)) a →
      ∀ ⦃b : α⦄,
        Membership.mem (γ := Set α)
            (Set.range (ι := Fin n)
              (⇑(x.trans
                    (subtype fun (x : α) ↦
                      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s)
                        x)) :
                (a : Fin n) → α))
            b →
          a ≠ b
⊢ Disjoint (α := Set α)
    (Set.range (ι := Fin s.ncard) (⇑(y.trans (subtype fun (x : α) ↦ x ∈ s)) : (a : Fin s.ncard) → α))
    (Set.range (ι := Fin n)
      (⇑(x.trans
            (subtype fun (x : α) ↦
              Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x)) :
        (a : Fin n) → α))

Tactic:
rw [Set.disjoint_iff_forall_ne]

Premises used: Set.disjoint_iff_forall_ne
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
n : ℕ
inst_2 : Finite.{u_2 + 1} (↑s : Type u_2)
x : Fin n ↪ ↥(ofFixingSubgroup M s)
this : Nonempty.{max 1 (u_2 + 1)} (Fin s.ncard ≃ (↑s : Type u_2))
y : Fin s.ncard ↪ (↑s : Type u_2) := (Classical.choice this).toEmbedding
j : Fin s.ncard
i : Fin n
H :
  Eq (α := α) ((y.trans (subtype fun (x : α) ↦ x ∈ s) : (a : Fin s.ncard) → α) j : α)
    ((x.trans
            (subtype fun (x : α) ↦
              Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) :
          (a : Fin n) → α)
        i :
      α)
apply : (↑((x : (a : Fin n) → ↥(ofFixingSubgroup M s)) i) : α) ∈ s
⊢ False

Tactic:
apply (x i).prop

Premises used: Subtype.prop, DFunLike.coe
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
n : ℕ
inst_2 : Finite.{u_2 + 1} (↑s : Type u_2)
x : Fin n ↪ ↥(ofFixingSubgroup M s)
this : Nonempty.{max 1 (u_2 + 1)} (Fin s.ncard ≃ (↑s : Type u_2))
y : Fin s.ncard ↪ (↑s : Type u_2) := (Classical.choice this).toEmbedding
j : Fin s.ncard
i : Fin n
H :
  Eq.{u_2 + 1} (α := α) (↑((y : (a : Fin s.ncard) → (↑s : Type u_2)) j) : α)
    (↑((x : (a : Fin n) → ↥(ofFixingSubgroup M s)) i) : α)
⊢ (↑((x : (a : Fin n) → ↥(ofFixingSubgroup M s)) i) : α) ∈ s

Tactic:
simpa [H] using Subtype.coe_prop (y j)

Premises used: Subtype.coe_prop, DFunLike.coe
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
n : ℕ
inst_2 : Finite.{u_2 + 1} (↑s : Type u_2)
x : Fin n ↪ ↥(ofFixingSubgroup M s)
i : Fin s.ncard
⊢ Nat.card (Fin s.ncard) = Nat.card.{u_2} (↑s : Type u_2)

Tactic:
simp [Nat.card_coe_set_eq]

Premises used: Nat.card_coe_set_eq
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
n : ℕ
inst_2 : Finite.{u_2 + 1} (↑s : Type u_2)
x : Fin n ↪ ↥(ofFixingSubgroup M s)
i : Fin s.ncard
⊢ let Hs : Nonempty.{max 1 (u_2 + 1)} (Fin s.ncard ≃ (↑s : Type u_2)) := ⋯;
  Eq (α := α) ((append (s := s) x : (a : Fin (s.ncard + n)) → α) (Fin.castAdd n i) : α)
    ((↑((Classical.choice Hs : (a : Fin s.ncard) → (↑s : Type u_2)) i) : α) : α)

Tactic:
simp [ofFixingSubgroup.append]

Premises used: SubMulAction.ofFixingSubgroup.append
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
n : ℕ
inst_2 : Finite.{u_2 + 1} (↑s : Type u_2)
x : Fin n ↪ ↥(ofFixingSubgroup M s)
i : Fin n
⊢ Eq (α := α) ((append (s := s) x : (a : Fin (s.ncard + n)) → α) (Fin.natAdd s.ncard i) : α)
    ((↑((x : (a : Fin n) → ↥(ofFixingSubgroup M s)) i) : α) : α)

Tactic:
simp [ofFixingSubgroup.append]

Premises used: SubMulAction.ofFixingSubgroup.append
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
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
ha : s ∪ g • s ≠ ⊤
⊢ (s ∪ g • s)ᶜ.Nonempty

Tactic:
rw [Ne, Set.top_eq_univ, ← Set.compl_empty_iff, ← Ne, ← Set.nonempty_iff_ne_empty] at ha

Premises used: Ne, Set.top_eq_univ, Set.compl_empty_iff, Set.nonempty_iff_ne_empty
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
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
ha : (s ∪ g • s)ᶜ.Nonempty
obtain :
  ∀ (a : α) (ha : a ∈ (s ∪ g • s)ᶜ),
    IsPretransitive.{u_1, u_2} ↥(fixingSubgroup M (s ∩ g • s)) ↥(ofFixingSubgroup M (s ∩ g • s))
⊢ IsPretransitive.{u_1, u_2} ↥(fixingSubgroup M (s ∩ g • s)) ↥(ofFixingSubgroup M (s ∩ g • s))

Tactic:
obtain ⟨a, ha⟩ := ha
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
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)ᶜ
⊢ a ∈ sᶜ ∩ (g • s)ᶜ

Tactic:
rw [Set.compl_union] at ha

Premises used: Set.compl_union
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
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)ᶜ
rw : a ∈ sᶜ ∪ (g • s)ᶜ
⊢ a ∈ (s ∩ g • s)ᶜ

Tactic:
rw [Set.compl_inter]

Premises used: Set.compl_inter
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
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)ᶜ
⊢ a ∈ sᶜ ∪ (g • s)ᶜ

Tactic:
Set.mem_union_left _ ha.1

Premises used: And.left, Set.mem_union_left
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
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)ᶜ
⊢ a ∈ sᶜ ∪ (g • s)ᶜ

Tactic:
exact Set.mem_union_left _ ha.1

Premises used: And.left, Set.mem_union_left
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
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)ᶜ
⊢ a ∈ (s ∩ g • s)ᶜ

Tactic:
have ha' : a ∈ (s ∩ g • s)ᶜ := by
    rw [Set.compl_inter]
    exact Set.mem_union_left _ ha.1