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

State before:
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
⊢ IsMultiplyPretransitive (Equiv.Perm α) α n
Tactic:
cases' le_or_gt n (Fintype.card α) with hn hn
State after:
case inl
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n ≤ Fintype.card α
⊢ IsMultiplyPretransitive (Equiv.Perm α) α n

case inr
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n > Fintype.card α
⊢ IsMultiplyPretransitive (Equiv.Perm α) α n

State before:
case inr
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n > Fintype.card α
⊢ IsMultiplyPretransitive (Equiv.Perm α) α n
Tactic:
suffices IsEmpty (Fin n ↪ α) by
  apply IsPretransitive.mk
  intro x
  exfalso
  exact this.false  x
State after:
case inr
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n > Fintype.card α
⊢ IsEmpty (Fin n ↪ α)

State before:
case inr
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n > Fintype.card α
⊢ IsEmpty (Fin n ↪ α)
Tactic:
apply Function.Embedding.isEmpty_of_card_lt
State after:
case inr.h
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n > Fintype.card α
⊢ Fintype.card α < Fintype.card (Fin n)

State before:
case inr.h
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n > Fintype.card α
⊢ Fintype.card α < Fintype.card (Fin n)
Tactic:
simp only [Fintype.card_fin]
State after:
case inr.h
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n > Fintype.card α
⊢ Fintype.card α < n

State before:
case inr.h
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n > Fintype.card α
⊢ Fintype.card α < n
Tactic:
exact hn
State after:
no goals

State before:
case inl
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n ≤ Fintype.card α
⊢ IsMultiplyPretransitive (Equiv.Perm α) α n
Tactic:
apply isMultiplyPretransitive_of_higher (Equiv.Perm α) α _ hn
State after:
case inl
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n ≤ Fintype.card α
⊢ ↑(Fintype.card α) ≤ PartENat.card α

M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n ≤ Fintype.card α
⊢ IsMultiplyPretransitive (Equiv.Perm α) α (Fintype.card α)

State before:
case inl
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n ≤ Fintype.card α
⊢ ↑(Fintype.card α) ≤ PartENat.card α

M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n ≤ Fintype.card α
⊢ IsMultiplyPretransitive (Equiv.Perm α) α (Fintype.card α)
Tactic:
apply le_of_eq
State after:
case inl.a
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n ≤ Fintype.card α
⊢ ↑(Fintype.card α) = PartENat.card α

M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n ≤ Fintype.card α
⊢ IsMultiplyPretransitive (Equiv.Perm α) α (Fintype.card α)

State before:
case inl.a
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n ≤ Fintype.card α
⊢ ↑(Fintype.card α) = PartENat.card α

M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n ≤ Fintype.card α
⊢ IsMultiplyPretransitive (Equiv.Perm α) α (Fintype.card α)
Tactic:
rw [PartENat.card_eq_coe_fintype_card]
State after:
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n ≤ Fintype.card α
⊢ IsMultiplyPretransitive (Equiv.Perm α) α (Fintype.card α)

State before:
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n ≤ Fintype.card α
⊢ IsMultiplyPretransitive (Equiv.Perm α) α (Fintype.card α)
Tactic:
apply IsPretransitive.mk
State after:
case exists_smul_eq
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n ≤ Fintype.card α
⊢ ∀ (x y : Fin (Fintype.card α) ↪ α), ∃ g, g • x = y

State before:
case exists_smul_eq
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n ≤ Fintype.card α
⊢ ∀ (x y : Fin (Fintype.card α) ↪ α), ∃ g, g • x = y
Tactic:
intro x y
State after:
case exists_smul_eq
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n ≤ Fintype.card α
x y : Fin (Fintype.card α) ↪ α
⊢ ∃ g, g • x = y

State before:
case exists_smul_eq
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n ≤ Fintype.card α
x y : Fin (Fintype.card α) ↪ α
⊢ ∃ g, g • x = y
Tactic:
suffices h : Function.Bijective x ∧ Function.Bijective y by
  let x' := Equiv.ofBijective x h.1
  let y' := Equiv.ofBijective y h.2
  use x'.symm.trans y'
  ext i
  simp only [smul_apply, Equiv.Perm.smul_def, Equiv.trans_apply, x', y']
  simp only [Equiv.ofBijective_symm_apply_apply, Equiv.ofBijective_apply]
State after:
case exists_smul_eq
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n ≤ Fintype.card α
x y : Fin (Fintype.card α) ↪ α
⊢ Function.Bijective ⇑x ∧ Function.Bijective ⇑y

State before:
case exists_smul_eq
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n ≤ Fintype.card α
x y : Fin (Fintype.card α) ↪ α
⊢ Function.Bijective ⇑x ∧ Function.Bijective ⇑y
Tactic:
constructor
State after:
case exists_smul_eq.left
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n ≤ Fintype.card α
x y : Fin (Fintype.card α) ↪ α
⊢ Function.Bijective ⇑x

