internlm/Lean-Github huggingface dataset:
Theorem: MulAction.IsMultiplyPretransitive.eq_top_of_is_full_minus_one_pretransitive
Proof 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
Proof 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
Theorem: MulAction.IsMultiplyPretransitive.eq_top_of_is_full_minus_one_pretransitive
Proof 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
Proof 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
Theorem: MulAction.IsMultiplyPretransitive.eq_top_of_is_full_minus_one_pretransitive
Proof 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
Proof 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
Theorem: MulAction.IsMultiplyPretransitive.eq_top_of_is_full_minus_one_pretransitive
Proof 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)
Proof 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
Theorem: MulAction.IsMultiplyPretransitive.eq_top_of_is_full_minus_one_pretransitive
Proof 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]
Proof 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
Theorem: MulAction.IsMultiplyPretransitive.eq_top_of_is_full_minus_one_pretransitive
Proof 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]
Proof state after:
no goals
Theorem: MulAction.IsMultiplyPretransitive.eq_top_of_is_full_minus_one_pretransitive
Proof 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
Proof 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
Theorem: MulAction.IsMultiplyPretransitive.eq_top_of_is_full_minus_one_pretransitive
Proof 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
Proof state after:
no goals
Theorem: MulAction.IsMultiplyPretransitive.eq_top_of_is_full_minus_one_pretransitive
Proof 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]
Proof 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
Theorem: MulAction.IsMultiplyPretransitive.eq_top_of_is_full_minus_one_pretransitive
Proof 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
Proof 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
Theorem: MulAction.IsMultiplyPretransitive.eq_top_of_is_full_minus_one_pretransitive
Proof 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]
Proof state after:
no goals
Theorem: MulAction.IsMultiplyPretransitive.alternatingGroup_of_sub_two
Proof state before:
M : Type ?u.254050
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ IsMultiplyPretransitive (↥(alternatingGroup α)) α (Fintype.card α - 2)
Tactic:
cases' lt_or_ge (Fintype.card α) 2 with h2 h2
Proof state after:
case inl
M : Type ?u.254050
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h2 : Fintype.card α < 2
⊢ IsMultiplyPretransitive (↥(alternatingGroup α)) α (Fintype.card α - 2)

case inr
M : Type ?u.254050
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h2 : Fintype.card α ≥ 2
⊢ IsMultiplyPretransitive (↥(alternatingGroup α)) α (Fintype.card α - 2)
Theorem: MulAction.IsMultiplyPretransitive.alternatingGroup_of_sub_two
Proof state before:
case inr
M : Type ?u.254050
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h2 : Fintype.card α ≥ 2
⊢ IsMultiplyPretransitive (↥(alternatingGroup α)) α (Fintype.card α - 2)
Tactic:
obtain ⟨n, hn⟩ := Nat.le.dest h2
Proof state after:
case inr.intro
M : Type ?u.254050
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h2 : Fintype.card α ≥ 2
n : ℕ
hn : 2 + n = Fintype.card α
⊢ IsMultiplyPretransitive (↥(alternatingGroup α)) α (Fintype.card α - 2)
Theorem: MulAction.IsMultiplyPretransitive.alternatingGroup_of_sub_two
Proof state before:
case inr.intro
M : Type ?u.254050
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h2 : Fintype.card α ≥ 2
n : ℕ
hn : 2 + n = Fintype.card α
⊢ IsMultiplyPretransitive (↥(alternatingGroup α)) α (Fintype.card α - 2)
Tactic:
have hn' : Fintype.card α - 2 = n := tsub_eq_of_eq_add_rev hn.symm
Proof state after:
case inr.intro
M : Type ?u.254050
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h2 : Fintype.card α ≥ 2
n : ℕ
hn : 2 + n = Fintype.card α
hn' : Fintype.card α - 2 = n
⊢ IsMultiplyPretransitive (↥(alternatingGroup α)) α (Fintype.card α - 2)
Theorem: MulAction.IsMultiplyPretransitive.alternatingGroup_of_sub_two
Proof state before:
case inr.intro
M : Type ?u.254050
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h2 : Fintype.card α ≥ 2
n : ℕ
hn : 2 + n = Fintype.card α
hn' : Fintype.card α - 2 = n
⊢ IsMultiplyPretransitive (↥(alternatingGroup α)) α (Fintype.card α - 2)
Tactic:
rw [add_comm] at hn
Proof state after:
case inr.intro
M : Type ?u.254050
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h2 : Fintype.card α ≥ 2
n : ℕ
hn : n + 2 = Fintype.card α
hn' : Fintype.card α - 2 = n
⊢ IsMultiplyPretransitive (↥(alternatingGroup α)) α (Fintype.card α - 2)
Theorem: MulAction.IsMultiplyPretransitive.alternatingGroup_of_sub_two
Proof state before:
case inr.intro
M : Type ?u.254050
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h2 : Fintype.card α ≥ 2
n : ℕ
hn : n + 2 = Fintype.card α
hn' : Fintype.card α - 2 = n
⊢ IsMultiplyPretransitive (↥(alternatingGroup α)) α (Fintype.card α - 2)
Tactic:
have hn_le : n ≤ Fintype.card α := by rw [← hn]; exact le_self_add
Proof state after:
case inr.intro
M : Type ?u.254050
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h2 : Fintype.card α ≥ 2
n : ℕ
hn : n + 2 = Fintype.card α
hn' : Fintype.card α - 2 = n
hn_le : n ≤ Fintype.card α
⊢ IsMultiplyPretransitive (↥(alternatingGroup α)) α (Fintype.card α - 2)
Theorem: MulAction.IsMultiplyPretransitive.alternatingGroup_of_sub_two
Proof state before:
case inr.intro
M : Type ?u.254050
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h2 : Fintype.card α ≥ 2
n : ℕ
hn : n + 2 = Fintype.card α
hn' : Fintype.card α - 2 = n
hn_le : n ≤ Fintype.card α
⊢ IsMultiplyPretransitive (↥(alternatingGroup α)) α (Fintype.card α - 2)
Tactic:
apply IsPretransitive.mk
Proof state after:
case inr.intro.exists_smul_eq
M : Type ?u.254050
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h2 : Fintype.card α ≥ 2
n : ℕ
hn : n + 2 = Fintype.card α
hn' : Fintype.card α - 2 = n
hn_le : n ≤ Fintype.card α
⊢ ∀ (x y : Fin (Fintype.card α - 2) ↪ α), ∃ g, g • x = y