awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
m n : ℕ
Hn : IsMultiplyPretransitive G α n
s : Set α
inst_2 : Finite.{u_2 + 1} (↑s : Type u_2)
hmn : s.ncard + m = n
x y : Fin m ↪ ↥(ofFixingSubgroup G s)
rw : IsMultiplyPretransitive G α n
⊢ IsMultiplyPretransitive G α (s.ncard + m)

Tactic:
rw [hmn]
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
m n : ℕ
Hn : IsMultiplyPretransitive G α n
s : Set α
inst_2 : Finite.{u_2 + 1} (↑s : Type u_2)
hmn : s.ncard + m = n
x y : Fin m ↪ ↥(ofFixingSubgroup G s)
⊢ IsMultiplyPretransitive G α n

Tactic:
infer_instance
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
m n : ℕ
Hn : IsMultiplyPretransitive G α n
s : Set α
inst_2 : Finite.{u_2 + 1} (↑s : Type u_2)
hmn : s.ncard + m = n
x y : Fin m ↪ ↥(ofFixingSubgroup G s)
⊢ IsMultiplyPretransitive G α (s.ncard + m)

Tactic:
have : IsMultiplyPretransitive G α (s.ncard + m) := by rw [hmn]; infer_instance
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
m n : ℕ
Hn : IsMultiplyPretransitive G α n
s : Set α
inst_2 : Finite.{u_2 + 1} (↑s : Type u_2)
hmn : s.ncard + m = n
x y : Fin m ↪ ↥(ofFixingSubgroup G s)
this : IsMultiplyPretransitive G α (s.ncard + m)
⊢ Nat.card (Fin s.ncard) = Nat.card.{u_2} (↑s : Type u_2)

Tactic:
simp [Nat.card_coe_set_eq]

Premises used: Nat.card_coe_set_eq
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
m n : ℕ
Hn : IsMultiplyPretransitive G α n
s : Set α
inst_2 : Finite.{u_2 + 1} (↑s : Type u_2)
hmn : s.ncard + m = n
x y : Fin m ↪ ↥(ofFixingSubgroup G s)
this : IsMultiplyPretransitive G α (s.ncard + m)
⊢ Nonempty.{max 1 (u_2 + 1)} (Fin s.ncard ≃ (↑s : Type u_2))

Tactic:
have Hs : Nonempty (Fin (s.ncard) ≃ s) :=
      Finite.card_eq.mp (by simp [Nat.card_coe_set_eq])
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
m n : ℕ
Hn : IsMultiplyPretransitive G α n
s : Set α
inst_2 : Finite.{u_2 + 1} (↑s : Type u_2)
hmn : s.ncard + m = n
x y : Fin m ↪ ↥(ofFixingSubgroup G s)
this : IsMultiplyPretransitive G α (s.ncard + m)
Hs : Nonempty.{max 1 (u_2 + 1)} (Fin s.ncard ≃ (↑s : Type u_2))
⊢ let x' := append (s := s) x;
  x' = append (s := s) x

Tactic:
set x' := ofFixingSubgroup.append x with hx

Premises used: SubMulAction.ofFixingSubgroup.append
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
m n : ℕ
Hn : IsMultiplyPretransitive G α n
s : Set α
inst_2 : Finite.{u_2 + 1} (↑s : Type u_2)
hmn : s.ncard + m = n
x y : Fin m ↪ ↥(ofFixingSubgroup G s)
this : IsMultiplyPretransitive G α (s.ncard + m)
Hs : Nonempty.{max 1 (u_2 + 1)} (Fin s.ncard ≃ (↑s : Type u_2))
x' : Fin (s.ncard + m) ↪ α := append (s := s) x
hx : x' = append (s := s) x
⊢ let y' := append (s := s) y;
  y' = append (s := s) y

Tactic:
set y' := ofFixingSubgroup.append y with hy

