internlm/Lean-Github huggingface dataset:
Theorem: MulAction.IsMultiplyPretransitive.eq_top_of_is_full_minus_one_pretransitive
Proof 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
Proof 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)
Theorem: MulAction.IsMultiplyPretransitive.eq_top_of_is_full_minus_one_pretransitive
Proof 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]
Proof 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)
Theorem: MulAction.IsMultiplyPretransitive.eq_top_of_is_full_minus_one_pretransitive
Proof 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]
Proof 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)
Theorem: MulAction.IsMultiplyPretransitive.eq_top_of_is_full_minus_one_pretransitive
Proof 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
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'
this : k = ↑g
⊢ k ∈ G
Tactic:
rw [this]
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'
this : k = ↑g
⊢ ↑g ∈ G
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'
this : k = ↑g
⊢ ↑g ∈ G
Tactic:
exact SetLike.coe_mem g
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'
⊢ ∀ (x : Fin (Fintype.card α) ↪ α), Function.Surjective x.toFun
Tactic:
intro x
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'
x : Fin (Fintype.card α) ↪ α
⊢ Function.Surjective x.toFun
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'
x : Fin (Fintype.card α) ↪ α
⊢ Function.Surjective x.toFun
Tactic:
apply Function.Bijective.surjective
Proof 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
Theorem: MulAction.IsMultiplyPretransitive.eq_top_of_is_full_minus_one_pretransitive
Proof 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]
Proof 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 α
Theorem: MulAction.IsMultiplyPretransitive.eq_top_of_is_full_minus_one_pretransitive
Proof 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 α)⟩
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
⊢ ∀ (i : Fin (Fintype.card α)), ↑i < Fintype.card α - 1 → (g • x) i = (k • x) i
Tactic:
intro i hi
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
i : Fin (Fintype.card α)
hi : ↑i < Fintype.card α - 1
⊢ (g • x) i = (k • x) i
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
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⟩
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 α)), (g • x) i = (k • x) i
Tactic:
intro i
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 α)
⊢ (g • x) i = (k • x) i
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 α)
⊢ (g • x) i = (k • x) i
Tactic:
cases' aux_lt_iff_lt_or_eq i.prop with hi hi
Proof 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
Theorem: MulAction.IsMultiplyPretransitive.eq_top_of_is_full_minus_one_pretransitive
Proof 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
Proof state after:
no goals
Theorem: MulAction.IsMultiplyPretransitive.eq_top_of_is_full_minus_one_pretransitive
Proof 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)
Proof 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