awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
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
⊢ Eq (α := α) ((g • x : (a : Fin (Fintype.card α)) → α) i : α) ((g • x : (a : Fin (Fintype.card α)) → α) j : α)
have inr : Eq (α := α) ((g • x : (a : Fin (Fintype.card α)) → α) i : α) ((k • x : (a : Fin (Fintype.card α)) → α) j : α)
Tactic: rw [hgk' j hj, hxj]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
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 (α := α) ((g • x : (a : Fin (Fintype.card α)) → α) i : α) ((k • x : (a : Fin (Fintype.card α)) → α) j : α)
⊢ Eq (α := α) ((g • x : (a : Fin (Fintype.card α)) → α) i : α) ((g • x : (a : Fin (Fintype.card α)) → α) j : α)
have inr₁ : Eq (α := α) ((g • x : (a : Fin (Fintype.card α)) → α) i : α) ((g • x : (a : Fin (Fintype.card α)) → α) i : α)
Tactic: rw [hgk' j hj, hxj]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
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
⊢ Eq (α := α) ((g • x : (a : Fin (Fintype.card α)) → α) i : α) ((k • x : (a : Fin (Fintype.card α)) → α) i : α)
have inr : Eq (α := α) ((k • x : (a : Fin (Fintype.card α)) → α) j : α) ((k • x : (a : Fin (Fintype.card α)) → α) i : α)
Tactic: rw [← hxj]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
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
⊢ Eq (α := α) ((k • x : (a : Fin (Fintype.card α)) → α) j : α) ((k • x : (a : Fin (Fintype.card α)) → α) i : α)
have inr : j = i
Tactic: apply congr_arg
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
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
⊢ j = i
have inr : (↑j : ℕ) = (↑i : ℕ)
Tactic: rw [Fin.ext_iff, hi, hj]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
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
⊢ j = i
have inr₂ : Fintype.card α - 1 = Fintype.card α - 1
Tactic: rw [Fin.ext_iff, hi, hj]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (hypothesis)
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 : α)
⊢ k = (↑g : Perm α)
have hgk : ∀ (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]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
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 : α)
⊢ k = (↑g : Perm α)
have H : ∀ (a : α), Eq (α := α) ((k : (a : α) → α) a : α) (((↑g : Perm α) : (a : α) → α) a : α)
Tactic: ext a
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
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 : α
⊢ Eq (α := α) ((k : (a : α) → α) a : α) (((↑g : Perm α) : (a : α) → α) a : α)
have H : ∀ (i : Fin (Fintype.card α)),
  Eq (α := α) ((k : (a : α) → α) (x.toFun i) : α) (((↑g : Perm α) : (a : α) → α) (x.toFun i) : α)