Premises used: SubMulAction.ofFixingSubgroup.append
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
m n : ℕ
Hn : IsMultiplyPretransitive G α n
s : Set α
inst_2 : Finite.{u_2 + 1} (↑s : Type u_2)
hmn : s.ncard + m = n
x y : Fin m ↪ ↥(ofFixingSubgroup G s)
this : IsMultiplyPretransitive G α (s.ncard + m)
Hs : Nonempty.{max 1 (u_2 + 1)} (Fin s.ncard ≃ (↑s : Type u_2))
x' : Fin (s.ncard + m) ↪ α := append (s := s) x
hx : x' = append (s := s) x
y' : Fin (s.ncard + m) ↪ α := append (s := s) y
hy : y' = append (s := s) y
obtain : ∀ (g : G) (hg : g • x' = y'), ∃ (g : ↥(fixingSubgroup G s)), g • x = y
⊢ ∃ (g : ↥(fixingSubgroup G s)), g • x = y

Tactic:
obtain ⟨g, hg⟩ := exists_smul_eq G x' y'

Premises used: MulAction.exists_smul_eq
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
m n : ℕ
Hn : IsMultiplyPretransitive G α n
s : Set α
inst_2 : Finite.{u_2 + 1} (↑s : Type u_2)
hmn : s.ncard + m = n
x y : Fin m ↪ ↥(ofFixingSubgroup G s)
this_1 : IsMultiplyPretransitive G α (s.ncard + m)
Hs : Nonempty.{max 1 (u_2 + 1)} (Fin s.ncard ≃ (↑s : Type u_2))
x' : Fin (s.ncard + m) ↪ α := append (s := s) x
hx : x' = append (s := s) x
y' : Fin (s.ncard + m) ↪ α := append (s := s) y
hy : y' = append (s := s) y
g : G
hg : g • x' = y'
this : Membership.mem (γ := Subgroup G) (fixingSubgroup G s) g
h : Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (fixingSubgroup G s) x) g this • x = y
⊢ ∃ (g : ↥(fixingSubgroup G s)), g • x = y

Tactic:
use ⟨g, this⟩
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
m n : ℕ
Hn : IsMultiplyPretransitive G α n
s : Set α
inst_2 : Finite.{u_2 + 1} (↑s : Type u_2)
hmn : s.ncard + m = n
x y : Fin m ↪ ↥(ofFixingSubgroup G s)
this_1 : IsMultiplyPretransitive G α (s.ncard + m)
Hs : Nonempty.{max 1 (u_2 + 1)} (Fin s.ncard ≃ (↑s : Type u_2))
x' : Fin (s.ncard + m) ↪ α := append (s := s) x
hx : x' = append (s := s) x
y' : Fin (s.ncard + m) ↪ α := append (s := s) y
hy : y' = append (s := s) y
g : G
hg : g • x' = y'
this : Membership.mem (γ := Subgroup G) (fixingSubgroup G s) g
h :
  ∀ (i : Fin m),
    Eq.{u_2 + 1} (α := α)
      (↑((Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (fixingSubgroup G s) x) g this • x :
              (a : Fin m) → ↥(ofFixingSubgroup G s))
            i) :
        α)
      (↑((y : (a : Fin m) → ↥(ofFixingSubgroup G s)) i) : α)
⊢ Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (fixingSubgroup G s) x) g this • x = y