case exists_smul_eq.right
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n ≤ Fintype.card α
x y : Fin (Fintype.card α) ↪ α
⊢ Function.Bijective ⇑y

State before:
case exists_smul_eq.left
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n ≤ Fintype.card α
x y : Fin (Fintype.card α) ↪ α
⊢ Function.Bijective ⇑x

case exists_smul_eq.right
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n ≤ Fintype.card α
x y : Fin (Fintype.card α) ↪ α
⊢ Function.Bijective ⇑y
Tactic:
all_goals
  rw [Fintype.bijective_iff_injective_and_card]
  constructor
  apply EmbeddingLike.injective
  exact Fintype.card_fin (Fintype.card α)
State after:
no goals

State before:
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n ≤ Fintype.card α
x y : Fin (Fintype.card α) ↪ α
h : Function.Bijective ⇑x ∧ Function.Bijective ⇑y
⊢ ∃ g, g • x = y
Tactic:
let x' := Equiv.ofBijective x h.1
State after:
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n ≤ Fintype.card α
x y : Fin (Fintype.card α) ↪ α
h : Function.Bijective ⇑x ∧ Function.Bijective ⇑y
x' : Fin (Fintype.card α) ≃ α := Equiv.ofBijective ⇑x ⋯
⊢ ∃ g, g • x = y

State before:
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n ≤ Fintype.card α
x y : Fin (Fintype.card α) ↪ α
h : Function.Bijective ⇑x ∧ Function.Bijective ⇑y
x' : Fin (Fintype.card α) ≃ α := Equiv.ofBijective ⇑x ⋯
⊢ ∃ g, g • x = y
Tactic:
let y' := Equiv.ofBijective y h.2
State after:
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n ≤ Fintype.card α
x y : Fin (Fintype.card α) ↪ α
h : Function.Bijective ⇑x ∧ Function.Bijective ⇑y
x' : Fin (Fintype.card α) ≃ α := Equiv.ofBijective ⇑x ⋯
y' : Fin (Fintype.card α) ≃ α := Equiv.ofBijective ⇑y ⋯
⊢ ∃ g, g • x = y

State before:
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n ≤ Fintype.card α
x y : Fin (Fintype.card α) ↪ α
h : Function.Bijective ⇑x ∧ Function.Bijective ⇑y
x' : Fin (Fintype.card α) ≃ α := Equiv.ofBijective ⇑x ⋯
y' : Fin (Fintype.card α) ≃ α := Equiv.ofBijective ⇑y ⋯
⊢ ∃ g, g • x = y
Tactic:
use x'.symm.trans y'
State after:
case h
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n ≤ Fintype.card α
x y : Fin (Fintype.card α) ↪ α
h : Function.Bijective ⇑x ∧ Function.Bijective ⇑y
x' : Fin (Fintype.card α) ≃ α := Equiv.ofBijective ⇑x ⋯
y' : Fin (Fintype.card α) ≃ α := Equiv.ofBijective ⇑y ⋯
⊢ x'.symm.trans y' • x = y

State before:
case h
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n ≤ Fintype.card α
x y : Fin (Fintype.card α) ↪ α
h : Function.Bijective ⇑x ∧ Function.Bijective ⇑y
x' : Fin (Fintype.card α) ≃ α := Equiv.ofBijective ⇑x ⋯
y' : Fin (Fintype.card α) ≃ α := Equiv.ofBijective ⇑y ⋯
⊢ x'.symm.trans y' • x = y
Tactic:
ext i
State after:
case h.h
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n ≤ Fintype.card α
x y : Fin (Fintype.card α) ↪ α
h : Function.Bijective ⇑x ∧ Function.Bijective ⇑y
x' : Fin (Fintype.card α) ≃ α := Equiv.ofBijective ⇑x ⋯
y' : Fin (Fintype.card α) ≃ α := Equiv.ofBijective ⇑y ⋯
i : Fin (Fintype.card α)
⊢ (x'.symm.trans y' • x) i = y i

State before:
case h.h
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n ≤ Fintype.card α
x y : Fin (Fintype.card α) ↪ α
h : Function.Bijective ⇑x ∧ Function.Bijective ⇑y
x' : Fin (Fintype.card α) ≃ α := Equiv.ofBijective ⇑x ⋯
y' : Fin (Fintype.card α) ≃ α := Equiv.ofBijective ⇑y ⋯
i : Fin (Fintype.card α)
⊢ (x'.symm.trans y' • x) i = y i
Tactic:
simp only [smul_apply, Equiv.Perm.smul_def, Equiv.trans_apply, x', y']
State after:
case h.h
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n ≤ Fintype.card α
x y : Fin (Fintype.card α) ↪ α
h : Function.Bijective ⇑x ∧ Function.Bijective ⇑y
x' : Fin (Fintype.card α) ≃ α := Equiv.ofBijective ⇑x ⋯
y' : Fin (Fintype.card α) ≃ α := Equiv.ofBijective ⇑y ⋯
i : Fin (Fintype.card α)
⊢ (Equiv.ofBijective ⇑y ⋯) ((Equiv.ofBijective ⇑x ⋯).symm (x i)) = y i

