awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
K : Type u_2
inst : Group K
inst_1 : MulAction K α
hα : Nat.card α = 2
hK : fixedPoints K α ≠ _root_.Set.univ
n : ℕ
this_1 : Finite α
this : Fintype α
φ : MonoidHom.{u_2, u_1} K (Perm α) := toPermHom K α
f : MulActionHom.{u_2, u_1, u_1, u_1} (M := K) (N := Perm α) (⇑φ : (a : K) → Perm α) α α :=
  { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective (α := α) (β := α) (⇑f : (a : α) → α)
h : Nat.card.{u_1} ↥φ.range = Nat.card.{u_1} (Perm α)
⊢ φ.range = ⊤

Tactic:
apply Subgroup.eq_top_of_card_eq

Premises used: Subgroup.eq_top_of_card_eq
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
K : Type u_2
inst : Group K
inst_1 : MulAction K α
hα : Nat.card α = 2
hK : fixedPoints K α ≠ _root_.Set.univ
n : ℕ
this_1 : Finite α
this : Fintype α
φ : MonoidHom.{u_2, u_1} K (Perm α) := toPermHom K α
f : MulActionHom.{u_2, u_1, u_1, u_1} (M := K) (N := Perm α) (⇑φ : (a : K) → Perm α) α α :=
  { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective (α := α) (β := α) (⇑f : (a : α) → α)
h : Nat.card.{u_1} (Perm α) ≤ Nat.card.{u_1} ↥φ.range
⊢ Nat.card.{u_1} ↥φ.range = Nat.card.{u_1} (Perm α)

Tactic:
apply le_antisymm (card_le_card_group φ.range)

Premises used: MonoidHom.range, Subgroup.card_le_card_group, le_antisymm
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
K : Type u_2
inst : Group K
inst_1 : MulAction K α
hα : Nat.card α = 2
hK : fixedPoints K α ≠ _root_.Set.univ
n : ℕ
this_1 : Finite α
this : Fintype α
φ : MonoidHom.{u_2, u_1} K (Perm α) := toPermHom K α
f : MulActionHom.{u_2, u_1, u_1, u_1} (M := K) (N := Perm α) (⇑φ : (a : K) → Perm α) α α :=
  { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective (α := α) (β := α) (⇑f : (a : α) → α)
h : 2 ≤ Nat.card.{u_1} ↥φ.range
⊢ Nat.card.{u_1} (Perm α) ≤ Nat.card.{u_1} ↥φ.range

Tactic:
simp only [Nat.card_perm, hα, Nat.factorial_two]

Premises used: Nat.card_perm, Nat.factorial_two
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
K : Type u_2
inst : Group K
inst_1 : MulAction K α
hα : Nat.card α = 2
hK : fixedPoints K α ≠ _root_.Set.univ
n : ℕ
this_1 : Finite α
this : Fintype α
φ : MonoidHom.{u_2, u_1} K (Perm α) := toPermHom K α
f : MulActionHom.{u_2, u_1, u_1, u_1} (M := K) (N := Perm α) (⇑φ : (a : K) → Perm α) α α :=
  { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective (α := α) (β := α) (⇑f : (a : α) → α)
h : ∀ (H : ¬2 ≤ Nat.card.{u_1} ↥φ.range), False
⊢ 2 ≤ Nat.card.{u_1} ↥φ.range

Tactic:
by_contra H
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
K : Type u_2
inst : Group K
inst_1 : MulAction K α
hα : Nat.card α = 2
hK : fixedPoints K α ≠ _root_.Set.univ
n : ℕ
this_1 : Finite α
this : Fintype α
φ : MonoidHom.{u_2, u_1} K (Perm α) := toPermHom K α
f : MulActionHom.{u_2, u_1, u_1, u_1} (M := K) (N := Perm α) (⇑φ : (a : K) → Perm α) α α :=
  { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective (α := α) (β := α) (⇑f : (a : α) → α)
H : ¬2 ≤ Nat.card.{u_1} ↥φ.range
⊢ Subsingleton.{u_1 + 1} ↥φ.range

Tactic:
simp only [not_le, Nat.lt_succ_iff, Finite.card_le_one_iff_subsingleton] at H

Premises used: not_le, Finite.card_le_one_iff_subsingleton, Nat.lt_succ_iff
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
K : Type u_2
inst : Group K
inst_1 : MulAction K α
hα : Nat.card α = 2
hK : fixedPoints K α ≠ _root_.Set.univ
n : ℕ
this_1 : Finite α
this : Fintype α
φ : MonoidHom.{u_2, u_1} K (Perm α) := toPermHom K α
f : MulActionHom.{u_2, u_1, u_1, u_1} (M := K) (N := Perm α) (⇑φ : (a : K) → Perm α) α α :=
  { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective (α := α) (β := α) (⇑f : (a : α) → α)
H : Subsingleton.{u_1 + 1} ↥φ.range
h : fixedPoints K α = _root_.Set.univ
⊢ False

Tactic:
apply hK
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
K : Type u_2
inst : Group K
inst_1 : MulAction K α
hα : Nat.card α = 2
hK : fixedPoints K α ≠ _root_.Set.univ
n : ℕ
this_1 : Finite α
this : Fintype α
φ : MonoidHom.{u_2, u_1} K (Perm α) := toPermHom K α
f : MulActionHom.{u_2, u_1, u_1, u_1} (M := K) (N := Perm α) (⇑φ : (a : K) → Perm α) α α :=
  { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective (α := α) (β := α) (⇑f : (a : α) → α)
H : Subsingleton.{u_1 + 1} ↥φ.range
h : _root_.Set.univ ⊆ fixedPoints K α
⊢ fixedPoints K α = _root_.Set.univ

Tactic:
apply Set.eq_univ_of_univ_subset

Premises used: Set.eq_univ_of_univ_subset
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
K : Type u_2
inst : Group K
inst_1 : MulAction K α
hα : Nat.card α = 2
hK : fixedPoints K α ≠ _root_.Set.univ
n : ℕ
this_1 : Finite α
this : Fintype α
φ : MonoidHom.{u_2, u_1} K (Perm α) := toPermHom K α
f : MulActionHom.{u_2, u_1, u_1, u_1} (M := K) (N := Perm α) (⇑φ : (a : K) → Perm α) α α :=
  { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective (α := α) (β := α) (⇑f : (a : α) → α)
H : Subsingleton.{u_1 + 1} ↥φ.range
a : α
h : Membership.mem (γ := Set α) _root_.Set.univ a → a ∈ fixedPoints K α
⊢ Membership.mem (γ := Set α) _root_.Set.univ a → a ∈ fixedPoints K α

Tactic:
_
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
K : Type u_2
inst : Group K
inst_1 : MulAction K α
hα : Nat.card α = 2
hK : fixedPoints K α ≠ _root_.Set.univ
n : ℕ
this_1 : Finite α
this_2 : Fintype α
φ : MonoidHom.{u_2, u_1} K (Perm α) := toPermHom K α
f : MulActionHom.{u_2, u_1, u_1, u_1} (M := K) (N := Perm α) (⇑φ : (a : K) → Perm α) α α :=
  { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective (α := α) (β := α) (⇑f : (a : α) → α)
H : Subsingleton.{u_1 + 1} ↥φ.range
a : α
h : Membership.mem (γ := Set α) _root_.Set.univ a
g : K
this : Eq.{u_1 + 1} (α := Perm α) ((φ : (a : K) → Perm α) g : Perm α) ((φ : (a : K) → Perm α) 1 : Perm α)
rw : HSMul.hSMul.{u_2, u_1, u_1} (α := K) 1 a
| a

Tactic:
rw [← one_smul K a]

Premises used: one_smul
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
K : Type u_2
inst : Group K
inst_1 : MulAction K α
hα : Nat.card α = 2
hK : fixedPoints K α ≠ _root_.Set.univ
n : ℕ
this_1 : Finite α
this_2 : Fintype α
φ : MonoidHom.{u_2, u_1} K (Perm α) := toPermHom K α
f : MulActionHom.{u_2, u_1, u_1, u_1} (M := K) (N := Perm α) (⇑φ : (a : K) → Perm α) α α :=
  { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective (α := α) (β := α) (⇑f : (a : α) → α)
H : Subsingleton.{u_1 + 1} ↥φ.range
a : α
h : Membership.mem (γ := Set α) _root_.Set.univ a
g : K
this : Eq.{u_1 + 1} (α := Perm α) ((φ : (a : K) → Perm α) g : Perm α) ((φ : (a : K) → Perm α) 1 : Perm α)
conv_rhs : g • a = HSMul.hSMul.{u_2, u_1, u_1} (α := K) 1 a
⊢ g • a = a

Tactic:
conv_rhs => rw [← one_smul K a]

Premises used: one_smul
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
K : Type u_2
inst : Group K
inst_1 : MulAction K α
hα : Nat.card α = 2
hK : fixedPoints K α ≠ _root_.Set.univ
n : ℕ
this_1 : Finite α
this_2 : Fintype α
φ : MonoidHom.{u_2, u_1} K (Perm α) := toPermHom K α
f : MulActionHom.{u_2, u_1, u_1, u_1} (M := K) (N := Perm α) (⇑φ : (a : K) → Perm α) α α :=
  { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective (α := α) (β := α) (⇑f : (a : α) → α)
H : Subsingleton.{u_1 + 1} ↥φ.range
a : α
h : Membership.mem (γ := Set α) _root_.Set.univ a
g : K
this : Eq.{u_1 + 1} (α := Perm α) ((φ : (a : K) → Perm α) g : Perm α) ((φ : (a : K) → Perm α) 1 : Perm α)
simp :
  Eq (α := α)
    (((((toPermHom K α : MonoidHom.{u_2, u_1} K (Perm α)) : (a : K) → Perm α) g : Perm α) : (a : α) → α) a : α)
    ((toPerm.{u_2, u_1} (α := K) 1 : (a : α) → α) a : α)
⊢ g • a = HSMul.hSMul.{u_2, u_1, u_1} (α := K) 1 a

Tactic:
simp only [← toPerm_apply, ← toPermHom_apply K α g]

Premises used: MulAction.toPerm_apply, MulAction.toPermHom_apply
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
K : Type u_2
inst : Group K
inst_1 : MulAction K α
hα : Nat.card α = 2
hK : fixedPoints K α ≠ _root_.Set.univ
n : ℕ
this_1 : Finite α
this_2 : Fintype α
φ : MonoidHom.{u_2, u_1} K (Perm α) := toPermHom K α
f : MulActionHom.{u_2, u_1, u_1, u_1} (M := K) (N := Perm α) (⇑φ : (a : K) → Perm α) α α :=
  { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective (α := α) (β := α) (⇑f : (a : α) → α)
H : Subsingleton.{u_1 + 1} ↥φ.range
a : α
h : Membership.mem (γ := Set α) _root_.Set.univ a
g : K
this : Eq.{u_1 + 1} (α := Perm α) ((φ : (a : K) → Perm α) g : Perm α) ((φ : (a : K) → Perm α) 1 : Perm α)
⊢ Eq (α := α)
    (((((toPermHom K α : MonoidHom.{u_2, u_1} K (Perm α)) : (a : K) → Perm α) g : Perm α) : (a : α) → α) a : α)
    ((toPerm.{u_2, u_1} (α := K) 1 : (a : α) → α) a : α)

Tactic:
congrFun (congrArg DFunLike.coe this) a

Premises used: congrArg, congrFun, DFunLike.coe
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
K : Type u_2
inst : Group K
inst_1 : MulAction K α
hα : Nat.card α = 2
hK : fixedPoints K α ≠ _root_.Set.univ
n : ℕ
this_1 : Finite α
this_2 : Fintype α
φ : MonoidHom.{u_2, u_1} K (Perm α) := toPermHom K α
f : MulActionHom.{u_2, u_1, u_1, u_1} (M := K) (N := Perm α) (⇑φ : (a : K) → Perm α) α α :=
  { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective (α := α) (β := α) (⇑f : (a : α) → α)
H : Subsingleton.{u_1 + 1} ↥φ.range
a : α
h : Membership.mem (γ := Set α) _root_.Set.univ a
g : K
this : Eq.{u_1 + 1} (α := Perm α) ((φ : (a : K) → Perm α) g : Perm α) ((φ : (a : K) → Perm α) 1 : Perm α)
⊢ Eq (α := α)
    (((((toPermHom K α : MonoidHom.{u_2, u_1} K (Perm α)) : (a : K) → Perm α) g : Perm α) : (a : α) → α) a : α)
    ((toPerm.{u_2, u_1} (α := K) 1 : (a : α) → α) a : α)

Tactic:
exact congrFun (congrArg DFunLike.coe this) a

Premises used: congrArg, congrFun, DFunLike.coe
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
K : Type u_2
inst : Group K
inst_1 : MulAction K α
hα : Nat.card α = 2
hK : fixedPoints K α ≠ _root_.Set.univ
n : ℕ
this_1 : Finite α
this : Fintype α
φ : MonoidHom.{u_2, u_1} K (Perm α) := toPermHom K α
f : MulActionHom.{u_2, u_1, u_1, u_1} (M := K) (N := Perm α) (⇑φ : (a : K) → Perm α) α α :=
  { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective (α := α) (β := α) (⇑f : (a : α) → α)
H : Subsingleton.{u_1 + 1} ↥φ.range
a : α
h_1 : Membership.mem (γ := Set α) _root_.Set.univ a
g : K
h : Eq.{u_1 + 1} (α := Perm α) ((φ : (a : K) → Perm α) g : Perm α) ((φ : (a : K) → Perm α) 1 : Perm α)
⊢ g • a = a

Tactic:
suffices φ g = φ 1 by
    conv_rhs => rw [← one_smul K a]
    simp only [← toPerm_apply, ← toPermHom_apply K α g]
    exact congrFun (congrArg DFunLike.coe this) a
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
K : Type u_2
inst : Group K
inst_1 : MulAction K α
hα : Nat.card α = 2
hK : fixedPoints K α ≠ _root_.Set.univ
n : ℕ
this_1 : Finite α
this : Fintype α
φ : MonoidHom.{u_2, u_1} K (Perm α) := toPermHom K α
f : MulActionHom.{u_2, u_1, u_1, u_1} (M := K) (N := Perm α) (⇑φ : (a : K) → Perm α) α α :=
  { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective (α := α) (β := α) (⇑f : (a : α) → α)
H : Subsingleton.{u_1 + 1} ↥φ.range
a : α
h : Membership.mem (γ := Set α) _root_.Set.univ a
g : K
⊢ Eq.{u_1 + 1} (α := Perm α) ((φ : (a : K) → Perm α) g : Perm α) ((φ : (a : K) → Perm α) 1 : Perm α)

Tactic:
simpa [← Subtype.coe_inj] using H.elim ⟨_, ⟨g, rfl⟩⟩ ⟨_, ⟨1, rfl⟩⟩

Premises used: Subtype.coe_inj, Subtype.mk, Exists.intro, Subsingleton.elim, OfNat.ofNat, rfl
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
G : Subgroup (Perm α)
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
hgc : g.IsCycle
hg : g ∈ G
obtain :
  ∀ (a : α),
    (g : (a : α) → α) a ≠ a →
      ∀ (hgc : ∀ ⦃y : α⦄, (g : (a : α) → α) y ≠ y → g.SameCycle a y),
        IsPretransitive.{u_1, u_1} ↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)
          ↥(ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ)
⊢ IsPretransitive.{u_1, u_1} ↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ) ↥(ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ)

Tactic:
obtain ⟨a, _, hgc⟩ := hgc
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
G : Subgroup (Perm α)
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
hg : g ∈ G
a : α
left : (g : (a : α) → α) a ≠ a
hgc : ∀ ⦃y : α⦄, (g : (a : α) → α) y ≠ y → g.SameCycle a y
x : α
⊢ g • x ≠ x ↔
    Membership.mem (γ := SubMulAction (↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)) α)
      (ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ) x

Tactic:
simp [SubMulAction.mem_ofFixingSubgroup_iff]

Premises used: SubMulAction.mem_ofFixingSubgroup_iff
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
G : Subgroup (Perm α)
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
hg : g ∈ G
a : α
left : (g : (a : α) → α) a ≠ a
hgc : ∀ ⦃y : α⦄, (g : (a : α) → α) y ≠ y → g.SameCycle a y
⊢ ∀ (x : α),
    g • x ≠ x ↔
      Membership.mem (γ := SubMulAction (↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)) α)
        (ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ) x

Tactic:
have hs : ∀ x : α, g • x ≠ x ↔
    x ∈ SubMulAction.ofFixingSubgroup G ((↑g.support : Set α)ᶜ) := by
    intro x
    simp [SubMulAction.mem_ofFixingSubgroup_iff]
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
G : Subgroup (Perm α)
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
hg : g ∈ G
a : α
left : (g : (a : α) → α) a ≠ a
hgc : ∀ ⦃y : α⦄, (g : (a : α) → α) y ≠ y → g.SameCycle a y
hs :
  ∀ (x : α),
    g • x ≠ x ↔
      Membership.mem (γ := SubMulAction (↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)) α)
        (ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ) x
this :
  ∀ (x : α),
    Membership.mem (γ := SubMulAction (↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)) α)
        (ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ) x →
      ∃ (k : ↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)), x = k • a
rw :
  ∀ (x y : ↥(ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ)),
    ∃ (g_1 : ↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)), g_1 • x = y
⊢ IsPretransitive.{u_1, u_1} ↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ) ↥(ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ)

Tactic:
rw [isPretransitive_iff]

Premises used: MulAction.isPretransitive_iff
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
G : Subgroup (Perm α)
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
hg : g ∈ G
a : α
left : (g : (a : α) → α) a ≠ a
hgc : ∀ ⦃y : α⦄, (g : (a : α) → α) y ≠ y → g.SameCycle a y
hs :
  ∀ (x : α),
    g • x ≠ x ↔
      Membership.mem (γ := SubMulAction (↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)) α)
        (ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ) x
this :
  ∀ (x : α),
    Membership.mem (γ := SubMulAction (↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)) α)
        (ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ) x →
      ∃ (k : ↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)), x = k • a
x : α
hx :
  Membership.mem (γ := SubMulAction (↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)) α)
    (ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ) x
y : α
hy :
  Membership.mem (γ := SubMulAction (↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)) α)
    (ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ) y
obtain :
  ∀ (k : ↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)) (hk : x = k • a),
    ∃ (g_1 : ↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)),
      g_1 •
          Subtype.mk (p := fun (x : α) ↦
            Membership.mem (γ := SubMulAction (↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)) α)
              (ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ) x)
            x hx =
        Subtype.mk (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction (↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)) α)
            (ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ) x)
          y hy