Tactic:
ext i
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
m n : ℕ
Hn : IsMultiplyPretransitive G α n
s : Set α
inst_2 : Finite.{u_2 + 1} (↑s : Type u_2)
hmn : s.ncard + m = n
x y : Fin m ↪ ↥(ofFixingSubgroup G s)
this_1 : IsMultiplyPretransitive G α (s.ncard + m)
Hs : Nonempty.{max 1 (u_2 + 1)} (Fin s.ncard ≃ (↑s : Type u_2))
x' : Fin (s.ncard + m) ↪ α := append (s := s) x
hx : x' = append (s := s) x
y' : Fin (s.ncard + m) ↪ α := append (s := s) y
hy : y' = append (s := s) y
g : G
hg : g • x' = y'
this : Membership.mem (γ := Subgroup G) (fixingSubgroup G s) g
i : Fin m
h :
  HSMul.hSMul (β := α) g (↑((x : (a : Fin m) → ↥(ofFixingSubgroup G s)) i) : α) =
    (↑((y : (a : Fin m) → ↥(ofFixingSubgroup G s)) i) : α)
⊢ Eq.{u_2 + 1} (α := α)
    (↑((Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (fixingSubgroup G s) x) g this • x :
            (a : Fin m) → ↥(ofFixingSubgroup G s))
          i) :
      α)
    (↑((y : (a : Fin m) → ↥(ofFixingSubgroup G s)) i) : α)

Tactic:
rw [smul_apply, SetLike.val_smul, Subgroup.mk_smul]

Premises used: Function.Embedding.smul_apply, SetLike.val_smul, Subgroup.mk_smul
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
m n : ℕ
Hn : IsMultiplyPretransitive G α n
s : Set α
inst_2 : Finite.{u_2 + 1} (↑s : Type u_2)
hmn : s.ncard + m = n
x y : Fin m ↪ ↥(ofFixingSubgroup G s)
this_1 : IsMultiplyPretransitive G α (s.ncard + m)
Hs : Nonempty.{max 1 (u_2 + 1)} (Fin s.ncard ≃ (↑s : Type u_2))
x' : Fin (s.ncard + m) ↪ α := append (s := s) x
hx : x' = append (s := s) x
y' : Fin (s.ncard + m) ↪ α := append (s := s) y
hy : y' = append (s := s) y
g : G
hg : g • x' = y'
this : Membership.mem (γ := Subgroup G) (fixingSubgroup G s) g
i : Fin m
⊢ HSMul.hSMul (β := α) g (↑((x : (a : Fin m) → ↥(ofFixingSubgroup G s)) i) : α) =
    (↑((y : (a : Fin m) → ↥(ofFixingSubgroup G s)) i) : α)

Tactic:
simp [← ofFixingSubgroup.append_right, ← smul_apply, ← hx, ← hy, hg]

Premises used: Function.Embedding.smul_apply, SubMulAction.ofFixingSubgroup.append_right
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
m n : ℕ
Hn : IsMultiplyPretransitive G α n
s : Set α
inst_2 : Finite.{u_2 + 1} (↑s : Type u_2)
hmn : s.ncard + m = n
x y : Fin m ↪ ↥(ofFixingSubgroup G s)
this : IsMultiplyPretransitive G α (s.ncard + m)
Hs : Nonempty.{max 1 (u_2 + 1)} (Fin s.ncard ≃ (↑s : Type u_2))
x' : Fin (s.ncard + m) ↪ α := append (s := s) x
hx : x' = append (s := s) x
y' : Fin (s.ncard + m) ↪ α := append (s := s) y
hy : y' = append (s := s) y
g : G
hg : g • x' = y'
suffices : Membership.mem (γ := Subgroup G) (fixingSubgroup G s) g
⊢ ∃ (g : ↥(fixingSubgroup G s)), g • x = y

