internlm/Lean-Github huggingface dataset:
Theorem: MulAction.IsMultiplyPretransitive.alternatingGroup_of_sub_two
Proof state before:
case h.h.a
M : Type ?u.254050
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h2 : Fintype.card α ≥ 2
n : ℕ
hn : n + 2 = Fintype.card α
hn' : Fintype.card α - 2 = n
hn_le : n ≤ Fintype.card α
x y : Fin n ↪ α
x' : Fin (Fintype.card α) ↪ α
hx' : Function.Embedding.trans (Fin.castLEEmb hn_le).toEmbedding x' = x
y' : Fin (Fintype.card α) ↪ α
hy' : Function.Embedding.trans (Fin.castLEEmb hn_le).toEmbedding y' = y
heq : ∀ (x y : Fin (Fintype.card α) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
g : Equiv.Perm α
hg : g • x' = y'
h✝ : Equiv.Perm.sign g = -1
hg'1 : n + 1 < Fintype.card α
hg'2 : n < Fintype.card α
g' : Equiv.Perm α := Equiv.swap (y'.toFun { val := n + 1, isLt := hg'1 }) (y'.toFun { val := n, isLt := hg'2 })
hg' : Equiv.Perm.sign g' = -1
i : Fin n
this : ∀ (i : Fin (Fintype.card α)), g (x' i) = y' i
h : y' (Fin.castLE hn_le i) = y'.toFun { val := n, isLt := hg'2 }
⊢ False
Tactic:
simp only [toFun_eq_coe, EmbeddingLike.apply_eq_iff_eq,
   ← Fin.val_inj, Fin.coe_castLE] at h
Proof state after:
case h.h.a
M : Type ?u.254050
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h2 : Fintype.card α ≥ 2
n : ℕ
hn : n + 2 = Fintype.card α
hn' : Fintype.card α - 2 = n
hn_le : n ≤ Fintype.card α
x y : Fin n ↪ α
x' : Fin (Fintype.card α) ↪ α
hx' : Function.Embedding.trans (Fin.castLEEmb hn_le).toEmbedding x' = x
y' : Fin (Fintype.card α) ↪ α
hy' : Function.Embedding.trans (Fin.castLEEmb hn_le).toEmbedding y' = y
heq : ∀ (x y : Fin (Fintype.card α) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
g : Equiv.Perm α
hg : g • x' = y'
h✝ : Equiv.Perm.sign g = -1
hg'1 : n + 1 < Fintype.card α
hg'2 : n < Fintype.card α
g' : Equiv.Perm α := Equiv.swap (y'.toFun { val := n + 1, isLt := hg'1 }) (y'.toFun { val := n, isLt := hg'2 })
hg' : Equiv.Perm.sign g' = -1
i : Fin n
this : ∀ (i : Fin (Fintype.card α)), g (x' i) = y' i
h : ↑i = n
⊢ False
Theorem: MulAction.IsMultiplyPretransitive.alternatingGroup_of_sub_two
Proof state before:
case h.h.a
M : Type ?u.254050
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h2 : Fintype.card α ≥ 2
n : ℕ
hn : n + 2 = Fintype.card α
hn' : Fintype.card α - 2 = n
hn_le : n ≤ Fintype.card α
x y : Fin n ↪ α
x' : Fin (Fintype.card α) ↪ α
hx' : Function.Embedding.trans (Fin.castLEEmb hn_le).toEmbedding x' = x
y' : Fin (Fintype.card α) ↪ α
hy' : Function.Embedding.trans (Fin.castLEEmb hn_le).toEmbedding y' = y
heq : ∀ (x y : Fin (Fintype.card α) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
g : Equiv.Perm α
hg : g • x' = y'
h✝ : Equiv.Perm.sign g = -1
hg'1 : n + 1 < Fintype.card α
hg'2 : n < Fintype.card α
g' : Equiv.Perm α := Equiv.swap (y'.toFun { val := n + 1, isLt := hg'1 }) (y'.toFun { val := n, isLt := hg'2 })
hg' : Equiv.Perm.sign g' = -1
i : Fin n
this : ∀ (i : Fin (Fintype.card α)), g (x' i) = y' i
h : ↑i = n
⊢ False
Tactic:
apply lt_irrefl n
Proof state after:
case h.h.a
M : Type ?u.254050
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h2 : Fintype.card α ≥ 2
n : ℕ
hn : n + 2 = Fintype.card α
hn' : Fintype.card α - 2 = n
hn_le : n ≤ Fintype.card α
x y : Fin n ↪ α
x' : Fin (Fintype.card α) ↪ α
hx' : Function.Embedding.trans (Fin.castLEEmb hn_le).toEmbedding x' = x
y' : Fin (Fintype.card α) ↪ α
hy' : Function.Embedding.trans (Fin.castLEEmb hn_le).toEmbedding y' = y
heq : ∀ (x y : Fin (Fintype.card α) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
g : Equiv.Perm α
hg : g • x' = y'
h✝ : Equiv.Perm.sign g = -1
hg'1 : n + 1 < Fintype.card α
hg'2 : n < Fintype.card α
g' : Equiv.Perm α := Equiv.swap (y'.toFun { val := n + 1, isLt := hg'1 }) (y'.toFun { val := n, isLt := hg'2 })
hg' : Equiv.Perm.sign g' = -1
i : Fin n
this : ∀ (i : Fin (Fintype.card α)), g (x' i) = y' i
h : ↑i = n
⊢ n < n
Theorem: MulAction.IsMultiplyPretransitive.alternatingGroup_of_sub_two
Proof state before:
case h.h.a
M : Type ?u.254050
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h2 : Fintype.card α ≥ 2
n : ℕ
hn : n + 2 = Fintype.card α
hn' : Fintype.card α - 2 = n
hn_le : n ≤ Fintype.card α
x y : Fin n ↪ α
x' : Fin (Fintype.card α) ↪ α
hx' : Function.Embedding.trans (Fin.castLEEmb hn_le).toEmbedding x' = x
y' : Fin (Fintype.card α) ↪ α
hy' : Function.Embedding.trans (Fin.castLEEmb hn_le).toEmbedding y' = y
heq : ∀ (x y : Fin (Fintype.card α) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
g : Equiv.Perm α
hg : g • x' = y'
h✝ : Equiv.Perm.sign g = -1
hg'1 : n + 1 < Fintype.card α
hg'2 : n < Fintype.card α
g' : Equiv.Perm α := Equiv.swap (y'.toFun { val := n + 1, isLt := hg'1 }) (y'.toFun { val := n, isLt := hg'2 })
hg' : Equiv.Perm.sign g' = -1
i : Fin n
this : ∀ (i : Fin (Fintype.card α)), g (x' i) = y' i
h : ↑i = n
⊢ n < n
Tactic:
convert i.prop
Proof state after:
case h.e'_3
M : Type ?u.254050
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h2 : Fintype.card α ≥ 2
n : ℕ
hn : n + 2 = Fintype.card α
hn' : Fintype.card α - 2 = n
hn_le : n ≤ Fintype.card α
x y : Fin n ↪ α
x' : Fin (Fintype.card α) ↪ α
hx' : Function.Embedding.trans (Fin.castLEEmb hn_le).toEmbedding x' = x
y' : Fin (Fintype.card α) ↪ α
hy' : Function.Embedding.trans (Fin.castLEEmb hn_le).toEmbedding y' = y
heq : ∀ (x y : Fin (Fintype.card α) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
g : Equiv.Perm α
hg : g • x' = y'
h✝ : Equiv.Perm.sign g = -1
hg'1 : n + 1 < Fintype.card α
hg'2 : n < Fintype.card α
g' : Equiv.Perm α := Equiv.swap (y'.toFun { val := n + 1, isLt := hg'1 }) (y'.toFun { val := n, isLt := hg'2 })
hg' : Equiv.Perm.sign g' = -1
i : Fin n
this : ∀ (i : Fin (Fintype.card α)), g (x' i) = y' i
h : ↑i = n
⊢ n = ↑i
Theorem: MulAction.IsMultiplyPretransitive.alternatingGroup_of_sub_two
Proof state before:
case h.e'_3
M : Type ?u.254050
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h2 : Fintype.card α ≥ 2
n : ℕ
hn : n + 2 = Fintype.card α
hn' : Fintype.card α - 2 = n
hn_le : n ≤ Fintype.card α
x y : Fin n ↪ α
x' : Fin (Fintype.card α) ↪ α
hx' : Function.Embedding.trans (Fin.castLEEmb hn_le).toEmbedding x' = x
y' : Fin (Fintype.card α) ↪ α
hy' : Function.Embedding.trans (Fin.castLEEmb hn_le).toEmbedding y' = y
heq : ∀ (x y : Fin (Fintype.card α) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
g : Equiv.Perm α
hg : g • x' = y'
h✝ : Equiv.Perm.sign g = -1
hg'1 : n + 1 < Fintype.card α
hg'2 : n < Fintype.card α
g' : Equiv.Perm α := Equiv.swap (y'.toFun { val := n + 1, isLt := hg'1 }) (y'.toFun { val := n, isLt := hg'2 })
hg' : Equiv.Perm.sign g' = -1
i : Fin n
this : ∀ (i : Fin (Fintype.card α)), g (x' i) = y' i
h : ↑i = n
⊢ n = ↑i
Tactic:
exact h.symm
Proof state after:
no goals
Theorem: MulAction.IsMultiplyPretransitive.alternatingGroup_le_of_sub_two
Proof state before:
M : Type ?u.274186
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 2)
⊢ alternatingGroup α ≤ G
Tactic:
cases' Nat.lt_or_ge (Fintype.card α) 2 with hα1 hα
Proof state after:
case inl
M : Type ?u.274186
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 2)
hα1 : Fintype.card α < 2
⊢ alternatingGroup α ≤ G

case inr
M : Type ?u.274186
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 2)
hα : Fintype.card α ≥ 2
⊢ alternatingGroup α ≤ G
Theorem: MulAction.IsMultiplyPretransitive.alternatingGroup_le_of_sub_two
Proof state before:
case inr
M : Type ?u.274186
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 2)
hα : Fintype.card α ≥ 2
⊢ alternatingGroup α ≤ G
Tactic:
apply large_subgroup_of_perm_contains_alternating
Proof state after:
case inr.hG
M : Type ?u.274186
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 2)
hα : Fintype.card α ≥ 2
⊢ Fintype.card (Equiv.Perm α) ≤ 2 * Fintype.card ↥G
Theorem: MulAction.IsMultiplyPretransitive.alternatingGroup_le_of_sub_two
Proof state before:
case inr.hG
M : Type ?u.274186
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 2)
hα : Fintype.card α ≥ 2
⊢ Fintype.card (Equiv.Perm α) ≤ 2 * Fintype.card ↥G
Tactic:
rw [Fintype.card_equiv (Equiv.refl _)]
Proof state after:
case inr.hG
M : Type ?u.274186
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 2)
hα : Fintype.card α ≥ 2
⊢ (Fintype.card α)! ≤ 2 * Fintype.card ↥G
Theorem: MulAction.IsMultiplyPretransitive.alternatingGroup_le_of_sub_two
Proof state before:
case inr.hG
M : Type ?u.274186
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 2)
hα : Fintype.card α ≥ 2
⊢ (Fintype.card α)! ≤ 2 * Fintype.card ↥G
Tactic:
obtain ⟨s, _, hs⟩ := Set.exists_smaller_set (Set.univ : Set α) (Fintype.card α - 2)
  (by
    rw [Set.ncard_univ, Nat.card_eq_fintype_card]
    exact sub_le (Fintype.card α) 2)
Proof state after:
case inr.hG.intro.intro
M : Type ?u.274186
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 2)
hα : Fintype.card α ≥ 2
s : Set α
left✝ : s ⊆ Set.univ
hs : Set.ncard s = Fintype.card α - 2
⊢ (Fintype.card α)! ≤ 2 * Fintype.card ↥G
Theorem: MulAction.IsMultiplyPretransitive.alternatingGroup_le_of_sub_two
Proof state before:
case inr.hG.intro.intro
M : Type ?u.274186
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 2)
hα : Fintype.card α ≥ 2
s : Set α
left✝ : s ⊆ Set.univ
hs : Set.ncard s = Fintype.card α - 2
⊢ (Fintype.card α)! ≤ 2 * Fintype.card ↥G
Tactic:
rw [← hs] at hmt
Proof state after:
case inr.hG.intro.intro
M : Type ?u.274186
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hα : Fintype.card α ≥ 2
s : Set α
hmt : IsMultiplyPretransitive (↥G) α (Set.ncard s)
left✝ : s ⊆ Set.univ
hs : Set.ncard s = Fintype.card α - 2
⊢ (Fintype.card α)! ≤ 2 * Fintype.card ↥G
Theorem: MulAction.IsMultiplyPretransitive.alternatingGroup_le_of_sub_two
Proof state before:
case inr.hG.intro.intro
M : Type ?u.274186
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hα : Fintype.card α ≥ 2
s : Set α
hmt : IsMultiplyPretransitive (↥G) α (Set.ncard s)
left✝ : s ⊆ Set.univ
hs : Set.ncard s = Fintype.card α - 2
⊢ (Fintype.card α)! ≤ 2 * Fintype.card ↥G
Tactic:
rw [← hmt.index_of_fixingSubgroup G α s, hs, Nat.sub_sub_self hα,
  Nat.factorial_two, mul_comm]
Proof state after:
case inr.hG.intro.intro
M : Type ?u.274186
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hα : Fintype.card α ≥ 2
s : Set α
hmt : IsMultiplyPretransitive (↥G) α (Set.ncard s)
left✝ : s ⊆ Set.univ
hs : Set.ncard s = Fintype.card α - 2
⊢ 2 * Subgroup.index (fixingSubgroup (↥G) s) ≤ 2 * Fintype.card ↥G
Theorem: MulAction.IsMultiplyPretransitive.alternatingGroup_le_of_sub_two
Proof state before:
case inr.hG.intro.intro
M : Type ?u.274186
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hα : Fintype.card α ≥ 2
s : Set α
hmt : IsMultiplyPretransitive (↥G) α (Set.ncard s)
left✝ : s ⊆ Set.univ
hs : Set.ncard s = Fintype.card α - 2
⊢ 2 * Subgroup.index (fixingSubgroup (↥G) s) ≤ 2 * Fintype.card ↥G
Tactic:
apply Nat.mul_le_mul_left
Proof state after:
case inr.hG.intro.intro.h
M : Type ?u.274186
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hα : Fintype.card α ≥ 2
s : Set α
hmt : IsMultiplyPretransitive (↥G) α (Set.ncard s)
left✝ : s ⊆ Set.univ
hs : Set.ncard s = Fintype.card α - 2
⊢ Subgroup.index (fixingSubgroup (↥G) s) ≤ Fintype.card ↥G
Theorem: MulAction.IsMultiplyPretransitive.alternatingGroup_le_of_sub_two
Proof state before:
case inr.hG.intro.intro.h
M : Type ?u.274186
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hα : Fintype.card α ≥ 2
s : Set α
hmt : IsMultiplyPretransitive (↥G) α (Set.ncard s)
left✝ : s ⊆ Set.univ
hs : Set.ncard s = Fintype.card α - 2
⊢ Subgroup.index (fixingSubgroup (↥G) s) ≤ Fintype.card ↥G
Tactic:
apply Nat.le_of_dvd (Fintype.card_pos)
Proof state after:
case inr.hG.intro.intro.h
M : Type ?u.274186
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hα : Fintype.card α ≥ 2
s : Set α
hmt : IsMultiplyPretransitive (↥G) α (Set.ncard s)
left✝ : s ⊆ Set.univ
hs : Set.ncard s = Fintype.card α - 2
⊢ Subgroup.index (fixingSubgroup (↥G) s) ∣ Fintype.card ↥G
Theorem: MulAction.IsMultiplyPretransitive.alternatingGroup_le_of_sub_two
Proof state before:
case inr.hG.intro.intro.h
M : Type ?u.274186
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hα : Fintype.card α ≥ 2
s : Set α
hmt : IsMultiplyPretransitive (↥G) α (Set.ncard s)
left✝ : s ⊆ Set.univ
hs : Set.ncard s = Fintype.card α - 2
⊢ Subgroup.index (fixingSubgroup (↥G) s) ∣ Fintype.card ↥G
Tactic:
apply Subgroup.index_dvd_card
Proof state after:
no goals
Theorem: MulAction.IsMultiplyPretransitive.alternatingGroup_le_of_sub_two
Proof state before:
case inl
M : Type ?u.274186
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 2)
hα1 : Fintype.card α < 2
⊢ alternatingGroup α ≤ G
Tactic:
rw [Nat.lt_succ_iff] at hα1
Proof state after:
case inl
M : Type ?u.274186
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 2)
hα1 : Fintype.card α ≤ 1
⊢ alternatingGroup α ≤ G
Theorem: MulAction.IsMultiplyPretransitive.alternatingGroup_le_of_sub_two
Proof state before:
case inl
M : Type ?u.274186
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 2)
hα1 : Fintype.card α ≤ 1
⊢ alternatingGroup α ≤ G
Tactic:
suffices alternatingGroup α = ⊥ by
  rw [this]; exact bot_le
Proof state after:
case inl
M : Type ?u.274186
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 2)
hα1 : Fintype.card α ≤ 1
⊢ alternatingGroup α = ⊥
Theorem: MulAction.IsMultiplyPretransitive.alternatingGroup_le_of_sub_two
Proof state before:
case inl
M : Type ?u.274186
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 2)
hα1 : Fintype.card α ≤ 1
⊢ alternatingGroup α = ⊥
Tactic:
rw [← Subgroup.card_le_one_iff_eq_bot]
Proof state after:
case inl
M : Type ?u.274186
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 2)
hα1 : Fintype.card α ≤ 1
⊢ Fintype.card ↥(alternatingGroup α) ≤ 1
Theorem: MulAction.IsMultiplyPretransitive.alternatingGroup_le_of_sub_two
Proof state before:
case inl
M : Type ?u.274186
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 2)
hα1 : Fintype.card α ≤ 1
⊢ Fintype.card ↥(alternatingGroup α) ≤ 1
Tactic:
suffices Fintype.card (alternatingGroup α) ≤ Fintype.card (Equiv.Perm α) by
  apply le_trans this
  rw [Fintype.card_perm]
  exact Nat.factorial_le hα1
Proof state after:
case inl
M : Type ?u.274186
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 2)
hα1 : Fintype.card α ≤ 1
⊢ Fintype.card ↥(alternatingGroup α) ≤ Fintype.card (Equiv.Perm α)
Theorem: MulAction.IsMultiplyPretransitive.alternatingGroup_le_of_sub_two
Proof state before:
case inl
M : Type ?u.274186
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 2)
hα1 : Fintype.card α ≤ 1
⊢ Fintype.card ↥(alternatingGroup α) ≤ Fintype.card (Equiv.Perm α)
Tactic:
convert Fintype.card_subtype_le (fun x ↦ x ∈ alternatingGroup α)
Proof state after:
no goals
Theorem: MulAction.IsMultiplyPretransitive.alternatingGroup_le_of_sub_two
Proof state before:
M : Type ?u.274186
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 2)
hα1 : Fintype.card α ≤ 1
this : alternatingGroup α = ⊥
⊢ alternatingGroup α ≤ G
Tactic:
rw [this]
Proof state after:
M : Type ?u.274186
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 2)
hα1 : Fintype.card α ≤ 1
this : alternatingGroup α = ⊥
⊢ ⊥ ≤ G
Theorem: MulAction.IsMultiplyPretransitive.alternatingGroup_le_of_sub_two
Proof state before:
M : Type ?u.274186
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 2)
hα1 : Fintype.card α ≤ 1
this : alternatingGroup α = ⊥
⊢ ⊥ ≤ G
Tactic:
exact bot_le
Proof state after:
no goals
Theorem: MulAction.IsMultiplyPretransitive.alternatingGroup_le_of_sub_two
Proof state before:
M : Type ?u.274186
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 2)
hα1 : Fintype.card α ≤ 1
this : Fintype.card ↥(alternatingGroup α) ≤ Fintype.card (Equiv.Perm α)
⊢ Fintype.card ↥(alternatingGroup α) ≤ 1
Tactic:
apply le_trans this
Proof state after:
M : Type ?u.274186
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 2)
hα1 : Fintype.card α ≤ 1
this : Fintype.card ↥(alternatingGroup α) ≤ Fintype.card (Equiv.Perm α)
⊢ Fintype.card (Equiv.Perm α) ≤ 1
Theorem: MulAction.IsMultiplyPretransitive.alternatingGroup_le_of_sub_two
Proof state before:
M : Type ?u.274186
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 2)
hα1 : Fintype.card α ≤ 1
this : Fintype.card ↥(alternatingGroup α) ≤ Fintype.card (Equiv.Perm α)
⊢ Fintype.card (Equiv.Perm α) ≤ 1
Tactic:
rw [Fintype.card_perm]
Proof state after:
M : Type ?u.274186
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 2)
hα1 : Fintype.card α ≤ 1
this : Fintype.card ↥(alternatingGroup α) ≤ Fintype.card (Equiv.Perm α)
⊢ (Fintype.card α)! ≤ 1
Theorem: MulAction.IsMultiplyPretransitive.alternatingGroup_le_of_sub_two
Proof state before:
M : Type ?u.274186
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 2)
hα1 : Fintype.card α ≤ 1
this : Fintype.card ↥(alternatingGroup α) ≤ Fintype.card (Equiv.Perm α)
⊢ (Fintype.card α)! ≤ 1
Tactic:
exact Nat.factorial_le hα1
Proof state after:
no goals
Theorem: MulAction.IsMultiplyPretransitive.alternatingGroup_le_of_sub_two
Proof state before:
M : Type ?u.274186
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 2)
hα : Fintype.card α ≥ 2
⊢ Fintype.card α - 2 ≤ Set.ncard Set.univ
Tactic:
rw [Set.ncard_univ, Nat.card_eq_fintype_card]
Proof state after:
M : Type ?u.274186
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 2)
hα : Fintype.card α ≥ 2
⊢ Fintype.card α - 2 ≤ Fintype.card α
Theorem: MulAction.IsMultiplyPretransitive.alternatingGroup_le_of_sub_two
Proof state before:
M : Type ?u.274186
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 2)
hα : Fintype.card α ≥ 2
⊢ Fintype.card α - 2 ≤ Fintype.card α
Tactic:
exact sub_le (Fintype.card α) 2
Proof state after:
no goals
Theorem: MulAction.alternatingGroup.isPretransitive
Proof state before:
M : Type ?u.287770
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h : 3 ≤ Fintype.card α
⊢ IsPretransitive (↥(alternatingGroup α)) α
Tactic:
rw [isPretransitive_iff_is_one_pretransitive]
Proof state after:
M : Type ?u.287770
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h : 3 ≤ Fintype.card α
⊢ IsMultiplyPretransitive (↥(alternatingGroup α)) α 1
Theorem: MulAction.alternatingGroup.isPretransitive
Proof state before:
M : Type ?u.287770
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h : 3 ≤ Fintype.card α
⊢ IsMultiplyPretransitive (↥(alternatingGroup α)) α 1
Tactic:
apply isMultiplyPretransitive_of_higher
Proof state after:
case hn
M : Type ?u.287770
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h : 3 ≤ Fintype.card α
⊢ IsMultiplyPretransitive (↥(alternatingGroup α)) α ?n

case hmn
M : Type ?u.287770
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h : 3 ≤ Fintype.card α
⊢ 1 ≤ ?n

case hα
M : Type ?u.287770
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h : 3 ≤ Fintype.card α
⊢ ↑?n ≤ PartENat.card α

case n
M : Type ?u.287770
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h : 3 ≤ Fintype.card α
⊢ ℕ