awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
Goal:
k : ℕ
hrec :
  ∀ {G : Type u_1} [inst : Group G] {α : Type u_2} [inst_3 : MulAction G α] [Finite α]
    (Hk : IsMultiplyPretransitive G α k) {s : Set α} (hs : s.ncard = k),
    Subgroup.index (fixingSubgroup G s) * (Nat.card α - k)! = (Nat.card α)!
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
inst_2 : Finite α
Hk : IsMultiplyPretransitive G α (k + 1)
s : Set α
hs : s.ncard = k + 1
hGX : IsPretransitive G α
a : α
has : a ∈ s
t : Set ↥(ofStabilizer G a) :=
  Subtype.val (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ⁻¹'
    s
hat :
  Subtype.val (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
      t =
    s \ {a}
hat' :
  s =
    insert a
      (Subtype.val (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
        t)
hfs :
  Eq (α := Subgroup G) (fixingSubgroup G s)
    (Subgroup.map (G := ↥(stabilizer G a)) (Subgroup.subtype (stabilizer G a)) (fixingSubgroup (↥(stabilizer G a)) t))
htcard : t.ncard = k
⊢ Nat.card α - 1 = Nat.card.{u_2} ↥(ofStabilizer G a)
have h : Nat.card α - 1 = Nat.card α - 1
Tactic: rw [nat_card_ofStabilizer_eq G a]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
Goal:
k : ℕ
hrec :
  ∀ {G : Type u_1} [inst : Group G] {α : Type u_2} [inst_3 : MulAction G α] [Finite α]
    (Hk : IsMultiplyPretransitive G α k) {s : Set α} (hs : s.ncard = k),
    Subgroup.index (fixingSubgroup G s) * (Nat.card α - k)! = (Nat.card α)!
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
inst_2 : Finite α
Hk : IsMultiplyPretransitive G α (k + 1)
s : Set α
hs : s.ncard = k + 1
hGX : IsPretransitive G α
a : α
has : a ∈ s
t : Set ↥(ofStabilizer G a) :=
  Subtype.val (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ⁻¹'
    s
hat :
  Subtype.val (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
      t =
    s \ {a}
hat' :
  s =
    insert a
      (Subtype.val (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
        t)
hfs :
  Eq (α := Subgroup G) (fixingSubgroup G s)
    (Subgroup.map (G := ↥(stabilizer G a)) (Subgroup.subtype (stabilizer G a)) (fixingSubgroup (↥(stabilizer G a)) t))
htcard : t.ncard = k
⊢ Nat.card α - 1 = Nat.card.{u_2} ↥(ofStabilizer G a)
have h : Nat.card α - 1 = Nat.card α - 1
Tactic: { rw [nat_card_ofStabilizer_eq G a] }
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
inst_2 : Finite α
k : ℕ
Hk : IsMultiplyPretransitive G α k
s : Set α
hs : s.ncard = k
⊢ Subgroup.index (fixingSubgroup G s) * (Nat.card α - k)! = (Nat.card α)!
have zero : ∀ {G : Type u_1} [inst : Group G] {α : Type u_2} [inst_3 : MulAction G α] [Finite α]
  (Hk : IsMultiplyPretransitive G α 0) {s : Set α} (hs : s.ncard = 0),
  Subgroup.index (fixingSubgroup G s) * (Nat.card α - 0)! = (Nat.card α)!
Tactic: induction k generalizing G α with
  | zero =>
    rw [Set.ncard_eq_zero] at hs
    simp [hs]
  | succ k hrec =>
    have hGX : IsPretransitive G α := by
      rw [← is_one_pretransitive_iff]
      apply isMultiplyPretransitive_of_le (n := k + 1)
      · rw [Nat.succ_le_succ_iff]; apply Nat.zero_le
      · rw [← hs, ← Set.ncard_univ]
        exact ncard_le_ncard s.subset_univ finite_univ
    have : s.Nonempty := by
      rw [← Set.ncard_pos, hs]
      exact succ_pos k
    obtain ⟨a, has⟩ := this
    let t : Set (SubMulAction.ofStabilizer G a) := Subtype.val ⁻¹' s
    have hat : Subtype.val '' t = s \ {a} := by
      rw [Set.image_preimage_eq_inter_range]
      simp only [Subtype.range_coe_subtype]
      rw [Set.diff_eq_compl_inter, Set.inter_comm]
      congr
    have hat' : s = insert a (Subtype.val '' t) := by
      rw [hat, Set.insert_diff_singleton, Set.insert_eq_of_mem has]
    have hfs := SubMulAction.fixingSubgroup_of_insert a t
    rw [← hat'] at hfs
    rw [hfs, Subgroup.index_map,
      (MonoidHom.ker_eq_bot_iff (stabilizer G a).subtype).mpr
        (by simp only [Subgroup.coe_subtype, Subtype.coe_injective])]
    simp only [sup_bot_eq, Subgroup.range_subtype]
    have htcard : t.ncard = k := by
      rw [← Nat.succ_inj, Nat.succ_eq_add_one, Nat.succ_eq_add_one, ← hs, hat', eq_comm]
      suffices ¬ a ∈ (Subtype.val '' t) by
        convert! Set.ncard_insert_of_notMem this ?_
        · rw [Set.ncard_image_of_injective _ Subtype.coe_injective]
        apply Set.toFinite
      intro h
      obtain ⟨⟨b, hb⟩, _, hb'⟩ := h
      apply hb
      simp only [← hb', Set.mem_singleton_iff]
    suffices (fixingSubgroup (stabilizer G a) t).index *
      (Nat.card α - 1 - k).factorial =
        (Nat.card α - 1).factorial by
      rw [add_comm k, Nat.mul_right_comm, ← Nat.sub_sub, this, mul_comm,
        index_stabilizer_of_transitive G a]
      exact Nat.mul_factorial_pred (card_ne_zero.mpr ⟨⟨a⟩, inferInstance⟩)
    convert! hrec (ofStabilizer.isMultiplyPretransitive.mp Hk) htcard
    all_goals { rw [nat_card_ofStabilizer_eq G a] }
Cleared hypotheses: G, inst, α, inst_1, inst_2, k, Hk, s, hs
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
inst_2 : Finite α
s : Set α
hMk : IsMultiplyPretransitive G α s.ncard
⊢ Subgroup.index (fixingSubgroup G s) = (Nat.card α).choose s.ncard * s.ncard !
have apply : Subgroup.index (fixingSubgroup G s) * (Nat.card α - s.ncard)! =
  (Nat.card α).choose s.ncard * s.ncard ! * (Nat.card α - s.ncard)!
Tactic: apply Nat.eq_of_mul_eq_mul_right (Nat.factorial_pos _)
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
inst_2 : Finite α
s : Set α
hMk : IsMultiplyPretransitive G α s.ncard
apply :
  Subgroup.index (fixingSubgroup G s) * (Nat.card α - s.ncard)! =
    (Nat.card α).choose s.ncard * s.ncard ! * (Nat.card α - s.ncard)!
⊢ Subgroup.index (fixingSubgroup G s) = (Nat.card α).choose s.ncard * s.ncard !
have apply₁ : ℕ
Tactic: apply Nat.eq_of_mul_eq_mul_right (Nat.factorial_pos _)
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
inst_2 : Finite α
s : Set α
hMk : IsMultiplyPretransitive G α s.ncard
⊢ s.ncard ≤ Nat.card α
have rw : s.ncard ≤ ncard.{u_2} (α := α) univ
Tactic: rw [← ncard_univ]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
Goal:
ι : Type u_2
inst : Finite ι
β : Type u_3
x y : ι ↪ β
⊢ ∃ (σ : Perm β), σ • x = y
have obtain : ∀ (σ : Perm β)
  (hσ : ∀ (a : ι), Eq (α := β) ((σ : (a : β) → β) ((x : (a : ι) → β) a : β) : β) ((y : (a : ι) → β) a : β)),
  ∃ (σ : Perm β), σ • x = y
Tactic: obtain ⟨σ, hσ⟩ := Equiv.Perm.exists_extending_pair x y x.injective y.injective
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
Goal:
α : Type u_1
n : ℕ
⊢ IsMultiplyPretransitive (Perm α) α n
have rw : ∀ (x y : Fin n ↪ α), ∃ (g : Perm α), g • x = y
Tactic: rw [isMultiplyPretransitive_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
Goal:
α : Type u_1
inst : Finite α
G : Subgroup (Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Nat.card α - 1)
⊢ G = ⊤
have have : ∀ (this : Fintype α), G = ⊤
Tactic: have := Fintype.ofFinite α
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (hypothesis)
Goal:
α : Type u_1
inst : Finite α
G : Subgroup (Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Nat.card α - 1)
this : Fintype α
⊢ G = ⊤
have hmt₁ : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
Tactic: simp only [Nat.card_eq_fintype_card] at hmt
Cleared hypotheses: hmt
-- 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 ⋯
⊢ G = ⊤
have rw : ⊤ ≤ G
Tactic: rw [eq_top_iff]
-- 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
⊢ k ∈ G
have obtain : ∀ (g : ↥G) (hg' : g • x' = k • x'), k ∈ G
Tactic: obtain ⟨g, hg'⟩ := exists_smul_eq G x' (k • x')
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
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 α)
⊢ k ∈ G
have rw : (↑g : Perm α) ∈ G
Tactic: rw [this]
-- 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'
⊢ k ∈ G
have suffices : k = (↑g : Perm α)
Tactic: suffices k = g by rw [this]; exact SetLike.coe_mem g
-- 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_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.Surjective x.toFun
have hf : Function.Bijective x.toFun
Tactic: apply Function.Bijective.surjective
-- 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_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.Bijective x.toFun
have hf : Function.Injective x.toFun ∧ Fintype.card (Fin (Fintype.card α)) = Fintype.card α
Tactic: rw [Fintype.bijective_iff_injective_and_card]
-- 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'
⊢ k = (↑g : Perm α)
have hx : ∀ (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 α)⟩
-- 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
⊢ k = (↑g : Perm α)
have 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 : α)
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⟩
-- 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 : α)
i : Fin (Fintype.card α)
⊢ Eq (α := α) ((g • x : (a : Fin (Fintype.card α)) → α) i : α) ((k • x : (a : Fin (Fintype.card α)) → α) i : α)
have inl : ∀ (hi : (↑i : ℕ) < Fintype.card α - 1),
  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
-- 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 : α)
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 : α)
⊢ Eq (α := α) ((g • x : (a : Fin (Fintype.card α)) → α) i : α) ((k • x : (a : Fin (Fintype.card α)) → α) i : α)
have inr : ∀ (hi : (↑i : ℕ) = Fintype.card α - 1),
  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
-- 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 : α)
i : Fin (Fintype.card α)
hi : (↑i : ℕ) = Fintype.card α - 1
⊢ Eq (α := α) ((g • x : (a : Fin (Fintype.card α)) → α) i : α) ((k • x : (a : Fin (Fintype.card α)) → α) i : α)
have 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 : α)
Tactic: obtain ⟨j, hxj : (k • x) j = (g • x) i⟩ := hx (k • x) ((g • x) i)
-- 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 : α)
⊢ Eq (α := α) ((g • x : (a : Fin (Fintype.card α)) → α) i : α) ((k • x : (a : Fin (Fintype.card α)) → α) i : α)
have inr : ∀ (hj : (↑j : ℕ) < Fintype.card α - 1),
  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
-- 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 : α)
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 : α)
have inr₁ : ∀ (hj : (↑j : ℕ) = Fintype.card α - 1),
  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
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (hypothesis)
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
⊢ Eq (α := α) ((g • x : (a : Fin (Fintype.card α)) → α) i : α) ((k • x : (a : Fin (Fintype.card α)) → α) i : α)
have hj₁ : (↑i : ℕ) < (↑i : ℕ)
Tactic: rw [← this, ← hi] at hj
Cleared hypotheses: hj, this
-- 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 : i = j
Tactic: suffices i = j by
          rw [← this, ← hi] at hj
          exact (lt_irrefl _ hj).elim
-- 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
⊢ i = j
have inr : Eq (α := α) ((g • x : (a : Fin (Fintype.card α)) → α) i : α) ((g • x : (a : Fin (Fintype.card α)) → α) j : α)
Tactic: apply EmbeddingLike.injective (g • x)