Tactic:
suffices g ∈ fixingSubgroup G s by
      use ⟨g, this⟩
      ext i
      rw [smul_apply, SetLike.val_smul, Subgroup.mk_smul]
      simp [← ofFixingSubgroup.append_right, ← smul_apply, ← hx, ← hy, hg]
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
m n : ℕ
Hn : IsMultiplyPretransitive G α n
s : Set α
inst_2 : Finite.{u_2 + 1} (↑s : Type u_2)
hmn : s.ncard + m = n
x y : Fin m ↪ ↥(ofFixingSubgroup G s)
this : IsMultiplyPretransitive G α (s.ncard + m)
Hs : Nonempty.{max 1 (u_2 + 1)} (Fin s.ncard ≃ (↑s : Type u_2))
x' : Fin (s.ncard + m) ↪ α := append (s := s) x
hx : x' = append (s := s) x
y' : Fin (s.ncard + m) ↪ α := append (s := s) y
hy : y' = append (s := s) y
g : G
hg : g • x' = y'
a : (↑s : Type u_2)
i : Fin s.ncard := ((Classical.choice Hs).symm : (a : (↑s : Type u_2)) → Fin s.ncard) a
⊢ (Classical.choice Hs : (a : Fin s.ncard) → (↑s : Type u_2)) i = a

Tactic:
simp [i]
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
m n : ℕ
Hn : IsMultiplyPretransitive G α n
s : Set α
inst_2 : Finite.{u_2 + 1} (↑s : Type u_2)
hmn : s.ncard + m = n
x y : Fin m ↪ ↥(ofFixingSubgroup G s)
this : IsMultiplyPretransitive G α (s.ncard + m)
Hs : Nonempty.{max 1 (u_2 + 1)} (Fin s.ncard ≃ (↑s : Type u_2))
x' : Fin (s.ncard + m) ↪ α := append (s := s) x
hx : x' = append (s := s) x
y' : Fin (s.ncard + m) ↪ α := append (s := s) y
hy : y' = append (s := s) y
g : G
hg : g • x' = y'
a : (↑s : Type u_2)
i : Fin s.ncard := ((Classical.choice Hs).symm : (a : (↑s : Type u_2)) → Fin s.ncard) a
⊢ (Classical.choice Hs : (a : Fin s.ncard) → (↑s : Type u_2)) i = a

Tactic:
have ha : (Classical.choice Hs) i = a := by simp [i]
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
m n : ℕ
Hn : IsMultiplyPretransitive G α n
s : Set α
inst_2 : Finite.{u_2 + 1} (↑s : Type u_2)
hmn : s.ncard + m = n
x y : Fin m ↪ ↥(ofFixingSubgroup G s)
this : IsMultiplyPretransitive G α (s.ncard + m)
Hs : Nonempty.{max 1 (u_2 + 1)} (Fin s.ncard ≃ (↑s : Type u_2))
x' : Fin (s.ncard + m) ↪ α := append (s := s) x
hx : x' = append (s := s) x
y' : Fin (s.ncard + m) ↪ α := append (s := s) y
hy : y' = append (s := s) y
g : G
hg : g • x' = y'
a : (↑s : Type u_2)
i : Fin s.ncard := ((Classical.choice Hs).symm : (a : (↑s : Type u_2)) → Fin s.ncard) a
ha : (Classical.choice Hs : (a : Fin s.ncard) → (↑s : Type u_2)) i = a
rw :
  HSMul.hSMul (β := α) g (↑((Classical.choice Hs : (a : Fin s.ncard) → (↑s : Type u_2)) i) : α) =
    (↑((Classical.choice Hs : (a : Fin s.ncard) → (↑s : Type u_2)) i) : α)
⊢ g • (↑a : α) = (↑a : α)

Tactic:
rw [← ha]
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
m n : ℕ
Hn : IsMultiplyPretransitive G α n
s : Set α
inst_2 : Finite.{u_2 + 1} (↑s : Type u_2)
hmn : s.ncard + m = n
x y : Fin m ↪ ↥(ofFixingSubgroup G s)
this : IsMultiplyPretransitive G α (s.ncard + m)
Hs : Nonempty.{max 1 (u_2 + 1)} (Fin s.ncard ≃ (↑s : Type u_2))
x' : Fin (s.ncard + m) ↪ α := append (s := s) x
hx : x' = append (s := s) x
y' : Fin (s.ncard + m) ↪ α := append (s := s) y
hy : y' = append (s := s) y
g : G
hg : g • x' = y'
a : (↑s : Type u_2)
i : Fin s.ncard := ((Classical.choice Hs).symm : (a : (↑s : Type u_2)) → Fin s.ncard) a
ha : (Classical.choice Hs : (a : Fin s.ncard) → (↑s : Type u_2)) i = a
nth_rewrite :
  HSMul.hSMul (β := α) g ((append (s := s) x : (a : Fin (s.ncard + m)) → α) (castAdd m i) : α) =
    (↑((Classical.choice Hs : (a : Fin s.ncard) → (↑s : Type u_2)) i) : α)
