Theorem: normalClosure_of_stabilizer_eq_top (Jordan/Jordan.lean)

State before:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : 2 < PartENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
⊢ Subgroup.normalClosure ↑(stabilizer G a) = ⊤
Tactic:
have hG : IsPretransitive G α := by
  rw [isPretransitive_iff_is_one_pretransitive]
  apply isMultiplyPretransitive_of_higher
  exact hG'
  norm_num
  rw [Nat.cast_two]
  exact le_of_lt hsn'
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 α
⊢ Subgroup.normalClosure ↑(stabilizer G a) = ⊤

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 α
⊢ Subgroup.normalClosure ↑(stabilizer G a) = ⊤
Tactic:
have : Nontrivial α := by
  rw [← PartENat.one_lt_card_iff_nontrivial]
  refine' lt_trans _ hsn'
  rw [← Nat.cast_two, ← Nat.cast_one, PartENat.coe_lt_coe]
  norm_num
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 α
⊢ Subgroup.normalClosure ↑(stabilizer G a) = ⊤

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.normalClosure ↑(stabilizer G a) = ⊤
Tactic:
have hGa : (stabilizer G a).IsMaximal :=  by
  rw [maximal_stabilizer_iff_preprimitive G a]
  exact hG'.isPreprimitive_of_two
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 α
hGa : Subgroup.IsMaximal (stabilizer G a)
⊢ Subgroup.normalClosure ↑(stabilizer G a) = ⊤

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 α
hGa : Subgroup.IsMaximal (stabilizer G a)
⊢ Subgroup.normalClosure ↑(stabilizer G a) = ⊤
Tactic:
rw [Subgroup.isMaximal_def] at hGa
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 α
hGa : IsCoatom (stabilizer G a)
⊢ Subgroup.normalClosure ↑(stabilizer G a) = ⊤

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 α
hGa : IsCoatom (stabilizer G a)
⊢ Subgroup.normalClosure ↑(stabilizer G a) = ⊤
Tactic:
apply hGa.right
State after:
case 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)
⊢ stabilizer G a < Subgroup.normalClosure ↑(stabilizer G a)

State before:
case 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)
⊢ stabilizer G a < Subgroup.normalClosure ↑(stabilizer G a)
Tactic:
constructor
State after:
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))

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)

State before:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : 2 < PartENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
⊢ IsPretransitive G α
Tactic:
rw [isPretransitive_iff_is_one_pretransitive]
State after:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : 2 < PartENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
⊢ IsMultiplyPretransitive G α 1

State before:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : 2 < PartENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
⊢ IsMultiplyPretransitive G α 1
Tactic:
apply isMultiplyPretransitive_of_higher
State after:
case hn
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : 2 < PartENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
⊢ IsMultiplyPretransitive G α ?n

case hmn
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : 2 < PartENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
⊢ 1 ≤ ?n

case hα
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : 2 < PartENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
⊢ ↑?n ≤ PartENat.card α

case n
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : 2 < PartENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
⊢ ℕ

State before:
case hn
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : 2 < PartENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
⊢ IsMultiplyPretransitive G α ?n

case hmn
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : 2 < PartENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
⊢ 1 ≤ ?n

case hα
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : 2 < PartENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
⊢ ↑?n ≤ PartENat.card α

case n
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : 2 < PartENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
⊢ ℕ
Tactic:
exact hG'
State after:
case hmn
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : 2 < PartENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
⊢ 1 ≤ 2

case hα
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : 2 < PartENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
⊢ ↑2 ≤ PartENat.card α

State before:
case hmn
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : 2 < PartENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
⊢ 1 ≤ 2

case hα
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : 2 < PartENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
⊢ ↑2 ≤ PartENat.card α
Tactic:
norm_num
State after:
case hα
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : 2 < PartENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
⊢ ↑2 ≤ PartENat.card α

State before:
case hα
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : 2 < PartENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
⊢ ↑2 ≤ PartENat.card α
Tactic:
rw [Nat.cast_two]
State after:
case hα
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : 2 < PartENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
⊢ 2 ≤ PartENat.card α

