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

State before:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : IsMultiplyPretransitive M α n
m : ℕ
hmn : m ≤ n
hα : ↑n ≤ PartENat.card α
⊢ IsMultiplyPretransitive M α m
Tactic:
unfold IsMultiplyPretransitive
State after:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : IsMultiplyPretransitive M α n
m : ℕ
hmn : m ≤ n
hα : ↑n ≤ PartENat.card α
⊢ IsPretransitive M (Fin m ↪ α)

State before:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : IsMultiplyPretransitive M α n
m : ℕ
hmn : m ≤ n
hα : ↑n ≤ PartENat.card α
⊢ IsPretransitive M (Fin m ↪ α)
Tactic:
let hn_eq := hn.exists_smul_eq
State after:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : IsMultiplyPretransitive M α n
m : ℕ
hmn : m ≤ n
hα : ↑n ≤ PartENat.card α
hn_eq : ∀ (x y : Fin n ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
⊢ IsPretransitive M (Fin m ↪ α)

State before:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : IsMultiplyPretransitive M α n
m : ℕ
hmn : m ≤ n
hα : ↑n ≤ PartENat.card α
hn_eq : ∀ (x y : Fin n ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
⊢ IsPretransitive M (Fin m ↪ α)
Tactic:
apply IsPretransitive.mk
State after:
case exists_smul_eq
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : IsMultiplyPretransitive M α n
m : ℕ
hmn : m ≤ n
hα : ↑n ≤ PartENat.card α
hn_eq : ∀ (x y : Fin n ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
⊢ ∀ (x y : Fin m ↪ α), ∃ g, g • x = y

State before:
case exists_smul_eq
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : IsMultiplyPretransitive M α n
m : ℕ
hmn : m ≤ n
hα : ↑n ≤ PartENat.card α
hn_eq : ∀ (x y : Fin n ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
⊢ ∀ (x y : Fin m ↪ α), ∃ g, g • x = y
Tactic:
intro x y
State after:
case exists_smul_eq
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : IsMultiplyPretransitive M α n
m : ℕ
hmn : m ≤ n
hα : ↑n ≤ PartENat.card α
hn_eq : ∀ (x y : Fin n ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : Fin m ↪ α
⊢ ∃ g, g • x = y

State before:
case exists_smul_eq
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : IsMultiplyPretransitive M α n
m : ℕ
hmn : m ≤ n
hα : ↑n ≤ PartENat.card α
hn_eq : ∀ (x y : Fin n ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : Fin m ↪ α
⊢ ∃ g, g • x = y
Tactic:
obtain ⟨x', hx'⟩ := may_extend hmn hα x
State after:
case exists_smul_eq.intro
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : IsMultiplyPretransitive M α n
m : ℕ
hmn : m ≤ n
hα : ↑n ≤ PartENat.card α
hn_eq : ∀ (x y : Fin n ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : Fin m ↪ α
x' : Fin n ↪ α
hx' : Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding x' = x
⊢ ∃ g, g • x = y

State before:
case exists_smul_eq.intro
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : IsMultiplyPretransitive M α n
m : ℕ
hmn : m ≤ n
hα : ↑n ≤ PartENat.card α
hn_eq : ∀ (x y : Fin n ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : Fin m ↪ α
x' : Fin n ↪ α
hx' : Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding x' = x
⊢ ∃ g, g • x = y
Tactic:
obtain ⟨y', hy'⟩ := may_extend hmn hα y
State after:
case exists_smul_eq.intro.intro
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : IsMultiplyPretransitive M α n
m : ℕ
hmn : m ≤ n
hα : ↑n ≤ PartENat.card α
hn_eq : ∀ (x y : Fin n ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : Fin m ↪ α
x' : Fin n ↪ α
hx' : Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding x' = x
y' : Fin n ↪ α
hy' : Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding y' = y
⊢ ∃ g, g • x = y

State before:
case exists_smul_eq.intro.intro
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : IsMultiplyPretransitive M α n
m : ℕ
hmn : m ≤ n
hα : ↑n ≤ PartENat.card α
hn_eq : ∀ (x y : Fin n ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : Fin m ↪ α
x' : Fin n ↪ α
hx' : Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding x' = x
y' : Fin n ↪ α
hy' : Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding y' = y
⊢ ∃ g, g • x = y
Tactic:
obtain ⟨g, hg⟩ := hn_eq x' y'
State after:
case exists_smul_eq.intro.intro.intro
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : IsMultiplyPretransitive M α n
m : ℕ
hmn : m ≤ n
hα : ↑n ≤ PartENat.card α
hn_eq : ∀ (x y : Fin n ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : Fin m ↪ α
x' : Fin n ↪ α
hx' : Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding x' = x
y' : Fin n ↪ α
hy' : Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding y' = y
g : M
hg : g • x' = y'
⊢ ∃ g, g • x = y

State before:
case exists_smul_eq.intro.intro.intro
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : IsMultiplyPretransitive M α n
m : ℕ
hmn : m ≤ n
hα : ↑n ≤ PartENat.card α
hn_eq : ∀ (x y : Fin n ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : Fin m ↪ α
x' : Fin n ↪ α
hx' : Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding x' = x
y' : Fin n ↪ α
hy' : Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding y' = y
g : M
hg : g • x' = y'
⊢ ∃ g, g • x = y
Tactic:
use g
State after:
case h
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : IsMultiplyPretransitive M α n
m : ℕ
hmn : m ≤ n
hα : ↑n ≤ PartENat.card α
hn_eq : ∀ (x y : Fin n ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : Fin m ↪ α
x' : Fin n ↪ α
hx' : Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding x' = x
y' : Fin n ↪ α
hy' : Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding y' = y
g : M
hg : g • x' = y'
⊢ g • x = y

State before:
case h
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : IsMultiplyPretransitive M α n
m : ℕ
hmn : m ≤ n
hα : ↑n ≤ PartENat.card α
hn_eq : ∀ (x y : Fin n ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : Fin m ↪ α
x' : Fin n ↪ α
hx' : Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding x' = x
y' : Fin n ↪ α
hy' : Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding y' = y
g : M
hg : g • x' = y'
⊢ g • x = y
Tactic:
ext
State after:
case h.h
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : IsMultiplyPretransitive M α n
m : ℕ
hmn : m ≤ n
hα : ↑n ≤ PartENat.card α
hn_eq : ∀ (x y : Fin n ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : Fin m ↪ α
x' : Fin n ↪ α
hx' : Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding x' = x
y' : Fin n ↪ α
hy' : Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding y' = y
g : M
hg : g • x' = y'
x✝ : Fin m
⊢ (g • x) x✝ = y x✝

State before:
case h.h
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : IsMultiplyPretransitive M α n
m : ℕ
hmn : m ≤ n
hα : ↑n ≤ PartENat.card α
hn_eq : ∀ (x y : Fin n ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : Fin m ↪ α
x' : Fin n ↪ α
hx' : Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding x' = x
y' : Fin n ↪ α
hy' : Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding y' = y
g : M
hg : g • x' = y'
x✝ : Fin m
⊢ (g • x) x✝ = y x✝
Tactic:
rw [← hy', ← hx', ← hg]
State after:
case h.h
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : IsMultiplyPretransitive M α n
m : ℕ
hmn : m ≤ n
hα : ↑n ≤ PartENat.card α
hn_eq : ∀ (x y : Fin n ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : Fin m ↪ α
x' : Fin n ↪ α
hx' : Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding x' = x
y' : Fin n ↪ α
hy' : Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding y' = y
g : M
hg : g • x' = y'
x✝ : Fin m
⊢ (g • Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding x') x✝ =
    (Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding (g • x')) x✝

State before:
case h.h
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : IsMultiplyPretransitive M α n
m : ℕ
hmn : m ≤ n
hα : ↑n ≤ PartENat.card α
hn_eq : ∀ (x y : Fin n ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : Fin m ↪ α
x' : Fin n ↪ α
hx' : Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding x' = x
y' : Fin n ↪ α
hy' : Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding y' = y
g : M
hg : g • x' = y'
x✝ : Fin m
⊢ (g • Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding x') x✝ =
    (Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding (g • x')) x✝
Tactic:
rfl
State after:
no goals