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

State before:
M : Type u_1
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : Monoid M
inst✝ : MulAction M α
K : Submonoid M
h : IsPretransitive (↥K) α
⊢ IsPretransitive M α
Tactic:
let h_eq := h.exists_smul_eq
State after:
M : Type u_1
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : Monoid M
inst✝ : MulAction M α
K : Submonoid M
h : IsPretransitive (↥K) α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
⊢ IsPretransitive M α

State before:
M : Type u_1
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : Monoid M
inst✝ : MulAction M α
K : Submonoid M
h : IsPretransitive (↥K) α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
⊢ IsPretransitive M α
Tactic:
apply IsPretransitive.mk
State after:
case exists_smul_eq
M : Type u_1
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : Monoid M
inst✝ : MulAction M α
K : Submonoid M
h : IsPretransitive (↥K) α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
⊢ ∀ (x y : α), ∃ g, g • x = y

State before:
case exists_smul_eq
M : Type u_1
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : Monoid M
inst✝ : MulAction M α
K : Submonoid M
h : IsPretransitive (↥K) α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
⊢ ∀ (x y : α), ∃ g, g • x = y
Tactic:
intro x y
State after:
case exists_smul_eq
M : Type u_1
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : Monoid M
inst✝ : MulAction M α
K : Submonoid M
h : IsPretransitive (↥K) α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : α
⊢ ∃ g, g • x = y

State before:
case exists_smul_eq
M : Type u_1
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : Monoid M
inst✝ : MulAction M α
K : Submonoid M
h : IsPretransitive (↥K) α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : α
⊢ ∃ g, g • x = y
Tactic:
obtain ⟨⟨k, hk⟩, hk'⟩ := h_eq x y
State after:
case exists_smul_eq.intro.mk
M : Type u_1
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : Monoid M
inst✝ : MulAction M α
K : Submonoid M
h : IsPretransitive (↥K) α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : α
k : M
hk : k ∈ K
hk' : { val := k, property := hk } • x = y
⊢ ∃ g, g • x = y

State before:
case exists_smul_eq.intro.mk
M : Type u_1
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : Monoid M
inst✝ : MulAction M α
K : Submonoid M
h : IsPretransitive (↥K) α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : α
k : M
hk : k ∈ K
hk' : { val := k, property := hk } • x = y
⊢ ∃ g, g • x = y
Tactic:
exact ⟨k, hk'⟩
State after:
no goals