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_1 s t : Set α
m : ↥(fixingSubgroup M (s ∪ t))
x : α
hx : Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x
hx'_1 :
  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) x hx)
hx' : x ∈ t
⊢ Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (fixingSubgroup M s) x) (↑m : M) ⋯ •
      (↑(Subtype.mk (p := fun (x : ↥(ofFixingSubgroup M s)) ↦
            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)
              x)
            (Subtype.mk (p := fun (x : α) ↦
              Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) x hx)
            hx'_1) :
        ↥(ofFixingSubgroup M s)) =
    (↑(Subtype.mk (p := fun (x : ↥(ofFixingSubgroup M s)) ↦
          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)
            x)
          (Subtype.mk (p := fun (x : α) ↦
            Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) x hx)
          hx'_1) :
      ↥(ofFixingSubgroup M s))
have simp : Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (fixingSubgroup M s) x) (↑m : M) sorry • x = x
Tactic: simp only [← SetLike.coe_eq_coe, SubMulAction.val_smul_of_tower]
-- 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_1 s t : Set α
m : ↥(fixingSubgroup M (s ∪ t))
hm : Membership.mem (γ := Subgroup M) (fixingSubgroup M (s ∪ t)) (↑m : M) := ⋯
⊢ Membership.mem (γ := Subgroup M) (fixingSubgroup M s) (↑m : M)
have hm₁ : Membership.mem (γ := Subgroup M) (fixingSubgroup M s) (↑m : M) ∧
  Membership.mem (γ := Subgroup M) (fixingSubgroup M t) (↑m : M)
Tactic: simp only [fixingSubgroup_union, Subgroup.mem_inf] at hm
Cleared hypotheses: hm
-- 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_1 s t : Set α
m : ↥(fixingSubgroup M (s ∪ t))
hm : Membership.mem (γ := Subgroup M) (fixingSubgroup M (s ∪ t)) (↑m : M) := ⋯
⊢ Membership.mem (γ := Subgroup ↥(fixingSubgroup M s))
    (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))
    (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (fixingSubgroup M s) x) (↑m : M) ⋯)
have hm₁ : Membership.mem (γ := Subgroup M) (fixingSubgroup M s) (↑m : M) ∧
  Membership.mem (γ := Subgroup M) (fixingSubgroup M t) (↑m : M)
Tactic: simp only [fixingSubgroup_union, Subgroup.mem_inf] at hm
Cleared hypotheses: hm
-- 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_1 s t : Set α
m : ↥(fixingSubgroup M (s ∪ t))
hm :
  Membership.mem (γ := Subgroup M) (fixingSubgroup M s) (↑m : M) ∧
    Membership.mem (γ := Subgroup M) (fixingSubgroup M t) (↑m : M)
x : α
hx : Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x
hx' :
  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) x hx)
⊢ Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (fixingSubgroup M s) x) (↑m : M) ⋯ •
      (↑(Subtype.mk (p := fun (x : ↥(ofFixingSubgroup M s)) ↦
            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)
              x)
            (Subtype.mk (p := fun (x : α) ↦
              Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) x hx)
            hx') :
        ↥(ofFixingSubgroup M s)) =
    (↑(Subtype.mk (p := fun (x : ↥(ofFixingSubgroup M s)) ↦
          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)
            x)
          (Subtype.mk (p := fun (x : α) ↦
            Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) x hx)
          hx') :
      ↥(ofFixingSubgroup M s))
have hx'₁ : x ∈ t
Tactic: simp only [Set.mem_preimage] at hx'
-- 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_1 s t : Set α
m : ↥(fixingSubgroup M (s ∪ t))
hm :
  Membership.mem (γ := Subgroup M) (fixingSubgroup M s) (↑m : M) ∧
    Membership.mem (γ := Subgroup M) (fixingSubgroup M t) (↑m : M)
x : α
hx : Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x
hx'_1 :
  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) x hx)
