awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
hsn' : 2 < ENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
⊢ IsMultiplyPretransitive G α 1

Tactic:
isMultiplyPretransitive_of_le' (one_le_two) (le_of_lt hsn')

Premises used: le_of_lt, one_le_two, MulAction.isMultiplyPretransitive_of_le'
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
hsn' : 2 < ENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
⊢ IsMultiplyPretransitive G α 1

Tactic:
exact isMultiplyPretransitive_of_le' (one_le_two) (le_of_lt hsn')

Premises used: le_of_lt, one_le_two, MulAction.isMultiplyPretransitive_of_le'
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
hsn' : 2 < ENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
⊢ IsPretransitive G α

Tactic:
have : IsPretransitive G α := by
    rw [← is_one_pretransitive_iff]
    exact isMultiplyPretransitive_of_le' (one_le_two) (le_of_lt hsn')
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
hsn' : 2 < ENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
this : IsPretransitive G α
rw : 1 < ENat.card α
⊢ Nontrivial α

Tactic:
rw [← ENat.one_lt_card_iff_nontrivial]

Premises used: ENat.one_lt_card_iff_nontrivial
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
hsn' : 2 < ENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
this : IsPretransitive G α
⊢ LT.lt (α := ℕ∞) 1 2

Tactic:
norm_num
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
hsn' : 2 < ENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
this : IsPretransitive G α
⊢ 1 < ENat.card α

Tactic:
exact lt_trans (by norm_num) hsn'

Premises used: lt_trans
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
hsn' : 2 < ENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
this : IsPretransitive G α
⊢ Nontrivial α

Tactic:
have : Nontrivial α := by
    rw [← ENat.one_lt_card_iff_nontrivial]
    exact lt_trans (by norm_num) hsn'
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
hsn' : 2 < ENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
this_1 : IsPretransitive G α
this : Nontrivial α
rw : IsPreprimitive G α
⊢ IsCoatom (α := Subgroup G) (stabilizer G a)

Tactic:
rw [isCoatom_stabilizer_iff_preprimitive]

Premises used: MulAction.isCoatom_stabilizer_iff_preprimitive
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
hsn' : 2 < ENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
this_1 : IsPretransitive G α
this : Nontrivial α
⊢ IsPreprimitive G α

Tactic:
isPreprimitive_of_is_two_pretransitive hG'

Premises used: MulAction.isPreprimitive_of_is_two_pretransitive
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
hsn' : 2 < ENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
this_1 : IsPretransitive G α
this : Nontrivial α
⊢ IsPreprimitive G α

Tactic:
exact isPreprimitive_of_is_two_pretransitive hG'

Premises used: MulAction.isPreprimitive_of_is_two_pretransitive
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
hsn' : 2 < ENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
this_1 : IsPretransitive G α
this : Nontrivial α
⊢ IsCoatom (α := Subgroup G) (stabilizer G a)

Tactic:
have hGa : IsCoatom (stabilizer G a) := by
    rw [isCoatom_stabilizer_iff_preprimitive]
    exact isPreprimitive_of_is_two_pretransitive hG'
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
hsn' : 2 < ENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
this_1 : IsPretransitive G α
this : Nontrivial α
hGa : IsCoatom (α := Subgroup G) (stabilizer G a)
a₁ : LT.lt (α := Subgroup G) (stabilizer G a) (normalClosure (↑(stabilizer G a) : Set G))
⊢ Eq (α := Subgroup G) (normalClosure (↑(stabilizer G a) : Set G)) ⊤

Tactic:
apply hGa.right

Premises used: And.right
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
hsn' : 2 < ENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
this_1 : IsPretransitive G α
this : Nontrivial α
hGa : IsCoatom (α := Subgroup G) (stabilizer G a)
a₁ : (↑(stabilizer G a) : Set G) ⊆ (↑(normalClosure (↑(stabilizer G a) : Set G)) : Set G)
a₂ : ¬(↑(normalClosure (↑(stabilizer G a) : Set G)) : Set G) ⊆ (↑(stabilizer G a) : Set G)
⊢ LT.lt (α := Subgroup G) (stabilizer G a) (normalClosure (↑(stabilizer G a) : Set G))

