awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
n : ℕ
hrec :
  ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_2 : MulAction G α] (hG : IsPreprimitive G α) {s : Set α}
    (hsn : s.ncard = n + 1) (hsn' : n + 2 < Nat.card α)
    (hprim : IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s)) (hα : Finite α),
    IsMultiplyPreprimitive G α (n + 2)
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
hG : IsPreprimitive G α
s : Set α
hsn : s.ncard = n + 1 + 1
hsn' : n + 1 + 2 < Nat.card α
hprim : IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s)
hα : Finite α
a : α
t : Set ↥(ofStabilizer G a)
left : a ∈ s
hst :
  s =
    insert a
      (Subtype.val (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
        t)
ha' :
  a ∉
    Subtype.val (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
      t
ht_prim : IsPreprimitive.{u_1, u_2} ↥(stabilizer G a) ↥(ofStabilizer G a)
this :
  IsPreprimitive.{u_1, u_2}
    ↥(fixingSubgroup G
        (insert a
          (Subtype.val (p := fun (x : α) ↦
              Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
            t)))
    ↥(ofFixingSubgroup G
        (insert a
          (Subtype.val (p := fun (x : α) ↦
              Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
            t)))
hGs' : IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup (↥(stabilizer G a)) t) ↥(ofFixingSubgroup (↥(stabilizer G a)) t)
⊢ n + 2 + 1 < Nat.card α

Tactic:
exact hsn'
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
n : ℕ
hrec :
  ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_2 : MulAction G α] (hG : IsPreprimitive G α) {s : Set α}
    (hsn : s.ncard = n + 1) (hsn' : n + 2 < Nat.card α)
    (hprim : IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s)) (hα : Finite α),
    IsMultiplyPreprimitive G α (n + 2)
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
hG : IsPreprimitive G α
s : Set α
hsn : s.ncard = n + 1 + 1
hsn' : n + 1 + 2 < Nat.card α
hprim : IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s)
hα : Finite α
succ :
  ∃ (a : α) (t : Set ↥(ofStabilizer G a)),
    a ∈ s ∧
      s =
        insert a
          (Subtype.val (p := fun (x : α) ↦
              Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
            t)
⊢ IsMultiplyPreprimitive G α (n + 1 + 2)

Tactic:
suffices ∃ (a : α) (t : Set (SubMulAction.ofStabilizer G a)),
      a ∈ s ∧ s = insert a (Subtype.val '' t) by
      obtain ⟨a, t, _, hst⟩ := this
      have ha' : a ∉ Subtype.val '' t := by
        intro h; rw [Set.mem_image] at h; obtain ⟨x, hx⟩ := h
        apply x.prop; rw [hx.right]; exact Set.mem_singleton a
      have ht_prim : IsPreprimitive (stabilizer G a) (SubMulAction.ofStabilizer G a) := by
        rw [← is_one_preprimitive_iff]
        rw [← isMultiplyPreprimitive_succ_iff_ofStabilizer]
        · apply is_two_preprimitive hG hsn hsn' hprim
        · norm_num
      have : IsPreprimitive ↥(fixingSubgroup G (insert a (Subtype.val '' t)))
          (ofFixingSubgroup G (insert a (Subtype.val '' t))) :=
        IsPreprimitive.of_surjective
          (ofFixingSubgroup_of_eq_bijective (hst := hst)).surjective
      have hGs' : IsPreprimitive (fixingSubgroup (stabilizer G a) t)
        (ofFixingSubgroup (stabilizer G a) t) :=
        IsPreprimitive.of_surjective
          ofFixingSubgroup_insert_map_bijective.surjective
      rw [isMultiplyPreprimitive_succ_iff_ofStabilizer G (a := a) _ (Nat.le_add_left 1 (n + 1))]
      refine hrec ht_prim ?_ ?_ hGs' Subtype.finite
      · -- t.card = Nat.succ n
        rw [← Set.ncard_image_of_injective t Subtype.val_injective]
        apply Nat.add_right_cancel
        rw [← Set.ncard_insert_of_notMem ha', ← hst, hsn]
      · -- n + 2 < Nat.card (SubMulAction.ofStabilizer G α a)
        rw [← Nat.add_lt_add_iff_right, nat_card_ofStabilizer_add_one_eq]
        exact hsn'
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
n : ℕ
hrec :
  ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_2 : MulAction G α] (hG : IsPreprimitive G α) {s : Set α}
    (hsn : s.ncard = n + 1) (hsn' : n + 2 < Nat.card α)
    (hprim : IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s)) (hα : Finite α),
    IsMultiplyPreprimitive G α (n + 2)
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
hG : IsPreprimitive G α
s : Set α
hsn : s.ncard = n + 1 + 1
hsn' : n + 1 + 2 < Nat.card α
hprim : IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s)
hα : Finite α
this : s.Nonempty
obtain :
  ∀ (a : α) (ha : a ∈ s),
    ∃ (a : α) (t : Set ↥(ofStabilizer G a)),
      a ∈ s ∧
        s =
          insert a
            (Subtype.val (p := fun (x : α) ↦
                Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
              t)
⊢ ∃ (a : α) (t : Set ↥(ofStabilizer G a)),
    a ∈ s ∧
      s =
        insert a
          (Subtype.val (p := fun (x : α) ↦
              Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
            t)

Tactic:
obtain ⟨a, ha⟩ := this
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
n : ℕ
hrec :
  ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_2 : MulAction G α] (hG : IsPreprimitive G α) {s : Set α}
    (hsn : s.ncard = n + 1) (hsn' : n + 2 < Nat.card α)
    (hprim : IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s)) (hα : Finite α),
    IsMultiplyPreprimitive G α (n + 2)
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
hG : IsPreprimitive G α
s : Set α
hsn : s.ncard = n + 1 + 1
hsn' : n + 1 + 2 < Nat.card α
hprim : IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s)
hα : Finite α
a : α
ha : a ∈ s
right :
  s =
    insert a
      (Set.image (α := ↥(ofStabilizer G a))
        (Subtype.val (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x))
        (Subtype.val (p := fun (x : α) ↦
            Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ⁻¹'
          s))
⊢ ∃ (a : α) (t : Set ↥(ofStabilizer G a)),
    a ∈ s ∧
      s =
        insert a
          (Subtype.val (p := fun (x : α) ↦
              Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
            t)

Tactic:
use a, Subtype.val ⁻¹' s, ha

Premises used: Subtype.val
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
n : ℕ
hrec :
  ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_2 : MulAction G α] (hG : IsPreprimitive G α) {s : Set α}
    (hsn : s.ncard = n + 1) (hsn' : n + 2 < Nat.card α)
    (hprim : IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s)) (hα : Finite α),
    IsMultiplyPreprimitive G α (n + 2)
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
hG : IsPreprimitive G α
s : Set α
hsn : s.ncard = n + 1 + 1
hsn' : n + 1 + 2 < Nat.card α
hprim : IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s)
hα : Finite α
a : α
ha : a ∈ s
right :
  ∀ (x : α),
    x ∈ s ↔
      x ∈
        insert a
          (Set.image (α := ↥(ofStabilizer G a))
            (Subtype.val (p := fun (x : α) ↦
              Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x))
            (Subtype.val (p := fun (x : α) ↦
                Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ⁻¹'
              s))
⊢ s =
    insert a
      (Set.image (α := ↥(ofStabilizer G a))
        (Subtype.val (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x))
        (Subtype.val (p := fun (x : α) ↦
            Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ⁻¹'
          s))

Tactic:
ext x
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
n : ℕ
hrec :
  ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_2 : MulAction G α] (hG : IsPreprimitive G α) {s : Set α}
    (hsn : s.ncard = n + 1) (hsn' : n + 2 < Nat.card α)
    (hprim : IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s)) (hα : Finite α),
    IsMultiplyPreprimitive G α (n + 2)
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
hG : IsPreprimitive G α
s : Set α
hsn : s.ncard = n + 1 + 1
hsn' : n + 1 + 2 < Nat.card α
hprim : IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s)
hα : Finite α
a : α
ha : a ∈ s
x : α
pos :
  ∀ (hx : x = a),
    x ∈ s ↔
      x ∈
        insert a
          (Set.image (α := ↥(ofStabilizer G a))
            (Subtype.val (p := fun (x : α) ↦
              Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x))
            (Subtype.val (p := fun (x : α) ↦
                Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ⁻¹'
              s))
neg :
  ∀ (hx : ¬x = a),
    x ∈ s ↔
      x ∈
        insert a
          (Set.image (α := ↥(ofStabilizer G a))
            (Subtype.val (p := fun (x : α) ↦
              Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x))
            (Subtype.val (p := fun (x : α) ↦
                Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ⁻¹'
              s))
⊢ x ∈ s ↔
    x ∈
      insert a
        (Set.image (α := ↥(ofStabilizer G a))
          (Subtype.val (p := fun (x : α) ↦
            Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x))
          (Subtype.val (p := fun (x : α) ↦
              Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ⁻¹'
            s))

Tactic:
by_cases hx : x = a
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
n : ℕ
hrec :
  ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_2 : MulAction G α] (hG : IsPreprimitive G α) {s : Set α}
    (hsn : s.ncard = n + 1) (hsn' : n + 2 < Nat.card α)
    (hprim : IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s)) (hα : Finite α),
    IsMultiplyPreprimitive G α (n + 2)
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
hG : IsPreprimitive G α
s : Set α
hsn : s.ncard = n + 1 + 1
hsn' : n + 1 + 2 < Nat.card α
hprim : IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s)
hα : Finite α
a : α
ha : a ∈ s
x : α
hx : x = a
⊢ x ∈ s ↔
    x ∈
      insert a
        (Set.image (α := ↥(ofStabilizer G a))
          (Subtype.val (p := fun (x : α) ↦
            Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x))
          (Subtype.val (p := fun (x : α) ↦
              Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ⁻¹'
            s))

Tactic:
simp [hx, mem_ofStabilizer_iff, ha]

Premises used: SubMulAction.mem_ofStabilizer_iff
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
n : ℕ
hrec :
  ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_2 : MulAction G α] (hG : IsPreprimitive G α) {s : Set α}
    (hsn : s.ncard = n + 1) (hsn' : n + 2 < Nat.card α)
    (hprim : IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s)) (hα : Finite α),
    IsMultiplyPreprimitive G α (n + 2)
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
hG : IsPreprimitive G α
s : Set α
hsn : s.ncard = n + 1 + 1
hsn' : n + 1 + 2 < Nat.card α
hprim : IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s)
hα : Finite α
a : α
ha : a ∈ s
x : α
hx : ¬x = a
⊢ x ∈ s ↔
    x ∈
      insert a
        (Set.image (α := ↥(ofStabilizer G a))
          (Subtype.val (p := fun (x : α) ↦
            Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x))
          (Subtype.val (p := fun (x : α) ↦
              Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ⁻¹'
            s))

Tactic:
simp [hx, mem_ofStabilizer_iff, ha]

Premises used: SubMulAction.mem_ofStabilizer_iff
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
n : ℕ
hrec :
  ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_2 : MulAction G α] (hG : IsPreprimitive G α) {s : Set α}
    (hsn : s.ncard = n + 1) (hsn' : n + 2 < Nat.card α)
    (hprim : IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s)) (hα : Finite α),
    IsMultiplyPreprimitive G α (n + 2)
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
hG : IsPreprimitive G α
s : Set α
hsn : s.ncard = n + 1 + 1
hsn' : n + 1 + 2 < Nat.card α
hprim : IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s)
hα : Finite α
succ : s.Nonempty
⊢ ∃ (a : α) (t : Set ↥(ofStabilizer G a)),
    a ∈ s ∧
      s =
        insert a
          (Subtype.val (p := fun (x : α) ↦
              Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
            t)

Tactic:
suffices s.Nonempty by
      obtain ⟨a, ha⟩ := this
      use a, Subtype.val ⁻¹' s, ha
      ext x
      by_cases hx : x = a <;> simp [hx, mem_ofStabilizer_iff, ha]
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
n : ℕ
hrec :
  ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_2 : MulAction G α] (hG : IsPreprimitive G α) {s : Set α}
    (hsn : s.ncard = n + 1) (hsn' : n + 2 < Nat.card α)
    (hprim : IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s)) (hα : Finite α),
    IsMultiplyPreprimitive G α (n + 2)
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
hG : IsPreprimitive G α
s : Set α
hsn : s.ncard = n + 1 + 1
hsn' : n + 1 + 2 < Nat.card α
hprim : IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s)
hα : Finite α
succ : 0 < n + 1 + 1
⊢ s.Nonempty