⊢ HSMul.hSMul (β := α) g (↑((Classical.choice Hs : (a : Fin s.ncard) → (↑s : Type u_2)) i) : α) =
    (↑((Classical.choice Hs : (a : Fin s.ncard) → (↑s : Type u_2)) i) : α)

Tactic:
nth_rewrite 1 [← ofFixingSubgroup.append_left x i]

Premises used: SubMulAction.ofFixingSubgroup.append_left
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
m n : ℕ
Hn : IsMultiplyPretransitive G α n
s : Set α
inst_2 : Finite.{u_2 + 1} (↑s : Type u_2)
hmn : s.ncard + m = n
x y : Fin m ↪ ↥(ofFixingSubgroup G s)
this : IsMultiplyPretransitive G α (s.ncard + m)
Hs : Nonempty.{max 1 (u_2 + 1)} (Fin s.ncard ≃ (↑s : Type u_2))
x' : Fin (s.ncard + m) ↪ α := append (s := s) x
hx : x' = append (s := s) x
y' : Fin (s.ncard + m) ↪ α := append (s := s) y
hy : y' = append (s := s) y
g : G
hg : g • x' = y'
a : (↑s : Type u_2)
i : Fin s.ncard := ((Classical.choice Hs).symm : (a : (↑s : Type u_2)) → Fin s.ncard) a
ha : (Classical.choice Hs : (a : Fin s.ncard) → (↑s : Type u_2)) i = a
rw :
  HSMul.hSMul (β := α) g ((append (s := s) x : (a : Fin (s.ncard + m)) → α) (castAdd m i) : α) =
    (append (s := s) y : (a : Fin (s.ncard + m)) → α) (castAdd m i)
