internlm/Lean-Github huggingface dataset:
Theorem: MulAction.stabilizer.isMultiplyPreprimitive
Proof state before:
case pos
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
x : α
hxs : x ∈ s
hxa : x = a
⊢ x ∈ insert a (Subtype.val '' t)

case neg
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
x : α
hxs : x ∈ s
hxa : ¬x = a
⊢ x ∈ insert a (Subtype.val '' t)
Tactic:
rw [hxa]
Proof state after:
case pos
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
x : α
hxs : x ∈ s
hxa : x = a
⊢ a ∈ insert a (Subtype.val '' t)

case neg
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
x : α
hxs : x ∈ s
hxa : ¬x = a
⊢ x ∈ insert a (Subtype.val '' t)
Theorem: MulAction.stabilizer.isMultiplyPreprimitive
Proof state before:
case pos
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
x : α
hxs : x ∈ s
hxa : x = a
⊢ a ∈ insert a (Subtype.val '' t)

case neg
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
x : α
hxs : x ∈ s
hxa : ¬x = a
⊢ x ∈ insert a (Subtype.val '' t)
Tactic:
apply Set.mem_insert
Proof state after:
case neg
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
x : α
hxs : x ∈ s
hxa : ¬x = a
⊢ x ∈ insert a (Subtype.val '' t)
Theorem: MulAction.stabilizer.isMultiplyPreprimitive
Proof state before:
case neg
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
x : α
hxs : x ∈ s
hxa : ¬x = a
⊢ x ∈ insert a (Subtype.val '' t)
Tactic:
apply Set.mem_insert_of_mem
Proof state after:
case neg.a
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
x : α
hxs : x ∈ s
hxa : ¬x = a
⊢ x ∈ Subtype.val '' t
Theorem: MulAction.stabilizer.isMultiplyPreprimitive
Proof state before:
case neg.a
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
x : α
hxs : x ∈ s
hxa : ¬x = a
⊢ x ∈ Subtype.val '' t
Tactic:
use ⟨x, ?_⟩
Proof state after:
case h
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
x : α
hxs : x ∈ s
hxa : ¬x = a
⊢ { val := x, property := ?w } ∈ t ∧ ↑{ val := x, property := ?w } = x

case w
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
x : α
hxs : x ∈ s
hxa : ¬x = a
⊢ x ∈ SubMulAction.ofStabilizer M a
Theorem: MulAction.stabilizer.isMultiplyPreprimitive
Proof state before:
case h
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
x : α
hxs : x ∈ s
hxa : ¬x = a
⊢ { val := x, property := ?w } ∈ t ∧ ↑{ val := x, property := ?w } = x

case w
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
x : α
hxs : x ∈ s
hxa : ¬x = a
⊢ x ∈ SubMulAction.ofStabilizer M a
Tactic:
refine' And.intro _ rfl
Proof state after:
case h
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
x : α
hxs : x ∈ s
hxa : ¬x = a
⊢ { val := x, property := ?w } ∈ t

case w
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
x : α
hxs : x ∈ s
hxa : ¬x = a
⊢ x ∈ SubMulAction.ofStabilizer M a
Theorem: MulAction.stabilizer.isMultiplyPreprimitive
Proof state before:
case w
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
x : α
hxs : x ∈ s
hxa : ¬x = a
⊢ x ∈ SubMulAction.ofStabilizer M a
Tactic:
exact hxa
Proof state after:
no goals
Theorem: MulAction.stabilizer.isMultiplyPreprimitive
Proof state before:
case h
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
x : α
hxs : x ∈ s
hxa : ¬x = a
⊢ { val := x, property := ?w } ∈ t
Tactic:
simp only [t, Set.mem_preimage]
Proof state after:
case h
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
x : α
hxs : x ∈ s
hxa : ¬x = a
⊢ x ∈ s
Theorem: MulAction.stabilizer.isMultiplyPreprimitive
Proof state before:
case h
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
x : α
hxs : x ∈ s
hxa : ¬x = a
⊢ x ∈ s
Tactic:
exact hxs
Proof state after:
no goals
Theorem: MulAction.stabilizer.isMultiplyPreprimitive
Proof state before:
case h.mpr
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
x : α
⊢ x ∈ insert a (Subtype.val '' t) → x ∈ s
Tactic:
intro hxat
Proof state after:
case h.mpr
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
x : α
hxat : x ∈ insert a (Subtype.val '' t)
⊢ x ∈ s
Theorem: MulAction.stabilizer.isMultiplyPreprimitive
Proof state before:
case h.mpr
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
x : α
hxat : x ∈ insert a (Subtype.val '' t)
⊢ x ∈ s
Tactic:
cases' Set.mem_insert_iff.mp hxat with hxa hxt
Proof state after:
case h.mpr.inl
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
x : α
hxat : x ∈ insert a (Subtype.val '' t)
hxa : x = a
⊢ x ∈ s

case h.mpr.inr
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
x : α
hxat : x ∈ insert a (Subtype.val '' t)
hxt : x ∈ Subtype.val '' t
⊢ x ∈ s
Theorem: MulAction.stabilizer.isMultiplyPreprimitive
Proof state before:
case h.mpr.inl
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
x : α
hxat : x ∈ insert a (Subtype.val '' t)
hxa : x = a
⊢ x ∈ s