Tactic:
rw [← Set.ncard_pos, hsn]

Premises used: Set.ncard_pos
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
n : ℕ
hrec :
  ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_2 : MulAction G α] (hG : IsPreprimitive G α) {s : Set α}
    (hsn : s.ncard = n + 1) (hsn' : n + 2 < Nat.card α)
    (hprim : IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s)) (hα : Finite α),
    IsMultiplyPreprimitive G α (n + 2)
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
hG : IsPreprimitive G α
s : Set α
hsn : s.ncard = n + 1 + 1
hsn' : n + 1 + 2 < Nat.card α
hprim : IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s)
hα : Finite α
⊢ 0 < n + 1 + 1

Tactic:
apply Nat.succ_pos

Premises used: Nat.succ_pos
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
G : Subgroup (Perm α)
inst : Finite α
hα : Nat.card α ≤ 2
hG : Nontrivial.{u_1} ↥G
h : Nat.card.{u_1} (Perm α) ≤ Nat.card.{u_1} ↥G
⊢ G = ⊤

Tactic:
apply Subgroup.eq_top_of_le_card

Premises used: Subgroup.eq_top_of_le_card
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
G : Subgroup (Perm α)
inst : Finite α
hα : Nat.card α ≤ 2
hG : Nontrivial.{u_1} ↥G
h : (Nat.card α).factorial ≤ Nat.card.{u_1} ↥G
⊢ Nat.card.{u_1} (Perm α) ≤ Nat.card.{u_1} ↥G

