internlm/Lean-Github huggingface dataset:
Theorem: MulAction.IsMultiplyPretransitive.alternatingGroup_of_sub_two
Proof state before:
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
Tactic:
rw [hn']
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 n ↪ α), ∃ g, g • x = y
Theorem: MulAction.IsMultiplyPretransitive.alternatingGroup_of_sub_two
Proof state before:
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 n ↪ α), ∃ g, g • x = y
Tactic:
intro x y
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 n ↪ α
⊢ ∃ g, g • x = y
Theorem: MulAction.IsMultiplyPretransitive.alternatingGroup_of_sub_two
Proof state before:
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 n ↪ α
⊢ ∃ g, g • x = y
Tactic:
obtain ⟨x', hx'⟩ := may_extend hn_le (le_of_eq PartENat.card_eq_coe_fintype_card.symm) x
Proof state after:
case inr.intro.exists_smul_eq.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 α
x y : Fin n ↪ α
x' : Fin (Fintype.card α) ↪ α
hx' : Function.Embedding.trans (Fin.castLEEmb hn_le).toEmbedding x' = x
⊢ ∃ g, g • x = y
Theorem: MulAction.IsMultiplyPretransitive.alternatingGroup_of_sub_two
Proof state before:
case inr.intro.exists_smul_eq.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 α
x y : Fin n ↪ α
x' : Fin (Fintype.card α) ↪ α
hx' : Function.Embedding.trans (Fin.castLEEmb hn_le).toEmbedding x' = x
⊢ ∃ g, g • x = y
Tactic:
obtain ⟨y', hy'⟩ := may_extend hn_le (le_of_eq PartENat.card_eq_coe_fintype_card.symm) y
Proof state after:
case inr.intro.exists_smul_eq.intro.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 α
x y : Fin n ↪ α
x' : Fin (Fintype.card α) ↪ α
hx' : Function.Embedding.trans (Fin.castLEEmb hn_le).toEmbedding x' = x
y' : Fin (Fintype.card α) ↪ α
hy' : Function.Embedding.trans (Fin.castLEEmb hn_le).toEmbedding y' = y
⊢ ∃ g, g • x = y
Theorem: MulAction.IsMultiplyPretransitive.alternatingGroup_of_sub_two
Proof state before:
case inr.intro.exists_smul_eq.intro.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 α
x y : Fin n ↪ α
x' : Fin (Fintype.card α) ↪ α
hx' : Function.Embedding.trans (Fin.castLEEmb hn_le).toEmbedding x' = x
y' : Fin (Fintype.card α) ↪ α
hy' : Function.Embedding.trans (Fin.castLEEmb hn_le).toEmbedding y' = y
⊢ ∃ g, g • x = y
Tactic:
let heq := (Equiv.Perm.isMultiplyPretransitive α (Fintype.card α)).exists_smul_eq
Proof state after:
case inr.intro.exists_smul_eq.intro.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 α
x y : Fin n ↪ α
x' : Fin (Fintype.card α) ↪ α
hx' : Function.Embedding.trans (Fin.castLEEmb hn_le).toEmbedding x' = x
y' : Fin (Fintype.card α) ↪ α
hy' : Function.Embedding.trans (Fin.castLEEmb hn_le).toEmbedding y' = y
heq : ∀ (x y : Fin (Fintype.card α) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
⊢ ∃ g, g • x = y
Theorem: MulAction.IsMultiplyPretransitive.alternatingGroup_of_sub_two
Proof state before:
case inr.intro.exists_smul_eq.intro.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 α
x y : Fin n ↪ α
x' : Fin (Fintype.card α) ↪ α
hx' : Function.Embedding.trans (Fin.castLEEmb hn_le).toEmbedding x' = x
y' : Fin (Fintype.card α) ↪ α
hy' : Function.Embedding.trans (Fin.castLEEmb hn_le).toEmbedding y' = y
heq : ∀ (x y : Fin (Fintype.card α) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
⊢ ∃ g, g • x = y
Tactic:
obtain ⟨g, hg⟩ := heq x' y'
Proof state after:
case inr.intro.exists_smul_eq.intro.intro.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 α
x y : Fin n ↪ α
x' : Fin (Fintype.card α) ↪ α
hx' : Function.Embedding.trans (Fin.castLEEmb hn_le).toEmbedding x' = x
y' : Fin (Fintype.card α) ↪ α
hy' : Function.Embedding.trans (Fin.castLEEmb hn_le).toEmbedding y' = y
heq : ∀ (x y : Fin (Fintype.card α) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
g : Equiv.Perm α
hg : g • x' = y'
⊢ ∃ g, g • x = y
Theorem: MulAction.IsMultiplyPretransitive.alternatingGroup_of_sub_two
Proof state before:
case inr.intro.exists_smul_eq.intro.intro.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 α
x y : Fin n ↪ α
x' : Fin (Fintype.card α) ↪ α
hx' : Function.Embedding.trans (Fin.castLEEmb hn_le).toEmbedding x' = x
y' : Fin (Fintype.card α) ↪ α
hy' : Function.Embedding.trans (Fin.castLEEmb hn_le).toEmbedding y' = y
heq : ∀ (x y : Fin (Fintype.card α) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
g : Equiv.Perm α
hg : g • x' = y'
⊢ ∃ g, g • x = y
Tactic:
cases' Int.units_eq_one_or (Equiv.Perm.sign g) with h h
Proof state after:
case inr.intro.exists_smul_eq.intro.intro.intro.inl
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 n ↪ α
x' : Fin (Fintype.card α) ↪ α
hx' : Function.Embedding.trans (Fin.castLEEmb hn_le).toEmbedding x' = x
y' : Fin (Fintype.card α) ↪ α
hy' : Function.Embedding.trans (Fin.castLEEmb hn_le).toEmbedding y' = y
heq : ∀ (x y : Fin (Fintype.card α) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
g : Equiv.Perm α
hg : g • x' = y'
h : Equiv.Perm.sign g = 1
⊢ ∃ g, g • x = y

case inr.intro.exists_smul_eq.intro.intro.intro.inr
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 n ↪ α
x' : Fin (Fintype.card α) ↪ α
hx' : Function.Embedding.trans (Fin.castLEEmb hn_le).toEmbedding x' = x
y' : Fin (Fintype.card α) ↪ α
hy' : Function.Embedding.trans (Fin.castLEEmb hn_le).toEmbedding y' = y
heq : ∀ (x y : Fin (Fintype.card α) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
g : Equiv.Perm α
hg : g • x' = y'
h : Equiv.Perm.sign g = -1
⊢ ∃ g, g • x = y
Theorem: MulAction.IsMultiplyPretransitive.alternatingGroup_of_sub_two
Proof state before:
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)
Tactic:
rw [Nat.sub_eq_zero_of_le (le_of_lt 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 α)) α 0
Theorem: MulAction.IsMultiplyPretransitive.alternatingGroup_of_sub_two
Proof state before:
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 α)) α 0
Tactic:
apply is_zero_pretransitive
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 α
h2 : Fintype.card α ≥ 2
n : ℕ
hn : n + 2 = Fintype.card α
hn' : Fintype.card α - 2 = n
⊢ n ≤ Fintype.card α
Tactic:
rw [← hn]
Proof state after:
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
⊢ n ≤ n + 2
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 α
h2 : Fintype.card α ≥ 2
n : ℕ
hn : n + 2 = Fintype.card α
hn' : Fintype.card α - 2 = n
⊢ n ≤ n + 2
Tactic:
exact le_self_add
Proof state after:
no goals
Theorem: MulAction.IsMultiplyPretransitive.alternatingGroup_of_sub_two
Proof state before:
case inr.intro.exists_smul_eq.intro.intro.intro.inl
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 n ↪ α
x' : Fin (Fintype.card α) ↪ α
hx' : Function.Embedding.trans (Fin.castLEEmb hn_le).toEmbedding x' = x
y' : Fin (Fintype.card α) ↪ α
hy' : Function.Embedding.trans (Fin.castLEEmb hn_le).toEmbedding y' = y
heq : ∀ (x y : Fin (Fintype.card α) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
g : Equiv.Perm α
hg : g • x' = y'
h : Equiv.Perm.sign g = 1
⊢ ∃ g, g • x = y
Tactic:
use ⟨g, Equiv.Perm.mem_alternatingGroup.mpr h⟩
Proof state after:
case h
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 n ↪ α
x' : Fin (Fintype.card α) ↪ α
hx' : Function.Embedding.trans (Fin.castLEEmb hn_le).toEmbedding x' = x
y' : Fin (Fintype.card α) ↪ α
hy' : Function.Embedding.trans (Fin.castLEEmb hn_le).toEmbedding y' = y
heq : ∀ (x y : Fin (Fintype.card α) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
g : Equiv.Perm α
hg : g • x' = y'
h : Equiv.Perm.sign g = 1
⊢ { val := g, property := ⋯ } • x = y
Theorem: MulAction.IsMultiplyPretransitive.alternatingGroup_of_sub_two
Proof state before:
case h
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 n ↪ α
x' : Fin (Fintype.card α) ↪ α
hx' : Function.Embedding.trans (Fin.castLEEmb hn_le).toEmbedding x' = x
y' : Fin (Fintype.card α) ↪ α
hy' : Function.Embedding.trans (Fin.castLEEmb hn_le).toEmbedding y' = y
heq : ∀ (x y : Fin (Fintype.card α) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
g : Equiv.Perm α
hg : g • x' = y'
h : Equiv.Perm.sign g = 1
⊢ { val := g, property := ⋯ } • x = y
Tactic:
ext i
Proof state after:
case h.h
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 n ↪ α
x' : Fin (Fintype.card α) ↪ α
hx' : Function.Embedding.trans (Fin.castLEEmb hn_le).toEmbedding x' = x
y' : Fin (Fintype.card α) ↪ α
hy' : Function.Embedding.trans (Fin.castLEEmb hn_le).toEmbedding y' = y
heq : ∀ (x y : Fin (Fintype.card α) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
g : Equiv.Perm α
hg : g • x' = y'
h : Equiv.Perm.sign g = 1
i : Fin n
⊢ ({ val := g, property := ⋯ } • x) i = y i
Theorem: MulAction.IsMultiplyPretransitive.alternatingGroup_of_sub_two
Proof state before:
case h.h
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 n ↪ α
x' : Fin (Fintype.card α) ↪ α
hx' : Function.Embedding.trans (Fin.castLEEmb hn_le).toEmbedding x' = x
y' : Fin (Fintype.card α) ↪ α
hy' : Function.Embedding.trans (Fin.castLEEmb hn_le).toEmbedding y' = y
heq : ∀ (x y : Fin (Fintype.card α) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
g : Equiv.Perm α
hg : g • x' = y'
h : Equiv.Perm.sign g = 1
i : Fin n
⊢ ({ val := g, property := ⋯ } • x) i = y i
Tactic:
simp only [Function.Embedding.smul_apply]
Proof state after:
case h.h
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 n ↪ α
x' : Fin (Fintype.card α) ↪ α
hx' : Function.Embedding.trans (Fin.castLEEmb hn_le).toEmbedding x' = x
y' : Fin (Fintype.card α) ↪ α
hy' : Function.Embedding.trans (Fin.castLEEmb hn_le).toEmbedding y' = y
heq : ∀ (x y : Fin (Fintype.card α) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
g : Equiv.Perm α
hg : g • x' = y'
h : Equiv.Perm.sign g = 1
i : Fin n
⊢ { val := g, property := ⋯ } • x i = y i
Theorem: MulAction.IsMultiplyPretransitive.alternatingGroup_of_sub_two
Proof state before:
case h.h
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 n ↪ α
x' : Fin (Fintype.card α) ↪ α
hx' : Function.Embedding.trans (Fin.castLEEmb hn_le).toEmbedding x' = x
y' : Fin (Fintype.card α) ↪ α
hy' : Function.Embedding.trans (Fin.castLEEmb hn_le).toEmbedding y' = y
heq : ∀ (x y : Fin (Fintype.card α) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
g : Equiv.Perm α
hg : g • x' = y'
h : Equiv.Perm.sign g = 1
i : Fin n
⊢ { val := g, property := ⋯ } • x i = y i
Tactic:
rw [← hx', ← hy', ← hg]
Proof state after:
case h.h
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 n ↪ α
x' : Fin (Fintype.card α) ↪ α
hx' : Function.Embedding.trans (Fin.castLEEmb hn_le).toEmbedding x' = x
y' : Fin (Fintype.card α) ↪ α
hy' : Function.Embedding.trans (Fin.castLEEmb hn_le).toEmbedding y' = y
heq : ∀ (x y : Fin (Fintype.card α) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
g : Equiv.Perm α
hg : g • x' = y'
h : Equiv.Perm.sign g = 1
i : Fin n
⊢ { val := g, property := ⋯ } • (Function.Embedding.trans (Fin.castLEEmb hn_le).toEmbedding x') i =
    (Function.Embedding.trans (Fin.castLEEmb hn_le).toEmbedding (g • x')) i
Theorem: MulAction.IsMultiplyPretransitive.alternatingGroup_of_sub_two
Proof state before:
case h.h
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 n ↪ α
x' : Fin (Fintype.card α) ↪ α
hx' : Function.Embedding.trans (Fin.castLEEmb hn_le).toEmbedding x' = x
y' : Fin (Fintype.card α) ↪ α
hy' : Function.Embedding.trans (Fin.castLEEmb hn_le).toEmbedding y' = y
heq : ∀ (x y : Fin (Fintype.card α) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
g : Equiv.Perm α
hg : g • x' = y'
h : Equiv.Perm.sign g = 1
i : Fin n
⊢ { val := g, property := ⋯ } • (Function.Embedding.trans (Fin.castLEEmb hn_le).toEmbedding x') i =
    (Function.Embedding.trans (Fin.castLEEmb hn_le).toEmbedding (g • x')) i
Tactic:
rfl
Proof state after:
no goals
Theorem: MulAction.IsMultiplyPretransitive.alternatingGroup_of_sub_two
Proof state before:
case inr.intro.exists_smul_eq.intro.intro.intro.inr
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 n ↪ α
x' : Fin (Fintype.card α) ↪ α
hx' : Function.Embedding.trans (Fin.castLEEmb hn_le).toEmbedding x' = x
y' : Fin (Fintype.card α) ↪ α
hy' : Function.Embedding.trans (Fin.castLEEmb hn_le).toEmbedding y' = y
heq : ∀ (x y : Fin (Fintype.card α) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
g : Equiv.Perm α
hg : g • x' = y'
h : Equiv.Perm.sign g = -1
⊢ ∃ g, g • x = y
Tactic:
have hg'1 : n + 1 < Fintype.card α := by
  rw [← hn]; exact Nat.lt.base (n + 1)
Proof state after:
case inr.intro.exists_smul_eq.intro.intro.intro.inr
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 n ↪ α
x' : Fin (Fintype.card α) ↪ α
hx' : Function.Embedding.trans (Fin.castLEEmb hn_le).toEmbedding x' = x
y' : Fin (Fintype.card α) ↪ α
hy' : Function.Embedding.trans (Fin.castLEEmb hn_le).toEmbedding y' = y
heq : ∀ (x y : Fin (Fintype.card α) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
g : Equiv.Perm α
hg : g • x' = y'
h : Equiv.Perm.sign g = -1
hg'1 : n + 1 < Fintype.card α
⊢ ∃ g, g • x = y
Theorem: MulAction.IsMultiplyPretransitive.alternatingGroup_of_sub_two
Proof state before:
case inr.intro.exists_smul_eq.intro.intro.intro.inr
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 n ↪ α
x' : Fin (Fintype.card α) ↪ α
hx' : Function.Embedding.trans (Fin.castLEEmb hn_le).toEmbedding x' = x
y' : Fin (Fintype.card α) ↪ α
hy' : Function.Embedding.trans (Fin.castLEEmb hn_le).toEmbedding y' = y
heq : ∀ (x y : Fin (Fintype.card α) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
g : Equiv.Perm α
hg : g • x' = y'
h : Equiv.Perm.sign g = -1
hg'1 : n + 1 < Fintype.card α
⊢ ∃ g, g • x = y
Tactic:
have hg'2 : n < Fintype.card α := by
    apply lt_trans _ hg'1; exact lt_add_one n
Proof state after:
case inr.intro.exists_smul_eq.intro.intro.intro.inr
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 n ↪ α
x' : Fin (Fintype.card α) ↪ α
hx' : Function.Embedding.trans (Fin.castLEEmb hn_le).toEmbedding x' = x
y' : Fin (Fintype.card α) ↪ α
hy' : Function.Embedding.trans (Fin.castLEEmb hn_le).toEmbedding y' = y
heq : ∀ (x y : Fin (Fintype.card α) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
g : Equiv.Perm α
hg : g • x' = y'
h : Equiv.Perm.sign g = -1
hg'1 : n + 1 < Fintype.card α
hg'2 : n < Fintype.card α
⊢ ∃ g, g • x = y
Theorem: MulAction.IsMultiplyPretransitive.alternatingGroup_of_sub_two
Proof state before:
case inr.intro.exists_smul_eq.intro.intro.intro.inr
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 n ↪ α
x' : Fin (Fintype.card α) ↪ α
hx' : Function.Embedding.trans (Fin.castLEEmb hn_le).toEmbedding x' = x
y' : Fin (Fintype.card α) ↪ α
hy' : Function.Embedding.trans (Fin.castLEEmb hn_le).toEmbedding y' = y
heq : ∀ (x y : Fin (Fintype.card α) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
g : Equiv.Perm α
hg : g • x' = y'
h : Equiv.Perm.sign g = -1
hg'1 : n + 1 < Fintype.card α
hg'2 : n < Fintype.card α
⊢ ∃ g, g • x = y
Tactic:
let g' := Equiv.swap (y'.toFun ⟨n + 1, hg'1⟩) (y'.toFun ⟨n, hg'2⟩)
Proof state after:
case inr.intro.exists_smul_eq.intro.intro.intro.inr
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 n ↪ α
x' : Fin (Fintype.card α) ↪ α
hx' : Function.Embedding.trans (Fin.castLEEmb hn_le).toEmbedding x' = x
y' : Fin (Fintype.card α) ↪ α
hy' : Function.Embedding.trans (Fin.castLEEmb hn_le).toEmbedding y' = y
heq : ∀ (x y : Fin (Fintype.card α) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
g : Equiv.Perm α
hg : g • x' = y'
h : Equiv.Perm.sign g = -1
hg'1 : n + 1 < Fintype.card α
hg'2 : n < Fintype.card α
g' : Equiv.Perm α := Equiv.swap (y'.toFun { val := n + 1, isLt := hg'1 }) (y'.toFun { val := n, isLt := hg'2 })
⊢ ∃ g, g • x = y
Theorem: MulAction.IsMultiplyPretransitive.alternatingGroup_of_sub_two
Proof state before:
case inr.intro.exists_smul_eq.intro.intro.intro.inr
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 n ↪ α
x' : Fin (Fintype.card α) ↪ α
hx' : Function.Embedding.trans (Fin.castLEEmb hn_le).toEmbedding x' = x
y' : Fin (Fintype.card α) ↪ α
hy' : Function.Embedding.trans (Fin.castLEEmb hn_le).toEmbedding y' = y
heq : ∀ (x y : Fin (Fintype.card α) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
g : Equiv.Perm α
hg : g • x' = y'
h : Equiv.Perm.sign g = -1
hg'1 : n + 1 < Fintype.card α
hg'2 : n < Fintype.card α
g' : Equiv.Perm α := Equiv.swap (y'.toFun { val := n + 1, isLt := hg'1 }) (y'.toFun { val := n, isLt := hg'2 })
⊢ ∃ g, g • x = y
Tactic:
have hg' : Equiv.Perm.sign g' = -1 := by
  rw [Equiv.Perm.IsSwap.sign_eq]
  use y'.toFun ⟨n + 1, hg'1⟩; use y'.toFun ⟨n, hg'2⟩
  simp only [toFun_eq_coe, ne_eq, EmbeddingLike.apply_eq_iff_eq, Fin.mk.injEq,
    add_right_eq_self, one_ne_zero, not_false_eq_true, and_self, g']
Proof state after:
case inr.intro.exists_smul_eq.intro.intro.intro.inr
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 n ↪ α
x' : Fin (Fintype.card α) ↪ α
hx' : Function.Embedding.trans (Fin.castLEEmb hn_le).toEmbedding x' = x
y' : Fin (Fintype.card α) ↪ α
hy' : Function.Embedding.trans (Fin.castLEEmb hn_le).toEmbedding y' = y
heq : ∀ (x y : Fin (Fintype.card α) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
g : Equiv.Perm α
hg : g • x' = y'
h : Equiv.Perm.sign g = -1
hg'1 : n + 1 < Fintype.card α
hg'2 : n < Fintype.card α
g' : Equiv.Perm α := Equiv.swap (y'.toFun { val := n + 1, isLt := hg'1 }) (y'.toFun { val := n, isLt := hg'2 })
hg' : Equiv.Perm.sign g' = -1
⊢ ∃ g, g • x = y