State before:
case h.h
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n ≤ Fintype.card α
x y : Fin (Fintype.card α) ↪ α
h : Function.Bijective ⇑x ∧ Function.Bijective ⇑y
x' : Fin (Fintype.card α) ≃ α := Equiv.ofBijective ⇑x ⋯
y' : Fin (Fintype.card α) ≃ α := Equiv.ofBijective ⇑y ⋯
i : Fin (Fintype.card α)
⊢ (Equiv.ofBijective ⇑y ⋯) ((Equiv.ofBijective ⇑x ⋯).symm (x i)) = y i
Tactic:
simp only [Equiv.ofBijective_symm_apply_apply, Equiv.ofBijective_apply]
State after:
no goals

State before:
case exists_smul_eq.right
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n ≤ Fintype.card α
x y : Fin (Fintype.card α) ↪ α
⊢ Function.Bijective ⇑y
Tactic:
rw [Fintype.bijective_iff_injective_and_card]
State after:
case exists_smul_eq.right
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n ≤ Fintype.card α
x y : Fin (Fintype.card α) ↪ α
⊢ Function.Injective ⇑y ∧ Fintype.card (Fin (Fintype.card α)) = Fintype.card α

State before:
case exists_smul_eq.right
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n ≤ Fintype.card α
x y : Fin (Fintype.card α) ↪ α
⊢ Function.Injective ⇑y ∧ Fintype.card (Fin (Fintype.card α)) = Fintype.card α
Tactic:
constructor
State after:
case exists_smul_eq.right.left
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n ≤ Fintype.card α
x y : Fin (Fintype.card α) ↪ α
⊢ Function.Injective ⇑y

case exists_smul_eq.right.right
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n ≤ Fintype.card α
x y : Fin (Fintype.card α) ↪ α
⊢ Fintype.card (Fin (Fintype.card α)) = Fintype.card α

State before:
case exists_smul_eq.right.left
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n ≤ Fintype.card α
x y : Fin (Fintype.card α) ↪ α
⊢ Function.Injective ⇑y

case exists_smul_eq.right.right
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n ≤ Fintype.card α
x y : Fin (Fintype.card α) ↪ α
⊢ Fintype.card (Fin (Fintype.card α)) = Fintype.card α
Tactic:
apply EmbeddingLike.injective
State after:
case exists_smul_eq.right.right
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n ≤ Fintype.card α
x y : Fin (Fintype.card α) ↪ α
⊢ Fintype.card (Fin (Fintype.card α)) = Fintype.card α

State before:
case exists_smul_eq.right.right
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n ≤ Fintype.card α
x y : Fin (Fintype.card α) ↪ α
⊢ Fintype.card (Fin (Fintype.card α)) = Fintype.card α
Tactic:
exact Fintype.card_fin (Fintype.card α)
State after:
no goals

State before:
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n > Fintype.card α
this : IsEmpty (Fin n ↪ α)
⊢ IsMultiplyPretransitive (Equiv.Perm α) α n
Tactic:
apply IsPretransitive.mk
State after:
case exists_smul_eq
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n > Fintype.card α
this : IsEmpty (Fin n ↪ α)
⊢ ∀ (x y : Fin n ↪ α), ∃ g, g • x = y

State before:
case exists_smul_eq
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n > Fintype.card α
this : IsEmpty (Fin n ↪ α)
⊢ ∀ (x y : Fin n ↪ α), ∃ g, g • x = y
Tactic:
intro x
State after:
case exists_smul_eq
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n > Fintype.card α
this : IsEmpty (Fin n ↪ α)
x : Fin n ↪ α
⊢ ∀ (y : Fin n ↪ α), ∃ g, g • x = y

State before:
case exists_smul_eq
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n > Fintype.card α
this : IsEmpty (Fin n ↪ α)
x : Fin n ↪ α
⊢ ∀ (y : Fin n ↪ α), ∃ g, g • x = y
Tactic:
exfalso
State after:
case exists_smul_eq
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n > Fintype.card α
this : IsEmpty (Fin n ↪ α)
x : Fin n ↪ α
⊢ False

State before:
case exists_smul_eq
M : Type ?u.240457
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
n : ℕ
hn : n > Fintype.card α
this : IsEmpty (Fin n ↪ α)
x : Fin n ↪ α
⊢ False
Tactic:
exact this.false  x
State after:
no goals