hx' : x ∈ t
⊢ Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (fixingSubgroup M s) x) (↑m : M) ⋯ •
      (↑(Subtype.mk (p := fun (x : ↥(ofFixingSubgroup M s)) ↦
            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)
              x)
            (Subtype.mk (p := fun (x : α) ↦
              Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) x hx)
            hx'_1) :
        ↥(ofFixingSubgroup M s)) =
    (↑(Subtype.mk (p := fun (x : ↥(ofFixingSubgroup M s)) ↦
          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)
            x)
          (Subtype.mk (p := fun (x : α) ↦
            Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) x hx)
          hx'_1) :
      ↥(ofFixingSubgroup M s))
have simp : Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (fixingSubgroup M s) x) (↑m : M) sorry • x = x
Tactic: simp only [← SetLike.coe_eq_coe, SubMulAction.val_smul_of_tower]
-- 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_1 s t : Set α
x : ↥(ofFixingSubgroup M (s ∪ t))
hx :
  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) (↑x : α) ⋯)
⊢ (↑x : α) ∈ s ∪ t
have apply : (↑x : α) ∈ t
Tactic: apply Set.mem_union_right s
-- 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 t : Set α
⊢ Bijective (α := ↥(ofFixingSubgroup M (s ∪ t))) (β :=
    ↥(ofFixingSubgroup (↥(fixingSubgroup M s))
        (Subtype.val (p := fun (x : α) ↦
            Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) ⁻¹'
          t)))
    (⇑(map_ofFixingSubgroupUnion M s t) :
      (a : ↥(ofFixingSubgroup M (s ∪ t))) → ↥(ofFixingSubgroup (↥(fixingSubgroup M s)) (Subtype.val ⁻¹' t)))
have left : Injective (α := ↥(ofFixingSubgroup M (s ∪ t))) (β :=
  ↥(ofFixingSubgroup (↥(fixingSubgroup M s))
      (Subtype.val (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) ⁻¹'
        t)))
  (⇑(map_ofFixingSubgroupUnion M s t) :
    (a : ↥(ofFixingSubgroup M (s ∪ t))) → ↥(ofFixingSubgroup (↥(fixingSubgroup M s)) (Subtype.val ⁻¹' t)))
Tactic: constructor
-- 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 t : Set α
left :
  Injective (α := ↥(ofFixingSubgroup M (s ∪ t))) (β :=
    ↥(ofFixingSubgroup (↥(fixingSubgroup M s))
        (Subtype.val (p := fun (x : α) ↦
            Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) ⁻¹'
          t)))
    (⇑(map_ofFixingSubgroupUnion M s t) :
      (a : ↥(ofFixingSubgroup M (s ∪ t))) → ↥(ofFixingSubgroup (↥(fixingSubgroup M s)) (Subtype.val ⁻¹' t)))
⊢ Bijective (α := ↥(ofFixingSubgroup M (s ∪ t))) (β :=
    ↥(ofFixingSubgroup (↥(fixingSubgroup M s))
        (Subtype.val (p := fun (x : α) ↦
            Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) ⁻¹'
          t)))
    (⇑(map_ofFixingSubgroupUnion M s t) :
      (a : ↥(ofFixingSubgroup M (s ∪ t))) → ↥(ofFixingSubgroup (↥(fixingSubgroup M s)) (Subtype.val ⁻¹' t)))
have right : Surjective (α := ↥(ofFixingSubgroup M (s ∪ t))) (β :=
  ↥(ofFixingSubgroup (↥(fixingSubgroup M s))
      (Subtype.val (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) ⁻¹'
        t)))
  (⇑(map_ofFixingSubgroupUnion M s t) :
    (a : ↥(ofFixingSubgroup M (s ∪ t))) → ↥(ofFixingSubgroup (↥(fixingSubgroup M s)) (Subtype.val ⁻¹' t)))
Tactic: constructor
-- 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 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)
⊢ ∃ (a_1 : ↥(ofFixingSubgroup M (s ∪ t))),
    (map_ofFixingSubgroupUnion M s t :
          (a : ↥(ofFixingSubgroup M (s ∪ t))) → ↥(ofFixingSubgroup (↥(fixingSubgroup M s)) (Subtype.val ⁻¹' t)))
        a_1 =
      Subtype.mk (p := fun (x : ↥(ofFixingSubgroup M s)) ↦
        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))
          x)
        (Subtype.mk (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) a ha)
        ha'
have right : Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M (s ∪ t))) α) (ofFixingSubgroup M (s ∪ t)) a
Tactic: suffices a ∈ ofFixingSubgroup M (s ∪ t) by
      exact ⟨⟨a, this⟩,  rfl⟩
-- 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 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
⊢ False
have right : ∀ (h : a ∈ s), False
Tactic: rcases (Set.mem_union a s t).mp hy with h | h
-- 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 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
⊢ False
have right₁ : ∀ (h : a ∈ t), False
Tactic: rcases (Set.mem_union a s t).mp hy with h | h
-- 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 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
⊢ False
have 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)
Tactic: apply 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 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))
⊢ 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
have 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) :
      α)
Tactic: rw [← SetLike.coe_eq_coe] at hxy ⊢
Cleared hypotheses: hxy
-- 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 α
n : ℕ
inst_2 : Finite.{u_2 + 1} (↑s : Type u_2)
x : Fin n ↪ ↥(ofFixingSubgroup M s)
⊢ Fin (s.ncard + n) ↪ α
have this : 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])
-- 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 α
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
⊢ Fin (s.ncard + n) ↪ α
have 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) → α))
Tactic: apply Fin.Embedding.append (x := y.trans (subtype _)) (y := x.trans (subtype _))
-- 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 α
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
⊢ 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) → α))
have 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
Tactic: rw [Set.disjoint_iff_forall_ne]
-- 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 α
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 :
      α)
