internlm/Lean-Github huggingface dataset:
Theorem: Equiv.Perm.isPreprimitive
Proof state before:
case inr
M : Type ?u.243758
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
h✝ : Nontrivial α
⊢ IsPreprimitive (Equiv.Perm α) α
Tactic:
apply IsMultiplyPretransitive.isPreprimitive_of_two
Proof state after:
case inr.h2
M : Type ?u.243758
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
h✝ : Nontrivial α
⊢ IsMultiplyPretransitive (Equiv.Perm α) α 2
Theorem: Equiv.Perm.isPreprimitive
Proof state before:
case inr.h2
M : Type ?u.243758
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
h✝ : Nontrivial α
⊢ IsMultiplyPretransitive (Equiv.Perm α) α 2
Tactic:
apply Equiv.Perm.isMultiplyPretransitive
Proof state after:
no goals
Theorem: Equiv.Perm.isPreprimitive
Proof state before:
case inl
M : Type ?u.243758
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
h✝ : Subsingleton α
⊢ IsPreprimitive (Equiv.Perm α) α
Tactic:
exact IsPreprimitive.on_subsingleton
Proof state after:
no goals
Theorem: MulAction.aux_lt_iff_lt_or_eq
Proof state before:
M : Type ?u.247599
α : Type ?u.247602
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
m n : ℕ
hmn : m < n
⊢ m < n - 1 ∨ m = n - 1
Tactic:
rw [Nat.lt_iff_le_not_le]
Proof state after:
M : Type ?u.247599
α : Type ?u.247602
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
m n : ℕ
hmn : m < n
⊢ m ≤ n - 1 ∧ ¬n - 1 ≤ m ∨ m = n - 1
Theorem: MulAction.aux_lt_iff_lt_or_eq
Proof state before:
M : Type ?u.247599
α : Type ?u.247602
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
m n : ℕ
hmn : m < n
⊢ m ≤ n - 1 ∧ ¬n - 1 ≤ m ∨ m = n - 1
Tactic:
cases' dec_em (m = n - 1) with h h'
Proof state after:
case inl
M : Type ?u.247599
α : Type ?u.247602
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
m n : ℕ
hmn : m < n
h : m = n - 1
⊢ m ≤ n - 1 ∧ ¬n - 1 ≤ m ∨ m = n - 1

case inr
M : Type ?u.247599
α : Type ?u.247602
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
m n : ℕ
hmn : m < n
h' : ¬m = n - 1
⊢ m ≤ n - 1 ∧ ¬n - 1 ≤ m ∨ m = n - 1
Theorem: MulAction.aux_lt_iff_lt_or_eq
Proof state before:
case inl
M : Type ?u.247599
α : Type ?u.247602
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
m n : ℕ
hmn : m < n
h : m = n - 1
⊢ m ≤ n - 1 ∧ ¬n - 1 ≤ m ∨ m = n - 1
Tactic:
exact Or.intro_right _ h
Proof state after:
no goals
Theorem: MulAction.aux_lt_iff_lt_or_eq
Proof state before:
case inr
M : Type ?u.247599
α : Type ?u.247602
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
m n : ℕ
hmn : m < n
h' : ¬m = n - 1
⊢ m ≤ n - 1 ∧ ¬n - 1 ≤ m ∨ m = n - 1
Tactic:
apply Or.intro_left
Proof state after:
case inr.h
M : Type ?u.247599
α : Type ?u.247602
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
m n : ℕ
hmn : m < n
h' : ¬m = n - 1
⊢ m ≤ n - 1 ∧ ¬n - 1 ≤ m
Theorem: MulAction.aux_lt_iff_lt_or_eq
Proof state before:
case inr.h
M : Type ?u.247599
α : Type ?u.247602
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
m n : ℕ
hmn : m < n
h' : ¬m = n - 1
⊢ m ≤ n - 1 ∧ ¬n - 1 ≤ m
Tactic:
apply And.intro
Proof state after:
case inr.h.left
M : Type ?u.247599
α : Type ?u.247602
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
m n : ℕ
hmn : m < n
h' : ¬m = n - 1
⊢ m ≤ n - 1

