Theorem: MulAction.IsMultiplyPretransitive.alternatingGroup_of_sub_two (Jordan/MultipleTransitivity.lean)

State before:
M : Type ?u.254050
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ IsMultiplyPretransitive (↥(alternatingGroup α)) α (Fintype.card α - 2)
Tactic:
cases' lt_or_ge (Fintype.card α) 2 with h2 h2
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 α)) α (Fintype.card α - 2)

case inr
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)

State before:
case inr
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:
obtain ⟨n, hn⟩ := Nat.le.dest h2
State after:
case inr.intro
M : Type ?u.254050
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h2 : Fintype.card α ≥ 2
n : ℕ
hn : 2 + n = Fintype.card α
⊢ IsMultiplyPretransitive (↥(alternatingGroup α)) α (Fintype.card α - 2)

State before:
case inr.intro
M : Type ?u.254050
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h2 : Fintype.card α ≥ 2
n : ℕ
hn : 2 + n = Fintype.card α
⊢ IsMultiplyPretransitive (↥(alternatingGroup α)) α (Fintype.card α - 2)
Tactic:
have hn' : Fintype.card α - 2 = n := tsub_eq_of_eq_add_rev hn.symm
State after:
case inr.intro
M : Type ?u.254050
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h2 : Fintype.card α ≥ 2
n : ℕ
hn : 2 + n = Fintype.card α
hn' : Fintype.card α - 2 = n
⊢ IsMultiplyPretransitive (↥(alternatingGroup α)) α (Fintype.card α - 2)

State before:
case inr.intro
M : Type ?u.254050
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h2 : Fintype.card α ≥ 2
n : ℕ
hn : 2 + n = Fintype.card α
hn' : Fintype.card α - 2 = n
⊢ IsMultiplyPretransitive (↥(alternatingGroup α)) α (Fintype.card α - 2)
Tactic:
rw [add_comm] at hn
State after:
case inr.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
⊢ IsMultiplyPretransitive (↥(alternatingGroup α)) α (Fintype.card α - 2)

State before:
case inr.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
⊢ IsMultiplyPretransitive (↥(alternatingGroup α)) α (Fintype.card α - 2)
Tactic:
have hn_le : n ≤ Fintype.card α := by rw [← hn]; exact le_self_add
State after:
case inr.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 α
⊢ IsMultiplyPretransitive (↥(alternatingGroup α)) α (Fintype.card α - 2)

State before:
case inr.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 α
⊢ IsMultiplyPretransitive (↥(alternatingGroup α)) α (Fintype.card α - 2)
Tactic:
apply IsPretransitive.mk
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 (Fintype.card α - 2) ↪ α), ∃ g, g • x = y

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']
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

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
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

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
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

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
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

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
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

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'
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

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
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

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)]
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

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
State after:
no goals

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]
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

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
State after:
no goals

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⟩
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

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
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

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]
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

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]
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

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
State after:
no goals

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)
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

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
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

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⟩)
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

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']
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

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, ?_⟩
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 α

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 := ?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 α
Tactic:
swap
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
⊢ g' * g ∈ alternatingGroup α

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

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
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

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
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

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]
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

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]
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

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]
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))

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]
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))

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]
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)

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
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 }

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]
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

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)
State after:
no goals

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
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

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
State after:
no goals

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]
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'

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⟩
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

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⟩
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 })

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']
State after:
no goals

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]
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

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']
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

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
State after:
no goals

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
State after:
no goals

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]
State after:
no goals

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
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

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
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

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)
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

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
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

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
State after:
no goals

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
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

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, isLt := hg'2 }
⊢ False
Tactic:
simp only [toFun_eq_coe, EmbeddingLike.apply_eq_iff_eq,
   ← Fin.val_inj, Fin.coe_castLE] at h
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
⊢ False

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
⊢ False
Tactic:
apply lt_irrefl n
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
⊢ n < n

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
⊢ n < n
Tactic:
convert i.prop
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
⊢ n = ↑i

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
⊢ n = ↑i
Tactic:
exact h.symm
State after:
no goals