Tactic:
rw [Nat.card_perm]

Premises used: Nat.card_perm
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
G : Subgroup (Perm α)
inst : Finite α
hα : Nat.card α ≤ 2
hG : Nontrivial.{u_1} ↥G
h : Nat.factorial 2 ≤ Nat.card.{u_1} ↥G
⊢ (Nat.card α).factorial ≤ Nat.card.{u_1} ↥G

Tactic:
apply (Nat.factorial_le hα).trans

Premises used: Nat.factorial_le, LE.le.trans
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
G : Subgroup (Perm α)
inst : Finite α
hα : Nat.card α ≤ 2
hG : Nontrivial.{u_1} ↥G
h : 2 ≤ Nat.card.{u_1} ↥G
h₁ : 1 < Nat.card.{u_1} ↥G
h₂ : G ≠ ⊥
h₃ h₄ h₅ h₆ : Nontrivial.{u_1} ↥G
⊢ Nat.factorial 2 ≤ Nat.card.{u_1} ↥G

Tactic:
rwa [Nat.factorial_two, Nat.succ_le_iff, one_lt_card_iff_ne_bot, ← nontrivial_iff_ne_bot]

Premises used: Subgroup.one_lt_card_iff_ne_bot, Nat.factorial_two, Nat.succ_le_iff, Subgroup.nontrivial_iff_ne_bot
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
K : Type u_2
inst : Group K
inst_1 : MulAction K α
hα : Nat.card α = 2
hK : fixedPoints K α ≠ _root_.Set.univ
n : ℕ
h : Infinite α
⊢ False