⊢ False
have apply : (↑((x : (a : Fin n) → ↥(ofFixingSubgroup M s)) i) : α) ∈ s
Tactic: apply (x i).prop
-- 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 α
hs : IsPretransitive.{u_1, u_2} ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
g : M
ha : s ∪ g • s ≠ ⊤
⊢ IsPretransitive.{u_1, u_2} ↥(fixingSubgroup M (s ∩ g • s)) ↥(ofFixingSubgroup M (s ∩ g • s))
have ha₁ : (s ∪ g • s)ᶜ.Nonempty
Tactic: rw [Ne, Set.top_eq_univ, ← Set.compl_empty_iff, ← Ne, ← Set.nonempty_iff_ne_empty] at ha
Cleared hypotheses: 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 α
hs : IsPretransitive.{u_1, u_2} ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
g : M
ha : (s ∪ g • s)ᶜ.Nonempty
⊢ IsPretransitive.{u_1, u_2} ↥(fixingSubgroup M (s ∩ g • s)) ↥(ofFixingSubgroup M (s ∩ g • s))
have obtain : ∀ (a : α) (ha : a ∈ (s ∪ g • s)ᶜ),
  IsPretransitive.{u_1, u_2} ↥(fixingSubgroup M (s ∩ g • s)) ↥(ofFixingSubgroup M (s ∩ g • s))
Tactic: obtain ⟨a, ha⟩ := ha
Cleared hypotheses: ha
-- 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 α
hs : IsPretransitive.{u_1, u_2} ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
g : M
a : α
ha : a ∈ (s ∪ g • s)ᶜ
⊢ IsPretransitive.{u_1, u_2} ↥(fixingSubgroup M (s ∩ g • s)) ↥(ofFixingSubgroup M (s ∩ g • s))
have ha₁ : a ∈ sᶜ ∩ (g • s)ᶜ
Tactic: rw [Set.compl_union] at ha
Cleared hypotheses: ha