Theorem: MulAction.IsMultiplyPretransitive.eq_top_of_is_full_minus_one_pretransitive (Jordan/MultipleTransitivity.lean)

State before:
M : Type ?u.248388
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
⊢ G = ⊤
Tactic:
let j : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) :=
  (Fin.castLEEmb ((Fintype.card α).sub_le 1)).toEmbedding
State after:
M : Type ?u.248388
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := (Fin.castLEEmb ⋯).toEmbedding
⊢ G = ⊤

State before:
M : Type ?u.248388
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := (Fin.castLEEmb ⋯).toEmbedding
⊢ G = ⊤
Tactic:
rw [eq_top_iff]
State after:
M : Type ?u.248388
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := (Fin.castLEEmb ⋯).toEmbedding
⊢ ⊤ ≤ G

State before:
M : Type ?u.248388
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := (Fin.castLEEmb ⋯).toEmbedding
⊢ ⊤ ≤ G
Tactic:
intro k _
State after:
M : Type ?u.248388
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := (Fin.castLEEmb ⋯).toEmbedding
k : Equiv.Perm α
a✝ : k ∈ ⊤
⊢ k ∈ G

State before:
M : Type ?u.248388
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := (Fin.castLEEmb ⋯).toEmbedding
k : Equiv.Perm α
a✝ : k ∈ ⊤
⊢ k ∈ G
Tactic:
let x : Fin (Fintype.card α) ↪ α := (Fintype.equivFinOfCardEq rfl).symm.toEmbedding
State after:
M : Type ?u.248388
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := (Fin.castLEEmb ⋯).toEmbedding
k : Equiv.Perm α
a✝ : k ∈ ⊤
x : Fin (Fintype.card α) ↪ α := Equiv.toEmbedding (Fintype.equivFinOfCardEq ⋯).symm
⊢ k ∈ G