State before:
case hα
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : 2 < PartENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
⊢ 2 ≤ PartENat.card α
Tactic:
exact le_of_lt hsn'
State after:
no goals

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 α
⊢ Nontrivial α
Tactic:
rw [← PartENat.one_lt_card_iff_nontrivial]
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 α
⊢ 1 < PartENat.card α

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 < PartENat.card α
Tactic:
refine' lt_trans _ hsn'
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 α
⊢ 1 < 2

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
State after:
no goals

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]
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 α

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
State after:
no goals

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
State after:
no goals

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
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

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
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

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
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

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
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

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'
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

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
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

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
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

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]
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

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
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

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
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

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
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

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]
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

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]
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

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
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

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]
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

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]
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

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
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))

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
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)

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
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

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
State after:
no goals

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 α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
⊢ Nontrivial ↥(SubMulAction.ofStabilizer G a)
Tactic:
apply Set.Nontrivial.coe_sort
State after:
case 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)
⊢ Set.Nontrivial ↑(SubMulAction.ofStabilizer G a)

State before:
case 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)
⊢ Set.Nontrivial ↑(SubMulAction.ofStabilizer G a)
Tactic:
rw [← Set.one_lt_encard_iff_nontrivial]
State after:
case 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)
⊢ 1 < Set.encard ↑(SubMulAction.ofStabilizer G a)

State before:
case 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)
⊢ 1 < Set.encard ↑(SubMulAction.ofStabilizer G a)
Tactic:
rw [← not_le, ← Nat.cast_one, ← WithTop.add_one_le_coe_succ_iff, not_le]
State after:
case 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)
⊢ ↑(Nat.succ 1) < Set.encard ↑(SubMulAction.ofStabilizer G a) + 1

State before:
case 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)
⊢ ↑(Nat.succ 1) < Set.encard ↑(SubMulAction.ofStabilizer G a) + 1
Tactic:
rw [← PartENat.withTopEquiv_lt, ← Set.encard_univ] at hsn'
State after:
case a
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : PartENat.withTopEquiv 2 < Set.encard Set.univ
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
⊢ ↑(Nat.succ 1) < Set.encard ↑(SubMulAction.ofStabilizer G a) + 1

State before:
case a
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : PartENat.withTopEquiv 2 < Set.encard Set.univ
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
⊢ ↑(Nat.succ 1) < Set.encard ↑(SubMulAction.ofStabilizer G a) + 1
Tactic:
convert hsn'
State after:
case h.e'_3
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : PartENat.withTopEquiv 2 < Set.encard Set.univ
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
⊢ ↑(Nat.succ 1) = PartENat.withTopEquiv 2

case h.e'_4
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : PartENat.withTopEquiv 2 < Set.encard Set.univ
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
⊢ Set.encard ↑(SubMulAction.ofStabilizer G a) + 1 = Set.encard Set.univ

State before:
case h.e'_3
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : PartENat.withTopEquiv 2 < Set.encard Set.univ
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
⊢ ↑(Nat.succ 1) = PartENat.withTopEquiv 2

case h.e'_4
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : PartENat.withTopEquiv 2 < Set.encard Set.univ
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
⊢ Set.encard ↑(SubMulAction.ofStabilizer G a) + 1 = Set.encard Set.univ
Tactic:
simp only [SetLike.coe_sort_coe, Nat.cast_succ, Nat.cast_one]
State after:
case h.e'_3
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : PartENat.withTopEquiv 2 < Set.encard Set.univ
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
⊢ ↑0 + 1 + 1 = PartENat.withTopEquiv 2

case h.e'_4
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : PartENat.withTopEquiv 2 < Set.encard Set.univ
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
⊢ Set.encard ↑(SubMulAction.ofStabilizer G a) + 1 = Set.encard Set.univ

State before:
case h.e'_3
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : PartENat.withTopEquiv 2 < Set.encard Set.univ
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
⊢ ↑0 + 1 + 1 = PartENat.withTopEquiv 2

