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

State before:
M : Type u_1
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : Monoid M
inst✝ : MulAction M α
G K : Submonoid M
hKG : K ≤ G
h : IsPretransitive (↥K) α
⊢ IsPretransitive (↥G) α
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 α
G K : Submonoid M
hKG : K ≤ G
h : IsPretransitive (↥K) α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
⊢ IsPretransitive (↥G) α

State before:
M : Type u_1
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : Monoid M
inst✝ : MulAction M α
G K : Submonoid M
hKG : K ≤ G
h : IsPretransitive (↥K) α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
⊢ IsPretransitive (↥G) α
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 α
G K : Submonoid M
hKG : K ≤ G
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 α
G K : Submonoid M
hKG : K ≤ G
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 α
G K : Submonoid M
hKG : K ≤ G
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 α
G K : Submonoid M
hKG : K ≤ G
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 α
G K : Submonoid M
hKG : K ≤ G
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 α
G K : Submonoid M
hKG : K ≤ G
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:
use ⟨k, hKG hk⟩
State after:
case h
M : Type u_1
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : Monoid M
inst✝ : MulAction M α
G K : Submonoid M
hKG : K ≤ G
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
⊢ { val := k, property := ⋯ } • x = y

State before:
case h
M : Type u_1
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : Monoid M
inst✝ : MulAction M α
G K : Submonoid M
hKG : K ≤ G
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
⊢ { val := k, property := ⋯ } • x = y
Tactic:
exact hk'
State after:
no goals