internlm/Lean-Github huggingface dataset:
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 α
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 })
⊢ Equiv.Perm.sign g' = -1
Tactic:
rw [Equiv.Perm.IsSwap.sign_eq]
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 α
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 })
⊢ Equiv.Perm.IsSwap g'
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 α
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 })
⊢ Equiv.Perm.IsSwap g'
Tactic:
use y'.toFun ⟨n + 1, hg'1⟩
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 })
⊢ ∃ y, y'.toFun { val := n + 1, isLt := hg'1 } ≠ y ∧ g' = Equiv.swap (y'.toFun { val := n + 1, isLt := hg'1 }) 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
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 })
⊢ ∃ y, y'.toFun { val := n + 1, isLt := hg'1 } ≠ y ∧ g' = Equiv.swap (y'.toFun { val := n + 1, isLt := hg'1 }) y
Tactic:
use y'.toFun ⟨n, hg'2⟩
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 })
⊢ y'.toFun { val := n + 1, isLt := hg'1 } ≠ y'.toFun { val := n, isLt := hg'2 } ∧
    g' = Equiv.swap (y'.toFun { val := n + 1, isLt := hg'1 }) (y'.toFun { val := n, isLt := hg'2 })
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 })
⊢ y'.toFun { val := n + 1, isLt := hg'1 } ≠ y'.toFun { val := n, isLt := hg'2 } ∧
    g' = Equiv.swap (y'.toFun { val := n + 1, isLt := hg'1 }) (y'.toFun { val := n, isLt := hg'2 })
Tactic:
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:
no goals
Theorem: MulAction.IsMultiplyPretransitive.alternatingGroup_of_sub_two
Proof state before:
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 α
Tactic:
rw [Equiv.Perm.mem_alternatingGroup]
Proof state after:
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
⊢ Equiv.Perm.sign (g' * g) = 1
Theorem: MulAction.IsMultiplyPretransitive.alternatingGroup_of_sub_two
Proof state before:
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
⊢ Equiv.Perm.sign (g' * g) = 1
Tactic:
simp only [Equiv.Perm.sign_mul, h, hg']
Proof state after:
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
⊢ -1 * -1 = 1
Theorem: MulAction.IsMultiplyPretransitive.alternatingGroup_of_sub_two
Proof state before:
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
⊢ -1 * -1 = 1
Tactic:
norm_num
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 α
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 : (g' * g) • x i = y i
⊢ ({ val := g' * g, property := ⋯ } • x) i = y i
Tactic:
exact this
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 α
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
i : Fin (Fintype.card α)
⊢ g (x' i) = y' i
Tactic:
rw [← hg, smul_apply, Equiv.Perm.smul_def]
Proof state after:
no goals
Theorem: MulAction.IsMultiplyPretransitive.alternatingGroup_of_sub_two
Proof state before:
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 }
Tactic:
intro h
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
h : y' (Fin.castLE hn_le i) = y'.toFun { val := n + 1, isLt := hg'1 }
⊢ False
Theorem: MulAction.IsMultiplyPretransitive.alternatingGroup_of_sub_two
Proof state before:
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
h : y' (Fin.castLE hn_le i) = y'.toFun { val := n + 1, isLt := hg'1 }
⊢ False
Tactic:
simp only [toFun_eq_coe, EmbeddingLike.apply_eq_iff_eq,
   ← Fin.val_inj, Fin.coe_castLE] at h
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
h : ↑i = n + 1
⊢ False
Theorem: MulAction.IsMultiplyPretransitive.alternatingGroup_of_sub_two
Proof state before:
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
h : ↑i = n + 1
⊢ False
Tactic:
apply not_lt.mpr (le_succ n)
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
h : ↑i = n + 1
⊢ succ n < n
Theorem: MulAction.IsMultiplyPretransitive.alternatingGroup_of_sub_two
Proof state before:
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
h : ↑i = n + 1
⊢ succ n < n
Tactic:
convert i.prop
Proof state after:
case h.e'_3
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
h : ↑i = n + 1
⊢ succ n = ↑i
Theorem: MulAction.IsMultiplyPretransitive.alternatingGroup_of_sub_two
Proof state before:
case h.e'_3
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
h : ↑i = n + 1
⊢ succ n = ↑i
Tactic:
exact h.symm
Proof state after:
no goals
Theorem: MulAction.IsMultiplyPretransitive.alternatingGroup_of_sub_two
Proof state before:
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 }
Tactic:
intro h
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
h : y' (Fin.castLE hn_le i) = y'.toFun { val := n, isLt := hg'2 }
⊢ False