Theorem: MulAction.isPretransitive_of_subgroup (Jordan/MultipleTransitivity.lean)

State before:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
K : Subgroup M
h : IsPretransitive (↥K) α
⊢ IsPretransitive M α
Tactic:
apply isPretransitive_of_submonoid
State after:
case h
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
K : Subgroup M
h : IsPretransitive (↥K) α
⊢ IsPretransitive (↥?K) α

case K
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
K : Subgroup M
h : IsPretransitive (↥K) α
⊢ Submonoid M

State before:
case h
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
K : Subgroup M
h : IsPretransitive (↥K) α
⊢ IsPretransitive (↥?K) α

case K
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
K : Subgroup M
h : IsPretransitive (↥K) α
⊢ Submonoid M
Tactic:
swap
State after:
case K
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
K : Subgroup M
h : IsPretransitive (↥K) α
⊢ Submonoid M

case h
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
K : Subgroup M
h : IsPretransitive (↥K) α
⊢ IsPretransitive (↥?K) α

State before:
case K
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
K : Subgroup M
h : IsPretransitive (↥K) α
⊢ Submonoid M

case h
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
K : Subgroup M
h : IsPretransitive (↥K) α
⊢ IsPretransitive (↥?K) α
Tactic:
exact K.toSubmonoid
State after:
case h
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
K : Subgroup M
h : IsPretransitive (↥K) α
⊢ IsPretransitive (↥K.toSubmonoid) α

State before:
case h
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
K : Subgroup M
h : IsPretransitive (↥K) α
⊢ IsPretransitive (↥K.toSubmonoid) α
Tactic:
exact h
State after:
no goals