case h.e'_4
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : PartENat.withTopEquiv 2 < Set.encard Set.univ
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
⊢ Set.encard ↑(SubMulAction.ofStabilizer G a) + 1 = Set.encard Set.univ
Tactic:
rw [← Nat.cast_two]
State after:
case h.e'_3
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : PartENat.withTopEquiv 2 < Set.encard Set.univ
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
⊢ ↑0 + 1 + 1 = PartENat.withTopEquiv ↑2

case h.e'_4
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : PartENat.withTopEquiv 2 < Set.encard Set.univ
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
⊢ Set.encard ↑(SubMulAction.ofStabilizer G a) + 1 = Set.encard Set.univ

State before:
case h.e'_3
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : PartENat.withTopEquiv 2 < Set.encard Set.univ
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
⊢ ↑0 + 1 + 1 = PartENat.withTopEquiv ↑2

case h.e'_4
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : PartENat.withTopEquiv 2 < Set.encard Set.univ
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
⊢ Set.encard ↑(SubMulAction.ofStabilizer G a) + 1 = Set.encard Set.univ
Tactic:
rw [← PartENat.withTopEquiv.symm_apply_eq]
State after:
case h.e'_3
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : PartENat.withTopEquiv 2 < Set.encard Set.univ
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
⊢ PartENat.withTopEquiv.symm (↑0 + 1 + 1) = ↑2

case h.e'_4
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : PartENat.withTopEquiv 2 < Set.encard Set.univ
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
⊢ Set.encard ↑(SubMulAction.ofStabilizer G a) + 1 = Set.encard Set.univ

State before:
case h.e'_3
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : PartENat.withTopEquiv 2 < Set.encard Set.univ
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
⊢ PartENat.withTopEquiv.symm (↑0 + 1 + 1) = ↑2

case h.e'_4
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : PartENat.withTopEquiv 2 < Set.encard Set.univ
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
⊢ Set.encard ↑(SubMulAction.ofStabilizer G a) + 1 = Set.encard Set.univ
Tactic:
rfl
State after:
case h.e'_4
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : PartENat.withTopEquiv 2 < Set.encard Set.univ
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
⊢ Set.encard ↑(SubMulAction.ofStabilizer G a) + 1 = Set.encard Set.univ

State before:
case h.e'_4
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : PartENat.withTopEquiv 2 < Set.encard Set.univ
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
⊢ Set.encard ↑(SubMulAction.ofStabilizer G a) + 1 = Set.encard Set.univ
Tactic:
rw [add_comm]
State after:
case h.e'_4
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : PartENat.withTopEquiv 2 < Set.encard Set.univ
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
⊢ 1 + Set.encard ↑(SubMulAction.ofStabilizer G a) = Set.encard Set.univ

State before:
case h.e'_4
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : PartENat.withTopEquiv 2 < Set.encard Set.univ
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
⊢ 1 + Set.encard ↑(SubMulAction.ofStabilizer G a) = Set.encard Set.univ
Tactic:
exact SubMulAction.add_encard_ofStabilizer_eq' a
State after:
no goals

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 α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
b c : ↥(SubMulAction.ofStabilizer G a)
hbc : b ≠ c
⊢ IsPretransitive ↥(stabilizer G a) ↥(SubMulAction.ofStabilizer G a)
Tactic:
rw [isPretransitive_iff_is_one_pretransitive]
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 α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
b c : ↥(SubMulAction.ofStabilizer G a)
hbc : b ≠ c
⊢ IsMultiplyPretransitive (↥(stabilizer G a)) (↥(SubMulAction.ofStabilizer G a)) 1

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 α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
b c : ↥(SubMulAction.ofStabilizer G a)
hbc : b ≠ c
⊢ IsMultiplyPretransitive (↥(stabilizer G a)) (↥(SubMulAction.ofStabilizer G a)) 1
Tactic:
exact (stabilizer.isMultiplyPretransitive G α hG).mp hG'
State after:
no goals