awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
α : Type u_1
n : ℕ
rw : ∀ (x y : Fin n ↪ α), ∃ (g : Perm α), g • x = y
⊢ IsMultiplyPretransitive (Perm α) α n

Tactic:
rw [isMultiplyPretransitive_iff]

Premises used: MulAction.isMultiplyPretransitive_iff
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
α : Type u_1
n : ℕ
⊢ ∀ (x y : Fin n ↪ α), ∃ (g : Perm α), g • x = y

Tactic:
exists_smul_eq_embedding

Premises used: Equiv.Perm.exists_smul_eq_embedding
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
α : Type u_1
n : ℕ
⊢ ∀ (x y : Fin n ↪ α), ∃ (g : Perm α), g • x = y

Tactic:
exact exists_smul_eq_embedding

Premises used: Equiv.Perm.exists_smul_eq_embedding
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
α : Type u_1
⊢ IsPreprimitive (Perm α) α

Tactic:
isPreprimitive_of_is_two_pretransitive (isMultiplyPretransitive _ _)

Premises used: MulAction.isPreprimitive_of_is_two_pretransitive, Equiv.Perm.isMultiplyPretransitive
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
α : Type u_1
inst : Finite α
G : Subgroup (Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Nat.card α - 1)
have : ∀ (this : Fintype α), G = ⊤
⊢ G = ⊤

Tactic:
have := Fintype.ofFinite α
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
α : Type u_1
inst : Finite α
G : Subgroup (Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Nat.card α - 1)
this : Fintype α
⊢ IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)

Tactic:
simp only [Nat.card_eq_fintype_card] at hmt

Premises used: Nat.card_eq_fintype_card
-- 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 ⋯
rw : ⊤ ≤ G
⊢ G = ⊤

Tactic:
rw [eq_top_iff]

Premises used: eq_top_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 α
_ : Membership.mem (γ := Subgroup (Perm α)) ⊤ k → k ∈ G
⊢ Membership.mem (γ := Subgroup (Perm α)) ⊤ k → k ∈ G

