internlm/Lean-Github huggingface dataset:
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 })
hg' : Equiv.Perm.sign g' = -1
⊢ ∃ g, g • x = y
Tactic:
use ⟨g' * g, ?_⟩
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
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
⊢ { val := g' * g, property := ?w } • x = y

case w
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 ∈ alternatingGroup α
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
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
⊢ { val := g' * 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
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
i : Fin n
⊢ ({ val := g' * 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
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
i : Fin n
⊢ ({ val := g' * g, property := ⋯ } • x) i = y i
Tactic:
suffices (g' * g) • x i = y i by exact this
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
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
i : Fin n
⊢ (g' * g) • 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
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
i : Fin n
⊢ (g' * g) • x i = y i
Tactic:
simp only [toFun_eq_coe, Equiv.Perm.smul_def, Equiv.Perm.coe_mul, Function.comp_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
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
i : Fin n
⊢ g' (g (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
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
i : Fin n
⊢ g' (g (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
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
i : Fin n
⊢ g' (g ((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
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
i : Fin n
⊢ g' (g ((Function.Embedding.trans (Fin.castLEEmb hn_le).toEmbedding x') i)) =
    (Function.Embedding.trans (Fin.castLEEmb hn_le).toEmbedding (g • x')) i
Tactic:
simp only [smul_apply, Equiv.Perm.smul_def, Fin.castLEEmb_toEmbedding, trans_apply, coeFn_mk]
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
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
i : Fin n
⊢ g' (g (x' (Fin.castLE hn_le i))) = g (x' (Fin.castLE hn_le 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
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
i : Fin n
⊢ g' (g (x' (Fin.castLE hn_le i))) = g (x' (Fin.castLE hn_le i))
Tactic:
have : ∀ i, g (x' i) = y' i := fun i ↦ by
  rw [← hg, smul_apply, Equiv.Perm.smul_def]
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
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
i : Fin n
this : ∀ (i : Fin (Fintype.card α)), g (x' i) = y' i
⊢ g' (g (x' (Fin.castLE hn_le i))) = g (x' (Fin.castLE hn_le 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
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
i : Fin n
this : ∀ (i : Fin (Fintype.card α)), g (x' i) = y' i
⊢ g' (g (x' (Fin.castLE hn_le i))) = g (x' (Fin.castLE hn_le i))
Tactic:
simp only [← Equiv.Perm.smul_def, ← smul_apply, 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
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
i : Fin n
this : ∀ (i : Fin (Fintype.card α)), g (x' i) = y' i
⊢ (g' • y') (Fin.castLE hn_le i) = y' (Fin.castLE hn_le 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
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
i : Fin n
this : ∀ (i : Fin (Fintype.card α)), g (x' i) = y' i
⊢ (g' • y') (Fin.castLE hn_le i) = y' (Fin.castLE hn_le i)
Tactic:
apply Equiv.swap_apply_of_ne_of_ne
Proof state after:
case h.h.a
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
i : Fin n
this : ∀ (i : Fin (Fintype.card α)), g (x' i) = y' i
⊢ y' (Fin.castLE hn_le i) ≠ y'.toFun { val := n + 1, isLt := hg'1 }

case h.h.a
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
i : Fin n
this : ∀ (i : Fin (Fintype.card α)), g (x' i) = y' i
⊢ y' (Fin.castLE hn_le i) ≠ y'.toFun { val := n, isLt := hg'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
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
⊢ n + 1 < 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
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
⊢ n + 1 < 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
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
⊢ n + 1 < n + 2
Tactic:
exact Nat.lt.base (n + 1)
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
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 α
⊢ n < Fintype.card α
Tactic:
apply lt_trans _ hg'1
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
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 α
⊢ n < n + 1
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
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 α
⊢ n < n + 1
Tactic:
exact lt_add_one n
Proof state after:
no goals