Theorem: MulAction.alternatingGroup.isPretransitive (Jordan/MultipleTransitivity.lean)

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

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
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 α
⊢ ℕ

State before:
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 α
⊢ ℕ
Tactic:
apply IsMultiplyPretransitive.alternatingGroup_of_sub_two
State after:
case hmn
M : Type ?u.287770
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h : 3 ≤ Fintype.card α
⊢ 1 ≤ Fintype.card α - 2

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

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

case hα
M : Type ?u.287770
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h : 3 ≤ Fintype.card α
⊢ ↑(Fintype.card α - 2) ≤ PartENat.card α
Tactic:
apply le_trans _ (Nat.sub_le_sub_right h 2)
State after:
M : Type ?u.287770
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h : 3 ≤ Fintype.card α
⊢ 1 ≤ 3 - 2

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

State before:
M : Type ?u.287770
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h : 3 ≤ Fintype.card α
⊢ 1 ≤ 3 - 2

case hα
M : Type ?u.287770
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h : 3 ≤ Fintype.card α
⊢ ↑(Fintype.card α - 2) ≤ PartENat.card α
Tactic:
norm_num
State after:
case hα
M : Type ?u.287770
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h : 3 ≤ Fintype.card α
⊢ ↑(Fintype.card α - 2) ≤ PartENat.card α

State before:
case hα
M : Type ?u.287770
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h : 3 ≤ Fintype.card α
⊢ ↑(Fintype.card α - 2) ≤ PartENat.card α
Tactic:
simp only [ge_iff_le, PartENat.card_eq_coe_fintype_card, PartENat.coe_le_coe,
  tsub_le_iff_right, le_add_iff_nonneg_right]
State after:
case hα
M : Type ?u.287770
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h : 3 ≤ Fintype.card α
⊢ 0 ≤ 2

State before:
case hα
M : Type ?u.287770
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h : 3 ≤ Fintype.card α
⊢ 0 ≤ 2
Tactic:
norm_num
State after:
no goals