Theorem: Equiv.Perm.isPretransitive (Jordan/MultipleTransitivity.lean)

State before:
M : Type ?u.237454
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : DecidableEq α
⊢ IsPretransitive (Equiv.Perm α) α
Tactic:
apply IsPretransitive.mk
State after:
case exists_smul_eq
M : Type ?u.237454
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : DecidableEq α
⊢ ∀ (x y : α), ∃ g, g • x = y

State before:
case exists_smul_eq
M : Type ?u.237454
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : DecidableEq α
⊢ ∀ (x y : α), ∃ g, g • x = y
Tactic:
intro x y
State after:
case exists_smul_eq
M : Type ?u.237454
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : DecidableEq α
x y : α
⊢ ∃ g, g • x = y

State before:
case exists_smul_eq
M : Type ?u.237454
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : DecidableEq α
x y : α
⊢ ∃ g, g • x = y
Tactic:
use Equiv.swap x y
State after:
case h
M : Type ?u.237454
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : DecidableEq α
x y : α
⊢ Equiv.swap x y • x = y

State before:
case h
M : Type ?u.237454
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : DecidableEq α
x y : α
⊢ Equiv.swap x y • x = y
Tactic:
simp only [Equiv.Perm.smul_def]
State after:
case h
M : Type ?u.237454
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : DecidableEq α
x y : α
⊢ (Equiv.swap x y) x = y

State before:
case h
M : Type ?u.237454
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : DecidableEq α
x y : α
⊢ (Equiv.swap x y) x = y
Tactic:
rw [Equiv.swap_apply_left x y]
State after:
no goals