Theorem: MulAction.remaining_transitivity' (Jordan/MultipleTransitivity.lean)

State before:
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
h : IsMultiplyPretransitive M α n
hmn : m + Set.ncard s ≤ n
hn : ↑n ≤ PartENat.card α
⊢ IsMultiplyPretransitive (↥(fixingSubgroup M s)) (↥(SubMulAction.ofFixingSubgroup M s)) m
Tactic:
apply remaining_transitivity
State after:
case h
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
h : IsMultiplyPretransitive M α n
hmn : m + Set.ncard s ≤ n
hn : ↑n ≤ PartENat.card α
⊢ IsMultiplyPretransitive M α ?n

case hmn
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
h : IsMultiplyPretransitive M α n
hmn : m + Set.ncard s ≤ n
hn : ↑n ≤ PartENat.card α
⊢ ?n = m + Set.ncard s

case n
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
h : IsMultiplyPretransitive M α n
hmn : m + Set.ncard s ≤ n
hn : ↑n ≤ PartENat.card α
⊢ ℕ

State before:
case h
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
h : IsMultiplyPretransitive M α n
hmn : m + Set.ncard s ≤ n
hn : ↑n ≤ PartENat.card α
⊢ IsMultiplyPretransitive M α ?n

case hmn
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
h : IsMultiplyPretransitive M α n
hmn : m + Set.ncard s ≤ n
hn : ↑n ≤ PartENat.card α
⊢ ?n = m + Set.ncard s

case n
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
h : IsMultiplyPretransitive M α n
hmn : m + Set.ncard s ≤ n
hn : ↑n ≤ PartENat.card α
⊢ ℕ
Tactic:
exact isMultiplyPretransitive_of_higher M α h hmn hn
State after:
case hmn
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
h : IsMultiplyPretransitive M α n
hmn : m + Set.ncard s ≤ n
hn : ↑n ≤ PartENat.card α
⊢ m + Set.ncard s = m + Set.ncard s

State before:
case hmn
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
h : IsMultiplyPretransitive M α n
hmn : m + Set.ncard s ≤ n
hn : ↑n ≤ PartENat.card α
⊢ m + Set.ncard s = m + Set.ncard s
Tactic:
rfl
State after:
no goals