internlm/Lean-Github huggingface dataset:
Theorem: normalClosure_of_stabilizer_eq_top
Proof state before:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : 2 < PartENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
⊢ 1 < 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: normalClosure_of_stabilizer_eq_top
Proof state before:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : 2 < PartENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this : Nontrivial α
⊢ Subgroup.IsMaximal (stabilizer G a)
Tactic:
rw [maximal_stabilizer_iff_preprimitive G a]
Proof state after:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : 2 < PartENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this : Nontrivial α
⊢ IsPreprimitive G α
Theorem: normalClosure_of_stabilizer_eq_top
Proof state before:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : 2 < PartENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this : Nontrivial α
⊢ IsPreprimitive G α
Tactic:
exact hG'.isPreprimitive_of_two
Proof state after:
no goals
Theorem: normalClosure_of_stabilizer_eq_top
Proof state before:
case a.left
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : 2 < PartENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this : Nontrivial α
hGa : IsCoatom (stabilizer G a)
⊢ ↑(stabilizer G a) ⊆ ↑(Subgroup.normalClosure ↑(stabilizer G a))
Tactic:
apply Subgroup.le_normalClosure
Proof state after:
no goals
Theorem: normalClosure_of_stabilizer_eq_top
Proof state before:
case a.right
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : 2 < PartENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this : Nontrivial α
hGa : IsCoatom (stabilizer G a)
⊢ ¬↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
Tactic:
intro hyp
Proof state after:
case a.right
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : 2 < PartENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
⊢ False
Theorem: normalClosure_of_stabilizer_eq_top
Proof state before:
case a.right
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : 2 < PartENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
⊢ False
Tactic:
have : Nontrivial (SubMulAction.ofStabilizer G a) := by
  apply Set.Nontrivial.coe_sort
  rw [← Set.one_lt_encard_iff_nontrivial]
  rw [← not_le, ← Nat.cast_one, ← WithTop.add_one_le_coe_succ_iff, not_le]
  rw [← PartENat.withTopEquiv_lt, ← Set.encard_univ] at hsn'
  convert hsn'
  simp only [SetLike.coe_sort_coe, Nat.cast_succ, Nat.cast_one]
  rw [← Nat.cast_two]
  rw [← PartENat.withTopEquiv.symm_apply_eq]
  rfl
  rw [add_comm]
  exact SubMulAction.add_encard_ofStabilizer_eq' a
Proof state after:
case a.right
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : 2 < PartENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this✝ : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
this : Nontrivial ↥(SubMulAction.ofStabilizer G a)
⊢ False
Theorem: normalClosure_of_stabilizer_eq_top
Proof state before:
case a.right
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : 2 < PartENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this✝ : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
this : Nontrivial ↥(SubMulAction.ofStabilizer G a)
⊢ False
Tactic:
rw [nontrivial_iff] at this
Proof state after:
case a.right
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : 2 < PartENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this✝ : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
this : ∃ x y, x ≠ y
⊢ False
Theorem: normalClosure_of_stabilizer_eq_top
Proof state before:
case a.right
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : 2 < PartENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this✝ : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
this : ∃ x y, x ≠ y
⊢ False
Tactic:
obtain ⟨b, c, hbc⟩ := this
Proof state after:
case a.right.intro.intro
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : 2 < PartENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
b c : ↥(SubMulAction.ofStabilizer G a)
hbc : b ≠ c
⊢ False
Theorem: normalClosure_of_stabilizer_eq_top
Proof state before:
case a.right.intro.intro
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : 2 < PartENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
b c : ↥(SubMulAction.ofStabilizer G a)
hbc : b ≠ c
⊢ False
Tactic:
have : IsPretransitive (stabilizer G a) (SubMulAction.ofStabilizer G a) := by
  rw [isPretransitive_iff_is_one_pretransitive]
  exact (stabilizer.isMultiplyPretransitive G α hG).mp hG'