Tactic:
simp [Nat.card_eq_zero_of_infinite] at hα

Premises used: Nat.card_eq_zero_of_infinite
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
K : Type u_2
inst : Group K
inst_1 : MulAction K α
hα : Nat.card α = 2
hK : fixedPoints K α ≠ _root_.Set.univ
n : ℕ
⊢ Finite α

Tactic:
have : Finite α := Or.resolve_right (finite_or_infinite α) (fun _ ↦ by
    simp [Nat.card_eq_zero_of_infinite] at hα)
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
K : Type u_2
inst : Group K
inst_1 : MulAction K α
hα : Nat.card α = 2
hK : fixedPoints K α ≠ _root_.Set.univ
n : ℕ
this : Finite α
have : ∀ (this : Fintype α), IsMultiplyPretransitive K α n
⊢ IsMultiplyPretransitive K α n

Tactic:
have : Fintype α := Fintype.ofFinite α
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
K : Type u_2
inst : Group K
inst_1 : MulAction K α
hα : Nat.card α = 2
hK : fixedPoints K α ≠ _root_.Set.univ
n : ℕ
this_1 : Finite α
this : Fintype α
h2 : IsMultiplyPretransitive K α 2
pos : ∀ (hn : n ≤ 2), IsMultiplyPretransitive K α n
neg : ∀ (hn : ¬n ≤ 2), IsMultiplyPretransitive K α n
⊢ IsMultiplyPretransitive K α n