⊢ ∃ (g_1 : ↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)),
    g_1 •
        Subtype.mk (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction (↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)) α)
            (ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ) x)
          x hx =
      Subtype.mk (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction (↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)) α)
          (ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ) x)
        y hy

Tactic:
obtain ⟨k, hk⟩ := this x hx
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
G : Subgroup (Perm α)
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
hg : g ∈ G
a : α
left : (g : (a : α) → α) a ≠ a
hgc : ∀ ⦃y : α⦄, (g : (a : α) → α) y ≠ y → g.SameCycle a y
hs :
  ∀ (x : α),
    g • x ≠ x ↔
      Membership.mem (γ := SubMulAction (↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)) α)
        (ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ) x
this :
  ∀ (x : α),
    Membership.mem (γ := SubMulAction (↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)) α)
        (ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ) x →
      ∃ (k : ↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)), x = k • a
x : α
hx :
  Membership.mem (γ := SubMulAction (↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)) α)
    (ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ) x
y : α
hy :
  Membership.mem (γ := SubMulAction (↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)) α)
    (ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ) y
k : ↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)
hk : x = k • a
obtain :
  ∀ (k' : ↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)) (hk' : y = k' • a),
    ∃ (g_1 : ↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)),
      g_1 •
          Subtype.mk (p := fun (x : α) ↦
            Membership.mem (γ := SubMulAction (↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)) α)
              (ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ) x)
            x hx =
        Subtype.mk (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction (↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)) α)
            (ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ) x)
          y hy