Tactic:
constructor
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
hsn' : 2 < ENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
this_1 : IsPretransitive G α
this : Nontrivial α
hGa : IsCoatom (α := Subgroup G) (stabilizer G a)
⊢ (↑(stabilizer G a) : Set G) ⊆ (↑(normalClosure (↑(stabilizer G a) : Set G)) : Set G)

Tactic:
apply le_normalClosure

Premises used: Subgroup.le_normalClosure
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
hsn' : 2 < ENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
this_1 : IsPretransitive G α
this : Nontrivial α
hGa : IsCoatom (α := Subgroup G) (stabilizer G a)
hyp : (↑(normalClosure (↑(stabilizer G a) : Set G)) : Set G) ⊆ (↑(stabilizer G a) : Set G)
rw : 1 < ENat.card.{u_2} ↥(ofStabilizer G a)
⊢ Nontrivial.{u_2} ↥(ofStabilizer G a)

Tactic:
rw [← ENat.one_lt_card_iff_nontrivial]

Premises used: ENat.one_lt_card_iff_nontrivial
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
hsn' : 2 < ENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
this_1 : IsPretransitive G α
this : Nontrivial α
hGa : IsCoatom (α := Subgroup G) (stabilizer G a)
hyp : (↑(normalClosure (↑(stabilizer G a) : Set G)) : Set G) ⊆ (↑(stabilizer G a) : Set G)
bc : HAdd.hAdd (α := ℕ∞) 1 1 < ENat.card.{u_2} ↥(ofStabilizer G a) + 1
a₁ : ℕ∞
⊢ 1 < ENat.card.{u_2} ↥(ofStabilizer G a)

Tactic:
apply lt_of_add_lt_add_right

Premises used: lt_of_add_lt_add_right
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
hsn' : 2 < ENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
this_1 : IsPretransitive G α
this : Nontrivial α
hGa : IsCoatom (α := Subgroup G) (stabilizer G a)
hyp : (↑(normalClosure (↑(stabilizer G a) : Set G)) : Set G) ⊆ (↑(stabilizer G a) : Set G)
⊢ Nontrivial.{u_2} ↥(ofStabilizer G a)

Tactic:
have : Nontrivial (ofStabilizer G a) := by
      rw [← ENat.one_lt_card_iff_nontrivial]
      apply lt_of_add_lt_add_right
      rwa [ENat_card_ofStabilizer_add_one_eq]
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
hsn' : 2 < ENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
this_1 : IsPretransitive G α
this_2 : Nontrivial α
hGa : IsCoatom (α := Subgroup G) (stabilizer G a)
hyp : (↑(normalClosure (↑(stabilizer G a) : Set G)) : Set G) ⊆ (↑(stabilizer G a) : Set G)
this : Nontrivial.{u_2} ↥(ofStabilizer G a)
⊢ ∃ (x : ↥(ofStabilizer G a)) (y : ↥(ofStabilizer G a)), x ≠ y

Tactic:
rw [nontrivial_iff] at this

Premises used: nontrivial_iff
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
hsn' : 2 < ENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
this_1 : IsPretransitive G α
this_2 : Nontrivial α
hGa : IsCoatom (α := Subgroup G) (stabilizer G a)
hyp : (↑(normalClosure (↑(stabilizer G a) : Set G)) : Set G) ⊆ (↑(stabilizer G a) : Set G)
this : ∃ (x : ↥(ofStabilizer G a)) (y : ↥(ofStabilizer G a)), x ≠ y
a₁ : ∀ (b c : ↥(ofStabilizer G a)) (hbc : b ≠ c), False
⊢ False

