internlm/Lean-Github huggingface dataset:
Theorem: isPretransitive_ofFixingSubgroup_inter
Proof state before:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ SubMulAction.ofFixingSubgroup G (s ∩ g • s)
hx : x ∉ g • s
hg'x : g⁻¹ • x ∈ SubMulAction.ofFixingSubgroup G s
hg'a : g⁻¹ • a ∈ SubMulAction.ofFixingSubgroup G s
k : G
hk✝ : k ∈ fixingSubgroup G s
hk : ∀ y ∈ s, k • y = y
hkax : { val := k, property := hk✝ } • { val := g⁻¹ • a, property := hg'a } = { val := g⁻¹ • x, property := hg'x }
y : α
hy : y ∈ s ∩ g • s
⊢ k • g⁻¹ • y = g⁻¹ • y
Tactic:
apply hk
Proof state after:
case a
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ SubMulAction.ofFixingSubgroup G (s ∩ g • s)
hx : x ∉ g • s
hg'x : g⁻¹ • x ∈ SubMulAction.ofFixingSubgroup G s
hg'a : g⁻¹ • a ∈ SubMulAction.ofFixingSubgroup G s
k : G
hk✝ : k ∈ fixingSubgroup G s
hk : ∀ y ∈ s, k • y = y
hkax : { val := k, property := hk✝ } • { val := g⁻¹ • a, property := hg'a } = { val := g⁻¹ • x, property := hg'x }
y : α
hy : y ∈ s ∩ g • s
⊢ g⁻¹ • y ∈ s
Theorem: isPretransitive_ofFixingSubgroup_inter
Proof state before:
case a
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ SubMulAction.ofFixingSubgroup G (s ∩ g • s)
hx : x ∉ g • s
hg'x : g⁻¹ • x ∈ SubMulAction.ofFixingSubgroup G s
hg'a : g⁻¹ • a ∈ SubMulAction.ofFixingSubgroup G s
k : G
hk✝ : k ∈ fixingSubgroup G s
hk : ∀ y ∈ s, k • y = y
hkax : { val := k, property := hk✝ } • { val := g⁻¹ • a, property := hg'a } = { val := g⁻¹ • x, property := hg'x }
y : α
hy : y ∈ s ∩ g • s
⊢ g⁻¹ • y ∈ s
Tactic:
rw [← Set.mem_smul_set_iff_inv_smul_mem]
Proof state after:
case a
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ SubMulAction.ofFixingSubgroup G (s ∩ g • s)
hx : x ∉ g • s
hg'x : g⁻¹ • x ∈ SubMulAction.ofFixingSubgroup G s
hg'a : g⁻¹ • a ∈ SubMulAction.ofFixingSubgroup G s
k : G
hk✝ : k ∈ fixingSubgroup G s
hk : ∀ y ∈ s, k • y = y
hkax : { val := k, property := hk✝ } • { val := g⁻¹ • a, property := hg'a } = { val := g⁻¹ • x, property := hg'x }
y : α
hy : y ∈ s ∩ g • s
⊢ y ∈ g • s
Theorem: isPretransitive_ofFixingSubgroup_inter
Proof state before:
case a
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ SubMulAction.ofFixingSubgroup G (s ∩ g • s)
hx : x ∉ g • s
hg'x : g⁻¹ • x ∈ SubMulAction.ofFixingSubgroup G s
hg'a : g⁻¹ • a ∈ SubMulAction.ofFixingSubgroup G s
k : G
hk✝ : k ∈ fixingSubgroup G s
hk : ∀ y ∈ s, k • y = y
hkax : { val := k, property := hk✝ } • { val := g⁻¹ • a, property := hg'a } = { val := g⁻¹ • x, property := hg'x }
y : α
hy : y ∈ s ∩ g • s
⊢ y ∈ g • s
Tactic:
exact Set.mem_of_mem_inter_right hy
Proof state after:
no goals
Theorem: isPretransitive_ofFixingSubgroup_inter
Proof state before:
case h
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ SubMulAction.ofFixingSubgroup G (s ∩ g • s)
hx : x ∉ g • s
hg'x : g⁻¹ • x ∈ SubMulAction.ofFixingSubgroup G s
hg'a : g⁻¹ • a ∈ SubMulAction.ofFixingSubgroup G s
k : G
hk : k ∈ fixingSubgroup G s
hkax : { val := k, property := hk } • { val := g⁻¹ • a, property := hg'a } = { val := g⁻¹ • x, property := hg'x }
⊢ { val := g * k * g⁻¹, property := ⋯ } • { val := a, property := ha' } = { val := x, property := hx✝ }
Tactic:
simp only [← SetLike.coe_eq_coe] at hkax ⊢
Proof state after:
case h
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ SubMulAction.ofFixingSubgroup G (s ∩ g • s)
hx : x ∉ g • s
hg'x : g⁻¹ • x ∈ SubMulAction.ofFixingSubgroup G s
hg'a : g⁻¹ • a ∈ SubMulAction.ofFixingSubgroup G s
k : G
hk : k ∈ fixingSubgroup G s
hkax : ↑({ val := k, property := hk } • { val := g⁻¹ • a, property := hg'a }) = g⁻¹ • x
⊢ ↑({ val := g * k * g⁻¹, property := ⋯ } • { val := a, property := ha' }) = x
Theorem: isPretransitive_ofFixingSubgroup_inter
Proof state before:
case h
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ SubMulAction.ofFixingSubgroup G (s ∩ g • s)
hx : x ∉ g • s
hg'x : g⁻¹ • x ∈ SubMulAction.ofFixingSubgroup G s
hg'a : g⁻¹ • a ∈ SubMulAction.ofFixingSubgroup G s
k : G
hk : k ∈ fixingSubgroup G s
hkax : ↑({ val := k, property := hk } • { val := g⁻¹ • a, property := hg'a }) = g⁻¹ • x
⊢ ↑({ val := g * k * g⁻¹, property := ⋯ } • { val := a, property := ha' }) = x
Tactic:
simp only [SetLike.val_smul] at hkax ⊢
Proof state after:
case h
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ SubMulAction.ofFixingSubgroup G (s ∩ g • s)
hx : x ∉ g • s
hg'x : g⁻¹ • x ∈ SubMulAction.ofFixingSubgroup G s
hg'a : g⁻¹ • a ∈ SubMulAction.ofFixingSubgroup G s
k : G
hk : k ∈ fixingSubgroup G s
hkax : { val := k, property := hk } • g⁻¹ • a = g⁻¹ • x
⊢ { val := g * k * g⁻¹, property := ⋯ } • a = x
Theorem: isPretransitive_ofFixingSubgroup_inter
Proof state before:
case h
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ SubMulAction.ofFixingSubgroup G (s ∩ g • s)
hx : x ∉ g • s
hg'x : g⁻¹ • x ∈ SubMulAction.ofFixingSubgroup G s
hg'a : g⁻¹ • a ∈ SubMulAction.ofFixingSubgroup G s
k : G
hk : k ∈ fixingSubgroup G s
hkax : { val := k, property := hk } • g⁻¹ • a = g⁻¹ • x
⊢ { val := g * k * g⁻¹, property := ⋯ } • a = x
Tactic:
rw [← smul_eq_iff_eq_inv_smul] at hkax
Proof state after:
case h
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ SubMulAction.ofFixingSubgroup G (s ∩ g • s)
hx : x ∉ g • s
hg'x : g⁻¹ • x ∈ SubMulAction.ofFixingSubgroup G s
hg'a : g⁻¹ • a ∈ SubMulAction.ofFixingSubgroup G s
k : G
hk : k ∈ fixingSubgroup G s
hkax : g • { val := k, property := hk } • g⁻¹ • a = x
⊢ { val := g * k * g⁻¹, property := ⋯ } • a = x
Theorem: isPretransitive_ofFixingSubgroup_inter
Proof state before:
case h
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ SubMulAction.ofFixingSubgroup G (s ∩ g • s)
hx : x ∉ g • s
hg'x : g⁻¹ • x ∈ SubMulAction.ofFixingSubgroup G s
hg'a : g⁻¹ • a ∈ SubMulAction.ofFixingSubgroup G s
k : G
hk : k ∈ fixingSubgroup G s
hkax : g • { val := k, property := hk } • g⁻¹ • a = x
⊢ { val := g * k * g⁻¹, property := ⋯ } • a = x
Tactic:
change (g * k * g⁻¹) • a = x
Proof state after:
case h
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ SubMulAction.ofFixingSubgroup G (s ∩ g • s)
hx : x ∉ g • s
hg'x : g⁻¹ • x ∈ SubMulAction.ofFixingSubgroup G s
hg'a : g⁻¹ • a ∈ SubMulAction.ofFixingSubgroup G s
k : G
hk : k ∈ fixingSubgroup G s
hkax : g • { val := k, property := hk } • g⁻¹ • a = x
⊢ (g * k * g⁻¹) • a = x
Theorem: isPretransitive_ofFixingSubgroup_inter
Proof state before:
case h
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ SubMulAction.ofFixingSubgroup G (s ∩ g • s)
hx : x ∉ g • s
hg'x : g⁻¹ • x ∈ SubMulAction.ofFixingSubgroup G s
hg'a : g⁻¹ • a ∈ SubMulAction.ofFixingSubgroup G s
k : G
hk : k ∈ fixingSubgroup G s
hkax : g • { val := k, property := hk } • g⁻¹ • a = x
⊢ (g * k * g⁻¹) • a = x
Tactic:
simp only [← smul_smul]
Proof state after:
case h
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ SubMulAction.ofFixingSubgroup G (s ∩ g • s)
hx : x ∉ g • s
hg'x : g⁻¹ • x ∈ SubMulAction.ofFixingSubgroup G s
hg'a : g⁻¹ • a ∈ SubMulAction.ofFixingSubgroup G s
k : G
hk : k ∈ fixingSubgroup G s
hkax : g • { val := k, property := hk } • g⁻¹ • a = x
⊢ g • k • g⁻¹ • a = x
Theorem: isPretransitive_ofFixingSubgroup_inter
Proof state before:
case h
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
a : α
ha : a ∈ (s ∪ g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ SubMulAction.ofFixingSubgroup G (s ∩ g • s)
hx : x ∉ g • s
hg'x : g⁻¹ • x ∈ SubMulAction.ofFixingSubgroup G s
hg'a : g⁻¹ • a ∈ SubMulAction.ofFixingSubgroup G s
k : G
hk : k ∈ fixingSubgroup G s
hkax : g • { val := k, property := hk } • g⁻¹ • a = x
⊢ g • k • g⁻¹ • a = x
Tactic:
exact hkax
Proof state after:
no goals
Theorem: SubMulAction.add_encard_ofStabilizer_eq
Proof state before:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
a : α
⊢ 1 + ↑(Set.encard (SubMulAction.ofStabilizer G a).carrier) = PartENat.card α
Tactic:
rw [SubMulAction.ofStabilizer_carrier]
Proof state after:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
a : α
⊢ 1 + ↑(Set.encard {a}ᶜ) = PartENat.card α
Theorem: SubMulAction.add_encard_ofStabilizer_eq
Proof state before:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
a : α
⊢ 1 + ↑(Set.encard {a}ᶜ) = PartENat.card α
Tactic:
rw [← Nat.cast_one]
Proof state after:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
a : α
⊢ ↑1 + ↑(Set.encard {a}ᶜ) = PartENat.card α
Theorem: SubMulAction.add_encard_ofStabilizer_eq
Proof state before:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
a : α
⊢ ↑1 + ↑(Set.encard {a}ᶜ) = PartENat.card α
Tactic:
apply PartENat.withTopAddEquiv.injective
Proof state after:
case a
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
a : α
⊢ PartENat.withTopAddEquiv (↑1 + ↑(Set.encard {a}ᶜ)) = PartENat.withTopAddEquiv (PartENat.card α)
Theorem: SubMulAction.add_encard_ofStabilizer_eq
Proof state before:
case a
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
a : α
⊢ PartENat.withTopAddEquiv (↑1 + ↑(Set.encard {a}ᶜ)) = PartENat.withTopAddEquiv (PartENat.card α)
Tactic:
rw [map_add]
Proof state after:
case a
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
a : α
⊢ PartENat.withTopAddEquiv ↑1 + PartENat.withTopAddEquiv ↑(Set.encard {a}ᶜ) = PartENat.withTopAddEquiv (PartENat.card α)
Theorem: SubMulAction.add_encard_ofStabilizer_eq
Proof state before:
case a
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
a : α
⊢ PartENat.withTopAddEquiv ↑1 + PartENat.withTopAddEquiv ↑(Set.encard {a}ᶜ) = PartENat.withTopAddEquiv (PartENat.card α)
Tactic:
convert Set.encard_add_encard_compl {a}
Proof state after:
case h.e'_2.h.e'_5
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
a : α
⊢ PartENat.withTopAddEquiv ↑1 = Set.encard {a}

case h.e'_2.h.e'_6
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
a : α
⊢ PartENat.withTopAddEquiv ↑(Set.encard {a}ᶜ) = Set.encard {a}ᶜ

case h.e'_3
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
a : α
⊢ PartENat.withTopAddEquiv (PartENat.card α) = Set.encard Set.univ
Theorem: SubMulAction.add_encard_ofStabilizer_eq
Proof state before:
case h.e'_2.h.e'_5
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
a : α
⊢ PartENat.withTopAddEquiv ↑1 = Set.encard {a}
Tactic:
rw [Set.encard_singleton]
Proof state after:
case h.e'_2.h.e'_5
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
a : α
⊢ PartENat.withTopAddEquiv ↑1 = 1
Theorem: SubMulAction.add_encard_ofStabilizer_eq
Proof state before:
case h.e'_2.h.e'_5
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
a : α
⊢ PartENat.withTopAddEquiv ↑1 = 1
Tactic:
apply PartENat.toWithTop_natCast'
Proof state after:
no goals
Theorem: SubMulAction.add_encard_ofStabilizer_eq
Proof state before:
case h.e'_2.h.e'_6
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
a : α
⊢ PartENat.withTopAddEquiv ↑(Set.encard {a}ᶜ) = Set.encard {a}ᶜ
Tactic:
rw [← AddEquiv.eq_symm_apply]
Proof state after:
case h.e'_2.h.e'_6
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
a : α
⊢ ↑(Set.encard {a}ᶜ) = (AddEquiv.symm PartENat.withTopAddEquiv) (Set.encard {a}ᶜ)
Theorem: SubMulAction.add_encard_ofStabilizer_eq
Proof state before:
case h.e'_2.h.e'_6
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
a : α
⊢ ↑(Set.encard {a}ᶜ) = (AddEquiv.symm PartENat.withTopAddEquiv) (Set.encard {a}ᶜ)
Tactic:
rfl
Proof state after:
no goals
Theorem: SubMulAction.add_encard_ofStabilizer_eq
Proof state before:
case h.e'_3
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
a : α
⊢ PartENat.withTopAddEquiv (PartENat.card α) = Set.encard Set.univ
Tactic:
convert (Set.encard_univ α).symm
Proof state after:
no goals
Theorem: SubMulAction.add_encard_ofStabilizer_eq'
Proof state before:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
a : α
⊢ 1 + Set.encard (SubMulAction.ofStabilizer G a).carrier = Set.encard Set.univ
Tactic:
rw [SubMulAction.ofStabilizer_carrier]
Proof state after:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
a : α
⊢ 1 + Set.encard {a}ᶜ = Set.encard Set.univ
Theorem: SubMulAction.add_encard_ofStabilizer_eq'
Proof state before:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
a : α
⊢ 1 + Set.encard {a}ᶜ = Set.encard Set.univ
Tactic:
convert Set.encard_add_encard_compl _
Proof state after:
case h.e'_2.h.e'_5
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
a : α
⊢ 1 = Set.encard {a}
Theorem: SubMulAction.add_encard_ofStabilizer_eq'
Proof state before:
case h.e'_2.h.e'_5
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
a : α
⊢ 1 = Set.encard {a}
Tactic:
simp only [Set.encard_singleton]
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 : α
⊢ 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'
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 α
⊢ Subgroup.normalClosure ↑(stabilizer G a) = ⊤
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 α
⊢ 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
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 α
⊢ Subgroup.normalClosure ↑(stabilizer G a) = ⊤
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.normalClosure ↑(stabilizer G a) = ⊤
Tactic:
have hGa : (stabilizer G a).IsMaximal :=  by
  rw [maximal_stabilizer_iff_preprimitive G a]
  exact hG'.isPreprimitive_of_two
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 α
hGa : Subgroup.IsMaximal (stabilizer G a)
⊢ Subgroup.normalClosure ↑(stabilizer G a) = ⊤
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 α
hGa : Subgroup.IsMaximal (stabilizer G a)
⊢ Subgroup.normalClosure ↑(stabilizer G a) = ⊤
Tactic:
rw [Subgroup.isMaximal_def] at hGa
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 α
hGa : IsCoatom (stabilizer G a)
⊢ Subgroup.normalClosure ↑(stabilizer G a) = ⊤
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 α
hGa : IsCoatom (stabilizer G a)
⊢ Subgroup.normalClosure ↑(stabilizer G a) = ⊤
Tactic:
apply hGa.right
Proof 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)
Theorem: normalClosure_of_stabilizer_eq_top
Proof 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
Proof 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)
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 : α
⊢ IsPretransitive G α
Tactic:
rw [isPretransitive_iff_is_one_pretransitive]
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 : α
⊢ IsMultiplyPretransitive G α 1
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 : α
⊢ IsMultiplyPretransitive G α 1
Tactic:
apply isMultiplyPretransitive_of_higher
Proof 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 : α
⊢ ℕ
Theorem: normalClosure_of_stabilizer_eq_top
Proof 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'
Proof 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 α
Theorem: normalClosure_of_stabilizer_eq_top
Proof 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
Proof 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 α
Theorem: normalClosure_of_stabilizer_eq_top
Proof 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]
Proof 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 α
Theorem: normalClosure_of_stabilizer_eq_top
Proof 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'
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 α
⊢ Nontrivial α
Tactic:
rw [← PartENat.one_lt_card_iff_nontrivial]
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 α
⊢ 1 < PartENat.card α
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 < PartENat.card α
Tactic:
refine' lt_trans _ hsn'
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 α
⊢ 1 < 2