⊢ ∃ (g_1 : ↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)),
    g_1 •
        Subtype.mk (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction (↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)) α)
            (ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ) x)
          x hx =
      Subtype.mk (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction (↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)) α)
          (ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ) x)
        y hy

Tactic:
obtain ⟨k', hk'⟩ := this y hy
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
G : Subgroup (Perm α)
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
hg : g ∈ G
a : α
left : (g : (a : α) → α) a ≠ a
hgc : ∀ ⦃y : α⦄, (g : (a : α) → α) y ≠ y → g.SameCycle a y
hs :
  ∀ (x : α),
    g • x ≠ x ↔
      Membership.mem (γ := SubMulAction (↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)) α)
        (ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ) x
this :
  ∀ (x : α),
    Membership.mem (γ := SubMulAction (↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)) α)
        (ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ) x →
      ∃ (k : ↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)), x = k • a
x : α
hx :
  Membership.mem (γ := SubMulAction (↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)) α)
    (ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ) x
y : α
hy :
  Membership.mem (γ := SubMulAction (↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)) α)
    (ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ) y
k : ↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)
hk : x = k • a
k' : ↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)
hk' : y = k' • a
h :
  (k' * k⁻¹) •
      Subtype.mk (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction (↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)) α)
          (ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ) x)
        x hx =
    Subtype.mk (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction (↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)) α)
        (ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ) x)
      y hy
