awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
α : Type u_1
inst : Finite α
G : Subgroup (Perm α)
this : Fintype α
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j_1 : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := castLEEmb ⋯
k : Perm α
h : Membership.mem (γ := Subgroup (Perm α)) ⊤ k
x : Fin (Fintype.card α) ↪ α := Equiv.toEmbedding (Equiv.symm (Fintype.equivFinOfCardEq ⋯))
x' : Fin (Fintype.card α - 1) ↪ α := j_1.trans x
g : ↥G
hg' : g • x' = k • x'
hx : ∀ (x : Fin (Fintype.card α) ↪ α), Function.Surjective x.toFun
hgk' :
  ∀ (i : Fin (Fintype.card α)) (hi : (↑i : ℕ) < Fintype.card α - 1),
    Eq (α := α) ((g • x : (a : Fin (Fintype.card α)) → α) i : α) ((k • x : (a : Fin (Fintype.card α)) → α) i : α)
i : Fin (Fintype.card α)
hi : (↑i : ℕ) = Fintype.card α - 1
j : Fin (Fintype.card α)
hxj : Eq (α := α) ((k • x : (a : Fin (Fintype.card α)) → α) j : α) ((g • x : (a : Fin (Fintype.card α)) → α) i : α)
hj : (↑j : ℕ) = Fintype.card α - 1
inr : Eq (α := α) ((k • x : (a : Fin (Fintype.card α)) → α) j : α) ((k • x : (a : Fin (Fintype.card α)) → α) i : α)
⊢ Eq (α := α) ((g • x : (a : Fin (Fintype.card α)) → α) i : α) ((k • x : (a : Fin (Fintype.card α)) → α) i : α)

Tactic:
rw [← hxj]
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
α : Type u_1
inst : Finite α
G : Subgroup (Perm α)
this : Fintype α
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j_1 : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := castLEEmb ⋯
k : Perm α
h : Membership.mem (γ := Subgroup (Perm α)) ⊤ k
x : Fin (Fintype.card α) ↪ α := Equiv.toEmbedding (Equiv.symm (Fintype.equivFinOfCardEq ⋯))
x' : Fin (Fintype.card α - 1) ↪ α := j_1.trans x
g : ↥G
hg' : g • x' = k • x'
hx : ∀ (x : Fin (Fintype.card α) ↪ α), Function.Surjective x.toFun
hgk' :
  ∀ (i : Fin (Fintype.card α)) (hi : (↑i : ℕ) < Fintype.card α - 1),
    Eq (α := α) ((g • x : (a : Fin (Fintype.card α)) → α) i : α) ((k • x : (a : Fin (Fintype.card α)) → α) i : α)
i : Fin (Fintype.card α)
hi : (↑i : ℕ) = Fintype.card α - 1
j : Fin (Fintype.card α)
hxj : Eq (α := α) ((k • x : (a : Fin (Fintype.card α)) → α) j : α) ((g • x : (a : Fin (Fintype.card α)) → α) i : α)
hj : (↑j : ℕ) = Fintype.card α - 1
inr : j = i
⊢ Eq (α := α) ((k • x : (a : Fin (Fintype.card α)) → α) j : α) ((k • x : (a : Fin (Fintype.card α)) → α) i : α)

Tactic:
apply congr_arg

Premises used: congr_arg
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
α : Type u_1
inst : Finite α
G : Subgroup (Perm α)
this : Fintype α
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j_1 : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := castLEEmb ⋯
k : Perm α
h : Membership.mem (γ := Subgroup (Perm α)) ⊤ k
x : Fin (Fintype.card α) ↪ α := Equiv.toEmbedding (Equiv.symm (Fintype.equivFinOfCardEq ⋯))
x' : Fin (Fintype.card α - 1) ↪ α := j_1.trans x
g : ↥G
hg' : g • x' = k • x'
hx : ∀ (x : Fin (Fintype.card α) ↪ α), Function.Surjective x.toFun
hgk' :
  ∀ (i : Fin (Fintype.card α)) (hi : (↑i : ℕ) < Fintype.card α - 1),
    Eq (α := α) ((g • x : (a : Fin (Fintype.card α)) → α) i : α) ((k • x : (a : Fin (Fintype.card α)) → α) i : α)