rw₁ :
  HSMul.hSMul (β := α) g ((append (s := s) x : (a : Fin (s.ncard + m)) → α) (castAdd m i) : α) =
    (y' : (a : Fin (s.ncard + m)) → α) (castAdd m i)
rw₂ :
  HSMul.hSMul (β := α) g ((append (s := s) x : (a : Fin (s.ncard + m)) → α) (castAdd m i) : α) =
    (g • x' : (a : Fin (s.ncard + m)) → α) (castAdd m i)
rw₃ :
  HSMul.hSMul (β := α) g ((append (s := s) x : (a : Fin (s.ncard + m)) → α) (castAdd m i) : α) =
    HSMul.hSMul (β := α) g ((x' : (a : Fin (s.ncard + m)) → α) (castAdd m i) : α)
rw₄ rw₅ :
  HSMul.hSMul (β := α) g ((x' : (a : Fin (s.ncard + m)) → α) (castAdd m i) : α) =
    HSMul.hSMul (β := α) g ((x' : (a : Fin (s.ncard + m)) → α) (castAdd m i) : α)
⊢ HSMul.hSMul (β := α) g ((append (s := s) x : (a : Fin (s.ncard + m)) → α) (castAdd m i) : α) =
    (↑((Classical.choice Hs : (a : Fin s.ncard) → (↑s : Type u_2)) i) : α)

Tactic:
rw [← ofFixingSubgroup.append_left y i, ← hy, ← hg, smul_apply, ← hx]

Premises used: Function.Embedding.smul_apply, SubMulAction.ofFixingSubgroup.append_left
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
m n : ℕ
inst_2 : IsMultiplyPretransitive G α n
s : Set α
inst_3 : Finite.{u_2 + 1} (↑s : Type u_2)
hmn : s.ncard + m ≤ n
hn : (↑n : ℕ∞) ≤ ENat.card α
⊢ IsMultiplyPretransitive.{u_1, u_2} (↥(fixingSubgroup G s)) (↥(ofFixingSubgroup G s)) m

Tactic:
letI : IsMultiplyPretransitive G α (s.ncard + m) := isMultiplyPretransitive_of_le' hmn hn
  isMultiplyPretransitive G s rfl

Premises used: SubMulAction.ofFixingSubgroup.isMultiplyPretransitive, rfl
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
inst_2 : Finite α
Hk : IsMultiplyPretransitive G α 0
s : Set α
hs : s.ncard = 0
⊢ s = ∅

Tactic:
rw [Set.ncard_eq_zero] at hs

Premises used: Set.ncard_eq_zero
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
inst_2 : Finite α
Hk : IsMultiplyPretransitive G α 0
s : Set α
hs : s = ∅
⊢ Subgroup.index (fixingSubgroup G s) * (Nat.card α - 0)! = (Nat.card α)!

Tactic:
simp [hs]
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
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
rw : IsMultiplyPretransitive G α 1
⊢ IsPretransitive G α

Tactic:
rw [← is_one_pretransitive_iff]

Premises used: MulAction.is_one_pretransitive_iff
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
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
hmn : 1 ≤ k + 1
hα : k + 1 ≤ Nat.card α
⊢ IsMultiplyPretransitive G α 1

Tactic:
apply isMultiplyPretransitive_of_le (n := k + 1)

Premises used: MulAction.isMultiplyPretransitive_of_le
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
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
hmn : 0 ≤ k
⊢ 1 ≤ k + 1

Tactic:
rw [Nat.succ_le_succ_iff]

Premises used: Nat.succ_le_succ_iff
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
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
⊢ 0 ≤ k

Tactic:
apply Nat.zero_le

Premises used: Nat.zero_le
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
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
hα : s.ncard ≤ ncard.{u_2} (α := α) univ
⊢ k + 1 ≤ Nat.card α

Tactic:
rw [← hs, ← Set.ncard_univ]

Premises used: Set.ncard_univ
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
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
⊢ s.ncard ≤ ncard.{u_2} (α := α) univ

Tactic:
ncard_le_ncard s.subset_univ finite_univ

Premises used: Set.subset_univ, Set.finite_univ, Set.ncard_le_ncard
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
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
⊢ s.ncard ≤ ncard.{u_2} (α := α) univ

Tactic:
exact ncard_le_ncard s.subset_univ finite_univ

Premises used: Set.subset_univ, Set.finite_univ, Set.ncard_le_ncard
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
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
⊢ IsPretransitive G α

Tactic:
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
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
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 α
rw : 0 < k + 1
⊢ s.Nonempty

Tactic:
rw [← Set.ncard_pos, hs]

Premises used: Set.ncard_pos
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
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 α
⊢ 0 < k + 1

Tactic:
succ_pos k

Premises used: Nat.succ_pos
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
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 α
⊢ 0 < k + 1

Tactic:
exact succ_pos k

Premises used: Nat.succ_pos
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
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 α
⊢ s.Nonempty

Tactic:
have : s.Nonempty := by
      rw [← Set.ncard_pos, hs]
      exact succ_pos k
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
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 α
this : s.Nonempty
succ : ∀ (a : α) (has : a ∈ s), Subgroup.index (fixingSubgroup G s) * (Nat.card α - (k + 1))! = (Nat.card α)!
⊢ Subgroup.index (fixingSubgroup G s) * (Nat.card α - (k + 1))! = (Nat.card α)!

Tactic:
obtain ⟨a, has⟩ := this