⊢ ∃ (g_1 : ↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)),
    g_1 •
        Subtype.mk (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction (↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)) α)
            (ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ) x)
          x hx =
      Subtype.mk (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction (↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)) α)
          (ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ) x)
        y hy

Tactic:
use k' * k⁻¹
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
G : Subgroup (Perm α)
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
hg : g ∈ G
a : α
left : (g : (a : α) → α) a ≠ a
hgc : ∀ ⦃y : α⦄, (g : (a : α) → α) y ≠ y → g.SameCycle a y
hs :
  ∀ (x : α),
    g • x ≠ x ↔
      Membership.mem (γ := SubMulAction (↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)) α)
        (ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ) x
this :
  ∀ (x : α),
    Membership.mem (γ := SubMulAction (↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)) α)
        (ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ) x →
      ∃ (k : ↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)), x = k • a
x : α
hx :
  Membership.mem (γ := SubMulAction (↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)) α)
    (ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ) x
y : α
hy :
  Membership.mem (γ := SubMulAction (↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)) α)
    (ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ) y
k : ↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)
hk : x = k • a
k' : ↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)
hk' : y = k' • a
h :
  (↑((k' * k⁻¹) •
          Subtype.mk (p := fun (x : α) ↦
            Membership.mem (γ := SubMulAction (↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)) α)
              (ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ) x)
            x hx) :
      α) =
    (↑(Subtype.mk (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction (↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)) α)
            (ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ) x)
          y hy) :
      α)