i : Fin (Fintype.card α)
hi : (↑i : ℕ) = Fintype.card α - 1
j : Fin (Fintype.card α)
hxj : Eq (α := α) ((k • x : (a : Fin (Fintype.card α)) → α) j : α) ((g • x : (a : Fin (Fintype.card α)) → α) i : α)
hj : (↑j : ℕ) = Fintype.card α - 1
inr : (↑j : ℕ) = (↑i : ℕ)
inr₁ : (↑j : ℕ) = Fintype.card α - 1
inr₂ inr₃ : Fintype.card α - 1 = Fintype.card α - 1
⊢ j = i

Tactic:
rw [Fin.ext_iff, hi, hj]

Premises used: Fin.ext_iff
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
α : Type u_1
inst : Finite α
G : Subgroup (Perm α)
this : Fintype α
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := castLEEmb ⋯
k : Perm α
h : Membership.mem (γ := Subgroup (Perm α)) ⊤ k
x : Fin (Fintype.card α) ↪ α := Equiv.toEmbedding (Equiv.symm (Fintype.equivFinOfCardEq ⋯))
x' : Fin (Fintype.card α - 1) ↪ α := j.trans x
g : ↥G
hg' : g • x' = k • x'
hx : ∀ (x : Fin (Fintype.card α) ↪ α), Function.Surjective x.toFun
hgk' :
  ∀ (i : Fin (Fintype.card α)) (hi : (↑i : ℕ) < Fintype.card α - 1),
    Eq (α := α) ((g • x : (a : Fin (Fintype.card α)) → α) i : α) ((k • x : (a : Fin (Fintype.card α)) → α) i : α)
⊢ ∀ (i : Fin (Fintype.card α)),
    Eq (α := α) ((g • x : (a : Fin (Fintype.card α)) → α) i : α) ((k • x : (a : Fin (Fintype.card α)) → α) i : α)

