awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
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 α
h2 : IsMultiplyPretransitive K α 2
hn : ¬n ≤ 2
neg : ¬Nonempty.{u_1 + 1} (Fin n ↪ α)
neg₁ : ¬Fintype.card (Fin n) ≤ Fintype.card α
⊢ IsEmpty.{max 1 (u_1 + 1)} (Fin n ↪ α)
have neg₂ : ¬n ≤ Fintype.card α
Tactic: rwa [← not_nonempty_iff, Function.Embedding.nonempty_iff_card_le, Fintype.card_fin,
        ← Nat.card_eq_fintype_card, hα]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
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 α
h2 : IsMultiplyPretransitive K α 2
hn : ¬n ≤ 2
neg : ¬Nonempty.{u_1 + 1} (Fin n ↪ α)
neg₁ : ¬Fintype.card (Fin n) ≤ Fintype.card α
neg₂ : ¬n ≤ Fintype.card α
⊢ IsEmpty.{max 1 (u_1 + 1)} (Fin n ↪ α)
have neg₃ : ¬n ≤ Nat.card α
Tactic: rwa [← not_nonempty_iff, Function.Embedding.nonempty_iff_card_le, Fintype.card_fin,
        ← Nat.card_eq_fintype_card, hα]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
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 α
⊢ IsMultiplyPretransitive K α n
have suffices : IsMultiplyPretransitive K α 2
Tactic: suffices h2 : IsMultiplyPretransitive K α 2 by
    by_cases hn : n ≤ 2
    · apply MulAction.isMultiplyPretransitive_of_le' hn
      simp [← hα]
    · suffices (IsEmpty (Fin n ↪ α)) by infer_instance
      rwa [← not_nonempty_iff, Function.Embedding.nonempty_iff_card_le, Fintype.card_fin,
        ← Nat.card_eq_fintype_card, hα]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (hypothesis)
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' := ⋯ }
⊢ IsMultiplyPretransitive K α 2
have hf : Function.Bijective (α := α) (β := α) (⇑f : (a : α) → α)
Tactic: have hf : Function.Bijective f := Function.bijective_id
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
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 : α) → α)
this : Function.Surjective.{u_2 + 1, u_1 + 1} (α := K) (β := Perm α) (⇑φ : (a : K) → Perm α)
⊢ IsPretransitive.{u_2, u_1} K (Fin 2 ↪ α)
have rw : IsPretransitive.{u_1, u_1} (Perm α) (Fin (Nat.card α) ↪ α)
Tactic: rw [IsPretransitive.of_embedding_congr this hf (n := Fin 2), ← hα]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
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 : α) → α)
⊢ IsMultiplyPretransitive K α 2
have suffices : Function.Surjective.{u_2 + 1, u_1 + 1} (α := K) (β := Perm α) (⇑φ : (a : K) → Perm α)
Tactic: suffices Function.Surjective φ by
    unfold IsMultiplyPretransitive
    rw [IsPretransitive.of_embedding_congr this hf (n := Fin 2), ← hα]
    apply Perm.isMultiplyPretransitive
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
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 : α) → α)
⊢ Function.Surjective.{u_2 + 1, u_1 + 1} (α := K) (β := Perm α) (⇑φ : (a : K) → Perm α)
have rw : φ.range = ⊤
Tactic: rw [← MonoidHom.range_eq_top]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
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 : α) → α)
⊢ φ.range = ⊤
have h : Nat.card.{u_1} ↥φ.range = Nat.card.{u_1} (Perm α)
Tactic: apply Subgroup.eq_top_of_card_eq
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
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 : α) → α)
⊢ Nat.card.{u_1} ↥φ.range = Nat.card.{u_1} (Perm α)
have h : Nat.card.{u_1} (Perm α) ≤ Nat.card.{u_1} ↥φ.range
Tactic: apply le_antisymm (card_le_card_group φ.range)
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
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 : α) → α)
⊢ Nat.card.{u_1} (Perm α) ≤ Nat.card.{u_1} ↥φ.range
have h : 2 ≤ Nat.card.{u_1} ↥φ.range
Tactic: simp only [Nat.card_perm, hα, Nat.factorial_two]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
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 : α) → α)
⊢ 2 ≤ Nat.card.{u_1} ↥φ.range
have h : ∀ (H : ¬2 ≤ Nat.card.{u_1} ↥φ.range), False
Tactic: by_contra H
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (hypothesis)
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
⊢ False
have H₁ : Subsingleton.{u_1 + 1} ↥φ.range
Tactic: simp only [not_le, Nat.lt_succ_iff, Finite.card_le_one_iff_subsingleton] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
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
⊢ False
have h : fixedPoints K α = _root_.Set.univ
Tactic: apply hK
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
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
⊢ fixedPoints K α = _root_.Set.univ
have h : _root_.Set.univ ⊆ fixedPoints K α
Tactic: apply Set.eq_univ_of_univ_subset
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
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 α)
| a
have rw : HSMul.hSMul.{u_2, u_1, u_1} (α := K) 1 a
Tactic: rw [← one_smul K a]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
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 α)
⊢ g • a = a
have conv_rhs : g • a = HSMul.hSMul.{u_2, u_1, u_1} (α := K) 1 a
Tactic: conv_rhs => rw [← one_smul K a]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
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 α)
⊢ g • a = HSMul.hSMul.{u_2, u_1, u_1} (α := K) 1 a
have 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 : α)
Tactic: simp only [← toPerm_apply, ← toPermHom_apply K α g]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
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
⊢ g • a = a
have h : Eq.{u_1 + 1} (α := Perm α) ((φ : (a : K) → Perm α) g : Perm α) ((φ : (a : K) → Perm α) 1 : Perm α)
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
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
Goal:
α : Type u_1
G : Subgroup (Perm α)
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
hgc : g.IsCycle
hg : g ∈ G
⊢ IsPretransitive.{u_1, u_1} ↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ) ↥(ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ)
have 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 α)ᶜ)
Tactic: obtain ⟨a, _, hgc⟩ := hgc
Cleared hypotheses: hgc
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (hypothesis)
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
⊢ IsPretransitive.{u_1, u_1} ↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ) ↥(ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ)
have hs : ∀ (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]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
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
⊢ IsPretransitive.{u_1, u_1} ↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ) ↥(ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ)
have rw : ∀ (x y : ↥(ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ)),
  ∃ (g_1 : ↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)), g_1 • x = y
Tactic: rw [isPretransitive_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
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
⊢ ∃ (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
have 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
Tactic: obtain ⟨k, hk⟩ := this x hx
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
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
⊢ ∃ (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
have 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
Tactic: obtain ⟨k', hk'⟩ := this y hy
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
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
⊢ ∃ (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
have 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
Tactic: use k' * k⁻¹
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
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
⊢ (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
have 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) :
    α)
Tactic: rw [← SetLike.coe_eq_coe]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
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
⊢ (↑((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) :
      α)
have h : (k' * k⁻¹) • x = y
Tactic: simp only [SetLike.mk_smul_mk]