Theorem: alternatingGroup.isPretransitive_ofFixingSubgroup (Jordan/AlternatingMaximal.lean)

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nontrivial s
hα : Set.ncard s < Set.ncard sᶜ
⊢ IsPretransitive ↥(fixingSubgroup (↥(alternatingGroup α)) s) ↥(SubMulAction.ofFixingSubgroup (↥(alternatingGroup α)) s)
Tactic:
rw [isPretransitive_iff_is_one_pretransitive]
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nontrivial s
hα : Set.ncard s < Set.ncard sᶜ
⊢ IsMultiplyPretransitive (↥(fixingSubgroup (↥(alternatingGroup α)) s))
    (↥(SubMulAction.ofFixingSubgroup (↥(alternatingGroup α)) s)) 1

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nontrivial s
hα : Set.ncard s < Set.ncard sᶜ
⊢ IsMultiplyPretransitive (↥(fixingSubgroup (↥(alternatingGroup α)) s))
    (↥(SubMulAction.ofFixingSubgroup (↥(alternatingGroup α)) s)) 1
Tactic:
apply remaining_transitivity'
State after:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nontrivial s
hα : Set.ncard s < Set.ncard sᶜ
⊢ IsMultiplyPretransitive (↥(alternatingGroup α)) α ?n

case hmn
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nontrivial s
hα : Set.ncard s < Set.ncard sᶜ
⊢ 1 + Set.ncard s ≤ ?n

case hn
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nontrivial s
hα : Set.ncard s < Set.ncard sᶜ
⊢ ↑?n ≤ PartENat.card α

case n
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nontrivial s
hα : Set.ncard s < Set.ncard sᶜ
⊢ ℕ

State before:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nontrivial s
hα : Set.ncard s < Set.ncard sᶜ
⊢ IsMultiplyPretransitive (↥(alternatingGroup α)) α ?n

case hmn
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nontrivial s
hα : Set.ncard s < Set.ncard sᶜ
⊢ 1 + Set.ncard s ≤ ?n

case hn
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nontrivial s
hα : Set.ncard s < Set.ncard sᶜ
⊢ ↑?n ≤ PartENat.card α

case n
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nontrivial s
hα : Set.ncard s < Set.ncard sᶜ
⊢ ℕ
Tactic:
apply IsMultiplyPretransitive.alternatingGroup_of_sub_two
State after:
case hmn
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nontrivial s
hα : Set.ncard s < Set.ncard sᶜ
⊢ 1 + Set.ncard s ≤ Fintype.card α - 2

case hn
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nontrivial s
hα : Set.ncard s < Set.ncard sᶜ
⊢ ↑(Fintype.card α - 2) ≤ PartENat.card α

State before:
case hmn
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nontrivial s
hα : Set.ncard s < Set.ncard sᶜ
⊢ 1 + Set.ncard s ≤ Fintype.card α - 2
Tactic:
have h1' : 2 < Set.ncard (sᶜ : Set α) := by
  apply lt_of_le_of_lt _ hα
  rw [Nat.succ_le_iff, Set.one_lt_ncard_iff_nontrivial]
  exact h0
State after:
case hmn
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nontrivial s
hα : Set.ncard s < Set.ncard sᶜ
h1' : 2 < Set.ncard sᶜ
⊢ 1 + Set.ncard s ≤ Fintype.card α - 2

State before:
case hmn
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nontrivial s
hα : Set.ncard s < Set.ncard sᶜ
h1' : 2 < Set.ncard sᶜ
⊢ 1 + Set.ncard s ≤ Fintype.card α - 2
Tactic:
rw [add_comm, ← Nat.card_eq_fintype_card, ← Set.ncard_add_ncard_compl s,
  Nat.add_sub_assoc (le_of_lt h1'), add_le_add_iff_left]
State after:
case hmn
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nontrivial s
hα : Set.ncard s < Set.ncard sᶜ
h1' : 2 < Set.ncard sᶜ
⊢ 1 ≤ Set.ncard sᶜ - 2

State before:
case hmn
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nontrivial s
hα : Set.ncard s < Set.ncard sᶜ
h1' : 2 < Set.ncard sᶜ
⊢ 1 ≤ Set.ncard sᶜ - 2
Tactic:
apply Nat.le_sub_of_add_le
State after:
case hmn.h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nontrivial s
hα : Set.ncard s < Set.ncard sᶜ
h1' : 2 < Set.ncard sᶜ
⊢ 1 + 2 ≤ Set.ncard sᶜ

State before:
case hmn.h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nontrivial s
hα : Set.ncard s < Set.ncard sᶜ
h1' : 2 < Set.ncard sᶜ
⊢ 1 + 2 ≤ Set.ncard sᶜ
Tactic:
exact h1'
State after:
no goals

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nontrivial s
hα : Set.ncard s < Set.ncard sᶜ
⊢ 2 < Set.ncard sᶜ
Tactic:
apply lt_of_le_of_lt _ hα
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nontrivial s
hα : Set.ncard s < Set.ncard sᶜ
⊢ 2 ≤ Set.ncard s

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nontrivial s
hα : Set.ncard s < Set.ncard sᶜ
⊢ 2 ≤ Set.ncard s
Tactic:
rw [Nat.succ_le_iff, Set.one_lt_ncard_iff_nontrivial]
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nontrivial s
hα : Set.ncard s < Set.ncard sᶜ
⊢ Set.Nontrivial s

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nontrivial s
hα : Set.ncard s < Set.ncard sᶜ
⊢ Set.Nontrivial s
Tactic:
exact h0
State after:
no goals

State before:
case hn
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nontrivial s
hα : Set.ncard s < Set.ncard sᶜ
⊢ ↑(Fintype.card α - 2) ≤ PartENat.card α
Tactic:
rw [PartENat.card_eq_coe_fintype_card]
State after:
case hn
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nontrivial s
hα : Set.ncard s < Set.ncard sᶜ
⊢ ↑(Fintype.card α - 2) ≤ ↑(Fintype.card α)

State before:
case hn
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nontrivial s
hα : Set.ncard s < Set.ncard sᶜ
⊢ ↑(Fintype.card α - 2) ≤ ↑(Fintype.card α)
Tactic:
simp only [Nat.cast_le, tsub_le_iff_right, le_add_iff_nonneg_right, zero_le]
State after:
no goals