Tactic:
obtain ⟨b, c, hbc⟩ := this
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
hsn' : 2 < ENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
this_1 : IsPretransitive G α
this : Nontrivial α
hGa : IsCoatom (α := Subgroup G) (stabilizer G a)
hyp : (↑(normalClosure (↑(stabilizer G a) : Set G)) : Set G) ⊆ (↑(stabilizer G a) : Set G)
b c : ↥(ofStabilizer G a)
hbc : b ≠ c
rw : IsMultiplyPretransitive.{u_1, u_2} (↥(stabilizer G a)) (↥(ofStabilizer G a)) 1
⊢ IsPretransitive.{u_1, u_2} ↥(stabilizer G a) ↥(ofStabilizer G a)

Tactic:
rw [← is_one_pretransitive_iff]

Premises used: MulAction.is_one_pretransitive_iff
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
hsn' : 2 < ENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
this_1 : IsPretransitive G α
this : Nontrivial α
hGa : IsCoatom (α := Subgroup G) (stabilizer G a)
hyp : (↑(normalClosure (↑(stabilizer G a) : Set G)) : Set G) ⊆ (↑(stabilizer G a) : Set G)
b c : ↥(ofStabilizer G a)
hbc : b ≠ c
rwa rwa₁ rwa₂ rwa₃ : IsMultiplyPretransitive G α (Nat.succ 1)
⊢ IsMultiplyPretransitive.{u_1, u_2} (↥(stabilizer G a)) (↥(ofStabilizer G a)) 1

Tactic:
rwa [← ofStabilizer.isMultiplyPretransitive]

Premises used: SubMulAction.ofStabilizer.isMultiplyPretransitive
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
hsn' : 2 < ENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
this_1 : IsPretransitive G α
this : Nontrivial α
hGa : IsCoatom (α := Subgroup G) (stabilizer G a)
hyp : (↑(normalClosure (↑(stabilizer G a) : Set G)) : Set G) ⊆ (↑(stabilizer G a) : Set G)
b c : ↥(ofStabilizer G a)
hbc : b ≠ c
⊢ IsPretransitive.{u_1, u_2} ↥(stabilizer G a) ↥(ofStabilizer G a)

Tactic:
have : IsPretransitive (stabilizer G a) (ofStabilizer G a) := by
      rw [← is_one_pretransitive_iff]
      rwa [← ofStabilizer.isMultiplyPretransitive]
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
hsn' : 2 < ENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
this_1 : IsPretransitive G α
this_2 : Nontrivial α
hGa : IsCoatom (α := Subgroup G) (stabilizer G a)
hyp : (↑(normalClosure (↑(stabilizer G a) : Set G)) : Set G) ⊆ (↑(stabilizer G a) : Set G)
b c : ↥(ofStabilizer G a)
hbc : b ≠ c
this : IsPretransitive.{u_1, u_2} ↥(stabilizer G a) ↥(ofStabilizer G a)
a₁ :
  ∀ (g : G) (hg : Membership.mem (γ := Subgroup G) (stabilizer G a) g)
    (hgbc : Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (stabilizer G a) x) g hg • b = c), False
⊢ False

Tactic:
obtain ⟨⟨g, hg⟩, hgbc⟩ := exists_smul_eq (stabilizer G a) b c

Premises used: Membership.mem, Subtype, MulAction.stabilizer, MulAction.exists_smul_eq
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
hsn' : 2 < ENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
this_1 : IsPretransitive G α
this_2 : Nontrivial α
hGa : IsCoatom (α := Subgroup G) (stabilizer G a)
hyp : (↑(normalClosure (↑(stabilizer G a) : Set G)) : Set G) ⊆ (↑(stabilizer G a) : Set G)
b c : ↥(ofStabilizer G a)
hbc : b ≠ c
this : IsPretransitive.{u_1, u_2} ↥(stabilizer G a) ↥(ofStabilizer G a)
g : G
hg : Membership.mem (γ := Subgroup G) (stabilizer G a) g
hgbc : Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (stabilizer G a) x) g hg • b = c
a₁ : b = c
⊢ False