Tactic:
_
-- 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
obtain : ∀ (g : ↥G) (hg' : g • x' = k • x'), k ∈ G
⊢ k ∈ G

Tactic:
obtain ⟨g, hg'⟩ := exists_smul_eq G x' (k • x')

Premises used: Membership.mem, Subtype, HSMul.hSMul, MulAction.exists_smul_eq
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
α : Type u_1
inst : Finite α
G : Subgroup (Perm α)
this_1 : 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'
this : k = (↑g : Perm α)
rw : (↑g : Perm α) ∈ G
⊢ k ∈ G

Tactic:
rw [this]
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
α : Type u_1
inst : Finite α
G : Subgroup (Perm α)
this_1 : 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'
this : k = (↑g : Perm α)
⊢ (↑g : Perm α) ∈ G

Tactic:
SetLike.coe_mem g

Premises used: SetLike.coe_mem
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
α : Type u_1
inst : Finite α
G : Subgroup (Perm α)
this_1 : 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'
this : k = (↑g : Perm α)
⊢ (↑g : Perm α) ∈ G

Tactic:
exact SetLike.coe_mem g

Premises used: SetLike.coe_mem
-- 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'
suffices : k = (↑g : Perm α)
⊢ k ∈ G

Tactic:
suffices k = g by rw [this]; exact SetLike.coe_mem g
-- 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_1 : Fin (Fintype.card α) ↪ α := Equiv.toEmbedding (Equiv.symm (Fintype.equivFinOfCardEq ⋯))
x' : Fin (Fintype.card α - 1) ↪ α := j.trans x_1
g : ↥G
hg' : g • x' = k • x'
x : Fin (Fintype.card α) ↪ α
hf : Function.Bijective x.toFun
⊢ Function.Surjective x.toFun

Tactic:
apply Function.Bijective.surjective

Premises used: Function.Bijective.surjective
-- 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_1 : Fin (Fintype.card α) ↪ α := Equiv.toEmbedding (Equiv.symm (Fintype.equivFinOfCardEq ⋯))
x' : Fin (Fintype.card α - 1) ↪ α := j.trans x_1
g : ↥G
hg' : g • x' = k • x'
x : Fin (Fintype.card α) ↪ α
hf : Function.Injective x.toFun ∧ Fintype.card (Fin (Fintype.card α)) = Fintype.card α
⊢ Function.Bijective x.toFun

Tactic:
rw [Fintype.bijective_iff_injective_and_card]

Premises used: Fintype.bijective_iff_injective_and_card
-- 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_1 : Fin (Fintype.card α) ↪ α := Equiv.toEmbedding (Equiv.symm (Fintype.equivFinOfCardEq ⋯))
x' : Fin (Fintype.card α - 1) ↪ α := j.trans x_1
g : ↥G
hg' : g • x' = k • x'
x : Fin (Fintype.card α) ↪ α
⊢ Function.Injective x.toFun ∧ Fintype.card (Fin (Fintype.card α)) = Fintype.card α

Tactic:
⟨EmbeddingLike.injective x, Fintype.card_fin (Fintype.card α)⟩

Premises used: Fintype.card_fin, Fintype.card, EmbeddingLike.injective, And.intro
-- 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_1 : Fin (Fintype.card α) ↪ α := Equiv.toEmbedding (Equiv.symm (Fintype.equivFinOfCardEq ⋯))
x' : Fin (Fintype.card α - 1) ↪ α := j.trans x_1
g : ↥G
hg' : g • x' = k • x'
x : Fin (Fintype.card α) ↪ α
⊢ Function.Injective x.toFun ∧ Fintype.card (Fin (Fintype.card α)) = Fintype.card α

Tactic:
exact ⟨EmbeddingLike.injective x, Fintype.card_fin (Fintype.card α)⟩
-- 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'
⊢ ∀ (x : Fin (Fintype.card α) ↪ α), Function.Surjective x.toFun

Tactic:
have hx (x : Fin (Fintype.card α) ↪ α) : Function.Surjective x.toFun := by
    apply Function.Bijective.surjective
    rw [Fintype.bijective_iff_injective_and_card]
    exact ⟨EmbeddingLike.injective x, Fintype.card_fin (Fintype.card α)⟩
-- 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
⊢ ∀ (i : Fin (Fintype.card α)) (hi : (↑i : ℕ) < Fintype.card α - 1),
    Eq (α := α) ((g • x : (a : Fin (Fintype.card α)) → α) i : α) ((k • x : (a : Fin (Fintype.card α)) → α) i : α)

Tactic:
have hgk' (i : Fin (Fintype.card α)) (hi : i.val < Fintype.card α - 1) :
      (g • x) i = (k • x) i :=
    Function.Embedding.ext_iff.mp hg' ⟨i.val, hi⟩
-- 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 α)
inl :
  ∀ (hi : (↑i : ℕ) < Fintype.card α - 1),
    Eq (α := α) ((g • x : (a : Fin (Fintype.card α)) → α) i : α) ((k • x : (a : Fin (Fintype.card α)) → α) i : α)
inr :
  ∀ (hi : (↑i : ℕ) = Fintype.card α - 1),
    Eq (α := α) ((g • x : (a : Fin (Fintype.card α)) → α) i : α) ((k • x : (a : Fin (Fintype.card α)) → α) i : α)
⊢ Eq (α := α) ((g • x : (a : Fin (Fintype.card α)) → α) i : α) ((k • x : (a : Fin (Fintype.card α)) → α) i : α)

Tactic:
rcases lt_or_eq_of_le (le_sub_one_of_lt i.prop) with hi | hi

Premises used: lt_or_eq_of_le, Fin.prop, Nat.le_sub_one_of_lt
-- 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 α)
hi : (↑i : ℕ) < Fintype.card α - 1
⊢ Eq (α := α) ((g • x : (a : Fin (Fintype.card α)) → α) i : α) ((k • x : (a : Fin (Fintype.card α)) → α) i : α)

Tactic:
hgk' i hi
-- 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 α)
hi : (↑i : ℕ) < Fintype.card α - 1
⊢ Eq (α := α) ((g • x : (a : Fin (Fintype.card α)) → α) i : α) ((k • x : (a : Fin (Fintype.card α)) → α) i : α)