case inr.h.right
M : Type ?u.247599
α : Type ?u.247602
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
m n : ℕ
hmn : m < n
h' : ¬m = n - 1
⊢ ¬n - 1 ≤ m
Theorem: MulAction.aux_lt_iff_lt_or_eq
Proof state before:
case inr.h.left
M : Type ?u.247599
α : Type ?u.247602
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
m n : ℕ
hmn : m < n
h' : ¬m = n - 1
⊢ m ≤ n - 1
Tactic:
exact Nat.le_pred_of_lt hmn
Proof state after:
no goals
Theorem: MulAction.aux_lt_iff_lt_or_eq
Proof state before:
case inr.h.right
M : Type ?u.247599
α : Type ?u.247602
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
m n : ℕ
hmn : m < n
h' : ¬m = n - 1
⊢ ¬n - 1 ≤ m
Tactic:
intro h
Proof state after:
case inr.h.right
M : Type ?u.247599
α : Type ?u.247602
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
m n : ℕ
hmn : m < n
h' : ¬m = n - 1
h : n - 1 ≤ m
⊢ False
Theorem: MulAction.aux_lt_iff_lt_or_eq
Proof state before:
case inr.h.right
M : Type ?u.247599
α : Type ?u.247602
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
m n : ℕ
hmn : m < n
h' : ¬m = n - 1
h : n - 1 ≤ m
⊢ False
Tactic:
apply h'
Proof state after:
case inr.h.right
M : Type ?u.247599
α : Type ?u.247602
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
m n : ℕ
hmn : m < n
h' : ¬m = n - 1
h : n - 1 ≤ m
⊢ m = n - 1
Theorem: MulAction.aux_lt_iff_lt_or_eq
Proof state before:
case inr.h.right
M : Type ?u.247599
α : Type ?u.247602
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
m n : ℕ
hmn : m < n
h' : ¬m = n - 1
h : n - 1 ≤ m
⊢ m = n - 1
Tactic:
exact Nat.le_antisymm (Nat.le_pred_of_lt hmn) h
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)
⊢ G = ⊤
Tactic:
let j : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) :=
  (Fin.castLEEmb ((Fintype.card α).sub_le 1)).toEmbedding
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
⊢ 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
⊢ G = ⊤
Tactic:
rw [eq_top_iff]
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
⊢ ⊤ ≤ 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
⊢ ⊤ ≤ G
Tactic:
intro k _
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 ∈ ⊤
⊢ k ∈ 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 ∈ ⊤
⊢ k ∈ G
Tactic:
let x : Fin (Fintype.card α) ↪ α := (Fintype.equivFinOfCardEq rfl).symm.toEmbedding
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
⊢ k ∈ 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
⊢ k ∈ G
Tactic:
let hmt_eq := hmt.exists_smul_eq
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
⊢ k ∈ 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
⊢ k ∈ G
Tactic:
let x' := j.trans 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
⊢ k ∈ 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
⊢ k ∈ G
Tactic:
obtain ⟨g, hg'⟩ := hmt_eq x' (k • x')
Proof 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
Theorem: MulAction.IsMultiplyPretransitive.eq_top_of_is_full_minus_one_pretransitive
Proof 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
Proof 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
Theorem: MulAction.IsMultiplyPretransitive.eq_top_of_is_full_minus_one_pretransitive
Proof 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 α)⟩
Proof 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
Theorem: MulAction.IsMultiplyPretransitive.eq_top_of_is_full_minus_one_pretransitive
Proof 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⟩
Proof 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
Theorem: MulAction.IsMultiplyPretransitive.eq_top_of_is_full_minus_one_pretransitive
Proof 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
Proof 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
Theorem: MulAction.IsMultiplyPretransitive.eq_top_of_is_full_minus_one_pretransitive
Proof 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
Proof 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
Theorem: MulAction.IsMultiplyPretransitive.eq_top_of_is_full_minus_one_pretransitive
Proof 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
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 α)
⊢ 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 α)
⊢ k (x.toFun i) = ↑g (x.toFun i)
Tactic:
let zi := hgk i
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)