Tactic:
apply hbc
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
hsn' : 2 < ENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
this_1 : IsPretransitive G α
this_2 : Nontrivial α
hGa : IsCoatom (α := Subgroup G) (stabilizer G a)
hyp : (↑(normalClosure (↑(stabilizer G a) : Set G)) : Set G) ⊆ (↑(stabilizer G a) : Set G)
b c : ↥(ofStabilizer G a)
hbc : b ≠ c
this : IsPretransitive.{u_1, u_2} ↥(stabilizer G a) ↥(ofStabilizer G a)
g : G
hg : Membership.mem (γ := Subgroup G) (stabilizer G a) g
hgbc : Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (stabilizer G a) x) g hg • b = c
a₁ :
  ∀
    (hgbc :
      (↑(Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (stabilizer G a) x) g hg • b) : α) = (↑c : α)),
    (↑b : α) = (↑c : α)
⊢ b = c

Tactic:
rw [← SetLike.coe_eq_coe] at hgbc ⊢

Premises used: SetLike.coe_eq_coe
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
hsn' : 2 < ENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
this_1 : IsPretransitive G α
this_2 : Nontrivial α
hGa : IsCoatom (α := Subgroup G) (stabilizer G a)
hyp : (↑(normalClosure (↑(stabilizer G a) : Set G)) : Set G) ⊆ (↑(stabilizer G a) : Set G)
b c : ↥(ofStabilizer G a)
hbc : b ≠ c
this : IsPretransitive.{u_1, u_2} ↥(stabilizer G a) ↥(ofStabilizer G a)
g : G
hg : Membership.mem (γ := Subgroup G) (stabilizer G a) g
hgbc : (↑(Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (stabilizer G a) x) g hg • b) : α) = (↑c : α)
a₁ : ∀ (h : G) (hinvab : h • (↑b : α) = a), (↑b : α) = (↑c : α)
⊢ (↑b : α) = (↑c : α)

Tactic:
obtain ⟨h, hinvab⟩ := exists_smul_eq G (b : α) a

Premises used: MulAction.exists_smul_eq, Subtype.val
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
hsn' : 2 < ENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
this_1 : IsPretransitive G α
this_2 : Nontrivial α
hGa : IsCoatom (α := Subgroup G) (stabilizer G a)
hyp : (↑(normalClosure (↑(stabilizer G a) : Set G)) : Set G) ⊆ (↑(stabilizer G a) : Set G)
b c : ↥(ofStabilizer G a)
hbc : b ≠ c
this : IsPretransitive.{u_1, u_2} ↥(stabilizer G a) ↥(ofStabilizer G a)
g : G
hg : Membership.mem (γ := Subgroup G) (stabilizer G a) g
hgbc : (↑(Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (stabilizer G a) x) g hg • b) : α) = (↑c : α)
h : G
hinvab : h • (↑b : α) = a
⊢ h⁻¹ • a = (↑b : α)

Tactic:
rw [eq_comm, ← inv_smul_eq_iff] at hinvab

Premises used: inv_smul_eq_iff, eq_comm
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
hsn' : 2 < ENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
this_1 : IsPretransitive G α
this_2 : Nontrivial α
hGa : IsCoatom (α := Subgroup G) (stabilizer G a)
hyp : (↑(normalClosure (↑(stabilizer G a) : Set G)) : Set G) ⊆ (↑(stabilizer G a) : Set G)
b c : ↥(ofStabilizer G a)
hbc : b ≠ c
this : IsPretransitive.{u_1, u_2} ↥(stabilizer G a) ↥(ofStabilizer G a)
g : G
hg : Membership.mem (γ := Subgroup G) (stabilizer G a) g
hgbc : (↑(Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (stabilizer G a) x) g hg • b) : α) = (↑c : α)
h : G
hinvab : h⁻¹ • a = (↑b : α)
a₁ : h • Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (stabilizer G a) x) g hg • h⁻¹ • a = a
⊢ (↑b : α) = (↑c : α)