Tactic:
by_cases hn : n ≤ 2
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
K : Type u_2
inst : Group K
inst_1 : MulAction K α
hα : Nat.card α = 2
hK : fixedPoints K α ≠ _root_.Set.univ
n : ℕ
this_1 : Finite α
this : Fintype α
h2 : IsMultiplyPretransitive K α 2
hn : n ≤ 2
pos : (↑2 : ℕ∞) ≤ ENat.card α
⊢ IsMultiplyPretransitive K α n

Tactic:
apply MulAction.isMultiplyPretransitive_of_le' hn

Premises used: MulAction.isMultiplyPretransitive_of_le'
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
K : Type u_2
inst : Group K
inst_1 : MulAction K α
hα : Nat.card α = 2
hK : fixedPoints K α ≠ _root_.Set.univ
n : ℕ
this_1 : Finite α
this : Fintype α
h2 : IsMultiplyPretransitive K α 2
hn : n ≤ 2
⊢ (↑2 : ℕ∞) ≤ ENat.card α

Tactic:
simp [← hα]
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
K : Type u_2
inst : Group K
inst_1 : MulAction K α
hα : Nat.card α = 2
hK : fixedPoints K α ≠ _root_.Set.univ
n : ℕ
this_1 : Finite α
this_2 : Fintype α
h2 : IsMultiplyPretransitive K α 2
hn : ¬n ≤ 2
this : IsEmpty.{max 1 (u_1 + 1)} (Fin n ↪ α)
⊢ IsMultiplyPretransitive K α n

Tactic:
infer_instance
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
K : Type u_2
inst : Group K
inst_1 : MulAction K α
hα : Nat.card α = 2
hK : fixedPoints K α ≠ _root_.Set.univ
n : ℕ
this_1 : Finite α
this : Fintype α
h2 : IsMultiplyPretransitive K α 2
hn : ¬n ≤ 2
neg : IsEmpty.{max 1 (u_1 + 1)} (Fin n ↪ α)
⊢ IsMultiplyPretransitive K α n

Tactic:
suffices (IsEmpty (Fin n ↪ α)) by infer_instance
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
K : Type u_2
inst : Group K
inst_1 : MulAction K α
hα : Nat.card α = 2
hK : fixedPoints K α ≠ _root_.Set.univ
n : ℕ
this_1 : Finite α
this : Fintype α
h2 : IsMultiplyPretransitive K α 2
hn : ¬n ≤ 2
neg : ¬Nonempty.{u_1 + 1} (Fin n ↪ α)
neg₁ : ¬Fintype.card (Fin n) ≤ Fintype.card α
neg₂ : ¬n ≤ Fintype.card α
neg₃ : ¬n ≤ Nat.card α
neg₄ neg₅ neg₆ neg₇ : ¬n ≤ 2
⊢ IsEmpty.{max 1 (u_1 + 1)} (Fin n ↪ α)

Tactic:
rwa [← not_nonempty_iff, Function.Embedding.nonempty_iff_card_le, Fintype.card_fin,
        ← Nat.card_eq_fintype_card, hα]

Premises used: Fintype.card_fin, Function.Embedding.nonempty_iff_card_le, not_nonempty_iff, Nat.card_eq_fintype_card
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
K : Type u_2
inst : Group K
inst_1 : MulAction K α
hα : Nat.card α = 2
hK : fixedPoints K α ≠ _root_.Set.univ
n : ℕ
this_1 : Finite α
this : Fintype α
suffices : IsMultiplyPretransitive K α 2
⊢ IsMultiplyPretransitive K α n

