awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Hom (goal)
Goal:
M : Type u_1
inst : Monoid M
N : Type u_2
inst_1 : Monoid N
φ : M →* N
R : Type u_10
inst_2 : Semiring R
inst_3 : MulSemiringAction M R
S : Type u_12
inst_4 : Semiring S
inst_5 : MulSemiringAction N S
f : R →ₑ+*[φ] S
x : R
⊢ Eq.{u_12 + 1} (α := S) ((f.comp (MulSemiringActionHom.id M) : (a : R) → S) x : S) ((f : (a : R) → S) x : S)
have rw : Eq.{u_12 + 1} (α := S) ((f : (a : R) → S) ((MulSemiringActionHom.id M : (a : R) → R) x : R) : S)
  ((f : (a : R) → S) x : S)
Tactic: rw [comp_apply, id_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Hom (goal)
Goal:
M : Type u_1
inst : Monoid M
N : Type u_2
inst_1 : Monoid N
φ : M →* N
R : Type u_10
inst_2 : Semiring R
inst_3 : MulSemiringAction M R
S : Type u_12
inst_4 : Semiring S
inst_5 : MulSemiringAction N S
f : R →ₑ+*[φ] S
x : R
rw :
  Eq.{u_12 + 1} (α := S) ((f : (a : R) → S) ((MulSemiringActionHom.id M : (a : R) → R) x : R) : S)
    ((f : (a : R) → S) x : S)
⊢ Eq.{u_12 + 1} (α := S) ((f.comp (MulSemiringActionHom.id M) : (a : R) → S) x : S) ((f : (a : R) → S) x : S)
have rw₁ : Eq.{u_12 + 1} (α := S) ((f : (a : R) → S) x : S) ((f : (a : R) → S) x : S)
Tactic: rw [comp_apply, id_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.IterateAct (goal)
Goal:
α : Type u_1
f : α → α
a b c : IterateMulAct f
⊢ a * b * c = a * (b * c)
have val : (a * b * c).val = (a * (b * c)).val
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.IterateAct (goal)
Goal:
α : Type u_1
f : α → α
x : IterateMulAct f
⊢ 1 * x = x
have val : (1 * x).val = x.val
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.IterateAct (goal)
Goal:
α : Type u_1
f : α → α
x : IterateMulAct f
⊢ Eq (α := IterateMulAct f) { val := 0 * x.val } 1
have val : val.{u_1} (α := α) (f := f) { val := 0 * x.val : IterateMulAct f } = val.{u_1} (α := α) (f := f) 1
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.IterateAct (goal)
Goal:
α : Type u_1
f : α → α
n : ℕ
a : IterateMulAct f
⊢ { val := (n + 1) * a.val } = { val := n * a.val : IterateMulAct f } * a
have val : val.{u_1} (α := α) (f := f) { val := (n + 1) * a.val : IterateMulAct f } =
  ({ val := n * a.val : IterateMulAct f } * a).val
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.IterateAct (goal)
Goal:
α : Type u_1
f : α → α
x x_1 : IterateMulAct f
⊢ x * x_1 = x_1 * x
have val : (x * x_1).val = (x_1 * x).val
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Iwasawa (hypothesis)
Goal:
M : Type u_1
inst : Group M
α : Type u_2
inst_1 : MulAction M α
IwaS : IwasawaStructure M α
inst_2 : IsQuasiPreprimitive M α
N : Subgroup M
nN : N.Normal
hNX : fixedPoints.{u_1, u_2} (↥N) α ≠ Set.univ
⊢ commutator M ≤ N
have is_transN : IsPretransitive.{u_1, u_2} (↥N) α
Tactic: have is_transN := IsQuasiPreprimitive.isPretransitive_of_normal hNX
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Iwasawa (hypothesis)
Goal:
M : Type u_1
inst : Group M
α : Type u_2
inst_1 : MulAction M α
IwaS : IwasawaStructure M α
inst_2 : IsQuasiPreprimitive M α
N : Subgroup M
nN : N.Normal
hNX : fixedPoints.{u_1, u_2} (↥N) α ≠ Set.univ
is_transN : IsPretransitive.{u_1, u_2} (↥N) α
⊢ commutator M ≤ N
have ntα : Nontrivial α
Tactic: have ntα : Nontrivial α := nontrivial_of_fixedPoints_ne_univ hNX
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Iwasawa (goal)
Goal:
M : Type u_1
inst : Group M
α : Type u_2
inst_1 : MulAction M α
IwaS : IwasawaStructure M α
inst_2 : IsQuasiPreprimitive M α
N : Subgroup M
nN : N.Normal
hNX : fixedPoints.{u_1, u_2} (↥N) α ≠ Set.univ
is_transN : IsPretransitive.{u_1, u_2} (↥N) α
ntα : Nontrivial α
⊢ commutator M ≤ N
have obtain : ∀ (a : α), commutator M ≤ N
Tactic: obtain a : α := Nontrivial.to_nonempty.some
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Iwasawa (goal)
Goal:
M : Type u_1
inst : Group M
α : Type u_2
inst_1 : MulAction M α
IwaS : IwasawaStructure M α
inst_2 : IsQuasiPreprimitive M α
N : Subgroup M
nN : N.Normal
hNX : fixedPoints.{u_1, u_2} (↥N) α ≠ Set.univ
is_transN : IsPretransitive.{u_1, u_2} (↥N) α
ntα : Nontrivial α
a : α
⊢ commutator M ≤ N
have apply : N ⊔ IwaS.T a = ⊤
Tactic: apply nN.commutator_le_of_self_sup_commutative_eq_top ?_ (IwaS.is_comm a)
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Iwasawa (goal)
Goal:
M : Type u_1
inst : Group M
α : Type u_2
inst_1 : MulAction M α
IwaS : IwasawaStructure M α
inst_2 : IsQuasiPreprimitive M α
N : Subgroup M
nN : N.Normal
hNX : fixedPoints.{u_1, u_2} (↥N) α ≠ Set.univ
is_transN : IsPretransitive.{u_1, u_2} (↥N) α
ntα : Nontrivial α
a : α
⊢ N ⊔ IwaS.T a = ⊤
have rw : ∀ (i : α), IwaS.T i ≤ N ⊔ IwaS.T a
Tactic: rw [eq_top_iff, ← IwaS.is_generator, iSup_le_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Iwasawa (goal)
Goal:
M : Type u_1
inst : Group M
α : Type u_2
inst_1 : MulAction M α
IwaS : IwasawaStructure M α
inst_2 : IsQuasiPreprimitive M α
N : Subgroup M
nN : N.Normal
hNX : fixedPoints.{u_1, u_2} (↥N) α ≠ Set.univ
is_transN : IsPretransitive.{u_1, u_2} (↥N) α
ntα : Nontrivial α
a x : α
⊢ IwaS.T x ≤ N ⊔ IwaS.T a
have obtain : ∀ (g : ↥N), IwaS.T (g • a) ≤ N ⊔ IwaS.T a
Tactic: obtain ⟨g, rfl⟩ := MulAction.exists_smul_eq N a x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Iwasawa (goal)
Goal:
M : Type u_1
inst : Group M
α : Type u_2
inst_1 : MulAction M α
IwaS : IwasawaStructure M α
inst_2 : IsQuasiPreprimitive M α
N : Subgroup M
nN : N.Normal
hNX : fixedPoints.{u_1, u_2} (↥N) α ≠ Set.univ
is_transN : IsPretransitive.{u_1, u_2} (↥N) α
ntα : Nontrivial α
a : α
g : ↥N
⊢ IwaS.T (g • a) ≤ N ⊔ IwaS.T a
have rw : HSMul.hSMul (α := MulAut M) ((MulAut.conj : (a : M) → MulAut M) (↑g : M) : MulAut M) (IwaS.T a) ≤ N ⊔ IwaS.T a
Tactic: rw [Subgroup.smul_def, IwaS.is_conj g a]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Iwasawa (hypothesis)
Goal:
M : Type u_1
inst : Group M
α : Type u_2
inst_1 : MulAction M α
IwaS : IwasawaStructure M α
inst_2 : IsQuasiPreprimitive M α
N : Subgroup M
nN : N.Normal
hNX : fixedPoints.{u_1, u_2} (↥N) α ≠ Set.univ
is_transN : IsPretransitive.{u_1, u_2} (↥N) α
ntα : Nontrivial α
a : α
g : ↥N
k : M
hk : k ∈ (↑(IwaS.T a) : Set M)
⊢ Membership.mem (α := M) (N ⊔ IwaS.T a)
    ((((MulDistribMulAction.toMonoidEnd (MulAut M) M : (a : MulAut M) → Monoid.End M)
              ((MulAut.conj : (a : M) → MulAut M) (↑g : M)) :
            Monoid.End M) :
          (a : M) → M)
        k :
      M)
have hg' : (↑g : M) ∈ N ⊔ IwaS.T a
Tactic: have hg' : ↑g ∈ N ⊔ IwaS.T a := Subgroup.mem_sup_left (Subtype.mem g)
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Iwasawa (hypothesis)
Goal:
M : Type u_1
inst : Group M
α : Type u_2
inst_1 : MulAction M α
IwaS : IwasawaStructure M α
inst_2 : IsQuasiPreprimitive M α
N : Subgroup M
nN : N.Normal
hNX : fixedPoints.{u_1, u_2} (↥N) α ≠ Set.univ
is_transN : IsPretransitive.{u_1, u_2} (↥N) α
ntα : Nontrivial α
a : α
g : ↥N
k : M
hk : k ∈ (↑(IwaS.T a) : Set M)
hg' : (↑g : M) ∈ N ⊔ IwaS.T a
⊢ Membership.mem (α := M) (N ⊔ IwaS.T a)
    ((((MulDistribMulAction.toMonoidEnd (MulAut M) M : (a : MulAut M) → Monoid.End M)
              ((MulAut.conj : (a : M) → MulAut M) (↑g : M)) :
            Monoid.End M) :
          (a : M) → M)
        k :
      M)
have hk' : k ∈ N ⊔ IwaS.T a
Tactic: have hk' : k ∈ N ⊔ IwaS.T a := Subgroup.mem_sup_right hk
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Iwasawa (goal)
Goal:
M : Type u_1
inst : Group M
α : Type u_2
inst_1 : MulAction M α
inst_2 : Nontrivial M
is_perfect : Eq (α := Subgroup M) (commutator M) ⊤
inst_3 : IsQuasiPreprimitive M α
IwaS : IwasawaStructure M α
is_faithful : FaithfulSMul M α
⊢ IsSimpleGroup M
have eq_bot_or_eq_top_of_normal : ∀ (H : Subgroup M), H.Normal → H = ⊥ ∨ H = ⊤
Tactic: apply IsSimpleGroup.mk
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Iwasawa (goal)
Goal:
M : Type u_1
inst : Group M
α : Type u_2
inst_1 : MulAction M α
inst_2 : Nontrivial M
is_perfect : Eq (α := Subgroup M) (commutator M) ⊤
inst_3 : IsQuasiPreprimitive M α
IwaS : IwasawaStructure M α
is_faithful : FaithfulSMul M α
N : Subgroup M
nN : N.Normal
h : fixedPoints.{u_1, u_2} (↥N) α = Set.univ
⊢ N = ⊥ ∨ N = ⊤
have eq_bot_or_eq_top_of_normal : ∀ (n : M) (hn : n ∈ N), n = 1
Tactic: refine Or.inl (N.eq_bot_iff_forall.mpr fun n hn => ?_)
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Iwasawa (goal)
Goal:
M : Type u_1
inst : Group M
α : Type u_2
inst_1 : MulAction M α
inst_2 : Nontrivial M
is_perfect : Eq (α := Subgroup M) (commutator M) ⊤
inst_3 : IsQuasiPreprimitive M α
IwaS : IwasawaStructure M α
is_faithful : FaithfulSMul M α
N : Subgroup M
nN : N.Normal
h : fixedPoints.{u_1, u_2} (↥N) α = Set.univ
n : M
hn : n ∈ N
⊢ n = 1
have eq_bot_or_eq_top_of_normal : ∀ (a : α), n • a = HSMul.hSMul.{u_1, u_2, u_2} (α := M) 1 a
Tactic: apply is_faithful.eq_of_smul_eq_smul
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Iwasawa (goal)
Goal:
M : Type u_1
inst : Group M
α : Type u_2
inst_1 : MulAction M α
inst_2 : Nontrivial M
is_perfect : Eq (α := Subgroup M) (commutator M) ⊤
inst_3 : IsQuasiPreprimitive M α
IwaS : IwasawaStructure M α
is_faithful : FaithfulSMul M α
N : Subgroup M
nN : N.Normal
h : fixedPoints.{u_1, u_2} (↥N) α = Set.univ
n : M
hn : n ∈ N
x : α
⊢ n • x = HSMul.hSMul.{u_1, u_2, u_2} (α := M) 1 x
have eq_bot_or_eq_top_of_normal : n • x = x
Tactic: rw [one_smul]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Iwasawa (hypothesis)
Goal:
M : Type u_1
inst : Group M
α : Type u_2
inst_1 : MulAction M α
inst_2 : Nontrivial M
is_perfect : Eq (α := Subgroup M) (commutator M) ⊤
inst_3 : IsQuasiPreprimitive M α
IwaS : IwasawaStructure M α
is_faithful : FaithfulSMul M α
N : Subgroup M
nN : N.Normal
⊢ N = ⊥ ∨ N = ⊤
have x : fixedPoints.{u_1, u_2} (↥N) α = Set.univ ∨ commutator M ≤ N
Tactic: cases or_iff_not_imp_left.mpr (IwaS.commutator_le N) with
  | inl h =>
    refine Or.inl (N.eq_bot_iff_forall.mpr fun n hn => ?_)
    apply is_faithful.eq_of_smul_eq_smul
    intro x
    rw [one_smul]
    exact Set.eq_univ_iff_forall.mp h x ⟨n, hn⟩
  | inr h => exact Or.inr (top_le_iff.mp (le_trans (ge_of_eq is_perfect) h))
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
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 α
have rw : IsMultiplyPretransitive G α 1
Tactic: rw [← is_one_pretransitive_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (hypothesis)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
hsn' : 2 < ENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
⊢ Eq (α := Subgroup G) (normalClosure (↑(stabilizer G a) : Set G)) ⊤
have this : IsPretransitive G α
Tactic: have : IsPretransitive G α := by
    rw [← is_one_pretransitive_iff]
    exact isMultiplyPretransitive_of_le' (one_le_two) (le_of_lt hsn')
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
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 α
have rw : 1 < ENat.card α
Tactic: rw [← ENat.one_lt_card_iff_nontrivial]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (hypothesis)
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 α
⊢ Eq (α := Subgroup G) (normalClosure (↑(stabilizer G a) : Set G)) ⊤
have this₁ : Nontrivial α
Tactic: have : Nontrivial α := by
    rw [← ENat.one_lt_card_iff_nontrivial]
    exact lt_trans (by norm_num) hsn'
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
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)
have rw : IsPreprimitive G α
Tactic: rw [isCoatom_stabilizer_iff_preprimitive]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (hypothesis)
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 α
⊢ Eq (α := Subgroup G) (normalClosure (↑(stabilizer G a) : Set G)) ⊤
have hGa : 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'
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
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)
⊢ Eq (α := Subgroup G) (normalClosure (↑(stabilizer G a) : Set G)) ⊤
have a₁ : LT.lt (α := Subgroup G) (stabilizer G a) (normalClosure (↑(stabilizer G a) : Set G))
Tactic: apply hGa.right
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
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)
⊢ LT.lt (α := Subgroup G) (stabilizer G a) (normalClosure (↑(stabilizer G a) : Set G))
have a₁ : (↑(stabilizer G a) : Set G) ⊆ (↑(normalClosure (↑(stabilizer G a) : Set G)) : Set G)
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
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)
⊢ LT.lt (α := Subgroup G) (stabilizer G a) (normalClosure (↑(stabilizer G a) : Set G))
have a₂ : ¬(↑(normalClosure (↑(stabilizer G a) : Set G)) : Set G) ⊆ (↑(stabilizer G a) : Set G)
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
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)
have rw : 1 < ENat.card.{u_2} ↥(ofStabilizer G a)
Tactic: rw [← ENat.one_lt_card_iff_nontrivial]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
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)
⊢ 1 < ENat.card.{u_2} ↥(ofStabilizer G a)
have bc : HAdd.hAdd (α := ℕ∞) 1 1 < ENat.card.{u_2} ↥(ofStabilizer G a) + 1
Tactic: apply lt_of_add_lt_add_right
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
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
⊢ 1 < ENat.card.{u_2} ↥(ofStabilizer G a)
have a₁ : ℕ∞
Tactic: apply lt_of_add_lt_add_right
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (hypothesis)
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)
⊢ False
have this₁ : 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]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (hypothesis)
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)
⊢ False
have this₁ : ∃ (x : ↥(ofStabilizer G a)) (y : ↥(ofStabilizer G a)), x ≠ y
Tactic: rw [nontrivial_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
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
⊢ False
have a₁ : ∀ (b c : ↥(ofStabilizer G a)) (hbc : b ≠ c), False
Tactic: obtain ⟨b, c, hbc⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
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)
have rw : IsMultiplyPretransitive.{u_1, u_2} (↥(stabilizer G a)) (↥(ofStabilizer G a)) 1
Tactic: rw [← is_one_pretransitive_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (hypothesis)
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
⊢ False
have this₁ : 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]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
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)
⊢ False
have 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
Tactic: obtain ⟨⟨g, hg⟩, hgbc⟩ := exists_smul_eq (stabilizer G a) b c
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
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
⊢ False
have a₁ : b = c
Tactic: apply hbc
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
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
⊢ b = c
have a₁ : ∀
  (hgbc :
    (↑(Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (stabilizer G a) x) g hg • b) : α) = (↑c : α)),
  (↑b : α) = (↑c : α)
Tactic: rw [← SetLike.coe_eq_coe] at hgbc ⊢
Cleared hypotheses: hgbc
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
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 : α)
⊢ (↑b : α) = (↑c : α)
have a₁ : ∀ (h : G) (hinvab : h • (↑b : α) = a), (↑b : α) = (↑c : α)
Tactic: obtain ⟨h, hinvab⟩ := exists_smul_eq G (b : α) a
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (hypothesis)
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
⊢ (↑b : α) = (↑c : α)
have hinvab₁ : h⁻¹ • a = (↑b : α)
Tactic: rw [eq_comm, ← inv_smul_eq_iff] at hinvab
Cleared hypotheses: hinvab
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
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 : α)
⊢ (↑b : α) = (↑c : α)
have a₁ : h • Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (stabilizer G a) x) g hg • h⁻¹ • a = a
Tactic: rw [← hgbc, SetLike.val_smul, ← hinvab, inv_smul_eq_iff, eq_comm]