Tactic:
rw [← hgbc, SetLike.val_smul, ← hinvab, inv_smul_eq_iff, eq_comm]

Premises used: inv_smul_eq_iff, eq_comm, SetLike.val_smul
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
hsn' : 2 < ENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
this_1 : IsPretransitive G α
this_2 : Nontrivial α
hGa : IsCoatom (α := Subgroup G) (stabilizer G a)
hyp : (↑(normalClosure (↑(stabilizer G a) : Set G)) : Set G) ⊆ (↑(stabilizer G a) : Set G)
b c : ↥(ofStabilizer G a)
hbc : b ≠ c
this : IsPretransitive.{u_1, u_2} ↥(stabilizer G a) ↥(ofStabilizer G a)
g : G
hg : Membership.mem (γ := Subgroup G) (stabilizer G a) g
hgbc : (↑(Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (stabilizer G a) x) g hg • b) : α) = (↑c : α)
h : G
hinvab : h⁻¹ • a = (↑b : α)
a₁ : Membership.mem (γ := Subgroup G) (stabilizer G a) (h * g * h⁻¹)
⊢ h • Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (stabilizer G a) x) g hg • h⁻¹ • a = a

Tactic:
simp only [subgroup_smul_def, smul_smul, ← mul_assoc, ← mem_stabilizer_iff]

Premises used: mul_assoc, smul_smul, MulAction.subgroup_smul_def, MulAction.mem_stabilizer_iff
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
hsn' : 2 < ENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
this_1 : IsPretransitive G α
this_2 : Nontrivial α
hGa : IsCoatom (α := Subgroup G) (stabilizer G a)
hyp : (↑(normalClosure (↑(stabilizer G a) : Set G)) : Set G) ⊆ (↑(stabilizer G a) : Set G)
b c : ↥(ofStabilizer G a)
hbc : b ≠ c
this : IsPretransitive.{u_1, u_2} ↥(stabilizer G a) ↥(ofStabilizer G a)
g : G
hg : Membership.mem (γ := Subgroup G) (stabilizer G a) g
hgbc : (↑(Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (stabilizer G a) x) g hg • b) : α) = (↑c : α)
h : G
hinvab : h⁻¹ • a = (↑b : α)
⊢ Membership.mem (γ := Subgroup G) (stabilizer G a) (h * g * h⁻¹)

Tactic:
hyp (normalClosure_normal.conj_mem g (le_normalClosure hg) h)

Premises used: Subgroup.le_normalClosure, Subgroup.normalClosure_normal, Subgroup.Normal.conj_mem
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
hsn' : 2 < ENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
this_1 : IsPretransitive G α
this_2 : Nontrivial α
hGa : IsCoatom (α := Subgroup G) (stabilizer G a)
hyp : (↑(normalClosure (↑(stabilizer G a) : Set G)) : Set G) ⊆ (↑(stabilizer G a) : Set G)
b c : ↥(ofStabilizer G a)
hbc : b ≠ c
this : IsPretransitive.{u_1, u_2} ↥(stabilizer G a) ↥(ofStabilizer G a)
g : G
hg : Membership.mem (γ := Subgroup G) (stabilizer G a) g
hgbc : (↑(Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (stabilizer G a) x) g hg • b) : α) = (↑c : α)
h : G
hinvab : h⁻¹ • a = (↑b : α)
⊢ Membership.mem (γ := Subgroup G) (stabilizer G a) (h * g * h⁻¹)

Tactic:
exact hyp (normalClosure_normal.conj_mem g (le_normalClosure hg) h)