Tactic:
suffices h2 : IsMultiplyPretransitive K α 2 by
    by_cases hn : n ≤ 2
    · apply MulAction.isMultiplyPretransitive_of_le' hn
      simp [← hα]
    · suffices (IsEmpty (Fin n ↪ α)) by infer_instance
      rwa [← not_nonempty_iff, Function.Embedding.nonempty_iff_card_le, Fintype.card_fin,
        ← Nat.card_eq_fintype_card, hα]
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
K : Type u_2
inst : Group K
inst_1 : MulAction K α
hα : Nat.card α = 2
hK : fixedPoints K α ≠ _root_.Set.univ
n : ℕ
this_1 : Finite α
this : Fintype α
φ : MonoidHom.{u_2, u_1} K (Perm α) := toPermHom K α
f : MulActionHom.{u_2, u_1, u_1, u_1} (M := K) (N := Perm α) (⇑φ : (a : K) → Perm α) α α :=
  { toFun := id, map_smul' := ⋯ }
⊢ Function.Bijective (α := α) (β := α) (⇑f : (a : α) → α)

Tactic:
have hf : Function.Bijective f := Function.bijective_id
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
K : Type u_2
inst : Group K
inst_1 : MulAction K α
hα : Nat.card α = 2
hK : fixedPoints K α ≠ _root_.Set.univ
n : ℕ
this_1 : Finite α
this_2 : Fintype α
φ : MonoidHom.{u_2, u_1} K (Perm α) := toPermHom K α
f : MulActionHom.{u_2, u_1, u_1, u_1} (M := K) (N := Perm α) (⇑φ : (a : K) → Perm α) α α :=
  { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective (α := α) (β := α) (⇑f : (a : α) → α)
this : Function.Surjective.{u_2 + 1, u_1 + 1} (α := K) (β := Perm α) (⇑φ : (a : K) → Perm α)
rw : IsPretransitive.{u_1, u_1} (Perm α) (Fin (Nat.card α) ↪ α)
⊢ IsPretransitive.{u_2, u_1} K (Fin 2 ↪ α)

Tactic:
rw [IsPretransitive.of_embedding_congr this hf (n := Fin 2), ← hα]

Premises used: MulAction.IsPretransitive.of_embedding_congr
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
K : Type u_2
inst : Group K
inst_1 : MulAction K α
hα : Nat.card α = 2
hK : fixedPoints K α ≠ _root_.Set.univ
n : ℕ
this_1 : Finite α
this_2 : Fintype α
φ : MonoidHom.{u_2, u_1} K (Perm α) := toPermHom K α
f : MulActionHom.{u_2, u_1, u_1, u_1} (M := K) (N := Perm α) (⇑φ : (a : K) → Perm α) α α :=
  { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective (α := α) (β := α) (⇑f : (a : α) → α)
this : Function.Surjective.{u_2 + 1, u_1 + 1} (α := K) (β := Perm α) (⇑φ : (a : K) → Perm α)
⊢ IsPretransitive.{u_1, u_1} (Perm α) (Fin (Nat.card α) ↪ α)

Tactic:
apply Perm.isMultiplyPretransitive

Premises used: Equiv.Perm.isMultiplyPretransitive
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
K : Type u_2
inst : Group K
inst_1 : MulAction K α
hα : Nat.card α = 2
hK : fixedPoints K α ≠ _root_.Set.univ
n : ℕ
this_1 : Finite α
this : Fintype α
φ : MonoidHom.{u_2, u_1} K (Perm α) := toPermHom K α
f : MulActionHom.{u_2, u_1, u_1, u_1} (M := K) (N := Perm α) (⇑φ : (a : K) → Perm α) α α :=
  { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective (α := α) (β := α) (⇑f : (a : α) → α)
suffices : Function.Surjective.{u_2 + 1, u_1 + 1} (α := K) (β := Perm α) (⇑φ : (a : K) → Perm α)
⊢ IsMultiplyPretransitive K α 2

Tactic:
suffices Function.Surjective φ by
    unfold IsMultiplyPretransitive
    rw [IsPretransitive.of_embedding_congr this hf (n := Fin 2), ← hα]
    apply Perm.isMultiplyPretransitive
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
K : Type u_2
inst : Group K
inst_1 : MulAction K α
hα : Nat.card α = 2
hK : fixedPoints K α ≠ _root_.Set.univ
n : ℕ
this_1 : Finite α
this : Fintype α
φ : MonoidHom.{u_2, u_1} K (Perm α) := toPermHom K α
f : MulActionHom.{u_2, u_1, u_1, u_1} (M := K) (N := Perm α) (⇑φ : (a : K) → Perm α) α α :=
  { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective (α := α) (β := α) (⇑f : (a : α) → α)
rw : φ.range = ⊤
⊢ Function.Surjective.{u_2 + 1, u_1 + 1} (α := K) (β := Perm α) (⇑φ : (a : K) → Perm α)

Tactic:
rw [← MonoidHom.range_eq_top]

Premises used: MonoidHom.range_eq_top