Tactic:
exact hgk' i hi
-- 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 α)
hi : (↑i : ℕ) = Fintype.card α - 1
inr :
  ∀ (j : Fin (Fintype.card α))
    (hxj :
      Eq (α := α) ((k • x : (a : Fin (Fintype.card α)) → α) j : α) ((g • x : (a : Fin (Fintype.card α)) → α) i : α)),
    Eq (α := α) ((g • x : (a : Fin (Fintype.card α)) → α) i : α) ((k • x : (a : Fin (Fintype.card α)) → α) i : α)
⊢ Eq (α := α) ((g • x : (a : Fin (Fintype.card α)) → α) i : α) ((k • x : (a : Fin (Fintype.card α)) → α) i : α)

Tactic:
obtain ⟨j, hxj : (k • x) j = (g • x) i⟩ := hx (k • x) ((g • x) i)

Premises used: HSMul.hSMul, DFunLike.coe
-- 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 : α)
inr :
  ∀ (hj : (↑j : ℕ) < Fintype.card α - 1),
    Eq (α := α) ((g • x : (a : Fin (Fintype.card α)) → α) i : α) ((k • x : (a : Fin (Fintype.card α)) → α) i : α)
inr₁ :
  ∀ (hj : (↑j : ℕ) = Fintype.card α - 1),
    Eq (α := α) ((g • x : (a : Fin (Fintype.card α)) → α) i : α) ((k • x : (a : Fin (Fintype.card α)) → α) i : α)
⊢ Eq (α := α) ((g • x : (a : Fin (Fintype.card α)) → α) i : α) ((k • x : (a : Fin (Fintype.card α)) → α) i : α)

Tactic:
rcases lt_or_eq_of_le (le_sub_one_of_lt j.prop) with hj | hj

Premises used: lt_or_eq_of_le, Fin.prop, Nat.le_sub_one_of_lt
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
α : Type u_1
inst : Finite α
G : Subgroup (Perm α)
this_1 : 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
this : i = j
⊢ (↑i : ℕ) < (↑i : ℕ)

Tactic:
rw [← this, ← hi] at hj
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
α : Type u_1
inst : Finite α
G : Subgroup (Perm α)
this_1 : 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
this : i = j
hj₁ : (↑i : ℕ) < (↑i : ℕ)
⊢ i = j

Tactic:
rw [← this, ← hi] at hj
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
α : Type u_1
inst : Finite α
G : Subgroup (Perm α)
this_1 : 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 : (↑i : ℕ) < (↑i : ℕ)
this : i = j
⊢ Eq (α := α) ((g • x : (a : Fin (Fintype.card α)) → α) i : α) ((k • x : (a : Fin (Fintype.card α)) → α) i : α)

Tactic:
(lt_irrefl _ hj).elim

Premises used: lt_irrefl, False.elim
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
α : Type u_1
inst : Finite α
G : Subgroup (Perm α)
this_1 : 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 : (↑i : ℕ) < (↑i : ℕ)
this : i = j
⊢ Eq (α := α) ((g • x : (a : Fin (Fintype.card α)) → α) i : α) ((k • x : (a : Fin (Fintype.card α)) → α) i : α)

Tactic:
exact (lt_irrefl _ hj).elim

Premises used: lt_irrefl, False.elim
-- 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 : i = j
⊢ Eq (α := α) ((g • x : (a : Fin (Fintype.card α)) → α) i : α) ((k • x : (a : Fin (Fintype.card α)) → α) i : α)

Tactic:
suffices i = j by
          rw [← this, ← hi] at hj
          exact (lt_irrefl _ hj).elim
-- 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 (α := α) ((g • x : (a : Fin (Fintype.card α)) → α) i : α) ((g • x : (a : Fin (Fintype.card α)) → α) j : α)
⊢ i = j

Tactic:
apply EmbeddingLike.injective (g • x)

Premises used: EmbeddingLike.injective, HSMul.hSMul
-- 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 (α := α) ((g • x : (a : Fin (Fintype.card α)) → α) i : α) ((k • x : (a : Fin (Fintype.card α)) → α) j : α)
inr₁ inr₂ :
  Eq (α := α) ((g • x : (a : Fin (Fintype.card α)) → α) i : α) ((g • x : (a : Fin (Fintype.card α)) → α) i : α)
⊢ Eq (α := α) ((g • x : (a : Fin (Fintype.card α)) → α) i : α) ((g • x : (a : Fin (Fintype.card α)) → α) j : α)

Tactic:
rw [hgk' j hj, hxj]