State before:
M : Type ?u.248388
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := (Fin.castLEEmb ⋯).toEmbedding
k : Equiv.Perm α
a✝ : k ∈ ⊤
x : Fin (Fintype.card α) ↪ α := Equiv.toEmbedding (Fintype.equivFinOfCardEq ⋯).symm
⊢ k ∈ G
Tactic:
let hmt_eq := hmt.exists_smul_eq
State after:
M : Type ?u.248388
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := (Fin.castLEEmb ⋯).toEmbedding
k : Equiv.Perm α
a✝ : k ∈ ⊤
x : Fin (Fintype.card α) ↪ α := Equiv.toEmbedding (Fintype.equivFinOfCardEq ⋯).symm
hmt_eq : ∀ (x y : Fin (Fintype.card α - 1) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
⊢ k ∈ G

State before:
M : Type ?u.248388
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := (Fin.castLEEmb ⋯).toEmbedding
k : Equiv.Perm α
a✝ : k ∈ ⊤
x : Fin (Fintype.card α) ↪ α := Equiv.toEmbedding (Fintype.equivFinOfCardEq ⋯).symm
hmt_eq : ∀ (x y : Fin (Fintype.card α - 1) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
⊢ k ∈ G
Tactic:
let x' := j.trans x
State after:
M : Type ?u.248388
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := (Fin.castLEEmb ⋯).toEmbedding
k : Equiv.Perm α
a✝ : k ∈ ⊤
x : Fin (Fintype.card α) ↪ α := Equiv.toEmbedding (Fintype.equivFinOfCardEq ⋯).symm
hmt_eq : ∀ (x y : Fin (Fintype.card α - 1) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x' : Fin (Fintype.card α - 1) ↪ α := Function.Embedding.trans j x
⊢ k ∈ G

State before:
M : Type ?u.248388
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := (Fin.castLEEmb ⋯).toEmbedding
k : Equiv.Perm α
a✝ : k ∈ ⊤
x : Fin (Fintype.card α) ↪ α := Equiv.toEmbedding (Fintype.equivFinOfCardEq ⋯).symm
hmt_eq : ∀ (x y : Fin (Fintype.card α - 1) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x' : Fin (Fintype.card α - 1) ↪ α := Function.Embedding.trans j x
⊢ k ∈ G
Tactic:
obtain ⟨g, hg'⟩ := hmt_eq x' (k • x')
State after:
case intro
M : Type ?u.248388
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := (Fin.castLEEmb ⋯).toEmbedding
k : Equiv.Perm α
a✝ : k ∈ ⊤
x : Fin (Fintype.card α) ↪ α := Equiv.toEmbedding (Fintype.equivFinOfCardEq ⋯).symm
hmt_eq : ∀ (x y : Fin (Fintype.card α - 1) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x' : Fin (Fintype.card α - 1) ↪ α := Function.Embedding.trans j x
g : ↥G
hg' : g • x' = k • x'
⊢ k ∈ G

State before:
case intro
M : Type ?u.248388
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := (Fin.castLEEmb ⋯).toEmbedding
k : Equiv.Perm α
a✝ : k ∈ ⊤
x : Fin (Fintype.card α) ↪ α := Equiv.toEmbedding (Fintype.equivFinOfCardEq ⋯).symm
hmt_eq : ∀ (x y : Fin (Fintype.card α - 1) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x' : Fin (Fintype.card α - 1) ↪ α := Function.Embedding.trans j x
g : ↥G
hg' : g • x' = k • x'
⊢ k ∈ G
Tactic:
suffices k = g by rw [this]; exact SetLike.coe_mem g
State after:
case intro
M : Type ?u.248388
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := (Fin.castLEEmb ⋯).toEmbedding
k : Equiv.Perm α
a✝ : k ∈ ⊤
x : Fin (Fintype.card α) ↪ α := Equiv.toEmbedding (Fintype.equivFinOfCardEq ⋯).symm
hmt_eq : ∀ (x y : Fin (Fintype.card α - 1) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x' : Fin (Fintype.card α - 1) ↪ α := Function.Embedding.trans j x
g : ↥G
hg' : g • x' = k • x'
⊢ k = ↑g

State before:
case intro
M : Type ?u.248388
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := (Fin.castLEEmb ⋯).toEmbedding
k : Equiv.Perm α
a✝ : k ∈ ⊤
x : Fin (Fintype.card α) ↪ α := Equiv.toEmbedding (Fintype.equivFinOfCardEq ⋯).symm
hmt_eq : ∀ (x y : Fin (Fintype.card α - 1) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x' : Fin (Fintype.card α - 1) ↪ α := Function.Embedding.trans j x
g : ↥G
hg' : g • x' = k • x'
⊢ k = ↑g
Tactic:
have hx : ∀ x : Fin (Fintype.card α) ↪ α, Function.Surjective x.toFun := by
  intro x
  apply Function.Bijective.surjective
  rw [Fintype.bijective_iff_injective_and_card]
  exact ⟨EmbeddingLike.injective x, Fintype.card_fin (Fintype.card α)⟩
State after:
case intro
M : Type ?u.248388
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := (Fin.castLEEmb ⋯).toEmbedding
k : Equiv.Perm α
a✝ : k ∈ ⊤
x : Fin (Fintype.card α) ↪ α := Equiv.toEmbedding (Fintype.equivFinOfCardEq ⋯).symm
hmt_eq : ∀ (x y : Fin (Fintype.card α - 1) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x' : Fin (Fintype.card α - 1) ↪ α := Function.Embedding.trans j x
g : ↥G
hg' : g • x' = k • x'
hx : ∀ (x : Fin (Fintype.card α) ↪ α), Function.Surjective x.toFun
⊢ k = ↑g

State before:
case intro
M : Type ?u.248388
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := (Fin.castLEEmb ⋯).toEmbedding
k : Equiv.Perm α
a✝ : k ∈ ⊤
x : Fin (Fintype.card α) ↪ α := Equiv.toEmbedding (Fintype.equivFinOfCardEq ⋯).symm
hmt_eq : ∀ (x y : Fin (Fintype.card α - 1) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x' : Fin (Fintype.card α - 1) ↪ α := Function.Embedding.trans j x
g : ↥G
hg' : g • x' = k • x'
hx : ∀ (x : Fin (Fintype.card α) ↪ α), Function.Surjective x.toFun
⊢ k = ↑g
Tactic:
have hgk' : ∀ (i : Fin (Fintype.card α)) (_ : i.val < Fintype.card α - 1),
  (g • x) i = (k • x) i := by
  intro i hi
  exact Function.Embedding.ext_iff.mpr hg' ⟨i.val, hi⟩
State after:
case intro
M : Type ?u.248388
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := (Fin.castLEEmb ⋯).toEmbedding
k : Equiv.Perm α
a✝ : k ∈ ⊤
x : Fin (Fintype.card α) ↪ α := Equiv.toEmbedding (Fintype.equivFinOfCardEq ⋯).symm
hmt_eq : ∀ (x y : Fin (Fintype.card α - 1) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x' : Fin (Fintype.card α - 1) ↪ α := Function.Embedding.trans j x
g : ↥G
hg' : g • x' = k • x'
hx : ∀ (x : Fin (Fintype.card α) ↪ α), Function.Surjective x.toFun
hgk' : ∀ (i : Fin (Fintype.card α)), ↑i < Fintype.card α - 1 → (g • x) i = (k • x) i
⊢ k = ↑g

State before:
case intro
M : Type ?u.248388
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := (Fin.castLEEmb ⋯).toEmbedding
k : Equiv.Perm α
a✝ : k ∈ ⊤
x : Fin (Fintype.card α) ↪ α := Equiv.toEmbedding (Fintype.equivFinOfCardEq ⋯).symm
hmt_eq : ∀ (x y : Fin (Fintype.card α - 1) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x' : Fin (Fintype.card α - 1) ↪ α := Function.Embedding.trans j x
g : ↥G
hg' : g • x' = k • x'
hx : ∀ (x : Fin (Fintype.card α) ↪ α), Function.Surjective x.toFun
hgk' : ∀ (i : Fin (Fintype.card α)), ↑i < Fintype.card α - 1 → (g • x) i = (k • x) i
hgk : ∀ (i : Fin (Fintype.card α)), (g • x) i = (k • x) i
⊢ k = ↑g
Tactic:
apply Equiv.Perm.ext
State after:
case intro.H
M : Type ?u.248388
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := (Fin.castLEEmb ⋯).toEmbedding
k : Equiv.Perm α
a✝ : k ∈ ⊤
x : Fin (Fintype.card α) ↪ α := Equiv.toEmbedding (Fintype.equivFinOfCardEq ⋯).symm
hmt_eq : ∀ (x y : Fin (Fintype.card α - 1) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x' : Fin (Fintype.card α - 1) ↪ α := Function.Embedding.trans j x
g : ↥G
hg' : g • x' = k • x'
hx : ∀ (x : Fin (Fintype.card α) ↪ α), Function.Surjective x.toFun
hgk' : ∀ (i : Fin (Fintype.card α)), ↑i < Fintype.card α - 1 → (g • x) i = (k • x) i
hgk : ∀ (i : Fin (Fintype.card α)), (g • x) i = (k • x) i
⊢ ∀ (x : α), k x = ↑g x

State before:
case intro.H
M : Type ?u.248388
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := (Fin.castLEEmb ⋯).toEmbedding
k : Equiv.Perm α
a✝ : k ∈ ⊤
x : Fin (Fintype.card α) ↪ α := Equiv.toEmbedding (Fintype.equivFinOfCardEq ⋯).symm
hmt_eq : ∀ (x y : Fin (Fintype.card α - 1) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x' : Fin (Fintype.card α - 1) ↪ α := Function.Embedding.trans j x
g : ↥G
hg' : g • x' = k • x'
hx : ∀ (x : Fin (Fintype.card α) ↪ α), Function.Surjective x.toFun
hgk' : ∀ (i : Fin (Fintype.card α)), ↑i < Fintype.card α - 1 → (g • x) i = (k • x) i
hgk : ∀ (i : Fin (Fintype.card α)), (g • x) i = (k • x) i
⊢ ∀ (x : α), k x = ↑g x
Tactic:
intro a
State after:
case intro.H
M : Type ?u.248388
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := (Fin.castLEEmb ⋯).toEmbedding
k : Equiv.Perm α
a✝ : k ∈ ⊤
x : Fin (Fintype.card α) ↪ α := Equiv.toEmbedding (Fintype.equivFinOfCardEq ⋯).symm
hmt_eq : ∀ (x y : Fin (Fintype.card α - 1) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x' : Fin (Fintype.card α - 1) ↪ α := Function.Embedding.trans j x
g : ↥G
hg' : g • x' = k • x'
hx : ∀ (x : Fin (Fintype.card α) ↪ α), Function.Surjective x.toFun
hgk' : ∀ (i : Fin (Fintype.card α)), ↑i < Fintype.card α - 1 → (g • x) i = (k • x) i
hgk : ∀ (i : Fin (Fintype.card α)), (g • x) i = (k • x) i
a : α
⊢ k a = ↑g a

State before:
case intro.H
M : Type ?u.248388
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := (Fin.castLEEmb ⋯).toEmbedding
k : Equiv.Perm α
a✝ : k ∈ ⊤
x : Fin (Fintype.card α) ↪ α := Equiv.toEmbedding (Fintype.equivFinOfCardEq ⋯).symm
hmt_eq : ∀ (x y : Fin (Fintype.card α - 1) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x' : Fin (Fintype.card α - 1) ↪ α := Function.Embedding.trans j x
g : ↥G
hg' : g • x' = k • x'
hx : ∀ (x : Fin (Fintype.card α) ↪ α), Function.Surjective x.toFun
hgk' : ∀ (i : Fin (Fintype.card α)), ↑i < Fintype.card α - 1 → (g • x) i = (k • x) i
hgk : ∀ (i : Fin (Fintype.card α)), (g • x) i = (k • x) i
a : α
⊢ k a = ↑g a
Tactic:
obtain ⟨i, rfl⟩ := (hx x) a
State after:
case intro.H.intro
M : Type ?u.248388
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := (Fin.castLEEmb ⋯).toEmbedding
k : Equiv.Perm α
a✝ : k ∈ ⊤
x : Fin (Fintype.card α) ↪ α := Equiv.toEmbedding (Fintype.equivFinOfCardEq ⋯).symm
hmt_eq : ∀ (x y : Fin (Fintype.card α - 1) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x' : Fin (Fintype.card α - 1) ↪ α := Function.Embedding.trans j x
g : ↥G
hg' : g • x' = k • x'
hx : ∀ (x : Fin (Fintype.card α) ↪ α), Function.Surjective x.toFun
hgk' : ∀ (i : Fin (Fintype.card α)), ↑i < Fintype.card α - 1 → (g • x) i = (k • x) i
hgk : ∀ (i : Fin (Fintype.card α)), (g • x) i = (k • x) i
i : Fin (Fintype.card α)
⊢ k (x.toFun i) = ↑g (x.toFun i)

State before:
case intro.H.intro
M : Type ?u.248388
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := (Fin.castLEEmb ⋯).toEmbedding
k : Equiv.Perm α
a✝ : k ∈ ⊤
x : Fin (Fintype.card α) ↪ α := Equiv.toEmbedding (Fintype.equivFinOfCardEq ⋯).symm
hmt_eq : ∀ (x y : Fin (Fintype.card α - 1) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x' : Fin (Fintype.card α - 1) ↪ α := Function.Embedding.trans j x
g : ↥G
hg' : g • x' = k • x'
hx : ∀ (x : Fin (Fintype.card α) ↪ α), Function.Surjective x.toFun
hgk' : ∀ (i : Fin (Fintype.card α)), ↑i < Fintype.card α - 1 → (g • x) i = (k • x) i
hgk : ∀ (i : Fin (Fintype.card α)), (g • x) i = (k • x) i
i : Fin (Fintype.card α)
⊢ k (x.toFun i) = ↑g (x.toFun i)
Tactic:
let zi := hgk i
State after:
case intro.H.intro
M : Type ?u.248388
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := (Fin.castLEEmb ⋯).toEmbedding
k : Equiv.Perm α
a✝ : k ∈ ⊤
x : Fin (Fintype.card α) ↪ α := Equiv.toEmbedding (Fintype.equivFinOfCardEq ⋯).symm
hmt_eq : ∀ (x y : Fin (Fintype.card α - 1) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x' : Fin (Fintype.card α - 1) ↪ α := Function.Embedding.trans j x
g : ↥G
hg' : g • x' = k • x'
hx : ∀ (x : Fin (Fintype.card α) ↪ α), Function.Surjective x.toFun
hgk' : ∀ (i : Fin (Fintype.card α)), ↑i < Fintype.card α - 1 → (g • x) i = (k • x) i
hgk : ∀ (i : Fin (Fintype.card α)), (g • x) i = (k • x) i
i : Fin (Fintype.card α)
zi : (g • x) i = (k • x) i := hgk i
⊢ k (x.toFun i) = ↑g (x.toFun i)

State before:
case intro.H.intro
M : Type ?u.248388
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := (Fin.castLEEmb ⋯).toEmbedding
k : Equiv.Perm α
a✝ : k ∈ ⊤
x : Fin (Fintype.card α) ↪ α := Equiv.toEmbedding (Fintype.equivFinOfCardEq ⋯).symm
hmt_eq : ∀ (x y : Fin (Fintype.card α - 1) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x' : Fin (Fintype.card α - 1) ↪ α := Function.Embedding.trans j x
g : ↥G
hg' : g • x' = k • x'
hx : ∀ (x : Fin (Fintype.card α) ↪ α), Function.Surjective x.toFun
hgk' : ∀ (i : Fin (Fintype.card α)), ↑i < Fintype.card α - 1 → (g • x) i = (k • x) i
hgk : ∀ (i : Fin (Fintype.card α)), (g • x) i = (k • x) i
i : Fin (Fintype.card α)
zi : (g • x) i = (k • x) i := hgk i
⊢ k (x.toFun i) = ↑g (x.toFun i)
Tactic:
simp only [Function.Embedding.smul_apply, Equiv.Perm.smul_def] at zi
State after:
case intro.H.intro
M : Type ?u.248388
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := (Fin.castLEEmb ⋯).toEmbedding
k : Equiv.Perm α
a✝ : k ∈ ⊤
x : Fin (Fintype.card α) ↪ α := Equiv.toEmbedding (Fintype.equivFinOfCardEq ⋯).symm
hmt_eq : ∀ (x y : Fin (Fintype.card α - 1) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x' : Fin (Fintype.card α - 1) ↪ α := Function.Embedding.trans j x
g : ↥G
hg' : g • x' = k • x'
hx : ∀ (x : Fin (Fintype.card α) ↪ α), Function.Surjective x.toFun
hgk' : ∀ (i : Fin (Fintype.card α)), ↑i < Fintype.card α - 1 → (g • x) i = (k • x) i
hgk : ∀ (i : Fin (Fintype.card α)), (g • x) i = (k • x) i
i : Fin (Fintype.card α)
zi : g • x i = k (x i) := hgk i
⊢ k (x.toFun i) = ↑g (x.toFun i)

State before:
case intro.H.intro
M : Type ?u.248388
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := (Fin.castLEEmb ⋯).toEmbedding
k : Equiv.Perm α
a✝ : k ∈ ⊤
x : Fin (Fintype.card α) ↪ α := Equiv.toEmbedding (Fintype.equivFinOfCardEq ⋯).symm
hmt_eq : ∀ (x y : Fin (Fintype.card α - 1) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x' : Fin (Fintype.card α - 1) ↪ α := Function.Embedding.trans j x
g : ↥G
hg' : g • x' = k • x'
hx : ∀ (x : Fin (Fintype.card α) ↪ α), Function.Surjective x.toFun
hgk' : ∀ (i : Fin (Fintype.card α)), ↑i < Fintype.card α - 1 → (g • x) i = (k • x) i
hgk : ∀ (i : Fin (Fintype.card α)), (g • x) i = (k • x) i
i : Fin (Fintype.card α)
zi : g • x i = k (x i) := hgk i
⊢ k (x.toFun i) = ↑g (x.toFun i)
Tactic:
simp only [Function.Embedding.toFun_eq_coe]
State after:
case intro.H.intro
M : Type ?u.248388
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := (Fin.castLEEmb ⋯).toEmbedding
k : Equiv.Perm α
a✝ : k ∈ ⊤
x : Fin (Fintype.card α) ↪ α := Equiv.toEmbedding (Fintype.equivFinOfCardEq ⋯).symm
hmt_eq : ∀ (x y : Fin (Fintype.card α - 1) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x' : Fin (Fintype.card α - 1) ↪ α := Function.Embedding.trans j x
g : ↥G
hg' : g • x' = k • x'
hx : ∀ (x : Fin (Fintype.card α) ↪ α), Function.Surjective x.toFun
hgk' : ∀ (i : Fin (Fintype.card α)), ↑i < Fintype.card α - 1 → (g • x) i = (k • x) i
hgk : ∀ (i : Fin (Fintype.card α)), (g • x) i = (k • x) i
i : Fin (Fintype.card α)
zi : g • x i = k (x i) := hgk i
⊢ k (x i) = ↑g (x i)

State before:
case intro.H.intro
M : Type ?u.248388
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := (Fin.castLEEmb ⋯).toEmbedding
k : Equiv.Perm α
a✝ : k ∈ ⊤
x : Fin (Fintype.card α) ↪ α := Equiv.toEmbedding (Fintype.equivFinOfCardEq ⋯).symm
hmt_eq : ∀ (x y : Fin (Fintype.card α - 1) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x' : Fin (Fintype.card α - 1) ↪ α := Function.Embedding.trans j x
g : ↥G
hg' : g • x' = k • x'
hx : ∀ (x : Fin (Fintype.card α) ↪ α), Function.Surjective x.toFun
hgk' : ∀ (i : Fin (Fintype.card α)), ↑i < Fintype.card α - 1 → (g • x) i = (k • x) i
hgk : ∀ (i : Fin (Fintype.card α)), (g • x) i = (k • x) i
i : Fin (Fintype.card α)
zi : g • x i = k (x i) := hgk i
⊢ k (x i) = ↑g (x i)
Tactic:
rw [← zi]
State after:
case intro.H.intro
M : Type ?u.248388
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := (Fin.castLEEmb ⋯).toEmbedding
k : Equiv.Perm α
a✝ : k ∈ ⊤
x : Fin (Fintype.card α) ↪ α := Equiv.toEmbedding (Fintype.equivFinOfCardEq ⋯).symm
hmt_eq : ∀ (x y : Fin (Fintype.card α - 1) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x' : Fin (Fintype.card α - 1) ↪ α := Function.Embedding.trans j x
g : ↥G
hg' : g • x' = k • x'
hx : ∀ (x : Fin (Fintype.card α) ↪ α), Function.Surjective x.toFun
hgk' : ∀ (i : Fin (Fintype.card α)), ↑i < Fintype.card α - 1 → (g • x) i = (k • x) i
hgk : ∀ (i : Fin (Fintype.card α)), (g • x) i = (k • x) i
i : Fin (Fintype.card α)
zi : g • x i = k (x i) := hgk i
⊢ g • x i = ↑g (x i)

State before:
case intro.H.intro
M : Type ?u.248388
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := (Fin.castLEEmb ⋯).toEmbedding
k : Equiv.Perm α
a✝ : k ∈ ⊤
x : Fin (Fintype.card α) ↪ α := Equiv.toEmbedding (Fintype.equivFinOfCardEq ⋯).symm
hmt_eq : ∀ (x y : Fin (Fintype.card α - 1) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x' : Fin (Fintype.card α - 1) ↪ α := Function.Embedding.trans j x
g : ↥G
hg' : g • x' = k • x'
hx : ∀ (x : Fin (Fintype.card α) ↪ α), Function.Surjective x.toFun
hgk' : ∀ (i : Fin (Fintype.card α)), ↑i < Fintype.card α - 1 → (g • x) i = (k • x) i
hgk : ∀ (i : Fin (Fintype.card α)), (g • x) i = (k • x) i
i : Fin (Fintype.card α)
zi : g • x i = k (x i) := hgk i
⊢ g • x i = ↑g (x i)
Tactic:
rfl
State after:
no goals

State before:
M : Type ?u.248388
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := (Fin.castLEEmb ⋯).toEmbedding
k : Equiv.Perm α
a✝ : k ∈ ⊤
x : Fin (Fintype.card α) ↪ α := Equiv.toEmbedding (Fintype.equivFinOfCardEq ⋯).symm
hmt_eq : ∀ (x y : Fin (Fintype.card α - 1) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x' : Fin (Fintype.card α - 1) ↪ α := Function.Embedding.trans j x
g : ↥G
hg' : g • x' = k • x'
this : k = ↑g
⊢ k ∈ G
Tactic:
rw [this]
State after:
M : Type ?u.248388
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := (Fin.castLEEmb ⋯).toEmbedding
k : Equiv.Perm α
a✝ : k ∈ ⊤
x : Fin (Fintype.card α) ↪ α := Equiv.toEmbedding (Fintype.equivFinOfCardEq ⋯).symm
hmt_eq : ∀ (x y : Fin (Fintype.card α - 1) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x' : Fin (Fintype.card α - 1) ↪ α := Function.Embedding.trans j x
g : ↥G
hg' : g • x' = k • x'
this : k = ↑g
⊢ ↑g ∈ G

State before:
M : Type ?u.248388
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := (Fin.castLEEmb ⋯).toEmbedding
k : Equiv.Perm α
a✝ : k ∈ ⊤
x : Fin (Fintype.card α) ↪ α := Equiv.toEmbedding (Fintype.equivFinOfCardEq ⋯).symm
hmt_eq : ∀ (x y : Fin (Fintype.card α - 1) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x' : Fin (Fintype.card α - 1) ↪ α := Function.Embedding.trans j x
g : ↥G
hg' : g • x' = k • x'
this : k = ↑g
⊢ ↑g ∈ G
Tactic:
exact SetLike.coe_mem g
State after:
no goals

State before:
M : Type ?u.248388
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := (Fin.castLEEmb ⋯).toEmbedding
k : Equiv.Perm α
a✝ : k ∈ ⊤
x : Fin (Fintype.card α) ↪ α := Equiv.toEmbedding (Fintype.equivFinOfCardEq ⋯).symm
hmt_eq : ∀ (x y : Fin (Fintype.card α - 1) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x' : Fin (Fintype.card α - 1) ↪ α := Function.Embedding.trans j x
g : ↥G
hg' : g • x' = k • x'
⊢ ∀ (x : Fin (Fintype.card α) ↪ α), Function.Surjective x.toFun
Tactic:
intro x
State after:
M : Type ?u.248388
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := (Fin.castLEEmb ⋯).toEmbedding
k : Equiv.Perm α
a✝ : k ∈ ⊤
x✝ : Fin (Fintype.card α) ↪ α := Equiv.toEmbedding (Fintype.equivFinOfCardEq ⋯).symm
hmt_eq : ∀ (x y : Fin (Fintype.card α - 1) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x' : Fin (Fintype.card α - 1) ↪ α := Function.Embedding.trans j x✝
g : ↥G
hg' : g • x' = k • x'
x : Fin (Fintype.card α) ↪ α
⊢ Function.Surjective x.toFun

State before:
M : Type ?u.248388
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := (Fin.castLEEmb ⋯).toEmbedding
k : Equiv.Perm α
a✝ : k ∈ ⊤
x✝ : Fin (Fintype.card α) ↪ α := Equiv.toEmbedding (Fintype.equivFinOfCardEq ⋯).symm
hmt_eq : ∀ (x y : Fin (Fintype.card α - 1) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x' : Fin (Fintype.card α - 1) ↪ α := Function.Embedding.trans j x✝
g : ↥G
hg' : g • x' = k • x'
x : Fin (Fintype.card α) ↪ α
⊢ Function.Surjective x.toFun
Tactic:
apply Function.Bijective.surjective
State after:
case hf
M : Type ?u.248388
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := (Fin.castLEEmb ⋯).toEmbedding
k : Equiv.Perm α
a✝ : k ∈ ⊤
x✝ : Fin (Fintype.card α) ↪ α := Equiv.toEmbedding (Fintype.equivFinOfCardEq ⋯).symm
hmt_eq : ∀ (x y : Fin (Fintype.card α - 1) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x' : Fin (Fintype.card α - 1) ↪ α := Function.Embedding.trans j x✝
g : ↥G
hg' : g • x' = k • x'
x : Fin (Fintype.card α) ↪ α
⊢ Function.Bijective x.toFun

State before:
case hf
M : Type ?u.248388
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := (Fin.castLEEmb ⋯).toEmbedding
k : Equiv.Perm α
a✝ : k ∈ ⊤
x✝ : Fin (Fintype.card α) ↪ α := Equiv.toEmbedding (Fintype.equivFinOfCardEq ⋯).symm
hmt_eq : ∀ (x y : Fin (Fintype.card α - 1) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x' : Fin (Fintype.card α - 1) ↪ α := Function.Embedding.trans j x✝
g : ↥G
hg' : g • x' = k • x'
x : Fin (Fintype.card α) ↪ α
⊢ Function.Bijective x.toFun
Tactic:
rw [Fintype.bijective_iff_injective_and_card]
State after:
case hf
M : Type ?u.248388
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := (Fin.castLEEmb ⋯).toEmbedding
k : Equiv.Perm α
a✝ : k ∈ ⊤
x✝ : Fin (Fintype.card α) ↪ α := Equiv.toEmbedding (Fintype.equivFinOfCardEq ⋯).symm
hmt_eq : ∀ (x y : Fin (Fintype.card α - 1) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x' : Fin (Fintype.card α - 1) ↪ α := Function.Embedding.trans j x✝
g : ↥G
hg' : g • x' = k • x'
x : Fin (Fintype.card α) ↪ α
⊢ Function.Injective x.toFun ∧ Fintype.card (Fin (Fintype.card α)) = Fintype.card α

State before:
case hf
M : Type ?u.248388
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := (Fin.castLEEmb ⋯).toEmbedding
k : Equiv.Perm α
a✝ : k ∈ ⊤
x✝ : Fin (Fintype.card α) ↪ α := Equiv.toEmbedding (Fintype.equivFinOfCardEq ⋯).symm
hmt_eq : ∀ (x y : Fin (Fintype.card α - 1) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x' : Fin (Fintype.card α - 1) ↪ α := Function.Embedding.trans j x✝
g : ↥G
hg' : g • x' = k • x'
x : Fin (Fintype.card α) ↪ α
⊢ Function.Injective x.toFun ∧ Fintype.card (Fin (Fintype.card α)) = Fintype.card α
Tactic:
exact ⟨EmbeddingLike.injective x, Fintype.card_fin (Fintype.card α)⟩
State after:
no goals

State before:
M : Type ?u.248388
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := (Fin.castLEEmb ⋯).toEmbedding
k : Equiv.Perm α
a✝ : k ∈ ⊤
x : Fin (Fintype.card α) ↪ α := Equiv.toEmbedding (Fintype.equivFinOfCardEq ⋯).symm
hmt_eq : ∀ (x y : Fin (Fintype.card α - 1) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x' : Fin (Fintype.card α - 1) ↪ α := Function.Embedding.trans j x
g : ↥G
hg' : g • x' = k • x'
hx : ∀ (x : Fin (Fintype.card α) ↪ α), Function.Surjective x.toFun
⊢ ∀ (i : Fin (Fintype.card α)), ↑i < Fintype.card α - 1 → (g • x) i = (k • x) i
Tactic:
intro i hi
State after:
M : Type ?u.248388
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := (Fin.castLEEmb ⋯).toEmbedding
k : Equiv.Perm α
a✝ : k ∈ ⊤
x : Fin (Fintype.card α) ↪ α := Equiv.toEmbedding (Fintype.equivFinOfCardEq ⋯).symm
hmt_eq : ∀ (x y : Fin (Fintype.card α - 1) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x' : Fin (Fintype.card α - 1) ↪ α := Function.Embedding.trans j x
g : ↥G
hg' : g • x' = k • x'
hx : ∀ (x : Fin (Fintype.card α) ↪ α), Function.Surjective x.toFun
i : Fin (Fintype.card α)
hi : ↑i < Fintype.card α - 1
⊢ (g • x) i = (k • x) i

State before:
M : Type ?u.248388
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := (Fin.castLEEmb ⋯).toEmbedding
k : Equiv.Perm α
a✝ : k ∈ ⊤
x : Fin (Fintype.card α) ↪ α := Equiv.toEmbedding (Fintype.equivFinOfCardEq ⋯).symm
hmt_eq : ∀ (x y : Fin (Fintype.card α - 1) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x' : Fin (Fintype.card α - 1) ↪ α := Function.Embedding.trans j x
g : ↥G
hg' : g • x' = k • x'
hx : ∀ (x : Fin (Fintype.card α) ↪ α), Function.Surjective x.toFun
i : Fin (Fintype.card α)
hi : ↑i < Fintype.card α - 1
⊢ (g • x) i = (k • x) i
Tactic:
exact Function.Embedding.ext_iff.mpr hg' ⟨i.val, hi⟩
State after:
no goals

State before:
M : Type ?u.248388
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := (Fin.castLEEmb ⋯).toEmbedding
k : Equiv.Perm α
a✝ : k ∈ ⊤
x : Fin (Fintype.card α) ↪ α := Equiv.toEmbedding (Fintype.equivFinOfCardEq ⋯).symm
hmt_eq : ∀ (x y : Fin (Fintype.card α - 1) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x' : Fin (Fintype.card α - 1) ↪ α := Function.Embedding.trans j x
g : ↥G
hg' : g • x' = k • x'
hx : ∀ (x : Fin (Fintype.card α) ↪ α), Function.Surjective x.toFun
hgk' : ∀ (i : Fin (Fintype.card α)), ↑i < Fintype.card α - 1 → (g • x) i = (k • x) i
⊢ ∀ (i : Fin (Fintype.card α)), (g • x) i = (k • x) i
Tactic:
intro i
State after:
M : Type ?u.248388
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := (Fin.castLEEmb ⋯).toEmbedding
k : Equiv.Perm α
a✝ : k ∈ ⊤
x : Fin (Fintype.card α) ↪ α := Equiv.toEmbedding (Fintype.equivFinOfCardEq ⋯).symm
hmt_eq : ∀ (x y : Fin (Fintype.card α - 1) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x' : Fin (Fintype.card α - 1) ↪ α := Function.Embedding.trans j x
g : ↥G
hg' : g • x' = k • x'
hx : ∀ (x : Fin (Fintype.card α) ↪ α), Function.Surjective x.toFun
hgk' : ∀ (i : Fin (Fintype.card α)), ↑i < Fintype.card α - 1 → (g • x) i = (k • x) i
i : Fin (Fintype.card α)
⊢ (g • x) i = (k • x) i

State before:
M : Type ?u.248388
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := (Fin.castLEEmb ⋯).toEmbedding
k : Equiv.Perm α
a✝ : k ∈ ⊤
x : Fin (Fintype.card α) ↪ α := Equiv.toEmbedding (Fintype.equivFinOfCardEq ⋯).symm
hmt_eq : ∀ (x y : Fin (Fintype.card α - 1) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x' : Fin (Fintype.card α - 1) ↪ α := Function.Embedding.trans j x
g : ↥G
hg' : g • x' = k • x'
hx : ∀ (x : Fin (Fintype.card α) ↪ α), Function.Surjective x.toFun
hgk' : ∀ (i : Fin (Fintype.card α)), ↑i < Fintype.card α - 1 → (g • x) i = (k • x) i
i : Fin (Fintype.card α)
⊢ (g • x) i = (k • x) i
Tactic:
cases' aux_lt_iff_lt_or_eq i.prop with hi hi
State after:
case inl
M : Type ?u.248388
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := (Fin.castLEEmb ⋯).toEmbedding
k : Equiv.Perm α
a✝ : k ∈ ⊤
x : Fin (Fintype.card α) ↪ α := Equiv.toEmbedding (Fintype.equivFinOfCardEq ⋯).symm
hmt_eq : ∀ (x y : Fin (Fintype.card α - 1) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x' : Fin (Fintype.card α - 1) ↪ α := Function.Embedding.trans j x
g : ↥G
hg' : g • x' = k • x'
hx : ∀ (x : Fin (Fintype.card α) ↪ α), Function.Surjective x.toFun
hgk' : ∀ (i : Fin (Fintype.card α)), ↑i < Fintype.card α - 1 → (g • x) i = (k • x) i
i : Fin (Fintype.card α)
hi : ↑i < Fintype.card α - 1
⊢ (g • x) i = (k • x) i

case inr
M : Type ?u.248388
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := (Fin.castLEEmb ⋯).toEmbedding
k : Equiv.Perm α
a✝ : k ∈ ⊤
x : Fin (Fintype.card α) ↪ α := Equiv.toEmbedding (Fintype.equivFinOfCardEq ⋯).symm
hmt_eq : ∀ (x y : Fin (Fintype.card α - 1) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x' : Fin (Fintype.card α - 1) ↪ α := Function.Embedding.trans j x
g : ↥G
hg' : g • x' = k • x'
hx : ∀ (x : Fin (Fintype.card α) ↪ α), Function.Surjective x.toFun
hgk' : ∀ (i : Fin (Fintype.card α)), ↑i < Fintype.card α - 1 → (g • x) i = (k • x) i
i : Fin (Fintype.card α)
hi : ↑i = Fintype.card α - 1
⊢ (g • x) i = (k • x) i

State before:
case inl
M : Type ?u.248388
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := (Fin.castLEEmb ⋯).toEmbedding
k : Equiv.Perm α
a✝ : k ∈ ⊤
x : Fin (Fintype.card α) ↪ α := Equiv.toEmbedding (Fintype.equivFinOfCardEq ⋯).symm
hmt_eq : ∀ (x y : Fin (Fintype.card α - 1) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x' : Fin (Fintype.card α - 1) ↪ α := Function.Embedding.trans j x
g : ↥G
hg' : g • x' = k • x'
hx : ∀ (x : Fin (Fintype.card α) ↪ α), Function.Surjective x.toFun
hgk' : ∀ (i : Fin (Fintype.card α)), ↑i < Fintype.card α - 1 → (g • x) i = (k • x) i
i : Fin (Fintype.card α)
hi : ↑i < Fintype.card α - 1
⊢ (g • x) i = (k • x) i
Tactic:
exact hgk' i hi
State after:
no goals

State before:
case inr
M : Type ?u.248388
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := (Fin.castLEEmb ⋯).toEmbedding
k : Equiv.Perm α
a✝ : k ∈ ⊤
x : Fin (Fintype.card α) ↪ α := Equiv.toEmbedding (Fintype.equivFinOfCardEq ⋯).symm
hmt_eq : ∀ (x y : Fin (Fintype.card α - 1) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x' : Fin (Fintype.card α - 1) ↪ α := Function.Embedding.trans j x
g : ↥G
hg' : g • x' = k • x'
hx : ∀ (x : Fin (Fintype.card α) ↪ α), Function.Surjective x.toFun
hgk' : ∀ (i : Fin (Fintype.card α)), ↑i < Fintype.card α - 1 → (g • x) i = (k • x) i
i : Fin (Fintype.card α)
hi : ↑i = Fintype.card α - 1
⊢ (g • x) i = (k • x) i
Tactic:
obtain ⟨j, hxj : (k • x) j = (g • x) i⟩ := hx (k • x) ((g • x) i)
State after:
case inr.intro
M : Type ?u.248388
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j✝ : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := (Fin.castLEEmb ⋯).toEmbedding
k : Equiv.Perm α
a✝ : k ∈ ⊤
x : Fin (Fintype.card α) ↪ α := Equiv.toEmbedding (Fintype.equivFinOfCardEq ⋯).symm
hmt_eq : ∀ (x y : Fin (Fintype.card α - 1) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x' : Fin (Fintype.card α - 1) ↪ α := Function.Embedding.trans j✝ x
g : ↥G
hg' : g • x' = k • x'
hx : ∀ (x : Fin (Fintype.card α) ↪ α), Function.Surjective x.toFun
hgk' : ∀ (i : Fin (Fintype.card α)), ↑i < Fintype.card α - 1 → (g • x) i = (k • x) i
i : Fin (Fintype.card α)
hi : ↑i = Fintype.card α - 1
j : Fin (Fintype.card α)
hxj : (k • x) j = (g • x) i
⊢ (g • x) i = (k • x) i

State before:
case inr.intro
M : Type ?u.248388
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j✝ : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := (Fin.castLEEmb ⋯).toEmbedding
k : Equiv.Perm α
a✝ : k ∈ ⊤
x : Fin (Fintype.card α) ↪ α := Equiv.toEmbedding (Fintype.equivFinOfCardEq ⋯).symm
hmt_eq : ∀ (x y : Fin (Fintype.card α - 1) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x' : Fin (Fintype.card α - 1) ↪ α := Function.Embedding.trans j✝ x
g : ↥G
hg' : g • x' = k • x'
hx : ∀ (x : Fin (Fintype.card α) ↪ α), Function.Surjective x.toFun
hgk' : ∀ (i : Fin (Fintype.card α)), ↑i < Fintype.card α - 1 → (g • x) i = (k • x) i
i : Fin (Fintype.card α)
hi : ↑i = Fintype.card α - 1
j : Fin (Fintype.card α)
hxj : (k • x) j = (g • x) i
⊢ (g • x) i = (k • x) i
Tactic:
cases' aux_lt_iff_lt_or_eq j.prop with hj hj
State after:
case inr.intro.inl
M : Type ?u.248388
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j✝ : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := (Fin.castLEEmb ⋯).toEmbedding
k : Equiv.Perm α
a✝ : k ∈ ⊤
x : Fin (Fintype.card α) ↪ α := Equiv.toEmbedding (Fintype.equivFinOfCardEq ⋯).symm
hmt_eq : ∀ (x y : Fin (Fintype.card α - 1) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x' : Fin (Fintype.card α - 1) ↪ α := Function.Embedding.trans j✝ x
g : ↥G
hg' : g • x' = k • x'
hx : ∀ (x : Fin (Fintype.card α) ↪ α), Function.Surjective x.toFun
hgk' : ∀ (i : Fin (Fintype.card α)), ↑i < Fintype.card α - 1 → (g • x) i = (k • x) i
i : Fin (Fintype.card α)
hi : ↑i = Fintype.card α - 1
j : Fin (Fintype.card α)
hxj : (k • x) j = (g • x) i
hj : ↑j < Fintype.card α - 1
⊢ (g • x) i = (k • x) i

case inr.intro.inr
M : Type ?u.248388
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j✝ : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := (Fin.castLEEmb ⋯).toEmbedding
k : Equiv.Perm α
a✝ : k ∈ ⊤
x : Fin (Fintype.card α) ↪ α := Equiv.toEmbedding (Fintype.equivFinOfCardEq ⋯).symm
hmt_eq : ∀ (x y : Fin (Fintype.card α - 1) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x' : Fin (Fintype.card α - 1) ↪ α := Function.Embedding.trans j✝ x
g : ↥G
hg' : g • x' = k • x'
hx : ∀ (x : Fin (Fintype.card α) ↪ α), Function.Surjective x.toFun
hgk' : ∀ (i : Fin (Fintype.card α)), ↑i < Fintype.card α - 1 → (g • x) i = (k • x) i
i : Fin (Fintype.card α)
hi : ↑i = Fintype.card α - 1
j : Fin (Fintype.card α)
hxj : (k • x) j = (g • x) i
hj : ↑j = Fintype.card α - 1
⊢ (g • x) i = (k • x) i

State before:
case inr.intro.inl
M : Type ?u.248388
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j✝ : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := (Fin.castLEEmb ⋯).toEmbedding
k : Equiv.Perm α
a✝ : k ∈ ⊤
x : Fin (Fintype.card α) ↪ α := Equiv.toEmbedding (Fintype.equivFinOfCardEq ⋯).symm
hmt_eq : ∀ (x y : Fin (Fintype.card α - 1) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x' : Fin (Fintype.card α - 1) ↪ α := Function.Embedding.trans j✝ x
g : ↥G
hg' : g • x' = k • x'
hx : ∀ (x : Fin (Fintype.card α) ↪ α), Function.Surjective x.toFun
hgk' : ∀ (i : Fin (Fintype.card α)), ↑i < Fintype.card α - 1 → (g • x) i = (k • x) i
i : Fin (Fintype.card α)
hi : ↑i = Fintype.card α - 1
j : Fin (Fintype.card α)
hxj : (k • x) j = (g • x) i
hj : ↑j < Fintype.card α - 1
⊢ (g • x) i = (k • x) i
Tactic:
exfalso
State after:
case inr.intro.inl
M : Type ?u.248388
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j✝ : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := (Fin.castLEEmb ⋯).toEmbedding
k : Equiv.Perm α
a✝ : k ∈ ⊤
x : Fin (Fintype.card α) ↪ α := Equiv.toEmbedding (Fintype.equivFinOfCardEq ⋯).symm
hmt_eq : ∀ (x y : Fin (Fintype.card α - 1) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x' : Fin (Fintype.card α - 1) ↪ α := Function.Embedding.trans j✝ x
g : ↥G
hg' : g • x' = k • x'
hx : ∀ (x : Fin (Fintype.card α) ↪ α), Function.Surjective x.toFun
hgk' : ∀ (i : Fin (Fintype.card α)), ↑i < Fintype.card α - 1 → (g • x) i = (k • x) i
i : Fin (Fintype.card α)
hi : ↑i = Fintype.card α - 1
j : Fin (Fintype.card α)
hxj : (k • x) j = (g • x) i
hj : ↑j < Fintype.card α - 1
⊢ False

State before:
case inr.intro.inl
M : Type ?u.248388
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j✝ : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := (Fin.castLEEmb ⋯).toEmbedding
k : Equiv.Perm α
a✝ : k ∈ ⊤
x : Fin (Fintype.card α) ↪ α := Equiv.toEmbedding (Fintype.equivFinOfCardEq ⋯).symm
hmt_eq : ∀ (x y : Fin (Fintype.card α - 1) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x' : Fin (Fintype.card α - 1) ↪ α := Function.Embedding.trans j✝ x
g : ↥G
hg' : g • x' = k • x'
hx : ∀ (x : Fin (Fintype.card α) ↪ α), Function.Surjective x.toFun
hgk' : ∀ (i : Fin (Fintype.card α)), ↑i < Fintype.card α - 1 → (g • x) i = (k • x) i
i : Fin (Fintype.card α)
hi : ↑i = Fintype.card α - 1
j : Fin (Fintype.card α)
hxj : (k • x) j = (g • x) i
hj : ↑j < Fintype.card α - 1
⊢ False
Tactic:
suffices i = j by rw [← this, ← hi] at hj ; refine' lt_irrefl _ hj
State after:
case inr.intro.inl
M : Type ?u.248388
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j✝ : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := (Fin.castLEEmb ⋯).toEmbedding
k : Equiv.Perm α
a✝ : k ∈ ⊤
x : Fin (Fintype.card α) ↪ α := Equiv.toEmbedding (Fintype.equivFinOfCardEq ⋯).symm
hmt_eq : ∀ (x y : Fin (Fintype.card α - 1) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x' : Fin (Fintype.card α - 1) ↪ α := Function.Embedding.trans j✝ x
g : ↥G
hg' : g • x' = k • x'
hx : ∀ (x : Fin (Fintype.card α) ↪ α), Function.Surjective x.toFun
hgk' : ∀ (i : Fin (Fintype.card α)), ↑i < Fintype.card α - 1 → (g • x) i = (k • x) i
i : Fin (Fintype.card α)
hi : ↑i = Fintype.card α - 1
j : Fin (Fintype.card α)
hxj : (k • x) j = (g • x) i
hj : ↑j < Fintype.card α - 1
⊢ i = j

State before:
case inr.intro.inl
M : Type ?u.248388
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j✝ : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := (Fin.castLEEmb ⋯).toEmbedding
k : Equiv.Perm α
a✝ : k ∈ ⊤
x : Fin (Fintype.card α) ↪ α := Equiv.toEmbedding (Fintype.equivFinOfCardEq ⋯).symm
hmt_eq : ∀ (x y : Fin (Fintype.card α - 1) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x' : Fin (Fintype.card α - 1) ↪ α := Function.Embedding.trans j✝ x
g : ↥G
hg' : g • x' = k • x'
hx : ∀ (x : Fin (Fintype.card α) ↪ α), Function.Surjective x.toFun
hgk' : ∀ (i : Fin (Fintype.card α)), ↑i < Fintype.card α - 1 → (g • x) i = (k • x) i
i : Fin (Fintype.card α)
hi : ↑i = Fintype.card α - 1
j : Fin (Fintype.card α)
hxj : (k • x) j = (g • x) i
hj : ↑j < Fintype.card α - 1
⊢ i = j
Tactic:
apply EmbeddingLike.injective (g • x)
State after:
case inr.intro.inl.a
M : Type ?u.248388
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j✝ : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := (Fin.castLEEmb ⋯).toEmbedding
k : Equiv.Perm α
a✝ : k ∈ ⊤
x : Fin (Fintype.card α) ↪ α := Equiv.toEmbedding (Fintype.equivFinOfCardEq ⋯).symm
hmt_eq : ∀ (x y : Fin (Fintype.card α - 1) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x' : Fin (Fintype.card α - 1) ↪ α := Function.Embedding.trans j✝ x
g : ↥G
hg' : g • x' = k • x'
hx : ∀ (x : Fin (Fintype.card α) ↪ α), Function.Surjective x.toFun
hgk' : ∀ (i : Fin (Fintype.card α)), ↑i < Fintype.card α - 1 → (g • x) i = (k • x) i
i : Fin (Fintype.card α)
hi : ↑i = Fintype.card α - 1
j : Fin (Fintype.card α)
hxj : (k • x) j = (g • x) i
hj : ↑j < Fintype.card α - 1
⊢ (g • x) i = (g • x) j

State before:
case inr.intro.inl.a
M : Type ?u.248388
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j✝ : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := (Fin.castLEEmb ⋯).toEmbedding
k : Equiv.Perm α
a✝ : k ∈ ⊤
x : Fin (Fintype.card α) ↪ α := Equiv.toEmbedding (Fintype.equivFinOfCardEq ⋯).symm
hmt_eq : ∀ (x y : Fin (Fintype.card α - 1) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x' : Fin (Fintype.card α - 1) ↪ α := Function.Embedding.trans j✝ x
g : ↥G
hg' : g • x' = k • x'
hx : ∀ (x : Fin (Fintype.card α) ↪ α), Function.Surjective x.toFun
hgk' : ∀ (i : Fin (Fintype.card α)), ↑i < Fintype.card α - 1 → (g • x) i = (k • x) i
i : Fin (Fintype.card α)
hi : ↑i = Fintype.card α - 1
j : Fin (Fintype.card α)
hxj : (k • x) j = (g • x) i
hj : ↑j < Fintype.card α - 1
⊢ (g • x) i = (g • x) j
Tactic:
rw [hgk' j hj]
State after:
case inr.intro.inl.a
M : Type ?u.248388
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j✝ : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := (Fin.castLEEmb ⋯).toEmbedding
k : Equiv.Perm α
a✝ : k ∈ ⊤
x : Fin (Fintype.card α) ↪ α := Equiv.toEmbedding (Fintype.equivFinOfCardEq ⋯).symm
hmt_eq : ∀ (x y : Fin (Fintype.card α - 1) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x' : Fin (Fintype.card α - 1) ↪ α := Function.Embedding.trans j✝ x
g : ↥G
hg' : g • x' = k • x'
hx : ∀ (x : Fin (Fintype.card α) ↪ α), Function.Surjective x.toFun
hgk' : ∀ (i : Fin (Fintype.card α)), ↑i < Fintype.card α - 1 → (g • x) i = (k • x) i
i : Fin (Fintype.card α)
hi : ↑i = Fintype.card α - 1
j : Fin (Fintype.card α)
hxj : (k • x) j = (g • x) i
hj : ↑j < Fintype.card α - 1
⊢ (g • x) i = (k • x) j

State before:
case inr.intro.inl.a
M : Type ?u.248388
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j✝ : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := (Fin.castLEEmb ⋯).toEmbedding
k : Equiv.Perm α
a✝ : k ∈ ⊤
x : Fin (Fintype.card α) ↪ α := Equiv.toEmbedding (Fintype.equivFinOfCardEq ⋯).symm
hmt_eq : ∀ (x y : Fin (Fintype.card α - 1) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x' : Fin (Fintype.card α - 1) ↪ α := Function.Embedding.trans j✝ x
g : ↥G
hg' : g • x' = k • x'
hx : ∀ (x : Fin (Fintype.card α) ↪ α), Function.Surjective x.toFun
hgk' : ∀ (i : Fin (Fintype.card α)), ↑i < Fintype.card α - 1 → (g • x) i = (k • x) i
i : Fin (Fintype.card α)
hi : ↑i = Fintype.card α - 1
j : Fin (Fintype.card α)
hxj : (k • x) j = (g • x) i
hj : ↑j < Fintype.card α - 1
⊢ (g • x) i = (k • x) j
Tactic:
rw [hxj]
State after:
no goals

State before:
M : Type ?u.248388
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j✝ : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := (Fin.castLEEmb ⋯).toEmbedding
k : Equiv.Perm α
a✝ : k ∈ ⊤
x : Fin (Fintype.card α) ↪ α := Equiv.toEmbedding (Fintype.equivFinOfCardEq ⋯).symm
hmt_eq : ∀ (x y : Fin (Fintype.card α - 1) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x' : Fin (Fintype.card α - 1) ↪ α := Function.Embedding.trans j✝ x
g : ↥G
hg' : g • x' = k • x'
hx : ∀ (x : Fin (Fintype.card α) ↪ α), Function.Surjective x.toFun
hgk' : ∀ (i : Fin (Fintype.card α)), ↑i < Fintype.card α - 1 → (g • x) i = (k • x) i
i : Fin (Fintype.card α)
hi : ↑i = Fintype.card α - 1
j : Fin (Fintype.card α)
hxj : (k • x) j = (g • x) i
hj : ↑j < Fintype.card α - 1
this : i = j
⊢ False
Tactic:
rw [← this, ← hi] at hj
State after:
M : Type ?u.248388
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j✝ : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := (Fin.castLEEmb ⋯).toEmbedding
k : Equiv.Perm α
a✝ : k ∈ ⊤
x : Fin (Fintype.card α) ↪ α := Equiv.toEmbedding (Fintype.equivFinOfCardEq ⋯).symm
hmt_eq : ∀ (x y : Fin (Fintype.card α - 1) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x' : Fin (Fintype.card α - 1) ↪ α := Function.Embedding.trans j✝ x
g : ↥G
hg' : g • x' = k • x'
hx : ∀ (x : Fin (Fintype.card α) ↪ α), Function.Surjective x.toFun
hgk' : ∀ (i : Fin (Fintype.card α)), ↑i < Fintype.card α - 1 → (g • x) i = (k • x) i
i : Fin (Fintype.card α)
hi : ↑i = Fintype.card α - 1
j : Fin (Fintype.card α)
hxj : (k • x) j = (g • x) i
hj : ↑i < ↑i
this : i = j
⊢ False

State before:
M : Type ?u.248388
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j✝ : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := (Fin.castLEEmb ⋯).toEmbedding
k : Equiv.Perm α
a✝ : k ∈ ⊤
x : Fin (Fintype.card α) ↪ α := Equiv.toEmbedding (Fintype.equivFinOfCardEq ⋯).symm
hmt_eq : ∀ (x y : Fin (Fintype.card α - 1) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x' : Fin (Fintype.card α - 1) ↪ α := Function.Embedding.trans j✝ x
g : ↥G
hg' : g • x' = k • x'
hx : ∀ (x : Fin (Fintype.card α) ↪ α), Function.Surjective x.toFun
hgk' : ∀ (i : Fin (Fintype.card α)), ↑i < Fintype.card α - 1 → (g • x) i = (k • x) i
i : Fin (Fintype.card α)
hi : ↑i = Fintype.card α - 1
j : Fin (Fintype.card α)
hxj : (k • x) j = (g • x) i
hj : ↑i < ↑i
this : i = j
⊢ False
Tactic:
refine' lt_irrefl _ hj
State after:
no goals

State before:
case inr.intro.inr
M : Type ?u.248388
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j✝ : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := (Fin.castLEEmb ⋯).toEmbedding
k : Equiv.Perm α
a✝ : k ∈ ⊤
x : Fin (Fintype.card α) ↪ α := Equiv.toEmbedding (Fintype.equivFinOfCardEq ⋯).symm
hmt_eq : ∀ (x y : Fin (Fintype.card α - 1) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x' : Fin (Fintype.card α - 1) ↪ α := Function.Embedding.trans j✝ x
g : ↥G
hg' : g • x' = k • x'
hx : ∀ (x : Fin (Fintype.card α) ↪ α), Function.Surjective x.toFun
hgk' : ∀ (i : Fin (Fintype.card α)), ↑i < Fintype.card α - 1 → (g • x) i = (k • x) i
i : Fin (Fintype.card α)
hi : ↑i = Fintype.card α - 1
j : Fin (Fintype.card α)
hxj : (k • x) j = (g • x) i
hj : ↑j = Fintype.card α - 1
⊢ (g • x) i = (k • x) i
Tactic:
rw [← hxj]
State after:
case inr.intro.inr
M : Type ?u.248388
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j✝ : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := (Fin.castLEEmb ⋯).toEmbedding
k : Equiv.Perm α
a✝ : k ∈ ⊤
x : Fin (Fintype.card α) ↪ α := Equiv.toEmbedding (Fintype.equivFinOfCardEq ⋯).symm
hmt_eq : ∀ (x y : Fin (Fintype.card α - 1) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x' : Fin (Fintype.card α - 1) ↪ α := Function.Embedding.trans j✝ x
g : ↥G
hg' : g • x' = k • x'
hx : ∀ (x : Fin (Fintype.card α) ↪ α), Function.Surjective x.toFun
hgk' : ∀ (i : Fin (Fintype.card α)), ↑i < Fintype.card α - 1 → (g • x) i = (k • x) i
i : Fin (Fintype.card α)
hi : ↑i = Fintype.card α - 1
j : Fin (Fintype.card α)
hxj : (k • x) j = (g • x) i
hj : ↑j = Fintype.card α - 1
⊢ (k • x) j = (k • x) i

State before:
case inr.intro.inr
M : Type ?u.248388
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j✝ : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := (Fin.castLEEmb ⋯).toEmbedding
k : Equiv.Perm α
a✝ : k ∈ ⊤
x : Fin (Fintype.card α) ↪ α := Equiv.toEmbedding (Fintype.equivFinOfCardEq ⋯).symm
hmt_eq : ∀ (x y : Fin (Fintype.card α - 1) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x' : Fin (Fintype.card α - 1) ↪ α := Function.Embedding.trans j✝ x
g : ↥G
hg' : g • x' = k • x'
hx : ∀ (x : Fin (Fintype.card α) ↪ α), Function.Surjective x.toFun
hgk' : ∀ (i : Fin (Fintype.card α)), ↑i < Fintype.card α - 1 → (g • x) i = (k • x) i
i : Fin (Fintype.card α)
hi : ↑i = Fintype.card α - 1
j : Fin (Fintype.card α)
hxj : (k • x) j = (g • x) i
hj : ↑j = Fintype.card α - 1
⊢ (k • x) j = (k • x) i
Tactic:
apply congr_arg
State after:
case inr.intro.inr.h
M : Type ?u.248388
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j✝ : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := (Fin.castLEEmb ⋯).toEmbedding
k : Equiv.Perm α
a✝ : k ∈ ⊤
x : Fin (Fintype.card α) ↪ α := Equiv.toEmbedding (Fintype.equivFinOfCardEq ⋯).symm
hmt_eq : ∀ (x y : Fin (Fintype.card α - 1) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x' : Fin (Fintype.card α - 1) ↪ α := Function.Embedding.trans j✝ x
g : ↥G
hg' : g • x' = k • x'
hx : ∀ (x : Fin (Fintype.card α) ↪ α), Function.Surjective x.toFun
hgk' : ∀ (i : Fin (Fintype.card α)), ↑i < Fintype.card α - 1 → (g • x) i = (k • x) i
i : Fin (Fintype.card α)
hi : ↑i = Fintype.card α - 1
j : Fin (Fintype.card α)
hxj : (k • x) j = (g • x) i
hj : ↑j = Fintype.card α - 1
⊢ j = i

State before:
case inr.intro.inr.h
M : Type ?u.248388
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j✝ : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := (Fin.castLEEmb ⋯).toEmbedding
k : Equiv.Perm α
a✝ : k ∈ ⊤
x : Fin (Fintype.card α) ↪ α := Equiv.toEmbedding (Fintype.equivFinOfCardEq ⋯).symm
hmt_eq : ∀ (x y : Fin (Fintype.card α - 1) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x' : Fin (Fintype.card α - 1) ↪ α := Function.Embedding.trans j✝ x
g : ↥G
hg' : g • x' = k • x'
hx : ∀ (x : Fin (Fintype.card α) ↪ α), Function.Surjective x.toFun
hgk' : ∀ (i : Fin (Fintype.card α)), ↑i < Fintype.card α - 1 → (g • x) i = (k • x) i
i : Fin (Fintype.card α)
hi : ↑i = Fintype.card α - 1
j : Fin (Fintype.card α)
hxj : (k • x) j = (g • x) i
hj : ↑j = Fintype.card α - 1
⊢ j = i
Tactic:
rw [Fin.ext_iff, hi, hj]
State after:
no goals