Tactic:
have hgk (i : Fin (Fintype.card α)) : (g • x) i = (k • x) i := by
    rcases lt_or_eq_of_le (le_sub_one_of_lt i.prop) with hi | hi
    · exact hgk' i hi
    · obtain ⟨j, hxj : (k • x) j = (g • x) i⟩ := hx (k • x) ((g • x) i)
      rcases lt_or_eq_of_le (le_sub_one_of_lt j.prop) with hj | hj
      · suffices i = j by
          rw [← this, ← hi] at hj
          exact (lt_irrefl _ hj).elim
        apply EmbeddingLike.injective (g • x)
        rw [hgk' j hj, hxj]
      · rw [← hxj]
        apply congr_arg
        rw [Fin.ext_iff, hi, hj]
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
α : Type u_1
inst : Finite α
G : Subgroup (Perm α)
this : Fintype α
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := castLEEmb ⋯
k : Perm α
h : Membership.mem (γ := Subgroup (Perm α)) ⊤ k
x : Fin (Fintype.card α) ↪ α := Equiv.toEmbedding (Equiv.symm (Fintype.equivFinOfCardEq ⋯))
x' : Fin (Fintype.card α - 1) ↪ α := j.trans x
g : ↥G
hg' : g • x' = k • x'
hx : ∀ (x : Fin (Fintype.card α) ↪ α), Function.Surjective x.toFun
hgk' :
  ∀ (i : Fin (Fintype.card α)) (hi : (↑i : ℕ) < Fintype.card α - 1),
    Eq (α := α) ((g • x : (a : Fin (Fintype.card α)) → α) i : α) ((k • x : (a : Fin (Fintype.card α)) → α) i : α)
hgk :
  ∀ (i : Fin (Fintype.card α)),
    Eq (α := α) ((g • x : (a : Fin (Fintype.card α)) → α) i : α) ((k • x : (a : Fin (Fintype.card α)) → α) i : α)
H : ∀ (a : α), Eq (α := α) ((k : (a : α) → α) a : α) (((↑g : Perm α) : (a : α) → α) a : α)
⊢ k = (↑g : Perm α)

Tactic:
ext a
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
α : Type u_1
inst : Finite α
G : Subgroup (Perm α)
this : Fintype α
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := castLEEmb ⋯
k : Perm α
h : Membership.mem (γ := Subgroup (Perm α)) ⊤ k
x : Fin (Fintype.card α) ↪ α := Equiv.toEmbedding (Equiv.symm (Fintype.equivFinOfCardEq ⋯))
x' : Fin (Fintype.card α - 1) ↪ α := j.trans x
g : ↥G
hg' : g • x' = k • x'
hx : ∀ (x : Fin (Fintype.card α) ↪ α), Function.Surjective x.toFun
hgk' :
  ∀ (i : Fin (Fintype.card α)) (hi : (↑i : ℕ) < Fintype.card α - 1),
    Eq (α := α) ((g • x : (a : Fin (Fintype.card α)) → α) i : α) ((k • x : (a : Fin (Fintype.card α)) → α) i : α)
hgk :
  ∀ (i : Fin (Fintype.card α)),
    Eq (α := α) ((g • x : (a : Fin (Fintype.card α)) → α) i : α) ((k • x : (a : Fin (Fintype.card α)) → α) i : α)
a : α
H :
  ∀ (i : Fin (Fintype.card α)),
    Eq (α := α) ((k : (a : α) → α) (x.toFun i) : α) (((↑g : Perm α) : (a : α) → α) (x.toFun i) : α)
⊢ Eq (α := α) ((k : (a : α) → α) a : α) (((↑g : Perm α) : (a : α) → α) a : α)

Tactic:
obtain ⟨i, rfl⟩ := (hx x) a

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
α : Type u_1
inst : Finite α
G : Subgroup (Perm α)
this : Fintype α
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := castLEEmb ⋯
k : Perm α
h : Membership.mem (γ := Subgroup (Perm α)) ⊤ k
x : Fin (Fintype.card α) ↪ α := Equiv.toEmbedding (Equiv.symm (Fintype.equivFinOfCardEq ⋯))
x' : Fin (Fintype.card α - 1) ↪ α := j.trans x
g : ↥G
hg' : g • x' = k • x'
hx : ∀ (x : Fin (Fintype.card α) ↪ α), Function.Surjective x.toFun
hgk' :
  ∀ (i : Fin (Fintype.card α)) (hi : (↑i : ℕ) < Fintype.card α - 1),
    Eq (α := α) ((g • x : (a : Fin (Fintype.card α)) → α) i : α) ((k • x : (a : Fin (Fintype.card α)) → α) i : α)
hgk :
  ∀ (i : Fin (Fintype.card α)),
    Eq (α := α) ((g • x : (a : Fin (Fintype.card α)) → α) i : α) ((k • x : (a : Fin (Fintype.card α)) → α) i : α)
i : Fin (Fintype.card α)
⊢ Eq (α := α) ((g • x : (a : Fin (Fintype.card α)) → α) i : α) ((k • x : (a : Fin (Fintype.card α)) → α) i : α)

Tactic:
specialize hgk i
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
α : Type u_1
inst : Finite α
G : Subgroup (Perm α)
this : Fintype α
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := castLEEmb ⋯
k : Perm α
h : Membership.mem (γ := Subgroup (Perm α)) ⊤ k
x : Fin (Fintype.card α) ↪ α := Equiv.toEmbedding (Equiv.symm (Fintype.equivFinOfCardEq ⋯))
x' : Fin (Fintype.card α - 1) ↪ α := j.trans x
g : ↥G
hg' : g • x' = k • x'
hx : ∀ (x : Fin (Fintype.card α) ↪ α), Function.Surjective x.toFun
hgk' :
  ∀ (i : Fin (Fintype.card α)) (hi : (↑i : ℕ) < Fintype.card α - 1),
    Eq (α := α) ((g • x : (a : Fin (Fintype.card α)) → α) i : α) ((k • x : (a : Fin (Fintype.card α)) → α) i : α)
i : Fin (Fintype.card α)
hgk :
  HSMul.hSMul (β := α) g ((x : (a : Fin (Fintype.card α)) → α) i : α) =
    (k : (a : α) → α) ((x : (a : Fin (Fintype.card α)) → α) i : α)
⊢ Eq (α := α) ((k : (a : α) → α) (x.toFun i) : α) (((↑g : Perm α) : (a : α) → α) (x.toFun i) : α)

Tactic:
simp [← hgk, Subgroup.smul_def, Perm.smul_def]

Premises used: Equiv.Perm.smul_def, Subgroup.smul_def
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
inl : ∀ (h2 : Nat.card α < 2), IsMultiplyPretransitive (↥(alternatingGroup α)) α (Nat.card α - 2)
inr : ∀ (h2 : 2 ≤ Nat.card α), IsMultiplyPretransitive (↥(alternatingGroup α)) α (Nat.card α - 2)
⊢ IsMultiplyPretransitive (↥(alternatingGroup α)) α (Nat.card α - 2)

Tactic:
rcases lt_or_ge (Nat.card α) 2 with h2 | h2

Premises used: Nat.card, lt_or_ge, OfNat.ofNat
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h2 : Nat.card α < 2
inl : IsMultiplyPretransitive (↥(alternatingGroup α)) α 0
⊢ IsMultiplyPretransitive (↥(alternatingGroup α)) α (Nat.card α - 2)

Tactic:
rw [Nat.sub_eq_zero_of_le (le_of_lt h2)]

Premises used: le_of_lt, Nat.sub_eq_zero_of_le
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h2 : Nat.card α < 2
⊢ IsMultiplyPretransitive (↥(alternatingGroup α)) α 0

Tactic:
apply is_zero_pretransitive

Premises used: MulAction.is_zero_pretransitive
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h2 : 2 ≤ Nat.card α
⊢ Nat.card α - 2 ≤ Nat.card α

Tactic:
have h2le : Nat.card α - 2 ≤ Nat.card α := sub_le (Nat.card α) 2
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h2 : 2 ≤ Nat.card α
h2le : Nat.card α - 2 ≤ Nat.card α
⊢ IsMultiplyPretransitive (Equiv.Perm α) α (Nat.card α)

Tactic:
have := Equiv.Perm.isMultiplyPretransitive α (Nat.card α)
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h2 : 2 ≤ Nat.card α
h2le : Nat.card α - 2 ≤ Nat.card α
this : IsMultiplyPretransitive (Equiv.Perm α) α (Nat.card α)
⊢ IsMultiplyPretransitive (Equiv.Perm α) α (Nat.card α - 2)

Tactic:
have : IsMultiplyPretransitive (Equiv.Perm α) α (Nat.card α - 2) :=
    MulAction.isMultiplyPretransitive_of_le h2le le_rfl
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h2 : 2 ≤ Nat.card α
h2le : Nat.card α - 2 ≤ Nat.card α
this_1 : IsMultiplyPretransitive (Equiv.Perm α) α (Nat.card α)
this : IsMultiplyPretransitive (Equiv.Perm α) α (Nat.card α - 2)
⊢ IsMultiplyPretransitive (↥(alternatingGroup α)) α (Nat.card α - 2)

Tactic:
⟨fun x y ↦ ?_⟩

Premises used: MulAction.IsPretransitive.mk
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h2 : 2 ≤ Nat.card α
h2le : Nat.card α - 2 ≤ Nat.card α
this_1 : IsMultiplyPretransitive (Equiv.Perm α) α (Nat.card α)
this : IsMultiplyPretransitive (Equiv.Perm α) α (Nat.card α - 2)
inr : ∀ (x y : Fin (Nat.card α - 2) ↪ α), ∃ (g : ↥(alternatingGroup α)), g • x = y
⊢ IsMultiplyPretransitive (↥(alternatingGroup α)) α (Nat.card α - 2)

Tactic:
refine ⟨fun x y ↦ ?_⟩
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h2 : 2 ≤ Nat.card α
h2le : Nat.card α - 2 ≤ Nat.card α
this_1 : IsMultiplyPretransitive (Equiv.Perm α) α (Nat.card α)
this : IsMultiplyPretransitive (Equiv.Perm α) α (Nat.card α - 2)
x y : Fin (Nat.card α - 2) ↪ α
inr : ∀ (g : Equiv.Perm α) (hg : g • x = y), ∃ (g : ↥(alternatingGroup α)), g • x = y
⊢ ∃ (g : ↥(alternatingGroup α)), g • x = y

Tactic:
obtain ⟨g, hg⟩ := exists_smul_eq (Equiv.Perm α) x y

Premises used: Equiv.Perm, MulAction.exists_smul_eq
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h2 : 2 ≤ Nat.card α
h2le : Nat.card α - 2 ≤ Nat.card α
this_1 : IsMultiplyPretransitive (Equiv.Perm α) α (Nat.card α)
this : IsMultiplyPretransitive (Equiv.Perm α) α (Nat.card α - 2)
x y : Fin (Nat.card α - 2) ↪ α
g : Equiv.Perm α
hg : g • x = y
inr :
  ∀ (h : Eq (α := ℤˣ) (((Equiv.Perm.sign : Equiv.Perm α →* ℤˣ) : (a : Equiv.Perm α) → ℤˣ) g : ℤˣ) (1 : ℤˣ)),
    ∃ (g : ↥(alternatingGroup α)), g • x = y
inr₁ :
  ∀ (h : Eq (α := ℤˣ) (((Equiv.Perm.sign : Equiv.Perm α →* ℤˣ) : (a : Equiv.Perm α) → ℤˣ) g : ℤˣ) (-1 : ℤˣ)),
    ∃ (g : ↥(alternatingGroup α)), g • x = y
⊢ ∃ (g : ↥(alternatingGroup α)), g • x = y

Tactic:
rcases Int.units_eq_one_or (Equiv.Perm.sign g) with h | h

Premises used: Equiv.Perm.sign, Int.units_eq_one_or, DFunLike.coe
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h2 : 2 ≤ Nat.card α
h2le : Nat.card α - 2 ≤ Nat.card α
this_1 : IsMultiplyPretransitive (Equiv.Perm α) α (Nat.card α)
this : IsMultiplyPretransitive (Equiv.Perm α) α (Nat.card α - 2)
x y : Fin (Nat.card α - 2) ↪ α
g : Equiv.Perm α
hg : g • x = y
h : Eq (α := ℤˣ) (((Equiv.Perm.sign : Equiv.Perm α →* ℤˣ) : (a : Equiv.Perm α) → ℤˣ) g : ℤˣ) (1 : ℤˣ)
⊢ ∃ (g : ↥(alternatingGroup α)), g • x = y

Tactic:
⟨⟨g, h⟩, hg⟩

Premises used: Subtype.mk, Exists.intro
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h2 : 2 ≤ Nat.card α
h2le : Nat.card α - 2 ≤ Nat.card α
this_1 : IsMultiplyPretransitive (Equiv.Perm α) α (Nat.card α)
this : IsMultiplyPretransitive (Equiv.Perm α) α (Nat.card α - 2)
x y : Fin (Nat.card α - 2) ↪ α
g : Equiv.Perm α
hg : g • x = y
h : Eq (α := ℤˣ) (((Equiv.Perm.sign : Equiv.Perm α →* ℤˣ) : (a : Equiv.Perm α) → ℤˣ) g : ℤˣ) (1 : ℤˣ)
⊢ ∃ (g : ↥(alternatingGroup α)), g • x = y

Tactic:
exact ⟨⟨g, h⟩, hg⟩
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h2 : 2 ≤ Nat.card α
h2le : Nat.card α - 2 ≤ Nat.card α
this_1 : IsMultiplyPretransitive (Equiv.Perm α) α (Nat.card α)
this : IsMultiplyPretransitive (Equiv.Perm α) α (Nat.card α - 2)
x y : Fin (Nat.card α - 2) ↪ α
g : Equiv.Perm α
hg : g • x = y
h : Eq (α := ℤˣ) (((Equiv.Perm.sign : Equiv.Perm α →* ℤˣ) : (a : Equiv.Perm α) → ℤˣ) g : ℤˣ) (-1 : ℤˣ)
⊢ Function.Injective (α := Fin (Nat.card α - 2)) (β := α) (⇑x : (a : Fin (Nat.card α - 2)) → α)

Tactic:
x.2

Premises used: Function.Embedding.inj'
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h2 : 2 ≤ Nat.card α
h2le : Nat.card α - 2 ≤ Nat.card α
this_1 : IsMultiplyPretransitive (Equiv.Perm α) α (Nat.card α)
this : IsMultiplyPretransitive (Equiv.Perm α) α (Nat.card α - 2)
x y : Fin (Nat.card α - 2) ↪ α
g : Equiv.Perm α
hg : g • x = y
h : Eq (α := ℤˣ) (((Equiv.Perm.sign : Equiv.Perm α →* ℤˣ) : (a : Equiv.Perm α) → ℤˣ) g : ℤˣ) (-1 : ℤˣ)
⊢ Function.Injective (α := Fin (Nat.card α - 2)) (β := α) (⇑x : (a : Fin (Nat.card α - 2)) → α)

Tactic:
exact x.2

Premises used: Function.Embedding.inj'
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h2 : 2 ≤ Nat.card α
h2le : Nat.card α - 2 ≤ Nat.card α
this_1 : IsMultiplyPretransitive (Equiv.Perm α) α (Nat.card α)
this : IsMultiplyPretransitive (Equiv.Perm α) α (Nat.card α - 2)
x y : Fin (Nat.card α - 2) ↪ α
g : Equiv.Perm α
hg : g • x = y
h : Eq (α := ℤˣ) (((Equiv.Perm.sign : Equiv.Perm α →* ℤˣ) : (a : Equiv.Perm α) → ℤˣ) g : ℤˣ) (-1 : ℤˣ)
rw :
  Fintype.card α -
      Finset.card (α := α)
        (Finset.image (α := Fin (Nat.card α - 2)) (⇑x : (a : Fin (Nat.card α - 2)) → α) Finset.univ) =
    2
rw₁ : Fintype.card α - Finset.card (α := Fin (Nat.card α - 2)) Finset.univ = 2
rw₂ : Fintype.card α - Fintype.card (Fin (Nat.card α - 2)) = 2
rw₃ : Nat.card α - Fintype.card (Fin (Nat.card α - 2)) = 2
rw₄ : Nat.card α - (Nat.card α - 2) = 2
rw₅ rw₆ : Eq (α := ℕ) 2 2
⊢ Finset.card (α := α) (Finset.image (α := Fin (Nat.card α - 2)) (⇑x : (a : Fin (Nat.card α - 2)) → α) Finset.univ)ᶜ = 2

Tactic:
rw [Finset.card_compl, Finset.univ.card_image_of_injective (by exact x.2), Finset.card_univ,
        ← Nat.card_eq_fintype_card, Fintype.card_fin, tsub_tsub_cancel_of_le h2]

Premises used: Finset.card_univ, Fintype.card_fin, Finset.univ, Finset.card_compl, Finset.card_image_of_injective, tsub_tsub_cancel_of_le, Nat.card_eq_fintype_card
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h2 : 2 ≤ Nat.card α
h2le : Nat.card α - 2 ≤ Nat.card α
this_1 : IsMultiplyPretransitive (Equiv.Perm α) α (Nat.card α)
this : IsMultiplyPretransitive (Equiv.Perm α) α (Nat.card α - 2)
x y : Fin (Nat.card α - 2) ↪ α
g : Equiv.Perm α
hg : g • x = y
h : Eq (α := ℤˣ) (((Equiv.Perm.sign : Equiv.Perm α →* ℤˣ) : (a : Equiv.Perm α) → ℤˣ) g : ℤˣ) (-1 : ℤˣ)
⊢ Finset.card (α := α) (Finset.image (α := Fin (Nat.card α - 2)) (⇑x : (a : Fin (Nat.card α - 2)) → α) Finset.univ)ᶜ = 2

Tactic:
have : (Finset.univ.image x)ᶜ.card = 2 := by
      rw [Finset.card_compl, Finset.univ.card_image_of_injective (by exact x.2), Finset.card_univ,
        ← Nat.card_eq_fintype_card, Fintype.card_fin, tsub_tsub_cancel_of_le h2]
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h2 : 2 ≤ Nat.card α
h2le : Nat.card α - 2 ≤ Nat.card α
this_1 : IsMultiplyPretransitive (Equiv.Perm α) α (Nat.card α)
this_2 : IsMultiplyPretransitive (Equiv.Perm α) α (Nat.card α - 2)
x y : Fin (Nat.card α - 2) ↪ α
g : Equiv.Perm α
hg : g • x = y
h : Eq (α := ℤˣ) (((Equiv.Perm.sign : Equiv.Perm α →* ℤˣ) : (a : Equiv.Perm α) → ℤˣ) g : ℤˣ) (-1 : ℤˣ)
this :
  Finset.card (α := α) (Finset.image (α := Fin (Nat.card α - 2)) (⇑x : (a : Fin (Nat.card α - 2)) → α) Finset.univ)ᶜ = 2
inr :
  ∀ (a b : α) (hab : a ≠ b)
    (hs :
      Eq (α := Finset α) (Finset.image (α := Fin (Nat.card α - 2)) (⇑x : (a : Fin (Nat.card α - 2)) → α) Finset.univ)ᶜ
        {a, b}),
    ∃ (g : ↥(alternatingGroup α)), g • x = y
⊢ ∃ (g : ↥(alternatingGroup α)), g • x = y

Tactic:
obtain ⟨a, b, hab, hs⟩ := Finset.card_eq_two.mp this

Premises used: Finset.card_eq_two, Iff.mp
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h2 : 2 ≤ Nat.card α
h2le : Nat.card α - 2 ≤ Nat.card α
this_1 : IsMultiplyPretransitive (Equiv.Perm α) α (Nat.card α)
this_2 : IsMultiplyPretransitive (Equiv.Perm α) α (Nat.card α - 2)
x y : Fin (Nat.card α - 2) ↪ α
g : Equiv.Perm α
hg : g • x = y
h : Eq (α := ℤˣ) (((Equiv.Perm.sign : Equiv.Perm α →* ℤˣ) : (a : Equiv.Perm α) → ℤˣ) g : ℤˣ) (-1 : ℤˣ)
this :
  Finset.card (α := α) (Finset.image (α := Fin (Nat.card α - 2)) (⇑x : (a : Fin (Nat.card α - 2)) → α) Finset.univ)ᶜ = 2
a b : α
hab : a ≠ b
hs :
  Eq (α := Finset α) (Finset.image (α := Fin (Nat.card α - 2)) (⇑x : (a : Fin (Nat.card α - 2)) → α) Finset.univ)ᶜ
    {a, b}
⊢ g * Equiv.swap a b ∈ alternatingGroup α

Tactic:
simp [h, hab]
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h2 : 2 ≤ Nat.card α
h2le : Nat.card α - 2 ≤ Nat.card α
this_1 : IsMultiplyPretransitive (Equiv.Perm α) α (Nat.card α)
this_2 : IsMultiplyPretransitive (Equiv.Perm α) α (Nat.card α - 2)
x y : Fin (Nat.card α - 2) ↪ α
g : Equiv.Perm α
hg : g • x = y
h : Eq (α := ℤˣ) (((Equiv.Perm.sign : Equiv.Perm α →* ℤˣ) : (a : Equiv.Perm α) → ℤˣ) g : ℤˣ) (-1 : ℤˣ)
this :
  Finset.card (α := α) (Finset.image (α := Fin (Nat.card α - 2)) (⇑x : (a : Fin (Nat.card α - 2)) → α) Finset.univ)ᶜ = 2
a b : α
hab : a ≠ b
hs :
  Eq (α := Finset α) (Finset.image (α := Fin (Nat.card α - 2)) (⇑x : (a : Fin (Nat.card α - 2)) → α) Finset.univ)ᶜ
    {a, b}
inr :
  ∀ (i : Fin (Nat.card α - 2)),
    Eq (α := α)
      ((HSMul.hSMul (α := ↥(alternatingGroup α))
              (Subtype.mk (p := fun (x : Equiv.Perm α) ↦ x ∈ alternatingGroup α) (g * Equiv.swap a b) ⋯) x :
            (a : Fin (Nat.card α - 2)) → α)
          i :
        α)
      ((y : (a : Fin (Nat.card α - 2)) → α) i : α)
⊢ HSMul.hSMul (α := ↥(alternatingGroup α))
      (Subtype.mk (p := fun (x : Equiv.Perm α) ↦ x ∈ alternatingGroup α) (g * Equiv.swap a b) ⋯) x =
    y

Tactic:
ext i
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h2 : 2 ≤ Nat.card α
h2le : Nat.card α - 2 ≤ Nat.card α
this_1 : IsMultiplyPretransitive (Equiv.Perm α) α (Nat.card α)
this_2 : IsMultiplyPretransitive (Equiv.Perm α) α (Nat.card α - 2)
x y : Fin (Nat.card α - 2) ↪ α
g : Equiv.Perm α
hg : g • x = y
h : Eq (α := ℤˣ) (((Equiv.Perm.sign : Equiv.Perm α →* ℤˣ) : (a : Equiv.Perm α) → ℤˣ) g : ℤˣ) (-1 : ℤˣ)
this :
  Finset.card (α := α) (Finset.image (α := Fin (Nat.card α - 2)) (⇑x : (a : Fin (Nat.card α - 2)) → α) Finset.univ)ᶜ = 2
a b : α
hab : a ≠ b
hs :
  Eq (α := Finset α) (Finset.image (α := Fin (Nat.card α - 2)) (⇑x : (a : Fin (Nat.card α - 2)) → α) Finset.univ)ᶜ
    {a, b}
i : Fin (Nat.card α - 2)
⊢ Membership.mem (α := α) (γ := Finset α)
    (Finset.image (α := Fin (Nat.card α - 2)) (⇑x : (a : Fin (Nat.card α - 2)) → α) Finset.univ)
    ((x : (a : Fin (Nat.card α - 2)) → α) i : α)

Tactic:
have h : x i ∈ Finset.univ.image x := Finset.mem_image.mpr ⟨i, Finset.mem_univ i, rfl⟩
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h2 : 2 ≤ Nat.card α
h2le : Nat.card α - 2 ≤ Nat.card α
this_1 : IsMultiplyPretransitive (Equiv.Perm α) α (Nat.card α)
this_2 : IsMultiplyPretransitive (Equiv.Perm α) α (Nat.card α - 2)
x y : Fin (Nat.card α - 2) ↪ α
g : Equiv.Perm α
hg : g • x = y
h_1 : Eq (α := ℤˣ) (((Equiv.Perm.sign : Equiv.Perm α →* ℤˣ) : (a : Equiv.Perm α) → ℤˣ) g : ℤˣ) (-1 : ℤˣ)
this :
  Finset.card (α := α) (Finset.image (α := Fin (Nat.card α - 2)) (⇑x : (a : Fin (Nat.card α - 2)) → α) Finset.univ)ᶜ = 2
a b : α
hab : a ≠ b
hs :
  Eq (α := Finset α) (Finset.image (α := Fin (Nat.card α - 2)) (⇑x : (a : Fin (Nat.card α - 2)) → α) Finset.univ)ᶜ
    {a, b}
i : Fin (Nat.card α - 2)
h :
  Membership.mem (α := α) (γ := Finset α)
    (Finset.image (α := Fin (Nat.card α - 2)) (⇑x : (a : Fin (Nat.card α - 2)) → α) Finset.univ)
    ((x : (a : Fin (Nat.card α - 2)) → α) i : α)
⊢ ¬(x : (a : Fin (Nat.card α - 2)) → α) i = a ∧ ¬(x : (a : Fin (Nat.card α - 2)) → α) i = b

Tactic:
rw [← Finset.notMem_compl, hs, Finset.mem_insert, Finset.mem_singleton, not_or] at h

Premises used: Finset.mem_singleton, Finset.mem_insert, not_or, Finset.notMem_compl