Tactic: obtain ⟨i, rfl⟩ := (hx x) a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (hypothesis)
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 (α := α) ((k : (a : α) → α) (x.toFun i) : α) (((↑g : Perm α) : (a : α) → α) (x.toFun i) : α)
have hgk₁ : Eq (α := α) ((g • x : (a : Fin (Fintype.card α)) → α) i : α) ((k • x : (a : Fin (Fintype.card α)) → α) i : α)
Tactic: specialize hgk i
Cleared hypotheses: hgk
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
⊢ IsMultiplyPretransitive (↥(alternatingGroup α)) α (Nat.card α - 2)
have inl : ∀ (h2 : Nat.card α < 2), IsMultiplyPretransitive (↥(alternatingGroup α)) α (Nat.card α - 2)
Tactic: rcases lt_or_ge (Nat.card α) 2 with h2 | h2
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
inl : ∀ (h2 : Nat.card α < 2), IsMultiplyPretransitive (↥(alternatingGroup α)) α (Nat.card α - 2)
⊢ IsMultiplyPretransitive (↥(alternatingGroup α)) α (Nat.card α - 2)
have inr : ∀ (h2 : 2 ≤ Nat.card α), IsMultiplyPretransitive (↥(alternatingGroup α)) α (Nat.card α - 2)
Tactic: rcases lt_or_ge (Nat.card α) 2 with h2 | h2
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h2 : Nat.card α < 2
⊢ IsMultiplyPretransitive (↥(alternatingGroup α)) α (Nat.card α - 2)
have inl : IsMultiplyPretransitive (↥(alternatingGroup α)) α 0
Tactic: rw [Nat.sub_eq_zero_of_le (le_of_lt h2)]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h2 : 2 ≤ Nat.card α
⊢ IsMultiplyPretransitive (↥(alternatingGroup α)) α (Nat.card α - 2)
have h2le : Nat.card α - 2 ≤ Nat.card α
Tactic: have h2le : Nat.card α - 2 ≤ Nat.card α := sub_le (Nat.card α) 2
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h2 : 2 ≤ Nat.card α
h2le : Nat.card α - 2 ≤ Nat.card α
⊢ IsMultiplyPretransitive (↥(alternatingGroup α)) α (Nat.card α - 2)
have this : IsMultiplyPretransitive (Equiv.Perm α) α (Nat.card α)
Tactic: have := Equiv.Perm.isMultiplyPretransitive α (Nat.card α)
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (hypothesis)
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 (↥(alternatingGroup α)) α (Nat.card α - 2)
have this₁ : IsMultiplyPretransitive (Equiv.Perm α) α (Nat.card α - 2)
Tactic: have : IsMultiplyPretransitive (Equiv.Perm α) α (Nat.card α - 2) :=
    MulAction.isMultiplyPretransitive_of_le h2le le_rfl
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
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)
have inr : ∀ (x y : Fin (Nat.card α - 2) ↪ α), ∃ (g : ↥(alternatingGroup α)), g • x = y
Tactic: refine ⟨fun x y ↦ ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
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 : ↥(alternatingGroup α)), g • x = y
have inr : ∀ (g : Equiv.Perm α) (hg : g • x = y), ∃ (g : ↥(alternatingGroup α)), g • x = y
Tactic: obtain ⟨g, hg⟩ := exists_smul_eq (Equiv.Perm α) x y
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
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
⊢ ∃ (g : ↥(alternatingGroup α)), g • x = y
have inr : ∀ (h : Eq (α := ℤˣ) (((Equiv.Perm.sign : Equiv.Perm α →* ℤˣ) : (a : Equiv.Perm α) → ℤˣ) g : ℤˣ) (1 : ℤˣ)),
  ∃ (g : ↥(alternatingGroup α)), g • x = y
Tactic: rcases Int.units_eq_one_or (Equiv.Perm.sign g) with h | h
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
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
⊢ ∃ (g : ↥(alternatingGroup α)), g • x = y
have inr₁ : ∀ (h : Eq (α := ℤˣ) (((Equiv.Perm.sign : Equiv.Perm α →* ℤˣ) : (a : Equiv.Perm α) → ℤˣ) g : ℤˣ) (-1 : ℤˣ)),
  ∃ (g : ↥(alternatingGroup α)), g • x = y
Tactic: rcases Int.units_eq_one_or (Equiv.Perm.sign g) with h | h
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
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
have rw : Fintype.card α -
    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]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
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
⊢ Finset.card (α := α) (Finset.image (α := Fin (Nat.card α - 2)) (⇑x : (a : Fin (Nat.card α - 2)) → α) Finset.univ)ᶜ = 2
have rw₁ : Fintype.card α - Finset.card (α := 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]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
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
⊢ Finset.card (α := α) (Finset.image (α := Fin (Nat.card α - 2)) (⇑x : (a : Fin (Nat.card α - 2)) → α) Finset.univ)ᶜ = 2
have rw₂ : Fintype.card α - Fintype.card (Fin (Nat.card α - 2)) = 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]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
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
⊢ Finset.card (α := α) (Finset.image (α := Fin (Nat.card α - 2)) (⇑x : (a : Fin (Nat.card α - 2)) → α) Finset.univ)ᶜ = 2
have rw₃ : Nat.card α - Fintype.card (Fin (Nat.card α - 2)) = 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]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
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
⊢ Finset.card (α := α) (Finset.image (α := Fin (Nat.card α - 2)) (⇑x : (a : Fin (Nat.card α - 2)) → α) Finset.univ)ᶜ = 2
have rw₄ : Nat.card α - (Nat.card α - 2) = 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]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
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
⊢ Finset.card (α := α) (Finset.image (α := Fin (Nat.card α - 2)) (⇑x : (a : Fin (Nat.card α - 2)) → α) Finset.univ)ᶜ = 2
have rw₅ : Eq (α := ℕ) 2 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]