Proof state after:
case a.right.intro.intro
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : 2 < PartENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this✝ : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
b c : ↥(SubMulAction.ofStabilizer G a)
hbc : b ≠ c
this : IsPretransitive ↥(stabilizer G a) ↥(SubMulAction.ofStabilizer G a)
⊢ False
Theorem: normalClosure_of_stabilizer_eq_top
Proof state before:
case a.right.intro.intro
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : 2 < PartENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this✝ : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
b c : ↥(SubMulAction.ofStabilizer G a)
hbc : b ≠ c
this : IsPretransitive ↥(stabilizer G a) ↥(SubMulAction.ofStabilizer G a)
⊢ False
Tactic:
obtain ⟨⟨g, hg⟩, hgbc⟩ := exists_smul_eq (stabilizer G a) b c
Proof state after:
case a.right.intro.intro.intro.mk
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : 2 < PartENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this✝ : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
b c : ↥(SubMulAction.ofStabilizer G a)
hbc : b ≠ c
this : IsPretransitive ↥(stabilizer G a) ↥(SubMulAction.ofStabilizer G a)
g : G
hg : g ∈ stabilizer G a
hgbc : { val := g, property := hg } • b = c
⊢ False
Theorem: normalClosure_of_stabilizer_eq_top
Proof state before:
case a.right.intro.intro.intro.mk
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : 2 < PartENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this✝ : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
b c : ↥(SubMulAction.ofStabilizer G a)
hbc : b ≠ c
this : IsPretransitive ↥(stabilizer G a) ↥(SubMulAction.ofStabilizer G a)
g : G
hg : g ∈ stabilizer G a
hgbc : { val := g, property := hg } • b = c
⊢ False
Tactic:
apply hbc
Proof state after:
case a.right.intro.intro.intro.mk
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : 2 < PartENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this✝ : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
b c : ↥(SubMulAction.ofStabilizer G a)
hbc : b ≠ c
this : IsPretransitive ↥(stabilizer G a) ↥(SubMulAction.ofStabilizer G a)
g : G
hg : g ∈ stabilizer G a
hgbc : { val := g, property := hg } • b = c
⊢ b = c
Theorem: normalClosure_of_stabilizer_eq_top
Proof state before:
case a.right.intro.intro.intro.mk
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : 2 < PartENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this✝ : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
b c : ↥(SubMulAction.ofStabilizer G a)
hbc : b ≠ c
this : IsPretransitive ↥(stabilizer G a) ↥(SubMulAction.ofStabilizer G a)
g : G
hg : g ∈ stabilizer G a
hgbc : { val := g, property := hg } • b = c
⊢ b = c
Tactic:
rw [← SetLike.coe_eq_coe]
Proof state after:
case a.right.intro.intro.intro.mk
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : 2 < PartENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this✝ : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
b c : ↥(SubMulAction.ofStabilizer G a)
hbc : b ≠ c
this : IsPretransitive ↥(stabilizer G a) ↥(SubMulAction.ofStabilizer G a)
g : G
hg : g ∈ stabilizer G a
hgbc : { val := g, property := hg } • b = c
⊢ ↑b = ↑c
Theorem: normalClosure_of_stabilizer_eq_top
Proof state before:
case a.right.intro.intro.intro.mk
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : 2 < PartENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this✝ : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
b c : ↥(SubMulAction.ofStabilizer G a)
hbc : b ≠ c
this : IsPretransitive ↥(stabilizer G a) ↥(SubMulAction.ofStabilizer G a)
g : G
hg : g ∈ stabilizer G a
hgbc : { val := g, property := hg } • b = c
⊢ ↑b = ↑c
Tactic:
rw [← SetLike.coe_eq_coe] at hgbc
Proof state after:
case a.right.intro.intro.intro.mk
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : 2 < PartENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this✝ : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
b c : ↥(SubMulAction.ofStabilizer G a)
hbc : b ≠ c
this : IsPretransitive ↥(stabilizer G a) ↥(SubMulAction.ofStabilizer G a)
g : G
hg : g ∈ stabilizer G a
hgbc : ↑({ val := g, property := hg } • b) = ↑c
⊢ ↑b = ↑c
Theorem: normalClosure_of_stabilizer_eq_top
Proof state before:
case a.right.intro.intro.intro.mk
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : 2 < PartENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this✝ : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
b c : ↥(SubMulAction.ofStabilizer G a)
hbc : b ≠ c
this : IsPretransitive ↥(stabilizer G a) ↥(SubMulAction.ofStabilizer G a)
g : G
hg : g ∈ stabilizer G a
hgbc : ↑({ val := g, property := hg } • b) = ↑c
⊢ ↑b = ↑c
Tactic:
obtain ⟨h, hinvab⟩ := exists_smul_eq G (b : α) a
Proof state after:
case a.right.intro.intro.intro.mk.intro
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : 2 < PartENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this✝ : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
b c : ↥(SubMulAction.ofStabilizer G a)
hbc : b ≠ c
this : IsPretransitive ↥(stabilizer G a) ↥(SubMulAction.ofStabilizer G a)
g : G
hg : g ∈ stabilizer G a
hgbc : ↑({ val := g, property := hg } • b) = ↑c
h : G
hinvab : h • ↑b = a
⊢ ↑b = ↑c
Theorem: normalClosure_of_stabilizer_eq_top
Proof state before:
case a.right.intro.intro.intro.mk.intro
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : 2 < PartENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this✝ : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
b c : ↥(SubMulAction.ofStabilizer G a)
hbc : b ≠ c
this : IsPretransitive ↥(stabilizer G a) ↥(SubMulAction.ofStabilizer G a)
g : G
hg : g ∈ stabilizer G a
hgbc : ↑({ val := g, property := hg } • b) = ↑c
h : G
hinvab : h • ↑b = a
⊢ ↑b = ↑c
Tactic:
rw [eq_comm, ← inv_smul_eq_iff] at hinvab
Proof state after:
case a.right.intro.intro.intro.mk.intro
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : 2 < PartENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this✝ : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
b c : ↥(SubMulAction.ofStabilizer G a)
hbc : b ≠ c
this : IsPretransitive ↥(stabilizer G a) ↥(SubMulAction.ofStabilizer G a)
g : G
hg : g ∈ stabilizer G a
hgbc : ↑({ val := g, property := hg } • b) = ↑c
h : G
hinvab : h⁻¹ • a = ↑b
⊢ ↑b = ↑c
Theorem: normalClosure_of_stabilizer_eq_top
Proof state before:
case a.right.intro.intro.intro.mk.intro
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : 2 < PartENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this✝ : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
b c : ↥(SubMulAction.ofStabilizer G a)
hbc : b ≠ c
this : IsPretransitive ↥(stabilizer G a) ↥(SubMulAction.ofStabilizer G a)
g : G
hg : g ∈ stabilizer G a
hgbc : ↑({ val := g, property := hg } • b) = ↑c
h : G
hinvab : h⁻¹ • a = ↑b
⊢ ↑b = ↑c
Tactic:
rw [← hgbc, SetLike.val_smul, ← hinvab]
Proof state after:
case a.right.intro.intro.intro.mk.intro
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : 2 < PartENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this✝ : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
b c : ↥(SubMulAction.ofStabilizer G a)
hbc : b ≠ c
this : IsPretransitive ↥(stabilizer G a) ↥(SubMulAction.ofStabilizer G a)
g : G
hg : g ∈ stabilizer G a
hgbc : ↑({ val := g, property := hg } • b) = ↑c
h : G
hinvab : h⁻¹ • a = ↑b
⊢ h⁻¹ • a = { val := g, property := hg } • h⁻¹ • a
Theorem: normalClosure_of_stabilizer_eq_top
Proof state before:
case a.right.intro.intro.intro.mk.intro
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : 2 < PartENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this✝ : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
b c : ↥(SubMulAction.ofStabilizer G a)
hbc : b ≠ c
this : IsPretransitive ↥(stabilizer G a) ↥(SubMulAction.ofStabilizer G a)
g : G
hg : g ∈ stabilizer G a
hgbc : ↑({ val := g, property := hg } • b) = ↑c
h : G
hinvab : h⁻¹ • a = ↑b
⊢ h⁻¹ • a = { val := g, property := hg } • h⁻¹ • a
Tactic:
rw [inv_smul_eq_iff, eq_comm]
Proof state after:
case a.right.intro.intro.intro.mk.intro
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : 2 < PartENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this✝ : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
b c : ↥(SubMulAction.ofStabilizer G a)
hbc : b ≠ c
this : IsPretransitive ↥(stabilizer G a) ↥(SubMulAction.ofStabilizer G a)
g : G
hg : g ∈ stabilizer G a
hgbc : ↑({ val := g, property := hg } • b) = ↑c
h : G
hinvab : h⁻¹ • a = ↑b
⊢ h • { val := g, property := hg } • h⁻¹ • a = a
Theorem: normalClosure_of_stabilizer_eq_top
Proof state before:
case a.right.intro.intro.intro.mk.intro
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : 2 < PartENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this✝ : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
b c : ↥(SubMulAction.ofStabilizer G a)
hbc : b ≠ c
this : IsPretransitive ↥(stabilizer G a) ↥(SubMulAction.ofStabilizer G a)
g : G
hg : g ∈ stabilizer G a
hgbc : ↑({ val := g, property := hg } • b) = ↑c
h : G
hinvab : h⁻¹ • a = ↑b
⊢ h • { val := g, property := hg } • h⁻¹ • a = a
Tactic:
change h • g • h⁻¹ • a = a
Proof state after:
case a.right.intro.intro.intro.mk.intro
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : 2 < PartENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this✝ : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
b c : ↥(SubMulAction.ofStabilizer G a)
hbc : b ≠ c
this : IsPretransitive ↥(stabilizer G a) ↥(SubMulAction.ofStabilizer G a)
g : G
hg : g ∈ stabilizer G a
hgbc : ↑({ val := g, property := hg } • b) = ↑c
h : G
hinvab : h⁻¹ • a = ↑b
⊢ h • g • h⁻¹ • a = a
Theorem: normalClosure_of_stabilizer_eq_top
Proof state before:
case a.right.intro.intro.intro.mk.intro
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : 2 < PartENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this✝ : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
b c : ↥(SubMulAction.ofStabilizer G a)
hbc : b ≠ c
this : IsPretransitive ↥(stabilizer G a) ↥(SubMulAction.ofStabilizer G a)
g : G
hg : g ∈ stabilizer G a
hgbc : ↑({ val := g, property := hg } • b) = ↑c
h : G
hinvab : h⁻¹ • a = ↑b
⊢ h • g • h⁻¹ • a = a
Tactic:
simp only [smul_smul, ← mul_assoc]
Proof state after:
case a.right.intro.intro.intro.mk.intro
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : 2 < PartENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this✝ : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
b c : ↥(SubMulAction.ofStabilizer G a)
hbc : b ≠ c
this : IsPretransitive ↥(stabilizer G a) ↥(SubMulAction.ofStabilizer G a)
g : G
hg : g ∈ stabilizer G a
hgbc : ↑({ val := g, property := hg } • b) = ↑c
h : G
hinvab : h⁻¹ • a = ↑b
⊢ (h * g * h⁻¹) • a = a
Theorem: normalClosure_of_stabilizer_eq_top
Proof state before:
case a.right.intro.intro.intro.mk.intro
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : 2 < PartENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this✝ : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
b c : ↥(SubMulAction.ofStabilizer G a)
hbc : b ≠ c
this : IsPretransitive ↥(stabilizer G a) ↥(SubMulAction.ofStabilizer G a)
g : G
hg : g ∈ stabilizer G a
hgbc : ↑({ val := g, property := hg } • b) = ↑c
h : G
hinvab : h⁻¹ • a = ↑b
⊢ (h * g * h⁻¹) • a = a
Tactic:
rw [← mem_stabilizer_iff]
Proof state after:
case a.right.intro.intro.intro.mk.intro
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : 2 < PartENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this✝ : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
b c : ↥(SubMulAction.ofStabilizer G a)
hbc : b ≠ c
this : IsPretransitive ↥(stabilizer G a) ↥(SubMulAction.ofStabilizer G a)
g : G
hg : g ∈ stabilizer G a
hgbc : ↑({ val := g, property := hg } • b) = ↑c
h : G
hinvab : h⁻¹ • a = ↑b
⊢ h * g * h⁻¹ ∈ stabilizer G a
Theorem: normalClosure_of_stabilizer_eq_top
Proof state before:
case a.right.intro.intro.intro.mk.intro
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : 2 < PartENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this✝ : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
b c : ↥(SubMulAction.ofStabilizer G a)
hbc : b ≠ c
this : IsPretransitive ↥(stabilizer G a) ↥(SubMulAction.ofStabilizer G a)
g : G
hg : g ∈ stabilizer G a
hgbc : ↑({ val := g, property := hg } • b) = ↑c
h : G
hinvab : h⁻¹ • a = ↑b
⊢ h * g * h⁻¹ ∈ stabilizer G a
Tactic:
apply hyp
Proof state after:
case a.right.intro.intro.intro.mk.intro.a
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : 2 < PartENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this✝ : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
b c : ↥(SubMulAction.ofStabilizer G a)
hbc : b ≠ c
this : IsPretransitive ↥(stabilizer G a) ↥(SubMulAction.ofStabilizer G a)
g : G
hg : g ∈ stabilizer G a
hgbc : ↑({ val := g, property := hg } • b) = ↑c
h : G
hinvab : h⁻¹ • a = ↑b
⊢ h * g * h⁻¹ ∈ ↑(Subgroup.normalClosure ↑(stabilizer G a))
Theorem: normalClosure_of_stabilizer_eq_top
Proof state before:
case a.right.intro.intro.intro.mk.intro.a
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : 2 < PartENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this✝ : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
b c : ↥(SubMulAction.ofStabilizer G a)
hbc : b ≠ c
this : IsPretransitive ↥(stabilizer G a) ↥(SubMulAction.ofStabilizer G a)
g : G
hg : g ∈ stabilizer G a
hgbc : ↑({ val := g, property := hg } • b) = ↑c
h : G
hinvab : h⁻¹ • a = ↑b
⊢ h * g * h⁻¹ ∈ ↑(Subgroup.normalClosure ↑(stabilizer G a))
Tactic:
apply Subgroup.normalClosure_normal.conj_mem
Proof state after:
case a.right.intro.intro.intro.mk.intro.a.a
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : 2 < PartENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this✝ : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
b c : ↥(SubMulAction.ofStabilizer G a)
hbc : b ≠ c
this : IsPretransitive ↥(stabilizer G a) ↥(SubMulAction.ofStabilizer G a)
g : G
hg : g ∈ stabilizer G a
hgbc : ↑({ val := g, property := hg } • b) = ↑c
h : G
hinvab : h⁻¹ • a = ↑b
⊢ g ∈ Subgroup.normalClosure ↑(stabilizer G a)
Theorem: normalClosure_of_stabilizer_eq_top
Proof state before:
case a.right.intro.intro.intro.mk.intro.a.a
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : 2 < PartENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this✝ : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
b c : ↥(SubMulAction.ofStabilizer G a)
hbc : b ≠ c
this : IsPretransitive ↥(stabilizer G a) ↥(SubMulAction.ofStabilizer G a)
g : G
hg : g ∈ stabilizer G a
hgbc : ↑({ val := g, property := hg } • b) = ↑c
h : G
hinvab : h⁻¹ • a = ↑b
⊢ g ∈ Subgroup.normalClosure ↑(stabilizer G a)
Tactic:
apply Subgroup.le_normalClosure
Proof state after:
case a.right.intro.intro.intro.mk.intro.a.a.a
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : 2 < PartENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this✝ : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
b c : ↥(SubMulAction.ofStabilizer G a)
hbc : b ≠ c
this : IsPretransitive ↥(stabilizer G a) ↥(SubMulAction.ofStabilizer G a)
g : G
hg : g ∈ stabilizer G a
hgbc : ↑({ val := g, property := hg } • b) = ↑c
h : G
hinvab : h⁻¹ • a = ↑b
⊢ g ∈ stabilizer G a
Theorem: normalClosure_of_stabilizer_eq_top
Proof state before:
case a.right.intro.intro.intro.mk.intro.a.a.a
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : 2 < PartENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this✝ : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
b c : ↥(SubMulAction.ofStabilizer G a)
hbc : b ≠ c
this : IsPretransitive ↥(stabilizer G a) ↥(SubMulAction.ofStabilizer G a)
g : G
hg : g ∈ stabilizer G a
hgbc : ↑({ val := g, property := hg } • b) = ↑c
h : G
hinvab : h⁻¹ • a = ↑b
⊢ g ∈ stabilizer G a
Tactic:
exact hg
Proof state after:
no goals