case h.mpr.inr
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
x : α
hxat : x ∈ insert a (Subtype.val '' t)
hxt : x ∈ Subtype.val '' t
⊢ x ∈ s
Tactic:
rw [hxa]
Proof state after:
case h.mpr.inl
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
x : α
hxat : x ∈ insert a (Subtype.val '' t)
hxa : x = a
⊢ a ∈ s

case h.mpr.inr
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
x : α
hxat : x ∈ insert a (Subtype.val '' t)
hxt : x ∈ Subtype.val '' t
⊢ x ∈ s
Theorem: MulAction.stabilizer.isMultiplyPreprimitive
Proof state before:
case h.mpr.inl
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
x : α
hxat : x ∈ insert a (Subtype.val '' t)
hxa : x = a
⊢ a ∈ s

case h.mpr.inr
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
x : α
hxat : x ∈ insert a (Subtype.val '' t)
hxt : x ∈ Subtype.val '' t
⊢ x ∈ s
Tactic:
exact has
Proof state after:
case h.mpr.inr
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
x : α
hxat : x ∈ insert a (Subtype.val '' t)
hxt : x ∈ Subtype.val '' t
⊢ x ∈ s
Theorem: MulAction.stabilizer.isMultiplyPreprimitive
Proof state before:
case h.mpr.inr
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
x : α
hxat : x ∈ insert a (Subtype.val '' t)
hxt : x ∈ Subtype.val '' t
⊢ x ∈ s
Tactic:
obtain ⟨y, hy, rfl⟩ := hxt
Proof state after:
case h.mpr.inr.intro.intro
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
y : ↥(SubMulAction.ofStabilizer M a)
hy : y ∈ t
hxat : ↑y ∈ insert a (Subtype.val '' t)
⊢ ↑y ∈ s
Theorem: MulAction.stabilizer.isMultiplyPreprimitive
Proof state before:
case h.mpr.inr.intro.intro
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
y : ↥(SubMulAction.ofStabilizer M a)
hy : y ∈ t
hxat : ↑y ∈ insert a (Subtype.val '' t)
⊢ ↑y ∈ s
Tactic:
simpa only using hy
Proof state after:
no goals
Theorem: MulAction.stabilizer.isMultiplyPreprimitive
Proof state before:
case mpr.right
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
hst : s = insert a (Subtype.val '' t)
⊢ IsPreprimitive ↥(fixingSubgroup (↥(stabilizer M a)) t) ↥(SubMulAction.ofFixingSubgroup (↥(stabilizer M a)) t)
Tactic:
apply hn_0.right t
Proof state after:
case mpr.right
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
hst : s = insert a (Subtype.val '' t)
⊢ Set.encard t + 1 = ↑n
Theorem: MulAction.stabilizer.isMultiplyPreprimitive
Proof state before:
case mpr.right
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
hst : s = insert a (Subtype.val '' t)
⊢ Set.encard t + 1 = ↑n
Tactic:
rw [← hs, hst, Set.encard_insert_of_not_mem, Subtype.coe_injective.encard_image]
Proof state after:
case mpr.right
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
hst : s = insert a (Subtype.val '' t)
⊢ a ∉ Subtype.val '' t
Theorem: MulAction.stabilizer.isMultiplyPreprimitive
Proof state before:
case mpr.right
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
hst : s = insert a (Subtype.val '' t)
⊢ a ∉ Subtype.val '' t
Tactic:
rintro ⟨x, hx⟩
Proof state after:
case mpr.right.intro
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
hst : s = insert a (Subtype.val '' t)
x : ↥(SubMulAction.ofStabilizer M a)
hx : x ∈ t ∧ ↑x = a
⊢ False
Theorem: MulAction.stabilizer.isMultiplyPreprimitive
Proof state before:
case mpr.right.intro
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
hst : s = insert a (Subtype.val '' t)
x : ↥(SubMulAction.ofStabilizer M a)
hx : x ∈ t ∧ ↑x = a
⊢ False
Tactic:
apply x.prop
Proof state after:
case mpr.right.intro
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
hst : s = insert a (Subtype.val '' t)
x : ↥(SubMulAction.ofStabilizer M a)
hx : x ∈ t ∧ ↑x = a
⊢ ↑x ∈ {a}
Theorem: MulAction.stabilizer.isMultiplyPreprimitive
Proof state before:
case mpr.right.intro
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
hst : s = insert a (Subtype.val '' t)
x : ↥(SubMulAction.ofStabilizer M a)
hx : x ∈ t ∧ ↑x = a
⊢ ↑x ∈ {a}
Tactic:
rw [hx.right]
Proof state after:
case mpr.right.intro
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
hst : s = insert a (Subtype.val '' t)
x : ↥(SubMulAction.ofStabilizer M a)
hx : x ∈ t ∧ ↑x = a
⊢ a ∈ {a}
Theorem: MulAction.stabilizer.isMultiplyPreprimitive
Proof state before:
case mpr.right.intro
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
hst : s = insert a (Subtype.val '' t)
x : ↥(SubMulAction.ofStabilizer M a)
hx : x ∈ t ∧ ↑x = a
⊢ a ∈ {a}
Tactic:
simp only [Set.mem_singleton]
Proof state after:
no goals