⊢ (k' * k⁻¹) •
      Subtype.mk (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction (↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)) α)
          (ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ) x)
        x hx =
    Subtype.mk (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction (↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)) α)
        (ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ) x)
      y hy

Tactic:
rw [← SetLike.coe_eq_coe]

Premises used: SetLike.coe_eq_coe
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
G : Subgroup (Perm α)
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
hg : g ∈ G
a : α
left : (g : (a : α) → α) a ≠ a
hgc : ∀ ⦃y : α⦄, (g : (a : α) → α) y ≠ y → g.SameCycle a y
hs :
  ∀ (x : α),
    g • x ≠ x ↔
      Membership.mem (γ := SubMulAction (↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)) α)
        (ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ) x
this :
  ∀ (x : α),
    Membership.mem (γ := SubMulAction (↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)) α)
        (ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ) x →
      ∃ (k : ↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)), x = k • a
x : α
hx :
  Membership.mem (γ := SubMulAction (↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)) α)
    (ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ) x
y : α
hy :
  Membership.mem (γ := SubMulAction (↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)) α)
    (ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ) y
k : ↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)
hk : x = k • a
k' : ↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)
hk' : y = k' • a
h : (k' * k⁻¹) • x = y
⊢ (↑((k' * k⁻¹) •
          Subtype.mk (p := fun (x : α) ↦
            Membership.mem (γ := SubMulAction (↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)) α)
              (ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ) x)
            x hx) :
      α) =
    (↑(Subtype.mk (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction (↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)) α)
            (ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ) x)
          y hy) :
      α)

Tactic:
simp only [SetLike.mk_smul_mk]

Premises used: SetLike.mk_smul_mk