Premises used: Subgroup.le_normalClosure, Subgroup.normalClosure_normal, Subgroup.Normal.conj_mem
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
n : ℕ
hrec :
  ∀ m < n,
    ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_2 : MulAction G α] (hG : IsPreprimitive G α) {s : Set α}
      (hsn : s.ncard = m + 1) (hsn' : m + 2 < Nat.card α),
      (IsPretransitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
        (IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 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
hsn' : n + 2 < Nat.card α
⊢ Finite α

Tactic:
have : Finite α := Nat.finite_of_card_ne_zero <| ne_zero_of_lt hsn'
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
n : ℕ
hrec :
  ∀ m < n,
    ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_2 : MulAction G α] (hG : IsPreprimitive G α) {s : Set α}
      (hsn : s.ncard = m + 1) (hsn' : m + 2 < Nat.card α),
      (IsPretransitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
        (IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 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
hsn' : n + 2 < Nat.card α
this : Finite α
hs : s = Set.univ
⊢ Nat.card α = n + 1

Tactic:
rw [hs, Set.ncard_univ] at hsn

Premises used: Set.ncard_univ
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
n : ℕ
hrec :
  ∀ m < n,
    ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_2 : MulAction G α] (hG : IsPreprimitive G α) {s : Set α}
      (hsn : s.ncard = m + 1) (hsn' : m + 2 < Nat.card α),
      (IsPretransitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
        (IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 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
hsn' : n + 2 < Nat.card α
this : Finite α
hs : s = Set.univ
hsn₁ : Nat.card α = n + 1
⊢ n + 2 < Nat.card α

Tactic:
rw [hs, Set.ncard_univ] at hsn

Premises used: Set.ncard_univ
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
n : ℕ
hrec :
  ∀ m < n,
    ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_2 : MulAction G α] (hG : IsPreprimitive G α) {s : Set α}
      (hsn : s.ncard = m + 1) (hsn' : m + 2 < Nat.card α),
      (IsPretransitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
        (IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 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
hsn' : n + 2 < Nat.card α
this : Finite α
hs : s = Set.univ
hsn₁ : Nat.card α = n + 1
hsn'₁ : n + 2 < Nat.card α
⊢ Finite α

Tactic:
rw [hs, Set.ncard_univ] at hsn

Premises used: Set.ncard_univ
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
n : ℕ
hrec :
  ∀ m < n,
    ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_2 : MulAction G α] (hG : IsPreprimitive G α) {s : Set α}
      (hsn : s.ncard = m + 1) (hsn' : m + 2 < Nat.card α),
      (IsPretransitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
        (IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 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
hsn' : n + 2 < Nat.card α
this : Finite α
hs : s = Set.univ
hsn₁ : Nat.card α = n + 1
hsn'₁ : n + 2 < Nat.card α
this₁ : Finite α
⊢ s = Set.univ

Tactic:
rw [hs, Set.ncard_univ] at hsn

Premises used: Set.ncard_univ
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
n : ℕ
hrec :
  ∀ m < n,
    ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_2 : MulAction G α] (hG : IsPreprimitive G α) {s : Set α}
      (hsn : s.ncard = m + 1) (hsn' : m + 2 < Nat.card α),
      (IsPretransitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
        (IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
hG : IsPreprimitive G α
s : Set α
hsn : Nat.card α = n + 1
hsn' : n + 2 < Nat.card α
this : Finite α
hs : s = Set.univ
⊢ False

Tactic:
simp only [hsn, add_lt_add_iff_left, Nat.not_ofNat_lt_one] at hsn'

Premises used: Nat.not_ofNat_lt_one, add_lt_add_iff_left
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
n : ℕ
hrec :
  ∀ m < n,
    ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_2 : MulAction G α] (hG : IsPreprimitive G α) {s : Set α}
      (hsn : s.ncard = m + 1) (hsn' : m + 2 < Nat.card α),
      (IsPretransitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
        (IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 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
hsn' : n + 2 < Nat.card α
this : Finite α
⊢ s ≠ Set.univ

Tactic:
have hs_ne_univ : s ≠ Set.univ := by
    intro hs
    rw [hs, Set.ncard_univ] at hsn
    simp only [hsn, add_lt_add_iff_left, Nat.not_ofNat_lt_one] at hsn'